%------------------------------------------------------------------------------
% File : Mace4---2026-6A
% Problem : SYO581+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : mace4 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 09:49:22 AM UTC 2026
% Result : CounterSatisfiable 0.38s 0.67s
% Output : FiniteModel 0.38s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(interp_domain,interpretation-domains,
! [X] :
( X = "d3"
| X = "d2"
| X = "d1"
| X = "d0" ) ).
fof(interp_functions,interpretation-mappings,
( c513 = "d2"
& c512 = "d0"
& c511 = "d0"
& c510 = "d0"
& c509 = "d2"
& c508 = "d2"
& c507 = "d0"
& c506 = "d2"
& c505 = "d0"
& c504 = "d0"
& c503 = "d2"
& c502 = "d3"
& c501 = "d2"
& c500 = "d0"
& c499 = "d2"
& c498 = "d0"
& c497 = "d0"
& c496 = "d0"
& c495 = "d0"
& c494 = "d0"
& c493 = "d0"
& c492 = "d3"
& c491 = "d0"
& c490 = "d0"
& c489 = "d0"
& c488 = "d0"
& c487 = "d0"
& c486 = "d0"
& c485 = "d0"
& c484 = "d2"
& c483 = "d2"
& c482 = "d0"
& c481 = "d0"
& c480 = "d2"
& c479 = "d0"
& c478 = "d0"
& c477 = "d0"
& c476 = "d0"
& c475 = "d0"
& c474 = "d2"
& c473 = "d2"
& c472 = "d0"
& c471 = "d3"
& c470 = "d0"
& c469 = "d2"
& c468 = "d2"
& c467 = "d0"
& c466 = "d0"
& c465 = "d0"
& c464 = "d0"
& c463 = "d3"
& c462 = "d0"
& c461 = "d2"
& c460 = "d2"
& c459 = "d0"
& c458 = "d0"
& c457 = "d2"
& c456 = "d2"
& c455 = "d2"
& c454 = "d0"
& c453 = "d0"
& c452 = "d0"
& c451 = "d2"
& c450 = "d2"
& c449 = "d0"
& c448 = "d0"
& c447 = "d0"
& c446 = "d0"
& c445 = "d0"
& c444 = "d0"
& c443 = "d0"
& c442 = "d0"
& c441 = "d0"
& c440 = "d0"
& c439 = "d2"
& c438 = "d0"
& c437 = "d2"
& c436 = "d0"
& c435 = "d2"
& c434 = "d0"
& c433 = "d0"
& c432 = "d0"
& c431 = "d0"
& c430 = "d0"
& c429 = "d0"
& c428 = "d0"
& c427 = "d0"
& c426 = "d0"
& c425 = "d0"
& c424 = "d0"
& c423 = "d2"
& c422 = "d2"
& c421 = "d3"
& c420 = "d2"
& c419 = "d0"
& c418 = "d0"
& c417 = "d2"
& c416 = "d0"
& c415 = "d0"
& c414 = "d0"
& c413 = "d2"
& c412 = "d2"
& c411 = "d0"
& c410 = "d0"
& c409 = "d0"
& c408 = "d0"
& c407 = "d0"
& c406 = "d0"
& c405 = "d0"
& c404 = "d0"
& c403 = "d0"
& c402 = "d0"
& c401 = "d0"
& c400 = "d0"
& c399 = "d0"
& c398 = "d2"
& c397 = "d0"
& c396 = "d0"
& c395 = "d0"
& c394 = "d0"
& c393 = "d0"
& c392 = "d0"
& c391 = "d0"
& c390 = "d0"
& c389 = "d0"
& c388 = "d2"
& c387 = "d2"
& c386 = "d2"
& c385 = "d0"
& c384 = "d2"
& c383 = "d2"
& c382 = "d0"
& c381 = "d0"
& c380 = "d0"
& c379 = "d0"
& c378 = "d1"
& c377 = "d0"
& c376 = "d0"
& c375 = "d2"
& c374 = "d2"
& c373 = "d0"
& c372 = "d2"
& c371 = "d0"
& c370 = "d0"
& c369 = "d0"
& c368 = "d2"
& c367 = "d2"
& c366 = "d2"
& c365 = "d0"
& c364 = "d3"
& c363 = "d0"
& c362 = "d3"
& c361 = "d2"
& c360 = "d0"
& c359 = "d0"
& c358 = "d0"
& c357 = "d0"
& c356 = "d2"
& c355 = "d0"
& c354 = "d0"
& c353 = "d2"
& c352 = "d2"
& c351 = "d0"
& c350 = "d0"
& c349 = "d0"
& c348 = "d0"
& c347 = "d0"
& c346 = "d0"
& c345 = "d0"
& c344 = "d0"
& c343 = "d0"
& c342 = "d0"
& c341 = "d0"
& c340 = "d0"
& c339 = "d0"
& c338 = "d0"
& c337 = "d0"
& c336 = "d0"
& c335 = "d0"
& c334 = "d0"
& c333 = "d2"
& c332 = "d2"
& c331 = "d0"
& c330 = "d0"
& c329 = "d2"
& c328 = "d0"
& c327 = "d2"
& c326 = "d2"
& c325 = "d0"
& c324 = "d0"
& c323 = "d2"
& c322 = "d2"
& c321 = "d0"
& c320 = "d0"
& c319 = "d0"
& c318 = "d0"
& c317 = "d0"
& c316 = "d2"
& c315 = "d0"
& c314 = "d0"
& c313 = "d0"
& c312 = "d0"
& c311 = "d0"
& c310 = "d0"
& c309 = "d0"
& c308 = "d0"
& c307 = "d0"
& c306 = "d0"
& c305 = "d0"
& c304 = "d0"
& c303 = "d0"
& c302 = "d0"
& c301 = "d0"
& c300 = "d1"
& c299 = "d2"
& c298 = "d2"
& c297 = "d0"
& c296 = "d0"
& c295 = "d0"
& c294 = "d2"
& c293 = "d0"
& c292 = "d0"
& c291 = "d0"
& c290 = "d0"
& c289 = "d0"
& c288 = "d0"
& c287 = "d0"
& c286 = "d0"
& c285 = "d0"
& c284 = "d0"
& c283 = "d0"
& c282 = "d0"
& c281 = "d0"
& c280 = "d0"
& c279 = "d0"
& c278 = "d0"
& c277 = "d0"
& c276 = "d0"
& c275 = "d0"
& c274 = "d0"
& c273 = "d0"
& c272 = "d0"
& c271 = "d0"
& c270 = "d0"
& c269 = "d0"
& c268 = "d0"
& c267 = "d0"
& c266 = "d0"
& c265 = "d0"
& c264 = "d0"
& c263 = "d0"
& c262 = "d0"
& c261 = "d0"
& c260 = "d0"
& c259 = "d0"
& c258 = "d0"
& c257 = "d0"
& c256 = "d0"
& c255 = "d0"
& c254 = "d0"
& c253 = "d0"
& c252 = "d0"
& c251 = "d0"
& c250 = "d0"
& c249 = "d0"
& c248 = "d0"
& c247 = "d0"
& c246 = "d0"
& c245 = "d0"
& c244 = "d0"
& c243 = "d0"
& c242 = "d0"
& c241 = "d0"
& c240 = "d0"
& c239 = "d0"
& c238 = "d0"
& c237 = "d0"
& c236 = "d0"
& c235 = "d0"
& c234 = "d0"
& c233 = "d1"
& c232 = "d1"
& c231 = "d0"
& c230 = "d0"
& c229 = "d0"
& c228 = "d0"
& c227 = "d0"
& c226 = "d0"
& c225 = "d0"
& c224 = "d2"
& c223 = "d2"
& c222 = "d0"
& c221 = "d0"
& c220 = "d0"
& c219 = "d0"
& c218 = "d0"
& c217 = "d0"
& c216 = "d0"
& c215 = "d0"
& c214 = "d0"
& c213 = "d0"
& c212 = "d0"
& c211 = "d0"
& c210 = "d0"
& c209 = "d0"
& c208 = "d0"
& c207 = "d0"
& c206 = "d0"
& c205 = "d0"
& c204 = "d0"
& c203 = "d0"
& c202 = "d0"
& c201 = "d0"
& c200 = "d0"
& c199 = "d0"
& c198 = "d0"
& c197 = "d0"
& c196 = "d0"
& c195 = "d0"
& c194 = "d0"
& c193 = "d0"
& c192 = "d2"
& c191 = "d0"
& c190 = "d0"
& c189 = "d0"
& c188 = "d0"
& c187 = "d0"
& c186 = "d0"
& c185 = "d0"
& c184 = "d0"
& c183 = "d0"
& c182 = "d0"
& c181 = "d0"
& c180 = "d0"
& c179 = "d0"
& c178 = "d0"
& c177 = "d0"
& c176 = "d0"
& c175 = "d0"
& c174 = "d0"
& c173 = "d0"
& c172 = "d0"
& c171 = "d0"
& c170 = "d0"
& c169 = "d0"
& c168 = "d0"
& c167 = "d0"
& c166 = "d0"
& c165 = "d0"
& c164 = "d0"
& c163 = "d0"
& c162 = "d0"
& c161 = "d0"
& c160 = "d0"
& c159 = "d0"
& c158 = "d0"
& c157 = "d0"
& c156 = "d0"
& c155 = "d0"
& c154 = "d0"
& c153 = "d0"
& c152 = "d0"
& c151 = "d0"
& c150 = "d1"
& c149 = "d2"
& c148 = "d0"
& c147 = "d2"
& c146 = "d1"
& c145 = "d2"
& c144 = "d0"
& c143 = "d0"
& c142 = "d2"
& c141 = "d0"
& c140 = "d0"
& c139 = "d0"
& c138 = "d0"
& c137 = "d0"
& c136 = "d0"
& c135 = "d0"
& c134 = "d0"
& c133 = "d0"
& c132 = "d0"
& c131 = "d0"
& c130 = "d1"
& c129 = "d1"
& c128 = "d1"
& c127 = "d0"
& c126 = "d0"
& c125 = "d0"
& c124 = "d0"
& c123 = "d0"
& c122 = "d0"
& c121 = "d0"
& c120 = "d0"
& c119 = "d0"
& c118 = "d0"
& c117 = "d1"
& c116 = "d0"
& c115 = "d0"
& c114 = "d1"
& c113 = "d0"
& c112 = "d2"
& c111 = "d1"
& c110 = "d2"
& c109 = "d0"
& c108 = "d0"
& c107 = "d0"
& c106 = "d0"
& c105 = "d0"
& c104 = "d0"
& c103 = "d1"
& c102 = "d0"
& c101 = "d0"
& c100 = "d0"
& c99 = "d0"
& c98 = "d0"
& c97 = "d0"
& c96 = "d0"
& c95 = "d0"
& c94 = "d0"
& c93 = "d0"
& c92 = "d2"
& c91 = "d0"
& c90 = "d0"
& c89 = "d0"
& c88 = "d0"
& c87 = "d1"
& c86 = "d0"
& c85 = "d2"
& c84 = "d1"
& c83 = "d0"
& c82 = "d0"
& c81 = "d0"
& c80 = "d0"
& c79 = "d2"
& c78 = "d0"
& c77 = "d0"
& c76 = "d0"
& c75 = "d0"
& c74 = "d2"
& c73 = "d0"
& c72 = "d0"
& c71 = "d0"
& c70 = "d0"
& c69 = "d1"
& c68 = "d0"
& c67 = "d0"
& c66 = "d0"
& c65 = "d0"
& c64 = "d0"
& c63 = "d0"
& c62 = "d0"
& c61 = "d0"
& c60 = "d0"
& c59 = "d0"
& c58 = "d0"
& c57 = "d0"
& c56 = "d0"
& c55 = "d0"
& c54 = "d0"
& c53 = "d0"
& c52 = "d0"
& c51 = "d0"
& c50 = "d0"
& c49 = "d3"
& c48 = "d0"
& c47 = "d0"
& c46 = "d0"
& c45 = "d0"
& c44 = "d0"
& c43 = "d0"
& c42 = "d0"
& c41 = "d0"
& c40 = "d0"
& c39 = "d1"
& c38 = "d0"
& c37 = "d0"
& c36 = "d0"
& c35 = "d0"
& c34 = "d0"
& c33 = "d0"
& c32 = "d0"
& c31 = "d0"
& c30 = "d0"
& c29 = "d0"
& c28 = "d0"
& c27 = "d0"
& c26 = "d0"
& c25 = "d1"
& c24 = "d0"
& c23 = "d0"
& c22 = "d1"
& c21 = "d0"
& c20 = "d0"
& c19 = "d0"
& c18 = "d2"
& c17 = "d0"
& c16 = "d0"
& c15 = "d0"
& c14 = "d0"
& c13 = "d1"
& c12 = "d2"
& c11 = "d0"
& c10 = "d0"
& c9 = "d0"
& c8 = "d0"
& c7 = "d0"
& c6 = "d0"
& c5 = "d0"
& c4 = "d0"
& c3 = "d0"
& c2 = "d0"
& c1 = "d0" ) ).
fof(interp_relations,interpretation-mappings,
( ~ k04_buttercup10643("d3")
& ~ k04_buttercup10643("d2")
& ~ k04_buttercup10643("d1")
& k04_buttercup10643("d0")
& ~ k04_buttercup10641("d3")
& ~ k04_buttercup10641("d2")
& ~ k04_buttercup10641("d1")
& k04_buttercup10641("d0")
& ~ k04_buttercup10639("d3")
& ~ k04_buttercup10639("d2")
& ~ k04_buttercup10639("d1")
& k04_buttercup10639("d0")
& ~ k04_buttercup10637("d3")
& ~ k04_buttercup10637("d2")
& ~ k04_buttercup10637("d1")
& k04_buttercup10637("d0")
& ~ k04_buttercup10635("d3")
& ~ k04_buttercup10635("d2")
& ~ k04_buttercup10635("d1")
& k04_buttercup10635("d0")
& ~ k04_buttercup10631("d3")
& ~ k04_buttercup10631("d2")
& ~ k04_buttercup10631("d1")
& k04_buttercup10631("d0")
& ~ k04_buttercup10628("d3")
& k04_buttercup10628("d2")
& ~ k04_buttercup10628("d1")
& k04_buttercup10628("d0")
& ~ k04_buttercup10626("d3")
& ~ k04_buttercup10626("d2")
& ~ k04_buttercup10626("d1")
& k04_buttercup10626("d0")
& ~ k04_buttercup10622("d3")
& k04_buttercup10622("d2")
& ~ k04_buttercup10622("d1")
& k04_buttercup10622("d0")
& k04_buttercup10620("d3")
& k04_buttercup10620("d2")
& ~ k04_buttercup10620("d1")
& k04_buttercup10620("d0")
& k04_buttercup10619("d3")
& k04_buttercup10619("d2")
& ~ k04_buttercup10619("d1")
& k04_buttercup10619("d0")
& ~ k04_buttercup10611("d3")
& ~ k04_buttercup10611("d2")
& ~ k04_buttercup10611("d1")
& k04_buttercup10611("d0")
& ~ k04_buttercup10608("d3")
& k04_buttercup10608("d2")
& ~ k04_buttercup10608("d1")
& k04_buttercup10608("d0")
& ~ k04_buttercup10602("d3")
& ~ k04_buttercup10602("d2")
& ~ k04_buttercup10602("d1")
& k04_buttercup10602("d0")
& ~ k04_buttercup10599("d3")
& ~ k04_buttercup10599("d2")
& ~ k04_buttercup10599("d1")
& k04_buttercup10599("d0")
& ~ k04_buttercup10593("d3")
& ~ k04_buttercup10593("d2")
& ~ k04_buttercup10593("d1")
& k04_buttercup10593("d0")
& ~ k04_buttercup10586("d3")
& ~ k04_buttercup10586("d2")
& ~ k04_buttercup10586("d1")
& k04_buttercup10586("d0")
& ~ k04_buttercup10581("d3")
& ~ k04_buttercup10581("d2")
& ~ k04_buttercup10581("d1")
& k04_buttercup10581("d0")
& ~ k04_buttercup10578("d3")
& ~ k04_buttercup10578("d2")
& ~ k04_buttercup10578("d1")
& k04_buttercup10578("d0")
& ~ k04_buttercup10567("d3")
& k04_buttercup10567("d2")
& ~ k04_buttercup10567("d1")
& k04_buttercup10567("d0")
& ~ k04_buttercup10559("d3")
& ~ k04_buttercup10559("d2")
& ~ k04_buttercup10559("d1")
& k04_buttercup10559("d0")
& ~ k04_buttercup10555("d3")
& ~ k04_buttercup10555("d2")
& ~ k04_buttercup10555("d1")
& k04_buttercup10555("d0")
& ~ k04_buttercup10551("d3")
& ~ k04_buttercup10551("d2")
& ~ k04_buttercup10551("d1")
& k04_buttercup10551("d0")
& ~ k04_buttercup10547("d3")
& ~ k04_buttercup10547("d2")
& ~ k04_buttercup10547("d1")
& k04_buttercup10547("d0")
& ~ k04_buttercup10546("d3")
& ~ k04_buttercup10546("d2")
& ~ k04_buttercup10546("d1")
& k04_buttercup10546("d0")
& ~ k04_buttercup10544("d3")
& ~ k04_buttercup10544("d2")
& ~ k04_buttercup10544("d1")
& k04_buttercup10544("d0")
& ~ k04_buttercup10540("d3")
& ~ k04_buttercup10540("d2")
& ~ k04_buttercup10540("d1")
& k04_buttercup10540("d0")
& ~ k04_buttercup10539("d3")
& ~ k04_buttercup10539("d2")
& ~ k04_buttercup10539("d1")
& k04_buttercup10539("d0")
& ~ k04_buttercup10535("d3")
& ~ k04_buttercup10535("d2")
& ~ k04_buttercup10535("d1")
& k04_buttercup10535("d0")
& ~ k04_buttercup10529("d3")
& ~ k04_buttercup10529("d2")
& ~ k04_buttercup10529("d1")
& k04_buttercup10529("d0")
& ~ k04_buttercup10524("d3")
& ~ k04_buttercup10524("d2")
& ~ k04_buttercup10524("d1")
& k04_buttercup10524("d0")
& ~ k04_buttercup10517("d3")
& ~ k04_buttercup10517("d2")
& ~ k04_buttercup10517("d1")
& k04_buttercup10517("d0")
& k04_buttercup10516("d3")
& ~ k04_buttercup10516("d2")
& ~ k04_buttercup10516("d1")
& k04_buttercup10516("d0")
& ~ k04_buttercup10510("d3")
& ~ k04_buttercup10510("d2")
& ~ k04_buttercup10510("d1")
& k04_buttercup10510("d0")
& ~ k04_buttercup10506("d3")
& ~ k04_buttercup10506("d2")
& ~ k04_buttercup10506("d1")
& k04_buttercup10506("d0")
& ~ k04_buttercup10504("d3")
& ~ k04_buttercup10504("d2")
& ~ k04_buttercup10504("d1")
& k04_buttercup10504("d0")
& ~ k04_buttercup10499("d3")
& ~ k04_buttercup10499("d2")
& ~ k04_buttercup10499("d1")
& k04_buttercup10499("d0")
& ~ k04_buttercup10495("d3")
& ~ k04_buttercup10495("d2")
& ~ k04_buttercup10495("d1")
& k04_buttercup10495("d0")
& ~ k04_buttercup10492("d3")
& ~ k04_buttercup10492("d2")
& ~ k04_buttercup10492("d1")
& k04_buttercup10492("d0")
& ~ k04_buttercup10486("d3")
& k04_buttercup10486("d2")
& ~ k04_buttercup10486("d1")
& k04_buttercup10486("d0")
& ~ k04_buttercup10482("d3")
& ~ k04_buttercup10482("d2")
& ~ k04_buttercup10482("d1")
& k04_buttercup10482("d0")
& ~ k04_buttercup10477("d3")
& k04_buttercup10477("d2")
& ~ k04_buttercup10477("d1")
& k04_buttercup10477("d0")
& ~ k04_buttercup10473("d3")
& ~ k04_buttercup10473("d2")
& ~ k04_buttercup10473("d1")
& k04_buttercup10473("d0")
& ~ k04_buttercup10470("d3")
& ~ k04_buttercup10470("d2")
& ~ k04_buttercup10470("d1")
& k04_buttercup10470("d0")
& ~ k04_buttercup10464("d3")
& k04_buttercup10464("d2")
& ~ k04_buttercup10464("d1")
& k04_buttercup10464("d0")
& ~ k04_buttercup10462("d3")
& ~ k04_buttercup10462("d2")
& ~ k04_buttercup10462("d1")
& k04_buttercup10462("d0")
& ~ k04_buttercup10453("d3")
& ~ k04_buttercup10453("d2")
& ~ k04_buttercup10453("d1")
& k04_buttercup10453("d0")
& ~ k04_buttercup10449("d3")
& k04_buttercup10449("d2")
& ~ k04_buttercup10449("d1")
& k04_buttercup10449("d0")
& ~ k04_buttercup10445("d3")
& ~ k04_buttercup10445("d2")
& ~ k04_buttercup10445("d1")
& k04_buttercup10445("d0")
& ~ k04_buttercup10437("d3")
& ~ k04_buttercup10437("d2")
& ~ k04_buttercup10437("d1")
& k04_buttercup10437("d0")
& ~ k04_buttercup10430("d3")
& ~ k04_buttercup10430("d2")
& ~ k04_buttercup10430("d1")
& k04_buttercup10430("d0")
& ~ k04_buttercup10425("d3")
& ~ k04_buttercup10425("d2")
& ~ k04_buttercup10425("d1")
& k04_buttercup10425("d0")
& ~ k04_buttercup10424("d3")
& ~ k04_buttercup10424("d2")
& ~ k04_buttercup10424("d1")
& k04_buttercup10424("d0")
& ~ k04_buttercup10419("d3")
& k04_buttercup10419("d2")
& ~ k04_buttercup10419("d1")
& k04_buttercup10419("d0")
& ~ k04_buttercup10415("d3")
& ~ k04_buttercup10415("d2")
& ~ k04_buttercup10415("d1")
& k04_buttercup10415("d0")
& ~ k04_buttercup10408("d3")
& ~ k04_buttercup10408("d2")
& ~ k04_buttercup10408("d1")
& k04_buttercup10408("d0")
& ~ k04_buttercup10406("d3")
& ~ k04_buttercup10406("d2")
& ~ k04_buttercup10406("d1")
& k04_buttercup10406("d0")
& ~ k04_buttercup10404("d3")
& ~ k04_buttercup10404("d2")
& ~ k04_buttercup10404("d1")
& k04_buttercup10404("d0")
& ~ k04_buttercup10400("d3")
& k04_buttercup10400("d2")
& ~ k04_buttercup10400("d1")
& k04_buttercup10400("d0")
& ~ k04_buttercup10397("d3")
& ~ k04_buttercup10397("d2")
& ~ k04_buttercup10397("d1")
& k04_buttercup10397("d0")
& ~ k04_buttercup10391("d3")
& ~ k04_buttercup10391("d2")
& ~ k04_buttercup10391("d1")
& k04_buttercup10391("d0")
& ~ k04_buttercup10389("d3")
& ~ k04_buttercup10389("d2")
& ~ k04_buttercup10389("d1")
& k04_buttercup10389("d0")
& ~ k04_buttercup10385("d3")
& ~ k04_buttercup10385("d2")
& ~ k04_buttercup10385("d1")
& k04_buttercup10385("d0")
& ~ k04_buttercup10382("d3")
& ~ k04_buttercup10382("d2")
& ~ k04_buttercup10382("d1")
& k04_buttercup10382("d0")
& ~ k04_buttercup10380("d3")
& ~ k04_buttercup10380("d2")
& ~ k04_buttercup10380("d1")
& k04_buttercup10380("d0")
& ~ k04_buttercup10376("d3")
& ~ k04_buttercup10376("d2")
& ~ k04_buttercup10376("d1")
& k04_buttercup10376("d0")
& ~ k04_buttercup10373("d3")
& ~ k04_buttercup10373("d2")
& ~ k04_buttercup10373("d1")
& k04_buttercup10373("d0")
& ~ k04_buttercup10371("d3")
& ~ k04_buttercup10371("d2")
& ~ k04_buttercup10371("d1")
& k04_buttercup10371("d0")
& ~ k04_buttercup10369("d3")
& ~ k04_buttercup10369("d2")
& ~ k04_buttercup10369("d1")
& k04_buttercup10369("d0")
& ~ k04_buttercup10364("d3")
& k04_buttercup10364("d2")
& ~ k04_buttercup10364("d1")
& k04_buttercup10364("d0")
& ~ k04_buttercup10360("d3")
& ~ k04_buttercup10360("d2")
& ~ k04_buttercup10360("d1")
& k04_buttercup10360("d0")
& ~ k04_buttercup10357("d3")
& ~ k04_buttercup10357("d2")
& ~ k04_buttercup10357("d1")
& k04_buttercup10357("d0")
& ~ k04_buttercup10356("d3")
& ~ k04_buttercup10356("d2")
& ~ k04_buttercup10356("d1")
& k04_buttercup10356("d0")
& ~ k04_buttercup10351("d3")
& ~ k04_buttercup10351("d2")
& ~ k04_buttercup10351("d1")
& k04_buttercup10351("d0")
& ~ k04_buttercup10347("d3")
& k04_buttercup10347("d2")
& ~ k04_buttercup10347("d1")
& k04_buttercup10347("d0")
& ~ k04_buttercup10342("d3")
& ~ k04_buttercup10342("d2")
& ~ k04_buttercup10342("d1")
& k04_buttercup10342("d0")
& ~ k04_buttercup10337("d3")
& k04_buttercup10337("d2")
& ~ k04_buttercup10337("d1")
& k04_buttercup10337("d0")
& ~ k04_buttercup10333("d3")
& ~ k04_buttercup10333("d2")
& ~ k04_buttercup10333("d1")
& k04_buttercup10333("d0")
& ~ k04_buttercup10329("d3")
& ~ k04_buttercup10329("d2")
& ~ k04_buttercup10329("d1")
& k04_buttercup10329("d0")
& ~ k04_buttercup10325("d3")
& ~ k04_buttercup10325("d2")
& ~ k04_buttercup10325("d1")
& k04_buttercup10325("d0")
& ~ k04_buttercup10316("d3")
& k04_buttercup10316("d2")
& ~ k04_buttercup10316("d1")
& k04_buttercup10316("d0")
& ~ k04_buttercup10312("d3")
& ~ k04_buttercup10312("d2")
& ~ k04_buttercup10312("d1")
& k04_buttercup10312("d0")
& ~ k04_buttercup10303("d3")
& k04_buttercup10303("d2")
& ~ k04_buttercup10303("d1")
& k04_buttercup10303("d0")
& ~ k04_buttercup10298("d3")
& ~ k04_buttercup10298("d2")
& ~ k04_buttercup10298("d1")
& k04_buttercup10298("d0")
& ~ k04_buttercup10296("d3")
& ~ k04_buttercup10296("d2")
& ~ k04_buttercup10296("d1")
& k04_buttercup10296("d0")
& ~ k04_buttercup10293("d3")
& ~ k04_buttercup10293("d2")
& ~ k04_buttercup10293("d1")
& k04_buttercup10293("d0")
& ~ k04_buttercup10288("d3")
& ~ k04_buttercup10288("d2")
& ~ k04_buttercup10288("d1")
& k04_buttercup10288("d0")
& ~ k04_buttercup10286("d3")
& ~ k04_buttercup10286("d2")
& ~ k04_buttercup10286("d1")
& k04_buttercup10286("d0")
& ~ k04_buttercup10282("d3")
& ~ k04_buttercup10282("d2")
& ~ k04_buttercup10282("d1")
& k04_buttercup10282("d0")
& ~ k04_buttercup10259("d3")
& ~ k04_buttercup10259("d2")
& k04_buttercup10259("d1")
& k04_buttercup10259("d0")
& ~ k04_buttercup10255("d3")
& ~ k04_buttercup10255("d2")
& ~ k04_buttercup10255("d1")
& k04_buttercup10255("d0")
& ~ k04_buttercup10252("d3")
& ~ k04_buttercup10252("d2")
& ~ k04_buttercup10252("d1")
& k04_buttercup10252("d0")
& ~ k04_buttercup10244("d3")
& ~ k04_buttercup10244("d2")
& ~ k04_buttercup10244("d1")
& k04_buttercup10244("d0")
& ~ k04_buttercup10238("d3")
& ~ k04_buttercup10238("d2")
& ~ k04_buttercup10238("d1")
& k04_buttercup10238("d0")
& ~ k04_buttercup10236("d3")
& ~ k04_buttercup10236("d2")
& ~ k04_buttercup10236("d1")
& k04_buttercup10236("d0")
& ~ k04_buttercup10234("d3")
& ~ k04_buttercup10234("d2")
& ~ k04_buttercup10234("d1")
& k04_buttercup10234("d0")
& k04_buttercup10225("d3")
& ~ k04_buttercup10225("d2")
& ~ k04_buttercup10225("d1")
& k04_buttercup10225("d0")
& ~ k04_buttercup10221("d3")
& k04_buttercup10221("d2")
& ~ k04_buttercup10221("d1")
& k04_buttercup10221("d0")
& ~ k04_buttercup10219("d3")
& ~ k04_buttercup10219("d2")
& ~ k04_buttercup10219("d1")
& k04_buttercup10219("d0")
& ~ k04_buttercup10213("d3")
& ~ k04_buttercup10213("d2")
& ~ k04_buttercup10213("d1")
& k04_buttercup10213("d0")
& ~ k04_buttercup10206("d3")
& ~ k04_buttercup10206("d2")
& ~ k04_buttercup10206("d1")
& k04_buttercup10206("d0")
& ~ k04_buttercup10204("d3")
& ~ k04_buttercup10204("d2")
& ~ k04_buttercup10204("d1")
& k04_buttercup10204("d0")
& ~ k04_buttercup10200("d3")
& ~ k04_buttercup10200("d2")
& ~ k04_buttercup10200("d1")
& k04_buttercup10200("d0")
& ~ k04_buttercup10190("d3")
& k04_buttercup10190("d2")
& ~ k04_buttercup10190("d1")
& k04_buttercup10190("d0")
& ~ k04_buttercup10184("d3")
& ~ k04_buttercup10184("d2")
& ~ k04_buttercup10184("d1")
& k04_buttercup10184("d0")
& ~ k04_buttercup10181("d3")
& ~ k04_buttercup10181("d2")
& ~ k04_buttercup10181("d1")
& k04_buttercup10181("d0")
& ~ k04_buttercup10172("d3")
& k04_buttercup10172("d2")
& ~ k04_buttercup10172("d1")
& k04_buttercup10172("d0")
& ~ k04_buttercup10164("d3")
& k04_buttercup10164("d2")
& ~ k04_buttercup10164("d1")
& k04_buttercup10164("d0")
& ~ k04_buttercup10153("d3")
& k04_buttercup10153("d2")
& ~ k04_buttercup10153("d1")
& k04_buttercup10153("d0")
& ~ k04_buttercup10147("d3")
& ~ k04_buttercup10147("d2")
& ~ k04_buttercup10147("d1")
& k04_buttercup10147("d0")
& ~ k04_buttercup10142("d3")
& k04_buttercup10142("d2")
& ~ k04_buttercup10142("d1")
& ~ k04_buttercup10142("d0")
& ~ k04_buttercup10139("d3")
& k04_buttercup10139("d2")
& ~ k04_buttercup10139("d1")
& k04_buttercup10139("d0")
& ~ k04_buttercup10135("d3")
& ~ k04_buttercup10135("d2")
& ~ k04_buttercup10135("d1")
& k04_buttercup10135("d0")
& ~ k04_buttercup10132("d3")
& k04_buttercup10132("d2")
& ~ k04_buttercup10132("d1")
& k04_buttercup10132("d0")
& ~ k04_buttercup10125("d3")
& ~ k04_buttercup10125("d2")
& ~ k04_buttercup10125("d1")
& k04_buttercup10125("d0")
& ~ k04_buttercup10117("d3")
& k04_buttercup10117("d2")
& ~ k04_buttercup10117("d1")
& k04_buttercup10117("d0")
& ~ k04_buttercup10100("d3")
& k04_buttercup10100("d2")
& ~ k04_buttercup10100("d1")
& k04_buttercup10100("d0")
& ~ k04_buttercup10097("d3")
& k04_buttercup10097("d2")
& ~ k04_buttercup10097("d1")
& ~ k04_buttercup10097("d0")
& ~ k04_buttercup10096("d3")
& k04_buttercup10096("d2")
& ~ k04_buttercup10096("d1")
& ~ k04_buttercup10096("d0")
& ~ k04_buttercup10095("d3")
& k04_buttercup10095("d2")
& ~ k04_buttercup10095("d1")
& k04_buttercup10095("d0")
& ~ k04_buttercup10089("d3")
& ~ k04_buttercup10089("d2")
& ~ k04_buttercup10089("d1")
& k04_buttercup10089("d0")
& ~ k04_buttercup10084("d3")
& ~ k04_buttercup10084("d2")
& ~ k04_buttercup10084("d1")
& k04_buttercup10084("d0")
& ~ k04_buttercup10079("d3")
& ~ k04_buttercup10079("d2")
& ~ k04_buttercup10079("d1")
& k04_buttercup10079("d0")
& ~ k04_buttercup10074("d3")
& ~ k04_buttercup10074("d2")
& ~ k04_buttercup10074("d1")
& k04_buttercup10074("d0")
& ~ k04_buttercup10067("d3")
& ~ k04_buttercup10067("d2")
& ~ k04_buttercup10067("d1")
& k04_buttercup10067("d0")
& ~ k04_buttercup10064("d3")
& k04_buttercup10064("d2")
& ~ k04_buttercup10064("d1")
& k04_buttercup10064("d0")
& ~ k04_buttercup10061("d3")
& ~ k04_buttercup10061("d2")
& ~ k04_buttercup10061("d1")
& k04_buttercup10061("d0")
& ~ k04_buttercup10057("d3")
& k04_buttercup10057("d2")
& ~ k04_buttercup10057("d1")
& k04_buttercup10057("d0")
& ~ k04_buttercup10053("d3")
& k04_buttercup10053("d2")
& ~ k04_buttercup10053("d1")
& k04_buttercup10053("d0")
& ~ k04_buttercup10051("d3")
& ~ k04_buttercup10051("d2")
& ~ k04_buttercup10051("d1")
& k04_buttercup10051("d0")
& ~ k04_buttercup10049("d3")
& ~ k04_buttercup10049("d2")
& ~ k04_buttercup10049("d1")
& k04_buttercup10049("d0")
& ~ k04_buttercup10048("d3")
& ~ k04_buttercup10048("d2")
& ~ k04_buttercup10048("d1")
& k04_buttercup10048("d0")
& ~ k04_buttercup10044("d3")
& ~ k04_buttercup10044("d2")
& ~ k04_buttercup10044("d1")
& k04_buttercup10044("d0")
& ~ k04_buttercup10042("d3")
& ~ k04_buttercup10042("d2")
& ~ k04_buttercup10042("d1")
& k04_buttercup10042("d0")
& ~ k04_buttercup10039("d3")
& ~ k04_buttercup10039("d2")
& ~ k04_buttercup10039("d1")
& k04_buttercup10039("d0")
& ~ k04_buttercup10033("d3")
& ~ k04_buttercup10033("d2")
& ~ k04_buttercup10033("d1")
& k04_buttercup10033("d0")
& ~ k04_buttercup10028("d3")
& ~ k04_buttercup10028("d2")
& ~ k04_buttercup10028("d1")
& k04_buttercup10028("d0")
& ~ k04_buttercup10026("d3")
& ~ k04_buttercup10026("d2")
& ~ k04_buttercup10026("d1")
& k04_buttercup10026("d0")
& ~ k04_buttercup10016("d3")
& k04_buttercup10016("d2")
& ~ k04_buttercup10016("d1")
& k04_buttercup10016("d0")
& k04_buttercup10012("d3")
& k04_buttercup10012("d2")
& ~ k04_buttercup10012("d1")
& k04_buttercup10012("d0")
& ~ k04_buttercup10004("d3")
& ~ k04_buttercup10004("d2")
& k04_buttercup10004("d1")
& ~ k04_buttercup10004("d0")
& ~ k04_buttercup10000("d3")
& ~ k04_buttercup10000("d2")
& k04_buttercup10000("d1")
& ~ k04_buttercup10000("d0")
& ~ b48_buttercup10646("d3")
& ~ b48_buttercup10646("d2")
& ~ b48_buttercup10646("d1")
& b48_buttercup10646("d0")
& ~ b48_buttercup10642("d3")
& ~ b48_buttercup10642("d2")
& ~ b48_buttercup10642("d1")
& b48_buttercup10642("d0")
& ~ b48_buttercup10640("d3")
& ~ b48_buttercup10640("d2")
& ~ b48_buttercup10640("d1")
& b48_buttercup10640("d0")
& ~ b48_buttercup10638("d3")
& ~ b48_buttercup10638("d2")
& ~ b48_buttercup10638("d1")
& b48_buttercup10638("d0")
& ~ b48_buttercup10636("d3")
& ~ b48_buttercup10636("d2")
& ~ b48_buttercup10636("d1")
& b48_buttercup10636("d0")
& ~ b48_buttercup10632("d3")
& ~ b48_buttercup10632("d2")
& ~ b48_buttercup10632("d1")
& b48_buttercup10632("d0")
& ~ b48_buttercup10629("d3")
& ~ b48_buttercup10629("d2")
& ~ b48_buttercup10629("d1")
& b48_buttercup10629("d0")
& ~ b48_buttercup10624("d3")
& ~ b48_buttercup10624("d2")
& ~ b48_buttercup10624("d1")
& b48_buttercup10624("d0")
& ~ b48_buttercup10616("d3")
& ~ b48_buttercup10616("d2")
& ~ b48_buttercup10616("d1")
& b48_buttercup10616("d0")
& ~ b48_buttercup10612("d3")
& ~ b48_buttercup10612("d2")
& ~ b48_buttercup10612("d1")
& b48_buttercup10612("d0")
& ~ b48_buttercup10609("d3")
& ~ b48_buttercup10609("d2")
& ~ b48_buttercup10609("d1")
& b48_buttercup10609("d0")
& ~ b48_buttercup10606("d3")
& ~ b48_buttercup10606("d2")
& ~ b48_buttercup10606("d1")
& b48_buttercup10606("d0")
& ~ b48_buttercup10605("d3")
& ~ b48_buttercup10605("d2")
& ~ b48_buttercup10605("d1")
& b48_buttercup10605("d0")
& ~ b48_buttercup10604("d3")
& ~ b48_buttercup10604("d2")
& ~ b48_buttercup10604("d1")
& b48_buttercup10604("d0")
& ~ b48_buttercup10596("d3")
& ~ b48_buttercup10596("d2")
& ~ b48_buttercup10596("d1")
& b48_buttercup10596("d0")
& ~ b48_buttercup10589("d3")
& ~ b48_buttercup10589("d2")
& ~ b48_buttercup10589("d1")
& b48_buttercup10589("d0")
& ~ b48_buttercup10582("d3")
& ~ b48_buttercup10582("d2")
& ~ b48_buttercup10582("d1")
& b48_buttercup10582("d0")
& ~ b48_buttercup10579("d3")
& ~ b48_buttercup10579("d2")
& ~ b48_buttercup10579("d1")
& b48_buttercup10579("d0")
& ~ b48_buttercup10575("d3")
& ~ b48_buttercup10575("d2")
& ~ b48_buttercup10575("d1")
& b48_buttercup10575("d0")
& ~ b48_buttercup10574("d3")
& b48_buttercup10574("d2")
& ~ b48_buttercup10574("d1")
& ~ b48_buttercup10574("d0")
& ~ b48_buttercup10572("d3")
& b48_buttercup10572("d2")
& ~ b48_buttercup10572("d1")
& ~ b48_buttercup10572("d0")
& ~ b48_buttercup10570("d3")
& b48_buttercup10570("d2")
& ~ b48_buttercup10570("d1")
& ~ b48_buttercup10570("d0")
& ~ b48_buttercup10563("d3")
& b48_buttercup10563("d2")
& ~ b48_buttercup10563("d1")
& b48_buttercup10563("d0")
& ~ b48_buttercup10562("d3")
& ~ b48_buttercup10562("d2")
& ~ b48_buttercup10562("d1")
& b48_buttercup10562("d0")
& ~ b48_buttercup10561("d3")
& ~ b48_buttercup10561("d2")
& ~ b48_buttercup10561("d1")
& b48_buttercup10561("d0")
& ~ b48_buttercup10552("d3")
& ~ b48_buttercup10552("d2")
& ~ b48_buttercup10552("d1")
& b48_buttercup10552("d0")
& ~ b48_buttercup10549("d3")
& ~ b48_buttercup10549("d2")
& ~ b48_buttercup10549("d1")
& b48_buttercup10549("d0")
& ~ b48_buttercup10548("d3")
& ~ b48_buttercup10548("d2")
& ~ b48_buttercup10548("d1")
& b48_buttercup10548("d0")
& ~ b48_buttercup10545("d3")
& ~ b48_buttercup10545("d2")
& ~ b48_buttercup10545("d1")
& b48_buttercup10545("d0")
& ~ b48_buttercup10542("d3")
& ~ b48_buttercup10542("d2")
& ~ b48_buttercup10542("d1")
& b48_buttercup10542("d0")
& ~ b48_buttercup10541("d3")
& ~ b48_buttercup10541("d2")
& ~ b48_buttercup10541("d1")
& b48_buttercup10541("d0")
& ~ b48_buttercup10538("d3")
& ~ b48_buttercup10538("d2")
& ~ b48_buttercup10538("d1")
& b48_buttercup10538("d0")
& ~ b48_buttercup10531("d3")
& ~ b48_buttercup10531("d2")
& ~ b48_buttercup10531("d1")
& b48_buttercup10531("d0")
& ~ b48_buttercup10530("d3")
& ~ b48_buttercup10530("d2")
& ~ b48_buttercup10530("d1")
& b48_buttercup10530("d0")
& ~ b48_buttercup10526("d3")
& ~ b48_buttercup10526("d2")
& ~ b48_buttercup10526("d1")
& b48_buttercup10526("d0")
& ~ b48_buttercup10522("d3")
& ~ b48_buttercup10522("d2")
& ~ b48_buttercup10522("d1")
& b48_buttercup10522("d0")
& b48_buttercup10521("d3")
& ~ b48_buttercup10521("d2")
& ~ b48_buttercup10521("d1")
& ~ b48_buttercup10521("d0")
& b48_buttercup10520("d3")
& ~ b48_buttercup10520("d2")
& ~ b48_buttercup10520("d1")
& ~ b48_buttercup10520("d0")
& b48_buttercup10519("d3")
& ~ b48_buttercup10519("d2")
& ~ b48_buttercup10519("d1")
& ~ b48_buttercup10519("d0")
& b48_buttercup10518("d3")
& ~ b48_buttercup10518("d2")
& ~ b48_buttercup10518("d1")
& ~ b48_buttercup10518("d0")
& b48_buttercup10515("d3")
& ~ b48_buttercup10515("d2")
& ~ b48_buttercup10515("d1")
& ~ b48_buttercup10515("d0")
& ~ b48_buttercup10514("d3")
& ~ b48_buttercup10514("d2")
& ~ b48_buttercup10514("d1")
& b48_buttercup10514("d0")
& ~ b48_buttercup10513("d3")
& ~ b48_buttercup10513("d2")
& ~ b48_buttercup10513("d1")
& b48_buttercup10513("d0")
& ~ b48_buttercup10512("d3")
& ~ b48_buttercup10512("d2")
& ~ b48_buttercup10512("d1")
& b48_buttercup10512("d0")
& ~ b48_buttercup10507("d3")
& ~ b48_buttercup10507("d2")
& ~ b48_buttercup10507("d1")
& b48_buttercup10507("d0")
& ~ b48_buttercup10502("d3")
& ~ b48_buttercup10502("d2")
& ~ b48_buttercup10502("d1")
& b48_buttercup10502("d0")
& ~ b48_buttercup10496("d3")
& ~ b48_buttercup10496("d2")
& ~ b48_buttercup10496("d1")
& b48_buttercup10496("d0")
& ~ b48_buttercup10493("d3")
& ~ b48_buttercup10493("d2")
& ~ b48_buttercup10493("d1")
& b48_buttercup10493("d0")
& ~ b48_buttercup10490("d3")
& ~ b48_buttercup10490("d2")
& ~ b48_buttercup10490("d1")
& b48_buttercup10490("d0")
& ~ b48_buttercup10489("d3")
& b48_buttercup10489("d2")
& ~ b48_buttercup10489("d1")
& ~ b48_buttercup10489("d0")
& ~ b48_buttercup10487("d3")
& b48_buttercup10487("d2")
& ~ b48_buttercup10487("d1")
& ~ b48_buttercup10487("d0")
& ~ b48_buttercup10483("d3")
& b48_buttercup10483("d2")
& ~ b48_buttercup10483("d1")
& ~ b48_buttercup10483("d0")
& ~ b48_buttercup10479("d3")
& ~ b48_buttercup10479("d2")
& ~ b48_buttercup10479("d1")
& b48_buttercup10479("d0")
& ~ b48_buttercup10478("d3")
& b48_buttercup10478("d2")
& ~ b48_buttercup10478("d1")
& ~ b48_buttercup10478("d0")
& ~ b48_buttercup10474("d3")
& b48_buttercup10474("d2")
& ~ b48_buttercup10474("d1")
& b48_buttercup10474("d0")
& ~ b48_buttercup10471("d3")
& ~ b48_buttercup10471("d2")
& ~ b48_buttercup10471("d1")
& b48_buttercup10471("d0")
& ~ b48_buttercup10469("d3")
& ~ b48_buttercup10469("d2")
& ~ b48_buttercup10469("d1")
& b48_buttercup10469("d0")
& ~ b48_buttercup10467("d3")
& b48_buttercup10467("d2")
& ~ b48_buttercup10467("d1")
& ~ b48_buttercup10467("d0")
& ~ b48_buttercup10466("d3")
& b48_buttercup10466("d2")
& ~ b48_buttercup10466("d1")
& ~ b48_buttercup10466("d0")
& ~ b48_buttercup10465("d3")
& b48_buttercup10465("d2")
& ~ b48_buttercup10465("d1")
& ~ b48_buttercup10465("d0")
& ~ b48_buttercup10460("d3")
& ~ b48_buttercup10460("d2")
& ~ b48_buttercup10460("d1")
& b48_buttercup10460("d0")
& ~ b48_buttercup10458("d3")
& ~ b48_buttercup10458("d2")
& b48_buttercup10458("d1")
& b48_buttercup10458("d0")
& ~ b48_buttercup10456("d3")
& b48_buttercup10456("d2")
& ~ b48_buttercup10456("d1")
& ~ b48_buttercup10456("d0")
& ~ b48_buttercup10454("d3")
& b48_buttercup10454("d2")
& ~ b48_buttercup10454("d1")
& ~ b48_buttercup10454("d0")
& ~ b48_buttercup10451("d3")
& ~ b48_buttercup10451("d2")
& ~ b48_buttercup10451("d1")
& b48_buttercup10451("d0")
& ~ b48_buttercup10450("d3")
& ~ b48_buttercup10450("d2")
& ~ b48_buttercup10450("d1")
& b48_buttercup10450("d0")
& ~ b48_buttercup10446("d3")
& b48_buttercup10446("d2")
& ~ b48_buttercup10446("d1")
& b48_buttercup10446("d0")
& ~ b48_buttercup10443("d3")
& ~ b48_buttercup10443("d2")
& ~ b48_buttercup10443("d1")
& b48_buttercup10443("d0")
& ~ b48_buttercup10442("d3")
& ~ b48_buttercup10442("d2")
& ~ b48_buttercup10442("d1")
& b48_buttercup10442("d0")
& ~ b48_buttercup10441("d3")
& ~ b48_buttercup10441("d2")
& ~ b48_buttercup10441("d1")
& b48_buttercup10441("d0")
& ~ b48_buttercup10440("d3")
& ~ b48_buttercup10440("d2")
& b48_buttercup10440("d1")
& b48_buttercup10440("d0")
& ~ b48_buttercup10434("d3")
& ~ b48_buttercup10434("d2")
& ~ b48_buttercup10434("d1")
& b48_buttercup10434("d0")
& ~ b48_buttercup10433("d3")
& ~ b48_buttercup10433("d2")
& ~ b48_buttercup10433("d1")
& b48_buttercup10433("d0")
& ~ b48_buttercup10427("d3")
& ~ b48_buttercup10427("d2")
& ~ b48_buttercup10427("d1")
& b48_buttercup10427("d0")
& ~ b48_buttercup10422("d3")
& b48_buttercup10422("d2")
& ~ b48_buttercup10422("d1")
& ~ b48_buttercup10422("d0")
& ~ b48_buttercup10421("d3")
& ~ b48_buttercup10421("d2")
& ~ b48_buttercup10421("d1")
& b48_buttercup10421("d0")
& ~ b48_buttercup10420("d3")
& ~ b48_buttercup10420("d2")
& ~ b48_buttercup10420("d1")
& b48_buttercup10420("d0")
& b48_buttercup10417("d3")
& ~ b48_buttercup10417("d2")
& b48_buttercup10417("d1")
& b48_buttercup10417("d0")
& ~ b48_buttercup10411("d3")
& ~ b48_buttercup10411("d2")
& ~ b48_buttercup10411("d1")
& b48_buttercup10411("d0")
& ~ b48_buttercup10410("d3")
& ~ b48_buttercup10410("d2")
& ~ b48_buttercup10410("d1")
& b48_buttercup10410("d0")
& ~ b48_buttercup10405("d3")
& ~ b48_buttercup10405("d2")
& ~ b48_buttercup10405("d1")
& b48_buttercup10405("d0")
& ~ b48_buttercup10402("d3")
& ~ b48_buttercup10402("d2")
& ~ b48_buttercup10402("d1")
& b48_buttercup10402("d0")
& ~ b48_buttercup10398("d3")
& b48_buttercup10398("d2")
& ~ b48_buttercup10398("d1")
& ~ b48_buttercup10398("d0")
& ~ b48_buttercup10394("d3")
& ~ b48_buttercup10394("d2")
& ~ b48_buttercup10394("d1")
& b48_buttercup10394("d0")
& ~ b48_buttercup10386("d3")
& ~ b48_buttercup10386("d2")
& ~ b48_buttercup10386("d1")
& b48_buttercup10386("d0")
& ~ b48_buttercup10383("d3")
& ~ b48_buttercup10383("d2")
& ~ b48_buttercup10383("d1")
& b48_buttercup10383("d0")
& ~ b48_buttercup10381("d3")
& b48_buttercup10381("d2")
& ~ b48_buttercup10381("d1")
& ~ b48_buttercup10381("d0")
& ~ b48_buttercup10378("d3")
& ~ b48_buttercup10378("d2")
& ~ b48_buttercup10378("d1")
& b48_buttercup10378("d0")
& ~ b48_buttercup10377("d3")
& ~ b48_buttercup10377("d2")
& ~ b48_buttercup10377("d1")
& b48_buttercup10377("d0")
& ~ b48_buttercup10374("d3")
& ~ b48_buttercup10374("d2")
& ~ b48_buttercup10374("d1")
& b48_buttercup10374("d0")
& ~ b48_buttercup10370("d3")
& ~ b48_buttercup10370("d2")
& ~ b48_buttercup10370("d1")
& b48_buttercup10370("d0")
& ~ b48_buttercup10367("d3")
& ~ b48_buttercup10367("d2")
& ~ b48_buttercup10367("d1")
& b48_buttercup10367("d0")
& ~ b48_buttercup10365("d3")
& ~ b48_buttercup10365("d2")
& ~ b48_buttercup10365("d1")
& b48_buttercup10365("d0")
& ~ b48_buttercup10362("d3")
& b48_buttercup10362("d2")
& ~ b48_buttercup10362("d1")
& ~ b48_buttercup10362("d0")
& ~ b48_buttercup10361("d3")
& ~ b48_buttercup10361("d2")
& ~ b48_buttercup10361("d1")
& b48_buttercup10361("d0")
& ~ b48_buttercup10359("d3")
& ~ b48_buttercup10359("d2")
& ~ b48_buttercup10359("d1")
& b48_buttercup10359("d0")
& ~ b48_buttercup10358("d3")
& ~ b48_buttercup10358("d2")
& ~ b48_buttercup10358("d1")
& b48_buttercup10358("d0")
& ~ b48_buttercup10353("d3")
& ~ b48_buttercup10353("d2")
& ~ b48_buttercup10353("d1")
& b48_buttercup10353("d0")
& ~ b48_buttercup10352("d3")
& b48_buttercup10352("d2")
& ~ b48_buttercup10352("d1")
& ~ b48_buttercup10352("d0")
& ~ b48_buttercup10348("d3")
& b48_buttercup10348("d2")
& ~ b48_buttercup10348("d1")
& ~ b48_buttercup10348("d0")
& ~ b48_buttercup10344("d3")
& b48_buttercup10344("d2")
& ~ b48_buttercup10344("d1")
& ~ b48_buttercup10344("d0")
& ~ b48_buttercup10343("d3")
& b48_buttercup10343("d2")
& ~ b48_buttercup10343("d1")
& ~ b48_buttercup10343("d0")
& ~ b48_buttercup10334("d3")
& b48_buttercup10334("d2")
& ~ b48_buttercup10334("d1")
& ~ b48_buttercup10334("d0")
& ~ b48_buttercup10332("d3")
& ~ b48_buttercup10332("d2")
& ~ b48_buttercup10332("d1")
& b48_buttercup10332("d0")
& ~ b48_buttercup10326("d3")
& ~ b48_buttercup10326("d2")
& ~ b48_buttercup10326("d1")
& b48_buttercup10326("d0")
& ~ b48_buttercup10322("d3")
& ~ b48_buttercup10322("d2")
& ~ b48_buttercup10322("d1")
& b48_buttercup10322("d0")
& ~ b48_buttercup10320("d3")
& b48_buttercup10320("d2")
& ~ b48_buttercup10320("d1")
& ~ b48_buttercup10320("d0")
& ~ b48_buttercup10318("d3")
& ~ b48_buttercup10318("d2")
& ~ b48_buttercup10318("d1")
& b48_buttercup10318("d0")
& ~ b48_buttercup10313("d3")
& b48_buttercup10313("d2")
& ~ b48_buttercup10313("d1")
& b48_buttercup10313("d0")
& ~ b48_buttercup10309("d3")
& ~ b48_buttercup10309("d2")
& ~ b48_buttercup10309("d1")
& b48_buttercup10309("d0")
& ~ b48_buttercup10308("d3")
& b48_buttercup10308("d2")
& ~ b48_buttercup10308("d1")
& ~ b48_buttercup10308("d0")
& ~ b48_buttercup10307("d3")
& b48_buttercup10307("d2")
& ~ b48_buttercup10307("d1")
& ~ b48_buttercup10307("d0")
& ~ b48_buttercup10305("d3")
& b48_buttercup10305("d2")
& ~ b48_buttercup10305("d1")
& ~ b48_buttercup10305("d0")
& ~ b48_buttercup10300("d3")
& b48_buttercup10300("d2")
& ~ b48_buttercup10300("d1")
& b48_buttercup10300("d0")
& ~ b48_buttercup10299("d3")
& ~ b48_buttercup10299("d2")
& ~ b48_buttercup10299("d1")
& b48_buttercup10299("d0")
& ~ b48_buttercup10294("d3")
& ~ b48_buttercup10294("d2")
& ~ b48_buttercup10294("d1")
& b48_buttercup10294("d0")
& ~ b48_buttercup10291("d3")
& ~ b48_buttercup10291("d2")
& ~ b48_buttercup10291("d1")
& b48_buttercup10291("d0")
& ~ b48_buttercup10290("d3")
& ~ b48_buttercup10290("d2")
& ~ b48_buttercup10290("d1")
& b48_buttercup10290("d0")
& ~ b48_buttercup10289("d3")
& b48_buttercup10289("d2")
& ~ b48_buttercup10289("d1")
& b48_buttercup10289("d0")
& ~ b48_buttercup10283("d3")
& ~ b48_buttercup10283("d2")
& ~ b48_buttercup10283("d1")
& b48_buttercup10283("d0")
& ~ b48_buttercup10279("d3")
& ~ b48_buttercup10279("d2")
& b48_buttercup10279("d1")
& b48_buttercup10279("d0")
& ~ b48_buttercup10278("d3")
& ~ b48_buttercup10278("d2")
& ~ b48_buttercup10278("d1")
& b48_buttercup10278("d0")
& ~ b48_buttercup10277("d3")
& ~ b48_buttercup10277("d2")
& ~ b48_buttercup10277("d1")
& b48_buttercup10277("d0")
& ~ b48_buttercup10276("d3")
& ~ b48_buttercup10276("d2")
& ~ b48_buttercup10276("d1")
& b48_buttercup10276("d0")
& ~ b48_buttercup10275("d3")
& ~ b48_buttercup10275("d2")
& ~ b48_buttercup10275("d1")
& b48_buttercup10275("d0")
& ~ b48_buttercup10274("d3")
& ~ b48_buttercup10274("d2")
& ~ b48_buttercup10274("d1")
& b48_buttercup10274("d0")
& ~ b48_buttercup10273("d3")
& ~ b48_buttercup10273("d2")
& ~ b48_buttercup10273("d1")
& b48_buttercup10273("d0")
& ~ b48_buttercup10272("d3")
& ~ b48_buttercup10272("d2")
& ~ b48_buttercup10272("d1")
& b48_buttercup10272("d0")
& ~ b48_buttercup10271("d3")
& ~ b48_buttercup10271("d2")
& ~ b48_buttercup10271("d1")
& b48_buttercup10271("d0")
& ~ b48_buttercup10269("d3")
& ~ b48_buttercup10269("d2")
& ~ b48_buttercup10269("d1")
& b48_buttercup10269("d0")
& ~ b48_buttercup10268("d3")
& ~ b48_buttercup10268("d2")
& ~ b48_buttercup10268("d1")
& b48_buttercup10268("d0")
& ~ b48_buttercup10267("d3")
& ~ b48_buttercup10267("d2")
& ~ b48_buttercup10267("d1")
& b48_buttercup10267("d0")
& ~ b48_buttercup10266("d3")
& ~ b48_buttercup10266("d2")
& ~ b48_buttercup10266("d1")
& b48_buttercup10266("d0")
& ~ b48_buttercup10261("d3")
& ~ b48_buttercup10261("d2")
& b48_buttercup10261("d1")
& ~ b48_buttercup10261("d0")
& ~ b48_buttercup10260("d3")
& ~ b48_buttercup10260("d2")
& b48_buttercup10260("d1")
& ~ b48_buttercup10260("d0")
& ~ b48_buttercup10253("d3")
& ~ b48_buttercup10253("d2")
& ~ b48_buttercup10253("d1")
& b48_buttercup10253("d0")
& ~ b48_buttercup10248("d3")
& ~ b48_buttercup10248("d2")
& ~ b48_buttercup10248("d1")
& b48_buttercup10248("d0")
& ~ b48_buttercup10247("d3")
& ~ b48_buttercup10247("d2")
& ~ b48_buttercup10247("d1")
& b48_buttercup10247("d0")
& ~ b48_buttercup10240("d3")
& ~ b48_buttercup10240("d2")
& ~ b48_buttercup10240("d1")
& b48_buttercup10240("d0")
& ~ b48_buttercup10231("d3")
& ~ b48_buttercup10231("d2")
& ~ b48_buttercup10231("d1")
& b48_buttercup10231("d0")
& b48_buttercup10229("d3")
& ~ b48_buttercup10229("d2")
& ~ b48_buttercup10229("d1")
& ~ b48_buttercup10229("d0")
& ~ b48_buttercup10228("d3")
& ~ b48_buttercup10228("d2")
& ~ b48_buttercup10228("d1")
& b48_buttercup10228("d0")
& b48_buttercup10227("d3")
& ~ b48_buttercup10227("d2")
& ~ b48_buttercup10227("d1")
& ~ b48_buttercup10227("d0")
& b48_buttercup10222("d3")
& ~ b48_buttercup10222("d2")
& b48_buttercup10222("d1")
& b48_buttercup10222("d0")
& ~ b48_buttercup10220("d3")
& ~ b48_buttercup10220("d2")
& ~ b48_buttercup10220("d1")
& b48_buttercup10220("d0")
& ~ b48_buttercup10217("d3")
& ~ b48_buttercup10217("d2")
& ~ b48_buttercup10217("d1")
& b48_buttercup10217("d0")
& ~ b48_buttercup10214("d3")
& b48_buttercup10214("d2")
& ~ b48_buttercup10214("d1")
& b48_buttercup10214("d0")
& ~ b48_buttercup10210("d3")
& ~ b48_buttercup10210("d2")
& ~ b48_buttercup10210("d1")
& b48_buttercup10210("d0")
& ~ b48_buttercup10208("d3")
& b48_buttercup10208("d2")
& ~ b48_buttercup10208("d1")
& b48_buttercup10208("d0")
& ~ b48_buttercup10201("d3")
& b48_buttercup10201("d2")
& b48_buttercup10201("d1")
& b48_buttercup10201("d0")
& ~ b48_buttercup10199("d3")
& ~ b48_buttercup10199("d2")
& ~ b48_buttercup10199("d1")
& b48_buttercup10199("d0")
& ~ b48_buttercup10198("d3")
& ~ b48_buttercup10198("d2")
& ~ b48_buttercup10198("d1")
& b48_buttercup10198("d0")
& ~ b48_buttercup10197("d3")
& ~ b48_buttercup10197("d2")
& ~ b48_buttercup10197("d1")
& b48_buttercup10197("d0")
& ~ b48_buttercup10196("d3")
& ~ b48_buttercup10196("d2")
& ~ b48_buttercup10196("d1")
& b48_buttercup10196("d0")
& ~ b48_buttercup10195("d3")
& b48_buttercup10195("d2")
& ~ b48_buttercup10195("d1")
& ~ b48_buttercup10195("d0")
& ~ b48_buttercup10193("d3")
& b48_buttercup10193("d2")
& ~ b48_buttercup10193("d1")
& ~ b48_buttercup10193("d0")
& ~ b48_buttercup10191("d3")
& b48_buttercup10191("d2")
& ~ b48_buttercup10191("d1")
& ~ b48_buttercup10191("d0")
& ~ b48_buttercup10186("d3")
& b48_buttercup10186("d2")
& ~ b48_buttercup10186("d1")
& b48_buttercup10186("d0")
& ~ b48_buttercup10182("d3")
& ~ b48_buttercup10182("d2")
& ~ b48_buttercup10182("d1")
& b48_buttercup10182("d0")
& ~ b48_buttercup10180("d3")
& ~ b48_buttercup10180("d2")
& ~ b48_buttercup10180("d1")
& b48_buttercup10180("d0")
& ~ b48_buttercup10179("d3")
& b48_buttercup10179("d2")
& ~ b48_buttercup10179("d1")
& ~ b48_buttercup10179("d0")
& ~ b48_buttercup10176("d3")
& ~ b48_buttercup10176("d2")
& ~ b48_buttercup10176("d1")
& b48_buttercup10176("d0")
& ~ b48_buttercup10174("d3")
& b48_buttercup10174("d2")
& ~ b48_buttercup10174("d1")
& ~ b48_buttercup10174("d0")
& ~ b48_buttercup10173("d3")
& b48_buttercup10173("d2")
& ~ b48_buttercup10173("d1")
& ~ b48_buttercup10173("d0")
& ~ b48_buttercup10170("d3")
& b48_buttercup10170("d2")
& ~ b48_buttercup10170("d1")
& b48_buttercup10170("d0")
& ~ b48_buttercup10169("d3")
& b48_buttercup10169("d2")
& ~ b48_buttercup10169("d1")
& ~ b48_buttercup10169("d0")
& ~ b48_buttercup10167("d3")
& b48_buttercup10167("d2")
& ~ b48_buttercup10167("d1")
& ~ b48_buttercup10167("d0")
& ~ b48_buttercup10166("d3")
& b48_buttercup10166("d2")
& ~ b48_buttercup10166("d1")
& ~ b48_buttercup10166("d0")
& ~ b48_buttercup10161("d3")
& b48_buttercup10161("d2")
& ~ b48_buttercup10161("d1")
& b48_buttercup10161("d0")
& ~ b48_buttercup10160("d3")
& b48_buttercup10160("d2")
& ~ b48_buttercup10160("d1")
& ~ b48_buttercup10160("d0")
& ~ b48_buttercup10159("d3")
& b48_buttercup10159("d2")
& ~ b48_buttercup10159("d1")
& ~ b48_buttercup10159("d0")
& ~ b48_buttercup10158("d3")
& b48_buttercup10158("d2")
& ~ b48_buttercup10158("d1")
& ~ b48_buttercup10158("d0")
& ~ b48_buttercup10156("d3")
& b48_buttercup10156("d2")
& ~ b48_buttercup10156("d1")
& ~ b48_buttercup10156("d0")
& ~ b48_buttercup10154("d3")
& b48_buttercup10154("d2")
& ~ b48_buttercup10154("d1")
& ~ b48_buttercup10154("d0")
& ~ b48_buttercup10150("d3")
& b48_buttercup10150("d2")
& ~ b48_buttercup10150("d1")
& b48_buttercup10150("d0")
& ~ b48_buttercup10143("d3")
& ~ b48_buttercup10143("d2")
& ~ b48_buttercup10143("d1")
& b48_buttercup10143("d0")
& ~ b48_buttercup10134("d3")
& b48_buttercup10134("d2")
& ~ b48_buttercup10134("d1")
& ~ b48_buttercup10134("d0")
& ~ b48_buttercup10133("d3")
& b48_buttercup10133("d2")
& ~ b48_buttercup10133("d1")
& ~ b48_buttercup10133("d0")
& ~ b48_buttercup10130("d3")
& b48_buttercup10130("d2")
& ~ b48_buttercup10130("d1")
& b48_buttercup10130("d0")
& ~ b48_buttercup10121("d3")
& ~ b48_buttercup10121("d2")
& ~ b48_buttercup10121("d1")
& b48_buttercup10121("d0")
& ~ b48_buttercup10120("d3")
& b48_buttercup10120("d2")
& ~ b48_buttercup10120("d1")
& ~ b48_buttercup10120("d0")
& ~ b48_buttercup10119("d3")
& ~ b48_buttercup10119("d2")
& ~ b48_buttercup10119("d1")
& b48_buttercup10119("d0")
& ~ b48_buttercup10115("d3")
& b48_buttercup10115("d2")
& ~ b48_buttercup10115("d1")
& b48_buttercup10115("d0")
& ~ b48_buttercup10111("d3")
& b48_buttercup10111("d2")
& ~ b48_buttercup10111("d1")
& ~ b48_buttercup10111("d0")
& ~ b48_buttercup10110("d3")
& b48_buttercup10110("d2")
& ~ b48_buttercup10110("d1")
& ~ b48_buttercup10110("d0")
& ~ b48_buttercup10109("d3")
& b48_buttercup10109("d2")
& ~ b48_buttercup10109("d1")
& ~ b48_buttercup10109("d0")
& ~ b48_buttercup10108("d3")
& b48_buttercup10108("d2")
& ~ b48_buttercup10108("d1")
& ~ b48_buttercup10108("d0")
& b48_buttercup10107("d3")
& b48_buttercup10107("d2")
& ~ b48_buttercup10107("d1")
& b48_buttercup10107("d0")
& ~ b48_buttercup10104("d3")
& b48_buttercup10104("d2")
& ~ b48_buttercup10104("d1")
& ~ b48_buttercup10104("d0")
& ~ b48_buttercup10102("d3")
& b48_buttercup10102("d2")
& ~ b48_buttercup10102("d1")
& ~ b48_buttercup10102("d0")
& b48_buttercup10098("d3")
& b48_buttercup10098("d2")
& b48_buttercup10098("d1")
& b48_buttercup10098("d0")
& ~ b48_buttercup10092("d3")
& b48_buttercup10092("d2")
& ~ b48_buttercup10092("d1")
& ~ b48_buttercup10092("d0")
& ~ b48_buttercup10086("d3")
& ~ b48_buttercup10086("d2")
& ~ b48_buttercup10086("d1")
& b48_buttercup10086("d0")
& ~ b48_buttercup10085("d3")
& b48_buttercup10085("d2")
& ~ b48_buttercup10085("d1")
& ~ b48_buttercup10085("d0")
& ~ b48_buttercup10082("d3")
& ~ b48_buttercup10082("d2")
& ~ b48_buttercup10082("d1")
& b48_buttercup10082("d0")
& ~ b48_buttercup10076("d3")
& ~ b48_buttercup10076("d2")
& ~ b48_buttercup10076("d1")
& b48_buttercup10076("d0")
& ~ b48_buttercup10075("d3")
& b48_buttercup10075("d2")
& ~ b48_buttercup10075("d1")
& ~ b48_buttercup10075("d0")
& ~ b48_buttercup10072("d3")
& ~ b48_buttercup10072("d2")
& ~ b48_buttercup10072("d1")
& b48_buttercup10072("d0")
& ~ b48_buttercup10070("d3")
& b48_buttercup10070("d2")
& ~ b48_buttercup10070("d1")
& ~ b48_buttercup10070("d0")
& ~ b48_buttercup10068("d3")
& b48_buttercup10068("d2")
& ~ b48_buttercup10068("d1")
& ~ b48_buttercup10068("d0")
& ~ b48_buttercup10065("d3")
& ~ b48_buttercup10065("d2")
& ~ b48_buttercup10065("d1")
& b48_buttercup10065("d0")
& ~ b48_buttercup10058("d3")
& ~ b48_buttercup10058("d2")
& ~ b48_buttercup10058("d1")
& b48_buttercup10058("d0")
& ~ b48_buttercup10054("d3")
& b48_buttercup10054("d2")
& ~ b48_buttercup10054("d1")
& b48_buttercup10054("d0")
& ~ b48_buttercup10052("d3")
& ~ b48_buttercup10052("d2")
& ~ b48_buttercup10052("d1")
& b48_buttercup10052("d0")
& ~ b48_buttercup10050("d3")
& ~ b48_buttercup10050("d2")
& ~ b48_buttercup10050("d1")
& b48_buttercup10050("d0")
& ~ b48_buttercup10046("d3")
& ~ b48_buttercup10046("d2")
& ~ b48_buttercup10046("d1")
& b48_buttercup10046("d0")
& ~ b48_buttercup10045("d3")
& ~ b48_buttercup10045("d2")
& ~ b48_buttercup10045("d1")
& b48_buttercup10045("d0")
& ~ b48_buttercup10043("d3")
& ~ b48_buttercup10043("d2")
& ~ b48_buttercup10043("d1")
& b48_buttercup10043("d0")
& ~ b48_buttercup10035("d3")
& ~ b48_buttercup10035("d2")
& ~ b48_buttercup10035("d1")
& b48_buttercup10035("d0")
& ~ b48_buttercup10034("d3")
& ~ b48_buttercup10034("d2")
& ~ b48_buttercup10034("d1")
& b48_buttercup10034("d0")
& ~ b48_buttercup10031("d3")
& ~ b48_buttercup10031("d2")
& ~ b48_buttercup10031("d1")
& b48_buttercup10031("d0")
& ~ b48_buttercup10029("d3")
& b48_buttercup10029("d2")
& ~ b48_buttercup10029("d1")
& b48_buttercup10029("d0")
& ~ b48_buttercup10024("d3")
& b48_buttercup10024("d2")
& b48_buttercup10024("d1")
& b48_buttercup10024("d0")
& ~ b48_buttercup10022("d3")
& b48_buttercup10022("d2")
& ~ b48_buttercup10022("d1")
& ~ b48_buttercup10022("d0")
& ~ b48_buttercup10021("d3")
& b48_buttercup10021("d2")
& ~ b48_buttercup10021("d1")
& ~ b48_buttercup10021("d0")
& ~ b48_buttercup10019("d3")
& b48_buttercup10019("d2")
& ~ b48_buttercup10019("d1")
& ~ b48_buttercup10019("d0")
& ~ b48_buttercup10013("d3")
& b48_buttercup10013("d2")
& ~ b48_buttercup10013("d1")
& b48_buttercup10013("d0")
& b48_buttercup10007("d3")
& b48_buttercup10007("d2")
& b48_buttercup10007("d1")
& b48_buttercup10007("d0") ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO581+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.04 % Command : mace4 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n002.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sat Sep 26 19:33:08 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.36 % Mace4 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.36 % Process 2515832 was started by sandbox2 on n002,
% 0.10/0.36 % Sat Sep 26 19:33:08 2026
% 0.10/0.36 % The command was "/export/starexec/sandbox2/solver/bin/mace4 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.38/0.67
% 0.38/0.67 % SZS status CounterSatisfiable for theBenchmark
% 0.38/0.67 % SZS output start FiniteModel for theBenchmark
% See solution above
%------------------------------------------------------------------------------