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