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