uf250-032.cnf

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