cvc5---1.3.4.THM-Prf.s

%------------------------------------------------------------------------------
% File     : cvc5---1.3.4
% Problem  : ITP038^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.46s 0.87s
% Output   : Proof 0.46s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem  : ITP038^1 : TPTP v9.2.1. Released v7.5.0.
% 0.00/0.13  % Command  : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.15/0.34  % Computer : n018.cluster.edu
% 0.15/0.34  % Model    : x86_64 x86_64
% 0.15/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34  % Memory   : 8042.1875MB
% 0.15/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34  % CPULimit : 300
% 0.15/0.34  % WCLimit  : 300
% 0.15/0.34  % DateTime : Tue Jun  2 04:11:20 EDT 2026
% 0.15/0.34  % CPUTime  : 
% 0.38/0.61  %----Proving TH0
% 0.46/0.87  --- 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.46/0.87  % SZS status Theorem
% 0.46/0.87  % SZS output start Proof
% 0.46/0.87  (
% 0.46/0.87  (declare-sort tptp.denota610675952t_unit 0)
% 0.46/0.87  (declare-sort tptp.trm_sf_sz 0)
% 0.46/0.87  (declare-sort tptp.frechet_strm_sf_sz 0)
% 0.46/0.87  (declare-sort tptp.trm_a_c 0)
% 0.46/0.87  (declare-sort tptp.frechet_strm_a_c 0)
% 0.46/0.87  (declare-sort tptp.freche2095075217_sc_sz 0)
% 0.46/0.87  (declare-sort tptp.set_Fi291318197eal_sz 0)
% 0.46/0.87  (declare-sort tptp.finite824932053eal_sz 0)
% 0.46/0.87  (declare-sort tptp.produc1892666919z_real 0)
% 0.46/0.87  (declare-sort tptp.real 0)
% 0.46/0.87  (declare-sort tptp.bounde472938360z_real 0)
% 0.46/0.87  (declare-sort tptp.formula_sf_sc_sz 0)
% 0.46/0.87  (declare-sort tptp.sz 0)
% 0.46/0.87  (declare-sort tptp.sf 0)
% 0.46/0.87  (declare-sort tptp.sc 0)
% 0.46/0.87  (declare-sort tptp.denota231621370t_unit 0)
% 0.46/0.87  (declare-sort tptp.set_Su1783761653um_b_c 0)
% 0.46/0.87  (declare-sort tptp.set_trm_a_c 0)
% 0.46/0.87  (declare-sort tptp.sum_su737395349um_b_c 0)
% 0.46/0.87  (declare-sort tptp.set_trm_sf_sz 0)
% 0.46/0.87  (declare-sort tptp.c 0)
% 0.46/0.87  (declare-sort tptp.produc190496183real_c 0)
% 0.46/0.87  (declare-sort tptp.set_Sum_sum_c_c 0)
% 0.46/0.87  (declare-sort tptp.produc1065634396_o_a_o 0)
% 0.46/0.87  (declare-sort tptp.a 0)
% 0.46/0.87  (declare-sort tptp.produc1989635468_a_a_o 0)
% 0.46/0.87  (declare-sort tptp.produc1149990247eal_sz 0)
% 0.46/0.87  (declare-sort tptp.set_Sum_sum_sz_sz 0)
% 0.46/0.87  (declare-sort tptp.set_De455519194t_unit 0)
% 0.46/0.87  (declare-sort tptp.freche914690577_a_b_c 0)
% 0.46/0.87  (declare-sort tptp.set_a 0)
% 0.46/0.87  (declare-sort tptp.finite1398487019real_c 0)
% 0.46/0.87  (declare-sort tptp.set_Pr1169339874_sc_sz 0)
% 0.46/0.87  (declare-sort tptp.produc866628903_sc_sz 0)
% 0.46/0.87  (declare-sort tptp.produc1821101996_sc_sz 0)
% 0.46/0.87  (declare-sort tptp.produc1553439972f_sz_o 0)
% 0.46/0.87  (declare-sort tptp.product_prod_a_o_a_o 0)
% 0.46/0.87  (declare-sort tptp.list_f1238882004_sc_sz 0)
% 0.46/0.87  (declare-sort tptp.produc903182423_set_a 0)
% 0.46/0.87  (declare-sort tptp.produc1144880887f_sz_o 0)
% 0.46/0.87  (declare-sort tptp.set_De208295462t_unit 0)
% 0.46/0.87  (declare-sort tptp.produc1561113620_set_a 0)
% 0.46/0.87  (declare-sort tptp.produc1691597095_set_a 0)
% 0.46/0.87  (declare-sort tptp.produc1241881959eal_sz 0)
% 0.46/0.87  (declare-const tptp.freche1421597129_sc_sz (-> tptp.freche2095075217_sc_sz tptp.denota610675952t_unit))
% 0.46/0.87  (declare-const tptp.freche782854530_sf_sz (-> tptp.frechet_strm_sf_sz tptp.trm_sf_sz))
% 0.46/0.87  (declare-const tptp.frechet_raw_term_a_c (-> tptp.frechet_strm_a_c tptp.trm_a_c))
% 0.46/0.87  (declare-const tptp.produc314122909real_c (-> tptp.produc190496183real_c tptp.finite1398487019real_c))
% 0.46/0.87  (declare-const tptp.produc2010422875real_c (-> tptp.produc190496183real_c tptp.finite1398487019real_c))
% 0.46/0.87  (declare-const tptp.denota229585092_a_b_c (-> tptp.denota231621370t_unit tptp.trm_a_c tptp.finite1398487019real_c tptp.finite1398487019real_c tptp.real))
% 0.46/0.87  (declare-const tptp.produc1269210629eal_sz (-> tptp.produc1149990247eal_sz tptp.finite824932053eal_sz))
% 0.46/0.87  (declare-const tptp.produc1111759555eal_sz (-> tptp.produc1149990247eal_sz tptp.finite824932053eal_sz))
% 0.46/0.87  (declare-const tptp.denota1979904720_sc_sz (-> tptp.denota610675952t_unit tptp.trm_sf_sz tptp.finite824932053eal_sz tptp.finite824932053eal_sz tptp.real))
% 0.46/0.87  (declare-const tptp.ord_le775706699real_c (-> tptp.finite1398487019real_c tptp.finite1398487019real_c Bool))
% 0.46/0.87  (declare-const tptp.produc918972485_set_a (-> tptp.produc1691597095_set_a tptp.set_a))
% 0.46/0.87  (declare-const tptp.member_a (-> tptp.a tptp.set_a Bool))
% 0.46/0.87  (declare-const tptp.produc1926412547_set_a (-> tptp.produc1691597095_set_a tptp.set_a))
% 0.46/0.87  (declare-const tptp.produc23639768_a_a_o (-> tptp.produc1989635468_a_a_o tptp.a Bool))
% 0.46/0.87  (declare-const tptp.ord_less_eq_a_o (-> (-> tptp.a Bool) (-> tptp.a Bool) Bool))
% 0.46/0.87  (declare-const tptp.produc1911461786_a_a_o (-> tptp.produc1989635468_a_a_o tptp.set_a))
% 0.46/0.87  (declare-const tptp.produc1305389080_set_a (-> tptp.produc1561113620_set_a tptp.set_a))
% 0.46/0.87  (declare-const tptp.produc1045727450_set_a (-> tptp.produc1561113620_set_a tptp.a Bool))
% 0.46/0.87  (declare-const tptp.ord_le787639925eal_sz (-> tptp.finite824932053eal_sz tptp.finite824932053eal_sz Bool))
% 0.46/0.87  (declare-const tptp.product_snd_a_o_a_o (-> tptp.product_prod_a_o_a_o tptp.a Bool))
% 0.46/0.87  (declare-const tptp.product_fst_a_o_a_o (-> tptp.product_prod_a_o_a_o tptp.a Bool))
% 0.46/0.87  (declare-const tptp.produc407510293f_sz_o (-> tptp.produc1144880887f_sz_o tptp.trm_sf_sz tptp.trm_sf_sz Bool))
% 0.46/0.87  (declare-const tptp.ord_le8515534f_sz_o (-> (-> tptp.trm_sf_sz tptp.trm_sf_sz Bool) (-> tptp.trm_sf_sz tptp.trm_sf_sz Bool) Bool))
% 0.46/0.87  (declare-const tptp.produc38604755f_sz_o (-> tptp.produc1144880887f_sz_o tptp.set_a))
% 0.46/0.87  (declare-const tptp.produc776178293_set_a (-> tptp.produc903182423_set_a tptp.set_a))
% 0.46/0.87  (declare-const tptp.produc407272755_set_a (-> tptp.produc903182423_set_a tptp.trm_sf_sz tptp.trm_sf_sz Bool))
% 0.46/0.87  (declare-const tptp.produc1630531752_o_a_o (-> tptp.produc1065634396_o_a_o tptp.a Bool))
% 0.46/0.87  (declare-const tptp.produc2013638506_o_a_o (-> tptp.produc1065634396_o_a_o tptp.trm_sf_sz tptp.trm_sf_sz Bool))
% 0.46/0.87  (declare-const tptp.produc1070758376f_sz_o (-> tptp.produc1553439972f_sz_o tptp.trm_sf_sz tptp.trm_sf_sz Bool))
% 0.46/0.87  (declare-const tptp.produc1453865130f_sz_o (-> tptp.produc1553439972f_sz_o tptp.a Bool))
% 0.46/0.87  (declare-const tptp.empty_sz_sf (-> tptp.sz tptp.trm_sf_sz))
% 0.46/0.87  (declare-const tptp.function_sf_sz (-> tptp.sf (-> tptp.sz tptp.trm_sf_sz) tptp.trm_sf_sz))
% 0.46/0.87  (declare-const tptp.produc789536734_sc_sz (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz tptp.produc1821101996_sc_sz))
% 0.46/0.87  (declare-const tptp.collec1199592193_sc_sz (-> (-> tptp.produc1821101996_sc_sz Bool) tptp.set_Pr1169339874_sc_sz))
% 0.46/0.87  (declare-const tptp.top_to1499569298_sc_sz tptp.set_Pr1169339874_sc_sz)
% 0.46/0.87  (declare-const tptp.member1057565379_sc_sz (-> tptp.produc1821101996_sc_sz tptp.set_Pr1169339874_sc_sz Bool))
% 0.46/0.87  (declare-const tptp.ord_le2003534918unit_o (-> (-> tptp.denota610675952t_unit tptp.denota610675952t_unit Bool) (-> tptp.denota610675952t_unit tptp.denota610675952t_unit Bool) Bool))
% 0.46/0.87  (declare-const tptp.quotie1549861309_sf_sz (-> (-> tptp.trm_sf_sz tptp.trm_sf_sz Bool) (-> tptp.trm_sf_sz tptp.frechet_strm_sf_sz) (-> tptp.frechet_strm_sf_sz tptp.trm_sf_sz) (-> tptp.trm_sf_sz tptp.frechet_strm_sf_sz Bool) Bool))
% 0.46/0.87  (declare-const tptp.quotie1467858509rm_a_c (-> (-> tptp.trm_a_c tptp.trm_a_c Bool) (-> tptp.trm_a_c tptp.frechet_strm_a_c) (-> tptp.frechet_strm_a_c tptp.trm_a_c) (-> tptp.trm_a_c tptp.frechet_strm_a_c Bool) Bool))
% 0.46/0.87  (declare-const tptp.quotie842200089_sc_sz (-> (-> tptp.denota610675952t_unit tptp.denota610675952t_unit Bool) (-> tptp.denota610675952t_unit tptp.freche2095075217_sc_sz) (-> tptp.freche2095075217_sc_sz tptp.denota610675952t_unit) (-> tptp.denota610675952t_unit tptp.freche2095075217_sc_sz Bool) Bool))
% 0.46/0.87  (declare-const tptp.bNF_eq1660582207t_unit (-> (-> tptp.denota610675952t_unit Bool) tptp.denota610675952t_unit tptp.denota610675952t_unit Bool))
% 0.46/0.87  (declare-const tptp.topolo1027477648z_real (-> tptp.set_Fi291318197eal_sz (-> tptp.finite824932053eal_sz tptp.produc1892666919z_real) Bool))
% 0.46/0.87  (declare-const tptp.top_to1660572043um_c_c tptp.set_Sum_sum_c_c)
% 0.46/0.87  (declare-const tptp.top_to646513176l_sz_o (-> tptp.finite824932053eal_sz Bool))
% 0.46/0.87  (declare-const tptp.bNF_eq_onp_trm_a_c (-> (-> tptp.trm_a_c Bool) tptp.trm_a_c tptp.trm_a_c Bool))
% 0.46/0.87  (declare-const tptp.top_to1201357528_b_c_o (-> tptp.sum_su737395349um_b_c Bool))
% 0.46/0.87  (declare-const tptp.freche585307148_sc_sz (-> tptp.freche2095075217_sc_sz tptp.frechet_strm_sf_sz tptp.finite824932053eal_sz tptp.bounde472938360z_real))
% 0.46/0.87  (declare-const tptp.top_to524132421um_b_c tptp.set_Su1783761653um_b_c)
% 0.46/0.87  (declare-const tptp.ids_sz_sf_sc (-> tptp.sz tptp.sz tptp.sz tptp.sf tptp.sf tptp.sf tptp.sc tptp.sc tptp.sc tptp.sc Bool))
% 0.46/0.87  (declare-const tptp.top_top_set_a tptp.set_a)
% 0.46/0.87  (declare-const tptp.topolo885751137z_real (-> tptp.set_Fi291318197eal_sz (-> tptp.finite824932053eal_sz tptp.bounde472938360z_real) Bool))
% 0.46/0.87  (declare-const tptp.if_Bou1785791806z_real (-> Bool tptp.bounde472938360z_real tptp.bounde472938360z_real tptp.bounde472938360z_real))
% 0.46/0.87  (declare-const tptp.ord_le108471557c_sz_o (-> (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz Bool) (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz Bool) Bool))
% 0.46/0.87  (declare-const tptp.ord_less_eq_real (-> tptp.real tptp.real Bool))
% 0.46/0.87  (declare-const tptp.static_FVT_sf_sz (-> tptp.trm_sf_sz tptp.set_Sum_sum_sz_sz))
% 0.46/0.87  (declare-const tptp.topolo1348430467z_real (-> tptp.set_Fi291318197eal_sz (-> tptp.finite824932053eal_sz tptp.real) Bool))
% 0.46/0.87  (declare-const tptp.static_FVT_a_c (-> tptp.trm_a_c tptp.set_Sum_sum_c_c))
% 0.46/0.87  (declare-const tptp.type_d1092523951t_unit (-> (-> tptp.freche2095075217_sc_sz tptp.denota610675952t_unit) (-> tptp.denota610675952t_unit tptp.freche2095075217_sc_sz) tptp.set_De208295462t_unit Bool))
% 0.46/0.87  (declare-const tptp.member754147591t_unit (-> tptp.denota610675952t_unit tptp.set_De208295462t_unit Bool))
% 0.46/0.87  (declare-const tptp.collec1767975749t_unit (-> (-> tptp.denota610675952t_unit Bool) tptp.set_De208295462t_unit))
% 0.46/0.87  (declare-const tptp.member1777622435t_unit (-> tptp.denota231621370t_unit tptp.set_De455519194t_unit Bool))
% 0.46/0.87  (declare-const tptp.collec451781861t_unit (-> (-> tptp.denota231621370t_unit Bool) tptp.set_De455519194t_unit))
% 0.46/0.87  (declare-const tptp.freche1608036107_a_b_c (-> tptp.freche914690577_a_b_c tptp.denota231621370t_unit))
% 0.46/0.87  (declare-const tptp.freche1473475332_a_b_c (-> tptp.denota231621370t_unit tptp.freche914690577_a_b_c))
% 0.46/0.87  (declare-const tptp.ord_le1369644495rm_a_c (-> tptp.set_trm_a_c tptp.set_trm_a_c Bool))
% 0.46/0.87  (declare-const tptp.ord_le1697056455_sf_sz (-> tptp.set_trm_sf_sz tptp.set_trm_sf_sz Bool))
% 0.46/0.87  (declare-const tptp.type_d46389773_sf_sz (-> (-> tptp.frechet_strm_sf_sz tptp.trm_sf_sz) (-> tptp.trm_sf_sz tptp.frechet_strm_sf_sz) tptp.set_trm_sf_sz Bool))
% 0.46/0.87  (declare-const tptp.type_d1238563341rm_a_c (-> (-> tptp.frechet_strm_a_c tptp.trm_a_c) (-> tptp.trm_a_c tptp.frechet_strm_a_c) tptp.set_trm_a_c Bool))
% 0.46/0.87  (declare-const tptp.freche1784963216_sc_sz (-> tptp.denota610675952t_unit tptp.freche2095075217_sc_sz))
% 0.46/0.87  (declare-const tptp.produc1152932438_o_a_o (-> (-> tptp.trm_sf_sz tptp.trm_sf_sz Bool) (-> tptp.a Bool) tptp.produc1065634396_o_a_o))
% 0.46/0.87  (declare-const tptp.bounde397081123z_real (-> (-> tptp.finite824932053eal_sz tptp.real) tptp.bounde472938360z_real))
% 0.46/0.87  (declare-const tptp.produc1543226183_set_a (-> (-> tptp.trm_sf_sz tptp.trm_sf_sz Bool) tptp.set_a tptp.produc903182423_set_a))
% 0.46/0.87  (declare-const tptp.produc1174558183f_sz_o (-> tptp.set_a (-> tptp.trm_sf_sz tptp.trm_sf_sz Bool) tptp.produc1144880887f_sz_o))
% 0.46/0.87  (declare-const tptp.ord_le978883847eal_sz (-> tptp.produc1241881959eal_sz tptp.produc1241881959eal_sz Bool))
% 0.46/0.87  (declare-const tptp.collect_trm_sf_sz (-> (-> tptp.trm_sf_sz Bool) tptp.set_trm_sf_sz))
% 0.46/0.87  (declare-const tptp.denota2042094639_a_b_c (-> tptp.denota231621370t_unit tptp.trm_a_c tptp.finite1398487019real_c tptp.real))
% 0.46/0.87  (declare-const tptp.member_trm_a_c (-> tptp.trm_a_c tptp.set_trm_a_c Bool))
% 0.46/0.87  (declare-const tptp.collect_trm_a_c (-> (-> tptp.trm_a_c Bool) tptp.set_trm_a_c))
% 0.46/0.87  (declare-const tptp.produc593159062f_sz_o (-> (-> tptp.a Bool) (-> tptp.trm_sf_sz tptp.trm_sf_sz Bool) tptp.produc1553439972f_sz_o))
% 0.46/0.87  (declare-const tptp.denota69106024_a_b_c (-> tptp.denota231621370t_unit tptp.denota231621370t_unit tptp.set_Su1783761653um_b_c Bool))
% 0.46/0.87  (declare-const tptp.ord_le1230423618_sc_sz (-> tptp.set_Pr1169339874_sc_sz tptp.set_Pr1169339874_sc_sz Bool))
% 0.46/0.87  (declare-const tptp.sum_In2139678582um_b_c (-> tptp.a tptp.sum_su737395349um_b_c))
% 0.46/0.87  (declare-const tptp.p_sc_sf_sz (-> tptp.sc tptp.formula_sf_sc_sz))
% 0.46/0.87  (declare-const tptp.produc286845635eal_sz (-> tptp.produc1241881959eal_sz tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (declare-const tptp.function_a_c (-> tptp.a (-> tptp.c tptp.trm_a_c) tptp.trm_a_c))
% 0.46/0.87  (declare-const tptp.j tptp.denota231621370t_unit)
% 0.46/0.87  (declare-const tptp.predic913887884_sf_sz (-> tptp.sc tptp.formula_sf_sc_sz))
% 0.46/0.87  (declare-const tptp.ord_le929608341um_b_c (-> tptp.set_Su1783761653um_b_c tptp.set_Su1783761653um_b_c Bool))
% 0.46/0.87  (declare-const tptp.freche665377492rm_a_c (-> tptp.trm_a_c tptp.frechet_strm_a_c))
% 0.46/0.87  (declare-const tptp.nu tptp.produc190496183real_c)
% 0.46/0.87  (declare-const tptp.bNF_eq_onp_trm_sf_sz (-> (-> tptp.trm_sf_sz Bool) tptp.trm_sf_sz tptp.trm_sf_sz Bool))
% 0.46/0.87  (declare-const tptp.times_sf_sz (-> tptp.trm_sf_sz tptp.trm_sf_sz tptp.trm_sf_sz))
% 0.46/0.87  (declare-const tptp.top_to1787697847eal_sz tptp.produc1241881959eal_sz)
% 0.46/0.87  (declare-const tptp.plus_sf_sz (-> tptp.trm_sf_sz tptp.trm_sf_sz tptp.trm_sf_sz))
% 0.46/0.87  (declare-const tptp.plus_a_c (-> tptp.trm_a_c tptp.trm_a_c tptp.trm_a_c))
% 0.46/0.87  (declare-const tptp.t1 tptp.trm_a_c)
% 0.46/0.87  (declare-const tptp.dfree_a_c (-> tptp.trm_a_c Bool))
% 0.46/0.87  (declare-const tptp.produc548504323_sc_sz (-> tptp.produc866628903_sc_sz tptp.list_f1238882004_sc_sz))
% 0.46/0.87  (declare-const tptp.t2 tptp.trm_a_c)
% 0.46/0.87  (declare-const tptp.produc1503602930_sc_sz (-> tptp.produc1821101996_sc_sz tptp.denota610675952t_unit))
% 0.46/0.87  (declare-const tptp.ord_le1110131657_sz_sz (-> tptp.set_Sum_sum_sz_sz tptp.set_Sum_sum_sz_sz Bool))
% 0.46/0.87  (declare-const tptp.nu2 tptp.produc190496183real_c)
% 0.46/0.87  (declare-const tptp.freche1046279700_sf_sz (-> tptp.trm_sf_sz tptp.frechet_strm_sf_sz))
% 0.46/0.87  (declare-const tptp.produc870616579z_real (-> tptp.produc1892666919z_real tptp.bounde472938360z_real))
% 0.46/0.87  (declare-const tptp.dfree_sf_sz (-> tptp.trm_sf_sz Bool))
% 0.46/0.87  (declare-const tptp.ord_le1772180283um_c_c (-> tptp.set_Sum_sum_c_c tptp.set_Sum_sum_c_c Bool))
% 0.46/0.87  (declare-const tptp.denota1179238309_sc_sz (-> tptp.denota610675952t_unit tptp.trm_sf_sz tptp.finite824932053eal_sz tptp.real))
% 0.46/0.87  (declare-const tptp.member_trm_sf_sz (-> tptp.trm_sf_sz tptp.set_trm_sf_sz Bool))
% 0.46/0.87  (declare-const tptp.static_SIGT_a_c (-> tptp.trm_a_c tptp.set_a))
% 0.46/0.87  (declare-const tptp.ord_le41263445eal_sz (-> tptp.set_Fi291318197eal_sz tptp.set_Fi291318197eal_sz Bool))
% 0.46/0.87  (declare-const tptp.top_to1873962757eal_sz tptp.set_Fi291318197eal_sz)
% 0.46/0.87  (declare-const tptp.times_a_c (-> tptp.trm_a_c tptp.trm_a_c tptp.trm_a_c))
% 0.46/0.87  (declare-const tptp.produc4753477_sc_sz (-> tptp.produc866628903_sc_sz tptp.list_f1238882004_sc_sz))
% 0.46/0.87  (declare-const tptp.produc784663575z_real (-> tptp.bounde472938360z_real tptp.bounde472938360z_real tptp.produc1892666919z_real))
% 0.46/0.87  (declare-const tptp.denota258389581_a_b_c (-> tptp.denota231621370t_unit Bool))
% 0.46/0.87  (declare-const tptp.produc1822718231_sc_sz (-> tptp.list_f1238882004_sc_sz tptp.list_f1238882004_sc_sz tptp.produc866628903_sc_sz))
% 0.46/0.87  (declare-const tptp.collec2086029184um_b_c (-> (-> tptp.sum_su737395349um_b_c Bool) tptp.set_Su1783761653um_b_c))
% 0.46/0.87  (declare-const tptp.produc1746886149eal_sz (-> tptp.produc1241881959eal_sz tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (declare-const tptp.produc1235791063eal_sz (-> tptp.set_Fi291318197eal_sz tptp.set_Fi291318197eal_sz tptp.produc1241881959eal_sz))
% 0.46/0.87  (declare-const tptp.produc1422611269z_real (-> tptp.produc1892666919z_real tptp.bounde472938360z_real))
% 0.46/0.87  (declare-const tptp.produc1308130519eal_sz (-> tptp.finite824932053eal_sz tptp.finite824932053eal_sz tptp.produc1149990247eal_sz))
% 0.46/0.87  (declare-const tptp.produc974239792_sc_sz (-> tptp.produc1821101996_sc_sz tptp.produc866628903_sc_sz))
% 0.46/0.87  (declare-const tptp.produc394644079real_c (-> tptp.finite1398487019real_c tptp.finite1398487019real_c tptp.produc190496183real_c))
% 0.46/0.87  (declare-const tptp.collec1002602816eal_sz (-> (-> tptp.finite824932053eal_sz Bool) tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (declare-const tptp.member1693951742eal_sz (-> tptp.finite824932053eal_sz tptp.set_Fi291318197eal_sz Bool))
% 0.46/0.87  (declare-const tptp.produc634809990_a_a_o (-> tptp.set_a (-> tptp.a Bool) tptp.produc1989635468_a_a_o))
% 0.46/0.87  (declare-const tptp.collect_a (-> (-> tptp.a Bool) tptp.set_a))
% 0.46/0.87  (declare-const tptp.denota1579475975_sc_sz (-> tptp.denota610675952t_unit Bool))
% 0.46/0.87  (declare-const tptp.member1893232190um_b_c (-> tptp.sum_su737395349um_b_c tptp.set_Su1783761653um_b_c Bool))
% 0.46/0.87  (declare-const tptp.static_FVDiff_sf_sz (-> tptp.trm_sf_sz tptp.set_Sum_sum_sz_sz))
% 0.46/0.87  (declare-const tptp.i tptp.denota231621370t_unit)
% 0.46/0.87  (declare-const tptp.produc1928581911_set_a (-> tptp.set_a tptp.set_a tptp.produc1691597095_set_a))
% 0.46/0.87  (declare-const tptp.static_FVDiff_a_c (-> tptp.trm_a_c tptp.set_Sum_sum_c_c))
% 0.46/0.87  (declare-const tptp.denota102713844ree_sz (-> tptp.produc1149990247eal_sz tptp.produc1149990247eal_sz tptp.set_Sum_sum_sz_sz Bool))
% 0.46/0.87  (declare-const tptp.produc1916559302_set_a (-> (-> tptp.a Bool) tptp.set_a tptp.produc1561113620_set_a))
% 0.46/0.87  (declare-const tptp.denota1997846518gree_c (-> tptp.produc190496183real_c tptp.produc190496183real_c tptp.set_Sum_sum_c_c Bool))
% 0.46/0.87  (declare-const tptp.product_Pair_a_o_a_o (-> (-> tptp.a Bool) (-> tptp.a Bool) tptp.product_prod_a_o_a_o))
% 0.46/0.87  (define tptp.freche58918398_sc_sz () (let ((_let_1 (@var "Y2" tptp.freche2095075217_sc_sz))) (let ((_let_2 (@var "X2" tptp.denota610675952t_unit))) (lambda (@list _let_2 _let_1) (= _let_2 (_ tptp.freche1421597129_sc_sz _let_1))))))
% 0.46/0.87  (define tptp.freche1244000341_sf_sz () (let ((_let_1 (@var "Y2" tptp.frechet_strm_sf_sz))) (let ((_let_2 (@var "X2" tptp.trm_sf_sz))) (lambda (@list _let_2 _let_1) (= _let_2 (_ tptp.freche782854530_sf_sz _let_1))))))
% 0.46/0.87  (define tptp.frechet_cr_strm_a_c () (let ((_let_1 (@var "Y2" tptp.frechet_strm_a_c))) (let ((_let_2 (@var "X2" tptp.trm_a_c))) (lambda (@list _let_2 _let_1) (= _let_2 (_ tptp.frechet_raw_term_a_c _let_1))))))
% 0.46/0.87  (define tptp.denota2112424896_a_b_c () (let ((_let_1 (@var "V2" tptp.produc190496183real_c))) (let ((_let_2 (@var "T" tptp.trm_a_c))) (let ((_let_3 (@var "I5" tptp.denota231621370t_unit))) (lambda (@list _let_3 _let_2 _let_1) (_ (_ (_ (_ tptp.denota229585092_a_b_c _let_3) _let_2) (_ tptp.produc2010422875real_c _let_1)) (_ tptp.produc314122909real_c _let_1)))))))
% 0.46/0.87  (define tptp.denota453121236_sc_sz () (let ((_let_1 (@var "V2" tptp.produc1149990247eal_sz))) (let ((_let_2 (@var "T" tptp.trm_sf_sz))) (let ((_let_3 (@var "I5" tptp.denota610675952t_unit))) (lambda (@list _let_3 _let_2 _let_1) (_ (_ (_ (_ tptp.denota1979904720_sc_sz _let_3) _let_2) (_ tptp.produc1111759555eal_sz _let_1)) (_ tptp.produc1269210629eal_sz _let_1)))))))
% 0.46/0.87  (define tptp.ord_le850691415real_c () (let ((_let_1 (@var "Y2" tptp.produc190496183real_c))) (let ((_let_2 (@var "X2" tptp.produc190496183real_c))) (lambda (@list _let_2 _let_1) (and (_ (_ tptp.ord_le775706699real_c (_ tptp.produc2010422875real_c _let_2)) (_ tptp.produc2010422875real_c _let_1)) (_ (_ tptp.ord_le775706699real_c (_ tptp.produc314122909real_c _let_2)) (_ tptp.produc314122909real_c _let_1)))))))
% 0.46/0.87  (define tptp.ord_less_eq_set_a () (let ((_let_1 (@var "B5" tptp.set_a))) (let ((_let_2 (@var "T" tptp.a))) (let ((_let_3 (_ tptp.member_a _let_2))) (let ((_let_4 (@var "A5" tptp.set_a))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1)))))))))
% 0.46/0.87  (define tptp.ord_le486764743_set_a () (let ((_let_1 (@var "Y2" tptp.produc1691597095_set_a))) (let ((_let_2 (@var "X2" tptp.produc1691597095_set_a))) (lambda (@list _let_2 _let_1) (and (_ (_ tptp.ord_less_eq_set_a (_ tptp.produc1926412547_set_a _let_2)) (_ tptp.produc1926412547_set_a _let_1)) (_ (_ tptp.ord_less_eq_set_a (_ tptp.produc918972485_set_a _let_2)) (_ tptp.produc918972485_set_a _let_1)))))))
% 0.46/0.87  (define tptp.ord_le501349868_a_a_o () (let ((_let_1 (@var "Y2" tptp.produc1989635468_a_a_o))) (let ((_let_2 (@var "X2" tptp.produc1989635468_a_a_o))) (lambda (@list _let_2 _let_1) (and (_ (_ tptp.ord_less_eq_set_a (_ tptp.produc1911461786_a_a_o _let_2)) (_ tptp.produc1911461786_a_a_o _let_1)) (_ (_ tptp.ord_less_eq_a_o (_ tptp.produc23639768_a_a_o _let_2)) (_ tptp.produc23639768_a_a_o _let_1)))))))
% 0.46/0.87  (define tptp.ord_le72828020_set_a () (let ((_let_1 (@var "Y2" tptp.produc1561113620_set_a))) (let ((_let_2 (@var "X2" tptp.produc1561113620_set_a))) (lambda (@list _let_2 _let_1) (and (_ (_ tptp.ord_less_eq_a_o (_ tptp.produc1045727450_set_a _let_2)) (_ tptp.produc1045727450_set_a _let_1)) (_ (_ tptp.ord_less_eq_set_a (_ tptp.produc1305389080_set_a _let_2)) (_ tptp.produc1305389080_set_a _let_1)))))))
% 0.46/0.87  (define tptp.ord_le473656583eal_sz () (let ((_let_1 (@var "Y2" tptp.produc1149990247eal_sz))) (let ((_let_2 (@var "X2" tptp.produc1149990247eal_sz))) (lambda (@list _let_2 _let_1) (and (_ (_ tptp.ord_le787639925eal_sz (_ tptp.produc1111759555eal_sz _let_2)) (_ tptp.produc1111759555eal_sz _let_1)) (_ (_ tptp.ord_le787639925eal_sz (_ tptp.produc1269210629eal_sz _let_2)) (_ tptp.produc1269210629eal_sz _let_1)))))))
% 0.46/0.87  (define tptp.ord_le1883211903_o_a_o () (let ((_let_1 (@var "Y2" tptp.product_prod_a_o_a_o))) (let ((_let_2 (@var "X2" tptp.product_prod_a_o_a_o))) (lambda (@list _let_2 _let_1) (and (_ (_ tptp.ord_less_eq_a_o (_ tptp.product_fst_a_o_a_o _let_2)) (_ tptp.product_fst_a_o_a_o _let_1)) (_ (_ tptp.ord_less_eq_a_o (_ tptp.product_snd_a_o_a_o _let_2)) (_ tptp.product_snd_a_o_a_o _let_1)))))))
% 0.46/0.87  (define tptp.ord_le1884788375f_sz_o () (let ((_let_1 (@var "Y2" tptp.produc1144880887f_sz_o))) (let ((_let_2 (@var "X2" tptp.produc1144880887f_sz_o))) (lambda (@list _let_2 _let_1) (and (_ (_ tptp.ord_less_eq_set_a (_ tptp.produc38604755f_sz_o _let_2)) (_ tptp.produc38604755f_sz_o _let_1)) (_ (_ tptp.ord_le8515534f_sz_o (_ tptp.produc407510293f_sz_o _let_2)) (_ tptp.produc407510293f_sz_o _let_1)))))))
% 0.46/0.87  (define tptp.ord_le1643089911_set_a () (let ((_let_1 (@var "Y2" tptp.produc903182423_set_a))) (let ((_let_2 (@var "X2" tptp.produc903182423_set_a))) (lambda (@list _let_2 _let_1) (and (_ (_ tptp.ord_le8515534f_sz_o (_ tptp.produc407272755_set_a _let_2)) (_ tptp.produc407272755_set_a _let_1)) (_ (_ tptp.ord_less_eq_set_a (_ tptp.produc776178293_set_a _let_2)) (_ tptp.produc776178293_set_a _let_1)))))))
% 0.46/0.87  (define tptp.ord_le2132572860_o_a_o () (let ((_let_1 (@var "Y2" tptp.produc1065634396_o_a_o))) (let ((_let_2 (@var "X2" tptp.produc1065634396_o_a_o))) (lambda (@list _let_2 _let_1) (and (_ (_ tptp.ord_le8515534f_sz_o (_ tptp.produc2013638506_o_a_o _let_2)) (_ tptp.produc2013638506_o_a_o _let_1)) (_ (_ tptp.ord_less_eq_a_o (_ tptp.produc1630531752_o_a_o _let_2)) (_ tptp.produc1630531752_o_a_o _let_1)))))))
% 0.46/0.87  (define tptp.ord_le472894788f_sz_o () (let ((_let_1 (@var "Y2" tptp.produc1553439972f_sz_o))) (let ((_let_2 (@var "X2" tptp.produc1553439972f_sz_o))) (lambda (@list _let_2 _let_1) (and (_ (_ tptp.ord_less_eq_a_o (_ tptp.produc1453865130f_sz_o _let_2)) (_ tptp.produc1453865130f_sz_o _let_1)) (_ (_ tptp.ord_le8515534f_sz_o (_ tptp.produc1070758376f_sz_o _let_2)) (_ tptp.produc1070758376f_sz_o _let_1)))))))
% 0.46/0.87  (define tptp.f0_sf_sz () (let ((_let_1 (@var "F" tptp.sf))) (lambda (@list _let_1) (_ (_ tptp.function_sf_sz _let_1) tptp.empty_sz_sf))))
% 0.46/0.87  (define tptp.bNF_Gr1775200401_sc_sz () (let ((_let_1 (@var "A5" tptp.set_a))) (let ((_let_2 (@var "A6" tptp.a))) (let ((_let_3 (@var "G" (-> tptp.a tptp.produc866628903_sc_sz)))) (let ((_let_4 (@var "F" (-> tptp.a tptp.denota610675952t_unit)))) (let ((_let_5 (@var "Uu" tptp.produc1821101996_sc_sz))) (lambda (@list _let_1 _let_4 _let_3) (_ tptp.collec1199592193_sc_sz (lambda (@list _let_5) (exists (@list _let_2) (and (= _let_5 (_ (_ tptp.produc789536734_sc_sz (_ _let_4 _let_2)) (_ _let_3 _let_2))) (_ (_ tptp.member_a _let_2) _let_1))))))))))))
% 0.46/0.87  (define tptp.top_to1399053141c_sz_o () (let ((_let_1 (@var "Y2" tptp.produc866628903_sc_sz))) (let ((_let_2 (@var "X2" tptp.denota610675952t_unit))) (lambda (@list _let_2 _let_1) (_ (_ tptp.member1057565379_sc_sz (_ (_ tptp.produc789536734_sc_sz _let_2) _let_1)) tptp.top_to1499569298_sc_sz)))))
% 0.46/0.87  (define @t1 () (@var "T2" tptp.trm_sf_sz))
% 0.46/0.87  (define @t2 () (@var "Nu2" tptp.produc1149990247eal_sz))
% 0.46/0.87  (define @t3 () (@var "Nu" tptp.produc1149990247eal_sz))
% 0.46/0.87  (define @t4 () (_ tptp.denota102713844ree_sz @t3))
% 0.46/0.87  (define @t5 () (_ @t4 @t2))
% 0.46/0.87  (define @t6 () (_ @t5 (_ tptp.static_FVDiff_sf_sz @t1)))
% 0.46/0.87  (define @t7 () (@var "T1" tptp.trm_sf_sz))
% 0.46/0.87  (define @t8 () (_ @t5 (_ tptp.static_FVDiff_sf_sz (_ (_ tptp.plus_sf_sz @t7) @t1))))
% 0.46/0.87  (define @t9 () (@list @t3 @t2 @t7 @t1))
% 0.46/0.87  (define @t10 () (@var "T2" tptp.trm_a_c))
% 0.46/0.87  (define @t11 () (_ tptp.static_FVDiff_a_c @t10))
% 0.46/0.87  (define @t12 () (@var "Nu2" tptp.produc190496183real_c))
% 0.46/0.87  (define @t13 () (@var "Nu" tptp.produc190496183real_c))
% 0.46/0.87  (define @t14 () (_ tptp.denota1997846518gree_c @t13))
% 0.46/0.87  (define @t15 () (_ @t14 @t12))
% 0.46/0.87  (define @t16 () (_ @t15 @t11))
% 0.46/0.87  (define @t17 () (@var "T1" tptp.trm_a_c))
% 0.46/0.87  (define @t18 () (_ (_ tptp.plus_a_c @t17) @t10))
% 0.46/0.87  (define @t19 () (_ tptp.static_FVDiff_a_c @t18))
% 0.46/0.87  (define @t20 () (_ @t15 @t19))
% 0.46/0.87  (define @t21 () (@list @t13 @t12 @t17 @t10))
% 0.46/0.87  (define @t22 () (forall @t21 (=> @t20 @t16)))
% 0.46/0.87  (define @t23 () (_ (_ tptp.plus_a_c tptp.t1) tptp.t2))
% 0.46/0.87  (define @t24 () (_ tptp.static_FVDiff_a_c @t23))
% 0.46/0.87  (define @t25 () (_ (_ tptp.denota1997846518gree_c tptp.nu) tptp.nu2))
% 0.46/0.87  (define @t26 () (_ @t25 @t24))
% 0.46/0.87  (define @t27 () (_ @t25 (_ tptp.static_FVDiff_a_c tptp.t1)))
% 0.46/0.87  (define @t28 () (_ @t5 (_ tptp.static_FVDiff_sf_sz @t7)))
% 0.46/0.87  (define @t29 () (_ @t15 (_ tptp.static_FVDiff_a_c @t17)))
% 0.46/0.87  (define @t30 () (@var "V" tptp.set_Sum_sum_sz_sz))
% 0.46/0.87  (define @t31 () (@var "A" tptp.produc1149990247eal_sz))
% 0.46/0.87  (define @t32 () (@var "B" tptp.produc1149990247eal_sz))
% 0.46/0.87  (define @t33 () (@var "V" tptp.set_Sum_sum_c_c))
% 0.46/0.87  (define @t34 () (@var "A" tptp.produc190496183real_c))
% 0.46/0.87  (define @t35 () (@var "B" tptp.produc190496183real_c))
% 0.46/0.87  (define @t36 () (@var "A" tptp.set_Sum_sum_sz_sz))
% 0.46/0.87  (define @t37 () (@var "A" tptp.set_Sum_sum_c_c))
% 0.46/0.87  (define @t38 () (@var "Y" tptp.freche2095075217_sc_sz))
% 0.46/0.87  (define @t39 () (@var "X" tptp.freche2095075217_sc_sz))
% 0.46/0.87  (define @t40 () (_ tptp.freche1421597129_sc_sz @t39))
% 0.46/0.87  (define @t41 () (@var "Y" tptp.frechet_strm_sf_sz))
% 0.46/0.87  (define @t42 () (@var "X" tptp.frechet_strm_sf_sz))
% 0.46/0.87  (define @t43 () (_ tptp.freche782854530_sf_sz @t42))
% 0.46/0.87  (define @t44 () (@var "Y" tptp.frechet_strm_a_c))
% 0.46/0.87  (define @t45 () (@var "X" tptp.frechet_strm_a_c))
% 0.46/0.87  (define @t46 () (_ tptp.frechet_raw_term_a_c @t45))
% 0.46/0.87  (define @t47 () (_ @t5 (_ tptp.static_FVDiff_sf_sz (_ (_ tptp.times_sf_sz @t7) @t1))))
% 0.46/0.87  (define @t48 () (_ @t15 (_ tptp.static_FVDiff_a_c (_ (_ tptp.times_a_c @t17) @t10))))
% 0.46/0.87  (define @t49 () (@var "I" tptp.sz))
% 0.46/0.87  (define @t50 () (@var "Args" (-> tptp.sz tptp.trm_sf_sz)))
% 0.46/0.87  (define @t51 () (_ @t50 @t49))
% 0.46/0.87  (define @t52 () (@var "Var" tptp.sf))
% 0.46/0.87  (define @t53 () (@var "I" tptp.c))
% 0.46/0.87  (define @t54 () (@var "Args" (-> tptp.c tptp.trm_a_c)))
% 0.46/0.87  (define @t55 () (@var "Var" tptp.a))
% 0.46/0.87  (define @t56 () (_ tptp.produc314122909real_c tptp.nu2))
% 0.46/0.87  (define @t57 () (_ tptp.produc2010422875real_c tptp.nu2))
% 0.46/0.87  (define @t58 () (_ tptp.denota229585092_a_b_c tptp.j))
% 0.46/0.87  (define @t59 () (_ tptp.produc314122909real_c tptp.nu))
% 0.46/0.87  (define @t60 () (_ tptp.produc2010422875real_c tptp.nu))
% 0.46/0.87  (define @t61 () (_ tptp.denota229585092_a_b_c tptp.i))
% 0.46/0.87  (define @t62 () (@var "X2" tptp.a))
% 0.46/0.87  (define @t63 () (_ tptp.member_a @t62))
% 0.46/0.87  (define @t64 () (@var "Uu" tptp.sum_su737395349um_b_c))
% 0.46/0.87  (define @t65 () (= @t64 (_ tptp.sum_In2139678582um_b_c @t62)))
% 0.46/0.87  (define @t66 () (@list @t62))
% 0.46/0.87  (define @t67 () (@list @t64))
% 0.46/0.87  (define @t68 () (_ tptp.collec2086029184um_b_c (lambda @t67 (exists @t66 (and @t65 (_ @t63 (_ tptp.static_SIGT_a_c tptp.t2)))))))
% 0.46/0.87  (define @t69 () (_ (_ tptp.denota69106024_a_b_c tptp.i) tptp.j))
% 0.46/0.87  (define @t70 () (_ @t69 @t68))
% 0.46/0.87  (define @t71 () (_ tptp.static_FVDiff_a_c tptp.t2))
% 0.46/0.87  (define @t72 () (_ @t25 @t71))
% 0.46/0.87  (define @t73 () (@var "S" tptp.produc866628903_sc_sz))
% 0.46/0.87  (define @t74 () (@var "I2" tptp.denota610675952t_unit))
% 0.46/0.87  (define @t75 () (@var "X" tptp.produc1821101996_sc_sz))
% 0.46/0.87  (define @t76 () (not (forall (@list @t74 @t73) (not (= @t75 (_ (_ tptp.produc789536734_sc_sz @t74) @t73))))))
% 0.46/0.87  (define @t77 () (_ tptp.collect_trm_a_c tptp.dfree_a_c))
% 0.46/0.87  (define @t78 () (@list @t45))
% 0.46/0.87  (define @t79 () (_ tptp.collect_trm_sf_sz tptp.dfree_sf_sz))
% 0.46/0.87  (define @t80 () (@list @t42))
% 0.46/0.87  (define @t81 () (@var "X3" tptp.frechet_strm_a_c))
% 0.46/0.87  (define @t82 () (_ tptp.frechet_raw_term_a_c @t81))
% 0.46/0.87  (define @t83 () (@var "Y" tptp.trm_a_c))
% 0.46/0.87  (define @t84 () (@list @t81))
% 0.46/0.87  (define @t85 () (_ (_ tptp.member_trm_a_c @t83) @t77))
% 0.46/0.87  (define @t86 () (@list @t83))
% 0.46/0.87  (define @t87 () (@var "X3" tptp.frechet_strm_sf_sz))
% 0.46/0.87  (define @t88 () (_ tptp.freche782854530_sf_sz @t87))
% 0.46/0.87  (define @t89 () (@var "Y" tptp.trm_sf_sz))
% 0.46/0.87  (define @t90 () (@list @t87))
% 0.46/0.87  (define @t91 () (_ (_ tptp.member_trm_sf_sz @t89) @t79))
% 0.46/0.87  (define @t92 () (@list @t89))
% 0.46/0.87  (define @t93 () (@var "P" (-> tptp.trm_a_c Bool)))
% 0.46/0.87  (define @t94 () (@var "P" (-> tptp.trm_sf_sz Bool)))
% 0.46/0.87  (define @t95 () (_ tptp.produc2010422875real_c @t12))
% 0.46/0.87  (define @t96 () (@var "Theta" tptp.trm_a_c))
% 0.46/0.87  (define @t97 () (@var "I3" tptp.denota231621370t_unit))
% 0.46/0.87  (define @t98 () (_ tptp.denota229585092_a_b_c @t97))
% 0.46/0.87  (define @t99 () (_ @t98 @t96))
% 0.46/0.87  (define @t100 () (_ tptp.produc314122909real_c @t13))
% 0.46/0.87  (define @t101 () (_ tptp.produc2010422875real_c @t13))
% 0.46/0.87  (define @t102 () (_ tptp.dfree_a_c @t96))
% 0.46/0.87  (define @t103 () (@var "Theta" tptp.trm_sf_sz))
% 0.46/0.87  (define @t104 () (@var "I3" tptp.denota610675952t_unit))
% 0.46/0.87  (define @t105 () (_ tptp.denota1979904720_sc_sz @t104))
% 0.46/0.87  (define @t106 () (_ @t105 @t103))
% 0.46/0.87  (define @t107 () (_ tptp.produc1269210629eal_sz @t3))
% 0.46/0.87  (define @t108 () (_ tptp.produc1111759555eal_sz @t3))
% 0.46/0.87  (define @t109 () (_ tptp.dfree_sf_sz @t103))
% 0.46/0.87  (define @t110 () (_ tptp.collec2086029184um_b_c (lambda @t67 (exists @t66 (and @t65 (_ @t63 (_ tptp.static_SIGT_a_c @t23)))))))
% 0.46/0.87  (define @t111 () (_ tptp.collec2086029184um_b_c (lambda @t67 (exists @t66 (and @t65 (_ @t63 (_ tptp.static_SIGT_a_c tptp.t1)))))))
% 0.46/0.87  (define @t112 () (_ @t69 @t111))
% 0.46/0.87  (define @t113 () (@var "V" tptp.set_Su1783761653um_b_c))
% 0.46/0.87  (define @t114 () (@var "A" tptp.denota231621370t_unit))
% 0.46/0.87  (define @t115 () (@var "B" tptp.denota231621370t_unit))
% 0.46/0.87  (define @t116 () (@var "A" tptp.set_Su1783761653um_b_c))
% 0.46/0.87  (define @t117 () (_ tptp.denota69106024_a_b_c @t97))
% 0.46/0.87  (define @t118 () (_ tptp.freche665377492rm_a_c @t83))
% 0.46/0.87  (define @t119 () (_ tptp.freche1046279700_sf_sz @t89))
% 0.46/0.87  (define @t120 () (@var "Prod" tptp.produc866628903_sc_sz))
% 0.46/0.87  (define @t121 () (_ (_ tptp.produc1822718231_sc_sz (_ tptp.produc548504323_sc_sz @t120)) (_ tptp.produc4753477_sc_sz @t120)))
% 0.46/0.87  (define @t122 () (@list @t120))
% 0.46/0.87  (define @t123 () (@var "Prod" tptp.produc1241881959eal_sz))
% 0.46/0.87  (define @t124 () (_ (_ tptp.produc1235791063eal_sz (_ tptp.produc286845635eal_sz @t123)) (_ tptp.produc1746886149eal_sz @t123)))
% 0.46/0.87  (define @t125 () (@list @t123))
% 0.46/0.87  (define @t126 () (@var "Prod" tptp.produc1892666919z_real))
% 0.46/0.87  (define @t127 () (_ (_ tptp.produc784663575z_real (_ tptp.produc870616579z_real @t126)) (_ tptp.produc1422611269z_real @t126)))
% 0.46/0.87  (define @t128 () (@list @t126))
% 0.46/0.87  (define @t129 () (@var "Prod" tptp.produc1149990247eal_sz))
% 0.46/0.87  (define @t130 () (_ tptp.produc1269210629eal_sz @t129))
% 0.46/0.87  (define @t131 () (_ tptp.produc1111759555eal_sz @t129))
% 0.46/0.87  (define @t132 () (_ (_ tptp.produc1308130519eal_sz @t131) @t130))
% 0.46/0.87  (define @t133 () (@list @t129))
% 0.46/0.87  (define @t134 () (@var "Prod" tptp.produc1821101996_sc_sz))
% 0.46/0.87  (define @t135 () (_ tptp.produc974239792_sc_sz @t134))
% 0.46/0.87  (define @t136 () (_ tptp.produc1503602930_sc_sz @t134))
% 0.46/0.87  (define @t137 () (_ (_ tptp.produc789536734_sc_sz @t136) @t135))
% 0.46/0.87  (define @t138 () (@list @t134))
% 0.46/0.87  (define @t139 () (@var "Prod" tptp.produc190496183real_c))
% 0.46/0.87  (define @t140 () (_ tptp.produc314122909real_c @t139))
% 0.46/0.87  (define @t141 () (_ tptp.produc2010422875real_c @t139))
% 0.46/0.87  (define @t142 () (_ (_ tptp.produc394644079real_c @t141) @t140))
% 0.46/0.87  (define @t143 () (@list @t139))
% 0.46/0.87  (define @t144 () (@var "B2" tptp.trm_a_c))
% 0.46/0.87  (define @t145 () (@var "A2" tptp.trm_a_c))
% 0.46/0.87  (define @t146 () (and (_ tptp.dfree_a_c @t145) (_ tptp.dfree_a_c @t144)))
% 0.46/0.87  (define @t147 () (@list @t145 @t144))
% 0.46/0.87  (define @t148 () (@var "B2" tptp.trm_sf_sz))
% 0.46/0.87  (define @t149 () (@var "A2" tptp.trm_sf_sz))
% 0.46/0.87  (define @t150 () (and (_ tptp.dfree_sf_sz @t149) (_ tptp.dfree_sf_sz @t148)))
% 0.46/0.87  (define @t151 () (@list @t149 @t148))
% 0.46/0.87  (define @t152 () (@var "X2" tptp.c))
% 0.46/0.87  (define @t153 () (@var "I" tptp.a))
% 0.46/0.87  (define @t154 () (_ tptp.dfree_a_c (_ (_ tptp.function_a_c @t153) @t54)))
% 0.46/0.87  (define @t155 () (@var "X2" tptp.sz))
% 0.46/0.87  (define @t156 () (@var "I" tptp.sf))
% 0.46/0.87  (define @t157 () (_ tptp.dfree_sf_sz (_ (_ tptp.function_sf_sz @t156) @t50)))
% 0.46/0.87  (define @t158 () (@var "Y3" tptp.trm_a_c))
% 0.46/0.87  (define @t159 () (_ (_ tptp.member_trm_a_c @t158) @t77))
% 0.46/0.87  (define @t160 () (_ tptp.freche665377492rm_a_c @t158))
% 0.46/0.87  (define @t161 () (@list @t158))
% 0.46/0.87  (define @t162 () (@var "Y3" tptp.trm_sf_sz))
% 0.46/0.87  (define @t163 () (_ (_ tptp.member_trm_sf_sz @t162) @t79))
% 0.46/0.87  (define @t164 () (_ tptp.freche1046279700_sf_sz @t162))
% 0.46/0.87  (define @t165 () (@list @t162))
% 0.46/0.87  (define @t166 () (@var "X" tptp.trm_a_c))
% 0.46/0.87  (define @t167 () (@var "X" tptp.trm_sf_sz))
% 0.46/0.87  (define @t168 () (@var "P" (-> tptp.frechet_strm_a_c Bool)))
% 0.46/0.87  (define @t169 () (@var "P" (-> tptp.frechet_strm_sf_sz Bool)))
% 0.46/0.87  (define @t170 () (@var "B3" tptp.finite1398487019real_c))
% 0.46/0.87  (define @t171 () (@var "B2" tptp.finite1398487019real_c))
% 0.46/0.87  (define @t172 () (= @t171 @t170))
% 0.46/0.87  (define @t173 () (@var "A3" tptp.finite1398487019real_c))
% 0.46/0.87  (define @t174 () (@var "A2" tptp.finite1398487019real_c))
% 0.46/0.87  (define @t175 () (= @t174 @t173))
% 0.46/0.87  (define @t176 () (_ (_ tptp.produc394644079real_c @t174) @t171))
% 0.46/0.87  (define @t177 () (= @t176 (_ (_ tptp.produc394644079real_c @t173) @t170)))
% 0.46/0.87  (define @t178 () (@list @t174 @t171 @t173 @t170))
% 0.46/0.87  (define @t179 () (@var "B3" tptp.list_f1238882004_sc_sz))
% 0.46/0.87  (define @t180 () (@var "B2" tptp.list_f1238882004_sc_sz))
% 0.46/0.87  (define @t181 () (= @t180 @t179))
% 0.46/0.87  (define @t182 () (@var "A3" tptp.list_f1238882004_sc_sz))
% 0.46/0.87  (define @t183 () (@var "A2" tptp.list_f1238882004_sc_sz))
% 0.46/0.87  (define @t184 () (= @t183 @t182))
% 0.46/0.87  (define @t185 () (= (_ (_ tptp.produc1822718231_sc_sz @t183) @t180) (_ (_ tptp.produc1822718231_sc_sz @t182) @t179)))
% 0.46/0.87  (define @t186 () (@list @t183 @t180 @t182 @t179))
% 0.46/0.87  (define @t187 () (@var "B3" tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (define @t188 () (@var "B2" tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (define @t189 () (= @t188 @t187))
% 0.46/0.87  (define @t190 () (@var "A3" tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (define @t191 () (@var "A2" tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (define @t192 () (= @t191 @t190))
% 0.46/0.87  (define @t193 () (_ (_ tptp.produc1235791063eal_sz @t191) @t188))
% 0.46/0.87  (define @t194 () (= @t193 (_ (_ tptp.produc1235791063eal_sz @t190) @t187)))
% 0.46/0.87  (define @t195 () (@list @t191 @t188 @t190 @t187))
% 0.46/0.87  (define @t196 () (@var "B3" tptp.bounde472938360z_real))
% 0.46/0.87  (define @t197 () (@var "B2" tptp.bounde472938360z_real))
% 0.46/0.87  (define @t198 () (= @t197 @t196))
% 0.46/0.87  (define @t199 () (@var "A3" tptp.bounde472938360z_real))
% 0.46/0.87  (define @t200 () (@var "A2" tptp.bounde472938360z_real))
% 0.46/0.87  (define @t201 () (= @t200 @t199))
% 0.46/0.87  (define @t202 () (= (_ (_ tptp.produc784663575z_real @t200) @t197) (_ (_ tptp.produc784663575z_real @t199) @t196)))
% 0.46/0.87  (define @t203 () (@list @t200 @t197 @t199 @t196))
% 0.46/0.87  (define @t204 () (@var "B3" tptp.produc866628903_sc_sz))
% 0.46/0.87  (define @t205 () (@var "B2" tptp.produc866628903_sc_sz))
% 0.46/0.87  (define @t206 () (= @t205 @t204))
% 0.46/0.87  (define @t207 () (@var "A3" tptp.denota610675952t_unit))
% 0.46/0.87  (define @t208 () (@var "A2" tptp.denota610675952t_unit))
% 0.46/0.87  (define @t209 () (= @t208 @t207))
% 0.46/0.87  (define @t210 () (= (_ (_ tptp.produc789536734_sc_sz @t208) @t205) (_ (_ tptp.produc789536734_sc_sz @t207) @t204)))
% 0.46/0.87  (define @t211 () (@list @t208 @t205 @t207 @t204))
% 0.46/0.87  (define @t212 () (@var "Y22" tptp.finite1398487019real_c))
% 0.46/0.87  (define @t213 () (@var "X22" tptp.finite1398487019real_c))
% 0.46/0.87  (define @t214 () (@var "Y1" tptp.finite1398487019real_c))
% 0.46/0.87  (define @t215 () (@var "X1" tptp.finite1398487019real_c))
% 0.46/0.87  (define @t216 () (_ (_ tptp.produc394644079real_c @t215) @t213))
% 0.46/0.87  (define @t217 () (@var "Y22" tptp.list_f1238882004_sc_sz))
% 0.46/0.87  (define @t218 () (@var "X22" tptp.list_f1238882004_sc_sz))
% 0.46/0.87  (define @t219 () (@var "Y1" tptp.list_f1238882004_sc_sz))
% 0.46/0.87  (define @t220 () (@var "X1" tptp.list_f1238882004_sc_sz))
% 0.46/0.87  (define @t221 () (_ (_ tptp.produc1822718231_sc_sz @t220) @t218))
% 0.46/0.87  (define @t222 () (@var "Y22" tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (define @t223 () (@var "X22" tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (define @t224 () (@var "Y1" tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (define @t225 () (@var "X1" tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (define @t226 () (_ (_ tptp.produc1235791063eal_sz @t225) @t223))
% 0.46/0.87  (define @t227 () (@var "Y22" tptp.bounde472938360z_real))
% 0.46/0.87  (define @t228 () (@var "X22" tptp.bounde472938360z_real))
% 0.46/0.87  (define @t229 () (@var "Y1" tptp.bounde472938360z_real))
% 0.46/0.87  (define @t230 () (@var "X1" tptp.bounde472938360z_real))
% 0.46/0.87  (define @t231 () (_ (_ tptp.produc784663575z_real @t230) @t228))
% 0.46/0.87  (define @t232 () (@var "Y22" tptp.produc866628903_sc_sz))
% 0.46/0.87  (define @t233 () (@var "X22" tptp.produc866628903_sc_sz))
% 0.46/0.87  (define @t234 () (@var "Y1" tptp.denota610675952t_unit))
% 0.46/0.87  (define @t235 () (@var "X1" tptp.denota610675952t_unit))
% 0.46/0.87  (define @t236 () (_ (_ tptp.produc789536734_sc_sz @t235) @t233))
% 0.46/0.87  (define @t237 () (@var "Y32" (-> tptp.c tptp.trm_a_c)))
% 0.46/0.87  (define @t238 () (@var "X32" (-> tptp.c tptp.trm_a_c)))
% 0.46/0.87  (define @t239 () (@var "Y31" tptp.a))
% 0.46/0.87  (define @t240 () (@var "X31" tptp.a))
% 0.46/0.87  (define @t241 () (_ (_ tptp.function_a_c @t240) @t238))
% 0.46/0.87  (define @t242 () (@var "Y32" (-> tptp.sz tptp.trm_sf_sz)))
% 0.46/0.87  (define @t243 () (@var "X32" (-> tptp.sz tptp.trm_sf_sz)))
% 0.46/0.87  (define @t244 () (@var "Y31" tptp.sf))
% 0.46/0.87  (define @t245 () (@var "X31" tptp.sf))
% 0.46/0.87  (define @t246 () (_ (_ tptp.function_sf_sz @t245) @t243))
% 0.46/0.87  (define @t247 () (@var "Y42" tptp.trm_sf_sz))
% 0.46/0.87  (define @t248 () (@var "X42" tptp.trm_sf_sz))
% 0.46/0.87  (define @t249 () (@var "Y41" tptp.trm_sf_sz))
% 0.46/0.87  (define @t250 () (@var "X41" tptp.trm_sf_sz))
% 0.46/0.87  (define @t251 () (_ (_ tptp.plus_sf_sz @t250) @t248))
% 0.46/0.87  (define @t252 () (@var "Y42" tptp.trm_a_c))
% 0.46/0.87  (define @t253 () (@var "X42" tptp.trm_a_c))
% 0.46/0.87  (define @t254 () (@var "Y41" tptp.trm_a_c))
% 0.46/0.87  (define @t255 () (@var "X41" tptp.trm_a_c))
% 0.46/0.87  (define @t256 () (_ (_ tptp.plus_a_c @t255) @t253))
% 0.46/0.87  (define @t257 () (@var "Y52" tptp.trm_a_c))
% 0.46/0.87  (define @t258 () (@var "X52" tptp.trm_a_c))
% 0.46/0.87  (define @t259 () (@var "Y51" tptp.trm_a_c))
% 0.46/0.87  (define @t260 () (@var "X51" tptp.trm_a_c))
% 0.46/0.87  (define @t261 () (_ (_ tptp.times_a_c @t260) @t258))
% 0.46/0.87  (define @t262 () (@var "Y52" tptp.trm_sf_sz))
% 0.46/0.87  (define @t263 () (@var "X52" tptp.trm_sf_sz))
% 0.46/0.87  (define @t264 () (@var "Y51" tptp.trm_sf_sz))
% 0.46/0.87  (define @t265 () (@var "X51" tptp.trm_sf_sz))
% 0.46/0.87  (define @t266 () (_ (_ tptp.times_sf_sz @t265) @t263))
% 0.46/0.87  (define @t267 () (@var "A2" tptp.finite824932053eal_sz))
% 0.46/0.87  (define @t268 () (@var "P" (-> tptp.finite824932053eal_sz Bool)))
% 0.46/0.87  (define @t269 () (_ tptp.collec1002602816eal_sz @t268))
% 0.46/0.87  (define @t270 () (@var "A2" tptp.produc1821101996_sc_sz))
% 0.46/0.87  (define @t271 () (@var "P" (-> tptp.produc1821101996_sc_sz Bool)))
% 0.46/0.87  (define @t272 () (_ tptp.collec1199592193_sc_sz @t271))
% 0.46/0.87  (define @t273 () (_ tptp.collect_trm_sf_sz @t94))
% 0.46/0.87  (define @t274 () (_ tptp.collect_trm_a_c @t93))
% 0.46/0.87  (define @t275 () (@var "A2" tptp.a))
% 0.46/0.87  (define @t276 () (@var "P" (-> tptp.a Bool)))
% 0.46/0.87  (define @t277 () (_ tptp.collect_a @t276))
% 0.46/0.87  (define @t278 () (@var "A2" tptp.sum_su737395349um_b_c))
% 0.46/0.87  (define @t279 () (@var "P" (-> tptp.sum_su737395349um_b_c Bool)))
% 0.46/0.87  (define @t280 () (_ tptp.collec2086029184um_b_c @t279))
% 0.46/0.87  (define @t281 () (@var "A" tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (define @t282 () (@var "X2" tptp.finite824932053eal_sz))
% 0.46/0.87  (define @t283 () (_ tptp.member1693951742eal_sz @t282))
% 0.46/0.87  (define @t284 () (_ @t283 @t281))
% 0.46/0.87  (define @t285 () (@list @t282))
% 0.46/0.87  (define @t286 () (@list @t281))
% 0.46/0.87  (define @t287 () (@var "A" tptp.set_Pr1169339874_sc_sz))
% 0.46/0.87  (define @t288 () (@var "X2" tptp.produc1821101996_sc_sz))
% 0.46/0.87  (define @t289 () (_ tptp.member1057565379_sc_sz @t288))
% 0.46/0.87  (define @t290 () (_ @t289 @t287))
% 0.46/0.87  (define @t291 () (@list @t288))
% 0.46/0.87  (define @t292 () (@var "A" tptp.set_trm_sf_sz))
% 0.46/0.87  (define @t293 () (@var "X2" tptp.trm_sf_sz))
% 0.46/0.87  (define @t294 () (_ tptp.member_trm_sf_sz @t293))
% 0.46/0.87  (define @t295 () (_ @t294 @t292))
% 0.46/0.87  (define @t296 () (@list @t293))
% 0.46/0.87  (define @t297 () (@var "A" tptp.set_trm_a_c))
% 0.46/0.87  (define @t298 () (@var "X2" tptp.trm_a_c))
% 0.46/0.87  (define @t299 () (_ tptp.member_trm_a_c @t298))
% 0.46/0.87  (define @t300 () (_ @t299 @t297))
% 0.46/0.87  (define @t301 () (@list @t298))
% 0.46/0.87  (define @t302 () (@var "A" tptp.set_a))
% 0.46/0.87  (define @t303 () (_ @t63 @t302))
% 0.46/0.87  (define @t304 () (@list @t302))
% 0.46/0.87  (define @t305 () (@var "X2" tptp.sum_su737395349um_b_c))
% 0.46/0.87  (define @t306 () (_ tptp.member1893232190um_b_c @t305))
% 0.46/0.87  (define @t307 () (_ @t306 @t116))
% 0.46/0.87  (define @t308 () (@list @t305))
% 0.46/0.87  (define @t309 () (@var "Q" (-> tptp.finite824932053eal_sz Bool)))
% 0.46/0.87  (define @t310 () (_ tptp.collec1002602816eal_sz @t309))
% 0.46/0.87  (define @t311 () (@var "X3" tptp.finite824932053eal_sz))
% 0.46/0.87  (define @t312 () (_ @t309 @t311))
% 0.46/0.87  (define @t313 () (_ @t268 @t311))
% 0.46/0.87  (define @t314 () (@list @t311))
% 0.46/0.87  (define @t315 () (@list @t268 @t309))
% 0.46/0.87  (define @t316 () (@var "Q" (-> tptp.produc1821101996_sc_sz Bool)))
% 0.46/0.87  (define @t317 () (_ tptp.collec1199592193_sc_sz @t316))
% 0.46/0.87  (define @t318 () (@var "X3" tptp.produc1821101996_sc_sz))
% 0.46/0.87  (define @t319 () (_ @t316 @t318))
% 0.46/0.87  (define @t320 () (_ @t271 @t318))
% 0.46/0.87  (define @t321 () (@list @t318))
% 0.46/0.87  (define @t322 () (@list @t271 @t316))
% 0.46/0.87  (define @t323 () (@var "Q" (-> tptp.trm_sf_sz Bool)))
% 0.46/0.87  (define @t324 () (_ tptp.collect_trm_sf_sz @t323))
% 0.46/0.87  (define @t325 () (@var "X3" tptp.trm_sf_sz))
% 0.46/0.87  (define @t326 () (_ @t323 @t325))
% 0.46/0.87  (define @t327 () (_ @t94 @t325))
% 0.46/0.87  (define @t328 () (@list @t325))
% 0.46/0.87  (define @t329 () (@list @t94 @t323))
% 0.46/0.87  (define @t330 () (@var "Q" (-> tptp.trm_a_c Bool)))
% 0.46/0.87  (define @t331 () (_ tptp.collect_trm_a_c @t330))
% 0.46/0.87  (define @t332 () (@var "X3" tptp.trm_a_c))
% 0.46/0.87  (define @t333 () (_ @t330 @t332))
% 0.46/0.87  (define @t334 () (_ @t93 @t332))
% 0.46/0.87  (define @t335 () (@list @t332))
% 0.46/0.87  (define @t336 () (@list @t93 @t330))
% 0.46/0.87  (define @t337 () (@var "Q" (-> tptp.a Bool)))
% 0.46/0.87  (define @t338 () (_ tptp.collect_a @t337))
% 0.46/0.87  (define @t339 () (@var "X3" tptp.a))
% 0.46/0.87  (define @t340 () (_ @t337 @t339))
% 0.46/0.87  (define @t341 () (_ @t276 @t339))
% 0.46/0.87  (define @t342 () (@list @t339))
% 0.46/0.87  (define @t343 () (@list @t276 @t337))
% 0.46/0.87  (define @t344 () (@var "Q" (-> tptp.sum_su737395349um_b_c Bool)))
% 0.46/0.87  (define @t345 () (_ tptp.collec2086029184um_b_c @t344))
% 0.46/0.87  (define @t346 () (@var "X3" tptp.sum_su737395349um_b_c))
% 0.46/0.87  (define @t347 () (_ @t344 @t346))
% 0.46/0.87  (define @t348 () (_ @t279 @t346))
% 0.46/0.87  (define @t349 () (@list @t346))
% 0.46/0.87  (define @t350 () (@list @t279 @t344))
% 0.46/0.87  (define @t351 () (@var "Omega" tptp.produc1149990247eal_sz))
% 0.46/0.87  (define @t352 () (_ @t4 @t351))
% 0.46/0.87  (define @t353 () (@var "B" tptp.set_Sum_sum_sz_sz))
% 0.46/0.87  (define @t354 () (@var "Omega" tptp.produc190496183real_c))
% 0.46/0.87  (define @t355 () (_ @t14 @t354))
% 0.46/0.87  (define @t356 () (@var "B" tptp.set_Sum_sum_c_c))
% 0.46/0.87  (define @t357 () (@var "P" (-> tptp.produc190496183real_c Bool)))
% 0.46/0.87  (define @t358 () (@var "B4" tptp.finite1398487019real_c))
% 0.46/0.87  (define @t359 () (@var "A4" tptp.finite1398487019real_c))
% 0.46/0.87  (define @t360 () (_ (_ tptp.produc394644079real_c @t359) @t358))
% 0.46/0.87  (define @t361 () (@list @t359 @t358))
% 0.46/0.87  (define @t362 () (forall @t361 (_ @t357 @t360)))
% 0.46/0.87  (define @t363 () (@var "P" (-> tptp.produc866628903_sc_sz Bool)))
% 0.46/0.87  (define @t364 () (@var "B4" tptp.list_f1238882004_sc_sz))
% 0.46/0.87  (define @t365 () (@var "A4" tptp.list_f1238882004_sc_sz))
% 0.46/0.87  (define @t366 () (_ (_ tptp.produc1822718231_sc_sz @t365) @t364))
% 0.46/0.87  (define @t367 () (@list @t365 @t364))
% 0.46/0.87  (define @t368 () (forall @t367 (_ @t363 @t366)))
% 0.46/0.87  (define @t369 () (@var "P" (-> tptp.produc1241881959eal_sz Bool)))
% 0.46/0.87  (define @t370 () (@var "B4" tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (define @t371 () (@var "A4" tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (define @t372 () (_ (_ tptp.produc1235791063eal_sz @t371) @t370))
% 0.46/0.87  (define @t373 () (@list @t371 @t370))
% 0.46/0.87  (define @t374 () (forall @t373 (_ @t369 @t372)))
% 0.46/0.87  (define @t375 () (@var "P" (-> tptp.produc1892666919z_real Bool)))
% 0.46/0.87  (define @t376 () (@var "B4" tptp.bounde472938360z_real))
% 0.46/0.87  (define @t377 () (@var "A4" tptp.bounde472938360z_real))
% 0.46/0.87  (define @t378 () (_ (_ tptp.produc784663575z_real @t377) @t376))
% 0.46/0.87  (define @t379 () (@list @t377 @t376))
% 0.46/0.87  (define @t380 () (forall @t379 (_ @t375 @t378)))
% 0.46/0.87  (define @t381 () (@var "B4" tptp.produc866628903_sc_sz))
% 0.46/0.87  (define @t382 () (@var "A4" tptp.denota610675952t_unit))
% 0.46/0.87  (define @t383 () (_ tptp.produc789536734_sc_sz @t382))
% 0.46/0.87  (define @t384 () (_ @t383 @t381))
% 0.46/0.87  (define @t385 () (@list @t382 @t381))
% 0.46/0.87  (define @t386 () (forall @t385 (_ @t271 @t384)))
% 0.46/0.87  (define @t387 () (@var "Y" tptp.produc190496183real_c))
% 0.46/0.87  (define @t388 () (@var "Y" tptp.produc866628903_sc_sz))
% 0.46/0.87  (define @t389 () (@var "Y" tptp.produc1241881959eal_sz))
% 0.46/0.87  (define @t390 () (@var "Y" tptp.produc1892666919z_real))
% 0.46/0.87  (define @t391 () (@var "Y" tptp.produc1821101996_sc_sz))
% 0.46/0.87  (define @t392 () (@list @t391))
% 0.46/0.87  (define @t393 () (@var "P2" tptp.produc190496183real_c))
% 0.46/0.87  (define @t394 () (@var "P2" tptp.produc866628903_sc_sz))
% 0.46/0.87  (define @t395 () (@var "P2" tptp.produc1241881959eal_sz))
% 0.46/0.87  (define @t396 () (@var "P2" tptp.produc1892666919z_real))
% 0.46/0.87  (define @t397 () (@var "P2" tptp.produc1821101996_sc_sz))
% 0.46/0.87  (define @t398 () (@var "Y3" tptp.finite1398487019real_c))
% 0.46/0.87  (define @t399 () (@var "X3" tptp.finite1398487019real_c))
% 0.46/0.87  (define @t400 () (@list @t399 @t398))
% 0.46/0.87  (define @t401 () (@var "Y3" tptp.list_f1238882004_sc_sz))
% 0.46/0.87  (define @t402 () (@var "X3" tptp.list_f1238882004_sc_sz))
% 0.46/0.87  (define @t403 () (@var "Y3" tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (define @t404 () (@var "X3" tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (define @t405 () (@var "Y3" tptp.bounde472938360z_real))
% 0.46/0.87  (define @t406 () (@var "X3" tptp.bounde472938360z_real))
% 0.46/0.87  (define @t407 () (@var "Y3" tptp.produc866628903_sc_sz))
% 0.46/0.87  (define @t408 () (@var "X3" tptp.denota610675952t_unit))
% 0.46/0.87  (define @t409 () (_ (_ tptp.produc789536734_sc_sz @t408) @t407))
% 0.46/0.87  (define @t410 () (@list @t408 @t407))
% 0.46/0.87  (define @t411 () (@var "C" tptp.list_f1238882004_sc_sz))
% 0.46/0.87  (define @t412 () (_ @t383 (_ (_ tptp.produc1822718231_sc_sz @t364) @t411)))
% 0.46/0.87  (define @t413 () (@list @t382 @t364 @t411))
% 0.46/0.87  (define @t414 () (@list @t220 @t218))
% 0.46/0.87  (define @t415 () (@list @t225 @t223))
% 0.46/0.87  (define @t416 () (@list @t230 @t228))
% 0.46/0.87  (define @t417 () (@var "X1" tptp.finite824932053eal_sz))
% 0.46/0.87  (define @t418 () (@var "X22" tptp.finite824932053eal_sz))
% 0.46/0.87  (define @t419 () (_ (_ tptp.produc1308130519eal_sz @t417) @t418))
% 0.46/0.87  (define @t420 () (@list @t417 @t418))
% 0.46/0.87  (define @t421 () (@list @t235 @t233))
% 0.46/0.87  (define @t422 () (@list @t215 @t213))
% 0.46/0.87  (define @t423 () (@var "X" tptp.list_f1238882004_sc_sz))
% 0.46/0.87  (define @t424 () (@var "Y" tptp.list_f1238882004_sc_sz))
% 0.46/0.87  (define @t425 () (_ (_ tptp.produc1822718231_sc_sz @t423) @t424))
% 0.46/0.87  (define @t426 () (_ tptp.produc548504323_sc_sz @t425))
% 0.46/0.87  (define @t427 () (@list @t423 @t424 @t183))
% 0.46/0.87  (define @t428 () (@var "X" tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (define @t429 () (@var "Y" tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (define @t430 () (_ (_ tptp.produc1235791063eal_sz @t428) @t429))
% 0.46/0.87  (define @t431 () (_ tptp.produc286845635eal_sz @t430))
% 0.46/0.87  (define @t432 () (@list @t428 @t429 @t191))
% 0.46/0.87  (define @t433 () (@var "X" tptp.bounde472938360z_real))
% 0.46/0.87  (define @t434 () (@var "Y" tptp.bounde472938360z_real))
% 0.46/0.87  (define @t435 () (_ (_ tptp.produc784663575z_real @t433) @t434))
% 0.46/0.87  (define @t436 () (_ tptp.produc870616579z_real @t435))
% 0.46/0.87  (define @t437 () (@list @t433 @t434 @t200))
% 0.46/0.87  (define @t438 () (@var "X" tptp.finite824932053eal_sz))
% 0.46/0.87  (define @t439 () (@var "Y" tptp.finite824932053eal_sz))
% 0.46/0.87  (define @t440 () (_ (_ tptp.produc1308130519eal_sz @t438) @t439))
% 0.46/0.87  (define @t441 () (_ tptp.produc1111759555eal_sz @t440))
% 0.46/0.87  (define @t442 () (@list @t438 @t439 @t267))
% 0.46/0.87  (define @t443 () (@var "X" tptp.denota610675952t_unit))
% 0.46/0.87  (define @t444 () (_ (_ tptp.produc789536734_sc_sz @t443) @t388))
% 0.46/0.87  (define @t445 () (_ tptp.produc1503602930_sc_sz @t444))
% 0.46/0.87  (define @t446 () (@var "X" tptp.finite1398487019real_c))
% 0.46/0.87  (define @t447 () (@var "Y" tptp.finite1398487019real_c))
% 0.46/0.87  (define @t448 () (_ (_ tptp.produc394644079real_c @t446) @t447))
% 0.46/0.87  (define @t449 () (_ tptp.produc2010422875real_c @t448))
% 0.46/0.87  (define @t450 () (@list @t446 @t447 @t174))
% 0.46/0.87  (define @t451 () (_ tptp.produc4753477_sc_sz @t425))
% 0.46/0.87  (define @t452 () (_ tptp.produc1746886149eal_sz @t430))
% 0.46/0.87  (define @t453 () (_ tptp.produc1422611269z_real @t435))
% 0.46/0.87  (define @t454 () (_ tptp.produc1269210629eal_sz @t440))
% 0.46/0.87  (define @t455 () (@var "A2" tptp.produc866628903_sc_sz))
% 0.46/0.87  (define @t456 () (_ tptp.produc974239792_sc_sz @t444))
% 0.46/0.87  (define @t457 () (_ tptp.produc314122909real_c @t448))
% 0.46/0.87  (define @t458 () (@var "T" tptp.produc1149990247eal_sz))
% 0.46/0.87  (define @t459 () (@var "S2" tptp.produc1149990247eal_sz))
% 0.46/0.87  (define @t460 () (@var "Z" tptp.produc1149990247eal_sz))
% 0.46/0.87  (define @t461 () (@var "Y4" tptp.produc1149990247eal_sz))
% 0.46/0.87  (define @t462 () (@var "T" tptp.produc1821101996_sc_sz))
% 0.46/0.87  (define @t463 () (@var "S2" tptp.produc1821101996_sc_sz))
% 0.46/0.87  (define @t464 () (@var "Z" tptp.produc1821101996_sc_sz))
% 0.46/0.87  (define @t465 () (@var "Y4" tptp.produc1821101996_sc_sz))
% 0.46/0.87  (define @t466 () (@var "T" tptp.produc190496183real_c))
% 0.46/0.87  (define @t467 () (@var "S2" tptp.produc190496183real_c))
% 0.46/0.87  (define @t468 () (@var "Z" tptp.produc190496183real_c))
% 0.46/0.87  (define @t469 () (@var "Y4" tptp.produc190496183real_c))
% 0.46/0.87  (define @t470 () (@var "Prod2" tptp.produc1149990247eal_sz))
% 0.46/0.87  (define @t471 () (@var "Prod2" tptp.produc1821101996_sc_sz))
% 0.46/0.87  (define @t472 () (@var "Prod2" tptp.produc190496183real_c))
% 0.46/0.87  (define @t473 () (@var "Q2" tptp.produc1149990247eal_sz))
% 0.46/0.87  (define @t474 () (@var "P2" tptp.produc1149990247eal_sz))
% 0.46/0.87  (define @t475 () (_ tptp.produc1269210629eal_sz @t474))
% 0.46/0.87  (define @t476 () (_ tptp.produc1111759555eal_sz @t474))
% 0.46/0.87  (define @t477 () (@var "Q2" tptp.produc1821101996_sc_sz))
% 0.46/0.87  (define @t478 () (_ tptp.produc974239792_sc_sz @t397))
% 0.46/0.87  (define @t479 () (_ tptp.produc1503602930_sc_sz @t397))
% 0.46/0.87  (define @t480 () (@var "Q2" tptp.produc190496183real_c))
% 0.46/0.87  (define @t481 () (_ tptp.produc314122909real_c @t393))
% 0.46/0.87  (define @t482 () (_ tptp.produc2010422875real_c @t393))
% 0.46/0.87  (define @t483 () (@var "I4" tptp.c))
% 0.46/0.87  (define @t484 () (@var "I4" tptp.sz))
% 0.46/0.87  (define @t485 () (@var "Theta_2" tptp.trm_sf_sz))
% 0.46/0.87  (define @t486 () (@var "Theta_1" tptp.trm_sf_sz))
% 0.46/0.87  (define @t487 () (_ tptp.dfree_sf_sz @t485))
% 0.46/0.87  (define @t488 () (_ tptp.dfree_sf_sz @t486))
% 0.46/0.87  (define @t489 () (@list @t486 @t485))
% 0.46/0.87  (define @t490 () (@var "Theta_2" tptp.trm_a_c))
% 0.46/0.87  (define @t491 () (@var "Theta_1" tptp.trm_a_c))
% 0.46/0.87  (define @t492 () (_ tptp.dfree_a_c @t490))
% 0.46/0.87  (define @t493 () (_ tptp.dfree_a_c @t491))
% 0.46/0.87  (define @t494 () (@list @t491 @t490))
% 0.46/0.87  (define @t495 () (@var "T3" tptp.produc866628903_sc_sz))
% 0.46/0.87  (define @t496 () (@var "T3" tptp.produc1241881959eal_sz))
% 0.46/0.87  (define @t497 () (@var "T3" tptp.produc1892666919z_real))
% 0.46/0.87  (define @t498 () (@var "T3" tptp.produc1149990247eal_sz))
% 0.46/0.87  (define @t499 () (@var "T3" tptp.produc1821101996_sc_sz))
% 0.46/0.87  (define @t500 () (@var "T3" tptp.produc190496183real_c))
% 0.46/0.87  (define @t501 () (@var "D" tptp.set_a))
% 0.46/0.87  (define @t502 () (@var "B2" tptp.set_a))
% 0.46/0.87  (define @t503 () (_ (_ tptp.ord_less_eq_set_a @t502) @t501))
% 0.46/0.87  (define @t504 () (@var "C2" tptp.set_a))
% 0.46/0.87  (define @t505 () (@var "A2" tptp.set_a))
% 0.46/0.87  (define @t506 () (_ (_ tptp.ord_less_eq_set_a @t505) @t504))
% 0.46/0.87  (define @t507 () (@var "D" (-> tptp.a Bool)))
% 0.46/0.87  (define @t508 () (@var "B2" (-> tptp.a Bool)))
% 0.46/0.87  (define @t509 () (_ (_ tptp.ord_less_eq_a_o @t508) @t507))
% 0.46/0.87  (define @t510 () (@var "C2" (-> tptp.a Bool)))
% 0.46/0.87  (define @t511 () (@var "A2" (-> tptp.a Bool)))
% 0.46/0.87  (define @t512 () (_ (_ tptp.ord_less_eq_a_o @t511) @t510))
% 0.46/0.87  (define @t513 () (@var "D" tptp.finite1398487019real_c))
% 0.46/0.87  (define @t514 () (@var "C2" tptp.finite1398487019real_c))
% 0.46/0.87  (define @t515 () (_ (_ tptp.produc394644079real_c @t514) @t513))
% 0.46/0.87  (define @t516 () (@list @t174 @t171 @t514 @t513))
% 0.46/0.87  (define @t517 () (@var "D" tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (define @t518 () (@var "C2" tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (define @t519 () (_ tptp.ord_le41263445eal_sz @t191))
% 0.46/0.87  (define @t520 () (@var "D" (-> tptp.trm_sf_sz tptp.trm_sf_sz Bool)))
% 0.46/0.87  (define @t521 () (@var "B2" (-> tptp.trm_sf_sz tptp.trm_sf_sz Bool)))
% 0.46/0.87  (define @t522 () (_ (_ tptp.ord_le8515534f_sz_o @t521) @t520))
% 0.46/0.87  (define @t523 () (@var "C2" (-> tptp.trm_sf_sz tptp.trm_sf_sz Bool)))
% 0.46/0.87  (define @t524 () (@var "A2" (-> tptp.trm_sf_sz tptp.trm_sf_sz Bool)))
% 0.46/0.87  (define @t525 () (_ (_ tptp.ord_le8515534f_sz_o @t524) @t523))
% 0.46/0.87  (define @t526 () (@list @t39))
% 0.46/0.87  (define @t527 () (@var "P" (-> tptp.list_f1238882004_sc_sz tptp.list_f1238882004_sc_sz Bool)))
% 0.46/0.87  (define @t528 () (@var "A2" tptp.produc1241881959eal_sz))
% 0.46/0.87  (define @t529 () (@var "P" (-> tptp.set_Fi291318197eal_sz tptp.set_Fi291318197eal_sz Bool)))
% 0.46/0.87  (define @t530 () (@var "A2" tptp.produc1892666919z_real))
% 0.46/0.87  (define @t531 () (@var "P" (-> tptp.bounde472938360z_real tptp.bounde472938360z_real Bool)))
% 0.46/0.87  (define @t532 () (@var "A2" tptp.produc1149990247eal_sz))
% 0.46/0.87  (define @t533 () (@var "P" (-> tptp.finite824932053eal_sz tptp.finite824932053eal_sz Bool)))
% 0.46/0.87  (define @t534 () (@var "P" (-> tptp.denota610675952t_unit tptp.produc866628903_sc_sz Bool)))
% 0.46/0.87  (define @t535 () (@var "A2" tptp.produc190496183real_c))
% 0.46/0.87  (define @t536 () (@var "P" (-> tptp.finite1398487019real_c tptp.finite1398487019real_c Bool)))
% 0.46/0.87  (define @t537 () (@var "Q2" tptp.list_f1238882004_sc_sz))
% 0.46/0.87  (define @t538 () (@var "P2" tptp.list_f1238882004_sc_sz))
% 0.46/0.87  (define @t539 () (_ (_ tptp.produc1822718231_sc_sz @t538) @t537))
% 0.46/0.87  (define @t540 () (@var "Q" (-> tptp.list_f1238882004_sc_sz Bool)))
% 0.46/0.87  (define @t541 () (@var "P" (-> tptp.list_f1238882004_sc_sz Bool)))
% 0.46/0.87  (define @t542 () (@var "Q2" tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (define @t543 () (@var "P2" tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (define @t544 () (_ (_ tptp.produc1235791063eal_sz @t543) @t542))
% 0.46/0.87  (define @t545 () (@var "Q" (-> tptp.set_Fi291318197eal_sz Bool)))
% 0.46/0.87  (define @t546 () (@var "P" (-> tptp.set_Fi291318197eal_sz Bool)))
% 0.46/0.87  (define @t547 () (@var "Q2" tptp.bounde472938360z_real))
% 0.46/0.87  (define @t548 () (@var "P2" tptp.bounde472938360z_real))
% 0.46/0.87  (define @t549 () (_ (_ tptp.produc784663575z_real @t548) @t547))
% 0.46/0.87  (define @t550 () (@var "Q" (-> tptp.bounde472938360z_real Bool)))
% 0.46/0.87  (define @t551 () (@var "P" (-> tptp.bounde472938360z_real Bool)))
% 0.46/0.87  (define @t552 () (@var "Q2" tptp.finite824932053eal_sz))
% 0.46/0.87  (define @t553 () (@var "P2" tptp.finite824932053eal_sz))
% 0.46/0.87  (define @t554 () (_ (_ tptp.produc1308130519eal_sz @t553) @t552))
% 0.46/0.87  (define @t555 () (@var "Q2" tptp.produc866628903_sc_sz))
% 0.46/0.87  (define @t556 () (@var "P2" tptp.denota610675952t_unit))
% 0.46/0.87  (define @t557 () (_ (_ tptp.produc789536734_sc_sz @t556) @t555))
% 0.46/0.87  (define @t558 () (@var "Q" (-> tptp.produc866628903_sc_sz Bool)))
% 0.46/0.87  (define @t559 () (@var "P" (-> tptp.denota610675952t_unit Bool)))
% 0.46/0.87  (define @t560 () (@var "Q2" tptp.finite1398487019real_c))
% 0.46/0.87  (define @t561 () (@var "P2" tptp.finite1398487019real_c))
% 0.46/0.87  (define @t562 () (_ (_ tptp.produc394644079real_c @t561) @t560))
% 0.46/0.87  (define @t563 () (@var "Q" (-> tptp.finite1398487019real_c Bool)))
% 0.46/0.87  (define @t564 () (@var "P" (-> tptp.finite1398487019real_c Bool)))
% 0.46/0.87  (define @t565 () (@var "P" (-> tptp.produc866628903_sc_sz tptp.denota610675952t_unit Bool)))
% 0.46/0.87  (define @t566 () (@var "J" tptp.denota231621370t_unit))
% 0.46/0.87  (define @t567 () (_ @t117 @t566))
% 0.46/0.87  (define @t568 () (@var "B" tptp.set_Su1783761653um_b_c))
% 0.46/0.87  (define @t569 () (_ (_ tptp.ord_le929608341um_b_c @t116) @t568))
% 0.46/0.87  (define @t570 () (_ @t268 @t282))
% 0.46/0.87  (define @t571 () (@var "B" tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (define @t572 () (_ @t283 @t571))
% 0.46/0.87  (define @t573 () (_ tptp.collec1002602816eal_sz (lambda @t285 (and @t284 @t570))))
% 0.46/0.87  (define @t574 () (_ tptp.ord_le41263445eal_sz @t571))
% 0.46/0.87  (define @t575 () (_ @t574 @t281))
% 0.46/0.87  (define @t576 () (_ @t271 @t288))
% 0.46/0.87  (define @t577 () (@var "B" tptp.set_Pr1169339874_sc_sz))
% 0.46/0.87  (define @t578 () (_ @t289 @t577))
% 0.46/0.87  (define @t579 () (_ tptp.collec1199592193_sc_sz (lambda @t291 (and @t290 @t576))))
% 0.46/0.87  (define @t580 () (_ tptp.ord_le1230423618_sc_sz @t577))
% 0.46/0.87  (define @t581 () (_ @t580 @t287))
% 0.46/0.87  (define @t582 () (_ @t94 @t293))
% 0.46/0.87  (define @t583 () (@var "B" tptp.set_trm_sf_sz))
% 0.46/0.87  (define @t584 () (_ @t294 @t583))
% 0.46/0.87  (define @t585 () (_ tptp.collect_trm_sf_sz (lambda @t296 (and @t295 @t582))))
% 0.46/0.87  (define @t586 () (_ tptp.ord_le1697056455_sf_sz @t583))
% 0.46/0.87  (define @t587 () (_ @t586 @t292))
% 0.46/0.87  (define @t588 () (_ @t93 @t298))
% 0.46/0.87  (define @t589 () (@var "B" tptp.set_trm_a_c))
% 0.46/0.87  (define @t590 () (_ @t299 @t589))
% 0.46/0.87  (define @t591 () (_ tptp.collect_trm_a_c (lambda @t301 (and @t300 @t588))))
% 0.46/0.87  (define @t592 () (_ tptp.ord_le1369644495rm_a_c @t589))
% 0.46/0.87  (define @t593 () (_ @t592 @t297))
% 0.46/0.87  (define @t594 () (_ @t276 @t62))
% 0.46/0.87  (define @t595 () (@var "B" tptp.set_a))
% 0.46/0.87  (define @t596 () (_ @t63 @t595))
% 0.46/0.87  (define @t597 () (_ tptp.collect_a (lambda @t66 (and @t303 @t594))))
% 0.46/0.87  (define @t598 () (_ tptp.ord_less_eq_set_a @t595))
% 0.46/0.87  (define @t599 () (_ @t598 @t302))
% 0.46/0.87  (define @t600 () (_ @t279 @t305))
% 0.46/0.87  (define @t601 () (_ @t306 @t568))
% 0.46/0.87  (define @t602 () (_ tptp.collec2086029184um_b_c (lambda @t308 (and @t307 @t600))))
% 0.46/0.87  (define @t603 () (_ tptp.ord_le929608341um_b_c @t568))
% 0.46/0.87  (define @t604 () (_ @t603 @t116))
% 0.46/0.87  (define @t605 () (_ @t309 @t282))
% 0.46/0.87  (define @t606 () (_ tptp.member1693951742eal_sz @t311))
% 0.46/0.87  (define @t607 () (_ @t606 @t571))
% 0.46/0.87  (define @t608 () (_ @t316 @t288))
% 0.46/0.87  (define @t609 () (_ tptp.member1057565379_sc_sz @t318))
% 0.46/0.87  (define @t610 () (_ @t609 @t577))
% 0.46/0.87  (define @t611 () (_ @t323 @t293))
% 0.46/0.87  (define @t612 () (_ tptp.member_trm_sf_sz @t325))
% 0.46/0.87  (define @t613 () (_ @t612 @t583))
% 0.46/0.87  (define @t614 () (_ @t330 @t298))
% 0.46/0.87  (define @t615 () (_ tptp.member_trm_a_c @t332))
% 0.46/0.87  (define @t616 () (_ @t615 @t589))
% 0.46/0.87  (define @t617 () (_ @t337 @t62))
% 0.46/0.87  (define @t618 () (_ tptp.member_a @t339))
% 0.46/0.87  (define @t619 () (_ @t618 @t595))
% 0.46/0.87  (define @t620 () (_ @t344 @t305))
% 0.46/0.87  (define @t621 () (_ tptp.member1893232190um_b_c @t346))
% 0.46/0.87  (define @t622 () (_ @t621 @t568))
% 0.46/0.87  (define @t623 () (@var "Y5" tptp.set_a))
% 0.46/0.87  (define @t624 () (@var "X4" tptp.set_a))
% 0.46/0.87  (define @t625 () (@var "Y" tptp.set_a))
% 0.46/0.87  (define @t626 () (@var "X" tptp.set_a))
% 0.46/0.87  (define @t627 () (_ (_ tptp.ord_less_eq_set_a @t625) @t623))
% 0.46/0.87  (define @t628 () (_ (_ tptp.ord_less_eq_set_a @t626) @t624))
% 0.46/0.87  (define @t629 () (@var "Y5" (-> tptp.a Bool)))
% 0.46/0.87  (define @t630 () (@var "Y" (-> tptp.a Bool)))
% 0.46/0.87  (define @t631 () (_ (_ tptp.ord_less_eq_a_o @t630) @t629))
% 0.46/0.87  (define @t632 () (@var "X4" (-> tptp.a Bool)))
% 0.46/0.87  (define @t633 () (@var "X" (-> tptp.a Bool)))
% 0.46/0.87  (define @t634 () (_ (_ tptp.ord_less_eq_a_o @t633) @t632))
% 0.46/0.87  (define @t635 () (@var "Y5" tptp.finite1398487019real_c))
% 0.46/0.87  (define @t636 () (@var "X4" tptp.finite1398487019real_c))
% 0.46/0.87  (define @t637 () (@var "Y5" tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (define @t638 () (@var "X4" tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (define @t639 () (@var "Y5" (-> tptp.trm_sf_sz tptp.trm_sf_sz Bool)))
% 0.46/0.87  (define @t640 () (@var "Y" (-> tptp.trm_sf_sz tptp.trm_sf_sz Bool)))
% 0.46/0.87  (define @t641 () (_ (_ tptp.ord_le8515534f_sz_o @t640) @t639))
% 0.46/0.87  (define @t642 () (@var "X4" (-> tptp.trm_sf_sz tptp.trm_sf_sz Bool)))
% 0.46/0.87  (define @t643 () (@var "X" (-> tptp.trm_sf_sz tptp.trm_sf_sz Bool)))
% 0.46/0.87  (define @t644 () (_ (_ tptp.ord_le8515534f_sz_o @t643) @t642))
% 0.46/0.87  (define @t645 () (@var "Y" tptp.produc1149990247eal_sz))
% 0.46/0.87  (define @t646 () (@var "X" tptp.produc1149990247eal_sz))
% 0.46/0.87  (define @t647 () (_ (_ tptp.ord_le473656583eal_sz @t646) @t645))
% 0.46/0.87  (define @t648 () (@list @t646 @t645))
% 0.46/0.87  (define @t649 () (@var "X" tptp.produc190496183real_c))
% 0.46/0.87  (define @t650 () (_ (_ tptp.ord_le850691415real_c @t649) @t387))
% 0.46/0.87  (define @t651 () (@list @t649 @t387))
% 0.46/0.87  (define @t652 () (@var "Y3" tptp.finite824932053eal_sz))
% 0.46/0.87  (define @t653 () (@var "Y1" tptp.a))
% 0.46/0.87  (define @t654 () (@var "X1" tptp.a))
% 0.46/0.87  (define @t655 () (@var "A3" tptp.a))
% 0.46/0.87  (define @t656 () (@var "Y" tptp.denota231621370t_unit))
% 0.46/0.87  (define @t657 () (_ tptp.freche1473475332_a_b_c @t656))
% 0.46/0.87  (define @t658 () (_ tptp.collec451781861t_unit tptp.denota258389581_a_b_c))
% 0.46/0.87  (define @t659 () (_ (_ tptp.member1777622435t_unit @t656) @t658))
% 0.46/0.87  (define @t660 () (@list @t656))
% 0.46/0.87  (define @t661 () (@var "Y" tptp.denota610675952t_unit))
% 0.46/0.87  (define @t662 () (_ tptp.freche1784963216_sc_sz @t661))
% 0.46/0.87  (define @t663 () (_ tptp.collec1767975749t_unit tptp.denota1579475975_sc_sz))
% 0.46/0.87  (define @t664 () (_ (_ tptp.member754147591t_unit @t661) @t663))
% 0.46/0.87  (define @t665 () (@list @t661))
% 0.46/0.87  (define @t666 () (_ tptp.ord_le41263445eal_sz @t281))
% 0.46/0.87  (define @t667 () (_ @t606 @t281))
% 0.46/0.87  (define @t668 () (_ tptp.ord_less_eq_set_a @t302))
% 0.46/0.87  (define @t669 () (_ @t668 @t595))
% 0.46/0.87  (define @t670 () (_ @t618 @t302))
% 0.46/0.87  (define @t671 () (@list @t302 @t595))
% 0.46/0.87  (define @t672 () (@var "P" (-> tptp.denota231621370t_unit Bool)))
% 0.46/0.87  (define @t673 () (@var "X3" tptp.freche914690577_a_b_c))
% 0.46/0.87  (define @t674 () (_ tptp.freche1608036107_a_b_c @t673))
% 0.46/0.87  (define @t675 () (@list @t673))
% 0.46/0.87  (define @t676 () (@var "X3" tptp.freche2095075217_sc_sz))
% 0.46/0.87  (define @t677 () (_ tptp.freche1421597129_sc_sz @t676))
% 0.46/0.87  (define @t678 () (@list @t676))
% 0.46/0.87  (define @t679 () (@var "X" tptp.freche914690577_a_b_c))
% 0.46/0.87  (define @t680 () (@list @t679))
% 0.46/0.87  (define @t681 () (@var "Y3" tptp.denota231621370t_unit))
% 0.46/0.87  (define @t682 () (_ (_ tptp.member1777622435t_unit @t681) @t658))
% 0.46/0.87  (define @t683 () (_ tptp.freche1473475332_a_b_c @t681))
% 0.46/0.87  (define @t684 () (@list @t681))
% 0.46/0.87  (define @t685 () (@var "Y3" tptp.denota610675952t_unit))
% 0.46/0.87  (define @t686 () (_ (_ tptp.member754147591t_unit @t685) @t663))
% 0.46/0.87  (define @t687 () (_ tptp.freche1784963216_sc_sz @t685))
% 0.46/0.87  (define @t688 () (@list @t685))
% 0.46/0.87  (define @t689 () (@var "P" (-> tptp.freche914690577_a_b_c Bool)))
% 0.46/0.87  (define @t690 () (@var "P" (-> tptp.freche2095075217_sc_sz Bool)))
% 0.46/0.87  (define @t691 () (@var "X" tptp.denota231621370t_unit))
% 0.46/0.87  (define @t692 () (_ (_ tptp.ord_le1230423618_sc_sz @t272) @t317))
% 0.46/0.87  (define @t693 () (_ (_ tptp.ord_le1697056455_sf_sz @t273) @t324))
% 0.46/0.87  (define @t694 () (_ (_ tptp.ord_le1369644495rm_a_c @t274) @t331))
% 0.46/0.87  (define @t695 () (_ (_ tptp.ord_less_eq_set_a @t277) @t338))
% 0.46/0.87  (define @t696 () (_ (_ tptp.ord_le929608341um_b_c @t280) @t345))
% 0.46/0.87  (define @t697 () (@var "A5" tptp.set_a))
% 0.46/0.87  (define @t698 () (@var "B5" tptp.set_a))
% 0.46/0.87  (define @t699 () (@list @t697 @t698))
% 0.46/0.87  (define @t700 () (@var "Z" tptp.set_a))
% 0.46/0.87  (define @t701 () (@var "Y4" tptp.set_a))
% 0.46/0.87  (define @t702 () (@var "C3" tptp.set_a))
% 0.46/0.87  (define @t703 () (_ @t63 @t698))
% 0.46/0.87  (define @t704 () (_ @t63 @t697))
% 0.46/0.87  (define @t705 () (@var "C2" tptp.a))
% 0.46/0.87  (define @t706 () (_ tptp.member_a @t705))
% 0.46/0.87  (define @t707 () (@var "X" tptp.a))
% 0.46/0.87  (define @t708 () (_ tptp.member_a @t707))
% 0.46/0.87  (define @t709 () (_ @t708 @t302))
% 0.46/0.87  (define @t710 () (@var "Y" tptp.a))
% 0.46/0.87  (define @t711 () (@var "Theta_22" tptp.trm_a_c))
% 0.46/0.87  (define @t712 () (@var "Theta_12" tptp.trm_a_c))
% 0.46/0.87  (define @t713 () (_ tptp.denota2042094639_a_b_c @t566))
% 0.46/0.87  (define @t714 () (_ tptp.denota2042094639_a_b_c @t97))
% 0.46/0.87  (define @t715 () (@var "Theta_22" tptp.trm_sf_sz))
% 0.46/0.87  (define @t716 () (@var "J" tptp.denota610675952t_unit))
% 0.46/0.87  (define @t717 () (@var "Theta_12" tptp.trm_sf_sz))
% 0.46/0.87  (define @t718 () (_ tptp.denota1179238309_sc_sz @t104))
% 0.46/0.87  (define @t719 () (_ tptp.denota1579475975_sc_sz @t104))
% 0.46/0.87  (define @t720 () (@var "G2" (-> tptp.a tptp.produc866628903_sc_sz)))
% 0.46/0.87  (define @t721 () (@var "F2" (-> tptp.a tptp.denota610675952t_unit)))
% 0.46/0.87  (define @t722 () (@var "C2" tptp.produc866628903_sc_sz))
% 0.46/0.87  (define @t723 () (@var "B2" tptp.denota610675952t_unit))
% 0.46/0.87  (define @t724 () (@var "S3" tptp.set_a))
% 0.46/0.87  (define @t725 () (@var "R" tptp.set_a))
% 0.46/0.87  (define @t726 () (_ @t718 @t103))
% 0.46/0.87  (define @t727 () (@var "S3" tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (define @t728 () (@var "F2" tptp.sf))
% 0.46/0.87  (define @t729 () (@var "S4" tptp.set_Pr1169339874_sc_sz))
% 0.46/0.87  (define @t730 () (@var "R2" tptp.set_Pr1169339874_sc_sz))
% 0.46/0.87  (define @t731 () (_ tptp.member1057565379_sc_sz @t409))
% 0.46/0.87  (define @t732 () (@var "F2" tptp.trm_a_c))
% 0.46/0.87  (define @t733 () (@var "S3" tptp.set_Pr1169339874_sc_sz))
% 0.46/0.87  (define @t734 () (@var "R" tptp.set_Pr1169339874_sc_sz))
% 0.46/0.87  (define @t735 () (@var "Y2" tptp.produc866628903_sc_sz))
% 0.46/0.87  (define @t736 () (@var "X2" tptp.denota610675952t_unit))
% 0.46/0.87  (define @t737 () (_ tptp.member1057565379_sc_sz (_ (_ tptp.produc789536734_sc_sz @t736) @t735)))
% 0.46/0.87  (define @t738 () (@list @t736 @t735))
% 0.46/0.87  (define @t739 () (lambda @t738 (_ @t737 @t733)))
% 0.46/0.87  (define @t740 () (lambda @t738 (_ @t737 @t734)))
% 0.46/0.87  (define @t741 () (@list @t734 @t733))
% 0.46/0.87  (define @t742 () (@list @t104 @t103))
% 0.46/0.87  (define @t743 () (@var "T" tptp.finite824932053eal_sz))
% 0.46/0.87  (define @t744 () (@var "G2" (-> tptp.finite824932053eal_sz tptp.bounde472938360z_real)))
% 0.46/0.87  (define @t745 () (@var "F2" (-> tptp.finite824932053eal_sz tptp.bounde472938360z_real)))
% 0.46/0.87  (define @t746 () (@var "A2" tptp.real))
% 0.46/0.87  (define @t747 () (@var "H" (-> tptp.finite824932053eal_sz tptp.real)))
% 0.46/0.87  (define @t748 () (_ @t747 @t743))
% 0.46/0.87  (define @t749 () (_ (_ tptp.ord_less_eq_real @t748) @t746))
% 0.46/0.87  (define @t750 () (@list @t743))
% 0.46/0.87  (define @t751 () (@var "S4" tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (define @t752 () (_ tptp.topolo885751137z_real @t751))
% 0.46/0.87  (define @t753 () (@var "T4" tptp.finite824932053eal_sz))
% 0.46/0.87  (define @t754 () (_ (_ tptp.member1693951742eal_sz @t743) @t751))
% 0.46/0.87  (define @t755 () (= @t191 tptp.top_to1873962757eal_sz))
% 0.46/0.87  (define @t756 () (_ (_ tptp.ord_le41263445eal_sz tptp.top_to1873962757eal_sz) @t191))
% 0.46/0.87  (define @t757 () (@list @t191))
% 0.46/0.87  (define @t758 () (@var "Pid4" tptp.sc))
% 0.46/0.87  (define @t759 () (@var "Pid3" tptp.sc))
% 0.46/0.87  (define @t760 () (@var "Pid2" tptp.sc))
% 0.46/0.87  (define @t761 () (@var "Pid1" tptp.sc))
% 0.46/0.87  (define @t762 () (@var "Fid3" tptp.sf))
% 0.46/0.87  (define @t763 () (@var "Fid2" tptp.sf))
% 0.46/0.87  (define @t764 () (@var "Fid1" tptp.sf))
% 0.46/0.87  (define @t765 () (@var "Vid3" tptp.sz))
% 0.46/0.87  (define @t766 () (@var "Vid2" tptp.sz))
% 0.46/0.87  (define @t767 () (@var "Vid1" tptp.sz))
% 0.46/0.87  (define @t768 () (_ (_ (_ (_ (_ (_ (_ (_ (_ (_ tptp.ids_sz_sf_sc @t767) @t766) @t765) @t764) @t763) @t762) @t761) @t760) @t759) @t758))
% 0.46/0.87  (define @t769 () (@var "P2" tptp.sc))
% 0.46/0.87  (define @t770 () (_ (_ tptp.freche585307148_sc_sz (_ tptp.freche1784963216_sc_sz @t104)) (_ tptp.freche1046279700_sf_sz @t103)))
% 0.46/0.87  (define @t771 () (=> @t719 (=> @t109 (_ (_ tptp.topolo885751137z_real tptp.top_to1873962757eal_sz) @t770))))
% 0.46/0.87  (define @t772 () (@list @t767 @t766 @t765 @t764 @t763 @t762 @t761 @t760 @t759 @t758 @t104 @t103))
% 0.46/0.87  (define @t773 () (@var "V2" tptp.finite824932053eal_sz))
% 0.46/0.87  (define @t774 () (=> @t719 (=> @t109 (= (lambda (@list @t773) (_ tptp.bounde397081123z_real (_ @t106 @t773))) @t770))))
% 0.46/0.87  (define @t775 () (@var "C2" tptp.bounde472938360z_real))
% 0.46/0.87  (define @t776 () (@var "T3" tptp.set_Fi291318197eal_sz))
% 0.46/0.87  (define @t777 () (_ @t752 @t745))
% 0.46/0.87  (define @t778 () (@var "Xa" tptp.trm_sf_sz))
% 0.46/0.87  (define @t779 () (@var "Xb" tptp.denota610675952t_unit))
% 0.46/0.87  (define @t780 () (_ tptp.bNF_eq_onp_trm_sf_sz tptp.dfree_sf_sz))
% 0.46/0.87  (define @t781 () (_ tptp.bNF_eq1660582207t_unit tptp.denota1579475975_sc_sz))
% 0.46/0.87  (define @t782 () (=> (_ (_ @t781 @t779) @t779) (=> (_ (_ @t780 @t778) @t778) (= (_ (_ (_ tptp.freche585307148_sc_sz (_ tptp.freche1784963216_sc_sz @t779)) (_ tptp.freche1046279700_sf_sz @t778)) @t438) (_ tptp.bounde397081123z_real (_ (_ (_ tptp.denota1979904720_sc_sz @t779) @t778) @t438))))))
% 0.46/0.87  (define @t783 () (@var "Z" tptp.denota610675952t_unit))
% 0.46/0.87  (define @t784 () (@var "Y4" tptp.denota610675952t_unit))
% 0.46/0.87  (define @t785 () (@var "Z" tptp.trm_sf_sz))
% 0.46/0.87  (define @t786 () (@var "Y4" tptp.trm_sf_sz))
% 0.46/0.87  (define @t787 () (@var "P" Bool))
% 0.46/0.87  (define @t788 () (@list @t433 @t434))
% 0.46/0.87  (define @t789 () (not @t72))
% 0.46/0.87  (define @t790 () (@var "Y2" tptp.freche2095075217_sc_sz))
% 0.46/0.87  (define @t791 () (lambda (@list @t736 @t790) (= @t736 (_ tptp.freche1421597129_sc_sz @t790))))
% 0.46/0.87  (define @t792 () (@var "Y2" tptp.frechet_strm_sf_sz))
% 0.46/0.87  (define @t793 () (lambda (@list @t293 @t792) (= @t293 (_ tptp.freche782854530_sf_sz @t792))))
% 0.46/0.87  (define @t794 () (@var "Y2" tptp.frechet_strm_a_c))
% 0.46/0.87  (define @t795 () (lambda (@list @t298 @t794) (= @t298 (_ tptp.frechet_raw_term_a_c @t794))))
% 0.46/0.87  (define @t796 () (@var "V2" tptp.produc190496183real_c))
% 0.46/0.87  (define @t797 () (@var "T" tptp.trm_a_c))
% 0.46/0.87  (define @t798 () (@var "I5" tptp.denota231621370t_unit))
% 0.46/0.87  (define @t799 () (lambda (@list @t798 @t797 @t796) (_ (_ (_ (_ tptp.denota229585092_a_b_c @t798) @t797) (_ tptp.produc2010422875real_c @t796)) (_ tptp.produc314122909real_c @t796))))
% 0.46/0.87  (define @t800 () (@var "V2" tptp.produc1149990247eal_sz))
% 0.46/0.87  (define @t801 () (@var "T" tptp.trm_sf_sz))
% 0.46/0.87  (define @t802 () (@var "I5" tptp.denota610675952t_unit))
% 0.46/0.87  (define @t803 () (lambda (@list @t802 @t801 @t800) (_ (_ (_ (_ tptp.denota1979904720_sc_sz @t802) @t801) (_ tptp.produc1111759555eal_sz @t800)) (_ tptp.produc1269210629eal_sz @t800))))
% 0.46/0.87  (define @t804 () (@var "Y2" tptp.produc190496183real_c))
% 0.46/0.87  (define @t805 () (@var "X2" tptp.produc190496183real_c))
% 0.46/0.87  (define @t806 () (lambda (@list @t805 @t804) (and (_ (_ tptp.ord_le775706699real_c (_ tptp.produc2010422875real_c @t805)) (_ tptp.produc2010422875real_c @t804)) (_ (_ tptp.ord_le775706699real_c (_ tptp.produc314122909real_c @t805)) (_ tptp.produc314122909real_c @t804)))))
% 0.46/0.87  (define @t807 () (@var "Y2" tptp.produc1691597095_set_a))
% 0.46/0.87  (define @t808 () (@var "X2" tptp.produc1691597095_set_a))
% 0.46/0.87  (define @t809 () (lambda (@list @t808 @t807) (and (_ (_ tptp.ord_less_eq_set_a (_ tptp.produc1926412547_set_a @t808)) (_ tptp.produc1926412547_set_a @t807)) (_ (_ tptp.ord_less_eq_set_a (_ tptp.produc918972485_set_a @t808)) (_ tptp.produc918972485_set_a @t807)))))
% 0.46/0.87  (define @t810 () (@var "Y2" tptp.produc1989635468_a_a_o))
% 0.46/0.87  (define @t811 () (@var "X2" tptp.produc1989635468_a_a_o))
% 0.46/0.87  (define @t812 () (lambda (@list @t811 @t810) (and (_ (_ tptp.ord_less_eq_set_a (_ tptp.produc1911461786_a_a_o @t811)) (_ tptp.produc1911461786_a_a_o @t810)) (_ (_ tptp.ord_less_eq_a_o (_ tptp.produc23639768_a_a_o @t811)) (_ tptp.produc23639768_a_a_o @t810)))))
% 0.46/0.87  (define @t813 () (@var "Y2" tptp.produc1561113620_set_a))
% 0.46/0.87  (define @t814 () (@var "X2" tptp.produc1561113620_set_a))
% 0.46/0.87  (define @t815 () (lambda (@list @t814 @t813) (and (_ (_ tptp.ord_less_eq_a_o (_ tptp.produc1045727450_set_a @t814)) (_ tptp.produc1045727450_set_a @t813)) (_ (_ tptp.ord_less_eq_set_a (_ tptp.produc1305389080_set_a @t814)) (_ tptp.produc1305389080_set_a @t813)))))
% 0.46/0.87  (define @t816 () (@var "Y2" tptp.produc1149990247eal_sz))
% 0.46/0.87  (define @t817 () (@var "X2" tptp.produc1149990247eal_sz))
% 0.46/0.87  (define @t818 () (lambda (@list @t817 @t816) (and (_ (_ tptp.ord_le787639925eal_sz (_ tptp.produc1111759555eal_sz @t817)) (_ tptp.produc1111759555eal_sz @t816)) (_ (_ tptp.ord_le787639925eal_sz (_ tptp.produc1269210629eal_sz @t817)) (_ tptp.produc1269210629eal_sz @t816)))))
% 0.46/0.87  (define @t819 () (@var "Y2" tptp.product_prod_a_o_a_o))
% 0.46/0.87  (define @t820 () (@var "X2" tptp.product_prod_a_o_a_o))
% 0.46/0.87  (define @t821 () (lambda (@list @t820 @t819) (and (_ (_ tptp.ord_less_eq_a_o (_ tptp.product_fst_a_o_a_o @t820)) (_ tptp.product_fst_a_o_a_o @t819)) (_ (_ tptp.ord_less_eq_a_o (_ tptp.product_snd_a_o_a_o @t820)) (_ tptp.product_snd_a_o_a_o @t819)))))
% 0.46/0.87  (define @t822 () (@var "Y2" tptp.produc1144880887f_sz_o))
% 0.46/0.87  (define @t823 () (@var "X2" tptp.produc1144880887f_sz_o))
% 0.46/0.87  (define @t824 () (lambda (@list @t823 @t822) (and (_ (_ tptp.ord_less_eq_set_a (_ tptp.produc38604755f_sz_o @t823)) (_ tptp.produc38604755f_sz_o @t822)) (_ (_ tptp.ord_le8515534f_sz_o (_ tptp.produc407510293f_sz_o @t823)) (_ tptp.produc407510293f_sz_o @t822)))))
% 0.46/0.87  (define @t825 () (@var "Y2" tptp.produc903182423_set_a))
% 0.46/0.87  (define @t826 () (@var "X2" tptp.produc903182423_set_a))
% 0.46/0.87  (define @t827 () (lambda (@list @t826 @t825) (and (_ (_ tptp.ord_le8515534f_sz_o (_ tptp.produc407272755_set_a @t826)) (_ tptp.produc407272755_set_a @t825)) (_ (_ tptp.ord_less_eq_set_a (_ tptp.produc776178293_set_a @t826)) (_ tptp.produc776178293_set_a @t825)))))
% 0.46/0.87  (define @t828 () (@var "Y2" tptp.produc1065634396_o_a_o))
% 0.46/0.87  (define @t829 () (@var "X2" tptp.produc1065634396_o_a_o))
% 0.46/0.87  (define @t830 () (lambda (@list @t829 @t828) (and (_ (_ tptp.ord_le8515534f_sz_o (_ tptp.produc2013638506_o_a_o @t829)) (_ tptp.produc2013638506_o_a_o @t828)) (_ (_ tptp.ord_less_eq_a_o (_ tptp.produc1630531752_o_a_o @t829)) (_ tptp.produc1630531752_o_a_o @t828)))))
% 0.46/0.87  (define @t831 () (@var "Y2" tptp.produc1553439972f_sz_o))
% 0.46/0.87  (define @t832 () (@var "X2" tptp.produc1553439972f_sz_o))
% 0.46/0.87  (define @t833 () (lambda (@list @t832 @t831) (and (_ (_ tptp.ord_less_eq_a_o (_ tptp.produc1453865130f_sz_o @t832)) (_ tptp.produc1453865130f_sz_o @t831)) (_ (_ tptp.ord_le8515534f_sz_o (_ tptp.produc1070758376f_sz_o @t832)) (_ tptp.produc1070758376f_sz_o @t831)))))
% 0.46/0.87  (define @t834 () (@var "F" tptp.sf))
% 0.46/0.87  (define @t835 () (lambda (@list @t834) (_ (_ tptp.function_sf_sz @t834) tptp.empty_sz_sf)))
% 0.46/0.87  (define @t836 () (@var "T" tptp.a))
% 0.46/0.87  (define @t837 () (_ tptp.member_a @t836))
% 0.46/0.87  (define @t838 () (lambda @t699 (forall (@list @t836) (=> (_ @t837 @t697) (_ @t837 @t698)))))
% 0.46/0.87  (define @t839 () (@var "A6" tptp.a))
% 0.46/0.87  (define @t840 () (@var "G" (-> tptp.a tptp.produc866628903_sc_sz)))
% 0.46/0.87  (define @t841 () (@var "F" (-> tptp.a tptp.denota610675952t_unit)))
% 0.46/0.87  (define @t842 () (@var "Uu" tptp.produc1821101996_sc_sz))
% 0.46/0.87  (define @t843 () (lambda (@list @t697 @t841 @t840) (_ tptp.collec1199592193_sc_sz (lambda (@list @t842) (exists (@list @t839) (and (= @t842 (_ (_ tptp.produc789536734_sc_sz (_ @t841 @t839)) (_ @t840 @t839))) (_ (_ tptp.member_a @t839) @t697)))))))
% 0.46/0.87  (define @t844 () (lambda @t738 (_ @t737 tptp.top_to1499569298_sc_sz)))
% 0.46/0.87  (define @t845 () (tptp.static_FVDiff_a_c @t10))
% 0.46/0.87  (define @t846 () (tptp.denota1997846518gree_c @t13 @t12 @t845))
% 0.46/0.87  (define @t847 () (tptp.plus_a_c @t17 @t10))
% 0.46/0.87  (define @t848 () (tptp.static_FVDiff_a_c @t847))
% 0.46/0.87  (define @t849 () (tptp.denota1997846518gree_c @t13 @t12 @t848))
% 0.46/0.87  (define @t850 () (not @t20))
% 0.46/0.87  (define @t851 () (or @t850 @t16))
% 0.46/0.87  (define @t852 () (tptp.plus_a_c tptp.t1 tptp.t2))
% 0.46/0.87  (define @t853 () (tptp.static_FVDiff_a_c @t852))
% 0.46/0.87  (define @t854 () (tptp.denota1997846518gree_c tptp.nu tptp.nu2 @t853))
% 0.46/0.87  (define @t855 () (tptp.static_FVDiff_a_c tptp.t2))
% 0.46/0.87  (define @t856 () (tptp.denota1997846518gree_c tptp.nu tptp.nu2 @t855))
% 0.46/0.87  (define @t857 () (not @t854))
% 0.46/0.87  (define @t858 () (or @t857 @t856))
% 0.46/0.87  (define @t859 () (not @t858))
% 0.46/0.87  (define @t860 () (@list true false))
% 0.46/0.87  (define @t861 () (forall @t21 (or (not @t849) @t846)))
% 0.46/0.87  (assume @p1 (forall @t9 (=> @t8 @t6)))
% 0.46/0.87  (assume @p2 @t22)
% 0.46/0.87  (assume @p3 @t26)
% 0.46/0.87  (assume @p4 @t27)
% 0.46/0.87  (assume @p5 (_ tptp.dfree_a_c tptp.t2))
% 0.46/0.87  (assume @p6 (forall @t9 (=> @t8 @t28)))
% 0.46/0.87  (assume @p7 (forall @t21 (=> @t20 @t29)))
% 0.46/0.87  (assume @p8 (forall (@list @t31 @t32 @t30) (=> (_ (_ (_ tptp.denota102713844ree_sz @t31) @t32) @t30) (_ (_ (_ tptp.denota102713844ree_sz @t32) @t31) @t30))))
% 0.46/0.87  (assume @p9 (forall (@list @t34 @t35 @t33) (=> (_ (_ (_ tptp.denota1997846518gree_c @t34) @t35) @t33) (_ (_ (_ tptp.denota1997846518gree_c @t35) @t34) @t33))))
% 0.46/0.87  (assume @p10 (forall (@list @t3 @t36) (_ (_ @t4 @t3) @t36)))
% 0.46/0.87  (assume @p11 (forall (@list @t13 @t37) (_ (_ @t14 @t13) @t37)))
% 0.46/0.87  (assume @p12 (_ tptp.dfree_a_c tptp.t1))
% 0.46/0.87  (assume @p13 (forall (@list @t39 @t38) (= (= @t40 (_ tptp.freche1421597129_sc_sz @t38)) (= @t39 @t38))))
% 0.46/0.87  (assume @p14 (forall (@list @t42 @t41) (= (= @t43 (_ tptp.freche782854530_sf_sz @t41)) (= @t42 @t41))))
% 0.46/0.87  (assume @p15 (forall (@list @t45 @t44) (= (= @t46 (_ tptp.frechet_raw_term_a_c @t44)) (= @t45 @t44))))
% 0.46/0.87  (assume @p16 (forall @t9 (=> @t47 @t28)))
% 0.46/0.87  (assume @p17 (forall @t21 (=> @t48 @t29)))
% 0.46/0.87  (assume @p18 (forall @t9 (=> @t47 @t6)))
% 0.46/0.87  (assume @p19 (forall @t21 (=> @t48 @t16)))
% 0.46/0.87  (assume @p20 (forall (@list @t3 @t2 @t52 @t50 @t49) (=> (_ @t5 (_ tptp.static_FVDiff_sf_sz (_ (_ tptp.function_sf_sz @t52) @t50))) (_ @t5 (_ tptp.static_FVDiff_sf_sz @t51)))))
% 0.46/0.87  (assume @p21 (forall (@list @t13 @t12 @t55 @t54 @t53) (=> (_ @t15 (_ tptp.static_FVDiff_a_c (_ (_ tptp.function_a_c @t55) @t54))) (_ @t15 (_ tptp.static_FVDiff_a_c (_ @t54 @t53))))))
% 0.46/0.87  (assume @p22 (= tptp.p_sc_sf_sz tptp.predic913887884_sf_sz))
% 0.46/0.87  (assume @p23 (=> @t72 (=> @t70 (= (_ (_ (_ @t61 tptp.t2) @t60) @t59) (_ (_ (_ @t58 tptp.t2) @t57) @t56)))))
% 0.46/0.87  (assume @p24 (forall (@list @t75) @t76))
% 0.46/0.87  (assume @p25 (forall @t78 (_ (_ tptp.member_trm_a_c @t46) @t77)))
% 0.46/0.87  (assume @p26 (forall @t80 (_ (_ tptp.member_trm_sf_sz @t43) @t79)))
% 0.46/0.87  (assume @p27 (forall @t86 (=> @t85 (not (forall @t84 (not (= @t83 @t82)))))))
% 0.46/0.87  (assume @p28 (forall @t92 (=> @t91 (not (forall @t90 (not (= @t89 @t88)))))))
% 0.46/0.87  (assume @p29 (forall (@list @t83 @t93) (=> @t85 (=> (forall @t84 (_ @t93 @t82)) (_ @t93 @t83)))))
% 0.46/0.87  (assume @p30 (forall (@list @t89 @t94) (=> @t91 (=> (forall @t90 (_ @t94 @t88)) (_ @t94 @t89)))))
% 0.46/0.87  (assume @p31 (forall (@list @t96 @t13 @t12 @t97) (=> @t102 (=> (_ @t15 (_ tptp.static_FVDiff_a_c @t96)) (= (_ (_ @t99 @t101) @t100) (_ (_ @t99 @t95) (_ tptp.produc314122909real_c @t12)))))))
% 0.46/0.87  (assume @p32 (forall (@list @t103 @t3 @t2 @t104) (=> @t109 (=> (_ @t5 (_ tptp.static_FVDiff_sf_sz @t103)) (= (_ (_ @t106 @t108) @t107) (_ (_ @t106 (_ tptp.produc1111759555eal_sz @t2)) (_ tptp.produc1269210629eal_sz @t2)))))))
% 0.46/0.87  (assume @p33 (_ @t69 @t110))
% 0.46/0.87  (assume @p34 @t112)
% 0.46/0.87  (assume @p35 @t70)
% 0.46/0.87  (assume @p36 (=> @t27 (=> @t112 (= (_ (_ (_ @t61 tptp.t1) @t60) @t59) (_ (_ (_ @t58 tptp.t1) @t57) @t56)))))
% 0.46/0.87  (assume @p37 (forall (@list @t114 @t115 @t113) (=> (_ (_ (_ tptp.denota69106024_a_b_c @t114) @t115) @t113) (_ (_ (_ tptp.denota69106024_a_b_c @t115) @t114) @t113))))
% 0.46/0.87  (assume @p38 (forall (@list @t97 @t116) (_ (_ @t117 @t97) @t116)))
% 0.46/0.87  (assume @p39 (_ (_ tptp.ord_le929608341um_b_c @t68) @t110))
% 0.46/0.87  (assume @p40 (_ (_ tptp.ord_le929608341um_b_c @t111) @t110))
% 0.46/0.87  (assume @p41 (forall @t86 (=> @t85 (= (_ tptp.frechet_raw_term_a_c @t118) @t83))))
% 0.46/0.87  (assume @p42 (forall @t92 (=> @t91 (= (_ tptp.freche782854530_sf_sz @t119) @t89))))
% 0.46/0.87  (assume @p43 (forall @t122 (= @t121 @t120)))
% 0.46/0.87  (assume @p44 (forall @t125 (= @t124 @t123)))
% 0.46/0.87  (assume @p45 (forall @t128 (= @t127 @t126)))
% 0.46/0.87  (assume @p46 (forall @t133 (= @t132 @t129)))
% 0.46/0.87  (assume @p47 (forall @t138 (= @t137 @t134)))
% 0.46/0.87  (assume @p48 (forall @t143 (= @t142 @t139)))
% 0.46/0.87  (assume @p49 (forall @t147 (= (_ tptp.dfree_a_c (_ (_ tptp.times_a_c @t145) @t144)) @t146)))
% 0.46/0.87  (assume @p50 (forall @t151 (= (_ tptp.dfree_sf_sz (_ (_ tptp.times_sf_sz @t149) @t148)) @t150)))
% 0.46/0.87  (assume @p51 (forall @t151 (= (_ tptp.dfree_sf_sz (_ (_ tptp.plus_sf_sz @t149) @t148)) @t150)))
% 0.46/0.87  (assume @p52 (forall @t147 (= (_ tptp.dfree_a_c (_ (_ tptp.plus_a_c @t145) @t144)) @t146)))
% 0.46/0.87  (assume @p53 (forall (@list @t153 @t54) (= @t154 (forall (@list @t152) (_ tptp.dfree_a_c (_ @t54 @t152))))))
% 0.46/0.87  (assume @p54 (forall (@list @t156 @t50) (= @t157 (forall (@list @t155) (_ tptp.dfree_sf_sz (_ @t50 @t155))))))
% 0.46/0.87  (assume @p55 (forall @t78 (not (forall @t161 (=> (= @t45 @t160) (not @t159))))))
% 0.46/0.87  (assume @p56 (forall @t80 (not (forall @t165 (=> (= @t42 @t164) (not @t163))))))
% 0.46/0.87  (assume @p57 (forall @t78 (= (_ tptp.freche665377492rm_a_c @t46) @t45)))
% 0.46/0.87  (assume @p58 (forall @t80 (= (_ tptp.freche1046279700_sf_sz @t43) @t42)))
% 0.46/0.87  (assume @p59 (forall (@list @t166 @t83) (=> (_ (_ tptp.member_trm_a_c @t166) @t77) (=> @t85 (= (= (_ tptp.freche665377492rm_a_c @t166) @t118) (= @t166 @t83))))))
% 0.46/0.87  (assume @p60 (forall (@list @t167 @t89) (=> (_ (_ tptp.member_trm_sf_sz @t167) @t79) (=> @t91 (= (= (_ tptp.freche1046279700_sf_sz @t167) @t119) (= @t167 @t89))))))
% 0.46/0.87  (assume @p61 (forall (@list @t168 @t45) (=> (forall @t161 (=> @t159 (_ @t168 @t160))) (_ @t168 @t45))))
% 0.46/0.87  (assume @p62 (forall (@list @t169 @t42) (=> (forall @t165 (=> @t163 (_ @t169 @t164))) (_ @t169 @t42))))
% 0.46/0.87  (assume @p63 (forall @t178 (= @t177 (and @t175 @t172))))
% 0.46/0.87  (assume @p64 (forall @t186 (= @t185 (and @t184 @t181))))
% 0.46/0.87  (assume @p65 (forall @t195 (= @t194 (and @t192 @t189))))
% 0.46/0.87  (assume @p66 (forall @t203 (= @t202 (and @t201 @t198))))
% 0.46/0.87  (assume @p67 (forall @t211 (= @t210 (and @t209 @t206))))
% 0.46/0.87  (assume @p68 (forall (@list @t215 @t213 @t214 @t212) (= (= @t216 (_ (_ tptp.produc394644079real_c @t214) @t212)) (and (= @t215 @t214) (= @t213 @t212)))))
% 0.46/0.87  (assume @p69 (forall (@list @t220 @t218 @t219 @t217) (= (= @t221 (_ (_ tptp.produc1822718231_sc_sz @t219) @t217)) (and (= @t220 @t219) (= @t218 @t217)))))
% 0.46/0.87  (assume @p70 (forall (@list @t225 @t223 @t224 @t222) (= (= @t226 (_ (_ tptp.produc1235791063eal_sz @t224) @t222)) (and (= @t225 @t224) (= @t223 @t222)))))
% 0.46/0.87  (assume @p71 (forall (@list @t230 @t228 @t229 @t227) (= (= @t231 (_ (_ tptp.produc784663575z_real @t229) @t227)) (and (= @t230 @t229) (= @t228 @t227)))))
% 0.46/0.87  (assume @p72 (forall (@list @t235 @t233 @t234 @t232) (= (= @t236 (_ (_ tptp.produc789536734_sc_sz @t234) @t232)) (and (= @t235 @t234) (= @t233 @t232)))))
% 0.46/0.87  (assume @p73 (forall (@list @t240 @t238 @t239 @t237) (= (= @t241 (_ (_ tptp.function_a_c @t239) @t237)) (and (= @t240 @t239) (= @t238 @t237)))))
% 0.46/0.87  (assume @p74 (forall (@list @t245 @t243 @t244 @t242) (= (= @t246 (_ (_ tptp.function_sf_sz @t244) @t242)) (and (= @t245 @t244) (= @t243 @t242)))))
% 0.46/0.87  (assume @p75 (forall (@list @t250 @t248 @t249 @t247) (= (= @t251 (_ (_ tptp.plus_sf_sz @t249) @t247)) (and (= @t250 @t249) (= @t248 @t247)))))
% 0.46/0.87  (assume @p76 (forall (@list @t255 @t253 @t254 @t252) (= (= @t256 (_ (_ tptp.plus_a_c @t254) @t252)) (and (= @t255 @t254) (= @t253 @t252)))))
% 0.46/0.87  (assume @p77 (forall (@list @t260 @t258 @t259 @t257) (= (= @t261 (_ (_ tptp.times_a_c @t259) @t257)) (and (= @t260 @t259) (= @t258 @t257)))))
% 0.46/0.87  (assume @p78 (forall (@list @t265 @t263 @t264 @t262) (= (= @t266 (_ (_ tptp.times_sf_sz @t264) @t262)) (and (= @t265 @t264) (= @t263 @t262)))))
% 0.46/0.87  (assume @p79 (forall (@list @t267 @t268) (= (_ (_ tptp.member1693951742eal_sz @t267) @t269) (_ @t268 @t267))))
% 0.46/0.87  (assume @p80 (forall (@list @t270 @t271) (= (_ (_ tptp.member1057565379_sc_sz @t270) @t272) (_ @t271 @t270))))
% 0.46/0.87  (assume @p81 (forall (@list @t149 @t94) (= (_ (_ tptp.member_trm_sf_sz @t149) @t273) (_ @t94 @t149))))
% 0.46/0.87  (assume @p82 (forall (@list @t145 @t93) (= (_ (_ tptp.member_trm_a_c @t145) @t274) (_ @t93 @t145))))
% 0.46/0.87  (assume @p83 (forall (@list @t275 @t276) (= (_ (_ tptp.member_a @t275) @t277) (_ @t276 @t275))))
% 0.46/0.87  (assume @p84 (forall (@list @t278 @t279) (= (_ (_ tptp.member1893232190um_b_c @t278) @t280) (_ @t279 @t278))))
% 0.46/0.87  (assume @p85 (forall @t286 (= (_ tptp.collec1002602816eal_sz (lambda @t285 @t284)) @t281)))
% 0.46/0.87  (assume @p86 (forall (@list @t287) (= (_ tptp.collec1199592193_sc_sz (lambda @t291 @t290)) @t287)))
% 0.46/0.87  (assume @p87 (forall (@list @t292) (= (_ tptp.collect_trm_sf_sz (lambda @t296 @t295)) @t292)))
% 0.46/0.87  (assume @p88 (forall (@list @t297) (= (_ tptp.collect_trm_a_c (lambda @t301 @t300)) @t297)))
% 0.46/0.87  (assume @p89 (forall @t304 (= (_ tptp.collect_a (lambda @t66 @t303)) @t302)))
% 0.46/0.87  (assume @p90 (forall (@list @t116) (= (_ tptp.collec2086029184um_b_c (lambda @t308 @t307)) @t116)))
% 0.46/0.87  (assume @p91 (forall @t315 (=> (forall @t314 (= @t313 @t312)) (= @t269 @t310))))
% 0.46/0.87  (assume @p92 (forall @t322 (=> (forall @t321 (= @t320 @t319)) (= @t272 @t317))))
% 0.46/0.87  (assume @p93 (forall @t329 (=> (forall @t328 (= @t327 @t326)) (= @t273 @t324))))
% 0.46/0.87  (assume @p94 (forall @t336 (=> (forall @t335 (= @t334 @t333)) (= @t274 @t331))))
% 0.46/0.87  (assume @p95 (forall @t343 (=> (forall @t342 (= @t341 @t340)) (= @t277 @t338))))
% 0.46/0.87  (assume @p96 (forall @t350 (=> (forall @t349 (= @t348 @t347)) (= @t280 @t345))))
% 0.46/0.87  (assume @p97 (forall (@list @t36 @t353 @t3 @t351) (=> (_ (_ tptp.ord_le1110131657_sz_sz @t36) @t353) (=> (_ @t352 @t353) (_ @t352 @t36)))))
% 0.46/0.87  (assume @p98 (forall (@list @t37 @t356 @t13 @t354) (=> (_ (_ tptp.ord_le1772180283um_c_c @t37) @t356) (=> (_ @t355 @t356) (_ @t355 @t37)))))
% 0.46/0.87  (assume @p99 (forall (@list @t353 @t36 @t3 @t2) (=> (_ (_ tptp.ord_le1110131657_sz_sz @t353) @t36) (=> (_ @t5 @t36) (_ @t5 @t353)))))
% 0.46/0.87  (assume @p100 (forall (@list @t356 @t37 @t13 @t12) (=> (_ (_ tptp.ord_le1772180283um_c_c @t356) @t37) (=> (_ @t15 @t37) (_ @t15 @t356)))))
% 0.46/0.87  (assume @p101 (forall (@list @t357 @t139) (=> @t362 (_ @t357 @t139))))
% 0.46/0.87  (assume @p102 (forall (@list @t363 @t120) (=> @t368 (_ @t363 @t120))))
% 0.46/0.87  (assume @p103 (forall (@list @t369 @t123) (=> @t374 (_ @t369 @t123))))
% 0.46/0.87  (assume @p104 (forall (@list @t375 @t126) (=> @t380 (_ @t375 @t126))))
% 0.46/0.87  (assume @p105 (forall (@list @t271 @t134) (=> @t386 (_ @t271 @t134))))
% 0.46/0.87  (assume @p106 (forall (@list @t387) (not (forall @t361 (not (= @t387 @t360))))))
% 0.46/0.87  (assume @p107 (forall (@list @t388) (not (forall @t367 (not (= @t388 @t366))))))
% 0.46/0.87  (assume @p108 (forall (@list @t389) (not (forall @t373 (not (= @t389 @t372))))))
% 0.46/0.87  (assume @p109 (forall (@list @t390) (not (forall @t379 (not (= @t390 @t378))))))
% 0.46/0.87  (assume @p110 (forall @t392 (not (forall @t385 (not (= @t391 @t384))))))
% 0.46/0.87  (assume @p111 (forall @t178 (=> @t177 (not (=> @t175 (not @t172))))))
% 0.46/0.87  (assume @p112 (forall @t186 (=> @t185 (not (=> @t184 (not @t181))))))
% 0.46/0.87  (assume @p113 (forall @t195 (=> @t194 (not (=> @t192 (not @t189))))))
% 0.46/0.87  (assume @p114 (forall @t203 (=> @t202 (not (=> @t201 (not @t198))))))
% 0.46/0.87  (assume @p115 (forall @t211 (=> @t210 (not (=> @t209 (not @t206))))))
% 0.46/0.87  (assume @p116 (forall (@list @t357 @t393) (=> @t362 (_ @t357 @t393))))
% 0.46/0.87  (assume @p117 (forall (@list @t363 @t394) (=> @t368 (_ @t363 @t394))))
% 0.46/0.87  (assume @p118 (forall (@list @t369 @t395) (=> @t374 (_ @t369 @t395))))
% 0.46/0.87  (assume @p119 (forall (@list @t375 @t396) (=> @t380 (_ @t375 @t396))))
% 0.46/0.87  (assume @p120 (forall (@list @t271 @t397) (=> @t386 (_ @t271 @t397))))
% 0.46/0.87  (assume @p121 (forall (@list @t393) (exists @t400 (= @t393 (_ (_ tptp.produc394644079real_c @t399) @t398)))))
% 0.46/0.87  (assume @p122 (forall (@list @t394) (exists (@list @t402 @t401) (= @t394 (_ (_ tptp.produc1822718231_sc_sz @t402) @t401)))))
% 0.46/0.87  (assume @p123 (forall (@list @t395) (exists (@list @t404 @t403) (= @t395 (_ (_ tptp.produc1235791063eal_sz @t404) @t403)))))
% 0.46/0.87  (assume @p124 (forall (@list @t396) (exists (@list @t406 @t405) (= @t396 (_ (_ tptp.produc784663575z_real @t406) @t405)))))
% 0.46/0.87  (assume @p125 (forall (@list @t397) (exists @t410 (= @t397 @t409))))
% 0.46/0.87  (assume @p126 (forall (@list @t271 @t75) (=> (forall @t413 (_ @t271 @t412)) (_ @t271 @t75))))
% 0.46/0.87  (assume @p127 (forall @t392 (not (forall @t413 (not (= @t391 @t412))))))
% 0.46/0.87  (assume @p128 (forall @t414 (= (_ tptp.produc548504323_sc_sz @t221) @t220)))
% 0.46/0.87  (assume @p129 (forall @t415 (= (_ tptp.produc286845635eal_sz @t226) @t225)))
% 0.46/0.87  (assume @p130 (forall @t416 (= (_ tptp.produc870616579z_real @t231) @t230)))
% 0.46/0.87  (assume @p131 (forall @t420 (= (_ tptp.produc1111759555eal_sz @t419) @t417)))
% 0.46/0.87  (assume @p132 (forall @t421 (= (_ tptp.produc1503602930_sc_sz @t236) @t235)))
% 0.46/0.87  (assume @p133 (forall @t422 (= (_ tptp.produc2010422875real_c @t216) @t215)))
% 0.46/0.87  (assume @p134 (forall @t427 (=> (= @t426 @t183) (= @t423 @t183))))
% 0.46/0.87  (assume @p135 (forall @t432 (=> (= @t431 @t191) (= @t428 @t191))))
% 0.46/0.87  (assume @p136 (forall @t437 (=> (= @t436 @t200) (= @t433 @t200))))
% 0.46/0.87  (assume @p137 (forall @t442 (=> (= @t441 @t267) (= @t438 @t267))))
% 0.46/0.87  (assume @p138 (forall (@list @t443 @t388 @t208) (=> (= @t445 @t208) (= @t443 @t208))))
% 0.46/0.87  (assume @p139 (forall @t450 (=> (= @t449 @t174) (= @t446 @t174))))
% 0.46/0.87  (assume @p140 (forall @t414 (= (_ tptp.produc4753477_sc_sz @t221) @t218)))
% 0.46/0.87  (assume @p141 (forall @t415 (= (_ tptp.produc1746886149eal_sz @t226) @t223)))
% 0.46/0.87  (assume @p142 (forall @t416 (= (_ tptp.produc1422611269z_real @t231) @t228)))
% 0.46/0.87  (assume @p143 (forall @t420 (= (_ tptp.produc1269210629eal_sz @t419) @t418)))
% 0.46/0.87  (assume @p144 (forall @t421 (= (_ tptp.produc974239792_sc_sz @t236) @t233)))
% 0.46/0.87  (assume @p145 (forall @t422 (= (_ tptp.produc314122909real_c @t216) @t213)))
% 0.46/0.87  (assume @p146 (forall @t427 (=> (= @t451 @t183) (= @t424 @t183))))
% 0.46/0.87  (assume @p147 (forall @t432 (=> (= @t452 @t191) (= @t429 @t191))))
% 0.46/0.87  (assume @p148 (forall @t437 (=> (= @t453 @t200) (= @t434 @t200))))
% 0.46/0.87  (assume @p149 (forall @t442 (=> (= @t454 @t267) (= @t439 @t267))))
% 0.46/0.87  (assume @p150 (forall (@list @t443 @t388 @t455) (=> (= @t456 @t455) (= @t388 @t455))))
% 0.46/0.87  (assume @p151 (forall @t450 (=> (= @t457 @t174) (= @t447 @t174))))
% 0.46/0.87  (assume @p152 (= (lambda (@list @t461 @t460) (= @t461 @t460)) (lambda (@list @t459 @t458) (and (= (_ tptp.produc1111759555eal_sz @t459) (_ tptp.produc1111759555eal_sz @t458)) (= (_ tptp.produc1269210629eal_sz @t459) (_ tptp.produc1269210629eal_sz @t458))))))
% 0.46/0.87  (assume @p153 (= (lambda (@list @t465 @t464) (= @t465 @t464)) (lambda (@list @t463 @t462) (and (= (_ tptp.produc1503602930_sc_sz @t463) (_ tptp.produc1503602930_sc_sz @t462)) (= (_ tptp.produc974239792_sc_sz @t463) (_ tptp.produc974239792_sc_sz @t462))))))
% 0.46/0.87  (assume @p154 (= (lambda (@list @t469 @t468) (= @t469 @t468)) (lambda (@list @t467 @t466) (and (= (_ tptp.produc2010422875real_c @t467) (_ tptp.produc2010422875real_c @t466)) (= (_ tptp.produc314122909real_c @t467) (_ tptp.produc314122909real_c @t466))))))
% 0.46/0.87  (assume @p155 (forall (@list @t129 @t470) (=> (and (= @t131 (_ tptp.produc1111759555eal_sz @t470)) (= @t130 (_ tptp.produc1269210629eal_sz @t470))) (= @t129 @t470))))
% 0.46/0.87  (assume @p156 (forall (@list @t134 @t471) (=> (and (= @t136 (_ tptp.produc1503602930_sc_sz @t471)) (= @t135 (_ tptp.produc974239792_sc_sz @t471))) (= @t134 @t471))))
% 0.46/0.87  (assume @p157 (forall (@list @t139 @t472) (=> (and (= @t141 (_ tptp.produc2010422875real_c @t472)) (= @t140 (_ tptp.produc314122909real_c @t472))) (= @t139 @t472))))
% 0.46/0.87  (assume @p158 (forall (@list @t474 @t473) (=> (= @t476 (_ tptp.produc1111759555eal_sz @t473)) (=> (= @t475 (_ tptp.produc1269210629eal_sz @t473)) (= @t474 @t473)))))
% 0.46/0.87  (assume @p159 (forall (@list @t397 @t477) (=> (= @t479 (_ tptp.produc1503602930_sc_sz @t477)) (=> (= @t478 (_ tptp.produc974239792_sc_sz @t477)) (= @t397 @t477)))))
% 0.46/0.87  (assume @p160 (forall (@list @t393 @t480) (=> (= @t482 (_ tptp.produc2010422875real_c @t480)) (=> (= @t481 (_ tptp.produc314122909real_c @t480)) (= @t393 @t480)))))
% 0.46/0.87  (assume @p161 (forall (@list @t54 @t153) (=> (forall (@list @t483) (_ tptp.dfree_a_c (_ @t54 @t483))) @t154)))
% 0.46/0.87  (assume @p162 (forall (@list @t50 @t156) (=> (forall (@list @t484) (_ tptp.dfree_sf_sz (_ @t50 @t484))) @t157)))
% 0.46/0.87  (assume @p163 (forall @t489 (=> @t488 (=> @t487 (_ tptp.dfree_sf_sz (_ (_ tptp.plus_sf_sz @t486) @t485))))))
% 0.46/0.87  (assume @p164 (forall @t494 (=> @t493 (=> @t492 (_ tptp.dfree_a_c (_ (_ tptp.plus_a_c @t491) @t490))))))
% 0.46/0.87  (assume @p165 (forall @t494 (=> @t493 (=> @t492 (_ tptp.dfree_a_c (_ (_ tptp.times_a_c @t491) @t490))))))
% 0.46/0.87  (assume @p166 (forall @t489 (=> @t488 (=> @t487 (_ tptp.dfree_sf_sz (_ (_ tptp.times_sf_sz @t486) @t485))))))
% 0.46/0.87  (assume @p167 (forall (@list @t240 @t238 @t255 @t253) (not (= @t241 @t256))))
% 0.46/0.87  (assume @p168 (forall (@list @t245 @t243 @t250 @t248) (not (= @t246 @t251))))
% 0.46/0.87  (assume @p169 (forall (@list @t240 @t238 @t260 @t258) (not (= @t241 @t261))))
% 0.46/0.87  (assume @p170 (forall (@list @t245 @t243 @t265 @t263) (not (= @t246 @t266))))
% 0.46/0.87  (assume @p171 (forall (@list @t250 @t248 @t265 @t263) (not (= @t251 @t266))))
% 0.46/0.87  (assume @p172 (forall (@list @t255 @t253 @t260 @t258) (not (= @t256 @t261))))
% 0.46/0.87  (assume @p173 (forall (@list @t495) (= @t495 (_ (_ tptp.produc1822718231_sc_sz (_ tptp.produc548504323_sc_sz @t495)) (_ tptp.produc4753477_sc_sz @t495)))))
% 0.46/0.87  (assume @p174 (forall (@list @t496) (= @t496 (_ (_ tptp.produc1235791063eal_sz (_ tptp.produc286845635eal_sz @t496)) (_ tptp.produc1746886149eal_sz @t496)))))
% 0.46/0.87  (assume @p175 (forall (@list @t497) (= @t497 (_ (_ tptp.produc784663575z_real (_ tptp.produc870616579z_real @t497)) (_ tptp.produc1422611269z_real @t497)))))
% 0.46/0.87  (assume @p176 (forall (@list @t498) (= @t498 (_ (_ tptp.produc1308130519eal_sz (_ tptp.produc1111759555eal_sz @t498)) (_ tptp.produc1269210629eal_sz @t498)))))
% 0.46/0.87  (assume @p177 (forall (@list @t499) (= @t499 (_ (_ tptp.produc789536734_sc_sz (_ tptp.produc1503602930_sc_sz @t499)) (_ tptp.produc974239792_sc_sz @t499)))))
% 0.46/0.87  (assume @p178 (forall (@list @t500) (= @t500 (_ (_ tptp.produc394644079real_c (_ tptp.produc2010422875real_c @t500)) (_ tptp.produc314122909real_c @t500)))))
% 0.46/0.87  (assume @p179 (forall @t122 (= @t120 @t121)))
% 0.46/0.87  (assume @p180 (forall @t125 (= @t123 @t124)))
% 0.46/0.87  (assume @p181 (forall @t128 (= @t126 @t127)))
% 0.46/0.87  (assume @p182 (forall @t133 (= @t129 @t132)))
% 0.46/0.87  (assume @p183 (forall @t138 (= @t134 @t137)))
% 0.46/0.87  (assume @p184 (forall @t143 (= @t139 @t142)))
% 0.46/0.87  (assume @p185 (forall (@list @t505 @t502 @t504 @t501) (= (_ (_ tptp.ord_le486764743_set_a (_ (_ tptp.produc1928581911_set_a @t505) @t502)) (_ (_ tptp.produc1928581911_set_a @t504) @t501)) (and @t506 @t503))))
% 0.46/0.87  (assume @p186 (forall (@list @t505 @t508 @t504 @t507) (= (_ (_ tptp.ord_le501349868_a_a_o (_ (_ tptp.produc634809990_a_a_o @t505) @t508)) (_ (_ tptp.produc634809990_a_a_o @t504) @t507)) (and @t506 @t509))))
% 0.46/0.87  (assume @p187 (forall (@list @t511 @t502 @t510 @t501) (= (_ (_ tptp.ord_le72828020_set_a (_ (_ tptp.produc1916559302_set_a @t511) @t502)) (_ (_ tptp.produc1916559302_set_a @t510) @t501)) (and @t512 @t503))))
% 0.46/0.87  (assume @p188 (forall @t516 (= (_ (_ tptp.ord_le850691415real_c @t176) @t515) (and (_ (_ tptp.ord_le775706699real_c @t174) @t514) (_ (_ tptp.ord_le775706699real_c @t171) @t513)))))
% 0.46/0.87  (assume @p189 (forall (@list @t511 @t508 @t510 @t507) (= (_ (_ tptp.ord_le1883211903_o_a_o (_ (_ tptp.product_Pair_a_o_a_o @t511) @t508)) (_ (_ tptp.product_Pair_a_o_a_o @t510) @t507)) (and @t512 @t509))))
% 0.46/0.87  (assume @p190 (forall (@list @t191 @t188 @t518 @t517) (= (_ (_ tptp.ord_le978883847eal_sz @t193) (_ (_ tptp.produc1235791063eal_sz @t518) @t517)) (and (_ @t519 @t518) (_ (_ tptp.ord_le41263445eal_sz @t188) @t517)))))
% 0.46/0.87  (assume @p191 (forall (@list @t505 @t521 @t504 @t520) (= (_ (_ tptp.ord_le1884788375f_sz_o (_ (_ tptp.produc1174558183f_sz_o @t505) @t521)) (_ (_ tptp.produc1174558183f_sz_o @t504) @t520)) (and @t506 @t522))))
% 0.46/0.87  (assume @p192 (forall (@list @t524 @t502 @t523 @t501) (= (_ (_ tptp.ord_le1643089911_set_a (_ (_ tptp.produc1543226183_set_a @t524) @t502)) (_ (_ tptp.produc1543226183_set_a @t523) @t501)) (and @t525 @t503))))
% 0.46/0.87  (assume @p193 (forall (@list @t524 @t508 @t523 @t507) (= (_ (_ tptp.ord_le2132572860_o_a_o (_ (_ tptp.produc1152932438_o_a_o @t524) @t508)) (_ (_ tptp.produc1152932438_o_a_o @t523) @t507)) (and @t525 @t509))))
% 0.46/0.87  (assume @p194 (forall (@list @t511 @t521 @t510 @t520) (= (_ (_ tptp.ord_le472894788f_sz_o (_ (_ tptp.produc593159062f_sz_o @t511) @t521)) (_ (_ tptp.produc593159062f_sz_o @t510) @t520)) (and @t512 @t522))))
% 0.46/0.87  (assume @p195 (forall @t526 (= (_ tptp.freche1784963216_sc_sz @t40) @t39)))
% 0.46/0.87  (assume @p196 (_ (_ (_ tptp.type_d1238563341rm_a_c tptp.frechet_raw_term_a_c) tptp.freche665377492rm_a_c) @t77))
% 0.46/0.87  (assume @p197 (_ (_ (_ tptp.type_d46389773_sf_sz tptp.freche782854530_sf_sz) tptp.freche1046279700_sf_sz) @t79))
% 0.46/0.87  (assume @p198 (forall (@list @t527 @t423 @t424 @t455) (=> (_ (_ @t527 @t423) @t424) (=> (= @t455 @t425) (_ (_ @t527 (_ tptp.produc548504323_sc_sz @t455)) (_ tptp.produc4753477_sc_sz @t455))))))
% 0.46/0.87  (assume @p199 (forall (@list @t529 @t428 @t429 @t528) (=> (_ (_ @t529 @t428) @t429) (=> (= @t528 @t430) (_ (_ @t529 (_ tptp.produc286845635eal_sz @t528)) (_ tptp.produc1746886149eal_sz @t528))))))
% 0.46/0.87  (assume @p200 (forall (@list @t531 @t433 @t434 @t530) (=> (_ (_ @t531 @t433) @t434) (=> (= @t530 @t435) (_ (_ @t531 (_ tptp.produc870616579z_real @t530)) (_ tptp.produc1422611269z_real @t530))))))
% 0.46/0.87  (assume @p201 (forall (@list @t533 @t438 @t439 @t532) (=> (_ (_ @t533 @t438) @t439) (=> (= @t532 @t440) (_ (_ @t533 (_ tptp.produc1111759555eal_sz @t532)) (_ tptp.produc1269210629eal_sz @t532))))))
% 0.46/0.87  (assume @p202 (forall (@list @t534 @t443 @t388 @t270) (=> (_ (_ @t534 @t443) @t388) (=> (= @t270 @t444) (_ (_ @t534 (_ tptp.produc1503602930_sc_sz @t270)) (_ tptp.produc974239792_sc_sz @t270))))))
% 0.46/0.87  (assume @p203 (forall (@list @t536 @t446 @t447 @t535) (=> (_ (_ @t536 @t446) @t447) (=> (= @t535 @t448) (_ (_ @t536 (_ tptp.produc2010422875real_c @t535)) (_ tptp.produc314122909real_c @t535))))))
% 0.46/0.87  (assume @p204 (forall (@list @t541 @t538 @t540 @t537) (=> (_ @t541 @t538) (=> (_ @t540 @t537) (and (_ @t541 (_ tptp.produc548504323_sc_sz @t539)) (_ @t540 (_ tptp.produc4753477_sc_sz @t539)))))))
% 0.46/0.87  (assume @p205 (forall (@list @t546 @t543 @t545 @t542) (=> (_ @t546 @t543) (=> (_ @t545 @t542) (and (_ @t546 (_ tptp.produc286845635eal_sz @t544)) (_ @t545 (_ tptp.produc1746886149eal_sz @t544)))))))
% 0.46/0.87  (assume @p206 (forall (@list @t551 @t548 @t550 @t547) (=> (_ @t551 @t548) (=> (_ @t550 @t547) (and (_ @t551 (_ tptp.produc870616579z_real @t549)) (_ @t550 (_ tptp.produc1422611269z_real @t549)))))))
% 0.46/0.87  (assume @p207 (forall (@list @t268 @t553 @t309 @t552) (=> (_ @t268 @t553) (=> (_ @t309 @t552) (and (_ @t268 (_ tptp.produc1111759555eal_sz @t554)) (_ @t309 (_ tptp.produc1269210629eal_sz @t554)))))))
% 0.46/0.87  (assume @p208 (forall (@list @t559 @t556 @t558 @t555) (=> (_ @t559 @t556) (=> (_ @t558 @t555) (and (_ @t559 (_ tptp.produc1503602930_sc_sz @t557)) (_ @t558 (_ tptp.produc974239792_sc_sz @t557)))))))
% 0.46/0.87  (assume @p209 (forall (@list @t564 @t561 @t563 @t560) (=> (_ @t564 @t561) (=> (_ @t563 @t560) (and (_ @t564 (_ tptp.produc2010422875real_c @t562)) (_ @t563 (_ tptp.produc314122909real_c @t562)))))))
% 0.46/0.87  (assume @p210 (forall (@list @t527 @t424 @t423) (=> (_ (_ @t527 @t424) @t423) (_ (_ @t527 @t451) @t426))))
% 0.46/0.87  (assume @p211 (forall (@list @t529 @t429 @t428) (=> (_ (_ @t529 @t429) @t428) (_ (_ @t529 @t452) @t431))))
% 0.46/0.87  (assume @p212 (forall (@list @t531 @t434 @t433) (=> (_ (_ @t531 @t434) @t433) (_ (_ @t531 @t453) @t436))))
% 0.46/0.87  (assume @p213 (forall (@list @t533 @t439 @t438) (=> (_ (_ @t533 @t439) @t438) (_ (_ @t533 @t454) @t441))))
% 0.46/0.87  (assume @p214 (forall (@list @t565 @t388 @t443) (=> (_ (_ @t565 @t388) @t443) (_ (_ @t565 @t456) @t445))))
% 0.46/0.87  (assume @p215 (forall (@list @t536 @t447 @t446) (=> (_ (_ @t536 @t447) @t446) (_ (_ @t536 @t457) @t449))))
% 0.46/0.87  (assume @p216 (forall (@list @t116 @t568 @t97 @t566) (=> @t569 (=> (_ @t567 @t568) (_ @t567 @t116)))))
% 0.46/0.87  (assume @p217 (forall (@list @t571 @t281 @t268) (=> @t575 (= (_ @t574 @t573) (forall @t285 (=> @t572 @t570))))))
% 0.46/0.87  (assume @p218 (forall (@list @t577 @t287 @t271) (=> @t581 (= (_ @t580 @t579) (forall @t291 (=> @t578 @t576))))))
% 0.46/0.87  (assume @p219 (forall (@list @t583 @t292 @t94) (=> @t587 (= (_ @t586 @t585) (forall @t296 (=> @t584 @t582))))))
% 0.46/0.87  (assume @p220 (forall (@list @t589 @t297 @t93) (=> @t593 (= (_ @t592 @t591) (forall @t301 (=> @t590 @t588))))))
% 0.46/0.87  (assume @p221 (forall (@list @t595 @t302 @t276) (=> @t599 (= (_ @t598 @t597) (forall @t66 (=> @t596 @t594))))))
% 0.46/0.87  (assume @p222 (forall (@list @t568 @t116 @t279) (=> @t604 (= (_ @t603 @t602) (forall @t308 (=> @t601 @t600))))))
% 0.46/0.87  (assume @p223 (forall (@list @t571 @t281 @t309 @t268) (=> @t575 (=> (forall @t314 (=> @t607 (=> @t312 @t313))) (_ (_ tptp.ord_le41263445eal_sz (_ tptp.collec1002602816eal_sz (lambda @t285 (and @t572 @t605)))) @t573)))))
% 0.46/0.87  (assume @p224 (forall (@list @t577 @t287 @t316 @t271) (=> @t581 (=> (forall @t321 (=> @t610 (=> @t319 @t320))) (_ (_ tptp.ord_le1230423618_sc_sz (_ tptp.collec1199592193_sc_sz (lambda @t291 (and @t578 @t608)))) @t579)))))
% 0.46/0.87  (assume @p225 (forall (@list @t583 @t292 @t323 @t94) (=> @t587 (=> (forall @t328 (=> @t613 (=> @t326 @t327))) (_ (_ tptp.ord_le1697056455_sf_sz (_ tptp.collect_trm_sf_sz (lambda @t296 (and @t584 @t611)))) @t585)))))
% 0.46/0.87  (assume @p226 (forall (@list @t589 @t297 @t330 @t93) (=> @t593 (=> (forall @t335 (=> @t616 (=> @t333 @t334))) (_ (_ tptp.ord_le1369644495rm_a_c (_ tptp.collect_trm_a_c (lambda @t301 (and @t590 @t614)))) @t591)))))
% 0.46/0.87  (assume @p227 (forall (@list @t595 @t302 @t337 @t276) (=> @t599 (=> (forall @t342 (=> @t619 (=> @t340 @t341))) (_ (_ tptp.ord_less_eq_set_a (_ tptp.collect_a (lambda @t66 (and @t596 @t617)))) @t597)))))
% 0.46/0.87  (assume @p228 (forall (@list @t568 @t116 @t344 @t279) (=> @t604 (=> (forall @t349 (=> @t622 (=> @t347 @t348))) (_ (_ tptp.ord_le929608341um_b_c (_ tptp.collec2086029184um_b_c (lambda @t308 (and @t601 @t620)))) @t602)))))
% 0.46/0.87  (assume @p229 (forall (@list @t626 @t624 @t625 @t623) (=> @t628 (=> @t627 (_ (_ tptp.ord_le486764743_set_a (_ (_ tptp.produc1928581911_set_a @t626) @t625)) (_ (_ tptp.produc1928581911_set_a @t624) @t623))))))
% 0.46/0.87  (assume @p230 (forall (@list @t626 @t624 @t630 @t629) (=> @t628 (=> @t631 (_ (_ tptp.ord_le501349868_a_a_o (_ (_ tptp.produc634809990_a_a_o @t626) @t630)) (_ (_ tptp.produc634809990_a_a_o @t624) @t629))))))
% 0.46/0.87  (assume @p231 (forall (@list @t633 @t632 @t625 @t623) (=> @t634 (=> @t627 (_ (_ tptp.ord_le72828020_set_a (_ (_ tptp.produc1916559302_set_a @t633) @t625)) (_ (_ tptp.produc1916559302_set_a @t632) @t623))))))
% 0.46/0.87  (assume @p232 (forall (@list @t446 @t636 @t447 @t635) (=> (_ (_ tptp.ord_le775706699real_c @t446) @t636) (=> (_ (_ tptp.ord_le775706699real_c @t447) @t635) (_ (_ tptp.ord_le850691415real_c @t448) (_ (_ tptp.produc394644079real_c @t636) @t635))))))
% 0.46/0.87  (assume @p233 (forall (@list @t633 @t632 @t630 @t629) (=> @t634 (=> @t631 (_ (_ tptp.ord_le1883211903_o_a_o (_ (_ tptp.product_Pair_a_o_a_o @t633) @t630)) (_ (_ tptp.product_Pair_a_o_a_o @t632) @t629))))))
% 0.46/0.87  (assume @p234 (forall (@list @t428 @t638 @t429 @t637) (=> (_ (_ tptp.ord_le41263445eal_sz @t428) @t638) (=> (_ (_ tptp.ord_le41263445eal_sz @t429) @t637) (_ (_ tptp.ord_le978883847eal_sz @t430) (_ (_ tptp.produc1235791063eal_sz @t638) @t637))))))
% 0.46/0.87  (assume @p235 (forall (@list @t626 @t624 @t640 @t639) (=> @t628 (=> @t641 (_ (_ tptp.ord_le1884788375f_sz_o (_ (_ tptp.produc1174558183f_sz_o @t626) @t640)) (_ (_ tptp.produc1174558183f_sz_o @t624) @t639))))))
% 0.46/0.87  (assume @p236 (forall (@list @t643 @t642 @t625 @t623) (=> @t644 (=> @t627 (_ (_ tptp.ord_le1643089911_set_a (_ (_ tptp.produc1543226183_set_a @t643) @t625)) (_ (_ tptp.produc1543226183_set_a @t642) @t623))))))
% 0.46/0.87  (assume @p237 (forall (@list @t643 @t642 @t630 @t629) (=> @t644 (=> @t631 (_ (_ tptp.ord_le2132572860_o_a_o (_ (_ tptp.produc1152932438_o_a_o @t643) @t630)) (_ (_ tptp.produc1152932438_o_a_o @t642) @t629))))))
% 0.46/0.87  (assume @p238 (forall (@list @t633 @t632 @t640 @t639) (=> @t634 (=> @t641 (_ (_ tptp.ord_le472894788f_sz_o (_ (_ tptp.produc593159062f_sz_o @t633) @t640)) (_ (_ tptp.produc593159062f_sz_o @t632) @t639))))))
% 0.46/0.87  (assume @p239 (forall @t648 (=> @t647 (_ (_ tptp.ord_le787639925eal_sz (_ tptp.produc1111759555eal_sz @t646)) (_ tptp.produc1111759555eal_sz @t645)))))
% 0.46/0.87  (assume @p240 (forall @t651 (=> @t650 (_ (_ tptp.ord_le775706699real_c (_ tptp.produc2010422875real_c @t649)) (_ tptp.produc2010422875real_c @t387)))))
% 0.46/0.87  (assume @p241 (forall @t648 (=> @t647 (_ (_ tptp.ord_le787639925eal_sz (_ tptp.produc1269210629eal_sz @t646)) (_ tptp.produc1269210629eal_sz @t645)))))
% 0.46/0.87  (assume @p242 (forall @t651 (=> @t650 (_ (_ tptp.ord_le775706699real_c (_ tptp.produc314122909real_c @t649)) (_ tptp.produc314122909real_c @t387)))))
% 0.46/0.87  (assume @p243 (forall (@list @t533 @t474) (=> (_ (_ @t533 @t475) @t476) (not (forall (@list @t311 @t652) (not (_ (_ @t533 @t652) @t311)))))))
% 0.46/0.87  (assume @p244 (forall (@list @t565 @t397) (=> (_ (_ @t565 @t478) @t479) (not (forall @t410 (not (_ (_ @t565 @t407) @t408)))))))
% 0.46/0.87  (assume @p245 (forall (@list @t536 @t393) (=> (_ (_ @t536 @t481) @t482) (not (forall @t400 (not (_ (_ @t536 @t398) @t399)))))))
% 0.46/0.87  (assume @p246 (forall (@list @t654 @t653) (= (= (_ tptp.sum_In2139678582um_b_c @t654) (_ tptp.sum_In2139678582um_b_c @t653)) (= @t654 @t653))))
% 0.46/0.87  (assume @p247 (forall (@list @t275 @t655) (= (= (_ tptp.sum_In2139678582um_b_c @t275) (_ tptp.sum_In2139678582um_b_c @t655)) (= @t275 @t655))))
% 0.46/0.87  (assume @p248 (forall @t660 (=> @t659 (= (_ tptp.freche1608036107_a_b_c @t657) @t656))))
% 0.46/0.87  (assume @p249 (forall @t665 (=> @t664 (= (_ tptp.freche1421597129_sc_sz @t662) @t661))))
% 0.46/0.87  (assume @p250 (forall (@list @t281 @t571) (=> (forall @t314 (=> @t667 @t607)) (_ @t666 @t571))))
% 0.46/0.87  (assume @p251 (forall (@list @t287 @t577) (=> (forall @t321 (=> (_ @t609 @t287) @t610)) (_ (_ tptp.ord_le1230423618_sc_sz @t287) @t577))))
% 0.46/0.87  (assume @p252 (forall (@list @t116 @t568) (=> (forall @t349 (=> (_ @t621 @t116) @t622)) @t569)))
% 0.46/0.87  (assume @p253 (forall (@list @t292 @t583) (=> (forall @t328 (=> (_ @t612 @t292) @t613)) (_ (_ tptp.ord_le1697056455_sf_sz @t292) @t583))))
% 0.46/0.87  (assume @p254 (forall (@list @t297 @t589) (=> (forall @t335 (=> (_ @t615 @t297) @t616)) (_ (_ tptp.ord_le1369644495rm_a_c @t297) @t589))))
% 0.46/0.87  (assume @p255 (forall @t671 (=> (forall @t342 (=> @t670 @t619)) @t669)))
% 0.46/0.87  (assume @p256 (forall (@list @t656 @t672) (=> @t659 (=> (forall @t675 (_ @t672 @t674)) (_ @t672 @t656)))))
% 0.46/0.87  (assume @p257 (forall (@list @t661 @t559) (=> @t664 (=> (forall @t678 (_ @t559 @t677)) (_ @t559 @t661)))))
% 0.46/0.87  (assume @p258 (forall @t660 (=> @t659 (not (forall @t675 (not (= @t656 @t674)))))))
% 0.46/0.87  (assume @p259 (forall @t665 (=> @t664 (not (forall @t678 (not (= @t661 @t677)))))))
% 0.46/0.87  (assume @p260 (forall @t680 (_ (_ tptp.member1777622435t_unit (_ tptp.freche1608036107_a_b_c @t679)) @t658)))
% 0.46/0.87  (assume @p261 (forall @t526 (_ (_ tptp.member754147591t_unit @t40) @t663)))
% 0.46/0.87  (assume @p262 (forall @t680 (not (forall @t684 (=> (= @t679 @t683) (not @t682))))))
% 0.46/0.87  (assume @p263 (forall @t526 (not (forall @t688 (=> (= @t39 @t687) (not @t686))))))
% 0.46/0.87  (assume @p264 (forall (@list @t689 @t679) (=> (forall @t684 (=> @t682 (_ @t689 @t683))) (_ @t689 @t679))))
% 0.46/0.87  (assume @p265 (forall (@list @t690 @t39) (=> (forall @t688 (=> @t686 (_ @t690 @t687))) (_ @t690 @t39))))
% 0.46/0.87  (assume @p266 (forall (@list @t691 @t656) (=> (_ (_ tptp.member1777622435t_unit @t691) @t658) (=> @t659 (= (= (_ tptp.freche1473475332_a_b_c @t691) @t657) (= @t691 @t656))))))
% 0.46/0.87  (assume @p267 (forall (@list @t443 @t661) (=> (_ (_ tptp.member754147591t_unit @t443) @t663) (=> @t664 (= (= (_ tptp.freche1784963216_sc_sz @t443) @t662) (= @t443 @t661))))))
% 0.46/0.87  (assume @p268 (forall @t671 (=> @t669 (=> @t599 (= @t302 @t595)))))
% 0.46/0.87  (assume @p269 (forall @t315 (= (_ (_ tptp.ord_le41263445eal_sz @t269) @t310) (forall @t285 (=> @t570 @t605)))))
% 0.46/0.87  (assume @p270 (forall @t322 (= @t692 (forall @t291 (=> @t576 @t608)))))
% 0.46/0.87  (assume @p271 (forall @t329 (= @t693 (forall @t296 (=> @t582 @t611)))))
% 0.46/0.87  (assume @p272 (forall @t336 (= @t694 (forall @t301 (=> @t588 @t614)))))
% 0.46/0.87  (assume @p273 (forall @t343 (= @t695 (forall @t66 (=> @t594 @t617)))))
% 0.46/0.87  (assume @p274 (forall @t350 (= @t696 (forall @t308 (=> @t600 @t620)))))
% 0.46/0.87  (assume @p275 (= (lambda (@list @t701 @t700) (= @t701 @t700)) (lambda @t699 (and (_ (_ tptp.ord_less_eq_set_a @t697) @t698) (_ (_ tptp.ord_less_eq_set_a @t698) @t697)))))
% 0.46/0.87  (assume @p276 (forall (@list @t302 @t595 @t702) (=> @t669 (=> (_ @t598 @t702) (_ @t668 @t702)))))
% 0.46/0.87  (assume @p277 (forall @t322 (=> (forall @t321 (=> @t320 @t319)) @t692)))
% 0.46/0.87  (assume @p278 (forall @t329 (=> (forall @t328 (=> @t327 @t326)) @t693)))
% 0.46/0.87  (assume @p279 (forall @t336 (=> (forall @t335 (=> @t334 @t333)) @t694)))
% 0.46/0.87  (assume @p280 (forall @t343 (=> (forall @t342 (=> @t341 @t340)) @t695)))
% 0.46/0.87  (assume @p281 (forall @t350 (=> (forall @t349 (=> @t348 @t347)) @t696)))
% 0.46/0.87  (assume @p282 (= tptp.ord_less_eq_set_a (lambda @t699 (forall @t66 (=> @t704 @t703)))))
% 0.46/0.87  (assume @p283 (forall (@list @t302 @t595 @t705) (=> @t669 (=> (_ @t706 @t302) (_ @t706 @t595)))))
% 0.46/0.87  (assume @p284 (forall (@list @t302 @t595 @t707) (=> @t669 (=> @t709 (_ @t708 @t595)))))
% 0.46/0.87  (assume @p285 (forall (@list @t707 @t710) (=> (= (_ tptp.sum_In2139678582um_b_c @t707) (_ tptp.sum_In2139678582um_b_c @t710)) (= @t707 @t710))))
% 0.46/0.87  (assume @p286 (forall (@list @t302 @t276) (_ (_ tptp.ord_less_eq_set_a @t597) @t302)))
% 0.46/0.87  (assume @p287 (forall (@list @t116 @t279) (_ (_ tptp.ord_le929608341um_b_c @t602) @t116)))
% 0.46/0.87  (assume @p288 (= tptp.ord_less_eq_set_a (lambda @t699 (_ (_ tptp.ord_less_eq_a_o (lambda @t66 @t704)) (lambda @t66 @t703)))))
% 0.46/0.87  (assume @p289 (forall (@list @t97 @t566 @t712 @t711 @t13) (=> (_ tptp.denota258389581_a_b_c @t97) (=> (_ tptp.denota258389581_a_b_c @t566) (=> (_ tptp.dfree_a_c @t712) (=> (_ tptp.dfree_a_c @t711) (=> (= (_ @t714 @t712) (_ @t713 @t711)) (= (_ (_ (_ @t98 @t712) @t101) @t100) (_ (_ (_ (_ tptp.denota229585092_a_b_c @t566) @t711) @t101) @t100)))))))))
% 0.46/0.87  (assume @p290 (forall (@list @t104 @t716 @t717 @t715 @t3) (=> @t719 (=> (_ tptp.denota1579475975_sc_sz @t716) (=> (_ tptp.dfree_sf_sz @t717) (=> (_ tptp.dfree_sf_sz @t715) (=> (= (_ @t718 @t717) (_ (_ tptp.denota1179238309_sc_sz @t716) @t715)) (= (_ (_ (_ @t105 @t717) @t108) @t107) (_ (_ (_ (_ tptp.denota1979904720_sc_sz @t716) @t715) @t108) @t107)))))))))
% 0.46/0.87  (assume @p291 (_ (_ (_ tptp.type_d1092523951t_unit tptp.freche1421597129_sc_sz) tptp.freche1784963216_sc_sz) @t663))
% 0.46/0.87  (assume @p292 (forall (@list @t723 @t721 @t707 @t722 @t720 @t302) (=> (= @t723 (_ @t721 @t707)) (=> (= @t722 (_ @t720 @t707)) (=> @t709 (_ (_ tptp.member1057565379_sc_sz (_ (_ tptp.produc789536734_sc_sz @t723) @t722)) (_ (_ (_ tptp.bNF_Gr1775200401_sc_sz @t302) @t721) @t720)))))))
% 0.46/0.87  (assume @p293 (forall (@list @t96 @t13 @t12 @t97 @t566) (=> @t102 (=> (_ @t15 (_ tptp.static_FVT_a_c @t96)) (=> (_ @t567 (_ tptp.collec2086029184um_b_c (lambda @t67 (exists @t66 (and @t65 (_ @t63 (_ tptp.static_SIGT_a_c @t96))))))) (= (_ (_ @t714 @t96) @t101) (_ (_ @t713 @t96) @t95)))))))
% 0.46/0.87  (assume @p294 (forall (@list @t725 @t724) (= (_ (_ tptp.ord_less_eq_a_o (lambda @t66 (_ @t63 @t725))) (lambda @t66 (_ @t63 @t724))) (_ (_ tptp.ord_less_eq_set_a @t725) @t724))))
% 0.46/0.87  (assume @p295 (forall (@list @t104 @t103 @t727) (=> @t719 (=> @t109 (_ (_ tptp.topolo1348430467z_real @t727) @t726)))))
% 0.46/0.87  (assume @p296 (forall (@list @t3 @t2 @t728 @t50 @t49) (=> (_ @t5 (_ tptp.static_FVT_sf_sz (_ (_ tptp.function_sf_sz @t728) @t50))) (_ @t5 (_ tptp.static_FVT_sf_sz @t51)))))
% 0.46/0.87  (assume @p297 (forall (@list @t730 @t729) (=> (forall @t410 (=> (_ @t731 @t730) (_ @t731 @t729))) (_ (_ tptp.ord_le1230423618_sc_sz @t730) @t729))))
% 0.46/0.87  (assume @p298 (forall (@list @t732) (_ (_ tptp.ord_le1772180283um_c_c (_ tptp.static_FVT_a_c @t732)) (_ tptp.static_FVDiff_a_c @t732))))
% 0.46/0.87  (assume @p299 (forall @t741 (= (= @t740 @t739) (= @t734 @t733))))
% 0.46/0.87  (assume @p300 (forall @t741 (= (_ (_ tptp.ord_le108471557c_sz_o @t740) @t739) (_ (_ tptp.ord_le1230423618_sc_sz @t734) @t733))))
% 0.46/0.87  (assume @p301 (forall @t742 (=> @t719 (=> @t109 (_ (_ tptp.topolo1348430467z_real tptp.top_to1873962757eal_sz) @t726)))))
% 0.46/0.87  (assume @p302 (forall (@list @t751 @t747 @t746 @t745 @t744) (=> (_ (_ tptp.topolo885751137z_real (_ tptp.collec1002602816eal_sz (lambda @t750 (and @t754 @t749)))) @t745) (=> (_ (_ tptp.topolo885751137z_real (_ tptp.collec1002602816eal_sz (lambda @t750 (and @t754 (_ (_ tptp.ord_less_eq_real @t746) @t748))))) @t744) (=> (_ (_ tptp.topolo1348430467z_real @t751) @t747) (=> (forall (@list @t753) (=> (_ (_ tptp.member1693951742eal_sz @t753) @t751) (=> (= (_ @t747 @t753) @t746) (= (_ @t745 @t753) (_ @t744 @t753))))) (_ @t752 (lambda @t750 (_ (_ (_ tptp.if_Bou1785791806z_real @t749) (_ @t745 @t743)) (_ @t744 @t743))))))))))
% 0.46/0.87  (assume @p303 (forall (@list @t707) (_ @t708 tptp.top_top_set_a)))
% 0.46/0.87  (assume @p304 (forall (@list @t438) (_ (_ tptp.member1693951742eal_sz @t438) tptp.top_to1873962757eal_sz)))
% 0.46/0.87  (assume @p305 (forall @t757 (=> @t756 @t755)))
% 0.46/0.87  (assume @p306 (forall @t757 (= @t756 @t755)))
% 0.46/0.87  (assume @p307 (forall @t757 (_ @t519 tptp.top_to1873962757eal_sz)))
% 0.46/0.87  (assume @p308 (forall @t286 (_ @t666 tptp.top_to1873962757eal_sz)))
% 0.46/0.87  (assume @p309 (forall (@list @t767 @t766 @t765 @t764 @t763 @t762 @t761 @t760 @t759 @t758 @t75) (=> @t768 @t76)))
% 0.46/0.87  (assume @p310 (= tptp.top_to524132421um_b_c (_ tptp.collec2086029184um_b_c (lambda @t308 true))))
% 0.46/0.87  (assume @p311 (= tptp.top_to1873962757eal_sz (_ tptp.collec1002602816eal_sz (lambda @t285 true))))
% 0.46/0.87  (assume @p312 (exists @t342 (_ @t618 tptp.top_top_set_a)))
% 0.46/0.87  (assume @p313 (exists @t314 (_ @t606 tptp.top_to1873962757eal_sz)))
% 0.46/0.87  (assume @p314 (forall @t304 (=> (forall @t342 @t670) (= tptp.top_top_set_a @t302))))
% 0.46/0.87  (assume @p315 (forall @t286 (=> (forall @t314 @t667) (= tptp.top_to1873962757eal_sz @t281))))
% 0.46/0.87  (assume @p316 (= tptp.top_to1787697847eal_sz (_ (_ tptp.produc1235791063eal_sz tptp.top_to1873962757eal_sz) tptp.top_to1873962757eal_sz)))
% 0.46/0.87  (assume @p317 (forall (@list @t767 @t766 @t765 @t764 @t763 @t762 @t761 @t760 @t759 @t758 @t769) (=> @t768 (= (_ tptp.p_sc_sf_sz @t769) (_ tptp.predic913887884_sf_sz @t769)))))
% 0.46/0.87  (assume @p318 (forall @t742 @t771))
% 0.46/0.87  (assume @p319 (= tptp.top_to524132421um_b_c (_ tptp.collec2086029184um_b_c tptp.top_to1201357528_b_c_o)))
% 0.46/0.87  (assume @p320 (= tptp.top_to1873962757eal_sz (_ tptp.collec1002602816eal_sz tptp.top_to646513176l_sz_o)))
% 0.46/0.87  (assume @p321 (forall @t516 (=> (_ (_ (_ tptp.denota1997846518gree_c @t176) @t515) tptp.top_to1660572043um_c_c) (and (= @t174 @t514) (= @t171 @t513)))))
% 0.46/0.87  (assume @p322 (forall (@list @t13 @t354) (=> (_ @t355 tptp.top_to1660572043um_c_c) (= @t13 @t354))))
% 0.46/0.87  (assume @p323 (forall @t772 (=> @t768 @t771)))
% 0.46/0.87  (assume @p324 (forall @t742 @t774))
% 0.46/0.87  (assume @p325 (forall (@list @t751 @t775) (_ @t752 (lambda @t285 @t775))))
% 0.46/0.87  (assume @p326 (forall (@list @t751 @t745 @t776) (=> @t777 (=> (_ (_ tptp.ord_le41263445eal_sz @t776) @t751) (_ (_ tptp.topolo885751137z_real @t776) @t745)))))
% 0.46/0.87  (assume @p327 (forall (@list @t751 @t745 @t744) (=> @t777 (=> (_ @t752 @t744) (_ (_ tptp.topolo1027477648z_real @t751) (lambda @t285 (_ (_ tptp.produc784663575z_real (_ @t745 @t282)) (_ @t744 @t282))))))))
% 0.46/0.87  (assume @p328 (forall @t772 (=> @t768 @t774)))
% 0.46/0.87  (assume @p329 (forall (@list @t779 @t778 @t438) @t782))
% 0.46/0.87  (assume @p330 (forall (@list @t767 @t766 @t765 @t764 @t763 @t762 @t761 @t760 @t759 @t758 @t779 @t778 @t438) (=> @t768 @t782)))
% 0.46/0.87  (assume @p331 (_ (_ (_ (_ tptp.quotie842200089_sc_sz @t781) tptp.freche1784963216_sc_sz) tptp.freche1421597129_sc_sz) tptp.freche58918398_sc_sz))
% 0.46/0.87  (assume @p332 (_ (_ (_ (_ tptp.quotie1467858509rm_a_c (_ tptp.bNF_eq_onp_trm_a_c tptp.dfree_a_c)) tptp.freche665377492rm_a_c) tptp.frechet_raw_term_a_c) tptp.frechet_cr_strm_a_c))
% 0.46/0.87  (assume @p333 (_ (_ (_ (_ tptp.quotie1549861309_sf_sz @t780) tptp.freche1046279700_sf_sz) tptp.freche782854530_sf_sz) tptp.freche1244000341_sf_sz))
% 0.46/0.87  (assume @p334 (forall (@list @t559) (_ (_ tptp.ord_le2003534918unit_o (_ tptp.bNF_eq1660582207t_unit @t559)) (lambda (@list @t784 @t783) (= @t784 @t783)))))
% 0.46/0.87  (assume @p335 (forall (@list @t94) (_ (_ tptp.ord_le8515534f_sz_o (_ tptp.bNF_eq_onp_trm_sf_sz @t94)) (lambda (@list @t786 @t785) (= @t786 @t785)))))
% 0.46/0.87  (assume @p336 (forall (@list @t787) (or (= @t787 true) (= @t787 false))))
% 0.46/0.87  (assume @p337 (forall @t788 (= (_ (_ (_ tptp.if_Bou1785791806z_real false) @t433) @t434) @t434)))
% 0.46/0.87  (assume @p338 (forall @t788 (= (_ (_ (_ tptp.if_Bou1785791806z_real true) @t433) @t434) @t433)))
% 0.46/0.87  (assume @p339 @t789)
% 0.46/0.87  (assume @p340 true)
% 0.46/0.87  (step @p341 (= tptp.freche58918398_sc_sz @t791) :rule refl :args (@t791))
% 0.46/0.87  (step @p342 (= tptp.freche1244000341_sf_sz @t793) :rule refl :args (@t793))
% 0.46/0.87  (step @p343 (= tptp.frechet_cr_strm_a_c @t795) :rule refl :args (@t795))
% 0.46/0.87  (step @p344 (= tptp.denota2112424896_a_b_c @t799) :rule refl :args (@t799))
% 0.46/0.87  (step @p345 (= tptp.denota453121236_sc_sz @t803) :rule refl :args (@t803))
% 0.46/0.87  (step @p346 (= tptp.ord_le850691415real_c @t806) :rule refl :args (@t806))
% 0.46/0.87  (step @p347 (= tptp.ord_le486764743_set_a @t809) :rule refl :args (@t809))
% 0.46/0.87  (step @p348 (= tptp.ord_le501349868_a_a_o @t812) :rule refl :args (@t812))
% 0.46/0.87  (step @p349 (= tptp.ord_le72828020_set_a @t815) :rule refl :args (@t815))
% 0.46/0.87  (step @p350 (= tptp.ord_le473656583eal_sz @t818) :rule refl :args (@t818))
% 0.46/0.87  (step @p351 (= tptp.ord_le1883211903_o_a_o @t821) :rule refl :args (@t821))
% 0.46/0.87  (step @p352 (= tptp.ord_le1884788375f_sz_o @t824) :rule refl :args (@t824))
% 0.46/0.87  (step @p353 (= tptp.ord_le1643089911_set_a @t827) :rule refl :args (@t827))
% 0.46/0.87  (step @p354 (= tptp.ord_le2132572860_o_a_o @t830) :rule refl :args (@t830))
% 0.46/0.87  (step @p355 (= tptp.ord_le472894788f_sz_o @t833) :rule refl :args (@t833))
% 0.46/0.87  (step @p356 (= tptp.f0_sf_sz @t835) :rule refl :args (@t835))
% 0.46/0.87  (step @p357 (= tptp.ord_less_eq_set_a @t838) :rule refl :args (@t838))
% 0.46/0.87  (step @p358 (= tptp.bNF_Gr1775200401_sc_sz @t843) :rule refl :args (@t843))
% 0.46/0.87  (step @p359 (= tptp.top_to1399053141c_sz_o @t844) :rule refl :args (@t844))
% 0.46/0.87  (step @p360 :rule refl :args ((tptp.denota1997846518gree_c @t13 @t12 @t11)))
% 0.46/0.87  (step @p361 :rule refl :args (@t845))
% 0.46/0.87  (step @p362 :rule refl :args (@t12))
% 0.46/0.87  (step @p363 :rule refl :args (@t13))
% 0.46/0.87  (step @p364 :rule cong :premises (@p363 @p362 @p361) :args (@t846))
% 0.46/0.87  (step @p365 :rule trans :premises (@p364 @p360))
% 0.46/0.87  (step @p366 :rule refl :args (@t15))
% 0.46/0.87  (step @p367 :rule ho_cong :premises (@p366 @p361))
% 0.46/0.87  (step @p368 :rule cong :premises (@p367 @p365) :args ((= (_ @t15 @t845) @t846)))
% 0.46/0.87  (step @p369 :rule symm :premises (@p368))
% 0.46/0.87  (step @p370 :rule refl :args (@t16))
% 0.46/0.87  (step @p371 :rule eq_resolve :premises (@p370 @p369))
% 0.46/0.87  (step @p372 :rule refl :args (@t11))
% 0.46/0.87  (step @p373 :rule cong :premises (@p372 @p361) :args ((= @t11 @t845)))
% 0.46/0.87  (step @p374 :rule symm :premises (@p373))
% 0.46/0.87  (step @p375 :rule eq_resolve :premises (@p372 @p374))
% 0.46/0.87  (step @p376 :rule ho_cong :premises (@p366 @p375))
% 0.46/0.87  (step @p377 :rule trans :premises (@p376 @p371))
% 0.46/0.87  (step @p378 :rule refl :args ((tptp.denota1997846518gree_c @t13 @t12 @t19)))
% 0.46/0.87  (step @p379 :rule refl :args ((tptp.static_FVDiff_a_c @t18)))
% 0.46/0.87  (step @p380 :rule refl :args (@t847))
% 0.46/0.87  (step @p381 :rule cong :premises (@p380) :args (@t848))
% 0.46/0.87  (step @p382 :rule trans :premises (@p381 @p379))
% 0.46/0.87  (step @p383 :rule cong :premises (@p363 @p362 @p382) :args (@t849))
% 0.46/0.87  (step @p384 :rule trans :premises (@p383 @p378))
% 0.46/0.87  (step @p385 :rule ho_cong :premises (@p366 @p382))
% 0.46/0.87  (step @p386 :rule cong :premises (@p385 @p384) :args ((= (_ @t15 @t848) @t849)))
% 0.46/0.87  (step @p387 :rule symm :premises (@p386))
% 0.46/0.87  (step @p388 :rule refl :args (@t20))
% 0.46/0.87  (step @p389 :rule eq_resolve :premises (@p388 @p387))
% 0.46/0.87  (step @p390 :rule refl :args (tptp.static_FVDiff_a_c))
% 0.46/0.87  (step @p391 :rule ho_cong :premises (@p390 @p380))
% 0.46/0.87  (step @p392 :rule cong :premises (@p391 @p382) :args ((= (_ tptp.static_FVDiff_a_c @t847) @t848)))
% 0.46/0.87  (step @p393 :rule symm :premises (@p392))
% 0.46/0.87  (step @p394 :rule refl :args (@t19))
% 0.46/0.87  (step @p395 :rule eq_resolve :premises (@p394 @p393))
% 0.46/0.87  (step @p396 :rule refl :args (@t18))
% 0.46/0.87  (step @p397 :rule cong :premises (@p396 @p380) :args ((= @t18 @t847)))
% 0.46/0.87  (step @p398 :rule symm :premises (@p397))
% 0.46/0.87  (step @p399 :rule eq_resolve :premises (@p396 @p398))
% 0.46/0.87  (step @p400 :rule ho_cong :premises (@p390 @p399))
% 0.46/0.87  (step @p401 :rule trans :premises (@p400 @p395))
% 0.46/0.87  (step @p402 :rule ho_cong :premises (@p366 @p401))
% 0.46/0.87  (step @p403 :rule trans :premises (@p402 @p389))
% 0.46/0.87  (step @p404 :rule cong :premises (@p403) :args (@t850))
% 0.46/0.87  (step @p405 :rule nary_cong :premises (@p404 @p377) :args (@t851))
% 0.46/0.87  (step @p406 :rule cong :premises (@p405) :args ((forall @t21 @t851)))
% 0.46/0.87  (step @p407 :rule bool-impl-elim :args (@t20 @t16))
% 0.46/0.87  (step @p408 :rule cong :premises (@p407) :args (@t22))
% 0.46/0.87  (step @p409 :rule trans :premises (@p408 @p406))
% 0.46/0.87  (step @p410 :rule eq_resolve :premises (@p2 @p409))
% 0.46/0.87  (step @p411 :rule refl :args ((tptp.denota1997846518gree_c tptp.nu tptp.nu2 @t24)))
% 0.46/0.87  (step @p412 :rule refl :args ((tptp.static_FVDiff_a_c @t23)))
% 0.46/0.87  (step @p413 :rule refl :args (@t852))
% 0.46/0.87  (step @p414 :rule cong :premises (@p413) :args (@t853))
% 0.46/0.87  (step @p415 :rule trans :premises (@p414 @p412))
% 0.46/0.87  (step @p416 :rule refl :args (tptp.nu2))
% 0.46/0.87  (step @p417 :rule refl :args (tptp.nu))
% 0.46/0.87  (step @p418 :rule cong :premises (@p417 @p416 @p415) :args (@t854))
% 0.46/0.87  (step @p419 :rule trans :premises (@p418 @p411))
% 0.46/0.87  (step @p420 :rule refl :args (@t25))
% 0.46/0.87  (step @p421 :rule ho_cong :premises (@p420 @p415))
% 0.46/0.87  (step @p422 :rule cong :premises (@p421 @p419) :args ((= (_ @t25 @t853) @t854)))
% 0.46/0.87  (step @p423 :rule symm :premises (@p422))
% 0.46/0.87  (step @p424 :rule refl :args (@t26))
% 0.46/0.87  (step @p425 :rule eq_resolve :premises (@p424 @p423))
% 0.46/0.87  (step @p426 :rule ho_cong :premises (@p390 @p413))
% 0.46/0.87  (step @p427 :rule cong :premises (@p426 @p415) :args ((= (_ tptp.static_FVDiff_a_c @t852) @t853)))
% 0.46/0.87  (step @p428 :rule symm :premises (@p427))
% 0.46/0.87  (step @p429 :rule refl :args (@t24))
% 0.46/0.87  (step @p430 :rule eq_resolve :premises (@p429 @p428))
% 0.46/0.87  (step @p431 :rule refl :args (@t23))
% 0.46/0.87  (step @p432 :rule cong :premises (@p431 @p413) :args ((= @t23 @t852)))
% 0.46/0.87  (step @p433 :rule symm :premises (@p432))
% 0.46/0.87  (step @p434 :rule eq_resolve :premises (@p431 @p433))
% 0.46/0.87  (step @p435 :rule refl :args (tptp.static_FVDiff_a_c))
% 0.46/0.87  (step @p436 :rule ho_cong :premises (@p435 @p434))
% 0.46/0.87  (step @p437 :rule trans :premises (@p436 @p430))
% 0.46/0.87  (step @p438 :rule refl :args (@t25))
% 0.46/0.87  (step @p439 :rule ho_cong :premises (@p438 @p437))
% 0.46/0.87  (step @p440 :rule trans :premises (@p439 @p425))
% 0.46/0.87  (step @p441 :rule eq_resolve :premises (@p3 @p440))
% 0.46/0.87  (step @p442 :rule refl :args ((tptp.denota1997846518gree_c tptp.nu tptp.nu2 @t71)))
% 0.46/0.87  (step @p443 :rule refl :args (@t855))
% 0.46/0.87  (step @p444 :rule cong :premises (@p417 @p416 @p443) :args (@t856))
% 0.46/0.87  (step @p445 :rule trans :premises (@p444 @p442))
% 0.46/0.87  (step @p446 :rule ho_cong :premises (@p420 @p443))
% 0.46/0.87  (step @p447 :rule cong :premises (@p446 @p445) :args ((= (_ @t25 @t855) @t856)))
% 0.46/0.87  (step @p448 :rule symm :premises (@p447))
% 0.46/0.87  (step @p449 :rule refl :args (@t72))
% 0.46/0.87  (step @p450 :rule eq_resolve :premises (@p449 @p448))
% 0.46/0.87  (step @p451 :rule refl :args (@t71))
% 0.46/0.87  (step @p452 :rule cong :premises (@p451 @p443) :args ((= @t71 @t855)))
% 0.46/0.87  (step @p453 :rule symm :premises (@p452))
% 0.46/0.87  (step @p454 :rule eq_resolve :premises (@p451 @p453))
% 0.46/0.87  (step @p455 :rule ho_cong :premises (@p438 @p454))
% 0.46/0.87  (step @p456 :rule trans :premises (@p455 @p450))
% 0.46/0.87  (step @p457 :rule cong :premises (@p456) :args (@t789))
% 0.46/0.87  (step @p458 :rule eq_resolve :premises (@p339 @p457))
% 0.46/0.87  (step @p459 :rule cnf_or_pos :args (@t858))
% 0.46/0.87  (step @p460 :rule reordering :premises (@p459) :args ((or @t856 @t857 @t859)))
% 0.46/0.87  (step @p461 :rule chain_m_resolution :premises (@p460 @p458 @p441) :args (@t859 @t860 (@list @t856 @t854)))
% 0.46/0.87  (assume-push @p468 @t861)
% 0.46/0.87  (step @p463 :rule instantiate :premises (@p410) :args ((@list tptp.nu tptp.nu2 tptp.t1 tptp.t2)))
% 0.46/0.87  (step-pop @p469 :rule scope :premises (@p463))
% 0.46/0.87  (step @p464 :rule process_scope :premises (@p469) :args (@t858))
% 0.46/0.87  (step @p466 :rule implies_elim :premises (@p464))
% 0.46/0.87  (step @p467 false :rule chain_m_resolution :premises (@p466 @p461 @p410) :args (false @t860 (@list @t858 @t861)))
% 0.46/0.87  )
% 0.46/0.87  % SZS output end Proof
% 0.46/0.87  % cvc5 exiting
%------------------------------------------------------------------------------