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