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