%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP041^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 : n018.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 08:24:52 AM UTC 2026 % Result : Theorem 0.44s 0.82s % Output : Proof 0.44s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP041^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.18/0.34 % Computer : n018.cluster.edu % 0.18/0.34 % Model : x86_64 x86_64 % 0.18/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.34 % Memory : 8042.1875MB % 0.18/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.34 % CPULimit : 300 % 0.18/0.34 % WCLimit : 300 % 0.18/0.34 % DateTime : Tue Jun 2 04:11:35 EDT 2026 % 0.18/0.34 % CPUTime : % 0.37/0.59 %----Proving TH0 % 0.44/0.82 --- 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.44/0.82 % SZS status Theorem % 0.44/0.82 % SZS output start Proof % 0.44/0.82 ( % 0.44/0.82 (declare-sort tptp.set_Sum_sum_c_c 0) % 0.44/0.82 (declare-sort tptp.finite1398487019real_c 0) % 0.44/0.82 (declare-sort tptp.set_c 0) % 0.44/0.82 (declare-sort tptp.real 0) % 0.44/0.82 (declare-sort tptp.set_real 0) % 0.44/0.82 (declare-sort tptp.set_Fi1407883041real_c 0) % 0.44/0.82 (declare-sort tptp.sum_sum_c_d 0) % 0.44/0.82 (declare-sort tptp.produc190496183real_c 0) % 0.44/0.82 (declare-sort tptp.set_Sum_sum_c_d 0) % 0.44/0.82 (declare-sort tptp.set_Pr1389752855real_c 0) % 0.44/0.82 (declare-sort tptp.sum_sum_c_c 0) % 0.44/0.82 (declare-sort tptp.c 0) % 0.44/0.82 (declare-sort tptp.oDE_a_c 0) % 0.44/0.82 (declare-sort tptp.filter_real 0) % 0.44/0.82 (declare-sort tptp.set_set_Sum_sum_c_c 0) % 0.44/0.82 (declare-sort tptp.hp_a_b_c 0) % 0.44/0.82 (declare-sort tptp.denota231621370t_unit 0) % 0.44/0.82 (declare-sort tptp.set_Su1783761653um_b_c 0) % 0.44/0.82 (declare-sort tptp.formula_a_b_c 0) % 0.44/0.82 (declare-sort tptp.produc754691304um_c_c 0) % 0.44/0.82 (declare-sort tptp.produc957004601l_real 0) % 0.44/0.82 (declare-sort tptp.produc214722967um_c_c 0) % 0.44/0.82 (declare-sort tptp.produc1398711912c_real 0) % 0.44/0.82 (declare-const tptp.member1895684704real_c (-> tptp.produc190496183real_c tptp.set_Pr1389752855real_c Bool)) % 0.44/0.82 (declare-const tptp.member_Sum_sum_c_d (-> tptp.sum_sum_c_d tptp.set_Sum_sum_c_d Bool)) % 0.44/0.82 (declare-const tptp.member_Sum_sum_c_c (-> tptp.sum_sum_c_c tptp.set_Sum_sum_c_c Bool)) % 0.44/0.82 (declare-const tptp.produc394644079real_c (-> tptp.finite1398487019real_c tptp.finite1398487019real_c tptp.produc190496183real_c)) % 0.44/0.82 (declare-const tptp.ord_less_eq_real (-> tptp.real tptp.real Bool)) % 0.44/0.82 (declare-const tptp.denota968303861_a_b_c (-> tptp.denota231621370t_unit tptp.formula_a_b_c tptp.set_Pr1389752855real_c)) % 0.44/0.82 (declare-const tptp.static_FVF_a_b_c (-> tptp.formula_a_b_c tptp.set_Sum_sum_c_c)) % 0.44/0.82 (declare-const tptp.denota1997846518gree_c (-> tptp.produc190496183real_c tptp.produc190496183real_c tptp.set_Sum_sum_c_c Bool)) % 0.44/0.82 (declare-const tptp.static_SIGF_a_b_c (-> tptp.formula_a_b_c tptp.set_Su1783761653um_b_c)) % 0.44/0.82 (declare-const tptp.denota69106024_a_b_c (-> tptp.denota231621370t_unit tptp.denota231621370t_unit tptp.set_Su1783761653um_b_c Bool)) % 0.44/0.82 (declare-const tptp.coinci772602909_a_b_c (-> tptp.hp_a_b_c tptp.denota231621370t_unit Bool)) % 0.44/0.82 (declare-const tptp.coinci354700372_a_b_c (-> tptp.hp_a_b_c tptp.denota231621370t_unit tptp.denota231621370t_unit Bool)) % 0.44/0.82 (declare-const tptp.collec1643251106real_c (-> (-> tptp.produc190496183real_c Bool) tptp.set_Pr1389752855real_c)) % 0.44/0.82 (declare-const tptp.collect_Sum_sum_c_d (-> (-> tptp.sum_sum_c_d Bool) tptp.set_Sum_sum_c_d)) % 0.44/0.82 (declare-const tptp.member1261661570real_c (-> tptp.finite1398487019real_c tptp.set_Fi1407883041real_c Bool)) % 0.44/0.82 (declare-const tptp.collec230941376real_c (-> (-> tptp.finite1398487019real_c Bool) tptp.set_Fi1407883041real_c)) % 0.44/0.82 (declare-const tptp.member_c (-> tptp.c tptp.set_c Bool)) % 0.44/0.82 (declare-const tptp.collect_c (-> (-> tptp.c Bool) tptp.set_c)) % 0.44/0.82 (declare-const tptp.collect_Sum_sum_c_c (-> (-> tptp.sum_sum_c_c Bool) tptp.set_Sum_sum_c_c)) % 0.44/0.82 (declare-const tptp.denota1275485728_a_b_c (-> tptp.denota231621370t_unit tptp.oDE_a_c tptp.finite1398487019real_c tptp.finite1398487019real_c)) % 0.44/0.82 (declare-const tptp.denota1293057250_a_b_c (-> tptp.denota231621370t_unit tptp.oDE_a_c tptp.set_Sum_sum_c_c)) % 0.44/0.82 (declare-const tptp.the_Pr1290640446real_c (-> (-> tptp.produc190496183real_c Bool) tptp.produc190496183real_c)) % 0.44/0.82 (declare-const tptp.ord_le775706699real_c (-> tptp.finite1398487019real_c tptp.finite1398487019real_c Bool)) % 0.44/0.82 (declare-const tptp.collec95329456um_c_c (-> (-> tptp.set_Sum_sum_c_c Bool) tptp.set_set_Sum_sum_c_c)) % 0.44/0.82 (declare-const tptp.collect_real (-> (-> tptp.real Bool) tptp.set_real)) % 0.44/0.82 (declare-const tptp.sum_Inr_c_c (-> tptp.c tptp.sum_sum_c_c)) % 0.44/0.82 (declare-const tptp.oDE_dom_a_c (-> tptp.oDE_a_c tptp.set_c)) % 0.44/0.82 (declare-const tptp.denota256060419gree_c (-> tptp.finite1398487019real_c tptp.finite1398487019real_c tptp.set_c Bool)) % 0.44/0.82 (declare-const tptp.sum_Inl_c_d (-> tptp.c tptp.sum_sum_c_d)) % 0.44/0.82 (declare-const tptp.sup_su1349021703um_c_c (-> tptp.set_Sum_sum_c_c tptp.set_Sum_sum_c_c tptp.set_Sum_sum_c_c)) % 0.44/0.82 (declare-const tptp.sum_Inl_c_c (-> tptp.c tptp.sum_sum_c_c)) % 0.44/0.82 (declare-const tptp.static_FVO_a_c (-> tptp.oDE_a_c tptp.set_c)) % 0.44/0.82 (declare-const tptp.image_327677598real_c (-> (-> tptp.real tptp.finite1398487019real_c) tptp.set_real tptp.set_Fi1407883041real_c)) % 0.44/0.82 (declare-const tptp.image_1980705354real_c (-> (-> tptp.sum_sum_c_d tptp.produc190496183real_c) tptp.set_Sum_sum_c_d tptp.set_Pr1389752855real_c)) % 0.44/0.82 (declare-const tptp.image_1146069259real_c (-> (-> tptp.sum_sum_c_c tptp.produc190496183real_c) tptp.set_Sum_sum_c_c tptp.set_Pr1389752855real_c)) % 0.44/0.82 (declare-const tptp.image_1467045143um_c_c (-> (-> tptp.produc190496183real_c tptp.sum_sum_c_c) tptp.set_Pr1389752855real_c tptp.set_Sum_sum_c_c)) % 0.44/0.82 (declare-const tptp.image_1567202899um_c_d (-> (-> tptp.sum_sum_c_d tptp.sum_sum_c_d) tptp.set_Sum_sum_c_d tptp.set_Sum_sum_c_d)) % 0.44/0.82 (declare-const tptp.image_1558941394um_c_c (-> (-> tptp.sum_sum_c_d tptp.sum_sum_c_c) tptp.set_Sum_sum_c_d tptp.set_Sum_sum_c_c)) % 0.44/0.82 (declare-const tptp.image_675141842um_c_d (-> (-> tptp.sum_sum_c_c tptp.sum_sum_c_d) tptp.set_Sum_sum_c_c tptp.set_Sum_sum_c_d)) % 0.44/0.82 (declare-const tptp.image_666880337um_c_c (-> (-> tptp.sum_sum_c_c tptp.sum_sum_c_c) tptp.set_Sum_sum_c_c tptp.set_Sum_sum_c_c)) % 0.44/0.82 (declare-const tptp.image_c_Sum_sum_c_d (-> (-> tptp.c tptp.sum_sum_c_d) tptp.set_c tptp.set_Sum_sum_c_d)) % 0.44/0.82 (declare-const tptp.image_real_real (-> (-> tptp.real tptp.real) tptp.set_real tptp.set_real)) % 0.44/0.82 (declare-const tptp.hpsafe_a_b_c (-> tptp.hp_a_b_c Bool)) % 0.44/0.82 (declare-const tptp.ord_le132810396r_real (-> tptp.filter_real tptp.filter_real Bool)) % 0.44/0.82 (declare-const tptp.has_ve217091583e_real (-> (-> tptp.real tptp.real) tptp.real tptp.filter_real Bool)) % 0.44/0.82 (declare-const tptp.has_ve373335844real_c (-> (-> tptp.real tptp.produc190496183real_c) tptp.produc190496183real_c tptp.filter_real Bool)) % 0.44/0.82 (declare-const tptp.ord_le1382916304al_c_o (-> (-> tptp.finite1398487019real_c tptp.finite1398487019real_c Bool) (-> tptp.finite1398487019real_c tptp.finite1398487019real_c Bool) Bool)) % 0.44/0.82 (declare-const tptp.image_1475306648um_c_d (-> (-> tptp.produc190496183real_c tptp.sum_sum_c_d) tptp.set_Pr1389752855real_c tptp.set_Sum_sum_c_d)) % 0.44/0.82 (declare-const tptp.has_ve1904308670real_c (-> (-> tptp.real tptp.finite1398487019real_c) tptp.finite1398487019real_c tptp.filter_real Bool)) % 0.44/0.82 (declare-const tptp.set_or385782508real_c (-> tptp.produc190496183real_c tptp.produc190496183real_c tptp.set_Pr1389752855real_c)) % 0.44/0.82 (declare-const tptp.uminus88729697_c_c_o (-> (-> tptp.sum_sum_c_c Bool) tptp.sum_sum_c_c Bool)) % 0.44/0.82 (declare-const tptp.uminus_uminus_c_o (-> (-> tptp.c Bool) tptp.c Bool)) % 0.44/0.82 (declare-const tptp.uminus856758960l_real (-> tptp.produc957004601l_real tptp.produc957004601l_real)) % 0.44/0.82 (declare-const tptp.uminus1629073887um_c_c (-> tptp.produc754691304um_c_c tptp.produc754691304um_c_c)) % 0.44/0.82 (declare-const tptp.uminus125610847c_real (-> tptp.produc1398711912c_real tptp.produc1398711912c_real)) % 0.44/0.82 (declare-const tptp.set_or935154662um_c_c (-> tptp.set_Sum_sum_c_c tptp.set_Sum_sum_c_c tptp.set_set_Sum_sum_c_c)) % 0.44/0.82 (declare-const tptp.uminus_uminus_real (-> tptp.real tptp.real)) % 0.44/0.82 (declare-const tptp.i tptp.denota231621370t_unit) % 0.44/0.82 (declare-const tptp.uminus1225118734um_c_c (-> tptp.produc214722967um_c_c tptp.produc214722967um_c_c)) % 0.44/0.82 (declare-const tptp.image_c_Sum_sum_c_c (-> (-> tptp.c tptp.sum_sum_c_c) tptp.set_c tptp.set_Sum_sum_c_c)) % 0.44/0.82 (declare-const tptp.uminus17964590real_c (-> tptp.produc190496183real_c tptp.produc190496183real_c)) % 0.44/0.82 (declare-const tptp.uminus1737280820real_c (-> tptp.finite1398487019real_c tptp.finite1398487019real_c)) % 0.44/0.82 (declare-const tptp.ab tptp.finite1398487019real_c) % 0.44/0.82 (declare-const tptp.set_or656347191t_real (-> tptp.real tptp.real tptp.set_real)) % 0.44/0.82 (declare-const tptp.produc1439061071um_c_c (-> tptp.set_Sum_sum_c_c tptp.set_Sum_sum_c_c tptp.produc214722967um_c_c)) % 0.44/0.82 (declare-const tptp.sol (-> tptp.real tptp.finite1398487019real_c)) % 0.44/0.82 (declare-const tptp.zero_z1506780526real_c tptp.produc190496183real_c) % 0.44/0.82 (declare-const tptp.bb tptp.finite1398487019real_c) % 0.44/0.82 (declare-const tptp.produc1528874528c_real (-> tptp.set_Sum_sum_c_c tptp.real tptp.produc1398711912c_real)) % 0.44/0.82 (declare-const tptp.set_or248124158real_c (-> tptp.produc190496183real_c tptp.set_Pr1389752855real_c)) % 0.44/0.82 (declare-const tptp.t tptp.real) % 0.44/0.82 (declare-const tptp.zero_z659284464l_real tptp.produc957004601l_real) % 0.44/0.82 (declare-const tptp.ode tptp.oDE_a_c) % 0.44/0.82 (declare-const tptp.ba tptp.finite1398487019real_c) % 0.44/0.82 (declare-const tptp.set_or10334466real_c (-> tptp.produc190496183real_c tptp.set_Pr1389752855real_c)) % 0.44/0.82 (declare-const tptp.v tptp.set_Sum_sum_c_c) % 0.44/0.82 (declare-const tptp.ord_less_eq_set_real (-> tptp.set_real tptp.set_real Bool)) % 0.44/0.82 (declare-const tptp.j tptp.denota231621370t_unit) % 0.44/0.82 (declare-const tptp.ord_less_eq_set_c (-> tptp.set_c tptp.set_c Bool)) % 0.44/0.82 (declare-const tptp.s tptp.real) % 0.44/0.82 (declare-const tptp.zero_z109254132real_c tptp.finite1398487019real_c) % 0.44/0.82 (declare-const tptp.osafe_a_c (-> tptp.oDE_a_c Bool)) % 0.44/0.82 (declare-const tptp.produc1186709024um_c_c (-> tptp.real tptp.set_Sum_sum_c_c tptp.produc754691304um_c_c)) % 0.44/0.82 (declare-const tptp.b tptp.finite1398487019real_c) % 0.44/0.82 (declare-const tptp.aa tptp.finite1398487019real_c) % 0.44/0.82 (declare-const tptp.produc705216881l_real (-> tptp.real tptp.real tptp.produc957004601l_real)) % 0.44/0.82 (declare-const tptp.ord_le1327118209real_c (-> tptp.set_Fi1407883041real_c tptp.set_Fi1407883041real_c Bool)) % 0.44/0.82 (declare-const tptp.topolo1830106092n_real (-> tptp.real tptp.set_real tptp.filter_real)) % 0.44/0.82 (declare-const tptp.ord_le850691415real_c (-> tptp.produc190496183real_c tptp.produc190496183real_c Bool)) % 0.44/0.82 (declare-const tptp.member2124950898um_c_c (-> tptp.set_Sum_sum_c_c tptp.set_set_Sum_sum_c_c Bool)) % 0.44/0.82 (declare-const tptp.ord_le684454199um_c_c (-> tptp.produc214722967um_c_c tptp.produc214722967um_c_c Bool)) % 0.44/0.82 (declare-const tptp.uminus916499104_c_d_o (-> (-> tptp.sum_sum_c_d Bool) tptp.sum_sum_c_d Bool)) % 0.44/0.82 (declare-const tptp.member_real (-> tptp.real tptp.set_real Bool)) % 0.44/0.82 (declare-const tptp.ord_le835231240c_real (-> tptp.produc1398711912c_real tptp.produc1398711912c_real Bool)) % 0.44/0.82 (declare-const tptp.ord_le191210632um_c_c (-> tptp.produc754691304um_c_c tptp.produc754691304um_c_c Bool)) % 0.44/0.82 (declare-const tptp.ord_le1342644953l_real (-> tptp.produc957004601l_real tptp.produc957004601l_real Bool)) % 0.44/0.82 (declare-const tptp.uminus32155087al_c_o (-> (-> tptp.produc190496183real_c Bool) tptp.produc190496183real_c Bool)) % 0.44/0.82 (declare-const tptp.ord_le657554289um_c_c (-> tptp.set_set_Sum_sum_c_c tptp.set_set_Sum_sum_c_c Bool)) % 0.44/0.82 (declare-const tptp.p tptp.formula_a_b_c) % 0.44/0.82 (declare-const tptp.static_BVO_a_c (-> tptp.oDE_a_c tptp.set_Sum_sum_c_c)) % 0.44/0.82 (declare-const tptp.zero_zero_real tptp.real) % 0.44/0.82 (declare-const tptp.equiv_a_b_c (-> tptp.formula_a_b_c tptp.formula_a_b_c tptp.formula_a_b_c)) % 0.44/0.82 (declare-const tptp.uminus23580315al_c_o (-> (-> tptp.finite1398487019real_c Bool) tptp.finite1398487019real_c Bool)) % 0.44/0.82 (declare-const tptp.a tptp.finite1398487019real_c) % 0.44/0.82 (declare-const tptp.ord_le929608341um_b_c (-> tptp.set_Su1783761653um_b_c tptp.set_Su1783761653um_b_c Bool)) % 0.44/0.82 (declare-const tptp.initia1631504802real_c (-> (-> tptp.real tptp.finite1398487019real_c) (-> tptp.real tptp.finite1398487019real_c tptp.finite1398487019real_c) tptp.set_real tptp.set_Fi1407883041real_c Bool)) % 0.44/0.82 (declare-const tptp.implies_a_b_c (-> tptp.formula_a_b_c tptp.formula_a_b_c tptp.formula_a_b_c)) % 0.44/0.82 (declare-const tptp.ord_le1132241894al_c_o (-> (-> tptp.produc190496183real_c Bool) (-> tptp.produc190496183real_c Bool) Bool)) % 0.44/0.82 (declare-const tptp.evolveODE_a_c_b (-> tptp.oDE_a_c tptp.formula_a_b_c tptp.hp_a_b_c)) % 0.44/0.82 (declare-const tptp.ord_le2143422793_c_d_o (-> (-> tptp.sum_sum_c_d Bool) (-> tptp.sum_sum_c_d Bool) Bool)) % 0.44/0.82 (declare-const tptp.fsafe_a_b_c (-> tptp.formula_a_b_c Bool)) % 0.44/0.82 (declare-const tptp.ord_le1315653386_c_c_o (-> (-> tptp.sum_sum_c_c Bool) (-> tptp.sum_sum_c_c Bool) Bool)) % 0.44/0.82 (define tptp.ord_le977353143real_c () (let ((_let_1 (@var "B5" tptp.set_Pr1389752855real_c))) (let ((_let_2 (@var "T" tptp.produc190496183real_c))) (let ((_let_3 (_ tptp.member1895684704real_c _let_2))) (let ((_let_4 (@var "A5" tptp.set_Pr1389752855real_c))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1))))))))) % 0.44/0.82 (define tptp.ord_le764260924um_c_d () (let ((_let_1 (@var "B5" tptp.set_Sum_sum_c_d))) (let ((_let_2 (@var "T" tptp.sum_sum_c_d))) (let ((_let_3 (_ tptp.member_Sum_sum_c_d _let_2))) (let ((_let_4 (@var "A5" tptp.set_Sum_sum_c_d))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1))))))))) % 0.44/0.82 (define tptp.ord_le1772180283um_c_c () (let ((_let_1 (@var "B5" tptp.set_Sum_sum_c_c))) (let ((_let_2 (@var "T" tptp.sum_sum_c_c))) (let ((_let_3 (_ tptp.member_Sum_sum_c_c _let_2))) (let ((_let_4 (@var "A5" tptp.set_Sum_sum_c_c))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1))))))))) % 0.44/0.82 (define tptp.bNF_Ca1693016812um_c_c () (let ((_let_1 (@var "J" tptp.finite1398487019real_c))) (let ((_let_2 (@var "As" (-> tptp.finite1398487019real_c tptp.set_Sum_sum_c_c)))) (let ((_let_3 (@var "I2" tptp.finite1398487019real_c))) (let ((_let_4 (@var "R" tptp.set_Pr1389752855real_c))) (lambda (@list _let_4 _let_2) (forall (@list _let_3 _let_1) (=> (_ (_ tptp.member1895684704real_c (_ (_ tptp.produc394644079real_c _let_3) _let_1)) _let_4) (_ (_ tptp.ord_le1772180283um_c_c (_ _let_2 _let_3)) (_ _let_2 _let_1)))))))))) % 0.44/0.82 (define tptp.bNF_Ca449034301c_real () (let ((_let_1 (@var "J" tptp.finite1398487019real_c))) (let ((_let_2 (@var "As" (-> tptp.finite1398487019real_c tptp.real)))) (let ((_let_3 (@var "I2" tptp.finite1398487019real_c))) (let ((_let_4 (@var "R" tptp.set_Pr1389752855real_c))) (lambda (@list _let_4 _let_2) (forall (@list _let_3 _let_1) (=> (_ (_ tptp.member1895684704real_c (_ (_ tptp.produc394644079real_c _let_3) _let_1)) _let_4) (_ (_ tptp.ord_less_eq_real (_ _let_2 _let_3)) (_ _let_2 _let_1)))))))))) % 0.44/0.82 (define tptp.coinci501627771_a_b_c () (let ((_let_1 (@var "Phi" tptp.formula_a_b_c))) (let ((_let_2 (@var "J2" tptp.denota231621370t_unit))) (let ((_let_3 (@var "Nu4" tptp.produc190496183real_c))) (let ((_let_4 (@var "I3" tptp.denota231621370t_unit))) (let ((_let_5 (@var "Nu3" tptp.produc190496183real_c))) (lambda (@list _let_1) (forall (@list _let_5 _let_3 _let_4 _let_2) (=> (_ (_ (_ tptp.denota69106024_a_b_c _let_4) _let_2) (_ tptp.static_SIGF_a_b_c _let_1)) (=> (_ (_ (_ tptp.denota1997846518gree_c _let_5) _let_3) (_ tptp.static_FVF_a_b_c _let_1)) (= (_ (_ tptp.member1895684704real_c _let_5) (_ (_ tptp.denota968303861_a_b_c _let_4) _let_1)) (_ (_ tptp.member1895684704real_c _let_3) (_ (_ tptp.denota968303861_a_b_c _let_2) _let_1))))))))))))) % 0.44/0.82 (define tptp.coinci1852866155_a_b_c () (let ((_let_1 (@var "I3" tptp.denota231621370t_unit))) (let ((_let_2 (@var "Alpha" tptp.hp_a_b_c))) (let ((_let_3 (@var "J2" tptp.denota231621370t_unit))) (lambda (@list _let_2) (forall (@list _let_1 _let_3) (and (_ (_ (_ tptp.coinci354700372_a_b_c _let_2) _let_1) _let_3) (_ (_ tptp.coinci772602909_a_b_c _let_2) _let_1)))))))) % 0.44/0.82 (define tptp.uminus232257166real_c () (let ((_let_1 (@var "A5" tptp.set_Pr1389752855real_c))) (let ((_let_2 (@var "X4" tptp.produc190496183real_c))) (lambda (@list _let_1) (_ tptp.collec1643251106real_c (lambda (@list _let_2) (not (_ (_ tptp.member1895684704real_c _let_2) _let_1)))))))) % 0.44/0.82 (define tptp.uminus373867045um_c_d () (let ((_let_1 (@var "A5" tptp.set_Sum_sum_c_d))) (let ((_let_2 (@var "X4" tptp.sum_sum_c_d))) (lambda (@list _let_1) (_ tptp.collect_Sum_sum_c_d (lambda (@list _let_2) (not (_ (_ tptp.member_Sum_sum_c_d _let_2) _let_1)))))))) % 0.44/0.82 (define tptp.uminus102402154real_c () (let ((_let_1 (@var "A5" tptp.set_Fi1407883041real_c))) (let ((_let_2 (@var "X4" tptp.finite1398487019real_c))) (lambda (@list _let_1) (_ tptp.collec230941376real_c (lambda (@list _let_2) (not (_ (_ tptp.member1261661570real_c _let_2) _let_1)))))))) % 0.44/0.82 (define tptp.uminus_uminus_set_c () (let ((_let_1 (@var "A5" tptp.set_c))) (let ((_let_2 (@var "X4" tptp.c))) (lambda (@list _let_1) (_ tptp.collect_c (lambda (@list _let_2) (not (_ (_ tptp.member_c _let_2) _let_1)))))))) % 0.44/0.82 (define tptp.uminus1381786404um_c_c () (let ((_let_1 (@var "A5" tptp.set_Sum_sum_c_c))) (let ((_let_2 (@var "X4" tptp.sum_sum_c_c))) (lambda (@list _let_1) (_ tptp.collect_Sum_sum_c_c (lambda (@list _let_2) (not (_ (_ tptp.member_Sum_sum_c_c _let_2) _let_1)))))))) % 0.44/0.82 (define tptp.denota1896987029_a_b_c () (let ((_let_1 (@var "Sol2" tptp.finite1398487019real_c))) (let ((_let_2 (@var "ODE2" tptp.oDE_a_c))) (let ((_let_3 (@var "I3" tptp.denota231621370t_unit))) (lambda (@list _let_3 _let_2 _let_1) (_ (_ tptp.produc394644079real_c _let_1) (_ (_ (_ tptp.denota1275485728_a_b_c _let_3) _let_2) _let_1))))))) % 0.44/0.82 (define tptp.denota161327353_a_b_c () (let ((_let_1 (@var "ODE2" tptp.oDE_a_c))) (let ((_let_2 (@var "I3" tptp.denota231621370t_unit))) (let ((_let_3 (_ (_ tptp.denota1293057250_a_b_c _let_2) _let_1))) (let ((_let_4 (@var "Sol2" tptp.finite1398487019real_c))) (let ((_let_5 (@var "Omega3" tptp.produc190496183real_c))) (let ((_let_6 (_ tptp.denota1997846518gree_c _let_5))) (let ((_let_7 (@var "Nu3" tptp.produc190496183real_c))) (lambda (@list _let_2 _let_1 _let_7 _let_4) (_ tptp.the_Pr1290640446real_c (lambda (@list _let_5) (and (_ (_ _let_6 _let_7) (_ tptp.uminus1381786404um_c_c _let_3)) (_ (_ _let_6 (_ (_ (_ tptp.denota1896987029_a_b_c _let_2) _let_1) _let_4)) _let_3))))))))))))) % 0.44/0.82 (define tptp.set_or2003963744real_c () (let ((_let_1 (@var "L3" tptp.finite1398487019real_c))) (lambda (@list _let_1) (_ tptp.collec230941376real_c (_ tptp.ord_le775706699real_c _let_1))))) % 0.44/0.82 (define tptp.set_or2028906832um_c_c () (let ((_let_1 (@var "L3" tptp.set_Sum_sum_c_c))) (lambda (@list _let_1) (_ tptp.collec95329456um_c_c (_ tptp.ord_le1772180283um_c_c _let_1))))) % 0.44/0.82 (define tptp.set_ord_atLeast_real () (let ((_let_1 (@var "L3" tptp.real))) (lambda (@list _let_1) (_ tptp.collect_real (_ tptp.ord_less_eq_real _let_1))))) % 0.44/0.82 (define tptp.set_or1478397028real_c () (let ((_let_1 (@var "U2" tptp.finite1398487019real_c))) (let ((_let_2 (@var "X4" tptp.finite1398487019real_c))) (lambda (@list _let_1) (_ tptp.collec230941376real_c (lambda (@list _let_2) (_ (_ tptp.ord_le775706699real_c _let_2) _let_1))))))) % 0.44/0.82 (define tptp.set_or326480468um_c_c () (let ((_let_1 (@var "U2" tptp.set_Sum_sum_c_c))) (let ((_let_2 (@var "X4" tptp.set_Sum_sum_c_c))) (lambda (@list _let_1) (_ tptp.collec95329456um_c_c (lambda (@list _let_2) (_ (_ tptp.ord_le1772180283um_c_c _let_2) _let_1))))))) % 0.44/0.82 (define tptp.set_ord_atMost_real () (let ((_let_1 (@var "U2" tptp.real))) (let ((_let_2 (@var "X4" tptp.real))) (lambda (@list _let_1) (_ tptp.collect_real (lambda (@list _let_2) (_ (_ tptp.ord_less_eq_real _let_2) _let_1))))))) % 0.44/0.82 (define @t1 () (_ tptp.denota1293057250_a_b_c tptp.j)) % 0.44/0.82 (define @t2 () (_ @t1 tptp.ode)) % 0.44/0.82 (define @t3 () (_ tptp.sol tptp.s)) % 0.44/0.82 (define @t4 () (_ (_ tptp.produc394644079real_c tptp.aa) tptp.ba)) % 0.44/0.82 (define @t5 () (_ (_ (_ tptp.denota161327353_a_b_c tptp.j) tptp.ode) @t4)) % 0.44/0.82 (define @t6 () (_ tptp.denota1997846518gree_c (_ @t5 @t3))) % 0.44/0.82 (define @t7 () (_ (_ @t6 (_ (_ (_ tptp.denota1896987029_a_b_c tptp.j) tptp.ode) @t3)) @t2)) % 0.44/0.82 (define @t8 () (_ tptp.uminus1381786404um_c_c @t2)) % 0.44/0.82 (define @t9 () (@var "S" tptp.real)) % 0.44/0.82 (define @t10 () (_ tptp.sol @t9)) % 0.44/0.82 (define @t11 () (@list @t9)) % 0.44/0.82 (define @t12 () (@var "ODE" tptp.oDE_a_c)) % 0.44/0.82 (define @t13 () (@var "I" tptp.denota231621370t_unit)) % 0.44/0.82 (define @t14 () (_ (_ tptp.denota1293057250_a_b_c @t13) @t12)) % 0.44/0.82 (define @t15 () (@var "Sol" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t16 () (_ (_ (_ tptp.denota1896987029_a_b_c @t13) @t12) @t15)) % 0.44/0.82 (define @t17 () (@var "Nu" tptp.produc190496183real_c)) % 0.44/0.82 (define @t18 () (_ tptp.denota1997846518gree_c (_ (_ (_ (_ tptp.denota161327353_a_b_c @t13) @t12) @t17) @t15))) % 0.44/0.82 (define @t19 () (_ tptp.uminus1381786404um_c_c @t14)) % 0.44/0.82 (define @t20 () (@var "Y2" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t21 () (@var "X2" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t22 () (@var "Y1" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t23 () (@var "X1" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t24 () (@var "B2" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t25 () (@var "B" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t26 () (= @t25 @t24)) % 0.44/0.82 (define @t27 () (@var "A2" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t28 () (@var "A" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t29 () (= @t28 @t27)) % 0.44/0.82 (define @t30 () (_ (_ tptp.produc394644079real_c @t28) @t25)) % 0.44/0.82 (define @t31 () (= @t30 (_ (_ tptp.produc394644079real_c @t27) @t24))) % 0.44/0.82 (define @t32 () (@list @t28 @t25 @t27 @t24)) % 0.44/0.82 (define @t33 () (@var "Omega" tptp.produc190496183real_c)) % 0.44/0.82 (define @t34 () (_ tptp.denota1997846518gree_c @t33)) % 0.44/0.82 (define @t35 () (_ (_ tptp.produc394644079real_c tptp.a) tptp.b)) % 0.44/0.82 (define @t36 () (_ (_ tptp.denota1997846518gree_c @t35) @t4)) % 0.44/0.82 (define @t37 () (_ (_ tptp.denota1293057250_a_b_c tptp.i) tptp.ode)) % 0.44/0.82 (define @t38 () (_ (_ (_ tptp.denota161327353_a_b_c tptp.i) tptp.ode) @t35)) % 0.44/0.82 (define @t39 () (_ tptp.denota1997846518gree_c (_ @t38 @t10))) % 0.44/0.82 (define @t40 () (_ tptp.static_BVO_a_c tptp.ode)) % 0.44/0.82 (define @t41 () (@var "V" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t42 () (@var "A3" tptp.produc190496183real_c)) % 0.44/0.82 (define @t43 () (@var "B3" tptp.produc190496183real_c)) % 0.44/0.82 (define @t44 () (@var "A3" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t45 () (_ tptp.denota1997846518gree_c @t17)) % 0.44/0.82 (define @t46 () (@var "Y" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t47 () (@var "X" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t48 () (_ (_ tptp.produc394644079real_c @t47) @t46)) % 0.44/0.82 (define @t49 () (@var "P" tptp.produc190496183real_c)) % 0.44/0.82 (define @t50 () (@list @t47 @t46)) % 0.44/0.82 (define @t51 () (@var "P2" (-> tptp.produc190496183real_c Bool))) % 0.44/0.82 (define @t52 () (@var "B4" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t53 () (@var "A4" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t54 () (_ (_ tptp.produc394644079real_c @t53) @t52)) % 0.44/0.82 (define @t55 () (@list @t53 @t52)) % 0.44/0.82 (define @t56 () (forall @t55 (_ @t51 @t54))) % 0.44/0.82 (define @t57 () (@var "Prod" tptp.produc190496183real_c)) % 0.44/0.82 (define @t58 () (@var "Y3" tptp.produc190496183real_c)) % 0.44/0.82 (define @t59 () (_ tptp.ord_le1772180283um_c_c @t37)) % 0.44/0.82 (define @t60 () (@var "B" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t61 () (_ tptp.uminus1381786404um_c_c @t60)) % 0.44/0.82 (define @t62 () (@var "A" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t63 () (_ tptp.uminus1381786404um_c_c @t62)) % 0.44/0.82 (define @t64 () (_ (_ tptp.produc1439061071um_c_c @t62) @t60)) % 0.44/0.82 (define @t65 () (@list @t62 @t60)) % 0.44/0.82 (define @t66 () (@var "B" tptp.real)) % 0.44/0.82 (define @t67 () (_ tptp.uminus_uminus_real @t66)) % 0.44/0.82 (define @t68 () (_ (_ tptp.produc1528874528c_real @t62) @t66)) % 0.44/0.82 (define @t69 () (@var "A" tptp.real)) % 0.44/0.82 (define @t70 () (_ tptp.uminus_uminus_real @t69)) % 0.44/0.82 (define @t71 () (_ (_ tptp.produc1186709024um_c_c @t69) @t60)) % 0.44/0.82 (define @t72 () (_ (_ tptp.produc705216881l_real @t69) @t66)) % 0.44/0.82 (define @t73 () (@list @t69 @t66)) % 0.44/0.82 (define @t74 () (@var "A3" tptp.set_Pr1389752855real_c)) % 0.44/0.82 (define @t75 () (@var "C" tptp.produc190496183real_c)) % 0.44/0.82 (define @t76 () (_ tptp.member1895684704real_c @t75)) % 0.44/0.82 (define @t77 () (_ @t76 (_ tptp.uminus232257166real_c @t74))) % 0.44/0.82 (define @t78 () (_ @t76 @t74)) % 0.44/0.82 (define @t79 () (not @t78)) % 0.44/0.82 (define @t80 () (@list @t75 @t74)) % 0.44/0.82 (define @t81 () (@var "A3" tptp.set_Sum_sum_c_d)) % 0.44/0.82 (define @t82 () (@var "C" tptp.sum_sum_c_d)) % 0.44/0.82 (define @t83 () (_ tptp.member_Sum_sum_c_d @t82)) % 0.44/0.82 (define @t84 () (_ @t83 (_ tptp.uminus373867045um_c_d @t81))) % 0.44/0.82 (define @t85 () (_ @t83 @t81)) % 0.44/0.82 (define @t86 () (not @t85)) % 0.44/0.82 (define @t87 () (@list @t82 @t81)) % 0.44/0.82 (define @t88 () (_ tptp.uminus1381786404um_c_c @t44)) % 0.44/0.82 (define @t89 () (@var "C" tptp.sum_sum_c_c)) % 0.44/0.82 (define @t90 () (_ tptp.member_Sum_sum_c_c @t89)) % 0.44/0.82 (define @t91 () (_ @t90 @t88)) % 0.44/0.82 (define @t92 () (_ @t90 @t44)) % 0.44/0.82 (define @t93 () (not @t92)) % 0.44/0.82 (define @t94 () (@list @t89 @t44)) % 0.44/0.82 (define @t95 () (@var "B3" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t96 () (= @t44 @t95)) % 0.44/0.82 (define @t97 () (_ tptp.uminus1381786404um_c_c @t95)) % 0.44/0.82 (define @t98 () (@list @t44 @t95)) % 0.44/0.82 (define @t99 () (@list @t69)) % 0.44/0.82 (define @t100 () (_ tptp.ord_le1772180283um_c_c @t95)) % 0.44/0.82 (define @t101 () (_ @t100 @t44)) % 0.44/0.82 (define @t102 () (_ tptp.ord_le1772180283um_c_c @t44)) % 0.44/0.82 (define @t103 () (_ @t102 @t95)) % 0.44/0.82 (define @t104 () (@var "B3" tptp.set_Pr1389752855real_c)) % 0.44/0.82 (define @t105 () (_ (_ tptp.ord_le977353143real_c @t74) @t104)) % 0.44/0.82 (define @t106 () (@var "X" tptp.produc190496183real_c)) % 0.44/0.82 (define @t107 () (_ tptp.member1895684704real_c @t106)) % 0.44/0.82 (define @t108 () (_ @t107 @t104)) % 0.44/0.82 (define @t109 () (_ @t107 @t74)) % 0.44/0.82 (define @t110 () (@list @t106)) % 0.44/0.82 (define @t111 () (@var "B3" tptp.set_Sum_sum_c_d)) % 0.44/0.82 (define @t112 () (_ (_ tptp.ord_le764260924um_c_d @t81) @t111)) % 0.44/0.82 (define @t113 () (@var "X" tptp.sum_sum_c_d)) % 0.44/0.82 (define @t114 () (_ tptp.member_Sum_sum_c_d @t113)) % 0.44/0.82 (define @t115 () (_ @t114 @t111)) % 0.44/0.82 (define @t116 () (_ @t114 @t81)) % 0.44/0.82 (define @t117 () (@list @t113)) % 0.44/0.82 (define @t118 () (@var "X" tptp.sum_sum_c_c)) % 0.44/0.82 (define @t119 () (_ tptp.member_Sum_sum_c_c @t118)) % 0.44/0.82 (define @t120 () (_ @t119 @t95)) % 0.44/0.82 (define @t121 () (_ @t119 @t44)) % 0.44/0.82 (define @t122 () (@list @t118)) % 0.44/0.82 (define @t123 () (@var "Y3" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t124 () (@var "X3" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t125 () (= @t124 @t123)) % 0.44/0.82 (define @t126 () (_ tptp.uminus1381786404um_c_c @t123)) % 0.44/0.82 (define @t127 () (_ tptp.uminus1381786404um_c_c @t124)) % 0.44/0.82 (define @t128 () (@list @t124 @t123)) % 0.44/0.82 (define @t129 () (@list @t124)) % 0.44/0.82 (define @t130 () (= @t69 @t66)) % 0.44/0.82 (define @t131 () (= @t70 @t67)) % 0.44/0.82 (define @t132 () (@var "A" tptp.produc190496183real_c)) % 0.44/0.82 (define @t133 () (@var "A" tptp.sum_sum_c_c)) % 0.44/0.82 (define @t134 () (@var "P2" (-> tptp.sum_sum_c_c Bool))) % 0.44/0.82 (define @t135 () (_ tptp.collect_Sum_sum_c_c @t134)) % 0.44/0.82 (define @t136 () (@var "A" tptp.sum_sum_c_d)) % 0.44/0.82 (define @t137 () (@var "P2" (-> tptp.sum_sum_c_d Bool))) % 0.44/0.82 (define @t138 () (@var "P2" (-> tptp.finite1398487019real_c Bool))) % 0.44/0.82 (define @t139 () (_ tptp.collec230941376real_c @t138)) % 0.44/0.82 (define @t140 () (@var "A" tptp.c)) % 0.44/0.82 (define @t141 () (@var "P2" (-> tptp.c Bool))) % 0.44/0.82 (define @t142 () (_ tptp.collect_c @t141)) % 0.44/0.82 (define @t143 () (@var "X4" tptp.produc190496183real_c)) % 0.44/0.82 (define @t144 () (_ tptp.member1895684704real_c @t143)) % 0.44/0.82 (define @t145 () (_ @t144 @t74)) % 0.44/0.82 (define @t146 () (@list @t143)) % 0.44/0.82 (define @t147 () (@var "X4" tptp.sum_sum_c_c)) % 0.44/0.82 (define @t148 () (_ tptp.member_Sum_sum_c_c @t147)) % 0.44/0.82 (define @t149 () (_ @t148 @t44)) % 0.44/0.82 (define @t150 () (@list @t147)) % 0.44/0.82 (define @t151 () (@list @t44)) % 0.44/0.82 (define @t152 () (@var "X4" tptp.sum_sum_c_d)) % 0.44/0.82 (define @t153 () (_ tptp.member_Sum_sum_c_d @t152)) % 0.44/0.82 (define @t154 () (_ @t153 @t81)) % 0.44/0.82 (define @t155 () (@list @t152)) % 0.44/0.82 (define @t156 () (@var "A3" tptp.set_Fi1407883041real_c)) % 0.44/0.82 (define @t157 () (@var "X4" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t158 () (_ tptp.member1261661570real_c @t157)) % 0.44/0.82 (define @t159 () (_ @t158 @t156)) % 0.44/0.82 (define @t160 () (@list @t157)) % 0.44/0.82 (define @t161 () (@var "A3" tptp.set_c)) % 0.44/0.82 (define @t162 () (@var "X4" tptp.c)) % 0.44/0.82 (define @t163 () (_ tptp.member_c @t162)) % 0.44/0.82 (define @t164 () (_ @t163 @t161)) % 0.44/0.82 (define @t165 () (@list @t162)) % 0.44/0.82 (define @t166 () (@var "Q" (-> tptp.finite1398487019real_c Bool))) % 0.44/0.82 (define @t167 () (_ tptp.collec230941376real_c @t166)) % 0.44/0.82 (define @t168 () (_ @t166 @t47)) % 0.44/0.82 (define @t169 () (_ @t138 @t47)) % 0.44/0.82 (define @t170 () (@list @t47)) % 0.44/0.82 (define @t171 () (@list @t138 @t166)) % 0.44/0.82 (define @t172 () (@var "Q" (-> tptp.c Bool))) % 0.44/0.82 (define @t173 () (_ tptp.collect_c @t172)) % 0.44/0.82 (define @t174 () (@var "X" tptp.c)) % 0.44/0.82 (define @t175 () (_ @t172 @t174)) % 0.44/0.82 (define @t176 () (_ @t141 @t174)) % 0.44/0.82 (define @t177 () (@list @t174)) % 0.44/0.82 (define @t178 () (@list @t141 @t172)) % 0.44/0.82 (define @t179 () (_ tptp.ord_le1772180283um_c_c @t123)) % 0.44/0.82 (define @t180 () (_ @t179 @t124)) % 0.44/0.82 (define @t181 () (_ tptp.ord_le1772180283um_c_c @t127)) % 0.44/0.82 (define @t182 () (_ tptp.ord_less_eq_real @t69)) % 0.44/0.82 (define @t183 () (_ @t182 @t66)) % 0.44/0.82 (define @t184 () (_ tptp.ord_less_eq_real @t67)) % 0.44/0.82 (define @t185 () (_ @t184 @t70)) % 0.44/0.82 (define @t186 () (@list @t66 @t69)) % 0.44/0.82 (define @t187 () (_ tptp.ord_less_eq_real @t66)) % 0.44/0.82 (define @t188 () (_ @t187 @t69)) % 0.44/0.82 (define @t189 () (not @t183)) % 0.44/0.82 (define @t190 () (_ @t166 @t157)) % 0.44/0.82 (define @t191 () (_ @t138 @t157)) % 0.44/0.82 (define @t192 () (_ (_ tptp.ord_le1327118209real_c @t139) @t167)) % 0.44/0.82 (define @t193 () (_ @t172 @t162)) % 0.44/0.82 (define @t194 () (_ @t141 @t162)) % 0.44/0.82 (define @t195 () (_ (_ tptp.ord_less_eq_set_c @t142) @t173)) % 0.44/0.82 (define @t196 () (@var "Q" (-> tptp.sum_sum_c_c Bool))) % 0.44/0.82 (define @t197 () (_ @t196 @t147)) % 0.44/0.82 (define @t198 () (_ @t134 @t147)) % 0.44/0.82 (define @t199 () (_ tptp.collect_Sum_sum_c_c @t196)) % 0.44/0.82 (define @t200 () (_ (_ tptp.ord_le1772180283um_c_c @t135) @t199)) % 0.44/0.82 (define @t201 () (@list @t134 @t196)) % 0.44/0.82 (define @t202 () (@var "A5" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t203 () (@var "B5" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t204 () (@list @t202 @t203)) % 0.44/0.82 (define @t205 () (@var "Z" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t206 () (@var "Y4" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t207 () (lambda (@list @t206 @t205) (= @t206 @t205))) % 0.44/0.82 (define @t208 () (@var "C2" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t209 () (_ @t196 @t118)) % 0.44/0.82 (define @t210 () (_ @t134 @t118)) % 0.44/0.82 (define @t211 () (@var "B5" tptp.set_Pr1389752855real_c)) % 0.44/0.82 (define @t212 () (_ @t144 @t211)) % 0.44/0.82 (define @t213 () (@var "A5" tptp.set_Pr1389752855real_c)) % 0.44/0.82 (define @t214 () (_ @t144 @t213)) % 0.44/0.82 (define @t215 () (@list @t213 @t211)) % 0.44/0.82 (define @t216 () (@var "B5" tptp.set_Sum_sum_c_d)) % 0.44/0.82 (define @t217 () (_ @t153 @t216)) % 0.44/0.82 (define @t218 () (@var "A5" tptp.set_Sum_sum_c_d)) % 0.44/0.82 (define @t219 () (_ @t153 @t218)) % 0.44/0.82 (define @t220 () (@list @t218 @t216)) % 0.44/0.82 (define @t221 () (_ @t148 @t203)) % 0.44/0.82 (define @t222 () (_ @t148 @t202)) % 0.44/0.82 (define @t223 () (@var "X3" tptp.produc190496183real_c)) % 0.44/0.82 (define @t224 () (_ tptp.member1895684704real_c @t223)) % 0.44/0.82 (define @t225 () (_ @t224 @t74)) % 0.44/0.82 (define @t226 () (@var "X3" tptp.sum_sum_c_d)) % 0.44/0.82 (define @t227 () (_ tptp.member_Sum_sum_c_d @t226)) % 0.44/0.82 (define @t228 () (_ @t227 @t81)) % 0.44/0.82 (define @t229 () (@var "X3" tptp.sum_sum_c_c)) % 0.44/0.82 (define @t230 () (_ tptp.member_Sum_sum_c_c @t229)) % 0.44/0.82 (define @t231 () (_ @t230 @t44)) % 0.44/0.82 (define @t232 () (_ tptp.ord_less_eq_real @t70)) % 0.44/0.82 (define @t233 () (_ tptp.ord_le1772180283um_c_c @t126)) % 0.44/0.82 (define @t234 () (@list @t123 @t124)) % 0.44/0.82 (define @t235 () (_ tptp.ord_le1772180283um_c_c @t124)) % 0.44/0.82 (define @t236 () (_ @t235 @t123)) % 0.44/0.82 (define @t237 () (@var "Omega2" tptp.produc190496183real_c)) % 0.44/0.82 (define @t238 () (_ @t45 @t237)) % 0.44/0.82 (define @t239 () (@var "Nu2" tptp.produc190496183real_c)) % 0.44/0.82 (define @t240 () (_ @t45 @t239)) % 0.44/0.82 (define @t241 () (@var "D" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t242 () (@var "C" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t243 () (@var "D" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t244 () (_ tptp.ord_le1772180283um_c_c @t60)) % 0.44/0.82 (define @t245 () (_ @t244 @t243)) % 0.44/0.82 (define @t246 () (@var "C" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t247 () (_ tptp.ord_le1772180283um_c_c @t62)) % 0.44/0.82 (define @t248 () (_ @t247 @t246)) % 0.44/0.82 (define @t249 () (@list @t62 @t60 @t246 @t243)) % 0.44/0.82 (define @t250 () (@var "D" tptp.real)) % 0.44/0.82 (define @t251 () (_ @t187 @t250)) % 0.44/0.82 (define @t252 () (@var "C" tptp.real)) % 0.44/0.82 (define @t253 () (_ @t182 @t252)) % 0.44/0.82 (define @t254 () (@list @t69 @t66 @t252 @t250)) % 0.44/0.82 (define @t255 () (@var "X3" tptp.real)) % 0.44/0.82 (define @t256 () (_ tptp.ord_less_eq_real @t255)) % 0.44/0.82 (define @t257 () (@list @t255)) % 0.44/0.82 (define @t258 () (@var "Y5" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t259 () (@var "X5" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t260 () (@var "Y3" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t261 () (@var "X3" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t262 () (@var "Y5" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t263 () (@var "X5" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t264 () (_ @t179 @t262)) % 0.44/0.82 (define @t265 () (_ @t235 @t263)) % 0.44/0.82 (define @t266 () (@var "Y5" tptp.real)) % 0.44/0.82 (define @t267 () (@var "Y3" tptp.real)) % 0.44/0.82 (define @t268 () (_ tptp.ord_less_eq_real @t267)) % 0.44/0.82 (define @t269 () (_ @t268 @t266)) % 0.44/0.82 (define @t270 () (@var "X5" tptp.real)) % 0.44/0.82 (define @t271 () (_ @t256 @t270)) % 0.44/0.82 (define @t272 () (_ tptp.static_FVF_a_b_c tptp.p)) % 0.44/0.82 (define @t273 () (_ (_ tptp.denota968303861_a_b_c tptp.i) tptp.p)) % 0.44/0.82 (define @t274 () (_ tptp.sol @t255)) % 0.44/0.82 (define @t275 () (_ @t256 tptp.t)) % 0.44/0.82 (define @t276 () (_ tptp.ord_less_eq_real tptp.zero_zero_real)) % 0.44/0.82 (define @t277 () (_ @t276 @t255)) % 0.44/0.82 (define @t278 () (= @t69 tptp.zero_zero_real)) % 0.44/0.82 (define @t279 () (@var "Ba" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t280 () (@var "Aa" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t281 () (_ (_ tptp.produc394644079real_c @t280) @t279)) % 0.44/0.82 (define @t282 () (@var "B6" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t283 () (@var "A6" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t284 () (_ (_ tptp.produc394644079real_c @t283) @t282)) % 0.44/0.82 (define @t285 () (=> (_ (_ (_ tptp.denota1997846518gree_c @t284) @t281) @t272) (= (_ (_ tptp.member1895684704real_c @t284) @t273) (_ (_ tptp.member1895684704real_c @t281) (_ (_ tptp.denota968303861_a_b_c tptp.j) tptp.p))))) % 0.44/0.82 (define @t286 () (@list @t283 @t282 @t280 @t279)) % 0.44/0.82 (define @t287 () (_ @t276 @t69)) % 0.44/0.82 (define @t288 () (_ @t182 tptp.zero_zero_real)) % 0.44/0.82 (define @t289 () (= @t255 tptp.zero_zero_real)) % 0.44/0.82 (define @t290 () (@var "A3" tptp.formula_a_b_c)) % 0.44/0.82 (define @t291 () (_ tptp.denota968303861_a_b_c @t13)) % 0.44/0.82 (define @t292 () (_ tptp.member1895684704real_c @t17)) % 0.44/0.82 (define @t293 () (_ @t292 (_ @t291 @t290))) % 0.44/0.82 (define @t294 () (@var "B3" tptp.formula_a_b_c)) % 0.44/0.82 (define @t295 () (_ @t292 (_ @t291 @t294))) % 0.44/0.82 (define @t296 () (=> @t293 @t295)) % 0.44/0.82 (define @t297 () (= @t293 @t295)) % 0.44/0.82 (define @t298 () (@list @t17 @t13 @t290 @t294)) % 0.44/0.82 (define @t299 () (@var "F" (-> tptp.set_Sum_sum_c_c tptp.set_Sum_sum_c_c))) % 0.44/0.82 (define @t300 () (@var "Y" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t301 () (@var "X" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t302 () (_ (_ tptp.ord_le1772180283um_c_c @t301) @t300)) % 0.44/0.82 (define @t303 () (@list @t301 @t300)) % 0.44/0.82 (define @t304 () (forall @t303 (=> @t302 (_ (_ tptp.ord_le1772180283um_c_c (_ @t299 @t301)) (_ @t299 @t300))))) % 0.44/0.82 (define @t305 () (_ @t244 @t246)) % 0.44/0.82 (define @t306 () (=> @t305 (=> @t304 (_ @t247 (_ @t299 @t246))))) % 0.44/0.82 (define @t307 () (_ @t299 @t60)) % 0.44/0.82 (define @t308 () (@list @t62 @t299 @t60 @t246)) % 0.44/0.82 (define @t309 () (@var "F" (-> tptp.real tptp.set_Sum_sum_c_c))) % 0.44/0.82 (define @t310 () (@var "Y" tptp.real)) % 0.44/0.82 (define @t311 () (@var "X" tptp.real)) % 0.44/0.82 (define @t312 () (_ (_ tptp.ord_less_eq_real @t311) @t310)) % 0.44/0.82 (define @t313 () (@list @t311 @t310)) % 0.44/0.82 (define @t314 () (forall @t313 (=> @t312 (_ (_ tptp.ord_le1772180283um_c_c (_ @t309 @t311)) (_ @t309 @t310))))) % 0.44/0.82 (define @t315 () (_ @t187 @t252)) % 0.44/0.82 (define @t316 () (=> @t315 (=> @t314 (_ @t247 (_ @t309 @t252))))) % 0.44/0.82 (define @t317 () (_ @t309 @t66)) % 0.44/0.82 (define @t318 () (@list @t62 @t309 @t66 @t252)) % 0.44/0.82 (define @t319 () (@var "F" (-> tptp.set_Sum_sum_c_c tptp.real))) % 0.44/0.82 (define @t320 () (forall @t303 (=> @t302 (_ (_ tptp.ord_less_eq_real (_ @t319 @t301)) (_ @t319 @t300))))) % 0.44/0.82 (define @t321 () (=> @t305 (=> @t320 (_ @t182 (_ @t319 @t246))))) % 0.44/0.82 (define @t322 () (_ @t319 @t60)) % 0.44/0.82 (define @t323 () (@list @t69 @t319 @t60 @t246)) % 0.44/0.82 (define @t324 () (@var "F" (-> tptp.real tptp.real))) % 0.44/0.82 (define @t325 () (forall @t313 (=> @t312 (_ (_ tptp.ord_less_eq_real (_ @t324 @t311)) (_ @t324 @t310))))) % 0.44/0.82 (define @t326 () (=> @t315 (=> @t325 (_ @t182 (_ @t324 @t252))))) % 0.44/0.82 (define @t327 () (_ @t324 @t66)) % 0.44/0.82 (define @t328 () (@list @t69 @t324 @t66 @t252)) % 0.44/0.82 (define @t329 () (=> @t304 (_ (_ tptp.ord_le1772180283um_c_c (_ @t299 @t62)) @t246))) % 0.44/0.82 (define @t330 () (_ @t247 @t60)) % 0.44/0.82 (define @t331 () (@list @t62 @t60 @t299 @t246)) % 0.44/0.82 (define @t332 () (=> @t320 (_ (_ tptp.ord_less_eq_real (_ @t319 @t62)) @t252))) % 0.44/0.82 (define @t333 () (@list @t62 @t60 @t319 @t252)) % 0.44/0.82 (define @t334 () (=> @t314 (_ (_ tptp.ord_le1772180283um_c_c (_ @t309 @t69)) @t246))) % 0.44/0.82 (define @t335 () (@list @t69 @t66 @t309 @t246)) % 0.44/0.82 (define @t336 () (=> @t325 (_ (_ tptp.ord_less_eq_real (_ @t324 @t69)) @t252))) % 0.44/0.82 (define @t337 () (@list @t69 @t66 @t324 @t252)) % 0.44/0.82 (define @t338 () (@var "X4" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t339 () (@var "Y6" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t340 () (_ tptp.ord_le1772180283um_c_c @t338)) % 0.44/0.82 (define @t341 () (@var "X4" tptp.real)) % 0.44/0.82 (define @t342 () (@var "Y6" tptp.real)) % 0.44/0.82 (define @t343 () (_ tptp.ord_less_eq_real @t341)) % 0.44/0.82 (define @t344 () (@var "Z" tptp.real)) % 0.44/0.82 (define @t345 () (@var "Y4" tptp.real)) % 0.44/0.82 (define @t346 () (lambda (@list @t345 @t344) (= @t345 @t344))) % 0.44/0.82 (define @t347 () (= @t255 @t267)) % 0.44/0.82 (define @t348 () (_ @t268 @t255)) % 0.44/0.82 (define @t349 () (_ @t256 @t267)) % 0.44/0.82 (define @t350 () (@list @t255 @t267)) % 0.44/0.82 (define @t351 () (not @t349)) % 0.44/0.82 (define @t352 () (=> @t305 @t248)) % 0.44/0.82 (define @t353 () (@list @t62 @t60 @t246)) % 0.44/0.82 (define @t354 () (=> @t315 @t253)) % 0.44/0.82 (define @t355 () (@list @t69 @t66 @t252)) % 0.44/0.82 (define @t356 () (@var "Z2" tptp.real)) % 0.44/0.82 (define @t357 () (_ tptp.ord_less_eq_real @t356)) % 0.44/0.82 (define @t358 () (_ @t357 @t255)) % 0.44/0.82 (define @t359 () (_ @t268 @t356)) % 0.44/0.82 (define @t360 () (_ @t357 @t267)) % 0.44/0.82 (define @t361 () (_ @t256 @t356)) % 0.44/0.82 (define @t362 () (@list @t255 @t267 @t356)) % 0.44/0.82 (define @t363 () (@var "A7" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t364 () (@var "B7" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t365 () (_ (_ tptp.ord_le1772180283um_c_c @t364) @t363)) % 0.44/0.82 (define @t366 () (_ (_ tptp.ord_le1772180283um_c_c @t363) @t364)) % 0.44/0.82 (define @t367 () (@list @t363 @t364)) % 0.44/0.82 (define @t368 () (@var "A7" tptp.real)) % 0.44/0.82 (define @t369 () (@var "B7" tptp.real)) % 0.44/0.82 (define @t370 () (_ (_ tptp.ord_less_eq_real @t369) @t368)) % 0.44/0.82 (define @t371 () (_ (_ tptp.ord_less_eq_real @t368) @t369)) % 0.44/0.82 (define @t372 () (@list @t368 @t369)) % 0.44/0.82 (define @t373 () (= @t62 @t60)) % 0.44/0.82 (define @t374 () (_ @t244 @t62)) % 0.44/0.82 (define @t375 () (@var "Z2" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t376 () (@var "P2" (-> tptp.real tptp.real Bool))) % 0.44/0.82 (define @t377 () (@var "B4" tptp.real)) % 0.44/0.82 (define @t378 () (@var "A4" tptp.real)) % 0.44/0.82 (define @t379 () (_ (_ @t376 @t378) @t377)) % 0.44/0.82 (define @t380 () (@list @t378 @t377)) % 0.44/0.82 (define @t381 () (_ tptp.ord_le1772180283um_c_c @t246)) % 0.44/0.82 (define @t382 () (_ @t381 @t62)) % 0.44/0.82 (define @t383 () (_ tptp.ord_less_eq_real @t252)) % 0.44/0.82 (define @t384 () (_ @t383 @t69)) % 0.44/0.82 (define @t385 () (_ (_ (_ tptp.denota69106024_a_b_c tptp.i) tptp.j) (_ tptp.static_SIGF_a_b_c tptp.p))) % 0.44/0.82 (define @t386 () (_ tptp.uminus_uminus_real @t255)) % 0.44/0.82 (define @t387 () (@var "A3" tptp.set_Su1783761653um_b_c)) % 0.44/0.82 (define @t388 () (@var "J3" tptp.denota231621370t_unit)) % 0.44/0.82 (define @t389 () (_ tptp.denota69106024_a_b_c @t13)) % 0.44/0.82 (define @t390 () (_ @t389 @t388)) % 0.44/0.82 (define @t391 () (@var "B3" tptp.set_Su1783761653um_b_c)) % 0.44/0.82 (define @t392 () (@var "V" tptp.set_Su1783761653um_b_c)) % 0.44/0.82 (define @t393 () (@var "A3" tptp.denota231621370t_unit)) % 0.44/0.82 (define @t394 () (@var "B3" tptp.denota231621370t_unit)) % 0.44/0.82 (define @t395 () (_ tptp.coinci772602909_a_b_c (_ (_ tptp.evolveODE_a_c_b tptp.ode) tptp.p))) % 0.44/0.82 (define @t396 () (@var "Y52" tptp.formula_a_b_c)) % 0.44/0.82 (define @t397 () (@var "X52" tptp.formula_a_b_c)) % 0.44/0.82 (define @t398 () (@var "Y51" tptp.oDE_a_c)) % 0.44/0.82 (define @t399 () (@var "X51" tptp.oDE_a_c)) % 0.44/0.82 (define @t400 () (_ (_ tptp.set_or656347191t_real tptp.zero_zero_real) tptp.t)) % 0.44/0.82 (define @t401 () (@var "__flatten_var_0" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t402 () (_ (_ tptp.denota1275485728_a_b_c tptp.i) tptp.ode)) % 0.44/0.82 (define @t403 () (lambda @t146 @t214)) % 0.44/0.82 (define @t404 () (lambda @t155 @t219)) % 0.44/0.82 (define @t405 () (lambda @t150 @t222)) % 0.44/0.82 (define @t406 () (_ @t51 @t143)) % 0.44/0.82 (define @t407 () (_ tptp.collec1643251106real_c (lambda @t146 (and @t145 @t406)))) % 0.44/0.82 (define @t408 () (_ @t137 @t152)) % 0.44/0.82 (define @t409 () (_ tptp.collect_Sum_sum_c_d (lambda @t155 (and @t154 @t408)))) % 0.44/0.82 (define @t410 () (_ tptp.collec230941376real_c (lambda @t160 (and @t159 @t191)))) % 0.44/0.82 (define @t411 () (_ tptp.collect_c (lambda @t165 (and @t164 @t194)))) % 0.44/0.82 (define @t412 () (_ tptp.collect_Sum_sum_c_c (lambda @t150 (and @t149 @t198)))) % 0.44/0.82 (define @t413 () (@list @t213)) % 0.44/0.82 (define @t414 () (@list @t218)) % 0.44/0.82 (define @t415 () (@var "A5" tptp.set_Fi1407883041real_c)) % 0.44/0.82 (define @t416 () (_ @t158 @t415)) % 0.44/0.82 (define @t417 () (@list @t415)) % 0.44/0.82 (define @t418 () (@var "A5" tptp.set_c)) % 0.44/0.82 (define @t419 () (_ @t163 @t418)) % 0.44/0.82 (define @t420 () (@list @t418)) % 0.44/0.82 (define @t421 () (@list @t202)) % 0.44/0.82 (define @t422 () (@var "Xb" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t423 () (@var "Xa" tptp.oDE_a_c)) % 0.44/0.82 (define @t424 () (@var "X3" tptp.denota231621370t_unit)) % 0.44/0.82 (define @t425 () (_ (_ tptp.set_or935154662um_c_c @t62) @t60)) % 0.44/0.82 (define @t426 () (_ (_ tptp.set_or656347191t_real @t69) @t66)) % 0.44/0.82 (define @t427 () (@var "U" tptp.produc190496183real_c)) % 0.44/0.82 (define @t428 () (@var "I4" tptp.produc190496183real_c)) % 0.44/0.82 (define @t429 () (_ tptp.ord_le850691415real_c @t428)) % 0.44/0.82 (define @t430 () (@var "L" tptp.produc190496183real_c)) % 0.44/0.82 (define @t431 () (_ tptp.member1895684704real_c @t428)) % 0.44/0.82 (define @t432 () (@var "U" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t433 () (@var "I4" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t434 () (_ tptp.ord_le1772180283um_c_c @t433)) % 0.44/0.82 (define @t435 () (@var "L" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t436 () (_ tptp.ord_le1772180283um_c_c @t435)) % 0.44/0.82 (define @t437 () (_ tptp.set_or935154662um_c_c @t435)) % 0.44/0.82 (define @t438 () (_ tptp.member2124950898um_c_c @t433)) % 0.44/0.82 (define @t439 () (@var "U" tptp.real)) % 0.44/0.82 (define @t440 () (@var "I4" tptp.real)) % 0.44/0.82 (define @t441 () (_ tptp.ord_less_eq_real @t440)) % 0.44/0.82 (define @t442 () (@var "L" tptp.real)) % 0.44/0.82 (define @t443 () (_ tptp.ord_less_eq_real @t442)) % 0.44/0.82 (define @t444 () (_ tptp.set_or656347191t_real @t442)) % 0.44/0.82 (define @t445 () (_ tptp.member_real @t440)) % 0.44/0.82 (define @t446 () (@var "H2" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t447 () (@var "L2" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t448 () (_ tptp.ord_le1772180283um_c_c @t447)) % 0.44/0.82 (define @t449 () (@var "H" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t450 () (not (_ @t436 @t449))) % 0.44/0.82 (define @t451 () (_ @t437 @t449)) % 0.44/0.82 (define @t452 () (@var "H2" tptp.real)) % 0.44/0.82 (define @t453 () (@var "L2" tptp.real)) % 0.44/0.82 (define @t454 () (_ tptp.ord_less_eq_real @t453)) % 0.44/0.82 (define @t455 () (@var "H" tptp.real)) % 0.44/0.82 (define @t456 () (not (_ @t443 @t455))) % 0.44/0.82 (define @t457 () (_ (_ tptp.set_or656347191t_real @t453) @t452)) % 0.44/0.82 (define @t458 () (_ @t444 @t455)) % 0.44/0.82 (define @t459 () (@var "S2" tptp.set_Pr1389752855real_c)) % 0.44/0.82 (define @t460 () (@var "R2" tptp.set_Pr1389752855real_c)) % 0.44/0.82 (define @t461 () (_ (_ tptp.ord_le977353143real_c @t460) @t459)) % 0.44/0.82 (define @t462 () (@list @t460 @t459)) % 0.44/0.82 (define @t463 () (@var "S2" tptp.set_Sum_sum_c_d)) % 0.44/0.82 (define @t464 () (@var "R2" tptp.set_Sum_sum_c_d)) % 0.44/0.82 (define @t465 () (@var "S2" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t466 () (@var "R2" tptp.set_Sum_sum_c_c)) % 0.44/0.82 (define @t467 () (_ tptp.topolo1830106092n_real @t255)) % 0.44/0.82 (define @t468 () (@var "S" tptp.set_Pr1389752855real_c)) % 0.44/0.82 (define @t469 () (@var "R3" tptp.set_Pr1389752855real_c)) % 0.44/0.82 (define @t470 () (_ tptp.member1895684704real_c @t48)) % 0.44/0.82 (define @t471 () (@var "Y6" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t472 () (_ tptp.member1895684704real_c (_ (_ tptp.produc394644079real_c @t157) @t471))) % 0.44/0.82 (define @t473 () (@list @t157 @t471)) % 0.44/0.82 (define @t474 () (lambda @t473 (_ @t472 @t459))) % 0.44/0.82 (define @t475 () (lambda @t473 (_ @t472 @t460))) % 0.44/0.82 (define @t476 () (@var "S" tptp.set_real)) % 0.44/0.82 (define @t477 () (_ @t467 @t476)) % 0.44/0.82 (define @t478 () (@var "G2" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t479 () (@var "F2" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t480 () (@var "G" (-> tptp.real tptp.finite1398487019real_c))) % 0.44/0.82 (define @t481 () (@var "F" (-> tptp.real tptp.finite1398487019real_c))) % 0.44/0.82 (define @t482 () (_ @t481 @t341)) % 0.44/0.82 (define @t483 () (@list @t341)) % 0.44/0.82 (define @t484 () (_ tptp.has_ve1904308670real_c @t480)) % 0.44/0.82 (define @t485 () (_ tptp.has_ve1904308670real_c @t481)) % 0.44/0.82 (define @t486 () (_ @t485 @t479)) % 0.44/0.82 (define @t487 () (@var "Net" tptp.filter_real)) % 0.44/0.82 (define @t488 () (@var "F2" tptp.real)) % 0.44/0.82 (define @t489 () (@var "T2" tptp.set_real)) % 0.44/0.82 (define @t490 () (_ @t467 @t489)) % 0.44/0.82 (define @t491 () (@var "S2" tptp.set_real)) % 0.44/0.82 (define @t492 () (_ (_ tptp.ord_less_eq_set_real @t489) @t491)) % 0.44/0.82 (define @t493 () (_ @t467 @t491)) % 0.44/0.82 (define @t494 () (@var "D2" tptp.finite1398487019real_c)) % 0.44/0.82 (define @t495 () (_ (_ tptp.ord_less_eq_set_real @t491) @t489)) % 0.44/0.82 (define @t496 () (_ tptp.member_real @t255)) % 0.44/0.82 (define @t497 () (@var "Y7" tptp.set_Fi1407883041real_c)) % 0.44/0.83 (define @t498 () (@var "F" (-> tptp.real tptp.finite1398487019real_c tptp.finite1398487019real_c))) % 0.44/0.83 (define @t499 () (@var "X3" (-> tptp.real tptp.finite1398487019real_c))) % 0.44/0.83 (define @t500 () (_ (_ tptp.initia1631504802real_c @t499) @t498)) % 0.44/0.83 (define @t501 () (_ @t500 @t489)) % 0.44/0.83 (define @t502 () (_ @t501 @t497)) % 0.44/0.83 (define @t503 () (@var "X6" tptp.set_Fi1407883041real_c)) % 0.44/0.83 (define @t504 () (_ @t501 @t503)) % 0.44/0.83 (define @t505 () (@list @t499 @t498 @t489 @t503 @t497)) % 0.44/0.83 (define @t506 () (_ @t500 @t491)) % 0.44/0.83 (define @t507 () (@var "T3" tptp.set_real)) % 0.44/0.83 (define @t508 () (@var "B" tptp.produc190496183real_c)) % 0.44/0.83 (define @t509 () (_ tptp.ord_le1327118209real_c @t156)) % 0.44/0.83 (define @t510 () (_ tptp.ord_less_eq_set_c @t161)) % 0.44/0.83 (define @t511 () (_ @t144 @t104)) % 0.44/0.83 (define @t512 () (_ tptp.ord_le977353143real_c @t104)) % 0.44/0.83 (define @t513 () (_ @t512 @t74)) % 0.44/0.83 (define @t514 () (_ @t153 @t111)) % 0.44/0.83 (define @t515 () (_ tptp.ord_le764260924um_c_d @t111)) % 0.44/0.83 (define @t516 () (_ @t515 @t81)) % 0.44/0.83 (define @t517 () (@var "B3" tptp.set_Fi1407883041real_c)) % 0.44/0.83 (define @t518 () (_ @t158 @t517)) % 0.44/0.83 (define @t519 () (_ tptp.ord_le1327118209real_c @t517)) % 0.44/0.83 (define @t520 () (_ @t519 @t156)) % 0.44/0.83 (define @t521 () (@var "B3" tptp.set_c)) % 0.44/0.83 (define @t522 () (_ @t163 @t521)) % 0.44/0.83 (define @t523 () (_ tptp.ord_less_eq_set_c @t521)) % 0.44/0.83 (define @t524 () (_ @t523 @t161)) % 0.44/0.83 (define @t525 () (_ @t148 @t95)) % 0.44/0.83 (define @t526 () (@var "Q" (-> tptp.produc190496183real_c Bool))) % 0.44/0.83 (define @t527 () (@var "Q" (-> tptp.sum_sum_c_d Bool))) % 0.44/0.83 (define @t528 () (_ tptp.member_c @t174)) % 0.44/0.83 (define @t529 () (@var "X6" tptp.set_Pr1389752855real_c)) % 0.44/0.83 (define @t530 () (_ tptp.collec1643251106real_c (lambda @t146 (and (_ @t144 @t529) @t406)))) % 0.44/0.83 (define @t531 () (@var "Z3" tptp.set_Pr1389752855real_c)) % 0.44/0.83 (define @t532 () (@var "X6" tptp.set_Sum_sum_c_d)) % 0.44/0.83 (define @t533 () (_ tptp.collect_Sum_sum_c_d (lambda @t155 (and (_ @t153 @t532) @t408)))) % 0.44/0.83 (define @t534 () (@var "Z3" tptp.set_Sum_sum_c_d)) % 0.44/0.83 (define @t535 () (_ tptp.collec230941376real_c (lambda @t160 (and (_ @t158 @t503) @t191)))) % 0.44/0.83 (define @t536 () (@var "Z3" tptp.set_Fi1407883041real_c)) % 0.44/0.83 (define @t537 () (@var "X3" tptp.c)) % 0.44/0.83 (define @t538 () (@var "X6" tptp.set_c)) % 0.44/0.83 (define @t539 () (_ tptp.collect_c (lambda @t165 (and (_ @t163 @t538) @t194)))) % 0.44/0.83 (define @t540 () (@var "Z3" tptp.set_c)) % 0.44/0.83 (define @t541 () (_ tptp.member_c @t537)) % 0.44/0.83 (define @t542 () (@var "X6" tptp.set_Sum_sum_c_c)) % 0.44/0.83 (define @t543 () (_ tptp.collect_Sum_sum_c_c (lambda @t150 (and (_ @t148 @t542) @t198)))) % 0.44/0.83 (define @t544 () (@var "Z3" tptp.set_Sum_sum_c_c)) % 0.44/0.83 (define @t545 () (@var "S3" tptp.finite1398487019real_c)) % 0.44/0.83 (define @t546 () (@var "R3" tptp.finite1398487019real_c)) % 0.44/0.83 (define @t547 () (_ tptp.produc394644079real_c @t546)) % 0.44/0.83 (define @t548 () (@var "S" tptp.finite1398487019real_c)) % 0.44/0.83 (define @t549 () (@var "P" tptp.formula_a_b_c)) % 0.44/0.83 (define @t550 () (_ tptp.osafe_a_c @t12)) % 0.44/0.83 (define @t551 () (_ tptp.evolveODE_a_c_b @t12)) % 0.44/0.83 (define @t552 () (@var "P2" tptp.formula_a_b_c)) % 0.44/0.83 (define @t553 () (_ tptp.ord_le657554289um_c_c @t451)) % 0.44/0.83 (define @t554 () (_ tptp.ord_less_eq_set_real @t458)) % 0.44/0.83 (define @t555 () (@var "K" tptp.produc190496183real_c)) % 0.44/0.83 (define @t556 () (@list @t428 @t555)) % 0.44/0.83 (define @t557 () (@var "K" tptp.set_Sum_sum_c_c)) % 0.44/0.83 (define @t558 () (@list @t433 @t557)) % 0.44/0.83 (define @t559 () (@var "K" tptp.real)) % 0.44/0.83 (define @t560 () (@list @t440 @t559)) % 0.44/0.83 (define @t561 () (_ tptp.set_ord_atMost_real @t255)) % 0.44/0.83 (define @t562 () (_ tptp.set_ord_atLeast_real @t255)) % 0.44/0.83 (define @t563 () (_ tptp.image_real_real tptp.uminus_uminus_real)) % 0.44/0.83 (define @t564 () (@var "F" (-> tptp.c tptp.sum_sum_c_c))) % 0.44/0.83 (define @t565 () (_ tptp.image_c_Sum_sum_c_c @t564)) % 0.44/0.83 (define @t566 () (_ @t565 @t161)) % 0.44/0.83 (define @t567 () (@var "B" tptp.sum_sum_c_c)) % 0.44/0.83 (define @t568 () (_ tptp.member_Sum_sum_c_c @t567)) % 0.44/0.83 (define @t569 () (_ @t541 @t161)) % 0.44/0.83 (define @t570 () (_ @t564 @t537)) % 0.44/0.83 (define @t571 () (@var "F" (-> tptp.c tptp.sum_sum_c_d))) % 0.44/0.83 (define @t572 () (_ tptp.image_c_Sum_sum_c_d @t571)) % 0.44/0.83 (define @t573 () (_ @t572 @t161)) % 0.44/0.83 (define @t574 () (@var "B" tptp.sum_sum_c_d)) % 0.44/0.83 (define @t575 () (_ tptp.member_Sum_sum_c_d @t574)) % 0.44/0.83 (define @t576 () (_ @t571 @t537)) % 0.44/0.83 (define @t577 () (@var "F" (-> tptp.sum_sum_c_c tptp.sum_sum_c_c))) % 0.44/0.83 (define @t578 () (_ tptp.image_666880337um_c_c @t577)) % 0.44/0.83 (define @t579 () (_ @t578 @t44)) % 0.44/0.83 (define @t580 () (_ @t577 @t229)) % 0.44/0.83 (define @t581 () (@var "F" (-> tptp.sum_sum_c_c tptp.sum_sum_c_d))) % 0.44/0.83 (define @t582 () (_ (_ tptp.image_675141842um_c_d @t581) @t44)) % 0.44/0.83 (define @t583 () (_ @t581 @t229)) % 0.44/0.83 (define @t584 () (@var "F" (-> tptp.sum_sum_c_d tptp.sum_sum_c_c))) % 0.44/0.83 (define @t585 () (_ (_ tptp.image_1558941394um_c_c @t584) @t81)) % 0.44/0.83 (define @t586 () (_ @t584 @t226)) % 0.44/0.83 (define @t587 () (@var "F" (-> tptp.sum_sum_c_d tptp.sum_sum_c_d))) % 0.44/0.83 (define @t588 () (_ (_ tptp.image_1567202899um_c_d @t587) @t81)) % 0.44/0.83 (define @t589 () (_ @t587 @t226)) % 0.44/0.83 (define @t590 () (@var "F" (-> tptp.produc190496183real_c tptp.sum_sum_c_c))) % 0.44/0.83 (define @t591 () (_ (_ tptp.image_1467045143um_c_c @t590) @t74)) % 0.44/0.83 (define @t592 () (_ @t590 @t223)) % 0.44/0.83 (define @t593 () (@var "F" (-> tptp.produc190496183real_c tptp.sum_sum_c_d))) % 0.44/0.83 (define @t594 () (_ (_ tptp.image_1475306648um_c_d @t593) @t74)) % 0.44/0.83 (define @t595 () (_ @t593 @t223)) % 0.44/0.83 (define @t596 () (@var "F" (-> tptp.sum_sum_c_c tptp.produc190496183real_c))) % 0.44/0.83 (define @t597 () (_ (_ tptp.image_1146069259real_c @t596) @t44)) % 0.44/0.83 (define @t598 () (_ tptp.member1895684704real_c @t508)) % 0.44/0.83 (define @t599 () (_ @t596 @t229)) % 0.44/0.83 (define @t600 () (@var "F" (-> tptp.sum_sum_c_d tptp.produc190496183real_c))) % 0.44/0.83 (define @t601 () (_ (_ tptp.image_1980705354real_c @t600) @t81)) % 0.44/0.83 (define @t602 () (_ @t600 @t226)) % 0.44/0.83 (define @t603 () (@var "AA" tptp.set_c)) % 0.44/0.83 (define @t604 () (_ (_ tptp.ord_less_eq_set_c @t603) @t161)) % 0.44/0.83 (define @t605 () (@list @t603)) % 0.44/0.83 (define @t606 () (_ @t515 @t573)) % 0.44/0.83 (define @t607 () (@list @t111 @t571 @t161)) % 0.44/0.83 (define @t608 () (_ @t100 @t566)) % 0.44/0.83 (define @t609 () (@list @t95 @t564 @t161)) % 0.44/0.83 (define @t610 () (@var "AA" tptp.set_Sum_sum_c_c)) % 0.44/0.83 (define @t611 () (_ @t100 @t579)) % 0.44/0.83 (define @t612 () (@list @t95 @t577 @t44)) % 0.44/0.83 (define @t613 () (_ @t571 @t162)) % 0.44/0.83 (define @t614 () (_ tptp.ord_le764260924um_c_d @t573)) % 0.44/0.83 (define @t615 () (_ @t614 @t111)) % 0.44/0.83 (define @t616 () (_ @t564 @t162)) % 0.44/0.83 (define @t617 () (_ tptp.ord_le1772180283um_c_c @t566)) % 0.44/0.83 (define @t618 () (_ @t617 @t95)) % 0.44/0.83 (define @t619 () (@var "C3" tptp.set_c)) % 0.44/0.83 (define @t620 () (_ (_ tptp.ord_less_eq_set_c @t619) @t161)) % 0.44/0.83 (define @t621 () (@list @t619)) % 0.44/0.83 (define @t622 () (@var "C3" tptp.set_Sum_sum_c_c)) % 0.44/0.83 (define @t623 () (_ @t571 @t174)) % 0.44/0.83 (define @t624 () (_ @t528 @t161)) % 0.44/0.83 (define @t625 () (_ @t564 @t174)) % 0.44/0.83 (define @t626 () (_ tptp.ord_le1772180283um_c_c @t579)) % 0.44/0.83 (define @t627 () (_ @t510 @t521)) % 0.44/0.83 (define @t628 () (@var "Z2" tptp.sum_sum_c_c)) % 0.44/0.83 (define @t629 () (@var "Z2" tptp.sum_sum_c_d)) % 0.44/0.83 (define @t630 () (@var "X7" tptp.sum_sum_c_c)) % 0.44/0.83 (define @t631 () (@var "X7" tptp.sum_sum_c_d)) % 0.44/0.83 (define @t632 () (@var "N" tptp.set_c)) % 0.44/0.83 (define @t633 () (@var "G" (-> tptp.c tptp.sum_sum_c_c))) % 0.44/0.83 (define @t634 () (@var "M" tptp.set_c)) % 0.44/0.83 (define @t635 () (_ @t528 @t632)) % 0.44/0.83 (define @t636 () (= @t634 @t632)) % 0.44/0.83 (define @t637 () (@var "G" (-> tptp.c tptp.sum_sum_c_d))) % 0.44/0.83 (define @t638 () (_ tptp.static_FVO_a_c tptp.ode)) % 0.44/0.83 (define @t639 () (_ tptp.image_c_Sum_sum_c_c tptp.sum_Inl_c_c)) % 0.44/0.83 (define @t640 () (@var "Uu" tptp.c)) % 0.44/0.83 (define @t641 () (_ tptp.member_Sum_sum_c_c (_ tptp.sum_Inl_c_c @t640))) % 0.44/0.83 (define @t642 () (_ tptp.oDE_dom_a_c tptp.ode)) % 0.44/0.83 (define @t643 () (not @t7)) % 0.44/0.83 (define @t644 () (@var "T" tptp.produc190496183real_c)) % 0.44/0.83 (define @t645 () (_ tptp.member1895684704real_c @t644)) % 0.44/0.83 (define @t646 () (lambda @t215 (forall (@list @t644) (=> (_ @t645 @t213) (_ @t645 @t211))))) % 0.44/0.83 (define @t647 () (@var "T" tptp.sum_sum_c_d)) % 0.44/0.83 (define @t648 () (_ tptp.member_Sum_sum_c_d @t647)) % 0.44/0.83 (define @t649 () (lambda @t220 (forall (@list @t647) (=> (_ @t648 @t218) (_ @t648 @t216))))) % 0.44/0.83 (define @t650 () (@var "T" tptp.sum_sum_c_c)) % 0.44/0.83 (define @t651 () (_ tptp.member_Sum_sum_c_c @t650)) % 0.44/0.83 (define @t652 () (lambda @t204 (forall (@list @t650) (=> (_ @t651 @t202) (_ @t651 @t203))))) % 0.44/0.83 (define @t653 () (@var "J" tptp.finite1398487019real_c)) % 0.44/0.83 (define @t654 () (@var "As" (-> tptp.finite1398487019real_c tptp.set_Sum_sum_c_c))) % 0.44/0.83 (define @t655 () (@var "I2" tptp.finite1398487019real_c)) % 0.44/0.83 (define @t656 () (@var "R" tptp.set_Pr1389752855real_c)) % 0.44/0.83 (define @t657 () (_ (_ tptp.member1895684704real_c (_ (_ tptp.produc394644079real_c @t655) @t653)) @t656)) % 0.44/0.83 (define @t658 () (@list @t655 @t653)) % 0.44/0.83 (define @t659 () (lambda (@list @t656 @t654) (forall @t658 (=> @t657 (_ (_ tptp.ord_le1772180283um_c_c (_ @t654 @t655)) (_ @t654 @t653)))))) % 0.44/0.83 (define @t660 () (@var "As" (-> tptp.finite1398487019real_c tptp.real))) % 0.44/0.83 (define @t661 () (lambda (@list @t656 @t660) (forall @t658 (=> @t657 (_ (_ tptp.ord_less_eq_real (_ @t660 @t655)) (_ @t660 @t653)))))) % 0.44/0.83 (define @t662 () (@var "Phi" tptp.formula_a_b_c)) % 0.44/0.83 (define @t663 () (@var "J2" tptp.denota231621370t_unit)) % 0.44/0.83 (define @t664 () (@var "Nu4" tptp.produc190496183real_c)) % 0.44/0.83 (define @t665 () (@var "I3" tptp.denota231621370t_unit)) % 0.44/0.83 (define @t666 () (@var "Nu3" tptp.produc190496183real_c)) % 0.44/0.83 (define @t667 () (lambda (@list @t662) (forall (@list @t666 @t664 @t665 @t663) (=> (_ (_ (_ tptp.denota69106024_a_b_c @t665) @t663) (_ tptp.static_SIGF_a_b_c @t662)) (=> (_ (_ (_ tptp.denota1997846518gree_c @t666) @t664) (_ tptp.static_FVF_a_b_c @t662)) (= (_ (_ tptp.member1895684704real_c @t666) (_ (_ tptp.denota968303861_a_b_c @t665) @t662)) (_ (_ tptp.member1895684704real_c @t664) (_ (_ tptp.denota968303861_a_b_c @t663) @t662)))))))) % 0.44/0.83 (define @t668 () (@var "Alpha" tptp.hp_a_b_c)) % 0.44/0.83 (define @t669 () (lambda (@list @t668) (forall (@list @t665 @t663) (and (_ (_ (_ tptp.coinci354700372_a_b_c @t668) @t665) @t663) (_ (_ tptp.coinci772602909_a_b_c @t668) @t665))))) % 0.44/0.83 (define @t670 () (lambda @t413 (_ tptp.collec1643251106real_c (lambda @t146 (not @t214))))) % 0.44/0.83 (define @t671 () (lambda @t414 (_ tptp.collect_Sum_sum_c_d (lambda @t155 (not @t219))))) % 0.44/0.83 (define @t672 () (lambda @t417 (_ tptp.collec230941376real_c (lambda @t160 (not @t416))))) % 0.44/0.83 (define @t673 () (lambda @t420 (_ tptp.collect_c (lambda @t165 (not @t419))))) % 0.44/0.83 (define @t674 () (lambda @t421 (_ tptp.collect_Sum_sum_c_c (lambda @t150 (not @t222))))) % 0.44/0.83 (define @t675 () (@var "Sol2" tptp.finite1398487019real_c)) % 0.44/0.83 (define @t676 () (@var "ODE2" tptp.oDE_a_c)) % 0.44/0.83 (define @t677 () (_ tptp.produc394644079real_c @t675)) % 0.44/0.83 (define @t678 () (_ @t677 (_ (_ (_ tptp.denota1275485728_a_b_c @t665) @t676) @t675))) % 0.44/0.83 (define @t679 () (lambda (@list @t665 @t676 @t675) @t678)) % 0.44/0.83 (define @t680 () (_ (_ tptp.denota1293057250_a_b_c @t665) @t676)) % 0.44/0.83 (define @t681 () (@var "Omega3" tptp.produc190496183real_c)) % 0.44/0.83 (define @t682 () (_ tptp.denota1997846518gree_c @t681)) % 0.44/0.83 (define @t683 () (_ @t682 @t666)) % 0.44/0.83 (define @t684 () (and (_ @t683 (_ tptp.uminus1381786404um_c_c @t680)) (_ (_ @t682 (_ (_ (_ tptp.denota1896987029_a_b_c @t665) @t676) @t675)) @t680))) % 0.44/0.83 (define @t685 () (@list @t681)) % 0.44/0.83 (define @t686 () (lambda @t685 @t684)) % 0.44/0.83 (define @t687 () (@list @t665 @t676 @t666 @t675)) % 0.44/0.83 (define @t688 () (lambda @t687 (_ tptp.the_Pr1290640446real_c @t686))) % 0.44/0.83 (define @t689 () (@var "L3" tptp.finite1398487019real_c)) % 0.44/0.83 (define @t690 () (lambda (@list @t689) (_ tptp.collec230941376real_c (_ tptp.ord_le775706699real_c @t689)))) % 0.44/0.83 (define @t691 () (@var "L3" tptp.set_Sum_sum_c_c)) % 0.44/0.83 (define @t692 () (lambda (@list @t691) (_ tptp.collec95329456um_c_c (_ tptp.ord_le1772180283um_c_c @t691)))) % 0.44/0.83 (define @t693 () (@var "L3" tptp.real)) % 0.44/0.83 (define @t694 () (lambda (@list @t693) (_ tptp.collect_real (_ tptp.ord_less_eq_real @t693)))) % 0.44/0.83 (define @t695 () (@var "U2" tptp.finite1398487019real_c)) % 0.44/0.83 (define @t696 () (lambda (@list @t695) (_ tptp.collec230941376real_c (lambda @t160 (_ (_ tptp.ord_le775706699real_c @t157) @t695))))) % 0.44/0.83 (define @t697 () (@var "U2" tptp.set_Sum_sum_c_c)) % 0.44/0.83 (define @t698 () (lambda (@list @t697) (_ tptp.collec95329456um_c_c (lambda (@list @t338) (_ @t340 @t697))))) % 0.44/0.83 (define @t699 () (@var "U2" tptp.real)) % 0.44/0.83 (define @t700 () (lambda (@list @t699) (_ tptp.collect_real (lambda @t483 (_ @t343 @t699))))) % 0.44/0.83 (define @t701 () (_ tptp.denota1275485728_a_b_c tptp.j)) % 0.44/0.83 (define @t702 () (_ @t701 tptp.ode)) % 0.44/0.83 (define @t703 () (_ (_ tptp.produc394644079real_c @t3) (_ @t702 @t3))) % 0.44/0.83 (define @t704 () (_ @t677 (_ @t702 @t675))) % 0.44/0.83 (define @t705 () (@list @t675)) % 0.44/0.83 (define @t706 () (lambda @t705 @t704)) % 0.44/0.83 (define @t707 () (_ @t677 (_ (_ @t701 @t676) @t675))) % 0.44/0.83 (define @t708 () (@list @t676 @t675)) % 0.44/0.83 (define @t709 () (lambda @t708 @t707)) % 0.44/0.83 (define @t710 () (_ @t679 tptp.j)) % 0.44/0.83 (define @t711 () (_ tptp.collect_Sum_sum_c_c (lambda @t150 (not (_ @t148 @t2))))) % 0.44/0.83 (define @t712 () (_ (_ @t682 @t4) @t711)) % 0.44/0.83 (define @t713 () (_ (_ @t682 @t704) @t2)) % 0.44/0.83 (define @t714 () (lambda @t705 (_ tptp.the_Pr1290640446real_c (lambda @t685 (and @t712 @t713))))) % 0.44/0.83 (define @t715 () (lambda (@list @t666 @t675) (_ tptp.the_Pr1290640446real_c (lambda @t685 (and (_ @t683 @t711) @t713))))) % 0.44/0.83 (define @t716 () (_ @t1 @t676)) % 0.44/0.83 (define @t717 () (lambda (@list @t676 @t666 @t675) (_ tptp.the_Pr1290640446real_c (lambda @t685 (and (_ @t683 (_ tptp.collect_Sum_sum_c_c (lambda @t150 (not (_ @t148 @t716))))) (_ (_ @t682 @t707) @t716)))))) % 0.44/0.83 (define @t718 () (_ tptp.collect_Sum_sum_c_c (lambda @t150 (not (_ @t148 @t680))))) % 0.44/0.83 (define @t719 () (_ (lambda @t687 (_ tptp.the_Pr1290640446real_c (lambda @t685 (and (_ @t683 @t718) (_ (_ @t682 @t678) @t680))))) tptp.j)) % 0.44/0.83 (define @t720 () (lambda @t705 @t678)) % 0.44/0.83 (define @t721 () (lambda @t708 @t678)) % 0.44/0.83 (define @t722 () (_ @t679 @t665)) % 0.44/0.83 (define @t723 () (_ @t674 @t680)) % 0.44/0.83 (define @t724 () (and (_ @t683 @t723) (_ (_ @t682 (_ (_ @t722 @t676) @t675)) @t680))) % 0.44/0.83 (assume @p1 (_ tptp.osafe_a_c tptp.ode)) % 0.44/0.83 (assume @p2 (and (_ (_ @t6 @t4) @t8) @t7)) % 0.44/0.83 (assume @p3 (forall @t11 (_ (_ (_ tptp.denota1997846518gree_c (_ @t5 @t10)) @t4) @t8))) % 0.44/0.83 (assume @p4 (forall (@list @t13 @t12 @t17 @t15) (and (_ (_ @t18 @t17) @t19) (_ (_ @t18 @t16) @t14)))) % 0.44/0.83 (assume @p5 (forall (@list @t23 @t21 @t22 @t20) (= (= (_ (_ tptp.produc394644079real_c @t23) @t21) (_ (_ tptp.produc394644079real_c @t22) @t20)) (and (= @t23 @t22) (= @t21 @t20))))) % 0.44/0.83 (assume @p6 (forall @t32 (= @t31 (and @t29 @t26)))) % 0.44/0.83 (assume @p7 (forall (@list @t17 @t13 @t12 @t15) (exists (@list @t33) (and (_ (_ @t34 @t17) @t19) (_ (_ @t34 @t16) @t14))))) % 0.44/0.83 (assume @p8 (_ @t36 tptp.v)) % 0.44/0.83 (assume @p9 (forall @t11 (_ (_ @t39 (_ (_ (_ tptp.denota1896987029_a_b_c tptp.i) tptp.ode) @t10)) @t37))) % 0.44/0.83 (assume @p10 (_ @t36 @t40)) % 0.44/0.83 (assume @p11 (forall (@list @t42 @t43 @t41) (=> (_ (_ (_ tptp.denota1997846518gree_c @t42) @t43) @t41) (_ (_ (_ tptp.denota1997846518gree_c @t43) @t42) @t41)))) % 0.44/0.83 (assume @p12 (forall (@list @t17 @t44) (_ (_ @t45 @t17) @t44))) % 0.44/0.83 (assume @p13 (forall @t11 (_ (_ @t39 @t35) (_ tptp.uminus1381786404um_c_c @t37)))) % 0.44/0.83 (assume @p14 (forall (@list @t49) (exists @t50 (= @t49 @t48)))) % 0.44/0.83 (assume @p15 (forall (@list @t51 @t49) (=> @t56 (_ @t51 @t49)))) % 0.44/0.83 (assume @p16 (_ (_ tptp.ord_le1772180283um_c_c @t40) tptp.v)) % 0.44/0.83 (assume @p17 (= (_ (_ tptp.produc394644079real_c tptp.ab) tptp.bb) (_ @t38 (_ tptp.sol tptp.t)))) % 0.44/0.83 (assume @p18 (forall (@list @t51 @t57) (=> @t56 (_ @t51 @t57)))) % 0.44/0.83 (assume @p19 (forall (@list @t58) (not (forall @t55 (not (= @t58 @t54)))))) % 0.44/0.83 (assume @p20 (forall @t32 (=> @t31 (not (=> @t29 (not @t26)))))) % 0.44/0.83 (assume @p21 (_ @t59 tptp.v)) % 0.44/0.83 (assume @p22 (_ @t59 @t40)) % 0.44/0.83 (assume @p23 (forall (@list @t28 @t25) (= (_ tptp.uminus17964590real_c @t30) (_ (_ tptp.produc394644079real_c (_ tptp.uminus1737280820real_c @t28)) (_ tptp.uminus1737280820real_c @t25))))) % 0.44/0.83 (assume @p24 (forall @t65 (= (_ tptp.uminus1225118734um_c_c @t64) (_ (_ tptp.produc1439061071um_c_c @t63) @t61)))) % 0.44/0.83 (assume @p25 (forall (@list @t62 @t66) (= (_ tptp.uminus125610847c_real @t68) (_ (_ tptp.produc1528874528c_real @t63) @t67)))) % 0.44/0.83 (assume @p26 (forall (@list @t69 @t60) (= (_ tptp.uminus1629073887um_c_c @t71) (_ (_ tptp.produc1186709024um_c_c @t70) @t61)))) % 0.44/0.83 (assume @p27 (forall @t73 (= (_ tptp.uminus856758960l_real @t72) (_ (_ tptp.produc705216881l_real @t70) @t67)))) % 0.44/0.83 (assume @p28 (forall @t80 (=> @t79 @t77))) % 0.44/0.83 (assume @p29 (forall @t87 (=> @t86 @t84))) % 0.44/0.83 (assume @p30 (forall @t94 (=> @t93 @t91))) % 0.44/0.83 (assume @p31 (forall @t80 (= @t77 @t79))) % 0.44/0.83 (assume @p32 (forall @t87 (= @t84 @t86))) % 0.44/0.83 (assume @p33 (forall @t94 (= @t91 @t93))) % 0.44/0.83 (assume @p34 (forall @t98 (= (= @t88 @t97) @t96))) % 0.44/0.83 (assume @p35 (forall (@list @t66) (= (_ tptp.uminus_uminus_real @t67) @t66))) % 0.44/0.83 (assume @p36 (forall @t99 (= (_ tptp.uminus_uminus_real @t70) @t69))) % 0.44/0.83 (assume @p37 (forall @t98 (=> @t103 (=> @t101 @t96)))) % 0.44/0.83 (assume @p38 (forall (@list @t74 @t104) (=> (forall @t110 (=> @t109 @t108)) @t105))) % 0.44/0.83 (assume @p39 (forall (@list @t81 @t111) (=> (forall @t117 (=> @t116 @t115)) @t112))) % 0.44/0.83 (assume @p40 (forall @t98 (=> (forall @t122 (=> @t121 @t120)) @t103))) % 0.44/0.83 (assume @p41 (forall @t128 (= (= @t127 @t126) @t125))) % 0.44/0.83 (assume @p42 (forall @t129 (= (_ tptp.uminus1381786404um_c_c @t127) @t124))) % 0.44/0.83 (assume @p43 (forall @t73 (= @t131 @t130))) % 0.44/0.83 (assume @p44 (forall (@list @t132 @t51) (= (_ (_ tptp.member1895684704real_c @t132) (_ tptp.collec1643251106real_c @t51)) (_ @t51 @t132)))) % 0.44/0.83 (assume @p45 (forall (@list @t133 @t134) (= (_ (_ tptp.member_Sum_sum_c_c @t133) @t135) (_ @t134 @t133)))) % 0.44/0.83 (assume @p46 (forall (@list @t136 @t137) (= (_ (_ tptp.member_Sum_sum_c_d @t136) (_ tptp.collect_Sum_sum_c_d @t137)) (_ @t137 @t136)))) % 0.44/0.83 (assume @p47 (forall (@list @t28 @t138) (= (_ (_ tptp.member1261661570real_c @t28) @t139) (_ @t138 @t28)))) % 0.44/0.83 (assume @p48 (forall (@list @t140 @t141) (= (_ (_ tptp.member_c @t140) @t142) (_ @t141 @t140)))) % 0.44/0.83 (assume @p49 (forall (@list @t74) (= (_ tptp.collec1643251106real_c (lambda @t146 @t145)) @t74))) % 0.44/0.83 (assume @p50 (forall @t151 (= (_ tptp.collect_Sum_sum_c_c (lambda @t150 @t149)) @t44))) % 0.44/0.83 (assume @p51 (forall (@list @t81) (= (_ tptp.collect_Sum_sum_c_d (lambda @t155 @t154)) @t81))) % 0.44/0.83 (assume @p52 (forall (@list @t156) (= (_ tptp.collec230941376real_c (lambda @t160 @t159)) @t156))) % 0.44/0.83 (assume @p53 (forall (@list @t161) (= (_ tptp.collect_c (lambda @t165 @t164)) @t161))) % 0.44/0.83 (assume @p54 (forall @t171 (=> (forall @t170 (= @t169 @t168)) (= @t139 @t167)))) % 0.44/0.83 (assume @p55 (forall @t178 (=> (forall @t177 (= @t176 @t175)) (= @t142 @t173)))) % 0.44/0.83 (assume @p56 (forall @t128 (= (_ @t181 @t126) @t180))) % 0.44/0.83 (assume @p57 (forall @t186 (= @t185 @t183))) % 0.44/0.83 (assume @p58 (forall @t98 (= (_ (_ tptp.ord_le1772180283um_c_c @t88) @t97) @t101))) % 0.44/0.83 (assume @p59 (forall @t98 (=> @t103 (_ (_ tptp.ord_le1772180283um_c_c @t97) @t88)))) % 0.44/0.83 (assume @p60 (forall @t73 (or @t130 @t189 (not @t188)))) % 0.44/0.83 (assume @p61 (forall @t171 (= @t192 (forall @t160 (=> @t191 @t190))))) % 0.44/0.83 (assume @p62 (forall @t178 (= @t195 (forall @t165 (=> @t194 @t193))))) % 0.44/0.83 (assume @p63 (forall @t201 (= @t200 (forall @t150 (=> @t198 @t197))))) % 0.44/0.83 (assume @p64 (= @t207 (lambda @t204 (and (_ (_ tptp.ord_le1772180283um_c_c @t202) @t203) (_ (_ tptp.ord_le1772180283um_c_c @t203) @t202))))) % 0.44/0.83 (assume @p65 (forall (@list @t44 @t95 @t208) (=> @t103 (=> (_ @t100 @t208) (_ @t102 @t208))))) % 0.44/0.83 (assume @p66 (forall @t171 (=> (forall @t170 (=> @t169 @t168)) @t192))) % 0.44/0.83 (assume @p67 (forall @t178 (=> (forall @t177 (=> @t176 @t175)) @t195))) % 0.44/0.83 (assume @p68 (forall @t201 (=> (forall @t122 (=> @t210 @t209)) @t200))) % 0.44/0.83 (assume @p69 (forall @t151 (_ @t102 @t44))) % 0.44/0.83 (assume @p70 (forall @t98 (=> @t96 @t101))) % 0.44/0.83 (assume @p71 (forall @t98 (=> @t96 @t103))) % 0.44/0.83 (assume @p72 (= tptp.ord_le977353143real_c (lambda @t215 (forall @t146 (=> @t214 @t212))))) % 0.44/0.83 (assume @p73 (= tptp.ord_le764260924um_c_d (lambda @t220 (forall @t155 (=> @t219 @t217))))) % 0.44/0.83 (assume @p74 (= tptp.ord_le1772180283um_c_c (lambda @t204 (forall @t150 (=> @t222 @t221))))) % 0.44/0.83 (assume @p75 (forall @t98 (=> @t96 (not (=> @t103 (not @t101)))))) % 0.44/0.83 (assume @p76 (forall (@list @t74 @t104 @t75) (=> @t105 (=> @t78 (_ @t76 @t104))))) % 0.44/0.83 (assume @p77 (forall (@list @t81 @t111 @t82) (=> @t112 (=> @t85 (_ @t83 @t111))))) % 0.44/0.83 (assume @p78 (forall (@list @t44 @t95 @t89) (=> @t103 (=> @t92 (_ @t90 @t95))))) % 0.44/0.83 (assume @p79 (forall (@list @t74 @t104 @t223) (=> @t105 (=> @t225 (_ @t224 @t104))))) % 0.44/0.83 (assume @p80 (forall (@list @t81 @t111 @t226) (=> @t112 (=> @t228 (_ @t227 @t111))))) % 0.44/0.83 (assume @p81 (forall (@list @t44 @t95 @t229) (=> @t103 (=> @t231 (_ @t230 @t95))))) % 0.44/0.83 (assume @p82 (forall @t73 (=> @t183 @t185))) % 0.44/0.83 (assume @p83 (forall @t73 (= (_ @t232 @t66) (_ @t184 @t69)))) % 0.44/0.83 (assume @p84 (forall @t73 (= (_ @t182 @t67) (_ @t187 @t70)))) % 0.44/0.83 (assume @p85 (forall @t234 (=> (_ @t233 @t124) (_ @t181 @t123)))) % 0.44/0.83 (assume @p86 (forall @t234 (=> (_ @t179 @t127) (_ @t235 @t126)))) % 0.44/0.83 (assume @p87 (forall @t128 (=> @t236 (_ @t233 @t127)))) % 0.44/0.83 (assume @p88 (forall (@list @t44 @t95 @t17 @t237) (=> @t103 (=> (_ @t238 @t95) (_ @t238 @t44))))) % 0.44/0.83 (assume @p89 (forall (@list @t95 @t44 @t17 @t239) (=> @t101 (=> (_ @t240 @t44) (_ @t240 @t95))))) % 0.44/0.83 (assume @p90 (forall @t73 (= (= @t70 @t66) (= @t67 @t69)))) % 0.44/0.83 (assume @p91 (forall @t73 (= (= @t69 @t67) (= @t66 @t70)))) % 0.44/0.83 (assume @p92 (forall @t73 (=> @t130 @t131))) % 0.44/0.83 (assume @p93 (forall @t151 (= (_ tptp.uminus1381786404um_c_c @t88) @t44))) % 0.44/0.83 (assume @p94 (forall @t80 (=> @t77 @t79))) % 0.44/0.83 (assume @p95 (forall @t87 (=> @t84 @t86))) % 0.44/0.83 (assume @p96 (forall @t94 (=> @t91 @t93))) % 0.44/0.83 (assume @p97 (forall (@list @t28 @t25 @t242 @t241) (= (_ (_ tptp.ord_le850691415real_c @t30) (_ (_ tptp.produc394644079real_c @t242) @t241)) (and (_ (_ tptp.ord_le775706699real_c @t28) @t242) (_ (_ tptp.ord_le775706699real_c @t25) @t241))))) % 0.44/0.83 (assume @p98 (forall @t249 (= (_ (_ tptp.ord_le684454199um_c_c @t64) (_ (_ tptp.produc1439061071um_c_c @t246) @t243)) (and @t248 @t245)))) % 0.44/0.83 (assume @p99 (forall (@list @t62 @t66 @t246 @t250) (= (_ (_ tptp.ord_le835231240c_real @t68) (_ (_ tptp.produc1528874528c_real @t246) @t250)) (and @t248 @t251)))) % 0.44/0.83 (assume @p100 (forall (@list @t69 @t60 @t252 @t243) (= (_ (_ tptp.ord_le191210632um_c_c @t71) (_ (_ tptp.produc1186709024um_c_c @t252) @t243)) (and @t253 @t245)))) % 0.44/0.83 (assume @p101 (forall @t254 (= (_ (_ tptp.ord_le1342644953l_real @t72) (_ (_ tptp.produc705216881l_real @t252) @t250)) (and @t253 @t251)))) % 0.44/0.83 (assume @p102 (forall @t129 (_ @t235 @t124))) % 0.44/0.83 (assume @p103 (forall @t257 (_ @t256 @t255))) % 0.44/0.83 (assume @p104 (forall (@list @t261 @t259 @t260 @t258) (=> (_ (_ tptp.ord_le775706699real_c @t261) @t259) (=> (_ (_ tptp.ord_le775706699real_c @t260) @t258) (_ (_ tptp.ord_le850691415real_c (_ (_ tptp.produc394644079real_c @t261) @t260)) (_ (_ tptp.produc394644079real_c @t259) @t258)))))) % 0.44/0.83 (assume @p105 (forall (@list @t124 @t263 @t123 @t262) (=> @t265 (=> @t264 (_ (_ tptp.ord_le684454199um_c_c (_ (_ tptp.produc1439061071um_c_c @t124) @t123)) (_ (_ tptp.produc1439061071um_c_c @t263) @t262)))))) % 0.44/0.83 (assume @p106 (forall (@list @t124 @t263 @t267 @t266) (=> @t265 (=> @t269 (_ (_ tptp.ord_le835231240c_real (_ (_ tptp.produc1528874528c_real @t124) @t267)) (_ (_ tptp.produc1528874528c_real @t263) @t266)))))) % 0.44/0.83 (assume @p107 (forall (@list @t255 @t270 @t123 @t262) (=> @t271 (=> @t264 (_ (_ tptp.ord_le191210632um_c_c (_ (_ tptp.produc1186709024um_c_c @t255) @t123)) (_ (_ tptp.produc1186709024um_c_c @t270) @t262)))))) % 0.44/0.83 (assume @p108 (forall (@list @t255 @t270 @t267 @t266) (=> @t271 (=> @t269 (_ (_ tptp.ord_le1342644953l_real (_ (_ tptp.produc705216881l_real @t255) @t267)) (_ (_ tptp.produc705216881l_real @t270) @t266)))))) % 0.44/0.83 (assume @p109 (_ (_ tptp.ord_le1772180283um_c_c @t272) tptp.v)) % 0.44/0.83 (assume @p110 (forall @t257 (=> @t277 (=> @t275 (_ (_ tptp.member1895684704real_c (_ @t38 @t274)) @t273))))) % 0.44/0.83 (assume @p111 (_ tptp.coinci501627771_a_b_c tptp.p)) % 0.44/0.83 (assume @p112 (_ @t276 tptp.t)) % 0.44/0.83 (assume @p113 (= (_ tptp.uminus_uminus_real tptp.zero_zero_real) tptp.zero_zero_real)) % 0.44/0.83 (assume @p114 (forall @t99 (= (= tptp.zero_zero_real @t70) (= tptp.zero_zero_real @t69)))) % 0.44/0.83 (assume @p115 (forall @t99 (= (= @t70 tptp.zero_zero_real) @t278))) % 0.44/0.83 (assume @p116 (forall @t99 (= (= @t69 @t70) @t278))) % 0.44/0.83 (assume @p117 (forall @t99 (= (= @t70 @t69) @t278))) % 0.44/0.83 (assume @p118 (forall @t286 @t285)) % 0.44/0.83 (assume @p119 (forall @t99 (= (_ @t232 @t69) @t287))) % 0.44/0.83 (assume @p120 (forall @t99 (= (_ @t182 @t70) @t288))) % 0.44/0.83 (assume @p121 (forall @t99 (= (_ @t232 tptp.zero_zero_real) @t287))) % 0.44/0.83 (assume @p122 (forall @t99 (= (_ @t276 @t70) @t288))) % 0.44/0.83 (assume @p123 (_ tptp.fsafe_a_b_c tptp.p)) % 0.44/0.83 (assume @p124 (= tptp.zero_z1506780526real_c (_ (_ tptp.produc394644079real_c tptp.zero_z109254132real_c) tptp.zero_z109254132real_c))) % 0.44/0.83 (assume @p125 (= tptp.zero_z659284464l_real (_ (_ tptp.produc705216881l_real tptp.zero_zero_real) tptp.zero_zero_real))) % 0.44/0.83 (assume @p126 (forall @t257 (= (= tptp.zero_zero_real @t255) @t289))) % 0.44/0.83 (assume @p127 (forall @t298 (= @t297 (and @t296 (=> @t295 @t293))))) % 0.44/0.83 (assume @p128 (forall @t308 (=> (_ @t247 @t307) @t306))) % 0.44/0.83 (assume @p129 (forall @t318 (=> (_ @t247 @t317) @t316))) % 0.44/0.83 (assume @p130 (forall @t323 (=> (_ @t182 @t322) @t321))) % 0.44/0.83 (assume @p131 (forall @t328 (=> (_ @t182 @t327) @t326))) % 0.44/0.83 (assume @p132 (forall @t331 (=> @t330 (=> (_ (_ tptp.ord_le1772180283um_c_c @t307) @t246) @t329)))) % 0.44/0.83 (assume @p133 (forall @t333 (=> @t330 (=> (_ (_ tptp.ord_less_eq_real @t322) @t252) @t332)))) % 0.44/0.83 (assume @p134 (forall @t335 (=> @t183 (=> (_ (_ tptp.ord_le1772180283um_c_c @t317) @t246) @t334)))) % 0.44/0.83 (assume @p135 (forall @t337 (=> @t183 (=> (_ (_ tptp.ord_less_eq_real @t327) @t252) @t336)))) % 0.44/0.83 (assume @p136 (forall @t308 (=> (= @t62 @t307) @t306))) % 0.44/0.83 (assume @p137 (forall @t323 (=> (= @t69 @t322) @t321))) % 0.44/0.83 (assume @p138 (forall @t318 (=> (= @t62 @t317) @t316))) % 0.44/0.83 (assume @p139 (forall @t328 (=> (= @t69 @t327) @t326))) % 0.44/0.83 (assume @p140 (forall @t331 (=> @t330 (=> (= @t307 @t246) @t329)))) % 0.44/0.83 (assume @p141 (forall @t333 (=> @t330 (=> (= @t322 @t252) @t332)))) % 0.44/0.83 (assume @p142 (forall @t335 (=> @t183 (=> (= @t317 @t246) @t334)))) % 0.44/0.83 (assume @p143 (forall @t337 (=> @t183 (=> (= @t327 @t252) @t336)))) % 0.44/0.83 (assume @p144 (= @t207 (lambda (@list @t338 @t339) (and (_ @t340 @t339) (_ (_ tptp.ord_le1772180283um_c_c @t339) @t338))))) % 0.44/0.83 (assume @p145 (= @t346 (lambda (@list @t341 @t342) (and (_ @t343 @t342) (_ (_ tptp.ord_less_eq_real @t342) @t341))))) % 0.44/0.83 (assume @p146 (forall @t128 (=> @t236 (=> @t180 @t125)))) % 0.44/0.83 (assume @p147 (forall @t350 (=> @t349 (=> @t348 @t347)))) % 0.44/0.83 (assume @p148 (forall @t350 (or @t349 @t348))) % 0.44/0.83 (assume @p149 (forall @t128 (=> @t125 @t236))) % 0.44/0.83 (assume @p150 (forall @t350 (=> @t347 @t349))) % 0.44/0.83 (assume @p151 (forall @t350 (=> @t351 @t348))) % 0.44/0.83 (assume @p152 (forall @t353 (=> @t330 @t352))) % 0.44/0.83 (assume @p153 (forall @t355 (=> @t183 @t354))) % 0.44/0.83 (assume @p154 (forall @t362 (=> (=> @t349 (not @t359)) (=> (=> @t348 (not @t361)) (=> (=> @t361 (not @t360)) (=> (=> @t360 (not @t348)) (=> (=> @t359 (not @t358)) (not (=> @t358 @t351))))))))) % 0.44/0.83 (assume @p155 (forall @t234 (=> @t180 (= @t236 @t125)))) % 0.44/0.83 (assume @p156 (forall (@list @t267 @t255) (=> @t348 (= @t349 @t347)))) % 0.44/0.83 (assume @p157 (= @t207 (lambda @t367 (and @t366 @t365)))) % 0.44/0.83 (assume @p158 (= @t346 (lambda @t372 (and @t371 @t370)))) % 0.44/0.83 (assume @p159 (forall @t353 (=> @t373 @t352))) % 0.44/0.83 (assume @p160 (forall @t355 (=> @t130 @t354))) % 0.44/0.83 (assume @p161 (forall @t353 (=> @t330 (=> (= @t60 @t246) @t248)))) % 0.44/0.83 (assume @p162 (forall @t355 (=> @t183 (=> (= @t66 @t252) @t253)))) % 0.44/0.83 (assume @p163 (forall @t65 (=> @t330 (=> @t374 @t373)))) % 0.44/0.83 (assume @p164 (forall @t73 (=> @t183 (=> @t188 @t130)))) % 0.44/0.83 (assume @p165 (forall (@list @t124 @t123 @t375) (=> @t236 (=> (_ @t179 @t375) (_ @t235 @t375))))) % 0.44/0.83 (assume @p166 (forall @t362 (=> @t349 (=> @t359 @t361)))) % 0.44/0.83 (assume @p167 (forall (@list @t62) (_ @t247 @t62))) % 0.44/0.83 (assume @p168 (forall @t99 (_ @t182 @t69))) % 0.44/0.83 (assume @p169 (forall (@list @t376 @t69 @t66) (=> (forall @t380 (=> (_ (_ tptp.ord_less_eq_real @t378) @t377) @t379)) (=> (forall @t380 (=> (_ (_ @t376 @t377) @t378) @t379)) (_ (_ @t376 @t69) @t66))))) % 0.44/0.83 (assume @p170 (forall (@list @t60 @t62 @t246) (=> @t374 (=> (_ @t381 @t60) @t382)))) % 0.44/0.83 (assume @p171 (forall (@list @t66 @t69 @t252) (=> @t188 (=> (_ @t383 @t66) @t384)))) % 0.44/0.83 (assume @p172 (= @t207 (lambda @t367 (and @t365 @t366)))) % 0.44/0.83 (assume @p173 (= @t346 (lambda @t372 (and @t370 @t371)))) % 0.44/0.83 (assume @p174 (forall (@list @t60 @t62) (=> @t374 (=> @t330 @t373)))) % 0.44/0.83 (assume @p175 (forall @t186 (=> @t188 (=> @t183 @t130)))) % 0.44/0.83 (assume @p176 (forall @t298 (= (_ @t292 (_ @t291 (_ (_ tptp.equiv_a_b_c @t290) @t294))) @t297))) % 0.44/0.83 (assume @p177 (forall @t286 (=> @t385 @t285))) % 0.44/0.83 (assume @p178 (forall @t257 (= @t289 (and @t277 (_ @t276 @t386))))) % 0.44/0.83 (assume @p179 (_ @t276 tptp.zero_zero_real)) % 0.44/0.83 (assume @p180 @t385) % 0.44/0.83 (assume @p181 (forall (@list @t387 @t391 @t13 @t388) (=> (_ (_ tptp.ord_le929608341um_b_c @t387) @t391) (=> (_ @t390 @t391) (_ @t390 @t387))))) % 0.44/0.83 (assume @p182 (forall (@list @t393 @t394 @t392) (=> (_ (_ (_ tptp.denota69106024_a_b_c @t393) @t394) @t392) (_ (_ (_ tptp.denota69106024_a_b_c @t394) @t393) @t392)))) % 0.44/0.83 (assume @p183 (forall (@list @t13 @t387) (_ (_ @t389 @t13) @t387))) % 0.44/0.83 (assume @p184 (_ @t395 tptp.j)) % 0.44/0.83 (assume @p185 (_ @t395 tptp.i)) % 0.44/0.83 (assume @p186 (forall @t298 (= (_ @t292 (_ @t291 (_ (_ tptp.implies_a_b_c @t290) @t294))) @t296))) % 0.44/0.83 (assume @p187 (forall (@list @t13) (_ @t395 @t13))) % 0.44/0.83 (assume @p188 (forall (@list @t399 @t397 @t398 @t396) (= (= (_ (_ tptp.evolveODE_a_c_b @t399) @t397) (_ (_ tptp.evolveODE_a_c_b @t398) @t396)) (and (= @t399 @t398) (= @t397 @t396))))) % 0.44/0.83 (assume @p189 (_ (_ (_ (_ tptp.initia1631504802real_c tptp.sol) (lambda (@list @t368 @t401) (_ @t402 @t401))) @t400) (_ tptp.collec230941376real_c (lambda @t160 (_ (_ tptp.member1895684704real_c (_ @t38 @t157)) @t273))))) % 0.44/0.83 (assume @p190 (= tptp.ord_le977353143real_c (lambda @t215 (_ (_ tptp.ord_le1132241894al_c_o @t403) (lambda @t146 @t212))))) % 0.44/0.83 (assume @p191 (= tptp.ord_le764260924um_c_d (lambda @t220 (_ (_ tptp.ord_le2143422793_c_d_o @t404) (lambda @t155 @t217))))) % 0.44/0.83 (assume @p192 (= tptp.ord_le1772180283um_c_c (lambda @t204 (_ (_ tptp.ord_le1315653386_c_c_o @t405) (lambda @t150 @t221))))) % 0.44/0.83 (assume @p193 (forall (@list @t74 @t51) (_ (_ tptp.ord_le977353143real_c @t407) @t74))) % 0.44/0.83 (assume @p194 (forall (@list @t81 @t137) (_ (_ tptp.ord_le764260924um_c_d @t409) @t81))) % 0.44/0.83 (assume @p195 (forall (@list @t156 @t138) (_ (_ tptp.ord_le1327118209real_c @t410) @t156))) % 0.44/0.83 (assume @p196 (forall (@list @t161 @t141) (_ (_ tptp.ord_less_eq_set_c @t411) @t161))) % 0.44/0.83 (assume @p197 (forall (@list @t44 @t134) (_ (_ tptp.ord_le1772180283um_c_c @t412) @t44))) % 0.44/0.83 (assume @p198 (forall (@list @t138) (= (_ tptp.collec230941376real_c (lambda @t160 (not @t191))) (_ tptp.uminus102402154real_c @t139)))) % 0.44/0.83 (assume @p199 (forall (@list @t141) (= (_ tptp.collect_c (lambda @t165 (not @t194))) (_ tptp.uminus_uminus_set_c @t142)))) % 0.44/0.83 (assume @p200 (forall (@list @t134) (= (_ tptp.collect_Sum_sum_c_c (lambda @t150 (not @t198))) (_ tptp.uminus1381786404um_c_c @t135)))) % 0.44/0.83 (assume @p201 (= tptp.uminus232257166real_c (lambda @t413 (_ tptp.collec1643251106real_c (_ tptp.uminus32155087al_c_o @t403))))) % 0.44/0.83 (assume @p202 (= tptp.uminus373867045um_c_d (lambda @t414 (_ tptp.collect_Sum_sum_c_d (_ tptp.uminus916499104_c_d_o @t404))))) % 0.44/0.83 (assume @p203 (= tptp.uminus102402154real_c (lambda @t417 (_ tptp.collec230941376real_c (_ tptp.uminus23580315al_c_o (lambda @t160 @t416)))))) % 0.44/0.83 (assume @p204 (= tptp.uminus_uminus_set_c (lambda @t420 (_ tptp.collect_c (_ tptp.uminus_uminus_c_o (lambda @t165 @t419)))))) % 0.44/0.83 (assume @p205 (= tptp.uminus1381786404um_c_c (lambda @t421 (_ tptp.collect_Sum_sum_c_c (_ tptp.uminus88729697_c_c_o @t405))))) % 0.44/0.83 (assume @p206 (forall (@list @t424 @t423 @t422 @t58) (=> (= (_ (_ (_ tptp.denota1896987029_a_b_c @t424) @t423) @t422) @t58) (= @t58 (_ (_ tptp.produc394644079real_c @t422) (_ (_ (_ tptp.denota1275485728_a_b_c @t424) @t423) @t422)))))) % 0.44/0.83 (assume @p207 (forall @t249 (= (_ (_ tptp.ord_le657554289um_c_c @t425) (_ (_ tptp.set_or935154662um_c_c @t246) @t243)) (or (not @t330) (and @t382 @t245))))) % 0.44/0.83 (assume @p208 (forall @t254 (= (_ (_ tptp.ord_less_eq_set_real @t426) (_ (_ tptp.set_or656347191t_real @t252) @t250)) (or @t189 (and @t384 @t251))))) % 0.44/0.83 (assume @p209 (forall (@list @t428 @t430 @t427) (= (_ @t431 (_ (_ tptp.set_or385782508real_c @t430) @t427)) (and (_ (_ tptp.ord_le850691415real_c @t430) @t428) (_ @t429 @t427))))) % 0.44/0.83 (assume @p210 (forall (@list @t433 @t435 @t432) (= (_ @t438 (_ @t437 @t432)) (and (_ @t436 @t433) (_ @t434 @t432))))) % 0.44/0.83 (assume @p211 (forall (@list @t440 @t442 @t439) (= (_ @t445 (_ @t444 @t439)) (and (_ @t443 @t440) (_ @t441 @t439))))) % 0.44/0.83 (assume @p212 (forall (@list @t435 @t449 @t447 @t446) (= (= @t451 (_ (_ tptp.set_or935154662um_c_c @t447) @t446)) (or (and (= @t435 @t447) (= @t449 @t446)) (and @t450 (not (_ @t448 @t446))))))) % 0.44/0.83 (assume @p213 (forall (@list @t442 @t455 @t453 @t452) (= (= @t458 @t457) (or (and (= @t442 @t453) (= @t455 @t452)) (and @t456 (not (_ @t454 @t452))))))) % 0.44/0.83 (assume @p214 (forall @t462 (= (_ (_ tptp.ord_le1132241894al_c_o (lambda @t146 (_ @t144 @t460))) (lambda @t146 (_ @t144 @t459))) @t461))) % 0.44/0.83 (assume @p215 (forall (@list @t464 @t463) (= (_ (_ tptp.ord_le2143422793_c_d_o (lambda @t155 (_ @t153 @t464))) (lambda @t155 (_ @t153 @t463))) (_ (_ tptp.ord_le764260924um_c_d @t464) @t463)))) % 0.44/0.83 (assume @p216 (forall (@list @t466 @t465) (= (_ (_ tptp.ord_le1315653386_c_c_o (lambda @t150 (_ @t148 @t466))) (lambda @t150 (_ @t148 @t465))) (_ (_ tptp.ord_le1772180283um_c_c @t466) @t465)))) % 0.44/0.83 (assume @p217 (forall @t257 (=> @t277 (=> @t275 (_ (_ (_ tptp.has_ve1904308670real_c tptp.sol) (_ @t402 @t274)) (_ @t467 @t400)))))) % 0.44/0.83 (assume @p218 (forall (@list @t469 @t468) (=> (forall @t50 (=> (_ @t470 @t469) (_ @t470 @t468))) (_ (_ tptp.ord_le977353143real_c @t469) @t468)))) % 0.44/0.83 (assume @p219 (forall @t462 (= (_ (_ tptp.ord_le1382916304al_c_o @t475) @t474) @t461))) % 0.44/0.83 (assume @p220 (forall @t462 (= (= @t475 @t474) (= @t460 @t459)))) % 0.44/0.83 (assume @p221 (forall (@list @t481 @t479 @t255 @t476 @t480 @t478) (=> (_ @t486 @t477) (=> (_ (_ @t484 @t478) @t477) (_ (_ (_ tptp.has_ve373335844real_c (lambda @t483 (_ (_ tptp.produc394644079real_c @t482) (_ @t480 @t341)))) (_ (_ tptp.produc394644079real_c @t479) @t478)) @t477))))) % 0.44/0.83 (assume @p222 (forall (@list @t324 @t488 @t487) (=> (_ (_ (_ tptp.has_ve217091583e_real @t324) @t488) @t487) (_ (_ (_ tptp.has_ve217091583e_real (lambda @t483 (_ tptp.uminus_uminus_real (_ @t324 @t341)))) (_ tptp.uminus_uminus_real @t488)) @t487)))) % 0.44/0.83 (assume @p223 (forall (@list @t481 @t479 @t487) (=> (_ @t486 @t487) (_ (_ (_ tptp.has_ve1904308670real_c (lambda @t483 (_ tptp.uminus1737280820real_c @t482))) (_ tptp.uminus1737280820real_c @t479)) @t487)))) % 0.44/0.83 (assume @p224 (forall (@list @t252 @t487) (_ (_ (_ tptp.has_ve217091583e_real (lambda @t483 @t252)) tptp.zero_zero_real) @t487))) % 0.44/0.83 (assume @p225 (forall (@list @t242 @t487) (_ (_ (_ tptp.has_ve1904308670real_c (lambda @t483 @t242)) tptp.zero_z109254132real_c) @t487))) % 0.44/0.83 (assume @p226 (forall (@list @t481 @t479 @t255 @t491 @t489) (=> (_ @t486 @t493) (=> @t492 (_ @t486 @t490))))) % 0.44/0.83 (assume @p227 (forall (@list @t481 @t494 @t255 @t489 @t491 @t480) (=> (_ (_ @t485 @t494) @t490) (=> (_ @t496 @t491) (=> @t495 (=> (forall (@list @t311) (=> (_ (_ tptp.member_real @t311) @t491) (= (_ @t481 @t311) (_ @t480 @t311)))) (_ (_ @t484 @t494) @t493))))))) % 0.44/0.83 (assume @p228 (forall @t505 (=> @t504 (=> (_ (_ tptp.ord_le1327118209real_c @t503) @t497) @t502)))) % 0.44/0.83 (assume @p229 (forall (@list @t499 @t498 @t489 @t503 @t491) (=> @t504 (=> @t495 (_ @t506 @t503))))) % 0.44/0.83 (assume @p230 (forall (@list @t499 @t498 @t491 @t497 @t489 @t503) (=> (_ @t506 @t497) (=> @t492 (=> (_ (_ tptp.ord_le1327118209real_c @t497) @t503) @t504))))) % 0.44/0.83 (assume @p231 (forall (@list @t476 @t507 @t255) (=> (_ (_ tptp.ord_less_eq_set_real @t476) @t507) (_ (_ tptp.ord_le132810396r_real @t477) (_ @t467 @t507))))) % 0.44/0.83 (assume @p232 (forall (@list @t132 @t223 @t508) (=> (and (_ (_ tptp.ord_le850691415real_c @t132) @t223) (_ (_ tptp.ord_le850691415real_c @t223) @t508)) (_ @t224 (_ (_ tptp.set_or385782508real_c @t132) @t508))))) % 0.44/0.83 (assume @p233 (forall (@list @t62 @t124 @t60) (=> (and (_ @t247 @t124) (_ @t235 @t60)) (_ (_ tptp.member2124950898um_c_c @t124) @t425)))) % 0.44/0.83 (assume @p234 (forall (@list @t69 @t255 @t66) (=> (and (_ @t182 @t255) (_ @t256 @t66)) (_ @t496 @t426)))) % 0.44/0.83 (assume @p235 (forall (@list @t156 @t138 @t166) (= (_ @t509 (_ tptp.collec230941376real_c (lambda @t160 (and @t191 @t190)))) (and (_ @t509 @t139) (_ @t509 @t167))))) % 0.44/0.83 (assume @p236 (forall (@list @t161 @t141 @t172) (= (_ @t510 (_ tptp.collect_c (lambda @t165 (and @t194 @t193)))) (and (_ @t510 @t142) (_ @t510 @t173))))) % 0.44/0.83 (assume @p237 (forall (@list @t44 @t134 @t196) (= (_ @t102 (_ tptp.collect_Sum_sum_c_c (lambda @t150 (and @t198 @t197)))) (and (_ @t102 @t135) (_ @t102 @t199))))) % 0.44/0.83 (assume @p238 (forall (@list @t104 @t74 @t51) (=> @t513 (= (_ @t512 @t407) (forall @t146 (=> @t511 @t406)))))) % 0.44/0.83 (assume @p239 (forall (@list @t111 @t81 @t137) (=> @t516 (= (_ @t515 @t409) (forall @t155 (=> @t514 @t408)))))) % 0.44/0.83 (assume @p240 (forall (@list @t517 @t156 @t138) (=> @t520 (= (_ @t519 @t410) (forall @t160 (=> @t518 @t191)))))) % 0.44/0.83 (assume @p241 (forall (@list @t521 @t161 @t141) (=> @t524 (= (_ @t523 @t411) (forall @t165 (=> @t522 @t194)))))) % 0.44/0.83 (assume @p242 (forall (@list @t95 @t44 @t134) (=> @t101 (= (_ @t100 @t412) (forall @t150 (=> @t525 @t198)))))) % 0.44/0.83 (assume @p243 (forall (@list @t104 @t74 @t526 @t51) (=> @t513 (=> (forall @t110 (=> @t108 (=> (_ @t526 @t106) (_ @t51 @t106)))) (_ (_ tptp.ord_le977353143real_c (_ tptp.collec1643251106real_c (lambda @t146 (and @t511 (_ @t526 @t143))))) @t407))))) % 0.44/0.83 (assume @p244 (forall (@list @t111 @t81 @t527 @t137) (=> @t516 (=> (forall @t117 (=> @t115 (=> (_ @t527 @t113) (_ @t137 @t113)))) (_ (_ tptp.ord_le764260924um_c_d (_ tptp.collect_Sum_sum_c_d (lambda @t155 (and @t514 (_ @t527 @t152))))) @t409))))) % 0.44/0.83 (assume @p245 (forall (@list @t517 @t156 @t166 @t138) (=> @t520 (=> (forall @t170 (=> (_ (_ tptp.member1261661570real_c @t47) @t517) (=> @t168 @t169))) (_ (_ tptp.ord_le1327118209real_c (_ tptp.collec230941376real_c (lambda @t160 (and @t518 @t190)))) @t410))))) % 0.44/0.83 (assume @p246 (forall (@list @t521 @t161 @t172 @t141) (=> @t524 (=> (forall @t177 (=> (_ @t528 @t521) (=> @t175 @t176))) (_ (_ tptp.ord_less_eq_set_c (_ tptp.collect_c (lambda @t165 (and @t522 @t193)))) @t411))))) % 0.44/0.83 (assume @p247 (forall (@list @t95 @t44 @t196 @t134) (=> @t101 (=> (forall @t122 (=> @t120 (=> @t209 @t210))) (_ (_ tptp.ord_le1772180283um_c_c (_ tptp.collect_Sum_sum_c_c (lambda @t150 (and @t525 @t197)))) @t412))))) % 0.44/0.83 (assume @p248 (forall (@list @t223 @t531 @t529 @t51) (=> (_ @t224 @t531) (=> (_ (_ tptp.ord_le977353143real_c @t531) @t530) (_ @t51 @t223))))) % 0.44/0.83 (assume @p249 (forall (@list @t226 @t534 @t532 @t137) (=> (_ @t227 @t534) (=> (_ (_ tptp.ord_le764260924um_c_d @t534) @t533) (_ @t137 @t226))))) % 0.44/0.83 (assume @p250 (forall (@list @t261 @t536 @t503 @t138) (=> (_ (_ tptp.member1261661570real_c @t261) @t536) (=> (_ (_ tptp.ord_le1327118209real_c @t536) @t535) (_ @t138 @t261))))) % 0.44/0.83 (assume @p251 (forall (@list @t537 @t540 @t538 @t141) (=> (_ @t541 @t540) (=> (_ (_ tptp.ord_less_eq_set_c @t540) @t539) (_ @t141 @t537))))) % 0.44/0.83 (assume @p252 (forall (@list @t229 @t544 @t542 @t134) (=> (_ @t230 @t544) (=> (_ (_ tptp.ord_le1772180283um_c_c @t544) @t543) (_ @t134 @t229))))) % 0.44/0.83 (assume @p253 (forall (@list @t529 @t51) (_ (_ tptp.ord_le977353143real_c @t530) @t529))) % 0.44/0.83 (assume @p254 (forall (@list @t532 @t137) (_ (_ tptp.ord_le764260924um_c_d @t533) @t532))) % 0.44/0.83 (assume @p255 (forall (@list @t503 @t138) (_ (_ tptp.ord_le1327118209real_c @t535) @t503))) % 0.44/0.83 (assume @p256 (forall (@list @t538 @t141) (_ (_ tptp.ord_less_eq_set_c @t539) @t538))) % 0.44/0.83 (assume @p257 (forall (@list @t542 @t134) (_ (_ tptp.ord_le1772180283um_c_c @t543) @t542))) % 0.44/0.83 (assume @p258 (forall (@list @t546 @t548 @t460 @t545) (=> (_ (_ tptp.member1895684704real_c (_ @t547 @t548)) @t460) (=> (= @t545 @t548) (_ (_ tptp.member1895684704real_c (_ @t547 @t545)) @t460))))) % 0.44/0.83 (assume @p259 (forall (@list @t12 @t549) (= (_ tptp.hpsafe_a_b_c (_ @t551 @t549)) (and @t550 (_ tptp.fsafe_a_b_c @t549))))) % 0.44/0.83 (assume @p260 (forall (@list @t12 @t552) (=> @t550 (=> (_ tptp.fsafe_a_b_c @t552) (_ tptp.hpsafe_a_b_c (_ @t551 @t552)))))) % 0.44/0.83 (assume @p261 (forall (@list @t435 @t449 @t447) (= (_ @t553 (_ tptp.set_or2028906832um_c_c @t447)) (or @t450 (_ @t448 @t435))))) % 0.44/0.83 (assume @p262 (forall (@list @t442 @t455 @t453) (= (_ @t554 (_ tptp.set_ord_atLeast_real @t453)) (or @t456 (_ @t454 @t442))))) % 0.44/0.83 (assume @p263 (forall (@list @t435 @t449 @t446) (= (_ @t553 (_ tptp.set_or326480468um_c_c @t446)) (or @t450 (_ (_ tptp.ord_le1772180283um_c_c @t449) @t446))))) % 0.44/0.83 (assume @p264 (forall (@list @t442 @t455 @t452) (= (_ @t554 (_ tptp.set_ord_atMost_real @t452)) (or @t456 (_ (_ tptp.ord_less_eq_real @t455) @t452))))) % 0.44/0.83 (assume @p265 (forall @t556 (= (_ @t431 (_ tptp.set_or248124158real_c @t555)) (_ @t429 @t555)))) % 0.44/0.83 (assume @p266 (forall @t558 (= (_ @t438 (_ tptp.set_or326480468um_c_c @t557)) (_ @t434 @t557)))) % 0.44/0.83 (assume @p267 (forall @t560 (= (_ @t445 (_ tptp.set_ord_atMost_real @t559)) (_ @t441 @t559)))) % 0.44/0.83 (assume @p268 (forall @t556 (= (_ @t431 (_ tptp.set_or10334466real_c @t555)) (_ (_ tptp.ord_le850691415real_c @t555) @t428)))) % 0.44/0.83 (assume @p269 (forall @t558 (= (_ @t438 (_ tptp.set_or2028906832um_c_c @t557)) (_ (_ tptp.ord_le1772180283um_c_c @t557) @t433)))) % 0.44/0.83 (assume @p270 (forall @t560 (= (_ @t445 (_ tptp.set_ord_atLeast_real @t559)) (_ (_ tptp.ord_less_eq_real @t559) @t440)))) % 0.44/0.83 (assume @p271 (forall @t128 (= (_ (_ tptp.ord_le657554289um_c_c (_ tptp.set_or326480468um_c_c @t124)) (_ tptp.set_or326480468um_c_c @t123)) @t236))) % 0.44/0.83 (assume @p272 (forall @t350 (= (_ (_ tptp.ord_less_eq_set_real @t561) (_ tptp.set_ord_atMost_real @t267)) @t349))) % 0.44/0.83 (assume @p273 (forall @t128 (= (_ (_ tptp.ord_le657554289um_c_c (_ tptp.set_or2028906832um_c_c @t124)) (_ tptp.set_or2028906832um_c_c @t123)) @t180))) % 0.44/0.83 (assume @p274 (forall @t350 (= (_ (_ tptp.ord_less_eq_set_real @t562) (_ tptp.set_ord_atLeast_real @t267)) @t348))) % 0.44/0.83 (assume @p275 (forall (@list @t442 @t453 @t452) (not (_ (_ tptp.ord_less_eq_set_real (_ tptp.set_ord_atLeast_real @t442)) @t457)))) % 0.44/0.83 (assume @p276 (forall (@list @t455 @t453 @t452) (not (_ (_ tptp.ord_less_eq_set_real (_ tptp.set_ord_atMost_real @t455)) @t457)))) % 0.44/0.83 (assume @p277 (forall @t257 (= (_ @t563 @t561) (_ tptp.set_ord_atLeast_real @t386)))) % 0.44/0.83 (assume @p278 (forall @t257 (= (_ @t563 @t562) (_ tptp.set_ord_atMost_real @t386)))) % 0.44/0.83 (assume @p279 (forall (@list @t567 @t564 @t537 @t161) (=> (= @t567 @t570) (=> @t569 (_ @t568 @t566))))) % 0.44/0.83 (assume @p280 (forall (@list @t574 @t571 @t537 @t161) (=> (= @t574 @t576) (=> @t569 (_ @t575 @t573))))) % 0.44/0.83 (assume @p281 (forall (@list @t567 @t577 @t229 @t44) (=> (= @t567 @t580) (=> @t231 (_ @t568 @t579))))) % 0.44/0.83 (assume @p282 (forall (@list @t574 @t581 @t229 @t44) (=> (= @t574 @t583) (=> @t231 (_ @t575 @t582))))) % 0.44/0.83 (assume @p283 (forall (@list @t567 @t584 @t226 @t81) (=> (= @t567 @t586) (=> @t228 (_ @t568 @t585))))) % 0.44/0.83 (assume @p284 (forall (@list @t574 @t587 @t226 @t81) (=> (= @t574 @t589) (=> @t228 (_ @t575 @t588))))) % 0.44/0.83 (assume @p285 (forall (@list @t567 @t590 @t223 @t74) (=> (= @t567 @t592) (=> @t225 (_ @t568 @t591))))) % 0.44/0.83 (assume @p286 (forall (@list @t574 @t593 @t223 @t74) (=> (= @t574 @t595) (=> @t225 (_ @t575 @t594))))) % 0.44/0.83 (assume @p287 (forall (@list @t508 @t596 @t229 @t44) (=> (= @t508 @t599) (=> @t231 (_ @t598 @t597))))) % 0.44/0.83 (assume @p288 (forall (@list @t508 @t600 @t226 @t81) (=> (= @t508 @t602) (=> @t228 (_ @t598 @t601))))) % 0.44/0.83 (assume @p289 (forall @t350 (= (_ @t563 (_ (_ tptp.set_or656347191t_real @t255) @t267)) (_ (_ tptp.set_or656347191t_real (_ tptp.uminus_uminus_real @t267)) @t386)))) % 0.44/0.83 (assume @p290 (forall @t607 (= @t606 (exists @t605 (and @t604 (= @t111 (_ @t572 @t603))))))) % 0.44/0.83 (assume @p291 (forall @t609 (= @t608 (exists @t605 (and @t604 (= @t95 (_ @t565 @t603))))))) % 0.44/0.83 (assume @p292 (forall @t612 (= @t611 (exists (@list @t610) (and (_ (_ tptp.ord_le1772180283um_c_c @t610) @t44) (= @t95 (_ @t578 @t610))))))) % 0.44/0.83 (assume @p293 (forall (@list @t571 @t161 @t111) (= @t615 (forall @t165 (=> @t164 (_ (_ tptp.member_Sum_sum_c_d @t613) @t111)))))) % 0.44/0.83 (assume @p294 (forall (@list @t564 @t161 @t95) (= @t618 (forall @t165 (=> @t164 (_ (_ tptp.member_Sum_sum_c_c @t616) @t95)))))) % 0.44/0.83 (assume @p295 (forall @t607 (=> @t606 (not (forall @t621 (=> @t620 (not (= @t111 (_ @t572 @t619))))))))) % 0.44/0.83 (assume @p296 (forall @t609 (=> @t608 (not (forall @t621 (=> @t620 (not (= @t95 (_ @t565 @t619))))))))) % 0.44/0.83 (assume @p297 (forall @t612 (=> @t611 (not (forall (@list @t622) (=> (_ (_ tptp.ord_le1772180283um_c_c @t622) @t44) (not (= @t95 (_ @t578 @t622))))))))) % 0.44/0.83 (assume @p298 (forall (@list @t161 @t571 @t111) (=> (forall @t177 (=> @t624 (_ (_ tptp.member_Sum_sum_c_d @t623) @t111))) @t615))) % 0.44/0.83 (assume @p299 (forall (@list @t161 @t564 @t95) (=> (forall @t177 (=> @t624 (_ (_ tptp.member_Sum_sum_c_c @t625) @t95))) @t618))) % 0.44/0.83 (assume @p300 (forall (@list @t44 @t581 @t111) (=> (forall @t122 (=> @t121 (_ (_ tptp.member_Sum_sum_c_d (_ @t581 @t118)) @t111))) (_ (_ tptp.ord_le764260924um_c_d @t582) @t111)))) % 0.44/0.83 (assume @p301 (forall (@list @t81 @t587 @t111) (=> (forall @t117 (=> @t116 (_ (_ tptp.member_Sum_sum_c_d (_ @t587 @t113)) @t111))) (_ (_ tptp.ord_le764260924um_c_d @t588) @t111)))) % 0.44/0.83 (assume @p302 (forall (@list @t44 @t577 @t95) (=> (forall @t122 (=> @t121 (_ (_ tptp.member_Sum_sum_c_c (_ @t577 @t118)) @t95))) (_ @t626 @t95)))) % 0.44/0.83 (assume @p303 (forall (@list @t81 @t584 @t95) (=> (forall @t117 (=> @t116 (_ (_ tptp.member_Sum_sum_c_c (_ @t584 @t113)) @t95))) (_ (_ tptp.ord_le1772180283um_c_c @t585) @t95)))) % 0.44/0.83 (assume @p304 (forall (@list @t74 @t593 @t111) (=> (forall @t110 (=> @t109 (_ (_ tptp.member_Sum_sum_c_d (_ @t593 @t106)) @t111))) (_ (_ tptp.ord_le764260924um_c_d @t594) @t111)))) % 0.44/0.83 (assume @p305 (forall (@list @t44 @t596 @t104) (=> (forall @t122 (=> @t121 (_ (_ tptp.member1895684704real_c (_ @t596 @t118)) @t104))) (_ (_ tptp.ord_le977353143real_c @t597) @t104)))) % 0.44/0.83 (assume @p306 (forall (@list @t81 @t600 @t104) (=> (forall @t117 (=> @t116 (_ (_ tptp.member1895684704real_c (_ @t600 @t113)) @t104))) (_ (_ tptp.ord_le977353143real_c @t601) @t104)))) % 0.44/0.83 (assume @p307 (forall (@list @t74 @t590 @t95) (=> (forall @t110 (=> @t109 (_ (_ tptp.member_Sum_sum_c_c (_ @t590 @t106)) @t95))) (_ (_ tptp.ord_le1772180283um_c_c @t591) @t95)))) % 0.44/0.83 (assume @p308 (forall (@list @t161 @t521 @t571) (=> @t627 (_ @t614 (_ @t572 @t521))))) % 0.44/0.83 (assume @p309 (forall (@list @t161 @t521 @t564) (=> @t627 (_ @t617 (_ @t565 @t521))))) % 0.44/0.83 (assume @p310 (forall (@list @t44 @t95 @t577) (=> @t103 (_ @t626 (_ @t578 @t95))))) % 0.44/0.83 (assume @p311 (forall @t505 (=> @t504 (=> (_ (_ tptp.ord_le1327118209real_c (_ (_ tptp.image_327677598real_c @t499) @t489)) @t497) @t502)))) % 0.44/0.83 (assume @p312 (forall (@list @t537 @t161 @t564) (=> @t569 (_ (_ tptp.member_Sum_sum_c_c @t570) @t566)))) % 0.44/0.83 (assume @p313 (forall (@list @t537 @t161 @t571) (=> @t569 (_ (_ tptp.member_Sum_sum_c_d @t576) @t573)))) % 0.44/0.83 (assume @p314 (forall (@list @t229 @t44 @t577) (=> @t231 (_ (_ tptp.member_Sum_sum_c_c @t580) @t579)))) % 0.44/0.83 (assume @p315 (forall (@list @t229 @t44 @t581) (=> @t231 (_ (_ tptp.member_Sum_sum_c_d @t583) @t582)))) % 0.44/0.83 (assume @p316 (forall (@list @t226 @t81 @t584) (=> @t228 (_ (_ tptp.member_Sum_sum_c_c @t586) @t585)))) % 0.44/0.83 (assume @p317 (forall (@list @t226 @t81 @t587) (=> @t228 (_ (_ tptp.member_Sum_sum_c_d @t589) @t588)))) % 0.44/0.83 (assume @p318 (forall (@list @t223 @t74 @t590) (=> @t225 (_ (_ tptp.member_Sum_sum_c_c @t592) @t591)))) % 0.44/0.83 (assume @p319 (forall (@list @t223 @t74 @t593) (=> @t225 (_ (_ tptp.member_Sum_sum_c_d @t595) @t594)))) % 0.44/0.83 (assume @p320 (forall (@list @t229 @t44 @t596) (=> @t231 (_ (_ tptp.member1895684704real_c @t599) @t597)))) % 0.44/0.83 (assume @p321 (forall (@list @t226 @t81 @t600) (=> @t228 (_ (_ tptp.member1895684704real_c @t602) @t601)))) % 0.44/0.83 (assume @p322 (forall (@list @t628 @t564 @t161) (= (_ (_ tptp.member_Sum_sum_c_c @t628) @t566) (exists @t165 (and @t164 (= @t628 @t616)))))) % 0.44/0.83 (assume @p323 (forall (@list @t629 @t571 @t161) (= (_ (_ tptp.member_Sum_sum_c_d @t629) @t573) (exists @t165 (and @t164 (= @t629 @t613)))))) % 0.44/0.83 (assume @p324 (forall (@list @t564 @t161 @t134) (=> (exists (@list @t630) (and (_ (_ tptp.member_Sum_sum_c_c @t630) @t566) (_ @t134 @t630))) (exists @t177 (and @t624 (_ @t134 @t625)))))) % 0.44/0.83 (assume @p325 (forall (@list @t571 @t161 @t137) (=> (exists (@list @t631) (and (_ (_ tptp.member_Sum_sum_c_d @t631) @t573) (_ @t137 @t631))) (exists @t177 (and @t624 (_ @t137 @t623)))))) % 0.44/0.83 (assume @p326 (forall (@list @t634 @t632 @t564 @t633) (=> @t636 (=> (forall @t177 (=> @t635 (= @t625 (_ @t633 @t174)))) (= (_ @t565 @t634) (_ (_ tptp.image_c_Sum_sum_c_c @t633) @t632)))))) % 0.44/0.83 (assume @p327 (forall (@list @t634 @t632 @t571 @t637) (=> @t636 (=> (forall @t177 (=> @t635 (= @t623 (_ @t637 @t174)))) (= (_ @t572 @t634) (_ (_ tptp.image_c_Sum_sum_c_d @t637) @t632)))))) % 0.44/0.83 (assume @p328 (_ (_ tptp.ord_le1772180283um_c_c (_ @t639 @t638)) tptp.v)) % 0.44/0.83 (assume @p329 (_ (_ (_ tptp.denota256060419gree_c (_ tptp.sol tptp.zero_zero_real)) tptp.a) (_ tptp.collect_c (lambda (@list @t640) (or (_ @t641 @t40) (_ (_ tptp.member_Sum_sum_c_d (_ tptp.sum_Inl_c_d @t640)) (_ (_ tptp.image_c_Sum_sum_c_d tptp.sum_Inl_c_d) @t638)) (_ @t641 @t272)))))) % 0.44/0.83 (assume @p330 (_ (_ tptp.ord_le1772180283um_c_c (_ (_ tptp.sup_su1349021703um_c_c (_ @t639 @t642)) (_ (_ tptp.image_c_Sum_sum_c_c tptp.sum_Inr_c_c) @t642))) tptp.v)) % 0.44/0.83 (assume @p331 @t643) % 0.44/0.83 (assume @p332 true) % 0.44/0.83 (step @p333 (= tptp.ord_le977353143real_c @t646) :rule refl :args (@t646)) % 0.44/0.83 (step @p334 (= tptp.ord_le764260924um_c_d @t649) :rule refl :args (@t649)) % 0.44/0.83 (step @p335 (= tptp.ord_le1772180283um_c_c @t652) :rule refl :args (@t652)) % 0.44/0.83 (step @p336 (= tptp.bNF_Ca1693016812um_c_c @t659) :rule refl :args (@t659)) % 0.44/0.83 (step @p337 (= tptp.bNF_Ca449034301c_real @t661) :rule refl :args (@t661)) % 0.44/0.83 (step @p338 (= tptp.coinci501627771_a_b_c @t667) :rule refl :args (@t667)) % 0.44/0.83 (step @p339 (= tptp.coinci1852866155_a_b_c @t669) :rule refl :args (@t669)) % 0.44/0.83 (step @p340 (= tptp.uminus232257166real_c @t670) :rule refl :args (@t670)) % 0.44/0.83 (step @p341 (= tptp.uminus373867045um_c_d @t671) :rule refl :args (@t671)) % 0.44/0.83 (step @p342 (= tptp.uminus102402154real_c @t672) :rule refl :args (@t672)) % 0.44/0.83 (step @p343 (= tptp.uminus_uminus_set_c @t673) :rule refl :args (@t673)) % 0.44/0.83 (step @p344 (= tptp.uminus1381786404um_c_c @t674) :rule refl :args (@t674)) % 0.44/0.83 (step @p345 (= tptp.denota1896987029_a_b_c @t679) :rule refl :args (@t679)) % 0.44/0.83 (step @p346 (= tptp.denota161327353_a_b_c @t688) :rule refl :args (@t688)) % 0.44/0.83 (step @p347 (= tptp.set_or2003963744real_c @t690) :rule refl :args (@t690)) % 0.44/0.83 (step @p348 (= tptp.set_or2028906832um_c_c @t692) :rule refl :args (@t692)) % 0.44/0.83 (step @p349 (= tptp.set_ord_atLeast_real @t694) :rule refl :args (@t694)) % 0.44/0.83 (step @p350 (= tptp.set_or1478397028real_c @t696) :rule refl :args (@t696)) % 0.44/0.83 (step @p351 (= tptp.set_or326480468um_c_c @t698) :rule refl :args (@t698)) % 0.44/0.83 (step @p352 (= tptp.set_ord_atMost_real @t700) :rule refl :args (@t700)) % 0.44/0.83 (step @p353 :rule refl :args (@t2)) % 0.44/0.83 (step @p354 :rule beta-reduce :args ((= (_ @t706 @t3) @t703))) % 0.44/0.83 (step @p355 :rule refl :args (@t3)) % 0.44/0.83 (step @p356 :rule beta-reduce :args ((= (_ @t709 tptp.ode) @t706))) % 0.44/0.83 (step @p357 :rule refl :args (tptp.ode)) % 0.44/0.83 (step @p358 :rule beta-reduce :args ((= @t710 @t709))) % 0.44/0.83 (step @p359 :rule ho_cong :premises (@p358 @p357)) % 0.44/0.83 (step @p360 :rule trans :premises (@p359 @p356)) % 0.44/0.83 (step @p361 :rule ho_cong :premises (@p360 @p355)) % 0.44/0.83 (step @p362 :rule trans :premises (@p361 @p354)) % 0.44/0.83 (step @p363 :rule beta-reduce :args ((= (_ @t714 @t3) (_ tptp.the_Pr1290640446real_c (lambda @t685 (and @t712 (_ (_ @t682 @t703) @t2))))))) % 0.44/0.83 (step @p364 :rule beta-reduce :args ((= (_ @t715 @t4) @t714))) % 0.44/0.83 (step @p365 :rule refl :args (@t4)) % 0.44/0.83 (step @p366 :rule beta-reduce :args ((= (_ @t717 tptp.ode) @t715))) % 0.44/0.83 (step @p367 :rule beta-reduce :args ((= @t719 @t717))) % 0.44/0.83 (step @p368 :rule ho_cong :premises (@p367 @p357)) % 0.44/0.83 (step @p369 :rule trans :premises (@p368 @p366)) % 0.44/0.83 (step @p370 :rule ho_cong :premises (@p369 @p365)) % 0.44/0.83 (step @p371 :rule trans :premises (@p370 @p364)) % 0.44/0.83 (step @p372 :rule ho_cong :premises (@p371 @p355)) % 0.44/0.83 (step @p373 :rule trans :premises (@p372 @p363)) % 0.44/0.83 (step @p374 :rule refl :args (tptp.denota1997846518gree_c)) % 0.44/0.83 (step @p375 :rule ho_cong :premises (@p374 @p373)) % 0.44/0.83 (step @p376 :rule ho_cong :premises (@p375 @p362)) % 0.44/0.83 (step @p377 :rule ho_cong :premises (@p376 @p353)) % 0.44/0.83 (step @p378 :rule cong :premises (@p377) :args ((not (_ (_ (_ tptp.denota1997846518gree_c (_ (_ (_ @t719 tptp.ode) @t4) @t3)) (_ (_ @t710 tptp.ode) @t3)) @t2)))) % 0.44/0.83 (step @p379 :rule refl :args (tptp.j)) % 0.44/0.83 (step @p380 :rule ho_cong :premises (@p345 @p379)) % 0.44/0.83 (step @p381 :rule ho_cong :premises (@p380 @p357)) % 0.44/0.83 (step @p382 :rule ho_cong :premises (@p381 @p355)) % 0.44/0.83 (step @p383 :rule refl :args (@t680)) % 0.44/0.83 (step @p384 :rule beta-reduce :args ((= (_ @t720 @t675) @t678))) % 0.44/0.83 (step @p385 :rule refl :args (@t675)) % 0.44/0.83 (step @p386 :rule beta-reduce :args ((= (_ @t721 @t676) @t720))) % 0.44/0.83 (step @p387 :rule refl :args (@t676)) % 0.44/0.83 (step @p388 :rule beta-reduce :args ((= @t722 @t721))) % 0.44/0.83 (step @p389 :rule ho_cong :premises (@p388 @p387)) % 0.44/0.83 (step @p390 :rule trans :premises (@p389 @p386)) % 0.44/0.83 (step @p391 :rule ho_cong :premises (@p390 @p385)) % 0.44/0.83 (step @p392 :rule trans :premises (@p391 @p384)) % 0.44/0.83 (step @p393 :rule refl :args (@t682)) % 0.44/0.83 (step @p394 :rule ho_cong :premises (@p393 @p392)) % 0.44/0.83 (step @p395 :rule ho_cong :premises (@p394 @p383)) % 0.44/0.83 (step @p396 :rule beta-reduce :args ((= @t723 @t718))) % 0.44/0.83 (step @p397 :rule refl :args (@t683)) % 0.44/0.83 (step @p398 :rule ho_cong :premises (@p397 @p396)) % 0.44/0.83 (step @p399 :rule nary_cong :premises (@p398 @p395) :args (@t724)) % 0.44/0.83 (step @p400 :rule cong :premises (@p399) :args ((lambda @t685 @t724))) % 0.44/0.83 (step @p401 :rule refl :args (tptp.the_Pr1290640446real_c)) % 0.44/0.83 (step @p402 :rule ho_cong :premises (@p401 @p400)) % 0.44/0.83 (step @p403 :rule refl :args (@t665)) % 0.44/0.83 (step @p404 :rule ho_cong :premises (@p345 @p403)) % 0.44/0.83 (step @p405 :rule ho_cong :premises (@p404 @p387)) % 0.44/0.83 (step @p406 :rule ho_cong :premises (@p405 @p385)) % 0.44/0.83 (step @p407 :rule ho_cong :premises (@p393 @p406)) % 0.44/0.83 (step @p408 :rule ho_cong :premises (@p407 @p383)) % 0.44/0.83 (step @p409 :rule ho_cong :premises (@p344 @p383)) % 0.44/0.83 (step @p410 :rule ho_cong :premises (@p397 @p409)) % 0.44/0.83 (step @p411 :rule nary_cong :premises (@p410 @p408) :args (@t684)) % 0.44/0.83 (step @p412 :rule cong :premises (@p411) :args (@t686)) % 0.44/0.83 (step @p413 :rule ho_cong :premises (@p401 @p412)) % 0.44/0.83 (step @p414 :rule trans :premises (@p413 @p402)) % 0.44/0.83 (step @p415 :rule cong :premises (@p414) :args (@t688)) % 0.44/0.83 (step @p416 :rule trans :premises (@p346 @p415)) % 0.44/0.83 (step @p417 :rule ho_cong :premises (@p416 @p379)) % 0.44/0.83 (step @p418 :rule ho_cong :premises (@p417 @p357)) % 0.44/0.83 (step @p419 :rule ho_cong :premises (@p418 @p365)) % 0.44/0.83 (step @p420 :rule ho_cong :premises (@p419 @p355)) % 0.44/0.83 (step @p421 :rule ho_cong :premises (@p374 @p420)) % 0.44/0.83 (step @p422 :rule ho_cong :premises (@p421 @p382)) % 0.44/0.83 (step @p423 :rule ho_cong :premises (@p422 @p353)) % 0.44/0.83 (step @p424 :rule cong :premises (@p423) :args (@t643)) % 0.44/0.83 (step @p425 :rule trans :premises (@p424 @p378)) % 0.44/0.83 (step @p426 :rule eq_resolve :premises (@p331 @p425)) % 0.44/0.83 (step @p427 :rule trans :premises (@p423 @p377)) % 0.44/0.83 (step @p428 :rule and_elim :premises (@p2) :args (1)) % 0.44/0.83 (step @p429 :rule eq_resolve :premises (@p428 @p427)) % 0.44/0.83 (step @p430 false :rule contra :premises (@p429 @p426)) % 0.44/0.83 ) % 0.44/0.83 % SZS output end Proof % 0.44/0.83 % cvc5 exiting %------------------------------------------------------------------------------