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