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