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