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