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