%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP072^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 : n028.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 3.11s 3.38s % Output : Proof 3.11s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP072^1 : TPTP v9.2.1. Released v7.5.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.17/0.34 % Computer : n028.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:35 EDT 2026 % 0.17/0.34 % CPUTime : % 0.31/0.56 %----Proving TH0 % 3.11/3.38 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 90s... % 3.11/3.38 % SZS status Theorem % 3.11/3.38 % SZS output start Proof % 3.11/3.38 ( % 3.11/3.38 (declare-sort tptp.set_HF_Mirabelle_hf 0) % 3.11/3.38 (declare-sort tptp.set_se933006839lle_hf 0) % 3.11/3.38 (declare-sort tptp.nat 0) % 3.11/3.38 (declare-sort tptp.set_nat 0) % 3.11/3.38 (declare-sort tptp.hF_Mirabelle_hf 0) % 3.11/3.38 (declare-const tptp.hF_Mirabelle_hfset (-> tptp.hF_Mirabelle_hf tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (declare-const tptp.member1367349282lle_hf (-> tptp.hF_Mirabelle_hf tptp.set_HF_Mirabelle_hf Bool)) % 3.11/3.38 (declare-const tptp.bot_bot_o Bool) % 3.11/3.38 (declare-const tptp.insert9649339lle_hf (-> tptp.hF_Mirabelle_hf tptp.set_HF_Mirabelle_hf tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (declare-const tptp.hF_Mirabelle_HF (-> tptp.set_HF_Mirabelle_hf tptp.hF_Mirabelle_hf)) % 3.11/3.38 (declare-const tptp.bot_bo53200981lle_hf tptp.set_HF_Mirabelle_hf) % 3.11/3.38 (declare-const tptp.the_el1104322134lle_hf (-> tptp.set_HF_Mirabelle_hf tptp.hF_Mirabelle_hf)) % 3.11/3.38 (declare-const tptp.member1490636632lle_hf (-> tptp.set_HF_Mirabelle_hf tptp.set_se933006839lle_hf Bool)) % 3.11/3.38 (declare-const tptp.ord_less_eq_nat (-> tptp.nat tptp.nat Bool)) % 3.11/3.38 (declare-const tptp.member_nat (-> tptp.nat tptp.set_nat Bool)) % 3.11/3.38 (declare-const tptp.z tptp.hF_Mirabelle_hf) % 3.11/3.38 (declare-const tptp.image_1514960916lle_hf (-> (-> tptp.set_HF_Mirabelle_hf tptp.set_HF_Mirabelle_hf) tptp.set_se933006839lle_hf tptp.set_se933006839lle_hf)) % 3.11/3.38 (declare-const tptp.minus_500612048lle_hf (-> tptp.set_se933006839lle_hf tptp.set_se933006839lle_hf tptp.set_se933006839lle_hf)) % 3.11/3.38 (declare-const tptp.minus_minus_nat (-> tptp.nat tptp.nat tptp.nat)) % 3.11/3.38 (declare-const tptp.image_nat_nat (-> (-> tptp.nat tptp.nat) tptp.set_nat tptp.set_nat)) % 3.11/3.38 (declare-const tptp.inj_on_nat_nat (-> (-> tptp.nat tptp.nat) tptp.set_nat Bool)) % 3.11/3.38 (declare-const tptp.image_246164834lle_hf (-> (-> tptp.nat tptp.hF_Mirabelle_hf) tptp.set_nat tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (declare-const tptp.inj_on1988990670lle_hf (-> (-> tptp.nat tptp.hF_Mirabelle_hf) tptp.set_nat Bool)) % 3.11/3.38 (declare-const tptp.image_131453538hf_nat (-> (-> tptp.hF_Mirabelle_hf tptp.nat) tptp.set_HF_Mirabelle_hf tptp.set_nat)) % 3.11/3.38 (declare-const tptp.inj_on1874279374hf_nat (-> (-> tptp.hF_Mirabelle_hf tptp.nat) tptp.set_HF_Mirabelle_hf Bool)) % 3.11/3.38 (declare-const tptp.image_1743964010lle_hf (-> (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf) tptp.set_HF_Mirabelle_hf tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (declare-const tptp.finite90088345lle_hf (-> tptp.set_se933006839lle_hf tptp.nat)) % 3.11/3.38 (declare-const tptp.minus_1450406810lle_hf (-> tptp.set_HF_Mirabelle_hf tptp.set_HF_Mirabelle_hf tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (declare-const tptp.minus_minus_set_nat (-> tptp.set_nat tptp.set_nat tptp.set_nat)) % 3.11/3.38 (declare-const tptp.lattic710307446hf_nat (-> (-> tptp.hF_Mirabelle_hf tptp.nat) tptp.set_HF_Mirabelle_hf tptp.hF_Mirabelle_hf)) % 3.11/3.38 (declare-const tptp.lattic1974000059at_nat (-> (-> tptp.nat tptp.nat) tptp.set_nat tptp.nat)) % 3.11/3.38 (declare-const tptp.inj_on755450110lle_hf (-> (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf) tptp.set_HF_Mirabelle_hf Bool)) % 3.11/3.38 (declare-const tptp.collect_nat (-> (-> tptp.nat Bool) tptp.set_nat)) % 3.11/3.38 (declare-const tptp.collec2046588256lle_hf (-> (-> tptp.hF_Mirabelle_hf Bool) tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (declare-const tptp.bot_bot_set_nat tptp.set_nat) % 3.11/3.38 (declare-const tptp.bot_bo2093393035lle_hf tptp.set_se933006839lle_hf) % 3.11/3.38 (declare-const tptp.finite1213132899lle_hf (-> tptp.set_HF_Mirabelle_hf tptp.nat)) % 3.11/3.38 (declare-const tptp.semiri2013084963it_nat (-> tptp.nat tptp.nat tptp.nat)) % 3.11/3.38 (declare-const tptp.finite1450550360lle_hf (-> tptp.set_se933006839lle_hf Bool)) % 3.11/3.38 (declare-const tptp.hF_Mirabelle_Abs_hf (-> tptp.nat tptp.hF_Mirabelle_hf)) % 3.11/3.38 (declare-const tptp.ord_le2016357975lle_hf (-> tptp.set_se933006839lle_hf tptp.set_se933006839lle_hf Bool)) % 3.11/3.38 (declare-const tptp.collec1758573718lle_hf (-> (-> tptp.set_HF_Mirabelle_hf Bool) tptp.set_se933006839lle_hf)) % 3.11/3.38 (declare-const tptp.semiring_1_Nats_nat tptp.set_nat) % 3.11/3.38 (declare-const tptp.zero_zero_nat tptp.nat) % 3.11/3.38 (declare-const tptp.finite586181922lle_hf (-> tptp.set_HF_Mirabelle_hf Bool)) % 3.11/3.38 (declare-const tptp.ord_less_eq_set_nat (-> tptp.set_nat tptp.set_nat Bool)) % 3.11/3.38 (declare-const tptp.semiri2115134414it_nat (-> tptp.nat tptp.nat tptp.nat)) % 3.11/3.38 (declare-const tptp.insert1636143089lle_hf (-> tptp.set_HF_Mirabelle_hf tptp.set_se933006839lle_hf tptp.set_se933006839lle_hf)) % 3.11/3.38 (declare-const tptp.zero_z189798548lle_hf tptp.hF_Mirabelle_hf) % 3.11/3.38 (declare-const tptp.insert_nat (-> tptp.nat tptp.set_nat tptp.set_nat)) % 3.11/3.38 (declare-const tptp.bot_bot_nat_o (-> tptp.nat Bool)) % 3.11/3.38 (declare-const tptp.bot_bot_nat tptp.nat) % 3.11/3.38 (declare-const tptp.finite_card_nat (-> tptp.set_nat tptp.nat)) % 3.11/3.38 (declare-const tptp.image_899003828lle_hf (-> (-> tptp.set_HF_Mirabelle_hf tptp.hF_Mirabelle_hf) tptp.set_se933006839lle_hf tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define tptp.hF_Mirabelle_hmem () (let ((_let_1 (@var "B" tptp.hF_Mirabelle_hf))) (let ((_let_2 (@var "A" tptp.hF_Mirabelle_hf))) (lambda (@list _let_2 _let_1) (_ (_ tptp.member1367349282lle_hf _let_2) (_ tptp.hF_Mirabelle_hfset _let_1)))))) % 3.11/3.38 (define tptp.bot_bo1263054448e_hf_o () (lambda (@list (@var "X" tptp.hF_Mirabelle_hf)) tptp.bot_bot_o)) % 3.11/3.38 (define tptp.bot_bo554042810e_hf_o () (lambda (@list (@var "X" tptp.set_HF_Mirabelle_hf)) tptp.bot_bot_o)) % 3.11/3.38 (define tptp.hF_Mirabelle_hinsert () (let ((_let_1 (@var "B" tptp.hF_Mirabelle_hf))) (let ((_let_2 (@var "A" tptp.hF_Mirabelle_hf))) (lambda (@list _let_2 _let_1) (_ tptp.hF_Mirabelle_HF (_ (_ tptp.insert9649339lle_hf _let_2) (_ tptp.hF_Mirabelle_hfset _let_1))))))) % 3.11/3.38 (define tptp.is_sin1448700567lle_hf () (let ((_let_1 (@var "A6" tptp.set_HF_Mirabelle_hf))) (lambda (@list _let_1) (= _let_1 (_ (_ tptp.insert9649339lle_hf (_ tptp.the_el1104322134lle_hf _let_1)) tptp.bot_bo53200981lle_hf))))) % 3.11/3.38 (define tptp.is_emp566801209lle_hf () (let ((_let_1 (@var "A6" tptp.set_HF_Mirabelle_hf))) (lambda (@list _let_1) (= _let_1 tptp.bot_bo53200981lle_hf)))) % 3.11/3.38 (define tptp.ord_le432112161lle_hf () (let ((_let_1 (@var "B6" tptp.set_HF_Mirabelle_hf))) (let ((_let_2 (@var "T" tptp.hF_Mirabelle_hf))) (let ((_let_3 (_ tptp.member1367349282lle_hf _let_2))) (let ((_let_4 (@var "A6" tptp.set_HF_Mirabelle_hf))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1))))))))) % 3.11/3.38 (define tptp.inj_on811196232lle_hf () (let ((_let_1 (@var "Y4" tptp.set_HF_Mirabelle_hf))) (let ((_let_2 (@var "X" tptp.set_HF_Mirabelle_hf))) (let ((_let_3 (@var "F4" (-> tptp.set_HF_Mirabelle_hf tptp.hF_Mirabelle_hf)))) (let ((_let_4 (@var "A6" tptp.set_se933006839lle_hf))) (lambda (@list _let_3 _let_4) (forall (@list _let_2) (=> (_ (_ tptp.member1490636632lle_hf _let_2) _let_4) (forall (@list _let_1) (=> (_ (_ tptp.member1490636632lle_hf _let_1) _let_4) (=> (= (_ _let_3 _let_2) (_ _let_3 _let_1)) (= _let_2 _let_1)))))))))))) % 3.11/3.38 (define tptp.finite_finite_nat () (let ((_let_1 (@var "M4" tptp.nat))) (let ((_let_2 (@var "X" tptp.nat))) (let ((_let_3 (@var "N2" tptp.set_nat))) (lambda (@list _let_3) (exists (@list _let_1) (forall (@list _let_2) (=> (_ (_ tptp.member_nat _let_2) _let_3) (_ (_ tptp.ord_less_eq_nat _let_2) _let_1))))))))) % 3.11/3.38 (define @t1 () (@var "B" tptp.hF_Mirabelle_hf)) % 3.11/3.38 (define @t2 () (@var "X" tptp.hF_Mirabelle_hf)) % 3.11/3.38 (define @t3 () (_ tptp.hF_Mirabelle_hmem @t2)) % 3.11/3.38 (define @t4 () (@var "A" tptp.hF_Mirabelle_hf)) % 3.11/3.38 (define @t5 () (@list @t2)) % 3.11/3.38 (define @t6 () (@list @t4 @t1)) % 3.11/3.38 (define @t7 () (@var "Z" tptp.hF_Mirabelle_hf)) % 3.11/3.38 (define @t8 () (@var "Y" tptp.hF_Mirabelle_hf)) % 3.11/3.38 (define @t9 () (@var "A2" tptp.hF_Mirabelle_hf)) % 3.11/3.38 (define @t10 () (_ tptp.hF_Mirabelle_hmem @t9)) % 3.11/3.38 (define @t11 () (not (_ @t10 tptp.zero_z189798548lle_hf))) % 3.11/3.38 (define @t12 () (@list @t9)) % 3.11/3.38 (define @t13 () (forall @t12 @t11)) % 3.11/3.38 (define @t14 () (@var "B2" tptp.hF_Mirabelle_hf)) % 3.11/3.38 (define @t15 () (@var "A3" tptp.hF_Mirabelle_hf)) % 3.11/3.38 (define @t16 () (@var "Y2" tptp.hF_Mirabelle_hf)) % 3.11/3.38 (define @t17 () (@var "C" tptp.hF_Mirabelle_hf)) % 3.11/3.38 (define @t18 () (@var "B3" tptp.hF_Mirabelle_hf)) % 3.11/3.38 (define @t19 () (= @t9 @t18)) % 3.11/3.38 (define @t20 () (@var "X2" tptp.hF_Mirabelle_hf)) % 3.11/3.38 (define @t21 () (@list @t20)) % 3.11/3.38 (define @t22 () (@var "X2" tptp.nat)) % 3.11/3.38 (define @t23 () (@list @t22)) % 3.11/3.38 (define @t24 () (= tptp.zero_z189798548lle_hf (_ tptp.hF_Mirabelle_HF tptp.bot_bo53200981lle_hf))) % 3.11/3.38 (define @t25 () (@var "N" tptp.nat)) % 3.11/3.38 (define @t26 () (_ tptp.semiri2013084963it_nat @t25)) % 3.11/3.38 (define @t27 () (@list @t25)) % 3.11/3.38 (define @t28 () (@var "A2" tptp.nat)) % 3.11/3.38 (define @t29 () (= @t28 tptp.zero_zero_nat)) % 3.11/3.38 (define @t30 () (_ tptp.hF_Mirabelle_hfset @t9)) % 3.11/3.38 (define @t31 () (_ tptp.hF_Mirabelle_HF @t30)) % 3.11/3.38 (define @t32 () (forall @t12 (= @t31 @t9))) % 3.11/3.38 (define @t33 () (@var "C" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t34 () (@var "C" tptp.nat)) % 3.11/3.38 (define @t35 () (_ tptp.member1367349282lle_hf @t17)) % 3.11/3.38 (define @t36 () (@var "A4" tptp.set_se933006839lle_hf)) % 3.11/3.38 (define @t37 () (= @t36 tptp.bot_bo2093393035lle_hf)) % 3.11/3.38 (define @t38 () (@var "X" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t39 () (_ tptp.member1490636632lle_hf @t38)) % 3.11/3.38 (define @t40 () (_ @t39 @t36)) % 3.11/3.38 (define @t41 () (@list @t38)) % 3.11/3.38 (define @t42 () (@list @t36)) % 3.11/3.38 (define @t43 () (@var "A4" tptp.set_nat)) % 3.11/3.38 (define @t44 () (= @t43 tptp.bot_bot_set_nat)) % 3.11/3.38 (define @t45 () (@var "X" tptp.nat)) % 3.11/3.38 (define @t46 () (_ tptp.member_nat @t45)) % 3.11/3.38 (define @t47 () (_ @t46 @t43)) % 3.11/3.38 (define @t48 () (@list @t45)) % 3.11/3.38 (define @t49 () (@list @t43)) % 3.11/3.38 (define @t50 () (@var "A4" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t51 () (= @t50 tptp.bot_bo53200981lle_hf)) % 3.11/3.38 (define @t52 () (_ tptp.member1367349282lle_hf @t2)) % 3.11/3.38 (define @t53 () (_ @t52 @t50)) % 3.11/3.38 (define @t54 () (@list @t50)) % 3.11/3.38 (define @t55 () (@var "P" (-> tptp.nat Bool))) % 3.11/3.38 (define @t56 () (forall @t48 (not (_ @t55 @t45)))) % 3.11/3.38 (define @t57 () (_ tptp.collect_nat @t55)) % 3.11/3.38 (define @t58 () (@list @t55)) % 3.11/3.38 (define @t59 () (@var "P" (-> tptp.set_HF_Mirabelle_hf Bool))) % 3.11/3.38 (define @t60 () (_ @t59 @t38)) % 3.11/3.38 (define @t61 () (forall @t41 (not @t60))) % 3.11/3.38 (define @t62 () (_ tptp.collec1758573718lle_hf @t59)) % 3.11/3.38 (define @t63 () (= @t62 tptp.bot_bo2093393035lle_hf)) % 3.11/3.38 (define @t64 () (@list @t59)) % 3.11/3.38 (define @t65 () (@var "P" (-> tptp.hF_Mirabelle_hf Bool))) % 3.11/3.38 (define @t66 () (forall @t5 (not (_ @t65 @t2)))) % 3.11/3.38 (define @t67 () (_ tptp.collec2046588256lle_hf @t65)) % 3.11/3.38 (define @t68 () (= @t67 tptp.bot_bo53200981lle_hf)) % 3.11/3.38 (define @t69 () (@list @t65)) % 3.11/3.38 (define @t70 () (_ tptp.finite586181922lle_hf @t50)) % 3.11/3.38 (define @t71 () (@var "A2" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t72 () (_ tptp.member1490636632lle_hf @t71)) % 3.11/3.38 (define @t73 () (@list @t71)) % 3.11/3.38 (define @t74 () (_ tptp.member_nat @t28)) % 3.11/3.38 (define @t75 () (@list @t28)) % 3.11/3.38 (define @t76 () (_ tptp.member1367349282lle_hf @t9)) % 3.11/3.38 (define @t77 () (_ @t72 @t36)) % 3.11/3.38 (define @t78 () (not @t77)) % 3.11/3.38 (define @t79 () (_ @t74 @t43)) % 3.11/3.38 (define @t80 () (not @t79)) % 3.11/3.38 (define @t81 () (@list @t43 @t28)) % 3.11/3.38 (define @t82 () (_ @t76 @t50)) % 3.11/3.38 (define @t83 () (not @t82)) % 3.11/3.38 (define @t84 () (@list @t50 @t9)) % 3.11/3.38 (define @t85 () (_ tptp.insert_nat @t22)) % 3.11/3.38 (define @t86 () (_ @t85 @t43)) % 3.11/3.38 (define @t87 () (@list @t22 @t43)) % 3.11/3.38 (define @t88 () (@var "X2" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t89 () (_ tptp.insert1636143089lle_hf @t88)) % 3.11/3.38 (define @t90 () (_ @t89 @t36)) % 3.11/3.38 (define @t91 () (@list @t88 @t36)) % 3.11/3.38 (define @t92 () (_ tptp.insert9649339lle_hf @t20)) % 3.11/3.38 (define @t93 () (_ @t92 @t50)) % 3.11/3.38 (define @t94 () (@list @t20 @t50)) % 3.11/3.38 (define @t95 () (@var "B3" tptp.nat)) % 3.11/3.38 (define @t96 () (= @t28 @t95)) % 3.11/3.38 (define @t97 () (_ tptp.insert_nat @t95)) % 3.11/3.38 (define @t98 () (_ @t74 (_ @t97 @t43))) % 3.11/3.38 (define @t99 () (@list @t28 @t95 @t43)) % 3.11/3.38 (define @t100 () (@var "B3" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t101 () (= @t71 @t100)) % 3.11/3.38 (define @t102 () (_ tptp.insert1636143089lle_hf @t100)) % 3.11/3.38 (define @t103 () (_ @t72 (_ @t102 @t36))) % 3.11/3.38 (define @t104 () (@list @t71 @t100 @t36)) % 3.11/3.38 (define @t105 () (_ tptp.insert9649339lle_hf @t18)) % 3.11/3.38 (define @t106 () (_ @t76 (_ @t105 @t50))) % 3.11/3.38 (define @t107 () (@list @t9 @t18 @t50)) % 3.11/3.38 (define @t108 () (@var "B4" tptp.set_nat)) % 3.11/3.38 (define @t109 () (_ @t97 @t108)) % 3.11/3.38 (define @t110 () (_ @t74 @t109)) % 3.11/3.38 (define @t111 () (_ @t74 @t108)) % 3.11/3.38 (define @t112 () (@list @t28 @t108 @t95)) % 3.11/3.38 (define @t113 () (@var "B4" tptp.set_se933006839lle_hf)) % 3.11/3.38 (define @t114 () (_ @t102 @t113)) % 3.11/3.38 (define @t115 () (_ @t72 @t114)) % 3.11/3.38 (define @t116 () (_ @t72 @t113)) % 3.11/3.38 (define @t117 () (@list @t71 @t113 @t100)) % 3.11/3.38 (define @t118 () (@var "B4" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t119 () (_ @t105 @t118)) % 3.11/3.38 (define @t120 () (_ @t76 @t119)) % 3.11/3.38 (define @t121 () (_ @t76 @t118)) % 3.11/3.38 (define @t122 () (not @t121)) % 3.11/3.38 (define @t123 () (=> @t122 @t19)) % 3.11/3.38 (define @t124 () (@list @t9 @t118 @t18)) % 3.11/3.38 (define @t125 () (forall @t124 (=> @t123 @t120))) % 3.11/3.38 (define @t126 () (_ tptp.insert1636143089lle_hf @t71)) % 3.11/3.38 (define @t127 () (_ @t126 tptp.bot_bo2093393035lle_hf)) % 3.11/3.38 (define @t128 () (_ tptp.insert_nat @t28)) % 3.11/3.38 (define @t129 () (_ @t128 tptp.bot_bot_set_nat)) % 3.11/3.38 (define @t130 () (_ tptp.insert9649339lle_hf @t9)) % 3.11/3.38 (define @t131 () (_ @t130 tptp.bot_bo53200981lle_hf)) % 3.11/3.38 (define @t132 () (@var "B5" tptp.set_nat)) % 3.11/3.38 (define @t133 () (@list @t132)) % 3.11/3.38 (define @t134 () (@list @t28 @t43)) % 3.11/3.38 (define @t135 () (@var "B5" tptp.set_se933006839lle_hf)) % 3.11/3.38 (define @t136 () (@list @t135)) % 3.11/3.38 (define @t137 () (@list @t71 @t36)) % 3.11/3.38 (define @t138 () (@var "B5" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t139 () (@list @t138)) % 3.11/3.38 (define @t140 () (@list @t9 @t50)) % 3.11/3.38 (define @t141 () (@var "Y2" tptp.nat)) % 3.11/3.38 (define @t142 () (_ tptp.insert_nat @t141)) % 3.11/3.38 (define @t143 () (@var "Y2" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t144 () (_ tptp.insert1636143089lle_hf @t143)) % 3.11/3.38 (define @t145 () (_ tptp.insert9649339lle_hf @t16)) % 3.11/3.38 (define @t146 () (@var "C2" tptp.set_nat)) % 3.11/3.38 (define @t147 () (_ tptp.member_nat @t95)) % 3.11/3.38 (define @t148 () (not @t96)) % 3.11/3.38 (define @t149 () (= @t43 @t108)) % 3.11/3.38 (define @t150 () (_ @t128 @t43)) % 3.11/3.38 (define @t151 () (@var "C2" tptp.set_se933006839lle_hf)) % 3.11/3.38 (define @t152 () (_ tptp.member1490636632lle_hf @t100)) % 3.11/3.38 (define @t153 () (not @t101)) % 3.11/3.38 (define @t154 () (= @t36 @t113)) % 3.11/3.38 (define @t155 () (_ @t126 @t36)) % 3.11/3.38 (define @t156 () (@var "C2" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t157 () (_ tptp.member1367349282lle_hf @t18)) % 3.11/3.38 (define @t158 () (not @t19)) % 3.11/3.38 (define @t159 () (= @t50 @t118)) % 3.11/3.38 (define @t160 () (_ @t130 @t50)) % 3.11/3.38 (define @t161 () (_ tptp.member_nat @t22)) % 3.11/3.38 (define @t162 () (_ @t161 @t43)) % 3.11/3.38 (define @t163 () (_ tptp.member1490636632lle_hf @t88)) % 3.11/3.38 (define @t164 () (_ @t163 @t36)) % 3.11/3.38 (define @t165 () (_ @t92 @t118)) % 3.11/3.38 (define @t166 () (_ tptp.member1367349282lle_hf @t20)) % 3.11/3.38 (define @t167 () (_ @t166 @t118)) % 3.11/3.38 (define @t168 () (not @t167)) % 3.11/3.38 (define @t169 () (_ @t166 @t50)) % 3.11/3.38 (define @t170 () (not @t169)) % 3.11/3.38 (define @t171 () (@list @t20 @t50 @t118)) % 3.11/3.38 (define @t172 () (_ @t128 @t108)) % 3.11/3.38 (define @t173 () (_ @t130 @t118)) % 3.11/3.38 (define @t174 () (@var "A5" tptp.set_se933006839lle_hf)) % 3.11/3.38 (define @t175 () (_ tptp.finite1450550360lle_hf @t174)) % 3.11/3.38 (define @t176 () (not @t175)) % 3.11/3.38 (define @t177 () (@var "X3" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t178 () (_ tptp.member1490636632lle_hf @t177)) % 3.11/3.38 (define @t179 () (_ tptp.insert1636143089lle_hf @t177)) % 3.11/3.38 (define @t180 () (@var "F" tptp.set_se933006839lle_hf)) % 3.11/3.38 (define @t181 () (not (= @t180 tptp.bot_bo2093393035lle_hf))) % 3.11/3.38 (define @t182 () (_ tptp.finite1450550360lle_hf @t180)) % 3.11/3.38 (define @t183 () (@var "A5" tptp.set_nat)) % 3.11/3.38 (define @t184 () (_ tptp.finite_finite_nat @t183)) % 3.11/3.38 (define @t185 () (not @t184)) % 3.11/3.38 (define @t186 () (@var "X3" tptp.nat)) % 3.11/3.38 (define @t187 () (_ tptp.member_nat @t186)) % 3.11/3.38 (define @t188 () (_ tptp.insert_nat @t186)) % 3.11/3.38 (define @t189 () (@var "F" tptp.set_nat)) % 3.11/3.38 (define @t190 () (not (= @t189 tptp.bot_bot_set_nat))) % 3.11/3.38 (define @t191 () (_ tptp.finite_finite_nat @t189)) % 3.11/3.38 (define @t192 () (@var "A5" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t193 () (_ tptp.finite586181922lle_hf @t192)) % 3.11/3.38 (define @t194 () (not @t193)) % 3.11/3.38 (define @t195 () (@var "X3" tptp.hF_Mirabelle_hf)) % 3.11/3.38 (define @t196 () (_ tptp.member1367349282lle_hf @t195)) % 3.11/3.38 (define @t197 () (_ @t196 @t192)) % 3.11/3.38 (define @t198 () (not @t197)) % 3.11/3.38 (define @t199 () (=> @t198 @t194)) % 3.11/3.38 (define @t200 () (_ tptp.insert9649339lle_hf @t195)) % 3.11/3.38 (define @t201 () (_ @t200 @t192)) % 3.11/3.38 (define @t202 () (@var "F" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t203 () (= @t202 @t201)) % 3.11/3.38 (define @t204 () (@list @t192 @t195)) % 3.11/3.38 (define @t205 () (forall @t204 (=> @t203 @t199))) % 3.11/3.38 (define @t206 () (not @t205)) % 3.11/3.38 (define @t207 () (not (= @t202 tptp.bot_bo53200981lle_hf))) % 3.11/3.38 (define @t208 () (=> @t207 @t206)) % 3.11/3.38 (define @t209 () (_ tptp.finite586181922lle_hf @t202)) % 3.11/3.38 (define @t210 () (=> @t209 @t208)) % 3.11/3.38 (define @t211 () (@list @t202)) % 3.11/3.38 (define @t212 () (forall @t211 @t210)) % 3.11/3.38 (define @t213 () (= tptp.bot_bo53200981lle_hf (_ tptp.collec2046588256lle_hf tptp.bot_bo1263054448e_hf_o))) % 3.11/3.38 (define @t214 () (_ @t102 tptp.bot_bo2093393035lle_hf)) % 3.11/3.38 (define @t215 () (_ @t97 tptp.bot_bot_set_nat)) % 3.11/3.38 (define @t216 () (@list @t28 @t95)) % 3.11/3.38 (define @t217 () (_ @t105 tptp.bot_bo53200981lle_hf)) % 3.11/3.38 (define @t218 () (@var "D" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t219 () (= @t95 @t34)) % 3.11/3.38 (define @t220 () (@var "D" tptp.nat)) % 3.11/3.38 (define @t221 () (@var "D" tptp.hF_Mirabelle_hf)) % 3.11/3.38 (define @t222 () (@var "Q" (-> tptp.hF_Mirabelle_hf Bool))) % 3.11/3.38 (define @t223 () (@list @t195)) % 3.11/3.38 (define @t224 () (@var "Q" (-> tptp.set_HF_Mirabelle_hf Bool))) % 3.11/3.38 (define @t225 () (_ tptp.collec1758573718lle_hf @t224)) % 3.11/3.38 (define @t226 () (_ @t224 @t177)) % 3.11/3.38 (define @t227 () (_ @t59 @t177)) % 3.11/3.38 (define @t228 () (@list @t177)) % 3.11/3.38 (define @t229 () (@list @t59 @t224)) % 3.11/3.38 (define @t230 () (= @t100 @t71)) % 3.11/3.38 (define @t231 () (_ @t152 @t127)) % 3.11/3.38 (define @t232 () (@list @t100 @t71)) % 3.11/3.38 (define @t233 () (= @t95 @t28)) % 3.11/3.38 (define @t234 () (_ @t147 @t129)) % 3.11/3.38 (define @t235 () (@list @t95 @t28)) % 3.11/3.38 (define @t236 () (= @t18 @t9)) % 3.11/3.38 (define @t237 () (_ @t157 @t131)) % 3.11/3.38 (define @t238 () (@list @t18 @t9)) % 3.11/3.38 (define @t239 () (_ tptp.finite586181922lle_hf @t30)) % 3.11/3.38 (define @t240 () (forall @t12 @t239)) % 3.11/3.38 (define @t241 () (not @t44)) % 3.11/3.38 (define @t242 () (not @t51)) % 3.11/3.38 (define @t243 () (@var "Y3" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t244 () (_ (_ tptp.member1490636632lle_hf @t243) @t36)) % 3.11/3.38 (define @t245 () (@var "Y3" tptp.nat)) % 3.11/3.38 (define @t246 () (@list @t245)) % 3.11/3.38 (define @t247 () (@var "Y3" tptp.hF_Mirabelle_hf)) % 3.11/3.38 (define @t248 () (_ (_ tptp.member1367349282lle_hf @t247) @t50)) % 3.11/3.38 (define @t249 () (_ tptp.finite1450550360lle_hf @t36)) % 3.11/3.38 (define @t250 () (_ tptp.finite586181922lle_hf @t160)) % 3.11/3.38 (define @t251 () (_ tptp.finite_finite_nat @t43)) % 3.11/3.38 (define @t252 () (_ tptp.finite_finite_nat @t150)) % 3.11/3.38 (define @t253 () (@var "A3" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t254 () (_ (_ tptp.insert1636143089lle_hf @t253) @t174)) % 3.11/3.38 (define @t255 () (@var "A2" tptp.set_se933006839lle_hf)) % 3.11/3.38 (define @t256 () (@list @t253)) % 3.11/3.38 (define @t257 () (@list @t174)) % 3.11/3.38 (define @t258 () (@var "A3" tptp.nat)) % 3.11/3.38 (define @t259 () (_ tptp.insert_nat @t258)) % 3.11/3.38 (define @t260 () (_ @t259 @t183)) % 3.11/3.38 (define @t261 () (@var "A2" tptp.set_nat)) % 3.11/3.38 (define @t262 () (@list @t183)) % 3.11/3.38 (define @t263 () (_ tptp.insert9649339lle_hf @t15)) % 3.11/3.38 (define @t264 () (_ @t263 @t192)) % 3.11/3.38 (define @t265 () (@list @t15)) % 3.11/3.38 (define @t266 () (@list @t192)) % 3.11/3.38 (define @t267 () (= @t71 tptp.bot_bo53200981lle_hf)) % 3.11/3.38 (define @t268 () (@var "A6" tptp.set_se933006839lle_hf)) % 3.11/3.38 (define @t269 () (@var "B" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t270 () (@var "A" tptp.set_se933006839lle_hf)) % 3.11/3.38 (define @t271 () (@var "A6" tptp.set_nat)) % 3.11/3.38 (define @t272 () (@var "B" tptp.nat)) % 3.11/3.38 (define @t273 () (@var "A" tptp.set_nat)) % 3.11/3.38 (define @t274 () (@var "A6" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t275 () (@var "A" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t276 () (@var "P" (-> tptp.set_se933006839lle_hf Bool))) % 3.11/3.38 (define @t277 () (_ @t276 @t180)) % 3.11/3.38 (define @t278 () (@var "F2" tptp.set_se933006839lle_hf)) % 3.11/3.38 (define @t279 () (=> (not (_ @t178 @t278)) (=> (_ @t276 @t278) (_ @t276 (_ @t179 @t278))))) % 3.11/3.38 (define @t280 () (_ tptp.finite1450550360lle_hf @t278)) % 3.11/3.38 (define @t281 () (@list @t177 @t278)) % 3.11/3.38 (define @t282 () (forall @t281 (=> @t280 @t279))) % 3.11/3.38 (define @t283 () (_ @t276 tptp.bot_bo2093393035lle_hf)) % 3.11/3.38 (define @t284 () (@list @t180 @t276)) % 3.11/3.38 (define @t285 () (@var "P" (-> tptp.set_nat Bool))) % 3.11/3.38 (define @t286 () (_ @t285 @t189)) % 3.11/3.38 (define @t287 () (@var "F2" tptp.set_nat)) % 3.11/3.38 (define @t288 () (_ @t285 @t287)) % 3.11/3.38 (define @t289 () (=> (not (_ @t187 @t287)) (=> @t288 (_ @t285 (_ @t188 @t287))))) % 3.11/3.38 (define @t290 () (_ tptp.finite_finite_nat @t287)) % 3.11/3.38 (define @t291 () (@list @t186 @t287)) % 3.11/3.38 (define @t292 () (forall @t291 (=> @t290 @t289))) % 3.11/3.38 (define @t293 () (_ @t285 tptp.bot_bot_set_nat)) % 3.11/3.38 (define @t294 () (@list @t189 @t285)) % 3.11/3.38 (define @t295 () (_ @t59 @t202)) % 3.11/3.38 (define @t296 () (@var "F2" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t297 () (_ @t59 @t296)) % 3.11/3.38 (define @t298 () (=> (not (_ @t196 @t296)) (=> @t297 (_ @t59 (_ @t200 @t296))))) % 3.11/3.38 (define @t299 () (_ tptp.finite586181922lle_hf @t296)) % 3.11/3.38 (define @t300 () (@list @t195 @t296)) % 3.11/3.38 (define @t301 () (forall @t300 (=> @t299 @t298))) % 3.11/3.38 (define @t302 () (_ @t59 tptp.bot_bo53200981lle_hf)) % 3.11/3.38 (define @t303 () (@list @t202 @t59)) % 3.11/3.38 (define @t304 () (@var "X2" tptp.set_se933006839lle_hf)) % 3.11/3.38 (define @t305 () (_ @t276 @t174)) % 3.11/3.38 (define @t306 () (@var "X2" tptp.set_nat)) % 3.11/3.38 (define @t307 () (_ @t285 @t183)) % 3.11/3.38 (define @t308 () (_ @t59 @t192)) % 3.11/3.38 (define @t309 () (@list @t186)) % 3.11/3.38 (define @t310 () (_ @t200 tptp.bot_bo53200981lle_hf)) % 3.11/3.38 (define @t311 () (_ @t92 tptp.bot_bo53200981lle_hf)) % 3.11/3.38 (define @t312 () (@var "S" tptp.set_nat)) % 3.11/3.38 (define @t313 () (not (= @t312 tptp.bot_bot_set_nat))) % 3.11/3.38 (define @t314 () (_ tptp.finite_finite_nat @t312)) % 3.11/3.38 (define @t315 () (not @t314)) % 3.11/3.38 (define @t316 () (@var "S" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t317 () (not (= @t316 tptp.bot_bo53200981lle_hf))) % 3.11/3.38 (define @t318 () (_ tptp.finite586181922lle_hf @t316)) % 3.11/3.38 (define @t319 () (not @t318)) % 3.11/3.38 (define @t320 () (@list @t274)) % 3.11/3.38 (define @t321 () (_ tptp.is_sin1448700567lle_hf @t50)) % 3.11/3.38 (define @t322 () (_ @t196 @t50)) % 3.11/3.38 (define @t323 () (_ tptp.finite_card_nat @t43)) % 3.11/3.38 (define @t324 () (= @t323 tptp.zero_zero_nat)) % 3.11/3.38 (define @t325 () (_ tptp.finite1213132899lle_hf @t50)) % 3.11/3.38 (define @t326 () (= @t325 tptp.zero_zero_nat)) % 3.11/3.38 (define @t327 () (_ tptp.member_nat @t258)) % 3.11/3.38 (define @t328 () (=> (not (_ @t327 @t287)) (=> @t288 (_ @t285 (_ @t259 @t287))))) % 3.11/3.38 (define @t329 () (_ @t327 @t43)) % 3.11/3.38 (define @t330 () (@list @t258 @t287)) % 3.11/3.38 (define @t331 () (_ (_ tptp.ord_less_eq_set_nat @t189) @t43)) % 3.11/3.38 (define @t332 () (@list @t189 @t43 @t285)) % 3.11/3.38 (define @t333 () (_ tptp.member1367349282lle_hf @t15)) % 3.11/3.38 (define @t334 () (=> (not (_ @t333 @t296)) (=> @t297 (_ @t59 (_ @t263 @t296))))) % 3.11/3.38 (define @t335 () (_ @t333 @t50)) % 3.11/3.38 (define @t336 () (@list @t15 @t296)) % 3.11/3.38 (define @t337 () (_ (_ tptp.ord_le432112161lle_hf @t202) @t50)) % 3.11/3.38 (define @t338 () (@list @t202 @t50 @t59)) % 3.11/3.38 (define @t339 () (_ tptp.ord_less_eq_nat @t22)) % 3.11/3.38 (define @t340 () (_ tptp.ord_le432112161lle_hf @t50)) % 3.11/3.38 (define @t341 () (_ @t340 @t118)) % 3.11/3.38 (define @t342 () (@list @t50 @t118)) % 3.11/3.38 (define @t343 () (_ tptp.ord_less_eq_nat @t25)) % 3.11/3.38 (define @t344 () (_ @t340 tptp.bot_bo53200981lle_hf)) % 3.11/3.38 (define @t345 () (_ tptp.ord_le432112161lle_hf tptp.bot_bo53200981lle_hf)) % 3.11/3.38 (define @t346 () (and @t19 (_ @t340 @t217))) % 3.11/3.38 (define @t347 () (_ tptp.finite1213132899lle_hf tptp.bot_bo53200981lle_hf)) % 3.11/3.38 (define @t348 () (not @t70)) % 3.11/3.38 (define @t349 () (not @t251)) % 3.11/3.38 (define @t350 () (_ tptp.ord_less_eq_nat @t28)) % 3.11/3.38 (define @t351 () (_ @t350 @t95)) % 3.11/3.38 (define @t352 () (_ tptp.ord_less_eq_nat @t95)) % 3.11/3.38 (define @t353 () (_ @t352 @t28)) % 3.11/3.38 (define @t354 () (@var "A" tptp.nat)) % 3.11/3.38 (define @t355 () (_ (_ tptp.ord_less_eq_nat @t354) @t272)) % 3.11/3.38 (define @t356 () (_ (_ tptp.ord_less_eq_nat @t272) @t354)) % 3.11/3.38 (define @t357 () (@list @t354 @t272)) % 3.11/3.38 (define @t358 () (@var "Z" tptp.nat)) % 3.11/3.38 (define @t359 () (@var "Y" tptp.nat)) % 3.11/3.38 (define @t360 () (lambda (@list @t359 @t358) (= @t359 @t358))) % 3.11/3.38 (define @t361 () (_ tptp.ord_less_eq_nat @t34)) % 3.11/3.38 (define @t362 () (@var "P" (-> tptp.nat tptp.nat Bool))) % 3.11/3.38 (define @t363 () (@var "B2" tptp.nat)) % 3.11/3.38 (define @t364 () (_ (_ @t362 @t258) @t363)) % 3.11/3.38 (define @t365 () (@list @t258 @t363)) % 3.11/3.38 (define @t366 () (@var "Z2" tptp.nat)) % 3.11/3.38 (define @t367 () (_ @t339 @t366)) % 3.11/3.38 (define @t368 () (_ tptp.ord_less_eq_nat @t141)) % 3.11/3.38 (define @t369 () (_ @t368 @t366)) % 3.11/3.38 (define @t370 () (_ @t339 @t141)) % 3.11/3.38 (define @t371 () (@list @t22 @t141 @t366)) % 3.11/3.38 (define @t372 () (_ @t350 @t34)) % 3.11/3.38 (define @t373 () (@list @t28 @t95 @t34)) % 3.11/3.38 (define @t374 () (_ @t352 @t34)) % 3.11/3.38 (define @t375 () (=> @t374 @t372)) % 3.11/3.38 (define @t376 () (= @t22 @t141)) % 3.11/3.38 (define @t377 () (_ @t368 @t22)) % 3.11/3.38 (define @t378 () (not @t370)) % 3.11/3.38 (define @t379 () (_ tptp.ord_less_eq_nat @t366)) % 3.11/3.38 (define @t380 () (_ @t379 @t22)) % 3.11/3.38 (define @t381 () (_ @t379 @t141)) % 3.11/3.38 (define @t382 () (@list @t22 @t141)) % 3.11/3.38 (define @t383 () (@var "Y4" tptp.nat)) % 3.11/3.38 (define @t384 () (_ tptp.ord_less_eq_nat @t45)) % 3.11/3.38 (define @t385 () (@var "F3" (-> tptp.nat tptp.nat))) % 3.11/3.38 (define @t386 () (_ @t385 @t186)) % 3.11/3.38 (define @t387 () (_ tptp.ord_less_eq_nat @t186)) % 3.11/3.38 (define @t388 () (forall (@list @t186 @t245) (=> (_ @t387 @t245) (_ (_ tptp.ord_less_eq_nat @t386) (_ @t385 @t245))))) % 3.11/3.38 (define @t389 () (=> @t388 (_ (_ tptp.ord_less_eq_nat (_ @t385 @t28)) @t34))) % 3.11/3.38 (define @t390 () (_ @t385 @t95)) % 3.11/3.38 (define @t391 () (@list @t28 @t95 @t385 @t34)) % 3.11/3.38 (define @t392 () (=> @t374 (=> @t388 (_ @t350 (_ @t385 @t34))))) % 3.11/3.38 (define @t393 () (@list @t28 @t385 @t95 @t34)) % 3.11/3.38 (define @t394 () (_ (_ tptp.ord_le2016357975lle_hf @t62) @t225)) % 3.11/3.38 (define @t395 () (@var "B6" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t396 () (@list @t274 @t395)) % 3.11/3.38 (define @t397 () (_ @t35 @t118)) % 3.11/3.38 (define @t398 () (_ @t35 @t50)) % 3.11/3.38 (define @t399 () (=> @t398 @t397)) % 3.11/3.38 (define @t400 () (_ tptp.finite1213132899lle_hf @t118)) % 3.11/3.38 (define @t401 () (_ tptp.finite586181922lle_hf @t118)) % 3.11/3.38 (define @t402 () (@list @t118 @t50)) % 3.11/3.38 (define @t403 () (_ tptp.finite_card_nat @t108)) % 3.11/3.38 (define @t404 () (_ (_ tptp.ord_less_eq_set_nat @t43) @t108)) % 3.11/3.38 (define @t405 () (_ tptp.finite_finite_nat @t108)) % 3.11/3.38 (define @t406 () (@list @t108 @t43)) % 3.11/3.38 (define @t407 () (_ tptp.ord_less_eq_nat tptp.zero_zero_nat)) % 3.11/3.38 (define @t408 () (_ (_ tptp.ord_le432112161lle_hf @t71) tptp.bot_bo53200981lle_hf)) % 3.11/3.38 (define @t409 () (= @t28 tptp.bot_bot_nat)) % 3.11/3.38 (define @t410 () (_ @t350 tptp.bot_bot_nat)) % 3.11/3.38 (define @t411 () (@var "Xa" tptp.nat)) % 3.11/3.38 (define @t412 () (= @t186 @t411)) % 3.11/3.38 (define @t413 () (_ (_ tptp.member_nat @t411) @t43)) % 3.11/3.38 (define @t414 () (@list @t411)) % 3.11/3.38 (define @t415 () (forall @t414 (=> @t413 (=> (_ @t387 @t411) @t412)))) % 3.11/3.38 (define @t416 () (_ @t187 @t43)) % 3.11/3.38 (define @t417 () (forall @t414 (=> @t413 (=> (_ (_ tptp.ord_less_eq_nat @t411) @t186) @t412)))) % 3.11/3.38 (define @t418 () (@list @t43 @t108)) % 3.11/3.38 (define @t419 () (@var "T2" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t420 () (@var "T2" tptp.set_nat)) % 3.11/3.38 (define @t421 () (@var "D2" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t422 () (@var "C3" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t423 () (_ tptp.ord_le432112161lle_hf @t118)) % 3.11/3.38 (define @t424 () (@var "X4" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t425 () (_ tptp.ord_le432112161lle_hf @t424)) % 3.11/3.38 (define @t426 () (@list @t50 @t20)) % 3.11/3.38 (define @t427 () (@var "F3" (-> tptp.set_HF_Mirabelle_hf tptp.hF_Mirabelle_hf))) % 3.11/3.38 (define @t428 () (_ tptp.inj_on811196232lle_hf @t427)) % 3.11/3.38 (define @t429 () (@var "S2" tptp.set_nat)) % 3.11/3.38 (define @t430 () (@var "Y5" tptp.nat)) % 3.11/3.38 (define @t431 () (@list @t430)) % 3.11/3.38 (define @t432 () (@var "S2" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t433 () (@var "F3" (-> tptp.hF_Mirabelle_hf tptp.nat))) % 3.11/3.38 (define @t434 () (@var "Y5" tptp.hF_Mirabelle_hf)) % 3.11/3.38 (define @t435 () (_ @t428 @t113)) % 3.11/3.38 (define @t436 () (_ tptp.ord_le2016357975lle_hf @t113)) % 3.11/3.38 (define @t437 () (_ @t428 @t36)) % 3.11/3.38 (define @t438 () (_ tptp.ord_le2016357975lle_hf @t36)) % 3.11/3.38 (define @t439 () (_ @t438 @t113)) % 3.11/3.38 (define @t440 () (_ @t350 tptp.zero_zero_nat)) % 3.11/3.38 (define @t441 () (@var "C3" tptp.nat)) % 3.11/3.38 (define @t442 () (@var "G" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t443 () (@var "G" tptp.set_nat)) % 3.11/3.38 (define @t444 () (_ tptp.ord_less_eq_nat @t325)) % 3.11/3.38 (define @t445 () (_ @t444 @t400)) % 3.11/3.38 (define @t446 () (_ tptp.ord_less_eq_nat @t323)) % 3.11/3.38 (define @t447 () (_ @t446 @t403)) % 3.11/3.38 (define @t448 () (@list @t43 @t22)) % 3.11/3.38 (define @t449 () (_ @t427 @t177)) % 3.11/3.38 (define @t450 () (@var "G2" (-> tptp.hF_Mirabelle_hf tptp.set_HF_Mirabelle_hf))) % 3.11/3.38 (define @t451 () (_ @t178 @t36)) % 3.11/3.38 (define @t452 () (= (_ @t427 @t88) (_ @t427 @t143))) % 3.11/3.38 (define @t453 () (_ (_ tptp.member1490636632lle_hf @t143) @t36)) % 3.11/3.38 (define @t454 () (= @t88 @t143)) % 3.11/3.38 (define @t455 () (@list @t427 @t36 @t88 @t143)) % 3.11/3.38 (define @t456 () (@var "G2" (-> tptp.set_HF_Mirabelle_hf tptp.hF_Mirabelle_hf))) % 3.11/3.38 (define @t457 () (@var "T3" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t458 () (@var "T3" tptp.set_nat)) % 3.11/3.38 (define @t459 () (@var "A22" tptp.hF_Mirabelle_hf)) % 3.11/3.38 (define @t460 () (@var "A1" tptp.hF_Mirabelle_hf)) % 3.11/3.38 (define @t461 () (= @t460 @t459)) % 3.11/3.38 (define @t462 () (@var "R" (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf Bool))) % 3.11/3.38 (define @t463 () (_ (_ tptp.member1367349282lle_hf @t459) @t50)) % 3.11/3.38 (define @t464 () (_ (_ tptp.member1367349282lle_hf @t460) @t50)) % 3.11/3.38 (define @t465 () (@var "B7" tptp.hF_Mirabelle_hf)) % 3.11/3.38 (define @t466 () (_ @t444 @t403)) % 3.11/3.38 (define @t467 () (@var "R" (-> tptp.hF_Mirabelle_hf tptp.nat Bool))) % 3.11/3.38 (define @t468 () (@var "B7" tptp.nat)) % 3.11/3.38 (define @t469 () (@var "M2" tptp.nat)) % 3.11/3.38 (define @t470 () (@var "X5" tptp.nat)) % 3.11/3.38 (define @t471 () (@var "M" tptp.nat)) % 3.11/3.38 (define @t472 () (_ @t55 @t186)) % 3.11/3.38 (define @t473 () (@var "K" tptp.nat)) % 3.11/3.38 (define @t474 () (@var "M3" tptp.nat)) % 3.11/3.38 (define @t475 () (_ @t343 @t474)) % 3.11/3.38 (define @t476 () (_ (_ tptp.ord_less_eq_nat @t474) @t25)) % 3.11/3.38 (define @t477 () (@list @t474 @t25)) % 3.11/3.38 (define @t478 () (= @t474 @t25)) % 3.11/3.38 (define @t479 () (@var "I" tptp.nat)) % 3.11/3.38 (define @t480 () (_ tptp.ord_less_eq_nat @t479)) % 3.11/3.38 (define @t481 () (@var "J" tptp.nat)) % 3.11/3.38 (define @t482 () (_ tptp.minus_minus_set_nat @t43)) % 3.11/3.38 (define @t483 () (_ tptp.minus_1450406810lle_hf @t50)) % 3.11/3.38 (define @t484 () (_ @t483 @t311)) % 3.11/3.38 (define @t485 () (@var "F5" (-> tptp.set_HF_Mirabelle_hf tptp.hF_Mirabelle_hf))) % 3.11/3.38 (define @t486 () (_ tptp.finite90088345lle_hf @t36)) % 3.11/3.38 (define @t487 () (_ (_ tptp.ord_less_eq_nat @t486) @t400)) % 3.11/3.38 (define @t488 () (@var "F5" (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf))) % 3.11/3.38 (define @t489 () (@var "F5" (-> tptp.hF_Mirabelle_hf tptp.nat))) % 3.11/3.38 (define @t490 () (@var "F5" (-> tptp.nat tptp.hF_Mirabelle_hf))) % 3.11/3.38 (define @t491 () (@var "F5" (-> tptp.nat tptp.nat))) % 3.11/3.38 (define @t492 () (_ tptp.image_899003828lle_hf @t427)) % 3.11/3.38 (define @t493 () (_ @t492 @t36)) % 3.11/3.38 (define @t494 () (@var "F3" (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf))) % 3.11/3.38 (define @t495 () (_ tptp.image_1743964010lle_hf @t494)) % 3.11/3.38 (define @t496 () (_ @t495 @t50)) % 3.11/3.38 (define @t497 () (_ @t494 @t20)) % 3.11/3.38 (define @t498 () (_ @t483 @t118)) % 3.11/3.38 (define @t499 () (_ @t35 @t498)) % 3.11/3.38 (define @t500 () (not @t397)) % 3.11/3.38 (define @t501 () (@list @t17 @t50 @t118)) % 3.11/3.38 (define @t502 () (_ tptp.minus_minus_nat @t28)) % 3.11/3.38 (define @t503 () (@list @t494 @t50)) % 3.11/3.38 (define @t504 () (@var "H" (-> tptp.hF_Mirabelle_hf tptp.hF_Mirabelle_hf))) % 3.11/3.38 (define @t505 () (@var "H" (-> tptp.hF_Mirabelle_hf tptp.nat))) % 3.11/3.38 (define @t506 () (@var "H" (-> tptp.nat tptp.hF_Mirabelle_hf))) % 3.11/3.38 (define @t507 () (@var "H" (-> tptp.nat tptp.nat))) % 3.11/3.38 (define @t508 () (_ @t494 @t9)) % 3.11/3.38 (define @t509 () (_ tptp.finite586181922lle_hf @t498)) % 3.11/3.38 (define @t510 () (_ tptp.finite_finite_nat (_ @t482 @t108))) % 3.11/3.38 (define @t511 () (_ tptp.minus_1450406810lle_hf @t93)) % 3.11/3.38 (define @t512 () (_ @t483 @t131)) % 3.11/3.38 (define @t513 () (_ @t130 @t512)) % 3.11/3.38 (define @t514 () (_ @t483 @t173)) % 3.11/3.38 (define @t515 () (@list @t50 @t9 @t118)) % 3.11/3.38 (define @t516 () (_ tptp.minus_500612048lle_hf @t36)) % 3.11/3.38 (define @t517 () (_ tptp.member1367349282lle_hf (_ @t427 @t71))) % 3.11/3.38 (define @t518 () (_ tptp.member1367349282lle_hf @t508)) % 3.11/3.38 (define @t519 () (_ tptp.inj_on755450110lle_hf @t494)) % 3.11/3.38 (define @t520 () (_ @t519 @t50)) % 3.11/3.38 (define @t521 () (_ @t492 @t113)) % 3.11/3.38 (define @t522 () (_ @t516 @t113)) % 3.11/3.38 (define @t523 () (@var "C3" tptp.set_se933006839lle_hf)) % 3.11/3.38 (define @t524 () (_ @t436 @t523)) % 3.11/3.38 (define @t525 () (_ @t428 @t523)) % 3.11/3.38 (define @t526 () (@list @t427 @t523 @t36 @t113)) % 3.11/3.38 (define @t527 () (_ @t423 @t496)) % 3.11/3.38 (define @t528 () (_ tptp.image_131453538hf_nat @t433)) % 3.11/3.38 (define @t529 () (_ @t528 @t50)) % 3.11/3.38 (define @t530 () (_ tptp.ord_less_eq_set_nat @t108)) % 3.11/3.38 (define @t531 () (_ @t530 @t529)) % 3.11/3.38 (define @t532 () (@var "F3" (-> tptp.nat tptp.hF_Mirabelle_hf))) % 3.11/3.38 (define @t533 () (_ tptp.image_246164834lle_hf @t532)) % 3.11/3.38 (define @t534 () (_ @t533 @t43)) % 3.11/3.38 (define @t535 () (_ @t423 @t534)) % 3.11/3.38 (define @t536 () (_ tptp.image_nat_nat @t385)) % 3.11/3.38 (define @t537 () (_ @t536 @t43)) % 3.11/3.38 (define @t538 () (_ @t530 @t537)) % 3.11/3.38 (define @t539 () (@var "C4" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t540 () (_ tptp.finite586181922lle_hf @t539)) % 3.11/3.38 (define @t541 () (_ (_ tptp.ord_le432112161lle_hf @t539) @t50)) % 3.11/3.38 (define @t542 () (@list @t539)) % 3.11/3.38 (define @t543 () (@var "C4" tptp.set_nat)) % 3.11/3.38 (define @t544 () (_ tptp.finite_finite_nat @t543)) % 3.11/3.38 (define @t545 () (_ (_ tptp.ord_less_eq_set_nat @t543) @t43)) % 3.11/3.38 (define @t546 () (@list @t543)) % 3.11/3.38 (define @t547 () (_ @t59 (_ @t495 @t395))) % 3.11/3.38 (define @t548 () (_ tptp.ord_le432112161lle_hf @t395)) % 3.11/3.38 (define @t549 () (_ @t548 @t50)) % 3.11/3.38 (define @t550 () (_ tptp.finite586181922lle_hf @t395)) % 3.11/3.38 (define @t551 () (@list @t395)) % 3.11/3.38 (define @t552 () (_ @t59 @t395)) % 3.11/3.38 (define @t553 () (_ @t548 @t496)) % 3.11/3.38 (define @t554 () (@list @t494 @t50 @t59)) % 3.11/3.38 (define @t555 () (@var "B6" tptp.set_nat)) % 3.11/3.38 (define @t556 () (_ @t59 (_ @t533 @t555))) % 3.11/3.38 (define @t557 () (_ tptp.ord_less_eq_set_nat @t555)) % 3.11/3.38 (define @t558 () (_ @t557 @t43)) % 3.11/3.38 (define @t559 () (_ tptp.finite_finite_nat @t555)) % 3.11/3.38 (define @t560 () (@list @t555)) % 3.11/3.38 (define @t561 () (_ @t548 @t534)) % 3.11/3.38 (define @t562 () (@list @t532 @t43 @t59)) % 3.11/3.38 (define @t563 () (_ @t285 (_ @t528 @t395))) % 3.11/3.38 (define @t564 () (_ @t285 @t555)) % 3.11/3.38 (define @t565 () (_ @t557 @t529)) % 3.11/3.38 (define @t566 () (@list @t433 @t50 @t285)) % 3.11/3.38 (define @t567 () (_ @t285 (_ @t536 @t555))) % 3.11/3.38 (define @t568 () (_ @t557 @t537)) % 3.11/3.38 (define @t569 () (@list @t385 @t43 @t285)) % 3.11/3.38 (define @t570 () (and @t550 @t549)) % 3.11/3.38 (define @t571 () (and @t559 @t558)) % 3.11/3.38 (define @t572 () (_ tptp.finite586181922lle_hf @t493)) % 3.11/3.38 (define @t573 () (@list @t427 @t36)) % 3.11/3.38 (define @t574 () (_ tptp.finite586181922lle_hf @t496)) % 3.11/3.38 (define @t575 () (_ (_ tptp.inj_on1988990670lle_hf @t532) @t43)) % 3.11/3.38 (define @t576 () (_ tptp.finite586181922lle_hf @t534)) % 3.11/3.38 (define @t577 () (@list @t532 @t43)) % 3.11/3.38 (define @t578 () (_ (_ tptp.inj_on1874279374hf_nat @t433) @t50)) % 3.11/3.38 (define @t579 () (_ tptp.finite_finite_nat @t529)) % 3.11/3.38 (define @t580 () (@list @t433 @t50)) % 3.11/3.38 (define @t581 () (_ (_ tptp.inj_on_nat_nat @t385) @t43)) % 3.11/3.38 (define @t582 () (_ tptp.finite_finite_nat @t537)) % 3.11/3.38 (define @t583 () (@list @t385 @t43)) % 3.11/3.38 (define @t584 () (@var "A7" tptp.set_se933006839lle_hf)) % 3.11/3.38 (define @t585 () (@var "X6" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t586 () (@var "A7" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t587 () (@var "X6" tptp.hF_Mirabelle_hf)) % 3.11/3.38 (define @t588 () (_ tptp.minus_1450406810lle_hf @t118)) % 3.11/3.38 (define @t589 () (not (_ @t3 tptp.z))) % 3.11/3.38 (define @t590 () (forall @t5 @t589)) % 3.11/3.38 (define @t591 () (= tptp.z tptp.zero_z189798548lle_hf)) % 3.11/3.38 (define @t592 () (= @t591 @t590)) % 3.11/3.38 (define @t593 () (not @t592)) % 3.11/3.38 (define @t594 () (_ tptp.hF_Mirabelle_hfset @t1)) % 3.11/3.38 (define @t595 () (lambda @t6 (_ (_ tptp.member1367349282lle_hf @t4) @t594))) % 3.11/3.38 (define @t596 () (lambda @t5 tptp.bot_bot_o)) % 3.11/3.38 (define @t597 () (lambda @t41 tptp.bot_bot_o)) % 3.11/3.38 (define @t598 () (lambda @t6 (_ tptp.hF_Mirabelle_HF (_ (_ tptp.insert9649339lle_hf @t4) @t594)))) % 3.11/3.38 (define @t599 () (lambda @t320 (= @t274 (_ (_ tptp.insert9649339lle_hf (_ tptp.the_el1104322134lle_hf @t274)) tptp.bot_bo53200981lle_hf)))) % 3.11/3.38 (define @t600 () (lambda @t320 (= @t274 tptp.bot_bo53200981lle_hf))) % 3.11/3.38 (define @t601 () (@var "T" tptp.hF_Mirabelle_hf)) % 3.11/3.38 (define @t602 () (_ tptp.member1367349282lle_hf @t601)) % 3.11/3.38 (define @t603 () (lambda @t396 (forall (@list @t601) (=> (_ @t602 @t274) (_ @t602 @t395))))) % 3.11/3.38 (define @t604 () (@var "Y4" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t605 () (@var "F4" (-> tptp.set_HF_Mirabelle_hf tptp.hF_Mirabelle_hf))) % 3.11/3.38 (define @t606 () (lambda (@list @t605 @t268) (forall @t41 (=> (_ @t39 @t268) (forall (@list @t604) (=> (_ (_ tptp.member1490636632lle_hf @t604) @t268) (=> (= (_ @t605 @t38) (_ @t605 @t604)) (= @t38 @t604)))))))) % 3.11/3.38 (define @t607 () (@var "M4" tptp.nat)) % 3.11/3.38 (define @t608 () (@var "N2" tptp.set_nat)) % 3.11/3.38 (define @t609 () (lambda (@list @t608) (exists (@list @t607) (forall @t48 (=> (_ @t46 @t608) (_ @t384 @t607)))))) % 3.11/3.38 (define @t610 () (@purify @t596)) % 3.11/3.38 (define @t611 () (tptp.collec2046588256lle_hf @t610)) % 3.11/3.38 (define @t612 () (tptp.finite1213132899lle_hf @t611)) % 3.11/3.38 (define @t613 () (tptp.hF_Mirabelle_Abs_hf @t612)) % 3.11/3.38 (define @t614 () (tptp.hF_Mirabelle_HF @t611)) % 3.11/3.38 (define @t615 () (_ tptp.collec2046588256lle_hf @t610)) % 3.11/3.38 (define @t616 () (_ tptp.finite1213132899lle_hf @t615)) % 3.11/3.38 (define @t617 () (_ tptp.collec2046588256lle_hf @t596)) % 3.11/3.38 (define @t618 () (_ tptp.finite1213132899lle_hf @t617)) % 3.11/3.38 (define @t619 () (_ tptp.hF_Mirabelle_Abs_hf @t618)) % 3.11/3.38 (define @t620 () (= tptp.z @t619)) % 3.11/3.38 (define @t621 () (tptp.hF_Mirabelle_hfset tptp.z)) % 3.11/3.38 (define @t622 () (tptp.member1367349282lle_hf @t2 @t621)) % 3.11/3.38 (define @t623 () (forall @t5 (not @t622))) % 3.11/3.38 (define @t624 () (= @t623 @t620)) % 3.11/3.38 (define @t625 () (= @t619 tptp.z)) % 3.11/3.38 (define @t626 () (= tptp.zero_z189798548lle_hf tptp.z)) % 3.11/3.38 (define @t627 () (= @t626 @t623)) % 3.11/3.38 (define @t628 () (_ tptp.hF_Mirabelle_hfset tptp.z)) % 3.11/3.38 (define @t629 () (_ @t52 @t628)) % 3.11/3.38 (define @t630 () (not @t629)) % 3.11/3.38 (define @t631 () (@list @t1)) % 3.11/3.38 (define @t632 () (lambda @t631 (_ @t52 @t594))) % 3.11/3.38 (define @t633 () (_ @t595 @t2)) % 3.11/3.38 (define @t634 () (not (_ @t633 tptp.z))) % 3.11/3.38 (define @t635 () (forall @t5 @t634)) % 3.11/3.38 (define @t636 () (= @t591 @t635)) % 3.11/3.38 (define @t637 () (tptp.hF_Mirabelle_hfset @t9)) % 3.11/3.38 (define @t638 () (tptp.hF_Mirabelle_HF @t637)) % 3.11/3.38 (define @t639 () (= @t9 @t31)) % 3.11/3.38 (define @t640 () (@list tptp.z)) % 3.11/3.38 (define @t641 () (= @t621 @t611)) % 3.11/3.38 (define @t642 () (not @t641)) % 3.11/3.38 (define @t643 () (tptp.hF_Mirabelle_HF @t621)) % 3.11/3.38 (define @t644 () (= tptp.z @t643)) % 3.11/3.38 (define @t645 () (not @t644)) % 3.11/3.38 (define @t646 () (= tptp.z @t613)) % 3.11/3.38 (define @t647 () (= @t614 @t613)) % 3.11/3.38 (define @t648 () (not @t647)) % 3.11/3.38 (define @t649 () (not @t646)) % 3.11/3.38 (define @t650 () (= @t614 @t643)) % 3.11/3.38 (define @t651 () (and @t647 @t650 @t644 @t649)) % 3.11/3.38 (define @t652 () (tptp.finite586181922lle_hf @t637)) % 3.11/3.38 (define @t653 () (tptp.finite586181922lle_hf @t192)) % 3.11/3.38 (define @t654 () (not @t653)) % 3.11/3.38 (define @t655 () (tptp.member1367349282lle_hf @t195 @t192)) % 3.11/3.38 (define @t656 () (tptp.insert9649339lle_hf @t195 @t192)) % 3.11/3.38 (define @t657 () (not (forall @t204 (or (not (= @t202 @t656)) @t655 @t654)))) % 3.11/3.38 (define @t658 () (tptp.collec2046588256lle_hf @t596)) % 3.11/3.38 (define @t659 () (= @t202 @t617)) % 3.11/3.38 (define @t660 () (tptp.finite586181922lle_hf @t202)) % 3.11/3.38 (define @t661 () (not @t660)) % 3.11/3.38 (define @t662 () (or @t661 @t659 @t657)) % 3.11/3.38 (define @t663 () (or @t661 (= @t617 @t202) @t657)) % 3.11/3.38 (define @t664 () (= tptp.bot_bo53200981lle_hf @t202)) % 3.11/3.38 (define @t665 () (or @t661 @t664 @t657)) % 3.11/3.38 (define @t666 () (not @t209)) % 3.11/3.38 (define @t667 () (or @t666 @t664 @t657)) % 3.11/3.38 (define @t668 () (not @t664)) % 3.11/3.38 (define @t669 () (=> @t668 @t657)) % 3.11/3.38 (define @t670 () (not @t203)) % 3.11/3.38 (define @t671 () (or @t670 @t197 @t194)) % 3.11/3.38 (define @t672 () (forall @t204 (or (not (= @t656 @t621)) @t655 @t654))) % 3.11/3.38 (define @t673 () (not @t672)) % 3.11/3.38 (define @t674 () (= @t621 @t658)) % 3.11/3.38 (define @t675 () (tptp.finite586181922lle_hf @t621)) % 3.11/3.38 (define @t676 () (not @t675)) % 3.11/3.38 (define @t677 () (or @t676 @t674 @t673)) % 3.11/3.38 (define @t678 () (forall @t211 (or @t661 (= @t202 @t658) @t657))) % 3.11/3.38 (define @t679 () (not (= @t621 @t656))) % 3.11/3.38 (define @t680 () (or @t679 @t655 @t654)) % 3.11/3.38 (define @t681 () (forall @t204 @t680)) % 3.11/3.38 (define @t682 () (not @t681)) % 3.11/3.38 (define @t683 () (or @t676 @t674 @t682)) % 3.11/3.38 (define @t684 () (or @t676 @t641 @t673)) % 3.11/3.38 (define @t685 () (@list false)) % 3.11/3.38 (define @t686 () (@quantifiers_skolemize @t672 0)) % 3.11/3.38 (define @t687 () (not (tptp.finite586181922lle_hf @t686))) % 3.11/3.38 (define @t688 () (@quantifiers_skolemize @t672 1)) % 3.11/3.38 (define @t689 () (tptp.member1367349282lle_hf @t688 @t686)) % 3.11/3.38 (define @t690 () (tptp.insert9649339lle_hf @t688 @t686)) % 3.11/3.38 (define @t691 () (= @t621 @t690)) % 3.11/3.38 (define @t692 () (not @t691)) % 3.11/3.38 (define @t693 () (or @t692 @t689 @t687)) % 3.11/3.38 (define @t694 () (not @t693)) % 3.11/3.38 (define @t695 () (not (= @t690 @t621))) % 3.11/3.38 (define @t696 () (or @t695 @t689 @t687)) % 3.11/3.38 (define @t697 () (not @t696)) % 3.11/3.38 (define @t698 () (tptp.member1367349282lle_hf @t688 @t621)) % 3.11/3.38 (define @t699 () (not @t698)) % 3.11/3.38 (define @t700 () (@var "BOUND_VARIABLE_10865" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t701 () (@var "BOUND_VARIABLE_10867" tptp.hF_Mirabelle_hf)) % 3.11/3.38 (define @t702 () (tptp.insert9649339lle_hf @t701 @t700)) % 3.11/3.38 (define @t703 () (tptp.member1367349282lle_hf @t701 @t702)) % 3.11/3.38 (define @t704 () (not (= @t701 @t701))) % 3.11/3.38 (define @t705 () (or @t704 @t703)) % 3.11/3.38 (define @t706 () (@list @t700 @t701)) % 3.11/3.38 (define @t707 () (@var "BOUND_VARIABLE_10863" tptp.hF_Mirabelle_hf)) % 3.11/3.38 (define @t708 () (tptp.member1367349282lle_hf @t707 @t702)) % 3.11/3.38 (define @t709 () (not (= @t707 @t701))) % 3.11/3.38 (define @t710 () (or @t709 @t709 @t708)) % 3.11/3.38 (define @t711 () (@list @t707)) % 3.11/3.38 (define @t712 () (or @t709 @t708)) % 3.11/3.38 (define @t713 () (forall @t711 @t712)) % 3.11/3.38 (define @t714 () (forall @t706 @t713)) % 3.11/3.38 (define @t715 () (forall (@list @t700 @t701 @t707) @t712)) % 3.11/3.38 (define @t716 () (forall (@list @t707 @t700 @t701) @t712)) % 3.11/3.38 (define @t717 () (@var "BOUND_VARIABLE_10852" tptp.set_HF_Mirabelle_hf)) % 3.11/3.38 (define @t718 () (@var "BOUND_VARIABLE_10854" tptp.hF_Mirabelle_hf)) % 3.11/3.38 (define @t719 () (@var "BOUND_VARIABLE_10850" tptp.hF_Mirabelle_hf)) % 3.11/3.38 (define @t720 () (forall (@list @t719 @t717 @t718) (or (not (tptp.member1367349282lle_hf @t719 @t717)) (tptp.member1367349282lle_hf @t719 (tptp.insert9649339lle_hf @t718 @t717))))) % 3.11/3.38 (define @t721 () (tptp.insert9649339lle_hf @t18 @t118)) % 3.11/3.38 (define @t722 () (tptp.member1367349282lle_hf @t9 @t721)) % 3.11/3.38 (define @t723 () (or @t158 @t722)) % 3.11/3.38 (define @t724 () (forall @t124 @t723)) % 3.11/3.38 (define @t725 () (@list @t9 @t118 @t18)) % 3.11/3.38 (define @t726 () (tptp.member1367349282lle_hf @t9 @t118)) % 3.11/3.38 (define @t727 () (not @t726)) % 3.11/3.38 (define @t728 () (or @t727 @t722)) % 3.11/3.38 (define @t729 () (forall @t124 @t728)) % 3.11/3.38 (define @t730 () (and @t729 @t724)) % 3.11/3.38 (define @t731 () (and @t122 @t158)) % 3.11/3.38 (define @t732 () (or @t731 @t120)) % 3.11/3.38 (define @t733 () (tptp.member1367349282lle_hf @t688 @t690)) % 3.11/3.38 (define @t734 () (not @t733)) % 3.11/3.38 (define @t735 () (= true false)) % 3.11/3.38 (define @t736 () (and @t699 @t691 @t733)) % 3.11/3.38 (define @t737 () (not @t623)) % 3.11/3.38 (define @t738 () (@list true)) % 3.11/3.38 (define @t739 () (@list @t623)) % 3.11/3.38 (define @t740 () (@quantifiers_skolemize @t623 0)) % 3.11/3.38 (define @t741 () (tptp.member1367349282lle_hf @t740 @t621)) % 3.11/3.38 (define @t742 () (not @t741)) % 3.11/3.38 (define @t743 () (not @t742)) % 3.11/3.38 (define @t744 () (tptp.finite1213132899lle_hf @t658)) % 3.11/3.38 (define @t745 () (tptp.hF_Mirabelle_Abs_hf @t744)) % 3.11/3.38 (define @t746 () (tptp.hF_Mirabelle_hfset @t619)) % 3.11/3.38 (define @t747 () (tptp.member1367349282lle_hf @t9 @t746)) % 3.11/3.38 (define @t748 () (not @t747)) % 3.11/3.38 (define @t749 () (tptp.hF_Mirabelle_hfset tptp.zero_z189798548lle_hf)) % 3.11/3.38 (define @t750 () (tptp.member1367349282lle_hf @t9 @t749)) % 3.11/3.38 (define @t751 () (not @t750)) % 3.11/3.38 (define @t752 () (_ tptp.hF_Mirabelle_hfset tptp.zero_z189798548lle_hf)) % 3.11/3.38 (define @t753 () (_ @t76 @t752)) % 3.11/3.38 (define @t754 () (not @t753)) % 3.11/3.38 (define @t755 () (lambda @t631 (_ @t76 @t594))) % 3.11/3.38 (define @t756 () (_ @t595 @t9)) % 3.11/3.38 (define @t757 () (not (_ @t756 tptp.zero_z189798548lle_hf))) % 3.11/3.38 (define @t758 () (tptp.hF_Mirabelle_hfset @t745)) % 3.11/3.38 (define @t759 () (tptp.member1367349282lle_hf @t740 @t758)) % 3.11/3.38 (define @t760 () (not @t759)) % 3.11/3.38 (define @t761 () (forall @t12 (not (tptp.member1367349282lle_hf @t9 @t758)))) % 3.11/3.38 (define @t762 () (tptp.member1367349282lle_hf @t740 (tptp.hF_Mirabelle_hfset @t613))) % 3.11/3.38 (define @t763 () (not @t762)) % 3.11/3.38 (define @t764 () (and @t763 @t647 @t646 @t741)) % 3.11/3.38 (assume @p1 (= (lambda (@list @t8 @t7) (= @t8 @t7)) (lambda @t6 (forall @t5 (= (_ @t3 @t4) (_ @t3 @t1)))))) % 3.11/3.38 (assume @p2 @t13) % 3.11/3.38 (assume @p3 (forall (@list @t16) (=> (not (= @t16 tptp.zero_z189798548lle_hf)) (not (forall (@list @t15 @t14) (=> (= @t16 (_ (_ tptp.hF_Mirabelle_hinsert @t15) @t14)) (_ (_ tptp.hF_Mirabelle_hmem @t15) @t14))))))) % 3.11/3.38 (assume @p4 (forall (@list @t9 @t18 @t17) (= (_ @t10 (_ (_ tptp.hF_Mirabelle_hinsert @t18) @t17)) (or @t19 (_ @t10 @t17))))) % 3.11/3.38 (assume @p5 (forall @t21 (= (= tptp.zero_z189798548lle_hf @t20) (= @t20 tptp.zero_z189798548lle_hf)))) % 3.11/3.38 (assume @p6 (forall @t23 (= (= tptp.zero_zero_nat @t22) (= @t22 tptp.zero_zero_nat)))) % 3.11/3.38 (assume @p7 (= (_ tptp.hF_Mirabelle_Abs_hf tptp.zero_zero_nat) tptp.zero_z189798548lle_hf)) % 3.11/3.38 (assume @p8 @t24) % 3.11/3.38 (assume @p9 (forall @t27 (= (_ @t26 tptp.zero_zero_nat) tptp.zero_zero_nat))) % 3.11/3.38 (assume @p10 (forall (@list @t25 @t28) (= (= (_ @t26 @t28) tptp.zero_zero_nat) @t29))) % 3.11/3.38 (assume @p11 (forall @t27 (= (_ (_ tptp.semiri2115134414it_nat @t25) tptp.zero_zero_nat) tptp.zero_zero_nat))) % 3.11/3.38 (assume @p12 (_ (_ tptp.member_nat tptp.zero_zero_nat) tptp.semiring_1_Nats_nat)) % 3.11/3.38 (assume @p13 @t32) % 3.11/3.38 (assume @p14 (forall (@list @t33) (not (_ (_ tptp.member1490636632lle_hf @t33) tptp.bot_bo2093393035lle_hf)))) % 3.11/3.38 (assume @p15 (forall (@list @t34) (not (_ (_ tptp.member_nat @t34) tptp.bot_bot_set_nat)))) % 3.11/3.38 (assume @p16 (forall (@list @t17) (not (_ @t35 tptp.bot_bo53200981lle_hf)))) % 3.11/3.38 (assume @p17 (forall @t42 (= (forall @t41 (not @t40)) @t37))) % 3.11/3.38 (assume @p18 (forall @t49 (= (forall @t48 (not @t47)) @t44))) % 3.11/3.38 (assume @p19 (forall @t54 (= (forall @t5 (not @t53)) @t51))) % 3.11/3.38 (assume @p20 (forall @t58 (= (= @t57 tptp.bot_bot_set_nat) @t56))) % 3.11/3.38 (assume @p21 (forall @t64 (= @t63 @t61))) % 3.11/3.38 (assume @p22 (forall @t69 (= @t68 @t66))) % 3.11/3.38 (assume @p23 (forall @t58 (= (= tptp.bot_bot_set_nat @t57) @t56))) % 3.11/3.38 (assume @p24 (forall @t64 (= (= tptp.bot_bo2093393035lle_hf @t62) @t61))) % 3.11/3.38 (assume @p25 (forall @t69 (= (= tptp.bot_bo53200981lle_hf @t67) @t66))) % 3.11/3.38 (assume @p26 (forall @t54 (=> @t70 (= (_ tptp.hF_Mirabelle_hfset (_ tptp.hF_Mirabelle_HF @t50)) @t50)))) % 3.11/3.38 (assume @p27 (= tptp.zero_zero_nat tptp.zero_zero_nat)) % 3.11/3.38 (assume @p28 (forall @t73 (not (_ @t72 tptp.bot_bo2093393035lle_hf)))) % 3.11/3.38 (assume @p29 (forall @t75 (not (_ @t74 tptp.bot_bot_set_nat)))) % 3.11/3.38 (assume @p30 (forall @t12 (not (_ @t76 tptp.bot_bo53200981lle_hf)))) % 3.11/3.38 (assume @p31 (forall (@list @t36 @t71) (=> @t37 @t78))) % 3.11/3.38 (assume @p32 (forall @t81 (=> @t44 @t80))) % 3.11/3.38 (assume @p33 (forall @t84 (=> @t51 @t83))) % 3.11/3.38 (assume @p34 (forall @t87 (= (_ @t85 @t86) @t86))) % 3.11/3.38 (assume @p35 (forall @t91 (= (_ @t89 @t90) @t90))) % 3.11/3.38 (assume @p36 (forall @t94 (= (_ @t92 @t93) @t93))) % 3.11/3.38 (assume @p37 (forall @t99 (= @t98 (or @t96 @t79)))) % 3.11/3.38 (assume @p38 (forall @t104 (= @t103 (or @t101 @t77)))) % 3.11/3.38 (assume @p39 (forall @t107 (= @t106 (or @t19 @t82)))) % 3.11/3.38 (assume @p40 (forall @t112 (=> (=> (not @t111) @t96) @t110))) % 3.11/3.38 (assume @p41 (forall @t117 (=> (=> (not @t116) @t101) @t115))) % 3.11/3.38 (assume @p42 @t125) % 3.11/3.38 (assume @p43 (forall @t73 (_ @t72 @t127))) % 3.11/3.38 (assume @p44 (forall @t75 (_ @t74 @t129))) % 3.11/3.38 (assume @p45 (forall @t12 (_ @t76 @t131))) % 3.11/3.38 (assume @p46 (forall @t134 (=> @t79 (exists @t133 (and (= @t43 (_ @t128 @t132)) (not (_ @t74 @t132))))))) % 3.11/3.38 (assume @p47 (forall @t137 (=> @t77 (exists @t136 (and (= @t36 (_ @t126 @t135)) (not (_ @t72 @t135))))))) % 3.11/3.38 (assume @p48 (forall @t140 (=> @t82 (exists @t139 (and (= @t50 (_ @t130 @t138)) (not (_ @t76 @t138))))))) % 3.11/3.38 (assume @p49 (forall (@list @t22 @t141 @t43) (= (_ @t85 (_ @t142 @t43)) (_ @t142 @t86)))) % 3.11/3.38 (assume @p50 (forall (@list @t88 @t143 @t36) (= (_ @t89 (_ @t144 @t36)) (_ @t144 @t90)))) % 3.11/3.38 (assume @p51 (forall (@list @t20 @t16 @t50) (= (_ @t92 (_ @t145 @t50)) (_ @t145 @t93)))) % 3.11/3.38 (assume @p52 (forall (@list @t28 @t43 @t95 @t108) (=> @t80 (=> (not (_ @t147 @t108)) (= (= @t150 @t109) (and (=> @t96 @t149) (=> @t148 (exists (@list @t146) (and (= @t43 (_ @t97 @t146)) (not (_ @t147 @t146)) (= @t108 (_ @t128 @t146)) (not (_ @t74 @t146))))))))))) % 3.11/3.38 (assume @p53 (forall (@list @t71 @t36 @t100 @t113) (=> @t78 (=> (not (_ @t152 @t113)) (= (= @t155 @t114) (and (=> @t101 @t154) (=> @t153 (exists (@list @t151) (and (= @t36 (_ @t102 @t151)) (not (_ @t152 @t151)) (= @t113 (_ @t126 @t151)) (not (_ @t72 @t151))))))))))) % 3.11/3.38 (assume @p54 (forall (@list @t9 @t50 @t18 @t118) (=> @t83 (=> (not (_ @t157 @t118)) (= (= @t160 @t119) (and (=> @t19 @t159) (=> @t158 (exists (@list @t156) (and (= @t50 (_ @t105 @t156)) (not (_ @t157 @t156)) (= @t118 (_ @t130 @t156)) (not (_ @t76 @t156))))))))))) % 3.11/3.38 (assume @p55 (forall @t134 (=> @t79 (= @t150 @t43)))) % 3.11/3.38 (assume @p56 (forall @t137 (=> @t77 (= @t155 @t36)))) % 3.11/3.38 (assume @p57 (forall @t140 (=> @t82 (= @t160 @t50)))) % 3.11/3.38 (assume @p58 (forall (@list @t22 @t43 @t108) (=> (not @t162) (=> (not (_ @t161 @t108)) (= (= @t86 (_ @t85 @t108)) @t149))))) % 3.11/3.38 (assume @p59 (forall (@list @t88 @t36 @t113) (=> (not @t164) (=> (not (_ @t163 @t113)) (= (= @t90 (_ @t89 @t113)) @t154))))) % 3.11/3.38 (assume @p60 (forall @t171 (=> @t170 (=> @t168 (= (= @t93 @t165) @t159))))) % 3.11/3.38 (assume @p61 (forall @t87 (=> @t162 (not (forall @t133 (=> (= @t43 (_ @t85 @t132)) (_ @t161 @t132))))))) % 3.11/3.38 (assume @p62 (forall @t91 (=> @t164 (not (forall @t136 (=> (= @t36 (_ @t89 @t135)) (_ @t163 @t135))))))) % 3.11/3.38 (assume @p63 (forall @t94 (=> @t169 (not (forall @t139 (=> (= @t50 (_ @t92 @t138)) (_ @t166 @t138))))))) % 3.11/3.38 (assume @p64 (forall @t112 (=> @t111 @t110))) % 3.11/3.38 (assume @p65 (forall @t117 (=> @t116 @t115))) % 3.11/3.38 (assume @p66 (forall @t124 (=> @t121 @t120))) % 3.11/3.38 (assume @p67 (forall (@list @t28 @t108) (_ @t74 @t172))) % 3.11/3.38 (assume @p68 (forall (@list @t71 @t113) (_ @t72 (_ @t126 @t113)))) % 3.11/3.38 (assume @p69 (forall (@list @t9 @t118) (_ @t76 @t173))) % 3.11/3.38 (assume @p70 (forall @t99 (=> @t98 (=> @t148 @t79)))) % 3.11/3.38 (assume @p71 (forall @t104 (=> @t103 (=> @t153 @t77)))) % 3.11/3.38 (assume @p72 (forall @t107 (=> @t106 (=> @t158 @t82)))) % 3.11/3.38 (assume @p73 (forall (@list @t180) (=> @t182 (=> @t181 (not (forall (@list @t174 @t177) (=> (= @t180 (_ @t179 @t174)) (=> (not (_ @t178 @t174)) @t176)))))))) % 3.11/3.38 (assume @p74 (forall (@list @t189) (=> @t191 (=> @t190 (not (forall (@list @t183 @t186) (=> (= @t189 (_ @t188 @t183)) (=> (not (_ @t187 @t183)) @t185)))))))) % 3.11/3.38 (assume @p75 @t212) % 3.11/3.38 (assume @p76 (= tptp.bot_bot_set_nat (_ tptp.collect_nat tptp.bot_bot_nat_o))) % 3.11/3.38 (assume @p77 (= tptp.bot_bo2093393035lle_hf (_ tptp.collec1758573718lle_hf tptp.bot_bo554042810e_hf_o))) % 3.11/3.38 (assume @p78 @t213) % 3.11/3.38 (assume @p79 (forall (@list @t71 @t100) (=> (= @t127 @t214) @t101))) % 3.11/3.38 (assume @p80 (forall @t216 (=> (= @t129 @t215) @t96))) % 3.11/3.38 (assume @p81 (forall (@list @t9 @t18) (=> (= @t131 @t217) @t19))) % 3.11/3.38 (assume @p82 (forall @t137 (not (= @t155 tptp.bot_bo2093393035lle_hf)))) % 3.11/3.38 (assume @p83 (forall @t134 (not (= @t150 tptp.bot_bot_set_nat)))) % 3.11/3.38 (assume @p84 (forall @t140 (not (= @t160 tptp.bot_bo53200981lle_hf)))) % 3.11/3.38 (assume @p85 (forall (@list @t71 @t100 @t33 @t218) (= (= (_ @t126 @t214) (_ (_ tptp.insert1636143089lle_hf @t33) (_ (_ tptp.insert1636143089lle_hf @t218) tptp.bot_bo2093393035lle_hf))) (or (and (= @t71 @t33) (= @t100 @t218)) (and (= @t71 @t218) (= @t100 @t33)))))) % 3.11/3.38 (assume @p86 (forall (@list @t28 @t95 @t34 @t220) (= (= (_ @t128 @t215) (_ (_ tptp.insert_nat @t34) (_ (_ tptp.insert_nat @t220) tptp.bot_bot_set_nat))) (or (and (= @t28 @t34) (= @t95 @t220)) (and (= @t28 @t220) @t219))))) % 3.11/3.38 (assume @p87 (forall (@list @t9 @t18 @t17 @t221) (= (= (_ @t130 @t217) (_ (_ tptp.insert9649339lle_hf @t17) (_ (_ tptp.insert9649339lle_hf @t221) tptp.bot_bo53200981lle_hf))) (or (and (= @t9 @t17) (= @t18 @t221)) (and (= @t9 @t221) (= @t18 @t17)))))) % 3.11/3.38 (assume @p88 (forall (@list @t28 @t55) (= (_ @t74 @t57) (_ @t55 @t28)))) % 3.11/3.38 (assume @p89 (forall (@list @t9 @t65) (= (_ @t76 @t67) (_ @t65 @t9)))) % 3.11/3.38 (assume @p90 (forall (@list @t71 @t59) (= (_ @t72 @t62) (_ @t59 @t71)))) % 3.11/3.38 (assume @p91 (forall @t49 (= (_ tptp.collect_nat (lambda @t48 @t47)) @t43))) % 3.11/3.38 (assume @p92 (forall @t54 (= (_ tptp.collec2046588256lle_hf (lambda @t5 @t53)) @t50))) % 3.11/3.38 (assume @p93 (forall @t42 (= (_ tptp.collec1758573718lle_hf (lambda @t41 @t40)) @t36))) % 3.11/3.38 (assume @p94 (forall (@list @t65 @t222) (=> (forall @t223 (= (_ @t65 @t195) (_ @t222 @t195))) (= @t67 (_ tptp.collec2046588256lle_hf @t222))))) % 3.11/3.38 (assume @p95 (forall @t229 (=> (forall @t228 (= @t227 @t226)) (= @t62 @t225)))) % 3.11/3.38 (assume @p96 (forall @t232 (= @t231 @t230))) % 3.11/3.38 (assume @p97 (forall @t235 (= @t234 @t233))) % 3.11/3.38 (assume @p98 (forall @t238 (= @t237 @t236))) % 3.11/3.38 (assume @p99 (forall @t232 (=> @t231 @t230))) % 3.11/3.38 (assume @p100 (forall @t235 (=> @t234 @t233))) % 3.11/3.38 (assume @p101 (forall @t238 (=> @t237 @t236))) % 3.11/3.38 (assume @p102 (= tptp.bot_bot_nat tptp.zero_zero_nat)) % 3.11/3.38 (assume @p103 @t240) % 3.11/3.38 (assume @p104 (forall @t42 (= (exists @t41 @t40) (not @t37)))) % 3.11/3.38 (assume @p105 (forall @t49 (= (exists @t48 @t47) @t241))) % 3.11/3.38 (assume @p106 (forall @t54 (= (exists @t5 @t53) @t242))) % 3.11/3.38 (assume @p107 (forall @t42 (=> (forall (@list @t243) (not @t244)) @t37))) % 3.11/3.38 (assume @p108 (forall @t49 (=> (forall @t246 (not (_ (_ tptp.member_nat @t245) @t43))) @t44))) % 3.11/3.38 (assume @p109 (forall @t54 (=> (forall (@list @t247) (not @t248)) @t51))) % 3.11/3.38 (assume @p110 (forall @t137 (= (_ tptp.finite1450550360lle_hf @t155) @t249))) % 3.11/3.38 (assume @p111 (forall @t140 (= @t250 @t70))) % 3.11/3.38 (assume @p112 (forall @t134 (= @t252 @t251))) % 3.11/3.38 (assume @p113 (forall (@list @t255) (=> (_ tptp.finite1450550360lle_hf @t255) (=> (not (= @t255 tptp.bot_bo2093393035lle_hf)) (not (forall @t257 (=> (exists @t256 (= @t255 @t254)) @t176))))))) % 3.11/3.38 (assume @p114 (forall (@list @t261) (=> (_ tptp.finite_finite_nat @t261) (=> (not (= @t261 tptp.bot_bot_set_nat)) (not (forall @t262 (=> (exists (@list @t258) (= @t261 @t260)) @t185))))))) % 3.11/3.38 (assume @p115 (forall @t73 (=> (_ tptp.finite586181922lle_hf @t71) (=> (not @t267) (not (forall @t266 (=> (exists @t265 (= @t71 @t264)) @t194))))))) % 3.11/3.38 (assume @p116 (= tptp.finite1450550360lle_hf (lambda (@list @t270) (or (= @t270 tptp.bot_bo2093393035lle_hf) (exists (@list @t268 @t269) (and (= @t270 (_ (_ tptp.insert1636143089lle_hf @t269) @t268)) (_ tptp.finite1450550360lle_hf @t268))))))) % 3.11/3.38 (assume @p117 (= tptp.finite_finite_nat (lambda (@list @t273) (or (= @t273 tptp.bot_bot_set_nat) (exists (@list @t271 @t272) (and (= @t273 (_ (_ tptp.insert_nat @t272) @t271)) (_ tptp.finite_finite_nat @t271))))))) % 3.11/3.38 (assume @p118 (= tptp.finite586181922lle_hf (lambda (@list @t275) (or (= @t275 tptp.bot_bo53200981lle_hf) (exists (@list @t274 @t1) (and (= @t275 (_ (_ tptp.insert9649339lle_hf @t1) @t274)) (_ tptp.finite586181922lle_hf @t274))))))) % 3.11/3.38 (assume @p119 (forall @t284 (=> @t182 (=> @t283 (=> @t282 @t277))))) % 3.11/3.38 (assume @p120 (forall @t294 (=> @t191 (=> @t293 (=> @t292 @t286))))) % 3.11/3.38 (assume @p121 (forall @t303 (=> @t209 (=> @t302 (=> @t301 @t295))))) % 3.11/3.38 (assume @p122 (forall (@list @t304 @t276) (=> (_ tptp.finite1450550360lle_hf @t304) (=> @t283 (=> (forall (@list @t174 @t253) (=> @t175 (=> @t305 (_ @t276 @t254)))) (_ @t276 @t304)))))) % 3.11/3.38 (assume @p123 (forall (@list @t306 @t285) (=> (_ tptp.finite_finite_nat @t306) (=> @t293 (=> (forall (@list @t183 @t258) (=> @t184 (=> @t307 (_ @t285 @t260)))) (_ @t285 @t306)))))) % 3.11/3.38 (assume @p124 (forall (@list @t88 @t59) (=> (_ tptp.finite586181922lle_hf @t88) (=> @t302 (=> (forall (@list @t192 @t15) (=> @t193 (=> @t308 (_ @t59 @t264)))) (_ @t59 @t88)))))) % 3.11/3.38 (assume @p125 (forall @t284 (=> @t182 (=> @t181 (=> (forall @t228 (_ @t276 (_ @t179 tptp.bot_bo2093393035lle_hf))) (=> (forall @t281 (=> @t280 (=> (not (= @t278 tptp.bot_bo2093393035lle_hf)) @t279))) @t277)))))) % 3.11/3.38 (assume @p126 (forall @t294 (=> @t191 (=> @t190 (=> (forall @t309 (_ @t285 (_ @t188 tptp.bot_bot_set_nat))) (=> (forall @t291 (=> @t290 (=> (not (= @t287 tptp.bot_bot_set_nat)) @t289))) @t286)))))) % 3.11/3.38 (assume @p127 (forall @t303 (=> @t209 (=> @t207 (=> (forall @t223 (_ @t59 @t310)) (=> (forall @t300 (=> @t299 (=> (not (= @t296 tptp.bot_bo53200981lle_hf)) @t298))) @t295)))))) % 3.11/3.38 (assume @p128 (forall (@list @t276 @t36) (=> (forall @t257 (=> @t176 @t305)) (=> @t283 (=> @t282 (_ @t276 @t36)))))) % 3.11/3.38 (assume @p129 (forall (@list @t285 @t43) (=> (forall @t262 (=> @t185 @t307)) (=> @t293 (=> @t292 (_ @t285 @t43)))))) % 3.11/3.38 (assume @p130 (forall (@list @t59 @t50) (=> (forall @t266 (=> @t194 @t308)) (=> @t302 (=> @t301 (_ @t59 @t50)))))) % 3.11/3.38 (assume @p131 (forall @t21 (= (_ tptp.the_el1104322134lle_hf @t311) @t20))) % 3.11/3.38 (assume @p132 (_ tptp.finite_finite_nat tptp.bot_bot_set_nat)) % 3.11/3.38 (assume @p133 (_ tptp.finite586181922lle_hf tptp.bot_bo53200981lle_hf)) % 3.11/3.38 (assume @p134 (forall (@list @t312) (=> @t315 @t313))) % 3.11/3.38 (assume @p135 (forall (@list @t316) (=> @t319 @t317))) % 3.11/3.38 (assume @p136 (forall @t84 (=> @t70 @t250))) % 3.11/3.38 (assume @p137 (forall @t81 (=> @t251 @t252))) % 3.11/3.38 (assume @p138 (= tptp.bot_bo1263054448e_hf_o (lambda @t5 (_ @t52 tptp.bot_bo53200981lle_hf)))) % 3.11/3.38 (assume @p139 (forall @t64 (= @t63 (= @t59 tptp.bot_bo554042810e_hf_o)))) % 3.11/3.38 (assume @p140 (forall @t69 (= @t68 (= @t65 tptp.bot_bo1263054448e_hf_o)))) % 3.11/3.38 (assume @p141 (forall @t21 (_ tptp.is_sin1448700567lle_hf @t311))) % 3.11/3.38 (assume @p142 (= tptp.is_sin1448700567lle_hf (lambda @t320 (exists @t5 (= @t274 (_ (_ tptp.insert9649339lle_hf @t2) tptp.bot_bo53200981lle_hf)))))) % 3.11/3.38 (assume @p143 (forall @t54 (=> @t321 (not (forall @t223 (not (= @t50 @t310))))))) % 3.11/3.38 (assume @p144 (forall @t54 (=> @t242 (=> (forall (@list @t195 @t247) (=> @t322 (=> @t248 (= @t195 @t247)))) @t321)))) % 3.11/3.38 (assume @p145 (forall @t49 (=> @t251 (= @t324 @t44)))) % 3.11/3.38 (assume @p146 (forall @t54 (=> @t70 (= @t326 @t51)))) % 3.11/3.38 (assume @p147 (forall @t332 (=> @t191 (=> @t331 (=> @t293 (=> (forall @t330 (=> @t290 (=> @t329 @t328))) @t286)))))) % 3.11/3.38 (assume @p148 (forall @t338 (=> @t209 (=> @t337 (=> @t302 (=> (forall @t336 (=> @t299 (=> @t335 @t334))) @t295)))))) % 3.11/3.38 (assume @p149 (forall @t332 (=> @t191 (=> @t331 (=> @t293 (=> (forall @t330 (=> @t290 (=> @t329 (=> (_ (_ tptp.ord_less_eq_set_nat @t287) @t43) @t328)))) @t286)))))) % 3.11/3.38 (assume @p150 (forall @t338 (=> @t209 (=> @t337 (=> @t302 (=> (forall @t336 (=> @t299 (=> @t335 (=> (_ (_ tptp.ord_le432112161lle_hf @t296) @t50) @t334)))) @t295)))))) % 3.11/3.38 (assume @p151 (_ (_ tptp.inj_on811196232lle_hf tptp.hF_Mirabelle_HF) (_ tptp.collec1758573718lle_hf tptp.finite586181922lle_hf))) % 3.11/3.38 (assume @p152 (forall @t23 (_ @t339 @t22))) % 3.11/3.38 (assume @p153 (forall @t342 (=> (forall @t223 (=> @t322 (_ @t196 @t118))) @t341))) % 3.11/3.38 (assume @p154 (forall @t27 (= (_ @t343 tptp.zero_zero_nat) (= @t25 tptp.zero_zero_nat)))) % 3.11/3.38 (assume @p155 (forall @t54 (= @t344 @t51))) % 3.11/3.38 (assume @p156 (forall @t54 (_ @t345 @t50))) % 3.11/3.38 (assume @p157 (forall @t171 (= (_ (_ tptp.ord_le432112161lle_hf @t93) @t118) (and @t167 @t341)))) % 3.11/3.38 (assume @p158 (forall (@list @t9 @t50 @t18) (= (= @t160 @t217) @t346))) % 3.11/3.38 (assume @p159 (forall (@list @t18 @t9 @t50) (= (= @t217 @t160) @t346))) % 3.11/3.38 (assume @p160 (= @t347 tptp.zero_zero_nat)) % 3.11/3.38 (assume @p161 (forall @t54 (=> @t348 @t326))) % 3.11/3.38 (assume @p162 (forall @t49 (=> @t349 @t324))) % 3.11/3.38 (assume @p163 (forall @t235 (=> @t353 (=> @t351 @t96)))) % 3.11/3.38 (assume @p164 (= @t360 (lambda @t357 (and @t356 @t355)))) % 3.11/3.38 (assume @p165 (forall (@list @t95 @t28 @t34) (=> @t353 (=> (_ @t361 @t95) (_ @t361 @t28))))) % 3.11/3.38 (assume @p166 (forall (@list @t362 @t28 @t95) (=> (forall @t365 (=> (_ (_ tptp.ord_less_eq_nat @t258) @t363) @t364)) (=> (forall @t365 (=> (_ (_ @t362 @t363) @t258) @t364)) (_ (_ @t362 @t28) @t95))))) % 3.11/3.38 (assume @p167 (forall @t75 (_ @t350 @t28))) % 3.11/3.38 (assume @p168 (forall @t371 (=> @t370 (=> @t369 @t367)))) % 3.11/3.38 (assume @p169 (forall @t216 (=> @t351 (=> @t353 @t96)))) % 3.11/3.38 (assume @p170 (forall @t373 (=> @t351 (=> @t219 @t372)))) % 3.11/3.38 (assume @p171 (forall @t373 (=> @t96 @t375))) % 3.11/3.38 (assume @p172 (= @t360 (lambda @t357 (and @t355 @t356)))) % 3.11/3.38 (assume @p173 (forall (@list @t141 @t22) (=> @t377 (= @t370 @t376)))) % 3.11/3.38 (assume @p174 (forall @t371 (=> (=> @t370 (not @t369)) (=> (=> @t377 (not @t367)) (=> (=> @t367 (not @t381)) (=> (=> @t381 (not @t377)) (=> (=> @t369 (not @t380)) (not (=> @t380 @t378))))))))) % 3.11/3.38 (assume @p175 (forall @t373 (=> @t351 @t375))) % 3.11/3.38 (assume @p176 (forall @t382 (=> @t378 @t377))) % 3.11/3.38 (assume @p177 (forall @t382 (=> @t376 @t370))) % 3.11/3.38 (assume @p178 (forall @t382 (or @t370 @t377))) % 3.11/3.38 (assume @p179 (forall @t382 (=> @t370 (=> @t377 @t376)))) % 3.11/3.38 (assume @p180 (= @t360 (lambda (@list @t45 @t383) (and (_ @t384 @t383) (_ (_ tptp.ord_less_eq_nat @t383) @t45))))) % 3.11/3.38 (assume @p181 (forall @t391 (=> @t351 (=> (= @t390 @t34) @t389)))) % 3.11/3.38 (assume @p182 (forall @t393 (=> (= @t28 @t390) @t392))) % 3.11/3.38 (assume @p183 (forall @t391 (=> @t351 (=> (_ (_ tptp.ord_less_eq_nat @t390) @t34) @t389)))) % 3.11/3.38 (assume @p184 (forall @t393 (=> (_ @t350 @t390) @t392))) % 3.11/3.38 (assume @p185 (forall @t229 (= @t394 (forall @t41 (=> @t60 (_ @t224 @t38)))))) % 3.11/3.38 (assume @p186 (forall @t229 (=> (forall @t228 (=> @t227 @t226)) @t394))) % 3.11/3.38 (assume @p187 (= tptp.ord_le432112161lle_hf (lambda @t396 (forall @t5 (=> (_ @t52 @t274) (_ @t52 @t395)))))) % 3.11/3.38 (assume @p188 (forall (@list @t50 @t118 @t17) (=> @t341 @t399))) % 3.11/3.38 (assume @p189 (forall (@list @t50 @t118 @t20) (=> @t341 (=> @t169 @t167)))) % 3.11/3.38 (assume @p190 (forall @t402 (=> @t401 (=> @t341 (=> (= @t325 @t400) @t159))))) % 3.11/3.38 (assume @p191 (forall @t406 (=> @t405 (=> @t404 (=> (= @t323 @t403) @t149))))) % 3.11/3.38 (assume @p192 (forall (@list @t50 @t25) (=> @t348 (exists @t139 (and (_ tptp.finite586181922lle_hf @t138) (= (_ tptp.finite1213132899lle_hf @t138) @t25) (_ (_ tptp.ord_le432112161lle_hf @t138) @t50)))))) % 3.11/3.38 (assume @p193 (forall (@list @t43 @t25) (=> @t349 (exists @t133 (and (_ tptp.finite_finite_nat @t132) (= (_ tptp.finite_card_nat @t132) @t25) (_ (_ tptp.ord_less_eq_set_nat @t132) @t43)))))) % 3.11/3.38 (assume @p194 (forall @t23 (_ @t407 @t22))) % 3.11/3.38 (assume @p195 (_ @t407 tptp.zero_zero_nat)) % 3.11/3.38 (assume @p196 (forall @t73 (_ @t345 @t71))) % 3.11/3.38 (assume @p197 (forall @t75 (_ (_ tptp.ord_less_eq_nat tptp.bot_bot_nat) @t28))) % 3.11/3.38 (assume @p198 (forall @t73 (= @t408 @t267))) % 3.11/3.38 (assume @p199 (forall @t75 (= @t410 @t409))) % 3.11/3.38 (assume @p200 (forall @t73 (=> @t408 @t267))) % 3.11/3.38 (assume @p201 (forall @t75 (=> @t410 @t409))) % 3.11/3.38 (assume @p202 (forall @t81 (=> @t251 (=> @t79 (exists @t309 (and @t416 (_ @t350 @t186) @t415)))))) % 3.11/3.38 (assume @p203 (forall @t81 (=> @t251 (=> @t79 (exists @t309 (and @t416 (_ @t387 @t28) @t417)))))) % 3.11/3.38 (assume @p204 (forall @t342 (=> @t341 (=> @t401 @t70)))) % 3.11/3.38 (assume @p205 (forall @t418 (=> @t404 (=> @t405 @t251)))) % 3.11/3.38 (assume @p206 (forall (@list @t316 @t419) (=> (_ (_ tptp.ord_le432112161lle_hf @t316) @t419) (=> @t319 (not (_ tptp.finite586181922lle_hf @t419)))))) % 3.11/3.38 (assume @p207 (forall (@list @t312 @t420) (=> (_ (_ tptp.ord_less_eq_set_nat @t312) @t420) (=> @t315 (not (_ tptp.finite_finite_nat @t420)))))) % 3.11/3.38 (assume @p208 (forall @t402 (=> @t401 (=> @t341 @t70)))) % 3.11/3.38 (assume @p209 (forall @t406 (=> @t405 (=> @t404 @t251)))) % 3.11/3.38 (assume @p210 (forall (@list @t422 @t421 @t9) (=> (_ (_ tptp.ord_le432112161lle_hf @t422) @t421) (_ (_ tptp.ord_le432112161lle_hf (_ @t130 @t422)) (_ @t130 @t421))))) % 3.11/3.38 (assume @p211 (forall @t171 (=> @t170 (= (_ @t340 @t165) @t341)))) % 3.11/3.38 (assume @p212 (forall (@list @t118 @t9) (_ @t423 @t173))) % 3.11/3.38 (assume @p213 (forall (@list @t50 @t118 @t18) (=> @t341 (_ @t340 @t119)))) % 3.11/3.38 (assume @p214 (forall @t49 (=> @t251 (=> @t241 (exists @t309 (and @t416 @t417)))))) % 3.11/3.38 (assume @p215 (forall @t49 (=> @t251 (=> @t241 (exists @t309 (and @t416 @t415)))))) % 3.11/3.38 (assume @p216 (forall (@list @t424 @t9) (= (_ @t425 @t131) (or (= @t424 tptp.bot_bo53200981lle_hf) (= @t424 @t131))))) % 3.11/3.38 (assume @p217 (forall @t426 (=> (_ @t340 @t311) (or @t51 (= @t50 @t311))))) % 3.11/3.38 (assume @p218 (forall @t49 (= @t324 (or @t44 @t349)))) % 3.11/3.38 (assume @p219 (forall @t54 (= @t326 (or @t51 @t348)))) % 3.11/3.38 (assume @p220 (forall (@list @t427) (_ @t428 tptp.bot_bo2093393035lle_hf))) % 3.11/3.38 (assume @p221 (forall (@list @t312 @t285 @t385) (=> @t314 (=> @t293 (=> (forall (@list @t186 @t429) (=> (_ tptp.finite_finite_nat @t429) (=> (forall @t431 (=> (_ (_ tptp.member_nat @t430) @t429) (_ (_ tptp.ord_less_eq_nat (_ @t385 @t430)) @t386))) (=> (_ @t285 @t429) (_ @t285 (_ @t188 @t429)))))) (_ @t285 @t312)))))) % 3.11/3.38 (assume @p222 (forall (@list @t316 @t59 @t433) (=> @t318 (=> @t302 (=> (forall (@list @t195 @t432) (=> (_ tptp.finite586181922lle_hf @t432) (=> (forall (@list @t434) (=> (_ (_ tptp.member1367349282lle_hf @t434) @t432) (_ (_ tptp.ord_less_eq_nat (_ @t433 @t434)) (_ @t433 @t195)))) (=> (_ @t59 @t432) (_ @t59 (_ @t200 @t432)))))) (_ @t59 @t316)))))) % 3.11/3.38 (assume @p223 (forall (@list @t427 @t36 @t113) (=> @t437 (=> (_ @t436 @t36) @t435)))) % 3.11/3.38 (assume @p224 (forall (@list @t427 @t113 @t36) (=> @t435 (=> @t439 @t437)))) % 3.11/3.38 (assume @p225 (forall (@list @t20 @t50 @t424) (=> @t169 (=> (_ @t425 @t50) (_ (_ tptp.ord_le432112161lle_hf (_ @t92 @t424)) @t50))))) % 3.11/3.38 (assume @p226 (forall @t54 (=> (forall @t223 (not @t322)) @t344))) % 3.11/3.38 (assume @p227 (forall @t75 (_ @t407 @t28))) % 3.11/3.38 (assume @p228 (forall @t27 (_ @t407 @t25))) % 3.11/3.38 (assume @p229 (forall @t75 (=> @t440 @t29))) % 3.11/3.38 (assume @p230 (forall @t75 (= @t440 @t29))) % 3.11/3.38 (assume @p231 (forall (@list @t202 @t441) (=> (forall (@list @t442) (=> (_ (_ tptp.ord_le432112161lle_hf @t442) @t202) (=> (_ tptp.finite586181922lle_hf @t442) (_ (_ tptp.ord_less_eq_nat (_ tptp.finite1213132899lle_hf @t442)) @t441)))) (and @t209 (_ (_ tptp.ord_less_eq_nat (_ tptp.finite1213132899lle_hf @t202)) @t441))))) % 3.11/3.38 (assume @p232 (forall (@list @t189 @t441) (=> (forall (@list @t443) (=> (_ (_ tptp.ord_less_eq_set_nat @t443) @t189) (=> (_ tptp.finite_finite_nat @t443) (_ (_ tptp.ord_less_eq_nat (_ tptp.finite_card_nat @t443)) @t441)))) (and @t191 (_ (_ tptp.ord_less_eq_nat (_ tptp.finite_card_nat @t189)) @t441))))) % 3.11/3.38 (assume @p233 (forall @t402 (=> @t401 (=> @t341 (=> (_ (_ tptp.ord_less_eq_nat @t400) @t325) @t159))))) % 3.11/3.38 (assume @p234 (forall @t406 (=> @t405 (=> @t404 (=> (_ (_ tptp.ord_less_eq_nat @t403) @t323) @t149))))) % 3.11/3.38 (assume @p235 (forall @t402 (=> @t401 (=> @t341 @t445)))) % 3.11/3.38 (assume @p236 (forall @t406 (=> @t405 (=> @t404 @t447)))) % 3.11/3.38 (assume @p237 (forall @t426 (=> @t70 (_ @t444 (_ tptp.finite1213132899lle_hf @t93))))) % 3.11/3.38 (assume @p238 (forall @t448 (=> @t251 (_ @t446 (_ tptp.finite_card_nat @t86))))) % 3.11/3.38 (assume @p239 (forall (@list @t36 @t450 @t427) (=> (forall @t228 (=> @t451 (= (_ @t450 @t449) @t177))) @t437))) % 3.11/3.38 (assume @p240 (forall @t455 (=> @t437 (=> (not @t454) (=> @t164 (=> @t453 (not @t452))))))) % 3.11/3.38 (assume @p241 (forall @t455 (=> @t437 (=> @t164 (=> @t453 (= @t452 @t454)))))) % 3.11/3.38 (assume @p242 (forall (@list @t36 @t427 @t456) (=> (forall @t256 (=> (_ (_ tptp.member1490636632lle_hf @t253) @t36) (= (_ @t427 @t253) (_ @t456 @t253)))) (= @t437 (_ (_ tptp.inj_on811196232lle_hf @t456) @t36))))) % 3.11/3.38 (assume @p243 (forall (@list @t36 @t427) (=> (forall (@list @t177 @t243) (=> @t451 (=> @t244 (=> (= @t449 (_ @t427 @t243)) (= @t177 @t243))))) @t437))) % 3.11/3.38 (assume @p244 (forall @t455 (=> @t437 (=> @t452 (=> @t164 (=> @t453 @t454)))))) % 3.11/3.38 (assume @p245 (forall (@list @t25 @t316) (=> (_ @t343 (_ tptp.finite1213132899lle_hf @t316)) (not (forall (@list @t457) (=> (_ (_ tptp.ord_le432112161lle_hf @t457) @t316) (=> (= (_ tptp.finite1213132899lle_hf @t457) @t25) (not (_ tptp.finite586181922lle_hf @t457))))))))) % 3.11/3.38 (assume @p246 (forall (@list @t25 @t312) (=> (_ @t343 (_ tptp.finite_card_nat @t312)) (not (forall (@list @t458) (=> (_ (_ tptp.ord_less_eq_set_nat @t458) @t312) (=> (= (_ tptp.finite_card_nat @t458) @t25) (not (_ tptp.finite_finite_nat @t458))))))))) % 3.11/3.38 (assume @p247 (forall (@list @t118 @t50 @t462) (=> @t401 (=> (forall @t265 (=> @t335 (exists (@list @t465) (and (_ (_ tptp.member1367349282lle_hf @t465) @t118) (_ (_ @t462 @t15) @t465))))) (=> (forall (@list @t460 @t459 @t14) (=> @t464 (=> @t463 (=> (_ (_ tptp.member1367349282lle_hf @t14) @t118) (=> (_ (_ @t462 @t460) @t14) (=> (_ (_ @t462 @t459) @t14) @t461)))))) @t445))))) % 3.11/3.38 (assume @p248 (forall (@list @t108 @t50 @t467) (=> @t405 (=> (forall @t265 (=> @t335 (exists (@list @t468) (and (_ (_ tptp.member_nat @t468) @t108) (_ (_ @t467 @t15) @t468))))) (=> (forall (@list @t460 @t459 @t363) (=> @t464 (=> @t463 (=> (_ (_ tptp.member_nat @t363) @t108) (=> (_ (_ @t467 @t460) @t363) (=> (_ (_ @t467 @t459) @t363) @t461)))))) @t466))))) % 3.11/3.38 (assume @p249 (forall (@list @t312 @t141 @t385) (=> @t314 (=> @t313 (=> (_ (_ tptp.member_nat @t141) @t312) (_ (_ tptp.ord_less_eq_nat (_ @t385 (_ (_ tptp.lattic1974000059at_nat @t385) @t312))) (_ @t385 @t141))))))) % 3.11/3.38 (assume @p250 (forall (@list @t316 @t16 @t433) (=> @t318 (=> @t317 (=> (_ (_ tptp.member1367349282lle_hf @t16) @t316) (_ (_ tptp.ord_less_eq_nat (_ @t433 (_ (_ tptp.lattic710307446hf_nat @t433) @t316))) (_ @t433 @t16))))))) % 3.11/3.38 (assume @p251 (forall (@list @t55 @t22 @t471) (=> (_ @t55 @t22) (=> (forall @t309 (=> @t472 (_ @t387 @t471))) (not (forall (@list @t469) (=> (_ @t55 @t469) (not (forall (@list @t470) (=> (_ @t55 @t470) (_ (_ tptp.ord_less_eq_nat @t470) @t469))))))))))) % 3.11/3.38 (assume @p252 (forall (@list @t55 @t473 @t95) (=> (_ @t55 @t473) (=> (forall @t246 (=> (_ @t55 @t245) (_ (_ tptp.ord_less_eq_nat @t245) @t95))) (exists @t309 (and @t472 (forall @t431 (=> (_ @t55 @t430) (_ (_ tptp.ord_less_eq_nat @t430) @t186))))))))) % 3.11/3.38 (assume @p253 (forall @t477 (or @t476 @t475))) % 3.11/3.38 (assume @p254 (forall @t477 (=> @t476 (=> @t475 @t478)))) % 3.11/3.38 (assume @p255 (forall @t477 (=> @t478 @t476))) % 3.11/3.38 (assume @p256 (forall (@list @t479 @t481 @t473) (=> (_ @t480 @t481) (=> (_ (_ tptp.ord_less_eq_nat @t481) @t473) (_ @t480 @t473))))) % 3.11/3.38 (assume @p257 (forall @t27 (_ @t343 @t25))) % 3.11/3.38 (assume @p258 (forall @t448 (=> @t251 (_ (_ tptp.ord_less_eq_nat (_ tptp.finite_card_nat (_ @t482 (_ @t85 tptp.bot_bot_set_nat)))) @t323)))) % 3.11/3.38 (assume @p259 (forall @t426 (=> @t70 (_ (_ tptp.ord_less_eq_nat (_ tptp.finite1213132899lle_hf @t484)) @t325)))) % 3.11/3.38 (assume @p260 (forall (@list @t36 @t118) (=> @t249 (=> @t401 (=> @t487 (exists (@list @t485) (and (_ (_ tptp.ord_le432112161lle_hf (_ (_ tptp.image_899003828lle_hf @t485) @t36)) @t118) (_ (_ tptp.inj_on811196232lle_hf @t485) @t36)))))))) % 3.11/3.38 (assume @p261 (forall @t342 (=> @t70 (=> @t401 (=> @t445 (exists (@list @t488) (and (_ (_ tptp.ord_le432112161lle_hf (_ (_ tptp.image_1743964010lle_hf @t488) @t50)) @t118) (_ (_ tptp.inj_on755450110lle_hf @t488) @t50)))))))) % 3.11/3.38 (assume @p262 (forall (@list @t50 @t108) (=> @t70 (=> @t405 (=> @t466 (exists (@list @t489) (and (_ (_ tptp.ord_less_eq_set_nat (_ (_ tptp.image_131453538hf_nat @t489) @t50)) @t108) (_ (_ tptp.inj_on1874279374hf_nat @t489) @t50)))))))) % 3.11/3.38 (assume @p263 (forall (@list @t43 @t118) (=> @t251 (=> @t401 (=> (_ @t446 @t400) (exists (@list @t490) (and (_ (_ tptp.ord_le432112161lle_hf (_ (_ tptp.image_246164834lle_hf @t490) @t43)) @t118) (_ (_ tptp.inj_on1988990670lle_hf @t490) @t43)))))))) % 3.11/3.38 (assume @p264 (forall @t418 (=> @t251 (=> @t405 (=> @t447 (exists (@list @t491) (and (_ (_ tptp.ord_less_eq_set_nat (_ (_ tptp.image_nat_nat @t491) @t43)) @t108) (_ (_ tptp.inj_on_nat_nat @t491) @t43)))))))) % 3.11/3.38 (assume @p265 (forall (@list @t427 @t36 @t118) (=> @t437 (=> (_ (_ tptp.ord_le432112161lle_hf @t493) @t118) (=> @t401 @t487))))) % 3.11/3.38 (assume @p266 (forall (@list @t18 @t494 @t20 @t50) (=> (= @t18 @t497) (=> @t169 (_ @t157 @t496))))) % 3.11/3.38 (assume @p267 (forall @t501 (=> @t398 (=> @t500 @t499)))) % 3.11/3.38 (assume @p268 (forall @t501 (= @t499 (and @t398 @t500)))) % 3.11/3.38 (assume @p269 (forall @t75 (= (_ @t502 @t28) tptp.zero_zero_nat))) % 3.11/3.38 (assume @p270 (forall @t75 (= (_ @t502 tptp.zero_zero_nat) @t28))) % 3.11/3.38 (assume @p271 (forall @t75 (= (_ (_ tptp.minus_minus_nat tptp.zero_zero_nat) @t28) tptp.zero_zero_nat))) % 3.11/3.38 (assume @p272 (forall (@list @t494) (= (_ @t495 tptp.bot_bo53200981lle_hf) tptp.bot_bo53200981lle_hf))) % 3.11/3.38 (assume @p273 (forall @t503 (= (= tptp.bot_bo53200981lle_hf @t496) @t51))) % 3.11/3.38 (assume @p274 (forall @t503 (= (= @t496 tptp.bot_bo53200981lle_hf) @t51))) % 3.11/3.38 (assume @p275 (forall (@list @t202 @t504) (=> @t209 (_ tptp.finite586181922lle_hf (_ (_ tptp.image_1743964010lle_hf @t504) @t202))))) % 3.11/3.38 (assume @p276 (forall (@list @t202 @t505) (=> @t209 (_ tptp.finite_finite_nat (_ (_ tptp.image_131453538hf_nat @t505) @t202))))) % 3.11/3.38 (assume @p277 (forall (@list @t189 @t506) (=> @t191 (_ tptp.finite586181922lle_hf (_ (_ tptp.image_246164834lle_hf @t506) @t189))))) % 3.11/3.38 (assume @p278 (forall (@list @t189 @t507) (=> @t191 (_ tptp.finite_finite_nat (_ (_ tptp.image_nat_nat @t507) @t189))))) % 3.11/3.38 (assume @p279 (forall (@list @t494 @t9 @t118) (= (_ @t495 @t173) (_ (_ tptp.insert9649339lle_hf @t508) (_ @t495 @t118))))) % 3.11/3.38 (assume @p280 (forall (@list @t20 @t50 @t494) (=> @t169 (= (_ (_ tptp.insert9649339lle_hf @t497) @t496) @t496)))) % 3.11/3.38 (assume @p281 (forall @t54 (= (_ @t483 tptp.bot_bo53200981lle_hf) @t50))) % 3.11/3.38 (assume @p282 (forall @t54 (= (_ (_ tptp.minus_1450406810lle_hf tptp.bot_bo53200981lle_hf) @t50) tptp.bot_bo53200981lle_hf))) % 3.11/3.38 (assume @p283 (forall @t54 (= (_ @t483 @t50) tptp.bot_bo53200981lle_hf))) % 3.11/3.38 (assume @p284 (forall @t342 (=> @t70 @t509))) % 3.11/3.38 (assume @p285 (forall @t418 (=> @t251 @t510))) % 3.11/3.38 (assume @p286 (forall @t402 (=> @t401 (= @t509 @t70)))) % 3.11/3.38 (assume @p287 (forall @t406 (=> @t405 (= @t510 @t251)))) % 3.11/3.38 (assume @p288 (forall @t171 (=> @t170 (= (_ @t483 @t165) @t498)))) % 3.11/3.38 (assume @p289 (forall (@list @t20 @t118 @t50) (=> @t167 (= (_ @t511 @t118) @t498)))) % 3.11/3.38 (assume @p290 (forall @t342 (= (= @t498 tptp.bot_bo53200981lle_hf) @t341))) % 3.11/3.38 (assume @p291 (forall @t140 (= @t513 @t160))) % 3.11/3.38 (assume @p292 (forall @t515 (= (_ tptp.finite586181922lle_hf @t514) @t509))) % 3.11/3.38 (assume @p293 (forall (@list @t43 @t28 @t108) (= (_ tptp.finite_finite_nat (_ @t482 @t172)) @t510))) % 3.11/3.38 (assume @p294 (forall (@list @t427 @t71 @t36) (= (_ @t428 @t155) (and @t437 (not (_ @t517 (_ @t492 (_ @t516 @t127)))))))) % 3.11/3.38 (assume @p295 (forall (@list @t494 @t9 @t50) (= (_ @t519 @t160) (and @t520 (not (_ @t518 (_ @t495 @t512))))))) % 3.11/3.38 (assume @p296 (forall @t526 (=> @t525 (=> (_ (_ tptp.ord_le2016357975lle_hf @t522) @t523) (=> @t524 (= (_ @t492 @t522) (_ (_ tptp.minus_1450406810lle_hf @t493) @t521))))))) % 3.11/3.38 (assume @p297 (forall (@list @t50 @t494 @t118) (=> (forall @t223 (=> @t322 (_ (_ tptp.member1367349282lle_hf (_ @t494 @t195)) @t118))) (_ (_ tptp.ord_le432112161lle_hf @t496) @t118)))) % 3.11/3.38 (assume @p298 (forall (@list @t50 @t118 @t494) (=> @t70 (=> @t527 @t401)))) % 3.11/3.38 (assume @p299 (forall (@list @t50 @t108 @t433) (=> @t70 (=> @t531 @t405)))) % 3.11/3.38 (assume @p300 (forall (@list @t43 @t118 @t532) (=> @t251 (=> @t535 @t401)))) % 3.11/3.38 (assume @p301 (forall (@list @t43 @t108 @t385) (=> @t251 (=> @t538 @t405)))) % 3.11/3.38 (assume @p302 (forall (@list @t118 @t494 @t50) (=> @t401 (=> @t527 (exists @t542 (and @t541 @t540 (= @t118 (_ @t495 @t539)))))))) % 3.11/3.38 (assume @p303 (forall (@list @t118 @t532 @t43) (=> @t401 (=> @t535 (exists @t546 (and @t545 @t544 (= @t118 (_ @t533 @t543)))))))) % 3.11/3.38 (assume @p304 (forall (@list @t108 @t433 @t50) (=> @t405 (=> @t531 (exists @t542 (and @t541 @t540 (= @t108 (_ @t528 @t539)))))))) % 3.11/3.38 (assume @p305 (forall (@list @t108 @t385 @t43) (=> @t405 (=> @t538 (exists @t546 (and @t545 @t544 (= @t108 (_ @t536 @t543)))))))) % 3.11/3.38 (assume @p306 (forall @t554 (= (exists @t551 (and @t550 @t553 @t552)) (exists @t551 (and @t550 @t549 @t547))))) % 3.11/3.38 (assume @p307 (forall @t562 (= (exists @t551 (and @t550 @t561 @t552)) (exists @t560 (and @t559 @t558 @t556))))) % 3.11/3.38 (assume @p308 (forall @t566 (= (exists @t560 (and @t559 @t565 @t564)) (exists @t551 (and @t550 @t549 @t563))))) % 3.11/3.38 (assume @p309 (forall @t569 (= (exists @t560 (and @t559 @t568 @t564)) (exists @t560 (and @t559 @t558 @t567))))) % 3.11/3.38 (assume @p310 (forall @t554 (= (forall @t551 (=> (and @t550 @t553) @t552)) (forall @t551 (=> @t570 @t547))))) % 3.11/3.38 (assume @p311 (forall @t562 (= (forall @t551 (=> (and @t550 @t561) @t552)) (forall @t560 (=> @t571 @t556))))) % 3.11/3.38 (assume @p312 (forall @t566 (= (forall @t560 (=> (and @t559 @t565) @t564)) (forall @t551 (=> @t570 @t563))))) % 3.11/3.38 (assume @p313 (forall @t569 (= (forall @t560 (=> (and @t559 @t568) @t564)) (forall @t560 (=> @t571 @t567))))) % 3.11/3.38 (assume @p314 (forall @t573 (=> @t572 (=> @t437 @t249)))) % 3.11/3.38 (assume @p315 (forall @t503 (=> @t574 (=> @t520 @t70)))) % 3.11/3.38 (assume @p316 (forall @t577 (=> @t576 (=> @t575 @t251)))) % 3.11/3.38 (assume @p317 (forall @t580 (=> @t579 (=> @t578 @t70)))) % 3.11/3.38 (assume @p318 (forall @t583 (=> @t582 (=> @t581 @t251)))) % 3.11/3.38 (assume @p319 (forall @t573 (=> @t437 (= @t572 @t249)))) % 3.11/3.38 (assume @p320 (forall @t503 (=> @t520 (= @t574 @t70)))) % 3.11/3.38 (assume @p321 (forall @t577 (=> @t575 (= @t576 @t251)))) % 3.11/3.38 (assume @p322 (forall @t580 (=> @t578 (= @t579 @t70)))) % 3.11/3.38 (assume @p323 (forall @t583 (=> @t581 (= @t582 @t251)))) % 3.11/3.38 (assume @p324 (forall @t526 (=> @t525 (=> (_ @t438 @t523) (=> @t524 (= (= @t493 @t521) @t154)))))) % 3.11/3.38 (assume @p325 (forall (@list @t427 @t113 @t71 @t36) (=> @t435 (=> @t116 (=> @t439 (= (_ @t517 @t493) @t77)))))) % 3.11/3.38 (assume @p326 (forall (@list @t494 @t118 @t9 @t50) (=> (_ @t519 @t118) (=> @t121 (=> @t341 (= (_ @t518 @t496) @t82)))))) % 3.11/3.38 (assume @p327 (forall (@list @t427 @t36 @t20 @t118) (=> @t437 (=> @t168 (=> (= @t165 @t493) (not (forall (@list @t585 @t584) (=> (not (_ (_ tptp.member1490636632lle_hf @t585) @t584)) (=> (= @t36 (_ (_ tptp.insert1636143089lle_hf @t585) @t584)) (=> (= @t20 (_ @t427 @t585)) (not (= @t118 (_ @t492 @t584))))))))))))) % 3.11/3.38 (assume @p328 (forall (@list @t494 @t50 @t20 @t118) (=> @t520 (=> @t168 (=> (= @t165 @t496) (not (forall (@list @t587 @t586) (=> (not (_ (_ tptp.member1367349282lle_hf @t587) @t586)) (=> (= @t50 (_ (_ tptp.insert9649339lle_hf @t587) @t586)) (=> (= @t20 (_ @t494 @t587)) (not (= @t118 (_ @t495 @t586))))))))))))) % 3.11/3.38 (assume @p329 (forall @t573 (=> @t437 (= (_ tptp.finite1213132899lle_hf @t493) @t486)))) % 3.11/3.38 (assume @p330 (forall @t94 (=> @t170 (= (_ @t511 @t311) @t50)))) % 3.11/3.38 (assume @p331 (forall @t515 (= @t514 (_ (_ tptp.minus_1450406810lle_hf @t512) @t118)))) % 3.11/3.38 (assume @p332 (forall @t140 (=> @t82 (= @t513 @t50)))) % 3.11/3.38 (assume @p333 (forall @t515 (= @t514 (_ (_ tptp.minus_1450406810lle_hf @t498) @t131)))) % 3.11/3.38 (assume @p334 (forall (@list @t50 @t118 @t20 @t422) (= (_ @t340 (_ @t588 (_ @t92 @t422))) (and (_ @t340 (_ @t588 @t422)) @t170)))) % 3.11/3.38 (assume @p335 (forall (@list @t113 @t20 @t50) (=> (forall @t542 (=> (_ (_ tptp.member1490636632lle_hf @t539) @t113) (not (_ @t166 @t539)))) (= (_ (_ tptp.member1490636632lle_hf @t50) (_ (_ tptp.image_1514960916lle_hf @t92) @t113)) (and @t169 (_ (_ tptp.member1490636632lle_hf @t484) @t113)))))) % 3.11/3.38 (assume @p336 (forall @t501 (=> @t499 (not @t399)))) % 3.11/3.38 (assume @p337 (forall @t501 (=> @t499 @t398))) % 3.11/3.38 (assume @p338 @t593) % 3.11/3.38 (assume @p339 true) % 3.11/3.38 (step @p340 (= tptp.hF_Mirabelle_hmem @t595) :rule refl :args (@t595)) % 3.11/3.38 (step @p341 (= tptp.bot_bo1263054448e_hf_o @t596) :rule refl :args (@t596)) % 3.11/3.38 (step @p342 (= tptp.bot_bo554042810e_hf_o @t597) :rule refl :args (@t597)) % 3.11/3.38 (step @p343 (= tptp.hF_Mirabelle_hinsert @t598) :rule refl :args (@t598)) % 3.11/3.38 (step @p344 (= tptp.is_sin1448700567lle_hf @t599) :rule refl :args (@t599)) % 3.11/3.38 (step @p345 (= tptp.is_emp566801209lle_hf @t600) :rule refl :args (@t600)) % 3.11/3.38 (step @p346 (= tptp.ord_le432112161lle_hf @t603) :rule refl :args (@t603)) % 3.11/3.38 (step @p347 (= tptp.inj_on811196232lle_hf @t606) :rule refl :args (@t606)) % 3.11/3.38 (step @p348 (= tptp.finite_finite_nat @t609) :rule refl :args (@t609)) % 3.11/3.38 (step @p349 :rule eq-symm :args (@t613 @t614)) % 3.11/3.38 (step @p350 :rule refl :args ((tptp.hF_Mirabelle_HF @t615))) % 3.11/3.38 (step @p351 :rule refl :args (@t611)) % 3.11/3.38 (step @p352 :rule cong :premises (@p351) :args (@t614)) % 3.11/3.38 (step @p353 :rule trans :premises (@p352 @p350)) % 3.11/3.38 (step @p354 :rule refl :args (tptp.hF_Mirabelle_HF)) % 3.11/3.38 (step @p355 :rule ho_cong :premises (@p354 @p351)) % 3.11/3.38 (step @p356 :rule cong :premises (@p355 @p353) :args ((= (_ tptp.hF_Mirabelle_HF @t611) @t614))) % 3.11/3.38 (step @p357 :rule symm :premises (@p356)) % 3.11/3.38 (step @p358 :rule refl :args ((_ tptp.hF_Mirabelle_HF @t615))) % 3.11/3.38 (step @p359 :rule eq_resolve :premises (@p358 @p357)) % 3.11/3.38 (step @p360 :rule refl :args (@t615)) % 3.11/3.38 (step @p361 :rule cong :premises (@p360 @p351) :args ((= @t615 @t611))) % 3.11/3.38 (step @p362 :rule symm :premises (@p361)) % 3.11/3.38 (step @p363 :rule eq_resolve :premises (@p360 @p362)) % 3.11/3.38 (step @p364 :rule eq-refl :args (@t596)) % 3.11/3.38 (step @p365 :rule skolem_intro :args (@t610)) % 3.11/3.38 (step @p366 :rule refl :args (@t596)) % 3.11/3.38 (step @p367 :rule cong :premises (@p366 @p365) :args ((= @t596 @t610))) % 3.11/3.38 (step @p368 :rule trans :premises (@p367 @p364)) % 3.11/3.38 (step @p369 :rule true_elim :premises (@p368)) % 3.11/3.38 (step @p370 :rule refl :args (tptp.collec2046588256lle_hf)) % 3.11/3.38 (step @p371 :rule ho_cong :premises (@p370 @p369)) % 3.11/3.38 (step @p372 :rule trans :premises (@p371 @p363)) % 3.11/3.38 (step @p373 :rule refl :args (tptp.hF_Mirabelle_HF)) % 3.11/3.38 (step @p374 :rule ho_cong :premises (@p373 @p372)) % 3.11/3.38 (step @p375 :rule trans :premises (@p374 @p359)) % 3.11/3.38 (step @p376 :rule refl :args ((tptp.hF_Mirabelle_Abs_hf @t616))) % 3.11/3.38 (step @p377 :rule refl :args ((tptp.finite1213132899lle_hf @t615))) % 3.11/3.38 (step @p378 :rule cong :premises (@p351) :args (@t612)) % 3.11/3.38 (step @p379 :rule trans :premises (@p378 @p377)) % 3.11/3.38 (step @p380 :rule cong :premises (@p379) :args (@t613)) % 3.11/3.38 (step @p381 :rule trans :premises (@p380 @p376)) % 3.11/3.38 (step @p382 :rule refl :args (tptp.hF_Mirabelle_Abs_hf)) % 3.11/3.38 (step @p383 :rule ho_cong :premises (@p382 @p379)) % 3.11/3.38 (step @p384 :rule cong :premises (@p383 @p381) :args ((= (_ tptp.hF_Mirabelle_Abs_hf @t612) @t613))) % 3.11/3.38 (step @p385 :rule symm :premises (@p384)) % 3.11/3.38 (step @p386 :rule refl :args ((_ tptp.hF_Mirabelle_Abs_hf @t616))) % 3.11/3.38 (step @p387 :rule eq_resolve :premises (@p386 @p385)) % 3.11/3.38 (step @p388 :rule refl :args (tptp.finite1213132899lle_hf)) % 3.11/3.38 (step @p389 :rule ho_cong :premises (@p388 @p351)) % 3.11/3.38 (step @p390 :rule cong :premises (@p389 @p379) :args ((= (_ tptp.finite1213132899lle_hf @t611) @t612))) % 3.11/3.38 (step @p391 :rule symm :premises (@p390)) % 3.11/3.38 (step @p392 :rule refl :args (@t616)) % 3.11/3.38 (step @p393 :rule eq_resolve :premises (@p392 @p391)) % 3.11/3.38 (step @p394 :rule refl :args (tptp.finite1213132899lle_hf)) % 3.11/3.38 (step @p395 :rule ho_cong :premises (@p394 @p372)) % 3.11/3.38 (step @p396 :rule trans :premises (@p395 @p393)) % 3.11/3.38 (step @p397 :rule refl :args (tptp.hF_Mirabelle_Abs_hf)) % 3.11/3.38 (step @p398 :rule ho_cong :premises (@p397 @p396)) % 3.11/3.38 (step @p399 :rule trans :premises (@p398 @p387)) % 3.11/3.38 (step @p400 :rule cong :premises (@p399 @p375) :args ((= @t619 (_ tptp.hF_Mirabelle_HF @t617)))) % 3.11/3.38 (step @p401 :rule trans :premises (@p400 @p349)) % 3.11/3.38 (step @p402 :rule ho_cong :premises (@p370 @p341)) % 3.11/3.38 (step @p403 :rule refl :args (tptp.bot_bo53200981lle_hf)) % 3.11/3.38 (step @p404 :rule cong :premises (@p403 @p402) :args (@t213)) % 3.11/3.38 (step @p405 :rule eq_resolve :premises (@p78 @p404)) % 3.11/3.38 (step @p406 :rule ho_cong :premises (@p373 @p405)) % 3.11/3.38 (step @p407 :rule ho_cong :premises (@p394 @p405)) % 3.11/3.38 (step @p408 :rule symm :premises (@p102)) % 3.11/3.38 (step @p409 :rule cong :premises (@p408 @p407) :args ((= tptp.zero_zero_nat @t347))) % 3.11/3.38 (step @p410 :rule symm :premises (@p160)) % 3.11/3.38 (step @p411 :rule eq_resolve :premises (@p410 @p409)) % 3.11/3.38 (step @p412 :rule trans :premises (@p408 @p411)) % 3.11/3.38 (step @p413 :rule ho_cong :premises (@p397 @p412)) % 3.11/3.38 (step @p414 :rule symm :premises (@p7)) % 3.11/3.38 (step @p415 :rule trans :premises (@p414 @p413)) % 3.11/3.38 (step @p416 :rule cong :premises (@p415 @p406) :args (@t24)) % 3.11/3.38 (step @p417 :rule trans :premises (@p416 @p401)) % 3.11/3.38 (step @p418 :rule eq_resolve :premises (@p8 @p417)) % 3.11/3.38 (step @p419 :rule refl :args (tptp.z)) % 3.11/3.38 (step @p420 :rule cong :premises (@p419 @p399) :args (@t620)) % 3.11/3.38 (step @p421 :rule refl :args (@t623)) % 3.11/3.38 (step @p422 :rule cong :premises (@p421 @p420) :args (@t624)) % 3.11/3.38 (step @p423 :rule cong :premises (@p422) :args ((not @t624))) % 3.11/3.38 (step @p424 :rule eq-symm :args (@t619 tptp.z)) % 3.11/3.38 (step @p425 :rule cong :premises (@p421 @p424) :args ((= @t623 @t625))) % 3.11/3.38 (step @p426 :rule eq-symm :args (@t625 @t623)) % 3.11/3.38 (step @p427 :rule trans :premises (@p426 @p425)) % 3.11/3.38 (step @p428 :rule cong :premises (@p427) :args ((not (= @t625 @t623)))) % 3.11/3.38 (step @p429 :rule cong :premises (@p415 @p419) :args (@t626)) % 3.11/3.38 (step @p430 :rule cong :premises (@p429 @p421) :args (@t627)) % 3.11/3.38 (step @p431 :rule cong :premises (@p430) :args ((not @t627))) % 3.11/3.38 (step @p432 :rule trans :premises (@p431 @p428)) % 3.11/3.38 (step @p433 :rule refl :args ((tptp.member1367349282lle_hf @t2 @t628))) % 3.11/3.38 (step @p434 :rule refl :args (@t621)) % 3.11/3.38 (step @p435 :rule refl :args (@t2)) % 3.11/3.38 (step @p436 :rule cong :premises (@p435 @p434) :args (@t622)) % 3.11/3.38 (step @p437 :rule trans :premises (@p436 @p433)) % 3.11/3.38 (step @p438 :rule refl :args (@t52)) % 3.11/3.38 (step @p439 :rule ho_cong :premises (@p438 @p434)) % 3.11/3.38 (step @p440 :rule cong :premises (@p439 @p437) :args ((= (_ @t52 @t621) @t622))) % 3.11/3.38 (step @p441 :rule symm :premises (@p440)) % 3.11/3.38 (step @p442 :rule refl :args (@t629)) % 3.11/3.38 (step @p443 :rule eq_resolve :premises (@p442 @p441)) % 3.11/3.38 (step @p444 :rule refl :args (@t628)) % 3.11/3.38 (step @p445 :rule cong :premises (@p444 @p434) :args ((= @t628 @t621))) % 3.11/3.38 (step @p446 :rule symm :premises (@p445)) % 3.11/3.38 (step @p447 :rule eq_resolve :premises (@p444 @p446)) % 3.11/3.38 (step @p448 :rule ho_cong :premises (@p438 @p447)) % 3.11/3.38 (step @p449 :rule trans :premises (@p448 @p443)) % 3.11/3.38 (step @p450 :rule cong :premises (@p449) :args (@t630)) % 3.11/3.38 (step @p451 :rule cong :premises (@p450) :args ((forall @t5 @t630))) % 3.11/3.38 (step @p452 :rule beta-reduce :args ((= (_ @t632 tptp.z) @t629))) % 3.11/3.38 (step @p453 :rule beta-reduce :args ((= @t633 @t632))) % 3.11/3.38 (step @p454 :rule ho_cong :premises (@p453 @p419)) % 3.11/3.38 (step @p455 :rule trans :premises (@p454 @p452)) % 3.11/3.38 (step @p456 :rule cong :premises (@p455) :args (@t634)) % 3.11/3.38 (step @p457 :rule cong :premises (@p456) :args (@t635)) % 3.11/3.38 (step @p458 :rule trans :premises (@p457 @p451)) % 3.11/3.38 (step @p459 :rule eq-symm :args (tptp.z tptp.zero_z189798548lle_hf)) % 3.11/3.38 (step @p460 :rule cong :premises (@p459 @p458) :args (@t636)) % 3.11/3.38 (step @p461 :rule cong :premises (@p460) :args ((not @t636))) % 3.11/3.38 (step @p462 :rule refl :args (@t2)) % 3.11/3.38 (step @p463 :rule ho_cong :premises (@p340 @p462)) % 3.11/3.38 (step @p464 :rule ho_cong :premises (@p463 @p419)) % 3.11/3.38 (step @p465 :rule cong :premises (@p464) :args (@t589)) % 3.11/3.38 (step @p466 :rule cong :premises (@p465) :args (@t590)) % 3.11/3.38 (step @p467 :rule refl :args (@t591)) % 3.11/3.38 (step @p468 :rule cong :premises (@p467 @p466) :args (@t592)) % 3.11/3.38 (step @p469 :rule cong :premises (@p468) :args (@t593)) % 3.11/3.38 (step @p470 :rule trans :premises (@p469 @p461)) % 3.11/3.38 (step @p471 :rule trans :premises (@p470 @p432 @p423)) % 3.11/3.38 (step @p472 :rule eq_resolve :premises (@p338 @p471)) % 3.11/3.38 (step @p473 :rule not_equiv_elim2 :premises (@p472)) % 3.11/3.38 (step @p474 :rule refl :args ((tptp.hF_Mirabelle_HF @t30))) % 3.11/3.38 (step @p475 :rule refl :args (@t637)) % 3.11/3.38 (step @p476 :rule cong :premises (@p475) :args (@t638)) % 3.11/3.38 (step @p477 :rule trans :premises (@p476 @p474)) % 3.11/3.38 (step @p478 :rule ho_cong :premises (@p354 @p475)) % 3.11/3.38 (step @p479 :rule cong :premises (@p478 @p477) :args ((= (_ tptp.hF_Mirabelle_HF @t637) @t638))) % 3.11/3.38 (step @p480 :rule symm :premises (@p479)) % 3.11/3.38 (step @p481 :rule refl :args (@t31)) % 3.11/3.38 (step @p482 :rule eq_resolve :premises (@p481 @p480)) % 3.11/3.38 (step @p483 :rule refl :args (@t30)) % 3.11/3.38 (step @p484 :rule cong :premises (@p483 @p475) :args ((= @t30 @t637))) % 3.11/3.38 (step @p485 :rule symm :premises (@p484)) % 3.11/3.38 (step @p486 :rule eq_resolve :premises (@p483 @p485)) % 3.11/3.38 (step @p487 :rule ho_cong :premises (@p354 @p486)) % 3.11/3.38 (step @p488 :rule trans :premises (@p487 @p482)) % 3.11/3.38 (step @p489 :rule refl :args (@t9)) % 3.11/3.38 (step @p490 :rule cong :premises (@p489 @p488) :args (@t639)) % 3.11/3.38 (step @p491 :rule cong :premises (@p490) :args ((forall @t12 @t639))) % 3.11/3.38 (step @p492 :rule eq-symm :args (@t31 @t9)) % 3.11/3.38 (step @p493 :rule cong :premises (@p492) :args (@t32)) % 3.11/3.38 (step @p494 :rule trans :premises (@p493 @p491)) % 3.11/3.38 (step @p495 :rule eq_resolve :premises (@p13 @p494)) % 3.11/3.38 (step @p496 :rule instantiate :premises (@p495) :args (@t640)) % 3.11/3.38 (step @p497 :rule refl :args (@t642)) % 3.11/3.38 (step @p498 :rule refl :args (@t645)) % 3.11/3.38 (step @p499 :rule bool-double-not-elim :args (@t646)) % 3.11/3.38 (step @p500 :rule refl :args (@t648)) % 3.11/3.38 (step @p501 :rule nary_cong :premises (@p500 @p499 @p498 @p497) :args ((or @t648 (not @t649) @t645 @t642))) % 3.11/3.38 (assume-push @p928 @t647) % 3.11/3.38 (assume-push @p929 @t650) % 3.11/3.38 (assume-push @p930 @t644) % 3.11/3.38 (assume-push @p931 @t649) % 3.11/3.38 (step @p506 :rule evaluate :args ((= false true))) % 3.11/3.38 (step @p507 :rule symm :premises (@p929)) % 3.11/3.38 (step @p508 :rule trans :premises (@p496 @p507)) % 3.11/3.38 (step @p509 :rule trans :premises (@p508 @p418)) % 3.11/3.38 (step @p510 :rule true_intro :premises (@p509)) % 3.11/3.38 (step @p511 :rule false_intro :premises (@p931)) % 3.11/3.38 (step @p512 :rule symm :premises (@p511)) % 3.11/3.38 (step @p513 :rule trans :premises (@p512 @p510)) % 3.11/3.38 (step @p514 false :rule eq_resolve :premises (@p513 @p506)) % 3.11/3.38 (step-pop @p932 :rule scope :premises (@p514)) % 3.11/3.38 (step-pop @p933 :rule scope :premises (@p932)) % 3.11/3.38 (step-pop @p934 :rule scope :premises (@p933)) % 3.11/3.38 (step-pop @p935 :rule scope :premises (@p934)) % 3.11/3.38 (step @p515 :rule process_scope :premises (@p935) :args (false)) % 3.11/3.38 (assume-push @p936 @t647) % 3.11/3.38 (assume-push @p937 @t649) % 3.11/3.38 (assume-push @p938 @t644) % 3.11/3.38 (assume-push @p939 @t641) % 3.11/3.38 (assume-push @p940 @t641) % 3.11/3.38 (step @p525 :rule symm :premises (@p939)) % 3.11/3.38 (step @p526 :rule cong :premises (@p525) :args (@t614)) % 3.11/3.38 (step-pop @p941 :rule scope :premises (@p526)) % 3.11/3.38 (step @p527 :rule process_scope :premises (@p941) :args (@t650)) % 3.11/3.38 (step @p529 :rule modus_ponens :premises (@p939 @p527)) % 3.11/3.38 (step @p530 :rule and_intro :premises (@p418 @p529 @p496 @p937)) % 3.11/3.38 (step-pop @p942 :rule scope :premises (@p530)) % 3.11/3.38 (step-pop @p943 :rule scope :premises (@p942)) % 3.11/3.38 (step-pop @p944 :rule scope :premises (@p943)) % 3.11/3.38 (step-pop @p945 :rule scope :premises (@p944)) % 3.11/3.38 (step @p531 :rule process_scope :premises (@p945) :args (@t651)) % 3.11/3.38 (step @p536 :rule implies_elim :premises (@p531)) % 3.11/3.38 (step @p537 :rule resolution :premises (@p536 @p515) :args (true @t651)) % 3.11/3.38 (step @p538 :rule not_and :premises (@p537)) % 3.11/3.38 (step @p539 :rule eq_resolve :premises (@p538 @p501)) % 3.11/3.38 (step @p540 :rule reordering :premises (@p539) :args ((or @t646 @t648 @t645 @t642))) % 3.11/3.38 (step @p541 :rule refl :args ((tptp.finite586181922lle_hf @t30))) % 3.11/3.38 (step @p542 :rule cong :premises (@p475) :args (@t652)) % 3.11/3.38 (step @p543 :rule trans :premises (@p542 @p541)) % 3.11/3.38 (step @p544 :rule refl :args (tptp.finite586181922lle_hf)) % 3.11/3.38 (step @p545 :rule ho_cong :premises (@p544 @p475)) % 3.11/3.38 (step @p546 :rule cong :premises (@p545 @p543) :args ((= (_ tptp.finite586181922lle_hf @t637) @t652))) % 3.11/3.38 (step @p547 :rule symm :premises (@p546)) % 3.11/3.38 (step @p548 :rule refl :args (@t239)) % 3.11/3.38 (step @p549 :rule eq_resolve :premises (@p548 @p547)) % 3.11/3.38 (step @p550 :rule ho_cong :premises (@p544 @p486)) % 3.11/3.38 (step @p551 :rule trans :premises (@p550 @p549)) % 3.11/3.38 (step @p552 :rule cong :premises (@p551) :args (@t240)) % 3.11/3.38 (step @p553 :rule eq_resolve :premises (@p103 @p552)) % 3.11/3.38 (step @p554 :rule instantiate :premises (@p553) :args (@t640)) % 3.11/3.38 (step @p555 :rule refl :args (@t657)) % 3.11/3.38 (step @p556 :rule refl :args (@t658)) % 3.11/3.38 (step @p557 :rule refl :args (@t617)) % 3.11/3.38 (step @p558 :rule cong :premises (@p557 @p556) :args ((= @t617 @t658))) % 3.11/3.38 (step @p559 :rule symm :premises (@p558)) % 3.11/3.38 (step @p560 :rule eq_resolve :premises (@p557 @p559)) % 3.11/3.38 (step @p561 :rule refl :args (@t202)) % 3.11/3.38 (step @p562 :rule cong :premises (@p561 @p560) :args (@t659)) % 3.11/3.38 (step @p563 :rule refl :args (@t661)) % 3.11/3.38 (step @p564 :rule nary_cong :premises (@p563 @p562 @p555) :args (@t662)) % 3.11/3.38 (step @p565 :rule cong :premises (@p564) :args ((forall @t211 @t662))) % 3.11/3.38 (step @p566 :rule refl :args (@t657)) % 3.11/3.38 (step @p567 :rule eq-symm :args (@t617 @t202)) % 3.11/3.38 (step @p568 :rule refl :args (@t661)) % 3.11/3.38 (step @p569 :rule nary_cong :premises (@p568 @p567 @p566) :args (@t663)) % 3.11/3.38 (step @p570 :rule cong :premises (@p569) :args ((forall @t211 @t663))) % 3.11/3.38 (step @p571 :rule trans :premises (@p570 @p565)) % 3.11/3.38 (step @p572 :rule refl :args (@t202)) % 3.11/3.38 (step @p573 :rule cong :premises (@p405 @p572) :args (@t664)) % 3.11/3.38 (step @p574 :rule nary_cong :premises (@p568 @p573 @p566) :args (@t665)) % 3.11/3.38 (step @p575 :rule cong :premises (@p574) :args ((forall @t211 @t665))) % 3.11/3.38 (step @p576 :rule trans :premises (@p575 @p571)) % 3.11/3.38 (step @p577 :rule refl :args (@t664)) % 3.11/3.38 (step @p578 :rule refl :args (@t660)) % 3.11/3.38 (step @p579 :rule refl :args (@t209)) % 3.11/3.38 (step @p580 :rule cong :premises (@p579 @p578) :args ((= @t209 @t660))) % 3.11/3.38 (step @p581 :rule symm :premises (@p580)) % 3.11/3.38 (step @p582 :rule eq_resolve :premises (@p579 @p581)) % 3.11/3.38 (step @p583 :rule cong :premises (@p582) :args (@t666)) % 3.11/3.38 (step @p584 :rule nary_cong :premises (@p583 @p577 @p555) :args (@t667)) % 3.11/3.38 (step @p585 :rule cong :premises (@p584) :args ((forall @t211 @t667))) % 3.11/3.38 (step @p586 :rule aci_norm :args ((= (or @t666 (or @t664 @t657)) @t667))) % 3.11/3.38 (step @p587 :rule bool-double-not-elim :args (@t664)) % 3.11/3.38 (step @p588 :rule nary_cong :premises (@p587 @p555) :args ((or (not @t668) @t657))) % 3.11/3.38 (step @p589 :rule bool-impl-elim :args (@t668 @t657)) % 3.11/3.38 (step @p590 :rule trans :premises (@p589 @p588)) % 3.11/3.38 (step @p591 :rule refl :args (@t666)) % 3.11/3.38 (step @p592 :rule nary_cong :premises (@p591 @p590) :args ((or @t666 @t669))) % 3.11/3.38 (step @p593 :rule trans :premises (@p592 @p586)) % 3.11/3.38 (step @p594 :rule bool-impl-elim :args (@t209 @t669)) % 3.11/3.38 (step @p595 :rule trans :premises (@p594 @p593)) % 3.11/3.38 (step @p596 :rule cong :premises (@p595) :args ((forall @t211 (=> @t209 @t669)))) % 3.11/3.38 (step @p597 :rule trans :premises (@p596 @p585)) % 3.11/3.38 (step @p598 :rule refl :args (@t653)) % 3.11/3.38 (step @p599 :rule refl :args (@t193)) % 3.11/3.38 (step @p600 :rule cong :premises (@p599 @p598) :args ((= @t193 @t653))) % 3.11/3.38 (step @p601 :rule symm :premises (@p600)) % 3.11/3.38 (step @p602 :rule eq_resolve :premises (@p599 @p601)) % 3.11/3.38 (step @p603 :rule cong :premises (@p602) :args (@t194)) % 3.11/3.38 (step @p604 :rule refl :args (@t655)) % 3.11/3.38 (step @p605 :rule refl :args (@t197)) % 3.11/3.38 (step @p606 :rule cong :premises (@p605 @p604) :args ((= @t197 @t655))) % 3.11/3.38 (step @p607 :rule symm :premises (@p606)) % 3.11/3.38 (step @p608 :rule eq_resolve :premises (@p605 @p607)) % 3.11/3.38 (step @p609 :rule refl :args (@t656)) % 3.11/3.38 (step @p610 :rule refl :args (@t201)) % 3.11/3.38 (step @p611 :rule cong :premises (@p610 @p609) :args ((= @t201 @t656))) % 3.11/3.38 (step @p612 :rule symm :premises (@p611)) % 3.11/3.38 (step @p613 :rule eq_resolve :premises (@p610 @p612)) % 3.11/3.38 (step @p614 :rule cong :premises (@p561 @p613) :args (@t203)) % 3.11/3.38 (step @p615 :rule cong :premises (@p614) :args (@t670)) % 3.11/3.38 (step @p616 :rule nary_cong :premises (@p615 @p608 @p603) :args (@t671)) % 3.11/3.38 (step @p617 :rule cong :premises (@p616) :args ((forall @t204 @t671))) % 3.11/3.38 (step @p618 :rule aci_norm :args ((= (or @t670 (or @t197 @t194)) @t671))) % 3.11/3.38 (step @p619 :rule refl :args (@t194)) % 3.11/3.38 (step @p620 :rule bool-double-not-elim :args (@t197)) % 3.11/3.38 (step @p621 :rule nary_cong :premises (@p620 @p619) :args ((or (not @t198) @t194))) % 3.11/3.38 (step @p622 :rule bool-impl-elim :args (@t198 @t194)) % 3.11/3.38 (step @p623 :rule trans :premises (@p622 @p621)) % 3.11/3.38 (step @p624 :rule refl :args (@t670)) % 3.11/3.38 (step @p625 :rule nary_cong :premises (@p624 @p623) :args ((or @t670 @t199))) % 3.11/3.38 (step @p626 :rule trans :premises (@p625 @p618)) % 3.11/3.38 (step @p627 :rule bool-impl-elim :args (@t203 @t199)) % 3.11/3.38 (step @p628 :rule trans :premises (@p627 @p626)) % 3.11/3.38 (step @p629 :rule cong :premises (@p628) :args (@t205)) % 3.11/3.38 (step @p630 :rule trans :premises (@p629 @p617)) % 3.11/3.38 (step @p631 :rule cong :premises (@p630) :args (@t206)) % 3.11/3.38 (step @p632 :rule eq-symm :args (@t202 tptp.bot_bo53200981lle_hf)) % 3.11/3.38 (step @p633 :rule cong :premises (@p632) :args (@t207)) % 3.11/3.38 (step @p634 :rule cong :premises (@p633 @p631) :args (@t208)) % 3.11/3.38 (step @p635 :rule refl :args (@t209)) % 3.11/3.38 (step @p636 :rule cong :premises (@p635 @p634) :args (@t210)) % 3.11/3.38 (step @p637 :rule cong :premises (@p636) :args (@t212)) % 3.11/3.38 (step @p638 :rule trans :premises (@p637 @p597)) % 3.11/3.38 (step @p639 :rule trans :premises (@p638 @p576)) % 3.11/3.38 (step @p640 :rule eq_resolve :premises (@p75 @p639)) % 3.11/3.38 (step @p641 :rule refl :args (@t673)) % 3.11/3.38 (step @p642 :rule cong :premises (@p369) :args (@t658)) % 3.11/3.38 (step @p643 :rule refl :args (@t621)) % 3.11/3.38 (step @p644 :rule cong :premises (@p643 @p642) :args (@t674)) % 3.11/3.38 (step @p645 :rule refl :args (@t676)) % 3.11/3.38 (step @p646 :rule nary_cong :premises (@p645 @p644 @p641) :args (@t677)) % 3.11/3.38 (step @p647 :rule refl :args (@t678)) % 3.11/3.38 (step @p648 :rule cong :premises (@p647 @p646) :args ((=> @t678 @t677))) % 3.11/3.38 (step @p649 :rule refl :args (@t654)) % 3.11/3.38 (step @p650 :rule refl :args (@t655)) % 3.11/3.38 (step @p651 :rule eq-symm :args (@t621 @t656)) % 3.11/3.38 (step @p652 :rule cong :premises (@p651) :args (@t679)) % 3.11/3.38 (step @p653 :rule nary_cong :premises (@p652 @p650 @p649) :args (@t680)) % 3.11/3.38 (step @p654 :rule cong :premises (@p653) :args (@t681)) % 3.11/3.38 (step @p655 :rule cong :premises (@p654) :args (@t682)) % 3.11/3.38 (step @p656 :rule refl :args (@t674)) % 3.11/3.38 (step @p657 :rule nary_cong :premises (@p645 @p656 @p655) :args (@t683)) % 3.11/3.38 (step @p658 :rule cong :premises (@p647 @p657) :args ((=> @t678 @t683))) % 3.11/3.38 (assume-push @p946 @t678) % 3.11/3.38 (step @p660 :rule instantiate :premises (@p640) :args ((@list @t621))) % 3.11/3.38 (step-pop @p947 :rule scope :premises (@p660)) % 3.11/3.38 (step @p661 :rule process_scope :premises (@p947) :args (@t683)) % 3.11/3.38 (step @p663 :rule eq_resolve :premises (@p661 @p658)) % 3.11/3.38 (step @p664 :rule eq_resolve :premises (@p663 @p648)) % 3.11/3.38 (step @p665 :rule implies_elim :premises (@p664)) % 3.11/3.38 (step @p666 :rule chain_m_resolution :premises (@p665 @p640) :args (@t684 @t685 (@list @t678))) % 3.11/3.38 (step @p667 :rule cnf_or_pos :args (@t684)) % 3.11/3.38 (step @p668 :rule reordering :premises (@p667) :args ((or @t676 @t673 @t641 (not @t684)))) % 3.11/3.38 (step @p669 :rule refl :args (@t694)) % 3.11/3.38 (step @p670 :rule bool-double-not-elim :args (@t672)) % 3.11/3.38 (step @p671 :rule nary_cong :premises (@p670 @p669) :args ((or (not @t673) @t694))) % 3.11/3.38 (step @p672 :rule refl :args (@t687)) % 3.11/3.38 (step @p673 :rule refl :args (@t689)) % 3.11/3.38 (step @p674 :rule eq-symm :args (@t690 @t621)) % 3.11/3.38 (step @p675 :rule cong :premises (@p674) :args (@t695)) % 3.11/3.38 (step @p676 :rule nary_cong :premises (@p675 @p673 @p672) :args (@t696)) % 3.11/3.38 (step @p677 :rule cong :premises (@p676) :args (@t697)) % 3.11/3.38 (step @p678 :rule cong :premises (@p641 @p677) :args ((=> @t673 @t697))) % 3.11/3.38 (assume-push @p948 @t673) % 3.11/3.38 (step @p680 :rule skolemize :premises (@p948)) % 3.11/3.38 (step-pop @p949 :rule scope :premises (@p680)) % 3.11/3.38 (step @p681 :rule process_scope :premises (@p949) :args (@t697)) % 3.11/3.38 (step @p683 :rule eq_resolve :premises (@p681 @p678)) % 3.11/3.38 (step @p684 :rule implies_elim :premises (@p683)) % 3.11/3.38 (step @p685 :rule eq_resolve :premises (@p684 @p671)) % 3.11/3.38 (step @p686 :rule bool-double-not-elim :args (@t691)) % 3.11/3.38 (step @p687 :rule refl :args (@t693)) % 3.11/3.38 (step @p688 :rule nary_cong :premises (@p687 @p686) :args ((or @t693 (not @t692)))) % 3.11/3.38 (step @p689 :rule cnf_or_neg :args (@t693 0)) % 3.11/3.38 (step @p690 :rule eq_resolve :premises (@p689 @p688)) % 3.11/3.38 (step @p691 :rule reordering :premises (@p690) :args ((or @t691 @t693))) % 3.11/3.38 (assume-push @p950 @t623) % 3.11/3.38 (step @p693 :rule instantiate :premises (@p950) :args ((@list @t688))) % 3.11/3.38 (step-pop @p951 :rule scope :premises (@p693)) % 3.11/3.38 (step @p694 :rule process_scope :premises (@p951) :args (@t699)) % 3.11/3.38 (step @p696 :rule implies_elim :premises (@p694)) % 3.11/3.38 (step @p697 :rule aci_norm :args ((= (or false @t703) @t703))) % 3.11/3.38 (step @p698 :rule refl :args (@t703)) % 3.11/3.38 (step @p699 :rule evaluate :args ((not true))) % 3.11/3.38 (step @p700 :rule eq-refl :args (@t701)) % 3.11/3.38 (step @p701 :rule cong :premises (@p700) :args (@t704)) % 3.11/3.38 (step @p702 :rule trans :premises (@p701 @p699)) % 3.11/3.38 (step @p703 :rule nary_cong :premises (@p702 @p698) :args (@t705)) % 3.11/3.38 (step @p704 :rule trans :premises (@p703 @p697)) % 3.11/3.38 (step @p705 :rule cong :premises (@p704) :args ((forall @t706 @t705))) % 3.11/3.38 (step @p706 :rule quant-var-elim-eq :args ((= (forall @t711 @t710) @t705))) % 3.11/3.38 (step @p707 :rule aci_norm :args ((= @t712 @t710))) % 3.11/3.38 (step @p708 :rule cong :premises (@p707) :args (@t713)) % 3.11/3.38 (step @p709 :rule trans :premises (@p708 @p706)) % 3.11/3.38 (step @p710 :rule cong :premises (@p709) :args (@t714)) % 3.11/3.38 (step @p711 :rule quant-merge-prenex :args ((= @t714 @t715))) % 3.11/3.38 (step @p712 :rule symm :premises (@p711)) % 3.11/3.38 (step @p713 :rule quant_var_reordering :args ((= @t716 @t715))) % 3.11/3.38 (step @p714 :rule trans :premises (@p713 @p712 @p710)) % 3.11/3.38 (step @p715 :rule trans :premises (@p714 @p705)) % 3.11/3.38 (step @p716 :rule refl :args (@t720)) % 3.11/3.38 (step @p717 :rule nary_cong :premises (@p716 @p715) :args ((and @t720 @t716))) % 3.11/3.38 (step @p718 :rule alpha_equiv :args (@t724 @t725 (@list @t707 @t700 @t701))) % 3.11/3.38 (step @p719 :rule alpha_equiv :args (@t729 @t725 (@list @t719 @t717 @t718))) % 3.11/3.38 (step @p720 :rule nary_cong :premises (@p719 @p718) :args (@t730)) % 3.11/3.38 (step @p721 :rule quant-miniscope-and :args ((= (forall @t124 (and @t728 @t723)) @t730))) % 3.11/3.38 (step @p722 :rule trans :premises (@p721 @p720)) % 3.11/3.38 (step @p723 :rule trans :premises (@p722 @p717)) % 3.11/3.38 (step @p724 :rule bool-or-and-distrib :args (@t727 @t158 true @t722 false)) % 3.11/3.38 (step @p725 :rule cong :premises (@p724) :args ((forall @t124 (or (and @t727 @t158) @t722)))) % 3.11/3.38 (step @p726 :rule trans :premises (@p725 @p723)) % 3.11/3.38 (step @p727 :rule refl :args ((tptp.member1367349282lle_hf @t9 @t119))) % 3.11/3.38 (step @p728 :rule refl :args (@t721)) % 3.11/3.38 (step @p729 :rule cong :premises (@p489 @p728) :args (@t722)) % 3.11/3.38 (step @p730 :rule trans :premises (@p729 @p727)) % 3.11/3.38 (step @p731 :rule refl :args (@t76)) % 3.11/3.38 (step @p732 :rule ho_cong :premises (@p731 @p728)) % 3.11/3.38 (step @p733 :rule cong :premises (@p732 @p730) :args ((= (_ @t76 @t721) @t722))) % 3.11/3.38 (step @p734 :rule symm :premises (@p733)) % 3.11/3.38 (step @p735 :rule refl :args (@t120)) % 3.11/3.38 (step @p736 :rule eq_resolve :premises (@p735 @p734)) % 3.11/3.38 (step @p737 :rule refl :args (@t119)) % 3.11/3.38 (step @p738 :rule cong :premises (@p737 @p728) :args ((= @t119 @t721))) % 3.11/3.38 (step @p739 :rule symm :premises (@p738)) % 3.11/3.38 (step @p740 :rule eq_resolve :premises (@p737 @p739)) % 3.11/3.38 (step @p741 :rule ho_cong :premises (@p731 @p740)) % 3.11/3.38 (step @p742 :rule trans :premises (@p741 @p736)) % 3.11/3.38 (step @p743 :rule refl :args (@t158)) % 3.11/3.38 (step @p744 :rule refl :args (@t726)) % 3.11/3.38 (step @p745 :rule refl :args (@t121)) % 3.11/3.38 (step @p746 :rule cong :premises (@p745 @p744) :args ((= @t121 @t726))) % 3.11/3.38 (step @p747 :rule symm :premises (@p746)) % 3.11/3.38 (step @p748 :rule eq_resolve :premises (@p745 @p747)) % 3.11/3.38 (step @p749 :rule cong :premises (@p748) :args (@t122)) % 3.11/3.38 (step @p750 :rule nary_cong :premises (@p749 @p743) :args (@t731)) % 3.11/3.38 (step @p751 :rule nary_cong :premises (@p750 @p742) :args (@t732)) % 3.11/3.38 (step @p752 :rule cong :premises (@p751) :args ((forall @t124 @t732))) % 3.11/3.38 (step @p753 :rule trans :premises (@p752 @p726)) % 3.11/3.38 (step @p754 :rule bool-implies-de-morgan :args (@t122 @t19)) % 3.11/3.38 (step @p755 :rule nary_cong :premises (@p754 @p735) :args ((or (not @t123) @t120))) % 3.11/3.38 (step @p756 :rule bool-impl-elim :args (@t123 @t120)) % 3.11/3.38 (step @p757 :rule trans :premises (@p756 @p755)) % 3.11/3.38 (step @p758 :rule cong :premises (@p757) :args (@t125)) % 3.11/3.38 (step @p759 :rule trans :premises (@p758 @p753)) % 3.11/3.38 (step @p760 :rule eq_resolve :premises (@p42 @p759)) % 3.11/3.38 (step @p761 :rule and_elim :premises (@p760) :args (1)) % 3.11/3.38 (step @p762 :rule instantiate :premises (@p761) :args ((@list @t686 @t688))) % 3.11/3.38 (step @p763 :rule bool-double-not-elim :args (@t698)) % 3.11/3.38 (step @p764 :rule refl :args (@t734)) % 3.11/3.38 (step @p765 :rule refl :args (@t692)) % 3.11/3.38 (step @p766 :rule nary_cong :premises (@p765 @p764 @p763) :args ((or @t692 @t734 (not @t699)))) % 3.11/3.38 (assume-push @p952 @t699) % 3.11/3.38 (assume-push @p953 @t691) % 3.11/3.38 (assume-push @p954 @t733) % 3.11/3.38 (step @p770 :rule evaluate :args (@t735)) % 3.11/3.38 (step @p771 :rule false_intro :premises (@p952)) % 3.11/3.38 (step @p772 :rule symm :premises (@p953)) % 3.11/3.38 (step @p773 :rule refl :args (@t688)) % 3.11/3.38 (step @p774 :rule cong :premises (@p773 @p772) :args (@t733)) % 3.11/3.38 (step @p775 :rule true_intro :premises (@p762)) % 3.11/3.38 (step @p776 :rule symm :premises (@p775)) % 3.11/3.38 (step @p777 :rule trans :premises (@p776 @p774 @p771)) % 3.11/3.38 (step @p778 false :rule eq_resolve :premises (@p777 @p770)) % 3.11/3.38 (step-pop @p955 :rule scope :premises (@p778)) % 3.11/3.38 (step-pop @p956 :rule scope :premises (@p955)) % 3.11/3.38 (step-pop @p957 :rule scope :premises (@p956)) % 3.11/3.38 (step @p779 :rule process_scope :premises (@p957) :args (false)) % 3.11/3.38 (assume-push @p958 @t691) % 3.11/3.38 (assume-push @p959 @t733) % 3.11/3.38 (assume-push @p960 @t699) % 3.11/3.38 (step @p786 :rule and_intro :premises (@p960 @p958 @p762)) % 3.11/3.38 (step-pop @p961 :rule scope :premises (@p786)) % 3.11/3.38 (step-pop @p962 :rule scope :premises (@p961)) % 3.11/3.38 (step-pop @p963 :rule scope :premises (@p962)) % 3.11/3.38 (step @p787 :rule process_scope :premises (@p963) :args (@t736)) % 3.11/3.38 (step @p791 :rule implies_elim :premises (@p787)) % 3.11/3.38 (step @p792 :rule resolution :premises (@p791 @p779) :args (true @t736)) % 3.11/3.38 (step @p793 :rule not_and :premises (@p792)) % 3.11/3.38 (step @p794 :rule eq_resolve :premises (@p793 @p766)) % 3.11/3.38 (step @p795 :rule chain_m_resolution :premises (@p794 @p762 @p696 @p691 @p685 @p668 @p666 @p554 @p540 @p496 @p418 @p473) :args (@t737 (@list false true false true true false false true false false true) (@list @t733 @t698 @t691 @t693 @t672 @t684 @t675 @t641 @t644 @t647 @t646))) % 3.11/3.38 (step @p796 :rule not_equiv_elim1 :premises (@p472)) % 3.11/3.38 (step @p797 :rule chain_m_resolution :premises (@p796 @p795) :args (@t646 @t738 @t739)) % 3.11/3.38 (step @p798 :rule refl :args (@t741)) % 3.11/3.38 (step @p799 :rule bool-double-not-elim :args (@t623)) % 3.11/3.38 (step @p800 :rule nary_cong :premises (@p799 @p798) :args ((or (not @t737) @t741))) % 3.11/3.38 (step @p801 :rule bool-double-not-elim :args (@t741)) % 3.11/3.38 (step @p802 :rule refl :args (@t737)) % 3.11/3.38 (step @p803 :rule cong :premises (@p802 @p801) :args ((=> @t737 @t743))) % 3.11/3.38 (assume-push @p964 @t737) % 3.11/3.38 (step @p805 :rule skolemize :premises (@p964)) % 3.11/3.38 (step-pop @p965 :rule scope :premises (@p805)) % 3.11/3.38 (step @p806 :rule process_scope :premises (@p965) :args (@t743)) % 3.11/3.38 (step @p808 :rule eq_resolve :premises (@p806 @p803)) % 3.11/3.38 (step @p809 :rule implies_elim :premises (@p808)) % 3.11/3.38 (step @p810 :rule eq_resolve :premises (@p809 @p800)) % 3.11/3.38 (step @p811 :rule chain_m_resolution :premises (@p810 @p795) :args (@t741 @t738 @t739)) % 3.11/3.38 (step @p812 :rule refl :args ((tptp.hF_Mirabelle_Abs_hf @t618))) % 3.11/3.38 (step @p813 :rule refl :args ((tptp.finite1213132899lle_hf @t617))) % 3.11/3.38 (step @p814 :rule cong :premises (@p556) :args (@t744)) % 3.11/3.38 (step @p815 :rule trans :premises (@p814 @p813)) % 3.11/3.38 (step @p816 :rule cong :premises (@p815) :args (@t745)) % 3.11/3.38 (step @p817 :rule trans :premises (@p816 @p812)) % 3.11/3.38 (step @p818 :rule ho_cong :premises (@p382 @p815)) % 3.11/3.38 (step @p819 :rule cong :premises (@p818 @p817) :args ((= (_ tptp.hF_Mirabelle_Abs_hf @t744) @t745))) % 3.11/3.38 (step @p820 :rule symm :premises (@p819)) % 3.11/3.38 (step @p821 :rule refl :args (@t619)) % 3.11/3.38 (step @p822 :rule eq_resolve :premises (@p821 @p820)) % 3.11/3.38 (step @p823 :rule ho_cong :premises (@p388 @p556)) % 3.11/3.38 (step @p824 :rule cong :premises (@p823 @p815) :args ((= (_ tptp.finite1213132899lle_hf @t658) @t744))) % 3.11/3.38 (step @p825 :rule symm :premises (@p824)) % 3.11/3.38 (step @p826 :rule refl :args (@t618)) % 3.11/3.38 (step @p827 :rule eq_resolve :premises (@p826 @p825)) % 3.11/3.38 (step @p828 :rule ho_cong :premises (@p388 @p560)) % 3.11/3.38 (step @p829 :rule trans :premises (@p828 @p827)) % 3.11/3.38 (step @p830 :rule ho_cong :premises (@p382 @p829)) % 3.11/3.38 (step @p831 :rule trans :premises (@p830 @p822)) % 3.11/3.38 (step @p832 :rule cong :premises (@p831) :args (@t746)) % 3.11/3.38 (step @p833 :rule cong :premises (@p489 @p832) :args (@t747)) % 3.11/3.38 (step @p834 :rule cong :premises (@p833) :args (@t748)) % 3.11/3.38 (step @p835 :rule cong :premises (@p834) :args ((forall @t12 @t748))) % 3.11/3.38 (step @p836 :rule cong :premises (@p415) :args (@t749)) % 3.11/3.38 (step @p837 :rule refl :args (@t9)) % 3.11/3.38 (step @p838 :rule cong :premises (@p837 @p836) :args (@t750)) % 3.11/3.38 (step @p839 :rule cong :premises (@p838) :args (@t751)) % 3.11/3.38 (step @p840 :rule cong :premises (@p839) :args ((forall @t12 @t751))) % 3.11/3.38 (step @p841 :rule trans :premises (@p840 @p835)) % 3.11/3.38 (step @p842 :rule refl :args ((tptp.member1367349282lle_hf @t9 @t752))) % 3.11/3.38 (step @p843 :rule refl :args (@t749)) % 3.11/3.38 (step @p844 :rule cong :premises (@p489 @p843) :args (@t750)) % 3.11/3.38 (step @p845 :rule trans :premises (@p844 @p842)) % 3.11/3.38 (step @p846 :rule ho_cong :premises (@p731 @p843)) % 3.11/3.38 (step @p847 :rule cong :premises (@p846 @p845) :args ((= (_ @t76 @t749) @t750))) % 3.11/3.38 (step @p848 :rule symm :premises (@p847)) % 3.11/3.38 (step @p849 :rule refl :args (@t753)) % 3.11/3.38 (step @p850 :rule eq_resolve :premises (@p849 @p848)) % 3.11/3.38 (step @p851 :rule refl :args (@t752)) % 3.11/3.38 (step @p852 :rule cong :premises (@p851 @p843) :args ((= @t752 @t749))) % 3.11/3.38 (step @p853 :rule symm :premises (@p852)) % 3.11/3.38 (step @p854 :rule eq_resolve :premises (@p851 @p853)) % 3.11/3.38 (step @p855 :rule ho_cong :premises (@p731 @p854)) % 3.11/3.38 (step @p856 :rule trans :premises (@p855 @p850)) % 3.11/3.38 (step @p857 :rule cong :premises (@p856) :args (@t754)) % 3.11/3.38 (step @p858 :rule cong :premises (@p857) :args ((forall @t12 @t754))) % 3.11/3.38 (step @p859 :rule beta-reduce :args ((= (_ @t755 tptp.zero_z189798548lle_hf) @t753))) % 3.11/3.38 (step @p860 :rule refl :args (tptp.zero_z189798548lle_hf)) % 3.11/3.38 (step @p861 :rule beta-reduce :args ((= @t756 @t755))) % 3.11/3.38 (step @p862 :rule ho_cong :premises (@p861 @p860)) % 3.11/3.38 (step @p863 :rule trans :premises (@p862 @p859)) % 3.11/3.38 (step @p864 :rule cong :premises (@p863) :args (@t757)) % 3.11/3.38 (step @p865 :rule cong :premises (@p864) :args ((forall @t12 @t757))) % 3.11/3.38 (step @p866 :rule trans :premises (@p865 @p858)) % 3.11/3.38 (step @p867 :rule ho_cong :premises (@p340 @p837)) % 3.11/3.38 (step @p868 :rule ho_cong :premises (@p867 @p860)) % 3.11/3.38 (step @p869 :rule cong :premises (@p868) :args (@t11)) % 3.11/3.38 (step @p870 :rule cong :premises (@p869) :args (@t13)) % 3.11/3.38 (step @p871 :rule trans :premises (@p870 @p866)) % 3.11/3.38 (step @p872 :rule trans :premises (@p871 @p841)) % 3.11/3.38 (step @p873 :rule eq_resolve :premises (@p2 @p872)) % 3.11/3.38 (step @p874 :rule cong :premises (@p642) :args (@t744)) % 3.11/3.38 (step @p875 :rule cong :premises (@p874) :args (@t745)) % 3.11/3.38 (step @p876 :rule cong :premises (@p875) :args (@t758)) % 3.11/3.38 (step @p877 :rule refl :args (@t740)) % 3.11/3.38 (step @p878 :rule cong :premises (@p877 @p876) :args (@t759)) % 3.11/3.38 (step @p879 :rule cong :premises (@p878) :args (@t760)) % 3.11/3.38 (step @p880 :rule refl :args (@t761)) % 3.11/3.38 (step @p881 :rule cong :premises (@p880 @p879) :args ((=> @t761 @t760))) % 3.11/3.38 (assume-push @p966 @t761) % 3.11/3.38 (step @p883 :rule instantiate :premises (@p873) :args ((@list @t740))) % 3.11/3.38 (step-pop @p967 :rule scope :premises (@p883)) % 3.11/3.38 (step @p884 :rule process_scope :premises (@p967) :args (@t760)) % 3.11/3.38 (step @p886 :rule eq_resolve :premises (@p884 @p881)) % 3.11/3.38 (step @p887 :rule implies_elim :premises (@p886)) % 3.11/3.38 (step @p888 :rule chain_m_resolution :premises (@p887 @p873) :args (@t763 @t685 (@list @t761))) % 3.11/3.38 (step @p889 :rule bool-double-not-elim :args (@t762)) % 3.11/3.38 (step @p890 :rule refl :args (@t742)) % 3.11/3.38 (step @p891 :rule refl :args (@t649)) % 3.11/3.38 (step @p892 :rule nary_cong :premises (@p500 @p891 @p890 @p889) :args ((or @t648 @t649 @t742 (not @t763)))) % 3.11/3.38 (assume-push @p968 @t763) % 3.11/3.38 (assume-push @p969 @t647) % 3.11/3.38 (assume-push @p970 @t646) % 3.11/3.38 (assume-push @p971 @t741) % 3.11/3.38 (step @p770 :rule evaluate :args (@t735)) % 3.11/3.38 (step @p897 :rule false_intro :premises (@p888)) % 3.11/3.38 (step @p898 :rule cong :premises (@p418) :args ((tptp.hF_Mirabelle_hfset @t614))) % 3.11/3.38 (step @p899 :rule symm :premises (@p418)) % 3.11/3.38 (step @p900 :rule trans :premises (@p970 @p899)) % 3.11/3.38 (step @p901 :rule cong :premises (@p900) :args (@t621)) % 3.11/3.38 (step @p902 :rule trans :premises (@p901 @p898)) % 3.11/3.38 (step @p903 :rule cong :premises (@p877 @p902) :args (@t741)) % 3.11/3.39 (step @p904 :rule true_intro :premises (@p971)) % 3.11/3.39 (step @p905 :rule symm :premises (@p904)) % 3.11/3.39 (step @p906 :rule trans :premises (@p905 @p903 @p897)) % 3.11/3.39 (step @p907 false :rule eq_resolve :premises (@p906 @p770)) % 3.11/3.39 (step-pop @p972 :rule scope :premises (@p907)) % 3.11/3.39 (step-pop @p973 :rule scope :premises (@p972)) % 3.11/3.39 (step-pop @p974 :rule scope :premises (@p973)) % 3.11/3.39 (step-pop @p975 :rule scope :premises (@p974)) % 3.11/3.39 (step @p908 :rule process_scope :premises (@p975) :args (false)) % 3.11/3.39 (assume-push @p976 @t647) % 3.11/3.39 (assume-push @p977 @t646) % 3.11/3.39 (assume-push @p978 @t741) % 3.11/3.39 (assume-push @p979 @t763) % 3.11/3.39 (step @p917 :rule and_intro :premises (@p888 @p418 @p977 @p978)) % 3.11/3.39 (step-pop @p980 :rule scope :premises (@p917)) % 3.11/3.39 (step-pop @p981 :rule scope :premises (@p980)) % 3.11/3.39 (step-pop @p982 :rule scope :premises (@p981)) % 3.11/3.39 (step-pop @p983 :rule scope :premises (@p982)) % 3.11/3.39 (step @p918 :rule process_scope :premises (@p983) :args (@t764)) % 3.11/3.39 (step @p923 :rule implies_elim :premises (@p918)) % 3.11/3.39 (step @p924 :rule resolution :premises (@p923 @p908) :args (true @t764)) % 3.11/3.39 (step @p925 :rule not_and :premises (@p924)) % 3.11/3.39 (step @p926 :rule eq_resolve :premises (@p925 @p892)) % 3.11/3.39 (step @p927 false :rule chain_m_resolution :premises (@p926 @p888 @p811 @p797 @p418) :args (false (@list true false false false) (@list @t762 @t741 @t646 @t647))) % 3.11/3.39 ) % 3.11/3.39 % SZS output end Proof % 3.11/3.39 % cvc5 exiting %------------------------------------------------------------------------------