%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP134^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 : n014.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:25:09 AM UTC 2026 % Result : Theorem 4.62s 4.88s % Output : Proof 4.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP134^1 : TPTP v9.2.1. Released v7.5.0. % 0.12/0.14 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.17/0.34 % Computer : n014.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:15:43 EDT 2026 % 0.17/0.34 % CPUTime : % 0.39/0.61 %----Proving TH0 % 4.62/4.88 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 90s... % 4.62/4.88 % SZS status Theorem % 4.62/4.88 % SZS output start Proof % 4.62/4.88 ( % 4.62/4.88 (declare-sort tptp.nat 0) % 4.62/4.88 (declare-sort tptp.set_nat_nat 0) % 4.62/4.88 (declare-sort tptp.set_set_nat_nat 0) % 4.62/4.88 (declare-sort tptp.set_se1657353at_nat 0) % 4.62/4.88 (declare-sort tptp.set_set_nat_nat_nat2 0) % 4.62/4.88 (declare-sort tptp.set_set_nat_nat_nat 0) % 4.62/4.88 (declare-sort tptp.set_set_nat 0) % 4.62/4.88 (declare-sort tptp.set_na1201295426at_nat 0) % 4.62/4.88 (declare-sort tptp.set_na1064332610at_nat 0) % 4.62/4.88 (declare-sort tptp.set_nat_nat_nat_nat5 0) % 4.62/4.88 (declare-sort tptp.set_nat_nat_nat_nat4 0) % 4.62/4.88 (declare-sort tptp.set_nat_nat_nat_nat2 0) % 4.62/4.88 (declare-sort tptp.set_nat_nat_nat2 0) % 4.62/4.88 (declare-sort tptp.set_nat_nat_nat 0) % 4.62/4.88 (declare-sort tptp.set_nat 0) % 4.62/4.88 (declare-sort tptp.set_nat_nat_nat_nat3 0) % 4.62/4.88 (declare-sort tptp.set_nat_nat_nat_nat 0) % 4.62/4.88 (declare-const tptp.plus_plus_nat (-> tptp.nat tptp.nat tptp.nat)) % 4.62/4.88 (declare-const tptp.member_nat (-> tptp.nat tptp.set_nat Bool)) % 4.62/4.88 (declare-const tptp.member_nat_nat (-> (-> tptp.nat tptp.nat) tptp.set_nat_nat Bool)) % 4.62/4.88 (declare-const tptp.collect_set_nat (-> (-> tptp.set_nat Bool) tptp.set_set_nat)) % 4.62/4.88 (declare-const tptp.finite2045569477at_nat (-> tptp.set_nat_nat_nat Bool)) % 4.62/4.88 (declare-const tptp.ord_le940807492at_nat (-> tptp.set_nat_nat_nat tptp.set_nat_nat_nat Bool)) % 4.62/4.88 (declare-const tptp.collec617280953at_nat (-> (-> tptp.set_nat_nat_nat Bool) tptp.set_set_nat_nat_nat)) % 4.62/4.88 (declare-const tptp.finite1440337093at_nat (-> tptp.set_nat_nat_nat2 Bool)) % 4.62/4.88 (declare-const tptp.ord_le633272388at_nat (-> tptp.set_nat_nat_nat2 tptp.set_nat_nat_nat2 Bool)) % 4.62/4.88 (declare-const tptp.collec309745849at_nat (-> (-> tptp.set_nat_nat_nat2 Bool) tptp.set_set_nat_nat_nat2)) % 4.62/4.88 (declare-const tptp.finite1064868788at_nat (-> tptp.set_nat_nat_nat_nat3 Bool)) % 4.62/4.88 (declare-const tptp.ord_le2040082867at_nat (-> tptp.set_nat_nat_nat_nat3 tptp.set_nat_nat_nat_nat3 Bool)) % 4.62/4.88 (declare-const tptp.collec1702444712at_nat (-> (-> tptp.set_nat_nat_nat_nat3 Bool) tptp.set_se1657353at_nat)) % 4.62/4.88 (declare-const tptp.finite570312790at_nat (-> tptp.set_nat_nat Bool)) % 4.62/4.88 (declare-const tptp.collect_set_nat_nat (-> (-> tptp.set_nat_nat Bool) tptp.set_set_nat_nat)) % 4.62/4.88 (declare-const tptp.ord_le2026740592_nat_o (-> (-> (-> tptp.nat tptp.nat) Bool) (-> (-> tptp.nat tptp.nat) Bool) Bool)) % 4.62/4.88 (declare-const tptp.ord_less_eq_nat_o (-> (-> tptp.nat Bool) (-> tptp.nat Bool) Bool)) % 4.62/4.88 (declare-const tptp.member_set_nat_nat (-> tptp.set_nat_nat tptp.set_set_nat_nat Bool)) % 4.62/4.88 (declare-const tptp.ord_le2059018749at_nat (-> (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat) (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat) Bool)) % 4.62/4.88 (declare-const tptp.ord_le809907342at_nat (-> (-> (-> tptp.nat tptp.nat) tptp.nat) (-> (-> tptp.nat tptp.nat) tptp.nat) Bool)) % 4.62/4.88 (declare-const tptp.ord_le1415139726at_nat (-> (-> tptp.nat tptp.nat tptp.nat) (-> tptp.nat tptp.nat tptp.nat) Bool)) % 4.62/4.88 (declare-const tptp.one_one_nat tptp.nat) % 4.62/4.88 (declare-const tptp.finite891768244at_nat (-> tptp.set_nat_nat_nat_nat Bool)) % 4.62/4.88 (declare-const tptp.collec1437545714at_nat (-> (-> (-> tptp.nat tptp.nat tptp.nat tptp.nat) Bool) tptp.set_nat_nat_nat_nat)) % 4.62/4.88 (declare-const tptp.finite2081887156at_nat (-> tptp.set_nat_nat_nat_nat4 Bool)) % 4.62/4.88 (declare-const tptp.member_nat_nat_nat2 (-> (-> tptp.nat tptp.nat tptp.nat) tptp.set_nat_nat_nat Bool)) % 4.62/4.88 (declare-const tptp.finite1090277411at_nat (-> tptp.set_na1201295426at_nat Bool)) % 4.62/4.88 (declare-const tptp.collect_nat (-> (-> tptp.nat Bool) tptp.set_nat)) % 4.62/4.88 (declare-const tptp.collec480180978at_nat (-> (-> (-> (-> tptp.nat tptp.nat tptp.nat) tptp.nat) Bool) tptp.set_nat_nat_nat_nat4)) % 4.62/4.88 (declare-const tptp.collect_nat_nat_nat2 (-> (-> (-> tptp.nat tptp.nat tptp.nat) Bool) tptp.set_nat_nat_nat)) % 4.62/4.88 (declare-const tptp.number1551313001itions (-> (-> tptp.nat tptp.nat) tptp.nat Bool)) % 4.62/4.88 (declare-const tptp.collect_nat_nat (-> (-> (-> tptp.nat tptp.nat) Bool) tptp.set_nat_nat)) % 4.62/4.88 (declare-const tptp.n tptp.nat) % 4.62/4.88 (declare-const tptp.collec1610646258at_nat (-> (-> (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat) Bool) tptp.set_nat_nat_nat_nat3)) % 4.62/4.88 (declare-const tptp.finite604103692at_nat (-> tptp.set_set_nat_nat Bool)) % 4.62/4.88 (declare-const tptp.member1128122036at_nat (-> (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat) tptp.set_nat_nat_nat_nat3 Bool)) % 4.62/4.88 (declare-const tptp.ord_less_eq_nat_nat (-> (-> tptp.nat tptp.nat) (-> tptp.nat tptp.nat) Bool)) % 4.62/4.88 (declare-const tptp.zero_zero_nat tptp.nat) % 4.62/4.88 (declare-const tptp.collec1130010610at_nat (-> (-> (-> tptp.nat (-> tptp.nat tptp.nat) tptp.nat) Bool) tptp.set_nat_nat_nat_nat2)) % 4.62/4.88 (declare-const tptp.finite1397812515at_nat (-> tptp.set_na1064332610at_nat Bool)) % 4.62/4.88 (declare-const tptp.collec2071977458at_nat (-> (-> (-> (-> (-> tptp.nat tptp.nat) tptp.nat) tptp.nat) Bool) tptp.set_nat_nat_nat_nat5)) % 4.62/4.88 (declare-const tptp.finite584233140at_nat (-> tptp.set_nat_nat_nat_nat2 Bool)) % 4.62/4.88 (declare-const tptp.member_nat_nat_nat (-> (-> (-> tptp.nat tptp.nat) tptp.nat) tptp.set_nat_nat_nat2 Bool)) % 4.62/4.88 (declare-const tptp.finite1526199988at_nat (-> tptp.set_nat_nat_nat_nat5 Bool)) % 4.62/4.88 (declare-const tptp.collec6783585at_nat (-> (-> (-> (-> tptp.nat tptp.nat) (-> tptp.nat tptp.nat) tptp.nat) Bool) tptp.set_na1201295426at_nat)) % 4.62/4.88 (declare-const tptp.collect_nat_nat_nat (-> (-> (-> (-> tptp.nat tptp.nat) tptp.nat) Bool) tptp.set_nat_nat_nat2)) % 4.62/4.88 (declare-const tptp.finite2012248349et_nat (-> tptp.set_set_nat Bool)) % 4.62/4.88 (declare-const tptp.finite137548155at_nat (-> tptp.set_set_nat_nat_nat Bool)) % 4.62/4.88 (declare-const tptp.collec314318689at_nat (-> (-> (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat tptp.nat) Bool) tptp.set_na1064332610at_nat)) % 4.62/4.88 (declare-const tptp.finite1977496699at_nat (-> tptp.set_set_nat_nat_nat2 Bool)) % 4.62/4.88 (declare-const tptp.finite547180394at_nat (-> tptp.set_se1657353at_nat Bool)) % 4.62/4.88 (define tptp.ord_less_eq_nat () (let ((_let_1 (@var "C2" tptp.nat))) (let ((_let_2 (@var "A2" tptp.nat))) (let ((_let_3 (@var "B4" tptp.nat))) (lambda (@list _let_2 _let_3) (exists (@list _let_1) (= _let_3 (_ (_ tptp.plus_plus_nat _let_2) _let_1)))))))) % 4.62/4.88 (define tptp.finite_finite_nat () (let ((_let_1 (@var "M2" tptp.nat))) (let ((_let_2 (@var "X" tptp.nat))) (let ((_let_3 (@var "N4" 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))))))))) % 4.62/4.88 (define tptp.ord_less_eq_set_nat () (let ((_let_1 (@var "B2" tptp.set_nat))) (let ((_let_2 (@var "X" tptp.nat))) (let ((_let_3 (_ tptp.member_nat _let_2))) (let ((_let_4 (@var "A5" tptp.set_nat))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1))))))))) % 4.62/4.88 (define tptp.ord_le1415039317at_nat () (let ((_let_1 (@var "B2" tptp.set_nat_nat))) (let ((_let_2 (@var "X" (-> tptp.nat tptp.nat)))) (let ((_let_3 (_ tptp.member_nat_nat _let_2))) (let ((_let_4 (@var "A5" tptp.set_nat_nat))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1))))))))) % 4.62/4.88 (define tptp.finite_Fpow_nat () (let ((_let_1 (@var "X6" tptp.set_nat))) (let ((_let_2 (@var "A5" tptp.set_nat))) (lambda (@list _let_2) (_ tptp.collect_set_nat (lambda (@list _let_1) (and (_ (_ tptp.ord_less_eq_set_nat _let_1) _let_2) (_ tptp.finite_finite_nat _let_1)))))))) % 4.62/4.88 (define tptp.finite90785608at_nat () (let ((_let_1 (@var "X6" tptp.set_nat_nat_nat))) (let ((_let_2 (@var "A5" tptp.set_nat_nat_nat))) (lambda (@list _let_2) (_ tptp.collec617280953at_nat (lambda (@list _let_1) (and (_ (_ tptp.ord_le940807492at_nat _let_1) _let_2) (_ tptp.finite2045569477at_nat _let_1)))))))) % 4.62/4.88 (define tptp.finite1633036872at_nat () (let ((_let_1 (@var "X6" tptp.set_nat_nat_nat2))) (let ((_let_2 (@var "A5" tptp.set_nat_nat_nat2))) (lambda (@list _let_2) (_ tptp.collec309745849at_nat (lambda (@list _let_1) (and (_ (_ tptp.ord_le633272388at_nat _let_1) _let_2) (_ tptp.finite1440337093at_nat _let_1)))))))) % 4.62/4.88 (define tptp.finite252967095at_nat () (let ((_let_1 (@var "X6" tptp.set_nat_nat_nat_nat3))) (let ((_let_2 (@var "A5" tptp.set_nat_nat_nat_nat3))) (lambda (@list _let_2) (_ tptp.collec1702444712at_nat (lambda (@list _let_1) (and (_ (_ tptp.ord_le2040082867at_nat _let_1) _let_2) (_ tptp.finite1064868788at_nat _let_1)))))))) % 4.62/4.88 (define tptp.finite_Fpow_nat_nat () (let ((_let_1 (@var "X6" tptp.set_nat_nat))) (let ((_let_2 (@var "A5" tptp.set_nat_nat))) (lambda (@list _let_2) (_ tptp.collect_set_nat_nat (lambda (@list _let_1) (and (_ (_ tptp.ord_le1415039317at_nat _let_1) _let_2) (_ tptp.finite570312790at_nat _let_1)))))))) % 4.62/4.88 (define tptp.ord_less_nat () (let ((_let_1 (@var "B4" tptp.nat))) (let ((_let_2 (@var "A2" tptp.nat))) (lambda (@list _let_1 _let_2) (and (_ (_ tptp.ord_less_eq_nat _let_1) _let_2) (not (= _let_2 _let_1))))))) % 4.62/4.88 (define tptp.ord_less_set_nat_nat () (let ((_let_1 (@var "B4" tptp.set_nat_nat))) (let ((_let_2 (@var "A2" tptp.set_nat_nat))) (lambda (@list _let_1 _let_2) (and (_ (_ tptp.ord_le1415039317at_nat _let_1) _let_2) (not (= _let_2 _let_1))))))) % 4.62/4.88 (define @t1 () (@var "I" tptp.nat)) % 4.62/4.88 (define @t2 () (@var "F" (-> tptp.nat tptp.nat))) % 4.62/4.88 (define @t3 () (_ @t2 @t1)) % 4.62/4.88 (define @t4 () (= @t3 tptp.zero_zero_nat)) % 4.62/4.88 (define @t5 () (_ (_ tptp.plus_plus_nat tptp.n) tptp.one_one_nat)) % 4.62/4.88 (define @t6 () (=> (_ (_ tptp.ord_less_eq_nat @t5) @t1) @t4)) % 4.62/4.88 (define @t7 () (@list @t1)) % 4.62/4.88 (define @t8 () (forall @t7 @t6)) % 4.62/4.88 (define @t9 () (_ tptp.ord_less_eq_nat @t3)) % 4.62/4.88 (define @t10 () (forall @t7 (_ @t9 tptp.n))) % 4.62/4.88 (define @t11 () (and @t10 @t8)) % 4.62/4.88 (define @t12 () (@list @t2)) % 4.62/4.88 (define @t13 () (lambda @t12 @t11)) % 4.62/4.88 (define @t14 () (_ tptp.collect_nat_nat @t13)) % 4.62/4.88 (define @t15 () (@var "P" (-> tptp.nat tptp.nat))) % 4.62/4.88 (define @t16 () (_ (_ tptp.number1551313001itions @t15) tptp.n)) % 4.62/4.88 (define @t17 () (@list @t15)) % 4.62/4.88 (define @t18 () (lambda @t17 @t16)) % 4.62/4.88 (define @t19 () (_ tptp.collect_nat_nat @t18)) % 4.62/4.88 (define @t20 () (@var "X" (-> tptp.nat tptp.nat tptp.nat))) % 4.62/4.88 (define @t21 () (@var "Q" (-> (-> tptp.nat tptp.nat tptp.nat) Bool))) % 4.62/4.88 (define @t22 () (_ @t21 @t20)) % 4.62/4.88 (define @t23 () (@var "P2" (-> (-> tptp.nat tptp.nat tptp.nat) Bool))) % 4.62/4.88 (define @t24 () (_ @t23 @t20)) % 4.62/4.88 (define @t25 () (@list @t20)) % 4.62/4.88 (define @t26 () (_ tptp.collect_nat_nat_nat2 (lambda @t25 (and @t24 @t22)))) % 4.62/4.88 (define @t27 () (_ tptp.collect_nat_nat_nat2 @t21)) % 4.62/4.88 (define @t28 () (_ tptp.finite2045569477at_nat @t27)) % 4.62/4.88 (define @t29 () (_ tptp.collect_nat_nat_nat2 @t23)) % 4.62/4.88 (define @t30 () (_ tptp.finite2045569477at_nat @t29)) % 4.62/4.88 (define @t31 () (@list @t23 @t21)) % 4.62/4.88 (define @t32 () (@var "X" (-> (-> tptp.nat tptp.nat) tptp.nat))) % 4.62/4.88 (define @t33 () (@var "Q" (-> (-> (-> tptp.nat tptp.nat) tptp.nat) Bool))) % 4.62/4.88 (define @t34 () (_ @t33 @t32)) % 4.62/4.88 (define @t35 () (@var "P2" (-> (-> (-> tptp.nat tptp.nat) tptp.nat) Bool))) % 4.62/4.88 (define @t36 () (_ @t35 @t32)) % 4.62/4.88 (define @t37 () (@list @t32)) % 4.62/4.88 (define @t38 () (_ tptp.collect_nat_nat_nat (lambda @t37 (and @t36 @t34)))) % 4.62/4.88 (define @t39 () (_ tptp.collect_nat_nat_nat @t33)) % 4.62/4.88 (define @t40 () (_ tptp.finite1440337093at_nat @t39)) % 4.62/4.88 (define @t41 () (_ tptp.collect_nat_nat_nat @t35)) % 4.62/4.88 (define @t42 () (_ tptp.finite1440337093at_nat @t41)) % 4.62/4.88 (define @t43 () (@list @t35 @t33)) % 4.62/4.88 (define @t44 () (@var "X" (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat))) % 4.62/4.88 (define @t45 () (@var "Q" (-> (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat) Bool))) % 4.62/4.88 (define @t46 () (_ @t45 @t44)) % 4.62/4.88 (define @t47 () (@var "P2" (-> (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat) Bool))) % 4.62/4.88 (define @t48 () (_ @t47 @t44)) % 4.62/4.88 (define @t49 () (@list @t44)) % 4.62/4.88 (define @t50 () (_ tptp.collec1610646258at_nat (lambda @t49 (and @t48 @t46)))) % 4.62/4.88 (define @t51 () (_ tptp.collec1610646258at_nat @t45)) % 4.62/4.88 (define @t52 () (_ tptp.finite1064868788at_nat @t51)) % 4.62/4.88 (define @t53 () (_ tptp.collec1610646258at_nat @t47)) % 4.62/4.88 (define @t54 () (_ tptp.finite1064868788at_nat @t53)) % 4.62/4.88 (define @t55 () (@list @t47 @t45)) % 4.62/4.88 (define @t56 () (@var "X" (-> tptp.nat tptp.nat))) % 4.62/4.88 (define @t57 () (@var "Q" (-> (-> tptp.nat tptp.nat) Bool))) % 4.62/4.88 (define @t58 () (_ @t57 @t56)) % 4.62/4.88 (define @t59 () (@var "P2" (-> (-> tptp.nat tptp.nat) Bool))) % 4.62/4.88 (define @t60 () (_ @t59 @t56)) % 4.62/4.88 (define @t61 () (@list @t56)) % 4.62/4.88 (define @t62 () (_ tptp.collect_nat_nat (lambda @t61 (and @t60 @t58)))) % 4.62/4.88 (define @t63 () (_ tptp.collect_nat_nat @t57)) % 4.62/4.88 (define @t64 () (_ tptp.finite570312790at_nat @t63)) % 4.62/4.88 (define @t65 () (_ tptp.collect_nat_nat @t59)) % 4.62/4.88 (define @t66 () (_ tptp.finite570312790at_nat @t65)) % 4.62/4.88 (define @t67 () (@list @t59 @t57)) % 4.62/4.88 (define @t68 () (@var "X" tptp.nat)) % 4.62/4.88 (define @t69 () (@var "Q" (-> tptp.nat Bool))) % 4.62/4.88 (define @t70 () (_ @t69 @t68)) % 4.62/4.88 (define @t71 () (@var "P2" (-> tptp.nat Bool))) % 4.62/4.88 (define @t72 () (_ @t71 @t68)) % 4.62/4.88 (define @t73 () (@list @t68)) % 4.62/4.88 (define @t74 () (_ tptp.collect_nat (lambda @t73 (and @t72 @t70)))) % 4.62/4.88 (define @t75 () (_ tptp.collect_nat @t69)) % 4.62/4.88 (define @t76 () (_ tptp.finite_finite_nat @t75)) % 4.62/4.88 (define @t77 () (_ tptp.collect_nat @t71)) % 4.62/4.88 (define @t78 () (_ tptp.finite_finite_nat @t77)) % 4.62/4.88 (define @t79 () (@list @t71 @t69)) % 4.62/4.88 (define @t80 () (@var "P3" (-> tptp.nat tptp.nat))) % 4.62/4.88 (define @t81 () (_ tptp.number1551313001itions @t80)) % 4.62/4.88 (define @t82 () (@var "N" tptp.nat)) % 4.62/4.88 (define @t83 () (@var "I2" tptp.nat)) % 4.62/4.88 (define @t84 () (_ @t81 @t82)) % 4.62/4.88 (define @t85 () (@var "D" tptp.nat)) % 4.62/4.88 (define @t86 () (_ @t2 @t68)) % 4.62/4.88 (define @t87 () (@var "A" tptp.set_nat)) % 4.62/4.88 (define @t88 () (_ tptp.member_nat @t68)) % 4.62/4.88 (define @t89 () (_ @t88 @t87)) % 4.62/4.88 (define @t90 () (not @t89)) % 4.62/4.88 (define @t91 () (@var "B" tptp.set_nat)) % 4.62/4.88 (define @t92 () (_ tptp.finite_finite_nat @t91)) % 4.62/4.88 (define @t93 () (_ tptp.finite_finite_nat @t87)) % 4.62/4.88 (define @t94 () (@var "F" (-> (-> tptp.nat tptp.nat) tptp.nat))) % 4.62/4.88 (define @t95 () (_ @t94 @t56)) % 4.62/4.88 (define @t96 () (@var "A" tptp.set_nat_nat)) % 4.62/4.88 (define @t97 () (_ tptp.member_nat_nat @t56)) % 4.62/4.88 (define @t98 () (_ @t97 @t96)) % 4.62/4.88 (define @t99 () (not @t98)) % 4.62/4.88 (define @t100 () (_ tptp.finite570312790at_nat @t96)) % 4.62/4.88 (define @t101 () (@var "D" (-> tptp.nat tptp.nat))) % 4.62/4.88 (define @t102 () (@var "F" (-> tptp.nat tptp.nat tptp.nat))) % 4.62/4.88 (define @t103 () (_ @t102 @t68)) % 4.62/4.88 (define @t104 () (@var "B" tptp.set_nat_nat)) % 4.62/4.88 (define @t105 () (_ tptp.finite570312790at_nat @t104)) % 4.62/4.88 (define @t106 () (@var "F" (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat))) % 4.62/4.88 (define @t107 () (_ @t106 @t56)) % 4.62/4.88 (define @t108 () (@var "D" (-> tptp.nat tptp.nat tptp.nat))) % 4.62/4.88 (define @t109 () (@var "F" (-> tptp.nat tptp.nat tptp.nat tptp.nat))) % 4.62/4.88 (define @t110 () (_ @t109 @t68)) % 4.62/4.88 (define @t111 () (@var "B" tptp.set_nat_nat_nat)) % 4.62/4.88 (define @t112 () (_ tptp.finite2045569477at_nat @t111)) % 4.62/4.88 (define @t113 () (@var "D" (-> (-> tptp.nat tptp.nat) tptp.nat))) % 4.62/4.88 (define @t114 () (@var "F" (-> tptp.nat (-> tptp.nat tptp.nat) tptp.nat))) % 4.62/4.88 (define @t115 () (_ @t114 @t68)) % 4.62/4.88 (define @t116 () (@var "B" tptp.set_nat_nat_nat2)) % 4.62/4.88 (define @t117 () (_ tptp.finite1440337093at_nat @t116)) % 4.62/4.88 (define @t118 () (@var "F" (-> (-> tptp.nat tptp.nat tptp.nat) tptp.nat))) % 4.62/4.88 (define @t119 () (_ @t118 @t20)) % 4.62/4.88 (define @t120 () (@var "A" tptp.set_nat_nat_nat)) % 4.62/4.88 (define @t121 () (_ tptp.member_nat_nat_nat2 @t20)) % 4.62/4.88 (define @t122 () (_ @t121 @t120)) % 4.62/4.88 (define @t123 () (_ tptp.finite2045569477at_nat @t120)) % 4.62/4.88 (define @t124 () (@var "F" (-> (-> (-> tptp.nat tptp.nat) tptp.nat) tptp.nat))) % 4.62/4.88 (define @t125 () (_ @t124 @t32)) % 4.62/4.88 (define @t126 () (@var "A" tptp.set_nat_nat_nat2)) % 4.62/4.88 (define @t127 () (_ tptp.member_nat_nat_nat @t32)) % 4.62/4.88 (define @t128 () (_ @t127 @t126)) % 4.62/4.88 (define @t129 () (_ tptp.finite1440337093at_nat @t126)) % 4.62/4.88 (define @t130 () (@var "F" (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat tptp.nat))) % 4.62/4.88 (define @t131 () (_ @t130 @t56)) % 4.62/4.88 (define @t132 () (@var "F" (-> (-> tptp.nat tptp.nat) (-> tptp.nat tptp.nat) tptp.nat))) % 4.62/4.88 (define @t133 () (_ @t132 @t56)) % 4.62/4.88 (define @t134 () (@var "X_1" (-> tptp.nat tptp.nat tptp.nat))) % 4.62/4.88 (define @t135 () (@var "X_1" (-> (-> tptp.nat tptp.nat) tptp.nat))) % 4.62/4.88 (define @t136 () (@var "X_1" (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat))) % 4.62/4.88 (define @t137 () (@var "X_1" (-> tptp.nat tptp.nat))) % 4.62/4.88 (define @t138 () (@var "X_1" tptp.nat)) % 4.62/4.88 (define @t139 () (@var "X2" tptp.nat)) % 4.62/4.88 (define @t140 () (@var "A2" tptp.nat)) % 4.62/4.88 (define @t141 () (@var "R" (-> tptp.nat tptp.nat Bool))) % 4.62/4.88 (define @t142 () (_ (_ tptp.member_nat @t140) @t87)) % 4.62/4.88 (define @t143 () (@list @t140)) % 4.62/4.88 (define @t144 () (_ tptp.member_nat @t139)) % 4.62/4.88 (define @t145 () (_ @t144 @t91)) % 4.62/4.88 (define @t146 () (@list @t139)) % 4.62/4.88 (define @t147 () (@var "Xa" tptp.nat)) % 4.62/4.88 (define @t148 () (_ tptp.member_nat @t147)) % 4.62/4.88 (define @t149 () (_ @t148 @t91)) % 4.62/4.88 (define @t150 () (@list @t147)) % 4.62/4.88 (define @t151 () (_ @t144 @t87)) % 4.62/4.88 (define @t152 () (not @t93)) % 4.62/4.88 (define @t153 () (@var "A2" (-> tptp.nat tptp.nat))) % 4.62/4.88 (define @t154 () (@var "R" (-> (-> tptp.nat tptp.nat) tptp.nat Bool))) % 4.62/4.88 (define @t155 () (_ (_ tptp.member_nat_nat @t153) @t96)) % 4.62/4.88 (define @t156 () (@list @t153)) % 4.62/4.88 (define @t157 () (@var "X2" (-> tptp.nat tptp.nat))) % 4.62/4.88 (define @t158 () (_ tptp.member_nat_nat @t157)) % 4.62/4.88 (define @t159 () (_ @t158 @t96)) % 4.62/4.88 (define @t160 () (@list @t157)) % 4.62/4.88 (define @t161 () (not @t100)) % 4.62/4.88 (define @t162 () (@var "R" (-> tptp.nat (-> tptp.nat tptp.nat) Bool))) % 4.62/4.88 (define @t163 () (_ @t158 @t104)) % 4.62/4.88 (define @t164 () (@var "Xa" (-> tptp.nat tptp.nat))) % 4.62/4.88 (define @t165 () (_ tptp.member_nat_nat @t164)) % 4.62/4.88 (define @t166 () (_ @t165 @t104)) % 4.62/4.88 (define @t167 () (@list @t164)) % 4.62/4.88 (define @t168 () (@var "R" (-> (-> tptp.nat tptp.nat) (-> tptp.nat tptp.nat) Bool))) % 4.62/4.88 (define @t169 () (@var "X2" (-> tptp.nat tptp.nat tptp.nat))) % 4.62/4.88 (define @t170 () (@var "R" (-> tptp.nat (-> tptp.nat tptp.nat tptp.nat) Bool))) % 4.62/4.88 (define @t171 () (_ tptp.member_nat_nat_nat2 @t169)) % 4.62/4.88 (define @t172 () (_ @t171 @t111)) % 4.62/4.88 (define @t173 () (@list @t169)) % 4.62/4.88 (define @t174 () (@var "Xa" (-> tptp.nat tptp.nat tptp.nat))) % 4.62/4.88 (define @t175 () (_ tptp.member_nat_nat_nat2 @t174)) % 4.62/4.88 (define @t176 () (_ @t175 @t111)) % 4.62/4.88 (define @t177 () (@list @t174)) % 4.62/4.88 (define @t178 () (@var "X2" (-> (-> tptp.nat tptp.nat) tptp.nat))) % 4.62/4.88 (define @t179 () (@var "R" (-> tptp.nat (-> (-> tptp.nat tptp.nat) tptp.nat) Bool))) % 4.62/4.88 (define @t180 () (_ tptp.member_nat_nat_nat @t178)) % 4.62/4.88 (define @t181 () (_ @t180 @t116)) % 4.62/4.88 (define @t182 () (@list @t178)) % 4.62/4.88 (define @t183 () (@var "Xa" (-> (-> tptp.nat tptp.nat) tptp.nat))) % 4.62/4.88 (define @t184 () (_ tptp.member_nat_nat_nat @t183)) % 4.62/4.88 (define @t185 () (_ @t184 @t116)) % 4.62/4.88 (define @t186 () (@list @t183)) % 4.62/4.88 (define @t187 () (@var "A2" (-> tptp.nat tptp.nat tptp.nat))) % 4.62/4.88 (define @t188 () (@var "R" (-> (-> tptp.nat tptp.nat tptp.nat) tptp.nat Bool))) % 4.62/4.88 (define @t189 () (_ @t171 @t120)) % 4.62/4.88 (define @t190 () (@var "A2" (-> (-> tptp.nat tptp.nat) tptp.nat))) % 4.62/4.88 (define @t191 () (@var "R" (-> (-> (-> tptp.nat tptp.nat) tptp.nat) tptp.nat Bool))) % 4.62/4.88 (define @t192 () (_ @t180 @t126)) % 4.62/4.88 (define @t193 () (@var "R" (-> (-> tptp.nat tptp.nat) (-> tptp.nat tptp.nat tptp.nat) Bool))) % 4.62/4.88 (define @t194 () (@var "R" (-> (-> tptp.nat tptp.nat) (-> (-> tptp.nat tptp.nat) tptp.nat) Bool))) % 4.62/4.88 (define @t195 () (@var "B2" tptp.set_nat)) % 4.62/4.88 (define @t196 () (@list @t87)) % 4.62/4.88 (define @t197 () (@var "B2" tptp.set_nat_nat_nat)) % 4.62/4.88 (define @t198 () (@list @t120)) % 4.62/4.88 (define @t199 () (@var "B2" tptp.set_nat_nat_nat2)) % 4.62/4.88 (define @t200 () (@list @t126)) % 4.62/4.88 (define @t201 () (@var "A" tptp.set_nat_nat_nat_nat3)) % 4.62/4.88 (define @t202 () (@var "B2" tptp.set_nat_nat_nat_nat3)) % 4.62/4.88 (define @t203 () (_ tptp.finite1064868788at_nat @t201)) % 4.62/4.88 (define @t204 () (@list @t201)) % 4.62/4.88 (define @t205 () (@var "B2" tptp.set_nat_nat)) % 4.62/4.88 (define @t206 () (_ tptp.ord_le1415039317at_nat @t205)) % 4.62/4.88 (define @t207 () (@list @t205)) % 4.62/4.88 (define @t208 () (@list @t96)) % 4.62/4.88 (define @t209 () (@var "M" tptp.nat)) % 4.62/4.88 (define @t210 () (_ tptp.ord_less_eq_nat @t209)) % 4.62/4.88 (define @t211 () (@list @t82 @t209)) % 4.62/4.88 (define @t212 () (@var "K" tptp.nat)) % 4.62/4.88 (define @t213 () (@var "N2" tptp.nat)) % 4.62/4.88 (define @t214 () (@list @t213)) % 4.62/4.88 (define @t215 () (@list @t212)) % 4.62/4.88 (define @t216 () (= @t157 @t164)) % 4.62/4.88 (define @t217 () (_ @t165 @t96)) % 4.62/4.88 (define @t218 () (@var "A3" (-> tptp.nat tptp.nat))) % 4.62/4.88 (define @t219 () (_ tptp.ord_less_eq_nat_nat @t157)) % 4.62/4.88 (define @t220 () (_ tptp.member_nat_nat @t218)) % 4.62/4.88 (define @t221 () (_ @t220 @t96)) % 4.62/4.88 (define @t222 () (@list @t96 @t218)) % 4.62/4.88 (define @t223 () (= @t169 @t174)) % 4.62/4.88 (define @t224 () (_ @t175 @t120)) % 4.62/4.88 (define @t225 () (@var "A3" (-> tptp.nat tptp.nat tptp.nat))) % 4.62/4.88 (define @t226 () (_ tptp.ord_le1415139726at_nat @t169)) % 4.62/4.88 (define @t227 () (_ tptp.member_nat_nat_nat2 @t225)) % 4.62/4.88 (define @t228 () (_ @t227 @t120)) % 4.62/4.88 (define @t229 () (@list @t120 @t225)) % 4.62/4.88 (define @t230 () (= @t178 @t183)) % 4.62/4.88 (define @t231 () (_ @t184 @t126)) % 4.62/4.88 (define @t232 () (@var "A3" (-> (-> tptp.nat tptp.nat) tptp.nat))) % 4.62/4.88 (define @t233 () (_ tptp.ord_le809907342at_nat @t178)) % 4.62/4.88 (define @t234 () (_ tptp.member_nat_nat_nat @t232)) % 4.62/4.88 (define @t235 () (_ @t234 @t126)) % 4.62/4.88 (define @t236 () (@list @t126 @t232)) % 4.62/4.88 (define @t237 () (@var "Xa" (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat))) % 4.62/4.88 (define @t238 () (@var "X2" (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat))) % 4.62/4.88 (define @t239 () (= @t238 @t237)) % 4.62/4.88 (define @t240 () (_ (_ tptp.member1128122036at_nat @t237) @t201)) % 4.62/4.88 (define @t241 () (@list @t237)) % 4.62/4.88 (define @t242 () (@var "A3" (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat))) % 4.62/4.88 (define @t243 () (_ tptp.ord_le2059018749at_nat @t238)) % 4.62/4.88 (define @t244 () (_ tptp.member1128122036at_nat @t238)) % 4.62/4.88 (define @t245 () (_ @t244 @t201)) % 4.62/4.88 (define @t246 () (@list @t238)) % 4.62/4.88 (define @t247 () (_ tptp.member1128122036at_nat @t242)) % 4.62/4.88 (define @t248 () (_ @t247 @t201)) % 4.62/4.88 (define @t249 () (@list @t201 @t242)) % 4.62/4.88 (define @t250 () (= @t139 @t147)) % 4.62/4.88 (define @t251 () (_ @t148 @t87)) % 4.62/4.88 (define @t252 () (@var "A3" tptp.nat)) % 4.62/4.88 (define @t253 () (_ tptp.ord_less_eq_nat @t139)) % 4.62/4.88 (define @t254 () (_ tptp.member_nat @t252)) % 4.62/4.88 (define @t255 () (_ @t254 @t87)) % 4.62/4.88 (define @t256 () (@list @t87 @t252)) % 4.62/4.88 (define @t257 () (@var "Xa" tptp.set_nat_nat)) % 4.62/4.88 (define @t258 () (@var "X2" tptp.set_nat_nat)) % 4.62/4.88 (define @t259 () (= @t258 @t257)) % 4.62/4.88 (define @t260 () (@var "A" tptp.set_set_nat_nat)) % 4.62/4.88 (define @t261 () (_ (_ tptp.member_set_nat_nat @t257) @t260)) % 4.62/4.88 (define @t262 () (@list @t257)) % 4.62/4.88 (define @t263 () (@var "A3" tptp.set_nat_nat)) % 4.62/4.88 (define @t264 () (_ tptp.ord_le1415039317at_nat @t258)) % 4.62/4.88 (define @t265 () (_ (_ tptp.member_set_nat_nat @t258) @t260)) % 4.62/4.88 (define @t266 () (@list @t258)) % 4.62/4.88 (define @t267 () (_ (_ tptp.member_set_nat_nat @t263) @t260)) % 4.62/4.88 (define @t268 () (_ tptp.finite604103692at_nat @t260)) % 4.62/4.88 (define @t269 () (@list @t260 @t263)) % 4.62/4.88 (define @t270 () (_ tptp.ord_less_eq_nat @t252)) % 4.62/4.88 (define @t271 () (_ tptp.ord_le1415039317at_nat @t263)) % 4.62/4.88 (define @t272 () (_ tptp.ord_less_eq_set_nat @t87)) % 4.62/4.88 (define @t273 () (_ @t272 @t91)) % 4.62/4.88 (define @t274 () (_ tptp.ord_le940807492at_nat @t120)) % 4.62/4.88 (define @t275 () (_ @t274 @t111)) % 4.62/4.88 (define @t276 () (_ tptp.ord_le633272388at_nat @t126)) % 4.62/4.88 (define @t277 () (_ @t276 @t116)) % 4.62/4.88 (define @t278 () (@var "B" tptp.set_nat_nat_nat_nat3)) % 4.62/4.88 (define @t279 () (_ tptp.ord_le2040082867at_nat @t201)) % 4.62/4.88 (define @t280 () (_ @t279 @t278)) % 4.62/4.88 (define @t281 () (_ tptp.finite1064868788at_nat @t278)) % 4.62/4.88 (define @t282 () (_ tptp.ord_le1415039317at_nat @t96)) % 4.62/4.88 (define @t283 () (_ @t282 @t104)) % 4.62/4.88 (define @t284 () (=> @t283 @t100)) % 4.62/4.88 (define @t285 () (=> @t105 @t284)) % 4.62/4.88 (define @t286 () (@list @t104 @t96)) % 4.62/4.88 (define @t287 () (forall @t286 @t285)) % 4.62/4.88 (define @t288 () (@var "T" tptp.set_nat)) % 4.62/4.88 (define @t289 () (@var "S" tptp.set_nat)) % 4.62/4.88 (define @t290 () (@var "T" tptp.set_nat_nat_nat)) % 4.62/4.88 (define @t291 () (@var "S" tptp.set_nat_nat_nat)) % 4.62/4.88 (define @t292 () (@var "T" tptp.set_nat_nat_nat2)) % 4.62/4.88 (define @t293 () (@var "S" tptp.set_nat_nat_nat2)) % 4.62/4.88 (define @t294 () (@var "T" tptp.set_nat_nat_nat_nat3)) % 4.62/4.88 (define @t295 () (@var "S" tptp.set_nat_nat_nat_nat3)) % 4.62/4.88 (define @t296 () (@var "T" tptp.set_nat_nat)) % 4.62/4.88 (define @t297 () (@var "S" tptp.set_nat_nat)) % 4.62/4.88 (define @t298 () (@list @t87 @t91)) % 4.62/4.88 (define @t299 () (@list @t96 @t104)) % 4.62/4.88 (define @t300 () (_ @t270 tptp.zero_zero_nat)) % 4.62/4.88 (define @t301 () (@var "B3" tptp.nat)) % 4.62/4.88 (define @t302 () (_ tptp.plus_plus_nat @t301)) % 4.62/4.88 (define @t303 () (_ @t302 @t252)) % 4.62/4.88 (define @t304 () (@list @t301 @t252)) % 4.62/4.88 (define @t305 () (_ tptp.plus_plus_nat @t252)) % 4.62/4.88 (define @t306 () (_ @t305 @t301)) % 4.62/4.88 (define @t307 () (_ tptp.ord_less_eq_nat @t306)) % 4.62/4.88 (define @t308 () (@list @t252 @t301)) % 4.62/4.88 (define @t309 () (_ tptp.ord_less_eq_nat tptp.zero_zero_nat)) % 4.62/4.88 (define @t310 () (_ @t309 @t301)) % 4.62/4.88 (define @t311 () (_ @t210 @t82)) % 4.62/4.88 (define @t312 () (_ tptp.plus_plus_nat @t212)) % 4.62/4.88 (define @t313 () (_ @t312 @t82)) % 4.62/4.88 (define @t314 () (_ @t312 @t209)) % 4.62/4.88 (define @t315 () (@list @t212 @t209 @t82)) % 4.62/4.88 (define @t316 () (= @t82 tptp.zero_zero_nat)) % 4.62/4.88 (define @t317 () (_ tptp.plus_plus_nat @t209)) % 4.62/4.88 (define @t318 () (_ @t317 @t82)) % 4.62/4.88 (define @t319 () (@list @t209 @t82)) % 4.62/4.88 (define @t320 () (@list @t82)) % 4.62/4.88 (define @t321 () (_ @t309 @t252)) % 4.62/4.88 (define @t322 () (@list @t252)) % 4.62/4.88 (define @t323 () (@var "C" tptp.nat)) % 4.62/4.88 (define @t324 () (= @t301 @t323)) % 4.62/4.88 (define @t325 () (_ tptp.plus_plus_nat @t323)) % 4.62/4.88 (define @t326 () (_ @t325 @t252)) % 4.62/4.88 (define @t327 () (= @t303 @t326)) % 4.62/4.88 (define @t328 () (@list @t301 @t252 @t323)) % 4.62/4.88 (define @t329 () (_ @t305 @t323)) % 4.62/4.88 (define @t330 () (= @t306 @t329)) % 4.62/4.88 (define @t331 () (@list @t252 @t301 @t323)) % 4.62/4.88 (define @t332 () (_ tptp.ord_less_eq_nat @t82)) % 4.62/4.88 (define @t333 () (_ @t270 @t301)) % 4.62/4.88 (define @t334 () (_ @t302 @t323)) % 4.62/4.88 (define @t335 () (_ tptp.ord_less_eq_nat @t329)) % 4.62/4.88 (define @t336 () (_ @t335 @t334)) % 4.62/4.88 (define @t337 () (@list @t252 @t323 @t301)) % 4.62/4.88 (define @t338 () (_ @t325 @t301)) % 4.62/4.88 (define @t339 () (_ (_ tptp.ord_less_eq_nat @t326) @t338)) % 4.62/4.88 (define @t340 () (@list @t323 @t252 @t301)) % 4.62/4.88 (define @t341 () (@var "Y" tptp.nat)) % 4.62/4.88 (define @t342 () (@var "X3" tptp.nat)) % 4.62/4.88 (define @t343 () (= @t342 tptp.zero_zero_nat)) % 4.62/4.88 (define @t344 () (and @t343 (= @t341 tptp.zero_zero_nat))) % 4.62/4.88 (define @t345 () (_ (_ tptp.plus_plus_nat @t342) @t341)) % 4.62/4.88 (define @t346 () (@list @t342 @t341)) % 4.62/4.88 (define @t347 () (= (= @t345 tptp.zero_zero_nat) @t344)) % 4.62/4.88 (define @t348 () (= @t301 tptp.zero_zero_nat)) % 4.62/4.88 (define @t349 () (_ tptp.member1128122036at_nat @t44)) % 4.62/4.88 (define @t350 () (_ @t349 @t201)) % 4.62/4.88 (define @t351 () (_ @t57 @t157)) % 4.62/4.88 (define @t352 () (_ @t59 @t157)) % 4.62/4.88 (define @t353 () (_ @t69 @t139)) % 4.62/4.88 (define @t354 () (_ @t71 @t139)) % 4.62/4.88 (define @t355 () (_ @t21 @t169)) % 4.62/4.88 (define @t356 () (_ @t23 @t169)) % 4.62/4.88 (define @t357 () (_ @t33 @t178)) % 4.62/4.88 (define @t358 () (_ @t35 @t178)) % 4.62/4.88 (define @t359 () (_ @t45 @t238)) % 4.62/4.88 (define @t360 () (_ @t47 @t238)) % 4.62/4.88 (define @t361 () (_ tptp.plus_plus_nat tptp.zero_zero_nat)) % 4.62/4.88 (define @t362 () (@list @t342)) % 4.62/4.88 (define @t363 () (_ @t305 @t334)) % 4.62/4.88 (define @t364 () (@var "B4" tptp.nat)) % 4.62/4.88 (define @t365 () (@list @t140 @t364)) % 4.62/4.88 (define @t366 () (_ @t312 @t306)) % 4.62/4.88 (define @t367 () (@var "B" tptp.nat)) % 4.62/4.88 (define @t368 () (@var "A" tptp.nat)) % 4.62/4.88 (define @t369 () (@var "L" tptp.nat)) % 4.62/4.88 (define @t370 () (@var "J" tptp.nat)) % 4.62/4.88 (define @t371 () (_ tptp.plus_plus_nat @t370)) % 4.62/4.88 (define @t372 () (_ @t371 @t369)) % 4.62/4.88 (define @t373 () (_ (_ tptp.plus_plus_nat @t83) @t212)) % 4.62/4.88 (define @t374 () (= @t212 @t369)) % 4.62/4.88 (define @t375 () (= @t83 @t370)) % 4.62/4.88 (define @t376 () (@list @t83 @t370 @t212 @t369)) % 4.62/4.88 (define @t377 () (@var "Y3" tptp.nat)) % 4.62/4.88 (define @t378 () (@var "Y2" tptp.nat)) % 4.62/4.88 (define @t379 () (_ @t332 @t209)) % 4.62/4.88 (define @t380 () (= @t209 @t82)) % 4.62/4.88 (define @t381 () (_ tptp.ord_less_eq_nat @t83)) % 4.62/4.88 (define @t382 () (_ @t381 @t370)) % 4.62/4.88 (define @t383 () (@list @t83 @t370 @t212)) % 4.62/4.88 (define @t384 () (_ @t309 @t342)) % 4.62/4.88 (define @t385 () (@var "C3" tptp.nat)) % 4.62/4.88 (define @t386 () (= @t301 (_ @t305 @t385))) % 4.62/4.88 (define @t387 () (@list @t385)) % 4.62/4.88 (define @t388 () (_ @t302 @t85)) % 4.62/4.88 (define @t389 () (_ tptp.ord_less_eq_nat @t323)) % 4.62/4.88 (define @t390 () (_ @t389 @t85)) % 4.62/4.88 (define @t391 () (@list @t252 @t301 @t323 @t85)) % 4.62/4.88 (define @t392 () (_ tptp.ord_less_eq_nat @t373)) % 4.62/4.88 (define @t393 () (_ @t392 @t372)) % 4.62/4.88 (define @t394 () (_ tptp.ord_less_eq_nat @t212)) % 4.62/4.88 (define @t395 () (_ @t394 @t369)) % 4.62/4.88 (define @t396 () (= @t252 tptp.zero_zero_nat)) % 4.62/4.88 (define @t397 () (@var "K2" tptp.nat)) % 4.62/4.88 (define @t398 () (@var "M2" tptp.nat)) % 4.62/4.88 (define @t399 () (@list @t397)) % 4.62/4.88 (define @t400 () (@list @t398 @t213)) % 4.62/4.88 (define @t401 () (@list @t83 @t370 @t209)) % 4.62/4.88 (define @t402 () (@var "N3" tptp.nat)) % 4.62/4.88 (define @t403 () (@list @t402)) % 4.62/4.88 (define @t404 () (_ @t394 @t82)) % 4.62/4.88 (define @t405 () (_ (_ tptp.ord_less_eq_nat (_ @t317 @t212)) @t82)) % 4.62/4.88 (define @t406 () (@list @t209 @t212 @t82)) % 4.62/4.88 (define @t407 () (_ tptp.ord_less_eq_nat @t341)) % 4.62/4.88 (define @t408 () (_ tptp.ord_less_eq_nat @t342)) % 4.62/4.88 (define @t409 () (_ tptp.ord_less_eq_nat @t301)) % 4.62/4.88 (define @t410 () (_ @t409 @t329)) % 4.62/4.88 (define @t411 () (_ @t409 @t252)) % 4.62/4.88 (define @t412 () (_ @t335 @t301)) % 4.62/4.88 (define @t413 () (_ @t409 @t323)) % 4.62/4.88 (define @t414 () (_ @t389 @t301)) % 4.62/4.88 (define @t415 () (@var "I" (-> tptp.nat tptp.nat))) % 4.62/4.88 (define @t416 () (@var "Y" (-> (-> tptp.nat tptp.nat) tptp.nat))) % 4.62/4.88 (define @t417 () (_ @t416 @t415)) % 4.62/4.88 (define @t418 () (@var "X3" (-> (-> tptp.nat tptp.nat) tptp.nat))) % 4.62/4.88 (define @t419 () (_ @t418 @t415)) % 4.62/4.88 (define @t420 () (@var "I3" tptp.set_nat_nat)) % 4.62/4.88 (define @t421 () (_ (_ tptp.member_nat_nat @t415) @t420)) % 4.62/4.88 (define @t422 () (@list @t415)) % 4.62/4.88 (define @t423 () (@var "Y" (-> tptp.nat tptp.nat))) % 4.62/4.88 (define @t424 () (_ @t423 @t1)) % 4.62/4.88 (define @t425 () (@var "X3" (-> tptp.nat tptp.nat))) % 4.62/4.88 (define @t426 () (_ @t425 @t1)) % 4.62/4.88 (define @t427 () (@var "I3" tptp.set_nat)) % 4.62/4.88 (define @t428 () (_ (_ tptp.member_nat @t1) @t427)) % 4.62/4.88 (define @t429 () (@var "I" (-> tptp.nat tptp.nat tptp.nat))) % 4.62/4.88 (define @t430 () (@var "Y" (-> (-> tptp.nat tptp.nat tptp.nat) tptp.nat))) % 4.62/4.88 (define @t431 () (_ @t430 @t429)) % 4.62/4.88 (define @t432 () (@var "X3" (-> (-> tptp.nat tptp.nat tptp.nat) tptp.nat))) % 4.62/4.88 (define @t433 () (_ @t432 @t429)) % 4.62/4.88 (define @t434 () (@var "I3" tptp.set_nat_nat_nat)) % 4.62/4.88 (define @t435 () (_ (_ tptp.member_nat_nat_nat2 @t429) @t434)) % 4.62/4.88 (define @t436 () (@list @t429)) % 4.62/4.88 (define @t437 () (@var "I" (-> (-> tptp.nat tptp.nat) tptp.nat))) % 4.62/4.88 (define @t438 () (@var "Y" (-> (-> (-> tptp.nat tptp.nat) tptp.nat) tptp.nat))) % 4.62/4.88 (define @t439 () (_ @t438 @t437)) % 4.62/4.88 (define @t440 () (@var "X3" (-> (-> (-> tptp.nat tptp.nat) tptp.nat) tptp.nat))) % 4.62/4.88 (define @t441 () (_ @t440 @t437)) % 4.62/4.88 (define @t442 () (@var "I3" tptp.set_nat_nat_nat2)) % 4.62/4.88 (define @t443 () (_ (_ tptp.member_nat_nat_nat @t437) @t442)) % 4.62/4.88 (define @t444 () (@list @t437)) % 4.62/4.88 (define @t445 () (@var "I" (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat))) % 4.62/4.88 (define @t446 () (@var "Y" (-> (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat) tptp.nat))) % 4.62/4.88 (define @t447 () (_ @t446 @t445)) % 4.62/4.88 (define @t448 () (@var "X3" (-> (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat) tptp.nat))) % 4.62/4.88 (define @t449 () (_ @t448 @t445)) % 4.62/4.88 (define @t450 () (@var "I3" tptp.set_nat_nat_nat_nat3)) % 4.62/4.88 (define @t451 () (_ (_ tptp.member1128122036at_nat @t445) @t450)) % 4.62/4.88 (define @t452 () (@list @t445)) % 4.62/4.88 (define @t453 () (_ tptp.ord_less_eq_nat tptp.one_one_nat)) % 4.62/4.88 (define @t454 () (@var "U" tptp.nat)) % 4.62/4.88 (define @t455 () (@var "F2" (-> tptp.nat tptp.nat))) % 4.62/4.88 (define @t456 () (= @t96 @t104)) % 4.62/4.88 (define @t457 () (_ tptp.ord_le1415039317at_nat @t104)) % 4.62/4.88 (define @t458 () (_ @t457 @t96)) % 4.62/4.88 (define @t459 () (@var "X3" tptp.set_nat_nat)) % 4.62/4.88 (define @t460 () (_ tptp.ord_le1415039317at_nat @t459)) % 4.62/4.88 (define @t461 () (@var "P2" (-> tptp.nat tptp.nat Bool))) % 4.62/4.88 (define @t462 () (_ (_ @t461 @t252) @t301)) % 4.62/4.88 (define @t463 () (@var "B5" tptp.nat)) % 4.62/4.88 (define @t464 () (@var "A4" tptp.nat)) % 4.62/4.88 (define @t465 () (_ @t461 @t464)) % 4.62/4.88 (define @t466 () (_ @t465 @t463)) % 4.62/4.88 (define @t467 () (@list @t464 @t463)) % 4.62/4.88 (define @t468 () (_ (_ @t461 @t463) @t464)) % 4.62/4.88 (define @t469 () (@list @t461 @t252 @t301)) % 4.62/4.88 (define @t470 () (_ @t253 @t378)) % 4.62/4.88 (define @t471 () (@list @t139 @t378)) % 4.62/4.88 (define @t472 () (forall @t471 (=> @t470 (_ (_ tptp.ord_less_eq_nat (_ @t455 @t139)) (_ @t455 @t378))))) % 4.62/4.88 (define @t473 () (=> @t413 (=> @t472 (_ @t270 (_ @t455 @t323))))) % 4.62/4.88 (define @t474 () (_ @t455 @t301)) % 4.62/4.88 (define @t475 () (@list @t252 @t455 @t301 @t323)) % 4.62/4.88 (define @t476 () (@var "C" tptp.set_nat_nat)) % 4.62/4.88 (define @t477 () (@var "F2" (-> tptp.set_nat_nat tptp.nat))) % 4.62/4.88 (define @t478 () (@var "Y2" tptp.set_nat_nat)) % 4.62/4.88 (define @t479 () (_ @t264 @t478)) % 4.62/4.88 (define @t480 () (@list @t258 @t478)) % 4.62/4.88 (define @t481 () (forall @t480 (=> @t479 (_ (_ tptp.ord_less_eq_nat (_ @t477 @t258)) (_ @t477 @t478))))) % 4.62/4.88 (define @t482 () (@var "B3" tptp.set_nat_nat)) % 4.62/4.88 (define @t483 () (_ tptp.ord_le1415039317at_nat @t482)) % 4.62/4.88 (define @t484 () (_ @t483 @t476)) % 4.62/4.88 (define @t485 () (=> @t484 (=> @t481 (_ @t270 (_ @t477 @t476))))) % 4.62/4.88 (define @t486 () (_ @t477 @t482)) % 4.62/4.88 (define @t487 () (@list @t252 @t477 @t482 @t476)) % 4.62/4.88 (define @t488 () (@var "F2" (-> tptp.nat tptp.set_nat_nat))) % 4.62/4.88 (define @t489 () (forall @t471 (=> @t470 (_ (_ tptp.ord_le1415039317at_nat (_ @t488 @t139)) (_ @t488 @t378))))) % 4.62/4.88 (define @t490 () (=> @t413 (=> @t489 (_ @t271 (_ @t488 @t323))))) % 4.62/4.88 (define @t491 () (_ @t488 @t301)) % 4.62/4.88 (define @t492 () (@list @t263 @t488 @t301 @t323)) % 4.62/4.88 (define @t493 () (@var "F2" (-> tptp.set_nat_nat tptp.set_nat_nat))) % 4.62/4.88 (define @t494 () (forall @t480 (=> @t479 (_ (_ tptp.ord_le1415039317at_nat (_ @t493 @t258)) (_ @t493 @t478))))) % 4.62/4.88 (define @t495 () (=> @t484 (=> @t494 (_ @t271 (_ @t493 @t476))))) % 4.62/4.88 (define @t496 () (_ @t493 @t482)) % 4.62/4.88 (define @t497 () (@list @t263 @t493 @t482 @t476)) % 4.62/4.88 (define @t498 () (=> @t472 (_ (_ tptp.ord_less_eq_nat (_ @t455 @t252)) @t323))) % 4.62/4.88 (define @t499 () (@list @t252 @t301 @t455 @t323)) % 4.62/4.88 (define @t500 () (=> @t489 (_ (_ tptp.ord_le1415039317at_nat (_ @t488 @t252)) @t476))) % 4.62/4.88 (define @t501 () (@list @t252 @t301 @t488 @t476)) % 4.62/4.88 (define @t502 () (=> @t481 (_ (_ tptp.ord_less_eq_nat (_ @t477 @t263)) @t323))) % 4.62/4.88 (define @t503 () (_ @t271 @t482)) % 4.62/4.88 (define @t504 () (@list @t263 @t482 @t477 @t323)) % 4.62/4.88 (define @t505 () (=> @t494 (_ (_ tptp.ord_le1415039317at_nat (_ @t493 @t263)) @t476))) % 4.62/4.88 (define @t506 () (@list @t263 @t482 @t493 @t476)) % 4.62/4.88 (define @t507 () (@var "Y5" tptp.nat)) % 4.62/4.88 (define @t508 () (_ tptp.ord_less_eq_nat @t68)) % 4.62/4.88 (define @t509 () (@var "Z" tptp.nat)) % 4.62/4.88 (define @t510 () (@var "Y4" tptp.nat)) % 4.62/4.88 (define @t511 () (lambda (@list @t510 @t509) (= @t510 @t509))) % 4.62/4.88 (define @t512 () (@var "X" tptp.set_nat_nat)) % 4.62/4.88 (define @t513 () (@var "Y5" tptp.set_nat_nat)) % 4.62/4.88 (define @t514 () (@var "Z" tptp.set_nat_nat)) % 4.62/4.88 (define @t515 () (@var "Y4" tptp.set_nat_nat)) % 4.62/4.88 (define @t516 () (lambda (@list @t515 @t514) (= @t515 @t514))) % 4.62/4.88 (define @t517 () (= @t342 @t341)) % 4.62/4.88 (define @t518 () (_ @t407 @t342)) % 4.62/4.88 (define @t519 () (_ @t408 @t341)) % 4.62/4.88 (define @t520 () (@var "Y" tptp.set_nat_nat)) % 4.62/4.88 (define @t521 () (= @t459 @t520)) % 4.62/4.88 (define @t522 () (_ tptp.ord_le1415039317at_nat @t520)) % 4.62/4.88 (define @t523 () (_ @t522 @t459)) % 4.62/4.88 (define @t524 () (_ @t460 @t520)) % 4.62/4.88 (define @t525 () (@list @t459 @t520)) % 4.62/4.88 (define @t526 () (not @t519)) % 4.62/4.88 (define @t527 () (_ @t270 @t323)) % 4.62/4.88 (define @t528 () (=> @t413 @t527)) % 4.62/4.88 (define @t529 () (_ @t271 @t476)) % 4.62/4.88 (define @t530 () (=> @t484 @t529)) % 4.62/4.88 (define @t531 () (@list @t263 @t482 @t476)) % 4.62/4.88 (define @t532 () (@var "Z2" tptp.nat)) % 4.62/4.88 (define @t533 () (_ tptp.ord_less_eq_nat @t532)) % 4.62/4.88 (define @t534 () (_ @t533 @t342)) % 4.62/4.88 (define @t535 () (_ @t407 @t532)) % 4.62/4.88 (define @t536 () (_ @t533 @t341)) % 4.62/4.88 (define @t537 () (_ @t408 @t532)) % 4.62/4.88 (define @t538 () (@list @t342 @t341 @t532)) % 4.62/4.88 (define @t539 () (_ (_ tptp.ord_less_eq_nat @t364) @t140)) % 4.62/4.88 (define @t540 () (_ (_ tptp.ord_less_eq_nat @t140) @t364)) % 4.62/4.88 (define @t541 () (@var "A2" tptp.set_nat_nat)) % 4.62/4.88 (define @t542 () (@var "B4" tptp.set_nat_nat)) % 4.62/4.88 (define @t543 () (_ (_ tptp.ord_le1415039317at_nat @t542) @t541)) % 4.62/4.88 (define @t544 () (_ (_ tptp.ord_le1415039317at_nat @t541) @t542)) % 4.62/4.88 (define @t545 () (@list @t541 @t542)) % 4.62/4.88 (define @t546 () (= @t252 @t301)) % 4.62/4.88 (define @t547 () (= @t263 @t482)) % 4.62/4.88 (define @t548 () (_ @t483 @t263)) % 4.62/4.88 (define @t549 () (@list @t263 @t482)) % 4.62/4.88 (define @t550 () (@var "Z2" tptp.set_nat_nat)) % 4.62/4.88 (define @t551 () (_ tptp.ord_le1415039317at_nat @t476)) % 4.62/4.88 (define @t552 () (_ @t551 @t482)) % 4.62/4.88 (define @t553 () (@list @t482 @t263 @t476)) % 4.62/4.88 (define @t554 () (@list @t482 @t263)) % 4.62/4.88 (define @t555 () (_ tptp.member_nat @t342)) % 4.62/4.88 (define @t556 () (_ tptp.member_nat_nat @t425)) % 4.62/4.88 (define @t557 () (_ tptp.member_nat @t323)) % 4.62/4.88 (define @t558 () (@var "C" (-> tptp.nat tptp.nat))) % 4.62/4.88 (define @t559 () (_ tptp.member_nat_nat @t558)) % 4.62/4.88 (define @t560 () (@var "T2" tptp.nat)) % 4.62/4.88 (define @t561 () (_ tptp.member_nat @t560)) % 4.62/4.88 (define @t562 () (@var "A5" tptp.set_nat)) % 4.62/4.88 (define @t563 () (@list @t562 @t195)) % 4.62/4.88 (define @t564 () (@var "T2" (-> tptp.nat tptp.nat))) % 4.62/4.88 (define @t565 () (_ tptp.member_nat_nat @t564)) % 4.62/4.88 (define @t566 () (@var "A5" tptp.set_nat_nat)) % 4.62/4.88 (define @t567 () (@list @t566 @t205)) % 4.62/4.88 (define @t568 () (_ (_ tptp.ord_less_eq_set_nat @t77) @t75)) % 4.62/4.88 (define @t569 () (_ (_ tptp.ord_le940807492at_nat @t29) @t27)) % 4.62/4.88 (define @t570 () (_ (_ tptp.ord_le633272388at_nat @t41) @t39)) % 4.62/4.88 (define @t571 () (_ (_ tptp.ord_le2040082867at_nat @t53) @t51)) % 4.62/4.88 (define @t572 () (_ (_ tptp.ord_le1415039317at_nat @t65) @t63)) % 4.62/4.88 (define @t573 () (@var "C4" tptp.set_nat_nat)) % 4.62/4.88 (define @t574 () (@var "M4" tptp.nat)) % 4.62/4.88 (define @t575 () (@var "X4" tptp.nat)) % 4.62/4.88 (define @t576 () (@var "M3" tptp.nat)) % 4.62/4.88 (define @t577 () (_ @t71 @t342)) % 4.62/4.88 (define @t578 () (_ tptp.collect_nat (lambda @t73 (and @t89 @t72)))) % 4.62/4.88 (define @t579 () (_ tptp.collect_nat_nat_nat2 (lambda @t25 (and @t122 @t24)))) % 4.62/4.88 (define @t580 () (_ tptp.collect_nat_nat_nat (lambda @t37 (and @t128 @t36)))) % 4.62/4.88 (define @t581 () (_ tptp.collec1610646258at_nat (lambda @t49 (and @t350 @t48)))) % 4.62/4.88 (define @t582 () (_ tptp.collect_nat_nat (lambda @t61 (and @t98 @t60)))) % 4.62/4.88 (define @t583 () (_ @t88 @t195)) % 4.62/4.88 (define @t584 () (_ @t88 @t562)) % 4.62/4.88 (define @t585 () (_ @t97 @t205)) % 4.62/4.88 (define @t586 () (_ @t97 @t566)) % 4.62/4.88 (define @t587 () (@var "R" tptp.set_nat)) % 4.62/4.88 (define @t588 () (@var "R" tptp.set_nat_nat)) % 4.62/4.88 (define @t589 () (_ @t88 @t91)) % 4.62/4.88 (define @t590 () (_ tptp.ord_less_eq_set_nat @t91)) % 4.62/4.88 (define @t591 () (_ @t590 @t87)) % 4.62/4.88 (define @t592 () (_ @t121 @t111)) % 4.62/4.88 (define @t593 () (_ tptp.ord_le940807492at_nat @t111)) % 4.62/4.88 (define @t594 () (_ @t593 @t120)) % 4.62/4.88 (define @t595 () (_ @t127 @t116)) % 4.62/4.88 (define @t596 () (_ tptp.ord_le633272388at_nat @t116)) % 4.62/4.88 (define @t597 () (_ @t596 @t126)) % 4.62/4.88 (define @t598 () (_ @t349 @t278)) % 4.62/4.88 (define @t599 () (_ tptp.ord_le2040082867at_nat @t278)) % 4.62/4.88 (define @t600 () (_ @t599 @t201)) % 4.62/4.88 (define @t601 () (_ @t97 @t104)) % 4.62/4.88 (define @t602 () (@var "X5" tptp.set_nat)) % 4.62/4.88 (define @t603 () (_ tptp.collect_nat (lambda @t73 (and (_ @t88 @t602) @t72)))) % 4.62/4.88 (define @t604 () (@var "X5" tptp.set_nat_nat_nat)) % 4.62/4.88 (define @t605 () (_ tptp.collect_nat_nat_nat2 (lambda @t25 (and (_ @t121 @t604) @t24)))) % 4.62/4.88 (define @t606 () (@var "X5" tptp.set_nat_nat_nat2)) % 4.62/4.88 (define @t607 () (_ tptp.collect_nat_nat_nat (lambda @t37 (and (_ @t127 @t606) @t36)))) % 4.62/4.88 (define @t608 () (@var "X5" tptp.set_nat_nat_nat_nat3)) % 4.62/4.88 (define @t609 () (_ tptp.collec1610646258at_nat (lambda @t49 (and (_ @t349 @t608) @t48)))) % 4.62/4.88 (define @t610 () (@var "X5" tptp.set_nat_nat)) % 4.62/4.88 (define @t611 () (_ tptp.collect_nat_nat (lambda @t61 (and (_ @t97 @t610) @t60)))) % 4.62/4.88 (define @t612 () (@var "Z3" tptp.set_nat)) % 4.62/4.88 (define @t613 () (@var "X3" (-> tptp.nat tptp.nat tptp.nat))) % 4.62/4.88 (define @t614 () (@var "Z3" tptp.set_nat_nat_nat)) % 4.62/4.88 (define @t615 () (@var "Z3" tptp.set_nat_nat_nat2)) % 4.62/4.88 (define @t616 () (@var "X3" (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat))) % 4.62/4.88 (define @t617 () (@var "Z3" tptp.set_nat_nat_nat_nat3)) % 4.62/4.88 (define @t618 () (@var "Z3" tptp.set_nat_nat)) % 4.62/4.88 (define @t619 () (_ tptp.ord_less_nat tptp.zero_zero_nat)) % 4.62/4.88 (define @t620 () (_ @t619 @t82)) % 4.62/4.88 (define @t621 () (_ tptp.ord_less_nat @t252)) % 4.62/4.88 (define @t622 () (_ @t621 @t301)) % 4.62/4.88 (define @t623 () (_ tptp.ord_less_nat @t329)) % 4.62/4.88 (define @t624 () (_ @t619 @t252)) % 4.62/4.88 (define @t625 () (_ tptp.ord_less_nat @t82)) % 4.62/4.88 (define @t626 () (_ (_ tptp.ord_less_nat @t209) @t82)) % 4.62/4.88 (define @t627 () (_ @t621 tptp.zero_zero_nat)) % 4.62/4.88 (define @t628 () (_ tptp.ord_less_nat @t306)) % 4.62/4.88 (define @t629 () (_ @t619 @t301)) % 4.62/4.88 (define @t630 () (_ @t623 @t388)) % 4.62/4.88 (define @t631 () (_ tptp.ord_less_nat @t323)) % 4.62/4.88 (define @t632 () (_ (_ tptp.ord_less_nat @t373) @t372)) % 4.62/4.88 (define @t633 () (_ tptp.ord_less_nat @t301)) % 4.62/4.88 (define @t634 () (_ tptp.ord_less_set_nat_nat @t263)) % 4.62/4.88 (define @t635 () (_ @t634 @t482)) % 4.62/4.88 (define @t636 () (_ @t633 @t252)) % 4.62/4.88 (define @t637 () (_ (_ tptp.ord_less_set_nat_nat @t482) @t263)) % 4.62/4.88 (define @t638 () (= @t140 @t364)) % 4.62/4.88 (define @t639 () (@list @t364 @t140)) % 4.62/4.88 (define @t640 () (= @t541 @t542)) % 4.62/4.88 (define @t641 () (@list @t542 @t541)) % 4.62/4.88 (define @t642 () (_ @t631 @t252)) % 4.62/4.88 (define @t643 () (_ tptp.ord_less_set_nat_nat @t476)) % 4.62/4.88 (define @t644 () (_ @t643 @t263)) % 4.62/4.88 (define @t645 () (not @t638)) % 4.62/4.88 (define @t646 () (not @t640)) % 4.62/4.88 (define @t647 () (= @t398 @t213)) % 4.62/4.88 (define @t648 () (@var "J2" tptp.nat)) % 4.62/4.88 (define @t649 () (@var "I4" tptp.nat)) % 4.62/4.88 (define @t650 () (@var "N5" tptp.set_nat)) % 4.62/4.88 (define @t651 () (@var "N4" tptp.set_nat)) % 4.62/4.88 (define @t652 () (_ @t88 @t651)) % 4.62/4.88 (define @t653 () (@list @t398)) % 4.62/4.88 (define @t654 () (@list @t651)) % 4.62/4.88 (define @t655 () (not (_ tptp.finite570312790at_nat @t19))) % 4.62/4.88 (define @t656 () (@var "C2" tptp.nat)) % 4.62/4.88 (define @t657 () (_ (_ tptp.plus_plus_nat @t140) @t656)) % 4.62/4.88 (define @t658 () (= @t364 @t657)) % 4.62/4.88 (define @t659 () (@list @t656)) % 4.62/4.88 (define @t660 () (exists @t659 @t658)) % 4.62/4.88 (define @t661 () (lambda @t365 @t660)) % 4.62/4.88 (define @t662 () (lambda @t654 (exists @t653 (forall @t73 (=> @t652 (_ @t508 @t398)))))) % 4.62/4.88 (define @t663 () (lambda @t563 (forall @t73 (=> @t584 @t583)))) % 4.62/4.88 (define @t664 () (forall @t61 (=> @t586 @t585))) % 4.62/4.88 (define @t665 () (lambda @t567 @t664)) % 4.62/4.88 (define @t666 () (@var "X6" tptp.set_nat)) % 4.62/4.88 (define @t667 () (lambda (@list @t562) (_ tptp.collect_set_nat (lambda (@list @t666) (and (_ (_ tptp.ord_less_eq_set_nat @t666) @t562) (_ tptp.finite_finite_nat @t666)))))) % 4.62/4.88 (define @t668 () (@var "X6" tptp.set_nat_nat_nat)) % 4.62/4.88 (define @t669 () (@var "A5" tptp.set_nat_nat_nat)) % 4.62/4.88 (define @t670 () (lambda (@list @t669) (_ tptp.collec617280953at_nat (lambda (@list @t668) (and (_ (_ tptp.ord_le940807492at_nat @t668) @t669) (_ tptp.finite2045569477at_nat @t668)))))) % 4.62/4.88 (define @t671 () (@var "X6" tptp.set_nat_nat_nat2)) % 4.62/4.88 (define @t672 () (@var "A5" tptp.set_nat_nat_nat2)) % 4.62/4.88 (define @t673 () (lambda (@list @t672) (_ tptp.collec309745849at_nat (lambda (@list @t671) (and (_ (_ tptp.ord_le633272388at_nat @t671) @t672) (_ tptp.finite1440337093at_nat @t671)))))) % 4.62/4.88 (define @t674 () (@var "X6" tptp.set_nat_nat_nat_nat3)) % 4.62/4.88 (define @t675 () (@var "A5" tptp.set_nat_nat_nat_nat3)) % 4.62/4.88 (define @t676 () (lambda (@list @t675) (_ tptp.collec1702444712at_nat (lambda (@list @t674) (and (_ (_ tptp.ord_le2040082867at_nat @t674) @t675) (_ tptp.finite1064868788at_nat @t674)))))) % 4.62/4.88 (define @t677 () (@var "X6" tptp.set_nat_nat)) % 4.62/4.88 (define @t678 () (lambda (@list @t566) (_ tptp.collect_set_nat_nat (lambda (@list @t677) (and (_ (_ tptp.ord_le1415039317at_nat @t677) @t566) (_ tptp.finite570312790at_nat @t677)))))) % 4.62/4.88 (define @t679 () (lambda @t639 (and @t539 @t645))) % 4.62/4.88 (define @t680 () (lambda @t641 (and @t543 @t646))) % 4.62/4.88 (define @t681 () (tptp.number1551313001itions @t15 tptp.n)) % 4.62/4.88 (define @t682 () (lambda @t17 @t681)) % 4.62/4.88 (define @t683 () (@purify @t682)) % 4.62/4.88 (define @t684 () (_ @t683 @t15)) % 4.62/4.88 (define @t685 () (_ @t682 @t15)) % 4.62/4.88 (define @t686 () (= @t684 @t685)) % 4.62/4.88 (define @t687 () (forall @t17 @t686)) % 4.62/4.88 (define @t688 () (@const 0 (-> tptp.nat tptp.nat))) % 4.62/4.88 (define @t689 () (tptp.number1551313001itions @t688 tptp.n)) % 4.62/4.88 (define @t690 () (_ @t683 @t688)) % 4.62/4.88 (define @t691 () (forall @t17 (= @t681 @t684))) % 4.62/4.88 (define @t692 () (= @t689 @t690)) % 4.62/4.88 (define @t693 () (@list @t688)) % 4.62/4.88 (define @t694 () (= @t690 @t689)) % 4.62/4.88 (define @t695 () (@list false)) % 4.62/4.88 (define @t696 () (@var "BOUND_VARIABLE_10704" tptp.nat)) % 4.62/4.88 (define @t697 () (_ (_ tptp.plus_plus_nat @t5) @t696)) % 4.62/4.88 (define @t698 () (@list @t696)) % 4.62/4.88 (define @t699 () (lambda @t12 (and (forall @t7 (not (forall @t659 (not (= tptp.n (_ (_ tptp.plus_plus_nat @t3) @t656)))))) (forall @t698 (= tptp.zero_zero_nat (_ @t2 @t697)))))) % 4.62/4.88 (define @t700 () (tptp.plus_plus_nat tptp.n tptp.one_one_nat)) % 4.62/4.88 (define @t701 () (tptp.plus_plus_nat @t700 @t696)) % 4.62/4.88 (define @t702 () (_ @t2 @t701)) % 4.62/4.88 (define @t703 () (= tptp.zero_zero_nat @t702)) % 4.62/4.88 (define @t704 () (forall @t698 @t703)) % 4.62/4.88 (define @t705 () (tptp.plus_plus_nat @t3 @t656)) % 4.62/4.88 (define @t706 () (_ @t2 @t1)) % 4.62/4.88 (define @t707 () (tptp.plus_plus_nat @t706 @t656)) % 4.62/4.88 (define @t708 () (= tptp.n @t707)) % 4.62/4.88 (define @t709 () (not @t708)) % 4.62/4.88 (define @t710 () (forall @t659 @t709)) % 4.62/4.88 (define @t711 () (not @t710)) % 4.62/4.88 (define @t712 () (forall @t7 @t711)) % 4.62/4.88 (define @t713 () (and @t712 @t704)) % 4.62/4.88 (define @t714 () (lambda @t12 @t713)) % 4.62/4.88 (define @t715 () (tptp.collect_nat_nat @t714)) % 4.62/4.88 (define @t716 () (_ tptp.collect_nat_nat @t714)) % 4.62/4.88 (define @t717 () (tptp.member_nat_nat @t56 @t716)) % 4.62/4.88 (define @t718 () (tptp.collect_nat_nat @t682)) % 4.62/4.88 (define @t719 () (not (tptp.member_nat_nat @t56 @t718))) % 4.62/4.88 (define @t720 () (or @t719 @t717)) % 4.62/4.88 (define @t721 () (forall @t61 @t720)) % 4.62/4.88 (define @t722 () (tptp.member_nat_nat @t56 @t205)) % 4.62/4.88 (define @t723 () (not (= @t701 @t701))) % 4.62/4.88 (define @t724 () (or @t723 @t703)) % 4.62/4.88 (define @t725 () (= tptp.zero_zero_nat @t706)) % 4.62/4.88 (define @t726 () (not (= @t1 @t701))) % 4.62/4.88 (define @t727 () (or @t726 @t726 @t725)) % 4.62/4.88 (define @t728 () (or @t726 @t725)) % 4.62/4.88 (define @t729 () (forall @t7 @t728)) % 4.62/4.88 (define @t730 () (forall @t698 @t729)) % 4.62/4.88 (define @t731 () (forall (@list @t696 @t1) @t728)) % 4.62/4.88 (define @t732 () (forall (@list @t1 @t696) @t728)) % 4.62/4.88 (define @t733 () (forall @t698 @t728)) % 4.62/4.88 (define @t734 () (forall @t698 @t726)) % 4.62/4.88 (define @t735 () (or @t734 @t725)) % 4.62/4.88 (define @t736 () (tptp.plus_plus_nat @t700 @t656)) % 4.62/4.88 (define @t737 () (forall @t659 (not (= @t1 @t736)))) % 4.62/4.88 (define @t738 () (= tptp.zero_zero_nat @t3)) % 4.62/4.88 (define @t739 () (or @t737 @t738)) % 4.62/4.88 (define @t740 () (not @t737)) % 4.62/4.88 (define @t741 () (@list @t364)) % 4.62/4.88 (define @t742 () (tptp.plus_plus_nat @t5 @t656)) % 4.62/4.88 (define @t743 () (= @t364 @t742)) % 4.62/4.88 (define @t744 () (not @t743)) % 4.62/4.88 (define @t745 () (forall @t659 @t744)) % 4.62/4.88 (define @t746 () (not @t745)) % 4.62/4.88 (define @t747 () (lambda @t741 @t746)) % 4.62/4.88 (define @t748 () (tptp.plus_plus_nat @t140 @t656)) % 4.62/4.88 (define @t749 () (lambda @t365 (not (forall @t659 (not (= @t364 @t748)))))) % 4.62/4.88 (define @t750 () (_ @t749 @t5)) % 4.62/4.88 (define @t751 () (=> (_ @t750 @t1) @t4)) % 4.62/4.88 (define @t752 () (forall @t7 @t751)) % 4.62/4.88 (define @t753 () (= @t364 @t705)) % 4.62/4.88 (define @t754 () (not @t753)) % 4.62/4.88 (define @t755 () (forall @t659 @t754)) % 4.62/4.88 (define @t756 () (not @t755)) % 4.62/4.88 (define @t757 () (lambda @t741 @t756)) % 4.62/4.88 (define @t758 () (_ @t749 @t3)) % 4.62/4.88 (define @t759 () (forall @t7 (_ @t758 tptp.n))) % 4.62/4.88 (define @t760 () (and @t759 @t752)) % 4.62/4.88 (define @t761 () (tptp.member_nat_nat @t56 @t19)) % 4.62/4.88 (define @t762 () (not @t761)) % 4.62/4.88 (define @t763 () (or @t762 @t722)) % 4.62/4.88 (define @t764 () (forall @t61 @t763)) % 4.62/4.88 (define @t765 () (lambda @t207 @t764)) % 4.62/4.88 (define @t766 () (tptp.member_nat_nat @t56 @t566)) % 4.62/4.88 (define @t767 () (lambda @t567 (forall @t61 (or (not @t766) @t722)))) % 4.62/4.88 (define @t768 () (not @t658)) % 4.62/4.88 (define @t769 () (forall @t659 @t768)) % 4.62/4.88 (define @t770 () (not @t769)) % 4.62/4.88 (define @t771 () (not @t586)) % 4.62/4.88 (define @t772 () (or @t771 @t585)) % 4.62/4.88 (define @t773 () (@purify @t714)) % 4.62/4.88 (define @t774 () (tptp.collect_nat_nat @t773)) % 4.62/4.88 (define @t775 () (@purify @t18)) % 4.62/4.88 (define @t776 () (tptp.collect_nat_nat @t775)) % 4.62/4.88 (define @t777 () (forall @t61 (or (not (tptp.member_nat_nat @t56 @t776)) (tptp.member_nat_nat @t56 @t774)))) % 4.62/4.88 (define @t778 () (@quantifiers_skolemize @t777 0)) % 4.62/4.88 (define @t779 () (tptp.member_nat_nat @t778 @t715)) % 4.62/4.88 (define @t780 () (tptp.member_nat_nat @t778 @t718)) % 4.62/4.88 (define @t781 () (not @t780)) % 4.62/4.88 (define @t782 () (or @t781 @t779)) % 4.62/4.88 (define @t783 () (forall @t61 (or @t719 (tptp.member_nat_nat @t56 @t715)))) % 4.62/4.88 (define @t784 () (tptp.member_nat_nat @t778 @t774)) % 4.62/4.88 (define @t785 () (tptp.collect_nat_nat @t683)) % 4.62/4.88 (define @t786 () (tptp.member_nat_nat @t778 @t785)) % 4.62/4.88 (define @t787 () (not @t786)) % 4.62/4.88 (define @t788 () (or @t787 @t784)) % 4.62/4.88 (define @t789 () (tptp.finite570312790at_nat @t96)) % 4.62/4.88 (define @t790 () (not (tptp.member_nat_nat @t56 @t96))) % 4.62/4.88 (define @t791 () (forall @t61 (or @t790 (tptp.member_nat_nat @t56 @t104)))) % 4.62/4.88 (define @t792 () (not @t791)) % 4.62/4.88 (define @t793 () (tptp.finite570312790at_nat @t104)) % 4.62/4.88 (define @t794 () (not @t105)) % 4.62/4.88 (define @t795 () (or @t794 @t792 @t100)) % 4.62/4.88 (define @t796 () (=> @t791 @t100)) % 4.62/4.88 (define @t797 () (lambda @t207 (forall @t61 (or @t790 @t722)))) % 4.62/4.88 (define @t798 () (_ @t767 @t96)) % 4.62/4.88 (define @t799 () (=> (_ @t798 @t104) @t100)) % 4.62/4.88 (define @t800 () (=> @t105 @t799)) % 4.62/4.88 (define @t801 () (_ tptp.collect_nat_nat @t773)) % 4.62/4.88 (define @t802 () (tptp.finite570312790at_nat @t774)) % 4.62/4.88 (define @t803 () (_ tptp.collect_nat_nat @t775)) % 4.62/4.88 (define @t804 () (tptp.finite570312790at_nat @t776)) % 4.62/4.88 (define @t805 () (not @t777)) % 4.62/4.88 (define @t806 () (not @t802)) % 4.62/4.88 (define @t807 () (or @t806 @t805 @t804)) % 4.62/4.88 (define @t808 () (@list true false false)) % 4.62/4.88 (define @t809 () (tptp.member_nat_nat @t778 @t776)) % 4.62/4.88 (define @t810 () (not @t809)) % 4.62/4.88 (define @t811 () (or @t810 @t784)) % 4.62/4.88 (define @t812 () (@list true)) % 4.62/4.88 (define @t813 () (@list @t811)) % 4.62/4.88 (define @t814 () (@list true false)) % 4.62/4.88 (define @t815 () (= @t775 @t683)) % 4.62/4.88 (define @t816 () (not @t815)) % 4.62/4.88 (define @t817 () (_ @t775 @t688)) % 4.62/4.88 (define @t818 () (= @t817 @t690)) % 4.62/4.88 (define @t819 () (not @t818)) % 4.62/4.88 (define @t820 () (_ @t775 @t15)) % 4.62/4.88 (define @t821 () (= @t16 @t820)) % 4.62/4.88 (define @t822 () (_ @t18 @t15)) % 4.62/4.88 (define @t823 () (= @t820 @t822)) % 4.62/4.88 (define @t824 () (forall @t17 @t823)) % 4.62/4.88 (define @t825 () (forall @t17 (= @t681 @t820))) % 4.62/4.88 (define @t826 () (= @t689 @t817)) % 4.62/4.88 (define @t827 () (= @t817 @t689)) % 4.62/4.88 (define @t828 () (not @t827)) % 4.62/4.88 (define @t829 () (not @t817)) % 4.62/4.88 (define @t830 () (not @t694)) % 4.62/4.88 (define @t831 () (not @t689)) % 4.62/4.88 (assume @p1 (_ tptp.finite570312790at_nat @t14)) % 4.62/4.88 (assume @p2 (_ (_ tptp.ord_le1415039317at_nat @t19) @t14)) % 4.62/4.88 (assume @p3 (forall @t31 (=> (or @t30 @t28) (_ tptp.finite2045569477at_nat @t26)))) % 4.62/4.88 (assume @p4 (forall @t43 (=> (or @t42 @t40) (_ tptp.finite1440337093at_nat @t38)))) % 4.62/4.88 (assume @p5 (forall @t55 (=> (or @t54 @t52) (_ tptp.finite1064868788at_nat @t50)))) % 4.62/4.88 (assume @p6 (forall @t67 (=> (or @t66 @t64) (_ tptp.finite570312790at_nat @t62)))) % 4.62/4.88 (assume @p7 (forall @t79 (=> (or @t78 @t76) (_ tptp.finite_finite_nat @t74)))) % 4.62/4.88 (assume @p8 (forall @t31 (= (_ tptp.finite2045569477at_nat (_ tptp.collect_nat_nat_nat2 (lambda @t25 (or @t24 @t22)))) (and @t30 @t28)))) % 4.62/4.88 (assume @p9 (forall @t43 (= (_ tptp.finite1440337093at_nat (_ tptp.collect_nat_nat_nat (lambda @t37 (or @t36 @t34)))) (and @t42 @t40)))) % 4.62/4.88 (assume @p10 (forall @t55 (= (_ tptp.finite1064868788at_nat (_ tptp.collec1610646258at_nat (lambda @t49 (or @t48 @t46)))) (and @t54 @t52)))) % 4.62/4.88 (assume @p11 (forall @t67 (= (_ tptp.finite570312790at_nat (_ tptp.collect_nat_nat (lambda @t61 (or @t60 @t58)))) (and @t66 @t64)))) % 4.62/4.88 (assume @p12 (forall @t79 (= (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t73 (or @t72 @t70)))) (and @t78 @t76)))) % 4.62/4.88 (assume @p13 (forall (@list @t80) (= (_ @t81 tptp.zero_zero_nat) (= @t80 (lambda @t7 tptp.zero_zero_nat))))) % 4.62/4.88 (assume @p14 (forall (@list @t80 @t82 @t83) (=> @t84 (_ (_ tptp.ord_less_eq_nat (_ @t80 @t83)) @t82)))) % 4.62/4.88 (assume @p15 (forall (@list @t87 @t91 @t85) (=> @t93 (=> @t92 (_ tptp.finite570312790at_nat (_ tptp.collect_nat_nat (lambda @t12 (forall @t73 (and (=> @t89 (_ (_ tptp.member_nat @t86) @t91)) (=> @t90 (= @t86 @t85))))))))))) % 4.62/4.88 (assume @p16 (forall (@list @t96 @t91 @t85) (=> @t100 (=> @t92 (_ tptp.finite1440337093at_nat (_ tptp.collect_nat_nat_nat (lambda (@list @t94) (forall @t61 (and (=> @t98 (_ (_ tptp.member_nat @t95) @t91)) (=> @t99 (= @t95 @t85))))))))))) % 4.62/4.88 (assume @p17 (forall (@list @t87 @t104 @t101) (=> @t93 (=> @t105 (_ tptp.finite2045569477at_nat (_ tptp.collect_nat_nat_nat2 (lambda (@list @t102) (forall @t73 (and (=> @t89 (_ (_ tptp.member_nat_nat @t103) @t104)) (=> @t90 (= @t103 @t101))))))))))) % 4.62/4.88 (assume @p18 (forall (@list @t96 @t104 @t101) (=> @t100 (=> @t105 (_ tptp.finite1064868788at_nat (_ tptp.collec1610646258at_nat (lambda (@list @t106) (forall @t61 (and (=> @t98 (_ (_ tptp.member_nat_nat @t107) @t104)) (=> @t99 (= @t107 @t101))))))))))) % 4.62/4.88 (assume @p19 (forall (@list @t87 @t111 @t108) (=> @t93 (=> @t112 (_ tptp.finite891768244at_nat (_ tptp.collec1437545714at_nat (lambda (@list @t109) (forall @t73 (and (=> @t89 (_ (_ tptp.member_nat_nat_nat2 @t110) @t111)) (=> @t90 (= @t110 @t108))))))))))) % 4.62/4.88 (assume @p20 (forall (@list @t87 @t116 @t113) (=> @t93 (=> @t117 (_ tptp.finite584233140at_nat (_ tptp.collec1130010610at_nat (lambda (@list @t114) (forall @t73 (and (=> @t89 (_ (_ tptp.member_nat_nat_nat @t115) @t116)) (=> @t90 (= @t115 @t113))))))))))) % 4.62/4.88 (assume @p21 (forall (@list @t120 @t91 @t85) (=> @t123 (=> @t92 (_ tptp.finite2081887156at_nat (_ tptp.collec480180978at_nat (lambda (@list @t118) (forall @t25 (and (=> @t122 (_ (_ tptp.member_nat @t119) @t91)) (=> (not @t122) (= @t119 @t85))))))))))) % 4.62/4.88 (assume @p22 (forall (@list @t126 @t91 @t85) (=> @t129 (=> @t92 (_ tptp.finite1526199988at_nat (_ tptp.collec2071977458at_nat (lambda (@list @t124) (forall @t37 (and (=> @t128 (_ (_ tptp.member_nat @t125) @t91)) (=> (not @t128) (= @t125 @t85))))))))))) % 4.62/4.88 (assume @p23 (forall (@list @t96 @t111 @t108) (=> @t100 (=> @t112 (_ tptp.finite1397812515at_nat (_ tptp.collec314318689at_nat (lambda (@list @t130) (forall @t61 (and (=> @t98 (_ (_ tptp.member_nat_nat_nat2 @t131) @t111)) (=> @t99 (= @t131 @t108))))))))))) % 4.62/4.88 (assume @p24 (forall (@list @t96 @t116 @t113) (=> @t100 (=> @t117 (_ tptp.finite1090277411at_nat (_ tptp.collec6783585at_nat (lambda (@list @t132) (forall @t61 (and (=> @t98 (_ (_ tptp.member_nat_nat_nat @t133) @t116)) (=> @t99 (= @t133 @t113))))))))))) % 4.62/4.88 (assume @p25 (forall (@list @t23) (=> (not @t30) (exists (@list @t134) (_ @t23 @t134))))) % 4.62/4.88 (assume @p26 (forall (@list @t35) (=> (not @t42) (exists (@list @t135) (_ @t35 @t135))))) % 4.62/4.88 (assume @p27 (forall (@list @t47) (=> (not @t54) (exists (@list @t136) (_ @t47 @t136))))) % 4.62/4.88 (assume @p28 (forall (@list @t59) (=> (not @t66) (exists (@list @t137) (_ @t59 @t137))))) % 4.62/4.88 (assume @p29 (forall (@list @t71) (=> (not @t78) (exists (@list @t138) (_ @t71 @t138))))) % 4.62/4.88 (assume @p30 (forall (@list @t87 @t91 @t141) (=> @t152 (=> @t92 (=> (forall @t146 (=> @t151 (exists @t150 (and @t149 (_ (_ @t141 @t139) @t147))))) (exists @t146 (and @t145 (not (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t143 (and @t142 (_ (_ @t141 @t140) @t139))))))))))))) % 4.62/4.88 (assume @p31 (forall (@list @t96 @t91 @t154) (=> @t161 (=> @t92 (=> (forall @t160 (=> @t159 (exists @t150 (and @t149 (_ (_ @t154 @t157) @t147))))) (exists @t146 (and @t145 (not (_ tptp.finite570312790at_nat (_ tptp.collect_nat_nat (lambda @t156 (and @t155 (_ (_ @t154 @t153) @t139))))))))))))) % 4.62/4.88 (assume @p32 (forall (@list @t87 @t104 @t162) (=> @t152 (=> @t105 (=> (forall @t146 (=> @t151 (exists @t167 (and @t166 (_ (_ @t162 @t139) @t164))))) (exists @t160 (and @t163 (not (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t143 (and @t142 (_ (_ @t162 @t140) @t157))))))))))))) % 4.62/4.88 (assume @p33 (forall (@list @t96 @t104 @t168) (=> @t161 (=> @t105 (=> (forall @t160 (=> @t159 (exists @t167 (and @t166 (_ (_ @t168 @t157) @t164))))) (exists @t160 (and @t163 (not (_ tptp.finite570312790at_nat (_ tptp.collect_nat_nat (lambda @t156 (and @t155 (_ (_ @t168 @t153) @t157))))))))))))) % 4.62/4.88 (assume @p34 (forall (@list @t87 @t111 @t170) (=> @t152 (=> @t112 (=> (forall @t146 (=> @t151 (exists @t177 (and @t176 (_ (_ @t170 @t139) @t174))))) (exists @t173 (and @t172 (not (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t143 (and @t142 (_ (_ @t170 @t140) @t169))))))))))))) % 4.62/4.88 (assume @p35 (forall (@list @t87 @t116 @t179) (=> @t152 (=> @t117 (=> (forall @t146 (=> @t151 (exists @t186 (and @t185 (_ (_ @t179 @t139) @t183))))) (exists @t182 (and @t181 (not (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t143 (and @t142 (_ (_ @t179 @t140) @t178))))))))))))) % 4.62/4.88 (assume @p36 (forall (@list @t120 @t91 @t188) (=> (not @t123) (=> @t92 (=> (forall @t173 (=> @t189 (exists @t150 (and @t149 (_ (_ @t188 @t169) @t147))))) (exists @t146 (and @t145 (not (_ tptp.finite2045569477at_nat (_ tptp.collect_nat_nat_nat2 (lambda (@list @t187) (and (_ (_ tptp.member_nat_nat_nat2 @t187) @t120) (_ (_ @t188 @t187) @t139))))))))))))) % 4.62/4.88 (assume @p37 (forall (@list @t126 @t91 @t191) (=> (not @t129) (=> @t92 (=> (forall @t182 (=> @t192 (exists @t150 (and @t149 (_ (_ @t191 @t178) @t147))))) (exists @t146 (and @t145 (not (_ tptp.finite1440337093at_nat (_ tptp.collect_nat_nat_nat (lambda (@list @t190) (and (_ (_ tptp.member_nat_nat_nat @t190) @t126) (_ (_ @t191 @t190) @t139))))))))))))) % 4.62/4.88 (assume @p38 (forall (@list @t96 @t111 @t193) (=> @t161 (=> @t112 (=> (forall @t160 (=> @t159 (exists @t177 (and @t176 (_ (_ @t193 @t157) @t174))))) (exists @t173 (and @t172 (not (_ tptp.finite570312790at_nat (_ tptp.collect_nat_nat (lambda @t156 (and @t155 (_ (_ @t193 @t153) @t169))))))))))))) % 4.62/4.88 (assume @p39 (forall (@list @t96 @t116 @t194) (=> @t161 (=> @t117 (=> (forall @t160 (=> @t159 (exists @t186 (and @t185 (_ (_ @t194 @t157) @t183))))) (exists @t182 (and @t181 (not (_ tptp.finite570312790at_nat (_ tptp.collect_nat_nat (lambda @t156 (and @t155 (_ (_ @t194 @t153) @t178))))))))))))) % 4.62/4.88 (assume @p40 (forall @t196 (=> @t93 (_ tptp.finite2012248349et_nat (_ tptp.collect_set_nat (lambda (@list @t195) (_ (_ tptp.ord_less_eq_set_nat @t195) @t87))))))) % 4.62/4.88 (assume @p41 (forall @t198 (=> @t123 (_ tptp.finite137548155at_nat (_ tptp.collec617280953at_nat (lambda (@list @t197) (_ (_ tptp.ord_le940807492at_nat @t197) @t120))))))) % 4.62/4.88 (assume @p42 (forall @t200 (=> @t129 (_ tptp.finite1977496699at_nat (_ tptp.collec309745849at_nat (lambda (@list @t199) (_ (_ tptp.ord_le633272388at_nat @t199) @t126))))))) % 4.62/4.88 (assume @p43 (forall @t204 (=> @t203 (_ tptp.finite547180394at_nat (_ tptp.collec1702444712at_nat (lambda (@list @t202) (_ (_ tptp.ord_le2040082867at_nat @t202) @t201))))))) % 4.62/4.88 (assume @p44 (forall @t208 (=> @t100 (_ tptp.finite604103692at_nat (_ tptp.collect_set_nat_nat (lambda @t207 (_ @t206 @t96))))))) % 4.62/4.88 (assume @p45 (forall @t211 (_ tptp.finite570312790at_nat (_ tptp.collect_nat_nat (lambda @t12 (and (forall @t7 (_ @t9 @t82)) (forall @t7 (=> (_ @t210 @t1) @t4)))))))) % 4.62/4.88 (assume @p46 (forall @t215 (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t214 (_ (_ tptp.ord_less_eq_nat @t213) @t212)))))) % 4.62/4.88 (assume @p47 (forall @t222 (=> @t100 (=> @t221 (exists @t160 (and @t159 (_ @t219 @t218) (forall @t167 (=> @t217 (=> (_ (_ tptp.ord_less_eq_nat_nat @t164) @t157) @t216))))))))) % 4.62/4.88 (assume @p48 (forall @t229 (=> @t123 (=> @t228 (exists @t173 (and @t189 (_ @t226 @t225) (forall @t177 (=> @t224 (=> (_ (_ tptp.ord_le1415139726at_nat @t174) @t169) @t223))))))))) % 4.62/4.88 (assume @p49 (forall @t236 (=> @t129 (=> @t235 (exists @t182 (and @t192 (_ @t233 @t232) (forall @t186 (=> @t231 (=> (_ (_ tptp.ord_le809907342at_nat @t183) @t178) @t230))))))))) % 4.62/4.88 (assume @p50 (forall @t249 (=> @t203 (=> @t248 (exists @t246 (and @t245 (_ @t243 @t242) (forall @t241 (=> @t240 (=> (_ (_ tptp.ord_le2059018749at_nat @t237) @t238) @t239))))))))) % 4.62/4.88 (assume @p51 (forall @t256 (=> @t93 (=> @t255 (exists @t146 (and @t151 (_ @t253 @t252) (forall @t150 (=> @t251 (=> (_ (_ tptp.ord_less_eq_nat @t147) @t139) @t250))))))))) % 4.62/4.88 (assume @p52 (forall @t269 (=> @t268 (=> @t267 (exists @t266 (and @t265 (_ @t264 @t263) (forall @t262 (=> @t261 (=> (_ (_ tptp.ord_le1415039317at_nat @t257) @t258) @t259))))))))) % 4.62/4.88 (assume @p53 (forall @t222 (=> @t100 (=> @t221 (exists @t160 (and @t159 (_ (_ tptp.ord_less_eq_nat_nat @t218) @t157) (forall @t167 (=> @t217 (=> (_ @t219 @t164) @t216))))))))) % 4.62/4.88 (assume @p54 (forall @t229 (=> @t123 (=> @t228 (exists @t173 (and @t189 (_ (_ tptp.ord_le1415139726at_nat @t225) @t169) (forall @t177 (=> @t224 (=> (_ @t226 @t174) @t223))))))))) % 4.62/4.88 (assume @p55 (forall @t236 (=> @t129 (=> @t235 (exists @t182 (and @t192 (_ (_ tptp.ord_le809907342at_nat @t232) @t178) (forall @t186 (=> @t231 (=> (_ @t233 @t183) @t230))))))))) % 4.62/4.88 (assume @p56 (forall @t249 (=> @t203 (=> @t248 (exists @t246 (and @t245 (_ (_ tptp.ord_le2059018749at_nat @t242) @t238) (forall @t241 (=> @t240 (=> (_ @t243 @t237) @t239))))))))) % 4.62/4.88 (assume @p57 (forall @t256 (=> @t93 (=> @t255 (exists @t146 (and @t151 (_ @t270 @t139) (forall @t150 (=> @t251 (=> (_ @t253 @t147) @t250))))))))) % 4.62/4.88 (assume @p58 (forall @t269 (=> @t268 (=> @t267 (exists @t266 (and @t265 (_ @t271 @t258) (forall @t262 (=> @t261 (=> (_ @t264 @t257) @t259))))))))) % 4.62/4.88 (assume @p59 (forall (@list @t91 @t87) (=> @t92 (=> @t273 @t93)))) % 4.62/4.88 (assume @p60 (forall (@list @t111 @t120) (=> @t112 (=> @t275 @t123)))) % 4.62/4.88 (assume @p61 (forall (@list @t116 @t126) (=> @t117 (=> @t277 @t129)))) % 4.62/4.88 (assume @p62 (forall (@list @t278 @t201) (=> @t281 (=> @t280 @t203)))) % 4.62/4.88 (assume @p63 @t287) % 4.62/4.88 (assume @p64 (forall (@list @t289 @t288) (=> (_ (_ tptp.ord_less_eq_set_nat @t289) @t288) (=> (not (_ tptp.finite_finite_nat @t289)) (not (_ tptp.finite_finite_nat @t288)))))) % 4.62/4.88 (assume @p65 (forall (@list @t291 @t290) (=> (_ (_ tptp.ord_le940807492at_nat @t291) @t290) (=> (not (_ tptp.finite2045569477at_nat @t291)) (not (_ tptp.finite2045569477at_nat @t290)))))) % 4.62/4.88 (assume @p66 (forall (@list @t293 @t292) (=> (_ (_ tptp.ord_le633272388at_nat @t293) @t292) (=> (not (_ tptp.finite1440337093at_nat @t293)) (not (_ tptp.finite1440337093at_nat @t292)))))) % 4.62/4.88 (assume @p67 (forall (@list @t295 @t294) (=> (_ (_ tptp.ord_le2040082867at_nat @t295) @t294) (=> (not (_ tptp.finite1064868788at_nat @t295)) (not (_ tptp.finite1064868788at_nat @t294)))))) % 4.62/4.88 (assume @p68 (forall (@list @t297 @t296) (=> (_ (_ tptp.ord_le1415039317at_nat @t297) @t296) (=> (not (_ tptp.finite570312790at_nat @t297)) (not (_ tptp.finite570312790at_nat @t296)))))) % 4.62/4.88 (assume @p69 (forall @t298 (=> @t273 (=> @t92 @t93)))) % 4.62/4.88 (assume @p70 (forall (@list @t120 @t111) (=> @t275 (=> @t112 @t123)))) % 4.62/4.88 (assume @p71 (forall (@list @t126 @t116) (=> @t277 (=> @t117 @t129)))) % 4.62/4.88 (assume @p72 (forall (@list @t201 @t278) (=> @t280 (=> @t281 @t203)))) % 4.62/4.88 (assume @p73 (forall @t299 (=> @t283 (=> @t105 @t100)))) % 4.62/4.88 (assume @p74 (forall @t304 (= (_ (_ tptp.ord_less_eq_nat @t303) @t301) @t300))) % 4.62/4.88 (assume @p75 (forall @t308 (= (_ @t307 @t301) @t300))) % 4.62/4.88 (assume @p76 (forall @t308 (= (_ @t270 @t306) @t310))) % 4.62/4.88 (assume @p77 (forall @t308 (= (_ @t270 @t303) @t310))) % 4.62/4.88 (assume @p78 (forall @t315 (= (_ (_ tptp.ord_less_eq_nat @t314) @t313) @t311))) % 4.62/4.88 (assume @p79 (forall @t319 (= (= @t318 tptp.zero_zero_nat) (and (= @t209 tptp.zero_zero_nat) @t316)))) % 4.62/4.88 (assume @p80 (forall (@list @t209) (= (_ @t317 tptp.zero_zero_nat) @t209))) % 4.62/4.88 (assume @p81 (forall @t320 (_ @t309 @t82))) % 4.62/4.88 (assume @p82 (forall @t322 @t321)) % 4.62/4.88 (assume @p83 (forall @t328 (= @t327 @t324))) % 4.62/4.88 (assume @p84 (forall @t331 (= @t330 @t324))) % 4.62/4.88 (assume @p85 (forall @t320 (= (_ @t332 tptp.zero_zero_nat) @t316))) % 4.62/4.88 (assume @p86 (forall @t337 (= @t336 @t333))) % 4.62/4.88 (assume @p87 (forall @t340 (= @t339 @t333))) % 4.62/4.88 (assume @p88 (forall @t346 (= (= tptp.zero_zero_nat @t345) @t344))) % 4.62/4.88 (assume @p89 (forall @t346 @t347)) % 4.62/4.88 (assume @p90 (forall @t308 (= (= @t252 @t306) @t348))) % 4.62/4.88 (assume @p91 (forall @t308 (= (= @t252 @t303) @t348))) % 4.62/4.88 (assume @p92 (forall @t308 (= (= @t306 @t252) @t348))) % 4.62/4.88 (assume @p93 (forall @t304 (= (= @t303 @t252) @t348))) % 4.62/4.88 (assume @p94 (forall (@list @t218 @t59) (= (_ @t220 @t65) (_ @t59 @t218)))) % 4.62/4.88 (assume @p95 (forall (@list @t252 @t71) (= (_ @t254 @t77) (_ @t71 @t252)))) % 4.62/4.88 (assume @p96 (forall (@list @t225 @t23) (= (_ @t227 @t29) (_ @t23 @t225)))) % 4.62/4.88 (assume @p97 (forall (@list @t232 @t35) (= (_ @t234 @t41) (_ @t35 @t232)))) % 4.62/4.88 (assume @p98 (forall (@list @t242 @t47) (= (_ @t247 @t53) (_ @t47 @t242)))) % 4.62/4.88 (assume @p99 (forall @t208 (= (_ tptp.collect_nat_nat (lambda @t61 @t98)) @t96))) % 4.62/4.88 (assume @p100 (forall @t196 (= (_ tptp.collect_nat (lambda @t73 @t89)) @t87))) % 4.62/4.88 (assume @p101 (forall @t198 (= (_ tptp.collect_nat_nat_nat2 (lambda @t25 @t122)) @t120))) % 4.62/4.88 (assume @p102 (forall @t200 (= (_ tptp.collect_nat_nat_nat (lambda @t37 @t128)) @t126))) % 4.62/4.88 (assume @p103 (forall @t204 (= (_ tptp.collec1610646258at_nat (lambda @t49 @t350)) @t201))) % 4.62/4.88 (assume @p104 (forall @t67 (=> (forall @t160 (= @t352 @t351)) (= @t65 @t63)))) % 4.62/4.88 (assume @p105 (forall @t79 (=> (forall @t146 (= @t354 @t353)) (= @t77 @t75)))) % 4.62/4.88 (assume @p106 (forall @t31 (=> (forall @t173 (= @t356 @t355)) (= @t29 @t27)))) % 4.62/4.88 (assume @p107 (forall @t43 (=> (forall @t182 (= @t358 @t357)) (= @t41 @t39)))) % 4.62/4.88 (assume @p108 (forall @t55 (=> (forall @t246 (= @t360 @t359)) (= @t53 @t51)))) % 4.62/4.88 (assume @p109 (forall @t322 (= (_ @t305 tptp.zero_zero_nat) @t252))) % 4.62/4.88 (assume @p110 (forall @t322 (= (_ @t361 @t252) @t252))) % 4.62/4.88 (assume @p111 (forall @t362 (= (= tptp.zero_zero_nat @t342) @t343))) % 4.62/4.88 (assume @p112 (forall @t328 (=> @t327 @t324))) % 4.62/4.88 (assume @p113 (forall @t331 (=> @t330 @t324))) % 4.62/4.88 (assume @p114 (forall @t328 (= (_ @t302 @t329) @t363))) % 4.62/4.88 (assume @p115 (= tptp.plus_plus_nat (lambda @t365 (_ (_ tptp.plus_plus_nat @t364) @t140)))) % 4.62/4.88 (assume @p116 (forall @t331 (= (_ (_ tptp.plus_plus_nat @t306) @t323) @t363))) % 4.62/4.88 (assume @p117 (forall (@list @t367 @t212 @t301 @t252) (=> (= @t367 (_ @t312 @t301)) (= (_ @t305 @t367) @t366)))) % 4.62/4.88 (assume @p118 (forall (@list @t368 @t212 @t252 @t301) (=> (= @t368 (_ @t312 @t252)) (= (_ (_ tptp.plus_plus_nat @t368) @t301) @t366)))) % 4.62/4.88 (assume @p119 (forall @t376 (=> (and @t375 @t374) (= @t373 @t372)))) % 4.62/4.88 (assume @p120 (forall @t362 (= (= tptp.one_one_nat @t342) (= @t342 tptp.one_one_nat)))) % 4.62/4.88 (assume @p121 (forall (@list @t71 @t212 @t301) (=> (_ @t71 @t212) (=> (forall (@list @t378) (=> (_ @t71 @t378) (_ (_ tptp.ord_less_eq_nat @t378) @t301))) (exists @t146 (and @t354 (forall (@list @t377) (=> (_ @t71 @t377) (_ (_ tptp.ord_less_eq_nat @t377) @t139))))))))) % 4.62/4.88 (assume @p122 (forall @t319 (or @t311 @t379))) % 4.62/4.88 (assume @p123 (forall @t319 (=> @t311 (=> @t379 @t380)))) % 4.62/4.88 (assume @p124 (forall @t319 (=> @t380 @t311))) % 4.62/4.88 (assume @p125 (forall @t383 (=> @t382 (=> (_ (_ tptp.ord_less_eq_nat @t370) @t212) (_ @t381 @t212))))) % 4.62/4.88 (assume @p126 (forall @t320 (_ @t332 @t82))) % 4.62/4.88 (assume @p127 (forall @t362 @t384)) % 4.62/4.88 (assume @p128 (forall @t337 (=> @t336 @t333))) % 4.62/4.88 (assume @p129 (forall @t340 (=> @t339 @t333))) % 4.62/4.88 (assume @p130 (forall @t331 (=> @t333 @t336))) % 4.62/4.88 (assume @p131 (forall @t308 (=> @t333 (not (forall @t387 (not @t386)))))) % 4.62/4.88 (assume @p132 (forall @t331 (=> @t333 @t339))) % 4.62/4.88 (assume @p133 (forall @t391 (=> @t333 (=> @t390 (_ @t335 @t388))))) % 4.62/4.88 (assume @p134 (forall @t376 (=> (and @t382 @t395) @t393))) % 4.62/4.88 (assume @p135 (forall @t376 (=> (and @t375 @t395) @t393))) % 4.62/4.88 (assume @p136 (forall @t376 (=> (and @t382 @t374) @t393))) % 4.62/4.88 (assume @p137 (forall @t322 (=> @t300 @t396))) % 4.62/4.88 (assume @p138 (forall @t322 (= @t300 @t396))) % 4.62/4.88 (assume @p139 (forall @t319 (=> (= @t318 @t209) @t316))) % 4.62/4.88 (assume @p140 (forall @t320 (= (_ @t361 @t82) @t82))) % 4.62/4.88 (assume @p141 (= tptp.ord_less_eq_nat (lambda @t400 (exists @t399 (= @t213 (_ (_ tptp.plus_plus_nat @t398) @t397)))))) % 4.62/4.88 (assume @p142 (forall @t401 (=> @t382 (_ @t381 (_ @t317 @t370))))) % 4.62/4.88 (assume @p143 (forall @t401 (=> @t382 (_ @t381 (_ @t371 @t209))))) % 4.62/4.88 (assume @p144 (forall @t383 (=> @t382 (_ @t392 (_ @t371 @t212))))) % 4.62/4.88 (assume @p145 (forall @t376 (=> @t382 (=> @t395 @t393)))) % 4.62/4.88 (assume @p146 (forall (@list @t212 @t369) (=> @t395 (exists @t403 (= @t369 (_ @t312 @t402)))))) % 4.62/4.88 (assume @p147 (forall @t406 (=> @t405 @t404))) % 4.62/4.88 (assume @p148 (forall @t406 (=> @t405 @t311))) % 4.62/4.88 (assume @p149 (forall @t211 (_ @t332 @t318))) % 4.62/4.88 (assume @p150 (forall @t211 (_ @t332 (_ (_ tptp.plus_plus_nat @t82) @t209)))) % 4.62/4.88 (assume @p151 (forall @t406 (=> @t405 (not (=> @t311 (not @t404)))))) % 4.62/4.88 (assume @p152 (forall @t346 (=> (_ @t408 tptp.zero_zero_nat) (=> (_ @t407 tptp.zero_zero_nat) @t347)))) % 4.62/4.88 (assume @p153 (forall @t346 (=> @t384 (=> (_ @t309 @t341) @t347)))) % 4.62/4.88 (assume @p154 (forall @t308 (=> @t300 (=> (_ @t409 tptp.zero_zero_nat) (_ @t307 tptp.zero_zero_nat))))) % 4.62/4.88 (assume @p155 (forall @t308 (=> @t321 (=> @t310 (_ @t309 @t306))))) % 4.62/4.88 (assume @p156 (forall (@list @t323 @t301 @t252) (=> (_ @t309 @t323) (=> @t411 @t410)))) % 4.62/4.88 (assume @p157 (forall @t340 (=> (_ @t389 tptp.zero_zero_nat) (=> @t333 @t412)))) % 4.62/4.88 (assume @p158 (forall @t331 (=> @t321 (=> @t413 @t410)))) % 4.62/4.88 (assume @p159 (forall @t337 (=> @t300 (=> @t414 @t412)))) % 4.62/4.88 (assume @p160 (forall (@list @t420 @t418 @t416) (=> (_ tptp.finite570312790at_nat (_ tptp.collect_nat_nat (lambda @t422 (and @t421 (not (= @t419 tptp.zero_zero_nat)))))) (=> (_ tptp.finite570312790at_nat (_ tptp.collect_nat_nat (lambda @t422 (and @t421 (not (= @t417 tptp.zero_zero_nat)))))) (_ tptp.finite570312790at_nat (_ tptp.collect_nat_nat (lambda @t422 (and @t421 (not (= (_ (_ tptp.plus_plus_nat @t419) @t417) tptp.zero_zero_nat)))))))))) % 4.62/4.88 (assume @p161 (forall (@list @t427 @t425 @t423) (=> (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t7 (and @t428 (not (= @t426 tptp.zero_zero_nat)))))) (=> (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t7 (and @t428 (not (= @t424 tptp.zero_zero_nat)))))) (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t7 (and @t428 (not (= (_ (_ tptp.plus_plus_nat @t426) @t424) tptp.zero_zero_nat)))))))))) % 4.62/4.88 (assume @p162 (forall (@list @t434 @t432 @t430) (=> (_ tptp.finite2045569477at_nat (_ tptp.collect_nat_nat_nat2 (lambda @t436 (and @t435 (not (= @t433 tptp.zero_zero_nat)))))) (=> (_ tptp.finite2045569477at_nat (_ tptp.collect_nat_nat_nat2 (lambda @t436 (and @t435 (not (= @t431 tptp.zero_zero_nat)))))) (_ tptp.finite2045569477at_nat (_ tptp.collect_nat_nat_nat2 (lambda @t436 (and @t435 (not (= (_ (_ tptp.plus_plus_nat @t433) @t431) tptp.zero_zero_nat)))))))))) % 4.62/4.88 (assume @p163 (forall (@list @t442 @t440 @t438) (=> (_ tptp.finite1440337093at_nat (_ tptp.collect_nat_nat_nat (lambda @t444 (and @t443 (not (= @t441 tptp.zero_zero_nat)))))) (=> (_ tptp.finite1440337093at_nat (_ tptp.collect_nat_nat_nat (lambda @t444 (and @t443 (not (= @t439 tptp.zero_zero_nat)))))) (_ tptp.finite1440337093at_nat (_ tptp.collect_nat_nat_nat (lambda @t444 (and @t443 (not (= (_ (_ tptp.plus_plus_nat @t441) @t439) tptp.zero_zero_nat)))))))))) % 4.62/4.88 (assume @p164 (forall (@list @t450 @t448 @t446) (=> (_ tptp.finite1064868788at_nat (_ tptp.collec1610646258at_nat (lambda @t452 (and @t451 (not (= @t449 tptp.zero_zero_nat)))))) (=> (_ tptp.finite1064868788at_nat (_ tptp.collec1610646258at_nat (lambda @t452 (and @t451 (not (= @t447 tptp.zero_zero_nat)))))) (_ tptp.finite1064868788at_nat (_ tptp.collec1610646258at_nat (lambda @t452 (and @t451 (not (= (_ (_ tptp.plus_plus_nat @t449) @t447) tptp.zero_zero_nat)))))))))) % 4.62/4.88 (assume @p165 (not (_ @t453 tptp.zero_zero_nat))) % 4.62/4.88 (assume @p166 (_ @t309 tptp.one_one_nat)) % 4.62/4.88 (assume @p167 (forall (@list @t455 @t454) (=> (forall @t403 (_ (_ tptp.ord_less_eq_nat @t402) (_ @t455 @t402))) (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t214 (_ (_ tptp.ord_less_eq_nat (_ @t455 @t213)) @t454))))))) % 4.62/4.88 (assume @p168 (forall @t299 (=> @t283 (=> @t458 @t456)))) % 4.62/4.88 (assume @p169 (forall @t298 (=> (forall @t146 (=> @t151 @t145)) @t273))) % 4.62/4.88 (assume @p170 (forall @t299 (=> (forall @t160 (=> @t159 @t163)) @t283))) % 4.62/4.88 (assume @p171 (forall @t362 (_ @t408 @t342))) % 4.62/4.88 (assume @p172 (forall (@list @t459) (_ @t460 @t459))) % 4.62/4.88 (assume @p173 (forall @t469 (=> (forall @t467 (= @t466 @t468)) (=> (forall (@list @t464) (_ @t465 tptp.zero_zero_nat)) (=> (forall @t467 (=> @t466 (_ @t465 (_ (_ tptp.plus_plus_nat @t464) @t463)))) @t462))))) % 4.62/4.88 (assume @p174 (forall @t475 (=> (_ @t270 @t474) @t473))) % 4.62/4.88 (assume @p175 (forall @t487 (=> (_ @t270 @t486) @t485))) % 4.62/4.88 (assume @p176 (forall @t492 (=> (_ @t271 @t491) @t490))) % 4.62/4.88 (assume @p177 (forall @t497 (=> (_ @t271 @t496) @t495))) % 4.62/4.88 (assume @p178 (forall @t499 (=> @t333 (=> (_ (_ tptp.ord_less_eq_nat @t474) @t323) @t498)))) % 4.62/4.88 (assume @p179 (forall @t501 (=> @t333 (=> (_ (_ tptp.ord_le1415039317at_nat @t491) @t476) @t500)))) % 4.62/4.88 (assume @p180 (forall @t504 (=> @t503 (=> (_ (_ tptp.ord_less_eq_nat @t486) @t323) @t502)))) % 4.62/4.88 (assume @p181 (forall @t506 (=> @t503 (=> (_ (_ tptp.ord_le1415039317at_nat @t496) @t476) @t505)))) % 4.62/4.88 (assume @p182 (forall @t475 (=> (= @t252 @t474) @t473))) % 4.62/4.88 (assume @p183 (forall @t492 (=> (= @t263 @t491) @t490))) % 4.62/4.88 (assume @p184 (forall @t487 (=> (= @t252 @t486) @t485))) % 4.62/4.88 (assume @p185 (forall @t497 (=> (= @t263 @t496) @t495))) % 4.62/4.88 (assume @p186 (forall @t499 (=> @t333 (=> (= @t474 @t323) @t498)))) % 4.62/4.88 (assume @p187 (forall @t501 (=> @t333 (=> (= @t491 @t476) @t500)))) % 4.62/4.88 (assume @p188 (forall @t504 (=> @t503 (=> (= @t486 @t323) @t502)))) % 4.62/4.88 (assume @p189 (forall @t506 (=> @t503 (=> (= @t496 @t476) @t505)))) % 4.62/4.88 (assume @p190 (= @t511 (lambda (@list @t68 @t507) (and (_ @t508 @t507) (_ (_ tptp.ord_less_eq_nat @t507) @t68))))) % 4.62/4.88 (assume @p191 (= @t516 (lambda (@list @t512 @t513) (and (_ (_ tptp.ord_le1415039317at_nat @t512) @t513) (_ (_ tptp.ord_le1415039317at_nat @t513) @t512))))) % 4.62/4.88 (assume @p192 (forall @t346 (=> @t519 (=> @t518 @t517)))) % 4.62/4.88 (assume @p193 (forall @t525 (=> @t524 (=> @t523 @t521)))) % 4.62/4.88 (assume @p194 (forall @t346 (or @t519 @t518))) % 4.62/4.88 (assume @p195 (forall @t346 (=> @t517 @t519))) % 4.62/4.88 (assume @p196 (forall @t525 (=> @t521 @t524))) % 4.62/4.88 (assume @p197 (forall @t346 (=> @t526 @t518))) % 4.62/4.88 (assume @p198 (forall @t331 (=> @t333 @t528))) % 4.62/4.88 (assume @p199 (forall @t531 (=> @t503 @t530))) % 4.62/4.88 (assume @p200 (forall @t538 (=> (=> @t519 (not @t535)) (=> (=> @t518 (not @t537)) (=> (=> @t537 (not @t536)) (=> (=> @t536 (not @t518)) (=> (=> @t535 (not @t534)) (not (=> @t534 @t526))))))))) % 4.62/4.88 (assume @p201 (forall (@list @t341 @t342) (=> @t518 (= @t519 @t517)))) % 4.62/4.88 (assume @p202 (forall (@list @t520 @t459) (=> @t523 (= @t524 @t521)))) % 4.62/4.88 (assume @p203 (= @t511 (lambda @t365 (and @t540 @t539)))) % 4.62/4.88 (assume @p204 (= @t516 (lambda @t545 (and @t544 @t543)))) % 4.62/4.88 (assume @p205 (forall @t331 (=> @t546 @t528))) % 4.62/4.88 (assume @p206 (forall @t531 (=> @t547 @t530))) % 4.62/4.88 (assume @p207 (forall @t331 (=> @t333 (=> @t324 @t527)))) % 4.62/4.88 (assume @p208 (forall @t531 (=> @t503 (=> (= @t482 @t476) @t529)))) % 4.62/4.88 (assume @p209 (forall @t308 (=> @t333 (=> @t411 @t546)))) % 4.62/4.88 (assume @p210 (forall @t549 (=> @t503 (=> @t548 @t547)))) % 4.62/4.88 (assume @p211 (forall @t538 (=> @t519 (=> @t535 @t537)))) % 4.62/4.88 (assume @p212 (forall (@list @t459 @t520 @t550) (=> @t524 (=> (_ @t522 @t550) (_ @t460 @t550))))) % 4.62/4.88 (assume @p213 (forall @t322 (_ @t270 @t252))) % 4.62/4.88 (assume @p214 (forall (@list @t263) (_ @t271 @t263))) % 4.62/4.88 (assume @p215 (forall @t469 (=> (forall @t467 (=> (_ (_ tptp.ord_less_eq_nat @t464) @t463) @t466)) (=> (forall @t467 (=> @t468 @t466)) @t462)))) % 4.62/4.88 (assume @p216 (forall @t328 (=> @t411 (=> @t414 (_ @t389 @t252))))) % 4.62/4.88 (assume @p217 (forall @t553 (=> @t548 (=> @t552 (_ @t551 @t263))))) % 4.62/4.88 (assume @p218 (= @t511 (lambda @t365 (and @t539 @t540)))) % 4.62/4.88 (assume @p219 (= @t516 (lambda @t545 (and @t543 @t544)))) % 4.62/4.88 (assume @p220 (forall @t304 (=> @t411 (=> @t333 @t546)))) % 4.62/4.88 (assume @p221 (forall @t554 (=> @t548 (=> @t503 @t547)))) % 4.62/4.88 (assume @p222 (forall (@list @t87 @t91 @t342) (=> @t273 (=> (_ @t555 @t87) (_ @t555 @t91))))) % 4.62/4.88 (assume @p223 (forall (@list @t96 @t104 @t425) (=> @t283 (=> (_ @t556 @t96) (_ @t556 @t104))))) % 4.62/4.88 (assume @p224 (forall (@list @t87 @t91 @t323) (=> @t273 (=> (_ @t557 @t87) (_ @t557 @t91))))) % 4.62/4.88 (assume @p225 (forall (@list @t96 @t104 @t558) (=> @t283 (=> (_ @t559 @t96) (_ @t559 @t104))))) % 4.62/4.88 (assume @p226 (forall @t299 (=> @t456 (not (=> @t283 (not @t458)))))) % 4.62/4.88 (assume @p227 (forall @t299 (=> @t456 @t283))) % 4.62/4.88 (assume @p228 (forall @t299 (=> @t456 @t458))) % 4.62/4.88 (assume @p229 (= tptp.ord_less_eq_set_nat (lambda @t563 (forall (@list @t560) (=> (_ @t561 @t562) (_ @t561 @t195)))))) % 4.62/4.88 (assume @p230 (= tptp.ord_le1415039317at_nat (lambda @t567 (forall (@list @t564) (=> (_ @t565 @t566) (_ @t565 @t205)))))) % 4.62/4.88 (assume @p231 (forall @t208 (_ @t282 @t96))) % 4.62/4.88 (assume @p232 (forall @t79 (=> (forall @t146 (=> @t354 @t353)) @t568))) % 4.62/4.88 (assume @p233 (forall @t31 (=> (forall @t173 (=> @t356 @t355)) @t569))) % 4.62/4.88 (assume @p234 (forall @t43 (=> (forall @t182 (=> @t358 @t357)) @t570))) % 4.62/4.88 (assume @p235 (forall @t55 (=> (forall @t246 (=> @t360 @t359)) @t571))) % 4.62/4.88 (assume @p236 (forall @t67 (=> (forall @t160 (=> @t352 @t351)) @t572))) % 4.62/4.88 (assume @p237 (forall (@list @t96 @t104 @t573) (=> @t283 (=> (_ @t457 @t573) (_ @t282 @t573))))) % 4.62/4.88 (assume @p238 (= @t516 (lambda @t567 (and (_ (_ tptp.ord_le1415039317at_nat @t566) @t205) (_ @t206 @t566))))) % 4.62/4.88 (assume @p239 (forall @t79 (= @t568 (forall @t73 (=> @t72 @t70))))) % 4.62/4.88 (assume @p240 (forall @t31 (= @t569 (forall @t25 (=> @t24 @t22))))) % 4.62/4.88 (assume @p241 (forall @t43 (= @t570 (forall @t37 (=> @t36 @t34))))) % 4.62/4.88 (assume @p242 (forall @t55 (= @t571 (forall @t49 (=> @t48 @t46))))) % 4.62/4.88 (assume @p243 (forall @t67 (= @t572 (forall @t61 (=> @t60 @t58))))) % 4.62/4.88 (assume @p244 (forall (@list @t71 @t342 @t576) (=> @t577 (=> (forall @t146 (=> @t354 (_ @t253 @t576))) (not (forall (@list @t574) (=> (_ @t71 @t574) (not (forall (@list @t575) (=> (_ @t71 @t575) (_ (_ tptp.ord_less_eq_nat @t575) @t574))))))))))) % 4.62/4.88 (assume @p245 (forall (@list @t87 @t71) (_ (_ tptp.ord_less_eq_set_nat @t578) @t87))) % 4.62/4.88 (assume @p246 (forall (@list @t120 @t23) (_ (_ tptp.ord_le940807492at_nat @t579) @t120))) % 4.62/4.88 (assume @p247 (forall (@list @t126 @t35) (_ (_ tptp.ord_le633272388at_nat @t580) @t126))) % 4.62/4.88 (assume @p248 (forall (@list @t201 @t47) (_ (_ tptp.ord_le2040082867at_nat @t581) @t201))) % 4.62/4.88 (assume @p249 (forall (@list @t96 @t59) (_ (_ tptp.ord_le1415039317at_nat @t582) @t96))) % 4.62/4.88 (assume @p250 (= tptp.ord_less_eq_set_nat (lambda @t563 (_ (_ tptp.ord_less_eq_nat_o (lambda @t73 @t584)) (lambda @t73 @t583))))) % 4.62/4.88 (assume @p251 (= tptp.ord_le1415039317at_nat (lambda @t567 (_ (_ tptp.ord_le2026740592_nat_o (lambda @t61 @t586)) (lambda @t61 @t585))))) % 4.62/4.88 (assume @p252 (not (= tptp.zero_zero_nat tptp.one_one_nat))) % 4.62/4.88 (assume @p253 (_ @t453 tptp.one_one_nat)) % 4.62/4.88 (assume @p254 (forall @t304 (= (= @t301 @t303) @t396))) % 4.62/4.88 (assume @p255 (_ @t309 tptp.zero_zero_nat)) % 4.62/4.88 (assume @p256 (forall @t308 (or @t546 (not @t333) (not @t411)))) % 4.62/4.88 (assume @p257 (forall (@list @t587 @t289) (= (_ (_ tptp.ord_less_eq_nat_o (lambda @t73 (_ @t88 @t587))) (lambda @t73 (_ @t88 @t289))) (_ (_ tptp.ord_less_eq_set_nat @t587) @t289)))) % 4.62/4.88 (assume @p258 (forall (@list @t588 @t297) (= (_ (_ tptp.ord_le2026740592_nat_o (lambda @t61 (_ @t97 @t588))) (lambda @t61 (_ @t97 @t297))) (_ (_ tptp.ord_le1415039317at_nat @t588) @t297)))) % 4.62/4.88 (assume @p259 (forall (@list @t87 @t71 @t69) (= (_ @t272 @t74) (and (_ @t272 @t77) (_ @t272 @t75))))) % 4.62/4.88 (assume @p260 (forall (@list @t120 @t23 @t21) (= (_ @t274 @t26) (and (_ @t274 @t29) (_ @t274 @t27))))) % 4.62/4.88 (assume @p261 (forall (@list @t126 @t35 @t33) (= (_ @t276 @t38) (and (_ @t276 @t41) (_ @t276 @t39))))) % 4.62/4.88 (assume @p262 (forall (@list @t201 @t47 @t45) (= (_ @t279 @t50) (and (_ @t279 @t53) (_ @t279 @t51))))) % 4.62/4.88 (assume @p263 (forall (@list @t96 @t59 @t57) (= (_ @t282 @t62) (and (_ @t282 @t65) (_ @t282 @t63))))) % 4.62/4.88 (assume @p264 (forall (@list @t91 @t87 @t71) (=> @t591 (= (_ @t590 @t578) (forall @t73 (=> @t589 @t72)))))) % 4.62/4.88 (assume @p265 (forall (@list @t111 @t120 @t23) (=> @t594 (= (_ @t593 @t579) (forall @t25 (=> @t592 @t24)))))) % 4.62/4.88 (assume @p266 (forall (@list @t116 @t126 @t35) (=> @t597 (= (_ @t596 @t580) (forall @t37 (=> @t595 @t36)))))) % 4.62/4.88 (assume @p267 (forall (@list @t278 @t201 @t47) (=> @t600 (= (_ @t599 @t581) (forall @t49 (=> @t598 @t48)))))) % 4.62/4.88 (assume @p268 (forall (@list @t104 @t96 @t59) (=> @t458 (= (_ @t457 @t582) (forall @t61 (=> @t601 @t60)))))) % 4.62/4.88 (assume @p269 (forall (@list @t91 @t87 @t69 @t71) (=> @t591 (=> (forall @t146 (=> @t145 (=> @t353 @t354))) (_ (_ tptp.ord_less_eq_set_nat (_ tptp.collect_nat (lambda @t73 (and @t589 @t70)))) @t578))))) % 4.62/4.88 (assume @p270 (forall (@list @t111 @t120 @t21 @t23) (=> @t594 (=> (forall @t173 (=> @t172 (=> @t355 @t356))) (_ (_ tptp.ord_le940807492at_nat (_ tptp.collect_nat_nat_nat2 (lambda @t25 (and @t592 @t22)))) @t579))))) % 4.62/4.88 (assume @p271 (forall (@list @t116 @t126 @t33 @t35) (=> @t597 (=> (forall @t182 (=> @t181 (=> @t357 @t358))) (_ (_ tptp.ord_le633272388at_nat (_ tptp.collect_nat_nat_nat (lambda @t37 (and @t595 @t34)))) @t580))))) % 4.62/4.88 (assume @p272 (forall (@list @t278 @t201 @t45 @t47) (=> @t600 (=> (forall @t246 (=> (_ @t244 @t278) (=> @t359 @t360))) (_ (_ tptp.ord_le2040082867at_nat (_ tptp.collec1610646258at_nat (lambda @t49 (and @t598 @t46)))) @t581))))) % 4.62/4.88 (assume @p273 (forall (@list @t104 @t96 @t57 @t59) (=> @t458 (=> (forall @t160 (=> @t163 (=> @t351 @t352))) (_ (_ tptp.ord_le1415039317at_nat (_ tptp.collect_nat_nat (lambda @t61 (and @t601 @t58)))) @t582))))) % 4.62/4.88 (assume @p274 (forall (@list @t602 @t71) (_ (_ tptp.ord_less_eq_set_nat @t603) @t602))) % 4.62/4.88 (assume @p275 (forall (@list @t604 @t23) (_ (_ tptp.ord_le940807492at_nat @t605) @t604))) % 4.62/4.88 (assume @p276 (forall (@list @t606 @t35) (_ (_ tptp.ord_le633272388at_nat @t607) @t606))) % 4.62/4.88 (assume @p277 (forall (@list @t608 @t47) (_ (_ tptp.ord_le2040082867at_nat @t609) @t608))) % 4.62/4.88 (assume @p278 (forall (@list @t610 @t59) (_ (_ tptp.ord_le1415039317at_nat @t611) @t610))) % 4.62/4.88 (assume @p279 (forall (@list @t342 @t612 @t602 @t71) (=> (_ @t555 @t612) (=> (_ (_ tptp.ord_less_eq_set_nat @t612) @t603) @t577)))) % 4.62/4.88 (assume @p280 (forall (@list @t613 @t614 @t604 @t23) (=> (_ (_ tptp.member_nat_nat_nat2 @t613) @t614) (=> (_ (_ tptp.ord_le940807492at_nat @t614) @t605) (_ @t23 @t613))))) % 4.62/4.88 (assume @p281 (forall (@list @t418 @t615 @t606 @t35) (=> (_ (_ tptp.member_nat_nat_nat @t418) @t615) (=> (_ (_ tptp.ord_le633272388at_nat @t615) @t607) (_ @t35 @t418))))) % 4.62/4.88 (assume @p282 (forall (@list @t616 @t617 @t608 @t47) (=> (_ (_ tptp.member1128122036at_nat @t616) @t617) (=> (_ (_ tptp.ord_le2040082867at_nat @t617) @t609) (_ @t47 @t616))))) % 4.62/4.88 (assume @p283 (forall (@list @t425 @t618 @t610 @t59) (=> (_ @t556 @t618) (=> (_ (_ tptp.ord_le1415039317at_nat @t618) @t611) (_ @t59 @t425))))) % 4.62/4.88 (assume @p284 (forall (@list @t80 @t82) (=> @t84 (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t7 (_ @t619 (_ @t80 @t1)))))))) % 4.62/4.88 (assume @p285 (forall @t320 (= (not @t620) @t316))) % 4.62/4.88 (assume @p286 (forall @t337 (= (_ @t623 @t334) @t622))) % 4.62/4.88 (assume @p287 (forall @t340 (= (_ (_ tptp.ord_less_nat @t326) @t338) @t622))) % 4.62/4.88 (assume @p288 (forall @t322 (= (not @t396) @t624))) % 4.62/4.88 (assume @p289 (forall @t320 (not (_ @t625 tptp.zero_zero_nat)))) % 4.62/4.88 (assume @p290 (forall @t320 (= (not @t316) @t620))) % 4.62/4.88 (assume @p291 (forall @t315 (= (_ (_ tptp.ord_less_nat @t314) @t313) @t626))) % 4.62/4.88 (assume @p292 (forall @t215 (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t214 (_ (_ tptp.ord_less_nat @t213) @t212)))))) % 4.62/4.88 (assume @p293 (forall @t304 (= (_ (_ tptp.ord_less_nat @t303) @t301) @t627))) % 4.62/4.88 (assume @p294 (forall @t308 (= (_ @t628 @t301) @t627))) % 4.62/4.88 (assume @p295 (forall @t308 (= (_ @t621 @t306) @t629))) % 4.62/4.88 (assume @p296 (forall @t308 (= (_ @t621 @t303) @t629))) % 4.62/4.88 (assume @p297 (forall @t319 (= (_ @t619 @t318) (or (_ @t619 @t209) @t620)))) % 4.62/4.88 (assume @p298 (forall @t320 (= (_ @t625 tptp.one_one_nat) @t316))) % 4.62/4.88 (assume @p299 (forall @t391 (=> @t622 (=> @t390 @t630)))) % 4.62/4.88 (assume @p300 (forall @t391 (=> @t333 (=> (_ @t631 @t85) @t630)))) % 4.62/4.88 (assume @p301 (forall @t376 (=> (and (_ (_ tptp.ord_less_nat @t83) @t370) @t395) @t632))) % 4.62/4.88 (assume @p302 (forall @t376 (=> (and @t382 (_ (_ tptp.ord_less_nat @t212) @t369)) @t632))) % 4.62/4.88 (assume @p303 (forall @t331 (=> @t624 (=> (_ @t633 @t323) (_ @t633 @t329))))) % 4.62/4.88 (assume @p304 (forall @t308 (=> @t622 (not (forall @t387 (=> @t386 (= @t385 tptp.zero_zero_nat))))))) % 4.62/4.88 (assume @p305 (forall @t308 (=> @t624 (=> @t629 (_ @t619 @t306))))) % 4.62/4.88 (assume @p306 (forall @t308 (=> @t627 (=> (_ @t633 tptp.zero_zero_nat) (_ @t628 tptp.zero_zero_nat))))) % 4.62/4.88 (assume @p307 (forall @t308 (=> (not @t546) (=> @t333 @t622)))) % 4.62/4.88 (assume @p308 (forall @t549 (=> (not @t547) (=> @t503 @t635)))) % 4.62/4.88 (assume @p309 (forall @t304 (=> @t636 @t411))) % 4.62/4.88 (assume @p310 (forall @t554 (=> @t637 @t548))) % 4.62/4.88 (assume @p311 (= tptp.ord_less_eq_nat (lambda @t639 (or (_ (_ tptp.ord_less_nat @t364) @t140) @t638)))) % 4.62/4.88 (assume @p312 (= tptp.ord_le1415039317at_nat (lambda @t641 (or (_ (_ tptp.ord_less_set_nat_nat @t542) @t541) @t640)))) % 4.62/4.88 (assume @p313 (forall @t308 (=> @t622 @t333))) % 4.62/4.88 (assume @p314 (forall @t549 (=> @t635 @t503))) % 4.62/4.88 (assume @p315 (forall @t328 (=> @t636 (=> @t414 @t642)))) % 4.62/4.88 (assume @p316 (forall @t553 (=> @t637 (=> @t552 @t644)))) % 4.62/4.88 (assume @p317 (forall @t328 (=> @t411 (=> (_ @t631 @t301) @t642)))) % 4.62/4.88 (assume @p318 (forall @t553 (=> @t548 (=> (_ @t643 @t482) @t644)))) % 4.62/4.88 (assume @p319 (= tptp.ord_less_nat (lambda @t365 (and @t540 @t645)))) % 4.62/4.88 (assume @p320 (= tptp.ord_less_set_nat_nat (lambda @t545 (and @t544 @t646)))) % 4.62/4.88 (assume @p321 (= tptp.ord_less_eq_nat (lambda @t365 (or (_ (_ tptp.ord_less_nat @t140) @t364) @t638)))) % 4.62/4.88 (assume @p322 (= tptp.ord_le1415039317at_nat (lambda @t545 (or (_ (_ tptp.ord_less_set_nat_nat @t541) @t542) @t640)))) % 4.62/4.88 (assume @p323 (forall @t531 (=> @t635 (=> @t484 (_ @t634 @t476))))) % 4.62/4.88 (assume @p324 (= tptp.ord_less_nat (lambda @t400 (and (_ (_ tptp.ord_less_eq_nat @t398) @t213) (not @t647))))) % 4.62/4.88 (assume @p325 (forall @t319 (=> @t626 @t311))) % 4.62/4.88 (assume @p326 (= tptp.ord_less_eq_nat (lambda @t400 (or (_ (_ tptp.ord_less_nat @t398) @t213) @t647)))) % 4.62/4.88 (assume @p327 (forall @t319 (=> (or @t626 @t380) @t311))) % 4.62/4.88 (assume @p328 (forall @t319 (=> @t311 (=> (not @t380) @t626)))) % 4.62/4.88 (assume @p329 (forall (@list @t455 @t83 @t370) (=> (forall (@list @t649 @t648) (=> (_ (_ tptp.ord_less_nat @t649) @t648) (_ (_ tptp.ord_less_nat (_ @t455 @t649)) (_ @t455 @t648)))) (=> @t382 (_ (_ tptp.ord_less_eq_nat (_ @t455 @t83)) (_ @t455 @t370)))))) % 4.62/4.88 (assume @p330 (forall (@list @t650 @t82) (=> (forall @t146 (=> (_ @t144 @t650) (_ (_ tptp.ord_less_nat @t139) @t82))) (_ tptp.finite_finite_nat @t650)))) % 4.62/4.88 (assume @p331 (= tptp.finite_finite_nat (lambda @t654 (exists @t653 (forall @t73 (=> @t652 (_ (_ tptp.ord_less_nat @t68) @t398))))))) % 4.62/4.88 (assume @p332 (forall (@list @t71 @t83) (_ tptp.finite_finite_nat (_ tptp.collect_nat (lambda @t399 (and (_ @t71 @t397) (_ (_ tptp.ord_less_nat @t397) @t83))))))) % 4.62/4.88 (assume @p333 @t655) % 4.62/4.88 (assume @p334 true) % 4.62/4.88 (step @p335 (= tptp.ord_less_eq_nat @t661) :rule refl :args (@t661)) % 4.62/4.88 (step @p336 (= tptp.finite_finite_nat @t662) :rule refl :args (@t662)) % 4.62/4.88 (step @p337 (= tptp.ord_less_eq_set_nat @t663) :rule refl :args (@t663)) % 4.62/4.88 (step @p338 (= tptp.ord_le1415039317at_nat @t665) :rule refl :args (@t665)) % 4.62/4.88 (step @p339 (= tptp.finite_Fpow_nat @t667) :rule refl :args (@t667)) % 4.62/4.88 (step @p340 (= tptp.finite90785608at_nat @t670) :rule refl :args (@t670)) % 4.62/4.88 (step @p341 (= tptp.finite1633036872at_nat @t673) :rule refl :args (@t673)) % 4.62/4.88 (step @p342 (= tptp.finite252967095at_nat @t676) :rule refl :args (@t676)) % 4.62/4.88 (step @p343 (= tptp.finite_Fpow_nat_nat @t678) :rule refl :args (@t678)) % 4.62/4.88 (step @p344 (= tptp.ord_less_nat @t679) :rule refl :args (@t679)) % 4.62/4.88 (step @p345 (= tptp.ord_less_set_nat_nat @t680) :rule refl :args (@t680)) % 4.62/4.88 (step @p346 :rule eq-symm :args (@t684 @t681)) % 4.62/4.88 (step @p347 :rule beta-reduce :args ((= @t685 @t681))) % 4.62/4.88 (step @p348 :rule refl :args (@t684)) % 4.62/4.88 (step @p349 :rule cong :premises (@p348 @p347) :args (@t686)) % 4.62/4.88 (step @p350 :rule trans :premises (@p349 @p346)) % 4.62/4.88 (step @p351 :rule cong :premises (@p350) :args (@t687)) % 4.62/4.88 (step @p352 :rule quant-unused-vars :args ((= (forall @t17 true) true))) % 4.62/4.88 (step @p353 :rule eq-refl :args (@t685)) % 4.62/4.88 (step @p354 :rule cong :premises (@p353) :args ((forall @t17 (= @t685 @t685)))) % 4.62/4.88 (step @p355 :rule trans :premises (@p354 @p352)) % 4.62/4.88 (step @p356 :rule refl :args (@t685)) % 4.62/4.88 (step @p357 :rule refl :args (@t15)) % 4.62/4.88 (step @p358 :rule skolem_intro :args (@t683)) % 4.62/4.88 (step @p359 :rule ho_cong :premises (@p358 @p357)) % 4.62/4.88 (step @p360 :rule cong :premises (@p359 @p356) :args (@t686)) % 4.62/4.88 (step @p361 :rule cong :premises (@p360) :args (@t687)) % 4.62/4.88 (step @p362 :rule trans :premises (@p361 @p355)) % 4.62/4.88 (step @p363 :rule true_elim :premises (@p362)) % 4.62/4.88 (step @p364 :rule eq_resolve :premises (@p363 @p351)) % 4.62/4.88 (step @p365 :rule eq-symm :args (@t689 @t690)) % 4.62/4.88 (step @p366 :rule refl :args (@t691)) % 4.62/4.88 (step @p367 :rule cong :premises (@p366 @p365) :args ((=> @t691 @t692))) % 4.62/4.88 (assume-push @p779 @t691) % 4.62/4.88 (step @p369 :rule instantiate :premises (@p364) :args (@t693)) % 4.62/4.88 (step-pop @p780 :rule scope :premises (@p369)) % 4.62/4.88 (step @p370 :rule process_scope :premises (@p780) :args (@t692)) % 4.62/4.88 (step @p372 :rule eq_resolve :premises (@p370 @p367)) % 4.62/4.88 (step @p373 :rule implies_elim :premises (@p372)) % 4.62/4.88 (step @p374 :rule chain_m_resolution :premises (@p373 @p364) :args (@t694 @t695 (@list @t691))) % 4.62/4.88 (step @p375 :rule refl :args ((tptp.collect_nat_nat @t699))) % 4.62/4.88 (step @p376 :rule refl :args ((_ @t2 @t697))) % 4.62/4.88 (step @p377 :rule refl :args ((tptp.plus_plus_nat @t5 @t696))) % 4.62/4.88 (step @p378 :rule refl :args (@t696)) % 4.62/4.88 (step @p379 :rule refl :args (@t700)) % 4.62/4.88 (step @p380 :rule cong :premises (@p379 @p378) :args (@t701)) % 4.62/4.88 (step @p381 :rule trans :premises (@p380 @p377)) % 4.62/4.88 (step @p382 :rule cong :premises (@p381) :args (@t702)) % 4.62/4.88 (step @p383 :rule trans :premises (@p382 @p376)) % 4.62/4.88 (step @p384 :rule refl :args (tptp.zero_zero_nat)) % 4.62/4.88 (step @p385 :rule cong :premises (@p384 @p383) :args (@t703)) % 4.62/4.88 (step @p386 :rule cong :premises (@p385) :args (@t704)) % 4.62/4.88 (step @p387 :rule refl :args (@t705)) % 4.62/4.88 (step @p388 :rule refl :args (@t656)) % 4.62/4.88 (step @p389 :rule refl :args (@t706)) % 4.62/4.88 (step @p390 :rule cong :premises (@p389 @p388) :args (@t707)) % 4.62/4.88 (step @p391 :rule trans :premises (@p390 @p387)) % 4.62/4.88 (step @p392 :rule refl :args (tptp.n)) % 4.62/4.88 (step @p393 :rule cong :premises (@p392 @p391) :args (@t708)) % 4.62/4.88 (step @p394 :rule cong :premises (@p393) :args (@t709)) % 4.62/4.88 (step @p395 :rule cong :premises (@p394) :args (@t710)) % 4.62/4.88 (step @p396 :rule cong :premises (@p395) :args (@t711)) % 4.62/4.88 (step @p397 :rule cong :premises (@p396) :args (@t712)) % 4.62/4.88 (step @p398 :rule nary_cong :premises (@p397 @p386) :args (@t713)) % 4.62/4.88 (step @p399 :rule cong :premises (@p398) :args (@t714)) % 4.62/4.88 (step @p400 :rule cong :premises (@p399) :args (@t715)) % 4.62/4.88 (step @p401 :rule trans :premises (@p400 @p375)) % 4.62/4.88 (step @p402 :rule refl :args (tptp.collect_nat_nat)) % 4.62/4.88 (step @p403 :rule ho_cong :premises (@p402 @p399)) % 4.62/4.88 (step @p404 :rule cong :premises (@p403 @p401) :args ((= @t716 @t715))) % 4.62/4.88 (step @p405 :rule symm :premises (@p404)) % 4.62/4.88 (step @p406 :rule refl :args ((_ tptp.collect_nat_nat @t699))) % 4.62/4.88 (step @p407 :rule eq_resolve :premises (@p406 @p405)) % 4.62/4.88 (step @p408 :rule refl :args (@t56)) % 4.62/4.88 (step @p409 :rule cong :premises (@p408 @p407) :args (@t717)) % 4.62/4.88 (step @p410 :rule refl :args (@t719)) % 4.62/4.88 (step @p411 :rule nary_cong :premises (@p410 @p409) :args (@t720)) % 4.62/4.88 (step @p412 :rule cong :premises (@p411) :args (@t721)) % 4.62/4.88 (step @p413 :rule beta-reduce :args ((= (_ (lambda @t207 (forall @t61 (or @t719 @t722))) @t716) @t721))) % 4.62/4.88 (step @p414 :rule trans :premises (@p413 @p412)) % 4.62/4.88 (step @p415 :rule aci_norm :args ((= (or false @t703) @t703))) % 4.62/4.88 (step @p416 :rule refl :args (@t703)) % 4.62/4.88 (step @p417 :rule evaluate :args ((not true))) % 4.62/4.88 (step @p418 :rule eq-refl :args (@t701)) % 4.62/4.88 (step @p419 :rule cong :premises (@p418) :args (@t723)) % 4.62/4.88 (step @p420 :rule trans :premises (@p419 @p417)) % 4.62/4.88 (step @p421 :rule nary_cong :premises (@p420 @p416) :args (@t724)) % 4.62/4.88 (step @p422 :rule trans :premises (@p421 @p415)) % 4.62/4.88 (step @p423 :rule cong :premises (@p422) :args ((forall @t698 @t724))) % 4.62/4.88 (step @p424 :rule quant-var-elim-eq :args ((= (forall @t7 @t727) @t724))) % 4.62/4.88 (step @p425 :rule aci_norm :args ((= @t728 @t727))) % 4.62/4.88 (step @p426 :rule cong :premises (@p425) :args (@t729)) % 4.62/4.88 (step @p427 :rule trans :premises (@p426 @p424)) % 4.62/4.88 (step @p428 :rule cong :premises (@p427) :args (@t730)) % 4.62/4.88 (step @p429 :rule quant-merge-prenex :args ((= @t730 @t731))) % 4.62/4.88 (step @p430 :rule symm :premises (@p429)) % 4.62/4.88 (step @p431 :rule quant_var_reordering :args ((= @t732 @t731))) % 4.62/4.88 (step @p432 :rule trans :premises (@p431 @p430 @p428)) % 4.62/4.88 (step @p433 :rule trans :premises (@p432 @p423)) % 4.62/4.88 (step @p434 :rule quant-merge-prenex :args ((= (forall @t7 @t733) @t732))) % 4.62/4.88 (step @p435 :rule refl :args (@t725)) % 4.62/4.88 (step @p436 :rule alpha_equiv :args (@t734 (@list @t696) (@list @t656))) % 4.62/4.88 (step @p437 :rule nary_cong :premises (@p436 @p435) :args (@t735)) % 4.62/4.88 (step @p438 :rule quant-miniscope-or :args ((= @t733 @t735))) % 4.62/4.88 (step @p439 :rule trans :premises (@p438 @p437)) % 4.62/4.88 (step @p440 :rule symm :premises (@p439)) % 4.62/4.88 (step @p441 :rule cong :premises (@p440) :args ((forall @t7 (or @t737 @t725)))) % 4.62/4.88 (step @p442 :rule trans :premises (@p441 @p434)) % 4.62/4.88 (step @p443 :rule trans :premises (@p442 @p433)) % 4.62/4.88 (step @p444 :rule refl :args (@t3)) % 4.62/4.88 (step @p445 :rule cong :premises (@p444 @p389) :args ((= @t3 @t706))) % 4.62/4.88 (step @p446 :rule symm :premises (@p445)) % 4.62/4.88 (step @p447 :rule eq_resolve :premises (@p444 @p446)) % 4.62/4.88 (step @p448 :rule cong :premises (@p384 @p447) :args (@t738)) % 4.62/4.88 (step @p449 :rule refl :args (@t737)) % 4.62/4.88 (step @p450 :rule nary_cong :premises (@p449 @p448) :args (@t739)) % 4.62/4.88 (step @p451 :rule cong :premises (@p450) :args ((forall @t7 @t739))) % 4.62/4.88 (step @p452 :rule trans :premises (@p451 @p443)) % 4.62/4.88 (step @p453 :rule refl :args (@t738)) % 4.62/4.88 (step @p454 :rule bool-double-not-elim :args (@t737)) % 4.62/4.88 (step @p455 :rule nary_cong :premises (@p454 @p453) :args ((or (not @t740) @t738))) % 4.62/4.88 (step @p456 :rule bool-impl-elim :args (@t740 @t738)) % 4.62/4.88 (step @p457 :rule trans :premises (@p456 @p455)) % 4.62/4.88 (step @p458 :rule cong :premises (@p457) :args ((forall @t7 (=> @t740 @t738)))) % 4.62/4.88 (step @p459 :rule trans :premises (@p458 @p452)) % 4.62/4.88 (step @p460 :rule eq-symm :args (@t3 tptp.zero_zero_nat)) % 4.62/4.88 (step @p461 :rule beta-reduce :args ((= (_ (lambda @t741 (not (forall @t659 (not (= @t364 @t736))))) @t1) @t740))) % 4.62/4.88 (step @p462 :rule refl :args (@t1)) % 4.62/4.88 (step @p463 :rule refl :args (@t5)) % 4.62/4.88 (step @p464 :rule cong :premises (@p463 @p379) :args ((= @t5 @t700))) % 4.62/4.88 (step @p465 :rule symm :premises (@p464)) % 4.62/4.88 (step @p466 :rule eq_resolve :premises (@p463 @p465)) % 4.62/4.88 (step @p467 :rule cong :premises (@p466 @p388) :args (@t742)) % 4.62/4.88 (step @p468 :rule refl :args (@t364)) % 4.62/4.88 (step @p469 :rule cong :premises (@p468 @p467) :args (@t743)) % 4.62/4.88 (step @p470 :rule cong :premises (@p469) :args (@t744)) % 4.62/4.88 (step @p471 :rule cong :premises (@p470) :args (@t745)) % 4.62/4.88 (step @p472 :rule cong :premises (@p471) :args (@t746)) % 4.62/4.88 (step @p473 :rule cong :premises (@p472) :args (@t747)) % 4.62/4.88 (step @p474 :rule beta-reduce :args ((= @t750 @t747))) % 4.62/4.88 (step @p475 :rule trans :premises (@p474 @p473)) % 4.62/4.88 (step @p476 :rule ho_cong :premises (@p475 @p462)) % 4.62/4.88 (step @p477 :rule trans :premises (@p476 @p461)) % 4.62/4.88 (step @p478 :rule cong :premises (@p477 @p460) :args (@t751)) % 4.62/4.88 (step @p479 :rule cong :premises (@p478) :args (@t752)) % 4.62/4.88 (step @p480 :rule trans :premises (@p479 @p459)) % 4.62/4.88 (step @p481 :rule beta-reduce :args ((= (_ (lambda @t741 (not (forall @t659 (not (= @t364 @t707))))) tptp.n) @t711))) % 4.62/4.88 (step @p482 :rule refl :args (tptp.n)) % 4.62/4.88 (step @p483 :rule cong :premises (@p447 @p388) :args (@t705)) % 4.62/4.88 (step @p484 :rule cong :premises (@p468 @p483) :args (@t753)) % 4.62/4.88 (step @p485 :rule cong :premises (@p484) :args (@t754)) % 4.62/4.88 (step @p486 :rule cong :premises (@p485) :args (@t755)) % 4.62/4.88 (step @p487 :rule cong :premises (@p486) :args (@t756)) % 4.62/4.88 (step @p488 :rule cong :premises (@p487) :args (@t757)) % 4.62/4.88 (step @p489 :rule beta-reduce :args ((= @t758 @t757))) % 4.62/4.88 (step @p490 :rule trans :premises (@p489 @p488)) % 4.62/4.88 (step @p491 :rule ho_cong :premises (@p490 @p482)) % 4.62/4.88 (step @p492 :rule trans :premises (@p491 @p481)) % 4.62/4.88 (step @p493 :rule cong :premises (@p492) :args (@t759)) % 4.62/4.88 (step @p494 :rule nary_cong :premises (@p493 @p480) :args (@t760)) % 4.62/4.88 (step @p495 :rule cong :premises (@p494) :args ((lambda @t12 @t760))) % 4.62/4.88 (step @p496 :rule refl :args (tptp.collect_nat_nat)) % 4.62/4.88 (step @p497 :rule ho_cong :premises (@p496 @p495)) % 4.62/4.88 (step @p498 :rule refl :args (@t722)) % 4.62/4.88 (step @p499 :rule refl :args ((tptp.collect_nat_nat @t18))) % 4.62/4.88 (step @p500 :rule refl :args (@t681)) % 4.62/4.88 (step @p501 :rule cong :premises (@p500) :args (@t682)) % 4.62/4.88 (step @p502 :rule cong :premises (@p501) :args (@t718)) % 4.62/4.88 (step @p503 :rule trans :premises (@p502 @p499)) % 4.62/4.88 (step @p504 :rule ho_cong :premises (@p402 @p501)) % 4.62/4.88 (step @p505 :rule cong :premises (@p504 @p503) :args ((= (_ tptp.collect_nat_nat @t682) @t718))) % 4.62/4.88 (step @p506 :rule symm :premises (@p505)) % 4.62/4.88 (step @p507 :rule refl :args (@t19)) % 4.62/4.88 (step @p508 :rule eq_resolve :premises (@p507 @p506)) % 4.62/4.88 (step @p509 :rule refl :args (@t16)) % 4.62/4.88 (step @p510 :rule cong :premises (@p509 @p500) :args ((= @t16 @t681))) % 4.62/4.88 (step @p511 :rule symm :premises (@p510)) % 4.62/4.88 (step @p512 :rule eq_resolve :premises (@p509 @p511)) % 4.62/4.88 (step @p513 :rule cong :premises (@p512) :args (@t18)) % 4.62/4.88 (step @p514 :rule ho_cong :premises (@p402 @p513)) % 4.62/4.88 (step @p515 :rule trans :premises (@p514 @p508)) % 4.62/4.88 (step @p516 :rule cong :premises (@p408 @p515) :args (@t761)) % 4.62/4.88 (step @p517 :rule cong :premises (@p516) :args (@t762)) % 4.62/4.88 (step @p518 :rule nary_cong :premises (@p517 @p498) :args (@t763)) % 4.62/4.88 (step @p519 :rule cong :premises (@p518) :args (@t764)) % 4.62/4.88 (step @p520 :rule cong :premises (@p519) :args (@t765)) % 4.62/4.88 (step @p521 :rule beta-reduce :args ((= (_ @t767 @t19) @t765))) % 4.62/4.88 (step @p522 :rule trans :premises (@p521 @p520)) % 4.62/4.88 (step @p523 :rule ho_cong :premises (@p522 @p497)) % 4.62/4.88 (step @p524 :rule trans :premises (@p523 @p414)) % 4.62/4.88 (step @p525 :rule refl :args (@t4)) % 4.62/4.88 (step @p526 :rule refl :args (@t5)) % 4.62/4.88 (step @p527 :rule refl :args (@t748)) % 4.62/4.88 (step @p528 :rule refl :args (@t657)) % 4.62/4.88 (step @p529 :rule cong :premises (@p528 @p527) :args ((= @t657 @t748))) % 4.62/4.88 (step @p530 :rule symm :premises (@p529)) % 4.62/4.88 (step @p531 :rule eq_resolve :premises (@p528 @p530)) % 4.62/4.88 (step @p532 :rule cong :premises (@p468 @p531) :args (@t658)) % 4.62/4.88 (step @p533 :rule cong :premises (@p532) :args (@t768)) % 4.62/4.88 (step @p534 :rule cong :premises (@p533) :args (@t769)) % 4.62/4.88 (step @p535 :rule cong :premises (@p534) :args (@t770)) % 4.62/4.88 (step @p536 :rule exists-elim :args ((= @t660 @t770))) % 4.62/4.88 (step @p537 :rule trans :premises (@p536 @p535)) % 4.62/4.88 (step @p538 :rule cong :premises (@p537) :args (@t661)) % 4.62/4.88 (step @p539 :rule trans :premises (@p335 @p538)) % 4.62/4.88 (step @p540 :rule ho_cong :premises (@p539 @p526)) % 4.62/4.88 (step @p541 :rule ho_cong :premises (@p540 @p462)) % 4.62/4.88 (step @p542 :rule cong :premises (@p541 @p525) :args (@t6)) % 4.62/4.88 (step @p543 :rule cong :premises (@p542) :args (@t8)) % 4.62/4.88 (step @p544 :rule refl :args (@t3)) % 4.62/4.88 (step @p545 :rule ho_cong :premises (@p539 @p544)) % 4.62/4.88 (step @p546 :rule ho_cong :premises (@p545 @p482)) % 4.62/4.88 (step @p547 :rule cong :premises (@p546) :args (@t10)) % 4.62/4.88 (step @p548 :rule nary_cong :premises (@p547 @p543) :args (@t11)) % 4.62/4.88 (step @p549 :rule cong :premises (@p548) :args (@t13)) % 4.62/4.88 (step @p550 :rule ho_cong :premises (@p496 @p549)) % 4.62/4.88 (step @p551 :rule refl :args (@t19)) % 4.62/4.88 (step @p552 :rule refl :args (@t722)) % 4.62/4.88 (step @p553 :rule refl :args (@t585)) % 4.62/4.88 (step @p554 :rule cong :premises (@p553 @p552) :args ((= @t585 @t722))) % 4.62/4.88 (step @p555 :rule symm :premises (@p554)) % 4.62/4.88 (step @p556 :rule eq_resolve :premises (@p553 @p555)) % 4.62/4.88 (step @p557 :rule refl :args (@t766)) % 4.62/4.88 (step @p558 :rule refl :args (@t586)) % 4.62/4.88 (step @p559 :rule cong :premises (@p558 @p557) :args ((= @t586 @t766))) % 4.62/4.88 (step @p560 :rule symm :premises (@p559)) % 4.62/4.88 (step @p561 :rule eq_resolve :premises (@p558 @p560)) % 4.62/4.88 (step @p562 :rule cong :premises (@p561) :args (@t771)) % 4.62/4.88 (step @p563 :rule nary_cong :premises (@p562 @p556) :args (@t772)) % 4.62/4.88 (step @p564 :rule cong :premises (@p563) :args ((forall @t61 @t772))) % 4.62/4.88 (step @p565 :rule bool-impl-elim :args (@t586 @t585)) % 4.62/4.88 (step @p566 :rule cong :premises (@p565) :args (@t664)) % 4.62/4.88 (step @p567 :rule trans :premises (@p566 @p564)) % 4.62/4.88 (step @p568 :rule cong :premises (@p567) :args (@t665)) % 4.62/4.88 (step @p569 :rule trans :premises (@p338 @p568)) % 4.62/4.88 (step @p570 :rule ho_cong :premises (@p569 @p551)) % 4.62/4.88 (step @p571 :rule ho_cong :premises (@p570 @p550)) % 4.62/4.88 (step @p572 :rule trans :premises (@p571 @p524)) % 4.62/4.88 (step @p573 :rule eq_resolve :premises (@p2 @p572)) % 4.62/4.88 (step @p574 :rule eq-refl :args (@t714)) % 4.62/4.88 (step @p575 :rule skolem_intro :args (@t773)) % 4.62/4.88 (step @p576 :rule refl :args (@t714)) % 4.62/4.88 (step @p577 :rule cong :premises (@p576 @p575) :args ((= @t714 @t773))) % 4.62/4.88 (step @p578 :rule trans :premises (@p577 @p574)) % 4.62/4.88 (step @p579 :rule true_elim :premises (@p578)) % 4.62/4.88 (step @p580 :rule cong :premises (@p579) :args (@t715)) % 4.62/4.88 (step @p581 :rule refl :args (@t778)) % 4.62/4.88 (step @p582 :rule cong :premises (@p581 @p580) :args (@t779)) % 4.62/4.88 (step @p583 :rule eq-refl :args (@t682)) % 4.62/4.88 (step @p584 :rule refl :args (@t682)) % 4.62/4.88 (step @p585 :rule cong :premises (@p584 @p358) :args ((= @t682 @t683))) % 4.62/4.88 (step @p586 :rule trans :premises (@p585 @p583)) % 4.62/4.88 (step @p587 :rule true_elim :premises (@p586)) % 4.62/4.88 (step @p588 :rule cong :premises (@p587) :args (@t718)) % 4.62/4.88 (step @p589 :rule cong :premises (@p581 @p588) :args (@t780)) % 4.62/4.88 (step @p590 :rule cong :premises (@p589) :args (@t781)) % 4.62/4.88 (step @p591 :rule nary_cong :premises (@p590 @p582) :args (@t782)) % 4.62/4.88 (step @p592 :rule refl :args (@t783)) % 4.62/4.88 (step @p593 :rule cong :premises (@p592 @p591) :args ((=> @t783 @t782))) % 4.62/4.88 (assume-push @p781 @t783) % 4.62/4.88 (step @p595 :rule instantiate :premises (@p573) :args ((@list @t778))) % 4.62/4.88 (step-pop @p782 :rule scope :premises (@p595)) % 4.62/4.88 (step @p596 :rule process_scope :premises (@p782) :args (@t782)) % 4.62/4.88 (step @p598 :rule eq_resolve :premises (@p596 @p593)) % 4.62/4.88 (step @p599 :rule implies_elim :premises (@p598)) % 4.62/4.88 (step @p600 :rule chain_m_resolution :premises (@p599 @p573) :args (@t788 @t695 (@list @t783))) % 4.62/4.88 (step @p601 :rule refl :args (@t789)) % 4.62/4.88 (step @p602 :rule refl :args (@t100)) % 4.62/4.88 (step @p603 :rule cong :premises (@p602 @p601) :args ((= @t100 @t789))) % 4.62/4.88 (step @p604 :rule symm :premises (@p603)) % 4.62/4.88 (step @p605 :rule eq_resolve :premises (@p602 @p604)) % 4.62/4.88 (step @p606 :rule refl :args (@t792)) % 4.62/4.88 (step @p607 :rule refl :args (@t793)) % 4.62/4.88 (step @p608 :rule refl :args (@t105)) % 4.62/4.88 (step @p609 :rule cong :premises (@p608 @p607) :args ((= @t105 @t793))) % 4.62/4.88 (step @p610 :rule symm :premises (@p609)) % 4.62/4.88 (step @p611 :rule eq_resolve :premises (@p608 @p610)) % 4.62/4.88 (step @p612 :rule cong :premises (@p611) :args (@t794)) % 4.62/4.88 (step @p613 :rule nary_cong :premises (@p612 @p606 @p605) :args (@t795)) % 4.62/4.88 (step @p614 :rule cong :premises (@p613) :args ((forall @t286 @t795))) % 4.62/4.88 (step @p615 :rule aci_norm :args ((= (or @t794 (or @t792 @t100)) @t795))) % 4.62/4.88 (step @p616 :rule bool-impl-elim :args (@t791 @t100)) % 4.62/4.88 (step @p617 :rule refl :args (@t794)) % 4.62/4.88 (step @p618 :rule nary_cong :premises (@p617 @p616) :args ((or @t794 @t796))) % 4.62/4.88 (step @p619 :rule trans :premises (@p618 @p615)) % 4.62/4.88 (step @p620 :rule bool-impl-elim :args (@t105 @t796)) % 4.62/4.88 (step @p621 :rule trans :premises (@p620 @p619)) % 4.62/4.88 (step @p622 :rule cong :premises (@p621) :args ((forall @t286 (=> @t105 @t796)))) % 4.62/4.88 (step @p623 :rule trans :premises (@p622 @p614)) % 4.62/4.88 (step @p624 :rule refl :args (@t100)) % 4.62/4.88 (step @p625 :rule beta-reduce :args ((= (_ @t797 @t104) @t791))) % 4.62/4.88 (step @p626 :rule refl :args (@t104)) % 4.62/4.88 (step @p627 :rule beta-reduce :args ((= @t798 @t797))) % 4.62/4.88 (step @p628 :rule ho_cong :premises (@p627 @p626)) % 4.62/4.88 (step @p629 :rule trans :premises (@p628 @p625)) % 4.62/4.88 (step @p630 :rule cong :premises (@p629 @p624) :args (@t799)) % 4.62/4.88 (step @p631 :rule refl :args (@t105)) % 4.62/4.88 (step @p632 :rule cong :premises (@p631 @p630) :args (@t800)) % 4.62/4.88 (step @p633 :rule cong :premises (@p632) :args ((forall @t286 @t800))) % 4.62/4.88 (step @p634 :rule trans :premises (@p633 @p623)) % 4.62/4.88 (step @p635 :rule refl :args (@t96)) % 4.62/4.88 (step @p636 :rule ho_cong :premises (@p569 @p635)) % 4.62/4.88 (step @p637 :rule ho_cong :premises (@p636 @p626)) % 4.62/4.88 (step @p638 :rule cong :premises (@p637 @p624) :args (@t284)) % 4.62/4.88 (step @p639 :rule cong :premises (@p631 @p638) :args (@t285)) % 4.62/4.88 (step @p640 :rule cong :premises (@p639) :args (@t287)) % 4.62/4.88 (step @p641 :rule trans :premises (@p640 @p634)) % 4.62/4.88 (step @p642 :rule eq_resolve :premises (@p63 @p641)) % 4.62/4.88 (step @p643 :rule instantiate :premises (@p642) :args ((@list @t774 @t776))) % 4.62/4.88 (step @p644 :rule refl :args ((tptp.finite570312790at_nat @t801))) % 4.62/4.88 (step @p645 :rule refl :args (@t774)) % 4.62/4.88 (step @p646 :rule cong :premises (@p645) :args (@t802)) % 4.62/4.88 (step @p647 :rule trans :premises (@p646 @p644)) % 4.62/4.88 (step @p648 :rule refl :args (tptp.finite570312790at_nat)) % 4.62/4.88 (step @p649 :rule ho_cong :premises (@p648 @p645)) % 4.62/4.88 (step @p650 :rule cong :premises (@p649 @p647) :args ((= (_ tptp.finite570312790at_nat @t774) @t802))) % 4.62/4.88 (step @p651 :rule symm :premises (@p650)) % 4.62/4.88 (step @p652 :rule refl :args ((_ tptp.finite570312790at_nat @t801))) % 4.62/4.88 (step @p653 :rule eq_resolve :premises (@p652 @p651)) % 4.62/4.88 (step @p654 :rule refl :args (@t801)) % 4.62/4.88 (step @p655 :rule cong :premises (@p654 @p645) :args ((= @t801 @t774))) % 4.62/4.88 (step @p656 :rule symm :premises (@p655)) % 4.62/4.88 (step @p657 :rule eq_resolve :premises (@p654 @p656)) % 4.62/4.88 (step @p658 :rule ho_cong :premises (@p496 @p579)) % 4.62/4.88 (step @p659 :rule trans :premises (@p658 @p657)) % 4.62/4.88 (step @p660 :rule refl :args (tptp.finite570312790at_nat)) % 4.62/4.88 (step @p661 :rule ho_cong :premises (@p660 @p659)) % 4.62/4.88 (step @p662 :rule trans :premises (@p661 @p653)) % 4.62/4.88 (step @p663 :rule ho_cong :premises (@p660 @p497)) % 4.62/4.88 (step @p664 :rule ho_cong :premises (@p660 @p550)) % 4.62/4.88 (step @p665 :rule trans :premises (@p664 @p663)) % 4.62/4.88 (step @p666 :rule trans :premises (@p665 @p662)) % 4.62/4.88 (step @p667 :rule eq_resolve :premises (@p1 @p666)) % 4.62/4.88 (step @p668 :rule refl :args ((tptp.finite570312790at_nat @t803))) % 4.62/4.88 (step @p669 :rule refl :args (@t776)) % 4.62/4.88 (step @p670 :rule cong :premises (@p669) :args (@t804)) % 4.62/4.88 (step @p671 :rule trans :premises (@p670 @p668)) % 4.62/4.88 (step @p672 :rule ho_cong :premises (@p648 @p669)) % 4.62/4.88 (step @p673 :rule cong :premises (@p672 @p671) :args ((= (_ tptp.finite570312790at_nat @t776) @t804))) % 4.62/4.88 (step @p674 :rule symm :premises (@p673)) % 4.62/4.88 (step @p675 :rule refl :args ((_ tptp.finite570312790at_nat @t803))) % 4.62/4.88 (step @p676 :rule eq_resolve :premises (@p675 @p674)) % 4.62/4.88 (step @p677 :rule refl :args (@t803)) % 4.62/4.88 (step @p678 :rule cong :premises (@p677 @p669) :args ((= @t803 @t776))) % 4.62/4.88 (step @p679 :rule symm :premises (@p678)) % 4.62/4.88 (step @p680 :rule eq_resolve :premises (@p677 @p679)) % 4.62/4.88 (step @p681 :rule eq-refl :args (@t18)) % 4.62/4.88 (step @p682 :rule skolem_intro :args (@t775)) % 4.62/4.88 (step @p683 :rule refl :args (@t18)) % 4.62/4.88 (step @p684 :rule cong :premises (@p683 @p682) :args ((= @t18 @t775))) % 4.62/4.88 (step @p685 :rule trans :premises (@p684 @p681)) % 4.62/4.88 (step @p686 :rule true_elim :premises (@p685)) % 4.62/4.88 (step @p687 :rule ho_cong :premises (@p496 @p686)) % 4.62/4.88 (step @p688 :rule trans :premises (@p687 @p680)) % 4.62/4.88 (step @p689 :rule ho_cong :premises (@p660 @p688)) % 4.62/4.88 (step @p690 :rule trans :premises (@p689 @p676)) % 4.62/4.88 (step @p691 :rule cong :premises (@p690) :args (@t655)) % 4.62/4.88 (step @p692 :rule eq_resolve :premises (@p333 @p691)) % 4.62/4.88 (step @p693 :rule cnf_or_pos :args (@t807)) % 4.62/4.88 (step @p694 :rule reordering :premises (@p693) :args ((or @t804 @t806 @t805 (not @t807)))) % 4.62/4.88 (step @p695 :rule chain_m_resolution :premises (@p694 @p692 @p667 @p643) :args (@t805 @t808 (@list @t804 @t802 @t807))) % 4.62/4.88 (step @p696 :rule skolemize :premises (@p695)) % 4.62/4.88 (step @p697 :rule cnf_or_neg :args (@t811 1)) % 4.62/4.88 (step @p698 :rule chain_m_resolution :premises (@p697 @p696) :args ((not @t784) @t812 @t813)) % 4.62/4.88 (step @p699 :rule cnf_or_pos :args (@t788)) % 4.62/4.88 (step @p700 :rule reordering :premises (@p699) :args ((or @t784 @t787 (not @t788)))) % 4.62/4.88 (step @p701 :rule chain_m_resolution :premises (@p700 @p698 @p600) :args (@t787 @t814 (@list @t784 @t788))) % 4.62/4.88 (step @p702 :rule bool-double-not-elim :args (@t809)) % 4.62/4.88 (step @p703 :rule refl :args (@t811)) % 4.62/4.88 (step @p704 :rule nary_cong :premises (@p703 @p702) :args ((or @t811 (not @t810)))) % 4.62/4.88 (step @p705 :rule cnf_or_neg :args (@t811 0)) % 4.62/4.88 (step @p706 :rule eq_resolve :premises (@p705 @p704)) % 4.62/4.88 (step @p707 :rule reordering :premises (@p706) :args ((or @t809 @t811))) % 4.62/4.88 (step @p708 :rule chain_m_resolution :premises (@p707 @p696) :args (@t809 @t812 @t813)) % 4.62/4.88 (step @p709 :rule bool-double-not-elim :args (@t786)) % 4.62/4.88 (step @p710 :rule refl :args (@t816)) % 4.62/4.88 (step @p711 :rule refl :args (@t810)) % 4.62/4.88 (step @p712 :rule nary_cong :premises (@p711 @p710 @p709) :args ((or @t810 @t816 (not @t787)))) % 4.62/4.88 (assume-push @p783 @t809) % 4.62/4.88 (assume-push @p784 @t815) % 4.62/4.88 (assume-push @p785 @t787) % 4.62/4.88 (step @p716 :rule evaluate :args ((= false true))) % 4.62/4.88 (step @p717 :rule true_intro :premises (@p708)) % 4.62/4.88 (step @p718 :rule symm :premises (@p784)) % 4.62/4.88 (step @p719 :rule cong :premises (@p718) :args (@t785)) % 4.62/4.88 (step @p720 :rule cong :premises (@p581 @p719) :args (@t786)) % 4.62/4.88 (step @p721 :rule false_intro :premises (@p701)) % 4.62/4.88 (step @p722 :rule symm :premises (@p721)) % 4.62/4.88 (step @p723 :rule trans :premises (@p722 @p720 @p717)) % 4.62/4.88 (step @p724 false :rule eq_resolve :premises (@p723 @p716)) % 4.62/4.88 (step-pop @p786 :rule scope :premises (@p724)) % 4.62/4.88 (step-pop @p787 :rule scope :premises (@p786)) % 4.62/4.88 (step-pop @p788 :rule scope :premises (@p787)) % 4.62/4.88 (step @p725 :rule process_scope :premises (@p788) :args (false)) % 4.62/4.88 (step @p729 :rule not_and :premises (@p725)) % 4.62/4.88 (step @p730 :rule eq_resolve :premises (@p729 @p712)) % 4.62/4.88 (step @p731 :rule chain_m_resolution :premises (@p730 @p708 @p701) :args (@t816 (@list false true) (@list @t809 @t786))) % 4.62/4.88 ; WARNING: add trust step for TRUST % 4.62/4.88 ; trust TRUST THEORY_LEMMA % 4.62/4.88 (step @p732 :rule trust :premises () :args ((or @t815 @t819))) % 4.62/4.88 (step @p733 :rule chain_m_resolution :premises (@p732 @p731) :args (@t819 @t812 (@list @t815))) % 4.62/4.88 (step @p734 :rule cnf_equiv_neg2 :args (@t818)) % 4.62/4.88 (step @p735 :rule refl :args (@t820)) % 4.62/4.88 (step @p736 :rule cong :premises (@p512 @p735) :args (@t821)) % 4.62/4.88 (step @p737 :rule cong :premises (@p736) :args ((forall @t17 @t821))) % 4.62/4.88 (step @p738 :rule eq-symm :args (@t820 @t16)) % 4.62/4.88 (step @p739 :rule beta-reduce :args ((= @t822 @t16))) % 4.62/4.88 (step @p740 :rule refl :args (@t820)) % 4.62/4.88 (step @p741 :rule cong :premises (@p740 @p739) :args (@t823)) % 4.62/4.88 (step @p742 :rule trans :premises (@p741 @p738)) % 4.62/4.88 (step @p743 :rule cong :premises (@p742) :args (@t824)) % 4.62/4.88 (step @p744 :rule trans :premises (@p743 @p737)) % 4.62/4.88 (step @p745 :rule eq-refl :args (@t822)) % 4.62/4.88 (step @p746 :rule cong :premises (@p745) :args ((forall @t17 (= @t822 @t822)))) % 4.62/4.88 (step @p747 :rule trans :premises (@p746 @p352)) % 4.62/4.88 (step @p748 :rule refl :args (@t822)) % 4.62/4.88 (step @p749 :rule ho_cong :premises (@p682 @p357)) % 4.62/4.88 (step @p750 :rule cong :premises (@p749 @p748) :args (@t823)) % 4.62/4.88 (step @p751 :rule cong :premises (@p750) :args (@t824)) % 4.62/4.88 (step @p752 :rule trans :premises (@p751 @p747)) % 4.62/4.88 (step @p753 :rule true_elim :premises (@p752)) % 4.62/4.88 (step @p754 :rule eq_resolve :premises (@p753 @p744)) % 4.62/4.88 (step @p755 :rule eq-symm :args (@t689 @t817)) % 4.62/4.88 (step @p756 :rule refl :args (@t825)) % 4.62/4.88 (step @p757 :rule cong :premises (@p756 @p755) :args ((=> @t825 @t826))) % 4.62/4.88 (assume-push @p789 @t825) % 4.62/4.88 (step @p759 :rule instantiate :premises (@p754) :args (@t693)) % 4.62/4.88 (step-pop @p790 :rule scope :premises (@p759)) % 4.62/4.88 (step @p760 :rule process_scope :premises (@p790) :args (@t826)) % 4.62/4.88 (step @p762 :rule eq_resolve :premises (@p760 @p757)) % 4.62/4.88 (step @p763 :rule implies_elim :premises (@p762)) % 4.62/4.88 (step @p764 :rule chain_m_resolution :premises (@p763 @p754) :args (@t827 @t695 (@list @t825))) % 4.62/4.88 (step @p765 :rule cnf_equiv_pos1 :args (@t827)) % 4.62/4.88 (step @p766 :rule reordering :premises (@p765) :args ((or @t829 @t689 @t828))) % 4.62/4.88 (step @p767 :rule cnf_equiv_pos2 :args (@t694)) % 4.62/4.88 (step @p768 :rule reordering :premises (@p767) :args ((or @t690 @t831 @t830))) % 4.62/4.88 (step @p769 :rule chain_m_resolution :premises (@p768 @p374 @p766 @p764 @p734 @p733) :args (@t829 (@list false false false true true) (@list @t694 @t689 @t827 @t690 @t818))) % 4.62/4.88 (step @p770 :rule cnf_equiv_neg1 :args (@t818)) % 4.62/4.88 (step @p771 :rule reordering :premises (@p770) :args ((or @t817 @t690 @t818))) % 4.62/4.88 (step @p772 :rule chain_m_resolution :premises (@p771 @p769 @p733) :args (@t690 (@list true true) (@list @t817 @t818))) % 4.62/4.88 (step @p773 :rule cnf_equiv_pos2 :args (@t827)) % 4.62/4.88 (step @p774 :rule reordering :premises (@p773) :args ((or @t817 @t831 @t828))) % 4.62/4.88 (step @p775 :rule chain_m_resolution :premises (@p774 @p769 @p764) :args (@t831 @t814 (@list @t817 @t827))) % 4.62/4.88 (step @p776 :rule cnf_equiv_pos1 :args (@t694)) % 4.62/4.88 (step @p777 :rule reordering :premises (@p776) :args ((or (not @t690) @t689 @t830))) % 4.62/4.88 (step @p778 false :rule chain_m_resolution :premises (@p777 @p775 @p772 @p374) :args (false @t808 (@list @t689 @t690 @t694))) % 4.62/4.88 ) % 4.62/4.88 % SZS output end Proof % 4.62/4.89 % cvc5 exiting %------------------------------------------------------------------------------