cvc5---1.3.4.THM-Prf.s

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

% Computer : n005.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:00 AM UTC 2026

% Result   : Theorem 0.45s 0.89s
% Output   : Proof 0.75s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem  : ITP083^1 : TPTP v9.2.1. Released v7.5.0.
% 0.11/0.13  % Command  : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.34  % Computer : n005.cluster.edu
% 0.15/0.34  % Model    : x86_64 x86_64
% 0.15/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34  % Memory   : 8042.1875MB
% 0.15/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34  % CPULimit : 300
% 0.15/0.34  % WCLimit  : 300
% 0.15/0.34  % DateTime : Tue Jun  2 04:13:33 EDT 2026
% 0.15/0.34  % CPUTime  : 
% 0.37/0.61  %----Proving TH0
% 0.45/0.89  --- 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.45/0.89  % SZS status Theorem
% 0.45/0.89  % SZS output start Proof
% 0.45/0.89  (
% 0.45/0.89  (declare-sort tptp.produc1324971431et_val 0)
% 0.45/0.89  (declare-sort tptp.set_Pr1311924359et_val 0)
% 0.45/0.89  (declare-sort tptp.produc1432036078de_val 0)
% 0.45/0.89  (declare-sort tptp.set_Pr699757092de_val 0)
% 0.45/0.89  (declare-sort tptp.set_val 0)
% 0.45/0.89  (declare-sort tptp.set_set_val 0)
% 0.45/0.89  (declare-sort tptp.node 0)
% 0.45/0.89  (declare-sort tptp.set_node 0)
% 0.45/0.89  (declare-sort tptp.option_list_val 0)
% 0.45/0.89  (declare-sort tptp.val 0)
% 0.45/0.89  (declare-sort tptp.produc1664334075de_val 0)
% 0.45/0.89  (declare-sort tptp.set_Pr701036849de_val 0)
% 0.45/0.89  (declare-sort tptp.list_val 0)
% 0.45/0.89  (declare-sort tptp.list_P1820443774de_val 0)
% 0.45/0.89  (declare-sort tptp.list_P844977291de_val 0)
% 0.45/0.89  (declare-sort tptp.option_set_val 0)
% 0.45/0.89  (declare-sort tptp.list_P2089461677et_val 0)
% 0.45/0.89  (declare-sort tptp.list_P88441325et_val 0)
% 0.45/0.89  (declare-sort tptp.set_Pr1587248327et_val 0)
% 0.45/0.89  (declare-sort tptp.product_prod_val_val 0)
% 0.45/0.89  (declare-sort tptp.set_Pr700443783al_val 0)
% 0.45/0.89  (declare-sort tptp.g 0)
% 0.45/0.89  (declare-sort tptp.list_P561207620_edgeD 0)
% 0.45/0.89  (declare-sort tptp.produc1946948786l_node 0)
% 0.45/0.89  (declare-sort tptp.set_Pr2105655784l_node 0)
% 0.45/0.89  (declare-sort tptp.var 0)
% 0.45/0.89  (declare-sort tptp.set_Pr978022247et_val 0)
% 0.45/0.89  (declare-sort tptp.produc1615737844de_val 0)
% 0.45/0.89  (declare-sort tptp.set_Pr1245322836de_val 0)
% 0.45/0.89  (declare-sort tptp.list_P1811375021al_val 0)
% 0.45/0.89  (declare-sort tptp.produc1062784462et_val 0)
% 0.45/0.89  (declare-sort tptp.set_Pr1320419588et_val 0)
% 0.45/0.89  (declare-sort tptp.list_P1078858818l_node 0)
% 0.45/0.89  (declare-sort tptp.list_P761482893et_val 0)
% 0.45/0.89  (declare-sort tptp.produc1904584935et_val 0)
% 0.45/0.89  (declare-sort tptp.produc1013974930l_node 0)
% 0.45/0.89  (declare-sort tptp.set_Pr574789832l_node 0)
% 0.45/0.89  (declare-sort tptp.produc951622955e_node 0)
% 0.45/0.89  (declare-sort tptp.set_Pr9085835e_node 0)
% 0.45/0.89  (declare-sort tptp.list_P729276995de_val 0)
% 0.45/0.89  (declare-sort tptp.set_Pr819703837de_val 0)
% 0.45/0.89  (declare-sort tptp.produc1858904199et_val 0)
% 0.45/0.89  (declare-sort tptp.list_set_val 0)
% 0.45/0.89  (declare-sort tptp.list_node 0)
% 0.45/0.89  (declare-sort tptp.produc452075965de_val 0)
% 0.45/0.89  (declare-sort tptp.list_P1108777338de_val 0)
% 0.45/0.89  (declare-sort tptp.list_P12184414et_val 0)
% 0.45/0.89  (declare-sort tptp.produc782216903al_val 0)
% 0.45/0.89  (declare-sort tptp.list_P1127016369e_node 0)
% 0.45/0.89  (declare-sort tptp.set_Pr1157324199al_val 0)
% 0.45/0.89  (declare-sort tptp.list_P1414038306l_node 0)
% 0.45/0.89  (declare-sort tptp.list_P940784845al_val 0)
% 0.45/0.89  (declare-const tptp.sSA_CF1517915011eD_val (-> (-> tptp.g tptp.list_node) (-> tptp.g tptp.node tptp.list_P561207620_edgeD) (-> tptp.g tptp.node tptp.set_val) (-> tptp.g tptp.node tptp.set_val) (-> tptp.g tptp.produc1432036078de_val tptp.option_list_val) tptp.g tptp.set_val))
% 0.45/0.89  (declare-const tptp.sSA_CF1909049442de_val (-> (-> tptp.g tptp.list_node) (-> tptp.g tptp.node tptp.set_val) (-> tptp.g tptp.produc1432036078de_val tptp.option_list_val) tptp.g tptp.val tptp.val Bool))
% 0.45/0.89  (declare-const tptp.member_val (-> tptp.val tptp.set_val Bool))
% 0.45/0.89  (declare-const tptp.sSA_CF794421325de_val (-> (-> tptp.g tptp.list_node) (-> tptp.g tptp.node tptp.set_val) (-> tptp.g tptp.node tptp.set_val) (-> tptp.g tptp.produc1432036078de_val tptp.option_list_val) tptp.g tptp.val Bool))
% 0.45/0.89  (declare-const tptp.sSA_CF370335846de_val (-> (-> tptp.g tptp.produc1432036078de_val tptp.option_list_val) tptp.g tptp.node tptp.set_val))
% 0.45/0.89  (declare-const tptp.set_node2 (-> tptp.list_node tptp.set_node))
% 0.45/0.89  (declare-const tptp.member_node (-> tptp.node tptp.set_node Bool))
% 0.45/0.89  (declare-const tptp.sup_sup_set_val (-> tptp.set_val tptp.set_val tptp.set_val))
% 0.45/0.89  (declare-const tptp.sSA_CF848637139eD_val (-> (-> tptp.g tptp.list_node) (-> tptp.g tptp.node tptp.list_P561207620_edgeD) (-> tptp.g tptp.produc1432036078de_val tptp.option_list_val) tptp.g tptp.node tptp.set_val))
% 0.45/0.89  (declare-const tptp.sSA_CF551432799de_val (-> (-> tptp.g tptp.list_node) (-> tptp.g tptp.node tptp.set_val) (-> tptp.g tptp.produc1432036078de_val tptp.option_list_val) tptp.g tptp.val tptp.node))
% 0.45/0.89  (declare-const tptp.produc1470527136de_val (-> tptp.node tptp.val tptp.produc1432036078de_val))
% 0.45/0.89  (declare-const tptp.set_val2 (-> tptp.list_val tptp.set_val))
% 0.45/0.89  (declare-const tptp.some_list_val (-> tptp.list_val tptp.option_list_val))
% 0.45/0.89  (declare-const tptp.member_set_val (-> tptp.set_val tptp.set_set_val Bool))
% 0.45/0.89  (declare-const tptp.member313544709de_val (-> tptp.produc1432036078de_val tptp.set_Pr699757092de_val Bool))
% 0.45/0.89  (declare-const tptp.member1711426256et_val (-> tptp.produc1324971431et_val tptp.set_Pr1311924359et_val Bool))
% 0.45/0.89  (declare-const tptp.insert1846469495et_val (-> tptp.produc1324971431et_val tptp.set_Pr1311924359et_val tptp.set_Pr1311924359et_val))
% 0.45/0.89  (declare-const tptp.insert869443870de_val (-> tptp.produc1432036078de_val tptp.set_Pr699757092de_val tptp.set_Pr699757092de_val))
% 0.45/0.89  (declare-const tptp.insert_set_val (-> tptp.set_val tptp.set_set_val tptp.set_set_val))
% 0.45/0.89  (declare-const tptp.insert_node (-> tptp.node tptp.set_node tptp.set_node))
% 0.45/0.89  (declare-const tptp.dom_Pr729677986st_val (-> (-> tptp.produc1432036078de_val tptp.option_list_val) tptp.set_Pr699757092de_val))
% 0.45/0.89  (declare-const tptp.insert_val (-> tptp.val tptp.set_val tptp.set_val))
% 0.45/0.89  (declare-const tptp.bot_bo404898488de_val tptp.set_Pr699757092de_val)
% 0.45/0.89  (declare-const tptp.sup_sup_set_set_val (-> tptp.set_set_val tptp.set_set_val tptp.set_set_val))
% 0.45/0.89  (declare-const tptp.sup_sup_set_node (-> tptp.set_node tptp.set_node tptp.set_node))
% 0.45/0.89  (declare-const tptp.bot_bot_set_val tptp.set_val)
% 0.45/0.89  (declare-const tptp.member1894062994de_val (-> tptp.produc1664334075de_val tptp.set_Pr701036849de_val Bool))
% 0.45/0.89  (declare-const tptp.member562853661de_val (-> tptp.produc1615737844de_val tptp.set_Pr1245322836de_val Bool))
% 0.45/0.89  (declare-const tptp.produc1162531244de_val (-> tptp.node tptp.produc1432036078de_val tptp.produc1615737844de_val))
% 0.45/0.89  (declare-const tptp.set_Pr1157337481de_val (-> tptp.list_P1108777338de_val tptp.set_Pr1245322836de_val))
% 0.45/0.89  (declare-const tptp.zip_no263301324de_val (-> tptp.list_node tptp.list_P1820443774de_val tptp.list_P1108777338de_val))
% 0.45/0.89  (declare-const tptp.bot_bo2078591731et_val tptp.set_Pr1311924359et_val)
% 0.45/0.89  (declare-const tptp.member39229872et_val (-> tptp.produc1858904199et_val tptp.set_Pr978022247et_val Bool))
% 0.45/0.89  (declare-const tptp.zip_val_set_val (-> tptp.list_val tptp.list_set_val tptp.list_P761482893et_val))
% 0.45/0.89  (declare-const tptp.member125181669et_val (-> tptp.produc1062784462et_val tptp.set_Pr1320419588et_val Bool))
% 0.45/0.89  (declare-const tptp.produc2042994048et_val (-> tptp.node tptp.set_val tptp.produc1062784462et_val))
% 0.45/0.89  (declare-const tptp.set_Pr1953765241et_val (-> tptp.list_P12184414et_val tptp.set_Pr1320419588et_val))
% 0.45/0.89  (declare-const tptp.set_Pr1027623516al_val (-> tptp.list_P940784845al_val tptp.set_Pr1157324199al_val))
% 0.45/0.89  (declare-const tptp.zip_set_val_val (-> tptp.list_set_val tptp.list_val tptp.list_P940784845al_val))
% 0.45/0.89  (declare-const tptp.set_Pr1904955709l_node (-> tptp.list_P1414038306l_node tptp.set_Pr574789832l_node))
% 0.45/0.89  (declare-const tptp.zip_set_val_node (-> tptp.list_set_val tptp.list_node tptp.list_P1414038306l_node))
% 0.45/0.89  (declare-const tptp.member76372137l_node (-> tptp.produc1013974930l_node tptp.set_Pr574789832l_node Bool))
% 0.45/0.89  (declare-const tptp.zip_val_node (-> tptp.list_val tptp.list_node tptp.list_P1078858818l_node))
% 0.45/0.89  (declare-const tptp.produc1074923692l_node (-> tptp.val tptp.node tptp.produc1946948786l_node))
% 0.45/0.89  (declare-const tptp.irredu1955035135eD_val (-> (-> tptp.g tptp.list_node) (-> tptp.g tptp.node tptp.list_P561207620_edgeD) (-> tptp.g tptp.node tptp.set_val) (-> tptp.g tptp.node tptp.set_val) (-> tptp.g tptp.produc1432036078de_val tptp.option_list_val) tptp.g tptp.set_val tptp.set_val Bool))
% 0.45/0.89  (declare-const tptp.zip_set_val_set_val (-> tptp.list_set_val tptp.list_set_val tptp.list_P2089461677et_val))
% 0.45/0.89  (declare-const tptp.zip_va679686869de_val (-> tptp.list_val tptp.list_P1820443774de_val tptp.list_P844977291de_val))
% 0.45/0.89  (declare-const tptp.member698732390de_val (-> tptp.produc452075965de_val tptp.set_Pr819703837de_val Bool))
% 0.45/0.89  (declare-const tptp.set_Pr482027474de_val (-> tptp.list_P729276995de_val tptp.set_Pr819703837de_val))
% 0.45/0.89  (declare-const tptp.zip_Pr1472086037de_val (-> tptp.list_P1820443774de_val tptp.list_P1820443774de_val tptp.list_P729276995de_val))
% 0.45/0.89  (declare-const tptp.member1110026224al_val (-> tptp.produc782216903al_val tptp.set_Pr1157324199al_val Bool))
% 0.45/0.89  (declare-const tptp.zip_val_val (-> tptp.list_val tptp.list_val tptp.list_P1811375021al_val))
% 0.45/0.89  (declare-const tptp.graph_1037173556_edgeD (-> (-> tptp.g tptp.list_node) (-> tptp.g tptp.node tptp.list_P561207620_edgeD) tptp.g tptp.node tptp.list_node))
% 0.45/0.89  (declare-const tptp.produc457016035e_node (-> tptp.node tptp.node tptp.produc951622955e_node))
% 0.45/0.89  (declare-const tptp.set_Pr450990656e_node (-> tptp.list_P1127016369e_node tptp.set_Pr9085835e_node))
% 0.45/0.89  (declare-const tptp.produc2052093836l_node (-> tptp.set_val tptp.node tptp.produc1013974930l_node))
% 0.45/0.89  (declare-const tptp.finite_finite_node (-> tptp.set_node Bool))
% 0.45/0.89  (declare-const tptp.set_set_val2 (-> tptp.list_set_val tptp.set_set_val))
% 0.45/0.89  (declare-const tptp.produc453318901de_val (-> tptp.produc1432036078de_val tptp.produc1432036078de_val tptp.produc452075965de_val))
% 0.45/0.89  (declare-const tptp.finite759259600al_val (-> tptp.set_Pr700443783al_val Bool))
% 0.45/0.89  (declare-const tptp.sSA_CF655860150de_val (-> (-> tptp.g tptp.list_node) (-> tptp.g tptp.node tptp.set_val) tptp.g tptp.set_val))
% 0.45/0.89  (declare-const tptp.member1680438992al_val (-> tptp.product_prod_val_val tptp.set_Pr700443783al_val Bool))
% 0.45/0.89  (declare-const tptp.set_Pr434939430de_val (-> tptp.list_P844977291de_val tptp.set_Pr701036849de_val))
% 0.45/0.89  (declare-const tptp.produc1377626967et_val (-> tptp.produc1324971431et_val tptp.produc1324971431et_val tptp.produc1904584935et_val))
% 0.45/0.89  (declare-const tptp.finite423892681l_node (-> tptp.set_Pr2105655784l_node Bool))
% 0.45/0.89  (declare-const tptp.set_Pr2104310812et_val (-> tptp.list_P761482893et_val tptp.set_Pr978022247et_val))
% 0.45/0.89  (declare-const tptp.bot_bot_set_set_val tptp.set_set_val)
% 0.45/0.89  (declare-const tptp.member828457417l_node (-> tptp.produc1946948786l_node tptp.set_Pr2105655784l_node Bool))
% 0.45/0.89  (declare-const tptp.ord_less_eq_val (-> tptp.val tptp.val Bool))
% 0.45/0.89  (declare-const tptp.finite1581417648et_val (-> tptp.set_Pr978022247et_val Bool))
% 0.45/0.89  (declare-const tptp.s tptp.val)
% 0.45/0.89  (declare-const tptp.set_Pr1600883293l_node (-> tptp.list_P1078858818l_node tptp.set_Pr2105655784l_node))
% 0.45/0.89  (declare-const tptp.collec885255687l_node (-> (-> tptp.produc1946948786l_node Bool) tptp.set_Pr2105655784l_node))
% 0.45/0.89  (declare-const tptp.set_Pr284769596et_val (-> tptp.list_P2089461677et_val tptp.set_Pr1311924359et_val))
% 0.45/0.89  (declare-const tptp.none_list_val tptp.option_list_val)
% 0.45/0.89  (declare-const tptp.phi tptp.val)
% 0.45/0.89  (declare-const tptp.phi2 tptp.val)
% 0.45/0.89  (declare-const tptp.graph_272749361_edgeD (-> (-> tptp.g tptp.node tptp.list_P561207620_edgeD) tptp.g tptp.node tptp.list_node))
% 0.45/0.89  (declare-const tptp.zip_Pr21865079et_val (-> tptp.list_P2089461677et_val tptp.list_P2089461677et_val tptp.list_P88441325et_val))
% 0.45/0.89  (declare-const tptp.g2 tptp.g)
% 0.45/0.89  (declare-const tptp.collec52550418al_val (-> (-> tptp.product_prod_val_val Bool) tptp.set_Pr700443783al_val))
% 0.45/0.89  (declare-const tptp.phis (-> tptp.g tptp.produc1432036078de_val tptp.option_list_val))
% 0.45/0.89  (declare-const tptp.collect_set_val (-> (-> tptp.set_val Bool) tptp.set_set_val))
% 0.45/0.89  (declare-const tptp.alpha_n (-> tptp.g tptp.list_node))
% 0.45/0.89  (declare-const tptp.produc1337903031al_val (-> tptp.set_val tptp.val tptp.produc782216903al_val))
% 0.45/0.89  (declare-const tptp.finite_finite_val (-> tptp.set_val Bool))
% 0.45/0.89  (declare-const tptp.phi_s tptp.val)
% 0.45/0.89  (declare-const tptp.finite79836624et_val (-> tptp.set_Pr1311924359et_val Bool))
% 0.45/0.89  (declare-const tptp.uses (-> tptp.g tptp.node tptp.set_val))
% 0.45/0.89  (declare-const tptp.ord_less_eq_node (-> tptp.node tptp.node Bool))
% 0.45/0.89  (declare-const tptp.finite781217938de_val (-> tptp.set_Pr701036849de_val Bool))
% 0.45/0.89  (declare-const tptp.inEdges (-> tptp.g tptp.node tptp.list_P561207620_edgeD))
% 0.45/0.89  (declare-const tptp.produc1041633943et_val (-> tptp.set_val tptp.set_val tptp.produc1324971431et_val))
% 0.45/0.89  (declare-const tptp.finite1265617511et_val (-> tptp.set_set_val Bool))
% 0.45/0.89  (declare-const tptp.set_Pr102746428al_val (-> tptp.list_P1811375021al_val tptp.set_Pr700443783al_val))
% 0.45/0.89  (declare-const tptp.collec1117167378et_val (-> (-> tptp.produc1324971431et_val Bool) tptp.set_Pr1311924359et_val))
% 0.45/0.89  (declare-const tptp.set_Pr1085970585de_val (-> tptp.list_P1820443774de_val tptp.set_Pr699757092de_val))
% 0.45/0.89  (declare-const tptp.defs (-> tptp.g tptp.node tptp.set_val))
% 0.45/0.89  (declare-const tptp.finite2056463621de_val (-> tptp.set_Pr699757092de_val Bool))
% 0.45/0.89  (declare-const tptp.var2 (-> tptp.g tptp.val tptp.var))
% 0.45/0.89  (declare-const tptp.collect_val (-> (-> tptp.val Bool) tptp.set_val))
% 0.45/0.89  (declare-const tptp.collect_node (-> (-> tptp.node Bool) tptp.set_node))
% 0.45/0.89  (declare-const tptp.produc1571934709de_val (-> tptp.val tptp.produc1432036078de_val tptp.produc1664334075de_val))
% 0.45/0.89  (declare-const tptp.irredu893086079de_val (-> (-> tptp.g tptp.list_node) (-> tptp.g tptp.node tptp.set_val) (-> tptp.g tptp.produc1432036078de_val tptp.option_list_val) tptp.g tptp.set_val tptp.set_Pr1311924359et_val))
% 0.45/0.89  (declare-const tptp.collec370342979de_val (-> (-> tptp.produc1432036078de_val Bool) tptp.set_Pr699757092de_val))
% 0.45/0.89  (declare-const tptp.zip_node_node (-> tptp.list_node tptp.list_node tptp.list_P1127016369e_node))
% 0.45/0.89  (declare-const tptp.transi1991289355lp_val (-> (-> tptp.val tptp.val Bool) tptp.val tptp.val Bool))
% 0.45/0.89  (declare-const tptp.sup_su2005730907et_val (-> tptp.set_Pr1311924359et_val tptp.set_Pr1311924359et_val tptp.set_Pr1311924359et_val))
% 0.45/0.89  (declare-const tptp.sup_su2138939728de_val (-> tptp.set_Pr699757092de_val tptp.set_Pr699757092de_val tptp.set_Pr699757092de_val))
% 0.45/0.89  (declare-const tptp.zip_node_set_val (-> tptp.list_node tptp.list_set_val tptp.list_P12184414et_val))
% 0.45/0.89  (declare-const tptp.transi1953622797et_val (-> tptp.set_Pr1311924359et_val Bool))
% 0.45/0.89  (declare-const tptp.member2110109140e_node (-> tptp.produc951622955e_node tptp.set_Pr9085835e_node Bool))
% 0.45/0.89  (declare-const tptp.dom_val_list_val (-> (-> tptp.val tptp.option_list_val) tptp.set_val))
% 0.45/0.89  (declare-const tptp.produc1446164855et_val (-> tptp.val tptp.set_val tptp.produc1858904199et_val))
% 0.45/0.89  (declare-const tptp.irredu681226810de_val (-> (-> tptp.g tptp.list_node) (-> tptp.g tptp.node tptp.set_val) (-> tptp.g tptp.produc1432036078de_val tptp.option_list_val) tptp.g tptp.set_val tptp.set_set_val))
% 0.45/0.89  (declare-const tptp.product_Pair_val_val (-> tptp.val tptp.val tptp.product_prod_val_val))
% 0.45/0.89  (declare-const tptp.irredu224829488eD_val (-> (-> tptp.g tptp.list_node) (-> tptp.g tptp.node tptp.list_P561207620_edgeD) (-> tptp.g tptp.node tptp.set_val) (-> tptp.g tptp.node tptp.set_val) (-> tptp.g tptp.produc1432036078de_val tptp.option_list_val) tptp.g tptp.set_val Bool))
% 0.45/0.89  (declare-const tptp.member1254968080et_val (-> tptp.produc1904584935et_val tptp.set_Pr1587248327et_val Bool))
% 0.45/0.89  (declare-const tptp.zip_node_val (-> tptp.list_node tptp.list_val tptp.list_P1820443774de_val))
% 0.45/0.89  (declare-const tptp.some_set_val (-> tptp.set_val tptp.option_set_val))
% 0.45/0.89  (declare-const tptp.sup_su1487070040et_val (-> tptp.option_set_val tptp.option_set_val tptp.option_set_val))
% 0.45/0.89  (declare-const tptp.ord_le596993316et_val (-> tptp.option_set_val tptp.option_set_val Bool))
% 0.45/0.89  (declare-const tptp.set_Pr1006393724et_val (-> tptp.list_P88441325et_val tptp.set_Pr1587248327et_val))
% 0.45/0.89  (define tptp.sSA_CF1899243830eD_val () (let ((_let_1 (@var "X" tptp.val))) (let ((_let_2 (@var "V3" tptp.val))) (let ((_let_3 (@var "G2" tptp.g))) (let ((_let_4 (@var "Phis" (-> tptp.g tptp.produc1432036078de_val tptp.option_list_val)))) (let ((_let_5 (@var "Defs" (-> tptp.g tptp.node tptp.set_val)))) (let ((_let_6 (@var "Alpha_n" (-> tptp.g tptp.list_node)))) (let ((_let_7 (@var "Uses" (-> tptp.g tptp.node tptp.set_val)))) (let ((_let_8 (@var "InEdges" (-> tptp.g tptp.node tptp.list_P561207620_edgeD)))) (lambda (@list _let_6 _let_8 _let_5 _let_7 _let_4 _let_3 _let_2) (exists (@list _let_1) (and (_ (_ tptp.member_val _let_1) (_ (_ (_ (_ (_ (_ tptp.sSA_CF1517915011eD_val _let_6) _let_8) _let_5) _let_7) _let_4) _let_3)) (_ (_ (_ (_ (_ (_ tptp.sSA_CF1909049442de_val _let_6) _let_5) _let_4) _let_3) _let_2) _let_1)))))))))))))
% 0.45/0.89  (define tptp.sSA_CF1660885746eD_val () (let ((_let_1 (@var "X" tptp.val))) (let ((_let_2 (@var "G2" tptp.g))) (let ((_let_3 (@var "Phis" (-> tptp.g tptp.produc1432036078de_val tptp.option_list_val)))) (let ((_let_4 (@var "Uses" (-> tptp.g tptp.node tptp.set_val)))) (let ((_let_5 (@var "Defs" (-> tptp.g tptp.node tptp.set_val)))) (let ((_let_6 (@var "InEdges" (-> tptp.g tptp.node tptp.list_P561207620_edgeD)))) (let ((_let_7 (@var "Alpha_n" (-> tptp.g tptp.list_node)))) (lambda (@list _let_7 _let_6 _let_5 _let_4 _let_3 _let_2) (exists (@list _let_1) (and (_ (_ tptp.member_val _let_1) (_ (_ (_ (_ (_ (_ tptp.sSA_CF1517915011eD_val _let_7) _let_6) _let_5) _let_4) _let_3) _let_2)) (_ (_ (_ (_ (_ (_ (_ tptp.sSA_CF1899243830eD_val _let_7) _let_6) _let_5) _let_4) _let_3) _let_2) _let_1))))))))))))
% 0.45/0.89  (define tptp.sSA_CF2074824714de_val () (let ((_let_1 (@var "Val2" tptp.val))) (let ((_let_2 (@var "G2" tptp.g))) (let ((_let_3 (@var "Phis" (-> tptp.g tptp.produc1432036078de_val tptp.option_list_val)))) (let ((_let_4 (@var "Uses" (-> tptp.g tptp.node tptp.set_val)))) (let ((_let_5 (@var "Defs" (-> tptp.g tptp.node tptp.set_val)))) (let ((_let_6 (@var "Alpha_n" (-> tptp.g tptp.list_node)))) (let ((_let_7 (@var "X" tptp.node))) (lambda (@list _let_6 _let_5 _let_4 _let_3 _let_2) (forall (@list _let_7) (=> (_ (_ tptp.member_node _let_7) (_ tptp.set_node2 (_ _let_6 _let_2))) (forall (@list _let_1) (=> (_ (_ tptp.member_val _let_1) (_ (_ (_ tptp.sSA_CF370335846de_val _let_3) _let_2) _let_7)) (_ (_ (_ (_ (_ (_ tptp.sSA_CF794421325de_val _let_6) _let_5) _let_4) _let_3) _let_2) _let_1))))))))))))))
% 0.45/0.89  (define tptp.sSA_CF139593942de_val () (let ((_let_1 (@var "N3" tptp.node))) (let ((_let_2 (@var "G2" tptp.g))) (let ((_let_3 (@var "Phis" (-> tptp.g tptp.produc1432036078de_val tptp.option_list_val)))) (let ((_let_4 (@var "Defs" (-> tptp.g tptp.node tptp.set_val)))) (lambda (@list _let_4 _let_3 _let_2 _let_1) (_ (_ tptp.sup_sup_set_val (_ (_ _let_4 _let_2) _let_1)) (_ (_ (_ tptp.sSA_CF370335846de_val _let_3) _let_2) _let_1))))))))
% 0.45/0.89  (define tptp.sSA_CF178745443eD_val () (let ((_let_1 (@var "N3" tptp.node))) (let ((_let_2 (@var "G2" tptp.g))) (let ((_let_3 (@var "Phis" (-> tptp.g tptp.produc1432036078de_val tptp.option_list_val)))) (let ((_let_4 (@var "InEdges" (-> tptp.g tptp.node tptp.list_P561207620_edgeD)))) (let ((_let_5 (@var "Alpha_n" (-> tptp.g tptp.list_node)))) (let ((_let_6 (@var "Uses" (-> tptp.g tptp.node tptp.set_val)))) (lambda (@list _let_5 _let_4 _let_6 _let_3 _let_2 _let_1) (_ (_ tptp.sup_sup_set_val (_ (_ _let_6 _let_2) _let_1)) (_ (_ (_ (_ (_ tptp.sSA_CF848637139eD_val _let_5) _let_4) _let_3) _let_2) _let_1))))))))))
% 0.45/0.89  (define tptp.sSA_CF262257161de_val () (let ((_let_1 (@var "V3" tptp.val))) (let ((_let_2 (@var "G2" tptp.g))) (let ((_let_3 (@var "Phis" (-> tptp.g tptp.produc1432036078de_val tptp.option_list_val)))) (let ((_let_4 (@var "Defs" (-> tptp.g tptp.node tptp.set_val)))) (let ((_let_5 (@var "Alpha_n" (-> tptp.g tptp.list_node)))) (lambda (@list _let_5 _let_4 _let_3 _let_2 _let_1) (_ (_ _let_3 _let_2) (_ (_ tptp.produc1470527136de_val (_ (_ (_ (_ (_ tptp.sSA_CF551432799de_val _let_5) _let_4) _let_3) _let_2) _let_1)) _let_1)))))))))
% 0.45/0.89  (define tptp.sSA_CF1252180629de_val () (let ((_let_1 (@var "Vs2" tptp.list_val))) (let ((_let_2 (@var "V4" tptp.val))) (let ((_let_3 (@var "V3" tptp.val))) (let ((_let_4 (@var "G2" tptp.g))) (let ((_let_5 (@var "Phis" (-> tptp.g tptp.produc1432036078de_val tptp.option_list_val)))) (let ((_let_6 (@var "Defs" (-> tptp.g tptp.node tptp.set_val)))) (let ((_let_7 (@var "Alpha_n" (-> tptp.g tptp.list_node)))) (lambda (@list _let_7 _let_6 _let_5 _let_4 _let_3 _let_2) (exists (@list _let_1) (and (= (_ (_ (_ (_ (_ tptp.sSA_CF262257161de_val _let_7) _let_6) _let_5) _let_4) _let_3) (_ tptp.some_list_val _let_1)) (_ (_ tptp.member_val _let_2) (_ tptp.set_val2 _let_1)))))))))))))
% 0.45/0.89  (define tptp.ord_less_eq_set_node () (let ((_let_1 (@var "B4" tptp.set_node))) (let ((_let_2 (@var "T2" tptp.node))) (let ((_let_3 (_ tptp.member_node _let_2))) (let ((_let_4 (@var "A5" tptp.set_node))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1)))))))))
% 0.45/0.89  (define tptp.ord_le1742111550et_val () (let ((_let_1 (@var "B4" tptp.set_set_val))) (let ((_let_2 (@var "T2" tptp.set_val))) (let ((_let_3 (_ tptp.member_set_val _let_2))) (let ((_let_4 (@var "A5" tptp.set_set_val))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1)))))))))
% 0.45/0.89  (define tptp.ord_le1643692676de_val () (let ((_let_1 (@var "B4" tptp.set_Pr699757092de_val))) (let ((_let_2 (@var "T2" tptp.produc1432036078de_val))) (let ((_let_3 (_ tptp.member313544709de_val _let_2))) (let ((_let_4 (@var "A5" tptp.set_Pr699757092de_val))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1)))))))))
% 0.45/0.89  (define tptp.ord_le299366439et_val () (let ((_let_1 (@var "B4" tptp.set_Pr1311924359et_val))) (let ((_let_2 (@var "T2" tptp.produc1324971431et_val))) (let ((_let_3 (_ tptp.member1711426256et_val _let_2))) (let ((_let_4 (@var "A5" tptp.set_Pr1311924359et_val))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1)))))))))
% 0.45/0.89  (define tptp.ord_less_eq_set_val () (let ((_let_1 (@var "B4" tptp.set_val))) (let ((_let_2 (@var "T2" tptp.val))) (let ((_let_3 (_ tptp.member_val _let_2))) (let ((_let_4 (@var "A5" tptp.set_val))) (lambda (@list _let_4 _let_1) (forall (@list _let_2) (=> (_ _let_3 _let_4) (_ _let_3 _let_1)))))))))
% 0.45/0.89  (define @t1 () (_ (_ (_ tptp.sSA_CF1252180629de_val tptp.alpha_n) tptp.defs) tptp.phis))
% 0.45/0.89  (define @t2 () (_ @t1 tptp.g2))
% 0.45/0.89  (define @t3 () (_ (_ (_ (_ (_ tptp.sSA_CF1517915011eD_val tptp.alpha_n) tptp.inEdges) tptp.defs) tptp.uses) tptp.phis))
% 0.45/0.89  (define @t4 () (_ @t3 tptp.g2))
% 0.45/0.89  (define @t5 () (@var "Phi" tptp.val))
% 0.45/0.89  (define @t6 () (@var "G" tptp.g))
% 0.45/0.89  (define @t7 () (_ @t3 @t6))
% 0.45/0.89  (define @t8 () (@var "V2" tptp.val))
% 0.45/0.89  (define @t9 () (_ tptp.member_val @t8))
% 0.45/0.89  (define @t10 () (_ @t9 @t7))
% 0.45/0.89  (define @t11 () (@var "V" tptp.val))
% 0.45/0.89  (define @t12 () (_ @t1 @t6))
% 0.45/0.89  (define @t13 () (_ @t12 @t11))
% 0.45/0.89  (define @t14 () (_ @t13 @t8))
% 0.45/0.89  (define @t15 () (=> @t14 @t10))
% 0.45/0.89  (define @t16 () (@list @t6 @t11 @t8))
% 0.45/0.89  (define @t17 () (forall @t16 @t15))
% 0.45/0.89  (define @t18 () (_ (_ (_ tptp.sSA_CF655860150de_val tptp.alpha_n) tptp.uses) @t6))
% 0.45/0.89  (define @t19 () (_ tptp.member_val @t11))
% 0.45/0.89  (define @t20 () (_ @t19 @t18))
% 0.45/0.89  (define @t21 () (@var "N" tptp.node))
% 0.45/0.89  (define @t22 () (_ tptp.uses @t6))
% 0.45/0.89  (define @t23 () (_ @t22 @t21))
% 0.45/0.89  (define @t24 () (_ @t19 @t23))
% 0.45/0.89  (define @t25 () (@list @t11 @t6 @t21))
% 0.45/0.89  (define @t26 () (_ @t19 @t7))
% 0.45/0.89  (define @t27 () (_ (_ (_ (_ (_ (_ tptp.sSA_CF1899243830eD_val tptp.alpha_n) tptp.inEdges) tptp.defs) tptp.uses) tptp.phis) @t6))
% 0.45/0.89  (define @t28 () (_ @t27 @t11))
% 0.45/0.89  (define @t29 () (@list @t6 @t11))
% 0.45/0.89  (define @t30 () (_ (_ (_ (_ (_ tptp.sSA_CF794421325de_val tptp.alpha_n) tptp.defs) tptp.uses) tptp.phis) @t6))
% 0.45/0.89  (define @t31 () (_ @t30 @t11))
% 0.45/0.89  (define @t32 () (@list @t6))
% 0.45/0.89  (define @t33 () (_ (_ (_ (_ (_ (_ tptp.sSA_CF178745443eD_val tptp.alpha_n) tptp.inEdges) tptp.uses) tptp.phis) @t6) @t21))
% 0.45/0.89  (define @t34 () (_ @t19 @t33))
% 0.45/0.89  (define @t35 () (@var "X" tptp.val))
% 0.45/0.89  (define @t36 () (_ tptp.member_val @t35))
% 0.45/0.89  (define @t37 () (_ @t36 @t7))
% 0.45/0.89  (define @t38 () (@list @t35))
% 0.45/0.89  (define @t39 () (_ (_ (_ tptp.sSA_CF551432799de_val tptp.alpha_n) tptp.defs) tptp.phis))
% 0.45/0.89  (define @t40 () (_ @t39 tptp.g2))
% 0.45/0.89  (define @t41 () (_ tptp.defs @t6))
% 0.45/0.89  (define @t42 () (_ @t41 @t21))
% 0.45/0.89  (define @t43 () (_ @t19 @t42))
% 0.45/0.89  (define @t44 () (_ tptp.set_node2 (_ tptp.alpha_n @t6)))
% 0.45/0.89  (define @t45 () (_ tptp.member_node @t21))
% 0.45/0.89  (define @t46 () (_ @t45 @t44))
% 0.45/0.89  (define @t47 () (@list @t21 @t6 @t11))
% 0.45/0.89  (define @t48 () (@var "Q" tptp.val))
% 0.45/0.89  (define @t49 () (_ @t39 @t6))
% 0.45/0.89  (define @t50 () (_ @t49 @t48))
% 0.45/0.89  (define @t51 () (@var "P" tptp.val))
% 0.45/0.89  (define @t52 () (_ @t49 @t51))
% 0.45/0.89  (define @t53 () (= @t52 @t50))
% 0.45/0.89  (define @t54 () (_ (_ tptp.member_val @t51) @t7))
% 0.45/0.89  (define @t55 () (not (= @t51 @t48)))
% 0.45/0.89  (define @t56 () (_ @t12 @t51))
% 0.45/0.89  (define @t57 () (_ @t56 @t48))
% 0.45/0.89  (define @t58 () (@list @t6 @t51 @t48))
% 0.45/0.89  (define @t59 () (@var "R" tptp.val))
% 0.45/0.89  (define @t60 () (@list @t6 @t21))
% 0.45/0.89  (define @t61 () (@var "N2" tptp.node))
% 0.45/0.89  (define @t62 () (_ @t22 @t61))
% 0.45/0.89  (define @t63 () (_ tptp.member_node @t61))
% 0.45/0.89  (define @t64 () (_ @t63 @t44))
% 0.45/0.89  (define @t65 () (@list @t61))
% 0.45/0.89  (define @t66 () (@list @t11 @t6))
% 0.45/0.89  (define @t67 () (@var "Val" tptp.val))
% 0.45/0.89  (define @t68 () (_ tptp.member_val @t67))
% 0.45/0.89  (define @t69 () (@var "V4" tptp.val))
% 0.45/0.89  (define @t70 () (@var "V3" tptp.val))
% 0.45/0.89  (define @t71 () (@var "A" tptp.val))
% 0.45/0.89  (define @t72 () (@list @t70 @t69))
% 0.45/0.89  (define @t73 () (@var "N3" tptp.node))
% 0.45/0.89  (define @t74 () (@var "Val2" tptp.val))
% 0.45/0.89  (define @t75 () (_ tptp.member_val @t74))
% 0.45/0.89  (define @t76 () (_ tptp.member_node @t73))
% 0.45/0.89  (define @t77 () (@list @t73 @t74))
% 0.45/0.89  (define @t78 () (_ @t30 @t71))
% 0.45/0.89  (define @t79 () (@list @t6 @t71))
% 0.45/0.89  (define @t80 () (@var "X2" tptp.val))
% 0.45/0.89  (define @t81 () (@var "P2" (-> tptp.val Bool)))
% 0.45/0.89  (define @t82 () (_ @t81 @t80))
% 0.45/0.89  (define @t83 () (@var "V6" tptp.val))
% 0.45/0.89  (define @t84 () (_ @t81 @t83))
% 0.45/0.89  (define @t85 () (@var "V5" tptp.val))
% 0.45/0.89  (define @t86 () (_ @t12 @t85))
% 0.45/0.89  (define @t87 () (_ @t81 @t85))
% 0.45/0.89  (define @t88 () (_ @t30 @t85))
% 0.45/0.89  (define @t89 () (@list @t85 @t83))
% 0.45/0.89  (define @t90 () (@var "Val3" tptp.val))
% 0.45/0.89  (define @t91 () (_ @t81 @t90))
% 0.45/0.89  (define @t92 () (_ tptp.member_val @t90))
% 0.45/0.89  (define @t93 () (@list @t61 @t90))
% 0.45/0.89  (define @t94 () (@list @t85))
% 0.45/0.89  (define @t95 () (_ tptp.member_val @t71))
% 0.45/0.89  (define @t96 () (@list @t21 @t6))
% 0.45/0.89  (define @t97 () (_ @t49 @t11))
% 0.45/0.89  (define @t98 () (=> @t46 @t26))
% 0.45/0.89  (define @t99 () (_ (_ (_ (_ tptp.sSA_CF848637139eD_val tptp.alpha_n) tptp.inEdges) tptp.phis) @t6))
% 0.45/0.89  (define @t100 () (_ @t99 @t21))
% 0.45/0.89  (define @t101 () (_ @t19 @t100))
% 0.45/0.89  (define @t102 () (_ (_ (_ tptp.sSA_CF139593942de_val tptp.defs) tptp.phis) @t6))
% 0.45/0.89  (define @t103 () (@var "X3" tptp.node))
% 0.45/0.89  (define @t104 () (@var "Y" tptp.node))
% 0.45/0.89  (define @t105 () (_ @t19 (_ @t102 @t103)))
% 0.45/0.89  (define @t106 () (_ tptp.member_node @t103))
% 0.45/0.89  (define @t107 () (_ @t106 @t44))
% 0.45/0.89  (define @t108 () (@list @t103))
% 0.45/0.89  (define @t109 () (@var "Xs" tptp.list_P844977291de_val))
% 0.45/0.89  (define @t110 () (@var "Xs" tptp.list_P761482893et_val))
% 0.45/0.89  (define @t111 () (@var "Xs" tptp.list_P1078858818l_node))
% 0.45/0.89  (define @t112 () (@var "Xs" tptp.list_P1811375021al_val))
% 0.45/0.89  (define @t113 () (@var "Xs" tptp.list_set_val))
% 0.45/0.89  (define @t114 () (_ tptp.set_set_val2 @t113))
% 0.45/0.89  (define @t115 () (@var "Xs" tptp.list_node))
% 0.45/0.89  (define @t116 () (_ tptp.set_node2 @t115))
% 0.45/0.89  (define @t117 () (@var "Xs" tptp.list_val))
% 0.45/0.89  (define @t118 () (_ tptp.set_val2 @t117))
% 0.45/0.89  (define @t119 () (@var "Xs" tptp.list_P2089461677et_val))
% 0.45/0.89  (define @t120 () (_ tptp.set_Pr284769596et_val @t119))
% 0.45/0.89  (define @t121 () (@var "Xs" tptp.list_P1820443774de_val))
% 0.45/0.89  (define @t122 () (_ tptp.set_Pr1085970585de_val @t121))
% 0.45/0.89  (define @t123 () (_ (_ tptp.sSA_CF370335846de_val tptp.phis) @t6))
% 0.45/0.89  (define @t124 () (_ @t123 @t21))
% 0.45/0.89  (define @t125 () (_ @t102 @t21))
% 0.45/0.89  (define @t126 () (_ tptp.var2 tptp.g2))
% 0.45/0.89  (define @t127 () (_ @t126 tptp.phi))
% 0.45/0.89  (define @t128 () (_ @t19 @t125))
% 0.45/0.89  (define @t129 () (@var "M" tptp.node))
% 0.45/0.89  (define @t130 () (_ tptp.member_node @t129))
% 0.45/0.89  (define @t131 () (@var "A" tptp.produc1946948786l_node))
% 0.45/0.89  (define @t132 () (@var "P2" (-> tptp.produc1946948786l_node Bool)))
% 0.45/0.89  (define @t133 () (@var "A" tptp.product_prod_val_val))
% 0.45/0.89  (define @t134 () (@var "P2" (-> tptp.product_prod_val_val Bool)))
% 0.45/0.89  (define @t135 () (_ tptp.collect_val @t81))
% 0.45/0.89  (define @t136 () (@var "A" tptp.node))
% 0.45/0.89  (define @t137 () (@var "P2" (-> tptp.node Bool)))
% 0.45/0.89  (define @t138 () (_ tptp.member_node @t136))
% 0.45/0.89  (define @t139 () (@var "A" tptp.set_val))
% 0.45/0.89  (define @t140 () (@var "P2" (-> tptp.set_val Bool)))
% 0.45/0.89  (define @t141 () (_ tptp.member_set_val @t139))
% 0.45/0.89  (define @t142 () (@var "A" tptp.produc1432036078de_val))
% 0.45/0.89  (define @t143 () (@var "P2" (-> tptp.produc1432036078de_val Bool)))
% 0.45/0.89  (define @t144 () (_ tptp.member313544709de_val @t142))
% 0.45/0.89  (define @t145 () (@var "A" tptp.produc1324971431et_val))
% 0.45/0.89  (define @t146 () (@var "P2" (-> tptp.produc1324971431et_val Bool)))
% 0.45/0.89  (define @t147 () (_ tptp.member1711426256et_val @t145))
% 0.45/0.89  (define @t148 () (@var "A2" tptp.set_val))
% 0.45/0.89  (define @t149 () (_ @t36 @t148))
% 0.45/0.89  (define @t150 () (@list @t148))
% 0.45/0.89  (define @t151 () (@var "A2" tptp.set_node))
% 0.45/0.89  (define @t152 () (@var "X" tptp.node))
% 0.45/0.89  (define @t153 () (_ tptp.member_node @t152))
% 0.45/0.89  (define @t154 () (@list @t152))
% 0.45/0.89  (define @t155 () (@list @t151))
% 0.45/0.89  (define @t156 () (@var "A2" tptp.set_set_val))
% 0.45/0.89  (define @t157 () (@var "X" tptp.set_val))
% 0.45/0.89  (define @t158 () (_ tptp.member_set_val @t157))
% 0.45/0.89  (define @t159 () (@list @t157))
% 0.45/0.89  (define @t160 () (@list @t156))
% 0.45/0.89  (define @t161 () (@var "A2" tptp.set_Pr699757092de_val))
% 0.45/0.89  (define @t162 () (@var "X" tptp.produc1432036078de_val))
% 0.45/0.89  (define @t163 () (_ tptp.member313544709de_val @t162))
% 0.45/0.89  (define @t164 () (@list @t162))
% 0.45/0.89  (define @t165 () (@list @t161))
% 0.45/0.89  (define @t166 () (@var "A2" tptp.set_Pr1311924359et_val))
% 0.45/0.89  (define @t167 () (@var "X" tptp.produc1324971431et_val))
% 0.45/0.89  (define @t168 () (_ tptp.member1711426256et_val @t167))
% 0.45/0.89  (define @t169 () (@list @t167))
% 0.45/0.89  (define @t170 () (@list @t166))
% 0.45/0.89  (define @t171 () (_ tptp.var2 @t6))
% 0.45/0.89  (define @t172 () (_ @t171 @t51))
% 0.45/0.89  (define @t173 () (_ @t171 @t48))
% 0.45/0.89  (define @t174 () (= (_ @t171 @t8) (_ @t171 @t11)))
% 0.45/0.89  (define @t175 () (_ tptp.member_val @t48))
% 0.45/0.89  (define @t176 () (@list @t74))
% 0.45/0.89  (define @t177 () (@var "Xs2" tptp.list_node))
% 0.45/0.89  (define @t178 () (_ tptp.finite_finite_node @t151))
% 0.45/0.89  (define @t179 () (@var "Xs2" tptp.list_val))
% 0.45/0.89  (define @t180 () (_ tptp.finite_finite_val @t148))
% 0.45/0.89  (define @t181 () (@var "Xs2" tptp.list_P2089461677et_val))
% 0.45/0.89  (define @t182 () (_ tptp.finite79836624et_val @t166))
% 0.45/0.89  (define @t183 () (@var "Xs2" tptp.list_P1820443774de_val))
% 0.45/0.89  (define @t184 () (_ tptp.finite2056463621de_val @t161))
% 0.45/0.89  (define @t185 () (@var "Phis2" (-> tptp.g tptp.produc1432036078de_val tptp.option_list_val)))
% 0.45/0.89  (define @t186 () (@var "Uses2" (-> tptp.g tptp.node tptp.set_val)))
% 0.45/0.89  (define @t187 () (@var "Defs2" (-> tptp.g tptp.node tptp.set_val)))
% 0.45/0.89  (define @t188 () (@var "Alpha_n2" (-> tptp.g tptp.list_node)))
% 0.45/0.89  (define @t189 () (_ (_ (_ (_ (_ tptp.sSA_CF794421325de_val @t188) @t187) @t186) @t185) @t6))
% 0.45/0.89  (define @t190 () (_ @t186 @t6))
% 0.45/0.89  (define @t191 () (_ tptp.set_node2 (_ @t188 @t6)))
% 0.45/0.89  (define @t192 () (_ (_ (_ (_ tptp.sSA_CF1252180629de_val @t188) @t187) @t185) @t6))
% 0.45/0.89  (define @t193 () (_ @t192 @t85))
% 0.45/0.89  (define @t194 () (_ @t189 @t85))
% 0.45/0.89  (define @t195 () (_ @t190 @t61))
% 0.45/0.89  (define @t196 () (_ @t63 @t191))
% 0.45/0.89  (define @t197 () (@var "G2" tptp.g))
% 0.45/0.89  (define @t198 () (@var "Phis" (-> tptp.g tptp.produc1432036078de_val tptp.option_list_val)))
% 0.45/0.89  (define @t199 () (@var "Defs" (-> tptp.g tptp.node tptp.set_val)))
% 0.45/0.89  (define @t200 () (@var "Alpha_n" (-> tptp.g tptp.list_node)))
% 0.45/0.89  (define @t201 () (@var "Uses" (-> tptp.g tptp.node tptp.set_val)))
% 0.45/0.89  (define @t202 () (_ (_ (_ (_ (_ tptp.sSA_CF794421325de_val @t200) @t199) @t201) @t198) @t197))
% 0.45/0.89  (define @t203 () (@var "A3" tptp.val))
% 0.45/0.89  (define @t204 () (_ (_ @t201 @t197) @t73))
% 0.45/0.89  (define @t205 () (_ tptp.set_node2 (_ @t200 @t197)))
% 0.45/0.89  (define @t206 () (@var "P2" tptp.set_val))
% 0.45/0.89  (define @t207 () (_ (_ (_ (_ (_ tptp.irredu893086079de_val tptp.alpha_n) tptp.defs) tptp.phis) @t6) @t206))
% 0.45/0.89  (define @t208 () (@list @t6 @t206))
% 0.45/0.89  (define @t209 () (_ (_ tptp.graph_272749361_edgeD tptp.inEdges) @t6))
% 0.45/0.89  (define @t210 () (@var "M2" tptp.node))
% 0.45/0.89  (define @t211 () (@var "N" tptp.val))
% 0.45/0.89  (define @t212 () (@var "Phi2" tptp.val))
% 0.45/0.89  (define @t213 () (_ (_ (_ (_ tptp.sSA_CF262257161de_val tptp.alpha_n) tptp.defs) tptp.phis) @t6))
% 0.45/0.89  (define @t214 () (_ @t213 @t11))
% 0.45/0.89  (define @t215 () (= @t214 tptp.none_list_val))
% 0.45/0.89  (define @t216 () (not @t215))
% 0.45/0.89  (define @t217 () (@var "G3" tptp.set_Pr1311924359et_val))
% 0.45/0.89  (define @t218 () (_ tptp.finite79836624et_val @t217))
% 0.45/0.89  (define @t219 () (@var "F" tptp.set_Pr1311924359et_val))
% 0.45/0.89  (define @t220 () (_ tptp.finite79836624et_val @t219))
% 0.45/0.89  (define @t221 () (_ tptp.finite79836624et_val (_ (_ tptp.sup_su2005730907et_val @t219) @t217)))
% 0.45/0.89  (define @t222 () (@list @t219 @t217))
% 0.45/0.89  (define @t223 () (@var "G3" tptp.set_Pr699757092de_val))
% 0.45/0.89  (define @t224 () (_ tptp.finite2056463621de_val @t223))
% 0.45/0.89  (define @t225 () (@var "F" tptp.set_Pr699757092de_val))
% 0.45/0.89  (define @t226 () (_ tptp.finite2056463621de_val @t225))
% 0.45/0.89  (define @t227 () (_ tptp.finite2056463621de_val (_ (_ tptp.sup_su2138939728de_val @t225) @t223)))
% 0.45/0.89  (define @t228 () (@list @t225 @t223))
% 0.45/0.89  (define @t229 () (@var "G3" tptp.set_val))
% 0.45/0.89  (define @t230 () (_ tptp.finite_finite_val @t229))
% 0.45/0.89  (define @t231 () (@var "F" tptp.set_val))
% 0.45/0.89  (define @t232 () (_ tptp.finite_finite_val @t231))
% 0.45/0.89  (define @t233 () (_ tptp.finite_finite_val (_ (_ tptp.sup_sup_set_val @t231) @t229)))
% 0.45/0.89  (define @t234 () (@list @t231 @t229))
% 0.45/0.89  (define @t235 () (_ tptp.member_val @t83))
% 0.45/0.89  (define @t236 () (_ @t235 (_ @t99 @t129)))
% 0.45/0.89  (define @t237 () (@list @t83))
% 0.45/0.89  (define @t238 () (@var "T" tptp.set_Pr1311924359et_val))
% 0.45/0.89  (define @t239 () (not (_ tptp.finite79836624et_val @t238)))
% 0.45/0.89  (define @t240 () (@var "S" tptp.set_Pr1311924359et_val))
% 0.45/0.89  (define @t241 () (not (_ tptp.finite79836624et_val @t240)))
% 0.45/0.89  (define @t242 () (not (_ tptp.finite79836624et_val (_ (_ tptp.sup_su2005730907et_val @t240) @t238))))
% 0.45/0.89  (define @t243 () (@list @t240 @t238))
% 0.45/0.89  (define @t244 () (@var "T" tptp.set_Pr699757092de_val))
% 0.45/0.89  (define @t245 () (not (_ tptp.finite2056463621de_val @t244)))
% 0.45/0.89  (define @t246 () (@var "S" tptp.set_Pr699757092de_val))
% 0.45/0.89  (define @t247 () (not (_ tptp.finite2056463621de_val @t246)))
% 0.45/0.89  (define @t248 () (not (_ tptp.finite2056463621de_val (_ (_ tptp.sup_su2138939728de_val @t246) @t244))))
% 0.45/0.89  (define @t249 () (@list @t246 @t244))
% 0.45/0.89  (define @t250 () (@var "T" tptp.set_val))
% 0.45/0.89  (define @t251 () (not (_ tptp.finite_finite_val @t250)))
% 0.45/0.89  (define @t252 () (@var "S" tptp.set_val))
% 0.45/0.89  (define @t253 () (not (_ tptp.finite_finite_val @t252)))
% 0.45/0.89  (define @t254 () (not (_ tptp.finite_finite_val (_ (_ tptp.sup_sup_set_val @t252) @t250))))
% 0.45/0.89  (define @t255 () (@list @t252 @t250))
% 0.45/0.89  (define @t256 () (@var "Vs" tptp.list_val))
% 0.45/0.89  (define @t257 () (_ tptp.some_list_val @t256))
% 0.45/0.89  (define @t258 () (= @t214 @t257))
% 0.45/0.89  (define @t259 () (_ tptp.phis @t6))
% 0.45/0.89  (define @t260 () (@var "Vs2" tptp.list_val))
% 0.45/0.89  (define @t261 () (_ tptp.set_val2 @t260))
% 0.45/0.89  (define @t262 () (_ tptp.some_list_val @t260))
% 0.45/0.89  (define @t263 () (@list @t260))
% 0.45/0.89  (define @t264 () (_ tptp.dom_val_list_val @t213))
% 0.45/0.89  (define @t265 () (@var "Scc" tptp.set_val))
% 0.45/0.89  (define @t266 () (_ tptp.member_val @t80))
% 0.45/0.89  (define @t267 () (_ (_ (_ (_ (_ tptp.irredu681226810de_val tptp.alpha_n) tptp.defs) tptp.phis) @t6) @t206))
% 0.45/0.89  (define @t268 () (_ (_ tptp.member_set_val @t265) @t267))
% 0.45/0.89  (define @t269 () (_ (_ (_ (_ (_ (_ (_ tptp.irredu224829488eD_val tptp.alpha_n) tptp.inEdges) tptp.defs) tptp.uses) tptp.phis) @t6) @t206))
% 0.45/0.89  (define @t270 () (@var "Vs3" tptp.list_val))
% 0.45/0.89  (define @t271 () (@var "N4" tptp.node))
% 0.45/0.89  (define @t272 () (_ tptp.produc1470527136de_val @t271))
% 0.45/0.89  (define @t273 () (= (_ @t259 (_ @t272 @t11)) (_ tptp.some_list_val @t270)))
% 0.45/0.89  (define @t274 () (_ (_ tptp.produc1470527136de_val @t21) @t11))
% 0.45/0.89  (define @t275 () (= (_ @t259 @t274) @t257))
% 0.45/0.89  (define @t276 () (@list @t6 @t21 @t11 @t256 @t271 @t270))
% 0.45/0.89  (define @t277 () (@list @t6 @t21 @t11 @t256))
% 0.45/0.89  (define @t278 () (_ tptp.set_val2 @t256))
% 0.45/0.89  (define @t279 () (_ @t130 (_ tptp.set_node2 (_ @t209 @t21))))
% 0.45/0.89  (define @t280 () (_ tptp.member313544709de_val @t274))
% 0.45/0.89  (define @t281 () (@var "Y2" tptp.list_val))
% 0.45/0.89  (define @t282 () (@var "X2" tptp.option_list_val))
% 0.45/0.89  (define @t283 () (= @t282 (_ tptp.some_list_val @t281)))
% 0.45/0.89  (define @t284 () (@list @t281))
% 0.45/0.89  (define @t285 () (= @t282 tptp.none_list_val))
% 0.45/0.89  (define @t286 () (@list @t282))
% 0.45/0.89  (define @t287 () (@var "Y3" tptp.set_val))
% 0.45/0.89  (define @t288 () (@var "X2" tptp.set_val))
% 0.45/0.89  (define @t289 () (_ tptp.sup_sup_set_val @t288))
% 0.45/0.89  (define @t290 () (_ @t289 @t287))
% 0.45/0.89  (define @t291 () (_ tptp.some_set_val @t287))
% 0.45/0.89  (define @t292 () (_ tptp.some_set_val @t288))
% 0.45/0.89  (define @t293 () (@list @t288 @t287))
% 0.45/0.89  (define @t294 () (@var "Y22" tptp.list_val))
% 0.45/0.89  (define @t295 () (@var "X22" tptp.list_val))
% 0.45/0.89  (define @t296 () (_ tptp.some_list_val @t295))
% 0.45/0.89  (define @t297 () (_ tptp.ord_less_eq_set_val @t288))
% 0.45/0.89  (define @t298 () (_ @t297 @t287))
% 0.45/0.89  (define @t299 () (@var "B" tptp.produc1324971431et_val))
% 0.45/0.89  (define @t300 () (@var "B" tptp.node))
% 0.45/0.89  (define @t301 () (_ tptp.zip_node_node @t115))
% 0.45/0.89  (define @t302 () (@var "B" tptp.val))
% 0.45/0.89  (define @t303 () (_ tptp.zip_val_val @t117))
% 0.45/0.89  (define @t304 () (@var "B" tptp.produc1432036078de_val))
% 0.45/0.89  (define @t305 () (@var "B" tptp.set_val))
% 0.45/0.89  (define @t306 () (_ tptp.zip_set_val_set_val @t113))
% 0.45/0.89  (define @t307 () (@var "Scc2" tptp.set_val))
% 0.45/0.89  (define @t308 () (@var "Vs4" tptp.list_val))
% 0.45/0.89  (define @t309 () (@var "N5" tptp.node))
% 0.45/0.89  (define @t310 () (_ (_ (_ tptp.graph_1037173556_edgeD tptp.alpha_n) tptp.inEdges) @t6))
% 0.45/0.89  (define @t311 () (@var "Xa" tptp.node))
% 0.45/0.89  (define @t312 () (= @t103 @t311))
% 0.45/0.89  (define @t313 () (_ (_ tptp.member_node @t311) @t151))
% 0.45/0.89  (define @t314 () (@list @t311))
% 0.45/0.89  (define @t315 () (_ tptp.ord_less_eq_node @t103))
% 0.45/0.89  (define @t316 () (_ @t106 @t151))
% 0.45/0.89  (define @t317 () (_ @t138 @t151))
% 0.45/0.89  (define @t318 () (@list @t151 @t136))
% 0.45/0.89  (define @t319 () (@var "Xa" tptp.val))
% 0.45/0.89  (define @t320 () (@var "X3" tptp.val))
% 0.45/0.89  (define @t321 () (= @t320 @t319))
% 0.45/0.89  (define @t322 () (_ (_ tptp.member_val @t319) @t148))
% 0.45/0.89  (define @t323 () (@list @t319))
% 0.45/0.89  (define @t324 () (forall @t323 (=> @t322 (=> (_ (_ tptp.ord_less_eq_val @t319) @t320) @t321))))
% 0.45/0.89  (define @t325 () (_ tptp.ord_less_eq_val @t320))
% 0.45/0.89  (define @t326 () (_ tptp.member_val @t320))
% 0.45/0.89  (define @t327 () (_ @t326 @t148))
% 0.45/0.89  (define @t328 () (@list @t320))
% 0.45/0.89  (define @t329 () (_ @t95 @t148))
% 0.45/0.89  (define @t330 () (@list @t148 @t71))
% 0.45/0.89  (define @t331 () (@var "Xa" tptp.set_val))
% 0.45/0.89  (define @t332 () (@var "X3" tptp.set_val))
% 0.45/0.89  (define @t333 () (= @t332 @t331))
% 0.45/0.89  (define @t334 () (_ (_ tptp.member_set_val @t331) @t156))
% 0.45/0.89  (define @t335 () (@list @t331))
% 0.45/0.89  (define @t336 () (forall @t335 (=> @t334 (=> (_ (_ tptp.ord_less_eq_set_val @t331) @t332) @t333))))
% 0.45/0.89  (define @t337 () (_ tptp.ord_less_eq_set_val @t332))
% 0.45/0.89  (define @t338 () (_ tptp.member_set_val @t332))
% 0.45/0.89  (define @t339 () (_ @t338 @t156))
% 0.45/0.89  (define @t340 () (@list @t332))
% 0.45/0.89  (define @t341 () (_ @t141 @t156))
% 0.45/0.89  (define @t342 () (_ tptp.finite1265617511et_val @t156))
% 0.45/0.89  (define @t343 () (@list @t156 @t139))
% 0.45/0.89  (define @t344 () (forall @t323 (=> @t322 (=> (_ @t325 @t319) @t321))))
% 0.45/0.89  (define @t345 () (forall @t335 (=> @t334 (=> (_ @t337 @t331) @t333))))
% 0.45/0.89  (define @t346 () (_ tptp.ord_less_eq_set_val @t139))
% 0.45/0.89  (define @t347 () (@var "B2" tptp.set_set_val))
% 0.45/0.89  (define @t348 () (@var "B2" tptp.set_Pr1311924359et_val))
% 0.45/0.89  (define @t349 () (@var "B2" tptp.set_node))
% 0.45/0.89  (define @t350 () (@var "B2" tptp.set_Pr699757092de_val))
% 0.45/0.89  (define @t351 () (@var "B2" tptp.set_val))
% 0.45/0.89  (define @t352 () (_ @t36 @t351))
% 0.45/0.89  (define @t353 () (_ (_ tptp.ord_le299366439et_val @t166) @t348))
% 0.45/0.89  (define @t354 () (_ tptp.finite79836624et_val @t348))
% 0.45/0.89  (define @t355 () (_ (_ tptp.ord_le1643692676de_val @t161) @t350))
% 0.45/0.89  (define @t356 () (_ tptp.finite2056463621de_val @t350))
% 0.45/0.89  (define @t357 () (_ tptp.ord_less_eq_set_val @t148))
% 0.45/0.89  (define @t358 () (_ @t357 @t351))
% 0.45/0.89  (define @t359 () (_ tptp.finite_finite_val @t351))
% 0.45/0.89  (define @t360 () (@list @t351 @t148))
% 0.45/0.89  (define @t361 () (@list @t166 @t348))
% 0.45/0.89  (define @t362 () (@list @t161 @t350))
% 0.45/0.89  (define @t363 () (@list @t148 @t351))
% 0.45/0.89  (define @t364 () (@var "Ys" tptp.list_node))
% 0.45/0.89  (define @t365 () (@var "Y3" tptp.node))
% 0.45/0.89  (define @t366 () (not (_ (_ tptp.member_node @t365) (_ tptp.set_node2 @t364))))
% 0.45/0.89  (define @t367 () (@var "X2" tptp.node))
% 0.45/0.89  (define @t368 () (_ tptp.member_node @t367))
% 0.45/0.89  (define @t369 () (_ @t368 @t116))
% 0.45/0.89  (define @t370 () (_ @t266 @t118))
% 0.45/0.89  (define @t371 () (@var "Ys" tptp.list_val))
% 0.45/0.89  (define @t372 () (@var "Y3" tptp.val))
% 0.45/0.89  (define @t373 () (_ (_ tptp.member_val @t372) (_ tptp.set_val2 @t371)))
% 0.45/0.89  (define @t374 () (not @t373))
% 0.45/0.89  (define @t375 () (_ (_ tptp.member313544709de_val (_ (_ tptp.produc1470527136de_val @t367) @t372)) (_ tptp.set_Pr1085970585de_val (_ (_ tptp.zip_node_val @t115) @t371))))
% 0.45/0.89  (define @t376 () (@list @t367 @t372 @t115 @t371))
% 0.45/0.89  (define @t377 () (_ tptp.member_set_val @t288))
% 0.45/0.89  (define @t378 () (_ @t377 @t114))
% 0.45/0.89  (define @t379 () (@var "Ys" tptp.list_set_val))
% 0.45/0.89  (define @t380 () (_ (_ tptp.member_set_val @t287) (_ tptp.set_set_val2 @t379)))
% 0.45/0.89  (define @t381 () (not @t380))
% 0.45/0.89  (define @t382 () (@var "Ys" tptp.list_P1820443774de_val))
% 0.45/0.89  (define @t383 () (@var "Y3" tptp.produc1432036078de_val))
% 0.45/0.89  (define @t384 () (not (_ (_ tptp.member313544709de_val @t383) (_ tptp.set_Pr1085970585de_val @t382))))
% 0.45/0.89  (define @t385 () (_ (_ tptp.member1711426256et_val (_ (_ tptp.produc1041633943et_val @t288) @t287)) (_ tptp.set_Pr284769596et_val (_ @t306 @t379))))
% 0.45/0.89  (define @t386 () (@list @t288 @t287 @t113 @t379))
% 0.45/0.89  (define @t387 () (@var "Y3" tptp.option_list_val))
% 0.45/0.89  (define @t388 () (@var "P2" (-> tptp.option_list_val tptp.option_list_val Bool)))
% 0.45/0.89  (define @t389 () (_ (_ @t388 @t282) @t387))
% 0.45/0.89  (define @t390 () (@var "B3" tptp.list_val))
% 0.45/0.89  (define @t391 () (@var "A4" tptp.list_val))
% 0.45/0.89  (define @t392 () (= @t387 tptp.none_list_val))
% 0.45/0.89  (define @t393 () (@var "X" tptp.list_val))
% 0.45/0.89  (define @t394 () (@var "P4" (-> tptp.option_list_val Bool)))
% 0.45/0.89  (define @t395 () (_ @t394 (_ tptp.some_list_val @t393)))
% 0.45/0.89  (define @t396 () (@list @t393))
% 0.45/0.89  (define @t397 () (_ @t394 tptp.none_list_val))
% 0.45/0.89  (define @t398 () (@list @t394))
% 0.45/0.89  (define @t399 () (@var "X4" tptp.option_list_val))
% 0.45/0.89  (define @t400 () (@var "P3" (-> tptp.option_list_val Bool)))
% 0.45/0.89  (define @t401 () (_ @t400 @t399))
% 0.45/0.89  (define @t402 () (@list @t399))
% 0.45/0.89  (define @t403 () (@list @t400))
% 0.45/0.89  (define @t404 () (@var "Option" tptp.option_list_val))
% 0.45/0.89  (define @t405 () (@var "P2" (-> tptp.option_list_val Bool)))
% 0.45/0.89  (define @t406 () (@var "X3" tptp.list_val))
% 0.45/0.89  (define @t407 () (@var "X23" tptp.list_val))
% 0.45/0.89  (define @t408 () (@var "Scc3" tptp.set_val))
% 0.45/0.89  (define @t409 () (@var "Leaf" tptp.set_val))
% 0.45/0.89  (define @t410 () (not (= @t206 tptp.bot_bot_set_val)))
% 0.45/0.89  (define @t411 () (@var "C" tptp.set_val))
% 0.45/0.89  (define @t412 () (_ tptp.ord_less_eq_set_val @t351))
% 0.45/0.89  (define @t413 () (_ @t412 @t411))
% 0.45/0.89  (define @t414 () (_ @t357 @t411))
% 0.45/0.89  (define @t415 () (_ tptp.sup_sup_set_val @t148))
% 0.45/0.89  (define @t416 () (_ @t415 @t351))
% 0.45/0.89  (define @t417 () (_ tptp.ord_less_eq_set_val @t416))
% 0.45/0.89  (define @t418 () (_ @t417 @t411))
% 0.45/0.89  (define @t419 () (@list @t148 @t351 @t411))
% 0.45/0.89  (define @t420 () (@var "Z" tptp.set_val))
% 0.45/0.89  (define @t421 () (_ tptp.ord_less_eq_set_val @t287))
% 0.45/0.89  (define @t422 () (@list @t288 @t287 @t420))
% 0.45/0.89  (define @t423 () (@var "C2" tptp.set_val))
% 0.45/0.89  (define @t424 () (_ tptp.ord_less_eq_set_val @t423))
% 0.45/0.89  (define @t425 () (_ @t424 @t139))
% 0.45/0.89  (define @t426 () (_ tptp.ord_less_eq_set_val @t305))
% 0.45/0.89  (define @t427 () (_ @t426 @t139))
% 0.45/0.89  (define @t428 () (_ tptp.sup_sup_set_val @t305))
% 0.45/0.89  (define @t429 () (_ @t428 @t423))
% 0.45/0.89  (define @t430 () (_ (_ tptp.ord_less_eq_set_val @t429) @t139))
% 0.45/0.89  (define @t431 () (@list @t305 @t423 @t139))
% 0.45/0.89  (define @t432 () (= @t148 @t351))
% 0.45/0.89  (define @t433 () (_ @t412 @t148))
% 0.45/0.89  (define @t434 () (_ (_ tptp.ord_less_eq_set_node @t151) @t349))
% 0.45/0.89  (define @t435 () (_ (_ tptp.ord_le1742111550et_val @t156) @t347))
% 0.45/0.89  (define @t436 () (@var "X3" tptp.produc1432036078de_val))
% 0.45/0.89  (define @t437 () (_ tptp.member313544709de_val @t436))
% 0.45/0.89  (define @t438 () (@var "X3" tptp.produc1324971431et_val))
% 0.45/0.89  (define @t439 () (_ tptp.member1711426256et_val @t438))
% 0.45/0.89  (define @t440 () (_ tptp.sup_sup_set_val @t139))
% 0.45/0.89  (define @t441 () (_ @t440 @t305))
% 0.45/0.89  (define @t442 () (_ tptp.sup_sup_set_val @t441))
% 0.45/0.89  (define @t443 () (@list @t139 @t305))
% 0.45/0.89  (define @t444 () (@list @t288))
% 0.45/0.89  (define @t445 () (@list @t139))
% 0.45/0.89  (define @t446 () (@var "C2" tptp.node))
% 0.45/0.89  (define @t447 () (_ tptp.member_node @t446))
% 0.45/0.89  (define @t448 () (_ @t447 @t349))
% 0.45/0.89  (define @t449 () (_ @t447 @t151))
% 0.45/0.89  (define @t450 () (_ @t447 (_ (_ tptp.sup_sup_set_node @t151) @t349)))
% 0.45/0.89  (define @t451 () (@list @t446 @t151 @t349))
% 0.45/0.89  (define @t452 () (_ tptp.member_set_val @t423))
% 0.45/0.89  (define @t453 () (_ @t452 @t347))
% 0.45/0.89  (define @t454 () (_ @t452 @t156))
% 0.45/0.89  (define @t455 () (_ @t452 (_ (_ tptp.sup_sup_set_set_val @t156) @t347)))
% 0.45/0.89  (define @t456 () (@list @t423 @t156 @t347))
% 0.45/0.89  (define @t457 () (@var "C2" tptp.produc1432036078de_val))
% 0.45/0.89  (define @t458 () (_ tptp.member313544709de_val @t457))
% 0.45/0.89  (define @t459 () (_ @t458 @t350))
% 0.45/0.89  (define @t460 () (_ @t458 @t161))
% 0.45/0.89  (define @t461 () (_ @t458 (_ (_ tptp.sup_su2138939728de_val @t161) @t350)))
% 0.45/0.89  (define @t462 () (@list @t457 @t161 @t350))
% 0.45/0.89  (define @t463 () (@var "C2" tptp.produc1324971431et_val))
% 0.45/0.89  (define @t464 () (_ tptp.member1711426256et_val @t463))
% 0.45/0.89  (define @t465 () (_ @t464 @t348))
% 0.45/0.89  (define @t466 () (_ @t464 @t166))
% 0.45/0.89  (define @t467 () (_ @t464 (_ (_ tptp.sup_su2005730907et_val @t166) @t348)))
% 0.45/0.89  (define @t468 () (@list @t463 @t166 @t348))
% 0.45/0.89  (define @t469 () (@var "C2" tptp.val))
% 0.45/0.89  (define @t470 () (_ tptp.member_val @t469))
% 0.45/0.89  (define @t471 () (_ @t470 @t351))
% 0.45/0.89  (define @t472 () (_ @t470 @t148))
% 0.45/0.89  (define @t473 () (_ @t470 @t416))
% 0.45/0.89  (define @t474 () (@list @t469 @t148 @t351))
% 0.45/0.89  (define @t475 () (@list @t446 @t349 @t151))
% 0.45/0.89  (define @t476 () (@list @t423 @t347 @t156))
% 0.45/0.89  (define @t477 () (@list @t457 @t350 @t161))
% 0.45/0.89  (define @t478 () (@list @t463 @t348 @t166))
% 0.45/0.89  (define @t479 () (@list @t469 @t351 @t148))
% 0.45/0.89  (define @t480 () (= @t148 tptp.bot_bot_set_val))
% 0.45/0.89  (define @t481 () (_ tptp.sup_sup_set_val tptp.bot_bot_set_val))
% 0.45/0.89  (define @t482 () (and (= @t288 tptp.bot_bot_set_val) (= @t287 tptp.bot_bot_set_val)))
% 0.45/0.89  (define @t483 () (and (= @t139 tptp.bot_bot_set_val) (= @t305 tptp.bot_bot_set_val)))
% 0.45/0.89  (define @t484 () (not @t480))
% 0.45/0.89  (define @t485 () (not (= @t156 tptp.bot_bot_set_set_val)))
% 0.45/0.89  (define @t486 () (@var "Q2" (-> tptp.val Bool)))
% 0.45/0.89  (define @t487 () (_ @t81 @t35))
% 0.45/0.89  (define @t488 () (_ (_ tptp.ord_less_eq_set_val @t135) (_ tptp.collect_val @t486)))
% 0.45/0.89  (define @t489 () (@list @t81 @t486))
% 0.45/0.89  (define @t490 () (@var "A5" tptp.set_val))
% 0.45/0.89  (define @t491 () (@var "B4" tptp.set_val))
% 0.45/0.89  (define @t492 () (@list @t490 @t491))
% 0.45/0.89  (define @t493 () (@var "Z2" tptp.set_val))
% 0.45/0.89  (define @t494 () (@var "Y4" tptp.set_val))
% 0.45/0.89  (define @t495 () (@var "B4" tptp.set_node))
% 0.45/0.89  (define @t496 () (@var "A5" tptp.set_node))
% 0.45/0.89  (define @t497 () (@list @t496 @t495))
% 0.45/0.89  (define @t498 () (@var "B4" tptp.set_set_val))
% 0.45/0.89  (define @t499 () (@var "A5" tptp.set_set_val))
% 0.45/0.89  (define @t500 () (@list @t499 @t498))
% 0.45/0.89  (define @t501 () (@var "B4" tptp.set_Pr699757092de_val))
% 0.45/0.89  (define @t502 () (@var "A5" tptp.set_Pr699757092de_val))
% 0.45/0.89  (define @t503 () (@list @t502 @t501))
% 0.45/0.89  (define @t504 () (@var "B4" tptp.set_Pr1311924359et_val))
% 0.45/0.89  (define @t505 () (@var "A5" tptp.set_Pr1311924359et_val))
% 0.45/0.89  (define @t506 () (@list @t505 @t504))
% 0.45/0.89  (define @t507 () (_ @t368 @t349))
% 0.45/0.89  (define @t508 () (_ @t377 @t347))
% 0.45/0.89  (define @t509 () (@var "X2" tptp.produc1432036078de_val))
% 0.45/0.89  (define @t510 () (_ tptp.member313544709de_val @t509))
% 0.45/0.89  (define @t511 () (_ @t510 @t350))
% 0.45/0.89  (define @t512 () (@var "X2" tptp.produc1324971431et_val))
% 0.45/0.89  (define @t513 () (_ tptp.member1711426256et_val @t512))
% 0.45/0.89  (define @t514 () (_ @t513 @t348))
% 0.45/0.89  (define @t515 () (_ @t266 @t351))
% 0.45/0.89  (define @t516 () (_ tptp.sup_sup_set_val @t287))
% 0.45/0.89  (define @t517 () (_ @t516 @t420))
% 0.45/0.89  (define @t518 () (_ @t289 @t517))
% 0.45/0.89  (define @t519 () (_ @t440 @t429))
% 0.45/0.89  (define @t520 () (@list @t305 @t139 @t423))
% 0.45/0.89  (define @t521 () (@var "Y2" tptp.set_val))
% 0.45/0.89  (define @t522 () (@list @t157 @t521))
% 0.45/0.89  (define @t523 () (@var "A3" tptp.set_val))
% 0.45/0.89  (define @t524 () (@var "B5" tptp.set_val))
% 0.45/0.89  (define @t525 () (@list @t523 @t524))
% 0.45/0.89  (define @t526 () (@var "K" tptp.set_val))
% 0.45/0.89  (define @t527 () (_ tptp.sup_sup_set_val @t526))
% 0.45/0.89  (define @t528 () (_ @t527 @t441))
% 0.45/0.89  (define @t529 () (_ tptp.sup_sup_set_val @t351))
% 0.45/0.89  (define @t530 () (_ @t415 (_ @t529 @t411)))
% 0.45/0.89  (define @t531 () (_ @t36 @t416))
% 0.45/0.89  (define @t532 () (@list @t148 @t351 @t81))
% 0.45/0.89  (define @t533 () (_ @t424 @t441))
% 0.45/0.89  (define @t534 () (_ (_ tptp.sup_sup_set_val @t523) @t524))
% 0.45/0.89  (define @t535 () (@list @t524 @t523))
% 0.45/0.89  (define @t536 () (@list @t305 @t139))
% 0.45/0.89  (define @t537 () (_ @t421 @t288))
% 0.45/0.89  (define @t538 () (@list @t287 @t288))
% 0.45/0.89  (define @t539 () (@var "F2" (-> tptp.set_val tptp.set_val tptp.set_val)))
% 0.45/0.89  (define @t540 () (@var "Z3" tptp.set_val))
% 0.45/0.89  (define @t541 () (@var "Y5" tptp.set_val))
% 0.45/0.89  (define @t542 () (_ tptp.ord_less_eq_set_val @t541))
% 0.45/0.89  (define @t543 () (_ (_ @t539 @t332) @t541))
% 0.45/0.89  (define @t544 () (@list @t332 @t541))
% 0.45/0.89  (define @t545 () (= @t139 @t441))
% 0.45/0.89  (define @t546 () (@var "D" tptp.set_val))
% 0.45/0.89  (define @t547 () (_ (_ tptp.sup_sup_set_val @t423) @t546))
% 0.45/0.89  (define @t548 () (_ tptp.ord_less_eq_set_val @t441))
% 0.45/0.89  (define @t549 () (_ @t297 @t441))
% 0.45/0.89  (define @t550 () (_ @t548 @t288))
% 0.45/0.89  (define @t551 () (_ @t426 @t288))
% 0.45/0.89  (define @t552 () (_ @t346 @t288))
% 0.45/0.89  (define @t553 () (@var "B6" tptp.set_val))
% 0.45/0.89  (define @t554 () (@var "A6" tptp.set_val))
% 0.45/0.89  (define @t555 () (@var "D2" tptp.set_val))
% 0.45/0.89  (define @t556 () (@var "Phi3" tptp.val))
% 0.45/0.89  (define @t557 () (@var "Y2" tptp.val))
% 0.45/0.89  (define @t558 () (@var "F2" (-> tptp.produc1432036078de_val tptp.option_list_val)))
% 0.45/0.89  (define @t559 () (@var "F2" (-> tptp.val tptp.option_list_val)))
% 0.45/0.89  (define @t560 () (_ tptp.member_val tptp.phi_s))
% 0.45/0.89  (define @t561 () (_ @t560 @t4))
% 0.45/0.89  (define @t562 () (not @t561))
% 0.45/0.89  (define @t563 () (@var "InEdges" (-> tptp.g tptp.node tptp.list_P561207620_edgeD)))
% 0.45/0.89  (define @t564 () (_ @t36 (_ (_ (_ (_ (_ (_ tptp.sSA_CF1517915011eD_val @t200) @t563) @t199) @t201) @t198) @t197)))
% 0.45/0.89  (define @t565 () (lambda (@list @t200 @t563 @t199 @t201 @t198 @t197) (exists @t38 (and @t564 (_ (_ (_ (_ (_ (_ (_ tptp.sSA_CF1899243830eD_val @t200) @t563) @t199) @t201) @t198) @t197) @t35)))))
% 0.45/0.89  (define @t566 () (lambda (@list @t200 @t563 @t199 @t201 @t198 @t197 @t70) (exists @t38 (and @t564 (_ (_ (_ (_ (_ (_ tptp.sSA_CF1909049442de_val @t200) @t199) @t198) @t197) @t70) @t35)))))
% 0.45/0.89  (define @t567 () (_ (_ tptp.sSA_CF370335846de_val @t198) @t197))
% 0.45/0.89  (define @t568 () (lambda (@list @t200 @t199 @t201 @t198 @t197) (forall @t154 (=> (_ @t153 @t205) (forall @t176 (=> (_ @t75 (_ @t567 @t152)) (_ @t202 @t74)))))))
% 0.45/0.89  (define @t569 () (lambda (@list @t199 @t198 @t197 @t73) (_ (_ tptp.sup_sup_set_val (_ (_ @t199 @t197) @t73)) (_ @t567 @t73))))
% 0.45/0.89  (define @t570 () (lambda (@list @t200 @t563 @t201 @t198 @t197 @t73) (_ (_ tptp.sup_sup_set_val @t204) (_ (_ (_ (_ (_ tptp.sSA_CF848637139eD_val @t200) @t563) @t198) @t197) @t73))))
% 0.45/0.89  (define @t571 () (_ (_ (_ (_ (_ tptp.sSA_CF551432799de_val @t200) @t199) @t198) @t197) @t70))
% 0.45/0.89  (define @t572 () (_ (_ tptp.produc1470527136de_val @t571) @t70))
% 0.45/0.89  (define @t573 () (_ @t198 @t197))
% 0.45/0.89  (define @t574 () (_ @t573 @t572))
% 0.45/0.89  (define @t575 () (lambda (@list @t200 @t199 @t198 @t197 @t70) @t574))
% 0.45/0.89  (define @t576 () (_ tptp.member_val @t69))
% 0.45/0.89  (define @t577 () (_ @t576 @t261))
% 0.45/0.89  (define @t578 () (= (_ (_ (_ (_ (_ tptp.sSA_CF262257161de_val @t200) @t199) @t198) @t197) @t70) @t262))
% 0.45/0.89  (define @t579 () (and @t578 @t577))
% 0.45/0.89  (define @t580 () (exists @t263 @t579))
% 0.45/0.89  (define @t581 () (@list @t200 @t199 @t198 @t197 @t70 @t69))
% 0.45/0.89  (define @t582 () (lambda @t581 @t580))
% 0.45/0.89  (define @t583 () (@var "T2" tptp.node))
% 0.45/0.89  (define @t584 () (_ tptp.member_node @t583))
% 0.45/0.89  (define @t585 () (lambda @t497 (forall (@list @t583) (=> (_ @t584 @t496) (_ @t584 @t495)))))
% 0.45/0.89  (define @t586 () (@var "T2" tptp.set_val))
% 0.45/0.89  (define @t587 () (_ tptp.member_set_val @t586))
% 0.45/0.89  (define @t588 () (lambda @t500 (forall (@list @t586) (=> (_ @t587 @t499) (_ @t587 @t498)))))
% 0.45/0.89  (define @t589 () (@var "T2" tptp.produc1432036078de_val))
% 0.45/0.89  (define @t590 () (_ tptp.member313544709de_val @t589))
% 0.45/0.89  (define @t591 () (lambda @t503 (forall (@list @t589) (=> (_ @t590 @t502) (_ @t590 @t501)))))
% 0.45/0.89  (define @t592 () (@var "T2" tptp.produc1324971431et_val))
% 0.45/0.89  (define @t593 () (_ tptp.member1711426256et_val @t592))
% 0.45/0.89  (define @t594 () (lambda @t506 (forall (@list @t592) (=> (_ @t593 @t505) (_ @t593 @t504)))))
% 0.45/0.89  (define @t595 () (@var "T2" tptp.val))
% 0.45/0.89  (define @t596 () (_ tptp.member_val @t595))
% 0.45/0.89  (define @t597 () (lambda @t492 (forall (@list @t595) (=> (_ @t596 @t490) (_ @t596 @t491)))))
% 0.45/0.89  (define @t598 () (@var "BOUND_VARIABLE_10826" tptp.list_val))
% 0.45/0.89  (define @t599 () (not (tptp.member_val @t8 (tptp.set_val2 @t598))))
% 0.45/0.89  (define @t600 () (tptp.some_list_val @t598))
% 0.45/0.89  (define @t601 () (tptp.phis @t6 (tptp.produc1470527136de_val (tptp.sSA_CF551432799de_val tptp.alpha_n tptp.defs tptp.phis @t6 @t11) @t11)))
% 0.45/0.89  (define @t602 () (not (= @t600 @t601)))
% 0.45/0.89  (define @t603 () (tptp.sSA_CF1517915011eD_val tptp.alpha_n tptp.inEdges tptp.defs tptp.uses tptp.phis @t6))
% 0.45/0.89  (define @t604 () (tptp.member_val @t8 @t603))
% 0.45/0.89  (define @t605 () (or @t604 @t602 @t599))
% 0.45/0.89  (define @t606 () (or @t602 @t599))
% 0.45/0.89  (define @t607 () (or @t606 @t604))
% 0.45/0.89  (define @t608 () (@list @t6 @t11 @t8 @t598))
% 0.45/0.89  (define @t609 () (forall @t608 @t607))
% 0.45/0.89  (define @t610 () (@list @t598))
% 0.45/0.89  (define @t611 () (forall @t610 @t607))
% 0.45/0.89  (define @t612 () (forall @t610 @t606))
% 0.45/0.89  (define @t613 () (or @t612 @t604))
% 0.45/0.89  (define @t614 () (tptp.set_val2 @t260))
% 0.45/0.89  (define @t615 () (tptp.some_list_val @t260))
% 0.45/0.89  (define @t616 () (not (= @t615 @t601)))
% 0.45/0.89  (define @t617 () (forall @t263 (or @t616 (not (tptp.member_val @t8 @t614)))))
% 0.45/0.89  (define @t618 () (or @t617 @t10))
% 0.45/0.89  (define @t619 () (not @t617))
% 0.45/0.89  (define @t620 () (tptp.member_val @t69 @t614))
% 0.45/0.89  (define @t621 () (not @t620))
% 0.45/0.89  (define @t622 () (@list @t69))
% 0.45/0.89  (define @t623 () (lambda @t622 (not (forall @t263 (or @t616 @t621)))))
% 0.45/0.89  (define @t624 () (lambda @t72 (not (forall @t263 (or (not (= @t615 (tptp.phis @t6 (tptp.produc1470527136de_val (tptp.sSA_CF551432799de_val tptp.alpha_n tptp.defs tptp.phis @t6 @t70) @t70)))) @t621)))))
% 0.45/0.89  (define @t625 () (lambda (@list @t197 @t70 @t69) (not (forall @t263 (or (not (= @t615 (tptp.phis @t197 (tptp.produc1470527136de_val (tptp.sSA_CF551432799de_val tptp.alpha_n tptp.defs tptp.phis @t197 @t70) @t70)))) @t621)))))
% 0.45/0.89  (define @t626 () (lambda (@list @t198 @t197 @t70 @t69) (not (forall @t263 (or (not (= @t615 (_ @t198 @t197 (tptp.produc1470527136de_val (tptp.sSA_CF551432799de_val tptp.alpha_n tptp.defs @t198 @t197 @t70) @t70)))) @t621)))))
% 0.45/0.89  (define @t627 () (lambda (@list @t199 @t198 @t197 @t70 @t69) (not (forall @t263 (or (not (= @t615 (_ @t198 @t197 (tptp.produc1470527136de_val (tptp.sSA_CF551432799de_val tptp.alpha_n @t199 @t198 @t197 @t70) @t70)))) @t621)))))
% 0.45/0.89  (define @t628 () (tptp.sSA_CF551432799de_val @t200 @t199 @t198 @t197 @t70))
% 0.45/0.89  (define @t629 () (tptp.produc1470527136de_val @t628 @t70))
% 0.45/0.89  (define @t630 () (_ @t198 @t197 @t629))
% 0.45/0.89  (define @t631 () (_ (lambda @t581 (not (forall @t263 (or (not (= @t615 @t630)) @t621)))) tptp.alpha_n))
% 0.45/0.89  (define @t632 () (=> (_ (_ (_ (_ (_ @t631 tptp.defs) tptp.phis) @t6) @t11) @t8) @t10))
% 0.45/0.89  (define @t633 () (not @t577))
% 0.45/0.89  (define @t634 () (= @t262 @t574))
% 0.45/0.89  (define @t635 () (not @t634))
% 0.45/0.89  (define @t636 () (or @t635 @t633))
% 0.45/0.89  (define @t637 () (and @t634 @t577))
% 0.45/0.89  (define @t638 () (forall @t263 (not @t637)))
% 0.45/0.89  (define @t639 () (not @t638))
% 0.45/0.89  (define @t640 () (lambda (@list @t70) @t574))
% 0.45/0.89  (define @t641 () (lambda (@list @t197 @t70) @t574))
% 0.45/0.89  (define @t642 () (lambda (@list @t198 @t197 @t70) @t574))
% 0.45/0.89  (define @t643 () (lambda (@list @t199 @t198 @t197 @t70) @t574))
% 0.45/0.89  (define @t644 () (_ @t575 @t200))
% 0.45/0.89  (define @t645 () (= (_ (_ (_ (_ @t644 @t199) @t198) @t197) @t70) @t262))
% 0.45/0.89  (define @t646 () (and @t645 @t577))
% 0.45/0.89  (define @t647 () (tptp.phis tptp.g2 (tptp.produc1470527136de_val (tptp.sSA_CF551432799de_val tptp.alpha_n tptp.defs tptp.phis tptp.g2 tptp.phi2) tptp.phi2)))
% 0.45/0.89  (define @t648 () (not (= @t615 @t647)))
% 0.45/0.89  (define @t649 () (forall @t263 (or @t648 (not (tptp.member_val tptp.phi_s @t614)))))
% 0.45/0.89  (define @t650 () (not @t649))
% 0.45/0.89  (define @t651 () (lambda @t622 (not (forall @t263 (or @t648 @t621)))))
% 0.45/0.89  (define @t652 () (lambda @t72 (not (forall @t263 (or (not (= @t615 (tptp.phis tptp.g2 (tptp.produc1470527136de_val (tptp.sSA_CF551432799de_val tptp.alpha_n tptp.defs tptp.phis tptp.g2 @t70) @t70)))) @t621)))))
% 0.45/0.89  (define @t653 () (@quantifiers_skolemize @t649 0))
% 0.45/0.89  (define @t654 () (tptp.member_val tptp.phi_s (tptp.set_val2 @t653)))
% 0.45/0.89  (define @t655 () (not @t654))
% 0.45/0.89  (define @t656 () (tptp.some_list_val @t653))
% 0.45/0.89  (define @t657 () (= @t647 @t656))
% 0.45/0.89  (define @t658 () (not @t657))
% 0.45/0.89  (define @t659 () (or @t658 @t655))
% 0.45/0.89  (define @t660 () (not @t659))
% 0.45/0.89  (define @t661 () (not (= @t656 @t647)))
% 0.45/0.89  (define @t662 () (or @t661 @t655))
% 0.45/0.89  (define @t663 () (not @t662))
% 0.45/0.89  (define @t664 () (@list true))
% 0.45/0.89  (define @t665 () (@list @t659))
% 0.45/0.89  (define @t666 () (tptp.sSA_CF1517915011eD_val tptp.alpha_n tptp.inEdges tptp.defs tptp.uses tptp.phis tptp.g2))
% 0.45/0.89  (define @t667 () (tptp.member_val tptp.phi_s @t666))
% 0.45/0.89  (define @t668 () (or @t667 @t658 @t655))
% 0.45/0.89  (define @t669 () (not @t668))
% 0.45/0.89  (define @t670 () (forall @t608 (or @t604 (not (= @t601 @t600)) @t599)))
% 0.45/0.89  (assume @p1 (not (= tptp.phi_s tptp.s)))
% 0.45/0.89  (assume @p2 (not (= tptp.phi tptp.phi_s)))
% 0.45/0.89  (assume @p3 (_ (_ @t2 tptp.phi2) tptp.phi_s))
% 0.45/0.89  (assume @p4 (_ (_ tptp.member_val tptp.s) @t4))
% 0.45/0.89  (assume @p5 (_ (_ tptp.member_val tptp.phi) @t4))
% 0.45/0.89  (assume @p6 (not (forall (@list @t5) (not (_ (_ @t2 @t5) tptp.phi_s)))))
% 0.45/0.89  (assume @p7 @t17)
% 0.45/0.89  (assume @p8 (forall @t25 (=> @t24 @t20)))
% 0.45/0.89  (assume @p9 (forall @t29 (=> @t28 @t26)))
% 0.45/0.89  (assume @p10 (forall @t29 (=> @t31 @t26)))
% 0.45/0.89  (assume @p11 (forall @t32 (_ tptp.finite_finite_val @t7)))
% 0.45/0.89  (assume @p12 (forall @t25 (=> @t24 @t34)))
% 0.45/0.89  (assume @p13 (forall @t32 (= (_ (_ (_ (_ (_ (_ tptp.sSA_CF1660885746eD_val tptp.alpha_n) tptp.inEdges) tptp.defs) tptp.uses) tptp.phis) @t6) (exists @t38 (and @t37 (_ @t27 @t35))))))
% 0.45/0.89  (assume @p14 (forall @t29 (= @t28 (exists @t38 (and @t37 (_ (_ (_ (_ (_ (_ tptp.sSA_CF1909049442de_val tptp.alpha_n) tptp.defs) tptp.phis) @t6) @t11) @t35))))))
% 0.45/0.89  (assume @p15 (= (_ @t40 tptp.phi_s) (_ @t40 tptp.s)))
% 0.45/0.89  (assume @p16 (forall @t47 (=> @t46 (=> @t43 (not @t24)))))
% 0.45/0.89  (assume @p17 (forall @t16 (=> @t31 (=> @t14 (_ @t30 @t8)))))
% 0.45/0.89  (assume @p18 (forall @t58 (=> @t57 (=> @t55 (=> @t54 (not @t53))))))
% 0.45/0.89  (assume @p19 (forall (@list @t6 @t51 @t48 @t59) (=> @t57 (=> (_ @t56 @t59) (=> (not (= @t48 @t59)) (=> @t54 (not (= @t50 (_ @t49 @t59)))))))))
% 0.45/0.89  (assume @p20 (forall @t25 (=> @t24 @t46)))
% 0.45/0.89  (assume @p21 (forall @t60 (_ tptp.finite_finite_val @t42)))
% 0.45/0.89  (assume @p22 (forall @t66 (=> @t20 (not (forall @t65 (=> @t64 (not (_ @t19 @t62))))))))
% 0.45/0.89  (assume @p23 (forall @t32 (_ tptp.finite_finite_val @t18)))
% 0.45/0.89  (assume @p24 (forall (@list @t21 @t6 @t67) (=> @t46 (=> (_ @t68 @t23) (_ @t30 @t67)))))
% 0.45/0.89  (assume @p25 (forall @t79 (= @t78 (or (exists @t77 (and (= @t71 @t74) (_ @t76 @t44) (_ @t75 (_ @t22 @t73)))) (exists @t72 (and (= @t71 @t69) (_ @t30 @t70) (_ (_ @t12 @t70) @t69)))))))
% 0.45/0.89  (assume @p26 (forall (@list @t6 @t80 @t81) (=> (_ @t30 @t80) (=> (forall @t93 (=> @t64 (=> (_ @t92 @t62) @t91))) (=> (forall @t89 (=> @t88 (=> @t87 (=> (_ @t86 @t83) @t84)))) @t82)))))
% 0.45/0.89  (assume @p27 (forall @t79 (=> @t78 (=> (forall @t65 (=> @t64 (not (_ @t95 @t62)))) (not (forall @t94 (=> @t88 (not (_ @t86 @t71)))))))))
% 0.45/0.89  (assume @p28 (forall @t96 (=> @t46 (_ tptp.finite_finite_val @t33))))
% 0.45/0.89  (assume @p29 (forall @t66 (=> @t26 (_ (_ tptp.member_node @t97) @t44))))
% 0.45/0.89  (assume @p30 (forall @t60 (_ tptp.finite_finite_val @t23)))
% 0.45/0.89  (assume @p31 (forall @t25 (=> @t34 @t98)))
% 0.45/0.89  (assume @p32 (forall @t25 (=> @t101 @t34)))
% 0.45/0.89  (assume @p33 (forall @t96 (=> @t46 (_ tptp.finite_finite_val @t100))))
% 0.45/0.89  (assume @p34 (forall @t66 (=> @t26 (_ @t19 (_ @t102 @t97)))))
% 0.45/0.89  (assume @p35 (forall @t66 (=> @t26 (exists @t108 (and @t107 @t105 (forall (@list @t104) (=> (and (_ (_ tptp.member_node @t104) @t44) (_ @t19 (_ @t102 @t104))) (= @t104 @t103))))))))
% 0.45/0.89  (assume @p36 (forall @t66 (=> @t26 (exists @t108 (and @t107 @t105)))))
% 0.45/0.89  (assume @p37 (forall (@list @t109) (_ tptp.finite781217938de_val (_ tptp.set_Pr434939430de_val @t109))))
% 0.45/0.89  (assume @p38 (forall (@list @t110) (_ tptp.finite1581417648et_val (_ tptp.set_Pr2104310812et_val @t110))))
% 0.45/0.89  (assume @p39 (forall (@list @t111) (_ tptp.finite423892681l_node (_ tptp.set_Pr1600883293l_node @t111))))
% 0.45/0.89  (assume @p40 (forall (@list @t112) (_ tptp.finite759259600al_val (_ tptp.set_Pr102746428al_val @t112))))
% 0.45/0.89  (assume @p41 (forall (@list @t113) (_ tptp.finite1265617511et_val @t114)))
% 0.45/0.89  (assume @p42 (forall (@list @t115) (_ tptp.finite_finite_node @t116)))
% 0.45/0.89  (assume @p43 (forall (@list @t117) (_ tptp.finite_finite_val @t118)))
% 0.45/0.89  (assume @p44 (forall (@list @t119) (_ tptp.finite79836624et_val @t120)))
% 0.45/0.89  (assume @p45 (forall (@list @t121) (_ tptp.finite2056463621de_val @t122)))
% 0.45/0.89  (assume @p46 (forall @t60 (_ tptp.finite_finite_val @t124)))
% 0.45/0.89  (assume @p47 (forall @t96 (=> @t46 (_ tptp.finite_finite_val @t125))))
% 0.45/0.89  (assume @p48 (= @t127 (_ @t126 tptp.s)))
% 0.45/0.89  (assume @p49 (forall @t25 (=> @t43 @t128)))
% 0.45/0.89  (assume @p50 (forall @t25 (=> (_ @t19 @t124) @t128)))
% 0.45/0.89  (assume @p51 (forall (@list @t21 @t6 @t129 @t11) (=> @t46 (=> (_ @t130 @t44) (=> @t128 (=> (_ @t19 (_ @t102 @t129)) (= @t21 @t129)))))))
% 0.45/0.89  (assume @p52 (forall (@list @t131 @t132) (= (_ (_ tptp.member828457417l_node @t131) (_ tptp.collec885255687l_node @t132)) (_ @t132 @t131))))
% 0.45/0.89  (assume @p53 (forall (@list @t133 @t134) (= (_ (_ tptp.member1680438992al_val @t133) (_ tptp.collec52550418al_val @t134)) (_ @t134 @t133))))
% 0.45/0.89  (assume @p54 (forall (@list @t71 @t81) (= (_ @t95 @t135) (_ @t81 @t71))))
% 0.45/0.89  (assume @p55 (forall (@list @t136 @t137) (= (_ @t138 (_ tptp.collect_node @t137)) (_ @t137 @t136))))
% 0.45/0.89  (assume @p56 (forall (@list @t139 @t140) (= (_ @t141 (_ tptp.collect_set_val @t140)) (_ @t140 @t139))))
% 0.45/0.89  (assume @p57 (forall (@list @t142 @t143) (= (_ @t144 (_ tptp.collec370342979de_val @t143)) (_ @t143 @t142))))
% 0.45/0.89  (assume @p58 (forall (@list @t145 @t146) (= (_ @t147 (_ tptp.collec1117167378et_val @t146)) (_ @t146 @t145))))
% 0.45/0.89  (assume @p59 (forall @t150 (= (_ tptp.collect_val (lambda @t38 @t149)) @t148)))
% 0.45/0.89  (assume @p60 (forall @t155 (= (_ tptp.collect_node (lambda @t154 (_ @t153 @t151))) @t151)))
% 0.45/0.89  (assume @p61 (forall @t160 (= (_ tptp.collect_set_val (lambda @t159 (_ @t158 @t156))) @t156)))
% 0.45/0.89  (assume @p62 (forall @t165 (= (_ tptp.collec370342979de_val (lambda @t164 (_ @t163 @t161))) @t161)))
% 0.45/0.89  (assume @p63 (forall @t170 (= (_ tptp.collec1117167378et_val (lambda @t169 (_ @t168 @t166))) @t166)))
% 0.45/0.89  (assume @p64 (forall @t58 (=> @t57 (= @t173 @t172))))
% 0.45/0.89  (assume @p65 (= @t127 (_ @t126 tptp.phi_s)))
% 0.45/0.89  (assume @p66 (forall (@list @t21 @t6 @t11 @t8) (=> @t46 (=> @t128 (=> (_ @t9 @t125) (=> (not (= @t11 @t8)) (not @t174)))))))
% 0.45/0.89  (assume @p67 (forall (@list @t51 @t6 @t48) (=> @t54 (=> (_ @t175 @t7) (=> @t55 (=> @t53 (not (= @t172 @t173))))))))
% 0.45/0.89  (assume @p68 (forall @t47 (=> @t46 (=> @t128 (= @t97 @t21)))))
% 0.45/0.89  (assume @p69 (forall @t25 (=> @t128 @t98)))
% 0.45/0.89  (assume @p70 (forall @t32 (= (_ (_ (_ (_ (_ tptp.sSA_CF2074824714de_val tptp.alpha_n) tptp.defs) tptp.uses) tptp.phis) @t6) (forall @t154 (=> (_ @t153 @t44) (forall @t176 (=> (_ @t75 (_ @t123 @t152)) (_ @t30 @t74))))))))
% 0.45/0.89  (assume @p71 (= tptp.sSA_CF848637139eD_val tptp.sSA_CF848637139eD_val))
% 0.45/0.89  (assume @p72 (= tptp.sSA_CF370335846de_val tptp.sSA_CF370335846de_val))
% 0.45/0.89  (assume @p73 (= tptp.sSA_CF139593942de_val tptp.sSA_CF139593942de_val))
% 0.45/0.89  (assume @p74 (= tptp.sSA_CF551432799de_val tptp.sSA_CF551432799de_val))
% 0.45/0.89  (assume @p75 (= tptp.sSA_CF1517915011eD_val tptp.sSA_CF1517915011eD_val))
% 0.45/0.89  (assume @p76 (= tptp.sSA_CF1252180629de_val tptp.sSA_CF1252180629de_val))
% 0.45/0.89  (assume @p77 (= tptp.sSA_CF178745443eD_val tptp.sSA_CF178745443eD_val))
% 0.45/0.89  (assume @p78 (= tptp.sSA_CF794421325de_val tptp.sSA_CF794421325de_val))
% 0.45/0.89  (assume @p79 (= tptp.sSA_CF1899243830eD_val tptp.sSA_CF1899243830eD_val))
% 0.45/0.89  (assume @p80 (= tptp.sSA_CF655860150de_val tptp.sSA_CF655860150de_val))
% 0.45/0.89  (assume @p81 (= tptp.sSA_CF1909049442de_val tptp.sSA_CF1909049442de_val))
% 0.45/0.89  (assume @p82 (= tptp.sSA_CF1660885746eD_val tptp.sSA_CF1660885746eD_val))
% 0.45/0.89  (assume @p83 (forall @t155 (=> @t178 (exists (@list @t177) (= (_ tptp.set_node2 @t177) @t151)))))
% 0.45/0.89  (assume @p84 (forall @t150 (=> @t180 (exists (@list @t179) (= (_ tptp.set_val2 @t179) @t148)))))
% 0.45/0.89  (assume @p85 (forall @t170 (=> @t182 (exists (@list @t181) (= (_ tptp.set_Pr284769596et_val @t181) @t166)))))
% 0.45/0.89  (assume @p86 (forall @t165 (=> @t184 (exists (@list @t183) (= (_ tptp.set_Pr1085970585de_val @t183) @t161)))))
% 0.45/0.89  (assume @p87 (forall (@list @t21 @t188 @t6 @t67 @t186 @t187 @t185) (=> (_ @t45 @t191) (=> (_ @t68 (_ @t190 @t21)) (_ @t189 @t67)))))
% 0.45/0.89  (assume @p88 (forall (@list @t188 @t187 @t186 @t185 @t6 @t11 @t8) (=> (_ @t189 @t11) (=> (_ (_ @t192 @t11) @t8) (_ @t189 @t8)))))
% 0.45/0.89  (assume @p89 (forall (@list @t188 @t187 @t186 @t185 @t6 @t80 @t81) (=> (_ @t189 @t80) (=> (forall @t93 (=> @t196 (=> (_ @t92 @t195) @t91))) (=> (forall @t89 (=> @t194 (=> @t87 (=> (_ @t193 @t83) @t84)))) @t82)))))
% 0.45/0.89  (assume @p90 (= tptp.sSA_CF794421325de_val (lambda (@list @t200 @t199 @t201 @t198 @t197 @t203) (or (exists @t77 (and (= @t203 @t74) (_ @t76 @t205) (_ @t75 @t204))) (exists @t72 (and (= @t203 @t69) (_ @t202 @t70) (_ (_ (_ (_ (_ (_ tptp.sSA_CF1252180629de_val @t200) @t199) @t198) @t197) @t70) @t69)))))))
% 0.45/0.89  (assume @p91 (forall (@list @t188 @t187 @t186 @t185 @t6 @t71) (=> (_ @t189 @t71) (=> (forall @t65 (=> @t196 (not (_ @t95 @t195)))) (not (forall @t94 (=> @t194 (not (_ @t193 @t71)))))))))
% 0.45/0.89  (assume @p92 (forall @t208 (_ tptp.finite79836624et_val @t207)))
% 0.45/0.89  (assume @p93 (forall @t58 (=> @t57 (=> @t54 (not (forall (@list @t210) (=> (_ @t175 (_ @t99 @t210)) (not (_ (_ tptp.member_node @t210) (_ tptp.set_node2 (_ @t209 @t52)))))))))))
% 0.45/0.89  (assume @p94 (forall @t60 (= @t33 (_ (_ tptp.sup_sup_set_val @t23) @t100))))
% 0.45/0.89  (assume @p95 (forall (@list @t6 @t212 @t211) (=> (_ (_ (_ tptp.transi1991289355lp_val @t12) @t212) @t211) (= (_ @t171 @t212) (_ @t171 @t211)))))
% 0.45/0.89  (assume @p96 (forall @t60 (= @t125 (_ (_ tptp.sup_sup_set_val @t42) @t124))))
% 0.45/0.89  (assume @p97 (forall @t66 (=> @t26 (=> (not (_ @t19 (_ @t41 @t97))) @t216))))
% 0.45/0.89  (assume @p98 (forall @t47 (=> @t46 (=> @t43 @t215))))
% 0.45/0.89  (assume @p99 (forall @t222 (= @t221 (and @t220 @t218))))
% 0.45/0.89  (assume @p100 (forall @t228 (= @t227 (and @t226 @t224))))
% 0.45/0.89  (assume @p101 (forall @t234 (= @t233 (and @t232 @t230))))
% 0.45/0.89  (assume @p102 (forall @t29 (=> @t28 @t216)))
% 0.45/0.89  (assume @p103 (forall (@list @t129 @t6 @t11) (=> (_ @t130 (_ tptp.set_node2 (_ @t209 @t97))) (=> @t216 (=> @t26 (not (forall @t237 (=> @t236 (not (_ @t13 @t83))))))))))
% 0.45/0.89  (assume @p104 (= tptp.sSA_CF262257161de_val tptp.sSA_CF262257161de_val))
% 0.45/0.89  (assume @p105 (forall @t243 (= @t242 (or @t241 @t239))))
% 0.45/0.89  (assume @p106 (forall @t249 (= @t248 (or @t247 @t245))))
% 0.45/0.89  (assume @p107 (forall @t255 (= @t254 (or @t253 @t251))))
% 0.45/0.89  (assume @p108 (forall @t243 (=> @t241 @t242)))
% 0.45/0.89  (assume @p109 (forall @t249 (=> @t247 @t248)))
% 0.45/0.89  (assume @p110 (forall @t255 (=> @t253 @t254)))
% 0.45/0.89  (assume @p111 (forall @t222 (=> @t220 (=> @t218 @t221))))
% 0.45/0.89  (assume @p112 (forall @t228 (=> @t226 (=> @t224 @t227))))
% 0.45/0.89  (assume @p113 (forall @t234 (=> @t232 (=> @t230 @t233))))
% 0.45/0.89  (assume @p114 (= tptp.irredu893086079de_val tptp.irredu893086079de_val))
% 0.45/0.89  (assume @p115 (= tptp.sSA_CF2074824714de_val tptp.sSA_CF2074824714de_val))
% 0.45/0.89  (assume @p116 (forall (@list @t6 @t11 @t256) (=> @t258 (_ @t19 (_ @t123 @t97)))))
% 0.45/0.89  (assume @p117 (forall @t208 (_ tptp.transi1953622797et_val @t207)))
% 0.45/0.89  (assume @p118 (forall @t29 (= @t214 (_ @t259 (_ (_ tptp.produc1470527136de_val @t97) @t11)))))
% 0.45/0.89  (assume @p119 (forall @t16 (= @t14 (exists @t263 (and (= @t214 @t262) (_ @t9 @t261))))))
% 0.45/0.89  (assume @p120 (forall @t32 (_ tptp.finite_finite_val @t264)))
% 0.45/0.89  (assume @p121 (forall (@list @t6 @t206 @t265 @t80) (=> @t269 (=> @t268 (=> (_ @t266 @t265) (not (= (_ @t213 @t80) tptp.none_list_val)))))))
% 0.45/0.89  (assume @p122 (forall @t276 (=> @t275 (=> @t273 (= @t256 @t270)))))
% 0.45/0.89  (assume @p123 (forall @t276 (=> @t275 (=> @t273 (= @t21 @t271)))))
% 0.45/0.89  (assume @p124 (forall @t277 (=> @t275 @t46)))
% 0.45/0.89  (assume @p125 (forall (@list @t6 @t21 @t11 @t256 @t8) (=> @t275 (=> (_ @t9 @t278) @t174))))
% 0.45/0.89  (assume @p126 (forall @t277 (=> @t275 @t258)))
% 0.45/0.89  (assume @p127 (forall (@list @t129 @t6 @t21 @t11 @t256) (=> @t279 (=> @t275 (=> @t46 (not (forall @t237 (=> @t236 (not (_ @t235 @t278))))))))))
% 0.45/0.89  (assume @p128 (= tptp.irredu681226810de_val tptp.irredu681226810de_val))
% 0.45/0.89  (assume @p129 (= tptp.irredu224829488eD_val tptp.irredu224829488eD_val))
% 0.45/0.89  (assume @p130 (forall (@list @t271 @t6 @t8 @t256 @t21 @t11) (=> (_ (_ tptp.member_node @t271) @t44) (=> (= (_ @t259 (_ @t272 @t8)) @t257) (=> (_ @t280 (_ tptp.set_Pr1085970585de_val (_ (_ tptp.zip_node_val (_ @t209 @t271)) @t256))) @t101)))))
% 0.45/0.89  (assume @p131 (forall (@list @t265 @t6 @t206) (=> @t268 (_ (_ tptp.ord_less_eq_set_val @t265) @t206))))
% 0.45/0.89  (assume @p132 (forall @t286 (= (not @t285) (exists @t284 @t283))))
% 0.45/0.89  (assume @p133 (forall @t286 (= (forall @t284 (not @t283)) @t285)))
% 0.45/0.89  (assume @p134 (forall @t293 (= (_ (_ tptp.sup_su1487070040et_val @t292) @t291) (_ tptp.some_set_val @t290))))
% 0.45/0.89  (assume @p135 (forall (@list @t295 @t294) (= (= @t296 (_ tptp.some_list_val @t294)) (= @t295 @t294))))
% 0.45/0.89  (assume @p136 (forall @t293 (= (_ (_ tptp.ord_le596993316et_val @t292) @t291) @t298)))
% 0.45/0.89  (assume @p137 (forall (@list @t145 @t299 @t119) (= (_ (_ tptp.member1254968080et_val (_ (_ tptp.produc1377626967et_val @t145) @t299)) (_ tptp.set_Pr1006393724et_val (_ (_ tptp.zip_Pr21865079et_val @t119) @t119))) (and (_ @t147 @t120) (= @t145 @t299)))))
% 0.45/0.89  (assume @p138 (forall (@list @t136 @t300 @t115) (= (_ (_ tptp.member2110109140e_node (_ (_ tptp.produc457016035e_node @t136) @t300)) (_ tptp.set_Pr450990656e_node (_ @t301 @t115))) (and (_ @t138 @t116) (= @t136 @t300)))))
% 0.45/0.89  (assume @p139 (forall (@list @t71 @t302 @t117) (= (_ (_ tptp.member1680438992al_val (_ (_ tptp.product_Pair_val_val @t71) @t302)) (_ tptp.set_Pr102746428al_val (_ @t303 @t117))) (and (_ @t95 @t118) (= @t71 @t302)))))
% 0.45/0.89  (assume @p140 (forall (@list @t142 @t304 @t121) (= (_ (_ tptp.member698732390de_val (_ (_ tptp.produc453318901de_val @t142) @t304)) (_ tptp.set_Pr482027474de_val (_ (_ tptp.zip_Pr1472086037de_val @t121) @t121))) (and (_ @t144 @t122) (= @t142 @t304)))))
% 0.45/0.89  (assume @p141 (forall (@list @t139 @t305 @t113) (= (_ (_ tptp.member1711426256et_val (_ (_ tptp.produc1041633943et_val @t139) @t305)) (_ tptp.set_Pr284769596et_val (_ @t306 @t113))) (and (_ @t141 @t114) (= @t139 @t305)))))
% 0.45/0.89  (assume @p142 (forall @t208 (=> @t269 (exists (@list @t307) (and (_ (_ tptp.ord_less_eq_set_val @t307) @t206) (_ (_ (_ (_ (_ (_ (_ (_ tptp.irredu1955035135eD_val tptp.alpha_n) tptp.inEdges) tptp.defs) tptp.uses) tptp.phis) @t6) @t206) @t307))))))
% 0.45/0.89  (assume @p143 (forall @t25 (=> @t101 (not (forall (@list @t309) (=> (_ (_ tptp.member_node @t309) (_ tptp.set_node2 (_ @t310 @t21))) (forall (@list @t83 @t308) (=> (_ @t280 (_ tptp.set_Pr1085970585de_val (_ (_ tptp.zip_node_val (_ @t209 @t309)) @t308))) (not (= (_ @t259 (_ (_ tptp.produc1470527136de_val @t309) @t83)) (_ tptp.some_list_val @t308)))))))))))
% 0.45/0.89  (assume @p144 (forall @t318 (=> @t178 (=> @t317 (exists @t108 (and @t316 (_ @t315 @t136) (forall @t314 (=> @t313 (=> (_ (_ tptp.ord_less_eq_node @t311) @t103) @t312)))))))))
% 0.45/0.89  (assume @p145 (forall @t330 (=> @t180 (=> @t329 (exists @t328 (and @t327 (_ @t325 @t71) @t324))))))
% 0.45/0.89  (assume @p146 (forall @t343 (=> @t342 (=> @t341 (exists @t340 (and @t339 (_ @t337 @t139) @t336))))))
% 0.45/0.89  (assume @p147 (forall @t318 (=> @t178 (=> @t317 (exists @t108 (and @t316 (_ (_ tptp.ord_less_eq_node @t136) @t103) (forall @t314 (=> @t313 (=> (_ @t315 @t311) @t312)))))))))
% 0.45/0.89  (assume @p148 (forall @t330 (=> @t180 (=> @t329 (exists @t328 (and @t327 (_ (_ tptp.ord_less_eq_val @t71) @t320) @t344))))))
% 0.45/0.89  (assume @p149 (forall @t343 (=> @t342 (=> @t341 (exists @t340 (and @t339 (_ @t346 @t332) @t345))))))
% 0.45/0.89  (assume @p150 (forall (@list @t113 @t347) (= (_ (_ tptp.ord_le1742111550et_val @t114) @t347) (forall @t159 (=> (_ @t158 @t114) (_ @t158 @t347))))))
% 0.45/0.89  (assume @p151 (forall (@list @t119 @t348) (= (_ (_ tptp.ord_le299366439et_val @t120) @t348) (forall @t169 (=> (_ @t168 @t120) (_ @t168 @t348))))))
% 0.45/0.89  (assume @p152 (forall (@list @t115 @t349) (= (_ (_ tptp.ord_less_eq_set_node @t116) @t349) (forall @t154 (=> (_ @t153 @t116) (_ @t153 @t349))))))
% 0.45/0.89  (assume @p153 (forall (@list @t121 @t350) (= (_ (_ tptp.ord_le1643692676de_val @t122) @t350) (forall @t164 (=> (_ @t163 @t122) (_ @t163 @t350))))))
% 0.45/0.89  (assume @p154 (forall (@list @t117 @t351) (= (_ (_ tptp.ord_less_eq_set_val @t118) @t351) (forall @t38 (=> (_ @t36 @t118) @t352)))))
% 0.45/0.89  (assume @p155 (forall (@list @t348 @t166) (=> @t354 (=> @t353 @t182))))
% 0.45/0.89  (assume @p156 (forall (@list @t350 @t161) (=> @t356 (=> @t355 @t184))))
% 0.45/0.89  (assume @p157 (forall @t360 (=> @t359 (=> @t358 @t180))))
% 0.45/0.89  (assume @p158 (forall @t243 (=> (_ (_ tptp.ord_le299366439et_val @t240) @t238) (=> @t241 @t239))))
% 0.45/0.89  (assume @p159 (forall @t249 (=> (_ (_ tptp.ord_le1643692676de_val @t246) @t244) (=> @t247 @t245))))
% 0.45/0.89  (assume @p160 (forall @t255 (=> (_ (_ tptp.ord_less_eq_set_val @t252) @t250) (=> @t253 @t251))))
% 0.45/0.89  (assume @p161 (forall @t361 (=> @t353 (=> @t354 @t182))))
% 0.45/0.89  (assume @p162 (forall @t362 (=> @t355 (=> @t356 @t184))))
% 0.45/0.89  (assume @p163 (forall @t363 (=> @t358 (=> @t359 @t180))))
% 0.45/0.89  (assume @p164 (forall (@list @t367 @t365 @t115 @t364) (=> (_ (_ tptp.member2110109140e_node (_ (_ tptp.produc457016035e_node @t367) @t365)) (_ tptp.set_Pr450990656e_node (_ @t301 @t364))) (not (=> @t369 @t366)))))
% 0.45/0.89  (assume @p165 (forall (@list @t80 @t365 @t117 @t364) (=> (_ (_ tptp.member828457417l_node (_ (_ tptp.produc1074923692l_node @t80) @t365)) (_ tptp.set_Pr1600883293l_node (_ (_ tptp.zip_val_node @t117) @t364))) (not (=> @t370 @t366)))))
% 0.45/0.89  (assume @p166 (forall (@list @t80 @t372 @t117 @t371) (=> (_ (_ tptp.member1680438992al_val (_ (_ tptp.product_Pair_val_val @t80) @t372)) (_ tptp.set_Pr102746428al_val (_ @t303 @t371))) (not (=> @t370 @t374)))))
% 0.45/0.89  (assume @p167 (forall @t376 (=> @t375 (not (=> @t369 @t374)))))
% 0.45/0.89  (assume @p168 (forall (@list @t288 @t365 @t113 @t364) (=> (_ (_ tptp.member76372137l_node (_ (_ tptp.produc2052093836l_node @t288) @t365)) (_ tptp.set_Pr1904955709l_node (_ (_ tptp.zip_set_val_node @t113) @t364))) (not (=> @t378 @t366)))))
% 0.45/0.89  (assume @p169 (forall (@list @t288 @t372 @t113 @t371) (=> (_ (_ tptp.member1110026224al_val (_ (_ tptp.produc1337903031al_val @t288) @t372)) (_ tptp.set_Pr1027623516al_val (_ (_ tptp.zip_set_val_val @t113) @t371))) (not (=> @t378 @t374)))))
% 0.45/0.89  (assume @p170 (forall (@list @t367 @t287 @t115 @t379) (=> (_ (_ tptp.member125181669et_val (_ (_ tptp.produc2042994048et_val @t367) @t287)) (_ tptp.set_Pr1953765241et_val (_ (_ tptp.zip_node_set_val @t115) @t379))) (not (=> @t369 @t381)))))
% 0.45/0.89  (assume @p171 (forall (@list @t80 @t287 @t117 @t379) (=> (_ (_ tptp.member39229872et_val (_ (_ tptp.produc1446164855et_val @t80) @t287)) (_ tptp.set_Pr2104310812et_val (_ (_ tptp.zip_val_set_val @t117) @t379))) (not (=> @t370 @t381)))))
% 0.45/0.89  (assume @p172 (forall (@list @t367 @t383 @t115 @t382) (=> (_ (_ tptp.member562853661de_val (_ (_ tptp.produc1162531244de_val @t367) @t383)) (_ tptp.set_Pr1157337481de_val (_ (_ tptp.zip_no263301324de_val @t115) @t382))) (not (=> @t369 @t384)))))
% 0.45/0.89  (assume @p173 (forall (@list @t80 @t383 @t117 @t382) (=> (_ (_ tptp.member1894062994de_val (_ (_ tptp.produc1571934709de_val @t80) @t383)) (_ tptp.set_Pr434939430de_val (_ (_ tptp.zip_va679686869de_val @t117) @t382))) (not (=> @t370 @t384)))))
% 0.45/0.89  (assume @p174 (forall @t376 (=> @t375 @t369)))
% 0.45/0.89  (assume @p175 (forall @t386 (=> @t385 @t378)))
% 0.45/0.89  (assume @p176 (forall @t376 (=> @t375 @t373)))
% 0.45/0.89  (assume @p177 (forall @t386 (=> @t385 @t380)))
% 0.45/0.89  (assume @p178 (forall (@list @t282 @t388 @t387) (=> (=> @t285 @t389) (=> (=> @t392 @t389) (=> (forall (@list @t391 @t390) (=> (= @t282 (_ tptp.some_list_val @t391)) (=> (= @t387 (_ tptp.some_list_val @t390)) @t389))) @t389)))))
% 0.45/0.89  (assume @p179 (= (lambda @t403 (forall @t402 @t401)) (lambda @t398 (and @t397 (forall @t396 @t395)))))
% 0.45/0.89  (assume @p180 (= (lambda @t403 (exists @t402 @t401)) (lambda @t398 (or @t397 (exists @t396 @t395)))))
% 0.45/0.89  (assume @p181 (forall (@list @t405 @t404) (=> (_ @t405 tptp.none_list_val) (=> (forall (@list @t406) (_ @t405 (_ tptp.some_list_val @t406))) (_ @t405 @t404)))))
% 0.45/0.89  (assume @p182 (forall (@list @t387) (=> (not @t392) (not (forall (@list @t407) (not (= @t387 (_ tptp.some_list_val @t407))))))))
% 0.45/0.89  (assume @p183 (forall (@list @t404 @t295) (=> (= @t404 @t296) (not (= @t404 tptp.none_list_val)))))
% 0.45/0.89  (assume @p184 (forall (@list @t295) (not (= tptp.none_list_val @t296))))
% 0.45/0.89  (assume @p185 (forall (@list @t206 @t6) (=> @t410 (exists (@list @t409) (and (_ (_ tptp.member_set_val @t409) @t267) (forall (@list @t408) (not (_ (_ tptp.member1711426256et_val (_ (_ tptp.produc1041633943et_val @t409) @t408)) @t207))))))))
% 0.45/0.89  (assume @p186 (forall @t419 (= @t418 (and @t414 @t413))))
% 0.45/0.89  (assume @p187 (forall @t422 (= (_ (_ tptp.ord_less_eq_set_val @t290) @t420) (and (_ @t297 @t420) (_ @t421 @t420)))))
% 0.45/0.90  (assume @p188 (forall @t431 (= @t430 (and @t427 @t425))))
% 0.45/0.90  (assume @p189 (forall @t363 (=> @t358 (=> @t433 @t432))))
% 0.45/0.90  (assume @p190 (forall (@list @t151 @t349) (=> (forall @t108 (=> @t316 (_ @t106 @t349))) @t434)))
% 0.45/0.90  (assume @p191 (forall (@list @t156 @t347) (=> (forall @t340 (=> @t339 (_ @t338 @t347))) @t435)))
% 0.45/0.90  (assume @p192 (forall @t362 (=> (forall (@list @t436) (=> (_ @t437 @t161) (_ @t437 @t350))) @t355)))
% 0.45/0.90  (assume @p193 (forall @t361 (=> (forall (@list @t438) (=> (_ @t439 @t166) (_ @t439 @t348))) @t353)))
% 0.45/0.90  (assume @p194 (forall @t363 (=> (forall @t328 (=> @t327 (_ @t326 @t351))) @t358)))
% 0.45/0.90  (assume @p195 (forall @t443 (= (_ @t442 @t305) @t441)))
% 0.45/0.90  (assume @p196 (forall @t293 (= (_ @t289 @t290) @t290)))
% 0.45/0.90  (assume @p197 (forall @t443 (= (_ @t440 @t441) @t441)))
% 0.45/0.90  (assume @p198 (forall @t444 (= (_ @t289 @t288) @t288)))
% 0.45/0.90  (assume @p199 (forall @t445 (= (_ @t440 @t139) @t139)))
% 0.45/0.90  (assume @p200 (forall @t451 (= @t450 (or @t449 @t448))))
% 0.45/0.90  (assume @p201 (forall @t456 (= @t455 (or @t454 @t453))))
% 0.45/0.90  (assume @p202 (forall @t462 (= @t461 (or @t460 @t459))))
% 0.45/0.90  (assume @p203 (forall @t468 (= @t467 (or @t466 @t465))))
% 0.45/0.90  (assume @p204 (forall @t474 (= @t473 (or @t472 @t471))))
% 0.45/0.90  (assume @p205 (forall @t475 (=> (=> (not @t448) @t449) @t450)))
% 0.45/0.90  (assume @p206 (forall @t476 (=> (=> (not @t453) @t454) @t455)))
% 0.45/0.90  (assume @p207 (forall @t477 (=> (=> (not @t459) @t460) @t461)))
% 0.45/0.90  (assume @p208 (forall @t478 (=> (=> (not @t465) @t466) @t467)))
% 0.45/0.90  (assume @p209 (forall @t479 (=> (=> (not @t471) @t472) @t473)))
% 0.45/0.90  (assume @p210 (forall @t150 (= (_ @t357 tptp.bot_bot_set_val) @t480)))
% 0.45/0.90  (assume @p211 (forall @t150 (_ (_ tptp.ord_less_eq_set_val tptp.bot_bot_set_val) @t148)))
% 0.45/0.90  (assume @p212 (forall @t444 (= (_ @t481 @t288) @t288)))
% 0.45/0.90  (assume @p213 (forall @t444 (= (_ @t289 tptp.bot_bot_set_val) @t288)))
% 0.45/0.90  (assume @p214 (forall @t293 (= (= tptp.bot_bot_set_val @t290) @t482)))
% 0.45/0.90  (assume @p215 (forall @t293 (= (= @t290 tptp.bot_bot_set_val) @t482)))
% 0.45/0.90  (assume @p216 (forall @t443 (= (= @t441 tptp.bot_bot_set_val) @t483)))
% 0.45/0.90  (assume @p217 (forall @t445 (= (_ @t481 @t139) @t139)))
% 0.45/0.90  (assume @p218 (forall @t443 (= (= tptp.bot_bot_set_val @t441) @t483)))
% 0.45/0.90  (assume @p219 (forall @t445 (= (_ @t440 tptp.bot_bot_set_val) @t139)))
% 0.45/0.90  (assume @p220 (forall @t363 (= (= @t416 tptp.bot_bot_set_val) (and @t480 (= @t351 tptp.bot_bot_set_val)))))
% 0.45/0.90  (assume @p221 (forall (@list @t21 @t6 @t129) (=> @t46 (= (_ @t45 (_ tptp.set_node2 (_ @t310 @t129))) @t279))))
% 0.45/0.90  (assume @p222 (forall (@list @t351) (= (_ @t481 @t351) @t351)))
% 0.45/0.90  (assume @p223 (forall @t150 (= (_ @t415 tptp.bot_bot_set_val) @t148)))
% 0.45/0.90  (assume @p224 (forall (@list @t240) (=> @t241 (not (= @t240 tptp.bot_bo2078591731et_val)))))
% 0.45/0.90  (assume @p225 (forall (@list @t246) (=> @t247 (not (= @t246 tptp.bot_bo404898488de_val)))))
% 0.45/0.90  (assume @p226 (forall (@list @t252) (=> @t253 (not (= @t252 tptp.bot_bot_set_val)))))
% 0.45/0.90  (assume @p227 (_ tptp.finite79836624et_val tptp.bot_bo2078591731et_val))
% 0.45/0.90  (assume @p228 (_ tptp.finite2056463621de_val tptp.bot_bo404898488de_val))
% 0.45/0.90  (assume @p229 (_ tptp.finite_finite_val tptp.bot_bot_set_val))
% 0.45/0.90  (assume @p230 (= tptp.irredu1955035135eD_val tptp.irredu1955035135eD_val))
% 0.45/0.90  (assume @p231 (forall @t150 (=> @t180 (=> @t484 (exists @t328 (and @t327 @t344))))))
% 0.45/0.90  (assume @p232 (forall @t160 (=> @t342 (=> @t485 (exists @t340 (and @t339 @t345))))))
% 0.45/0.90  (assume @p233 (forall @t150 (=> @t180 (=> @t484 (exists @t328 (and @t327 @t324))))))
% 0.45/0.90  (assume @p234 (forall @t160 (=> @t342 (=> @t485 (exists @t340 (and @t339 @t336))))))
% 0.45/0.90  (assume @p235 (forall @t489 (= @t488 (forall @t38 (=> @t487 (_ @t486 @t35))))))
% 0.45/0.90  (assume @p236 (= (lambda (@list @t494 @t493) (= @t494 @t493)) (lambda @t492 (and (_ (_ tptp.ord_less_eq_set_val @t490) @t491) (_ (_ tptp.ord_less_eq_set_val @t491) @t490)))))
% 0.45/0.90  (assume @p237 (forall @t419 (=> @t358 (=> @t413 @t414))))
% 0.45/0.90  (assume @p238 (forall @t489 (=> (forall @t328 (=> (_ @t81 @t320) (_ @t486 @t320))) @t488)))
% 0.45/0.90  (assume @p239 (forall @t150 (_ @t357 @t148)))
% 0.45/0.90  (assume @p240 (forall @t363 (=> @t432 @t433)))
% 0.45/0.90  (assume @p241 (forall @t363 (=> @t432 @t358)))
% 0.45/0.90  (assume @p242 (= tptp.ord_less_eq_set_node (lambda @t497 (forall @t154 (=> (_ @t153 @t496) (_ @t153 @t495))))))
% 0.45/0.90  (assume @p243 (= tptp.ord_le1742111550et_val (lambda @t500 (forall @t159 (=> (_ @t158 @t499) (_ @t158 @t498))))))
% 0.45/0.90  (assume @p244 (= tptp.ord_le1643692676de_val (lambda @t503 (forall @t164 (=> (_ @t163 @t502) (_ @t163 @t501))))))
% 0.45/0.90  (assume @p245 (= tptp.ord_le299366439et_val (lambda @t506 (forall @t169 (=> (_ @t168 @t505) (_ @t168 @t504))))))
% 0.45/0.90  (assume @p246 (= tptp.ord_less_eq_set_val (lambda @t492 (forall @t38 (=> (_ @t36 @t490) (_ @t36 @t491))))))
% 0.45/0.90  (assume @p247 (forall @t363 (=> @t432 (not (=> @t358 (not @t433))))))
% 0.45/0.90  (assume @p248 (forall (@list @t151 @t349 @t446) (=> @t434 (=> @t449 @t448))))
% 0.45/0.90  (assume @p249 (forall (@list @t156 @t347 @t423) (=> @t435 (=> @t454 @t453))))
% 0.45/0.90  (assume @p250 (forall (@list @t161 @t350 @t457) (=> @t355 (=> @t460 @t459))))
% 0.45/0.90  (assume @p251 (forall (@list @t166 @t348 @t463) (=> @t353 (=> @t466 @t465))))
% 0.45/0.90  (assume @p252 (forall (@list @t148 @t351 @t469) (=> @t358 (=> @t472 @t471))))
% 0.45/0.90  (assume @p253 (forall (@list @t151 @t349 @t367) (=> @t434 (=> (_ @t368 @t151) @t507))))
% 0.45/0.90  (assume @p254 (forall (@list @t156 @t347 @t288) (=> @t435 (=> (_ @t377 @t156) @t508))))
% 0.45/0.90  (assume @p255 (forall (@list @t161 @t350 @t509) (=> @t355 (=> (_ @t510 @t161) @t511))))
% 0.45/0.90  (assume @p256 (forall (@list @t166 @t348 @t512) (=> @t353 (=> (_ @t513 @t166) @t514))))
% 0.45/0.90  (assume @p257 (forall (@list @t148 @t351 @t80) (=> @t358 (=> (_ @t266 @t148) @t515))))
% 0.45/0.90  (assume @p258 (forall @t422 (= @t518 (_ @t516 (_ @t289 @t420)))))
% 0.45/0.90  (assume @p259 (forall @t520 (= (_ @t428 (_ @t440 @t423)) @t519)))
% 0.45/0.90  (assume @p260 (= tptp.sup_sup_set_val (lambda @t522 (_ (_ tptp.sup_sup_set_val @t521) @t157))))
% 0.45/0.90  (assume @p261 (= tptp.sup_sup_set_val (lambda @t525 (_ (_ tptp.sup_sup_set_val @t524) @t523))))
% 0.45/0.90  (assume @p262 (forall @t422 (= (_ (_ tptp.sup_sup_set_val @t290) @t420) @t518)))
% 0.45/0.90  (assume @p263 (forall (@list @t139 @t305 @t423) (= (_ @t442 @t423) @t519)))
% 0.45/0.90  (assume @p264 (forall (@list @t351 @t526 @t305 @t139) (=> (= @t351 (_ @t527 @t305)) (= (_ @t440 @t351) @t528))))
% 0.45/0.90  (assume @p265 (forall (@list @t148 @t526 @t139 @t305) (=> (= @t148 (_ @t527 @t139)) (= (_ @t415 @t305) @t528))))
% 0.45/0.90  (assume @p266 (forall @t419 (= @t530 (_ @t529 (_ @t415 @t411)))))
% 0.45/0.90  (assume @p267 (forall @t363 (= (_ @t415 @t416) @t416)))
% 0.45/0.90  (assume @p268 (= tptp.sup_sup_set_val (lambda @t492 (_ (_ tptp.sup_sup_set_val @t491) @t490))))
% 0.45/0.90  (assume @p269 (forall @t150 (= (_ @t415 @t148) @t148)))
% 0.45/0.90  (assume @p270 (forall @t419 (= (_ (_ tptp.sup_sup_set_val @t416) @t411) @t530)))
% 0.45/0.90  (assume @p271 (forall @t532 (= (forall @t38 (=> @t531 @t487)) (and (forall @t38 (=> @t149 @t487)) (forall @t38 (=> @t352 @t487))))))
% 0.45/0.90  (assume @p272 (forall @t532 (= (exists @t38 (and @t531 @t487)) (or (exists @t38 (and @t149 @t487)) (exists @t38 (and @t352 @t487))))))
% 0.45/0.90  (assume @p273 (forall @t475 (=> @t448 @t450)))
% 0.45/0.90  (assume @p274 (forall @t476 (=> @t453 @t455)))
% 0.45/0.90  (assume @p275 (forall @t477 (=> @t459 @t461)))
% 0.45/0.90  (assume @p276 (forall @t478 (=> @t465 @t467)))
% 0.45/0.90  (assume @p277 (forall @t479 (=> @t471 @t473)))
% 0.45/0.90  (assume @p278 (forall @t451 (=> @t449 @t450)))
% 0.45/0.90  (assume @p279 (forall @t456 (=> @t454 @t455)))
% 0.45/0.90  (assume @p280 (forall @t462 (=> @t460 @t461)))
% 0.45/0.90  (assume @p281 (forall @t468 (=> @t466 @t467)))
% 0.45/0.90  (assume @p282 (forall @t474 (=> @t472 @t473)))
% 0.45/0.90  (assume @p283 (forall @t451 (=> @t450 (=> (not @t449) @t448))))
% 0.45/0.90  (assume @p284 (forall @t456 (=> @t455 (=> (not @t454) @t453))))
% 0.45/0.90  (assume @p285 (forall @t462 (=> @t461 (=> (not @t460) @t459))))
% 0.45/0.90  (assume @p286 (forall @t468 (=> @t467 (=> (not @t466) @t465))))
% 0.45/0.90  (assume @p287 (forall @t474 (=> @t473 (=> (not @t472) @t471))))
% 0.45/0.90  (assume @p288 (forall (@list @t423 @t305 @t139) (=> (_ @t424 @t305) @t533)))
% 0.45/0.90  (assume @p289 (forall (@list @t423 @t139 @t305) (=> @t425 @t533)))
% 0.45/0.90  (assume @p290 (= tptp.ord_less_eq_set_val (lambda @t525 (= @t534 @t524))))
% 0.45/0.90  (assume @p291 (= tptp.ord_less_eq_set_val (lambda @t535 (= @t534 @t523))))
% 0.45/0.90  (assume @p292 (forall @t536 (_ @t426 @t441)))
% 0.45/0.90  (assume @p293 (forall @t443 (_ @t346 @t441)))
% 0.45/0.90  (assume @p294 (= tptp.ord_less_eq_set_val (lambda @t535 (= @t523 @t534))))
% 0.45/0.90  (assume @p295 (forall @t520 (=> @t427 (=> @t425 @t430))))
% 0.45/0.90  (assume @p296 (forall @t431 (=> @t430 (not (=> @t427 (not @t425))))))
% 0.45/0.90  (assume @p297 (forall @t293 (=> @t298 (= @t290 @t287))))
% 0.45/0.90  (assume @p298 (forall @t538 (=> @t537 (= @t290 @t288))))
% 0.45/0.90  (assume @p299 (forall @t443 (=> (_ @t346 @t305) (= @t441 @t305))))
% 0.45/0.90  (assume @p300 (forall @t536 (=> @t427 (= @t441 @t139))))
% 0.45/0.90  (assume @p301 (forall (@list @t539 @t288 @t287) (=> (forall @t544 (_ @t337 @t543)) (=> (forall @t544 (_ @t542 @t543)) (=> (forall (@list @t332 @t541 @t540) (=> (_ @t542 @t332) (=> (_ (_ tptp.ord_less_eq_set_val @t540) @t332) (_ (_ tptp.ord_less_eq_set_val (_ (_ @t539 @t541) @t540)) @t332)))) (= @t290 (_ (_ @t539 @t288) @t287)))))))
% 0.45/0.90  (assume @p302 (forall @t443 (=> @t545 @t427)))
% 0.45/0.90  (assume @p303 (forall @t536 (=> @t427 @t545)))
% 0.45/0.90  (assume @p304 (= tptp.ord_less_eq_set_val (lambda @t522 (= (_ (_ tptp.sup_sup_set_val @t157) @t521) @t521))))
% 0.45/0.90  (assume @p305 (forall (@list @t287 @t288 @t420) (=> @t537 (=> (_ (_ tptp.ord_less_eq_set_val @t420) @t288) (_ (_ tptp.ord_less_eq_set_val @t517) @t288)))))
% 0.45/0.90  (assume @p306 (forall (@list @t139 @t423 @t305 @t546) (=> (_ @t346 @t423) (=> (_ @t426 @t546) (_ @t548 @t547)))))
% 0.45/0.90  (assume @p307 (forall (@list @t423 @t139 @t546 @t305) (=> @t425 (=> (_ (_ tptp.ord_less_eq_set_val @t546) @t305) (_ (_ tptp.ord_less_eq_set_val @t547) @t441)))))
% 0.45/0.90  (assume @p308 (forall (@list @t288 @t305 @t139) (=> (_ @t297 @t305) @t549)))
% 0.45/0.90  (assume @p309 (forall (@list @t288 @t139 @t305) (=> (_ @t297 @t139) @t549)))
% 0.45/0.90  (assume @p310 (forall @t538 (_ @t421 @t290)))
% 0.45/0.90  (assume @p311 (forall @t293 (_ @t297 @t290)))
% 0.45/0.90  (assume @p312 (forall (@list @t139 @t288 @t305) (=> @t552 (=> @t551 @t550))))
% 0.45/0.90  (assume @p313 (forall (@list @t139 @t305 @t288) (=> @t550 (not (=> @t552 (not @t551))))))
% 0.45/0.90  (assume @p314 (= tptp.ord_less_eq_set_val (lambda @t492 (= (_ (_ tptp.sup_sup_set_val @t490) @t491) @t491))))
% 0.45/0.90  (assume @p315 (forall (@list @t411 @t148 @t351) (=> (_ (_ tptp.ord_less_eq_set_val @t411) @t416) (not (forall (@list @t554) (=> (_ (_ tptp.ord_less_eq_set_val @t554) @t148) (forall (@list @t553) (=> (_ (_ tptp.ord_less_eq_set_val @t553) @t351) (not (= @t411 (_ (_ tptp.sup_sup_set_val @t554) @t553)))))))))))
% 0.45/0.90  (assume @p316 (forall @t360 (=> @t433 (= @t416 @t148))))
% 0.45/0.90  (assume @p317 (forall @t363 (=> @t358 (= @t416 @t351))))
% 0.45/0.90  (assume @p318 (forall @t360 (_ @t412 @t416)))
% 0.45/0.90  (assume @p319 (forall @t363 (_ @t357 @t416)))
% 0.45/0.90  (assume @p320 (forall (@list @t148 @t411 @t351) (=> @t414 (=> @t413 @t418))))
% 0.45/0.90  (assume @p321 (forall (@list @t148 @t411 @t351 @t555) (=> @t414 (=> (_ @t412 @t555) (_ @t417 (_ (_ tptp.sup_sup_set_val @t411) @t555))))))
% 0.45/0.90  (assume @p322 (forall @t208 (= @t269 (and @t410 (_ (_ tptp.ord_less_eq_set_val @t206) @t264) (exists @t38 (and @t37 (forall (@list @t557) (=> (_ (_ tptp.member_val @t557) @t206) (forall (@list @t556) (=> (_ (_ @t12 @t557) @t556) (_ (_ tptp.member_val @t556) (_ (_ tptp.sup_sup_set_val @t206) (_ (_ tptp.insert_val @t35) tptp.bot_bot_set_val)))))))))))))
% 0.45/0.90  (assume @p323 (forall (@list @t51 @t6 @t256) (=> @t54 (=> (= (_ @t213 @t51) @t257) (not (= @t278 (_ (_ tptp.insert_val @t51) tptp.bot_bot_set_val)))))))
% 0.45/0.90  (assume @p324 (forall (@list @t558) (= (= (_ tptp.dom_Pr729677986st_val @t558) tptp.bot_bo404898488de_val) (= @t558 (lambda @t164 tptp.none_list_val)))))
% 0.45/0.90  (assume @p325 (forall (@list @t559) (= (= (_ tptp.dom_val_list_val @t559) tptp.bot_bot_set_val) (= @t559 (lambda @t38 tptp.none_list_val)))))
% 0.45/0.90  (assume @p326 (forall @t32 (_ tptp.finite2056463621de_val (_ tptp.dom_Pr729677986st_val @t259))))
% 0.45/0.90  (assume @p327 (forall (@list @t367 @t151 @t349) (= (_ (_ tptp.ord_less_eq_set_node (_ (_ tptp.insert_node @t367) @t151)) @t349) (and @t507 @t434))))
% 0.45/0.90  (assume @p328 (forall (@list @t288 @t156 @t347) (= (_ (_ tptp.ord_le1742111550et_val (_ (_ tptp.insert_set_val @t288) @t156)) @t347) (and @t508 @t435))))
% 0.45/0.90  (assume @p329 (forall (@list @t509 @t161 @t350) (= (_ (_ tptp.ord_le1643692676de_val (_ (_ tptp.insert869443870de_val @t509) @t161)) @t350) (and @t511 @t355))))
% 0.45/0.90  (assume @p330 (forall (@list @t512 @t166 @t348) (= (_ (_ tptp.ord_le299366439et_val (_ (_ tptp.insert1846469495et_val @t512) @t166)) @t348) (and @t514 @t353))))
% 0.45/0.90  (assume @p331 (forall (@list @t80 @t148 @t351) (= (_ (_ tptp.ord_less_eq_set_val (_ (_ tptp.insert_val @t80) @t148)) @t351) (and @t515 @t358))))
% 0.45/0.90  (assume @p332 (forall (@list @t71 @t148) (= (_ tptp.finite_finite_val (_ (_ tptp.insert_val @t71) @t148)) @t180)))
% 0.45/0.90  (assume @p333 (forall (@list @t145 @t166) (= (_ tptp.finite79836624et_val (_ (_ tptp.insert1846469495et_val @t145) @t166)) @t182)))
% 0.45/0.90  (assume @p334 (forall (@list @t142 @t161) (= (_ tptp.finite2056463621de_val (_ (_ tptp.insert869443870de_val @t142) @t161)) @t184)))
% 0.45/0.90  (assume @p335 @t562)
% 0.45/0.90  (assume @p336 true)
% 0.45/0.90  (step @p337 (= tptp.sSA_CF1660885746eD_val @t565) :rule refl :args (@t565))
% 0.45/0.90  (step @p338 (= tptp.sSA_CF1899243830eD_val @t566) :rule refl :args (@t566))
% 0.45/0.90  (step @p339 (= tptp.sSA_CF2074824714de_val @t568) :rule refl :args (@t568))
% 0.45/0.90  (step @p340 (= tptp.sSA_CF139593942de_val @t569) :rule refl :args (@t569))
% 0.45/0.90  (step @p341 (= tptp.sSA_CF178745443eD_val @t570) :rule refl :args (@t570))
% 0.45/0.90  (step @p342 (= tptp.sSA_CF262257161de_val @t575) :rule refl :args (@t575))
% 0.45/0.90  (step @p343 (= tptp.sSA_CF1252180629de_val @t582) :rule refl :args (@t582))
% 0.45/0.90  (step @p344 (= tptp.ord_less_eq_set_node @t585) :rule refl :args (@t585))
% 0.45/0.90  (step @p345 (= tptp.ord_le1742111550et_val @t588) :rule refl :args (@t588))
% 0.45/0.90  (step @p346 (= tptp.ord_le1643692676de_val @t591) :rule refl :args (@t591))
% 0.45/0.90  (step @p347 (= tptp.ord_le299366439et_val @t594) :rule refl :args (@t594))
% 0.45/0.90  (step @p348 (= tptp.ord_less_eq_set_val @t597) :rule refl :args (@t597))
% 0.45/0.90  (step @p349 :rule refl :args (@t599))
% 0.45/0.90  (step @p350 :rule eq-symm :args (@t600 @t601))
% 0.45/0.90  (step @p351 :rule cong :premises (@p350) :args (@t602))
% 0.45/0.90  (step @p352 :rule refl :args (@t604))
% 0.45/0.90  (step @p353 :rule nary_cong :premises (@p352 @p351 @p349) :args (@t605))
% 0.45/0.90  (step @p354 :rule aci_norm :args ((= @t607 @t605)))
% 0.45/0.90  (step @p355 :rule trans :premises (@p354 @p353))
% 0.45/0.90  (step @p356 :rule cong :premises (@p355) :args (@t609))
% 0.45/0.90  (step @p357 :rule quant-merge-prenex :args ((= (forall @t16 @t611) @t609)))
% 0.45/0.90  (step @p358 :rule refl :args (@t604))
% 0.45/0.90  (step @p359 :rule alpha_equiv :args (@t612 (@list @t598) (@list @t260)))
% 0.45/0.90  (step @p360 :rule nary_cong :premises (@p359 @p358) :args (@t613))
% 0.45/0.90  (step @p361 :rule quant-miniscope-or :args ((= @t611 @t613)))
% 0.45/0.90  (step @p362 :rule trans :premises (@p361 @p360))
% 0.45/0.90  (step @p363 :rule symm :premises (@p362))
% 0.45/0.90  (step @p364 :rule cong :premises (@p363) :args ((forall @t16 (or @t617 @t604))))
% 0.45/0.90  (step @p365 :rule trans :premises (@p364 @p357))
% 0.45/0.90  (step @p366 :rule trans :premises (@p365 @p356))
% 0.45/0.90  (step @p367 :rule refl :args ((tptp.member_val @t8 @t7)))
% 0.45/0.90  (step @p368 :rule refl :args (@t603))
% 0.45/0.90  (step @p369 :rule refl :args (@t8))
% 0.45/0.90  (step @p370 :rule cong :premises (@p369 @p368) :args (@t604))
% 0.45/0.90  (step @p371 :rule trans :premises (@p370 @p367))
% 0.45/0.90  (step @p372 :rule refl :args (@t9))
% 0.45/0.90  (step @p373 :rule ho_cong :premises (@p372 @p368))
% 0.45/0.90  (step @p374 :rule cong :premises (@p373 @p371) :args ((= (_ @t9 @t603) @t604)))
% 0.45/0.90  (step @p375 :rule symm :premises (@p374))
% 0.45/0.90  (step @p376 :rule refl :args (@t10))
% 0.45/0.90  (step @p377 :rule eq_resolve :premises (@p376 @p375))
% 0.45/0.90  (step @p378 :rule refl :args (@t7))
% 0.45/0.90  (step @p379 :rule cong :premises (@p378 @p368) :args ((= @t7 @t603)))
% 0.45/0.90  (step @p380 :rule symm :premises (@p379))
% 0.45/0.90  (step @p381 :rule eq_resolve :premises (@p378 @p380))
% 0.45/0.90  (step @p382 :rule ho_cong :premises (@p372 @p381))
% 0.45/0.90  (step @p383 :rule trans :premises (@p382 @p377))
% 0.45/0.90  (step @p384 :rule refl :args (@t617))
% 0.45/0.90  (step @p385 :rule nary_cong :premises (@p384 @p383) :args (@t618))
% 0.45/0.90  (step @p386 :rule cong :premises (@p385) :args ((forall @t16 @t618)))
% 0.45/0.90  (step @p387 :rule trans :premises (@p386 @p366))
% 0.45/0.90  (step @p388 :rule bool-double-not-elim :args (@t617))
% 0.45/0.90  (step @p389 :rule nary_cong :premises (@p388 @p376) :args ((or (not @t619) @t10)))
% 0.45/0.90  (step @p390 :rule bool-impl-elim :args (@t619 @t10))
% 0.45/0.90  (step @p391 :rule trans :premises (@p390 @p389))
% 0.45/0.90  (step @p392 :rule cong :premises (@p391) :args ((forall @t16 (=> @t619 @t10))))
% 0.45/0.90  (step @p393 :rule trans :premises (@p392 @p387))
% 0.45/0.90  (step @p394 :rule refl :args (@t10))
% 0.45/0.90  (step @p395 :rule beta-reduce :args ((= (_ @t623 @t8) @t619)))
% 0.45/0.90  (step @p396 :rule refl :args (@t8))
% 0.45/0.90  (step @p397 :rule beta-reduce :args ((= (_ @t624 @t11) @t623)))
% 0.45/0.90  (step @p398 :rule refl :args (@t11))
% 0.45/0.90  (step @p399 :rule beta-reduce :args ((= (_ @t625 @t6) @t624)))
% 0.45/0.90  (step @p400 :rule refl :args (@t6))
% 0.45/0.90  (step @p401 :rule beta-reduce :args ((= (_ @t626 tptp.phis) @t625)))
% 0.45/0.90  (step @p402 :rule refl :args (tptp.phis))
% 0.45/0.90  (step @p403 :rule beta-reduce :args ((= (_ @t627 tptp.defs) @t626)))
% 0.45/0.90  (step @p404 :rule refl :args (tptp.defs))
% 0.45/0.90  (step @p405 :rule beta-reduce :args ((= @t631 @t627)))
% 0.45/0.90  (step @p406 :rule ho_cong :premises (@p405 @p404))
% 0.45/0.90  (step @p407 :rule trans :premises (@p406 @p403))
% 0.45/0.90  (step @p408 :rule ho_cong :premises (@p407 @p402))
% 0.45/0.90  (step @p409 :rule trans :premises (@p408 @p401))
% 0.45/0.90  (step @p410 :rule ho_cong :premises (@p409 @p400))
% 0.45/0.90  (step @p411 :rule trans :premises (@p410 @p399))
% 0.45/0.90  (step @p412 :rule ho_cong :premises (@p411 @p398))
% 0.45/0.90  (step @p413 :rule trans :premises (@p412 @p397))
% 0.45/0.90  (step @p414 :rule ho_cong :premises (@p413 @p396))
% 0.45/0.90  (step @p415 :rule trans :premises (@p414 @p395))
% 0.45/0.90  (step @p416 :rule cong :premises (@p415 @p394) :args (@t632))
% 0.45/0.90  (step @p417 :rule cong :premises (@p416) :args ((forall @t16 @t632)))
% 0.45/0.90  (step @p418 :rule trans :premises (@p417 @p393))
% 0.45/0.90  (step @p419 :rule refl :args (tptp.alpha_n))
% 0.45/0.90  (step @p420 :rule refl :args ((tptp.member_val @t69 @t261)))
% 0.45/0.90  (step @p421 :rule refl :args (@t614))
% 0.45/0.90  (step @p422 :rule refl :args (@t69))
% 0.45/0.90  (step @p423 :rule cong :premises (@p422 @p421) :args (@t620))
% 0.45/0.90  (step @p424 :rule trans :premises (@p423 @p420))
% 0.45/0.90  (step @p425 :rule refl :args (@t576))
% 0.45/0.90  (step @p426 :rule ho_cong :premises (@p425 @p421))
% 0.45/0.90  (step @p427 :rule cong :premises (@p426 @p424) :args ((= (_ @t576 @t614) @t620)))
% 0.45/0.90  (step @p428 :rule symm :premises (@p427))
% 0.45/0.90  (step @p429 :rule refl :args (@t577))
% 0.45/0.90  (step @p430 :rule eq_resolve :premises (@p429 @p428))
% 0.45/0.90  (step @p431 :rule refl :args (@t261))
% 0.45/0.90  (step @p432 :rule cong :premises (@p431 @p421) :args ((= @t261 @t614)))
% 0.45/0.90  (step @p433 :rule symm :premises (@p432))
% 0.45/0.90  (step @p434 :rule eq_resolve :premises (@p431 @p433))
% 0.45/0.90  (step @p435 :rule ho_cong :premises (@p425 @p434))
% 0.45/0.90  (step @p436 :rule trans :premises (@p435 @p430))
% 0.45/0.90  (step @p437 :rule cong :premises (@p436) :args (@t633))
% 0.45/0.90  (step @p438 :rule refl :args ((_ @t198 @t197 @t572)))
% 0.45/0.90  (step @p439 :rule refl :args ((tptp.produc1470527136de_val @t571 @t70)))
% 0.45/0.90  (step @p440 :rule refl :args (@t70))
% 0.45/0.90  (step @p441 :rule refl :args (@t628))
% 0.45/0.90  (step @p442 :rule cong :premises (@p441 @p440) :args (@t629))
% 0.45/0.90  (step @p443 :rule trans :premises (@p442 @p439))
% 0.45/0.90  (step @p444 :rule refl :args (@t197))
% 0.45/0.90  (step @p445 :rule cong :premises (@p444 @p443) :args (@t630))
% 0.45/0.90  (step @p446 :rule trans :premises (@p445 @p438))
% 0.45/0.90  (step @p447 :rule refl :args (@t573))
% 0.45/0.90  (step @p448 :rule ho_cong :premises (@p447 @p443))
% 0.45/0.90  (step @p449 :rule cong :premises (@p448 @p446) :args ((= (_ @t573 @t629) @t630)))
% 0.45/0.90  (step @p450 :rule symm :premises (@p449))
% 0.45/0.90  (step @p451 :rule refl :args (@t574))
% 0.45/0.90  (step @p452 :rule eq_resolve :premises (@p451 @p450))
% 0.45/0.90  (step @p453 :rule refl :args (tptp.produc1470527136de_val))
% 0.45/0.90  (step @p454 :rule ho_cong :premises (@p453 @p441))
% 0.45/0.90  (step @p455 :rule ho_cong :premises (@p454 @p440))
% 0.45/0.90  (step @p456 :rule cong :premises (@p455 @p443) :args ((= (_ (_ tptp.produc1470527136de_val @t628) @t70) @t629)))
% 0.45/0.90  (step @p457 :rule symm :premises (@p456))
% 0.45/0.90  (step @p458 :rule refl :args (@t572))
% 0.45/0.90  (step @p459 :rule eq_resolve :premises (@p458 @p457))
% 0.45/0.90  (step @p460 :rule refl :args (@t571))
% 0.45/0.90  (step @p461 :rule cong :premises (@p460 @p441) :args ((= @t571 @t628)))
% 0.45/0.90  (step @p462 :rule symm :premises (@p461))
% 0.45/0.90  (step @p463 :rule eq_resolve :premises (@p460 @p462))
% 0.45/0.90  (step @p464 :rule ho_cong :premises (@p453 @p463))
% 0.45/0.90  (step @p465 :rule ho_cong :premises (@p464 @p440))
% 0.45/0.90  (step @p466 :rule trans :premises (@p465 @p459))
% 0.45/0.90  (step @p467 :rule ho_cong :premises (@p447 @p466))
% 0.45/0.90  (step @p468 :rule trans :premises (@p467 @p452))
% 0.45/0.90  (step @p469 :rule refl :args (@t615))
% 0.45/0.90  (step @p470 :rule refl :args (@t262))
% 0.45/0.90  (step @p471 :rule cong :premises (@p470 @p469) :args ((= @t262 @t615)))
% 0.45/0.90  (step @p472 :rule symm :premises (@p471))
% 0.45/0.90  (step @p473 :rule eq_resolve :premises (@p470 @p472))
% 0.45/0.90  (step @p474 :rule cong :premises (@p473 @p468) :args (@t634))
% 0.45/0.90  (step @p475 :rule cong :premises (@p474) :args (@t635))
% 0.45/0.90  (step @p476 :rule nary_cong :premises (@p475 @p437) :args (@t636))
% 0.45/0.90  (step @p477 :rule cong :premises (@p476) :args ((forall @t263 @t636)))
% 0.75/0.90  (step @p478 :rule bool-and-de-morgan :args (@t634 @t577 true))
% 0.75/0.90  (step @p479 :rule cong :premises (@p478) :args (@t638))
% 0.75/0.90  (step @p480 :rule trans :premises (@p479 @p477))
% 0.75/0.90  (step @p481 :rule cong :premises (@p480) :args (@t639))
% 0.75/0.90  (step @p482 :rule exists-elim :args ((= (exists @t263 @t637) @t639)))
% 0.75/0.90  (step @p483 :rule trans :premises (@p482 @p481))
% 0.75/0.90  (step @p484 :rule refl :args (@t577))
% 0.75/0.90  (step @p485 :rule eq-symm :args (@t574 @t262))
% 0.75/0.90  (step @p486 :rule refl :args (@t262))
% 0.75/0.90  (step @p487 :rule beta-reduce :args ((= (_ @t640 @t70) @t574)))
% 0.75/0.90  (step @p488 :rule refl :args (@t70))
% 0.75/0.90  (step @p489 :rule beta-reduce :args ((= (_ @t641 @t197) @t640)))
% 0.75/0.90  (step @p490 :rule refl :args (@t197))
% 0.75/0.90  (step @p491 :rule beta-reduce :args ((= (_ @t642 @t198) @t641)))
% 0.75/0.90  (step @p492 :rule refl :args (@t198))
% 0.75/0.90  (step @p493 :rule beta-reduce :args ((= (_ @t643 @t199) @t642)))
% 0.75/0.90  (step @p494 :rule refl :args (@t199))
% 0.75/0.90  (step @p495 :rule beta-reduce :args ((= @t644 @t643)))
% 0.75/0.90  (step @p496 :rule ho_cong :premises (@p495 @p494))
% 0.75/0.90  (step @p497 :rule trans :premises (@p496 @p493))
% 0.75/0.90  (step @p498 :rule ho_cong :premises (@p497 @p492))
% 0.75/0.90  (step @p499 :rule trans :premises (@p498 @p491))
% 0.75/0.90  (step @p500 :rule ho_cong :premises (@p499 @p490))
% 0.75/0.90  (step @p501 :rule trans :premises (@p500 @p489))
% 0.75/0.90  (step @p502 :rule ho_cong :premises (@p501 @p488))
% 0.75/0.90  (step @p503 :rule trans :premises (@p502 @p487))
% 0.75/0.90  (step @p504 :rule cong :premises (@p503 @p486) :args (@t645))
% 0.75/0.90  (step @p505 :rule trans :premises (@p504 @p485))
% 0.75/0.90  (step @p506 :rule nary_cong :premises (@p505 @p484) :args (@t646))
% 0.75/0.90  (step @p507 :rule cong :premises (@p506) :args ((exists @t263 @t646)))
% 0.75/0.90  (step @p508 :rule trans :premises (@p507 @p483))
% 0.75/0.90  (step @p509 :rule refl :args (@t200))
% 0.75/0.90  (step @p510 :rule ho_cong :premises (@p342 @p509))
% 0.75/0.90  (step @p511 :rule ho_cong :premises (@p510 @p494))
% 0.75/0.90  (step @p512 :rule ho_cong :premises (@p511 @p492))
% 0.75/0.90  (step @p513 :rule ho_cong :premises (@p512 @p490))
% 0.75/0.90  (step @p514 :rule ho_cong :premises (@p513 @p488))
% 0.75/0.90  (step @p515 :rule cong :premises (@p514 @p486) :args (@t578))
% 0.75/0.90  (step @p516 :rule nary_cong :premises (@p515 @p484) :args (@t579))
% 0.75/0.90  (step @p517 :rule cong :premises (@p516) :args (@t580))
% 0.75/0.90  (step @p518 :rule trans :premises (@p517 @p508))
% 0.75/0.90  (step @p519 :rule cong :premises (@p518) :args (@t582))
% 0.75/0.90  (step @p520 :rule trans :premises (@p343 @p519))
% 0.75/0.90  (step @p521 :rule ho_cong :premises (@p520 @p419))
% 0.75/0.90  (step @p522 :rule ho_cong :premises (@p521 @p404))
% 0.75/0.90  (step @p523 :rule ho_cong :premises (@p522 @p402))
% 0.75/0.90  (step @p524 :rule ho_cong :premises (@p523 @p400))
% 0.75/0.90  (step @p525 :rule ho_cong :premises (@p524 @p398))
% 0.75/0.90  (step @p526 :rule ho_cong :premises (@p525 @p396))
% 0.75/0.90  (step @p527 :rule cong :premises (@p526 @p394) :args (@t15))
% 0.75/0.90  (step @p528 :rule cong :premises (@p527) :args (@t17))
% 0.75/0.90  (step @p529 :rule trans :premises (@p528 @p418))
% 0.75/0.90  (step @p530 :rule eq_resolve :premises (@p7 @p529))
% 0.75/0.90  (step @p531 :rule beta-reduce :args ((= (_ @t651 tptp.phi_s) @t650)))
% 0.75/0.90  (step @p532 :rule refl :args (tptp.phi_s))
% 0.75/0.90  (step @p533 :rule beta-reduce :args ((= (_ @t652 tptp.phi2) @t651)))
% 0.75/0.90  (step @p534 :rule refl :args (tptp.phi2))
% 0.75/0.90  (step @p535 :rule beta-reduce :args ((= (_ @t625 tptp.g2) @t652)))
% 0.75/0.90  (step @p536 :rule refl :args (tptp.g2))
% 0.75/0.90  (step @p537 :rule ho_cong :premises (@p409 @p536))
% 0.75/0.90  (step @p538 :rule trans :premises (@p537 @p535))
% 0.75/0.90  (step @p539 :rule ho_cong :premises (@p538 @p534))
% 0.75/0.90  (step @p540 :rule trans :premises (@p539 @p533))
% 0.75/0.90  (step @p541 :rule ho_cong :premises (@p540 @p532))
% 0.75/0.90  (step @p542 :rule trans :premises (@p541 @p531))
% 0.75/0.90  (step @p543 :rule ho_cong :premises (@p523 @p536))
% 0.75/0.90  (step @p544 :rule ho_cong :premises (@p543 @p534))
% 0.75/0.90  (step @p545 :rule ho_cong :premises (@p544 @p532))
% 0.75/0.90  (step @p546 :rule trans :premises (@p545 @p542))
% 0.75/0.90  (step @p547 :rule eq_resolve :premises (@p3 @p546))
% 0.75/0.90  (step @p548 :rule refl :args (@t660))
% 0.75/0.90  (step @p549 :rule bool-double-not-elim :args (@t649))
% 0.75/0.90  (step @p550 :rule nary_cong :premises (@p549 @p548) :args ((or (not @t650) @t660)))
% 0.75/0.90  (step @p551 :rule refl :args (@t655))
% 0.75/0.90  (step @p552 :rule eq-symm :args (@t656 @t647))
% 0.75/0.90  (step @p553 :rule cong :premises (@p552) :args (@t661))
% 0.75/0.90  (step @p554 :rule nary_cong :premises (@p553 @p551) :args (@t662))
% 0.75/0.90  (step @p555 :rule cong :premises (@p554) :args (@t663))
% 0.75/0.90  (step @p556 :rule refl :args (@t650))
% 0.75/0.90  (step @p557 :rule cong :premises (@p556 @p555) :args ((=> @t650 @t663)))
% 0.75/0.90  (assume-push @p608 @t650)
% 0.75/0.90  (step @p559 :rule skolemize :premises (@p547))
% 0.75/0.90  (step-pop @p609 :rule scope :premises (@p559))
% 0.75/0.90  (step @p560 :rule process_scope :premises (@p609) :args (@t663))
% 0.75/0.90  (step @p562 :rule eq_resolve :premises (@p560 @p557))
% 0.75/0.90  (step @p563 :rule implies_elim :premises (@p562))
% 0.75/0.90  (step @p564 :rule eq_resolve :premises (@p563 @p550))
% 0.75/0.90  (step @p565 :rule chain_m_resolution :premises (@p564 @p547) :args (@t660 @t664 (@list @t649)))
% 0.75/0.90  (step @p566 :rule bool-double-not-elim :args (@t657))
% 0.75/0.90  (step @p567 :rule refl :args (@t659))
% 0.75/0.90  (step @p568 :rule nary_cong :premises (@p567 @p566) :args ((or @t659 (not @t658))))
% 0.75/0.90  (step @p569 :rule cnf_or_neg :args (@t659 0))
% 0.75/0.90  (step @p570 :rule eq_resolve :premises (@p569 @p568))
% 0.75/0.90  (step @p571 :rule reordering :premises (@p570) :args ((or @t657 @t659)))
% 0.75/0.90  (step @p572 :rule chain_m_resolution :premises (@p571 @p565) :args (@t657 @t664 @t665))
% 0.75/0.90  (step @p573 :rule bool-double-not-elim :args (@t654))
% 0.75/0.90  (step @p574 :rule nary_cong :premises (@p567 @p573) :args ((or @t659 (not @t655))))
% 0.75/0.90  (step @p575 :rule cnf_or_neg :args (@t659 1))
% 0.75/0.90  (step @p576 :rule eq_resolve :premises (@p575 @p574))
% 0.75/0.90  (step @p577 :rule reordering :premises (@p576) :args ((or @t654 @t659)))
% 0.75/0.90  (step @p578 :rule chain_m_resolution :premises (@p577 @p565) :args (@t654 @t664 @t665))
% 0.75/0.90  (step @p579 :rule refl :args ((tptp.member_val tptp.phi_s @t4)))
% 0.75/0.90  (step @p580 :rule refl :args (@t666))
% 0.75/0.90  (step @p581 :rule refl :args (tptp.phi_s))
% 0.75/0.90  (step @p582 :rule cong :premises (@p581 @p580) :args (@t667))
% 0.75/0.90  (step @p583 :rule trans :premises (@p582 @p579))
% 0.75/0.90  (step @p584 :rule refl :args (@t560))
% 0.75/0.90  (step @p585 :rule ho_cong :premises (@p584 @p580))
% 0.75/0.90  (step @p586 :rule cong :premises (@p585 @p583) :args ((= (_ @t560 @t666) @t667)))
% 0.75/0.90  (step @p587 :rule symm :premises (@p586))
% 0.75/0.90  (step @p588 :rule refl :args (@t561))
% 0.75/0.90  (step @p589 :rule eq_resolve :premises (@p588 @p587))
% 0.75/0.90  (step @p590 :rule refl :args (@t4))
% 0.75/0.90  (step @p591 :rule cong :premises (@p590 @p580) :args ((= @t4 @t666)))
% 0.75/0.90  (step @p592 :rule symm :premises (@p591))
% 0.75/0.90  (step @p593 :rule eq_resolve :premises (@p590 @p592))
% 0.75/0.90  (step @p594 :rule refl :args (@t560))
% 0.75/0.90  (step @p595 :rule ho_cong :premises (@p594 @p593))
% 0.75/0.90  (step @p596 :rule trans :premises (@p595 @p589))
% 0.75/0.90  (step @p597 :rule cong :premises (@p596) :args (@t562))
% 0.75/0.90  (step @p598 :rule eq_resolve :premises (@p335 @p597))
% 0.75/0.90  (step @p599 :rule cnf_or_pos :args (@t668))
% 0.75/0.90  (step @p600 :rule reordering :premises (@p599) :args ((or @t667 @t655 @t658 @t669)))
% 0.75/0.90  (step @p601 :rule chain_m_resolution :premises (@p600 @p598 @p578 @p572) :args (@t669 (@list true false false) (@list @t667 @t654 @t657)))
% 0.75/0.90  (assume-push @p610 @t670)
% 0.75/0.90  (step @p603 :rule instantiate :premises (@p530) :args ((@list tptp.g2 tptp.phi2 tptp.phi_s @t653)))
% 0.75/0.90  (step-pop @p611 :rule scope :premises (@p603))
% 0.75/0.90  (step @p604 :rule process_scope :premises (@p611) :args (@t668))
% 0.75/0.90  (step @p606 :rule implies_elim :premises (@p604))
% 0.75/0.90  (step @p607 false :rule chain_m_resolution :premises (@p606 @p601 @p530) :args (false (@list true false) (@list @t668 @t670)))
% 0.75/0.90  )
% 0.75/0.90  % SZS output end Proof
% 0.75/0.90  % cvc5 exiting
%------------------------------------------------------------------------------