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