c This Formular is generated by mcnf
c
c    horn? no 
c    forced? no 
c    mixed sat? no 
c    clause length = 3 
c
p cnf 250  1065 
 146 -130 78 0
-227 -14 -201 0
99 -120 221 0
-226 -209 -238 0
106 -66 -122 0
47 -145 -5 0
-182 162 184 0
82 -173 220 0
95 -195 -53 0
220 28 33 0
-217 142 177 0
141 197 23 0
-175 -160 -20 0
239 -57 183 0
8 -109 -134 0
-72 -166 -120 0
-109 28 -82 0
-228 -27 70 0
-235 -159 -89 0
-23 -208 87 0
134 70 202 0
-139 176 -116 0
-129 34 -244 0
230 -16 74 0
-46 206 -232 0
169 -246 48 0
208 138 41 0
40 -235 -131 0
198 -163 177 0
45 -27 -65 0
5 -78 -172 0
-167 -154 -58 0
-55 17 149 0
97 248 -244 0
-133 63 -1 0
124 -92 -237 0
215 61 88 0
186 73 -80 0
-165 -104 -127 0
-133 -8 207 0
43 79 136 0
213 87 91 0
-114 -44 -181 0
-73 -42 -41 0
93 -82 -174 0
-93 8 207 0
8 250 167 0
-206 163 -69 0
73 -178 -237 0
-30 219 -19 0
82 110 241 0
119 -96 27 0
-59 148 239 0
72 -107 -23 0
245 -250 -118 0
-246 35 245 0
14 -192 178 0
117 -35 19 0
-200 234 -159 0
-122 37 129 0
124 46 -115 0
-202 45 130 0
250 202 140 0
-70 -7 34 0
-108 101 -113 0
-67 213 -207 0
-120 33 249 0
-162 -70 243 0
-250 133 -78 0
86 212 -16 0
138 14 134 0
-188 129 155 0
40 -202 -92 0
-77 130 -100 0
57 194 -173 0
-250 -152 237 0
-5 159 211 0
182 -135 203 0
241 -244 213 0
-51 204 14 0
-197 -25 -180 0
-16 163 -58 0
-227 4 -37 0
-12 19 198 0
45 -160 49 0
86 79 100 0
-165 28 -170 0
-125 -230 246 0
115 -169 -42 0
-158 -188 -59 0
-30 81 21 0
136 -11 61 0
47 107 -43 0
66 -133 120 0
6 103 -200 0
6 -88 26 0
58 -103 132 0
-182 -205 -221 0
176 -63 122 0
57 -175 -169 0
-201 245 65 0
-98 -78 135 0
94 128 -248 0
-53 28 -58 0
-241 -129 -151 0
-136 85 -134 0
233 -158 -232 0
-160 230 -55 0
-152 97 185 0
185 -11 135 0
224 56 -104 0
-11 239 -72 0
-170 -16 -188 0
132 74 79 0
-72 217 110 0
225 -25 85 0
242 -143 -80 0
-22 54 201 0
192 -160 -196 0
-119 47 -194 0
8 227 -20 0
184 47 -45 0
-199 131 233 0
-22 32 -170 0
-195 -170 -191 0
-133 -155 -171 0
54 -180 -22 0
27 141 13 0
-20 61 -134 0
84 222 104 0
-218 -242 -156 0
-113 198 82 0
16 72 -165 0
131 101 15 0
199 -125 13 0
-54 117 115 0
-111 118 206 0
-216 18 -73 0
83 -177 5 0
-139 170 152 0
-244 -186 -138 0
63 58 102 0
220 78 175 0
182 -50 -84 0
167 128 48 0
-93 62 -52 0
-126 77 50 0
80 -51 187 0
-83 80 109 0
45 25 226 0
208 -186 106 0
1 42 197 0
159 98 -78 0
154 186 -56 0
111 -146 189 0
-131 -196 -218 0
107 206 -175 0
-81 164 -41 0
-135 -162 -78 0
104 35 75 0
75 -2 -8 0
175 -94 -167 0
41 -228 85 0
225 -20 -4 0
232 65 213 0
118 -181 86 0
87 -147 167 0
175 36 -40 0
102 -92 -195 0
-34 -125 220 0
-81 -48 -7 0
-239 10 126 0
218 -188 157 0
-182 -49 115 0
32 -189 133 0
77 -16 111 0
-63 170 43 0
-60 42 -243 0
240 230 -239 0
-113 -138 81 0
-59 216 -32 0
-202 113 -133 0
49 111 249 0
-230 -66 -26 0
-111 33 -20 0
-208 87 -125 0
202 -207 36 0
41 249 197 0
85 -18 89 0
243 96 42 0
172 -245 -156 0
220 184 117 0
92 58 65 0
-62 181 121 0
-158 34 -202 0
-19 218 -233 0
-85 -234 -149 0
18 81 224 0
185 180 1 0
161 -237 76 0
101 -205 90 0
-49 -213 87 0
114 181 156 0
-158 198 204 0
200 164 -19 0
-147 -127 160 0
-90 -10 -2 0
-1 -71 96 0
-180 -66 56 0
-165 -173 -222 0
139 94 124 0
87 170 94 0
3 96 121 0
207 182 95 0
70 -229 -240 0
-38 51 31 0
246 185 30 0
139 25 -221 0
-38 78 -153 0
-201 -160 195 0
-128 -238 157 0
18 -145 -189 0
-172 -121 235 0
114 168 185 0
-233 -1 -183 0
-34 -68 121 0
-194 244 -164 0
94 213 -18 0
186 -218 65 0
144 -218 116 0
210 178 124 0
100 -61 -93 0
-160 38 -96 0
-75 -51 -168 0
5 -64 119 0
177 -100 192 0
-150 29 120 0
-125 -203 -101 0
170 204 -17 0
240 -98 -1 0
122 -144 -241 0
-122 94 -199 0
-55 -210 194 0
-121 -100 27 0
74 177 -217 0
-215 -156 79 0
125 91 -116 0
65 138 160 0
81 163 -189 0
-226 -124 52 0
-128 163 -242 0
229 243 -52 0
-45 -131 21 0
-43 219 226 0
-107 -51 149 0
-245 121 8 0
-197 -55 -118 0
-132 -193 -63 0
-215 -190 -169 0
215 -28 45 0
-209 -180 -159 0
-92 112 -41 0
-141 -241 132 0
155 108 -217 0
67 -13 165 0
149 85 -30 0
43 143 -58 0
-22 -242 159 0
-181 -100 -159 0
-35 240 220 0
49 250 -181 0
25 -100 -124 0
-249 204 -216 0
208 -37 -10 0
74 -218 172 0
139 215 21 0
-50 -68 177 0
147 149 -62 0
23 -13 -205 0
-214 -204 106 0
-157 -136 237 0
-6 -4 -98 0
41 -74 -146 0
-21 -208 214 0
-113 203 46 0
-241 -246 -178 0
8 179 136 0
-103 151 136 0
-199 -24 29 0
5 112 221 0
93 70 -54 0
152 -54 155 0
-99 11 -165 0
56 208 -191 0
101 -124 -51 0
-130 17 -200 0
160 -187 -50 0
-79 73 -219 0
161 -113 185 0
41 47 178 0
-221 -247 -118 0
-166 -90 91 0
-174 -232 -137 0
120 -136 56 0
109 29 -48 0
138 90 162 0
-159 -176 181 0
-63 65 -199 0
-76 -175 -197 0
239 190 -245 0
-163 -149 -72 0
76 -85 -94 0
137 -41 242 0
-226 -73 206 0
120 -192 57 0
25 129 -15 0
10 -122 -9 0
31 -82 25 0
54 141 94 0
-126 182 -238 0
49 -71 -82 0
-238 176 -249 0
230 59 -25 0
27 -134 -81 0
-166 -19 76 0
-107 250 193 0
65 51 34 0
7 26 -122 0
221 -57 -86 0
195 -93 -247 0
143 102 198 0
-193 -104 62 0
-39 -172 -134 0
-112 -173 -221 0
-176 -169 -239 0
121 -82 85 0
-80 109 -227 0
-249 125 64 0
46 146 -189 0
-162 -20 82 0
-135 -63 103 0
93 211 -128 0
212 -100 88 0
-42 28 17 0
-144 205 130 0
247 -240 135 0
-119 51 226 0
210 82 -177 0
-168 -149 -186 0
-45 -23 183 0
-247 245 -27 0
147 -213 -36 0
199 -169 237 0
-33 133 242 0
-197 112 -143 0
-168 -33 -135 0
-180 -60 -191 0
121 130 68 0
-200 37 -164 0
-62 202 -92 0
-95 -250 161 0
-207 124 135 0
47 209 -196 0
146 -15 -237 0
-41 -18 194 0
-10 66 -24 0
-246 -2 -91 0
-197 196 -138 0
92 205 -217 0
69 -55 -191 0
37 197 228 0
28 -113 -24 0
-47 190 -118 0
137 -172 -132 0
-27 69 -202 0
129 -117 -85 0
-130 205 65 0
-76 120 247 0
121 191 -250 0
149 70 -67 0
238 165 -14 0
24 151 -146 0
-146 129 -88 0
-220 -192 82 0
218 -93 -195 0
-182 179 -145 0
136 24 67 0
-249 7 -87 0
118 -13 -60 0
54 -48 129 0
-21 -169 -4 0
-101 192 237 0
-130 -60 -105 0
195 -75 -187 0
189 215 -191 0
-177 74 99 0
100 140 209 0
192 151 71 0
-221 62 102 0
-51 4 227 0
172 -248 -103 0
-37 27 31 0
8 53 202 0
-107 -69 -130 0
-220 27 199 0
226 -189 -18 0
-219 -246 221 0
50 250 -135 0
-69 -184 53 0
144 112 56 0
-113 33 -12 0
75 80 -217 0
128 -127 207 0
247 -197 218 0
-77 -39 221 0
-205 244 -61 0
-187 -199 1 0
111 -123 205 0
103 -132 -29 0
-180 -7 213 0
-179 93 -87 0
-161 -246 -160 0
-240 10 -27 0
27 -180 -43 0
229 180 191 0
-8 211 121 0
158 -15 -241 0
58 173 172 0
28 -180 126 0
61 -110 -78 0
-35 -197 -155 0
-236 -102 189 0
121 -228 25 0
126 8 -205 0
-100 -152 -244 0
121 187 129 0
-199 77 174 0
239 -174 72 0
-39 92 -59 0
129 193 -50 0
-55 240 -139 0
-6 214 57 0
23 90 34 0
-145 -142 -92 0
-102 -13 -127 0
-104 189 -235 0
223 128 213 0
-139 -79 153 0
173 68 146 0
199 122 -44 0
71 127 -116 0
55 90 -115 0
-81 -8 -250 0
-238 104 241 0
-164 -67 -132 0
-134 213 -31 0
238 72 239 0
23 -170 116 0
-196 140 149 0
196 -186 -83 0
233 27 -186 0
-163 14 26 0
9 -138 -34 0
171 106 76 0
-86 238 -34 0
142 48 -202 0
31 -224 241 0
-171 135 -244 0
-141 -179 10 0
63 83 39 0
-22 -143 -152 0
-201 1 187 0
47 -228 -197 0
-194 72 -134 0
5 -100 -214 0
147 -217 107 0
-12 140 -78 0
-11 -128 113 0
162 111 -116 0
-176 68 -3 0
-105 7 164 0
38 66 243 0
1 -24 202 0
157 -142 230 0
175 -112 177 0
105 229 -38 0
-104 99 -134 0
220 137 159 0
239 -9 8 0
186 56 -162 0
236 -162 -112 0
164 82 244 0
-4 21 243 0
-191 93 119 0
-248 -39 -119 0
-42 -136 87 0
48 72 -145 0
-147 123 216 0
250 -225 162 0
181 170 -53 0
224 121 -88 0
124 71 -67 0
-214 -8 57 0
-248 146 -67 0
-173 -194 -158 0
177 215 -107 0
9 -148 200 0
10 129 -69 0
-158 -56 111 0
213 137 67 0
-106 38 24 0
92 -61 196 0
-102 -145 240 0
-135 120 103 0
-119 -56 203 0
244 -32 -102 0
64 -85 214 0
121 -228 -244 0
158 32 -75 0
76 146 -224 0
-93 74 -181 0
97 -154 -9 0
-159 -33 112 0
-107 50 40 0
100 -135 212 0
-222 -5 -115 0
77 46 108 0
219 -14 -53 0
-88 -23 245 0
-194 -54 189 0
197 -98 106 0
16 -77 -99 0
-143 -130 -218 0
-141 -48 157 0
-190 118 164 0
229 220 -137 0
-137 -46 213 0
-189 62 -3 0
-40 147 -9 0
-57 222 51 0
-9 -78 44 0
-32 48 120 0
117 -222 100 0
81 168 3 0
23 -171 8 0
-147 149 185 0
-14 75 -144 0
171 184 148 0
-126 -133 194 0
-164 244 228 0
-28 -214 15 0
-58 167 -133 0
127 -220 -134 0
-51 -116 68 0
51 159 33 0
-145 107 -63 0
218 126 -132 0
-50 -203 -151 0
-119 27 7 0
227 71 -159 0
-108 -244 -94 0
135 -121 37 0
197 -21 65 0
-238 73 69 0
-245 -235 160 0
-140 102 -1 0
-145 -156 -24 0
45 -119 -14 0
-150 -204 40 0
-57 192 34 0
-224 -234 -128 0
-129 112 -55 0
-146 -88 95 0
-127 97 -15 0
-215 121 -153 0
-25 61 -230 0
51 164 58 0
-82 211 -189 0
238 -248 232 0
213 128 167 0
111 149 64 0
36 -102 13 0
-195 -38 -39 0
-19 -202 156 0
-46 165 197 0
215 -141 221 0
-128 16 123 0
217 -55 117 0
164 -207 -33 0
139 -2 -150 0
-157 -179 70 0
148 -84 -66 0
-100 -190 -230 0
48 -109 125 0
-65 -67 83 0
-145 -59 -225 0
15 -84 80 0
-203 178 -235 0
216 -231 27 0
111 -226 -189 0
-220 187 -210 0
198 206 -156 0
33 -12 -71 0
-170 -146 173 0
-52 -57 -241 0
96 -121 185 0
228 198 231 0
38 -18 -194 0
-225 93 -60 0
-222 -85 -197 0
188 57 -1 0
-198 64 -191 0
-51 -106 -214 0
-132 135 4 0
81 -26 123 0
-158 176 -141 0
151 -245 40 0
37 -224 214 0
-162 100 8 0
204 -121 88 0
160 -56 250 0
27 -114 -43 0
-175 -241 -189 0
12 153 6 0
-82 23 167 0
-243 8 120 0
41 -84 -196 0
-48 -74 -140 0
-142 -224 34 0
194 -75 -125 0
174 -236 231 0
126 19 121 0
221 -149 95 0
241 -27 30 0
127 -118 97 0
-224 -151 76 0
242 -70 -73 0
-133 -112 -73 0
33 -213 -234 0
-85 112 25 0
21 86 152 0
-150 -31 165 0
-146 25 -167 0
-176 34 100 0
67 181 198 0
-93 -132 -147 0
89 128 217 0
-59 -245 -134 0
-113 139 169 0
-48 -114 195 0
-56 47 -188 0
139 -129 -43 0
214 -191 137 0
-232 -27 239 0
165 37 149 0
165 89 -149 0
18 179 -68 0
203 247 140 0
-190 -76 81 0
213 -141 -107 0
214 164 228 0
50 34 -198 0
-67 -47 228 0
10 76 148 0
161 216 14 0
-157 -39 -177 0
154 201 226 0
82 134 117 0
131 -100 78 0
-151 101 46 0
177 -25 160 0
46 -63 11 0
-91 245 212 0
210 -184 151 0
-117 112 191 0
-34 201 -84 0
4 99 -56 0
92 -211 214 0
106 -127 -201 0
96 -31 23 0
-96 -226 248 0
-173 149 -229 0
29 -229 -161 0
-188 -23 128 0
39 -218 61 0
171 137 -105 0
23 -228 54 0
198 192 -51 0
-36 -211 -220 0
202 192 124 0
-120 189 -171 0
-129 61 204 0
5 10 59 0
-2 153 -43 0
128 18 -138 0
-36 149 -93 0
-182 -1 192 0
2 -188 -13 0
-142 -246 33 0
129 95 -116 0
171 132 -44 0
144 -20 167 0
89 -156 38 0
231 107 -26 0
-111 -169 -87 0
-122 105 -64 0
-81 11 172 0
-97 185 -232 0
-164 15 53 0
181 139 -11 0
200 -237 -50 0
165 -233 178 0
-161 -77 -208 0
-89 124 7 0
-233 244 173 0
-189 -210 -24 0
155 -138 -159 0
105 134 -215 0
54 114 48 0
94 -237 104 0
53 -169 75 0
-2 -61 -184 0
49 247 40 0
-188 -111 -179 0
-95 14 -171 0
-63 -81 -69 0
184 159 -35 0
24 -118 -173 0
129 68 91 0
-241 148 24 0
-61 159 133 0
-105 229 198 0
-66 -120 135 0
218 62 -84 0
69 110 -33 0
143 -81 37 0
-65 -61 13 0
19 -26 -164 0
225 -20 -13 0
-101 248 181 0
86 99 -96 0
-175 124 -239 0
-216 96 -171 0
59 77 150 0
-219 -210 36 0
209 237 -153 0
-232 -21 -86 0
115 173 8 0
165 -111 187 0
-102 151 -5 0
192 9 -142 0
-56 44 -9 0
53 -128 -139 0
170 -78 -51 0
-151 -243 -132 0
-60 -72 190 0
-190 221 45 0
165 -163 186 0
243 -142 176 0
-25 149 -59 0
87 113 -10 0
27 -4 145 0
130 -117 -168 0
-163 33 -88 0
-230 -179 -213 0
-222 -94 162 0
23 161 -232 0
224 -230 155 0
201 62 78 0
-193 -247 36 0
-58 103 110 0
55 -122 177 0
-23 -189 -20 0
222 -177 -231 0
-157 158 -245 0
208 120 229 0
84 -143 -200 0
50 -202 104 0
-239 -100 -7 0
-218 -56 -129 0
89 205 -61 0
145 105 -42 0
8 -165 172 0
-192 -222 150 0
169 158 104 0
239 208 56 0
-197 168 182 0
-209 -19 -211 0
180 72 166 0
-127 -188 -14 0
-80 224 90 0
-212 -219 32 0
-191 165 -61 0
96 225 12 0
-118 -180 -218 0
14 239 -176 0
-216 -86 166 0
39 171 38 0
40 -168 57 0
81 -47 -38 0
-1 191 186 0
124 9 146 0
-162 -45 46 0
31 -183 -35 0
-196 64 -11 0
181 112 -129 0
176 -162 -180 0
-196 112 230 0
-108 -92 55 0
106 124 -101 0
-54 -37 75 0
103 -79 -24 0
-218 95 -86 0
70 193 -238 0
162 190 -39 0
225 109 183 0
-161 -143 164 0
-159 143 -158 0
-141 159 185 0
44 -194 209 0
-228 -180 -122 0
-245 139 -54 0
-221 -232 -121 0
120 -117 -119 0
73 39 94 0
-45 98 -228 0
-78 -2 -94 0
-110 131 148 0
191 -128 -240 0
210 5 -24 0
102 -80 -242 0
-35 -73 -1 0
-45 63 42 0
65 233 177 0
39 1 -113 0
-206 -155 -228 0
-197 -19 -46 0
-109 -192 62 0
198 -87 -125 0
41 -129 -95 0
59 87 -220 0
-203 -89 -238 0
-9 177 -48 0
-106 7 238 0
212 -50 -244 0
48 -211 12 0
-210 169 -170 0
-184 -77 -82 0
132 90 -148 0
-235 30 206 0
-154 -134 69 0
-246 110 205 0
-71 -241 100 0
-43 -103 -174 0
97 -205 22 0
-161 86 -241 0
-15 -247 1 0
242 -233 48 0
176 177 121 0
91 213 -47 0
-219 -175 66 0
99 -168 -62 0
-157 -129 205 0
223 -146 -16 0
-186 -84 94 0
211 164 -34 0
-92 222 -105 0
126 -227 120 0
-170 -155 -234 0
-66 -184 62 0
19 -126 171 0
239 -244 14 0
-84 22 -61 0
42 -23 -146 0
3 -23 -77 0
-71 201 118 0
34 240 -13 0
-131 167 181 0
184 -161 55 0
223 189 -35 0
-41 74 -167 0
-178 -99 -159 0
99 -27 158 0
62 -151 187 0
-128 202 61 0
129 -42 -138 0
214 127 -51 0
114 -165 -223 0
-48 4 91 0
-107 -248 23 0
231 38 65 0
70 -47 -140 0
66 33 120 0
228 102 -67 0
-139 193 185 0
-185 -90 -132 0
-13 -27 -11 0
-109 -212 213 0
41 227 -120 0
-43 183 148 0
-71 29 97 0
-167 -41 -81 0
108 52 -190 0
-88 -70 -165 0
162 -219 -142 0
-66 -17 15 0
216 135 83 0
-25 -170 77 0
152 77 176 0
-26 194 71 0
-153 -68 34 0
209 -196 -137 0
-66 -18 118 0
-248 -133 -184 0
26 -225 -160 0
-114 -44 -231 0
149 -169 -157 0
234 -24 -167 0
-208 164 -31 0
108 -113 204 0
-180 -73 140 0
121 -118 -18 0
176 -136 -250 0
240 195 -79 0
-249 -194 -29 0
-48 140 61 0
37 -171 148 0
31 -123 -185 0
196 -204 -116 0
-190 -221 145 0
207 -221 245 0
-47 -194 -215 0
-244 29 -35 0
-100 5 -202 0
167 -219 146 0
-166 -144 -39 0
-205 -207 -141 0
82 144 -167 0
114 -172 231 0
-240 54 -229 0
-203 -31 -60 0
189 147 176 0
-217 148 220 0
110 -127 214 0
100 182 154 0
244 20 -50 0
-22 200 -138 0
-24 -245 101 0
-36 237 -240 0
99 176 -113 0
22 248 -199 0
-63 72 -159 0
153 43 181 0
117 71 45 0
-37 -168 47 0
79 193 48 0
-237 76 -169 0
82 -178 230 0
70 -47 -86 0
235 189 -73 0
-82 -167 -186 0
-227 181 25 0
83 -159 -227 0
-79 241 203 0
-70 90 -44 0
136 203 -48 0
20 -58 -172 0
93 36 156 0
-226 177 -67 0
34 160 -10 0
207 188 -83 0
-246 29 -222 0
-165 210 -71 0
-210 235 -213 0
-171 235 143 0
-204 -224 105 0
204 11 -240 0
35 -247 -123 0
-2 191 -165 0
-97 -249 225 0
11 -200 -236 0
134 -112 228 0
-36 17 56 0
90 123 227 0
-245 -184 54 0
-231 183 -250 0
-183 182 19 0
219 -90 -17 0
62 88 11 0
-93 87 -31 0
-196 36 -135 0
103 184 -114 0
-122 62 7 0
26 -148 -93 0
-134 -28 22 0
116 120 113 0
184 168 -48 0
-215 160 203 0
226 74 186 0
3 -244 149 0
-101 23 193 0
-78 207 -174 0
-17 -219 -122 0
-8 -165 243 0
-65 236 96 0
-36 111 25 0
-235 151 5 0
-121 43 -227 0
-161 -20 81 0
6 -28 50 0
-104 27 -170 0
-176 -239 -144 0
-189 18 -213 0
-80 171 -244 0
223 -80 -235 0
-81 -34 2 0
-243 87 -245 0
56 206 -160 0
-242 199 -89 0
-191 82 -242 0
-151 -184 206 0
-158 176 -204 0
-44 -117 175 0
-122 126 244 0
124 -52 183 0
-38 127 -219 0
109 186 -77 0
-32 132 -5 0
-1 -207 15 0
96 -42 -176 0
64 -194 29 0
184 44 243 0
-148 137 212 0
41 94 -4 0
180 -183 212 0
8 24 -62 0
93 -239 -41 0
-165 147 32 0
-173 -90 218 0
98 -74 -237 0
-178 -186 221 0
236 -64 15 0
-171 -63 -161 0
77 113 -49 0
100 -136 -16 0
34 122 130 0
30 96 165 0
-58 -42 126 0
-178 71 -177 0
-169 215 101 0
127 85 168 0
107 -117 -124 0
-84 -219 36 0
-25 116 -101 0
167 -10 -181 0
-64 70 -67 0
-9 -183 -21 0
-127 -38 151 0
192 -22 204 0
-9 -140 -54 0
-172 -221 -66 0
-142 211 74 0
-94 -220 65 0
83 74 84 0
-81 124 197 0