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