%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NUM481+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:28:54 EST 2010
% Result : Theorem 95.14s
% Output : Solution 96.18s
% 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/SystemOnTPTP29432/NUM481+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% not found
% Adding ~C to TBU ... ~m__:
% ---- Iteration 1 (0 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... mSortsC:
% CSA axiom mSortsC found
% Looking for CSA axiom ... mSortsC_01:
% CSA axiom mSortsC_01 found
% Looking for CSA axiom ... mDivTrans:
% CSA axiom mDivTrans found
% ---- Iteration 2 (3 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... mDefPrime:
% CSA axiom mDefPrime found
% Looking for CSA axiom ... mLENTr:
% CSA axiom mLENTr found
% Looking for CSA axiom ... mDivLE:
% CSA axiom mDivLE found
% ---- Iteration 3 (6 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... m_MulUnit:
% CSA axiom m_MulUnit found
% Looking for CSA axiom ... mIH_03:
% CSA axiom mIH_03 found
% Looking for CSA axiom ... mDefDiv:
% CSA axiom mDefDiv found
% ---- Iteration 4 (9 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... m_MulZero:
% CSA axiom m_MulZero found
% Looking for CSA axiom ... mMulCanc:
% CSA axiom mMulCanc found
% Looking for CSA axiom ... mZeroMul:
% CSA axiom mZeroMul found
% ---- Iteration 5 (12 axioms selected)
% Looking for TBU SAT ...
% no
% Looking for TBU UNS ...
% yes - theorem proved
% ---- Selection completed
% Selected axioms are ... :mZeroMul:mMulCanc:m_MulZero:mDefDiv:mIH_03:m_MulUnit:mDivLE:mLENTr:mDefPrime:mDivTrans:mSortsC_01:mSortsC (12)
% Unselected axioms are ... :m_AddZero:mZeroAdd:mDivSum:mDivMin:mDefQuot:mDivAsso:mNatSort:mSortsB:mSortsB_02:mAddComm:mAddAsso:mMulComm:mMulAsso:mAddCanc:mLERefl:mLEAsym:mLETran:mLETotal:mIH:mMonMul:mMonMul2:mAMDistr:mDefLE:mMonAdd:mDefDiff (25)
% SZS status THM for /tmp/SystemOnTPTP29432/NUM481+1.tptp
% Looking for THM ...
% found
% SZS output start Solution for /tmp/SystemOnTPTP29432/NUM481+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=600 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 600s
% TreeLimitedRun: WC time limit is 1200s
% TreeLimitedRun: PID is 31617
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Preprocessing time : 0.014 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(3, axiom,![X1]:(aNaturalNumber0(X1)=>(sdtasdt0(X1,sz00)=sz00&sz00=sdtasdt0(sz00,X1))),file('/tmp/SRASS.s.p', m_MulZero)).
% fof(4, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>(doDivides0(X1,X2)<=>?[X3]:(aNaturalNumber0(X3)&X2=sdtasdt0(X1,X3)))),file('/tmp/SRASS.s.p', mDefDiv)).
% fof(5, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>((~(X1=X2)&sdtlseqdt0(X1,X2))=>iLess0(X1,X2))),file('/tmp/SRASS.s.p', mIH_03)).
% fof(6, axiom,![X1]:(aNaturalNumber0(X1)=>(sdtasdt0(X1,sz10)=X1&X1=sdtasdt0(sz10,X1))),file('/tmp/SRASS.s.p', m_MulUnit)).
% fof(7, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>((doDivides0(X1,X2)&~(X2=sz00))=>sdtlseqdt0(X1,X2))),file('/tmp/SRASS.s.p', mDivLE)).
% fof(9, 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(10, axiom,![X1]:![X2]:![X3]:(((aNaturalNumber0(X1)&aNaturalNumber0(X2))&aNaturalNumber0(X3))=>((doDivides0(X1,X2)&doDivides0(X2,X3))=>doDivides0(X1,X3))),file('/tmp/SRASS.s.p', mDivTrans)).
% fof(11, axiom,(aNaturalNumber0(sz10)&~(sz10=sz00)),file('/tmp/SRASS.s.p', mSortsC_01)).
% fof(12, axiom,aNaturalNumber0(sz00),file('/tmp/SRASS.s.p', mSortsC)).
% fof(13, conjecture,![X1]:(((aNaturalNumber0(X1)&~(X1=sz00))&~(X1=sz10))=>(![X2]:(((aNaturalNumber0(X2)&~(X2=sz00))&~(X2=sz10))=>(iLess0(X2,X1)=>?[X3]:((aNaturalNumber0(X3)&doDivides0(X3,X2))&isPrime0(X3))))=>?[X2]:((aNaturalNumber0(X2)&doDivides0(X2,X1))&isPrime0(X2)))),file('/tmp/SRASS.s.p', m__)).
% fof(14, negated_conjecture,~(![X1]:(((aNaturalNumber0(X1)&~(X1=sz00))&~(X1=sz10))=>(![X2]:(((aNaturalNumber0(X2)&~(X2=sz00))&~(X2=sz10))=>(iLess0(X2,X1)=>?[X3]:((aNaturalNumber0(X3)&doDivides0(X3,X2))&isPrime0(X3))))=>?[X2]:((aNaturalNumber0(X2)&doDivides0(X2,X1))&isPrime0(X2))))),inference(assume_negation,[status(cth)],[13])).
% fof(24, plain,![X1]:(~(aNaturalNumber0(X1))|(sdtasdt0(X1,sz00)=sz00&sz00=sdtasdt0(sz00,X1))),inference(fof_nnf,[status(thm)],[3])).
% fof(25, plain,![X2]:(~(aNaturalNumber0(X2))|(sdtasdt0(X2,sz00)=sz00&sz00=sdtasdt0(sz00,X2))),inference(variable_rename,[status(thm)],[24])).
% fof(26, plain,![X2]:((sdtasdt0(X2,sz00)=sz00|~(aNaturalNumber0(X2)))&(sz00=sdtasdt0(sz00,X2)|~(aNaturalNumber0(X2)))),inference(distribute,[status(thm)],[25])).
% cnf(27,plain,(sz00=sdtasdt0(sz00,X1)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[26])).
% cnf(28,plain,(sdtasdt0(X1,sz00)=sz00|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[26])).
% fof(29, 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)],[4])).
% fof(30, 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)],[29])).
% fof(31, plain,![X4]:![X5]:((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|((~(doDivides0(X4,X5))|(aNaturalNumber0(esk1_2(X4,X5))&X5=sdtasdt0(X4,esk1_2(X4,X5))))&(![X7]:(~(aNaturalNumber0(X7))|~(X5=sdtasdt0(X4,X7)))|doDivides0(X4,X5)))),inference(skolemize,[status(esa)],[30])).
% fof(32, plain,![X4]:![X5]:![X7]:((((~(aNaturalNumber0(X7))|~(X5=sdtasdt0(X4,X7)))|doDivides0(X4,X5))&(~(doDivides0(X4,X5))|(aNaturalNumber0(esk1_2(X4,X5))&X5=sdtasdt0(X4,esk1_2(X4,X5)))))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))),inference(shift_quantors,[status(thm)],[31])).
% fof(33, plain,![X4]:![X5]:![X7]:((((~(aNaturalNumber0(X7))|~(X5=sdtasdt0(X4,X7)))|doDivides0(X4,X5))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5))))&(((aNaturalNumber0(esk1_2(X4,X5))|~(doDivides0(X4,X5)))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5))))&((X5=sdtasdt0(X4,esk1_2(X4,X5))|~(doDivides0(X4,X5)))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))))),inference(distribute,[status(thm)],[32])).
% cnf(34,plain,(X1=sdtasdt0(X2,esk1_2(X2,X1))|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~doDivides0(X2,X1)),inference(split_conjunct,[status(thm)],[33])).
% cnf(35,plain,(aNaturalNumber0(esk1_2(X2,X1))|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~doDivides0(X2,X1)),inference(split_conjunct,[status(thm)],[33])).
% cnf(36,plain,(doDivides0(X2,X1)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|X1!=sdtasdt0(X2,X3)|~aNaturalNumber0(X3)),inference(split_conjunct,[status(thm)],[33])).
% fof(37, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|((X1=X2|~(sdtlseqdt0(X1,X2)))|iLess0(X1,X2))),inference(fof_nnf,[status(thm)],[5])).
% fof(38, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|((X3=X4|~(sdtlseqdt0(X3,X4)))|iLess0(X3,X4))),inference(variable_rename,[status(thm)],[37])).
% cnf(39,plain,(iLess0(X1,X2)|X1=X2|~sdtlseqdt0(X1,X2)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[38])).
% fof(40, plain,![X1]:(~(aNaturalNumber0(X1))|(sdtasdt0(X1,sz10)=X1&X1=sdtasdt0(sz10,X1))),inference(fof_nnf,[status(thm)],[6])).
% fof(41, plain,![X2]:(~(aNaturalNumber0(X2))|(sdtasdt0(X2,sz10)=X2&X2=sdtasdt0(sz10,X2))),inference(variable_rename,[status(thm)],[40])).
% fof(42, plain,![X2]:((sdtasdt0(X2,sz10)=X2|~(aNaturalNumber0(X2)))&(X2=sdtasdt0(sz10,X2)|~(aNaturalNumber0(X2)))),inference(distribute,[status(thm)],[41])).
% cnf(44,plain,(sdtasdt0(X1,sz10)=X1|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[42])).
% fof(45, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|((~(doDivides0(X1,X2))|X2=sz00)|sdtlseqdt0(X1,X2))),inference(fof_nnf,[status(thm)],[7])).
% fof(46, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|((~(doDivides0(X3,X4))|X4=sz00)|sdtlseqdt0(X3,X4))),inference(variable_rename,[status(thm)],[45])).
% cnf(47,plain,(sdtlseqdt0(X1,X2)|X2=sz00|~doDivides0(X1,X2)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[46])).
% fof(53, 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)],[9])).
% fof(54, 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)],[53])).
% fof(55, 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(esk2_1(X3))&doDivides0(esk2_1(X3),X3))&(~(esk2_1(X3)=sz10)&~(esk2_1(X3)=X3))))|isPrime0(X3)))),inference(skolemize,[status(esa)],[54])).
% fof(56, plain,![X3]:![X4]:((((((~(aNaturalNumber0(X4))|~(doDivides0(X4,X3)))|(X4=sz10|X4=X3))&(~(X3=sz00)&~(X3=sz10)))|~(isPrime0(X3)))&(((X3=sz00|X3=sz10)|((aNaturalNumber0(esk2_1(X3))&doDivides0(esk2_1(X3),X3))&(~(esk2_1(X3)=sz10)&~(esk2_1(X3)=X3))))|isPrime0(X3)))|~(aNaturalNumber0(X3))),inference(shift_quantors,[status(thm)],[55])).
% fof(57, 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(esk2_1(X3))|(X3=sz00|X3=sz10))|isPrime0(X3))|~(aNaturalNumber0(X3)))&(((doDivides0(esk2_1(X3),X3)|(X3=sz00|X3=sz10))|isPrime0(X3))|~(aNaturalNumber0(X3))))&((((~(esk2_1(X3)=sz10)|(X3=sz00|X3=sz10))|isPrime0(X3))|~(aNaturalNumber0(X3)))&(((~(esk2_1(X3)=X3)|(X3=sz00|X3=sz10))|isPrime0(X3))|~(aNaturalNumber0(X3)))))),inference(distribute,[status(thm)],[56])).
% cnf(58,plain,(isPrime0(X1)|X1=sz10|X1=sz00|~aNaturalNumber0(X1)|esk2_1(X1)!=X1),inference(split_conjunct,[status(thm)],[57])).
% cnf(59,plain,(isPrime0(X1)|X1=sz10|X1=sz00|~aNaturalNumber0(X1)|esk2_1(X1)!=sz10),inference(split_conjunct,[status(thm)],[57])).
% cnf(60,plain,(isPrime0(X1)|X1=sz10|X1=sz00|doDivides0(esk2_1(X1),X1)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[57])).
% cnf(61,plain,(isPrime0(X1)|X1=sz10|X1=sz00|aNaturalNumber0(esk2_1(X1))|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[57])).
% fof(65, plain,![X1]:![X2]:![X3]:(((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|~(aNaturalNumber0(X3)))|((~(doDivides0(X1,X2))|~(doDivides0(X2,X3)))|doDivides0(X1,X3))),inference(fof_nnf,[status(thm)],[10])).
% fof(66, plain,![X4]:![X5]:![X6]:(((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|~(aNaturalNumber0(X6)))|((~(doDivides0(X4,X5))|~(doDivides0(X5,X6)))|doDivides0(X4,X6))),inference(variable_rename,[status(thm)],[65])).
% cnf(67,plain,(doDivides0(X1,X2)|~doDivides0(X3,X2)|~doDivides0(X1,X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X3)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[66])).
% cnf(69,plain,(aNaturalNumber0(sz10)),inference(split_conjunct,[status(thm)],[11])).
% cnf(70,plain,(aNaturalNumber0(sz00)),inference(split_conjunct,[status(thm)],[12])).
% fof(71, negated_conjecture,?[X1]:(((aNaturalNumber0(X1)&~(X1=sz00))&~(X1=sz10))&(![X2]:(((~(aNaturalNumber0(X2))|X2=sz00)|X2=sz10)|(~(iLess0(X2,X1))|?[X3]:((aNaturalNumber0(X3)&doDivides0(X3,X2))&isPrime0(X3))))&![X2]:((~(aNaturalNumber0(X2))|~(doDivides0(X2,X1)))|~(isPrime0(X2))))),inference(fof_nnf,[status(thm)],[14])).
% fof(72, negated_conjecture,?[X4]:(((aNaturalNumber0(X4)&~(X4=sz00))&~(X4=sz10))&(![X5]:(((~(aNaturalNumber0(X5))|X5=sz00)|X5=sz10)|(~(iLess0(X5,X4))|?[X6]:((aNaturalNumber0(X6)&doDivides0(X6,X5))&isPrime0(X6))))&![X7]:((~(aNaturalNumber0(X7))|~(doDivides0(X7,X4)))|~(isPrime0(X7))))),inference(variable_rename,[status(thm)],[71])).
% fof(73, negated_conjecture,(((aNaturalNumber0(esk3_0)&~(esk3_0=sz00))&~(esk3_0=sz10))&(![X5]:(((~(aNaturalNumber0(X5))|X5=sz00)|X5=sz10)|(~(iLess0(X5,esk3_0))|((aNaturalNumber0(esk4_1(X5))&doDivides0(esk4_1(X5),X5))&isPrime0(esk4_1(X5)))))&![X7]:((~(aNaturalNumber0(X7))|~(doDivides0(X7,esk3_0)))|~(isPrime0(X7))))),inference(skolemize,[status(esa)],[72])).
% fof(74, negated_conjecture,![X5]:![X7]:((((~(aNaturalNumber0(X7))|~(doDivides0(X7,esk3_0)))|~(isPrime0(X7)))&(((~(aNaturalNumber0(X5))|X5=sz00)|X5=sz10)|(~(iLess0(X5,esk3_0))|((aNaturalNumber0(esk4_1(X5))&doDivides0(esk4_1(X5),X5))&isPrime0(esk4_1(X5))))))&((aNaturalNumber0(esk3_0)&~(esk3_0=sz00))&~(esk3_0=sz10))),inference(shift_quantors,[status(thm)],[73])).
% fof(75, negated_conjecture,![X5]:![X7]:((((~(aNaturalNumber0(X7))|~(doDivides0(X7,esk3_0)))|~(isPrime0(X7)))&((((aNaturalNumber0(esk4_1(X5))|~(iLess0(X5,esk3_0)))|((~(aNaturalNumber0(X5))|X5=sz00)|X5=sz10))&((doDivides0(esk4_1(X5),X5)|~(iLess0(X5,esk3_0)))|((~(aNaturalNumber0(X5))|X5=sz00)|X5=sz10)))&((isPrime0(esk4_1(X5))|~(iLess0(X5,esk3_0)))|((~(aNaturalNumber0(X5))|X5=sz00)|X5=sz10))))&((aNaturalNumber0(esk3_0)&~(esk3_0=sz00))&~(esk3_0=sz10))),inference(distribute,[status(thm)],[74])).
% cnf(76,negated_conjecture,(esk3_0!=sz10),inference(split_conjunct,[status(thm)],[75])).
% cnf(77,negated_conjecture,(esk3_0!=sz00),inference(split_conjunct,[status(thm)],[75])).
% cnf(78,negated_conjecture,(aNaturalNumber0(esk3_0)),inference(split_conjunct,[status(thm)],[75])).
% cnf(79,negated_conjecture,(X1=sz10|X1=sz00|isPrime0(esk4_1(X1))|~aNaturalNumber0(X1)|~iLess0(X1,esk3_0)),inference(split_conjunct,[status(thm)],[75])).
% cnf(80,negated_conjecture,(X1=sz10|X1=sz00|doDivides0(esk4_1(X1),X1)|~aNaturalNumber0(X1)|~iLess0(X1,esk3_0)),inference(split_conjunct,[status(thm)],[75])).
% cnf(81,negated_conjecture,(X1=sz10|X1=sz00|aNaturalNumber0(esk4_1(X1))|~aNaturalNumber0(X1)|~iLess0(X1,esk3_0)),inference(split_conjunct,[status(thm)],[75])).
% cnf(82,negated_conjecture,(~isPrime0(X1)|~doDivides0(X1,esk3_0)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[75])).
% cnf(85,negated_conjecture,(sz00=X1|sz10=X1|~doDivides0(esk4_1(X1),esk3_0)|~aNaturalNumber0(esk4_1(X1))|~iLess0(X1,esk3_0)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[82,79,theory(equality)])).
% cnf(95,plain,(X1=X2|iLess0(X1,X2)|sz00=X2|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)|~doDivides0(X1,X2)),inference(spm,[status(thm)],[39,47,theory(equality)])).
% cnf(99,plain,(doDivides0(X1,X2)|sz00=X2|sz10=X2|isPrime0(X2)|~doDivides0(X1,esk2_1(X2))|~aNaturalNumber0(esk2_1(X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[67,60,theory(equality)])).
% cnf(100,plain,(doDivides0(X1,sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(sdtasdt0(X1,X2))),inference(er,[status(thm)],[36,theory(equality)])).
% cnf(103,plain,(doDivides0(X1,X2)|X1!=X2|~aNaturalNumber0(sz10)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(spm,[status(thm)],[36,44,theory(equality)])).
% cnf(104,plain,(doDivides0(X1,X2)|sz00!=X2|~aNaturalNumber0(sz00)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(spm,[status(thm)],[36,28,theory(equality)])).
% cnf(110,plain,(doDivides0(X1,X2)|X1!=X2|$false|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(rw,[status(thm)],[103,69,theory(equality)])).
% cnf(111,plain,(doDivides0(X1,X2)|X1!=X2|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(cn,[status(thm)],[110,theory(equality)])).
% cnf(112,plain,(doDivides0(X1,X1)|~aNaturalNumber0(X1)),inference(er,[status(thm)],[111,theory(equality)])).
% cnf(113,plain,(doDivides0(X1,X2)|sz00!=X2|$false|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(rw,[status(thm)],[104,70,theory(equality)])).
% cnf(114,plain,(doDivides0(X1,X2)|sz00!=X2|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(cn,[status(thm)],[113,theory(equality)])).
% cnf(116,plain,(X1=sz00|~aNaturalNumber0(esk1_2(sz00,X1))|~doDivides0(sz00,X1)|~aNaturalNumber0(sz00)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[27,34,theory(equality)])).
% cnf(121,plain,(X1=sz00|~aNaturalNumber0(esk1_2(sz00,X1))|~doDivides0(sz00,X1)|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[116,70,theory(equality)])).
% cnf(122,plain,(X1=sz00|~aNaturalNumber0(esk1_2(sz00,X1))|~doDivides0(sz00,X1)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[121,theory(equality)])).
% cnf(206,negated_conjecture,(sz00=X1|sz10=X1|~iLess0(X1,esk3_0)|~doDivides0(esk4_1(X1),esk3_0)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[85,81])).
% cnf(250,plain,(X1=sz00|~doDivides0(sz00,X1)|~aNaturalNumber0(X1)|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[122,35,theory(equality)])).
% cnf(251,plain,(X1=sz00|~doDivides0(sz00,X1)|~aNaturalNumber0(X1)|$false),inference(rw,[status(thm)],[250,70,theory(equality)])).
% cnf(252,plain,(X1=sz00|~doDivides0(sz00,X1)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[251,theory(equality)])).
% cnf(292,plain,(doDivides0(X1,sdtasdt0(X2,X3))|~doDivides0(X1,X2)|~aNaturalNumber0(X2)|~aNaturalNumber0(sdtasdt0(X2,X3))|~aNaturalNumber0(X1)|~aNaturalNumber0(X3)),inference(spm,[status(thm)],[67,100,theory(equality)])).
% cnf(355,plain,(sz00=X2|sz10=X2|isPrime0(X2)|doDivides0(X1,X2)|~doDivides0(X1,esk2_1(X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[99,61])).
% cnf(356,plain,(sz10=X2|isPrime0(X2)|doDivides0(X1,X2)|~doDivides0(X1,esk2_1(X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[355,114])).
% cnf(357,negated_conjecture,(sz10=X1|isPrime0(X1)|doDivides0(esk4_1(esk2_1(X1)),X1)|sz00=esk2_1(X1)|sz10=esk2_1(X1)|~aNaturalNumber0(X1)|~aNaturalNumber0(esk4_1(esk2_1(X1)))|~iLess0(esk2_1(X1),esk3_0)|~aNaturalNumber0(esk2_1(X1))),inference(spm,[status(thm)],[356,80,theory(equality)])).
% cnf(394,plain,(sdtasdt0(X1,X2)=sz00|~aNaturalNumber0(sdtasdt0(X1,X2))|~doDivides0(sz00,X1)|~aNaturalNumber0(X1)|~aNaturalNumber0(sz00)|~aNaturalNumber0(X2)),inference(spm,[status(thm)],[252,292,theory(equality)])).
% cnf(402,plain,(sdtasdt0(X1,X2)=sz00|~aNaturalNumber0(sdtasdt0(X1,X2))|~doDivides0(sz00,X1)|~aNaturalNumber0(X1)|$false|~aNaturalNumber0(X2)),inference(rw,[status(thm)],[394,70,theory(equality)])).
% cnf(403,plain,(sdtasdt0(X1,X2)=sz00|~aNaturalNumber0(sdtasdt0(X1,X2))|~doDivides0(sz00,X1)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(cn,[status(thm)],[402,theory(equality)])).
% cnf(439,plain,(X2=sz00|~doDivides0(sz00,X1)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(esk1_2(X1,X2))|~doDivides0(X1,X2)),inference(spm,[status(thm)],[403,34,theory(equality)])).
% cnf(452,plain,(X2=sz00|~doDivides0(sz00,X1)|~doDivides0(X1,X2)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[439,35])).
% cnf(456,plain,(X1=sz00|~doDivides0(X2,X1)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|sz00!=X2|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[452,114,theory(equality)])).
% cnf(466,plain,(X1=sz00|~doDivides0(X2,X1)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|sz00!=X2|$false),inference(rw,[status(thm)],[456,70,theory(equality)])).
% cnf(467,plain,(X1=sz00|~doDivides0(X2,X1)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|sz00!=X2),inference(cn,[status(thm)],[466,theory(equality)])).
% cnf(489,plain,(X1=sz00|sz10=X1|isPrime0(X1)|sz00!=esk2_1(X1)|~aNaturalNumber0(X1)|~aNaturalNumber0(esk2_1(X1))),inference(spm,[status(thm)],[467,60,theory(equality)])).
% cnf(503,plain,(X1=sz00|sz10=X1|isPrime0(X1)|esk2_1(X1)!=sz00|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[489,61])).
% cnf(831,negated_conjecture,(esk2_1(X1)=sz00|esk2_1(X1)=sz10|sz10=X1|isPrime0(X1)|doDivides0(esk4_1(esk2_1(X1)),X1)|~iLess0(esk2_1(X1),esk3_0)|~aNaturalNumber0(esk2_1(X1))|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[357,81])).
% cnf(838,negated_conjecture,(sz10=esk2_1(esk3_0)|sz00=esk2_1(esk3_0)|sz10=esk3_0|isPrime0(esk3_0)|~iLess0(esk2_1(esk3_0),esk3_0)|~aNaturalNumber0(esk2_1(esk3_0))|~aNaturalNumber0(esk3_0)),inference(spm,[status(thm)],[206,831,theory(equality)])).
% cnf(839,negated_conjecture,(sz10=esk2_1(esk3_0)|sz00=esk2_1(esk3_0)|sz10=esk3_0|isPrime0(esk3_0)|~iLess0(esk2_1(esk3_0),esk3_0)|~aNaturalNumber0(esk2_1(esk3_0))|$false),inference(rw,[status(thm)],[838,78,theory(equality)])).
% cnf(840,negated_conjecture,(sz10=esk2_1(esk3_0)|sz00=esk2_1(esk3_0)|sz10=esk3_0|isPrime0(esk3_0)|~iLess0(esk2_1(esk3_0),esk3_0)|~aNaturalNumber0(esk2_1(esk3_0))),inference(cn,[status(thm)],[839,theory(equality)])).
% cnf(841,negated_conjecture,(esk2_1(esk3_0)=sz10|esk2_1(esk3_0)=sz00|isPrime0(esk3_0)|~iLess0(esk2_1(esk3_0),esk3_0)|~aNaturalNumber0(esk2_1(esk3_0))),inference(sr,[status(thm)],[840,76,theory(equality)])).
% cnf(842,negated_conjecture,(esk2_1(esk3_0)=sz00|esk2_1(esk3_0)=sz10|isPrime0(esk3_0)|sz00=esk3_0|esk2_1(esk3_0)=esk3_0|~aNaturalNumber0(esk2_1(esk3_0))|~doDivides0(esk2_1(esk3_0),esk3_0)|~aNaturalNumber0(esk3_0)),inference(spm,[status(thm)],[841,95,theory(equality)])).
% cnf(843,negated_conjecture,(esk2_1(esk3_0)=sz00|esk2_1(esk3_0)=sz10|isPrime0(esk3_0)|sz00=esk3_0|esk2_1(esk3_0)=esk3_0|~aNaturalNumber0(esk2_1(esk3_0))|~doDivides0(esk2_1(esk3_0),esk3_0)|$false),inference(rw,[status(thm)],[842,78,theory(equality)])).
% cnf(844,negated_conjecture,(esk2_1(esk3_0)=sz00|esk2_1(esk3_0)=sz10|isPrime0(esk3_0)|sz00=esk3_0|esk2_1(esk3_0)=esk3_0|~aNaturalNumber0(esk2_1(esk3_0))|~doDivides0(esk2_1(esk3_0),esk3_0)),inference(cn,[status(thm)],[843,theory(equality)])).
% cnf(845,negated_conjecture,(esk2_1(esk3_0)=sz00|esk2_1(esk3_0)=sz10|isPrime0(esk3_0)|esk2_1(esk3_0)=esk3_0|~aNaturalNumber0(esk2_1(esk3_0))|~doDivides0(esk2_1(esk3_0),esk3_0)),inference(sr,[status(thm)],[844,77,theory(equality)])).
% cnf(847,negated_conjecture,(esk2_1(esk3_0)=esk3_0|esk2_1(esk3_0)=sz10|esk2_1(esk3_0)=sz00|isPrime0(esk3_0)|sz00=esk3_0|sz10=esk3_0|~aNaturalNumber0(esk2_1(esk3_0))|~aNaturalNumber0(esk3_0)),inference(spm,[status(thm)],[845,60,theory(equality)])).
% cnf(851,negated_conjecture,(esk2_1(esk3_0)=esk3_0|esk2_1(esk3_0)=sz10|esk2_1(esk3_0)=sz00|isPrime0(esk3_0)|sz00=esk3_0|sz10=esk3_0|~aNaturalNumber0(esk2_1(esk3_0))|$false),inference(rw,[status(thm)],[847,78,theory(equality)])).
% cnf(852,negated_conjecture,(esk2_1(esk3_0)=esk3_0|esk2_1(esk3_0)=sz10|esk2_1(esk3_0)=sz00|isPrime0(esk3_0)|sz00=esk3_0|sz10=esk3_0|~aNaturalNumber0(esk2_1(esk3_0))),inference(cn,[status(thm)],[851,theory(equality)])).
% cnf(853,negated_conjecture,(esk2_1(esk3_0)=esk3_0|esk2_1(esk3_0)=sz10|esk2_1(esk3_0)=sz00|isPrime0(esk3_0)|esk3_0=sz10|~aNaturalNumber0(esk2_1(esk3_0))),inference(sr,[status(thm)],[852,77,theory(equality)])).
% cnf(854,negated_conjecture,(esk2_1(esk3_0)=esk3_0|esk2_1(esk3_0)=sz10|esk2_1(esk3_0)=sz00|isPrime0(esk3_0)|~aNaturalNumber0(esk2_1(esk3_0))),inference(sr,[status(thm)],[853,76,theory(equality)])).
% cnf(858,negated_conjecture,(esk2_1(esk3_0)=sz00|esk2_1(esk3_0)=sz10|esk2_1(esk3_0)=esk3_0|isPrime0(esk3_0)|sz00=esk3_0|sz10=esk3_0|~aNaturalNumber0(esk3_0)),inference(spm,[status(thm)],[854,61,theory(equality)])).
% cnf(859,negated_conjecture,(esk2_1(esk3_0)=sz00|esk2_1(esk3_0)=sz10|esk2_1(esk3_0)=esk3_0|isPrime0(esk3_0)|sz00=esk3_0|sz10=esk3_0|$false),inference(rw,[status(thm)],[858,78,theory(equality)])).
% cnf(860,negated_conjecture,(esk2_1(esk3_0)=sz00|esk2_1(esk3_0)=sz10|esk2_1(esk3_0)=esk3_0|isPrime0(esk3_0)|sz00=esk3_0|sz10=esk3_0),inference(cn,[status(thm)],[859,theory(equality)])).
% cnf(861,negated_conjecture,(esk2_1(esk3_0)=sz00|esk2_1(esk3_0)=sz10|esk2_1(esk3_0)=esk3_0|isPrime0(esk3_0)|esk3_0=sz10),inference(sr,[status(thm)],[860,77,theory(equality)])).
% cnf(862,negated_conjecture,(esk2_1(esk3_0)=sz00|esk2_1(esk3_0)=sz10|esk2_1(esk3_0)=esk3_0|isPrime0(esk3_0)),inference(sr,[status(thm)],[861,76,theory(equality)])).
% cnf(866,negated_conjecture,(sz00=esk3_0|sz10=esk3_0|isPrime0(esk3_0)|esk2_1(esk3_0)=sz10|esk2_1(esk3_0)=sz00|~aNaturalNumber0(esk3_0)),inference(spm,[status(thm)],[58,862,theory(equality)])).
% cnf(879,negated_conjecture,(sz00=esk3_0|sz10=esk3_0|isPrime0(esk3_0)|esk2_1(esk3_0)=sz10|esk2_1(esk3_0)=sz00|$false),inference(rw,[status(thm)],[866,78,theory(equality)])).
% cnf(880,negated_conjecture,(sz00=esk3_0|sz10=esk3_0|isPrime0(esk3_0)|esk2_1(esk3_0)=sz10|esk2_1(esk3_0)=sz00),inference(cn,[status(thm)],[879,theory(equality)])).
% cnf(881,negated_conjecture,(esk3_0=sz10|isPrime0(esk3_0)|esk2_1(esk3_0)=sz10|esk2_1(esk3_0)=sz00),inference(sr,[status(thm)],[880,77,theory(equality)])).
% cnf(882,negated_conjecture,(isPrime0(esk3_0)|esk2_1(esk3_0)=sz10|esk2_1(esk3_0)=sz00),inference(sr,[status(thm)],[881,76,theory(equality)])).
% cnf(915,negated_conjecture,(sz00=esk3_0|sz10=esk3_0|isPrime0(esk3_0)|esk2_1(esk3_0)=sz00|~aNaturalNumber0(esk3_0)),inference(spm,[status(thm)],[59,882,theory(equality)])).
% cnf(925,negated_conjecture,(sz00=esk3_0|sz10=esk3_0|isPrime0(esk3_0)|esk2_1(esk3_0)=sz00|$false),inference(rw,[status(thm)],[915,78,theory(equality)])).
% cnf(926,negated_conjecture,(sz00=esk3_0|sz10=esk3_0|isPrime0(esk3_0)|esk2_1(esk3_0)=sz00),inference(cn,[status(thm)],[925,theory(equality)])).
% cnf(927,negated_conjecture,(esk3_0=sz10|isPrime0(esk3_0)|esk2_1(esk3_0)=sz00),inference(sr,[status(thm)],[926,77,theory(equality)])).
% cnf(928,negated_conjecture,(isPrime0(esk3_0)|esk2_1(esk3_0)=sz00),inference(sr,[status(thm)],[927,76,theory(equality)])).
% cnf(968,negated_conjecture,(sz10=esk3_0|esk3_0=sz00|isPrime0(esk3_0)|~aNaturalNumber0(esk3_0)),inference(spm,[status(thm)],[503,928,theory(equality)])).
% cnf(997,negated_conjecture,(sz10=esk3_0|esk3_0=sz00|isPrime0(esk3_0)|$false),inference(rw,[status(thm)],[968,78,theory(equality)])).
% cnf(998,negated_conjecture,(sz10=esk3_0|esk3_0=sz00|isPrime0(esk3_0)),inference(cn,[status(thm)],[997,theory(equality)])).
% cnf(999,negated_conjecture,(esk3_0=sz00|isPrime0(esk3_0)),inference(sr,[status(thm)],[998,76,theory(equality)])).
% cnf(1000,negated_conjecture,(isPrime0(esk3_0)),inference(sr,[status(thm)],[999,77,theory(equality)])).
% cnf(1007,negated_conjecture,(~doDivides0(esk3_0,esk3_0)|~aNaturalNumber0(esk3_0)),inference(spm,[status(thm)],[82,1000,theory(equality)])).
% cnf(1013,negated_conjecture,(~doDivides0(esk3_0,esk3_0)|$false),inference(rw,[status(thm)],[1007,78,theory(equality)])).
% cnf(1014,negated_conjecture,(~doDivides0(esk3_0,esk3_0)),inference(cn,[status(thm)],[1013,theory(equality)])).
% cnf(1016,negated_conjecture,(~aNaturalNumber0(esk3_0)),inference(spm,[status(thm)],[1014,112,theory(equality)])).
% cnf(1019,negated_conjecture,($false),inference(rw,[status(thm)],[1016,78,theory(equality)])).
% cnf(1020,negated_conjecture,($false),inference(cn,[status(thm)],[1019,theory(equality)])).
% cnf(1021,negated_conjecture,($false),1020,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 265
% # ...of these trivial : 0
% # ...subsumed : 121
% # ...remaining for further processing: 144
% # Other redundant clauses eliminated : 11
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 14
% # Backward-rewritten : 2
% # Generated clauses : 353
% # ...of the previous two non-trivial : 287
% # Contextual simplify-reflections : 136
% # Paramodulations : 332
% # Factorizations : 3
% # Equation resolutions : 18
% # Current number of processed clauses: 97
% # Positive orientable unit clauses: 5
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 5
% # Non-unit-clauses : 87
% # Current number of unprocessed clauses: 48
% # ...number of literals in the above : 435
% # Clause-clause subsumption calls (NU) : 1932
% # Rec. Clause-clause subsumption calls : 695
% # Unit Clause-clause subsumption calls : 2
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 2
% # Indexed BW rewrite successes : 2
% # Backwards rewriting index: 66 leaves, 1.38+/-0.966 terms/leaf
% # Paramod-from index: 33 leaves, 1.09+/-0.287 terms/leaf
% # Paramod-into index: 59 leaves, 1.27+/-0.777 terms/leaf
% # -------------------------------------------------
% # User time : 0.043 s
% # System time : 0.004 s
% # Total time : 0.047 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.17 CPU 0.28 WC
% FINAL PrfWatch: 0.17 CPU 0.28 WC
% SZS output end Solution for /tmp/SystemOnTPTP29432/NUM481+1.tptp
%
%------------------------------------------------------------------------------