%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : SCT171+5 : TPTP v9.2.1. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n004.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:28 AM UTC 2026 % Result : Theorem 0.50s 0.79s % Output : Proof 0.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SCT171+5 : TPTP v9.2.1. Released v5.3.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.16/0.34 % Computer : n004.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue Jun 2 14:37:52 EDT 2026 % 0.16/0.34 % CPUTime : % 0.39/0.65 %----Proving TF0_NAR, FOF, or CNF % 0.50/0.79 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.50/0.79 % SZS status Theorem % 0.50/0.79 % SZS output start Proof % 0.50/0.79 ( % 0.50/0.79 (declare-sort $$unsorted 0) % 0.50/0.79 (declare-const tptp.order (-> $$unsorted Bool)) % 0.50/0.79 (declare-const tptp.n $$unsorted) % 0.50/0.79 (declare-const tptp.e $$unsorted) % 0.50/0.79 (declare-const tptp.d $$unsorted) % 0.50/0.79 (declare-const tptp.c $$unsorted) % 0.50/0.79 (declare-const tptp.a $$unsorted) % 0.50/0.79 (declare-const tptp.p $$unsorted) % 0.50/0.79 (declare-const tptp.linorder (-> $$unsorted Bool)) % 0.50/0.79 (declare-const tptp.member (-> $$unsorted $$unsorted)) % 0.50/0.79 (declare-const tptp.hBOOL (-> $$unsorted Bool)) % 0.50/0.79 (declare-const tptp.fequal (-> $$unsorted $$unsorted)) % 0.50/0.79 (declare-const tptp.fFalse $$unsorted) % 0.50/0.79 (declare-const tptp.collect (-> $$unsorted $$unsorted)) % 0.50/0.79 (declare-const tptp.product_prod_rec (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.50/0.79 (declare-const tptp.product_Pair (-> $$unsorted $$unsorted $$unsorted)) % 0.50/0.79 (declare-const tptp.arrow_844286440_mkbot $$unsorted) % 0.50/0.79 (declare-const tptp.finite_card (-> $$unsorted $$unsorted)) % 0.50/0.79 (declare-const tptp.arrow_1990387629ctator $$unsorted) % 0.50/0.79 (declare-const tptp.top_top (-> $$unsorted $$unsorted)) % 0.50/0.79 (declare-const tptp.arrow_638930832le_Lin $$unsorted) % 0.50/0.79 (declare-const tptp.lba $$unsorted) % 0.50/0.79 (declare-const tptp.ti (-> $$unsorted $$unsorted $$unsorted)) % 0.50/0.79 (declare-const tptp.arrow_1834574746e_Prof $$unsorted) % 0.50/0.79 (declare-const tptp.ord (-> $$unsorted Bool)) % 0.50/0.79 (declare-const tptp.arrow_1384031255e_indi $$unsorted) % 0.50/0.79 (declare-const tptp.hAPP (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.50/0.79 (declare-const tptp.combi (-> $$unsorted $$unsorted)) % 0.50/0.79 (declare-const tptp.product_prod (-> $$unsorted $$unsorted $$unsorted)) % 0.50/0.79 (declare-const tptp.f $$unsorted) % 0.50/0.79 (declare-const tptp.arrow_1932713123nimity $$unsorted) % 0.50/0.79 (declare-const tptp.arrow_1212486748le_alt $$unsorted) % 0.50/0.79 (declare-const tptp.arrow_1726925404_above $$unsorted) % 0.50/0.79 (declare-const tptp.lab $$unsorted) % 0.50/0.79 (declare-const tptp.bool $$unsorted) % 0.50/0.79 (declare-const tptp.h $$unsorted) % 0.50/0.79 (declare-const tptp.if (-> $$unsorted $$unsorted)) % 0.50/0.79 (declare-const tptp.inj_on (-> $$unsorted $$unsorted $$unsorted)) % 0.50/0.79 (declare-const tptp.arrow_992993526_mktop $$unsorted) % 0.50/0.79 (declare-const tptp.fun (-> $$unsorted $$unsorted $$unsorted)) % 0.50/0.79 (declare-const tptp.combb (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.50/0.79 (declare-const tptp.combc (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.50/0.79 (declare-const tptp.top (-> $$unsorted Bool)) % 0.50/0.79 (declare-const tptp.combs (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.50/0.79 (declare-const tptp.nat $$unsorted) % 0.50/0.79 (declare-const tptp.fTrue $$unsorted) % 0.50/0.79 (declare-const tptp.hilbert_inv_into (-> $$unsorted $$unsorted $$unsorted)) % 0.50/0.79 (declare-const tptp.arrow_612047104le_IIA $$unsorted) % 0.50/0.79 (declare-const tptp.pi (-> $$unsorted $$unsorted $$unsorted)) % 0.50/0.79 (declare-const tptp.preorder (-> $$unsorted Bool)) % 0.50/0.79 (declare-const tptp.b $$unsorted) % 0.50/0.79 (declare-const tptp.undefined (-> $$unsorted $$unsorted)) % 0.50/0.79 (declare-const tptp.combk (-> $$unsorted $$unsorted $$unsorted)) % 0.50/0.79 (declare-const tptp.ord_less (-> $$unsorted $$unsorted)) % 0.50/0.79 (define @t1 () (tptp.product_prod tptp.arrow_1212486748le_alt tptp.arrow_1212486748le_alt)) % 0.50/0.79 (define @t2 () (tptp.fun @t1 tptp.bool)) % 0.50/0.79 (define @t3 () (tptp.fun tptp.arrow_1384031255e_indi @t2)) % 0.50/0.79 (define @t4 () (tptp.fun @t3 @t2)) % 0.50/0.79 (define @t5 () (tptp.fun @t4 tptp.bool)) % 0.50/0.79 (define @t6 () (tptp.fun @t2 tptp.bool)) % 0.50/0.79 (define @t7 () (tptp.fun @t3 tptp.bool)) % 0.50/0.79 (define @t8 () (tptp.fun tptp.arrow_1212486748le_alt @t2)) % 0.50/0.79 (define @t9 () (tptp.fun tptp.arrow_1212486748le_alt @t8)) % 0.50/0.79 (define @t10 () (tptp.fun @t2 @t9)) % 0.50/0.79 (define @t11 () (tptp.fun tptp.arrow_1384031255e_indi tptp.bool)) % 0.50/0.79 (define @t12 () (tptp.fun @t2 @t8)) % 0.50/0.79 (define @t13 () (@var "X_a" $$unsorted)) % 0.50/0.79 (define @t14 () (@var "X_c" $$unsorted)) % 0.50/0.79 (define @t15 () (@var "X_b" $$unsorted)) % 0.50/0.79 (define @t16 () (tptp.combb @t15 @t14 @t13)) % 0.50/0.79 (define @t17 () (tptp.fun @t13 @t14)) % 0.50/0.79 (define @t18 () (tptp.fun @t13 @t15)) % 0.50/0.79 (define @t19 () (tptp.fun @t18 @t17)) % 0.50/0.79 (define @t20 () (tptp.fun @t15 @t14)) % 0.50/0.79 (define @t21 () (@list @t15 @t14 @t13)) % 0.50/0.79 (define @t22 () (tptp.combc @t13 @t15 @t14)) % 0.50/0.79 (define @t23 () (tptp.fun @t15 @t17)) % 0.50/0.79 (define @t24 () (tptp.fun @t13 @t20)) % 0.50/0.79 (define @t25 () (@list @t13 @t15 @t14)) % 0.50/0.79 (define @t26 () (tptp.combi @t13)) % 0.50/0.79 (define @t27 () (tptp.fun @t13 @t13)) % 0.50/0.79 (define @t28 () (@list @t13)) % 0.50/0.79 (define @t29 () (tptp.combk @t13 @t15)) % 0.50/0.79 (define @t30 () (tptp.fun @t15 @t13)) % 0.50/0.79 (define @t31 () (@list @t13 @t15)) % 0.50/0.79 (define @t32 () (tptp.combs @t13 @t15 @t14)) % 0.50/0.79 (define @t33 () (tptp.finite_card tptp.arrow_1384031255e_indi)) % 0.50/0.79 (define @t34 () (tptp.inj_on @t13 @t15)) % 0.50/0.79 (define @t35 () (tptp.fun @t13 tptp.bool)) % 0.50/0.79 (define @t36 () (tptp.fun @t35 tptp.bool)) % 0.50/0.79 (define @t37 () (tptp.pi @t13 @t15)) % 0.50/0.79 (define @t38 () (tptp.fun @t18 tptp.bool)) % 0.50/0.79 (define @t39 () (tptp.fun @t15 tptp.bool)) % 0.50/0.79 (define @t40 () (tptp.fun @t13 @t39)) % 0.50/0.79 (define @t41 () (tptp.fun @t40 @t38)) % 0.50/0.79 (define @t42 () (tptp.undefined @t13)) % 0.50/0.79 (define @t43 () (tptp.hilbert_inv_into @t13 @t15)) % 0.50/0.79 (define @t44 () (tptp.fun @t18 @t30)) % 0.50/0.79 (define @t45 () (tptp.if @t13)) % 0.50/0.79 (define @t46 () (tptp.fun @t13 @t27)) % 0.50/0.79 (define @t47 () (tptp.ord_less @t13)) % 0.50/0.79 (define @t48 () (tptp.fun @t13 @t35)) % 0.50/0.79 (define @t49 () (tptp.ord @t13)) % 0.50/0.79 (define @t50 () (tptp.top_top @t13)) % 0.50/0.79 (define @t51 () (tptp.top @t13)) % 0.50/0.79 (define @t52 () (tptp.product_Pair @t13 @t15)) % 0.50/0.79 (define @t53 () (tptp.product_prod @t13 @t15)) % 0.50/0.79 (define @t54 () (tptp.fun @t15 @t53)) % 0.50/0.79 (define @t55 () (tptp.product_prod_rec @t15 @t14 @t13)) % 0.50/0.79 (define @t56 () (tptp.product_prod @t15 @t14)) % 0.50/0.79 (define @t57 () (tptp.fun @t56 @t13)) % 0.50/0.79 (define @t58 () (tptp.fun @t14 @t13)) % 0.50/0.79 (define @t59 () (tptp.fun @t15 @t58)) % 0.50/0.79 (define @t60 () (tptp.collect @t13)) % 0.50/0.79 (define @t61 () (tptp.fequal @t13)) % 0.50/0.79 (define @t62 () (@var "B_2_1" $$unsorted)) % 0.50/0.79 (define @t63 () (@var "B_1_1" $$unsorted)) % 0.50/0.79 (define @t64 () (tptp.hAPP @t13 @t14 @t63 @t62)) % 0.50/0.79 (define @t65 () (@list @t13 @t14 @t63 @t62)) % 0.50/0.79 (define @t66 () (tptp.member @t13)) % 0.50/0.79 (define @t67 () (tptp.fun tptp.arrow_1384031255e_indi tptp.nat)) % 0.50/0.79 (define @t68 () (tptp.member @t3)) % 0.50/0.79 (define @t69 () (tptp.fun @t7 tptp.bool)) % 0.50/0.79 (define @t70 () (@var "L" $$unsorted)) % 0.50/0.79 (define @t71 () (@var "Y_1" $$unsorted)) % 0.50/0.79 (define @t72 () (@var "X_2" $$unsorted)) % 0.50/0.79 (define @t73 () (tptp.product_Pair tptp.arrow_1212486748le_alt tptp.arrow_1212486748le_alt)) % 0.50/0.79 (define @t74 () (tptp.fun tptp.arrow_1212486748le_alt @t1)) % 0.50/0.79 (define @t75 () (tptp.hAPP tptp.arrow_1212486748le_alt @t74 @t73 @t72)) % 0.50/0.79 (define @t76 () (tptp.member @t1)) % 0.50/0.79 (define @t77 () (tptp.hAPP @t1 @t6 @t76 (tptp.hAPP tptp.arrow_1212486748le_alt @t1 @t75 @t71))) % 0.50/0.79 (define @t78 () (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t77 @t70))) % 0.50/0.79 (define @t79 () (@var "Z_1" $$unsorted)) % 0.50/0.79 (define @t80 () (tptp.ti tptp.arrow_1212486748le_alt @t79)) % 0.50/0.79 (define @t81 () (tptp.ti tptp.arrow_1212486748le_alt @t72)) % 0.50/0.79 (define @t82 () (= @t81 @t80)) % 0.50/0.79 (define @t83 () (not @t82)) % 0.50/0.79 (define @t84 () (tptp.ti tptp.arrow_1212486748le_alt @t71)) % 0.50/0.79 (define @t85 () (not (= @t81 @t84))) % 0.50/0.79 (define @t86 () (= @t84 @t80)) % 0.50/0.79 (define @t87 () (not @t86)) % 0.50/0.79 (define @t88 () (tptp.hAPP @t2 @t8 tptp.arrow_844286440_mkbot @t70)) % 0.50/0.79 (define @t89 () (@list @t72 @t71 @t70 @t79)) % 0.50/0.79 (define @t90 () (tptp.hAPP @t2 @t8 tptp.arrow_992993526_mktop @t70)) % 0.50/0.79 (define @t91 () (@var "P_1" $$unsorted)) % 0.50/0.79 (define @t92 () (tptp.hAPP @t3 @t2 tptp.f @t91)) % 0.50/0.79 (define @t93 () (@var "B_3" $$unsorted)) % 0.50/0.79 (define @t94 () (@var "A_4" $$unsorted)) % 0.50/0.79 (define @t95 () (tptp.hAPP @t1 @t6 @t76 (tptp.hAPP tptp.arrow_1212486748le_alt @t1 (tptp.hAPP tptp.arrow_1212486748le_alt @t74 @t73 @t94) @t93))) % 0.50/0.79 (define @t96 () (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t95 @t92))) % 0.50/0.79 (define @t97 () (@var "Pa" $$unsorted)) % 0.50/0.79 (define @t98 () (@var "Ba" $$unsorted)) % 0.50/0.79 (define @t99 () (@var "Aa" $$unsorted)) % 0.50/0.79 (define @t100 () (tptp.hAPP tptp.arrow_1212486748le_alt @t74 @t73 @t99)) % 0.50/0.79 (define @t101 () (tptp.hAPP @t1 @t6 @t76 (tptp.hAPP tptp.arrow_1212486748le_alt @t1 @t100 @t98))) % 0.50/0.79 (define @t102 () (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t101 (tptp.hAPP @t3 @t2 tptp.f @t97)))) % 0.50/0.79 (define @t103 () (@var "I" $$unsorted)) % 0.50/0.79 (define @t104 () (tptp.hAPP tptp.arrow_1384031255e_indi @t2 @t91 @t103)) % 0.50/0.79 (define @t105 () (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t101 (tptp.hAPP tptp.arrow_1384031255e_indi @t2 @t97 @t103)))) % 0.50/0.79 (define @t106 () (@list @t103)) % 0.50/0.79 (define @t107 () (forall @t106 (= @t105 (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t95 @t104))))) % 0.50/0.79 (define @t108 () (tptp.hBOOL (tptp.hAPP @t7 tptp.bool (tptp.hAPP @t3 @t69 @t68 @t91) tptp.arrow_1834574746e_Prof))) % 0.50/0.79 (define @t109 () (tptp.hBOOL (tptp.hAPP @t7 tptp.bool (tptp.hAPP @t3 @t69 @t68 @t97) tptp.arrow_1834574746e_Prof))) % 0.50/0.79 (define @t110 () (=> @t109 (=> @t108 (=> @t107 (= @t102 @t96))))) % 0.50/0.79 (define @t111 () (tptp.ti tptp.arrow_1212486748le_alt @t94)) % 0.50/0.79 (define @t112 () (tptp.ti tptp.arrow_1212486748le_alt @t98)) % 0.50/0.79 (define @t113 () (not (= @t112 @t111))) % 0.50/0.79 (define @t114 () (tptp.ti tptp.arrow_1212486748le_alt @t93)) % 0.50/0.79 (define @t115 () (tptp.ti tptp.arrow_1212486748le_alt @t99)) % 0.50/0.79 (define @t116 () (not (= @t115 @t114))) % 0.50/0.79 (define @t117 () (not (= @t111 @t114))) % 0.50/0.79 (define @t118 () (not (= @t115 @t112))) % 0.50/0.79 (define @t119 () (@list @t91 @t97 @t94 @t93 @t99 @t98)) % 0.50/0.79 (define @t120 () (@var "Ca" $$unsorted)) % 0.50/0.79 (define @t121 () (tptp.hAPP tptp.arrow_1212486748le_alt @t74 @t73 @t98)) % 0.50/0.79 (define @t122 () (tptp.hAPP @t1 @t6 @t76 (tptp.hAPP tptp.arrow_1212486748le_alt @t1 @t121 @t120))) % 0.50/0.79 (define @t123 () (tptp.ti tptp.arrow_1212486748le_alt @t120)) % 0.50/0.79 (define @t124 () (tptp.hAPP @t1 @t6 @t76 (tptp.hAPP tptp.arrow_1212486748le_alt @t1 @t121 @t99))) % 0.50/0.79 (define @t125 () (tptp.hAPP tptp.arrow_1384031255e_indi @t2 tptp.p @t103)) % 0.50/0.79 (define @t126 () (tptp.hAPP tptp.arrow_1212486748le_alt @t2 (tptp.hAPP @t2 @t8 tptp.arrow_844286440_mkbot @t125) tptp.e)) % 0.50/0.79 (define @t127 () (tptp.hAPP tptp.arrow_1212486748le_alt @t74 @t73 tptp.c)) % 0.50/0.79 (define @t128 () (tptp.hAPP @t1 @t6 @t76 (tptp.hAPP tptp.arrow_1212486748le_alt @t1 @t127 tptp.d))) % 0.50/0.79 (define @t129 () (tptp.hAPP tptp.arrow_1384031255e_indi tptp.nat tptp.h @t103)) % 0.50/0.79 (define @t130 () (= @t129 tptp.n)) % 0.50/0.79 (define @t131 () (not @t130)) % 0.50/0.79 (define @t132 () (tptp.hAPP tptp.arrow_1212486748le_alt @t2 (tptp.hAPP tptp.arrow_1212486748le_alt @t8 (tptp.hAPP @t2 @t9 tptp.arrow_1726925404_above @t125) tptp.c) tptp.e)) % 0.50/0.79 (define @t133 () (tptp.ord_less tptp.nat)) % 0.50/0.79 (define @t134 () (tptp.fun tptp.nat tptp.bool)) % 0.50/0.79 (define @t135 () (tptp.hBOOL (tptp.hAPP tptp.nat tptp.bool (tptp.hAPP tptp.nat @t134 @t133 @t129) tptp.n))) % 0.50/0.79 (define @t136 () (not @t135)) % 0.50/0.79 (define @t137 () (tptp.hAPP tptp.arrow_1212486748le_alt @t2 (tptp.hAPP @t2 @t8 tptp.arrow_992993526_mktop @t125) tptp.e)) % 0.50/0.79 (define @t138 () (tptp.top_top @t11)) % 0.50/0.79 (define @t139 () (tptp.fun tptp.nat tptp.arrow_1384031255e_indi)) % 0.50/0.79 (define @t140 () (tptp.combb @t2 @t8 tptp.arrow_1384031255e_indi)) % 0.50/0.79 (define @t141 () (tptp.fun tptp.arrow_1384031255e_indi @t8)) % 0.50/0.79 (define @t142 () (tptp.fun @t3 @t141)) % 0.50/0.79 (define @t143 () (tptp.combc tptp.arrow_1384031255e_indi tptp.arrow_1212486748le_alt @t2)) % 0.50/0.79 (define @t144 () (tptp.fun tptp.arrow_1212486748le_alt @t3)) % 0.50/0.79 (define @t145 () (tptp.fun tptp.arrow_1384031255e_indi @t9)) % 0.50/0.79 (define @t146 () (tptp.combb tptp.nat @t134 tptp.arrow_1384031255e_indi)) % 0.50/0.79 (define @t147 () (tptp.fun tptp.arrow_1384031255e_indi @t134)) % 0.50/0.79 (define @t148 () (tptp.fun @t67 @t147)) % 0.50/0.79 (define @t149 () (tptp.fun tptp.nat @t134)) % 0.50/0.79 (define @t150 () (tptp.combc tptp.arrow_1384031255e_indi tptp.nat tptp.bool)) % 0.50/0.79 (define @t151 () (tptp.fun tptp.nat @t11)) % 0.50/0.79 (define @t152 () (tptp.fun @t2 @t2)) % 0.50/0.79 (define @t153 () (tptp.fun @t2 @t152)) % 0.50/0.79 (define @t154 () (tptp.fun tptp.arrow_1384031255e_indi @t153)) % 0.50/0.79 (define @t155 () (tptp.hAPP (tptp.fun tptp.bool @t153) (tptp.fun @t11 @t154) (tptp.combb tptp.bool @t153 tptp.arrow_1384031255e_indi) (tptp.if @t2))) % 0.50/0.79 (define @t156 () (tptp.combs tptp.arrow_1384031255e_indi @t2 @t152)) % 0.50/0.79 (define @t157 () (tptp.fun tptp.arrow_1384031255e_indi @t152)) % 0.50/0.79 (define @t158 () (tptp.fun @t3 @t157)) % 0.50/0.79 (define @t159 () (tptp.combs tptp.arrow_1384031255e_indi @t2 @t2)) % 0.50/0.79 (define @t160 () (tptp.fun @t3 @t3)) % 0.50/0.79 (define @t161 () (tptp.hAPP @t147 @t151 @t150 (tptp.hAPP @t67 @t147 (tptp.hAPP @t149 @t148 @t146 @t133) tptp.h))) % 0.50/0.79 (define @t162 () (tptp.hAPP @t11 @t154 @t155 (tptp.hAPP tptp.nat @t11 @t161 tptp.n))) % 0.50/0.79 (define @t163 () (tptp.hAPP @t3 @t3 (tptp.hAPP @t157 @t160 @t159 (tptp.hAPP @t3 @t157 (tptp.hAPP @t154 @t158 @t156 @t162) (tptp.hAPP tptp.arrow_1212486748le_alt @t3 (tptp.hAPP @t141 @t144 @t143 (tptp.hAPP @t3 @t141 (tptp.hAPP @t12 @t142 @t140 tptp.arrow_992993526_mktop) tptp.p)) tptp.e))) (tptp.hAPP @t3 @t3 (tptp.hAPP @t157 @t160 @t159 (tptp.hAPP @t3 @t157 (tptp.hAPP @t154 @t158 @t156 (tptp.hAPP @t11 @t154 @t155 (tptp.hAPP tptp.nat @t11 (tptp.hAPP @t147 @t151 @t150 (tptp.hAPP @t67 @t147 (tptp.hAPP @t149 @t148 @t146 (tptp.fequal tptp.nat)) tptp.h)) tptp.n))) (tptp.hAPP tptp.arrow_1212486748le_alt @t3 (tptp.hAPP @t141 @t144 @t143 (tptp.hAPP tptp.arrow_1212486748le_alt @t141 (tptp.hAPP @t145 (tptp.fun tptp.arrow_1212486748le_alt @t141) (tptp.combc tptp.arrow_1384031255e_indi tptp.arrow_1212486748le_alt @t8) (tptp.hAPP @t3 @t145 (tptp.hAPP @t10 (tptp.fun @t3 @t145) (tptp.combb @t2 @t9 tptp.arrow_1384031255e_indi) tptp.arrow_1726925404_above) tptp.p)) tptp.c)) tptp.e))) (tptp.hAPP tptp.arrow_1212486748le_alt @t3 (tptp.hAPP @t141 @t144 @t143 (tptp.hAPP @t3 @t141 (tptp.hAPP @t12 @t142 @t140 tptp.arrow_844286440_mkbot) tptp.p)) tptp.e)))) % 0.50/0.79 (define @t164 () (tptp.hAPP @t3 @t2 tptp.f @t163)) % 0.50/0.79 (define @t165 () (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t128 @t164))) % 0.50/0.79 (define @t166 () (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t128 (tptp.hAPP @t3 @t2 tptp.f tptp.p)))) % 0.50/0.79 (define @t167 () (@var "B_1" $$unsorted)) % 0.50/0.79 (define @t168 () (@var "A_2" $$unsorted)) % 0.50/0.79 (define @t169 () (@list @t168 @t167)) % 0.50/0.79 (define @t170 () (@var "X1" $$unsorted)) % 0.50/0.79 (define @t171 () (tptp.hAPP @t1 @t6 @t76 (tptp.hAPP tptp.arrow_1212486748le_alt @t1 (tptp.hAPP tptp.arrow_1212486748le_alt @t74 @t73 tptp.e) tptp.d))) % 0.50/0.79 (define @t172 () (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t171 @t164))) % 0.50/0.79 (define @t173 () (@var "B_4" $$unsorted)) % 0.50/0.79 (define @t174 () (@var "B_2" $$unsorted)) % 0.50/0.79 (define @t175 () (@var "A_5" $$unsorted)) % 0.50/0.79 (define @t176 () (@var "A_3" $$unsorted)) % 0.50/0.79 (define @t177 () (tptp.ti @t13 @t99)) % 0.50/0.79 (define @t178 () (@var "Xa" $$unsorted)) % 0.50/0.79 (define @t179 () (@var "Fa" $$unsorted)) % 0.50/0.79 (define @t180 () (tptp.hAPP @t1 @t6 @t76 (tptp.hAPP tptp.arrow_1212486748le_alt @t1 (tptp.hAPP tptp.arrow_1212486748le_alt @t74 @t73 @t168) @t167))) % 0.50/0.79 (define @t181 () (@var "X_1" $$unsorted)) % 0.50/0.79 (define @t182 () (tptp.hAPP @t3 @t2 @t179 @t181)) % 0.50/0.79 (define @t183 () (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t180 @t182))) % 0.50/0.79 (define @t184 () (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t180 (tptp.hAPP tptp.arrow_1384031255e_indi @t2 @t181 @t103)))) % 0.50/0.79 (define @t185 () (@list @t178)) % 0.50/0.79 (define @t186 () (tptp.hBOOL (tptp.hAPP @t7 tptp.bool (tptp.hAPP @t3 @t69 @t68 @t181) tptp.arrow_1834574746e_Prof))) % 0.50/0.79 (define @t187 () (@list @t181)) % 0.50/0.79 (define @t188 () (@list @t179)) % 0.50/0.79 (define @t189 () (tptp.top_top @t35)) % 0.50/0.79 (define @t190 () (@list @t13 @t72)) % 0.50/0.79 (define @t191 () (tptp.hAPP @t13 @t36 @t66 @t72)) % 0.50/0.79 (define @t192 () (@var "F1" $$unsorted)) % 0.50/0.79 (define @t193 () (@var "X" $$unsorted)) % 0.50/0.79 (define @t194 () (@var "Y" $$unsorted)) % 0.50/0.79 (define @t195 () (tptp.hAPP @t13 @t35 @t47 @t194)) % 0.50/0.79 (define @t196 () (tptp.hBOOL (tptp.hAPP @t13 tptp.bool @t195 @t193))) % 0.50/0.79 (define @t197 () (tptp.ti @t13 @t194)) % 0.50/0.79 (define @t198 () (tptp.ti @t13 @t193)) % 0.50/0.79 (define @t199 () (= @t198 @t197)) % 0.50/0.79 (define @t200 () (not @t199)) % 0.50/0.79 (define @t201 () (tptp.hAPP @t13 @t35 @t47 @t193)) % 0.50/0.79 (define @t202 () (tptp.hBOOL (tptp.hAPP @t13 tptp.bool @t201 @t194))) % 0.50/0.79 (define @t203 () (not @t202)) % 0.50/0.79 (define @t204 () (@list @t193 @t194)) % 0.50/0.79 (define @t205 () (tptp.linorder @t13)) % 0.50/0.79 (define @t206 () (tptp.preorder @t13)) % 0.50/0.79 (define @t207 () (@var "Z" $$unsorted)) % 0.50/0.79 (define @t208 () (tptp.hAPP @t13 @t35 @t47 @t207)) % 0.50/0.79 (define @t209 () (tptp.order @t13)) % 0.50/0.79 (define @t210 () (@var "C" $$unsorted)) % 0.50/0.79 (define @t211 () (tptp.hAPP @t13 @t35 @t47 @t210)) % 0.50/0.79 (define @t212 () (tptp.hBOOL (tptp.hAPP @t13 tptp.bool @t211 @t176))) % 0.50/0.79 (define @t213 () (= @t174 @t210)) % 0.50/0.79 (define @t214 () (tptp.hAPP @t13 @t35 @t47 @t174)) % 0.50/0.79 (define @t215 () (tptp.hBOOL (tptp.hAPP @t13 tptp.bool @t214 @t176))) % 0.50/0.79 (define @t216 () (tptp.hAPP @t13 @t35 @t47 @t176)) % 0.50/0.79 (define @t217 () (tptp.hBOOL (tptp.hAPP @t13 tptp.bool @t216 @t210))) % 0.50/0.79 (define @t218 () (tptp.hBOOL (tptp.hAPP @t13 tptp.bool @t216 @t174))) % 0.50/0.79 (define @t219 () (@list @t210 @t176 @t174)) % 0.50/0.79 (define @t220 () (= @t176 @t174)) % 0.50/0.79 (define @t221 () (tptp.hBOOL (tptp.hAPP @t13 tptp.bool (tptp.hAPP @t13 @t35 @t47 @t71) @t72))) % 0.50/0.79 (define @t222 () (tptp.hBOOL (tptp.hAPP @t13 tptp.bool (tptp.hAPP @t13 @t35 @t47 @t72) @t71))) % 0.50/0.79 (define @t223 () (tptp.ti @t13 @t72)) % 0.50/0.79 (define @t224 () (= @t223 (tptp.ti @t13 @t71))) % 0.50/0.79 (define @t225 () (not @t222)) % 0.50/0.79 (define @t226 () (@list @t72 @t71)) % 0.50/0.79 (define @t227 () (not @t224)) % 0.50/0.79 (define @t228 () (@var "S" $$unsorted)) % 0.50/0.79 (define @t229 () (tptp.fun @t53 tptp.bool)) % 0.50/0.79 (define @t230 () (@var "R_1" $$unsorted)) % 0.50/0.79 (define @t231 () (tptp.hAPP @t53 (tptp.fun @t229 tptp.bool) (tptp.member @t53) (tptp.hAPP @t15 @t53 (tptp.hAPP @t13 @t54 @t52 @t181) @t178))) % 0.50/0.79 (define @t232 () (@var "F" $$unsorted)) % 0.50/0.79 (define @t233 () (tptp.hAPP @t18 @t30 (tptp.hAPP @t35 @t44 @t43 @t189) @t232)) % 0.50/0.79 (define @t234 () (tptp.hAPP @t13 @t15 @t232 @t72)) % 0.50/0.79 (define @t235 () (= @t234 (tptp.ti @t15 @t71))) % 0.50/0.79 (define @t236 () (tptp.hAPP @t18 @t36 @t34 @t232)) % 0.50/0.79 (define @t237 () (tptp.hBOOL (tptp.hAPP @t35 tptp.bool @t236 @t189))) % 0.50/0.79 (define @t238 () (@list @t13 @t15 @t72 @t71 @t232)) % 0.50/0.79 (define @t239 () (tptp.fun @t14 @t15)) % 0.50/0.79 (define @t240 () (tptp.fun @t13 @t239)) % 0.50/0.79 (define @t241 () (@var "A_1" $$unsorted)) % 0.50/0.79 (define @t242 () (tptp.hAPP @t18 @t30 (tptp.hAPP @t35 @t44 @t43 @t241) @t232)) % 0.50/0.79 (define @t243 () (tptp.hBOOL (tptp.hAPP @t35 tptp.bool @t191 @t241))) % 0.50/0.79 (define @t244 () (tptp.hBOOL (tptp.hAPP @t35 tptp.bool @t236 @t241))) % 0.50/0.79 (define @t245 () (@list @t13 @t15 @t71 @t72 @t232 @t241)) % 0.50/0.79 (define @t246 () (= @t234 (tptp.hAPP @t13 @t15 @t232 @t71))) % 0.50/0.79 (define @t247 () (= @t246 @t224)) % 0.50/0.79 (define @t248 () (tptp.ti @t13 @t181)) % 0.50/0.79 (define @t249 () (tptp.hAPP @t13 @t15 @t232 @t181)) % 0.50/0.79 (define @t250 () (tptp.hBOOL (tptp.hAPP @t35 tptp.bool (tptp.hAPP @t13 @t36 @t66 @t71) @t241))) % 0.50/0.79 (define @t251 () (@list @t13 @t15 @t72 @t71 @t232 @t241)) % 0.50/0.79 (define @t252 () (@list @t13 @t241)) % 0.50/0.79 (define @t253 () (@var "G" $$unsorted)) % 0.50/0.79 (define @t254 () (@var "Y_2" $$unsorted)) % 0.50/0.79 (define @t255 () (tptp.fun @t3 @t6)) % 0.50/0.79 (define @t256 () (tptp.hAPP @t255 @t5 (tptp.hAPP @t7 (tptp.fun @t255 @t5) (tptp.pi @t3 @t2) tptp.arrow_1834574746e_Prof) (tptp.hAPP @t6 @t255 (tptp.combk @t6 @t3) tptp.arrow_638930832le_Lin))) % 0.50/0.79 (define @t257 () (tptp.member @t4)) % 0.50/0.79 (define @t258 () (tptp.fun @t5 tptp.bool)) % 0.50/0.79 (define @t259 () (tptp.member @t2)) % 0.50/0.79 (define @t260 () (tptp.fun @t6 tptp.bool)) % 0.50/0.79 (define @t261 () (tptp.hBOOL (tptp.hAPP @t6 tptp.bool (tptp.hAPP @t2 @t260 @t259 @t70) tptp.arrow_638930832le_Lin))) % 0.50/0.79 (define @t262 () (@list @t72 @t70)) % 0.50/0.79 (define @t263 () (tptp.hAPP @t2 @t9 tptp.arrow_1726925404_above @t70)) % 0.50/0.79 (define @t264 () (= @t84 @t112)) % 0.50/0.79 (define @t265 () (= @t81 @t112)) % 0.50/0.79 (define @t266 () (@var "I_1" $$unsorted)) % 0.50/0.79 (define @t267 () (tptp.hBOOL (tptp.hAPP tptp.arrow_1384031255e_indi tptp.bool (tptp.hAPP @t4 @t11 tptp.arrow_1990387629ctator @t179) @t266))) % 0.50/0.79 (define @t268 () (tptp.hAPP tptp.arrow_1384031255e_indi @t2 @t181 @t266)) % 0.50/0.79 (define @t269 () (@var "B" $$unsorted)) % 0.50/0.79 (define @t270 () (tptp.hAPP @t15 (tptp.fun @t39 tptp.bool) (tptp.member @t15) @t234)) % 0.50/0.79 (define @t271 () (tptp.hBOOL (tptp.hAPP @t39 tptp.bool @t270 (tptp.hAPP @t13 @t39 @t269 @t72)))) % 0.50/0.79 (define @t272 () (tptp.hAPP @t35 @t41 @t37 @t241)) % 0.50/0.79 (define @t273 () (tptp.hAPP @t18 (tptp.fun @t38 tptp.bool) (tptp.member @t18) @t232)) % 0.50/0.79 (define @t274 () (tptp.hBOOL (tptp.hAPP @t38 tptp.bool @t273 (tptp.hAPP @t40 @t38 @t272 @t269)))) % 0.50/0.79 (define @t275 () (@list @t13 @t15 @t72 @t232 @t241 @t269)) % 0.50/0.79 (define @t276 () (@var "Na" $$unsorted)) % 0.50/0.79 (define @t277 () (tptp.combc tptp.arrow_1384031255e_indi @t2 @t152)) % 0.50/0.79 (define @t278 () (tptp.fun @t2 @t157)) % 0.50/0.79 (define @t279 () (tptp.combc tptp.arrow_1384031255e_indi @t2 @t2)) % 0.50/0.79 (define @t280 () (tptp.fun @t2 @t3)) % 0.50/0.79 (define @t281 () (tptp.fun tptp.arrow_1384031255e_indi @t6)) % 0.50/0.79 (define @t282 () (tptp.combk @t39 @t13)) % 0.50/0.79 (define @t283 () (tptp.fun @t27 tptp.bool)) % 0.50/0.79 (define @t284 () (tptp.hAPP @t1 @t6 @t76 (tptp.hAPP tptp.arrow_1212486748le_alt @t1 (tptp.hAPP tptp.arrow_1212486748le_alt @t74 @t73 tptp.b) tptp.a))) % 0.50/0.79 (define @t285 () (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t284 tptp.lba))) % 0.50/0.79 (define @t286 () (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t284 tptp.lab))) % 0.50/0.79 (define @t287 () (tptp.hAPP @t1 @t6 @t76 (tptp.hAPP tptp.arrow_1212486748le_alt @t1 (tptp.hAPP tptp.arrow_1212486748le_alt @t74 @t73 tptp.a) tptp.b))) % 0.50/0.79 (define @t288 () (@var "T_1" $$unsorted)) % 0.50/0.79 (define @t289 () (@var "T_2" $$unsorted)) % 0.50/0.79 (define @t290 () (tptp.fun @t289 @t288)) % 0.50/0.79 (define @t291 () (@list @t289 @t288)) % 0.50/0.79 (define @t292 () (@var "A" $$unsorted)) % 0.50/0.79 (define @t293 () (@var "T" $$unsorted)) % 0.50/0.79 (define @t294 () (tptp.ti @t293 @t292)) % 0.50/0.79 (define @t295 () (@list @t13 @t193 @t194)) % 0.50/0.79 (define @t296 () (@var "P" $$unsorted)) % 0.50/0.79 (define @t297 () (tptp.ti tptp.bool @t296)) % 0.50/0.79 (define @t298 () (@var "R" $$unsorted)) % 0.50/0.79 (define @t299 () (@var "Q" $$unsorted)) % 0.50/0.79 (define @t300 () (tptp.hAPP @t13 @t15 @t299 @t298)) % 0.50/0.79 (define @t301 () (@list @t13 @t14 @t15 @t296 @t299 @t298)) % 0.50/0.79 (define @t302 () (tptp.hAPP @t13 @t20 @t296 @t298)) % 0.50/0.79 (define @t303 () (tptp.ti @t13 @t296)) % 0.50/0.79 (define @t304 () (tptp.hBOOL (tptp.hAPP @t13 tptp.bool (tptp.hAPP @t13 @t35 @t61 @t193) @t194))) % 0.50/0.79 (define @t305 () (@list false)) % 0.50/0.79 (assume @p1 (= (tptp.ti @t5 tptp.arrow_612047104le_IIA) tptp.arrow_612047104le_IIA)) % 0.50/0.79 (assume @p2 (= (tptp.ti @t6 tptp.arrow_638930832le_Lin) tptp.arrow_638930832le_Lin)) % 0.50/0.79 (assume @p3 (= (tptp.ti @t7 tptp.arrow_1834574746e_Prof) tptp.arrow_1834574746e_Prof)) % 0.50/0.79 (assume @p4 (= (tptp.ti @t10 tptp.arrow_1726925404_above) tptp.arrow_1726925404_above)) % 0.50/0.79 (assume @p5 (= (tptp.ti (tptp.fun @t4 @t11) tptp.arrow_1990387629ctator) tptp.arrow_1990387629ctator)) % 0.50/0.79 (assume @p6 (= (tptp.ti @t12 tptp.arrow_844286440_mkbot) tptp.arrow_844286440_mkbot)) % 0.50/0.79 (assume @p7 (= (tptp.ti @t12 tptp.arrow_992993526_mktop) tptp.arrow_992993526_mktop)) % 0.50/0.79 (assume @p8 (= (tptp.ti @t5 tptp.arrow_1932713123nimity) tptp.arrow_1932713123nimity)) % 0.50/0.79 (assume @p9 (forall @t21 (= (tptp.ti (tptp.fun @t20 @t19) @t16) @t16))) % 0.50/0.79 (assume @p10 (forall @t25 (= (tptp.ti (tptp.fun @t24 @t23) @t22) @t22))) % 0.50/0.79 (assume @p11 (forall @t28 (= (tptp.ti @t27 @t26) @t26))) % 0.50/0.79 (assume @p12 (forall @t31 (= (tptp.ti (tptp.fun @t13 @t30) @t29) @t29))) % 0.50/0.79 (assume @p13 (forall @t25 (= (tptp.ti (tptp.fun @t24 @t19) @t32) @t32))) % 0.50/0.79 (assume @p14 (= (tptp.ti (tptp.fun @t11 tptp.nat) @t33) @t33)) % 0.50/0.79 (assume @p15 (forall @t31 (= (tptp.ti (tptp.fun @t18 @t36) @t34) @t34))) % 0.50/0.79 (assume @p16 (forall @t31 (= (tptp.ti (tptp.fun @t35 @t41) @t37) @t37))) % 0.50/0.79 (assume @p17 (forall @t28 (= (tptp.ti @t13 @t42) @t42))) % 0.50/0.79 (assume @p18 (forall @t31 (= (tptp.ti (tptp.fun @t35 @t44) @t43) @t43))) % 0.50/0.79 (assume @p19 (forall @t28 (= (tptp.ti (tptp.fun tptp.bool @t46) @t45) @t45))) % 0.50/0.79 (assume @p20 (forall @t28 (=> @t49 (= (tptp.ti @t48 @t47) @t47)))) % 0.50/0.79 (assume @p21 (forall @t28 (=> @t51 (= (tptp.ti @t13 @t50) @t50)))) % 0.50/0.79 (assume @p22 (forall @t31 (= (tptp.ti (tptp.fun @t13 @t54) @t52) @t52))) % 0.50/0.79 (assume @p23 (forall @t21 (= (tptp.ti (tptp.fun @t59 @t57) @t55) @t55))) % 0.50/0.79 (assume @p24 (forall @t28 (= (tptp.ti (tptp.fun @t35 @t35) @t60) @t60))) % 0.50/0.79 (assume @p25 (= (tptp.ti tptp.bool tptp.fFalse) tptp.fFalse)) % 0.50/0.79 (assume @p26 (= (tptp.ti tptp.bool tptp.fTrue) tptp.fTrue)) % 0.50/0.79 (assume @p27 (forall @t28 (= (tptp.ti @t48 @t61) @t61))) % 0.50/0.79 (assume @p28 (forall @t65 (= (tptp.hAPP @t13 @t14 (tptp.ti @t17 @t63) @t62) @t64))) % 0.50/0.79 (assume @p29 (forall @t65 (= (tptp.hAPP @t13 @t14 @t63 (tptp.ti @t13 @t62)) @t64))) % 0.50/0.79 (assume @p30 (forall (@list @t14 @t13 @t63 @t62) (= (tptp.ti @t14 @t64) @t64))) % 0.50/0.79 (assume @p31 (forall (@list @t63) (= (tptp.hBOOL (tptp.ti tptp.bool @t63)) (tptp.hBOOL @t63)))) % 0.50/0.79 (assume @p32 (forall @t28 (= (tptp.ti (tptp.fun @t13 @t36) @t66) @t66))) % 0.50/0.79 (assume @p33 (= (tptp.ti @t4 tptp.f) tptp.f)) % 0.50/0.79 (assume @p34 (= (tptp.ti @t2 tptp.lab) tptp.lab)) % 0.50/0.79 (assume @p35 (= (tptp.ti @t2 tptp.lba) tptp.lba)) % 0.50/0.79 (assume @p36 (= (tptp.ti @t3 tptp.p) tptp.p)) % 0.50/0.79 (assume @p37 (= (tptp.ti tptp.arrow_1212486748le_alt tptp.a) tptp.a)) % 0.50/0.79 (assume @p38 (= (tptp.ti tptp.arrow_1212486748le_alt tptp.b) tptp.b)) % 0.50/0.79 (assume @p39 (= (tptp.ti tptp.arrow_1212486748le_alt tptp.c) tptp.c)) % 0.50/0.79 (assume @p40 (= (tptp.ti tptp.arrow_1212486748le_alt tptp.d) tptp.d)) % 0.50/0.79 (assume @p41 (= (tptp.ti tptp.arrow_1212486748le_alt tptp.e) tptp.e)) % 0.50/0.79 (assume @p42 (= (tptp.ti @t67 tptp.h) tptp.h)) % 0.50/0.79 (assume @p43 (= (tptp.ti tptp.nat tptp.n) tptp.n)) % 0.50/0.79 (assume @p44 (tptp.hBOOL (tptp.hAPP @t4 tptp.bool tptp.arrow_612047104le_IIA tptp.f))) % 0.50/0.79 (assume @p45 (tptp.hBOOL (tptp.hAPP @t4 tptp.bool tptp.arrow_1932713123nimity tptp.f))) % 0.50/0.79 (assume @p46 (not (= tptp.c tptp.d))) % 0.50/0.79 (assume @p47 (tptp.hBOOL (tptp.hAPP @t7 tptp.bool (tptp.hAPP @t3 @t69 @t68 tptp.p) tptp.arrow_1834574746e_Prof))) % 0.50/0.79 (assume @p48 (forall @t89 (= (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t77 (tptp.hAPP tptp.arrow_1212486748le_alt @t2 @t88 @t79))) (and @t87 (=> @t82 @t85) (=> @t83 @t78))))) % 0.50/0.79 (assume @p49 (forall @t89 (= (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t77 (tptp.hAPP tptp.arrow_1212486748le_alt @t2 @t90 @t79))) (and @t83 (=> @t86 @t85) (=> @t87 @t78))))) % 0.50/0.79 (assume @p50 (forall @t119 (=> @t118 (=> @t117 (=> @t116 (=> @t113 @t110)))))) % 0.50/0.79 (assume @p51 (forall @t119 (=> @t118 (=> @t117 (=> @t116 (=> @t113 (=> @t109 (=> @t108 (=> @t107 (=> @t102 @t96)))))))))) % 0.50/0.79 (assume @p52 (forall (@list @t91 @t97 @t120 @t99 @t98) (=> @t118 (=> (not (= @t112 @t123)) (=> (not (= @t115 @t123)) (=> @t109 (=> @t108 (=> (forall @t106 (= @t105 (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t122 @t104)))) (= @t102 (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t122 @t92))))))))))) % 0.50/0.79 (assume @p53 (forall @t119 (=> @t118 (=> @t117 @t110)))) % 0.50/0.79 (assume @p54 (forall (@list @t91 @t97 @t99 @t98) (=> @t118 (=> @t109 (=> @t108 (=> (forall @t106 (= @t105 (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t124 @t104)))) (= @t102 (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t124 @t92))))))))) % 0.50/0.79 (assume @p55 (forall @t106 (= (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t128 @t125)) (and (=> @t135 (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t128 @t137))) (=> @t136 (and (=> @t130 (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t128 @t132))) (=> @t131 (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t128 @t126))))))))) % 0.50/0.79 (assume @p56 (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t128 (tptp.hAPP tptp.arrow_1384031255e_indi @t2 tptp.p (tptp.hAPP tptp.nat tptp.arrow_1384031255e_indi (tptp.hAPP @t67 @t139 (tptp.hAPP @t11 (tptp.fun @t67 @t139) (tptp.hilbert_inv_into tptp.arrow_1384031255e_indi tptp.nat) @t138) tptp.h) tptp.n))))) % 0.50/0.79 (assume @p57 @t165) % 0.50/0.79 (assume @p58 (= @t166 @t165)) % 0.50/0.79 (assume @p59 (forall (@list @t13 @t15 @t97) (= (forall (@list @t170) (tptp.hBOOL (tptp.hAPP @t53 tptp.bool @t97 @t170))) (forall @t169 (tptp.hBOOL (tptp.hAPP @t53 tptp.bool @t97 (tptp.hAPP @t15 @t53 (tptp.hAPP @t13 @t54 @t52 @t168) @t167))))))) % 0.50/0.79 (assume @p60 (tptp.hBOOL (tptp.hAPP @t7 tptp.bool (tptp.hAPP @t3 @t69 @t68 @t163) tptp.arrow_1834574746e_Prof))) % 0.50/0.79 (assume @p61 (tptp.hBOOL (tptp.hAPP @t2 tptp.bool (tptp.hAPP @t1 @t6 @t76 (tptp.hAPP tptp.arrow_1212486748le_alt @t1 @t127 tptp.e)) @t164))) % 0.50/0.79 (assume @p62 @t172) % 0.50/0.79 (assume @p63 (tptp.hBOOL (tptp.hAPP tptp.nat tptp.bool (tptp.hAPP tptp.nat @t134 @t133 tptp.n) (tptp.hAPP @t11 tptp.nat @t33 @t138)))) % 0.50/0.79 (assume @p64 (tptp.hBOOL (tptp.hAPP @t11 tptp.bool (tptp.hAPP @t67 (tptp.fun @t11 tptp.bool) (tptp.inj_on tptp.arrow_1384031255e_indi tptp.nat) tptp.h) @t138))) % 0.50/0.79 (assume @p65 (forall (@list @t15 @t13 @t176 @t174 @t175 @t173) (=> (= (tptp.hAPP @t15 @t53 (tptp.hAPP @t13 @t54 @t52 @t176) @t174) (tptp.hAPP @t15 @t53 (tptp.hAPP @t13 @t54 @t52 @t175) @t173)) (not (=> (= (tptp.ti @t13 @t176) (tptp.ti @t13 @t175)) (not (= (tptp.ti @t15 @t174) (tptp.ti @t15 @t173)))))))) % 0.50/0.79 (assume @p66 (forall (@list @t15 @t13 @t99 @t98 @t94 @t93) (= (= (tptp.hAPP @t15 @t53 (tptp.hAPP @t13 @t54 @t52 @t99) @t98) (tptp.hAPP @t15 @t53 (tptp.hAPP @t13 @t54 @t52 @t94) @t93)) (and (= @t177 (tptp.ti @t13 @t94)) (= (tptp.ti @t15 @t98) (tptp.ti @t15 @t93)))))) % 0.50/0.79 (assume @p67 (forall @t188 (= (tptp.hBOOL (tptp.hAPP @t4 tptp.bool tptp.arrow_612047104le_IIA @t179)) (forall @t187 (=> @t186 (forall @t185 (=> (tptp.hBOOL (tptp.hAPP @t7 tptp.bool (tptp.hAPP @t3 @t69 @t68 @t178) tptp.arrow_1834574746e_Prof)) (forall @t169 (=> (forall @t106 (= @t184 (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t180 (tptp.hAPP tptp.arrow_1384031255e_indi @t2 @t178 @t103))))) (= @t183 (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t180 (tptp.hAPP @t3 @t2 @t179 @t178))))))))))))) % 0.50/0.79 (assume @p68 (forall @t188 (= (tptp.hBOOL (tptp.hAPP @t4 tptp.bool tptp.arrow_1932713123nimity @t179)) (forall @t187 (=> @t186 (forall @t169 (=> (forall @t106 @t184) @t183))))))) % 0.50/0.79 (assume @p69 (forall @t190 (tptp.hBOOL (tptp.hAPP @t13 tptp.bool @t189 @t72)))) % 0.50/0.79 (assume @p70 (forall @t190 (tptp.hBOOL (tptp.hAPP @t35 tptp.bool @t191 @t189)))) % 0.50/0.79 (assume @p71 (forall (@list @t15 @t14 @t13 @t192 @t99 @t98) (= (tptp.hAPP @t56 @t13 (tptp.hAPP @t59 @t57 @t55 @t192) (tptp.hAPP @t14 @t56 (tptp.hAPP @t15 (tptp.fun @t14 @t56) (tptp.product_Pair @t15 @t14) @t99) @t98)) (tptp.hAPP @t14 @t13 (tptp.hAPP @t15 @t58 @t192 @t99) @t98)))) % 0.50/0.79 (assume @p72 (forall (@list @t15 @t13) (=> @t51 (forall (@list @t72) (= (tptp.hAPP @t15 @t13 (tptp.top_top @t30) @t72) @t50))))) % 0.50/0.79 (assume @p73 (forall @t28 (=> @t51 (forall (@list @t176) (not (tptp.hBOOL (tptp.hAPP @t13 tptp.bool (tptp.hAPP @t13 @t35 @t47 @t50) @t176))))))) % 0.50/0.79 (assume @p74 (forall @t28 (=> @t205 (forall @t204 (=> @t203 (=> @t200 @t196)))))) % 0.50/0.79 (assume @p75 (forall @t28 (=> @t206 (forall @t204 (=> @t202 (not @t196)))))) % 0.50/0.79 (assume @p76 (forall @t28 (=> @t209 (forall (@list @t207 @t194 @t193) (=> @t196 (=> (tptp.hBOOL (tptp.hAPP @t13 tptp.bool @t208 @t194)) (tptp.hBOOL (tptp.hAPP @t13 tptp.bool @t208 @t193)))))))) % 0.50/0.79 (assume @p77 (forall @t28 (=> @t206 (forall (@list @t207 @t193 @t194) (=> @t202 (=> (tptp.hBOOL (tptp.hAPP @t13 tptp.bool @t195 @t207)) (tptp.hBOOL (tptp.hAPP @t13 tptp.bool @t201 @t207)))))))) % 0.50/0.79 (assume @p78 (forall @t28 (=> @t209 (forall (@list @t210 @t174 @t176) (=> @t215 (=> @t213 @t212)))))) % 0.50/0.79 (assume @p79 (forall @t28 (=> @t49 (forall @t219 (=> @t218 (=> @t213 @t217)))))) % 0.50/0.79 (assume @p80 (forall @t28 (=> @t209 (forall @t219 (=> @t220 (=> (tptp.hBOOL (tptp.hAPP @t13 tptp.bool @t211 @t174)) @t212)))))) % 0.50/0.79 (assume @p81 (forall @t28 (=> @t49 (forall @t219 (=> @t220 (=> (tptp.hBOOL (tptp.hAPP @t13 tptp.bool @t214 @t210)) @t217)))))) % 0.50/0.79 (assume @p82 (forall @t28 (=> @t209 (forall (@list @t174 @t176) (=> @t215 (not @t218)))))) % 0.50/0.79 (assume @p83 (forall @t28 (=> @t206 (forall (@list @t176 @t174) (=> @t218 (not @t215)))))) % 0.50/0.79 (assume @p84 (forall @t28 (=> @t206 (forall (@list @t97 @t72 @t71) (=> @t222 (=> @t221 (tptp.hBOOL @t97))))))) % 0.50/0.79 (assume @p85 (forall @t28 (=> @t209 (forall @t204 (=> @t202 (not (= @t194 @t193))))))) % 0.50/0.79 (assume @p86 (forall @t28 (=> @t209 (forall @t204 (=> @t202 (not (= @t193 @t194))))))) % 0.50/0.79 (assume @p87 (forall @t28 (=> @t205 (forall @t204 (=> @t200 (=> @t203 @t196)))))) % 0.50/0.79 (assume @p88 (forall @t28 (=> @t205 (forall (@list @t71 @t72) (=> (not @t221) (= @t225 @t224)))))) % 0.50/0.79 (assume @p89 (forall @t28 (=> @t205 (forall @t204 (or @t202 @t199 @t196))))) % 0.50/0.79 (assume @p90 (forall @t28 (=> @t205 (forall @t226 (= @t225 (or @t221 @t224)))))) % 0.50/0.79 (assume @p91 (forall @t28 (=> @t205 (forall @t226 (= @t227 (or @t222 @t221)))))) % 0.50/0.79 (assume @p92 (forall @t28 (=> @t206 (forall (@list @t193) (not (tptp.hBOOL (tptp.hAPP @t13 tptp.bool @t201 @t193))))))) % 0.50/0.79 (assume @p93 (forall @t28 (= @t189 (tptp.hAPP @t35 @t35 @t60 (tptp.hAPP tptp.bool @t35 (tptp.combk tptp.bool @t13) tptp.fTrue))))) % 0.50/0.79 (assume @p94 (forall (@list @t13 @t15 @t228 @t230) (= (forall (@list @t181 @t178) (= (tptp.hBOOL (tptp.hAPP @t229 tptp.bool @t231 @t230)) (tptp.hBOOL (tptp.hAPP @t229 tptp.bool @t231 @t228)))) (= (tptp.ti @t229 @t230) (tptp.ti @t229 @t228))))) % 0.50/0.79 (assume @p95 (forall @t28 (=> @t51 (forall (@list @t99) (= (not (= @t177 @t50)) (tptp.hBOOL (tptp.hAPP @t13 tptp.bool (tptp.hAPP @t13 @t35 @t47 @t99) @t50))))))) % 0.50/0.79 (assume @p96 (forall @t238 (=> @t237 (=> @t235 (= (tptp.hAPP @t15 @t13 @t233 @t71) @t223))))) % 0.50/0.79 (assume @p97 (forall (@list @t13 @t15 @t72 @t232) (=> @t237 (= (tptp.hAPP @t15 @t13 @t233 @t234) @t223)))) % 0.50/0.79 (assume @p98 (forall (@list @t14 @t13 @t15 @t232) (=> @t237 (tptp.hBOOL (tptp.hAPP @t35 tptp.bool (tptp.hAPP @t240 @t36 (tptp.inj_on @t13 @t239) (tptp.hAPP @t18 @t240 (tptp.hAPP (tptp.fun @t15 @t239) (tptp.fun @t18 @t240) (tptp.combb @t15 @t239 @t13) (tptp.combk @t15 @t14)) @t232)) @t189))))) % 0.50/0.79 (assume @p99 (forall (@list @t13 @t15 @t72 @t232 @t241) (=> @t244 (=> @t243 (= (tptp.hAPP @t15 @t13 @t242 @t234) @t223))))) % 0.50/0.79 (assume @p100 (forall @t245 (=> @t244 (=> @t243 (=> @t235 (= (tptp.hAPP @t15 @t13 @t242 @t71) @t223)))))) % 0.50/0.79 (assume @p101 (forall @t238 (=> @t237 @t247))) % 0.50/0.79 (assume @p102 (forall (@list @t13 @t15 @t232 @t241) (= @t244 (forall @t187 (=> (tptp.hBOOL (tptp.hAPP @t35 tptp.bool (tptp.hAPP @t13 @t36 @t66 @t181) @t241)) (forall @t185 (=> (tptp.hBOOL (tptp.hAPP @t35 tptp.bool (tptp.hAPP @t13 @t36 @t66 @t178) @t241)) (=> (= @t249 (tptp.hAPP @t13 @t15 @t232 @t178)) (= @t248 (tptp.ti @t13 @t178)))))))))) % 0.50/0.79 (assume @p103 (forall @t251 (=> @t244 (=> @t227 (=> @t243 (=> @t250 (not @t246))))))) % 0.50/0.79 (assume @p104 (forall @t245 (=> @t244 (=> @t243 (=> @t250 @t247))))) % 0.50/0.79 (assume @p105 (forall @t251 (=> @t244 (=> @t246 (=> @t243 (=> @t250 @t224)))))) % 0.50/0.79 (assume @p106 (forall @t252 (tptp.hBOOL (tptp.hAPP @t35 tptp.bool (tptp.hAPP @t27 @t36 (tptp.inj_on @t13 @t13) @t26) @t241)))) % 0.50/0.79 (assume @p107 (forall @t238 (=> @t237 (=> @t246 @t224)))) % 0.50/0.79 (assume @p108 (forall (@list @t13 @t15 @t253 @t232) (=> @t237 (=> (forall @t187 (= (tptp.hAPP @t13 @t15 @t232 (tptp.hAPP @t15 @t13 @t253 @t181)) (tptp.ti @t15 @t181))) (= @t233 (tptp.ti @t30 @t253)))))) % 0.50/0.79 (assume @p109 (forall (@list @t13 @t15 @t232) (=> (forall (@list @t181 @t254) (=> (= @t249 (tptp.hAPP @t13 @t15 @t232 @t254)) (= @t248 (tptp.ti @t13 @t254)))) @t237))) % 0.50/0.79 (assume @p110 (tptp.hBOOL (tptp.hAPP @t5 tptp.bool (tptp.hAPP @t4 @t258 @t257 tptp.f) @t256))) % 0.50/0.79 (assume @p111 (tptp.hBOOL (tptp.hAPP @t6 tptp.bool (tptp.hAPP @t2 @t260 @t259 tptp.lba) tptp.arrow_638930832le_Lin))) % 0.50/0.79 (assume @p112 (tptp.hBOOL (tptp.hAPP @t6 tptp.bool (tptp.hAPP @t2 @t260 @t259 tptp.lab) tptp.arrow_638930832le_Lin))) % 0.50/0.79 (assume @p113 (forall (@list @t99 @t98 @t70) (=> @t261 (=> (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t101 @t70)) (not (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t124 @t70))))))) % 0.50/0.79 (assume @p114 (forall (@list @t72 @t71 @t70) (=> @t261 (=> @t85 (= (not @t78) (tptp.hBOOL (tptp.hAPP @t2 tptp.bool (tptp.hAPP @t1 @t6 @t76 (tptp.hAPP tptp.arrow_1212486748le_alt @t1 (tptp.hAPP tptp.arrow_1212486748le_alt @t74 @t73 @t71) @t72)) @t70))))))) % 0.50/0.79 (assume @p115 (forall (@list @t13 @t15 @t232 @t253) (=> (forall @t187 (= @t249 (tptp.hAPP @t13 @t15 @t253 @t181))) (= (tptp.ti @t18 @t232) (tptp.ti @t18 @t253))))) % 0.50/0.79 (assume @p116 (forall (@list @t13 @t72 @t241) (= @t243 (tptp.hBOOL (tptp.hAPP @t13 tptp.bool @t241 @t72))))) % 0.50/0.79 (assume @p117 (forall (@list @t13 @t97) (= (tptp.hAPP @t35 @t35 @t60 @t97) (tptp.ti @t35 @t97)))) % 0.50/0.79 (assume @p118 (forall @t262 (=> @t261 (tptp.hBOOL (tptp.hAPP @t6 tptp.bool (tptp.hAPP @t2 @t260 @t259 (tptp.hAPP tptp.arrow_1212486748le_alt @t2 @t90 @t72)) tptp.arrow_638930832le_Lin))))) % 0.50/0.79 (assume @p119 (forall @t262 (=> @t261 (tptp.hBOOL (tptp.hAPP @t6 tptp.bool (tptp.hAPP @t2 @t260 @t259 (tptp.hAPP tptp.arrow_1212486748le_alt @t2 @t88 @t72)) tptp.arrow_638930832le_Lin))))) % 0.50/0.79 (assume @p120 (forall (@list @t70 @t72 @t71) (=> @t85 (=> @t261 (tptp.hBOOL (tptp.hAPP @t6 tptp.bool (tptp.hAPP @t2 @t260 @t259 (tptp.hAPP tptp.arrow_1212486748le_alt @t2 (tptp.hAPP tptp.arrow_1212486748le_alt @t8 @t263 @t72) @t71)) tptp.arrow_638930832le_Lin)))))) % 0.50/0.79 (assume @p121 (forall (@list @t70) (=> @t261 (tptp.hBOOL (tptp.hAPP @t7 tptp.bool (tptp.hAPP @t3 @t69 @t68 (tptp.hAPP @t2 @t3 (tptp.combk @t2 tptp.arrow_1384031255e_indi) @t70)) tptp.arrow_1834574746e_Prof))))) % 0.50/0.79 (assume @p122 (forall (@list @t72 @t71 @t70 @t99 @t98) (=> @t118 (=> @t261 (= (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t77 (tptp.hAPP tptp.arrow_1212486748le_alt @t2 (tptp.hAPP tptp.arrow_1212486748le_alt @t8 @t263 @t99) @t98))) (and @t85 (=> @t265 (tptp.hBOOL (tptp.hAPP @t2 tptp.bool (tptp.hAPP @t1 @t6 @t76 (tptp.hAPP tptp.arrow_1212486748le_alt @t1 @t100 @t71)) @t70))) (=> (not @t265) (and (=> @t264 (or (= @t81 @t115) (tptp.hBOOL (tptp.hAPP @t2 tptp.bool (tptp.hAPP @t1 @t6 @t76 (tptp.hAPP tptp.arrow_1212486748le_alt @t1 @t75 @t99)) @t70)))) (=> (not @t264) @t78))))))))) % 0.50/0.79 (assume @p123 (forall (@list @t266 @t179) (=> (tptp.hBOOL (tptp.hAPP @t5 tptp.bool (tptp.hAPP @t4 @t258 @t257 @t179) @t256)) (=> (forall @t187 (=> @t186 (forall @t169 (=> (not (= (tptp.ti tptp.arrow_1212486748le_alt @t168) (tptp.ti tptp.arrow_1212486748le_alt @t167))) (=> (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t180 @t268)) @t183))))) @t267)))) % 0.50/0.79 (assume @p124 (forall @t275 (=> @t274 (=> (not @t271) (not @t243))))) % 0.50/0.79 (assume @p125 (forall (@list @t99 @t98) (=> @t118 (exists @t187 (and (tptp.hBOOL (tptp.hAPP @t6 tptp.bool (tptp.hAPP @t2 @t260 @t259 @t181) tptp.arrow_638930832le_Lin)) (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t101 @t181))))))) % 0.50/0.79 (assume @p126 (forall (@list @t276) (tptp.hBOOL (tptp.hAPP @t7 tptp.bool (tptp.hAPP @t3 @t69 @t68 (tptp.hAPP @t2 @t3 (tptp.hAPP @t157 @t280 @t279 (tptp.hAPP @t2 @t157 (tptp.hAPP @t154 @t278 @t277 (tptp.hAPP @t11 @t154 @t155 (tptp.hAPP tptp.nat @t11 @t161 @t276))) tptp.lab)) tptp.lba)) tptp.arrow_1834574746e_Prof)))) % 0.50/0.79 (assume @p127 (forall @t275 (=> @t274 (=> @t243 @t271)))) % 0.50/0.79 (assume @p128 (= tptp.arrow_1834574746e_Prof (tptp.hAPP @t281 @t7 (tptp.hAPP @t11 (tptp.fun @t281 @t7) (tptp.pi tptp.arrow_1384031255e_indi @t2) @t138) (tptp.hAPP @t6 @t281 (tptp.combk @t6 tptp.arrow_1384031255e_indi) tptp.arrow_638930832le_Lin)))) % 0.50/0.79 (assume @p129 (forall @t275 (=> (tptp.hBOOL (tptp.hAPP @t38 tptp.bool @t273 (tptp.hAPP @t40 @t38 @t272 (tptp.hAPP @t39 @t40 @t282 @t269)))) (=> @t243 (tptp.hBOOL (tptp.hAPP @t39 tptp.bool @t270 @t269)))))) % 0.50/0.79 (assume @p130 (forall @t252 (tptp.hBOOL (tptp.hAPP @t283 tptp.bool (tptp.hAPP @t27 (tptp.fun @t283 tptp.bool) (tptp.member @t27) @t26) (tptp.hAPP @t48 @t283 (tptp.hAPP @t35 (tptp.fun @t48 @t283) (tptp.pi @t13 @t13) @t241) (tptp.hAPP @t35 @t48 (tptp.combk @t35 @t13) @t241)))))) % 0.50/0.79 (assume @p131 (forall (@list @t179 @t266) (= @t267 (forall @t187 (=> @t186 (= @t182 @t268)))))) % 0.50/0.79 (assume @p132 (forall (@list @t13 @t15 @t241) (= (tptp.hAPP @t40 @t38 @t272 (tptp.hAPP @t39 @t40 @t282 (tptp.top_top @t39))) (tptp.top_top @t38)))) % 0.50/0.79 (assume @p133 (= @t172 (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t284 (tptp.hAPP @t3 @t2 tptp.f (tptp.hAPP @t2 @t3 (tptp.hAPP @t157 @t280 @t279 (tptp.hAPP @t2 @t157 (tptp.hAPP @t154 @t278 @t277 @t162) tptp.lab)) tptp.lba)))))) % 0.50/0.79 (assume @p134 (forall @t106 (= (and (=> @t135 (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t171 @t137))) (=> @t136 (and (=> @t130 (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t171 @t132))) (=> @t131 (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t171 @t126)))))) (and (=> @t135 @t286) (=> @t136 @t285))))) % 0.50/0.79 (assume @p135 (not (= tptp.a tptp.b))) % 0.50/0.79 (assume @p136 @t285) % 0.50/0.79 (assume @p137 (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t287 tptp.lab))) % 0.50/0.79 (assume @p138 (not (tptp.hBOOL (tptp.hAPP @t2 tptp.bool @t287 tptp.lba)))) % 0.50/0.79 (assume @p139 (not @t286)) % 0.50/0.79 (assume @p140 (forall @t291 (=> (tptp.preorder @t288) (tptp.preorder @t290)))) % 0.50/0.79 (assume @p141 (forall @t291 (=> (tptp.order @t288) (tptp.order @t290)))) % 0.50/0.79 (assume @p142 (forall @t291 (=> (tptp.top @t288) (tptp.top @t290)))) % 0.50/0.79 (assume @p143 (forall @t291 (=> (tptp.ord @t288) (tptp.ord @t290)))) % 0.50/0.79 (assume @p144 (tptp.preorder tptp.nat)) % 0.50/0.79 (assume @p145 (tptp.linorder tptp.nat)) % 0.50/0.79 (assume @p146 (tptp.order tptp.nat)) % 0.50/0.79 (assume @p147 (tptp.ord tptp.nat)) % 0.50/0.79 (assume @p148 (tptp.preorder tptp.bool)) % 0.50/0.79 (assume @p149 (tptp.order tptp.bool)) % 0.50/0.79 (assume @p150 (tptp.top tptp.bool)) % 0.50/0.79 (assume @p151 (tptp.ord tptp.bool)) % 0.50/0.79 (assume @p152 (forall (@list @t293 @t292) (= (tptp.ti @t293 @t294) @t294))) % 0.50/0.79 (assume @p153 (forall @t295 (= (tptp.hAPP @t13 @t13 (tptp.hAPP @t13 @t27 (tptp.hAPP tptp.bool @t46 @t45 tptp.fTrue) @t193) @t194) @t198))) % 0.50/0.79 (assume @p154 (forall @t295 (= (tptp.hAPP @t13 @t13 (tptp.hAPP @t13 @t27 (tptp.hAPP tptp.bool @t46 @t45 tptp.fFalse) @t193) @t194) @t197))) % 0.50/0.79 (assume @p155 (forall (@list @t296) (or (= @t297 tptp.fTrue) (= @t297 tptp.fFalse)))) % 0.50/0.79 (assume @p156 (forall @t301 (= (tptp.hAPP @t13 @t14 (tptp.hAPP @t18 @t17 (tptp.hAPP @t20 @t19 @t16 @t296) @t299) @t298) (tptp.hAPP @t15 @t14 @t296 @t300)))) % 0.50/0.79 (assume @p157 (forall @t301 (= (tptp.hAPP @t13 @t14 (tptp.hAPP @t15 @t17 (tptp.hAPP @t24 @t23 @t22 @t296) @t299) @t298) (tptp.hAPP @t15 @t14 @t302 @t299)))) % 0.50/0.79 (assume @p158 (forall (@list @t13 @t296) (= (tptp.hAPP @t13 @t13 @t26 @t296) @t303))) % 0.50/0.79 (assume @p159 (forall (@list @t15 @t13 @t296 @t299) (= (tptp.hAPP @t15 @t13 (tptp.hAPP @t13 @t30 @t29 @t296) @t299) @t303))) % 0.50/0.79 (assume @p160 (forall @t301 (= (tptp.hAPP @t13 @t14 (tptp.hAPP @t18 @t17 (tptp.hAPP @t24 @t19 @t32 @t296) @t299) @t298) (tptp.hAPP @t15 @t14 @t302 @t300)))) % 0.50/0.79 (assume @p161 (tptp.hBOOL tptp.fTrue)) % 0.50/0.79 (assume @p162 (forall @t295 (or (not @t304) @t199))) % 0.50/0.79 (assume @p163 (forall @t295 (or @t200 @t304))) % 0.50/0.79 (assume @p164 (not @t166)) % 0.50/0.79 (assume @p165 true) % 0.50/0.79 (step @p166 :rule symm :premises (@p58)) % 0.50/0.79 (step @p167 :rule equiv_elim1 :premises (@p166)) % 0.50/0.79 (step @p168 :rule reordering :premises (@p167) :args ((or @t166 (not @t165)))) % 0.50/0.79 (step @p169 :rule chain_m_resolution :premises (@p168 @p57) :args (@t166 @t305 (@list @t165))) % 0.50/0.79 (step @p170 false :rule chain_m_resolution :premises (@p164 @p169) :args (false @t305 (@list @t166))) % 0.50/0.79 ) % 0.50/0.79 % SZS output end Proof % 0.50/0.79 % cvc5 exiting %------------------------------------------------------------------------------