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