%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NUM587+3 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art04.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Wed Dec 29 20:23:01 EST 2010
% Result : Theorem 13.12s
% Output : Solution 13.12s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP6371/NUM587+3.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP6371/NUM587+3.tptp
% SZS output start Solution for /tmp/SystemOnTPTP6371/NUM587+3.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 6467
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% PrfWatch: 1.92 CPU 2.01 WC
% PrfWatch: 3.91 CPU 4.01 WC
% PrfWatch: 5.91 CPU 6.02 WC
% PrfWatch: 7.90 CPU 8.02 WC
% # Preprocessing time : 0.565 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 9.89 CPU 10.03 WC
% PrfWatch: 11.88 CPU 12.03 WC
% # SZS output start CNFRefutation.
% fof(44, axiom,![X1]:(aFunction0(X1)=>![X2]:(aElementOf0(X2,szDzozmdt0(X1))=>aElementOf0(sdtlpdtrp0(X1,X2),sdtlcdtrc0(X1,szDzozmdt0(X1))))),file('/tmp/SRASS.s.p', mImgRng)).
% fof(49, axiom,((((((aFunction0(xc)&![X1]:((aElementOf0(X1,szDzozmdt0(xc))=>(((aSet0(X1)&![X2]:(aElementOf0(X2,X1)=>aElementOf0(X2,xS)))&aSubsetOf0(X1,xS))&sbrdtbr0(X1)=xK))&((((aSet0(X1)&![X2]:(aElementOf0(X2,X1)=>aElementOf0(X2,xS)))|aSubsetOf0(X1,xS))&sbrdtbr0(X1)=xK)=>aElementOf0(X1,szDzozmdt0(xc)))))&szDzozmdt0(xc)=slbdtsldtrb0(xS,xK))&aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc))))&![X1]:(aElementOf0(X1,sdtlcdtrc0(xc,szDzozmdt0(xc)))<=>?[X2]:(aElementOf0(X2,szDzozmdt0(xc))&sdtlpdtrp0(xc,X2)=X1)))&![X1]:(aElementOf0(X1,sdtlcdtrc0(xc,szDzozmdt0(xc)))=>aElementOf0(X1,xT)))&aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)),file('/tmp/SRASS.s.p', m__3453)).
% fof(59, axiom,((aFunction0(xC)&szDzozmdt0(xC)=szNzAzT0)&![X1]:(aElementOf0(X1,szNzAzT0)=>(((((((aFunction0(sdtlpdtrp0(xC,X1))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1)))&![X2]:(aElementOf0(X2,sdtlpdtrp0(xN,X1))=>sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X2)))&aSet0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))))&![X2]:(aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))<=>((aElement0(X2)&aElementOf0(X2,sdtlpdtrp0(xN,X1)))&~(X2=szmzizndt0(sdtlpdtrp0(xN,X1))))))&![X2]:((aElementOf0(X2,szDzozmdt0(sdtlpdtrp0(xC,X1)))=>(((aSet0(X2)&![X3]:(aElementOf0(X3,X2)=>aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))))&aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))))&sbrdtbr0(X2)=xk))&((((aSet0(X2)&![X3]:(aElementOf0(X3,X2)=>aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))))|aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))))&sbrdtbr0(X2)=xk)=>aElementOf0(X2,szDzozmdt0(sdtlpdtrp0(xC,X1))))))&szDzozmdt0(sdtlpdtrp0(xC,X1))=slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))),xk))&![X2]:((aSet0(X2)&((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1))&![X3]:(aElementOf0(X3,sdtlpdtrp0(xN,X1))=>sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X3)))=>((aSet0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))&![X3]:(aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))<=>((aElement0(X3)&aElementOf0(X3,sdtlpdtrp0(xN,X1)))&~(X3=szmzizndt0(sdtlpdtrp0(xN,X1))))))=>(((![X3]:(aElementOf0(X3,X2)=>aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))))|aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))))&sbrdtbr0(X2)=xk)|aElementOf0(X2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))),xk))))))=>(((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1))&![X3]:(aElementOf0(X3,sdtlpdtrp0(xN,X1))=>sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X3)))&![X3]:(aElementOf0(X3,sdtpldt0(X2,szmzizndt0(sdtlpdtrp0(xN,X1))))<=>(aElement0(X3)&(aElementOf0(X3,X2)|X3=szmzizndt0(sdtlpdtrp0(xN,X1))))))&sdtlpdtrp0(sdtlpdtrp0(xC,X1),X2)=sdtlpdtrp0(xc,sdtpldt0(X2,szmzizndt0(sdtlpdtrp0(xN,X1))))))))),file('/tmp/SRASS.s.p', m__4151)).
% fof(60, axiom,aElementOf0(xi,szNzAzT0),file('/tmp/SRASS.s.p', m__4200)).
% fof(62, axiom,(((((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&![X1]:(aElementOf0(X1,sdtlpdtrp0(xN,xi))=>sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X1)))&aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))&![X1]:(aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))<=>((aElement0(X1)&aElementOf0(X1,sdtlpdtrp0(xN,xi)))&~(X1=szmzizndt0(sdtlpdtrp0(xN,xi))))))&aSet0(xQ))&![X1]:(aElementOf0(X1,xQ)=>aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))))&aSubsetOf0(xQ,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))&sbrdtbr0(xQ)=xk)&aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk)))&sdtlpdtrp0(sdtlpdtrp0(xC,xi),xQ)=xx),file('/tmp/SRASS.s.p', m__4237)).
% fof(63, axiom,((((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&![X1]:(aElementOf0(X1,sdtlpdtrp0(xN,xi))=>sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X1)))&aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))&![X1]:(aElementOf0(X1,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))<=>(aElement0(X1)&(aElementOf0(X1,xQ)|X1=szmzizndt0(sdtlpdtrp0(xN,xi))))))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)))&![X1]:(aElementOf0(X1,sdtlpdtrp0(xN,xi))=>sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X1)))&aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))&![X1]:(aElementOf0(X1,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))<=>(aElement0(X1)&(aElementOf0(X1,xQ)|X1=szmzizndt0(sdtlpdtrp0(xN,xi))))))&?[X1]:(aElementOf0(X1,szDzozmdt0(xc))&sdtlpdtrp0(xc,X1)=sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))),file('/tmp/SRASS.s.p', m__4263)).
% fof(91, conjecture,aElementOf0(xx,xT),file('/tmp/SRASS.s.p', m__)).
% fof(92, negated_conjecture,~(aElementOf0(xx,xT)),inference(assume_negation,[status(cth)],[91])).
% fof(105, negated_conjecture,~(aElementOf0(xx,xT)),inference(fof_simplification,[status(thm)],[92,theory(equality)])).
% fof(107, plain,![X1]:(epred2_1(X1)=>(((((((aFunction0(sdtlpdtrp0(xC,X1))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1)))&![X2]:(aElementOf0(X2,sdtlpdtrp0(xN,X1))=>sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X2)))&aSet0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))))&![X2]:(aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))<=>((aElement0(X2)&aElementOf0(X2,sdtlpdtrp0(xN,X1)))&~(X2=szmzizndt0(sdtlpdtrp0(xN,X1))))))&![X2]:((aElementOf0(X2,szDzozmdt0(sdtlpdtrp0(xC,X1)))=>(((aSet0(X2)&![X3]:(aElementOf0(X3,X2)=>aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))))&aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))))&sbrdtbr0(X2)=xk))&((((aSet0(X2)&![X3]:(aElementOf0(X3,X2)=>aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))))|aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))))&sbrdtbr0(X2)=xk)=>aElementOf0(X2,szDzozmdt0(sdtlpdtrp0(xC,X1))))))&szDzozmdt0(sdtlpdtrp0(xC,X1))=slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))),xk))&![X2]:((aSet0(X2)&((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1))&![X3]:(aElementOf0(X3,sdtlpdtrp0(xN,X1))=>sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X3)))=>((aSet0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))&![X3]:(aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))<=>((aElement0(X3)&aElementOf0(X3,sdtlpdtrp0(xN,X1)))&~(X3=szmzizndt0(sdtlpdtrp0(xN,X1))))))=>(((![X3]:(aElementOf0(X3,X2)=>aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))))|aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))))&sbrdtbr0(X2)=xk)|aElementOf0(X2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))),xk))))))=>(((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1))&![X3]:(aElementOf0(X3,sdtlpdtrp0(xN,X1))=>sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X3)))&![X3]:(aElementOf0(X3,sdtpldt0(X2,szmzizndt0(sdtlpdtrp0(xN,X1))))<=>(aElement0(X3)&(aElementOf0(X3,X2)|X3=szmzizndt0(sdtlpdtrp0(xN,X1))))))&sdtlpdtrp0(sdtlpdtrp0(xC,X1),X2)=sdtlpdtrp0(xc,sdtpldt0(X2,szmzizndt0(sdtlpdtrp0(xN,X1)))))))),introduced(definition)).
% fof(109, plain,((aFunction0(xC)&szDzozmdt0(xC)=szNzAzT0)&![X1]:(aElementOf0(X1,szNzAzT0)=>epred2_1(X1))),inference(apply_def,[status(esa)],[59,107,theory(equality)])).
% fof(312, plain,![X1]:(~(aFunction0(X1))|![X2]:(~(aElementOf0(X2,szDzozmdt0(X1)))|aElementOf0(sdtlpdtrp0(X1,X2),sdtlcdtrc0(X1,szDzozmdt0(X1))))),inference(fof_nnf,[status(thm)],[44])).
% fof(313, plain,![X3]:(~(aFunction0(X3))|![X4]:(~(aElementOf0(X4,szDzozmdt0(X3)))|aElementOf0(sdtlpdtrp0(X3,X4),sdtlcdtrc0(X3,szDzozmdt0(X3))))),inference(variable_rename,[status(thm)],[312])).
% fof(314, plain,![X3]:![X4]:((~(aElementOf0(X4,szDzozmdt0(X3)))|aElementOf0(sdtlpdtrp0(X3,X4),sdtlcdtrc0(X3,szDzozmdt0(X3))))|~(aFunction0(X3))),inference(shift_quantors,[status(thm)],[313])).
% cnf(315,plain,(aElementOf0(sdtlpdtrp0(X1,X2),sdtlcdtrc0(X1,szDzozmdt0(X1)))|~aFunction0(X1)|~aElementOf0(X2,szDzozmdt0(X1))),inference(split_conjunct,[status(thm)],[314])).
% fof(335, plain,((((((aFunction0(xc)&![X1]:((~(aElementOf0(X1,szDzozmdt0(xc)))|(((aSet0(X1)&![X2]:(~(aElementOf0(X2,X1))|aElementOf0(X2,xS)))&aSubsetOf0(X1,xS))&sbrdtbr0(X1)=xK))&((((~(aSet0(X1))|?[X2]:(aElementOf0(X2,X1)&~(aElementOf0(X2,xS))))&~(aSubsetOf0(X1,xS)))|~(sbrdtbr0(X1)=xK))|aElementOf0(X1,szDzozmdt0(xc)))))&szDzozmdt0(xc)=slbdtsldtrb0(xS,xK))&aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc))))&![X1]:((~(aElementOf0(X1,sdtlcdtrc0(xc,szDzozmdt0(xc))))|?[X2]:(aElementOf0(X2,szDzozmdt0(xc))&sdtlpdtrp0(xc,X2)=X1))&(![X2]:(~(aElementOf0(X2,szDzozmdt0(xc)))|~(sdtlpdtrp0(xc,X2)=X1))|aElementOf0(X1,sdtlcdtrc0(xc,szDzozmdt0(xc))))))&![X1]:(~(aElementOf0(X1,sdtlcdtrc0(xc,szDzozmdt0(xc))))|aElementOf0(X1,xT)))&aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)),inference(fof_nnf,[status(thm)],[49])).
% fof(336, plain,((((((aFunction0(xc)&![X3]:((~(aElementOf0(X3,szDzozmdt0(xc)))|(((aSet0(X3)&![X4]:(~(aElementOf0(X4,X3))|aElementOf0(X4,xS)))&aSubsetOf0(X3,xS))&sbrdtbr0(X3)=xK))&((((~(aSet0(X3))|?[X5]:(aElementOf0(X5,X3)&~(aElementOf0(X5,xS))))&~(aSubsetOf0(X3,xS)))|~(sbrdtbr0(X3)=xK))|aElementOf0(X3,szDzozmdt0(xc)))))&szDzozmdt0(xc)=slbdtsldtrb0(xS,xK))&aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc))))&![X6]:((~(aElementOf0(X6,sdtlcdtrc0(xc,szDzozmdt0(xc))))|?[X7]:(aElementOf0(X7,szDzozmdt0(xc))&sdtlpdtrp0(xc,X7)=X6))&(![X8]:(~(aElementOf0(X8,szDzozmdt0(xc)))|~(sdtlpdtrp0(xc,X8)=X6))|aElementOf0(X6,sdtlcdtrc0(xc,szDzozmdt0(xc))))))&![X9]:(~(aElementOf0(X9,sdtlcdtrc0(xc,szDzozmdt0(xc))))|aElementOf0(X9,xT)))&aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)),inference(variable_rename,[status(thm)],[335])).
% fof(337, plain,((((((aFunction0(xc)&![X3]:((~(aElementOf0(X3,szDzozmdt0(xc)))|(((aSet0(X3)&![X4]:(~(aElementOf0(X4,X3))|aElementOf0(X4,xS)))&aSubsetOf0(X3,xS))&sbrdtbr0(X3)=xK))&((((~(aSet0(X3))|(aElementOf0(esk13_1(X3),X3)&~(aElementOf0(esk13_1(X3),xS))))&~(aSubsetOf0(X3,xS)))|~(sbrdtbr0(X3)=xK))|aElementOf0(X3,szDzozmdt0(xc)))))&szDzozmdt0(xc)=slbdtsldtrb0(xS,xK))&aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc))))&![X6]:((~(aElementOf0(X6,sdtlcdtrc0(xc,szDzozmdt0(xc))))|(aElementOf0(esk14_1(X6),szDzozmdt0(xc))&sdtlpdtrp0(xc,esk14_1(X6))=X6))&(![X8]:(~(aElementOf0(X8,szDzozmdt0(xc)))|~(sdtlpdtrp0(xc,X8)=X6))|aElementOf0(X6,sdtlcdtrc0(xc,szDzozmdt0(xc))))))&![X9]:(~(aElementOf0(X9,sdtlcdtrc0(xc,szDzozmdt0(xc))))|aElementOf0(X9,xT)))&aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)),inference(skolemize,[status(esa)],[336])).
% fof(338, plain,![X3]:![X4]:![X6]:![X8]:![X9]:(((~(aElementOf0(X9,sdtlcdtrc0(xc,szDzozmdt0(xc))))|aElementOf0(X9,xT))&((((~(aElementOf0(X8,szDzozmdt0(xc)))|~(sdtlpdtrp0(xc,X8)=X6))|aElementOf0(X6,sdtlcdtrc0(xc,szDzozmdt0(xc))))&(~(aElementOf0(X6,sdtlcdtrc0(xc,szDzozmdt0(xc))))|(aElementOf0(esk14_1(X6),szDzozmdt0(xc))&sdtlpdtrp0(xc,esk14_1(X6))=X6)))&(((((((((~(aElementOf0(X4,X3))|aElementOf0(X4,xS))&aSet0(X3))&aSubsetOf0(X3,xS))&sbrdtbr0(X3)=xK)|~(aElementOf0(X3,szDzozmdt0(xc))))&((((~(aSet0(X3))|(aElementOf0(esk13_1(X3),X3)&~(aElementOf0(esk13_1(X3),xS))))&~(aSubsetOf0(X3,xS)))|~(sbrdtbr0(X3)=xK))|aElementOf0(X3,szDzozmdt0(xc))))&aFunction0(xc))&szDzozmdt0(xc)=slbdtsldtrb0(xS,xK))&aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc))))))&aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)),inference(shift_quantors,[status(thm)],[337])).
% fof(339, plain,![X3]:![X4]:![X6]:![X8]:![X9]:(((~(aElementOf0(X9,sdtlcdtrc0(xc,szDzozmdt0(xc))))|aElementOf0(X9,xT))&((((~(aElementOf0(X8,szDzozmdt0(xc)))|~(sdtlpdtrp0(xc,X8)=X6))|aElementOf0(X6,sdtlcdtrc0(xc,szDzozmdt0(xc))))&((aElementOf0(esk14_1(X6),szDzozmdt0(xc))|~(aElementOf0(X6,sdtlcdtrc0(xc,szDzozmdt0(xc)))))&(sdtlpdtrp0(xc,esk14_1(X6))=X6|~(aElementOf0(X6,sdtlcdtrc0(xc,szDzozmdt0(xc)))))))&(((((((((~(aElementOf0(X4,X3))|aElementOf0(X4,xS))|~(aElementOf0(X3,szDzozmdt0(xc))))&(aSet0(X3)|~(aElementOf0(X3,szDzozmdt0(xc)))))&(aSubsetOf0(X3,xS)|~(aElementOf0(X3,szDzozmdt0(xc)))))&(sbrdtbr0(X3)=xK|~(aElementOf0(X3,szDzozmdt0(xc)))))&(((((aElementOf0(esk13_1(X3),X3)|~(aSet0(X3)))|~(sbrdtbr0(X3)=xK))|aElementOf0(X3,szDzozmdt0(xc)))&(((~(aElementOf0(esk13_1(X3),xS))|~(aSet0(X3)))|~(sbrdtbr0(X3)=xK))|aElementOf0(X3,szDzozmdt0(xc))))&((~(aSubsetOf0(X3,xS))|~(sbrdtbr0(X3)=xK))|aElementOf0(X3,szDzozmdt0(xc)))))&aFunction0(xc))&szDzozmdt0(xc)=slbdtsldtrb0(xS,xK))&aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc))))))&aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)),inference(distribute,[status(thm)],[338])).
% cnf(343,plain,(aFunction0(xc)),inference(split_conjunct,[status(thm)],[339])).
% cnf(354,plain,(aElementOf0(X1,xT)|~aElementOf0(X1,sdtlcdtrc0(xc,szDzozmdt0(xc)))),inference(split_conjunct,[status(thm)],[339])).
% fof(4401, plain,((aFunction0(xC)&szDzozmdt0(xC)=szNzAzT0)&![X1]:(~(aElementOf0(X1,szNzAzT0))|epred2_1(X1))),inference(fof_nnf,[status(thm)],[109])).
% fof(4402, plain,((aFunction0(xC)&szDzozmdt0(xC)=szNzAzT0)&![X2]:(~(aElementOf0(X2,szNzAzT0))|epred2_1(X2))),inference(variable_rename,[status(thm)],[4401])).
% fof(4403, plain,![X2]:((~(aElementOf0(X2,szNzAzT0))|epred2_1(X2))&(aFunction0(xC)&szDzozmdt0(xC)=szNzAzT0)),inference(shift_quantors,[status(thm)],[4402])).
% cnf(4406,plain,(epred2_1(X1)|~aElementOf0(X1,szNzAzT0)),inference(split_conjunct,[status(thm)],[4403])).
% cnf(4407,plain,(aElementOf0(xi,szNzAzT0)),inference(split_conjunct,[status(thm)],[60])).
% fof(4413, plain,(((((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&![X1]:(~(aElementOf0(X1,sdtlpdtrp0(xN,xi)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X1)))&aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))&![X1]:((~(aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))|((aElement0(X1)&aElementOf0(X1,sdtlpdtrp0(xN,xi)))&~(X1=szmzizndt0(sdtlpdtrp0(xN,xi)))))&(((~(aElement0(X1))|~(aElementOf0(X1,sdtlpdtrp0(xN,xi))))|X1=szmzizndt0(sdtlpdtrp0(xN,xi)))|aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))&aSet0(xQ))&![X1]:(~(aElementOf0(X1,xQ))|aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))))&aSubsetOf0(xQ,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))&sbrdtbr0(xQ)=xk)&aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk)))&sdtlpdtrp0(sdtlpdtrp0(xC,xi),xQ)=xx),inference(fof_nnf,[status(thm)],[62])).
% fof(4414, plain,(((((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&![X2]:(~(aElementOf0(X2,sdtlpdtrp0(xN,xi)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X2)))&aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))&![X3]:((~(aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))|((aElement0(X3)&aElementOf0(X3,sdtlpdtrp0(xN,xi)))&~(X3=szmzizndt0(sdtlpdtrp0(xN,xi)))))&(((~(aElement0(X3))|~(aElementOf0(X3,sdtlpdtrp0(xN,xi))))|X3=szmzizndt0(sdtlpdtrp0(xN,xi)))|aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))&aSet0(xQ))&![X4]:(~(aElementOf0(X4,xQ))|aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))))&aSubsetOf0(xQ,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))&sbrdtbr0(xQ)=xk)&aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk)))&sdtlpdtrp0(sdtlpdtrp0(xC,xi),xQ)=xx),inference(variable_rename,[status(thm)],[4413])).
% fof(4415, plain,![X2]:![X3]:![X4]:((((((~(aElementOf0(X4,xQ))|aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))&((((~(aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))|((aElement0(X3)&aElementOf0(X3,sdtlpdtrp0(xN,xi)))&~(X3=szmzizndt0(sdtlpdtrp0(xN,xi)))))&(((~(aElement0(X3))|~(aElementOf0(X3,sdtlpdtrp0(xN,xi))))|X3=szmzizndt0(sdtlpdtrp0(xN,xi)))|aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))))&(((~(aElementOf0(X2,sdtlpdtrp0(xN,xi)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X2))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)))&aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))))&aSet0(xQ)))&aSubsetOf0(xQ,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))&sbrdtbr0(xQ)=xk)&aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk)))&sdtlpdtrp0(sdtlpdtrp0(xC,xi),xQ)=xx),inference(shift_quantors,[status(thm)],[4414])).
% fof(4416, plain,![X2]:![X3]:![X4]:((((((~(aElementOf0(X4,xQ))|aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))&((((((aElement0(X3)|~(aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))))&(aElementOf0(X3,sdtlpdtrp0(xN,xi))|~(aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))&(~(X3=szmzizndt0(sdtlpdtrp0(xN,xi)))|~(aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))&(((~(aElement0(X3))|~(aElementOf0(X3,sdtlpdtrp0(xN,xi))))|X3=szmzizndt0(sdtlpdtrp0(xN,xi)))|aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))))&(((~(aElementOf0(X2,sdtlpdtrp0(xN,xi)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X2))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)))&aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))))&aSet0(xQ)))&aSubsetOf0(xQ,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))&sbrdtbr0(xQ)=xk)&aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk)))&sdtlpdtrp0(sdtlpdtrp0(xC,xi),xQ)=xx),inference(distribute,[status(thm)],[4415])).
% cnf(4417,plain,(sdtlpdtrp0(sdtlpdtrp0(xC,xi),xQ)=xx),inference(split_conjunct,[status(thm)],[4416])).
% cnf(4418,plain,(aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk))),inference(split_conjunct,[status(thm)],[4416])).
% cnf(4421,plain,(aSet0(xQ)),inference(split_conjunct,[status(thm)],[4416])).
% fof(4430, plain,((((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&![X1]:(~(aElementOf0(X1,sdtlpdtrp0(xN,xi)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X1)))&aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))&![X1]:((~(aElementOf0(X1,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))|(aElement0(X1)&(aElementOf0(X1,xQ)|X1=szmzizndt0(sdtlpdtrp0(xN,xi)))))&((~(aElement0(X1))|(~(aElementOf0(X1,xQ))&~(X1=szmzizndt0(sdtlpdtrp0(xN,xi)))))|aElementOf0(X1,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)))&![X1]:(~(aElementOf0(X1,sdtlpdtrp0(xN,xi)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X1)))&aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))&![X1]:((~(aElementOf0(X1,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))|(aElement0(X1)&(aElementOf0(X1,xQ)|X1=szmzizndt0(sdtlpdtrp0(xN,xi)))))&((~(aElement0(X1))|(~(aElementOf0(X1,xQ))&~(X1=szmzizndt0(sdtlpdtrp0(xN,xi)))))|aElementOf0(X1,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))))&?[X1]:(aElementOf0(X1,szDzozmdt0(xc))&sdtlpdtrp0(xc,X1)=sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))),inference(fof_nnf,[status(thm)],[63])).
% fof(4431, plain,((((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&![X2]:(~(aElementOf0(X2,sdtlpdtrp0(xN,xi)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X2)))&aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))&![X3]:((~(aElementOf0(X3,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))|(aElement0(X3)&(aElementOf0(X3,xQ)|X3=szmzizndt0(sdtlpdtrp0(xN,xi)))))&((~(aElement0(X3))|(~(aElementOf0(X3,xQ))&~(X3=szmzizndt0(sdtlpdtrp0(xN,xi)))))|aElementOf0(X3,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)))&![X4]:(~(aElementOf0(X4,sdtlpdtrp0(xN,xi)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X4)))&aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))&![X5]:((~(aElementOf0(X5,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))|(aElement0(X5)&(aElementOf0(X5,xQ)|X5=szmzizndt0(sdtlpdtrp0(xN,xi)))))&((~(aElement0(X5))|(~(aElementOf0(X5,xQ))&~(X5=szmzizndt0(sdtlpdtrp0(xN,xi)))))|aElementOf0(X5,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))))&?[X6]:(aElementOf0(X6,szDzozmdt0(xc))&sdtlpdtrp0(xc,X6)=sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))),inference(variable_rename,[status(thm)],[4430])).
% fof(4432, plain,((((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&![X2]:(~(aElementOf0(X2,sdtlpdtrp0(xN,xi)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X2)))&aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))&![X3]:((~(aElementOf0(X3,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))|(aElement0(X3)&(aElementOf0(X3,xQ)|X3=szmzizndt0(sdtlpdtrp0(xN,xi)))))&((~(aElement0(X3))|(~(aElementOf0(X3,xQ))&~(X3=szmzizndt0(sdtlpdtrp0(xN,xi)))))|aElementOf0(X3,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)))&![X4]:(~(aElementOf0(X4,sdtlpdtrp0(xN,xi)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X4)))&aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))&![X5]:((~(aElementOf0(X5,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))|(aElement0(X5)&(aElementOf0(X5,xQ)|X5=szmzizndt0(sdtlpdtrp0(xN,xi)))))&((~(aElement0(X5))|(~(aElementOf0(X5,xQ))&~(X5=szmzizndt0(sdtlpdtrp0(xN,xi)))))|aElementOf0(X5,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))))&(aElementOf0(esk26_0,szDzozmdt0(xc))&sdtlpdtrp0(xc,esk26_0)=sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))),inference(skolemize,[status(esa)],[4431])).
% fof(4433, plain,![X2]:![X3]:![X4]:![X5]:((((~(aElementOf0(X5,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))|(aElement0(X5)&(aElementOf0(X5,xQ)|X5=szmzizndt0(sdtlpdtrp0(xN,xi)))))&((~(aElement0(X5))|(~(aElementOf0(X5,xQ))&~(X5=szmzizndt0(sdtlpdtrp0(xN,xi)))))|aElementOf0(X5,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))))&(((~(aElementOf0(X4,sdtlpdtrp0(xN,xi)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X4))&((((~(aElementOf0(X3,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))|(aElement0(X3)&(aElementOf0(X3,xQ)|X3=szmzizndt0(sdtlpdtrp0(xN,xi)))))&((~(aElement0(X3))|(~(aElementOf0(X3,xQ))&~(X3=szmzizndt0(sdtlpdtrp0(xN,xi)))))|aElementOf0(X3,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))))&(((~(aElementOf0(X2,sdtlpdtrp0(xN,xi)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X2))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)))&aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))))&aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))))&(aElementOf0(esk26_0,szDzozmdt0(xc))&sdtlpdtrp0(xc,esk26_0)=sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))),inference(shift_quantors,[status(thm)],[4432])).
% fof(4434, plain,![X2]:![X3]:![X4]:![X5]:(((((aElement0(X5)|~(aElementOf0(X5,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))))&((aElementOf0(X5,xQ)|X5=szmzizndt0(sdtlpdtrp0(xN,xi)))|~(aElementOf0(X5,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))))&(((~(aElementOf0(X5,xQ))|~(aElement0(X5)))|aElementOf0(X5,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))&((~(X5=szmzizndt0(sdtlpdtrp0(xN,xi)))|~(aElement0(X5)))|aElementOf0(X5,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))))&(((~(aElementOf0(X4,sdtlpdtrp0(xN,xi)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X4))&(((((aElement0(X3)|~(aElementOf0(X3,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))))&((aElementOf0(X3,xQ)|X3=szmzizndt0(sdtlpdtrp0(xN,xi)))|~(aElementOf0(X3,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))))&(((~(aElementOf0(X3,xQ))|~(aElement0(X3)))|aElementOf0(X3,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))&((~(X3=szmzizndt0(sdtlpdtrp0(xN,xi)))|~(aElement0(X3)))|aElementOf0(X3,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))))&(((~(aElementOf0(X2,sdtlpdtrp0(xN,xi)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X2))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)))&aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))))&aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))))&(aElementOf0(esk26_0,szDzozmdt0(xc))&sdtlpdtrp0(xc,esk26_0)=sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))))),inference(distribute,[status(thm)],[4433])).
% cnf(4435,plain,(sdtlpdtrp0(xc,esk26_0)=sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))),inference(split_conjunct,[status(thm)],[4434])).
% cnf(4436,plain,(aElementOf0(esk26_0,szDzozmdt0(xc))),inference(split_conjunct,[status(thm)],[4434])).
% cnf(4577,negated_conjecture,(~aElementOf0(xx,xT)),inference(split_conjunct,[status(thm)],[105])).
% fof(4704, plain,![X1]:(~(epred2_1(X1))|(((((((aFunction0(sdtlpdtrp0(xC,X1))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1)))&![X2]:(~(aElementOf0(X2,sdtlpdtrp0(xN,X1)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X2)))&aSet0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))))&![X2]:((~(aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))))|((aElement0(X2)&aElementOf0(X2,sdtlpdtrp0(xN,X1)))&~(X2=szmzizndt0(sdtlpdtrp0(xN,X1)))))&(((~(aElement0(X2))|~(aElementOf0(X2,sdtlpdtrp0(xN,X1))))|X2=szmzizndt0(sdtlpdtrp0(xN,X1)))|aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))))))&![X2]:((~(aElementOf0(X2,szDzozmdt0(sdtlpdtrp0(xC,X1))))|(((aSet0(X2)&![X3]:(~(aElementOf0(X3,X2))|aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))))&aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))))&sbrdtbr0(X2)=xk))&((((~(aSet0(X2))|?[X3]:(aElementOf0(X3,X2)&~(aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))))))&~(aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))))|~(sbrdtbr0(X2)=xk))|aElementOf0(X2,szDzozmdt0(sdtlpdtrp0(xC,X1))))))&szDzozmdt0(sdtlpdtrp0(xC,X1))=slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))),xk))&![X2]:((~(aSet0(X2))|((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1))&![X3]:(~(aElementOf0(X3,sdtlpdtrp0(xN,X1)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X3)))&((aSet0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))&![X3]:((~(aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))))|((aElement0(X3)&aElementOf0(X3,sdtlpdtrp0(xN,X1)))&~(X3=szmzizndt0(sdtlpdtrp0(xN,X1)))))&(((~(aElement0(X3))|~(aElementOf0(X3,sdtlpdtrp0(xN,X1))))|X3=szmzizndt0(sdtlpdtrp0(xN,X1)))|aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))))))&(((?[X3]:(aElementOf0(X3,X2)&~(aElementOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))))&~(aSubsetOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))))|~(sbrdtbr0(X2)=xk))&~(aElementOf0(X2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))),xk)))))))|(((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1))&![X3]:(~(aElementOf0(X3,sdtlpdtrp0(xN,X1)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X3)))&![X3]:((~(aElementOf0(X3,sdtpldt0(X2,szmzizndt0(sdtlpdtrp0(xN,X1)))))|(aElement0(X3)&(aElementOf0(X3,X2)|X3=szmzizndt0(sdtlpdtrp0(xN,X1)))))&((~(aElement0(X3))|(~(aElementOf0(X3,X2))&~(X3=szmzizndt0(sdtlpdtrp0(xN,X1)))))|aElementOf0(X3,sdtpldt0(X2,szmzizndt0(sdtlpdtrp0(xN,X1)))))))&sdtlpdtrp0(sdtlpdtrp0(xC,X1),X2)=sdtlpdtrp0(xc,sdtpldt0(X2,szmzizndt0(sdtlpdtrp0(xN,X1)))))))),inference(fof_nnf,[status(thm)],[107])).
% fof(4705, plain,![X4]:(~(epred2_1(X4))|(((((((aFunction0(sdtlpdtrp0(xC,X4))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4)))&![X5]:(~(aElementOf0(X5,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X5)))&aSet0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))&![X6]:((~(aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|((aElement0(X6)&aElementOf0(X6,sdtlpdtrp0(xN,X4)))&~(X6=szmzizndt0(sdtlpdtrp0(xN,X4)))))&(((~(aElement0(X6))|~(aElementOf0(X6,sdtlpdtrp0(xN,X4))))|X6=szmzizndt0(sdtlpdtrp0(xN,X4)))|aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))))&![X7]:((~(aElementOf0(X7,szDzozmdt0(sdtlpdtrp0(xC,X4))))|(((aSet0(X7)&![X8]:(~(aElementOf0(X8,X7))|aElementOf0(X8,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))&aSubsetOf0(X7,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))&sbrdtbr0(X7)=xk))&((((~(aSet0(X7))|?[X9]:(aElementOf0(X9,X7)&~(aElementOf0(X9,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))))&~(aSubsetOf0(X7,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(sbrdtbr0(X7)=xk))|aElementOf0(X7,szDzozmdt0(sdtlpdtrp0(xC,X4))))))&szDzozmdt0(sdtlpdtrp0(xC,X4))=slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))),xk))&![X10]:((~(aSet0(X10))|((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4))&![X11]:(~(aElementOf0(X11,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X11)))&((aSet0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))&![X12]:((~(aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|((aElement0(X12)&aElementOf0(X12,sdtlpdtrp0(xN,X4)))&~(X12=szmzizndt0(sdtlpdtrp0(xN,X4)))))&(((~(aElement0(X12))|~(aElementOf0(X12,sdtlpdtrp0(xN,X4))))|X12=szmzizndt0(sdtlpdtrp0(xN,X4)))|aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))))&(((?[X13]:(aElementOf0(X13,X10)&~(aElementOf0(X13,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))&~(aSubsetOf0(X10,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(sbrdtbr0(X10)=xk))&~(aElementOf0(X10,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))),xk)))))))|(((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4))&![X14]:(~(aElementOf0(X14,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X14)))&![X15]:((~(aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))|(aElement0(X15)&(aElementOf0(X15,X10)|X15=szmzizndt0(sdtlpdtrp0(xN,X4)))))&((~(aElement0(X15))|(~(aElementOf0(X15,X10))&~(X15=szmzizndt0(sdtlpdtrp0(xN,X4)))))|aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))&sdtlpdtrp0(sdtlpdtrp0(xC,X4),X10)=sdtlpdtrp0(xc,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))),inference(variable_rename,[status(thm)],[4704])).
% fof(4706, plain,![X4]:(~(epred2_1(X4))|(((((((aFunction0(sdtlpdtrp0(xC,X4))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4)))&![X5]:(~(aElementOf0(X5,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X5)))&aSet0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))&![X6]:((~(aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|((aElement0(X6)&aElementOf0(X6,sdtlpdtrp0(xN,X4)))&~(X6=szmzizndt0(sdtlpdtrp0(xN,X4)))))&(((~(aElement0(X6))|~(aElementOf0(X6,sdtlpdtrp0(xN,X4))))|X6=szmzizndt0(sdtlpdtrp0(xN,X4)))|aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))))&![X7]:((~(aElementOf0(X7,szDzozmdt0(sdtlpdtrp0(xC,X4))))|(((aSet0(X7)&![X8]:(~(aElementOf0(X8,X7))|aElementOf0(X8,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))&aSubsetOf0(X7,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))&sbrdtbr0(X7)=xk))&((((~(aSet0(X7))|(aElementOf0(esk35_2(X4,X7),X7)&~(aElementOf0(esk35_2(X4,X7),sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))))&~(aSubsetOf0(X7,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(sbrdtbr0(X7)=xk))|aElementOf0(X7,szDzozmdt0(sdtlpdtrp0(xC,X4))))))&szDzozmdt0(sdtlpdtrp0(xC,X4))=slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))),xk))&![X10]:((~(aSet0(X10))|((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4))&![X11]:(~(aElementOf0(X11,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X11)))&((aSet0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))&![X12]:((~(aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|((aElement0(X12)&aElementOf0(X12,sdtlpdtrp0(xN,X4)))&~(X12=szmzizndt0(sdtlpdtrp0(xN,X4)))))&(((~(aElement0(X12))|~(aElementOf0(X12,sdtlpdtrp0(xN,X4))))|X12=szmzizndt0(sdtlpdtrp0(xN,X4)))|aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))))&((((aElementOf0(esk36_2(X4,X10),X10)&~(aElementOf0(esk36_2(X4,X10),sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))&~(aSubsetOf0(X10,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(sbrdtbr0(X10)=xk))&~(aElementOf0(X10,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))),xk)))))))|(((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4))&![X14]:(~(aElementOf0(X14,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X14)))&![X15]:((~(aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))|(aElement0(X15)&(aElementOf0(X15,X10)|X15=szmzizndt0(sdtlpdtrp0(xN,X4)))))&((~(aElement0(X15))|(~(aElementOf0(X15,X10))&~(X15=szmzizndt0(sdtlpdtrp0(xN,X4)))))|aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))&sdtlpdtrp0(sdtlpdtrp0(xC,X4),X10)=sdtlpdtrp0(xc,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))),inference(skolemize,[status(esa)],[4705])).
% fof(4707, plain,![X4]:![X5]:![X6]:![X7]:![X8]:![X10]:![X11]:![X12]:![X14]:![X15]:(((((((~(aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))|(aElement0(X15)&(aElementOf0(X15,X10)|X15=szmzizndt0(sdtlpdtrp0(xN,X4)))))&((~(aElement0(X15))|(~(aElementOf0(X15,X10))&~(X15=szmzizndt0(sdtlpdtrp0(xN,X4)))))|aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4))))))&((~(aElementOf0(X14,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X14))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4))))&sdtlpdtrp0(sdtlpdtrp0(xC,X4),X10)=sdtlpdtrp0(xc,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))|((((((~(aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|((aElement0(X12)&aElementOf0(X12,sdtlpdtrp0(xN,X4)))&~(X12=szmzizndt0(sdtlpdtrp0(xN,X4)))))&(((~(aElement0(X12))|~(aElementOf0(X12,sdtlpdtrp0(xN,X4))))|X12=szmzizndt0(sdtlpdtrp0(xN,X4)))|aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))&((((aElementOf0(esk36_2(X4,X10),X10)&~(aElementOf0(esk36_2(X4,X10),sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))&~(aSubsetOf0(X10,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(sbrdtbr0(X10)=xk))&~(aElementOf0(X10,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))),xk)))))&((~(aElementOf0(X11,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X11))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4))))|~(aSet0(X10))))&((((((((~(aElementOf0(X8,X7))|aElementOf0(X8,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))&aSet0(X7))&aSubsetOf0(X7,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))&sbrdtbr0(X7)=xk)|~(aElementOf0(X7,szDzozmdt0(sdtlpdtrp0(xC,X4)))))&((((~(aSet0(X7))|(aElementOf0(esk35_2(X4,X7),X7)&~(aElementOf0(esk35_2(X4,X7),sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))))&~(aSubsetOf0(X7,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(sbrdtbr0(X7)=xk))|aElementOf0(X7,szDzozmdt0(sdtlpdtrp0(xC,X4)))))&(((~(aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|((aElement0(X6)&aElementOf0(X6,sdtlpdtrp0(xN,X4)))&~(X6=szmzizndt0(sdtlpdtrp0(xN,X4)))))&(((~(aElement0(X6))|~(aElementOf0(X6,sdtlpdtrp0(xN,X4))))|X6=szmzizndt0(sdtlpdtrp0(xN,X4)))|aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))&(((~(aElementOf0(X5,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X5))&(aFunction0(sdtlpdtrp0(xC,X4))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))))&szDzozmdt0(sdtlpdtrp0(xC,X4))=slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))),xk)))|~(epred2_1(X4))),inference(shift_quantors,[status(thm)],[4706])).
% fof(4708, plain,![X4]:![X5]:![X6]:![X7]:![X8]:![X10]:![X11]:![X12]:![X14]:![X15]:(((((((((((((((aElement0(X12)|~(aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(aSet0(X10)))|(aElement0(X15)|~(aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))|~(epred2_1(X4)))&((((aElementOf0(X12,sdtlpdtrp0(xN,X4))|~(aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(aSet0(X10)))|(aElement0(X15)|~(aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))|~(epred2_1(X4))))&((((~(X12=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(aSet0(X10)))|(aElement0(X15)|~(aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))|~(epred2_1(X4))))&((((((~(aElement0(X12))|~(aElementOf0(X12,sdtlpdtrp0(xN,X4))))|X12=szmzizndt0(sdtlpdtrp0(xN,X4)))|aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(aSet0(X10)))|(aElement0(X15)|~(aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))|~(epred2_1(X4))))&(((aSet0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))|~(aSet0(X10)))|(aElement0(X15)|~(aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))|~(epred2_1(X4))))&(((((((aElementOf0(esk36_2(X4,X10),X10)|~(sbrdtbr0(X10)=xk))|~(aSet0(X10)))|(aElement0(X15)|~(aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))|~(epred2_1(X4)))&((((~(aElementOf0(esk36_2(X4,X10),sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(sbrdtbr0(X10)=xk))|~(aSet0(X10)))|(aElement0(X15)|~(aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))|~(epred2_1(X4))))&((((~(aSubsetOf0(X10,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(sbrdtbr0(X10)=xk))|~(aSet0(X10)))|(aElement0(X15)|~(aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))|~(epred2_1(X4))))&(((~(aElementOf0(X10,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))),xk)))|~(aSet0(X10)))|(aElement0(X15)|~(aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))|~(epred2_1(X4)))))&(((((~(aElementOf0(X11,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X11))|~(aSet0(X10)))|(aElement0(X15)|~(aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))|~(epred2_1(X4)))&(((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4))|~(aSet0(X10)))|(aElement0(X15)|~(aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))|~(epred2_1(X4)))))&((((((((((aElement0(X12)|~(aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(aSet0(X10)))|((aElementOf0(X15,X10)|X15=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))|~(epred2_1(X4)))&((((aElementOf0(X12,sdtlpdtrp0(xN,X4))|~(aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(aSet0(X10)))|((aElementOf0(X15,X10)|X15=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))|~(epred2_1(X4))))&((((~(X12=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(aSet0(X10)))|((aElementOf0(X15,X10)|X15=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))|~(epred2_1(X4))))&((((((~(aElement0(X12))|~(aElementOf0(X12,sdtlpdtrp0(xN,X4))))|X12=szmzizndt0(sdtlpdtrp0(xN,X4)))|aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(aSet0(X10)))|((aElementOf0(X15,X10)|X15=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))|~(epred2_1(X4))))&(((aSet0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))|~(aSet0(X10)))|((aElementOf0(X15,X10)|X15=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))|~(epred2_1(X4))))&(((((((aElementOf0(esk36_2(X4,X10),X10)|~(sbrdtbr0(X10)=xk))|~(aSet0(X10)))|((aElementOf0(X15,X10)|X15=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))|~(epred2_1(X4)))&((((~(aElementOf0(esk36_2(X4,X10),sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(sbrdtbr0(X10)=xk))|~(aSet0(X10)))|((aElementOf0(X15,X10)|X15=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))|~(epred2_1(X4))))&((((~(aSubsetOf0(X10,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(sbrdtbr0(X10)=xk))|~(aSet0(X10)))|((aElementOf0(X15,X10)|X15=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))|~(epred2_1(X4))))&(((~(aElementOf0(X10,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))),xk)))|~(aSet0(X10)))|((aElementOf0(X15,X10)|X15=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))|~(epred2_1(X4)))))&(((((~(aElementOf0(X11,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X11))|~(aSet0(X10)))|((aElementOf0(X15,X10)|X15=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))|~(epred2_1(X4)))&(((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4))|~(aSet0(X10)))|((aElementOf0(X15,X10)|X15=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))))|~(epred2_1(X4))))))&(((((((((((aElement0(X12)|~(aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(aSet0(X10)))|((~(aElementOf0(X15,X10))|~(aElement0(X15)))|aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(epred2_1(X4)))&((((aElementOf0(X12,sdtlpdtrp0(xN,X4))|~(aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(aSet0(X10)))|((~(aElementOf0(X15,X10))|~(aElement0(X15)))|aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(epred2_1(X4))))&((((~(X12=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(aSet0(X10)))|((~(aElementOf0(X15,X10))|~(aElement0(X15)))|aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(epred2_1(X4))))&((((((~(aElement0(X12))|~(aElementOf0(X12,sdtlpdtrp0(xN,X4))))|X12=szmzizndt0(sdtlpdtrp0(xN,X4)))|aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(aSet0(X10)))|((~(aElementOf0(X15,X10))|~(aElement0(X15)))|aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(epred2_1(X4))))&(((aSet0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))|~(aSet0(X10)))|((~(aElementOf0(X15,X10))|~(aElement0(X15)))|aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(epred2_1(X4))))&(((((((aElementOf0(esk36_2(X4,X10),X10)|~(sbrdtbr0(X10)=xk))|~(aSet0(X10)))|((~(aElementOf0(X15,X10))|~(aElement0(X15)))|aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(epred2_1(X4)))&((((~(aElementOf0(esk36_2(X4,X10),sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(sbrdtbr0(X10)=xk))|~(aSet0(X10)))|((~(aElementOf0(X15,X10))|~(aElement0(X15)))|aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(epred2_1(X4))))&((((~(aSubsetOf0(X10,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(sbrdtbr0(X10)=xk))|~(aSet0(X10)))|((~(aElementOf0(X15,X10))|~(aElement0(X15)))|aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(epred2_1(X4))))&(((~(aElementOf0(X10,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))),xk)))|~(aSet0(X10)))|((~(aElementOf0(X15,X10))|~(aElement0(X15)))|aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(epred2_1(X4)))))&(((((~(aElementOf0(X11,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X11))|~(aSet0(X10)))|((~(aElementOf0(X15,X10))|~(aElement0(X15)))|aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(epred2_1(X4)))&(((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4))|~(aSet0(X10)))|((~(aElementOf0(X15,X10))|~(aElement0(X15)))|aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(epred2_1(X4)))))&((((((((((aElement0(X12)|~(aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(aSet0(X10)))|((~(X15=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElement0(X15)))|aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(epred2_1(X4)))&((((aElementOf0(X12,sdtlpdtrp0(xN,X4))|~(aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(aSet0(X10)))|((~(X15=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElement0(X15)))|aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(epred2_1(X4))))&((((~(X12=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(aSet0(X10)))|((~(X15=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElement0(X15)))|aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(epred2_1(X4))))&((((((~(aElement0(X12))|~(aElementOf0(X12,sdtlpdtrp0(xN,X4))))|X12=szmzizndt0(sdtlpdtrp0(xN,X4)))|aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(aSet0(X10)))|((~(X15=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElement0(X15)))|aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(epred2_1(X4))))&(((aSet0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))|~(aSet0(X10)))|((~(X15=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElement0(X15)))|aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(epred2_1(X4))))&(((((((aElementOf0(esk36_2(X4,X10),X10)|~(sbrdtbr0(X10)=xk))|~(aSet0(X10)))|((~(X15=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElement0(X15)))|aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(epred2_1(X4)))&((((~(aElementOf0(esk36_2(X4,X10),sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(sbrdtbr0(X10)=xk))|~(aSet0(X10)))|((~(X15=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElement0(X15)))|aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(epred2_1(X4))))&((((~(aSubsetOf0(X10,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(sbrdtbr0(X10)=xk))|~(aSet0(X10)))|((~(X15=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElement0(X15)))|aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(epred2_1(X4))))&(((~(aElementOf0(X10,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))),xk)))|~(aSet0(X10)))|((~(X15=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElement0(X15)))|aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(epred2_1(X4)))))&(((((~(aElementOf0(X11,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X11))|~(aSet0(X10)))|((~(X15=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElement0(X15)))|aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(epred2_1(X4)))&(((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4))|~(aSet0(X10)))|((~(X15=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElement0(X15)))|aElementOf0(X15,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(epred2_1(X4)))))))&(((((((((((aElement0(X12)|~(aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(aSet0(X10)))|(~(aElementOf0(X14,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X14)))|~(epred2_1(X4)))&((((aElementOf0(X12,sdtlpdtrp0(xN,X4))|~(aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(aSet0(X10)))|(~(aElementOf0(X14,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X14)))|~(epred2_1(X4))))&((((~(X12=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(aSet0(X10)))|(~(aElementOf0(X14,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X14)))|~(epred2_1(X4))))&((((((~(aElement0(X12))|~(aElementOf0(X12,sdtlpdtrp0(xN,X4))))|X12=szmzizndt0(sdtlpdtrp0(xN,X4)))|aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(aSet0(X10)))|(~(aElementOf0(X14,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X14)))|~(epred2_1(X4))))&(((aSet0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))|~(aSet0(X10)))|(~(aElementOf0(X14,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X14)))|~(epred2_1(X4))))&(((((((aElementOf0(esk36_2(X4,X10),X10)|~(sbrdtbr0(X10)=xk))|~(aSet0(X10)))|(~(aElementOf0(X14,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X14)))|~(epred2_1(X4)))&((((~(aElementOf0(esk36_2(X4,X10),sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(sbrdtbr0(X10)=xk))|~(aSet0(X10)))|(~(aElementOf0(X14,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X14)))|~(epred2_1(X4))))&((((~(aSubsetOf0(X10,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(sbrdtbr0(X10)=xk))|~(aSet0(X10)))|(~(aElementOf0(X14,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X14)))|~(epred2_1(X4))))&(((~(aElementOf0(X10,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))),xk)))|~(aSet0(X10)))|(~(aElementOf0(X14,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X14)))|~(epred2_1(X4)))))&(((((~(aElementOf0(X11,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X11))|~(aSet0(X10)))|(~(aElementOf0(X14,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X14)))|~(epred2_1(X4)))&(((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4))|~(aSet0(X10)))|(~(aElementOf0(X14,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X14)))|~(epred2_1(X4)))))&((((((((((aElement0(X12)|~(aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(aSet0(X10)))|aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4)))|~(epred2_1(X4)))&((((aElementOf0(X12,sdtlpdtrp0(xN,X4))|~(aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(aSet0(X10)))|aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4)))|~(epred2_1(X4))))&((((~(X12=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(aSet0(X10)))|aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4)))|~(epred2_1(X4))))&((((((~(aElement0(X12))|~(aElementOf0(X12,sdtlpdtrp0(xN,X4))))|X12=szmzizndt0(sdtlpdtrp0(xN,X4)))|aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(aSet0(X10)))|aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4)))|~(epred2_1(X4))))&(((aSet0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))|~(aSet0(X10)))|aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4)))|~(epred2_1(X4))))&(((((((aElementOf0(esk36_2(X4,X10),X10)|~(sbrdtbr0(X10)=xk))|~(aSet0(X10)))|aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4)))|~(epred2_1(X4)))&((((~(aElementOf0(esk36_2(X4,X10),sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(sbrdtbr0(X10)=xk))|~(aSet0(X10)))|aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4)))|~(epred2_1(X4))))&((((~(aSubsetOf0(X10,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(sbrdtbr0(X10)=xk))|~(aSet0(X10)))|aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4)))|~(epred2_1(X4))))&(((~(aElementOf0(X10,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))),xk)))|~(aSet0(X10)))|aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4)))|~(epred2_1(X4)))))&(((((~(aElementOf0(X11,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X11))|~(aSet0(X10)))|aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4)))|~(epred2_1(X4)))&(((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4))|~(aSet0(X10)))|aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4)))|~(epred2_1(X4)))))))&((((((((((aElement0(X12)|~(aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(aSet0(X10)))|sdtlpdtrp0(sdtlpdtrp0(xC,X4),X10)=sdtlpdtrp0(xc,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(epred2_1(X4)))&((((aElementOf0(X12,sdtlpdtrp0(xN,X4))|~(aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(aSet0(X10)))|sdtlpdtrp0(sdtlpdtrp0(xC,X4),X10)=sdtlpdtrp0(xc,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(epred2_1(X4))))&((((~(X12=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(aSet0(X10)))|sdtlpdtrp0(sdtlpdtrp0(xC,X4),X10)=sdtlpdtrp0(xc,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(epred2_1(X4))))&((((((~(aElement0(X12))|~(aElementOf0(X12,sdtlpdtrp0(xN,X4))))|X12=szmzizndt0(sdtlpdtrp0(xN,X4)))|aElementOf0(X12,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(aSet0(X10)))|sdtlpdtrp0(sdtlpdtrp0(xC,X4),X10)=sdtlpdtrp0(xc,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(epred2_1(X4))))&(((aSet0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))|~(aSet0(X10)))|sdtlpdtrp0(sdtlpdtrp0(xC,X4),X10)=sdtlpdtrp0(xc,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(epred2_1(X4))))&(((((((aElementOf0(esk36_2(X4,X10),X10)|~(sbrdtbr0(X10)=xk))|~(aSet0(X10)))|sdtlpdtrp0(sdtlpdtrp0(xC,X4),X10)=sdtlpdtrp0(xc,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(epred2_1(X4)))&((((~(aElementOf0(esk36_2(X4,X10),sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(sbrdtbr0(X10)=xk))|~(aSet0(X10)))|sdtlpdtrp0(sdtlpdtrp0(xC,X4),X10)=sdtlpdtrp0(xc,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(epred2_1(X4))))&((((~(aSubsetOf0(X10,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(sbrdtbr0(X10)=xk))|~(aSet0(X10)))|sdtlpdtrp0(sdtlpdtrp0(xC,X4),X10)=sdtlpdtrp0(xc,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(epred2_1(X4))))&(((~(aElementOf0(X10,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))),xk)))|~(aSet0(X10)))|sdtlpdtrp0(sdtlpdtrp0(xC,X4),X10)=sdtlpdtrp0(xc,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(epred2_1(X4)))))&(((((~(aElementOf0(X11,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X11))|~(aSet0(X10)))|sdtlpdtrp0(sdtlpdtrp0(xC,X4),X10)=sdtlpdtrp0(xc,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(epred2_1(X4)))&(((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4))|~(aSet0(X10)))|sdtlpdtrp0(sdtlpdtrp0(xC,X4),X10)=sdtlpdtrp0(xc,sdtpldt0(X10,szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(epred2_1(X4))))))&(((((((((~(aElementOf0(X8,X7))|aElementOf0(X8,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(aElementOf0(X7,szDzozmdt0(sdtlpdtrp0(xC,X4)))))|~(epred2_1(X4)))&((aSet0(X7)|~(aElementOf0(X7,szDzozmdt0(sdtlpdtrp0(xC,X4)))))|~(epred2_1(X4))))&((aSubsetOf0(X7,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))|~(aElementOf0(X7,szDzozmdt0(sdtlpdtrp0(xC,X4)))))|~(epred2_1(X4))))&((sbrdtbr0(X7)=xk|~(aElementOf0(X7,szDzozmdt0(sdtlpdtrp0(xC,X4)))))|~(epred2_1(X4))))&((((((aElementOf0(esk35_2(X4,X7),X7)|~(aSet0(X7)))|~(sbrdtbr0(X7)=xk))|aElementOf0(X7,szDzozmdt0(sdtlpdtrp0(xC,X4))))|~(epred2_1(X4)))&((((~(aElementOf0(esk35_2(X4,X7),sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(aSet0(X7)))|~(sbrdtbr0(X7)=xk))|aElementOf0(X7,szDzozmdt0(sdtlpdtrp0(xC,X4))))|~(epred2_1(X4))))&(((~(aSubsetOf0(X7,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(sbrdtbr0(X7)=xk))|aElementOf0(X7,szDzozmdt0(sdtlpdtrp0(xC,X4))))|~(epred2_1(X4)))))&((((((aElement0(X6)|~(aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(epred2_1(X4)))&((aElementOf0(X6,sdtlpdtrp0(xN,X4))|~(aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(epred2_1(X4))))&((~(X6=szmzizndt0(sdtlpdtrp0(xN,X4)))|~(aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))))|~(epred2_1(X4))))&((((~(aElement0(X6))|~(aElementOf0(X6,sdtlpdtrp0(xN,X4))))|X6=szmzizndt0(sdtlpdtrp0(xN,X4)))|aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4)))))|~(epred2_1(X4))))&((((~(aElementOf0(X5,sdtlpdtrp0(xN,X4)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X4)),X5))|~(epred2_1(X4)))&((aFunction0(sdtlpdtrp0(xC,X4))|~(epred2_1(X4)))&(aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X4)),sdtlpdtrp0(xN,X4))|~(epred2_1(X4)))))&(aSet0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))))|~(epred2_1(X4))))))&(szDzozmdt0(sdtlpdtrp0(xC,X4))=slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X4),szmzizndt0(sdtlpdtrp0(xN,X4))),xk)|~(epred2_1(X4))))),inference(distribute,[status(thm)],[4707])).
% cnf(4727,plain,(sdtlpdtrp0(sdtlpdtrp0(xC,X1),X2)=sdtlpdtrp0(xc,sdtpldt0(X2,szmzizndt0(sdtlpdtrp0(xN,X1))))|~epred2_1(X1)|~aSet0(X2)|~aElementOf0(X2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))),xk))),inference(split_conjunct,[status(thm)],[4708])).
% cnf(11087,plain,(sdtlpdtrp0(xc,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))=sdtlpdtrp0(sdtlpdtrp0(xC,xi),xQ)|~epred2_1(xi)|~aSet0(xQ)),inference(spm,[status(thm)],[4727,4418,theory(equality)])).
% cnf(11100,plain,(sdtlpdtrp0(xc,esk26_0)=sdtlpdtrp0(sdtlpdtrp0(xC,xi),xQ)|~epred2_1(xi)|~aSet0(xQ)),inference(rw,[status(thm)],[11087,4435,theory(equality)])).
% cnf(11101,plain,(sdtlpdtrp0(xc,esk26_0)=xx|~epred2_1(xi)|~aSet0(xQ)),inference(rw,[status(thm)],[11100,4417,theory(equality)])).
% cnf(11102,plain,(sdtlpdtrp0(xc,esk26_0)=xx|~epred2_1(xi)|$false),inference(rw,[status(thm)],[11101,4421,theory(equality)])).
% cnf(11103,plain,(sdtlpdtrp0(xc,esk26_0)=xx|~epred2_1(xi)),inference(cn,[status(thm)],[11102,theory(equality)])).
% cnf(72950,plain,(sdtlpdtrp0(xc,esk26_0)=xx|~aElementOf0(xi,szNzAzT0)),inference(spm,[status(thm)],[11103,4406,theory(equality)])).
% cnf(72951,plain,(sdtlpdtrp0(xc,esk26_0)=xx|$false),inference(rw,[status(thm)],[72950,4407,theory(equality)])).
% cnf(72952,plain,(sdtlpdtrp0(xc,esk26_0)=xx),inference(cn,[status(thm)],[72951,theory(equality)])).
% cnf(72953,plain,(aElementOf0(xx,sdtlcdtrc0(xc,szDzozmdt0(xc)))|~aFunction0(xc)|~aElementOf0(esk26_0,szDzozmdt0(xc))),inference(spm,[status(thm)],[315,72952,theory(equality)])).
% cnf(72957,plain,(aElementOf0(xx,sdtlcdtrc0(xc,szDzozmdt0(xc)))|$false|~aElementOf0(esk26_0,szDzozmdt0(xc))),inference(rw,[status(thm)],[72953,343,theory(equality)])).
% cnf(72958,plain,(aElementOf0(xx,sdtlcdtrc0(xc,szDzozmdt0(xc)))|$false|$false),inference(rw,[status(thm)],[72957,4436,theory(equality)])).
% cnf(72959,plain,(aElementOf0(xx,sdtlcdtrc0(xc,szDzozmdt0(xc)))),inference(cn,[status(thm)],[72958,theory(equality)])).
% cnf(75138,plain,(aElementOf0(xx,xT)),inference(spm,[status(thm)],[354,72959,theory(equality)])).
% cnf(75804,plain,($false),inference(sr,[status(thm)],[75138,4577,theory(equality)])).
% cnf(75805,plain,($false),75804,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 6136
% # ...of these trivial : 14
% # ...subsumed : 471
% # ...remaining for further processing: 5651
% # Other redundant clauses eliminated : 13
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 7
% # Backward-rewritten : 10
% # Generated clauses : 56911
% # ...of the previous two non-trivial : 45626
% # Contextual simplify-reflections : 2805
% # Paramodulations : 56868
% # Factorizations : 0
% # Equation resolutions : 43
% # Current number of processed clauses: 2886
% # Positive orientable unit clauses: 77
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 31
% # Non-unit-clauses : 2778
% # Current number of unprocessed clauses: 45294
% # ...number of literals in the above : 707889
% # Clause-clause subsumption calls (NU) : 958525
% # Rec. Clause-clause subsumption calls : 41802
% # Unit Clause-clause subsumption calls : 41604
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 5
% # Indexed BW rewrite successes : 5
% # Backwards rewriting index: 396 leaves, 1.96+/-2.333 terms/leaf
% # Paramod-from index: 189 leaves, 1.04+/-0.215 terms/leaf
% # Paramod-into index: 354 leaves, 1.45+/-1.275 terms/leaf
% # -------------------------------------------------
% # User time : 8.868 s
% # System time : 0.183 s
% # Total time : 9.051 s
% # Maximum resident set size: 0 pages
% PrfWatch: 12.07 CPU 12.23 WC
% FINAL PrfWatch: 12.07 CPU 12.23 WC
% SZS output end Solution for /tmp/SystemOnTPTP6371/NUM587+3.tptp
%
%------------------------------------------------------------------------------