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