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