cvc5---1.3.4.THM-Prf.s

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

% Computer : n027.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:09 AM UTC 2026

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

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem  : ITP136^1 : TPTP v9.2.1. Released v7.5.0.
% 0.13/0.13  % Command  : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/0.34  % Computer : n027.cluster.edu
% 0.17/0.34  % Model    : x86_64 x86_64
% 0.17/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34  % Memory   : 8042.1875MB
% 0.17/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34  % CPULimit : 300
% 0.17/0.34  % WCLimit  : 300
% 0.17/0.34  % DateTime : Tue Jun  2 04:15:36 EDT 2026
% 0.17/0.34  % CPUTime  : 
% 0.47/0.63  %----Proving TH0
% 0.48/0.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...
% 0.48/0.91  % SZS status Theorem
% 0.48/0.91  % SZS output start Proof
% 0.48/0.91  (
% 0.48/0.91  (declare-sort tptp.set_Pa1764573435lle_tv 0)
% 0.48/0.91  (declare-sort tptp.set_nat 0)
% 0.48/0.91  (declare-sort tptp.nat 0)
% 0.48/0.91  (declare-sort tptp.set_Pr2014382200lle_tv 0)
% 0.48/0.91  (declare-sort tptp.set_Pr698334450lle_tv 0)
% 0.48/0.91  (declare-sort tptp.list_char 0)
% 0.48/0.91  (declare-sort tptp.paraco1605129243lle_tv 0)
% 0.48/0.91  (declare-sort tptp.set_Pr1019238018lle_fm 0)
% 0.48/0.91  (declare-sort tptp.produc1647334210lle_tv 0)
% 0.48/0.91  (declare-sort tptp.produc1720769084lle_tv 0)
% 0.48/0.91  (declare-sort tptp.produc931990033lle_tv 0)
% 0.48/0.91  (declare-sort tptp.set_Pr1357842111at_nat 0)
% 0.48/0.91  (declare-sort tptp.produc1281043295at_nat 0)
% 0.48/0.91  (declare-sort tptp.produc1250255278lle_fm 0)
% 0.48/0.91  (declare-sort tptp.set_Pr1475944804lle_fm 0)
% 0.48/0.91  (declare-sort tptp.produc696645085lle_fm 0)
% 0.48/0.91  (declare-sort tptp.set_Pr2061825550lle_tv 0)
% 0.48/0.91  (declare-sort tptp.produc1852595672lle_tv 0)
% 0.48/0.91  (declare-sort tptp.produc450659916lle_fm 0)
% 0.48/0.91  (declare-sort tptp.paraco1604210848lle_fm 0)
% 0.48/0.91  (declare-sort tptp.set_Pr2012908090lle_tv 0)
% 0.48/0.91  (declare-sort tptp.produc194167194tv_nat 0)
% 0.48/0.91  (declare-sort tptp.set_Pr13445366lle_tv 0)
% 0.48/0.91  (declare-sort tptp.produc270694976lle_tv 0)
% 0.48/0.91  (declare-sort tptp.set_Pr560526279lle_tv 0)
% 0.48/0.91  (declare-sort tptp.product_prod_nat_nat 0)
% 0.48/0.91  (declare-sort tptp.set_Pr1986765409at_nat 0)
% 0.48/0.91  (declare-sort tptp.set_Pr1725653840tv_nat 0)
% 0.48/0.91  (declare-sort tptp.produc596913417at_nat 0)
% 0.48/0.91  (declare-sort tptp.set_Pr292927124lle_tv 0)
% 0.48/0.91  (declare-sort tptp.set_Pr2120184979lle_fm 0)
% 0.48/0.91  (declare-sort tptp.produc1443694919lle_tv 0)
% 0.48/0.91  (declare-sort tptp.set_Pr1723822845lle_tv 0)
% 0.48/0.91  (declare-sort tptp.set_Pr840833727at_nat 0)
% 0.48/0.91  (declare-sort tptp.set_Pr1490359111at_nat 0)
% 0.48/0.91  (declare-sort tptp.set_Pr1943077434tv_nat 0)
% 0.48/0.91  (declare-const tptp.paraco1344940915le_Det (-> Bool tptp.paraco1605129243lle_tv))
% 0.48/0.91  (declare-const tptp.paraco1325918602e_eval (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.paraco1604210848lle_fm tptp.paraco1605129243lle_tv))
% 0.48/0.91  (declare-const tptp.paraco1147068288nge_tv (-> (-> tptp.nat tptp.nat) tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv))
% 0.48/0.91  (declare-const tptp.top_top_o Bool)
% 0.48/0.91  (declare-const tptp.member_nat (-> tptp.nat tptp.set_nat Bool))
% 0.48/0.91  (declare-const tptp.member266900804lle_tv (-> tptp.paraco1605129243lle_tv tptp.set_Pa1764573435lle_tv Bool))
% 0.48/0.91  (declare-const tptp.if_Par1134130401lle_tv (-> Bool tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv))
% 0.48/0.91  (declare-const tptp.produc262413013lle_tv (-> tptp.produc1443694919lle_tv tptp.paraco1604210848lle_fm))
% 0.48/0.91  (declare-const tptp.produc381314067lle_tv (-> tptp.produc1443694919lle_tv tptp.list_char tptp.paraco1605129243lle_tv))
% 0.48/0.91  (declare-const tptp.produc1710735575lle_fm (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.paraco1604210848lle_fm tptp.produc696645085lle_fm))
% 0.48/0.91  (declare-const tptp.produc1589291287at_nat (-> tptp.produc596913417at_nat tptp.paraco1605129243lle_tv))
% 0.48/0.91  (declare-const tptp.produc500618325at_nat (-> tptp.produc596913417at_nat tptp.nat tptp.nat))
% 0.48/0.91  (declare-const tptp.produc1680557635lle_tv (-> (-> tptp.nat tptp.nat) tptp.paraco1605129243lle_tv tptp.produc931990033lle_tv))
% 0.48/0.91  (declare-const tptp.ord_le241064091lle_tv (-> tptp.set_Pa1764573435lle_tv tptp.set_Pa1764573435lle_tv Bool))
% 0.48/0.91  (declare-const tptp.ord_less_eq_set_nat (-> tptp.set_nat tptp.set_nat Bool))
% 0.48/0.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))
% 0.48/0.91  (declare-const tptp.wf_Par1378404612lle_tv (-> tptp.set_Pr2014382200lle_tv Bool))
% 0.48/0.91  (declare-const tptp.wf_nat (-> tptp.set_Pr1986765409at_nat Bool))
% 0.48/0.91  (declare-const tptp.member1339857875lle_tv (-> tptp.produc1720769084lle_tv tptp.set_Pr698334450lle_tv Bool))
% 0.48/0.91  (declare-const tptp.produc2057188974lle_tv (-> tptp.produc931990033lle_tv tptp.produc931990033lle_tv tptp.produc1720769084lle_tv))
% 0.48/0.91  (declare-const tptp.lex_pr1093414955lle_tv (-> tptp.set_Pr1357842111at_nat tptp.set_Pr2014382200lle_tv tptp.set_Pr698334450lle_tv))
% 0.48/0.91  (declare-const tptp.produc780837143at_nat (-> (-> tptp.nat tptp.nat) (-> tptp.nat tptp.nat) tptp.produc1281043295at_nat))
% 0.48/0.91  (declare-const tptp.produc2058540732lle_tv (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv tptp.produc1647334210lle_tv))
% 0.48/0.91  (declare-const tptp.member1592865093lle_fm (-> tptp.produc1250255278lle_fm tptp.set_Pr1475944804lle_fm Bool))
% 0.48/0.91  (declare-const tptp.produc407632608lle_fm (-> tptp.produc696645085lle_fm tptp.produc696645085lle_fm tptp.produc1250255278lle_fm))
% 0.48/0.91  (declare-const tptp.lex_pr2001015487lle_fm (-> tptp.set_Pr2061825550lle_tv tptp.set_Pr1019238018lle_fm tptp.set_Pr1475944804lle_fm))
% 0.48/0.91  (declare-const tptp.produc1297923922lle_tv (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.produc1852595672lle_tv))
% 0.48/0.91  (declare-const tptp.produc1126104134lle_fm (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm tptp.produc450659916lle_fm))
% 0.48/0.91  (declare-const tptp.total_92239038lle_tv (-> tptp.set_Pr2014382200lle_tv tptp.set_Pr2012908090lle_tv Bool))
% 0.48/0.91  (declare-const tptp.lex_pr567812260lle_tv (-> tptp.set_Pr2014382200lle_tv tptp.set_Pr2014382200lle_tv tptp.set_Pr2012908090lle_tv))
% 0.48/0.91  (declare-const tptp.total_440843542tv_nat (-> tptp.set_Pr1725653840tv_nat tptp.set_Pr1943077434tv_nat Bool))
% 0.48/0.91  (declare-const tptp.the_in452116896lle_tv (-> tptp.set_Pa1764573435lle_tv (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv))
% 0.48/0.91  (declare-const tptp.the_inv_into_nat_nat (-> tptp.set_nat (-> tptp.nat tptp.nat) tptp.nat tptp.nat))
% 0.48/0.91  (declare-const tptp.accp_P2085826120lle_tv (-> (-> tptp.produc931990033lle_tv tptp.produc931990033lle_tv Bool) tptp.produc931990033lle_tv Bool))
% 0.48/0.91  (declare-const tptp.lex_pr1785529980tv_nat (-> tptp.set_Pr2014382200lle_tv tptp.set_Pr1986765409at_nat tptp.set_Pr1943077434tv_nat))
% 0.48/0.91  (declare-const tptp.collec7649004at_nat (-> (-> tptp.product_prod_nat_nat Bool) tptp.set_Pr1986765409at_nat))
% 0.48/0.91  (declare-const tptp.top_to900819589_nat_o (-> tptp.produc194167194tv_nat Bool))
% 0.48/0.91  (declare-const tptp.paraco1480028776le_Pro (-> tptp.list_char tptp.paraco1604210848lle_fm))
% 0.48/0.91  (declare-const tptp.member1234290208at_nat (-> tptp.produc596913417at_nat tptp.set_Pr840833727at_nat Bool))
% 0.48/0.91  (declare-const tptp.collec1111687558lle_tv (-> (-> tptp.paraco1605129243lle_tv Bool) tptp.set_Pa1764573435lle_tv))
% 0.48/0.91  (declare-const tptp.paraco793048302_Indet (-> tptp.nat tptp.paraco1605129243lle_tv))
% 0.48/0.91  (declare-const tptp.collec791369802at_nat (-> (-> tptp.produc1281043295at_nat Bool) tptp.set_Pr1357842111at_nat))
% 0.48/0.91  (declare-const tptp.collec1624074086lle_tv (-> (-> tptp.produc931990033lle_tv Bool) tptp.set_Pr560526279lle_tv))
% 0.48/0.91  (declare-const tptp.collec1102043437lle_tv (-> (-> tptp.produc1852595672lle_tv Bool) tptp.set_Pr2061825550lle_tv))
% 0.48/0.91  (declare-const tptp.collec835549234lle_fm (-> (-> tptp.produc696645085lle_fm Bool) tptp.set_Pr2120184979lle_fm))
% 0.48/0.91  (declare-const tptp.i (-> tptp.list_char tptp.paraco1605129243lle_tv))
% 0.48/0.91  (declare-const tptp.paraco55203475lid_in (-> tptp.set_nat tptp.paraco1604210848lle_fm Bool))
% 0.48/0.91  (declare-const tptp.inj_on1745913142lle_tv (-> (-> tptp.produc270694976lle_tv tptp.produc270694976lle_tv) tptp.set_Pr13445366lle_tv Bool))
% 0.48/0.91  (declare-const tptp.inj_on2112487900lle_tv (-> (-> tptp.produc1647334210lle_tv tptp.produc1647334210lle_tv) tptp.set_Pr2014382200lle_tv Bool))
% 0.48/0.91  (declare-const tptp.inv_image_nat_nat (-> tptp.set_Pr1986765409at_nat (-> tptp.nat tptp.nat) tptp.set_Pr1986765409at_nat))
% 0.48/0.91  (declare-const tptp.produc1942165868lle_fm (-> (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.list_char tptp.paraco1605129243lle_tv) tptp.produc696645085lle_fm tptp.produc696645085lle_fm))
% 0.48/0.91  (declare-const tptp.top_top_set_nat tptp.set_nat)
% 0.48/0.91  (declare-const tptp.collec924990229lle_tv (-> (-> tptp.produc270694976lle_tv Bool) tptp.set_Pr13445366lle_tv))
% 0.48/0.91  (declare-const tptp.paraco69239110le_Con (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm))
% 0.48/0.91  (declare-const tptp.member813679063lle_tv (-> tptp.produc270694976lle_tv tptp.set_Pr13445366lle_tv Bool))
% 0.48/0.91  (declare-const tptp.member334644067lle_fm (-> tptp.produc450659916lle_fm tptp.set_Pr1019238018lle_fm Bool))
% 0.48/0.91  (declare-const tptp.paraco1389086619le_Eql (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm))
% 0.48/0.91  (declare-const tptp.total_1775715973at_nat (-> tptp.set_Pr1986765409at_nat tptp.set_Pr1490359111at_nat Bool))
% 0.48/0.91  (declare-const tptp.member737151281tv_nat (-> tptp.produc194167194tv_nat tptp.set_Pr1725653840tv_nat Bool))
% 0.48/0.91  (declare-const tptp.member1531318361lle_tv (-> tptp.produc1647334210lle_tv tptp.set_Pr2014382200lle_tv Bool))
% 0.48/0.91  (declare-const tptp.paraco367965286_Truth tptp.paraco1604210848lle_fm)
% 0.48/0.91  (declare-const tptp.image_149830562lle_tv (-> (-> tptp.produc270694976lle_tv tptp.produc270694976lle_tv) tptp.set_Pr13445366lle_tv tptp.set_Pr13445366lle_tv))
% 0.48/0.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))
% 0.48/0.91  (declare-const tptp.paraco1745535428le_Eql (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm))
% 0.48/0.91  (declare-const tptp.member74361182lle_tv (-> tptp.produc1443694919lle_tv tptp.set_Pr1723822845lle_tv Bool))
% 0.48/0.91  (declare-const tptp.paraco445776468le_Neg (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm))
% 0.48/0.91  (declare-const tptp.top_to1871154984lle_tv tptp.set_Pr2014382200lle_tv)
% 0.48/0.91  (declare-const tptp.member1474794996lle_fm (-> tptp.produc696645085lle_fm tptp.set_Pr2120184979lle_fm Bool))
% 0.48/0.91  (declare-const tptp.top_to632227436_nat_o (-> tptp.product_prod_nat_nat Bool))
% 0.48/0.91  (declare-const tptp.top_to1889334367e_tv_o (-> tptp.produc270694976lle_tv Bool))
% 0.48/0.91  (declare-const tptp.p1 tptp.paraco1604210848lle_fm)
% 0.48/0.91  (declare-const tptp.same_f1138187694lle_tv (-> (-> (-> tptp.nat tptp.nat) Bool) (-> (-> tptp.nat tptp.nat) tptp.set_Pr2014382200lle_tv) tptp.set_Pr698334450lle_tv))
% 0.48/0.91  (declare-const tptp.top_to1057771083lle_tv tptp.set_Pa1764573435lle_tv)
% 0.48/0.91  (declare-const tptp.produc1000205111lle_fm (-> tptp.produc696645085lle_fm tptp.produc1443694919lle_tv))
% 0.48/0.91  (declare-const tptp.produc939316703lle_tv (-> (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat) tptp.produc931990033lle_tv tptp.produc931990033lle_tv))
% 0.48/0.91  (declare-const tptp.top_to775056195lle_fm tptp.set_Pr2120184979lle_fm)
% 0.48/0.91  (declare-const tptp.produc225513635lle_tv (-> tptp.produc931990033lle_tv tptp.produc596913417at_nat))
% 0.48/0.91  (declare-const tptp.inj_on26176689at_nat (-> (-> tptp.product_prod_nat_nat tptp.product_prod_nat_nat) tptp.set_Pr1986765409at_nat Bool))
% 0.48/0.91  (declare-const tptp.produc1250721397at_nat (-> (-> tptp.nat tptp.paraco1605129243lle_tv) (-> tptp.nat tptp.nat) tptp.product_prod_nat_nat tptp.produc194167194tv_nat))
% 0.48/0.91  (declare-const tptp.collec848462447tv_nat (-> (-> tptp.produc194167194tv_nat Bool) tptp.set_Pr1725653840tv_nat))
% 0.48/0.91  (declare-const tptp.p2 tptp.paraco1604210848lle_fm)
% 0.48/0.91  (declare-const tptp.top_to138697918lle_tv tptp.set_Pr2061825550lle_tv)
% 0.48/0.91  (declare-const tptp.top_to449985143lle_tv tptp.set_Pr560526279lle_tv)
% 0.48/0.91  (declare-const tptp.image_1221801032lle_tv (-> (-> tptp.produc1647334210lle_tv tptp.produc1647334210lle_tv) tptp.set_Pr2014382200lle_tv tptp.set_Pr2014382200lle_tv))
% 0.48/0.91  (declare-const tptp.inj_on552895452tv_nat (-> (-> tptp.produc194167194tv_nat tptp.produc194167194tv_nat) tptp.set_Pr1725653840tv_nat Bool))
% 0.48/0.91  (declare-const tptp.produc1975500101lle_tv (-> (-> tptp.nat tptp.paraco1605129243lle_tv) (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.produc270694976lle_tv tptp.produc1647334210lle_tv))
% 0.48/0.91  (declare-const tptp.member1569366824lle_tv (-> tptp.produc931990033lle_tv tptp.set_Pr560526279lle_tv Bool))
% 0.48/0.91  (declare-const tptp.paraco1632582009tv_rel (-> tptp.produc931990033lle_tv tptp.produc931990033lle_tv Bool))
% 0.48/0.91  (declare-const tptp.top_to1541413903at_nat tptp.set_Pr1357842111at_nat)
% 0.48/0.91  (declare-const tptp.f (-> tptp.nat tptp.nat))
% 0.48/0.91  (declare-const tptp.paraco2051596139lle_tv (-> (-> Bool tptp.paraco1605129243lle_tv) (-> tptp.nat tptp.paraco1605129243lle_tv) tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv))
% 0.48/0.91  (declare-const tptp.member112824072at_nat (-> tptp.produc1281043295at_nat tptp.set_Pr1357842111at_nat Bool))
% 0.48/0.91  (declare-const tptp.member146333935lle_tv (-> tptp.produc1852595672lle_tv tptp.set_Pr2061825550lle_tv Bool))
% 0.48/0.91  (declare-const tptp.top_to1411004326lle_tv tptp.set_Pr13445366lle_tv)
% 0.48/0.91  (declare-const tptp.top_to975729152tv_nat tptp.set_Pr1725653840tv_nat)
% 0.48/0.91  (declare-const tptp.collect_nat (-> (-> tptp.nat Bool) tptp.set_nat))
% 0.48/0.91  (declare-const tptp.top_to1555900337at_nat tptp.set_Pr1986765409at_nat)
% 0.48/0.91  (declare-const tptp.member701585322at_nat (-> tptp.product_prod_nat_nat tptp.set_Pr1986765409at_nat Bool))
% 0.48/0.91  (declare-const tptp.produc1807466521lle_tv (-> (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm) tptp.produc696645085lle_fm tptp.produc696645085lle_fm))
% 0.48/0.91  (declare-const tptp.produc109093078at_nat (-> (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.produc931990033lle_tv tptp.produc931990033lle_tv))
% 0.48/0.91  (declare-const tptp.image_1585092542lle_fm (-> (-> tptp.produc931990033lle_tv tptp.produc696645085lle_fm) tptp.set_Pr560526279lle_tv tptp.set_Pr2120184979lle_fm))
% 0.48/0.91  (declare-const tptp.produc505105722at_nat (-> (-> tptp.nat tptp.nat) (-> tptp.nat tptp.nat) tptp.product_prod_nat_nat tptp.product_prod_nat_nat))
% 0.48/0.91  (declare-const tptp.produc2101297531lle_tv (-> (-> tptp.nat tptp.nat) (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.produc270694976lle_tv tptp.produc270694976lle_tv))
% 0.48/0.91  (declare-const tptp.produc42536895at_nat (-> (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) (-> tptp.nat tptp.nat) tptp.produc194167194tv_nat tptp.produc194167194tv_nat))
% 0.48/0.91  (declare-const tptp.produc1345917071lle_tv (-> (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.produc1647334210lle_tv tptp.produc1647334210lle_tv))
% 0.48/0.91  (declare-const tptp.produc275353523e_fm_o (-> (-> tptp.produc696645085lle_fm Bool) (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.paraco1604210848lle_fm Bool))
% 0.48/0.91  (declare-const tptp.image_1724396928at_nat (-> (-> tptp.produc931990033lle_tv tptp.produc596913417at_nat) tptp.set_Pr560526279lle_tv tptp.set_Pr840833727at_nat))
% 0.48/0.91  (declare-const tptp.produc752649287e_tv_o (-> (-> tptp.produc931990033lle_tv Bool) (-> tptp.nat tptp.nat) tptp.paraco1605129243lle_tv Bool))
% 0.48/0.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))
% 0.48/0.91  (declare-const tptp.image_1674248956lle_tv (-> (-> tptp.product_prod_nat_nat tptp.produc270694976lle_tv) tptp.set_Pr1986765409at_nat tptp.set_Pr13445366lle_tv))
% 0.48/0.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))
% 0.48/0.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))
% 0.48/0.91  (declare-const tptp.image_nat_nat (-> (-> tptp.nat tptp.nat) tptp.set_nat tptp.set_nat))
% 0.48/0.91  (declare-const tptp.image_335818702lle_tv (-> (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.set_Pa1764573435lle_tv tptp.set_Pa1764573435lle_tv))
% 0.48/0.91  (declare-const tptp.image_807538418lle_fm (-> (-> tptp.produc696645085lle_fm tptp.produc696645085lle_fm) tptp.set_Pr2120184979lle_fm tptp.set_Pr2120184979lle_fm))
% 0.48/0.91  (declare-const tptp.image_1154804148lle_tv (-> (-> tptp.produc696645085lle_fm tptp.produc931990033lle_tv) tptp.set_Pr2120184979lle_fm tptp.set_Pr560526279lle_tv))
% 0.48/0.91  (declare-const tptp.image_1751508608lle_tv (-> (-> tptp.produc931990033lle_tv tptp.produc931990033lle_tv) tptp.set_Pr560526279lle_tv tptp.set_Pr560526279lle_tv))
% 0.48/0.91  (declare-const tptp.produc1943344577lle_tv (-> tptp.paraco1604210848lle_fm (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.produc1443694919lle_tv))
% 0.48/0.91  (declare-const tptp.produc1633679363at_nat (-> tptp.paraco1605129243lle_tv (-> tptp.nat tptp.nat) tptp.produc596913417at_nat))
% 0.48/0.91  (declare-const tptp.image_924970994lle_tv (-> (-> tptp.produc696645085lle_fm tptp.produc1443694919lle_tv) tptp.set_Pr2120184979lle_fm tptp.set_Pr1723822845lle_tv))
% 0.48/0.91  (declare-const tptp.image_326034184lle_fm (-> (-> tptp.produc1443694919lle_tv tptp.produc696645085lle_fm) tptp.set_Pr1723822845lle_tv tptp.set_Pr2120184979lle_fm))
% 0.48/0.91  (declare-const tptp.image_769496456lle_tv (-> (-> tptp.produc596913417at_nat tptp.produc931990033lle_tv) tptp.set_Pr840833727at_nat tptp.set_Pr560526279lle_tv))
% 0.48/0.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))
% 0.48/0.91  (declare-const tptp.produc313957681lle_tv (-> (-> tptp.nat tptp.nat) (-> tptp.nat tptp.paraco1605129243lle_tv) tptp.product_prod_nat_nat tptp.produc270694976lle_tv))
% 0.48/0.91  (declare-const tptp.inj_on1955349912lle_tv (-> (-> tptp.nat tptp.paraco1605129243lle_tv) tptp.set_nat Bool))
% 0.48/0.91  (declare-const tptp.image_53754658tv_nat (-> (-> tptp.produc270694976lle_tv tptp.produc194167194tv_nat) tptp.set_Pr13445366lle_tv tptp.set_Pr1725653840tv_nat))
% 0.48/0.91  (declare-const tptp.image_988201162lle_tv (-> (-> tptp.produc270694976lle_tv tptp.produc1647334210lle_tv) tptp.set_Pr13445366lle_tv tptp.set_Pr2014382200lle_tv))
% 0.48/0.91  (declare-const tptp.inj_on1179712058tv_nat (-> (-> tptp.paraco1605129243lle_tv tptp.nat) tptp.set_Pa1764573435lle_tv Bool))
% 0.48/0.91  (declare-const tptp.image_1151963140lle_tv (-> (-> tptp.nat tptp.paraco1605129243lle_tv) tptp.set_nat tptp.set_Pa1764573435lle_tv))
% 0.48/0.91  (declare-const tptp.produc1685803475tv_nat (-> (-> tptp.nat tptp.nat) (-> tptp.paraco1605129243lle_tv tptp.nat) tptp.produc270694976lle_tv tptp.product_prod_nat_nat))
% 0.48/0.91  (declare-const tptp.image_1787705850at_nat (-> (-> tptp.produc270694976lle_tv tptp.product_prod_nat_nat) tptp.set_Pr13445366lle_tv tptp.set_Pr1986765409at_nat))
% 0.48/0.91  (declare-const tptp.image_376325286tv_nat (-> (-> tptp.paraco1605129243lle_tv tptp.nat) tptp.set_Pa1764573435lle_tv tptp.set_nat))
% 0.48/0.91  (declare-const tptp.image_1597721174tv_nat (-> (-> tptp.product_prod_nat_nat tptp.produc194167194tv_nat) tptp.set_Pr1986765409at_nat tptp.set_Pr1725653840tv_nat))
% 0.48/0.91  (declare-const tptp.produc210389789lle_tv (-> (-> tptp.nat tptp.paraco1605129243lle_tv) (-> tptp.nat tptp.paraco1605129243lle_tv) tptp.product_prod_nat_nat tptp.produc1647334210lle_tv))
% 0.48/0.91  (declare-const tptp.image_1507992062lle_tv (-> (-> tptp.product_prod_nat_nat tptp.produc1647334210lle_tv) tptp.set_Pr1986765409at_nat tptp.set_Pr2014382200lle_tv))
% 0.48/0.91  (declare-const tptp.produc189459613tv_nat (-> (-> tptp.nat tptp.paraco1605129243lle_tv) (-> tptp.paraco1605129243lle_tv tptp.nat) tptp.produc270694976lle_tv tptp.produc194167194tv_nat))
% 0.48/0.91  (declare-const tptp.image_1805124128at_nat (-> (-> tptp.produc194167194tv_nat tptp.product_prod_nat_nat) tptp.set_Pr1725653840tv_nat tptp.set_Pr1986765409at_nat))
% 0.48/0.91  (declare-const tptp.produc386540311at_nat (-> (-> tptp.paraco1605129243lle_tv tptp.nat) (-> tptp.nat tptp.nat) tptp.produc194167194tv_nat tptp.product_prod_nat_nat))
% 0.48/0.91  (declare-const tptp.produc72207551lle_tv (-> (-> tptp.paraco1605129243lle_tv tptp.nat) (-> tptp.nat tptp.paraco1605129243lle_tv) tptp.produc194167194tv_nat tptp.produc270694976lle_tv))
% 0.48/0.91  (declare-const tptp.image_1200372424lle_tv (-> (-> tptp.produc194167194tv_nat tptp.produc270694976lle_tv) tptp.set_Pr1725653840tv_nat tptp.set_Pr13445366lle_tv))
% 0.48/0.91  (declare-const tptp.total_on_nat (-> tptp.set_nat tptp.set_Pr1986765409at_nat Bool))
% 0.48/0.91  (declare-const tptp.inv_im516950809tv_nat (-> tptp.set_Pr2014382200lle_tv (-> tptp.nat tptp.paraco1605129243lle_tv) tptp.set_Pr1986765409at_nat))
% 0.48/0.91  (declare-const tptp.total_1781621663lle_tv (-> tptp.set_Pa1764573435lle_tv tptp.set_Pr2014382200lle_tv Bool))
% 0.48/0.91  (declare-const tptp.inv_im1292588663lle_tv (-> tptp.set_Pr1986765409at_nat (-> tptp.paraco1605129243lle_tv tptp.nat) tptp.set_Pr2014382200lle_tv))
% 0.48/0.91  (declare-const tptp.inv_im719552961lle_tv (-> tptp.set_Pr2014382200lle_tv (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv) tptp.set_Pr2014382200lle_tv))
% 0.48/0.91  (declare-const tptp.produc148705065lle_fm (-> tptp.produc696645085lle_fm tptp.paraco1604210848lle_fm))
% 0.48/0.91  (declare-const tptp.produc29804011lle_fm (-> tptp.produc696645085lle_fm tptp.list_char tptp.paraco1605129243lle_tv))
% 0.48/0.91  (declare-const tptp.produc547496597lle_tv (-> tptp.produc931990033lle_tv tptp.paraco1605129243lle_tv))
% 0.48/0.91  (declare-const tptp.produc1636169559lle_tv (-> tptp.produc931990033lle_tv tptp.nat tptp.nat))
% 0.48/0.91  (declare-const tptp.lex_prod_nat_nat (-> tptp.set_Pr1986765409at_nat tptp.set_Pr1986765409at_nat tptp.set_Pr1490359111at_nat))
% 0.48/0.91  (declare-const tptp.lex_pr413684186lle_tv (-> tptp.set_Pr1986765409at_nat tptp.set_Pr2014382200lle_tv tptp.set_Pr292927124lle_tv))
% 0.48/0.91  (declare-const tptp.total_517371324lle_tv (-> tptp.set_Pr13445366lle_tv tptp.set_Pr292927124lle_tv Bool))
% 0.48/0.91  (define tptp.paraco327635598_valid () (let ((_let_1 (@var "P" tptp.paraco1604210848lle_fm))) (let ((_let_2 (@var "I" (-> 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)))))))
% 0.48/0.91  (define tptp.paraco761681009ge_int () (let ((_let_1 (@var "S" tptp.list_char))) (let ((_let_2 (@var "I" (-> tptp.list_char tptp.paraco1605129243lle_tv)))) (let ((_let_3 (@var "F" (-> tptp.nat tptp.nat)))) (lambda (@list _let_3 _let_2 _let_1) (_ (_ tptp.paraco1147068288nge_tv _let_3) (_ _let_2 _let_1)))))))
% 0.48/0.91  (define tptp.top_to1299250770e_tv_o () (lambda (@list (@var "X2" tptp.paraco1605129243lle_tv)) tptp.top_top_o))
% 0.48/0.91  (define tptp.top_top_nat_o () (lambda (@list (@var "X2" tptp.nat)) tptp.top_top_o))
% 0.48/0.91  (define tptp.inj_on_nat_nat () (let ((_let_1 (@var "Y4" tptp.nat))) (let ((_let_2 (@var "X2" tptp.nat))) (let ((_let_3 (@var "F" (-> tptp.nat tptp.nat)))) (let ((_let_4 (@var "A4" 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))))))))))))
% 0.48/0.91  (define tptp.inj_on772319074lle_tv () (let ((_let_1 (@var "Y4" tptp.paraco1605129243lle_tv))) (let ((_let_2 (@var "X2" tptp.paraco1605129243lle_tv))) (let ((_let_3 (@var "F" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv)))) (let ((_let_4 (@var "A4" 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))))))))))))
% 0.48/0.91  (define tptp.produc234482697lle_tv () (let ((_let_1 (@var "F22" 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))))))
% 0.48/0.91  (define tptp.produc1232814113lle_tv () (let ((_let_1 (@var "P" tptp.produc1443694919lle_tv))) (lambda (@list _let_1) (_ (_ tptp.produc1710735575lle_fm (_ tptp.produc381314067lle_tv _let_1)) (_ tptp.produc262413013lle_tv _let_1)))))
% 0.48/0.91  (define tptp.produc178635363at_nat () (let ((_let_1 (@var "P" tptp.produc596913417at_nat))) (lambda (@list _let_1) (_ (_ tptp.produc1680557635lle_tv (_ tptp.produc500618325at_nat _let_1)) (_ tptp.produc1589291287at_nat _let_1)))))
% 0.48/0.91  (define @t1 () (_ tptp.paraco1344940915le_Det true))
% 0.48/0.91  (define @t2 () (_ tptp.paraco1325918602e_eval tptp.i))
% 0.48/0.91  (define @t3 () (_ @t2 tptp.p2))
% 0.48/0.91  (define @t4 () (= @t3 @t1))
% 0.48/0.91  (define @t5 () (not @t4))
% 0.48/0.91  (define @t6 () (_ @t2 tptp.p1))
% 0.48/0.91  (define @t7 () (_ tptp.paraco1344940915le_Det false))
% 0.48/0.91  (define @t8 () (_ tptp.paraco1325918602e_eval (_ (_ tptp.paraco761681009ge_int tptp.f) tptp.i)))
% 0.48/0.91  (define @t9 () (_ @t8 tptp.p1))
% 0.48/0.91  (define @t10 () (= @t3 @t7))
% 0.48/0.91  (define @t11 () (_ @t8 tptp.p2))
% 0.48/0.91  (define @t12 () (= @t11 @t7))
% 0.48/0.91  (define @t13 () (@var "Y1" Bool))
% 0.48/0.91  (define @t14 () (@var "X1" Bool))
% 0.48/0.91  (define @t15 () (_ tptp.paraco1344940915le_Det @t14))
% 0.48/0.91  (define @t16 () (_ tptp.paraco1147068288nge_tv tptp.f))
% 0.48/0.91  (define @t17 () (_ @t16 @t3))
% 0.48/0.91  (define @t18 () (@var "I2" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t19 () (_ tptp.paraco1325918602e_eval @t18))
% 0.48/0.91  (define @t20 () (@var "Q" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t21 () (@var "P2" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t22 () (_ @t19 (_ (_ tptp.paraco1389086619le_Eql @t21) @t20)))
% 0.48/0.91  (define @t23 () (_ @t19 @t20))
% 0.48/0.91  (define @t24 () (_ @t19 @t21))
% 0.48/0.91  (define @t25 () (= @t24 @t23))
% 0.48/0.91  (define @t26 () (not @t25))
% 0.48/0.91  (define @t27 () (@list @t18 @t21 @t20))
% 0.48/0.91  (define @t28 () (_ (_ tptp.paraco69239110le_Con @t21) @t20))
% 0.48/0.91  (define @t29 () (_ @t19 @t28))
% 0.48/0.91  (define @t30 () (= @t23 @t1))
% 0.48/0.91  (define @t31 () (not @t30))
% 0.48/0.91  (define @t32 () (= @t29 @t24))
% 0.48/0.91  (define @t33 () (= @t24 @t1))
% 0.48/0.91  (define @t34 () (not @t33))
% 0.48/0.91  (define @t35 () (@var "F1" (-> Bool tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t36 () (@var "F2" (-> tptp.nat tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t37 () (_ (_ tptp.paraco2051596139lle_tv @t35) @t36))
% 0.48/0.91  (define @t38 () (_ @t19 (_ tptp.paraco445776468le_Neg @t21)))
% 0.48/0.91  (define @t39 () (= @t24 @t7))
% 0.48/0.91  (define @t40 () (not @t39))
% 0.48/0.91  (define @t41 () (@list @t18 @t21))
% 0.48/0.91  (define @t42 () (@var "B" Bool))
% 0.48/0.91  (define @t43 () (_ tptp.paraco1344940915le_Det @t42))
% 0.48/0.91  (define @t44 () (@var "F3" (-> tptp.nat tptp.nat)))
% 0.48/0.91  (define @t45 () (_ tptp.paraco1147068288nge_tv @t44))
% 0.48/0.91  (define @t46 () (@var "Y3" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t47 () (@var "X3" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t48 () (_ tptp.paraco445776468le_Neg @t47))
% 0.48/0.91  (define @t49 () (@var "Y42" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t50 () (@var "X42" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t51 () (@var "Y41" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t52 () (@var "X41" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t53 () (_ (_ tptp.paraco69239110le_Con @t52) @t50))
% 0.48/0.91  (define @t54 () (@var "Y62" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t55 () (@var "X62" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t56 () (@var "Y61" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t57 () (@var "X61" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t58 () (_ (_ tptp.paraco1745535428le_Eql @t57) @t55))
% 0.48/0.91  (define @t59 () (@var "Y52" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t60 () (@var "X52" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t61 () (@var "Y51" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t62 () (@var "X51" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t63 () (_ (_ tptp.paraco1389086619le_Eql @t62) @t60))
% 0.48/0.91  (define @t64 () (_ tptp.paraco327635598_valid @t21))
% 0.48/0.91  (define @t65 () (_ @t19 (_ (_ tptp.paraco1745535428le_Eql @t21) @t20)))
% 0.48/0.91  (define @t66 () (= @t23 @t7))
% 0.48/0.91  (define @t67 () (@var "P" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t68 () (@var "I" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t69 () (_ tptp.paraco1325918602e_eval @t68))
% 0.48/0.91  (define @t70 () (@var "X" tptp.produc696645085lle_fm))
% 0.48/0.91  (define @t71 () (@list @t70))
% 0.48/0.91  (define @t72 () (@var "X" tptp.produc1852595672lle_tv))
% 0.48/0.91  (define @t73 () (@var "X" tptp.produc931990033lle_tv))
% 0.48/0.91  (define @t74 () (@list @t73))
% 0.48/0.91  (define @t75 () (@var "X" tptp.produc1281043295at_nat))
% 0.48/0.91  (define @t76 () (@var "X" tptp.produc194167194tv_nat))
% 0.48/0.91  (define @t77 () (_ tptp.member737151281tv_nat @t76))
% 0.48/0.91  (define @t78 () (@var "X" tptp.produc270694976lle_tv))
% 0.48/0.91  (define @t79 () (_ tptp.member813679063lle_tv @t78))
% 0.48/0.91  (define @t80 () (@var "X" tptp.product_prod_nat_nat))
% 0.48/0.91  (define @t81 () (_ tptp.member701585322at_nat @t80))
% 0.48/0.91  (define @t82 () (@var "X" tptp.nat))
% 0.48/0.91  (define @t83 () (_ tptp.member_nat @t82))
% 0.48/0.91  (define @t84 () (@var "X" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t85 () (_ tptp.member266900804lle_tv @t84))
% 0.48/0.91  (define @t86 () (@list @t84))
% 0.48/0.91  (define @t87 () (@var "Y" tptp.produc1647334210lle_tv))
% 0.48/0.91  (define @t88 () (@var "X" tptp.produc1647334210lle_tv))
% 0.48/0.91  (define @t89 () (= @t88 @t87))
% 0.48/0.91  (define @t90 () (@var "F3" (-> tptp.produc1647334210lle_tv tptp.produc1647334210lle_tv)))
% 0.48/0.91  (define @t91 () (= (_ @t90 @t88) (_ @t90 @t87)))
% 0.48/0.91  (define @t92 () (_ tptp.inj_on2112487900lle_tv @t90))
% 0.48/0.91  (define @t93 () (_ @t92 tptp.top_to1871154984lle_tv))
% 0.48/0.91  (define @t94 () (@list @t90 @t88 @t87))
% 0.48/0.91  (define @t95 () (@var "Y" tptp.nat))
% 0.48/0.91  (define @t96 () (= @t82 @t95))
% 0.48/0.91  (define @t97 () (@var "F3" (-> tptp.nat tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t98 () (= (_ @t97 @t82) (_ @t97 @t95)))
% 0.48/0.91  (define @t99 () (_ tptp.inj_on1955349912lle_tv @t97))
% 0.48/0.91  (define @t100 () (_ @t99 tptp.top_top_set_nat))
% 0.48/0.91  (define @t101 () (@list @t97 @t82 @t95))
% 0.48/0.91  (define @t102 () (@var "Y" tptp.produc194167194tv_nat))
% 0.48/0.91  (define @t103 () (= @t76 @t102))
% 0.48/0.91  (define @t104 () (@var "F3" (-> tptp.produc194167194tv_nat tptp.produc194167194tv_nat)))
% 0.48/0.91  (define @t105 () (= (_ @t104 @t76) (_ @t104 @t102)))
% 0.48/0.91  (define @t106 () (_ tptp.inj_on552895452tv_nat @t104))
% 0.48/0.91  (define @t107 () (_ @t106 tptp.top_to975729152tv_nat))
% 0.48/0.91  (define @t108 () (@list @t104 @t76 @t102))
% 0.48/0.91  (define @t109 () (@var "Y" tptp.produc270694976lle_tv))
% 0.48/0.91  (define @t110 () (= @t78 @t109))
% 0.48/0.91  (define @t111 () (@var "F3" (-> tptp.produc270694976lle_tv tptp.produc270694976lle_tv)))
% 0.48/0.91  (define @t112 () (= (_ @t111 @t78) (_ @t111 @t109)))
% 0.48/0.91  (define @t113 () (_ tptp.inj_on1745913142lle_tv @t111))
% 0.48/0.91  (define @t114 () (_ @t113 tptp.top_to1411004326lle_tv))
% 0.48/0.91  (define @t115 () (@list @t111 @t78 @t109))
% 0.48/0.91  (define @t116 () (@var "Y" tptp.product_prod_nat_nat))
% 0.48/0.91  (define @t117 () (= @t80 @t116))
% 0.48/0.91  (define @t118 () (@var "F3" (-> tptp.product_prod_nat_nat tptp.product_prod_nat_nat)))
% 0.48/0.91  (define @t119 () (= (_ @t118 @t80) (_ @t118 @t116)))
% 0.48/0.91  (define @t120 () (_ tptp.inj_on26176689at_nat @t118))
% 0.48/0.91  (define @t121 () (_ @t120 tptp.top_to1555900337at_nat))
% 0.48/0.91  (define @t122 () (@list @t118 @t80 @t116))
% 0.48/0.91  (define @t123 () (_ @t44 @t82))
% 0.48/0.91  (define @t124 () (= @t123 (_ @t44 @t95)))
% 0.48/0.91  (define @t125 () (_ tptp.inj_on_nat_nat @t44))
% 0.48/0.91  (define @t126 () (_ @t125 tptp.top_top_set_nat))
% 0.48/0.91  (define @t127 () (@list @t44 @t82 @t95))
% 0.48/0.91  (define @t128 () (@var "Y" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t129 () (= @t84 @t128))
% 0.48/0.91  (define @t130 () (@var "F3" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t131 () (_ @t130 @t128))
% 0.48/0.91  (define @t132 () (_ @t130 @t84))
% 0.48/0.91  (define @t133 () (= @t132 @t131))
% 0.48/0.91  (define @t134 () (_ tptp.inj_on772319074lle_tv @t130))
% 0.48/0.91  (define @t135 () (_ @t134 tptp.top_to1057771083lle_tv))
% 0.48/0.91  (define @t136 () (@list @t130 @t84 @t128))
% 0.48/0.91  (define @t137 () (@var "A" tptp.produc696645085lle_fm))
% 0.48/0.91  (define @t138 () (@var "P3" (-> tptp.produc696645085lle_fm Bool)))
% 0.48/0.91  (define @t139 () (@var "A" tptp.produc1852595672lle_tv))
% 0.48/0.91  (define @t140 () (@var "P3" (-> tptp.produc1852595672lle_tv Bool)))
% 0.48/0.91  (define @t141 () (@var "A" tptp.produc931990033lle_tv))
% 0.48/0.91  (define @t142 () (@var "P3" (-> tptp.produc931990033lle_tv Bool)))
% 0.48/0.91  (define @t143 () (@var "A" tptp.produc1281043295at_nat))
% 0.48/0.91  (define @t144 () (@var "P3" (-> tptp.produc1281043295at_nat Bool)))
% 0.48/0.91  (define @t145 () (@var "A" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t146 () (@var "P3" (-> tptp.paraco1605129243lle_tv Bool)))
% 0.48/0.91  (define @t147 () (_ tptp.collec1111687558lle_tv @t146))
% 0.48/0.91  (define @t148 () (_ tptp.member266900804lle_tv @t145))
% 0.48/0.91  (define @t149 () (@var "A" tptp.nat))
% 0.48/0.91  (define @t150 () (@var "P3" (-> tptp.nat Bool)))
% 0.48/0.91  (define @t151 () (_ tptp.collect_nat @t150))
% 0.48/0.91  (define @t152 () (_ tptp.member_nat @t149))
% 0.48/0.91  (define @t153 () (@var "A2" tptp.set_Pr2120184979lle_fm))
% 0.48/0.91  (define @t154 () (@var "X2" tptp.produc696645085lle_fm))
% 0.48/0.91  (define @t155 () (@list @t153))
% 0.48/0.91  (define @t156 () (@var "A2" tptp.set_Pr2061825550lle_tv))
% 0.48/0.91  (define @t157 () (@var "X2" tptp.produc1852595672lle_tv))
% 0.48/0.91  (define @t158 () (@list @t156))
% 0.48/0.91  (define @t159 () (@var "A2" tptp.set_Pr560526279lle_tv))
% 0.48/0.91  (define @t160 () (@var "X2" tptp.produc931990033lle_tv))
% 0.48/0.91  (define @t161 () (@list @t159))
% 0.48/0.91  (define @t162 () (@var "A2" tptp.set_Pr1357842111at_nat))
% 0.48/0.91  (define @t163 () (@var "X2" tptp.produc1281043295at_nat))
% 0.48/0.91  (define @t164 () (@list @t162))
% 0.48/0.91  (define @t165 () (@var "A2" tptp.set_Pa1764573435lle_tv))
% 0.48/0.91  (define @t166 () (@var "X2" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t167 () (_ tptp.member266900804lle_tv @t166))
% 0.48/0.91  (define @t168 () (@list @t166))
% 0.48/0.91  (define @t169 () (@list @t165))
% 0.48/0.91  (define @t170 () (@var "A2" tptp.set_nat))
% 0.48/0.91  (define @t171 () (@var "X2" tptp.nat))
% 0.48/0.91  (define @t172 () (_ tptp.member_nat @t171))
% 0.48/0.91  (define @t173 () (@list @t171))
% 0.48/0.91  (define @t174 () (@list @t170))
% 0.48/0.91  (define @t175 () (@var "Q2" (-> tptp.paraco1605129243lle_tv Bool)))
% 0.48/0.91  (define @t176 () (@var "X4" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t177 () (@list @t176))
% 0.48/0.91  (define @t178 () (@var "Q2" (-> tptp.nat Bool)))
% 0.48/0.91  (define @t179 () (@var "X4" tptp.nat))
% 0.48/0.91  (define @t180 () (@list @t179))
% 0.48/0.91  (define @t181 () (@var "Y2" tptp.produc1647334210lle_tv))
% 0.48/0.91  (define @t182 () (@var "X4" tptp.produc1647334210lle_tv))
% 0.48/0.91  (define @t183 () (_ @t90 @t182))
% 0.48/0.91  (define @t184 () (@list @t90))
% 0.48/0.91  (define @t185 () (@var "Y2" tptp.nat))
% 0.48/0.91  (define @t186 () (= @t179 @t185))
% 0.48/0.91  (define @t187 () (_ @t97 @t179))
% 0.48/0.91  (define @t188 () (@list @t179 @t185))
% 0.48/0.91  (define @t189 () (@list @t97))
% 0.48/0.91  (define @t190 () (@var "Y2" tptp.produc194167194tv_nat))
% 0.48/0.91  (define @t191 () (@var "X4" tptp.produc194167194tv_nat))
% 0.48/0.91  (define @t192 () (_ @t104 @t191))
% 0.48/0.91  (define @t193 () (@list @t104))
% 0.48/0.91  (define @t194 () (@var "Y2" tptp.produc270694976lle_tv))
% 0.48/0.91  (define @t195 () (@var "X4" tptp.produc270694976lle_tv))
% 0.48/0.91  (define @t196 () (_ @t111 @t195))
% 0.48/0.91  (define @t197 () (@list @t111))
% 0.48/0.91  (define @t198 () (@var "Y2" tptp.product_prod_nat_nat))
% 0.48/0.91  (define @t199 () (@var "X4" tptp.product_prod_nat_nat))
% 0.48/0.91  (define @t200 () (_ @t118 @t199))
% 0.48/0.91  (define @t201 () (@list @t118))
% 0.48/0.91  (define @t202 () (_ @t44 @t179))
% 0.48/0.91  (define @t203 () (=> (= @t202 (_ @t44 @t185)) @t186))
% 0.48/0.91  (define @t204 () (@list @t44))
% 0.48/0.91  (define @t205 () (@var "Y2" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t206 () (_ @t130 @t176))
% 0.48/0.91  (define @t207 () (=> (= @t206 (_ @t130 @t205)) (= @t176 @t205)))
% 0.48/0.91  (define @t208 () (@list @t176 @t205))
% 0.48/0.91  (define @t209 () (@list @t130))
% 0.48/0.91  (define @t210 () (= @t91 @t89))
% 0.48/0.91  (define @t211 () (= @t98 @t96))
% 0.48/0.91  (define @t212 () (= @t105 @t103))
% 0.48/0.91  (define @t213 () (= @t112 @t110))
% 0.48/0.91  (define @t214 () (= @t119 @t117))
% 0.48/0.91  (define @t215 () (= @t124 @t96))
% 0.48/0.91  (define @t216 () (= @t133 @t129))
% 0.48/0.91  (define @t217 () (@var "Y4" tptp.produc1647334210lle_tv))
% 0.48/0.91  (define @t218 () (@var "X2" tptp.produc1647334210lle_tv))
% 0.48/0.91  (define @t219 () (@var "Y4" tptp.nat))
% 0.48/0.91  (define @t220 () (= @t171 @t219))
% 0.48/0.91  (define @t221 () (_ @t97 @t171))
% 0.48/0.91  (define @t222 () (@list @t171 @t219))
% 0.48/0.91  (define @t223 () (@var "Y4" tptp.produc194167194tv_nat))
% 0.48/0.91  (define @t224 () (@var "X2" tptp.produc194167194tv_nat))
% 0.48/0.91  (define @t225 () (@var "Y4" tptp.produc270694976lle_tv))
% 0.48/0.91  (define @t226 () (@var "X2" tptp.produc270694976lle_tv))
% 0.48/0.91  (define @t227 () (@var "Y4" tptp.product_prod_nat_nat))
% 0.48/0.91  (define @t228 () (@var "X2" tptp.product_prod_nat_nat))
% 0.48/0.91  (define @t229 () (_ @t44 @t219))
% 0.48/0.91  (define @t230 () (_ @t44 @t171))
% 0.48/0.91  (define @t231 () (@var "Y4" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t232 () (= @t166 @t231))
% 0.48/0.91  (define @t233 () (_ @t130 @t231))
% 0.48/0.91  (define @t234 () (_ @t130 @t166))
% 0.48/0.91  (define @t235 () (@var "Fm" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t236 () (@var "P3" (-> tptp.paraco1604210848lle_fm Bool)))
% 0.48/0.91  (define @t237 () (@var "X22" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t238 () (@var "X1a" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t239 () (_ @t236 @t237))
% 0.48/0.91  (define @t240 () (_ @t236 @t238))
% 0.48/0.91  (define @t241 () (@list @t238 @t237))
% 0.48/0.91  (define @t242 () (@var "X4" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t243 () (_ @t236 tptp.paraco367965286_Truth))
% 0.48/0.91  (define @t244 () (@var "X4" tptp.list_char))
% 0.48/0.91  (define @t245 () (@var "X622" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t246 () (@var "X612" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t247 () (@var "Y" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t248 () (@var "X522" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t249 () (@var "X512" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t250 () (@var "X422" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t251 () (@var "X412" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t252 () (@var "X32" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t253 () (@var "X12" tptp.list_char))
% 0.48/0.91  (define @t254 () (@var "Q3" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t255 () (@var "P4" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t256 () (_ (_ tptp.paraco1745535428le_Eql @t255) @t254))
% 0.48/0.91  (define @t257 () (@var "X" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t258 () (@list @t255 @t254))
% 0.48/0.91  (define @t259 () (_ (_ tptp.paraco1389086619le_Eql @t255) @t254))
% 0.48/0.91  (define @t260 () (_ (_ tptp.paraco69239110le_Con @t255) @t254))
% 0.48/0.91  (define @t261 () (_ tptp.paraco445776468le_Neg @t255))
% 0.48/0.91  (define @t262 () (@list @t255))
% 0.48/0.91  (define @t263 () (@var "S2" tptp.list_char))
% 0.48/0.91  (define @t264 () (_ tptp.paraco1480028776le_Pro @t263))
% 0.48/0.91  (define @t265 () (@list @t263))
% 0.48/0.91  (define @t266 () (@var "Y1" tptp.list_char))
% 0.48/0.91  (define @t267 () (@var "X1" tptp.list_char))
% 0.48/0.91  (define @t268 () (_ tptp.paraco1480028776le_Pro @t267))
% 0.48/0.91  (define @t269 () (@var "S3" tptp.list_char))
% 0.48/0.91  (define @t270 () (@var "X4" tptp.produc696645085lle_fm))
% 0.48/0.91  (define @t271 () (_ tptp.member1474794996lle_fm @t270))
% 0.48/0.91  (define @t272 () (@list @t270))
% 0.48/0.91  (define @t273 () (@var "X4" tptp.produc1852595672lle_tv))
% 0.48/0.91  (define @t274 () (_ tptp.member146333935lle_tv @t273))
% 0.48/0.91  (define @t275 () (@list @t273))
% 0.48/0.91  (define @t276 () (@var "X4" tptp.produc931990033lle_tv))
% 0.48/0.91  (define @t277 () (_ tptp.member1569366824lle_tv @t276))
% 0.48/0.91  (define @t278 () (@list @t276))
% 0.48/0.91  (define @t279 () (@var "X4" tptp.produc1281043295at_nat))
% 0.48/0.91  (define @t280 () (_ tptp.member112824072at_nat @t279))
% 0.48/0.91  (define @t281 () (@list @t279))
% 0.48/0.91  (define @t282 () (_ tptp.member737151281tv_nat @t191))
% 0.48/0.91  (define @t283 () (@list @t191))
% 0.48/0.91  (define @t284 () (_ tptp.member813679063lle_tv @t195))
% 0.48/0.91  (define @t285 () (@list @t195))
% 0.48/0.91  (define @t286 () (_ tptp.member701585322at_nat @t199))
% 0.48/0.91  (define @t287 () (@list @t199))
% 0.48/0.91  (define @t288 () (_ tptp.member_nat @t179))
% 0.48/0.91  (define @t289 () (_ tptp.member266900804lle_tv @t176))
% 0.48/0.91  (define @t290 () (@var "A2" tptp.set_Pr1725653840tv_nat))
% 0.48/0.91  (define @t291 () (_ @t282 @t290))
% 0.48/0.91  (define @t292 () (@var "A2" tptp.set_Pr13445366lle_tv))
% 0.48/0.91  (define @t293 () (_ @t284 @t292))
% 0.48/0.91  (define @t294 () (@var "A2" tptp.set_Pr1986765409at_nat))
% 0.48/0.91  (define @t295 () (_ @t286 @t294))
% 0.48/0.91  (define @t296 () (_ @t288 @t170))
% 0.48/0.91  (define @t297 () (_ @t289 @t165))
% 0.48/0.91  (define @t298 () (@var "A2" tptp.set_Pr2014382200lle_tv))
% 0.48/0.91  (define @t299 () (_ @t92 @t298))
% 0.48/0.91  (define @t300 () (@var "G" (-> tptp.produc1647334210lle_tv tptp.produc1647334210lle_tv)))
% 0.48/0.91  (define @t301 () (_ @t106 @t290))
% 0.48/0.91  (define @t302 () (@var "G" (-> tptp.produc194167194tv_nat tptp.produc194167194tv_nat)))
% 0.48/0.91  (define @t303 () (_ @t113 @t292))
% 0.48/0.91  (define @t304 () (@var "G" (-> tptp.produc270694976lle_tv tptp.produc270694976lle_tv)))
% 0.48/0.91  (define @t305 () (_ @t120 @t294))
% 0.48/0.91  (define @t306 () (@var "G" (-> tptp.product_prod_nat_nat tptp.product_prod_nat_nat)))
% 0.48/0.91  (define @t307 () (_ @t99 @t170))
% 0.48/0.91  (define @t308 () (@var "G" (-> tptp.paraco1605129243lle_tv tptp.nat)))
% 0.48/0.91  (define @t309 () (= (_ @t308 @t187) @t179))
% 0.48/0.91  (define @t310 () (_ @t125 @t170))
% 0.48/0.91  (define @t311 () (@var "G" (-> tptp.nat tptp.nat)))
% 0.48/0.91  (define @t312 () (_ @t311 @t202))
% 0.48/0.91  (define @t313 () (= @t312 @t179))
% 0.48/0.91  (define @t314 () (@list @t170 @t311 @t44))
% 0.48/0.91  (define @t315 () (_ @t134 @t165))
% 0.48/0.91  (define @t316 () (@var "G" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t317 () (_ @t316 @t206))
% 0.48/0.91  (define @t318 () (= @t317 @t176))
% 0.48/0.91  (define @t319 () (@list @t165 @t316 @t130))
% 0.48/0.91  (define @t320 () (_ (_ tptp.member1531318361lle_tv @t87) @t298))
% 0.48/0.91  (define @t321 () (_ (_ tptp.member1531318361lle_tv @t88) @t298))
% 0.48/0.91  (define @t322 () (@list @t90 @t298 @t88 @t87))
% 0.48/0.91  (define @t323 () (_ (_ tptp.member737151281tv_nat @t102) @t290))
% 0.48/0.91  (define @t324 () (_ @t77 @t290))
% 0.48/0.91  (define @t325 () (@list @t104 @t290 @t76 @t102))
% 0.48/0.91  (define @t326 () (_ (_ tptp.member813679063lle_tv @t109) @t292))
% 0.48/0.91  (define @t327 () (_ @t79 @t292))
% 0.48/0.91  (define @t328 () (@list @t111 @t292 @t78 @t109))
% 0.48/0.91  (define @t329 () (_ (_ tptp.member701585322at_nat @t116) @t294))
% 0.48/0.91  (define @t330 () (_ @t81 @t294))
% 0.48/0.91  (define @t331 () (@list @t118 @t294 @t80 @t116))
% 0.48/0.91  (define @t332 () (_ tptp.member_nat @t95))
% 0.48/0.91  (define @t333 () (_ @t332 @t170))
% 0.48/0.91  (define @t334 () (_ @t83 @t170))
% 0.48/0.91  (define @t335 () (not @t96))
% 0.48/0.91  (define @t336 () (@list @t97 @t170 @t82 @t95))
% 0.48/0.91  (define @t337 () (@list @t44 @t170 @t82 @t95))
% 0.48/0.91  (define @t338 () (_ tptp.member266900804lle_tv @t128))
% 0.48/0.91  (define @t339 () (_ @t338 @t165))
% 0.48/0.91  (define @t340 () (_ @t85 @t165))
% 0.48/0.91  (define @t341 () (@list @t130 @t165 @t84 @t128))
% 0.48/0.91  (define @t342 () (@var "A3" tptp.produc1647334210lle_tv))
% 0.48/0.91  (define @t343 () (@var "A3" tptp.produc194167194tv_nat))
% 0.48/0.91  (define @t344 () (@var "A3" tptp.produc270694976lle_tv))
% 0.48/0.91  (define @t345 () (@var "A3" tptp.product_prod_nat_nat))
% 0.48/0.91  (define @t346 () (@var "G" (-> tptp.nat tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t347 () (@var "A3" tptp.nat))
% 0.48/0.91  (define @t348 () (_ (_ tptp.member_nat @t347) @t170))
% 0.48/0.91  (define @t349 () (@list @t347))
% 0.48/0.91  (define @t350 () (_ tptp.inj_on_nat_nat @t311))
% 0.48/0.91  (define @t351 () (_ @t350 @t170))
% 0.48/0.91  (define @t352 () (_ tptp.inj_on772319074lle_tv @t316))
% 0.48/0.91  (define @t353 () (_ @t352 @t165))
% 0.48/0.91  (define @t354 () (@var "A3" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t355 () (@var "A0" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t356 () (_ @t236 @t254))
% 0.48/0.91  (define @t357 () (_ @t236 @t255))
% 0.48/0.91  (define @t358 () (@var "I3" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t359 () (_ tptp.produc1710735575lle_fm @t358))
% 0.48/0.91  (define @t360 () (@list @t358 @t255 @t254))
% 0.48/0.91  (define @t361 () (@var "N" tptp.nat))
% 0.48/0.91  (define @t362 () (@var "X" (-> tptp.nat tptp.nat)))
% 0.48/0.91  (define @t363 () (= @t128 (_ tptp.paraco793048302_Indet (_ @t362 @t361))))
% 0.48/0.91  (define @t364 () (_ tptp.paraco793048302_Indet @t361))
% 0.48/0.91  (define @t365 () (@var "Xa" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t366 () (= @t365 @t364))
% 0.48/0.91  (define @t367 () (@list @t361))
% 0.48/0.91  (define @t368 () (@var "B2" Bool))
% 0.48/0.91  (define @t369 () (_ tptp.paraco1344940915le_Det @t368))
% 0.48/0.91  (define @t370 () (= @t128 @t369))
% 0.48/0.91  (define @t371 () (= @t365 @t369))
% 0.48/0.91  (define @t372 () (@list @t368))
% 0.48/0.91  (define @t373 () (= (_ (_ tptp.paraco1147068288nge_tv @t362) @t365) @t128))
% 0.48/0.91  (define @t374 () (@list @t362 @t365 @t128))
% 0.48/0.91  (define @t375 () (@var "U" tptp.set_nat))
% 0.48/0.91  (define @t376 () (_ tptp.paraco55203475lid_in @t375))
% 0.48/0.91  (define @t377 () (_ @t376 @t21))
% 0.48/0.91  (define @t378 () (@var "Y22" tptp.nat))
% 0.48/0.91  (define @t379 () (@var "X23" tptp.nat))
% 0.48/0.91  (define @t380 () (_ tptp.paraco793048302_Indet @t379))
% 0.48/0.91  (define @t381 () (@var "A0" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t382 () (@var "A1" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t383 () (@var "A0" (-> tptp.nat tptp.nat)))
% 0.48/0.91  (define @t384 () (@var "P3" (-> (-> tptp.nat tptp.nat) tptp.paraco1605129243lle_tv Bool)))
% 0.48/0.91  (define @t385 () (@var "F4" (-> tptp.nat tptp.nat)))
% 0.48/0.91  (define @t386 () (_ @t384 @t385))
% 0.48/0.91  (define @t387 () (@list @t385 @t361))
% 0.48/0.91  (define @t388 () (@list @t385 @t368))
% 0.48/0.91  (define @t389 () (@var "X22" tptp.nat))
% 0.48/0.91  (define @t390 () (@var "X12" Bool))
% 0.48/0.91  (define @t391 () (@var "Tv" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t392 () (@var "X4" Bool))
% 0.48/0.91  (define @t393 () (_ (_ tptp.the_inv_into_nat_nat @t170) @t44))
% 0.48/0.91  (define @t394 () (_ (_ tptp.the_in452116896lle_tv @t165) @t130))
% 0.48/0.91  (define @t395 () (_ @t393 @t95))
% 0.48/0.91  (define @t396 () (_ @t394 @t128))
% 0.48/0.91  (define @t397 () (@var "N2" tptp.nat))
% 0.48/0.91  (define @t398 () (@var "Y22" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t399 () (@var "X23" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t400 () (@var "Y1" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t401 () (@var "X1" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t402 () (_ (_ tptp.produc1710735575lle_fm @t401) @t399))
% 0.48/0.91  (define @t403 () (@var "Y22" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t404 () (@var "X23" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t405 () (@var "Y1" (-> tptp.nat tptp.nat)))
% 0.48/0.91  (define @t406 () (@var "X1" (-> tptp.nat tptp.nat)))
% 0.48/0.91  (define @t407 () (_ (_ tptp.produc1680557635lle_tv @t406) @t404))
% 0.48/0.91  (define @t408 () (@var "B3" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t409 () (@var "B" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t410 () (= @t409 @t408))
% 0.48/0.91  (define @t411 () (@var "A5" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t412 () (@var "A" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t413 () (= @t412 @t411))
% 0.48/0.91  (define @t414 () (_ (_ tptp.produc1710735575lle_fm @t411) @t408))
% 0.48/0.91  (define @t415 () (_ tptp.produc1710735575lle_fm @t412))
% 0.48/0.91  (define @t416 () (_ @t415 @t409))
% 0.48/0.91  (define @t417 () (= @t416 @t414))
% 0.48/0.91  (define @t418 () (@list @t412 @t409 @t411 @t408))
% 0.48/0.91  (define @t419 () (@var "B3" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t420 () (@var "B" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t421 () (= @t420 @t419))
% 0.48/0.91  (define @t422 () (@var "A5" (-> tptp.nat tptp.nat)))
% 0.48/0.91  (define @t423 () (@var "A" (-> tptp.nat tptp.nat)))
% 0.48/0.91  (define @t424 () (= @t423 @t422))
% 0.48/0.91  (define @t425 () (_ (_ tptp.produc1680557635lle_tv @t422) @t419))
% 0.48/0.91  (define @t426 () (_ tptp.produc1680557635lle_tv @t423))
% 0.48/0.91  (define @t427 () (_ @t426 @t420))
% 0.48/0.91  (define @t428 () (= @t427 @t425))
% 0.48/0.91  (define @t429 () (@list @t423 @t420 @t422 @t419))
% 0.48/0.91  (define @t430 () (@var "Y2" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t431 () (@var "X4" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t432 () (_ (_ tptp.produc1710735575lle_fm @t431) @t430))
% 0.48/0.91  (define @t433 () (@var "P2" tptp.produc696645085lle_fm))
% 0.48/0.91  (define @t434 () (@list @t431 @t430))
% 0.48/0.91  (define @t435 () (@var "X4" (-> tptp.nat tptp.nat)))
% 0.48/0.91  (define @t436 () (_ (_ tptp.produc1680557635lle_tv @t435) @t205))
% 0.48/0.91  (define @t437 () (@var "P2" tptp.produc931990033lle_tv))
% 0.48/0.91  (define @t438 () (@list @t435 @t205))
% 0.48/0.91  (define @t439 () (@var "F2" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t440 () (_ @t146 @t439))
% 0.48/0.91  (define @t441 () (@var "Bool" Bool))
% 0.48/0.91  (define @t442 () (not @t441))
% 0.48/0.91  (define @t443 () (@var "F1" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t444 () (_ @t146 @t443))
% 0.48/0.91  (define @t445 () (_ (_ tptp.produc234482697lle_tv @t443) @t439))
% 0.48/0.91  (define @t446 () (_ @t445 @t441))
% 0.48/0.91  (define @t447 () (_ @t146 @t446))
% 0.48/0.91  (define @t448 () (@list @t146 @t443 @t439 @t441))
% 0.48/0.91  (define @t449 () (@var "H" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t450 () (@list @t443 @t439))
% 0.48/0.91  (define @t451 () (_ tptp.produc1680557635lle_tv @t385))
% 0.48/0.91  (define @t452 () (@var "Prod" tptp.produc696645085lle_fm))
% 0.48/0.91  (define @t453 () (@var "B2" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t454 () (@var "A3" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t455 () (_ (_ tptp.produc1710735575lle_fm @t454) @t453))
% 0.48/0.91  (define @t456 () (@list @t454 @t453))
% 0.48/0.91  (define @t457 () (forall @t456 (_ @t138 @t455)))
% 0.48/0.91  (define @t458 () (@var "Prod" tptp.produc931990033lle_tv))
% 0.48/0.91  (define @t459 () (@var "B2" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t460 () (@var "A3" (-> tptp.nat tptp.nat)))
% 0.48/0.91  (define @t461 () (_ (_ tptp.produc1680557635lle_tv @t460) @t459))
% 0.48/0.91  (define @t462 () (@list @t460 @t459))
% 0.48/0.91  (define @t463 () (forall @t462 (_ @t142 @t461)))
% 0.48/0.91  (define @t464 () (@var "Y" tptp.produc696645085lle_fm))
% 0.48/0.91  (define @t465 () (@var "Y" tptp.produc931990033lle_tv))
% 0.48/0.91  (define @t466 () (@var "R2" tptp.set_Pr2120184979lle_fm))
% 0.48/0.91  (define @t467 () (@var "S4" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t468 () (@var "R" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t469 () (_ tptp.produc1710735575lle_fm @t468))
% 0.48/0.91  (define @t470 () (@var "S3" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t471 () (@var "R2" tptp.set_Pr560526279lle_tv))
% 0.48/0.91  (define @t472 () (@var "S4" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t473 () (@var "R" (-> tptp.nat tptp.nat)))
% 0.48/0.91  (define @t474 () (_ tptp.produc1680557635lle_tv @t473))
% 0.48/0.91  (define @t475 () (@var "S3" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t476 () (@var "X" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t477 () (@var "F3" (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.list_char tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t478 () (_ tptp.produc1710735575lle_fm @t476))
% 0.48/0.91  (define @t479 () (_ @t478 @t247))
% 0.48/0.91  (define @t480 () (@var "F3" (-> (-> tptp.nat tptp.nat) tptp.nat tptp.nat)))
% 0.48/0.91  (define @t481 () (_ tptp.produc1680557635lle_tv @t362))
% 0.48/0.91  (define @t482 () (_ @t481 @t128))
% 0.48/0.91  (define @t483 () (@var "F3" (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm)))
% 0.48/0.91  (define @t484 () (_ tptp.accp_P2085826120lle_tv tptp.paraco1632582009tv_rel))
% 0.48/0.91  (define @t485 () (@var "F2" (-> tptp.nat tptp.nat)))
% 0.48/0.91  (define @t486 () (@var "F1" (-> tptp.nat tptp.nat)))
% 0.48/0.91  (define @t487 () (_ (_ tptp.inj_on_nat_nat @t485) tptp.top_top_set_nat))
% 0.48/0.91  (define @t488 () (_ (_ tptp.inj_on_nat_nat @t486) tptp.top_top_set_nat))
% 0.48/0.91  (define @t489 () (@var "F2" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t490 () (_ (_ tptp.inj_on772319074lle_tv @t489) tptp.top_to1057771083lle_tv))
% 0.48/0.91  (define @t491 () (@var "F1" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t492 () (_ (_ tptp.inj_on772319074lle_tv @t491) tptp.top_to1057771083lle_tv))
% 0.48/0.91  (define @t493 () (@var "F3" (-> tptp.produc696645085lle_fm Bool)))
% 0.48/0.91  (define @t494 () (_ (_ (_ tptp.produc275353523e_fm_o @t493) @t412) @t409))
% 0.48/0.91  (define @t495 () (_ @t493 @t416))
% 0.48/0.91  (define @t496 () (@list @t493 @t412 @t409))
% 0.48/0.91  (define @t497 () (@var "F3" (-> tptp.produc931990033lle_tv Bool)))
% 0.48/0.91  (define @t498 () (_ (_ (_ tptp.produc752649287e_tv_o @t497) @t423) @t420))
% 0.48/0.91  (define @t499 () (_ @t497 @t427))
% 0.48/0.91  (define @t500 () (@list @t497 @t423 @t420))
% 0.48/0.91  (define @t501 () (@var "G" (-> tptp.paraco1604210848lle_fm tptp.paraco1604210848lle_fm)))
% 0.48/0.91  (define @t502 () (_ (_ tptp.produc1710735575lle_fm (_ @t477 @t412)) (_ @t501 @t409)))
% 0.48/0.91  (define @t503 () (_ (_ tptp.produc1900967599lle_fm @t477) @t501))
% 0.48/0.91  (define @t504 () (@var "G" (-> tptp.paraco1604210848lle_fm tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t505 () (@var "F3" (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.nat tptp.nat)))
% 0.48/0.91  (define @t506 () (_ (_ tptp.produc1680557635lle_tv (_ @t505 @t412)) (_ @t504 @t409)))
% 0.48/0.91  (define @t507 () (_ (_ tptp.produc1566550641lle_tv @t505) @t504))
% 0.48/0.91  (define @t508 () (@var "G" (-> tptp.paraco1605129243lle_tv tptp.paraco1604210848lle_fm)))
% 0.48/0.91  (define @t509 () (@var "F3" (-> (-> tptp.nat tptp.nat) tptp.list_char tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t510 () (_ (_ tptp.produc1710735575lle_fm (_ @t509 @t423)) (_ @t508 @t420)))
% 0.48/0.91  (define @t511 () (_ (_ tptp.produc951033137lle_fm @t509) @t508))
% 0.48/0.91  (define @t512 () (_ (_ tptp.produc1680557635lle_tv (_ @t480 @t423)) (_ @t316 @t420)))
% 0.48/0.91  (define @t513 () (_ (_ tptp.produc532909085lle_tv @t480) @t316))
% 0.48/0.91  (define @t514 () (_ tptp.image_nat_nat @t44))
% 0.48/0.91  (define @t515 () (_ @t514 @t170))
% 0.48/0.91  (define @t516 () (@list @t44 @t170))
% 0.48/0.91  (define @t517 () (_ tptp.image_335818702lle_tv @t130))
% 0.48/0.91  (define @t518 () (_ @t517 @t165))
% 0.48/0.91  (define @t519 () (@list @t130 @t165))
% 0.48/0.91  (define @t520 () (_ (_ tptp.image_807538418lle_fm @t503) @t466))
% 0.48/0.91  (define @t521 () (_ (_ tptp.member1474794996lle_fm @t416) @t466))
% 0.48/0.91  (define @t522 () (_ (_ tptp.image_1154804148lle_tv @t507) @t466))
% 0.48/0.91  (define @t523 () (_ (_ tptp.image_1585092542lle_fm @t511) @t471))
% 0.48/0.91  (define @t524 () (_ (_ tptp.member1569366824lle_tv @t427) @t471))
% 0.48/0.91  (define @t525 () (_ (_ tptp.image_1751508608lle_tv @t513) @t471))
% 0.48/0.91  (define @t526 () (@var "Y" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t527 () (_ tptp.produc1710735575lle_fm @t526))
% 0.48/0.91  (define @t528 () (_ @t527 @t257))
% 0.48/0.91  (define @t529 () (_ (_ tptp.produc1943344577lle_tv @t257) @t526))
% 0.48/0.91  (define @t530 () (@var "Y" (-> tptp.nat tptp.nat)))
% 0.48/0.91  (define @t531 () (_ tptp.produc1680557635lle_tv @t530))
% 0.48/0.91  (define @t532 () (_ @t531 @t84))
% 0.48/0.91  (define @t533 () (_ (_ tptp.produc1633679363at_nat @t84) @t530))
% 0.48/0.91  (define @t534 () (_ (_ tptp.produc1943344577lle_tv @t247) @t476))
% 0.48/0.91  (define @t535 () (_ (_ tptp.produc1633679363at_nat @t128) @t362))
% 0.48/0.91  (define @t536 () (@var "A2" tptp.set_Pr1723822845lle_tv))
% 0.48/0.91  (define @t537 () (@var "A2" tptp.set_Pr840833727at_nat))
% 0.48/0.91  (define @t538 () (_ tptp.produc505105722at_nat @t44))
% 0.48/0.91  (define @t539 () (= (_ (_ tptp.image_nat_nat @t311) tptp.top_top_set_nat) tptp.top_top_set_nat))
% 0.48/0.91  (define @t540 () (_ @t514 tptp.top_top_set_nat))
% 0.48/0.91  (define @t541 () (= @t540 tptp.top_top_set_nat))
% 0.48/0.91  (define @t542 () (= (_ (_ tptp.image_1151963140lle_tv @t346) tptp.top_top_set_nat) tptp.top_to1057771083lle_tv))
% 0.48/0.91  (define @t543 () (= (_ (_ tptp.image_376325286tv_nat @t308) tptp.top_to1057771083lle_tv) tptp.top_top_set_nat))
% 0.48/0.91  (define @t544 () (= (_ (_ tptp.image_335818702lle_tv @t316) tptp.top_to1057771083lle_tv) tptp.top_to1057771083lle_tv))
% 0.48/0.91  (define @t545 () (= (_ (_ tptp.image_1151963140lle_tv @t97) tptp.top_top_set_nat) tptp.top_to1057771083lle_tv))
% 0.48/0.91  (define @t546 () (@var "F3" (-> tptp.paraco1605129243lle_tv tptp.nat)))
% 0.48/0.91  (define @t547 () (= (_ (_ tptp.image_376325286tv_nat @t546) tptp.top_to1057771083lle_tv) tptp.top_top_set_nat))
% 0.48/0.91  (define @t548 () (@var "Xa2" tptp.nat))
% 0.48/0.91  (define @t549 () (@var "Xa2" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t550 () (= @t95 @t202))
% 0.48/0.91  (define @t551 () (@list @t44 @t95))
% 0.48/0.91  (define @t552 () (= @t128 @t187))
% 0.48/0.91  (define @t553 () (@list @t97 @t128))
% 0.48/0.91  (define @t554 () (_ @t546 @t176))
% 0.48/0.91  (define @t555 () (= @t95 @t554))
% 0.48/0.91  (define @t556 () (@list @t546 @t95))
% 0.48/0.91  (define @t557 () (= @t128 @t206))
% 0.48/0.91  (define @t558 () (_ @t517 tptp.top_to1057771083lle_tv))
% 0.48/0.91  (define @t559 () (= @t558 tptp.top_to1057771083lle_tv))
% 0.48/0.91  (define @t560 () (@list @t130 @t128))
% 0.48/0.91  (define @t561 () (@list @t219))
% 0.48/0.91  (define @t562 () (@list @t231))
% 0.48/0.91  (define @t563 () (@var "B" tptp.nat))
% 0.48/0.91  (define @t564 () (@var "B4" tptp.set_nat))
% 0.48/0.91  (define @t565 () (= (= @t515 (_ @t514 @t564)) (= @t170 @t564)))
% 0.48/0.91  (define @t566 () (@list @t44 @t170 @t564))
% 0.48/0.91  (define @t567 () (@var "B4" tptp.set_Pa1764573435lle_tv))
% 0.48/0.91  (define @t568 () (= (= @t518 (_ @t517 @t567)) (= @t165 @t567)))
% 0.48/0.91  (define @t569 () (@list @t130 @t165 @t567))
% 0.48/0.91  (define @t570 () (= (_ (_ tptp.member_nat (_ @t44 @t149)) @t515) (_ @t152 @t170)))
% 0.48/0.91  (define @t571 () (= (_ (_ tptp.member266900804lle_tv (_ @t130 @t145)) @t518) (_ @t148 @t165)))
% 0.48/0.91  (define @t572 () (not (_ (_ tptp.member1474794996lle_fm @t432) @t466)))
% 0.48/0.91  (define @t573 () (@var "C" tptp.produc696645085lle_fm))
% 0.48/0.91  (define @t574 () (_ tptp.member1474794996lle_fm @t573))
% 0.48/0.91  (define @t575 () (not (_ (_ tptp.member1569366824lle_tv @t436) @t471)))
% 0.48/0.91  (define @t576 () (@var "C" tptp.produc931990033lle_tv))
% 0.48/0.91  (define @t577 () (_ tptp.member1569366824lle_tv @t576))
% 0.48/0.91  (define @t578 () (@var "R" tptp.set_Pr1986765409at_nat))
% 0.48/0.91  (define @t579 () (_ tptp.total_on_nat tptp.top_top_set_nat))
% 0.48/0.91  (define @t580 () (_ @t579 @t578))
% 0.48/0.91  (define @t581 () (@var "R" tptp.set_Pr2014382200lle_tv))
% 0.48/0.91  (define @t582 () (_ tptp.total_1781621663lle_tv tptp.top_to1057771083lle_tv))
% 0.48/0.91  (define @t583 () (_ @t582 @t581))
% 0.48/0.91  (define @t584 () (_ (_ tptp.produc1710735575lle_fm (_ tptp.produc29804011lle_fm @t452)) (_ tptp.produc148705065lle_fm @t452)))
% 0.48/0.91  (define @t585 () (@list @t452))
% 0.48/0.91  (define @t586 () (_ (_ tptp.produc1680557635lle_tv (_ tptp.produc1636169559lle_tv @t458)) (_ tptp.produc547496597lle_tv @t458)))
% 0.48/0.91  (define @t587 () (@list @t458))
% 0.48/0.91  (define @t588 () (_ tptp.produc29804011lle_fm @t479))
% 0.48/0.91  (define @t589 () (_ tptp.produc1636169559lle_tv @t482))
% 0.48/0.91  (define @t590 () (@var "A" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t591 () (_ tptp.produc148705065lle_fm @t479))
% 0.48/0.91  (define @t592 () (_ tptp.produc547496597lle_tv @t482))
% 0.48/0.91  (define @t593 () (@list @t401 @t399))
% 0.48/0.91  (define @t594 () (@list @t406 @t404))
% 0.48/0.91  (define @t595 () (@var "T" tptp.produc696645085lle_fm))
% 0.48/0.91  (define @t596 () (@var "T" tptp.produc931990033lle_tv))
% 0.48/0.91  (define @t597 () (@var "P3" (-> tptp.paraco1604210848lle_fm (-> tptp.list_char tptp.paraco1605129243lle_tv) Bool)))
% 0.48/0.91  (define @t598 () (@var "P3" (-> tptp.paraco1605129243lle_tv (-> tptp.nat tptp.nat) Bool)))
% 0.48/0.91  (define @t599 () (@var "P2" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t600 () (_ (_ tptp.produc1710735575lle_fm @t599) @t20))
% 0.48/0.91  (define @t601 () (@var "Q2" (-> tptp.paraco1604210848lle_fm Bool)))
% 0.48/0.91  (define @t602 () (@var "P3" (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) Bool)))
% 0.48/0.91  (define @t603 () (@var "Q" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t604 () (@var "P2" (-> tptp.nat tptp.nat)))
% 0.48/0.91  (define @t605 () (_ (_ tptp.produc1680557635lle_tv @t604) @t603))
% 0.48/0.91  (define @t606 () (@var "P3" (-> (-> tptp.nat tptp.nat) Bool)))
% 0.48/0.91  (define @t607 () (@var "P3" (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.paraco1604210848lle_fm Bool)))
% 0.48/0.91  (define @t608 () (@var "A6" (-> tptp.list_char tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t609 () (@var "A6" (-> tptp.nat tptp.nat)))
% 0.48/0.91  (define @t610 () (@var "Z" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t611 () (= @t70 (_ @t527 @t610)))
% 0.48/0.91  (define @t612 () (@list @t70 @t526 @t610))
% 0.48/0.91  (define @t613 () (@var "Z" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t614 () (= @t73 (_ @t531 @t613)))
% 0.48/0.91  (define @t615 () (@list @t73 @t530 @t613))
% 0.48/0.91  (define @t616 () (@var "B5" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t617 () (@var "B5" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t618 () (@var "S3" tptp.set_Pr1986765409at_nat))
% 0.48/0.91  (define @t619 () (_ @t579 @t618))
% 0.48/0.91  (define @t620 () (@var "S3" tptp.set_Pr2014382200lle_tv))
% 0.48/0.91  (define @t621 () (_ @t582 @t620))
% 0.48/0.91  (define @t622 () (@var "S3" tptp.set_Pr1019238018lle_fm))
% 0.48/0.91  (define @t623 () (@var "R" tptp.set_Pr2061825550lle_tv))
% 0.48/0.91  (define @t624 () (@var "R" tptp.set_Pr1357842111at_nat))
% 0.48/0.91  (define @t625 () (@var "R2" (-> (-> tptp.list_char tptp.paraco1605129243lle_tv) tptp.set_Pr1019238018lle_fm)))
% 0.48/0.91  (define @t626 () (@var "Y5" tptp.paraco1604210848lle_fm))
% 0.48/0.91  (define @t627 () (@var "R2" (-> (-> tptp.nat tptp.nat) tptp.set_Pr2014382200lle_tv)))
% 0.48/0.91  (define @t628 () (@var "Y5" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t629 () (_ tptp.ord_less_eq_set_nat @t170))
% 0.48/0.91  (define @t630 () (_ @t629 @t564))
% 0.48/0.91  (define @t631 () (_ tptp.ord_le241064091lle_tv @t165))
% 0.48/0.91  (define @t632 () (_ @t631 @t567))
% 0.48/0.91  (define @t633 () (@var "C2" tptp.set_nat))
% 0.48/0.91  (define @t634 () (_ tptp.ord_less_eq_set_nat @t564))
% 0.48/0.91  (define @t635 () (@var "C2" tptp.set_Pa1764573435lle_tv))
% 0.48/0.91  (define @t636 () (_ tptp.ord_le241064091lle_tv @t567))
% 0.48/0.91  (define @t637 () (_ @t125 @t564))
% 0.48/0.91  (define @t638 () (_ @t134 @t567))
% 0.48/0.91  (define @t639 () (@var "A" tptp.set_nat))
% 0.48/0.91  (define @t640 () (= @t639 tptp.top_top_set_nat))
% 0.48/0.91  (define @t641 () (_ (_ tptp.ord_less_eq_set_nat tptp.top_top_set_nat) @t639))
% 0.48/0.91  (define @t642 () (@list @t639))
% 0.48/0.91  (define @t643 () (@var "A" tptp.set_Pa1764573435lle_tv))
% 0.48/0.91  (define @t644 () (= @t643 tptp.top_to1057771083lle_tv))
% 0.48/0.91  (define @t645 () (_ (_ tptp.ord_le241064091lle_tv tptp.top_to1057771083lle_tv) @t643))
% 0.48/0.91  (define @t646 () (@list @t643))
% 0.48/0.91  (define @t647 () (@var "P3" Bool))
% 0.48/0.91  (define @t648 () (@list @t84 @t128))
% 0.48/0.91  (define @t649 () (= @t11 @t1))
% 0.48/0.91  (define @t650 () (not @t649))
% 0.48/0.91  (define @t651 () (not @t650))
% 0.48/0.91  (define @t652 () (lambda (@list @t67) (forall (@list @t68) (= (_ @t69 @t67) @t1))))
% 0.48/0.91  (define @t653 () (@var "S" tptp.list_char))
% 0.48/0.91  (define @t654 () (_ @t68 @t653))
% 0.48/0.91  (define @t655 () (@var "F" (-> tptp.nat tptp.nat)))
% 0.48/0.91  (define @t656 () (lambda (@list @t655 @t68 @t653) (_ (_ tptp.paraco1147068288nge_tv @t655) @t654)))
% 0.48/0.91  (define @t657 () (lambda @t168 tptp.top_top_o))
% 0.48/0.91  (define @t658 () (lambda @t173 tptp.top_top_o))
% 0.48/0.91  (define @t659 () (@var "A4" tptp.set_nat))
% 0.48/0.91  (define @t660 () (lambda (@list @t655 @t659) (forall @t173 (=> (_ @t172 @t659) (forall @t561 (=> (_ (_ tptp.member_nat @t219) @t659) (=> (= (_ @t655 @t171) (_ @t655 @t219)) @t220)))))))
% 0.48/0.91  (define @t661 () (@var "F" (-> tptp.paraco1605129243lle_tv tptp.paraco1605129243lle_tv)))
% 0.48/0.91  (define @t662 () (@var "A4" tptp.set_Pa1764573435lle_tv))
% 0.48/0.91  (define @t663 () (lambda (@list @t661 @t662) (forall @t168 (=> (_ @t167 @t662) (forall @t562 (=> (_ (_ tptp.member266900804lle_tv @t231) @t662) (=> (= (_ @t661 @t166) (_ @t661 @t231)) @t232)))))))
% 0.48/0.91  (define @t664 () (@var "F22" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t665 () (@var "F12" tptp.paraco1605129243lle_tv))
% 0.48/0.91  (define @t666 () (@var "Bool2" Bool))
% 0.48/0.91  (define @t667 () (lambda (@list @t665 @t664 @t666) (_ (_ (_ tptp.if_Par1134130401lle_tv @t666) @t665) @t664)))
% 0.48/0.91  (define @t668 () (@var "P" tptp.produc1443694919lle_tv))
% 0.48/0.91  (define @t669 () (lambda (@list @t668) (_ (_ tptp.produc1710735575lle_fm (_ tptp.produc381314067lle_tv @t668)) (_ tptp.produc262413013lle_tv @t668))))
% 0.48/0.91  (define @t670 () (@var "P" tptp.produc596913417at_nat))
% 0.48/0.91  (define @t671 () (lambda (@list @t670) (_ (_ tptp.produc1680557635lle_tv (_ tptp.produc500618325at_nat @t670)) (_ tptp.produc1589291287at_nat @t670))))
% 0.48/0.91  (define @t672 () (tptp.paraco1325918602e_eval tptp.i tptp.p2))
% 0.48/0.91  (define @t673 () (@purify true))
% 0.48/0.91  (define @t674 () (tptp.paraco1344940915le_Det @t673))
% 0.48/0.91  (define @t675 () (_ tptp.paraco1344940915le_Det @t673))
% 0.48/0.91  (define @t676 () (@purify false))
% 0.48/0.91  (define @t677 () (tptp.paraco1344940915le_Det @t676))
% 0.48/0.91  (define @t678 () (_ tptp.paraco1344940915le_Det @t676))
% 0.48/0.91  (define @t679 () (lambda (@list @t653) (_ @t16 (_ tptp.i @t653))))
% 0.48/0.91  (define @t680 () (@purify @t679))
% 0.48/0.91  (define @t681 () (tptp.paraco1325918602e_eval @t680 tptp.p2))
% 0.48/0.91  (define @t682 () (_ (_ tptp.paraco1325918602e_eval @t680) tptp.p2))
% 0.48/0.91  (define @t683 () (_ (_ tptp.paraco1325918602e_eval @t679) tptp.p2))
% 0.48/0.91  (define @t684 () (lambda (@list @t68 @t653) (_ @t16 @t654)))
% 0.48/0.91  (define @t685 () (_ @t656 tptp.f))
% 0.48/0.91  (define @t686 () (_ (_ tptp.paraco1325918602e_eval (_ @t685 tptp.i)) tptp.p2))
% 0.48/0.91  (define @t687 () (= @t686 @t1))
% 0.48/0.91  (define @t688 () (= @t674 @t681))
% 0.48/0.91  (define @t689 () (not @t688))
% 0.48/0.91  (define @t690 () (= @t677 @t681))
% 0.48/0.91  (define @t691 () (not @t690))
% 0.48/0.91  (define @t692 () (= @t672 @t677))
% 0.48/0.91  (define @t693 () (not @t692))
% 0.48/0.91  (define @t694 () (= @t674 @t672))
% 0.48/0.91  (define @t695 () (not @t694))
% 0.48/0.91  (define @t696 () (and @t695 @t692 @t690))
% 0.48/0.91  (assume @p1 @t5)
% 0.48/0.91  (assume @p2 (not (= @t6 @t1)))
% 0.48/0.91  (assume @p3 (not (= @t6 @t7)))
% 0.48/0.91  (assume @p4 (not (= @t9 @t1)))
% 0.48/0.91  (assume @p5 @t10)
% 0.48/0.91  (assume @p6 (not (= @t6 @t3)))
% 0.48/0.91  (assume @p7 @t12)
% 0.48/0.91  (assume @p8 (not (= @t9 @t11)))
% 0.48/0.91  (assume @p9 (forall (@list @t14 @t13) (= (= @t15 (_ tptp.paraco1344940915le_Det @t13)) (= @t14 @t13))))
% 0.48/0.91  (assume @p10 (= @t11 @t17))
% 0.48/0.91  (assume @p11 (= @t9 (_ @t16 @t6)))
% 0.48/0.91  (assume @p12 (= @t17 @t7))
% 0.48/0.91  (assume @p13 (= (_ @t2 (_ (_ tptp.paraco1745535428le_Eql tptp.p1) tptp.p2)) (_ @t2 (_ tptp.paraco445776468le_Neg tptp.p1))))
% 0.48/0.91  (assume @p14 (forall (@list @t18) (= (_ @t19 tptp.paraco367965286_Truth) @t1)))
% 0.48/0.91  (assume @p15 (forall @t27 (and (=> @t25 (= @t22 @t1)) (=> @t26 (= @t22 @t7)))))
% 0.48/0.91  (assume @p16 (forall @t27 (= @t22 (_ tptp.paraco1344940915le_Det @t25))))
% 0.48/0.91  (assume @p17 (forall @t27 (and (=> @t25 @t32) (=> @t26 (and (=> @t33 (= @t29 @t23)) (=> @t34 (and (=> @t30 @t32) (=> @t31 (= @t29 @t7)))))))))
% 0.48/0.91  (assume @p18 (forall (@list @t35 @t36 @t14) (= (_ @t37 @t15) (_ @t35 @t14))))
% 0.48/0.91  (assume @p19 (forall @t41 (and (=> @t39 (= @t38 @t1)) (=> @t40 (and (=> @t33 (= @t38 @t7)) (=> @t34 (= @t38 @t24)))))))
% 0.48/0.91  (assume @p20 (_ (_ tptp.inj_on_nat_nat tptp.f) tptp.top_top_set_nat))
% 0.48/0.91  (assume @p21 (forall (@list @t44 @t42) (= (_ @t45 @t43) @t43)))
% 0.48/0.91  (assume @p22 (forall (@list @t47 @t46) (= (= @t48 (_ tptp.paraco445776468le_Neg @t46)) (= @t47 @t46))))
% 0.48/0.91  (assume @p23 (forall (@list @t52 @t50 @t51 @t49) (= (= @t53 (_ (_ tptp.paraco69239110le_Con @t51) @t49)) (and (= @t52 @t51) (= @t50 @t49)))))
% 0.48/0.91  (assume @p24 (forall (@list @t57 @t55 @t56 @t54) (= (= @t58 (_ (_ tptp.paraco1745535428le_Eql @t56) @t54)) (and (= @t57 @t56) (= @t55 @t54)))))
% 0.48/0.91  (assume @p25 (forall (@list @t62 @t60 @t61 @t59) (= (= @t63 (_ (_ tptp.paraco1389086619le_Eql @t61) @t59)) (and (= @t62 @t61) (= @t60 @t59)))))
% 0.48/0.91  (assume @p26 (forall (@list @t62 @t60 @t57 @t55) (not (= @t63 @t58))))
% 0.48/0.91  (assume @p27 (forall (@list @t52 @t50 @t57 @t55) (not (= @t53 @t58))))
% 0.48/0.91  (assume @p28 (forall (@list @t52 @t50 @t62 @t60) (not (= @t53 @t63))))
% 0.48/0.91  (assume @p29 (forall (@list @t47 @t57 @t55) (not (= @t48 @t58))))
% 0.48/0.91  (assume @p30 (forall (@list @t47 @t62 @t60) (not (= @t48 @t63))))
% 0.48/0.91  (assume @p31 (forall (@list @t47 @t52 @t50) (not (= @t48 @t53))))
% 0.48/0.91  (assume @p32 (forall (@list @t57 @t55) (not (= tptp.paraco367965286_Truth @t58))))
% 0.48/0.91  (assume @p33 (forall (@list @t62 @t60) (not (= tptp.paraco367965286_Truth @t63))))
% 0.48/0.91  (assume @p34 (forall (@list @t52 @t50) (not (= tptp.paraco367965286_Truth @t53))))
% 0.48/0.91  (assume @p35 (forall (@list @t47) (not (= tptp.paraco367965286_Truth @t48))))
% 0.48/0.91  (assume @p36 (forall (@list @t21 @t20) (= (_ tptp.paraco327635598_valid @t28) (and @t64 (_ tptp.paraco327635598_valid @t20)))))
% 0.48/0.91  (assume @p37 (forall @t27 (and (=> @t25 (= @t65 @t1)) (=> @t26 (and (=> @t33 (= @t65 @t23)) (=> @t34 (and (=> @t30 (= @t65 @t24)) (=> @t31 (and (=> @t39 (= @t65 (_ @t19 (_ tptp.paraco445776468le_Neg @t20)))) (=> @t40 (and (=> @t66 (= @t65 @t38)) (=> (not @t66) (= @t65 @t7)))))))))))))
% 0.48/0.91  (assume @p38 (= tptp.paraco1325918602e_eval (lambda (@list @t68 @t67) (_ @t69 (_ tptp.paraco445776468le_Neg (_ tptp.paraco445776468le_Neg @t67))))))
% 0.48/0.91  (assume @p39 (forall @t71 (_ (_ tptp.member1474794996lle_fm @t70) tptp.top_to775056195lle_fm)))
% 0.48/0.91  (assume @p40 (forall (@list @t72) (_ (_ tptp.member146333935lle_tv @t72) tptp.top_to138697918lle_tv)))
% 0.48/0.91  (assume @p41 (forall @t74 (_ (_ tptp.member1569366824lle_tv @t73) tptp.top_to449985143lle_tv)))
% 0.48/0.91  (assume @p42 (forall (@list @t75) (_ (_ tptp.member112824072at_nat @t75) tptp.top_to1541413903at_nat)))
% 0.48/0.91  (assume @p43 (forall (@list @t76) (_ @t77 tptp.top_to975729152tv_nat)))
% 0.48/0.91  (assume @p44 (forall (@list @t78) (_ @t79 tptp.top_to1411004326lle_tv)))
% 0.48/0.91  (assume @p45 (forall (@list @t80) (_ @t81 tptp.top_to1555900337at_nat)))
% 0.48/0.91  (assume @p46 (forall (@list @t82) (_ @t83 tptp.top_top_set_nat)))
% 0.48/0.91  (assume @p47 (forall @t86 (_ @t85 tptp.top_to1057771083lle_tv)))
% 0.48/0.91  (assume @p48 (forall @t94 (=> @t93 (=> @t91 @t89))))
% 0.48/0.91  (assume @p49 (forall @t101 (=> @t100 (=> @t98 @t96))))
% 0.48/0.91  (assume @p50 (forall @t108 (=> @t107 (=> @t105 @t103))))
% 0.48/0.91  (assume @p51 (forall @t115 (=> @t114 (=> @t112 @t110))))
% 0.48/0.91  (assume @p52 (forall @t122 (=> @t121 (=> @t119 @t117))))
% 0.48/0.91  (assume @p53 (forall @t127 (=> @t126 (=> @t124 @t96))))
% 0.48/0.91  (assume @p54 (forall @t136 (=> @t135 (=> @t133 @t129))))
% 0.48/0.91  (assume @p55 (forall (@list @t137 @t138) (= (_ (_ tptp.member1474794996lle_fm @t137) (_ tptp.collec835549234lle_fm @t138)) (_ @t138 @t137))))
% 0.48/0.91  (assume @p56 (forall (@list @t139 @t140) (= (_ (_ tptp.member146333935lle_tv @t139) (_ tptp.collec1102043437lle_tv @t140)) (_ @t140 @t139))))
% 0.48/0.91  (assume @p57 (forall (@list @t141 @t142) (= (_ (_ tptp.member1569366824lle_tv @t141) (_ tptp.collec1624074086lle_tv @t142)) (_ @t142 @t141))))
% 0.48/0.91  (assume @p58 (forall (@list @t143 @t144) (= (_ (_ tptp.member112824072at_nat @t143) (_ tptp.collec791369802at_nat @t144)) (_ @t144 @t143))))
% 0.48/0.91  (assume @p59 (forall (@list @t145 @t146) (= (_ @t148 @t147) (_ @t146 @t145))))
% 0.48/0.91  (assume @p60 (forall (@list @t149 @t150) (= (_ @t152 @t151) (_ @t150 @t149))))
% 0.48/0.91  (assume @p61 (forall @t155 (= (_ tptp.collec835549234lle_fm (lambda (@list @t154) (_ (_ tptp.member1474794996lle_fm @t154) @t153))) @t153)))
% 0.48/0.91  (assume @p62 (forall @t158 (= (_ tptp.collec1102043437lle_tv (lambda (@list @t157) (_ (_ tptp.member146333935lle_tv @t157) @t156))) @t156)))
% 0.48/0.91  (assume @p63 (forall @t161 (= (_ tptp.collec1624074086lle_tv (lambda (@list @t160) (_ (_ tptp.member1569366824lle_tv @t160) @t159))) @t159)))
% 0.48/0.91  (assume @p64 (forall @t164 (= (_ tptp.collec791369802at_nat (lambda (@list @t163) (_ (_ tptp.member112824072at_nat @t163) @t162))) @t162)))
% 0.48/0.91  (assume @p65 (forall @t169 (= (_ tptp.collec1111687558lle_tv (lambda @t168 (_ @t167 @t165))) @t165)))
% 0.48/0.91  (assume @p66 (forall @t174 (= (_ tptp.collect_nat (lambda @t173 (_ @t172 @t170))) @t170)))
% 0.48/0.91  (assume @p67 (forall (@list @t146 @t175) (=> (forall @t177 (= (_ @t146 @t176) (_ @t175 @t176))) (= @t147 (_ tptp.collec1111687558lle_tv @t175)))))
% 0.48/0.91  (assume @p68 (forall (@list @t150 @t178) (=> (forall @t180 (= (_ @t150 @t179) (_ @t178 @t179))) (= @t151 (_ tptp.collect_nat @t178)))))
% 0.48/0.91  (assume @p69 (forall @t184 (=> (forall (@list @t182 @t181) (=> (= @t183 (_ @t90 @t181)) (= @t182 @t181))) @t93)))
% 0.48/0.91  (assume @p70 (forall @t189 (=> (forall @t188 (=> (= @t187 (_ @t97 @t185)) @t186)) @t100)))
% 0.48/0.91  (assume @p71 (forall @t193 (=> (forall (@list @t191 @t190) (=> (= @t192 (_ @t104 @t190)) (= @t191 @t190))) @t107)))
% 0.48/0.91  (assume @p72 (forall @t197 (=> (forall (@list @t195 @t194) (=> (= @t196 (_ @t111 @t194)) (= @t195 @t194))) @t114)))
% 0.48/0.91  (assume @p73 (forall @t201 (=> (forall (@list @t199 @t198) (=> (= @t200 (_ @t118 @t198)) (= @t199 @t198))) @t121)))
% 0.48/0.91  (assume @p74 (forall @t204 (=> (forall @t188 @t203) @t126)))
% 0.48/0.91  (assume @p75 (forall @t209 (=> (forall @t208 @t207) @t135)))
% 0.48/0.91  (assume @p76 (forall @t94 (=> @t93 @t210)))
% 0.48/0.91  (assume @p77 (forall @t101 (=> @t100 @t211)))
% 0.48/0.91  (assume @p78 (forall @t108 (=> @t107 @t212)))
% 0.48/0.91  (assume @p79 (forall @t115 (=> @t114 @t213)))
% 0.48/0.91  (assume @p80 (forall @t122 (=> @t121 @t214)))
% 0.48/0.91  (assume @p81 (forall @t127 (=> @t126 @t215)))
% 0.48/0.91  (assume @p82 (forall @t136 (=> @t135 @t216)))
% 0.48/0.91  (assume @p83 (forall @t184 (= @t93 (forall (@list @t218 @t217) (=> (= (_ @t90 @t218) (_ @t90 @t217)) (= @t218 @t217))))))
% 0.48/0.91  (assume @p84 (forall @t189 (= @t100 (forall @t222 (=> (= @t221 (_ @t97 @t219)) @t220)))))
% 0.48/0.91  (assume @p85 (forall @t193 (= @t107 (forall (@list @t224 @t223) (=> (= (_ @t104 @t224) (_ @t104 @t223)) (= @t224 @t223))))))
% 0.48/0.91  (assume @p86 (forall @t197 (= @t114 (forall (@list @t226 @t225) (=> (= (_ @t111 @t226) (_ @t111 @t225)) (= @t226 @t225))))))
% 0.48/0.91  (assume @p87 (forall @t201 (= @t121 (forall (@list @t228 @t227) (=> (= (_ @t118 @t228) (_ @t118 @t227)) (= @t228 @t227))))))
% 0.48/0.91  (assume @p88 (forall @t204 (= @t126 (forall @t222 (=> (= @t230 @t229) @t220)))))
% 0.48/0.91  (assume @p89 (forall @t209 (= @t135 (forall (@list @t166 @t231) (=> (= @t234 @t233) @t232)))))
% 0.48/0.91  (assume @p90 (forall (@list @t236 @t235) (=> (forall (@list @t244) (_ @t236 (_ tptp.paraco1480028776le_Pro @t244))) (=> @t243 (=> (forall (@list @t242) (=> (_ @t236 @t242) (_ @t236 (_ tptp.paraco445776468le_Neg @t242)))) (=> (forall @t241 (=> @t240 (=> @t239 (_ @t236 (_ (_ tptp.paraco69239110le_Con @t238) @t237))))) (=> (forall @t241 (=> @t240 (=> @t239 (_ @t236 (_ (_ tptp.paraco1389086619le_Eql @t238) @t237))))) (=> (forall @t241 (=> @t240 (=> @t239 (_ @t236 (_ (_ tptp.paraco1745535428le_Eql @t238) @t237))))) (_ @t236 @t235)))))))))
% 0.48/0.91  (assume @p91 (forall (@list @t247) (=> (forall (@list @t253) (not (= @t247 (_ tptp.paraco1480028776le_Pro @t253)))) (=> (not (= @t247 tptp.paraco367965286_Truth)) (=> (forall (@list @t252) (not (= @t247 (_ tptp.paraco445776468le_Neg @t252)))) (=> (forall (@list @t251 @t250) (not (= @t247 (_ (_ tptp.paraco69239110le_Con @t251) @t250)))) (=> (forall (@list @t249 @t248) (not (= @t247 (_ (_ tptp.paraco1389086619le_Eql @t249) @t248)))) (not (forall (@list @t246 @t245) (not (= @t247 (_ (_ tptp.paraco1745535428le_Eql @t246) @t245))))))))))))
% 0.48/0.91  (assume @p92 (forall (@list @t257) (=> (not (= @t257 tptp.paraco367965286_Truth)) (=> (forall @t265 (not (= @t257 @t264))) (=> (forall @t262 (not (= @t257 @t261))) (=> (forall @t258 (not (= @t257 @t260))) (=> (forall @t258 (not (= @t257 @t259))) (not (forall @t258 (not (= @t257 @t256)))))))))))
% 0.48/0.91  (assume @p93 (forall (@list @t267 @t266) (= (= @t268 (_ tptp.paraco1480028776le_Pro @t266)) (= @t267 @t266))))
% 0.48/0.91  (assume @p94 (= tptp.top_to975729152tv_nat (_ tptp.collec848462447tv_nat tptp.top_to900819589_nat_o)))
% 0.48/0.91  (assume @p95 (= tptp.top_to1411004326lle_tv (_ tptp.collec924990229lle_tv tptp.top_to1889334367e_tv_o)))
% 0.48/0.91  (assume @p96 (= tptp.top_to1555900337at_nat (_ tptp.collec7649004at_nat tptp.top_to632227436_nat_o)))
% 0.48/0.91  (assume @p97 (= tptp.top_top_set_nat (_ tptp.collect_nat tptp.top_top_nat_o)))
% 0.48/0.91  (assume @p98 (= tptp.top_to1057771083lle_tv (_ tptp.collec1111687558lle_tv tptp.top_to1299250770e_tv_o)))
% 0.48/0.91  (assume @p99 (forall (@list @t18 @t269) (= (_ @t19 (_ tptp.paraco1480028776le_Pro @t269)) (_ @t18 @t269))))
% 0.48/0.91  (assume @p100 (forall (@list @t267 @t47) (not (= @t268 @t48))))
% 0.48/0.91  (assume @p101 (forall (@list @t267 @t52 @t50) (not (= @t268 @t53))))
% 0.48/0.91  (assume @p102 (forall (@list @t267 @t57 @t55) (not (= @t268 @t58))))
% 0.48/0.91  (assume @p103 (forall (@list @t267 @t62 @t60) (not (= @t268 @t63))))
% 0.48/0.91  (assume @p104 (forall (@list @t267) (not (= @t268 tptp.paraco367965286_Truth))))
% 0.48/0.91  (assume @p105 (forall @t204 (=> @t126 (_ (_ tptp.inj_on772319074lle_tv @t45) tptp.top_to1057771083lle_tv))))
% 0.48/0.91  (assume @p106 (exists @t272 (_ @t271 tptp.top_to775056195lle_fm)))
% 0.48/0.91  (assume @p107 (exists @t275 (_ @t274 tptp.top_to138697918lle_tv)))
% 0.48/0.91  (assume @p108 (exists @t278 (_ @t277 tptp.top_to449985143lle_tv)))
% 0.48/0.91  (assume @p109 (exists @t281 (_ @t280 tptp.top_to1541413903at_nat)))
% 0.48/0.91  (assume @p110 (exists @t283 (_ @t282 tptp.top_to975729152tv_nat)))
% 0.48/0.91  (assume @p111 (exists @t285 (_ @t284 tptp.top_to1411004326lle_tv)))
% 0.48/0.91  (assume @p112 (exists @t287 (_ @t286 tptp.top_to1555900337at_nat)))
% 0.48/0.91  (assume @p113 (exists @t180 (_ @t288 tptp.top_top_set_nat)))
% 0.48/0.91  (assume @p114 (exists @t177 (_ @t289 tptp.top_to1057771083lle_tv)))
% 0.48/0.91  (assume @p115 (forall @t155 (=> (forall @t272 (_ @t271 @t153)) (= tptp.top_to775056195lle_fm @t153))))
% 0.48/0.91  (assume @p116 (forall @t158 (=> (forall @t275 (_ @t274 @t156)) (= tptp.top_to138697918lle_tv @t156))))
% 0.48/0.91  (assume @p117 (forall @t161 (=> (forall @t278 (_ @t277 @t159)) (= tptp.top_to449985143lle_tv @t159))))
% 0.48/0.91  (assume @p118 (forall @t164 (=> (forall @t281 (_ @t280 @t162)) (= tptp.top_to1541413903at_nat @t162))))
% 0.48/0.91  (assume @p119 (forall (@list @t290) (=> (forall @t283 @t291) (= tptp.top_to975729152tv_nat @t290))))
% 0.48/0.91  (assume @p120 (forall (@list @t292) (=> (forall @t285 @t293) (= tptp.top_to1411004326lle_tv @t292))))
% 0.48/0.91  (assume @p121 (forall (@list @t294) (=> (forall @t287 @t295) (= tptp.top_to1555900337at_nat @t294))))
% 0.48/0.91  (assume @p122 (forall @t174 (=> (forall @t180 @t296) (= tptp.top_top_set_nat @t170))))
% 0.48/0.91  (assume @p123 (forall @t169 (=> (forall @t177 @t297) (= tptp.top_to1057771083lle_tv @t165))))
% 0.48/0.91  (assume @p124 (forall (@list @t298 @t300 @t90) (=> (forall (@list @t182) (=> (_ (_ tptp.member1531318361lle_tv @t182) @t298) (= (_ @t300 @t183) @t182))) @t299)))
% 0.48/0.91  (assume @p125 (forall (@list @t290 @t302 @t104) (=> (forall @t283 (=> @t291 (= (_ @t302 @t192) @t191))) @t301)))
% 0.48/0.91  (assume @p126 (forall (@list @t292 @t304 @t111) (=> (forall @t285 (=> @t293 (= (_ @t304 @t196) @t195))) @t303)))
% 0.48/0.91  (assume @p127 (forall (@list @t294 @t306 @t118) (=> (forall @t287 (=> @t295 (= (_ @t306 @t200) @t199))) @t305)))
% 0.48/0.91  (assume @p128 (forall (@list @t170 @t308 @t97) (=> (forall @t180 (=> @t296 @t309)) @t307)))
% 0.48/0.91  (assume @p129 (forall @t314 (=> (forall @t180 (=> @t296 @t313)) @t310)))
% 0.48/0.91  (assume @p130 (forall @t319 (=> (forall @t177 (=> @t297 @t318)) @t315)))
% 0.48/0.91  (assume @p131 (forall @t322 (=> @t299 (=> (not @t89) (=> @t321 (=> @t320 (not @t91)))))))
% 0.48/0.91  (assume @p132 (forall @t325 (=> @t301 (=> (not @t103) (=> @t324 (=> @t323 (not @t105)))))))
% 0.48/0.91  (assume @p133 (forall @t328 (=> @t303 (=> (not @t110) (=> @t327 (=> @t326 (not @t112)))))))
% 0.48/0.91  (assume @p134 (forall @t331 (=> @t305 (=> (not @t117) (=> @t330 (=> @t329 (not @t119)))))))
% 0.48/0.91  (assume @p135 (forall @t336 (=> @t307 (=> @t335 (=> @t334 (=> @t333 (not @t98)))))))
% 0.48/0.91  (assume @p136 (forall @t337 (=> @t310 (=> @t335 (=> @t334 (=> @t333 (not @t124)))))))
% 0.48/0.91  (assume @p137 (forall @t341 (=> @t315 (=> (not @t129) (=> @t340 (=> @t339 (not @t133)))))))
% 0.48/0.91  (assume @p138 (forall @t322 (=> @t299 (=> @t321 (=> @t320 @t210)))))
% 0.48/0.91  (assume @p139 (forall @t325 (=> @t301 (=> @t324 (=> @t323 @t212)))))
% 0.48/0.91  (assume @p140 (forall @t328 (=> @t303 (=> @t327 (=> @t326 @t213)))))
% 0.48/0.91  (assume @p141 (forall @t331 (=> @t305 (=> @t330 (=> @t329 @t214)))))
% 0.48/0.91  (assume @p142 (forall @t336 (=> @t307 (=> @t334 (=> @t333 @t211)))))
% 0.48/0.91  (assume @p143 (forall @t337 (=> @t310 (=> @t334 (=> @t333 @t215)))))
% 0.48/0.91  (assume @p144 (forall @t341 (=> @t315 (=> @t340 (=> @t339 @t216)))))
% 0.48/0.91  (assume @p145 (forall (@list @t298 @t90 @t300) (=> (forall (@list @t342) (=> (_ (_ tptp.member1531318361lle_tv @t342) @t298) (= (_ @t90 @t342) (_ @t300 @t342)))) (= @t299 (_ (_ tptp.inj_on2112487900lle_tv @t300) @t298)))))
% 0.48/0.91  (assume @p146 (forall (@list @t290 @t104 @t302) (=> (forall (@list @t343) (=> (_ (_ tptp.member737151281tv_nat @t343) @t290) (= (_ @t104 @t343) (_ @t302 @t343)))) (= @t301 (_ (_ tptp.inj_on552895452tv_nat @t302) @t290)))))
% 0.48/0.91  (assume @p147 (forall (@list @t292 @t111 @t304) (=> (forall (@list @t344) (=> (_ (_ tptp.member813679063lle_tv @t344) @t292) (= (_ @t111 @t344) (_ @t304 @t344)))) (= @t303 (_ (_ tptp.inj_on1745913142lle_tv @t304) @t292)))))
% 0.48/0.91  (assume @p148 (forall (@list @t294 @t118 @t306) (=> (forall (@list @t345) (=> (_ (_ tptp.member701585322at_nat @t345) @t294) (= (_ @t118 @t345) (_ @t306 @t345)))) (= @t305 (_ (_ tptp.inj_on26176689at_nat @t306) @t294)))))
% 0.48/0.91  (assume @p149 (forall (@list @t170 @t97 @t346) (=> (forall @t349 (=> @t348 (= (_ @t97 @t347) (_ @t346 @t347)))) (= @t307 (_ (_ tptp.inj_on1955349912lle_tv @t346) @t170)))))
% 0.48/0.91  (assume @p150 (forall (@list @t170 @t44 @t311) (=> (forall @t349 (=> @t348 (= (_ @t44 @t347) (_ @t311 @t347)))) (= @t310 @t351))))
% 0.48/0.91  (assume @p151 (forall (@list @t165 @t130 @t316) (=> (forall (@list @t354) (=> (_ (_ tptp.member266900804lle_tv @t354) @t165) (= (_ @t130 @t354) (_ @t316 @t354)))) (= @t315 @t353))))
% 0.48/0.91  (assume @p152 (forall (@list @t170 @t44) (=> (forall @t188 (=> @t296 (=> (_ (_ tptp.member_nat @t185) @t170) @t203))) @t310)))
% 0.48/0.91  (assume @p153 (forall (@list @t165 @t130) (=> (forall @t208 (=> @t297 (=> (_ (_ tptp.member266900804lle_tv @t205) @t165) @t207))) @t315)))
% 0.48/0.91  (assume @p154 (forall @t337 (=> @t310 (=> @t124 (=> @t334 (=> @t333 @t96))))))
% 0.48/0.91  (assume @p155 (forall @t341 (=> @t315 (=> @t133 (=> @t340 (=> @t339 @t129))))))
% 0.48/0.91  (assume @p156 (forall (@list @t236 @t355) (=> @t243 (=> (forall @t265 (_ @t236 @t264)) (=> (forall @t262 (=> @t357 (_ @t236 @t261))) (=> (forall @t258 (=> @t357 (=> @t356 (_ @t236 @t260)))) (=> (forall @t258 (=> @t357 (=> @t356 (_ @t236 @t259)))) (=> (forall @t258 (=> @t357 (=> @t356 (_ @t236 @t256)))) (_ @t236 @t355)))))))))
% 0.48/0.91  (assume @p157 (forall @t71 (=> (forall (@list @t358 @t263) (not (= @t70 (_ @t359 @t264)))) (=> (forall (@list @t358) (not (= @t70 (_ @t359 tptp.paraco367965286_Truth)))) (=> (forall (@list @t358 @t255) (not (= @t70 (_ @t359 @t261)))) (=> (forall @t360 (not (= @t70 (_ @t359 @t260)))) (=> (forall @t360 (not (= @t70 (_ @t359 @t259)))) (not (forall @t360 (not (= @t70 (_ @t359 @t256))))))))))))
% 0.48/0.91  (assume @p158 (= tptp.top_top_nat_o (lambda @t173 (_ @t172 tptp.top_top_set_nat))))
% 0.48/0.91  (assume @p159 (= tptp.top_to1299250770e_tv_o (lambda @t168 (_ @t167 tptp.top_to1057771083lle_tv))))
% 0.48/0.91  (assume @p160 (forall @t374 (=> @t373 (=> (forall @t372 (=> @t371 (not @t370))) (not (forall @t367 (=> @t366 (not @t363))))))))
% 0.48/0.91  (assume @p161 (forall (@list @t21 @t375) (=> @t64 @t377)))
% 0.48/0.91  (assume @p162 (forall (@list @t375 @t21) (=> (not @t377) (not @t64))))
% 0.48/0.91  (assume @p163 (forall (@list @t44 @t82) (=> @t126 (= (_ (_ (_ tptp.the_inv_into_nat_nat tptp.top_top_set_nat) @t44) @t123) @t82))))
% 0.48/0.91  (assume @p164 (forall (@list @t130 @t84) (=> @t135 (= (_ (_ (_ tptp.the_in452116896lle_tv tptp.top_to1057771083lle_tv) @t130) @t132) @t84))))
% 0.48/0.91  (assume @p165 (forall (@list @t375 @t21 @t20) (= (_ @t376 @t28) (and @t377 (_ @t376 @t20)))))
% 0.48/0.91  (assume @p166 (forall (@list @t379 @t378) (= (= @t380 (_ tptp.paraco793048302_Indet @t378)) (= @t379 @t378))))
% 0.48/0.91  (assume @p167 (forall (@list @t146 @t381) (=> (_ @t146 @t1) (=> (_ @t146 @t7) (=> (forall @t367 (_ @t146 @t364)) (_ @t146 @t381))))))
% 0.48/0.91  (assume @p168 (forall (@list @t384 @t383 @t382) (=> (forall @t388 (_ @t386 @t369)) (=> (forall @t387 (_ @t386 @t364)) (_ (_ @t384 @t383) @t382)))))
% 0.48/0.91  (assume @p169 (forall @t86 (=> (not (= @t84 @t1)) (=> (not (= @t84 @t7)) (not (forall @t367 (not (= @t84 @t364))))))))
% 0.48/0.91  (assume @p170 (forall (@list @t128) (=> (forall (@list @t390) (not (= @t128 (_ tptp.paraco1344940915le_Det @t390)))) (not (forall (@list @t389) (not (= @t128 (_ tptp.paraco793048302_Indet @t389))))))))
% 0.48/0.91  (assume @p171 (forall (@list @t146 @t391) (=> (forall (@list @t392) (_ @t146 (_ tptp.paraco1344940915le_Det @t392))) (=> (forall @t180 (_ @t146 (_ tptp.paraco793048302_Indet @t179))) (_ @t146 @t391)))))
% 0.48/0.91  (assume @p172 (forall (@list @t14 @t379) (not (= @t15 @t380))))
% 0.48/0.91  (assume @p173 (forall (@list @t44 @t170 @t82) (=> @t310 (=> @t334 (= (_ @t393 @t123) @t82)))))
% 0.48/0.91  (assume @p174 (forall (@list @t130 @t165 @t84) (=> @t315 (=> @t340 (= (_ @t394 @t132) @t84)))))
% 0.48/0.91  (assume @p175 (forall @t337 (=> @t310 (=> (= @t123 @t95) (=> @t334 (= @t395 @t82))))))
% 0.48/0.91  (assume @p176 (forall @t341 (=> @t315 (=> (= @t132 @t128) (=> @t340 (= @t396 @t84))))))
% 0.48/0.91  (assume @p177 (forall (@list @t35 @t36 @t379) (= (_ @t37 @t380) (_ @t36 @t379))))
% 0.48/0.91  (assume @p178 (forall (@list @t44 @t397) (= (_ @t45 (_ tptp.paraco793048302_Indet @t397)) (_ tptp.paraco793048302_Indet (_ @t44 @t397)))))
% 0.48/0.91  (assume @p179 (forall (@list @t401 @t399 @t400 @t398) (= (= @t402 (_ (_ tptp.produc1710735575lle_fm @t400) @t398)) (and (= @t401 @t400) (= @t399 @t398)))))
% 0.48/0.91  (assume @p180 (forall (@list @t406 @t404 @t405 @t403) (= (= @t407 (_ (_ tptp.produc1680557635lle_tv @t405) @t403)) (and (= @t406 @t405) (= @t404 @t403)))))
% 0.48/0.91  (assume @p181 (forall @t418 (= @t417 (and @t413 @t410))))
% 0.48/0.91  (assume @p182 (forall @t429 (= @t428 (and @t424 @t421))))
% 0.48/0.91  (assume @p183 (forall @t41 (= @t38 (_ (_ (_ tptp.paraco2051596139lle_tv (_ (_ tptp.produc234482697lle_tv @t7) @t1)) tptp.paraco793048302_Indet) @t24))))
% 0.48/0.91  (assume @p184 (forall (@list @t433) (exists @t434 (= @t433 @t432))))
% 0.48/0.91  (assume @p185 (forall (@list @t437) (exists @t438 (= @t437 @t436))))
% 0.48/0.91  (assume @p186 (forall @t448 (= @t447 (not (or (and @t441 (not @t444)) (and @t442 (not @t440)))))))
% 0.48/0.91  (assume @p187 (forall (@list @t449 @t443 @t439 @t441) (= (_ @t449 @t446) (_ (_ (_ tptp.produc234482697lle_tv (_ @t449 @t443)) (_ @t449 @t439)) @t441))))
% 0.48/0.91  (assume @p188 (forall @t448 (= @t447 (and (=> @t441 @t444) (=> @t442 @t440)))))
% 0.48/0.91  (assume @p189 (forall @t450 (= (_ @t445 true) @t443)))
% 0.48/0.91  (assume @p190 (forall @t450 (= (_ @t445 false) @t439)))
% 0.48/0.91  (assume @p191 (forall @t74 (=> (forall @t388 (not (= @t73 (_ @t451 @t369)))) (not (forall @t387 (not (= @t73 (_ @t451 @t364))))))))
% 0.48/0.91  (assume @p192 (forall (@list @t138 @t452) (=> @t457 (_ @t138 @t452))))
% 0.48/0.91  (assume @p193 (forall (@list @t142 @t458) (=> @t463 (_ @t142 @t458))))
% 0.48/0.91  (assume @p194 (forall (@list @t464) (not (forall @t456 (not (= @t464 @t455))))))
% 0.48/0.91  (assume @p195 (forall (@list @t465) (not (forall @t462 (not (= @t465 @t461))))))
% 0.48/0.91  (assume @p196 (forall @t418 (=> @t417 (not (=> @t413 (not @t410))))))
% 0.48/0.91  (assume @p197 (forall @t429 (=> @t428 (not (=> @t424 (not @t421))))))
% 0.48/0.91  (assume @p198 (forall (@list @t138 @t433) (=> @t457 (_ @t138 @t433))))
% 0.48/0.91  (assume @p199 (forall (@list @t142 @t437) (=> @t463 (_ @t142 @t437))))
% 0.48/0.91  (assume @p200 (forall (@list @t468 @t470 @t466 @t467) (=> (_ (_ tptp.member1474794996lle_fm (_ @t469 @t470)) @t466) (=> (= @t467 @t470) (_ (_ tptp.member1474794996lle_fm (_ @t469 @t467)) @t466)))))
% 0.48/0.91  (assume @p201 (forall (@list @t473 @t475 @t471 @t472) (=> (_ (_ tptp.member1569366824lle_tv (_ @t474 @t475)) @t471) (=> (= @t472 @t475) (_ (_ tptp.member1569366824lle_tv (_ @t474 @t472)) @t471)))))
% 0.48/0.91  (assume @p202 (forall (@list @t477 @t476 @t247) (= (_ (_ tptp.produc1942165868lle_fm @t477) @t479) (_ (_ tptp.produc1710735575lle_fm (_ @t477 @t476)) @t247))))
% 0.48/0.91  (assume @p203 (forall (@list @t480 @t362 @t128) (= (_ (_ tptp.produc939316703lle_tv @t480) @t482) (_ (_ tptp.produc1680557635lle_tv (_ @t480 @t362)) @t128))))
% 0.48/0.91  (assume @p204 (forall (@list @t483 @t476 @t247) (= (_ (_ tptp.produc1807466521lle_tv @t483) @t479) (_ @t478 (_ @t483 @t247)))))
% 0.48/0.91  (assume @p205 (forall (@list @t130 @t362 @t128) (= (_ (_ tptp.produc109093078at_nat @t130) @t482) (_ @t481 @t131))))
% 0.48/0.91  (assume @p206 (forall @t374 (=> @t373 (=> (_ @t484 (_ @t481 @t365)) (=> (forall @t372 (=> @t371 (=> @t370 (not (_ @t484 (_ @t481 @t369)))))) (not (forall @t367 (=> @t366 (=> @t363 (not (_ @t484 (_ @t481 @t364))))))))))))
% 0.48/0.91  (assume @p207 (forall (@list @t486 @t485) (=> @t488 (=> @t487 (_ (_ tptp.inj_on26176689at_nat (_ (_ tptp.produc505105722at_nat @t486) @t485)) tptp.top_to1555900337at_nat)))))
% 0.48/0.91  (assume @p208 (forall (@list @t486 @t489) (=> @t488 (=> @t490 (_ (_ tptp.inj_on1745913142lle_tv (_ (_ tptp.produc2101297531lle_tv @t486) @t489)) tptp.top_to1411004326lle_tv)))))
% 0.48/0.91  (assume @p209 (forall (@list @t491 @t485) (=> @t492 (=> @t487 (_ (_ tptp.inj_on552895452tv_nat (_ (_ tptp.produc42536895at_nat @t491) @t485)) tptp.top_to975729152tv_nat)))))
% 0.48/0.91  (assume @p210 (forall (@list @t491 @t489) (=> @t492 (=> @t490 (_ (_ tptp.inj_on2112487900lle_tv (_ (_ tptp.produc1345917071lle_tv @t491) @t489)) tptp.top_to1871154984lle_tv)))))
% 0.48/0.91  (assume @p211 (forall @t496 (=> @t495 @t494)))
% 0.48/0.91  (assume @p212 (forall @t500 (=> @t499 @t498)))
% 0.48/0.91  (assume @p213 (forall (@list @t477 @t501 @t412 @t409) (= (_ @t503 @t416) @t502)))
% 0.48/0.91  (assume @p214 (forall (@list @t505 @t504 @t412 @t409) (= (_ @t507 @t416) @t506)))
% 0.48/0.91  (assume @p215 (forall (@list @t509 @t508 @t423 @t420) (= (_ @t511 @t427) @t510)))
% 0.48/0.91  (assume @p216 (forall (@list @t480 @t316 @t423 @t420) (= (_ @t513 @t427) @t512)))
% 0.48/0.91  (assume @p217 (forall @t496 (=> @t494 @t495)))
% 0.48/0.91  (assume @p218 (forall @t500 (=> @t498 @t499)))
% 0.48/0.91  (assume @p219 (forall @t516 (=> @t310 (= (_ (_ tptp.image_nat_nat @t393) @t515) @t170))))
% 0.48/0.91  (assume @p220 (forall @t519 (=> @t315 (= (_ (_ tptp.image_335818702lle_tv @t394) @t518) @t165))))
% 0.48/0.91  (assume @p221 (forall (@list @t412 @t409 @t466 @t477 @t501) (=> @t521 (_ (_ tptp.member1474794996lle_fm @t502) @t520))))
% 0.48/0.91  (assume @p222 (forall (@list @t412 @t409 @t466 @t505 @t504) (=> @t521 (_ (_ tptp.member1569366824lle_tv @t506) @t522))))
% 0.48/0.91  (assume @p223 (forall (@list @t423 @t420 @t471 @t509 @t508) (=> @t524 (_ (_ tptp.member1474794996lle_fm @t510) @t523))))
% 0.48/0.91  (assume @p224 (forall (@list @t423 @t420 @t471 @t480 @t316) (=> @t524 (_ (_ tptp.member1569366824lle_tv @t512) @t525))))
% 0.48/0.91  (assume @p225 (forall (@list @t257 @t526) (= (_ tptp.produc1232814113lle_tv @t529) @t528)))
% 0.48/0.91  (assume @p226 (forall (@list @t84 @t530) (= (_ tptp.produc178635363at_nat @t533) @t532)))
% 0.48/0.91  (assume @p227 (forall (@list @t476 @t247) (= (_ tptp.produc1000205111lle_fm @t479) @t534)))
% 0.48/0.91  (assume @p228 (forall (@list @t362 @t128) (= (_ tptp.produc225513635lle_tv @t482) @t535)))
% 0.48/0.91  (assume @p229 (forall (@list @t247 @t476 @t153) (= (_ (_ tptp.member74361182lle_tv @t534) (_ (_ tptp.image_924970994lle_tv tptp.produc1000205111lle_fm) @t153)) (_ (_ tptp.member1474794996lle_fm @t479) @t153))))
% 0.48/0.91  (assume @p230 (forall (@list @t128 @t362 @t159) (= (_ (_ tptp.member1234290208at_nat @t535) (_ (_ tptp.image_1724396928at_nat tptp.produc225513635lle_tv) @t159)) (_ (_ tptp.member1569366824lle_tv @t482) @t159))))
% 0.48/0.91  (assume @p231 (forall (@list @t526 @t257 @t536) (= (_ (_ tptp.member1474794996lle_fm @t528) (_ (_ tptp.image_326034184lle_fm tptp.produc1232814113lle_tv) @t536)) (_ (_ tptp.member74361182lle_tv @t529) @t536))))
% 0.48/0.91  (assume @p232 (forall (@list @t530 @t84 @t537) (= (_ (_ tptp.member1569366824lle_tv @t532) (_ (_ tptp.image_769496456lle_tv tptp.produc178635363at_nat) @t537)) (_ (_ tptp.member1234290208at_nat @t533) @t537))))
% 0.48/0.91  (assume @p233 (forall (@list @t44 @t311) (=> @t541 (=> @t539 (= (_ (_ tptp.image_815163717at_nat (_ @t538 @t311)) tptp.top_to1555900337at_nat) tptp.top_to1555900337at_nat)))))
% 0.48/0.91  (assume @p234 (forall (@list @t44 @t346) (=> @t541 (=> @t542 (= (_ (_ tptp.image_1674248956lle_tv (_ (_ tptp.produc313957681lle_tv @t44) @t346)) tptp.top_to1555900337at_nat) tptp.top_to1411004326lle_tv)))))
% 0.48/0.91  (assume @p235 (forall (@list @t44 @t308) (=> @t541 (=> @t543 (= (_ (_ tptp.image_1787705850at_nat (_ (_ tptp.produc1685803475tv_nat @t44) @t308)) tptp.top_to1411004326lle_tv) tptp.top_to1555900337at_nat)))))
% 0.48/0.91  (assume @p236 (forall (@list @t44 @t316) (=> @t541 (=> @t544 (= (_ (_ tptp.image_149830562lle_tv (_ (_ tptp.produc2101297531lle_tv @t44) @t316)) tptp.top_to1411004326lle_tv) tptp.top_to1411004326lle_tv)))))
% 0.48/0.91  (assume @p237 (forall (@list @t97 @t311) (=> @t545 (=> @t539 (= (_ (_ tptp.image_1597721174tv_nat (_ (_ tptp.produc1250721397at_nat @t97) @t311)) tptp.top_to1555900337at_nat) tptp.top_to975729152tv_nat)))))
% 0.48/0.91  (assume @p238 (forall (@list @t97 @t346) (=> @t545 (=> @t542 (= (_ (_ tptp.image_1507992062lle_tv (_ (_ tptp.produc210389789lle_tv @t97) @t346)) tptp.top_to1555900337at_nat) tptp.top_to1871154984lle_tv)))))
% 0.48/0.91  (assume @p239 (forall (@list @t97 @t308) (=> @t545 (=> @t543 (= (_ (_ tptp.image_53754658tv_nat (_ (_ tptp.produc189459613tv_nat @t97) @t308)) tptp.top_to1411004326lle_tv) tptp.top_to975729152tv_nat)))))
% 0.48/0.91  (assume @p240 (forall (@list @t97 @t316) (=> @t545 (=> @t544 (= (_ (_ tptp.image_988201162lle_tv (_ (_ tptp.produc1975500101lle_tv @t97) @t316)) tptp.top_to1411004326lle_tv) tptp.top_to1871154984lle_tv)))))
% 0.48/0.91  (assume @p241 (forall (@list @t546 @t311) (=> @t547 (=> @t539 (= (_ (_ tptp.image_1805124128at_nat (_ (_ tptp.produc386540311at_nat @t546) @t311)) tptp.top_to975729152tv_nat) tptp.top_to1555900337at_nat)))))
% 0.48/0.91  (assume @p242 (forall (@list @t546 @t346) (=> @t547 (=> @t542 (= (_ (_ tptp.image_1200372424lle_tv (_ (_ tptp.produc72207551lle_tv @t546) @t346)) tptp.top_to975729152tv_nat) tptp.top_to1411004326lle_tv)))))
% 0.48/0.91  (assume @p243 (forall @t314 (=> (forall @t180 (=> @t296 (forall (@list @t548) (=> (_ (_ tptp.member_nat @t548) @t170) (= (= @t312 (_ @t311 (_ @t44 @t548))) (= (_ @t311 @t179) (_ @t311 @t548))))))) (=> @t310 (= (_ @t350 @t515) @t351)))))
% 0.48/0.91  (assume @p244 (forall @t319 (=> (forall @t177 (=> @t297 (forall (@list @t549) (=> (_ (_ tptp.member266900804lle_tv @t549) @t165) (= (= @t317 (_ @t316 (_ @t130 @t549))) (= (_ @t316 @t176) (_ @t316 @t549))))))) (=> @t315 (= (_ @t352 @t518) @t353)))))
% 0.48/0.91  (assume @p245 (forall @t551 (=> @t541 (exists @t180 @t550))))
% 0.48/0.91  (assume @p246 (forall @t553 (=> @t545 (exists @t180 @t552))))
% 0.48/0.91  (assume @p247 (forall @t556 (=> @t547 (exists @t177 @t555))))
% 0.48/0.91  (assume @p248 (forall @t560 (=> @t559 (exists @t177 @t557))))
% 0.48/0.91  (assume @p249 (forall @t551 (=> @t541 (not (forall @t180 (not @t550))))))
% 0.48/0.91  (assume @p250 (forall @t553 (=> @t545 (not (forall @t180 (not @t552))))))
% 0.48/0.91  (assume @p251 (forall @t556 (=> @t547 (not (forall @t177 (not @t555))))))
% 0.48/0.91  (assume @p252 (forall @t560 (=> @t559 (not (forall @t177 (not @t557))))))
% 0.48/0.91  (assume @p253 (forall (@list @t311 @t44) (=> (forall @t180 @t313) @t539)))
% 0.48/0.91  (assume @p254 (forall (@list @t346 @t546) (=> (forall @t177 (= (_ @t346 @t554) @t176)) @t542)))
% 0.48/0.91  (assume @p255 (forall (@list @t308 @t97) (=> (forall @t180 @t309) @t543)))
% 0.48/0.91  (assume @p256 (forall (@list @t316 @t130) (=> (forall @t177 @t318) @t544)))
% 0.48/0.91  (assume @p257 (forall @t204 (= @t541 (forall @t561 (exists @t173 (= @t219 @t230))))))
% 0.48/0.91  (assume @p258 (forall @t189 (= @t545 (forall @t562 (exists @t173 (= @t231 @t221))))))
% 0.48/0.91  (assume @p259 (forall (@list @t546) (= @t547 (forall @t561 (exists @t168 (= @t219 (_ @t546 @t166)))))))
% 0.48/0.91  (assume @p260 (forall @t209 (= @t559 (forall @t562 (exists @t168 (= @t231 @t234))))))
% 0.48/0.91  (assume @p261 (forall (@list @t44 @t563) (=> @t126 (= (_ (_ tptp.member_nat @t563) @t540) (exists @t173 (and (= @t563 @t230) (forall @t561 (=> (= @t563 @t229) (= @t219 @t171)))))))))
% 0.48/0.91  (assume @p262 (forall (@list @t130 @t420) (=> @t135 (= (_ (_ tptp.member266900804lle_tv @t420) @t558) (exists @t168 (and (= @t420 @t234) (forall @t562 (=> (= @t420 @t233) (= @t231 @t166)))))))))
% 0.48/0.91  (assume @p263 (forall @t566 (=> @t126 @t565)))
% 0.48/0.91  (assume @p264 (forall @t569 (=> @t135 @t568)))
% 0.48/0.91  (assume @p265 (forall (@list @t44 @t149 @t170) (=> @t126 @t570)))
% 0.48/0.91  (assume @p266 (forall (@list @t130 @t145 @t165) (=> @t135 @t571)))
% 0.48/0.91  (assume @p267 (forall (@list @t573 @t477 @t501 @t466) (=> (_ @t574 @t520) (not (forall @t434 (=> (= @t573 (_ (_ tptp.produc1710735575lle_fm (_ @t477 @t431)) (_ @t501 @t430))) @t572))))))
% 0.48/0.91  (assume @p268 (forall (@list @t573 @t509 @t508 @t471) (=> (_ @t574 @t523) (not (forall @t438 (=> (= @t573 (_ (_ tptp.produc1710735575lle_fm (_ @t509 @t435)) (_ @t508 @t205))) @t575))))))
% 0.48/0.91  (assume @p269 (forall (@list @t576 @t505 @t504 @t466) (=> (_ @t577 @t522) (not (forall @t434 (=> (= @t576 (_ (_ tptp.produc1680557635lle_tv (_ @t505 @t431)) (_ @t504 @t430))) @t572))))))
% 0.48/0.91  (assume @p270 (forall (@list @t576 @t480 @t316 @t471) (=> (_ @t577 @t525) (not (forall @t438 (=> (= @t576 (_ (_ tptp.produc1680557635lle_tv (_ @t480 @t435)) (_ @t316 @t205))) @t575))))))
% 0.48/0.91  (assume @p271 (forall (@list @t44 @t170 @t95) (=> @t310 (=> (_ @t332 @t515) (= (_ @t44 @t395) @t95)))))
% 0.48/0.91  (assume @p272 (forall (@list @t130 @t165 @t128) (=> @t315 (=> (_ @t338 @t518) (= (_ @t130 @t396) @t128)))))
% 0.48/0.91  (assume @p273 (forall @t516 (=> @t310 (_ (_ tptp.inj_on_nat_nat @t393) @t515))))
% 0.48/0.91  (assume @p274 (forall @t519 (=> @t315 (_ (_ tptp.inj_on772319074lle_tv @t394) @t518))))
% 0.48/0.91  (assume @p275 (forall (@list @t44 @t578) (=> @t126 (=> @t580 (_ @t579 (_ (_ tptp.inv_image_nat_nat @t578) @t44))))))
% 0.48/0.91  (assume @p276 (forall (@list @t97 @t581) (=> @t100 (=> @t583 (_ @t579 (_ (_ tptp.inv_im516950809tv_nat @t581) @t97))))))
% 0.48/0.91  (assume @p277 (forall (@list @t546 @t578) (=> (_ (_ tptp.inj_on1179712058tv_nat @t546) tptp.top_to1057771083lle_tv) (=> @t580 (_ @t582 (_ (_ tptp.inv_im1292588663lle_tv @t578) @t546))))))
% 0.48/0.91  (assume @p278 (forall (@list @t130 @t581) (=> @t135 (=> @t583 (_ @t582 (_ (_ tptp.inv_im719552961lle_tv @t581) @t130))))))
% 0.48/0.91  (assume @p279 (forall @t585 (= @t584 @t452)))
% 0.48/0.91  (assume @p280 (forall @t587 (= @t586 @t458)))
% 0.48/0.91  (assume @p281 (forall (@list @t476 @t247 @t412) (=> (= @t588 @t412) (= @t476 @t412))))
% 0.48/0.91  (assume @p282 (forall (@list @t362 @t128 @t423) (=> (= @t589 @t423) (= @t362 @t423))))
% 0.48/0.91  (assume @p283 (forall (@list @t476 @t247 @t590) (=> (= @t591 @t590) (= @t247 @t590))))
% 0.48/0.91  (assume @p284 (forall (@list @t362 @t128 @t145) (=> (= @t592 @t145) (= @t128 @t145))))
% 0.48/0.91  (assume @p285 (forall @t593 (= (_ tptp.produc29804011lle_fm @t402) @t401)))
% 0.48/0.91  (assume @p286 (forall @t594 (= (_ tptp.produc1636169559lle_tv @t407) @t406)))
% 0.48/0.91  (assume @p287 (forall @t593 (= (_ tptp.produc148705065lle_fm @t402) @t399)))
% 0.48/0.91  (assume @p288 (forall @t594 (= (_ tptp.produc547496597lle_tv @t407) @t404)))
% 0.48/0.91  (assume @p289 (forall @t585 (= @t452 @t584)))
% 0.48/0.91  (assume @p290 (forall @t587 (= @t458 @t586)))
% 0.48/0.91  (assume @p291 (forall (@list @t595) (= @t595 (_ (_ tptp.produc1710735575lle_fm (_ tptp.produc29804011lle_fm @t595)) (_ tptp.produc148705065lle_fm @t595)))))
% 0.48/0.91  (assume @p292 (forall (@list @t596) (= @t596 (_ (_ tptp.produc1680557635lle_tv (_ tptp.produc1636169559lle_tv @t596)) (_ tptp.produc547496597lle_tv @t596)))))
% 0.48/0.91  (assume @p293 (forall (@list @t597 @t247 @t476) (=> (_ (_ @t597 @t247) @t476) (_ (_ @t597 @t591) @t588))))
% 0.48/0.91  (assume @p294 (forall (@list @t598 @t128 @t362) (=> (_ (_ @t598 @t128) @t362) (_ (_ @t598 @t592) @t589))))
% 0.48/0.91  (assume @p295 (forall (@list @t602 @t599 @t601 @t20) (=> (_ @t602 @t599) (=> (_ @t601 @t20) (and (_ @t602 (_ tptp.produc29804011lle_fm @t600)) (_ @t601 (_ tptp.produc148705065lle_fm @t600)))))))
% 0.48/0.91  (assume @p296 (forall (@list @t606 @t604 @t175 @t603) (=> (_ @t606 @t604) (=> (_ @t175 @t603) (and (_ @t606 (_ tptp.produc1636169559lle_tv @t605)) (_ @t175 (_ tptp.produc547496597lle_tv @t605)))))))
% 0.48/0.91  (assume @p297 (forall (@list @t607 @t476 @t247 @t137) (=> (_ (_ @t607 @t476) @t247) (=> (= @t137 @t479) (_ (_ @t607 (_ tptp.produc29804011lle_fm @t137)) (_ tptp.produc148705065lle_fm @t137))))))
% 0.48/0.91  (assume @p298 (forall (@list @t384 @t362 @t128 @t141) (=> (_ (_ @t384 @t362) @t128) (=> (= @t141 @t482) (_ (_ @t384 (_ tptp.produc1636169559lle_tv @t141)) (_ tptp.produc547496597lle_tv @t141))))))
% 0.48/0.91  (assume @p299 (forall (@list @t409 @t433) (= (= @t409 (_ tptp.produc148705065lle_fm @t433)) (exists (@list @t608) (= @t433 (_ (_ tptp.produc1710735575lle_fm @t608) @t409))))))
% 0.48/0.91  (assume @p300 (forall (@list @t420 @t437) (= (= @t420 (_ tptp.produc547496597lle_tv @t437)) (exists (@list @t609) (= @t437 (_ (_ tptp.produc1680557635lle_tv @t609) @t420))))))
% 0.48/0.91  (assume @p301 (forall @t612 (=> @t611 (= (_ tptp.produc148705065lle_fm @t70) @t610))))
% 0.48/0.91  (assume @p302 (forall @t615 (=> @t614 (= (_ tptp.produc547496597lle_tv @t73) @t613))))
% 0.48/0.91  (assume @p303 (forall @t612 (=> @t611 (= (_ tptp.produc29804011lle_fm @t70) @t526))))
% 0.48/0.91  (assume @p304 (forall @t615 (=> @t614 (= (_ tptp.produc1636169559lle_tv @t73) @t530))))
% 0.48/0.91  (assume @p305 (forall (@list @t412 @t433) (= (= @t412 (_ tptp.produc29804011lle_fm @t433)) (exists (@list @t616) (= @t433 (_ @t415 @t616))))))
% 0.48/0.91  (assume @p306 (forall (@list @t423 @t437) (= (= @t423 (_ tptp.produc1636169559lle_tv @t437)) (exists (@list @t617) (= @t437 (_ @t426 @t617))))))
% 0.48/0.91  (assume @p307 (forall (@list @t578 @t618) (=> @t580 (=> @t619 (_ (_ tptp.total_1775715973at_nat tptp.top_to1555900337at_nat) (_ (_ tptp.lex_prod_nat_nat @t578) @t618))))))
% 0.48/0.91  (assume @p308 (forall (@list @t578 @t620) (=> @t580 (=> @t621 (_ (_ tptp.total_517371324lle_tv tptp.top_to1411004326lle_tv) (_ (_ tptp.lex_pr413684186lle_tv @t578) @t620))))))
% 0.48/0.91  (assume @p309 (forall (@list @t581 @t618) (=> @t583 (=> @t619 (_ (_ tptp.total_440843542tv_nat tptp.top_to975729152tv_nat) (_ (_ tptp.lex_pr1785529980tv_nat @t581) @t618))))))
% 0.48/0.91  (assume @p310 (forall (@list @t581 @t620) (=> @t583 (=> @t621 (_ (_ tptp.total_92239038lle_tv tptp.top_to1871154984lle_tv) (_ (_ tptp.lex_pr567812260lle_tv @t581) @t620))))))
% 0.48/0.91  (assume @p311 (forall (@list @t412 @t409 @t411 @t408 @t623 @t622) (= (_ (_ tptp.member1592865093lle_fm (_ (_ tptp.produc407632608lle_fm @t416) @t414)) (_ (_ tptp.lex_pr2001015487lle_fm @t623) @t622)) (or (_ (_ tptp.member146333935lle_tv (_ (_ tptp.produc1297923922lle_tv @t412) @t411)) @t623) (and @t413 (_ (_ tptp.member334644067lle_fm (_ (_ tptp.produc1126104134lle_fm @t409) @t408)) @t622))))))
% 0.48/0.91  (assume @p312 (forall (@list @t423 @t420 @t422 @t419 @t624 @t620) (= (_ (_ tptp.member1339857875lle_tv (_ (_ tptp.produc2057188974lle_tv @t427) @t425)) (_ (_ tptp.lex_pr1093414955lle_tv @t624) @t620)) (or (_ (_ tptp.member112824072at_nat (_ (_ tptp.produc780837143at_nat @t423) @t422)) @t624) (and @t424 (_ (_ tptp.member1531318361lle_tv (_ (_ tptp.produc2058540732lle_tv @t420) @t419)) @t620))))))
% 0.48/0.91  (assume @p313 (forall (@list @t578 @t44) (=> (_ tptp.wf_nat @t578) (=> @t126 (_ tptp.wf_nat (_ (_ tptp.image_815163717at_nat (_ @t538 @t44)) @t578))))))
% 0.48/0.91  (assume @p314 (forall (@list @t581 @t130) (=> (_ tptp.wf_Par1378404612lle_tv @t581) (=> @t135 (_ tptp.wf_Par1378404612lle_tv (_ (_ tptp.image_1221801032lle_tv (_ (_ tptp.produc1345917071lle_tv @t130) @t130)) @t581))))))
% 0.48/0.91  (assume @p315 (forall (@list @t602 @t476 @t626 @t247 @t625) (=> (_ @t602 @t476) (=> (_ (_ tptp.member334644067lle_fm (_ (_ tptp.produc1126104134lle_fm @t626) @t247)) (_ @t625 @t476)) (_ (_ tptp.member1592865093lle_fm (_ (_ tptp.produc407632608lle_fm (_ @t478 @t626)) @t479)) (_ (_ tptp.same_f1581085506lle_fm @t602) @t625))))))
% 0.48/0.91  (assume @p316 (forall (@list @t606 @t362 @t628 @t128 @t627) (=> (_ @t606 @t362) (=> (_ (_ tptp.member1531318361lle_tv (_ (_ tptp.produc2058540732lle_tv @t628) @t128)) (_ @t627 @t362)) (_ (_ tptp.member1339857875lle_tv (_ (_ tptp.produc2057188974lle_tv (_ @t481 @t628)) @t482)) (_ (_ tptp.same_f1138187694lle_tv @t606) @t627))))))
% 0.48/0.91  (assume @p317 (forall (@list @t44 @t170 @t82 @t564) (=> @t310 (=> (_ @t83 @t515) (=> @t630 (_ (_ tptp.member_nat (_ @t393 @t82)) @t564))))))
% 0.48/0.91  (assume @p318 (forall (@list @t130 @t165 @t84 @t567) (=> @t315 (=> (_ @t85 @t518) (=> @t632 (_ (_ tptp.member266900804lle_tv (_ @t394 @t84)) @t567))))))
% 0.48/0.91  (assume @p319 (forall (@list @t44 @t633 @t170 @t564) (=> (_ @t125 @t633) (=> (_ @t629 @t633) (=> (_ @t634 @t633) @t565)))))
% 0.48/0.91  (assume @p320 (forall (@list @t130 @t635 @t165 @t567) (=> (_ @t134 @t635) (=> (_ @t631 @t635) (=> (_ @t636 @t635) @t568)))))
% 0.48/0.91  (assume @p321 (forall (@list @t44 @t564 @t149 @t170) (=> @t637 (=> (_ @t152 @t564) (=> @t630 @t570)))))
% 0.48/0.91  (assume @p322 (forall (@list @t130 @t567 @t145 @t165) (=> @t638 (=> (_ @t148 @t567) (=> @t632 @t571)))))
% 0.48/0.91  (assume @p323 (forall @t642 (=> @t641 @t640)))
% 0.48/0.91  (assume @p324 (forall @t646 (=> @t645 @t644)))
% 0.48/0.91  (assume @p325 (forall @t642 (= @t641 @t640)))
% 0.48/0.91  (assume @p326 (forall @t646 (= @t645 @t644)))
% 0.48/0.91  (assume @p327 (forall @t642 (_ (_ tptp.ord_less_eq_set_nat @t639) tptp.top_top_set_nat)))
% 0.48/0.91  (assume @p328 (forall @t646 (_ (_ tptp.ord_le241064091lle_tv @t643) tptp.top_to1057771083lle_tv)))
% 0.48/0.91  (assume @p329 (forall @t174 (_ @t629 tptp.top_top_set_nat)))
% 0.48/0.91  (assume @p330 (forall @t169 (_ @t631 tptp.top_to1057771083lle_tv)))
% 0.48/0.91  (assume @p331 (forall @t566 (=> @t310 (=> (_ @t634 @t170) @t637))))
% 0.48/0.91  (assume @p332 (forall @t569 (=> @t315 (=> (_ @t636 @t165) @t638))))
% 0.48/0.91  (assume @p333 (forall (@list @t44 @t564 @t170) (=> @t637 (=> @t630 @t310))))
% 0.48/0.91  (assume @p334 (forall (@list @t130 @t567 @t165) (=> @t638 (=> @t632 @t315))))
% 0.48/0.91  (assume @p335 (forall (@list @t647) (or (= @t647 true) (= @t647 false))))
% 0.48/0.91  (assume @p336 (forall @t648 (= (_ (_ (_ tptp.if_Par1134130401lle_tv false) @t84) @t128) @t128)))
% 0.48/0.91  (assume @p337 (forall @t648 (= (_ (_ (_ tptp.if_Par1134130401lle_tv true) @t84) @t128) @t84)))
% 0.48/0.91  (assume @p338 @t651)
% 0.48/0.91  (assume @p339 true)
% 0.48/0.91  (step @p340 (= tptp.paraco327635598_valid @t652) :rule refl :args (@t652))
% 0.48/0.91  (step @p341 (= tptp.paraco761681009ge_int @t656) :rule refl :args (@t656))
% 0.48/0.91  (step @p342 (= tptp.top_to1299250770e_tv_o @t657) :rule refl :args (@t657))
% 0.48/0.91  (step @p343 (= tptp.top_top_nat_o @t658) :rule refl :args (@t658))
% 0.48/0.91  (step @p344 (= tptp.inj_on_nat_nat @t660) :rule refl :args (@t660))
% 0.48/0.91  (step @p345 (= tptp.inj_on772319074lle_tv @t663) :rule refl :args (@t663))
% 0.48/0.91  (step @p346 (= tptp.produc234482697lle_tv @t667) :rule refl :args (@t667))
% 0.48/0.91  (step @p347 (= tptp.produc1232814113lle_tv @t669) :rule refl :args (@t669))
% 0.48/0.91  (step @p348 (= tptp.produc178635363at_nat @t671) :rule refl :args (@t671))
% 0.48/0.91  (step @p349 :rule eq-symm :args (@t672 @t674))
% 0.48/0.91  (step @p350 :rule refl :args (@t674))
% 0.48/0.91  (step @p351 :rule refl :args (@t675))
% 0.48/0.91  (step @p352 :rule cong :premises (@p351 @p350) :args ((= @t675 @t674)))
% 0.48/0.91  (step @p353 :rule symm :premises (@p352))
% 0.48/0.91  (step @p354 :rule eq_resolve :premises (@p351 @p353))
% 0.48/0.91  (step @p355 :rule skolem_intro :args (@t673))
% 0.48/0.91  (step @p356 :rule symm :premises (@p355))
% 0.48/0.91  (step @p357 :rule refl :args (tptp.paraco1344940915le_Det))
% 0.48/0.91  (step @p358 :rule ho_cong :premises (@p357 @p356))
% 0.48/0.91  (step @p359 :rule trans :premises (@p358 @p354))
% 0.48/0.91  (step @p360 :rule refl :args (@t672))
% 0.48/0.91  (step @p361 :rule refl :args (@t3))
% 0.48/0.91  (step @p362 :rule cong :premises (@p361 @p360) :args ((= @t3 @t672)))
% 0.48/0.91  (step @p363 :rule symm :premises (@p362))
% 0.48/0.91  (step @p364 :rule eq_resolve :premises (@p361 @p363))
% 0.48/0.91  (step @p365 :rule cong :premises (@p364 @p359) :args (@t4))
% 0.48/0.91  (step @p366 :rule trans :premises (@p365 @p349))
% 0.48/0.91  (step @p367 :rule cong :premises (@p366) :args (@t5))
% 0.48/0.91  (step @p368 :rule eq_resolve :premises (@p1 @p367))
% 0.48/0.91  (step @p369 :rule refl :args (@t677))
% 0.48/0.91  (step @p370 :rule refl :args (@t678))
% 0.48/0.91  (step @p371 :rule cong :premises (@p370 @p369) :args ((= @t678 @t677)))
% 0.48/0.91  (step @p372 :rule symm :premises (@p371))
% 0.48/0.91  (step @p373 :rule eq_resolve :premises (@p370 @p372))
% 0.48/0.91  (step @p374 :rule evaluate :args ((not false)))
% 0.48/0.91  (step @p375 :rule skolem_intro :args (@t676))
% 0.48/0.91  (step @p376 :rule cong :premises (@p375) :args ((not @t676)))
% 0.48/0.91  (step @p377 :rule bool-eq-false :args (@t676))
% 0.48/0.91  (step @p378 :rule eq-symm :args (false @t676))
% 0.48/0.91  (step @p379 :rule trans :premises (@p378 @p377))
% 0.48/0.91  (step @p380 :rule trans :premises (@p379 @p376 @p374))
% 0.48/0.91  (step @p381 :rule true_elim :premises (@p380))
% 0.48/0.91  (step @p382 :rule ho_cong :premises (@p357 @p381))
% 0.48/0.91  (step @p383 :rule trans :premises (@p382 @p373))
% 0.48/0.91  (step @p384 :rule cong :premises (@p364 @p383) :args (@t10))
% 0.48/0.91  (step @p385 :rule eq_resolve :premises (@p5 @p384))
% 0.48/0.91  (step @p386 :rule refl :args (@t681))
% 0.48/0.91  (step @p387 :rule refl :args (@t682))
% 0.48/0.91  (step @p388 :rule cong :premises (@p387 @p386) :args ((= @t682 @t681)))
% 0.48/0.91  (step @p389 :rule symm :premises (@p388))
% 0.48/0.91  (step @p390 :rule eq_resolve :premises (@p387 @p389))
% 0.48/0.91  (step @p391 :rule refl :args (tptp.p2))
% 0.48/0.91  (step @p392 :rule eq-refl :args (@t679))
% 0.48/0.91  (step @p393 :rule skolem_intro :args (@t680))
% 0.48/0.91  (step @p394 :rule refl :args (@t679))
% 0.48/0.91  (step @p395 :rule cong :premises (@p394 @p393) :args ((= @t679 @t680)))
% 0.48/0.91  (step @p396 :rule trans :premises (@p395 @p392))
% 0.48/0.91  (step @p397 :rule true_elim :premises (@p396))
% 0.48/0.91  (step @p398 :rule refl :args (tptp.paraco1325918602e_eval))
% 0.48/0.91  (step @p399 :rule ho_cong :premises (@p398 @p397))
% 0.48/0.91  (step @p400 :rule ho_cong :premises (@p399 @p391))
% 0.48/0.91  (step @p401 :rule trans :premises (@p400 @p390))
% 0.48/0.91  (step @p402 :rule cong :premises (@p383 @p401) :args ((= @t7 @t683)))
% 0.48/0.91  (step @p403 :rule eq-symm :args (@t683 @t7))
% 0.48/0.91  (step @p404 :rule refl :args (@t7))
% 0.48/0.91  (step @p405 :rule beta-reduce :args ((= (_ @t684 tptp.i) @t679)))
% 0.48/0.91  (step @p406 :rule refl :args (tptp.i))
% 0.48/0.91  (step @p407 :rule beta-reduce :args ((= @t685 @t684)))
% 0.48/0.91  (step @p408 :rule ho_cong :premises (@p407 @p406))
% 0.48/0.91  (step @p409 :rule trans :premises (@p408 @p405))
% 0.48/0.91  (step @p410 :rule ho_cong :premises (@p398 @p409))
% 0.48/0.91  (step @p411 :rule ho_cong :premises (@p410 @p391))
% 0.48/0.91  (step @p412 :rule cong :premises (@p411 @p404) :args ((= @t686 @t7)))
% 0.48/0.91  (step @p413 :rule trans :premises (@p412 @p403))
% 0.48/0.91  (step @p414 :rule refl :args (tptp.f))
% 0.48/0.91  (step @p415 :rule ho_cong :premises (@p341 @p414))
% 0.48/0.91  (step @p416 :rule ho_cong :premises (@p415 @p406))
% 0.48/0.91  (step @p417 :rule ho_cong :premises (@p398 @p416))
% 0.48/0.91  (step @p418 :rule ho_cong :premises (@p417 @p391))
% 0.48/0.91  (step @p419 :rule cong :premises (@p418 @p404) :args (@t12))
% 0.48/0.91  (step @p420 :rule trans :premises (@p419 @p413))
% 0.48/0.91  (step @p421 :rule trans :premises (@p420 @p402))
% 0.48/0.91  (step @p422 :rule eq_resolve :premises (@p7 @p421))
% 0.48/0.91  (step @p423 :rule cong :premises (@p359 @p401) :args ((= @t1 @t683)))
% 0.48/0.91  (step @p424 :rule eq-symm :args (@t683 @t1))
% 0.48/0.91  (step @p425 :rule refl :args (@t1))
% 0.48/0.91  (step @p426 :rule cong :premises (@p411 @p425) :args (@t687))
% 0.48/0.91  (step @p427 :rule trans :premises (@p426 @p424))
% 0.48/0.91  (step @p428 :rule bool-double-not-elim :args (@t687))
% 0.48/0.91  (step @p429 :rule trans :premises (@p428 @p427))
% 0.48/0.91  (step @p430 :rule cong :premises (@p418 @p425) :args (@t649))
% 0.48/0.91  (step @p431 :rule cong :premises (@p430) :args (@t650))
% 0.48/0.91  (step @p432 :rule cong :premises (@p431) :args (@t651))
% 0.48/0.91  (step @p433 :rule trans :premises (@p432 @p429))
% 0.48/0.91  (step @p434 :rule trans :premises (@p433 @p423))
% 0.48/0.91  (step @p435 :rule eq_resolve :premises (@p338 @p434))
% 0.48/0.91  (step @p436 :rule refl :args (@t689))
% 0.48/0.91  (step @p437 :rule refl :args (@t691))
% 0.48/0.91  (step @p438 :rule refl :args (@t693))
% 0.48/0.91  (step @p439 :rule bool-double-not-elim :args (@t694))
% 0.48/0.91  (step @p440 :rule nary_cong :premises (@p439 @p438 @p437 @p436) :args ((or (not @t695) @t693 @t691 @t689)))
% 0.48/0.91  (assume-push @p461 @t695)
% 0.48/0.91  (assume-push @p462 @t692)
% 0.48/0.91  (assume-push @p463 @t690)
% 0.48/0.91  (step @p444 :rule false_intro :premises (@p368))
% 0.48/0.91  (step @p445 :rule symm :premises (@p385))
% 0.48/0.91  (step @p446 :rule symm :premises (@p422))
% 0.48/0.91  (step @p447 :rule trans :premises (@p446 @p445))
% 0.48/0.91  (step @p448 :rule refl :args (@t674))
% 0.48/0.91  (step @p449 :rule cong :premises (@p448 @p447) :args (@t688))
% 0.48/0.91  (step @p450 :rule trans :premises (@p449 @p444))
% 0.48/0.91  (step @p451 :rule false_elim :premises (@p450))
% 0.48/0.91  (step-pop @p464 :rule scope :premises (@p451))
% 0.48/0.91  (step-pop @p465 :rule scope :premises (@p464))
% 0.48/0.91  (step-pop @p466 :rule scope :premises (@p465))
% 0.48/0.91  (step @p452 :rule process_scope :premises (@p466) :args (@t689))
% 0.48/0.91  (step @p456 :rule implies_elim :premises (@p452))
% 0.48/0.91  (step @p457 :rule cnf_and_neg :args (@t696))
% 0.48/0.91  (step @p458 :rule resolution :premises (@p457 @p456) :args (true @t696))
% 0.48/0.91  (step @p459 :rule eq_resolve :premises (@p458 @p440))
% 0.48/0.91  (step @p460 false :rule chain_m_resolution :premises (@p459 @p435 @p422 @p385 @p368) :args (false (@list false false false true) (@list @t688 @t690 @t692 @t694)))
% 0.48/0.91  )
% 0.48/0.91  % SZS output end Proof
% 0.48/0.91  % cvc5 exiting
%------------------------------------------------------------------------------