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