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