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