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