%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : SCT149+1 : TPTP v9.2.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n002.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:46:22 AM UTC 2026 % Result : Theorem 0.54s 0.93s % Output : Proof 0.54s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SCT149+1 : TPTP v9.2.1. Released v5.2.0. % 0.00/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.17/0.34 % Computer : n002.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 14:31:18 EDT 2026 % 0.17/0.34 % CPUTime : % 0.41/0.68 %----Proving TF0_NAR, FOF, or CNF % 0.54/0.93 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.54/0.93 % SZS status Theorem % 0.54/0.93 % SZS output start Proof % 0.54/0.93 ( % 0.54/0.93 (declare-sort $$unsorted 0) % 0.54/0.93 (declare-const tptp.c_Wellfounded_Omin__ext (-> $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_FunDef_Omin__strict $$unsorted) % 0.54/0.93 (declare-const tptp.c_FunDef_Omin__weak $$unsorted) % 0.54/0.93 (declare-const tptp.c_FunDef_Opair__leq $$unsorted) % 0.54/0.93 (declare-const tptp.c_FunDef_Opair__less $$unsorted) % 0.54/0.93 (declare-const tptp.class_Orderings_Oord (-> $$unsorted Bool)) % 0.54/0.93 (declare-const tptp.class_Orderings_Opreorder (-> $$unsorted Bool)) % 0.54/0.93 (declare-const tptp.c_Relation_Oantisym (-> $$unsorted $$unsorted Bool)) % 0.54/0.93 (declare-const tptp.c_FunDef_Oreduction__pair (-> $$unsorted $$unsorted Bool)) % 0.54/0.93 (declare-const tptp.c_Wellfounded_Omlex__prod (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Orderings_Oord__class_Oless (-> $$unsorted $$unsorted $$unsorted Bool)) % 0.54/0.93 (declare-const tptp.tc_Nat_Onat $$unsorted) % 0.54/0.93 (declare-const tptp.c_Fun_Othe__inv__into (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_fconj $$unsorted) % 0.54/0.93 (declare-const tptp.c_fFalse $$unsorted) % 0.54/0.93 (declare-const tptp.c_Wellfounded_OwfP (-> $$unsorted $$unsorted Bool)) % 0.54/0.93 (declare-const tptp.c_HOL_OThe (-> $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Wellfounded_Omeasure (-> $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Transitive__Closure_Otranclp (-> $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_FunDef_Omax__strict $$unsorted) % 0.54/0.93 (declare-const tptp.c_Wellfounded_Owf (-> $$unsorted $$unsorted Bool)) % 0.54/0.93 (declare-const tptp.c_Set_Oinsert (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Relation_OId (-> $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Relation_Orefl__on (-> $$unsorted $$unsorted $$unsorted Bool)) % 0.54/0.93 (declare-const tptp.c_Relation_Oinv__image (-> $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Wellfounded_Olex__prod (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_COMBK (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.tc_fun (-> $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_fNot $$unsorted) % 0.54/0.93 (declare-const tptp.c_Recdef_Owfrec__rel (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.tc_Arrow__Order__Mirabelle_Oindi $$unsorted) % 0.54/0.93 (declare-const tptp.c_Product__Type_Ocurry (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.class_Lattices_Osemilattice__inf (-> $$unsorted Bool)) % 0.54/0.93 (declare-const tptp.v_c____ $$unsorted) % 0.54/0.93 (declare-const tptp.c_COMBI (-> $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Arrow__Order__Mirabelle_Omktop (-> $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Recdef_Ocut (-> $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Relation_OId__on (-> $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Transitive__Closure_Ortranclp (-> $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Arrow__Order__Mirabelle_OProf $$unsorted) % 0.54/0.93 (declare-const tptp.c_FuncSet_OPi (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Orderings_Oord__class_Oless__eq (-> $$unsorted $$unsorted $$unsorted Bool)) % 0.54/0.93 (declare-const tptp.c_Arrow__Order__Mirabelle_Omkbot (-> $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Nitpick_Owf__wfrec (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.hAPP (-> $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.v_F $$unsorted) % 0.54/0.93 (declare-const tptp.c_member (-> $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Product__Type_Oprod_Oprod__case (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Wellfounded_Oacc (-> $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Arrow__Order__Mirabelle_OIIA (-> $$unsorted Bool)) % 0.54/0.93 (declare-const tptp.c_HOL_Oundefined (-> $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Arrow__Order__Mirabelle_Obelow $$unsorted) % 0.54/0.93 (declare-const tptp.c_FunDef_Orp__inv__image (-> $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Arrow__Order__Mirabelle_Ounanimity (-> $$unsorted Bool)) % 0.54/0.93 (declare-const tptp.c_Wellfounded_Opred__nat $$unsorted) % 0.54/0.93 (declare-const tptp.c_COMBB (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Relation_Orel__comp (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.class_Orderings_Olinorder (-> $$unsorted Bool)) % 0.54/0.93 (declare-const tptp.v_P_H____ $$unsorted) % 0.54/0.93 (declare-const tptp.c_Predicate_ODomainP (-> $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 0.54/0.93 (declare-const tptp.v_b____ $$unsorted) % 0.54/0.93 (declare-const tptp.c_Nitpick_Owfrec_H (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_FunDef_Oin__rel (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Relation_Oirrefl (-> $$unsorted $$unsorted Bool)) % 0.54/0.93 (declare-const tptp.v_a____ $$unsorted) % 0.54/0.93 (declare-const tptp.c_Product__Type_Oprod_Oprod__rec (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.tc_Arrow__Order__Mirabelle_Oalt $$unsorted) % 0.54/0.93 (declare-const tptp.c_Product__Type_OPair (-> $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Recdef_Owfrec (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.class_Lattices_Olattice (-> $$unsorted Bool)) % 0.54/0.93 (declare-const tptp.tc_prod (-> $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Nitpick_Orefl_H (-> $$unsorted $$unsorted Bool)) % 0.54/0.93 (declare-const tptp.hBOOL (-> $$unsorted Bool)) % 0.54/0.93 (declare-const tptp.c_Wellfounded_Oacyclic (-> $$unsorted $$unsorted Bool)) % 0.54/0.93 (declare-const tptp.tc_HOL_Obool $$unsorted) % 0.54/0.93 (declare-const tptp.c_Relation_ORange (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Nitpick_Owf__wfrec_H (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Arrow__Order__Mirabelle_Odictator (-> $$unsorted $$unsorted Bool)) % 0.54/0.93 (declare-const tptp.c_Recdef_Osame__fst (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.v_P____ $$unsorted) % 0.54/0.93 (declare-const tptp.c_fequal $$unsorted) % 0.54/0.93 (declare-const tptp.c_Arrow__Order__Mirabelle_Oabove (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_COMBC (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Wellfounded_Oaccp (-> $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Transitive__Closure_Ortrancl (-> $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_COMBS (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Fun_Ofun__upd (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Recdef_Oadm__wf (-> $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 0.54/0.93 (declare-const tptp.c_Arrow__Order__Mirabelle_OLin $$unsorted) % 0.54/0.93 (declare-const tptp.c_FuncSet_Oextensional (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Relation_Osingle__valued (-> $$unsorted $$unsorted $$unsorted Bool)) % 0.54/0.93 (declare-const tptp.c_Fun_Ooverride__on (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Lattices_Osemilattice__inf__class_Oinf (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Wellfounded_Oless__than $$unsorted) % 0.54/0.93 (declare-const tptp.c_Relation_ODomain (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_FuncSet_Orestrict (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Product__Type_Ointernal__split (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_FuncSet_Oextensional__funcset (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_FunDef_Omax__weak $$unsorted) % 0.54/0.93 (declare-const tptp.c_Transitive__Closure_Otrancl (-> $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Predicate_ORangeP (-> $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 0.54/0.93 (declare-const tptp.class_Orderings_Oorder (-> $$unsorted Bool)) % 0.54/0.93 (declare-const tptp.c_FuncSet_Ocompose (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.54/0.93 (declare-const tptp.c_Relation_Ototal__on (-> $$unsorted $$unsorted $$unsorted Bool)) % 0.54/0.93 (define @t1 () (@var "V_g_2" $$unsorted)) % 0.54/0.93 (define @t2 () (@var "V_f_2" $$unsorted)) % 0.54/0.93 (define @t3 () (= @t2 @t1)) % 0.54/0.93 (define @t4 () (@var "B_x" $$unsorted)) % 0.54/0.93 (define @t5 () (tptp.hAPP @t1 @t4)) % 0.54/0.93 (define @t6 () (tptp.hAPP @t2 @t4)) % 0.54/0.93 (define @t7 () (= @t6 @t5)) % 0.54/0.93 (define @t8 () (@list @t4)) % 0.54/0.93 (define @t9 () (@var "B_i" $$unsorted)) % 0.54/0.93 (define @t10 () (tptp.c_Product__Type_OPair tptp.tc_Arrow__Order__Mirabelle_Oalt tptp.tc_Arrow__Order__Mirabelle_Oalt)) % 0.54/0.93 (define @t11 () (tptp.hAPP @t10 tptp.v_b____)) % 0.54/0.93 (define @t12 () (tptp.tc_prod tptp.tc_Arrow__Order__Mirabelle_Oalt tptp.tc_Arrow__Order__Mirabelle_Oalt)) % 0.54/0.93 (define @t13 () (tptp.c_member @t12)) % 0.54/0.93 (define @t14 () (tptp.hAPP @t13 (tptp.hAPP @t11 tptp.v_a____))) % 0.54/0.93 (define @t15 () (tptp.hBOOL (tptp.hAPP @t14 (tptp.hAPP tptp.v_P_H____ @t9)))) % 0.54/0.93 (define @t16 () (tptp.hAPP tptp.v_P____ @t9)) % 0.54/0.93 (define @t17 () (tptp.hAPP @t10 tptp.v_a____)) % 0.54/0.93 (define @t18 () (tptp.hAPP @t13 (tptp.hAPP @t17 tptp.v_b____))) % 0.54/0.93 (define @t19 () (tptp.hBOOL (tptp.hAPP @t18 @t16))) % 0.54/0.93 (define @t20 () (@list @t9)) % 0.54/0.93 (define @t21 () (@var "V_B_2" $$unsorted)) % 0.54/0.93 (define @t22 () (@var "V_ca_2" $$unsorted)) % 0.54/0.93 (define @t23 () (@var "T_a" $$unsorted)) % 0.54/0.93 (define @t24 () (tptp.c_member @t23)) % 0.54/0.93 (define @t25 () (tptp.hAPP @t24 @t22)) % 0.54/0.93 (define @t26 () (tptp.hBOOL (tptp.hAPP @t25 @t21))) % 0.54/0.93 (define @t27 () (@var "V_A_2" $$unsorted)) % 0.54/0.93 (define @t28 () (tptp.hBOOL (tptp.hAPP @t25 @t27))) % 0.54/0.93 (define @t29 () (=> @t28 (not @t26))) % 0.54/0.93 (define @t30 () (= @t27 @t21)) % 0.54/0.93 (define @t31 () (@var "V_L_2" $$unsorted)) % 0.54/0.93 (define @t32 () (@var "V_y_2" $$unsorted)) % 0.54/0.93 (define @t33 () (@var "V_x_2" $$unsorted)) % 0.54/0.93 (define @t34 () (tptp.hAPP @t10 @t33)) % 0.54/0.93 (define @t35 () (tptp.hAPP @t13 (tptp.hAPP @t34 @t32))) % 0.54/0.93 (define @t36 () (tptp.hBOOL (tptp.hAPP @t35 @t31))) % 0.54/0.93 (define @t37 () (@var "V_z_2" $$unsorted)) % 0.54/0.93 (define @t38 () (= @t33 @t37)) % 0.54/0.93 (define @t39 () (not @t38)) % 0.54/0.93 (define @t40 () (= @t33 @t32)) % 0.54/0.93 (define @t41 () (not @t40)) % 0.54/0.93 (define @t42 () (= @t32 @t37)) % 0.54/0.93 (define @t43 () (not @t42)) % 0.54/0.93 (define @t44 () (@list @t37 @t31 @t32 @t33)) % 0.54/0.93 (define @t45 () (tptp.hAPP (tptp.hAPP (tptp.hAPP tptp.c_Arrow__Order__Mirabelle_Obelow @t16) tptp.v_c____) tptp.v_b____)) % 0.54/0.93 (define @t46 () (tptp.hAPP (tptp.hAPP (tptp.hAPP tptp.c_Arrow__Order__Mirabelle_Obelow @t45) tptp.v_b____) tptp.v_a____)) % 0.54/0.93 (define @t47 () (tptp.hBOOL (tptp.hAPP @t14 (tptp.hAPP (tptp.hAPP (tptp.hAPP tptp.c_Arrow__Order__Mirabelle_Obelow @t46) tptp.v_a____) tptp.v_c____)))) % 0.54/0.93 (define @t48 () (tptp.hAPP @t13 (tptp.hAPP @t17 tptp.v_c____))) % 0.54/0.93 (define @t49 () (tptp.hBOOL (tptp.hAPP @t48 @t45))) % 0.54/0.93 (define @t50 () (tptp.hAPP @t13 (tptp.hAPP @t11 tptp.v_c____))) % 0.54/0.93 (define @t51 () (tptp.hBOOL (tptp.hAPP @t50 @t46))) % 0.54/0.93 (define @t52 () (@var "V_R_2" $$unsorted)) % 0.54/0.93 (define @t53 () (@var "T_b" $$unsorted)) % 0.54/0.93 (define @t54 () (tptp.c_Product__Type_OPair @t23 @t53)) % 0.54/0.93 (define @t55 () (tptp.hAPP @t54 @t33)) % 0.54/0.93 (define @t56 () (tptp.hAPP @t55 @t32)) % 0.54/0.93 (define @t57 () (tptp.tc_prod @t23 @t53)) % 0.54/0.93 (define @t58 () (tptp.c_member @t57)) % 0.54/0.93 (define @t59 () (tptp.hAPP @t58 @t56)) % 0.54/0.93 (define @t60 () (@var "V_Pa_2" $$unsorted)) % 0.54/0.93 (define @t61 () (tptp.c_Recdef_Osame__fst @t23 @t53 @t60 @t52)) % 0.54/0.93 (define @t62 () (@var "V_y_H_2" $$unsorted)) % 0.54/0.93 (define @t63 () (tptp.c_Product__Type_OPair @t57 @t57)) % 0.54/0.93 (define @t64 () (tptp.c_member (tptp.tc_prod @t57 @t57))) % 0.54/0.93 (define @t65 () (tptp.c_Product__Type_OPair @t53 @t53)) % 0.54/0.93 (define @t66 () (tptp.tc_prod @t53 @t53)) % 0.54/0.93 (define @t67 () (tptp.c_member @t66)) % 0.54/0.93 (define @t68 () (tptp.hAPP @t60 @t33)) % 0.54/0.93 (define @t69 () (tptp.hBOOL @t68)) % 0.54/0.93 (define @t70 () (tptp.tc_fun @t12 tptp.tc_HOL_Obool)) % 0.54/0.93 (define @t71 () (tptp.tc_fun tptp.tc_Arrow__Order__Mirabelle_Oindi @t70)) % 0.54/0.93 (define @t72 () (tptp.c_member @t71)) % 0.54/0.93 (define @t73 () (tptp.hBOOL (tptp.hAPP @t14 (tptp.hAPP tptp.v_F tptp.v_P_H____)))) % 0.54/0.93 (define @t74 () (tptp.tc_fun tptp.tc_Arrow__Order__Mirabelle_Oalt @t70)) % 0.54/0.93 (define @t75 () (tptp.hAPP (tptp.c_COMBB @t70 (tptp.tc_fun tptp.tc_Arrow__Order__Mirabelle_Oalt @t74) tptp.tc_Arrow__Order__Mirabelle_Oindi) tptp.c_Arrow__Order__Mirabelle_Obelow)) % 0.54/0.93 (define @t76 () (tptp.c_COMBC tptp.tc_Arrow__Order__Mirabelle_Oindi tptp.tc_Arrow__Order__Mirabelle_Oalt @t74)) % 0.54/0.94 (define @t77 () (tptp.c_COMBC tptp.tc_Arrow__Order__Mirabelle_Oindi tptp.tc_Arrow__Order__Mirabelle_Oalt @t70)) % 0.54/0.94 (define @t78 () (tptp.hAPP (tptp.hAPP @t77 (tptp.hAPP (tptp.hAPP @t76 (tptp.hAPP @t75 tptp.v_P____)) tptp.v_c____)) tptp.v_b____)) % 0.54/0.94 (define @t79 () (tptp.hAPP (tptp.hAPP @t77 (tptp.hAPP (tptp.hAPP @t76 (tptp.hAPP @t75 @t78)) tptp.v_b____)) tptp.v_a____)) % 0.54/0.94 (define @t80 () (tptp.hAPP (tptp.hAPP @t77 (tptp.hAPP (tptp.hAPP @t76 (tptp.hAPP @t75 @t79)) tptp.v_a____)) tptp.v_c____)) % 0.54/0.94 (define @t81 () (tptp.hBOOL (tptp.hAPP @t14 (tptp.hAPP tptp.v_F @t80)))) % 0.54/0.94 (define @t82 () (tptp.hBOOL (tptp.hAPP @t50 (tptp.hAPP tptp.v_F @t79)))) % 0.54/0.94 (define @t83 () (tptp.hBOOL (tptp.hAPP @t48 (tptp.hAPP tptp.v_F @t78)))) % 0.54/0.94 (define @t84 () (tptp.hBOOL (tptp.hAPP @t18 (tptp.hAPP tptp.v_F tptp.v_P____)))) % 0.54/0.94 (define @t85 () (@var "V_aa_2" $$unsorted)) % 0.54/0.94 (define @t86 () (tptp.hAPP @t24 @t85)) % 0.54/0.94 (define @t87 () (tptp.hBOOL (tptp.hAPP @t86 @t27))) % 0.54/0.94 (define @t88 () (@var "V_ba_2" $$unsorted)) % 0.54/0.94 (define @t89 () (tptp.hAPP @t24 @t88)) % 0.54/0.94 (define @t90 () (= @t85 @t88)) % 0.54/0.94 (define @t91 () (@list @t27 @t23 @t88 @t85)) % 0.54/0.94 (define @t92 () (tptp.hAPP @t24 @t32)) % 0.54/0.94 (define @t93 () (tptp.hBOOL (tptp.hAPP @t92 @t27))) % 0.54/0.94 (define @t94 () (tptp.hAPP @t24 @t33)) % 0.54/0.94 (define @t95 () (tptp.hBOOL (tptp.hAPP @t94 @t27))) % 0.54/0.94 (define @t96 () (tptp.hBOOL (tptp.hAPP @t94 @t21))) % 0.54/0.94 (define @t97 () (tptp.hAPP @t27 @t33)) % 0.54/0.94 (define @t98 () (tptp.hBOOL @t97)) % 0.54/0.94 (define @t99 () (@list @t27 @t33 @t23)) % 0.54/0.94 (define @t100 () (@var "V_P_Ha_2" $$unsorted)) % 0.54/0.94 (define @t101 () (@var "V_b_H_2" $$unsorted)) % 0.54/0.94 (define @t102 () (@var "V_a_H_2" $$unsorted)) % 0.54/0.94 (define @t103 () (tptp.hAPP @t13 (tptp.hAPP (tptp.hAPP @t10 @t102) @t101))) % 0.54/0.94 (define @t104 () (tptp.hBOOL (tptp.hAPP @t103 (tptp.hAPP tptp.v_F @t100)))) % 0.54/0.94 (define @t105 () (tptp.hAPP @t10 @t85)) % 0.54/0.94 (define @t106 () (tptp.hAPP @t13 (tptp.hAPP @t105 @t88))) % 0.54/0.94 (define @t107 () (tptp.hBOOL (tptp.hAPP @t106 (tptp.hAPP tptp.v_F @t60)))) % 0.54/0.94 (define @t108 () (forall @t20 (= (tptp.hBOOL (tptp.hAPP @t106 (tptp.hAPP @t60 @t9))) (tptp.hBOOL (tptp.hAPP @t103 (tptp.hAPP @t100 @t9)))))) % 0.54/0.94 (define @t109 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t72 @t100) tptp.c_Arrow__Order__Mirabelle_OProf))) % 0.54/0.94 (define @t110 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t72 @t60) tptp.c_Arrow__Order__Mirabelle_OProf))) % 0.54/0.94 (define @t111 () (not (= @t88 @t102))) % 0.54/0.94 (define @t112 () (not (= @t85 @t101))) % 0.54/0.94 (define @t113 () (not (= @t102 @t101))) % 0.54/0.94 (define @t114 () (not @t90)) % 0.54/0.94 (define @t115 () (@list @t100 @t60 @t101 @t102 @t88 @t85)) % 0.54/0.94 (define @t116 () (@var "V_S_2" $$unsorted)) % 0.54/0.94 (define @t117 () (= @t52 @t116)) % 0.54/0.94 (define @t118 () (tptp.tc_fun @t57 tptp.tc_HOL_Obool)) % 0.54/0.94 (define @t119 () (tptp.tc_fun @t118 tptp.tc_HOL_Obool)) % 0.54/0.94 (define @t120 () (tptp.tc_fun @t53 @t119)) % 0.54/0.94 (define @t121 () (tptp.tc_fun @t53 tptp.tc_HOL_Obool)) % 0.54/0.94 (define @t122 () (tptp.hAPP (tptp.c_COMBC @t23 @t118 @t121) (tptp.hAPP (tptp.hAPP (tptp.c_COMBB @t120 (tptp.tc_fun @t118 @t121) @t23) (tptp.c_COMBC @t53 @t118 tptp.tc_HOL_Obool)) (tptp.hAPP (tptp.hAPP (tptp.c_COMBB (tptp.tc_fun @t53 @t57) @t120 @t23) (tptp.hAPP (tptp.c_COMBB @t57 @t119 @t53) @t58)) @t54)))) % 0.54/0.94 (define @t123 () (tptp.hAPP @t122 @t116)) % 0.54/0.94 (define @t124 () (tptp.hAPP @t122 @t52)) % 0.54/0.94 (define @t125 () (@list @t116 @t52 @t53 @t23)) % 0.54/0.94 (define @t126 () (tptp.c_FuncSet_OPi @t71 @t70 tptp.c_Arrow__Order__Mirabelle_OProf (tptp.c_COMBK (tptp.tc_fun @t70 tptp.tc_HOL_Obool) @t71 tptp.c_Arrow__Order__Mirabelle_OLin))) % 0.54/0.94 (define @t127 () (tptp.c_member (tptp.tc_fun @t71 @t70))) % 0.54/0.94 (define @t128 () (@var "B_xa" $$unsorted)) % 0.54/0.94 (define @t129 () (@var "V_Fa_2" $$unsorted)) % 0.54/0.94 (define @t130 () (@var "B_b" $$unsorted)) % 0.54/0.94 (define @t131 () (@var "B_a" $$unsorted)) % 0.54/0.94 (define @t132 () (tptp.hAPP @t13 (tptp.hAPP (tptp.hAPP @t10 @t131) @t130))) % 0.54/0.94 (define @t133 () (tptp.hAPP @t129 @t4)) % 0.54/0.94 (define @t134 () (tptp.hBOOL (tptp.hAPP @t132 @t133))) % 0.54/0.94 (define @t135 () (tptp.hBOOL (tptp.hAPP @t132 (tptp.hAPP @t4 @t9)))) % 0.54/0.94 (define @t136 () (@list @t131 @t130)) % 0.54/0.94 (define @t137 () (@list @t128)) % 0.54/0.94 (define @t138 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t72 @t4) tptp.c_Arrow__Order__Mirabelle_OProf))) % 0.54/0.94 (define @t139 () (@list @t129)) % 0.54/0.94 (define @t140 () (@var "V_s_2" $$unsorted)) % 0.54/0.94 (define @t141 () (= @t85 @t102)) % 0.54/0.94 (define @t142 () (@var "V_r_2" $$unsorted)) % 0.54/0.94 (define @t143 () (tptp.c_Product__Type_OPair @t23 @t23)) % 0.54/0.94 (define @t144 () (tptp.hAPP @t143 @t85)) % 0.54/0.94 (define @t145 () (tptp.tc_prod @t23 @t23)) % 0.54/0.94 (define @t146 () (tptp.c_member @t145)) % 0.54/0.94 (define @t147 () (tptp.hAPP (tptp.hAPP @t54 @t102) @t101)) % 0.54/0.94 (define @t148 () (tptp.hAPP @t54 @t85)) % 0.54/0.94 (define @t149 () (tptp.hAPP @t148 @t88)) % 0.54/0.94 (define @t150 () (@var "V_i_2" $$unsorted)) % 0.54/0.94 (define @t151 () (tptp.hAPP @t4 @t150)) % 0.54/0.94 (define @t152 () (tptp.c_Arrow__Order__Mirabelle_Odictator @t129 @t150)) % 0.54/0.94 (define @t153 () (@list @t150 @t129)) % 0.54/0.94 (define @t154 () (= @t33 @t85)) % 0.54/0.94 (define @t155 () (not @t154)) % 0.54/0.94 (define @t156 () (tptp.hAPP @t10 @t88)) % 0.54/0.94 (define @t157 () (= @t32 @t88)) % 0.54/0.94 (define @t158 () (= @t32 @t85)) % 0.54/0.94 (define @t159 () (tptp.hAPP tptp.c_Arrow__Order__Mirabelle_Obelow @t31)) % 0.54/0.94 (define @t160 () (tptp.c_member @t70)) % 0.54/0.94 (define @t161 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t160 @t31) tptp.c_Arrow__Order__Mirabelle_OLin))) % 0.54/0.94 (define @t162 () (@list @t32 @t33 @t31 @t88 @t85)) % 0.54/0.94 (define @t163 () (tptp.tc_fun @t23 tptp.tc_HOL_Obool)) % 0.54/0.94 (define @t164 () (tptp.hAPP (tptp.c_COMBC @t23 @t163 tptp.tc_HOL_Obool) @t24)) % 0.54/0.94 (define @t165 () (tptp.hAPP @t164 @t116)) % 0.54/0.94 (define @t166 () (tptp.hAPP @t164 @t52)) % 0.54/0.94 (define @t167 () (@list @t116 @t52 @t23)) % 0.54/0.94 (define @t168 () (@list @t31 @t32 @t33)) % 0.54/0.94 (define @t169 () (@list @t33 @t31)) % 0.54/0.94 (define @t170 () (@list @t32 @t33 @t23)) % 0.54/0.94 (define @t171 () (not @t95)) % 0.54/0.94 (define @t172 () (tptp.hAPP @t21 @t33)) % 0.54/0.94 (define @t173 () (tptp.hAPP @t2 @t33)) % 0.54/0.94 (define @t174 () (tptp.c_member @t53)) % 0.54/0.94 (define @t175 () (tptp.hAPP @t174 @t173)) % 0.54/0.94 (define @t176 () (tptp.hBOOL (tptp.hAPP @t175 @t172))) % 0.54/0.94 (define @t177 () (tptp.c_FuncSet_OPi @t23 @t53 @t27 @t21)) % 0.54/0.94 (define @t178 () (tptp.tc_fun @t23 @t53)) % 0.54/0.94 (define @t179 () (tptp.c_member @t178)) % 0.54/0.94 (define @t180 () (tptp.hAPP @t179 @t2)) % 0.54/0.94 (define @t181 () (tptp.hBOOL (tptp.hAPP @t180 @t177))) % 0.54/0.94 (define @t182 () (@list @t33 @t21 @t27 @t2 @t53 @t23)) % 0.54/0.94 (define @t183 () (= @t33 @t88)) % 0.54/0.94 (define @t184 () (tptp.c_FuncSet_OPi @t23 @t53 @t27 (tptp.c_COMBK @t121 @t23 @t21))) % 0.54/0.94 (define @t185 () (tptp.hBOOL (tptp.hAPP @t180 @t184))) % 0.54/0.94 (define @t186 () (tptp.c_COMBI @t23)) % 0.54/0.94 (define @t187 () (tptp.tc_fun @t23 @t23)) % 0.54/0.94 (define @t188 () (@list @t27 @t23)) % 0.54/0.94 (define @t189 () (tptp.hAPP @t143 @t4)) % 0.54/0.94 (define @t190 () (tptp.hAPP @t189 @t4)) % 0.54/0.94 (define @t191 () (tptp.hAPP @t146 @t190)) % 0.54/0.94 (define @t192 () (tptp.hBOOL (tptp.hAPP @t191 @t142))) % 0.54/0.94 (define @t193 () (@list @t142 @t23)) % 0.54/0.94 (define @t194 () (tptp.c_Wellfounded_Oacc @t23 @t142)) % 0.54/0.94 (define @t195 () (tptp.hAPP @t24 @t4)) % 0.54/0.94 (define @t196 () (tptp.hBOOL (tptp.hAPP @t195 @t194))) % 0.54/0.94 (define @t197 () (tptp.hBOOL (tptp.hAPP @t86 @t194))) % 0.54/0.94 (define @t198 () (@list @t142 @t85 @t23)) % 0.54/0.94 (define @t199 () (tptp.hAPP @t146 (tptp.hAPP @t144 @t88))) % 0.54/0.94 (define @t200 () (tptp.hBOOL (tptp.hAPP @t199 @t142))) % 0.54/0.94 (define @t201 () (tptp.hBOOL (tptp.hAPP @t89 @t194))) % 0.54/0.94 (define @t202 () (tptp.hBOOL (tptp.hAPP @t94 @t194))) % 0.54/0.94 (define @t203 () (tptp.tc_fun @t145 tptp.tc_HOL_Obool)) % 0.54/0.94 (define @t204 () (tptp.tc_fun @t203 tptp.tc_HOL_Obool)) % 0.54/0.94 (define @t205 () (tptp.tc_fun @t23 @t204)) % 0.54/0.94 (define @t206 () (tptp.hAPP (tptp.hAPP (tptp.c_COMBC @t23 @t203 @t163) (tptp.hAPP (tptp.hAPP (tptp.c_COMBB @t205 (tptp.tc_fun @t203 @t163) @t23) (tptp.c_COMBC @t23 @t203 tptp.tc_HOL_Obool)) (tptp.hAPP (tptp.hAPP (tptp.c_COMBB (tptp.tc_fun @t23 @t145) @t205 @t23) (tptp.hAPP (tptp.c_COMBB @t145 @t204 @t23) @t146)) @t143))) @t142)) % 0.54/0.94 (define @t207 () (@list @t33 @t142 @t23)) % 0.54/0.94 (define @t208 () (tptp.c_Wellfounded_Oacc @t23 @t52)) % 0.54/0.94 (define @t209 () (@var "B_z" $$unsorted)) % 0.54/0.94 (define @t210 () (tptp.hAPP @t143 @t209)) % 0.54/0.94 (define @t211 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t146 (tptp.hAPP @t210 @t33)) @t52))) % 0.54/0.94 (define @t212 () (@list @t209)) % 0.54/0.94 (define @t213 () (@var "B_y" $$unsorted)) % 0.54/0.94 (define @t214 () (tptp.hAPP @t24 @t213)) % 0.54/0.94 (define @t215 () (tptp.hAPP @t143 @t213)) % 0.54/0.94 (define @t216 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t146 (tptp.hAPP @t215 @t33)) @t142))) % 0.54/0.94 (define @t217 () (@list @t213)) % 0.54/0.94 (define @t218 () (tptp.hAPP @t174 @t6)) % 0.54/0.94 (define @t219 () (tptp.hBOOL (tptp.hAPP @t195 @t27))) % 0.54/0.94 (define @t220 () (forall @t8 (=> @t219 (tptp.hBOOL (tptp.hAPP @t218 (tptp.hAPP @t21 @t4)))))) % 0.54/0.94 (define @t221 () (@list @t21 @t2 @t53 @t27 @t23)) % 0.54/0.94 (define @t222 () (forall @t8 (=> @t219 (tptp.hBOOL (tptp.hAPP @t218 @t21))))) % 0.54/0.94 (define @t223 () (tptp.hAPP @t179 @t1)) % 0.54/0.94 (define @t224 () (@var "B_w" $$unsorted)) % 0.54/0.94 (define @t225 () (@var "V_C_2" $$unsorted)) % 0.54/0.94 (define @t226 () (@var "T_c" $$unsorted)) % 0.54/0.94 (define @t227 () (tptp.tc_fun @t226 tptp.tc_HOL_Obool)) % 0.54/0.94 (define @t228 () (tptp.c_FuncSet_Ocompose @t23 @t53 @t226 @t27 @t1 @t2)) % 0.54/0.94 (define @t229 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP (tptp.c_member (tptp.tc_fun @t53 @t226)) @t1) (tptp.c_FuncSet_OPi @t53 @t226 @t21 (tptp.c_COMBK @t227 @t53 @t225))))) % 0.54/0.94 (define @t230 () (@var "V_h_2" $$unsorted)) % 0.54/0.94 (define @t231 () (@var "T_d" $$unsorted)) % 0.54/0.94 (define @t232 () (@var "V_D_2" $$unsorted)) % 0.54/0.94 (define @t233 () (tptp.c_Wellfounded_Oaccp @t23 @t142)) % 0.54/0.94 (define @t234 () (tptp.hBOOL (tptp.hAPP @t233 @t85))) % 0.54/0.94 (define @t235 () (@list @t85 @t142 @t23)) % 0.54/0.94 (define @t236 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t142 @t85) @t88))) % 0.54/0.94 (define @t237 () (tptp.hBOOL (tptp.hAPP @t233 @t88))) % 0.54/0.94 (define @t238 () (@list @t85 @t88 @t142 @t23)) % 0.54/0.94 (define @t239 () (tptp.c_FuncSet_Ocompose @t23 @t226 @t53 @t27 @t1 @t2)) % 0.54/0.94 (define @t240 () (tptp.c_FuncSet_Oextensional @t23 @t53 @t27)) % 0.54/0.94 (define @t241 () (tptp.c_Transitive__Closure_Ortrancl @t23 @t142)) % 0.54/0.94 (define @t242 () (tptp.hAPP @t143 @t88)) % 0.54/0.94 (define @t243 () (tptp.hAPP @t146 (tptp.hAPP @t242 @t85))) % 0.54/0.94 (define @t244 () (tptp.hBOOL (tptp.hAPP @t243 @t241))) % 0.54/0.94 (define @t245 () (@var "B_g" $$unsorted)) % 0.54/0.94 (define @t246 () (tptp.hAPP @t245 @t209)) % 0.54/0.94 (define @t247 () (tptp.c_Recdef_Owfrec__rel @t23 @t53 @t52 @t129 @t209)) % 0.54/0.94 (define @t248 () (@var "V_a1_2" $$unsorted)) % 0.54/0.94 (define @t249 () (forall @t212 (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t146 (tptp.hAPP @t210 @t248)) @t52)) (tptp.hBOOL (tptp.hAPP @t247 @t246))))) % 0.54/0.94 (define @t250 () (tptp.hAPP @t129 @t245)) % 0.54/0.94 (define @t251 () (tptp.hAPP @t250 @t248)) % 0.54/0.94 (define @t252 () (@var "V_a2_2" $$unsorted)) % 0.54/0.94 (define @t253 () (tptp.hAPP (tptp.hAPP @t129 @t252) @t248)) % 0.54/0.94 (define @t254 () (@list @t245)) % 0.54/0.94 (define @t255 () (tptp.c_Recdef_Owfrec__rel @t23 @t53 @t52 @t129 @t248)) % 0.54/0.94 (define @t256 () (@list @t252 @t248 @t129 @t52 @t53 @t23)) % 0.54/0.94 (define @t257 () (@var "B_f" $$unsorted)) % 0.54/0.94 (define @t258 () (@var "B_R" $$unsorted)) % 0.54/0.94 (define @t259 () (tptp.c_Recdef_Ocut @t23 @t53)) % 0.54/0.94 (define @t260 () (tptp.hAPP @t143 @t33)) % 0.54/0.94 (define @t261 () (tptp.hAPP @t146 (tptp.hAPP @t260 @t85))) % 0.54/0.94 (define @t262 () (tptp.hAPP (tptp.hAPP @t259 @t2) @t142)) % 0.54/0.94 (define @t263 () (tptp.hAPP @t262 @t33)) % 0.54/0.94 (define @t264 () (tptp.hAPP @t262 @t85)) % 0.54/0.94 (define @t265 () (tptp.hBOOL (tptp.hAPP @t261 @t142))) % 0.54/0.94 (define @t266 () (@var "B_L" $$unsorted)) % 0.54/0.94 (define @t267 () (tptp.hAPP (tptp.hAPP @t54 @t131) @t130)) % 0.54/0.94 (define @t268 () (@var "B_x1" $$unsorted)) % 0.54/0.94 (define @t269 () (@list @t268)) % 0.54/0.94 (define @t270 () (@var "V_b_H" $$unsorted)) % 0.54/0.94 (define @t271 () (@var "V_b" $$unsorted)) % 0.54/0.94 (define @t272 () (@var "V_a_H" $$unsorted)) % 0.54/0.94 (define @t273 () (@var "V_a" $$unsorted)) % 0.54/0.94 (define @t274 () (tptp.hAPP @t146 (tptp.hAPP @t144 @t85))) % 0.54/0.94 (define @t275 () (@var "V_p_2" $$unsorted)) % 0.54/0.94 (define @t276 () (tptp.hAPP @t146 @t275)) % 0.54/0.94 (define @t277 () (tptp.hBOOL (tptp.hAPP @t276 @t142))) % 0.54/0.94 (define @t278 () (@list @t142 @t275 @t23)) % 0.54/0.94 (define @t279 () (tptp.hAPP @t146 (tptp.hAPP @t144 @t22))) % 0.54/0.94 (define @t280 () (tptp.hBOOL (tptp.hAPP @t279 @t241))) % 0.54/0.94 (define @t281 () (tptp.hAPP @t146 (tptp.hAPP @t242 @t22))) % 0.54/0.94 (define @t282 () (tptp.hBOOL (tptp.hAPP @t281 @t241))) % 0.54/0.94 (define @t283 () (=> @t282 @t280)) % 0.54/0.94 (define @t284 () (tptp.hBOOL (tptp.hAPP @t199 @t241))) % 0.54/0.94 (define @t285 () (@list @t22 @t142 @t88 @t85 @t23)) % 0.54/0.94 (define @t286 () (tptp.hBOOL (tptp.hAPP @t281 @t142))) % 0.54/0.94 (define @t287 () (@var "V_f1_2" $$unsorted)) % 0.54/0.94 (define @t288 () (tptp.c_Product__Type_OPair @t53 @t226)) % 0.54/0.94 (define @t289 () (tptp.hAPP (tptp.hAPP @t288 @t85) @t88)) % 0.54/0.94 (define @t290 () (tptp.c_COMBI @t53)) % 0.54/0.94 (define @t291 () (tptp.hBOOL (tptp.hAPP @t180 @t240))) % 0.54/0.94 (define @t292 () (@list @t21 @t27 @t2 @t53 @t23)) % 0.54/0.94 (define @t293 () (tptp.hBOOL (tptp.hAPP @t223 @t240))) % 0.54/0.94 (define @t294 () (tptp.c_FuncSet_Orestrict @t23 @t53 @t2 @t27)) % 0.54/0.94 (define @t295 () (@list @t27 @t2 @t53 @t23)) % 0.54/0.94 (define @t296 () (tptp.hAPP @t179 @t294)) % 0.54/0.94 (define @t297 () (tptp.tc_fun @t23 @t178)) % 0.54/0.94 (define @t298 () (tptp.hAPP (tptp.hAPP (tptp.c_COMBC @t178 @t187 @t178) (tptp.hAPP (tptp.hAPP (tptp.c_COMBB @t297 (tptp.tc_fun @t187 @t178) @t178) (tptp.c_COMBS @t23 @t23 @t53)) (tptp.hAPP (tptp.hAPP (tptp.c_COMBB @t297 @t297 @t178) (tptp.hAPP (tptp.c_COMBB @t178 @t178 @t23) @t129)) (tptp.hAPP (tptp.hAPP (tptp.c_COMBC @t178 @t203 @t297) @t259) @t52)))) @t186)) % 0.54/0.94 (define @t299 () (@list @t129 @t52 @t53 @t23)) % 0.54/0.94 (define @t300 () (tptp.hAPP @t143 @t32)) % 0.54/0.94 (define @t301 () (tptp.hAPP @t146 (tptp.hAPP @t300 @t37))) % 0.54/0.94 (define @t302 () (tptp.hAPP @t146 (tptp.hAPP @t260 @t37))) % 0.54/0.94 (define @t303 () (tptp.hBOOL (tptp.hAPP @t302 @t241))) % 0.54/0.94 (define @t304 () (tptp.hAPP @t146 (tptp.hAPP @t260 @t32))) % 0.54/0.94 (define @t305 () (tptp.hBOOL (tptp.hAPP @t304 @t241))) % 0.54/0.94 (define @t306 () (@list @t37 @t32 @t33 @t142 @t23)) % 0.54/0.94 (define @t307 () (tptp.c_HOL_Oundefined @t53)) % 0.54/0.94 (define @t308 () (tptp.hAPP @t263 @t32)) % 0.54/0.94 (define @t309 () (tptp.hAPP @t300 @t33)) % 0.54/0.94 (define @t310 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t146 @t309) @t142))) % 0.54/0.94 (define @t311 () (tptp.hAPP @t2 @t32)) % 0.54/0.94 (define @t312 () (tptp.c_Transitive__Closure_Ortrancl @t23 @t52)) % 0.54/0.94 (define @t313 () (tptp.hBOOL (tptp.hAPP @t304 @t312))) % 0.54/0.94 (define @t314 () (tptp.hBOOL (tptp.c_Product__Type_Ocurry @t23 @t53 tptp.tc_HOL_Obool @t2 @t85 @t88))) % 0.54/0.94 (define @t315 () (tptp.hBOOL (tptp.hAPP @t2 @t149))) % 0.54/0.94 (define @t316 () (tptp.hAPP @t294 @t33)) % 0.54/0.94 (define @t317 () (= @t173 @t307)) % 0.54/0.94 (define @t318 () (tptp.c_Relation_ODomain @t23 @t53 @t142)) % 0.54/0.94 (define @t319 () (tptp.hBOOL (tptp.hAPP @t86 @t318))) % 0.54/0.94 (define @t320 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t58 @t149) @t142))) % 0.54/0.94 (define @t321 () (@list @t142 @t88 @t85 @t53 @t23)) % 0.54/0.94 (define @t322 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t58 (tptp.hAPP @t148 @t213)) @t142))) % 0.54/0.94 (define @t323 () (@list @t142 @t53 @t85 @t23)) % 0.54/0.94 (define @t324 () (tptp.c_Relation_Osingle__valued @t23 @t53 @t142)) % 0.54/0.94 (define @t325 () (tptp.hAPP @t54 @t4)) % 0.54/0.94 (define @t326 () (@list @t4 @t213)) % 0.54/0.94 (define @t327 () (forall @t326 (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t58 (tptp.hAPP @t325 @t213)) @t142)) (forall @t212 (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t58 (tptp.hAPP @t325 @t209)) @t142)) (= @t213 @t209)))))) % 0.54/0.94 (define @t328 () (@list @t142 @t53 @t23)) % 0.54/0.94 (define @t329 () (tptp.hAPP @t122 @t142)) % 0.54/0.94 (define @t330 () (@list @t33 @t142 @t53 @t23)) % 0.54/0.94 (define @t331 () (tptp.c_Recdef_Oadm__wf @t23 @t53 @t52 @t129)) % 0.54/0.94 (define @t332 () (tptp.hBOOL (tptp.hAPP @t94 @t116))) % 0.54/0.94 (define @t333 () (not @t332)) % 0.54/0.94 (define @t334 () (@var "V_T_2" $$unsorted)) % 0.54/0.94 (define @t335 () (tptp.c_FuncSet_Oextensional__funcset @t23 @t53 @t116 @t334)) % 0.54/0.94 (define @t336 () (tptp.hBOOL (tptp.hAPP @t180 @t335))) % 0.54/0.94 (define @t337 () (@list @t33 @t334 @t116 @t2 @t53 @t23)) % 0.54/0.94 (define @t338 () (@list @t53 @t23 @t88 @t85 @t142)) % 0.54/0.94 (define @t339 () (tptp.c_Relation_ORange @t23 @t53 @t142)) % 0.54/0.94 (define @t340 () (tptp.c_Relation_OId__on @t23 @t27)) % 0.54/0.94 (define @t341 () (@list @t27 @t32 @t33 @t23)) % 0.54/0.94 (define @t342 () (tptp.c_Transitive__Closure_Ortrancl @t57 @t142)) % 0.54/0.94 (define @t343 () (@var "V_zb_2" $$unsorted)) % 0.54/0.94 (define @t344 () (@var "V_za_2" $$unsorted)) % 0.54/0.94 (define @t345 () (tptp.hAPP (tptp.hAPP @t54 @t344) @t343)) % 0.54/0.94 (define @t346 () (tptp.hAPP @t63 @t267)) % 0.54/0.94 (define @t347 () (@var "V_xb_2" $$unsorted)) % 0.54/0.94 (define @t348 () (@var "V_xa_2" $$unsorted)) % 0.54/0.94 (define @t349 () (tptp.hAPP (tptp.hAPP @t54 @t348) @t347)) % 0.54/0.94 (define @t350 () (tptp.hAPP @t63 @t349)) % 0.54/0.94 (define @t351 () (@var "V_ay_2" $$unsorted)) % 0.54/0.94 (define @t352 () (@var "V_ax_2" $$unsorted)) % 0.54/0.94 (define @t353 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t60 @t352) @t351))) % 0.54/0.94 (define @t354 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t60 @t131) @t130))) % 0.54/0.94 (define @t355 () (@var "B_ba" $$unsorted)) % 0.54/0.94 (define @t356 () (@var "B_aa" $$unsorted)) % 0.54/0.94 (define @t357 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t60 @t356) @t355))) % 0.54/0.94 (define @t358 () (@var "V_by_2" $$unsorted)) % 0.54/0.94 (define @t359 () (@var "V_bx_2" $$unsorted)) % 0.54/0.94 (define @t360 () (tptp.hAPP (tptp.hAPP @t54 @t359) @t358)) % 0.54/0.94 (define @t361 () (tptp.hAPP (tptp.hAPP @t54 @t356) @t355)) % 0.54/0.94 (define @t362 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t64 (tptp.hAPP @t346 @t361)) @t142))) % 0.54/0.94 (define @t363 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t60 @t359) @t358))) % 0.54/0.94 (define @t364 () (tptp.hAPP @t63 (tptp.hAPP (tptp.hAPP @t54 @t352) @t351))) % 0.54/0.94 (define @t365 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t64 (tptp.hAPP @t364 @t360)) @t342))) % 0.54/0.94 (define @t366 () (@list @t60 @t142 @t358 @t359 @t351 @t352 @t53 @t23)) % 0.54/0.94 (define @t367 () (tptp.c_Product__Type_OPair @t53 @t23)) % 0.54/0.94 (define @t368 () (tptp.tc_prod @t53 @t23)) % 0.54/0.94 (define @t369 () (tptp.c_member @t368)) % 0.54/0.94 (define @t370 () (tptp.c_Relation_ORange @t53 @t23 @t142)) % 0.54/0.94 (define @t371 () (tptp.c_Recdef_Owfrec__rel @t23 @t53 @t52 @t129 @t33)) % 0.54/0.94 (define @t372 () (forall @t8 (=> @t219 @t7))) % 0.54/0.94 (define @t373 () (tptp.tc_fun @t178 tptp.tc_HOL_Obool)) % 0.54/0.94 (define @t374 () (tptp.hBOOL (tptp.hAPP @t60 @t88))) % 0.54/0.94 (define @t375 () (tptp.hBOOL (tptp.hAPP @t60 @t209))) % 0.54/0.94 (define @t376 () (tptp.hBOOL (tptp.hAPP @t60 @t213))) % 0.54/0.94 (define @t377 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t146 (tptp.hAPP @t215 @t209)) @t142))) % 0.54/0.94 (define @t378 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t146 (tptp.hAPP @t144 @t213)) @t241))) % 0.54/0.94 (define @t379 () (tptp.hBOOL (tptp.hAPP @t60 @t85))) % 0.54/0.94 (define @t380 () (@list @t60 @t142 @t88 @t85 @t23)) % 0.54/0.94 (define @t381 () (tptp.hAPP @t146 (tptp.hAPP @t215 @t37))) % 0.54/0.94 (define @t382 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t146 (tptp.hAPP @t260 @t213)) @t142))) % 0.54/0.94 (define @t383 () (@list @t142 @t37 @t33 @t23)) % 0.54/0.94 (define @t384 () (@list @t142 @t88 @t85 @t23)) % 0.54/0.94 (define @t385 () (tptp.hBOOL @t172)) % 0.54/0.94 (define @t386 () (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t163 @t27 @t21)) % 0.54/0.94 (define @t387 () (tptp.hBOOL (tptp.hAPP @t386 @t33))) % 0.54/0.94 (define @t388 () (@list @t33 @t21 @t27 @t23)) % 0.54/0.94 (define @t389 () (tptp.hBOOL (tptp.hAPP @t25 @t386))) % 0.54/0.94 (define @t390 () (@list @t21 @t27 @t22 @t23)) % 0.54/0.94 (define @t391 () (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t163 @t21 @t225)) % 0.54/0.94 (define @t392 () (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t163 @t27 @t391)) % 0.54/0.94 (define @t393 () (@list @t225 @t21 @t27 @t23)) % 0.54/0.94 (define @t394 () (@list @t21 @t27 @t23)) % 0.54/0.94 (define @t395 () (tptp.hAPP @t1 @t33)) % 0.54/0.94 (define @t396 () (tptp.tc_fun @t53 @t23)) % 0.54/0.94 (define @t397 () (tptp.class_Lattices_Olattice @t23)) % 0.54/0.94 (define @t398 () (tptp.hBOOL (tptp.hAPP @t304 @t142))) % 0.54/0.94 (define @t399 () (tptp.c_Relation_Orefl__on @t23 @t27 @t142)) % 0.54/0.94 (define @t400 () (@list @t32 @t33 @t142 @t27 @t23)) % 0.54/0.94 (define @t401 () (tptp.tc_fun @t23 @t121)) % 0.54/0.94 (define @t402 () (@var "V_z" $$unsorted)) % 0.54/0.94 (define @t403 () (@var "V_y" $$unsorted)) % 0.54/0.94 (define @t404 () (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t23 @t403 @t402)) % 0.54/0.94 (define @t405 () (@var "V_x" $$unsorted)) % 0.54/0.94 (define @t406 () (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t23 @t405 @t404)) % 0.54/0.94 (define @t407 () (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t23 @t405 @t403)) % 0.54/0.94 (define @t408 () (= (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t23 @t407 @t402) @t406)) % 0.54/0.94 (define @t409 () (tptp.class_Lattices_Osemilattice__inf @t23)) % 0.54/0.94 (define @t410 () (@list @t402 @t403 @t405 @t23)) % 0.54/0.94 (define @t411 () (@var "V_c" $$unsorted)) % 0.54/0.94 (define @t412 () (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t23 @t273 (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t23 @t271 @t411))) % 0.54/0.94 (define @t413 () (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t23 @t273 @t271)) % 0.54/0.94 (define @t414 () (@list @t411 @t271 @t273 @t23)) % 0.54/0.94 (define @t415 () (= @t406 (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t23 @t403 (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t23 @t405 @t402)))) % 0.54/0.94 (define @t416 () (@list @t411 @t273 @t271 @t23)) % 0.54/0.94 (define @t417 () (= (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t23 @t405 @t407) @t407)) % 0.54/0.94 (define @t418 () (@list @t403 @t405 @t23)) % 0.54/0.94 (define @t419 () (@list @t271 @t273 @t23)) % 0.54/0.94 (define @t420 () (= @t407 (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t23 @t403 @t405))) % 0.54/0.94 (define @t421 () (= (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t23 @t405 @t405) @t405)) % 0.54/0.94 (define @t422 () (@list @t405 @t23)) % 0.54/0.94 (define @t423 () (tptp.hBOOL (tptp.hAPP @t274 @t142))) % 0.54/0.94 (define @t424 () (tptp.c_Transitive__Closure_Otrancl @t23 @t142)) % 0.54/0.94 (define @t425 () (tptp.hBOOL (tptp.hAPP @t199 @t424))) % 0.54/0.94 (define @t426 () (tptp.hAPP @t146 (tptp.hAPP @t260 @t348))) % 0.54/0.94 (define @t427 () (@list @t348 @t33 @t142 @t23)) % 0.54/0.94 (define @t428 () (tptp.c_Recdef_Ocut @t53 @t23)) % 0.54/0.94 (define @t429 () (@list @t33 @t129 @t52 @t23 @t53)) % 0.54/0.94 (define @t430 () (tptp.c_Relation_OId @t23)) % 0.54/0.94 (define @t431 () (@list @t85 @t23)) % 0.54/0.94 (define @t432 () (tptp.c_Transitive__Closure_Ortranclp @t23 @t142)) % 0.54/0.94 (define @t433 () (tptp.hAPP @t432 @t33)) % 0.54/0.94 (define @t434 () (tptp.hBOOL (tptp.hAPP @t433 @t32))) % 0.54/0.94 (define @t435 () (tptp.hAPP @t432 @t85)) % 0.54/0.94 (define @t436 () (tptp.hBOOL (tptp.hAPP @t172 @t32))) % 0.54/0.94 (define @t437 () (tptp.hBOOL (tptp.hAPP @t97 @t32))) % 0.54/0.94 (define @t438 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t401 @t27 @t21) @t33) @t32))) % 0.54/0.94 (define @t439 () (@list @t32 @t33 @t21 @t27 @t53 @t23)) % 0.54/0.94 (define @t440 () (tptp.tc_fun @t23 @t163)) % 0.54/0.94 (define @t441 () (tptp.hBOOL (tptp.hAPP @t435 @t22))) % 0.54/0.94 (define @t442 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t142 @t88) @t22))) % 0.54/0.94 (define @t443 () (tptp.hBOOL (tptp.hAPP @t435 @t88))) % 0.54/0.94 (define @t444 () (@list @t22 @t88 @t85 @t142 @t23)) % 0.54/0.94 (define @t445 () (tptp.hAPP @t432 @t88)) % 0.54/0.94 (define @t446 () (tptp.hBOOL (tptp.hAPP @t445 @t22))) % 0.54/0.94 (define @t447 () (@list @t22 @t23 @t88 @t85 @t142)) % 0.54/0.94 (define @t448 () (@var "V_a3_2" $$unsorted)) % 0.54/0.94 (define @t449 () (tptp.hAPP @t142 @t130)) % 0.54/0.94 (define @t450 () (tptp.hBOOL (tptp.hAPP @t449 @t448))) % 0.54/0.94 (define @t451 () (tptp.hAPP @t432 @t248)) % 0.54/0.94 (define @t452 () (@list @t130)) % 0.54/0.94 (define @t453 () (@list @t448 @t248 @t142 @t23)) % 0.54/0.94 (define @t454 () (tptp.hBOOL (tptp.hAPP @t276 @t424))) % 0.54/0.94 (define @t455 () (tptp.c_Transitive__Closure_Otrancl @t23 @t52)) % 0.54/0.94 (define @t456 () (@list @t52 @t23)) % 0.54/0.94 (define @t457 () (tptp.hBOOL (tptp.hAPP @t445 @t85))) % 0.54/0.94 (define @t458 () (@list @t88 @t85 @t142 @t23)) % 0.54/0.94 (define @t459 () (@list @t23)) % 0.54/0.94 (define @t460 () (tptp.hBOOL (tptp.hAPP @t279 @t424))) % 0.54/0.94 (define @t461 () (=> (tptp.hBOOL (tptp.hAPP @t281 @t424)) @t460)) % 0.54/0.94 (define @t462 () (=> @t286 @t460)) % 0.54/0.94 (define @t463 () (tptp.hBOOL (tptp.hAPP @t302 @t424))) % 0.54/0.94 (define @t464 () (=> @t282 @t460)) % 0.54/0.94 (define @t465 () (tptp.hBOOL (tptp.hAPP @t304 @t455))) % 0.54/0.94 (define @t466 () (@list @t52 @t32 @t33 @t23)) % 0.54/0.94 (define @t467 () (tptp.hAPP @t146 (tptp.hAPP @t210 @t32))) % 0.54/0.94 (define @t468 () (tptp.hAPP @t146 (tptp.hAPP @t260 @t209))) % 0.54/0.94 (define @t469 () (forall @t8 (not (tptp.hBOOL (tptp.hAPP @t191 @t424))))) % 0.54/0.94 (define @t470 () (tptp.c_Wellfounded_Oacyclic @t23 @t142)) % 0.54/0.94 (define @t471 () (@var "B_c" $$unsorted)) % 0.54/0.94 (define @t472 () (not @t305)) % 0.54/0.94 (define @t473 () (tptp.c_Set_Oinsert @t145 @t309 @t142)) % 0.54/0.94 (define @t474 () (@list @t142 @t33 @t32 @t23)) % 0.54/0.94 (define @t475 () (tptp.hBOOL (tptp.hAPP @t86 (tptp.c_Set_Oinsert @t23 @t88 @t27)))) % 0.54/0.94 (define @t476 () (@list @t27 @t88 @t85 @t23)) % 0.54/0.94 (define @t477 () (tptp.c_Set_Oinsert @t23 @t88 @t21)) % 0.54/0.94 (define @t478 () (tptp.hBOOL (tptp.hAPP @t86 @t477))) % 0.54/0.94 (define @t479 () (tptp.hBOOL (tptp.hAPP @t86 @t21))) % 0.54/0.94 (define @t480 () (@list @t88 @t21 @t85 @t23)) % 0.54/0.94 (define @t481 () (tptp.c_Set_Oinsert @t23 @t32 @t27)) % 0.54/0.94 (define @t482 () (tptp.c_Set_Oinsert @t23 @t33 @t27)) % 0.54/0.94 (define @t483 () (tptp.c_Set_Oinsert @t23 @t85 @t386)) % 0.54/0.94 (define @t484 () (tptp.c_Set_Oinsert @t23 @t85 @t21)) % 0.54/0.94 (define @t485 () (tptp.c_Set_Oinsert @t23 @t85 @t27)) % 0.54/0.94 (define @t486 () (@list @t21 @t27 @t85 @t23)) % 0.54/0.94 (define @t487 () (tptp.c_Set_Oinsert @t23 @t33 @t21)) % 0.54/0.94 (define @t488 () (@list @t21 @t27 @t33 @t23)) % 0.54/0.94 (define @t489 () (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t163 @t27 @t484)) % 0.54/0.94 (define @t490 () (not @t87)) % 0.54/0.94 (define @t491 () (=> @t490 (= @t489 @t386))) % 0.54/0.94 (define @t492 () (=> @t87 (= @t489 @t483))) % 0.54/0.94 (define @t493 () (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t163 @t484 @t225)) % 0.54/0.94 (define @t494 () (tptp.hBOOL (tptp.hAPP @t86 @t225))) % 0.54/0.94 (define @t495 () (=> (not @t494) (= @t493 @t391))) % 0.54/0.94 (define @t496 () (=> @t494 (= @t493 (tptp.c_Set_Oinsert @t23 @t85 @t391)))) % 0.54/0.94 (define @t497 () (@list @t21 @t225 @t85 @t23)) % 0.54/0.94 (define @t498 () (tptp.c_Fun_Ofun__upd @t53 @t23 @t2 @t33 @t32)) % 0.54/0.94 (define @t499 () (tptp.c_member @t396)) % 0.54/0.94 (define @t500 () (tptp.c_Wellfounded_Owf @t23 @t142)) % 0.54/0.94 (define @t501 () (tptp.c_Transitive__Closure_Otranclp @t23 @t142)) % 0.54/0.94 (define @t502 () (tptp.hAPP @t501 @t85)) % 0.54/0.94 (define @t503 () (tptp.hBOOL (tptp.hAPP @t502 @t88))) % 0.54/0.94 (define @t504 () (tptp.c_Relation_Oinv__image @t23 @t53)) % 0.54/0.94 (define @t505 () (@var "V_rb_2" $$unsorted)) % 0.54/0.94 (define @t506 () (@var "V_ra_2" $$unsorted)) % 0.54/0.94 (define @t507 () (@var "V_r_H_2" $$unsorted)) % 0.54/0.94 (define @t508 () (@list @t507 @t142 @t23)) % 0.54/0.94 (define @t509 () (tptp.hAPP @t501 @t248)) % 0.54/0.94 (define @t510 () (tptp.hBOOL (tptp.hAPP @t509 @t130))) % 0.54/0.94 (define @t511 () (tptp.hAPP @t142 @t248)) % 0.54/0.94 (define @t512 () (tptp.hBOOL (tptp.hAPP @t502 @t22))) % 0.54/0.94 (define @t513 () (=> @t442 @t512)) % 0.54/0.94 (define @t514 () (tptp.hAPP @t501 @t33)) % 0.54/0.94 (define @t515 () (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t501 @t32) @t37)) (tptp.hBOOL (tptp.hAPP @t514 @t37)))) % 0.54/0.94 (define @t516 () (=> @t446 @t512)) % 0.54/0.94 (define @t517 () (tptp.c_Transitive__Closure_Ortranclp @t23 @t52)) % 0.54/0.94 (define @t518 () (forall @t8 @t196)) % 0.54/0.94 (define @t519 () (tptp.c_Wellfounded_Omeasure @t23)) % 0.54/0.94 (define @t520 () (tptp.hAPP @t519 @t2)) % 0.54/0.94 (define @t521 () (tptp.c_Nitpick_Owfrec_H @t23 @t53 @t52 @t129 @t33)) % 0.54/0.94 (define @t522 () (tptp.c_Wellfounded_Owf @t23 @t52)) % 0.54/0.94 (define @t523 () (@var "V_H_2" $$unsorted)) % 0.54/0.94 (define @t524 () (tptp.hAPP @t2 @t85)) % 0.54/0.94 (define @t525 () (tptp.c_Recdef_Owfrec @t23 @t53 @t142 @t523)) % 0.54/0.94 (define @t526 () (tptp.tc_fun @t53 @t396)) % 0.54/0.94 (define @t527 () (tptp.tc_fun @t66 tptp.tc_HOL_Obool)) % 0.54/0.94 (define @t528 () (tptp.tc_fun @t53 @t53)) % 0.54/0.94 (define @t529 () (= @t173 @t32)) % 0.54/0.94 (define @t530 () (tptp.c_Fun_Ofun__upd @t23 @t53 @t2 @t33 @t32)) % 0.54/0.94 (define @t531 () (tptp.hAPP @t530 @t37)) % 0.54/0.94 (define @t532 () (= @t37 @t33)) % 0.54/0.94 (define @t533 () (=> (not @t532) (= @t531 (tptp.hAPP @t2 @t37)))) % 0.54/0.94 (define @t534 () (@list @t32 @t2 @t53 @t23 @t33 @t37)) % 0.54/0.94 (define @t535 () (@var "V_d_2" $$unsorted)) % 0.54/0.94 (define @t536 () (@var "V_m_2" $$unsorted)) % 0.54/0.94 (define @t537 () (tptp.hAPP (tptp.c_Fun_Ofun__upd @t23 @t53 @t2 @t85 @t88) @t33)) % 0.54/0.94 (define @t538 () (@var "B_M" $$unsorted)) % 0.54/0.94 (define @t539 () (tptp.c_Recdef_Owfrec @t23 @t53 @t258 @t538)) % 0.54/0.94 (define @t540 () (tptp.hAPP tptp.c_fequal @t33)) % 0.54/0.94 (define @t541 () (@var "B_Q" $$unsorted)) % 0.54/0.94 (define @t542 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t146 (tptp.hAPP @t215 @t4)) @t142))) % 0.54/0.94 (define @t543 () (tptp.hBOOL (tptp.hAPP @t195 @t541))) % 0.54/0.94 (define @t544 () (tptp.c_Wellfounded_OwfP @t23 @t142)) % 0.54/0.94 (define @t545 () (tptp.c_Orderings_Oord__class_Oless tptp.tc_Nat_Onat @t173 @t311)) % 0.54/0.94 (define @t546 () (tptp.c_Orderings_Oord__class_Oless @t23 @t413 @t405)) % 0.54/0.94 (define @t547 () (@list @t273 @t405 @t271 @t23)) % 0.54/0.94 (define @t548 () (@list @t271 @t405 @t273 @t23)) % 0.54/0.94 (define @t549 () (tptp.c_Wellfounded_Omlex__prod @t23 @t2 @t52)) % 0.54/0.94 (define @t550 () (tptp.hBOOL (tptp.hAPP @t304 @t549))) % 0.54/0.94 (define @t551 () (@list @t52 @t23 @t32 @t33 @t2)) % 0.54/0.94 (define @t552 () (tptp.c_Fun_Ooverride__on @t23 @t53 @t2 @t1 @t27 @t85)) % 0.54/0.94 (define @t553 () (=> @t490 (= @t552 @t524))) % 0.54/0.94 (define @t554 () (=> @t87 (= @t552 (tptp.hAPP @t1 @t85)))) % 0.54/0.94 (define @t555 () (@list @t1 @t2 @t53 @t27 @t85 @t23)) % 0.54/0.94 (define @t556 () (=> @t28 @t26)) % 0.54/0.94 (define @t557 () (tptp.c_Orderings_Oord__class_Oless @t163 @t27 @t21)) % 0.54/0.94 (define @t558 () (@list @t22 @t21 @t27 @t23)) % 0.54/0.94 (define @t559 () (tptp.tc_prod tptp.tc_Nat_Onat @t23)) % 0.54/0.94 (define @t560 () (tptp.c_Product__Type_OPair tptp.tc_Nat_Onat tptp.tc_Nat_Onat)) % 0.54/0.94 (define @t561 () (tptp.tc_prod tptp.tc_Nat_Onat tptp.tc_Nat_Onat)) % 0.54/0.94 (define @t562 () (tptp.c_member @t561)) % 0.54/0.94 (define @t563 () (@list @t32 @t33)) % 0.54/0.94 (define @t564 () (tptp.c_Transitive__Closure_Otrancl tptp.tc_Nat_Onat tptp.c_Wellfounded_Opred__nat)) % 0.54/0.94 (define @t565 () (tptp.c_Orderings_Oord__class_Oless tptp.tc_Nat_Onat @t405 @t403)) % 0.54/0.94 (define @t566 () (@list @t403 @t405)) % 0.54/0.94 (define @t567 () (tptp.c_Orderings_Oord__class_Oless @t163 @t27 @t225)) % 0.54/0.94 (define @t568 () (=> (tptp.c_Orderings_Oord__class_Oless @t163 @t21 @t225) @t567)) % 0.54/0.94 (define @t569 () (@var "V_n_2" $$unsorted)) % 0.54/0.94 (define @t570 () (tptp.c_Orderings_Oord__class_Oless__eq tptp.tc_Nat_Onat @t536 @t569)) % 0.54/0.94 (define @t571 () (tptp.hAPP @t562 (tptp.hAPP (tptp.hAPP @t560 @t536) @t569))) % 0.54/0.94 (define @t572 () (@list @t569 @t536)) % 0.54/0.94 (define @t573 () (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t405 @t271)) % 0.54/0.94 (define @t574 () (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t405 @t273)) % 0.54/0.94 (define @t575 () (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t405 @t413)) % 0.54/0.94 (define @t576 () (@list @t271 @t273 @t405 @t23)) % 0.54/0.94 (define @t577 () (@var "V_d" $$unsorted)) % 0.54/0.94 (define @t578 () (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t273 @t411)) % 0.54/0.94 (define @t579 () (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t405 @t402)) % 0.54/0.94 (define @t580 () (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t405 @t403)) % 0.54/0.94 (define @t581 () (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t403 @t405)) % 0.54/0.94 (define @t582 () (@list @t405 @t403 @t23)) % 0.54/0.94 (define @t583 () (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t413 @t405)) % 0.54/0.94 (define @t584 () (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t33 @t32)) % 0.54/0.94 (define @t585 () (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t407 @t403)) % 0.54/0.94 (define @t586 () (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t407 @t405)) % 0.54/0.94 (define @t587 () (tptp.c_Orderings_Oord__class_Oless tptp.tc_Nat_Onat @t536 @t569)) % 0.54/0.94 (define @t588 () (tptp.c_Relation_Oantisym @t23 @t142)) % 0.54/0.94 (define @t589 () (tptp.class_Orderings_Opreorder @t23)) % 0.54/0.94 (define @t590 () (@var "V_n" $$unsorted)) % 0.54/0.94 (define @t591 () (@var "V_m" $$unsorted)) % 0.54/0.94 (define @t592 () (tptp.c_Orderings_Oord__class_Oless__eq tptp.tc_Nat_Onat @t591 @t590)) % 0.54/0.94 (define @t593 () (= @t591 @t590)) % 0.54/0.94 (define @t594 () (tptp.c_Orderings_Oord__class_Oless tptp.tc_Nat_Onat @t591 @t590)) % 0.54/0.94 (define @t595 () (@list @t590 @t591)) % 0.54/0.94 (define @t596 () (not @t593)) % 0.54/0.94 (define @t597 () (tptp.c_Orderings_Oord__class_Oless__eq @t163 @t27 @t21)) % 0.54/0.94 (define @t598 () (tptp.c_Orderings_Oord__class_Oless__eq @t163 @t21 @t225)) % 0.54/0.94 (define @t599 () (tptp.c_Orderings_Oord__class_Oless__eq @t178 @t2 @t1)) % 0.54/0.94 (define @t600 () (tptp.class_Orderings_Oord @t53)) % 0.54/0.94 (define @t601 () (@list @t1 @t2 @t23 @t53)) % 0.54/0.94 (define @t602 () (@list @t275 @t142 @t23)) % 0.54/0.94 (define @t603 () (@var "V_A_H_2" $$unsorted)) % 0.54/0.94 (define @t604 () (@var "V_R1_2" $$unsorted)) % 0.54/0.94 (define @t605 () (@var "V_R2_2" $$unsorted)) % 0.54/0.94 (define @t606 () (@list @t605 @t604 @t23)) % 0.54/0.94 (define @t607 () (tptp.c_Orderings_Oord__class_Oless__eq @t203 @t142 @t140)) % 0.54/0.94 (define @t608 () (@list @t140 @t142 @t23)) % 0.54/0.94 (define @t609 () (tptp.c_Orderings_Oord__class_Oless__eq @t118 @t142 @t140)) % 0.54/0.94 (define @t610 () (@list @t140 @t142 @t53 @t23)) % 0.54/0.94 (define @t611 () (tptp.c_Transitive__Closure_Ortrancl @t23 @t140)) % 0.54/0.94 (define @t612 () (tptp.c_Orderings_Oord__class_Oless__eq @t203 @t241 @t611)) % 0.54/0.94 (define @t613 () (tptp.c_Orderings_Oord__class_Oless__eq @t163 @t27 @t225)) % 0.54/0.94 (define @t614 () (tptp.c_Orderings_Oord__class_Oless__eq @t163 @t21 @t27)) % 0.54/0.94 (define @t615 () (tptp.class_Orderings_Olinorder @t23)) % 0.54/0.94 (define @t616 () (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t32 @t33)) % 0.54/0.94 (define @t617 () (tptp.class_Orderings_Oorder @t23)) % 0.54/0.94 (define @t618 () (= @t405 @t403)) % 0.54/0.94 (define @t619 () (= @t584 @t40)) % 0.54/0.94 (define @t620 () (@list @t33 @t32 @t23)) % 0.54/0.94 (define @t621 () (= @t273 @t271)) % 0.54/0.94 (define @t622 () (tptp.class_Orderings_Oord @t23)) % 0.54/0.94 (define @t623 () (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t411 @t273)) % 0.54/0.94 (define @t624 () (= @t271 @t411)) % 0.54/0.94 (define @t625 () (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t273 @t271)) % 0.54/0.94 (define @t626 () (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t271 @t273)) % 0.54/0.94 (define @t627 () (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t403 @t402)) % 0.54/0.94 (define @t628 () (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t402 @t403)) % 0.54/0.94 (define @t629 () (@list @t402 @t405 @t403 @t23)) % 0.54/0.94 (define @t630 () (tptp.c_Orderings_Oord__class_Oless @t23 @t32 @t33)) % 0.54/0.94 (define @t631 () (tptp.c_Orderings_Oord__class_Oless @t23 @t33 @t32)) % 0.54/0.94 (define @t632 () (not @t631)) % 0.54/0.94 (define @t633 () (tptp.c_Orderings_Oord__class_Oless @t23 @t403 @t405)) % 0.54/0.94 (define @t634 () (tptp.c_Orderings_Oord__class_Oless @t23 @t405 @t403)) % 0.54/0.94 (define @t635 () (= @t632 @t40)) % 0.54/0.94 (define @t636 () (not @t634)) % 0.54/0.94 (define @t637 () (not @t618)) % 0.54/0.94 (define @t638 () (tptp.c_Orderings_Oord__class_Oless @t23 @t271 @t273)) % 0.54/0.94 (define @t639 () (tptp.c_Orderings_Oord__class_Oless @t23 @t273 @t271)) % 0.54/0.94 (define @t640 () (@list @t273 @t271 @t23)) % 0.54/0.94 (define @t641 () (tptp.c_Orderings_Oord__class_Oless @t23 @t273 @t411)) % 0.54/0.94 (define @t642 () (tptp.c_Orderings_Oord__class_Oless @t23 @t411 @t273)) % 0.54/0.94 (define @t643 () (tptp.c_Orderings_Oord__class_Oless @t23 @t405 @t402)) % 0.54/0.94 (define @t644 () (=> (tptp.c_Orderings_Oord__class_Oless @t23 @t403 @t402) @t643)) % 0.54/0.94 (define @t645 () (tptp.c_Orderings_Oord__class_Oless @t23 @t402 @t405)) % 0.54/0.94 (define @t646 () (=> (tptp.c_Orderings_Oord__class_Oless @t23 @t402 @t403) @t645)) % 0.54/0.94 (define @t647 () (@list @t590)) % 0.54/0.94 (define @t648 () (tptp.c_Orderings_Oord__class_Oless tptp.tc_Nat_Onat @t569 @t536)) % 0.54/0.94 (define @t649 () (= @t536 @t569)) % 0.54/0.94 (define @t650 () (not @t649)) % 0.54/0.94 (define @t651 () (@var "V_t" $$unsorted)) % 0.54/0.94 (define @t652 () (@var "V_s" $$unsorted)) % 0.54/0.94 (define @t653 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t60 @t569) @t536))) % 0.54/0.94 (define @t654 () (tptp.c_Orderings_Oord__class_Oless__eq tptp.tc_Nat_Onat @t590 @t591)) % 0.54/0.94 (define @t655 () (@var "V_k" $$unsorted)) % 0.54/0.94 (define @t656 () (@var "V_i" $$unsorted)) % 0.54/0.94 (define @t657 () (@var "V_j" $$unsorted)) % 0.54/0.94 (define @t658 () (@list @t21 @t27 @t53 @t23)) % 0.54/0.94 (define @t659 () (not @t621)) % 0.54/0.94 (define @t660 () (@var "V_t_2" $$unsorted)) % 0.54/0.94 (define @t661 () (tptp.c_Product__Type_OPair @t561 @t561)) % 0.54/0.94 (define @t662 () (tptp.c_member (tptp.tc_prod @t561 @t561))) % 0.54/0.94 (define @t663 () (tptp.hAPP @t662 (tptp.hAPP (tptp.hAPP @t661 (tptp.hAPP (tptp.hAPP @t560 @t85) @t140)) (tptp.hAPP (tptp.hAPP @t560 @t88) @t660)))) % 0.54/0.94 (define @t664 () (tptp.hBOOL (tptp.hAPP @t663 tptp.c_FunDef_Opair__less))) % 0.54/0.94 (define @t665 () (tptp.c_Orderings_Oord__class_Oless__eq tptp.tc_Nat_Onat @t85 @t88)) % 0.54/0.94 (define @t666 () (@list @t660 @t140 @t88 @t85)) % 0.54/0.94 (define @t667 () (tptp.hBOOL (tptp.hAPP @t663 tptp.c_FunDef_Opair__leq))) % 0.54/0.94 (define @t668 () (tptp.c_Orderings_Oord__class_Oless tptp.tc_Nat_Onat @t85 @t88)) % 0.54/0.94 (define @t669 () (@list @t23 @t21 @t27)) % 0.54/0.94 (define @t670 () (@var "V_Q_2" $$unsorted)) % 0.54/0.94 (define @t671 () (tptp.hAPP @t670 @t33)) % 0.54/0.94 (define @t672 () (tptp.hBOOL @t671)) % 0.54/0.94 (define @t673 () (tptp.c_Orderings_Oord__class_Oless__eq @t163 @t60 @t670)) % 0.54/0.94 (define @t674 () (tptp.hBOOL (tptp.hAPP @t671 @t32))) % 0.54/0.94 (define @t675 () (tptp.hBOOL (tptp.hAPP @t68 @t32))) % 0.54/0.94 (define @t676 () (tptp.c_Orderings_Oord__class_Oless__eq @t401 @t60 @t670)) % 0.54/0.94 (define @t677 () (@var "V_YS_2" $$unsorted)) % 0.54/0.94 (define @t678 () (@var "V_XS_2" $$unsorted)) % 0.54/0.94 (define @t679 () (tptp.tc_fun @t561 tptp.tc_HOL_Obool)) % 0.54/0.94 (define @t680 () (tptp.c_Product__Type_OPair @t679 @t679)) % 0.54/0.94 (define @t681 () (tptp.tc_prod @t679 @t679)) % 0.54/0.94 (define @t682 () (tptp.c_member @t681)) % 0.54/0.94 (define @t683 () (tptp.hAPP @t680 @t678)) % 0.54/0.94 (define @t684 () (tptp.hAPP @t682 (tptp.hAPP @t683 @t677))) % 0.54/0.94 (define @t685 () (tptp.hAPP @t662 (tptp.hAPP (tptp.hAPP @t661 @t33) @t32))) % 0.54/0.94 (define @t686 () (tptp.hBOOL (tptp.hAPP @t685 tptp.c_FunDef_Opair__leq))) % 0.54/0.94 (define @t687 () (tptp.hAPP @t562 @t32)) % 0.54/0.94 (define @t688 () (tptp.hAPP @t682 (tptp.hAPP @t683 (tptp.c_Set_Oinsert @t561 @t32 @t677)))) % 0.54/0.94 (define @t689 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t562 @t33) @t678))) % 0.54/0.94 (define @t690 () (@list @t677 @t32 @t678 @t33)) % 0.54/0.94 (define @t691 () (tptp.hBOOL (tptp.hAPP @t685 tptp.c_FunDef_Opair__less))) % 0.54/0.94 (define @t692 () (@var "V_Y_2" $$unsorted)) % 0.54/0.94 (define @t693 () (@var "V_X_2" $$unsorted)) % 0.54/0.94 (define @t694 () (tptp.tc_fun @t681 tptp.tc_HOL_Obool)) % 0.54/0.94 (define @t695 () (tptp.c_Product__Type_OPair @t694 @t694)) % 0.54/0.94 (define @t696 () (tptp.c_FunDef_Orp__inv__image @t23 @t53)) % 0.54/0.94 (define @t697 () (tptp.tc_prod @t527 @t527)) % 0.54/0.94 (define @t698 () (tptp.tc_fun @t527 @t697)) % 0.54/0.94 (define @t699 () (tptp.tc_fun @t396 @t698)) % 0.54/0.94 (define @t700 () (tptp.tc_fun @t396 @t527)) % 0.54/0.94 (define @t701 () (tptp.tc_fun @t396 @t697)) % 0.54/0.94 (define @t702 () (tptp.tc_fun @t700 @t701)) % 0.54/0.94 (define @t703 () (tptp.tc_fun @t203 @t701)) % 0.54/0.94 (define @t704 () (tptp.tc_fun @t203 @t700)) % 0.54/0.94 (define @t705 () (tptp.c_Relation_Orel__comp @t23 @t53 @t226 @t142 @t140)) % 0.54/0.94 (define @t706 () (tptp.tc_prod @t23 @t226)) % 0.54/0.94 (define @t707 () (tptp.tc_prod @t53 @t226)) % 0.54/0.94 (define @t708 () (@var "V_s_H_2" $$unsorted)) % 0.54/0.94 (define @t709 () (@var "T_1" $$unsorted)) % 0.54/0.94 (define @t710 () (@var "T_2" $$unsorted)) % 0.54/0.94 (define @t711 () (tptp.tc_fun @t710 @t709)) % 0.54/0.94 (define @t712 () (tptp.class_Lattices_Olattice @t709)) % 0.54/0.94 (define @t713 () (@list @t710 @t709)) % 0.54/0.94 (define @t714 () (@var "V_P" $$unsorted)) % 0.54/0.94 (define @t715 () (@var "V_Q" $$unsorted)) % 0.54/0.94 (define @t716 () (tptp.hAPP @t670 @t52)) % 0.54/0.94 (define @t717 () (tptp.hAPP @t60 @t52)) % 0.54/0.94 (define @t718 () (@list @t52 @t670 @t60 @t23 @t226 @t53)) % 0.54/0.94 (define @t719 () (tptp.hBOOL (tptp.hAPP @t540 @t32))) % 0.54/0.94 (define @t720 () (tptp.hBOOL @t60)) % 0.54/0.94 (define @t721 () (not @t720)) % 0.54/0.94 (define @t722 () (tptp.hBOOL (tptp.hAPP tptp.c_fNot @t60))) % 0.54/0.94 (define @t723 () (@list @t60)) % 0.54/0.94 (define @t724 () (tptp.hBOOL (tptp.hAPP (tptp.hAPP tptp.c_fconj @t60) @t670))) % 0.54/0.94 (define @t725 () (tptp.hBOOL @t670)) % 0.54/0.94 (define @t726 () (@list @t670 @t60)) % 0.54/0.94 (define @t727 () (not @t724)) % 0.54/0.94 (define @t728 () (not @t81)) % 0.54/0.94 (define @t729 () (@list false)) % 0.54/0.94 (define @t730 () (@list @t81)) % 0.54/0.94 (assume @p1 (forall (@list @t1 @t2) (=> (forall @t8 @t7) @t3))) % 0.54/0.94 (assume @p2 (tptp.c_Arrow__Order__Mirabelle_OIIA tptp.v_F)) % 0.54/0.94 (assume @p3 (tptp.c_Arrow__Order__Mirabelle_Ounanimity tptp.v_F)) % 0.54/0.94 (assume @p4 (not (= tptp.v_a____ tptp.v_b____))) % 0.54/0.94 (assume @p5 (forall @t20 (= @t19 @t15))) % 0.54/0.94 (assume @p6 (forall (@list @t22 @t23 @t21 @t27) (=> @t30 (=> @t29 (not (=> (not @t28) @t26)))))) % 0.54/0.94 (assume @p7 (forall @t44 (= (tptp.hBOOL (tptp.hAPP @t35 (tptp.c_Arrow__Order__Mirabelle_Omkbot @t31 @t37))) (and @t43 (=> @t38 @t41) (=> @t39 @t36))))) % 0.54/0.94 (assume @p8 (forall @t44 (= (tptp.hBOOL (tptp.hAPP @t35 (tptp.c_Arrow__Order__Mirabelle_Omktop @t31 @t37))) (and @t39 (=> @t42 @t41) (=> @t43 @t36))))) % 0.54/0.94 (assume @p9 (forall @t20 (= @t47 @t15))) % 0.54/0.94 (assume @p10 (forall @t20 (= @t19 @t49))) % 0.54/0.94 (assume @p11 (forall @t20 (= @t49 @t51))) % 0.54/0.94 (assume @p12 (forall @t20 (= @t51 @t47))) % 0.54/0.94 (assume @p13 (forall @t20 (= @t47 @t19))) % 0.54/0.94 (assume @p14 (forall (@list @t32 @t33 @t52 @t53 @t23) (= (tptp.hBOOL (tptp.hAPP (tptp.hAPP (tptp.c_FunDef_Oin__rel @t23 @t53 @t52) @t33) @t32)) (tptp.hBOOL (tptp.hAPP @t59 @t52))))) % 0.54/0.94 (assume @p15 (forall (@list @t23 @t52 @t32 @t62 @t53 @t33 @t60) (=> @t69 (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t67 (tptp.hAPP (tptp.hAPP @t65 @t62) @t32)) (tptp.hAPP @t52 @t33))) (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t64 (tptp.hAPP (tptp.hAPP @t63 (tptp.hAPP @t55 @t62)) @t56)) @t61)))))) % 0.54/0.94 (assume @p16 (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t72 tptp.v_P_H____) tptp.c_Arrow__Order__Mirabelle_OProf))) % 0.54/0.94 (assume @p17 (= @t81 @t73)) % 0.54/0.94 (assume @p18 (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t72 tptp.v_P____) tptp.c_Arrow__Order__Mirabelle_OProf))) % 0.54/0.94 (assume @p19 (= @t82 @t81)) % 0.54/0.94 (assume @p20 (= @t83 @t82)) % 0.54/0.94 (assume @p21 (= @t84 @t83)) % 0.54/0.94 (assume @p22 (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t72 @t78) tptp.c_Arrow__Order__Mirabelle_OProf))) % 0.54/0.94 (assume @p23 (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t72 @t80) tptp.c_Arrow__Order__Mirabelle_OProf))) % 0.54/0.94 (assume @p24 (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t72 @t79) tptp.c_Arrow__Order__Mirabelle_OProf))) % 0.54/0.94 (assume @p25 (forall @t91 (=> @t90 (=> (tptp.hBOOL (tptp.hAPP @t89 @t27)) @t87)))) % 0.54/0.94 (assume @p26 (forall (@list @t27 @t23 @t32 @t33) (=> @t40 (= @t95 @t93)))) % 0.54/0.94 (assume @p27 (forall (@list @t33 @t23 @t21 @t27) (=> @t30 (= @t95 @t96)))) % 0.54/0.94 (assume @p28 (forall @t99 (= @t95 @t98))) % 0.54/0.94 (assume @p29 (forall @t115 (=> @t114 (=> @t113 (=> @t112 (=> @t111 (=> @t110 (=> @t109 (=> @t108 (=> @t107 @t104)))))))))) % 0.54/0.94 (assume @p30 (forall @t115 (=> @t114 (=> @t113 (=> @t112 (=> @t111 (=> @t110 (=> @t109 (=> @t108 (= @t107 @t104)))))))))) % 0.54/0.94 (assume @p31 (forall @t125 (= (= @t124 @t123) @t117))) % 0.54/0.94 (assume @p32 (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t127 tptp.v_F) @t126))) % 0.54/0.94 (assume @p33 (forall @t139 (= (tptp.c_Arrow__Order__Mirabelle_OIIA @t129) (forall @t8 (=> @t138 (forall @t137 (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t72 @t128) tptp.c_Arrow__Order__Mirabelle_OProf)) (forall @t136 (=> (forall @t20 (= @t135 (tptp.hBOOL (tptp.hAPP @t132 (tptp.hAPP @t128 @t9))))) (= @t134 (tptp.hBOOL (tptp.hAPP @t132 (tptp.hAPP @t129 @t128))))))))))))) % 0.54/0.94 (assume @p34 (forall @t139 (= (tptp.c_Arrow__Order__Mirabelle_Ounanimity @t129) (forall @t8 (=> @t138 (forall @t136 (=> (forall @t20 @t135) @t134))))))) % 0.54/0.94 (assume @p35 (forall (@list @t140 @t142 @t101 @t102 @t88 @t85 @t53 @t23) (= (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t64 (tptp.hAPP (tptp.hAPP @t63 @t149) @t147)) (tptp.c_Wellfounded_Olex__prod @t23 @t53 @t142 @t140))) (or (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t146 (tptp.hAPP @t144 @t102)) @t142)) (and @t141 (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t67 (tptp.hAPP (tptp.hAPP @t65 @t88) @t101)) @t140))))))) % 0.54/0.94 (assume @p36 (forall @t153 (= @t152 (forall @t8 (=> @t138 (= @t133 @t151)))))) % 0.54/0.94 (assume @p37 (forall @t162 (=> @t114 (=> @t161 (= (tptp.hBOOL (tptp.hAPP @t35 (tptp.hAPP (tptp.hAPP @t159 @t85) @t88))) (and @t41 (=> @t158 (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t13 (tptp.hAPP @t34 @t88)) @t31))) (=> (not @t158) (and (=> @t154 (or @t157 (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t13 (tptp.hAPP @t156 @t32)) @t31)))) (=> @t155 @t36))))))))) % 0.54/0.94 (assume @p38 (forall (@list @t31) (=> @t161 (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t72 (tptp.c_COMBK @t70 tptp.tc_Arrow__Order__Mirabelle_Oindi @t31)) tptp.c_Arrow__Order__Mirabelle_OProf))))) % 0.54/0.94 (assume @p39 (forall @t167 (= (= @t166 @t165) @t117))) % 0.54/0.94 (assume @p40 (forall @t168 (=> @t41 (=> @t161 (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t160 (tptp.hAPP (tptp.hAPP @t159 @t33) @t32)) tptp.c_Arrow__Order__Mirabelle_OLin)))))) % 0.54/0.94 (assume @p41 (forall @t169 (=> @t161 (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t160 (tptp.c_Arrow__Order__Mirabelle_Omktop @t31 @t33)) tptp.c_Arrow__Order__Mirabelle_OLin))))) % 0.54/0.94 (assume @p42 (forall @t169 (=> @t161 (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t160 (tptp.c_Arrow__Order__Mirabelle_Omkbot @t31 @t33)) tptp.c_Arrow__Order__Mirabelle_OLin))))) % 0.54/0.94 (assume @p43 (forall @t170 (= (tptp.hBOOL (tptp.hAPP @t94 (tptp.hAPP tptp.c_fequal @t32))) @t40))) % 0.54/0.94 (assume @p44 (forall (@list @t32 @t33 @t31) (=> @t161 (=> @t41 (= (not @t36) (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t13 (tptp.hAPP (tptp.hAPP @t10 @t32) @t33)) @t31))))))) % 0.54/0.94 (assume @p45 (forall (@list @t88 @t85 @t31) (=> @t161 (=> (tptp.hBOOL (tptp.hAPP @t106 @t31)) (not (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t13 (tptp.hAPP @t156 @t85)) @t31))))))) % 0.54/0.94 (assume @p46 (forall @t182 (=> @t181 (=> (not @t176) @t171)))) % 0.54/0.94 (assume @p47 (forall @t162 (=> @t114 (=> @t161 (= (tptp.hBOOL (tptp.hAPP @t35 (tptp.c_Arrow__Order__Mirabelle_Oabove @t31 @t85 @t88))) (and @t41 (=> @t183 (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t13 (tptp.hAPP @t105 @t32)) @t31))) (=> (not @t183) (and (=> @t157 (or @t154 (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t13 (tptp.hAPP @t34 @t85)) @t31)))) (=> (not @t157) @t36))))))))) % 0.54/0.94 (assume @p48 (forall @t153 (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t127 @t129) @t126)) (=> (forall @t8 (=> @t138 (forall @t136 (=> (not (= @t131 @t130)) (=> (tptp.hBOOL (tptp.hAPP @t132 @t151)) @t134))))) @t152)))) % 0.54/0.94 (assume @p49 (forall @t182 (=> @t185 (=> @t95 (tptp.hBOOL (tptp.hAPP @t175 @t21)))))) % 0.54/0.94 (assume @p50 (forall @t182 (=> @t181 (=> @t95 @t176)))) % 0.54/0.94 (assume @p51 (forall @t188 (tptp.hBOOL (tptp.hAPP (tptp.hAPP (tptp.c_member @t187) @t186) (tptp.c_FuncSet_OPi @t23 @t23 @t27 (tptp.c_COMBK @t163 @t23 @t27)))))) % 0.54/0.94 (assume @p52 (forall @t168 (=> @t41 (=> @t161 (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t160 (tptp.c_Arrow__Order__Mirabelle_Oabove @t31 @t33 @t32)) tptp.c_Arrow__Order__Mirabelle_OLin)))))) % 0.54/0.94 (assume @p53 (forall (@list @t88 @t85) (=> @t114 (exists @t8 (and (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t160 @t4) tptp.c_Arrow__Order__Mirabelle_OLin)) (tptp.hBOOL (tptp.hAPP @t106 @t4))))))) % 0.54/0.94 (assume @p54 (forall @t193 (= (tptp.c_Nitpick_Orefl_H @t23 @t142) (forall @t8 @t192)))) % 0.54/0.94 (assume @p55 (forall @t198 (= @t197 (forall @t8 (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t146 (tptp.hAPP @t189 @t85)) @t142)) @t196))))) % 0.54/0.94 (assume @p56 (forall (@list @t85 @t142 @t88 @t23) (=> @t201 (=> @t200 @t197)))) % 0.54/0.94 (assume @p57 (forall @t207 (= (tptp.hBOOL (tptp.hAPP (tptp.c_Wellfounded_Oaccp @t23 @t206) @t33)) @t202))) % 0.54/0.94 (assume @p58 (forall (@list @t52 @t33 @t23) (=> (not (tptp.hBOOL (tptp.hAPP @t94 @t208))) (not (forall @t212 (=> @t211 (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t24 @t209) @t208)))))))) % 0.54/0.94 (assume @p59 (forall (@list @t142 @t33 @t23) (=> (forall @t217 (=> @t216 (tptp.hBOOL (tptp.hAPP @t214 @t194)))) @t202))) % 0.54/0.94 (assume @p60 (forall @t221 (=> @t220 @t181))) % 0.54/0.94 (assume @p61 (forall @t221 (=> @t222 @t185))) % 0.54/0.94 (assume @p62 (forall (@list @t21 @t53 @t1 @t2 @t27 @t23) (=> (forall (@list @t224) (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t24 @t224) @t27)) (= (tptp.hAPP @t2 @t224) (tptp.hAPP @t1 @t224)))) (= @t181 (tptp.hBOOL (tptp.hAPP @t223 @t177)))))) % 0.54/0.94 (assume @p63 (forall (@list @t225 @t1 @t226 @t21 @t27 @t2 @t53 @t23) (=> @t185 (=> @t229 (tptp.hBOOL (tptp.hAPP (tptp.hAPP (tptp.c_member (tptp.tc_fun @t23 @t226)) @t228) (tptp.c_FuncSet_OPi @t23 @t226 @t27 (tptp.c_COMBK @t227 @t23 @t225)))))))) % 0.54/0.94 (assume @p64 (forall (@list @t232 @t230 @t231 @t225 @t1 @t226 @t21 @t27 @t2 @t53 @t23) (=> @t185 (=> @t229 (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP (tptp.c_member (tptp.tc_fun @t226 @t231)) @t230) (tptp.c_FuncSet_OPi @t226 @t231 @t225 (tptp.c_COMBK (tptp.tc_fun @t231 tptp.tc_HOL_Obool) @t226 @t232)))) (= (tptp.c_FuncSet_Ocompose @t23 @t226 @t231 @t27 @t230 @t228) (tptp.c_FuncSet_Ocompose @t23 @t53 @t231 @t27 (tptp.c_FuncSet_Ocompose @t53 @t226 @t231 @t21 @t230 @t1) @t2))))))) % 0.54/0.94 (assume @p65 (forall @t235 (= @t234 (forall @t8 (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t142 @t4) @t85)) (tptp.hBOOL (tptp.hAPP @t233 @t4))))))) % 0.54/0.94 (assume @p66 (forall @t238 (=> @t237 (=> @t236 @t234)))) % 0.54/0.94 (assume @p67 (forall (@list @t2 @t1 @t53 @t226 @t27 @t33 @t23) (=> @t95 (= (tptp.hAPP @t239 @t33) (tptp.hAPP @t1 @t173))))) % 0.54/0.94 (assume @p68 (forall (@list @t1 @t2 @t27 @t226 @t53 @t23) (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t179 (tptp.c_FuncSet_Ocompose @t23 @t226 @t53 @t27 @t2 @t1)) @t240)))) % 0.54/0.94 (assume @p69 (forall (@list @t88 @t142 @t85 @t23) (=> @t197 (=> @t244 @t201)))) % 0.54/0.94 (assume @p70 (forall (@list @t142 @t85 @t88 @t23) (=> @t244 (=> @t197 @t201)))) % 0.54/0.94 (assume @p71 (forall @t256 (= (tptp.hBOOL (tptp.hAPP @t255 @t253)) (exists @t254 (and (= @t253 @t251) @t249))))) % 0.54/0.94 (assume @p72 (forall (@list @t53 @t85 @t33 @t23 @t257 @t258) (=> (tptp.hBOOL (tptp.hAPP @t261 @t258)) (= (tptp.hAPP (tptp.hAPP (tptp.hAPP (tptp.hAPP @t259 @t257) @t258) @t85) @t33) (tptp.hAPP @t257 @t33))))) % 0.54/0.94 (assume @p73 (forall (@list @t1 @t33 @t142 @t2 @t53 @t23) (= (= @t263 (tptp.hAPP (tptp.hAPP (tptp.hAPP @t259 @t1) @t142) @t33)) (forall @t217 (=> @t216 (= (tptp.hAPP @t2 @t213) (tptp.hAPP @t1 @t213))))))) % 0.54/0.94 (assume @p74 (forall (@list @t2 @t53 @t142 @t85 @t33 @t23) (=> @t265 (= (tptp.hAPP @t264 @t33) @t173)))) % 0.54/0.94 (assume @p75 (exists (@list @t266) (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t160 @t266) tptp.c_Arrow__Order__Mirabelle_OLin)))) % 0.54/0.94 (assume @p76 (forall (@list @t53 @t23 @t60) (= (forall @t269 (tptp.hBOOL (tptp.hAPP @t60 @t268))) (forall @t136 (tptp.hBOOL (tptp.hAPP @t60 @t267)))))) % 0.54/0.94 (assume @p77 (forall (@list @t270 @t272 @t271 @t273 @t53 @t23) (=> (= (tptp.hAPP (tptp.hAPP @t54 @t273) @t271) (tptp.hAPP (tptp.hAPP @t54 @t272) @t270)) (not (=> (= @t273 @t272) (not (= @t271 @t270))))))) % 0.54/0.94 (assume @p78 (forall (@list @t101 @t102 @t88 @t85 @t53 @t23) (= (= @t149 @t147) (and @t141 (= @t88 @t101))))) % 0.54/0.94 (assume @p79 (forall @t198 (tptp.hBOOL (tptp.hAPP @t274 @t241)))) % 0.54/0.94 (assume @p80 (forall @t278 (=> @t277 (tptp.hBOOL (tptp.hAPP @t276 @t241))))) % 0.54/0.94 (assume @p81 (forall @t285 (=> @t284 @t283))) % 0.54/0.94 (assume @p82 (forall @t285 (=> @t284 (=> @t286 @t280)))) % 0.54/0.94 (assume @p83 (forall @t285 (=> @t200 @t283))) % 0.54/0.94 (assume @p84 (forall (@list @t88 @t85 @t287 @t23 @t226 @t53) (= (tptp.c_Product__Type_Oprod_Oprod__rec @t53 @t226 @t23 @t287 @t289) (tptp.hAPP (tptp.hAPP @t287 @t85) @t88)))) % 0.54/0.94 (assume @p85 (forall @t292 (=> @t185 (=> @t291 (= (tptp.c_FuncSet_Ocompose @t23 @t53 @t53 @t27 (tptp.c_FuncSet_Orestrict @t53 @t53 @t290 @t21) @t2) @t2))))) % 0.54/0.94 (assume @p86 (forall (@list @t21 @t27 @t1 @t53 @t23) (=> (tptp.hBOOL (tptp.hAPP @t223 @t184)) (=> @t293 (= (tptp.c_FuncSet_Ocompose @t23 @t23 @t53 @t27 @t1 (tptp.c_FuncSet_Orestrict @t23 @t23 @t186 @t27)) @t1))))) % 0.54/0.94 (assume @p87 (forall (@list @t2 @t1 @t27 @t53 @t226 @t23) (= @t239 (tptp.c_FuncSet_Orestrict @t23 @t53 (tptp.hAPP (tptp.hAPP (tptp.c_COMBB @t226 @t53 @t23) @t1) @t2) @t27)))) % 0.54/0.94 (assume @p88 (forall @t295 (=> @t291 (= @t294 @t2)))) % 0.54/0.94 (assume @p89 (forall @t295 (tptp.hBOOL (tptp.hAPP @t296 @t240)))) % 0.54/0.94 (assume @p90 (forall @t193 (= (tptp.c_Transitive__Closure_Ortrancl @t23 @t241) @t241))) % 0.54/0.94 (assume @p91 (forall @t221 (=> @t220 (tptp.hBOOL (tptp.hAPP @t296 @t177))))) % 0.54/0.94 (assume @p92 (forall @t299 (tptp.c_Recdef_Oadm__wf @t23 @t53 @t52 @t298))) % 0.54/0.94 (assume @p93 (forall @t221 (=> @t222 (tptp.hBOOL (tptp.hAPP @t296 @t184))))) % 0.54/0.94 (assume @p94 (forall @t306 (=> (tptp.c_Relation_Osingle__valued @t23 @t23 @t142) (=> @t305 (=> @t303 (or (tptp.hBOOL (tptp.hAPP @t301 @t241)) (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t146 (tptp.hAPP (tptp.hAPP @t143 @t37) @t32)) @t241)))))))) % 0.54/0.94 (assume @p95 (forall (@list @t2 @t53 @t142 @t33 @t32 @t23) (and (=> @t310 (= @t308 @t311)) (=> (not @t310) (= @t308 @t307))))) % 0.54/0.94 (assume @p96 (forall (@list @t32 @t52 @t33 @t23) (=> (not (tptp.hBOOL (tptp.hAPP @t94 (tptp.c_Relation_ODomain @t23 @t23 @t52)))) (= @t313 @t40)))) % 0.54/0.94 (assume @p97 (forall (@list @t88 @t85 @t22 @t23 @t226 @t53) (= (tptp.hAPP (tptp.hAPP (tptp.c_Product__Type_Ointernal__split @t53 @t226 @t23) @t22) @t289) (tptp.hAPP (tptp.hAPP @t22 @t85) @t88)))) % 0.54/0.94 (assume @p98 (forall (@list @t32 @t33 @t22 @t23 @t226 @t53) (= (tptp.c_Product__Type_Ocurry @t53 @t226 @t23 @t22 @t33 @t32) (tptp.hAPP @t22 (tptp.hAPP (tptp.hAPP @t288 @t33) @t32))))) % 0.54/0.94 (assume @p99 (forall (@list @t88 @t85 @t53 @t23 @t2) (=> @t315 @t314))) % 0.54/0.94 (assume @p100 (forall (@list @t88 @t85 @t2 @t53 @t23) (=> @t314 @t315))) % 0.54/0.94 (assume @p101 (forall (@list @t88 @t85 @t2 @t23 @t226 @t53) (= (tptp.c_Product__Type_Ocurry @t53 @t226 @t23 @t2 @t85 @t88) (tptp.hAPP @t2 @t289)))) % 0.54/0.94 (assume @p102 (forall (@list @t2 @t53 @t27 @t33 @t23) (and (=> @t95 (= @t316 @t173)) (=> @t171 (= @t316 @t307))))) % 0.54/0.94 (assume @p103 (forall (@list @t33 @t27 @t2 @t53 @t23) (=> @t291 (=> @t171 @t317)))) % 0.54/0.94 (assume @p104 (forall @t321 (=> @t320 @t319))) % 0.54/0.94 (assume @p105 (forall @t323 (= @t319 (exists @t217 @t322)))) % 0.54/0.94 (assume @p106 (forall (@list @t37 @t32 @t33 @t142 @t53 @t23) (=> @t324 (=> (tptp.hBOOL (tptp.hAPP @t59 @t142)) (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t58 (tptp.hAPP @t55 @t37)) @t142)) @t42))))) % 0.54/0.94 (assume @p107 (forall @t328 (= @t324 @t327))) % 0.54/0.94 (assume @p108 (forall @t330 (= (tptp.c_Predicate_ODomainP @t23 @t53 @t329 @t33) (tptp.hBOOL (tptp.hAPP @t94 @t318))))) % 0.54/0.94 (assume @p109 (forall @t299 (= @t331 (forall (@list @t257 @t245 @t4) (=> (forall @t212 (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t146 (tptp.hAPP @t210 @t4)) @t52)) (= (tptp.hAPP @t257 @t209) @t246))) (= (tptp.hAPP (tptp.hAPP @t129 @t257) @t4) (tptp.hAPP @t250 @t4))))))) % 0.54/0.94 (assume @p110 (forall @t337 (=> @t336 (=> @t333 @t317)))) % 0.54/0.94 (assume @p111 (forall @t338 (=> @t236 (tptp.c_Predicate_ODomainP @t23 @t53 @t142 @t85)))) % 0.54/0.94 (assume @p112 (forall @t337 (=> @t336 (=> @t332 (tptp.hBOOL (tptp.hAPP @t175 @t334)))))) % 0.54/0.94 (assume @p113 (forall @t193 (= (tptp.c_Relation_Oirrefl @t23 @t142) (forall @t8 (not @t192))))) % 0.54/0.94 (assume @p114 (forall @t323 (=> @t319 (not (forall @t217 (not @t322)))))) % 0.54/0.94 (assume @p115 (forall @t321 (=> @t320 (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t174 @t88) @t339))))) % 0.54/0.94 (assume @p116 (forall @t341 (= (tptp.hBOOL (tptp.hAPP @t304 @t340)) (and @t40 @t95)))) % 0.54/0.94 (assume @p117 (forall @t91 (=> @t90 (=> @t87 (tptp.hBOOL (tptp.hAPP @t199 @t340)))))) % 0.54/0.94 (assume @p118 (forall (@list @t142 @t343 @t344 @t347 @t348 @t53 @t23) (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t64 (tptp.hAPP @t350 @t345)) @t342)) (=> (not (= @t349 @t345)) (not (forall @t136 (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t64 (tptp.hAPP @t350 @t267)) @t142)) (not (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t64 (tptp.hAPP @t346 @t345)) @t342)))))))))) % 0.54/0.94 (assume @p119 (forall @t366 (=> @t365 (=> @t363 (=> (forall (@list @t131 @t130 @t356 @t355) (=> @t362 (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t64 (tptp.hAPP (tptp.hAPP @t63 @t361) @t360)) @t342)) (=> @t357 @t354)))) @t353))))) % 0.54/0.94 (assume @p120 (forall @t188 (= (tptp.c_Relation_ORange @t23 @t23 @t340) @t27))) % 0.54/0.94 (assume @p121 (forall @t188 (= (tptp.c_Relation_ODomain @t23 @t23 @t340) @t27))) % 0.54/0.94 (assume @p122 (forall @t188 (tptp.c_Relation_Osingle__valued @t23 @t23 @t340))) % 0.54/0.94 (assume @p123 (forall @t323 (= (tptp.hBOOL (tptp.hAPP @t86 @t370)) (exists @t217 (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t369 (tptp.hAPP (tptp.hAPP @t367 @t213) @t85)) @t142)))))) % 0.54/0.94 (assume @p124 (forall @t330 (= (tptp.c_Predicate_ORangeP @t23 @t53 @t329 @t33) (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t174 @t33) @t339))))) % 0.54/0.94 (assume @p125 (forall (@list @t27 @t22 @t23) (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t146 @t22) @t340)) (not (forall @t8 (=> @t219 (not (= @t22 @t190)))))))) % 0.54/0.94 (assume @p126 (forall (@list @t142 @t53 @t88 @t23) (=> (tptp.hBOOL (tptp.hAPP @t89 @t370)) (not (forall @t8 (not (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t369 (tptp.hAPP (tptp.hAPP @t367 @t4) @t88)) @t142)))))))) % 0.54/0.94 (assume @p127 (forall @t366 (=> @t365 (=> @t353 (=> (forall @t136 (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t64 (tptp.hAPP @t364 @t267)) @t342)) (forall (@list @t356 @t355) (=> @t362 (=> @t354 @t357))))) @t363))))) % 0.54/0.94 (assume @p128 (forall (@list @t1 @t129 @t53 @t52 @t33 @t23) (=> (forall @t212 (=> @t211 (tptp.hBOOL (tptp.hAPP @t247 (tptp.hAPP @t1 @t209))))) (tptp.hBOOL (tptp.hAPP @t371 (tptp.hAPP (tptp.hAPP @t129 @t1) @t33)))))) % 0.54/0.94 (assume @p129 (forall @t256 (= (tptp.hBOOL (tptp.hAPP @t255 @t252)) (exists @t254 (and (= @t252 @t251) @t249))))) % 0.54/0.94 (assume @p130 (forall (@list @t1 @t27 @t2 @t53 @t23) (=> @t291 (=> @t293 (=> @t372 @t3))))) % 0.54/0.94 (assume @p131 (forall @t338 (=> @t236 (tptp.c_Predicate_ORangeP @t23 @t53 @t142 @t88)))) % 0.54/0.94 (assume @p132 (forall (@list @t252 @t142 @t53 @t23) (= (tptp.c_Predicate_ORangeP @t23 @t53 @t142 @t252) (exists (@list @t131) (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t142 @t131) @t252)))))) % 0.54/0.94 (assume @p133 (forall @t328 (=> @t327 @t324))) % 0.54/0.94 (assume @p134 (forall (@list @t334 @t116 @t53 @t23) (= @t335 (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t373 (tptp.c_FuncSet_OPi @t23 @t53 @t116 (tptp.c_COMBK @t121 @t23 @t334)) (tptp.c_FuncSet_Oextensional @t23 @t53 @t116))))) % 0.54/0.94 (assume @p135 (forall @t380 (=> @t284 (=> @t379 (=> (forall @t217 (=> @t378 (forall @t212 (=> @t377 (=> @t376 @t375))))) @t374))))) % 0.54/0.94 (assume @p136 (forall @t380 (=> @t284 (=> @t374 (=> (forall (@list @t213 @t209) (=> @t377 (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t146 (tptp.hAPP @t210 @t88)) @t241)) (=> @t375 @t376)))) @t379))))) % 0.54/0.94 (assume @p137 (forall @t383 (=> @t303 (=> @t39 (not (forall @t217 (=> @t382 (not (tptp.hBOOL (tptp.hAPP @t381 @t241)))))))))) % 0.54/0.94 (assume @p138 (forall @t384 (=> @t284 (=> @t114 (not (forall @t217 (=> @t378 (not (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t146 (tptp.hAPP @t215 @t88)) @t142)))))))))) % 0.54/0.94 (assume @p139 (forall @t388 (=> @t387 (not (=> @t98 (not @t385)))))) % 0.54/0.94 (assume @p140 (forall (@list @t23 @t21 @t33 @t27) (=> @t98 (=> @t385 @t387)))) % 0.54/0.94 (assume @p141 (forall @t390 (=> @t389 (not @t29)))) % 0.54/0.94 (assume @p142 (forall @t390 (=> @t28 (=> @t26 @t389)))) % 0.54/0.94 (assume @p143 (forall @t388 (=> @t387 @t385))) % 0.54/0.94 (assume @p144 (forall @t388 (=> @t387 @t98))) % 0.54/0.94 (assume @p145 (forall @t393 (= (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t163 @t386 @t225) @t392))) % 0.54/0.94 (assume @p146 (forall @t393 (= @t392 (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t163 @t21 (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t163 @t27 @t225))))) % 0.54/0.94 (assume @p147 (forall @t394 (= (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t163 @t27 @t386) @t386))) % 0.54/0.94 (assume @p148 (forall @t394 (= @t386 (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t163 @t21 @t27)))) % 0.54/0.94 (assume @p149 (forall @t188 (= (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t163 @t27 @t27) @t27))) % 0.54/0.94 (assume @p150 (forall @t390 (=> @t389 @t26))) % 0.54/0.94 (assume @p151 (forall @t390 (=> @t389 @t28))) % 0.54/0.94 (assume @p152 (forall @t390 (= @t389 (and @t28 @t26)))) % 0.54/0.94 (assume @p153 (forall (@list @t33 @t116 @t52 @t23) (= (tptp.hBOOL (tptp.hAPP (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t163 @t166 @t165) @t33)) (tptp.hBOOL (tptp.hAPP @t94 (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t163 @t52 @t116)))))) % 0.54/0.94 (assume @p154 (forall (@list @t33 @t1 @t2 @t53 @t23) (=> @t397 (= (tptp.hAPP (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t396 @t2 @t1) @t33) (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t23 @t173 @t395))))) % 0.54/0.94 (assume @p155 (forall (@list @t142 @t27 @t23) (= (tptp.c_Relation_Ototal__on @t23 @t27 @t142) (forall @t8 (=> @t219 (forall @t137 (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t24 @t128) @t27)) (=> (not (= @t4 @t128)) (or (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t146 (tptp.hAPP @t189 @t128)) @t142)) (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t146 (tptp.hAPP (tptp.hAPP @t143 @t128) @t4)) @t142))))))))))) % 0.54/0.94 (assume @p156 (forall (@list @t2 @t142 @t53 @t32 @t33 @t23) (= (tptp.hBOOL (tptp.hAPP @t304 (tptp.hAPP (tptp.hAPP (tptp.c_Relation_Oinv__image @t53 @t23) @t142) @t2))) (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t67 (tptp.hAPP (tptp.hAPP @t65 @t173) @t311)) @t142))))) % 0.54/0.94 (assume @p157 (forall @t400 (=> @t399 (=> @t398 @t93)))) % 0.54/0.94 (assume @p158 (forall @t400 (=> @t399 (=> @t398 @t95)))) % 0.54/0.94 (assume @p159 (forall (@list @t32 @t33 @t116 @t52 @t53 @t23) (= (tptp.hBOOL (tptp.hAPP (tptp.hAPP (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t401 @t124 @t123) @t33) @t32)) (tptp.hBOOL (tptp.hAPP @t59 (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t118 @t52 @t116)))))) % 0.54/0.94 (assume @p160 (forall (@list @t140 @t21 @t142 @t27 @t23) (=> @t399 (=> (tptp.c_Relation_Orefl__on @t23 @t21 @t140) (tptp.c_Relation_Orefl__on @t23 @t386 (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t203 @t142 @t140)))))) % 0.54/0.94 (assume @p161 (forall @t188 (tptp.c_Relation_Orefl__on @t23 @t27 @t340))) % 0.54/0.94 (assume @p162 (forall @t410 (=> @t409 @t408))) % 0.54/0.94 (assume @p163 (forall @t410 (=> @t397 @t408))) % 0.54/0.94 (assume @p164 (forall @t414 (=> @t409 (= (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t23 @t413 @t411) @t412)))) % 0.54/0.94 (assume @p165 (forall @t410 (=> @t409 @t415))) % 0.54/0.94 (assume @p166 (forall @t410 (=> @t397 @t415))) % 0.54/0.94 (assume @p167 (forall @t416 (=> @t409 (= (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t23 @t271 (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t23 @t273 @t411)) @t412)))) % 0.54/0.94 (assume @p168 (forall @t418 (=> @t409 @t417))) % 0.54/0.94 (assume @p169 (forall @t418 (=> @t397 @t417))) % 0.54/0.94 (assume @p170 (forall @t419 (=> @t409 (= (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t23 @t273 @t413) @t413)))) % 0.54/0.94 (assume @p171 (forall @t418 (=> @t409 @t420))) % 0.54/0.94 (assume @p172 (forall @t418 (=> @t397 @t420))) % 0.54/0.94 (assume @p173 (forall @t419 (=> @t409 (= @t413 (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t23 @t271 @t273))))) % 0.54/0.94 (assume @p174 (forall @t422 (=> @t409 @t421))) % 0.54/0.94 (assume @p175 (forall (@list @t273 @t23) (=> @t409 (= (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t23 @t273 @t273) @t273)))) % 0.54/0.94 (assume @p176 (forall (@list @t85 @t142 @t27 @t23) (=> @t399 (=> @t87 @t423)))) % 0.54/0.94 (assume @p177 (forall @t384 (=> @t425 @t284))) % 0.54/0.94 (assume @p178 (forall @t427 (= (tptp.hBOOL (tptp.hAPP (tptp.hAPP (tptp.c_Transitive__Closure_Ortranclp @t23 @t206) @t33) @t348)) (tptp.hBOOL (tptp.hAPP @t426 @t241))))) % 0.54/0.94 (assume @p179 (forall @t429 (= (tptp.c_Nitpick_Owf__wfrec_H @t53 @t23 @t52 @t129 @t33) (tptp.hAPP (tptp.hAPP @t129 (tptp.hAPP (tptp.hAPP (tptp.hAPP @t428 (tptp.c_Nitpick_Owf__wfrec @t53 @t23 @t52 @t129)) @t52) @t33)) @t33)))) % 0.54/0.94 (assume @p180 (forall @t422 (=> @t397 @t421))) % 0.54/0.94 (assume @p181 (forall @t431 (tptp.hBOOL (tptp.hAPP @t274 @t430)))) % 0.54/0.94 (assume @p182 (forall (@list @t53 @t1 @t2 @t27 @t23) (=> @t372 (= @t294 (tptp.c_FuncSet_Orestrict @t23 @t53 @t1 @t27))))) % 0.54/0.94 (assume @p183 (forall (@list @t23 @t32 @t33 @t142) (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t142 @t33) @t32)) @t434))) % 0.54/0.94 (assume @p184 (forall @t235 (tptp.hBOOL (tptp.hAPP @t435 @t85)))) % 0.54/0.94 (assume @p185 (forall @t439 (=> @t438 (not (=> @t437 (not @t436)))))) % 0.54/0.94 (assume @p186 (forall (@list @t53 @t23 @t21 @t32 @t33 @t27) (=> @t437 (=> @t436 @t438)))) % 0.54/0.94 (assume @p187 (forall @t384 (=> @t200 @t425))) % 0.54/0.94 (assume @p188 (forall @t193 (= (tptp.c_Transitive__Closure_Ortranclp @t23 (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t440 @t142 (tptp.hAPP (tptp.hAPP (tptp.c_COMBB @t163 @t163 @t23) (tptp.hAPP (tptp.c_COMBB tptp.tc_HOL_Obool tptp.tc_HOL_Obool @t23) tptp.c_fNot)) tptp.c_fequal))) @t432))) % 0.54/0.94 (assume @p189 (forall @t439 (=> @t438 @t436))) % 0.54/0.94 (assume @p190 (forall @t439 (=> @t438 @t437))) % 0.54/0.94 (assume @p191 (forall @t306 (=> @t434 (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t432 @t32) @t37)) (tptp.hBOOL (tptp.hAPP @t433 @t37)))))) % 0.54/0.94 (assume @p192 (forall @t444 (=> @t443 (=> @t442 @t441)))) % 0.54/0.94 (assume @p193 (forall @t447 (=> @t236 (=> @t446 @t441)))) % 0.54/0.94 (assume @p194 (forall @t453 (= (tptp.hBOOL (tptp.hAPP @t451 @t448)) (or (= @t448 @t248) (exists @t452 (and (tptp.hBOOL (tptp.hAPP @t451 @t130)) @t450)))))) % 0.54/0.94 (assume @p195 (forall @t193 (= (tptp.c_Transitive__Closure_Ortranclp @t23 @t432) @t432))) % 0.54/0.94 (assume @p196 (forall @t278 (=> @t277 @t454))) % 0.54/0.94 (assume @p197 (forall @t456 (= (tptp.c_Transitive__Closure_Ortrancl @t23 @t455) @t312))) % 0.54/0.94 (assume @p198 (forall @t456 (= (tptp.c_Transitive__Closure_Otrancl @t23 @t312) @t312))) % 0.54/0.94 (assume @p199 (forall @t193 (= (tptp.c_Relation_ODomain @t23 @t23 @t424) (tptp.c_Relation_ODomain @t23 @t23 @t142)))) % 0.54/0.94 (assume @p200 (forall @t193 (= (tptp.c_Relation_ORange @t23 @t23 @t424) (tptp.c_Relation_ORange @t23 @t23 @t142)))) % 0.54/0.94 (assume @p201 (forall @t238 (=> @t457 (=> @t234 @t237)))) % 0.54/0.94 (assume @p202 (forall @t458 (=> @t234 (=> @t457 @t237)))) % 0.54/0.94 (assume @p203 (forall @t459 (tptp.c_Relation_Osingle__valued @t23 @t23 @t430))) % 0.54/0.94 (assume @p204 (forall @t285 (=> @t425 @t461))) % 0.54/0.94 (assume @p205 (forall @t285 (=> @t425 @t462))) % 0.54/0.94 (assume @p206 (forall @t285 (=> @t200 @t461))) % 0.54/0.94 (assume @p207 (forall (@list @t22 @t52 @t88 @t85 @t23) (=> (tptp.hBOOL (tptp.hAPP @t199 @t52)) (=> (tptp.hBOOL (tptp.hAPP @t281 @t52)) (tptp.hBOOL (tptp.hAPP @t279 @t455)))))) % 0.54/0.94 (assume @p208 (forall (@list @t88 @t85 @t23) (= (tptp.hBOOL (tptp.hAPP @t199 @t430)) @t90))) % 0.54/0.94 (assume @p209 (forall (@list @t37 @t142 @t32 @t33 @t23) (=> @t305 (=> (tptp.hBOOL (tptp.hAPP @t301 @t424)) @t463)))) % 0.54/0.94 (assume @p210 (forall @t285 (=> @t425 @t464))) % 0.54/0.94 (assume @p211 (forall @t285 (=> @t284 @t462))) % 0.54/0.94 (assume @p212 (forall (@list @t52 @t88 @t85 @t23) (=> (tptp.hBOOL (tptp.hAPP @t199 @t312)) (or @t90 (and @t114 (tptp.hBOOL (tptp.hAPP @t199 @t455))))))) % 0.54/0.94 (assume @p213 (forall @t285 (=> @t200 @t464))) % 0.54/0.94 (assume @p214 (forall @t466 (= @t313 (or @t40 (and @t41 @t465))))) % 0.54/0.94 (assume @p215 (forall @t466 (=> @t465 (exists @t212 (and (tptp.hBOOL (tptp.hAPP @t468 @t52)) (tptp.hBOOL (tptp.hAPP @t467 @t312))))))) % 0.54/0.94 (assume @p216 (forall @t466 (=> @t465 (exists @t212 (and (tptp.hBOOL (tptp.hAPP @t468 @t312)) (tptp.hBOOL (tptp.hAPP @t467 @t52))))))) % 0.54/0.94 (assume @p217 (forall (@list @t275 @t23) (=> (tptp.hBOOL (tptp.hAPP @t276 @t430)) (not (forall @t8 (not (= @t275 @t190))))))) % 0.54/0.94 (assume @p218 (forall @t193 (= @t470 @t469))) % 0.54/0.94 (assume @p219 (forall @t384 (=> @t425 (=> (not @t200) (not (forall (@list @t471) (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t146 (tptp.hAPP @t144 @t471)) @t424)) (not (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t146 (tptp.hAPP (tptp.hAPP @t143 @t471) @t88)) @t142)))))))))) % 0.54/0.94 (assume @p220 (forall @t193 (=> @t469 @t470))) % 0.54/0.94 (assume @p221 (forall @t474 (= (tptp.c_Wellfounded_Oacyclic @t23 @t473) (and @t470 @t472)))) % 0.54/0.94 (assume @p222 (forall (@list @t32 @t33 @t142 @t23) (=> @t469 (=> @t398 @t41)))) % 0.54/0.94 (assume @p223 (forall @t383 (=> @t463 (=> (not (tptp.hBOOL (tptp.hAPP @t302 @t142))) (not (forall @t217 (=> @t382 (not (tptp.hBOOL (tptp.hAPP @t381 @t424)))))))))) % 0.54/0.94 (assume @p224 (forall @t476 (=> @t475 (=> @t114 @t87)))) % 0.54/0.94 (assume @p225 (forall @t480 (=> (=> (not @t479) @t90) @t478))) % 0.54/0.94 (assume @p226 (forall @t321 (= (tptp.c_Relation_ODomain @t23 @t53 (tptp.c_Set_Oinsert @t57 @t149 @t142)) (tptp.c_Set_Oinsert @t23 @t85 @t318)))) % 0.54/0.94 (assume @p227 (forall (@list @t142 @t88 @t85 @t23 @t53) (= (tptp.c_Relation_ORange @t53 @t23 (tptp.c_Set_Oinsert @t368 (tptp.hAPP (tptp.hAPP @t367 @t85) @t88) @t142)) (tptp.c_Set_Oinsert @t23 @t88 @t370)))) % 0.54/0.94 (assume @p228 (forall (@list @t33 @t27 @t32 @t23) (= (tptp.hBOOL (tptp.hAPP @t481 @t33)) (or (= @t32 @t33) @t98)))) % 0.54/0.94 (assume @p229 (forall @t341 (= (tptp.c_Set_Oinsert @t23 @t33 @t481) (tptp.c_Set_Oinsert @t23 @t32 @t482)))) % 0.54/0.94 (assume @p230 (forall @t99 (= (tptp.c_Set_Oinsert @t23 @t33 @t482) @t482))) % 0.54/0.94 (assume @p231 (forall @t486 (= (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t163 @t485 @t484) @t483))) % 0.54/0.94 (assume @p232 (forall (@list @t21 @t85 @t23) (tptp.hBOOL (tptp.hAPP @t86 @t484)))) % 0.54/0.94 (assume @p233 (forall @t476 (= @t475 (or @t90 @t87)))) % 0.54/0.94 (assume @p234 (forall @t488 (=> @t171 (=> (not @t96) (= (= @t482 @t487) @t30))))) % 0.54/0.94 (assume @p235 (forall @t480 (=> @t479 @t478))) % 0.54/0.94 (assume @p236 (forall (@list @t27 @t85 @t23) (=> @t87 (= @t485 @t27)))) % 0.54/0.94 (assume @p237 (forall @t486 (and @t492 @t491))) % 0.54/0.94 (assume @p238 (forall @t497 (and @t496 @t495))) % 0.54/0.94 (assume @p239 (forall @t486 @t491)) % 0.54/0.94 (assume @p240 (forall @t497 @t495)) % 0.54/0.94 (assume @p241 (forall @t486 @t492)) % 0.54/0.94 (assume @p242 (forall @t497 @t496)) % 0.54/0.94 (assume @p243 (forall (@list @t334 @t2 @t53 @t116 @t33 @t23) (=> @t333 (=> (tptp.hBOOL (tptp.hAPP @t180 (tptp.c_FuncSet_Oextensional__funcset @t23 @t53 (tptp.c_Set_Oinsert @t23 @t33 @t116) @t334))) (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t179 (tptp.c_Fun_Ofun__upd @t23 @t53 @t2 @t33 @t307)) @t335)))))) % 0.54/0.94 (assume @p244 (forall (@list @t33 @t116 @t2 @t53 @t334 @t32 @t23) (=> (tptp.hBOOL (tptp.hAPP @t92 @t334)) (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t499 @t2) (tptp.c_FuncSet_Oextensional__funcset @t53 @t23 @t116 @t334))) (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t499 @t498) (tptp.c_FuncSet_Oextensional__funcset @t53 @t23 (tptp.c_Set_Oinsert @t53 @t33 @t116) @t334))))))) % 0.54/0.94 (assume @p245 (forall @t474 (= (tptp.c_Wellfounded_Owf @t23 @t473) (and @t500 @t472)))) % 0.54/0.94 (assume @p246 (forall @t427 (= (tptp.hBOOL (tptp.hAPP (tptp.hAPP (tptp.c_Transitive__Closure_Otranclp @t23 @t206) @t33) @t348)) (tptp.hBOOL (tptp.hAPP @t426 @t424))))) % 0.54/0.94 (assume @p247 (forall (@list @t23 @t88 @t85 @t142) (=> @t236 @t503))) % 0.54/0.94 (assume @p248 (forall (@list @t2 @t53 @t142 @t23) (=> @t500 (tptp.c_Wellfounded_Owf @t53 (tptp.hAPP (tptp.hAPP @t504 @t142) @t2))))) % 0.54/0.94 (assume @p249 (forall (@list @t505 @t53 @t506 @t23) (=> (tptp.c_Wellfounded_Owf @t23 @t506) (=> (tptp.c_Wellfounded_Owf @t53 @t505) (tptp.c_Wellfounded_Owf @t57 (tptp.c_Wellfounded_Olex__prod @t23 @t53 @t506 @t505)))))) % 0.54/0.94 (assume @p250 (forall @t508 (=> @t500 (tptp.c_Wellfounded_Owf @t23 (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t203 @t507 @t142))))) % 0.54/0.94 (assume @p251 (forall @t508 (=> @t500 (tptp.c_Wellfounded_Owf @t23 (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t203 @t142 @t507))))) % 0.54/0.94 (assume @p252 (forall (@list @t252 @t248 @t142 @t23) (= (tptp.hBOOL (tptp.hAPP @t509 @t252)) (or (tptp.hBOOL (tptp.hAPP @t511 @t252)) (exists @t452 (and @t510 (tptp.hBOOL (tptp.hAPP @t449 @t252)))))))) % 0.54/0.94 (assume @p253 (forall @t453 (= (tptp.hBOOL (tptp.hAPP @t509 @t448)) (or (tptp.hBOOL (tptp.hAPP @t511 @t448)) (exists @t452 (and @t510 @t450)))))) % 0.54/0.94 (assume @p254 (forall @t447 (=> @t236 (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t501 @t88) @t22)) @t512)))) % 0.54/0.94 (assume @p255 (forall @t444 (=> @t503 @t513))) % 0.54/0.94 (assume @p256 (forall @t306 (=> (tptp.hBOOL (tptp.hAPP @t514 @t32)) @t515))) % 0.54/0.94 (assume @p257 (forall @t193 (=> @t500 (tptp.c_Wellfounded_Owf @t23 @t424)))) % 0.54/0.94 (assume @p258 (forall @t447 (=> @t236 @t516))) % 0.54/0.94 (assume @p259 (forall (@list @t88 @t85 @t52 @t23) (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t517 @t85) @t88)) (or @t90 (and @t114 (tptp.hBOOL (tptp.hAPP (tptp.hAPP (tptp.c_Transitive__Closure_Otranclp @t23 @t52) @t85) @t88))))))) % 0.54/0.94 (assume @p260 (forall @t458 (=> @t503 @t443))) % 0.54/0.94 (assume @p261 (forall @t444 (=> @t443 @t513))) % 0.54/0.94 (assume @p262 (forall @t444 (=> @t503 @t516))) % 0.54/0.94 (assume @p263 (forall @t306 (=> @t434 @t515))) % 0.54/0.94 (assume @p264 (forall @t193 (=> @t500 @t470))) % 0.54/0.94 (assume @p265 (forall @t235 (=> @t500 (not @t423)))) % 0.54/0.94 (assume @p266 (forall (@list @t33 @t85 @t142 @t23) (=> @t500 (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t146 (tptp.hAPP @t144 @t33)) @t142)) (not @t265))))) % 0.54/0.94 (assume @p267 (forall @t193 (= @t500 @t518))) % 0.54/0.94 (assume @p268 (forall @t207 (=> @t500 @t202))) % 0.54/0.94 (assume @p269 (forall (@list @t33 @t2 @t53 @t23) (= (tptp.c_Fun_Ofun__upd @t23 @t53 @t2 @t33 @t173) @t2))) % 0.54/0.94 (assume @p270 (forall (@list @t2 @t23) (tptp.c_Wellfounded_Owf @t23 @t520))) % 0.54/0.94 (assume @p271 (forall (@list @t33 @t129 @t53 @t52 @t23) (and (=> @t522 (= @t521 (tptp.c_Nitpick_Owf__wfrec_H @t23 @t53 @t52 @t129 @t33))) (=> (not @t522) (= @t521 (tptp.c_HOL_OThe @t53 (tptp.c_Recdef_Owfrec__rel @t23 @t53 @t52 @t298 @t33))))))) % 0.54/0.94 (assume @p272 (forall (@list @t85 @t523 @t142 @t53 @t23 @t2) (=> (= @t2 @t525) (=> @t500 (= @t524 (tptp.hAPP (tptp.hAPP @t523 @t264) @t85)))))) % 0.54/0.94 (assume @p273 (forall @t429 (= (tptp.hAPP (tptp.c_Recdef_Owfrec @t53 @t23 @t52 @t129) @t33) (tptp.c_HOL_OThe @t23 (tptp.c_Recdef_Owfrec__rel @t53 @t23 @t52 (tptp.hAPP (tptp.hAPP (tptp.c_COMBC @t396 @t528 @t396) (tptp.hAPP (tptp.hAPP (tptp.c_COMBB @t526 (tptp.tc_fun @t528 @t396) @t396) (tptp.c_COMBS @t53 @t53 @t23)) (tptp.hAPP (tptp.hAPP (tptp.c_COMBB @t526 @t526 @t396) (tptp.hAPP (tptp.c_COMBB @t396 @t396 @t53) @t129)) (tptp.hAPP (tptp.hAPP (tptp.c_COMBC @t396 @t527 @t526) @t428) @t52)))) @t290) @t33))))) % 0.54/0.94 (assume @p274 (forall (@list @t32 @t33 @t2 @t53 @t23) (= (= @t530 @t2) @t529))) % 0.54/0.94 (assume @p275 (forall (@list @t37 @t32 @t33 @t2 @t53 @t23) (= (tptp.c_Fun_Ofun__upd @t23 @t53 @t530 @t33 @t37) (tptp.c_Fun_Ofun__upd @t23 @t53 @t2 @t33 @t37)))) % 0.54/0.94 (assume @p276 (forall (@list @t32 @t33 @t2 @t23 @t53) (= (tptp.hAPP @t498 @t33) @t32))) % 0.54/0.94 (assume @p277 (forall @t534 (and (=> @t532 (= @t531 @t32)) @t533))) % 0.54/0.94 (assume @p278 (forall (@list @t535 @t88 @t536 @t53 @t23 @t22 @t85) (=> (not (= @t85 @t22)) (= (tptp.c_Fun_Ofun__upd @t23 @t53 (tptp.c_Fun_Ofun__upd @t23 @t53 @t536 @t85 @t88) @t22 @t535) (tptp.c_Fun_Ofun__upd @t23 @t53 (tptp.c_Fun_Ofun__upd @t23 @t53 @t536 @t22 @t535) @t85 @t88))))) % 0.54/0.94 (assume @p279 (forall @t534 @t533)) % 0.54/0.94 (assume @p280 (forall (@list @t23 @t53 @t32 @t33 @t2) (=> @t529 (= @t498 @t2)))) % 0.54/0.94 (assume @p281 (forall (@list @t88 @t2 @t53 @t23 @t85 @t33) (and (=> @t154 (= @t537 @t88)) (=> @t155 (= @t537 @t173))))) % 0.54/0.94 (assume @p282 (forall (@list @t53 @t23 @t538 @t258) (=> (tptp.c_Wellfounded_Owf @t23 @t258) (forall @t8 (= (tptp.hAPP @t539 @t4) (tptp.hAPP (tptp.hAPP @t538 (tptp.hAPP (tptp.hAPP (tptp.hAPP @t259 @t539) @t258) @t4)) @t4)))))) % 0.54/0.94 (assume @p283 (forall (@list @t85 @t523 @t53 @t142 @t23) (=> @t500 (= (tptp.hAPP @t525 @t85) (tptp.hAPP (tptp.hAPP @t523 (tptp.hAPP (tptp.hAPP (tptp.hAPP @t259 @t525) @t142) @t85)) @t85))))) % 0.54/0.94 (assume @p284 (forall (@list @t23 @t52 @t53 @t60) (=> (forall @t8 (=> (tptp.hBOOL (tptp.hAPP @t60 @t4)) (tptp.c_Wellfounded_Owf @t53 (tptp.hAPP @t52 @t4)))) (tptp.c_Wellfounded_Owf @t57 @t61)))) % 0.54/0.94 (assume @p285 (forall (@list @t33 @t23) (= (tptp.c_HOL_OThe @t23 @t540) @t33))) % 0.54/0.94 (assume @p286 (forall @t431 (= (tptp.c_HOL_OThe @t23 (tptp.hAPP (tptp.hAPP (tptp.c_COMBC @t23 @t23 tptp.tc_HOL_Obool) tptp.c_fequal) @t85)) @t85))) % 0.54/0.94 (assume @p287 (forall (@list @t33 @t129 @t52 @t53 @t23) (=> @t331 (=> @t522 (exists @t8 (and (tptp.hBOOL (tptp.hAPP @t371 @t4)) (forall @t217 (=> (tptp.hBOOL (tptp.hAPP @t371 @t213)) (= @t213 @t4))))))))) % 0.54/0.94 (assume @p288 (forall @t193 (= (tptp.c_Wellfounded_OwfP @t23 @t206) @t500))) % 0.54/0.94 (assume @p289 (forall @t193 (= @t500 (forall (@list @t541) (=> (exists @t8 @t543) (exists @t8 (and @t543 (forall @t217 (=> @t542 (not (tptp.hBOOL (tptp.hAPP @t214 @t541)))))))))))) % 0.54/0.94 (assume @p290 (forall @t459 (tptp.c_Wellfounded_OwfP @t23 (tptp.c_COMBK @t163 @t23 (tptp.c_COMBK tptp.tc_HOL_Obool @t23 tptp.c_fFalse))))) % 0.54/0.94 (assume @p291 (forall @t207 (=> @t544 (tptp.hBOOL (tptp.hAPP @t233 @t33))))) % 0.54/0.94 (assume @p292 (forall @t193 (= @t544 (forall @t269 (tptp.hBOOL (tptp.hAPP @t233 @t268)))))) % 0.54/0.94 (assume @p293 (forall @t193 (=> @t544 (tptp.c_Wellfounded_OwfP @t23 @t501)))) % 0.54/0.94 (assume @p294 (forall @t456 (=> @t522 (tptp.c_Wellfounded_OwfP @t23 (tptp.c_FunDef_Oin__rel @t23 @t23 @t52))))) % 0.54/0.94 (assume @p295 (forall (@list @t33 @t2 @t27 @t53 @t23) (= (tptp.c_Fun_Othe__inv__into @t23 @t53 @t27 @t2 @t33) (tptp.c_HOL_OThe @t23 (tptp.hAPP (tptp.hAPP (tptp.c_COMBS @t23 tptp.tc_HOL_Obool tptp.tc_HOL_Obool) (tptp.hAPP (tptp.hAPP (tptp.c_COMBB tptp.tc_HOL_Obool (tptp.tc_fun tptp.tc_HOL_Obool tptp.tc_HOL_Obool) @t23) tptp.c_fconj) (tptp.hAPP @t164 @t27))) (tptp.hAPP (tptp.hAPP (tptp.c_COMBC @t23 @t53 tptp.tc_HOL_Obool) (tptp.hAPP (tptp.hAPP (tptp.c_COMBB @t53 @t121 @t23) tptp.c_fequal) @t2)) @t33)))))) % 0.54/0.94 (assume @p296 (forall @t193 (=> @t518 @t500))) % 0.54/0.94 (assume @p297 (forall (@list @t2 @t32 @t33 @t23) (= (tptp.hBOOL (tptp.hAPP @t304 @t520)) @t545))) % 0.54/0.94 (assume @p298 (forall @t547 (=> @t409 (=> (tptp.c_Orderings_Oord__class_Oless @t23 @t271 @t405) @t546)))) % 0.54/0.94 (assume @p299 (forall @t548 (=> @t409 (=> (tptp.c_Orderings_Oord__class_Oless @t23 @t273 @t405) @t546)))) % 0.54/0.94 (assume @p300 (forall @t551 (=> @t545 @t550))) % 0.54/0.94 (assume @p301 (forall @t555 (and @t554 @t553))) % 0.54/0.94 (assume @p302 (forall @t459 (= @t519 (tptp.hAPP (tptp.c_Relation_Oinv__image tptp.tc_Nat_Onat @t23) tptp.c_Wellfounded_Oless__than)))) % 0.54/0.94 (assume @p303 (tptp.c_Wellfounded_Owf tptp.tc_Nat_Onat tptp.c_Wellfounded_Oless__than)) % 0.54/0.94 (assume @p304 (forall @t558 (=> @t557 @t556))) % 0.54/0.94 (assume @p305 (forall (@list @t52 @t2 @t23) (= @t549 (tptp.hAPP (tptp.hAPP (tptp.c_Relation_Oinv__image @t559 @t23) (tptp.c_Wellfounded_Olex__prod tptp.tc_Nat_Onat @t23 tptp.c_Wellfounded_Oless__than @t52)) (tptp.hAPP (tptp.hAPP (tptp.c_COMBS @t23 @t23 @t559) (tptp.hAPP (tptp.hAPP (tptp.c_COMBB tptp.tc_Nat_Onat (tptp.tc_fun @t23 @t559) @t23) (tptp.c_Product__Type_OPair tptp.tc_Nat_Onat @t23)) @t2)) @t186))))) % 0.54/0.94 (assume @p306 (forall @t563 (= (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t562 (tptp.hAPP (tptp.hAPP @t560 @t33) @t32)) tptp.c_Wellfounded_Oless__than)) (tptp.c_Orderings_Oord__class_Oless tptp.tc_Nat_Onat @t33 @t32)))) % 0.54/0.94 (assume @p307 (forall @t555 @t553)) % 0.54/0.94 (assume @p308 (forall @t555 @t554)) % 0.54/0.94 (assume @p309 (forall (@list @t2 @t52 @t23) (=> @t522 (tptp.c_Wellfounded_Owf @t23 @t549)))) % 0.54/0.94 (assume @p310 (= tptp.c_Wellfounded_Oless__than @t564)) % 0.54/0.94 (assume @p311 (forall @t551 (=> (tptp.c_Orderings_Oord__class_Oless__eq tptp.tc_Nat_Onat @t173 @t311) (=> (tptp.hBOOL (tptp.hAPP @t304 @t52)) @t550)))) % 0.54/0.94 (assume @p312 (forall @t193 (=> @t470 (tptp.c_Relation_Oantisym @t23 @t241)))) % 0.54/0.94 (assume @p313 (forall @t566 (=> @t565 (tptp.c_Orderings_Oord__class_Oless__eq tptp.tc_Nat_Onat @t405 @t403)))) % 0.54/0.94 (assume @p314 (forall @t393 (=> @t557 @t568))) % 0.54/0.94 (assume @p315 (tptp.c_Wellfounded_Owf tptp.tc_Nat_Onat tptp.c_Wellfounded_Opred__nat)) % 0.54/0.94 (assume @p316 (forall @t572 (= (tptp.hBOOL (tptp.hAPP @t571 (tptp.c_Transitive__Closure_Ortrancl tptp.tc_Nat_Onat tptp.c_Wellfounded_Opred__nat))) @t570))) % 0.54/0.94 (assume @p317 (forall @t576 (=> @t409 (=> @t575 (not (=> @t574 (not @t573))))))) % 0.54/0.94 (assume @p318 (forall (@list @t577 @t271 @t411 @t273 @t23) (=> @t409 (=> @t578 (=> (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t271 @t577) (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t413 (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t23 @t411 @t577))))))) % 0.54/0.94 (assume @p319 (forall @t410 (=> @t409 (=> @t580 (=> @t579 (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t405 @t404)))))) % 0.54/0.94 (assume @p320 (forall @t576 (=> @t409 (=> @t574 (=> @t573 @t575))))) % 0.54/0.94 (assume @p321 (forall @t582 (=> @t409 (=> @t581 (= @t407 @t403))))) % 0.54/0.94 (assume @p322 (forall @t418 (=> @t409 (=> @t580 (= @t407 @t405))))) % 0.54/0.94 (assume @p323 (forall @t547 (=> @t409 (=> (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t271 @t405) @t583)))) % 0.54/0.94 (assume @p324 (forall @t548 (=> @t409 (=> (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t273 @t405) @t583)))) % 0.54/0.94 (assume @p325 (forall (@list @t37 @t32 @t33 @t23) (=> @t409 (= (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t33 (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t23 @t32 @t37)) (and @t584 (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t33 @t37)))))) % 0.54/0.94 (assume @p326 (forall @t170 (=> @t409 (= @t584 (= (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t23 @t33 @t32) @t33))))) % 0.54/0.94 (assume @p327 (forall @t418 (=> @t409 @t585))) % 0.54/0.94 (assume @p328 (forall @t418 (=> @t397 @t585))) % 0.54/0.94 (assume @p329 (forall @t418 (=> @t409 @t586))) % 0.54/0.94 (assume @p330 (forall @t418 (=> @t397 @t586))) % 0.54/0.94 (assume @p331 (forall @t459 (tptp.c_Relation_Oantisym @t23 @t430))) % 0.54/0.94 (assume @p332 (forall @t188 (tptp.c_Relation_Oantisym @t23 @t340))) % 0.54/0.94 (assume @p333 (forall @t572 (= (tptp.hBOOL (tptp.hAPP @t571 @t564)) @t587))) % 0.54/0.94 (assume @p334 (forall @t193 (= @t588 (forall @t326 (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t146 (tptp.hAPP @t189 @t213)) @t142)) (=> @t542 (= @t4 @t213))))))) % 0.54/0.94 (assume @p335 (forall @t458 (=> @t588 (=> @t200 (=> (tptp.hBOOL (tptp.hAPP @t243 @t142)) @t90))))) % 0.54/0.94 (assume @p336 (forall @t422 (=> @t589 (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t405 @t405)))) % 0.54/0.94 (assume @p337 (forall @t595 (=> (or @t594 @t593) @t592))) % 0.54/0.94 (assume @p338 (forall @t595 (=> @t592 (=> @t596 @t594)))) % 0.54/0.94 (assume @p339 (forall @t558 (=> @t597 @t556))) % 0.54/0.94 (assume @p340 (forall @t394 (= @t557 (and @t597 (not @t30))))) % 0.54/0.94 (assume @p341 (forall @t394 (= @t597 (or @t557 @t30)))) % 0.54/0.94 (assume @p342 (forall @t394 (=> @t557 @t597))) % 0.54/0.94 (assume @p343 (forall @t393 (=> @t557 (=> @t598 @t567)))) % 0.54/0.94 (assume @p344 (forall @t393 (=> @t597 @t568))) % 0.54/0.94 (assume @p345 (forall @t601 (=> @t600 (= (tptp.c_Orderings_Oord__class_Oless @t178 @t2 @t1) (and @t599 (not (tptp.c_Orderings_Oord__class_Oless__eq @t178 @t1 @t2))))))) % 0.54/0.94 (assume @p346 (forall @t602 (=> @t544 (=> (tptp.c_Orderings_Oord__class_Oless__eq @t440 @t275 @t142) (tptp.c_Wellfounded_OwfP @t23 @t275))))) % 0.54/0.94 (assume @p347 (forall @t602 (=> @t500 (=> (tptp.c_Orderings_Oord__class_Oless__eq @t203 @t275 @t142) (tptp.c_Wellfounded_Owf @t23 @t275))))) % 0.54/0.94 (assume @p348 (forall @t125 (= (tptp.c_Orderings_Oord__class_Oless__eq @t401 @t124 @t123) (tptp.c_Orderings_Oord__class_Oless__eq @t118 @t52 @t116)))) % 0.54/0.94 (assume @p349 (forall @t388 (=> @t597 (=> @t95 @t96)))) % 0.54/0.94 (assume @p350 (forall @t488 (=> @t95 (=> @t597 @t96)))) % 0.54/0.94 (assume @p351 (forall (@list @t21 @t53 @t27 @t603 @t23) (=> (tptp.c_Orderings_Oord__class_Oless__eq @t163 @t603 @t27) (tptp.c_Orderings_Oord__class_Oless__eq @t373 @t177 (tptp.c_FuncSet_OPi @t23 @t53 @t603 @t21))))) % 0.54/0.94 (assume @p352 (forall @t606 (=> (tptp.c_Orderings_Oord__class_Oless__eq @t203 @t604 @t605) (tptp.c_Orderings_Oord__class_Oless__eq @t163 (tptp.c_Wellfounded_Oacc @t23 @t605) (tptp.c_Wellfounded_Oacc @t23 @t604))))) % 0.54/0.94 (assume @p353 (forall @t606 (=> (tptp.c_Orderings_Oord__class_Oless__eq @t440 @t604 @t605) (tptp.c_Orderings_Oord__class_Oless__eq @t163 (tptp.c_Wellfounded_Oaccp @t23 @t605) (tptp.c_Wellfounded_Oaccp @t23 @t604))))) % 0.54/0.94 (assume @p354 (forall @t608 (=> @t607 (=> (tptp.c_Relation_Oantisym @t23 @t140) @t588)))) % 0.54/0.94 (assume @p355 (forall @t610 (=> @t609 (tptp.c_Orderings_Oord__class_Oless__eq @t163 @t318 (tptp.c_Relation_ODomain @t23 @t53 @t140))))) % 0.54/0.94 (assume @p356 (forall @t608 (=> (tptp.c_Orderings_Oord__class_Oless__eq @t203 @t142 @t611) @t612))) % 0.54/0.94 (assume @p357 (forall @t167 (=> (tptp.c_Orderings_Oord__class_Oless__eq @t203 @t52 @t116) (=> (tptp.c_Orderings_Oord__class_Oless__eq @t203 @t116 @t312) (= (tptp.c_Transitive__Closure_Ortrancl @t23 @t116) @t312))))) % 0.54/0.94 (assume @p358 (forall @t608 (=> @t607 @t612))) % 0.54/0.94 (assume @p359 (forall @t167 (=> (tptp.c_Orderings_Oord__class_Oless__eq @t440 @t52 @t116) (=> (tptp.c_Orderings_Oord__class_Oless__eq @t440 @t116 @t517) (= (tptp.c_Transitive__Closure_Ortranclp @t23 @t116) @t517))))) % 0.54/0.94 (assume @p360 (forall @t608 (=> (tptp.c_Orderings_Oord__class_Oless__eq @t440 @t142 @t140) (tptp.c_Orderings_Oord__class_Oless__eq @t440 @t432 (tptp.c_Transitive__Closure_Ortranclp @t23 @t140))))) % 0.54/0.94 (assume @p361 (forall (@list @t232 @t21 @t225 @t27 @t23) (=> @t613 (=> (tptp.c_Orderings_Oord__class_Oless__eq @t163 @t21 @t232) (tptp.c_Orderings_Oord__class_Oless__eq @t163 @t386 (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t163 @t225 @t232)))))) % 0.54/0.94 (assume @p362 (forall (@list @t21 @t27 @t225 @t23) (=> (tptp.c_Orderings_Oord__class_Oless__eq @t163 @t225 @t27) (=> (tptp.c_Orderings_Oord__class_Oless__eq @t163 @t225 @t21) (tptp.c_Orderings_Oord__class_Oless__eq @t163 @t225 @t386))))) % 0.54/0.94 (assume @p363 (forall (@list @t27 @t21 @t23) (=> @t614 (= @t386 @t21)))) % 0.54/0.94 (assume @p364 (forall @t394 (=> @t597 (= @t386 @t27)))) % 0.54/0.94 (assume @p365 (forall @t394 (tptp.c_Orderings_Oord__class_Oless__eq @t163 @t386 @t21))) % 0.54/0.94 (assume @p366 (forall @t394 (tptp.c_Orderings_Oord__class_Oless__eq @t163 @t386 @t27))) % 0.54/0.94 (assume @p367 (forall @t167 (= (tptp.c_Orderings_Oord__class_Oless__eq @t163 @t166 @t165) (tptp.c_Orderings_Oord__class_Oless__eq @t163 @t52 @t116)))) % 0.54/0.94 (assume @p368 (forall @t610 (=> @t609 (=> (tptp.c_Relation_Osingle__valued @t23 @t53 @t140) @t324)))) % 0.54/0.94 (assume @p369 (forall (@list @t142 @t140 @t23) (=> (tptp.c_Wellfounded_Oacyclic @t23 @t140) (=> @t607 @t470)))) % 0.54/0.94 (assume @p370 (forall (@list @t85 @t21 @t23) (tptp.c_Orderings_Oord__class_Oless__eq @t163 @t21 @t484))) % 0.54/0.94 (assume @p371 (forall (@list @t88 @t21 @t27 @t23) (=> @t597 (tptp.c_Orderings_Oord__class_Oless__eq @t163 @t27 @t477)))) % 0.54/0.94 (assume @p372 (forall (@list @t85 @t232 @t225 @t23) (=> (tptp.c_Orderings_Oord__class_Oless__eq @t163 @t225 @t232) (tptp.c_Orderings_Oord__class_Oless__eq @t163 (tptp.c_Set_Oinsert @t23 @t85 @t225) (tptp.c_Set_Oinsert @t23 @t85 @t232))))) % 0.54/0.94 (assume @p373 (forall @t488 (= (tptp.c_Orderings_Oord__class_Oless__eq @t163 @t482 @t21) (and @t96 @t597)))) % 0.54/0.94 (assume @p374 (forall @t488 (=> @t171 (= (tptp.c_Orderings_Oord__class_Oless__eq @t163 @t27 @t487) @t597)))) % 0.54/0.94 (assume @p375 (forall (@list @t140 @t142 @t275 @t23) (=> @t454 (=> @t607 (tptp.hBOOL (tptp.hAPP @t276 (tptp.c_Transitive__Closure_Otrancl @t23 @t140))))))) % 0.54/0.94 (assume @p376 (forall @t292 (=> @t291 (=> @t597 (tptp.hBOOL (tptp.hAPP @t180 (tptp.c_FuncSet_Oextensional @t23 @t53 @t21))))))) % 0.54/0.94 (assume @p377 (forall @t601 (=> @t600 (= @t599 (forall @t8 (tptp.c_Orderings_Oord__class_Oless__eq @t53 @t6 @t5)))))) % 0.54/0.94 (assume @p378 (forall @t418 (=> @t615 (or @t580 @t581)))) % 0.54/0.94 (assume @p379 (forall @t170 (=> @t617 (= @t40 (and @t584 @t616))))) % 0.54/0.94 (assume @p380 (forall @t418 (=> @t589 (=> @t618 @t580)))) % 0.54/0.94 (assume @p381 (forall (@list @t33 @t1 @t2 @t23 @t53) (=> @t600 (=> @t599 (tptp.c_Orderings_Oord__class_Oless__eq @t53 @t173 @t395))))) % 0.54/0.94 (assume @p382 (forall @t620 (=> @t617 (=> @t616 @t619)))) % 0.54/0.94 (assume @p383 (forall @t414 (=> @t622 (=> @t621 (=> (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t271 @t411) @t578))))) % 0.54/0.94 (assume @p384 (forall @t414 (=> @t617 (=> @t621 (=> (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t411 @t271) @t623))))) % 0.54/0.94 (assume @p385 (forall @t414 (=> @t622 (=> @t625 (=> @t624 @t578))))) % 0.54/0.94 (assume @p386 (forall @t416 (=> @t617 (=> @t626 (=> @t624 @t623))))) % 0.54/0.94 (assume @p387 (forall @t418 (=> @t617 (=> @t580 (=> @t581 @t618))))) % 0.54/0.94 (assume @p388 (forall @t410 (=> @t589 (=> @t580 (=> @t627 @t579))))) % 0.54/0.94 (assume @p389 (forall @t582 (=> @t617 (=> @t581 (=> @t580 @t618))))) % 0.54/0.94 (assume @p390 (forall @t629 (=> @t617 (=> @t581 (=> @t628 (tptp.c_Orderings_Oord__class_Oless__eq @t23 @t402 @t405)))))) % 0.54/0.94 (assume @p391 (forall @t418 (=> @t615 (=> (not @t580) @t581)))) % 0.54/0.94 (assume @p392 (forall @t422 (=> @t589 (not (tptp.c_Orderings_Oord__class_Oless @t23 @t405 @t405))))) % 0.54/0.94 (assume @p393 (forall @t170 (=> @t615 (= @t41 (or @t631 @t630))))) % 0.54/0.94 (assume @p394 (forall @t170 (=> @t615 (= @t632 (or @t630 @t40))))) % 0.54/0.94 (assume @p395 (forall @t418 (=> @t615 (or @t634 @t618 @t633)))) % 0.54/0.94 (assume @p396 (forall @t620 (=> @t615 (=> (not @t630) @t635)))) % 0.54/0.94 (assume @p397 (forall @t418 (=> @t615 (=> @t637 (=> @t636 @t633))))) % 0.54/0.94 (assume @p398 (forall @t418 (=> @t617 (=> @t634 @t637)))) % 0.54/0.94 (assume @p399 (forall @t418 (=> @t589 (=> @t634 (not @t633))))) % 0.54/0.94 (assume @p400 (forall @t418 (=> @t617 (=> @t634 (not (= @t403 @t405)))))) % 0.54/0.94 (assume @p401 (forall @t419 (=> @t589 (=> @t639 (not @t638))))) % 0.54/0.94 (assume @p402 (forall @t640 (=> @t617 (=> @t638 (not @t639))))) % 0.54/0.94 (assume @p403 (forall @t414 (=> @t622 (=> @t621 (=> (tptp.c_Orderings_Oord__class_Oless @t23 @t271 @t411) @t641))))) % 0.54/0.94 (assume @p404 (forall @t414 (=> @t617 (=> @t621 (=> (tptp.c_Orderings_Oord__class_Oless @t23 @t411 @t271) @t642))))) % 0.54/0.94 (assume @p405 (forall @t414 (=> @t622 (=> @t639 (=> @t624 @t641))))) % 0.54/0.94 (assume @p406 (forall @t416 (=> @t617 (=> @t638 (=> @t624 @t642))))) % 0.54/0.94 (assume @p407 (forall @t410 (=> @t589 (=> @t634 @t644)))) % 0.54/0.94 (assume @p408 (forall @t629 (=> @t617 (=> @t633 @t646)))) % 0.54/0.94 (assume @p409 (forall @t418 (=> @t615 (=> @t636 (=> @t637 @t633))))) % 0.54/0.94 (assume @p410 (forall @t647 (not (tptp.c_Orderings_Oord__class_Oless tptp.tc_Nat_Onat @t590 @t590)))) % 0.54/0.94 (assume @p411 (forall @t572 (= @t650 (or @t587 @t648)))) % 0.54/0.94 (assume @p412 (forall @t566 (=> @t637 (=> (not @t565) (tptp.c_Orderings_Oord__class_Oless tptp.tc_Nat_Onat @t403 @t405))))) % 0.54/0.94 (assume @p413 (forall (@list @t591 @t590) (=> (tptp.c_Orderings_Oord__class_Oless tptp.tc_Nat_Onat @t590 @t591) @t596))) % 0.54/0.94 (assume @p414 (forall (@list @t651 @t652) (=> (tptp.c_Orderings_Oord__class_Oless tptp.tc_Nat_Onat @t652 @t651) (not (= @t652 @t651))))) % 0.54/0.94 (assume @p415 (forall (@list @t60 @t569 @t536) (=> (=> @t587 @t653) (=> (=> @t649 @t653) (=> (=> @t648 @t653) @t653))))) % 0.54/0.94 (assume @p416 (forall @t647 (tptp.c_Orderings_Oord__class_Oless__eq tptp.tc_Nat_Onat @t590 @t590))) % 0.54/0.94 (assume @p417 (forall @t595 (or @t592 @t654))) % 0.54/0.94 (assume @p418 (forall @t595 (=> @t593 @t592))) % 0.54/0.94 (assume @p419 (forall (@list @t655 @t657 @t656) (=> (tptp.c_Orderings_Oord__class_Oless__eq tptp.tc_Nat_Onat @t656 @t657) (=> (tptp.c_Orderings_Oord__class_Oless__eq tptp.tc_Nat_Onat @t657 @t655) (tptp.c_Orderings_Oord__class_Oless__eq tptp.tc_Nat_Onat @t656 @t655))))) % 0.54/0.94 (assume @p420 (forall @t595 (=> @t592 (=> @t654 @t593)))) % 0.54/0.94 (assume @p421 (forall @t658 (tptp.c_Orderings_Oord__class_Oless__eq @t163 (tptp.c_Relation_ODomain @t23 @t53 (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t118 @t27 @t21)) (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t163 (tptp.c_Relation_ODomain @t23 @t53 @t27) (tptp.c_Relation_ODomain @t23 @t53 @t21))))) % 0.54/0.94 (assume @p422 (forall @t658 (tptp.c_Orderings_Oord__class_Oless__eq @t163 (tptp.c_Relation_ORange @t53 @t23 (tptp.c_Lattices_Osemilattice__inf__class_Oinf (tptp.tc_fun @t368 tptp.tc_HOL_Obool) @t27 @t21)) (tptp.c_Lattices_Osemilattice__inf__class_Oinf @t163 (tptp.c_Relation_ORange @t53 @t23 @t27) (tptp.c_Relation_ORange @t53 @t23 @t21))))) % 0.54/0.94 (assume @p423 (forall @t170 (=> @t615 (= @t632 @t616)))) % 0.54/0.94 (assume @p424 (forall @t170 (=> @t615 (= (not @t584) @t630)))) % 0.54/0.94 (assume @p425 (forall @t418 (=> @t615 (or @t580 @t633)))) % 0.54/0.94 (assume @p426 (forall @t170 (=> @t617 (= @t631 (and @t584 @t41))))) % 0.54/0.94 (assume @p427 (forall @t170 (=> @t589 (= @t631 (and @t584 (not @t616)))))) % 0.54/0.94 (assume @p428 (forall @t170 (=> @t617 (= @t584 (or @t631 @t40))))) % 0.54/0.94 (assume @p429 (forall @t418 (=> @t615 (=> @t636 @t581)))) % 0.54/0.94 (assume @p430 (forall @t582 (=> @t615 (=> (not @t581) @t634)))) % 0.54/0.94 (assume @p431 (forall @t170 (=> @t615 (=> @t632 @t619)))) % 0.54/0.94 (assume @p432 (forall @t419 (=> @t617 (=> @t659 (=> @t625 @t639))))) % 0.54/0.94 (assume @p433 (forall @t419 (=> @t617 (=> @t659 (=> @t626 @t638))))) % 0.54/0.94 (assume @p434 (forall @t582 (=> @t615 (=> @t581 @t636)))) % 0.54/0.94 (assume @p435 (forall @t418 (=> @t589 (=> @t634 @t580)))) % 0.54/0.94 (assume @p436 (forall @t170 (=> @t615 (=> @t584 @t635)))) % 0.54/0.94 (assume @p437 (forall @t418 (=> @t617 (=> @t580 (or @t634 @t618))))) % 0.54/0.94 (assume @p438 (forall @t419 (=> @t617 (=> @t625 (=> @t659 @t639))))) % 0.54/0.94 (assume @p439 (forall @t640 (=> @t617 (=> @t626 (=> @t659 @t638))))) % 0.54/0.94 (assume @p440 (forall @t410 (=> @t589 (=> @t634 (=> @t627 @t643))))) % 0.54/0.94 (assume @p441 (forall @t629 (=> @t617 (=> @t633 (=> @t628 @t645))))) % 0.54/0.94 (assume @p442 (forall @t410 (=> @t589 (=> @t580 @t644)))) % 0.54/0.94 (assume @p443 (forall @t629 (=> @t617 (=> @t581 @t646)))) % 0.54/0.94 (assume @p444 (forall @t572 (= @t587 (and @t570 @t650)))) % 0.54/0.94 (assume @p445 (forall @t572 (= @t570 (or @t587 @t649)))) % 0.54/0.94 (assume @p446 (forall @t595 (=> @t594 @t592))) % 0.54/0.94 (assume @p447 (forall @t666 (=> @t665 (=> (tptp.c_Orderings_Oord__class_Oless tptp.tc_Nat_Onat @t140 @t660) @t664)))) % 0.54/0.94 (assume @p448 (forall @t666 (=> @t665 (=> (tptp.c_Orderings_Oord__class_Oless__eq tptp.tc_Nat_Onat @t140 @t660) @t667)))) % 0.54/0.94 (assume @p449 (forall @t666 (=> @t668 @t667))) % 0.54/0.94 (assume @p450 (forall @t394 (=> @t597 (=> @t614 @t30)))) % 0.54/0.94 (assume @p451 (forall @t188 (tptp.c_Orderings_Oord__class_Oless__eq @t163 @t27 @t27))) % 0.54/0.94 (assume @p452 (forall @t669 (= @t30 (and @t597 @t614)))) % 0.54/0.94 (assume @p453 (forall @t669 (=> @t30 @t597))) % 0.54/0.94 (assume @p454 (forall @t669 (=> @t30 @t614))) % 0.54/0.94 (assume @p455 (forall @t393 (=> @t597 (=> @t598 @t613)))) % 0.54/0.94 (assume @p456 (forall @t669 (=> @t30 (not (=> @t597 (not @t614)))))) % 0.54/0.94 (assume @p457 (forall (@list @t670 @t23 @t33 @t60) (=> @t69 (=> @t673 @t672)))) % 0.54/0.94 (assume @p458 (forall (@list @t33 @t670 @t60 @t23) (=> @t673 (=> @t69 @t672)))) % 0.54/0.94 (assume @p459 (forall (@list @t32 @t33 @t670 @t60 @t53 @t23) (=> @t676 (=> @t675 @t674)))) % 0.54/0.94 (assume @p460 (forall (@list @t670 @t53 @t23 @t32 @t33 @t60) (=> @t675 (=> @t676 @t674)))) % 0.54/0.94 (assume @p461 (tptp.c_Wellfounded_Owf @t561 tptp.c_FunDef_Opair__less)) % 0.54/0.94 (assume @p462 (= tptp.c_FunDef_Opair__less (tptp.c_Wellfounded_Olex__prod tptp.tc_Nat_Onat tptp.tc_Nat_Onat tptp.c_Wellfounded_Oless__than tptp.c_Wellfounded_Oless__than))) % 0.54/0.94 (assume @p463 (forall @t666 (=> @t668 @t664))) % 0.54/0.94 (assume @p464 (forall (@list @t678 @t33 @t677 @t32) (=> (tptp.hBOOL (tptp.hAPP @t687 @t677)) (=> @t686 (=> (tptp.hBOOL (tptp.hAPP @t684 tptp.c_FunDef_Omax__weak)) (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t682 (tptp.hAPP (tptp.hAPP @t680 (tptp.c_Set_Oinsert @t561 @t33 @t678)) @t677)) tptp.c_FunDef_Omax__weak))))))) % 0.54/0.94 (assume @p465 (forall @t690 (=> @t689 (=> @t686 (=> (tptp.hBOOL (tptp.hAPP @t684 tptp.c_FunDef_Omin__weak)) (tptp.hBOOL (tptp.hAPP @t688 tptp.c_FunDef_Omin__weak))))))) % 0.54/0.94 (assume @p466 (forall @t690 (=> @t689 (=> @t691 (=> (tptp.hBOOL (tptp.hAPP @t684 tptp.c_FunDef_Omin__strict)) (tptp.hBOOL (tptp.hAPP @t688 tptp.c_FunDef_Omin__strict))))))) % 0.54/0.94 (assume @p467 (forall (@list @t693 @t33 @t692 @t32) (=> (tptp.hBOOL (tptp.hAPP @t687 @t692)) (=> @t691 (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t682 (tptp.hAPP (tptp.hAPP @t680 @t693) @t692)) tptp.c_FunDef_Omax__strict)) (tptp.hBOOL (tptp.hAPP (tptp.hAPP @t682 (tptp.hAPP (tptp.hAPP @t680 (tptp.c_Set_Oinsert @t561 @t33 @t693)) @t692)) tptp.c_FunDef_Omax__strict))))))) % 0.54/0.94 (assume @p468 (tptp.c_FunDef_Oreduction__pair @t679 (tptp.hAPP (tptp.hAPP @t695 tptp.c_FunDef_Omin__strict) tptp.c_FunDef_Omin__weak))) % 0.54/0.94 (assume @p469 (tptp.c_FunDef_Oreduction__pair @t679 (tptp.hAPP (tptp.hAPP @t695 tptp.c_FunDef_Omax__strict) tptp.c_FunDef_Omax__weak))) % 0.54/0.94 (assume @p470 (= tptp.c_FunDef_Omin__strict (tptp.c_Wellfounded_Omin__ext @t561 tptp.c_FunDef_Opair__less))) % 0.54/0.94 (assume @p471 (forall (@list @t2 @t53 @t60 @t23) (=> (tptp.c_FunDef_Oreduction__pair @t23 @t60) (tptp.c_FunDef_Oreduction__pair @t53 (tptp.hAPP (tptp.hAPP @t696 @t60) @t2))))) % 0.54/0.94 (assume @p472 (forall @t193 (=> @t500 (tptp.c_Wellfounded_Owf @t163 (tptp.c_Wellfounded_Omin__ext @t23 @t142))))) % 0.54/0.94 (assume @p473 (forall @t167 (=> @t522 (=> (tptp.c_Orderings_Oord__class_Oless__eq @t203 (tptp.c_Relation_Orel__comp @t23 @t23 @t23 @t52 @t116) @t52) (tptp.c_FunDef_Oreduction__pair @t23 (tptp.hAPP (tptp.hAPP (tptp.c_Product__Type_OPair @t203 @t203) @t52) @t116)))))) % 0.54/0.94 (assume @p474 (forall (@list @t53 @t23) (= @t696 (tptp.hAPP (tptp.c_Product__Type_Oprod_Oprod__case @t203 @t203 @t701) (tptp.hAPP (tptp.hAPP (tptp.c_COMBC @t203 @t704 @t703) (tptp.hAPP (tptp.hAPP (tptp.c_COMBB @t702 (tptp.tc_fun @t704 @t703) @t203) (tptp.c_COMBB @t700 @t701 @t203)) (tptp.hAPP (tptp.hAPP (tptp.c_COMBB @t699 @t702 @t203) (tptp.c_COMBS @t396 @t527 @t697)) (tptp.hAPP (tptp.hAPP (tptp.c_COMBB @t700 @t699 @t203) (tptp.hAPP (tptp.c_COMBB @t527 @t698 @t396) (tptp.c_Product__Type_OPair @t527 @t527))) @t504)))) @t504))))) % 0.54/0.94 (assume @p475 (forall (@list @t140 @t22 @t226 @t142 @t88 @t85 @t53 @t23) (=> @t320 (=> (tptp.hBOOL (tptp.hAPP (tptp.hAPP (tptp.c_member @t707) (tptp.hAPP (tptp.hAPP @t288 @t88) @t22)) @t140)) (tptp.hBOOL (tptp.hAPP (tptp.hAPP (tptp.c_member @t706) (tptp.hAPP (tptp.hAPP (tptp.c_Product__Type_OPair @t23 @t226) @t85) @t22)) @t705)))))) % 0.54/0.94 (assume @p476 (forall (@list @t140 @t708 @t226 @t142 @t507 @t53 @t23) (=> (tptp.c_Orderings_Oord__class_Oless__eq @t118 @t507 @t142) (=> (tptp.c_Orderings_Oord__class_Oless__eq (tptp.tc_fun @t707 tptp.tc_HOL_Obool) @t708 @t140) (tptp.c_Orderings_Oord__class_Oless__eq (tptp.tc_fun @t706 tptp.tc_HOL_Obool) (tptp.c_Relation_Orel__comp @t23 @t53 @t226 @t507 @t708) @t705))))) % 0.54/0.94 (assume @p477 (forall @t193 (= @t424 (tptp.c_Relation_Orel__comp @t23 @t23 @t23 @t142 @t241)))) % 0.54/0.94 (assume @p478 (forall @t193 (= @t424 (tptp.c_Relation_Orel__comp @t23 @t23 @t23 @t241 @t142)))) % 0.54/0.94 (assume @p479 (forall (@list @t226 @t53 @t23) (= (tptp.c_Product__Type_Ointernal__split @t23 @t53 @t226) (tptp.c_Product__Type_Oprod_Oprod__case @t23 @t53 @t226)))) % 0.54/0.94 (assume @p480 (forall (@list @t140 @t226 @t142 @t53 @t23) (=> @t324 (=> (tptp.c_Relation_Osingle__valued @t53 @t226 @t140) (tptp.c_Relation_Osingle__valued @t23 @t226 @t705))))) % 0.54/0.94 (assume @p481 (forall @t713 (=> @t712 (tptp.class_Lattices_Osemilattice__inf @t711)))) % 0.54/0.94 (assume @p482 (forall @t713 (=> (tptp.class_Orderings_Opreorder @t709) (tptp.class_Orderings_Opreorder @t711)))) % 0.54/0.94 (assume @p483 (forall @t713 (=> @t712 (tptp.class_Lattices_Olattice @t711)))) % 0.54/0.94 (assume @p484 (forall @t713 (=> (tptp.class_Orderings_Oorder @t709) (tptp.class_Orderings_Oorder @t711)))) % 0.54/0.94 (assume @p485 (forall @t713 (=> (tptp.class_Orderings_Oord @t709) (tptp.class_Orderings_Oord @t711)))) % 0.54/0.94 (assume @p486 (tptp.class_Lattices_Osemilattice__inf tptp.tc_Nat_Onat)) % 0.54/0.94 (assume @p487 (tptp.class_Orderings_Opreorder tptp.tc_Nat_Onat)) % 0.54/0.94 (assume @p488 (tptp.class_Orderings_Olinorder tptp.tc_Nat_Onat)) % 0.54/0.94 (assume @p489 (tptp.class_Lattices_Olattice tptp.tc_Nat_Onat)) % 0.54/0.94 (assume @p490 (tptp.class_Orderings_Oorder tptp.tc_Nat_Onat)) % 0.54/0.94 (assume @p491 (tptp.class_Orderings_Oord tptp.tc_Nat_Onat)) % 0.54/0.94 (assume @p492 (tptp.class_Lattices_Osemilattice__inf tptp.tc_HOL_Obool)) % 0.54/0.94 (assume @p493 (tptp.class_Orderings_Opreorder tptp.tc_HOL_Obool)) % 0.54/0.94 (assume @p494 (tptp.class_Lattices_Olattice tptp.tc_HOL_Obool)) % 0.54/0.94 (assume @p495 (tptp.class_Orderings_Oorder tptp.tc_HOL_Obool)) % 0.54/0.94 (assume @p496 (tptp.class_Orderings_Oord tptp.tc_HOL_Obool)) % 0.54/0.94 (assume @p497 (forall (@list @t714 @t23) (= (tptp.hAPP @t186 @t714) @t714))) % 0.54/0.94 (assume @p498 (forall (@list @t715 @t714 @t53 @t23) (= (tptp.hAPP (tptp.c_COMBK @t23 @t53 @t714) @t715) @t714))) % 0.54/0.94 (assume @p499 (forall (@list @t52 @t670 @t60 @t226 @t23 @t53) (= (tptp.hAPP (tptp.hAPP (tptp.hAPP (tptp.c_COMBB @t53 @t23 @t226) @t60) @t670) @t52) (tptp.hAPP @t60 @t716)))) % 0.54/0.94 (assume @p500 (forall @t718 (= (tptp.hAPP (tptp.hAPP (tptp.hAPP (tptp.c_COMBC @t53 @t226 @t23) @t60) @t670) @t52) (tptp.hAPP @t717 @t670)))) % 0.54/0.94 (assume @p501 (forall @t718 (= (tptp.hAPP (tptp.hAPP (tptp.hAPP (tptp.c_COMBS @t53 @t226 @t23) @t60) @t670) @t52) (tptp.hAPP @t717 @t716)))) % 0.54/0.94 (assume @p502 (forall @t563 (or (not @t719) @t40))) % 0.54/0.94 (assume @p503 (forall @t563 (or @t41 @t719))) % 0.54/0.94 (assume @p504 (not (tptp.hBOOL tptp.c_fFalse))) % 0.54/0.94 (assume @p505 (forall @t723 (or (not @t722) @t721))) % 0.54/0.94 (assume @p506 (forall @t723 (or (not @t721) @t722))) % 0.54/0.94 (assume @p507 (forall @t726 (or @t721 (not @t725) @t724))) % 0.54/0.94 (assume @p508 (forall @t726 (or @t727 @t720))) % 0.54/0.94 (assume @p509 (forall @t726 (or @t727 @t725))) % 0.54/0.94 (assume @p510 (not (= @t84 @t73))) % 0.54/0.94 (assume @p511 true) % 0.54/0.94 (step @p512 :rule equiv_elim2 :premises (@p17)) % 0.54/0.94 (step @p513 :rule symm :premises (@p19)) % 0.54/0.94 (step @p514 :rule equiv_elim2 :premises (@p513)) % 0.54/0.94 (step @p515 :rule symm :premises (@p510)) % 0.54/0.94 (step @p516 :rule not_equiv_elim1 :premises (@p515)) % 0.54/0.94 (step @p517 :rule symm :premises (@p20)) % 0.54/0.94 (step @p518 :rule equiv_elim2 :premises (@p517)) % 0.54/0.94 (step @p519 :rule symm :premises (@p21)) % 0.54/0.94 (step @p520 :rule equiv_elim2 :premises (@p519)) % 0.54/0.94 (step @p521 :rule chain_m_resolution :premises (@p520 @p518 @p516 @p514 @p512) :args (@t81 (@list true false true true) (@list @t83 @t84 @t82 @t73))) % 0.54/0.94 (step @p522 :rule equiv_elim1 :premises (@p17)) % 0.54/0.94 (step @p523 :rule reordering :premises (@p522) :args ((or @t73 @t728))) % 0.54/0.94 (step @p524 :rule chain_m_resolution :premises (@p523 @p521) :args (@t73 @t729 @t730)) % 0.54/0.94 (step @p525 :rule not_equiv_elim2 :premises (@p515)) % 0.54/0.94 (step @p526 :rule chain_m_resolution :premises (@p525 @p524) :args ((not @t84) @t729 (@list @t73))) % 0.54/0.94 (step @p527 :rule equiv_elim1 :premises (@p513)) % 0.54/0.94 (step @p528 :rule reordering :premises (@p527) :args ((or @t82 @t728))) % 0.54/0.94 (step @p529 :rule chain_m_resolution :premises (@p528 @p521) :args (@t82 @t729 @t730)) % 0.54/0.94 (step @p530 :rule equiv_elim1 :premises (@p517)) % 0.54/0.94 (step @p531 :rule reordering :premises (@p530) :args ((or @t83 (not @t82)))) % 0.54/0.94 (step @p532 :rule chain_m_resolution :premises (@p531 @p529) :args (@t83 @t729 (@list @t82))) % 0.54/0.94 (step @p533 :rule equiv_elim1 :premises (@p519)) % 0.54/0.94 (step @p534 :rule reordering :premises (@p533) :args ((or @t84 (not @t83)))) % 0.54/0.94 (step @p535 false :rule chain_m_resolution :premises (@p534 @p532 @p526) :args (false (@list false true) (@list @t83 @t84))) % 0.54/0.94 ) % 0.54/0.94 % SZS output end Proof % 0.54/0.94 % cvc5 exiting %------------------------------------------------------------------------------