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