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