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