%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NUM588+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:26 EST 2010
% Result : Theorem 12.57s
% Output : Solution 12.57s
% 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/SystemOnTPTP6630/NUM588+3.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP6630/NUM588+3.tptp
% SZS output start Solution for /tmp/SystemOnTPTP6630/NUM588+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 6726
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% PrfWatch: 1.91 CPU 2.01 WC
% PrfWatch: 3.90 CPU 4.01 WC
% PrfWatch: 5.90 CPU 6.02 WC
% PrfWatch: 7.89 CPU 8.02 WC
% # Preprocessing time : 0.566 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 9.89 CPU 10.03 WC
% # SZS output start CNFRefutation.
% fof(88, conjecture,![X1]:(aElementOf0(X1,szNzAzT0)=>![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))))))&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)))))&isCountable0(X2))=>![X3]:(((((aSet0(X3)&![X4]:(aElementOf0(X4,X3)=>aElementOf0(X4,X2)))&aSubsetOf0(X3,X2))&sbrdtbr0(X3)=xk)&aElementOf0(X3,slbdtsldtrb0(X2,xk)))=>((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1))&![X4]:(aElementOf0(X4,sdtlpdtrp0(xN,X1))=>sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X4)))=>((aSet0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))&![X4]:(aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))<=>((aElement0(X4)&aElementOf0(X4,sdtlpdtrp0(xN,X1)))&~(X4=szmzizndt0(sdtlpdtrp0(xN,X1))))))=>((![X4]:(aElementOf0(X4,X3)=>aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))))|aSubsetOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))))|aElementOf0(X3,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))),xk)))))))),file('/tmp/SRASS.s.p', m__)).
% fof(89, negated_conjecture,~(![X1]:(aElementOf0(X1,szNzAzT0)=>![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))))))&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)))))&isCountable0(X2))=>![X3]:(((((aSet0(X3)&![X4]:(aElementOf0(X4,X3)=>aElementOf0(X4,X2)))&aSubsetOf0(X3,X2))&sbrdtbr0(X3)=xk)&aElementOf0(X3,slbdtsldtrb0(X2,xk)))=>((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1))&![X4]:(aElementOf0(X4,sdtlpdtrp0(xN,X1))=>sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X4)))=>((aSet0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))&![X4]:(aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))<=>((aElement0(X4)&aElementOf0(X4,sdtlpdtrp0(xN,X1)))&~(X4=szmzizndt0(sdtlpdtrp0(xN,X1))))))=>((![X4]:(aElementOf0(X4,X3)=>aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))))|aSubsetOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))))|aElementOf0(X3,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))),xk))))))))),inference(assume_negation,[status(cth)],[88])).
% fof(4540, negated_conjecture,?[X1]:(aElementOf0(X1,szNzAzT0)&?[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)))))))&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)))))&isCountable0(X2))&?[X3]:(((((aSet0(X3)&![X4]:(~(aElementOf0(X4,X3))|aElementOf0(X4,X2)))&aSubsetOf0(X3,X2))&sbrdtbr0(X3)=xk)&aElementOf0(X3,slbdtsldtrb0(X2,xk)))&((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1))&![X4]:(~(aElementOf0(X4,sdtlpdtrp0(xN,X1)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X4)))&((aSet0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))&![X4]:((~(aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))))|((aElement0(X4)&aElementOf0(X4,sdtlpdtrp0(xN,X1)))&~(X4=szmzizndt0(sdtlpdtrp0(xN,X1)))))&(((~(aElement0(X4))|~(aElementOf0(X4,sdtlpdtrp0(xN,X1))))|X4=szmzizndt0(sdtlpdtrp0(xN,X1)))|aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))))))&((?[X4]:(aElementOf0(X4,X3)&~(aElementOf0(X4,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))))&~(aSubsetOf0(X3,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))))))&~(aElementOf0(X3,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))),xk))))))))),inference(fof_nnf,[status(thm)],[89])).
% fof(4541, negated_conjecture,?[X5]:(aElementOf0(X5,szNzAzT0)&?[X6]:((((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X5)),sdtlpdtrp0(xN,X5))&![X7]:(~(aElementOf0(X7,sdtlpdtrp0(xN,X5)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X5)),X7)))&aSet0(sdtmndt0(sdtlpdtrp0(xN,X5),szmzizndt0(sdtlpdtrp0(xN,X5)))))&![X8]:((~(aElementOf0(X8,sdtmndt0(sdtlpdtrp0(xN,X5),szmzizndt0(sdtlpdtrp0(xN,X5)))))|((aElement0(X8)&aElementOf0(X8,sdtlpdtrp0(xN,X5)))&~(X8=szmzizndt0(sdtlpdtrp0(xN,X5)))))&(((~(aElement0(X8))|~(aElementOf0(X8,sdtlpdtrp0(xN,X5))))|X8=szmzizndt0(sdtlpdtrp0(xN,X5)))|aElementOf0(X8,sdtmndt0(sdtlpdtrp0(xN,X5),szmzizndt0(sdtlpdtrp0(xN,X5)))))))&aSet0(X6))&![X9]:(~(aElementOf0(X9,X6))|aElementOf0(X9,sdtmndt0(sdtlpdtrp0(xN,X5),szmzizndt0(sdtlpdtrp0(xN,X5))))))&aSubsetOf0(X6,sdtmndt0(sdtlpdtrp0(xN,X5),szmzizndt0(sdtlpdtrp0(xN,X5)))))&isCountable0(X6))&?[X10]:(((((aSet0(X10)&![X11]:(~(aElementOf0(X11,X10))|aElementOf0(X11,X6)))&aSubsetOf0(X10,X6))&sbrdtbr0(X10)=xk)&aElementOf0(X10,slbdtsldtrb0(X6,xk)))&((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X5)),sdtlpdtrp0(xN,X5))&![X12]:(~(aElementOf0(X12,sdtlpdtrp0(xN,X5)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X5)),X12)))&((aSet0(sdtmndt0(sdtlpdtrp0(xN,X5),szmzizndt0(sdtlpdtrp0(xN,X5))))&![X13]:((~(aElementOf0(X13,sdtmndt0(sdtlpdtrp0(xN,X5),szmzizndt0(sdtlpdtrp0(xN,X5)))))|((aElement0(X13)&aElementOf0(X13,sdtlpdtrp0(xN,X5)))&~(X13=szmzizndt0(sdtlpdtrp0(xN,X5)))))&(((~(aElement0(X13))|~(aElementOf0(X13,sdtlpdtrp0(xN,X5))))|X13=szmzizndt0(sdtlpdtrp0(xN,X5)))|aElementOf0(X13,sdtmndt0(sdtlpdtrp0(xN,X5),szmzizndt0(sdtlpdtrp0(xN,X5)))))))&((?[X14]:(aElementOf0(X14,X10)&~(aElementOf0(X14,sdtmndt0(sdtlpdtrp0(xN,X5),szmzizndt0(sdtlpdtrp0(xN,X5))))))&~(aSubsetOf0(X10,sdtmndt0(sdtlpdtrp0(xN,X5),szmzizndt0(sdtlpdtrp0(xN,X5))))))&~(aElementOf0(X10,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X5),szmzizndt0(sdtlpdtrp0(xN,X5))),xk))))))))),inference(variable_rename,[status(thm)],[4540])).
% fof(4542, negated_conjecture,(aElementOf0(esk33_0,szNzAzT0)&((((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,esk33_0)),sdtlpdtrp0(xN,esk33_0))&![X7]:(~(aElementOf0(X7,sdtlpdtrp0(xN,esk33_0)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,esk33_0)),X7)))&aSet0(sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0)))))&![X8]:((~(aElementOf0(X8,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0)))))|((aElement0(X8)&aElementOf0(X8,sdtlpdtrp0(xN,esk33_0)))&~(X8=szmzizndt0(sdtlpdtrp0(xN,esk33_0)))))&(((~(aElement0(X8))|~(aElementOf0(X8,sdtlpdtrp0(xN,esk33_0))))|X8=szmzizndt0(sdtlpdtrp0(xN,esk33_0)))|aElementOf0(X8,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0)))))))&aSet0(esk34_0))&![X9]:(~(aElementOf0(X9,esk34_0))|aElementOf0(X9,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0))))))&aSubsetOf0(esk34_0,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0)))))&isCountable0(esk34_0))&(((((aSet0(esk35_0)&![X11]:(~(aElementOf0(X11,esk35_0))|aElementOf0(X11,esk34_0)))&aSubsetOf0(esk35_0,esk34_0))&sbrdtbr0(esk35_0)=xk)&aElementOf0(esk35_0,slbdtsldtrb0(esk34_0,xk)))&((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,esk33_0)),sdtlpdtrp0(xN,esk33_0))&![X12]:(~(aElementOf0(X12,sdtlpdtrp0(xN,esk33_0)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,esk33_0)),X12)))&((aSet0(sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0))))&![X13]:((~(aElementOf0(X13,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0)))))|((aElement0(X13)&aElementOf0(X13,sdtlpdtrp0(xN,esk33_0)))&~(X13=szmzizndt0(sdtlpdtrp0(xN,esk33_0)))))&(((~(aElement0(X13))|~(aElementOf0(X13,sdtlpdtrp0(xN,esk33_0))))|X13=szmzizndt0(sdtlpdtrp0(xN,esk33_0)))|aElementOf0(X13,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0)))))))&(((aElementOf0(esk36_0,esk35_0)&~(aElementOf0(esk36_0,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0))))))&~(aSubsetOf0(esk35_0,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0))))))&~(aElementOf0(esk35_0,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0))),xk))))))))),inference(skolemize,[status(esa)],[4541])).
% fof(4543, negated_conjecture,![X7]:![X8]:![X9]:![X11]:![X12]:![X13]:((((((((~(aElementOf0(X13,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0)))))|((aElement0(X13)&aElementOf0(X13,sdtlpdtrp0(xN,esk33_0)))&~(X13=szmzizndt0(sdtlpdtrp0(xN,esk33_0)))))&(((~(aElement0(X13))|~(aElementOf0(X13,sdtlpdtrp0(xN,esk33_0))))|X13=szmzizndt0(sdtlpdtrp0(xN,esk33_0)))|aElementOf0(X13,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0))))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0)))))&(((aElementOf0(esk36_0,esk35_0)&~(aElementOf0(esk36_0,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0))))))&~(aSubsetOf0(esk35_0,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0))))))&~(aElementOf0(esk35_0,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0))),xk)))))&((~(aElementOf0(X12,sdtlpdtrp0(xN,esk33_0)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,esk33_0)),X12))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,esk33_0)),sdtlpdtrp0(xN,esk33_0))))&(((((~(aElementOf0(X11,esk35_0))|aElementOf0(X11,esk34_0))&aSet0(esk35_0))&aSubsetOf0(esk35_0,esk34_0))&sbrdtbr0(esk35_0)=xk)&aElementOf0(esk35_0,slbdtsldtrb0(esk34_0,xk))))&((((~(aElementOf0(X9,esk34_0))|aElementOf0(X9,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0)))))&((((~(aElementOf0(X8,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0)))))|((aElement0(X8)&aElementOf0(X8,sdtlpdtrp0(xN,esk33_0)))&~(X8=szmzizndt0(sdtlpdtrp0(xN,esk33_0)))))&(((~(aElement0(X8))|~(aElementOf0(X8,sdtlpdtrp0(xN,esk33_0))))|X8=szmzizndt0(sdtlpdtrp0(xN,esk33_0)))|aElementOf0(X8,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0))))))&(((~(aElementOf0(X7,sdtlpdtrp0(xN,esk33_0)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,esk33_0)),X7))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,esk33_0)),sdtlpdtrp0(xN,esk33_0)))&aSet0(sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0))))))&aSet0(esk34_0)))&aSubsetOf0(esk34_0,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0)))))&isCountable0(esk34_0)))&aElementOf0(esk33_0,szNzAzT0)),inference(shift_quantors,[status(thm)],[4542])).
% fof(4544, negated_conjecture,![X7]:![X8]:![X9]:![X11]:![X12]:![X13]:((((((((((aElement0(X13)|~(aElementOf0(X13,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0))))))&(aElementOf0(X13,sdtlpdtrp0(xN,esk33_0))|~(aElementOf0(X13,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0)))))))&(~(X13=szmzizndt0(sdtlpdtrp0(xN,esk33_0)))|~(aElementOf0(X13,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0)))))))&(((~(aElement0(X13))|~(aElementOf0(X13,sdtlpdtrp0(xN,esk33_0))))|X13=szmzizndt0(sdtlpdtrp0(xN,esk33_0)))|aElementOf0(X13,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0))))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0)))))&(((aElementOf0(esk36_0,esk35_0)&~(aElementOf0(esk36_0,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0))))))&~(aSubsetOf0(esk35_0,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0))))))&~(aElementOf0(esk35_0,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0))),xk)))))&((~(aElementOf0(X12,sdtlpdtrp0(xN,esk33_0)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,esk33_0)),X12))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,esk33_0)),sdtlpdtrp0(xN,esk33_0))))&(((((~(aElementOf0(X11,esk35_0))|aElementOf0(X11,esk34_0))&aSet0(esk35_0))&aSubsetOf0(esk35_0,esk34_0))&sbrdtbr0(esk35_0)=xk)&aElementOf0(esk35_0,slbdtsldtrb0(esk34_0,xk))))&((((~(aElementOf0(X9,esk34_0))|aElementOf0(X9,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0)))))&((((((aElement0(X8)|~(aElementOf0(X8,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0))))))&(aElementOf0(X8,sdtlpdtrp0(xN,esk33_0))|~(aElementOf0(X8,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0)))))))&(~(X8=szmzizndt0(sdtlpdtrp0(xN,esk33_0)))|~(aElementOf0(X8,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0)))))))&(((~(aElement0(X8))|~(aElementOf0(X8,sdtlpdtrp0(xN,esk33_0))))|X8=szmzizndt0(sdtlpdtrp0(xN,esk33_0)))|aElementOf0(X8,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0))))))&(((~(aElementOf0(X7,sdtlpdtrp0(xN,esk33_0)))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,esk33_0)),X7))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,esk33_0)),sdtlpdtrp0(xN,esk33_0)))&aSet0(sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0))))))&aSet0(esk34_0)))&aSubsetOf0(esk34_0,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0)))))&isCountable0(esk34_0)))&aElementOf0(esk33_0,szNzAzT0)),inference(distribute,[status(thm)],[4543])).
% cnf(4556,negated_conjecture,(aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0))))|~aElementOf0(X1,esk34_0)),inference(split_conjunct,[status(thm)],[4544])).
% cnf(4561,negated_conjecture,(aElementOf0(X1,esk34_0)|~aElementOf0(X1,esk35_0)),inference(split_conjunct,[status(thm)],[4544])).
% cnf(4566,negated_conjecture,(~aElementOf0(esk36_0,sdtmndt0(sdtlpdtrp0(xN,esk33_0),szmzizndt0(sdtlpdtrp0(xN,esk33_0))))),inference(split_conjunct,[status(thm)],[4544])).
% cnf(4567,negated_conjecture,(aElementOf0(esk36_0,esk35_0)),inference(split_conjunct,[status(thm)],[4544])).
% cnf(7602,negated_conjecture,(aElementOf0(esk36_0,esk34_0)),inference(spm,[status(thm)],[4561,4567,theory(equality)])).
% cnf(7766,negated_conjecture,(~aElementOf0(esk36_0,esk34_0)),inference(spm,[status(thm)],[4566,4556,theory(equality)])).
% cnf(69120,negated_conjecture,($false),inference(sr,[status(thm)],[7602,7766,theory(equality)])).
% cnf(69121,negated_conjecture,($false),69120,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 5873
% # ...of these trivial : 3
% # ...subsumed : 361
% # ...remaining for further processing: 5509
% # Other redundant clauses eliminated : 13
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 2
% # Backward-rewritten : 0
% # Generated clauses : 54173
% # ...of the previous two non-trivial : 42992
% # Contextual simplify-reflections : 2783
% # Paramodulations : 54131
% # Factorizations : 0
% # Equation resolutions : 42
% # Current number of processed clauses: 2756
% # Positive orientable unit clauses: 36
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 10
% # Non-unit-clauses : 2710
% # Current number of unprocessed clauses: 42974
% # ...number of literals in the above : 684295
% # Clause-clause subsumption calls (NU) : 961724
% # Rec. Clause-clause subsumption calls : 40527
% # Unit Clause-clause subsumption calls : 11497
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 0
% # Indexed BW rewrite successes : 0
% # Backwards rewriting index: 293 leaves, 2.30+/-2.628 terms/leaf
% # Paramod-from index: 124 leaves, 1.04+/-0.234 terms/leaf
% # Paramod-into index: 251 leaves, 1.64+/-1.464 terms/leaf
% # -------------------------------------------------
% # User time : 8.470 s
% # System time : 0.185 s
% # Total time : 8.655 s
% # Maximum resident set size: 0 pages
% PrfWatch: 11.52 CPU 11.66 WC
% FINAL PrfWatch: 11.52 CPU 11.66 WC
% SZS output end Solution for /tmp/SystemOnTPTP6630/NUM588+3.tptp
%
%------------------------------------------------------------------------------