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