%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : NLP002^7 : 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 08:37:20 AM UTC 2026 % Result : CounterSatisfiable 192.45s 192.72s % Output : Model 192.45s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : NLP002^7 : TPTP v9.2.1. Released v5.5.0. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.16/0.34 % Computer : n011.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue Jun 2 09:50:35 EDT 2026 % 0.16/0.34 % CPUTime : % 0.30/0.52 %----Disproving TH0 % 192.45/192.72 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 72s... % 192.45/192.72 --- 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... % 192.45/192.72 --- 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... % 192.45/192.72 --- Run --ho-elim --full-saturate-quant at 9s... % 192.45/192.72 --- Run --ho-elim --no-e-matching --full-saturate-quant at 9s... % 192.45/192.72 --- Run --ho-elim --no-e-matching --enum-inst-sum --full-saturate-quant at 9s... % 192.45/192.72 --- Run --ho-elim --finite-model-find --uf-ss=no-minimal at 30s... % 192.45/192.72 --- Run --no-ho-matching --finite-model-find --uf-ss=no-minimal at 75s... % 192.45/192.72 % SZS status CounterSatisfiable % 192.45/192.72 % SZS output start Model % 192.45/192.72 ( % 192.45/192.72 ; cardinality of $$unsorted is 1 % 192.45/192.72 ; rep: (as @$$unsorted_0 $$unsorted) % 192.45/192.72 ; cardinality of tptp.mu is 7 % 192.45/192.72 ; rep: (as @tptp.mu_0 tptp.mu) % 192.45/192.72 ; rep: (as @tptp.mu_1 tptp.mu) % 192.45/192.72 ; rep: (as @tptp.mu_2 tptp.mu) % 192.45/192.72 ; rep: (as @tptp.mu_3 tptp.mu) % 192.45/192.72 ; rep: (as @tptp.mu_4 tptp.mu) % 192.45/192.72 ; rep: (as @tptp.mu_5 tptp.mu) % 192.45/192.72 ; rep: (as @tptp.mu_6 tptp.mu) % 192.45/192.72 (define-fun tptp.qmltpeq ((BOUND_VARIABLE_62533 tptp.mu) (BOUND_VARIABLE_62535 tptp.mu) (BOUND_VARIABLE_62537 $$unsorted)) Bool (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_62533) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_62535) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62537)) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_62533) (and (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_62535) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62537)) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_62533) (and (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_62535) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62537)) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_62533) (and (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_62535) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62537)) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_62533) (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_62535) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62537))))))) % 192.45/192.72 (define-fun tptp.meq_prop ((X (-> $$unsorted Bool)) (Y (-> $$unsorted Bool)) (W $$unsorted)) Bool (= (@ X W) (@ Y W))) % 192.45/192.72 (define-fun tptp.mnot ((Phi (-> $$unsorted Bool)) (W $$unsorted)) Bool (not (@ Phi W))) % 192.45/192.72 (define-fun tptp.mor ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (W $$unsorted)) Bool (or (@ Phi W) (@ Psi W))) % 192.45/192.72 (define-fun tptp.mbox ((R (-> $$unsorted $$unsorted Bool)) (Phi (-> $$unsorted Bool)) (W $$unsorted)) Bool (forall ((V $$unsorted)) (or (not (R W V)) (Phi V)))) % 192.45/192.72 (define-fun tptp.mforall_prop ((Phi (-> (-> $$unsorted Bool) $$unsorted Bool)) (W $$unsorted)) Bool (forall ((P (-> $$unsorted Bool))) (Phi P W))) % 192.45/192.72 (define-fun tptp.mtrue ((BOUND_VARIABLE_2171 $$unsorted)) Bool true) % 192.45/192.72 (define-fun tptp.mfalse ((BOUND_VARIABLE_62051 $$unsorted)) Bool false) % 192.45/192.72 (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))))) % 192.45/192.72 (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))) % 192.45/192.72 (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))) % 192.45/192.72 (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)))))) % 192.45/192.72 (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))))) % 192.45/192.72 (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)))))) % 192.45/192.72 (define-fun tptp.exists_in_world ((BOUND_VARIABLE_62966 tptp.mu) (BOUND_VARIABLE_62968 $$unsorted)) Bool (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_62966) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62968) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_62966) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62968) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_62966) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62968) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_62966) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62968)))))) % 192.45/192.72 (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)))) % 192.45/192.72 (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)))))) % 192.45/192.72 (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))))) % 192.45/192.72 (define-fun tptp.mreflexive ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((S $$unsorted)) (R S S))) % 192.45/192.72 (define-fun tptp.msymmetric ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((S $$unsorted) (T $$unsorted)) (or (not (R S T)) (R T S)))) % 192.45/192.72 (define-fun tptp.mserial ((R (-> $$unsorted $$unsorted Bool))) Bool (forall ((S $$unsorted)) (not (forall ((T $$unsorted)) (not (R S T)))))) % 192.45/192.72 (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)))) % 192.45/192.72 (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)))) % 192.45/192.72 (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)))) % 192.45/192.72 (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))))))))) % 192.45/192.72 (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)))))))) % 192.45/192.72 (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)))) % 192.45/192.72 (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)))))))) % 192.45/192.72 (define-fun tptp.mvalid ((Phi (-> $$unsorted Bool))) Bool (forall ((W $$unsorted)) (Phi W))) % 192.45/192.72 (define-fun tptp.msatisfiable ((Phi (-> $$unsorted Bool))) Bool (not (forall ((W $$unsorted)) (not (Phi W))))) % 192.45/192.72 (define-fun tptp.mcountersatisfiable ((Phi (-> $$unsorted Bool))) Bool (not (forall ((W $$unsorted)) (Phi W)))) % 192.45/192.72 (define-fun tptp.minvalid ((Phi (-> $$unsorted Bool))) Bool (forall ((W $$unsorted)) (not (Phi W)))) % 192.45/192.72 (define-fun tptp.rel_s4 ((BOUND_VARIABLE_63074 $$unsorted) (BOUND_VARIABLE_63076 $$unsorted)) Bool (and (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63074) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63076))) % 192.45/192.72 (define-fun tptp.mbox_s4 ((Phi (-> $$unsorted Bool)) (W $$unsorted)) Bool (forall ((V $$unsorted)) (or (not (tptp.rel_s4 W V)) (Phi V)))) % 192.45/192.72 (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)))))) % 192.45/192.72 (define-fun tptp.vehicle ((BOUND_VARIABLE_63934 tptp.mu) (BOUND_VARIABLE_63936 $$unsorted)) Bool (ite (= (as @tptp.mu_6 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936) (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936) (and (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936))))) % 192.45/192.72 (define-fun tptp.transport ((BOUND_VARIABLE_63934 tptp.mu) (BOUND_VARIABLE_63936 $$unsorted)) Bool (ite (= (as @tptp.mu_6 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936) (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936) (and (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936))))) % 192.45/192.72 (define-fun tptp.instrumentality ((BOUND_VARIABLE_63934 tptp.mu) (BOUND_VARIABLE_63936 $$unsorted)) Bool (ite (= (as @tptp.mu_6 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936) (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936) (and (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936))))) % 192.45/192.72 (define-fun tptp.artifact ((BOUND_VARIABLE_64083 tptp.mu) (BOUND_VARIABLE_64085 $$unsorted)) Bool (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_64083) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64085) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_64083) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64085) (and (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_64083) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64085))))) % 192.45/192.72 (define-fun tptp.location ((BOUND_VARIABLE_64309 tptp.mu) (BOUND_VARIABLE_64311 $$unsorted)) Bool (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_64309) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64311) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_64309) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64311)))) % 192.45/192.72 (define-fun tptp.object ((BOUND_VARIABLE_64511 tptp.mu) (BOUND_VARIABLE_64513 $$unsorted)) Bool (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_64511) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64513) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_64511) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64513) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_64511) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64513))))) % 192.45/192.72 (define-fun tptp.new ((BOUND_VARIABLE_64921 tptp.mu) (BOUND_VARIABLE_64923 $$unsorted)) Bool (ite (= (as @tptp.mu_5 tptp.mu) BOUND_VARIABLE_64921) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64923) (and (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_64921) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64923)))) % 192.45/192.72 (define-fun tptp.eventuality ((BOUND_VARIABLE_62259 tptp.mu) (BOUND_VARIABLE_62261 $$unsorted)) Bool (and (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_62259) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62261))) % 192.45/192.72 (define-fun tptp.abstraction ((BOUND_VARIABLE_64921 tptp.mu) (BOUND_VARIABLE_64923 $$unsorted)) Bool (ite (= (as @tptp.mu_5 tptp.mu) BOUND_VARIABLE_64921) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64923) (and (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_64921) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64923)))) % 192.45/192.72 (define-fun tptp.man ((BOUND_VARIABLE_64921 tptp.mu) (BOUND_VARIABLE_64923 $$unsorted)) Bool (ite (= (as @tptp.mu_5 tptp.mu) BOUND_VARIABLE_64921) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64923) (and (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_64921) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64923)))) % 192.45/192.72 (define-fun tptp.male ((BOUND_VARIABLE_64921 tptp.mu) (BOUND_VARIABLE_64923 $$unsorted)) Bool (ite (= (as @tptp.mu_5 tptp.mu) BOUND_VARIABLE_64921) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64923) (and (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_64921) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64923)))) % 192.45/192.72 (define-fun tptp.female ((BOUND_VARIABLE_63934 tptp.mu) (BOUND_VARIABLE_63936 $$unsorted)) Bool (ite (= (as @tptp.mu_6 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936) (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936) (and (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936))))) % 192.45/192.72 (define-fun tptp.woman ((BOUND_VARIABLE_63934 tptp.mu) (BOUND_VARIABLE_63936 $$unsorted)) Bool (ite (= (as @tptp.mu_6 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936) (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936) (and (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936))))) % 192.45/192.72 (define-fun tptp.proposition ((BOUND_VARIABLE_63934 tptp.mu) (BOUND_VARIABLE_63936 $$unsorted)) Bool (ite (= (as @tptp.mu_6 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936) (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936) (and (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936))))) % 192.45/192.72 (define-fun tptp.drs ((BOUND_VARIABLE_63934 tptp.mu) (BOUND_VARIABLE_63936 $$unsorted)) Bool (ite (= (as @tptp.mu_6 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936) (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936) (and (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936))))) % 192.45/192.72 (define-fun tptp.entity ((BOUND_VARIABLE_64511 tptp.mu) (BOUND_VARIABLE_64513 $$unsorted)) Bool (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_64511) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64513) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_64511) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64513) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_64511) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64513))))) % 192.45/192.72 (define-fun tptp.owner ((BOUND_VARIABLE_63934 tptp.mu) (BOUND_VARIABLE_63936 $$unsorted)) Bool (ite (= (as @tptp.mu_6 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936) (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936) (and (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936))))) % 192.45/192.72 (define-fun tptp.human ((BOUND_VARIABLE_63934 tptp.mu) (BOUND_VARIABLE_63936 $$unsorted)) Bool (ite (= (as @tptp.mu_6 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936) (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936) (and (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936))))) % 192.45/192.72 (define-fun tptp.nonhuman ((BOUND_VARIABLE_64921 tptp.mu) (BOUND_VARIABLE_64923 $$unsorted)) Bool (ite (= (as @tptp.mu_5 tptp.mu) BOUND_VARIABLE_64921) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64923) (and (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_64921) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64923)))) % 192.45/192.72 (define-fun tptp.have ((BOUND_VARIABLE_66452 tptp.mu) (BOUND_VARIABLE_66454 tptp.mu) (BOUND_VARIABLE_66456 tptp.mu) (BOUND_VARIABLE_66458 $$unsorted)) Bool (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_66452) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_66454) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458))))) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_66454) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458))))) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_66454) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458))))) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66454) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458))))))))) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_66452) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_66454) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458))))) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_66454) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458))))) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_66454) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458))))) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66454) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458))))))))) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_66452) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_66454) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458))))) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_66454) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458))))) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_66454) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458))))) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66454) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458))))))))) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66452) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_66454) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458))))) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_66454) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458))))) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_66454) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458))))) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66454) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_66456) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_66458)))))))))))))) % 192.45/192.72 (define-fun tptp.of ((BOUND_VARIABLE_65438 tptp.mu) (BOUND_VARIABLE_65440 tptp.mu) (BOUND_VARIABLE_65442 $$unsorted)) Bool (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65438) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442))))) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65438) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442))))) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_65438) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442))))) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_65438) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442)))))))))) % 192.45/192.72 (define-fun tptp.partof ((BOUND_VARIABLE_62533 tptp.mu) (BOUND_VARIABLE_62535 tptp.mu) (BOUND_VARIABLE_62537 $$unsorted)) Bool (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_62533) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_62535) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62537)) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_62533) (and (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_62535) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62537)) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_62533) (and (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_62535) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62537)) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_62533) (and (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_62535) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62537)) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_62533) (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_62535) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62537))))))) % 192.45/192.72 (define-fun tptp.in ((BOUND_VARIABLE_65438 tptp.mu) (BOUND_VARIABLE_65440 tptp.mu) (BOUND_VARIABLE_65442 $$unsorted)) Bool (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65438) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442))))) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65438) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442))))) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_65438) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442))))) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_65438) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442)))))))))) % 192.45/192.72 (define-fun tptp.down ((BOUND_VARIABLE_65438 tptp.mu) (BOUND_VARIABLE_65440 tptp.mu) (BOUND_VARIABLE_65442 $$unsorted)) Bool (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65438) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442))))) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65438) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442))))) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_65438) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442))))) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_65438) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442)))))))))) % 192.45/192.72 (define-fun tptp.barrel ((BOUND_VARIABLE_65438 tptp.mu) (BOUND_VARIABLE_65440 tptp.mu) (BOUND_VARIABLE_65442 $$unsorted)) Bool (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65438) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442))))) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65438) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442))))) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_65438) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442))))) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_65438) (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_65440) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_65442)))))))))) % 192.45/192.72 (define-fun tptp.old ((BOUND_VARIABLE_62966 tptp.mu) (BOUND_VARIABLE_62968 $$unsorted)) Bool (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_62966) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62968) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_62966) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62968) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_62966) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62968) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_62966) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62968)))))) % 192.45/192.72 (define-fun tptp.dirty ((BOUND_VARIABLE_62966 tptp.mu) (BOUND_VARIABLE_62968 $$unsorted)) Bool (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_62966) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62968) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_62966) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62968) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_62966) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62968) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_62966) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62968)))))) % 192.45/192.72 (define-fun tptp.white ((BOUND_VARIABLE_62966 tptp.mu) (BOUND_VARIABLE_62968 $$unsorted)) Bool (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_62966) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62968) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_62966) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62968) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_62966) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62968) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_62966) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62968)))))) % 192.45/192.72 (define-fun tptp.car ((BOUND_VARIABLE_63934 tptp.mu) (BOUND_VARIABLE_63936 $$unsorted)) Bool (ite (= (as @tptp.mu_6 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936) (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936) (and (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936))))) % 192.45/192.72 (define-fun tptp.chevy ((BOUND_VARIABLE_63934 tptp.mu) (BOUND_VARIABLE_63936 $$unsorted)) Bool (ite (= (as @tptp.mu_6 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936) (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936) (and (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_63934) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_63936))))) % 192.45/192.72 (define-fun tptp.lonely ((BOUND_VARIABLE_62966 tptp.mu) (BOUND_VARIABLE_62968 $$unsorted)) Bool (ite (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_62966) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62968) (ite (= (as @tptp.mu_2 tptp.mu) BOUND_VARIABLE_62966) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62968) (ite (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_62966) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62968) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_62966) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62968)))))) % 192.45/192.72 (define-fun tptp.way ((BOUND_VARIABLE_62365 tptp.mu) (BOUND_VARIABLE_62367 $$unsorted)) Bool (and (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_62365) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62367))) % 192.45/192.72 (define-fun tptp.street ((BOUND_VARIABLE_62365 tptp.mu) (BOUND_VARIABLE_62367 $$unsorted)) Bool (and (= (as @tptp.mu_3 tptp.mu) BOUND_VARIABLE_62365) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62367))) % 192.45/192.72 (define-fun tptp.event ((BOUND_VARIABLE_62259 tptp.mu) (BOUND_VARIABLE_62261 $$unsorted)) Bool (and (= (as @tptp.mu_1 tptp.mu) BOUND_VARIABLE_62259) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_62261))) % 192.45/192.72 (define-fun tptp.city ((BOUND_VARIABLE_64309 tptp.mu) (BOUND_VARIABLE_64311 $$unsorted)) Bool (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_64309) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64311) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_64309) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64311)))) % 192.45/192.73 (define-fun tptp.hollywood ((BOUND_VARIABLE_64309 tptp.mu) (BOUND_VARIABLE_64311 $$unsorted)) Bool (ite (= (as @tptp.mu_4 tptp.mu) BOUND_VARIABLE_64309) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64311) (and (= (as @tptp.mu_0 tptp.mu) BOUND_VARIABLE_64309) (= (as @$$unsorted_0 $$unsorted) BOUND_VARIABLE_64311)))) % 192.45/192.73 ) % 192.45/192.73 % SZS output end Model % 192.45/192.73 % cvc5 exiting %------------------------------------------------------------------------------