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