cvc5---1.3.4.THM-Prf.s

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

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

% Result   : Theorem 151.11s 151.91s
% Output   : Proof 151.11s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11  % Problem  : ITP140^1 : TPTP v9.2.1. Released v7.5.0.
% 0.00/0.12  % Command  : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.15/0.33  % Computer : n026.cluster.edu
% 0.15/0.33  % Model    : x86_64 x86_64
% 0.15/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33  % Memory   : 8042.1875MB
% 0.15/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33  % CPULimit : 300
% 0.15/0.33  % WCLimit  : 300
% 0.15/0.33  % DateTime : Tue Jun  2 04:15:55 EDT 2026
% 0.15/0.33  % CPUTime  : 
% 0.40/0.61  %----Proving TH0
% 151.11/151.91  --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 90s...
% 151.11/151.91  --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --mbqi-enum-choice-grammar-all --no-cegqi --no-sygus-inst at 30s...
% 151.11/151.91  --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-mbqi-nested-check --no-cegqi --no-sygus-inst at 30s...
% 151.11/151.91  --- Run --ho-elim --full-saturate-quant at 18s...
% 151.11/151.91  % SZS status Theorem
% 151.11/151.91  % SZS output start Proof
% 151.11/151.91  (
% 151.11/151.91  (declare-sort tptp.set_Pr560526279lle_tv 0)
% 151.11/151.91  (declare-sort tptp.set_Pr2120184979lle_fm 0)
% 151.11/151.91  (declare-sort tptp.set_Pa1764573435lle_tv 0)
% 151.11/151.91  (declare-sort tptp.set_nat 0)
% 151.11/151.91  (declare-sort tptp.produc1647334210lle_tv 0)
% 151.11/151.91  (declare-sort tptp.set_Pr2014382200lle_tv 0)
% 151.11/151.91  (declare-sort tptp.nat 0)
% 151.11/151.91  (declare-sort tptp.set_Pr698334450lle_tv 0)
% 151.11/151.91  (declare-sort tptp.list_char 0)
% 151.11/151.91  (declare-sort tptp.paraco1605129243lle_tv 0)
% 151.11/151.91  (declare-sort tptp.set_Pr1019238018lle_fm 0)
% 151.11/151.91  (declare-sort tptp.set_Pr1475944804lle_fm 0)
% 151.11/151.91  (declare-sort tptp.produc931990033lle_tv 0)
% 151.11/151.91  (declare-sort tptp.produc696645085lle_fm 0)
% 151.11/151.91  (declare-sort tptp.produc1720769084lle_tv 0)
% 151.11/151.91  (declare-sort tptp.set_Pr1357842111at_nat 0)
% 151.11/151.91  (declare-sort tptp.paraco1604210848lle_fm 0)
% 151.11/151.91  (declare-sort tptp.produc1281043295at_nat 0)
% 151.11/151.91  (declare-sort tptp.produc1250255278lle_fm 0)
% 151.11/151.91  (declare-sort tptp.set_Pr2061825550lle_tv 0)
% 151.11/151.91  (declare-sort tptp.produc1852595672lle_tv 0)
% 151.11/151.91  (declare-sort tptp.produc450659916lle_fm 0)
% 151.11/151.91  (declare-sort tptp.produc270694976lle_tv 0)
% 151.11/151.91  (declare-sort tptp.produc194167194tv_nat 0)
% 151.11/151.91  (declare-sort tptp.product_prod_nat_nat 0)
% 151.11/151.91  (declare-sort tptp.set_Pr1490359111at_nat 0)
% 151.11/151.91  (declare-sort tptp.set_Pr1986765409at_nat 0)
% 151.11/151.91  (declare-sort tptp.set_Pr13445366lle_tv 0)
% 151.11/151.91  (declare-sort tptp.set_Pr1725653840tv_nat 0)
% 151.11/151.91  (declare-sort tptp.set_Pr2012908090lle_tv 0)
% 151.11/151.91  (declare-sort tptp.set_Pr1943077434tv_nat 0)
% 151.11/151.91  (declare-sort tptp.produc596913417at_nat 0)
% 151.11/151.91  (declare-sort tptp.produc1443694919lle_tv 0)
% 151.11/151.91  (declare-sort tptp.set_Pr1723822845lle_tv 0)
% 151.11/151.91  (declare-sort tptp.set_Pr840833727at_nat 0)
% 151.11/151.91  (declare-sort tptp.set_Pr292927124lle_tv 0)
% 151.11/151.91  (declare-const tptp.paraco1147068288nge_tv (-> (-> tptp.nat tptp.nat) tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv))
% 151.11/151.91  (declare-const tptp.paraco1344940915le_Det (-> Bool tptp.paraco1605129243lle_tv))
% 151.11/151.91  (declare-const tptp.paraco1325918602e_eval (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.paraco1604210848lle_fm tptp.paraco1605129243lle_tv))
% 151.11/151.91  (declare-const tptp.top_top_o Bool)
% 151.11/151.91  (declare-const tptp.member1531318361lle_tv (-> tptp.produc1647334210lle_tv tptp.set_Pr2014382200lle_tv Bool))
% 151.11/151.91  (declare-const tptp.member737151281tv_nat (-> tptp.produc194167194tv_nat tptp.set_Pr1725653840tv_nat Bool))
% 151.11/151.91  (declare-const tptp.member813679063lle_tv (-> tptp.produc270694976lle_tv tptp.set_Pr13445366lle_tv Bool))
% 151.11/151.91  (declare-const tptp.member701585322at_nat (-> tptp.product_prod_nat_nat tptp.set_Pr1986765409at_nat Bool))
% 151.11/151.91  (declare-const tptp.member_nat (-> tptp.nat tptp.set_nat Bool))
% 151.11/151.91  (declare-const tptp.member266900804lle_tv (-> tptp.paraco1605129243lle_tv tptp.set_Pa1764573435lle_tv Bool))
% 151.11/151.91  (declare-const tptp.if_Par1134130401lle_tv (-> Bool tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv))
% 151.11/151.91  (declare-const tptp.produc262413013lle_tv (-> tptp.produc1443694919lle_tv tptp.paraco1604210848lle_fm))
% 151.11/151.91  (declare-const tptp.produc381314067lle_tv (-> tptp.produc1443694919lle_tv tptp.list_char tptp.paraco1605129243lle_tv))
% 151.11/151.91  (declare-const tptp.produc1710735575lle_fm (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.paraco1604210848lle_fm tptp.produc696645085lle_fm))
% 151.11/151.91  (declare-const tptp.produc1589291287at_nat (-> tptp.produc596913417at_nat tptp.paraco1605129243lle_tv))
% 151.11/151.91  (declare-const tptp.produc500618325at_nat (-> tptp.produc596913417at_nat tptp.nat tptp.nat))
% 151.11/151.91  (declare-const tptp.produc1680557635lle_tv (-> (-> tptp.nat tptp.nat) tptp.paraco1605129243lle_tv tptp.produc931990033lle_tv))
% 151.11/151.91  (declare-const tptp.ord_le1784136743lle_tv (-> tptp.set_Pr560526279lle_tv tptp.set_Pr560526279lle_tv Bool))
% 151.11/151.91  (declare-const tptp.ord_le1007985907lle_fm (-> tptp.set_Pr2120184979lle_fm tptp.set_Pr2120184979lle_fm Bool))
% 151.11/151.91  (declare-const tptp.order_769474267at_nat (-> (-> tptp.nat tptp.nat) Bool))
% 151.11/151.91  (declare-const tptp.ord_le241064091lle_tv (-> tptp.set_Pa1764573435lle_tv tptp.set_Pa1764573435lle_tv Bool))
% 151.11/151.91  (declare-const tptp.ord_less_eq_set_nat (-> tptp.set_nat tptp.set_nat Bool))
% 151.11/151.91  (declare-const tptp.wf_Par1378404612lle_tv (-> tptp.set_Pr2014382200lle_tv Bool))
% 151.11/151.91  (declare-const tptp.image_1221801032lle_tv (-> (-> tptp.produc1647334210lle_tv tptp.produc1647334210lle_tv) tptp.set_Pr2014382200lle_tv tptp.set_Pr2014382200lle_tv))
% 151.11/151.91  (declare-const tptp.wf_nat (-> tptp.set_Pr1986765409at_nat Bool))
% 151.11/151.91  (declare-const tptp.same_f1581085506lle_fm (-> (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) Bool) (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.set_Pr1019238018lle_fm) tptp.set_Pr1475944804lle_fm))
% 151.11/151.91  (declare-const tptp.produc1636169559lle_tv (-> tptp.produc931990033lle_tv tptp.nat tptp.nat))
% 151.11/151.91  (declare-const tptp.produc547496597lle_tv (-> tptp.produc931990033lle_tv tptp.paraco1605129243lle_tv))
% 151.11/151.91  (declare-const tptp.produc29804011lle_fm (-> tptp.produc696645085lle_fm tptp.list_char tptp.paraco1605129243lle_tv))
% 151.11/151.91  (declare-const tptp.produc148705065lle_fm (-> tptp.produc696645085lle_fm tptp.paraco1604210848lle_fm))
% 151.11/151.91  (declare-const tptp.produc2057188974lle_tv (-> tptp.produc931990033lle_tv tptp.produc931990033lle_tv tptp.produc1720769084lle_tv))
% 151.11/151.91  (declare-const tptp.lex_pr1093414955lle_tv (-> tptp.set_Pr1357842111at_nat tptp.set_Pr2014382200lle_tv tptp.set_Pr698334450lle_tv))
% 151.11/151.91  (declare-const tptp.produc780837143at_nat (-> (-> tptp.nat tptp.nat) (-> tptp.nat tptp.nat) tptp.produc1281043295at_nat))
% 151.11/151.91  (declare-const tptp.produc2058540732lle_tv (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv tptp.produc1647334210lle_tv))
% 151.11/151.91  (declare-const tptp.member1592865093lle_fm (-> tptp.produc1250255278lle_fm tptp.set_Pr1475944804lle_fm Bool))
% 151.11/151.91  (declare-const tptp.produc2101297531lle_tv (-> (-> tptp.nat tptp.nat) (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.produc270694976lle_tv tptp.produc270694976lle_tv))
% 151.11/151.91  (declare-const tptp.paraco1480028776le_Pro (-> tptp.list_char tptp.paraco1604210848lle_fm))
% 151.11/151.91  (declare-const tptp.produc1345917071lle_tv (-> (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.produc1647334210lle_tv tptp.produc1647334210lle_tv))
% 151.11/151.91  (declare-const tptp.lex_pr567812260lle_tv (-> tptp.set_Pr2014382200lle_tv tptp.set_Pr2014382200lle_tv tptp.set_Pr2012908090lle_tv))
% 151.11/151.91  (declare-const tptp.produc42536895at_nat (-> (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) (-> tptp.nat tptp.nat) tptp.produc194167194tv_nat tptp.produc194167194tv_nat))
% 151.11/151.91  (declare-const tptp.lex_pr1785529980tv_nat (-> tptp.set_Pr2014382200lle_tv tptp.set_Pr1986765409at_nat tptp.set_Pr1943077434tv_nat))
% 151.11/151.91  (declare-const tptp.collec848462447tv_nat (-> (-> tptp.produc194167194tv_nat Bool) tptp.set_Pr1725653840tv_nat))
% 151.11/151.91  (declare-const tptp.top_to900819589_nat_o (-> tptp.produc194167194tv_nat Bool))
% 151.11/151.91  (declare-const tptp.produc1250721397at_nat (-> (-> tptp.nat tptp.paraco1605129243lle_tv) (-> tptp.nat tptp.nat) tptp.product_prod_nat_nat tptp.produc194167194tv_nat))
% 151.11/151.91  (declare-const tptp.top_to1871154984lle_tv tptp.set_Pr2014382200lle_tv)
% 151.11/151.91  (declare-const tptp.inv_image_nat_nat (-> tptp.set_Pr1986765409at_nat (-> tptp.nat tptp.nat) tptp.set_Pr1986765409at_nat))
% 151.11/151.91  (declare-const tptp.top_to1057771083lle_tv tptp.set_Pa1764573435lle_tv)
% 151.11/151.91  (declare-const tptp.produc1000205111lle_fm (-> tptp.produc696645085lle_fm tptp.produc1443694919lle_tv))
% 151.11/151.91  (declare-const tptp.member146333935lle_tv (-> tptp.produc1852595672lle_tv tptp.set_Pr2061825550lle_tv Bool))
% 151.11/151.91  (declare-const tptp.top_to1555900337at_nat tptp.set_Pr1986765409at_nat)
% 151.11/151.91  (declare-const tptp.produc109093078at_nat (-> (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.produc931990033lle_tv tptp.produc931990033lle_tv))
% 151.11/151.91  (declare-const tptp.image_1585092542lle_fm (-> (-> tptp.produc931990033lle_tv tptp.produc696645085lle_fm) tptp.set_Pr560526279lle_tv tptp.set_Pr2120184979lle_fm))
% 151.11/151.91  (declare-const tptp.top_to1411004326lle_tv tptp.set_Pr13445366lle_tv)
% 151.11/151.91  (declare-const tptp.top_to1541413903at_nat tptp.set_Pr1357842111at_nat)
% 151.11/151.91  (declare-const tptp.paraco445776468le_Neg (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm))
% 151.11/151.91  (declare-const tptp.produc939316703lle_tv (-> (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat) tptp.produc931990033lle_tv tptp.produc931990033lle_tv))
% 151.11/151.91  (declare-const tptp.top_to775056195lle_fm tptp.set_Pr2120184979lle_fm)
% 151.11/151.91  (declare-const tptp.produc225513635lle_tv (-> tptp.produc931990033lle_tv tptp.produc596913417at_nat))
% 151.11/151.91  (declare-const tptp.collec7649004at_nat (-> (-> tptp.product_prod_nat_nat Bool) tptp.set_Pr1986765409at_nat))
% 151.11/151.91  (declare-const tptp.f (-> tptp.nat tptp.nat))
% 151.11/151.91  (declare-const tptp.collec1102043437lle_tv (-> (-> tptp.produc1852595672lle_tv Bool) tptp.set_Pr2061825550lle_tv))
% 151.11/151.91  (declare-const tptp.paraco55203475lid_in (-> tptp.set_nat tptp.paraco1604210848lle_fm Bool))
% 151.11/151.91  (declare-const tptp.p1 tptp.paraco1604210848lle_fm)
% 151.11/151.91  (declare-const tptp.collec835549234lle_fm (-> (-> tptp.produc696645085lle_fm Bool) tptp.set_Pr2120184979lle_fm))
% 151.11/151.91  (declare-const tptp.paraco1389086619le_Eql (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm))
% 151.11/151.91  (declare-const tptp.member74361182lle_tv (-> tptp.produc1443694919lle_tv tptp.set_Pr1723822845lle_tv Bool))
% 151.11/151.91  (declare-const tptp.total_1775715973at_nat (-> tptp.set_Pr1986765409at_nat tptp.set_Pr1490359111at_nat Bool))
% 151.11/151.91  (declare-const tptp.collec791369802at_nat (-> (-> tptp.produc1281043295at_nat Bool) tptp.set_Pr1357842111at_nat))
% 151.11/151.91  (declare-const tptp.produc1807466521lle_tv (-> (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm) tptp.produc696645085lle_fm tptp.produc696645085lle_fm))
% 151.11/151.91  (declare-const tptp.top_to449985143lle_tv tptp.set_Pr560526279lle_tv)
% 151.11/151.91  (declare-const tptp.top_to1889334367e_tv_o (-> tptp.produc270694976lle_tv Bool))
% 151.11/151.91  (declare-const tptp.p2 tptp.paraco1604210848lle_fm)
% 151.11/151.91  (declare-const tptp.member1339857875lle_tv (-> tptp.produc1720769084lle_tv tptp.set_Pr698334450lle_tv Bool))
% 151.11/151.91  (declare-const tptp.paraco793048302_Indet (-> tptp.nat tptp.paraco1605129243lle_tv))
% 151.11/151.91  (declare-const tptp.top_to632227436_nat_o (-> tptp.product_prod_nat_nat Bool))
% 151.11/151.91  (declare-const tptp.paraco2051596139lle_tv (-> (-> Bool tptp.paraco1605129243lle_tv) (-> tptp.nat tptp.paraco1605129243lle_tv) tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv))
% 151.11/151.91  (declare-const tptp.i (-> tptp.list_char tptp.paraco1605129243lle_tv))
% 151.11/151.91  (declare-const tptp.collec924990229lle_tv (-> (-> tptp.produc270694976lle_tv Bool) tptp.set_Pr13445366lle_tv))
% 151.11/151.91  (declare-const tptp.produc1942165868lle_fm (-> (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.list_char tptp.paraco1605129243lle_tv) tptp.produc696645085lle_fm tptp.produc696645085lle_fm))
% 151.11/151.91  (declare-const tptp.same_f1138187694lle_tv (-> (-> (-> tptp.nat tptp.nat) Bool) (-> (-> tptp.nat tptp.nat) tptp.set_Pr2014382200lle_tv) tptp.set_Pr698334450lle_tv))
% 151.11/151.91  (declare-const tptp.top_top_set_nat tptp.set_nat)
% 151.11/151.91  (declare-const tptp.image_988201162lle_tv (-> (-> tptp.produc270694976lle_tv tptp.produc1647334210lle_tv) tptp.set_Pr13445366lle_tv tptp.set_Pr2014382200lle_tv))
% 151.11/151.91  (declare-const tptp.produc313957681lle_tv (-> (-> tptp.nat tptp.nat) (-> tptp.nat tptp.paraco1605129243lle_tv) tptp.product_prod_nat_nat tptp.produc270694976lle_tv))
% 151.11/151.91  (declare-const tptp.image_53754658tv_nat (-> (-> tptp.produc270694976lle_tv tptp.produc194167194tv_nat) tptp.set_Pr13445366lle_tv tptp.set_Pr1725653840tv_nat))
% 151.11/151.91  (declare-const tptp.produc505105722at_nat (-> (-> tptp.nat tptp.nat) (-> tptp.nat tptp.nat) tptp.product_prod_nat_nat tptp.product_prod_nat_nat))
% 151.11/151.91  (declare-const tptp.top_to975729152tv_nat tptp.set_Pr1725653840tv_nat)
% 151.11/151.91  (declare-const tptp.member1474794996lle_fm (-> tptp.produc696645085lle_fm tptp.set_Pr2120184979lle_fm Bool))
% 151.11/151.91  (declare-const tptp.inv_im1292588663lle_tv (-> tptp.set_Pr1986765409at_nat (-> tptp.paraco1605129243lle_tv tptp.nat) tptp.set_Pr2014382200lle_tv))
% 151.11/151.91  (declare-const tptp.paraco367965286_Truth tptp.paraco1604210848lle_fm)
% 151.11/151.91  (declare-const tptp.total_92239038lle_tv (-> tptp.set_Pr2014382200lle_tv tptp.set_Pr2012908090lle_tv Bool))
% 151.11/151.91  (declare-const tptp.top_to138697918lle_tv tptp.set_Pr2061825550lle_tv)
% 151.11/151.91  (declare-const tptp.collec1624074086lle_tv (-> (-> tptp.produc931990033lle_tv Bool) tptp.set_Pr560526279lle_tv))
% 151.11/151.91  (declare-const tptp.member1569366824lle_tv (-> tptp.produc931990033lle_tv tptp.set_Pr560526279lle_tv Bool))
% 151.11/151.91  (declare-const tptp.inv_im719552961lle_tv (-> tptp.set_Pr2014382200lle_tv (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.set_Pr2014382200lle_tv))
% 151.11/151.91  (declare-const tptp.member112824072at_nat (-> tptp.produc1281043295at_nat tptp.set_Pr1357842111at_nat Bool))
% 151.11/151.91  (declare-const tptp.inv_im516950809tv_nat (-> tptp.set_Pr2014382200lle_tv (-> tptp.nat tptp.paraco1605129243lle_tv) tptp.set_Pr1986765409at_nat))
% 151.11/151.91  (declare-const tptp.collec1111687558lle_tv (-> (-> tptp.paraco1605129243lle_tv Bool) tptp.set_Pa1764573435lle_tv))
% 151.11/151.91  (declare-const tptp.collect_nat (-> (-> tptp.nat Bool) tptp.set_nat))
% 151.11/151.91  (declare-const tptp.produc275353523e_fm_o (-> (-> tptp.produc696645085lle_fm Bool) (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.paraco1604210848lle_fm Bool))
% 151.11/151.91  (declare-const tptp.image_1724396928at_nat (-> (-> tptp.produc931990033lle_tv tptp.produc596913417at_nat) tptp.set_Pr560526279lle_tv tptp.set_Pr840833727at_nat))
% 151.11/151.91  (declare-const tptp.produc752649287e_tv_o (-> (-> tptp.produc931990033lle_tv Bool) (-> tptp.nat tptp.nat) tptp.paraco1605129243lle_tv Bool))
% 151.11/151.91  (declare-const tptp.produc1900967599lle_fm (-> (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.list_char tptp.paraco1605129243lle_tv) (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm) tptp.produc696645085lle_fm tptp.produc696645085lle_fm))
% 151.11/151.91  (declare-const tptp.image_1674248956lle_tv (-> (-> tptp.product_prod_nat_nat tptp.produc270694976lle_tv) tptp.set_Pr1986765409at_nat tptp.set_Pr13445366lle_tv))
% 151.11/151.91  (declare-const tptp.produc1566550641lle_tv (-> (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.nat tptp.nat) (-> tptp.paraco1604210848lle_fm tptp.paraco1605129243lle_tv) tptp.produc696645085lle_fm tptp.produc931990033lle_tv))
% 151.11/151.91  (declare-const tptp.produc951033137lle_fm (-> (-> (-> tptp.nat tptp.nat) tptp.list_char tptp.paraco1605129243lle_tv) (-> tptp.paraco1605129243lle_tv tptp.paraco1604210848lle_fm) tptp.produc931990033lle_tv tptp.produc696645085lle_fm))
% 151.11/151.91  (declare-const tptp.image_149830562lle_tv (-> (-> tptp.produc270694976lle_tv tptp.produc270694976lle_tv) tptp.set_Pr13445366lle_tv tptp.set_Pr13445366lle_tv))
% 151.11/151.91  (declare-const tptp.inj_on1179712058tv_nat (-> (-> tptp.paraco1605129243lle_tv tptp.nat) tptp.set_Pa1764573435lle_tv Bool))
% 151.11/151.91  (declare-const tptp.produc532909085lle_tv (-> (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat) (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.produc931990033lle_tv tptp.produc931990033lle_tv))
% 151.11/151.91  (declare-const tptp.the_inv_into_nat_nat (-> tptp.set_nat (-> tptp.nat tptp.nat) tptp.nat tptp.nat))
% 151.11/151.91  (declare-const tptp.the_in452116896lle_tv (-> tptp.set_Pa1764573435lle_tv (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv))
% 151.11/151.91  (declare-const tptp.image_1200372424lle_tv (-> (-> tptp.produc194167194tv_nat tptp.produc270694976lle_tv) tptp.set_Pr1725653840tv_nat tptp.set_Pr13445366lle_tv))
% 151.11/151.91  (declare-const tptp.paraco1632582009tv_rel (-> tptp.produc931990033lle_tv tptp.produc931990033lle_tv Bool))
% 151.11/151.91  (declare-const tptp.accp_P2085826120lle_tv (-> (-> tptp.produc931990033lle_tv tptp.produc931990033lle_tv Bool) tptp.produc931990033lle_tv Bool))
% 151.11/151.91  (declare-const tptp.total_on_nat (-> tptp.set_nat tptp.set_Pr1986765409at_nat Bool))
% 151.11/151.91  (declare-const tptp.total_1781621663lle_tv (-> tptp.set_Pa1764573435lle_tv tptp.set_Pr2014382200lle_tv Bool))
% 151.11/151.91  (declare-const tptp.image_nat_nat (-> (-> tptp.nat tptp.nat) tptp.set_nat tptp.set_nat))
% 151.11/151.91  (declare-const tptp.image_335818702lle_tv (-> (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.set_Pa1764573435lle_tv tptp.set_Pa1764573435lle_tv))
% 151.11/151.91  (declare-const tptp.image_807538418lle_fm (-> (-> tptp.produc696645085lle_fm tptp.produc696645085lle_fm) tptp.set_Pr2120184979lle_fm tptp.set_Pr2120184979lle_fm))
% 151.11/151.91  (declare-const tptp.image_1154804148lle_tv (-> (-> tptp.produc696645085lle_fm tptp.produc931990033lle_tv) tptp.set_Pr2120184979lle_fm tptp.set_Pr560526279lle_tv))
% 151.11/151.91  (declare-const tptp.image_1751508608lle_tv (-> (-> tptp.produc931990033lle_tv tptp.produc931990033lle_tv) tptp.set_Pr560526279lle_tv tptp.set_Pr560526279lle_tv))
% 151.11/151.91  (declare-const tptp.produc1943344577lle_tv (-> tptp.paraco1604210848lle_fm (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.produc1443694919lle_tv))
% 151.11/151.91  (declare-const tptp.produc1633679363at_nat (-> tptp.paraco1605129243lle_tv (-> tptp.nat tptp.nat) tptp.produc596913417at_nat))
% 151.11/151.91  (declare-const tptp.image_924970994lle_tv (-> (-> tptp.produc696645085lle_fm tptp.produc1443694919lle_tv) tptp.set_Pr2120184979lle_fm tptp.set_Pr1723822845lle_tv))
% 151.11/151.91  (declare-const tptp.paraco1745535428le_Eql (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm))
% 151.11/151.91  (declare-const tptp.member1234290208at_nat (-> tptp.produc596913417at_nat tptp.set_Pr840833727at_nat Bool))
% 151.11/151.91  (declare-const tptp.total_440843542tv_nat (-> tptp.set_Pr1725653840tv_nat tptp.set_Pr1943077434tv_nat Bool))
% 151.11/151.91  (declare-const tptp.image_326034184lle_fm (-> (-> tptp.produc1443694919lle_tv tptp.produc696645085lle_fm) tptp.set_Pr1723822845lle_tv tptp.set_Pr2120184979lle_fm))
% 151.11/151.91  (declare-const tptp.image_769496456lle_tv (-> (-> tptp.produc596913417at_nat tptp.produc931990033lle_tv) tptp.set_Pr840833727at_nat tptp.set_Pr560526279lle_tv))
% 151.11/151.91  (declare-const tptp.image_815163717at_nat (-> (-> tptp.product_prod_nat_nat tptp.product_prod_nat_nat) tptp.set_Pr1986765409at_nat tptp.set_Pr1986765409at_nat))
% 151.11/151.91  (declare-const tptp.image_1151963140lle_tv (-> (-> tptp.nat tptp.paraco1605129243lle_tv) tptp.set_nat tptp.set_Pa1764573435lle_tv))
% 151.11/151.91  (declare-const tptp.produc1685803475tv_nat (-> (-> tptp.nat tptp.nat) (-> tptp.paraco1605129243lle_tv tptp.nat) tptp.produc270694976lle_tv tptp.product_prod_nat_nat))
% 151.11/151.91  (declare-const tptp.image_1787705850at_nat (-> (-> tptp.produc270694976lle_tv tptp.product_prod_nat_nat) tptp.set_Pr13445366lle_tv tptp.set_Pr1986765409at_nat))
% 151.11/151.91  (declare-const tptp.image_376325286tv_nat (-> (-> tptp.paraco1605129243lle_tv tptp.nat) tptp.set_Pa1764573435lle_tv tptp.set_nat))
% 151.11/151.91  (declare-const tptp.image_1597721174tv_nat (-> (-> tptp.product_prod_nat_nat tptp.produc194167194tv_nat) tptp.set_Pr1986765409at_nat tptp.set_Pr1725653840tv_nat))
% 151.11/151.91  (declare-const tptp.produc210389789lle_tv (-> (-> tptp.nat tptp.paraco1605129243lle_tv) (-> tptp.nat tptp.paraco1605129243lle_tv) tptp.product_prod_nat_nat tptp.produc1647334210lle_tv))
% 151.11/151.91  (declare-const tptp.image_1507992062lle_tv (-> (-> tptp.product_prod_nat_nat tptp.produc1647334210lle_tv) tptp.set_Pr1986765409at_nat tptp.set_Pr2014382200lle_tv))
% 151.11/151.91  (declare-const tptp.produc189459613tv_nat (-> (-> tptp.nat tptp.paraco1605129243lle_tv) (-> tptp.paraco1605129243lle_tv tptp.nat) tptp.produc270694976lle_tv tptp.produc194167194tv_nat))
% 151.11/151.91  (declare-const tptp.image_1805124128at_nat (-> (-> tptp.produc194167194tv_nat tptp.product_prod_nat_nat) tptp.set_Pr1725653840tv_nat tptp.set_Pr1986765409at_nat))
% 151.11/151.91  (declare-const tptp.produc1975500101lle_tv (-> (-> tptp.nat tptp.paraco1605129243lle_tv) (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.produc270694976lle_tv tptp.produc1647334210lle_tv))
% 151.11/151.91  (declare-const tptp.produc386540311at_nat (-> (-> tptp.paraco1605129243lle_tv tptp.nat) (-> tptp.nat tptp.nat) tptp.produc194167194tv_nat tptp.product_prod_nat_nat))
% 151.11/151.91  (declare-const tptp.produc72207551lle_tv (-> (-> tptp.paraco1605129243lle_tv tptp.nat) (-> tptp.nat tptp.paraco1605129243lle_tv) tptp.produc194167194tv_nat tptp.produc270694976lle_tv))
% 151.11/151.91  (declare-const tptp.lex_prod_nat_nat (-> tptp.set_Pr1986765409at_nat tptp.set_Pr1986765409at_nat tptp.set_Pr1490359111at_nat))
% 151.11/151.91  (declare-const tptp.lex_pr413684186lle_tv (-> tptp.set_Pr1986765409at_nat tptp.set_Pr2014382200lle_tv tptp.set_Pr292927124lle_tv))
% 151.11/151.91  (declare-const tptp.total_517371324lle_tv (-> tptp.set_Pr13445366lle_tv tptp.set_Pr292927124lle_tv Bool))
% 151.11/151.91  (declare-const tptp.paraco69239110le_Con (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm))
% 151.11/151.91  (declare-const tptp.member334644067lle_fm (-> tptp.produc450659916lle_fm tptp.set_Pr1019238018lle_fm Bool))
% 151.11/151.91  (declare-const tptp.produc1126104134lle_fm (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm tptp.produc450659916lle_fm))
% 151.11/151.91  (declare-const tptp.produc1297923922lle_tv (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.produc1852595672lle_tv))
% 151.11/151.91  (declare-const tptp.lex_pr2001015487lle_fm (-> tptp.set_Pr2061825550lle_tv tptp.set_Pr1019238018lle_fm tptp.set_Pr1475944804lle_fm))
% 151.11/151.91  (declare-const tptp.produc407632608lle_fm (-> tptp.produc696645085lle_fm tptp.produc696645085lle_fm tptp.produc1250255278lle_fm))
% 151.11/151.91  (define tptp.paraco761681009ge_int () (let ((_let_1 (@var "S" tptp.list_char))) (let ((_let_2 (@var "I2" (-> tptp.list_char tptp.paraco1605129243lle_tv)))) (let ((_let_3 (@var "F2" (-> tptp.nat tptp.nat)))) (lambda (@list _let_3 _let_2 _let_1) (_ (_ tptp.paraco1147068288nge_tv _let_3) (_ _let_2 _let_1)))))))
% 151.11/151.91  (define tptp.paraco327635598_valid () (let ((_let_1 (@var "P2" tptp.paraco1604210848lle_fm))) (let ((_let_2 (@var "I2" (-> tptp.list_char tptp.paraco1605129243lle_tv)))) (lambda (@list _let_1) (forall (@list _let_2) (= (_ (_ tptp.paraco1325918602e_eval _let_2) _let_1) (_ tptp.paraco1344940915le_Det true)))))))
% 151.11/151.91  (define tptp.top_to1299250770e_tv_o () (lambda (@list (@var "X4" tptp.paraco1605129243lle_tv)) tptp.top_top_o))
% 151.11/151.91  (define tptp.top_top_nat_o () (lambda (@list (@var "X4" tptp.nat)) tptp.top_top_o))
% 151.11/151.91  (define tptp.inj_on2112487900lle_tv () (let ((_let_1 (@var "Y4" tptp.produc1647334210lle_tv))) (let ((_let_2 (@var "X4" tptp.produc1647334210lle_tv))) (let ((_let_3 (@var "F2" (-> tptp.produc1647334210lle_tv tptp.produc1647334210lle_tv)))) (let ((_let_4 (@var "A3" tptp.set_Pr2014382200lle_tv))) (lambda (@list _let_3 _let_4) (forall (@list _let_2) (=> (_ (_ tptp.member1531318361lle_tv _let_2) _let_4) (forall (@list _let_1) (=> (_ (_ tptp.member1531318361lle_tv _let_1) _let_4) (=> (= (_ _let_3 _let_2) (_ _let_3 _let_1)) (= _let_2 _let_1))))))))))))
% 151.11/151.91  (define tptp.inj_on552895452tv_nat () (let ((_let_1 (@var "Y4" tptp.produc194167194tv_nat))) (let ((_let_2 (@var "X4" tptp.produc194167194tv_nat))) (let ((_let_3 (@var "F2" (-> tptp.produc194167194tv_nat tptp.produc194167194tv_nat)))) (let ((_let_4 (@var "A3" tptp.set_Pr1725653840tv_nat))) (lambda (@list _let_3 _let_4) (forall (@list _let_2) (=> (_ (_ tptp.member737151281tv_nat _let_2) _let_4) (forall (@list _let_1) (=> (_ (_ tptp.member737151281tv_nat _let_1) _let_4) (=> (= (_ _let_3 _let_2) (_ _let_3 _let_1)) (= _let_2 _let_1))))))))))))
% 151.11/151.91  (define tptp.inj_on1745913142lle_tv () (let ((_let_1 (@var "Y4" tptp.produc270694976lle_tv))) (let ((_let_2 (@var "X4" tptp.produc270694976lle_tv))) (let ((_let_3 (@var "F2" (-> tptp.produc270694976lle_tv tptp.produc270694976lle_tv)))) (let ((_let_4 (@var "A3" tptp.set_Pr13445366lle_tv))) (lambda (@list _let_3 _let_4) (forall (@list _let_2) (=> (_ (_ tptp.member813679063lle_tv _let_2) _let_4) (forall (@list _let_1) (=> (_ (_ tptp.member813679063lle_tv _let_1) _let_4) (=> (= (_ _let_3 _let_2) (_ _let_3 _let_1)) (= _let_2 _let_1))))))))))))
% 151.11/151.91  (define tptp.inj_on26176689at_nat () (let ((_let_1 (@var "Y4" tptp.product_prod_nat_nat))) (let ((_let_2 (@var "X4" tptp.product_prod_nat_nat))) (let ((_let_3 (@var "F2" (-> tptp.product_prod_nat_nat tptp.product_prod_nat_nat)))) (let ((_let_4 (@var "A3" tptp.set_Pr1986765409at_nat))) (lambda (@list _let_3 _let_4) (forall (@list _let_2) (=> (_ (_ tptp.member701585322at_nat _let_2) _let_4) (forall (@list _let_1) (=> (_ (_ tptp.member701585322at_nat _let_1) _let_4) (=> (= (_ _let_3 _let_2) (_ _let_3 _let_1)) (= _let_2 _let_1))))))))))))
% 151.11/151.91  (define tptp.inj_on1955349912lle_tv () (let ((_let_1 (@var "Y4" tptp.nat))) (let ((_let_2 (@var "X4" tptp.nat))) (let ((_let_3 (@var "F2" (-> tptp.nat tptp.paraco1605129243lle_tv)))) (let ((_let_4 (@var "A3" tptp.set_nat))) (lambda (@list _let_3 _let_4) (forall (@list _let_2) (=> (_ (_ tptp.member_nat _let_2) _let_4) (forall (@list _let_1) (=> (_ (_ tptp.member_nat _let_1) _let_4) (=> (= (_ _let_3 _let_2) (_ _let_3 _let_1)) (= _let_2 _let_1))))))))))))
% 151.11/151.91  (define tptp.inj_on_nat_nat () (let ((_let_1 (@var "Y4" tptp.nat))) (let ((_let_2 (@var "X4" tptp.nat))) (let ((_let_3 (@var "F2" (-> tptp.nat tptp.nat)))) (let ((_let_4 (@var "A3" tptp.set_nat))) (lambda (@list _let_3 _let_4) (forall (@list _let_2) (=> (_ (_ tptp.member_nat _let_2) _let_4) (forall (@list _let_1) (=> (_ (_ tptp.member_nat _let_1) _let_4) (=> (= (_ _let_3 _let_2) (_ _let_3 _let_1)) (= _let_2 _let_1))))))))))))
% 151.11/151.91  (define tptp.inj_on772319074lle_tv () (let ((_let_1 (@var "Y4" tptp.paraco1605129243lle_tv))) (let ((_let_2 (@var "X4" tptp.paraco1605129243lle_tv))) (let ((_let_3 (@var "F2" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv)))) (let ((_let_4 (@var "A3" tptp.set_Pa1764573435lle_tv))) (lambda (@list _let_3 _let_4) (forall (@list _let_2) (=> (_ (_ tptp.member266900804lle_tv _let_2) _let_4) (forall (@list _let_1) (=> (_ (_ tptp.member266900804lle_tv _let_1) _let_4) (=> (= (_ _let_3 _let_2) (_ _let_3 _let_1)) (= _let_2 _let_1))))))))))))
% 151.11/151.91  (define tptp.produc234482697lle_tv () (let ((_let_1 (@var "F23" tptp.paraco1605129243lle_tv))) (let ((_let_2 (@var "F12" tptp.paraco1605129243lle_tv))) (let ((_let_3 (@var "Bool2" Bool))) (lambda (@list _let_2 _let_1 _let_3) (_ (_ (_ tptp.if_Par1134130401lle_tv _let_3) _let_2) _let_1))))))
% 151.11/151.91  (define tptp.produc1232814113lle_tv () (let ((_let_1 (@var "P2" tptp.produc1443694919lle_tv))) (lambda (@list _let_1) (_ (_ tptp.produc1710735575lle_fm (_ tptp.produc381314067lle_tv _let_1)) (_ tptp.produc262413013lle_tv _let_1)))))
% 151.11/151.91  (define tptp.produc178635363at_nat () (let ((_let_1 (@var "P2" tptp.produc596913417at_nat))) (lambda (@list _let_1) (_ (_ tptp.produc1680557635lle_tv (_ tptp.produc500618325at_nat _let_1)) (_ tptp.produc1589291287at_nat _let_1)))))
% 151.11/151.91  (define @t1 () (_ tptp.paraco1344940915le_Det true))
% 151.11/151.91  (define @t2 () (_ tptp.paraco1325918602e_eval tptp.i))
% 151.11/151.91  (define @t3 () (_ @t2 tptp.p1))
% 151.11/151.91  (define @t4 () (not (= @t3 @t1)))
% 151.11/151.91  (define @t5 () (_ @t2 tptp.p2))
% 151.11/151.91  (define @t6 () (not (= @t3 @t5)))
% 151.11/151.91  (define @t7 () (@var "Y42" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t8 () (@var "X42" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t9 () (@var "Y41" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t10 () (@var "X41" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t11 () (_ (_ tptp.paraco69239110le_Con @t10) @t8))
% 151.11/151.91  (define @t12 () (_ tptp.paraco1325918602e_eval (_ (_ tptp.paraco761681009ge_int tptp.f) tptp.i)))
% 151.11/151.91  (define @t13 () (_ @t12 tptp.p2))
% 151.11/151.91  (define @t14 () (_ @t12 tptp.p1))
% 151.11/151.91  (define @t15 () (_ tptp.paraco1344940915le_Det false))
% 151.11/151.91  (define @t16 () (@var "Q" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t17 () (@var "P" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t18 () (_ (_ tptp.paraco69239110le_Con @t17) @t16))
% 151.11/151.91  (define @t19 () (@var "I" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t20 () (_ tptp.paraco1325918602e_eval @t19))
% 151.11/151.91  (define @t21 () (_ @t20 @t18))
% 151.11/151.91  (define @t22 () (= @t21 @t15))
% 151.11/151.91  (define @t23 () (_ @t20 @t16))
% 151.11/151.91  (define @t24 () (= @t23 @t1))
% 151.11/151.91  (define @t25 () (not @t24))
% 151.11/151.91  (define @t26 () (=> @t25 @t22))
% 151.11/151.91  (define @t27 () (_ @t20 @t17))
% 151.11/151.91  (define @t28 () (= @t21 @t27))
% 151.11/151.91  (define @t29 () (=> @t24 @t28))
% 151.11/151.91  (define @t30 () (and @t29 @t26))
% 151.11/151.91  (define @t31 () (= @t27 @t1))
% 151.11/151.91  (define @t32 () (not @t31))
% 151.11/151.91  (define @t33 () (=> @t32 @t30))
% 151.11/151.91  (define @t34 () (= @t21 @t23))
% 151.11/151.91  (define @t35 () (=> @t31 @t34))
% 151.11/151.91  (define @t36 () (and @t35 @t33))
% 151.11/151.91  (define @t37 () (= @t27 @t23))
% 151.11/151.91  (define @t38 () (not @t37))
% 151.11/151.91  (define @t39 () (=> @t38 @t36))
% 151.11/151.91  (define @t40 () (=> @t37 @t28))
% 151.11/151.91  (define @t41 () (and @t40 @t39))
% 151.11/151.91  (define @t42 () (@list @t19 @t17 @t16))
% 151.11/151.91  (define @t43 () (forall @t42 @t41))
% 151.11/151.91  (define @t44 () (_ tptp.paraco1147068288nge_tv tptp.f))
% 151.11/151.91  (define @t45 () (@var "Y1" Bool))
% 151.11/151.91  (define @t46 () (@var "X1" Bool))
% 151.11/151.91  (define @t47 () (_ tptp.paraco1344940915le_Det @t46))
% 151.11/151.91  (define @t48 () (_ tptp.paraco327635598_valid @t17))
% 151.11/151.91  (define @t49 () (@var "U" tptp.set_nat))
% 151.11/151.91  (define @t50 () (_ tptp.paraco55203475lid_in @t49))
% 151.11/151.91  (define @t51 () (_ @t50 @t17))
% 151.11/151.91  (define @t52 () (@var "X52" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t53 () (@var "X51" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t54 () (_ (_ tptp.paraco1389086619le_Eql @t53) @t52))
% 151.11/151.91  (define @t55 () (@var "Y52" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t56 () (@var "Y51" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t57 () (@var "B" Bool))
% 151.11/151.91  (define @t58 () (_ tptp.paraco1344940915le_Det @t57))
% 151.11/151.91  (define @t59 () (@var "F" (-> tptp.nat tptp.nat)))
% 151.11/151.91  (define @t60 () (_ tptp.paraco1147068288nge_tv @t59))
% 151.11/151.91  (define @t61 () (_ @t20 (_ (_ tptp.paraco1389086619le_Eql @t17) @t16)))
% 151.11/151.91  (define @t62 () (@var "N" tptp.nat))
% 151.11/151.91  (define @t63 () (@var "X" (-> tptp.nat tptp.nat)))
% 151.11/151.91  (define @t64 () (@var "Y" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t65 () (= @t64 (_ tptp.paraco793048302_Indet (_ @t63 @t62))))
% 151.11/151.91  (define @t66 () (_ tptp.paraco793048302_Indet @t62))
% 151.11/151.91  (define @t67 () (@var "Xa" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t68 () (= @t67 @t66))
% 151.11/151.91  (define @t69 () (@list @t62))
% 151.11/151.91  (define @t70 () (@var "B2" Bool))
% 151.11/151.91  (define @t71 () (_ tptp.paraco1344940915le_Det @t70))
% 151.11/151.91  (define @t72 () (= @t64 @t71))
% 151.11/151.91  (define @t73 () (= @t67 @t71))
% 151.11/151.91  (define @t74 () (@list @t70))
% 151.11/151.91  (define @t75 () (= (_ (_ tptp.paraco1147068288nge_tv @t63) @t67) @t64))
% 151.11/151.91  (define @t76 () (@list @t63 @t67 @t64))
% 151.11/151.91  (define @t77 () (@var "F1" (-> Bool tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t78 () (@var "F22" (-> tptp.nat tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t79 () (_ (_ tptp.paraco2051596139lle_tv @t77) @t78))
% 151.11/151.91  (define @t80 () (_ @t20 (_ tptp.paraco445776468le_Neg @t17)))
% 151.11/151.91  (define @t81 () (= @t27 @t15))
% 151.11/151.91  (define @t82 () (not @t81))
% 151.11/151.91  (define @t83 () (@list @t19 @t17))
% 151.11/151.91  (define @t84 () (@var "N2" tptp.nat))
% 151.11/151.91  (define @t85 () (@var "X62" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t86 () (@var "X61" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t87 () (_ (_ tptp.paraco1745535428le_Eql @t86) @t85))
% 151.11/151.91  (define @t88 () (@var "Y3" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t89 () (@var "X3" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t90 () (_ tptp.paraco445776468le_Neg @t89))
% 151.11/151.91  (define @t91 () (@var "Y62" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t92 () (@var "Y61" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t93 () (@var "Y2" tptp.nat))
% 151.11/151.91  (define @t94 () (@var "X2" tptp.nat))
% 151.11/151.91  (define @t95 () (_ tptp.paraco793048302_Indet @t94))
% 151.11/151.91  (define @t96 () (@var "A" tptp.produc696645085lle_fm))
% 151.11/151.91  (define @t97 () (@var "P3" (-> tptp.produc696645085lle_fm Bool)))
% 151.11/151.91  (define @t98 () (@var "A" tptp.produc1852595672lle_tv))
% 151.11/151.91  (define @t99 () (@var "P3" (-> tptp.produc1852595672lle_tv Bool)))
% 151.11/151.91  (define @t100 () (@var "A" tptp.produc931990033lle_tv))
% 151.11/151.91  (define @t101 () (@var "P3" (-> tptp.produc931990033lle_tv Bool)))
% 151.11/151.91  (define @t102 () (@var "A" tptp.produc1281043295at_nat))
% 151.11/151.91  (define @t103 () (@var "P3" (-> tptp.produc1281043295at_nat Bool)))
% 151.11/151.91  (define @t104 () (@var "A" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t105 () (@var "P3" (-> tptp.paraco1605129243lle_tv Bool)))
% 151.11/151.91  (define @t106 () (_ tptp.collec1111687558lle_tv @t105))
% 151.11/151.91  (define @t107 () (_ tptp.member266900804lle_tv @t104))
% 151.11/151.91  (define @t108 () (@var "A" tptp.nat))
% 151.11/151.91  (define @t109 () (@var "P3" (-> tptp.nat Bool)))
% 151.11/151.91  (define @t110 () (_ tptp.collect_nat @t109))
% 151.11/151.91  (define @t111 () (_ tptp.member_nat @t108))
% 151.11/151.91  (define @t112 () (@var "A2" tptp.set_Pr2120184979lle_fm))
% 151.11/151.91  (define @t113 () (@var "X4" tptp.produc696645085lle_fm))
% 151.11/151.91  (define @t114 () (@list @t112))
% 151.11/151.91  (define @t115 () (@var "A2" tptp.set_Pr2061825550lle_tv))
% 151.11/151.91  (define @t116 () (@var "X4" tptp.produc1852595672lle_tv))
% 151.11/151.91  (define @t117 () (@list @t115))
% 151.11/151.91  (define @t118 () (@var "A2" tptp.set_Pr560526279lle_tv))
% 151.11/151.91  (define @t119 () (@var "X4" tptp.produc931990033lle_tv))
% 151.11/151.91  (define @t120 () (@list @t118))
% 151.11/151.91  (define @t121 () (@var "A2" tptp.set_Pr1357842111at_nat))
% 151.11/151.91  (define @t122 () (@var "X4" tptp.produc1281043295at_nat))
% 151.11/151.91  (define @t123 () (@list @t121))
% 151.11/151.91  (define @t124 () (@var "A2" tptp.set_Pa1764573435lle_tv))
% 151.11/151.91  (define @t125 () (@var "X4" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t126 () (_ tptp.member266900804lle_tv @t125))
% 151.11/151.91  (define @t127 () (@list @t125))
% 151.11/151.91  (define @t128 () (@list @t124))
% 151.11/151.91  (define @t129 () (@var "A2" tptp.set_nat))
% 151.11/151.91  (define @t130 () (@var "X4" tptp.nat))
% 151.11/151.91  (define @t131 () (_ tptp.member_nat @t130))
% 151.11/151.91  (define @t132 () (@list @t130))
% 151.11/151.91  (define @t133 () (@list @t129))
% 151.11/151.91  (define @t134 () (@var "Q2" (-> tptp.paraco1605129243lle_tv Bool)))
% 151.11/151.91  (define @t135 () (@var "X5" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t136 () (@list @t135))
% 151.11/151.91  (define @t137 () (@var "Q2" (-> tptp.nat Bool)))
% 151.11/151.91  (define @t138 () (@var "X5" tptp.nat))
% 151.11/151.91  (define @t139 () (@list @t138))
% 151.11/151.91  (define @t140 () (_ @t20 (_ (_ tptp.paraco1745535428le_Eql @t17) @t16)))
% 151.11/151.91  (define @t141 () (= @t23 @t15))
% 151.11/151.91  (define @t142 () (@var "P2" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t143 () (@var "I2" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t144 () (_ tptp.paraco1325918602e_eval @t143))
% 151.11/151.91  (define @t145 () (@var "A0" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t146 () (@var "A1" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t147 () (@var "A0" (-> tptp.nat tptp.nat)))
% 151.11/151.91  (define @t148 () (@var "P3" (-> (-> tptp.nat tptp.nat) tptp.paraco1605129243lle_tv Bool)))
% 151.11/151.91  (define @t149 () (@var "F3" (-> tptp.nat tptp.nat)))
% 151.11/151.91  (define @t150 () (_ @t148 @t149))
% 151.11/151.91  (define @t151 () (@list @t149 @t62))
% 151.11/151.91  (define @t152 () (@list @t149 @t70))
% 151.11/151.91  (define @t153 () (@var "X" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t154 () (@list @t153))
% 151.11/151.91  (define @t155 () (@var "X22" tptp.nat))
% 151.11/151.91  (define @t156 () (@var "X12" Bool))
% 151.11/151.91  (define @t157 () (@var "Tv" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t158 () (@var "X5" Bool))
% 151.11/151.91  (define @t159 () (@var "X" tptp.produc696645085lle_fm))
% 151.11/151.91  (define @t160 () (@list @t159))
% 151.11/151.91  (define @t161 () (@var "X" tptp.produc1852595672lle_tv))
% 151.11/151.91  (define @t162 () (@var "X" tptp.produc931990033lle_tv))
% 151.11/151.91  (define @t163 () (@list @t162))
% 151.11/151.91  (define @t164 () (@var "X" tptp.produc1281043295at_nat))
% 151.11/151.91  (define @t165 () (@var "X" tptp.produc194167194tv_nat))
% 151.11/151.91  (define @t166 () (_ tptp.member737151281tv_nat @t165))
% 151.11/151.91  (define @t167 () (@var "X" tptp.produc270694976lle_tv))
% 151.11/151.91  (define @t168 () (_ tptp.member813679063lle_tv @t167))
% 151.11/151.91  (define @t169 () (@var "X" tptp.product_prod_nat_nat))
% 151.11/151.91  (define @t170 () (_ tptp.member701585322at_nat @t169))
% 151.11/151.91  (define @t171 () (@var "X" tptp.nat))
% 151.11/151.91  (define @t172 () (_ tptp.member_nat @t171))
% 151.11/151.91  (define @t173 () (_ tptp.member266900804lle_tv @t153))
% 151.11/151.91  (define @t174 () (@var "Y4" tptp.produc1647334210lle_tv))
% 151.11/151.91  (define @t175 () (@var "X4" tptp.produc1647334210lle_tv))
% 151.11/151.91  (define @t176 () (= @t175 @t174))
% 151.11/151.91  (define @t177 () (@var "F" (-> tptp.produc1647334210lle_tv tptp.produc1647334210lle_tv)))
% 151.11/151.91  (define @t178 () (_ tptp.inj_on2112487900lle_tv @t177))
% 151.11/151.91  (define @t179 () (_ @t178 tptp.top_to1871154984lle_tv))
% 151.11/151.91  (define @t180 () (@list @t177))
% 151.11/151.91  (define @t181 () (@var "Y4" tptp.nat))
% 151.11/151.91  (define @t182 () (= @t130 @t181))
% 151.11/151.91  (define @t183 () (@var "F" (-> tptp.nat tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t184 () (_ @t183 @t130))
% 151.11/151.91  (define @t185 () (@list @t130 @t181))
% 151.11/151.91  (define @t186 () (_ tptp.inj_on1955349912lle_tv @t183))
% 151.11/151.91  (define @t187 () (_ @t186 tptp.top_top_set_nat))
% 151.11/151.91  (define @t188 () (@list @t183))
% 151.11/151.91  (define @t189 () (@var "Y4" tptp.produc194167194tv_nat))
% 151.11/151.91  (define @t190 () (@var "X4" tptp.produc194167194tv_nat))
% 151.11/151.91  (define @t191 () (= @t190 @t189))
% 151.11/151.91  (define @t192 () (@var "F" (-> tptp.produc194167194tv_nat tptp.produc194167194tv_nat)))
% 151.11/151.91  (define @t193 () (_ tptp.inj_on552895452tv_nat @t192))
% 151.11/151.91  (define @t194 () (_ @t193 tptp.top_to975729152tv_nat))
% 151.11/151.91  (define @t195 () (@list @t192))
% 151.11/151.91  (define @t196 () (@var "Y4" tptp.produc270694976lle_tv))
% 151.11/151.91  (define @t197 () (@var "X4" tptp.produc270694976lle_tv))
% 151.11/151.91  (define @t198 () (= @t197 @t196))
% 151.11/151.91  (define @t199 () (@var "F" (-> tptp.produc270694976lle_tv tptp.produc270694976lle_tv)))
% 151.11/151.91  (define @t200 () (_ tptp.inj_on1745913142lle_tv @t199))
% 151.11/151.91  (define @t201 () (_ @t200 tptp.top_to1411004326lle_tv))
% 151.11/151.91  (define @t202 () (@list @t199))
% 151.11/151.91  (define @t203 () (@var "Y4" tptp.product_prod_nat_nat))
% 151.11/151.91  (define @t204 () (@var "X4" tptp.product_prod_nat_nat))
% 151.11/151.91  (define @t205 () (= @t204 @t203))
% 151.11/151.91  (define @t206 () (@var "F" (-> tptp.product_prod_nat_nat tptp.product_prod_nat_nat)))
% 151.11/151.91  (define @t207 () (_ tptp.inj_on26176689at_nat @t206))
% 151.11/151.91  (define @t208 () (_ @t207 tptp.top_to1555900337at_nat))
% 151.11/151.91  (define @t209 () (@list @t206))
% 151.11/151.91  (define @t210 () (_ @t59 @t181))
% 151.11/151.91  (define @t211 () (_ @t59 @t130))
% 151.11/151.91  (define @t212 () (_ tptp.inj_on_nat_nat @t59))
% 151.11/151.91  (define @t213 () (_ @t212 tptp.top_top_set_nat))
% 151.11/151.91  (define @t214 () (@list @t59))
% 151.11/151.91  (define @t215 () (@var "Y4" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t216 () (= @t125 @t215))
% 151.11/151.91  (define @t217 () (@var "F" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t218 () (_ @t217 @t215))
% 151.11/151.91  (define @t219 () (_ @t217 @t125))
% 151.11/151.91  (define @t220 () (_ tptp.inj_on772319074lle_tv @t217))
% 151.11/151.91  (define @t221 () (_ @t220 tptp.top_to1057771083lle_tv))
% 151.11/151.91  (define @t222 () (@list @t217))
% 151.11/151.91  (define @t223 () (@var "Y" tptp.produc1647334210lle_tv))
% 151.11/151.91  (define @t224 () (@var "X" tptp.produc1647334210lle_tv))
% 151.11/151.91  (define @t225 () (= @t224 @t223))
% 151.11/151.91  (define @t226 () (= (_ @t177 @t224) (_ @t177 @t223)))
% 151.11/151.91  (define @t227 () (= @t226 @t225))
% 151.11/151.91  (define @t228 () (@list @t177 @t224 @t223))
% 151.11/151.91  (define @t229 () (@var "Y" tptp.nat))
% 151.11/151.91  (define @t230 () (= @t171 @t229))
% 151.11/151.91  (define @t231 () (= (_ @t183 @t171) (_ @t183 @t229)))
% 151.11/151.91  (define @t232 () (= @t231 @t230))
% 151.11/151.91  (define @t233 () (@list @t183 @t171 @t229))
% 151.11/151.91  (define @t234 () (@var "Y" tptp.produc194167194tv_nat))
% 151.11/151.91  (define @t235 () (= @t165 @t234))
% 151.11/151.91  (define @t236 () (= (_ @t192 @t165) (_ @t192 @t234)))
% 151.11/151.91  (define @t237 () (= @t236 @t235))
% 151.11/151.91  (define @t238 () (@list @t192 @t165 @t234))
% 151.11/151.91  (define @t239 () (@var "Y" tptp.produc270694976lle_tv))
% 151.11/151.91  (define @t240 () (= @t167 @t239))
% 151.11/151.91  (define @t241 () (= (_ @t199 @t167) (_ @t199 @t239)))
% 151.11/151.91  (define @t242 () (= @t241 @t240))
% 151.11/151.91  (define @t243 () (@list @t199 @t167 @t239))
% 151.11/151.91  (define @t244 () (@var "Y" tptp.product_prod_nat_nat))
% 151.11/151.91  (define @t245 () (= @t169 @t244))
% 151.11/151.91  (define @t246 () (= (_ @t206 @t169) (_ @t206 @t244)))
% 151.11/151.91  (define @t247 () (= @t246 @t245))
% 151.11/151.91  (define @t248 () (@list @t206 @t169 @t244))
% 151.11/151.91  (define @t249 () (_ @t59 @t171))
% 151.11/151.91  (define @t250 () (= @t249 (_ @t59 @t229)))
% 151.11/151.91  (define @t251 () (= @t250 @t230))
% 151.11/151.91  (define @t252 () (@list @t59 @t171 @t229))
% 151.11/151.91  (define @t253 () (= @t153 @t64))
% 151.11/151.91  (define @t254 () (_ @t217 @t64))
% 151.11/151.91  (define @t255 () (_ @t217 @t153))
% 151.11/151.91  (define @t256 () (= @t255 @t254))
% 151.11/151.91  (define @t257 () (= @t256 @t253))
% 151.11/151.91  (define @t258 () (@list @t217 @t153 @t64))
% 151.11/151.91  (define @t259 () (@var "Y5" tptp.produc1647334210lle_tv))
% 151.11/151.91  (define @t260 () (@var "X5" tptp.produc1647334210lle_tv))
% 151.11/151.91  (define @t261 () (=> (= (_ @t177 @t260) (_ @t177 @t259)) (= @t260 @t259)))
% 151.11/151.91  (define @t262 () (@list @t260 @t259))
% 151.11/151.91  (define @t263 () (@var "Y5" tptp.nat))
% 151.11/151.91  (define @t264 () (= @t138 @t263))
% 151.11/151.91  (define @t265 () (_ @t183 @t138))
% 151.11/151.91  (define @t266 () (=> (= @t265 (_ @t183 @t263)) @t264))
% 151.11/151.91  (define @t267 () (@list @t138 @t263))
% 151.11/151.91  (define @t268 () (@var "Y5" tptp.produc194167194tv_nat))
% 151.11/151.91  (define @t269 () (@var "X5" tptp.produc194167194tv_nat))
% 151.11/151.91  (define @t270 () (=> (= (_ @t192 @t269) (_ @t192 @t268)) (= @t269 @t268)))
% 151.11/151.91  (define @t271 () (@list @t269 @t268))
% 151.11/151.91  (define @t272 () (@var "Y5" tptp.produc270694976lle_tv))
% 151.11/151.91  (define @t273 () (@var "X5" tptp.produc270694976lle_tv))
% 151.11/151.91  (define @t274 () (=> (= (_ @t199 @t273) (_ @t199 @t272)) (= @t273 @t272)))
% 151.11/151.91  (define @t275 () (@list @t273 @t272))
% 151.11/151.91  (define @t276 () (@var "Y5" tptp.product_prod_nat_nat))
% 151.11/151.91  (define @t277 () (@var "X5" tptp.product_prod_nat_nat))
% 151.11/151.91  (define @t278 () (=> (= (_ @t206 @t277) (_ @t206 @t276)) (= @t277 @t276)))
% 151.11/151.91  (define @t279 () (@list @t277 @t276))
% 151.11/151.91  (define @t280 () (_ @t59 @t138))
% 151.11/151.91  (define @t281 () (=> (= @t280 (_ @t59 @t263)) @t264))
% 151.11/151.91  (define @t282 () (@var "Y5" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t283 () (_ @t217 @t135))
% 151.11/151.91  (define @t284 () (=> (= @t283 (_ @t217 @t282)) (= @t135 @t282)))
% 151.11/151.91  (define @t285 () (@list @t135 @t282))
% 151.11/151.91  (define @t286 () (@var "X5" tptp.produc696645085lle_fm))
% 151.11/151.91  (define @t287 () (_ tptp.member1474794996lle_fm @t286))
% 151.11/151.91  (define @t288 () (@list @t286))
% 151.11/151.91  (define @t289 () (@var "X5" tptp.produc1852595672lle_tv))
% 151.11/151.91  (define @t290 () (_ tptp.member146333935lle_tv @t289))
% 151.11/151.91  (define @t291 () (@list @t289))
% 151.11/151.91  (define @t292 () (@var "X5" tptp.produc931990033lle_tv))
% 151.11/151.91  (define @t293 () (_ tptp.member1569366824lle_tv @t292))
% 151.11/151.91  (define @t294 () (@list @t292))
% 151.11/151.91  (define @t295 () (@var "X5" tptp.produc1281043295at_nat))
% 151.11/151.91  (define @t296 () (_ tptp.member112824072at_nat @t295))
% 151.11/151.91  (define @t297 () (@list @t295))
% 151.11/151.91  (define @t298 () (@var "A2" tptp.set_Pr1725653840tv_nat))
% 151.11/151.91  (define @t299 () (_ tptp.member737151281tv_nat @t269))
% 151.11/151.91  (define @t300 () (_ @t299 @t298))
% 151.11/151.91  (define @t301 () (@list @t269))
% 151.11/151.91  (define @t302 () (@var "A2" tptp.set_Pr13445366lle_tv))
% 151.11/151.91  (define @t303 () (_ tptp.member813679063lle_tv @t273))
% 151.11/151.91  (define @t304 () (_ @t303 @t302))
% 151.11/151.91  (define @t305 () (@list @t273))
% 151.11/151.91  (define @t306 () (@var "A2" tptp.set_Pr1986765409at_nat))
% 151.11/151.91  (define @t307 () (_ tptp.member701585322at_nat @t277))
% 151.11/151.91  (define @t308 () (_ @t307 @t306))
% 151.11/151.91  (define @t309 () (@list @t277))
% 151.11/151.91  (define @t310 () (_ tptp.member_nat @t138))
% 151.11/151.91  (define @t311 () (_ @t310 @t129))
% 151.11/151.91  (define @t312 () (_ tptp.member266900804lle_tv @t135))
% 151.11/151.91  (define @t313 () (_ @t312 @t124))
% 151.11/151.91  (define @t314 () (@var "A2" tptp.set_Pr2014382200lle_tv))
% 151.11/151.91  (define @t315 () (_ (_ tptp.member1531318361lle_tv @t223) @t314))
% 151.11/151.91  (define @t316 () (_ (_ tptp.member1531318361lle_tv @t224) @t314))
% 151.11/151.91  (define @t317 () (_ @t178 @t314))
% 151.11/151.91  (define @t318 () (@list @t177 @t314 @t224 @t223))
% 151.11/151.91  (define @t319 () (_ (_ tptp.member737151281tv_nat @t234) @t298))
% 151.11/151.91  (define @t320 () (_ @t166 @t298))
% 151.11/151.91  (define @t321 () (_ @t193 @t298))
% 151.11/151.91  (define @t322 () (@list @t192 @t298 @t165 @t234))
% 151.11/151.91  (define @t323 () (_ (_ tptp.member813679063lle_tv @t239) @t302))
% 151.11/151.91  (define @t324 () (_ @t168 @t302))
% 151.11/151.91  (define @t325 () (_ @t200 @t302))
% 151.11/151.91  (define @t326 () (@list @t199 @t302 @t167 @t239))
% 151.11/151.91  (define @t327 () (_ (_ tptp.member701585322at_nat @t244) @t306))
% 151.11/151.91  (define @t328 () (_ @t170 @t306))
% 151.11/151.91  (define @t329 () (_ @t207 @t306))
% 151.11/151.91  (define @t330 () (@list @t206 @t306 @t169 @t244))
% 151.11/151.91  (define @t331 () (_ tptp.member_nat @t229))
% 151.11/151.91  (define @t332 () (_ @t331 @t129))
% 151.11/151.91  (define @t333 () (_ @t172 @t129))
% 151.11/151.91  (define @t334 () (=> @t333 (=> @t332 @t230)))
% 151.11/151.91  (define @t335 () (_ @t186 @t129))
% 151.11/151.91  (define @t336 () (@list @t183 @t129 @t171 @t229))
% 151.11/151.91  (define @t337 () (_ @t212 @t129))
% 151.11/151.91  (define @t338 () (@list @t59 @t129 @t171 @t229))
% 151.11/151.91  (define @t339 () (_ tptp.member266900804lle_tv @t64))
% 151.11/151.91  (define @t340 () (_ @t339 @t124))
% 151.11/151.91  (define @t341 () (_ @t173 @t124))
% 151.11/151.91  (define @t342 () (_ @t220 @t124))
% 151.11/151.91  (define @t343 () (@list @t217 @t124 @t153 @t64))
% 151.11/151.91  (define @t344 () (_ (_ tptp.member_nat @t263) @t129))
% 151.11/151.91  (define @t345 () (@var "G" (-> tptp.produc1647334210lle_tv tptp.produc1647334210lle_tv)))
% 151.11/151.91  (define @t346 () (@var "A4" tptp.produc1647334210lle_tv))
% 151.11/151.91  (define @t347 () (@var "G" (-> tptp.produc194167194tv_nat tptp.produc194167194tv_nat)))
% 151.11/151.91  (define @t348 () (@var "A4" tptp.produc194167194tv_nat))
% 151.11/151.91  (define @t349 () (@var "G" (-> tptp.produc270694976lle_tv tptp.produc270694976lle_tv)))
% 151.11/151.91  (define @t350 () (@var "A4" tptp.produc270694976lle_tv))
% 151.11/151.91  (define @t351 () (@var "G" (-> tptp.product_prod_nat_nat tptp.product_prod_nat_nat)))
% 151.11/151.91  (define @t352 () (@var "A4" tptp.product_prod_nat_nat))
% 151.11/151.91  (define @t353 () (@var "G" (-> tptp.nat tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t354 () (@var "A4" tptp.nat))
% 151.11/151.91  (define @t355 () (_ (_ tptp.member_nat @t354) @t129))
% 151.11/151.91  (define @t356 () (@list @t354))
% 151.11/151.91  (define @t357 () (@var "G" (-> tptp.nat tptp.nat)))
% 151.11/151.91  (define @t358 () (_ tptp.inj_on_nat_nat @t357))
% 151.11/151.91  (define @t359 () (_ @t358 @t129))
% 151.11/151.91  (define @t360 () (@var "G" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t361 () (_ tptp.inj_on772319074lle_tv @t360))
% 151.11/151.91  (define @t362 () (_ @t361 @t124))
% 151.11/151.91  (define @t363 () (@var "A4" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t364 () (not @t230))
% 151.11/151.91  (define @t365 () (_ @t357 @t280))
% 151.11/151.91  (define @t366 () (= @t365 @t138))
% 151.11/151.91  (define @t367 () (@list @t129 @t357 @t59))
% 151.11/151.91  (define @t368 () (_ @t360 @t283))
% 151.11/151.91  (define @t369 () (= @t368 @t135))
% 151.11/151.91  (define @t370 () (@list @t124 @t360 @t217))
% 151.11/151.91  (define @t371 () (@var "Fm" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t372 () (@var "P3" (-> tptp.paraco1604210848lle_fm Bool)))
% 151.11/151.91  (define @t373 () (@var "X22" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t374 () (@var "X1a" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t375 () (_ @t372 @t373))
% 151.11/151.91  (define @t376 () (_ @t372 @t374))
% 151.11/151.91  (define @t377 () (@list @t374 @t373))
% 151.11/151.91  (define @t378 () (@var "X5" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t379 () (_ @t372 tptp.paraco367965286_Truth))
% 151.11/151.91  (define @t380 () (@var "X5" tptp.list_char))
% 151.11/151.91  (define @t381 () (@var "X622" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t382 () (@var "X612" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t383 () (@var "Y" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t384 () (@var "X522" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t385 () (@var "X512" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t386 () (@var "X422" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t387 () (@var "X412" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t388 () (@var "X32" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t389 () (@var "X12" tptp.list_char))
% 151.11/151.91  (define @t390 () (@var "Q3" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t391 () (@var "P4" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t392 () (_ (_ tptp.paraco1745535428le_Eql @t391) @t390))
% 151.11/151.91  (define @t393 () (@var "X" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t394 () (@list @t391 @t390))
% 151.11/151.91  (define @t395 () (_ (_ tptp.paraco1389086619le_Eql @t391) @t390))
% 151.11/151.91  (define @t396 () (_ (_ tptp.paraco69239110le_Con @t391) @t390))
% 151.11/151.91  (define @t397 () (_ tptp.paraco445776468le_Neg @t391))
% 151.11/151.91  (define @t398 () (@list @t391))
% 151.11/151.91  (define @t399 () (@var "S2" tptp.list_char))
% 151.11/151.91  (define @t400 () (_ tptp.paraco1480028776le_Pro @t399))
% 151.11/151.91  (define @t401 () (@list @t399))
% 151.11/151.91  (define @t402 () (@var "A0" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t403 () (_ @t372 @t390))
% 151.11/151.91  (define @t404 () (_ @t372 @t391))
% 151.11/151.91  (define @t405 () (@var "F22" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t406 () (@var "F1" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t407 () (_ (_ tptp.produc234482697lle_tv @t406) @t405))
% 151.11/151.91  (define @t408 () (@list @t406 @t405))
% 151.11/151.91  (define @t409 () (_ @t105 @t405))
% 151.11/151.91  (define @t410 () (@var "Bool" Bool))
% 151.11/151.91  (define @t411 () (not @t410))
% 151.11/151.91  (define @t412 () (_ @t105 @t406))
% 151.11/151.91  (define @t413 () (_ @t407 @t410))
% 151.11/151.91  (define @t414 () (_ @t105 @t413))
% 151.11/151.91  (define @t415 () (@list @t105 @t406 @t405 @t410))
% 151.11/151.91  (define @t416 () (@var "Y1" tptp.list_char))
% 151.11/151.91  (define @t417 () (@var "X1" tptp.list_char))
% 151.11/151.91  (define @t418 () (_ tptp.paraco1480028776le_Pro @t417))
% 151.11/151.91  (define @t419 () (@var "S3" tptp.list_char))
% 151.11/151.91  (define @t420 () (@var "H" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t421 () (@var "I3" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t422 () (_ tptp.produc1710735575lle_fm @t421))
% 151.11/151.91  (define @t423 () (@list @t421 @t391 @t390))
% 151.11/151.91  (define @t424 () (@var "B3" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t425 () (@var "B" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t426 () (= @t425 @t424))
% 151.11/151.91  (define @t427 () (@var "A5" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t428 () (@var "A" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t429 () (= @t428 @t427))
% 151.11/151.91  (define @t430 () (_ (_ tptp.produc1710735575lle_fm @t427) @t424))
% 151.11/151.91  (define @t431 () (_ tptp.produc1710735575lle_fm @t428))
% 151.11/151.91  (define @t432 () (_ @t431 @t425))
% 151.11/151.91  (define @t433 () (= @t432 @t430))
% 151.11/151.91  (define @t434 () (@list @t428 @t425 @t427 @t424))
% 151.11/151.91  (define @t435 () (@var "B3" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t436 () (@var "B" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t437 () (= @t436 @t435))
% 151.11/151.91  (define @t438 () (@var "A5" (-> tptp.nat tptp.nat)))
% 151.11/151.91  (define @t439 () (@var "A" (-> tptp.nat tptp.nat)))
% 151.11/151.91  (define @t440 () (= @t439 @t438))
% 151.11/151.91  (define @t441 () (_ (_ tptp.produc1680557635lle_tv @t438) @t435))
% 151.11/151.91  (define @t442 () (_ tptp.produc1680557635lle_tv @t439))
% 151.11/151.91  (define @t443 () (_ @t442 @t436))
% 151.11/151.91  (define @t444 () (= @t443 @t441))
% 151.11/151.91  (define @t445 () (@list @t439 @t436 @t438 @t435))
% 151.11/151.91  (define @t446 () (@var "Y2" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t447 () (@var "X2" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t448 () (@var "Y1" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t449 () (@var "X1" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t450 () (_ (_ tptp.produc1710735575lle_fm @t449) @t447))
% 151.11/151.91  (define @t451 () (@var "Y2" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t452 () (@var "X2" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t453 () (@var "Y1" (-> tptp.nat tptp.nat)))
% 151.11/151.91  (define @t454 () (@var "X1" (-> tptp.nat tptp.nat)))
% 151.11/151.91  (define @t455 () (_ (_ tptp.produc1680557635lle_tv @t454) @t452))
% 151.11/151.91  (define @t456 () (@var "X" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t457 () (@var "F" (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.list_char tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t458 () (_ tptp.produc1710735575lle_fm @t456))
% 151.11/151.91  (define @t459 () (_ @t458 @t383))
% 151.11/151.91  (define @t460 () (@var "F" (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat)))
% 151.11/151.91  (define @t461 () (_ tptp.produc1680557635lle_tv @t63))
% 151.11/151.91  (define @t462 () (_ @t461 @t64))
% 151.11/151.91  (define @t463 () (@var "F" (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm)))
% 151.11/151.91  (define @t464 () (@var "Prod" tptp.produc696645085lle_fm))
% 151.11/151.91  (define @t465 () (@var "B2" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t466 () (@var "A4" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t467 () (_ (_ tptp.produc1710735575lle_fm @t466) @t465))
% 151.11/151.91  (define @t468 () (@list @t466 @t465))
% 151.11/151.91  (define @t469 () (forall @t468 (_ @t97 @t467)))
% 151.11/151.91  (define @t470 () (@var "Prod" tptp.produc931990033lle_tv))
% 151.11/151.91  (define @t471 () (@var "B2" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t472 () (@var "A4" (-> tptp.nat tptp.nat)))
% 151.11/151.91  (define @t473 () (_ (_ tptp.produc1680557635lle_tv @t472) @t471))
% 151.11/151.91  (define @t474 () (@list @t472 @t471))
% 151.11/151.91  (define @t475 () (forall @t474 (_ @t101 @t473)))
% 151.11/151.91  (define @t476 () (@var "Y" tptp.produc696645085lle_fm))
% 151.11/151.91  (define @t477 () (@var "Y" tptp.produc931990033lle_tv))
% 151.11/151.91  (define @t478 () (@var "P" tptp.produc696645085lle_fm))
% 151.11/151.91  (define @t479 () (@var "P" tptp.produc931990033lle_tv))
% 151.11/151.91  (define @t480 () (@var "Y5" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t481 () (@var "X5" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t482 () (_ (_ tptp.produc1710735575lle_fm @t481) @t480))
% 151.11/151.91  (define @t483 () (@list @t481 @t480))
% 151.11/151.91  (define @t484 () (@var "X5" (-> tptp.nat tptp.nat)))
% 151.11/151.91  (define @t485 () (_ (_ tptp.produc1680557635lle_tv @t484) @t282))
% 151.11/151.91  (define @t486 () (@list @t484 @t282))
% 151.11/151.91  (define @t487 () (@var "F22" (-> tptp.nat tptp.nat)))
% 151.11/151.91  (define @t488 () (@var "F1" (-> tptp.nat tptp.nat)))
% 151.11/151.91  (define @t489 () (_ (_ tptp.inj_on_nat_nat @t487) tptp.top_top_set_nat))
% 151.11/151.91  (define @t490 () (_ (_ tptp.inj_on_nat_nat @t488) tptp.top_top_set_nat))
% 151.11/151.91  (define @t491 () (@var "F22" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t492 () (_ (_ tptp.inj_on772319074lle_tv @t491) tptp.top_to1057771083lle_tv))
% 151.11/151.91  (define @t493 () (@var "F1" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t494 () (_ (_ tptp.inj_on772319074lle_tv @t493) tptp.top_to1057771083lle_tv))
% 151.11/151.91  (define @t495 () (@var "R2" tptp.set_Pr2120184979lle_fm))
% 151.11/151.91  (define @t496 () (@var "S4" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t497 () (@var "R" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t498 () (_ tptp.produc1710735575lle_fm @t497))
% 151.11/151.91  (define @t499 () (@var "S3" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t500 () (@var "R2" tptp.set_Pr560526279lle_tv))
% 151.11/151.91  (define @t501 () (@var "S4" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t502 () (@var "R" (-> tptp.nat tptp.nat)))
% 151.11/151.91  (define @t503 () (_ tptp.produc1680557635lle_tv @t502))
% 151.11/151.91  (define @t504 () (@var "S3" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t505 () (@var "F" (-> tptp.produc696645085lle_fm Bool)))
% 151.11/151.91  (define @t506 () (_ (_ (_ tptp.produc275353523e_fm_o @t505) @t428) @t425))
% 151.11/151.91  (define @t507 () (_ @t505 @t432))
% 151.11/151.91  (define @t508 () (@list @t505 @t428 @t425))
% 151.11/151.91  (define @t509 () (@var "F" (-> tptp.produc931990033lle_tv Bool)))
% 151.11/151.91  (define @t510 () (_ (_ (_ tptp.produc752649287e_tv_o @t509) @t439) @t436))
% 151.11/151.91  (define @t511 () (_ @t509 @t443))
% 151.11/151.91  (define @t512 () (@list @t509 @t439 @t436))
% 151.11/151.91  (define @t513 () (@var "G" (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm)))
% 151.11/151.91  (define @t514 () (_ (_ tptp.produc1710735575lle_fm (_ @t457 @t428)) (_ @t513 @t425)))
% 151.11/151.91  (define @t515 () (_ (_ tptp.produc1900967599lle_fm @t457) @t513))
% 151.11/151.91  (define @t516 () (@var "G" (-> tptp.paraco1604210848lle_fm tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t517 () (@var "F" (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.nat tptp.nat)))
% 151.11/151.91  (define @t518 () (_ (_ tptp.produc1680557635lle_tv (_ @t517 @t428)) (_ @t516 @t425)))
% 151.11/151.91  (define @t519 () (_ (_ tptp.produc1566550641lle_tv @t517) @t516))
% 151.11/151.91  (define @t520 () (@var "G" (-> tptp.paraco1605129243lle_tv tptp.paraco1604210848lle_fm)))
% 151.11/151.91  (define @t521 () (@var "F" (-> (-> tptp.nat tptp.nat) tptp.list_char tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t522 () (_ (_ tptp.produc1710735575lle_fm (_ @t521 @t439)) (_ @t520 @t436)))
% 151.11/151.91  (define @t523 () (_ (_ tptp.produc951033137lle_fm @t521) @t520))
% 151.11/151.91  (define @t524 () (_ (_ tptp.produc1680557635lle_tv (_ @t460 @t439)) (_ @t360 @t436)))
% 151.11/151.91  (define @t525 () (_ (_ tptp.produc532909085lle_tv @t460) @t360))
% 151.11/151.91  (define @t526 () (_ tptp.produc1680557635lle_tv @t149))
% 151.11/151.91  (define @t527 () (_ tptp.accp_P2085826120lle_tv tptp.paraco1632582009tv_rel))
% 151.11/151.91  (define @t528 () (_ (_ tptp.the_inv_into_nat_nat @t129) @t59))
% 151.11/151.91  (define @t529 () (_ (_ tptp.the_in452116896lle_tv @t124) @t217))
% 151.11/151.91  (define @t530 () (_ @t528 @t229))
% 151.11/151.91  (define @t531 () (_ @t529 @t64))
% 151.11/151.91  (define @t532 () (@var "R" tptp.set_Pr1986765409at_nat))
% 151.11/151.91  (define @t533 () (_ tptp.total_on_nat tptp.top_top_set_nat))
% 151.11/151.91  (define @t534 () (_ @t533 @t532))
% 151.11/151.91  (define @t535 () (@var "R" tptp.set_Pr2014382200lle_tv))
% 151.11/151.91  (define @t536 () (_ tptp.total_1781621663lle_tv tptp.top_to1057771083lle_tv))
% 151.11/151.91  (define @t537 () (_ @t536 @t535))
% 151.11/151.91  (define @t538 () (@var "F" (-> tptp.paraco1605129243lle_tv tptp.nat)))
% 151.11/151.91  (define @t539 () (_ tptp.image_nat_nat @t59))
% 151.11/151.91  (define @t540 () (_ @t539 @t129))
% 151.11/151.91  (define @t541 () (@list @t59 @t129))
% 151.11/151.91  (define @t542 () (_ tptp.image_335818702lle_tv @t217))
% 151.11/151.91  (define @t543 () (_ @t542 @t124))
% 151.11/151.91  (define @t544 () (@list @t217 @t124))
% 151.11/151.91  (define @t545 () (_ (_ tptp.image_807538418lle_fm @t515) @t495))
% 151.11/151.91  (define @t546 () (_ (_ tptp.member1474794996lle_fm @t432) @t495))
% 151.11/151.91  (define @t547 () (_ (_ tptp.image_1154804148lle_tv @t519) @t495))
% 151.11/151.91  (define @t548 () (_ (_ tptp.image_1585092542lle_fm @t523) @t500))
% 151.11/151.91  (define @t549 () (_ (_ tptp.member1569366824lle_tv @t443) @t500))
% 151.11/151.91  (define @t550 () (_ (_ tptp.image_1751508608lle_tv @t525) @t500))
% 151.11/151.91  (define @t551 () (@var "Y" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t552 () (_ tptp.produc1710735575lle_fm @t551))
% 151.11/151.91  (define @t553 () (_ @t552 @t393))
% 151.11/151.91  (define @t554 () (_ (_ tptp.produc1943344577lle_tv @t393) @t551))
% 151.11/151.91  (define @t555 () (@var "Y" (-> tptp.nat tptp.nat)))
% 151.11/151.91  (define @t556 () (_ tptp.produc1680557635lle_tv @t555))
% 151.11/151.91  (define @t557 () (_ @t556 @t153))
% 151.11/151.91  (define @t558 () (_ (_ tptp.produc1633679363at_nat @t153) @t555))
% 151.11/151.91  (define @t559 () (_ (_ tptp.produc1943344577lle_tv @t383) @t456))
% 151.11/151.91  (define @t560 () (_ (_ tptp.produc1633679363at_nat @t64) @t63))
% 151.11/151.91  (define @t561 () (@var "A2" tptp.set_Pr1723822845lle_tv))
% 151.11/151.91  (define @t562 () (@var "A2" tptp.set_Pr840833727at_nat))
% 151.11/151.91  (define @t563 () (_ tptp.produc505105722at_nat @t59))
% 151.11/151.91  (define @t564 () (= (_ (_ tptp.image_nat_nat @t357) tptp.top_top_set_nat) tptp.top_top_set_nat))
% 151.11/151.91  (define @t565 () (_ @t539 tptp.top_top_set_nat))
% 151.11/151.91  (define @t566 () (= @t565 tptp.top_top_set_nat))
% 151.11/151.91  (define @t567 () (@list @t59 @t357))
% 151.11/151.91  (define @t568 () (= (_ (_ tptp.image_1151963140lle_tv @t353) tptp.top_top_set_nat) tptp.top_to1057771083lle_tv))
% 151.11/151.91  (define @t569 () (@var "G" (-> tptp.paraco1605129243lle_tv tptp.nat)))
% 151.11/151.91  (define @t570 () (= (_ (_ tptp.image_376325286tv_nat @t569) tptp.top_to1057771083lle_tv) tptp.top_top_set_nat))
% 151.11/151.91  (define @t571 () (= (_ (_ tptp.image_335818702lle_tv @t360) tptp.top_to1057771083lle_tv) tptp.top_to1057771083lle_tv))
% 151.11/151.91  (define @t572 () (= (_ (_ tptp.image_1151963140lle_tv @t183) tptp.top_top_set_nat) tptp.top_to1057771083lle_tv))
% 151.11/151.91  (define @t573 () (= (_ (_ tptp.image_376325286tv_nat @t538) tptp.top_to1057771083lle_tv) tptp.top_top_set_nat))
% 151.11/151.91  (define @t574 () (@list @t181))
% 151.11/151.91  (define @t575 () (@list @t215))
% 151.11/151.91  (define @t576 () (_ @t542 tptp.top_to1057771083lle_tv))
% 151.11/151.91  (define @t577 () (= @t576 tptp.top_to1057771083lle_tv))
% 151.11/151.91  (define @t578 () (forall @t139 @t366))
% 151.11/151.91  (define @t579 () (_ @t538 @t135))
% 151.11/151.91  (define @t580 () (= @t229 @t280))
% 151.11/151.91  (define @t581 () (@list @t59 @t229))
% 151.11/151.91  (define @t582 () (= @t64 @t265))
% 151.11/151.91  (define @t583 () (@list @t183 @t64))
% 151.11/151.91  (define @t584 () (= @t229 @t579))
% 151.11/151.91  (define @t585 () (@list @t538 @t229))
% 151.11/151.91  (define @t586 () (= @t64 @t283))
% 151.11/151.91  (define @t587 () (@list @t217 @t64))
% 151.11/151.91  (define @t588 () (@var "Xa2" tptp.nat))
% 151.11/151.91  (define @t589 () (@var "Xa2" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t590 () (= (_ (_ tptp.member_nat (_ @t59 @t108)) @t540) (_ @t111 @t129)))
% 151.11/151.91  (define @t591 () (= (_ (_ tptp.member266900804lle_tv (_ @t217 @t104)) @t543) (_ @t107 @t124)))
% 151.11/151.91  (define @t592 () (@var "B4" tptp.set_nat))
% 151.11/151.91  (define @t593 () (= (= @t540 (_ @t539 @t592)) (= @t129 @t592)))
% 151.11/151.91  (define @t594 () (@list @t59 @t129 @t592))
% 151.11/151.91  (define @t595 () (@var "B4" tptp.set_Pa1764573435lle_tv))
% 151.11/151.91  (define @t596 () (= (= @t543 (_ @t542 @t595)) (= @t124 @t595)))
% 151.11/151.91  (define @t597 () (@list @t217 @t124 @t595))
% 151.11/151.91  (define @t598 () (@var "B" tptp.nat))
% 151.11/151.91  (define @t599 () (_ tptp.member1474794996lle_fm @t482))
% 151.11/151.91  (define @t600 () (not (_ @t599 @t495)))
% 151.11/151.91  (define @t601 () (@var "C" tptp.produc696645085lle_fm))
% 151.11/151.91  (define @t602 () (_ tptp.member1474794996lle_fm @t601))
% 151.11/151.91  (define @t603 () (_ tptp.member1569366824lle_tv @t485))
% 151.11/151.91  (define @t604 () (not (_ @t603 @t500)))
% 151.11/151.91  (define @t605 () (@var "C" tptp.produc931990033lle_tv))
% 151.11/151.91  (define @t606 () (_ tptp.member1569366824lle_tv @t605))
% 151.11/151.91  (define @t607 () (@var "S3" tptp.set_Pr1986765409at_nat))
% 151.11/151.91  (define @t608 () (_ @t533 @t607))
% 151.11/151.91  (define @t609 () (@var "S3" tptp.set_Pr2014382200lle_tv))
% 151.11/151.91  (define @t610 () (_ @t536 @t609))
% 151.11/151.91  (define @t611 () (@var "S3" tptp.set_Pr1019238018lle_fm))
% 151.11/151.91  (define @t612 () (@var "R" tptp.set_Pr2061825550lle_tv))
% 151.11/151.91  (define @t613 () (@var "R" tptp.set_Pr1357842111at_nat))
% 151.11/151.91  (define @t614 () (_ (_ tptp.produc1710735575lle_fm (_ tptp.produc29804011lle_fm @t464)) (_ tptp.produc148705065lle_fm @t464)))
% 151.11/151.91  (define @t615 () (@list @t464))
% 151.11/151.91  (define @t616 () (_ (_ tptp.produc1680557635lle_tv (_ tptp.produc1636169559lle_tv @t470)) (_ tptp.produc547496597lle_tv @t470)))
% 151.11/151.91  (define @t617 () (@list @t470))
% 151.11/151.91  (define @t618 () (_ tptp.produc29804011lle_fm @t459))
% 151.11/151.91  (define @t619 () (_ tptp.produc1636169559lle_tv @t462))
% 151.11/151.91  (define @t620 () (@var "A" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t621 () (_ tptp.produc148705065lle_fm @t459))
% 151.11/151.91  (define @t622 () (_ tptp.produc547496597lle_tv @t462))
% 151.11/151.91  (define @t623 () (@list @t449 @t447))
% 151.11/151.91  (define @t624 () (@list @t454 @t452))
% 151.11/151.91  (define @t625 () (@var "T" tptp.produc696645085lle_fm))
% 151.11/151.91  (define @t626 () (@var "T" tptp.produc931990033lle_tv))
% 151.11/151.91  (define @t627 () (@var "P3" (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.paraco1604210848lle_fm Bool)))
% 151.11/151.91  (define @t628 () (@var "P" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t629 () (_ (_ tptp.produc1710735575lle_fm @t628) @t16))
% 151.11/151.91  (define @t630 () (@var "Q2" (-> tptp.paraco1604210848lle_fm Bool)))
% 151.11/151.91  (define @t631 () (@var "P3" (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) Bool)))
% 151.11/151.91  (define @t632 () (@var "Q" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t633 () (@var "P" (-> tptp.nat tptp.nat)))
% 151.11/151.91  (define @t634 () (_ (_ tptp.produc1680557635lle_tv @t633) @t632))
% 151.11/151.91  (define @t635 () (@var "P3" (-> (-> tptp.nat tptp.nat) Bool)))
% 151.11/151.91  (define @t636 () (@var "P3" (-> tptp.paraco1604210848lle_fm (-> tptp.list_char tptp.paraco1605129243lle_tv) Bool)))
% 151.11/151.91  (define @t637 () (@var "P3" (-> tptp.paraco1605129243lle_tv (-> tptp.nat tptp.nat) Bool)))
% 151.11/151.91  (define @t638 () (@var "Z" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t639 () (= @t159 (_ @t552 @t638)))
% 151.11/151.91  (define @t640 () (@list @t159 @t551 @t638))
% 151.11/151.91  (define @t641 () (@var "Z" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t642 () (= @t162 (_ @t556 @t641)))
% 151.11/151.91  (define @t643 () (@list @t162 @t555 @t641))
% 151.11/151.91  (define @t644 () (@var "A6" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t645 () (@var "A6" (-> tptp.nat tptp.nat)))
% 151.11/151.91  (define @t646 () (@var "B5" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t647 () (@var "B5" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t648 () (@var "R2" (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.set_Pr1019238018lle_fm)))
% 151.11/151.91  (define @t649 () (@var "Y6" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t650 () (@var "R2" (-> (-> tptp.nat tptp.nat) tptp.set_Pr2014382200lle_tv)))
% 151.11/151.91  (define @t651 () (@var "Y6" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t652 () (_ tptp.ord_less_eq_set_nat @t129))
% 151.11/151.91  (define @t653 () (_ @t652 @t592))
% 151.11/151.91  (define @t654 () (_ tptp.ord_le241064091lle_tv @t124))
% 151.11/151.91  (define @t655 () (_ @t654 @t595))
% 151.11/151.91  (define @t656 () (@var "S3" tptp.set_Pr2120184979lle_fm))
% 151.11/151.91  (define @t657 () (@var "R" tptp.set_Pr2120184979lle_fm))
% 151.11/151.91  (define @t658 () (@var "S3" tptp.set_Pr560526279lle_tv))
% 151.11/151.91  (define @t659 () (@var "R" tptp.set_Pr560526279lle_tv))
% 151.11/151.91  (define @t660 () (_ @t212 @t592))
% 151.11/151.91  (define @t661 () (_ @t220 @t595))
% 151.11/151.91  (define @t662 () (@var "C2" tptp.set_nat))
% 151.11/151.91  (define @t663 () (_ tptp.ord_less_eq_set_nat @t592))
% 151.11/151.91  (define @t664 () (@var "C2" tptp.set_Pa1764573435lle_tv))
% 151.11/151.91  (define @t665 () (_ tptp.ord_le241064091lle_tv @t595))
% 151.11/151.91  (define @t666 () (@var "P3" Bool))
% 151.11/151.91  (define @t667 () (@list @t153 @t64))
% 151.11/151.91  (define @t668 () (_ @t2 (_ (_ tptp.paraco69239110le_Con tptp.p1) tptp.p2)))
% 151.11/151.91  (define @t669 () (not (= @t668 @t3)))
% 151.11/151.91  (define @t670 () (@var "S" tptp.list_char))
% 151.11/151.91  (define @t671 () (@var "F2" (-> tptp.nat tptp.nat)))
% 151.11/151.91  (define @t672 () (lambda (@list @t671 @t143 @t670) (_ (_ tptp.paraco1147068288nge_tv @t671) (_ @t143 @t670))))
% 151.11/151.91  (define @t673 () (lambda (@list @t142) (forall (@list @t143) (= (_ @t144 @t142) @t1))))
% 151.11/151.91  (define @t674 () (lambda @t127 tptp.top_top_o))
% 151.11/151.91  (define @t675 () (lambda @t132 tptp.top_top_o))
% 151.11/151.91  (define @t676 () (@var "F2" (-> tptp.produc1647334210lle_tv tptp.produc1647334210lle_tv)))
% 151.11/151.91  (define @t677 () (@var "A3" tptp.set_Pr2014382200lle_tv))
% 151.11/151.91  (define @t678 () (lambda (@list @t676 @t677) (forall (@list @t175) (=> (_ (_ tptp.member1531318361lle_tv @t175) @t677) (forall (@list @t174) (=> (_ (_ tptp.member1531318361lle_tv @t174) @t677) (=> (= (_ @t676 @t175) (_ @t676 @t174)) @t176)))))))
% 151.11/151.91  (define @t679 () (@var "F2" (-> tptp.produc194167194tv_nat tptp.produc194167194tv_nat)))
% 151.11/151.91  (define @t680 () (@var "A3" tptp.set_Pr1725653840tv_nat))
% 151.11/151.91  (define @t681 () (lambda (@list @t679 @t680) (forall (@list @t190) (=> (_ (_ tptp.member737151281tv_nat @t190) @t680) (forall (@list @t189) (=> (_ (_ tptp.member737151281tv_nat @t189) @t680) (=> (= (_ @t679 @t190) (_ @t679 @t189)) @t191)))))))
% 151.11/151.91  (define @t682 () (@var "F2" (-> tptp.produc270694976lle_tv tptp.produc270694976lle_tv)))
% 151.11/151.91  (define @t683 () (@var "A3" tptp.set_Pr13445366lle_tv))
% 151.11/151.91  (define @t684 () (lambda (@list @t682 @t683) (forall (@list @t197) (=> (_ (_ tptp.member813679063lle_tv @t197) @t683) (forall (@list @t196) (=> (_ (_ tptp.member813679063lle_tv @t196) @t683) (=> (= (_ @t682 @t197) (_ @t682 @t196)) @t198)))))))
% 151.11/151.91  (define @t685 () (@var "F2" (-> tptp.product_prod_nat_nat tptp.product_prod_nat_nat)))
% 151.11/151.91  (define @t686 () (@var "A3" tptp.set_Pr1986765409at_nat))
% 151.11/151.91  (define @t687 () (lambda (@list @t685 @t686) (forall (@list @t204) (=> (_ (_ tptp.member701585322at_nat @t204) @t686) (forall (@list @t203) (=> (_ (_ tptp.member701585322at_nat @t203) @t686) (=> (= (_ @t685 @t204) (_ @t685 @t203)) @t205)))))))
% 151.11/151.91  (define @t688 () (@var "F2" (-> tptp.nat tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t689 () (@var "A3" tptp.set_nat))
% 151.11/151.91  (define @t690 () (_ (_ tptp.member_nat @t181) @t689))
% 151.11/151.91  (define @t691 () (_ @t131 @t689))
% 151.11/151.91  (define @t692 () (lambda (@list @t688 @t689) (forall @t132 (=> @t691 (forall @t574 (=> @t690 (=> (= (_ @t688 @t130) (_ @t688 @t181)) @t182)))))))
% 151.11/151.91  (define @t693 () (lambda (@list @t671 @t689) (forall @t132 (=> @t691 (forall @t574 (=> @t690 (=> (= (_ @t671 @t130) (_ @t671 @t181)) @t182)))))))
% 151.11/151.91  (define @t694 () (@var "F2" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t695 () (@var "A3" tptp.set_Pa1764573435lle_tv))
% 151.11/151.91  (define @t696 () (lambda (@list @t694 @t695) (forall @t127 (=> (_ @t126 @t695) (forall @t575 (=> (_ (_ tptp.member266900804lle_tv @t215) @t695) (=> (= (_ @t694 @t125) (_ @t694 @t215)) @t216)))))))
% 151.11/151.91  (define @t697 () (@var "F23" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t698 () (@var "F12" tptp.paraco1605129243lle_tv))
% 151.11/151.91  (define @t699 () (@var "Bool2" Bool))
% 151.11/151.91  (define @t700 () (lambda (@list @t698 @t697 @t699) (_ (_ (_ tptp.if_Par1134130401lle_tv @t699) @t698) @t697)))
% 151.11/151.91  (define @t701 () (@var "P2" tptp.produc1443694919lle_tv))
% 151.11/151.91  (define @t702 () (lambda (@list @t701) (_ (_ tptp.produc1710735575lle_fm (_ tptp.produc381314067lle_tv @t701)) (_ tptp.produc262413013lle_tv @t701))))
% 151.11/151.91  (define @t703 () (@var "P2" tptp.produc596913417at_nat))
% 151.11/151.91  (define @t704 () (lambda (@list @t703) (_ (_ tptp.produc1680557635lle_tv (_ tptp.produc500618325at_nat @t703)) (_ tptp.produc1589291287at_nat @t703))))
% 151.11/151.91  (define @t705 () (@var "BOUND_VARIABLE_11362" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t706 () (@var "BOUND_VARIABLE_11360" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t707 () (@const 0 (@ho-elim-sort (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm))))
% 151.11/151.91  (define @t708 () (@const 1 (-> (@ho-elim-sort (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm)) tptp.paraco1604210848lle_fm (@ho-elim-sort (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm)))))
% 151.11/151.91  (define @t709 () (@const 2 (-> (@ho-elim-sort (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm)) tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm)))
% 151.11/151.91  (define @t710 () (@var "BOUND_VARIABLE_19098" (@ho-elim-sort (-> tptp.list_char tptp.paraco1605129243lle_tv))))
% 151.11/151.91  (define @t711 () (@const 3 (@ho-elim-sort (-> (@ho-elim-sort (-> tptp.list_char tptp.paraco1605129243lle_tv)) tptp.paraco1604210848lle_fm tptp.paraco1605129243lle_tv))))
% 151.11/151.91  (define @t712 () (@const 4 (-> (@ho-elim-sort (-> (@ho-elim-sort (-> tptp.list_char tptp.paraco1605129243lle_tv)) tptp.paraco1604210848lle_fm tptp.paraco1605129243lle_tv)) (@ho-elim-sort (-> tptp.list_char tptp.paraco1605129243lle_tv)) (@ho-elim-sort (-> tptp.paraco1604210848lle_fm tptp.paraco1605129243lle_tv)))))
% 151.11/151.91  (define @t713 () (_ @t712 @t711 @t710))
% 151.11/151.91  (define @t714 () (@const 5 (-> (@ho-elim-sort (-> tptp.paraco1604210848lle_fm tptp.paraco1605129243lle_tv)) tptp.paraco1604210848lle_fm tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t715 () (_ @t714 @t713 (_ @t709 (_ @t708 @t707 @t706) @t705)))
% 151.11/151.91  (define @t716 () (@const 6 (@ho-elim-sort (-> Bool tptp.paraco1605129243lle_tv))))
% 151.11/151.91  (define @t717 () (@const 7 (-> (@ho-elim-sort (-> Bool tptp.paraco1605129243lle_tv)) Bool tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t718 () (_ @t717 @t716 false))
% 151.11/151.91  (define @t719 () (_ @t714 @t713 @t705))
% 151.11/151.91  (define @t720 () (_ @t717 @t716 true))
% 151.11/151.91  (define @t721 () (= @t720 @t719))
% 151.11/151.91  (define @t722 () (or @t721 (= @t715 @t718)))
% 151.11/151.91  (define @t723 () (_ @t714 @t713 @t706))
% 151.11/151.91  (define @t724 () (not @t721))
% 151.11/151.91  (define @t725 () (or @t724 (= @t723 @t715)))
% 151.11/151.91  (define @t726 () (and @t725 @t722))
% 151.11/151.91  (define @t727 () (= @t720 @t723))
% 151.11/151.91  (define @t728 () (or @t727 @t726))
% 151.11/151.91  (define @t729 () (not @t727))
% 151.11/151.91  (define @t730 () (or @t729 (= @t719 @t715)))
% 151.11/151.91  (define @t731 () (and @t730 @t728))
% 151.11/151.91  (define @t732 () (= @t719 @t723))
% 151.11/151.91  (define @t733 () (or @t732 @t731))
% 151.11/151.91  (define @t734 () (@list @t710 @t706 @t705))
% 151.11/151.91  (define @t735 () (forall @t734 @t733))
% 151.11/151.91  (define @t736 () (@var "BOUND_VARIABLE_11342" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t737 () (@var "BOUND_VARIABLE_19122" (@ho-elim-sort (-> tptp.list_char tptp.paraco1605129243lle_tv))))
% 151.11/151.91  (define @t738 () (_ @t712 @t711 @t737))
% 151.11/151.91  (define @t739 () (_ @t714 @t738 @t736))
% 151.11/151.91  (define @t740 () (@var "BOUND_VARIABLE_11344" tptp.paraco1604210848lle_fm))
% 151.11/151.91  (define @t741 () (_ @t714 @t738 (_ @t709 (_ @t708 @t707 @t736) @t740)))
% 151.11/151.91  (define @t742 () (_ @t714 @t738 @t740))
% 151.11/151.91  (define @t743 () (not (= @t742 @t739)))
% 151.11/151.91  (define @t744 () (or @t743 (= @t739 @t741)))
% 151.11/151.91  (define @t745 () (forall (@list @t737 @t736 @t740) @t744))
% 151.11/151.91  (define @t746 () (and @t745 @t735))
% 151.11/151.91  (define @t747 () (tptp.paraco1344940915le_Det false))
% 151.11/151.91  (define @t748 () (tptp.paraco69239110le_Con @t706 @t705))
% 151.11/151.91  (define @t749 () (@var "BOUND_VARIABLE_11358" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t750 () (tptp.paraco1325918602e_eval @t749 @t748))
% 151.11/151.91  (define @t751 () (tptp.paraco1325918602e_eval @t749 @t705))
% 151.11/151.91  (define @t752 () (tptp.paraco1344940915le_Det true))
% 151.11/151.91  (define @t753 () (= @t752 @t751))
% 151.11/151.91  (define @t754 () (tptp.paraco1325918602e_eval @t749 @t706))
% 151.11/151.91  (define @t755 () (or (not @t753) (= @t754 @t750)))
% 151.11/151.91  (define @t756 () (= @t752 @t754))
% 151.11/151.91  (define @t757 () (or (not @t756) (= @t751 @t750)))
% 151.11/151.91  (define @t758 () (= @t751 @t754))
% 151.11/151.91  (define @t759 () (@list @t749 @t706 @t705))
% 151.11/151.91  (define @t760 () (tptp.paraco69239110le_Con @t736 @t740))
% 151.11/151.91  (define @t761 () (@var "BOUND_VARIABLE_11340" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 151.11/151.91  (define @t762 () (tptp.paraco1325918602e_eval @t761 @t760))
% 151.11/151.91  (define @t763 () (tptp.paraco1325918602e_eval @t761 @t736))
% 151.11/151.91  (define @t764 () (tptp.paraco1325918602e_eval @t761 @t740))
% 151.11/151.91  (define @t765 () (@list @t761 @t736 @t740))
% 151.11/151.91  (define @t766 () (or @t753 (= @t747 @t750)))
% 151.11/151.91  (define @t767 () (and @t755 @t766))
% 151.11/151.91  (define @t768 () (or @t756 @t767))
% 151.11/151.91  (define @t769 () (and @t757 @t768))
% 151.11/151.91  (define @t770 () (or @t758 @t769))
% 151.11/151.91  (define @t771 () (_ (_ tptp.paraco69239110le_Con @t706) @t705))
% 151.11/151.91  (define @t772 () (_ tptp.paraco1325918602e_eval @t749))
% 151.11/151.91  (define @t773 () (_ @t772 @t771))
% 151.11/151.91  (define @t774 () (= @t15 @t773))
% 151.11/151.91  (define @t775 () (_ @t772 @t705))
% 151.11/151.91  (define @t776 () (= @t1 @t775))
% 151.11/151.91  (define @t777 () (or @t776 @t774))
% 151.11/151.91  (define @t778 () (_ @t772 @t706))
% 151.11/151.91  (define @t779 () (= @t778 @t773))
% 151.11/151.91  (define @t780 () (not @t776))
% 151.11/151.91  (define @t781 () (or @t780 @t779))
% 151.11/151.91  (define @t782 () (and @t781 @t777))
% 151.11/151.91  (define @t783 () (= @t1 @t778))
% 151.11/151.91  (define @t784 () (or @t783 @t782))
% 151.11/151.91  (define @t785 () (= @t775 @t773))
% 151.11/151.91  (define @t786 () (not @t783))
% 151.11/151.91  (define @t787 () (or @t786 @t785))
% 151.11/151.91  (define @t788 () (and @t787 @t784))
% 151.11/151.91  (define @t789 () (= @t775 @t778))
% 151.11/151.91  (define @t790 () (or @t789 @t788))
% 151.11/151.91  (define @t791 () (or @t776 (= @t773 @t15)))
% 151.11/151.91  (define @t792 () (or @t780 (= @t773 @t778)))
% 151.11/151.91  (define @t793 () (and @t792 @t791))
% 151.11/151.91  (define @t794 () (or @t783 @t793))
% 151.11/151.91  (define @t795 () (or @t786 (= @t773 @t775)))
% 151.11/151.91  (define @t796 () (and @t795 @t794))
% 151.11/151.91  (define @t797 () (or @t789 @t796))
% 151.11/151.91  (define @t798 () (forall @t759 @t797))
% 151.11/151.91  (define @t799 () (_ (_ tptp.paraco69239110le_Con @t736) @t740))
% 151.11/151.91  (define @t800 () (_ tptp.paraco1325918602e_eval @t761))
% 151.11/151.91  (define @t801 () (_ @t800 @t799))
% 151.11/151.91  (define @t802 () (_ @t800 @t736))
% 151.11/151.91  (define @t803 () (= @t802 @t801))
% 151.11/151.91  (define @t804 () (_ @t800 @t740))
% 151.11/151.91  (define @t805 () (= @t804 @t802))
% 151.11/151.91  (define @t806 () (not @t805))
% 151.11/151.91  (define @t807 () (or @t806 @t803))
% 151.11/151.91  (define @t808 () (or @t806 (= @t801 @t802)))
% 151.11/151.91  (define @t809 () (forall @t765 @t808))
% 151.11/151.91  (define @t810 () (= @t1 @t23))
% 151.11/151.91  (define @t811 () (not @t810))
% 151.11/151.91  (define @t812 () (= @t1 @t27))
% 151.11/151.91  (define @t813 () (not @t812))
% 151.11/151.91  (define @t814 () (= @t23 @t27))
% 151.11/151.91  (define @t815 () (or @t814 (and (or @t813 @t34) (or @t812 (and (or @t811 @t28) (or @t810 @t22))))))
% 151.11/151.91  (define @t816 () (forall @t42 @t815))
% 151.11/151.91  (define @t817 () (@list @t19 @t17 @t16))
% 151.11/151.91  (define @t818 () (not @t814))
% 151.11/151.91  (define @t819 () (or @t818 @t28))
% 151.11/151.91  (define @t820 () (forall @t42 @t819))
% 151.11/151.91  (define @t821 () (and @t820 @t816))
% 151.11/151.91  (define @t822 () (and (=> @t810 @t28) (=> @t811 @t22)))
% 151.11/151.91  (define @t823 () (and (=> @t812 @t34) (=> @t813 @t822)))
% 151.11/151.91  (define @t824 () (and (=> @t814 @t28) (=> @t818 @t823)))
% 151.11/151.91  (define @t825 () (@purify false))
% 151.11/151.91  (define @t826 () (_ @t717 @t716 @t825))
% 151.11/151.91  (define @t827 () (@const 8 (@ho-elim-sort (-> tptp.list_char tptp.paraco1605129243lle_tv))))
% 151.11/151.91  (define @t828 () (_ @t712 @t711 @t827))
% 151.11/151.91  (define @t829 () (_ @t714 @t828 (_ @t709 (_ @t708 @t707 tptp.p1) tptp.p2)))
% 151.11/151.91  (define @t830 () (= @t718 @t829))
% 151.11/151.91  (define @t831 () (@purify true))
% 151.11/151.91  (define @t832 () (_ @t717 @t716 @t831))
% 151.11/151.91  (define @t833 () (_ @t714 @t828 tptp.p2))
% 151.11/151.91  (define @t834 () (= @t720 @t833))
% 151.11/151.91  (define @t835 () (or @t834 @t830))
% 151.11/151.91  (define @t836 () (_ @t714 @t828 tptp.p1))
% 151.11/151.91  (define @t837 () (= @t836 @t829))
% 151.11/151.91  (define @t838 () (not @t834))
% 151.11/151.91  (define @t839 () (or @t838 @t837))
% 151.11/151.91  (define @t840 () (and @t839 @t835))
% 151.11/151.91  (define @t841 () (= @t720 @t836))
% 151.11/151.91  (define @t842 () (or @t841 @t840))
% 151.11/151.91  (define @t843 () (= @t833 @t829))
% 151.11/151.91  (define @t844 () (not @t841))
% 151.11/151.91  (define @t845 () (or @t844 @t843))
% 151.11/151.91  (define @t846 () (and @t845 @t842))
% 151.11/151.91  (define @t847 () (= @t836 @t833))
% 151.11/151.91  (define @t848 () (or @t847 @t846))
% 151.11/151.91  (define @t849 () (forall @t734 (or @t732 (and (or @t729 (= @t715 @t719)) (or @t727 (and (or @t724 (= @t715 @t723)) (or @t721 (= @t718 @t715))))))))
% 151.11/151.91  (define @t850 () (or @t838 (= @t829 @t836)))
% 151.11/151.91  (define @t851 () (and @t850 @t835))
% 151.11/151.91  (define @t852 () (or @t841 @t851))
% 151.11/151.91  (define @t853 () (or @t844 (= @t829 @t833)))
% 151.11/151.91  (define @t854 () (and @t853 @t852))
% 151.11/151.91  (define @t855 () (or (= @t833 @t836) @t854))
% 151.11/151.91  (define @t856 () (= @t833 @t832))
% 151.11/151.91  (define @t857 () (not @t856))
% 151.11/151.91  (define @t858 () (or @t857 @t837))
% 151.11/151.91  (define @t859 () (and @t858 (or @t856 (= @t829 @t826))))
% 151.11/151.91  (define @t860 () (= @t836 @t832))
% 151.11/151.91  (define @t861 () (or @t860 @t859))
% 151.11/151.91  (define @t862 () (and (or (not @t860) @t843) @t861))
% 151.11/151.91  (define @t863 () (or @t847 @t862))
% 151.11/151.91  (define @t864 () (@list true false))
% 151.11/151.91  (define @t865 () (not @t858))
% 151.11/151.91  (define @t866 () (not @t859))
% 151.11/151.91  (define @t867 () (not (= @t836 @t720)))
% 151.11/151.91  (define @t868 () (not @t861))
% 151.11/151.91  (assume @p1 @t4)
% 151.11/151.91  (assume @p2 (= @t5 @t1))
% 151.11/151.91  (assume @p3 @t6)
% 151.11/151.91  (assume @p4 (forall (@list @t10 @t8 @t9 @t7) (= (= @t11 (_ (_ tptp.paraco69239110le_Con @t9) @t7)) (and (= @t10 @t9) (= @t8 @t7)))))
% 151.11/151.91  (assume @p5 (not (= @t14 @t13)))
% 151.11/151.91  (assume @p6 @t43)
% 151.11/151.91  (assume @p7 (= @t13 (_ @t44 @t5)))
% 151.11/151.91  (assume @p8 (= @t14 (_ @t44 @t3)))
% 151.11/151.91  (assume @p9 (not (= @t14 @t1)))
% 151.11/151.91  (assume @p10 (forall (@list @t46 @t45) (= (= @t47 (_ tptp.paraco1344940915le_Det @t45)) (= @t46 @t45))))
% 151.11/151.91  (assume @p11 (forall (@list @t17 @t16) (= (_ tptp.paraco327635598_valid @t18) (and @t48 (_ tptp.paraco327635598_valid @t16)))))
% 151.11/151.91  (assume @p12 (forall (@list @t49 @t17 @t16) (= (_ @t50 @t18) (and @t51 (_ @t50 @t16)))))
% 151.11/151.91  (assume @p13 (forall (@list @t10 @t8) (not (= tptp.paraco367965286_Truth @t11))))
% 151.11/151.91  (assume @p14 (forall (@list @t10 @t8 @t53 @t52) (not (= @t11 @t54))))
% 151.11/151.91  (assume @p15 (forall (@list @t53 @t52 @t56 @t55) (= (= @t54 (_ (_ tptp.paraco1389086619le_Eql @t56) @t55)) (and (= @t53 @t56) (= @t52 @t55)))))
% 151.11/151.91  (assume @p16 (forall (@list @t53 @t52) (not (= tptp.paraco367965286_Truth @t54))))
% 151.11/151.91  (assume @p17 (forall (@list @t59 @t57) (= (_ @t60 @t58) @t58)))
% 151.11/151.91  (assume @p18 (forall (@list @t49 @t17) (=> (not @t51) (not @t48))))
% 151.11/151.91  (assume @p19 (forall (@list @t17 @t49) (=> @t48 @t51)))
% 151.11/151.91  (assume @p20 (forall @t42 (= @t61 (_ tptp.paraco1344940915le_Det @t37))))
% 151.11/151.91  (assume @p21 (forall @t42 (and (=> @t37 (= @t61 @t1)) (=> @t38 (= @t61 @t15)))))
% 151.11/151.91  (assume @p22 (forall (@list @t19) (= (_ @t20 tptp.paraco367965286_Truth) @t1)))
% 151.11/151.91  (assume @p23 (forall @t76 (=> @t75 (=> (forall @t74 (=> @t73 (not @t72))) (not (forall @t69 (=> @t68 (not @t65))))))))
% 151.11/151.91  (assume @p24 (forall (@list @t77 @t78 @t46) (= (_ @t79 @t47) (_ @t77 @t46))))
% 151.11/151.91  (assume @p25 (forall @t83 (and (=> @t81 (= @t80 @t1)) (=> @t82 (and (=> @t31 (= @t80 @t15)) (=> @t32 (= @t80 @t27)))))))
% 151.11/151.91  (assume @p26 (_ (_ tptp.inj_on_nat_nat tptp.f) tptp.top_top_set_nat))
% 151.11/151.91  (assume @p27 (forall (@list @t59 @t84) (= (_ @t60 (_ tptp.paraco793048302_Indet @t84)) (_ tptp.paraco793048302_Indet (_ @t59 @t84)))))
% 151.11/151.91  (assume @p28 (forall (@list @t86 @t85) (not (= tptp.paraco367965286_Truth @t87))))
% 151.11/151.91  (assume @p29 (forall (@list @t89 @t88) (= (= @t90 (_ tptp.paraco445776468le_Neg @t88)) (= @t89 @t88))))
% 151.11/151.91  (assume @p30 (forall (@list @t86 @t85 @t92 @t91) (= (= @t87 (_ (_ tptp.paraco1745535428le_Eql @t92) @t91)) (and (= @t86 @t92) (= @t85 @t91)))))
% 151.11/151.91  (assume @p31 (forall (@list @t94 @t93) (= (= @t95 (_ tptp.paraco793048302_Indet @t93)) (= @t94 @t93))))
% 151.11/151.91  (assume @p32 (forall (@list @t89 @t86 @t85) (not (= @t90 @t87))))
% 151.11/151.91  (assume @p33 (forall (@list @t77 @t78 @t94) (= (_ @t79 @t95) (_ @t78 @t94))))
% 151.11/151.91  (assume @p34 (forall (@list @t96 @t97) (= (_ (_ tptp.member1474794996lle_fm @t96) (_ tptp.collec835549234lle_fm @t97)) (_ @t97 @t96))))
% 151.11/151.91  (assume @p35 (forall (@list @t98 @t99) (= (_ (_ tptp.member146333935lle_tv @t98) (_ tptp.collec1102043437lle_tv @t99)) (_ @t99 @t98))))
% 151.11/151.91  (assume @p36 (forall (@list @t100 @t101) (= (_ (_ tptp.member1569366824lle_tv @t100) (_ tptp.collec1624074086lle_tv @t101)) (_ @t101 @t100))))
% 151.11/151.91  (assume @p37 (forall (@list @t102 @t103) (= (_ (_ tptp.member112824072at_nat @t102) (_ tptp.collec791369802at_nat @t103)) (_ @t103 @t102))))
% 151.11/151.91  (assume @p38 (forall (@list @t104 @t105) (= (_ @t107 @t106) (_ @t105 @t104))))
% 151.11/151.91  (assume @p39 (forall (@list @t108 @t109) (= (_ @t111 @t110) (_ @t109 @t108))))
% 151.11/151.91  (assume @p40 (forall @t114 (= (_ tptp.collec835549234lle_fm (lambda (@list @t113) (_ (_ tptp.member1474794996lle_fm @t113) @t112))) @t112)))
% 151.11/151.91  (assume @p41 (forall @t117 (= (_ tptp.collec1102043437lle_tv (lambda (@list @t116) (_ (_ tptp.member146333935lle_tv @t116) @t115))) @t115)))
% 151.11/151.91  (assume @p42 (forall @t120 (= (_ tptp.collec1624074086lle_tv (lambda (@list @t119) (_ (_ tptp.member1569366824lle_tv @t119) @t118))) @t118)))
% 151.11/151.91  (assume @p43 (forall @t123 (= (_ tptp.collec791369802at_nat (lambda (@list @t122) (_ (_ tptp.member112824072at_nat @t122) @t121))) @t121)))
% 151.11/151.91  (assume @p44 (forall @t128 (= (_ tptp.collec1111687558lle_tv (lambda @t127 (_ @t126 @t124))) @t124)))
% 151.11/151.91  (assume @p45 (forall @t133 (= (_ tptp.collect_nat (lambda @t132 (_ @t131 @t129))) @t129)))
% 151.11/151.91  (assume @p46 (forall (@list @t105 @t134) (=> (forall @t136 (= (_ @t105 @t135) (_ @t134 @t135))) (= @t106 (_ tptp.collec1111687558lle_tv @t134)))))
% 151.11/151.91  (assume @p47 (forall (@list @t109 @t137) (=> (forall @t139 (= (_ @t109 @t138) (_ @t137 @t138))) (= @t110 (_ tptp.collect_nat @t137)))))
% 151.11/151.91  (assume @p48 (forall @t42 (and (=> @t37 (= @t140 @t1)) (=> @t38 (and (=> @t31 (= @t140 @t23)) (=> @t32 (and (=> @t24 (= @t140 @t27)) (=> @t25 (and (=> @t81 (= @t140 (_ @t20 (_ tptp.paraco445776468le_Neg @t16)))) (=> @t82 (and (=> @t141 (= @t140 @t80)) (=> (not @t141) (= @t140 @t15)))))))))))))
% 151.11/151.91  (assume @p49 (= tptp.paraco1325918602e_eval (lambda (@list @t143 @t142) (_ @t144 (_ tptp.paraco445776468le_Neg (_ tptp.paraco445776468le_Neg @t142))))))
% 151.11/151.91  (assume @p50 (forall (@list @t89 @t10 @t8) (not (= @t90 @t11))))
% 151.11/151.91  (assume @p51 (forall (@list @t105 @t145) (=> (_ @t105 @t1) (=> (_ @t105 @t15) (=> (forall @t69 (_ @t105 @t66)) (_ @t105 @t145))))))
% 151.11/151.91  (assume @p52 (forall (@list @t148 @t147 @t146) (=> (forall @t152 (_ @t150 @t71)) (=> (forall @t151 (_ @t150 @t66)) (_ (_ @t148 @t147) @t146)))))
% 151.11/151.91  (assume @p53 (forall @t154 (=> (not (= @t153 @t1)) (=> (not (= @t153 @t15)) (not (forall @t69 (not (= @t153 @t66))))))))
% 151.11/151.91  (assume @p54 (forall (@list @t64) (=> (forall (@list @t156) (not (= @t64 (_ tptp.paraco1344940915le_Det @t156)))) (not (forall (@list @t155) (not (= @t64 (_ tptp.paraco793048302_Indet @t155))))))))
% 151.11/151.91  (assume @p55 (forall (@list @t105 @t157) (=> (forall (@list @t158) (_ @t105 (_ tptp.paraco1344940915le_Det @t158))) (=> (forall @t139 (_ @t105 (_ tptp.paraco793048302_Indet @t138))) (_ @t105 @t157)))))
% 151.11/151.91  (assume @p56 (forall (@list @t46 @t94) (not (= @t47 @t95))))
% 151.11/151.91  (assume @p57 (forall (@list @t89 @t53 @t52) (not (= @t90 @t54))))
% 151.11/151.91  (assume @p58 (forall (@list @t89) (not (= tptp.paraco367965286_Truth @t90))))
% 151.11/151.91  (assume @p59 (forall (@list @t10 @t8 @t86 @t85) (not (= @t11 @t87))))
% 151.11/151.91  (assume @p60 (forall (@list @t53 @t52 @t86 @t85) (not (= @t54 @t87))))
% 151.11/151.91  (assume @p61 (forall @t160 (_ (_ tptp.member1474794996lle_fm @t159) tptp.top_to775056195lle_fm)))
% 151.11/151.91  (assume @p62 (forall (@list @t161) (_ (_ tptp.member146333935lle_tv @t161) tptp.top_to138697918lle_tv)))
% 151.11/151.91  (assume @p63 (forall @t163 (_ (_ tptp.member1569366824lle_tv @t162) tptp.top_to449985143lle_tv)))
% 151.11/151.91  (assume @p64 (forall (@list @t164) (_ (_ tptp.member112824072at_nat @t164) tptp.top_to1541413903at_nat)))
% 151.11/151.91  (assume @p65 (forall (@list @t165) (_ @t166 tptp.top_to975729152tv_nat)))
% 151.11/151.91  (assume @p66 (forall (@list @t167) (_ @t168 tptp.top_to1411004326lle_tv)))
% 151.11/151.91  (assume @p67 (forall (@list @t169) (_ @t170 tptp.top_to1555900337at_nat)))
% 151.11/151.91  (assume @p68 (forall (@list @t171) (_ @t172 tptp.top_top_set_nat)))
% 151.11/151.91  (assume @p69 (forall @t154 (_ @t173 tptp.top_to1057771083lle_tv)))
% 151.11/151.91  (assume @p70 (forall @t83 (= @t80 (_ (_ (_ tptp.paraco2051596139lle_tv (_ (_ tptp.produc234482697lle_tv @t15) @t1)) tptp.paraco793048302_Indet) @t27))))
% 151.11/151.91  (assume @p71 (forall @t180 (= @t179 (forall (@list @t175 @t174) (=> (= (_ @t177 @t175) (_ @t177 @t174)) @t176)))))
% 151.11/151.91  (assume @p72 (forall @t188 (= @t187 (forall @t185 (=> (= @t184 (_ @t183 @t181)) @t182)))))
% 151.11/151.91  (assume @p73 (forall @t195 (= @t194 (forall (@list @t190 @t189) (=> (= (_ @t192 @t190) (_ @t192 @t189)) @t191)))))
% 151.11/151.91  (assume @p74 (forall @t202 (= @t201 (forall (@list @t197 @t196) (=> (= (_ @t199 @t197) (_ @t199 @t196)) @t198)))))
% 151.11/151.91  (assume @p75 (forall @t209 (= @t208 (forall (@list @t204 @t203) (=> (= (_ @t206 @t204) (_ @t206 @t203)) @t205)))))
% 151.11/151.91  (assume @p76 (forall @t214 (= @t213 (forall @t185 (=> (= @t211 @t210) @t182)))))
% 151.11/151.91  (assume @p77 (forall @t222 (= @t221 (forall (@list @t125 @t215) (=> (= @t219 @t218) @t216)))))
% 151.11/151.91  (assume @p78 (forall @t228 (=> @t179 @t227)))
% 151.11/151.91  (assume @p79 (forall @t233 (=> @t187 @t232)))
% 151.11/151.91  (assume @p80 (forall @t238 (=> @t194 @t237)))
% 151.11/151.91  (assume @p81 (forall @t243 (=> @t201 @t242)))
% 151.11/151.91  (assume @p82 (forall @t248 (=> @t208 @t247)))
% 151.11/151.91  (assume @p83 (forall @t252 (=> @t213 @t251)))
% 151.11/151.91  (assume @p84 (forall @t258 (=> @t221 @t257)))
% 151.11/151.91  (assume @p85 (forall @t180 (=> (forall @t262 @t261) @t179)))
% 151.11/151.91  (assume @p86 (forall @t188 (=> (forall @t267 @t266) @t187)))
% 151.11/151.91  (assume @p87 (forall @t195 (=> (forall @t271 @t270) @t194)))
% 151.11/151.91  (assume @p88 (forall @t202 (=> (forall @t275 @t274) @t201)))
% 151.11/151.91  (assume @p89 (forall @t209 (=> (forall @t279 @t278) @t208)))
% 151.11/151.91  (assume @p90 (forall @t214 (=> (forall @t267 @t281) @t213)))
% 151.11/151.91  (assume @p91 (forall @t222 (=> (forall @t285 @t284) @t221)))
% 151.11/151.91  (assume @p92 (forall @t228 (=> @t179 (=> @t226 @t225))))
% 151.11/151.91  (assume @p93 (forall @t233 (=> @t187 (=> @t231 @t230))))
% 151.11/151.91  (assume @p94 (forall @t238 (=> @t194 (=> @t236 @t235))))
% 151.11/151.91  (assume @p95 (forall @t243 (=> @t201 (=> @t241 @t240))))
% 151.11/151.91  (assume @p96 (forall @t248 (=> @t208 (=> @t246 @t245))))
% 151.11/151.91  (assume @p97 (forall @t252 (=> @t213 (=> @t250 @t230))))
% 151.11/151.91  (assume @p98 (forall @t258 (=> @t221 (=> @t256 @t253))))
% 151.11/151.91  (assume @p99 (= tptp.top_to975729152tv_nat (_ tptp.collec848462447tv_nat tptp.top_to900819589_nat_o)))
% 151.11/151.91  (assume @p100 (= tptp.top_to1411004326lle_tv (_ tptp.collec924990229lle_tv tptp.top_to1889334367e_tv_o)))
% 151.11/151.91  (assume @p101 (= tptp.top_to1555900337at_nat (_ tptp.collec7649004at_nat tptp.top_to632227436_nat_o)))
% 151.11/151.91  (assume @p102 (= tptp.top_top_set_nat (_ tptp.collect_nat tptp.top_top_nat_o)))
% 151.11/151.91  (assume @p103 (= tptp.top_to1057771083lle_tv (_ tptp.collec1111687558lle_tv tptp.top_to1299250770e_tv_o)))
% 151.11/151.91  (assume @p104 (forall @t214 (=> @t213 (_ (_ tptp.inj_on772319074lle_tv @t60) tptp.top_to1057771083lle_tv))))
% 151.11/151.91  (assume @p105 (forall @t114 (=> (forall @t288 (_ @t287 @t112)) (= tptp.top_to775056195lle_fm @t112))))
% 151.11/151.91  (assume @p106 (forall @t117 (=> (forall @t291 (_ @t290 @t115)) (= tptp.top_to138697918lle_tv @t115))))
% 151.11/151.91  (assume @p107 (forall @t120 (=> (forall @t294 (_ @t293 @t118)) (= tptp.top_to449985143lle_tv @t118))))
% 151.11/151.91  (assume @p108 (forall @t123 (=> (forall @t297 (_ @t296 @t121)) (= tptp.top_to1541413903at_nat @t121))))
% 151.11/151.91  (assume @p109 (forall (@list @t298) (=> (forall @t301 @t300) (= tptp.top_to975729152tv_nat @t298))))
% 151.11/151.91  (assume @p110 (forall (@list @t302) (=> (forall @t305 @t304) (= tptp.top_to1411004326lle_tv @t302))))
% 151.11/151.91  (assume @p111 (forall (@list @t306) (=> (forall @t309 @t308) (= tptp.top_to1555900337at_nat @t306))))
% 151.11/151.91  (assume @p112 (forall @t133 (=> (forall @t139 @t311) (= tptp.top_top_set_nat @t129))))
% 151.11/151.91  (assume @p113 (forall @t128 (=> (forall @t136 @t313) (= tptp.top_to1057771083lle_tv @t124))))
% 151.11/151.91  (assume @p114 (exists @t288 (_ @t287 tptp.top_to775056195lle_fm)))
% 151.11/151.91  (assume @p115 (exists @t291 (_ @t290 tptp.top_to138697918lle_tv)))
% 151.11/151.91  (assume @p116 (exists @t294 (_ @t293 tptp.top_to449985143lle_tv)))
% 151.11/151.91  (assume @p117 (exists @t297 (_ @t296 tptp.top_to1541413903at_nat)))
% 151.11/151.91  (assume @p118 (exists @t301 (_ @t299 tptp.top_to975729152tv_nat)))
% 151.11/151.91  (assume @p119 (exists @t305 (_ @t303 tptp.top_to1411004326lle_tv)))
% 151.11/151.91  (assume @p120 (exists @t309 (_ @t307 tptp.top_to1555900337at_nat)))
% 151.11/151.91  (assume @p121 (exists @t139 (_ @t310 tptp.top_top_set_nat)))
% 151.11/151.91  (assume @p122 (exists @t136 (_ @t312 tptp.top_to1057771083lle_tv)))
% 151.11/151.91  (assume @p123 (forall @t318 (=> @t317 (=> @t226 (=> @t316 (=> @t315 @t225))))))
% 151.11/151.91  (assume @p124 (forall @t322 (=> @t321 (=> @t236 (=> @t320 (=> @t319 @t235))))))
% 151.11/151.91  (assume @p125 (forall @t326 (=> @t325 (=> @t241 (=> @t324 (=> @t323 @t240))))))
% 151.11/151.91  (assume @p126 (forall @t330 (=> @t329 (=> @t246 (=> @t328 (=> @t327 @t245))))))
% 151.11/151.91  (assume @p127 (forall @t336 (=> @t335 (=> @t231 @t334))))
% 151.11/151.91  (assume @p128 (forall @t338 (=> @t337 (=> @t250 @t334))))
% 151.11/151.91  (assume @p129 (forall @t343 (=> @t342 (=> @t256 (=> @t341 (=> @t340 @t253))))))
% 151.11/151.91  (assume @p130 (forall (@list @t314 @t177) (=> (forall @t262 (=> (_ (_ tptp.member1531318361lle_tv @t260) @t314) (=> (_ (_ tptp.member1531318361lle_tv @t259) @t314) @t261))) @t317)))
% 151.11/151.91  (assume @p131 (forall (@list @t298 @t192) (=> (forall @t271 (=> @t300 (=> (_ (_ tptp.member737151281tv_nat @t268) @t298) @t270))) @t321)))
% 151.11/151.91  (assume @p132 (forall (@list @t302 @t199) (=> (forall @t275 (=> @t304 (=> (_ (_ tptp.member813679063lle_tv @t272) @t302) @t274))) @t325)))
% 151.11/151.91  (assume @p133 (forall (@list @t306 @t206) (=> (forall @t279 (=> @t308 (=> (_ (_ tptp.member701585322at_nat @t276) @t306) @t278))) @t329)))
% 151.11/151.91  (assume @p134 (forall (@list @t129 @t183) (=> (forall @t267 (=> @t311 (=> @t344 @t266))) @t335)))
% 151.11/151.91  (assume @p135 (forall (@list @t129 @t59) (=> (forall @t267 (=> @t311 (=> @t344 @t281))) @t337)))
% 151.11/151.91  (assume @p136 (forall (@list @t124 @t217) (=> (forall @t285 (=> @t313 (=> (_ (_ tptp.member266900804lle_tv @t282) @t124) @t284))) @t342)))
% 151.11/151.91  (assume @p137 (forall (@list @t314 @t177 @t345) (=> (forall (@list @t346) (=> (_ (_ tptp.member1531318361lle_tv @t346) @t314) (= (_ @t177 @t346) (_ @t345 @t346)))) (= @t317 (_ (_ tptp.inj_on2112487900lle_tv @t345) @t314)))))
% 151.11/151.91  (assume @p138 (forall (@list @t298 @t192 @t347) (=> (forall (@list @t348) (=> (_ (_ tptp.member737151281tv_nat @t348) @t298) (= (_ @t192 @t348) (_ @t347 @t348)))) (= @t321 (_ (_ tptp.inj_on552895452tv_nat @t347) @t298)))))
% 151.11/151.91  (assume @p139 (forall (@list @t302 @t199 @t349) (=> (forall (@list @t350) (=> (_ (_ tptp.member813679063lle_tv @t350) @t302) (= (_ @t199 @t350) (_ @t349 @t350)))) (= @t325 (_ (_ tptp.inj_on1745913142lle_tv @t349) @t302)))))
% 151.11/151.91  (assume @p140 (forall (@list @t306 @t206 @t351) (=> (forall (@list @t352) (=> (_ (_ tptp.member701585322at_nat @t352) @t306) (= (_ @t206 @t352) (_ @t351 @t352)))) (= @t329 (_ (_ tptp.inj_on26176689at_nat @t351) @t306)))))
% 151.11/151.91  (assume @p141 (forall (@list @t129 @t183 @t353) (=> (forall @t356 (=> @t355 (= (_ @t183 @t354) (_ @t353 @t354)))) (= @t335 (_ (_ tptp.inj_on1955349912lle_tv @t353) @t129)))))
% 151.11/151.91  (assume @p142 (forall (@list @t129 @t59 @t357) (=> (forall @t356 (=> @t355 (= (_ @t59 @t354) (_ @t357 @t354)))) (= @t337 @t359))))
% 151.11/151.91  (assume @p143 (forall (@list @t124 @t217 @t360) (=> (forall (@list @t363) (=> (_ (_ tptp.member266900804lle_tv @t363) @t124) (= (_ @t217 @t363) (_ @t360 @t363)))) (= @t342 @t362))))
% 151.11/151.91  (assume @p144 (forall @t318 (=> @t317 (=> @t316 (=> @t315 @t227)))))
% 151.11/151.91  (assume @p145 (forall @t322 (=> @t321 (=> @t320 (=> @t319 @t237)))))
% 151.11/151.91  (assume @p146 (forall @t326 (=> @t325 (=> @t324 (=> @t323 @t242)))))
% 151.11/151.91  (assume @p147 (forall @t330 (=> @t329 (=> @t328 (=> @t327 @t247)))))
% 151.11/151.91  (assume @p148 (forall @t336 (=> @t335 (=> @t333 (=> @t332 @t232)))))
% 151.11/151.91  (assume @p149 (forall @t338 (=> @t337 (=> @t333 (=> @t332 @t251)))))
% 151.11/151.91  (assume @p150 (forall @t343 (=> @t342 (=> @t341 (=> @t340 @t257)))))
% 151.11/151.91  (assume @p151 (forall @t318 (=> @t317 (=> (not @t225) (=> @t316 (=> @t315 (not @t226)))))))
% 151.11/151.91  (assume @p152 (forall @t322 (=> @t321 (=> (not @t235) (=> @t320 (=> @t319 (not @t236)))))))
% 151.11/151.91  (assume @p153 (forall @t326 (=> @t325 (=> (not @t240) (=> @t324 (=> @t323 (not @t241)))))))
% 151.11/151.91  (assume @p154 (forall @t330 (=> @t329 (=> (not @t245) (=> @t328 (=> @t327 (not @t246)))))))
% 151.11/151.91  (assume @p155 (forall @t336 (=> @t335 (=> @t364 (=> @t333 (=> @t332 (not @t231)))))))
% 151.11/151.91  (assume @p156 (forall @t338 (=> @t337 (=> @t364 (=> @t333 (=> @t332 (not @t250)))))))
% 151.11/151.91  (assume @p157 (forall @t343 (=> @t342 (=> (not @t253) (=> @t341 (=> @t340 (not @t256)))))))
% 151.11/151.91  (assume @p158 (forall @t367 (=> (forall @t139 (=> @t311 @t366)) @t337)))
% 151.11/151.91  (assume @p159 (forall @t370 (=> (forall @t136 (=> @t313 @t369)) @t342)))
% 151.11/151.91  (assume @p160 (forall (@list @t372 @t371) (=> (forall (@list @t380) (_ @t372 (_ tptp.paraco1480028776le_Pro @t380))) (=> @t379 (=> (forall (@list @t378) (=> (_ @t372 @t378) (_ @t372 (_ tptp.paraco445776468le_Neg @t378)))) (=> (forall @t377 (=> @t376 (=> @t375 (_ @t372 (_ (_ tptp.paraco69239110le_Con @t374) @t373))))) (=> (forall @t377 (=> @t376 (=> @t375 (_ @t372 (_ (_ tptp.paraco1389086619le_Eql @t374) @t373))))) (=> (forall @t377 (=> @t376 (=> @t375 (_ @t372 (_ (_ tptp.paraco1745535428le_Eql @t374) @t373))))) (_ @t372 @t371)))))))))
% 151.11/151.91  (assume @p161 (forall (@list @t383) (=> (forall (@list @t389) (not (= @t383 (_ tptp.paraco1480028776le_Pro @t389)))) (=> (not (= @t383 tptp.paraco367965286_Truth)) (=> (forall (@list @t388) (not (= @t383 (_ tptp.paraco445776468le_Neg @t388)))) (=> (forall (@list @t387 @t386) (not (= @t383 (_ (_ tptp.paraco69239110le_Con @t387) @t386)))) (=> (forall (@list @t385 @t384) (not (= @t383 (_ (_ tptp.paraco1389086619le_Eql @t385) @t384)))) (not (forall (@list @t382 @t381) (not (= @t383 (_ (_ tptp.paraco1745535428le_Eql @t382) @t381))))))))))))
% 151.11/151.91  (assume @p162 (forall (@list @t393) (=> (not (= @t393 tptp.paraco367965286_Truth)) (=> (forall @t401 (not (= @t393 @t400))) (=> (forall @t398 (not (= @t393 @t397))) (=> (forall @t394 (not (= @t393 @t396))) (=> (forall @t394 (not (= @t393 @t395))) (not (forall @t394 (not (= @t393 @t392)))))))))))
% 151.11/151.91  (assume @p163 (forall (@list @t372 @t402) (=> @t379 (=> (forall @t401 (_ @t372 @t400)) (=> (forall @t398 (=> @t404 (_ @t372 @t397))) (=> (forall @t394 (=> @t404 (=> @t403 (_ @t372 @t396)))) (=> (forall @t394 (=> @t404 (=> @t403 (_ @t372 @t395)))) (=> (forall @t394 (=> @t404 (=> @t403 (_ @t372 @t392)))) (_ @t372 @t402)))))))))
% 151.11/151.91  (assume @p164 (forall @t408 (= (_ @t407 false) @t405)))
% 151.11/151.91  (assume @p165 (forall @t408 (= (_ @t407 true) @t406)))
% 151.11/151.91  (assume @p166 (forall @t415 (= @t414 (and (=> @t410 @t412) (=> @t411 @t409)))))
% 151.11/151.91  (assume @p167 (forall (@list @t417 @t416) (= (= @t418 (_ tptp.paraco1480028776le_Pro @t416)) (= @t417 @t416))))
% 151.11/151.91  (assume @p168 (forall (@list @t19 @t419) (= (_ @t20 (_ tptp.paraco1480028776le_Pro @t419)) (_ @t19 @t419))))
% 151.11/151.91  (assume @p169 (forall (@list @t417 @t89) (not (= @t418 @t90))))
% 151.11/151.91  (assume @p170 (forall (@list @t417 @t10 @t8) (not (= @t418 @t11))))
% 151.11/151.91  (assume @p171 (forall (@list @t417 @t86 @t85) (not (= @t418 @t87))))
% 151.11/151.91  (assume @p172 (forall (@list @t417 @t53 @t52) (not (= @t418 @t54))))
% 151.11/151.91  (assume @p173 (forall (@list @t417) (not (= @t418 tptp.paraco367965286_Truth))))
% 151.11/151.91  (assume @p174 (forall @t415 (= @t414 (not (or (and @t410 (not @t412)) (and @t411 (not @t409)))))))
% 151.11/151.91  (assume @p175 (forall (@list @t420 @t406 @t405 @t410) (= (_ @t420 @t413) (_ (_ (_ tptp.produc234482697lle_tv (_ @t420 @t406)) (_ @t420 @t405)) @t410))))
% 151.11/151.91  (assume @p176 (= tptp.top_top_nat_o (lambda @t132 (_ @t131 tptp.top_top_set_nat))))
% 151.11/151.91  (assume @p177 (= tptp.top_to1299250770e_tv_o (lambda @t127 (_ @t126 tptp.top_to1057771083lle_tv))))
% 151.11/151.91  (assume @p178 (forall @t160 (=> (forall (@list @t421 @t399) (not (= @t159 (_ @t422 @t400)))) (=> (forall (@list @t421) (not (= @t159 (_ @t422 tptp.paraco367965286_Truth)))) (=> (forall (@list @t421 @t391) (not (= @t159 (_ @t422 @t397)))) (=> (forall @t423 (not (= @t159 (_ @t422 @t396)))) (=> (forall @t423 (not (= @t159 (_ @t422 @t395)))) (not (forall @t423 (not (= @t159 (_ @t422 @t392))))))))))))
% 151.11/151.91  (assume @p179 (forall @t434 (= @t433 (and @t429 @t426))))
% 151.11/151.91  (assume @p180 (forall @t445 (= @t444 (and @t440 @t437))))
% 151.11/151.91  (assume @p181 (forall (@list @t449 @t447 @t448 @t446) (= (= @t450 (_ (_ tptp.produc1710735575lle_fm @t448) @t446)) (and (= @t449 @t448) (= @t447 @t446)))))
% 151.11/151.91  (assume @p182 (forall (@list @t454 @t452 @t453 @t451) (= (= @t455 (_ (_ tptp.produc1680557635lle_tv @t453) @t451)) (and (= @t454 @t453) (= @t452 @t451)))))
% 151.11/151.91  (assume @p183 (forall (@list @t457 @t456 @t383) (= (_ (_ tptp.produc1942165868lle_fm @t457) @t459) (_ (_ tptp.produc1710735575lle_fm (_ @t457 @t456)) @t383))))
% 151.11/151.91  (assume @p184 (forall (@list @t460 @t63 @t64) (= (_ (_ tptp.produc939316703lle_tv @t460) @t462) (_ (_ tptp.produc1680557635lle_tv (_ @t460 @t63)) @t64))))
% 151.11/151.91  (assume @p185 (forall (@list @t463 @t456 @t383) (= (_ (_ tptp.produc1807466521lle_tv @t463) @t459) (_ @t458 (_ @t463 @t383)))))
% 151.11/151.91  (assume @p186 (forall (@list @t217 @t63 @t64) (= (_ (_ tptp.produc109093078at_nat @t217) @t462) (_ @t461 @t254))))
% 151.11/151.91  (assume @p187 (forall (@list @t97 @t464) (=> @t469 (_ @t97 @t464))))
% 151.11/151.91  (assume @p188 (forall (@list @t101 @t470) (=> @t475 (_ @t101 @t470))))
% 151.11/151.91  (assume @p189 (forall (@list @t476) (not (forall @t468 (not (= @t476 @t467))))))
% 151.11/151.91  (assume @p190 (forall (@list @t477) (not (forall @t474 (not (= @t477 @t473))))))
% 151.11/151.91  (assume @p191 (forall @t434 (=> @t433 (not (=> @t429 (not @t426))))))
% 151.11/151.91  (assume @p192 (forall @t445 (=> @t444 (not (=> @t440 (not @t437))))))
% 151.11/151.91  (assume @p193 (forall (@list @t97 @t478) (=> @t469 (_ @t97 @t478))))
% 151.11/151.91  (assume @p194 (forall (@list @t101 @t479) (=> @t475 (_ @t101 @t479))))
% 151.11/151.91  (assume @p195 (forall (@list @t478) (exists @t483 (= @t478 @t482))))
% 151.11/151.91  (assume @p196 (forall (@list @t479) (exists @t486 (= @t479 @t485))))
% 151.11/151.91  (assume @p197 (forall (@list @t488 @t487) (=> @t490 (=> @t489 (_ (_ tptp.inj_on26176689at_nat (_ (_ tptp.produc505105722at_nat @t488) @t487)) tptp.top_to1555900337at_nat)))))
% 151.11/151.91  (assume @p198 (forall (@list @t488 @t491) (=> @t490 (=> @t492 (_ (_ tptp.inj_on1745913142lle_tv (_ (_ tptp.produc2101297531lle_tv @t488) @t491)) tptp.top_to1411004326lle_tv)))))
% 151.11/151.91  (assume @p199 (forall (@list @t493 @t487) (=> @t494 (=> @t489 (_ (_ tptp.inj_on552895452tv_nat (_ (_ tptp.produc42536895at_nat @t493) @t487)) tptp.top_to975729152tv_nat)))))
% 151.11/151.91  (assume @p200 (forall (@list @t493 @t491) (=> @t494 (=> @t492 (_ (_ tptp.inj_on2112487900lle_tv (_ (_ tptp.produc1345917071lle_tv @t493) @t491)) tptp.top_to1871154984lle_tv)))))
% 151.11/151.91  (assume @p201 (forall (@list @t497 @t499 @t495 @t496) (=> (_ (_ tptp.member1474794996lle_fm (_ @t498 @t499)) @t495) (=> (= @t496 @t499) (_ (_ tptp.member1474794996lle_fm (_ @t498 @t496)) @t495)))))
% 151.11/151.91  (assume @p202 (forall (@list @t502 @t504 @t500 @t501) (=> (_ (_ tptp.member1569366824lle_tv (_ @t503 @t504)) @t500) (=> (= @t501 @t504) (_ (_ tptp.member1569366824lle_tv (_ @t503 @t501)) @t500)))))
% 151.11/151.91  (assume @p203 (forall @t508 (=> @t507 @t506)))
% 151.11/151.91  (assume @p204 (forall @t512 (=> @t511 @t510)))
% 151.11/151.91  (assume @p205 (forall (@list @t457 @t513 @t428 @t425) (= (_ @t515 @t432) @t514)))
% 151.11/151.91  (assume @p206 (forall (@list @t517 @t516 @t428 @t425) (= (_ @t519 @t432) @t518)))
% 151.11/151.91  (assume @p207 (forall (@list @t521 @t520 @t439 @t436) (= (_ @t523 @t443) @t522)))
% 151.11/151.91  (assume @p208 (forall (@list @t460 @t360 @t439 @t436) (= (_ @t525 @t443) @t524)))
% 151.11/151.91  (assume @p209 (forall @t508 (=> @t506 @t507)))
% 151.11/151.91  (assume @p210 (forall @t512 (=> @t510 @t511)))
% 151.11/151.91  (assume @p211 (forall @t163 (=> (forall @t152 (not (= @t162 (_ @t526 @t71)))) (not (forall @t151 (not (= @t162 (_ @t526 @t66))))))))
% 151.11/151.91  (assume @p212 (forall (@list @t59 @t171) (=> @t213 (= (_ (_ (_ tptp.the_inv_into_nat_nat tptp.top_top_set_nat) @t59) @t249) @t171))))
% 151.11/151.91  (assume @p213 (forall (@list @t217 @t153) (=> @t221 (= (_ (_ (_ tptp.the_in452116896lle_tv tptp.top_to1057771083lle_tv) @t217) @t255) @t153))))
% 151.11/151.91  (assume @p214 (forall @t76 (=> @t75 (=> (_ @t527 (_ @t461 @t67)) (=> (forall @t74 (=> @t73 (=> @t72 (not (_ @t527 (_ @t461 @t71)))))) (not (forall @t69 (=> @t68 (=> @t65 (not (_ @t527 (_ @t461 @t66))))))))))))
% 151.11/151.91  (assume @p215 (forall (@list @t59 @t129 @t171) (=> @t337 (=> @t333 (= (_ @t528 @t249) @t171)))))
% 151.11/151.91  (assume @p216 (forall (@list @t217 @t124 @t153) (=> @t342 (=> @t341 (= (_ @t529 @t255) @t153)))))
% 151.11/151.91  (assume @p217 (forall @t338 (=> @t337 (=> (= @t249 @t229) (=> @t333 (= @t530 @t171))))))
% 151.11/151.91  (assume @p218 (forall @t343 (=> @t342 (=> (= @t255 @t64) (=> @t341 (= @t531 @t153))))))
% 151.11/151.91  (assume @p219 (forall (@list @t59 @t532) (=> @t213 (=> @t534 (_ @t533 (_ (_ tptp.inv_image_nat_nat @t532) @t59))))))
% 151.11/151.91  (assume @p220 (forall (@list @t183 @t535) (=> @t187 (=> @t537 (_ @t533 (_ (_ tptp.inv_im516950809tv_nat @t535) @t183))))))
% 151.11/151.91  (assume @p221 (forall (@list @t538 @t532) (=> (_ (_ tptp.inj_on1179712058tv_nat @t538) tptp.top_to1057771083lle_tv) (=> @t534 (_ @t536 (_ (_ tptp.inv_im1292588663lle_tv @t532) @t538))))))
% 151.11/151.91  (assume @p222 (forall (@list @t217 @t535) (=> @t221 (=> @t537 (_ @t536 (_ (_ tptp.inv_im719552961lle_tv @t535) @t217))))))
% 151.11/151.91  (assume @p223 (forall @t541 (=> @t337 (= (_ (_ tptp.image_nat_nat @t528) @t540) @t129))))
% 151.11/151.91  (assume @p224 (forall @t544 (=> @t342 (= (_ (_ tptp.image_335818702lle_tv @t529) @t543) @t124))))
% 151.11/151.91  (assume @p225 (forall (@list @t428 @t425 @t495 @t457 @t513) (=> @t546 (_ (_ tptp.member1474794996lle_fm @t514) @t545))))
% 151.11/151.91  (assume @p226 (forall (@list @t428 @t425 @t495 @t517 @t516) (=> @t546 (_ (_ tptp.member1569366824lle_tv @t518) @t547))))
% 151.11/151.91  (assume @p227 (forall (@list @t439 @t436 @t500 @t521 @t520) (=> @t549 (_ (_ tptp.member1474794996lle_fm @t522) @t548))))
% 151.11/151.91  (assume @p228 (forall (@list @t439 @t436 @t500 @t460 @t360) (=> @t549 (_ (_ tptp.member1569366824lle_tv @t524) @t550))))
% 151.11/151.91  (assume @p229 (forall (@list @t393 @t551) (= (_ tptp.produc1232814113lle_tv @t554) @t553)))
% 151.11/151.91  (assume @p230 (forall (@list @t153 @t555) (= (_ tptp.produc178635363at_nat @t558) @t557)))
% 151.11/151.91  (assume @p231 (forall (@list @t456 @t383) (= (_ tptp.produc1000205111lle_fm @t459) @t559)))
% 151.11/151.91  (assume @p232 (forall (@list @t63 @t64) (= (_ tptp.produc225513635lle_tv @t462) @t560)))
% 151.11/151.91  (assume @p233 (forall (@list @t383 @t456 @t112) (= (_ (_ tptp.member74361182lle_tv @t559) (_ (_ tptp.image_924970994lle_tv tptp.produc1000205111lle_fm) @t112)) (_ (_ tptp.member1474794996lle_fm @t459) @t112))))
% 151.11/151.91  (assume @p234 (forall (@list @t64 @t63 @t118) (= (_ (_ tptp.member1234290208at_nat @t560) (_ (_ tptp.image_1724396928at_nat tptp.produc225513635lle_tv) @t118)) (_ (_ tptp.member1569366824lle_tv @t462) @t118))))
% 151.11/151.91  (assume @p235 (forall (@list @t551 @t393 @t561) (= (_ (_ tptp.member1474794996lle_fm @t553) (_ (_ tptp.image_326034184lle_fm tptp.produc1232814113lle_tv) @t561)) (_ (_ tptp.member74361182lle_tv @t554) @t561))))
% 151.11/151.91  (assume @p236 (forall (@list @t555 @t153 @t562) (= (_ (_ tptp.member1569366824lle_tv @t557) (_ (_ tptp.image_769496456lle_tv tptp.produc178635363at_nat) @t562)) (_ (_ tptp.member1234290208at_nat @t558) @t562))))
% 151.11/151.91  (assume @p237 (forall @t567 (=> @t566 (=> @t564 (= (_ (_ tptp.image_815163717at_nat (_ @t563 @t357)) tptp.top_to1555900337at_nat) tptp.top_to1555900337at_nat)))))
% 151.11/151.91  (assume @p238 (forall (@list @t59 @t353) (=> @t566 (=> @t568 (= (_ (_ tptp.image_1674248956lle_tv (_ (_ tptp.produc313957681lle_tv @t59) @t353)) tptp.top_to1555900337at_nat) tptp.top_to1411004326lle_tv)))))
% 151.11/151.91  (assume @p239 (forall (@list @t59 @t569) (=> @t566 (=> @t570 (= (_ (_ tptp.image_1787705850at_nat (_ (_ tptp.produc1685803475tv_nat @t59) @t569)) tptp.top_to1411004326lle_tv) tptp.top_to1555900337at_nat)))))
% 151.11/151.91  (assume @p240 (forall (@list @t59 @t360) (=> @t566 (=> @t571 (= (_ (_ tptp.image_149830562lle_tv (_ (_ tptp.produc2101297531lle_tv @t59) @t360)) tptp.top_to1411004326lle_tv) tptp.top_to1411004326lle_tv)))))
% 151.11/151.91  (assume @p241 (forall (@list @t183 @t357) (=> @t572 (=> @t564 (= (_ (_ tptp.image_1597721174tv_nat (_ (_ tptp.produc1250721397at_nat @t183) @t357)) tptp.top_to1555900337at_nat) tptp.top_to975729152tv_nat)))))
% 151.11/151.91  (assume @p242 (forall (@list @t183 @t353) (=> @t572 (=> @t568 (= (_ (_ tptp.image_1507992062lle_tv (_ (_ tptp.produc210389789lle_tv @t183) @t353)) tptp.top_to1555900337at_nat) tptp.top_to1871154984lle_tv)))))
% 151.11/151.91  (assume @p243 (forall (@list @t183 @t569) (=> @t572 (=> @t570 (= (_ (_ tptp.image_53754658tv_nat (_ (_ tptp.produc189459613tv_nat @t183) @t569)) tptp.top_to1411004326lle_tv) tptp.top_to975729152tv_nat)))))
% 151.11/151.91  (assume @p244 (forall (@list @t183 @t360) (=> @t572 (=> @t571 (= (_ (_ tptp.image_988201162lle_tv (_ (_ tptp.produc1975500101lle_tv @t183) @t360)) tptp.top_to1411004326lle_tv) tptp.top_to1871154984lle_tv)))))
% 151.11/151.91  (assume @p245 (forall (@list @t538 @t357) (=> @t573 (=> @t564 (= (_ (_ tptp.image_1805124128at_nat (_ (_ tptp.produc386540311at_nat @t538) @t357)) tptp.top_to975729152tv_nat) tptp.top_to1555900337at_nat)))))
% 151.11/151.91  (assume @p246 (forall (@list @t538 @t353) (=> @t573 (=> @t568 (= (_ (_ tptp.image_1200372424lle_tv (_ (_ tptp.produc72207551lle_tv @t538) @t353)) tptp.top_to975729152tv_nat) tptp.top_to1411004326lle_tv)))))
% 151.11/151.91  (assume @p247 (forall @t214 (= @t566 (forall @t574 (exists @t132 (= @t181 @t211))))))
% 151.11/151.91  (assume @p248 (forall @t188 (= @t572 (forall @t575 (exists @t132 (= @t215 @t184))))))
% 151.11/151.91  (assume @p249 (forall (@list @t538) (= @t573 (forall @t574 (exists @t127 (= @t181 (_ @t538 @t125)))))))
% 151.11/151.91  (assume @p250 (forall @t222 (= @t577 (forall @t575 (exists @t127 (= @t215 @t219))))))
% 151.11/151.91  (assume @p251 (forall (@list @t357 @t59) (=> @t578 @t564)))
% 151.11/151.91  (assume @p252 (forall (@list @t353 @t538) (=> (forall @t136 (= (_ @t353 @t579) @t135)) @t568)))
% 151.11/151.91  (assume @p253 (forall (@list @t569 @t183) (=> (forall @t139 (= (_ @t569 @t265) @t138)) @t570)))
% 151.11/151.91  (assume @p254 (forall (@list @t360 @t217) (=> (forall @t136 @t369) @t571)))
% 151.11/151.91  (assume @p255 (forall @t581 (=> @t566 (not (forall @t139 (not @t580))))))
% 151.11/151.91  (assume @p256 (forall @t583 (=> @t572 (not (forall @t139 (not @t582))))))
% 151.11/151.91  (assume @p257 (forall @t585 (=> @t573 (not (forall @t136 (not @t584))))))
% 151.11/151.91  (assume @p258 (forall @t587 (=> @t577 (not (forall @t136 (not @t586))))))
% 151.11/151.91  (assume @p259 (forall @t581 (=> @t566 (exists @t139 @t580))))
% 151.11/151.91  (assume @p260 (forall @t583 (=> @t572 (exists @t139 @t582))))
% 151.11/151.91  (assume @p261 (forall @t585 (=> @t573 (exists @t136 @t584))))
% 151.11/151.91  (assume @p262 (forall @t587 (=> @t577 (exists @t136 @t586))))
% 151.11/151.91  (assume @p263 (forall @t367 (=> (forall @t139 (=> @t311 (forall (@list @t588) (=> (_ (_ tptp.member_nat @t588) @t129) (= (= @t365 (_ @t357 (_ @t59 @t588))) (= (_ @t357 @t138) (_ @t357 @t588))))))) (=> @t337 (= (_ @t358 @t540) @t359)))))
% 151.11/151.91  (assume @p264 (forall @t370 (=> (forall @t136 (=> @t313 (forall (@list @t589) (=> (_ (_ tptp.member266900804lle_tv @t589) @t124) (= (= @t368 (_ @t360 (_ @t217 @t589))) (= (_ @t360 @t135) (_ @t360 @t589))))))) (=> @t342 (= (_ @t361 @t543) @t362)))))
% 151.11/151.91  (assume @p265 (forall (@list @t59 @t108 @t129) (=> @t213 @t590)))
% 151.11/151.91  (assume @p266 (forall (@list @t217 @t104 @t124) (=> @t221 @t591)))
% 151.11/151.91  (assume @p267 (forall @t594 (=> @t213 @t593)))
% 151.11/151.91  (assume @p268 (forall @t597 (=> @t221 @t596)))
% 151.11/151.91  (assume @p269 (forall (@list @t59 @t598) (=> @t213 (= (_ (_ tptp.member_nat @t598) @t565) (exists @t132 (and (= @t598 @t211) (forall @t574 (=> (= @t598 @t210) (= @t181 @t130)))))))))
% 151.11/151.91  (assume @p270 (forall (@list @t217 @t436) (=> @t221 (= (_ (_ tptp.member266900804lle_tv @t436) @t576) (exists @t127 (and (= @t436 @t219) (forall @t575 (=> (= @t436 @t218) (= @t215 @t125)))))))))
% 151.11/151.91  (assume @p271 (forall (@list @t601 @t457 @t513 @t495) (=> (_ @t602 @t545) (not (forall @t483 (=> (= @t601 (_ (_ tptp.produc1710735575lle_fm (_ @t457 @t481)) (_ @t513 @t480))) @t600))))))
% 151.11/151.91  (assume @p272 (forall (@list @t601 @t521 @t520 @t500) (=> (_ @t602 @t548) (not (forall @t486 (=> (= @t601 (_ (_ tptp.produc1710735575lle_fm (_ @t521 @t484)) (_ @t520 @t282))) @t604))))))
% 151.11/151.91  (assume @p273 (forall (@list @t605 @t517 @t516 @t495) (=> (_ @t606 @t547) (not (forall @t483 (=> (= @t605 (_ (_ tptp.produc1680557635lle_tv (_ @t517 @t481)) (_ @t516 @t480))) @t600))))))
% 151.11/151.91  (assume @p274 (forall (@list @t605 @t460 @t360 @t500) (=> (_ @t606 @t550) (not (forall @t486 (=> (= @t605 (_ (_ tptp.produc1680557635lle_tv (_ @t460 @t484)) (_ @t360 @t282))) @t604))))))
% 151.11/151.91  (assume @p275 (forall @t541 (=> @t337 (_ (_ tptp.inj_on_nat_nat @t528) @t540))))
% 151.11/151.91  (assume @p276 (forall @t544 (=> @t342 (_ (_ tptp.inj_on772319074lle_tv @t529) @t543))))
% 151.11/151.91  (assume @p277 (forall (@list @t59 @t129 @t229) (=> @t337 (=> (_ @t331 @t540) (= (_ @t59 @t530) @t229)))))
% 151.11/151.91  (assume @p278 (forall (@list @t217 @t124 @t64) (=> @t342 (=> (_ @t339 @t543) (= (_ @t217 @t531) @t64)))))
% 151.11/151.91  (assume @p279 (forall (@list @t532 @t607) (=> @t534 (=> @t608 (_ (_ tptp.total_1775715973at_nat tptp.top_to1555900337at_nat) (_ (_ tptp.lex_prod_nat_nat @t532) @t607))))))
% 151.11/151.91  (assume @p280 (forall (@list @t532 @t609) (=> @t534 (=> @t610 (_ (_ tptp.total_517371324lle_tv tptp.top_to1411004326lle_tv) (_ (_ tptp.lex_pr413684186lle_tv @t532) @t609))))))
% 151.11/151.91  (assume @p281 (forall (@list @t535 @t607) (=> @t537 (=> @t608 (_ (_ tptp.total_440843542tv_nat tptp.top_to975729152tv_nat) (_ (_ tptp.lex_pr1785529980tv_nat @t535) @t607))))))
% 151.11/151.91  (assume @p282 (forall (@list @t535 @t609) (=> @t537 (=> @t610 (_ (_ tptp.total_92239038lle_tv tptp.top_to1871154984lle_tv) (_ (_ tptp.lex_pr567812260lle_tv @t535) @t609))))))
% 151.11/151.91  (assume @p283 (forall (@list @t428 @t425 @t427 @t424 @t612 @t611) (= (_ (_ tptp.member1592865093lle_fm (_ (_ tptp.produc407632608lle_fm @t432) @t430)) (_ (_ tptp.lex_pr2001015487lle_fm @t612) @t611)) (or (_ (_ tptp.member146333935lle_tv (_ (_ tptp.produc1297923922lle_tv @t428) @t427)) @t612) (and @t429 (_ (_ tptp.member334644067lle_fm (_ (_ tptp.produc1126104134lle_fm @t425) @t424)) @t611))))))
% 151.11/151.91  (assume @p284 (forall (@list @t439 @t436 @t438 @t435 @t613 @t609) (= (_ (_ tptp.member1339857875lle_tv (_ (_ tptp.produc2057188974lle_tv @t443) @t441)) (_ (_ tptp.lex_pr1093414955lle_tv @t613) @t609)) (or (_ (_ tptp.member112824072at_nat (_ (_ tptp.produc780837143at_nat @t439) @t438)) @t613) (and @t440 (_ (_ tptp.member1531318361lle_tv (_ (_ tptp.produc2058540732lle_tv @t436) @t435)) @t609))))))
% 151.11/151.91  (assume @p285 (forall @t615 (= @t614 @t464)))
% 151.11/151.91  (assume @p286 (forall @t617 (= @t616 @t470)))
% 151.11/151.91  (assume @p287 (forall (@list @t456 @t383 @t428) (=> (= @t618 @t428) (= @t456 @t428))))
% 151.11/151.91  (assume @p288 (forall (@list @t63 @t64 @t439) (=> (= @t619 @t439) (= @t63 @t439))))
% 151.11/151.91  (assume @p289 (forall (@list @t456 @t383 @t620) (=> (= @t621 @t620) (= @t383 @t620))))
% 151.11/151.91  (assume @p290 (forall (@list @t63 @t64 @t104) (=> (= @t622 @t104) (= @t64 @t104))))
% 151.11/151.91  (assume @p291 (forall @t623 (= (_ tptp.produc29804011lle_fm @t450) @t449)))
% 151.11/151.91  (assume @p292 (forall @t624 (= (_ tptp.produc1636169559lle_tv @t455) @t454)))
% 151.11/151.91  (assume @p293 (forall @t623 (= (_ tptp.produc148705065lle_fm @t450) @t447)))
% 151.11/151.91  (assume @p294 (forall @t624 (= (_ tptp.produc547496597lle_tv @t455) @t452)))
% 151.11/151.91  (assume @p295 (forall @t615 (= @t464 @t614)))
% 151.11/151.91  (assume @p296 (forall @t617 (= @t470 @t616)))
% 151.11/151.91  (assume @p297 (forall (@list @t625) (= @t625 (_ (_ tptp.produc1710735575lle_fm (_ tptp.produc29804011lle_fm @t625)) (_ tptp.produc148705065lle_fm @t625)))))
% 151.11/151.91  (assume @p298 (forall (@list @t626) (= @t626 (_ (_ tptp.produc1680557635lle_tv (_ tptp.produc1636169559lle_tv @t626)) (_ tptp.produc547496597lle_tv @t626)))))
% 151.11/151.91  (assume @p299 (forall (@list @t627 @t456 @t383 @t96) (=> (_ (_ @t627 @t456) @t383) (=> (= @t96 @t459) (_ (_ @t627 (_ tptp.produc29804011lle_fm @t96)) (_ tptp.produc148705065lle_fm @t96))))))
% 151.11/151.91  (assume @p300 (forall (@list @t148 @t63 @t64 @t100) (=> (_ (_ @t148 @t63) @t64) (=> (= @t100 @t462) (_ (_ @t148 (_ tptp.produc1636169559lle_tv @t100)) (_ tptp.produc547496597lle_tv @t100))))))
% 151.11/151.91  (assume @p301 (forall (@list @t631 @t628 @t630 @t16) (=> (_ @t631 @t628) (=> (_ @t630 @t16) (and (_ @t631 (_ tptp.produc29804011lle_fm @t629)) (_ @t630 (_ tptp.produc148705065lle_fm @t629)))))))
% 151.11/151.91  (assume @p302 (forall (@list @t635 @t633 @t134 @t632) (=> (_ @t635 @t633) (=> (_ @t134 @t632) (and (_ @t635 (_ tptp.produc1636169559lle_tv @t634)) (_ @t134 (_ tptp.produc547496597lle_tv @t634)))))))
% 151.11/151.91  (assume @p303 (forall (@list @t636 @t383 @t456) (=> (_ (_ @t636 @t383) @t456) (_ (_ @t636 @t621) @t618))))
% 151.11/151.91  (assume @p304 (forall (@list @t637 @t64 @t63) (=> (_ (_ @t637 @t64) @t63) (_ (_ @t637 @t622) @t619))))
% 151.11/151.91  (assume @p305 (forall @t640 (=> @t639 (= (_ tptp.produc148705065lle_fm @t159) @t638))))
% 151.11/151.91  (assume @p306 (forall @t643 (=> @t642 (= (_ tptp.produc547496597lle_tv @t162) @t641))))
% 151.11/151.91  (assume @p307 (forall (@list @t425 @t478) (= (= @t425 (_ tptp.produc148705065lle_fm @t478)) (exists (@list @t644) (= @t478 (_ (_ tptp.produc1710735575lle_fm @t644) @t425))))))
% 151.11/151.91  (assume @p308 (forall (@list @t436 @t479) (= (= @t436 (_ tptp.produc547496597lle_tv @t479)) (exists (@list @t645) (= @t479 (_ (_ tptp.produc1680557635lle_tv @t645) @t436))))))
% 151.11/151.91  (assume @p309 (forall (@list @t428 @t478) (= (= @t428 (_ tptp.produc29804011lle_fm @t478)) (exists (@list @t646) (= @t478 (_ @t431 @t646))))))
% 151.11/151.91  (assume @p310 (forall (@list @t439 @t479) (= (= @t439 (_ tptp.produc1636169559lle_tv @t479)) (exists (@list @t647) (= @t479 (_ @t442 @t647))))))
% 151.11/151.91  (assume @p311 (forall @t640 (=> @t639 (= (_ tptp.produc29804011lle_fm @t159) @t551))))
% 151.11/151.91  (assume @p312 (forall @t643 (=> @t642 (= (_ tptp.produc1636169559lle_tv @t162) @t555))))
% 151.11/151.91  (assume @p313 (forall (@list @t631 @t456 @t649 @t383 @t648) (=> (_ @t631 @t456) (=> (_ (_ tptp.member334644067lle_fm (_ (_ tptp.produc1126104134lle_fm @t649) @t383)) (_ @t648 @t456)) (_ (_ tptp.member1592865093lle_fm (_ (_ tptp.produc407632608lle_fm (_ @t458 @t649)) @t459)) (_ (_ tptp.same_f1581085506lle_fm @t631) @t648))))))
% 151.11/151.91  (assume @p314 (forall (@list @t635 @t63 @t651 @t64 @t650) (=> (_ @t635 @t63) (=> (_ (_ tptp.member1531318361lle_tv (_ (_ tptp.produc2058540732lle_tv @t651) @t64)) (_ @t650 @t63)) (_ (_ tptp.member1339857875lle_tv (_ (_ tptp.produc2057188974lle_tv (_ @t461 @t651)) @t462)) (_ (_ tptp.same_f1138187694lle_tv @t635) @t650))))))
% 151.11/151.91  (assume @p315 (forall (@list @t532 @t59) (=> (_ tptp.wf_nat @t532) (=> @t213 (_ tptp.wf_nat (_ (_ tptp.image_815163717at_nat (_ @t563 @t59)) @t532))))))
% 151.11/151.91  (assume @p316 (forall (@list @t535 @t217) (=> (_ tptp.wf_Par1378404612lle_tv @t535) (=> @t221 (_ tptp.wf_Par1378404612lle_tv (_ (_ tptp.image_1221801032lle_tv (_ (_ tptp.produc1345917071lle_tv @t217) @t217)) @t535))))))
% 151.11/151.91  (assume @p317 (forall (@list @t59 @t129 @t171 @t592) (=> @t337 (=> (_ @t172 @t540) (=> @t653 (_ (_ tptp.member_nat (_ @t528 @t171)) @t592))))))
% 151.11/151.91  (assume @p318 (forall (@list @t217 @t124 @t153 @t595) (=> @t342 (=> (_ @t173 @t543) (=> @t655 (_ (_ tptp.member266900804lle_tv (_ @t529 @t153)) @t595))))))
% 151.11/151.91  (assume @p319 (forall @t567 (=> (_ tptp.order_769474267at_nat @t59) (=> @t566 (=> @t578 (_ tptp.order_769474267at_nat @t357))))))
% 151.11/151.91  (assume @p320 (forall (@list @t657 @t656) (=> (forall @t483 (=> (_ @t599 @t657) (_ @t599 @t656))) (_ (_ tptp.ord_le1007985907lle_fm @t657) @t656))))
% 151.11/151.91  (assume @p321 (forall (@list @t659 @t658) (=> (forall @t486 (=> (_ @t603 @t659) (_ @t603 @t658))) (_ (_ tptp.ord_le1784136743lle_tv @t659) @t658))))
% 151.11/151.91  (assume @p322 (forall (@list @t59 @t592 @t108 @t129) (=> @t660 (=> (_ @t111 @t592) (=> @t653 @t590)))))
% 151.11/151.91  (assume @p323 (forall (@list @t217 @t595 @t104 @t124) (=> @t661 (=> (_ @t107 @t595) (=> @t655 @t591)))))
% 151.11/151.91  (assume @p324 (forall (@list @t59 @t662 @t129 @t592) (=> (_ @t212 @t662) (=> (_ @t652 @t662) (=> (_ @t663 @t662) @t593)))))
% 151.11/151.91  (assume @p325 (forall (@list @t217 @t664 @t124 @t595) (=> (_ @t220 @t664) (=> (_ @t654 @t664) (=> (_ @t665 @t664) @t596)))))
% 151.11/151.91  (assume @p326 (forall @t594 (=> @t337 (=> (_ @t663 @t129) @t660))))
% 151.11/151.91  (assume @p327 (forall @t597 (=> @t342 (=> (_ @t665 @t124) @t661))))
% 151.11/151.91  (assume @p328 (forall (@list @t59 @t592 @t129) (=> @t660 (=> @t653 @t337))))
% 151.11/151.91  (assume @p329 (forall (@list @t217 @t595 @t124) (=> @t661 (=> @t655 @t342))))
% 151.11/151.91  (assume @p330 (forall (@list @t666) (or (= @t666 true) (= @t666 false))))
% 151.11/151.91  (assume @p331 (forall @t667 (= (_ (_ (_ tptp.if_Par1134130401lle_tv false) @t153) @t64) @t64)))
% 151.11/151.91  (assume @p332 (forall @t667 (= (_ (_ (_ tptp.if_Par1134130401lle_tv true) @t153) @t64) @t153)))
% 151.11/151.91  (assume @p333 @t669)
% 151.11/151.91  (assume @p334 true)
% 151.11/151.91  (step @p335 (= tptp.paraco761681009ge_int @t672) :rule refl :args (@t672))
% 151.11/151.91  (step @p336 (= tptp.paraco327635598_valid @t673) :rule refl :args (@t673))
% 151.11/151.91  (step @p337 (= tptp.top_to1299250770e_tv_o @t674) :rule refl :args (@t674))
% 151.11/151.91  (step @p338 (= tptp.top_top_nat_o @t675) :rule refl :args (@t675))
% 151.11/151.91  (step @p339 (= tptp.inj_on2112487900lle_tv @t678) :rule refl :args (@t678))
% 151.11/151.91  (step @p340 (= tptp.inj_on552895452tv_nat @t681) :rule refl :args (@t681))
% 151.11/151.91  (step @p341 (= tptp.inj_on1745913142lle_tv @t684) :rule refl :args (@t684))
% 151.11/151.91  (step @p342 (= tptp.inj_on26176689at_nat @t687) :rule refl :args (@t687))
% 151.11/151.91  (step @p343 (= tptp.inj_on1955349912lle_tv @t692) :rule refl :args (@t692))
% 151.11/151.91  (step @p344 (= tptp.inj_on_nat_nat @t693) :rule refl :args (@t693))
% 151.11/151.91  (step @p345 (= tptp.inj_on772319074lle_tv @t696) :rule refl :args (@t696))
% 151.11/151.91  (step @p346 (= tptp.produc234482697lle_tv @t700) :rule refl :args (@t700))
% 151.11/151.91  (step @p347 (= tptp.produc1232814113lle_tv @t702) :rule refl :args (@t702))
% 151.11/151.91  (step @p348 (= tptp.produc178635363at_nat @t704) :rule refl :args (@t704))
% 151.11/151.91  (step @p349 :rule eq-symm :args (@t715 @t718))
% 151.11/151.91  (step @p350 :rule refl :args (@t721))
% 151.11/151.91  (step @p351 :rule nary_cong :premises (@p350 @p349) :args (@t722))
% 151.11/151.91  (step @p352 :rule eq-symm :args (@t723 @t715))
% 151.11/151.91  (step @p353 :rule refl :args (@t724))
% 151.11/151.91  (step @p354 :rule nary_cong :premises (@p353 @p352) :args (@t725))
% 151.11/151.91  (step @p355 :rule nary_cong :premises (@p354 @p351) :args (@t726))
% 151.11/151.91  (step @p356 :rule refl :args (@t727))
% 151.11/151.91  (step @p357 :rule nary_cong :premises (@p356 @p355) :args (@t728))
% 151.11/151.91  (step @p358 :rule eq-symm :args (@t719 @t715))
% 151.11/151.91  (step @p359 :rule refl :args (@t729))
% 151.11/151.91  (step @p360 :rule nary_cong :premises (@p359 @p358) :args (@t730))
% 151.11/151.91  (step @p361 :rule nary_cong :premises (@p360 @p357) :args (@t731))
% 151.11/151.91  (step @p362 :rule refl :args (@t732))
% 151.11/151.91  (step @p363 :rule nary_cong :premises (@p362 @p361) :args (@t733))
% 151.11/151.91  (step @p364 :rule cong :premises (@p363) :args (@t735))
% 151.11/151.91  (step @p365 :rule eq-symm :args (@t739 @t741))
% 151.11/151.91  (step @p366 :rule eq-symm :args (@t742 @t739))
% 151.11/151.91  (step @p367 :rule cong :premises (@p366) :args (@t743))
% 151.11/151.91  (step @p368 :rule nary_cong :premises (@p367 @p365) :args (@t744))
% 151.11/151.91  (step @p369 :rule cong :premises (@p368) :args (@t745))
% 151.11/151.91  (step @p370 :rule nary_cong :premises (@p369 @p364) :args (@t746))
% 151.11/151.91  ; WARNING: add trust step for TRUST
% 151.11/151.91  ; trust TRUST PREPROCESS_HO_ELIM
% 151.11/151.91  (step @p371 :rule trust :premises () :args ((= (and (forall @t765 (or (not (= @t764 @t763)) (= @t763 @t762))) (forall @t759 (or @t758 (and @t757 (or @t756 (and @t755 (or @t753 (= @t750 @t747)))))))) @t746)))
% 151.11/151.91  (step @p372 :rule eq-symm :args (@t747 @t750))
% 151.11/151.91  (step @p373 :rule refl :args (@t753))
% 151.11/151.91  (step @p374 :rule nary_cong :premises (@p373 @p372) :args (@t766))
% 151.11/151.91  (step @p375 :rule refl :args (@t755))
% 151.11/151.91  (step @p376 :rule nary_cong :premises (@p375 @p374) :args (@t767))
% 151.11/151.91  (step @p377 :rule refl :args (@t756))
% 151.11/151.91  (step @p378 :rule nary_cong :premises (@p377 @p376) :args (@t768))
% 151.11/151.91  (step @p379 :rule refl :args (@t757))
% 151.11/151.91  (step @p380 :rule nary_cong :premises (@p379 @p378) :args (@t769))
% 151.11/151.91  (step @p381 :rule refl :args (@t758))
% 151.11/151.91  (step @p382 :rule nary_cong :premises (@p381 @p380) :args (@t770))
% 151.11/151.91  (step @p383 :rule cong :premises (@p382) :args ((forall @t759 @t770)))
% 151.11/151.91  (step @p384 :rule refl :args ((tptp.paraco1325918602e_eval @t749 @t771)))
% 151.11/151.91  (step @p385 :rule refl :args (@t748))
% 151.11/151.91  (step @p386 :rule refl :args (@t749))
% 151.11/151.91  (step @p387 :rule cong :premises (@p386 @p385) :args (@t750))
% 151.11/151.91  (step @p388 :rule trans :premises (@p387 @p384))
% 151.11/151.91  (step @p389 :rule refl :args (@t772))
% 151.11/151.91  (step @p390 :rule ho_cong :premises (@p389 @p385))
% 151.11/151.91  (step @p391 :rule cong :premises (@p390 @p388) :args ((= (_ @t772 @t748) @t750)))
% 151.11/151.91  (step @p392 :rule symm :premises (@p391))
% 151.11/151.91  (step @p393 :rule refl :args (@t773))
% 151.11/151.91  (step @p394 :rule eq_resolve :premises (@p393 @p392))
% 151.11/151.91  (step @p395 :rule refl :args (@t771))
% 151.11/151.91  (step @p396 :rule cong :premises (@p395 @p385) :args ((= @t771 @t748)))
% 151.11/151.91  (step @p397 :rule symm :premises (@p396))
% 151.11/151.91  (step @p398 :rule eq_resolve :premises (@p395 @p397))
% 151.11/151.91  (step @p399 :rule ho_cong :premises (@p389 @p398))
% 151.11/151.91  (step @p400 :rule trans :premises (@p399 @p394))
% 151.11/151.91  (step @p401 :rule refl :args (@t747))
% 151.11/151.91  (step @p402 :rule refl :args (@t15))
% 151.11/151.91  (step @p403 :rule cong :premises (@p402 @p401) :args ((= @t15 @t747)))
% 151.11/151.91  (step @p404 :rule symm :premises (@p403))
% 151.11/151.91  (step @p405 :rule eq_resolve :premises (@p402 @p404))
% 151.11/151.91  (step @p406 :rule cong :premises (@p405 @p400) :args (@t774))
% 151.11/151.91  (step @p407 :rule refl :args (@t751))
% 151.11/151.91  (step @p408 :rule refl :args (@t775))
% 151.11/151.91  (step @p409 :rule cong :premises (@p408 @p407) :args ((= @t775 @t751)))
% 151.11/151.91  (step @p410 :rule symm :premises (@p409))
% 151.11/151.91  (step @p411 :rule eq_resolve :premises (@p408 @p410))
% 151.11/151.91  (step @p412 :rule refl :args (@t752))
% 151.11/151.91  (step @p413 :rule refl :args (@t1))
% 151.11/151.91  (step @p414 :rule cong :premises (@p413 @p412) :args ((= @t1 @t752)))
% 151.11/151.91  (step @p415 :rule symm :premises (@p414))
% 151.11/151.91  (step @p416 :rule eq_resolve :premises (@p413 @p415))
% 151.11/151.91  (step @p417 :rule cong :premises (@p416 @p411) :args (@t776))
% 151.11/151.91  (step @p418 :rule nary_cong :premises (@p417 @p406) :args (@t777))
% 151.11/151.91  (step @p419 :rule refl :args (@t754))
% 151.11/151.91  (step @p420 :rule refl :args (@t778))
% 151.11/151.91  (step @p421 :rule cong :premises (@p420 @p419) :args ((= @t778 @t754)))
% 151.11/151.91  (step @p422 :rule symm :premises (@p421))
% 151.11/151.91  (step @p423 :rule eq_resolve :premises (@p420 @p422))
% 151.11/151.91  (step @p424 :rule cong :premises (@p423 @p400) :args (@t779))
% 151.11/151.91  (step @p425 :rule cong :premises (@p417) :args (@t780))
% 151.11/151.91  (step @p426 :rule nary_cong :premises (@p425 @p424) :args (@t781))
% 151.11/151.91  (step @p427 :rule nary_cong :premises (@p426 @p418) :args (@t782))
% 151.11/151.91  (step @p428 :rule cong :premises (@p416 @p423) :args (@t783))
% 151.11/151.91  (step @p429 :rule nary_cong :premises (@p428 @p427) :args (@t784))
% 151.11/151.91  (step @p430 :rule cong :premises (@p411 @p400) :args (@t785))
% 151.11/151.91  (step @p431 :rule cong :premises (@p428) :args (@t786))
% 151.11/151.91  (step @p432 :rule nary_cong :premises (@p431 @p430) :args (@t787))
% 151.11/151.91  (step @p433 :rule nary_cong :premises (@p432 @p429) :args (@t788))
% 151.11/151.91  (step @p434 :rule cong :premises (@p411 @p423) :args (@t789))
% 151.11/151.91  (step @p435 :rule nary_cong :premises (@p434 @p433) :args (@t790))
% 151.11/151.91  (step @p436 :rule cong :premises (@p435) :args ((forall @t759 @t790)))
% 151.11/151.91  (step @p437 :rule trans :premises (@p436 @p383))
% 151.11/151.91  (step @p438 :rule eq-symm :args (@t773 @t15))
% 151.11/151.91  (step @p439 :rule refl :args (@t776))
% 151.11/151.91  (step @p440 :rule nary_cong :premises (@p439 @p438) :args (@t791))
% 151.11/151.91  (step @p441 :rule eq-symm :args (@t773 @t778))
% 151.11/151.91  (step @p442 :rule refl :args (@t780))
% 151.11/151.91  (step @p443 :rule nary_cong :premises (@p442 @p441) :args (@t792))
% 151.11/151.91  (step @p444 :rule nary_cong :premises (@p443 @p440) :args (@t793))
% 151.11/151.91  (step @p445 :rule refl :args (@t783))
% 151.11/151.91  (step @p446 :rule nary_cong :premises (@p445 @p444) :args (@t794))
% 151.11/151.91  (step @p447 :rule eq-symm :args (@t773 @t775))
% 151.11/151.91  (step @p448 :rule refl :args (@t786))
% 151.11/151.91  (step @p449 :rule nary_cong :premises (@p448 @p447) :args (@t795))
% 151.11/151.91  (step @p450 :rule nary_cong :premises (@p449 @p446) :args (@t796))
% 151.11/151.91  (step @p451 :rule refl :args (@t789))
% 151.11/151.91  (step @p452 :rule nary_cong :premises (@p451 @p450) :args (@t797))
% 151.11/151.91  (step @p453 :rule cong :premises (@p452) :args (@t798))
% 151.11/151.91  (step @p454 :rule trans :premises (@p453 @p437))
% 151.11/151.91  (step @p455 :rule refl :args ((tptp.paraco1325918602e_eval @t761 @t799)))
% 151.11/151.91  (step @p456 :rule refl :args (@t760))
% 151.11/151.91  (step @p457 :rule refl :args (@t761))
% 151.11/151.91  (step @p458 :rule cong :premises (@p457 @p456) :args (@t762))
% 151.11/151.91  (step @p459 :rule trans :premises (@p458 @p455))
% 151.11/151.91  (step @p460 :rule refl :args (@t800))
% 151.11/151.91  (step @p461 :rule ho_cong :premises (@p460 @p456))
% 151.11/151.91  (step @p462 :rule cong :premises (@p461 @p459) :args ((= (_ @t800 @t760) @t762)))
% 151.11/151.91  (step @p463 :rule symm :premises (@p462))
% 151.11/151.91  (step @p464 :rule refl :args (@t801))
% 151.11/151.91  (step @p465 :rule eq_resolve :premises (@p464 @p463))
% 151.11/151.91  (step @p466 :rule refl :args (@t799))
% 151.11/151.91  (step @p467 :rule cong :premises (@p466 @p456) :args ((= @t799 @t760)))
% 151.11/151.91  (step @p468 :rule symm :premises (@p467))
% 151.11/151.91  (step @p469 :rule eq_resolve :premises (@p466 @p468))
% 151.11/151.91  (step @p470 :rule ho_cong :premises (@p460 @p469))
% 151.11/151.91  (step @p471 :rule trans :premises (@p470 @p465))
% 151.11/151.91  (step @p472 :rule refl :args (@t763))
% 151.11/151.91  (step @p473 :rule refl :args (@t802))
% 151.11/151.91  (step @p474 :rule cong :premises (@p473 @p472) :args ((= @t802 @t763)))
% 151.11/151.91  (step @p475 :rule symm :premises (@p474))
% 151.11/151.91  (step @p476 :rule eq_resolve :premises (@p473 @p475))
% 151.11/151.91  (step @p477 :rule cong :premises (@p476 @p471) :args (@t803))
% 151.11/151.91  (step @p478 :rule refl :args (@t764))
% 151.11/151.91  (step @p479 :rule refl :args (@t804))
% 151.11/151.91  (step @p480 :rule cong :premises (@p479 @p478) :args ((= @t804 @t764)))
% 151.11/151.91  (step @p481 :rule symm :premises (@p480))
% 151.11/151.91  (step @p482 :rule eq_resolve :premises (@p479 @p481))
% 151.11/151.91  (step @p483 :rule cong :premises (@p482 @p476) :args (@t805))
% 151.11/151.91  (step @p484 :rule cong :premises (@p483) :args (@t806))
% 151.11/151.91  (step @p485 :rule nary_cong :premises (@p484 @p477) :args (@t807))
% 151.11/151.91  (step @p486 :rule cong :premises (@p485) :args ((forall @t765 @t807)))
% 151.11/151.91  (step @p487 :rule eq-symm :args (@t801 @t802))
% 151.11/151.91  (step @p488 :rule refl :args (@t806))
% 151.11/151.91  (step @p489 :rule nary_cong :premises (@p488 @p487) :args (@t808))
% 151.11/151.91  (step @p490 :rule cong :premises (@p489) :args (@t809))
% 151.11/151.91  (step @p491 :rule trans :premises (@p490 @p486))
% 151.11/151.91  (step @p492 :rule nary_cong :premises (@p491 @p454) :args ((and @t809 @t798)))
% 151.11/151.91  (step @p493 :rule alpha_equiv :args (@t816 @t817 (@list @t749 @t706 @t705)))
% 151.11/151.91  (step @p494 :rule alpha_equiv :args (@t820 @t817 (@list @t761 @t736 @t740)))
% 151.11/151.91  (step @p495 :rule nary_cong :premises (@p494 @p493) :args (@t821))
% 151.11/151.91  (step @p496 :rule quant-miniscope-and :args ((= (forall @t42 (and @t819 @t815)) @t821)))
% 151.11/151.91  (step @p497 :rule trans :premises (@p496 @p495))
% 151.11/151.91  (step @p498 :rule trans :premises (@p497 @p492))
% 151.11/151.91  (step @p499 :rule refl :args (@t22))
% 151.11/151.91  (step @p500 :rule bool-double-not-elim :args (@t810))
% 151.11/151.91  (step @p501 :rule nary_cong :premises (@p500 @p499) :args ((or (not @t811) @t22)))
% 151.11/151.91  (step @p502 :rule bool-impl-elim :args (@t811 @t22))
% 151.11/151.91  (step @p503 :rule trans :premises (@p502 @p501))
% 151.11/151.91  (step @p504 :rule bool-impl-elim :args (@t810 @t28))
% 151.11/151.91  (step @p505 :rule nary_cong :premises (@p504 @p503) :args (@t822))
% 151.11/151.91  (step @p506 :rule refl :args (@t812))
% 151.11/151.91  (step @p507 :rule nary_cong :premises (@p506 @p505) :args ((or @t812 @t822)))
% 151.11/151.91  (step @p508 :rule refl :args (@t822))
% 151.11/151.91  (step @p509 :rule bool-double-not-elim :args (@t812))
% 151.11/151.91  (step @p510 :rule nary_cong :premises (@p509 @p508) :args ((or (not @t813) @t822)))
% 151.11/151.91  (step @p511 :rule bool-impl-elim :args (@t813 @t822))
% 151.11/151.91  (step @p512 :rule trans :premises (@p511 @p510))
% 151.11/151.91  (step @p513 :rule trans :premises (@p512 @p507))
% 151.11/151.91  (step @p514 :rule bool-impl-elim :args (@t812 @t34))
% 151.11/151.91  (step @p515 :rule nary_cong :premises (@p514 @p513) :args (@t823))
% 151.11/151.91  (step @p516 :rule refl :args (@t814))
% 151.11/151.91  (step @p517 :rule nary_cong :premises (@p516 @p515) :args ((or @t814 @t823)))
% 151.11/151.91  (step @p518 :rule refl :args (@t823))
% 151.11/151.91  (step @p519 :rule bool-double-not-elim :args (@t814))
% 151.11/151.91  (step @p520 :rule nary_cong :premises (@p519 @p518) :args ((or (not @t818) @t823)))
% 151.11/151.91  (step @p521 :rule bool-impl-elim :args (@t818 @t823))
% 151.11/151.91  (step @p522 :rule trans :premises (@p521 @p520))
% 151.11/151.91  (step @p523 :rule trans :premises (@p522 @p517))
% 151.11/151.91  (step @p524 :rule bool-impl-elim :args (@t814 @t28))
% 151.11/151.91  (step @p525 :rule nary_cong :premises (@p524 @p523) :args (@t824))
% 151.11/151.91  (step @p526 :rule cong :premises (@p525) :args ((forall @t42 @t824)))
% 151.11/151.91  (step @p527 :rule trans :premises (@p526 @p498))
% 151.11/151.91  (step @p528 :rule refl :args (@t22))
% 151.11/151.91  (step @p529 :rule eq-symm :args (@t23 @t1))
% 151.11/151.91  (step @p530 :rule cong :premises (@p529) :args (@t25))
% 151.11/151.91  (step @p531 :rule cong :premises (@p530 @p528) :args (@t26))
% 151.11/151.91  (step @p532 :rule refl :args (@t28))
% 151.11/151.91  (step @p533 :rule cong :premises (@p529 @p532) :args (@t29))
% 151.11/151.91  (step @p534 :rule nary_cong :premises (@p533 @p531) :args (@t30))
% 151.11/151.91  (step @p535 :rule eq-symm :args (@t27 @t1))
% 151.11/151.91  (step @p536 :rule cong :premises (@p535) :args (@t32))
% 151.11/151.91  (step @p537 :rule cong :premises (@p536 @p534) :args (@t33))
% 151.11/151.91  (step @p538 :rule refl :args (@t34))
% 151.11/151.91  (step @p539 :rule cong :premises (@p535 @p538) :args (@t35))
% 151.11/151.91  (step @p540 :rule nary_cong :premises (@p539 @p537) :args (@t36))
% 151.11/151.91  (step @p541 :rule eq-symm :args (@t27 @t23))
% 151.11/151.91  (step @p542 :rule cong :premises (@p541) :args (@t38))
% 151.11/151.91  (step @p543 :rule cong :premises (@p542 @p540) :args (@t39))
% 151.11/151.91  (step @p544 :rule cong :premises (@p541 @p532) :args (@t40))
% 151.11/151.91  (step @p545 :rule nary_cong :premises (@p544 @p543) :args (@t41))
% 151.11/151.91  (step @p546 :rule cong :premises (@p545) :args (@t43))
% 151.11/151.91  (step @p547 :rule trans :premises (@p546 @p527))
% 151.11/151.91  (step @p548 :rule trans :premises (@p547 @p371 @p370))
% 151.11/151.91  (step @p549 :rule eq_resolve :premises (@p6 @p548))
% 151.11/151.91  (step @p550 :rule and_elim :premises (@p549) :args (1))
% 151.11/151.91  (step @p551 :rule eq-symm :args (@t826 @t829))
% 151.11/151.91  (step @p552 :rule refl :args (@t829))
% 151.11/151.91  (step @p553 :rule evaluate :args ((not false)))
% 151.11/151.91  (step @p554 :rule skolem_intro :args (@t825))
% 151.11/151.91  (step @p555 :rule cong :premises (@p554) :args ((not @t825)))
% 151.11/151.91  (step @p556 :rule bool-eq-false :args (@t825))
% 151.11/151.91  (step @p557 :rule eq-symm :args (false @t825))
% 151.11/151.91  (step @p558 :rule trans :premises (@p557 @p556))
% 151.11/151.91  (step @p559 :rule trans :premises (@p558 @p555 @p553))
% 151.11/151.91  (step @p560 :rule true_elim :premises (@p559))
% 151.11/151.91  (step @p561 :rule refl :args (@t716))
% 151.11/151.91  (step @p562 :rule cong :premises (@p561 @p560) :args (@t718))
% 151.11/151.91  (step @p563 :rule cong :premises (@p562 @p552) :args (@t830))
% 151.11/151.91  (step @p564 :rule trans :premises (@p563 @p551))
% 151.11/151.91  (step @p565 :rule eq-symm :args (@t832 @t833))
% 151.11/151.91  (step @p566 :rule refl :args (@t833))
% 151.11/151.91  (step @p567 :rule skolem_intro :args (@t831))
% 151.11/151.91  (step @p568 :rule symm :premises (@p567))
% 151.11/151.91  (step @p569 :rule cong :premises (@p561 @p568) :args (@t720))
% 151.11/151.91  (step @p570 :rule cong :premises (@p569 @p566) :args (@t834))
% 151.11/151.91  (step @p571 :rule trans :premises (@p570 @p565))
% 151.11/151.91  (step @p572 :rule nary_cong :premises (@p571 @p564) :args (@t835))
% 151.11/151.91  (step @p573 :rule refl :args (@t837))
% 151.11/151.91  (step @p574 :rule cong :premises (@p571) :args (@t838))
% 151.11/151.91  (step @p575 :rule nary_cong :premises (@p574 @p573) :args (@t839))
% 151.11/151.91  (step @p576 :rule nary_cong :premises (@p575 @p572) :args (@t840))
% 151.11/151.91  (step @p577 :rule eq-symm :args (@t832 @t836))
% 151.11/151.91  (step @p578 :rule refl :args (@t836))
% 151.11/151.91  (step @p579 :rule cong :premises (@p569 @p578) :args (@t841))
% 151.11/151.91  (step @p580 :rule trans :premises (@p579 @p577))
% 151.11/151.91  (step @p581 :rule nary_cong :premises (@p580 @p576) :args (@t842))
% 151.11/151.91  (step @p582 :rule refl :args (@t843))
% 151.11/151.91  (step @p583 :rule cong :premises (@p580) :args (@t844))
% 151.11/151.91  (step @p584 :rule nary_cong :premises (@p583 @p582) :args (@t845))
% 151.11/151.91  (step @p585 :rule nary_cong :premises (@p584 @p581) :args (@t846))
% 151.11/151.91  (step @p586 :rule refl :args (@t847))
% 151.11/151.91  (step @p587 :rule nary_cong :premises (@p586 @p585) :args (@t848))
% 151.11/151.91  (step @p588 :rule refl :args (@t849))
% 151.11/151.91  (step @p589 :rule cong :premises (@p588 @p587) :args ((=> @t849 @t848)))
% 151.11/151.91  (step @p590 :rule refl :args (@t835))
% 151.11/151.91  (step @p591 :rule eq-symm :args (@t829 @t836))
% 151.11/151.91  (step @p592 :rule refl :args (@t838))
% 151.11/151.91  (step @p593 :rule nary_cong :premises (@p592 @p591) :args (@t850))
% 151.11/151.91  (step @p594 :rule nary_cong :premises (@p593 @p590) :args (@t851))
% 151.11/151.91  (step @p595 :rule refl :args (@t841))
% 151.11/151.91  (step @p596 :rule nary_cong :premises (@p595 @p594) :args (@t852))
% 151.11/151.91  (step @p597 :rule eq-symm :args (@t829 @t833))
% 151.11/151.91  (step @p598 :rule refl :args (@t844))
% 151.11/151.91  (step @p599 :rule nary_cong :premises (@p598 @p597) :args (@t853))
% 151.11/151.91  (step @p600 :rule nary_cong :premises (@p599 @p596) :args (@t854))
% 151.11/151.91  (step @p601 :rule eq-symm :args (@t833 @t836))
% 151.11/151.91  (step @p602 :rule nary_cong :premises (@p601 @p600) :args (@t855))
% 151.11/151.91  (step @p603 :rule cong :premises (@p588 @p602) :args ((=> @t849 @t855)))
% 151.11/151.91  (assume-push @p643 @t849)
% 151.11/151.91  (step @p605 :rule instantiate :premises (@p550) :args ((@list @t827 tptp.p1 tptp.p2)))
% 151.11/151.91  (step-pop @p644 :rule scope :premises (@p605))
% 151.11/151.91  (step @p606 :rule process_scope :premises (@p644) :args (@t855))
% 151.11/151.91  (step @p608 :rule eq_resolve :premises (@p606 @p603))
% 151.11/151.91  (step @p609 :rule eq_resolve :premises (@p608 @p589))
% 151.11/151.91  (step @p610 :rule implies_elim :premises (@p609))
% 151.11/151.91  (step @p611 :rule chain_m_resolution :premises (@p610 @p550) :args (@t863 (@list false) (@list @t849)))
% 151.11/151.91  ; trust TRUST PREPROCESS_HO_ELIM
% 151.11/151.91  (step @p612 :rule trust :premises () :args ((= @t6 (not @t847))))
% 151.11/151.91  (step @p613 :rule eq_resolve :premises (@p3 @p612))
% 151.11/151.91  (step @p614 :rule cnf_or_pos :args (@t863))
% 151.11/151.91  (step @p615 :rule reordering :premises (@p614) :args ((or @t847 @t862 (not @t863))))
% 151.11/151.91  (step @p616 :rule chain_m_resolution :premises (@p615 @p613 @p611) :args (@t862 @t864 (@list @t847 @t863)))
% 151.11/151.91  ; trust TRUST PREPROCESS_HO_ELIM
% 151.11/151.91  (step @p617 :rule trust :premises () :args ((= (= @t1 @t5) @t834)))
% 151.11/151.91  (step @p618 :rule eq-symm :args (@t5 @t1))
% 151.11/151.91  (step @p619 :rule trans :premises (@p618 @p617 @p571))
% 151.11/151.91  (step @p620 :rule eq_resolve :premises (@p2 @p619))
% 151.11/151.91  ; trust TRUST PREPROCESS_HO_ELIM
% 151.11/151.91  (step @p621 :rule trust :premises () :args ((= (not (= @t3 @t668)) (not @t837))))
% 151.11/151.91  (step @p622 :rule eq-symm :args (@t668 @t3))
% 151.11/151.91  (step @p623 :rule cong :premises (@p622) :args (@t669))
% 151.11/151.91  (step @p624 :rule trans :premises (@p623 @p621))
% 151.11/151.91  (step @p625 :rule eq_resolve :premises (@p333 @p624))
% 151.11/151.91  (step @p626 :rule cnf_or_pos :args (@t858))
% 151.11/151.91  (step @p627 :rule reordering :premises (@p626) :args ((or @t837 @t857 @t865)))
% 151.11/151.91  (step @p628 :rule chain_m_resolution :premises (@p627 @p625 @p620) :args (@t865 @t864 (@list @t837 @t856)))
% 151.11/151.91  (step @p629 :rule cnf_and_pos :args (@t859 0))
% 151.11/151.91  (step @p630 :rule reordering :premises (@p629) :args ((or @t858 @t866)))
% 151.11/151.92  (step @p631 :rule chain_m_resolution :premises (@p630 @p628) :args (@t866 (@list true) (@list @t858)))
% 151.11/151.92  (step @p632 :rule eq-symm :args (@t836 @t720))
% 151.11/151.92  (step @p633 :rule cong :premises (@p632) :args (@t867))
% 151.11/151.92  ; trust TRUST PREPROCESS_HO_ELIM
% 151.11/151.92  (step @p634 :rule trust :premises () :args ((= @t4 @t867)))
% 151.11/151.92  (step @p635 :rule trans :premises (@p634 @p633 @p583))
% 151.11/151.92  (step @p636 :rule eq_resolve :premises (@p1 @p635))
% 151.11/151.92  (step @p637 :rule cnf_or_pos :args (@t861))
% 151.11/151.92  (step @p638 :rule reordering :premises (@p637) :args ((or @t860 @t859 @t868)))
% 151.11/151.92  (step @p639 :rule chain_m_resolution :premises (@p638 @p636 @p631) :args (@t868 (@list true true) (@list @t860 @t859)))
% 151.11/151.92  (step @p640 :rule cnf_and_pos :args (@t862 1))
% 151.11/151.92  (step @p641 :rule reordering :premises (@p640) :args ((or @t861 (not @t862))))
% 151.11/151.92  (step @p642 false :rule chain_m_resolution :premises (@p641 @p639 @p616) :args (false @t864 (@list @t861 @t862)))
% 151.11/151.92  )
% 151.11/151.92  % SZS output end Proof
% 151.11/151.92  % cvc5 exiting
%------------------------------------------------------------------------------