%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NUM601+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 : art09.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:34:31 EST 2010
% Result : Theorem 15.65s
% Output : Solution 15.65s
% 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/SystemOnTPTP21525/NUM601+3.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP21525/NUM601+3.tptp
% SZS output start Solution for /tmp/SystemOnTPTP21525/NUM601+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 21621
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% PrfWatch: 1.94 CPU 2.01 WC
% PrfWatch: 3.93 CPU 4.02 WC
% PrfWatch: 5.92 CPU 6.02 WC
% PrfWatch: 7.91 CPU 8.03 WC
% PrfWatch: 9.91 CPU 10.03 WC
% # Preprocessing time : 0.612 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 11.90 CPU 12.04 WC
% PrfWatch: 13.89 CPU 14.04 WC
% # SZS output start CNFRefutation.
% fof(3, axiom,![X1]:(aSet0(X1)=>![X2]:(aSubsetOf0(X2,X1)<=>(aSet0(X2)&![X3]:(aElementOf0(X3,X2)=>aElementOf0(X3,X1))))),file('/tmp/SRASS.s.p', mDefSub)).
% fof(17, axiom,aElementOf0(sz00,szNzAzT0),file('/tmp/SRASS.s.p', mZeroNum)).
% fof(22, axiom,![X1]:(aElementOf0(X1,szNzAzT0)=>sdtlseqdt0(sz00,X1)),file('/tmp/SRASS.s.p', mZeroLess)).
% fof(51, axiom,(((aSet0(xS)&![X1]:(aElementOf0(X1,xS)=>aElementOf0(X1,szNzAzT0)))&aSubsetOf0(xS,szNzAzT0))&isCountable0(xS)),file('/tmp/SRASS.s.p', m__3435)).
% fof(57, axiom,(((aFunction0(xN)&szDzozmdt0(xN)=szNzAzT0)&sdtlpdtrp0(xN,sz00)=xS)&![X1]:(aElementOf0(X1,szNzAzT0)=>((((aSet0(sdtlpdtrp0(xN,X1))&![X2]:(aElementOf0(X2,sdtlpdtrp0(xN,X1))=>aElementOf0(X2,szNzAzT0)))|aSubsetOf0(sdtlpdtrp0(xN,X1),szNzAzT0))&isCountable0(sdtlpdtrp0(xN,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))))))&aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X1))))&![X2]:(aElementOf0(X2,sdtlpdtrp0(xN,szszuzczcdt0(X1)))=>aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))))&aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X1)),sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))))&isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X1))))))),file('/tmp/SRASS.s.p', m__3623)).
% fof(58, axiom,![X1]:(aElementOf0(X1,szNzAzT0)=>(((aSet0(sdtlpdtrp0(xN,X1))&![X2]:(aElementOf0(X2,sdtlpdtrp0(xN,X1))=>aElementOf0(X2,szNzAzT0)))&aSubsetOf0(sdtlpdtrp0(xN,X1),szNzAzT0))&isCountable0(sdtlpdtrp0(xN,X1)))),file('/tmp/SRASS.s.p', m__3671)).
% fof(59, axiom,![X1]:![X2]:((aElementOf0(X1,szNzAzT0)&aElementOf0(X2,szNzAzT0))=>(sdtlseqdt0(X2,X1)=>(![X3]:(aElementOf0(X3,sdtlpdtrp0(xN,X1))=>aElementOf0(X3,sdtlpdtrp0(xN,X2)))&aSubsetOf0(sdtlpdtrp0(xN,X1),sdtlpdtrp0(xN,X2))))),file('/tmp/SRASS.s.p', m__3754)).
% fof(67, axiom,((aFunction0(xe)&szDzozmdt0(xe)=szNzAzT0)&![X1]:(aElementOf0(X1,szNzAzT0)=>((aElementOf0(sdtlpdtrp0(xe,X1),sdtlpdtrp0(xN,X1))&![X2]:(aElementOf0(X2,sdtlpdtrp0(xN,X1))=>sdtlseqdt0(sdtlpdtrp0(xe,X1),X2)))&sdtlpdtrp0(xe,X1)=szmzizndt0(sdtlpdtrp0(xN,X1))))),file('/tmp/SRASS.s.p', m__4660)).
% fof(73, axiom,![X1]:((?[X2]:(aElementOf0(X2,sdtlbdtrb0(xd,szDzizrdt0(xd)))&sdtlpdtrp0(xe,X2)=X1)|aElementOf0(X1,xO))=>?[X2]:(((aElementOf0(X2,szNzAzT0)&sdtlpdtrp0(xd,X2)=szDzizrdt0(xd))&aElementOf0(X2,sdtlbdtrb0(xd,szDzizrdt0(xd))))&sdtlpdtrp0(xe,X2)=X1)),file('/tmp/SRASS.s.p', m__4982)).
% fof(75, axiom,![X1]:((aSubsetOf0(X1,szNzAzT0)&~(X1=slcrc0))=>![X2]:(X2=szmzizndt0(X1)<=>(aElementOf0(X2,X1)&![X3]:(aElementOf0(X3,X1)=>sdtlseqdt0(X2,X3))))),file('/tmp/SRASS.s.p', mDefMin)).
% fof(85, axiom,![X1]:((aSet0(X1)&isCountable0(X1))=>~(X1=slcrc0)),file('/tmp/SRASS.s.p', mCountNFin_01)).
% fof(90, axiom,![X1]:(X1=slcrc0<=>(aSet0(X1)&~(?[X2]:aElementOf0(X2,X1)))),file('/tmp/SRASS.s.p', mDefEmp)).
% fof(98, conjecture,(![X1]:(aElementOf0(X1,xO)=>aElementOf0(X1,xS))|aSubsetOf0(xO,xS)),file('/tmp/SRASS.s.p', m__)).
% fof(99, negated_conjecture,~((![X1]:(aElementOf0(X1,xO)=>aElementOf0(X1,xS))|aSubsetOf0(xO,xS))),inference(assume_negation,[status(cth)],[98])).
% fof(127, plain,![X1]:(~(aSet0(X1))|![X2]:((~(aSubsetOf0(X2,X1))|(aSet0(X2)&![X3]:(~(aElementOf0(X3,X2))|aElementOf0(X3,X1))))&((~(aSet0(X2))|?[X3]:(aElementOf0(X3,X2)&~(aElementOf0(X3,X1))))|aSubsetOf0(X2,X1)))),inference(fof_nnf,[status(thm)],[3])).
% fof(128, plain,![X4]:(~(aSet0(X4))|![X5]:((~(aSubsetOf0(X5,X4))|(aSet0(X5)&![X6]:(~(aElementOf0(X6,X5))|aElementOf0(X6,X4))))&((~(aSet0(X5))|?[X7]:(aElementOf0(X7,X5)&~(aElementOf0(X7,X4))))|aSubsetOf0(X5,X4)))),inference(variable_rename,[status(thm)],[127])).
% fof(129, plain,![X4]:(~(aSet0(X4))|![X5]:((~(aSubsetOf0(X5,X4))|(aSet0(X5)&![X6]:(~(aElementOf0(X6,X5))|aElementOf0(X6,X4))))&((~(aSet0(X5))|(aElementOf0(esk1_2(X4,X5),X5)&~(aElementOf0(esk1_2(X4,X5),X4))))|aSubsetOf0(X5,X4)))),inference(skolemize,[status(esa)],[128])).
% fof(130, plain,![X4]:![X5]:![X6]:(((((~(aElementOf0(X6,X5))|aElementOf0(X6,X4))&aSet0(X5))|~(aSubsetOf0(X5,X4)))&((~(aSet0(X5))|(aElementOf0(esk1_2(X4,X5),X5)&~(aElementOf0(esk1_2(X4,X5),X4))))|aSubsetOf0(X5,X4)))|~(aSet0(X4))),inference(shift_quantors,[status(thm)],[129])).
% fof(131, plain,![X4]:![X5]:![X6]:(((((~(aElementOf0(X6,X5))|aElementOf0(X6,X4))|~(aSubsetOf0(X5,X4)))|~(aSet0(X4)))&((aSet0(X5)|~(aSubsetOf0(X5,X4)))|~(aSet0(X4))))&((((aElementOf0(esk1_2(X4,X5),X5)|~(aSet0(X5)))|aSubsetOf0(X5,X4))|~(aSet0(X4)))&(((~(aElementOf0(esk1_2(X4,X5),X4))|~(aSet0(X5)))|aSubsetOf0(X5,X4))|~(aSet0(X4))))),inference(distribute,[status(thm)],[130])).
% cnf(135,plain,(aElementOf0(X3,X1)|~aSet0(X1)|~aSubsetOf0(X2,X1)|~aElementOf0(X3,X2)),inference(split_conjunct,[status(thm)],[131])).
% cnf(202,plain,(aElementOf0(sz00,szNzAzT0)),inference(split_conjunct,[status(thm)],[17])).
% fof(220, plain,![X1]:(~(aElementOf0(X1,szNzAzT0))|sdtlseqdt0(sz00,X1)),inference(fof_nnf,[status(thm)],[22])).
% fof(221, plain,![X2]:(~(aElementOf0(X2,szNzAzT0))|sdtlseqdt0(sz00,X2)),inference(variable_rename,[status(thm)],[220])).
% cnf(222,plain,(sdtlseqdt0(sz00,X1)|~aElementOf0(X1,szNzAzT0)),inference(split_conjunct,[status(thm)],[221])).
% fof(358, plain,(((aSet0(xS)&![X1]:(~(aElementOf0(X1,xS))|aElementOf0(X1,szNzAzT0)))&aSubsetOf0(xS,szNzAzT0))&isCountable0(xS)),inference(fof_nnf,[status(thm)],[51])).
% fof(359, plain,(((aSet0(xS)&![X2]:(~(aElementOf0(X2,xS))|aElementOf0(X2,szNzAzT0)))&aSubsetOf0(xS,szNzAzT0))&isCountable0(xS)),inference(variable_rename,[status(thm)],[358])).
% fof(360, plain,![X2]:((((~(aElementOf0(X2,xS))|aElementOf0(X2,szNzAzT0))&aSet0(xS))&aSubsetOf0(xS,szNzAzT0))&isCountable0(xS)),inference(shift_quantors,[status(thm)],[359])).
% cnf(363,plain,(aSet0(xS)),inference(split_conjunct,[status(thm)],[360])).
% fof(4363, plain,(((aFunction0(xN)&szDzozmdt0(xN)=szNzAzT0)&sdtlpdtrp0(xN,sz00)=xS)&![X1]:(~(aElementOf0(X1,szNzAzT0))|((((~(aSet0(sdtlpdtrp0(xN,X1)))|?[X2]:(aElementOf0(X2,sdtlpdtrp0(xN,X1))&~(aElementOf0(X2,szNzAzT0))))&~(aSubsetOf0(sdtlpdtrp0(xN,X1),szNzAzT0)))|~(isCountable0(sdtlpdtrp0(xN,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)))))))&aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X1))))&![X2]:(~(aElementOf0(X2,sdtlpdtrp0(xN,szszuzczcdt0(X1))))|aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))))&aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X1)),sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))))&isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X1))))))),inference(fof_nnf,[status(thm)],[57])).
% fof(4364, plain,(((aFunction0(xN)&szDzozmdt0(xN)=szNzAzT0)&sdtlpdtrp0(xN,sz00)=xS)&![X3]:(~(aElementOf0(X3,szNzAzT0))|((((~(aSet0(sdtlpdtrp0(xN,X3)))|?[X4]:(aElementOf0(X4,sdtlpdtrp0(xN,X3))&~(aElementOf0(X4,szNzAzT0))))&~(aSubsetOf0(sdtlpdtrp0(xN,X3),szNzAzT0)))|~(isCountable0(sdtlpdtrp0(xN,X3))))|(((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X3)),sdtlpdtrp0(xN,X3))&![X5]:(~(aElementOf0(X5,sdtlpdtrp0(xN,X3)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X3)),X5)))&aSet0(sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))&![X6]:((~(aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))|((aElement0(X6)&aElementOf0(X6,sdtlpdtrp0(xN,X3)))&~(X6=szmzizndt0(sdtlpdtrp0(xN,X3)))))&(((~(aElement0(X6))|~(aElementOf0(X6,sdtlpdtrp0(xN,X3))))|X6=szmzizndt0(sdtlpdtrp0(xN,X3)))|aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))))&aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X3))))&![X7]:(~(aElementOf0(X7,sdtlpdtrp0(xN,szszuzczcdt0(X3))))|aElementOf0(X7,sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3))))))&aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X3)),sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))&isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X3))))))),inference(variable_rename,[status(thm)],[4363])).
% fof(4365, plain,(((aFunction0(xN)&szDzozmdt0(xN)=szNzAzT0)&sdtlpdtrp0(xN,sz00)=xS)&![X3]:(~(aElementOf0(X3,szNzAzT0))|((((~(aSet0(sdtlpdtrp0(xN,X3)))|(aElementOf0(esk24_1(X3),sdtlpdtrp0(xN,X3))&~(aElementOf0(esk24_1(X3),szNzAzT0))))&~(aSubsetOf0(sdtlpdtrp0(xN,X3),szNzAzT0)))|~(isCountable0(sdtlpdtrp0(xN,X3))))|(((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X3)),sdtlpdtrp0(xN,X3))&![X5]:(~(aElementOf0(X5,sdtlpdtrp0(xN,X3)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X3)),X5)))&aSet0(sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))&![X6]:((~(aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))|((aElement0(X6)&aElementOf0(X6,sdtlpdtrp0(xN,X3)))&~(X6=szmzizndt0(sdtlpdtrp0(xN,X3)))))&(((~(aElement0(X6))|~(aElementOf0(X6,sdtlpdtrp0(xN,X3))))|X6=szmzizndt0(sdtlpdtrp0(xN,X3)))|aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))))&aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X3))))&![X7]:(~(aElementOf0(X7,sdtlpdtrp0(xN,szszuzczcdt0(X3))))|aElementOf0(X7,sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3))))))&aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X3)),sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))&isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X3))))))),inference(skolemize,[status(esa)],[4364])).
% fof(4366, plain,![X3]:![X5]:![X6]:![X7]:(((((((~(aElementOf0(X7,sdtlpdtrp0(xN,szszuzczcdt0(X3))))|aElementOf0(X7,sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))&((((~(aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))|((aElement0(X6)&aElementOf0(X6,sdtlpdtrp0(xN,X3)))&~(X6=szmzizndt0(sdtlpdtrp0(xN,X3)))))&(((~(aElement0(X6))|~(aElementOf0(X6,sdtlpdtrp0(xN,X3))))|X6=szmzizndt0(sdtlpdtrp0(xN,X3)))|aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3))))))&(((~(aElementOf0(X5,sdtlpdtrp0(xN,X3)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X3)),X5))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X3)),sdtlpdtrp0(xN,X3)))&aSet0(sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3))))))&aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X3)))))&aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X3)),sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))&isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X3))))|(((~(aSet0(sdtlpdtrp0(xN,X3)))|(aElementOf0(esk24_1(X3),sdtlpdtrp0(xN,X3))&~(aElementOf0(esk24_1(X3),szNzAzT0))))&~(aSubsetOf0(sdtlpdtrp0(xN,X3),szNzAzT0)))|~(isCountable0(sdtlpdtrp0(xN,X3)))))|~(aElementOf0(X3,szNzAzT0)))&((aFunction0(xN)&szDzozmdt0(xN)=szNzAzT0)&sdtlpdtrp0(xN,sz00)=xS)),inference(shift_quantors,[status(thm)],[4365])).
% fof(4367, plain,![X3]:![X5]:![X6]:![X7]:((((((((((aElementOf0(esk24_1(X3),sdtlpdtrp0(xN,X3))|~(aSet0(sdtlpdtrp0(xN,X3))))|~(isCountable0(sdtlpdtrp0(xN,X3))))|(~(aElementOf0(X7,sdtlpdtrp0(xN,szszuzczcdt0(X3))))|aElementOf0(X7,sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3))))))|~(aElementOf0(X3,szNzAzT0)))&((((~(aElementOf0(esk24_1(X3),szNzAzT0))|~(aSet0(sdtlpdtrp0(xN,X3))))|~(isCountable0(sdtlpdtrp0(xN,X3))))|(~(aElementOf0(X7,sdtlpdtrp0(xN,szszuzczcdt0(X3))))|aElementOf0(X7,sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3))))))|~(aElementOf0(X3,szNzAzT0))))&(((~(aSubsetOf0(sdtlpdtrp0(xN,X3),szNzAzT0))|~(isCountable0(sdtlpdtrp0(xN,X3))))|(~(aElementOf0(X7,sdtlpdtrp0(xN,szszuzczcdt0(X3))))|aElementOf0(X7,sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3))))))|~(aElementOf0(X3,szNzAzT0))))&(((((((((((aElementOf0(esk24_1(X3),sdtlpdtrp0(xN,X3))|~(aSet0(sdtlpdtrp0(xN,X3))))|~(isCountable0(sdtlpdtrp0(xN,X3))))|(aElement0(X6)|~(aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))))|~(aElementOf0(X3,szNzAzT0)))&((((~(aElementOf0(esk24_1(X3),szNzAzT0))|~(aSet0(sdtlpdtrp0(xN,X3))))|~(isCountable0(sdtlpdtrp0(xN,X3))))|(aElement0(X6)|~(aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))))|~(aElementOf0(X3,szNzAzT0))))&(((~(aSubsetOf0(sdtlpdtrp0(xN,X3),szNzAzT0))|~(isCountable0(sdtlpdtrp0(xN,X3))))|(aElement0(X6)|~(aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))))|~(aElementOf0(X3,szNzAzT0))))&((((((aElementOf0(esk24_1(X3),sdtlpdtrp0(xN,X3))|~(aSet0(sdtlpdtrp0(xN,X3))))|~(isCountable0(sdtlpdtrp0(xN,X3))))|(aElementOf0(X6,sdtlpdtrp0(xN,X3))|~(aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))))|~(aElementOf0(X3,szNzAzT0)))&((((~(aElementOf0(esk24_1(X3),szNzAzT0))|~(aSet0(sdtlpdtrp0(xN,X3))))|~(isCountable0(sdtlpdtrp0(xN,X3))))|(aElementOf0(X6,sdtlpdtrp0(xN,X3))|~(aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))))|~(aElementOf0(X3,szNzAzT0))))&(((~(aSubsetOf0(sdtlpdtrp0(xN,X3),szNzAzT0))|~(isCountable0(sdtlpdtrp0(xN,X3))))|(aElementOf0(X6,sdtlpdtrp0(xN,X3))|~(aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))))|~(aElementOf0(X3,szNzAzT0)))))&((((((aElementOf0(esk24_1(X3),sdtlpdtrp0(xN,X3))|~(aSet0(sdtlpdtrp0(xN,X3))))|~(isCountable0(sdtlpdtrp0(xN,X3))))|(~(X6=szmzizndt0(sdtlpdtrp0(xN,X3)))|~(aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))))|~(aElementOf0(X3,szNzAzT0)))&((((~(aElementOf0(esk24_1(X3),szNzAzT0))|~(aSet0(sdtlpdtrp0(xN,X3))))|~(isCountable0(sdtlpdtrp0(xN,X3))))|(~(X6=szmzizndt0(sdtlpdtrp0(xN,X3)))|~(aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))))|~(aElementOf0(X3,szNzAzT0))))&(((~(aSubsetOf0(sdtlpdtrp0(xN,X3),szNzAzT0))|~(isCountable0(sdtlpdtrp0(xN,X3))))|(~(X6=szmzizndt0(sdtlpdtrp0(xN,X3)))|~(aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))))|~(aElementOf0(X3,szNzAzT0)))))&((((((aElementOf0(esk24_1(X3),sdtlpdtrp0(xN,X3))|~(aSet0(sdtlpdtrp0(xN,X3))))|~(isCountable0(sdtlpdtrp0(xN,X3))))|(((~(aElement0(X6))|~(aElementOf0(X6,sdtlpdtrp0(xN,X3))))|X6=szmzizndt0(sdtlpdtrp0(xN,X3)))|aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3))))))|~(aElementOf0(X3,szNzAzT0)))&((((~(aElementOf0(esk24_1(X3),szNzAzT0))|~(aSet0(sdtlpdtrp0(xN,X3))))|~(isCountable0(sdtlpdtrp0(xN,X3))))|(((~(aElement0(X6))|~(aElementOf0(X6,sdtlpdtrp0(xN,X3))))|X6=szmzizndt0(sdtlpdtrp0(xN,X3)))|aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3))))))|~(aElementOf0(X3,szNzAzT0))))&(((~(aSubsetOf0(sdtlpdtrp0(xN,X3),szNzAzT0))|~(isCountable0(sdtlpdtrp0(xN,X3))))|(((~(aElement0(X6))|~(aElementOf0(X6,sdtlpdtrp0(xN,X3))))|X6=szmzizndt0(sdtlpdtrp0(xN,X3)))|aElementOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3))))))|~(aElementOf0(X3,szNzAzT0)))))&((((((((aElementOf0(esk24_1(X3),sdtlpdtrp0(xN,X3))|~(aSet0(sdtlpdtrp0(xN,X3))))|~(isCountable0(sdtlpdtrp0(xN,X3))))|(~(aElementOf0(X5,sdtlpdtrp0(xN,X3)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X3)),X5)))|~(aElementOf0(X3,szNzAzT0)))&((((~(aElementOf0(esk24_1(X3),szNzAzT0))|~(aSet0(sdtlpdtrp0(xN,X3))))|~(isCountable0(sdtlpdtrp0(xN,X3))))|(~(aElementOf0(X5,sdtlpdtrp0(xN,X3)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X3)),X5)))|~(aElementOf0(X3,szNzAzT0))))&(((~(aSubsetOf0(sdtlpdtrp0(xN,X3),szNzAzT0))|~(isCountable0(sdtlpdtrp0(xN,X3))))|(~(aElementOf0(X5,sdtlpdtrp0(xN,X3)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X3)),X5)))|~(aElementOf0(X3,szNzAzT0))))&((((((aElementOf0(esk24_1(X3),sdtlpdtrp0(xN,X3))|~(aSet0(sdtlpdtrp0(xN,X3))))|~(isCountable0(sdtlpdtrp0(xN,X3))))|aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X3)),sdtlpdtrp0(xN,X3)))|~(aElementOf0(X3,szNzAzT0)))&((((~(aElementOf0(esk24_1(X3),szNzAzT0))|~(aSet0(sdtlpdtrp0(xN,X3))))|~(isCountable0(sdtlpdtrp0(xN,X3))))|aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X3)),sdtlpdtrp0(xN,X3)))|~(aElementOf0(X3,szNzAzT0))))&(((~(aSubsetOf0(sdtlpdtrp0(xN,X3),szNzAzT0))|~(isCountable0(sdtlpdtrp0(xN,X3))))|aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X3)),sdtlpdtrp0(xN,X3)))|~(aElementOf0(X3,szNzAzT0)))))&((((((aElementOf0(esk24_1(X3),sdtlpdtrp0(xN,X3))|~(aSet0(sdtlpdtrp0(xN,X3))))|~(isCountable0(sdtlpdtrp0(xN,X3))))|aSet0(sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))|~(aElementOf0(X3,szNzAzT0)))&((((~(aElementOf0(esk24_1(X3),szNzAzT0))|~(aSet0(sdtlpdtrp0(xN,X3))))|~(isCountable0(sdtlpdtrp0(xN,X3))))|aSet0(sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))|~(aElementOf0(X3,szNzAzT0))))&(((~(aSubsetOf0(sdtlpdtrp0(xN,X3),szNzAzT0))|~(isCountable0(sdtlpdtrp0(xN,X3))))|aSet0(sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))|~(aElementOf0(X3,szNzAzT0))))))&((((((aElementOf0(esk24_1(X3),sdtlpdtrp0(xN,X3))|~(aSet0(sdtlpdtrp0(xN,X3))))|~(isCountable0(sdtlpdtrp0(xN,X3))))|aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X3))))|~(aElementOf0(X3,szNzAzT0)))&((((~(aElementOf0(esk24_1(X3),szNzAzT0))|~(aSet0(sdtlpdtrp0(xN,X3))))|~(isCountable0(sdtlpdtrp0(xN,X3))))|aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X3))))|~(aElementOf0(X3,szNzAzT0))))&(((~(aSubsetOf0(sdtlpdtrp0(xN,X3),szNzAzT0))|~(isCountable0(sdtlpdtrp0(xN,X3))))|aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X3))))|~(aElementOf0(X3,szNzAzT0))))))&((((((aElementOf0(esk24_1(X3),sdtlpdtrp0(xN,X3))|~(aSet0(sdtlpdtrp0(xN,X3))))|~(isCountable0(sdtlpdtrp0(xN,X3))))|aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X3)),sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))|~(aElementOf0(X3,szNzAzT0)))&((((~(aElementOf0(esk24_1(X3),szNzAzT0))|~(aSet0(sdtlpdtrp0(xN,X3))))|~(isCountable0(sdtlpdtrp0(xN,X3))))|aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X3)),sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))|~(aElementOf0(X3,szNzAzT0))))&(((~(aSubsetOf0(sdtlpdtrp0(xN,X3),szNzAzT0))|~(isCountable0(sdtlpdtrp0(xN,X3))))|aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X3)),sdtmndt0(sdtlpdtrp0(xN,X3),szmzizndt0(sdtlpdtrp0(xN,X3)))))|~(aElementOf0(X3,szNzAzT0)))))&((((((aElementOf0(esk24_1(X3),sdtlpdtrp0(xN,X3))|~(aSet0(sdtlpdtrp0(xN,X3))))|~(isCountable0(sdtlpdtrp0(xN,X3))))|isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X3))))|~(aElementOf0(X3,szNzAzT0)))&((((~(aElementOf0(esk24_1(X3),szNzAzT0))|~(aSet0(sdtlpdtrp0(xN,X3))))|~(isCountable0(sdtlpdtrp0(xN,X3))))|isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X3))))|~(aElementOf0(X3,szNzAzT0))))&(((~(aSubsetOf0(sdtlpdtrp0(xN,X3),szNzAzT0))|~(isCountable0(sdtlpdtrp0(xN,X3))))|isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X3))))|~(aElementOf0(X3,szNzAzT0)))))&((aFunction0(xN)&szDzozmdt0(xN)=szNzAzT0)&sdtlpdtrp0(xN,sz00)=xS)),inference(distribute,[status(thm)],[4366])).
% cnf(4368,plain,(sdtlpdtrp0(xN,sz00)=xS),inference(split_conjunct,[status(thm)],[4367])).
% fof(4404, plain,![X1]:(~(aElementOf0(X1,szNzAzT0))|(((aSet0(sdtlpdtrp0(xN,X1))&![X2]:(~(aElementOf0(X2,sdtlpdtrp0(xN,X1)))|aElementOf0(X2,szNzAzT0)))&aSubsetOf0(sdtlpdtrp0(xN,X1),szNzAzT0))&isCountable0(sdtlpdtrp0(xN,X1)))),inference(fof_nnf,[status(thm)],[58])).
% fof(4405, plain,![X3]:(~(aElementOf0(X3,szNzAzT0))|(((aSet0(sdtlpdtrp0(xN,X3))&![X4]:(~(aElementOf0(X4,sdtlpdtrp0(xN,X3)))|aElementOf0(X4,szNzAzT0)))&aSubsetOf0(sdtlpdtrp0(xN,X3),szNzAzT0))&isCountable0(sdtlpdtrp0(xN,X3)))),inference(variable_rename,[status(thm)],[4404])).
% fof(4406, plain,![X3]:![X4]:(((((~(aElementOf0(X4,sdtlpdtrp0(xN,X3)))|aElementOf0(X4,szNzAzT0))&aSet0(sdtlpdtrp0(xN,X3)))&aSubsetOf0(sdtlpdtrp0(xN,X3),szNzAzT0))&isCountable0(sdtlpdtrp0(xN,X3)))|~(aElementOf0(X3,szNzAzT0))),inference(shift_quantors,[status(thm)],[4405])).
% fof(4407, plain,![X3]:![X4]:(((((~(aElementOf0(X4,sdtlpdtrp0(xN,X3)))|aElementOf0(X4,szNzAzT0))|~(aElementOf0(X3,szNzAzT0)))&(aSet0(sdtlpdtrp0(xN,X3))|~(aElementOf0(X3,szNzAzT0))))&(aSubsetOf0(sdtlpdtrp0(xN,X3),szNzAzT0)|~(aElementOf0(X3,szNzAzT0))))&(isCountable0(sdtlpdtrp0(xN,X3))|~(aElementOf0(X3,szNzAzT0)))),inference(distribute,[status(thm)],[4406])).
% cnf(4408,plain,(isCountable0(sdtlpdtrp0(xN,X1))|~aElementOf0(X1,szNzAzT0)),inference(split_conjunct,[status(thm)],[4407])).
% cnf(4409,plain,(aSubsetOf0(sdtlpdtrp0(xN,X1),szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(split_conjunct,[status(thm)],[4407])).
% fof(4412, plain,![X1]:![X2]:((~(aElementOf0(X1,szNzAzT0))|~(aElementOf0(X2,szNzAzT0)))|(~(sdtlseqdt0(X2,X1))|(![X3]:(~(aElementOf0(X3,sdtlpdtrp0(xN,X1)))|aElementOf0(X3,sdtlpdtrp0(xN,X2)))&aSubsetOf0(sdtlpdtrp0(xN,X1),sdtlpdtrp0(xN,X2))))),inference(fof_nnf,[status(thm)],[59])).
% fof(4413, plain,![X4]:![X5]:((~(aElementOf0(X4,szNzAzT0))|~(aElementOf0(X5,szNzAzT0)))|(~(sdtlseqdt0(X5,X4))|(![X6]:(~(aElementOf0(X6,sdtlpdtrp0(xN,X4)))|aElementOf0(X6,sdtlpdtrp0(xN,X5)))&aSubsetOf0(sdtlpdtrp0(xN,X4),sdtlpdtrp0(xN,X5))))),inference(variable_rename,[status(thm)],[4412])).
% fof(4414, plain,![X4]:![X5]:![X6]:((((~(aElementOf0(X6,sdtlpdtrp0(xN,X4)))|aElementOf0(X6,sdtlpdtrp0(xN,X5)))&aSubsetOf0(sdtlpdtrp0(xN,X4),sdtlpdtrp0(xN,X5)))|~(sdtlseqdt0(X5,X4)))|(~(aElementOf0(X4,szNzAzT0))|~(aElementOf0(X5,szNzAzT0)))),inference(shift_quantors,[status(thm)],[4413])).
% fof(4415, plain,![X4]:![X5]:![X6]:((((~(aElementOf0(X6,sdtlpdtrp0(xN,X4)))|aElementOf0(X6,sdtlpdtrp0(xN,X5)))|~(sdtlseqdt0(X5,X4)))|(~(aElementOf0(X4,szNzAzT0))|~(aElementOf0(X5,szNzAzT0))))&((aSubsetOf0(sdtlpdtrp0(xN,X4),sdtlpdtrp0(xN,X5))|~(sdtlseqdt0(X5,X4)))|(~(aElementOf0(X4,szNzAzT0))|~(aElementOf0(X5,szNzAzT0))))),inference(distribute,[status(thm)],[4414])).
% cnf(4416,plain,(aSubsetOf0(sdtlpdtrp0(xN,X2),sdtlpdtrp0(xN,X1))|~aElementOf0(X1,szNzAzT0)|~aElementOf0(X2,szNzAzT0)|~sdtlseqdt0(X1,X2)),inference(split_conjunct,[status(thm)],[4415])).
% fof(4464, plain,((aFunction0(xe)&szDzozmdt0(xe)=szNzAzT0)&![X1]:(~(aElementOf0(X1,szNzAzT0))|((aElementOf0(sdtlpdtrp0(xe,X1),sdtlpdtrp0(xN,X1))&![X2]:(~(aElementOf0(X2,sdtlpdtrp0(xN,X1)))|sdtlseqdt0(sdtlpdtrp0(xe,X1),X2)))&sdtlpdtrp0(xe,X1)=szmzizndt0(sdtlpdtrp0(xN,X1))))),inference(fof_nnf,[status(thm)],[67])).
% fof(4465, plain,((aFunction0(xe)&szDzozmdt0(xe)=szNzAzT0)&![X3]:(~(aElementOf0(X3,szNzAzT0))|((aElementOf0(sdtlpdtrp0(xe,X3),sdtlpdtrp0(xN,X3))&![X4]:(~(aElementOf0(X4,sdtlpdtrp0(xN,X3)))|sdtlseqdt0(sdtlpdtrp0(xe,X3),X4)))&sdtlpdtrp0(xe,X3)=szmzizndt0(sdtlpdtrp0(xN,X3))))),inference(variable_rename,[status(thm)],[4464])).
% fof(4466, plain,![X3]:![X4]:(((((~(aElementOf0(X4,sdtlpdtrp0(xN,X3)))|sdtlseqdt0(sdtlpdtrp0(xe,X3),X4))&aElementOf0(sdtlpdtrp0(xe,X3),sdtlpdtrp0(xN,X3)))&sdtlpdtrp0(xe,X3)=szmzizndt0(sdtlpdtrp0(xN,X3)))|~(aElementOf0(X3,szNzAzT0)))&(aFunction0(xe)&szDzozmdt0(xe)=szNzAzT0)),inference(shift_quantors,[status(thm)],[4465])).
% fof(4467, plain,![X3]:![X4]:(((((~(aElementOf0(X4,sdtlpdtrp0(xN,X3)))|sdtlseqdt0(sdtlpdtrp0(xe,X3),X4))|~(aElementOf0(X3,szNzAzT0)))&(aElementOf0(sdtlpdtrp0(xe,X3),sdtlpdtrp0(xN,X3))|~(aElementOf0(X3,szNzAzT0))))&(sdtlpdtrp0(xe,X3)=szmzizndt0(sdtlpdtrp0(xN,X3))|~(aElementOf0(X3,szNzAzT0))))&(aFunction0(xe)&szDzozmdt0(xe)=szNzAzT0)),inference(distribute,[status(thm)],[4466])).
% cnf(4470,plain,(sdtlpdtrp0(xe,X1)=szmzizndt0(sdtlpdtrp0(xN,X1))|~aElementOf0(X1,szNzAzT0)),inference(split_conjunct,[status(thm)],[4467])).
% fof(4520, plain,![X1]:((![X2]:(~(aElementOf0(X2,sdtlbdtrb0(xd,szDzizrdt0(xd))))|~(sdtlpdtrp0(xe,X2)=X1))&~(aElementOf0(X1,xO)))|?[X2]:(((aElementOf0(X2,szNzAzT0)&sdtlpdtrp0(xd,X2)=szDzizrdt0(xd))&aElementOf0(X2,sdtlbdtrb0(xd,szDzizrdt0(xd))))&sdtlpdtrp0(xe,X2)=X1)),inference(fof_nnf,[status(thm)],[73])).
% fof(4521, plain,![X3]:((![X4]:(~(aElementOf0(X4,sdtlbdtrb0(xd,szDzizrdt0(xd))))|~(sdtlpdtrp0(xe,X4)=X3))&~(aElementOf0(X3,xO)))|?[X5]:(((aElementOf0(X5,szNzAzT0)&sdtlpdtrp0(xd,X5)=szDzizrdt0(xd))&aElementOf0(X5,sdtlbdtrb0(xd,szDzizrdt0(xd))))&sdtlpdtrp0(xe,X5)=X3)),inference(variable_rename,[status(thm)],[4520])).
% fof(4522, plain,![X3]:((![X4]:(~(aElementOf0(X4,sdtlbdtrb0(xd,szDzizrdt0(xd))))|~(sdtlpdtrp0(xe,X4)=X3))&~(aElementOf0(X3,xO)))|(((aElementOf0(esk32_1(X3),szNzAzT0)&sdtlpdtrp0(xd,esk32_1(X3))=szDzizrdt0(xd))&aElementOf0(esk32_1(X3),sdtlbdtrb0(xd,szDzizrdt0(xd))))&sdtlpdtrp0(xe,esk32_1(X3))=X3)),inference(skolemize,[status(esa)],[4521])).
% fof(4523, plain,![X3]:![X4]:(((~(aElementOf0(X4,sdtlbdtrb0(xd,szDzizrdt0(xd))))|~(sdtlpdtrp0(xe,X4)=X3))&~(aElementOf0(X3,xO)))|(((aElementOf0(esk32_1(X3),szNzAzT0)&sdtlpdtrp0(xd,esk32_1(X3))=szDzizrdt0(xd))&aElementOf0(esk32_1(X3),sdtlbdtrb0(xd,szDzizrdt0(xd))))&sdtlpdtrp0(xe,esk32_1(X3))=X3)),inference(shift_quantors,[status(thm)],[4522])).
% fof(4524, plain,![X3]:![X4]:(((((aElementOf0(esk32_1(X3),szNzAzT0)|(~(aElementOf0(X4,sdtlbdtrb0(xd,szDzizrdt0(xd))))|~(sdtlpdtrp0(xe,X4)=X3)))&(sdtlpdtrp0(xd,esk32_1(X3))=szDzizrdt0(xd)|(~(aElementOf0(X4,sdtlbdtrb0(xd,szDzizrdt0(xd))))|~(sdtlpdtrp0(xe,X4)=X3))))&(aElementOf0(esk32_1(X3),sdtlbdtrb0(xd,szDzizrdt0(xd)))|(~(aElementOf0(X4,sdtlbdtrb0(xd,szDzizrdt0(xd))))|~(sdtlpdtrp0(xe,X4)=X3))))&(sdtlpdtrp0(xe,esk32_1(X3))=X3|(~(aElementOf0(X4,sdtlbdtrb0(xd,szDzizrdt0(xd))))|~(sdtlpdtrp0(xe,X4)=X3))))&((((aElementOf0(esk32_1(X3),szNzAzT0)|~(aElementOf0(X3,xO)))&(sdtlpdtrp0(xd,esk32_1(X3))=szDzizrdt0(xd)|~(aElementOf0(X3,xO))))&(aElementOf0(esk32_1(X3),sdtlbdtrb0(xd,szDzizrdt0(xd)))|~(aElementOf0(X3,xO))))&(sdtlpdtrp0(xe,esk32_1(X3))=X3|~(aElementOf0(X3,xO))))),inference(distribute,[status(thm)],[4523])).
% cnf(4525,plain,(sdtlpdtrp0(xe,esk32_1(X1))=X1|~aElementOf0(X1,xO)),inference(split_conjunct,[status(thm)],[4524])).
% cnf(4528,plain,(aElementOf0(esk32_1(X1),szNzAzT0)|~aElementOf0(X1,xO)),inference(split_conjunct,[status(thm)],[4524])).
% fof(4537, plain,![X1]:((~(aSubsetOf0(X1,szNzAzT0))|X1=slcrc0)|![X2]:((~(X2=szmzizndt0(X1))|(aElementOf0(X2,X1)&![X3]:(~(aElementOf0(X3,X1))|sdtlseqdt0(X2,X3))))&((~(aElementOf0(X2,X1))|?[X3]:(aElementOf0(X3,X1)&~(sdtlseqdt0(X2,X3))))|X2=szmzizndt0(X1)))),inference(fof_nnf,[status(thm)],[75])).
% fof(4538, plain,![X4]:((~(aSubsetOf0(X4,szNzAzT0))|X4=slcrc0)|![X5]:((~(X5=szmzizndt0(X4))|(aElementOf0(X5,X4)&![X6]:(~(aElementOf0(X6,X4))|sdtlseqdt0(X5,X6))))&((~(aElementOf0(X5,X4))|?[X7]:(aElementOf0(X7,X4)&~(sdtlseqdt0(X5,X7))))|X5=szmzizndt0(X4)))),inference(variable_rename,[status(thm)],[4537])).
% fof(4539, plain,![X4]:((~(aSubsetOf0(X4,szNzAzT0))|X4=slcrc0)|![X5]:((~(X5=szmzizndt0(X4))|(aElementOf0(X5,X4)&![X6]:(~(aElementOf0(X6,X4))|sdtlseqdt0(X5,X6))))&((~(aElementOf0(X5,X4))|(aElementOf0(esk33_2(X4,X5),X4)&~(sdtlseqdt0(X5,esk33_2(X4,X5)))))|X5=szmzizndt0(X4)))),inference(skolemize,[status(esa)],[4538])).
% fof(4540, plain,![X4]:![X5]:![X6]:(((((~(aElementOf0(X6,X4))|sdtlseqdt0(X5,X6))&aElementOf0(X5,X4))|~(X5=szmzizndt0(X4)))&((~(aElementOf0(X5,X4))|(aElementOf0(esk33_2(X4,X5),X4)&~(sdtlseqdt0(X5,esk33_2(X4,X5)))))|X5=szmzizndt0(X4)))|(~(aSubsetOf0(X4,szNzAzT0))|X4=slcrc0)),inference(shift_quantors,[status(thm)],[4539])).
% fof(4541, plain,![X4]:![X5]:![X6]:(((((~(aElementOf0(X6,X4))|sdtlseqdt0(X5,X6))|~(X5=szmzizndt0(X4)))|(~(aSubsetOf0(X4,szNzAzT0))|X4=slcrc0))&((aElementOf0(X5,X4)|~(X5=szmzizndt0(X4)))|(~(aSubsetOf0(X4,szNzAzT0))|X4=slcrc0)))&((((aElementOf0(esk33_2(X4,X5),X4)|~(aElementOf0(X5,X4)))|X5=szmzizndt0(X4))|(~(aSubsetOf0(X4,szNzAzT0))|X4=slcrc0))&(((~(sdtlseqdt0(X5,esk33_2(X4,X5)))|~(aElementOf0(X5,X4)))|X5=szmzizndt0(X4))|(~(aSubsetOf0(X4,szNzAzT0))|X4=slcrc0)))),inference(distribute,[status(thm)],[4540])).
% cnf(4544,plain,(X1=slcrc0|aElementOf0(X2,X1)|~aSubsetOf0(X1,szNzAzT0)|X2!=szmzizndt0(X1)),inference(split_conjunct,[status(thm)],[4541])).
% fof(4600, plain,![X1]:((~(aSet0(X1))|~(isCountable0(X1)))|~(X1=slcrc0)),inference(fof_nnf,[status(thm)],[85])).
% fof(4601, plain,![X2]:((~(aSet0(X2))|~(isCountable0(X2)))|~(X2=slcrc0)),inference(variable_rename,[status(thm)],[4600])).
% cnf(4602,plain,(X1!=slcrc0|~isCountable0(X1)|~aSet0(X1)),inference(split_conjunct,[status(thm)],[4601])).
% fof(4619, plain,![X1]:((~(X1=slcrc0)|(aSet0(X1)&![X2]:~(aElementOf0(X2,X1))))&((~(aSet0(X1))|?[X2]:aElementOf0(X2,X1))|X1=slcrc0)),inference(fof_nnf,[status(thm)],[90])).
% fof(4620, plain,![X3]:((~(X3=slcrc0)|(aSet0(X3)&![X4]:~(aElementOf0(X4,X3))))&((~(aSet0(X3))|?[X5]:aElementOf0(X5,X3))|X3=slcrc0)),inference(variable_rename,[status(thm)],[4619])).
% fof(4621, plain,![X3]:((~(X3=slcrc0)|(aSet0(X3)&![X4]:~(aElementOf0(X4,X3))))&((~(aSet0(X3))|aElementOf0(esk38_1(X3),X3))|X3=slcrc0)),inference(skolemize,[status(esa)],[4620])).
% fof(4622, plain,![X3]:![X4]:(((~(aElementOf0(X4,X3))&aSet0(X3))|~(X3=slcrc0))&((~(aSet0(X3))|aElementOf0(esk38_1(X3),X3))|X3=slcrc0)),inference(shift_quantors,[status(thm)],[4621])).
% fof(4623, plain,![X3]:![X4]:(((~(aElementOf0(X4,X3))|~(X3=slcrc0))&(aSet0(X3)|~(X3=slcrc0)))&((~(aSet0(X3))|aElementOf0(esk38_1(X3),X3))|X3=slcrc0)),inference(distribute,[status(thm)],[4622])).
% cnf(4625,plain,(aSet0(X1)|X1!=slcrc0),inference(split_conjunct,[status(thm)],[4623])).
% fof(4639, negated_conjecture,(?[X1]:(aElementOf0(X1,xO)&~(aElementOf0(X1,xS)))&~(aSubsetOf0(xO,xS))),inference(fof_nnf,[status(thm)],[99])).
% fof(4640, negated_conjecture,(?[X2]:(aElementOf0(X2,xO)&~(aElementOf0(X2,xS)))&~(aSubsetOf0(xO,xS))),inference(variable_rename,[status(thm)],[4639])).
% fof(4641, negated_conjecture,((aElementOf0(esk39_0,xO)&~(aElementOf0(esk39_0,xS)))&~(aSubsetOf0(xO,xS))),inference(skolemize,[status(esa)],[4640])).
% cnf(4643,negated_conjecture,(~aElementOf0(esk39_0,xS)),inference(split_conjunct,[status(thm)],[4641])).
% cnf(4644,negated_conjecture,(aElementOf0(esk39_0,xO)),inference(split_conjunct,[status(thm)],[4641])).
% cnf(5299,plain,(slcrc0!=X1|~isCountable0(X1)),inference(csr,[status(thm)],[4602,4625])).
% cnf(8495,plain,(slcrc0!=sdtlpdtrp0(xN,X1)|~aElementOf0(X1,szNzAzT0)),inference(spm,[status(thm)],[5299,4408,theory(equality)])).
% cnf(8758,plain,(slcrc0=sdtlpdtrp0(xN,X1)|aElementOf0(X2,sdtlpdtrp0(xN,X1))|sdtlpdtrp0(xe,X1)!=X2|~aSubsetOf0(sdtlpdtrp0(xN,X1),szNzAzT0)|~aElementOf0(X1,szNzAzT0)),inference(spm,[status(thm)],[4544,4470,theory(equality)])).
% cnf(9266,plain,(aSubsetOf0(sdtlpdtrp0(xN,X1),xS)|~sdtlseqdt0(sz00,X1)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(sz00,szNzAzT0)),inference(spm,[status(thm)],[4416,4368,theory(equality)])).
% cnf(9268,plain,(aSubsetOf0(sdtlpdtrp0(xN,X1),xS)|~sdtlseqdt0(sz00,X1)|~aElementOf0(X1,szNzAzT0)|$false),inference(rw,[status(thm)],[9266,202,theory(equality)])).
% cnf(9269,plain,(aSubsetOf0(sdtlpdtrp0(xN,X1),xS)|~sdtlseqdt0(sz00,X1)|~aElementOf0(X1,szNzAzT0)),inference(cn,[status(thm)],[9268,theory(equality)])).
% cnf(94189,plain,(sdtlpdtrp0(xN,X1)=slcrc0|aElementOf0(X2,sdtlpdtrp0(xN,X1))|sdtlpdtrp0(xe,X1)!=X2|~aElementOf0(X1,szNzAzT0)),inference(csr,[status(thm)],[8758,4409])).
% cnf(94190,plain,(aElementOf0(X2,sdtlpdtrp0(xN,X1))|sdtlpdtrp0(xe,X1)!=X2|~aElementOf0(X1,szNzAzT0)),inference(csr,[status(thm)],[94189,8495])).
% cnf(98375,plain,(aSubsetOf0(sdtlpdtrp0(xN,X1),xS)|~aElementOf0(X1,szNzAzT0)),inference(csr,[status(thm)],[9269,222])).
% cnf(98385,plain,(aElementOf0(X1,xS)|~aElementOf0(X1,sdtlpdtrp0(xN,X2))|~aSet0(xS)|~aElementOf0(X2,szNzAzT0)),inference(spm,[status(thm)],[135,98375,theory(equality)])).
% cnf(98419,plain,(aElementOf0(X1,xS)|~aElementOf0(X1,sdtlpdtrp0(xN,X2))|$false|~aElementOf0(X2,szNzAzT0)),inference(rw,[status(thm)],[98385,363,theory(equality)])).
% cnf(98420,plain,(aElementOf0(X1,xS)|~aElementOf0(X1,sdtlpdtrp0(xN,X2))|~aElementOf0(X2,szNzAzT0)),inference(cn,[status(thm)],[98419,theory(equality)])).
% cnf(100098,plain,(aElementOf0(X1,xS)|~aElementOf0(X2,szNzAzT0)|sdtlpdtrp0(xe,X2)!=X1),inference(spm,[status(thm)],[98420,94190,theory(equality)])).
% cnf(100170,plain,(aElementOf0(X1,xS)|X2!=X1|~aElementOf0(esk32_1(X2),szNzAzT0)|~aElementOf0(X2,xO)),inference(spm,[status(thm)],[100098,4525,theory(equality)])).
% cnf(100179,plain,(aElementOf0(X1,xS)|~aElementOf0(esk32_1(X1),szNzAzT0)|~aElementOf0(X1,xO)),inference(er,[status(thm)],[100170,theory(equality)])).
% cnf(100181,plain,(aElementOf0(X1,xS)|~aElementOf0(X1,xO)),inference(csr,[status(thm)],[100179,4528])).
% cnf(100198,negated_conjecture,(~aElementOf0(esk39_0,xO)),inference(spm,[status(thm)],[4643,100181,theory(equality)])).
% cnf(100346,negated_conjecture,($false),inference(rw,[status(thm)],[100198,4644,theory(equality)])).
% cnf(100347,negated_conjecture,($false),inference(cn,[status(thm)],[100346,theory(equality)])).
% cnf(100348,negated_conjecture,($false),100347,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 7734
% # ...of these trivial : 36
% # ...subsumed : 1173
% # ...remaining for further processing: 6525
% # Other redundant clauses eliminated : 22
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 16
% # Backward-rewritten : 16
% # Generated clauses : 67801
% # ...of the previous two non-trivial : 59078
% # Contextual simplify-reflections : 3408
% # Paramodulations : 67734
% # Factorizations : 0
% # Equation resolutions : 62
% # Current number of processed clauses: 3471
% # Positive orientable unit clauses: 88
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 36
% # Non-unit-clauses : 3347
% # Current number of unprocessed clauses: 57793
% # ...number of literals in the above : 829065
% # Clause-clause subsumption calls (NU) : 1642467
% # Rec. Clause-clause subsumption calls : 55881
% # Unit Clause-clause subsumption calls : 55387
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 10
% # Indexed BW rewrite successes : 7
% # Backwards rewriting index: 703 leaves, 1.71+/-2.210 terms/leaf
% # Paramod-from index: 323 leaves, 1.04+/-0.204 terms/leaf
% # Paramod-into index: 611 leaves, 1.38+/-1.204 terms/leaf
% # -------------------------------------------------
% # User time : 11.171 s
% # System time : 0.209 s
% # Total time : 11.380 s
% # Maximum resident set size: 0 pages
% PrfWatch: 14.56 CPU 14.72 WC
% FINAL PrfWatch: 14.56 CPU 14.72 WC
% SZS output end Solution for /tmp/SystemOnTPTP21525/NUM601+3.tptp
%
%------------------------------------------------------------------------------