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