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