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