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