%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP074^1 : TPTP v9.2.1. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n011.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 08:24:58 AM UTC 2026 % Result : Theorem 0.41s 0.80s % Output : Proof 0.41s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP074^1 : TPTP v9.2.1. Released v7.5.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 : n011.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 04:13:05 EDT 2026 % 0.17/0.34 % CPUTime : % 0.37/0.58 %----Proving TH0 % 0.41/0.80 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 90s... % 0.41/0.80 % SZS status Theorem % 0.41/0.80 % SZS output start Proof % 0.41/0.80 ( % 0.41/0.80 (declare-sort tptp.set_HF_Mirabelle_hf 0) % 0.41/0.80 (declare-sort tptp.hF_Mirabelle_hf 0) % 0.41/0.80 (declare-sort tptp.nat 0) % 0.41/0.80 (declare-const tptp.zero_z189798548lle_hf tptp.hF_Mirabelle_hf) % 0.41/0.80 (declare-const tptp.hF_Mirabelle_hinsert (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf)) % 0.41/0.80 (declare-const tptp.hF_Mirabelle_hfset (-> tptp.hF_Mirabelle_hf tptp.set_HF_Mirabelle_hf)) % 0.41/0.80 (declare-const tptp.member1367349282lle_hf (-> tptp.hF_Mirabelle_hf tptp.set_HF_Mirabelle_hf Bool)) % 0.41/0.80 (declare-const tptp.inf_in956532509lle_hf (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf)) % 0.41/0.80 (declare-const tptp.inf_inf_nat (-> tptp.nat tptp.nat tptp.nat)) % 0.41/0.80 (declare-const tptp.y tptp.hF_Mirabelle_hf) % 0.41/0.80 (declare-const tptp.hF_Mir1248913145eplace (-> tptp.hF_Mirabelle_hf (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf Bool) tptp.hF_Mirabelle_hf)) % 0.41/0.80 (declare-const tptp.hF_Mirabelle_HF (-> tptp.set_HF_Mirabelle_hf tptp.hF_Mirabelle_hf)) % 0.41/0.80 (declare-const tptp.collec2046588256lle_hf (-> (-> tptp.hF_Mirabelle_hf Bool) tptp.set_HF_Mirabelle_hf)) % 0.41/0.80 (declare-const tptp.sup_sup_nat (-> tptp.nat tptp.nat tptp.nat)) % 0.41/0.80 (declare-const tptp.minus_minus_nat (-> tptp.nat tptp.nat tptp.nat)) % 0.41/0.80 (declare-const tptp.minus_1232880740lle_hf (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf)) % 0.41/0.80 (declare-const tptp.hF_Mirabelle_hfst (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf)) % 0.41/0.80 (declare-const tptp.hF_Mirabelle_hsnd (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf)) % 0.41/0.80 (declare-const tptp.hF_Mirabelle_HInter (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf)) % 0.41/0.80 (declare-const tptp.hF_Mir818139703ollect (-> (-> tptp.hF_Mirabelle_hf Bool) tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf)) % 0.41/0.80 (declare-const tptp.hF_Mirabelle_Abs_hf (-> tptp.nat tptp.hF_Mirabelle_hf)) % 0.41/0.80 (declare-const tptp.hF_Mirabelle_Replace (-> tptp.hF_Mirabelle_hf (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf Bool) tptp.hF_Mirabelle_hf)) % 0.41/0.80 (declare-const tptp.x tptp.hF_Mirabelle_hf) % 0.41/0.80 (declare-const tptp.hF_Mirabelle_HUnion (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf)) % 0.41/0.80 (declare-const tptp.semiri1382578993at_nat (-> tptp.nat tptp.nat)) % 0.41/0.80 (declare-const tptp.zero_zero_nat tptp.nat) % 0.41/0.80 (declare-const tptp.hF_Mirabelle_RepFun (-> tptp.hF_Mirabelle_hf (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf) tptp.hF_Mirabelle_hf)) % 0.41/0.80 (declare-const tptp.sup_su638957495lle_hf (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define tptp.hF_Mirabelle_hpair () (let ((_let_1 (@var "B3" tptp.hF_Mirabelle_hf))) (let ((_let_2 (@var "A3" tptp.hF_Mirabelle_hf))) (let ((_let_3 (_ tptp.hF_Mirabelle_hinsert _let_2))) (lambda (@list _let_2 _let_1) (_ (_ tptp.hF_Mirabelle_hinsert (_ _let_3 tptp.zero_z189798548lle_hf)) (_ (_ tptp.hF_Mirabelle_hinsert (_ _let_3 (_ (_ tptp.hF_Mirabelle_hinsert _let_1) tptp.zero_z189798548lle_hf))) tptp.zero_z189798548lle_hf))))))) % 0.41/0.80 (define tptp.hF_Mirabelle_hmem () (let ((_let_1 (@var "B3" tptp.hF_Mirabelle_hf))) (let ((_let_2 (@var "A3" tptp.hF_Mirabelle_hf))) (lambda (@list _let_2 _let_1) (_ (_ tptp.member1367349282lle_hf _let_2) (_ tptp.hF_Mirabelle_hfset _let_1)))))) % 0.41/0.80 (define tptp.ord_le976219883lle_hf () (let ((_let_1 (@var "B3" tptp.hF_Mirabelle_hf))) (let ((_let_2 (@var "A3" tptp.hF_Mirabelle_hf))) (lambda (@list _let_1 _let_2) (= (_ (_ tptp.inf_in956532509lle_hf _let_2) _let_1) _let_1))))) % 0.41/0.80 (define tptp.ord_less_eq_nat () (let ((_let_1 (@var "B3" tptp.nat))) (let ((_let_2 (@var "A3" tptp.nat))) (lambda (@list _let_1 _let_2) (= (_ (_ tptp.inf_inf_nat _let_2) _let_1) _let_1))))) % 0.41/0.80 (define @t1 () (@var "B2" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t2 () (@var "B" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t3 () (= @t2 @t1)) % 0.41/0.80 (define @t4 () (@var "A2" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t5 () (@var "A" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t6 () (= @t5 @t4)) % 0.41/0.80 (define @t7 () (_ (_ tptp.hF_Mirabelle_hpair @t5) @t2)) % 0.41/0.80 (define @t8 () (= @t7 (_ (_ tptp.hF_Mirabelle_hpair @t4) @t1))) % 0.41/0.80 (define @t9 () (@list @t5 @t2 @t4 @t1)) % 0.41/0.80 (define @t10 () (@list @t5 @t2)) % 0.41/0.80 (define @t11 () (@var "P" (-> tptp.hF_Mirabelle_hf Bool))) % 0.41/0.80 (define @t12 () (_ tptp.hF_Mir818139703ollect @t11)) % 0.41/0.80 (define @t13 () (@var "R" (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf Bool))) % 0.41/0.80 (define @t14 () (@var "X" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t15 () (@list @t14)) % 0.41/0.80 (define @t16 () (@var "X" tptp.nat)) % 0.41/0.80 (define @t17 () (@list @t16)) % 0.41/0.80 (define @t18 () (@var "F" (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf))) % 0.41/0.80 (define @t19 () (@var "B3" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t20 () (_ (_ tptp.hF_Mirabelle_hinsert @t19) tptp.zero_z189798548lle_hf)) % 0.41/0.80 (define @t21 () (@var "A3" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t22 () (_ tptp.hF_Mirabelle_hinsert @t21)) % 0.41/0.80 (define @t23 () (_ (_ tptp.hF_Mirabelle_hinsert (_ @t22 @t20)) tptp.zero_z189798548lle_hf)) % 0.41/0.80 (define @t24 () (_ @t22 tptp.zero_z189798548lle_hf)) % 0.41/0.80 (define @t25 () (@list @t21 @t19)) % 0.41/0.80 (define @t26 () (= @t5 @t2)) % 0.41/0.80 (define @t27 () (_ tptp.hF_Mirabelle_hinsert @t2)) % 0.41/0.80 (define @t28 () (_ @t27 tptp.zero_z189798548lle_hf)) % 0.41/0.80 (define @t29 () (_ tptp.hF_Mirabelle_hinsert @t5)) % 0.41/0.80 (define @t30 () (_ @t29 tptp.zero_z189798548lle_hf)) % 0.41/0.80 (define @t31 () (@var "Z" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t32 () (_ tptp.hF_Mirabelle_hinsert @t14)) % 0.41/0.80 (define @t33 () (@var "Y" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t34 () (_ tptp.hF_Mirabelle_hinsert @t33)) % 0.41/0.80 (define @t35 () (@list @t14 @t33 @t31)) % 0.41/0.80 (define @t36 () (@var "A4" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t37 () (_ @t29 @t36)) % 0.41/0.80 (define @t38 () (not (= @t37 tptp.zero_z189798548lle_hf))) % 0.41/0.80 (define @t39 () (@list @t5 @t36)) % 0.41/0.80 (define @t40 () (forall @t39 @t38)) % 0.41/0.80 (define @t41 () (@var "C" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t42 () (@var "D" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t43 () (_ @t11 @t14)) % 0.41/0.80 (define @t44 () (@var "X2" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t45 () (@var "Y2" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t46 () (_ @t11 @t45)) % 0.41/0.80 (define @t47 () (_ @t11 @t44)) % 0.41/0.80 (define @t48 () (@list @t44)) % 0.41/0.80 (define @t49 () (_ @t11 tptp.zero_z189798548lle_hf)) % 0.41/0.80 (define @t50 () (_ tptp.hF_Mirabelle_HInter @t36)) % 0.41/0.80 (define @t51 () (_ tptp.inf_in956532509lle_hf @t5)) % 0.41/0.80 (define @t52 () (not (= @t36 tptp.zero_z189798548lle_hf))) % 0.41/0.80 (define @t53 () (_ tptp.hF_Mirabelle_Abs_hf tptp.zero_zero_nat)) % 0.41/0.80 (define @t54 () (@var "Y3" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t55 () (_ tptp.hF_Mirabelle_hmem @t14)) % 0.41/0.80 (define @t56 () (_ @t55 @t54)) % 0.41/0.80 (define @t57 () (_ tptp.hF_Mirabelle_hmem @t54)) % 0.41/0.80 (define @t58 () (_ @t57 @t36)) % 0.41/0.80 (define @t59 () (@list @t54)) % 0.41/0.80 (define @t60 () (_ tptp.hF_Mirabelle_HUnion @t36)) % 0.41/0.80 (define @t61 () (_ tptp.sup_su638957495lle_hf @t5)) % 0.41/0.80 (define @t62 () (@var "B4" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t63 () (_ tptp.minus_1232880740lle_hf @t36)) % 0.41/0.80 (define @t64 () (_ @t63 @t62)) % 0.41/0.80 (define @t65 () (_ tptp.sup_su638957495lle_hf @t19)) % 0.41/0.80 (define @t66 () (_ tptp.hF_Mirabelle_hmem @t44)) % 0.41/0.80 (define @t67 () (@list @t44 @t45)) % 0.41/0.80 (define @t68 () (@var "B5" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t69 () (@var "A5" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t70 () (_ tptp.hF_Mirabelle_Replace @t62)) % 0.41/0.80 (define @t71 () (_ tptp.hF_Mirabelle_Replace @t36)) % 0.41/0.80 (define @t72 () (_ @t71 @t13)) % 0.41/0.80 (define @t73 () (_ tptp.sup_su638957495lle_hf @t36)) % 0.41/0.80 (define @t74 () (_ @t73 @t62)) % 0.41/0.80 (define @t75 () (@var "A" tptp.nat)) % 0.41/0.80 (define @t76 () (_ tptp.minus_minus_nat tptp.zero_zero_nat)) % 0.41/0.80 (define @t77 () (@list @t75)) % 0.41/0.80 (define @t78 () (_ tptp.minus_minus_nat @t75)) % 0.41/0.80 (define @t79 () (_ tptp.hF_Mirabelle_hmem @t5)) % 0.41/0.80 (define @t80 () (@list @t5 @t2 @t41)) % 0.41/0.80 (define @t81 () (_ @t61 @t2)) % 0.41/0.80 (define @t82 () (@list @t14 @t5 @t2)) % 0.41/0.80 (define @t83 () (@var "U" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t84 () (_ tptp.hF_Mirabelle_hmem @t83)) % 0.41/0.80 (define @t85 () (_ @t84 @t33)) % 0.41/0.80 (define @t86 () (_ @t84 @t14)) % 0.41/0.80 (define @t87 () (_ tptp.inf_in956532509lle_hf @t14)) % 0.41/0.80 (define @t88 () (_ @t87 @t33)) % 0.41/0.80 (define @t89 () (@list @t83 @t14 @t33)) % 0.41/0.80 (define @t90 () (@var "U2" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t91 () (_ @t18 @t90)) % 0.41/0.80 (define @t92 () (@var "V" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t93 () (_ tptp.hF_Mirabelle_hmem @t90)) % 0.41/0.80 (define @t94 () (_ @t93 @t36)) % 0.41/0.80 (define @t95 () (@list @t90)) % 0.41/0.80 (define @t96 () (_ (_ tptp.hF_Mirabelle_RepFun @t36) @t18)) % 0.41/0.80 (define @t97 () (_ tptp.hF_Mirabelle_hmem @t92)) % 0.41/0.80 (define @t98 () (@list @t36)) % 0.41/0.80 (define @t99 () (_ tptp.collec2046588256lle_hf @t11)) % 0.41/0.80 (define @t100 () (@var "A4" tptp.set_HF_Mirabelle_hf)) % 0.41/0.80 (define @t101 () (@var "X3" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t102 () (@list @t101)) % 0.41/0.80 (define @t103 () (@var "Q" (-> tptp.hF_Mirabelle_hf Bool))) % 0.41/0.80 (define @t104 () (_ tptp.minus_1232880740lle_hf @t14)) % 0.41/0.80 (define @t105 () (_ tptp.inf_in956532509lle_hf @t36)) % 0.41/0.80 (define @t106 () (_ @t13 @t90)) % 0.41/0.80 (define @t107 () (_ @t106 @t92)) % 0.41/0.80 (define @t108 () (_ tptp.hF_Mirabelle_RepFun @t62)) % 0.41/0.80 (define @t109 () (@list @t36 @t62)) % 0.41/0.80 (define @t110 () (@var "C" tptp.nat)) % 0.41/0.80 (define @t111 () (@var "B" tptp.nat)) % 0.41/0.80 (define @t112 () (@list @t75 @t110 @t111)) % 0.41/0.80 (define @t113 () (@var "V2" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t114 () (_ @t93 @t14)) % 0.41/0.80 (define @t115 () (@var "Z2" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t116 () (_ (_ tptp.hF_Mirabelle_hmem @t113) @t115)) % 0.41/0.80 (define @t117 () (@list @t113)) % 0.41/0.80 (define @t118 () (@list @t115)) % 0.41/0.80 (define @t119 () (@var "U3" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t120 () (_ tptp.hF_Mirabelle_hmem @t119)) % 0.41/0.80 (define @t121 () (_ @t120 @t14)) % 0.41/0.80 (define @t122 () (_ @t120 @t115)) % 0.41/0.80 (define @t123 () (@list @t119)) % 0.41/0.80 (define @t124 () (_ @t55 @t33)) % 0.41/0.80 (define @t125 () (@list @t14 @t33)) % 0.41/0.80 (define @t126 () (@var "V3" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t127 () (@var "V4" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t128 () (@var "U4" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t129 () (_ @t13 @t128)) % 0.41/0.80 (define @t130 () (=> (_ @t129 @t126) (=> (_ @t129 @t127) (= @t127 @t126)))) % 0.41/0.80 (define @t131 () (_ tptp.hF_Mirabelle_hmem @t128)) % 0.41/0.80 (define @t132 () (@list @t128 @t126 @t127)) % 0.41/0.80 (define @t133 () (_ tptp.hF_Mirabelle_hmem @t101)) % 0.41/0.80 (define @t134 () (@var "Z3" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t135 () (@var "Y4" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t136 () (lambda (@list @t135 @t134) (= @t135 @t134))) % 0.41/0.80 (define @t137 () (_ tptp.inf_in956532509lle_hf @t62)) % 0.41/0.80 (define @t138 () (_ @t137 @t36)) % 0.41/0.80 (define @t139 () (_ @t32 @t36)) % 0.41/0.80 (define @t140 () (_ @t137 @t139)) % 0.41/0.80 (define @t141 () (_ @t55 @t62)) % 0.41/0.80 (define @t142 () (not @t141)) % 0.41/0.80 (define @t143 () (@list @t14 @t62 @t36)) % 0.41/0.80 (define @t144 () (_ @t105 @t62)) % 0.41/0.80 (define @t145 () (_ (_ tptp.inf_in956532509lle_hf @t139) @t62)) % 0.41/0.80 (define @t146 () (@var "W" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t147 () (= @t31 tptp.zero_z189798548lle_hf)) % 0.41/0.80 (define @t148 () (@list @t31)) % 0.41/0.80 (define @t149 () (_ (_ tptp.minus_1232880740lle_hf @t139) @t62)) % 0.41/0.80 (define @t150 () (@list @t5)) % 0.41/0.80 (define @t151 () (_ tptp.sup_su638957495lle_hf @t62)) % 0.41/0.80 (define @t152 () (@var "G" (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf))) % 0.41/0.80 (define @t153 () (_ @t66 @t62)) % 0.41/0.80 (define @t154 () (= @t36 @t62)) % 0.41/0.80 (define @t155 () (@var "Q" (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf Bool))) % 0.41/0.80 (define @t156 () (@var "P" (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf Bool))) % 0.41/0.80 (define @t157 () (@var "Y" tptp.nat)) % 0.41/0.80 (define @t158 () (_ tptp.inf_inf_nat @t16)) % 0.41/0.80 (define @t159 () (_ @t158 @t157)) % 0.41/0.80 (define @t160 () (_ tptp.sup_sup_nat @t16)) % 0.41/0.80 (define @t161 () (@list @t16 @t157)) % 0.41/0.80 (define @t162 () (_ tptp.sup_su638957495lle_hf @t14)) % 0.41/0.80 (define @t163 () (_ @t160 @t157)) % 0.41/0.80 (define @t164 () (_ @t162 @t33)) % 0.41/0.80 (define @t165 () (_ tptp.sup_sup_nat @t75)) % 0.41/0.80 (define @t166 () (_ @t165 @t111)) % 0.41/0.80 (define @t167 () (_ tptp.sup_sup_nat @t166)) % 0.41/0.80 (define @t168 () (@list @t75 @t111)) % 0.41/0.80 (define @t169 () (_ tptp.sup_su638957495lle_hf @t81)) % 0.41/0.80 (define @t170 () (_ tptp.inf_inf_nat @t159)) % 0.41/0.80 (define @t171 () (_ tptp.inf_in956532509lle_hf @t88)) % 0.41/0.80 (define @t172 () (_ tptp.inf_inf_nat @t75)) % 0.41/0.80 (define @t173 () (_ @t172 @t111)) % 0.41/0.80 (define @t174 () (_ @t51 @t2)) % 0.41/0.80 (define @t175 () (_ tptp.inf_inf_nat @t173)) % 0.41/0.80 (define @t176 () (_ tptp.inf_in956532509lle_hf @t174)) % 0.41/0.80 (define @t177 () (@var "Z" tptp.nat)) % 0.41/0.80 (define @t178 () (_ @t158 @t177)) % 0.41/0.80 (define @t179 () (_ tptp.inf_inf_nat @t157)) % 0.41/0.80 (define @t180 () (_ @t179 @t177)) % 0.41/0.80 (define @t181 () (_ @t158 @t180)) % 0.41/0.80 (define @t182 () (@list @t16 @t157 @t177)) % 0.41/0.80 (define @t183 () (_ @t87 @t31)) % 0.41/0.80 (define @t184 () (_ tptp.inf_in956532509lle_hf @t33)) % 0.41/0.80 (define @t185 () (_ @t184 @t31)) % 0.41/0.80 (define @t186 () (_ @t87 @t185)) % 0.41/0.80 (define @t187 () (@var "X3" tptp.nat)) % 0.41/0.80 (define @t188 () (@var "Y3" tptp.nat)) % 0.41/0.80 (define @t189 () (@list @t187 @t188)) % 0.41/0.80 (define @t190 () (@list @t101 @t54)) % 0.41/0.80 (define @t191 () (@var "K" tptp.nat)) % 0.41/0.80 (define @t192 () (_ tptp.inf_inf_nat @t191)) % 0.41/0.80 (define @t193 () (_ @t192 @t173)) % 0.41/0.80 (define @t194 () (@var "A4" tptp.nat)) % 0.41/0.80 (define @t195 () (@list @t194 @t191 @t75 @t111)) % 0.41/0.80 (define @t196 () (@var "K" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t197 () (_ tptp.inf_in956532509lle_hf @t196)) % 0.41/0.80 (define @t198 () (_ @t197 @t174)) % 0.41/0.80 (define @t199 () (@list @t36 @t196 @t5 @t2)) % 0.41/0.80 (define @t200 () (@var "B4" tptp.nat)) % 0.41/0.80 (define @t201 () (@list @t200 @t191 @t111 @t75)) % 0.41/0.80 (define @t202 () (@list @t62 @t196 @t2 @t5)) % 0.41/0.80 (define @t203 () (_ tptp.inf_inf_nat @t111)) % 0.41/0.80 (define @t204 () (_ @t203 @t110)) % 0.41/0.80 (define @t205 () (_ @t172 @t204)) % 0.41/0.80 (define @t206 () (@list @t75 @t111 @t110)) % 0.41/0.80 (define @t207 () (_ tptp.inf_in956532509lle_hf @t2)) % 0.41/0.80 (define @t208 () (_ @t207 @t41)) % 0.41/0.80 (define @t209 () (_ @t51 @t208)) % 0.41/0.80 (define @t210 () (@var "A3" tptp.nat)) % 0.41/0.80 (define @t211 () (@var "B3" tptp.nat)) % 0.41/0.80 (define @t212 () (@list @t210 @t211)) % 0.41/0.80 (define @t213 () (@list @t111 @t75 @t110)) % 0.41/0.80 (define @t214 () (@list @t2 @t5 @t41)) % 0.41/0.80 (define @t215 () (_ @t160 @t177)) % 0.41/0.80 (define @t216 () (_ tptp.sup_sup_nat @t157)) % 0.41/0.80 (define @t217 () (_ @t216 @t177)) % 0.41/0.80 (define @t218 () (_ @t160 @t217)) % 0.41/0.80 (define @t219 () (_ @t162 @t31)) % 0.41/0.80 (define @t220 () (_ tptp.sup_su638957495lle_hf @t33)) % 0.41/0.80 (define @t221 () (_ @t220 @t31)) % 0.41/0.80 (define @t222 () (_ @t162 @t221)) % 0.41/0.80 (define @t223 () (_ tptp.sup_sup_nat @t191)) % 0.41/0.80 (define @t224 () (_ @t223 @t166)) % 0.41/0.80 (define @t225 () (_ tptp.sup_su638957495lle_hf @t196)) % 0.41/0.80 (define @t226 () (_ @t225 @t81)) % 0.41/0.80 (define @t227 () (_ tptp.sup_sup_nat @t111)) % 0.41/0.80 (define @t228 () (_ @t227 @t110)) % 0.41/0.80 (define @t229 () (_ @t165 @t228)) % 0.41/0.80 (define @t230 () (_ tptp.sup_su638957495lle_hf @t2)) % 0.41/0.80 (define @t231 () (_ @t230 @t41)) % 0.41/0.80 (define @t232 () (_ @t61 @t231)) % 0.41/0.80 (define @t233 () (_ (_ tptp.inf_inf_nat @t163) @t215)) % 0.41/0.80 (define @t234 () (_ @t160 @t180)) % 0.41/0.80 (define @t235 () (= @t234 @t233)) % 0.41/0.80 (define @t236 () (@var "Z2" tptp.nat)) % 0.41/0.80 (define @t237 () (@var "X2" tptp.nat)) % 0.41/0.80 (define @t238 () (_ tptp.inf_inf_nat @t237)) % 0.41/0.80 (define @t239 () (@var "Y2" tptp.nat)) % 0.41/0.80 (define @t240 () (@list @t237 @t239 @t236)) % 0.41/0.80 (define @t241 () (_ (_ tptp.inf_in956532509lle_hf @t164) @t219)) % 0.41/0.80 (define @t242 () (_ @t162 @t185)) % 0.41/0.80 (define @t243 () (= @t242 @t241)) % 0.41/0.80 (define @t244 () (_ tptp.inf_in956532509lle_hf @t44)) % 0.41/0.80 (define @t245 () (@list @t44 @t45 @t115)) % 0.41/0.80 (define @t246 () (_ (_ tptp.sup_sup_nat @t159) @t178)) % 0.41/0.80 (define @t247 () (_ @t158 @t217)) % 0.41/0.80 (define @t248 () (= @t247 @t246)) % 0.41/0.80 (define @t249 () (_ tptp.sup_sup_nat @t237)) % 0.41/0.80 (define @t250 () (_ (_ tptp.sup_su638957495lle_hf @t88) @t183)) % 0.41/0.80 (define @t251 () (_ @t87 @t221)) % 0.41/0.80 (define @t252 () (= @t251 @t250)) % 0.41/0.80 (define @t253 () (_ tptp.sup_su638957495lle_hf @t44)) % 0.41/0.80 (define @t254 () (@list @t157 @t177 @t16)) % 0.41/0.80 (define @t255 () (@list @t33 @t31 @t14)) % 0.41/0.80 (define @t256 () (@var "M" tptp.nat)) % 0.41/0.80 (define @t257 () (_ tptp.minus_minus_nat @t256)) % 0.41/0.80 (define @t258 () (@list @t256)) % 0.41/0.80 (define @t259 () (@var "N" tptp.nat)) % 0.41/0.80 (define @t260 () (@list @t259)) % 0.41/0.80 (define @t261 () (= @t256 @t259)) % 0.41/0.80 (define @t262 () (_ tptp.minus_minus_nat @t259)) % 0.41/0.80 (define @t263 () (_ @t257 @t259)) % 0.41/0.80 (define @t264 () (= @t263 tptp.zero_zero_nat)) % 0.41/0.80 (define @t265 () (@list @t256 @t259)) % 0.41/0.80 (define @t266 () (@var "J" tptp.nat)) % 0.41/0.80 (define @t267 () (@var "I" tptp.nat)) % 0.41/0.80 (define @t268 () (_ tptp.minus_minus_nat @t267)) % 0.41/0.80 (define @t269 () (@list @t267 @t266 @t191)) % 0.41/0.80 (define @t270 () (_ tptp.ord_le976219883lle_hf @t33)) % 0.41/0.80 (define @t271 () (_ @t270 @t31)) % 0.41/0.80 (define @t272 () (_ @t32 @t33)) % 0.41/0.80 (define @t273 () (_ (_ tptp.ord_less_eq_nat @t256) @t259)) % 0.41/0.80 (define @t274 () (_ tptp.ord_less_eq_nat @t259)) % 0.41/0.80 (define @t275 () (_ tptp.ord_le976219883lle_hf @t5)) % 0.41/0.80 (define @t276 () (_ @t275 @t41)) % 0.41/0.80 (define @t277 () (_ @t275 @t2)) % 0.41/0.80 (define @t278 () (_ @t275 @t208)) % 0.41/0.80 (define @t279 () (_ tptp.ord_less_eq_nat @t75)) % 0.41/0.80 (define @t280 () (_ @t279 @t110)) % 0.41/0.80 (define @t281 () (_ @t279 @t111)) % 0.41/0.80 (define @t282 () (_ @t279 @t204)) % 0.41/0.80 (define @t283 () (_ tptp.ord_le976219883lle_hf @t14)) % 0.41/0.80 (define @t284 () (_ @t283 @t31)) % 0.41/0.80 (define @t285 () (_ @t283 @t33)) % 0.41/0.80 (define @t286 () (_ @t283 @t185)) % 0.41/0.80 (define @t287 () (_ tptp.ord_less_eq_nat @t16)) % 0.41/0.80 (define @t288 () (_ @t287 @t177)) % 0.41/0.80 (define @t289 () (_ @t287 @t157)) % 0.41/0.80 (define @t290 () (_ @t287 @t180)) % 0.41/0.80 (define @t291 () (_ tptp.ord_le976219883lle_hf @t41)) % 0.41/0.80 (define @t292 () (_ @t291 @t5)) % 0.41/0.80 (define @t293 () (_ tptp.ord_le976219883lle_hf @t2)) % 0.41/0.80 (define @t294 () (_ @t293 @t5)) % 0.41/0.80 (define @t295 () (_ (_ tptp.ord_le976219883lle_hf @t231) @t5)) % 0.41/0.80 (define @t296 () (@list @t2 @t41 @t5)) % 0.41/0.80 (define @t297 () (_ tptp.ord_less_eq_nat @t110)) % 0.41/0.80 (define @t298 () (_ @t297 @t75)) % 0.41/0.80 (define @t299 () (_ tptp.ord_less_eq_nat @t111)) % 0.41/0.80 (define @t300 () (_ @t299 @t75)) % 0.41/0.80 (define @t301 () (_ (_ tptp.ord_less_eq_nat @t228) @t75)) % 0.41/0.80 (define @t302 () (@list @t111 @t110 @t75)) % 0.41/0.80 (define @t303 () (_ tptp.ord_less_eq_nat @t157)) % 0.41/0.80 (define @t304 () (_ tptp.ord_less_eq_nat tptp.zero_zero_nat)) % 0.41/0.80 (define @t305 () (_ tptp.ord_less_eq_nat @t267)) % 0.41/0.80 (define @t306 () (_ (_ tptp.ord_le976219883lle_hf @t36) @t62)) % 0.41/0.80 (define @t307 () (@var "L" tptp.nat)) % 0.41/0.80 (define @t308 () (_ tptp.minus_minus_nat @t307)) % 0.41/0.80 (define @t309 () (@list @t256 @t259 @t307)) % 0.41/0.80 (define @t310 () (_ tptp.minus_minus_nat @t110)) % 0.41/0.80 (define @t311 () (_ @t299 @t110)) % 0.41/0.80 (define @t312 () (_ @t262 @t191)) % 0.41/0.80 (define @t313 () (_ @t257 @t191)) % 0.41/0.80 (define @t314 () (_ tptp.ord_less_eq_nat @t191)) % 0.41/0.80 (define @t315 () (_ @t314 @t259)) % 0.41/0.80 (define @t316 () (_ @t314 @t256)) % 0.41/0.80 (define @t317 () (@list @t191 @t256 @t259)) % 0.41/0.80 (define @t318 () (= @t75 tptp.zero_zero_nat)) % 0.41/0.80 (define @t319 () (_ @t279 tptp.zero_zero_nat)) % 0.41/0.80 (define @t320 () (@var "Y5" tptp.nat)) % 0.41/0.80 (define @t321 () (@var "P" (-> tptp.nat Bool))) % 0.41/0.80 (define @t322 () (_ tptp.ord_less_eq_nat @t239)) % 0.41/0.80 (define @t323 () (_ @t274 @t256)) % 0.41/0.80 (define @t324 () (_ @t305 @t266)) % 0.41/0.80 (define @t325 () (_ tptp.ord_le976219883lle_hf @t174)) % 0.41/0.80 (define @t326 () (_ @t325 @t41)) % 0.41/0.80 (define @t327 () (_ tptp.ord_less_eq_nat @t173)) % 0.41/0.80 (define @t328 () (_ @t327 @t110)) % 0.41/0.80 (define @t329 () (_ (_ tptp.inf_in956532509lle_hf @t21) @t19)) % 0.41/0.80 (define @t330 () (_ (_ tptp.inf_inf_nat @t210) @t211)) % 0.41/0.80 (define @t331 () (_ @t270 @t14)) % 0.41/0.80 (define @t332 () (@list @t33 @t14)) % 0.41/0.80 (define @t333 () (_ @t303 @t16)) % 0.41/0.80 (define @t334 () (@list @t157 @t16)) % 0.41/0.80 (define @t335 () (@list @t2 @t5)) % 0.41/0.80 (define @t336 () (@list @t111 @t75)) % 0.41/0.80 (define @t337 () (@var "F" (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf))) % 0.41/0.80 (define @t338 () (_ (_ @t337 @t14) @t33)) % 0.41/0.80 (define @t339 () (_ (_ @t337 @t45) @t115)) % 0.41/0.80 (define @t340 () (_ tptp.ord_le976219883lle_hf @t44)) % 0.41/0.80 (define @t341 () (_ (_ @t337 @t44) @t45)) % 0.41/0.80 (define @t342 () (_ tptp.ord_le976219883lle_hf @t341)) % 0.41/0.80 (define @t343 () (@list @t337 @t14 @t33)) % 0.41/0.80 (define @t344 () (@var "F" (-> tptp.nat tptp.nat tptp.nat))) % 0.41/0.80 (define @t345 () (_ (_ @t344 @t16) @t157)) % 0.41/0.80 (define @t346 () (_ (_ @t344 @t239) @t236)) % 0.41/0.80 (define @t347 () (_ tptp.ord_less_eq_nat @t237)) % 0.41/0.80 (define @t348 () (_ (_ @t344 @t237) @t239)) % 0.41/0.80 (define @t349 () (_ tptp.ord_less_eq_nat @t348)) % 0.41/0.80 (define @t350 () (@list @t237 @t239)) % 0.41/0.80 (define @t351 () (@list @t344 @t16 @t157)) % 0.41/0.80 (define @t352 () (= @t5 @t174)) % 0.41/0.80 (define @t353 () (= @t75 @t173)) % 0.41/0.80 (define @t354 () (_ @t325 @t14)) % 0.41/0.80 (define @t355 () (_ @t293 @t14)) % 0.41/0.80 (define @t356 () (_ @t327 @t16)) % 0.41/0.80 (define @t357 () (_ @t299 @t16)) % 0.41/0.80 (define @t358 () (_ @t275 @t14)) % 0.41/0.80 (define @t359 () (@list @t5 @t14 @t2)) % 0.41/0.80 (define @t360 () (_ @t279 @t16)) % 0.41/0.80 (define @t361 () (@list @t75 @t16 @t111)) % 0.41/0.80 (define @t362 () (_ @t293 @t42)) % 0.41/0.80 (define @t363 () (@list @t5 @t41 @t2 @t42)) % 0.41/0.80 (define @t364 () (@var "D" tptp.nat)) % 0.41/0.80 (define @t365 () (_ @t299 @t364)) % 0.41/0.80 (define @t366 () (@list @t75 @t110 @t111 @t364)) % 0.41/0.80 (define @t367 () (_ @t283 @t174)) % 0.41/0.80 (define @t368 () (_ @t283 @t2)) % 0.41/0.80 (define @t369 () (_ @t283 @t5)) % 0.41/0.80 (define @t370 () (_ @t287 @t173)) % 0.41/0.80 (define @t371 () (_ @t287 @t111)) % 0.41/0.80 (define @t372 () (_ @t287 @t75)) % 0.41/0.80 (define @t373 () (@list @t16 @t75 @t111)) % 0.41/0.80 (define @t374 () (_ tptp.ord_le976219883lle_hf @t88)) % 0.41/0.80 (define @t375 () (_ tptp.ord_less_eq_nat @t159)) % 0.41/0.80 (define @t376 () (_ @t291 @t81)) % 0.41/0.80 (define @t377 () (_ @t297 @t166)) % 0.41/0.80 (define @t378 () (_ (_ tptp.sup_su638957495lle_hf @t21) @t19)) % 0.41/0.80 (define @t379 () (_ (_ tptp.sup_sup_nat @t210) @t211)) % 0.41/0.80 (define @t380 () (@list @t19 @t21)) % 0.41/0.80 (define @t381 () (@list @t211 @t210)) % 0.41/0.80 (define @t382 () (_ tptp.ord_le976219883lle_hf @t45)) % 0.41/0.80 (define @t383 () (= @t5 @t81)) % 0.41/0.80 (define @t384 () (= @t75 @t166)) % 0.41/0.80 (define @t385 () (_ tptp.ord_le976219883lle_hf @t31)) % 0.41/0.80 (define @t386 () (_ (_ tptp.sup_su638957495lle_hf @t41) @t42)) % 0.41/0.80 (define @t387 () (_ tptp.ord_le976219883lle_hf @t81)) % 0.41/0.80 (define @t388 () (_ (_ tptp.sup_sup_nat @t110) @t364)) % 0.41/0.80 (define @t389 () (_ tptp.ord_less_eq_nat @t166)) % 0.41/0.80 (define @t390 () (_ @t283 @t81)) % 0.41/0.80 (define @t391 () (_ @t287 @t166)) % 0.41/0.80 (define @t392 () (_ @t387 @t14)) % 0.41/0.80 (define @t393 () (_ @t389 @t16)) % 0.41/0.80 (define @t394 () (@var "B6" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t395 () (@var "A6" tptp.hF_Mirabelle_hf)) % 0.41/0.80 (define @t396 () (_ tptp.hF_Mirabelle_hmem @t41)) % 0.41/0.80 (define @t397 () (_ @t396 @t62)) % 0.41/0.80 (define @t398 () (_ @t396 @t36)) % 0.41/0.80 (define @t399 () (= @t256 tptp.zero_zero_nat)) % 0.41/0.80 (define @t400 () (_ tptp.semiri1382578993at_nat @t256)) % 0.41/0.80 (define @t401 () (_ tptp.ord_less_eq_nat @t400)) % 0.41/0.80 (define @t402 () (_ tptp.semiri1382578993at_nat @t259)) % 0.41/0.80 (define @t403 () (@var "Z3" tptp.nat)) % 0.41/0.80 (define @t404 () (@var "Y4" tptp.nat)) % 0.41/0.80 (define @t405 () (= (_ (_ tptp.hF_Mirabelle_hpair tptp.x) tptp.y) tptp.zero_z189798548lle_hf)) % 0.41/0.80 (define @t406 () (not @t405)) % 0.41/0.80 (define @t407 () (not @t406)) % 0.41/0.80 (define @t408 () (lambda @t25 (_ (_ tptp.hF_Mirabelle_hinsert @t24) @t23))) % 0.41/0.80 (define @t409 () (lambda @t25 (_ (_ tptp.member1367349282lle_hf @t21) (_ tptp.hF_Mirabelle_hfset @t19)))) % 0.41/0.80 (define @t410 () (lambda @t380 (= @t329 @t19))) % 0.41/0.80 (define @t411 () (lambda @t381 (= @t330 @t211))) % 0.41/0.80 (define @t412 () (tptp.hF_Mirabelle_Abs_hf tptp.zero_zero_nat)) % 0.41/0.80 (define @t413 () (tptp.hF_Mirabelle_hinsert @t5 @t36)) % 0.41/0.80 (define @t414 () (not (= @t412 @t413))) % 0.41/0.80 (define @t415 () (= @t53 @t413)) % 0.41/0.80 (define @t416 () (not @t415)) % 0.41/0.80 (define @t417 () (= tptp.zero_z189798548lle_hf @t413)) % 0.41/0.80 (define @t418 () (not @t417)) % 0.41/0.80 (define @t419 () (= tptp.zero_z189798548lle_hf @t37)) % 0.41/0.80 (define @t420 () (not @t419)) % 0.41/0.80 (define @t421 () (_ tptp.hF_Mirabelle_hinsert tptp.y)) % 0.41/0.80 (define @t422 () (_ @t421 @t53)) % 0.41/0.80 (define @t423 () (_ tptp.hF_Mirabelle_hinsert tptp.x)) % 0.41/0.80 (define @t424 () (_ @t423 @t422)) % 0.41/0.80 (define @t425 () (_ (_ tptp.hF_Mirabelle_hinsert @t424) @t53)) % 0.41/0.80 (define @t426 () (_ @t423 @t53)) % 0.41/0.80 (define @t427 () (tptp.hF_Mirabelle_hinsert tptp.y @t412)) % 0.41/0.80 (define @t428 () (tptp.hF_Mirabelle_hinsert tptp.x @t427)) % 0.41/0.80 (define @t429 () (tptp.hF_Mirabelle_hinsert @t428 @t412)) % 0.41/0.80 (define @t430 () (tptp.hF_Mirabelle_hinsert tptp.x @t412)) % 0.41/0.80 (define @t431 () (tptp.hF_Mirabelle_hinsert @t430 @t429)) % 0.41/0.80 (define @t432 () (_ (_ tptp.hF_Mirabelle_hinsert @t426) @t425)) % 0.41/0.80 (define @t433 () (_ tptp.hF_Mirabelle_hinsert (_ @t423 tptp.zero_z189798548lle_hf))) % 0.41/0.80 (define @t434 () (_ @t433 (_ (_ tptp.hF_Mirabelle_hinsert (_ @t423 (_ @t421 tptp.zero_z189798548lle_hf))) tptp.zero_z189798548lle_hf))) % 0.41/0.80 (define @t435 () (lambda (@list @t19) (_ @t433 (_ (_ tptp.hF_Mirabelle_hinsert (_ @t423 @t20)) tptp.zero_z189798548lle_hf)))) % 0.41/0.80 (define @t436 () (_ @t408 tptp.x)) % 0.41/0.80 (define @t437 () (= (_ @t436 tptp.y) tptp.zero_z189798548lle_hf)) % 0.41/0.80 (define @t438 () (not (= @t431 @t412))) % 0.41/0.80 (define @t439 () (forall @t39 (not (= @t413 @t412)))) % 0.41/0.80 (assume @p1 (forall @t9 (= @t8 (and @t6 @t3)))) % 0.41/0.80 (assume @p2 (forall @t9 (=> @t8 (not (=> @t6 (not @t3)))))) % 0.41/0.80 (assume @p3 (forall @t10 (not (= @t7 @t5)))) % 0.41/0.80 (assume @p4 (forall @t10 (not (= @t7 @t2)))) % 0.41/0.80 (assume @p5 (forall @t10 (= (_ tptp.hF_Mirabelle_hfst @t7) @t5))) % 0.41/0.80 (assume @p6 (forall @t10 (= (_ tptp.hF_Mirabelle_hsnd @t7) @t2))) % 0.41/0.80 (assume @p7 (= (_ tptp.hF_Mirabelle_HInter tptp.zero_z189798548lle_hf) tptp.zero_z189798548lle_hf)) % 0.41/0.80 (assume @p8 (forall (@list @t11) (= (_ @t12 tptp.zero_z189798548lle_hf) tptp.zero_z189798548lle_hf))) % 0.41/0.80 (assume @p9 (forall (@list @t13) (= (_ (_ tptp.hF_Mirabelle_Replace tptp.zero_z189798548lle_hf) @t13) tptp.zero_z189798548lle_hf))) % 0.41/0.80 (assume @p10 (= (_ tptp.hF_Mirabelle_HUnion tptp.zero_z189798548lle_hf) tptp.zero_z189798548lle_hf)) % 0.41/0.80 (assume @p11 (forall @t15 (= (= tptp.zero_z189798548lle_hf @t14) (= @t14 tptp.zero_z189798548lle_hf)))) % 0.41/0.80 (assume @p12 (forall @t17 (= (= tptp.zero_zero_nat @t16) (= @t16 tptp.zero_zero_nat)))) % 0.41/0.80 (assume @p13 (forall (@list @t18) (= (_ (_ tptp.hF_Mirabelle_RepFun tptp.zero_z189798548lle_hf) @t18) tptp.zero_z189798548lle_hf))) % 0.41/0.80 (assume @p14 (= tptp.hF_Mirabelle_hpair (lambda @t25 (_ (_ tptp.hF_Mirabelle_hinsert (_ @t22 @t24)) @t23)))) % 0.41/0.80 (assume @p15 (forall @t10 (= (= @t30 @t28) @t26))) % 0.41/0.80 (assume @p16 (forall (@list @t5 @t2 @t18) (= (_ (_ tptp.hF_Mirabelle_RepFun (_ @t29 @t2)) @t18) (_ (_ tptp.hF_Mirabelle_hinsert (_ @t18 @t5)) (_ (_ tptp.hF_Mirabelle_RepFun @t2) @t18))))) % 0.41/0.80 (assume @p17 (forall @t35 (= (_ @t32 (_ @t34 @t31)) (_ @t34 (_ @t32 @t31))))) % 0.41/0.80 (assume @p18 @t40) % 0.41/0.80 (assume @p19 (forall (@list @t5 @t2 @t41 @t42) (= (= (_ @t29 @t28) (_ (_ tptp.hF_Mirabelle_hinsert @t41) (_ (_ tptp.hF_Mirabelle_hinsert @t42) tptp.zero_z189798548lle_hf))) (or (and (= @t5 @t41) (= @t2 @t42)) (and (= @t5 @t42) (= @t2 @t41)))))) % 0.41/0.80 (assume @p20 (forall (@list @t11 @t14) (=> @t49 (=> (forall @t48 (=> @t47 (forall (@list @t45) (=> @t46 (_ @t11 (_ (_ tptp.hF_Mirabelle_hinsert @t45) @t44)))))) @t43)))) % 0.41/0.80 (assume @p21 (forall (@list @t36 @t5) (=> @t52 (= (_ tptp.hF_Mirabelle_HInter @t37) (_ @t51 @t50))))) % 0.41/0.80 (assume @p22 (= @t53 tptp.zero_z189798548lle_hf)) % 0.41/0.80 (assume @p23 (forall (@list @t36 @t14) (=> @t52 (= (_ @t55 @t50) (forall @t59 (=> @t58 @t56)))))) % 0.41/0.80 (assume @p24 (forall @t39 (= (_ tptp.hF_Mirabelle_HUnion @t37) (_ @t61 @t60)))) % 0.41/0.80 (assume @p25 (forall (@list @t36 @t5 @t62) (= (_ @t63 (_ @t29 @t62)) (_ (_ tptp.minus_1232880740lle_hf @t64) @t30)))) % 0.41/0.80 (assume @p26 (= tptp.hF_Mirabelle_hinsert (lambda @t25 (_ @t65 @t24)))) % 0.41/0.80 (assume @p27 (forall (@list @t11 @t31) (=> @t49 (=> (forall @t67 (=> @t47 (=> @t46 (=> (not (_ @t66 @t45)) (_ @t11 (_ (_ tptp.hF_Mirabelle_hinsert @t44) @t45)))))) (_ @t11 @t31))))) % 0.41/0.80 (assume @p28 (forall (@list @t33) (=> (not (= @t33 tptp.zero_z189798548lle_hf)) (not (forall (@list @t69 @t68) (=> (= @t33 (_ (_ tptp.hF_Mirabelle_hinsert @t69) @t68)) (_ (_ tptp.hF_Mirabelle_hmem @t69) @t68))))))) % 0.41/0.80 (assume @p29 (forall (@list @t36 @t62 @t13) (= (_ (_ tptp.hF_Mirabelle_Replace @t74) @t13) (_ (_ tptp.sup_su638957495lle_hf @t72) (_ @t70 @t13))))) % 0.41/0.80 (assume @p30 (forall (@list @t14 @t11 @t36) (= (_ @t55 (_ @t12 @t36)) (and @t43 (_ @t55 @t36))))) % 0.41/0.80 (assume @p31 (forall @t10 (=> (forall @t48 (= (_ @t66 @t5) (_ @t66 @t2))) @t26))) % 0.41/0.80 (assume @p32 (forall @t77 (= (_ @t76 @t75) tptp.zero_zero_nat))) % 0.41/0.80 (assume @p33 (forall @t77 (= (_ @t78 tptp.zero_zero_nat) @t75))) % 0.41/0.80 (assume @p34 (forall @t77 (= (_ @t78 @t75) tptp.zero_zero_nat))) % 0.41/0.80 (assume @p35 (forall @t80 (= (_ @t79 (_ @t27 @t41)) (or @t26 (_ @t79 @t41))))) % 0.41/0.80 (assume @p36 (forall @t82 (= (_ @t55 @t81) (or (_ @t55 @t5) (_ @t55 @t2))))) % 0.41/0.80 (assume @p37 (forall @t89 (= (_ @t84 @t88) (and @t86 @t85)))) % 0.41/0.80 (assume @p38 (forall (@list @t92 @t36 @t18) (= (_ @t97 @t96) (exists @t95 (and @t94 (= @t92 @t91)))))) % 0.41/0.80 (assume @p39 (forall @t98 (= (_ (_ tptp.sup_su638957495lle_hf tptp.zero_z189798548lle_hf) @t36) @t36))) % 0.41/0.80 (assume @p40 (forall @t98 (= (_ @t73 tptp.zero_z189798548lle_hf) @t36))) % 0.41/0.80 (assume @p41 (forall (@list @t14 @t36) (= (_ @t55 @t60) (exists @t59 (and @t58 @t56))))) % 0.41/0.80 (assume @p42 (forall (@list @t5 @t11) (= (_ (_ tptp.member1367349282lle_hf @t5) @t99) (_ @t11 @t5)))) % 0.41/0.80 (assume @p43 (forall (@list @t100) (= (_ tptp.collec2046588256lle_hf (lambda @t102 (_ (_ tptp.member1367349282lle_hf @t101) @t100))) @t100))) % 0.41/0.80 (assume @p44 (forall (@list @t11 @t103) (=> (forall @t48 (= @t47 (_ @t103 @t44))) (= @t99 (_ tptp.collec2046588256lle_hf @t103))))) % 0.41/0.80 (assume @p45 (forall @t89 (= (_ @t84 (_ @t104 @t33)) (and @t86 (not @t85))))) % 0.41/0.80 (assume @p46 (forall @t98 (= (_ (_ tptp.inf_in956532509lle_hf tptp.zero_z189798548lle_hf) @t36) tptp.zero_z189798548lle_hf))) % 0.41/0.80 (assume @p47 (forall @t98 (= (_ @t105 tptp.zero_z189798548lle_hf) tptp.zero_z189798548lle_hf))) % 0.41/0.80 (assume @p48 (forall (@list @t92 @t36 @t13) (= (_ @t97 @t72) (exists @t95 (and @t94 @t107 (forall @t59 (=> (_ @t106 @t54) (= @t54 @t92)))))))) % 0.41/0.80 (assume @p49 (forall @t15 (= (_ @t104 tptp.zero_z189798548lle_hf) @t14))) % 0.41/0.80 (assume @p50 (forall @t15 (= (_ (_ tptp.minus_1232880740lle_hf tptp.zero_z189798548lle_hf) @t14) tptp.zero_z189798548lle_hf))) % 0.41/0.80 (assume @p51 (forall (@list @t36 @t62 @t18) (= (_ (_ tptp.hF_Mirabelle_RepFun @t74) @t18) (_ (_ tptp.sup_su638957495lle_hf @t96) (_ @t108 @t18))))) % 0.41/0.80 (assume @p52 (forall @t109 (= (_ tptp.hF_Mirabelle_HUnion @t74) (_ (_ tptp.sup_su638957495lle_hf @t60) (_ tptp.hF_Mirabelle_HUnion @t62))))) % 0.41/0.80 (assume @p53 (forall @t112 (= (_ (_ tptp.minus_minus_nat (_ @t78 @t110)) @t111) (_ (_ tptp.minus_minus_nat (_ @t78 @t111)) @t110)))) % 0.41/0.80 (assume @p54 (forall (@list @t14 @t18) (exists @t118 (forall @t117 (= @t116 (exists @t95 (and @t114 (= @t113 @t91)))))))) % 0.41/0.80 (assume @p55 (forall @t15 (not (_ @t55 @t14)))) % 0.41/0.80 (assume @p56 (forall (@list @t14 @t11) (exists @t118 (forall @t123 (= @t122 (and @t121 (_ @t11 @t119))))))) % 0.41/0.80 (assume @p57 (forall @t15 (exists @t118 (forall @t123 (= @t122 (exists @t59 (and (_ @t57 @t14) (_ @t120 @t54)))))))) % 0.41/0.80 (assume @p58 (forall @t125 (not (and @t124 (_ (_ tptp.hF_Mirabelle_hmem @t33) @t14))))) % 0.41/0.80 (assume @p59 (forall @t125 (exists @t118 (forall @t123 (= @t122 (or @t121 (_ @t120 @t33))))))) % 0.41/0.80 (assume @p60 (forall (@list @t14 @t13) (=> (forall @t132 (=> (_ @t131 @t14) @t130)) (exists @t118 (forall @t117 (= @t116 (exists @t95 (and @t114 (_ @t106 @t113))))))))) % 0.41/0.80 (assume @p61 (forall @t125 (=> @t124 (not (= @t14 @t33))))) % 0.41/0.80 (assume @p62 (= @t136 (lambda @t25 (forall @t102 (= (_ @t133 @t21) (_ @t133 @t19)))))) % 0.41/0.80 (assume @p63 (forall @t143 (and (=> @t141 (= @t140 (_ @t32 @t138))) (=> @t142 (= @t140 @t138))))) % 0.41/0.80 (assume @p64 (forall @t143 (and (=> @t141 (= @t145 (_ @t32 @t144))) (=> @t142 (= @t145 @t144))))) % 0.41/0.80 (assume @p65 (forall @t148 (=> (not @t147) (exists (@list @t146) (and (_ (_ tptp.hF_Mirabelle_hmem @t146) @t31) (= (_ (_ tptp.inf_in956532509lle_hf @t146) @t31) tptp.zero_z189798548lle_hf)))))) % 0.41/0.80 (assume @p66 (forall @t143 (and (=> @t141 (= @t149 @t64)) (=> @t142 (= @t149 (_ @t32 @t64)))))) % 0.41/0.80 (assume @p67 (forall (@list @t31 @t33 @t14) (= (= @t31 (_ @t34 @t14)) (forall @t95 (= (_ @t93 @t31) (or @t114 (= @t90 @t33))))))) % 0.41/0.80 (assume @p68 (forall @t150 (not (_ @t79 tptp.zero_z189798548lle_hf)))) % 0.41/0.80 (assume @p69 (forall @t148 (= @t147 (forall @t102 (not (_ @t133 @t31)))))) % 0.41/0.80 (assume @p70 (forall (@list @t62 @t14 @t36) (= (_ @t151 @t139) (_ @t32 (_ @t151 @t36))))) % 0.41/0.80 (assume @p71 (forall (@list @t14 @t36 @t62) (= (_ (_ tptp.sup_su638957495lle_hf @t139) @t62) (_ @t32 @t74)))) % 0.41/0.80 (assume @p72 (forall (@list @t36 @t62 @t18 @t152) (=> @t154 (=> (forall @t48 (=> @t153 (= (_ @t18 @t44) (_ @t152 @t44)))) (= @t96 (_ @t108 @t152)))))) % 0.41/0.80 (assume @p73 (forall @t125 (=> @t124 (not (= (_ tptp.hF_Mirabelle_HUnion @t14) @t33))))) % 0.41/0.80 (assume @p74 (forall (@list @t36 @t62 @t156 @t155) (=> @t154 (=> (forall @t67 (=> @t153 (= (_ (_ @t156 @t44) @t45) (_ (_ @t155 @t44) @t45)))) (= (_ @t71 @t156) (_ @t70 @t155)))))) % 0.41/0.80 (assume @p75 (forall @t161 (= (_ @t160 @t159) @t16))) % 0.41/0.80 (assume @p76 (forall @t125 (= (_ @t162 @t88) @t14))) % 0.41/0.80 (assume @p77 (forall @t161 (= (_ @t158 @t163) @t16))) % 0.41/0.80 (assume @p78 (forall @t125 (= (_ @t87 @t164) @t14))) % 0.41/0.80 (assume @p79 (forall @t168 (= (_ @t167 @t111) @t166))) % 0.41/0.80 (assume @p80 (forall @t10 (= (_ @t169 @t2) @t81))) % 0.41/0.80 (assume @p81 (forall @t161 (= (_ @t160 @t163) @t163))) % 0.41/0.80 (assume @p82 (forall @t125 (= (_ @t162 @t164) @t164))) % 0.41/0.80 (assume @p83 (forall @t168 (= (_ @t165 @t166) @t166))) % 0.41/0.80 (assume @p84 (forall @t10 (= (_ @t61 @t81) @t81))) % 0.41/0.80 (assume @p85 (forall @t17 (= (_ @t160 @t16) @t16))) % 0.41/0.80 (assume @p86 (forall @t15 (= (_ @t162 @t14) @t14))) % 0.41/0.80 (assume @p87 (forall @t77 (= (_ @t165 @t75) @t75))) % 0.41/0.80 (assume @p88 (forall @t150 (= (_ @t61 @t5) @t5))) % 0.41/0.80 (assume @p89 (forall @t161 (= (_ @t170 @t157) @t159))) % 0.41/0.80 (assume @p90 (forall @t125 (= (_ @t171 @t33) @t88))) % 0.41/0.80 (assume @p91 (forall @t77 (= (_ @t172 @t75) @t75))) % 0.41/0.80 (assume @p92 (forall @t150 (= (_ @t51 @t5) @t5))) % 0.41/0.80 (assume @p93 (forall @t17 (= (_ @t158 @t16) @t16))) % 0.41/0.80 (assume @p94 (forall @t15 (= (_ @t87 @t14) @t14))) % 0.41/0.80 (assume @p95 (forall @t168 (= (_ @t172 @t173) @t173))) % 0.41/0.80 (assume @p96 (forall @t10 (= (_ @t51 @t174) @t174))) % 0.41/0.80 (assume @p97 (forall @t161 (= (_ @t158 @t159) @t159))) % 0.41/0.80 (assume @p98 (forall @t125 (= (_ @t87 @t88) @t88))) % 0.41/0.80 (assume @p99 (forall @t168 (= (_ @t175 @t111) @t173))) % 0.41/0.80 (assume @p100 (forall @t10 (= (_ @t176 @t2) @t174))) % 0.41/0.80 (assume @p101 (forall @t182 (= @t181 (_ @t179 @t178)))) % 0.41/0.80 (assume @p102 (forall @t35 (= @t186 (_ @t184 @t183)))) % 0.41/0.80 (assume @p103 (forall @t182 (= (_ @t170 @t177) @t181))) % 0.41/0.80 (assume @p104 (forall @t35 (= (_ @t171 @t31) @t186))) % 0.41/0.80 (assume @p105 (= tptp.inf_inf_nat (lambda @t189 (_ (_ tptp.inf_inf_nat @t188) @t187)))) % 0.41/0.80 (assume @p106 (= tptp.inf_in956532509lle_hf (lambda @t190 (_ (_ tptp.inf_in956532509lle_hf @t54) @t101)))) % 0.41/0.80 (assume @p107 (forall @t195 (=> (= @t194 (_ @t192 @t75)) (= (_ (_ tptp.inf_inf_nat @t194) @t111) @t193)))) % 0.41/0.80 (assume @p108 (forall @t199 (=> (= @t36 (_ @t197 @t5)) (= (_ @t105 @t2) @t198)))) % 0.41/0.80 (assume @p109 (forall @t201 (=> (= @t200 (_ @t192 @t111)) (= (_ @t172 @t200) @t193)))) % 0.41/0.80 (assume @p110 (forall @t202 (=> (= @t62 (_ @t197 @t2)) (= (_ @t51 @t62) @t198)))) % 0.41/0.80 (assume @p111 (forall @t206 (= (_ @t175 @t110) @t205))) % 0.41/0.80 (assume @p112 (forall @t80 (= (_ @t176 @t41) @t209))) % 0.41/0.80 (assume @p113 (= tptp.inf_inf_nat (lambda @t212 (_ (_ tptp.inf_inf_nat @t211) @t210)))) % 0.41/0.80 (assume @p114 (= tptp.inf_in956532509lle_hf (lambda @t25 (_ (_ tptp.inf_in956532509lle_hf @t19) @t21)))) % 0.41/0.80 (assume @p115 (forall @t213 (= (_ @t203 (_ @t172 @t110)) @t205))) % 0.41/0.80 (assume @p116 (forall @t214 (= (_ @t207 (_ @t51 @t41)) @t209))) % 0.41/0.80 (assume @p117 (forall @t182 (= @t218 (_ @t216 @t215)))) % 0.41/0.80 (assume @p118 (forall @t35 (= @t222 (_ @t220 @t219)))) % 0.41/0.80 (assume @p119 (forall @t182 (= (_ (_ tptp.sup_sup_nat @t163) @t177) @t218))) % 0.41/0.80 (assume @p120 (forall @t35 (= (_ (_ tptp.sup_su638957495lle_hf @t164) @t31) @t222))) % 0.41/0.80 (assume @p121 (= tptp.sup_sup_nat (lambda @t189 (_ (_ tptp.sup_sup_nat @t188) @t187)))) % 0.41/0.80 (assume @p122 (= tptp.sup_su638957495lle_hf (lambda @t190 (_ (_ tptp.sup_su638957495lle_hf @t54) @t101)))) % 0.41/0.80 (assume @p123 (forall @t195 (=> (= @t194 (_ @t223 @t75)) (= (_ (_ tptp.sup_sup_nat @t194) @t111) @t224)))) % 0.41/0.80 (assume @p124 (forall @t199 (=> (= @t36 (_ @t225 @t5)) (= (_ @t73 @t2) @t226)))) % 0.41/0.80 (assume @p125 (forall @t201 (=> (= @t200 (_ @t223 @t111)) (= (_ @t165 @t200) @t224)))) % 0.41/0.80 (assume @p126 (forall @t202 (=> (= @t62 (_ @t225 @t2)) (= (_ @t61 @t62) @t226)))) % 0.41/0.80 (assume @p127 (forall @t206 (= (_ @t167 @t110) @t229))) % 0.41/0.80 (assume @p128 (forall @t80 (= (_ @t169 @t41) @t232))) % 0.41/0.80 (assume @p129 (= tptp.sup_sup_nat (lambda @t212 (_ (_ tptp.sup_sup_nat @t211) @t210)))) % 0.41/0.80 (assume @p130 (= tptp.sup_su638957495lle_hf (lambda @t25 (_ @t65 @t21)))) % 0.41/0.80 (assume @p131 (forall @t213 (= (_ @t227 (_ @t165 @t110)) @t229))) % 0.41/0.80 (assume @p132 (forall @t214 (= (_ @t230 (_ @t61 @t41)) @t232))) % 0.41/0.80 (assume @p133 (forall @t182 (=> (forall @t240 (= (_ @t238 (_ (_ tptp.sup_sup_nat @t239) @t236)) (_ (_ tptp.sup_sup_nat (_ @t238 @t239)) (_ @t238 @t236)))) @t235))) % 0.41/0.80 (assume @p134 (forall @t35 (=> (forall @t245 (= (_ @t244 (_ (_ tptp.sup_su638957495lle_hf @t45) @t115)) (_ (_ tptp.sup_su638957495lle_hf (_ @t244 @t45)) (_ @t244 @t115)))) @t243))) % 0.41/0.80 (assume @p135 (forall @t182 (=> (forall @t240 (= (_ @t249 (_ (_ tptp.inf_inf_nat @t239) @t236)) (_ (_ tptp.inf_inf_nat (_ @t249 @t239)) (_ @t249 @t236)))) @t248))) % 0.41/0.80 (assume @p136 (forall @t35 (=> (forall @t245 (= (_ @t253 (_ (_ tptp.inf_in956532509lle_hf @t45) @t115)) (_ (_ tptp.inf_in956532509lle_hf (_ @t253 @t45)) (_ @t253 @t115)))) @t252))) % 0.41/0.80 (assume @p137 (forall @t182 @t248)) % 0.41/0.80 (assume @p138 (forall @t35 @t252)) % 0.41/0.80 (assume @p139 (forall @t254 (= (_ (_ tptp.inf_inf_nat @t217) @t16) (_ (_ tptp.sup_sup_nat (_ @t179 @t16)) (_ (_ tptp.inf_inf_nat @t177) @t16))))) % 0.41/0.80 (assume @p140 (forall @t255 (= (_ (_ tptp.inf_in956532509lle_hf @t221) @t14) (_ (_ tptp.sup_su638957495lle_hf (_ @t184 @t14)) (_ (_ tptp.inf_in956532509lle_hf @t31) @t14))))) % 0.41/0.80 (assume @p141 (forall @t182 @t235)) % 0.41/0.80 (assume @p142 (forall @t35 @t243)) % 0.41/0.80 (assume @p143 (forall @t254 (= (_ (_ tptp.sup_sup_nat @t180) @t16) (_ (_ tptp.inf_inf_nat (_ @t216 @t16)) (_ (_ tptp.sup_sup_nat @t177) @t16))))) % 0.41/0.80 (assume @p144 (forall @t255 (= (_ (_ tptp.sup_su638957495lle_hf @t185) @t14) (_ (_ tptp.inf_in956532509lle_hf (_ @t220 @t14)) (_ (_ tptp.sup_su638957495lle_hf @t31) @t14))))) % 0.41/0.80 (assume @p145 (forall @t258 (= (_ @t257 @t256) tptp.zero_zero_nat))) % 0.41/0.80 (assume @p146 (forall @t260 (= (_ @t76 @t259) tptp.zero_zero_nat))) % 0.41/0.80 (assume @p147 (forall (@list @t36 @t13 @t92) (=> (forall @t132 (=> (_ @t131 @t36) @t130)) (= (_ @t97 (_ (_ tptp.hF_Mir1248913145eplace @t36) @t13)) (exists @t95 (and @t94 @t107)))))) % 0.41/0.80 (assume @p148 (forall @t265 (=> @t264 (=> (= (_ @t262 @t256) tptp.zero_zero_nat) @t261)))) % 0.41/0.80 (assume @p149 (forall @t258 (= (_ @t257 tptp.zero_zero_nat) @t256))) % 0.41/0.80 (assume @p150 (= tptp.zero_zero_nat tptp.zero_zero_nat)) % 0.41/0.80 (assume @p151 (forall @t269 (= (_ (_ tptp.minus_minus_nat (_ @t268 @t266)) @t191) (_ (_ tptp.minus_minus_nat (_ @t268 @t191)) @t266)))) % 0.41/0.80 (assume @p152 (forall @t35 (= (_ (_ tptp.ord_le976219883lle_hf @t272) @t31) (and (_ @t55 @t31) @t271)))) % 0.41/0.80 (assume @p153 (forall @t265 (= @t264 @t273))) % 0.41/0.80 (assume @p154 (forall @t260 (= (_ @t274 tptp.zero_zero_nat) (= @t259 tptp.zero_zero_nat)))) % 0.41/0.80 (assume @p155 (forall @t80 (= @t278 (and @t277 @t276)))) % 0.41/0.80 (assume @p156 (forall @t206 (= @t282 (and @t281 @t280)))) % 0.41/0.80 (assume @p157 (forall @t35 (= @t286 (and @t285 @t284)))) % 0.41/0.80 (assume @p158 (forall @t182 (= @t290 (and @t289 @t288)))) % 0.41/0.80 (assume @p159 (forall @t296 (= @t295 (and @t294 @t292)))) % 0.41/0.80 (assume @p160 (forall @t302 (= @t301 (and @t300 @t298)))) % 0.41/0.80 (assume @p161 (forall @t35 (= (_ (_ tptp.ord_le976219883lle_hf @t164) @t31) (and @t284 @t271)))) % 0.41/0.80 (assume @p162 (forall @t182 (= (_ (_ tptp.ord_less_eq_nat @t163) @t177) (and @t288 (_ @t303 @t177))))) % 0.41/0.80 (assume @p163 (forall @t77 (_ @t304 @t75))) % 0.41/0.80 (assume @p164 (forall @t260 (_ @t304 @t259))) % 0.41/0.80 (assume @p165 (forall (@list @t267 @t259) (=> (_ @t305 @t259) (= (_ @t262 (_ @t262 @t267)) @t267)))) % 0.41/0.80 (assume @p166 (forall @t109 (=> (forall @t48 (=> (_ @t66 @t36) @t153)) @t306))) % 0.41/0.80 (assume @p167 (forall (@list @t83) (= (_ (_ tptp.ord_le976219883lle_hf @t83) tptp.zero_z189798548lle_hf) (= @t83 tptp.zero_z189798548lle_hf)))) % 0.41/0.80 (assume @p168 (forall @t265 (=> @t273 @t264))) % 0.41/0.80 (assume @p169 (forall @t309 (=> @t273 (_ (_ tptp.ord_less_eq_nat (_ @t308 @t259)) (_ @t308 @t256))))) % 0.41/0.80 (assume @p170 (forall @t112 (=> @t280 (=> @t311 (= (_ (_ tptp.ord_less_eq_nat (_ @t310 @t75)) (_ @t310 @t111)) @t300))))) % 0.41/0.80 (assume @p171 (forall @t265 (_ (_ tptp.ord_less_eq_nat @t263) @t256))) % 0.41/0.80 (assume @p172 (forall @t309 (=> @t273 (_ (_ tptp.ord_less_eq_nat (_ @t257 @t307)) (_ @t262 @t307))))) % 0.41/0.80 (assume @p173 (forall @t317 (=> @t316 (=> @t315 (= (_ (_ tptp.minus_minus_nat @t313) @t312) @t263))))) % 0.41/0.80 (assume @p174 (forall @t317 (=> @t316 (=> @t315 (= (_ (_ tptp.ord_less_eq_nat @t313) @t312) @t273))))) % 0.41/0.80 (assume @p175 (forall @t317 (=> @t316 (=> @t315 (= (= @t313 @t312) @t261))))) % 0.41/0.80 (assume @p176 (forall @t77 (=> @t319 @t318))) % 0.41/0.80 (assume @p177 (forall @t77 (= @t319 @t318))) % 0.41/0.80 (assume @p178 (forall (@list @t321 @t191 @t111) (=> (_ @t321 @t191) (=> (forall (@list @t239) (=> (_ @t321 @t239) (_ @t322 @t111))) (exists (@list @t237) (and (_ @t321 @t237) (forall (@list @t320) (=> (_ @t321 @t320) (_ (_ tptp.ord_less_eq_nat @t320) @t237))))))))) % 0.41/0.80 (assume @p179 (forall @t265 (or @t273 @t323))) % 0.41/0.80 (assume @p180 (forall @t265 (=> @t273 (=> @t323 @t261)))) % 0.41/0.80 (assume @p181 (forall @t265 (=> @t261 @t273))) % 0.41/0.80 (assume @p182 (forall @t269 (=> @t324 (=> (_ (_ tptp.ord_less_eq_nat @t266) @t191) (_ @t305 @t191))))) % 0.41/0.80 (assume @p183 (forall @t260 (_ @t274 @t259))) % 0.41/0.80 (assume @p184 (forall @t17 (_ @t304 @t16))) % 0.41/0.80 (assume @p185 (forall @t296 (=> (_ @t293 @t41) @t326))) % 0.41/0.80 (assume @p186 (forall @t302 (=> @t311 @t328))) % 0.41/0.80 (assume @p187 (forall (@list @t5 @t41 @t2) (=> @t276 @t326))) % 0.41/0.80 (assume @p188 (forall @t112 (=> @t280 @t328))) % 0.41/0.80 (assume @p189 (= tptp.ord_le976219883lle_hf (lambda @t25 (= @t329 @t21)))) % 0.41/0.80 (assume @p190 (= tptp.ord_less_eq_nat (lambda @t212 (= @t330 @t210)))) % 0.41/0.80 (assume @p191 (forall @t10 (_ @t325 @t2))) % 0.41/0.80 (assume @p192 (forall @t168 (_ @t327 @t111))) % 0.41/0.80 (assume @p193 (forall @t10 (_ @t325 @t5))) % 0.41/0.80 (assume @p194 (forall @t168 (_ @t327 @t75))) % 0.41/0.80 (assume @p195 (= tptp.ord_le976219883lle_hf (lambda @t25 (= @t21 @t329)))) % 0.41/0.80 (assume @p196 (= tptp.ord_less_eq_nat (lambda @t212 (= @t210 @t330)))) % 0.41/0.80 (assume @p197 (forall @t35 (=> @t285 (=> @t284 @t286)))) % 0.41/0.80 (assume @p198 (forall @t182 (=> @t289 (=> @t288 @t290)))) % 0.41/0.80 (assume @p199 (forall @t80 (=> @t277 (=> @t276 @t278)))) % 0.41/0.80 (assume @p200 (forall @t206 (=> @t281 (=> @t280 @t282)))) % 0.41/0.80 (assume @p201 (forall @t80 (=> @t278 (not (=> @t277 (not @t276)))))) % 0.41/0.80 (assume @p202 (forall @t206 (=> @t282 (not (=> @t281 (not @t280)))))) % 0.41/0.80 (assume @p203 (forall @t332 (=> @t331 (= @t88 @t33)))) % 0.41/0.80 (assume @p204 (forall @t334 (=> @t333 (= @t159 @t157)))) % 0.41/0.80 (assume @p205 (forall @t125 (=> @t285 (= @t88 @t14)))) % 0.41/0.80 (assume @p206 (forall @t161 (=> @t289 (= @t159 @t16)))) % 0.41/0.80 (assume @p207 (forall @t335 (=> @t294 (= @t174 @t2)))) % 0.41/0.80 (assume @p208 (forall @t336 (=> @t300 (= @t173 @t111)))) % 0.41/0.80 (assume @p209 (forall @t10 (=> @t277 (= @t174 @t5)))) % 0.41/0.80 (assume @p210 (forall @t168 (=> @t281 (= @t173 @t75)))) % 0.41/0.80 (assume @p211 (= tptp.ord_le976219883lle_hf (lambda @t190 (= (_ (_ tptp.inf_in956532509lle_hf @t101) @t54) @t101)))) % 0.41/0.80 (assume @p212 (= tptp.ord_less_eq_nat (lambda @t189 (= (_ (_ tptp.inf_inf_nat @t187) @t188) @t187)))) % 0.41/0.80 (assume @p213 (forall @t343 (=> (forall @t67 (_ @t342 @t44)) (=> (forall @t67 (_ @t342 @t45)) (=> (forall @t245 (=> (_ @t340 @t45) (=> (_ @t340 @t115) (_ @t340 @t339)))) (= @t88 @t338)))))) % 0.41/0.80 (assume @p214 (forall @t351 (=> (forall @t350 (_ @t349 @t237)) (=> (forall @t350 (_ @t349 @t239)) (=> (forall @t240 (=> (_ @t347 @t239) (=> (_ @t347 @t236) (_ @t347 @t346)))) (= @t159 @t345)))))) % 0.41/0.80 (assume @p215 (forall @t10 (=> @t352 @t277))) % 0.41/0.80 (assume @p216 (forall @t168 (=> @t353 @t281))) % 0.41/0.80 (assume @p217 (forall @t10 (=> @t277 @t352))) % 0.41/0.80 (assume @p218 (forall @t168 (=> @t281 @t353))) % 0.41/0.80 (assume @p219 (forall (@list @t2 @t14 @t5) (=> @t355 @t354))) % 0.41/0.80 (assume @p220 (forall (@list @t111 @t16 @t75) (=> @t357 @t356))) % 0.41/0.80 (assume @p221 (forall @t359 (=> @t358 @t354))) % 0.41/0.80 (assume @p222 (forall @t361 (=> @t360 @t356))) % 0.41/0.80 (assume @p223 (forall @t363 (=> @t276 (=> @t362 (_ @t325 (_ (_ tptp.inf_in956532509lle_hf @t41) @t42)))))) % 0.41/0.80 (assume @p224 (forall @t366 (=> @t280 (=> @t365 (_ @t327 (_ (_ tptp.inf_inf_nat @t110) @t364)))))) % 0.41/0.80 (assume @p225 (forall @t82 (=> @t369 (=> @t368 @t367)))) % 0.41/0.80 (assume @p226 (forall @t373 (=> @t372 (=> @t371 @t370)))) % 0.41/0.80 (assume @p227 (forall @t82 (=> @t367 (not (=> @t369 (not @t368)))))) % 0.41/0.80 (assume @p228 (forall @t373 (=> @t370 (not (=> @t372 (not @t371)))))) % 0.41/0.80 (assume @p229 (forall @t125 (_ @t374 @t33))) % 0.41/0.80 (assume @p230 (forall @t161 (_ @t375 @t157))) % 0.41/0.80 (assume @p231 (forall @t125 (_ @t374 @t14))) % 0.41/0.80 (assume @p232 (forall @t161 (_ @t375 @t16))) % 0.41/0.80 (assume @p233 (forall (@list @t41 @t2 @t5) (=> (_ @t291 @t2) @t376))) % 0.41/0.80 (assume @p234 (forall (@list @t110 @t111 @t75) (=> (_ @t297 @t111) @t377))) % 0.41/0.80 (assume @p235 (forall (@list @t41 @t5 @t2) (=> @t292 @t376))) % 0.41/0.80 (assume @p236 (forall (@list @t110 @t75 @t111) (=> @t298 @t377))) % 0.41/0.80 (assume @p237 (= tptp.ord_le976219883lle_hf (lambda @t25 (= @t378 @t19)))) % 0.41/0.80 (assume @p238 (= tptp.ord_less_eq_nat (lambda @t212 (= @t379 @t211)))) % 0.41/0.80 (assume @p239 (= tptp.ord_le976219883lle_hf (lambda @t380 (= @t378 @t21)))) % 0.41/0.80 (assume @p240 (= tptp.ord_less_eq_nat (lambda @t381 (= @t379 @t210)))) % 0.41/0.80 (assume @p241 (forall @t335 (_ @t293 @t81))) % 0.41/0.80 (assume @p242 (forall @t336 (_ @t299 @t166))) % 0.41/0.80 (assume @p243 (forall @t10 (_ @t275 @t81))) % 0.41/0.80 (assume @p244 (forall @t168 (_ @t279 @t166))) % 0.41/0.80 (assume @p245 (= tptp.ord_le976219883lle_hf (lambda @t380 (= @t21 @t378)))) % 0.41/0.80 (assume @p246 (= tptp.ord_less_eq_nat (lambda @t381 (= @t210 @t379)))) % 0.41/0.80 (assume @p247 (forall @t214 (=> @t294 (=> @t292 @t295)))) % 0.41/0.80 (assume @p248 (forall @t213 (=> @t300 (=> @t298 @t301)))) % 0.41/0.80 (assume @p249 (forall @t296 (=> @t295 (not (=> @t294 (not @t292)))))) % 0.41/0.80 (assume @p250 (forall @t302 (=> @t301 (not (=> @t300 (not @t298)))))) % 0.41/0.80 (assume @p251 (forall @t125 (=> @t285 (= @t164 @t33)))) % 0.41/0.80 (assume @p252 (forall @t161 (=> @t289 (= @t163 @t157)))) % 0.41/0.80 (assume @p253 (forall @t332 (=> @t331 (= @t164 @t14)))) % 0.41/0.80 (assume @p254 (forall @t334 (=> @t333 (= @t163 @t16)))) % 0.41/0.80 (assume @p255 (forall @t10 (=> @t277 (= @t81 @t2)))) % 0.41/0.80 (assume @p256 (forall @t168 (=> @t281 (= @t166 @t111)))) % 0.41/0.80 (assume @p257 (forall @t335 (=> @t294 (= @t81 @t5)))) % 0.41/0.80 (assume @p258 (forall @t336 (=> @t300 (= @t166 @t75)))) % 0.41/0.80 (assume @p259 (forall @t343 (=> (forall @t67 (_ @t340 @t341)) (=> (forall @t67 (_ @t382 @t341)) (=> (forall @t245 (=> (_ @t382 @t44) (=> (_ (_ tptp.ord_le976219883lle_hf @t115) @t44) (_ (_ tptp.ord_le976219883lle_hf @t339) @t44)))) (= @t164 @t338)))))) % 0.41/0.80 (assume @p260 (forall @t351 (=> (forall @t350 (_ @t347 @t348)) (=> (forall @t350 (_ @t322 @t348)) (=> (forall @t240 (=> (_ @t322 @t237) (=> (_ (_ tptp.ord_less_eq_nat @t236) @t237) (_ (_ tptp.ord_less_eq_nat @t346) @t237)))) (= @t163 @t345)))))) % 0.41/0.80 (assume @p261 (forall @t10 (=> @t383 @t294))) % 0.41/0.80 (assume @p262 (forall @t168 (=> @t384 @t300))) % 0.41/0.80 (assume @p263 (forall @t335 (=> @t294 @t383))) % 0.41/0.80 (assume @p264 (forall @t336 (=> @t300 @t384))) % 0.41/0.80 (assume @p265 (= tptp.ord_le976219883lle_hf (lambda @t190 (= (_ (_ tptp.sup_su638957495lle_hf @t101) @t54) @t54)))) % 0.41/0.80 (assume @p266 (= tptp.ord_less_eq_nat (lambda @t189 (= (_ (_ tptp.sup_sup_nat @t187) @t188) @t188)))) % 0.41/0.80 (assume @p267 (forall (@list @t33 @t14 @t31) (=> @t331 (=> (_ @t385 @t14) (_ (_ tptp.ord_le976219883lle_hf @t221) @t14))))) % 0.41/0.80 (assume @p268 (forall (@list @t157 @t16 @t177) (=> @t333 (=> (_ (_ tptp.ord_less_eq_nat @t177) @t16) (_ (_ tptp.ord_less_eq_nat @t217) @t16))))) % 0.41/0.80 (assume @p269 (forall @t363 (=> @t276 (=> @t362 (_ @t387 @t386))))) % 0.41/0.80 (assume @p270 (forall @t366 (=> @t280 (=> @t365 (_ @t389 @t388))))) % 0.41/0.80 (assume @p271 (forall (@list @t41 @t5 @t42 @t2) (=> @t292 (=> (_ (_ tptp.ord_le976219883lle_hf @t42) @t2) (_ (_ tptp.ord_le976219883lle_hf @t386) @t81))))) % 0.41/0.80 (assume @p272 (forall (@list @t110 @t75 @t364 @t111) (=> @t298 (=> (_ (_ tptp.ord_less_eq_nat @t364) @t111) (_ (_ tptp.ord_less_eq_nat @t388) @t166))))) % 0.41/0.80 (assume @p273 (forall (@list @t14 @t2 @t5) (=> @t368 @t390))) % 0.41/0.80 (assume @p274 (forall (@list @t16 @t111 @t75) (=> @t371 @t391))) % 0.41/0.80 (assume @p275 (forall @t82 (=> @t369 @t390))) % 0.41/0.80 (assume @p276 (forall @t373 (=> @t372 @t391))) % 0.41/0.80 (assume @p277 (forall @t332 (_ @t270 @t164))) % 0.41/0.80 (assume @p278 (forall @t334 (_ @t303 @t163))) % 0.41/0.80 (assume @p279 (forall @t125 (_ @t283 @t164))) % 0.41/0.80 (assume @p280 (forall @t161 (_ @t287 @t163))) % 0.41/0.80 (assume @p281 (forall @t359 (=> @t358 (=> @t355 @t392)))) % 0.41/0.80 (assume @p282 (forall @t361 (=> @t360 (=> @t357 @t393)))) % 0.41/0.80 (assume @p283 (forall (@list @t5 @t2 @t14) (=> @t392 (not (=> @t358 (not @t355)))))) % 0.41/0.80 (assume @p284 (forall (@list @t75 @t111 @t16) (=> @t393 (not (=> @t360 (not @t357)))))) % 0.41/0.80 (assume @p285 (= tptp.ord_le976219883lle_hf (lambda (@list @t395 @t394) (forall @t102 (=> (_ @t133 @t395) (_ @t133 @t394)))))) % 0.41/0.80 (assume @p286 (forall (@list @t41 @t36 @t62) (=> @t398 (=> @t306 @t397)))) % 0.41/0.80 (assume @p287 (forall (@list @t36 @t62 @t41) (=> @t306 (=> @t398 @t397)))) % 0.41/0.80 (assume @p288 (forall @t15 (_ (_ tptp.ord_le976219883lle_hf tptp.zero_z189798548lle_hf) @t14))) % 0.41/0.80 (assume @p289 (forall @t109 (=> @t154 (not (=> @t306 (not (_ (_ tptp.ord_le976219883lle_hf @t62) @t36))))))) % 0.41/0.80 (assume @p290 (forall @t35 (_ (_ tptp.ord_le976219883lle_hf @t250) @t251))) % 0.41/0.80 (assume @p291 (forall @t182 (_ (_ tptp.ord_less_eq_nat @t246) @t247))) % 0.41/0.80 (assume @p292 (forall @t35 (_ (_ tptp.ord_le976219883lle_hf @t242) @t241))) % 0.41/0.80 (assume @p293 (forall @t182 (_ (_ tptp.ord_less_eq_nat @t234) @t233))) % 0.41/0.80 (assume @p294 (forall (@list @t31 @t14 @t33) (= (_ @t385 @t272) (or (_ @t385 @t33) (exists @t95 (and (= (_ @t32 @t90) @t31) (not (_ @t55 @t90)) (_ (_ tptp.ord_le976219883lle_hf @t90) @t33))))))) % 0.41/0.80 (assume @p295 (forall @t15 (_ @t283 @t14))) % 0.41/0.80 (assume @p296 (forall @t17 (_ @t287 @t16))) % 0.41/0.80 (assume @p297 (_ @t304 tptp.zero_zero_nat)) % 0.41/0.80 (assume @p298 (forall @t150 (= (_ tptp.hF_Mirabelle_HF (_ tptp.hF_Mirabelle_hfset @t5)) @t5))) % 0.41/0.80 (assume @p299 (forall @t258 (= (_ @t401 tptp.zero_zero_nat) @t399))) % 0.41/0.80 (assume @p300 (forall @t265 (= (= @t400 @t402) @t261))) % 0.41/0.80 (assume @p301 (= (_ tptp.semiri1382578993at_nat tptp.zero_zero_nat) tptp.zero_zero_nat)) % 0.41/0.80 (assume @p302 (forall @t260 (= (= tptp.zero_zero_nat @t402) (= tptp.zero_zero_nat @t259)))) % 0.41/0.80 (assume @p303 (forall @t258 (= (= @t400 tptp.zero_zero_nat) @t399))) % 0.41/0.80 (assume @p304 (forall @t265 (= (_ @t401 @t402) @t273))) % 0.41/0.80 (assume @p305 (forall @t260 (_ @t304 @t402))) % 0.41/0.80 (assume @p306 (forall (@list @t267 @t266) (=> @t324 (_ (_ tptp.ord_less_eq_nat (_ tptp.semiri1382578993at_nat @t267)) (_ tptp.semiri1382578993at_nat @t266))))) % 0.41/0.80 (assume @p307 (forall (@list @t259 @t256) (=> @t323 (= (_ tptp.semiri1382578993at_nat @t263) (_ (_ tptp.minus_minus_nat @t400) @t402))))) % 0.41/0.80 (assume @p308 (forall @t335 (=> @t294 (=> @t277 @t26)))) % 0.41/0.80 (assume @p309 (forall @t336 (=> @t300 (=> @t281 (= @t75 @t111))))) % 0.41/0.80 (assume @p310 (= @t136 (lambda @t25 (and (_ (_ tptp.ord_le976219883lle_hf @t19) @t21) (_ (_ tptp.ord_le976219883lle_hf @t21) @t19))))) % 0.41/0.80 (assume @p311 (= (lambda (@list @t404 @t403) (= @t404 @t403)) (lambda @t212 (and (_ (_ tptp.ord_less_eq_nat @t211) @t210) (_ (_ tptp.ord_less_eq_nat @t210) @t211))))) % 0.41/0.80 (assume @p312 @t407) % 0.41/0.80 (assume @p313 true) % 0.41/0.80 (step @p314 (= tptp.hF_Mirabelle_hpair @t408) :rule refl :args (@t408)) % 0.41/0.80 (step @p315 (= tptp.hF_Mirabelle_hmem @t409) :rule refl :args (@t409)) % 0.41/0.80 (step @p316 (= tptp.ord_le976219883lle_hf @t410) :rule refl :args (@t410)) % 0.41/0.80 (step @p317 (= tptp.ord_less_eq_nat @t411) :rule refl :args (@t411)) % 0.41/0.80 (step @p318 :rule eq-symm :args (@t412 @t413)) % 0.41/0.80 (step @p319 :rule cong :premises (@p318) :args (@t414)) % 0.41/0.80 (step @p320 :rule cong :premises (@p319) :args ((forall @t39 @t414))) % 0.41/0.80 (step @p321 :rule refl :args (@t413)) % 0.41/0.80 (step @p322 :rule refl :args (@t412)) % 0.41/0.80 (step @p323 :rule refl :args (@t53)) % 0.41/0.80 (step @p324 :rule cong :premises (@p323 @p322) :args ((= @t53 @t412))) % 0.41/0.80 (step @p325 :rule symm :premises (@p324)) % 0.41/0.80 (step @p326 :rule eq_resolve :premises (@p323 @p325)) % 0.41/0.80 (step @p327 :rule cong :premises (@p326 @p321) :args (@t415)) % 0.41/0.80 (step @p328 :rule cong :premises (@p327) :args (@t416)) % 0.41/0.80 (step @p329 :rule cong :premises (@p328) :args ((forall @t39 @t416))) % 0.41/0.80 (step @p330 :rule trans :premises (@p329 @p320)) % 0.41/0.80 (step @p331 :rule refl :args (@t413)) % 0.41/0.80 (step @p332 :rule symm :premises (@p22)) % 0.41/0.80 (step @p333 :rule cong :premises (@p332 @p331) :args (@t417)) % 0.41/0.80 (step @p334 :rule cong :premises (@p333) :args (@t418)) % 0.41/0.80 (step @p335 :rule cong :premises (@p334) :args ((forall @t39 @t418))) % 0.41/0.80 (step @p336 :rule trans :premises (@p335 @p330)) % 0.41/0.80 (step @p337 :rule refl :args (@t413)) % 0.41/0.80 (step @p338 :rule refl :args (@t37)) % 0.41/0.80 (step @p339 :rule cong :premises (@p338 @p337) :args ((= @t37 @t413))) % 0.41/0.80 (step @p340 :rule symm :premises (@p339)) % 0.41/0.80 (step @p341 :rule eq_resolve :premises (@p338 @p340)) % 0.41/0.80 (step @p342 :rule refl :args (tptp.zero_z189798548lle_hf)) % 0.41/0.80 (step @p343 :rule cong :premises (@p342 @p341) :args (@t419)) % 0.41/0.80 (step @p344 :rule cong :premises (@p343) :args (@t420)) % 0.41/0.80 (step @p345 :rule cong :premises (@p344) :args ((forall @t39 @t420))) % 0.41/0.80 (step @p346 :rule eq-symm :args (@t37 tptp.zero_z189798548lle_hf)) % 0.41/0.80 (step @p347 :rule cong :premises (@p346) :args (@t38)) % 0.41/0.80 (step @p348 :rule cong :premises (@p347) :args (@t40)) % 0.41/0.80 (step @p349 :rule trans :premises (@p348 @p345)) % 0.41/0.80 (step @p350 :rule trans :premises (@p349 @p336)) % 0.41/0.80 (step @p351 :rule eq_resolve :premises (@p18 @p350)) % 0.41/0.80 (step @p352 :rule refl :args ((tptp.hF_Mirabelle_hinsert @t426 @t425))) % 0.41/0.80 (step @p353 :rule refl :args ((tptp.hF_Mirabelle_hinsert @t424 @t53))) % 0.41/0.80 (step @p354 :rule refl :args ((tptp.hF_Mirabelle_hinsert tptp.x @t422))) % 0.41/0.80 (step @p355 :rule refl :args ((tptp.hF_Mirabelle_hinsert tptp.y @t53))) % 0.41/0.80 (step @p356 :rule refl :args (tptp.y)) % 0.41/0.80 (step @p357 :rule cong :premises (@p356 @p322) :args (@t427)) % 0.41/0.80 (step @p358 :rule trans :premises (@p357 @p355)) % 0.41/0.80 (step @p359 :rule refl :args (tptp.x)) % 0.41/0.80 (step @p360 :rule cong :premises (@p359 @p358) :args (@t428)) % 0.41/0.80 (step @p361 :rule trans :premises (@p360 @p354)) % 0.41/0.80 (step @p362 :rule cong :premises (@p361 @p322) :args (@t429)) % 0.41/0.80 (step @p363 :rule trans :premises (@p362 @p353)) % 0.41/0.80 (step @p364 :rule refl :args ((tptp.hF_Mirabelle_hinsert tptp.x @t53))) % 0.41/0.80 (step @p365 :rule cong :premises (@p359 @p322) :args (@t430)) % 0.41/0.80 (step @p366 :rule trans :premises (@p365 @p364)) % 0.41/0.80 (step @p367 :rule cong :premises (@p366 @p363) :args (@t431)) % 0.41/0.80 (step @p368 :rule trans :premises (@p367 @p352)) % 0.41/0.80 (step @p369 :rule refl :args (tptp.hF_Mirabelle_hinsert)) % 0.41/0.80 (step @p370 :rule ho_cong :premises (@p369 @p366)) % 0.41/0.80 (step @p371 :rule ho_cong :premises (@p370 @p363)) % 0.41/0.80 (step @p372 :rule cong :premises (@p371 @p368) :args ((= (_ (_ tptp.hF_Mirabelle_hinsert @t430) @t429) @t431))) % 0.41/0.80 (step @p373 :rule symm :premises (@p372)) % 0.41/0.80 (step @p374 :rule refl :args (@t432)) % 0.41/0.80 (step @p375 :rule eq_resolve :premises (@p374 @p373)) % 0.41/0.80 (step @p376 :rule ho_cong :premises (@p369 @p361)) % 0.41/0.80 (step @p377 :rule ho_cong :premises (@p376 @p322)) % 0.41/0.80 (step @p378 :rule cong :premises (@p377 @p363) :args ((= (_ (_ tptp.hF_Mirabelle_hinsert @t428) @t412) @t429))) % 0.41/0.80 (step @p379 :rule symm :premises (@p378)) % 0.41/0.80 (step @p380 :rule refl :args (@t425)) % 0.41/0.80 (step @p381 :rule eq_resolve :premises (@p380 @p379)) % 0.41/0.80 (step @p382 :rule refl :args (@t423)) % 0.41/0.80 (step @p383 :rule ho_cong :premises (@p382 @p358)) % 0.41/0.80 (step @p384 :rule cong :premises (@p383 @p361) :args ((= (_ @t423 @t427) @t428))) % 0.41/0.80 (step @p385 :rule symm :premises (@p384)) % 0.41/0.80 (step @p386 :rule refl :args (@t424)) % 0.41/0.80 (step @p387 :rule eq_resolve :premises (@p386 @p385)) % 0.41/0.80 (step @p388 :rule refl :args (@t421)) % 0.41/0.80 (step @p389 :rule ho_cong :premises (@p388 @p322)) % 0.41/0.80 (step @p390 :rule cong :premises (@p389 @p358) :args ((= (_ @t421 @t412) @t427))) % 0.41/0.80 (step @p391 :rule symm :premises (@p390)) % 0.41/0.80 (step @p392 :rule refl :args (@t422)) % 0.41/0.80 (step @p393 :rule eq_resolve :premises (@p392 @p391)) % 0.41/0.80 (step @p394 :rule refl :args (@t421)) % 0.41/0.80 (step @p395 :rule ho_cong :premises (@p394 @p326)) % 0.41/0.80 (step @p396 :rule trans :premises (@p395 @p393)) % 0.41/0.80 (step @p397 :rule refl :args (@t423)) % 0.41/0.80 (step @p398 :rule ho_cong :premises (@p397 @p396)) % 0.41/0.80 (step @p399 :rule trans :premises (@p398 @p387)) % 0.41/0.80 (step @p400 :rule refl :args (tptp.hF_Mirabelle_hinsert)) % 0.41/0.80 (step @p401 :rule ho_cong :premises (@p400 @p399)) % 0.41/0.80 (step @p402 :rule ho_cong :premises (@p401 @p326)) % 0.41/0.80 (step @p403 :rule trans :premises (@p402 @p381)) % 0.41/0.80 (step @p404 :rule ho_cong :premises (@p382 @p322)) % 0.41/0.80 (step @p405 :rule cong :premises (@p404 @p366) :args ((= (_ @t423 @t412) @t430))) % 0.41/0.80 (step @p406 :rule symm :premises (@p405)) % 0.41/0.80 (step @p407 :rule refl :args (@t426)) % 0.41/0.80 (step @p408 :rule eq_resolve :premises (@p407 @p406)) % 0.41/0.80 (step @p409 :rule ho_cong :premises (@p397 @p326)) % 0.41/0.80 (step @p410 :rule trans :premises (@p409 @p408)) % 0.41/0.80 (step @p411 :rule ho_cong :premises (@p400 @p410)) % 0.41/0.80 (step @p412 :rule ho_cong :premises (@p411 @p403)) % 0.41/0.80 (step @p413 :rule trans :premises (@p412 @p375)) % 0.41/0.80 (step @p414 :rule cong :premises (@p326 @p413) :args ((= @t53 @t432))) % 0.41/0.80 (step @p415 :rule ho_cong :premises (@p394 @p332)) % 0.41/0.80 (step @p416 :rule ho_cong :premises (@p397 @p415)) % 0.41/0.80 (step @p417 :rule ho_cong :premises (@p400 @p416)) % 0.41/0.80 (step @p418 :rule ho_cong :premises (@p417 @p332)) % 0.41/0.80 (step @p419 :rule ho_cong :premises (@p397 @p332)) % 0.41/0.80 (step @p420 :rule ho_cong :premises (@p400 @p419)) % 0.41/0.80 (step @p421 :rule ho_cong :premises (@p420 @p418)) % 0.41/0.80 (step @p422 :rule cong :premises (@p332 @p421) :args ((= tptp.zero_z189798548lle_hf @t434))) % 0.41/0.80 (step @p423 :rule eq-symm :args (@t434 tptp.zero_z189798548lle_hf)) % 0.41/0.80 (step @p424 :rule refl :args (tptp.zero_z189798548lle_hf)) % 0.41/0.80 (step @p425 :rule beta-reduce :args ((= (_ @t435 tptp.y) @t434))) % 0.41/0.80 (step @p426 :rule refl :args (tptp.y)) % 0.41/0.80 (step @p427 :rule beta-reduce :args ((= @t436 @t435))) % 0.41/0.80 (step @p428 :rule ho_cong :premises (@p427 @p426)) % 0.41/0.80 (step @p429 :rule trans :premises (@p428 @p425)) % 0.41/0.80 (step @p430 :rule cong :premises (@p429 @p424) :args (@t437)) % 0.41/0.80 (step @p431 :rule trans :premises (@p430 @p423)) % 0.41/0.80 (step @p432 :rule bool-double-not-elim :args (@t437)) % 0.41/0.80 (step @p433 :rule trans :premises (@p432 @p431)) % 0.41/0.80 (step @p434 :rule refl :args (tptp.x)) % 0.41/0.80 (step @p435 :rule ho_cong :premises (@p314 @p434)) % 0.41/0.80 (step @p436 :rule ho_cong :premises (@p435 @p426)) % 0.41/0.80 (step @p437 :rule cong :premises (@p436 @p424) :args (@t405)) % 0.41/0.80 (step @p438 :rule cong :premises (@p437) :args (@t406)) % 0.41/0.80 (step @p439 :rule cong :premises (@p438) :args (@t407)) % 0.41/0.80 (step @p440 :rule trans :premises (@p439 @p433)) % 0.41/0.80 (step @p441 :rule trans :premises (@p440 @p422 @p414)) % 0.41/0.80 (step @p442 :rule eq_resolve :premises (@p312 @p441)) % 0.41/0.80 (step @p443 :rule eq-symm :args (@t431 @t412)) % 0.41/0.80 (step @p444 :rule cong :premises (@p443) :args (@t438)) % 0.41/0.80 (step @p445 :rule refl :args (@t439)) % 0.41/0.80 (step @p446 :rule cong :premises (@p445 @p444) :args ((=> @t439 @t438))) % 0.41/0.80 (assume-push @p454 @t439) % 0.41/0.80 (step @p448 :rule instantiate :premises (@p351) :args ((@list @t430 @t429))) % 0.41/0.80 (step-pop @p455 :rule scope :premises (@p448)) % 0.41/0.80 (step @p449 :rule process_scope :premises (@p455) :args (@t438)) % 0.41/0.80 (step @p451 :rule eq_resolve :premises (@p449 @p446)) % 0.41/0.80 (step @p452 :rule implies_elim :premises (@p451)) % 0.41/0.80 (step @p453 false :rule chain_m_resolution :premises (@p452 @p442 @p351) :args (false (@list false false) (@list (= @t412 @t431) @t439))) % 0.41/0.80 ) % 0.41/0.80 % SZS output end Proof % 0.41/0.80 % cvc5 exiting %------------------------------------------------------------------------------