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