cvc5---1.3.4.THM-Prf.s

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

% Computer : n001.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:17 AM UTC 2026

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

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13  % Problem  : ITP177^1 : TPTP v9.2.1. Released v7.5.0.
% 0.11/0.14  % Command  : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.18/0.35  % Computer : n001.cluster.edu
% 0.18/0.35  % Model    : x86_64 x86_64
% 0.18/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.35  % Memory   : 8042.1875MB
% 0.18/0.35  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.18/0.35  % CPULimit : 300
% 0.18/0.35  % WCLimit  : 300
% 0.18/0.35  % DateTime : Tue Jun  2 04:18:35 EDT 2026
% 0.18/0.35  % CPUTime  : 
% 0.39/0.62  %----Proving TH0
% 0.48/0.94  --- 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.94  % SZS status Theorem
% 0.48/0.94  % SZS output start Proof
% 0.48/0.94  (
% 0.48/0.94  (declare-sort tptp.b 0)
% 0.48/0.94  (declare-sort tptp.product_prod_b_b 0)
% 0.48/0.94  (declare-sort tptp.set_b 0)
% 0.48/0.94  (declare-sort tptp.set_Product_prod_b_b 0)
% 0.48/0.94  (declare-sort tptp.set_Pr1987088711_a_nat 0)
% 0.48/0.94  (declare-sort tptp.produc1871334759_a_nat 0)
% 0.48/0.94  (declare-sort tptp.set_Pr924198087_a_nat 0)
% 0.48/0.94  (declare-sort tptp.produc398057191_a_nat 0)
% 0.48/0.94  (declare-sort tptp.set_Pr2106913242_nat_b 0)
% 0.48/0.94  (declare-sort tptp.standard_Constant_a 0)
% 0.48/0.94  (declare-sort tptp.set_Pr1324126435od_b_b 0)
% 0.48/0.94  (declare-sort tptp.set_Pr2007082183od_b_b 0)
% 0.48/0.94  (declare-sort tptp.produc90515391tant_a 0)
% 0.48/0.94  (declare-sort tptp.set_Pr154086431tant_a 0)
% 0.48/0.94  (declare-sort tptp.set_la1083530965_a_nat 0)
% 0.48/0.94  (declare-sort tptp.produc1084374401od_b_b 0)
% 0.48/0.94  (declare-sort tptp.set_Pr1190604087od_b_b 0)
% 0.48/0.94  (declare-sort tptp.produc255402447od_b_b 0)
% 0.48/0.94  (declare-sort tptp.produc845793663_nat_b 0)
% 0.48/0.94  (declare-sort tptp.produc970027067od_b_b 0)
% 0.48/0.94  (declare-sort tptp.produc1213276845od_b_b 0)
% 0.48/0.94  (declare-sort tptp.set_Pr2134561957od_b_b 0)
% 0.48/0.94  (declare-sort tptp.set_Pr1906739389_b_b_b 0)
% 0.48/0.94  (declare-sort tptp.set_Pr1021918435od_b_b 0)
% 0.48/0.94  (declare-sort tptp.produc644633773od_b_b 0)
% 0.48/0.94  (declare-sort tptp.set_Pr357419743_b_b_b 0)
% 0.48/0.94  (declare-sort tptp.labele935650037_a_nat 0)
% 0.48/0.94  (declare-sort tptp.set_St761939237tant_a 0)
% 0.48/0.94  (declare-sort tptp.labele1159362096nt_a_b 0)
% 0.48/0.94  (declare-sort tptp.set_Pr1646010159_a_nat 0)
% 0.48/0.94  (declare-sort tptp.set_Pr2109276827od_b_b 0)
% 0.48/0.94  (declare-sort tptp.allego510293162tant_a 0)
% 0.48/0.94  (declare-sort tptp.labele1644675410od_b_b 0)
% 0.48/0.94  (declare-sort tptp.labele1835558936od_b_b 0)
% 0.48/0.94  (declare-sort tptp.produc1168037607od_b_b 0)
% 0.48/0.94  (declare-sort tptp.produc1485083751od_b_b 0)
% 0.48/0.94  (declare-sort tptp.set_Pr667377223od_b_b 0)
% 0.48/0.94  (declare-sort tptp.produc1990339951od_b_b 0)
% 0.48/0.94  (declare-sort tptp.produc1605346267od_b_b 0)
% 0.48/0.94  (declare-sort tptp.produc2112523263_b_b_b 0)
% 0.48/0.94  (declare-sort tptp.set_Pr621705391od_b_b 0)
% 0.48/0.94  (declare-sort tptp.set_Pr1071216121od_b_b 0)
% 0.48/0.94  (declare-sort tptp.set_Pr812188767_nat_b 0)
% 0.48/0.94  (declare-sort tptp.set_Pr2060523537od_b_b 0)
% 0.48/0.94  (declare-sort tptp.produc1398946881nt_a_b 0)
% 0.48/0.94  (declare-sort tptp.set_Pr1954438265od_b_b 0)
% 0.48/0.94  (declare-sort tptp.produc1052326083od_b_b 0)
% 0.48/0.94  (declare-sort tptp.produc1169496899od_b_b 0)
% 0.48/0.94  (declare-sort tptp.set_Pr1649131859tant_a 0)
% 0.48/0.94  (declare-sort tptp.produc276146823_b_b_b 0)
% 0.48/0.94  (declare-sort tptp.labele1322729112_a_nat 0)
% 0.48/0.94  (declare-sort tptp.set_Pr197580003_a_nat 0)
% 0.48/0.94  (declare-const tptp.member_b (-> tptp.b tptp.set_b Bool))
% 0.48/0.94  (declare-const tptp.getRel904497637nt_a_b (-> tptp.standard_Constant_a tptp.labele1159362096nt_a_b tptp.set_Product_prod_b_b))
% 0.48/0.94  (declare-const tptp.hilbert_Eps_b (-> (-> tptp.b Bool) tptp.b))
% 0.48/0.94  (declare-const tptp.bot_bot_set_b tptp.set_b)
% 0.48/0.94  (declare-const tptp.g tptp.labele1159362096nt_a_b)
% 0.48/0.94  (declare-const tptp.insert_b (-> tptp.b tptp.set_b tptp.set_b))
% 0.48/0.94  (declare-const tptp.standard_S_Idt_a tptp.standard_Constant_a)
% 0.48/0.94  (declare-const tptp.image_b_b (-> tptp.set_Product_prod_b_b tptp.set_b tptp.set_b))
% 0.48/0.94  (declare-const tptp.if_b (-> Bool tptp.b tptp.b tptp.b))
% 0.48/0.94  (declare-const tptp.labele1424214014nt_a_b (-> tptp.labele1159362096nt_a_b tptp.set_b))
% 0.48/0.94  (declare-const tptp.member1285940496od_b_b (-> tptp.product_prod_b_b tptp.set_Product_prod_b_b Bool))
% 0.48/0.94  (declare-const tptp.member1516365892od_b_b (-> tptp.produc1213276845od_b_b tptp.set_Pr1324126435od_b_b Bool))
% 0.48/0.94  (declare-const tptp.image_1683732397od_b_b (-> (-> tptp.b tptp.product_prod_b_b) tptp.set_b tptp.set_Product_prod_b_b))
% 0.48/0.94  (declare-const tptp.standa1795879409tant_a (-> tptp.standard_Constant_a tptp.produc1871334759_a_nat))
% 0.48/0.94  (declare-const tptp.standa997693288tant_a (-> tptp.standard_Constant_a tptp.produc1871334759_a_nat))
% 0.48/0.94  (declare-const tptp.relcom1338300020_a_nat (-> tptp.set_Pr1987088711_a_nat tptp.set_Pr1987088711_a_nat tptp.set_Pr1987088711_a_nat))
% 0.48/0.94  (declare-const tptp.collec357096914_a_nat (-> (-> tptp.produc1871334759_a_nat Bool) tptp.set_Pr1987088711_a_nat))
% 0.48/0.94  (declare-const tptp.ord_le107617383_a_nat (-> tptp.set_Pr924198087_a_nat tptp.set_Pr924198087_a_nat Bool))
% 0.48/0.94  (declare-const tptp.equiv_1125628061od_b_b (-> tptp.set_Product_prod_b_b tptp.set_Pr2007082183od_b_b Bool))
% 0.48/0.94  (declare-const tptp.equiv_291114781_a_nat (-> tptp.set_Pr1987088711_a_nat tptp.set_Pr924198087_a_nat Bool))
% 0.48/0.94  (declare-const tptp.conseq956760372_nat_b (-> tptp.set_Pr1987088711_a_nat tptp.labele1159362096nt_a_b Bool))
% 0.48/0.94  (declare-const tptp.map_gr1495881666tant_a (-> tptp.set_Pr1906739389_b_b_b tptp.labele1644675410od_b_b tptp.labele1159362096nt_a_b))
% 0.48/0.94  (declare-const tptp.mainta374363448_a_b_b (-> tptp.produc1398946881nt_a_b tptp.labele1159362096nt_a_b Bool))
% 0.48/0.94  (declare-const tptp.bot_bo2122869057_a_nat tptp.set_la1083530965_a_nat)
% 0.48/0.94  (declare-const tptp.extens1554515172_nat_b (-> tptp.produc1871334759_a_nat tptp.labele1159362096nt_a_b tptp.set_Pr2106913242_nat_b Bool))
% 0.48/0.94  (declare-const tptp.map_gr1314489926tant_a (-> tptp.set_Pr357419743_b_b_b tptp.labele1835558936od_b_b tptp.labele1159362096nt_a_b))
% 0.48/0.94  (declare-const tptp.semant55076487nt_a_b (-> tptp.labele1159362096nt_a_b tptp.allego510293162tant_a tptp.set_Product_prod_b_b))
% 0.48/0.94  (declare-const tptp.image_532916993od_b_b (-> tptp.set_Pr1071216121od_b_b tptp.set_Product_prod_b_b tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (declare-const tptp.edge_p1817988046tant_a (-> tptp.set_Pr1906739389_b_b_b tptp.set_Pr1190604087od_b_b tptp.set_Pr1324126435od_b_b Bool))
% 0.48/0.94  (declare-const tptp.image_1928024979od_b_b (-> tptp.set_Pr2007082183od_b_b tptp.set_Product_prod_b_b tptp.set_Product_prod_b_b))
% 0.48/0.94  (declare-const tptp.edge_p1384198690tant_a (-> tptp.set_Product_prod_b_b tptp.set_Pr1324126435od_b_b tptp.set_Pr1324126435od_b_b Bool))
% 0.48/0.94  (declare-const tptp.image_984343321od_b_b (-> tptp.set_Pr2060523537od_b_b tptp.set_b tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (declare-const tptp.produc618266719od_b_b (-> tptp.standard_Constant_a tptp.produc1168037607od_b_b tptp.produc644633773od_b_b))
% 0.48/0.94  (declare-const tptp.produc1788032435od_b_b (-> tptp.standard_Constant_a tptp.produc970027067od_b_b tptp.produc1084374401od_b_b))
% 0.48/0.94  (declare-const tptp.edge_p1969196346tant_a (-> tptp.set_Pr357419743_b_b_b tptp.set_Pr1021918435od_b_b tptp.set_Pr1324126435od_b_b Bool))
% 0.48/0.94  (declare-const tptp.image_921732011_b_b_b (-> tptp.set_Pr357419743_b_b_b tptp.set_Product_prod_b_b tptp.set_b))
% 0.48/0.94  (declare-const tptp.standa63370785tant_a (-> tptp.standard_Constant_a tptp.produc1871334759_a_nat))
% 0.48/0.94  (declare-const tptp.labele372159959od_b_b (-> tptp.labele1835558936od_b_b tptp.set_Pr1021918435od_b_b))
% 0.48/0.94  (declare-const tptp.relcom1823941168od_b_b (-> tptp.set_Pr1324126435od_b_b tptp.set_Pr2007082183od_b_b tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (declare-const tptp.id_on_250271696od_b_b (-> tptp.set_Pr1324126435od_b_b tptp.set_Pr2109276827od_b_b))
% 0.48/0.94  (declare-const tptp.id_on_2019020932od_b_b (-> tptp.set_Product_prod_b_b tptp.set_Pr2007082183od_b_b))
% 0.48/0.94  (declare-const tptp.produc732676669od_b_b (-> tptp.product_prod_b_b tptp.produc1213276845od_b_b tptp.produc1052326083od_b_b))
% 0.48/0.94  (declare-const tptp.collec279084418od_b_b (-> (-> tptp.produc1213276845od_b_b Bool) tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (declare-const tptp.bot_bo1836341171_a_nat tptp.set_Pr1987088711_a_nat)
% 0.48/0.94  (declare-const tptp.collec1481886546od_b_b (-> (-> tptp.product_prod_b_b Bool) tptp.set_Product_prod_b_b))
% 0.48/0.94  (declare-const tptp.collect_b (-> (-> tptp.b Bool) tptp.set_b))
% 0.48/0.94  (declare-const tptp.ord_le1718765799_a_nat (-> tptp.set_Pr1987088711_a_nat tptp.set_Pr1987088711_a_nat Bool))
% 0.48/0.94  (declare-const tptp.getRel59882567od_b_b (-> tptp.standard_Constant_a tptp.labele1644675410od_b_b tptp.set_Pr2109276827od_b_b))
% 0.48/0.94  (declare-const tptp.x tptp.b)
% 0.48/0.94  (declare-const tptp.image_1168831379_a_nat (-> tptp.set_Pr924198087_a_nat tptp.set_Pr1987088711_a_nat tptp.set_Pr1987088711_a_nat))
% 0.48/0.94  (declare-const tptp.refl_o1921098222od_b_b (-> tptp.set_Pr1324126435od_b_b tptp.set_Pr2109276827od_b_b Bool))
% 0.48/0.94  (declare-const tptp.labele1741081071nt_a_b (-> tptp.labele1159362096nt_a_b tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (declare-const tptp.member584645392_a_nat (-> tptp.produc398057191_a_nat tptp.set_Pr924198087_a_nat Bool))
% 0.48/0.94  (declare-const tptp.bNF_Gr492676974_b_b_b (-> tptp.set_Pr1324126435od_b_b (-> tptp.produc1213276845od_b_b tptp.b) tptp.set_Pr1906739389_b_b_b))
% 0.48/0.94  (declare-const tptp.produc800495189od_b_b (-> tptp.b tptp.produc1213276845od_b_b tptp.produc1605346267od_b_b))
% 0.48/0.94  (declare-const tptp.l2 tptp.standard_Constant_a)
% 0.48/0.94  (declare-const tptp.extens1779443913_a_b_b (-> tptp.produc1398946881nt_a_b tptp.labele1159362096nt_a_b tptp.set_Product_prod_b_b Bool))
% 0.48/0.94  (declare-const tptp.map_gr926947118tant_a (-> tptp.set_Product_prod_b_b tptp.labele1159362096nt_a_b tptp.labele1159362096nt_a_b))
% 0.48/0.94  (declare-const tptp.image_763305007od_b_b (-> tptp.set_Pr2109276827od_b_b tptp.set_Pr1324126435od_b_b tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (declare-const tptp.equiv_equiv_b (-> tptp.set_b tptp.set_Product_prod_b_b Bool))
% 0.48/0.94  (declare-const tptp.l tptp.set_St761939237tant_a)
% 0.48/0.94  (declare-const tptp.mainta1604381365_nat_b (-> tptp.produc1871334759_a_nat tptp.labele1159362096nt_a_b Bool))
% 0.48/0.94  (declare-const tptp.restri446606278nt_a_b (-> tptp.labele1159362096nt_a_b tptp.labele1159362096nt_a_b))
% 0.48/0.94  (declare-const tptp.id_on_b (-> tptp.set_b tptp.set_Product_prod_b_b))
% 0.48/0.94  (declare-const tptp.refl_on_b (-> tptp.set_b tptp.set_Product_prod_b_b Bool))
% 0.48/0.94  (declare-const tptp.labele1230159100nt_a_b (-> tptp.set_Pr1324126435od_b_b tptp.set_b tptp.labele1159362096nt_a_b))
% 0.48/0.94  (declare-const tptp.graph_714568023_nat_b (-> tptp.labele935650037_a_nat tptp.labele1159362096nt_a_b tptp.set_Pr2106913242_nat_b Bool))
% 0.48/0.94  (declare-const tptp.image_1749766139_a_nat (-> tptp.set_Pr1646010159_a_nat tptp.set_b tptp.set_Pr1987088711_a_nat))
% 0.48/0.94  (declare-const tptp.produc1432590431od_b_b (-> tptp.standard_Constant_a tptp.product_prod_b_b tptp.produc1213276845od_b_b))
% 0.48/0.94  (declare-const tptp.member1086024932od_b_b (-> tptp.produc970027067od_b_b tptp.set_Pr2109276827od_b_b Bool))
% 0.48/0.94  (declare-const tptp.product_Pair_b_b (-> tptp.b tptp.b tptp.product_prod_b_b))
% 0.48/0.94  (declare-const tptp.labele2032816061od_b_b (-> tptp.labele1644675410od_b_b tptp.set_Pr1190604087od_b_b))
% 0.48/0.94  (declare-const tptp.relcom883816262od_b_b (-> tptp.set_Pr154086431tant_a tptp.set_Pr1324126435od_b_b tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (declare-const tptp.standa1568205540ules_a (-> tptp.set_St761939237tant_a tptp.set_Pr1987088711_a_nat))
% 0.48/0.94  (declare-const tptp.y tptp.b)
% 0.48/0.94  (declare-const tptp.produc1676969687_a_nat (-> tptp.labele935650037_a_nat tptp.labele935650037_a_nat tptp.produc1871334759_a_nat))
% 0.48/0.94  (declare-const tptp.image_480774529od_b_b (-> tptp.set_Pr1954438265od_b_b tptp.set_Pr1987088711_a_nat tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (declare-const tptp.produc449289715od_b_b (-> tptp.produc1213276845od_b_b tptp.produc1213276845od_b_b tptp.produc970027067od_b_b))
% 0.48/0.94  (declare-const tptp.graph_1309249505nt_a_b (-> tptp.labele1159362096nt_a_b tptp.labele1159362096nt_a_b tptp.labele1159362096nt_a_b))
% 0.48/0.94  (declare-const tptp.refl_o1031343860_a_nat (-> tptp.set_la1083530965_a_nat tptp.set_Pr1987088711_a_nat Bool))
% 0.48/0.94  (declare-const tptp.member832397200_a_nat (-> tptp.produc1871334759_a_nat tptp.set_Pr1987088711_a_nat Bool))
% 0.48/0.94  (declare-const tptp.produc1569511545nt_a_b (-> tptp.labele1159362096nt_a_b tptp.labele1159362096nt_a_b tptp.produc1398946881nt_a_b))
% 0.48/0.94  (declare-const tptp.graph_222606102_a_b_b (-> tptp.labele1159362096nt_a_b tptp.labele1159362096nt_a_b tptp.set_Product_prod_b_b Bool))
% 0.48/0.94  (declare-const tptp.member1652792080od_b_b (-> tptp.produc1168037607od_b_b tptp.set_Pr2007082183od_b_b Bool))
% 0.48/0.94  (declare-const tptp.labele442485990od_b_b (-> tptp.labele1835558936od_b_b tptp.set_Product_prod_b_b))
% 0.48/0.94  (declare-const tptp.relcomp_b_b_b (-> tptp.set_Product_prod_b_b tptp.set_Product_prod_b_b tptp.set_Product_prod_b_b))
% 0.48/0.94  (declare-const tptp.bNF_Gr521784954_b_b_b (-> tptp.set_Product_prod_b_b (-> tptp.product_prod_b_b tptp.b) tptp.set_Pr357419743_b_b_b))
% 0.48/0.94  (declare-const tptp.bNF_Gr_b_b (-> tptp.set_b (-> tptp.b tptp.b) tptp.set_Product_prod_b_b))
% 0.48/0.94  (declare-const tptp.getRel118493133od_b_b (-> tptp.standard_Constant_a tptp.labele1835558936od_b_b tptp.set_Pr2007082183od_b_b))
% 0.48/0.94  (declare-const tptp.image_1214223635od_b_b (-> tptp.set_Pr667377223od_b_b tptp.set_Pr1987088711_a_nat tptp.set_Product_prod_b_b))
% 0.48/0.94  (declare-const tptp.member147868824od_b_b (-> tptp.produc1084374401od_b_b tptp.set_Pr1190604087od_b_b Bool))
% 0.48/0.94  (declare-const tptp.produc546497367od_b_b (-> tptp.product_prod_b_b tptp.product_prod_b_b tptp.produc1168037607od_b_b))
% 0.48/0.94  (declare-const tptp.refl_o2134473190od_b_b (-> tptp.set_Product_prod_b_b tptp.set_Pr2007082183od_b_b Bool))
% 0.48/0.94  (declare-const tptp.member1632892294tant_a (-> tptp.standard_Constant_a tptp.set_St761939237tant_a Bool))
% 0.48/0.94  (declare-const tptp.labele595103470od_b_b (-> tptp.labele1644675410od_b_b tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (declare-const tptp.relcom112561144od_b_b (-> tptp.set_Pr1649131859tant_a tptp.set_Pr1324126435od_b_b tptp.set_Pr621705391od_b_b))
% 0.48/0.94  (declare-const tptp.member1744485444od_b_b (-> tptp.produc644633773od_b_b tptp.set_Pr1021918435od_b_b Bool))
% 0.48/0.94  (declare-const tptp.image_1177096571od_b_b (-> tptp.set_Pr621705391od_b_b tptp.set_b tptp.set_Product_prod_b_b))
% 0.48/0.94  (declare-const tptp.graph_726202286_nat_b (-> tptp.labele1322729112_a_nat tptp.labele1159362096nt_a_b tptp.set_Pr812188767_nat_b Bool))
% 0.48/0.94  (declare-const tptp.produc1257047359od_b_b (-> tptp.b tptp.product_prod_b_b tptp.produc255402447od_b_b))
% 0.48/0.94  (declare-const tptp.equiv_2048442231od_b_b (-> tptp.set_Pr1324126435od_b_b tptp.set_Pr2109276827od_b_b Bool))
% 0.48/0.94  (declare-const tptp.member641857272od_b_b (-> tptp.produc255402447od_b_b tptp.set_Pr621705391od_b_b Bool))
% 0.48/0.94  (declare-const tptp.equiv_1821124534_set_b (-> tptp.set_Product_prod_b_b (-> tptp.b tptp.set_b) Bool))
% 0.48/0.94  (declare-const tptp.member599505522od_b_b (-> tptp.produc1605346267od_b_b tptp.set_Pr2060523537od_b_b Bool))
% 0.48/0.94  (declare-const tptp.produc1001682799_b_b_b (-> tptp.product_prod_b_b tptp.b tptp.produc2112523263_b_b_b))
% 0.48/0.94  (declare-const tptp.member351494440_b_b_b (-> tptp.produc2112523263_b_b_b tptp.set_Pr357419743_b_b_b Bool))
% 0.48/0.94  (declare-const tptp.image_1764625405_b_b_b (-> tptp.set_Pr1906739389_b_b_b tptp.set_Pr1324126435od_b_b tptp.set_b))
% 0.48/0.94  (declare-const tptp.produc1580777273_b_b_b (-> tptp.produc1213276845od_b_b tptp.b tptp.produc276146823_b_b_b))
% 0.48/0.94  (declare-const tptp.member1417789726_b_b_b (-> tptp.produc276146823_b_b_b tptp.set_Pr1906739389_b_b_b Bool))
% 0.48/0.94  (declare-const tptp.image_1397930469od_b_b (-> tptp.set_Pr2134561957od_b_b tptp.set_Pr1324126435od_b_b tptp.set_Product_prod_b_b))
% 0.48/0.94  (declare-const tptp.produc1597690145od_b_b (-> tptp.produc1213276845od_b_b tptp.product_prod_b_b tptp.produc1990339951od_b_b))
% 0.48/0.94  (declare-const tptp.bNF_Gr1272216980od_b_b (-> tptp.set_St761939237tant_a (-> tptp.standard_Constant_a tptp.product_prod_b_b) tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (declare-const tptp.member942707974od_b_b (-> tptp.produc1990339951od_b_b tptp.set_Pr2134561957od_b_b Bool))
% 0.48/0.94  (declare-const tptp.bNF_Gr996500706_a_nat (-> tptp.set_la1083530965_a_nat (-> tptp.labele935650037_a_nat tptp.labele935650037_a_nat) tptp.set_Pr1987088711_a_nat))
% 0.48/0.94  (declare-const tptp.image_1916422435od_b_b (-> tptp.set_Pr1324126435od_b_b tptp.set_St761939237tant_a tptp.set_Product_prod_b_b))
% 0.48/0.94  (declare-const tptp.image_924992811_nat_b (-> tptp.set_Pr812188767_nat_b tptp.set_Pr1987088711_a_nat tptp.set_b))
% 0.48/0.94  (declare-const tptp.bot_bo1343651123od_b_b tptp.set_Product_prod_b_b)
% 0.48/0.94  (declare-const tptp.image_1971191571_a_nat (-> tptp.set_Pr1987088711_a_nat tptp.set_la1083530965_a_nat tptp.set_la1083530965_a_nat))
% 0.48/0.94  (declare-const tptp.id_on_689842066_a_nat (-> tptp.set_la1083530965_a_nat tptp.set_Pr1987088711_a_nat))
% 0.48/0.94  (declare-const tptp.member4694106od_b_b (-> tptp.produc1052326083od_b_b tptp.set_Pr1071216121od_b_b Bool))
% 0.48/0.94  (declare-const tptp.bNF_Gr230160332tant_a (-> tptp.set_b (-> tptp.b tptp.standard_Constant_a) tptp.set_Pr1649131859tant_a))
% 0.48/0.94  (declare-const tptp.bot_bo1973379891_a_nat tptp.set_Pr924198087_a_nat)
% 0.48/0.94  (declare-const tptp.id_on_1651096324_a_nat (-> tptp.set_Pr1987088711_a_nat tptp.set_Pr924198087_a_nat))
% 0.48/0.94  (declare-const tptp.insert1574423351_a_nat (-> tptp.produc1871334759_a_nat tptp.set_Pr1987088711_a_nat tptp.set_Pr1987088711_a_nat))
% 0.48/0.94  (declare-const tptp.insert1167839429_a_nat (-> tptp.labele935650037_a_nat tptp.set_la1083530965_a_nat tptp.set_la1083530965_a_nat))
% 0.48/0.94  (declare-const tptp.insert1952693431od_b_b (-> tptp.product_prod_b_b tptp.set_Product_prod_b_b tptp.set_Product_prod_b_b))
% 0.48/0.94  (declare-const tptp.insert2037698781od_b_b (-> tptp.produc1213276845od_b_b tptp.set_Pr1324126435od_b_b tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (declare-const tptp.insert1909710879tant_a (-> tptp.standard_Constant_a tptp.set_St761939237tant_a tptp.set_St761939237tant_a))
% 0.48/0.94  (declare-const tptp.bot_bo1160111033tant_a tptp.set_St761939237tant_a)
% 0.48/0.94  (declare-const tptp.produc2059954415_nat_b (-> tptp.produc1871334759_a_nat tptp.b tptp.produc845793663_nat_b))
% 0.48/0.94  (declare-const tptp.member1544800936_nat_b (-> tptp.produc845793663_nat_b tptp.set_Pr812188767_nat_b Bool))
% 0.48/0.94  (declare-const tptp.produc590959831od_b_b (-> tptp.produc1871334759_a_nat tptp.product_prod_b_b tptp.produc1485083751od_b_b))
% 0.48/0.94  (declare-const tptp.member301892752od_b_b (-> tptp.produc1485083751od_b_b tptp.set_Pr667377223od_b_b Bool))
% 0.48/0.94  (declare-const tptp.produc401731773od_b_b (-> tptp.produc1871334759_a_nat tptp.produc1213276845od_b_b tptp.produc1169496899od_b_b))
% 0.48/0.94  (declare-const tptp.member1533761242od_b_b (-> tptp.produc1169496899od_b_b tptp.set_Pr1954438265od_b_b Bool))
% 0.48/0.94  (declare-const tptp.bot_bo1113554635_nat_b tptp.set_Pr812188767_nat_b)
% 0.48/0.94  (declare-const tptp.bot_bo1653310327_a_nat tptp.set_Pr197580003_a_nat)
% 0.48/0.94  (declare-const tptp.labele27098724_a_nat (-> tptp.set_Pr197580003_a_nat tptp.set_Pr1987088711_a_nat tptp.labele1322729112_a_nat))
% 0.48/0.94  (declare-const tptp.refl_o1213627494_a_nat (-> tptp.set_Pr1987088711_a_nat tptp.set_Pr924198087_a_nat Bool))
% 0.48/0.94  (declare-const tptp.bot_bo1664927607od_b_b tptp.set_Pr1324126435od_b_b)
% 0.48/0.94  (declare-const tptp.produc1677124439_a_nat (-> tptp.produc1871334759_a_nat tptp.produc1871334759_a_nat tptp.produc398057191_a_nat))
% 0.48/0.94  (declare-const tptp.insert1810136247_a_nat (-> tptp.produc398057191_a_nat tptp.set_Pr924198087_a_nat tptp.set_Pr924198087_a_nat))
% 0.48/0.94  (declare-const tptp.produc342647tant_a (-> tptp.standard_Constant_a tptp.standard_Constant_a tptp.produc90515391tant_a))
% 0.48/0.94  (declare-const tptp.member1214736488tant_a (-> tptp.produc90515391tant_a tptp.set_Pr154086431tant_a Bool))
% 0.48/0.94  (declare-const tptp.ord_le1484132922_nat_b (-> tptp.set_Pr2106913242_nat_b tptp.set_Pr2106913242_nat_b Bool))
% 0.48/0.94  (define tptp.p () (let ((_let_1 (@var "X5" tptp.b))) (let ((_let_2 (@var "Y4" tptp.b))) (lambda (@list _let_1 _let_2) (_ (_ tptp.member_b _let_2) (_ (_ tptp.image_b_b (_ (_ tptp.getRel904497637nt_a_b tptp.standard_S_Idt_a) tptp.g)) (_ (_ tptp.insert_b _let_1) tptp.bot_bot_set_b)))))))
% 0.48/0.94  (define tptp.f () (let ((_let_1 (@var "X5" tptp.b))) (lambda (@list _let_1) (_ (_ (_ tptp.if_b (= (_ (_ tptp.image_b_b (_ (_ tptp.getRel904497637nt_a_b tptp.standard_S_Idt_a) tptp.g)) (_ (_ tptp.insert_b _let_1) tptp.bot_bot_set_b)) tptp.bot_bot_set_b)) _let_1) (_ tptp.hilbert_Eps_b (_ tptp.p _let_1))))))
% 0.48/0.94  (define tptp.agree_221379389_a_b_b () (let ((_let_1 (@var "X5" tptp.b))) (let ((_let_2 (_ (_ tptp.insert_b _let_1) tptp.bot_bot_set_b))) (let ((_let_3 (@var "F_2" tptp.set_Product_prod_b_b))) (let ((_let_4 (@var "F_1" tptp.set_Product_prod_b_b))) (let ((_let_5 (@var "G4" tptp.labele1159362096nt_a_b))) (lambda (@list _let_5 _let_4 _let_3) (forall (@list _let_1) (=> (_ (_ tptp.member_b _let_1) (_ tptp.labele1424214014nt_a_b _let_5)) (= (_ (_ tptp.image_b_b _let_4) _let_2) (_ (_ tptp.image_b_b _let_3) _let_2)))))))))))
% 0.48/0.94  (define tptp.ord_less_eq_set_b () (let ((_let_1 (@var "B7" tptp.set_b))) (let ((_let_2 (@var "T" tptp.b))) (let ((_let_3 (_ tptp.member_b _let_2))) (let ((_let_4 (@var "A7" tptp.set_b))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1)))))))))
% 0.48/0.94  (define tptp.ord_le1036320359od_b_b () (let ((_let_1 (@var "B7" tptp.set_Product_prod_b_b))) (let ((_let_2 (@var "T" tptp.product_prod_b_b))) (let ((_let_3 (_ tptp.member1285940496od_b_b _let_2))) (let ((_let_4 (@var "A7" tptp.set_Product_prod_b_b))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1)))))))))
% 0.48/0.94  (define tptp.ord_le123089219od_b_b () (let ((_let_1 (@var "B7" tptp.set_Pr1324126435od_b_b))) (let ((_let_2 (@var "T" tptp.produc1213276845od_b_b))) (let ((_let_3 (_ tptp.member1516365892od_b_b _let_2))) (let ((_let_4 (@var "A7" tptp.set_Pr1324126435od_b_b))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1)))))))))
% 0.48/0.94  (define @t1 () (_ tptp.labele1424214014nt_a_b tptp.g))
% 0.48/0.94  (define @t2 () (@var "Xa" tptp.b))
% 0.48/0.94  (define @t3 () (_ tptp.f tptp.y))
% 0.48/0.94  (define @t4 () (_ tptp.f tptp.x))
% 0.48/0.94  (define @t5 () (@var "X" tptp.b))
% 0.48/0.94  (define @t6 () (_ tptp.f @t5))
% 0.48/0.94  (define @t7 () (_ tptp.member_b @t5))
% 0.48/0.94  (define @t8 () (_ @t7 @t1))
% 0.48/0.94  (define @t9 () (@list @t5))
% 0.48/0.94  (define @t10 () (_ tptp.p @t5))
% 0.48/0.94  (define @t11 () (@var "X2" tptp.produc1871334759_a_nat))
% 0.48/0.94  (define @t12 () (_ (_ tptp.mainta1604381365_nat_b @t11) tptp.g))
% 0.48/0.94  (define @t13 () (_ tptp.member832397200_a_nat @t11))
% 0.48/0.94  (define @t14 () (@list @t11))
% 0.48/0.94  (define @t15 () (_ (_ tptp.product_Pair_b_b @t4) @t3))
% 0.48/0.94  (define @t16 () (_ tptp.labele1741081071nt_a_b tptp.g))
% 0.48/0.94  (define @t17 () (_ tptp.getRel904497637nt_a_b tptp.standard_S_Idt_a))
% 0.48/0.94  (define @t18 () (_ @t17 tptp.g))
% 0.48/0.94  (define @t19 () (_ (_ tptp.map_gr926947118tant_a (_ (_ tptp.bNF_Gr_b_b @t1) tptp.f)) tptp.g))
% 0.48/0.94  (define @t20 () (@var "Y" tptp.b))
% 0.48/0.94  (define @t21 () (@var "L" tptp.standard_Constant_a))
% 0.48/0.94  (define @t22 () (_ tptp.produc1432590431od_b_b @t21))
% 0.48/0.94  (define @t23 () (_ tptp.member_b @t20))
% 0.48/0.94  (define @t24 () (_ tptp.product_Pair_b_b @t5))
% 0.48/0.94  (define @t25 () (_ @t24 @t20))
% 0.48/0.94  (define @t26 () (_ @t24 @t5))
% 0.48/0.94  (define @t27 () (@var "X22" tptp.set_b))
% 0.48/0.94  (define @t28 () (@var "X1" tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (define @t29 () (_ (_ tptp.labele1230159100nt_a_b @t28) @t27))
% 0.48/0.94  (define @t30 () (@list @t28 @t27))
% 0.48/0.94  (define @t31 () (_ tptp.labele1424214014nt_a_b @t19))
% 0.48/0.94  (define @t32 () (@var "G" tptp.labele1159362096nt_a_b))
% 0.48/0.94  (define @t33 () (_ tptp.labele1424214014nt_a_b @t32))
% 0.48/0.94  (define @t34 () (_ tptp.restri446606278nt_a_b @t32))
% 0.48/0.94  (define @t35 () (@list @t32))
% 0.48/0.94  (define @t36 () (@var "X" tptp.labele1159362096nt_a_b))
% 0.48/0.94  (define @t37 () (_ tptp.restri446606278nt_a_b @t36))
% 0.48/0.94  (define @t38 () (@var "A" tptp.labele1159362096nt_a_b))
% 0.48/0.94  (define @t39 () (@var "B" tptp.labele1159362096nt_a_b))
% 0.48/0.94  (define @t40 () (_ (_ tptp.graph_1309249505nt_a_b @t39) @t38))
% 0.48/0.94  (define @t41 () (_ tptp.graph_1309249505nt_a_b @t38))
% 0.48/0.94  (define @t42 () (@list @t38 @t39))
% 0.48/0.94  (define @t43 () (_ @t41 @t39))
% 0.48/0.94  (define @t44 () (@var "F" tptp.set_Product_prod_b_b))
% 0.48/0.94  (define @t45 () (_ tptp.map_gr926947118tant_a @t44))
% 0.48/0.94  (define @t46 () (_ @t45 @t32))
% 0.48/0.94  (define @t47 () (= @t32 @t34))
% 0.48/0.94  (define @t48 () (@list @t32 @t44))
% 0.48/0.94  (define @t49 () (@var "G_2" tptp.labele1159362096nt_a_b))
% 0.48/0.94  (define @t50 () (@var "G_1" tptp.labele1159362096nt_a_b))
% 0.48/0.94  (define @t51 () (_ (_ tptp.graph_1309249505nt_a_b @t50) @t49))
% 0.48/0.94  (define @t52 () (= @t49 (_ tptp.restri446606278nt_a_b @t49)))
% 0.48/0.94  (define @t53 () (_ tptp.restri446606278nt_a_b @t50))
% 0.48/0.94  (define @t54 () (= @t50 @t53))
% 0.48/0.94  (define @t55 () (@list @t50 @t49))
% 0.48/0.94  (define @t56 () (@var "Labeled_graph" tptp.labele1159362096nt_a_b))
% 0.48/0.94  (define @t57 () (_ tptp.labele1424214014nt_a_b @t56))
% 0.48/0.94  (define @t58 () (_ tptp.labele1741081071nt_a_b @t56))
% 0.48/0.94  (define @t59 () (_ (_ tptp.labele1230159100nt_a_b @t58) @t57))
% 0.48/0.94  (define @t60 () (@list @t56))
% 0.48/0.94  (define @t61 () (_ tptp.id_on_b @t33))
% 0.48/0.94  (define @t62 () (_ tptp.graph_222606102_a_b_b @t32))
% 0.48/0.94  (define @t63 () (@var "A2" tptp.labele1159362096nt_a_b))
% 0.48/0.94  (define @t64 () (_ tptp.id_on_b (_ tptp.labele1424214014nt_a_b @t63)))
% 0.48/0.94  (define @t65 () (_ tptp.restri446606278nt_a_b @t63))
% 0.48/0.94  (define @t66 () (_ @t45 @t38))
% 0.48/0.94  (define @t67 () (_ tptp.labele1424214014nt_a_b @t38))
% 0.48/0.94  (define @t68 () (_ tptp.id_on_b @t67))
% 0.48/0.94  (define @t69 () (_ tptp.graph_222606102_a_b_b @t38))
% 0.48/0.94  (define @t70 () (_ @t69 @t39))
% 0.48/0.94  (define @t71 () (_ @t70 @t68))
% 0.48/0.94  (define @t72 () (@var "X3" tptp.labele1159362096nt_a_b))
% 0.48/0.94  (define @t73 () (_ tptp.labele1424214014nt_a_b @t72))
% 0.48/0.94  (define @t74 () (@var "F" (-> tptp.b tptp.b)))
% 0.48/0.94  (define @t75 () (_ tptp.bNF_Gr_b_b @t33))
% 0.48/0.94  (define @t76 () (_ @t75 @t74))
% 0.48/0.94  (define @t77 () (_ (_ tptp.map_gr926947118tant_a @t76) @t32))
% 0.48/0.94  (define @t78 () (@list @t32 @t74))
% 0.48/0.94  (define @t79 () (= @t51 @t49))
% 0.48/0.94  (define @t80 () (_ tptp.labele1424214014nt_a_b @t50))
% 0.48/0.94  (define @t81 () (_ tptp.id_on_b @t80))
% 0.48/0.94  (define @t82 () (_ tptp.graph_222606102_a_b_b @t50))
% 0.48/0.94  (define @t83 () (_ (_ @t82 @t49) @t81))
% 0.48/0.94  (define @t84 () (@var "G_3" tptp.labele1159362096nt_a_b))
% 0.48/0.94  (define @t85 () (_ tptp.labele1424214014nt_a_b @t49))
% 0.48/0.94  (define @t86 () (@var "G2" (-> tptp.b tptp.b)))
% 0.48/0.94  (define @t87 () (@var "X4" tptp.b))
% 0.48/0.94  (define @t88 () (_ @t74 @t87))
% 0.48/0.94  (define @t89 () (_ tptp.member_b @t87))
% 0.48/0.94  (define @t90 () (@list @t87))
% 0.48/0.94  (define @t91 () (@var "H" tptp.set_Product_prod_b_b))
% 0.48/0.94  (define @t92 () (_ tptp.graph_222606102_a_b_b @t72))
% 0.48/0.94  (define @t93 () (@var "Labeled_graph2" tptp.labele1159362096nt_a_b))
% 0.48/0.94  (define @t94 () (@var "G" tptp.labele1835558936od_b_b))
% 0.48/0.94  (define @t95 () (@var "F" (-> tptp.product_prod_b_b tptp.b)))
% 0.48/0.94  (define @t96 () (_ tptp.labele442485990od_b_b @t94))
% 0.48/0.94  (define @t97 () (_ tptp.getRel904497637nt_a_b @t21))
% 0.48/0.94  (define @t98 () (_ @t97 (_ (_ tptp.map_gr1314489926tant_a (_ (_ tptp.bNF_Gr521784954_b_b_b @t96) @t95)) @t94)))
% 0.48/0.94  (define @t99 () (@var "Z" tptp.product_prod_b_b))
% 0.48/0.94  (define @t100 () (@var "Y" tptp.product_prod_b_b))
% 0.48/0.94  (define @t101 () (_ tptp.member1285940496od_b_b @t100))
% 0.48/0.94  (define @t102 () (_ (_ tptp.getRel118493133od_b_b @t21) @t94))
% 0.48/0.94  (define @t103 () (@var "G" tptp.labele1644675410od_b_b))
% 0.48/0.94  (define @t104 () (@var "F" (-> tptp.produc1213276845od_b_b tptp.b)))
% 0.48/0.94  (define @t105 () (_ tptp.labele595103470od_b_b @t103))
% 0.48/0.94  (define @t106 () (_ @t97 (_ (_ tptp.map_gr1495881666tant_a (_ (_ tptp.bNF_Gr492676974_b_b_b @t105) @t104)) @t103)))
% 0.48/0.94  (define @t107 () (@var "Z" tptp.produc1213276845od_b_b))
% 0.48/0.94  (define @t108 () (@var "Y" tptp.produc1213276845od_b_b))
% 0.48/0.94  (define @t109 () (_ tptp.member1516365892od_b_b @t108))
% 0.48/0.94  (define @t110 () (_ (_ tptp.getRel59882567od_b_b @t21) @t103))
% 0.48/0.94  (define @t111 () (_ @t97 @t77))
% 0.48/0.94  (define @t112 () (@var "Z" tptp.b))
% 0.48/0.94  (define @t113 () (_ @t97 @t32))
% 0.48/0.94  (define @t114 () (_ tptp.product_Pair_b_b @t20))
% 0.48/0.94  (define @t115 () (_ tptp.member1285940496od_b_b (_ @t114 @t112)))
% 0.48/0.94  (define @t116 () (_ @t115 @t113))
% 0.48/0.94  (define @t117 () (@var "B3" tptp.b))
% 0.48/0.94  (define @t118 () (@var "A2" tptp.b))
% 0.48/0.94  (define @t119 () (_ tptp.product_Pair_b_b @t118))
% 0.48/0.94  (define @t120 () (_ @t119 @t117))
% 0.48/0.94  (define @t121 () (_ tptp.member1285940496od_b_b @t120))
% 0.48/0.94  (define @t122 () (@var "B2" tptp.product_prod_b_b))
% 0.48/0.94  (define @t123 () (@var "A22" tptp.product_prod_b_b))
% 0.48/0.94  (define @t124 () (@var "B2" tptp.produc1213276845od_b_b))
% 0.48/0.94  (define @t125 () (@var "A22" tptp.produc1213276845od_b_b))
% 0.48/0.94  (define @t126 () (@var "B2" tptp.b))
% 0.48/0.94  (define @t127 () (@var "A22" tptp.b))
% 0.48/0.94  (define @t128 () (_ tptp.hilbert_Eps_b @t10))
% 0.48/0.94  (define @t129 () (@list @t5 @t20))
% 0.48/0.94  (define @t130 () (@var "P" (-> tptp.b Bool)))
% 0.48/0.94  (define @t131 () (_ tptp.collect_b @t130))
% 0.48/0.94  (define @t132 () (_ tptp.member_b @t118))
% 0.48/0.94  (define @t133 () (@var "A2" tptp.product_prod_b_b))
% 0.48/0.94  (define @t134 () (@var "P" (-> tptp.product_prod_b_b Bool)))
% 0.48/0.94  (define @t135 () (_ tptp.member1285940496od_b_b @t133))
% 0.48/0.94  (define @t136 () (@var "A2" tptp.produc1213276845od_b_b))
% 0.48/0.94  (define @t137 () (@var "P" (-> tptp.produc1213276845od_b_b Bool)))
% 0.48/0.94  (define @t138 () (_ tptp.member1516365892od_b_b @t136))
% 0.48/0.94  (define @t139 () (@var "A" tptp.set_b))
% 0.48/0.94  (define @t140 () (@var "X5" tptp.b))
% 0.48/0.94  (define @t141 () (_ tptp.member_b @t140))
% 0.48/0.94  (define @t142 () (_ @t141 @t139))
% 0.48/0.94  (define @t143 () (@list @t140))
% 0.48/0.94  (define @t144 () (@list @t139))
% 0.48/0.94  (define @t145 () (@var "A" tptp.set_Product_prod_b_b))
% 0.48/0.94  (define @t146 () (@var "X5" tptp.product_prod_b_b))
% 0.48/0.94  (define @t147 () (_ tptp.member1285940496od_b_b @t146))
% 0.48/0.94  (define @t148 () (_ @t147 @t145))
% 0.48/0.94  (define @t149 () (@list @t146))
% 0.48/0.94  (define @t150 () (@list @t145))
% 0.48/0.94  (define @t151 () (@var "A" tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (define @t152 () (@var "X5" tptp.produc1213276845od_b_b))
% 0.48/0.94  (define @t153 () (_ tptp.member1516365892od_b_b @t152))
% 0.48/0.94  (define @t154 () (_ @t153 @t151))
% 0.48/0.94  (define @t155 () (@list @t152))
% 0.48/0.94  (define @t156 () (@list @t151))
% 0.48/0.94  (define @t157 () (@var "G3" tptp.labele1159362096nt_a_b))
% 0.48/0.94  (define @t158 () (_ @t74 @t5))
% 0.48/0.94  (define @t159 () (= @t158 @t20))
% 0.48/0.94  (define @t160 () (_ @t7 @t139))
% 0.48/0.94  (define @t161 () (_ (_ tptp.bNF_Gr_b_b @t139) @t74))
% 0.48/0.94  (define @t162 () (_ tptp.member1285940496od_b_b @t25))
% 0.48/0.94  (define @t163 () (@var "X" tptp.standard_Constant_a))
% 0.48/0.94  (define @t164 () (@var "F" (-> tptp.standard_Constant_a tptp.product_prod_b_b)))
% 0.48/0.94  (define @t165 () (_ @t164 @t163))
% 0.48/0.94  (define @t166 () (= @t165 @t100))
% 0.48/0.94  (define @t167 () (@var "A" tptp.set_St761939237tant_a))
% 0.48/0.94  (define @t168 () (_ tptp.member1632892294tant_a @t163))
% 0.48/0.94  (define @t169 () (_ @t168 @t167))
% 0.48/0.94  (define @t170 () (_ (_ tptp.bNF_Gr1272216980od_b_b @t167) @t164))
% 0.48/0.94  (define @t171 () (_ tptp.produc1432590431od_b_b @t163))
% 0.48/0.94  (define @t172 () (_ tptp.member1516365892od_b_b (_ @t171 @t100)))
% 0.48/0.94  (define @t173 () (@var "F2" tptp.set_b))
% 0.48/0.94  (define @t174 () (_ (_ tptp.bNF_Gr_b_b @t173) @t74))
% 0.48/0.94  (define @t175 () (@var "F2" tptp.set_St761939237tant_a))
% 0.48/0.94  (define @t176 () (_ (_ tptp.bNF_Gr1272216980od_b_b @t175) @t164))
% 0.48/0.94  (define @t177 () (_ tptp.id_on_2019020932od_b_b @t145))
% 0.48/0.94  (define @t178 () (_ tptp.produc546497367od_b_b @t133))
% 0.48/0.94  (define @t179 () (_ tptp.member1652792080od_b_b (_ @t178 @t133)))
% 0.48/0.94  (define @t180 () (_ @t135 @t145))
% 0.48/0.94  (define @t181 () (@list @t133 @t145))
% 0.48/0.94  (define @t182 () (_ tptp.id_on_250271696od_b_b @t151))
% 0.48/0.94  (define @t183 () (_ tptp.produc449289715od_b_b @t136))
% 0.48/0.94  (define @t184 () (_ tptp.member1086024932od_b_b (_ @t183 @t136)))
% 0.48/0.94  (define @t185 () (_ @t138 @t151))
% 0.48/0.94  (define @t186 () (@list @t136 @t151))
% 0.48/0.94  (define @t187 () (_ tptp.id_on_b @t139))
% 0.48/0.94  (define @t188 () (_ tptp.member1285940496od_b_b (_ @t119 @t118)))
% 0.48/0.94  (define @t189 () (_ @t132 @t139))
% 0.48/0.94  (define @t190 () (@list @t118 @t139))
% 0.48/0.94  (define @t191 () (_ tptp.member_b @t117))
% 0.48/0.94  (define @t192 () (_ @t121 @t113))
% 0.48/0.94  (define @t193 () (@list @t32 @t118 @t117 @t21))
% 0.48/0.94  (define @t194 () (@var "X" tptp.product_prod_b_b))
% 0.48/0.94  (define @t195 () (_ tptp.member1285940496od_b_b @t194))
% 0.48/0.94  (define @t196 () (_ @t195 @t145))
% 0.48/0.94  (define @t197 () (_ tptp.member1652792080od_b_b (_ (_ tptp.produc546497367od_b_b @t194) @t100)))
% 0.48/0.94  (define @t198 () (@var "X" tptp.produc1213276845od_b_b))
% 0.48/0.94  (define @t199 () (_ tptp.member1516365892od_b_b @t198))
% 0.48/0.94  (define @t200 () (_ @t199 @t151))
% 0.48/0.94  (define @t201 () (_ tptp.member1086024932od_b_b (_ (_ tptp.produc449289715od_b_b @t198) @t108)))
% 0.48/0.94  (define @t202 () (@list @t5 @t20 @t139))
% 0.48/0.94  (define @t203 () (@var "B3" tptp.product_prod_b_b))
% 0.48/0.94  (define @t204 () (_ tptp.member1652792080od_b_b (_ @t178 @t203)))
% 0.48/0.94  (define @t205 () (= @t133 @t203))
% 0.48/0.94  (define @t206 () (@list @t133 @t203 @t145))
% 0.48/0.94  (define @t207 () (@var "B3" tptp.produc1213276845od_b_b))
% 0.48/0.94  (define @t208 () (_ tptp.member1086024932od_b_b (_ @t183 @t207)))
% 0.48/0.94  (define @t209 () (= @t136 @t207))
% 0.48/0.94  (define @t210 () (@list @t136 @t207 @t151))
% 0.48/0.94  (define @t211 () (= @t118 @t117))
% 0.48/0.94  (define @t212 () (@list @t118 @t117 @t139))
% 0.48/0.94  (define @t213 () (@var "X4" tptp.product_prod_b_b))
% 0.48/0.94  (define @t214 () (_ tptp.produc546497367od_b_b @t213))
% 0.48/0.94  (define @t215 () (@var "C" tptp.produc1168037607od_b_b))
% 0.48/0.94  (define @t216 () (_ tptp.member1285940496od_b_b @t213))
% 0.48/0.94  (define @t217 () (_ @t216 @t145))
% 0.48/0.94  (define @t218 () (@list @t213))
% 0.48/0.94  (define @t219 () (@var "X4" tptp.produc1213276845od_b_b))
% 0.48/0.94  (define @t220 () (_ tptp.produc449289715od_b_b @t219))
% 0.48/0.94  (define @t221 () (@var "C" tptp.produc970027067od_b_b))
% 0.48/0.94  (define @t222 () (_ tptp.member1516365892od_b_b @t219))
% 0.48/0.94  (define @t223 () (_ @t222 @t151))
% 0.48/0.94  (define @t224 () (@list @t219))
% 0.48/0.94  (define @t225 () (_ tptp.product_Pair_b_b @t87))
% 0.48/0.94  (define @t226 () (@var "C" tptp.product_prod_b_b))
% 0.48/0.94  (define @t227 () (_ @t89 @t139))
% 0.48/0.94  (define @t228 () (_ tptp.member1285940496od_b_b @t226))
% 0.48/0.94  (define @t229 () (@var "R" tptp.set_Pr2007082183od_b_b))
% 0.48/0.94  (define @t230 () (_ @t197 @t229))
% 0.48/0.94  (define @t231 () (_ (_ tptp.refl_o2134473190od_b_b @t145) @t229))
% 0.48/0.94  (define @t232 () (@list @t145 @t229 @t194 @t100))
% 0.48/0.94  (define @t233 () (@var "R" tptp.set_Pr2109276827od_b_b))
% 0.48/0.94  (define @t234 () (_ @t201 @t233))
% 0.48/0.94  (define @t235 () (_ (_ tptp.refl_o1921098222od_b_b @t151) @t233))
% 0.48/0.94  (define @t236 () (@list @t151 @t233 @t198 @t108))
% 0.48/0.94  (define @t237 () (@var "R" tptp.set_Product_prod_b_b))
% 0.48/0.94  (define @t238 () (_ @t162 @t237))
% 0.48/0.94  (define @t239 () (_ tptp.refl_on_b @t139))
% 0.48/0.94  (define @t240 () (_ @t239 @t237))
% 0.48/0.94  (define @t241 () (@list @t139 @t237 @t5 @t20))
% 0.48/0.94  (define @t242 () (@var "V" tptp.b))
% 0.48/0.94  (define @t243 () (@var "U" tptp.b))
% 0.48/0.94  (define @t244 () (@var "R2" tptp.labele935650037_a_nat))
% 0.48/0.94  (define @t245 () (@var "Y2" tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (define @t246 () (@var "X3" tptp.labele1835558936od_b_b))
% 0.48/0.94  (define @t247 () (_ tptp.labele372159959od_b_b @t246))
% 0.48/0.94  (define @t248 () (_ tptp.labele442485990od_b_b @t246))
% 0.48/0.94  (define @t249 () (@var "Y3" tptp.product_prod_b_b))
% 0.48/0.94  (define @t250 () (@var "L2" tptp.standard_Constant_a))
% 0.48/0.94  (define @t251 () (_ tptp.produc1432590431od_b_b @t250))
% 0.48/0.94  (define @t252 () (_ tptp.member1285940496od_b_b @t249))
% 0.48/0.94  (define @t253 () (@var "X3" tptp.labele1644675410od_b_b))
% 0.48/0.94  (define @t254 () (_ tptp.labele2032816061od_b_b @t253))
% 0.48/0.94  (define @t255 () (_ tptp.labele595103470od_b_b @t253))
% 0.48/0.94  (define @t256 () (@var "Y3" tptp.produc1213276845od_b_b))
% 0.48/0.94  (define @t257 () (_ tptp.member1516365892od_b_b @t256))
% 0.48/0.94  (define @t258 () (_ tptp.labele1741081071nt_a_b @t72))
% 0.48/0.94  (define @t259 () (@var "Y3" tptp.b))
% 0.48/0.94  (define @t260 () (_ tptp.member_b @t259))
% 0.48/0.94  (define @t261 () (_ @t225 @t259))
% 0.48/0.94  (define @t262 () (@var "B4" tptp.b))
% 0.48/0.94  (define @t263 () (= @t117 @t262))
% 0.48/0.94  (define @t264 () (@var "A3" tptp.b))
% 0.48/0.94  (define @t265 () (= @t118 @t264))
% 0.48/0.94  (define @t266 () (_ (_ tptp.product_Pair_b_b @t264) @t262))
% 0.48/0.94  (define @t267 () (= @t120 @t266))
% 0.48/0.94  (define @t268 () (@list @t118 @t117 @t264 @t262))
% 0.48/0.94  (define @t269 () (@var "B4" tptp.product_prod_b_b))
% 0.48/0.94  (define @t270 () (= @t203 @t269))
% 0.48/0.94  (define @t271 () (@var "A3" tptp.standard_Constant_a))
% 0.48/0.94  (define @t272 () (@var "A2" tptp.standard_Constant_a))
% 0.48/0.94  (define @t273 () (= @t272 @t271))
% 0.48/0.94  (define @t274 () (_ tptp.produc1432590431od_b_b @t272))
% 0.48/0.94  (define @t275 () (_ @t274 @t203))
% 0.48/0.94  (define @t276 () (= @t275 (_ (_ tptp.produc1432590431od_b_b @t271) @t269)))
% 0.48/0.94  (define @t277 () (@list @t272 @t203 @t271 @t269))
% 0.48/0.94  (define @t278 () (@var "Y22" tptp.b))
% 0.48/0.94  (define @t279 () (@var "X22" tptp.b))
% 0.48/0.94  (define @t280 () (@var "Y1" tptp.b))
% 0.48/0.94  (define @t281 () (@var "X1" tptp.b))
% 0.48/0.94  (define @t282 () (_ (_ tptp.product_Pair_b_b @t281) @t279))
% 0.48/0.94  (define @t283 () (@var "Y22" tptp.product_prod_b_b))
% 0.48/0.94  (define @t284 () (@var "X22" tptp.product_prod_b_b))
% 0.48/0.94  (define @t285 () (@var "Y1" tptp.standard_Constant_a))
% 0.48/0.94  (define @t286 () (@var "X1" tptp.standard_Constant_a))
% 0.48/0.94  (define @t287 () (_ (_ tptp.produc1432590431od_b_b @t286) @t284))
% 0.48/0.94  (define @t288 () (_ tptp.member1285940496od_b_b @t203))
% 0.48/0.94  (define @t289 () (_ @t288 @t145))
% 0.48/0.94  (define @t290 () (_ @t204 @t229))
% 0.48/0.94  (define @t291 () (_ tptp.member1516365892od_b_b @t207))
% 0.48/0.94  (define @t292 () (_ @t291 @t151))
% 0.48/0.94  (define @t293 () (_ @t208 @t233))
% 0.48/0.94  (define @t294 () (_ @t191 @t139))
% 0.48/0.94  (define @t295 () (_ @t121 @t237))
% 0.48/0.94  (define @t296 () (@list @t139 @t237 @t118 @t117))
% 0.48/0.94  (define @t297 () (@var "Fx" tptp.b))
% 0.48/0.94  (define @t298 () (_ (_ tptp.member1285940496od_b_b (_ @t24 @t297)) @t161))
% 0.48/0.94  (define @t299 () (@list @t5 @t297 @t139 @t74))
% 0.48/0.94  (define @t300 () (@var "Fx" tptp.product_prod_b_b))
% 0.48/0.94  (define @t301 () (_ (_ tptp.member1516365892od_b_b (_ @t171 @t300)) @t170))
% 0.48/0.94  (define @t302 () (@list @t163 @t300 @t167 @t164))
% 0.48/0.94  (define @t303 () (_ tptp.labele1741081071nt_a_b @t32))
% 0.48/0.94  (define @t304 () (@list @t44 @t32))
% 0.48/0.94  (define @t305 () (@var "E2" tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (define @t306 () (@var "V22" tptp.b))
% 0.48/0.94  (define @t307 () (@var "V12" tptp.b))
% 0.48/0.94  (define @t308 () (@var "K" tptp.standard_Constant_a))
% 0.48/0.94  (define @t309 () (_ tptp.produc1432590431od_b_b @t308))
% 0.48/0.94  (define @t310 () (@var "E1" tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (define @t311 () (@var "V2" tptp.b))
% 0.48/0.94  (define @t312 () (@var "V1" tptp.b))
% 0.48/0.94  (define @t313 () (_ tptp.product_Pair_b_b @t312))
% 0.48/0.94  (define @t314 () (@var "H1" tptp.set_Product_prod_b_b))
% 0.48/0.94  (define @t315 () (@var "P2" tptp.product_prod_b_b))
% 0.48/0.94  (define @t316 () (@list @t87 @t259))
% 0.48/0.94  (define @t317 () (@var "X4" tptp.standard_Constant_a))
% 0.48/0.94  (define @t318 () (_ tptp.produc1432590431od_b_b @t317))
% 0.48/0.94  (define @t319 () (_ @t318 @t249))
% 0.48/0.94  (define @t320 () (@var "P2" tptp.produc1213276845od_b_b))
% 0.48/0.94  (define @t321 () (@list @t317 @t249))
% 0.48/0.94  (define @t322 () (@var "B5" tptp.b))
% 0.48/0.94  (define @t323 () (@var "A4" tptp.b))
% 0.48/0.94  (define @t324 () (_ (_ tptp.product_Pair_b_b @t323) @t322))
% 0.48/0.94  (define @t325 () (@list @t323 @t322))
% 0.48/0.94  (define @t326 () (forall @t325 (_ @t134 @t324)))
% 0.48/0.94  (define @t327 () (@var "B5" tptp.product_prod_b_b))
% 0.48/0.94  (define @t328 () (@var "A4" tptp.standard_Constant_a))
% 0.48/0.94  (define @t329 () (_ tptp.produc1432590431od_b_b @t328))
% 0.48/0.94  (define @t330 () (_ @t329 @t327))
% 0.48/0.94  (define @t331 () (@list @t328 @t327))
% 0.48/0.94  (define @t332 () (forall @t331 (_ @t137 @t330)))
% 0.48/0.94  (define @t333 () (@list @t108))
% 0.48/0.94  (define @t334 () (@var "Prod" tptp.product_prod_b_b))
% 0.48/0.94  (define @t335 () (@var "Prod" tptp.produc1213276845od_b_b))
% 0.48/0.94  (define @t336 () (@var "C2" tptp.b))
% 0.48/0.94  (define @t337 () (_ tptp.product_Pair_b_b @t322))
% 0.48/0.94  (define @t338 () (_ @t337 @t336))
% 0.48/0.94  (define @t339 () (_ @t329 @t338))
% 0.48/0.94  (define @t340 () (@list @t328 @t322 @t336))
% 0.48/0.94  (define @t341 () (@var "E" tptp.allego510293162tant_a))
% 0.48/0.94  (define @t342 () (@var "B" tptp.labele935650037_a_nat))
% 0.48/0.94  (define @t343 () (@var "A" tptp.labele935650037_a_nat))
% 0.48/0.94  (define @t344 () (_ (_ tptp.produc1676969687_a_nat @t343) @t342))
% 0.48/0.94  (define @t345 () (_ (_ tptp.mainta1604381365_nat_b @t344) @t32))
% 0.48/0.94  (define @t346 () (@var "F3" tptp.set_Pr2106913242_nat_b))
% 0.48/0.94  (define @t347 () (_ (_ tptp.extens1554515172_nat_b @t344) @t32))
% 0.48/0.94  (define @t348 () (_ (_ tptp.graph_714568023_nat_b @t343) @t32))
% 0.48/0.94  (define @t349 () (_ (_ tptp.produc1569511545nt_a_b @t38) @t39))
% 0.48/0.94  (define @t350 () (_ (_ tptp.mainta374363448_a_b_b @t349) @t32))
% 0.48/0.94  (define @t351 () (@var "F3" tptp.set_Product_prod_b_b))
% 0.48/0.94  (define @t352 () (_ (_ tptp.extens1779443913_a_b_b @t349) @t32))
% 0.48/0.94  (define @t353 () (_ @t69 @t32))
% 0.48/0.94  (define @t354 () (@var "V" tptp.set_b))
% 0.48/0.94  (define @t355 () (@var "E_2" tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (define @t356 () (_ (_ tptp.labele1230159100nt_a_b @t355) @t354))
% 0.48/0.94  (define @t357 () (@var "E_1" tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (define @t358 () (_ (_ tptp.labele1230159100nt_a_b @t357) @t354))
% 0.48/0.94  (define @t359 () (@var "R2" tptp.labele1159362096nt_a_b))
% 0.48/0.94  (define @t360 () (_ (_ tptp.semant55076487nt_a_b @t39) @t341))
% 0.48/0.94  (define @t361 () (_ tptp.product_Pair_b_b @t117))
% 0.48/0.94  (define @t362 () (_ (_ tptp.semant55076487nt_a_b @t38) @t341))
% 0.48/0.94  (define @t363 () (_ @t121 @t362))
% 0.48/0.94  (define @t364 () (_ @t70 @t44))
% 0.48/0.94  (define @t365 () (@var "R2" tptp.produc1871334759_a_nat))
% 0.48/0.94  (define @t366 () (@var "Rs" tptp.set_Pr1987088711_a_nat))
% 0.48/0.94  (define @t367 () (= @t38 (_ tptp.restri446606278nt_a_b @t38)))
% 0.48/0.94  (define @t368 () (@list @t38 @t118 @t117 @t341))
% 0.48/0.94  (define @t369 () (@var "F" tptp.set_Pr2106913242_nat_b))
% 0.48/0.94  (define @t370 () (_ @t348 @t369))
% 0.48/0.94  (define @t371 () (@list @t343 @t342 @t32 @t369))
% 0.48/0.94  (define @t372 () (_ @t353 @t44))
% 0.48/0.94  (define @t373 () (@list @t38 @t39 @t32 @t44))
% 0.48/0.94  (define @t374 () (@var "R22" tptp.labele1159362096nt_a_b))
% 0.48/0.94  (define @t375 () (@var "R1" tptp.labele1159362096nt_a_b))
% 0.48/0.94  (define @t376 () (@var "G2" tptp.set_Product_prod_b_b))
% 0.48/0.94  (define @t377 () (_ tptp.labele1741081071nt_a_b @t49))
% 0.48/0.94  (define @t378 () (_ (_ (_ tptp.graph_222606102_a_b_b @t43) @t32) @t44))
% 0.48/0.94  (define @t379 () (_ tptp.labele1424214014nt_a_b @t39))
% 0.48/0.94  (define @t380 () (_ (_ tptp.graph_222606102_a_b_b @t39) @t32))
% 0.48/0.94  (define @t381 () (@var "R" tptp.set_Pr621705391od_b_b))
% 0.48/0.94  (define @t382 () (_ tptp.image_1177096571od_b_b @t381))
% 0.48/0.94  (define @t383 () (_ @t288 (_ @t382 @t139)))
% 0.48/0.94  (define @t384 () (_ (_ tptp.member641857272od_b_b (_ (_ tptp.produc1257047359od_b_b @t118) @t203)) @t381))
% 0.48/0.94  (define @t385 () (@var "R" tptp.set_Pr2060523537od_b_b))
% 0.48/0.94  (define @t386 () (_ tptp.image_984343321od_b_b @t385))
% 0.48/0.94  (define @t387 () (_ @t291 (_ @t386 @t139)))
% 0.48/0.94  (define @t388 () (_ (_ tptp.member599505522od_b_b (_ (_ tptp.produc800495189od_b_b @t118) @t207)) @t385))
% 0.48/0.94  (define @t389 () (@var "R" tptp.set_Pr357419743_b_b_b))
% 0.48/0.94  (define @t390 () (_ @t191 (_ (_ tptp.image_921732011_b_b_b @t389) @t145)))
% 0.48/0.94  (define @t391 () (_ (_ tptp.member351494440_b_b_b (_ (_ tptp.produc1001682799_b_b_b @t133) @t117)) @t389))
% 0.48/0.94  (define @t392 () (_ tptp.image_1928024979od_b_b @t229))
% 0.48/0.94  (define @t393 () (_ @t288 (_ @t392 @t145)))
% 0.48/0.94  (define @t394 () (@var "R" tptp.set_Pr1071216121od_b_b))
% 0.48/0.94  (define @t395 () (_ @t291 (_ (_ tptp.image_532916993od_b_b @t394) @t145)))
% 0.48/0.94  (define @t396 () (_ (_ tptp.member4694106od_b_b (_ (_ tptp.produc732676669od_b_b @t133) @t207)) @t394))
% 0.48/0.94  (define @t397 () (@var "R" tptp.set_Pr1906739389_b_b_b))
% 0.48/0.94  (define @t398 () (_ @t191 (_ (_ tptp.image_1764625405_b_b_b @t397) @t151)))
% 0.48/0.94  (define @t399 () (_ (_ tptp.member1417789726_b_b_b (_ (_ tptp.produc1580777273_b_b_b @t136) @t117)) @t397))
% 0.48/0.94  (define @t400 () (@var "R" tptp.set_Pr2134561957od_b_b))
% 0.48/0.94  (define @t401 () (_ @t288 (_ (_ tptp.image_1397930469od_b_b @t400) @t151)))
% 0.48/0.94  (define @t402 () (_ (_ tptp.member942707974od_b_b (_ (_ tptp.produc1597690145od_b_b @t136) @t203)) @t400))
% 0.48/0.94  (define @t403 () (_ tptp.image_763305007od_b_b @t233))
% 0.48/0.94  (define @t404 () (_ @t291 (_ @t403 @t151)))
% 0.48/0.94  (define @t405 () (_ tptp.image_b_b @t237))
% 0.48/0.94  (define @t406 () (_ @t405 @t139))
% 0.48/0.94  (define @t407 () (_ @t191 @t406))
% 0.48/0.94  (define @t408 () (@var "R" tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (define @t409 () (_ tptp.image_1916422435od_b_b @t408))
% 0.48/0.94  (define @t410 () (_ @t288 (_ @t409 @t167)))
% 0.48/0.94  (define @t411 () (_ (_ tptp.member1632892294tant_a @t272) @t167))
% 0.48/0.94  (define @t412 () (_ (_ tptp.member1516365892od_b_b @t275) @t408))
% 0.48/0.94  (define @t413 () (@var "R2" tptp.set_Product_prod_b_b))
% 0.48/0.94  (define @t414 () (_ tptp.image_b_b @t413))
% 0.48/0.94  (define @t415 () (@var "R2" tptp.set_Pr1646010159_a_nat))
% 0.48/0.94  (define @t416 () (@var "R2" tptp.set_Pr812188767_nat_b))
% 0.48/0.94  (define @t417 () (@var "R2" tptp.set_Pr924198087_a_nat))
% 0.48/0.94  (define @t418 () (_ tptp.image_1168831379_a_nat @t417))
% 0.48/0.94  (define @t419 () (@var "X3" tptp.set_b))
% 0.48/0.94  (define @t420 () (@var "X3" tptp.set_la1083530965_a_nat))
% 0.48/0.94  (define @t421 () (@var "F" (-> tptp.labele935650037_a_nat tptp.labele935650037_a_nat)))
% 0.48/0.94  (define @t422 () (@var "Y" tptp.set_Product_prod_b_b))
% 0.48/0.94  (define @t423 () (@var "X" tptp.set_Product_prod_b_b))
% 0.48/0.94  (define @t424 () (@var "C" tptp.labele1159362096nt_a_b))
% 0.48/0.94  (define @t425 () (_ tptp.graph_222606102_a_b_b @t63))
% 0.48/0.94  (define @t426 () (@var "B3" tptp.labele1159362096nt_a_b))
% 0.48/0.94  (define @t427 () (_ @t425 @t426))
% 0.48/0.94  (define @t428 () (_ tptp.insert_b @t5))
% 0.48/0.94  (define @t429 () (_ @t428 tptp.bot_bot_set_b))
% 0.48/0.94  (define @t430 () (_ tptp.image_b_b @t18))
% 0.48/0.94  (define @t431 () (_ @t430 @t429))
% 0.48/0.94  (define @t432 () (= @t431 tptp.bot_bot_set_b))
% 0.48/0.94  (define @t433 () (@var "F2" tptp.set_la1083530965_a_nat))
% 0.48/0.94  (define @t434 () (@var "X" tptp.labele935650037_a_nat))
% 0.48/0.94  (define @t435 () (_ tptp.produc1676969687_a_nat @t434))
% 0.48/0.94  (define @t436 () (_ tptp.insert1167839429_a_nat @t434))
% 0.48/0.94  (define @t437 () (_ tptp.insert_b @t118))
% 0.48/0.94  (define @t438 () (_ @t437 tptp.bot_bot_set_b))
% 0.48/0.94  (define @t439 () (_ @t405 @t438))
% 0.48/0.94  (define @t440 () (@var "R" tptp.set_Pr812188767_nat_b))
% 0.48/0.94  (define @t441 () (@var "A2" tptp.produc1871334759_a_nat))
% 0.48/0.94  (define @t442 () (_ tptp.insert1574423351_a_nat @t441))
% 0.48/0.94  (define @t443 () (_ @t442 tptp.bot_bo1836341171_a_nat))
% 0.48/0.94  (define @t444 () (@var "R" tptp.set_Pr667377223od_b_b))
% 0.48/0.94  (define @t445 () (@var "R" tptp.set_Pr1954438265od_b_b))
% 0.48/0.94  (define @t446 () (@var "B3" tptp.set_Product_prod_b_b))
% 0.48/0.94  (define @t447 () (@var "A2" (-> tptp.b tptp.b)))
% 0.48/0.94  (define @t448 () (_ @t7 @t33))
% 0.48/0.94  (define @t449 () (@var "B3" tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (define @t450 () (@var "A2" (-> tptp.b tptp.standard_Constant_a)))
% 0.48/0.94  (define @t451 () (@var "F" tptp.set_Pr812188767_nat_b))
% 0.48/0.94  (define @t452 () (_ tptp.labele1230159100nt_a_b tptp.bot_bo1664927607od_b_b))
% 0.48/0.94  (define @t453 () (_ (_ tptp.ord_less_eq_set_b @t80) @t85))
% 0.48/0.94  (define @t454 () (_ (_ tptp.ord_le123089219od_b_b (_ tptp.labele1741081071nt_a_b @t50)) @t377))
% 0.48/0.94  (define @t455 () (@var "C" tptp.b))
% 0.48/0.94  (define @t456 () (_ tptp.insert_b @t455))
% 0.48/0.94  (define @t457 () (_ tptp.insert_b @t117))
% 0.48/0.94  (define @t458 () (_ @t361 @t455))
% 0.48/0.94  (define @t459 () (_ (_ tptp.labele1230159100nt_a_b (_ (_ tptp.insert2037698781od_b_b (_ @t274 @t458)) tptp.bot_bo1664927607od_b_b)) (_ @t457 (_ @t456 tptp.bot_bot_set_b))))
% 0.48/0.94  (define @t460 () (not @t8))
% 0.48/0.94  (define @t461 () (= @t432 @t460))
% 0.48/0.94  (define @t462 () (forall @t9 @t461))
% 0.48/0.94  (define @t463 () (@var "X" tptp.produc1871334759_a_nat))
% 0.48/0.94  (define @t464 () (_ tptp.insert1574423351_a_nat @t463))
% 0.48/0.94  (define @t465 () (_ tptp.product_Pair_b_b @t140))
% 0.48/0.94  (define @t466 () (@list @t117 @t237 @t139))
% 0.48/0.94  (define @t467 () (@var "X5" tptp.standard_Constant_a))
% 0.48/0.94  (define @t468 () (@list @t203 @t408 @t167))
% 0.48/0.94  (define @t469 () (not @t217))
% 0.48/0.94  (define @t470 () (not @t223))
% 0.48/0.94  (define @t471 () (not @t227))
% 0.48/0.94  (define @t472 () (@var "S" tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (define @t473 () (@var "R" tptp.set_Pr154086431tant_a))
% 0.48/0.94  (define @t474 () (_ (_ tptp.relcom883816262od_b_b @t473) @t472))
% 0.48/0.94  (define @t475 () (_ tptp.member1516365892od_b_b (_ @t274 @t226)))
% 0.48/0.94  (define @t476 () (_ @t475 @t474))
% 0.48/0.94  (define @t477 () (@var "B3" tptp.standard_Constant_a))
% 0.48/0.94  (define @t478 () (_ tptp.produc342647tant_a @t272))
% 0.48/0.94  (define @t479 () (@var "S" tptp.set_Product_prod_b_b))
% 0.48/0.94  (define @t480 () (_ (_ tptp.relcomp_b_b_b @t237) @t479))
% 0.48/0.94  (define @t481 () (_ (_ tptp.member1285940496od_b_b (_ @t119 @t455)) @t480))
% 0.48/0.94  (define @t482 () (@var "S" tptp.set_Pr2007082183od_b_b))
% 0.48/0.94  (define @t483 () (_ (_ tptp.relcom1823941168od_b_b @t408) @t482))
% 0.48/0.94  (define @t484 () (_ @t475 @t483))
% 0.48/0.94  (define @t485 () (@var "P" (-> tptp.b tptp.b Bool)))
% 0.48/0.94  (define @t486 () (@var "P" (-> tptp.standard_Constant_a tptp.product_prod_b_b Bool)))
% 0.48/0.94  (define @t487 () (_ (_ @t486 @t286) @t284))
% 0.48/0.94  (define @t488 () (@var "C2" tptp.product_prod_b_b))
% 0.48/0.94  (define @t489 () (_ (_ @t486 @t328) @t488))
% 0.48/0.94  (define @t490 () (@var "B5" tptp.standard_Constant_a))
% 0.48/0.94  (define @t491 () (_ tptp.produc1432590431od_b_b @t490))
% 0.48/0.94  (define @t492 () (_ tptp.member1516365892od_b_b @t287))
% 0.48/0.94  (define @t493 () (_ tptp.produc546497367od_b_b @t327))
% 0.48/0.94  (define @t494 () (@var "C3" tptp.b))
% 0.48/0.94  (define @t495 () (@var "B6" tptp.b))
% 0.48/0.94  (define @t496 () (@var "A5" tptp.b))
% 0.48/0.94  (define @t497 () (@var "A1" tptp.b))
% 0.48/0.94  (define @t498 () (_ tptp.product_Pair_b_b @t497))
% 0.48/0.94  (define @t499 () (_ (_ tptp.member1285940496od_b_b (_ @t498 @t127)) @t480))
% 0.48/0.94  (define @t500 () (@list @t497 @t127 @t237 @t479))
% 0.48/0.94  (define @t501 () (@var "C3" tptp.product_prod_b_b))
% 0.48/0.94  (define @t502 () (@var "B6" tptp.standard_Constant_a))
% 0.48/0.94  (define @t503 () (@var "A5" tptp.standard_Constant_a))
% 0.48/0.94  (define @t504 () (= @t123 @t501))
% 0.48/0.94  (define @t505 () (@var "A1" tptp.standard_Constant_a))
% 0.48/0.94  (define @t506 () (= @t505 @t503))
% 0.48/0.94  (define @t507 () (_ tptp.produc1432590431od_b_b @t505))
% 0.48/0.94  (define @t508 () (_ tptp.member1516365892od_b_b (_ @t507 @t123)))
% 0.48/0.94  (define @t509 () (_ @t508 @t474))
% 0.48/0.94  (define @t510 () (@list @t505 @t123 @t473 @t472))
% 0.48/0.94  (define @t511 () (@var "B6" tptp.product_prod_b_b))
% 0.48/0.94  (define @t512 () (_ @t508 @t483))
% 0.48/0.94  (define @t513 () (@list @t505 @t123 @t408 @t482))
% 0.48/0.94  (define @t514 () (@list @t322))
% 0.48/0.94  (define @t515 () (@list @t490))
% 0.48/0.94  (define @t516 () (@list @t327))
% 0.48/0.94  (define @t517 () (@var "Z2" tptp.b))
% 0.48/0.94  (define @t518 () (_ tptp.member1285940496od_b_b @t261))
% 0.48/0.94  (define @t519 () (_ @t518 @t237))
% 0.48/0.94  (define @t520 () (@var "Xz" tptp.product_prod_b_b))
% 0.48/0.94  (define @t521 () (@var "Z2" tptp.product_prod_b_b))
% 0.48/0.94  (define @t522 () (@var "Y3" tptp.standard_Constant_a))
% 0.48/0.94  (define @t523 () (@var "Xz" tptp.produc1213276845od_b_b))
% 0.48/0.94  (define @t524 () (= @t523 (_ @t318 @t521)))
% 0.48/0.94  (define @t525 () (_ tptp.member1516365892od_b_b @t523))
% 0.48/0.94  (define @t526 () (_ tptp.member1516365892od_b_b @t319))
% 0.48/0.94  (define @t527 () (_ @t526 @t408))
% 0.48/0.94  (define @t528 () (@var "Z3" tptp.set_b))
% 0.48/0.94  (define @t529 () (@var "X3" tptp.set_Product_prod_b_b))
% 0.48/0.94  (define @t530 () (@var "Y2" tptp.set_Product_prod_b_b))
% 0.48/0.94  (define @t531 () (@var "A6" tptp.set_b))
% 0.48/0.94  (define @t532 () (@var "R3" tptp.set_Product_prod_b_b))
% 0.48/0.94  (define @t533 () (@var "G5" tptp.set_Pr2106913242_nat_b))
% 0.48/0.94  (define @t534 () (@var "G5" tptp.set_Product_prod_b_b))
% 0.48/0.94  (define @t535 () (@var "Ba" tptp.b))
% 0.48/0.94  (define @t536 () (@var "Aa" tptp.b))
% 0.48/0.94  (define @t537 () (_ tptp.member1285940496od_b_b (_ (_ tptp.product_Pair_b_b @t536) @t535)))
% 0.48/0.94  (define @t538 () (_ @t537 @t44))
% 0.48/0.94  (define @t539 () (_ @t427 @t44))
% 0.48/0.94  (define @t540 () (@list @t63 @t426 @t44 @t536 @t535))
% 0.48/0.94  (define @t541 () (_ (_ tptp.bNF_Gr_b_b @t379) @t74))
% 0.48/0.94  (define @t542 () (_ @t457 tptp.bot_bot_set_b))
% 0.48/0.94  (define @t543 () (_ tptp.ord_less_eq_set_b @t139))
% 0.48/0.94  (define @t544 () (and @t211 (_ @t543 @t542)))
% 0.48/0.94  (define @t545 () (_ @t437 @t139))
% 0.48/0.94  (define @t546 () (@var "B3" tptp.produc1871334759_a_nat))
% 0.48/0.94  (define @t547 () (_ tptp.insert1574423351_a_nat @t546))
% 0.48/0.94  (define @t548 () (_ @t547 tptp.bot_bo1836341171_a_nat))
% 0.48/0.94  (define @t549 () (@var "A" tptp.set_Pr1987088711_a_nat))
% 0.48/0.94  (define @t550 () (_ tptp.ord_le1718765799_a_nat @t549))
% 0.48/0.94  (define @t551 () (= @t441 @t546))
% 0.48/0.94  (define @t552 () (and @t551 (_ @t550 @t548)))
% 0.48/0.94  (define @t553 () (_ @t442 @t549))
% 0.48/0.94  (define @t554 () (_ @t405 @t542))
% 0.48/0.94  (define @t555 () (_ tptp.equiv_equiv_b @t139))
% 0.48/0.94  (define @t556 () (_ @t555 @t237))
% 0.48/0.94  (define @t557 () (@var "R" tptp.set_Pr924198087_a_nat))
% 0.48/0.94  (define @t558 () (_ tptp.image_1168831379_a_nat @t557))
% 0.48/0.94  (define @t559 () (_ @t558 @t548))
% 0.48/0.94  (define @t560 () (_ @t558 @t443))
% 0.48/0.94  (define @t561 () (_ (_ tptp.member584645392_a_nat (_ (_ tptp.produc1677124439_a_nat @t441) @t546)) @t557))
% 0.48/0.94  (define @t562 () (_ tptp.equiv_291114781_a_nat @t549))
% 0.48/0.94  (define @t563 () (_ @t562 @t557))
% 0.48/0.94  (define @t564 () (_ tptp.insert1952693431od_b_b @t133))
% 0.48/0.94  (define @t565 () (_ @t564 tptp.bot_bo1343651123od_b_b))
% 0.48/0.94  (define @t566 () (_ tptp.insert1952693431od_b_b @t203))
% 0.48/0.94  (define @t567 () (_ tptp.insert2037698781od_b_b @t136))
% 0.48/0.94  (define @t568 () (_ @t567 tptp.bot_bo1664927607od_b_b))
% 0.48/0.94  (define @t569 () (_ tptp.insert2037698781od_b_b @t207))
% 0.48/0.94  (define @t570 () (_ tptp.member832397200_a_nat @t546))
% 0.48/0.94  (define @t571 () (@var "S2" tptp.set_Product_prod_b_b))
% 0.48/0.94  (define @t572 () (_ tptp.image_b_b @t571))
% 0.48/0.94  (define @t573 () (@var "S2" tptp.set_Pr924198087_a_nat))
% 0.48/0.94  (define @t574 () (_ tptp.image_1168831379_a_nat @t573))
% 0.48/0.94  (define @t575 () (forall @t143 (not (_ @t130 @t140))))
% 0.48/0.94  (define @t576 () (@list @t130))
% 0.48/0.94  (define @t577 () (@var "X5" tptp.produc1871334759_a_nat))
% 0.48/0.94  (define @t578 () (@var "P" (-> tptp.produc1871334759_a_nat Bool)))
% 0.48/0.94  (define @t579 () (@list @t577))
% 0.48/0.94  (define @t580 () (forall @t579 (not (_ @t578 @t577))))
% 0.48/0.94  (define @t581 () (_ tptp.collec357096914_a_nat @t578))
% 0.48/0.94  (define @t582 () (@list @t578))
% 0.48/0.94  (define @t583 () (= @t145 tptp.bot_bo1343651123od_b_b))
% 0.48/0.94  (define @t584 () (= @t151 tptp.bot_bo1664927607od_b_b))
% 0.48/0.94  (define @t585 () (= @t139 tptp.bot_bot_set_b))
% 0.48/0.94  (define @t586 () (= @t549 tptp.bot_bo1836341171_a_nat))
% 0.48/0.94  (define @t587 () (_ (_ tptp.member832397200_a_nat @t577) @t549))
% 0.48/0.94  (define @t588 () (@list @t549))
% 0.48/0.94  (define @t589 () (@var "C" tptp.produc1213276845od_b_b))
% 0.48/0.94  (define @t590 () (_ tptp.member1516365892od_b_b @t589))
% 0.48/0.94  (define @t591 () (_ tptp.member_b @t455))
% 0.48/0.94  (define @t592 () (@var "C" tptp.produc1871334759_a_nat))
% 0.48/0.94  (define @t593 () (@var "B" tptp.set_b))
% 0.48/0.94  (define @t594 () (_ @t543 @t593))
% 0.48/0.94  (define @t595 () (@var "B" tptp.set_Product_prod_b_b))
% 0.48/0.94  (define @t596 () (_ (_ tptp.ord_le1036320359od_b_b @t145) @t595))
% 0.48/0.94  (define @t597 () (@var "B" tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (define @t598 () (_ (_ tptp.ord_le123089219od_b_b @t151) @t597))
% 0.48/0.94  (define @t599 () (_ @t428 @t139))
% 0.48/0.94  (define @t600 () (@list @t5 @t139))
% 0.48/0.94  (define @t601 () (_ @t464 @t549))
% 0.48/0.94  (define @t602 () (@list @t463 @t549))
% 0.48/0.94  (define @t603 () (_ tptp.member832397200_a_nat @t441))
% 0.48/0.94  (define @t604 () (_ @t603 @t549))
% 0.48/0.94  (define @t605 () (_ @t603 (_ @t547 @t549)))
% 0.48/0.94  (define @t606 () (@list @t441 @t546 @t549))
% 0.48/0.94  (define @t607 () (_ @t132 (_ @t457 @t139)))
% 0.48/0.94  (define @t608 () (_ @t135 (_ @t566 @t145)))
% 0.48/0.94  (define @t609 () (_ @t138 (_ @t569 @t151)))
% 0.48/0.94  (define @t610 () (@var "B" tptp.set_Pr1987088711_a_nat))
% 0.48/0.94  (define @t611 () (_ @t547 @t610))
% 0.48/0.94  (define @t612 () (_ @t603 @t611))
% 0.48/0.94  (define @t613 () (_ @t603 @t610))
% 0.48/0.94  (define @t614 () (@list @t441 @t610 @t546))
% 0.48/0.94  (define @t615 () (_ @t457 @t593))
% 0.48/0.94  (define @t616 () (_ @t132 @t615))
% 0.48/0.94  (define @t617 () (_ @t132 @t593))
% 0.48/0.94  (define @t618 () (@list @t118 @t593 @t117))
% 0.48/0.94  (define @t619 () (_ @t566 @t595))
% 0.48/0.94  (define @t620 () (_ @t135 @t619))
% 0.48/0.94  (define @t621 () (_ @t135 @t595))
% 0.48/0.94  (define @t622 () (@list @t133 @t595 @t203))
% 0.48/0.94  (define @t623 () (_ @t569 @t597))
% 0.48/0.94  (define @t624 () (_ @t138 @t623))
% 0.48/0.94  (define @t625 () (_ @t138 @t597))
% 0.48/0.94  (define @t626 () (@list @t136 @t597 @t207))
% 0.48/0.94  (define @t627 () (@list @t133))
% 0.48/0.94  (define @t628 () (@list @t136))
% 0.48/0.94  (define @t629 () (@list @t118))
% 0.48/0.94  (define @t630 () (@list @t441))
% 0.48/0.94  (define @t631 () (_ tptp.member832397200_a_nat @t463))
% 0.48/0.94  (define @t632 () (_ @t631 @t610))
% 0.48/0.94  (define @t633 () (@list @t463 @t549 @t610))
% 0.48/0.94  (define @t634 () (_ @t7 @t593))
% 0.48/0.94  (define @t635 () (@list @t5 @t139 @t593))
% 0.48/0.94  (define @t636 () (_ @t195 @t595))
% 0.48/0.94  (define @t637 () (_ tptp.insert1952693431od_b_b @t194))
% 0.48/0.94  (define @t638 () (_ @t637 @t145))
% 0.48/0.94  (define @t639 () (@list @t194 @t145 @t595))
% 0.48/0.94  (define @t640 () (_ @t199 @t597))
% 0.48/0.94  (define @t641 () (_ tptp.insert2037698781od_b_b @t198))
% 0.48/0.94  (define @t642 () (_ @t641 @t151))
% 0.48/0.94  (define @t643 () (@list @t198 @t151 @t597))
% 0.48/0.94  (define @t644 () (@var "R2" tptp.set_Pr1987088711_a_nat))
% 0.48/0.94  (define @t645 () (@list @t644))
% 0.48/0.94  (define @t646 () (_ @t452 @t354))
% 0.48/0.94  (define @t647 () (@var "Y3" tptp.produc1871334759_a_nat))
% 0.48/0.94  (define @t648 () (not @t180))
% 0.48/0.94  (define @t649 () (not @t185))
% 0.48/0.94  (define @t650 () (not @t189))
% 0.48/0.94  (define @t651 () (not @t604))
% 0.48/0.94  (define @t652 () (@var "B7" tptp.set_b))
% 0.48/0.94  (define @t653 () (@var "A7" tptp.set_b))
% 0.48/0.94  (define @t654 () (@list @t653 @t652))
% 0.48/0.94  (define @t655 () (@var "B7" tptp.set_Product_prod_b_b))
% 0.48/0.94  (define @t656 () (@var "A7" tptp.set_Product_prod_b_b))
% 0.48/0.94  (define @t657 () (@list @t656 @t655))
% 0.48/0.94  (define @t658 () (@var "B7" tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (define @t659 () (@var "A7" tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (define @t660 () (@list @t659 @t658))
% 0.48/0.94  (define @t661 () (@var "B8" tptp.set_Pr1987088711_a_nat))
% 0.48/0.94  (define @t662 () (@list @t661))
% 0.48/0.94  (define @t663 () (@list @t441 @t549))
% 0.48/0.94  (define @t664 () (@var "B8" tptp.set_b))
% 0.48/0.94  (define @t665 () (@list @t664))
% 0.48/0.94  (define @t666 () (@var "B8" tptp.set_Product_prod_b_b))
% 0.48/0.94  (define @t667 () (@list @t666))
% 0.48/0.94  (define @t668 () (@var "B8" tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (define @t669 () (@list @t668))
% 0.48/0.94  (define @t670 () (_ tptp.insert_b @t20))
% 0.48/0.94  (define @t671 () (@var "Y" tptp.produc1871334759_a_nat))
% 0.48/0.94  (define @t672 () (_ tptp.insert1574423351_a_nat @t671))
% 0.48/0.94  (define @t673 () (@var "C4" tptp.set_Pr1987088711_a_nat))
% 0.48/0.94  (define @t674 () (not @t551))
% 0.48/0.94  (define @t675 () (= @t549 @t610))
% 0.48/0.94  (define @t676 () (@var "C4" tptp.set_b))
% 0.48/0.94  (define @t677 () (not @t211))
% 0.48/0.94  (define @t678 () (= @t139 @t593))
% 0.48/0.94  (define @t679 () (@var "C4" tptp.set_Product_prod_b_b))
% 0.48/0.94  (define @t680 () (not @t205))
% 0.48/0.94  (define @t681 () (= @t145 @t595))
% 0.48/0.94  (define @t682 () (_ @t564 @t145))
% 0.48/0.94  (define @t683 () (@var "C4" tptp.set_Pr1324126435od_b_b))
% 0.48/0.94  (define @t684 () (not @t209))
% 0.48/0.94  (define @t685 () (= @t151 @t597))
% 0.48/0.94  (define @t686 () (_ @t567 @t151))
% 0.48/0.94  (define @t687 () (_ @t631 @t549))
% 0.48/0.94  (define @t688 () (@var "D" tptp.b))
% 0.48/0.94  (define @t689 () (@var "D" tptp.produc1871334759_a_nat))
% 0.48/0.94  (define @t690 () (@var "V3" tptp.b))
% 0.48/0.94  (define @t691 () (_ @t97 tptp.g))
% 0.48/0.94  (define @t692 () (@var "P" Bool))
% 0.48/0.94  (define @t693 () (_ (_ (_ tptp.if_b true) @t5) @t20))
% 0.48/0.94  (define @t694 () (forall @t129 (= @t693 @t5)))
% 0.48/0.94  (define @t695 () (_ tptp.member_b tptp.x))
% 0.48/0.94  (define @t696 () (_ @t695 @t1))
% 0.48/0.94  (define @t697 () (not @t696))
% 0.48/0.94  (define @t698 () (_ tptp.hilbert_Eps_b (_ tptp.p @t140)))
% 0.48/0.94  (define @t699 () (_ (_ tptp.insert_b @t140) tptp.bot_bot_set_b))
% 0.48/0.94  (define @t700 () (_ @t430 @t699))
% 0.48/0.94  (define @t701 () (lambda @t143 (_ (_ (_ tptp.if_b (= @t700 tptp.bot_bot_set_b)) @t140) @t698)))
% 0.48/0.94  (define @t702 () (@var "F_2" tptp.set_Product_prod_b_b))
% 0.48/0.94  (define @t703 () (@var "F_1" tptp.set_Product_prod_b_b))
% 0.48/0.94  (define @t704 () (@var "G4" tptp.labele1159362096nt_a_b))
% 0.48/0.94  (define @t705 () (lambda (@list @t704 @t703 @t702) (forall @t143 (=> (_ @t141 (_ tptp.labele1424214014nt_a_b @t704)) (= (_ (_ tptp.image_b_b @t703) @t699) (_ (_ tptp.image_b_b @t702) @t699))))))
% 0.48/0.94  (define @t706 () (@var "T" tptp.b))
% 0.48/0.94  (define @t707 () (_ tptp.member_b @t706))
% 0.48/0.94  (define @t708 () (lambda @t654 (forall (@list @t706) (=> (_ @t707 @t653) (_ @t707 @t652)))))
% 0.48/0.94  (define @t709 () (@var "T" tptp.product_prod_b_b))
% 0.48/0.94  (define @t710 () (_ tptp.member1285940496od_b_b @t709))
% 0.48/0.94  (define @t711 () (lambda @t657 (forall (@list @t709) (=> (_ @t710 @t656) (_ @t710 @t655)))))
% 0.48/0.94  (define @t712 () (@var "T" tptp.produc1213276845od_b_b))
% 0.48/0.94  (define @t713 () (_ tptp.member1516365892od_b_b @t712))
% 0.48/0.94  (define @t714 () (lambda @t660 (forall (@list @t712) (=> (_ @t713 @t659) (_ @t713 @t658)))))
% 0.48/0.94  (define @t715 () (@var "Y4" tptp.b))
% 0.48/0.94  (define @t716 () (_ tptp.member_b @t715))
% 0.48/0.94  (define @t717 () (_ @t716 @t700))
% 0.48/0.94  (define @t718 () (lambda (@list @t140 @t715) @t717))
% 0.48/0.94  (define @t719 () (tptp.insert_b @t5 tptp.bot_bot_set_b))
% 0.48/0.94  (define @t720 () (tptp.getRel904497637nt_a_b tptp.standard_S_Idt_a tptp.g))
% 0.48/0.94  (define @t721 () (tptp.image_b_b @t720 @t719))
% 0.48/0.94  (define @t722 () (_ tptp.image_b_b @t720))
% 0.48/0.94  (define @t723 () (= tptp.bot_bot_set_b @t431))
% 0.48/0.94  (define @t724 () (tptp.labele1424214014nt_a_b tptp.g))
% 0.48/0.94  (define @t725 () (tptp.member_b @t5 @t724))
% 0.48/0.94  (define @t726 () (= @t460 @t723))
% 0.48/0.94  (define @t727 () (tptp.member_b tptp.x @t724))
% 0.48/0.94  (define @t728 () (tptp.if_b true @t5 @t20))
% 0.48/0.94  (define @t729 () (= @t5 @t693))
% 0.48/0.94  (define @t730 () (_ (_ tptp.insert_b tptp.x) tptp.bot_bot_set_b))
% 0.48/0.94  (define @t731 () (_ @t430 @t730))
% 0.48/0.94  (define @t732 () (@list @t715))
% 0.48/0.94  (define @t733 () (lambda @t732 (_ @t716 @t731)))
% 0.48/0.94  (define @t734 () (@purify @t733))
% 0.48/0.94  (define @t735 () (tptp.hilbert_Eps_b @t734))
% 0.48/0.94  (define @t736 () (@purify true))
% 0.48/0.94  (define @t737 () (tptp.if_b true tptp.x @t735))
% 0.48/0.94  (define @t738 () (= tptp.x @t737))
% 0.48/0.94  (define @t739 () (forall @t129 (= @t5 @t728)))
% 0.48/0.94  (define @t740 () (tptp.if_b @t736 tptp.x @t735))
% 0.48/0.94  (define @t741 () (= tptp.x @t740))
% 0.48/0.94  (define @t742 () (_ tptp.hilbert_Eps_b @t734))
% 0.48/0.94  (define @t743 () (= tptp.bot_bot_set_b @t731))
% 0.48/0.94  (define @t744 () (@purify @t743))
% 0.48/0.94  (define @t745 () (_ (_ tptp.if_b @t744) tptp.x))
% 0.48/0.94  (define @t746 () (_ @t745 @t742))
% 0.48/0.94  (define @t747 () (tptp.if_b @t744 tptp.x @t735))
% 0.48/0.94  (define @t748 () (tptp.member_b @t747 @t724))
% 0.48/0.94  (define @t749 () (= @t743 @t744))
% 0.48/0.94  (define @t750 () (lambda @t732 @t717))
% 0.48/0.94  (define @t751 () (_ (_ tptp.if_b (= tptp.bot_bot_set_b @t700)) @t140))
% 0.48/0.94  (define @t752 () (_ @t718 @t140))
% 0.48/0.94  (define @t753 () (not @t741))
% 0.48/0.94  (define @t754 () (not @t736))
% 0.48/0.94  (define @t755 () (not @t748))
% 0.48/0.94  (define @t756 () (not @t744))
% 0.48/0.94  (define @t757 () (not @t727))
% 0.48/0.94  (define @t758 () (not @t757))
% 0.48/0.94  (define @t759 () (and @t748 @t744 @t736 @t741 @t757))
% 0.48/0.94  (define @t760 () (tptp.insert_b tptp.x tptp.bot_bot_set_b))
% 0.48/0.94  (define @t761 () (tptp.image_b_b @t720 @t760))
% 0.48/0.94  (define @t762 () (= tptp.bot_bot_set_b @t761))
% 0.48/0.94  (define @t763 () (= @t762 @t757))
% 0.48/0.94  (define @t764 () (not @t763))
% 0.48/0.94  (define @t765 () (forall @t9 (= (not @t725) (= tptp.bot_bot_set_b @t721))))
% 0.48/0.94  (define @t766 () (= @t757 @t762))
% 0.48/0.94  (assume @p1 (forall (@list @t2) (=> (_ (_ tptp.member_b (_ tptp.f @t2)) @t1) (_ (_ tptp.member_b @t2) @t1))))
% 0.48/0.94  (assume @p2 (_ (_ tptp.member_b @t3) @t1))
% 0.48/0.94  (assume @p3 (_ (_ tptp.member_b @t4) @t1))
% 0.48/0.94  (assume @p4 (forall @t9 (=> @t8 (_ (_ tptp.member_b @t6) @t1))))
% 0.48/0.94  (assume @p5 (= tptp.g (_ tptp.restri446606278nt_a_b tptp.g)))
% 0.48/0.94  (assume @p6 (forall @t9 (= @t8 (_ @t10 @t5))))
% 0.48/0.94  (assume @p7 (forall @t14 (=> (_ @t13 (_ tptp.standa1568205540ules_a tptp.l)) @t12)))
% 0.48/0.94  (assume @p8 (_ (_ tptp.member1285940496od_b_b @t15) (_ (_ tptp.getRel904497637nt_a_b tptp.l2) tptp.g)))
% 0.48/0.94  (assume @p9 (_ (_ tptp.member1516365892od_b_b (_ (_ tptp.produc1432590431od_b_b tptp.l2) @t15)) @t16))
% 0.48/0.94  (assume @p10 (_ (_ tptp.refl_on_b @t1) @t18))
% 0.48/0.94  (assume @p11 (_ (_ tptp.equiv_equiv_b @t1) @t18))
% 0.48/0.94  (assume @p12 (= (_ (_ tptp.graph_1309249505nt_a_b @t19) tptp.g) tptp.g))
% 0.48/0.94  (assume @p13 (forall (@list @t21 @t5 @t20) (=> (_ (_ tptp.member1516365892od_b_b (_ @t22 @t25)) @t16) (=> @t8 (=> (_ @t23 @t1) (_ (_ tptp.member1516365892od_b_b (_ @t22 (_ (_ tptp.product_Pair_b_b @t6) (_ tptp.f @t20)))) @t16))))))
% 0.48/0.94  (assume @p14 (forall @t9 (=> @t8 (_ (_ tptp.member1285940496od_b_b @t26) @t18))))
% 0.48/0.94  (assume @p15 (forall @t30 (= (_ tptp.labele1424214014nt_a_b @t29) @t27)))
% 0.48/0.94  (assume @p16 (_ (_ (_ tptp.graph_222606102_a_b_b @t19) tptp.g) (_ tptp.id_on_b @t31)))
% 0.48/0.94  (assume @p17 (forall @t35 (= (_ tptp.labele1424214014nt_a_b @t34) @t33)))
% 0.48/0.94  (assume @p18 (forall (@list @t36) (= (_ tptp.restri446606278nt_a_b @t37) @t37)))
% 0.48/0.94  (assume @p19 (forall @t42 (= (_ @t41 @t40) @t40)))
% 0.48/0.94  (assume @p20 (forall @t42 (= (_ @t41 @t43) @t43)))
% 0.48/0.94  (assume @p21 (forall (@list @t38) (= (_ @t41 @t38) @t38)))
% 0.48/0.94  (assume @p22 (forall @t48 (=> @t47 (= @t46 (_ tptp.restri446606278nt_a_b @t46)))))
% 0.48/0.94  (assume @p23 (forall @t55 (=> @t54 (=> @t52 (= @t51 (_ tptp.restri446606278nt_a_b @t51))))))
% 0.48/0.94  (assume @p24 (forall @t60 (= @t59 @t56)))
% 0.48/0.94  (assume @p25 (forall @t35 (= (_ (_ @t62 @t32) @t61) @t47)))
% 0.48/0.94  (assume @p26 (forall @t35 (= (_ (_ @t62 @t34) @t61) @t47)))
% 0.48/0.94  (assume @p27 (forall (@list @t63) (_ (_ (_ tptp.graph_222606102_a_b_b @t65) @t65) @t64)))
% 0.48/0.94  (assume @p28 (forall (@list @t38 @t39 @t44) (=> @t71 (_ (_ (_ tptp.graph_222606102_a_b_b @t66) (_ @t45 @t39)) (_ tptp.id_on_b (_ tptp.labele1424214014nt_a_b @t66))))))
% 0.48/0.94  (assume @p29 (forall (@list @t72) (= (_ (_ tptp.map_gr926947118tant_a (_ tptp.id_on_b @t73)) @t72) (_ tptp.restri446606278nt_a_b @t72))))
% 0.48/0.94  (assume @p30 (forall @t78 (= @t77 (_ tptp.restri446606278nt_a_b @t77))))
% 0.48/0.94  (assume @p31 (forall @t78 (=> @t47 (_ (_ @t62 @t77) @t76))))
% 0.48/0.94  (assume @p32 (forall @t30 (= (_ tptp.labele1741081071nt_a_b @t29) @t28)))
% 0.48/0.94  (assume @p33 (forall @t55 (= @t83 (and @t54 @t52 @t79))))
% 0.48/0.94  (assume @p34 (forall (@list @t50 @t49 @t84) (=> @t83 (=> (_ (_ (_ tptp.graph_222606102_a_b_b @t49) @t84) (_ tptp.id_on_b @t85)) (_ (_ @t82 @t84) @t81)))))
% 0.48/0.94  (assume @p35 (forall (@list @t32 @t74 @t86) (=> (forall @t90 (=> (_ @t89 @t33) (= @t88 (_ @t86 @t87)))) (= @t77 (_ (_ tptp.map_gr926947118tant_a (_ @t75 @t86)) @t32)))))
% 0.48/0.94  (assume @p36 (forall (@list @t38 @t39 @t72 @t91) (=> @t71 (=> (_ (_ @t92 @t38) @t91) (_ (_ @t92 @t39) @t91)))))
% 0.48/0.94  (assume @p37 (forall @t60 (= @t56 @t59)))
% 0.48/0.94  (assume @p38 (forall (@list @t56 @t93) (=> (and (= @t58 (_ tptp.labele1741081071nt_a_b @t93)) (= @t57 (_ tptp.labele1424214014nt_a_b @t93))) (= @t56 @t93))))
% 0.48/0.94  (assume @p39 (forall (@list @t100 @t99 @t21 @t94 @t95) (=> (_ (_ tptp.member1652792080od_b_b (_ (_ tptp.produc546497367od_b_b @t100) @t99)) @t102) (=> (_ @t101 @t96) (=> (_ (_ tptp.member1285940496od_b_b @t99) @t96) (_ (_ tptp.member1285940496od_b_b (_ (_ tptp.product_Pair_b_b (_ @t95 @t100)) (_ @t95 @t99))) @t98))))))
% 0.48/0.94  (assume @p40 (forall (@list @t108 @t107 @t21 @t103 @t104) (=> (_ (_ tptp.member1086024932od_b_b (_ (_ tptp.produc449289715od_b_b @t108) @t107)) @t110) (=> (_ @t109 @t105) (=> (_ (_ tptp.member1516365892od_b_b @t107) @t105) (_ (_ tptp.member1285940496od_b_b (_ (_ tptp.product_Pair_b_b (_ @t104 @t108)) (_ @t104 @t107))) @t106))))))
% 0.48/0.94  (assume @p41 (forall (@list @t20 @t112 @t21 @t32 @t74) (=> @t116 (=> (_ @t23 @t33) (=> (_ (_ tptp.member_b @t112) @t33) (_ (_ tptp.member1285940496od_b_b (_ (_ tptp.product_Pair_b_b (_ @t74 @t20)) (_ @t74 @t112))) @t111))))))
% 0.48/0.94  (assume @p42 (forall (@list @t123 @t94 @t122 @t21 @t95 @t118 @t117) (=> (_ (_ tptp.member1285940496od_b_b @t123) @t96) (=> (_ (_ tptp.member1285940496od_b_b @t122) @t96) (=> (_ (_ tptp.member1652792080od_b_b (_ (_ tptp.produc546497367od_b_b @t123) @t122)) @t102) (=> (= (_ @t95 @t123) @t118) (=> (= (_ @t95 @t122) @t117) (_ @t121 @t98))))))))
% 0.48/0.94  (assume @p43 (forall (@list @t125 @t103 @t124 @t21 @t104 @t118 @t117) (=> (_ (_ tptp.member1516365892od_b_b @t125) @t105) (=> (_ (_ tptp.member1516365892od_b_b @t124) @t105) (=> (_ (_ tptp.member1086024932od_b_b (_ (_ tptp.produc449289715od_b_b @t125) @t124)) @t110) (=> (= (_ @t104 @t125) @t118) (=> (= (_ @t104 @t124) @t117) (_ @t121 @t106))))))))
% 0.48/0.94  (assume @p44 (forall (@list @t127 @t32 @t126 @t21 @t74 @t118 @t117) (=> (_ (_ tptp.member_b @t127) @t33) (=> (_ (_ tptp.member_b @t126) @t33) (=> (_ (_ tptp.member1285940496od_b_b (_ (_ tptp.product_Pair_b_b @t127) @t126)) @t113) (=> (= (_ @t74 @t127) @t118) (=> (= (_ @t74 @t126) @t117) (_ @t121 @t111))))))))
% 0.48/0.94  (assume @p45 (forall @t129 (=> (_ (_ tptp.member1516365892od_b_b (_ (_ tptp.produc1432590431od_b_b tptp.standard_S_Idt_a) @t25)) @t16) (= @t128 (_ tptp.hilbert_Eps_b (_ tptp.p @t20))))))
% 0.48/0.94  (assume @p46 (forall @t9 (=> @t8 (_ (_ tptp.member1285940496od_b_b (_ @t24 @t128)) @t18))))
% 0.48/0.94  (assume @p47 (forall (@list @t118 @t130) (= (_ @t132 @t131) (_ @t130 @t118))))
% 0.48/0.94  (assume @p48 (forall (@list @t133 @t134) (= (_ @t135 (_ tptp.collec1481886546od_b_b @t134)) (_ @t134 @t133))))
% 0.48/0.94  (assume @p49 (forall (@list @t136 @t137) (= (_ @t138 (_ tptp.collec279084418od_b_b @t137)) (_ @t137 @t136))))
% 0.48/0.94  (assume @p50 (forall @t144 (= (_ tptp.collect_b (lambda @t143 @t142)) @t139)))
% 0.48/0.94  (assume @p51 (forall @t150 (= (_ tptp.collec1481886546od_b_b (lambda @t149 @t148)) @t145)))
% 0.48/0.94  (assume @p52 (forall @t156 (= (_ tptp.collec279084418od_b_b (lambda @t155 @t154)) @t151)))
% 0.48/0.94  (assume @p53 (forall (@list @t20 @t112 @t21 @t32 @t157) (=> @t116 (=> (_ (_ @t62 @t157) @t61) (_ @t115 (_ @t97 @t157))))))
% 0.48/0.94  (assume @p54 (forall (@list @t5 @t20 @t139 @t74) (= (_ @t162 @t161) (and @t160 @t159))))
% 0.48/0.94  (assume @p55 (forall (@list @t163 @t100 @t167 @t164) (= (_ @t172 @t170) (and @t169 @t166))))
% 0.48/0.94  (assume @p56 (forall (@list @t5 @t173 @t74 @t20) (=> (or (not (_ @t7 @t173)) (not @t159)) (not (_ @t162 @t174)))))
% 0.48/0.94  (assume @p57 (forall (@list @t163 @t175 @t164 @t100) (=> (or (not (_ @t168 @t175)) (not @t166)) (not (_ @t172 @t176)))))
% 0.48/0.94  (assume @p58 (forall @t181 (=> @t180 (_ @t179 @t177))))
% 0.48/0.94  (assume @p59 (forall @t186 (=> @t185 (_ @t184 @t182))))
% 0.48/0.94  (assume @p60 (forall @t190 (=> @t189 (_ @t188 @t187))))
% 0.48/0.94  (assume @p61 (forall @t193 (=> @t47 (=> @t192 (_ @t191 @t33)))))
% 0.48/0.94  (assume @p62 (forall @t193 (=> @t47 (=> @t192 (_ @t132 @t33)))))
% 0.48/0.94  (assume @p63 (forall (@list @t194 @t100 @t145) (= (_ @t197 @t177) (and (= @t194 @t100) @t196))))
% 0.48/0.94  (assume @p64 (forall (@list @t198 @t108 @t151) (= (_ @t201 @t182) (and (= @t198 @t108) @t200))))
% 0.48/0.94  (assume @p65 (forall @t202 (= (_ @t162 @t187) (and (= @t5 @t20) @t160))))
% 0.48/0.94  (assume @p66 (forall @t206 (=> @t205 (=> @t180 (_ @t204 @t177)))))
% 0.48/0.94  (assume @p67 (forall @t210 (=> @t209 (=> @t185 (_ @t208 @t182)))))
% 0.48/0.94  (assume @p68 (forall @t212 (=> @t211 (=> @t189 (_ @t121 @t187)))))
% 0.48/0.94  (assume @p69 (forall (@list @t215 @t145) (=> (_ (_ tptp.member1652792080od_b_b @t215) @t177) (not (forall @t218 (=> @t217 (not (= @t215 (_ @t214 @t213)))))))))
% 0.48/0.94  (assume @p70 (forall (@list @t221 @t151) (=> (_ (_ tptp.member1086024932od_b_b @t221) @t182) (not (forall @t224 (=> @t223 (not (= @t221 (_ @t220 @t219)))))))))
% 0.48/0.94  (assume @p71 (forall (@list @t226 @t139) (=> (_ @t228 @t187) (not (forall @t90 (=> @t227 (not (= @t226 (_ @t225 @t87)))))))))
% 0.48/0.94  (assume @p72 (forall @t232 (=> @t231 (=> @t230 (_ @t101 @t145)))))
% 0.48/0.94  (assume @p73 (forall @t236 (=> @t235 (=> @t234 (_ @t109 @t151)))))
% 0.48/0.94  (assume @p74 (forall @t241 (=> @t240 (=> @t238 (_ @t23 @t139)))))
% 0.48/0.94  (assume @p75 (forall @t232 (=> @t231 (=> @t230 @t196))))
% 0.48/0.94  (assume @p76 (forall @t236 (=> @t235 (=> @t234 @t200))))
% 0.48/0.94  (assume @p77 (forall @t241 (=> @t240 (=> @t238 @t160))))
% 0.48/0.94  (assume @p78 (forall (@list @t145 @t229 @t133) (=> @t231 (=> @t180 (_ @t179 @t229)))))
% 0.48/0.94  (assume @p79 (forall (@list @t151 @t233 @t136) (=> @t235 (=> @t185 (_ @t184 @t233)))))
% 0.48/0.94  (assume @p80 (forall (@list @t139 @t237 @t118) (=> @t240 (=> @t189 (_ @t188 @t237)))))
% 0.48/0.94  (assume @p81 (forall @t144 (_ @t239 @t187)))
% 0.48/0.94  (assume @p82 (forall (@list @t20 @t112 @t21 @t32 @t243 @t44 @t242) (=> @t116 (=> (_ (_ tptp.member1285940496od_b_b (_ @t114 @t243)) @t44) (=> (_ (_ tptp.member1285940496od_b_b (_ (_ tptp.product_Pair_b_b @t112) @t242)) @t44) (_ (_ tptp.member1285940496od_b_b (_ (_ tptp.product_Pair_b_b @t243) @t242)) (_ @t97 @t46)))))))
% 0.48/0.94  (assume @p83 (forall (@list @t244 @t32) (_ (_ tptp.mainta1604381365_nat_b (_ (_ tptp.produc1676969687_a_nat @t244) @t244)) @t32)))
% 0.48/0.94  (assume @p84 (forall (@list @t246 @t95 @t245) (=> (forall (@list @t250 @t213 @t249) (=> (_ (_ tptp.member1744485444od_b_b (_ (_ tptp.produc618266719od_b_b @t250) (_ @t214 @t249))) @t247) (=> (_ @t216 @t248) (=> (_ @t252 @t248) (_ (_ tptp.member1516365892od_b_b (_ @t251 (_ (_ tptp.product_Pair_b_b (_ @t95 @t213)) (_ @t95 @t249)))) @t245))))) (_ (_ (_ tptp.edge_p1969196346tant_a (_ (_ tptp.bNF_Gr521784954_b_b_b @t248) @t95)) @t247) @t245))))
% 0.48/0.94  (assume @p85 (forall (@list @t253 @t104 @t245) (=> (forall (@list @t250 @t219 @t256) (=> (_ (_ tptp.member147868824od_b_b (_ (_ tptp.produc1788032435od_b_b @t250) (_ @t220 @t256))) @t254) (=> (_ @t222 @t255) (=> (_ @t257 @t255) (_ (_ tptp.member1516365892od_b_b (_ @t251 (_ (_ tptp.product_Pair_b_b (_ @t104 @t219)) (_ @t104 @t256)))) @t245))))) (_ (_ (_ tptp.edge_p1817988046tant_a (_ (_ tptp.bNF_Gr492676974_b_b_b @t255) @t104)) @t254) @t245))))
% 0.48/0.94  (assume @p86 (forall (@list @t72 @t74 @t245) (=> (forall (@list @t250 @t87 @t259) (=> (_ (_ tptp.member1516365892od_b_b (_ @t251 @t261)) @t258) (=> (_ @t89 @t73) (=> (_ @t260 @t73) (_ (_ tptp.member1516365892od_b_b (_ @t251 (_ (_ tptp.product_Pair_b_b @t88) (_ @t74 @t259)))) @t245))))) (_ (_ (_ tptp.edge_p1384198690tant_a (_ (_ tptp.bNF_Gr_b_b @t73) @t74)) @t258) @t245))))
% 0.48/0.94  (assume @p87 (forall (@list @t32 @t21) (=> @t47 (=> (_ (_ tptp.mainta1604381365_nat_b (_ tptp.standa63370785tant_a @t21)) @t32) (_ (_ tptp.refl_on_b @t33) @t113)))))
% 0.48/0.94  (assume @p88 (forall @t268 (= @t267 (and @t265 @t263))))
% 0.48/0.94  (assume @p89 (forall @t277 (= @t276 (and @t273 @t270))))
% 0.48/0.94  (assume @p90 (forall (@list @t281 @t279 @t280 @t278) (= (= @t282 (_ (_ tptp.product_Pair_b_b @t280) @t278)) (and (= @t281 @t280) (= @t279 @t278)))))
% 0.48/0.94  (assume @p91 (forall (@list @t286 @t284 @t285 @t283) (= (= @t287 (_ (_ tptp.produc1432590431od_b_b @t285) @t283)) (and (= @t286 @t285) (= @t284 @t283)))))
% 0.48/0.94  (assume @p92 (forall (@list @t145 @t229 @t133 @t203) (=> @t231 (=> @t290 (and @t180 @t289)))))
% 0.48/0.94  (assume @p93 (forall (@list @t151 @t233 @t136 @t207) (=> @t235 (=> @t293 (and @t185 @t292)))))
% 0.48/0.94  (assume @p94 (forall @t296 (=> @t240 (=> @t295 (and @t189 @t294)))))
% 0.48/0.94  (assume @p95 (forall @t299 (=> @t298 (= @t158 @t297))))
% 0.48/0.94  (assume @p96 (forall @t302 (=> @t301 (= @t165 @t300))))
% 0.48/0.94  (assume @p97 (forall @t299 (=> @t298 @t160)))
% 0.48/0.94  (assume @p98 (forall @t302 (=> @t301 @t169)))
% 0.48/0.94  (assume @p99 (forall @t304 (_ (_ (_ tptp.edge_p1384198690tant_a @t44) @t303) (_ tptp.labele1741081071nt_a_b @t46))))
% 0.48/0.94  (assume @p100 (forall (@list @t314 @t310 @t305 @t312 @t307 @t311 @t306 @t308) (=> (_ (_ (_ tptp.edge_p1384198690tant_a @t314) @t310) @t305) (=> (_ (_ tptp.member1285940496od_b_b (_ @t313 @t307)) @t314) (=> (_ (_ tptp.member1285940496od_b_b (_ (_ tptp.product_Pair_b_b @t311) @t306)) @t314) (=> (_ (_ tptp.member1516365892od_b_b (_ @t309 (_ @t313 @t311))) @t310) (_ (_ tptp.member1516365892od_b_b (_ @t309 (_ (_ tptp.product_Pair_b_b @t307) @t306))) @t305)))))))
% 0.48/0.94  (assume @p101 (forall (@list @t315) (exists @t316 (= @t315 @t261))))
% 0.48/0.94  (assume @p102 (forall (@list @t320) (exists @t321 (= @t320 @t319))))
% 0.48/0.94  (assume @p103 (forall (@list @t134 @t315) (=> @t326 (_ @t134 @t315))))
% 0.48/0.94  (assume @p104 (forall (@list @t137 @t320) (=> @t332 (_ @t137 @t320))))
% 0.48/0.94  (assume @p105 (forall @t268 (=> @t267 (not (=> @t265 (not @t263))))))
% 0.48/0.94  (assume @p106 (forall @t277 (=> @t276 (not (=> @t273 (not @t270))))))
% 0.48/0.94  (assume @p107 (forall (@list @t100) (not (forall @t325 (not (= @t100 @t324))))))
% 0.48/0.94  (assume @p108 (forall @t333 (not (forall @t331 (not (= @t108 @t330))))))
% 0.48/0.94  (assume @p109 (forall (@list @t134 @t334) (=> @t326 (_ @t134 @t334))))
% 0.48/0.94  (assume @p110 (forall (@list @t137 @t335) (=> @t332 (_ @t137 @t335))))
% 0.48/0.94  (assume @p111 (forall @t333 (not (forall @t340 (not (= @t108 @t339))))))
% 0.48/0.94  (assume @p112 (forall (@list @t137 @t198) (=> (forall @t340 (_ @t137 @t339)) (_ @t137 @t198))))
% 0.48/0.94  (assume @p113 (forall (@list @t32 @t118 @t117 @t341 @t74) (=> @t47 (=> (_ @t121 (_ (_ tptp.semant55076487nt_a_b @t32) @t341)) (_ (_ tptp.member1285940496od_b_b (_ (_ tptp.product_Pair_b_b (_ @t74 @t118)) (_ @t74 @t117))) (_ (_ tptp.semant55076487nt_a_b @t77) @t341))))))
% 0.48/0.94  (assume @p114 (forall (@list @t343 @t32 @t342) (=> (forall (@list @t346) (=> (_ @t348 @t346) (_ @t347 @t346))) @t345)))
% 0.48/0.94  (assume @p115 (forall (@list @t38 @t32 @t39) (=> (forall (@list @t351) (=> (_ @t353 @t351) (_ @t352 @t351))) @t350)))
% 0.48/0.94  (assume @p116 (forall (@list @t357 @t354 @t32 @t44 @t355) (=> (_ (_ (_ tptp.graph_222606102_a_b_b @t358) @t32) @t44) (= (_ (_ (_ tptp.extens1779443913_a_b_b (_ (_ tptp.produc1569511545nt_a_b @t358) @t356)) @t32) @t44) (_ (_ (_ tptp.graph_222606102_a_b_b @t356) @t32) @t44)))))
% 0.48/0.94  (assume @p117 (forall (@list @t359 @t32 @t44) (=> (_ (_ (_ tptp.graph_222606102_a_b_b @t359) @t32) @t44) (_ (_ (_ tptp.extens1779443913_a_b_b (_ (_ tptp.produc1569511545nt_a_b @t359) @t359)) @t32) @t44))))
% 0.48/0.94  (assume @p118 (forall (@list @t38 @t39 @t44 @t118 @t117 @t341 @t264 @t262) (=> @t364 (=> @t363 (=> (_ (_ tptp.member1285940496od_b_b (_ @t119 @t264)) @t44) (=> (_ (_ tptp.member1285940496od_b_b (_ @t361 @t262)) @t44) (_ (_ tptp.member1285940496od_b_b @t266) @t360)))))))
% 0.48/0.94  (assume @p119 (forall (@list @t366 @t32 @t365) (=> (_ (_ tptp.conseq956760372_nat_b @t366) @t32) (=> (_ (_ tptp.member832397200_a_nat @t365) @t366) (_ (_ tptp.mainta1604381365_nat_b @t365) @t32)))))
% 0.48/0.94  (assume @p120 (forall @t368 (=> @t367 (=> @t363 (_ @t132 @t67)))))
% 0.48/0.94  (assume @p121 (forall @t368 (=> @t367 (=> @t363 (_ @t191 @t67)))))
% 0.48/0.94  (assume @p122 (forall (@list @t38 @t39 @t118 @t117 @t341) (=> @t71 (=> @t363 (_ @t121 @t360)))))
% 0.48/0.94  (assume @p123 (forall @t371 (=> @t345 (=> @t370 (_ @t347 @t369)))))
% 0.48/0.94  (assume @p124 (forall @t373 (=> @t350 (=> @t372 (_ @t352 @t44)))))
% 0.48/0.94  (assume @p125 (forall (@list @t374 @t32 @t376 @t375 @t44) (=> (_ (_ (_ tptp.graph_222606102_a_b_b @t374) @t32) @t376) (=> (_ (_ (_ tptp.agree_221379389_a_b_b @t375) @t44) @t376) (_ (_ (_ tptp.extens1779443913_a_b_b (_ (_ tptp.produc1569511545nt_a_b @t375) @t374)) @t32) @t44)))))
% 0.48/0.94  (assume @p126 (forall @t55 (=> @t83 (_ (_ tptp.ord_le123089219od_b_b (_ tptp.labele1741081071nt_a_b @t53)) @t377))))
% 0.48/0.94  (assume @p127 (forall @t373 (=> @t378 (=> @t367 (_ @t353 (_ (_ tptp.relcomp_b_b_b @t68) @t44))))))
% 0.48/0.94  (assume @p128 (forall @t373 (=> @t378 (=> (= @t39 (_ tptp.restri446606278nt_a_b @t39)) (_ @t380 (_ (_ tptp.relcomp_b_b_b (_ tptp.id_on_b @t379)) @t44))))))
% 0.48/0.94  (assume @p129 (forall (@list @t118 @t203 @t381 @t139) (=> @t384 (=> @t189 @t383))))
% 0.48/0.94  (assume @p130 (forall (@list @t118 @t207 @t385 @t139) (=> @t388 (=> @t189 @t387))))
% 0.48/0.94  (assume @p131 (forall (@list @t133 @t117 @t389 @t145) (=> @t391 (=> @t180 @t390))))
% 0.48/0.94  (assume @p132 (forall (@list @t133 @t203 @t229 @t145) (=> @t290 (=> @t180 @t393))))
% 0.48/0.94  (assume @p133 (forall (@list @t133 @t207 @t394 @t145) (=> @t396 (=> @t180 @t395))))
% 0.48/0.94  (assume @p134 (forall (@list @t136 @t117 @t397 @t151) (=> @t399 (=> @t185 @t398))))
% 0.48/0.94  (assume @p135 (forall (@list @t136 @t203 @t400 @t151) (=> @t402 (=> @t185 @t401))))
% 0.48/0.94  (assume @p136 (forall (@list @t136 @t207 @t233 @t151) (=> @t293 (=> @t185 @t404))))
% 0.48/0.94  (assume @p137 (forall (@list @t118 @t117 @t237 @t139) (=> @t295 (=> @t189 @t407))))
% 0.48/0.94  (assume @p138 (forall (@list @t272 @t203 @t408 @t167) (=> @t412 (=> @t411 @t410))))
% 0.48/0.94  (assume @p139 (forall (@list @t413) (= (_ @t414 tptp.bot_bot_set_b) tptp.bot_bot_set_b)))
% 0.48/0.94  (assume @p140 (forall (@list @t415) (= (_ (_ tptp.image_1749766139_a_nat @t415) tptp.bot_bot_set_b) tptp.bot_bo1836341171_a_nat)))
% 0.48/0.94  (assume @p141 (forall (@list @t416) (= (_ (_ tptp.image_924992811_nat_b @t416) tptp.bot_bo1836341171_a_nat) tptp.bot_bot_set_b)))
% 0.48/0.94  (assume @p142 (forall (@list @t417) (= (_ @t418 tptp.bot_bo1836341171_a_nat) tptp.bot_bo1836341171_a_nat)))
% 0.48/0.94  (assume @p143 (forall (@list @t419) (= (_ (_ tptp.image_b_b tptp.bot_bo1343651123od_b_b) @t419) tptp.bot_bot_set_b)))
% 0.48/0.94  (assume @p144 (forall (@list @t420) (= (_ (_ tptp.image_1971191571_a_nat tptp.bot_bo1836341171_a_nat) @t420) tptp.bot_bo2122869057_a_nat)))
% 0.48/0.94  (assume @p145 (= (_ tptp.id_on_689842066_a_nat tptp.bot_bo2122869057_a_nat) tptp.bot_bo1836341171_a_nat))
% 0.48/0.94  (assume @p146 (= (_ tptp.id_on_b tptp.bot_bot_set_b) tptp.bot_bo1343651123od_b_b))
% 0.48/0.94  (assume @p147 (= (_ tptp.id_on_1651096324_a_nat tptp.bot_bo1836341171_a_nat) tptp.bot_bo1973379891_a_nat))
% 0.48/0.94  (assume @p148 (forall (@list @t421) (= (_ (_ tptp.bNF_Gr996500706_a_nat tptp.bot_bo2122869057_a_nat) @t421) tptp.bot_bo1836341171_a_nat)))
% 0.48/0.94  (assume @p149 (forall (@list @t74) (= (_ (_ tptp.bNF_Gr_b_b tptp.bot_bot_set_b) @t74) tptp.bot_bo1343651123od_b_b)))
% 0.48/0.94  (assume @p150 (forall (@list @t63 @t426 @t423 @t424 @t422) (=> (_ @t427 @t423) (=> (_ (_ (_ tptp.graph_222606102_a_b_b @t426) @t424) @t422) (_ (_ @t425 @t424) (_ (_ tptp.relcomp_b_b_b @t423) @t422))))))
% 0.48/0.94  (assume @p151 (forall @t9 (=> (not @t432) (= (_ tptp.hilbert_Eps_b (_ tptp.p @t128)) @t128))))
% 0.48/0.94  (assume @p152 (forall (@list @t434 @t433 @t421) (= (_ (_ tptp.bNF_Gr996500706_a_nat (_ @t436 @t433)) @t421) (_ (_ tptp.insert1574423351_a_nat (_ @t435 (_ @t421 @t434))) (_ (_ tptp.bNF_Gr996500706_a_nat @t433) @t421)))))
% 0.48/0.94  (assume @p153 (forall (@list @t5 @t173 @t74) (= (_ (_ tptp.bNF_Gr_b_b (_ @t428 @t173)) @t74) (_ (_ tptp.insert1952693431od_b_b (_ @t24 @t158)) @t174))))
% 0.48/0.94  (assume @p154 (forall (@list @t163 @t175 @t164) (= (_ (_ tptp.bNF_Gr1272216980od_b_b (_ (_ tptp.insert1909710879tant_a @t163) @t175)) @t164) (_ (_ tptp.insert2037698781od_b_b (_ @t171 @t165)) @t176))))
% 0.48/0.94  (assume @p155 (forall @t304 (= (_ tptp.labele1424214014nt_a_b @t46) (_ (_ tptp.image_b_b @t44) @t33))))
% 0.48/0.94  (assume @p156 (forall (@list @t203 @t408 @t272) (= (_ @t288 (_ @t409 (_ (_ tptp.insert1909710879tant_a @t272) tptp.bot_bo1160111033tant_a))) @t412)))
% 0.48/0.94  (assume @p157 (forall (@list @t203 @t381 @t118) (= (_ @t288 (_ @t382 @t438)) @t384)))
% 0.48/0.94  (assume @p158 (forall (@list @t207 @t385 @t118) (= (_ @t291 (_ @t386 @t438)) @t388)))
% 0.48/0.94  (assume @p159 (forall (@list @t117 @t237 @t118) (= (_ @t191 @t439) @t295)))
% 0.48/0.94  (assume @p160 (forall (@list @t117 @t440 @t441) (= (_ @t191 (_ (_ tptp.image_924992811_nat_b @t440) @t443)) (_ (_ tptp.member1544800936_nat_b (_ (_ tptp.produc2059954415_nat_b @t441) @t117)) @t440))))
% 0.48/0.94  (assume @p161 (forall (@list @t203 @t444 @t441) (= (_ @t288 (_ (_ tptp.image_1214223635od_b_b @t444) @t443)) (_ (_ tptp.member301892752od_b_b (_ (_ tptp.produc590959831od_b_b @t441) @t203)) @t444))))
% 0.48/0.94  (assume @p162 (forall (@list @t207 @t445 @t441) (= (_ @t291 (_ (_ tptp.image_480774529od_b_b @t445) @t443)) (_ (_ tptp.member1533761242od_b_b (_ (_ tptp.produc401731773od_b_b @t441) @t207)) @t445))))
% 0.48/0.94  (assume @p163 (forall (@list @t5 @t32 @t447 @t20 @t446) (=> @t448 (=> (_ (_ tptp.member1285940496od_b_b (_ (_ tptp.product_Pair_b_b (_ @t447 @t5)) @t20)) @t446) (_ @t162 (_ (_ tptp.relcomp_b_b_b (_ @t75 @t447)) @t446))))))
% 0.48/0.94  (assume @p164 (forall (@list @t5 @t32 @t450 @t100 @t449) (=> @t448 (=> (_ (_ tptp.member1516365892od_b_b (_ (_ tptp.produc1432590431od_b_b (_ @t450 @t5)) @t100)) @t449) (_ (_ tptp.member641857272od_b_b (_ (_ tptp.produc1257047359od_b_b @t5) @t100)) (_ (_ tptp.relcom112561144od_b_b (_ (_ tptp.bNF_Gr230160332tant_a @t33) @t450)) @t449))))))
% 0.48/0.94  (assume @p165 (forall (@list @t32 @t451) (= (_ (_ (_ tptp.graph_726202286_nat_b (_ (_ tptp.labele27098724_a_nat tptp.bot_bo1653310327_a_nat) tptp.bot_bo1836341171_a_nat)) @t32) @t451) (and (= @t451 tptp.bot_bo1113554635_nat_b) @t47))))
% 0.48/0.94  (assume @p166 (forall @t48 (= (_ (_ (_ tptp.graph_222606102_a_b_b (_ @t452 tptp.bot_bot_set_b)) @t32) @t44) (and (= @t44 tptp.bot_bo1343651123od_b_b) @t47))))
% 0.48/0.94  (assume @p167 (forall @t55 (=> @t454 (=> @t453 @t79))))
% 0.48/0.94  (assume @p168 (forall (@list @t272 @t117 @t455) (= @t459 (_ tptp.restri446606278nt_a_b @t459))))
% 0.48/0.94  (assume @p169 @t462)
% 0.48/0.94  (assume @p170 (forall (@list @t434) (_ (_ tptp.refl_o1031343860_a_nat (_ @t436 tptp.bot_bo2122869057_a_nat)) (_ (_ tptp.insert1574423351_a_nat (_ @t435 @t434)) tptp.bot_bo1836341171_a_nat))))
% 0.48/0.94  (assume @p171 (forall @t9 (_ (_ tptp.refl_on_b @t429) (_ (_ tptp.insert1952693431od_b_b @t26) tptp.bot_bo1343651123od_b_b))))
% 0.48/0.94  (assume @p172 (forall (@list @t463) (_ (_ tptp.refl_o1213627494_a_nat (_ @t464 tptp.bot_bo1836341171_a_nat)) (_ (_ tptp.insert1810136247_a_nat (_ (_ tptp.produc1677124439_a_nat @t463) @t463)) tptp.bot_bo1973379891_a_nat))))
% 0.48/0.94  (assume @p173 (forall (@list @t118 @t139 @t203 @t381) (=> @t189 (=> @t384 @t383))))
% 0.48/0.94  (assume @p174 (forall (@list @t118 @t139 @t207 @t385) (=> @t189 (=> @t388 @t387))))
% 0.48/0.94  (assume @p175 (forall (@list @t133 @t145 @t117 @t389) (=> @t180 (=> @t391 @t390))))
% 0.48/0.94  (assume @p176 (forall (@list @t133 @t145 @t203 @t229) (=> @t180 (=> @t290 @t393))))
% 0.48/0.94  (assume @p177 (forall (@list @t133 @t145 @t207 @t394) (=> @t180 (=> @t396 @t395))))
% 0.48/0.94  (assume @p178 (forall (@list @t136 @t151 @t117 @t397) (=> @t185 (=> @t399 @t398))))
% 0.48/0.94  (assume @p179 (forall (@list @t136 @t151 @t203 @t400) (=> @t185 (=> @t402 @t401))))
% 0.48/0.94  (assume @p180 (forall (@list @t136 @t151 @t207 @t233) (=> @t185 (=> @t293 @t404))))
% 0.48/0.94  (assume @p181 (forall (@list @t118 @t139 @t117 @t237) (=> @t189 (=> @t295 @t407))))
% 0.48/0.94  (assume @p182 (forall (@list @t272 @t167 @t203 @t408) (=> @t411 (=> @t412 @t410))))
% 0.48/0.94  (assume @p183 (forall @t466 (= @t407 (exists @t143 (and @t142 (_ (_ tptp.member1285940496od_b_b (_ @t465 @t117)) @t237))))))
% 0.48/0.94  (assume @p184 (forall @t468 (= @t410 (exists (@list @t467) (and (_ (_ tptp.member1632892294tant_a @t467) @t167) (_ (_ tptp.member1516365892od_b_b (_ (_ tptp.produc1432590431od_b_b @t467) @t203)) @t408))))))
% 0.48/0.94  (assume @p185 (forall (@list @t117 @t389 @t145) (=> @t390 (not (forall @t218 (=> (_ (_ tptp.member351494440_b_b_b (_ (_ tptp.produc1001682799_b_b_b @t213) @t117)) @t389) @t469))))))
% 0.48/0.94  (assume @p186 (forall (@list @t117 @t397 @t151) (=> @t398 (not (forall @t224 (=> (_ (_ tptp.member1417789726_b_b_b (_ (_ tptp.produc1580777273_b_b_b @t219) @t117)) @t397) @t470))))))
% 0.48/0.94  (assume @p187 (forall (@list @t203 @t381 @t139) (=> @t383 (not (forall @t90 (=> (_ (_ tptp.member641857272od_b_b (_ (_ tptp.produc1257047359od_b_b @t87) @t203)) @t381) @t471))))))
% 0.48/0.94  (assume @p188 (forall (@list @t203 @t229 @t145) (=> @t393 (not (forall @t218 (=> (_ (_ tptp.member1652792080od_b_b (_ @t214 @t203)) @t229) @t469))))))
% 0.48/0.94  (assume @p189 (forall (@list @t203 @t400 @t151) (=> @t401 (not (forall @t224 (=> (_ (_ tptp.member942707974od_b_b (_ (_ tptp.produc1597690145od_b_b @t219) @t203)) @t400) @t470))))))
% 0.48/0.94  (assume @p190 (forall (@list @t207 @t385 @t139) (=> @t387 (not (forall @t90 (=> (_ (_ tptp.member599505522od_b_b (_ (_ tptp.produc800495189od_b_b @t87) @t207)) @t385) @t471))))))
% 0.48/0.94  (assume @p191 (forall (@list @t207 @t394 @t145) (=> @t395 (not (forall @t218 (=> (_ (_ tptp.member4694106od_b_b (_ (_ tptp.produc732676669od_b_b @t213) @t207)) @t394) @t469))))))
% 0.48/0.94  (assume @p192 (forall (@list @t207 @t233 @t151) (=> @t404 (not (forall @t224 (=> (_ (_ tptp.member1086024932od_b_b (_ @t220 @t207)) @t233) @t470))))))
% 0.48/0.94  (assume @p193 (forall @t466 (=> @t407 (not (forall @t90 (=> (_ (_ tptp.member1285940496od_b_b (_ @t225 @t117)) @t237) @t471))))))
% 0.48/0.94  (assume @p194 (forall @t468 (=> @t410 (not (forall (@list @t317) (=> (_ (_ tptp.member1516365892od_b_b (_ @t318 @t203)) @t408) (not (_ (_ tptp.member1632892294tant_a @t317) @t167))))))))
% 0.48/0.94  (assume @p195 (forall (@list @t272 @t477 @t473 @t226 @t472) (=> (_ (_ tptp.member1214736488tant_a (_ @t478 @t477)) @t473) (=> (_ (_ tptp.member1516365892od_b_b (_ (_ tptp.produc1432590431od_b_b @t477) @t226)) @t472) @t476))))
% 0.48/0.94  (assume @p196 (forall (@list @t118 @t117 @t237 @t455 @t479) (=> @t295 (=> (_ (_ tptp.member1285940496od_b_b @t458) @t479) @t481))))
% 0.48/0.94  (assume @p197 (forall (@list @t272 @t203 @t408 @t226 @t482) (=> @t412 (=> (_ (_ tptp.member1652792080od_b_b (_ (_ tptp.produc546497367od_b_b @t203) @t226)) @t482) @t484))))
% 0.48/0.94  (assume @p198 (forall (@list @t281 @t279 @t237 @t479 @t485) (=> (_ (_ tptp.member1285940496od_b_b @t282) @t480) (=> (forall (@list @t323 @t322 @t336) (=> (_ (_ tptp.member1285940496od_b_b @t324) @t237) (=> (_ (_ tptp.member1285940496od_b_b @t338) @t479) (_ (_ @t485 @t323) @t336)))) (_ (_ @t485 @t281) @t279)))))
% 0.48/0.94  (assume @p199 (forall (@list @t286 @t284 @t473 @t472 @t486) (=> (_ @t492 @t474) (=> (forall (@list @t328 @t490 @t488) (=> (_ (_ tptp.member1214736488tant_a (_ (_ tptp.produc342647tant_a @t328) @t490)) @t473) (=> (_ (_ tptp.member1516365892od_b_b (_ @t491 @t488)) @t472) @t489))) @t487))))
% 0.48/0.94  (assume @p200 (forall (@list @t286 @t284 @t408 @t482 @t486) (=> (_ @t492 @t483) (=> (forall (@list @t328 @t327 @t488) (=> (_ (_ tptp.member1516365892od_b_b @t330) @t408) (=> (_ (_ tptp.member1652792080od_b_b (_ @t493 @t488)) @t482) @t489))) @t487))))
% 0.48/0.94  (assume @p201 (forall @t500 (= @t499 (exists (@list @t496 @t495 @t494) (and (= @t497 @t496) (= @t127 @t494) (_ (_ tptp.member1285940496od_b_b (_ (_ tptp.product_Pair_b_b @t496) @t495)) @t237) (_ (_ tptp.member1285940496od_b_b (_ (_ tptp.product_Pair_b_b @t495) @t494)) @t479))))))
% 0.48/0.94  (assume @p202 (forall @t510 (= @t509 (exists (@list @t503 @t502 @t501) (and @t506 @t504 (_ (_ tptp.member1214736488tant_a (_ (_ tptp.produc342647tant_a @t503) @t502)) @t473) (_ (_ tptp.member1516365892od_b_b (_ (_ tptp.produc1432590431od_b_b @t502) @t501)) @t472))))))
% 0.48/0.94  (assume @p203 (forall @t513 (= @t512 (exists (@list @t503 @t511 @t501) (and @t506 @t504 (_ (_ tptp.member1516365892od_b_b (_ (_ tptp.produc1432590431od_b_b @t503) @t511)) @t408) (_ (_ tptp.member1652792080od_b_b (_ (_ tptp.produc546497367od_b_b @t511) @t501)) @t482))))))
% 0.48/0.94  (assume @p204 (forall @t500 (=> @t499 (not (forall @t514 (=> (_ (_ tptp.member1285940496od_b_b (_ @t498 @t322)) @t237) (not (_ (_ tptp.member1285940496od_b_b (_ @t337 @t127)) @t479))))))))
% 0.48/0.94  (assume @p205 (forall @t510 (=> @t509 (not (forall @t515 (=> (_ (_ tptp.member1214736488tant_a (_ (_ tptp.produc342647tant_a @t505) @t490)) @t473) (not (_ (_ tptp.member1516365892od_b_b (_ @t491 @t123)) @t472))))))))
% 0.48/0.94  (assume @p206 (forall @t513 (=> @t512 (not (forall @t516 (=> (_ (_ tptp.member1516365892od_b_b (_ @t507 @t327)) @t408) (not (_ (_ tptp.member1652792080od_b_b (_ @t493 @t123)) @t482))))))))
% 0.48/0.94  (assume @p207 (forall (@list @t118 @t455 @t237 @t479) (=> @t481 (not (forall @t514 (=> (_ (_ tptp.member1285940496od_b_b (_ @t119 @t322)) @t237) (not (_ (_ tptp.member1285940496od_b_b (_ @t337 @t455)) @t479))))))))
% 0.48/0.94  (assume @p208 (forall (@list @t272 @t226 @t473 @t472) (=> @t476 (not (forall @t515 (=> (_ (_ tptp.member1214736488tant_a (_ @t478 @t490)) @t473) (not (_ (_ tptp.member1516365892od_b_b (_ @t491 @t226)) @t472))))))))
% 0.48/0.94  (assume @p209 (forall (@list @t272 @t226 @t408 @t482) (=> @t484 (not (forall @t516 (=> (_ (_ tptp.member1516365892od_b_b (_ @t274 @t327)) @t408) (not (_ (_ tptp.member1652792080od_b_b (_ @t493 @t226)) @t482))))))))
% 0.48/0.94  (assume @p210 (forall (@list @t520 @t237 @t479) (=> (_ (_ tptp.member1285940496od_b_b @t520) @t480) (not (forall (@list @t87 @t259 @t517) (=> (= @t520 (_ @t225 @t517)) (=> @t519 (not (_ (_ tptp.member1285940496od_b_b (_ (_ tptp.product_Pair_b_b @t259) @t517)) @t479)))))))))
% 0.48/0.94  (assume @p211 (forall (@list @t523 @t473 @t472) (=> (_ @t525 @t474) (not (forall (@list @t317 @t522 @t521) (=> @t524 (=> (_ (_ tptp.member1214736488tant_a (_ (_ tptp.produc342647tant_a @t317) @t522)) @t473) (not (_ (_ tptp.member1516365892od_b_b (_ (_ tptp.produc1432590431od_b_b @t522) @t521)) @t472)))))))))
% 0.48/0.94  (assume @p212 (forall (@list @t523 @t408 @t482) (=> (_ @t525 @t483) (not (forall (@list @t317 @t249 @t521) (=> @t524 (=> @t527 (not (_ (_ tptp.member1652792080od_b_b (_ (_ tptp.produc546497367od_b_b @t249) @t521)) @t482)))))))))
% 0.48/0.94  (assume @p213 (forall (@list @t529 @t530 @t528) (= (_ (_ tptp.image_b_b (_ (_ tptp.relcomp_b_b_b @t529) @t530)) @t528) (_ (_ tptp.image_b_b @t530) (_ (_ tptp.image_b_b @t529) @t528)))))
% 0.48/0.94  (assume @p214 (forall (@list @t532 @t237 @t531 @t139) (=> (_ (_ tptp.ord_le1036320359od_b_b @t532) @t237) (=> (_ (_ tptp.ord_less_eq_set_b @t531) @t139) (_ (_ tptp.ord_less_eq_set_b (_ (_ tptp.image_b_b @t532) @t531)) @t406)))))
% 0.48/0.94  (assume @p215 (_ (_ tptp.refl_o1031343860_a_nat tptp.bot_bo2122869057_a_nat) tptp.bot_bo1836341171_a_nat))
% 0.48/0.94  (assume @p216 (_ (_ tptp.refl_on_b tptp.bot_bot_set_b) tptp.bot_bo1343651123od_b_b))
% 0.48/0.94  (assume @p217 (_ (_ tptp.refl_o1213627494_a_nat tptp.bot_bo1836341171_a_nat) tptp.bot_bo1973379891_a_nat))
% 0.48/0.94  (assume @p218 (forall (@list @t237 @t479) (=> (forall @t316 (=> @t519 (_ @t518 @t479))) (_ (_ tptp.ord_le1036320359od_b_b @t237) @t479))))
% 0.48/0.94  (assume @p219 (forall (@list @t408 @t472) (=> (forall @t321 (=> @t527 (_ @t526 @t472))) (_ (_ tptp.ord_le123089219od_b_b @t408) @t472))))
% 0.48/0.94  (assume @p220 (forall @t55 (= @t79 (and @t454 @t453))))
% 0.48/0.94  (assume @p221 (forall @t35 (=> (_ (_ tptp.ord_le123089219od_b_b @t303) (_ tptp.labele1741081071nt_a_b @t34)) @t47)))
% 0.48/0.94  (assume @p222 (forall @t55 (=> @t54 (=> @t52 (= @t83 (and @t453 @t454))))))
% 0.48/0.94  (assume @p223 (forall @t55 (=> @t83 @t453)))
% 0.48/0.94  (assume @p224 (forall @t371 (=> @t345 (=> @t370 (not (forall (@list @t533) (=> (_ (_ (_ tptp.graph_714568023_nat_b @t342) @t32) @t533) (not (_ (_ tptp.ord_le1484132922_nat_b @t369) @t533)))))))))
% 0.48/0.94  (assume @p225 (forall @t373 (=> @t350 (=> @t372 (not (forall (@list @t534) (=> (_ @t380 @t534) (not (_ (_ tptp.ord_le1036320359od_b_b @t44) @t534)))))))))
% 0.48/0.94  (assume @p226 (forall @t540 (=> @t539 (=> @t538 (_ @t537 (_ (_ tptp.relcomp_b_b_b @t44) (_ tptp.id_on_b (_ tptp.labele1424214014nt_a_b @t426))))))))
% 0.48/0.94  (assume @p227 (forall @t540 (=> @t539 (=> @t538 (_ @t537 (_ (_ tptp.relcomp_b_b_b @t64) @t44))))))
% 0.48/0.94  (assume @p228 (forall (@list @t38 @t39 @t413 @t74) (=> (_ @t70 @t413) (_ (_ @t69 (_ (_ tptp.map_gr926947118tant_a @t541) @t39)) (_ (_ tptp.relcomp_b_b_b @t413) @t541)))))
% 0.48/0.94  (assume @p229 (forall (@list @t117 @t118 @t139) (= (= @t542 @t545) @t544)))
% 0.48/0.94  (assume @p230 (forall (@list @t546 @t441 @t549) (= (= @t548 @t553) @t552)))
% 0.48/0.94  (assume @p231 (forall (@list @t118 @t139 @t117) (= (= @t545 @t542) @t544)))
% 0.48/0.94  (assume @p232 (forall (@list @t441 @t549 @t546) (= (= @t553 @t548) @t552)))
% 0.48/0.94  (assume @p233 (forall @t296 (=> @t556 (=> @t295 (_ (_ tptp.ord_less_eq_set_b @t439) @t554)))))
% 0.48/0.94  (assume @p234 (forall (@list @t549 @t557 @t441 @t546) (=> @t563 (=> @t561 (_ (_ tptp.ord_le1718765799_a_nat @t560) @t559)))))
% 0.48/0.94  (assume @p235 (forall (@list @t145 @t229 @t203 @t133) (=> (_ (_ tptp.equiv_1125628061od_b_b @t145) @t229) (=> (_ (_ tptp.ord_le1036320359od_b_b (_ @t392 (_ @t566 tptp.bot_bo1343651123od_b_b))) (_ @t392 @t565)) (=> @t289 @t290)))))
% 0.48/0.94  (assume @p236 (forall (@list @t151 @t233 @t207 @t136) (=> (_ (_ tptp.equiv_2048442231od_b_b @t151) @t233) (=> (_ (_ tptp.ord_le123089219od_b_b (_ @t403 (_ @t569 tptp.bot_bo1664927607od_b_b))) (_ @t403 @t568)) (=> @t292 @t293)))))
% 0.48/0.94  (assume @p237 (forall (@list @t139 @t237 @t117 @t118) (=> @t556 (=> (_ (_ tptp.ord_less_eq_set_b @t554) @t439) (=> @t294 @t295)))))
% 0.48/0.94  (assume @p238 (forall (@list @t549 @t557 @t546 @t441) (=> @t563 (=> (_ (_ tptp.ord_le1718765799_a_nat @t559) @t560) (=> (_ @t570 @t549) @t561)))))
% 0.48/0.94  (assume @p239 (forall (@list @t413 @t571 @t139 @t118) (=> (_ (_ tptp.ord_le1036320359od_b_b @t413) @t571) (=> (_ @t555 @t413) (=> (_ @t555 @t571) (= (_ @t572 (_ @t414 @t438)) (_ @t572 @t438)))))))
% 0.48/0.94  (assume @p240 (forall (@list @t417 @t573 @t549 @t441) (=> (_ (_ tptp.ord_le107617383_a_nat @t417) @t573) (=> (_ @t562 @t417) (=> (_ @t562 @t573) (= (_ @t574 (_ @t418 @t443)) (_ @t574 @t443)))))))
% 0.48/0.94  (assume @p241 (forall @t576 (= (= tptp.bot_bot_set_b @t131) @t575)))
% 0.48/0.94  (assume @p242 (forall @t582 (= (= tptp.bot_bo1836341171_a_nat @t581) @t580)))
% 0.48/0.94  (assume @p243 (forall @t576 (= (= @t131 tptp.bot_bot_set_b) @t575)))
% 0.48/0.94  (assume @p244 (forall @t582 (= (= @t581 tptp.bot_bo1836341171_a_nat) @t580)))
% 0.48/0.94  (assume @p245 (forall @t150 (= (forall @t149 (not @t148)) @t583)))
% 0.48/0.94  (assume @p246 (forall @t156 (= (forall @t155 (not @t154)) @t584)))
% 0.48/0.94  (assume @p247 (forall @t144 (= (forall @t143 (not @t142)) @t585)))
% 0.48/0.94  (assume @p248 (forall @t588 (= (forall @t579 (not @t587)) @t586)))
% 0.48/0.94  (assume @p249 (forall (@list @t226) (not (_ @t228 tptp.bot_bo1343651123od_b_b))))
% 0.48/0.94  (assume @p250 (forall (@list @t589) (not (_ @t590 tptp.bot_bo1664927607od_b_b))))
% 0.48/0.94  (assume @p251 (forall (@list @t455) (not (_ @t591 tptp.bot_bot_set_b))))
% 0.48/0.94  (assume @p252 (forall (@list @t592) (not (_ (_ tptp.member832397200_a_nat @t592) tptp.bot_bo1836341171_a_nat))))
% 0.48/0.94  (assume @p253 (forall (@list @t139 @t593) (=> (forall @t90 (=> @t227 (_ @t89 @t593))) @t594)))
% 0.48/0.94  (assume @p254 (forall (@list @t145 @t595) (=> (forall @t218 (=> @t217 (_ @t216 @t595))) @t596)))
% 0.48/0.94  (assume @p255 (forall (@list @t151 @t597) (=> (forall @t224 (=> @t223 (_ @t222 @t597))) @t598)))
% 0.48/0.94  (assume @p256 (forall @t600 (= (_ @t428 @t599) @t599)))
% 0.48/0.94  (assume @p257 (forall @t602 (= (_ @t464 @t601) @t601)))
% 0.48/0.94  (assume @p258 (forall @t606 (= @t605 (or @t551 @t604))))
% 0.48/0.94  (assume @p259 (forall @t212 (= @t607 (or @t211 @t189))))
% 0.48/0.94  (assume @p260 (forall @t206 (= @t608 (or @t205 @t180))))
% 0.48/0.94  (assume @p261 (forall @t210 (= @t609 (or @t209 @t185))))
% 0.48/0.94  (assume @p262 (forall @t614 (=> (=> (not @t613) @t551) @t612)))
% 0.48/0.94  (assume @p263 (forall @t618 (=> (=> (not @t617) @t211) @t616)))
% 0.48/0.94  (assume @p264 (forall @t622 (=> (=> (not @t621) @t205) @t620)))
% 0.48/0.94  (assume @p265 (forall @t626 (=> (=> (not @t625) @t209) @t624)))
% 0.48/0.94  (assume @p266 (forall @t144 (_ (_ tptp.ord_less_eq_set_b tptp.bot_bot_set_b) @t139)))
% 0.48/0.94  (assume @p267 (forall @t588 (_ (_ tptp.ord_le1718765799_a_nat tptp.bot_bo1836341171_a_nat) @t549)))
% 0.48/0.94  (assume @p268 (forall @t144 (= (_ @t543 tptp.bot_bot_set_b) @t585)))
% 0.48/0.94  (assume @p269 (forall @t588 (= (_ @t550 tptp.bot_bo1836341171_a_nat) @t586)))
% 0.48/0.94  (assume @p270 (forall @t627 (_ @t135 @t565)))
% 0.48/0.94  (assume @p271 (forall @t628 (_ @t138 @t568)))
% 0.48/0.94  (assume @p272 (forall @t629 (_ @t132 @t438)))
% 0.48/0.94  (assume @p273 (forall @t630 (_ @t603 @t443)))
% 0.48/0.94  (assume @p274 (forall @t633 (= (_ (_ tptp.ord_le1718765799_a_nat @t601) @t610) (and @t632 (_ @t550 @t610)))))
% 0.48/0.94  (assume @p275 (forall @t635 (= (_ (_ tptp.ord_less_eq_set_b @t599) @t593) (and @t634 @t594))))
% 0.48/0.94  (assume @p276 (forall @t639 (= (_ (_ tptp.ord_le1036320359od_b_b @t638) @t595) (and @t636 @t596))))
% 0.48/0.94  (assume @p277 (forall @t643 (= (_ (_ tptp.ord_le123089219od_b_b @t642) @t597) (and @t640 @t598))))
% 0.48/0.94  (assume @p278 (forall @t645 (= (_ (_ tptp.relcom1338300020_a_nat tptp.bot_bo1836341171_a_nat) @t644) tptp.bot_bo1836341171_a_nat)))
% 0.48/0.94  (assume @p279 (forall @t645 (= (_ (_ tptp.relcom1338300020_a_nat @t644) tptp.bot_bo1836341171_a_nat) tptp.bot_bo1836341171_a_nat)))
% 0.48/0.94  (assume @p280 (forall (@list @t354) (= @t646 (_ tptp.restri446606278nt_a_b @t646))))
% 0.48/0.94  (assume @p281 (forall (@list @t38 @t39 @t44 @t341) (=> @t364 (=> (not (= @t362 tptp.bot_bo1343651123od_b_b)) (not (= @t360 tptp.bot_bo1343651123od_b_b))))))
% 0.48/0.94  (assume @p282 (forall @t150 (= (exists @t149 @t148) (not @t583))))
% 0.48/0.94  (assume @p283 (forall @t156 (= (exists @t155 @t154) (not @t584))))
% 0.48/0.94  (assume @p284 (forall @t144 (= (exists @t143 @t142) (not @t585))))
% 0.48/0.94  (assume @p285 (forall @t588 (= (exists @t579 @t587) (not @t586))))
% 0.48/0.94  (assume @p286 (forall @t150 (=> (forall (@list @t249) (not (_ @t252 @t145))) @t583)))
% 0.48/0.94  (assume @p287 (forall @t156 (=> (forall (@list @t256) (not (_ @t257 @t151))) @t584)))
% 0.48/0.94  (assume @p288 (forall @t144 (=> (forall (@list @t259) (not (_ @t260 @t139))) @t585)))
% 0.48/0.94  (assume @p289 (forall @t588 (=> (forall (@list @t647) (not (_ (_ tptp.member832397200_a_nat @t647) @t549))) @t586)))
% 0.48/0.94  (assume @p290 (forall (@list @t145 @t133) (=> @t583 @t648)))
% 0.48/0.94  (assume @p291 (forall (@list @t151 @t136) (=> @t584 @t649)))
% 0.48/0.94  (assume @p292 (forall (@list @t139 @t118) (=> @t585 @t650)))
% 0.48/0.94  (assume @p293 (forall (@list @t549 @t441) (=> @t586 @t651)))
% 0.48/0.94  (assume @p294 (forall @t627 (not (_ @t135 tptp.bot_bo1343651123od_b_b))))
% 0.48/0.94  (assume @p295 (forall @t628 (not (_ @t138 tptp.bot_bo1664927607od_b_b))))
% 0.48/0.94  (assume @p296 (forall @t629 (not (_ @t132 tptp.bot_bot_set_b))))
% 0.48/0.94  (assume @p297 (forall @t630 (not (_ @t603 tptp.bot_bo1836341171_a_nat))))
% 0.48/0.94  (assume @p298 (= tptp.ord_less_eq_set_b (lambda @t654 (forall @t143 (=> (_ @t141 @t653) (_ @t141 @t652))))))
% 0.48/0.94  (assume @p299 (= tptp.ord_le1036320359od_b_b (lambda @t657 (forall @t149 (=> (_ @t147 @t656) (_ @t147 @t655))))))
% 0.48/0.94  (assume @p300 (= tptp.ord_le123089219od_b_b (lambda @t660 (forall @t155 (=> (_ @t153 @t659) (_ @t153 @t658))))))
% 0.48/0.94  (assume @p301 (forall (@list @t139 @t593 @t455) (=> @t594 (=> (_ @t591 @t139) (_ @t591 @t593)))))
% 0.48/0.94  (assume @p302 (forall (@list @t145 @t595 @t226) (=> @t596 (=> (_ @t228 @t145) (_ @t228 @t595)))))
% 0.48/0.94  (assume @p303 (forall (@list @t151 @t597 @t589) (=> @t598 (=> (_ @t590 @t151) (_ @t590 @t597)))))
% 0.48/0.94  (assume @p304 (forall (@list @t139 @t593 @t5) (=> @t594 (=> @t160 @t634))))
% 0.48/0.94  (assume @p305 (forall (@list @t145 @t595 @t194) (=> @t596 (=> @t196 @t636))))
% 0.48/0.94  (assume @p306 (forall (@list @t151 @t597 @t198) (=> @t598 (=> @t200 @t640))))
% 0.48/0.94  (assume @p307 (forall @t663 (=> @t604 (exists @t662 (and (= @t549 (_ @t442 @t661)) (not (_ @t603 @t661)))))))
% 0.48/0.94  (assume @p308 (forall @t190 (=> @t189 (exists @t665 (and (= @t139 (_ @t437 @t664)) (not (_ @t132 @t664)))))))
% 0.48/0.94  (assume @p309 (forall @t181 (=> @t180 (exists @t667 (and (= @t145 (_ @t564 @t666)) (not (_ @t135 @t666)))))))
% 0.48/0.94  (assume @p310 (forall @t186 (=> @t185 (exists @t669 (and (= @t151 (_ @t567 @t668)) (not (_ @t138 @t668)))))))
% 0.48/0.94  (assume @p311 (forall @t202 (= (_ @t428 (_ @t670 @t139)) (_ @t670 @t599))))
% 0.48/0.94  (assume @p312 (forall (@list @t463 @t671 @t549) (= (_ @t464 (_ @t672 @t549)) (_ @t672 @t601))))
% 0.48/0.94  (assume @p313 (forall (@list @t441 @t549 @t546 @t610) (=> @t651 (=> (not (_ @t570 @t610)) (= (= @t553 @t611) (and (=> @t551 @t675) (=> @t674 (exists (@list @t673) (and (= @t549 (_ @t547 @t673)) (not (_ @t570 @t673)) (= @t610 (_ @t442 @t673)) (not (_ @t603 @t673)))))))))))
% 0.48/0.94  (assume @p314 (forall (@list @t118 @t139 @t117 @t593) (=> @t650 (=> (not (_ @t191 @t593)) (= (= @t545 @t615) (and (=> @t211 @t678) (=> @t677 (exists (@list @t676) (and (= @t139 (_ @t457 @t676)) (not (_ @t191 @t676)) (= @t593 (_ @t437 @t676)) (not (_ @t132 @t676)))))))))))
% 0.48/0.94  (assume @p315 (forall (@list @t133 @t145 @t203 @t595) (=> @t648 (=> (not (_ @t288 @t595)) (= (= @t682 @t619) (and (=> @t205 @t681) (=> @t680 (exists (@list @t679) (and (= @t145 (_ @t566 @t679)) (not (_ @t288 @t679)) (= @t595 (_ @t564 @t679)) (not (_ @t135 @t679)))))))))))
% 0.48/0.94  (assume @p316 (forall (@list @t136 @t151 @t207 @t597) (=> @t649 (=> (not (_ @t291 @t597)) (= (= @t686 @t623) (and (=> @t209 @t685) (=> @t684 (exists (@list @t683) (and (= @t151 (_ @t569 @t683)) (not (_ @t291 @t683)) (= @t597 (_ @t567 @t683)) (not (_ @t138 @t683)))))))))))
% 0.48/0.94  (assume @p317 (forall @t663 (=> @t604 (= @t553 @t549))))
% 0.48/0.94  (assume @p318 (forall @t190 (=> @t189 (= @t545 @t139))))
% 0.48/0.94  (assume @p319 (forall @t181 (=> @t180 (= @t682 @t145))))
% 0.48/0.94  (assume @p320 (forall @t186 (=> @t185 (= @t686 @t151))))
% 0.48/0.94  (assume @p321 (forall @t633 (=> (not @t687) (=> (not @t632) (= (= @t601 (_ @t464 @t610)) @t675)))))
% 0.48/0.94  (assume @p322 (forall @t635 (=> (not @t160) (=> (not @t634) (= (= @t599 (_ @t428 @t593)) @t678)))))
% 0.48/0.94  (assume @p323 (forall @t639 (=> (not @t196) (=> (not @t636) (= (= @t638 (_ @t637 @t595)) @t681)))))
% 0.48/0.94  (assume @p324 (forall @t643 (=> (not @t200) (=> (not @t640) (= (= @t642 (_ @t641 @t597)) @t685)))))
% 0.48/0.94  (assume @p325 (forall @t602 (=> @t687 (not (forall @t662 (=> (= @t549 (_ @t464 @t661)) (_ @t631 @t661)))))))
% 0.48/0.94  (assume @p326 (forall @t600 (=> @t160 (not (forall @t665 (=> (= @t139 (_ @t428 @t664)) (_ @t7 @t664)))))))
% 0.48/0.94  (assume @p327 (forall (@list @t194 @t145) (=> @t196 (not (forall @t667 (=> (= @t145 (_ @t637 @t666)) (_ @t195 @t666)))))))
% 0.48/0.94  (assume @p328 (forall (@list @t198 @t151) (=> @t200 (not (forall @t669 (=> (= @t151 (_ @t641 @t668)) (_ @t199 @t668)))))))
% 0.48/0.94  (assume @p329 (forall @t614 (=> @t613 @t612)))
% 0.48/0.94  (assume @p330 (forall @t618 (=> @t617 @t616)))
% 0.48/0.94  (assume @p331 (forall @t622 (=> @t621 @t620)))
% 0.48/0.94  (assume @p332 (forall @t626 (=> @t625 @t624)))
% 0.48/0.94  (assume @p333 (forall (@list @t441 @t610) (_ @t603 (_ @t442 @t610))))
% 0.48/0.94  (assume @p334 (forall (@list @t118 @t593) (_ @t132 (_ @t437 @t593))))
% 0.48/0.94  (assume @p335 (forall (@list @t133 @t595) (_ @t135 (_ @t564 @t595))))
% 0.48/0.94  (assume @p336 (forall (@list @t136 @t597) (_ @t138 (_ @t567 @t597))))
% 0.48/0.94  (assume @p337 (forall @t606 (=> @t605 (=> @t674 @t604))))
% 0.48/0.94  (assume @p338 (forall @t212 (=> @t607 (=> @t677 @t189))))
% 0.48/0.94  (assume @p339 (forall @t206 (=> @t608 (=> @t680 @t180))))
% 0.48/0.94  (assume @p340 (forall @t210 (=> @t609 (=> @t684 @t185))))
% 0.48/0.94  (assume @p341 (forall (@list @t118 @t117) (=> (= @t438 @t542) @t211)))
% 0.48/0.94  (assume @p342 (forall (@list @t441 @t546) (=> (= @t443 @t548) @t551)))
% 0.48/0.94  (assume @p343 (forall @t190 (not (= @t545 tptp.bot_bot_set_b))))
% 0.48/0.94  (assume @p344 (forall @t663 (not (= @t553 tptp.bot_bo1836341171_a_nat))))
% 0.48/0.94  (assume @p345 (forall (@list @t118 @t117 @t455 @t688) (= (= (_ @t437 @t542) (_ @t456 (_ (_ tptp.insert_b @t688) tptp.bot_bot_set_b))) (or (and (= @t118 @t455) (= @t117 @t688)) (and (= @t118 @t688) (= @t117 @t455))))))
% 0.48/0.94  (assume @p346 (forall (@list @t441 @t546 @t592 @t689) (= (= (_ @t442 @t548) (_ (_ tptp.insert1574423351_a_nat @t592) (_ (_ tptp.insert1574423351_a_nat @t689) tptp.bot_bo1836341171_a_nat))) (or (and (= @t441 @t592) (= @t546 @t689)) (and (= @t441 @t689) (= @t546 @t592))))))
% 0.48/0.94  (assume @p347 (forall @t14 (=> (_ @t13 (_ (_ tptp.insert1574423351_a_nat (_ tptp.standa63370785tant_a tptp.standard_S_Idt_a)) (_ (_ tptp.insert1574423351_a_nat (_ tptp.standa1795879409tant_a tptp.standard_S_Idt_a)) (_ (_ tptp.insert1574423351_a_nat (_ tptp.standa997693288tant_a tptp.standard_S_Idt_a)) tptp.bot_bo1836341171_a_nat)))) @t12)))
% 0.48/0.94  (assume @p348 (forall (@list @t5 @t20 @t21) (=> (_ @t162 @t691) (_ (_ tptp.equiv_1821124534_set_b @t18) (lambda (@list @t690) (_ (_ tptp.image_b_b @t691) (_ (_ tptp.insert_b @t690) tptp.bot_bot_set_b)))))))
% 0.48/0.94  (assume @p349 (= (_ @t17 @t19) (_ (_ tptp.image_1683732397od_b_b (lambda @t143 (_ @t465 @t140))) @t31)))
% 0.48/0.94  (assume @p350 (forall (@list @t692) (or (= @t692 true) (= @t692 false))))
% 0.48/0.94  (assume @p351 (forall @t129 (= (_ (_ (_ tptp.if_b false) @t5) @t20) @t20)))
% 0.48/0.94  (assume @p352 @t694)
% 0.48/0.94  (assume @p353 @t697)
% 0.48/0.94  (assume @p354 true)
% 0.48/0.94  (step @p355 (= tptp.f @t701) :rule refl :args (@t701))
% 0.48/0.94  (step @p356 (= tptp.agree_221379389_a_b_b @t705) :rule refl :args (@t705))
% 0.48/0.94  (step @p357 (= tptp.ord_less_eq_set_b @t708) :rule refl :args (@t708))
% 0.48/0.94  (step @p358 (= tptp.ord_le1036320359od_b_b @t711) :rule refl :args (@t711))
% 0.48/0.94  (step @p359 (= tptp.ord_le123089219od_b_b @t714) :rule refl :args (@t714))
% 0.48/0.94  (step @p360 (= tptp.p @t718) :rule refl :args (@t718))
% 0.48/0.94  (step @p361 :rule refl :args ((tptp.image_b_b @t18 @t429)))
% 0.48/0.94  (step @p362 :rule refl :args (@t719))
% 0.48/0.94  (step @p363 :rule refl :args (@t720))
% 0.48/0.94  (step @p364 :rule cong :premises (@p363 @p362) :args (@t721))
% 0.48/0.94  (step @p365 :rule trans :premises (@p364 @p361))
% 0.48/0.94  (step @p366 :rule refl :args (tptp.image_b_b))
% 0.48/0.94  (step @p367 :rule ho_cong :premises (@p366 @p363))
% 0.48/0.94  (step @p368 :rule ho_cong :premises (@p367 @p362))
% 0.48/0.94  (step @p369 :rule cong :premises (@p368 @p365) :args ((= (_ @t722 @t719) @t721)))
% 0.48/0.94  (step @p370 :rule symm :premises (@p369))
% 0.48/0.94  (step @p371 :rule refl :args (@t431))
% 0.48/0.94  (step @p372 :rule eq_resolve :premises (@p371 @p370))
% 0.48/0.94  (step @p373 :rule refl :args (@t429))
% 0.48/0.94  (step @p374 :rule cong :premises (@p373 @p362) :args ((= @t429 @t719)))
% 0.48/0.94  (step @p375 :rule symm :premises (@p374))
% 0.48/0.94  (step @p376 :rule eq_resolve :premises (@p373 @p375))
% 0.48/0.94  (step @p377 :rule refl :args (@t18))
% 0.48/0.94  (step @p378 :rule cong :premises (@p377 @p363) :args ((= @t18 @t720)))
% 0.48/0.94  (step @p379 :rule symm :premises (@p378))
% 0.48/0.94  (step @p380 :rule eq_resolve :premises (@p377 @p379))
% 0.48/0.94  (step @p381 :rule ho_cong :premises (@p366 @p380))
% 0.48/0.94  (step @p382 :rule ho_cong :premises (@p381 @p376))
% 0.48/0.94  (step @p383 :rule trans :premises (@p382 @p372))
% 0.48/0.94  (step @p384 :rule refl :args (tptp.bot_bot_set_b))
% 0.48/0.94  (step @p385 :rule cong :premises (@p384 @p383) :args (@t723))
% 0.48/0.94  (step @p386 :rule refl :args ((tptp.member_b @t5 @t1)))
% 0.48/0.94  (step @p387 :rule refl :args (@t724))
% 0.48/0.94  (step @p388 :rule refl :args (@t5))
% 0.48/0.94  (step @p389 :rule cong :premises (@p388 @p387) :args (@t725))
% 0.48/0.94  (step @p390 :rule trans :premises (@p389 @p386))
% 0.48/0.94  (step @p391 :rule refl :args (@t7))
% 0.48/0.94  (step @p392 :rule ho_cong :premises (@p391 @p387))
% 0.48/0.94  (step @p393 :rule cong :premises (@p392 @p390) :args ((= (_ @t7 @t724) @t725)))
% 0.48/0.94  (step @p394 :rule symm :premises (@p393))
% 0.48/0.94  (step @p395 :rule refl :args (@t8))
% 0.48/0.94  (step @p396 :rule eq_resolve :premises (@p395 @p394))
% 0.48/0.94  (step @p397 :rule refl :args (@t1))
% 0.48/0.94  (step @p398 :rule cong :premises (@p397 @p387) :args ((= @t1 @t724)))
% 0.48/0.94  (step @p399 :rule symm :premises (@p398))
% 0.48/0.94  (step @p400 :rule eq_resolve :premises (@p397 @p399))
% 0.48/0.94  (step @p401 :rule ho_cong :premises (@p391 @p400))
% 0.48/0.94  (step @p402 :rule trans :premises (@p401 @p396))
% 0.48/0.94  (step @p403 :rule cong :premises (@p402) :args (@t460))
% 0.48/0.94  (step @p404 :rule cong :premises (@p403 @p385) :args (@t726))
% 0.48/0.94  (step @p405 :rule cong :premises (@p404) :args ((forall @t9 @t726)))
% 0.48/0.94  (step @p406 :rule eq-symm :args (@t723 @t460))
% 0.48/0.94  (step @p407 :rule refl :args (@t460))
% 0.48/0.94  (step @p408 :rule eq-symm :args (@t431 tptp.bot_bot_set_b))
% 0.48/0.94  (step @p409 :rule cong :premises (@p408 @p407) :args (@t461))
% 0.48/0.94  (step @p410 :rule trans :premises (@p409 @p406))
% 0.48/0.94  (step @p411 :rule cong :premises (@p410) :args (@t462))
% 0.48/0.94  (step @p412 :rule trans :premises (@p411 @p405))
% 0.48/0.94  (step @p413 :rule eq_resolve :premises (@p169 @p412))
% 0.48/0.94  (step @p414 :rule refl :args ((tptp.member_b tptp.x @t1)))
% 0.48/0.94  (step @p415 :rule refl :args (tptp.x))
% 0.48/0.94  (step @p416 :rule cong :premises (@p415 @p387) :args (@t727))
% 0.48/0.94  (step @p417 :rule trans :premises (@p416 @p414))
% 0.48/0.94  (step @p418 :rule refl :args (@t695))
% 0.48/0.94  (step @p419 :rule ho_cong :premises (@p418 @p387))
% 0.48/0.94  (step @p420 :rule cong :premises (@p419 @p417) :args ((= (_ @t695 @t724) @t727)))
% 0.48/0.94  (step @p421 :rule symm :premises (@p420))
% 0.48/0.94  (step @p422 :rule refl :args (@t696))
% 0.48/0.94  (step @p423 :rule eq_resolve :premises (@p422 @p421))
% 0.48/0.94  (step @p424 :rule refl :args (@t695))
% 0.48/0.94  (step @p425 :rule ho_cong :premises (@p424 @p400))
% 0.48/0.94  (step @p426 :rule trans :premises (@p425 @p423))
% 0.48/0.94  (step @p427 :rule cong :premises (@p426) :args (@t697))
% 0.48/0.94  (step @p428 :rule eq_resolve :premises (@p353 @p427))
% 0.48/0.94  (step @p429 :rule refl :args (@t728))
% 0.48/0.94  (step @p430 :rule refl :args (@t693))
% 0.48/0.94  (step @p431 :rule cong :premises (@p430 @p429) :args ((= @t693 @t728)))
% 0.48/0.94  (step @p432 :rule symm :premises (@p431))
% 0.48/0.94  (step @p433 :rule eq_resolve :premises (@p430 @p432))
% 0.48/0.94  (step @p434 :rule cong :premises (@p388 @p433) :args (@t729))
% 0.48/0.94  (step @p435 :rule cong :premises (@p434) :args ((forall @t129 @t729)))
% 0.48/0.94  (step @p436 :rule eq-symm :args (@t693 @t5))
% 0.48/0.94  (step @p437 :rule cong :premises (@p436) :args (@t694))
% 0.48/0.94  (step @p438 :rule trans :premises (@p437 @p435))
% 0.48/0.94  (step @p439 :rule eq_resolve :premises (@p352 @p438))
% 0.48/0.94  (step @p440 :rule refl :args (@t735))
% 0.48/0.94  (step @p441 :rule refl :args (tptp.x))
% 0.48/0.94  (step @p442 :rule skolem_intro :args (@t736))
% 0.48/0.94  (step @p443 :rule symm :premises (@p442))
% 0.48/0.94  (step @p444 :rule cong :premises (@p443 @p441 @p440) :args (@t737))
% 0.48/0.94  (step @p445 :rule cong :premises (@p441 @p444) :args (@t738))
% 0.48/0.94  (step @p446 :rule refl :args (@t739))
% 0.48/0.94  (step @p447 :rule cong :premises (@p446 @p445) :args ((=> @t739 @t738)))
% 0.48/0.94  (assume-push @p629 @t739)
% 0.48/0.94  (step @p449 :rule instantiate :premises (@p439) :args ((@list tptp.x @t735)))
% 0.48/0.94  (step-pop @p630 :rule scope :premises (@p449))
% 0.48/0.94  (step @p450 :rule process_scope :premises (@p630) :args (@t738))
% 0.48/0.94  (step @p452 :rule eq_resolve :premises (@p450 @p447))
% 0.48/0.94  (step @p453 :rule implies_elim :premises (@p452))
% 0.48/0.94  (step @p454 :rule chain_m_resolution :premises (@p453 @p439) :args (@t741 (@list false) (@list @t739)))
% 0.48/0.94  (step @p455 :rule bool-eq-true :args (@t736))
% 0.48/0.94  (step @p456 :rule eq_resolve :premises (@p442 @p455))
% 0.48/0.94  (step @p457 :rule refl :args ((tptp.member_b @t746 @t1)))
% 0.48/0.94  (step @p458 :rule refl :args ((tptp.if_b @t744 tptp.x @t742)))
% 0.48/0.94  (step @p459 :rule refl :args (@t735))
% 0.48/0.94  (step @p460 :rule refl :args (@t744))
% 0.48/0.94  (step @p461 :rule cong :premises (@p460 @p415 @p459) :args (@t747))
% 0.48/0.94  (step @p462 :rule trans :premises (@p461 @p458))
% 0.48/0.94  (step @p463 :rule cong :premises (@p462 @p387) :args (@t748))
% 0.48/0.94  (step @p464 :rule trans :premises (@p463 @p457))
% 0.48/0.94  (step @p465 :rule refl :args (tptp.member_b))
% 0.48/0.94  (step @p466 :rule ho_cong :premises (@p465 @p462))
% 0.48/0.94  (step @p467 :rule ho_cong :premises (@p466 @p387))
% 0.48/0.94  (step @p468 :rule cong :premises (@p467 @p464) :args ((= (_ (_ tptp.member_b @t747) @t724) @t748)))
% 0.48/0.94  (step @p469 :rule symm :premises (@p468))
% 0.48/0.94  (step @p470 :rule refl :args ((_ (_ tptp.member_b @t746) @t1)))
% 0.48/0.94  (step @p471 :rule eq_resolve :premises (@p470 @p469))
% 0.48/0.94  (step @p472 :rule refl :args (@t745))
% 0.48/0.94  (step @p473 :rule ho_cong :premises (@p472 @p459))
% 0.48/0.94  (step @p474 :rule cong :premises (@p473 @p462) :args ((= (_ @t745 @t735) @t747)))
% 0.48/0.94  (step @p475 :rule symm :premises (@p474))
% 0.48/0.94  (step @p476 :rule refl :args (@t746))
% 0.48/0.94  (step @p477 :rule eq_resolve :premises (@p476 @p475))
% 0.48/0.94  (step @p478 :rule refl :args (@t742))
% 0.48/0.94  (step @p479 :rule cong :premises (@p478 @p459) :args ((= @t742 @t735)))
% 0.48/0.94  (step @p480 :rule symm :premises (@p479))
% 0.48/0.94  (step @p481 :rule eq_resolve :premises (@p478 @p480))
% 0.48/0.94  (step @p482 :rule eq-refl :args (@t733))
% 0.48/0.94  (step @p483 :rule skolem_intro :args (@t734))
% 0.48/0.94  (step @p484 :rule refl :args (@t733))
% 0.48/0.94  (step @p485 :rule cong :premises (@p484 @p483) :args ((= @t733 @t734)))
% 0.48/0.94  (step @p486 :rule trans :premises (@p485 @p482))
% 0.48/0.94  (step @p487 :rule true_elim :premises (@p486))
% 0.48/0.94  (step @p488 :rule refl :args (tptp.hilbert_Eps_b))
% 0.48/0.94  (step @p489 :rule ho_cong :premises (@p488 @p487))
% 0.48/0.94  (step @p490 :rule trans :premises (@p489 @p481))
% 0.48/0.94  (step @p491 :rule eq-refl :args (@t743))
% 0.48/0.94  (step @p492 :rule skolem_intro :args (@t744))
% 0.48/0.94  (step @p493 :rule refl :args (@t743))
% 0.48/0.94  (step @p494 :rule cong :premises (@p493 @p492) :args (@t749))
% 0.48/0.94  (step @p495 :rule trans :premises (@p494 @p491))
% 0.48/0.94  (step @p496 :rule true_elim :premises (@p495))
% 0.48/0.94  (step @p497 :rule refl :args (tptp.if_b))
% 0.48/0.94  (step @p498 :rule ho_cong :premises (@p497 @p496))
% 0.48/0.94  (step @p499 :rule ho_cong :premises (@p498 @p441))
% 0.48/0.94  (step @p500 :rule ho_cong :premises (@p499 @p490))
% 0.48/0.94  (step @p501 :rule trans :premises (@p500 @p477))
% 0.48/0.94  (step @p502 :rule refl :args (tptp.member_b))
% 0.48/0.94  (step @p503 :rule ho_cong :premises (@p502 @p501))
% 0.48/0.94  (step @p504 :rule ho_cong :premises (@p503 @p400))
% 0.48/0.94  (step @p505 :rule trans :premises (@p504 @p471))
% 0.48/0.94  (step @p506 :rule refl :args (@t1))
% 0.48/0.94  (step @p507 :rule beta-reduce :args ((= (_ (lambda @t143 (_ @t751 (_ tptp.hilbert_Eps_b @t750))) tptp.x) (_ (_ (_ tptp.if_b @t743) tptp.x) (_ tptp.hilbert_Eps_b @t733)))))
% 0.48/0.94  (step @p508 :rule beta-reduce :args ((= @t752 @t750)))
% 0.48/0.94  (step @p509 :rule ho_cong :premises (@p488 @p508))
% 0.48/0.94  (step @p510 :rule refl :args (@t751))
% 0.48/0.94  (step @p511 :rule ho_cong :premises (@p510 @p509))
% 0.48/0.94  (step @p512 :rule cong :premises (@p511) :args ((lambda @t143 (_ @t751 (_ tptp.hilbert_Eps_b @t752)))))
% 0.48/0.94  (step @p513 :rule ho_cong :premises (@p512 @p441))
% 0.48/0.94  (step @p514 :rule trans :premises (@p513 @p507))
% 0.48/0.94  (step @p515 :rule ho_cong :premises (@p502 @p514))
% 0.48/0.94  (step @p516 :rule ho_cong :premises (@p515 @p506))
% 0.48/0.94  (step @p517 :rule refl :args (@t140))
% 0.48/0.94  (step @p518 :rule ho_cong :premises (@p360 @p517))
% 0.48/0.94  (step @p519 :rule ho_cong :premises (@p488 @p518))
% 0.48/0.94  (step @p520 :rule ho_cong :premises (@p510 @p519))
% 0.48/0.94  (step @p521 :rule cong :premises (@p520) :args ((lambda @t143 (_ @t751 @t698))))
% 0.48/0.94  (step @p522 :rule refl :args (@t698))
% 0.48/0.94  (step @p523 :rule eq-symm :args (@t700 tptp.bot_bot_set_b))
% 0.48/0.94  (step @p524 :rule ho_cong :premises (@p497 @p523))
% 0.48/0.94  (step @p525 :rule ho_cong :premises (@p524 @p517))
% 0.48/0.94  (step @p526 :rule ho_cong :premises (@p525 @p522))
% 0.48/0.94  (step @p527 :rule cong :premises (@p526) :args (@t701))
% 0.48/0.94  (step @p528 :rule trans :premises (@p355 @p527))
% 0.48/0.94  (step @p529 :rule trans :premises (@p528 @p521))
% 0.48/0.94  (step @p530 :rule ho_cong :premises (@p529 @p441))
% 0.48/0.94  (step @p531 :rule ho_cong :premises (@p502 @p530))
% 0.48/0.94  (step @p532 :rule ho_cong :premises (@p531 @p506))
% 0.48/0.94  (step @p533 :rule trans :premises (@p532 @p516))
% 0.48/0.94  (step @p534 :rule trans :premises (@p533 @p505))
% 0.48/0.94  (step @p535 :rule eq_resolve :premises (@p3 @p534))
% 0.48/0.94  (step @p536 :rule refl :args (@t753))
% 0.48/0.94  (step @p537 :rule refl :args (@t754))
% 0.48/0.94  (step @p538 :rule bool-double-not-elim :args (@t727))
% 0.48/0.94  (step @p539 :rule refl :args (@t755))
% 0.48/0.94  (step @p540 :rule refl :args (@t756))
% 0.48/0.94  (step @p541 :rule nary_cong :premises (@p540 @p539 @p538 @p537 @p536) :args ((or @t756 @t755 @t758 @t754 @t753)))
% 0.48/0.94  (assume-push @p631 @t748)
% 0.48/0.94  (assume-push @p632 @t744)
% 0.48/0.94  (assume-push @p633 @t736)
% 0.48/0.94  (assume-push @p634 @t741)
% 0.48/0.94  (assume-push @p635 @t757)
% 0.48/0.94  (step @p547 :rule evaluate :args ((= false true)))
% 0.48/0.94  (step @p548 :rule true_intro :premises (@p535))
% 0.48/0.94  (step @p549 :rule refl :args (@t724))
% 0.48/0.94  (step @p550 :rule true_intro :premises (@p632))
% 0.48/0.94  (step @p551 :rule symm :premises (@p550))
% 0.48/0.94  (step @p552 :rule trans :premises (@p442 @p551))
% 0.48/0.94  (step @p553 :rule cong :premises (@p552 @p441 @p440) :args (@t740))
% 0.48/0.94  (step @p554 :rule trans :premises (@p454 @p553))
% 0.48/0.94  (step @p555 :rule cong :premises (@p554 @p549) :args (@t727))
% 0.48/0.94  (step @p556 :rule false_intro :premises (@p428))
% 0.48/0.94  (step @p557 :rule symm :premises (@p556))
% 0.48/0.94  (step @p558 :rule trans :premises (@p557 @p555 @p548))
% 0.48/0.94  (step @p559 false :rule eq_resolve :premises (@p558 @p547))
% 0.48/0.94  (step-pop @p636 :rule scope :premises (@p559))
% 0.48/0.94  (step-pop @p637 :rule scope :premises (@p636))
% 0.48/0.94  (step-pop @p638 :rule scope :premises (@p637))
% 0.48/0.94  (step-pop @p639 :rule scope :premises (@p638))
% 0.48/0.94  (step-pop @p640 :rule scope :premises (@p639))
% 0.48/0.94  (step @p560 :rule process_scope :premises (@p640) :args (false))
% 0.48/0.94  (assume-push @p641 @t744)
% 0.48/0.94  (assume-push @p642 @t748)
% 0.48/0.94  (assume-push @p643 @t757)
% 0.48/0.94  (assume-push @p644 @t736)
% 0.48/0.94  (assume-push @p645 @t741)
% 0.48/0.94  (step @p571 :rule and_intro :premises (@p535 @p641 @p456 @p454 @p428))
% 0.48/0.94  (step-pop @p646 :rule scope :premises (@p571))
% 0.48/0.94  (step-pop @p647 :rule scope :premises (@p646))
% 0.48/0.94  (step-pop @p648 :rule scope :premises (@p647))
% 0.48/0.94  (step-pop @p649 :rule scope :premises (@p648))
% 0.48/0.94  (step-pop @p650 :rule scope :premises (@p649))
% 0.48/0.94  (step @p572 :rule process_scope :premises (@p650) :args (@t759))
% 0.48/0.94  (step @p578 :rule implies_elim :premises (@p572))
% 0.48/0.94  (step @p579 :rule resolution :premises (@p578 @p560) :args (true @t759))
% 0.48/0.94  (step @p580 :rule not_and :premises (@p579))
% 0.48/0.94  (step @p581 :rule eq_resolve :premises (@p580 @p541))
% 0.48/0.94  (step @p582 :rule reordering :premises (@p581) :args ((or @t727 @t755 @t756 @t754 @t753)))
% 0.48/0.94  (step @p583 :rule chain_m_resolution :premises (@p582 @p428 @p535 @p456 @p454) :args (@t756 (@list true false false false) (@list @t727 @t748 @t736 @t741)))
% 0.48/0.94  (step @p584 :rule eq-symm :args (@t762 @t744))
% 0.48/0.94  (step @p585 :rule refl :args (@t744))
% 0.48/0.94  (step @p586 :rule refl :args ((tptp.image_b_b @t18 @t730)))
% 0.48/0.94  (step @p587 :rule refl :args (@t760))
% 0.48/0.94  (step @p588 :rule cong :premises (@p363 @p587) :args (@t761))
% 0.48/0.94  (step @p589 :rule trans :premises (@p588 @p586))
% 0.48/0.94  (step @p590 :rule ho_cong :premises (@p367 @p587))
% 0.48/0.94  (step @p591 :rule cong :premises (@p590 @p589) :args ((= (_ @t722 @t760) @t761)))
% 0.48/0.94  (step @p592 :rule symm :premises (@p591))
% 0.48/0.94  (step @p593 :rule refl :args (@t731))
% 0.48/0.94  (step @p594 :rule eq_resolve :premises (@p593 @p592))
% 0.48/0.94  (step @p595 :rule refl :args (@t730))
% 0.48/0.94  (step @p596 :rule cong :premises (@p595 @p587) :args ((= @t730 @t760)))
% 0.48/0.94  (step @p597 :rule symm :premises (@p596))
% 0.48/0.94  (step @p598 :rule eq_resolve :premises (@p595 @p597))
% 0.48/0.94  (step @p599 :rule refl :args (tptp.image_b_b))
% 0.48/0.94  (step @p600 :rule ho_cong :premises (@p599 @p380))
% 0.48/0.94  (step @p601 :rule ho_cong :premises (@p600 @p598))
% 0.48/0.94  (step @p602 :rule trans :premises (@p601 @p594))
% 0.48/0.94  (step @p603 :rule refl :args (tptp.bot_bot_set_b))
% 0.48/0.94  (step @p604 :rule cong :premises (@p603 @p602) :args (@t743))
% 0.48/0.94  (step @p605 :rule cong :premises (@p604 @p585) :args (@t749))
% 0.48/0.94  (step @p606 :rule trans :premises (@p605 @p584))
% 0.48/0.94  (step @p607 :rule eq-symm :args (@t744 @t743))
% 0.48/0.94  (step @p608 :rule trans :premises (@p607 @p606))
% 0.48/0.94  (step @p609 :rule eq_resolve :premises (@p492 @p608))
% 0.48/0.94  (step @p610 :rule equiv_elim2 :premises (@p609))
% 0.48/0.94  (step @p611 :rule chain_m_resolution :premises (@p610 @p583) :args ((not @t762) (@list true) (@list @t744)))
% 0.48/0.94  (step @p612 :rule refl :args (@t762))
% 0.48/0.94  (step @p613 :rule refl :args (@t764))
% 0.48/0.94  (step @p614 :rule nary_cong :premises (@p613 @p612 @p538) :args ((or @t764 @t762 @t758)))
% 0.48/0.94  (step @p615 :rule cnf_equiv_pos2 :args (@t763))
% 0.48/0.94  (step @p616 :rule eq_resolve :premises (@p615 @p614))
% 0.48/0.94  (step @p617 :rule reordering :premises (@p616) :args ((or @t762 @t727 @t764)))
% 0.48/0.94  (step @p618 :rule chain_m_resolution :premises (@p617 @p611 @p428) :args (@t764 (@list true true) (@list @t762 @t727)))
% 0.48/0.94  (step @p619 :rule eq-symm :args (@t757 @t762))
% 0.48/0.94  (step @p620 :rule refl :args (@t765))
% 0.48/0.94  (step @p621 :rule cong :premises (@p620 @p619) :args ((=> @t765 @t766)))
% 0.48/0.94  (assume-push @p651 @t765)
% 0.48/0.94  (step @p623 :rule instantiate :premises (@p413) :args ((@list tptp.x)))
% 0.48/0.94  (step-pop @p652 :rule scope :premises (@p623))
% 0.48/0.94  (step @p624 :rule process_scope :premises (@p652) :args (@t766))
% 0.48/0.94  (step @p626 :rule eq_resolve :premises (@p624 @p621))
% 0.48/0.94  (step @p627 :rule implies_elim :premises (@p626))
% 0.48/0.94  (step @p628 false :rule chain_m_resolution :premises (@p627 @p618 @p413) :args (false (@list true false) (@list @t763 @t765)))
% 0.48/0.94  )
% 0.48/0.94  % SZS output end Proof
% 0.48/0.94  % cvc5 exiting
%------------------------------------------------------------------------------