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