%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP197^1 : TPTP v9.2.1. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n029.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:21 AM UTC 2026 % Result : Theorem 3.70s 3.99s % Output : Proof 3.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP197^1 : TPTP v9.2.1. Released v7.5.0. % 0.13/0.13 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.17/0.34 % Computer : n029.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:18:32 EDT 2026 % 0.17/0.34 % CPUTime : % 0.38/0.59 %----Proving TH0 % 3.70/3.99 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 90s... % 3.70/3.99 % SZS status Theorem % 3.70/3.99 % SZS output start Proof % 3.70/3.99 ( % 3.70/3.99 (declare-sort tptp.list_nat 0) % 3.70/3.99 (declare-sort tptp.nat 0) % 3.70/3.99 (declare-sort tptp.list_nat_o 0) % 3.70/3.99 (declare-sort tptp.set_nat 0) % 3.70/3.99 (declare-sort tptp.list_set_nat 0) % 3.70/3.99 (declare-sort tptp.list_l1704431731scheme 0) % 3.70/3.99 (declare-sort tptp.list_T247403987scheme 0) % 3.70/3.99 (declare-sort tptp.list_l1790670291le_typ 0) % 3.70/3.99 (declare-sort tptp.list_n396811828le_typ 0) % 3.70/3.99 (declare-sort tptp.list_l865305402le_typ 0) % 3.70/3.99 (declare-sort tptp.list_T1103309005le_typ 0) % 3.70/3.99 (declare-sort tptp.type_Mirabelle_typ 0) % 3.70/3.99 (declare-sort tptp.type_M1694694083scheme 0) % 3.70/3.99 (declare-sort tptp.list_l1334080099scheme 0) % 3.70/3.99 (declare-const tptp.sup_sup_nat (-> tptp.nat tptp.nat tptp.nat)) % 3.70/3.99 (declare-const tptp.type_M1691543772le_typ (-> tptp.list_n396811828le_typ tptp.set_nat)) % 3.70/3.99 (declare-const tptp.member_nat (-> tptp.nat tptp.set_nat Bool)) % 3.70/3.99 (declare-const tptp.type_M1958029241scheme (-> tptp.list_l1334080099scheme tptp.set_nat)) % 3.70/3.99 (declare-const tptp.type_M510873837le_typ (-> tptp.list_T1103309005le_typ tptp.set_nat)) % 3.70/3.99 (declare-const tptp.type_M1050318637scheme (-> tptp.type_M1694694083scheme tptp.set_nat)) % 3.70/3.99 (declare-const tptp.type_M49385309le_typ (-> tptp.type_Mirabelle_typ tptp.set_nat)) % 3.70/3.99 (declare-const tptp.type_M141510067scheme (-> tptp.list_T247403987scheme tptp.set_nat)) % 3.70/3.99 (declare-const tptp.type_Mirabelle_cod (-> (-> tptp.nat tptp.type_Mirabelle_typ) tptp.set_nat)) % 3.70/3.99 (declare-const tptp.type_Mirabelle_TVar (-> tptp.nat tptp.type_Mirabelle_typ)) % 3.70/3.99 (declare-const tptp.collect_nat (-> (-> tptp.nat Bool) tptp.set_nat)) % 3.70/3.99 (declare-const tptp.bot_bot_o Bool) % 3.70/3.99 (declare-const tptp.bot_bot_set_nat tptp.set_nat) % 3.70/3.99 (declare-const tptp.the_nat (-> (-> tptp.nat Bool) tptp.nat)) % 3.70/3.99 (declare-const tptp.sup_sup_nat_o (-> (-> tptp.nat Bool) (-> tptp.nat Bool) tptp.nat Bool)) % 3.70/3.99 (declare-const tptp.x tptp.nat) % 3.70/3.99 (declare-const tptp.s2 (-> tptp.nat tptp.type_Mirabelle_typ)) % 3.70/3.99 (declare-const tptp.nil_Ty61485117scheme tptp.list_T247403987scheme) % 3.70/3.99 (declare-const tptp.nil_nat tptp.list_nat) % 3.70/3.99 (declare-const tptp.s1 (-> tptp.nat tptp.type_Mirabelle_typ)) % 3.70/3.99 (declare-const tptp.cons_l1800589546le_typ (-> tptp.list_n396811828le_typ tptp.list_l865305402le_typ tptp.list_l865305402le_typ)) % 3.70/3.99 (declare-const tptp.type_M1826376056le_typ (-> tptp.nat tptp.list_l1790670291le_typ Bool)) % 3.70/3.99 (declare-const tptp.cons_T633159821scheme (-> tptp.type_M1694694083scheme tptp.list_T247403987scheme tptp.list_T247403987scheme)) % 3.70/3.99 (declare-const tptp.type_Mirabelle_Fun (-> tptp.type_Mirabelle_typ tptp.type_Mirabelle_typ tptp.type_Mirabelle_typ)) % 3.70/3.99 (declare-const tptp.cons_l1910959773scheme (-> tptp.list_T247403987scheme tptp.list_l1334080099scheme tptp.list_l1334080099scheme)) % 3.70/3.99 (declare-const tptp.type_M1944210753scheme (-> (-> tptp.nat tptp.type_Mirabelle_typ) tptp.list_T247403987scheme tptp.list_T247403987scheme)) % 3.70/3.99 (declare-const tptp.if_Typ1169047309le_typ (-> Bool tptp.type_Mirabelle_typ tptp.type_Mirabelle_typ tptp.type_Mirabelle_typ)) % 3.70/3.99 (declare-const tptp.type_M513401740le_typ (-> tptp.list_n396811828le_typ tptp.set_nat)) % 3.70/3.99 (declare-const tptp.cons_T363929085le_typ (-> tptp.type_Mirabelle_typ tptp.list_T1103309005le_typ tptp.list_T1103309005le_typ)) % 3.70/3.99 (declare-const tptp.type_M1898948661at_nat (-> tptp.nat tptp.nat)) % 3.70/3.99 (declare-const tptp.type_M784671311le_typ (-> (-> tptp.nat tptp.type_Mirabelle_typ) tptp.type_Mirabelle_typ tptp.type_Mirabelle_typ)) % 3.70/3.99 (declare-const tptp.cons_l392684675le_typ (-> tptp.list_T1103309005le_typ tptp.list_l1790670291le_typ tptp.list_l1790670291le_typ)) % 3.70/3.99 (declare-const tptp.type_M876316792e_FVar (-> tptp.nat tptp.type_M1694694083scheme)) % 3.70/3.99 (declare-const tptp.ord_lexordp_eq_nat_o (-> tptp.list_nat_o tptp.list_nat_o Bool)) % 3.70/3.99 (declare-const tptp.type_M1440203487le_typ (-> (-> tptp.nat tptp.type_Mirabelle_typ) tptp.list_T1103309005le_typ tptp.list_T1103309005le_typ)) % 3.70/3.99 (declare-const tptp.cons_set_nat (-> tptp.set_nat tptp.list_set_nat tptp.list_set_nat)) % 3.70/3.99 (declare-const tptp.type_M1690910139scheme (-> (-> tptp.nat tptp.type_Mirabelle_typ) tptp.type_M1694694083scheme tptp.type_M1694694083scheme)) % 3.70/3.99 (declare-const tptp.type_M1913464047le_typ (-> (-> tptp.nat tptp.type_Mirabelle_typ) tptp.list_l1790670291le_typ tptp.list_l1790670291le_typ)) % 3.70/3.99 (declare-const tptp.type_M1006385707scheme (-> tptp.type_Mirabelle_typ tptp.type_M1694694083scheme)) % 3.70/3.99 (declare-const tptp.type_M2048935292e_BVar (-> tptp.nat tptp.type_M1694694083scheme)) % 3.70/3.99 (declare-const tptp.type_M155660035e_SFun (-> tptp.type_M1694694083scheme tptp.type_M1694694083scheme tptp.type_M1694694083scheme)) % 3.70/3.99 (declare-const tptp.ord_lexordp_eq_nat (-> tptp.list_nat tptp.list_nat Bool)) % 3.70/3.99 (declare-const tptp.type_M2086816231le_typ (-> tptp.nat tptp.list_l865305402le_typ Bool)) % 3.70/3.99 (declare-const tptp.type_M737052622le_typ (-> (-> tptp.nat tptp.type_Mirabelle_typ) tptp.list_n396811828le_typ tptp.list_n396811828le_typ)) % 3.70/3.99 (declare-const tptp.type_M1158474302le_typ (-> (-> tptp.nat tptp.type_Mirabelle_typ) (-> tptp.nat tptp.type_Mirabelle_typ) tptp.nat tptp.type_Mirabelle_typ)) % 3.70/3.99 (declare-const tptp.ord_le727790544et_nat (-> tptp.list_set_nat tptp.list_set_nat Bool)) % 3.70/3.99 (declare-const tptp.cons_n499085924le_typ (-> (-> tptp.nat tptp.type_Mirabelle_typ) tptp.list_n396811828le_typ tptp.list_n396811828le_typ)) % 3.70/3.99 (declare-const tptp.type_M1172169604scheme (-> tptp.nat tptp.list_l1704431731scheme Bool)) % 3.70/3.99 (declare-const tptp.type_M1385924301scheme (-> (-> tptp.nat tptp.type_Mirabelle_typ) tptp.list_l1704431731scheme tptp.list_l1704431731scheme)) % 3.70/3.99 (declare-const tptp.bot_bot_nat tptp.nat) % 3.70/3.99 (declare-const tptp.n tptp.nat) % 3.70/3.99 (declare-const tptp.cons_l531914285scheme (-> tptp.list_l1334080099scheme tptp.list_l1704431731scheme tptp.list_l1704431731scheme)) % 3.70/3.99 (declare-const tptp.type_M1061687367scheme (-> (-> tptp.nat tptp.type_Mirabelle_typ) tptp.list_l1334080099scheme tptp.list_l1334080099scheme)) % 3.70/3.99 (declare-const tptp.cons_nat (-> tptp.nat tptp.list_nat tptp.list_nat)) % 3.70/3.99 (declare-const tptp.type_M326705277scheme (-> tptp.type_M1694694083scheme tptp.set_nat)) % 3.70/3.99 (declare-const tptp.type_M405566558_subst (-> tptp.nat tptp.type_Mirabelle_typ)) % 3.70/3.99 (declare-const tptp.type_M1539052445le_typ (-> tptp.list_T1103309005le_typ tptp.set_nat)) % 3.70/3.99 (declare-const tptp.type_M801073677le_typ (-> tptp.type_Mirabelle_typ tptp.set_nat)) % 3.70/3.99 (declare-const tptp.type_M772783356le_typ (-> (-> tptp.nat tptp.type_Mirabelle_typ) tptp.set_nat)) % 3.70/3.99 (declare-const tptp.type_M1496178953scheme (-> tptp.list_l1334080099scheme tptp.set_nat)) % 3.70/3.99 (declare-const tptp.type_M961603331scheme (-> tptp.list_T247403987scheme tptp.set_nat)) % 3.70/3.99 (declare-const tptp.semila1369944356et_nat (-> (-> tptp.set_nat tptp.set_nat tptp.set_nat) tptp.set_nat Bool)) % 3.70/3.99 (declare-const tptp.type_M906078444le_typ (-> tptp.list_l865305402le_typ tptp.set_nat)) % 3.70/3.99 (declare-const tptp.type_M1926053183scheme (-> tptp.list_l1704431731scheme tptp.set_nat)) % 3.70/3.99 (declare-const tptp.type_M1418941437le_typ (-> tptp.list_l1790670291le_typ tptp.set_nat)) % 3.70/3.99 (declare-const tptp.type_M1743451154le_typ (-> tptp.type_Mirabelle_typ tptp.type_Mirabelle_typ)) % 3.70/3.99 (declare-const tptp.nil_set_nat tptp.list_set_nat) % 3.70/3.99 (declare-const tptp.semila1414375521_nat_o (-> (-> (-> tptp.nat Bool) (-> tptp.nat Bool) tptp.nat Bool) (-> tptp.nat Bool) Bool)) % 3.70/3.99 (declare-const tptp.cons_nat_o (-> (-> tptp.nat Bool) tptp.list_nat_o tptp.list_nat_o)) % 3.70/3.99 (declare-const tptp.nil_nat_o tptp.list_nat_o) % 3.70/3.99 (define tptp.ord_less_nat () (let ((_let_1 (@var "B6" tptp.nat))) (let ((_let_2 (@var "A3" tptp.nat))) (lambda (@list _let_1 _let_2) (and (= _let_2 (_ (_ tptp.sup_sup_nat _let_2) _let_1)) (not (= _let_2 _let_1))))))) % 3.70/3.99 (define tptp.type_M244876119le_typ () (let ((_let_1 (@var "N3" tptp.nat))) (let ((_let_2 (@var "M2" tptp.nat))) (let ((_let_3 (@var "Ts" tptp.list_n396811828le_typ))) (lambda (@list _let_1 _let_3) (forall (@list _let_2) (=> (_ (_ tptp.member_nat _let_2) (_ tptp.type_M1691543772le_typ _let_3)) (_ (_ tptp.ord_less_nat _let_2) _let_1)))))))) % 3.70/3.99 (define tptp.type_M1377662078scheme () (let ((_let_1 (@var "N3" tptp.nat))) (let ((_let_2 (@var "M2" tptp.nat))) (let ((_let_3 (@var "Ts" tptp.list_l1334080099scheme))) (lambda (@list _let_1 _let_3) (forall (@list _let_2) (=> (_ (_ tptp.member_nat _let_2) (_ tptp.type_M1958029241scheme _let_3)) (_ (_ tptp.ord_less_nat _let_2) _let_1)))))))) % 3.70/3.99 (define tptp.type_M263553000le_typ () (let ((_let_1 (@var "N3" tptp.nat))) (let ((_let_2 (@var "M2" tptp.nat))) (let ((_let_3 (@var "Ts" tptp.list_T1103309005le_typ))) (lambda (@list _let_1 _let_3) (forall (@list _let_2) (=> (_ (_ tptp.member_nat _let_2) (_ tptp.type_M510873837le_typ _let_3)) (_ (_ tptp.ord_less_nat _let_2) _let_1)))))))) % 3.70/3.99 (define tptp.type_M1963061490scheme () (let ((_let_1 (@var "N3" tptp.nat))) (let ((_let_2 (@var "M2" tptp.nat))) (let ((_let_3 (@var "Ts" tptp.type_M1694694083scheme))) (lambda (@list _let_1 _let_3) (forall (@list _let_2) (=> (_ (_ tptp.member_nat _let_2) (_ tptp.type_M1050318637scheme _let_3)) (_ (_ tptp.ord_less_nat _let_2) _let_1)))))))) % 3.70/3.99 (define tptp.type_M1211611096le_typ () (let ((_let_1 (@var "N3" tptp.nat))) (let ((_let_2 (@var "M2" tptp.nat))) (let ((_let_3 (@var "Ts" tptp.type_Mirabelle_typ))) (lambda (@list _let_1 _let_3) (forall (@list _let_2) (=> (_ (_ tptp.member_nat _let_2) (_ tptp.type_M49385309le_typ _let_3)) (_ (_ tptp.ord_less_nat _let_2) _let_1)))))))) % 3.70/3.99 (define tptp.type_M2064939256scheme () (let ((_let_1 (@var "N3" tptp.nat))) (let ((_let_2 (@var "M2" tptp.nat))) (let ((_let_3 (@var "Ts" tptp.list_T247403987scheme))) (lambda (@list _let_1 _let_3) (forall (@list _let_2) (=> (_ (_ tptp.member_nat _let_2) (_ tptp.type_M141510067scheme _let_3)) (_ (_ tptp.ord_less_nat _let_2) _let_1)))))))) % 3.70/3.99 (define tptp.type_Mirabelle_dom () (let ((_let_1 (@var "N3" tptp.nat))) (let ((_let_2 (@var "S4" (-> tptp.nat tptp.type_Mirabelle_typ)))) (lambda (@list _let_2) (_ tptp.collect_nat (lambda (@list _let_1) (not (= (_ _let_2 _let_1) (_ tptp.type_Mirabelle_TVar _let_1))))))))) % 3.70/3.99 (define tptp.sup_sup_set_nat () (let ((_let_1 (@var "B4" tptp.set_nat))) (let ((_let_2 (@var "X4" tptp.nat))) (let ((_let_3 (_ tptp.member_nat _let_2))) (let ((_let_4 (@var "A4" tptp.set_nat))) (lambda (@list _let_4 _let_1) (_ tptp.collect_nat (lambda (@list _let_2) (or (_ _let_3 _let_4) (_ _let_3 _let_1)))))))))) % 3.70/3.99 (define tptp.type_M1715972684le_typ () (let ((_let_1 (@var "S4" (-> tptp.nat tptp.type_Mirabelle_typ)))) (lambda (@list _let_1) (_ (_ tptp.sup_sup_set_nat (_ tptp.type_Mirabelle_dom _let_1)) (_ tptp.type_Mirabelle_cod _let_1))))) % 3.70/3.99 (define tptp.type_M1734147655le_typ () (let ((_let_1 (@var "N3" tptp.nat))) (let ((_let_2 (@var "M2" tptp.nat))) (let ((_let_3 (@var "Ts" (-> tptp.nat tptp.type_Mirabelle_typ)))) (lambda (@list _let_1 _let_3) (forall (@list _let_2) (=> (_ (_ tptp.member_nat _let_2) (_ tptp.type_M1715972684le_typ _let_3)) (_ (_ tptp.ord_less_nat _let_2) _let_1)))))))) % 3.70/3.99 (define tptp.insert_nat () (let ((_let_1 (@var "B4" tptp.set_nat))) (let ((_let_2 (@var "X4" tptp.nat))) (let ((_let_3 (@var "A3" tptp.nat))) (lambda (@list _let_3 _let_1) (_ tptp.collect_nat (lambda (@list _let_2) (or (= _let_2 _let_3) (_ (_ tptp.member_nat _let_2) _let_1))))))))) % 3.70/3.99 (define tptp.bot_bot_nat_o () (lambda (@list (@var "X4" tptp.nat)) tptp.bot_bot_o)) % 3.70/3.99 (define tptp.the_elem_nat () (let ((_let_1 (@var "X4" tptp.nat))) (let ((_let_2 (@var "X6" tptp.set_nat))) (lambda (@list _let_2) (_ tptp.the_nat (lambda (@list _let_1) (= _let_2 (_ (_ tptp.insert_nat _let_1) tptp.bot_bot_set_nat)))))))) % 3.70/3.99 (define tptp.is_singleton_nat () (let ((_let_1 (@var "A4" tptp.set_nat))) (lambda (@list _let_1) (= _let_1 (_ (_ tptp.insert_nat (_ tptp.the_elem_nat _let_1)) tptp.bot_bot_set_nat))))) % 3.70/3.99 (define tptp.is_empty_nat () (let ((_let_1 (@var "A4" tptp.set_nat))) (lambda (@list _let_1) (= _let_1 tptp.bot_bot_set_nat)))) % 3.70/3.99 (define tptp.ord_less_nat_o () (let ((_let_1 (@var "B6" (-> tptp.nat Bool)))) (let ((_let_2 (@var "A3" (-> tptp.nat Bool)))) (lambda (@list _let_1 _let_2) (and (= _let_2 (_ (_ tptp.sup_sup_nat_o _let_2) _let_1)) (not (= _let_2 _let_1))))))) % 3.70/3.99 (define tptp.ord_less_set_nat () (let ((_let_1 (@var "B4" tptp.set_nat))) (let ((_let_2 (@var "X4" tptp.nat))) (let ((_let_3 (_ tptp.member_nat _let_2))) (let ((_let_4 (@list _let_2))) (let ((_let_5 (@var "A4" tptp.set_nat))) (lambda (@list _let_5 _let_1) (_ (_ tptp.ord_less_nat_o (lambda _let_4 (_ _let_3 _let_5))) (lambda _let_4 (_ _let_3 _let_1)))))))))) % 3.70/3.99 (define tptp.if_nat () (let ((_let_1 (@var "Y6" tptp.nat))) (let ((_let_2 (@var "Z3" tptp.nat))) (let ((_let_3 (@var "P3" Bool))) (let ((_let_4 (@var "X4" tptp.nat))) (lambda (@list _let_3 _let_4 _let_1) (_ tptp.the_nat (lambda (@list _let_2) (and (=> _let_3 (= _let_2 _let_4)) (=> (not _let_3) (= _let_2 _let_1))))))))))) % 3.70/3.99 (define @t1 () (@var "Y1" tptp.nat)) % 3.70/3.99 (define @t2 () (@var "X1" tptp.nat)) % 3.70/3.99 (define @t3 () (= @t2 @t1)) % 3.70/3.99 (define @t4 () (_ tptp.type_M876316792e_FVar @t2)) % 3.70/3.99 (define @t5 () (@list @t2 @t1)) % 3.70/3.99 (define @t6 () (@var "Sch" tptp.type_M1694694083scheme)) % 3.70/3.99 (define @t7 () (@var "S2" (-> tptp.nat tptp.type_Mirabelle_typ))) % 3.70/3.99 (define @t8 () (@var "S1" (-> tptp.nat tptp.type_Mirabelle_typ))) % 3.70/3.99 (define @t9 () (@var "N" tptp.nat)) % 3.70/3.99 (define @t10 () (= (_ @t8 @t9) (_ @t7 @t9))) % 3.70/3.99 (define @t11 () (_ tptp.type_M1050318637scheme @t6)) % 3.70/3.99 (define @t12 () (_ tptp.member_nat @t9)) % 3.70/3.99 (define @t13 () (@list @t9)) % 3.70/3.99 (define @t14 () (@var "S3" (-> tptp.nat tptp.type_Mirabelle_typ))) % 3.70/3.99 (define @t15 () (@var "S" (-> tptp.nat tptp.type_Mirabelle_typ))) % 3.70/3.99 (define @t16 () (_ tptp.type_M1690910139scheme @t15)) % 3.70/3.99 (define @t17 () (_ @t16 @t6)) % 3.70/3.99 (define @t18 () (@var "X" tptp.nat)) % 3.70/3.99 (define @t19 () (= (_ @t15 @t18) (_ @t14 @t18))) % 3.70/3.99 (define @t20 () (_ tptp.member_nat @t18)) % 3.70/3.99 (define @t21 () (@list @t18)) % 3.70/3.99 (define @t22 () (@var "N2" tptp.nat)) % 3.70/3.99 (define @t23 () (_ @t15 @t22)) % 3.70/3.99 (define @t24 () (_ tptp.type_M1006385707scheme @t23)) % 3.70/3.99 (define @t25 () (_ tptp.type_M876316792e_FVar @t22)) % 3.70/3.99 (define @t26 () (_ @t16 @t25)) % 3.70/3.99 (define @t27 () (= @t26 @t24)) % 3.70/3.99 (define @t28 () (@list @t15 @t22)) % 3.70/3.99 (define @t29 () (forall @t28 @t27)) % 3.70/3.99 (define @t30 () (_ tptp.type_M2048935292e_BVar @t22)) % 3.70/3.99 (define @t31 () (@var "Sch2" tptp.type_M1694694083scheme)) % 3.70/3.99 (define @t32 () (@var "Sch1" tptp.type_M1694694083scheme)) % 3.70/3.99 (define @t33 () (_ (_ tptp.type_M155660035e_SFun @t32) @t31)) % 3.70/3.99 (define @t34 () (@var "X2" tptp.nat)) % 3.70/3.99 (define @t35 () (_ tptp.type_M2048935292e_BVar @t34)) % 3.70/3.99 (define @t36 () (@var "X32" tptp.type_M1694694083scheme)) % 3.70/3.99 (define @t37 () (@var "X31" tptp.type_M1694694083scheme)) % 3.70/3.99 (define @t38 () (_ (_ tptp.type_M155660035e_SFun @t37) @t36)) % 3.70/3.99 (define @t39 () (@var "L" tptp.list_n396811828le_typ)) % 3.70/3.99 (define @t40 () (_ tptp.type_M737052622le_typ @t15)) % 3.70/3.99 (define @t41 () (@var "X3" (-> tptp.nat tptp.type_Mirabelle_typ))) % 3.70/3.99 (define @t42 () (_ tptp.cons_n499085924le_typ @t41)) % 3.70/3.99 (define @t43 () (_ @t42 @t39)) % 3.70/3.99 (define @t44 () (@var "L" tptp.list_l1704431731scheme)) % 3.70/3.99 (define @t45 () (_ tptp.type_M1385924301scheme @t15)) % 3.70/3.99 (define @t46 () (@var "X3" tptp.list_l1334080099scheme)) % 3.70/3.99 (define @t47 () (_ tptp.type_M1061687367scheme @t15)) % 3.70/3.99 (define @t48 () (_ (_ tptp.cons_l531914285scheme @t46) @t44)) % 3.70/3.99 (define @t49 () (@var "L" tptp.list_l1790670291le_typ)) % 3.70/3.99 (define @t50 () (_ tptp.type_M1913464047le_typ @t15)) % 3.70/3.99 (define @t51 () (@var "X3" tptp.list_T1103309005le_typ)) % 3.70/3.99 (define @t52 () (_ tptp.type_M1440203487le_typ @t15)) % 3.70/3.99 (define @t53 () (_ (_ tptp.cons_l392684675le_typ @t51) @t49)) % 3.70/3.99 (define @t54 () (@var "L" tptp.list_T1103309005le_typ)) % 3.70/3.99 (define @t55 () (@var "X3" tptp.type_Mirabelle_typ)) % 3.70/3.99 (define @t56 () (_ tptp.type_M784671311le_typ @t15)) % 3.70/3.99 (define @t57 () (_ tptp.cons_T363929085le_typ @t55)) % 3.70/3.99 (define @t58 () (_ @t57 @t54)) % 3.70/3.99 (define @t59 () (@var "L" tptp.list_l1334080099scheme)) % 3.70/3.99 (define @t60 () (@var "X3" tptp.list_T247403987scheme)) % 3.70/3.99 (define @t61 () (_ tptp.type_M1944210753scheme @t15)) % 3.70/3.99 (define @t62 () (_ tptp.cons_l1910959773scheme @t60)) % 3.70/3.99 (define @t63 () (_ @t62 @t59)) % 3.70/3.99 (define @t64 () (@var "L" tptp.list_T247403987scheme)) % 3.70/3.99 (define @t65 () (@var "X3" tptp.type_M1694694083scheme)) % 3.70/3.99 (define @t66 () (_ tptp.cons_T633159821scheme @t65)) % 3.70/3.99 (define @t67 () (_ @t66 @t64)) % 3.70/3.99 (define @t68 () (@var "T" tptp.type_Mirabelle_typ)) % 3.70/3.99 (define @t69 () (_ tptp.type_M49385309le_typ @t68)) % 3.70/3.99 (define @t70 () (_ tptp.type_M1006385707scheme @t68)) % 3.70/3.99 (define @t71 () (_ tptp.type_M1050318637scheme @t70)) % 3.70/3.99 (define @t72 () (= @t71 @t69)) % 3.70/3.99 (define @t73 () (forall (@list @t68) @t72)) % 3.70/3.99 (define @t74 () (@var "M" tptp.nat)) % 3.70/3.99 (define @t75 () (_ (_ tptp.insert_nat @t74) tptp.bot_bot_set_nat)) % 3.70/3.99 (define @t76 () (_ tptp.type_M876316792e_FVar @t74)) % 3.70/3.99 (define @t77 () (@list @t74)) % 3.70/3.99 (define @t78 () (@var "K" tptp.nat)) % 3.70/3.99 (define @t79 () (lambda (@list @t78) (_ (_ (_ tptp.if_Typ1169047309le_typ (_ (_ tptp.ord_less_nat @t78) @t22)) (_ @t15 @t78)) (_ @t14 @t78)))) % 3.70/3.99 (define @t80 () (_ tptp.type_M1963061490scheme @t22)) % 3.70/3.99 (define @t81 () (@var "Y32" tptp.type_M1694694083scheme)) % 3.70/3.99 (define @t82 () (@var "Y31" tptp.type_M1694694083scheme)) % 3.70/3.99 (define @t83 () (@var "Y2" tptp.nat)) % 3.70/3.99 (define @t84 () (@var "L" tptp.list_l865305402le_typ)) % 3.70/3.99 (define @t85 () (_ tptp.type_M2086816231le_typ @t22)) % 3.70/3.99 (define @t86 () (@var "X3" tptp.list_n396811828le_typ)) % 3.70/3.99 (define @t87 () (_ tptp.type_M244876119le_typ @t22)) % 3.70/3.99 (define @t88 () (_ (_ tptp.cons_l1800589546le_typ @t86) @t84)) % 3.70/3.99 (define @t89 () (_ tptp.type_M1826376056le_typ @t22)) % 3.70/3.99 (define @t90 () (_ tptp.type_M263553000le_typ @t22)) % 3.70/3.99 (define @t91 () (_ tptp.type_M1172169604scheme @t22)) % 3.70/3.99 (define @t92 () (_ tptp.type_M1377662078scheme @t22)) % 3.70/3.99 (define @t93 () (_ tptp.type_M2064939256scheme @t22)) % 3.70/3.99 (define @t94 () (_ tptp.type_M1211611096le_typ @t22)) % 3.70/3.99 (define @t95 () (_ tptp.type_M1734147655le_typ @t22)) % 3.70/3.99 (define @t96 () (_ @t56 @t68)) % 3.70/3.99 (define @t97 () (@var "T2" tptp.type_M1694694083scheme)) % 3.70/3.99 (define @t98 () (@var "T1" tptp.type_M1694694083scheme)) % 3.70/3.99 (define @t99 () (_ tptp.type_M2048935292e_BVar @t74)) % 3.70/3.99 (define @t100 () (@list @t22 @t74)) % 3.70/3.99 (define @t101 () (_ (_ tptp.ord_less_nat @t74) @t22)) % 3.70/3.99 (define @t102 () (@var "T22" tptp.type_Mirabelle_typ)) % 3.70/3.99 (define @t103 () (@var "T12" tptp.type_Mirabelle_typ)) % 3.70/3.99 (define @t104 () (_ (_ tptp.type_M784671311le_typ @t7) @t68)) % 3.70/3.99 (define @t105 () (_ (_ tptp.type_M784671311le_typ @t8) @t68)) % 3.70/3.99 (define @t106 () (= @t105 @t104)) % 3.70/3.99 (define @t107 () (_ @t7 @t22)) % 3.70/3.99 (define @t108 () (_ @t8 @t22)) % 3.70/3.99 (define @t109 () (= @t108 @t107)) % 3.70/3.99 (define @t110 () (_ tptp.member_nat @t22)) % 3.70/3.99 (define @t111 () (_ @t110 @t69)) % 3.70/3.99 (define @t112 () (=> @t111 @t109)) % 3.70/3.99 (define @t113 () (@list @t8 @t68 @t7 @t22)) % 3.70/3.99 (define @t114 () (forall @t113 (=> @t106 @t112))) % 3.70/3.99 (define @t115 () (@var "T3" tptp.type_Mirabelle_typ)) % 3.70/3.99 (define @t116 () (= @t68 @t115)) % 3.70/3.99 (define @t117 () (_ tptp.type_M1006385707scheme @t115)) % 3.70/3.99 (define @t118 () (= @t70 @t117)) % 3.70/3.99 (define @t119 () (@list @t68 @t115)) % 3.70/3.99 (define @t120 () (forall @t119 (=> @t118 @t116))) % 3.70/3.99 (define @t121 () (@var "X322" tptp.type_M1694694083scheme)) % 3.70/3.99 (define @t122 () (@var "X312" tptp.type_M1694694083scheme)) % 3.70/3.99 (define @t123 () (@var "Y" tptp.type_M1694694083scheme)) % 3.70/3.99 (define @t124 () (@var "X22" tptp.nat)) % 3.70/3.99 (define @t125 () (@var "X12" tptp.nat)) % 3.70/3.99 (define @t126 () (@list @t125)) % 3.70/3.99 (define @t127 () (@var "Type_scheme" tptp.type_M1694694083scheme)) % 3.70/3.99 (define @t128 () (@var "P" (-> tptp.type_M1694694083scheme Bool))) % 3.70/3.99 (define @t129 () (@var "X2a" tptp.type_M1694694083scheme)) % 3.70/3.99 (define @t130 () (@var "X1a" tptp.type_M1694694083scheme)) % 3.70/3.99 (define @t131 () (@var "A" tptp.nat)) % 3.70/3.99 (define @t132 () (_ tptp.insert_nat @t131)) % 3.70/3.99 (define @t133 () (_ @t132 tptp.bot_bot_set_nat)) % 3.70/3.99 (define @t134 () (@var "X4" tptp.nat)) % 3.70/3.99 (define @t135 () (= @t134 @t131)) % 3.70/3.99 (define @t136 () (@list @t134)) % 3.70/3.99 (define @t137 () (lambda @t136 @t135)) % 3.70/3.99 (define @t138 () (@list @t131)) % 3.70/3.99 (define @t139 () (@var "Z" tptp.nat)) % 3.70/3.99 (define @t140 () (@var "Y3" tptp.nat)) % 3.70/3.99 (define @t141 () (lambda (@list @t140 @t139) (= @t140 @t139))) % 3.70/3.99 (define @t142 () (_ tptp.member_nat @t131)) % 3.70/3.99 (define @t143 () (@var "B" tptp.set_nat)) % 3.70/3.99 (define @t144 () (@var "B2" tptp.nat)) % 3.70/3.99 (define @t145 () (_ tptp.insert_nat @t144)) % 3.70/3.99 (define @t146 () (_ @t145 @t143)) % 3.70/3.99 (define @t147 () (_ @t142 @t146)) % 3.70/3.99 (define @t148 () (= @t131 @t144)) % 3.70/3.99 (define @t149 () (_ @t142 @t143)) % 3.70/3.99 (define @t150 () (@list @t131 @t143 @t144)) % 3.70/3.99 (define @t151 () (@var "A2" tptp.set_nat)) % 3.70/3.99 (define @t152 () (_ @t142 @t151)) % 3.70/3.99 (define @t153 () (_ @t142 (_ @t145 @t151))) % 3.70/3.99 (define @t154 () (@list @t131 @t144 @t151)) % 3.70/3.99 (define @t155 () (@var "X3" tptp.nat)) % 3.70/3.99 (define @t156 () (_ tptp.insert_nat @t155)) % 3.70/3.99 (define @t157 () (_ @t156 @t151)) % 3.70/3.99 (define @t158 () (@list @t155 @t151)) % 3.70/3.99 (define @t159 () (@var "Y22" tptp.list_T247403987scheme)) % 3.70/3.99 (define @t160 () (@var "X222" tptp.list_T247403987scheme)) % 3.70/3.99 (define @t161 () (@var "Y21" tptp.type_M1694694083scheme)) % 3.70/3.99 (define @t162 () (@var "X21" tptp.type_M1694694083scheme)) % 3.70/3.99 (define @t163 () (@var "Y22" tptp.list_l1334080099scheme)) % 3.70/3.99 (define @t164 () (@var "X222" tptp.list_l1334080099scheme)) % 3.70/3.99 (define @t165 () (@var "Y21" tptp.list_T247403987scheme)) % 3.70/3.99 (define @t166 () (@var "X21" tptp.list_T247403987scheme)) % 3.70/3.99 (define @t167 () (@var "Y22" tptp.list_T1103309005le_typ)) % 3.70/3.99 (define @t168 () (@var "X222" tptp.list_T1103309005le_typ)) % 3.70/3.99 (define @t169 () (@var "Y21" tptp.type_Mirabelle_typ)) % 3.70/3.99 (define @t170 () (@var "X21" tptp.type_Mirabelle_typ)) % 3.70/3.99 (define @t171 () (= @t170 @t169)) % 3.70/3.99 (define @t172 () (@var "Y22" tptp.list_n396811828le_typ)) % 3.70/3.99 (define @t173 () (@var "X222" tptp.list_n396811828le_typ)) % 3.70/3.99 (define @t174 () (@var "Y21" (-> tptp.nat tptp.type_Mirabelle_typ))) % 3.70/3.99 (define @t175 () (@var "X21" (-> tptp.nat tptp.type_Mirabelle_typ))) % 3.70/3.99 (define @t176 () (@var "Y22" tptp.list_nat)) % 3.70/3.99 (define @t177 () (@var "X222" tptp.list_nat)) % 3.70/3.99 (define @t178 () (@var "Y21" tptp.nat)) % 3.70/3.99 (define @t179 () (@var "X21" tptp.nat)) % 3.70/3.99 (define @t180 () (@var "C" tptp.nat)) % 3.70/3.99 (define @t181 () (_ tptp.member_nat @t180)) % 3.70/3.99 (define @t182 () (@var "P" (-> tptp.nat Bool))) % 3.70/3.99 (define @t183 () (_ @t182 @t131)) % 3.70/3.99 (define @t184 () (_ tptp.collect_nat @t182)) % 3.70/3.99 (define @t185 () (@list @t131 @t182)) % 3.70/3.99 (define @t186 () (_ tptp.member_nat @t134)) % 3.70/3.99 (define @t187 () (_ @t186 @t151)) % 3.70/3.99 (define @t188 () (@list @t151)) % 3.70/3.99 (define @t189 () (@var "Q" (-> tptp.nat Bool))) % 3.70/3.99 (define @t190 () (_ tptp.collect_nat @t189)) % 3.70/3.99 (define @t191 () (_ @t189 @t18)) % 3.70/3.99 (define @t192 () (_ @t182 @t18)) % 3.70/3.99 (define @t193 () (@list @t182 @t189)) % 3.70/3.99 (define @t194 () (= @t151 tptp.bot_bot_set_nat)) % 3.70/3.99 (define @t195 () (_ @t182 @t134)) % 3.70/3.99 (define @t196 () (forall @t136 (not @t195))) % 3.70/3.99 (define @t197 () (= @t184 tptp.bot_bot_set_nat)) % 3.70/3.99 (define @t198 () (@list @t182)) % 3.70/3.99 (define @t199 () (@var "A2" tptp.list_T247403987scheme)) % 3.70/3.99 (define @t200 () (_ @t61 @t199)) % 3.70/3.99 (define @t201 () (not @t194)) % 3.70/3.99 (define @t202 () (@var "Y4" tptp.nat)) % 3.70/3.99 (define @t203 () (_ (_ tptp.member_nat @t202) @t151)) % 3.70/3.99 (define @t204 () (@list @t202)) % 3.70/3.99 (define @t205 () (not @t152)) % 3.70/3.99 (define @t206 () (@var "Xs" tptp.list_T247403987scheme)) % 3.70/3.99 (define @t207 () (@var "Xs" tptp.list_l1334080099scheme)) % 3.70/3.99 (define @t208 () (@var "Xs" tptp.list_T1103309005le_typ)) % 3.70/3.99 (define @t209 () (@var "Xs" tptp.list_n396811828le_typ)) % 3.70/3.99 (define @t210 () (@var "Xs" tptp.list_nat)) % 3.70/3.99 (define @t211 () (_ (_ tptp.cons_nat @t155) @t210)) % 3.70/3.99 (define @t212 () (@var "B3" tptp.set_nat)) % 3.70/3.99 (define @t213 () (@list @t212)) % 3.70/3.99 (define @t214 () (@list @t131 @t151)) % 3.70/3.99 (define @t215 () (@var "Y" tptp.nat)) % 3.70/3.99 (define @t216 () (_ tptp.insert_nat @t215)) % 3.70/3.99 (define @t217 () (@var "C2" tptp.set_nat)) % 3.70/3.99 (define @t218 () (_ tptp.member_nat @t144)) % 3.70/3.99 (define @t219 () (not @t148)) % 3.70/3.99 (define @t220 () (= @t151 @t143)) % 3.70/3.99 (define @t221 () (_ @t132 @t151)) % 3.70/3.99 (define @t222 () (_ tptp.member_nat @t155)) % 3.70/3.99 (define @t223 () (_ @t222 @t151)) % 3.70/3.99 (define @t224 () (@list @t155 @t151 @t143)) % 3.70/3.99 (define @t225 () (_ @t132 @t143)) % 3.70/3.99 (define @t226 () (@var "U" tptp.nat)) % 3.70/3.99 (define @t227 () (_ @t145 tptp.bot_bot_set_nat)) % 3.70/3.99 (define @t228 () (@list @t131 @t144)) % 3.70/3.99 (define @t229 () (= @t144 @t180)) % 3.70/3.99 (define @t230 () (@var "D" tptp.nat)) % 3.70/3.99 (define @t231 () (= @t144 @t131)) % 3.70/3.99 (define @t232 () (_ @t218 @t133)) % 3.70/3.99 (define @t233 () (@list @t144 @t131)) % 3.70/3.99 (define @t234 () (_ tptp.collect_nat (lambda @t136 (and (= @t131 @t134) @t195)))) % 3.70/3.99 (define @t235 () (not @t183)) % 3.70/3.99 (define @t236 () (@list @t182 @t131)) % 3.70/3.99 (define @t237 () (_ tptp.collect_nat (lambda @t136 (and @t135 @t195)))) % 3.70/3.99 (define @t238 () (_ @t156 tptp.bot_bot_set_nat)) % 3.70/3.99 (define @t239 () (@list @t155)) % 3.70/3.99 (define @t240 () (@var "A" (-> tptp.nat Bool))) % 3.70/3.99 (define @t241 () (= @t240 tptp.bot_bot_nat_o)) % 3.70/3.99 (define @t242 () (@list @t240)) % 3.70/3.99 (define @t243 () (@var "A" tptp.set_nat)) % 3.70/3.99 (define @t244 () (= @t243 tptp.bot_bot_set_nat)) % 3.70/3.99 (define @t245 () (@list @t243)) % 3.70/3.99 (define @t246 () (_ tptp.ord_less_nat_o @t240)) % 3.70/3.99 (define @t247 () (_ tptp.ord_less_set_nat @t243)) % 3.70/3.99 (define @t248 () (_ tptp.ord_less_nat @t131)) % 3.70/3.99 (define @t249 () (_ tptp.type_Mirabelle_TVar @t74)) % 3.70/3.99 (define @t250 () (_ tptp.type_Mirabelle_TVar @t2)) % 3.70/3.99 (define @t251 () (@list @t22)) % 3.70/3.99 (define @t252 () (_ tptp.type_M141510067scheme @t199)) % 3.70/3.99 (define @t253 () (_ tptp.ord_less_set_nat @t151)) % 3.70/3.99 (define @t254 () (_ tptp.type_Mirabelle_TVar @t22)) % 3.70/3.99 (define @t255 () (_ @t56 @t254)) % 3.70/3.99 (define @t256 () (forall @t28 (= @t255 @t23))) % 3.70/3.99 (define @t257 () (_ tptp.is_singleton_nat @t151)) % 3.70/3.99 (define @t258 () (@list @t18 @t202)) % 3.70/3.99 (define @t259 () (@var "F" (-> tptp.nat tptp.set_nat))) % 3.70/3.99 (define @t260 () (_ (_ tptp.ord_less_nat @t18) @t202)) % 3.70/3.99 (define @t261 () (forall @t258 (=> @t260 (_ (_ tptp.ord_less_set_nat (_ @t259 @t18)) (_ @t259 @t202))))) % 3.70/3.99 (define @t262 () (_ tptp.ord_less_nat @t144)) % 3.70/3.99 (define @t263 () (_ @t262 @t180)) % 3.70/3.99 (define @t264 () (=> @t263 (=> @t261 (_ @t247 (_ @t259 @t180))))) % 3.70/3.99 (define @t265 () (_ @t259 @t144)) % 3.70/3.99 (define @t266 () (@list @t243 @t259 @t144 @t180)) % 3.70/3.99 (define @t267 () (@var "F" (-> tptp.nat tptp.nat Bool))) % 3.70/3.99 (define @t268 () (forall @t258 (=> @t260 (_ (_ tptp.ord_less_nat_o (_ @t267 @t18)) (_ @t267 @t202))))) % 3.70/3.99 (define @t269 () (=> @t263 (=> @t268 (_ @t246 (_ @t267 @t180))))) % 3.70/3.99 (define @t270 () (_ @t267 @t144)) % 3.70/3.99 (define @t271 () (@list @t240 @t267 @t144 @t180)) % 3.70/3.99 (define @t272 () (@var "C" tptp.set_nat)) % 3.70/3.99 (define @t273 () (@var "F" (-> tptp.set_nat tptp.nat))) % 3.70/3.99 (define @t274 () (@var "Y4" tptp.set_nat)) % 3.70/3.99 (define @t275 () (@var "X" tptp.set_nat)) % 3.70/3.99 (define @t276 () (_ (_ tptp.ord_less_set_nat @t275) @t274)) % 3.70/3.99 (define @t277 () (@list @t275 @t274)) % 3.70/3.99 (define @t278 () (forall @t277 (=> @t276 (_ (_ tptp.ord_less_nat (_ @t273 @t275)) (_ @t273 @t274))))) % 3.70/3.99 (define @t279 () (@var "B2" tptp.set_nat)) % 3.70/3.99 (define @t280 () (_ tptp.ord_less_set_nat @t279)) % 3.70/3.99 (define @t281 () (_ @t280 @t272)) % 3.70/3.99 (define @t282 () (=> @t281 (=> @t278 (_ @t248 (_ @t273 @t272))))) % 3.70/3.99 (define @t283 () (_ @t273 @t279)) % 3.70/3.99 (define @t284 () (@list @t131 @t273 @t279 @t272)) % 3.70/3.99 (define @t285 () (@var "F" (-> tptp.set_nat tptp.set_nat))) % 3.70/3.99 (define @t286 () (forall @t277 (=> @t276 (_ (_ tptp.ord_less_set_nat (_ @t285 @t275)) (_ @t285 @t274))))) % 3.70/3.99 (define @t287 () (=> @t281 (=> @t286 (_ @t247 (_ @t285 @t272))))) % 3.70/3.99 (define @t288 () (_ @t285 @t279)) % 3.70/3.99 (define @t289 () (@list @t243 @t285 @t279 @t272)) % 3.70/3.99 (define @t290 () (@var "F" (-> tptp.set_nat tptp.nat Bool))) % 3.70/3.99 (define @t291 () (forall @t277 (=> @t276 (_ (_ tptp.ord_less_nat_o (_ @t290 @t275)) (_ @t290 @t274))))) % 3.70/3.99 (define @t292 () (=> @t281 (=> @t291 (_ @t246 (_ @t290 @t272))))) % 3.70/3.99 (define @t293 () (_ @t290 @t279)) % 3.70/3.99 (define @t294 () (@list @t240 @t290 @t279 @t272)) % 3.70/3.99 (define @t295 () (@var "C" (-> tptp.nat Bool))) % 3.70/3.99 (define @t296 () (@var "F" (-> (-> tptp.nat Bool) tptp.nat))) % 3.70/3.99 (define @t297 () (@var "Y4" (-> tptp.nat Bool))) % 3.70/3.99 (define @t298 () (@var "X" (-> tptp.nat Bool))) % 3.70/3.99 (define @t299 () (_ (_ tptp.ord_less_nat_o @t298) @t297)) % 3.70/3.99 (define @t300 () (@list @t298 @t297)) % 3.70/3.99 (define @t301 () (forall @t300 (=> @t299 (_ (_ tptp.ord_less_nat (_ @t296 @t298)) (_ @t296 @t297))))) % 3.70/3.99 (define @t302 () (@var "B2" (-> tptp.nat Bool))) % 3.70/3.99 (define @t303 () (_ tptp.ord_less_nat_o @t302)) % 3.70/3.99 (define @t304 () (_ @t303 @t295)) % 3.70/3.99 (define @t305 () (=> @t304 (=> @t301 (_ @t248 (_ @t296 @t295))))) % 3.70/3.99 (define @t306 () (_ @t296 @t302)) % 3.70/3.99 (define @t307 () (@list @t131 @t296 @t302 @t295)) % 3.70/3.99 (define @t308 () (@var "F" (-> (-> tptp.nat Bool) tptp.set_nat))) % 3.70/3.99 (define @t309 () (forall @t300 (=> @t299 (_ (_ tptp.ord_less_set_nat (_ @t308 @t298)) (_ @t308 @t297))))) % 3.70/3.99 (define @t310 () (=> @t304 (=> @t309 (_ @t247 (_ @t308 @t295))))) % 3.70/3.99 (define @t311 () (_ @t308 @t302)) % 3.70/3.99 (define @t312 () (@list @t243 @t308 @t302 @t295)) % 3.70/3.99 (define @t313 () (@var "F" (-> (-> tptp.nat Bool) tptp.nat Bool))) % 3.70/3.99 (define @t314 () (forall @t300 (=> @t299 (_ (_ tptp.ord_less_nat_o (_ @t313 @t298)) (_ @t313 @t297))))) % 3.70/3.99 (define @t315 () (=> @t304 (=> @t314 (_ @t246 (_ @t313 @t295))))) % 3.70/3.99 (define @t316 () (_ @t313 @t302)) % 3.70/3.99 (define @t317 () (@list @t240 @t313 @t302 @t295)) % 3.70/3.99 (define @t318 () (@var "F" (-> tptp.nat tptp.nat))) % 3.70/3.99 (define @t319 () (forall @t258 (=> @t260 (_ (_ tptp.ord_less_nat (_ @t318 @t18)) (_ @t318 @t202))))) % 3.70/3.99 (define @t320 () (=> @t263 (=> @t319 (_ @t248 (_ @t318 @t180))))) % 3.70/3.99 (define @t321 () (_ @t318 @t144)) % 3.70/3.99 (define @t322 () (@list @t131 @t318 @t144 @t180)) % 3.70/3.99 (define @t323 () (=> @t261 (_ (_ tptp.ord_less_set_nat (_ @t259 @t131)) @t272))) % 3.70/3.99 (define @t324 () (_ @t248 @t144)) % 3.70/3.99 (define @t325 () (@list @t131 @t144 @t259 @t272)) % 3.70/3.99 (define @t326 () (=> @t268 (_ (_ tptp.ord_less_nat_o (_ @t267 @t131)) @t295))) % 3.70/3.99 (define @t327 () (@list @t131 @t144 @t267 @t295)) % 3.70/3.99 (define @t328 () (=> @t278 (_ (_ tptp.ord_less_nat (_ @t273 @t243)) @t180))) % 3.70/3.99 (define @t329 () (_ @t247 @t279)) % 3.70/3.99 (define @t330 () (@list @t243 @t279 @t273 @t180)) % 3.70/3.99 (define @t331 () (=> @t286 (_ (_ tptp.ord_less_set_nat (_ @t285 @t243)) @t272))) % 3.70/3.99 (define @t332 () (@list @t243 @t279 @t285 @t272)) % 3.70/3.99 (define @t333 () (=> @t291 (_ (_ tptp.ord_less_nat_o (_ @t290 @t243)) @t295))) % 3.70/3.99 (define @t334 () (@list @t243 @t279 @t290 @t295)) % 3.70/3.99 (define @t335 () (=> @t301 (_ (_ tptp.ord_less_nat (_ @t296 @t240)) @t180))) % 3.70/3.99 (define @t336 () (_ @t246 @t302)) % 3.70/3.99 (define @t337 () (@list @t240 @t302 @t296 @t180)) % 3.70/3.99 (define @t338 () (=> @t309 (_ (_ tptp.ord_less_set_nat (_ @t308 @t240)) @t272))) % 3.70/3.99 (define @t339 () (@list @t240 @t302 @t308 @t272)) % 3.70/3.99 (define @t340 () (=> @t314 (_ (_ tptp.ord_less_nat_o (_ @t313 @t240)) @t295))) % 3.70/3.99 (define @t341 () (@list @t240 @t302 @t313 @t295)) % 3.70/3.99 (define @t342 () (=> @t319 (_ (_ tptp.ord_less_nat (_ @t318 @t131)) @t180))) % 3.70/3.99 (define @t343 () (@list @t131 @t144 @t318 @t180)) % 3.70/3.99 (define @t344 () (@var "X_1" tptp.nat)) % 3.70/3.99 (define @t345 () (_ tptp.ord_less_nat @t155)) % 3.70/3.99 (define @t346 () (_ tptp.ord_less_nat @t215)) % 3.70/3.99 (define @t347 () (_ @t346 @t155)) % 3.70/3.99 (define @t348 () (_ @t345 @t215)) % 3.70/3.99 (define @t349 () (not @t348)) % 3.70/3.99 (define @t350 () (= @t155 @t215)) % 3.70/3.99 (define @t351 () (not @t350)) % 3.70/3.99 (define @t352 () (@list @t155 @t215)) % 3.70/3.99 (define @t353 () (_ @t280 @t243)) % 3.70/3.99 (define @t354 () (@list @t243 @t279)) % 3.70/3.99 (define @t355 () (_ @t303 @t240)) % 3.70/3.99 (define @t356 () (@list @t240 @t302)) % 3.70/3.99 (define @t357 () (_ @t262 @t131)) % 3.70/3.99 (define @t358 () (@var "Y" tptp.set_nat)) % 3.70/3.99 (define @t359 () (@var "X3" tptp.set_nat)) % 3.70/3.99 (define @t360 () (_ tptp.ord_less_set_nat @t359)) % 3.70/3.99 (define @t361 () (_ @t360 @t358)) % 3.70/3.99 (define @t362 () (@list @t359 @t358)) % 3.70/3.99 (define @t363 () (@var "Y" (-> tptp.nat Bool))) % 3.70/3.99 (define @t364 () (@var "X3" (-> tptp.nat Bool))) % 3.70/3.99 (define @t365 () (_ tptp.ord_less_nat_o @t364)) % 3.70/3.99 (define @t366 () (_ @t365 @t363)) % 3.70/3.99 (define @t367 () (@list @t364 @t363)) % 3.70/3.99 (define @t368 () (_ tptp.ord_less_set_nat @t358)) % 3.70/3.99 (define @t369 () (_ @t368 @t359)) % 3.70/3.99 (define @t370 () (not @t369)) % 3.70/3.99 (define @t371 () (_ tptp.ord_less_nat_o @t363)) % 3.70/3.99 (define @t372 () (_ @t371 @t364)) % 3.70/3.99 (define @t373 () (not @t372)) % 3.70/3.99 (define @t374 () (not @t347)) % 3.70/3.99 (define @t375 () (@var "Z2" tptp.set_nat)) % 3.70/3.99 (define @t376 () (@var "Z2" (-> tptp.nat Bool))) % 3.70/3.99 (define @t377 () (@var "Z2" tptp.nat)) % 3.70/3.99 (define @t378 () (@list @t359)) % 3.70/3.99 (define @t379 () (@list @t364)) % 3.70/3.99 (define @t380 () (_ @t247 @t272)) % 3.70/3.99 (define @t381 () (=> @t281 @t380)) % 3.70/3.99 (define @t382 () (= @t243 @t279)) % 3.70/3.99 (define @t383 () (@list @t243 @t279 @t272)) % 3.70/3.99 (define @t384 () (_ @t246 @t295)) % 3.70/3.99 (define @t385 () (=> @t304 @t384)) % 3.70/3.99 (define @t386 () (= @t240 @t302)) % 3.70/3.99 (define @t387 () (@list @t240 @t302 @t295)) % 3.70/3.99 (define @t388 () (_ @t248 @t180)) % 3.70/3.99 (define @t389 () (=> @t263 @t388)) % 3.70/3.99 (define @t390 () (@list @t131 @t144 @t180)) % 3.70/3.99 (define @t391 () (@list @t279 @t243)) % 3.70/3.99 (define @t392 () (@list @t302 @t240)) % 3.70/3.99 (define @t393 () (@var "Y5" tptp.nat)) % 3.70/3.99 (define @t394 () (@var "P" Bool)) % 3.70/3.99 (define @t395 () (@var "M2" tptp.nat)) % 3.70/3.99 (define @t396 () (@var "P3" (-> tptp.nat Bool))) % 3.70/3.99 (define @t397 () (@var "N3" tptp.nat)) % 3.70/3.99 (define @t398 () (_ (_ tptp.ord_less_nat @t395) @t397)) % 3.70/3.99 (define @t399 () (@list @t395)) % 3.70/3.99 (define @t400 () (@list @t397)) % 3.70/3.99 (define @t401 () (@var "X5" tptp.nat)) % 3.70/3.99 (define @t402 () (@var "P2" (-> tptp.nat Bool))) % 3.70/3.99 (define @t403 () (@var "P" (-> tptp.nat tptp.nat Bool))) % 3.70/3.99 (define @t404 () (@var "B5" tptp.nat)) % 3.70/3.99 (define @t405 () (@var "A5" tptp.nat)) % 3.70/3.99 (define @t406 () (_ @t403 @t405)) % 3.70/3.99 (define @t407 () (_ @t406 @t404)) % 3.70/3.99 (define @t408 () (@list @t405 @t404)) % 3.70/3.99 (define @t409 () (_ tptp.ord_less_set_nat @t272)) % 3.70/3.99 (define @t410 () (_ @t409 @t243)) % 3.70/3.99 (define @t411 () (_ @t409 @t279)) % 3.70/3.99 (define @t412 () (_ tptp.ord_less_nat_o @t295)) % 3.70/3.99 (define @t413 () (_ @t412 @t240)) % 3.70/3.99 (define @t414 () (_ @t412 @t302)) % 3.70/3.99 (define @t415 () (_ tptp.ord_less_nat @t180)) % 3.70/3.99 (define @t416 () (_ @t415 @t131)) % 3.70/3.99 (define @t417 () (_ @t415 @t144)) % 3.70/3.99 (define @t418 () (not @t382)) % 3.70/3.99 (define @t419 () (not @t386)) % 3.70/3.99 (define @t420 () (_ tptp.type_M1006385707scheme @t254)) % 3.70/3.99 (define @t421 () (forall @t251 (= @t420 @t25))) % 3.70/3.99 (define @t422 () (_ (_ tptp.insert_nat @t134) tptp.bot_bot_set_nat)) % 3.70/3.99 (define @t423 () (@var "A4" tptp.set_nat)) % 3.70/3.99 (define @t424 () (@list @t423)) % 3.70/3.99 (define @t425 () (@var "T2" tptp.type_Mirabelle_typ)) % 3.70/3.99 (define @t426 () (@var "T1" tptp.type_Mirabelle_typ)) % 3.70/3.99 (define @t427 () (_ (_ tptp.type_Mirabelle_Fun @t426) @t425)) % 3.70/3.99 (define @t428 () (@list @t426 @t425)) % 3.70/3.99 (define @t429 () (@var "Y22" tptp.type_Mirabelle_typ)) % 3.70/3.99 (define @t430 () (@var "X222" tptp.type_Mirabelle_typ)) % 3.70/3.99 (define @t431 () (_ (_ tptp.type_Mirabelle_Fun @t170) @t430)) % 3.70/3.99 (define @t432 () (_ @t181 @t143)) % 3.70/3.99 (define @t433 () (_ @t181 @t151)) % 3.70/3.99 (define @t434 () (_ @t253 @t143)) % 3.70/3.99 (define @t435 () (@var "C3" tptp.set_nat)) % 3.70/3.99 (define @t436 () (@list @t151 @t143 @t435)) % 3.70/3.99 (define @t437 () (@var "X223" tptp.type_Mirabelle_typ)) % 3.70/3.99 (define @t438 () (@var "X212" tptp.type_Mirabelle_typ)) % 3.70/3.99 (define @t439 () (@var "Y" tptp.type_Mirabelle_typ)) % 3.70/3.99 (define @t440 () (@var "Typ" tptp.type_Mirabelle_typ)) % 3.70/3.99 (define @t441 () (@var "P" (-> tptp.type_Mirabelle_typ Bool))) % 3.70/3.99 (define @t442 () (@var "X22" tptp.type_Mirabelle_typ)) % 3.70/3.99 (define @t443 () (@var "X1a" tptp.type_Mirabelle_typ)) % 3.70/3.99 (define @t444 () (_ @t141 @t155)) % 3.70/3.99 (define @t445 () (_ tptp.the_nat @t182)) % 3.70/3.99 (define @t446 () (= @t445 @t131)) % 3.70/3.99 (define @t447 () (forall @t21 (=> @t192 (= @t18 @t131)))) % 3.70/3.99 (define @t448 () (_ @t182 @t445)) % 3.70/3.99 (define @t449 () (@var "X7" tptp.nat)) % 3.70/3.99 (define @t450 () (_ @t182 @t449)) % 3.70/3.99 (define @t451 () (@list @t449)) % 3.70/3.99 (define @t452 () (exists @t451 (and @t450 (forall @t204 (=> (_ @t182 @t202) (= @t202 @t449)))))) % 3.70/3.99 (define @t453 () (=> (forall @t21 (=> @t192 @t191)) (_ @t189 @t445))) % 3.70/3.99 (define @t454 () (_ tptp.sup_sup_set_nat @t151)) % 3.70/3.99 (define @t455 () (_ @t454 @t143)) % 3.70/3.99 (define @t456 () (_ @t181 @t455)) % 3.70/3.99 (define @t457 () (@list @t180 @t143 @t151)) % 3.70/3.99 (define @t458 () (@list @t180 @t151 @t143)) % 3.70/3.99 (define @t459 () (= @t143 tptp.bot_bot_set_nat)) % 3.70/3.99 (define @t460 () (@list @t151 @t143)) % 3.70/3.99 (define @t461 () (_ tptp.sup_sup_set_nat @t143)) % 3.70/3.99 (define @t462 () (_ @t461 @t435)) % 3.70/3.99 (define @t463 () (@var "Q" Bool)) % 3.70/3.99 (define @t464 () (_ @t186 @t143)) % 3.70/3.99 (define @t465 () (_ @t186 @t455)) % 3.70/3.99 (define @t466 () (@list @t151 @t143 @t182)) % 3.70/3.99 (define @t467 () (_ @t454 @t462)) % 3.70/3.99 (define @t468 () (@var "B4" tptp.set_nat)) % 3.70/3.99 (define @t469 () (@list @t423 @t468)) % 3.70/3.99 (define @t470 () (@var "__flatten_var_0" tptp.set_nat)) % 3.70/3.99 (define @t471 () (@var "A3" tptp.nat)) % 3.70/3.99 (define @t472 () (= @t134 @t471)) % 3.70/3.99 (define @t473 () (@list @t471 @t470)) % 3.70/3.99 (define @t474 () (_ tptp.sup_sup_set_nat tptp.bot_bot_set_nat)) % 3.70/3.99 (define @t475 () (= @t143 @t238)) % 3.70/3.99 (define @t476 () (= @t151 @t238)) % 3.70/3.99 (define @t477 () (or (and @t194 @t475) (and @t476 @t459) (and @t476 @t475))) % 3.70/3.99 (define @t478 () (@list @t55 @t54)) % 3.70/3.99 (define @t479 () (@list @t41 @t39)) % 3.70/3.99 (define @t480 () (@list @t60 @t59)) % 3.70/3.99 (define @t481 () (@list @t65 @t64)) % 3.70/3.99 (define @t482 () (@var "S2" tptp.type_M1694694083scheme)) % 3.70/3.99 (define @t483 () (@var "S1" tptp.type_M1694694083scheme)) % 3.70/3.99 (define @t484 () (_ (_ tptp.type_M155660035e_SFun @t483) @t482)) % 3.70/3.99 (define @t485 () (@list @t483 @t482)) % 3.70/3.99 (define @t486 () (@var "F2" (-> tptp.nat tptp.type_Mirabelle_typ))) % 3.70/3.99 (define @t487 () (lambda @t400 (_ tptp.type_M1743451154le_typ (_ @t486 (_ tptp.type_M1898948661at_nat @t397))))) % 3.70/3.99 (define @t488 () (_ tptp.sup_sup_nat_o tptp.bot_bot_nat_o)) % 3.70/3.99 (define @t489 () (_ tptp.sup_sup_nat_o @t364)) % 3.70/3.99 (define @t490 () (_ tptp.sup_sup_set_nat @t359)) % 3.70/3.99 (define @t491 () (_ tptp.sup_sup_nat_o @t240)) % 3.70/3.99 (define @t492 () (_ tptp.sup_sup_set_nat @t243)) % 3.70/3.99 (define @t493 () (and @t241 (= @t302 tptp.bot_bot_nat_o))) % 3.70/3.99 (define @t494 () (_ @t491 @t302)) % 3.70/3.99 (define @t495 () (and @t244 (= @t279 tptp.bot_bot_set_nat))) % 3.70/3.99 (define @t496 () (_ @t492 @t279)) % 3.70/3.99 (define @t497 () (and (= @t364 tptp.bot_bot_nat_o) (= @t363 tptp.bot_bot_nat_o))) % 3.70/3.99 (define @t498 () (_ @t489 @t363)) % 3.70/3.99 (define @t499 () (and (= @t359 tptp.bot_bot_set_nat) (= @t358 tptp.bot_bot_set_nat))) % 3.70/3.99 (define @t500 () (_ @t490 @t358)) % 3.70/3.99 (define @t501 () (@var "S" tptp.set_nat)) % 3.70/3.99 (define @t502 () (@var "R" tptp.set_nat)) % 3.70/3.99 (define @t503 () (_ @t186 @t468)) % 3.70/3.99 (define @t504 () (lambda @t136 @t503)) % 3.70/3.99 (define @t505 () (_ @t186 @t423)) % 3.70/3.99 (define @t506 () (lambda @t136 @t505)) % 3.70/3.99 (define @t507 () (_ @t365 @t494)) % 3.70/3.99 (define @t508 () (_ @t360 @t496)) % 3.70/3.99 (define @t509 () (_ (_ tptp.sup_sup_nat @t131) @t144)) % 3.70/3.99 (define @t510 () (_ @t345 @t509)) % 3.70/3.99 (define @t511 () (@var "B6" tptp.set_nat)) % 3.70/3.99 (define @t512 () (@var "A3" tptp.set_nat)) % 3.70/3.99 (define @t513 () (_ @t412 @t494)) % 3.70/3.99 (define @t514 () (_ @t409 @t496)) % 3.70/3.99 (define @t515 () (_ @t415 @t509)) % 3.70/3.99 (define @t516 () (@list @t182 @t155)) % 3.70/3.99 (define @t517 () (@var "Ys" tptp.list_set_nat)) % 3.70/3.99 (define @t518 () (@var "Xs" tptp.list_set_nat)) % 3.70/3.99 (define @t519 () (_ (_ tptp.ord_le727790544et_nat @t518) @t517)) % 3.70/3.99 (define @t520 () (_ (_ tptp.ord_le727790544et_nat (_ (_ tptp.cons_set_nat @t359) @t518)) (_ (_ tptp.cons_set_nat @t358) @t517))) % 3.70/3.99 (define @t521 () (@var "Ys" tptp.list_nat_o)) % 3.70/3.99 (define @t522 () (@var "Xs" tptp.list_nat_o)) % 3.70/3.99 (define @t523 () (_ (_ tptp.ord_lexordp_eq_nat_o @t522) @t521)) % 3.70/3.99 (define @t524 () (_ (_ tptp.ord_lexordp_eq_nat_o (_ (_ tptp.cons_nat_o @t364) @t522)) (_ (_ tptp.cons_nat_o @t363) @t521))) % 3.70/3.99 (define @t525 () (@var "Ys" tptp.list_nat)) % 3.70/3.99 (define @t526 () (_ tptp.ord_lexordp_eq_nat @t210)) % 3.70/3.99 (define @t527 () (_ @t526 @t525)) % 3.70/3.99 (define @t528 () (_ (_ tptp.ord_lexordp_eq_nat @t211) (_ (_ tptp.cons_nat @t215) @t525))) % 3.70/3.99 (define @t529 () (@list @t359 @t358 @t518 @t517)) % 3.70/3.99 (define @t530 () (@list @t364 @t363 @t522 @t521)) % 3.70/3.99 (define @t531 () (@list @t155 @t215 @t210 @t525)) % 3.70/3.99 (define @t532 () (_ tptp.ord_lexordp_eq_nat @t525)) % 3.70/3.99 (define @t533 () (_ @t532 @t210)) % 3.70/3.99 (define @t534 () (@list @t210 @t525)) % 3.70/3.99 (define @t535 () (@var "Zs" tptp.list_nat)) % 3.70/3.99 (define @t536 () (@var "Ys2" tptp.list_set_nat)) % 3.70/3.99 (define @t537 () (@var "Xs2" tptp.list_set_nat)) % 3.70/3.99 (define @t538 () (not @t276)) % 3.70/3.99 (define @t539 () (@var "A22" tptp.list_set_nat)) % 3.70/3.99 (define @t540 () (= @t539 (_ (_ tptp.cons_set_nat @t274) @t536))) % 3.70/3.99 (define @t541 () (@list @t536)) % 3.70/3.99 (define @t542 () (@var "A1" tptp.list_set_nat)) % 3.70/3.99 (define @t543 () (= @t542 (_ (_ tptp.cons_set_nat @t275) @t537))) % 3.70/3.99 (define @t544 () (@var "Ys2" tptp.list_nat_o)) % 3.70/3.99 (define @t545 () (@var "Xs2" tptp.list_nat_o)) % 3.70/3.99 (define @t546 () (not @t299)) % 3.70/3.99 (define @t547 () (@var "A22" tptp.list_nat_o)) % 3.70/3.99 (define @t548 () (= @t547 (_ (_ tptp.cons_nat_o @t297) @t544))) % 3.70/3.99 (define @t549 () (@list @t544)) % 3.70/3.99 (define @t550 () (@var "A1" tptp.list_nat_o)) % 3.70/3.99 (define @t551 () (= @t550 (_ (_ tptp.cons_nat_o @t298) @t545))) % 3.70/3.99 (define @t552 () (@var "Ys2" tptp.list_nat)) % 3.70/3.99 (define @t553 () (@var "Xs2" tptp.list_nat)) % 3.70/3.99 (define @t554 () (_ (_ tptp.ord_lexordp_eq_nat @t553) @t552)) % 3.70/3.99 (define @t555 () (not (_ (_ tptp.ord_less_nat @t202) @t18))) % 3.70/3.99 (define @t556 () (not @t260)) % 3.70/3.99 (define @t557 () (_ (_ tptp.cons_nat @t202) @t552)) % 3.70/3.99 (define @t558 () (@var "A22" tptp.list_nat)) % 3.70/3.99 (define @t559 () (= @t558 @t557)) % 3.70/3.99 (define @t560 () (@list @t552)) % 3.70/3.99 (define @t561 () (_ (_ tptp.cons_nat @t18) @t553)) % 3.70/3.99 (define @t562 () (@var "A1" tptp.list_nat)) % 3.70/3.99 (define @t563 () (= @t562 @t561)) % 3.70/3.99 (define @t564 () (@var "Ys3" tptp.list_set_nat)) % 3.70/3.99 (define @t565 () (@var "Xs3" tptp.list_set_nat)) % 3.70/3.99 (define @t566 () (@var "X4" tptp.set_nat)) % 3.70/3.99 (define @t567 () (@var "Y6" tptp.set_nat)) % 3.70/3.99 (define @t568 () (_ (_ tptp.ord_less_set_nat @t566) @t567)) % 3.70/3.99 (define @t569 () (@var "A23" tptp.list_set_nat)) % 3.70/3.99 (define @t570 () (= @t569 (_ (_ tptp.cons_set_nat @t567) @t564))) % 3.70/3.99 (define @t571 () (@var "A12" tptp.list_set_nat)) % 3.70/3.99 (define @t572 () (= @t571 (_ (_ tptp.cons_set_nat @t566) @t565))) % 3.70/3.99 (define @t573 () (@list @t566 @t567 @t565 @t564)) % 3.70/3.99 (define @t574 () (@var "Ys3" tptp.list_nat_o)) % 3.70/3.99 (define @t575 () (@var "Xs3" tptp.list_nat_o)) % 3.70/3.99 (define @t576 () (@var "X4" (-> tptp.nat Bool))) % 3.70/3.99 (define @t577 () (@var "Y6" (-> tptp.nat Bool))) % 3.70/3.99 (define @t578 () (_ (_ tptp.ord_less_nat_o @t576) @t577)) % 3.70/3.99 (define @t579 () (@var "A23" tptp.list_nat_o)) % 3.70/3.99 (define @t580 () (= @t579 (_ (_ tptp.cons_nat_o @t577) @t574))) % 3.70/3.99 (define @t581 () (@var "A12" tptp.list_nat_o)) % 3.70/3.99 (define @t582 () (= @t581 (_ (_ tptp.cons_nat_o @t576) @t575))) % 3.70/3.99 (define @t583 () (@list @t576 @t577 @t575 @t574)) % 3.70/3.99 (define @t584 () (@var "Ys3" tptp.list_nat)) % 3.70/3.99 (define @t585 () (@var "Xs3" tptp.list_nat)) % 3.70/3.99 (define @t586 () (@var "Y6" tptp.nat)) % 3.70/3.99 (define @t587 () (_ (_ tptp.ord_less_nat @t134) @t586)) % 3.70/3.99 (define @t588 () (@var "A23" tptp.list_nat)) % 3.70/3.99 (define @t589 () (= @t588 (_ (_ tptp.cons_nat @t586) @t584))) % 3.70/3.99 (define @t590 () (@var "A12" tptp.list_nat)) % 3.70/3.99 (define @t591 () (= @t590 (_ (_ tptp.cons_nat @t134) @t585))) % 3.70/3.99 (define @t592 () (@list @t134 @t586 @t585 @t584)) % 3.70/3.99 (define @t593 () (@var "X2" tptp.list_nat)) % 3.70/3.99 (define @t594 () (@var "X1" tptp.list_nat)) % 3.70/3.99 (define @t595 () (@var "P" (-> tptp.list_nat tptp.list_nat Bool))) % 3.70/3.99 (define @t596 () (_ (_ @t595 @t561) @t557)) % 3.70/3.99 (define @t597 () (@list @t18 @t202 @t553 @t552)) % 3.70/3.99 (define @t598 () (@var "X_1" tptp.list_nat)) % 3.70/3.99 (define @t599 () (@list @t55 @t439)) % 3.70/3.99 (define @t600 () (_ tptp.s2 tptp.n)) % 3.70/3.99 (define @t601 () (_ tptp.s1 tptp.n)) % 3.70/3.99 (define @t602 () (= @t601 @t600)) % 3.70/3.99 (define @t603 () (_ tptp.type_M876316792e_FVar tptp.x)) % 3.70/3.99 (define @t604 () (_ tptp.type_M1050318637scheme @t603)) % 3.70/3.99 (define @t605 () (_ tptp.member_nat tptp.n)) % 3.70/3.99 (define @t606 () (_ @t605 @t604)) % 3.70/3.99 (define @t607 () (not @t606)) % 3.70/3.99 (define @t608 () (_ tptp.type_M1690910139scheme tptp.s2)) % 3.70/3.99 (define @t609 () (_ @t608 @t603)) % 3.70/3.99 (define @t610 () (_ tptp.type_M1690910139scheme tptp.s1)) % 3.70/3.99 (define @t611 () (_ @t610 @t603)) % 3.70/3.99 (define @t612 () (= @t611 @t609)) % 3.70/3.99 (define @t613 () (not @t612)) % 3.70/3.99 (define @t614 () (or @t613 @t607 @t602)) % 3.70/3.99 (define @t615 () (not @t614)) % 3.70/3.99 (define @t616 () (@var "Ts" tptp.list_n396811828le_typ)) % 3.70/3.99 (define @t617 () (_ tptp.member_nat @t395)) % 3.70/3.99 (define @t618 () (lambda (@list @t397 @t616) (forall @t399 (=> (_ @t617 (_ tptp.type_M1691543772le_typ @t616)) @t398)))) % 3.70/3.99 (define @t619 () (@var "Ts" tptp.list_l1334080099scheme)) % 3.70/3.99 (define @t620 () (lambda (@list @t397 @t619) (forall @t399 (=> (_ @t617 (_ tptp.type_M1958029241scheme @t619)) @t398)))) % 3.70/3.99 (define @t621 () (@var "Ts" tptp.list_T1103309005le_typ)) % 3.70/3.99 (define @t622 () (lambda (@list @t397 @t621) (forall @t399 (=> (_ @t617 (_ tptp.type_M510873837le_typ @t621)) @t398)))) % 3.70/3.99 (define @t623 () (@var "Ts" tptp.type_M1694694083scheme)) % 3.70/3.99 (define @t624 () (lambda (@list @t397 @t623) (forall @t399 (=> (_ @t617 (_ tptp.type_M1050318637scheme @t623)) @t398)))) % 3.70/3.99 (define @t625 () (@var "Ts" tptp.type_Mirabelle_typ)) % 3.70/3.99 (define @t626 () (lambda (@list @t397 @t625) (forall @t399 (=> (_ @t617 (_ tptp.type_M49385309le_typ @t625)) @t398)))) % 3.70/3.99 (define @t627 () (@var "Ts" tptp.list_T247403987scheme)) % 3.70/3.99 (define @t628 () (lambda (@list @t397 @t627) (forall @t399 (=> (_ @t617 (_ tptp.type_M141510067scheme @t627)) @t398)))) % 3.70/3.99 (define @t629 () (@var "Ts" (-> tptp.nat tptp.type_Mirabelle_typ))) % 3.70/3.99 (define @t630 () (lambda (@list @t397 @t629) (forall @t399 (=> (_ @t617 (_ tptp.type_M1715972684le_typ @t629)) @t398)))) % 3.70/3.99 (define @t631 () (lambda (@list @t471 @t468) (_ tptp.collect_nat (lambda @t136 (or @t472 @t503))))) % 3.70/3.99 (define @t632 () (lambda @t136 tptp.bot_bot_o)) % 3.70/3.99 (define @t633 () (lambda @t424 (= @t423 (_ (_ tptp.insert_nat (_ tptp.the_elem_nat @t423)) tptp.bot_bot_set_nat)))) % 3.70/3.99 (define @t634 () (lambda @t424 (= @t423 tptp.bot_bot_set_nat))) % 3.70/3.99 (define @t635 () (@var "X6" tptp.set_nat)) % 3.70/3.99 (define @t636 () (lambda (@list @t635) (_ tptp.the_nat (lambda @t136 (= @t635 @t422))))) % 3.70/3.99 (define @t637 () (@var "S4" (-> tptp.nat tptp.type_Mirabelle_typ))) % 3.70/3.99 (define @t638 () (@list @t637)) % 3.70/3.99 (define @t639 () (lambda @t638 (_ tptp.collect_nat (lambda @t400 (not (= (_ @t637 @t397) (_ tptp.type_Mirabelle_TVar @t397))))))) % 3.70/3.99 (define @t640 () (lambda @t469 (_ (_ tptp.ord_less_nat_o @t506) @t504))) % 3.70/3.99 (define @t641 () (@var "Z3" tptp.nat)) % 3.70/3.99 (define @t642 () (@var "P3" Bool)) % 3.70/3.99 (define @t643 () (lambda (@list @t642 @t134 @t586) (_ tptp.the_nat (lambda (@list @t641) (and (=> @t642 (= @t641 @t134)) (=> (not @t642) (= @t641 @t586))))))) % 3.70/3.99 (define @t644 () (lambda @t638 (_ (_ tptp.sup_sup_set_nat (_ tptp.type_Mirabelle_dom @t637)) (_ tptp.type_Mirabelle_cod @t637)))) % 3.70/3.99 (define @t645 () (lambda @t469 (_ tptp.collect_nat (lambda @t136 (or @t505 @t503))))) % 3.70/3.99 (define @t646 () (@var "B6" (-> tptp.nat Bool))) % 3.70/3.99 (define @t647 () (@var "A3" (-> tptp.nat Bool))) % 3.70/3.99 (define @t648 () (lambda (@list @t646 @t647) (and (= @t647 (_ (_ tptp.sup_sup_nat_o @t647) @t646)) (not (= @t647 @t646))))) % 3.70/3.99 (define @t649 () (@var "B6" tptp.nat)) % 3.70/3.99 (define @t650 () (lambda (@list @t649 @t471) (and (= @t471 (_ (_ tptp.sup_sup_nat @t471) @t649)) (not (= @t471 @t649))))) % 3.70/3.99 (define @t651 () (_ @t7 @t22)) % 3.70/3.99 (define @t652 () (_ @t8 @t22)) % 3.70/3.99 (define @t653 () (tptp.type_M49385309le_typ @t68)) % 3.70/3.99 (define @t654 () (tptp.member_nat @t22 @t653)) % 3.70/3.99 (define @t655 () (not @t111)) % 3.70/3.99 (define @t656 () (tptp.type_M784671311le_typ @t7 @t68)) % 3.70/3.99 (define @t657 () (tptp.type_M784671311le_typ @t8 @t68)) % 3.70/3.99 (define @t658 () (not @t106)) % 3.70/3.99 (define @t659 () (or @t658 @t655 @t109)) % 3.70/3.99 (define @t660 () (tptp.s1 tptp.n)) % 3.70/3.99 (define @t661 () (tptp.s2 tptp.n)) % 3.70/3.99 (define @t662 () (= @t661 @t660)) % 3.70/3.99 (define @t663 () (tptp.type_Mirabelle_TVar tptp.x)) % 3.70/3.99 (define @t664 () (tptp.member_nat tptp.n (tptp.type_M49385309le_typ @t663))) % 3.70/3.99 (define @t665 () (not @t664)) % 3.70/3.99 (define @t666 () (tptp.type_M784671311le_typ tptp.s2 @t663)) % 3.70/3.99 (define @t667 () (tptp.type_M784671311le_typ tptp.s1 @t663)) % 3.70/3.99 (define @t668 () (not (= @t666 @t667))) % 3.70/3.99 (define @t669 () (or @t668 @t665 @t662)) % 3.70/3.99 (define @t670 () (forall @t113 (or (not (= @t657 @t656)) (not @t654) (= @t652 @t651)))) % 3.70/3.99 (define @t671 () (not (= @t667 @t666))) % 3.70/3.99 (define @t672 () (or @t671 @t665 @t662)) % 3.70/3.99 (define @t673 () (tptp.type_M876316792e_FVar tptp.x)) % 3.70/3.99 (define @t674 () (tptp.type_M1050318637scheme @t673)) % 3.70/3.99 (define @t675 () (tptp.member_nat tptp.n @t674)) % 3.70/3.99 (define @t676 () (tptp.type_M1690910139scheme tptp.s1 @t673)) % 3.70/3.99 (define @t677 () (tptp.type_M1690910139scheme tptp.s2 @t673)) % 3.70/3.99 (define @t678 () (tptp.type_Mirabelle_TVar @t22)) % 3.70/3.99 (define @t679 () (tptp.type_M1006385707scheme @t678)) % 3.70/3.99 (define @t680 () (tptp.type_M876316792e_FVar @t22)) % 3.70/3.99 (define @t681 () (= @t25 @t420)) % 3.70/3.99 (define @t682 () (tptp.type_M1006385707scheme @t68)) % 3.70/3.99 (define @t683 () (tptp.type_M1050318637scheme @t682)) % 3.70/3.99 (define @t684 () (tptp.type_M784671311le_typ @t15 @t678)) % 3.70/3.99 (define @t685 () (_ @t15 @t22)) % 3.70/3.99 (define @t686 () (= @t23 @t255)) % 3.70/3.99 (define @t687 () (@list tptp.s2 tptp.x)) % 3.70/3.99 (define @t688 () (tptp.type_M1006385707scheme @t115)) % 3.70/3.99 (define @t689 () (not @t118)) % 3.70/3.99 (define @t690 () (or @t689 @t116)) % 3.70/3.99 (define @t691 () (tptp.s2 tptp.x)) % 3.70/3.99 (define @t692 () (tptp.s1 tptp.x)) % 3.70/3.99 (define @t693 () (tptp.type_M1006385707scheme @t685)) % 3.70/3.99 (define @t694 () (tptp.type_M1690910139scheme @t15 @t680)) % 3.70/3.99 (define @t695 () (@list tptp.s1 tptp.x)) % 3.70/3.99 (define @t696 () (= @t692 @t691)) % 3.70/3.99 (define @t697 () (= (tptp.type_M1006385707scheme @t692) (tptp.type_M1006385707scheme @t691))) % 3.70/3.99 (define @t698 () (not @t697)) % 3.70/3.99 (define @t699 () (or @t698 @t696)) % 3.70/3.99 (assume @p1 (forall @t5 (= (= @t4 (_ tptp.type_M876316792e_FVar @t1)) @t3))) % 3.70/3.99 (assume @p2 (forall (@list @t6 @t8 @t7) (=> (forall @t13 (=> (_ @t12 @t11) @t10)) (= (_ (_ tptp.type_M1690910139scheme @t8) @t6) (_ (_ tptp.type_M1690910139scheme @t7) @t6))))) % 3.70/3.99 (assume @p3 (forall (@list @t6 @t15 @t14) (=> (forall @t21 (=> (_ @t20 @t11) @t19)) (= @t17 (_ (_ tptp.type_M1690910139scheme @t14) @t6))))) % 3.70/3.99 (assume @p4 @t29) % 3.70/3.99 (assume @p5 (forall @t28 (= (_ @t16 @t30) @t30))) % 3.70/3.99 (assume @p6 (forall (@list @t15 @t32 @t31) (= (_ @t16 @t33) (_ (_ tptp.type_M155660035e_SFun (_ @t16 @t32)) (_ @t16 @t31))))) % 3.70/3.99 (assume @p7 (forall (@list @t2 @t34) (not (= @t4 @t35)))) % 3.70/3.99 (assume @p8 (forall (@list @t2 @t37 @t36) (not (= @t4 @t38)))) % 3.70/3.99 (assume @p9 (forall (@list @t15 @t41 @t39) (= (_ @t40 @t43) (_ (_ tptp.cons_n499085924le_typ (_ (_ tptp.type_M1158474302le_typ @t15) @t41)) (_ @t40 @t39))))) % 3.70/3.99 (assume @p10 (forall (@list @t15 @t46 @t44) (= (_ @t45 @t48) (_ (_ tptp.cons_l531914285scheme (_ @t47 @t46)) (_ @t45 @t44))))) % 3.70/3.99 (assume @p11 (forall (@list @t15 @t51 @t49) (= (_ @t50 @t53) (_ (_ tptp.cons_l392684675le_typ (_ @t52 @t51)) (_ @t50 @t49))))) % 3.70/3.99 (assume @p12 (forall (@list @t15 @t55 @t54) (= (_ @t52 @t58) (_ (_ tptp.cons_T363929085le_typ (_ @t56 @t55)) (_ @t52 @t54))))) % 3.70/3.99 (assume @p13 (forall (@list @t15 @t60 @t59) (= (_ @t47 @t63) (_ (_ tptp.cons_l1910959773scheme (_ @t61 @t60)) (_ @t47 @t59))))) % 3.70/3.99 (assume @p14 (forall (@list @t15 @t65 @t64) (= (_ @t61 @t67) (_ (_ tptp.cons_T633159821scheme (_ @t16 @t65)) (_ @t61 @t64))))) % 3.70/3.99 (assume @p15 @t73) % 3.70/3.99 (assume @p16 (forall @t77 (= (_ tptp.type_M1050318637scheme @t76) @t75))) % 3.70/3.99 (assume @p17 (forall (@list @t22 @t6 @t15 @t14) (=> (_ @t80 @t6) (= (_ (_ tptp.type_M1690910139scheme @t79) @t6) @t17)))) % 3.70/3.99 (assume @p18 (forall (@list @t37 @t36 @t82 @t81) (= (= @t38 (_ (_ tptp.type_M155660035e_SFun @t82) @t81)) (and (= @t37 @t82) (= @t36 @t81))))) % 3.70/3.99 (assume @p19 (forall (@list @t34 @t83) (= (= @t35 (_ tptp.type_M2048935292e_BVar @t83)) (= @t34 @t83)))) % 3.70/3.99 (assume @p20 (forall (@list @t22 @t86 @t84) (= (_ @t85 @t88) (and (_ @t87 @t86) (_ @t85 @t84))))) % 3.70/3.99 (assume @p21 (forall (@list @t22 @t51 @t49) (= (_ @t89 @t53) (and (_ @t90 @t51) (_ @t89 @t49))))) % 3.70/3.99 (assume @p22 (forall (@list @t22 @t46 @t44) (= (_ @t91 @t48) (and (_ @t92 @t46) (_ @t91 @t44))))) % 3.70/3.99 (assume @p23 (forall (@list @t22 @t60 @t59) (= (_ @t92 @t63) (and (_ @t93 @t60) (_ @t92 @t59))))) % 3.70/3.99 (assume @p24 (forall (@list @t22 @t55 @t54) (= (_ @t90 @t58) (and (_ @t94 @t55) (_ @t90 @t54))))) % 3.70/3.99 (assume @p25 (forall (@list @t22 @t41 @t39) (= (_ @t87 @t43) (and (_ @t95 @t41) (_ @t87 @t39))))) % 3.70/3.99 (assume @p26 (forall (@list @t22 @t65 @t64) (= (_ @t93 @t67) (and (_ @t80 @t65) (_ @t93 @t64))))) % 3.70/3.99 (assume @p27 (forall (@list @t15 @t68) (= (_ @t16 @t70) (_ tptp.type_M1006385707scheme @t96)))) % 3.70/3.99 (assume @p28 (forall (@list @t22 @t98 @t97) (= (_ @t80 (_ (_ tptp.type_M155660035e_SFun @t98) @t97)) (and (_ @t80 @t98) (_ @t80 @t97))))) % 3.70/3.99 (assume @p29 (forall @t100 (_ @t80 @t99))) % 3.70/3.99 (assume @p30 (forall @t100 (= (_ @t80 @t76) @t101))) % 3.70/3.99 (assume @p31 (forall (@list @t34 @t37 @t36) (not (= @t35 @t38)))) % 3.70/3.99 (assume @p32 (forall (@list @t68 @t32 @t31) (=> (= @t70 @t33) (exists (@list @t103 @t102) (and (= @t32 (_ tptp.type_M1006385707scheme @t103)) (= @t31 (_ tptp.type_M1006385707scheme @t102))))))) % 3.70/3.99 (assume @p33 (forall (@list @t68 @t8 @t7) (=> (forall @t13 (=> (_ @t12 @t69) @t10)) @t106))) % 3.70/3.99 (assume @p34 @t114) % 3.70/3.99 (assume @p35 (forall (@list @t68 @t15 @t14) (=> (forall @t21 (=> (_ @t20 @t69) @t19)) (= @t96 (_ (_ tptp.type_M784671311le_typ @t14) @t68))))) % 3.70/3.99 (assume @p36 @t120) % 3.70/3.99 (assume @p37 (forall @t77 (= (_ tptp.type_M1050318637scheme @t99) tptp.bot_bot_set_nat))) % 3.70/3.99 (assume @p38 (forall (@list @t123) (=> (forall @t126 (not (= @t123 (_ tptp.type_M876316792e_FVar @t125)))) (=> (forall (@list @t124) (not (= @t123 (_ tptp.type_M2048935292e_BVar @t124)))) (not (forall (@list @t122 @t121) (not (= @t123 (_ (_ tptp.type_M155660035e_SFun @t122) @t121))))))))) % 3.70/3.99 (assume @p39 (forall (@list @t128 @t127) (=> (forall @t21 (_ @t128 (_ tptp.type_M876316792e_FVar @t18))) (=> (forall @t21 (_ @t128 (_ tptp.type_M2048935292e_BVar @t18))) (=> (forall (@list @t130 @t129) (=> (_ @t128 @t130) (=> (_ @t128 @t129) (_ @t128 (_ (_ tptp.type_M155660035e_SFun @t130) @t129))))) (_ @t128 @t127)))))) % 3.70/3.99 (assume @p40 (forall @t138 (= (_ tptp.collect_nat @t137) @t133))) % 3.70/3.99 (assume @p41 (forall @t138 (= (_ tptp.collect_nat (_ @t141 @t131)) @t133))) % 3.70/3.99 (assume @p42 (forall @t138 (_ @t142 @t133))) % 3.70/3.99 (assume @p43 (forall @t150 (=> (=> (not @t149) @t148) @t147))) % 3.70/3.99 (assume @p44 (forall @t154 (= @t153 (or @t148 @t152)))) % 3.70/3.99 (assume @p45 (forall @t158 (= (_ @t156 @t157) @t157))) % 3.70/3.99 (assume @p46 (forall (@list @t162 @t160 @t161 @t159) (= (= (_ (_ tptp.cons_T633159821scheme @t162) @t160) (_ (_ tptp.cons_T633159821scheme @t161) @t159)) (and (= @t162 @t161) (= @t160 @t159))))) % 3.70/3.99 (assume @p47 (forall (@list @t166 @t164 @t165 @t163) (= (= (_ (_ tptp.cons_l1910959773scheme @t166) @t164) (_ (_ tptp.cons_l1910959773scheme @t165) @t163)) (and (= @t166 @t165) (= @t164 @t163))))) % 3.70/3.99 (assume @p48 (forall (@list @t170 @t168 @t169 @t167) (= (= (_ (_ tptp.cons_T363929085le_typ @t170) @t168) (_ (_ tptp.cons_T363929085le_typ @t169) @t167)) (and @t171 (= @t168 @t167))))) % 3.70/3.99 (assume @p49 (forall (@list @t175 @t173 @t174 @t172) (= (= (_ (_ tptp.cons_n499085924le_typ @t175) @t173) (_ (_ tptp.cons_n499085924le_typ @t174) @t172)) (and (= @t175 @t174) (= @t173 @t172))))) % 3.70/3.99 (assume @p50 (forall (@list @t179 @t177 @t178 @t176) (= (= (_ (_ tptp.cons_nat @t179) @t177) (_ (_ tptp.cons_nat @t178) @t176)) (and (= @t179 @t178) (= @t177 @t176))))) % 3.70/3.99 (assume @p51 (forall (@list @t180) (not (_ @t181 tptp.bot_bot_set_nat)))) % 3.70/3.99 (assume @p52 (forall @t185 (= (_ @t142 @t184) @t183))) % 3.70/3.99 (assume @p53 (forall @t188 (= (_ tptp.collect_nat (lambda @t136 @t187)) @t151))) % 3.70/3.99 (assume @p54 (forall @t193 (=> (forall @t21 (= @t192 @t191)) (= @t184 @t190)))) % 3.70/3.99 (assume @p55 (forall @t188 (= (forall @t136 (not @t187)) @t194))) % 3.70/3.99 (assume @p56 (forall @t198 (= @t197 @t196))) % 3.70/3.99 (assume @p57 (forall @t198 (= (= tptp.bot_bot_set_nat @t184) @t196))) % 3.70/3.99 (assume @p58 (forall (@list @t22 @t199 @t15 @t14) (=> (_ @t93 @t199) (= (_ (_ tptp.type_M1944210753scheme @t79) @t199) @t200)))) % 3.70/3.99 (assume @p59 (forall @t188 (= (exists @t136 @t187) @t201))) % 3.70/3.99 (assume @p60 (forall @t188 (=> (forall @t204 (not @t203)) @t194))) % 3.70/3.99 (assume @p61 (forall (@list @t151 @t131) (=> @t194 @t205))) % 3.70/3.99 (assume @p62 (forall @t138 (not (_ @t142 tptp.bot_bot_set_nat)))) % 3.70/3.99 (assume @p63 (forall (@list @t65 @t206) (not (= (_ @t66 @t206) @t206)))) % 3.70/3.99 (assume @p64 (forall (@list @t60 @t207) (not (= (_ @t62 @t207) @t207)))) % 3.70/3.99 (assume @p65 (forall (@list @t55 @t208) (not (= (_ @t57 @t208) @t208)))) % 3.70/3.99 (assume @p66 (forall (@list @t41 @t209) (not (= (_ @t42 @t209) @t209)))) % 3.70/3.99 (assume @p67 (forall (@list @t155 @t210) (not (= @t211 @t210)))) % 3.70/3.99 (assume @p68 (forall @t214 (=> @t152 (exists @t213 (and (= @t151 (_ @t132 @t212)) (not (_ @t142 @t212))))))) % 3.70/3.99 (assume @p69 (forall (@list @t155 @t215 @t151) (= (_ @t156 (_ @t216 @t151)) (_ @t216 @t157)))) % 3.70/3.99 (assume @p70 (forall (@list @t131 @t151 @t144 @t143) (=> @t205 (=> (not (_ @t218 @t143)) (= (= @t221 @t146) (and (=> @t148 @t220) (=> @t219 (exists (@list @t217) (and (= @t151 (_ @t145 @t217)) (not (_ @t218 @t217)) (= @t143 (_ @t132 @t217)) (not (_ @t142 @t217))))))))))) % 3.70/3.99 (assume @p71 (forall @t214 (=> @t152 (= @t221 @t151)))) % 3.70/3.99 (assume @p72 (forall @t224 (=> (not @t223) (=> (not (_ @t222 @t143)) (= (= @t157 (_ @t156 @t143)) @t220))))) % 3.70/3.99 (assume @p73 (forall @t158 (=> @t223 (not (forall @t213 (=> (= @t151 (_ @t156 @t212)) (_ @t222 @t212))))))) % 3.70/3.99 (assume @p74 (forall @t150 (=> @t149 @t147))) % 3.70/3.99 (assume @p75 (forall (@list @t131 @t143) (_ @t142 @t225))) % 3.70/3.99 (assume @p76 (forall @t154 (=> @t153 (=> @t219 @t152)))) % 3.70/3.99 (assume @p77 (= tptp.bot_bot_set_nat (_ tptp.collect_nat (lambda @t136 false)))) % 3.70/3.99 (assume @p78 (forall @t185 (= (_ @t132 @t184) (_ tptp.collect_nat (lambda (@list @t226) (=> (not (= @t226 @t131)) (_ @t182 @t226))))))) % 3.70/3.99 (assume @p79 (forall @t228 (=> (= @t133 @t227) @t148))) % 3.70/3.99 (assume @p80 (forall @t214 (not (= @t221 tptp.bot_bot_set_nat)))) % 3.70/3.99 (assume @p81 (forall (@list @t131 @t144 @t180 @t230) (= (= (_ @t132 @t227) (_ (_ tptp.insert_nat @t180) (_ (_ tptp.insert_nat @t230) tptp.bot_bot_set_nat))) (or (and (= @t131 @t180) (= @t144 @t230)) (and (= @t131 @t230) @t229))))) % 3.70/3.99 (assume @p82 (forall @t233 (= @t232 @t231))) % 3.70/3.99 (assume @p83 (forall @t233 (=> @t232 @t231))) % 3.70/3.99 (assume @p84 (forall @t236 (and (=> @t183 (= @t234 @t133)) (=> @t235 (= @t234 tptp.bot_bot_set_nat))))) % 3.70/3.99 (assume @p85 (forall @t236 (and (=> @t183 (= @t237 @t133)) (=> @t235 (= @t237 tptp.bot_bot_set_nat))))) % 3.70/3.99 (assume @p86 (forall @t239 (= (_ tptp.the_elem_nat @t238) @t155))) % 3.70/3.99 (assume @p87 (forall @t77 (= (_ tptp.type_M326705277scheme @t99) @t75))) % 3.70/3.99 (assume @p88 (forall @t239 (_ tptp.is_singleton_nat @t238))) % 3.70/3.99 (assume @p89 (forall @t242 (= (not @t241) (_ (_ tptp.ord_less_nat_o tptp.bot_bot_nat_o) @t240)))) % 3.70/3.99 (assume @p90 (forall @t245 (= (not @t244) (_ (_ tptp.ord_less_set_nat tptp.bot_bot_set_nat) @t243)))) % 3.70/3.99 (assume @p91 (forall @t138 (= (not (= @t131 tptp.bot_bot_nat)) (_ (_ tptp.ord_less_nat tptp.bot_bot_nat) @t131)))) % 3.70/3.99 (assume @p92 (forall @t242 (not (_ @t246 tptp.bot_bot_nat_o)))) % 3.70/3.99 (assume @p93 (forall @t245 (not (_ @t247 tptp.bot_bot_set_nat)))) % 3.70/3.99 (assume @p94 (forall @t138 (not (_ @t248 tptp.bot_bot_nat)))) % 3.70/3.99 (assume @p95 (forall @t77 (= (_ tptp.type_M49385309le_typ @t249) @t75))) % 3.70/3.99 (assume @p96 (forall @t77 (= (_ tptp.type_M326705277scheme @t76) tptp.bot_bot_set_nat))) % 3.70/3.99 (assume @p97 (forall @t5 (= (= @t250 (_ tptp.type_Mirabelle_TVar @t1)) @t3))) % 3.70/3.99 (assume @p98 (forall @t100 (= (_ @t94 @t249) @t101))) % 3.70/3.99 (assume @p99 (forall @t251 (_ @t95 tptp.type_Mirabelle_TVar))) % 3.70/3.99 (assume @p100 (forall (@list @t199 @t8 @t7) (=> (forall @t13 (=> (_ @t12 @t252) @t10)) (= (_ (_ tptp.type_M1944210753scheme @t8) @t199) (_ (_ tptp.type_M1944210753scheme @t7) @t199))))) % 3.70/3.99 (assume @p101 (forall (@list @t199 @t15 @t14) (=> (forall @t21 (=> (_ @t20 @t252) @t19)) (= @t200 (_ (_ tptp.type_M1944210753scheme @t14) @t199))))) % 3.70/3.99 (assume @p102 (= tptp.bot_bot_set_nat (_ tptp.collect_nat tptp.bot_bot_nat_o))) % 3.70/3.99 (assume @p103 (forall @t188 (not (_ @t253 tptp.bot_bot_set_nat)))) % 3.70/3.99 (assume @p104 @t256) % 3.70/3.99 (assume @p105 (forall @t188 (=> @t201 (=> (forall @t258 (=> (_ @t20 @t151) (=> @t203 (= @t18 @t202)))) @t257)))) % 3.70/3.99 (assume @p106 (forall @t266 (=> (= @t243 @t265) @t264))) % 3.70/3.99 (assume @p107 (forall @t271 (=> (= @t240 @t270) @t269))) % 3.70/3.99 (assume @p108 (forall @t284 (=> (= @t131 @t283) @t282))) % 3.70/3.99 (assume @p109 (forall @t289 (=> (= @t243 @t288) @t287))) % 3.70/3.99 (assume @p110 (forall @t294 (=> (= @t240 @t293) @t292))) % 3.70/3.99 (assume @p111 (forall @t307 (=> (= @t131 @t306) @t305))) % 3.70/3.99 (assume @p112 (forall @t312 (=> (= @t243 @t311) @t310))) % 3.70/3.99 (assume @p113 (forall @t317 (=> (= @t240 @t316) @t315))) % 3.70/3.99 (assume @p114 (forall @t322 (=> (= @t131 @t321) @t320))) % 3.70/3.99 (assume @p115 (forall @t325 (=> @t324 (=> (= @t265 @t272) @t323)))) % 3.70/3.99 (assume @p116 (forall @t327 (=> @t324 (=> (= @t270 @t295) @t326)))) % 3.70/3.99 (assume @p117 (forall @t330 (=> @t329 (=> (= @t283 @t180) @t328)))) % 3.70/3.99 (assume @p118 (forall @t332 (=> @t329 (=> (= @t288 @t272) @t331)))) % 3.70/3.99 (assume @p119 (forall @t334 (=> @t329 (=> (= @t293 @t295) @t333)))) % 3.70/3.99 (assume @p120 (forall @t337 (=> @t336 (=> (= @t306 @t180) @t335)))) % 3.70/3.99 (assume @p121 (forall @t339 (=> @t336 (=> (= @t311 @t272) @t338)))) % 3.70/3.99 (assume @p122 (forall @t341 (=> @t336 (=> (= @t316 @t295) @t340)))) % 3.70/3.99 (assume @p123 (forall @t343 (=> @t324 (=> (= @t321 @t180) @t342)))) % 3.70/3.99 (assume @p124 (forall @t284 (=> (_ @t248 @t283) @t282))) % 3.70/3.99 (assume @p125 (forall @t307 (=> (_ @t248 @t306) @t305))) % 3.70/3.99 (assume @p126 (forall @t266 (=> (_ @t247 @t265) @t264))) % 3.70/3.99 (assume @p127 (forall @t289 (=> (_ @t247 @t288) @t287))) % 3.70/3.99 (assume @p128 (forall @t312 (=> (_ @t247 @t311) @t310))) % 3.70/3.99 (assume @p129 (forall @t271 (=> (_ @t246 @t270) @t269))) % 3.70/3.99 (assume @p130 (forall @t294 (=> (_ @t246 @t293) @t292))) % 3.70/3.99 (assume @p131 (forall @t317 (=> (_ @t246 @t316) @t315))) % 3.70/3.99 (assume @p132 (forall @t322 (=> (_ @t248 @t321) @t320))) % 3.70/3.99 (assume @p133 (forall @t325 (=> @t324 (=> (_ (_ tptp.ord_less_set_nat @t265) @t272) @t323)))) % 3.70/3.99 (assume @p134 (forall @t327 (=> @t324 (=> (_ (_ tptp.ord_less_nat_o @t270) @t295) @t326)))) % 3.70/3.99 (assume @p135 (forall @t330 (=> @t329 (=> (_ (_ tptp.ord_less_nat @t283) @t180) @t328)))) % 3.70/3.99 (assume @p136 (forall @t332 (=> @t329 (=> (_ (_ tptp.ord_less_set_nat @t288) @t272) @t331)))) % 3.70/3.99 (assume @p137 (forall @t334 (=> @t329 (=> (_ (_ tptp.ord_less_nat_o @t293) @t295) @t333)))) % 3.70/3.99 (assume @p138 (forall @t337 (=> @t336 (=> (_ (_ tptp.ord_less_nat @t306) @t180) @t335)))) % 3.70/3.99 (assume @p139 (forall @t339 (=> @t336 (=> (_ (_ tptp.ord_less_set_nat @t311) @t272) @t338)))) % 3.70/3.99 (assume @p140 (forall @t341 (=> @t336 (=> (_ (_ tptp.ord_less_nat_o @t316) @t295) @t340)))) % 3.70/3.99 (assume @p141 (forall @t343 (=> @t324 (=> (_ (_ tptp.ord_less_nat @t321) @t180) @t342)))) % 3.70/3.99 (assume @p142 (forall @t239 (exists (@list @t344) (_ @t345 @t344)))) % 3.70/3.99 (assume @p143 (forall @t352 (=> @t351 (=> @t349 @t347)))) % 3.70/3.99 (assume @p144 (forall @t352 (= @t351 (or @t348 @t347)))) % 3.70/3.99 (assume @p145 (forall @t354 (=> @t329 (not @t353)))) % 3.70/3.99 (assume @p146 (forall @t356 (=> @t336 (not @t355)))) % 3.70/3.99 (assume @p147 (forall @t228 (=> @t324 (not @t357)))) % 3.70/3.99 (assume @p148 (forall @t362 (=> @t361 (not (= @t359 @t358))))) % 3.70/3.99 (assume @p149 (forall @t367 (=> @t366 (not (= @t364 @t363))))) % 3.70/3.99 (assume @p150 (forall @t352 (=> @t348 @t351))) % 3.70/3.99 (assume @p151 (forall @t362 (=> @t361 @t370))) % 3.70/3.99 (assume @p152 (forall @t367 (=> @t366 @t373))) % 3.70/3.99 (assume @p153 (forall @t352 (=> @t348 @t374))) % 3.70/3.99 (assume @p154 (forall (@list @t359 @t358 @t375) (=> @t361 (=> (_ @t368 @t375) (_ @t360 @t375))))) % 3.70/3.99 (assume @p155 (forall (@list @t364 @t363 @t376) (=> @t366 (=> (_ @t371 @t376) (_ @t365 @t376))))) % 3.70/3.99 (assume @p156 (forall (@list @t155 @t215 @t377) (=> @t348 (=> (_ @t346 @t377) (_ @t345 @t377))))) % 3.70/3.99 (assume @p157 (forall @t352 (or @t348 @t350 @t347))) % 3.70/3.99 (assume @p158 (forall @t378 (not (_ @t360 @t359)))) % 3.70/3.99 (assume @p159 (forall @t379 (not (_ @t365 @t364)))) % 3.70/3.99 (assume @p160 (forall @t239 (not (_ @t345 @t155)))) % 3.70/3.99 (assume @p161 (forall @t383 (=> @t382 @t381))) % 3.70/3.99 (assume @p162 (forall @t387 (=> @t386 @t385))) % 3.70/3.99 (assume @p163 (forall @t390 (=> @t148 @t389))) % 3.70/3.99 (assume @p164 (forall @t383 (=> @t329 (=> (= @t279 @t272) @t380)))) % 3.70/3.99 (assume @p165 (forall @t387 (=> @t336 (=> (= @t302 @t295) @t384)))) % 3.70/3.99 (assume @p166 (forall @t390 (=> @t324 (=> @t229 @t388)))) % 3.70/3.99 (assume @p167 (forall @t391 (=> @t353 (not @t329)))) % 3.70/3.99 (assume @p168 (forall @t392 (=> @t355 (not @t336)))) % 3.70/3.99 (assume @p169 (forall @t233 (=> @t357 (not @t324)))) % 3.70/3.99 (assume @p170 (forall @t236 (=> (forall @t21 (=> (forall (@list @t393) (=> (_ (_ tptp.ord_less_nat @t393) @t18) (_ @t182 @t393))) @t192)) @t183))) % 3.70/3.99 (assume @p171 (forall (@list @t215 @t155) (=> @t374 (= @t349 @t350)))) % 3.70/3.99 (assume @p172 (forall @t362 (=> @t361 (not (= @t358 @t359))))) % 3.70/3.99 (assume @p173 (forall @t367 (=> @t366 (not (= @t363 @t364))))) % 3.70/3.99 (assume @p174 (forall @t352 (=> @t348 (not (= @t215 @t155))))) % 3.70/3.99 (assume @p175 (forall (@list @t359 @t358 @t394) (=> @t361 (=> @t369 @t394)))) % 3.70/3.99 (assume @p176 (forall (@list @t364 @t363 @t394) (=> @t366 (=> @t372 @t394)))) % 3.70/3.99 (assume @p177 (forall (@list @t155 @t215 @t394) (=> @t348 (=> @t347 @t394)))) % 3.70/3.99 (assume @p178 (forall @t352 (=> @t349 (=> @t351 @t347)))) % 3.70/3.99 (assume @p179 (forall @t245 (not (_ @t247 @t243)))) % 3.70/3.99 (assume @p180 (forall @t242 (not (_ @t246 @t240)))) % 3.70/3.99 (assume @p181 (forall @t138 (not (_ @t248 @t131)))) % 3.70/3.99 (assume @p182 (forall @t383 (=> @t329 @t381))) % 3.70/3.99 (assume @p183 (forall @t387 (=> @t336 @t385))) % 3.70/3.99 (assume @p184 (forall @t390 (=> @t324 @t389))) % 3.70/3.99 (assume @p185 (= (lambda (@list @t402) (exists (@list @t401) (_ @t402 @t401))) (lambda (@list @t396) (exists @t400 (and (_ @t396 @t397) (forall @t399 (=> @t398 (not (_ @t396 @t395))))))))) % 3.70/3.99 (assume @p186 (forall (@list @t403 @t131 @t144) (=> (forall @t408 (=> (_ (_ tptp.ord_less_nat @t405) @t404) @t407)) (=> (forall (@list @t405) (_ @t406 @t405)) (=> (forall @t408 (=> (_ (_ @t403 @t404) @t405) @t407)) (_ (_ @t403 @t131) @t144)))))) % 3.70/3.99 (assume @p187 (forall (@list @t279 @t243 @t272) (=> @t353 (=> @t411 @t410)))) % 3.70/3.99 (assume @p188 (forall (@list @t302 @t240 @t295) (=> @t355 (=> @t414 @t413)))) % 3.70/3.99 (assume @p189 (forall (@list @t144 @t131 @t180) (=> @t357 (=> @t417 @t416)))) % 3.70/3.99 (assume @p190 (forall @t352 (= @t349 (or @t347 @t350)))) % 3.70/3.99 (assume @p191 (forall @t354 (=> @t329 @t418))) % 3.70/3.99 (assume @p192 (forall @t356 (=> @t336 @t419))) % 3.70/3.99 (assume @p193 (forall @t228 (=> @t324 @t219))) % 3.70/3.99 (assume @p194 (forall @t391 (=> @t353 @t418))) % 3.70/3.99 (assume @p195 (forall @t392 (=> @t355 @t419))) % 3.70/3.99 (assume @p196 (forall @t233 (=> @t357 @t219))) % 3.70/3.99 (assume @p197 @t421) % 3.70/3.99 (assume @p198 (forall @t188 (=> @t257 (not (forall @t21 (not (= @t151 (_ (_ tptp.insert_nat @t18) tptp.bot_bot_set_nat)))))))) % 3.70/3.99 (assume @p199 (= tptp.is_singleton_nat (lambda @t424 (exists @t136 (= @t423 @t422))))) % 3.70/3.99 (assume @p200 (= (_ tptp.type_M1715972684le_typ tptp.type_M405566558_subst) tptp.bot_bot_set_nat)) % 3.70/3.99 (assume @p201 (forall @t428 (= (_ tptp.type_M1006385707scheme @t427) (_ (_ tptp.type_M155660035e_SFun (_ tptp.type_M1006385707scheme @t426)) (_ tptp.type_M1006385707scheme @t425))))) % 3.70/3.99 (assume @p202 (= tptp.type_M405566558_subst tptp.type_Mirabelle_TVar)) % 3.70/3.99 (assume @p203 (forall (@list @t170 @t430 @t169 @t429) (= (= @t431 (_ (_ tptp.type_Mirabelle_Fun @t169) @t429)) (and @t171 (= @t430 @t429))))) % 3.70/3.99 (assume @p204 (forall (@list @t22 @t426 @t425) (= (_ @t94 @t427) (and (_ @t94 @t426) (_ @t94 @t425))))) % 3.70/3.99 (assume @p205 (= (_ tptp.type_Mirabelle_dom tptp.type_M405566558_subst) tptp.bot_bot_set_nat)) % 3.70/3.99 (assume @p206 (forall (@list @t151 @t143 @t180) (=> @t434 (=> @t433 @t432)))) % 3.70/3.99 (assume @p207 (forall @t436 (=> @t434 (=> (_ (_ tptp.ord_less_set_nat @t143) @t435) (_ @t253 @t435))))) % 3.70/3.99 (assume @p208 (forall @t251 (_ @t95 tptp.type_M405566558_subst))) % 3.70/3.99 (assume @p209 (forall (@list @t15 @t426 @t425) (= (_ @t56 @t427) (_ (_ tptp.type_Mirabelle_Fun (_ @t56 @t426)) (_ @t56 @t425))))) % 3.70/3.99 (assume @p210 (forall (@list @t439) (=> (forall @t126 (not (= @t439 (_ tptp.type_Mirabelle_TVar @t125)))) (not (forall (@list @t438 @t437) (not (= @t439 (_ (_ tptp.type_Mirabelle_Fun @t438) @t437)))))))) % 3.70/3.99 (assume @p211 (forall (@list @t441 @t440) (=> (forall @t21 (_ @t441 (_ tptp.type_Mirabelle_TVar @t18))) (=> (forall (@list @t443 @t442) (=> (_ @t441 @t443) (=> (_ @t441 @t442) (_ @t441 (_ (_ tptp.type_Mirabelle_Fun @t443) @t442))))) (_ @t441 @t440))))) % 3.70/3.99 (assume @p212 (forall (@list @t2 @t170 @t430) (not (= @t250 @t431)))) % 3.70/3.99 (assume @p213 (forall @t239 (= (_ tptp.the_nat @t444) @t155))) % 3.70/3.99 (assume @p214 (forall @t138 (= (_ tptp.the_nat @t137) @t131))) % 3.70/3.99 (assume @p215 (forall @t236 (=> @t183 (=> @t447 @t446)))) % 3.70/3.99 (assume @p216 (= (_ tptp.type_Mirabelle_cod tptp.type_M405566558_subst) tptp.bot_bot_set_nat)) % 3.70/3.99 (assume @p217 (forall @t236 (=> @t183 (=> @t447 @t448)))) % 3.70/3.99 (assume @p218 (forall @t198 (=> @t452 @t448))) % 3.70/3.99 (assume @p219 (forall (@list @t182 @t131 @t189) (=> @t183 (=> @t447 @t453)))) % 3.70/3.99 (assume @p220 (forall @t193 (=> @t452 @t453))) % 3.70/3.99 (assume @p221 (forall @t236 (=> @t452 (=> @t183 @t446)))) % 3.70/3.99 (assume @p222 (forall @t198 (= @t197 (= @t182 tptp.bot_bot_nat_o)))) % 3.70/3.99 (assume @p223 (= tptp.bot_bot_nat_o (lambda @t136 (_ @t186 tptp.bot_bot_set_nat)))) % 3.70/3.99 (assume @p224 (forall @t457 (=> (=> (not @t432) @t433) @t456))) % 3.70/3.99 (assume @p225 (forall @t458 (= @t456 (or @t433 @t432)))) % 3.70/3.99 (assume @p226 (forall @t460 (= (= @t455 tptp.bot_bot_set_nat) (and @t194 @t459)))) % 3.70/3.99 (assume @p227 (forall (@list @t131 @t143 @t435) (= (_ (_ tptp.sup_sup_set_nat @t225) @t435) (_ @t132 @t462)))) % 3.70/3.99 (assume @p228 (forall (@list @t151 @t131 @t143) (= (_ @t454 @t225) (_ @t132 @t455)))) % 3.70/3.99 (assume @p229 (forall (@list @t151 @t182 @t463 @t143) (=> (=> (forall @t451 (=> (_ (_ tptp.member_nat @t449) @t151) @t450)) @t463) (=> (forall @t21 (=> (_ @t20 @t455) @t192)) @t463)))) % 3.70/3.99 (assume @p230 (forall @t458 (=> @t456 (=> (not @t433) @t432)))) % 3.70/3.99 (assume @p231 (forall @t458 (=> @t433 @t456))) % 3.70/3.99 (assume @p232 (forall @t457 (=> @t432 @t456))) % 3.70/3.99 (assume @p233 (forall @t466 (= (exists @t136 (and @t465 @t195)) (or (exists @t136 (and @t187 @t195)) (exists @t136 (and @t464 @t195)))))) % 3.70/3.99 (assume @p234 (forall @t466 (= (forall @t136 (=> @t465 @t195)) (and (forall @t136 (=> @t187 @t195)) (forall @t136 (=> @t464 @t195)))))) % 3.70/3.99 (assume @p235 (forall @t436 (= (_ (_ tptp.sup_sup_set_nat @t455) @t435) @t467))) % 3.70/3.99 (assume @p236 (forall @t188 (= (_ @t454 @t151) @t151))) % 3.70/3.99 (assume @p237 (= tptp.sup_sup_set_nat (lambda @t469 (_ (_ tptp.sup_sup_set_nat @t468) @t423)))) % 3.70/3.99 (assume @p238 (forall @t460 (= (_ @t454 @t455) @t455))) % 3.70/3.99 (assume @p239 (forall @t193 (= (_ tptp.collect_nat (lambda @t136 (or @t195 (_ @t189 @t134)))) (_ (_ tptp.sup_sup_set_nat @t184) @t190)))) % 3.70/3.99 (assume @p240 (forall @t436 (= @t467 (_ @t461 (_ @t454 @t435))))) % 3.70/3.99 (assume @p241 (= tptp.insert_nat (lambda @t473 (_ (_ tptp.sup_sup_set_nat (_ tptp.collect_nat (lambda @t136 @t472))) @t470)))) % 3.70/3.99 (assume @p242 (forall (@list @t143) (= (_ @t474 @t143) @t143))) % 3.70/3.99 (assume @p243 (forall @t188 (= (_ @t454 tptp.bot_bot_set_nat) @t151))) % 3.70/3.99 (assume @p244 (forall @t224 (= (= @t238 @t455) @t477))) % 3.70/3.99 (assume @p245 (forall (@list @t151 @t143 @t155) (= (= @t455 @t238) @t477))) % 3.70/3.99 (assume @p246 (= tptp.insert_nat (lambda @t473 (_ (_ tptp.sup_sup_set_nat (_ (_ tptp.insert_nat @t471) tptp.bot_bot_set_nat)) @t470)))) % 3.70/3.99 (assume @p247 (forall @t478 (= (_ tptp.type_M1539052445le_typ @t58) (_ (_ tptp.sup_sup_set_nat (_ tptp.type_M801073677le_typ @t55)) (_ tptp.type_M1539052445le_typ @t54))))) % 3.70/3.99 (assume @p248 (forall @t479 (= (_ tptp.type_M513401740le_typ @t43) (_ (_ tptp.sup_sup_set_nat (_ tptp.type_M772783356le_typ @t41)) (_ tptp.type_M513401740le_typ @t39))))) % 3.70/3.99 (assume @p249 (forall @t480 (= (_ tptp.type_M1496178953scheme @t63) (_ (_ tptp.sup_sup_set_nat (_ tptp.type_M961603331scheme @t60)) (_ tptp.type_M1496178953scheme @t59))))) % 3.70/3.99 (assume @p250 (forall @t481 (= (_ tptp.type_M961603331scheme @t67) (_ (_ tptp.sup_sup_set_nat (_ tptp.type_M326705277scheme @t65)) (_ tptp.type_M961603331scheme @t64))))) % 3.70/3.99 (assume @p251 (forall @t428 (= (_ tptp.type_M49385309le_typ @t427) (_ (_ tptp.sup_sup_set_nat (_ tptp.type_M49385309le_typ @t426)) (_ tptp.type_M49385309le_typ @t425))))) % 3.70/3.99 (assume @p252 (forall @t485 (= (_ tptp.type_M1050318637scheme @t484) (_ (_ tptp.sup_sup_set_nat (_ tptp.type_M1050318637scheme @t483)) (_ tptp.type_M1050318637scheme @t482))))) % 3.70/3.99 (assume @p253 (forall @t485 (= (_ tptp.type_M326705277scheme @t484) (_ (_ tptp.sup_sup_set_nat (_ tptp.type_M326705277scheme @t483)) (_ tptp.type_M326705277scheme @t482))))) % 3.70/3.99 (assume @p254 (forall (@list @t86 @t84) (= (_ tptp.type_M906078444le_typ @t88) (_ (_ tptp.sup_sup_set_nat (_ tptp.type_M1691543772le_typ @t86)) (_ tptp.type_M906078444le_typ @t84))))) % 3.70/3.99 (assume @p255 (forall (@list @t46 @t44) (= (_ tptp.type_M1926053183scheme @t48) (_ (_ tptp.sup_sup_set_nat (_ tptp.type_M1958029241scheme @t46)) (_ tptp.type_M1926053183scheme @t44))))) % 3.70/3.99 (assume @p256 (forall (@list @t51 @t49) (= (_ tptp.type_M1418941437le_typ @t53) (_ (_ tptp.sup_sup_set_nat (_ tptp.type_M510873837le_typ @t51)) (_ tptp.type_M1418941437le_typ @t49))))) % 3.70/3.99 (assume @p257 (forall @t478 (= (_ tptp.type_M510873837le_typ @t58) (_ (_ tptp.sup_sup_set_nat (_ tptp.type_M49385309le_typ @t55)) (_ tptp.type_M510873837le_typ @t54))))) % 3.70/3.99 (assume @p258 (forall @t480 (= (_ tptp.type_M1958029241scheme @t63) (_ (_ tptp.sup_sup_set_nat (_ tptp.type_M141510067scheme @t60)) (_ tptp.type_M1958029241scheme @t59))))) % 3.70/3.99 (assume @p259 (forall @t479 (= (_ tptp.type_M1691543772le_typ @t43) (_ (_ tptp.sup_sup_set_nat (_ tptp.type_M1715972684le_typ @t41)) (_ tptp.type_M1691543772le_typ @t39))))) % 3.70/3.99 (assume @p260 (forall @t481 (= (_ tptp.type_M141510067scheme @t67) (_ (_ tptp.sup_sup_set_nat (_ tptp.type_M1050318637scheme @t65)) (_ tptp.type_M141510067scheme @t64))))) % 3.70/3.99 (assume @p261 (= tptp.type_M1715972684le_typ (lambda (@list @t486) (_ (_ tptp.sup_sup_set_nat (_ tptp.type_Mirabelle_dom @t487)) (_ tptp.type_Mirabelle_cod @t487))))) % 3.70/3.99 (assume @p262 (forall @t379 (= (_ @t488 @t364) @t364))) % 3.70/3.99 (assume @p263 (forall @t378 (= (_ @t474 @t359) @t359))) % 3.70/3.99 (assume @p264 (forall @t379 (= (_ @t489 tptp.bot_bot_nat_o) @t364))) % 3.70/3.99 (assume @p265 (forall @t378 (= (_ @t490 tptp.bot_bot_set_nat) @t359))) % 3.70/3.99 (assume @p266 (forall @t242 (= (_ @t491 tptp.bot_bot_nat_o) @t240))) % 3.70/3.99 (assume @p267 (forall @t245 (= (_ @t492 tptp.bot_bot_set_nat) @t243))) % 3.70/3.99 (assume @p268 (forall @t356 (= (= tptp.bot_bot_nat_o @t494) @t493))) % 3.70/3.99 (assume @p269 (forall @t354 (= (= tptp.bot_bot_set_nat @t496) @t495))) % 3.70/3.99 (assume @p270 (forall @t242 (= (_ @t488 @t240) @t240))) % 3.70/3.99 (assume @p271 (forall @t245 (= (_ @t474 @t243) @t243))) % 3.70/3.99 (assume @p272 (forall @t356 (= (= @t494 tptp.bot_bot_nat_o) @t493))) % 3.70/3.99 (assume @p273 (forall @t354 (= (= @t496 tptp.bot_bot_set_nat) @t495))) % 3.70/3.99 (assume @p274 (forall @t367 (= (= @t498 tptp.bot_bot_nat_o) @t497))) % 3.70/3.99 (assume @p275 (forall @t362 (= (= @t500 tptp.bot_bot_set_nat) @t499))) % 3.70/3.99 (assume @p276 (forall @t367 (= (= tptp.bot_bot_nat_o @t498) @t497))) % 3.70/3.99 (assume @p277 (forall @t362 (= (= tptp.bot_bot_set_nat @t500) @t499))) % 3.70/3.99 (assume @p278 (forall (@list @t502 @t501) (= (_ (_ tptp.sup_sup_nat_o (lambda @t136 (_ @t186 @t502))) (lambda @t136 (_ @t186 @t501))) (lambda @t136 (_ @t186 (_ (_ tptp.sup_sup_set_nat @t502) @t501)))))) % 3.70/3.99 (assume @p279 (= tptp.sup_sup_set_nat (lambda @t469 (_ tptp.collect_nat (_ (_ tptp.sup_sup_nat_o @t506) @t504))))) % 3.70/3.99 (assume @p280 (forall (@list @t364 @t240 @t302) (=> (_ @t365 @t240) @t507))) % 3.70/3.99 (assume @p281 (forall (@list @t359 @t243 @t279) (=> (_ @t360 @t243) @t508))) % 3.70/3.99 (assume @p282 (forall (@list @t155 @t131 @t144) (=> (_ @t345 @t131) @t510))) % 3.70/3.99 (assume @p283 (forall (@list @t364 @t302 @t240) (=> (_ @t365 @t302) @t507))) % 3.70/3.99 (assume @p284 (forall (@list @t359 @t279 @t243) (=> (_ @t360 @t279) @t508))) % 3.70/3.99 (assume @p285 (forall (@list @t155 @t144 @t131) (=> (_ @t345 @t144) @t510))) % 3.70/3.99 (assume @p286 (forall (@list @t302 @t295 @t240) (=> (_ (_ tptp.ord_less_nat_o (_ (_ tptp.sup_sup_nat_o @t302) @t295)) @t240) (not (=> @t355 (not @t413)))))) % 3.70/3.99 (assume @p287 (forall (@list @t279 @t272 @t243) (=> (_ (_ tptp.ord_less_set_nat (_ (_ tptp.sup_sup_set_nat @t279) @t272)) @t243) (not (=> @t353 (not @t410)))))) % 3.70/3.99 (assume @p288 (forall (@list @t144 @t180 @t131) (=> (_ (_ tptp.ord_less_nat (_ (_ tptp.sup_sup_nat @t144) @t180)) @t131) (not (=> @t357 (not @t416)))))) % 3.70/3.99 (assume @p289 (= tptp.ord_less_set_nat (lambda (@list @t511 @t512) (and (= @t512 (_ (_ tptp.sup_sup_set_nat @t512) @t511)) (not (= @t512 @t511)))))) % 3.70/3.99 (assume @p290 (forall (@list @t295 @t240 @t302) (=> @t413 @t513))) % 3.70/3.99 (assume @p291 (forall (@list @t272 @t243 @t279) (=> @t410 @t514))) % 3.70/3.99 (assume @p292 (forall (@list @t180 @t131 @t144) (=> @t416 @t515))) % 3.70/3.99 (assume @p293 (forall (@list @t295 @t302 @t240) (=> @t414 @t513))) % 3.70/3.99 (assume @p294 (forall (@list @t272 @t279 @t243) (=> @t411 @t514))) % 3.70/3.99 (assume @p295 (forall (@list @t180 @t144 @t131) (=> @t417 @t515))) % 3.70/3.99 (assume @p296 (forall @t516 (=> (= @t182 @t444) (= @t445 @t155)))) % 3.70/3.99 (assume @p297 (forall @t516 (=> @t452 (= (_ @t182 @t155) (= @t155 @t445))))) % 3.70/3.99 (assume @p298 (_ (_ tptp.semila1414375521_nat_o tptp.sup_sup_nat_o) tptp.bot_bot_nat_o)) % 3.70/3.99 (assume @p299 (_ (_ tptp.semila1369944356et_nat tptp.sup_sup_set_nat) tptp.bot_bot_set_nat)) % 3.70/3.99 (assume @p300 (forall (@list @t359 @t518 @t358 @t517) (= @t520 (or @t361 (and @t370 @t519))))) % 3.70/3.99 (assume @p301 (forall (@list @t364 @t522 @t363 @t521) (= @t524 (or @t366 (and @t373 @t523))))) % 3.70/3.99 (assume @p302 (forall (@list @t155 @t210 @t215 @t525) (= @t528 (or @t348 (and @t374 @t527))))) % 3.70/3.99 (assume @p303 (forall @t529 (=> (not @t361) (=> @t370 (=> @t519 @t520))))) % 3.70/3.99 (assume @p304 (forall @t530 (=> (not @t366) (=> @t373 (=> @t523 @t524))))) % 3.70/3.99 (assume @p305 (forall @t531 (=> @t349 (=> @t374 (=> @t527 @t528))))) % 3.70/3.99 (assume @p306 (forall @t529 (=> @t361 @t520))) % 3.70/3.99 (assume @p307 (forall @t530 (=> @t366 @t524))) % 3.70/3.99 (assume @p308 (forall @t531 (=> @t348 @t528))) % 3.70/3.99 (assume @p309 (forall @t534 (=> @t527 (=> @t533 (= @t210 @t525))))) % 3.70/3.99 (assume @p310 (forall @t534 (or @t527 @t533))) % 3.70/3.99 (assume @p311 (forall (@list @t210 @t525 @t535) (=> @t527 (=> (_ @t532 @t535) (_ @t526 @t535))))) % 3.70/3.99 (assume @p312 (forall (@list @t210) (_ @t526 @t210))) % 3.70/3.99 (assume @p313 (forall (@list @t542 @t539) (=> (_ (_ tptp.ord_le727790544et_nat @t542) @t539) (=> (not (= @t542 tptp.nil_set_nat)) (=> (forall (@list @t275) (=> (exists (@list @t537) @t543) (forall (@list @t274) (=> (exists @t541 @t540) @t538)))) (not (forall (@list @t275 @t274 @t537) (=> @t543 (forall @t541 (=> @t540 (=> @t538 (=> (not (_ (_ tptp.ord_less_set_nat @t274) @t275)) (not (_ (_ tptp.ord_le727790544et_nat @t537) @t536)))))))))))))) % 3.70/3.99 (assume @p314 (forall (@list @t550 @t547) (=> (_ (_ tptp.ord_lexordp_eq_nat_o @t550) @t547) (=> (not (= @t550 tptp.nil_nat_o)) (=> (forall (@list @t298) (=> (exists (@list @t545) @t551) (forall (@list @t297) (=> (exists @t549 @t548) @t546)))) (not (forall (@list @t298 @t297 @t545) (=> @t551 (forall @t549 (=> @t548 (=> @t546 (=> (not (_ (_ tptp.ord_less_nat_o @t297) @t298)) (not (_ (_ tptp.ord_lexordp_eq_nat_o @t545) @t544)))))))))))))) % 3.70/3.99 (assume @p315 (forall (@list @t562 @t558) (=> (_ (_ tptp.ord_lexordp_eq_nat @t562) @t558) (=> (not (= @t562 tptp.nil_nat)) (=> (forall @t21 (=> (exists (@list @t553) @t563) (forall @t204 (=> (exists @t560 @t559) @t556)))) (not (forall (@list @t18 @t202 @t553) (=> @t563 (forall @t560 (=> @t559 (=> @t556 (=> @t555 (not @t554))))))))))))) % 3.70/3.99 (assume @p316 (= tptp.ord_le727790544et_nat (lambda (@list @t571 @t569) (or (exists (@list @t564) (and (= @t571 tptp.nil_set_nat) (= @t569 @t564))) (exists @t573 (and @t572 @t570 @t568)) (exists @t573 (and @t572 @t570 (not @t568) (not (_ (_ tptp.ord_less_set_nat @t567) @t566)) (_ (_ tptp.ord_le727790544et_nat @t565) @t564))))))) % 3.70/3.99 (assume @p317 (= tptp.ord_lexordp_eq_nat_o (lambda (@list @t581 @t579) (or (exists (@list @t574) (and (= @t581 tptp.nil_nat_o) (= @t579 @t574))) (exists @t583 (and @t582 @t580 @t578)) (exists @t583 (and @t582 @t580 (not @t578) (not (_ (_ tptp.ord_less_nat_o @t577) @t576)) (_ (_ tptp.ord_lexordp_eq_nat_o @t575) @t574))))))) % 3.70/3.99 (assume @p318 (= tptp.ord_lexordp_eq_nat (lambda (@list @t590 @t588) (or (exists (@list @t584) (and (= @t590 tptp.nil_nat) (= @t588 @t584))) (exists @t592 (and @t591 @t589 @t587)) (exists @t592 (and @t591 @t589 (not @t587) (not (_ (_ tptp.ord_less_nat @t586) @t134)) (_ (_ tptp.ord_lexordp_eq_nat @t585) @t584))))))) % 3.70/3.99 (assume @p319 (forall (@list @t15) (= (_ @t61 tptp.nil_Ty61485117scheme) tptp.nil_Ty61485117scheme))) % 3.70/3.99 (assume @p320 (forall @t251 (_ @t93 tptp.nil_Ty61485117scheme))) % 3.70/3.99 (assume @p321 (= (_ tptp.type_M141510067scheme tptp.nil_Ty61485117scheme) tptp.bot_bot_set_nat)) % 3.70/3.99 (assume @p322 (forall (@list @t594 @t593 @t595) (=> (_ (_ tptp.ord_lexordp_eq_nat @t594) @t593) (=> (forall (@list @t598) (_ (_ @t595 tptp.nil_nat) @t598)) (=> (forall @t597 (=> @t260 @t596)) (=> (forall @t597 (=> @t556 (=> @t555 (=> @t554 (=> (_ (_ @t595 @t553) @t552) @t596))))) (_ (_ @t595 @t594) @t593))))))) % 3.70/3.99 (assume @p323 (forall @t352 (= (_ (_ (_ tptp.if_nat false) @t155) @t215) @t215))) % 3.70/3.99 (assume @p324 (forall @t352 (= (_ (_ (_ tptp.if_nat true) @t155) @t215) @t155))) % 3.70/3.99 (assume @p325 (forall (@list @t394) (or (= @t394 true) (= @t394 false)))) % 3.70/3.99 (assume @p326 (forall @t599 (= (_ (_ (_ tptp.if_Typ1169047309le_typ false) @t55) @t439) @t439))) % 3.70/3.99 (assume @p327 (forall @t599 (= (_ (_ (_ tptp.if_Typ1169047309le_typ true) @t55) @t439) @t55))) % 3.70/3.99 (assume @p328 @t615) % 3.70/3.99 (assume @p329 true) % 3.70/3.99 (step @p330 (= tptp.type_M244876119le_typ @t618) :rule refl :args (@t618)) % 3.70/3.99 (step @p331 (= tptp.type_M1377662078scheme @t620) :rule refl :args (@t620)) % 3.70/3.99 (step @p332 (= tptp.type_M263553000le_typ @t622) :rule refl :args (@t622)) % 3.70/3.99 (step @p333 (= tptp.type_M1963061490scheme @t624) :rule refl :args (@t624)) % 3.70/3.99 (step @p334 (= tptp.type_M1211611096le_typ @t626) :rule refl :args (@t626)) % 3.70/3.99 (step @p335 (= tptp.type_M2064939256scheme @t628) :rule refl :args (@t628)) % 3.70/3.99 (step @p336 (= tptp.type_M1734147655le_typ @t630) :rule refl :args (@t630)) % 3.70/3.99 (step @p337 (= tptp.insert_nat @t631) :rule refl :args (@t631)) % 3.70/3.99 (step @p338 (= tptp.bot_bot_nat_o @t632) :rule refl :args (@t632)) % 3.70/3.99 (step @p339 (= tptp.is_singleton_nat @t633) :rule refl :args (@t633)) % 3.70/3.99 (step @p340 (= tptp.is_empty_nat @t634) :rule refl :args (@t634)) % 3.70/3.99 (step @p341 (= tptp.the_elem_nat @t636) :rule refl :args (@t636)) % 3.70/3.99 (step @p342 (= tptp.type_Mirabelle_dom @t639) :rule refl :args (@t639)) % 3.70/3.99 (step @p343 (= tptp.ord_less_set_nat @t640) :rule refl :args (@t640)) % 3.70/3.99 (step @p344 (= tptp.if_nat @t643) :rule refl :args (@t643)) % 3.70/3.99 (step @p345 (= tptp.type_M1715972684le_typ @t644) :rule refl :args (@t644)) % 3.70/3.99 (step @p346 (= tptp.sup_sup_set_nat @t645) :rule refl :args (@t645)) % 3.70/3.99 (step @p347 (= tptp.ord_less_nat_o @t648) :rule refl :args (@t648)) % 3.70/3.99 (step @p348 (= tptp.ord_less_nat @t650) :rule refl :args (@t650)) % 3.70/3.99 (step @p349 :rule evaluate :args ((= true false))) % 3.70/3.99 (step @p350 :rule refl :args (@t651)) % 3.70/3.99 (step @p351 :rule refl :args (@t107)) % 3.70/3.99 (step @p352 :rule cong :premises (@p351 @p350) :args ((= @t107 @t651))) % 3.70/3.99 (step @p353 :rule symm :premises (@p352)) % 3.70/3.99 (step @p354 :rule eq_resolve :premises (@p351 @p353)) % 3.70/3.99 (step @p355 :rule refl :args (@t652)) % 3.70/3.99 (step @p356 :rule refl :args (@t108)) % 3.70/3.99 (step @p357 :rule cong :premises (@p356 @p355) :args ((= @t108 @t652))) % 3.70/3.99 (step @p358 :rule symm :premises (@p357)) % 3.70/3.99 (step @p359 :rule eq_resolve :premises (@p356 @p358)) % 3.70/3.99 (step @p360 :rule cong :premises (@p359 @p354) :args (@t109)) % 3.70/3.99 (step @p361 :rule refl :args ((tptp.member_nat @t22 @t69))) % 3.70/3.99 (step @p362 :rule refl :args (@t653)) % 3.70/3.99 (step @p363 :rule refl :args (@t22)) % 3.70/3.99 (step @p364 :rule cong :premises (@p363 @p362) :args (@t654)) % 3.70/3.99 (step @p365 :rule trans :premises (@p364 @p361)) % 3.70/3.99 (step @p366 :rule refl :args (@t110)) % 3.70/3.99 (step @p367 :rule ho_cong :premises (@p366 @p362)) % 3.70/3.99 (step @p368 :rule cong :premises (@p367 @p365) :args ((= (_ @t110 @t653) @t654))) % 3.70/3.99 (step @p369 :rule symm :premises (@p368)) % 3.70/3.99 (step @p370 :rule refl :args (@t111)) % 3.70/3.99 (step @p371 :rule eq_resolve :premises (@p370 @p369)) % 3.70/3.99 (step @p372 :rule refl :args (@t69)) % 3.70/3.99 (step @p373 :rule cong :premises (@p372 @p362) :args ((= @t69 @t653))) % 3.70/3.99 (step @p374 :rule symm :premises (@p373)) % 3.70/3.99 (step @p375 :rule eq_resolve :premises (@p372 @p374)) % 3.70/3.99 (step @p376 :rule ho_cong :premises (@p366 @p375)) % 3.70/3.99 (step @p377 :rule trans :premises (@p376 @p371)) % 3.70/3.99 (step @p378 :rule cong :premises (@p377) :args (@t655)) % 3.70/3.99 (step @p379 :rule refl :args (@t656)) % 3.70/3.99 (step @p380 :rule refl :args (@t104)) % 3.70/3.99 (step @p381 :rule cong :premises (@p380 @p379) :args ((= @t104 @t656))) % 3.70/3.99 (step @p382 :rule symm :premises (@p381)) % 3.70/3.99 (step @p383 :rule eq_resolve :premises (@p380 @p382)) % 3.70/3.99 (step @p384 :rule refl :args (@t657)) % 3.70/3.99 (step @p385 :rule refl :args (@t105)) % 3.70/3.99 (step @p386 :rule cong :premises (@p385 @p384) :args ((= @t105 @t657))) % 3.70/3.99 (step @p387 :rule symm :premises (@p386)) % 3.70/3.99 (step @p388 :rule eq_resolve :premises (@p385 @p387)) % 3.70/3.99 (step @p389 :rule cong :premises (@p388 @p383) :args (@t106)) % 3.70/3.99 (step @p390 :rule cong :premises (@p389) :args (@t658)) % 3.70/3.99 (step @p391 :rule nary_cong :premises (@p390 @p378 @p360) :args (@t659)) % 3.70/3.99 (step @p392 :rule cong :premises (@p391) :args ((forall @t113 @t659))) % 3.70/3.99 (step @p393 :rule aci_norm :args ((= (or @t658 (or @t655 @t109)) @t659))) % 3.70/3.99 (step @p394 :rule bool-impl-elim :args (@t111 @t109)) % 3.70/3.99 (step @p395 :rule refl :args (@t658)) % 3.70/3.99 (step @p396 :rule nary_cong :premises (@p395 @p394) :args ((or @t658 @t112))) % 3.70/3.99 (step @p397 :rule trans :premises (@p396 @p393)) % 3.70/3.99 (step @p398 :rule bool-impl-elim :args (@t106 @t112)) % 3.70/3.99 (step @p399 :rule trans :premises (@p398 @p397)) % 3.70/3.99 (step @p400 :rule cong :premises (@p399) :args (@t114)) % 3.70/3.99 (step @p401 :rule trans :premises (@p400 @p392)) % 3.70/3.99 (step @p402 :rule eq_resolve :premises (@p34 @p401)) % 3.70/3.99 (step @p403 :rule refl :args (@t662)) % 3.70/3.99 (step @p404 :rule refl :args (@t665)) % 3.70/3.99 (step @p405 :rule eq-symm :args (@t666 @t667)) % 3.70/3.99 (step @p406 :rule cong :premises (@p405) :args (@t668)) % 3.70/3.99 (step @p407 :rule nary_cong :premises (@p406 @p404 @p403) :args (@t669)) % 3.70/3.99 (step @p408 :rule refl :args (@t670)) % 3.70/3.99 (step @p409 :rule cong :premises (@p408 @p407) :args ((=> @t670 @t669))) % 3.70/3.99 (assume-push @p637 @t670) % 3.70/3.99 (step @p411 :rule instantiate :premises (@p402) :args ((@list tptp.s2 @t663 tptp.s1 tptp.n))) % 3.70/3.99 (step-pop @p638 :rule scope :premises (@p411)) % 3.70/3.99 (step @p412 :rule process_scope :premises (@p638) :args (@t669)) % 3.70/3.99 (step @p414 :rule eq_resolve :premises (@p412 @p409)) % 3.70/3.99 (step @p415 :rule implies_elim :premises (@p414)) % 3.70/3.99 (step @p416 :rule chain_m_resolution :premises (@p415 @p402) :args (@t672 (@list false) (@list @t670))) % 3.70/3.99 (step @p417 :rule eq-symm :args (@t660 @t661)) % 3.70/3.99 (step @p418 :rule refl :args (@t661)) % 3.70/3.99 (step @p419 :rule refl :args (@t600)) % 3.70/3.99 (step @p420 :rule cong :premises (@p419 @p418) :args ((= @t600 @t661))) % 3.70/3.99 (step @p421 :rule symm :premises (@p420)) % 3.70/3.99 (step @p422 :rule eq_resolve :premises (@p419 @p421)) % 3.70/3.99 (step @p423 :rule refl :args (@t660)) % 3.70/3.99 (step @p424 :rule refl :args (@t601)) % 3.70/3.99 (step @p425 :rule cong :premises (@p424 @p423) :args ((= @t601 @t660))) % 3.70/3.99 (step @p426 :rule symm :premises (@p425)) % 3.70/3.99 (step @p427 :rule eq_resolve :premises (@p424 @p426)) % 3.70/3.99 (step @p428 :rule cong :premises (@p427 @p422) :args (@t602)) % 3.70/3.99 (step @p429 :rule trans :premises (@p428 @p417)) % 3.70/3.99 (step @p430 :rule refl :args ((tptp.member_nat tptp.n @t604))) % 3.70/3.99 (step @p431 :rule refl :args ((tptp.type_M1050318637scheme @t603))) % 3.70/3.99 (step @p432 :rule refl :args (@t673)) % 3.70/3.99 (step @p433 :rule cong :premises (@p432) :args (@t674)) % 3.70/3.99 (step @p434 :rule trans :premises (@p433 @p431)) % 3.70/3.99 (step @p435 :rule refl :args (tptp.n)) % 3.70/3.99 (step @p436 :rule cong :premises (@p435 @p434) :args (@t675)) % 3.70/3.99 (step @p437 :rule trans :premises (@p436 @p430)) % 3.70/3.99 (step @p438 :rule refl :args (@t605)) % 3.70/3.99 (step @p439 :rule ho_cong :premises (@p438 @p434)) % 3.70/3.99 (step @p440 :rule cong :premises (@p439 @p437) :args ((= (_ @t605 @t674) @t675))) % 3.70/3.99 (step @p441 :rule symm :premises (@p440)) % 3.70/3.99 (step @p442 :rule refl :args (@t606)) % 3.70/3.99 (step @p443 :rule eq_resolve :premises (@p442 @p441)) % 3.70/3.99 (step @p444 :rule refl :args (tptp.type_M1050318637scheme)) % 3.70/3.99 (step @p445 :rule ho_cong :premises (@p444 @p432)) % 3.70/3.99 (step @p446 :rule cong :premises (@p445 @p434) :args ((= (_ tptp.type_M1050318637scheme @t673) @t674))) % 3.70/3.99 (step @p447 :rule symm :premises (@p446)) % 3.70/3.99 (step @p448 :rule refl :args (@t604)) % 3.70/3.99 (step @p449 :rule eq_resolve :premises (@p448 @p447)) % 3.70/3.99 (step @p450 :rule refl :args (@t603)) % 3.70/3.99 (step @p451 :rule cong :premises (@p450 @p432) :args ((= @t603 @t673))) % 3.70/3.99 (step @p452 :rule symm :premises (@p451)) % 3.70/3.99 (step @p453 :rule eq_resolve :premises (@p450 @p452)) % 3.70/3.99 (step @p454 :rule refl :args (tptp.type_M1050318637scheme)) % 3.70/3.99 (step @p455 :rule ho_cong :premises (@p454 @p453)) % 3.70/3.99 (step @p456 :rule trans :premises (@p455 @p449)) % 3.70/3.99 (step @p457 :rule refl :args (@t605)) % 3.70/3.99 (step @p458 :rule ho_cong :premises (@p457 @p456)) % 3.70/3.99 (step @p459 :rule trans :premises (@p458 @p443)) % 3.70/3.99 (step @p460 :rule cong :premises (@p459) :args (@t607)) % 3.70/3.99 (step @p461 :rule eq-symm :args (@t676 @t677)) % 3.70/3.99 (step @p462 :rule refl :args ((tptp.type_M1690910139scheme tptp.s2 @t603))) % 3.70/3.99 (step @p463 :rule refl :args (tptp.s2)) % 3.70/3.99 (step @p464 :rule cong :premises (@p463 @p432) :args (@t677)) % 3.70/3.99 (step @p465 :rule trans :premises (@p464 @p462)) % 3.70/3.99 (step @p466 :rule refl :args (@t608)) % 3.70/3.99 (step @p467 :rule ho_cong :premises (@p466 @p432)) % 3.70/3.99 (step @p468 :rule cong :premises (@p467 @p465) :args ((= (_ @t608 @t673) @t677))) % 3.70/3.99 (step @p469 :rule symm :premises (@p468)) % 3.70/3.99 (step @p470 :rule refl :args (@t609)) % 3.70/3.99 (step @p471 :rule eq_resolve :premises (@p470 @p469)) % 3.70/3.99 (step @p472 :rule refl :args (@t608)) % 3.70/3.99 (step @p473 :rule ho_cong :premises (@p472 @p453)) % 3.70/3.99 (step @p474 :rule trans :premises (@p473 @p471)) % 3.70/3.99 (step @p475 :rule refl :args ((tptp.type_M1690910139scheme tptp.s1 @t603))) % 3.70/3.99 (step @p476 :rule refl :args (tptp.s1)) % 3.70/3.99 (step @p477 :rule cong :premises (@p476 @p432) :args (@t676)) % 3.70/3.99 (step @p478 :rule trans :premises (@p477 @p475)) % 3.70/3.99 (step @p479 :rule refl :args (@t610)) % 3.70/3.99 (step @p480 :rule ho_cong :premises (@p479 @p432)) % 3.70/3.99 (step @p481 :rule cong :premises (@p480 @p478) :args ((= (_ @t610 @t673) @t676))) % 3.70/3.99 (step @p482 :rule symm :premises (@p481)) % 3.70/3.99 (step @p483 :rule refl :args (@t611)) % 3.70/3.99 (step @p484 :rule eq_resolve :premises (@p483 @p482)) % 3.70/3.99 (step @p485 :rule refl :args (@t610)) % 3.70/3.99 (step @p486 :rule ho_cong :premises (@p485 @p453)) % 3.70/3.99 (step @p487 :rule trans :premises (@p486 @p484)) % 3.70/3.99 (step @p488 :rule cong :premises (@p487 @p474) :args (@t612)) % 3.70/3.99 (step @p489 :rule trans :premises (@p488 @p461)) % 3.70/3.99 (step @p490 :rule cong :premises (@p489) :args (@t613)) % 3.70/3.99 (step @p491 :rule nary_cong :premises (@p490 @p460 @p429) :args (@t614)) % 3.70/3.99 (step @p492 :rule cong :premises (@p491) :args (@t615)) % 3.70/3.99 (step @p493 :rule eq_resolve :premises (@p328 @p492)) % 3.70/3.99 (step @p494 :rule not_or_elim :premises (@p493) :args (1)) % 3.70/3.99 (step @p495 :rule not_not_elim :premises (@p494)) % 3.70/3.99 (step @p496 :rule true_intro :premises (@p495)) % 3.70/3.99 (step @p497 :rule refl :args ((tptp.type_M1006385707scheme @t254))) % 3.70/3.99 (step @p498 :rule refl :args (@t678)) % 3.70/3.99 (step @p499 :rule cong :premises (@p498) :args (@t679)) % 3.70/3.99 (step @p500 :rule trans :premises (@p499 @p497)) % 3.70/3.99 (step @p501 :rule refl :args (tptp.type_M1006385707scheme)) % 3.70/3.99 (step @p502 :rule ho_cong :premises (@p501 @p498)) % 3.70/3.99 (step @p503 :rule cong :premises (@p502 @p500) :args ((= (_ tptp.type_M1006385707scheme @t678) @t679))) % 3.70/3.99 (step @p504 :rule symm :premises (@p503)) % 3.70/3.99 (step @p505 :rule refl :args (@t420)) % 3.70/3.99 (step @p506 :rule eq_resolve :premises (@p505 @p504)) % 3.70/3.99 (step @p507 :rule refl :args (@t254)) % 3.70/3.99 (step @p508 :rule cong :premises (@p507 @p498) :args ((= @t254 @t678))) % 3.70/3.99 (step @p509 :rule symm :premises (@p508)) % 3.70/3.99 (step @p510 :rule eq_resolve :premises (@p507 @p509)) % 3.70/3.99 (step @p511 :rule ho_cong :premises (@p501 @p510)) % 3.70/3.99 (step @p512 :rule trans :premises (@p511 @p506)) % 3.70/3.99 (step @p513 :rule refl :args (@t680)) % 3.70/3.99 (step @p514 :rule refl :args (@t25)) % 3.70/3.99 (step @p515 :rule cong :premises (@p514 @p513) :args ((= @t25 @t680))) % 3.70/3.99 (step @p516 :rule symm :premises (@p515)) % 3.70/3.99 (step @p517 :rule eq_resolve :premises (@p514 @p516)) % 3.70/3.99 (step @p518 :rule cong :premises (@p517 @p512) :args (@t681)) % 3.70/3.99 (step @p519 :rule cong :premises (@p518) :args ((forall @t251 @t681))) % 3.70/3.99 (step @p520 :rule eq-symm :args (@t420 @t25)) % 3.70/3.99 (step @p521 :rule cong :premises (@p520) :args (@t421)) % 3.70/3.99 (step @p522 :rule trans :premises (@p521 @p519)) % 3.70/3.99 (step @p523 :rule eq_resolve :premises (@p197 @p522)) % 3.70/3.99 (step @p524 :rule instantiate :premises (@p523) :args ((@list tptp.x))) % 3.70/3.99 (step @p525 :rule symm :premises (@p524)) % 3.70/3.99 (step @p526 :rule cong :premises (@p525) :args ((tptp.type_M1050318637scheme (tptp.type_M1006385707scheme @t663)))) % 3.70/3.99 (step @p527 :rule refl :args ((tptp.type_M1050318637scheme @t70))) % 3.70/3.99 (step @p528 :rule refl :args (@t682)) % 3.70/3.99 (step @p529 :rule cong :premises (@p528) :args (@t683)) % 3.70/3.99 (step @p530 :rule trans :premises (@p529 @p527)) % 3.70/3.99 (step @p531 :rule ho_cong :premises (@p444 @p528)) % 3.70/3.99 (step @p532 :rule cong :premises (@p531 @p530) :args ((= (_ tptp.type_M1050318637scheme @t682) @t683))) % 3.70/3.99 (step @p533 :rule symm :premises (@p532)) % 3.70/3.99 (step @p534 :rule refl :args (@t71)) % 3.70/3.99 (step @p535 :rule eq_resolve :premises (@p534 @p533)) % 3.70/3.99 (step @p536 :rule refl :args (@t70)) % 3.70/3.99 (step @p537 :rule cong :premises (@p536 @p528) :args ((= @t70 @t682))) % 3.70/3.99 (step @p538 :rule symm :premises (@p537)) % 3.70/3.99 (step @p539 :rule eq_resolve :premises (@p536 @p538)) % 3.70/3.99 (step @p540 :rule ho_cong :premises (@p444 @p539)) % 3.70/3.99 (step @p541 :rule trans :premises (@p540 @p535)) % 3.70/3.99 (step @p542 :rule cong :premises (@p541 @p375) :args (@t72)) % 3.70/3.99 (step @p543 :rule cong :premises (@p542) :args (@t73)) % 3.70/3.99 (step @p544 :rule eq_resolve :premises (@p15 @p543)) % 3.70/3.99 (step @p545 :rule instantiate :premises (@p544) :args ((@list @t663))) % 3.70/3.99 (step @p546 :rule symm :premises (@p545)) % 3.70/3.99 (step @p547 :rule trans :premises (@p546 @p526)) % 3.70/3.99 (step @p548 :rule refl :args (tptp.n)) % 3.70/3.99 (step @p549 :rule cong :premises (@p548 @p547) :args (@t664)) % 3.70/3.99 (step @p550 :rule trans :premises (@p549 @p496)) % 3.70/3.99 (step @p551 :rule true_elim :premises (@p550)) % 3.70/3.99 (step @p552 :rule not_or_elim :premises (@p493) :args (2)) % 3.70/3.99 (step @p553 :rule cnf_or_pos :args (@t672)) % 3.70/3.99 (step @p554 :rule reordering :premises (@p553) :args ((or @t662 @t665 @t671 (not @t672)))) % 3.70/3.99 (step @p555 :rule chain_m_resolution :premises (@p554 @p552 @p551 @p416) :args (@t671 (@list true false false) (@list @t662 @t664 @t672))) % 3.70/3.99 (step @p556 :rule false_intro :premises (@p555)) % 3.70/3.99 (step @p557 :rule refl :args ((tptp.type_M784671311le_typ @t15 @t254))) % 3.70/3.99 (step @p558 :rule refl :args (@t15)) % 3.70/3.99 (step @p559 :rule cong :premises (@p558 @p498) :args (@t684)) % 3.70/3.99 (step @p560 :rule trans :premises (@p559 @p557)) % 3.70/3.99 (step @p561 :rule refl :args (@t56)) % 3.70/3.99 (step @p562 :rule ho_cong :premises (@p561 @p498)) % 3.70/3.99 (step @p563 :rule cong :premises (@p562 @p560) :args ((= (_ @t56 @t678) @t684))) % 3.70/3.99 (step @p564 :rule symm :premises (@p563)) % 3.70/3.99 (step @p565 :rule refl :args (@t255)) % 3.70/3.99 (step @p566 :rule eq_resolve :premises (@p565 @p564)) % 3.70/3.99 (step @p567 :rule ho_cong :premises (@p561 @p510)) % 3.70/3.99 (step @p568 :rule trans :premises (@p567 @p566)) % 3.70/3.99 (step @p569 :rule refl :args (@t685)) % 3.70/3.99 (step @p570 :rule refl :args (@t23)) % 3.70/3.99 (step @p571 :rule cong :premises (@p570 @p569) :args ((= @t23 @t685))) % 3.70/3.99 (step @p572 :rule symm :premises (@p571)) % 3.70/3.99 (step @p573 :rule eq_resolve :premises (@p570 @p572)) % 3.70/3.99 (step @p574 :rule cong :premises (@p573 @p568) :args (@t686)) % 3.70/3.99 (step @p575 :rule cong :premises (@p574) :args ((forall @t28 @t686))) % 3.70/3.99 (step @p576 :rule eq-symm :args (@t255 @t23)) % 3.70/3.99 (step @p577 :rule cong :premises (@p576) :args (@t256)) % 3.70/3.99 (step @p578 :rule trans :premises (@p577 @p575)) % 3.70/3.99 (step @p579 :rule eq_resolve :premises (@p104 @p578)) % 3.70/3.99 (step @p580 :rule instantiate :premises (@p579) :args (@t687)) % 3.70/3.99 (step @p581 :rule refl :args (@t116)) % 3.70/3.99 (step @p582 :rule refl :args (@t688)) % 3.70/3.99 (step @p583 :rule refl :args (@t117)) % 3.70/3.99 (step @p584 :rule cong :premises (@p583 @p582) :args ((= @t117 @t688))) % 3.70/3.99 (step @p585 :rule symm :premises (@p584)) % 3.70/3.99 (step @p586 :rule eq_resolve :premises (@p583 @p585)) % 3.70/3.99 (step @p587 :rule cong :premises (@p539 @p586) :args (@t118)) % 3.70/3.99 (step @p588 :rule cong :premises (@p587) :args (@t689)) % 3.70/3.99 (step @p589 :rule nary_cong :premises (@p588 @p581) :args (@t690)) % 3.70/3.99 (step @p590 :rule cong :premises (@p589) :args ((forall @t119 @t690))) % 3.70/3.99 (step @p591 :rule bool-impl-elim :args (@t118 @t116)) % 3.70/3.99 (step @p592 :rule cong :premises (@p591) :args (@t120)) % 3.70/3.99 (step @p593 :rule trans :premises (@p592 @p590)) % 3.70/3.99 (step @p594 :rule eq_resolve :premises (@p36 @p593)) % 3.70/3.99 (step @p595 :rule instantiate :premises (@p594) :args ((@list @t692 @t691))) % 3.70/3.99 (step @p596 :rule refl :args ((tptp.type_M1006385707scheme @t23))) % 3.70/3.99 (step @p597 :rule cong :premises (@p569) :args (@t693)) % 3.70/3.99 (step @p598 :rule trans :premises (@p597 @p596)) % 3.70/3.99 (step @p599 :rule ho_cong :premises (@p501 @p569)) % 3.70/3.99 (step @p600 :rule cong :premises (@p599 @p598) :args ((= (_ tptp.type_M1006385707scheme @t685) @t693))) % 3.70/3.99 (step @p601 :rule symm :premises (@p600)) % 3.70/3.99 (step @p602 :rule refl :args (@t24)) % 3.70/3.99 (step @p603 :rule eq_resolve :premises (@p602 @p601)) % 3.70/3.99 (step @p604 :rule ho_cong :premises (@p501 @p573)) % 3.70/3.99 (step @p605 :rule trans :premises (@p604 @p603)) % 3.70/3.99 (step @p606 :rule refl :args ((tptp.type_M1690910139scheme @t15 @t25))) % 3.70/3.99 (step @p607 :rule cong :premises (@p558 @p513) :args (@t694)) % 3.70/3.99 (step @p608 :rule trans :premises (@p607 @p606)) % 3.70/3.99 (step @p609 :rule refl :args (@t16)) % 3.70/3.99 (step @p610 :rule ho_cong :premises (@p609 @p513)) % 3.70/3.99 (step @p611 :rule cong :premises (@p610 @p608) :args ((= (_ @t16 @t680) @t694))) % 3.70/3.99 (step @p612 :rule symm :premises (@p611)) % 3.70/3.99 (step @p613 :rule refl :args (@t26)) % 3.70/3.99 (step @p614 :rule eq_resolve :premises (@p613 @p612)) % 3.70/3.99 (step @p615 :rule ho_cong :premises (@p609 @p517)) % 3.70/3.99 (step @p616 :rule trans :premises (@p615 @p614)) % 3.70/3.99 (step @p617 :rule cong :premises (@p616 @p605) :args (@t27)) % 3.70/3.99 (step @p618 :rule cong :premises (@p617) :args (@t29)) % 3.70/3.99 (step @p619 :rule eq_resolve :premises (@p4 @p618)) % 3.70/3.99 (step @p620 :rule instantiate :premises (@p619) :args (@t687)) % 3.70/3.99 (step @p621 :rule not_or_elim :premises (@p493) :args (0)) % 3.70/3.99 (step @p622 :rule not_not_elim :premises (@p621)) % 3.70/3.99 (step @p623 :rule symm :premises (@p622)) % 3.70/4.00 (step @p624 :rule instantiate :premises (@p619) :args (@t695)) % 3.70/4.00 (step @p625 :rule symm :premises (@p624)) % 3.70/4.00 (step @p626 :rule trans :premises (@p625 @p623 @p620)) % 3.70/4.00 (step @p627 :rule cnf_or_pos :args (@t699)) % 3.70/4.00 (step @p628 :rule reordering :premises (@p627) :args ((or @t698 @t696 (not @t699)))) % 3.70/4.00 (step @p629 :rule chain_m_resolution :premises (@p628 @p626 @p595) :args (@t696 (@list false false) (@list @t697 @t699))) % 3.70/4.00 (step @p630 :rule instantiate :premises (@p579) :args (@t695)) % 3.70/4.00 (step @p631 :rule symm :premises (@p630)) % 3.70/4.00 (step @p632 :rule trans :premises (@p631 @p629 @p580)) % 3.70/4.00 (step @p633 :rule true_intro :premises (@p632)) % 3.70/4.00 (step @p634 :rule symm :premises (@p633)) % 3.70/4.00 (step @p635 :rule trans :premises (@p634 @p556)) % 3.70/4.00 (step @p636 false :rule eq_resolve :premises (@p635 @p349)) % 3.70/4.00 ) % 3.70/4.00 % SZS output end Proof % 3.70/4.00 % cvc5 exiting %------------------------------------------------------------------------------