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