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