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