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