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