%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : NLP003^7 : TPTP v9.2.1. Released v5.5.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n007.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 08:37:20 AM UTC 2026 % Result : CounterSatisfiable 194.27s 195.71s % Output : Model 194.27s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NLP003^7 : TPTP v9.2.1. Released v5.5.0. % 0.11/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.17/0.34 % Computer : n007.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Tue Jun 2 09:50:41 EDT 2026 % 0.17/0.34 % CPUTime : % 0.28/0.53 %----Disproving TH0 % 194.27/195.71 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 72s... % 194.27/195.71 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --mbqi-enum-choice-grammar-all --no-cegqi --no-sygus-inst at 30s... % 194.27/195.71 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-mbqi-nested-check --no-cegqi --no-sygus-inst at 18s... % 194.27/195.71 --- Run --ho-elim --full-saturate-quant at 9s... % 194.27/195.71 --- Run --ho-elim --no-e-matching --full-saturate-quant at 9s... % 194.27/195.71 --- Run --ho-elim --no-e-matching --enum-inst-sum --full-saturate-quant at 9s... % 194.27/195.71 --- Run --ho-elim --finite-model-find --uf-ss=no-minimal at 30s... % 194.27/195.71 --- Run --no-ho-matching --finite-model-find --uf-ss=no-minimal at 75s... % 194.27/195.71 % SZS status CounterSatisfiable % 194.27/195.71 % SZS output start Model % 194.27/195.71 ( % 194.27/195.71 ; cardinality of $$unsorted is 1 % 194.27/195.71 ; rep: (as @$$unsorted_0 $$unsorted) % 194.27/195.71 ; cardinality of tptp.mu is 7 % 194.27/195.71 ; rep: (as @tptp.mu_0 tptp.mu) % 194.27/195.71 ; rep: (as @tptp.mu_1 tptp.mu) % 194.27/195.71 ; rep: (as @tptp.mu_2 tptp.mu) % 194.27/195.71 ; rep: (as @tptp.mu_3 tptp.mu) % 194.27/195.71 ; rep: (as @tptp.mu_4 tptp.mu) % 194.27/195.71 ; rep: (as @tptp.mu_5 tptp.mu) % 194.27/195.71 ; rep: (as @tptp.mu_6 tptp.mu) % 194.27/195.71 (define-fun tptp.qmltpeq ((BOUND_VARIABLE_64792 tptp.mu) (BOUND_VARIABLE_64794 tptp.mu) (BOUND_VARIABLE_64796 $$unsorted)) Bool (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_64792) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_64794) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64796)) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_64792) (and (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_64794) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64796)) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_64792) (and (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_64794) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64796)) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_64792) (and (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_64794) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64796)) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_64792) (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_64794) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64796))))))) % 194.27/195.71 (define-fun tptp.meq_prop ((X (-> $$unsorted Bool)) (Y (-> $$unsorted Bool)) (W $$unsorted)) Bool (= (@ X W) (@ Y W))) % 194.27/195.71 (define-fun tptp.mnot ((Phi (-> $$unsorted Bool)) (W $$unsorted)) Bool (not (@ Phi W))) % 194.27/195.71 (define-fun tptp.mor ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (W $$unsorted)) Bool (or (@ Phi W) (@ Psi W))) % 194.27/195.71 (define-fun tptp.mbox ((R (-> $$unsorted $$unsorted Bool)) (Phi (-> $$unsorted Bool)) (W $$unsorted)) Bool (forall ((V $$unsorted)) (or (not (R W V)) (Phi V)))) % 194.27/195.71 (define-fun tptp.mforall_prop ((Phi (-> (-> $$unsorted Bool) $$unsorted Bool)) (W $$unsorted)) Bool (forall ((P (-> $$unsorted Bool))) (Phi P W))) % 194.27/195.71 (define-fun tptp.mtrue ((BOUND_VARIABLE_2171 $$unsorted)) Bool true) % 194.27/195.71 (define-fun tptp.mfalse ((BOUND_VARIABLE_64310 $$unsorted)) Bool false) % 194.27/195.71 (define-fun tptp.mand ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) Bool (not (or (not (@ Phi __flatten_var_0)) (not (@ Psi __flatten_var_0))))) % 194.27/195.71 (define-fun tptp.mimplies ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) Bool (or (not (@ Phi __flatten_var_0)) (@ Psi __flatten_var_0))) % 194.27/195.71 (define-fun tptp.mimplied ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) Bool (or (not (@ Psi __flatten_var_0)) (@ Phi __flatten_var_0))) % 194.27/195.71 (define-fun tptp.mequiv ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) Bool (not (or (not (or (not (@ Phi __flatten_var_0)) (@ Psi __flatten_var_0))) (not (or (not (@ Psi __flatten_var_0)) (@ Phi __flatten_var_0)))))) % 194.27/195.71 (define-fun tptp.mxor ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) Bool (or (not (or (not (@ Phi __flatten_var_0)) (@ Psi __flatten_var_0))) (not (or (not (@ Psi __flatten_var_0)) (@ Phi __flatten_var_0))))) % 194.27/195.71 (define-fun tptp.mdia ((R (-> $$unsorted $$unsorted Bool)) (Phi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) Bool (not (forall ((V $$unsorted)) (or (not (R __flatten_var_0 V)) (not (Phi V)))))) % 194.27/195.71 (define-fun tptp.exists_in_world ((BOUND_VARIABLE_65231 tptp.mu) (BOUND_VARIABLE_65233 $$unsorted)) Bool (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65231) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65233) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65231) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65233) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_65231) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65233) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_65231) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65233)))))) % 194.27/195.71 (define-fun tptp.mforall_ind ((Phi (-> tptp.mu $$unsorted Bool)) (W $$unsorted)) Bool (forall ((X tptp.mu)) (or (not (tptp.exists_in_world X W)) (Phi X W)))) % 194.27/195.71 (define-fun tptp.mexists_ind ((Phi (-> tptp.mu $$unsorted Bool)) (__flatten_var_0 $$unsorted)) Bool (not (forall ((X tptp.mu)) (or (not (tptp.exists_in_world X __flatten_var_0)) (not (Phi X __flatten_var_0)))))) % 194.27/195.71 (define-fun tptp.mexists_prop ((Phi (-> (-> $$unsorted Bool) $$unsorted Bool)) (__flatten_var_0 $$unsorted)) Bool (not (forall ((P (-> $$unsorted Bool))) (not (Phi P __flatten_var_0))))) % 194.27/195.71 (define-fun tptp.mreflexive ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((S $$unsorted)) (R S S))) % 194.27/195.71 (define-fun tptp.msymmetric ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((S $$unsorted) (T $$unsorted)) (or (not (R S T)) (R T S)))) % 194.27/195.71 (define-fun tptp.mserial ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((S $$unsorted)) (not (forall ((T $$unsorted)) (not (R S T)))))) % 194.27/195.71 (define-fun tptp.mtransitive ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((S $$unsorted) (T $$unsorted) (U $$unsorted)) (or (not (R S T)) (not (R T U)) (R S U)))) % 194.27/195.71 (define-fun tptp.meuclidean ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((S $$unsorted) (T $$unsorted) (U $$unsorted)) (or (not (R S T)) (not (R S U)) (R T U)))) % 194.27/195.71 (define-fun tptp.mpartially_functional ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((S $$unsorted) (T $$unsorted) (U $$unsorted)) (or (not (R S T)) (not (R S U)) (= T U)))) % 194.27/195.71 (define-fun tptp.mfunctional ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((S $$unsorted)) (not (forall ((T $$unsorted)) (or (not (R S T)) (not (forall ((U $$unsorted)) (or (not (R S U)) (= T U))))))))) % 194.27/195.71 (define-fun tptp.mweakly_dense ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((S $$unsorted) (T $$unsorted)) (or (not (R S T)) (not (forall ((BOUND_VARIABLE_966 $$unsorted)) (or (not (R S BOUND_VARIABLE_966)) (not (R BOUND_VARIABLE_966 T)))))))) % 194.27/195.71 (define-fun tptp.mweakly_connected ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((S $$unsorted) (T $$unsorted) (U $$unsorted)) (or (not (R S T)) (not (R S U)) (R T U) (= T U) (R U T)))) % 194.27/195.71 (define-fun tptp.mweakly_directed ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((S $$unsorted) (T $$unsorted) (U $$unsorted)) (or (not (R S T)) (not (R S U)) (not (forall ((V $$unsorted)) (or (not (R T V)) (not (R U V)))))))) % 194.27/195.71 (define-fun tptp.mvalid ((Phi (-> $$unsorted Bool))) Bool (forall ((W $$unsorted)) (Phi W))) % 194.27/195.71 (define-fun tptp.msatisfiable ((Phi (-> $$unsorted Bool))) Bool (not (forall ((W $$unsorted)) (not (Phi W))))) % 194.27/195.71 (define-fun tptp.mcountersatisfiable ((Phi (-> $$unsorted Bool))) Bool (not (forall ((W $$unsorted)) (Phi W)))) % 194.27/195.71 (define-fun tptp.minvalid ((Phi (-> $$unsorted Bool))) Bool (forall ((W $$unsorted)) (not (Phi W)))) % 194.27/195.71 (define-fun tptp.rel_s4 ((BOUND_VARIABLE_65339 $$unsorted) (BOUND_VARIABLE_65341 $$unsorted)) Bool (and (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65339) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65341))) % 194.27/195.71 (define-fun tptp.mbox_s4 ((Phi (-> $$unsorted Bool)) (W $$unsorted)) Bool (forall ((V $$unsorted)) (or (not (tptp.rel_s4 W V)) (Phi V)))) % 194.27/195.71 (define-fun tptp.mdia_s4 ((Phi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) Bool (not (forall ((V $$unsorted)) (or (not (tptp.rel_s4 __flatten_var_0 V)) (not (Phi V)))))) % 194.27/195.71 (define-fun tptp.vehicle ((BOUND_VARIABLE_65836 tptp.mu) (BOUND_VARIABLE_65838 $$unsorted)) Bool (ite (= (as @tptp.mu_5 tptp.mu) BOUND_VARIABLE_65836) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65838) (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_65836) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65838) (and (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65836) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65838))))) % 194.27/195.71 (define-fun tptp.transport ((BOUND_VARIABLE_65836 tptp.mu) (BOUND_VARIABLE_65838 $$unsorted)) Bool (ite (= (as @tptp.mu_5 tptp.mu) BOUND_VARIABLE_65836) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65838) (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_65836) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65838) (and (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65836) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65838))))) % 194.27/195.71 (define-fun tptp.instrumentality ((BOUND_VARIABLE_65836 tptp.mu) (BOUND_VARIABLE_65838 $$unsorted)) Bool (ite (= (as @tptp.mu_5 tptp.mu) BOUND_VARIABLE_65836) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65838) (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_65836) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65838) (and (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65836) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65838))))) % 194.27/195.71 (define-fun tptp.artifact ((BOUND_VARIABLE_65988 tptp.mu) (BOUND_VARIABLE_65990 $$unsorted)) Bool (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_65988) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65990) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65988) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65990) (and (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65988) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65990))))) % 194.27/195.71 (define-fun tptp.location ((BOUND_VARIABLE_66214 tptp.mu) (BOUND_VARIABLE_66216 $$unsorted)) Bool (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_66214) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66216) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66214) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66216)))) % 194.27/195.71 (define-fun tptp.object ((BOUND_VARIABLE_66414 tptp.mu) (BOUND_VARIABLE_66416 $$unsorted)) Bool (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_66414) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66416) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_66414) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66416) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66414) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66416))))) % 194.27/195.71 (define-fun tptp.new ((BOUND_VARIABLE_66782 tptp.mu) (BOUND_VARIABLE_66784 $$unsorted)) Bool (ite (= (as @tptp.mu_6 tptp.mu) BOUND_VARIABLE_66782) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66784) (ite (= (as @tptp.mu_5 tptp.mu) BOUND_VARIABLE_66782) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66784) (and (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_66782) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66784))))) % 194.27/195.71 (define-fun tptp.eventuality ((BOUND_VARIABLE_64518 tptp.mu) (BOUND_VARIABLE_64520 $$unsorted)) Bool (and (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_64518) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64520))) % 194.27/195.71 (define-fun tptp.abstraction ((BOUND_VARIABLE_66782 tptp.mu) (BOUND_VARIABLE_66784 $$unsorted)) Bool (ite (= (as @tptp.mu_6 tptp.mu) BOUND_VARIABLE_66782) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66784) (ite (= (as @tptp.mu_5 tptp.mu) BOUND_VARIABLE_66782) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66784) (and (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_66782) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66784))))) % 194.27/195.71 (define-fun tptp.man ((BOUND_VARIABLE_66782 tptp.mu) (BOUND_VARIABLE_66784 $$unsorted)) Bool (ite (= (as @tptp.mu_6 tptp.mu) BOUND_VARIABLE_66782) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66784) (ite (= (as @tptp.mu_5 tptp.mu) BOUND_VARIABLE_66782) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66784) (and (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_66782) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66784))))) % 194.27/195.71 (define-fun tptp.male ((BOUND_VARIABLE_66782 tptp.mu) (BOUND_VARIABLE_66784 $$unsorted)) Bool (ite (= (as @tptp.mu_6 tptp.mu) BOUND_VARIABLE_66782) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66784) (ite (= (as @tptp.mu_5 tptp.mu) BOUND_VARIABLE_66782) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66784) (and (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_66782) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66784))))) % 194.27/195.71 (define-fun tptp.female ((BOUND_VARIABLE_67586 tptp.mu) (BOUND_VARIABLE_67588 $$unsorted)) Bool (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_67586) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67588) (and (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67586) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67588)))) % 194.27/195.71 (define-fun tptp.woman ((BOUND_VARIABLE_67586 tptp.mu) (BOUND_VARIABLE_67588 $$unsorted)) Bool (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_67586) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67588) (and (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67586) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67588)))) % 194.27/195.71 (define-fun tptp.proposition ((BOUND_VARIABLE_67586 tptp.mu) (BOUND_VARIABLE_67588 $$unsorted)) Bool (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_67586) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67588) (and (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67586) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67588)))) % 194.27/195.71 (define-fun tptp.drs ((BOUND_VARIABLE_67586 tptp.mu) (BOUND_VARIABLE_67588 $$unsorted)) Bool (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_67586) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67588) (and (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67586) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67588)))) % 194.27/195.71 (define-fun tptp.entity ((BOUND_VARIABLE_66414 tptp.mu) (BOUND_VARIABLE_66416 $$unsorted)) Bool (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_66414) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66416) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_66414) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66416) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66414) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66416))))) % 194.27/195.71 (define-fun tptp.owner ((BOUND_VARIABLE_67586 tptp.mu) (BOUND_VARIABLE_67588 $$unsorted)) Bool (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_67586) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67588) (and (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67586) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67588)))) % 194.27/195.71 (define-fun tptp.human ((BOUND_VARIABLE_67586 tptp.mu) (BOUND_VARIABLE_67588 $$unsorted)) Bool (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_67586) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67588) (and (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67586) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67588)))) % 194.27/195.71 (define-fun tptp.nonhuman ((BOUND_VARIABLE_65836 tptp.mu) (BOUND_VARIABLE_65838 $$unsorted)) Bool (ite (= (as @tptp.mu_5 tptp.mu) BOUND_VARIABLE_65836) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65838) (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_65836) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65838) (and (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65836) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65838))))) % 194.27/195.71 (define-fun tptp.have ((BOUND_VARIABLE_68908 tptp.mu) (BOUND_VARIABLE_68910 tptp.mu) (BOUND_VARIABLE_68912 tptp.mu) (BOUND_VARIABLE_68914 $$unsorted)) Bool (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_68908) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_68910) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914))))) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_68910) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914))))) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_68910) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914))))) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_68910) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914))))))))) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_68908) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_68910) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914))))) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_68910) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914))))) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_68910) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914))))) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_68910) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914))))))))) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_68908) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_68910) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914))))) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_68910) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914))))) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_68910) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914))))) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_68910) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914))))))))) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_68908) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_68910) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914))))) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_68910) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914))))) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_68910) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914))))) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_68910) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_68912) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_68914)))))))))))))) % 194.27/195.71 (define-fun tptp.of ((BOUND_VARIABLE_67894 tptp.mu) (BOUND_VARIABLE_67896 tptp.mu) (BOUND_VARIABLE_67898 $$unsorted)) Bool (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_67894) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898))))) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67894) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898))))) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_67894) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898))))) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_67894) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898)))))))))) % 194.27/195.71 (define-fun tptp.partof ((BOUND_VARIABLE_64792 tptp.mu) (BOUND_VARIABLE_64794 tptp.mu) (BOUND_VARIABLE_64796 $$unsorted)) Bool (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_64792) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_64794) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64796)) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_64792) (and (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_64794) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64796)) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_64792) (and (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_64794) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64796)) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_64792) (and (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_64794) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64796)) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_64792) (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_64794) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64796))))))) % 194.27/195.71 (define-fun tptp.in ((BOUND_VARIABLE_67894 tptp.mu) (BOUND_VARIABLE_67896 tptp.mu) (BOUND_VARIABLE_67898 $$unsorted)) Bool (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_67894) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898))))) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67894) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898))))) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_67894) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898))))) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_67894) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898)))))))))) % 194.27/195.71 (define-fun tptp.down ((BOUND_VARIABLE_67894 tptp.mu) (BOUND_VARIABLE_67896 tptp.mu) (BOUND_VARIABLE_67898 $$unsorted)) Bool (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_67894) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898))))) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67894) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898))))) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_67894) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898))))) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_67894) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898)))))))))) % 194.27/195.71 (define-fun tptp.barrel ((BOUND_VARIABLE_67894 tptp.mu) (BOUND_VARIABLE_67896 tptp.mu) (BOUND_VARIABLE_67898 $$unsorted)) Bool (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_67894) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898))))) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67894) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898))))) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_67894) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898))))) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_67894) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_67896) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67898)))))))))) % 194.27/195.71 (define-fun tptp.lonely ((BOUND_VARIABLE_65231 tptp.mu) (BOUND_VARIABLE_65233 $$unsorted)) Bool (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65231) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65233) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65231) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65233) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_65231) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65233) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_65231) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65233)))))) % 194.27/195.71 (define-fun tptp.way ((BOUND_VARIABLE_67586 tptp.mu) (BOUND_VARIABLE_67588 $$unsorted)) Bool (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_67586) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67588) (and (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67586) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67588)))) % 194.27/195.71 (define-fun tptp.street ((BOUND_VARIABLE_67586 tptp.mu) (BOUND_VARIABLE_67588 $$unsorted)) Bool (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_67586) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67588) (and (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_67586) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_67588)))) % 194.27/195.71 (define-fun tptp.old ((BOUND_VARIABLE_65231 tptp.mu) (BOUND_VARIABLE_65233 $$unsorted)) Bool (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65231) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65233) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65231) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65233) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_65231) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65233) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_65231) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65233)))))) % 194.27/195.71 (define-fun tptp.dirty ((BOUND_VARIABLE_65231 tptp.mu) (BOUND_VARIABLE_65233 $$unsorted)) Bool (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65231) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65233) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65231) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65233) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_65231) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65233) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_65231) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65233)))))) % 194.27/195.71 (define-fun tptp.white ((BOUND_VARIABLE_65231 tptp.mu) (BOUND_VARIABLE_65233 $$unsorted)) Bool (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65231) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65233) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65231) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65233) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_65231) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65233) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_65231) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65233)))))) % 194.27/195.71 (define-fun tptp.car ((BOUND_VARIABLE_65836 tptp.mu) (BOUND_VARIABLE_65838 $$unsorted)) Bool (ite (= (as @tptp.mu_5 tptp.mu) BOUND_VARIABLE_65836) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65838) (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_65836) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65838) (and (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65836) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65838))))) % 194.27/195.71 (define-fun tptp.chevy ((BOUND_VARIABLE_65836 tptp.mu) (BOUND_VARIABLE_65838 $$unsorted)) Bool (ite (= (as @tptp.mu_5 tptp.mu) BOUND_VARIABLE_65836) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65838) (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_65836) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65838) (and (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65836) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65838))))) % 194.27/195.71 (define-fun tptp.event ((BOUND_VARIABLE_64518 tptp.mu) (BOUND_VARIABLE_64520 $$unsorted)) Bool (and (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_64518) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64520))) % 194.27/195.71 (define-fun tptp.city ((BOUND_VARIABLE_66214 tptp.mu) (BOUND_VARIABLE_66216 $$unsorted)) Bool (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_66214) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66216) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66214) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66216)))) % 194.27/195.71 (define-fun tptp.hollywood ((BOUND_VARIABLE_66214 tptp.mu) (BOUND_VARIABLE_66216 $$unsorted)) Bool (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_66214) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66216) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66214) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66216)))) % 194.27/195.71 ) % 194.27/195.71 % SZS output end Model % 194.27/195.71 % cvc5 exiting %------------------------------------------------------------------------------