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