%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NUM492+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 : art02.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:33:22 EST 2010
% Result : Theorem 6.86s
% Output : Solution 6.86s
% 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/SystemOnTPTP29944/NUM492+3.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP29944/NUM492+3.tptp
% SZS output start Solution for /tmp/SystemOnTPTP29944/NUM492+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 30040
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% PrfWatch: 1.94 CPU 2.02 WC
% # Preprocessing time : 0.030 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 3.52 CPU 4.03 WC
% PrfWatch: 5.18 CPU 6.03 WC
% # SZS output start CNFRefutation.
% fof(2, axiom,(aNaturalNumber0(sz10)&~(sz10=sz00)),file('/tmp/SRASS.s.p', mSortsC_01)).
% fof(3, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>aNaturalNumber0(sdtpldt0(X1,X2))),file('/tmp/SRASS.s.p', mSortsB)).
% fof(4, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>aNaturalNumber0(sdtasdt0(X1,X2))),file('/tmp/SRASS.s.p', mSortsB_02)).
% fof(8, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>sdtasdt0(X1,X2)=sdtasdt0(X2,X1)),file('/tmp/SRASS.s.p', mMulComm)).
% fof(9, axiom,![X1]:![X2]:![X3]:(((aNaturalNumber0(X1)&aNaturalNumber0(X2))&aNaturalNumber0(X3))=>sdtasdt0(sdtasdt0(X1,X2),X3)=sdtasdt0(X1,sdtasdt0(X2,X3))),file('/tmp/SRASS.s.p', mMulAsso)).
% fof(10, axiom,![X1]:(aNaturalNumber0(X1)=>(sdtasdt0(X1,sz10)=X1&X1=sdtasdt0(sz10,X1))),file('/tmp/SRASS.s.p', m_MulUnit)).
% fof(14, axiom,![X1]:(aNaturalNumber0(X1)=>(~(X1=sz00)=>![X2]:![X3]:((aNaturalNumber0(X2)&aNaturalNumber0(X3))=>((sdtasdt0(X1,X2)=sdtasdt0(X1,X3)|sdtasdt0(X2,X1)=sdtasdt0(X3,X1))=>X2=X3)))),file('/tmp/SRASS.s.p', mMulCanc)).
% fof(17, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>(sdtlseqdt0(X1,X2)<=>?[X3]:(aNaturalNumber0(X3)&sdtpldt0(X1,X3)=X2))),file('/tmp/SRASS.s.p', mDefLE)).
% fof(18, 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(28, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>(doDivides0(X1,X2)<=>?[X3]:(aNaturalNumber0(X3)&X2=sdtasdt0(X1,X3)))),file('/tmp/SRASS.s.p', mDefDiv)).
% fof(31, 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(35, axiom,((aNaturalNumber0(xn)&aNaturalNumber0(xm))&aNaturalNumber0(xp)),file('/tmp/SRASS.s.p', m__1837)).
% fof(37, axiom,(((((~(xp=sz00)&~(xp=sz10))&![X1]:((aNaturalNumber0(X1)&(?[X2]:(aNaturalNumber0(X2)&xp=sdtasdt0(X1,X2))|doDivides0(X1,xp)))=>(X1=sz10|X1=xp)))&isPrime0(xp))&?[X1]:(aNaturalNumber0(X1)&sdtasdt0(xn,xm)=sdtasdt0(xp,X1)))&doDivides0(xp,sdtasdt0(xn,xm))),file('/tmp/SRASS.s.p', m__1860)).
% fof(39, axiom,((aNaturalNumber0(xr)&sdtpldt0(xp,xr)=xn)&xr=sdtmndt0(xn,xp)),file('/tmp/SRASS.s.p', m__1883)).
% fof(42, axiom,sdtasdt0(xn,xm)=sdtpldt0(sdtasdt0(xp,xm),sdtasdt0(xr,xm)),file('/tmp/SRASS.s.p', m__1951)).
% fof(43, axiom,(sdtpldt0(sdtasdt0(xp,xm),sdtasdt0(xr,xm))=sdtasdt0(xn,xm)&sdtasdt0(xr,xm)=sdtmndt0(sdtasdt0(xn,xm),sdtasdt0(xp,xm))),file('/tmp/SRASS.s.p', m__1978)).
% fof(44, axiom,((?[X1]:(aNaturalNumber0(X1)&sdtasdt0(xn,xm)=sdtasdt0(xp,X1))&?[X1]:(aNaturalNumber0(X1)&sdtasdt0(xp,xm)=sdtasdt0(xp,X1)))&doDivides0(xp,sdtasdt0(xp,xm))),file('/tmp/SRASS.s.p', m__2001)).
% fof(49, conjecture,(?[X1]:(aNaturalNumber0(X1)&sdtasdt0(xr,xm)=sdtasdt0(xp,X1))|doDivides0(xp,sdtasdt0(xr,xm))),file('/tmp/SRASS.s.p', m__)).
% fof(50, negated_conjecture,~((?[X1]:(aNaturalNumber0(X1)&sdtasdt0(xr,xm)=sdtasdt0(xp,X1))|doDivides0(xp,sdtasdt0(xr,xm)))),inference(assume_negation,[status(cth)],[49])).
% cnf(55,plain,(aNaturalNumber0(sz10)),inference(split_conjunct,[status(thm)],[2])).
% fof(56, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|aNaturalNumber0(sdtpldt0(X1,X2))),inference(fof_nnf,[status(thm)],[3])).
% fof(57, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|aNaturalNumber0(sdtpldt0(X3,X4))),inference(variable_rename,[status(thm)],[56])).
% cnf(58,plain,(aNaturalNumber0(sdtpldt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[57])).
% fof(59, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|aNaturalNumber0(sdtasdt0(X1,X2))),inference(fof_nnf,[status(thm)],[4])).
% fof(60, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|aNaturalNumber0(sdtasdt0(X3,X4))),inference(variable_rename,[status(thm)],[59])).
% cnf(61,plain,(aNaturalNumber0(sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[60])).
% fof(73, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|sdtasdt0(X1,X2)=sdtasdt0(X2,X1)),inference(fof_nnf,[status(thm)],[8])).
% fof(74, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|sdtasdt0(X3,X4)=sdtasdt0(X4,X3)),inference(variable_rename,[status(thm)],[73])).
% cnf(75,plain,(sdtasdt0(X1,X2)=sdtasdt0(X2,X1)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[74])).
% fof(76, plain,![X1]:![X2]:![X3]:(((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|~(aNaturalNumber0(X3)))|sdtasdt0(sdtasdt0(X1,X2),X3)=sdtasdt0(X1,sdtasdt0(X2,X3))),inference(fof_nnf,[status(thm)],[9])).
% fof(77, plain,![X4]:![X5]:![X6]:(((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|~(aNaturalNumber0(X6)))|sdtasdt0(sdtasdt0(X4,X5),X6)=sdtasdt0(X4,sdtasdt0(X5,X6))),inference(variable_rename,[status(thm)],[76])).
% cnf(78,plain,(sdtasdt0(sdtasdt0(X1,X2),X3)=sdtasdt0(X1,sdtasdt0(X2,X3))|~aNaturalNumber0(X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[77])).
% fof(79, plain,![X1]:(~(aNaturalNumber0(X1))|(sdtasdt0(X1,sz10)=X1&X1=sdtasdt0(sz10,X1))),inference(fof_nnf,[status(thm)],[10])).
% fof(80, plain,![X2]:(~(aNaturalNumber0(X2))|(sdtasdt0(X2,sz10)=X2&X2=sdtasdt0(sz10,X2))),inference(variable_rename,[status(thm)],[79])).
% fof(81, plain,![X2]:((sdtasdt0(X2,sz10)=X2|~(aNaturalNumber0(X2)))&(X2=sdtasdt0(sz10,X2)|~(aNaturalNumber0(X2)))),inference(distribute,[status(thm)],[80])).
% cnf(82,plain,(X1=sdtasdt0(sz10,X1)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[81])).
% fof(99, plain,![X1]:(~(aNaturalNumber0(X1))|(X1=sz00|![X2]:![X3]:((~(aNaturalNumber0(X2))|~(aNaturalNumber0(X3)))|((~(sdtasdt0(X1,X2)=sdtasdt0(X1,X3))&~(sdtasdt0(X2,X1)=sdtasdt0(X3,X1)))|X2=X3)))),inference(fof_nnf,[status(thm)],[14])).
% fof(100, plain,![X4]:(~(aNaturalNumber0(X4))|(X4=sz00|![X5]:![X6]:((~(aNaturalNumber0(X5))|~(aNaturalNumber0(X6)))|((~(sdtasdt0(X4,X5)=sdtasdt0(X4,X6))&~(sdtasdt0(X5,X4)=sdtasdt0(X6,X4)))|X5=X6)))),inference(variable_rename,[status(thm)],[99])).
% fof(101, plain,![X4]:![X5]:![X6]:((((~(aNaturalNumber0(X5))|~(aNaturalNumber0(X6)))|((~(sdtasdt0(X4,X5)=sdtasdt0(X4,X6))&~(sdtasdt0(X5,X4)=sdtasdt0(X6,X4)))|X5=X6))|X4=sz00)|~(aNaturalNumber0(X4))),inference(shift_quantors,[status(thm)],[100])).
% fof(102, plain,![X4]:![X5]:![X6]:(((((~(sdtasdt0(X4,X5)=sdtasdt0(X4,X6))|X5=X6)|(~(aNaturalNumber0(X5))|~(aNaturalNumber0(X6))))|X4=sz00)|~(aNaturalNumber0(X4)))&((((~(sdtasdt0(X5,X4)=sdtasdt0(X6,X4))|X5=X6)|(~(aNaturalNumber0(X5))|~(aNaturalNumber0(X6))))|X4=sz00)|~(aNaturalNumber0(X4)))),inference(distribute,[status(thm)],[101])).
% cnf(104,plain,(X1=sz00|X3=X2|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~aNaturalNumber0(X3)|sdtasdt0(X1,X3)!=sdtasdt0(X1,X2)),inference(split_conjunct,[status(thm)],[102])).
% fof(113, 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)],[17])).
% fof(114, 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)],[113])).
% fof(115, 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)],[114])).
% fof(116, 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)],[115])).
% fof(117, 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)],[116])).
% cnf(120,plain,(sdtlseqdt0(X2,X1)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|sdtpldt0(X2,X3)!=X1|~aNaturalNumber0(X3)),inference(split_conjunct,[status(thm)],[117])).
% fof(121, 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)],[18])).
% fof(122, 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)],[121])).
% fof(123, 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)],[122])).
% fof(124, 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)],[123])).
% cnf(125,plain,(X3=sdtmndt0(X1,X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~sdtlseqdt0(X2,X1)|sdtpldt0(X2,X3)!=X1|~aNaturalNumber0(X3)),inference(split_conjunct,[status(thm)],[124])).
% fof(168, 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)],[28])).
% fof(169, 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)],[168])).
% fof(170, 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)],[169])).
% fof(171, 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)],[170])).
% fof(172, 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)],[171])).
% cnf(173,plain,(X1=sdtasdt0(X2,esk2_2(X2,X1))|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~doDivides0(X2,X1)),inference(split_conjunct,[status(thm)],[172])).
% cnf(174,plain,(aNaturalNumber0(esk2_2(X2,X1))|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~doDivides0(X2,X1)),inference(split_conjunct,[status(thm)],[172])).
% cnf(175,plain,(doDivides0(X2,X1)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|X1!=sdtasdt0(X2,X3)|~aNaturalNumber0(X3)),inference(split_conjunct,[status(thm)],[172])).
% fof(182, 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)],[31])).
% fof(183, 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)],[182])).
% cnf(184,plain,(doDivides0(X1,X2)|~doDivides0(X1,sdtpldt0(X3,X2))|~doDivides0(X1,X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X3)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[183])).
% cnf(207,plain,(aNaturalNumber0(xp)),inference(split_conjunct,[status(thm)],[35])).
% cnf(208,plain,(aNaturalNumber0(xm)),inference(split_conjunct,[status(thm)],[35])).
% fof(341, plain,(((((~(xp=sz00)&~(xp=sz10))&![X1]:((~(aNaturalNumber0(X1))|(![X2]:(~(aNaturalNumber0(X2))|~(xp=sdtasdt0(X1,X2)))&~(doDivides0(X1,xp))))|(X1=sz10|X1=xp)))&isPrime0(xp))&?[X1]:(aNaturalNumber0(X1)&sdtasdt0(xn,xm)=sdtasdt0(xp,X1)))&doDivides0(xp,sdtasdt0(xn,xm))),inference(fof_nnf,[status(thm)],[37])).
% fof(342, plain,(((((~(xp=sz00)&~(xp=sz10))&![X3]:((~(aNaturalNumber0(X3))|(![X4]:(~(aNaturalNumber0(X4))|~(xp=sdtasdt0(X3,X4)))&~(doDivides0(X3,xp))))|(X3=sz10|X3=xp)))&isPrime0(xp))&?[X5]:(aNaturalNumber0(X5)&sdtasdt0(xn,xm)=sdtasdt0(xp,X5)))&doDivides0(xp,sdtasdt0(xn,xm))),inference(variable_rename,[status(thm)],[341])).
% fof(343, plain,(((((~(xp=sz00)&~(xp=sz10))&![X3]:((~(aNaturalNumber0(X3))|(![X4]:(~(aNaturalNumber0(X4))|~(xp=sdtasdt0(X3,X4)))&~(doDivides0(X3,xp))))|(X3=sz10|X3=xp)))&isPrime0(xp))&(aNaturalNumber0(esk9_0)&sdtasdt0(xn,xm)=sdtasdt0(xp,esk9_0)))&doDivides0(xp,sdtasdt0(xn,xm))),inference(skolemize,[status(esa)],[342])).
% fof(344, plain,![X3]:![X4]:((((((((~(aNaturalNumber0(X4))|~(xp=sdtasdt0(X3,X4)))&~(doDivides0(X3,xp)))|~(aNaturalNumber0(X3)))|(X3=sz10|X3=xp))&(~(xp=sz00)&~(xp=sz10)))&isPrime0(xp))&(aNaturalNumber0(esk9_0)&sdtasdt0(xn,xm)=sdtasdt0(xp,esk9_0)))&doDivides0(xp,sdtasdt0(xn,xm))),inference(shift_quantors,[status(thm)],[343])).
% fof(345, plain,![X3]:![X4]:((((((((~(aNaturalNumber0(X4))|~(xp=sdtasdt0(X3,X4)))|~(aNaturalNumber0(X3)))|(X3=sz10|X3=xp))&((~(doDivides0(X3,xp))|~(aNaturalNumber0(X3)))|(X3=sz10|X3=xp)))&(~(xp=sz00)&~(xp=sz10)))&isPrime0(xp))&(aNaturalNumber0(esk9_0)&sdtasdt0(xn,xm)=sdtasdt0(xp,esk9_0)))&doDivides0(xp,sdtasdt0(xn,xm))),inference(distribute,[status(thm)],[344])).
% cnf(346,plain,(doDivides0(xp,sdtasdt0(xn,xm))),inference(split_conjunct,[status(thm)],[345])).
% cnf(347,plain,(sdtasdt0(xn,xm)=sdtasdt0(xp,esk9_0)),inference(split_conjunct,[status(thm)],[345])).
% cnf(351,plain,(xp!=sz00),inference(split_conjunct,[status(thm)],[345])).
% cnf(361,plain,(aNaturalNumber0(xr)),inference(split_conjunct,[status(thm)],[39])).
% cnf(369,plain,(sdtasdt0(xn,xm)=sdtpldt0(sdtasdt0(xp,xm),sdtasdt0(xr,xm))),inference(split_conjunct,[status(thm)],[42])).
% cnf(370,plain,(sdtasdt0(xr,xm)=sdtmndt0(sdtasdt0(xn,xm),sdtasdt0(xp,xm))),inference(split_conjunct,[status(thm)],[43])).
% fof(372, plain,((?[X2]:(aNaturalNumber0(X2)&sdtasdt0(xn,xm)=sdtasdt0(xp,X2))&?[X3]:(aNaturalNumber0(X3)&sdtasdt0(xp,xm)=sdtasdt0(xp,X3)))&doDivides0(xp,sdtasdt0(xp,xm))),inference(variable_rename,[status(thm)],[44])).
% fof(373, plain,(((aNaturalNumber0(esk12_0)&sdtasdt0(xn,xm)=sdtasdt0(xp,esk12_0))&(aNaturalNumber0(esk13_0)&sdtasdt0(xp,xm)=sdtasdt0(xp,esk13_0)))&doDivides0(xp,sdtasdt0(xp,xm))),inference(skolemize,[status(esa)],[372])).
% cnf(374,plain,(doDivides0(xp,sdtasdt0(xp,xm))),inference(split_conjunct,[status(thm)],[373])).
% cnf(375,plain,(sdtasdt0(xp,xm)=sdtasdt0(xp,esk13_0)),inference(split_conjunct,[status(thm)],[373])).
% cnf(376,plain,(aNaturalNumber0(esk13_0)),inference(split_conjunct,[status(thm)],[373])).
% fof(394, negated_conjecture,(![X1]:(~(aNaturalNumber0(X1))|~(sdtasdt0(xr,xm)=sdtasdt0(xp,X1)))&~(doDivides0(xp,sdtasdt0(xr,xm)))),inference(fof_nnf,[status(thm)],[50])).
% fof(395, negated_conjecture,(![X2]:(~(aNaturalNumber0(X2))|~(sdtasdt0(xr,xm)=sdtasdt0(xp,X2)))&~(doDivides0(xp,sdtasdt0(xr,xm)))),inference(variable_rename,[status(thm)],[394])).
% fof(396, negated_conjecture,![X2]:((~(aNaturalNumber0(X2))|~(sdtasdt0(xr,xm)=sdtasdt0(xp,X2)))&~(doDivides0(xp,sdtasdt0(xr,xm)))),inference(shift_quantors,[status(thm)],[395])).
% cnf(397,negated_conjecture,(~doDivides0(xp,sdtasdt0(xr,xm))),inference(split_conjunct,[status(thm)],[396])).
% cnf(400,plain,(aNaturalNumber0(sdtasdt0(xp,xm))|~aNaturalNumber0(esk13_0)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[61,375,theory(equality)])).
% cnf(401,plain,(aNaturalNumber0(sdtasdt0(xp,xm))|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[400,376,theory(equality)])).
% cnf(402,plain,(aNaturalNumber0(sdtasdt0(xp,xm))|$false|$false),inference(rw,[status(thm)],[401,207,theory(equality)])).
% cnf(403,plain,(aNaturalNumber0(sdtasdt0(xp,xm))),inference(cn,[status(thm)],[402,theory(equality)])).
% cnf(411,plain,(doDivides0(xp,sdtasdt0(xp,esk9_0))),inference(rw,[status(thm)],[346,347,theory(equality)])).
% cnf(455,plain,(sdtpldt0(sdtasdt0(xp,xm),sdtasdt0(xr,xm))=sdtasdt0(xp,esk9_0)),inference(rw,[status(thm)],[369,347,theory(equality)])).
% cnf(460,negated_conjecture,(~doDivides0(xp,sdtasdt0(xm,xr))|~aNaturalNumber0(xr)|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[397,75,theory(equality)])).
% cnf(461,plain,(sdtpldt0(sdtasdt0(xp,xm),sdtasdt0(xm,xr))=sdtasdt0(xp,esk9_0)|~aNaturalNumber0(xr)|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[455,75,theory(equality)])).
% cnf(482,negated_conjecture,(~doDivides0(xp,sdtasdt0(xm,xr))|$false|~aNaturalNumber0(xm)),inference(rw,[status(thm)],[460,361,theory(equality)])).
% cnf(483,negated_conjecture,(~doDivides0(xp,sdtasdt0(xm,xr))|$false|$false),inference(rw,[status(thm)],[482,208,theory(equality)])).
% cnf(484,negated_conjecture,(~doDivides0(xp,sdtasdt0(xm,xr))),inference(cn,[status(thm)],[483,theory(equality)])).
% cnf(485,plain,(sdtpldt0(sdtasdt0(xp,xm),sdtasdt0(xm,xr))=sdtasdt0(xp,esk9_0)|$false|~aNaturalNumber0(xm)),inference(rw,[status(thm)],[461,361,theory(equality)])).
% cnf(486,plain,(sdtpldt0(sdtasdt0(xp,xm),sdtasdt0(xm,xr))=sdtasdt0(xp,esk9_0)|$false|$false),inference(rw,[status(thm)],[485,208,theory(equality)])).
% cnf(487,plain,(sdtpldt0(sdtasdt0(xp,xm),sdtasdt0(xm,xr))=sdtasdt0(xp,esk9_0)),inference(cn,[status(thm)],[486,theory(equality)])).
% cnf(535,plain,(doDivides0(X1,X2)|sdtasdt0(X3,X1)!=X2|~aNaturalNumber0(X3)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(spm,[status(thm)],[175,75,theory(equality)])).
% cnf(556,plain,(sdtmndt0(sdtasdt0(xp,esk9_0),sdtasdt0(xp,xm))=sdtasdt0(xr,xm)),inference(rw,[status(thm)],[370,347,theory(equality)])).
% cnf(738,plain,(sdtasdt0(X1,sdtasdt0(X2,X3))=sdtasdt0(X2,sdtasdt0(X3,X1))|~aNaturalNumber0(sdtasdt0(X2,X3))|~aNaturalNumber0(X1)|~aNaturalNumber0(X3)|~aNaturalNumber0(X2)),inference(spm,[status(thm)],[75,78,theory(equality)])).
% cnf(742,plain,(aNaturalNumber0(sdtasdt0(X1,sdtasdt0(X2,X3)))|~aNaturalNumber0(X3)|~aNaturalNumber0(sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[61,78,theory(equality)])).
% cnf(748,plain,(sdtasdt0(X1,X2)=sdtasdt0(sz10,sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(sz10)),inference(spm,[status(thm)],[78,82,theory(equality)])).
% cnf(767,plain,(sdtasdt0(X1,X2)=sdtasdt0(sz10,sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)|$false),inference(rw,[status(thm)],[748,55,theory(equality)])).
% cnf(768,plain,(sdtasdt0(X1,X2)=sdtasdt0(sz10,sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[767,theory(equality)])).
% cnf(958,plain,(sz00=xp|X1=esk13_0|sdtasdt0(xp,X1)!=sdtasdt0(xp,xm)|~aNaturalNumber0(esk13_0)|~aNaturalNumber0(X1)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[104,375,theory(equality)])).
% cnf(976,plain,(sz00=xp|X1=esk13_0|sdtasdt0(xp,X1)!=sdtasdt0(xp,xm)|$false|~aNaturalNumber0(X1)|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[958,376,theory(equality)])).
% cnf(977,plain,(sz00=xp|X1=esk13_0|sdtasdt0(xp,X1)!=sdtasdt0(xp,xm)|$false|~aNaturalNumber0(X1)|$false),inference(rw,[status(thm)],[976,207,theory(equality)])).
% cnf(978,plain,(sz00=xp|X1=esk13_0|sdtasdt0(xp,X1)!=sdtasdt0(xp,xm)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[977,theory(equality)])).
% cnf(979,plain,(X1=esk13_0|sdtasdt0(xp,X1)!=sdtasdt0(xp,xm)|~aNaturalNumber0(X1)),inference(sr,[status(thm)],[978,351,theory(equality)])).
% cnf(1043,plain,(doDivides0(X1,sdtasdt0(xr,xm))|~doDivides0(X1,sdtasdt0(xp,esk9_0))|~doDivides0(X1,sdtasdt0(xp,xm))|~aNaturalNumber0(sdtasdt0(xp,xm))|~aNaturalNumber0(sdtasdt0(xr,xm))|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[184,455,theory(equality)])).
% cnf(1285,plain,(sdtmndt0(X1,X2)=X3|sdtpldt0(X2,X3)!=X1|~aNaturalNumber0(X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[125,120])).
% cnf(1286,plain,(sdtmndt0(sdtpldt0(X1,X2),X1)=X2|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(sdtpldt0(X1,X2))),inference(er,[status(thm)],[1285,theory(equality)])).
% cnf(10107,plain,(doDivides0(esk13_0,X1)|sdtasdt0(xp,xm)!=X1|~aNaturalNumber0(xp)|~aNaturalNumber0(esk13_0)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[535,375,theory(equality)])).
% cnf(10120,plain,(doDivides0(esk13_0,X1)|sdtasdt0(xp,xm)!=X1|$false|~aNaturalNumber0(esk13_0)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[10107,207,theory(equality)])).
% cnf(10121,plain,(doDivides0(esk13_0,X1)|sdtasdt0(xp,xm)!=X1|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[10120,376,theory(equality)])).
% cnf(10122,plain,(doDivides0(esk13_0,X1)|sdtasdt0(xp,xm)!=X1|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[10121,theory(equality)])).
% cnf(12072,plain,(doDivides0(esk13_0,sdtasdt0(xp,xm))|~aNaturalNumber0(sdtasdt0(xp,xm))),inference(er,[status(thm)],[10122,theory(equality)])).
% cnf(12073,plain,(doDivides0(esk13_0,sdtasdt0(xp,xm))|$false),inference(rw,[status(thm)],[12072,403,theory(equality)])).
% cnf(12074,plain,(doDivides0(esk13_0,sdtasdt0(xp,xm))),inference(cn,[status(thm)],[12073,theory(equality)])).
% cnf(12077,plain,(aNaturalNumber0(esk2_2(esk13_0,sdtasdt0(xp,xm)))|~aNaturalNumber0(esk13_0)|~aNaturalNumber0(sdtasdt0(xp,xm))),inference(spm,[status(thm)],[174,12074,theory(equality)])).
% cnf(12078,plain,(sdtasdt0(esk13_0,esk2_2(esk13_0,sdtasdt0(xp,xm)))=sdtasdt0(xp,xm)|~aNaturalNumber0(esk13_0)|~aNaturalNumber0(sdtasdt0(xp,xm))),inference(spm,[status(thm)],[173,12074,theory(equality)])).
% cnf(12133,plain,(aNaturalNumber0(esk2_2(esk13_0,sdtasdt0(xp,xm)))|$false|~aNaturalNumber0(sdtasdt0(xp,xm))),inference(rw,[status(thm)],[12077,376,theory(equality)])).
% cnf(12134,plain,(aNaturalNumber0(esk2_2(esk13_0,sdtasdt0(xp,xm)))|$false|$false),inference(rw,[status(thm)],[12133,403,theory(equality)])).
% cnf(12135,plain,(aNaturalNumber0(esk2_2(esk13_0,sdtasdt0(xp,xm)))),inference(cn,[status(thm)],[12134,theory(equality)])).
% cnf(12136,plain,(sdtasdt0(esk13_0,esk2_2(esk13_0,sdtasdt0(xp,xm)))=sdtasdt0(xp,xm)|$false|~aNaturalNumber0(sdtasdt0(xp,xm))),inference(rw,[status(thm)],[12078,376,theory(equality)])).
% cnf(12137,plain,(sdtasdt0(esk13_0,esk2_2(esk13_0,sdtasdt0(xp,xm)))=sdtasdt0(xp,xm)|$false|$false),inference(rw,[status(thm)],[12136,403,theory(equality)])).
% cnf(12138,plain,(sdtasdt0(esk13_0,esk2_2(esk13_0,sdtasdt0(xp,xm)))=sdtasdt0(xp,xm)),inference(cn,[status(thm)],[12137,theory(equality)])).
% cnf(27475,plain,(sdtasdt0(X1,sdtasdt0(X2,X3))=sdtasdt0(X2,sdtasdt0(X3,X1))|~aNaturalNumber0(X1)|~aNaturalNumber0(X3)|~aNaturalNumber0(X2)),inference(csr,[status(thm)],[738,61])).
% cnf(28822,plain,(aNaturalNumber0(sdtasdt0(X1,sdtasdt0(X2,X3)))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(X3)),inference(csr,[status(thm)],[742,61])).
% cnf(32120,plain,(sdtasdt0(sz10,sdtasdt0(xp,xm))=sdtasdt0(xp,xm)|~aNaturalNumber0(esk2_2(esk13_0,sdtasdt0(xp,xm)))|~aNaturalNumber0(esk13_0)),inference(spm,[status(thm)],[768,12138,theory(equality)])).
% cnf(32482,plain,(sdtasdt0(sz10,sdtasdt0(xp,xm))=sdtasdt0(xp,xm)|$false|~aNaturalNumber0(esk13_0)),inference(rw,[status(thm)],[32120,12135,theory(equality)])).
% cnf(32483,plain,(sdtasdt0(sz10,sdtasdt0(xp,xm))=sdtasdt0(xp,xm)|$false|$false),inference(rw,[status(thm)],[32482,376,theory(equality)])).
% cnf(32484,plain,(sdtasdt0(sz10,sdtasdt0(xp,xm))=sdtasdt0(xp,xm)),inference(cn,[status(thm)],[32483,theory(equality)])).
% cnf(51990,plain,(sdtasdt0(xp,xm)=sdtasdt0(xp,sdtasdt0(xm,sz10))|~aNaturalNumber0(sz10)|~aNaturalNumber0(xm)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[27475,32484,theory(equality)])).
% cnf(52463,plain,(sdtasdt0(xp,xm)=sdtasdt0(xp,sdtasdt0(xm,sz10))|$false|~aNaturalNumber0(xm)|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[51990,55,theory(equality)])).
% cnf(52464,plain,(sdtasdt0(xp,xm)=sdtasdt0(xp,sdtasdt0(xm,sz10))|$false|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[52463,208,theory(equality)])).
% cnf(52465,plain,(sdtasdt0(xp,xm)=sdtasdt0(xp,sdtasdt0(xm,sz10))|$false|$false|$false),inference(rw,[status(thm)],[52464,207,theory(equality)])).
% cnf(52466,plain,(sdtasdt0(xp,xm)=sdtasdt0(xp,sdtasdt0(xm,sz10))),inference(cn,[status(thm)],[52465,theory(equality)])).
% cnf(61789,plain,(xm=esk13_0|~aNaturalNumber0(xm)),inference(er,[status(thm)],[979,theory(equality)])).
% cnf(61805,plain,(xm=esk13_0|$false),inference(rw,[status(thm)],[61789,208,theory(equality)])).
% cnf(61806,plain,(xm=esk13_0),inference(cn,[status(thm)],[61805,theory(equality)])).
% cnf(61864,plain,(X1=xm|sdtasdt0(xp,X1)!=sdtasdt0(xp,xm)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[979,61806,theory(equality)])).
% cnf(63335,plain,(sdtasdt0(xm,sz10)=xm|~aNaturalNumber0(sdtasdt0(xm,sz10))),inference(spm,[status(thm)],[61864,52466,theory(equality)])).
% cnf(63408,plain,(sdtasdt0(xm,sz10)=xm|~aNaturalNumber0(sz10)|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[63335,61,theory(equality)])).
% cnf(63415,plain,(sdtasdt0(xm,sz10)=xm|$false|~aNaturalNumber0(xm)),inference(rw,[status(thm)],[63408,55,theory(equality)])).
% cnf(63416,plain,(sdtasdt0(xm,sz10)=xm|$false|$false),inference(rw,[status(thm)],[63415,208,theory(equality)])).
% cnf(63417,plain,(sdtasdt0(xm,sz10)=xm),inference(cn,[status(thm)],[63416,theory(equality)])).
% cnf(63535,plain,(aNaturalNumber0(sdtasdt0(X1,xm))|~aNaturalNumber0(sz10)|~aNaturalNumber0(xm)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[28822,63417,theory(equality)])).
% cnf(63993,plain,(aNaturalNumber0(sdtasdt0(X1,xm))|$false|~aNaturalNumber0(xm)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[63535,55,theory(equality)])).
% cnf(63994,plain,(aNaturalNumber0(sdtasdt0(X1,xm))|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[63993,208,theory(equality)])).
% cnf(63995,plain,(aNaturalNumber0(sdtasdt0(X1,xm))|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[63994,theory(equality)])).
% cnf(78730,plain,(doDivides0(X1,sdtasdt0(xr,xm))|~doDivides0(X1,sdtasdt0(xp,esk9_0))|~doDivides0(X1,sdtasdt0(xp,xm))|$false|~aNaturalNumber0(sdtasdt0(xr,xm))|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[1043,403,theory(equality)])).
% cnf(78731,plain,(doDivides0(X1,sdtasdt0(xr,xm))|~doDivides0(X1,sdtasdt0(xp,esk9_0))|~doDivides0(X1,sdtasdt0(xp,xm))|~aNaturalNumber0(sdtasdt0(xr,xm))|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[78730,theory(equality)])).
% cnf(160248,plain,(sdtmndt0(sdtpldt0(X1,X2),X1)=X2|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[1286,58])).
% cnf(160269,plain,(sdtmndt0(sdtasdt0(xp,esk9_0),sdtasdt0(xp,xm))=sdtasdt0(xm,xr)|~aNaturalNumber0(sdtasdt0(xm,xr))|~aNaturalNumber0(sdtasdt0(xp,xm))),inference(spm,[status(thm)],[160248,487,theory(equality)])).
% cnf(160374,plain,(sdtasdt0(xr,xm)=sdtasdt0(xm,xr)|~aNaturalNumber0(sdtasdt0(xm,xr))|~aNaturalNumber0(sdtasdt0(xp,xm))),inference(rw,[status(thm)],[160269,556,theory(equality)])).
% cnf(160375,plain,(sdtasdt0(xr,xm)=sdtasdt0(xm,xr)|~aNaturalNumber0(sdtasdt0(xm,xr))|$false),inference(rw,[status(thm)],[160374,403,theory(equality)])).
% cnf(160376,plain,(sdtasdt0(xr,xm)=sdtasdt0(xm,xr)|~aNaturalNumber0(sdtasdt0(xm,xr))),inference(cn,[status(thm)],[160375,theory(equality)])).
% cnf(160450,plain,(sdtasdt0(xr,xm)=sdtasdt0(xm,xr)|~aNaturalNumber0(xr)|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[160376,61,theory(equality)])).
% cnf(160453,plain,(sdtasdt0(xr,xm)=sdtasdt0(xm,xr)|$false|~aNaturalNumber0(xm)),inference(rw,[status(thm)],[160450,361,theory(equality)])).
% cnf(160454,plain,(sdtasdt0(xr,xm)=sdtasdt0(xm,xr)|$false|$false),inference(rw,[status(thm)],[160453,208,theory(equality)])).
% cnf(160455,plain,(sdtasdt0(xr,xm)=sdtasdt0(xm,xr)),inference(cn,[status(thm)],[160454,theory(equality)])).
% cnf(160713,plain,(aNaturalNumber0(sdtasdt0(xm,xr))|~aNaturalNumber0(xr)),inference(spm,[status(thm)],[63995,160455,theory(equality)])).
% cnf(160734,plain,(doDivides0(X1,sdtasdt0(xm,xr))|~doDivides0(X1,sdtasdt0(xp,esk9_0))|~doDivides0(X1,sdtasdt0(xp,xm))|~aNaturalNumber0(sdtasdt0(xr,xm))|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[78731,160455,theory(equality)])).
% cnf(160735,plain,(doDivides0(X1,sdtasdt0(xm,xr))|~doDivides0(X1,sdtasdt0(xp,esk9_0))|~doDivides0(X1,sdtasdt0(xp,xm))|~aNaturalNumber0(sdtasdt0(xm,xr))|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[160734,160455,theory(equality)])).
% cnf(161510,plain,(aNaturalNumber0(sdtasdt0(xm,xr))|$false),inference(rw,[status(thm)],[160713,361,theory(equality)])).
% cnf(161511,plain,(aNaturalNumber0(sdtasdt0(xm,xr))),inference(cn,[status(thm)],[161510,theory(equality)])).
% cnf(164700,plain,(doDivides0(X1,sdtasdt0(xm,xr))|~doDivides0(X1,sdtasdt0(xp,esk9_0))|~doDivides0(X1,sdtasdt0(xp,xm))|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[160735,161511,theory(equality)])).
% cnf(164701,plain,(doDivides0(X1,sdtasdt0(xm,xr))|~doDivides0(X1,sdtasdt0(xp,esk9_0))|~doDivides0(X1,sdtasdt0(xp,xm))|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[164700,theory(equality)])).
% cnf(164706,plain,(doDivides0(xp,sdtasdt0(xm,xr))|~doDivides0(xp,sdtasdt0(xp,xm))|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[164701,411,theory(equality)])).
% cnf(164726,plain,(doDivides0(xp,sdtasdt0(xm,xr))|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[164706,374,theory(equality)])).
% cnf(164727,plain,(doDivides0(xp,sdtasdt0(xm,xr))|$false|$false),inference(rw,[status(thm)],[164726,207,theory(equality)])).
% cnf(164728,plain,(doDivides0(xp,sdtasdt0(xm,xr))),inference(cn,[status(thm)],[164727,theory(equality)])).
% cnf(164729,plain,($false),inference(sr,[status(thm)],[164728,484,theory(equality)])).
% cnf(164730,plain,($false),164729,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 2808
% # ...of these trivial : 199
% # ...subsumed : 1080
% # ...remaining for further processing: 1529
% # Other redundant clauses eliminated : 39
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 42
% # Backward-rewritten : 358
% # Generated clauses : 48597
% # ...of the previous two non-trivial : 44493
% # Contextual simplify-reflections : 321
% # Paramodulations : 48346
% # Factorizations : 6
% # Equation resolutions : 242
% # Current number of processed clauses: 1125
% # Positive orientable unit clauses: 419
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 26
% # Non-unit-clauses : 680
% # Current number of unprocessed clauses: 30732
% # ...number of literals in the above : 221320
% # Clause-clause subsumption calls (NU) : 19078
% # Rec. Clause-clause subsumption calls : 6593
% # Unit Clause-clause subsumption calls : 488
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 2337
% # Indexed BW rewrite successes : 107
% # Backwards rewriting index: 918 leaves, 1.34+/-1.759 terms/leaf
% # Paramod-from index: 522 leaves, 1.31+/-2.029 terms/leaf
% # Paramod-into index: 835 leaves, 1.31+/-1.772 terms/leaf
% # -------------------------------------------------
% # User time : 2.901 s
% # System time : 0.122 s
% # Total time : 3.023 s
% # Maximum resident set size: 0 pages
% PrfWatch: 5.97 CPU 6.84 WC
% FINAL PrfWatch: 5.97 CPU 6.84 WC
% SZS output end Solution for /tmp/SystemOnTPTP29944/NUM492+3.tptp
%
%------------------------------------------------------------------------------