%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NUM571+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 : art05.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:10:54 EST 2010
% Result : Theorem 11.05s
% Output : Solution 11.05s
% 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/SystemOnTPTP32208/NUM571+3.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP32208/NUM571+3.tptp
% SZS output start Solution for /tmp/SystemOnTPTP32208/NUM571+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 32304
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% PrfWatch: 1.94 CPU 2.02 WC
% PrfWatch: 3.55 CPU 4.02 WC
% PrfWatch: 5.20 CPU 6.03 WC
% PrfWatch: 7.20 CPU 8.03 WC
% # Preprocessing time : 0.542 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 9.20 CPU 10.04 WC
% # SZS output start CNFRefutation.
% fof(42, axiom,(((aSet0(xS)&![X1]:(aElementOf0(X1,xS)=>aElementOf0(X1,szNzAzT0)))&aSubsetOf0(xS,szNzAzT0))&isCountable0(xS)),file('/tmp/SRASS.s.p', m__3435)).
% fof(48, 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(51, axiom,(~(xi=sz00)=>((((?[X1]:(aElementOf0(X1,szNzAzT0)&szszuzczcdt0(X1)=xi)&aSet0(sdtlpdtrp0(xN,xi)))&![X1]:(aElementOf0(X1,sdtlpdtrp0(xN,xi))=>aElementOf0(X1,szNzAzT0)))&aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0))&isCountable0(sdtlpdtrp0(xN,xi)))),file('/tmp/SRASS.s.p', m__3702_02)).
% fof(85, conjecture,(((aSet0(sdtlpdtrp0(xN,xi))&![X1]:(aElementOf0(X1,sdtlpdtrp0(xN,xi))=>aElementOf0(X1,szNzAzT0)))|aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0))&isCountable0(sdtlpdtrp0(xN,xi))),file('/tmp/SRASS.s.p', m__)).
% fof(86, negated_conjecture,~((((aSet0(sdtlpdtrp0(xN,xi))&![X1]:(aElementOf0(X1,sdtlpdtrp0(xN,xi))=>aElementOf0(X1,szNzAzT0)))|aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0))&isCountable0(sdtlpdtrp0(xN,xi)))),inference(assume_negation,[status(cth)],[85])).
% fof(284, plain,(((aSet0(xS)&![X1]:(~(aElementOf0(X1,xS))|aElementOf0(X1,szNzAzT0)))&aSubsetOf0(xS,szNzAzT0))&isCountable0(xS)),inference(fof_nnf,[status(thm)],[42])).
% fof(285, plain,(((aSet0(xS)&![X2]:(~(aElementOf0(X2,xS))|aElementOf0(X2,szNzAzT0)))&aSubsetOf0(xS,szNzAzT0))&isCountable0(xS)),inference(variable_rename,[status(thm)],[284])).
% fof(286, plain,![X2]:((((~(aElementOf0(X2,xS))|aElementOf0(X2,szNzAzT0))&aSet0(xS))&aSubsetOf0(xS,szNzAzT0))&isCountable0(xS)),inference(shift_quantors,[status(thm)],[285])).
% cnf(287,plain,(isCountable0(xS)),inference(split_conjunct,[status(thm)],[286])).
% cnf(288,plain,(aSubsetOf0(xS,szNzAzT0)),inference(split_conjunct,[status(thm)],[286])).
% fof(4289, 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)],[48])).
% fof(4290, 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)],[4289])).
% fof(4291, plain,(((aFunction0(xN)&szDzozmdt0(xN)=szNzAzT0)&sdtlpdtrp0(xN,sz00)=xS)&![X3]:(~(aElementOf0(X3,szNzAzT0))|((((~(aSet0(sdtlpdtrp0(xN,X3)))|(aElementOf0(esk22_1(X3),sdtlpdtrp0(xN,X3))&~(aElementOf0(esk22_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)],[4290])).
% fof(4292, 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(esk22_1(X3),sdtlpdtrp0(xN,X3))&~(aElementOf0(esk22_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)],[4291])).
% fof(4293, plain,![X3]:![X5]:![X6]:![X7]:((((((((((aElementOf0(esk22_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(esk22_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(esk22_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(esk22_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(esk22_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(esk22_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(esk22_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(esk22_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(esk22_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(esk22_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(esk22_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(esk22_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(esk22_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(esk22_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(esk22_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(esk22_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(esk22_1(X3),sdtlpdtrp0(xN,X3))|~(aSet0(sdtlpdtrp0(xN,X3))))|~(isCountable0(sdtlpdtrp0(xN,X3))))|aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X3))))|~(aElementOf0(X3,szNzAzT0)))&((((~(aElementOf0(esk22_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(esk22_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(esk22_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(esk22_1(X3),sdtlpdtrp0(xN,X3))|~(aSet0(sdtlpdtrp0(xN,X3))))|~(isCountable0(sdtlpdtrp0(xN,X3))))|isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X3))))|~(aElementOf0(X3,szNzAzT0)))&((((~(aElementOf0(esk22_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)],[4292])).
% cnf(4294,plain,(sdtlpdtrp0(xN,sz00)=xS),inference(split_conjunct,[status(thm)],[4293])).
% fof(4339, plain,(xi=sz00|((((?[X1]:(aElementOf0(X1,szNzAzT0)&szszuzczcdt0(X1)=xi)&aSet0(sdtlpdtrp0(xN,xi)))&![X1]:(~(aElementOf0(X1,sdtlpdtrp0(xN,xi)))|aElementOf0(X1,szNzAzT0)))&aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0))&isCountable0(sdtlpdtrp0(xN,xi)))),inference(fof_nnf,[status(thm)],[51])).
% fof(4340, plain,(xi=sz00|((((?[X2]:(aElementOf0(X2,szNzAzT0)&szszuzczcdt0(X2)=xi)&aSet0(sdtlpdtrp0(xN,xi)))&![X3]:(~(aElementOf0(X3,sdtlpdtrp0(xN,xi)))|aElementOf0(X3,szNzAzT0)))&aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0))&isCountable0(sdtlpdtrp0(xN,xi)))),inference(variable_rename,[status(thm)],[4339])).
% fof(4341, plain,(xi=sz00|(((((aElementOf0(esk23_0,szNzAzT0)&szszuzczcdt0(esk23_0)=xi)&aSet0(sdtlpdtrp0(xN,xi)))&![X3]:(~(aElementOf0(X3,sdtlpdtrp0(xN,xi)))|aElementOf0(X3,szNzAzT0)))&aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0))&isCountable0(sdtlpdtrp0(xN,xi)))),inference(skolemize,[status(esa)],[4340])).
% fof(4342, plain,![X3]:(((((~(aElementOf0(X3,sdtlpdtrp0(xN,xi)))|aElementOf0(X3,szNzAzT0))&((aElementOf0(esk23_0,szNzAzT0)&szszuzczcdt0(esk23_0)=xi)&aSet0(sdtlpdtrp0(xN,xi))))&aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0))&isCountable0(sdtlpdtrp0(xN,xi)))|xi=sz00),inference(shift_quantors,[status(thm)],[4341])).
% fof(4343, plain,![X3]:(((((~(aElementOf0(X3,sdtlpdtrp0(xN,xi)))|aElementOf0(X3,szNzAzT0))|xi=sz00)&(((aElementOf0(esk23_0,szNzAzT0)|xi=sz00)&(szszuzczcdt0(esk23_0)=xi|xi=sz00))&(aSet0(sdtlpdtrp0(xN,xi))|xi=sz00)))&(aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)|xi=sz00))&(isCountable0(sdtlpdtrp0(xN,xi))|xi=sz00)),inference(distribute,[status(thm)],[4342])).
% cnf(4344,plain,(xi=sz00|isCountable0(sdtlpdtrp0(xN,xi))),inference(split_conjunct,[status(thm)],[4343])).
% cnf(4345,plain,(xi=sz00|aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)),inference(split_conjunct,[status(thm)],[4343])).
% fof(4509, negated_conjecture,(((~(aSet0(sdtlpdtrp0(xN,xi)))|?[X1]:(aElementOf0(X1,sdtlpdtrp0(xN,xi))&~(aElementOf0(X1,szNzAzT0))))&~(aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)))|~(isCountable0(sdtlpdtrp0(xN,xi)))),inference(fof_nnf,[status(thm)],[86])).
% fof(4510, negated_conjecture,(((~(aSet0(sdtlpdtrp0(xN,xi)))|?[X2]:(aElementOf0(X2,sdtlpdtrp0(xN,xi))&~(aElementOf0(X2,szNzAzT0))))&~(aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)))|~(isCountable0(sdtlpdtrp0(xN,xi)))),inference(variable_rename,[status(thm)],[4509])).
% fof(4511, negated_conjecture,(((~(aSet0(sdtlpdtrp0(xN,xi)))|(aElementOf0(esk32_0,sdtlpdtrp0(xN,xi))&~(aElementOf0(esk32_0,szNzAzT0))))&~(aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)))|~(isCountable0(sdtlpdtrp0(xN,xi)))),inference(skolemize,[status(esa)],[4510])).
% fof(4512, negated_conjecture,((((aElementOf0(esk32_0,sdtlpdtrp0(xN,xi))|~(aSet0(sdtlpdtrp0(xN,xi))))|~(isCountable0(sdtlpdtrp0(xN,xi))))&((~(aElementOf0(esk32_0,szNzAzT0))|~(aSet0(sdtlpdtrp0(xN,xi))))|~(isCountable0(sdtlpdtrp0(xN,xi)))))&(~(aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0))|~(isCountable0(sdtlpdtrp0(xN,xi))))),inference(distribute,[status(thm)],[4511])).
% cnf(4513,negated_conjecture,(~isCountable0(sdtlpdtrp0(xN,xi))|~aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)),inference(split_conjunct,[status(thm)],[4512])).
% cnf(7014,negated_conjecture,(xi=sz00|~aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)),inference(spm,[status(thm)],[4513,4344,theory(equality)])).
% cnf(62867,negated_conjecture,(xi=sz00),inference(csr,[status(thm)],[7014,4345])).
% cnf(62887,negated_conjecture,($false|~isCountable0(sdtlpdtrp0(xN,xi))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[4513,62867,theory(equality)]),4294,theory(equality)]),288,theory(equality)])).
% cnf(62888,negated_conjecture,($false|$false),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[62887,62867,theory(equality)]),4294,theory(equality)]),287,theory(equality)])).
% cnf(62889,negated_conjecture,($false),inference(cn,[status(thm)],[62888,theory(equality)])).
% cnf(62890,negated_conjecture,($false),62889,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 5497
% # ...of these trivial : 0
% # ...subsumed : 265
% # ...remaining for further processing: 5232
% # Other redundant clauses eliminated : 13
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 0
% # Backward-rewritten : 17
% # Generated clauses : 49472
% # ...of the previous two non-trivial : 36162
% # Contextual simplify-reflections : 2463
% # Paramodulations : 49434
% # Factorizations : 0
% # Equation resolutions : 38
% # Current number of processed clauses: 2606
% # Positive orientable unit clauses: 27
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 6
% # Non-unit-clauses : 2573
% # Current number of unprocessed clauses: 35963
% # ...number of literals in the above : 588358
% # Clause-clause subsumption calls (NU) : 535028
% # Rec. Clause-clause subsumption calls : 38852
% # Unit Clause-clause subsumption calls : 15648
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 1
% # Indexed BW rewrite successes : 1
% # Backwards rewriting index: 240 leaves, 2.23+/-2.661 terms/leaf
% # Paramod-from index: 102 leaves, 1.02+/-0.139 terms/leaf
% # Paramod-into index: 204 leaves, 1.57+/-1.462 terms/leaf
% # -------------------------------------------------
% # User time : 7.513 s
% # System time : 0.146 s
% # Total time : 7.659 s
% # Maximum resident set size: 0 pages
% PrfWatch: 10.03 CPU 10.95 WC
% FINAL PrfWatch: 10.03 CPU 10.95 WC
% SZS output end Solution for /tmp/SystemOnTPTP32208/NUM571+3.tptp
%
%------------------------------------------------------------------------------