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