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