%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : SYO581+1 : TPTP v9.2.1. Released v5.5.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n011.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 09:14:47 AM UTC 2026 % Result : CounterSatisfiable 44.00s 44.15s % Output : Model 44.00s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYO581+1 : TPTP v9.2.1. Released v5.5.0. % 0.13/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.18/0.34 % Computer : n011.cluster.edu % 0.18/0.34 % Model : x86_64 x86_64 % 0.18/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.34 % Memory : 8042.1875MB % 0.18/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.34 % CPULimit : 300 % 0.18/0.35 % WCLimit : 300 % 0.18/0.35 % DateTime : Wed Jun 3 00:21:50 EDT 2026 % 0.18/0.35 % CPUTime : % 0.39/0.61 %----Disproving FOF, CNF % 44.00/44.15 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 12... % 44.00/44.15 --- Run --no-e-matching --full-saturate-quant at 12... % 44.00/44.15 --- Run --no-e-matching --enum-inst-sum --full-saturate-quant at 12... % 44.00/44.15 --- Run --finite-model-find --uf-ss=no-minimal at 54... % 44.00/44.15 % SZS status CounterSatisfiable % 44.00/44.15 % SZS output start Model % 44.00/44.15 ( % 44.00/44.15 ; cardinality of $$unsorted is 6 % 44.00/44.15 ; rep: (as @$$unsorted_0 $$unsorted) % 44.00/44.15 ; rep: (as @$$unsorted_1 $$unsorted) % 44.00/44.15 ; rep: (as @$$unsorted_2 $$unsorted) % 44.00/44.15 ; rep: (as @$$unsorted_3 $$unsorted) % 44.00/44.15 ; rep: (as @$$unsorted_4 $$unsorted) % 44.00/44.15 ; rep: (as @$$unsorted_5 $$unsorted) % 44.00/44.15 (define-fun tptp.k04_buttercup10049 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10048 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10051 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10096 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10095 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10097 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10342 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10337 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10347 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10351 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10453 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10449 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10462 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10464 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10482 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10477 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10486 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10546 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10544 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10547 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10406 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10404 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10408 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10599 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10593 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10602 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10236 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10234 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10238 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10371 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10369 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10373 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10376 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10296 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10293 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10298 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10637 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10635 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10639 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10641 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10028 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10026 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10033 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10425 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10424 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10206 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10204 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10213 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10219 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10061 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10057 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10064 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10067 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10074 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10559 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10555 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10620 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10619 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10622 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10506 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10504 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10142 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10139 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10517 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10516 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10184 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10012 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10190 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10200 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10221 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10225 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10244 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10252 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10282 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10303 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10312 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10316 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10325 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10329 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10333 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10356 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10016 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10039 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10053 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10079 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10084 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10089 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10100 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10117 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10125 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10132 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10135 (($x1 $$unsorted)) Bool (= (as @$$unsorted_2 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10147 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10153 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10164 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10172 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10181 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10364 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10380 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10382 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10385 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10389 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10391 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10397 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10400 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10415 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10419 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10430 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10437 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10445 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10470 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10473 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10492 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10495 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10499 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10510 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10524 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10529 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10535 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10551 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10567 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10578 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10581 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10586 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10608 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10611 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10626 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10628 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10631 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10643 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10050 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10046 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10052 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10305 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10300 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10307 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10308 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10227 (($x1 $$unsorted)) Bool (= (as @$$unsorted_4 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10222 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10228 (($x1 $$unsorted)) Bool (= (as @$$unsorted_4 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10229 (($x1 $$unsorted)) Bool (= (as @$$unsorted_4 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10191 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10186 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10193 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10195 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10133 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10130 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10134 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10343 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10334 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10344 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10348 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10352 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10267 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10266 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10268 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10102 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10098 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10104 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10107 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10108 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10109 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10110 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10111 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10441 (($x1 $$unsorted)) Bool (= (as @$$unsorted_2 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10440 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10442 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10478 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10474 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10479 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10483 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10487 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10489 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10545 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10542 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10548 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10275 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10274 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10276 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10277 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10278 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10405 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10402 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10410 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10166 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10161 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10167 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10169 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10119 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10115 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10120 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10596 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10589 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10604 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10370 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10367 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10374 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10377 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10294 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10291 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10299 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10318 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10313 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10320 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10173 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10170 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10174 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10636 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10632 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10638 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10640 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10029 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10024 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10031 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10034 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10574 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10563 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10154 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10150 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10156 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10158 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10159 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10160 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10208 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10201 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10210 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10214 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10217 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10220 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10513 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10512 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10514 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10058 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10054 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10065 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10068 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10070 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10072 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10075 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10561 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10552 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10562 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10518 (($x1 $$unsorted)) Bool (= (as @$$unsorted_4 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10515 (($x1 $$unsorted)) Bool (= (as @$$unsorted_4 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10519 (($x1 $$unsorted)) Bool (= (as @$$unsorted_4 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10520 (($x1 $$unsorted)) Bool (= (as @$$unsorted_4 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10521 (($x1 $$unsorted)) Bool (= (as @$$unsorted_4 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10273 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10271 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10007 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10196 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10197 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10198 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10199 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10231 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10240 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10247 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10248 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10269 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10272 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10279 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10309 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10322 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10326 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10332 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10353 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10362 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10013 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10035 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10076 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10082 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10085 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10086 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10092 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10121 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10143 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10176 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10180 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10182 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10365 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10378 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10381 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10383 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10386 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10394 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10398 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10411 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10417 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10420 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10427 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10433 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10434 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10443 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10446 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10450 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10469 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10471 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10490 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10493 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10496 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10502 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10507 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10522 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10526 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10530 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10531 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10549 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10570 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10572 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10575 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10579 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10582 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10605 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10606 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10609 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10612 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10616 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10624 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10629 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10642 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10646 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10465 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10466 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10467 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10456 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10458 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10022 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10021 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10019 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10288 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10290 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.k04_buttercup10357 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10361 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10289 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10421 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10454 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10460 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.b48_buttercup10179 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10004 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10286 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10283 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.k04_buttercup10000 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10360 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10359 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.k04_buttercup10540 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10541 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.k04_buttercup10539 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10538 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10451 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 44.00/44.15 (define-fun tptp.k04_buttercup10044 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10043 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.k04_buttercup10042 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10045 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10261 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.k04_buttercup10259 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.k04_buttercup10255 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10253 (($x1 $$unsorted)) Bool true) % 44.00/44.15 (define-fun tptp.b48_buttercup10260 (($x1 $$unsorted)) Bool (= (as @$$unsorted_1 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10422 (($x1 $$unsorted)) Bool (= (as @$$unsorted_2 $$unsorted) $x1)) % 44.00/44.15 (define-fun tptp.b48_buttercup10358 ((_arg_1 $$unsorted)) Bool true) % 44.00/44.15 ) % 44.00/44.15 % SZS output end Model % 44.00/44.15 % cvc5 exiting %------------------------------------------------------------------------------