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