%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NUM487+1 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art01.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 19:31:03 EST 2010
% Result : Theorem 1.36s
% Output : Solution 1.36s
% 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/SystemOnTPTP31783/NUM487+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP31783/NUM487+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP31783/NUM487+1.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 31879
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% # Preprocessing time : 0.020 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(3, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>sdtpldt0(X1,X2)=sdtpldt0(X2,X1)),file('/tmp/SRASS.s.p', mAddComm)).
% fof(9, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>(sdtlseqdt0(X1,X2)<=>?[X3]:(aNaturalNumber0(X3)&sdtpldt0(X1,X3)=X2))),file('/tmp/SRASS.s.p', mDefLE)).
% fof(10, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>(sdtlseqdt0(X1,X2)=>![X3]:(X3=sdtmndt0(X2,X1)<=>(aNaturalNumber0(X3)&sdtpldt0(X1,X3)=X2)))),file('/tmp/SRASS.s.p', mDefDiff)).
% fof(12, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>((sdtlseqdt0(X1,X2)&sdtlseqdt0(X2,X1))=>X1=X2)),file('/tmp/SRASS.s.p', mLEAsym)).
% fof(17, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>(doDivides0(X1,X2)<=>?[X3]:(aNaturalNumber0(X3)&X2=sdtasdt0(X1,X3)))),file('/tmp/SRASS.s.p', mDefDiv)).
% fof(20, axiom,![X1]:![X2]:![X3]:(((aNaturalNumber0(X1)&aNaturalNumber0(X2))&aNaturalNumber0(X3))=>((doDivides0(X1,X2)&doDivides0(X1,sdtpldt0(X2,X3)))=>doDivides0(X1,X3))),file('/tmp/SRASS.s.p', mDivMin)).
% fof(21, axiom,((aNaturalNumber0(xn)&aNaturalNumber0(xm))&aNaturalNumber0(xp)),file('/tmp/SRASS.s.p', m__1837)).
% fof(23, axiom,(isPrime0(xp)&doDivides0(xp,sdtasdt0(xn,xm))),file('/tmp/SRASS.s.p', m__1860)).
% fof(24, axiom,sdtlseqdt0(xp,xn),file('/tmp/SRASS.s.p', m__1870)).
% fof(25, axiom,xr=sdtmndt0(xn,xp),file('/tmp/SRASS.s.p', m__1883)).
% fof(26, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>((doDivides0(X1,X2)&~(X2=sz00))=>sdtlseqdt0(X1,X2))),file('/tmp/SRASS.s.p', mDivLE)).
% fof(29, axiom,![X1]:(aNaturalNumber0(X1)=>(sdtpldt0(X1,sz00)=X1&X1=sdtpldt0(sz00,X1))),file('/tmp/SRASS.s.p', m_AddZero)).
% fof(30, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>(sdtpldt0(X1,X2)=sz00=>(X1=sz00&X2=sz00))),file('/tmp/SRASS.s.p', mZeroAdd)).
% fof(34, axiom,![X1]:(aNaturalNumber0(X1)=>(isPrime0(X1)<=>((~(X1=sz00)&~(X1=sz10))&![X2]:((aNaturalNumber0(X2)&doDivides0(X2,X1))=>(X2=sz10|X2=X1))))),file('/tmp/SRASS.s.p', mDefPrime)).
% fof(38, axiom,![X1]:(aNaturalNumber0(X1)=>(sdtasdt0(X1,sz10)=X1&X1=sdtasdt0(sz10,X1))),file('/tmp/SRASS.s.p', m_MulUnit)).
% fof(40, axiom,aNaturalNumber0(sz00),file('/tmp/SRASS.s.p', mSortsC)).
% fof(41, axiom,(aNaturalNumber0(sz10)&~(sz10=sz00)),file('/tmp/SRASS.s.p', mSortsC_01)).
% fof(44, conjecture,(~(xr=xn)&sdtlseqdt0(xr,xn)),file('/tmp/SRASS.s.p', m__)).
% fof(45, negated_conjecture,~((~(xr=xn)&sdtlseqdt0(xr,xn))),inference(assume_negation,[status(cth)],[44])).
% fof(54, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|sdtpldt0(X1,X2)=sdtpldt0(X2,X1)),inference(fof_nnf,[status(thm)],[3])).
% fof(55, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|sdtpldt0(X3,X4)=sdtpldt0(X4,X3)),inference(variable_rename,[status(thm)],[54])).
% cnf(56,plain,(sdtpldt0(X1,X2)=sdtpldt0(X2,X1)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[55])).
% fof(76, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|((~(sdtlseqdt0(X1,X2))|?[X3]:(aNaturalNumber0(X3)&sdtpldt0(X1,X3)=X2))&(![X3]:(~(aNaturalNumber0(X3))|~(sdtpldt0(X1,X3)=X2))|sdtlseqdt0(X1,X2)))),inference(fof_nnf,[status(thm)],[9])).
% fof(77, plain,![X4]:![X5]:((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|((~(sdtlseqdt0(X4,X5))|?[X6]:(aNaturalNumber0(X6)&sdtpldt0(X4,X6)=X5))&(![X7]:(~(aNaturalNumber0(X7))|~(sdtpldt0(X4,X7)=X5))|sdtlseqdt0(X4,X5)))),inference(variable_rename,[status(thm)],[76])).
% fof(78, plain,![X4]:![X5]:((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|((~(sdtlseqdt0(X4,X5))|(aNaturalNumber0(esk1_2(X4,X5))&sdtpldt0(X4,esk1_2(X4,X5))=X5))&(![X7]:(~(aNaturalNumber0(X7))|~(sdtpldt0(X4,X7)=X5))|sdtlseqdt0(X4,X5)))),inference(skolemize,[status(esa)],[77])).
% fof(79, plain,![X4]:![X5]:![X7]:((((~(aNaturalNumber0(X7))|~(sdtpldt0(X4,X7)=X5))|sdtlseqdt0(X4,X5))&(~(sdtlseqdt0(X4,X5))|(aNaturalNumber0(esk1_2(X4,X5))&sdtpldt0(X4,esk1_2(X4,X5))=X5)))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))),inference(shift_quantors,[status(thm)],[78])).
% fof(80, plain,![X4]:![X5]:![X7]:((((~(aNaturalNumber0(X7))|~(sdtpldt0(X4,X7)=X5))|sdtlseqdt0(X4,X5))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5))))&(((aNaturalNumber0(esk1_2(X4,X5))|~(sdtlseqdt0(X4,X5)))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5))))&((sdtpldt0(X4,esk1_2(X4,X5))=X5|~(sdtlseqdt0(X4,X5)))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))))),inference(distribute,[status(thm)],[79])).
% cnf(81,plain,(sdtpldt0(X2,esk1_2(X2,X1))=X1|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~sdtlseqdt0(X2,X1)),inference(split_conjunct,[status(thm)],[80])).
% cnf(82,plain,(aNaturalNumber0(esk1_2(X2,X1))|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~sdtlseqdt0(X2,X1)),inference(split_conjunct,[status(thm)],[80])).
% cnf(83,plain,(sdtlseqdt0(X2,X1)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|sdtpldt0(X2,X3)!=X1|~aNaturalNumber0(X3)),inference(split_conjunct,[status(thm)],[80])).
% fof(84, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|(~(sdtlseqdt0(X1,X2))|![X3]:((~(X3=sdtmndt0(X2,X1))|(aNaturalNumber0(X3)&sdtpldt0(X1,X3)=X2))&((~(aNaturalNumber0(X3))|~(sdtpldt0(X1,X3)=X2))|X3=sdtmndt0(X2,X1))))),inference(fof_nnf,[status(thm)],[10])).
% fof(85, plain,![X4]:![X5]:((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|(~(sdtlseqdt0(X4,X5))|![X6]:((~(X6=sdtmndt0(X5,X4))|(aNaturalNumber0(X6)&sdtpldt0(X4,X6)=X5))&((~(aNaturalNumber0(X6))|~(sdtpldt0(X4,X6)=X5))|X6=sdtmndt0(X5,X4))))),inference(variable_rename,[status(thm)],[84])).
% fof(86, plain,![X4]:![X5]:![X6]:((((~(X6=sdtmndt0(X5,X4))|(aNaturalNumber0(X6)&sdtpldt0(X4,X6)=X5))&((~(aNaturalNumber0(X6))|~(sdtpldt0(X4,X6)=X5))|X6=sdtmndt0(X5,X4)))|~(sdtlseqdt0(X4,X5)))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))),inference(shift_quantors,[status(thm)],[85])).
% fof(87, plain,![X4]:![X5]:![X6]:(((((aNaturalNumber0(X6)|~(X6=sdtmndt0(X5,X4)))|~(sdtlseqdt0(X4,X5)))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5))))&(((sdtpldt0(X4,X6)=X5|~(X6=sdtmndt0(X5,X4)))|~(sdtlseqdt0(X4,X5)))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))))&((((~(aNaturalNumber0(X6))|~(sdtpldt0(X4,X6)=X5))|X6=sdtmndt0(X5,X4))|~(sdtlseqdt0(X4,X5)))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5))))),inference(distribute,[status(thm)],[86])).
% cnf(88,plain,(X3=sdtmndt0(X1,X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~sdtlseqdt0(X2,X1)|sdtpldt0(X2,X3)!=X1|~aNaturalNumber0(X3)),inference(split_conjunct,[status(thm)],[87])).
% cnf(89,plain,(sdtpldt0(X2,X3)=X1|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~sdtlseqdt0(X2,X1)|X3!=sdtmndt0(X1,X2)),inference(split_conjunct,[status(thm)],[87])).
% cnf(90,plain,(aNaturalNumber0(X3)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~sdtlseqdt0(X2,X1)|X3!=sdtmndt0(X1,X2)),inference(split_conjunct,[status(thm)],[87])).
% fof(94, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|((~(sdtlseqdt0(X1,X2))|~(sdtlseqdt0(X2,X1)))|X1=X2)),inference(fof_nnf,[status(thm)],[12])).
% fof(95, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|((~(sdtlseqdt0(X3,X4))|~(sdtlseqdt0(X4,X3)))|X3=X4)),inference(variable_rename,[status(thm)],[94])).
% cnf(96,plain,(X1=X2|~sdtlseqdt0(X2,X1)|~sdtlseqdt0(X1,X2)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[95])).
% fof(116, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|((~(doDivides0(X1,X2))|?[X3]:(aNaturalNumber0(X3)&X2=sdtasdt0(X1,X3)))&(![X3]:(~(aNaturalNumber0(X3))|~(X2=sdtasdt0(X1,X3)))|doDivides0(X1,X2)))),inference(fof_nnf,[status(thm)],[17])).
% fof(117, plain,![X4]:![X5]:((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|((~(doDivides0(X4,X5))|?[X6]:(aNaturalNumber0(X6)&X5=sdtasdt0(X4,X6)))&(![X7]:(~(aNaturalNumber0(X7))|~(X5=sdtasdt0(X4,X7)))|doDivides0(X4,X5)))),inference(variable_rename,[status(thm)],[116])).
% fof(118, plain,![X4]:![X5]:((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|((~(doDivides0(X4,X5))|(aNaturalNumber0(esk2_2(X4,X5))&X5=sdtasdt0(X4,esk2_2(X4,X5))))&(![X7]:(~(aNaturalNumber0(X7))|~(X5=sdtasdt0(X4,X7)))|doDivides0(X4,X5)))),inference(skolemize,[status(esa)],[117])).
% fof(119, plain,![X4]:![X5]:![X7]:((((~(aNaturalNumber0(X7))|~(X5=sdtasdt0(X4,X7)))|doDivides0(X4,X5))&(~(doDivides0(X4,X5))|(aNaturalNumber0(esk2_2(X4,X5))&X5=sdtasdt0(X4,esk2_2(X4,X5)))))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))),inference(shift_quantors,[status(thm)],[118])).
% fof(120, plain,![X4]:![X5]:![X7]:((((~(aNaturalNumber0(X7))|~(X5=sdtasdt0(X4,X7)))|doDivides0(X4,X5))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5))))&(((aNaturalNumber0(esk2_2(X4,X5))|~(doDivides0(X4,X5)))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5))))&((X5=sdtasdt0(X4,esk2_2(X4,X5))|~(doDivides0(X4,X5)))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))))),inference(distribute,[status(thm)],[119])).
% cnf(123,plain,(doDivides0(X2,X1)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|X1!=sdtasdt0(X2,X3)|~aNaturalNumber0(X3)),inference(split_conjunct,[status(thm)],[120])).
% fof(130, plain,![X1]:![X2]:![X3]:(((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|~(aNaturalNumber0(X3)))|((~(doDivides0(X1,X2))|~(doDivides0(X1,sdtpldt0(X2,X3))))|doDivides0(X1,X3))),inference(fof_nnf,[status(thm)],[20])).
% fof(131, plain,![X4]:![X5]:![X6]:(((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|~(aNaturalNumber0(X6)))|((~(doDivides0(X4,X5))|~(doDivides0(X4,sdtpldt0(X5,X6))))|doDivides0(X4,X6))),inference(variable_rename,[status(thm)],[130])).
% cnf(132,plain,(doDivides0(X1,X2)|~doDivides0(X1,sdtpldt0(X3,X2))|~doDivides0(X1,X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X3)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[131])).
% cnf(133,plain,(aNaturalNumber0(xp)),inference(split_conjunct,[status(thm)],[21])).
% cnf(135,plain,(aNaturalNumber0(xn)),inference(split_conjunct,[status(thm)],[21])).
% cnf(140,plain,(isPrime0(xp)),inference(split_conjunct,[status(thm)],[23])).
% cnf(141,plain,(sdtlseqdt0(xp,xn)),inference(split_conjunct,[status(thm)],[24])).
% cnf(142,plain,(xr=sdtmndt0(xn,xp)),inference(split_conjunct,[status(thm)],[25])).
% fof(143, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|((~(doDivides0(X1,X2))|X2=sz00)|sdtlseqdt0(X1,X2))),inference(fof_nnf,[status(thm)],[26])).
% fof(144, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|((~(doDivides0(X3,X4))|X4=sz00)|sdtlseqdt0(X3,X4))),inference(variable_rename,[status(thm)],[143])).
% cnf(145,plain,(sdtlseqdt0(X1,X2)|X2=sz00|~doDivides0(X1,X2)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[144])).
% fof(156, plain,![X1]:(~(aNaturalNumber0(X1))|(sdtpldt0(X1,sz00)=X1&X1=sdtpldt0(sz00,X1))),inference(fof_nnf,[status(thm)],[29])).
% fof(157, plain,![X2]:(~(aNaturalNumber0(X2))|(sdtpldt0(X2,sz00)=X2&X2=sdtpldt0(sz00,X2))),inference(variable_rename,[status(thm)],[156])).
% fof(158, plain,![X2]:((sdtpldt0(X2,sz00)=X2|~(aNaturalNumber0(X2)))&(X2=sdtpldt0(sz00,X2)|~(aNaturalNumber0(X2)))),inference(distribute,[status(thm)],[157])).
% cnf(160,plain,(sdtpldt0(X1,sz00)=X1|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[158])).
% fof(161, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|(~(sdtpldt0(X1,X2)=sz00)|(X1=sz00&X2=sz00))),inference(fof_nnf,[status(thm)],[30])).
% fof(162, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|(~(sdtpldt0(X3,X4)=sz00)|(X3=sz00&X4=sz00))),inference(variable_rename,[status(thm)],[161])).
% fof(163, plain,![X3]:![X4]:(((X3=sz00|~(sdtpldt0(X3,X4)=sz00))|(~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4))))&((X4=sz00|~(sdtpldt0(X3,X4)=sz00))|(~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4))))),inference(distribute,[status(thm)],[162])).
% cnf(165,plain,(X2=sz00|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|sdtpldt0(X2,X1)!=sz00),inference(split_conjunct,[status(thm)],[163])).
% fof(180, plain,![X1]:(~(aNaturalNumber0(X1))|((~(isPrime0(X1))|((~(X1=sz00)&~(X1=sz10))&![X2]:((~(aNaturalNumber0(X2))|~(doDivides0(X2,X1)))|(X2=sz10|X2=X1))))&(((X1=sz00|X1=sz10)|?[X2]:((aNaturalNumber0(X2)&doDivides0(X2,X1))&(~(X2=sz10)&~(X2=X1))))|isPrime0(X1)))),inference(fof_nnf,[status(thm)],[34])).
% fof(181, plain,![X3]:(~(aNaturalNumber0(X3))|((~(isPrime0(X3))|((~(X3=sz00)&~(X3=sz10))&![X4]:((~(aNaturalNumber0(X4))|~(doDivides0(X4,X3)))|(X4=sz10|X4=X3))))&(((X3=sz00|X3=sz10)|?[X5]:((aNaturalNumber0(X5)&doDivides0(X5,X3))&(~(X5=sz10)&~(X5=X3))))|isPrime0(X3)))),inference(variable_rename,[status(thm)],[180])).
% fof(182, plain,![X3]:(~(aNaturalNumber0(X3))|((~(isPrime0(X3))|((~(X3=sz00)&~(X3=sz10))&![X4]:((~(aNaturalNumber0(X4))|~(doDivides0(X4,X3)))|(X4=sz10|X4=X3))))&(((X3=sz00|X3=sz10)|((aNaturalNumber0(esk3_1(X3))&doDivides0(esk3_1(X3),X3))&(~(esk3_1(X3)=sz10)&~(esk3_1(X3)=X3))))|isPrime0(X3)))),inference(skolemize,[status(esa)],[181])).
% fof(183, plain,![X3]:![X4]:((((((~(aNaturalNumber0(X4))|~(doDivides0(X4,X3)))|(X4=sz10|X4=X3))&(~(X3=sz00)&~(X3=sz10)))|~(isPrime0(X3)))&(((X3=sz00|X3=sz10)|((aNaturalNumber0(esk3_1(X3))&doDivides0(esk3_1(X3),X3))&(~(esk3_1(X3)=sz10)&~(esk3_1(X3)=X3))))|isPrime0(X3)))|~(aNaturalNumber0(X3))),inference(shift_quantors,[status(thm)],[182])).
% fof(184, plain,![X3]:![X4]:((((((~(aNaturalNumber0(X4))|~(doDivides0(X4,X3)))|(X4=sz10|X4=X3))|~(isPrime0(X3)))|~(aNaturalNumber0(X3)))&(((~(X3=sz00)|~(isPrime0(X3)))|~(aNaturalNumber0(X3)))&((~(X3=sz10)|~(isPrime0(X3)))|~(aNaturalNumber0(X3)))))&(((((aNaturalNumber0(esk3_1(X3))|(X3=sz00|X3=sz10))|isPrime0(X3))|~(aNaturalNumber0(X3)))&(((doDivides0(esk3_1(X3),X3)|(X3=sz00|X3=sz10))|isPrime0(X3))|~(aNaturalNumber0(X3))))&((((~(esk3_1(X3)=sz10)|(X3=sz00|X3=sz10))|isPrime0(X3))|~(aNaturalNumber0(X3)))&(((~(esk3_1(X3)=X3)|(X3=sz00|X3=sz10))|isPrime0(X3))|~(aNaturalNumber0(X3)))))),inference(distribute,[status(thm)],[183])).
% cnf(189,plain,(~aNaturalNumber0(X1)|~isPrime0(X1)|X1!=sz10),inference(split_conjunct,[status(thm)],[184])).
% cnf(190,plain,(~aNaturalNumber0(X1)|~isPrime0(X1)|X1!=sz00),inference(split_conjunct,[status(thm)],[184])).
% cnf(191,plain,(X2=X1|X2=sz10|~aNaturalNumber0(X1)|~isPrime0(X1)|~doDivides0(X2,X1)|~aNaturalNumber0(X2)),inference(split_conjunct,[status(thm)],[184])).
% fof(210, plain,![X1]:(~(aNaturalNumber0(X1))|(sdtasdt0(X1,sz10)=X1&X1=sdtasdt0(sz10,X1))),inference(fof_nnf,[status(thm)],[38])).
% fof(211, plain,![X2]:(~(aNaturalNumber0(X2))|(sdtasdt0(X2,sz10)=X2&X2=sdtasdt0(sz10,X2))),inference(variable_rename,[status(thm)],[210])).
% fof(212, plain,![X2]:((sdtasdt0(X2,sz10)=X2|~(aNaturalNumber0(X2)))&(X2=sdtasdt0(sz10,X2)|~(aNaturalNumber0(X2)))),inference(distribute,[status(thm)],[211])).
% cnf(214,plain,(sdtasdt0(X1,sz10)=X1|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[212])).
% cnf(217,plain,(aNaturalNumber0(sz00)),inference(split_conjunct,[status(thm)],[40])).
% cnf(219,plain,(aNaturalNumber0(sz10)),inference(split_conjunct,[status(thm)],[41])).
% fof(227, negated_conjecture,(xr=xn|~(sdtlseqdt0(xr,xn))),inference(fof_nnf,[status(thm)],[45])).
% cnf(228,negated_conjecture,(xr=xn|~sdtlseqdt0(xr,xn)),inference(split_conjunct,[status(thm)],[227])).
% cnf(230,plain,(sdtmndt0(X1,X2)=X3|sdtpldt0(X2,X3)!=X1|~aNaturalNumber0(X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[88,83])).
% cnf(236,plain,(~isPrime0(sz00)|~aNaturalNumber0(sz00)),inference(er,[status(thm)],[190,theory(equality)])).
% cnf(237,plain,(~isPrime0(sz00)|$false),inference(rw,[status(thm)],[236,217,theory(equality)])).
% cnf(238,plain,(~isPrime0(sz00)),inference(cn,[status(thm)],[237,theory(equality)])).
% cnf(239,plain,(~isPrime0(sz10)|~aNaturalNumber0(sz10)),inference(er,[status(thm)],[189,theory(equality)])).
% cnf(240,plain,(~isPrime0(sz10)|$false),inference(rw,[status(thm)],[239,219,theory(equality)])).
% cnf(241,plain,(~isPrime0(sz10)),inference(cn,[status(thm)],[240,theory(equality)])).
% cnf(353,plain,(aNaturalNumber0(esk1_2(xp,xn))|~aNaturalNumber0(xp)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[82,141,theory(equality)])).
% cnf(360,plain,(aNaturalNumber0(esk1_2(xp,xn))|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[353,133,theory(equality)])).
% cnf(361,plain,(aNaturalNumber0(esk1_2(xp,xn))|$false|$false),inference(rw,[status(thm)],[360,135,theory(equality)])).
% cnf(362,plain,(aNaturalNumber0(esk1_2(xp,xn))),inference(cn,[status(thm)],[361,theory(equality)])).
% cnf(372,plain,(sdtpldt0(xp,esk1_2(xp,xn))=xn|~aNaturalNumber0(xp)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[81,141,theory(equality)])).
% cnf(379,plain,(sdtpldt0(xp,esk1_2(xp,xn))=xn|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[372,133,theory(equality)])).
% cnf(380,plain,(sdtpldt0(xp,esk1_2(xp,xn))=xn|$false|$false),inference(rw,[status(thm)],[379,135,theory(equality)])).
% cnf(381,plain,(sdtpldt0(xp,esk1_2(xp,xn))=xn),inference(cn,[status(thm)],[380,theory(equality)])).
% cnf(393,plain,(sdtlseqdt0(X1,X2)|sdtpldt0(X3,X1)!=X2|~aNaturalNumber0(X3)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(spm,[status(thm)],[83,56,theory(equality)])).
% cnf(402,plain,(aNaturalNumber0(X1)|xr!=X1|~sdtlseqdt0(xp,xn)|~aNaturalNumber0(xp)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[90,142,theory(equality)])).
% cnf(403,plain,(aNaturalNumber0(X1)|xr!=X1|$false|~aNaturalNumber0(xp)|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[402,141,theory(equality)])).
% cnf(404,plain,(aNaturalNumber0(X1)|xr!=X1|$false|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[403,133,theory(equality)])).
% cnf(405,plain,(aNaturalNumber0(X1)|xr!=X1|$false|$false|$false),inference(rw,[status(thm)],[404,135,theory(equality)])).
% cnf(406,plain,(aNaturalNumber0(X1)|xr!=X1),inference(cn,[status(thm)],[405,theory(equality)])).
% cnf(428,plain,(doDivides0(X1,X2)|X1!=X2|~aNaturalNumber0(sz10)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(spm,[status(thm)],[123,214,theory(equality)])).
% cnf(437,plain,(doDivides0(X1,X2)|X1!=X2|$false|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(rw,[status(thm)],[428,219,theory(equality)])).
% cnf(438,plain,(doDivides0(X1,X2)|X1!=X2|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(cn,[status(thm)],[437,theory(equality)])).
% cnf(439,plain,(doDivides0(X1,X1)|~aNaturalNumber0(X1)),inference(er,[status(thm)],[438,theory(equality)])).
% cnf(482,plain,(sdtpldt0(xp,X1)=xn|xr!=X1|~sdtlseqdt0(xp,xn)|~aNaturalNumber0(xp)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[89,142,theory(equality)])).
% cnf(483,plain,(sdtpldt0(xp,X1)=xn|xr!=X1|$false|~aNaturalNumber0(xp)|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[482,141,theory(equality)])).
% cnf(484,plain,(sdtpldt0(xp,X1)=xn|xr!=X1|$false|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[483,133,theory(equality)])).
% cnf(485,plain,(sdtpldt0(xp,X1)=xn|xr!=X1|$false|$false|$false),inference(rw,[status(thm)],[484,135,theory(equality)])).
% cnf(486,plain,(sdtpldt0(xp,X1)=xn|xr!=X1),inference(cn,[status(thm)],[485,theory(equality)])).
% cnf(514,plain,(sdtmndt0(X1,X2)=sz00|X2!=X1|~aNaturalNumber0(sz00)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[230,160,theory(equality)])).
% cnf(520,plain,(sdtmndt0(X1,X2)=sz00|X2!=X1|$false|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[514,217,theory(equality)])).
% cnf(521,plain,(sdtmndt0(X1,X2)=sz00|X2!=X1|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[520,theory(equality)])).
% cnf(522,plain,(sdtmndt0(X1,X1)=sz00|~aNaturalNumber0(X1)),inference(er,[status(thm)],[521,theory(equality)])).
% cnf(825,plain,(aNaturalNumber0(xr)),inference(er,[status(thm)],[406,theory(equality)])).
% cnf(1052,plain,(sz00=xp|xn!=sz00|~aNaturalNumber0(xp)|~aNaturalNumber0(esk1_2(xp,xn))),inference(spm,[status(thm)],[165,381,theory(equality)])).
% cnf(1065,plain,(sz00=xp|xn!=sz00|$false|~aNaturalNumber0(esk1_2(xp,xn))),inference(rw,[status(thm)],[1052,133,theory(equality)])).
% cnf(1066,plain,(sz00=xp|xn!=sz00|$false|$false),inference(rw,[status(thm)],[1065,362,theory(equality)])).
% cnf(1067,plain,(sz00=xp|xn!=sz00),inference(cn,[status(thm)],[1066,theory(equality)])).
% cnf(2373,plain,(sdtpldt0(xp,xr)=xn),inference(er,[status(thm)],[486,theory(equality)])).
% cnf(4475,plain,(sdtlseqdt0(xr,X1)|xn!=X1|~aNaturalNumber0(xp)|~aNaturalNumber0(xr)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[393,2373,theory(equality)])).
% cnf(4527,plain,(sdtlseqdt0(xr,X1)|xn!=X1|$false|~aNaturalNumber0(xr)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[4475,133,theory(equality)])).
% cnf(4528,plain,(sdtlseqdt0(xr,X1)|xn!=X1|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[4527,825,theory(equality)])).
% cnf(4529,plain,(sdtlseqdt0(xr,X1)|xn!=X1|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[4528,theory(equality)])).
% cnf(4759,plain,(sdtlseqdt0(xr,xn)|~aNaturalNumber0(xn)),inference(er,[status(thm)],[4529,theory(equality)])).
% cnf(4760,plain,(sdtlseqdt0(xr,xn)|$false),inference(rw,[status(thm)],[4759,135,theory(equality)])).
% cnf(4761,plain,(sdtlseqdt0(xr,xn)),inference(cn,[status(thm)],[4760,theory(equality)])).
% cnf(4860,negated_conjecture,(xr=xn|$false),inference(rw,[status(thm)],[228,4761,theory(equality)])).
% cnf(4861,negated_conjecture,(xr=xn),inference(cn,[status(thm)],[4860,theory(equality)])).
% cnf(5023,plain,(sdtpldt0(xp,xn)=xn),inference(rw,[status(thm)],[2373,4861,theory(equality)])).
% cnf(5055,plain,(sdtmndt0(xn,xp)=xn),inference(rw,[status(thm)],[142,4861,theory(equality)])).
% cnf(5061,plain,(sdtpldt0(xn,xp)=xn|~aNaturalNumber0(xp)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[56,5023,theory(equality)])).
% cnf(5078,plain,(sdtpldt0(xn,xp)=xn|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[5061,133,theory(equality)])).
% cnf(5079,plain,(sdtpldt0(xn,xp)=xn|$false|$false),inference(rw,[status(thm)],[5078,135,theory(equality)])).
% cnf(5080,plain,(sdtpldt0(xn,xp)=xn),inference(cn,[status(thm)],[5079,theory(equality)])).
% cnf(5294,plain,(doDivides0(X1,xp)|~doDivides0(X1,xn)|~aNaturalNumber0(xn)|~aNaturalNumber0(xp)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[132,5080,theory(equality)])).
% cnf(5329,plain,(doDivides0(X1,xp)|~doDivides0(X1,xn)|$false|~aNaturalNumber0(xp)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[5294,135,theory(equality)])).
% cnf(5330,plain,(doDivides0(X1,xp)|~doDivides0(X1,xn)|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[5329,133,theory(equality)])).
% cnf(5331,plain,(doDivides0(X1,xp)|~doDivides0(X1,xn)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[5330,theory(equality)])).
% cnf(6038,plain,(doDivides0(xn,xp)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[5331,439,theory(equality)])).
% cnf(6046,plain,(doDivides0(xn,xp)|$false),inference(rw,[status(thm)],[6038,135,theory(equality)])).
% cnf(6047,plain,(doDivides0(xn,xp)),inference(cn,[status(thm)],[6046,theory(equality)])).
% cnf(6084,plain,(sz00=xp|sdtlseqdt0(xn,xp)|~aNaturalNumber0(xp)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[145,6047,theory(equality)])).
% cnf(6085,plain,(sz10=xn|xp=xn|~isPrime0(xp)|~aNaturalNumber0(xn)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[191,6047,theory(equality)])).
% cnf(6091,plain,(sz00=xp|sdtlseqdt0(xn,xp)|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[6084,133,theory(equality)])).
% cnf(6092,plain,(sz00=xp|sdtlseqdt0(xn,xp)|$false|$false),inference(rw,[status(thm)],[6091,135,theory(equality)])).
% cnf(6093,plain,(sz00=xp|sdtlseqdt0(xn,xp)),inference(cn,[status(thm)],[6092,theory(equality)])).
% cnf(6094,plain,(sz10=xn|xp=xn|$false|~aNaturalNumber0(xn)|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[6085,140,theory(equality)])).
% cnf(6095,plain,(sz10=xn|xp=xn|$false|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[6094,135,theory(equality)])).
% cnf(6096,plain,(sz10=xn|xp=xn|$false|$false|$false),inference(rw,[status(thm)],[6095,133,theory(equality)])).
% cnf(6097,plain,(sz10=xn|xp=xn),inference(cn,[status(thm)],[6096,theory(equality)])).
% cnf(6115,plain,(sdtmndt0(xn,xn)=xn|xn=sz10),inference(spm,[status(thm)],[5055,6097,theory(equality)])).
% cnf(6131,plain,(xp=xn|xp=sz00|~sdtlseqdt0(xp,xn)|~aNaturalNumber0(xn)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[96,6093,theory(equality)])).
% cnf(6147,plain,(xp=xn|xp=sz00|$false|~aNaturalNumber0(xn)|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[6131,141,theory(equality)])).
% cnf(6148,plain,(xp=xn|xp=sz00|$false|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[6147,135,theory(equality)])).
% cnf(6149,plain,(xp=xn|xp=sz00|$false|$false|$false),inference(rw,[status(thm)],[6148,133,theory(equality)])).
% cnf(6150,plain,(xp=xn|xp=sz00),inference(cn,[status(thm)],[6149,theory(equality)])).
% cnf(6244,plain,(isPrime0(xn)|xp=sz00),inference(spm,[status(thm)],[140,6150,theory(equality)])).
% cnf(6770,plain,(xn=sz00|xn=sz10|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[522,6115,theory(equality)])).
% cnf(6779,plain,(xn=sz00|xn=sz10|$false),inference(rw,[status(thm)],[6770,135,theory(equality)])).
% cnf(6780,plain,(xn=sz00|xn=sz10),inference(cn,[status(thm)],[6779,theory(equality)])).
% cnf(6819,plain,(xp=sz00|isPrime0(sz10)|xn=sz00),inference(spm,[status(thm)],[6244,6780,theory(equality)])).
% cnf(6846,plain,(xp=sz00|xn=sz00),inference(sr,[status(thm)],[6819,241,theory(equality)])).
% cnf(6915,plain,(xp=sz00),inference(csr,[status(thm)],[6846,1067])).
% cnf(6961,plain,(isPrime0(sz00)),inference(rw,[status(thm)],[140,6915,theory(equality)])).
% cnf(6962,plain,($false),inference(sr,[status(thm)],[6961,238,theory(equality)])).
% cnf(6963,plain,($false),6962,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 658
% # ...of these trivial : 6
% # ...subsumed : 234
% # ...remaining for further processing: 418
% # Other redundant clauses eliminated : 33
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 18
% # Backward-rewritten : 129
% # Generated clauses : 2235
% # ...of the previous two non-trivial : 1823
% # Contextual simplify-reflections : 114
% # Paramodulations : 2143
% # Factorizations : 8
% # Equation resolutions : 84
% # Current number of processed clauses: 199
% # Positive orientable unit clauses: 39
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 4
% # Non-unit-clauses : 156
% # Current number of unprocessed clauses: 770
% # ...number of literals in the above : 3513
% # Clause-clause subsumption calls (NU) : 2072
% # Rec. Clause-clause subsumption calls : 1177
% # Unit Clause-clause subsumption calls : 45
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 14
% # Indexed BW rewrite successes : 14
% # Backwards rewriting index: 152 leaves, 1.30+/-0.924 terms/leaf
% # Paramod-from index: 111 leaves, 1.07+/-0.291 terms/leaf
% # Paramod-into index: 138 leaves, 1.20+/-0.806 terms/leaf
% # -------------------------------------------------
% # User time : 0.139 s
% # System time : 0.005 s
% # Total time : 0.144 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.34 CPU 0.44 WC
% FINAL PrfWatch: 0.34 CPU 0.44 WC
% SZS output end Solution for /tmp/SystemOnTPTP31783/NUM487+1.tptp
%
%------------------------------------------------------------------------------