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