cvc5---1.3.4.THM-Prf.s

%------------------------------------------------------------------------------
% File     : cvc5---1.3.4
% Problem  : ITP026^1 : TPTP v9.2.1. Released v7.5.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM

% Computer : n001.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Wed Jun  3 08:24:50 AM UTC 2026

% Result   : Theorem 152.02s 152.36s
% Output   : Proof 152.02s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem  : ITP026^1 : TPTP v9.2.1. Released v7.5.0.
% 0.12/0.13  % Command  : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.16/0.34  % Computer : n001.cluster.edu
% 0.16/0.34  % Model    : x86_64 x86_64
% 0.16/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34  % Memory   : 8042.1875MB
% 0.16/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34  % CPULimit : 300
% 0.16/0.34  % WCLimit  : 300
% 0.16/0.34  % DateTime : Tue Jun  2 04:11:05 EDT 2026
% 0.16/0.34  % CPUTime  : 
% 0.46/0.63  %----Proving TH0
% 152.02/152.36  --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 90s...
% 152.02/152.36  --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --mbqi-enum-choice-grammar-all --no-cegqi --no-sygus-inst at 30s...
% 152.02/152.36  --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-mbqi-nested-check --no-cegqi --no-sygus-inst at 30s...
% 152.02/152.36  --- Run --ho-elim --full-saturate-quant at 18s...
% 152.02/152.36  % SZS status Theorem
% 152.02/152.36  % SZS output start Proof
% 152.02/152.36  (
% 152.02/152.36  (declare-sort tptp.nat 0)
% 152.02/152.36  (declare-sort tptp.b 0)
% 152.02/152.36  (declare-sort tptp.set_nat_b 0)
% 152.02/152.36  (declare-sort tptp.set_nat_a 0)
% 152.02/152.36  (declare-sort tptp.set_a 0)
% 152.02/152.36  (declare-sort tptp.carrie722926983_a_b_c 0)
% 152.02/152.36  (declare-sort tptp.a 0)
% 152.02/152.36  (declare-sort tptp.carrie1950868226xt_b_d 0)
% 152.02/152.36  (declare-sort tptp.set_b 0)
% 152.02/152.36  (declare-sort tptp.carrie1963041556t_unit 0)
% 152.02/152.36  (declare-sort tptp.carrie1821755406_e_b_f 0)
% 152.02/152.36  (declare-sort tptp.set_e 0)
% 152.02/152.36  (declare-sort tptp.carrie980467975t_unit 0)
% 152.02/152.37  (declare-sort tptp.carrie1065537299t_unit 0)
% 152.02/152.37  (declare-sort tptp.carrie292259835t_unit 0)
% 152.02/152.37  (declare-sort tptp.carrie377329159t_unit 0)
% 152.02/152.37  (declare-sort tptp.set_nat 0)
% 152.02/152.37  (declare-sort tptp.set_nat_e 0)
% 152.02/152.37  (declare-sort tptp.e 0)
% 152.02/152.37  (declare-const tptp.ord_less_nat (-> tptp.nat tptp.nat Bool))
% 152.02/152.37  (declare-const tptp.xa tptp.nat)
% 152.02/152.37  (declare-const tptp.x tptp.a)
% 152.02/152.37  (declare-const tptp.n tptp.carrie1821755406_e_b_f)
% 152.02/152.37  (declare-const tptp.t (-> tptp.nat tptp.b))
% 152.02/152.37  (declare-const tptp.h1 tptp.set_a)
% 152.02/152.37  (declare-const tptp.insert_nat_b (-> (-> tptp.nat tptp.b) tptp.set_nat_b tptp.set_nat_b))
% 152.02/152.37  (declare-const tptp.minus_780847917_nat_b (-> tptp.set_nat_b tptp.set_nat_b tptp.set_nat_b))
% 152.02/152.37  (declare-const tptp.insert_nat_a (-> (-> tptp.nat tptp.a) tptp.set_nat_a tptp.set_nat_a))
% 152.02/152.37  (declare-const tptp.minus_1788767276_nat_a (-> tptp.set_nat_a tptp.set_nat_a tptp.set_nat_a))
% 152.02/152.37  (declare-const tptp.bot_bot_set_nat tptp.set_nat)
% 152.02/152.37  (declare-const tptp.bot_bot_set_nat_a tptp.set_nat_a)
% 152.02/152.37  (declare-const tptp.minus_minus_set_a (-> tptp.set_a tptp.set_a tptp.set_a))
% 152.02/152.37  (declare-const tptp.ord_less_set_a (-> tptp.set_a tptp.set_a Bool))
% 152.02/152.37  (declare-const tptp.zero_a1261444626_a_b_c (-> tptp.carrie722926983_a_b_c tptp.a))
% 152.02/152.37  (declare-const tptp.linear_span_b_d_a_c (-> tptp.carrie1950868226xt_b_d tptp.carrie722926983_a_b_c tptp.set_b tptp.set_a tptp.set_a))
% 152.02/152.37  (declare-const tptp.insert_a (-> tptp.a tptp.set_a tptp.set_a))
% 152.02/152.37  (declare-const tptp.mdl_a_b_c (-> tptp.carrie722926983_a_b_c tptp.set_a tptp.carrie1963041556t_unit))
% 152.02/152.37  (declare-const tptp.quotie1196826005t_unit (-> tptp.carrie1950868226xt_b_d tptp.carrie1963041556t_unit tptp.set_a tptp.set_a tptp.set_b))
% 152.02/152.37  (declare-const tptp.quotie169863047_d_e_f (-> tptp.carrie1950868226xt_b_d tptp.carrie1821755406_e_b_f tptp.set_e tptp.set_e tptp.set_b))
% 152.02/152.37  (declare-const tptp.smodul132175289t_unit (-> tptp.carrie1950868226xt_b_d tptp.carrie1963041556t_unit tptp.set_b tptp.set_a))
% 152.02/152.37  (declare-const tptp.smodul1982583723_d_e_f (-> tptp.carrie1950868226xt_b_d tptp.carrie1821755406_e_b_f tptp.set_b tptp.set_e))
% 152.02/152.37  (declare-const tptp.ord_le1296932838_nat_b (-> tptp.set_nat_b tptp.set_nat_b Bool))
% 152.02/152.37  (declare-const tptp.annihilator_b_d_e_f (-> tptp.carrie1950868226xt_b_d tptp.carrie1821755406_e_b_f tptp.set_b))
% 152.02/152.37  (declare-const tptp.g (-> tptp.nat tptp.a))
% 152.02/152.37  (declare-const tptp.genera1692266857t_unit (-> tptp.carrie1950868226xt_b_d tptp.carrie1963041556t_unit tptp.set_a Bool))
% 152.02/152.37  (declare-const tptp.m2 tptp.nat)
% 152.02/152.37  (declare-const tptp.generator_b_d_e_f (-> tptp.carrie1950868226xt_b_d tptp.carrie1821755406_e_b_f tptp.set_e Bool))
% 152.02/152.37  (declare-const tptp.hOM_b_1103679019t_unit (-> tptp.carrie1950868226xt_b_d tptp.carrie1963041556t_unit tptp.carrie1963041556t_unit tptp.carrie980467975t_unit))
% 152.02/152.37  (declare-const tptp.hOM_b_796081438it_a_c (-> tptp.carrie1950868226xt_b_d tptp.carrie1963041556t_unit tptp.carrie722926983_a_b_c tptp.carrie980467975t_unit))
% 152.02/152.37  (declare-const tptp.hOM_b_1375846429t_unit (-> tptp.carrie1950868226xt_b_d tptp.carrie1821755406_e_b_f tptp.carrie1963041556t_unit tptp.carrie292259835t_unit))
% 152.02/152.37  (declare-const tptp.module1330273449unit_d (-> tptp.carrie292259835t_unit tptp.carrie1950868226xt_b_d Bool))
% 152.02/152.37  (declare-const tptp.hOM_b_d_e_f_a_c (-> tptp.carrie1950868226xt_b_d tptp.carrie1821755406_e_b_f tptp.carrie722926983_a_b_c tptp.carrie292259835t_unit))
% 152.02/152.37  (declare-const tptp.module241733029unit_d (-> tptp.carrie377329159t_unit tptp.carrie1950868226xt_b_d Bool))
% 152.02/152.37  (declare-const tptp.hOM_b_d_e_f_e_f (-> tptp.carrie1950868226xt_b_d tptp.carrie1821755406_e_b_f tptp.carrie1821755406_e_b_f tptp.carrie377329159t_unit))
% 152.02/152.37  (declare-const tptp.misomo493403663t_unit (-> tptp.carrie1950868226xt_b_d tptp.carrie1963041556t_unit tptp.carrie1963041556t_unit Bool))
% 152.02/152.37  (declare-const tptp.misomo951986689it_e_f (-> tptp.carrie1950868226xt_b_d tptp.carrie1963041556t_unit tptp.carrie1821755406_e_b_f Bool))
% 152.02/152.37  (declare-const tptp.misomo368157697t_unit (-> tptp.carrie1950868226xt_b_d tptp.carrie1821755406_e_b_f tptp.carrie1963041556t_unit Bool))
% 152.02/152.37  (declare-const tptp.module_e_b_f_d (-> tptp.carrie1821755406_e_b_f tptp.carrie1950868226xt_b_d Bool))
% 152.02/152.37  (declare-const tptp.member_nat_a (-> (-> tptp.nat tptp.a) tptp.set_nat_a Bool))
% 152.02/152.37  (declare-const tptp.algebr1152250919_d_a_c (-> tptp.carrie1950868226xt_b_d tptp.carrie722926983_a_b_c tptp.set_a tptp.set_a))
% 152.02/152.37  (declare-const tptp.ord_less_eq_set_e (-> tptp.set_e tptp.set_e Bool))
% 152.02/152.37  (declare-const tptp.bot_bot_set_nat_b tptp.set_nat_b)
% 152.02/152.37  (declare-const tptp.carrie730238621_e_b_f (-> tptp.carrie1821755406_e_b_f tptp.set_e))
% 152.02/152.37  (declare-const tptp.l_comb_b_d_a_c (-> tptp.carrie1950868226xt_b_d tptp.carrie722926983_a_b_c tptp.nat (-> tptp.nat tptp.b) (-> tptp.nat tptp.a) tptp.a))
% 152.02/152.37  (declare-const tptp.algebr168361254_d_e_f (-> tptp.carrie1950868226xt_b_d tptp.carrie1821755406_e_b_f tptp.set_e tptp.set_e))
% 152.02/152.37  (declare-const tptp.member_nat_b (-> (-> tptp.nat tptp.b) tptp.set_nat_b Bool))
% 152.02/152.37  (declare-const tptp.h tptp.set_a)
% 152.02/152.37  (declare-const tptp.free_g637607517t_unit (-> tptp.carrie1950868226xt_b_d tptp.carrie1963041556t_unit tptp.set_a Bool))
% 152.02/152.37  (declare-const tptp.smodul818989740_d_a_c (-> tptp.carrie1950868226xt_b_d tptp.carrie722926983_a_b_c tptp.set_b tptp.set_a))
% 152.02/152.37  (declare-const tptp.module_a_b_c_d (-> tptp.carrie722926983_a_b_c tptp.carrie1950868226xt_b_d Bool))
% 152.02/152.37  (declare-const tptp.algebr1039611956t_unit (-> tptp.carrie1950868226xt_b_d tptp.carrie1963041556t_unit tptp.set_a tptp.set_a))
% 152.02/152.37  (declare-const tptp.misomo1935876354it_a_c (-> tptp.carrie1950868226xt_b_d tptp.carrie1963041556t_unit tptp.carrie722926983_a_b_c Bool))
% 152.02/152.37  (declare-const tptp.ord_le157368549_nat_a (-> tptp.set_nat_a tptp.set_nat_a Bool))
% 152.02/152.37  (declare-const tptp.annihilator_b_d_a_c (-> tptp.carrie1950868226xt_b_d tptp.carrie722926983_a_b_c tptp.set_b))
% 152.02/152.37  (declare-const tptp.member_e (-> tptp.e tptp.set_e Bool))
% 152.02/152.37  (declare-const tptp.l_comb1138968323t_unit (-> tptp.carrie1950868226xt_b_d tptp.carrie1963041556t_unit tptp.nat (-> tptp.nat tptp.b) (-> tptp.nat tptp.a) tptp.a))
% 152.02/152.37  (declare-const tptp.minus_minus_nat (-> tptp.nat tptp.nat tptp.nat))
% 152.02/152.37  (declare-const tptp.pi_nat_a (-> tptp.set_nat (-> tptp.nat tptp.set_a) tptp.set_nat_a))
% 152.02/152.37  (declare-const tptp.ideal_b_d (-> tptp.carrie1950868226xt_b_d tptp.set_b Bool))
% 152.02/152.37  (declare-const tptp.hOM_b_d_a_c_e_f (-> tptp.carrie1950868226xt_b_d tptp.carrie722926983_a_b_c tptp.carrie1821755406_e_b_f tptp.carrie1065537299t_unit))
% 152.02/152.37  (declare-const tptp.collect_nat (-> (-> tptp.nat Bool) tptp.set_nat))
% 152.02/152.37  (declare-const tptp.bot_bot_set_a tptp.set_a)
% 152.02/152.37  (declare-const tptp.ring_b_d (-> tptp.carrie1950868226xt_b_d Bool))
% 152.02/152.37  (declare-const tptp.pi_nat_e (-> tptp.set_nat (-> tptp.nat tptp.set_e) tptp.set_nat_e))
% 152.02/152.37  (declare-const tptp.member_a (-> tptp.a tptp.set_a Bool))
% 152.02/152.37  (declare-const tptp.pi_nat_b (-> tptp.set_nat (-> tptp.nat tptp.set_b) tptp.set_nat_b))
% 152.02/152.37  (declare-const tptp.h2 tptp.a)
% 152.02/152.37  (declare-const tptp.generator_b_d_a_c (-> tptp.carrie1950868226xt_b_d tptp.carrie722926983_a_b_c tptp.set_a Bool))
% 152.02/152.37  (declare-const tptp.submodule_b_d_a_c (-> tptp.carrie1950868226xt_b_d tptp.carrie722926983_a_b_c tptp.set_a Bool))
% 152.02/152.37  (declare-const tptp.quotie1153752712_d_a_c (-> tptp.carrie1950868226xt_b_d tptp.carrie722926983_a_b_c tptp.set_a tptp.set_a tptp.set_b))
% 152.02/152.37  (declare-const tptp.ord_less_eq_set_a (-> tptp.set_a tptp.set_a Bool))
% 152.02/152.37  (declare-const tptp.hOM_b_d_a_c_a_c (-> tptp.carrie1950868226xt_b_d tptp.carrie722926983_a_b_c tptp.carrie722926983_a_b_c tptp.carrie980467975t_unit))
% 152.02/152.37  (declare-const tptp.member_nat (-> tptp.nat tptp.set_nat Bool))
% 152.02/152.37  (declare-const tptp.r tptp.carrie1950868226xt_b_d)
% 152.02/152.37  (declare-const tptp.free_g103796815_d_e_f (-> tptp.carrie1950868226xt_b_d tptp.carrie1821755406_e_b_f tptp.set_e Bool))
% 152.02/152.37  (declare-const tptp.m tptp.carrie722926983_a_b_c)
% 152.02/152.37  (declare-const tptp.free_g1087686480_d_a_c (-> tptp.carrie1950868226xt_b_d tptp.carrie722926983_a_b_c tptp.set_a Bool))
% 152.02/152.37  (declare-const tptp.member_nat_e (-> (-> tptp.nat tptp.e) tptp.set_nat_e Bool))
% 152.02/152.37  (declare-const tptp.annihi259882159t_unit (-> tptp.carrie1950868226xt_b_d tptp.carrie1963041556t_unit tptp.set_b))
% 152.02/152.37  (declare-const tptp.misomo1282343797_c_a_c (-> tptp.carrie1950868226xt_b_d tptp.carrie722926983_a_b_c tptp.carrie722926983_a_b_c Bool))
% 152.02/152.37  (declare-const tptp.carrie1074654371t_unit (-> tptp.carrie1963041556t_unit tptp.set_a))
% 152.02/152.37  (declare-const tptp.module1821517916unit_d (-> tptp.carrie1963041556t_unit tptp.carrie1950868226xt_b_d Bool))
% 152.02/152.37  (declare-const tptp.submodule_b_d_e_f (-> tptp.carrie1950868226xt_b_d tptp.carrie1821755406_e_b_f tptp.set_e Bool))
% 152.02/152.37  (declare-const tptp.submod903911234t_unit (-> tptp.carrie1950868226xt_b_d tptp.carrie1963041556t_unit tptp.set_a Bool))
% 152.02/152.37  (declare-const tptp.l_comb_b_d_e_f (-> tptp.carrie1950868226xt_b_d tptp.carrie1821755406_e_b_f tptp.nat (-> tptp.nat tptp.b) (-> tptp.nat tptp.e) tptp.e))
% 152.02/152.37  (declare-const tptp.bot_bot_set_e tptp.set_e)
% 152.02/152.37  (declare-const tptp.module1648870817unit_d (-> tptp.carrie1065537299t_unit tptp.carrie1950868226xt_b_d Bool))
% 152.02/152.37  (declare-const tptp.module589927589unit_d (-> tptp.carrie980467975t_unit tptp.carrie1950868226xt_b_d Bool))
% 152.02/152.37  (declare-const tptp.hOM_b_717364638t_unit (-> tptp.carrie1950868226xt_b_d tptp.carrie722926983_a_b_c tptp.carrie1963041556t_unit tptp.carrie980467975t_unit))
% 152.02/152.37  (declare-const tptp.carrie2021454486_a_b_c (-> tptp.carrie722926983_a_b_c tptp.set_a))
% 152.02/152.37  (declare-const tptp.zero_zero_nat tptp.nat)
% 152.02/152.37  (declare-const tptp.carrie2079586589xt_b_d (-> tptp.carrie1950868226xt_b_d tptp.set_b))
% 152.02/152.37  (declare-const tptp.suc (-> tptp.nat tptp.nat))
% 152.02/152.37  (declare-const tptp.misomo1752826100_f_a_c (-> tptp.carrie1950868226xt_b_d tptp.carrie1821755406_e_b_f tptp.carrie722926983_a_b_c Bool))
% 152.02/152.37  (declare-const tptp.misomo298454132_c_e_f (-> tptp.carrie1950868226xt_b_d tptp.carrie722926983_a_b_c tptp.carrie1821755406_e_b_f Bool))
% 152.02/152.37  (declare-const tptp.misomo1857159554t_unit (-> tptp.carrie1950868226xt_b_d tptp.carrie722926983_a_b_c tptp.carrie1963041556t_unit Bool))
% 152.02/152.37  (declare-const tptp.hOM_b_1959675421it_e_f (-> tptp.carrie1950868226xt_b_d tptp.carrie1963041556t_unit tptp.carrie1821755406_e_b_f tptp.carrie1065537299t_unit))
% 152.02/152.37  (declare-const tptp.collect_nat_a (-> (-> (-> tptp.nat tptp.a) Bool) tptp.set_nat_a))
% 152.02/152.37  (declare-const tptp.collect_nat_b (-> (-> (-> tptp.nat tptp.b) Bool) tptp.set_nat_b))
% 152.02/152.37  (declare-const tptp.collect_a (-> (-> tptp.a Bool) tptp.set_a))
% 152.02/152.37  (declare-const tptp.misomo768936435_f_e_f (-> tptp.carrie1950868226xt_b_d tptp.carrie1821755406_e_b_f tptp.carrie1821755406_e_b_f Bool))
% 152.02/152.37  (define tptp.ord_less_eq_nat () (let ((_let_1 (@var "N4" tptp.nat))) (let ((_let_2 (@var "M6" tptp.nat))) (lambda (@list _let_2 _let_1) (or (_ (_ tptp.ord_less_nat _let_2) _let_1) (= _let_2 _let_1))))))
% 152.02/152.37  (define @t1 () (_ tptp.carrie2021454486_a_b_c tptp.m))
% 152.02/152.37  (define @t2 () (@var "H2" tptp.a))
% 152.02/152.37  (define @t3 () (_ tptp.member_a @t2))
% 152.02/152.37  (define @t4 () (@var "H" tptp.set_a))
% 152.02/152.37  (define @t5 () (_ @t3 @t4))
% 152.02/152.37  (define @t6 () (_ (_ tptp.submodule_b_d_a_c tptp.r) tptp.m))
% 152.02/152.37  (define @t7 () (_ @t6 @t4))
% 152.02/152.37  (define @t8 () (@list @t4 @t2))
% 152.02/152.37  (define @t9 () (_ tptp.ord_less_eq_set_a @t4))
% 152.02/152.37  (define @t10 () (_ @t9 @t1))
% 152.02/152.37  (define @t11 () (@list @t4))
% 152.02/152.37  (define @t12 () (_ (_ tptp.free_g1087686480_d_a_c tptp.r) tptp.m))
% 152.02/152.37  (define @t13 () (_ @t12 @t4))
% 152.02/152.37  (define @t14 () (@var "A" tptp.set_a))
% 152.02/152.37  (define @t15 () (_ (_ tptp.algebr1152250919_d_a_c tptp.r) tptp.m))
% 152.02/152.37  (define @t16 () (_ @t15 @t14))
% 152.02/152.37  (define @t17 () (@var "X" tptp.a))
% 152.02/152.37  (define @t18 () (_ tptp.member_a @t17))
% 152.02/152.37  (define @t19 () (_ @t18 @t14))
% 152.02/152.37  (define @t20 () (_ tptp.ord_less_eq_set_a @t14))
% 152.02/152.37  (define @t21 () (_ @t20 @t1))
% 152.02/152.37  (define @t22 () (@list @t14))
% 152.02/152.37  (define @t23 () (@var "K" tptp.set_a))
% 152.02/152.37  (define @t24 () (_ @t15 @t23))
% 152.02/152.37  (define @t25 () (@var "J" tptp.set_a))
% 152.02/152.37  (define @t26 () (_ tptp.ord_less_eq_set_a @t23))
% 152.02/152.37  (define @t27 () (_ @t26 @t4))
% 152.02/152.37  (define @t28 () (_ (_ tptp.ord_less_eq_set_a @t25) @t23))
% 152.02/152.37  (define @t29 () (@var "G" (-> tptp.nat tptp.a)))
% 152.02/152.37  (define @t30 () (@var "S" (-> tptp.nat tptp.b)))
% 152.02/152.37  (define @t31 () (@var "N" tptp.nat))
% 152.02/152.37  (define @t32 () (_ (_ tptp.l_comb_b_d_a_c tptp.r) tptp.m))
% 152.02/152.37  (define @t33 () (_ @t32 @t31))
% 152.02/152.37  (define @t34 () (_ @t33 @t30))
% 152.02/152.37  (define @t35 () (@var "F" (-> tptp.nat tptp.a)))
% 152.02/152.37  (define @t36 () (_ @t34 @t35))
% 152.02/152.37  (define @t37 () (= @t36 (_ @t34 @t29)))
% 152.02/152.37  (define @t38 () (@var "X2" tptp.nat))
% 152.02/152.37  (define @t39 () (@var "J2" tptp.nat))
% 152.02/152.37  (define @t40 () (_ tptp.ord_less_eq_nat @t39))
% 152.02/152.37  (define @t41 () (@list @t39))
% 152.02/152.37  (define @t42 () (_ tptp.collect_nat (lambda @t41 (_ @t40 @t31))))
% 152.02/152.37  (define @t43 () (_ (_ tptp.member_nat @t38) @t42))
% 152.02/152.37  (define @t44 () (@list @t38))
% 152.02/152.37  (define @t45 () (forall @t44 (=> @t43 (= (_ @t35 @t38) (_ @t29 @t38)))))
% 152.02/152.37  (define @t46 () (@list (@var "Uu" tptp.nat)))
% 152.02/152.37  (define @t47 () (_ tptp.pi_nat_a @t42))
% 152.02/152.37  (define @t48 () (_ @t47 (lambda @t46 @t4)))
% 152.02/152.37  (define @t49 () (_ (_ tptp.member_nat_a @t29) @t48))
% 152.02/152.37  (define @t50 () (_ tptp.member_nat_a @t35))
% 152.02/152.37  (define @t51 () (_ @t50 @t48))
% 152.02/152.37  (define @t52 () (_ tptp.carrie2079586589xt_b_d tptp.r))
% 152.02/152.37  (define @t53 () (lambda @t46 @t52))
% 152.02/152.37  (define @t54 () (_ tptp.pi_nat_b @t42))
% 152.02/152.37  (define @t55 () (_ tptp.member_nat_b @t30))
% 152.02/152.37  (define @t56 () (_ @t55 (_ @t54 @t53)))
% 152.02/152.37  (define @t57 () (@list @t4 @t30 @t31 @t35 @t29))
% 152.02/152.37  (define @t58 () (@var "M" (-> tptp.nat tptp.a)))
% 152.02/152.37  (define @t59 () (_ @t34 @t58))
% 152.02/152.37  (define @t60 () (_ tptp.member_nat_a @t58))
% 152.02/152.37  (define @t61 () (_ @t60 @t48))
% 152.02/152.37  (define @t62 () (@var "A2" tptp.set_b))
% 152.02/152.37  (define @t63 () (lambda @t46 @t62))
% 152.02/152.37  (define @t64 () (_ @t54 @t63))
% 152.02/152.37  (define @t65 () (_ @t55 @t64))
% 152.02/152.37  (define @t66 () (_ tptp.ideal_b_d tptp.r))
% 152.02/152.37  (define @t67 () (_ @t66 @t62))
% 152.02/152.37  (define @t68 () (@var "M2" (-> tptp.nat tptp.a)))
% 152.02/152.37  (define @t69 () (@var "S2" (-> tptp.nat tptp.b)))
% 152.02/152.37  (define @t70 () (_ (_ tptp.member_nat_b @t69) @t64))
% 152.02/152.37  (define @t71 () (and @t70 (_ (_ tptp.member_nat_a @t68) @t48)))
% 152.02/152.37  (define @t72 () (@list @t69 @t68))
% 152.02/152.37  (define @t73 () (@var "X2" (-> tptp.nat tptp.a)))
% 152.02/152.37  (define @t74 () (@var "Xa" (-> tptp.nat tptp.b)))
% 152.02/152.37  (define @t75 () (@var "N2" tptp.nat))
% 152.02/152.37  (define @t76 () (_ @t32 @t75))
% 152.02/152.37  (define @t77 () (_ tptp.collect_nat (lambda @t41 (_ @t40 @t75))))
% 152.02/152.37  (define @t78 () (_ tptp.pi_nat_b @t77))
% 152.02/152.37  (define @t79 () (_ tptp.member_nat_b @t74))
% 152.02/152.37  (define @t80 () (@list @t74))
% 152.02/152.37  (define @t81 () (lambda @t46 @t23))
% 152.02/152.37  (define @t82 () (_ tptp.pi_nat_a @t77))
% 152.02/152.37  (define @t83 () (_ tptp.member_nat_a @t73))
% 152.02/152.37  (define @t84 () (_ @t83 (_ @t82 @t81)))
% 152.02/152.37  (define @t85 () (@list @t75 @t73))
% 152.02/152.37  (define @t86 () (not (= @t23 tptp.bot_bot_set_a)))
% 152.02/152.37  (define @t87 () (@var "Q" tptp.set_a))
% 152.02/152.37  (define @t88 () (@var "P" tptp.set_a))
% 152.02/152.37  (define @t89 () (_ (_ (_ tptp.smodul818989740_d_a_c tptp.r) tptp.m) @t62))
% 152.02/152.37  (define @t90 () (@list @t62))
% 152.02/152.37  (define @t91 () (@var "Xa" (-> tptp.nat tptp.a)))
% 152.02/152.37  (define @t92 () (@var "X2" (-> tptp.nat tptp.b)))
% 152.02/152.37  (define @t93 () (_ tptp.member_nat_a @t91))
% 152.02/152.37  (define @t94 () (@list @t91))
% 152.02/152.37  (define @t95 () (_ tptp.member_nat_b @t92))
% 152.02/152.37  (define @t96 () (_ @t95 (_ @t78 @t63)))
% 152.02/152.37  (define @t97 () (@list @t75 @t92))
% 152.02/152.37  (define @t98 () (@var "A" tptp.set_e))
% 152.02/152.37  (define @t99 () (@var "M3" tptp.carrie1821755406_e_b_f))
% 152.02/152.37  (define @t100 () (@var "R" tptp.carrie1950868226xt_b_d))
% 152.02/152.37  (define @t101 () (_ (_ tptp.algebr168361254_d_e_f @t100) @t99))
% 152.02/152.37  (define @t102 () (_ @t101 @t98))
% 152.02/152.37  (define @t103 () (@var "X" tptp.e))
% 152.02/152.37  (define @t104 () (_ tptp.member_e @t103))
% 152.02/152.37  (define @t105 () (_ tptp.carrie730238621_e_b_f @t99))
% 152.02/152.37  (define @t106 () (_ (_ tptp.ord_less_eq_set_e @t98) @t105))
% 152.02/152.37  (define @t107 () (_ (_ tptp.module_e_b_f_d @t99) @t100))
% 152.02/152.37  (define @t108 () (@var "M3" tptp.carrie1963041556t_unit))
% 152.02/152.37  (define @t109 () (_ (_ tptp.algebr1039611956t_unit @t100) @t108))
% 152.02/152.37  (define @t110 () (_ @t109 @t14))
% 152.02/152.37  (define @t111 () (_ tptp.carrie1074654371t_unit @t108))
% 152.02/152.37  (define @t112 () (_ @t20 @t111))
% 152.02/152.37  (define @t113 () (_ (_ tptp.module1821517916unit_d @t108) @t100))
% 152.02/152.37  (define @t114 () (@var "M3" tptp.carrie722926983_a_b_c))
% 152.02/152.37  (define @t115 () (_ (_ tptp.algebr1152250919_d_a_c @t100) @t114))
% 152.02/152.37  (define @t116 () (_ @t115 @t14))
% 152.02/152.37  (define @t117 () (_ tptp.carrie2021454486_a_b_c @t114))
% 152.02/152.37  (define @t118 () (_ @t20 @t117))
% 152.02/152.37  (define @t119 () (_ (_ tptp.module_a_b_c_d @t114) @t100))
% 152.02/152.37  (define @t120 () (@var "K" tptp.set_e))
% 152.02/152.37  (define @t121 () (_ @t101 @t120))
% 152.02/152.37  (define @t122 () (@var "J" tptp.set_e))
% 152.02/152.37  (define @t123 () (@var "H" tptp.set_e))
% 152.02/152.37  (define @t124 () (_ tptp.ord_less_eq_set_e @t120))
% 152.02/152.37  (define @t125 () (_ (_ (_ tptp.free_g103796815_d_e_f @t100) @t99) @t123))
% 152.02/152.37  (define @t126 () (_ @t109 @t23))
% 152.02/152.37  (define @t127 () (_ (_ (_ tptp.free_g637607517t_unit @t100) @t108) @t4))
% 152.02/152.37  (define @t128 () (_ @t115 @t23))
% 152.02/152.37  (define @t129 () (_ (_ (_ tptp.free_g1087686480_d_a_c @t100) @t114) @t4))
% 152.02/152.37  (define @t130 () (_ (_ tptp.submodule_b_d_e_f @t100) @t99))
% 152.02/152.37  (define @t131 () (@list @t99 @t100 @t98))
% 152.02/152.37  (define @t132 () (_ (_ tptp.submod903911234t_unit @t100) @t108))
% 152.02/152.37  (define @t133 () (@list @t108 @t100 @t14))
% 152.02/152.37  (define @t134 () (_ (_ tptp.submodule_b_d_a_c @t100) @t114))
% 152.02/152.37  (define @t135 () (@list @t114 @t100 @t14))
% 152.02/152.37  (define @t136 () (@var "X2" (-> tptp.nat tptp.e)))
% 152.02/152.37  (define @t137 () (_ (_ tptp.l_comb_b_d_e_f @t100) @t99))
% 152.02/152.37  (define @t138 () (_ @t137 @t75))
% 152.02/152.37  (define @t139 () (lambda @t46 (_ tptp.carrie2079586589xt_b_d @t100)))
% 152.02/152.37  (define @t140 () (_ @t79 (_ @t78 @t139)))
% 152.02/152.37  (define @t141 () (_ tptp.pi_nat_e @t77))
% 152.02/152.37  (define @t142 () (_ (_ tptp.l_comb1138968323t_unit @t100) @t108))
% 152.02/152.37  (define @t143 () (_ @t142 @t75))
% 152.02/152.37  (define @t144 () (_ (_ tptp.l_comb_b_d_a_c @t100) @t114))
% 152.02/152.37  (define @t145 () (_ @t144 @t75))
% 152.02/152.37  (define @t146 () (_ tptp.misomo1282343797_c_a_c tptp.r))
% 152.02/152.37  (define @t147 () (_ @t146 tptp.m))
% 152.02/152.37  (define @t148 () (@var "N3" tptp.carrie1821755406_e_b_f))
% 152.02/152.37  (define @t149 () (_ tptp.module_e_b_f_d @t148))
% 152.02/152.37  (define @t150 () (_ @t149 tptp.r))
% 152.02/152.37  (define @t151 () (@list @t148))
% 152.02/152.37  (define @t152 () (@var "N3" tptp.carrie722926983_a_b_c))
% 152.02/152.37  (define @t153 () (_ tptp.module_a_b_c_d @t152))
% 152.02/152.37  (define @t154 () (_ @t153 tptp.r))
% 152.02/152.37  (define @t155 () (@list @t152))
% 152.02/152.37  (define @t156 () (@var "N3" tptp.carrie1963041556t_unit))
% 152.02/152.37  (define @t157 () (_ tptp.module1821517916unit_d @t156))
% 152.02/152.37  (define @t158 () (_ @t157 tptp.r))
% 152.02/152.37  (define @t159 () (@list @t156))
% 152.02/152.37  (define @t160 () (_ tptp.suc tptp.zero_zero_nat))
% 152.02/152.37  (define @t161 () (_ tptp.minus_minus_nat @t31))
% 152.02/152.37  (define @t162 () (_ @t161 @t160))
% 152.02/152.37  (define @t163 () (_ tptp.suc @t162))
% 152.02/152.37  (define @t164 () (_ tptp.ord_less_nat tptp.zero_zero_nat))
% 152.02/152.37  (define @t165 () (_ @t164 @t31))
% 152.02/152.37  (define @t166 () (=> @t165 (= @t163 @t31)))
% 152.02/152.37  (define @t167 () (@list @t31))
% 152.02/152.37  (define @t168 () (forall @t167 @t166))
% 152.02/152.37  (define @t169 () (_ (_ tptp.generator_b_d_a_c tptp.r) tptp.m))
% 152.02/152.37  (define @t170 () (_ @t169 @t4))
% 152.02/152.37  (define @t171 () (@var "M" (-> tptp.nat tptp.e)))
% 152.02/152.37  (define @t172 () (_ @t137 @t31))
% 152.02/152.37  (define @t173 () (_ @t172 @t30))
% 152.02/152.37  (define @t174 () (_ (_ tptp.pi_nat_e @t42) (lambda @t46 @t123)))
% 152.02/152.37  (define @t175 () (_ (_ tptp.ord_less_eq_set_e @t123) @t105))
% 152.02/152.37  (define @t176 () (_ tptp.ideal_b_d @t100))
% 152.02/152.37  (define @t177 () (_ @t176 @t62))
% 152.02/152.37  (define @t178 () (_ @t144 @t31))
% 152.02/152.37  (define @t179 () (_ @t178 @t30))
% 152.02/152.37  (define @t180 () (_ @t9 @t117))
% 152.02/152.37  (define @t181 () (_ @t142 @t31))
% 152.02/152.37  (define @t182 () (_ @t181 @t30))
% 152.02/152.37  (define @t183 () (_ @t9 @t111))
% 152.02/152.37  (define @t184 () (@var "M2" (-> tptp.nat tptp.e)))
% 152.02/152.37  (define @t185 () (@var "M" tptp.nat))
% 152.02/152.37  (define @t186 () (_ tptp.ord_less_nat @t185))
% 152.02/152.37  (define @t187 () (_ @t186 @t31))
% 152.02/152.37  (define @t188 () (_ @t161 @t185))
% 152.02/152.37  (define @t189 () (@list @t31 @t185))
% 152.02/152.37  (define @t190 () (@var "G" (-> tptp.nat tptp.e)))
% 152.02/152.37  (define @t191 () (@var "F" (-> tptp.nat tptp.e)))
% 152.02/152.37  (define @t192 () (= (_ @t173 @t191) (_ @t173 @t190)))
% 152.02/152.37  (define @t193 () (forall @t44 (=> @t43 (= (_ @t191 @t38) (_ @t190 @t38)))))
% 152.02/152.37  (define @t194 () (_ (_ tptp.member_nat_e @t190) @t174))
% 152.02/152.37  (define @t195 () (_ (_ tptp.member_nat_e @t191) @t174))
% 152.02/152.37  (define @t196 () (_ @t55 (_ @t54 @t139)))
% 152.02/152.37  (define @t197 () (@list @t99 @t100 @t123 @t30 @t31 @t191 @t190))
% 152.02/152.37  (define @t198 () (= (_ @t179 @t35) (_ @t179 @t29)))
% 152.02/152.37  (define @t199 () (@list @t114 @t100 @t4 @t30 @t31 @t35 @t29))
% 152.02/152.37  (define @t200 () (= (_ @t182 @t35) (_ @t182 @t29)))
% 152.02/152.37  (define @t201 () (@list @t108 @t100 @t4 @t30 @t31 @t35 @t29))
% 152.02/152.37  (define @t202 () (and @t196 @t51 @t49 @t45))
% 152.02/152.37  (define @t203 () (_ tptp.ord_less_eq_nat @t185))
% 152.02/152.37  (define @t204 () (_ @t203 @t31))
% 152.02/152.37  (define @t205 () (_ tptp.minus_minus_nat @t185))
% 152.02/152.37  (define @t206 () (_ @t205 @t31))
% 152.02/152.37  (define @t207 () (= @t206 tptp.zero_zero_nat))
% 152.02/152.37  (define @t208 () (@list @t185 @t31))
% 152.02/152.37  (define @t209 () (@var "Nat2" tptp.nat))
% 152.02/152.37  (define @t210 () (@var "Nat" tptp.nat))
% 152.02/152.37  (define @t211 () (_ tptp.suc @t209))
% 152.02/152.37  (define @t212 () (@var "Y2" tptp.nat))
% 152.02/152.37  (define @t213 () (@var "X22" tptp.nat))
% 152.02/152.37  (define @t214 () (_ tptp.suc @t213))
% 152.02/152.37  (define @t215 () (_ tptp.misomo1752826100_f_a_c tptp.r))
% 152.02/152.37  (define @t216 () (_ tptp.misomo298454132_c_e_f tptp.r))
% 152.02/152.37  (define @t217 () (_ (_ @t216 tptp.m) @t148))
% 152.02/152.37  (define @t218 () (_ tptp.misomo1935876354it_a_c tptp.r))
% 152.02/152.37  (define @t219 () (_ tptp.misomo1857159554t_unit tptp.r))
% 152.02/152.37  (define @t220 () (_ (_ @t219 tptp.m) @t156))
% 152.02/152.37  (define @t221 () (_ @t147 @t152))
% 152.02/152.37  (define @t222 () (_ tptp.ord_less_eq_nat @t31))
% 152.02/152.37  (define @t223 () (_ @t222 @t185))
% 152.02/152.37  (define @t224 () (_ tptp.suc @t185))
% 152.02/152.37  (define @t225 () (_ tptp.suc @t31))
% 152.02/152.37  (define @t226 () (_ tptp.ord_less_eq_nat @t225))
% 152.02/152.37  (define @t227 () (@var "A" tptp.nat))
% 152.02/152.37  (define @t228 () (_ tptp.ord_less_eq_nat tptp.zero_zero_nat))
% 152.02/152.37  (define @t229 () (@list @t227))
% 152.02/152.37  (define @t230 () (_ tptp.ord_less_nat @t224))
% 152.02/152.37  (define @t231 () (_ @t230 @t225))
% 152.02/152.37  (define @t232 () (@var "A" (-> tptp.nat tptp.a)))
% 152.02/152.37  (define @t233 () (@var "P" (-> (-> tptp.nat tptp.a) Bool)))
% 152.02/152.37  (define @t234 () (_ tptp.member_nat_a @t232))
% 152.02/152.37  (define @t235 () (@var "A" (-> tptp.nat tptp.b)))
% 152.02/152.37  (define @t236 () (@var "P" (-> (-> tptp.nat tptp.b) Bool)))
% 152.02/152.37  (define @t237 () (_ tptp.member_nat_b @t235))
% 152.02/152.37  (define @t238 () (@var "A" tptp.a))
% 152.02/152.37  (define @t239 () (@var "P" (-> tptp.a Bool)))
% 152.02/152.37  (define @t240 () (_ tptp.collect_a @t239))
% 152.02/152.37  (define @t241 () (_ tptp.member_a @t238))
% 152.02/152.37  (define @t242 () (@var "P" (-> tptp.nat Bool)))
% 152.02/152.37  (define @t243 () (_ tptp.collect_nat @t242))
% 152.02/152.37  (define @t244 () (@var "A2" tptp.set_nat_a))
% 152.02/152.37  (define @t245 () (@var "X3" (-> tptp.nat tptp.a)))
% 152.02/152.37  (define @t246 () (_ (_ tptp.member_nat_a @t245) @t244))
% 152.02/152.37  (define @t247 () (@list @t245))
% 152.02/152.37  (define @t248 () (@list @t244))
% 152.02/152.37  (define @t249 () (@var "A2" tptp.set_nat_b))
% 152.02/152.37  (define @t250 () (@var "X3" (-> tptp.nat tptp.b)))
% 152.02/152.37  (define @t251 () (_ (_ tptp.member_nat_b @t250) @t249))
% 152.02/152.37  (define @t252 () (@list @t250))
% 152.02/152.37  (define @t253 () (@list @t249))
% 152.02/152.37  (define @t254 () (@var "A2" tptp.set_a))
% 152.02/152.37  (define @t255 () (@var "X3" tptp.a))
% 152.02/152.37  (define @t256 () (_ (_ tptp.member_a @t255) @t254))
% 152.02/152.37  (define @t257 () (@list @t255))
% 152.02/152.37  (define @t258 () (@list @t254))
% 152.02/152.37  (define @t259 () (@var "A2" tptp.set_nat))
% 152.02/152.37  (define @t260 () (@var "X3" tptp.nat))
% 152.02/152.37  (define @t261 () (@list @t260))
% 152.02/152.37  (define @t262 () (@var "Q" (-> tptp.nat Bool)))
% 152.02/152.37  (define @t263 () (_ @t242 @t38))
% 152.02/152.37  (define @t264 () (= @t227 tptp.zero_zero_nat))
% 152.02/152.37  (define @t265 () (_ tptp.ord_less_nat @t31))
% 152.02/152.37  (define @t266 () (= @t31 tptp.zero_zero_nat))
% 152.02/152.37  (define @t267 () (not @t266))
% 152.02/152.37  (define @t268 () (@var "I" tptp.nat))
% 152.02/152.37  (define @t269 () (_ tptp.ord_less_eq_nat @t268))
% 152.02/152.37  (define @t270 () (@var "K2" tptp.nat))
% 152.02/152.37  (define @t271 () (_ tptp.minus_minus_nat @t224))
% 152.02/152.37  (define @t272 () (_ @t271 @t31))
% 152.02/152.37  (define @t273 () (@list @t185))
% 152.02/152.37  (define @t274 () (_ tptp.minus_minus_nat tptp.zero_zero_nat))
% 152.02/152.37  (define @t275 () (@var "L" tptp.carrie1821755406_e_b_f))
% 152.02/152.37  (define @t276 () (_ @t215 @t275))
% 152.02/152.37  (define @t277 () (_ @t276 tptp.m))
% 152.02/152.37  (define @t278 () (_ tptp.module_e_b_f_d @t275))
% 152.02/152.37  (define @t279 () (_ @t278 tptp.r))
% 152.02/152.37  (define @t280 () (@var "L" tptp.carrie1963041556t_unit))
% 152.02/152.37  (define @t281 () (_ @t218 @t280))
% 152.02/152.37  (define @t282 () (_ @t281 tptp.m))
% 152.02/152.37  (define @t283 () (_ tptp.module1821517916unit_d @t280))
% 152.02/152.37  (define @t284 () (_ @t283 tptp.r))
% 152.02/152.37  (define @t285 () (@var "L" tptp.carrie722926983_a_b_c))
% 152.02/152.37  (define @t286 () (_ @t146 @t285))
% 152.02/152.37  (define @t287 () (_ @t286 tptp.m))
% 152.02/152.37  (define @t288 () (_ tptp.module_a_b_c_d @t285))
% 152.02/152.37  (define @t289 () (_ @t288 tptp.r))
% 152.02/152.37  (define @t290 () (_ @t149 @t100))
% 152.02/152.37  (define @t291 () (@list @t99 @t100 @t148))
% 152.02/152.37  (define @t292 () (_ @t153 @t100))
% 152.02/152.37  (define @t293 () (@list @t99 @t100 @t152))
% 152.02/152.37  (define @t294 () (_ @t157 @t100))
% 152.02/152.37  (define @t295 () (@list @t99 @t100 @t156))
% 152.02/152.37  (define @t296 () (@list @t114 @t100 @t148))
% 152.02/152.37  (define @t297 () (@list @t114 @t100 @t152))
% 152.02/152.37  (define @t298 () (@list @t114 @t100 @t156))
% 152.02/152.37  (define @t299 () (@list @t108 @t100 @t148))
% 152.02/152.37  (define @t300 () (@list @t108 @t100 @t152))
% 152.02/152.37  (define @t301 () (@list @t108 @t100 @t156))
% 152.02/152.37  (define @t302 () (_ tptp.misomo768936435_f_e_f @t100))
% 152.02/152.37  (define @t303 () (_ @t302 @t275))
% 152.02/152.37  (define @t304 () (_ @t303 @t148))
% 152.02/152.37  (define @t305 () (_ @t302 @t99))
% 152.02/152.37  (define @t306 () (_ @t305 @t148))
% 152.02/152.37  (define @t307 () (_ @t303 @t99))
% 152.02/152.37  (define @t308 () (_ @t278 @t100))
% 152.02/152.37  (define @t309 () (_ tptp.misomo1752826100_f_a_c @t100))
% 152.02/152.37  (define @t310 () (_ @t309 @t275))
% 152.02/152.37  (define @t311 () (_ (_ @t309 @t99) @t152))
% 152.02/152.37  (define @t312 () (_ tptp.misomo368157697t_unit @t100))
% 152.02/152.37  (define @t313 () (_ (_ @t312 @t275) @t156))
% 152.02/152.37  (define @t314 () (_ (_ @t312 @t99) @t156))
% 152.02/152.37  (define @t315 () (_ tptp.misomo298454132_c_e_f @t100))
% 152.02/152.37  (define @t316 () (_ @t315 @t285))
% 152.02/152.37  (define @t317 () (_ @t316 @t99))
% 152.02/152.37  (define @t318 () (_ @t288 @t100))
% 152.02/152.37  (define @t319 () (_ tptp.misomo1857159554t_unit @t100))
% 152.02/152.37  (define @t320 () (_ tptp.misomo951986689it_e_f @t100))
% 152.02/152.37  (define @t321 () (_ @t320 @t280))
% 152.02/152.37  (define @t322 () (_ @t321 @t99))
% 152.02/152.37  (define @t323 () (_ @t283 @t100))
% 152.02/152.37  (define @t324 () (_ tptp.misomo1935876354it_a_c @t100))
% 152.02/152.37  (define @t325 () (_ tptp.misomo493403663t_unit @t100))
% 152.02/152.37  (define @t326 () (_ (_ @t315 @t114) @t148))
% 152.02/152.37  (define @t327 () (_ @t310 @t114))
% 152.02/152.37  (define @t328 () (_ (_ @t319 @t114) @t156))
% 152.02/152.37  (define @t329 () (@list @t99 @t100))
% 152.02/152.37  (define @t330 () (_ @t325 @t108))
% 152.02/152.37  (define @t331 () (@list @t108 @t100))
% 152.02/152.37  (define @t332 () (_ tptp.misomo1282343797_c_a_c @t100))
% 152.02/152.37  (define @t333 () (_ @t332 @t114))
% 152.02/152.37  (define @t334 () (@list @t114 @t100))
% 152.02/152.37  (define @t335 () (_ (_ (_ tptp.generator_b_d_e_f @t100) @t99) @t123))
% 152.02/152.37  (define @t336 () (@list @t99 @t100 @t123))
% 152.02/152.37  (define @t337 () (_ (_ (_ tptp.genera1692266857t_unit @t100) @t108) @t4))
% 152.02/152.37  (define @t338 () (@list @t108 @t100 @t4))
% 152.02/152.37  (define @t339 () (_ (_ (_ tptp.generator_b_d_a_c @t100) @t114) @t4))
% 152.02/152.37  (define @t340 () (@list @t114 @t100 @t4))
% 152.02/152.37  (define @t341 () (@var "Y3" tptp.nat))
% 152.02/152.37  (define @t342 () (_ tptp.ord_less_eq_nat @t341))
% 152.02/152.37  (define @t343 () (@list @t341))
% 152.02/152.37  (define @t344 () (@var "B" tptp.nat))
% 152.02/152.37  (define @t345 () (@var "Y" tptp.nat))
% 152.02/152.37  (define @t346 () (@list @t345))
% 152.02/152.37  (define @t347 () (_ @t242 @t270))
% 152.02/152.37  (define @t348 () (= @t185 @t31))
% 152.02/152.37  (define @t349 () (@var "J3" tptp.nat))
% 152.02/152.37  (define @t350 () (=> (_ (_ tptp.ord_less_eq_nat @t349) @t270) (_ @t269 @t270)))
% 152.02/152.37  (define @t351 () (_ @t269 @t349))
% 152.02/152.37  (define @t352 () (=> @t351 @t350))
% 152.02/152.37  (define @t353 () (@list @t268 @t349 @t270))
% 152.02/152.37  (define @t354 () (forall @t353 @t352))
% 152.02/152.37  (define @t355 () (@var "Y4" tptp.nat))
% 152.02/152.37  (define @t356 () (@var "X" tptp.nat))
% 152.02/152.37  (define @t357 () (= @t356 @t355))
% 152.02/152.37  (define @t358 () (@list @t356 @t355))
% 152.02/152.37  (define @t359 () (_ @t242 @t31))
% 152.02/152.37  (define @t360 () (@var "M2" tptp.nat))
% 152.02/152.37  (define @t361 () (_ @t242 @t360))
% 152.02/152.37  (define @t362 () (_ (_ tptp.ord_less_nat @t360) @t75))
% 152.02/152.37  (define @t363 () (@list @t360))
% 152.02/152.37  (define @t364 () (_ @t242 @t75))
% 152.02/152.37  (define @t365 () (=> (not @t364) (exists @t363 (and @t362 (not @t361)))))
% 152.02/152.37  (define @t366 () (@list @t75))
% 152.02/152.37  (define @t367 () (@list @t242 @t31))
% 152.02/152.37  (define @t368 () (@var "T" tptp.nat))
% 152.02/152.37  (define @t369 () (@var "S" tptp.nat))
% 152.02/152.37  (define @t370 () (not @t348))
% 152.02/152.37  (define @t371 () (_ @t265 @t185))
% 152.02/152.37  (define @t372 () (_ tptp.minus_minus_nat @t268))
% 152.02/152.37  (define @t373 () (_ (_ (_ tptp.smodul1982583723_d_e_f @t100) @t99) @t62))
% 152.02/152.37  (define @t374 () (_ (_ (_ tptp.smodul132175289t_unit @t100) @t108) @t62))
% 152.02/152.37  (define @t375 () (_ (_ (_ tptp.smodul818989740_d_a_c @t100) @t114) @t62))
% 152.02/152.37  (define @t376 () (@var "Q" tptp.set_e))
% 152.02/152.37  (define @t377 () (@var "P" tptp.set_e))
% 152.02/152.37  (define @t378 () (@var "R" (-> tptp.nat tptp.nat Bool)))
% 152.02/152.37  (define @t379 () (_ tptp.suc @t75))
% 152.02/152.37  (define @t380 () (@var "Z" tptp.nat))
% 152.02/152.37  (define @t381 () (_ @t378 @t38))
% 152.02/152.37  (define @t382 () (_ @t242 @t379))
% 152.02/152.37  (define @t383 () (=> @t364 @t382))
% 152.02/152.37  (define @t384 () (not @t204))
% 152.02/152.37  (define @t385 () (= @t384 (_ @t226 @t185)))
% 152.02/152.37  (define @t386 () (forall @t208 @t385))
% 152.02/152.37  (define @t387 () (= @t185 @t225))
% 152.02/152.37  (define @t388 () (_ @t203 @t225))
% 152.02/152.37  (define @t389 () (@var "M5" tptp.nat))
% 152.02/152.37  (define @t390 () (_ tptp.suc @t389))
% 152.02/152.37  (define @t391 () (@var "M4" tptp.nat))
% 152.02/152.37  (define @t392 () (@list @t389))
% 152.02/152.37  (define @t393 () (_ (_ tptp.ord_less_eq_nat @t224) @t31))
% 152.02/152.37  (define @t394 () (_ tptp.ord_less_eq_nat @t227))
% 152.02/152.37  (define @t395 () (_ @t394 tptp.zero_zero_nat))
% 152.02/152.37  (define @t396 () (exists @t392 (= @t31 @t390)))
% 152.02/152.37  (define @t397 () (@var "Nat3" tptp.nat))
% 152.02/152.37  (define @t398 () (_ tptp.suc @t397))
% 152.02/152.37  (define @t399 () (@list @t397))
% 152.02/152.37  (define @t400 () (_ @t242 tptp.zero_zero_nat))
% 152.02/152.37  (define @t401 () (=> @t382 @t364))
% 152.02/152.37  (define @t402 () (forall @t366 @t401))
% 152.02/152.37  (define @t403 () (@var "P" (-> tptp.nat tptp.nat Bool)))
% 152.02/152.37  (define @t404 () (_ tptp.suc @t345))
% 152.02/152.37  (define @t405 () (_ @t403 @t38))
% 152.02/152.37  (define @t406 () (@list @t209))
% 152.02/152.37  (define @t407 () (@var "F" (-> tptp.nat tptp.nat)))
% 152.02/152.37  (define @t408 () (@var "J4" tptp.nat))
% 152.02/152.37  (define @t409 () (@var "I2" tptp.nat))
% 152.02/152.37  (define @t410 () (_ tptp.ord_less_nat @t409))
% 152.02/152.37  (define @t411 () (_ @t410 @t408))
% 152.02/152.37  (define @t412 () (or @t187 @t348))
% 152.02/152.37  (define @t413 () (@var "N4" tptp.nat))
% 152.02/152.37  (define @t414 () (@var "M6" tptp.nat))
% 152.02/152.37  (define @t415 () (= @t414 @t413))
% 152.02/152.37  (define @t416 () (@list @t414 @t413))
% 152.02/152.37  (define @t417 () (= @t31 @t185))
% 152.02/152.37  (define @t418 () (_ @t265 @t224))
% 152.02/152.37  (define @t419 () (= @t418 @t417))
% 152.02/152.37  (define @t420 () (not @t371))
% 152.02/152.37  (define @t421 () (_ @t242 @t268))
% 152.02/152.37  (define @t422 () (_ @t242 @t409))
% 152.02/152.37  (define @t423 () (_ tptp.suc @t409))
% 152.02/152.37  (define @t424 () (@list @t409))
% 152.02/152.37  (define @t425 () (_ tptp.ord_less_nat @t268))
% 152.02/152.37  (define @t426 () (_ @t425 @t349))
% 152.02/152.37  (define @t427 () (@list @t268 @t349 @t242))
% 152.02/152.37  (define @t428 () (@var "K3" tptp.nat))
% 152.02/152.37  (define @t429 () (_ @t403 @t409))
% 152.02/152.37  (define @t430 () (_ tptp.suc @t268))
% 152.02/152.37  (define @t431 () (_ (_ tptp.ord_less_nat @t430) @t270))
% 152.02/152.37  (define @t432 () (_ tptp.ord_less_nat @t349))
% 152.02/152.37  (define @t433 () (_ @t432 @t270))
% 152.02/152.37  (define @t434 () (@var "M7" tptp.nat))
% 152.02/152.37  (define @t435 () (_ tptp.ord_less_nat @t225))
% 152.02/152.37  (define @t436 () (_ @t435 @t185))
% 152.02/152.37  (define @t437 () (@var "I3" tptp.nat))
% 152.02/152.37  (define @t438 () (_ @t242 @t437))
% 152.02/152.37  (define @t439 () (_ tptp.ord_less_nat @t437))
% 152.02/152.37  (define @t440 () (_ @t439 @t31))
% 152.02/152.37  (define @t441 () (@list @t437))
% 152.02/152.37  (define @t442 () (_ @t439 @t225))
% 152.02/152.37  (define @t443 () (forall @t441 (=> @t442 @t438)))
% 152.02/152.37  (define @t444 () (@list @t31 @t242))
% 152.02/152.37  (define @t445 () (not @t187))
% 152.02/152.37  (define @t446 () (_ @t186 @t225))
% 152.02/152.37  (define @t447 () (and @t440 @t438))
% 152.02/152.37  (define @t448 () (exists @t441 @t447))
% 152.02/152.37  (define @t449 () (or @t359 @t448))
% 152.02/152.37  (define @t450 () (and @t442 @t438))
% 152.02/152.37  (define @t451 () (exists @t441 @t450))
% 152.02/152.37  (define @t452 () (= @t451 @t449))
% 152.02/152.37  (define @t453 () (forall @t444 @t452))
% 152.02/152.37  (define @t454 () (_ @t230 @t31))
% 152.02/152.37  (define @t455 () (not (forall (@list @t408) (=> (_ @t425 @t408) (not (= @t270 (_ tptp.suc @t408)))))))
% 152.02/152.37  (define @t456 () (@list @t268 @t270))
% 152.02/152.37  (define @t457 () (_ @t425 @t270))
% 152.02/152.37  (define @t458 () (_ tptp.ord_less_nat @t227))
% 152.02/152.37  (define @t459 () (not @t165))
% 152.02/152.37  (define @t460 () (@var "L2" tptp.nat))
% 152.02/152.37  (define @t461 () (_ tptp.minus_minus_nat @t460))
% 152.02/152.37  (define @t462 () (_ @t461 @t185))
% 152.02/152.37  (define @t463 () (_ @t461 @t31))
% 152.02/152.37  (define @t464 () (@list @t185 @t31 @t460))
% 152.02/152.37  (define @t465 () (_ tptp.ord_less_eq_nat @t344))
% 152.02/152.37  (define @t466 () (@var "C" tptp.nat))
% 152.02/152.37  (define @t467 () (_ tptp.minus_minus_nat @t466))
% 152.02/152.37  (define @t468 () (_ @t161 @t270))
% 152.02/152.37  (define @t469 () (_ @t205 @t270))
% 152.02/152.37  (define @t470 () (_ tptp.ord_less_eq_nat @t270))
% 152.02/152.37  (define @t471 () (_ @t470 @t31))
% 152.02/152.37  (define @t472 () (_ @t470 @t185))
% 152.02/152.37  (define @t473 () (@list @t270 @t185 @t31))
% 152.02/152.37  (define @t474 () (_ tptp.ring_b_d @t100))
% 152.02/152.37  (define @t475 () (@var "Xa" (-> tptp.nat tptp.e)))
% 152.02/152.37  (define @t476 () (_ @t407 @t31))
% 152.02/152.37  (define @t477 () (@var "N5" tptp.nat))
% 152.02/152.37  (define @t478 () (_ @t407 @t477))
% 152.02/152.37  (define @t479 () (_ @t222 @t477))
% 152.02/152.37  (define @t480 () (_ @t407 @t75))
% 152.02/152.37  (define @t481 () (_ @t407 @t379))
% 152.02/152.37  (define @t482 () (@list @t407 @t31 @t477))
% 152.02/152.37  (define @t483 () (@var "F" (-> tptp.nat tptp.set_a)))
% 152.02/152.37  (define @t484 () (_ @t483 @t31))
% 152.02/152.37  (define @t485 () (_ @t483 @t477))
% 152.02/152.37  (define @t486 () (_ @t483 @t75))
% 152.02/152.37  (define @t487 () (_ @t483 @t379))
% 152.02/152.37  (define @t488 () (@list @t483 @t31 @t477))
% 152.02/152.37  (define @t489 () (_ tptp.ord_less_nat @t476))
% 152.02/152.37  (define @t490 () (forall @t366 (_ (_ tptp.ord_less_nat @t480) @t481)))
% 152.02/152.37  (define @t491 () (=> @t204 @t446))
% 152.02/152.37  (define @t492 () (forall @t208 @t491))
% 152.02/152.37  (define @t493 () (@var "__flatten_var_0" tptp.nat))
% 152.02/152.37  (define @t494 () (_ (_ tptp.ord_less_nat @t75) @t349))
% 152.02/152.37  (define @t495 () (_ @t269 @t75))
% 152.02/152.37  (define @t496 () (_ @t242 @t349))
% 152.02/152.37  (define @t497 () (@var "I4" tptp.nat))
% 152.02/152.37  (define @t498 () (not (_ @t242 @t497)))
% 152.02/152.37  (define @t499 () (@list @t497))
% 152.02/152.37  (define @t500 () (@list @t428))
% 152.02/152.37  (define @t501 () (not @t400))
% 152.02/152.37  (define @t502 () (_ @t242 (_ tptp.suc @t437)))
% 152.02/152.37  (define @t503 () (_ tptp.minus_minus_nat @t227))
% 152.02/152.37  (define @t504 () (_ tptp.ord_less_nat @t206))
% 152.02/152.37  (define @t505 () (@var "H2" tptp.e))
% 152.02/152.37  (define @t506 () (_ tptp.member_e @t505))
% 152.02/152.37  (define @t507 () (_ @t130 @t123))
% 152.02/152.37  (define @t508 () (_ @t134 @t4))
% 152.02/152.37  (define @t509 () (_ @t132 @t4))
% 152.02/152.37  (define @t510 () (_ tptp.mdl_a_b_c tptp.m))
% 152.02/152.37  (define @t511 () (= (_ (_ (_ (_ (_ tptp.l_comb1138968323t_unit tptp.r) (_ @t510 @t24)) @t31) @t30) @t35) @t36))
% 152.02/152.37  (define @t512 () (_ @t50 (_ @t47 @t81)))
% 152.02/152.37  (define @t513 () (@list @t4 @t23 @t35 @t31 @t30))
% 152.02/152.37  (define @t514 () (@var "B" tptp.a))
% 152.02/152.37  (define @t515 () (_ tptp.insert_a @t514))
% 152.02/152.37  (define @t516 () (_ @t515 tptp.bot_bot_set_a))
% 152.02/152.37  (define @t517 () (_ tptp.ord_less_eq_set_a @t254))
% 152.02/152.37  (define @t518 () (= @t238 @t514))
% 152.02/152.37  (define @t519 () (and @t518 (_ @t517 @t516)))
% 152.02/152.37  (define @t520 () (_ tptp.insert_a @t238))
% 152.02/152.37  (define @t521 () (_ @t520 @t254))
% 152.02/152.37  (define @t522 () (_ (_ tptp.linear_span_b_d_a_c tptp.r) tptp.m))
% 152.02/152.37  (define @t523 () (_ @t522 @t62))
% 152.02/152.37  (define @t524 () (_ @t523 @t4))
% 152.02/152.37  (define @t525 () (_ (_ tptp.member_a @t36) @t524))
% 152.02/152.37  (define @t526 () (_ @t522 @t52))
% 152.02/152.37  (define @t527 () (_ @t526 @t4))
% 152.02/152.37  (define @t528 () (_ @t50 (_ @t47 (lambda @t46 @t527))))
% 152.02/152.37  (define @t529 () (@list @t62 @t4 @t30 @t31 @t35))
% 152.02/152.37  (define @t530 () (_ tptp.zero_a1261444626_a_b_c tptp.m))
% 152.02/152.37  (define @t531 () (= @t59 @t530))
% 152.02/152.37  (define @t532 () (_ (_ tptp.insert_a @t530) tptp.bot_bot_set_a))
% 152.02/152.37  (define @t533 () (_ @t60 (_ @t47 (lambda @t46 @t532))))
% 152.02/152.37  (define @t534 () (@list @t62 @t30 @t31 @t58))
% 152.02/152.37  (define @t535 () (_ tptp.member_a @t530))
% 152.02/152.37  (define @t536 () (@var "B2" tptp.set_a))
% 152.02/152.37  (define @t537 () (= @t254 @t536))
% 152.02/152.37  (define @t538 () (_ @t517 @t536))
% 152.02/152.37  (define @t539 () (@list @t254 @t536))
% 152.02/152.37  (define @t540 () (@var "B2" tptp.set_nat_a))
% 152.02/152.37  (define @t541 () (_ (_ tptp.ord_le157368549_nat_a @t244) @t540))
% 152.02/152.37  (define @t542 () (@var "B2" tptp.set_nat_b))
% 152.02/152.37  (define @t543 () (_ (_ tptp.ord_le1296932838_nat_b @t249) @t542))
% 152.02/152.37  (define @t544 () (@var "X2" tptp.a))
% 152.02/152.37  (define @t545 () (_ tptp.member_a @t544))
% 152.02/152.37  (define @t546 () (_ tptp.minus_minus_set_a @t254))
% 152.02/152.37  (define @t547 () (@var "C" (-> tptp.nat tptp.a)))
% 152.02/152.37  (define @t548 () (@var "C" (-> tptp.nat tptp.b)))
% 152.02/152.37  (define @t549 () (@var "C" tptp.a))
% 152.02/152.37  (define @t550 () (= @t254 tptp.bot_bot_set_a))
% 152.02/152.37  (define @t551 () (forall @t261 (not (_ @t242 @t260))))
% 152.02/152.37  (define @t552 () (@list @t242))
% 152.02/152.37  (define @t553 () (forall @t257 (not (_ @t239 @t255))))
% 152.02/152.37  (define @t554 () (@list @t239))
% 152.02/152.37  (define @t555 () (_ tptp.minus_1788767276_nat_a @t244))
% 152.02/152.37  (define @t556 () (_ @t555 @t540))
% 152.02/152.37  (define @t557 () (@var "X" (-> tptp.nat tptp.a)))
% 152.02/152.37  (define @t558 () (_ tptp.insert_nat_a @t557))
% 152.02/152.37  (define @t559 () (_ tptp.member_nat_a @t557))
% 152.02/152.37  (define @t560 () (@list @t557 @t244 @t540))
% 152.02/152.37  (define @t561 () (_ tptp.minus_780847917_nat_b @t249))
% 152.02/152.37  (define @t562 () (_ @t561 @t542))
% 152.02/152.37  (define @t563 () (@var "X" (-> tptp.nat tptp.b)))
% 152.02/152.37  (define @t564 () (_ tptp.insert_nat_b @t563))
% 152.02/152.37  (define @t565 () (_ tptp.member_nat_b @t563))
% 152.02/152.37  (define @t566 () (@list @t563 @t249 @t542))
% 152.02/152.37  (define @t567 () (_ @t546 @t536))
% 152.02/152.37  (define @t568 () (_ tptp.insert_a @t17))
% 152.02/152.37  (define @t569 () (@list @t17 @t254 @t536))
% 152.02/152.37  (define @t570 () (_ @t558 @t244))
% 152.02/152.37  (define @t571 () (_ @t559 @t540))
% 152.02/152.37  (define @t572 () (_ @t564 @t249))
% 152.02/152.37  (define @t573 () (_ @t565 @t542))
% 152.02/152.37  (define @t574 () (_ @t568 @t254))
% 152.02/152.37  (define @t575 () (_ @t18 @t536))
% 152.02/152.37  (define @t576 () (@var "B" (-> tptp.nat tptp.a)))
% 152.02/152.37  (define @t577 () (_ tptp.insert_nat_a @t576))
% 152.02/152.37  (define @t578 () (= @t232 @t576))
% 152.02/152.37  (define @t579 () (@var "B" (-> tptp.nat tptp.b)))
% 152.02/152.37  (define @t580 () (_ tptp.insert_nat_b @t579))
% 152.02/152.37  (define @t581 () (= @t235 @t579))
% 152.02/152.37  (define @t582 () (_ @t510 @t4))
% 152.02/152.37  (define @t583 () (@var "N3" tptp.set_a))
% 152.02/152.37  (define @t584 () (_ @t9 @t583))
% 152.02/152.37  (define @t585 () (_ @t6 @t583))
% 152.02/152.37  (define @t586 () (_ tptp.ord_less_eq_set_a @t524))
% 152.02/152.37  (define @t587 () (@list @t62 @t4))
% 152.02/152.37  (define @t588 () (_ @t520 tptp.bot_bot_set_a))
% 152.02/152.37  (define @t589 () (@list @t238))
% 152.02/152.37  (define @t590 () (@var "H1" tptp.set_a))
% 152.02/152.37  (define @t591 () (_ tptp.insert_a tptp.h2))
% 152.02/152.37  (define @t592 () (_ @t591 tptp.h1))
% 152.02/152.37  (define @t593 () (@var "K4" tptp.nat))
% 152.02/152.37  (define @t594 () (_ tptp.collect_nat (lambda (@list @t593) (_ (_ tptp.ord_less_eq_nat @t593) tptp.m2))))
% 152.02/152.37  (define @t595 () (@var "X4" tptp.nat))
% 152.02/152.37  (define @t596 () (_ tptp.g @t341))
% 152.02/152.37  (define @t597 () (_ tptp.g @t595))
% 152.02/152.37  (define @t598 () (= @t597 @t596))
% 152.02/152.37  (define @t599 () (=> @t598 (= @t595 @t341)))
% 152.02/152.37  (define @t600 () (=> (_ @t342 tptp.m2) @t599))
% 152.02/152.37  (define @t601 () (forall @t343 @t600))
% 152.02/152.37  (define @t602 () (=> (_ (_ tptp.ord_less_eq_nat @t595) tptp.m2) @t601))
% 152.02/152.37  (define @t603 () (@list @t595))
% 152.02/152.37  (define @t604 () (forall @t603 @t602))
% 152.02/152.37  (define @t605 () (_ tptp.g tptp.m2))
% 152.02/152.37  (define @t606 () (_ tptp.ord_less_eq_set_a tptp.h1))
% 152.02/152.37  (define @t607 () (_ (_ (_ @t32 tptp.m2) tptp.t) tptp.g))
% 152.02/152.37  (define @t608 () (_ tptp.member_a tptp.h2))
% 152.02/152.37  (define @t609 () (_ @t164 tptp.m2))
% 152.02/152.37  (define @t610 () (_ (_ tptp.minus_minus_nat tptp.m2) @t160))
% 152.02/152.37  (define @t611 () (_ tptp.g tptp.xa))
% 152.02/152.37  (define @t612 () (_ (_ tptp.member_a @t611) tptp.h1))
% 152.02/152.37  (define @t613 () (or (= @t611 tptp.h2) @t612))
% 152.02/152.37  (define @t614 () (not @t612))
% 152.02/152.37  (define @t615 () (lambda @t416 (or (_ (_ tptp.ord_less_nat @t414) @t413) @t415)))
% 152.02/152.37  (define @t616 () (@const 0 (@ho-elim-sort (-> tptp.nat tptp.nat))))
% 152.02/152.37  (define @t617 () (@const 1 (-> (@ho-elim-sort (-> tptp.nat tptp.nat)) tptp.nat tptp.nat)))
% 152.02/152.37  (define @t618 () (_ @t617 @t616 tptp.zero_zero_nat))
% 152.02/152.37  (define @t619 () (@const 2 (@ho-elim-sort (-> tptp.nat tptp.nat tptp.nat))))
% 152.02/152.37  (define @t620 () (@const 3 (-> (@ho-elim-sort (-> tptp.nat tptp.nat tptp.nat)) tptp.nat (@ho-elim-sort (-> tptp.nat tptp.nat)))))
% 152.02/152.37  (define @t621 () (@const 4 (@ho-elim-sort (-> tptp.nat tptp.nat Bool))))
% 152.02/152.37  (define @t622 () (@const 5 (-> (@ho-elim-sort (-> tptp.nat tptp.nat Bool)) tptp.nat (@ho-elim-sort (-> tptp.nat Bool)))))
% 152.02/152.37  (define @t623 () (_ @t622 @t621 tptp.zero_zero_nat))
% 152.02/152.37  (define @t624 () (@const 6 (-> (@ho-elim-sort (-> tptp.nat Bool)) tptp.nat Bool)))
% 152.02/152.37  (define @t625 () (tptp.suc tptp.zero_zero_nat))
% 152.02/152.37  (define @t626 () (tptp.minus_minus_nat @t31 @t625))
% 152.02/152.37  (define @t627 () (tptp.suc @t626))
% 152.02/152.37  (define @t628 () (tptp.ord_less_nat tptp.zero_zero_nat @t31))
% 152.02/152.37  (define @t629 () (= @t31 @t163))
% 152.02/152.37  (define @t630 () (or @t459 @t629))
% 152.02/152.37  (define @t631 () (_ @t624 @t623 tptp.m2))
% 152.02/152.37  (define @t632 () (_ @t617 (_ @t620 @t619 tptp.m2) @t618))
% 152.02/152.37  (define @t633 () (_ @t617 @t616 @t632))
% 152.02/152.37  (define @t634 () (= tptp.m2 @t633))
% 152.02/152.37  (define @t635 () (not @t631))
% 152.02/152.37  (define @t636 () (or @t635 @t634))
% 152.02/152.37  (define @t637 () (@var "BOUND_VARIABLE_14723" tptp.nat))
% 152.02/152.37  (define @t638 () (@list @t637))
% 152.02/152.37  (define @t639 () (@var "BOUND_VARIABLE_14712" tptp.nat))
% 152.02/152.37  (define @t640 () (@var "BOUND_VARIABLE_14710" tptp.nat))
% 152.02/152.37  (define @t641 () (_ @t622 @t621 @t640))
% 152.02/152.37  (define @t642 () (@list @t640 @t639))
% 152.02/152.37  (define @t643 () (tptp.suc @t637))
% 152.02/152.37  (define @t644 () (tptp.ord_less_nat @t637 @t643))
% 152.02/152.37  (define @t645 () (forall @t642 (or (not (tptp.ord_less_nat @t640 @t639)) (tptp.ord_less_nat @t640 (tptp.suc @t639)))))
% 152.02/152.37  (define @t646 () (not (= @t637 @t637)))
% 152.02/152.37  (define @t647 () (or @t646 @t644))
% 152.02/152.37  (define @t648 () (@var "BOUND_VARIABLE_14721" tptp.nat))
% 152.02/152.37  (define @t649 () (tptp.ord_less_nat @t648 @t643))
% 152.02/152.37  (define @t650 () (not (= @t648 @t637)))
% 152.02/152.37  (define @t651 () (or @t650 @t650 @t649))
% 152.02/152.37  (define @t652 () (@list @t648))
% 152.02/152.37  (define @t653 () (or @t650 @t649))
% 152.02/152.37  (define @t654 () (forall @t652 @t653))
% 152.02/152.37  (define @t655 () (forall @t638 @t654))
% 152.02/152.37  (define @t656 () (forall (@list @t637 @t648) @t653))
% 152.02/152.37  (define @t657 () (@list @t648 @t637))
% 152.02/152.37  (define @t658 () (not (= @t637 @t648)))
% 152.02/152.37  (define @t659 () (or @t658 @t649))
% 152.02/152.37  (define @t660 () (forall @t657 @t659))
% 152.02/152.37  (define @t661 () (tptp.suc @t31))
% 152.02/152.37  (define @t662 () (tptp.ord_less_nat @t185 @t661))
% 152.02/152.37  (define @t663 () (not @t417))
% 152.02/152.37  (define @t664 () (or @t663 @t662))
% 152.02/152.37  (define @t665 () (forall @t208 @t664))
% 152.02/152.37  (define @t666 () (@list @t185 @t31))
% 152.02/152.37  (define @t667 () (tptp.ord_less_nat @t185 @t31))
% 152.02/152.37  (define @t668 () (not @t667))
% 152.02/152.37  (define @t669 () (or @t668 @t662))
% 152.02/152.37  (define @t670 () (forall @t208 @t669))
% 152.02/152.37  (define @t671 () (and @t670 @t665))
% 152.02/152.37  (define @t672 () (and @t668 @t663))
% 152.02/152.37  (define @t673 () (and @t445 @t663))
% 152.02/152.37  (define @t674 () (or @t673 @t446))
% 152.02/152.37  (define @t675 () (or @t187 @t417))
% 152.02/152.37  (define @t676 () (not @t675))
% 152.02/152.37  (define @t677 () (@list @t413))
% 152.02/152.37  (define @t678 () (lambda @t677 (or (_ @t186 @t413) (= @t185 @t413))))
% 152.02/152.37  (define @t679 () (_ @t615 @t185))
% 152.02/152.37  (define @t680 () (_ @t679 @t31))
% 152.02/152.37  (define @t681 () (=> @t680 @t446))
% 152.02/152.37  (define @t682 () (_ @t622 @t621 tptp.xa))
% 152.02/152.37  (define @t683 () (not (_ @t624 @t682 @t437)))
% 152.02/152.37  (define @t684 () (_ @t622 @t621 @t437))
% 152.02/152.37  (define @t685 () (_ @t624 @t682 @t632))
% 152.02/152.37  (define @t686 () (or @t685 (not (forall @t441 (or (not (_ @t624 @t684 @t632)) @t683)))))
% 152.02/152.37  (define @t687 () (not @t685))
% 152.02/152.37  (define @t688 () (= tptp.xa @t632))
% 152.02/152.37  (define @t689 () (not @t688))
% 152.02/152.37  (define @t690 () (and @t687 @t689))
% 152.02/152.37  (define @t691 () (not @t690))
% 152.02/152.37  (define @t692 () (@var "BOUND_VARIABLE_18482" (@ho-elim-sort (-> tptp.nat Bool))))
% 152.02/152.37  (define @t693 () (not (_ @t624 @t692 @t437)))
% 152.02/152.37  (define @t694 () (_ @t617 @t616 @t31))
% 152.02/152.37  (define @t695 () (not (forall @t441 (or (not (_ @t624 @t684 @t694)) @t693))))
% 152.02/152.37  (define @t696 () (or (_ @t624 @t692 @t31) (not (forall @t441 (or (not (_ @t624 @t684 @t31)) @t693)))))
% 152.02/152.37  (define @t697 () (forall (@list @t31 @t692) (= @t695 @t696)))
% 152.02/152.37  (define @t698 () (_ @t242 @t437))
% 152.02/152.37  (define @t699 () (not @t698))
% 152.02/152.37  (define @t700 () (tptp.ord_less_nat @t437 @t31))
% 152.02/152.37  (define @t701 () (not (forall @t441 (or (not @t700) @t699))))
% 152.02/152.37  (define @t702 () (_ @t242 @t31))
% 152.02/152.37  (define @t703 () (tptp.ord_less_nat @t437 @t661))
% 152.02/152.37  (define @t704 () (not (forall @t441 (or (not @t703) @t699))))
% 152.02/152.37  (define @t705 () (or @t359 @t701))
% 152.02/152.37  (define @t706 () (= @t704 @t705))
% 152.02/152.37  (define @t707 () (not @t438))
% 152.02/152.37  (define @t708 () (not @t440))
% 152.02/152.37  (define @t709 () (or @t708 @t707))
% 152.02/152.37  (define @t710 () (forall @t441 (not @t447)))
% 152.02/152.37  (define @t711 () (not @t710))
% 152.02/152.37  (define @t712 () (not @t442))
% 152.02/152.37  (define @t713 () (or @t712 @t707))
% 152.02/152.37  (define @t714 () (forall @t441 (not @t450)))
% 152.02/152.37  (define @t715 () (not @t714))
% 152.02/152.37  (define @t716 () (forall @t441 (or (not (_ @t624 @t684 @t633)) @t683)))
% 152.02/152.37  (define @t717 () (not @t716))
% 152.02/152.37  (define @t718 () (= @t686 @t717))
% 152.02/152.37  (define @t719 () (forall @t208 (= (and (not (_ @t624 (_ @t622 @t621 @t185) @t31)) @t663) (or (_ @t624 (_ @t622 @t621 @t694) @t185) (= @t185 @t694)))))
% 152.02/152.37  (define @t720 () (tptp.ord_less_nat @t661 @t185))
% 152.02/152.37  (define @t721 () (or @t436 @t387))
% 152.02/152.37  (define @t722 () (= @t673 @t721))
% 152.02/152.37  (define @t723 () (= @t676 @t721))
% 152.02/152.37  (define @t724 () (not @t680))
% 152.02/152.37  (define @t725 () (or @t436 (= @t225 @t185)))
% 152.02/152.37  (define @t726 () (lambda @t677 (or (_ @t435 @t413) (= @t225 @t413))))
% 152.02/152.37  (define @t727 () (_ @t615 @t225))
% 152.02/152.37  (define @t728 () (_ @t727 @t185))
% 152.02/152.37  (define @t729 () (= tptp.xa @t633))
% 152.02/152.37  (define @t730 () (or (_ @t624 (_ @t622 @t621 @t633) tptp.xa) @t729))
% 152.02/152.37  (define @t731 () (not (= @t632 tptp.xa)))
% 152.02/152.37  (define @t732 () (and @t687 @t731))
% 152.02/152.37  (define @t733 () (= @t732 @t730))
% 152.02/152.37  (define @t734 () (= @t690 @t730))
% 152.02/152.37  (define @t735 () (@list false))
% 152.02/152.37  (define @t736 () (not @t730))
% 152.02/152.37  (define @t737 () (@quantifiers_skolemize @t716 0))
% 152.02/152.37  (define @t738 () (_ @t624 @t682 @t737))
% 152.02/152.37  (define @t739 () (not @t738))
% 152.02/152.37  (define @t740 () (_ @t624 (_ @t622 @t621 @t737) @t633))
% 152.02/152.37  (define @t741 () (not @t740))
% 152.02/152.37  (define @t742 () (or @t741 @t739))
% 152.02/152.37  (define @t743 () (not @t742))
% 152.02/152.37  (define @t744 () (and @t741 (not (= @t633 @t737))))
% 152.02/152.37  (define @t745 () (and @t739 (not (= tptp.xa @t737))))
% 152.02/152.37  (define @t746 () (= @t268 @t270))
% 152.02/152.37  (define @t747 () (_ @t622 @t621 @t268))
% 152.02/152.37  (define @t748 () (= @t270 @t349))
% 152.02/152.37  (define @t749 () (not @t748))
% 152.02/152.37  (define @t750 () (= @t268 @t349))
% 152.02/152.37  (define @t751 () (not @t750))
% 152.02/152.37  (define @t752 () (tptp.ord_less_nat @t268 @t270))
% 152.02/152.37  (define @t753 () (tptp.ord_less_nat @t349 @t270))
% 152.02/152.37  (define @t754 () (tptp.ord_less_nat @t268 @t349))
% 152.02/152.37  (define @t755 () (not @t433))
% 152.02/152.37  (define @t756 () (and @t755 @t749))
% 152.02/152.37  (define @t757 () (not @t426))
% 152.02/152.37  (define @t758 () (and @t757 @t751))
% 152.02/152.37  (define @t759 () (or @t758 @t756 @t457 @t746))
% 152.02/152.37  (define @t760 () (or @t756 @t457 @t746))
% 152.02/152.37  (define @t761 () (or @t457 @t746))
% 152.02/152.37  (define @t762 () (or @t433 @t748))
% 152.02/152.37  (define @t763 () (=> @t762 @t761))
% 152.02/152.37  (define @t764 () (or @t426 @t750))
% 152.02/152.37  (define @t765 () (lambda @t677 (or (_ @t425 @t413) (= @t268 @t413))))
% 152.02/152.37  (define @t766 () (_ @t615 @t268))
% 152.02/152.37  (define @t767 () (or @t433 (= @t349 @t270)))
% 152.02/152.37  (define @t768 () (lambda @t677 (or (_ @t432 @t413) (= @t349 @t413))))
% 152.02/152.37  (define @t769 () (_ @t615 @t349))
% 152.02/152.37  (define @t770 () (=> (_ @t769 @t270) (_ @t766 @t270)))
% 152.02/152.37  (define @t771 () (=> (_ @t766 @t349) @t770))
% 152.02/152.37  (define @t772 () (_ @t624 @t682 @t633))
% 152.02/152.37  (define @t773 () (or @t745 @t744 @t772 @t729))
% 152.02/152.37  (define @t774 () (_ @t624 @t682 tptp.m2))
% 152.02/152.37  (define @t775 () (and @t634 @t772))
% 152.02/152.37  (define @t776 () (not @t772))
% 152.02/152.37  (define @t777 () (not @t634))
% 152.02/152.37  (define @t778 () (= tptp.m2 tptp.xa))
% 152.02/152.37  (define @t779 () (not @t778))
% 152.02/152.37  (define @t780 () (not @t774))
% 152.02/152.37  (define @t781 () (and @t780 @t779))
% 152.02/152.37  (define @t782 () (@const 7 (@ho-elim-sort (-> tptp.nat tptp.a))))
% 152.02/152.37  (define @t783 () (@const 8 (-> (@ho-elim-sort (-> tptp.nat tptp.a)) tptp.nat tptp.a)))
% 152.02/152.37  (define @t784 () (_ @t783 @t782 tptp.xa))
% 152.02/152.37  (define @t785 () (_ (@const 11 (-> (@ho-elim-sort (-> tptp.set_a Bool)) tptp.set_a Bool)) (_ (@const 10 (-> (@ho-elim-sort (-> tptp.a tptp.set_a Bool)) tptp.a (@ho-elim-sort (-> tptp.set_a Bool)))) (@const 9 (@ho-elim-sort (-> tptp.a tptp.set_a Bool))) @t784) tptp.h1))
% 152.02/152.37  (define @t786 () (_ @t783 @t782 tptp.m2))
% 152.02/152.37  (define @t787 () (= @t786 @t784))
% 152.02/152.37  (define @t788 () (= tptp.h2 @t611))
% 152.02/152.37  (define @t789 () (@list true))
% 152.02/152.37  (define @t790 () (@var "BOUND_VARIABLE_16403" tptp.nat))
% 152.02/152.37  (define @t791 () (= @t595 @t790))
% 152.02/152.37  (define @t792 () (_ @t783 @t782 @t595))
% 152.02/152.37  (define @t793 () (_ @t783 @t782 @t790))
% 152.02/152.37  (define @t794 () (not (= @t792 @t793)))
% 152.02/152.37  (define @t795 () (not (= tptp.m2 @t790)))
% 152.02/152.37  (define @t796 () (and (not (_ @t624 (_ @t622 @t621 @t790) tptp.m2)) @t795))
% 152.02/152.37  (define @t797 () (= tptp.m2 @t595))
% 152.02/152.37  (define @t798 () (not @t797))
% 152.02/152.37  (define @t799 () (and (not (_ @t624 (_ @t622 @t621 @t595) tptp.m2)) @t798))
% 152.02/152.37  (define @t800 () (or @t799 @t796 @t794 @t791))
% 152.02/152.37  (define @t801 () (@list @t595 @t790))
% 152.02/152.37  (define @t802 () (forall @t801 @t800))
% 152.02/152.37  (define @t803 () (tptp.g @t595))
% 152.02/152.37  (define @t804 () (not (= @t803 (tptp.g @t790))))
% 152.02/152.37  (define @t805 () (and (not (tptp.ord_less_nat @t790 tptp.m2)) @t795))
% 152.02/152.37  (define @t806 () (tptp.ord_less_nat @t595 tptp.m2))
% 152.02/152.37  (define @t807 () (and (not @t806) @t798))
% 152.02/152.37  (define @t808 () (= @t790 @t595))
% 152.02/152.37  (define @t809 () (or @t807 @t805 @t804 @t808))
% 152.02/152.37  (define @t810 () (or @t805 @t804 @t808))
% 152.02/152.37  (define @t811 () (or @t807 @t810))
% 152.02/152.37  (define @t812 () (forall @t801 @t811))
% 152.02/152.37  (define @t813 () (@list @t790))
% 152.02/152.37  (define @t814 () (forall @t813 @t811))
% 152.02/152.37  (define @t815 () (forall @t813 @t810))
% 152.02/152.37  (define @t816 () (or @t807 @t815))
% 152.02/152.37  (define @t817 () (= @t341 @t595))
% 152.02/152.37  (define @t818 () (tptp.g @t341))
% 152.02/152.37  (define @t819 () (= tptp.m2 @t341))
% 152.02/152.37  (define @t820 () (not @t819))
% 152.02/152.37  (define @t821 () (tptp.ord_less_nat @t341 tptp.m2))
% 152.02/152.37  (define @t822 () (forall @t343 (or (and (not @t821) @t820) (not (= @t803 @t818)) @t817)))
% 152.02/152.37  (define @t823 () (_ tptp.ord_less_nat @t595))
% 152.02/152.37  (define @t824 () (_ @t823 tptp.m2))
% 152.02/152.37  (define @t825 () (not @t824))
% 152.02/152.37  (define @t826 () (and @t825 @t798))
% 152.02/152.37  (define @t827 () (or @t826 @t822))
% 152.02/152.37  (define @t828 () (or @t824 @t797))
% 152.02/152.37  (define @t829 () (not @t598))
% 152.02/152.37  (define @t830 () (_ tptp.ord_less_nat @t341))
% 152.02/152.37  (define @t831 () (_ @t830 tptp.m2))
% 152.02/152.37  (define @t832 () (not @t831))
% 152.02/152.37  (define @t833 () (and @t832 @t820))
% 152.02/152.37  (define @t834 () (or @t833 @t829 @t817))
% 152.02/152.37  (define @t835 () (=> @t598 @t817))
% 152.02/152.37  (define @t836 () (or @t831 @t819))
% 152.02/152.37  (define @t837 () (or @t831 (= @t341 tptp.m2)))
% 152.02/152.37  (define @t838 () (lambda @t677 (or (_ @t830 @t413) (= @t341 @t413))))
% 152.02/152.37  (define @t839 () (_ @t615 @t341))
% 152.02/152.37  (define @t840 () (=> (_ @t839 tptp.m2) @t599))
% 152.02/152.37  (define @t841 () (forall @t343 @t840))
% 152.02/152.37  (define @t842 () (_ @t823 @t413))
% 152.02/152.37  (define @t843 () (or @t842 (= @t595 @t413)))
% 152.02/152.37  (define @t844 () (lambda @t677 @t843))
% 152.02/152.37  (define @t845 () (_ @t615 @t595))
% 152.02/152.37  (define @t846 () (=> (_ @t845 tptp.m2) @t841))
% 152.02/152.37  (define @t847 () (not @t787))
% 152.02/152.37  (define @t848 () (or @t781 @t847 @t778))
% 152.02/152.37  (define @t849 () (not (= @t784 @t786)))
% 152.02/152.37  (define @t850 () (not (_ @t624 (_ @t622 @t621 tptp.m2) tptp.m2)))
% 152.02/152.37  (define @t851 () (not (= tptp.m2 tptp.m2)))
% 152.02/152.37  (define @t852 () (and @t850 @t851))
% 152.02/152.37  (define @t853 () (or @t852 @t781 @t849 @t778))
% 152.02/152.37  (define @t854 () (forall @t801 (or @t799 @t796 (not (= @t793 @t792)) @t791)))
% 152.02/152.37  (define @t855 () (not @t729))
% 152.02/152.37  (define @t856 () (_ tptp.ord_less_nat tptp.xa))
% 152.02/152.37  (define @t857 () (or (_ @t856 @t610) (= tptp.xa @t610)))
% 152.02/152.37  (define @t858 () (lambda @t677 (or (_ @t856 @t413) (= tptp.xa @t413))))
% 152.02/152.37  (define @t859 () (@list false true))
% 152.02/152.37  (define @t860 () (_ @t624 @t682 (_ @t617 @t616 tptp.xa)))
% 152.02/152.37  (define @t861 () (and @t688 @t634 @t860))
% 152.02/152.37  (assume @p1 (_ tptp.ring_b_d tptp.r))
% 152.02/152.37  (assume @p2 (forall @t8 (=> @t7 (=> @t5 (_ @t3 @t1)))))
% 152.02/152.37  (assume @p3 (_ @t6 @t1))
% 152.02/152.37  (assume @p4 (forall @t11 (=> @t7 @t10)))
% 152.02/152.37  (assume @p5 (forall @t11 (=> @t13 @t10)))
% 152.02/152.37  (assume @p6 (forall (@list @t14 @t17) (=> @t21 (=> @t19 (_ @t18 @t16)))))
% 152.02/152.37  (assume @p7 (forall @t22 (=> @t21 (_ (_ tptp.ord_less_eq_set_a @t16) @t1))))
% 152.02/152.37  (assume @p8 (forall (@list @t4 @t25 @t23) (=> @t13 (=> @t28 (=> @t27 (_ (_ tptp.ord_less_eq_set_a (_ @t15 @t25)) @t24))))))
% 152.02/152.37  (assume @p9 (forall @t22 (=> @t21 (_ @t6 @t16))))
% 152.02/152.37  (assume @p10 (forall @t57 (=> @t10 (=> @t56 (=> @t51 (=> @t49 (=> @t45 @t37)))))))
% 152.02/152.37  (assume @p11 (forall @t57 (=> @t10 (=> (and @t56 @t51 @t49 @t45) @t37))))
% 152.02/152.37  (assume @p12 (forall (@list @t62 @t4 @t30 @t31 @t58) (=> @t67 (=> @t10 (=> @t65 (=> @t61 (_ (_ tptp.member_a @t59) @t1)))))))
% 152.02/152.37  (assume @p13 (forall (@list @t62 @t4 @t31) (=> @t67 (=> @t10 (forall @t72 (=> @t71 (_ (_ tptp.member_a (_ (_ @t33 @t69) @t68)) @t1)))))))
% 152.02/152.37  (assume @p14 (_ @t66 (_ (_ tptp.annihilator_b_d_a_c tptp.r) tptp.m)))
% 152.02/152.37  (assume @p15 (forall (@list @t23 @t17) (=> @t86 (=> (_ @t26 @t1) (=> (_ @t18 @t24) (exists @t85 (and @t84 (exists @t80 (and (_ @t79 (_ @t78 @t53)) (= @t17 (_ (_ @t76 @t74) @t73)))))))))))
% 152.02/152.37  (assume @p16 (_ (_ tptp.module_a_b_c_d tptp.m) tptp.r))
% 152.02/152.37  (assume @p17 (forall (@list @t88 @t87) (=> (_ @t6 @t88) (=> (_ @t6 @t87) (_ @t66 (_ (_ (_ (_ tptp.quotie1153752712_d_a_c tptp.r) tptp.m) @t88) @t87))))))
% 152.02/152.37  (assume @p18 (forall @t90 (=> @t67 (_ @t6 @t89))))
% 152.02/152.37  (assume @p19 (forall (@list @t62 @t17) (=> @t67 (=> (_ @t18 @t89) (exists @t97 (and @t96 (exists @t94 (and (_ @t93 (_ @t82 (lambda @t46 @t1))) (= @t17 (_ (_ @t76 @t92) @t91))))))))))
% 152.02/152.37  (assume @p20 (forall (@list @t99 @t100 @t98 @t103) (=> @t107 (=> @t106 (=> (_ @t104 @t98) (_ @t104 @t102))))))
% 152.02/152.37  (assume @p21 (forall (@list @t108 @t100 @t14 @t17) (=> @t113 (=> @t112 (=> @t19 (_ @t18 @t110))))))
% 152.02/152.37  (assume @p22 (forall (@list @t114 @t100 @t14 @t17) (=> @t119 (=> @t118 (=> @t19 (_ @t18 @t116))))))
% 152.02/152.37  (assume @p23 (forall (@list @t99 @t100 @t123 @t122 @t120) (=> @t107 (=> @t125 (=> (_ (_ tptp.ord_less_eq_set_e @t122) @t120) (=> (_ @t124 @t123) (_ (_ tptp.ord_less_eq_set_e (_ @t101 @t122)) @t121)))))))
% 152.02/152.37  (assume @p24 (forall (@list @t108 @t100 @t4 @t25 @t23) (=> @t113 (=> @t127 (=> @t28 (=> @t27 (_ (_ tptp.ord_less_eq_set_a (_ @t109 @t25)) @t126)))))))
% 152.02/152.37  (assume @p25 (forall (@list @t114 @t100 @t4 @t25 @t23) (=> @t119 (=> @t129 (=> @t28 (=> @t27 (_ (_ tptp.ord_less_eq_set_a (_ @t115 @t25)) @t128)))))))
% 152.02/152.37  (assume @p26 (forall @t131 (=> @t107 (=> @t106 (_ @t130 @t102)))))
% 152.02/152.37  (assume @p27 (forall @t133 (=> @t113 (=> @t112 (_ @t132 @t110)))))
% 152.02/152.37  (assume @p28 (forall @t135 (=> @t119 (=> @t118 (_ @t134 @t116)))))
% 152.02/152.37  (assume @p29 (forall (@list @t99 @t100 @t120 @t103) (=> @t107 (=> (not (= @t120 tptp.bot_bot_set_e)) (=> (_ @t124 @t105) (=> (_ @t104 @t121) (exists (@list @t75 @t136) (and (_ (_ tptp.member_nat_e @t136) (_ @t141 (lambda @t46 @t120))) (exists @t80 (and @t140 (= @t103 (_ (_ @t138 @t74) @t136))))))))))))
% 152.02/152.37  (assume @p30 (forall (@list @t108 @t100 @t23 @t17) (=> @t113 (=> @t86 (=> (_ @t26 @t111) (=> (_ @t18 @t126) (exists @t85 (and @t84 (exists @t80 (and @t140 (= @t17 (_ (_ @t143 @t74) @t73))))))))))))
% 152.02/152.37  (assume @p31 (forall (@list @t114 @t100 @t23 @t17) (=> @t119 (=> @t86 (=> (_ @t26 @t117) (=> (_ @t18 @t128) (exists @t85 (and @t84 (exists @t80 (and @t140 (= @t17 (_ (_ @t145 @t74) @t73))))))))))))
% 152.02/152.37  (assume @p32 (forall @t131 (=> @t107 (=> @t106 (_ (_ tptp.ord_less_eq_set_e @t102) @t105)))))
% 152.02/152.37  (assume @p33 (forall @t133 (=> @t113 (=> @t112 (_ (_ tptp.ord_less_eq_set_a @t110) @t111)))))
% 152.02/152.37  (assume @p34 (forall @t135 (=> @t119 (=> @t118 (_ (_ tptp.ord_less_eq_set_a @t116) @t117)))))
% 152.02/152.37  (assume @p35 (_ @t147 tptp.m))
% 152.02/152.37  (assume @p36 (forall @t151 (=> @t150 (_ (_ tptp.module1648870817unit_d (_ (_ (_ tptp.hOM_b_d_a_c_e_f tptp.r) tptp.m) @t148)) tptp.r))))
% 152.02/152.37  (assume @p37 (forall @t155 (=> @t154 (_ (_ tptp.module589927589unit_d (_ (_ (_ tptp.hOM_b_d_a_c_a_c tptp.r) tptp.m) @t152)) tptp.r))))
% 152.02/152.37  (assume @p38 (forall @t159 (=> @t158 (_ (_ tptp.module589927589unit_d (_ (_ (_ tptp.hOM_b_717364638t_unit tptp.r) tptp.m) @t156)) tptp.r))))
% 152.02/152.37  (assume @p39 @t168)
% 152.02/152.37  (assume @p40 (forall @t11 (=> @t170 @t10)))
% 152.02/152.37  (assume @p41 (forall @t11 (=> @t13 @t170)))
% 152.02/152.37  (assume @p42 (forall (@list @t99 @t100 @t62 @t123 @t30 @t31 @t171) (=> @t107 (=> @t177 (=> @t175 (=> @t65 (=> (_ (_ tptp.member_nat_e @t171) @t174) (_ (_ tptp.member_e (_ @t173 @t171)) @t105))))))))
% 152.02/152.37  (assume @p43 (forall (@list @t114 @t100 @t62 @t4 @t30 @t31 @t58) (=> @t119 (=> @t177 (=> @t180 (=> @t65 (=> @t61 (_ (_ tptp.member_a (_ @t179 @t58)) @t117))))))))
% 152.02/152.37  (assume @p44 (forall (@list @t108 @t100 @t62 @t4 @t30 @t31 @t58) (=> @t113 (=> @t177 (=> @t183 (=> @t65 (=> @t61 (_ (_ tptp.member_a (_ @t182 @t58)) @t111))))))))
% 152.02/152.37  (assume @p45 (forall (@list @t99 @t100 @t62 @t123 @t31) (=> @t107 (=> @t177 (=> @t175 (forall (@list @t69 @t184) (=> (and @t70 (_ (_ tptp.member_nat_e @t184) @t174)) (_ (_ tptp.member_e (_ (_ @t172 @t69) @t184)) @t105))))))))
% 152.02/152.37  (assume @p46 (forall (@list @t114 @t100 @t62 @t4 @t31) (=> @t119 (=> @t177 (=> @t180 (forall @t72 (=> @t71 (_ (_ tptp.member_a (_ (_ @t178 @t69) @t68)) @t117))))))))
% 152.02/152.37  (assume @p47 (forall (@list @t108 @t100 @t62 @t4 @t31) (=> @t113 (=> @t177 (=> @t183 (forall @t72 (=> @t71 (_ (_ tptp.member_a (_ (_ @t181 @t69) @t68)) @t111))))))))
% 152.02/152.37  (assume @p48 (forall @t189 (= (_ @t164 @t188) @t187)))
% 152.02/152.37  (assume @p49 (forall @t197 (=> @t107 (=> @t175 (=> @t196 (=> @t195 (=> @t194 (=> @t193 @t192))))))))
% 152.02/152.37  (assume @p50 (forall @t199 (=> @t119 (=> @t180 (=> @t196 (=> @t51 (=> @t49 (=> @t45 @t198))))))))
% 152.02/152.37  (assume @p51 (forall @t201 (=> @t113 (=> @t183 (=> @t196 (=> @t51 (=> @t49 (=> @t45 @t200))))))))
% 152.02/152.37  (assume @p52 (forall @t197 (=> @t107 (=> @t175 (=> (and @t196 @t195 @t194 @t193) @t192)))))
% 152.02/152.37  (assume @p53 (forall @t199 (=> @t119 (=> @t180 (=> @t202 @t198)))))
% 152.02/152.37  (assume @p54 (forall @t201 (=> @t113 (=> @t183 (=> @t202 @t200)))))
% 152.02/152.37  (assume @p55 (forall @t208 (= @t207 @t204)))
% 152.02/152.37  (assume @p56 (forall @t208 (=> @t204 @t207)))
% 152.02/152.37  (assume @p57 (forall (@list @t210 @t209) (= (= (_ tptp.suc @t210) @t211) (= @t210 @t209))))
% 152.02/152.37  (assume @p58 (forall (@list @t213 @t212) (= (= @t214 (_ tptp.suc @t212)) (= @t213 @t212))))
% 152.02/152.37  (assume @p59 (forall @t151 (=> @t150 (=> @t217 (_ (_ @t215 @t148) tptp.m)))))
% 152.02/152.37  (assume @p60 (forall @t159 (=> @t158 (=> @t220 (_ (_ @t218 @t156) tptp.m)))))
% 152.02/152.37  (assume @p61 (forall @t155 (=> @t154 (=> @t221 (_ (_ @t146 @t152) tptp.m)))))
% 152.02/152.37  (assume @p62 (forall @t189 (= (_ @t226 @t224) @t223)))
% 152.02/152.37  (assume @p63 (forall @t229 (_ @t228 @t227)))
% 152.02/152.37  (assume @p64 (forall @t167 (_ @t228 @t31)))
% 152.02/152.37  (assume @p65 (forall @t208 (= @t231 @t187)))
% 152.02/152.37  (assume @p66 (forall @t208 (=> @t187 @t231)))
% 152.02/152.37  (assume @p67 (forall (@list @t232 @t233) (= (_ @t234 (_ tptp.collect_nat_a @t233)) (_ @t233 @t232))))
% 152.02/152.37  (assume @p68 (forall (@list @t235 @t236) (= (_ @t237 (_ tptp.collect_nat_b @t236)) (_ @t236 @t235))))
% 152.02/152.37  (assume @p69 (forall (@list @t238 @t239) (= (_ @t241 @t240) (_ @t239 @t238))))
% 152.02/152.37  (assume @p70 (forall (@list @t227 @t242) (= (_ (_ tptp.member_nat @t227) @t243) (_ @t242 @t227))))
% 152.02/152.37  (assume @p71 (forall @t248 (= (_ tptp.collect_nat_a (lambda @t247 @t246)) @t244)))
% 152.02/152.37  (assume @p72 (forall @t253 (= (_ tptp.collect_nat_b (lambda @t252 @t251)) @t249)))
% 152.02/152.37  (assume @p73 (forall @t258 (= (_ tptp.collect_a (lambda @t257 @t256)) @t254)))
% 152.02/152.37  (assume @p74 (forall (@list @t259) (= (_ tptp.collect_nat (lambda @t261 (_ (_ tptp.member_nat @t260) @t259))) @t259)))
% 152.02/152.37  (assume @p75 (forall (@list @t242 @t262) (=> (forall @t44 (= @t263 (_ @t262 @t38))) (= @t243 (_ tptp.collect_nat @t262)))))
% 152.02/152.37  (assume @p76 (forall @t229 (= (not @t264) (_ @t164 @t227))))
% 152.02/152.37  (assume @p77 (forall @t167 (not (_ @t265 tptp.zero_zero_nat))))
% 152.02/152.37  (assume @p78 (forall @t167 (= @t267 @t165)))
% 152.02/152.37  (assume @p79 (forall (@list @t268 @t31) (=> (_ @t269 @t31) (= (_ @t161 (_ @t161 @t268)) @t268))))
% 152.02/152.37  (assume @p80 (forall (@list @t185 @t31 @t270) (= (_ (_ tptp.minus_minus_nat @t272) (_ tptp.suc @t270)) (_ (_ tptp.minus_minus_nat @t206) @t270))))
% 152.02/152.37  (assume @p81 (forall @t208 (= (_ @t271 @t225) @t206)))
% 152.02/152.37  (assume @p82 (forall @t273 (= (_ @t205 @t185) tptp.zero_zero_nat)))
% 152.02/152.37  (assume @p83 (forall @t167 (= (_ @t274 @t31) tptp.zero_zero_nat)))
% 152.02/152.37  (assume @p84 (forall (@list @t275 @t148) (=> @t279 (=> @t150 (=> @t277 (=> @t217 (_ (_ (_ tptp.misomo768936435_f_e_f tptp.r) @t275) @t148)))))))
% 152.02/152.37  (assume @p85 (forall (@list @t275 @t156) (=> @t279 (=> @t158 (=> @t277 (=> @t220 (_ (_ (_ tptp.misomo368157697t_unit tptp.r) @t275) @t156)))))))
% 152.02/152.37  (assume @p86 (forall (@list @t280 @t148) (=> @t284 (=> @t150 (=> @t282 (=> @t217 (_ (_ (_ tptp.misomo951986689it_e_f tptp.r) @t280) @t148)))))))
% 152.02/152.37  (assume @p87 (forall (@list @t280 @t156) (=> @t284 (=> @t158 (=> @t282 (=> @t220 (_ (_ (_ tptp.misomo493403663t_unit tptp.r) @t280) @t156)))))))
% 152.02/152.37  (assume @p88 (forall (@list @t275 @t152) (=> @t279 (=> @t154 (=> @t277 (=> @t221 (_ @t276 @t152)))))))
% 152.02/152.37  (assume @p89 (forall (@list @t280 @t152) (=> @t284 (=> @t154 (=> @t282 (=> @t221 (_ @t281 @t152)))))))
% 152.02/152.37  (assume @p90 (forall (@list @t285 @t148) (=> @t289 (=> @t150 (=> @t287 (=> @t217 (_ (_ @t216 @t285) @t148)))))))
% 152.02/152.37  (assume @p91 (forall (@list @t285 @t156) (=> @t289 (=> @t158 (=> @t287 (=> @t220 (_ (_ @t219 @t285) @t156)))))))
% 152.02/152.37  (assume @p92 (forall (@list @t285 @t152) (=> @t289 (=> @t154 (=> @t287 (=> @t221 (_ @t286 @t152)))))))
% 152.02/152.37  (assume @p93 (forall @t167 (_ @t164 @t225)))
% 152.02/152.37  (assume @p94 (forall @t167 (= (_ @t265 @t160) @t266)))
% 152.02/152.37  (assume @p95 (forall @t291 (=> @t107 (=> @t290 (_ (_ tptp.module241733029unit_d (_ (_ (_ tptp.hOM_b_d_e_f_e_f @t100) @t99) @t148)) @t100)))))
% 152.02/152.37  (assume @p96 (forall @t293 (=> @t107 (=> @t292 (_ (_ tptp.module1330273449unit_d (_ (_ (_ tptp.hOM_b_d_e_f_a_c @t100) @t99) @t152)) @t100)))))
% 152.02/152.37  (assume @p97 (forall @t295 (=> @t107 (=> @t294 (_ (_ tptp.module1330273449unit_d (_ (_ (_ tptp.hOM_b_1375846429t_unit @t100) @t99) @t156)) @t100)))))
% 152.02/152.37  (assume @p98 (forall @t296 (=> @t119 (=> @t290 (_ (_ tptp.module1648870817unit_d (_ (_ (_ tptp.hOM_b_d_a_c_e_f @t100) @t114) @t148)) @t100)))))
% 152.02/152.37  (assume @p99 (forall @t297 (=> @t119 (=> @t292 (_ (_ tptp.module589927589unit_d (_ (_ (_ tptp.hOM_b_d_a_c_a_c @t100) @t114) @t152)) @t100)))))
% 152.02/152.37  (assume @p100 (forall @t298 (=> @t119 (=> @t294 (_ (_ tptp.module589927589unit_d (_ (_ (_ tptp.hOM_b_717364638t_unit @t100) @t114) @t156)) @t100)))))
% 152.02/152.37  (assume @p101 (forall @t299 (=> @t113 (=> @t290 (_ (_ tptp.module1648870817unit_d (_ (_ (_ tptp.hOM_b_1959675421it_e_f @t100) @t108) @t148)) @t100)))))
% 152.02/152.37  (assume @p102 (forall @t300 (=> @t113 (=> @t292 (_ (_ tptp.module589927589unit_d (_ (_ (_ tptp.hOM_b_796081438it_a_c @t100) @t108) @t152)) @t100)))))
% 152.02/152.37  (assume @p103 (forall @t301 (=> @t113 (=> @t294 (_ (_ tptp.module589927589unit_d (_ (_ (_ tptp.hOM_b_1103679019t_unit @t100) @t108) @t156)) @t100)))))
% 152.02/152.37  (assume @p104 (forall (@list @t99 @t100 @t275 @t148) (=> @t107 (=> @t308 (=> @t290 (=> @t307 (=> @t306 @t304)))))))
% 152.02/152.37  (assume @p105 (forall (@list @t99 @t100 @t275 @t152) (=> @t107 (=> @t308 (=> @t292 (=> @t307 (=> @t311 (_ @t310 @t152))))))))
% 152.02/152.37  (assume @p106 (forall (@list @t99 @t100 @t275 @t156) (=> @t107 (=> @t308 (=> @t294 (=> @t307 (=> @t314 @t313)))))))
% 152.02/152.37  (assume @p107 (forall (@list @t99 @t100 @t285 @t148) (=> @t107 (=> @t318 (=> @t290 (=> @t317 (=> @t306 (_ @t316 @t148))))))))
% 152.02/152.37  (assume @p108 (forall (@list @t99 @t100 @t285 @t156) (=> @t107 (=> @t318 (=> @t294 (=> @t317 (=> @t314 (_ (_ @t319 @t285) @t156))))))))
% 152.02/152.37  (assume @p109 (forall (@list @t99 @t100 @t280 @t148) (=> @t107 (=> @t323 (=> @t290 (=> @t322 (=> @t306 (_ @t321 @t148))))))))
% 152.02/152.37  (assume @p110 (forall (@list @t99 @t100 @t280 @t152) (=> @t107 (=> @t323 (=> @t292 (=> @t322 (=> @t311 (_ (_ @t324 @t280) @t152))))))))
% 152.02/152.37  (assume @p111 (forall (@list @t99 @t100 @t280 @t156) (=> @t107 (=> @t323 (=> @t294 (=> @t322 (=> @t314 (_ (_ @t325 @t280) @t156))))))))
% 152.02/152.37  (assume @p112 (forall (@list @t114 @t100 @t275 @t148) (=> @t119 (=> @t308 (=> @t290 (=> @t327 (=> @t326 @t304)))))))
% 152.02/152.37  (assume @p113 (forall (@list @t114 @t100 @t275 @t156) (=> @t119 (=> @t308 (=> @t294 (=> @t327 (=> @t328 @t313)))))))
% 152.02/152.37  (assume @p114 (forall @t329 (=> @t107 (_ @t305 @t99))))
% 152.02/152.37  (assume @p115 (forall @t331 (=> @t113 (_ @t330 @t108))))
% 152.02/152.37  (assume @p116 (forall @t334 (=> @t119 (_ @t333 @t114))))
% 152.02/152.37  (assume @p117 (forall @t291 (=> @t107 (=> @t290 (=> @t306 (_ (_ @t302 @t148) @t99))))))
% 152.02/152.37  (assume @p118 (forall @t293 (=> @t107 (=> @t292 (=> @t311 (_ (_ @t315 @t152) @t99))))))
% 152.02/152.37  (assume @p119 (forall @t295 (=> @t107 (=> @t294 (=> @t314 (_ (_ @t320 @t156) @t99))))))
% 152.02/152.37  (assume @p120 (forall @t296 (=> @t119 (=> @t290 (=> @t326 (_ (_ @t309 @t148) @t114))))))
% 152.02/152.37  (assume @p121 (forall @t298 (=> @t119 (=> @t294 (=> @t328 (_ (_ @t324 @t156) @t114))))))
% 152.02/152.37  (assume @p122 (forall @t299 (=> @t113 (=> @t290 (=> (_ (_ @t320 @t108) @t148) (_ (_ @t312 @t148) @t108))))))
% 152.02/152.37  (assume @p123 (forall @t300 (=> @t113 (=> @t292 (=> (_ (_ @t324 @t108) @t152) (_ (_ @t319 @t152) @t108))))))
% 152.02/152.37  (assume @p124 (forall @t301 (=> @t113 (=> @t294 (=> (_ @t330 @t156) (_ (_ @t325 @t156) @t108))))))
% 152.02/152.37  (assume @p125 (forall @t297 (=> @t119 (=> @t292 (=> (_ @t333 @t152) (_ (_ @t332 @t152) @t114))))))
% 152.02/152.37  (assume @p126 (forall @t336 (=> @t107 (=> @t125 @t335))))
% 152.02/152.37  (assume @p127 (forall @t338 (=> @t113 (=> @t127 @t337))))
% 152.02/152.37  (assume @p128 (forall @t340 (=> @t119 (=> @t129 @t339))))
% 152.02/152.37  (assume @p129 (forall @t336 (=> @t107 (=> @t335 @t175))))
% 152.02/152.37  (assume @p130 (forall @t340 (=> @t119 (=> @t339 @t180))))
% 152.02/152.37  (assume @p131 (forall @t338 (=> @t113 (=> @t337 @t183))))
% 152.02/152.37  (assume @p132 (forall @t329 (=> @t107 (_ @t176 (_ (_ tptp.annihilator_b_d_e_f @t100) @t99)))))
% 152.02/152.37  (assume @p133 (forall @t331 (=> @t113 (_ @t176 (_ (_ tptp.annihi259882159t_unit @t100) @t108)))))
% 152.02/152.37  (assume @p134 (forall @t334 (=> @t119 (_ @t176 (_ (_ tptp.annihilator_b_d_a_c @t100) @t114)))))
% 152.02/152.37  (assume @p135 (forall (@list @t242 @t270 @t344) (=> @t347 (=> (forall @t346 (=> (_ @t242 @t345) (_ (_ tptp.ord_less_eq_nat @t345) @t344))) (exists @t44 (and @t263 (forall @t343 (=> (_ @t242 @t341) (_ @t342 @t38)))))))))
% 152.02/152.37  (assume @p136 (forall @t208 (or @t204 @t223)))
% 152.02/152.37  (assume @p137 (forall @t208 (=> @t204 (=> @t223 @t348))))
% 152.02/152.37  (assume @p138 @t354)
% 152.02/152.37  (assume @p139 (forall @t167 (not (= @t31 @t225))))
% 152.02/152.37  (assume @p140 (forall @t358 (=> (= (_ tptp.suc @t356) (_ tptp.suc @t355)) @t357)))
% 152.02/152.37  (assume @p141 (forall @t358 (=> (not @t357) (=> (not (_ (_ tptp.ord_less_nat @t356) @t355)) (_ (_ tptp.ord_less_nat @t355) @t356)))))
% 152.02/152.37  (assume @p142 (forall @t367 (=> (forall @t366 @t365) @t359)))
% 152.02/152.37  (assume @p143 (forall @t367 (=> (forall @t366 (=> (forall @t363 (=> @t362 @t361)) @t364)) @t359)))
% 152.02/152.37  (assume @p144 (forall @t167 (not (_ @t265 @t31))))
% 152.02/152.37  (assume @p145 (forall (@list @t369 @t368) (=> (_ (_ tptp.ord_less_nat @t369) @t368) (not (= @t369 @t368)))))
% 152.02/152.37  (assume @p146 (forall @t189 (=> @t371 @t370)))
% 152.02/152.37  (assume @p147 (forall @t208 (= @t370 (or @t187 @t371))))
% 152.02/152.37  (assume @p148 (forall @t353 (= (_ (_ tptp.minus_minus_nat (_ @t372 @t349)) @t270) (_ (_ tptp.minus_minus_nat (_ @t372 @t270)) @t349))))
% 152.02/152.37  (assume @p149 (forall (@list @t99 @t100 @t62) (=> @t107 (=> @t177 (_ @t130 @t373)))))
% 152.02/152.37  (assume @p150 (forall (@list @t108 @t100 @t62) (=> @t113 (=> @t177 (_ @t132 @t374)))))
% 152.02/152.37  (assume @p151 (forall (@list @t114 @t100 @t62) (=> @t119 (=> @t177 (_ @t134 @t375)))))
% 152.02/152.37  (assume @p152 (forall (@list @t99 @t100 @t377 @t376) (=> @t107 (=> (_ @t130 @t377) (=> (_ @t130 @t376) (_ @t176 (_ (_ (_ (_ tptp.quotie169863047_d_e_f @t100) @t99) @t377) @t376)))))))
% 152.02/152.37  (assume @p153 (forall (@list @t108 @t100 @t88 @t87) (=> @t113 (=> (_ @t132 @t88) (=> (_ @t132 @t87) (_ @t176 (_ (_ (_ (_ tptp.quotie1196826005t_unit @t100) @t108) @t88) @t87)))))))
% 152.02/152.37  (assume @p154 (forall (@list @t114 @t100 @t88 @t87) (=> @t119 (=> (_ @t134 @t88) (=> (_ @t134 @t87) (_ @t176 (_ (_ (_ (_ tptp.quotie1153752712_d_a_c @t100) @t114) @t88) @t87)))))))
% 152.02/152.37  (assume @p155 (forall (@list @t185 @t31 @t378) (=> @t204 (=> (forall @t44 (_ @t381 @t38)) (=> (forall (@list @t38 @t345 @t380) (=> (_ @t381 @t345) (=> (_ (_ @t378 @t345) @t380) (_ @t381 @t380)))) (=> (forall @t366 (_ (_ @t378 @t75) @t379)) (_ (_ @t378 @t185) @t31)))))))
% 152.02/152.37  (assume @p156 (forall (@list @t185 @t31 @t242) (=> @t204 (=> (_ @t242 @t185) (=> (forall @t366 (=> (_ @t203 @t75) @t383)) @t359)))))
% 152.02/152.37  (assume @p157 (forall @t367 (=> (forall @t366 (=> (forall @t363 (=> (_ (_ tptp.ord_less_eq_nat (_ tptp.suc @t360)) @t75) @t361)) @t364)) @t359)))
% 152.02/152.37  (assume @p158 @t386)
% 152.02/152.37  (assume @p159 (forall @t167 (not (_ @t226 @t31))))
% 152.02/152.37  (assume @p160 (forall @t208 (= @t388 (or @t204 @t387))))
% 152.02/152.37  (assume @p161 (forall (@list @t31 @t391) (=> (_ @t226 @t391) (exists @t392 (= @t391 @t390)))))
% 152.02/152.37  (assume @p162 (forall @t208 (=> @t204 @t388)))
% 152.02/152.37  (assume @p163 (forall @t208 (=> @t388 (=> @t384 @t387))))
% 152.02/152.37  (assume @p164 (forall @t208 (=> @t393 @t204)))
% 152.02/152.37  (assume @p165 (forall @t229 (=> @t395 @t264)))
% 152.02/152.37  (assume @p166 (forall @t229 (= @t395 @t264)))
% 152.02/152.37  (assume @p167 (forall @t167 (= (_ @t222 tptp.zero_zero_nat) @t266)))
% 152.02/152.37  (assume @p168 (forall @t167 (=> @t267 @t396)))
% 152.02/152.37  (assume @p169 (forall (@list @t242 @t210) (=> @t400 (=> (forall @t399 (=> (_ @t242 @t397) (_ @t242 @t398))) (_ @t242 @t210)))))
% 152.02/152.37  (assume @p170 (forall (@list @t355) (=> (not (= @t355 tptp.zero_zero_nat)) (not (forall @t399 (not (= @t355 @t398)))))))
% 152.02/152.37  (assume @p171 (forall @t273 (not (= tptp.zero_zero_nat @t224))))
% 152.02/152.37  (assume @p172 (forall @t273 (not (= @t224 tptp.zero_zero_nat))))
% 152.02/152.37  (assume @p173 (forall (@list @t242 @t270) (=> @t347 (=> @t402 @t400))))
% 152.02/152.37  (assume @p174 (forall (@list @t403 @t185 @t31) (=> (forall @t44 (_ @t405 tptp.zero_zero_nat)) (=> (forall @t346 (_ (_ @t403 tptp.zero_zero_nat) @t404)) (=> (forall (@list @t38 @t345) (=> (_ @t405 @t345) (_ (_ @t403 (_ tptp.suc @t38)) @t404))) (_ (_ @t403 @t185) @t31))))))
% 152.02/152.37  (assume @p175 (forall @t367 (=> @t400 (=> (forall @t366 @t383) @t359))))
% 152.02/152.37  (assume @p176 (forall (@list @t210 @t213) (=> (= @t210 @t214) (not (= @t210 tptp.zero_zero_nat)))))
% 152.02/152.37  (assume @p177 (forall @t406 (not (= tptp.zero_zero_nat @t211))))
% 152.02/152.37  (assume @p178 (forall @t406 (not (= @t211 tptp.zero_zero_nat))))
% 152.02/152.37  (assume @p179 (forall (@list @t213) (not (= tptp.zero_zero_nat @t214))))
% 152.02/152.37  (assume @p180 (forall (@list @t407 @t268 @t349) (=> (forall (@list @t409 @t408) (=> @t411 (_ (_ tptp.ord_less_nat (_ @t407 @t409)) (_ @t407 @t408)))) (=> @t351 (_ (_ tptp.ord_less_eq_nat (_ @t407 @t268)) (_ @t407 @t349))))))
% 152.02/152.37  (assume @p181 (forall @t208 (=> @t204 (=> @t370 @t187))))
% 152.02/152.37  (assume @p182 (forall @t208 (=> @t412 @t204)))
% 152.02/152.37  (assume @p183 (forall @t208 (=> @t187 @t204)))
% 152.02/152.37  (assume @p184 (= tptp.ord_less_nat (lambda @t416 (and (_ (_ tptp.ord_less_eq_nat @t414) @t413) (not @t415)))))
% 152.02/152.37  (assume @p185 (forall @t189 (=> @t420 @t419)))
% 152.02/152.37  (assume @p186 (forall @t427 (=> @t426 (=> (forall @t424 (=> (= @t349 @t423) @t422)) (=> (forall @t424 (=> (_ @t410 @t349) (=> (_ @t242 @t423) @t422))) @t421)))))
% 152.02/152.37  (assume @p187 (forall (@list @t268 @t349 @t403) (=> @t426 (=> (forall @t424 (_ @t429 @t423)) (=> (forall (@list @t409 @t408 @t428) (=> @t411 (=> (_ (_ tptp.ord_less_nat @t408) @t428) (=> (_ @t429 @t408) (=> (_ (_ @t403 @t408) @t428) (_ @t429 @t428)))))) (_ (_ @t403 @t268) @t349))))))
% 152.02/152.37  (assume @p188 (forall @t353 (=> @t426 (=> @t433 @t431))))
% 152.02/152.37  (assume @p189 (forall @t208 (=> @t231 @t187)))
% 152.02/152.37  (assume @p190 (forall @t189 (=> @t420 (=> @t418 @t348))))
% 152.02/152.37  (assume @p191 (forall @t189 (= @t436 (exists (@list @t434) (and (= @t185 (_ tptp.suc @t434)) (_ @t265 @t434))))))
% 152.02/152.37  (assume @p192 (forall @t444 (= @t443 (and @t359 (forall @t441 (=> @t440 @t438))))))
% 152.02/152.37  (assume @p193 (forall @t208 (= @t445 @t418)))
% 152.02/152.37  (assume @p194 (forall @t208 (= @t446 @t412)))
% 152.02/152.37  (assume @p195 @t453)
% 152.02/152.37  (assume @p196 (forall @t208 (=> @t187 @t446)))
% 152.02/152.37  (assume @p197 (forall @t208 (=> @t446 (=> @t445 @t348))))
% 152.02/152.37  (assume @p198 (forall @t208 (=> @t187 (=> (not (= @t224 @t31)) @t454))))
% 152.02/152.37  (assume @p199 (forall @t456 (=> @t431 @t455)))
% 152.02/152.37  (assume @p200 (forall @t208 (=> @t454 @t187)))
% 152.02/152.37  (assume @p201 (forall @t456 (=> @t457 (=> (not (= @t270 @t430)) @t455))))
% 152.02/152.37  (assume @p202 (forall @t229 (not (_ @t458 tptp.zero_zero_nat))))
% 152.02/152.37  (assume @p203 (forall @t367 (=> @t400 (=> (forall @t366 (=> (_ @t164 @t75) @t365)) @t359))))
% 152.02/152.37  (assume @p204 (forall @t208 (=> @t187 @t267)))
% 152.02/152.37  (assume @p205 (forall @t167 (= @t459 @t266)))
% 152.02/152.37  (assume @p206 (forall @t167 (=> @t267 @t165)))
% 152.02/152.37  (assume @p207 (forall @t464 (=> @t204 (_ (_ tptp.ord_less_eq_nat @t463) @t462))))
% 152.02/152.37  (assume @p208 (forall (@list @t227 @t466 @t344) (=> (_ @t394 @t466) (=> (_ @t465 @t466) (= (_ (_ tptp.ord_less_eq_nat (_ @t467 @t227)) (_ @t467 @t344)) (_ @t465 @t227))))))
% 152.02/152.37  (assume @p209 (forall @t208 (_ (_ tptp.ord_less_eq_nat @t206) @t185)))
% 152.02/152.37  (assume @p210 (forall @t464 (=> @t204 (_ (_ tptp.ord_less_eq_nat (_ @t205 @t460)) (_ @t161 @t460)))))
% 152.02/152.37  (assume @p211 (forall @t473 (=> @t472 (=> @t471 (= (_ (_ tptp.minus_minus_nat @t469) @t468) @t206)))))
% 152.02/152.37  (assume @p212 (forall @t473 (=> @t472 (=> @t471 (= (_ (_ tptp.ord_less_eq_nat @t469) @t468) @t204)))))
% 152.02/152.37  (assume @p213 (forall @t473 (=> @t472 (=> @t471 (= (= @t469 @t468) @t348)))))
% 152.02/152.37  (assume @p214 (forall (@list @t242 @t270 @t268) (=> @t347 (=> @t402 (_ @t242 (_ (_ tptp.minus_minus_nat @t270) @t268))))))
% 152.02/152.37  (assume @p215 (forall @t273 (= (_ @t205 tptp.zero_zero_nat) @t185)))
% 152.02/152.37  (assume @p216 (forall @t208 (=> @t207 (=> (= @t188 tptp.zero_zero_nat) @t348))))
% 152.02/152.37  (assume @p217 (forall (@list @t349 @t270 @t31) (=> @t433 (_ (_ tptp.ord_less_nat (_ (_ tptp.minus_minus_nat @t349) @t31)) @t270))))
% 152.02/152.37  (assume @p218 (forall @t464 (=> @t187 (=> (_ @t186 @t460) (_ (_ tptp.ord_less_nat @t463) @t462)))))
% 152.02/152.37  (assume @p219 (forall @t329 (=> @t107 @t474)))
% 152.02/152.37  (assume @p220 (forall @t334 (=> @t119 @t474)))
% 152.02/152.37  (assume @p221 (forall @t331 (=> @t113 @t474)))
% 152.02/152.37  (assume @p222 (forall (@list @t99 @t100 @t62 @t103) (=> @t107 (=> @t177 (=> (_ @t104 @t373) (exists @t97 (and @t96 (exists (@list @t475) (and (_ (_ tptp.member_nat_e @t475) (_ @t141 (lambda @t46 @t105))) (= @t103 (_ (_ @t138 @t92) @t475)))))))))))
% 152.02/152.37  (assume @p223 (forall (@list @t108 @t100 @t62 @t17) (=> @t113 (=> @t177 (=> (_ @t18 @t374) (exists @t97 (and @t96 (exists @t94 (and (_ @t93 (_ @t82 (lambda @t46 @t111))) (= @t17 (_ (_ @t143 @t92) @t91)))))))))))
% 152.02/152.37  (assume @p224 (forall (@list @t114 @t100 @t62 @t17) (=> @t119 (=> @t177 (=> (_ @t18 @t375) (exists @t97 (and @t96 (exists @t94 (and (_ @t93 (_ @t82 (lambda @t46 @t117))) (= @t17 (_ (_ @t145 @t92) @t91)))))))))))
% 152.02/152.37  (assume @p225 (forall @t482 (=> (forall @t366 (_ (_ tptp.ord_less_eq_nat @t481) @t480)) (=> @t479 (_ (_ tptp.ord_less_eq_nat @t478) @t476)))))
% 152.02/152.37  (assume @p226 (forall @t488 (=> (forall @t366 (_ (_ tptp.ord_less_eq_set_a @t487) @t486)) (=> @t479 (_ (_ tptp.ord_less_eq_set_a @t485) @t484)))))
% 152.02/152.37  (assume @p227 (forall @t482 (=> (forall @t366 (_ (_ tptp.ord_less_eq_nat @t480) @t481)) (=> @t479 (_ (_ tptp.ord_less_eq_nat @t476) @t478)))))
% 152.02/152.37  (assume @p228 (forall @t488 (=> (forall @t366 (_ (_ tptp.ord_less_eq_set_a @t486) @t487)) (=> @t479 (_ (_ tptp.ord_less_eq_set_a @t484) @t485)))))
% 152.02/152.37  (assume @p229 (forall (@list @t407 @t31 @t185) (=> @t490 (= (_ @t489 (_ @t407 @t185)) @t371))))
% 152.02/152.37  (assume @p230 (forall @t482 (=> @t490 (=> (_ @t265 @t477) (_ @t489 @t478)))))
% 152.02/152.37  (assume @p231 @t492)
% 152.02/152.37  (assume @p232 (= tptp.ord_less_nat (lambda (@list @t413 @t493) (_ (_ tptp.ord_less_eq_nat (_ tptp.suc @t413)) @t493))))
% 152.02/152.37  (assume @p233 (forall @t208 (= @t446 @t204)))
% 152.02/152.37  (assume @p234 (forall @t208 (=> @t204 @t419)))
% 152.02/152.37  (assume @p235 (forall @t208 (=> @t393 @t187)))
% 152.02/152.37  (assume @p236 (forall @t427 (=> @t351 (=> @t496 (=> (forall @t366 (=> @t495 (=> @t494 @t401))) @t421)))))
% 152.02/152.37  (assume @p237 (forall @t427 (=> @t351 (=> @t421 (=> (forall @t366 (=> @t495 (=> @t494 @t383))) @t496)))))
% 152.02/152.37  (assume @p238 (forall @t208 (= @t393 @t187)))
% 152.02/152.37  (assume @p239 (forall @t208 (=> @t187 @t393)))
% 152.02/152.37  (assume @p240 (forall @t367 (=> @t359 (=> @t501 (exists @t500 (and (_ (_ tptp.ord_less_eq_nat @t428) @t31) (forall @t499 (=> (_ (_ tptp.ord_less_nat @t497) @t428) @t498)) (_ @t242 @t428)))))))
% 152.02/152.37  (assume @p241 (forall @t208 (= @t446 (or (= @t185 tptp.zero_zero_nat) (exists @t41 (and (= @t185 (_ tptp.suc @t39)) (_ (_ tptp.ord_less_nat @t39) @t31)))))))
% 152.02/152.37  (assume @p242 (forall @t167 (=> @t165 @t396)))
% 152.02/152.37  (assume @p243 (forall @t444 (= @t443 (and @t400 (forall @t441 (=> @t440 @t502))))))
% 152.02/152.37  (assume @p244 (forall @t167 (= @t165 (exists (@list @t414) (= @t31 (_ tptp.suc @t414))))))
% 152.02/152.37  (assume @p245 (forall @t444 (= @t451 (or @t400 (exists @t441 (and @t440 @t502))))))
% 152.02/152.37  (assume @p246 (forall @t189 (=> @t223 (= @t272 (_ tptp.suc @t206)))))
% 152.02/152.37  (assume @p247 (forall (@list @t227 @t344 @t466) (=> (_ @t458 @t344) (=> (_ (_ tptp.ord_less_eq_nat @t466) @t227) (_ (_ tptp.ord_less_nat (_ @t503 @t466)) (_ (_ tptp.minus_minus_nat @t344) @t466))))))
% 152.02/152.37  (assume @p248 (forall @t473 (=> @t472 (=> @t471 (= (_ (_ tptp.ord_less_nat @t469) @t468) @t187)))))
% 152.02/152.37  (assume @p249 (forall @t208 (_ @t504 @t224)))
% 152.02/152.37  (assume @p250 (forall @t189 (=> @t371 (= (_ tptp.suc (_ @t205 @t225)) @t206))))
% 152.02/152.37  (assume @p251 (forall @t189 (=> @t165 (=> (_ @t164 @t185) (_ @t504 @t185)))))
% 152.02/152.37  (assume @p252 (forall (@list @t99 @t100 @t123 @t505) (=> @t107 (=> @t507 (=> (_ @t506 @t123) (_ @t506 @t105))))))
% 152.02/152.37  (assume @p253 (forall (@list @t114 @t100 @t4 @t2) (=> @t119 (=> @t508 (=> @t5 (_ @t3 @t117))))))
% 152.02/152.37  (assume @p254 (forall (@list @t108 @t100 @t4 @t2) (=> @t113 (=> @t509 (=> @t5 (_ @t3 @t111))))))
% 152.02/152.37  (assume @p255 (forall @t329 (=> @t107 (_ @t130 @t105))))
% 152.02/152.37  (assume @p256 (forall @t334 (=> @t119 (_ @t134 @t117))))
% 152.02/152.37  (assume @p257 (forall @t331 (=> @t113 (_ @t132 @t111))))
% 152.02/152.37  (assume @p258 (forall @t367 (=> @t359 (=> @t501 (exists @t500 (and (_ (_ tptp.ord_less_nat @t428) @t31) (forall @t499 (=> (_ (_ tptp.ord_less_eq_nat @t497) @t428) @t498)) (_ @t242 (_ tptp.suc @t428))))))))
% 152.02/152.37  (assume @p259 (forall (@list @t31 @t268) (=> @t165 (_ (_ tptp.ord_less_nat (_ @t161 @t430)) @t31))))
% 152.02/152.37  (assume @p260 (forall @t336 (=> @t107 (=> @t507 @t175))))
% 152.02/152.37  (assume @p261 (forall @t340 (=> @t119 (=> @t508 @t180))))
% 152.02/152.37  (assume @p262 (forall @t338 (=> @t113 (=> @t509 @t183))))
% 152.02/152.37  (assume @p263 (forall @t336 (=> @t107 (=> @t125 @t175))))
% 152.02/152.37  (assume @p264 (forall @t340 (=> @t119 (=> @t129 @t180))))
% 152.02/152.37  (assume @p265 (forall @t338 (=> @t113 (=> @t127 @t183))))
% 152.02/152.37  (assume @p266 (forall @t513 (=> @t10 (=> @t27 (=> (and @t512 @t56) @t511)))))
% 152.02/152.37  (assume @p267 (forall @t513 (=> @t10 (=> @t27 (=> @t512 (=> @t56 @t511))))))
% 152.02/152.37  (assume @p268 (forall (@list @t238 @t254 @t514) (= (= @t521 @t516) @t519)))
% 152.02/152.37  (assume @p269 (forall (@list @t514 @t238 @t254) (= (= @t516 @t521) @t519)))
% 152.02/152.37  (assume @p270 (forall @t529 (=> @t67 (=> @t10 (=> (and @t65 @t528) @t525)))))
% 152.02/152.37  (assume @p271 (forall @t529 (=> @t67 (=> @t10 (=> @t65 (=> @t528 @t525))))))
% 152.02/152.37  (assume @p272 (forall @t534 (=> @t67 (=> (and @t65 @t533) @t531))))
% 152.02/152.37  (assume @p273 (_ @t535 @t1))
% 152.02/152.37  (assume @p274 (forall @t539 (=> @t538 (=> (not @t537) (_ (_ tptp.ord_less_set_a @t254) @t536)))))
% 152.02/152.37  (assume @p275 (forall (@list @t244 @t540) (=> (forall (@list @t73) (=> (_ @t83 @t244) (_ @t83 @t540))) @t541)))
% 152.02/152.37  (assume @p276 (forall (@list @t249 @t542) (=> (forall (@list @t92) (=> (_ @t95 @t249) (_ @t95 @t542))) @t543)))
% 152.02/152.37  (assume @p277 (forall @t539 (=> (forall (@list @t544) (=> (_ @t545 @t254) (_ @t545 @t536))) @t538)))
% 152.02/152.37  (assume @p278 (forall @t539 (=> @t538 (=> (_ (_ tptp.ord_less_eq_set_a @t536) @t254) @t537))))
% 152.02/152.37  (assume @p279 (forall @t258 (= (_ @t546 tptp.bot_bot_set_a) @t254)))
% 152.02/152.37  (assume @p280 (forall @t258 (= (_ (_ tptp.minus_minus_set_a tptp.bot_bot_set_a) @t254) tptp.bot_bot_set_a)))
% 152.02/152.37  (assume @p281 (forall @t258 (= (_ @t546 @t254) tptp.bot_bot_set_a)))
% 152.02/152.37  (assume @p282 (forall (@list @t547) (not (_ (_ tptp.member_nat_a @t547) tptp.bot_bot_set_nat_a))))
% 152.02/152.37  (assume @p283 (forall (@list @t548) (not (_ (_ tptp.member_nat_b @t548) tptp.bot_bot_set_nat_b))))
% 152.02/152.37  (assume @p284 (forall (@list @t549) (not (_ (_ tptp.member_a @t549) tptp.bot_bot_set_a))))
% 152.02/152.37  (assume @p285 (forall @t248 (= (forall @t247 (not @t246)) (= @t244 tptp.bot_bot_set_nat_a))))
% 152.02/152.37  (assume @p286 (forall @t253 (= (forall @t252 (not @t251)) (= @t249 tptp.bot_bot_set_nat_b))))
% 152.02/152.37  (assume @p287 (forall @t258 (= (forall @t257 (not @t256)) @t550)))
% 152.02/152.37  (assume @p288 (forall @t552 (= (= @t243 tptp.bot_bot_set_nat) @t551)))
% 152.02/152.37  (assume @p289 (forall @t554 (= (= @t240 tptp.bot_bot_set_a) @t553)))
% 152.02/152.37  (assume @p290 (forall @t552 (= (= tptp.bot_bot_set_nat @t243) @t551)))
% 152.02/152.37  (assume @p291 (forall @t554 (= (= tptp.bot_bot_set_a @t240) @t553)))
% 152.02/152.37  (assume @p292 (forall @t560 (=> (not (_ @t559 @t244)) (= (_ @t555 (_ @t558 @t540)) @t556))))
% 152.02/152.37  (assume @p293 (forall @t566 (=> (not (_ @t565 @t249)) (= (_ @t561 (_ @t564 @t542)) @t562))))
% 152.02/152.37  (assume @p294 (forall @t569 (=> (not (_ @t18 @t254)) (= (_ @t546 (_ @t568 @t536)) @t567))))
% 152.02/152.37  (assume @p295 (forall (@list @t557 @t540 @t244) (=> @t571 (= (_ (_ tptp.minus_1788767276_nat_a @t570) @t540) @t556))))
% 152.02/152.37  (assume @p296 (forall (@list @t563 @t542 @t249) (=> @t573 (= (_ (_ tptp.minus_780847917_nat_b @t572) @t542) @t562))))
% 152.02/152.37  (assume @p297 (forall (@list @t17 @t536 @t254) (=> @t575 (= (_ (_ tptp.minus_minus_set_a @t574) @t536) @t567))))
% 152.02/152.37  (assume @p298 (forall (@list @t232 @t540 @t576) (=> (=> (not (_ @t234 @t540)) @t578) (_ @t234 (_ @t577 @t540)))))
% 152.02/152.37  (assume @p299 (forall (@list @t235 @t542 @t579) (=> (=> (not (_ @t237 @t542)) @t581) (_ @t237 (_ @t580 @t542)))))
% 152.02/152.37  (assume @p300 (forall (@list @t238 @t536 @t514) (=> (=> (not (_ @t241 @t536)) @t518) (_ @t241 (_ @t515 @t536)))))
% 152.02/152.37  (assume @p301 (forall (@list @t232 @t576 @t244) (= (_ @t234 (_ @t577 @t244)) (or @t578 (_ @t234 @t244)))))
% 152.02/152.37  (assume @p302 (forall (@list @t235 @t579 @t249) (= (_ @t237 (_ @t580 @t249)) (or @t581 (_ @t237 @t249)))))
% 152.02/152.37  (assume @p303 (forall (@list @t238 @t514 @t254) (= (_ @t241 (_ @t515 @t254)) (or @t518 (_ @t241 @t254)))))
% 152.02/152.37  (assume @p304 (forall (@list @t17 @t254) (= (_ @t568 @t574) @t574)))
% 152.02/152.37  (assume @p305 (forall @t11 (=> @t7 (_ @t535 @t4))))
% 152.02/152.37  (assume @p306 (forall @t11 (=> @t7 (= (_ tptp.carrie1074654371t_unit @t582) @t4))))
% 152.02/152.37  (assume @p307 (forall @t11 (=> @t7 (_ (_ tptp.module1821517916unit_d @t582) tptp.r))))
% 152.02/152.37  (assume @p308 (forall (@list @t4 @t583) (=> @t7 (=> @t585 (=> @t584 (_ (_ (_ tptp.submod903911234t_unit tptp.r) (_ @t510 @t583)) @t4))))))
% 152.02/152.37  (assume @p309 (forall @t8 (=> @t10 (=> @t5 (_ @t3 @t527)))))
% 152.02/152.37  (assume @p310 (forall @t11 (=> @t10 (_ @t9 @t527))))
% 152.02/152.37  (assume @p311 (forall @t11 (=> @t10 (= (_ @t526 @t527) @t527))))
% 152.02/152.37  (assume @p312 (forall (@list @t23 @t4 @t62) (=> @t27 (=> @t10 (=> @t67 (_ (_ tptp.ord_less_eq_set_a (_ @t523 @t23)) @t524))))))
% 152.02/152.37  (assume @p313 (forall @t587 (=> @t67 (=> @t10 (_ @t586 @t1)))))
% 152.02/152.37  (assume @p314 (forall (@list @t62 @t583 @t4) (=> @t67 (=> @t585 (=> @t584 (_ @t586 @t583))))))
% 152.02/152.37  (assume @p315 (forall @t11 (=> @t10 (_ (_ (_ tptp.genera1692266857t_unit tptp.r) (_ @t510 (_ @t15 @t4))) @t4))))
% 152.02/152.37  (assume @p316 (_ @t6 @t532))
% 152.02/152.37  (assume @p317 (= (_ @t15 tptp.bot_bot_set_a) @t532))
% 152.02/152.37  (assume @p318 (forall @t229 (= (_ @t274 @t227) tptp.zero_zero_nat)))
% 152.02/152.37  (assume @p319 (forall @t229 (= (_ @t503 tptp.zero_zero_nat) @t227)))
% 152.02/152.37  (assume @p320 (forall @t229 (= (_ @t503 @t227) tptp.zero_zero_nat)))
% 152.02/152.37  (assume @p321 (forall @t539 (= (= @t567 tptp.bot_bot_set_a) @t538)))
% 152.02/152.37  (assume @p322 (forall @t258 (= (_ @t517 tptp.bot_bot_set_a) @t550)))
% 152.02/152.37  (assume @p323 (forall @t258 (_ (_ tptp.ord_less_eq_set_a tptp.bot_bot_set_a) @t254)))
% 152.02/152.37  (assume @p324 (forall @t560 (= (_ (_ tptp.ord_le157368549_nat_a @t570) @t540) (and @t571 @t541))))
% 152.02/152.37  (assume @p325 (forall @t566 (= (_ (_ tptp.ord_le1296932838_nat_b @t572) @t542) (and @t573 @t543))))
% 152.02/152.37  (assume @p326 (forall @t569 (= (_ (_ tptp.ord_less_eq_set_a @t574) @t536) (and @t575 @t538))))
% 152.02/152.37  (assume @p327 (forall (@list @t238 @t254) (= (_ @t520 (_ @t546 @t588)) @t521)))
% 152.02/152.37  (assume @p328 (forall (@list @t232) (_ @t234 (_ (_ tptp.insert_nat_a @t232) tptp.bot_bot_set_nat_a))))
% 152.02/152.37  (assume @p329 (forall (@list @t235) (_ @t237 (_ (_ tptp.insert_nat_b @t235) tptp.bot_bot_set_nat_b))))
% 152.02/152.37  (assume @p330 (forall @t589 (_ @t241 @t588)))
% 152.02/152.37  (assume @p331 (forall @t587 (=> @t67 (=> @t10 (_ @t6 @t524)))))
% 152.02/152.37  (assume @p332 (forall @t587 (=> @t67 (=> @t10 (= (_ @t523 @t527) @t524)))))
% 152.02/152.37  (assume @p333 (forall @t587 (=> @t67 (=> @t10 (_ @t586 @t527)))))
% 152.02/152.37  (assume @p334 (forall @t587 (=> @t67 (=> @t10 (_ @t535 @t524)))))
% 152.02/152.37  (assume @p335 (forall (@list @t4 @t590) (=> @t170 (=> (_ (_ tptp.ord_less_eq_set_a @t590) @t1) (=> (_ @t9 (_ @t526 @t590)) (_ @t169 @t590))))))
% 152.02/152.37  (assume @p336 (forall @t90 (=> @t67 (= (_ @t523 @t532) @t532))))
% 152.02/152.37  (assume @p337 (forall @t587 (=> @t67 (=> @t170 (=> (= @t89 @t1) (= @t524 @t1))))))
% 152.02/152.37  (assume @p338 (forall @t589 (= (_ tptp.collect_a (lambda @t257 (= @t255 @t238))) @t588)))
% 152.02/152.37  (assume @p339 (forall @t529 (=> @t67 (=> @t10 (=> @t65 (=> @t51 @t525))))))
% 152.02/152.37  (assume @p340 (forall @t529 (=> @t67 (=> @t10 (=> @t65 (=> (_ @t50 (_ @t47 (lambda @t46 @t524))) @t525))))))
% 152.02/152.37  (assume @p341 (forall @t534 (=> @t67 (=> @t65 (=> @t533 @t531)))))
% 152.02/152.37  (assume @p342 (_ (_ tptp.member_nat_a tptp.g) (_ (_ tptp.pi_nat_a @t594) (lambda @t46 @t592))))
% 152.02/152.37  (assume @p343 @t604)
% 152.02/152.37  (assume @p344 (_ (_ tptp.member_nat_b tptp.t) (_ (_ tptp.pi_nat_b @t594) @t53)))
% 152.02/152.37  (assume @p345 (= @t605 tptp.h2))
% 152.02/152.37  (assume @p346 (_ (_ tptp.module_e_b_f_d tptp.n) tptp.r))
% 152.02/152.37  (assume @p347 (_ @t12 tptp.h))
% 152.02/152.37  (assume @p348 (_ @t606 tptp.h))
% 152.02/152.37  (assume @p349 true)
% 152.02/152.37  (assume @p350 (_ @t66 @t52))
% 152.02/152.37  (assume @p351 (_ (_ tptp.ord_less_eq_set_a tptp.h) @t1))
% 152.02/152.37  (assume @p352 (_ @t606 @t1))
% 152.02/152.37  (assume @p353 (_ (_ tptp.ord_less_eq_set_a (_ @t15 tptp.h1)) @t1))
% 152.02/152.37  (assume @p354 (_ (_ tptp.member_a @t607) (_ @t15 @t592)))
% 152.02/152.37  (assume @p355 (= tptp.x @t607))
% 152.02/152.37  (assume @p356 (_ @t608 tptp.h))
% 152.02/152.37  (assume @p357 (not (_ @t608 tptp.h1)))
% 152.02/152.37  (assume @p358 @t609)
% 152.02/152.37  (assume @p359 (_ @t608 @t1))
% 152.02/152.37  (assume @p360 (_ @t6 (_ @t15 (_ @t591 tptp.bot_bot_set_a))))
% 152.02/152.37  (assume @p361 (_ (_ tptp.ord_less_eq_nat tptp.xa) @t610))
% 152.02/152.37  (assume @p362 @t613)
% 152.02/152.37  (assume @p363 @t614)
% 152.02/152.37  (step @p364 (= tptp.ord_less_eq_nat @t615) :rule refl :args (@t615))
% 152.02/152.37  ; WARNING: add trust step for TRUST
% 152.02/152.37  ; trust TRUST PREPROCESS_HO_ELIM
% 152.02/152.37  (step @p365 :rule trust :premises () :args ((= (forall @t167 (or (not @t628) (= @t31 @t627))) (forall @t167 (or (not (_ @t624 @t623 @t31)) (= @t31 (_ @t617 @t616 (_ @t617 (_ @t620 @t619 @t31) @t618))))))))
% 152.02/152.37  (step @p366 :rule refl :args ((tptp.suc @t162)))
% 152.02/152.37  (step @p367 :rule refl :args ((tptp.minus_minus_nat @t31 @t160)))
% 152.02/152.37  (step @p368 :rule refl :args (@t625))
% 152.02/152.37  (step @p369 :rule refl :args (@t31))
% 152.02/152.37  (step @p370 :rule cong :premises (@p369 @p368) :args (@t626))
% 152.02/152.37  (step @p371 :rule trans :premises (@p370 @p367))
% 152.02/152.37  (step @p372 :rule cong :premises (@p371) :args (@t627))
% 152.02/152.37  (step @p373 :rule trans :premises (@p372 @p366))
% 152.02/152.37  (step @p374 :rule refl :args (tptp.suc))
% 152.02/152.37  (step @p375 :rule ho_cong :premises (@p374 @p371))
% 152.02/152.37  (step @p376 :rule cong :premises (@p375 @p373) :args ((= (_ tptp.suc @t626) @t627)))
% 152.02/152.37  (step @p377 :rule symm :premises (@p376))
% 152.02/152.37  (step @p378 :rule refl :args (@t163))
% 152.02/152.37  (step @p379 :rule eq_resolve :premises (@p378 @p377))
% 152.02/152.37  (step @p380 :rule refl :args (@t161))
% 152.02/152.37  (step @p381 :rule ho_cong :premises (@p380 @p368))
% 152.02/152.37  (step @p382 :rule cong :premises (@p381 @p371) :args ((= (_ @t161 @t625) @t626)))
% 152.02/152.37  (step @p383 :rule symm :premises (@p382))
% 152.02/152.37  (step @p384 :rule refl :args (@t162))
% 152.02/152.37  (step @p385 :rule eq_resolve :premises (@p384 @p383))
% 152.02/152.37  (step @p386 :rule refl :args (@t160))
% 152.02/152.37  (step @p387 :rule cong :premises (@p386 @p368) :args ((= @t160 @t625)))
% 152.02/152.37  (step @p388 :rule symm :premises (@p387))
% 152.02/152.37  (step @p389 :rule eq_resolve :premises (@p386 @p388))
% 152.02/152.37  (step @p390 :rule ho_cong :premises (@p380 @p389))
% 152.02/152.37  (step @p391 :rule trans :premises (@p390 @p385))
% 152.02/152.37  (step @p392 :rule ho_cong :premises (@p374 @p391))
% 152.02/152.37  (step @p393 :rule trans :premises (@p392 @p379))
% 152.02/152.37  (step @p394 :rule cong :premises (@p369 @p393) :args (@t629))
% 152.02/152.37  (step @p395 :rule refl :args (@t628))
% 152.02/152.37  (step @p396 :rule refl :args (@t165))
% 152.02/152.37  (step @p397 :rule cong :premises (@p396 @p395) :args ((= @t165 @t628)))
% 152.02/152.37  (step @p398 :rule symm :premises (@p397))
% 152.02/152.37  (step @p399 :rule eq_resolve :premises (@p396 @p398))
% 152.02/152.37  (step @p400 :rule cong :premises (@p399) :args (@t459))
% 152.02/152.37  (step @p401 :rule nary_cong :premises (@p400 @p394) :args (@t630))
% 152.02/152.37  (step @p402 :rule cong :premises (@p401) :args ((forall @t167 @t630)))
% 152.02/152.37  (step @p403 :rule bool-impl-elim :args (@t165 @t629))
% 152.02/152.37  (step @p404 :rule cong :premises (@p403) :args ((forall @t167 (=> @t165 @t629))))
% 152.02/152.37  (step @p405 :rule trans :premises (@p404 @p402))
% 152.02/152.37  (step @p406 :rule eq-symm :args (@t163 @t31))
% 152.02/152.37  (step @p407 :rule refl :args (@t165))
% 152.02/152.37  (step @p408 :rule cong :premises (@p407 @p406) :args (@t166))
% 152.02/152.37  (step @p409 :rule cong :premises (@p408) :args (@t168))
% 152.02/152.37  (step @p410 :rule trans :premises (@p409 @p405))
% 152.02/152.37  (step @p411 :rule trans :premises (@p410 @p365))
% 152.02/152.37  (step @p412 :rule eq_resolve :premises (@p39 @p411))
% 152.02/152.37  (step @p413 :rule instantiate :premises (@p412) :args ((@list tptp.m2)))
% 152.02/152.37  ; trust TRUST PREPROCESS_HO_ELIM
% 152.02/152.37  (step @p414 :rule trust :premises () :args ((= @t609 @t631)))
% 152.02/152.37  (step @p415 :rule eq_resolve :premises (@p358 @p414))
% 152.02/152.37  (step @p416 :rule cnf_or_pos :args (@t636))
% 152.02/152.37  (step @p417 :rule reordering :premises (@p416) :args ((or @t635 @t634 (not @t636))))
% 152.02/152.37  (step @p418 :rule chain_m_resolution :premises (@p417 @p415 @p413) :args (@t634 (@list false false) (@list @t631 @t636)))
% 152.02/152.37  ; trust TRUST PREPROCESS_HO_ELIM
% 152.02/152.37  (step @p419 :rule trust :premises () :args ((= (and @t645 (forall @t638 @t644)) (and (forall @t642 (or (not (_ @t624 @t641 @t639)) (_ @t624 @t641 (_ @t617 @t616 @t639)))) (forall @t638 (_ @t624 (_ @t622 @t621 @t637) (_ @t617 @t616 @t637)))))))
% 152.02/152.37  (step @p420 :rule aci_norm :args ((= (or false @t644) @t644)))
% 152.02/152.37  (step @p421 :rule refl :args (@t644))
% 152.02/152.37  (step @p422 :rule evaluate :args ((not true)))
% 152.02/152.37  (step @p423 :rule eq-refl :args (@t637))
% 152.02/152.37  (step @p424 :rule cong :premises (@p423) :args (@t646))
% 152.02/152.37  (step @p425 :rule trans :premises (@p424 @p422))
% 152.02/152.37  (step @p426 :rule nary_cong :premises (@p425 @p421) :args (@t647))
% 152.02/152.37  (step @p427 :rule trans :premises (@p426 @p420))
% 152.02/152.37  (step @p428 :rule cong :premises (@p427) :args ((forall @t638 @t647)))
% 152.02/152.37  (step @p429 :rule quant-var-elim-eq :args ((= (forall @t652 @t651) @t647)))
% 152.02/152.37  (step @p430 :rule aci_norm :args ((= @t653 @t651)))
% 152.02/152.37  (step @p431 :rule cong :premises (@p430) :args (@t654))
% 152.02/152.37  (step @p432 :rule trans :premises (@p431 @p429))
% 152.02/152.37  (step @p433 :rule cong :premises (@p432) :args (@t655))
% 152.02/152.37  (step @p434 :rule quant-merge-prenex :args ((= @t655 @t656)))
% 152.02/152.37  (step @p435 :rule symm :premises (@p434))
% 152.02/152.37  (step @p436 :rule quant_var_reordering :args ((= (forall @t657 @t653) @t656)))
% 152.02/152.37  (step @p437 :rule trans :premises (@p436 @p435 @p433))
% 152.02/152.37  (step @p438 :rule trans :premises (@p437 @p428))
% 152.02/152.37  (step @p439 :rule refl :args (@t649))
% 152.02/152.37  (step @p440 :rule eq-symm :args (@t637 @t648))
% 152.02/152.37  (step @p441 :rule cong :premises (@p440) :args (@t658))
% 152.02/152.37  (step @p442 :rule nary_cong :premises (@p441 @p439) :args (@t659))
% 152.02/152.37  (step @p443 :rule cong :premises (@p442) :args (@t660))
% 152.02/152.37  (step @p444 :rule trans :premises (@p443 @p438))
% 152.02/152.37  (step @p445 :rule refl :args (@t645))
% 152.02/152.37  (step @p446 :rule nary_cong :premises (@p445 @p444) :args ((and @t645 @t660)))
% 152.02/152.37  (step @p447 :rule alpha_equiv :args (@t665 @t666 (@list @t648 @t637)))
% 152.02/152.37  (step @p448 :rule alpha_equiv :args (@t670 @t666 (@list @t640 @t639)))
% 152.02/152.37  (step @p449 :rule nary_cong :premises (@p448 @p447) :args (@t671))
% 152.02/152.37  (step @p450 :rule quant-miniscope-and :args ((= (forall @t208 (and @t669 @t664)) @t671)))
% 152.02/152.37  (step @p451 :rule trans :premises (@p450 @p449))
% 152.02/152.37  (step @p452 :rule trans :premises (@p451 @p446))
% 152.02/152.37  (step @p453 :rule bool-or-and-distrib :args (@t668 @t663 true @t662 false))
% 152.02/152.37  (step @p454 :rule cong :premises (@p453) :args ((forall @t208 (or @t672 @t662))))
% 152.02/152.37  (step @p455 :rule trans :premises (@p454 @p452))
% 152.02/152.37  (step @p456 :rule refl :args ((tptp.ord_less_nat @t185 @t225)))
% 152.02/152.37  (step @p457 :rule refl :args (@t661))
% 152.02/152.37  (step @p458 :rule refl :args (@t185))
% 152.02/152.37  (step @p459 :rule cong :premises (@p458 @p457) :args (@t662))
% 152.02/152.37  (step @p460 :rule trans :premises (@p459 @p456))
% 152.02/152.37  (step @p461 :rule refl :args (@t186))
% 152.02/152.37  (step @p462 :rule ho_cong :premises (@p461 @p457))
% 152.02/152.37  (step @p463 :rule cong :premises (@p462 @p460) :args ((= (_ @t186 @t661) @t662)))
% 152.02/152.37  (step @p464 :rule symm :premises (@p463))
% 152.02/152.37  (step @p465 :rule refl :args (@t446))
% 152.02/152.37  (step @p466 :rule eq_resolve :premises (@p465 @p464))
% 152.02/152.37  (step @p467 :rule refl :args (@t225))
% 152.02/152.37  (step @p468 :rule cong :premises (@p467 @p457) :args ((= @t225 @t661)))
% 152.02/152.37  (step @p469 :rule symm :premises (@p468))
% 152.02/152.37  (step @p470 :rule eq_resolve :premises (@p467 @p469))
% 152.02/152.37  (step @p471 :rule ho_cong :premises (@p461 @p470))
% 152.02/152.37  (step @p472 :rule trans :premises (@p471 @p466))
% 152.02/152.37  (step @p473 :rule refl :args (@t663))
% 152.02/152.37  (step @p474 :rule refl :args (@t667))
% 152.02/152.37  (step @p475 :rule refl :args (@t187))
% 152.02/152.37  (step @p476 :rule cong :premises (@p475 @p474) :args ((= @t187 @t667)))
% 152.02/152.37  (step @p477 :rule symm :premises (@p476))
% 152.02/152.37  (step @p478 :rule eq_resolve :premises (@p475 @p477))
% 152.02/152.37  (step @p479 :rule cong :premises (@p478) :args (@t445))
% 152.02/152.37  (step @p480 :rule nary_cong :premises (@p479 @p473) :args (@t673))
% 152.02/152.37  (step @p481 :rule nary_cong :premises (@p480 @p472) :args (@t674))
% 152.02/152.37  (step @p482 :rule cong :premises (@p481) :args ((forall @t208 @t674)))
% 152.02/152.37  (step @p483 :rule trans :premises (@p482 @p455))
% 152.02/152.37  (step @p484 :rule bool-or-de-morgan :args (@t187 @t417 false))
% 152.02/152.37  (step @p485 :rule nary_cong :premises (@p484 @p465) :args ((or @t676 @t446)))
% 152.02/152.37  (step @p486 :rule bool-impl-elim :args (@t675 @t446))
% 152.02/152.37  (step @p487 :rule trans :premises (@p486 @p485))
% 152.02/152.37  (step @p488 :rule cong :premises (@p487) :args ((forall @t208 (=> @t675 @t446))))
% 152.02/152.37  (step @p489 :rule trans :premises (@p488 @p483))
% 152.02/152.37  (step @p490 :rule refl :args (@t446))
% 152.02/152.37  (step @p491 :rule eq-symm :args (@t185 @t31))
% 152.02/152.37  (step @p492 :rule refl :args (@t187))
% 152.02/152.37  (step @p493 :rule nary_cong :premises (@p492 @p491) :args (@t412))
% 152.02/152.37  (step @p494 :rule beta-reduce :args ((= (_ @t678 @t31) @t412)))
% 152.02/152.37  (step @p495 :rule trans :premises (@p494 @p493))
% 152.02/152.37  (step @p496 :rule refl :args (@t31))
% 152.02/152.37  (step @p497 :rule beta-reduce :args ((= @t679 @t678)))
% 152.02/152.37  (step @p498 :rule ho_cong :premises (@p497 @p496))
% 152.02/152.37  (step @p499 :rule trans :premises (@p498 @p495))
% 152.02/152.37  (step @p500 :rule cong :premises (@p499 @p490) :args (@t681))
% 152.02/152.37  (step @p501 :rule cong :premises (@p500) :args ((forall @t208 @t681)))
% 152.02/152.37  (step @p502 :rule trans :premises (@p501 @p489))
% 152.02/152.37  (step @p503 :rule refl :args (@t185))
% 152.02/152.37  (step @p504 :rule ho_cong :premises (@p364 @p503))
% 152.02/152.37  (step @p505 :rule ho_cong :premises (@p504 @p496))
% 152.02/152.37  (step @p506 :rule cong :premises (@p505 @p490) :args (@t491))
% 152.02/152.37  (step @p507 :rule cong :premises (@p506) :args (@t492))
% 152.02/152.37  (step @p508 :rule trans :premises (@p507 @p502))
% 152.02/152.37  (step @p509 :rule trans :premises (@p508 @p419))
% 152.02/152.37  (step @p510 :rule eq_resolve :premises (@p231 @p509))
% 152.02/152.37  (step @p511 :rule and_elim :premises (@p510) :args (1))
% 152.02/152.37  (step @p512 :rule instantiate :premises (@p511) :args ((@list tptp.xa)))
% 152.02/152.37  (step @p513 :rule cnf_or_neg :args (@t686 0))
% 152.02/152.37  (step @p514 :rule reordering :premises (@p513) :args ((or @t687 @t686)))
% 152.02/152.37  (step @p515 :rule cnf_and_pos :args (@t690 0))
% 152.02/152.37  (step @p516 :rule reordering :premises (@p515) :args ((or @t687 @t691)))
% 152.02/152.37  (step @p517 :rule eq-symm :args (@t695 @t696))
% 152.02/152.37  (step @p518 :rule cong :premises (@p517) :args (@t697))
% 152.02/152.37  ; trust TRUST PREPROCESS_HO_ELIM
% 152.02/152.37  (step @p519 :rule trust :premises () :args ((= (forall @t444 (= @t704 (or @t702 @t701))) @t697)))
% 152.02/152.37  (step @p520 :rule refl :args (@t701))
% 152.02/152.37  (step @p521 :rule refl :args (@t702))
% 152.02/152.37  (step @p522 :rule refl :args (@t359))
% 152.02/152.37  (step @p523 :rule cong :premises (@p522 @p521) :args ((= @t359 @t702)))
% 152.02/152.37  (step @p524 :rule symm :premises (@p523))
% 152.02/152.37  (step @p525 :rule eq_resolve :premises (@p522 @p524))
% 152.02/152.37  (step @p526 :rule nary_cong :premises (@p525 @p520) :args (@t705))
% 152.02/152.37  (step @p527 :rule refl :args (@t704))
% 152.02/152.37  (step @p528 :rule cong :premises (@p527 @p526) :args (@t706))
% 152.02/152.37  (step @p529 :rule cong :premises (@p528) :args ((forall @t444 @t706)))
% 152.02/152.37  (step @p530 :rule refl :args (@t698))
% 152.02/152.37  (step @p531 :rule refl :args (@t438))
% 152.02/152.37  (step @p532 :rule cong :premises (@p531 @p530) :args ((= @t438 @t698)))
% 152.02/152.37  (step @p533 :rule symm :premises (@p532))
% 152.02/152.37  (step @p534 :rule eq_resolve :premises (@p531 @p533))
% 152.02/152.37  (step @p535 :rule cong :premises (@p534) :args (@t707))
% 152.02/152.37  (step @p536 :rule refl :args (@t700))
% 152.02/152.37  (step @p537 :rule refl :args (@t440))
% 152.02/152.37  (step @p538 :rule cong :premises (@p537 @p536) :args ((= @t440 @t700)))
% 152.02/152.37  (step @p539 :rule symm :premises (@p538))
% 152.02/152.37  (step @p540 :rule eq_resolve :premises (@p537 @p539))
% 152.02/152.37  (step @p541 :rule cong :premises (@p540) :args (@t708))
% 152.02/152.37  (step @p542 :rule nary_cong :premises (@p541 @p535) :args (@t709))
% 152.02/152.37  (step @p543 :rule cong :premises (@p542) :args ((forall @t441 @t709)))
% 152.02/152.37  (step @p544 :rule bool-and-de-morgan :args (@t440 @t438 true))
% 152.02/152.37  (step @p545 :rule cong :premises (@p544) :args (@t710))
% 152.02/152.37  (step @p546 :rule trans :premises (@p545 @p543))
% 152.02/152.37  (step @p547 :rule cong :premises (@p546) :args (@t711))
% 152.02/152.37  (step @p548 :rule exists-elim :args ((= @t448 @t711)))
% 152.02/152.37  (step @p549 :rule trans :premises (@p548 @p547))
% 152.02/152.37  (step @p550 :rule refl :args (@t359))
% 152.02/152.37  (step @p551 :rule nary_cong :premises (@p550 @p549) :args (@t449))
% 152.02/152.37  (step @p552 :rule refl :args ((tptp.ord_less_nat @t437 @t225)))
% 152.02/152.37  (step @p553 :rule refl :args (@t437))
% 152.02/152.37  (step @p554 :rule cong :premises (@p553 @p457) :args (@t703))
% 152.02/152.37  (step @p555 :rule trans :premises (@p554 @p552))
% 152.02/152.37  (step @p556 :rule refl :args (@t439))
% 152.02/152.37  (step @p557 :rule ho_cong :premises (@p556 @p457))
% 152.02/152.37  (step @p558 :rule cong :premises (@p557 @p555) :args ((= (_ @t439 @t661) @t703)))
% 152.02/152.37  (step @p559 :rule symm :premises (@p558))
% 152.02/152.37  (step @p560 :rule refl :args (@t442))
% 152.02/152.37  (step @p561 :rule eq_resolve :premises (@p560 @p559))
% 152.02/152.37  (step @p562 :rule ho_cong :premises (@p556 @p470))
% 152.02/152.37  (step @p563 :rule trans :premises (@p562 @p561))
% 152.02/152.37  (step @p564 :rule cong :premises (@p563) :args (@t712))
% 152.02/152.37  (step @p565 :rule nary_cong :premises (@p564 @p535) :args (@t713))
% 152.02/152.37  (step @p566 :rule cong :premises (@p565) :args ((forall @t441 @t713)))
% 152.02/152.37  (step @p567 :rule bool-and-de-morgan :args (@t442 @t438 true))
% 152.02/152.37  (step @p568 :rule cong :premises (@p567) :args (@t714))
% 152.02/152.37  (step @p569 :rule trans :premises (@p568 @p566))
% 152.02/152.37  (step @p570 :rule cong :premises (@p569) :args (@t715))
% 152.02/152.37  (step @p571 :rule exists-elim :args ((= @t451 @t715)))
% 152.02/152.37  (step @p572 :rule trans :premises (@p571 @p570))
% 152.02/152.37  (step @p573 :rule cong :premises (@p572 @p551) :args (@t452))
% 152.02/152.37  (step @p574 :rule cong :premises (@p573) :args (@t453))
% 152.02/152.37  (step @p575 :rule trans :premises (@p574 @p529))
% 152.02/152.37  (step @p576 :rule trans :premises (@p575 @p519 @p518))
% 152.02/152.37  (step @p577 :rule eq_resolve :premises (@p195 @p576))
% 152.02/152.37  (step @p578 :rule instantiate :premises (@p577) :args ((@list @t632 @t682)))
% 152.02/152.37  (step @p579 :rule cnf_equiv_pos1 :args (@t718))
% 152.02/152.37  (step @p580 :rule reordering :premises (@p579) :args ((or @t717 (not @t686) (not @t718))))
% 152.02/152.37  ; trust TRUST PREPROCESS_HO_ELIM
% 152.02/152.37  (step @p581 :rule trust :premises () :args ((= (forall @t208 (= @t672 (or @t720 (= @t185 @t661)))) @t719)))
% 152.02/152.37  (step @p582 :rule cong :premises (@p458 @p470) :args (@t387))
% 152.02/152.37  (step @p583 :rule refl :args ((tptp.ord_less_nat @t225 @t185)))
% 152.02/152.37  (step @p584 :rule cong :premises (@p457 @p458) :args (@t720))
% 152.02/152.37  (step @p585 :rule trans :premises (@p584 @p583))
% 152.02/152.37  (step @p586 :rule refl :args (tptp.ord_less_nat))
% 152.02/152.37  (step @p587 :rule ho_cong :premises (@p586 @p457))
% 152.02/152.37  (step @p588 :rule ho_cong :premises (@p587 @p458))
% 152.02/152.37  (step @p589 :rule cong :premises (@p588 @p585) :args ((= (_ (_ tptp.ord_less_nat @t661) @t185) @t720)))
% 152.02/152.37  (step @p590 :rule symm :premises (@p589))
% 152.02/152.37  (step @p591 :rule refl :args (@t436))
% 152.02/152.37  (step @p592 :rule eq_resolve :premises (@p591 @p590))
% 152.02/152.37  (step @p593 :rule ho_cong :premises (@p586 @p470))
% 152.02/152.37  (step @p594 :rule ho_cong :premises (@p593 @p458))
% 152.02/152.37  (step @p595 :rule trans :premises (@p594 @p592))
% 152.02/152.37  (step @p596 :rule nary_cong :premises (@p595 @p582) :args (@t721))
% 152.02/152.37  (step @p597 :rule cong :premises (@p480 @p596) :args (@t722))
% 152.02/152.37  (step @p598 :rule cong :premises (@p597) :args ((forall @t208 @t722)))
% 152.02/152.37  (step @p599 :rule refl :args (@t721))
% 152.02/152.37  (step @p600 :rule cong :premises (@p484 @p599) :args (@t723))
% 152.02/152.37  (step @p601 :rule cong :premises (@p600) :args ((forall @t208 @t723)))
% 152.02/152.37  (step @p602 :rule trans :premises (@p601 @p598))
% 152.02/152.37  (step @p603 :rule eq-symm :args (@t721 @t676))
% 152.02/152.37  (step @p604 :rule cong :premises (@p499) :args (@t724))
% 152.02/152.37  (step @p605 :rule eq-symm :args (@t225 @t185))
% 152.02/152.37  (step @p606 :rule refl :args (@t436))
% 152.02/152.37  (step @p607 :rule nary_cong :premises (@p606 @p605) :args (@t725))
% 152.02/152.37  (step @p608 :rule beta-reduce :args ((= (_ @t726 @t185) @t725)))
% 152.02/152.37  (step @p609 :rule trans :premises (@p608 @p607))
% 152.02/152.37  (step @p610 :rule beta-reduce :args ((= @t727 @t726)))
% 152.02/152.37  (step @p611 :rule ho_cong :premises (@p610 @p503))
% 152.02/152.37  (step @p612 :rule trans :premises (@p611 @p609))
% 152.02/152.37  (step @p613 :rule cong :premises (@p612 @p604) :args ((= @t728 @t724)))
% 152.02/152.37  (step @p614 :rule trans :premises (@p613 @p603))
% 152.02/152.37  (step @p615 :rule eq-symm :args (@t724 @t728))
% 152.02/152.37  (step @p616 :rule trans :premises (@p615 @p614))
% 152.02/152.37  (step @p617 :rule cong :premises (@p616) :args ((forall @t208 (= @t724 @t728))))
% 152.02/152.37  (step @p618 :rule trans :premises (@p617 @p602))
% 152.02/152.37  (step @p619 :rule refl :args (@t225))
% 152.02/152.37  (step @p620 :rule ho_cong :premises (@p364 @p619))
% 152.02/152.37  (step @p621 :rule ho_cong :premises (@p620 @p503))
% 152.02/152.37  (step @p622 :rule cong :premises (@p505) :args (@t384))
% 152.02/152.37  (step @p623 :rule cong :premises (@p622 @p621) :args (@t385))
% 152.02/152.37  (step @p624 :rule cong :premises (@p623) :args (@t386))
% 152.02/152.37  (step @p625 :rule trans :premises (@p624 @p618))
% 152.02/152.37  (step @p626 :rule trans :premises (@p625 @p581))
% 152.02/152.37  (step @p627 :rule eq_resolve :premises (@p158 @p626))
% 152.02/152.37  (step @p628 :rule refl :args (@t730))
% 152.02/152.37  (step @p629 :rule eq-symm :args (@t632 tptp.xa))
% 152.02/152.37  (step @p630 :rule cong :premises (@p629) :args (@t731))
% 152.02/152.37  (step @p631 :rule refl :args (@t687))
% 152.02/152.37  (step @p632 :rule nary_cong :premises (@p631 @p630) :args (@t732))
% 152.02/152.37  (step @p633 :rule cong :premises (@p632 @p628) :args (@t733))
% 152.02/152.37  (step @p634 :rule refl :args (@t719))
% 152.02/152.37  (step @p635 :rule cong :premises (@p634 @p633) :args ((=> @t719 @t733)))
% 152.02/152.37  (assume-push @p1002 @t719)
% 152.02/152.37  (step @p637 :rule instantiate :premises (@p627) :args ((@list tptp.xa @t632)))
% 152.02/152.37  (step-pop @p1003 :rule scope :premises (@p637))
% 152.02/152.37  (step @p638 :rule process_scope :premises (@p1003) :args (@t733))
% 152.02/152.37  (step @p640 :rule eq_resolve :premises (@p638 @p635))
% 152.02/152.37  (step @p641 :rule implies_elim :premises (@p640))
% 152.02/152.37  (step @p642 :rule chain_m_resolution :premises (@p641 @p627) :args (@t734 @t735 (@list @t719)))
% 152.02/152.37  (step @p643 :rule cnf_equiv_pos2 :args (@t734))
% 152.02/152.37  (step @p644 :rule reordering :premises (@p643) :args ((or @t690 @t736 (not @t734))))
% 152.02/152.37  (step @p645 :rule refl :args (@t743))
% 152.02/152.37  (step @p646 :rule bool-double-not-elim :args (@t716))
% 152.02/152.37  (step @p647 :rule nary_cong :premises (@p646 @p645) :args ((or (not @t717) @t743)))
% 152.02/152.37  (assume-push @p1004 @t717)
% 152.02/152.37  (step @p649 :rule skolemize :premises (@p1004))
% 152.02/152.37  (step-pop @p1005 :rule scope :premises (@p649))
% 152.02/152.37  (step @p650 :rule process_scope :premises (@p1005) :args (@t743))
% 152.02/152.37  (step @p652 :rule implies_elim :premises (@p650))
% 152.02/152.37  (step @p653 :rule eq_resolve :premises (@p652 @p647))
% 152.02/152.37  (step @p654 :rule cnf_or_neg :args (@t730 1))
% 152.02/152.37  (step @p655 :rule bool-double-not-elim :args (@t740))
% 152.02/152.37  (step @p656 :rule refl :args (@t742))
% 152.02/152.37  (step @p657 :rule nary_cong :premises (@p656 @p655) :args ((or @t742 (not @t741))))
% 152.02/152.37  (step @p658 :rule cnf_or_neg :args (@t742 0))
% 152.02/152.37  (step @p659 :rule eq_resolve :premises (@p658 @p657))
% 152.02/152.37  (step @p660 :rule reordering :premises (@p659) :args ((or @t740 @t742)))
% 152.02/152.37  (step @p661 :rule bool-double-not-elim :args (@t738))
% 152.02/152.37  (step @p662 :rule nary_cong :premises (@p656 @p661) :args ((or @t742 (not @t739))))
% 152.02/152.37  (step @p663 :rule cnf_or_neg :args (@t742 1))
% 152.02/152.37  (step @p664 :rule eq_resolve :premises (@p663 @p662))
% 152.02/152.37  (step @p665 :rule reordering :premises (@p664) :args ((or @t738 @t742)))
% 152.02/152.37  (step @p666 :rule cnf_and_pos :args (@t744 0))
% 152.02/152.37  (step @p667 :rule reordering :premises (@p666) :args ((or @t741 (not @t744))))
% 152.02/152.37  (step @p668 :rule cnf_and_pos :args (@t745 0))
% 152.02/152.37  (step @p669 :rule reordering :premises (@p668) :args ((or @t739 (not @t745))))
% 152.02/152.37  ; trust TRUST PREPROCESS_HO_ELIM
% 152.02/152.37  (step @p670 :rule trust :premises () :args ((= (forall @t353 (or (and (not @t754) @t751) (and (not @t753) @t749) @t752 @t746)) (forall @t353 (or (and (not (_ @t624 @t747 @t349)) @t751) (and (not (_ @t624 (_ @t622 @t621 @t349) @t270)) @t749) (_ @t624 @t747 @t270) @t746)))))
% 152.02/152.37  (step @p671 :rule refl :args (@t746))
% 152.02/152.37  (step @p672 :rule refl :args (@t752))
% 152.02/152.37  (step @p673 :rule refl :args (@t457))
% 152.02/152.37  (step @p674 :rule cong :premises (@p673 @p672) :args ((= @t457 @t752)))
% 152.02/152.37  (step @p675 :rule symm :premises (@p674))
% 152.02/152.37  (step @p676 :rule eq_resolve :premises (@p673 @p675))
% 152.02/152.37  (step @p677 :rule refl :args (@t749))
% 152.02/152.37  (step @p678 :rule refl :args (@t753))
% 152.02/152.37  (step @p679 :rule refl :args (@t433))
% 152.02/152.37  (step @p680 :rule cong :premises (@p679 @p678) :args ((= @t433 @t753)))
% 152.02/152.37  (step @p681 :rule symm :premises (@p680))
% 152.02/152.37  (step @p682 :rule eq_resolve :premises (@p679 @p681))
% 152.02/152.37  (step @p683 :rule cong :premises (@p682) :args (@t755))
% 152.02/152.37  (step @p684 :rule nary_cong :premises (@p683 @p677) :args (@t756))
% 152.02/152.37  (step @p685 :rule refl :args (@t751))
% 152.02/152.37  (step @p686 :rule refl :args (@t754))
% 152.02/152.37  (step @p687 :rule refl :args (@t426))
% 152.02/152.37  (step @p688 :rule cong :premises (@p687 @p686) :args ((= @t426 @t754)))
% 152.02/152.37  (step @p689 :rule symm :premises (@p688))
% 152.02/152.37  (step @p690 :rule eq_resolve :premises (@p687 @p689))
% 152.02/152.37  (step @p691 :rule cong :premises (@p690) :args (@t757))
% 152.02/152.37  (step @p692 :rule nary_cong :premises (@p691 @p685) :args (@t758))
% 152.02/152.37  (step @p693 :rule nary_cong :premises (@p692 @p684 @p676 @p671) :args (@t759))
% 152.02/152.37  (step @p694 :rule cong :premises (@p693) :args ((forall @t353 @t759)))
% 152.02/152.37  (step @p695 :rule aci_norm :args ((= (or @t758 @t760) @t759)))
% 152.02/152.37  (step @p696 :rule aci_norm :args ((= (or @t756 @t761) @t760)))
% 152.02/152.37  (step @p697 :rule refl :args (@t761))
% 152.02/152.37  (step @p698 :rule bool-or-de-morgan :args (@t433 @t748 false))
% 152.02/152.37  (step @p699 :rule nary_cong :premises (@p698 @p697) :args ((or (not @t762) @t761)))
% 152.02/152.37  (step @p700 :rule trans :premises (@p699 @p696))
% 152.02/152.37  (step @p701 :rule bool-impl-elim :args (@t762 @t761))
% 152.02/152.37  (step @p702 :rule trans :premises (@p701 @p700))
% 152.02/152.37  (step @p703 :rule bool-or-de-morgan :args (@t426 @t750 false))
% 152.02/152.37  (step @p704 :rule nary_cong :premises (@p703 @p702) :args ((or (not @t764) @t763)))
% 152.02/152.37  (step @p705 :rule trans :premises (@p704 @p695))
% 152.02/152.37  (step @p706 :rule bool-impl-elim :args (@t764 @t763))
% 152.02/152.37  (step @p707 :rule trans :premises (@p706 @p705))
% 152.02/152.37  (step @p708 :rule cong :premises (@p707) :args ((forall @t353 (=> @t764 @t763))))
% 152.02/152.37  (step @p709 :rule trans :premises (@p708 @p694))
% 152.02/152.37  (step @p710 :rule beta-reduce :args ((= (_ @t765 @t270) @t761)))
% 152.02/152.37  (step @p711 :rule refl :args (@t270))
% 152.02/152.37  (step @p712 :rule beta-reduce :args ((= @t766 @t765)))
% 152.02/152.37  (step @p713 :rule ho_cong :premises (@p712 @p711))
% 152.02/152.37  (step @p714 :rule trans :premises (@p713 @p710))
% 152.02/152.37  (step @p715 :rule eq-symm :args (@t349 @t270))
% 152.02/152.37  (step @p716 :rule refl :args (@t433))
% 152.02/152.37  (step @p717 :rule nary_cong :premises (@p716 @p715) :args (@t767))
% 152.02/152.37  (step @p718 :rule beta-reduce :args ((= (_ @t768 @t270) @t767)))
% 152.02/152.37  (step @p719 :rule trans :premises (@p718 @p717))
% 152.02/152.37  (step @p720 :rule beta-reduce :args ((= @t769 @t768)))
% 152.02/152.37  (step @p721 :rule ho_cong :premises (@p720 @p711))
% 152.02/152.37  (step @p722 :rule trans :premises (@p721 @p719))
% 152.02/152.37  (step @p723 :rule cong :premises (@p722 @p714) :args (@t770))
% 152.02/152.37  (step @p724 :rule beta-reduce :args ((= (_ @t765 @t349) @t764)))
% 152.02/152.37  (step @p725 :rule refl :args (@t349))
% 152.02/152.37  (step @p726 :rule ho_cong :premises (@p712 @p725))
% 152.02/152.37  (step @p727 :rule trans :premises (@p726 @p724))
% 152.02/152.37  (step @p728 :rule cong :premises (@p727 @p723) :args (@t771))
% 152.02/152.37  (step @p729 :rule cong :premises (@p728) :args ((forall @t353 @t771)))
% 152.02/152.37  (step @p730 :rule trans :premises (@p729 @p709))
% 152.02/152.37  (step @p731 :rule refl :args (@t268))
% 152.02/152.37  (step @p732 :rule ho_cong :premises (@p364 @p731))
% 152.02/152.37  (step @p733 :rule ho_cong :premises (@p732 @p711))
% 152.02/152.37  (step @p734 :rule ho_cong :premises (@p364 @p725))
% 152.02/152.37  (step @p735 :rule ho_cong :premises (@p734 @p711))
% 152.02/152.37  (step @p736 :rule cong :premises (@p735 @p733) :args (@t350))
% 152.02/152.37  (step @p737 :rule ho_cong :premises (@p732 @p725))
% 152.02/152.37  (step @p738 :rule cong :premises (@p737 @p736) :args (@t352))
% 152.02/152.37  (step @p739 :rule cong :premises (@p738) :args (@t354))
% 152.02/152.37  (step @p740 :rule trans :premises (@p739 @p730))
% 152.02/152.37  (step @p741 :rule trans :premises (@p740 @p670))
% 152.02/152.37  (step @p742 :rule eq_resolve :premises (@p138 @p741))
% 152.02/152.37  (step @p743 :rule instantiate :premises (@p742) :args ((@list tptp.xa @t737 @t633)))
% 152.02/152.37  (step @p744 :rule cnf_or_pos :args (@t773))
% 152.02/152.37  (step @p745 :rule reordering :premises (@p744) :args ((or @t745 @t744 @t772 @t729 (not @t773))))
% 152.02/152.37  (assume-push @p1006 @t634)
% 152.02/152.37  (assume-push @p1007 @t772)
% 152.02/152.37  (assume-push @p1008 @t772)
% 152.02/152.37  (assume-push @p1009 @t634)
% 152.02/152.37  (step @p750 :rule true_intro :premises (@p1007))
% 152.02/152.37  (step @p751 :rule refl :args (@t682))
% 152.02/152.37  (step @p752 :rule cong :premises (@p751 @p418) :args (@t774))
% 152.02/152.37  (step @p753 :rule trans :premises (@p752 @p750))
% 152.02/152.37  (step @p754 :rule true_elim :premises (@p753))
% 152.02/152.37  (step-pop @p1010 :rule scope :premises (@p754))
% 152.02/152.37  (step-pop @p1011 :rule scope :premises (@p1010))
% 152.02/152.37  (step @p755 :rule process_scope :premises (@p1011) :args (@t774))
% 152.02/152.37  (step @p758 :rule and_intro :premises (@p1007 @p418))
% 152.02/152.37  (step @p759 :rule modus_ponens :premises (@p758 @p755))
% 152.02/152.37  (step-pop @p1012 :rule scope :premises (@p759))
% 152.02/152.37  (step-pop @p1013 :rule scope :premises (@p1012))
% 152.02/152.37  (step @p760 :rule process_scope :premises (@p1013) :args (@t774))
% 152.02/152.37  (step @p763 :rule implies_elim :premises (@p760))
% 152.02/152.37  (step @p764 :rule cnf_and_neg :args (@t775))
% 152.02/152.37  (step @p765 :rule resolution :premises (@p764 @p763) :args (true @t775))
% 152.02/152.37  (step @p766 :rule reordering :premises (@p765) :args ((or @t777 @t774 @t776)))
% 152.02/152.37  (step @p767 :rule cnf_and_pos :args (@t781 0))
% 152.02/152.37  (step @p768 :rule reordering :premises (@p767) :args ((or @t780 (not @t781))))
% 152.02/152.37  ; trust TRUST PREPROCESS_HO_ELIM
% 152.02/152.37  (step @p769 :rule trust :premises () :args ((= @t614 (not @t785))))
% 152.02/152.37  (step @p770 :rule eq_resolve :premises (@p363 @p769))
% 152.02/152.37  ; trust TRUST PREPROCESS_HO_ELIM
% 152.02/152.37  (step @p771 :rule trust :premises () :args ((= (or (= @t605 @t611) @t612) (or @t787 @t785))))
% 152.02/152.37  (step @p772 :rule refl :args (@t612))
% 152.02/152.37  (step @p773 :rule refl :args (@t611))
% 152.02/152.37  (step @p774 :rule symm :premises (@p345))
% 152.02/152.37  (step @p775 :rule cong :premises (@p774 @p773) :args (@t788))
% 152.02/152.37  (step @p776 :rule nary_cong :premises (@p775 @p772) :args ((or @t788 @t612)))
% 152.02/152.37  (step @p777 :rule eq-symm :args (@t611 tptp.h2))
% 152.02/152.37  (step @p778 :rule nary_cong :premises (@p777 @p772) :args (@t613))
% 152.02/152.37  (step @p779 :rule trans :premises (@p778 @p776 @p771))
% 152.02/152.37  (step @p780 :rule eq_resolve :premises (@p362 @p779))
% 152.02/152.37  (step @p781 :rule reordering :premises (@p780) :args ((or @t785 @t787)))
% 152.02/152.37  (step @p782 :rule chain_m_resolution :premises (@p781 @p770) :args (@t787 @t789 (@list @t785)))
% 152.02/152.37  (step @p783 :rule refl :args (@t791))
% 152.02/152.37  (step @p784 :rule eq-symm :args (@t792 @t793))
% 152.02/152.37  (step @p785 :rule cong :premises (@p784) :args (@t794))
% 152.02/152.37  (step @p786 :rule refl :args (@t796))
% 152.02/152.37  (step @p787 :rule refl :args (@t799))
% 152.02/152.37  (step @p788 :rule nary_cong :premises (@p787 @p786 @p785 @p783) :args (@t800))
% 152.02/152.37  (step @p789 :rule cong :premises (@p788) :args (@t802))
% 152.02/152.37  ; trust TRUST PREPROCESS_HO_ELIM
% 152.02/152.37  (step @p790 :rule trust :premises () :args ((= (forall @t801 (or @t807 @t805 @t804 @t791)) @t802)))
% 152.02/152.37  (step @p791 :rule eq-symm :args (@t790 @t595))
% 152.02/152.37  (step @p792 :rule refl :args (@t804))
% 152.02/152.37  (step @p793 :rule refl :args (@t805))
% 152.02/152.37  (step @p794 :rule refl :args (@t807))
% 152.02/152.37  (step @p795 :rule nary_cong :premises (@p794 @p793 @p792 @p791) :args (@t809))
% 152.02/152.37  (step @p796 :rule aci_norm :args ((= @t811 @t809)))
% 152.02/152.37  (step @p797 :rule trans :premises (@p796 @p795))
% 152.02/152.37  (step @p798 :rule cong :premises (@p797) :args (@t812))
% 152.02/152.37  (step @p799 :rule quant-merge-prenex :args ((= (forall @t603 @t814) @t812)))
% 152.02/152.37  (step @p800 :rule alpha_equiv :args (@t815 (@list @t790) (@list @t341)))
% 152.02/152.37  (step @p801 :rule refl :args (@t807))
% 152.02/152.37  (step @p802 :rule nary_cong :premises (@p801 @p800) :args (@t816))
% 152.02/152.37  (step @p803 :rule quant-miniscope-or :args ((= @t814 @t816)))
% 152.02/152.37  (step @p804 :rule trans :premises (@p803 @p802))
% 152.02/152.37  (step @p805 :rule symm :premises (@p804))
% 152.02/152.37  (step @p806 :rule cong :premises (@p805) :args ((forall @t603 (or @t807 @t822))))
% 152.02/152.37  (step @p807 :rule trans :premises (@p806 @p799))
% 152.02/152.37  (step @p808 :rule trans :premises (@p807 @p798))
% 152.02/152.37  (step @p809 :rule refl :args (@t822))
% 152.02/152.37  (step @p810 :rule refl :args (@t798))
% 152.02/152.37  (step @p811 :rule refl :args (@t806))
% 152.02/152.37  (step @p812 :rule refl :args (@t824))
% 152.02/152.37  (step @p813 :rule cong :premises (@p812 @p811) :args ((= @t824 @t806)))
% 152.02/152.37  (step @p814 :rule symm :premises (@p813))
% 152.02/152.37  (step @p815 :rule eq_resolve :premises (@p812 @p814))
% 152.02/152.37  (step @p816 :rule cong :premises (@p815) :args (@t825))
% 152.02/152.37  (step @p817 :rule nary_cong :premises (@p816 @p810) :args (@t826))
% 152.02/152.37  (step @p818 :rule nary_cong :premises (@p817 @p809) :args (@t827))
% 152.02/152.37  (step @p819 :rule cong :premises (@p818) :args ((forall @t603 @t827)))
% 152.02/152.37  (step @p820 :rule trans :premises (@p819 @p808))
% 152.02/152.37  (step @p821 :rule bool-or-de-morgan :args (@t824 @t797 false))
% 152.02/152.37  (step @p822 :rule nary_cong :premises (@p821 @p809) :args ((or (not @t828) @t822)))
% 152.02/152.37  (step @p823 :rule bool-impl-elim :args (@t828 @t822))
% 152.02/152.37  (step @p824 :rule trans :premises (@p823 @p822))
% 152.02/152.37  (step @p825 :rule cong :premises (@p824) :args ((forall @t603 (=> @t828 @t822))))
% 152.02/152.37  (step @p826 :rule trans :premises (@p825 @p820))
% 152.02/152.37  (step @p827 :rule refl :args (@t817))
% 152.02/152.37  (step @p828 :rule refl :args (@t818))
% 152.02/152.37  (step @p829 :rule refl :args (@t596))
% 152.02/152.37  (step @p830 :rule cong :premises (@p829 @p828) :args ((= @t596 @t818)))
% 152.02/152.37  (step @p831 :rule symm :premises (@p830))
% 152.02/152.37  (step @p832 :rule eq_resolve :premises (@p829 @p831))
% 152.02/152.37  (step @p833 :rule refl :args (@t803))
% 152.02/152.37  (step @p834 :rule refl :args (@t597))
% 152.02/152.37  (step @p835 :rule cong :premises (@p834 @p833) :args ((= @t597 @t803)))
% 152.02/152.37  (step @p836 :rule symm :premises (@p835))
% 152.02/152.37  (step @p837 :rule eq_resolve :premises (@p834 @p836))
% 152.02/152.37  (step @p838 :rule cong :premises (@p837 @p832) :args (@t598))
% 152.02/152.37  (step @p839 :rule cong :premises (@p838) :args (@t829))
% 152.02/152.37  (step @p840 :rule refl :args (@t820))
% 152.02/152.37  (step @p841 :rule refl :args (@t821))
% 152.02/152.37  (step @p842 :rule refl :args (@t831))
% 152.02/152.37  (step @p843 :rule cong :premises (@p842 @p841) :args ((= @t831 @t821)))
% 152.02/152.37  (step @p844 :rule symm :premises (@p843))
% 152.02/152.37  (step @p845 :rule eq_resolve :premises (@p842 @p844))
% 152.02/152.37  (step @p846 :rule cong :premises (@p845) :args (@t832))
% 152.02/152.37  (step @p847 :rule nary_cong :premises (@p846 @p840) :args (@t833))
% 152.02/152.37  (step @p848 :rule nary_cong :premises (@p847 @p839 @p827) :args (@t834))
% 152.02/152.37  (step @p849 :rule cong :premises (@p848) :args ((forall @t343 @t834)))
% 152.02/152.37  (step @p850 :rule aci_norm :args ((= (or @t833 (or @t829 @t817)) @t834)))
% 152.02/152.37  (step @p851 :rule bool-impl-elim :args (@t598 @t817))
% 152.02/152.37  (step @p852 :rule bool-or-de-morgan :args (@t831 @t819 false))
% 152.02/152.37  (step @p853 :rule nary_cong :premises (@p852 @p851) :args ((or (not @t836) @t835)))
% 152.02/152.37  (step @p854 :rule trans :premises (@p853 @p850))
% 152.02/152.37  (step @p855 :rule bool-impl-elim :args (@t836 @t835))
% 152.02/152.37  (step @p856 :rule trans :premises (@p855 @p854))
% 152.02/152.37  (step @p857 :rule cong :premises (@p856) :args ((forall @t343 (=> @t836 @t835))))
% 152.02/152.37  (step @p858 :rule trans :premises (@p857 @p849))
% 152.02/152.37  (step @p859 :rule eq-symm :args (@t595 @t341))
% 152.02/152.37  (step @p860 :rule refl :args (@t598))
% 152.02/152.37  (step @p861 :rule cong :premises (@p860 @p859) :args (@t599))
% 152.02/152.37  (step @p862 :rule eq-symm :args (@t341 tptp.m2))
% 152.02/152.37  (step @p863 :rule refl :args (@t831))
% 152.02/152.37  (step @p864 :rule nary_cong :premises (@p863 @p862) :args (@t837))
% 152.02/152.37  (step @p865 :rule beta-reduce :args ((= (_ @t838 tptp.m2) @t837)))
% 152.02/152.37  (step @p866 :rule trans :premises (@p865 @p864))
% 152.02/152.37  (step @p867 :rule refl :args (tptp.m2))
% 152.02/152.37  (step @p868 :rule beta-reduce :args ((= @t839 @t838)))
% 152.02/152.37  (step @p869 :rule ho_cong :premises (@p868 @p867))
% 152.02/152.37  (step @p870 :rule trans :premises (@p869 @p866))
% 152.02/152.37  (step @p871 :rule cong :premises (@p870 @p861) :args (@t840))
% 152.02/152.37  (step @p872 :rule cong :premises (@p871) :args (@t841))
% 152.02/152.37  (step @p873 :rule trans :premises (@p872 @p858))
% 152.02/152.37  (step @p874 :rule beta-reduce :args ((= (_ (lambda @t677 (or @t842 (= @t413 @t595))) tptp.m2) @t828)))
% 152.02/152.37  (step @p875 :rule eq-symm :args (@t595 @t413))
% 152.02/152.37  (step @p876 :rule refl :args (@t842))
% 152.02/152.37  (step @p877 :rule nary_cong :premises (@p876 @p875) :args (@t843))
% 152.02/152.37  (step @p878 :rule cong :premises (@p877) :args (@t844))
% 152.02/152.37  (step @p879 :rule beta-reduce :args ((= @t845 @t844)))
% 152.02/152.37  (step @p880 :rule trans :premises (@p879 @p878))
% 152.02/152.37  (step @p881 :rule ho_cong :premises (@p880 @p867))
% 152.02/152.37  (step @p882 :rule trans :premises (@p881 @p874))
% 152.02/152.37  (step @p883 :rule cong :premises (@p882 @p873) :args (@t846))
% 152.02/152.37  (step @p884 :rule cong :premises (@p883) :args ((forall @t603 @t846)))
% 152.02/152.37  (step @p885 :rule trans :premises (@p884 @p826))
% 152.02/152.37  (step @p886 :rule refl :args (@t599))
% 152.02/152.37  (step @p887 :rule refl :args (@t341))
% 152.02/152.37  (step @p888 :rule ho_cong :premises (@p364 @p887))
% 152.02/152.37  (step @p889 :rule ho_cong :premises (@p888 @p867))
% 152.02/152.37  (step @p890 :rule cong :premises (@p889 @p886) :args (@t600))
% 152.02/152.37  (step @p891 :rule cong :premises (@p890) :args (@t601))
% 152.02/152.37  (step @p892 :rule refl :args (@t595))
% 152.02/152.37  (step @p893 :rule ho_cong :premises (@p364 @p892))
% 152.02/152.37  (step @p894 :rule ho_cong :premises (@p893 @p867))
% 152.02/152.37  (step @p895 :rule cong :premises (@p894 @p891) :args (@t602))
% 152.02/152.37  (step @p896 :rule cong :premises (@p895) :args (@t604))
% 152.02/152.37  (step @p897 :rule trans :premises (@p896 @p885))
% 152.02/152.37  (step @p898 :rule trans :premises (@p897 @p790 @p789))
% 152.02/152.37  (step @p899 :rule eq_resolve :premises (@p343 @p898))
% 152.02/152.37  (step @p900 :rule aci_norm :args ((= (or false @t781 @t847 @t778) @t848)))
% 152.02/152.37  (step @p901 :rule refl :args (@t778))
% 152.02/152.37  (step @p902 :rule eq-symm :args (@t784 @t786))
% 152.02/152.37  (step @p903 :rule cong :premises (@p902) :args (@t849))
% 152.02/152.37  (step @p904 :rule refl :args (@t781))
% 152.02/152.37  (step @p905 :rule absorb :args ((= (and @t850 false) false)))
% 152.02/152.37  (step @p906 :rule eq-refl :args (tptp.m2))
% 152.02/152.37  (step @p907 :rule cong :premises (@p906) :args (@t851))
% 152.02/152.37  (step @p908 :rule trans :premises (@p907 @p422))
% 152.02/152.37  (step @p909 :rule refl :args (@t850))
% 152.02/152.37  (step @p910 :rule nary_cong :premises (@p909 @p908) :args (@t852))
% 152.02/152.37  (step @p911 :rule trans :premises (@p910 @p905))
% 152.02/152.37  (step @p912 :rule nary_cong :premises (@p911 @p904 @p903 @p901) :args (@t853))
% 152.02/152.37  (step @p913 :rule trans :premises (@p912 @p900))
% 152.02/152.37  (step @p914 :rule refl :args (@t854))
% 152.02/152.37  (step @p915 :rule cong :premises (@p914 @p913) :args ((=> @t854 @t853)))
% 152.02/152.37  (assume-push @p1014 @t854)
% 152.02/152.37  (step @p917 :rule instantiate :premises (@p899) :args ((@list tptp.m2 tptp.xa)))
% 152.02/152.37  (step-pop @p1015 :rule scope :premises (@p917))
% 152.02/152.37  (step @p918 :rule process_scope :premises (@p1015) :args (@t853))
% 152.02/152.37  (step @p920 :rule eq_resolve :premises (@p918 @p915))
% 152.02/152.37  (step @p921 :rule implies_elim :premises (@p920))
% 152.02/152.37  (step @p922 :rule chain_m_resolution :premises (@p921 @p899) :args (@t848 @t735 (@list @t854)))
% 152.02/152.37  (step @p923 :rule cnf_or_pos :args (@t848))
% 152.02/152.37  (step @p924 :rule reordering :premises (@p923) :args ((or @t847 @t778 @t781 (not @t848))))
% 152.02/152.37  (step @p925 :rule bool-double-not-elim :args (@t729))
% 152.02/152.37  (step @p926 :rule refl :args (@t779))
% 152.02/152.37  (step @p927 :rule refl :args (@t777))
% 152.02/152.37  (step @p928 :rule nary_cong :premises (@p927 @p926 @p925) :args ((or @t777 @t779 (not @t855))))
% 152.02/152.37  (assume-push @p1016 @t634)
% 152.02/152.37  (assume-push @p1017 @t778)
% 152.02/152.37  (assume-push @p1018 @t855)
% 152.02/152.37  (step @p932 :rule evaluate :args ((= false true)))
% 152.02/152.37  (step @p933 :rule symm :premises (@p1017))
% 152.02/152.37  (step @p934 :rule trans :premises (@p933 @p418))
% 152.02/152.37  (step @p935 :rule true_intro :premises (@p934))
% 152.02/152.37  (step @p936 :rule false_intro :premises (@p1018))
% 152.02/152.37  (step @p937 :rule symm :premises (@p936))
% 152.02/152.37  (step @p938 :rule trans :premises (@p937 @p935))
% 152.02/152.37  (step @p939 false :rule eq_resolve :premises (@p938 @p932))
% 152.02/152.37  (step-pop @p1019 :rule scope :premises (@p939))
% 152.02/152.37  (step-pop @p1020 :rule scope :premises (@p1019))
% 152.02/152.37  (step-pop @p1021 :rule scope :premises (@p1020))
% 152.02/152.37  (step @p940 :rule process_scope :premises (@p1021) :args (false))
% 152.02/152.37  (step @p944 :rule not_and :premises (@p940))
% 152.02/152.37  (step @p945 :rule eq_resolve :premises (@p944 @p928))
% 152.02/152.37  (step @p946 :rule reordering :premises (@p945) :args ((or @t777 @t729 @t779)))
% 152.02/152.37  (step @p947 :rule chain_m_resolution :premises (@p946 @p418 @p924 @p922 @p782 @p768 @p766 @p418 @p745 @p743 @p669 @p667 @p665 @p660 @p654 @p653 @p644 @p642 @p580 @p578 @p516 @p514) :args (@t687 (@list false false false false true false false false false true true false false true true true false true false true false) (@list @t634 @t778 @t848 @t787 @t781 @t774 @t634 @t772 @t773 @t745 @t744 @t738 @t740 @t729 @t742 @t730 @t734 @t716 @t718 @t690 @t686)))
% 152.02/152.37  ; trust TRUST PREPROCESS_HO_ELIM
% 152.02/152.37  (step @p948 :rule trust :premises () :args ((= @t857 (or @t685 @t688))))
% 152.02/152.37  (step @p949 :rule beta-reduce :args ((= (_ @t858 @t610) @t857)))
% 152.02/152.37  (step @p950 :rule refl :args (@t610))
% 152.02/152.37  (step @p951 :rule beta-reduce :args ((= (_ @t615 tptp.xa) @t858)))
% 152.02/152.37  (step @p952 :rule ho_cong :premises (@p951 @p950))
% 152.02/152.37  (step @p953 :rule trans :premises (@p952 @p949))
% 152.02/152.37  (step @p954 :rule refl :args (tptp.xa))
% 152.02/152.37  (step @p955 :rule ho_cong :premises (@p364 @p954))
% 152.02/152.37  (step @p956 :rule ho_cong :premises (@p955 @p950))
% 152.02/152.37  (step @p957 :rule trans :premises (@p956 @p953))
% 152.02/152.37  (step @p958 :rule trans :premises (@p957 @p948))
% 152.02/152.37  (step @p959 :rule eq_resolve :premises (@p361 @p958))
% 152.02/152.37  (step @p960 :rule reordering :premises (@p959) :args ((or @t688 @t685)))
% 152.02/152.37  (step @p961 :rule chain_m_resolution :premises (@p960 @p947) :args (@t688 @t789 (@list @t685)))
% 152.02/152.37  (step @p962 :rule cnf_and_pos :args (@t690 1))
% 152.02/152.37  (step @p963 :rule reordering :premises (@p962) :args ((or @t689 @t691)))
% 152.02/152.37  (step @p964 :rule chain_m_resolution :premises (@p963 @p961) :args (@t691 @t735 (@list @t688)))
% 152.02/152.37  (step @p965 :rule chain_m_resolution :premises (@p644 @p964 @p642) :args (@t736 (@list true false) (@list @t690 @t734)))
% 152.02/152.37  (step @p966 :rule chain_m_resolution :premises (@p654 @p965) :args (@t855 @t789 (@list @t730)))
% 152.02/152.37  (step @p967 :rule chain_m_resolution :premises (@p946 @p418 @p966) :args (@t779 @t859 (@list @t634 @t729)))
% 152.02/152.37  (step @p968 :rule chain_m_resolution :premises (@p924 @p782 @p967 @p922) :args (@t781 (@list false true false) (@list @t787 @t778 @t848)))
% 152.02/152.37  (step @p969 :rule chain_m_resolution :premises (@p768 @p968) :args (@t780 @t735 (@list @t781)))
% 152.02/152.37  (step @p970 :rule chain_m_resolution :premises (@p766 @p418 @p969) :args (@t776 @t859 (@list @t634 @t774)))
% 152.02/152.37  (assume-push @p1022 @t688)
% 152.02/152.37  (assume-push @p1023 @t634)
% 152.02/152.37  (assume-push @p1024 @t860)
% 152.02/152.37  (assume-push @p1025 @t860)
% 152.02/152.37  (assume-push @p1026 @t688)
% 152.02/152.37  (assume-push @p1027 @t634)
% 152.02/152.37  (step @p977 :rule true_intro :premises (@p512))
% 152.02/152.37  (step @p978 :rule symm :premises (@p1022))
% 152.02/152.37  (step @p979 :rule refl :args (@t616))
% 152.02/152.37  (step @p980 :rule cong :premises (@p979 @p978) :args (@t633))
% 152.02/152.37  (step @p981 :rule trans :premises (@p418 @p980))
% 152.02/152.37  (step @p751 :rule refl :args (@t682))
% 152.02/152.37  (step @p982 :rule cong :premises (@p751 @p981) :args (@t774))
% 152.02/152.37  (step @p983 :rule symm :premises (@p418))
% 152.02/152.37  (step @p984 :rule cong :premises (@p751 @p983) :args (@t772))
% 152.02/152.37  (step @p985 :rule trans :premises (@p984 @p982 @p977))
% 152.02/152.37  (step @p986 :rule true_elim :premises (@p985))
% 152.02/152.37  (step-pop @p1028 :rule scope :premises (@p986))
% 152.02/152.37  (step-pop @p1029 :rule scope :premises (@p1028))
% 152.02/152.37  (step-pop @p1030 :rule scope :premises (@p1029))
% 152.02/152.37  (step @p987 :rule process_scope :premises (@p1030) :args (@t772))
% 152.02/152.37  (step @p991 :rule and_intro :premises (@p512 @p1022 @p418))
% 152.02/152.37  (step @p992 :rule modus_ponens :premises (@p991 @p987))
% 152.02/152.37  (step-pop @p1031 :rule scope :premises (@p992))
% 152.02/152.37  (step-pop @p1032 :rule scope :premises (@p1031))
% 152.02/152.37  (step-pop @p1033 :rule scope :premises (@p1032))
% 152.02/152.37  (step @p993 :rule process_scope :premises (@p1033) :args (@t772))
% 152.02/152.37  (step @p997 :rule implies_elim :premises (@p993))
% 152.02/152.37  (step @p998 :rule cnf_and_neg :args (@t861))
% 152.02/152.37  (step @p999 :rule resolution :premises (@p998 @p997) :args (true @t861))
% 152.02/152.37  (step @p1000 :rule reordering :premises (@p999) :args ((or @t689 @t777 @t772 (not @t860))))
% 152.02/152.37  (step @p1001 false :rule chain_m_resolution :premises (@p1000 @p970 @p961 @p512 @p418) :args (false (@list true false false false) (@list @t772 @t688 @t860 @t634)))
% 152.02/152.37  )
% 152.02/152.37  % SZS output end Proof
% 152.02/152.37  % cvc5 exiting
%------------------------------------------------------------------------------