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