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