%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NUM496+3 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art09.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Wed Dec 29 19:35:27 EST 2010
% Result : Theorem 1.77s
% Output : Solution 1.77s
% 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/SystemOnTPTP8269/NUM496+3.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP8269/NUM496+3.tptp
% SZS output start Solution for /tmp/SystemOnTPTP8269/NUM496+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 8365
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Preprocessing time : 0.030 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(2, axiom,(aNaturalNumber0(sz10)&~(sz10=sz00)),file('/tmp/SRASS.s.p', mSortsC_01)).
% fof(5, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>sdtpldt0(X1,X2)=sdtpldt0(X2,X1)),file('/tmp/SRASS.s.p', mAddComm)).
% fof(30, axiom,![X1]:![X2]:![X3]:(((aNaturalNumber0(X1)&aNaturalNumber0(X2))&aNaturalNumber0(X3))=>((doDivides0(X1,X2)&doDivides0(X1,X3))=>doDivides0(X1,sdtpldt0(X2,X3)))),file('/tmp/SRASS.s.p', mDivSum)).
% fof(33, 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(34, axiom,![X1]:(((aNaturalNumber0(X1)&~(X1=sz00))&~(X1=sz10))=>?[X2]:((aNaturalNumber0(X2)&doDivides0(X2,X1))&isPrime0(X2))),file('/tmp/SRASS.s.p', mPrimDiv)).
% 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,((?[X1]:(aNaturalNumber0(X1)&xr=sdtasdt0(xp,X1))&doDivides0(xp,xr))|(?[X1]:(aNaturalNumber0(X1)&xm=sdtasdt0(xp,X1))&doDivides0(xp,xm))),file('/tmp/SRASS.s.p', m__2027)).
% fof(47, conjecture,(((?[X1]:(aNaturalNumber0(X1)&xn=sdtasdt0(xp,X1))|doDivides0(xp,xn))|?[X1]:(aNaturalNumber0(X1)&xm=sdtasdt0(xp,X1)))|doDivides0(xp,xm)),file('/tmp/SRASS.s.p', m__)).
% fof(48, negated_conjecture,~((((?[X1]:(aNaturalNumber0(X1)&xn=sdtasdt0(xp,X1))|doDivides0(xp,xn))|?[X1]:(aNaturalNumber0(X1)&xm=sdtasdt0(xp,X1)))|doDivides0(xp,xm))),inference(assume_negation,[status(cth)],[47])).
% cnf(53,plain,(aNaturalNumber0(sz10)),inference(split_conjunct,[status(thm)],[2])).
% fof(60, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|sdtpldt0(X1,X2)=sdtpldt0(X2,X1)),inference(fof_nnf,[status(thm)],[5])).
% fof(61, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|sdtpldt0(X3,X4)=sdtpldt0(X4,X3)),inference(variable_rename,[status(thm)],[60])).
% cnf(62,plain,(sdtpldt0(X1,X2)=sdtpldt0(X2,X1)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[61])).
% fof(177, plain,![X1]:![X2]:![X3]:(((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|~(aNaturalNumber0(X3)))|((~(doDivides0(X1,X2))|~(doDivides0(X1,X3)))|doDivides0(X1,sdtpldt0(X2,X3)))),inference(fof_nnf,[status(thm)],[30])).
% fof(178, plain,![X4]:![X5]:![X6]:(((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|~(aNaturalNumber0(X6)))|((~(doDivides0(X4,X5))|~(doDivides0(X4,X6)))|doDivides0(X4,sdtpldt0(X5,X6)))),inference(variable_rename,[status(thm)],[177])).
% cnf(179,plain,(doDivides0(X1,sdtpldt0(X2,X3))|~doDivides0(X1,X3)|~doDivides0(X1,X2)|~aNaturalNumber0(X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[178])).
% fof(186, 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)],[33])).
% fof(187, 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)],[186])).
% fof(188, 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)],[187])).
% fof(189, 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)],[188])).
% fof(190, 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)],[189])).
% cnf(195,plain,(~aNaturalNumber0(X1)|~isPrime0(X1)|X1!=sz10),inference(split_conjunct,[status(thm)],[190])).
% fof(198, plain,![X1]:(((~(aNaturalNumber0(X1))|X1=sz00)|X1=sz10)|?[X2]:((aNaturalNumber0(X2)&doDivides0(X2,X1))&isPrime0(X2))),inference(fof_nnf,[status(thm)],[34])).
% fof(199, plain,![X3]:(((~(aNaturalNumber0(X3))|X3=sz00)|X3=sz10)|?[X4]:((aNaturalNumber0(X4)&doDivides0(X4,X3))&isPrime0(X4))),inference(variable_rename,[status(thm)],[198])).
% fof(200, plain,![X3]:(((~(aNaturalNumber0(X3))|X3=sz00)|X3=sz10)|((aNaturalNumber0(esk4_1(X3))&doDivides0(esk4_1(X3),X3))&isPrime0(esk4_1(X3)))),inference(skolemize,[status(esa)],[199])).
% fof(201, plain,![X3]:(((aNaturalNumber0(esk4_1(X3))|((~(aNaturalNumber0(X3))|X3=sz00)|X3=sz10))&(doDivides0(esk4_1(X3),X3)|((~(aNaturalNumber0(X3))|X3=sz00)|X3=sz10)))&(isPrime0(esk4_1(X3))|((~(aNaturalNumber0(X3))|X3=sz00)|X3=sz10))),inference(distribute,[status(thm)],[200])).
% cnf(202,plain,(X1=sz10|X1=sz00|isPrime0(esk4_1(X1))|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[201])).
% cnf(203,plain,(X1=sz10|X1=sz00|doDivides0(esk4_1(X1),X1)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[201])).
% cnf(204,plain,(X1=sz10|X1=sz00|aNaturalNumber0(esk4_1(X1))|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[201])).
% cnf(205,plain,(aNaturalNumber0(xp)),inference(split_conjunct,[status(thm)],[35])).
% fof(339, 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(340, 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)],[339])).
% fof(341, 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)],[340])).
% fof(342, 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)],[341])).
% fof(343, 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)],[342])).
% cnf(348,plain,(xp!=sz10),inference(split_conjunct,[status(thm)],[343])).
% cnf(349,plain,(xp!=sz00),inference(split_conjunct,[status(thm)],[343])).
% cnf(350,plain,(X1=xp|X1=sz10|~aNaturalNumber0(X1)|~doDivides0(X1,xp)),inference(split_conjunct,[status(thm)],[343])).
% cnf(358,plain,(sdtpldt0(xp,xr)=xn),inference(split_conjunct,[status(thm)],[39])).
% cnf(359,plain,(aNaturalNumber0(xr)),inference(split_conjunct,[status(thm)],[39])).
% fof(371, plain,((?[X2]:(aNaturalNumber0(X2)&xr=sdtasdt0(xp,X2))&doDivides0(xp,xr))|(?[X3]:(aNaturalNumber0(X3)&xm=sdtasdt0(xp,X3))&doDivides0(xp,xm))),inference(variable_rename,[status(thm)],[42])).
% fof(372, plain,(((aNaturalNumber0(esk13_0)&xr=sdtasdt0(xp,esk13_0))&doDivides0(xp,xr))|((aNaturalNumber0(esk14_0)&xm=sdtasdt0(xp,esk14_0))&doDivides0(xp,xm))),inference(skolemize,[status(esa)],[371])).
% fof(373, plain,(((((aNaturalNumber0(esk14_0)|aNaturalNumber0(esk13_0))&(xm=sdtasdt0(xp,esk14_0)|aNaturalNumber0(esk13_0)))&(doDivides0(xp,xm)|aNaturalNumber0(esk13_0)))&(((aNaturalNumber0(esk14_0)|xr=sdtasdt0(xp,esk13_0))&(xm=sdtasdt0(xp,esk14_0)|xr=sdtasdt0(xp,esk13_0)))&(doDivides0(xp,xm)|xr=sdtasdt0(xp,esk13_0))))&(((aNaturalNumber0(esk14_0)|doDivides0(xp,xr))&(xm=sdtasdt0(xp,esk14_0)|doDivides0(xp,xr)))&(doDivides0(xp,xm)|doDivides0(xp,xr)))),inference(distribute,[status(thm)],[372])).
% cnf(374,plain,(doDivides0(xp,xr)|doDivides0(xp,xm)),inference(split_conjunct,[status(thm)],[373])).
% fof(398, negated_conjecture,(((![X1]:(~(aNaturalNumber0(X1))|~(xn=sdtasdt0(xp,X1)))&~(doDivides0(xp,xn)))&![X1]:(~(aNaturalNumber0(X1))|~(xm=sdtasdt0(xp,X1))))&~(doDivides0(xp,xm))),inference(fof_nnf,[status(thm)],[48])).
% fof(399, negated_conjecture,(((![X2]:(~(aNaturalNumber0(X2))|~(xn=sdtasdt0(xp,X2)))&~(doDivides0(xp,xn)))&![X3]:(~(aNaturalNumber0(X3))|~(xm=sdtasdt0(xp,X3))))&~(doDivides0(xp,xm))),inference(variable_rename,[status(thm)],[398])).
% fof(400, negated_conjecture,![X2]:![X3]:(((~(aNaturalNumber0(X3))|~(xm=sdtasdt0(xp,X3)))&((~(aNaturalNumber0(X2))|~(xn=sdtasdt0(xp,X2)))&~(doDivides0(xp,xn))))&~(doDivides0(xp,xm))),inference(shift_quantors,[status(thm)],[399])).
% cnf(401,negated_conjecture,(~doDivides0(xp,xm)),inference(split_conjunct,[status(thm)],[400])).
% cnf(402,negated_conjecture,(~doDivides0(xp,xn)),inference(split_conjunct,[status(thm)],[400])).
% cnf(407,plain,(doDivides0(xp,xr)),inference(sr,[status(thm)],[374,401,theory(equality)])).
% cnf(487,plain,(~isPrime0(sz10)|~aNaturalNumber0(sz10)),inference(er,[status(thm)],[195,theory(equality)])).
% cnf(488,plain,(~isPrime0(sz10)|$false),inference(rw,[status(thm)],[487,53,theory(equality)])).
% cnf(489,plain,(~isPrime0(sz10)),inference(cn,[status(thm)],[488,theory(equality)])).
% cnf(624,plain,(xp=esk4_1(xp)|sz10=esk4_1(xp)|sz10=xp|sz00=xp|~aNaturalNumber0(esk4_1(xp))|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[350,203,theory(equality)])).
% cnf(626,plain,(xp=esk4_1(xp)|sz10=esk4_1(xp)|sz10=xp|sz00=xp|~aNaturalNumber0(esk4_1(xp))|$false),inference(rw,[status(thm)],[624,205,theory(equality)])).
% cnf(627,plain,(xp=esk4_1(xp)|sz10=esk4_1(xp)|sz10=xp|sz00=xp|~aNaturalNumber0(esk4_1(xp))),inference(cn,[status(thm)],[626,theory(equality)])).
% cnf(628,plain,(esk4_1(xp)=xp|esk4_1(xp)=sz10|sz00=xp|~aNaturalNumber0(esk4_1(xp))),inference(sr,[status(thm)],[627,348,theory(equality)])).
% cnf(629,plain,(esk4_1(xp)=xp|esk4_1(xp)=sz10|~aNaturalNumber0(esk4_1(xp))),inference(sr,[status(thm)],[628,349,theory(equality)])).
% cnf(17848,plain,(esk4_1(xp)=sz10|esk4_1(xp)=xp|sz10=xp|sz00=xp|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[629,204,theory(equality)])).
% cnf(17849,plain,(esk4_1(xp)=sz10|esk4_1(xp)=xp|sz10=xp|sz00=xp|$false),inference(rw,[status(thm)],[17848,205,theory(equality)])).
% cnf(17850,plain,(esk4_1(xp)=sz10|esk4_1(xp)=xp|sz10=xp|sz00=xp),inference(cn,[status(thm)],[17849,theory(equality)])).
% cnf(17851,plain,(esk4_1(xp)=sz10|esk4_1(xp)=xp|sz00=xp),inference(sr,[status(thm)],[17850,348,theory(equality)])).
% cnf(17852,plain,(esk4_1(xp)=sz10|esk4_1(xp)=xp),inference(sr,[status(thm)],[17851,349,theory(equality)])).
% cnf(17855,plain,(sz10=xp|sz00=xp|isPrime0(sz10)|esk4_1(xp)=xp|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[202,17852,theory(equality)])).
% cnf(17861,plain,(sz10=xp|sz00=xp|isPrime0(sz10)|esk4_1(xp)=xp|$false),inference(rw,[status(thm)],[17855,205,theory(equality)])).
% cnf(17862,plain,(sz10=xp|sz00=xp|isPrime0(sz10)|esk4_1(xp)=xp),inference(cn,[status(thm)],[17861,theory(equality)])).
% cnf(17863,plain,(sz00=xp|isPrime0(sz10)|esk4_1(xp)=xp),inference(sr,[status(thm)],[17862,348,theory(equality)])).
% cnf(17864,plain,(isPrime0(sz10)|esk4_1(xp)=xp),inference(sr,[status(thm)],[17863,349,theory(equality)])).
% cnf(17865,plain,(esk4_1(xp)=xp),inference(sr,[status(thm)],[17864,489,theory(equality)])).
% cnf(17873,plain,(sz10=xp|sz00=xp|doDivides0(xp,xp)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[203,17865,theory(equality)])).
% cnf(17882,plain,(sz10=xp|sz00=xp|doDivides0(xp,xp)|$false),inference(rw,[status(thm)],[17873,205,theory(equality)])).
% cnf(17883,plain,(sz10=xp|sz00=xp|doDivides0(xp,xp)),inference(cn,[status(thm)],[17882,theory(equality)])).
% cnf(17884,plain,(sz00=xp|doDivides0(xp,xp)),inference(sr,[status(thm)],[17883,348,theory(equality)])).
% cnf(17885,plain,(doDivides0(xp,xp)),inference(sr,[status(thm)],[17884,349,theory(equality)])).
% cnf(17891,plain,(doDivides0(xp,sdtpldt0(X1,xp))|~doDivides0(xp,X1)|~aNaturalNumber0(xp)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[179,17885,theory(equality)])).
% cnf(17905,plain,(doDivides0(xp,sdtpldt0(X1,xp))|~doDivides0(xp,X1)|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[17891,205,theory(equality)])).
% cnf(17906,plain,(doDivides0(xp,sdtpldt0(X1,xp))|~doDivides0(xp,X1)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[17905,theory(equality)])).
% cnf(20103,plain,(doDivides0(xp,sdtpldt0(xr,xp))|~aNaturalNumber0(xr)),inference(spm,[status(thm)],[17906,407,theory(equality)])).
% cnf(20114,plain,(doDivides0(xp,sdtpldt0(xr,xp))|$false),inference(rw,[status(thm)],[20103,359,theory(equality)])).
% cnf(20115,plain,(doDivides0(xp,sdtpldt0(xr,xp))),inference(cn,[status(thm)],[20114,theory(equality)])).
% cnf(20210,plain,(doDivides0(xp,sdtpldt0(xp,xr))|~aNaturalNumber0(xr)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[20115,62,theory(equality)])).
% cnf(20233,plain,(doDivides0(xp,xn)|~aNaturalNumber0(xr)|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[20210,358,theory(equality)])).
% cnf(20234,plain,(doDivides0(xp,xn)|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[20233,359,theory(equality)])).
% cnf(20235,plain,(doDivides0(xp,xn)|$false|$false),inference(rw,[status(thm)],[20234,205,theory(equality)])).
% cnf(20236,plain,(doDivides0(xp,xn)),inference(cn,[status(thm)],[20235,theory(equality)])).
% cnf(20237,plain,($false),inference(sr,[status(thm)],[20236,402,theory(equality)])).
% cnf(20238,plain,($false),20237,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 512
% # ...of these trivial : 9
% # ...subsumed : 104
% # ...remaining for further processing: 399
% # Other redundant clauses eliminated : 15
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 6
% # Backward-rewritten : 12
% # Generated clauses : 5583
% # ...of the previous two non-trivial : 5284
% # Contextual simplify-reflections : 24
% # Paramodulations : 5465
% # Factorizations : 4
% # Equation resolutions : 114
% # Current number of processed clauses: 380
% # Positive orientable unit clauses: 84
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 19
% # Non-unit-clauses : 277
% # Current number of unprocessed clauses: 4471
% # ...number of literals in the above : 34907
% # Clause-clause subsumption calls (NU) : 10752
% # Rec. Clause-clause subsumption calls : 853
% # Unit Clause-clause subsumption calls : 519
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 13
% # Indexed BW rewrite successes : 11
% # Backwards rewriting index: 249 leaves, 1.25+/-0.847 terms/leaf
% # Paramod-from index: 141 leaves, 1.04+/-0.234 terms/leaf
% # Paramod-into index: 208 leaves, 1.13+/-0.735 terms/leaf
% # -------------------------------------------------
% # User time : 0.404 s
% # System time : 0.017 s
% # Total time : 0.421 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.90 CPU 0.98 WC
% FINAL PrfWatch: 0.90 CPU 0.98 WC
% SZS output end Solution for /tmp/SystemOnTPTP8269/NUM496+3.tptp
%
%------------------------------------------------------------------------------