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