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