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