cvc5---1.3.4.THM-Prf.s

%------------------------------------------------------------------------------
% File     : cvc5---1.3.4
% Problem  : ITP199^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 : n026.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Wed Jun  3 08:25:21 AM UTC 2026

% Result   : Theorem 0.48s 0.88s
% Output   : Proof 0.48s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem  : ITP199^1 : TPTP v9.2.1. Released v7.5.0.
% 0.12/0.13  % Command  : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.17/0.35  % Computer : n026.cluster.edu
% 0.17/0.35  % Model    : x86_64 x86_64
% 0.17/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.35  % Memory   : 8042.1875MB
% 0.17/0.35  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.17/0.35  % CPULimit : 300
% 0.17/0.35  % WCLimit  : 300
% 0.17/0.35  % DateTime : Tue Jun  2 04:18:55 EDT 2026
% 0.17/0.35  % CPUTime  : 
% 0.43/0.61  %----Proving TH0
% 0.48/0.88  --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 90s...
% 0.48/0.88  % SZS status Theorem
% 0.48/0.88  % SZS output start Proof
% 0.48/0.88  (
% 0.48/0.88  (declare-sort tptp.nat 0)
% 0.48/0.88  (declare-sort tptp.option_variable_real 0)
% 0.48/0.88  (declare-sort tptp.variable 0)
% 0.48/0.88  (declare-sort tptp.real 0)
% 0.48/0.88  (declare-sort tptp.option_variable 0)
% 0.48/0.88  (declare-sort tptp.set_variable_real 0)
% 0.48/0.88  (declare-sort tptp.set_variable 0)
% 0.48/0.88  (declare-sort tptp.option_trm 0)
% 0.48/0.88  (declare-sort tptp.set_trm 0)
% 0.48/0.88  (declare-sort tptp.trm 0)
% 0.48/0.88  (declare-sort tptp.set_op12188086e_real 0)
% 0.48/0.88  (declare-sort tptp.set_option_variable 0)
% 0.48/0.88  (declare-sort tptp.set_option_trm 0)
% 0.48/0.88  (declare-sort tptp.char 0)
% 0.48/0.88  (declare-sort tptp.denotational_interp 0)
% 0.48/0.88  (declare-sort tptp.set_real 0)
% 0.48/0.88  (declare-sort tptp.produc1418842292n_game 0)
% 0.48/0.88  (declare-sort tptp.set_nat 0)
% 0.48/0.88  (declare-const tptp.member_variable (-> tptp.variable tptp.set_variable Bool))
% 0.48/0.88  (declare-const tptp.bot_bot_set_variable tptp.set_variable)
% 0.48/0.88  (declare-const tptp.bot_bo721182586e_real tptp.set_variable_real)
% 0.48/0.88  (declare-const tptp.member_variable_real (-> (-> tptp.variable tptp.real) tptp.set_variable_real Bool))
% 0.48/0.88  (declare-const tptp.the_elem_variable (-> tptp.set_variable tptp.variable))
% 0.48/0.88  (declare-const tptp.insert_variable (-> tptp.variable tptp.set_variable tptp.set_variable))
% 0.48/0.88  (declare-const tptp.the_el1059226619e_real (-> tptp.set_variable_real tptp.variable tptp.real))
% 0.48/0.88  (declare-const tptp.insert_variable_real (-> (-> tptp.variable tptp.real) tptp.set_variable_real tptp.set_variable_real))
% 0.48/0.88  (declare-const tptp.if_real (-> Bool tptp.real tptp.real tptp.real))
% 0.48/0.88  (declare-const tptp.ord_less_eq_nat (-> tptp.nat tptp.nat Bool))
% 0.48/0.88  (declare-const tptp.inf_in1556002680e_real (-> tptp.set_variable_real tptp.set_variable_real tptp.set_variable_real))
% 0.48/0.88  (declare-const tptp.ord_le1113654598e_real (-> tptp.set_variable_real tptp.set_variable_real Bool))
% 0.48/0.88  (declare-const tptp.ord_le282106107riable (-> tptp.set_variable tptp.set_variable Bool))
% 0.48/0.88  (declare-const tptp.inf_inf_set_variable (-> tptp.set_variable tptp.set_variable tptp.set_variable))
% 0.48/0.88  (declare-const tptp.static_FVT (-> tptp.trm tptp.set_variable))
% 0.48/0.88  (declare-const tptp.times (-> tptp.trm tptp.trm tptp.trm))
% 0.48/0.88  (declare-const tptp.uSubst918876924Timeso (-> tptp.option_trm tptp.option_trm tptp.option_trm))
% 0.48/0.88  (declare-const tptp.uminus1851247844riable (-> tptp.set_variable tptp.set_variable))
% 0.48/0.88  (declare-const tptp.the_variable_real (-> tptp.option_variable_real tptp.variable tptp.real))
% 0.48/0.88  (declare-const tptp.the_variable (-> tptp.option_variable tptp.variable))
% 0.48/0.88  (declare-const tptp.set_op697949218e_real (-> tptp.option_variable_real tptp.set_variable_real))
% 0.48/0.88  (declare-const tptp.sigma tptp.produc1418842292n_game)
% 0.48/0.88  (declare-const tptp.zero_zero_set_real tptp.set_real)
% 0.48/0.88  (declare-const tptp.collect_variable (-> (-> tptp.variable Bool) tptp.set_variable))
% 0.48/0.88  (declare-const tptp.zero_zero_nat tptp.nat)
% 0.48/0.88  (declare-const tptp.bot_bot_set_nat tptp.set_nat)
% 0.48/0.88  (declare-const tptp.insert_real (-> tptp.real tptp.set_real tptp.set_real))
% 0.48/0.88  (declare-const tptp.none_trm tptp.option_trm)
% 0.48/0.88  (declare-const tptp.bot_bot_set_real tptp.set_real)
% 0.48/0.88  (declare-const tptp.i tptp.denotational_interp)
% 0.48/0.88  (declare-const tptp.denota1778088425es_ODE (-> tptp.denotational_interp (-> tptp.real tptp.variable tptp.real) tptp.char tptp.trm Bool))
% 0.48/0.88  (declare-const tptp.insert_nat (-> tptp.nat tptp.set_nat tptp.set_nat))
% 0.48/0.88  (declare-const tptp.x tptp.char)
% 0.48/0.88  (declare-const tptp.uminus430703407e_real (-> tptp.set_variable_real tptp.set_variable_real))
% 0.48/0.88  (declare-const tptp.rr (-> tptp.trm tptp.denotational_interp tptp.trm tptp.denotational_interp tptp.char (-> tptp.real tptp.variable tptp.real) tptp.variable tptp.real))
% 0.48/0.88  (declare-const tptp.zero_zero_set_nat tptp.set_nat)
% 0.48/0.88  (declare-const tptp.denota1863255036rm_sem (-> tptp.denotational_interp tptp.trm (-> tptp.variable tptp.real) tptp.real))
% 0.48/0.88  (declare-const tptp.omega (-> tptp.variable tptp.real))
% 0.48/0.88  (declare-const tptp.collec633296133e_real (-> (-> (-> tptp.variable tptp.real) Bool) tptp.set_variable_real))
% 0.48/0.88  (declare-const tptp.u tptp.set_variable)
% 0.48/0.88  (declare-const tptp.zero_zero_real tptp.real)
% 0.48/0.88  (declare-const tptp.dVar (-> tptp.char tptp.variable))
% 0.48/0.88  (declare-const tptp.uSubst1599435252djoint (-> tptp.produc1418842292n_game tptp.denotational_interp (-> tptp.variable tptp.real) tptp.denotational_interp))
% 0.48/0.88  (declare-const tptp.sup_sup_set_variable (-> tptp.set_variable tptp.set_variable tptp.set_variable))
% 0.48/0.88  (declare-const tptp.insert_option_trm (-> tptp.option_trm tptp.set_option_trm tptp.set_option_trm))
% 0.48/0.88  (declare-const tptp.f (-> tptp.real tptp.variable tptp.real))
% 0.48/0.88  (declare-const tptp.rVar (-> tptp.char tptp.variable))
% 0.48/0.88  (declare-const tptp.these_trm (-> tptp.set_option_trm tptp.set_trm))
% 0.48/0.88  (declare-const tptp.sup_su1685293586e_real (-> tptp.set_variable_real tptp.set_variable_real tptp.set_variable_real))
% 0.48/0.88  (declare-const tptp.uminus_uminus_real (-> tptp.real tptp.real))
% 0.48/0.88  (declare-const tptp.theta tptp.trm)
% 0.48/0.88  (declare-const tptp.uSubst516392818stappt (-> tptp.produc1418842292n_game tptp.set_variable tptp.trm tptp.option_trm))
% 0.48/0.88  (declare-const tptp.the_trm (-> tptp.option_trm tptp.trm))
% 0.48/0.88  (declare-const tptp.size_variable (-> tptp.variable tptp.nat))
% 0.48/0.88  (declare-const tptp.size_size_variable (-> tptp.variable tptp.nat))
% 0.48/0.88  (declare-const tptp.insert1340772453riable (-> tptp.option_variable tptp.set_option_variable tptp.set_option_variable))
% 0.48/0.88  (declare-const tptp.bot_bo1411475018e_real tptp.set_op12188086e_real)
% 0.48/0.88  (declare-const tptp.bot_bo946428664on_trm tptp.set_option_trm)
% 0.48/0.88  (declare-const tptp.bot_bot_set_trm tptp.set_trm)
% 0.48/0.88  (declare-const tptp.member_option_trm (-> tptp.option_trm tptp.set_option_trm Bool))
% 0.48/0.88  (declare-const tptp.bot_bo266290559riable tptp.set_option_variable)
% 0.48/0.88  (declare-const tptp.statediff (-> (-> tptp.variable tptp.real) (-> tptp.variable tptp.real) tptp.set_variable))
% 0.48/0.88  (declare-const tptp.member523846807e_real (-> tptp.option_variable_real tptp.set_op12188086e_real Bool))
% 0.48/0.88  (declare-const tptp.none_variable tptp.option_variable)
% 0.48/0.88  (declare-const tptp.these_variable (-> tptp.set_option_variable tptp.set_variable))
% 0.48/0.88  (declare-const tptp.none_variable_real tptp.option_variable_real)
% 0.48/0.88  (declare-const tptp.insert526581936e_real (-> tptp.option_variable_real tptp.set_op12188086e_real tptp.set_op12188086e_real))
% 0.48/0.88  (declare-const tptp.these_variable_real (-> tptp.set_op12188086e_real tptp.set_variable_real))
% 0.48/0.88  (declare-const tptp.some_variable (-> tptp.variable tptp.option_variable))
% 0.48/0.88  (declare-const tptp.some_variable_real (-> (-> tptp.variable tptp.real) tptp.option_variable_real))
% 0.48/0.88  (declare-const tptp.insert_trm (-> tptp.trm tptp.set_trm tptp.set_trm))
% 0.48/0.88  (declare-const tptp.some_trm (-> tptp.trm tptp.option_trm))
% 0.48/0.88  (declare-const tptp.static_selectlike (-> tptp.set_variable_real (-> tptp.variable tptp.real) tptp.set_variable tptp.set_variable_real))
% 0.48/0.88  (declare-const tptp.member814448204riable (-> tptp.option_variable tptp.set_option_variable Bool))
% 0.48/0.88  (declare-const tptp.member_trm (-> tptp.trm tptp.set_trm Bool))
% 0.48/0.88  (declare-const tptp.set_option_trm2 (-> tptp.option_trm tptp.set_trm))
% 0.48/0.88  (declare-const tptp.set_option_variable2 (-> tptp.option_variable tptp.set_variable))
% 0.48/0.88  (define tptp.denota1419872369iation () (let ((_let_1 (@var "I" tptp.variable))) (let ((_let_2 (@var "Nu4" (-> tptp.variable tptp.real)))) (let ((_let_3 (@var "Nu3" (-> tptp.variable tptp.real)))) (let ((_let_4 (@var "U2" tptp.set_variable))) (lambda (@list _let_3 _let_2 _let_4) (forall (@list _let_1) (=> (not (_ (_ tptp.member_variable _let_1) _let_4)) (= (_ _let_3 _let_1) (_ _let_2 _let_1))))))))))
% 0.48/0.88  (define tptp.bot_bot_variable_o () (let ((_let_1 (@var "X2" tptp.variable))) (lambda (@list _let_1) (_ (_ tptp.member_variable _let_1) tptp.bot_bot_set_variable))))
% 0.48/0.88  (define tptp.bot_bo1661475211real_o () (let ((_let_1 (@var "X2" (-> tptp.variable tptp.real)))) (lambda (@list _let_1) (_ (_ tptp.member_variable_real _let_1) tptp.bot_bo721182586e_real))))
% 0.48/0.88  (define tptp.is_sin155454833riable () (let ((_let_1 (@var "A4" tptp.set_variable))) (lambda (@list _let_1) (= _let_1 (_ (_ tptp.insert_variable (_ tptp.the_elem_variable _let_1)) tptp.bot_bot_set_variable)))))
% 0.48/0.88  (define tptp.is_sin524757308e_real () (let ((_let_1 (@var "A4" tptp.set_variable_real))) (lambda (@list _let_1) (= _let_1 (_ (_ tptp.insert_variable_real (_ tptp.the_el1059226619e_real _let_1)) tptp.bot_bo721182586e_real)))))
% 0.48/0.88  (define tptp.is_empty_variable () (let ((_let_1 (@var "A4" tptp.set_variable))) (lambda (@list _let_1) (= _let_1 tptp.bot_bot_set_variable))))
% 0.48/0.88  (define tptp.is_emp227886046e_real () (let ((_let_1 (@var "A4" tptp.set_variable_real))) (lambda (@list _let_1) (= _let_1 tptp.bot_bo721182586e_real))))
% 0.48/0.88  (define tptp.denotational_repv () (let ((_let_1 (@var "Y3" tptp.variable))) (let ((_let_2 (@var "Omega2" (-> tptp.variable tptp.real)))) (let ((_let_3 (@var "R" tptp.real))) (let ((_let_4 (@var "X2" tptp.variable))) (lambda (@list _let_2 _let_4 _let_3 _let_1) (_ (_ (_ tptp.if_real (= _let_4 _let_1)) _let_3) (_ _let_2 _let_1))))))))
% 0.48/0.88  (define tptp.denotational_Vagree () (let ((_let_1 (@var "I" tptp.variable))) (let ((_let_2 (@var "Nu4" (-> tptp.variable tptp.real)))) (let ((_let_3 (@var "Nu3" (-> tptp.variable tptp.real)))) (let ((_let_4 (@var "V3" tptp.set_variable))) (lambda (@list _let_3 _let_2 _let_4) (forall (@list _let_1) (=> (_ (_ tptp.member_variable _let_1) _let_4) (= (_ _let_3 _let_1) (_ _let_2 _let_1))))))))))
% 0.48/0.88  (define tptp.stateinterpol () (let ((_let_1 (@var "X2" tptp.variable))) (let ((_let_2 (@var "Omega2" (-> tptp.variable tptp.real)))) (let ((_let_3 (@var "Nu3" (-> tptp.variable tptp.real)))) (let ((_let_4 (@var "S2" tptp.set_variable))) (lambda (@list _let_3 _let_2 _let_4 _let_1) (_ (_ (_ tptp.if_real (_ (_ tptp.member_variable _let_1) _let_4)) (_ _let_3 _let_1)) (_ _let_2 _let_1))))))))
% 0.48/0.88  (define @t1 () (_ tptp.dVar tptp.x))
% 0.48/0.88  (define @t2 () (_ tptp.insert_variable @t1))
% 0.48/0.88  (define @t3 () (_ @t2 tptp.bot_bot_set_variable))
% 0.48/0.88  (define @t4 () (_ tptp.rVar tptp.x))
% 0.48/0.88  (define @t5 () (_ tptp.insert_variable @t4))
% 0.48/0.88  (define @t6 () (_ @t5 @t3))
% 0.48/0.88  (define @t7 () (_ tptp.sup_sup_set_variable tptp.u))
% 0.48/0.88  (define @t8 () (_ @t7 @t6))
% 0.48/0.88  (define @t9 () (_ tptp.f tptp.zero_zero_real))
% 0.48/0.88  (define @t10 () (_ (_ tptp.denota1419872369iation @t9) tptp.omega))
% 0.48/0.88  (define @t11 () (@var "Nu2" (-> tptp.variable tptp.real)))
% 0.48/0.88  (define @t12 () (@var "Nu" (-> tptp.variable tptp.real)))
% 0.48/0.88  (define @t13 () (_ tptp.denota1419872369iation @t12))
% 0.48/0.88  (define @t14 () (_ @t13 @t11))
% 0.48/0.88  (define @t15 () (@list @t12 @t11))
% 0.48/0.88  (define @t16 () (@var "C" tptp.set_variable))
% 0.48/0.88  (define @t17 () (@var "B" tptp.set_variable))
% 0.48/0.88  (define @t18 () (_ tptp.sup_sup_set_variable @t17))
% 0.48/0.88  (define @t19 () (_ @t18 @t16))
% 0.48/0.88  (define @t20 () (@var "A" tptp.variable))
% 0.48/0.88  (define @t21 () (_ tptp.insert_variable @t20))
% 0.48/0.88  (define @t22 () (_ @t21 @t17))
% 0.48/0.88  (define @t23 () (@var "C" tptp.set_variable_real))
% 0.48/0.88  (define @t24 () (@var "B" tptp.set_variable_real))
% 0.48/0.88  (define @t25 () (_ tptp.sup_su1685293586e_real @t24))
% 0.48/0.88  (define @t26 () (_ @t25 @t23))
% 0.48/0.88  (define @t27 () (@var "A" (-> tptp.variable tptp.real)))
% 0.48/0.88  (define @t28 () (_ tptp.insert_variable_real @t27))
% 0.48/0.88  (define @t29 () (_ @t28 @t24))
% 0.48/0.88  (define @t30 () (@var "A2" tptp.set_variable))
% 0.48/0.88  (define @t31 () (_ tptp.sup_sup_set_variable @t30))
% 0.48/0.88  (define @t32 () (_ @t31 @t17))
% 0.48/0.88  (define @t33 () (@var "A2" tptp.set_variable_real))
% 0.48/0.88  (define @t34 () (_ tptp.sup_su1685293586e_real @t33))
% 0.48/0.88  (define @t35 () (_ @t34 @t24))
% 0.48/0.88  (define @t36 () (= @t24 tptp.bot_bo721182586e_real))
% 0.48/0.88  (define @t37 () (= @t33 tptp.bot_bo721182586e_real))
% 0.48/0.88  (define @t38 () (@list @t33 @t24))
% 0.48/0.88  (define @t39 () (= @t17 tptp.bot_bot_set_variable))
% 0.48/0.88  (define @t40 () (= @t30 tptp.bot_bot_set_variable))
% 0.48/0.88  (define @t41 () (@list @t30 @t17))
% 0.48/0.88  (define @t42 () (@var "X" tptp.set_variable_real))
% 0.48/0.88  (define @t43 () (_ tptp.sup_su1685293586e_real tptp.bot_bo721182586e_real))
% 0.48/0.88  (define @t44 () (@list @t42))
% 0.48/0.88  (define @t45 () (@var "X" tptp.set_variable))
% 0.48/0.88  (define @t46 () (_ tptp.sup_sup_set_variable tptp.bot_bot_set_variable))
% 0.48/0.88  (define @t47 () (@list @t45))
% 0.48/0.88  (define @t48 () (_ tptp.sup_su1685293586e_real @t42))
% 0.48/0.88  (define @t49 () (_ tptp.sup_sup_set_variable @t45))
% 0.48/0.88  (define @t50 () (@var "Y" tptp.set_variable_real))
% 0.48/0.88  (define @t51 () (and (= @t42 tptp.bot_bo721182586e_real) (= @t50 tptp.bot_bo721182586e_real)))
% 0.48/0.88  (define @t52 () (_ @t48 @t50))
% 0.48/0.88  (define @t53 () (@list @t42 @t50))
% 0.48/0.88  (define @t54 () (@var "Y" tptp.set_variable))
% 0.48/0.88  (define @t55 () (and (= @t45 tptp.bot_bot_set_variable) (= @t54 tptp.bot_bot_set_variable)))
% 0.48/0.88  (define @t56 () (_ @t49 @t54))
% 0.48/0.88  (define @t57 () (@list @t45 @t54))
% 0.48/0.88  (define @t58 () (@var "B2" tptp.set_variable_real))
% 0.48/0.88  (define @t59 () (@var "A" tptp.set_variable_real))
% 0.48/0.88  (define @t60 () (and (= @t59 tptp.bot_bo721182586e_real) (= @t58 tptp.bot_bo721182586e_real)))
% 0.48/0.88  (define @t61 () (_ tptp.sup_su1685293586e_real @t59))
% 0.48/0.88  (define @t62 () (_ @t61 @t58))
% 0.48/0.88  (define @t63 () (@list @t59 @t58))
% 0.48/0.88  (define @t64 () (@var "B2" tptp.set_variable))
% 0.48/0.88  (define @t65 () (@var "A" tptp.set_variable))
% 0.48/0.88  (define @t66 () (and (= @t65 tptp.bot_bot_set_variable) (= @t64 tptp.bot_bot_set_variable)))
% 0.48/0.88  (define @t67 () (_ tptp.sup_sup_set_variable @t65))
% 0.48/0.88  (define @t68 () (_ @t67 @t64))
% 0.48/0.88  (define @t69 () (@list @t65 @t64))
% 0.48/0.88  (define @t70 () (@list @t65))
% 0.48/0.88  (define @t71 () (@list @t59))
% 0.48/0.88  (define @t72 () (@var "X2" tptp.variable))
% 0.48/0.88  (define @t73 () (@var "P" (-> tptp.variable Bool)))
% 0.48/0.88  (define @t74 () (_ @t73 @t72))
% 0.48/0.88  (define @t75 () (@list @t72))
% 0.48/0.88  (define @t76 () (forall @t75 (not @t74)))
% 0.48/0.88  (define @t77 () (_ tptp.collect_variable @t73))
% 0.48/0.88  (define @t78 () (@list @t73))
% 0.48/0.88  (define @t79 () (@var "X2" (-> tptp.variable tptp.real)))
% 0.48/0.88  (define @t80 () (@var "P" (-> (-> tptp.variable tptp.real) Bool)))
% 0.48/0.88  (define @t81 () (_ @t80 @t79))
% 0.48/0.88  (define @t82 () (@list @t79))
% 0.48/0.88  (define @t83 () (forall @t82 (not @t81)))
% 0.48/0.88  (define @t84 () (_ tptp.collec633296133e_real @t80))
% 0.48/0.88  (define @t85 () (@list @t80))
% 0.48/0.88  (define @t86 () (= @t77 tptp.bot_bot_set_variable))
% 0.48/0.88  (define @t87 () (= @t84 tptp.bot_bo721182586e_real))
% 0.48/0.88  (define @t88 () (_ tptp.member_variable @t72))
% 0.48/0.88  (define @t89 () (_ @t88 @t30))
% 0.48/0.88  (define @t90 () (@list @t30))
% 0.48/0.88  (define @t91 () (_ tptp.member_variable_real @t79))
% 0.48/0.88  (define @t92 () (_ @t91 @t33))
% 0.48/0.88  (define @t93 () (@list @t33))
% 0.48/0.88  (define @t94 () (@var "C2" tptp.variable))
% 0.48/0.88  (define @t95 () (_ tptp.member_variable @t94))
% 0.48/0.88  (define @t96 () (@var "C2" (-> tptp.variable tptp.real)))
% 0.48/0.88  (define @t97 () (_ tptp.member_variable_real @t96))
% 0.48/0.88  (define @t98 () (@var "X" tptp.variable))
% 0.48/0.88  (define @t99 () (_ tptp.insert_variable @t98))
% 0.48/0.88  (define @t100 () (_ @t99 @t30))
% 0.48/0.88  (define @t101 () (@list @t98 @t30))
% 0.48/0.88  (define @t102 () (@var "X" (-> tptp.variable tptp.real)))
% 0.48/0.88  (define @t103 () (_ tptp.insert_variable_real @t102))
% 0.48/0.88  (define @t104 () (_ @t103 @t33))
% 0.48/0.88  (define @t105 () (@list @t102 @t33))
% 0.48/0.88  (define @t106 () (_ tptp.member_variable @t20))
% 0.48/0.88  (define @t107 () (_ @t106 @t30))
% 0.48/0.88  (define @t108 () (@var "B2" tptp.variable))
% 0.48/0.88  (define @t109 () (= @t20 @t108))
% 0.48/0.88  (define @t110 () (_ tptp.insert_variable @t108))
% 0.48/0.88  (define @t111 () (_ @t106 (_ @t110 @t30)))
% 0.48/0.88  (define @t112 () (@list @t20 @t108 @t30))
% 0.48/0.88  (define @t113 () (_ tptp.member_variable_real @t27))
% 0.48/0.88  (define @t114 () (_ @t113 @t33))
% 0.48/0.88  (define @t115 () (@var "B2" (-> tptp.variable tptp.real)))
% 0.48/0.88  (define @t116 () (= @t27 @t115))
% 0.48/0.88  (define @t117 () (_ tptp.insert_variable_real @t115))
% 0.48/0.88  (define @t118 () (_ @t113 (_ @t117 @t33)))
% 0.48/0.88  (define @t119 () (@list @t27 @t115 @t33))
% 0.48/0.88  (define @t120 () (_ @t110 @t17))
% 0.48/0.88  (define @t121 () (_ @t106 @t120))
% 0.48/0.88  (define @t122 () (_ @t106 @t17))
% 0.48/0.88  (define @t123 () (@list @t20 @t17 @t108))
% 0.48/0.88  (define @t124 () (_ @t117 @t24))
% 0.48/0.88  (define @t125 () (_ @t113 @t124))
% 0.48/0.88  (define @t126 () (_ @t113 @t24))
% 0.48/0.88  (define @t127 () (@list @t27 @t24 @t115))
% 0.48/0.88  (define @t128 () (_ tptp.sup_sup_set_variable @t68))
% 0.48/0.88  (define @t129 () (_ tptp.sup_su1685293586e_real @t62))
% 0.48/0.88  (define @t130 () (_ @t95 @t32))
% 0.48/0.88  (define @t131 () (_ @t95 @t30))
% 0.48/0.88  (define @t132 () (_ @t95 @t17))
% 0.48/0.88  (define @t133 () (@list @t94 @t17 @t30))
% 0.48/0.88  (define @t134 () (_ @t97 @t35))
% 0.48/0.88  (define @t135 () (_ @t97 @t33))
% 0.48/0.88  (define @t136 () (_ @t97 @t24))
% 0.48/0.88  (define @t137 () (@list @t96 @t24 @t33))
% 0.48/0.88  (define @t138 () (_ @t21 tptp.bot_bot_set_variable))
% 0.48/0.88  (define @t139 () (@list @t20))
% 0.48/0.88  (define @t140 () (_ @t28 tptp.bot_bo721182586e_real))
% 0.48/0.88  (define @t141 () (@list @t27))
% 0.48/0.88  (define @t142 () (not @t40))
% 0.48/0.88  (define @t143 () (not @t37))
% 0.48/0.88  (define @t144 () (@var "Y2" tptp.variable))
% 0.48/0.88  (define @t145 () (_ (_ tptp.member_variable @t144) @t30))
% 0.48/0.88  (define @t146 () (@var "Y2" (-> tptp.variable tptp.real)))
% 0.48/0.88  (define @t147 () (_ (_ tptp.member_variable_real @t146) @t33))
% 0.48/0.88  (define @t148 () (not @t107))
% 0.48/0.88  (define @t149 () (not @t114))
% 0.48/0.88  (define @t150 () (@var "B3" tptp.set_variable))
% 0.48/0.88  (define @t151 () (@list @t150))
% 0.48/0.88  (define @t152 () (@list @t20 @t30))
% 0.48/0.88  (define @t153 () (@var "B3" tptp.set_variable_real))
% 0.48/0.88  (define @t154 () (@list @t153))
% 0.48/0.88  (define @t155 () (@list @t27 @t33))
% 0.48/0.88  (define @t156 () (@var "Y" tptp.variable))
% 0.48/0.88  (define @t157 () (_ tptp.insert_variable @t156))
% 0.48/0.88  (define @t158 () (@var "Y" (-> tptp.variable tptp.real)))
% 0.48/0.88  (define @t159 () (_ tptp.insert_variable_real @t158))
% 0.48/0.88  (define @t160 () (@var "C3" tptp.set_variable))
% 0.48/0.88  (define @t161 () (_ tptp.member_variable @t108))
% 0.48/0.88  (define @t162 () (not @t109))
% 0.48/0.88  (define @t163 () (= @t30 @t17))
% 0.48/0.88  (define @t164 () (_ @t21 @t30))
% 0.48/0.88  (define @t165 () (@var "C3" tptp.set_variable_real))
% 0.48/0.88  (define @t166 () (_ tptp.member_variable_real @t115))
% 0.48/0.88  (define @t167 () (not @t116))
% 0.48/0.88  (define @t168 () (= @t33 @t24))
% 0.48/0.88  (define @t169 () (_ @t28 @t33))
% 0.48/0.88  (define @t170 () (_ tptp.member_variable @t98))
% 0.48/0.88  (define @t171 () (not (_ @t170 @t17)))
% 0.48/0.88  (define @t172 () (_ @t170 @t30))
% 0.48/0.88  (define @t173 () (not @t172))
% 0.48/0.88  (define @t174 () (@list @t98 @t30 @t17))
% 0.48/0.88  (define @t175 () (_ tptp.member_variable_real @t102))
% 0.48/0.88  (define @t176 () (not (_ @t175 @t24)))
% 0.48/0.88  (define @t177 () (_ @t175 @t33))
% 0.48/0.88  (define @t178 () (not @t177))
% 0.48/0.88  (define @t179 () (@list @t102 @t33 @t24))
% 0.48/0.88  (define @t180 () (@var "Z" tptp.set_variable))
% 0.48/0.88  (define @t181 () (_ tptp.sup_sup_set_variable @t54))
% 0.48/0.88  (define @t182 () (_ @t49 (_ @t181 @t180)))
% 0.48/0.88  (define @t183 () (@list @t45 @t54 @t180))
% 0.48/0.88  (define @t184 () (@var "Z" tptp.set_variable_real))
% 0.48/0.88  (define @t185 () (_ tptp.sup_su1685293586e_real @t50))
% 0.48/0.88  (define @t186 () (_ @t48 (_ @t185 @t184)))
% 0.48/0.88  (define @t187 () (@list @t42 @t50 @t184))
% 0.48/0.88  (define @t188 () (@var "C2" tptp.set_variable))
% 0.48/0.88  (define @t189 () (_ tptp.sup_sup_set_variable @t64))
% 0.48/0.88  (define @t190 () (_ @t189 @t188))
% 0.48/0.88  (define @t191 () (_ @t67 @t190))
% 0.48/0.88  (define @t192 () (@var "C2" tptp.set_variable_real))
% 0.48/0.88  (define @t193 () (_ tptp.sup_su1685293586e_real @t58))
% 0.48/0.88  (define @t194 () (_ @t61 (_ @t193 @t192)))
% 0.48/0.88  (define @t195 () (@var "X2" tptp.set_variable))
% 0.48/0.88  (define @t196 () (@var "Y3" tptp.set_variable))
% 0.48/0.88  (define @t197 () (@var "X2" tptp.set_variable_real))
% 0.48/0.88  (define @t198 () (@var "Y3" tptp.set_variable_real))
% 0.48/0.88  (define @t199 () (_ @t73 @t20))
% 0.48/0.88  (define @t200 () (_ @t80 @t27))
% 0.48/0.88  (define @t201 () (@var "A3" tptp.set_variable))
% 0.48/0.88  (define @t202 () (@var "B4" tptp.set_variable))
% 0.48/0.88  (define @t203 () (@var "A3" tptp.set_variable_real))
% 0.48/0.88  (define @t204 () (@var "B4" tptp.set_variable_real))
% 0.48/0.88  (define @t205 () (@list @t65 @t64 @t188))
% 0.48/0.88  (define @t206 () (@var "K" tptp.set_variable))
% 0.48/0.88  (define @t207 () (_ tptp.sup_sup_set_variable @t206))
% 0.48/0.88  (define @t208 () (_ @t207 @t68))
% 0.48/0.88  (define @t209 () (@var "K" tptp.set_variable_real))
% 0.48/0.88  (define @t210 () (_ tptp.sup_su1685293586e_real @t209))
% 0.48/0.88  (define @t211 () (_ @t210 @t62))
% 0.48/0.88  (define @t212 () (_ @t31 @t19))
% 0.48/0.88  (define @t213 () (@list @t30 @t17 @t16))
% 0.48/0.88  (define @t214 () (_ @t34 @t26))
% 0.48/0.88  (define @t215 () (@list @t33 @t24 @t23))
% 0.48/0.88  (define @t216 () (@var "A4" tptp.set_variable))
% 0.48/0.88  (define @t217 () (@var "B5" tptp.set_variable))
% 0.48/0.88  (define @t218 () (lambda (@list @t216 @t217) (_ (_ tptp.sup_sup_set_variable @t217) @t216)))
% 0.48/0.88  (define @t219 () (= tptp.sup_sup_set_variable @t218))
% 0.48/0.88  (define @t220 () (@var "A4" tptp.set_variable_real))
% 0.48/0.88  (define @t221 () (@var "B5" tptp.set_variable_real))
% 0.48/0.88  (define @t222 () (_ @t88 @t17))
% 0.48/0.88  (define @t223 () (forall @t75 (=> @t222 @t74)))
% 0.48/0.88  (define @t224 () (_ @t88 @t32))
% 0.48/0.88  (define @t225 () (@list @t30 @t17 @t73))
% 0.48/0.88  (define @t226 () (_ @t91 @t24))
% 0.48/0.88  (define @t227 () (forall @t82 (=> @t226 @t81)))
% 0.48/0.88  (define @t228 () (_ @t91 @t35))
% 0.48/0.88  (define @t229 () (@list @t33 @t24 @t80))
% 0.48/0.88  (define @t230 () (@list @t94 @t30 @t17))
% 0.48/0.88  (define @t231 () (@list @t96 @t33 @t24))
% 0.48/0.88  (define @t232 () (not @t131))
% 0.48/0.88  (define @t233 () (not @t135))
% 0.48/0.88  (define @t234 () (@var "U" tptp.set_variable))
% 0.48/0.88  (define @t235 () (@var "Omega" (-> tptp.variable tptp.real)))
% 0.48/0.88  (define @t236 () (_ (_ @t13 @t235) @t234))
% 0.48/0.88  (define @t237 () (_ tptp.denota1419872369iation @t235))
% 0.48/0.88  (define @t238 () (_ (_ @t237 @t12) @t234))
% 0.48/0.88  (define @t239 () (@var "V" tptp.set_variable))
% 0.48/0.88  (define @t240 () (@list @t12 @t239))
% 0.48/0.88  (define @t241 () (@var "__flatten_var_0" tptp.set_variable))
% 0.48/0.88  (define @t242 () (@var "Omega2" (-> tptp.variable tptp.real)))
% 0.48/0.88  (define @t243 () (@var "Nu3" (-> tptp.variable tptp.real)))
% 0.48/0.88  (define @t244 () (_ @t110 tptp.bot_bot_set_variable))
% 0.48/0.88  (define @t245 () (_ @t117 tptp.bot_bo721182586e_real))
% 0.48/0.88  (define @t246 () (@var "D" tptp.variable))
% 0.48/0.88  (define @t247 () (@var "D" (-> tptp.variable tptp.real)))
% 0.48/0.88  (define @t248 () (= @t108 @t20))
% 0.48/0.88  (define @t249 () (_ @t161 @t138))
% 0.48/0.88  (define @t250 () (@list @t108 @t20))
% 0.48/0.88  (define @t251 () (= @t115 @t27))
% 0.48/0.88  (define @t252 () (_ @t166 @t140))
% 0.48/0.88  (define @t253 () (@list @t115 @t27))
% 0.48/0.88  (define @t254 () (_ tptp.sup_sup_set_variable @t234))
% 0.48/0.88  (define @t255 () (@var "Mu" (-> tptp.variable tptp.real)))
% 0.48/0.88  (define @t256 () (_ @t99 tptp.bot_bot_set_variable))
% 0.48/0.88  (define @t257 () (= @t17 @t256))
% 0.48/0.88  (define @t258 () (= @t30 @t256))
% 0.48/0.88  (define @t259 () (or (and @t40 @t257) (and @t258 @t39) (and @t258 @t257)))
% 0.48/0.88  (define @t260 () (_ @t103 tptp.bot_bo721182586e_real))
% 0.48/0.88  (define @t261 () (= @t24 @t260))
% 0.48/0.88  (define @t262 () (= @t33 @t260))
% 0.48/0.88  (define @t263 () (or (and @t37 @t261) (and @t262 @t36) (and @t262 @t261)))
% 0.48/0.88  (define @t264 () (@var "A3" tptp.variable))
% 0.48/0.88  (define @t265 () (@var "__flatten_var_0" tptp.set_variable_real))
% 0.48/0.88  (define @t266 () (@var "A3" (-> tptp.variable tptp.real)))
% 0.48/0.88  (define @t267 () (@var "X5" (-> tptp.real tptp.variable tptp.real)))
% 0.48/0.88  (define @t268 () (@var "X4" tptp.char))
% 0.48/0.88  (define @t269 () (@var "X3" tptp.denotational_interp))
% 0.48/0.88  (define @t270 () (@var "X22" tptp.trm))
% 0.48/0.88  (define @t271 () (@var "X1" tptp.denotational_interp))
% 0.48/0.88  (define @t272 () (@var "X0" tptp.trm))
% 0.48/0.88  (define @t273 () (@var "Rr" (-> tptp.trm tptp.denotational_interp tptp.trm tptp.denotational_interp tptp.char (-> tptp.real tptp.variable tptp.real) tptp.variable tptp.real)))
% 0.48/0.88  (define @t274 () (_ (_ (_ (_ (_ (_ @t273 @t272) @t271) @t270) @t269) @t268) @t267))
% 0.48/0.88  (define @t275 () (_ (_ tptp.denota1863255036rm_sem @t271) @t272))
% 0.48/0.88  (define @t276 () (_ (_ tptp.denota1863255036rm_sem @t269) @t270))
% 0.48/0.88  (define @t277 () (_ (_ tptp.insert_variable (_ tptp.rVar @t268)) (_ (_ tptp.insert_variable (_ tptp.dVar @t268)) tptp.bot_bot_set_variable)))
% 0.48/0.88  (define @t278 () (_ @t267 tptp.zero_zero_real))
% 0.48/0.88  (define @t279 () (@var "V6" (-> tptp.variable tptp.real)))
% 0.48/0.88  (define @t280 () (exists (@list @t279) (and (_ (_ (_ tptp.denota1419872369iation @t279) @t278) @t277) (not (= (_ @t276 @t279) (_ @t275 @t279))))))
% 0.48/0.88  (define @t281 () (@list @t272 @t271 @t270 @t269 @t268 @t267))
% 0.48/0.88  (define @t282 () (@var "X" tptp.char))
% 0.48/0.88  (define @t283 () (_ (_ tptp.insert_variable (_ tptp.rVar @t282)) (_ (_ tptp.insert_variable (_ tptp.dVar @t282)) tptp.bot_bot_set_variable)))
% 0.48/0.88  (define @t284 () (@var "Zeta" tptp.real))
% 0.48/0.88  (define @t285 () (@var "F" (-> tptp.real tptp.variable tptp.real)))
% 0.48/0.88  (define @t286 () (_ @t285 @t284))
% 0.48/0.88  (define @t287 () (_ tptp.denota1419872369iation @t286))
% 0.48/0.88  (define @t288 () (@var "Theta" tptp.trm))
% 0.48/0.88  (define @t289 () (@var "I2" tptp.denotational_interp))
% 0.48/0.88  (define @t290 () (_ (_ (_ tptp.denota1778088425es_ODE @t289) @t285) @t282))
% 0.48/0.88  (define @t291 () (_ @t290 @t288))
% 0.48/0.88  (define @t292 () (_ @t285 tptp.zero_zero_real))
% 0.48/0.88  (define @t293 () (_ (_ (_ (_ (_ (_ tptp.rr @t272) @t271) @t270) @t269) @t268) @t267))
% 0.48/0.88  (define @t294 () (@var "Y1" tptp.char))
% 0.48/0.88  (define @t295 () (@var "X12" tptp.char))
% 0.48/0.88  (define @t296 () (_ tptp.rVar @t295))
% 0.48/0.88  (define @t297 () (@var "Y22" tptp.char))
% 0.48/0.88  (define @t298 () (@var "X23" tptp.char))
% 0.48/0.88  (define @t299 () (_ tptp.dVar @t298))
% 0.48/0.88  (define @t300 () (@list @t98))
% 0.48/0.88  (define @t301 () (@list @t102))
% 0.48/0.88  (define @t302 () (@var "Ta" tptp.trm))
% 0.48/0.88  (define @t303 () (@var "C4" tptp.char))
% 0.48/0.88  (define @t304 () (@var "F2" (-> tptp.real tptp.variable tptp.real)))
% 0.48/0.88  (define @t305 () (@var "Ia" tptp.denotational_interp))
% 0.48/0.88  (define @t306 () (@var "T" tptp.trm))
% 0.48/0.88  (define @t307 () (@var "I3" tptp.denotational_interp))
% 0.48/0.88  (define @t308 () (_ (_ (_ (_ (_ (_ tptp.rr @t302) @t305) @t306) @t307) @t303) @t304))
% 0.48/0.88  (define @t309 () (@var "X" tptp.real))
% 0.48/0.88  (define @t310 () (@var "X" tptp.nat))
% 0.48/0.88  (define @t311 () (@var "Eta" tptp.trm))
% 0.48/0.88  (define @t312 () (@var "J" tptp.denotational_interp))
% 0.48/0.88  (define @t313 () (@var "Nu5" (-> tptp.variable tptp.real)))
% 0.48/0.88  (define @t314 () (_ tptp.denota1863255036rm_sem @t289))
% 0.48/0.88  (define @t315 () (_ @t314 @t288))
% 0.48/0.88  (define @t316 () (@var "Variable" tptp.variable))
% 0.48/0.88  (define @t317 () (@var "X6" tptp.char))
% 0.48/0.88  (define @t318 () (@list @t317))
% 0.48/0.88  (define @t319 () (@var "X24" tptp.char))
% 0.48/0.88  (define @t320 () (@var "X13" tptp.char))
% 0.48/0.88  (define @t321 () (_ (_ @t287 @t292) @t6))
% 0.48/0.88  (define @t322 () (_ (_ tptp.uSubst1599435252djoint tptp.sigma) tptp.i))
% 0.48/0.88  (define @t323 () (_ tptp.denota1778088425es_ODE (_ @t322 tptp.omega)))
% 0.48/0.88  (define @t324 () (@list @t285 @t288 @t284))
% 0.48/0.88  (define @t325 () (_ (_ (_ @t323 tptp.f) tptp.x) tptp.theta))
% 0.48/0.88  (define @t326 () (_ tptp.is_sin155454833riable @t30))
% 0.48/0.88  (define @t327 () (@var "X6" tptp.variable))
% 0.48/0.88  (define @t328 () (_ tptp.member_variable @t327))
% 0.48/0.88  (define @t329 () (_ @t328 @t30))
% 0.48/0.88  (define @t330 () (_ tptp.is_sin524757308e_real @t33))
% 0.48/0.88  (define @t331 () (@var "X6" (-> tptp.variable tptp.real)))
% 0.48/0.88  (define @t332 () (_ tptp.member_variable_real @t331))
% 0.48/0.88  (define @t333 () (_ @t332 @t33))
% 0.48/0.88  (define @t334 () (@list @t216))
% 0.48/0.88  (define @t335 () (@list @t220))
% 0.48/0.88  (define @t336 () (@list @t327))
% 0.48/0.88  (define @t337 () (@list @t331))
% 0.48/0.88  (define @t338 () (_ (_ tptp.uSubst516392818stappt tptp.sigma) @t8))
% 0.48/0.88  (define @t339 () (_ tptp.denota1778088425es_ODE tptp.i))
% 0.48/0.88  (define @t340 () (_ @t338 tptp.theta))
% 0.48/0.88  (define @t341 () (_ tptp.the_trm @t340))
% 0.48/0.88  (define @t342 () (@list @t295))
% 0.48/0.88  (define @t343 () (@var "Sigma" tptp.produc1418842292n_game))
% 0.48/0.88  (define @t344 () (_ (_ tptp.uSubst1599435252djoint @t343) @t289))
% 0.48/0.88  (define @t345 () (_ tptp.uSubst516392818stappt @t343))
% 0.48/0.88  (define @t346 () (_ @t345 @t234))
% 0.48/0.88  (define @t347 () (_ @t346 @t288))
% 0.48/0.88  (define @t348 () (not (= @t347 tptp.none_trm)))
% 0.48/0.88  (define @t349 () (_ (_ @t345 @t239) @t288))
% 0.48/0.88  (define @t350 () (_ (_ @t345 @t283) @t288))
% 0.48/0.88  (define @t351 () (@list @t298))
% 0.48/0.88  (define @t352 () (@var "Option2" tptp.option_trm))
% 0.48/0.88  (define @t353 () (@var "Option" tptp.option_trm))
% 0.48/0.88  (define @t354 () (_ tptp.the_trm @t353))
% 0.48/0.88  (define @t355 () (= @t352 tptp.none_trm))
% 0.48/0.88  (define @t356 () (= @t353 tptp.none_trm))
% 0.48/0.88  (define @t357 () (not @t356))
% 0.48/0.88  (define @t358 () (@var "D" tptp.real))
% 0.48/0.88  (define @t359 () (_ (_ tptp.denotational_repv @t235) @t98))
% 0.48/0.88  (define @t360 () (_ @t359 @t358))
% 0.48/0.88  (define @t361 () (@list @t235 @t98 @t358))
% 0.48/0.88  (define @t362 () (_ tptp.insert_option_trm tptp.none_trm))
% 0.48/0.88  (define @t363 () (@var "B" tptp.set_option_trm))
% 0.48/0.88  (define @t364 () (= @t363 (_ @t362 tptp.bot_bo946428664on_trm)))
% 0.48/0.88  (define @t365 () (= @t363 tptp.bot_bo946428664on_trm))
% 0.48/0.88  (define @t366 () (= (_ tptp.these_trm @t363) tptp.bot_bot_set_trm))
% 0.48/0.88  (define @t367 () (@list @t363))
% 0.48/0.88  (define @t368 () (@var "B" tptp.set_option_variable))
% 0.48/0.88  (define @t369 () (= @t368 (_ (_ tptp.insert1340772453riable tptp.none_variable) tptp.bot_bo266290559riable)))
% 0.48/0.88  (define @t370 () (= @t368 tptp.bot_bo266290559riable))
% 0.48/0.88  (define @t371 () (= (_ tptp.these_variable @t368) tptp.bot_bot_set_variable))
% 0.48/0.88  (define @t372 () (@list @t368))
% 0.48/0.88  (define @t373 () (@var "B" tptp.set_op12188086e_real))
% 0.48/0.88  (define @t374 () (= @t373 (_ (_ tptp.insert526581936e_real tptp.none_variable_real) tptp.bot_bo1411475018e_real)))
% 0.48/0.88  (define @t375 () (= @t373 tptp.bot_bo1411475018e_real))
% 0.48/0.88  (define @t376 () (= (_ tptp.these_variable_real @t373) tptp.bot_bo721182586e_real))
% 0.48/0.88  (define @t377 () (@list @t373))
% 0.48/0.88  (define @t378 () (_ @t235 @t98))
% 0.48/0.88  (define @t379 () (_ tptp.these_variable tptp.bot_bo266290559riable))
% 0.48/0.88  (define @t380 () (@var "A2" tptp.set_option_trm))
% 0.48/0.88  (define @t381 () (_ tptp.these_trm @t380))
% 0.48/0.88  (define @t382 () (@var "A2" tptp.set_option_variable))
% 0.48/0.88  (define @t383 () (_ tptp.these_variable @t382))
% 0.48/0.88  (define @t384 () (_ tptp.some_variable @t98))
% 0.48/0.88  (define @t385 () (@list @t98 @t382))
% 0.48/0.88  (define @t386 () (@var "A2" tptp.set_op12188086e_real))
% 0.48/0.88  (define @t387 () (_ tptp.these_variable_real @t386))
% 0.48/0.88  (define @t388 () (_ tptp.some_variable_real @t102))
% 0.48/0.88  (define @t389 () (@list @t102 @t386))
% 0.48/0.88  (define @t390 () (@var "X" tptp.trm))
% 0.48/0.88  (define @t391 () (_ tptp.some_trm @t390))
% 0.48/0.88  (define @t392 () (@list @t390 @t380))
% 0.48/0.88  (define @t393 () (@var "X7" tptp.set_variable_real))
% 0.48/0.88  (define @t394 () (_ tptp.static_selectlike @t393))
% 0.48/0.88  (define @t395 () (_ @t394 @t235))
% 0.48/0.88  (define @t396 () (_ tptp.member_variable_real @t360))
% 0.48/0.88  (define @t397 () (_ @t396 (_ @t395 (_ @t157 tptp.bot_bot_set_variable))))
% 0.48/0.88  (define @t398 () (_ @t396 @t393))
% 0.48/0.88  (define @t399 () (not (= @t98 @t156)))
% 0.48/0.88  (define @t400 () (@list @t98 @t156 @t235 @t358 @t393))
% 0.48/0.88  (define @t401 () (= @t358 @t378))
% 0.48/0.88  (define @t402 () (@var "Y22" tptp.trm))
% 0.48/0.88  (define @t403 () (@var "X23" tptp.trm))
% 0.48/0.88  (define @t404 () (_ tptp.some_trm @t403))
% 0.48/0.88  (define @t405 () (_ tptp.member_variable_real @t12))
% 0.48/0.88  (define @t406 () (_ @t405 @t393))
% 0.48/0.88  (define @t407 () (_ @t394 @t12))
% 0.48/0.88  (define @t408 () (_ @t407 @t239))
% 0.48/0.88  (define @t409 () (@var "Y3" tptp.trm))
% 0.48/0.88  (define @t410 () (@var "X" tptp.option_trm))
% 0.48/0.88  (define @t411 () (= @t410 (_ tptp.some_trm @t409)))
% 0.48/0.88  (define @t412 () (@list @t409))
% 0.48/0.88  (define @t413 () (= @t410 tptp.none_trm))
% 0.48/0.88  (define @t414 () (@list @t410))
% 0.48/0.88  (define @t415 () (@var "W" tptp.set_variable))
% 0.48/0.88  (define @t416 () (_ (_ tptp.sup_sup_set_variable @t239) @t415))
% 0.48/0.88  (define @t417 () (_ tptp.some_trm @t354))
% 0.48/0.88  (define @t418 () (@list @t353))
% 0.48/0.88  (define @t419 () (_ tptp.member_trm @t390))
% 0.48/0.88  (define @t420 () (@var "Y4" tptp.set_variable_real))
% 0.48/0.88  (define @t421 () (_ (_ tptp.static_selectlike @t420) @t12))
% 0.48/0.88  (define @t422 () (_ @t421 @t239))
% 0.48/0.88  (define @t423 () (@list @t403))
% 0.48/0.88  (define @t424 () (@var "X24" tptp.trm))
% 0.48/0.88  (define @t425 () (@var "Y" tptp.option_trm))
% 0.48/0.88  (define @t426 () (= @t425 tptp.none_trm))
% 0.48/0.88  (define @t427 () (not @t426))
% 0.48/0.88  (define @t428 () (@var "P" (-> tptp.option_trm Bool)))
% 0.48/0.88  (define @t429 () (@var "X6" tptp.trm))
% 0.48/0.88  (define @t430 () (@list @t429))
% 0.48/0.88  (define @t431 () (_ @t428 tptp.none_trm))
% 0.48/0.88  (define @t432 () (@var "X2" tptp.trm))
% 0.48/0.88  (define @t433 () (@var "P3" (-> tptp.option_trm Bool)))
% 0.48/0.88  (define @t434 () (_ @t433 (_ tptp.some_trm @t432)))
% 0.48/0.88  (define @t435 () (@list @t432))
% 0.48/0.88  (define @t436 () (_ @t433 tptp.none_trm))
% 0.48/0.88  (define @t437 () (@list @t433))
% 0.48/0.88  (define @t438 () (@var "X8" tptp.option_trm))
% 0.48/0.88  (define @t439 () (@var "P2" (-> tptp.option_trm Bool)))
% 0.48/0.88  (define @t440 () (_ @t439 @t438))
% 0.48/0.88  (define @t441 () (@list @t438))
% 0.48/0.88  (define @t442 () (@list @t439))
% 0.48/0.88  (define @t443 () (@var "P" (-> tptp.option_trm tptp.option_trm Bool)))
% 0.48/0.88  (define @t444 () (_ (_ @t443 @t410) @t425))
% 0.48/0.88  (define @t445 () (@var "B6" tptp.trm))
% 0.48/0.88  (define @t446 () (@var "A5" tptp.trm))
% 0.48/0.88  (define @t447 () (@var "A1" tptp.option_trm))
% 0.48/0.88  (define @t448 () (@var "A0" tptp.char))
% 0.48/0.88  (define @t449 () (@var "P" (-> tptp.char tptp.option_trm Bool)))
% 0.48/0.88  (define @t450 () (_ @t449 @t317))
% 0.48/0.88  (define @t451 () (@var "Theta2" tptp.trm))
% 0.48/0.88  (define @t452 () (_ tptp.some_trm @t451))
% 0.48/0.88  (define @t453 () (@var "T2" tptp.trm))
% 0.48/0.88  (define @t454 () (@var "Theta" tptp.option_trm))
% 0.48/0.88  (define @t455 () (= @t454 tptp.none_trm))
% 0.48/0.88  (define @t456 () (@var "A0" tptp.option_trm))
% 0.48/0.88  (define @t457 () (@var "V2" tptp.trm))
% 0.48/0.88  (define @t458 () (_ tptp.some_trm @t457))
% 0.48/0.88  (define @t459 () (@list @t457))
% 0.48/0.88  (define @t460 () (@var "X_1" tptp.option_trm))
% 0.48/0.88  (define @t461 () (@var "Eta2" tptp.trm))
% 0.48/0.88  (define @t462 () (_ tptp.some_trm @t461))
% 0.48/0.88  (define @t463 () (@var "A0" tptp.variable))
% 0.48/0.88  (define @t464 () (@var "P" (-> tptp.variable tptp.option_trm Bool)))
% 0.48/0.88  (define @t465 () (_ @t464 @t327))
% 0.48/0.88  (define @t466 () (= @t410 @t452))
% 0.48/0.88  (define @t467 () (@list @t451))
% 0.48/0.88  (define @t468 () (_ tptp.set_option_trm2 @t404))
% 0.48/0.88  (define @t469 () (@var "X23" tptp.variable))
% 0.48/0.88  (define @t470 () (_ tptp.set_option_variable2 (_ tptp.some_variable @t469)))
% 0.48/0.88  (define @t471 () (@list @t469))
% 0.48/0.88  (define @t472 () (@var "X23" (-> tptp.variable tptp.real)))
% 0.48/0.88  (define @t473 () (_ tptp.set_op697949218e_real (_ tptp.some_variable_real @t472)))
% 0.48/0.89  (define @t474 () (@list @t472))
% 0.48/0.89  (define @t475 () (_ tptp.denotational_Vagree @t235))
% 0.48/0.89  (define @t476 () (_ @t475 @t360))
% 0.48/0.89  (define @t477 () (@var "Xo" tptp.option_variable))
% 0.48/0.89  (define @t478 () (_ tptp.set_option_variable2 @t477))
% 0.48/0.89  (define @t479 () (@var "Xo" tptp.option_variable_real))
% 0.48/0.89  (define @t480 () (_ tptp.set_op697949218e_real @t479))
% 0.48/0.89  (define @t481 () (@var "Xo" tptp.option_trm))
% 0.48/0.89  (define @t482 () (_ tptp.set_option_trm2 @t481))
% 0.48/0.89  (define @t483 () (_ tptp.denotational_Vagree @t12))
% 0.48/0.89  (define @t484 () (_ @t483 @t11))
% 0.48/0.89  (define @t485 () (_ @t484 @t416))
% 0.48/0.89  (define @t486 () (_ @t484 @t415))
% 0.48/0.89  (define @t487 () (_ @t484 @t239))
% 0.48/0.89  (define @t488 () (@list @t12 @t11 @t239 @t415))
% 0.48/0.89  (define @t489 () (_ @t395 @t239))
% 0.48/0.89  (define @t490 () (_ (_ @t483 @t235) @t239))
% 0.48/0.89  (define @t491 () (@list @t12 @t235 @t239 @t393))
% 0.48/0.89  (define @t492 () (@var "E" tptp.variable))
% 0.48/0.89  (define @t493 () (@var "A" tptp.option_variable))
% 0.48/0.89  (define @t494 () (_ tptp.set_option_variable2 @t493))
% 0.48/0.89  (define @t495 () (@var "E" (-> tptp.variable tptp.real)))
% 0.48/0.89  (define @t496 () (@var "A" tptp.option_variable_real))
% 0.48/0.89  (define @t497 () (_ tptp.set_op697949218e_real @t496))
% 0.48/0.89  (define @t498 () (@var "E" tptp.trm))
% 0.48/0.89  (define @t499 () (@var "A" tptp.option_trm))
% 0.48/0.89  (define @t500 () (_ tptp.set_option_trm2 @t499))
% 0.48/0.89  (define @t501 () (@var "P" (-> tptp.trm Bool)))
% 0.48/0.89  (define @t502 () (@var "A2" tptp.option_trm))
% 0.48/0.89  (define @t503 () (@var "Nu4" (-> tptp.variable tptp.real)))
% 0.48/0.89  (define @t504 () (@list @t12 @t11 @t239))
% 0.48/0.89  (define @t505 () (@var "V4" tptp.trm))
% 0.48/0.89  (define @t506 () (_ tptp.uminus1851247844riable @t54))
% 0.48/0.89  (define @t507 () (_ tptp.uminus1851247844riable @t45))
% 0.48/0.89  (define @t508 () (_ tptp.uminus430703407e_real @t50))
% 0.48/0.89  (define @t509 () (_ tptp.uminus430703407e_real @t42))
% 0.48/0.89  (define @t510 () (_ tptp.uminus1851247844riable @t30))
% 0.48/0.89  (define @t511 () (_ tptp.uminus430703407e_real @t33))
% 0.48/0.89  (define @t512 () (_ @t95 @t510))
% 0.48/0.89  (define @t513 () (@list @t94 @t30))
% 0.48/0.89  (define @t514 () (_ @t97 @t511))
% 0.48/0.89  (define @t515 () (@list @t96 @t33))
% 0.48/0.89  (define @t516 () (@var "A" tptp.real))
% 0.48/0.89  (define @t517 () (_ tptp.uminus_uminus_real @t516))
% 0.48/0.89  (define @t518 () (@list @t516))
% 0.48/0.89  (define @t519 () (= @t516 tptp.zero_zero_real))
% 0.48/0.89  (define @t520 () (_ tptp.uminus1851247844riable @t239))
% 0.48/0.89  (define @t521 () (@var "Eta" tptp.option_trm))
% 0.48/0.89  (define @t522 () (= (_ @t407 @t520) (_ @t421 @t520)))
% 0.48/0.89  (define @t523 () (@var "Mu2" (-> tptp.variable tptp.real)))
% 0.48/0.89  (define @t524 () (_ tptp.member_variable_real @t523))
% 0.48/0.89  (define @t525 () (= (_ @t524 @t393) (_ @t524 @t420)))
% 0.48/0.89  (define @t526 () (_ (_ tptp.denota1419872369iation @t523) @t12))
% 0.48/0.89  (define @t527 () (@list @t523))
% 0.48/0.89  (define @t528 () (@list @t12 @t239 @t393 @t420))
% 0.48/0.89  (define @t529 () (= @t408 @t422))
% 0.48/0.89  (define @t530 () (@var "Mu3" (-> tptp.variable tptp.real)))
% 0.48/0.89  (define @t531 () (_ tptp.member_variable_real @t530))
% 0.48/0.89  (define @t532 () (= (_ @t531 @t393) (_ @t531 @t420)))
% 0.48/0.89  (define @t533 () (_ (_ tptp.denota1419872369iation @t530) @t12))
% 0.48/0.89  (define @t534 () (@list @t530))
% 0.48/0.89  (define @t535 () (@list @t393 @t12 @t239 @t420))
% 0.48/0.89  (define @t536 () (@var "Z" tptp.variable))
% 0.48/0.89  (define @t537 () (_ tptp.insert_variable @t536))
% 0.48/0.89  (define @t538 () (@var "S" tptp.set_variable))
% 0.48/0.89  (define @t539 () (_ @t537 @t538))
% 0.48/0.89  (define @t540 () (@var "W2" (-> tptp.variable tptp.real)))
% 0.48/0.89  (define @t541 () (@var "V4" (-> tptp.variable tptp.real)))
% 0.48/0.89  (define @t542 () (_ (_ tptp.stateinterpol @t541) @t540))
% 0.48/0.89  (define @t543 () (@var "Xa" tptp.option_trm))
% 0.48/0.89  (define @t544 () (@var "Y62" tptp.trm))
% 0.48/0.89  (define @t545 () (@var "X62" tptp.trm))
% 0.48/0.89  (define @t546 () (@var "Y61" tptp.trm))
% 0.48/0.89  (define @t547 () (@var "X61" tptp.trm))
% 0.48/0.89  (define @t548 () (_ @t12 @t98))
% 0.48/0.89  (define @t549 () (_ (_ tptp.stateinterpol @t12) @t235))
% 0.48/0.89  (define @t550 () (_ @t549 @t538))
% 0.48/0.89  (define @t551 () (_ @t550 @t98))
% 0.48/0.89  (define @t552 () (_ @t170 @t538))
% 0.48/0.89  (define @t553 () (@list @t98 @t538 @t12 @t235))
% 0.48/0.89  (define @t554 () (@list @t12 @t235))
% 0.48/0.89  (define @t555 () (_ @t346 @t311))
% 0.48/0.89  (define @t556 () (_ (_ tptp.times @t288) @t311))
% 0.48/0.89  (define @t557 () (_ @t346 @t556))
% 0.48/0.89  (define @t558 () (@list @t343 @t234 @t288 @t311))
% 0.48/0.89  (define @t559 () (_ (_ tptp.statediff @t12) @t235))
% 0.48/0.89  (define @t560 () (@var "Omega3" (-> tptp.variable tptp.real)))
% 0.48/0.89  (define @t561 () (_ (_ tptp.stateinterpol @t235) @t560))
% 0.48/0.89  (define @t562 () (@var "T3" tptp.trm))
% 0.48/0.89  (define @t563 () (_ @t314 @t562))
% 0.48/0.89  (define @t564 () (= (_ @t315 @t235) (_ @t315 @t560)))
% 0.48/0.89  (define @t565 () (_ tptp.static_FVT @t288))
% 0.48/0.89  (define @t566 () (_ @t475 @t560))
% 0.48/0.89  (define @t567 () (_ tptp.ord_le282106107riable @t45))
% 0.48/0.89  (define @t568 () (_ (_ tptp.ord_le282106107riable @t30) @t17))
% 0.48/0.89  (define @t569 () (_ tptp.inf_inf_set_variable @t65))
% 0.48/0.89  (define @t570 () (_ tptp.inf_inf_set_variable @t45))
% 0.48/0.89  (define @t571 () (_ @t569 @t64))
% 0.48/0.89  (define @t572 () (_ @t570 @t54))
% 0.48/0.89  (define @t573 () (_ @t97 (_ (_ tptp.inf_in1556002680e_real @t33) @t24)))
% 0.48/0.89  (define @t574 () (_ @t95 (_ (_ tptp.inf_inf_set_variable @t30) @t17)))
% 0.48/0.89  (define @t575 () (@var "N" tptp.nat))
% 0.48/0.89  (define @t576 () (_ tptp.ord_le1113654598e_real @t50))
% 0.48/0.89  (define @t577 () (_ tptp.ord_le282106107riable @t54))
% 0.48/0.89  (define @t578 () (_ @t567 @t180))
% 0.48/0.89  (define @t579 () (_ tptp.ord_le282106107riable @t65))
% 0.48/0.89  (define @t580 () (@var "P" Bool))
% 0.48/0.89  (define @t581 () (@var "Y" tptp.real))
% 0.48/0.89  (define @t582 () (@list @t309 @t581))
% 0.48/0.89  (define @t583 () (_ (_ tptp.sup_sup_set_variable @t6) tptp.u))
% 0.48/0.89  (define @t584 () (not (_ @t10 @t583)))
% 0.48/0.89  (define @t585 () (@var "I" tptp.variable))
% 0.48/0.89  (define @t586 () (_ @t503 @t585))
% 0.48/0.89  (define @t587 () (_ @t243 @t585))
% 0.48/0.89  (define @t588 () (= @t587 @t586))
% 0.48/0.89  (define @t589 () (@var "U2" tptp.set_variable))
% 0.48/0.89  (define @t590 () (_ tptp.member_variable @t585))
% 0.48/0.89  (define @t591 () (_ @t590 @t589))
% 0.48/0.89  (define @t592 () (not @t591))
% 0.48/0.89  (define @t593 () (@list @t585))
% 0.48/0.89  (define @t594 () (forall @t593 (=> @t592 @t588)))
% 0.48/0.89  (define @t595 () (@list @t243 @t503 @t589))
% 0.48/0.89  (define @t596 () (lambda @t595 @t594))
% 0.48/0.89  (define @t597 () (lambda @t75 (_ @t88 tptp.bot_bot_set_variable)))
% 0.48/0.89  (define @t598 () (lambda @t82 (_ @t91 tptp.bot_bo721182586e_real)))
% 0.48/0.89  (define @t599 () (lambda @t334 (= @t216 (_ (_ tptp.insert_variable (_ tptp.the_elem_variable @t216)) tptp.bot_bot_set_variable))))
% 0.48/0.89  (define @t600 () (lambda @t335 (= @t220 (_ (_ tptp.insert_variable_real (_ tptp.the_el1059226619e_real @t220)) tptp.bot_bo721182586e_real))))
% 0.48/0.89  (define @t601 () (lambda @t334 (= @t216 tptp.bot_bot_set_variable)))
% 0.48/0.89  (define @t602 () (lambda @t335 (= @t220 tptp.bot_bo721182586e_real)))
% 0.48/0.89  (define @t603 () (@var "Y3" tptp.variable))
% 0.48/0.89  (define @t604 () (@var "R" tptp.real))
% 0.48/0.89  (define @t605 () (lambda (@list @t242 @t72 @t604 @t603) (_ (_ (_ tptp.if_real (= @t72 @t603)) @t604) (_ @t242 @t603))))
% 0.48/0.89  (define @t606 () (@var "V3" tptp.set_variable))
% 0.48/0.89  (define @t607 () (lambda (@list @t243 @t503 @t606) (forall @t593 (=> (_ @t590 @t606) @t588))))
% 0.48/0.89  (define @t608 () (@var "S2" tptp.set_variable))
% 0.48/0.89  (define @t609 () (lambda (@list @t243 @t242 @t608 @t72) (_ (_ (_ tptp.if_real (_ @t88 @t608)) (_ @t243 @t72)) (_ @t242 @t72))))
% 0.48/0.89  (define @t610 () (tptp.omega @t585))
% 0.48/0.89  (define @t611 () (tptp.f tptp.zero_zero_real @t585))
% 0.48/0.89  (define @t612 () (= @t611 @t610))
% 0.48/0.89  (define @t613 () (tptp.these_variable tptp.bot_bo266290559riable))
% 0.48/0.89  (define @t614 () (tptp.dVar tptp.x))
% 0.48/0.89  (define @t615 () (tptp.insert_variable @t614 @t379))
% 0.48/0.89  (define @t616 () (tptp.rVar tptp.x))
% 0.48/0.89  (define @t617 () (tptp.insert_variable @t616 @t615))
% 0.48/0.89  (define @t618 () (tptp.sup_sup_set_variable tptp.u @t617))
% 0.48/0.89  (define @t619 () (tptp.member_variable @t585 @t618))
% 0.48/0.89  (define @t620 () (or @t619 @t612))
% 0.48/0.89  (define @t621 () (tptp.insert_variable @t614 tptp.bot_bot_set_variable))
% 0.48/0.89  (define @t622 () (tptp.insert_variable @t616 @t621))
% 0.48/0.89  (define @t623 () (tptp.sup_sup_set_variable tptp.u @t622))
% 0.48/0.89  (define @t624 () (tptp.member_variable @t585 @t623))
% 0.48/0.89  (define @t625 () (or @t624 @t612))
% 0.48/0.89  (define @t626 () (tptp.member_variable @t585 @t8))
% 0.48/0.89  (define @t627 () (or @t626 @t612))
% 0.48/0.89  (define @t628 () (forall @t593 @t627))
% 0.48/0.89  (define @t629 () (tptp.member_variable @t585 @t589))
% 0.48/0.89  (define @t630 () (@list @t589))
% 0.48/0.89  (define @t631 () (lambda @t630 (forall @t593 (or @t629 @t612))))
% 0.48/0.89  (define @t632 () (or @t629 (= @t610 @t611)))
% 0.48/0.89  (define @t633 () (forall @t593 @t632))
% 0.48/0.89  (define @t634 () (lambda @t630 @t633))
% 0.48/0.89  (define @t635 () (_ @t503 @t585))
% 0.48/0.89  (define @t636 () (@list @t503 @t589))
% 0.48/0.89  (define @t637 () (_ @t9 @t585))
% 0.48/0.89  (define @t638 () (= @t635 @t637))
% 0.48/0.89  (define @t639 () (or @t629 @t638))
% 0.48/0.89  (define @t640 () (_ @t9 @t585))
% 0.48/0.89  (define @t641 () (= @t640 @t635))
% 0.48/0.89  (define @t642 () (or @t629 @t641))
% 0.48/0.89  (define @t643 () (forall @t593 @t642))
% 0.48/0.89  (define @t644 () (lambda @t636 @t643))
% 0.48/0.89  (define @t645 () (_ @t243 @t585))
% 0.48/0.89  (define @t646 () (_ (lambda @t595 (forall @t593 (or @t629 (= @t645 @t635)))) @t9))
% 0.48/0.89  (define @t647 () (or @t591 @t588))
% 0.48/0.89  (define @t648 () (tptp.insert_variable @t614 @t613))
% 0.48/0.89  (define @t649 () (tptp.insert_variable @t616 @t648))
% 0.48/0.89  (define @t650 () (tptp.sup_sup_set_variable @t649 tptp.u))
% 0.48/0.89  (define @t651 () (@quantifiers_skolemize (forall @t593 (or (tptp.member_variable @t585 @t650) @t612)) 0))
% 0.48/0.89  (define @t652 () (tptp.sup_sup_set_variable @t617 tptp.u))
% 0.48/0.89  (define @t653 () (tptp.member_variable @t585 @t652))
% 0.48/0.89  (define @t654 () (or @t653 @t612))
% 0.48/0.89  (define @t655 () (forall @t593 @t654))
% 0.48/0.89  (define @t656 () (tptp.sup_sup_set_variable @t622 tptp.u))
% 0.48/0.89  (define @t657 () (tptp.member_variable @t585 @t656))
% 0.48/0.89  (define @t658 () (or @t657 @t612))
% 0.48/0.89  (define @t659 () (forall @t593 @t658))
% 0.48/0.89  (define @t660 () (tptp.member_variable @t585 @t583))
% 0.48/0.89  (define @t661 () (or @t660 @t612))
% 0.48/0.89  (define @t662 () (forall @t593 @t661))
% 0.48/0.89  (define @t663 () (= (tptp.f tptp.zero_zero_real @t651) (tptp.omega @t651)))
% 0.48/0.89  (define @t664 () (tptp.member_variable @t651 @t650))
% 0.48/0.89  (define @t665 () (or @t664 @t663))
% 0.48/0.89  (define @t666 () (@list true))
% 0.48/0.89  (define @t667 () (@list @t665))
% 0.48/0.89  (define @t668 () (tptp.sup_sup_set_variable tptp.u @t649))
% 0.48/0.89  (define @t669 () (tptp.member_variable @t651 @t668))
% 0.48/0.89  (define @t670 () (or @t669 @t663))
% 0.48/0.89  (define @t671 () (@purify @t218))
% 0.48/0.89  (define @t672 () (_ @t2 @t379))
% 0.48/0.89  (define @t673 () (_ @t5 @t672))
% 0.48/0.89  (define @t674 () (_ (_ tptp.sup_sup_set_variable @t649) tptp.u))
% 0.48/0.89  (define @t675 () (= @t668 @t674))
% 0.48/0.89  (define @t676 () (= tptp.sup_sup_set_variable @t671))
% 0.48/0.89  (define @t677 () (=> @t676 @t675))
% 0.48/0.89  (assume @p1 (_ @t10 @t8))
% 0.48/0.89  (assume @p2 (forall @t15 (= (_ @t14 tptp.bot_bot_set_variable) (= @t12 @t11))))
% 0.48/0.89  (assume @p3 (forall (@list @t20 @t17 @t16) (= (_ (_ tptp.sup_sup_set_variable @t22) @t16) (_ @t21 @t19))))
% 0.48/0.89  (assume @p4 (forall (@list @t27 @t24 @t23) (= (_ (_ tptp.sup_su1685293586e_real @t29) @t23) (_ @t28 @t26))))
% 0.48/0.89  (assume @p5 (forall (@list @t30 @t20 @t17) (= (_ @t31 @t22) (_ @t21 @t32))))
% 0.48/0.89  (assume @p6 (forall (@list @t33 @t27 @t24) (= (_ @t34 @t29) (_ @t28 @t35))))
% 0.48/0.89  (assume @p7 (forall @t38 (= (= @t35 tptp.bot_bo721182586e_real) (and @t37 @t36))))
% 0.48/0.89  (assume @p8 (forall @t41 (= (= @t32 tptp.bot_bot_set_variable) (and @t40 @t39))))
% 0.48/0.89  (assume @p9 (forall @t44 (= (_ @t43 @t42) @t42)))
% 0.48/0.89  (assume @p10 (forall @t47 (= (_ @t46 @t45) @t45)))
% 0.48/0.89  (assume @p11 (forall @t44 (= (_ @t48 tptp.bot_bo721182586e_real) @t42)))
% 0.48/0.89  (assume @p12 (forall @t47 (= (_ @t49 tptp.bot_bot_set_variable) @t45)))
% 0.48/0.89  (assume @p13 (forall @t53 (= (= tptp.bot_bo721182586e_real @t52) @t51)))
% 0.48/0.89  (assume @p14 (forall @t57 (= (= tptp.bot_bot_set_variable @t56) @t55)))
% 0.48/0.89  (assume @p15 (forall @t53 (= (= @t52 tptp.bot_bo721182586e_real) @t51)))
% 0.48/0.89  (assume @p16 (forall @t57 (= (= @t56 tptp.bot_bot_set_variable) @t55)))
% 0.48/0.89  (assume @p17 (forall @t63 (= (= @t62 tptp.bot_bo721182586e_real) @t60)))
% 0.48/0.89  (assume @p18 (forall @t69 (= (= @t68 tptp.bot_bot_set_variable) @t66)))
% 0.48/0.89  (assume @p19 (forall @t70 (= (_ @t46 @t65) @t65)))
% 0.48/0.89  (assume @p20 (forall @t71 (= (_ @t43 @t59) @t59)))
% 0.48/0.89  (assume @p21 (forall @t69 (= (= tptp.bot_bot_set_variable @t68) @t66)))
% 0.48/0.89  (assume @p22 (forall @t63 (= (= tptp.bot_bo721182586e_real @t62) @t60)))
% 0.48/0.89  (assume @p23 (forall @t70 (= (_ @t67 tptp.bot_bot_set_variable) @t65)))
% 0.48/0.89  (assume @p24 (forall @t71 (= (_ @t61 tptp.bot_bo721182586e_real) @t59)))
% 0.48/0.89  (assume @p25 (forall @t78 (= (= tptp.bot_bot_set_variable @t77) @t76)))
% 0.48/0.89  (assume @p26 (forall @t85 (= (= tptp.bot_bo721182586e_real @t84) @t83)))
% 0.48/0.89  (assume @p27 (forall @t78 (= @t86 @t76)))
% 0.48/0.89  (assume @p28 (forall @t85 (= @t87 @t83)))
% 0.48/0.89  (assume @p29 (forall @t90 (= (forall @t75 (not @t89)) @t40)))
% 0.48/0.89  (assume @p30 (forall @t93 (= (forall @t82 (not @t92)) @t37)))
% 0.48/0.89  (assume @p31 (forall (@list @t94) (not (_ @t95 tptp.bot_bot_set_variable))))
% 0.48/0.89  (assume @p32 (forall (@list @t96) (not (_ @t97 tptp.bot_bo721182586e_real))))
% 0.48/0.89  (assume @p33 (forall @t101 (= (_ @t99 @t100) @t100)))
% 0.48/0.89  (assume @p34 (forall @t105 (= (_ @t103 @t104) @t104)))
% 0.48/0.89  (assume @p35 (forall @t112 (= @t111 (or @t109 @t107))))
% 0.48/0.89  (assume @p36 (forall @t119 (= @t118 (or @t116 @t114))))
% 0.48/0.89  (assume @p37 (forall @t123 (=> (=> (not @t122) @t109) @t121)))
% 0.48/0.89  (assume @p38 (forall @t127 (=> (=> (not @t126) @t116) @t125)))
% 0.48/0.89  (assume @p39 (forall @t69 (= (_ @t128 @t64) @t68)))
% 0.48/0.89  (assume @p40 (forall @t63 (= (_ @t129 @t58) @t62)))
% 0.48/0.89  (assume @p41 (forall @t57 (= (_ @t49 @t56) @t56)))
% 0.48/0.89  (assume @p42 (forall @t53 (= (_ @t48 @t52) @t52)))
% 0.48/0.89  (assume @p43 (forall @t69 (= (_ @t67 @t68) @t68)))
% 0.48/0.89  (assume @p44 (forall @t63 (= (_ @t61 @t62) @t62)))
% 0.48/0.89  (assume @p45 (forall @t47 (= (_ @t49 @t45) @t45)))
% 0.48/0.89  (assume @p46 (forall @t44 (= (_ @t48 @t42) @t42)))
% 0.48/0.89  (assume @p47 (forall @t70 (= (_ @t67 @t65) @t65)))
% 0.48/0.89  (assume @p48 (forall @t71 (= (_ @t61 @t59) @t59)))
% 0.48/0.89  (assume @p49 (forall @t133 (=> (=> (not @t132) @t131) @t130)))
% 0.48/0.89  (assume @p50 (forall @t137 (=> (=> (not @t136) @t135) @t134)))
% 0.48/0.89  (assume @p51 (forall @t139 (_ @t106 @t138)))
% 0.48/0.89  (assume @p52 (forall @t141 (_ @t113 @t140)))
% 0.48/0.89  (assume @p53 (= tptp.bot_bot_set_variable (_ tptp.collect_variable tptp.bot_bot_variable_o)))
% 0.48/0.89  (assume @p54 (= tptp.bot_bo721182586e_real (_ tptp.collec633296133e_real tptp.bot_bo1661475211real_o)))
% 0.48/0.89  (assume @p55 (forall @t90 (= (exists @t75 @t89) @t142)))
% 0.48/0.89  (assume @p56 (forall @t93 (= (exists @t82 @t92) @t143)))
% 0.48/0.89  (assume @p57 (forall @t90 (=> (forall (@list @t144) (not @t145)) @t40)))
% 0.48/0.89  (assume @p58 (forall @t93 (=> (forall (@list @t146) (not @t147)) @t37)))
% 0.48/0.89  (assume @p59 (forall (@list @t30 @t20) (=> @t40 @t148)))
% 0.48/0.89  (assume @p60 (forall (@list @t33 @t27) (=> @t37 @t149)))
% 0.48/0.89  (assume @p61 (forall @t139 (not (_ @t106 tptp.bot_bot_set_variable))))
% 0.48/0.89  (assume @p62 (forall @t141 (not (_ @t113 tptp.bot_bo721182586e_real))))
% 0.48/0.89  (assume @p63 (forall @t152 (=> @t107 (exists @t151 (and (= @t30 (_ @t21 @t150)) (not (_ @t106 @t150)))))))
% 0.48/0.89  (assume @p64 (forall @t155 (=> @t114 (exists @t154 (and (= @t33 (_ @t28 @t153)) (not (_ @t113 @t153)))))))
% 0.48/0.89  (assume @p65 (forall (@list @t98 @t156 @t30) (= (_ @t99 (_ @t157 @t30)) (_ @t157 @t100))))
% 0.48/0.89  (assume @p66 (forall (@list @t102 @t158 @t33) (= (_ @t103 (_ @t159 @t33)) (_ @t159 @t104))))
% 0.48/0.89  (assume @p67 (forall (@list @t20 @t30 @t108 @t17) (=> @t148 (=> (not (_ @t161 @t17)) (= (= @t164 @t120) (and (=> @t109 @t163) (=> @t162 (exists (@list @t160) (and (= @t30 (_ @t110 @t160)) (not (_ @t161 @t160)) (= @t17 (_ @t21 @t160)) (not (_ @t106 @t160)))))))))))
% 0.48/0.89  (assume @p68 (forall (@list @t27 @t33 @t115 @t24) (=> @t149 (=> (not (_ @t166 @t24)) (= (= @t169 @t124) (and (=> @t116 @t168) (=> @t167 (exists (@list @t165) (and (= @t33 (_ @t117 @t165)) (not (_ @t166 @t165)) (= @t24 (_ @t28 @t165)) (not (_ @t113 @t165)))))))))))
% 0.48/0.89  (assume @p69 (forall @t152 (=> @t107 (= @t164 @t30))))
% 0.48/0.89  (assume @p70 (forall @t155 (=> @t114 (= @t169 @t33))))
% 0.48/0.89  (assume @p71 (forall @t174 (=> @t173 (=> @t171 (= (= @t100 (_ @t99 @t17)) @t163)))))
% 0.48/0.89  (assume @p72 (forall @t179 (=> @t178 (=> @t176 (= (= @t104 (_ @t103 @t24)) @t168)))))
% 0.48/0.89  (assume @p73 (forall @t101 (=> @t172 (not (forall @t151 (=> (= @t30 (_ @t99 @t150)) (_ @t170 @t150)))))))
% 0.48/0.89  (assume @p74 (forall @t105 (=> @t177 (not (forall @t154 (=> (= @t33 (_ @t103 @t153)) (_ @t175 @t153)))))))
% 0.48/0.89  (assume @p75 (forall @t123 (=> @t122 @t121)))
% 0.48/0.89  (assume @p76 (forall @t127 (=> @t126 @t125)))
% 0.48/0.89  (assume @p77 (forall (@list @t20 @t17) (_ @t106 @t22)))
% 0.48/0.89  (assume @p78 (forall (@list @t27 @t24) (_ @t113 @t29)))
% 0.48/0.89  (assume @p79 (forall @t112 (=> @t111 (=> @t162 @t107))))
% 0.48/0.89  (assume @p80 (forall @t119 (=> @t118 (=> @t167 @t114))))
% 0.48/0.89  (assume @p81 (forall @t183 (= @t182 (_ @t181 (_ @t49 @t180)))))
% 0.48/0.89  (assume @p82 (forall @t187 (= @t186 (_ @t185 (_ @t48 @t184)))))
% 0.48/0.89  (assume @p83 (forall (@list @t64 @t65 @t188) (= (_ @t189 (_ @t67 @t188)) @t191)))
% 0.48/0.89  (assume @p84 (forall (@list @t58 @t59 @t192) (= (_ @t193 (_ @t61 @t192)) @t194)))
% 0.48/0.89  (assume @p85 (= tptp.sup_sup_set_variable (lambda (@list @t195 @t196) (_ (_ tptp.sup_sup_set_variable @t196) @t195))))
% 0.48/0.89  (assume @p86 (= tptp.sup_su1685293586e_real (lambda (@list @t197 @t198) (_ (_ tptp.sup_su1685293586e_real @t198) @t197))))
% 0.48/0.89  (assume @p87 (forall (@list @t20 @t73) (= (_ @t106 @t77) @t199)))
% 0.48/0.89  (assume @p88 (forall (@list @t27 @t80) (= (_ @t113 @t84) @t200)))
% 0.48/0.89  (assume @p89 (forall @t90 (= (_ tptp.collect_variable (lambda @t75 @t89)) @t30)))
% 0.48/0.89  (assume @p90 (forall @t93 (= (_ tptp.collec633296133e_real (lambda @t82 @t92)) @t33)))
% 0.48/0.89  (assume @p91 (= tptp.sup_sup_set_variable (lambda (@list @t201 @t202) (_ (_ tptp.sup_sup_set_variable @t202) @t201))))
% 0.48/0.89  (assume @p92 (= tptp.sup_su1685293586e_real (lambda (@list @t203 @t204) (_ (_ tptp.sup_su1685293586e_real @t204) @t203))))
% 0.48/0.89  (assume @p93 (forall @t183 (= (_ (_ tptp.sup_sup_set_variable @t56) @t180) @t182)))
% 0.48/0.89  (assume @p94 (forall @t187 (= (_ (_ tptp.sup_su1685293586e_real @t52) @t184) @t186)))
% 0.48/0.89  (assume @p95 (forall @t205 (= (_ @t128 @t188) @t191)))
% 0.48/0.89  (assume @p96 (forall (@list @t59 @t58 @t192) (= (_ @t129 @t192) @t194)))
% 0.48/0.89  (assume @p97 (forall (@list @t17 @t206 @t64 @t65) (=> (= @t17 (_ @t207 @t64)) (= (_ @t67 @t17) @t208))))
% 0.48/0.89  (assume @p98 (forall (@list @t24 @t209 @t58 @t59) (=> (= @t24 (_ @t210 @t58)) (= (_ @t61 @t24) @t211))))
% 0.48/0.89  (assume @p99 (forall (@list @t30 @t206 @t65 @t64) (=> (= @t30 (_ @t207 @t65)) (= (_ @t31 @t64) @t208))))
% 0.48/0.89  (assume @p100 (forall (@list @t33 @t209 @t59 @t58) (=> (= @t33 (_ @t210 @t59)) (= (_ @t34 @t58) @t211))))
% 0.48/0.89  (assume @p101 (forall @t213 (= @t212 (_ @t18 (_ @t31 @t16)))))
% 0.48/0.89  (assume @p102 (forall @t215 (= @t214 (_ @t25 (_ @t34 @t23)))))
% 0.48/0.89  (assume @p103 (forall @t41 (= (_ @t31 @t32) @t32)))
% 0.48/0.89  (assume @p104 (forall @t38 (= (_ @t34 @t35) @t35)))
% 0.48/0.89  (assume @p105 @t219)
% 0.48/0.89  (assume @p106 (= tptp.sup_su1685293586e_real (lambda (@list @t220 @t221) (_ (_ tptp.sup_su1685293586e_real @t221) @t220))))
% 0.48/0.89  (assume @p107 (forall @t90 (= (_ @t31 @t30) @t30)))
% 0.48/0.89  (assume @p108 (forall @t93 (= (_ @t34 @t33) @t33)))
% 0.48/0.89  (assume @p109 (forall @t213 (= (_ (_ tptp.sup_sup_set_variable @t32) @t16) @t212)))
% 0.48/0.89  (assume @p110 (forall @t215 (= (_ (_ tptp.sup_su1685293586e_real @t35) @t23) @t214)))
% 0.48/0.89  (assume @p111 (forall @t225 (= (forall @t75 (=> @t224 @t74)) (and (forall @t75 (=> @t89 @t74)) @t223))))
% 0.48/0.89  (assume @p112 (forall @t229 (= (forall @t82 (=> @t228 @t81)) (and (forall @t82 (=> @t92 @t81)) @t227))))
% 0.48/0.89  (assume @p113 (forall @t225 (= (exists @t75 (and @t224 @t74)) (or (exists @t75 (and @t89 @t74)) (exists @t75 (and @t222 @t74))))))
% 0.48/0.89  (assume @p114 (forall @t229 (= (exists @t82 (and @t228 @t81)) (or (exists @t82 (and @t92 @t81)) (exists @t82 (and @t226 @t81))))))
% 0.48/0.89  (assume @p115 (forall @t133 (=> @t132 @t130)))
% 0.48/0.89  (assume @p116 (forall @t137 (=> @t136 @t134)))
% 0.48/0.89  (assume @p117 (forall @t230 (=> @t131 @t130)))
% 0.48/0.89  (assume @p118 (forall @t231 (=> @t135 @t134)))
% 0.48/0.89  (assume @p119 (forall @t230 (=> @t130 (=> @t232 @t132))))
% 0.48/0.89  (assume @p120 (forall @t231 (=> @t134 (=> @t233 @t136))))
% 0.48/0.89  (assume @p121 (forall (@list @t235 @t12 @t234) (=> @t238 @t236)))
% 0.48/0.89  (assume @p122 (forall @t240 (_ (_ @t13 @t12) @t239)))
% 0.48/0.89  (assume @p123 (= tptp.denota1419872369iation (lambda (@list @t242 @t243 @t241) (_ (_ (_ tptp.denota1419872369iation @t243) @t242) @t241))))
% 0.48/0.89  (assume @p124 (forall (@list @t20 @t108) (=> (= @t138 @t244) @t109)))
% 0.48/0.89  (assume @p125 (forall (@list @t27 @t115) (=> (= @t140 @t245) @t116)))
% 0.48/0.89  (assume @p126 (forall @t152 (not (= @t164 tptp.bot_bot_set_variable))))
% 0.48/0.89  (assume @p127 (forall @t155 (not (= @t169 tptp.bot_bo721182586e_real))))
% 0.48/0.89  (assume @p128 (forall (@list @t20 @t108 @t94 @t246) (= (= (_ @t21 @t244) (_ (_ tptp.insert_variable @t94) (_ (_ tptp.insert_variable @t246) tptp.bot_bot_set_variable))) (or (and (= @t20 @t94) (= @t108 @t246)) (and (= @t20 @t246) (= @t108 @t94))))))
% 0.48/0.89  (assume @p129 (forall (@list @t27 @t115 @t96 @t247) (= (= (_ @t28 @t245) (_ (_ tptp.insert_variable_real @t96) (_ (_ tptp.insert_variable_real @t247) tptp.bot_bo721182586e_real))) (or (and (= @t27 @t96) (= @t115 @t247)) (and (= @t27 @t247) (= @t115 @t96))))))
% 0.48/0.89  (assume @p130 (forall @t250 (= @t249 @t248)))
% 0.48/0.89  (assume @p131 (forall @t253 (= @t252 @t251)))
% 0.48/0.89  (assume @p132 (forall @t250 (=> @t249 @t248)))
% 0.48/0.89  (assume @p133 (forall @t253 (=> @t252 @t251)))
% 0.48/0.89  (assume @p134 (forall @t90 (= (_ @t31 tptp.bot_bot_set_variable) @t30)))
% 0.48/0.89  (assume @p135 (forall @t93 (= (_ @t34 tptp.bot_bo721182586e_real) @t33)))
% 0.48/0.89  (assume @p136 (forall (@list @t17) (= (_ @t46 @t17) @t17)))
% 0.48/0.89  (assume @p137 (forall (@list @t24) (= (_ @t43 @t24) @t24)))
% 0.48/0.89  (assume @p138 (forall (@list @t235 @t12 @t234 @t255 @t239) (=> @t238 (=> (_ (_ @t13 @t255) @t239) (_ (_ @t237 @t255) (_ @t254 @t239))))))
% 0.48/0.89  (assume @p139 (forall @t174 (= (= @t256 @t32) @t259)))
% 0.48/0.89  (assume @p140 (forall @t179 (= (= @t260 @t35) @t263)))
% 0.48/0.89  (assume @p141 (forall (@list @t30 @t17 @t98) (= (= @t32 @t256) @t259)))
% 0.48/0.89  (assume @p142 (forall (@list @t33 @t24 @t102) (= (= @t35 @t260) @t263)))
% 0.48/0.89  (assume @p143 (= tptp.insert_variable (lambda (@list @t264 @t241) (_ (_ tptp.sup_sup_set_variable (_ (_ tptp.insert_variable @t264) tptp.bot_bot_set_variable)) @t241))))
% 0.48/0.89  (assume @p144 (= tptp.insert_variable_real (lambda (@list @t266 @t265) (_ (_ tptp.sup_su1685293586e_real (_ (_ tptp.insert_variable_real @t266) tptp.bot_bo721182586e_real)) @t265))))
% 0.48/0.89  (assume @p145 (not (forall (@list @t273) (not (forall @t281 (= @t280 (and (_ (_ (_ tptp.denota1419872369iation @t274) @t278) @t277) (not (= (_ @t276 @t274) (_ @t275 @t274))))))))))
% 0.48/0.89  (assume @p146 (forall (@list @t285 @t235 @t234 @t289 @t282 @t288 @t284) (=> (_ (_ (_ tptp.denota1419872369iation @t292) @t235) @t234) (=> @t291 (_ (_ @t287 @t235) (_ @t254 @t283))))))
% 0.48/0.89  (assume @p147 (forall @t281 (= @t280 (and (_ (_ (_ tptp.denota1419872369iation @t293) @t278) @t277) (not (= (_ @t276 @t293) (_ @t275 @t293)))))))
% 0.48/0.89  (assume @p148 (forall (@list @t295 @t294) (= (= @t296 (_ tptp.rVar @t294)) (= @t295 @t294))))
% 0.48/0.89  (assume @p149 (= tptp.zero_zero_set_real (_ (_ tptp.insert_real tptp.zero_zero_real) tptp.bot_bot_set_real)))
% 0.48/0.89  (assume @p150 (= tptp.zero_zero_set_nat (_ (_ tptp.insert_nat tptp.zero_zero_nat) tptp.bot_bot_set_nat)))
% 0.48/0.89  (assume @p151 (forall (@list @t298 @t297) (= (= @t299 (_ tptp.dVar @t297)) (= @t298 @t297))))
% 0.48/0.89  (assume @p152 (forall @t230 (= @t130 (or @t131 @t132))))
% 0.48/0.89  (assume @p153 (forall @t231 (= @t134 (or @t135 @t136))))
% 0.48/0.89  (assume @p154 (forall (@list @t20 @t17 @t73) (= (forall @t75 (=> (_ @t88 @t22) @t74)) (and @t199 @t223))))
% 0.48/0.89  (assume @p155 (forall (@list @t27 @t24 @t80) (= (forall @t82 (=> (_ @t91 @t29) @t81)) (and @t200 @t227))))
% 0.48/0.89  (assume @p156 (forall @t300 (= (_ tptp.the_elem_variable @t256) @t98)))
% 0.48/0.89  (assume @p157 (forall @t301 (= (_ tptp.the_el1059226619e_real @t260) @t102)))
% 0.48/0.89  (assume @p158 (forall (@list @t304 @t303 @t307 @t306 @t305 @t302) (or (and (_ (_ (_ tptp.denota1419872369iation @t308) (_ @t304 tptp.zero_zero_real)) (_ (_ tptp.insert_variable (_ tptp.rVar @t303)) (_ (_ tptp.insert_variable (_ tptp.dVar @t303)) tptp.bot_bot_set_variable))) (not (= (_ (_ (_ tptp.denota1863255036rm_sem @t307) @t306) @t308) (_ (_ (_ tptp.denota1863255036rm_sem @t305) @t302) @t308)))) (= (_ (_ (_ (_ tptp.denota1778088425es_ODE @t307) @t304) @t303) @t306) (_ (_ (_ (_ tptp.denota1778088425es_ODE @t305) @t304) @t303) @t302)))))
% 0.48/0.89  (assume @p159 (forall (@list @t309) (= (= tptp.zero_zero_real @t309) (= @t309 tptp.zero_zero_real))))
% 0.48/0.89  (assume @p160 (forall (@list @t310) (= (= tptp.zero_zero_nat @t310) (= @t310 tptp.zero_zero_nat))))
% 0.48/0.89  (assume @p161 (forall @t174 (= (not (_ @t170 @t32)) (and @t173 @t171))))
% 0.48/0.89  (assume @p162 (forall @t179 (= (not (_ @t175 @t35)) (and @t178 @t176))))
% 0.48/0.89  (assume @p163 (forall (@list @t285 @t282 @t289 @t288 @t312 @t311) (=> (forall (@list @t313) (=> (_ (_ (_ tptp.denota1419872369iation @t313) @t292) @t283) (= (_ @t315 @t313) (_ (_ (_ tptp.denota1863255036rm_sem @t312) @t311) @t313)))) (= @t291 (_ (_ (_ (_ tptp.denota1778088425es_ODE @t312) @t285) @t282) @t311)))))
% 0.48/0.89  (assume @p164 (forall (@list @t295 @t298) (not (= @t296 @t299))))
% 0.48/0.89  (assume @p165 (forall (@list @t73 @t316) (=> (forall @t318 (_ @t73 (_ tptp.rVar @t317))) (=> (forall @t318 (_ @t73 (_ tptp.dVar @t317))) (_ @t73 @t316)))))
% 0.48/0.89  (assume @p166 (forall (@list @t156) (=> (forall (@list @t320) (not (= @t156 (_ tptp.rVar @t320)))) (not (forall (@list @t319) (not (= @t156 (_ tptp.dVar @t319))))))))
% 0.48/0.89  (assume @p167 (forall @t78 (= @t86 (= @t73 tptp.bot_bot_variable_o))))
% 0.48/0.89  (assume @p168 (forall @t85 (= @t87 (= @t80 tptp.bot_bo1661475211real_o))))
% 0.48/0.89  (assume @p169 (forall @t324 (=> (_ (_ (_ @t323 @t285) tptp.x) @t288) @t321)))
% 0.48/0.89  (assume @p170 (forall @t300 (_ tptp.is_sin155454833riable @t256)))
% 0.48/0.89  (assume @p171 (forall @t301 (_ tptp.is_sin524757308e_real @t260)))
% 0.48/0.89  (assume @p172 @t325)
% 0.48/0.89  (assume @p173 (forall @t90 (=> @t142 (=> (forall (@list @t327 @t144) (=> @t329 (=> @t145 (= @t327 @t144)))) @t326))))
% 0.48/0.89  (assume @p174 (forall @t93 (=> @t143 (=> (forall (@list @t331 @t146) (=> @t333 (=> @t147 (= @t331 @t146)))) @t330))))
% 0.48/0.89  (assume @p175 (= tptp.is_sin155454833riable (lambda @t334 (exists @t75 (= @t216 (_ (_ tptp.insert_variable @t72) tptp.bot_bot_set_variable))))))
% 0.48/0.89  (assume @p176 (= tptp.is_sin524757308e_real (lambda @t335 (exists @t82 (= @t220 (_ (_ tptp.insert_variable_real @t79) tptp.bot_bo721182586e_real))))))
% 0.48/0.89  (assume @p177 (forall @t90 (=> @t326 (not (forall @t336 (not (= @t30 (_ (_ tptp.insert_variable @t327) tptp.bot_bot_set_variable))))))))
% 0.48/0.89  (assume @p178 (forall @t93 (=> @t330 (not (forall @t337 (not (= @t33 (_ (_ tptp.insert_variable_real @t331) tptp.bot_bo721182586e_real))))))))
% 0.48/0.89  (assume @p179 (forall @t324 (=> (_ (_ (_ @t339 @t285) tptp.x) (_ tptp.the_trm (_ @t338 @t288))) @t321)))
% 0.48/0.89  (assume @p180 (=> (_ (_ (_ @t339 tptp.f) tptp.x) @t341) @t325))
% 0.48/0.89  (assume @p181 (forall (@list @t12) (=> (_ (_ @t13 @t9) @t8) (= (_ (_ (_ tptp.denota1863255036rm_sem tptp.i) @t341) @t12) (_ (_ (_ tptp.denota1863255036rm_sem (_ @t322 @t9)) tptp.theta) @t12)))))
% 0.48/0.89  (assume @p182 (not (= @t340 tptp.none_trm)))
% 0.48/0.89  (assume @p183 (forall @t342 (= (_ tptp.size_variable @t296) tptp.zero_zero_nat)))
% 0.48/0.89  (assume @p184 (forall (@list @t12 @t235 @t234 @t343 @t288 @t289) (=> @t236 (=> @t348 (= (_ (_ @t314 (_ tptp.the_trm @t347)) @t12) (_ (_ (_ tptp.denota1863255036rm_sem (_ @t344 @t235)) @t288) @t12))))))
% 0.48/0.89  (assume @p185 (forall (@list @t343 @t234 @t288 @t239) (=> @t348 (=> (not (= @t349 tptp.none_trm)) (= @t347 @t349)))))
% 0.48/0.89  (assume @p186 (= tptp.none_trm tptp.none_trm))
% 0.48/0.89  (assume @p187 (forall (@list @t343 @t282 @t288 @t289 @t285) (=> (not (= @t350 tptp.none_trm)) (= (_ @t290 (_ tptp.the_trm @t350)) (_ (_ (_ (_ tptp.denota1778088425es_ODE (_ @t344 @t292)) @t285) @t282) @t288)))))
% 0.48/0.89  (assume @p188 (forall @t351 (= (_ tptp.size_variable @t299) tptp.zero_zero_nat)))
% 0.48/0.89  (assume @p189 (forall (@list @t353 @t352) (=> (= @t356 @t355) (=> (=> @t357 (=> (not @t355) (= @t354 (_ tptp.the_trm @t352)))) (= @t353 @t352)))))
% 0.48/0.89  (assume @p190 (forall @t342 (= (_ tptp.size_size_variable @t296) tptp.zero_zero_nat)))
% 0.48/0.89  (assume @p191 (forall @t351 (= (_ tptp.size_size_variable @t299) tptp.zero_zero_nat)))
% 0.48/0.89  (assume @p192 (forall @t361 (_ (_ @t237 @t360) @t256)))
% 0.48/0.89  (assume @p193 (forall @t367 (= @t366 (or @t365 @t364))))
% 0.48/0.89  (assume @p194 (forall @t372 (= @t371 (or @t370 @t369))))
% 0.48/0.89  (assume @p195 (forall @t377 (= @t376 (or @t375 @t374))))
% 0.48/0.89  (assume @p196 (forall @t367 (= (not @t366) (and (not @t365) (not @t364)))))
% 0.48/0.89  (assume @p197 (forall @t372 (= (not @t371) (and (not @t370) (not @t369)))))
% 0.48/0.89  (assume @p198 (forall @t377 (= (not @t376) (and (not @t375) (not @t374)))))
% 0.48/0.89  (assume @p199 (forall (@list @t235 @t98) (= (_ @t359 @t378) @t235)))
% 0.48/0.89  (assume @p200 (= @t379 tptp.bot_bot_set_variable))
% 0.48/0.89  (assume @p201 (= (_ tptp.these_variable_real tptp.bot_bo1411475018e_real) tptp.bot_bo721182586e_real))
% 0.48/0.89  (assume @p202 (forall (@list @t380) (= (_ tptp.these_trm (_ @t362 @t380)) @t381)))
% 0.48/0.89  (assume @p203 (forall @t385 (= (_ tptp.these_variable (_ (_ tptp.insert1340772453riable @t384) @t382)) (_ @t99 @t383))))
% 0.48/0.89  (assume @p204 (forall @t389 (= (_ tptp.these_variable_real (_ (_ tptp.insert526581936e_real @t388) @t386)) (_ @t103 @t387))))
% 0.48/0.89  (assume @p205 (forall @t392 (= (_ tptp.these_trm (_ (_ tptp.insert_option_trm @t391) @t380)) (_ (_ tptp.insert_trm @t390) @t381))))
% 0.48/0.89  (assume @p206 (forall @t400 (=> @t399 (= @t398 @t397))))
% 0.48/0.89  (assume @p207 (forall @t400 (=> @t399 (= @t397 @t398))))
% 0.48/0.89  (assume @p208 (forall (@list @t235 @t98 @t358 @t393) (= (_ @t396 (_ @t395 @t256)) (and @t401 (_ (_ tptp.member_variable_real @t235) @t393)))))
% 0.48/0.89  (assume @p209 (forall (@list @t403 @t402) (= (= @t404 (_ tptp.some_trm @t402)) (= @t403 @t402))))
% 0.48/0.89  (assume @p210 (forall (@list @t12 @t393 @t239) (= (_ @t405 @t408) @t406)))
% 0.48/0.89  (assume @p211 (forall @t414 (= (not @t413) (exists @t412 @t411))))
% 0.48/0.89  (assume @p212 (forall @t414 (= (forall @t412 (not @t411)) @t413)))
% 0.48/0.89  (assume @p213 (forall (@list @t393 @t12) (= (_ @t407 tptp.bot_bot_set_variable) @t393)))
% 0.48/0.89  (assume @p214 (forall (@list @t393 @t12 @t239 @t415) (= (_ (_ (_ tptp.static_selectlike @t408) @t12) @t415) (_ @t407 @t416))))
% 0.48/0.89  (assume @p215 (forall @t418 (=> @t357 (= @t417 @t353))))
% 0.48/0.89  (assume @p216 (forall @t385 (= (_ @t170 @t383) (_ (_ tptp.member814448204riable @t384) @t382))))
% 0.48/0.89  (assume @p217 (forall @t389 (= (_ @t175 @t387) (_ (_ tptp.member523846807e_real @t388) @t386))))
% 0.48/0.89  (assume @p218 (forall @t392 (= (_ @t419 @t381) (_ (_ tptp.member_option_trm @t391) @t380))))
% 0.48/0.89  (assume @p219 (forall (@list @t393 @t420 @t12 @t239) (= (_ (_ (_ tptp.static_selectlike (_ (_ tptp.sup_su1685293586e_real @t393) @t420)) @t12) @t239) (_ (_ tptp.sup_su1685293586e_real @t408) @t422))))
% 0.48/0.89  (assume @p220 (forall @t423 (not (= tptp.none_trm @t404))))
% 0.48/0.89  (assume @p221 (forall @t423 (= (_ tptp.the_trm @t404) @t403)))
% 0.48/0.89  (assume @p222 (forall (@list @t353 @t403) (=> (= @t353 @t404) @t357)))
% 0.48/0.89  (assume @p223 (forall (@list @t425) (=> @t427 (not (forall (@list @t424) (not (= @t425 (_ tptp.some_trm @t424))))))))
% 0.48/0.89  (assume @p224 (forall (@list @t428 @t353) (=> @t431 (=> (forall @t430 (_ @t428 (_ tptp.some_trm @t429))) (_ @t428 @t353)))))
% 0.48/0.89  (assume @p225 (= (lambda @t442 (exists @t441 @t440)) (lambda @t437 (or @t436 (exists @t435 @t434)))))
% 0.48/0.89  (assume @p226 (= (lambda @t442 (forall @t441 @t440)) (lambda @t437 (and @t436 (forall @t435 @t434)))))
% 0.48/0.89  (assume @p227 (forall (@list @t410 @t443 @t425) (=> (=> @t413 @t444) (=> (=> @t426 @t444) (=> (forall (@list @t446 @t445) (=> (= @t410 (_ tptp.some_trm @t446)) (=> (= @t425 (_ tptp.some_trm @t445)) @t444))) @t444)))))
% 0.48/0.89  (assume @p228 (forall (@list @t449 @t448 @t447) (=> (forall (@list @t317 @t451) (_ @t450 @t452)) (=> (forall @t318 (_ @t450 tptp.none_trm)) (_ (_ @t449 @t448) @t447)))))
% 0.48/0.89  (assume @p229 (forall (@list @t454) (= (not @t455) (exists (@list @t453) (= @t454 (_ tptp.some_trm @t453))))))
% 0.48/0.89  (assume @p230 (forall (@list @t443 @t456 @t447) (=> (forall (@list @t451 @t461) (_ (_ @t443 @t452) @t462)) (=> (forall (@list @t460) (_ (_ @t443 tptp.none_trm) @t460)) (=> (forall @t459 (_ (_ @t443 @t458) tptp.none_trm)) (_ (_ @t443 @t456) @t447))))))
% 0.48/0.89  (assume @p231 (forall (@list @t464 @t463 @t447) (=> (forall (@list @t327 @t451) (_ @t465 @t452)) (=> (forall @t336 (_ @t465 tptp.none_trm)) (_ (_ @t464 @t463) @t447)))))
% 0.48/0.89  (assume @p232 (forall @t414 (=> (forall @t467 (not @t466)) @t413)))
% 0.48/0.89  (assume @p233 (forall (@list @t428 @t456) (=> (forall @t467 (_ @t428 @t452)) (=> @t431 (_ @t428 @t456)))))
% 0.48/0.89  (assume @p234 (forall @t418 (=> @t357 (= @t353 @t417))))
% 0.48/0.89  (assume @p235 (forall @t423 (= @t468 (_ (_ tptp.insert_trm @t403) tptp.bot_bot_set_trm))))
% 0.48/0.89  (assume @p236 (forall @t471 (= @t470 (_ (_ tptp.insert_variable @t469) tptp.bot_bot_set_variable))))
% 0.48/0.89  (assume @p237 (forall @t474 (= @t473 (_ (_ tptp.insert_variable_real @t472) tptp.bot_bo721182586e_real))))
% 0.48/0.89  (assume @p238 (forall @t361 (= (_ @t476 @t256) @t401)))
% 0.48/0.89  (assume @p239 (forall (@list @t98 @t477) (= (_ @t170 @t478) (= @t477 @t384))))
% 0.48/0.89  (assume @p240 (forall (@list @t102 @t479) (= (_ @t175 @t480) (= @t479 @t388))))
% 0.48/0.89  (assume @p241 (forall (@list @t390 @t481) (= (_ @t419 @t482) (= @t481 @t391))))
% 0.48/0.89  (assume @p242 (forall @t488 (= (and @t487 @t486) @t485)))
% 0.48/0.89  (assume @p243 (forall (@list @t481) (= (= @t482 tptp.bot_bot_set_trm) (= @t481 tptp.none_trm))))
% 0.48/0.89  (assume @p244 (forall (@list @t477) (= (= @t478 tptp.bot_bot_set_variable) (= @t477 tptp.none_variable))))
% 0.48/0.89  (assume @p245 (forall (@list @t479) (= (= @t480 tptp.bot_bo721182586e_real) (= @t479 tptp.none_variable_real))))
% 0.48/0.89  (assume @p246 (forall @t491 (=> @t490 (= (_ @t405 @t489) @t406))))
% 0.48/0.89  (assume @p247 (forall @t491 (=> @t490 (= @t408 @t489))))
% 0.48/0.89  (assume @p248 (= tptp.some_trm tptp.some_trm))
% 0.48/0.89  (assume @p249 (forall @t471 (_ (_ tptp.member_variable @t469) @t470)))
% 0.48/0.89  (assume @p250 (forall @t474 (_ (_ tptp.member_variable_real @t472) @t473)))
% 0.48/0.89  (assume @p251 (forall @t423 (_ (_ tptp.member_trm @t403) @t468)))
% 0.48/0.89  (assume @p252 (forall (@list @t492 @t493) (=> (_ (_ tptp.member_variable @t492) @t494) (= @t493 (_ tptp.some_variable @t492)))))
% 0.48/0.89  (assume @p253 (forall (@list @t495 @t496) (=> (_ (_ tptp.member_variable_real @t495) @t497) (= @t496 (_ tptp.some_variable_real @t495)))))
% 0.48/0.89  (assume @p254 (forall (@list @t498 @t499) (=> (_ (_ tptp.member_trm @t498) @t500) (= @t499 (_ tptp.some_trm @t498)))))
% 0.48/0.89  (assume @p255 (forall (@list @t502 @t501 @t390) (=> (forall @t430 (=> (_ (_ tptp.member_trm @t429) (_ tptp.set_option_trm2 @t502)) (_ @t501 @t429))) (=> (= @t502 @t391) (_ @t501 @t390)))))
% 0.48/0.89  (assume @p256 (forall @t488 (=> @t487 (=> @t486 @t485))))
% 0.48/0.89  (assume @p257 (= tptp.denotational_Vagree (lambda (@list @t243 @t503 @t241) (_ (_ (_ tptp.denotational_Vagree @t503) @t243) @t241))))
% 0.48/0.89  (assume @p258 (forall @t240 (_ (_ @t483 @t12) @t239)))
% 0.48/0.89  (assume @p259 (forall @t504 (=> @t487 (_ (_ (_ tptp.denotational_Vagree @t11) @t12) @t239))))
% 0.48/0.89  (assume @p260 (forall @t15 (_ @t484 tptp.bot_bot_set_variable)))
% 0.48/0.89  (assume @p261 (= (_ tptp.set_option_trm2 tptp.none_trm) tptp.bot_bot_set_trm))
% 0.48/0.89  (assume @p262 (= (_ tptp.set_option_variable2 tptp.none_variable) tptp.bot_bot_set_variable))
% 0.48/0.89  (assume @p263 (= (_ tptp.set_op697949218e_real tptp.none_variable_real) tptp.bot_bo721182586e_real))
% 0.48/0.89  (assume @p264 (forall (@list @t493) (=> (not (= @t493 tptp.none_variable)) (_ (_ tptp.member_variable (_ tptp.the_variable @t493)) @t494))))
% 0.48/0.89  (assume @p265 (forall (@list @t496) (=> (not (= @t496 tptp.none_variable_real)) (_ (_ tptp.member_variable_real (_ tptp.the_variable_real @t496)) @t497))))
% 0.48/0.89  (assume @p266 (forall (@list @t499) (=> (not (= @t499 tptp.none_trm)) (_ (_ tptp.member_trm (_ tptp.the_trm @t499)) @t500))))
% 0.48/0.89  (assume @p267 (forall (@list @t289 @t285 @t282 @t288 @t284) (=> @t291 (_ (_ (_ tptp.denotational_Vagree @t286) @t292) (_ tptp.uminus1851247844riable @t283)))))
% 0.48/0.89  (assume @p268 (forall @t361 (_ @t476 (_ tptp.uminus1851247844riable @t256))))
% 0.48/0.89  (assume @p269 (forall (@list @t505) (= (_ (_ tptp.uSubst918876924Timeso (_ tptp.some_trm @t505)) tptp.none_trm) tptp.none_trm)))
% 0.48/0.89  (assume @p270 (forall @t57 (= (= @t507 @t506) (= @t45 @t54))))
% 0.48/0.89  (assume @p271 (forall @t53 (= (= @t509 @t508) (= @t42 @t50))))
% 0.48/0.89  (assume @p272 (forall @t47 (= (_ tptp.uminus1851247844riable @t507) @t45)))
% 0.48/0.89  (assume @p273 (forall @t44 (= (_ tptp.uminus430703407e_real @t509) @t42)))
% 0.48/0.89  (assume @p274 (forall @t41 (= (= @t510 (_ tptp.uminus1851247844riable @t17)) @t163)))
% 0.48/0.89  (assume @p275 (forall @t38 (= (= @t511 (_ tptp.uminus430703407e_real @t24)) @t168)))
% 0.48/0.89  (assume @p276 (forall @t513 (= @t512 @t232)))
% 0.48/0.89  (assume @p277 (forall @t515 (= @t514 @t233)))
% 0.48/0.89  (assume @p278 (forall @t513 (=> @t232 @t512)))
% 0.48/0.89  (assume @p279 (forall @t515 (=> @t233 @t514)))
% 0.48/0.89  (assume @p280 (= (_ tptp.uminus_uminus_real tptp.zero_zero_real) tptp.zero_zero_real))
% 0.48/0.89  (assume @p281 (forall @t518 (= (= tptp.zero_zero_real @t517) (= tptp.zero_zero_real @t516))))
% 0.48/0.89  (assume @p282 (forall @t518 (= (= @t517 tptp.zero_zero_real) @t519)))
% 0.48/0.89  (assume @p283 (forall @t518 (= (= @t516 @t517) @t519)))
% 0.48/0.89  (assume @p284 (forall @t518 (= (= @t517 @t516) @t519)))
% 0.48/0.89  (assume @p285 (forall @t504 (= (_ @t14 @t520) @t487)))
% 0.48/0.89  (assume @p286 (forall @t90 (= (_ tptp.uminus1851247844riable @t510) @t30)))
% 0.48/0.89  (assume @p287 (forall @t93 (= (_ tptp.uminus430703407e_real @t511) @t33)))
% 0.48/0.89  (assume @p288 (forall @t513 (=> @t512 @t232)))
% 0.48/0.89  (assume @p289 (forall @t515 (=> @t514 @t233)))
% 0.48/0.89  (assume @p290 (forall (@list @t521) (= (_ (_ tptp.uSubst918876924Timeso tptp.none_trm) @t521) tptp.none_trm)))
% 0.48/0.89  (assume @p291 (forall (@list @t454 @t521) (= (= (_ (_ tptp.uSubst918876924Timeso @t454) @t521) tptp.none_trm) (or @t455 (= @t521 tptp.none_trm)))))
% 0.48/0.89  (assume @p292 (forall @t528 (=> (forall @t527 (=> (_ @t526 @t239) @t525)) @t522)))
% 0.48/0.89  (assume @p293 (forall @t528 (=> (forall @t527 (=> (_ @t526 @t520) @t525)) @t529)))
% 0.48/0.89  (assume @p294 (forall @t535 (= @t522 (forall @t534 (=> (_ @t533 @t239) @t532)))))
% 0.48/0.89  (assume @p295 (forall @t535 (= @t529 (forall @t534 (=> (_ @t533 @t520) @t532)))))
% 0.48/0.89  (assume @p296 (forall (@list @t541 @t540 @t538 @t536) (_ (_ (_ tptp.denotational_Vagree (_ @t542 @t538)) (_ @t542 @t539)) (_ tptp.uminus1851247844riable (_ @t537 tptp.bot_bot_set_variable)))))
% 0.48/0.89  (assume @p297 (forall (@list @t410 @t543 @t425) (=> (= (_ (_ tptp.uSubst918876924Timeso @t410) @t543) @t425) (=> (forall @t467 (=> @t466 (forall (@list @t461) (=> (= @t543 @t462) (not (= @t425 (_ tptp.some_trm (_ (_ tptp.times @t451) @t461)))))))) (=> (=> @t413 @t427) (not (=> (exists @t459 (= @t410 @t458)) (=> (= @t543 tptp.none_trm) @t427))))))))
% 0.48/0.89  (assume @p298 (forall (@list @t547 @t545 @t546 @t544) (= (= (_ (_ tptp.times @t547) @t545) (_ (_ tptp.times @t546) @t544)) (and (= @t547 @t546) (= @t545 @t544)))))
% 0.48/0.89  (assume @p299 (forall @t553 (=> @t552 (= @t551 @t548))))
% 0.48/0.89  (assume @p300 (forall @t553 (=> (not @t552) (= @t551 @t378))))
% 0.48/0.89  (assume @p301 (forall (@list @t393 @t12 @t239) (= (_ (_ (_ tptp.static_selectlike (_ tptp.uminus430703407e_real @t408)) @t12) @t239) (_ (_ (_ tptp.static_selectlike (_ tptp.uminus430703407e_real @t393)) @t12) @t239))))
% 0.48/0.89  (assume @p302 (forall @t554 (= (_ @t549 tptp.bot_bot_set_variable) @t235)))
% 0.48/0.89  (assume @p303 (forall (@list @t12 @t235 @t538) (_ (_ (_ tptp.denotational_Vagree @t550) @t12) @t538)))
% 0.48/0.89  (assume @p304 (forall @t558 (=> (not (= @t557 tptp.none_trm)) (and @t348 (not (= @t555 tptp.none_trm))))))
% 0.48/0.89  (assume @p305 (forall @t558 (= @t557 (_ (_ tptp.uSubst918876924Timeso @t347) @t555))))
% 0.48/0.89  (assume @p306 (forall (@list @t288 @t311) (= (_ (_ tptp.uSubst918876924Timeso (_ tptp.some_trm @t288)) (_ tptp.some_trm @t311)) (_ tptp.some_trm @t556))))
% 0.48/0.89  (assume @p307 (forall @t554 (= (_ @t549 @t559) @t12)))
% 0.48/0.89  (assume @p308 (forall (@list @t536 @t562 @t289 @t235 @t560 @t538) (=> (not (_ (_ tptp.member_variable @t536) (_ tptp.static_FVT @t562))) (= (_ @t563 (_ @t561 @t538)) (_ @t563 (_ @t561 @t539))))))
% 0.48/0.89  (assume @p309 (forall (@list @t98 @t12 @t235) (=> (not (_ @t170 @t559)) (= @t548 @t378))))
% 0.48/0.89  (assume @p310 (forall (@list @t235 @t560 @t288 @t289) (=> (_ @t566 @t565) @t564)))
% 0.48/0.89  (assume @p311 (forall (@list @t235 @t560 @t234 @t288 @t289) (=> (_ (_ @t237 @t560) @t234) (=> (= (_ (_ tptp.inf_inf_set_variable @t565) @t234) tptp.bot_bot_set_variable) @t564))))
% 0.48/0.89  (assume @p312 (forall (@list @t235 @t560 @t538) (=> (_ @t566 @t538) (_ (_ tptp.ord_le282106107riable (_ (_ tptp.statediff @t235) @t560)) (_ tptp.uminus1851247844riable @t538)))))
% 0.48/0.89  (assume @p313 (forall @t47 (_ @t567 @t45)))
% 0.48/0.89  (assume @p314 (forall @t38 (=> (forall @t337 (=> @t333 (_ @t332 @t24))) (_ (_ tptp.ord_le1113654598e_real @t33) @t24))))
% 0.48/0.89  (assume @p315 (forall @t41 (=> (forall @t336 (=> @t329 (_ @t328 @t17))) @t568)))
% 0.48/0.89  (assume @p316 (forall @t41 (=> @t568 (=> (_ (_ tptp.ord_le282106107riable @t17) @t30) @t163))))
% 0.48/0.89  (assume @p317 (forall @t70 (= (_ @t569 @t65) @t65)))
% 0.48/0.89  (assume @p318 (forall @t47 (= (_ @t570 @t45) @t45)))
% 0.48/0.89  (assume @p319 (forall @t69 (= (_ @t569 @t571) @t571)))
% 0.48/0.89  (assume @p320 (forall @t57 (= (_ @t570 @t572) @t572)))
% 0.48/0.89  (assume @p321 (forall @t69 (= (_ (_ tptp.inf_inf_set_variable @t571) @t64) @t571)))
% 0.48/0.89  (assume @p322 (forall @t57 (= (_ (_ tptp.inf_inf_set_variable @t572) @t54) @t572)))
% 0.48/0.89  (assume @p323 (forall @t231 (=> @t135 (=> @t136 @t573))))
% 0.48/0.89  (assume @p324 (forall @t230 (=> @t131 (=> @t132 @t574))))
% 0.48/0.89  (assume @p325 (forall @t231 (= @t573 (and @t135 @t136))))
% 0.48/0.89  (assume @p326 (forall @t230 (= @t574 (and @t131 @t132))))
% 0.48/0.89  (assume @p327 (forall (@list @t575) (= (_ (_ tptp.ord_less_eq_nat @t575) tptp.zero_zero_nat) (= @t575 tptp.zero_zero_nat))))
% 0.48/0.89  (assume @p328 (forall @t53 (= (_ (_ tptp.ord_le1113654598e_real @t509) @t508) (_ @t576 @t42))))
% 0.48/0.89  (assume @p329 (forall @t57 (= (_ (_ tptp.ord_le282106107riable @t507) @t506) (_ @t577 @t45))))
% 0.48/0.89  (assume @p330 (forall @t183 (= (_ @t567 (_ (_ tptp.inf_inf_set_variable @t54) @t180)) (and (_ @t567 @t54) @t578))))
% 0.48/0.89  (assume @p331 (forall @t205 (= (_ @t579 (_ (_ tptp.inf_inf_set_variable @t64) @t188)) (and (_ @t579 @t64) (_ @t579 @t188)))))
% 0.48/0.89  (assume @p332 (forall @t187 (= (_ (_ tptp.ord_le1113654598e_real @t52) @t184) (and (_ (_ tptp.ord_le1113654598e_real @t42) @t184) (_ @t576 @t184)))))
% 0.48/0.89  (assume @p333 (forall @t183 (= (_ (_ tptp.ord_le282106107riable @t56) @t180) (and @t578 (_ @t577 @t180)))))
% 0.48/0.89  (assume @p334 (forall (@list @t64 @t188 @t65) (= (_ (_ tptp.ord_le282106107riable @t190) @t65) (and (_ (_ tptp.ord_le282106107riable @t64) @t65) (_ (_ tptp.ord_le282106107riable @t188) @t65)))))
% 0.48/0.89  (assume @p335 (forall (@list @t580) (or (= @t580 true) (= @t580 false))))
% 0.48/0.89  (assume @p336 (forall @t582 (= (_ (_ (_ tptp.if_real false) @t309) @t581) @t581)))
% 0.48/0.89  (assume @p337 (forall @t582 (= (_ (_ (_ tptp.if_real true) @t309) @t581) @t309)))
% 0.48/0.89  (assume @p338 @t584)
% 0.48/0.89  (assume @p339 true)
% 0.48/0.89  (step @p340 (= tptp.denota1419872369iation @t596) :rule refl :args (@t596))
% 0.48/0.89  (step @p341 (= tptp.bot_bot_variable_o @t597) :rule refl :args (@t597))
% 0.48/0.89  (step @p342 (= tptp.bot_bo1661475211real_o @t598) :rule refl :args (@t598))
% 0.48/0.89  (step @p343 (= tptp.is_sin155454833riable @t599) :rule refl :args (@t599))
% 0.48/0.89  (step @p344 (= tptp.is_sin524757308e_real @t600) :rule refl :args (@t600))
% 0.48/0.89  (step @p345 (= tptp.is_empty_variable @t601) :rule refl :args (@t601))
% 0.48/0.89  (step @p346 (= tptp.is_emp227886046e_real @t602) :rule refl :args (@t602))
% 0.48/0.89  (step @p347 (= tptp.denotational_repv @t605) :rule refl :args (@t605))
% 0.48/0.89  (step @p348 (= tptp.denotational_Vagree @t607) :rule refl :args (@t607))
% 0.48/0.89  (step @p349 (= tptp.stateinterpol @t609) :rule refl :args (@t609))
% 0.48/0.89  (step @p350 :rule evaluate :args ((= false true)))
% 0.48/0.89  (step @p351 :rule refl :args (@t612))
% 0.48/0.89  (step @p352 :rule refl :args (@t613))
% 0.48/0.89  (step @p353 :rule refl :args (@t379))
% 0.48/0.89  (step @p354 :rule cong :premises (@p353 @p352) :args ((= @t379 @t613)))
% 0.48/0.89  (step @p355 :rule symm :premises (@p354))
% 0.48/0.89  (step @p356 :rule eq_resolve :premises (@p353 @p355))
% 0.48/0.89  (step @p357 :rule refl :args (@t614))
% 0.48/0.89  (step @p358 :rule cong :premises (@p357 @p356) :args (@t615))
% 0.48/0.89  (step @p359 :rule refl :args (@t616))
% 0.48/0.89  (step @p360 :rule cong :premises (@p359 @p358) :args (@t617))
% 0.48/0.89  (step @p361 :rule refl :args (tptp.u))
% 0.48/0.89  (step @p362 :rule cong :premises (@p361 @p360) :args (@t618))
% 0.48/0.89  (step @p363 :rule refl :args (@t585))
% 0.48/0.89  (step @p364 :rule cong :premises (@p363 @p362) :args (@t619))
% 0.48/0.89  (step @p365 :rule nary_cong :premises (@p364 @p351) :args (@t620))
% 0.48/0.89  (step @p366 :rule cong :premises (@p365) :args ((forall @t593 @t620)))
% 0.48/0.89  (step @p367 :rule refl :args (@t612))
% 0.48/0.89  (step @p368 :rule symm :premises (@p200))
% 0.48/0.89  (step @p369 :rule refl :args (@t614))
% 0.48/0.89  (step @p370 :rule cong :premises (@p369 @p368) :args (@t621))
% 0.48/0.89  (step @p371 :rule refl :args (@t616))
% 0.48/0.89  (step @p372 :rule cong :premises (@p371 @p370) :args (@t622))
% 0.48/0.89  (step @p373 :rule refl :args (tptp.u))
% 0.48/0.89  (step @p374 :rule cong :premises (@p373 @p372) :args (@t623))
% 0.48/0.89  (step @p375 :rule refl :args (@t585))
% 0.48/0.89  (step @p376 :rule cong :premises (@p375 @p374) :args (@t624))
% 0.48/0.89  (step @p377 :rule nary_cong :premises (@p376 @p367) :args (@t625))
% 0.48/0.89  (step @p378 :rule cong :premises (@p377) :args ((forall @t593 @t625)))
% 0.48/0.89  (step @p379 :rule trans :premises (@p378 @p366))
% 0.48/0.89  (step @p380 :rule refl :args ((tptp.sup_sup_set_variable tptp.u @t6)))
% 0.48/0.89  (step @p381 :rule refl :args ((tptp.insert_variable @t4 @t3)))
% 0.48/0.89  (step @p382 :rule refl :args ((tptp.insert_variable @t1 tptp.bot_bot_set_variable)))
% 0.48/0.89  (step @p383 :rule refl :args (tptp.bot_bot_set_variable))
% 0.48/0.89  (step @p384 :rule refl :args (@t614))
% 0.48/0.89  (step @p385 :rule cong :premises (@p384 @p383) :args (@t621))
% 0.48/0.89  (step @p386 :rule trans :premises (@p385 @p382))
% 0.48/0.89  (step @p387 :rule refl :args (@t616))
% 0.48/0.89  (step @p388 :rule cong :premises (@p387 @p386) :args (@t622))
% 0.48/0.89  (step @p389 :rule trans :premises (@p388 @p381))
% 0.48/0.89  (step @p390 :rule cong :premises (@p361 @p389) :args (@t623))
% 0.48/0.89  (step @p391 :rule trans :premises (@p390 @p380))
% 0.48/0.89  (step @p392 :rule refl :args (@t7))
% 0.48/0.89  (step @p393 :rule ho_cong :premises (@p392 @p389))
% 0.48/0.89  (step @p394 :rule cong :premises (@p393 @p391) :args ((= (_ @t7 @t622) @t623)))
% 0.48/0.89  (step @p395 :rule symm :premises (@p394))
% 0.48/0.89  (step @p396 :rule refl :args (@t8))
% 0.48/0.89  (step @p397 :rule eq_resolve :premises (@p396 @p395))
% 0.48/0.89  (step @p398 :rule refl :args (tptp.insert_variable))
% 0.48/0.89  (step @p399 :rule ho_cong :premises (@p398 @p387))
% 0.48/0.89  (step @p400 :rule ho_cong :premises (@p399 @p386))
% 0.48/0.89  (step @p401 :rule cong :premises (@p400 @p389) :args ((= (_ (_ tptp.insert_variable @t616) @t621) @t622)))
% 0.48/0.89  (step @p402 :rule symm :premises (@p401))
% 0.48/0.89  (step @p403 :rule refl :args (@t6))
% 0.48/0.89  (step @p404 :rule eq_resolve :premises (@p403 @p402))
% 0.48/0.89  (step @p405 :rule ho_cong :premises (@p398 @p384))
% 0.48/0.89  (step @p406 :rule ho_cong :premises (@p405 @p383))
% 0.48/0.89  (step @p407 :rule cong :premises (@p406 @p386) :args ((= (_ (_ tptp.insert_variable @t614) tptp.bot_bot_set_variable) @t621)))
% 0.48/0.89  (step @p408 :rule symm :premises (@p407))
% 0.48/0.89  (step @p409 :rule refl :args (@t3))
% 0.48/0.89  (step @p410 :rule eq_resolve :premises (@p409 @p408))
% 0.48/0.89  (step @p411 :rule refl :args (@t1))
% 0.48/0.89  (step @p412 :rule cong :premises (@p411 @p384) :args ((= @t1 @t614)))
% 0.48/0.89  (step @p413 :rule symm :premises (@p412))
% 0.48/0.89  (step @p414 :rule eq_resolve :premises (@p411 @p413))
% 0.48/0.89  (step @p415 :rule ho_cong :premises (@p398 @p414))
% 0.48/0.89  (step @p416 :rule ho_cong :premises (@p415 @p383))
% 0.48/0.89  (step @p417 :rule trans :premises (@p416 @p410))
% 0.48/0.89  (step @p418 :rule refl :args (@t4))
% 0.48/0.89  (step @p419 :rule cong :premises (@p418 @p387) :args ((= @t4 @t616)))
% 0.48/0.89  (step @p420 :rule symm :premises (@p419))
% 0.48/0.89  (step @p421 :rule eq_resolve :premises (@p418 @p420))
% 0.48/0.89  (step @p422 :rule ho_cong :premises (@p398 @p421))
% 0.48/0.89  (step @p423 :rule ho_cong :premises (@p422 @p417))
% 0.48/0.89  (step @p424 :rule trans :premises (@p423 @p404))
% 0.48/0.89  (step @p425 :rule ho_cong :premises (@p392 @p424))
% 0.48/0.89  (step @p426 :rule trans :premises (@p425 @p397))
% 0.48/0.89  (step @p427 :rule cong :premises (@p363 @p426) :args (@t626))
% 0.48/0.89  (step @p428 :rule nary_cong :premises (@p427 @p351) :args (@t627))
% 0.48/0.89  (step @p429 :rule cong :premises (@p428) :args (@t628))
% 0.48/0.89  (step @p430 :rule beta-reduce :args ((= (_ @t631 @t8) @t628)))
% 0.48/0.89  (step @p431 :rule trans :premises (@p430 @p429))
% 0.48/0.89  (step @p432 :rule refl :args (@t8))
% 0.48/0.89  (step @p433 :rule eq-symm :args (@t610 @t611))
% 0.48/0.89  (step @p434 :rule refl :args (@t629))
% 0.48/0.89  (step @p435 :rule nary_cong :premises (@p434 @p433) :args (@t632))
% 0.48/0.89  (step @p436 :rule cong :premises (@p435) :args (@t633))
% 0.48/0.89  (step @p437 :rule cong :premises (@p436) :args (@t634))
% 0.48/0.89  (step @p438 :rule beta-reduce :args ((= (_ (lambda @t636 (forall @t593 (or @t629 (= @t635 @t611)))) tptp.omega) @t634)))
% 0.48/0.89  (step @p439 :rule trans :premises (@p438 @p437))
% 0.48/0.89  (step @p440 :rule refl :args (tptp.omega))
% 0.48/0.89  (step @p441 :rule refl :args (@t611))
% 0.48/0.89  (step @p442 :rule refl :args (@t637))
% 0.48/0.89  (step @p443 :rule cong :premises (@p442 @p441) :args ((= @t637 @t611)))
% 0.48/0.89  (step @p444 :rule symm :premises (@p443))
% 0.48/0.89  (step @p445 :rule eq_resolve :premises (@p442 @p444))
% 0.48/0.89  (step @p446 :rule refl :args (@t635))
% 0.48/0.89  (step @p447 :rule cong :premises (@p446 @p445) :args (@t638))
% 0.48/0.89  (step @p448 :rule refl :args (@t629))
% 0.48/0.89  (step @p449 :rule nary_cong :premises (@p448 @p447) :args (@t639))
% 0.48/0.89  (step @p450 :rule cong :premises (@p449) :args ((forall @t593 @t639)))
% 0.48/0.89  (step @p451 :rule eq-symm :args (@t637 @t635))
% 0.48/0.89  (step @p452 :rule refl :args (@t635))
% 0.48/0.89  (step @p453 :rule refl :args (@t640))
% 0.48/0.89  (step @p454 :rule cong :premises (@p453 @p452) :args (@t641))
% 0.48/0.89  (step @p455 :rule trans :premises (@p454 @p451))
% 0.48/0.89  (step @p456 :rule nary_cong :premises (@p434 @p455) :args (@t642))
% 0.48/0.89  (step @p457 :rule cong :premises (@p456) :args (@t643))
% 0.48/0.89  (step @p458 :rule trans :premises (@p457 @p450))
% 0.48/0.89  (step @p459 :rule cong :premises (@p458) :args (@t644))
% 0.48/0.89  (step @p460 :rule beta-reduce :args ((= @t646 @t644)))
% 0.48/0.89  (step @p461 :rule trans :premises (@p460 @p459))
% 0.48/0.89  (step @p462 :rule ho_cong :premises (@p461 @p440))
% 0.48/0.89  (step @p463 :rule trans :premises (@p462 @p439))
% 0.48/0.89  (step @p464 :rule ho_cong :premises (@p463 @p432))
% 0.48/0.89  (step @p465 :rule trans :premises (@p464 @p431))
% 0.48/0.89  (step @p466 :rule refl :args (@t9))
% 0.48/0.89  (step @p467 :rule refl :args (@t635))
% 0.48/0.89  (step @p468 :rule refl :args (@t586))
% 0.48/0.89  (step @p469 :rule cong :premises (@p468 @p467) :args ((= @t586 @t635)))
% 0.48/0.89  (step @p470 :rule symm :premises (@p469))
% 0.48/0.89  (step @p471 :rule eq_resolve :premises (@p468 @p470))
% 0.48/0.89  (step @p472 :rule refl :args (@t645))
% 0.48/0.89  (step @p473 :rule refl :args (@t587))
% 0.48/0.89  (step @p474 :rule cong :premises (@p473 @p472) :args ((= @t587 @t645)))
% 0.48/0.89  (step @p475 :rule symm :premises (@p474))
% 0.48/0.89  (step @p476 :rule eq_resolve :premises (@p473 @p475))
% 0.48/0.89  (step @p477 :rule cong :premises (@p476 @p471) :args (@t588))
% 0.48/0.89  (step @p478 :rule refl :args (@t629))
% 0.48/0.89  (step @p479 :rule refl :args (@t591))
% 0.48/0.89  (step @p480 :rule cong :premises (@p479 @p478) :args ((= @t591 @t629)))
% 0.48/0.89  (step @p481 :rule symm :premises (@p480))
% 0.48/0.89  (step @p482 :rule eq_resolve :premises (@p479 @p481))
% 0.48/0.89  (step @p483 :rule nary_cong :premises (@p482 @p477) :args (@t647))
% 0.48/0.89  (step @p484 :rule cong :premises (@p483) :args ((forall @t593 @t647)))
% 0.48/0.89  (step @p485 :rule refl :args (@t588))
% 0.48/0.89  (step @p486 :rule bool-double-not-elim :args (@t591))
% 0.48/0.89  (step @p487 :rule nary_cong :premises (@p486 @p485) :args ((or (not @t592) @t588)))
% 0.48/0.89  (step @p488 :rule bool-impl-elim :args (@t592 @t588))
% 0.48/0.89  (step @p489 :rule trans :premises (@p488 @p487))
% 0.48/0.89  (step @p490 :rule cong :premises (@p489) :args (@t594))
% 0.48/0.89  (step @p491 :rule trans :premises (@p490 @p484))
% 0.48/0.89  (step @p492 :rule cong :premises (@p491) :args (@t596))
% 0.48/0.89  (step @p493 :rule trans :premises (@p340 @p492))
% 0.48/0.89  (step @p494 :rule ho_cong :premises (@p493 @p466))
% 0.48/0.89  (step @p495 :rule ho_cong :premises (@p494 @p440))
% 0.48/0.89  (step @p496 :rule ho_cong :premises (@p495 @p432))
% 0.48/0.89  (step @p497 :rule trans :premises (@p496 @p465))
% 0.48/0.89  (step @p498 :rule trans :premises (@p497 @p379))
% 0.48/0.89  (step @p499 :rule eq_resolve :premises (@p1 @p498))
% 0.48/0.89  (step @p500 :rule instantiate :premises (@p499) :args ((@list @t651)))
% 0.48/0.89  (step @p501 :rule cong :premises (@p360 @p361) :args (@t652))
% 0.48/0.89  (step @p502 :rule cong :premises (@p363 @p501) :args (@t653))
% 0.48/0.89  (step @p503 :rule nary_cong :premises (@p502 @p351) :args (@t654))
% 0.48/0.89  (step @p504 :rule cong :premises (@p503) :args (@t655))
% 0.48/0.89  (step @p505 :rule cong :premises (@p504) :args ((not @t655)))
% 0.48/0.89  (step @p506 :rule cong :premises (@p372 @p373) :args (@t656))
% 0.48/0.89  (step @p507 :rule cong :premises (@p375 @p506) :args (@t657))
% 0.48/0.89  (step @p508 :rule nary_cong :premises (@p507 @p367) :args (@t658))
% 0.48/0.89  (step @p509 :rule cong :premises (@p508) :args (@t659))
% 0.48/0.89  (step @p510 :rule cong :premises (@p509) :args ((not @t659)))
% 0.48/0.89  (step @p511 :rule trans :premises (@p510 @p505))
% 0.48/0.89  (step @p512 :rule refl :args ((tptp.sup_sup_set_variable @t6 tptp.u)))
% 0.48/0.89  (step @p513 :rule cong :premises (@p389 @p361) :args (@t656))
% 0.48/0.89  (step @p514 :rule trans :premises (@p513 @p512))
% 0.48/0.89  (step @p515 :rule refl :args (tptp.sup_sup_set_variable))
% 0.48/0.89  (step @p516 :rule ho_cong :premises (@p515 @p389))
% 0.48/0.89  (step @p517 :rule ho_cong :premises (@p516 @p361))
% 0.48/0.89  (step @p518 :rule cong :premises (@p517 @p514) :args ((= (_ (_ tptp.sup_sup_set_variable @t622) tptp.u) @t656)))
% 0.48/0.89  (step @p519 :rule symm :premises (@p518))
% 0.48/0.89  (step @p520 :rule refl :args (@t583))
% 0.48/0.89  (step @p521 :rule eq_resolve :premises (@p520 @p519))
% 0.48/0.89  (step @p522 :rule ho_cong :premises (@p515 @p424))
% 0.48/0.89  (step @p523 :rule ho_cong :premises (@p522 @p361))
% 0.48/0.89  (step @p524 :rule trans :premises (@p523 @p521))
% 0.48/0.89  (step @p525 :rule cong :premises (@p363 @p524) :args (@t660))
% 0.48/0.89  (step @p526 :rule nary_cong :premises (@p525 @p351) :args (@t661))
% 0.48/0.89  (step @p527 :rule cong :premises (@p526) :args (@t662))
% 0.48/0.89  (step @p528 :rule beta-reduce :args ((= (_ @t631 @t583) @t662)))
% 0.48/0.89  (step @p529 :rule trans :premises (@p528 @p527))
% 0.48/0.89  (step @p530 :rule refl :args (@t583))
% 0.48/0.89  (step @p531 :rule ho_cong :premises (@p463 @p530))
% 0.48/0.89  (step @p532 :rule trans :premises (@p531 @p529))
% 0.48/0.89  (step @p533 :rule cong :premises (@p532) :args ((not (_ (_ @t646 tptp.omega) @t583))))
% 0.48/0.89  (step @p534 :rule ho_cong :premises (@p495 @p530))
% 0.48/0.89  (step @p535 :rule cong :premises (@p534) :args (@t584))
% 0.48/0.89  (step @p536 :rule trans :premises (@p535 @p533))
% 0.48/0.89  (step @p537 :rule trans :premises (@p536 @p511))
% 0.48/0.89  (step @p538 :rule eq_resolve :premises (@p338 @p537))
% 0.48/0.89  (step @p539 :rule skolemize :premises (@p538))
% 0.48/0.89  (step @p540 :rule cnf_or_neg :args (@t665 1))
% 0.48/0.89  (step @p541 :rule chain_m_resolution :premises (@p540 @p539) :args ((not @t663) @t666 @t667))
% 0.48/0.89  (step @p542 :rule cnf_or_pos :args (@t670))
% 0.48/0.89  (step @p543 :rule reordering :premises (@p542) :args ((or @t663 @t669 (not @t670))))
% 0.48/0.89  (step @p544 :rule chain_m_resolution :premises (@p543 @p541 @p500) :args (@t669 (@list true false) (@list @t663 @t670)))
% 0.48/0.89  (step @p545 :rule true_intro :premises (@p544))
% 0.48/0.89  (step @p546 :rule eq-refl :args (@t218))
% 0.48/0.89  (step @p547 :rule skolem_intro :args (@t671))
% 0.48/0.89  (step @p548 :rule refl :args (@t218))
% 0.48/0.89  (step @p549 :rule cong :premises (@p548 @p547) :args ((= @t218 @t671)))
% 0.48/0.89  (step @p550 :rule trans :premises (@p549 @p546))
% 0.48/0.89  (step @p551 :rule true_elim :premises (@p550))
% 0.48/0.89  (step @p552 :rule refl :args (tptp.sup_sup_set_variable))
% 0.48/0.89  (step @p553 :rule cong :premises (@p552 @p551) :args (@t219))
% 0.48/0.89  (step @p554 :rule eq_resolve :premises (@p105 @p553))
% 0.48/0.89  (step @p555 :rule eq-symm :args (@t668 @t650))
% 0.48/0.89  (step @p556 :rule refl :args ((tptp.sup_sup_set_variable @t673 tptp.u)))
% 0.48/0.89  (step @p557 :rule refl :args ((tptp.insert_variable @t4 @t672)))
% 0.48/0.89  (step @p558 :rule refl :args ((tptp.insert_variable @t1 @t379)))
% 0.48/0.89  (step @p559 :rule cong :premises (@p384 @p352) :args (@t648))
% 0.48/0.89  (step @p560 :rule trans :premises (@p559 @p558))
% 0.48/0.89  (step @p561 :rule cong :premises (@p387 @p560) :args (@t649))
% 0.48/0.89  (step @p562 :rule trans :premises (@p561 @p557))
% 0.48/0.89  (step @p563 :rule cong :premises (@p562 @p361) :args (@t650))
% 0.48/0.89  (step @p564 :rule trans :premises (@p563 @p556))
% 0.48/0.89  (step @p565 :rule ho_cong :premises (@p515 @p562))
% 0.48/0.89  (step @p566 :rule ho_cong :premises (@p565 @p361))
% 0.48/0.89  (step @p567 :rule cong :premises (@p566 @p564) :args ((= @t674 @t650)))
% 0.48/0.89  (step @p568 :rule symm :premises (@p567))
% 0.48/0.89  (step @p569 :rule refl :args ((_ (_ tptp.sup_sup_set_variable @t673) tptp.u)))
% 0.48/0.89  (step @p570 :rule eq_resolve :premises (@p569 @p568))
% 0.48/0.89  (step @p571 :rule refl :args (@t668))
% 0.48/0.89  (step @p572 :rule cong :premises (@p571 @p570) :args (@t675))
% 0.48/0.89  (step @p573 :rule trans :premises (@p572 @p555))
% 0.48/0.89  (step @p574 :rule refl :args (@t676))
% 0.48/0.89  (step @p575 :rule cong :premises (@p574 @p573) :args (@t677))
% 0.48/0.89  ; WARNING: add trust step for TRUST
% 0.48/0.89  ; trust TRUST THEORY_LEMMA
% 0.48/0.89  (step @p576 :rule trust :premises () :args (@t677))
% 0.48/0.89  (step @p577 :rule eq_resolve :premises (@p576 @p575))
% 0.48/0.89  (step @p578 :rule implies_elim :premises (@p577))
% 0.48/0.89  (step @p579 :rule chain_m_resolution :premises (@p578 @p554) :args ((= @t650 @t668) (@list false) (@list @t676)))
% 0.48/0.89  (step @p580 :rule refl :args (@t651))
% 0.48/0.89  (step @p581 :rule cong :premises (@p580 @p579) :args (@t664))
% 0.48/0.89  (step @p582 :rule cnf_or_neg :args (@t665 0))
% 0.48/0.89  (step @p583 :rule chain_m_resolution :premises (@p582 @p539) :args ((not @t664) @t666 @t667))
% 0.48/0.89  (step @p584 :rule false_intro :premises (@p583))
% 0.48/0.89  (step @p585 :rule symm :premises (@p584))
% 0.48/0.89  (step @p586 :rule trans :premises (@p585 @p581 @p545))
% 0.48/0.89  (step @p587 false :rule eq_resolve :premises (@p586 @p350))
% 0.48/0.89  )
% 0.48/0.89  % SZS output end Proof
% 0.48/0.89  % cvc5 exiting
%------------------------------------------------------------------------------