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