%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NUM529+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:55:44 EST 2010
% Result : Theorem 3.74s
% Output : Solution 3.74s
% 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/SystemOnTPTP17699/NUM529+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP17699/NUM529+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP17699/NUM529+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 17795
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% # Preprocessing time : 0.020 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 1.93 CPU 2.03 WC
% # SZS output start CNFRefutation.
% fof(1, axiom,aNaturalNumber0(sz00),file('/tmp/SRASS.s.p', mSortsC)).
% fof(2, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>aNaturalNumber0(sdtasdt0(X1,X2))),file('/tmp/SRASS.s.p', mSortsB_02)).
% fof(3, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>sdtasdt0(X1,X2)=sdtasdt0(X2,X1)),file('/tmp/SRASS.s.p', mMulComm)).
% fof(4, 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(5, axiom,![X1]:(aNaturalNumber0(X1)=>(sdtasdt0(X1,sz00)=sz00&sz00=sdtasdt0(sz00,X1))),file('/tmp/SRASS.s.p', m_MulZero)).
% fof(6, 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(7, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>(sdtasdt0(X1,X2)=sz00=>(X1=sz00|X2=sz00))),file('/tmp/SRASS.s.p', mZeroMul)).
% fof(8, axiom,![X1]:(aNaturalNumber0(X1)=>sdtlseqdt0(X1,X1)),file('/tmp/SRASS.s.p', mLERefl)).
% fof(9, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>((sdtlseqdt0(X1,X2)&sdtlseqdt0(X2,X1))=>X1=X2)),file('/tmp/SRASS.s.p', mLEAsym)).
% fof(10, axiom,![X1]:![X2]:![X3]:(((aNaturalNumber0(X1)&aNaturalNumber0(X2))&aNaturalNumber0(X3))=>((sdtlseqdt0(X1,X2)&sdtlseqdt0(X2,X3))=>sdtlseqdt0(X1,X3))),file('/tmp/SRASS.s.p', mLETran)).
% fof(13, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>(~(X1=sz00)=>sdtlseqdt0(X2,sdtasdt0(X2,X1)))),file('/tmp/SRASS.s.p', mMonMul2)).
% fof(14, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>((~(X1=X2)&sdtlseqdt0(X1,X2))=>iLess0(X1,X2))),file('/tmp/SRASS.s.p', mIH_03)).
% fof(15, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>(doDivides0(X1,X2)<=>?[X3]:(aNaturalNumber0(X3)&X2=sdtasdt0(X1,X3)))),file('/tmp/SRASS.s.p', mDefDiv)).
% fof(16, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>((~(X1=sz00)&doDivides0(X1,X2))=>![X3]:(X3=sdtsldt0(X2,X1)<=>(aNaturalNumber0(X3)&X2=sdtasdt0(X1,X3))))),file('/tmp/SRASS.s.p', mDefQuot)).
% fof(17, 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(18, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>((doDivides0(X1,X2)&~(X2=sz00))=>sdtlseqdt0(X1,X2))),file('/tmp/SRASS.s.p', mDivLE)).
% fof(19, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>((~(X1=sz00)&doDivides0(X1,X2))=>![X3]:(aNaturalNumber0(X3)=>sdtasdt0(X3,sdtsldt0(X2,X1))=sdtsldt0(sdtasdt0(X3,X2),X1)))),file('/tmp/SRASS.s.p', mDivAsso)).
% fof(20, axiom,![X1]:![X2]:![X3]:(((aNaturalNumber0(X1)&aNaturalNumber0(X2))&aNaturalNumber0(X3))=>((isPrime0(X3)&doDivides0(X3,sdtasdt0(X1,X2)))=>(doDivides0(X3,X1)|doDivides0(X3,X2)))),file('/tmp/SRASS.s.p', mPDP)).
% fof(21, axiom,(((((aNaturalNumber0(xn)&aNaturalNumber0(xm))&aNaturalNumber0(xp))&~(xn=sz00))&~(xm=sz00))&~(xp=sz00)),file('/tmp/SRASS.s.p', m__2987)).
% fof(22, axiom,![X1]:![X2]:![X3]:((((((aNaturalNumber0(X1)&aNaturalNumber0(X2))&aNaturalNumber0(X3))&~(X1=sz00))&~(X2=sz00))&~(X3=sz00))=>(sdtasdt0(X3,sdtasdt0(X2,X2))=sdtasdt0(X1,X1)=>(iLess0(X1,xn)=>~(isPrime0(X3))))),file('/tmp/SRASS.s.p', m__2963)).
% fof(23, axiom,sdtasdt0(xp,sdtasdt0(xm,xm))=sdtasdt0(xn,xn),file('/tmp/SRASS.s.p', m__3014)).
% fof(24, axiom,isPrime0(xp),file('/tmp/SRASS.s.p', m__3025)).
% fof(25, axiom,(doDivides0(xp,sdtasdt0(xn,xn))&doDivides0(xp,xn)),file('/tmp/SRASS.s.p', m__3046)).
% fof(26, axiom,xq=sdtsldt0(xn,xp),file('/tmp/SRASS.s.p', m__3059)).
% fof(27, axiom,sdtasdt0(xm,xm)=sdtasdt0(xp,sdtasdt0(xq,xq)),file('/tmp/SRASS.s.p', m__3082)).
% fof(28, axiom,(~(xm=xn)&sdtlseqdt0(xm,xn)),file('/tmp/SRASS.s.p', m__3124)).
% fof(29, 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(32, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>(sdtlseqdt0(X1,X2)<=>?[X3]:(aNaturalNumber0(X3)&sdtpldt0(X1,X3)=X2))),file('/tmp/SRASS.s.p', mDefLE)).
% fof(35, axiom,![X1]:(aNaturalNumber0(X1)=>(sdtpldt0(X1,sz00)=X1&X1=sdtpldt0(sz00,X1))),file('/tmp/SRASS.s.p', m_AddZero)).
% fof(38, 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(39, axiom,(aNaturalNumber0(sz10)&~(sz10=sz00)),file('/tmp/SRASS.s.p', mSortsC_01)).
% fof(40, axiom,![X1]:(aNaturalNumber0(X1)=>(sdtasdt0(X1,sz10)=X1&X1=sdtasdt0(sz10,X1))),file('/tmp/SRASS.s.p', m_MulUnit)).
% fof(42, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>aNaturalNumber0(sdtpldt0(X1,X2))),file('/tmp/SRASS.s.p', mSortsB)).
% fof(43, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>sdtpldt0(X1,X2)=sdtpldt0(X2,X1)),file('/tmp/SRASS.s.p', mAddComm)).
% fof(45, axiom,![X1]:![X2]:![X3]:(((aNaturalNumber0(X1)&aNaturalNumber0(X2))&aNaturalNumber0(X3))=>((sdtpldt0(X1,X2)=sdtpldt0(X1,X3)|sdtpldt0(X2,X1)=sdtpldt0(X3,X1))=>X2=X3)),file('/tmp/SRASS.s.p', mAddCanc)).
% fof(47, 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(50, plain,![X1]:![X2]:![X3]:((((((aNaturalNumber0(X1)&aNaturalNumber0(X2))&aNaturalNumber0(X3))&~(X1=sz00))&~(X2=sz00))&~(X3=sz00))=>(sdtasdt0(X3,sdtasdt0(X2,X2))=sdtasdt0(X1,X1)=>(iLess0(X1,xn)=>~(isPrime0(X3))))),inference(fof_simplification,[status(thm)],[22,theory(equality)])).
% cnf(54,plain,(aNaturalNumber0(sz00)),inference(split_conjunct,[status(thm)],[1])).
% fof(55, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|aNaturalNumber0(sdtasdt0(X1,X2))),inference(fof_nnf,[status(thm)],[2])).
% fof(56, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|aNaturalNumber0(sdtasdt0(X3,X4))),inference(variable_rename,[status(thm)],[55])).
% cnf(57,plain,(aNaturalNumber0(sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[56])).
% fof(58, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|sdtasdt0(X1,X2)=sdtasdt0(X2,X1)),inference(fof_nnf,[status(thm)],[3])).
% fof(59, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|sdtasdt0(X3,X4)=sdtasdt0(X4,X3)),inference(variable_rename,[status(thm)],[58])).
% cnf(60,plain,(sdtasdt0(X1,X2)=sdtasdt0(X2,X1)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[59])).
% fof(61, 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)],[4])).
% fof(62, 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)],[61])).
% cnf(63,plain,(sdtasdt0(sdtasdt0(X1,X2),X3)=sdtasdt0(X1,sdtasdt0(X2,X3))|~aNaturalNumber0(X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[62])).
% fof(64, plain,![X1]:(~(aNaturalNumber0(X1))|(sdtasdt0(X1,sz00)=sz00&sz00=sdtasdt0(sz00,X1))),inference(fof_nnf,[status(thm)],[5])).
% fof(65, plain,![X2]:(~(aNaturalNumber0(X2))|(sdtasdt0(X2,sz00)=sz00&sz00=sdtasdt0(sz00,X2))),inference(variable_rename,[status(thm)],[64])).
% fof(66, plain,![X2]:((sdtasdt0(X2,sz00)=sz00|~(aNaturalNumber0(X2)))&(sz00=sdtasdt0(sz00,X2)|~(aNaturalNumber0(X2)))),inference(distribute,[status(thm)],[65])).
% cnf(67,plain,(sz00=sdtasdt0(sz00,X1)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[66])).
% fof(69, 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)],[6])).
% fof(70, 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)],[69])).
% fof(71, 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)],[70])).
% fof(72, 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)],[71])).
% cnf(73,plain,(X1=sz00|X3=X2|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~aNaturalNumber0(X3)|sdtasdt0(X3,X1)!=sdtasdt0(X2,X1)),inference(split_conjunct,[status(thm)],[72])).
% cnf(74,plain,(X1=sz00|X3=X2|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~aNaturalNumber0(X3)|sdtasdt0(X1,X3)!=sdtasdt0(X1,X2)),inference(split_conjunct,[status(thm)],[72])).
% fof(75, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|(~(sdtasdt0(X1,X2)=sz00)|(X1=sz00|X2=sz00))),inference(fof_nnf,[status(thm)],[7])).
% fof(76, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|(~(sdtasdt0(X3,X4)=sz00)|(X3=sz00|X4=sz00))),inference(variable_rename,[status(thm)],[75])).
% cnf(77,plain,(X1=sz00|X2=sz00|sdtasdt0(X2,X1)!=sz00|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(split_conjunct,[status(thm)],[76])).
% fof(78, plain,![X1]:(~(aNaturalNumber0(X1))|sdtlseqdt0(X1,X1)),inference(fof_nnf,[status(thm)],[8])).
% fof(79, plain,![X2]:(~(aNaturalNumber0(X2))|sdtlseqdt0(X2,X2)),inference(variable_rename,[status(thm)],[78])).
% cnf(80,plain,(sdtlseqdt0(X1,X1)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[79])).
% fof(81, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|((~(sdtlseqdt0(X1,X2))|~(sdtlseqdt0(X2,X1)))|X1=X2)),inference(fof_nnf,[status(thm)],[9])).
% fof(82, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|((~(sdtlseqdt0(X3,X4))|~(sdtlseqdt0(X4,X3)))|X3=X4)),inference(variable_rename,[status(thm)],[81])).
% cnf(83,plain,(X1=X2|~sdtlseqdt0(X2,X1)|~sdtlseqdt0(X1,X2)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[82])).
% fof(84, plain,![X1]:![X2]:![X3]:(((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|~(aNaturalNumber0(X3)))|((~(sdtlseqdt0(X1,X2))|~(sdtlseqdt0(X2,X3)))|sdtlseqdt0(X1,X3))),inference(fof_nnf,[status(thm)],[10])).
% fof(85, plain,![X4]:![X5]:![X6]:(((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|~(aNaturalNumber0(X6)))|((~(sdtlseqdt0(X4,X5))|~(sdtlseqdt0(X5,X6)))|sdtlseqdt0(X4,X6))),inference(variable_rename,[status(thm)],[84])).
% cnf(86,plain,(sdtlseqdt0(X1,X2)|~sdtlseqdt0(X3,X2)|~sdtlseqdt0(X1,X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X3)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[85])).
% fof(99, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|(X1=sz00|sdtlseqdt0(X2,sdtasdt0(X2,X1)))),inference(fof_nnf,[status(thm)],[13])).
% fof(100, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|(X3=sz00|sdtlseqdt0(X4,sdtasdt0(X4,X3)))),inference(variable_rename,[status(thm)],[99])).
% cnf(101,plain,(sdtlseqdt0(X1,sdtasdt0(X1,X2))|X2=sz00|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(split_conjunct,[status(thm)],[100])).
% fof(102, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|((X1=X2|~(sdtlseqdt0(X1,X2)))|iLess0(X1,X2))),inference(fof_nnf,[status(thm)],[14])).
% fof(103, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|((X3=X4|~(sdtlseqdt0(X3,X4)))|iLess0(X3,X4))),inference(variable_rename,[status(thm)],[102])).
% cnf(104,plain,(iLess0(X1,X2)|X1=X2|~sdtlseqdt0(X1,X2)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[103])).
% fof(105, 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)],[15])).
% fof(106, 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)],[105])).
% fof(107, 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)],[106])).
% fof(108, 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)],[107])).
% fof(109, 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)],[108])).
% cnf(110,plain,(X1=sdtasdt0(X2,esk1_2(X2,X1))|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~doDivides0(X2,X1)),inference(split_conjunct,[status(thm)],[109])).
% cnf(111,plain,(aNaturalNumber0(esk1_2(X2,X1))|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~doDivides0(X2,X1)),inference(split_conjunct,[status(thm)],[109])).
% cnf(112,plain,(doDivides0(X2,X1)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|X1!=sdtasdt0(X2,X3)|~aNaturalNumber0(X3)),inference(split_conjunct,[status(thm)],[109])).
% fof(113, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|((X1=sz00|~(doDivides0(X1,X2)))|![X3]:((~(X3=sdtsldt0(X2,X1))|(aNaturalNumber0(X3)&X2=sdtasdt0(X1,X3)))&((~(aNaturalNumber0(X3))|~(X2=sdtasdt0(X1,X3)))|X3=sdtsldt0(X2,X1))))),inference(fof_nnf,[status(thm)],[16])).
% fof(114, plain,![X4]:![X5]:((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|((X4=sz00|~(doDivides0(X4,X5)))|![X6]:((~(X6=sdtsldt0(X5,X4))|(aNaturalNumber0(X6)&X5=sdtasdt0(X4,X6)))&((~(aNaturalNumber0(X6))|~(X5=sdtasdt0(X4,X6)))|X6=sdtsldt0(X5,X4))))),inference(variable_rename,[status(thm)],[113])).
% fof(115, plain,![X4]:![X5]:![X6]:((((~(X6=sdtsldt0(X5,X4))|(aNaturalNumber0(X6)&X5=sdtasdt0(X4,X6)))&((~(aNaturalNumber0(X6))|~(X5=sdtasdt0(X4,X6)))|X6=sdtsldt0(X5,X4)))|(X4=sz00|~(doDivides0(X4,X5))))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))),inference(shift_quantors,[status(thm)],[114])).
% fof(116, plain,![X4]:![X5]:![X6]:(((((aNaturalNumber0(X6)|~(X6=sdtsldt0(X5,X4)))|(X4=sz00|~(doDivides0(X4,X5))))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5))))&(((X5=sdtasdt0(X4,X6)|~(X6=sdtsldt0(X5,X4)))|(X4=sz00|~(doDivides0(X4,X5))))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))))&((((~(aNaturalNumber0(X6))|~(X5=sdtasdt0(X4,X6)))|X6=sdtsldt0(X5,X4))|(X4=sz00|~(doDivides0(X4,X5))))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5))))),inference(distribute,[status(thm)],[115])).
% cnf(117,plain,(X2=sz00|X3=sdtsldt0(X1,X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~doDivides0(X2,X1)|X1!=sdtasdt0(X2,X3)|~aNaturalNumber0(X3)),inference(split_conjunct,[status(thm)],[116])).
% cnf(118,plain,(X2=sz00|X1=sdtasdt0(X2,X3)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~doDivides0(X2,X1)|X3!=sdtsldt0(X1,X2)),inference(split_conjunct,[status(thm)],[116])).
% cnf(119,plain,(X2=sz00|aNaturalNumber0(X3)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~doDivides0(X2,X1)|X3!=sdtsldt0(X1,X2)),inference(split_conjunct,[status(thm)],[116])).
% fof(120, plain,![X1]:![X2]:![X3]:(((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|~(aNaturalNumber0(X3)))|((~(doDivides0(X1,X2))|~(doDivides0(X2,X3)))|doDivides0(X1,X3))),inference(fof_nnf,[status(thm)],[17])).
% fof(121, plain,![X4]:![X5]:![X6]:(((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|~(aNaturalNumber0(X6)))|((~(doDivides0(X4,X5))|~(doDivides0(X5,X6)))|doDivides0(X4,X6))),inference(variable_rename,[status(thm)],[120])).
% cnf(122,plain,(doDivides0(X1,X2)|~doDivides0(X3,X2)|~doDivides0(X1,X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X3)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[121])).
% fof(123, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|((~(doDivides0(X1,X2))|X2=sz00)|sdtlseqdt0(X1,X2))),inference(fof_nnf,[status(thm)],[18])).
% fof(124, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|((~(doDivides0(X3,X4))|X4=sz00)|sdtlseqdt0(X3,X4))),inference(variable_rename,[status(thm)],[123])).
% cnf(125,plain,(sdtlseqdt0(X1,X2)|X2=sz00|~doDivides0(X1,X2)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[124])).
% fof(126, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|((X1=sz00|~(doDivides0(X1,X2)))|![X3]:(~(aNaturalNumber0(X3))|sdtasdt0(X3,sdtsldt0(X2,X1))=sdtsldt0(sdtasdt0(X3,X2),X1)))),inference(fof_nnf,[status(thm)],[19])).
% fof(127, plain,![X4]:![X5]:((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|((X4=sz00|~(doDivides0(X4,X5)))|![X6]:(~(aNaturalNumber0(X6))|sdtasdt0(X6,sdtsldt0(X5,X4))=sdtsldt0(sdtasdt0(X6,X5),X4)))),inference(variable_rename,[status(thm)],[126])).
% fof(128, plain,![X4]:![X5]:![X6]:(((~(aNaturalNumber0(X6))|sdtasdt0(X6,sdtsldt0(X5,X4))=sdtsldt0(sdtasdt0(X6,X5),X4))|(X4=sz00|~(doDivides0(X4,X5))))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))),inference(shift_quantors,[status(thm)],[127])).
% cnf(129,plain,(X2=sz00|sdtasdt0(X3,sdtsldt0(X1,X2))=sdtsldt0(sdtasdt0(X3,X1),X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~doDivides0(X2,X1)|~aNaturalNumber0(X3)),inference(split_conjunct,[status(thm)],[128])).
% fof(130, plain,![X1]:![X2]:![X3]:(((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|~(aNaturalNumber0(X3)))|((~(isPrime0(X3))|~(doDivides0(X3,sdtasdt0(X1,X2))))|(doDivides0(X3,X1)|doDivides0(X3,X2)))),inference(fof_nnf,[status(thm)],[20])).
% fof(131, plain,![X4]:![X5]:![X6]:(((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|~(aNaturalNumber0(X6)))|((~(isPrime0(X6))|~(doDivides0(X6,sdtasdt0(X4,X5))))|(doDivides0(X6,X4)|doDivides0(X6,X5)))),inference(variable_rename,[status(thm)],[130])).
% cnf(132,plain,(doDivides0(X1,X2)|doDivides0(X1,X3)|~doDivides0(X1,sdtasdt0(X3,X2))|~isPrime0(X1)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~aNaturalNumber0(X3)),inference(split_conjunct,[status(thm)],[131])).
% cnf(133,plain,(xp!=sz00),inference(split_conjunct,[status(thm)],[21])).
% cnf(134,plain,(xm!=sz00),inference(split_conjunct,[status(thm)],[21])).
% cnf(135,plain,(xn!=sz00),inference(split_conjunct,[status(thm)],[21])).
% cnf(136,plain,(aNaturalNumber0(xp)),inference(split_conjunct,[status(thm)],[21])).
% cnf(137,plain,(aNaturalNumber0(xm)),inference(split_conjunct,[status(thm)],[21])).
% cnf(138,plain,(aNaturalNumber0(xn)),inference(split_conjunct,[status(thm)],[21])).
% fof(139, plain,![X1]:![X2]:![X3]:((((((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|~(aNaturalNumber0(X3)))|X1=sz00)|X2=sz00)|X3=sz00)|(~(sdtasdt0(X3,sdtasdt0(X2,X2))=sdtasdt0(X1,X1))|(~(iLess0(X1,xn))|~(isPrime0(X3))))),inference(fof_nnf,[status(thm)],[50])).
% fof(140, plain,![X4]:![X5]:![X6]:((((((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|~(aNaturalNumber0(X6)))|X4=sz00)|X5=sz00)|X6=sz00)|(~(sdtasdt0(X6,sdtasdt0(X5,X5))=sdtasdt0(X4,X4))|(~(iLess0(X4,xn))|~(isPrime0(X6))))),inference(variable_rename,[status(thm)],[139])).
% cnf(141,plain,(X1=sz00|X3=sz00|X2=sz00|~isPrime0(X1)|~iLess0(X2,xn)|sdtasdt0(X1,sdtasdt0(X3,X3))!=sdtasdt0(X2,X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(X3)|~aNaturalNumber0(X2)),inference(split_conjunct,[status(thm)],[140])).
% cnf(142,plain,(sdtasdt0(xp,sdtasdt0(xm,xm))=sdtasdt0(xn,xn)),inference(split_conjunct,[status(thm)],[23])).
% cnf(143,plain,(isPrime0(xp)),inference(split_conjunct,[status(thm)],[24])).
% cnf(144,plain,(doDivides0(xp,xn)),inference(split_conjunct,[status(thm)],[25])).
% cnf(145,plain,(doDivides0(xp,sdtasdt0(xn,xn))),inference(split_conjunct,[status(thm)],[25])).
% cnf(146,plain,(xq=sdtsldt0(xn,xp)),inference(split_conjunct,[status(thm)],[26])).
% cnf(147,plain,(sdtasdt0(xm,xm)=sdtasdt0(xp,sdtasdt0(xq,xq))),inference(split_conjunct,[status(thm)],[27])).
% cnf(148,plain,(sdtlseqdt0(xm,xn)),inference(split_conjunct,[status(thm)],[28])).
% cnf(149,plain,(xm!=xn),inference(split_conjunct,[status(thm)],[28])).
% fof(150, 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)],[29])).
% fof(151, 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)],[150])).
% fof(152, 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)],[151])).
% fof(153, 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)],[152])).
% fof(154, 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)],[153])).
% cnf(160,plain,(~aNaturalNumber0(X1)|~isPrime0(X1)|X1!=sz00),inference(split_conjunct,[status(thm)],[154])).
% fof(174, 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)],[32])).
% fof(175, 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)],[174])).
% fof(176, plain,![X4]:![X5]:((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|((~(sdtlseqdt0(X4,X5))|(aNaturalNumber0(esk4_2(X4,X5))&sdtpldt0(X4,esk4_2(X4,X5))=X5))&(![X7]:(~(aNaturalNumber0(X7))|~(sdtpldt0(X4,X7)=X5))|sdtlseqdt0(X4,X5)))),inference(skolemize,[status(esa)],[175])).
% fof(177, plain,![X4]:![X5]:![X7]:((((~(aNaturalNumber0(X7))|~(sdtpldt0(X4,X7)=X5))|sdtlseqdt0(X4,X5))&(~(sdtlseqdt0(X4,X5))|(aNaturalNumber0(esk4_2(X4,X5))&sdtpldt0(X4,esk4_2(X4,X5))=X5)))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))),inference(shift_quantors,[status(thm)],[176])).
% fof(178, plain,![X4]:![X5]:![X7]:((((~(aNaturalNumber0(X7))|~(sdtpldt0(X4,X7)=X5))|sdtlseqdt0(X4,X5))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5))))&(((aNaturalNumber0(esk4_2(X4,X5))|~(sdtlseqdt0(X4,X5)))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5))))&((sdtpldt0(X4,esk4_2(X4,X5))=X5|~(sdtlseqdt0(X4,X5)))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))))),inference(distribute,[status(thm)],[177])).
% cnf(179,plain,(sdtpldt0(X2,esk4_2(X2,X1))=X1|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~sdtlseqdt0(X2,X1)),inference(split_conjunct,[status(thm)],[178])).
% cnf(180,plain,(aNaturalNumber0(esk4_2(X2,X1))|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~sdtlseqdt0(X2,X1)),inference(split_conjunct,[status(thm)],[178])).
% cnf(181,plain,(sdtlseqdt0(X2,X1)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|sdtpldt0(X2,X3)!=X1|~aNaturalNumber0(X3)),inference(split_conjunct,[status(thm)],[178])).
% fof(195, plain,![X1]:(~(aNaturalNumber0(X1))|(sdtpldt0(X1,sz00)=X1&X1=sdtpldt0(sz00,X1))),inference(fof_nnf,[status(thm)],[35])).
% fof(196, plain,![X2]:(~(aNaturalNumber0(X2))|(sdtpldt0(X2,sz00)=X2&X2=sdtpldt0(sz00,X2))),inference(variable_rename,[status(thm)],[195])).
% fof(197, plain,![X2]:((sdtpldt0(X2,sz00)=X2|~(aNaturalNumber0(X2)))&(X2=sdtpldt0(sz00,X2)|~(aNaturalNumber0(X2)))),inference(distribute,[status(thm)],[196])).
% cnf(198,plain,(X1=sdtpldt0(sz00,X1)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[197])).
% cnf(199,plain,(sdtpldt0(X1,sz00)=X1|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[197])).
% fof(208, 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)],[38])).
% fof(209, 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)],[208])).
% cnf(210,plain,(doDivides0(X1,X2)|~doDivides0(X1,sdtpldt0(X3,X2))|~doDivides0(X1,X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X3)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[209])).
% cnf(211,plain,(sz10!=sz00),inference(split_conjunct,[status(thm)],[39])).
% cnf(212,plain,(aNaturalNumber0(sz10)),inference(split_conjunct,[status(thm)],[39])).
% fof(213, plain,![X1]:(~(aNaturalNumber0(X1))|(sdtasdt0(X1,sz10)=X1&X1=sdtasdt0(sz10,X1))),inference(fof_nnf,[status(thm)],[40])).
% fof(214, plain,![X2]:(~(aNaturalNumber0(X2))|(sdtasdt0(X2,sz10)=X2&X2=sdtasdt0(sz10,X2))),inference(variable_rename,[status(thm)],[213])).
% fof(215, plain,![X2]:((sdtasdt0(X2,sz10)=X2|~(aNaturalNumber0(X2)))&(X2=sdtasdt0(sz10,X2)|~(aNaturalNumber0(X2)))),inference(distribute,[status(thm)],[214])).
% cnf(216,plain,(X1=sdtasdt0(sz10,X1)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[215])).
% cnf(217,plain,(sdtasdt0(X1,sz10)=X1|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[215])).
% fof(220, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|aNaturalNumber0(sdtpldt0(X1,X2))),inference(fof_nnf,[status(thm)],[42])).
% fof(221, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|aNaturalNumber0(sdtpldt0(X3,X4))),inference(variable_rename,[status(thm)],[220])).
% cnf(222,plain,(aNaturalNumber0(sdtpldt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[221])).
% fof(223, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|sdtpldt0(X1,X2)=sdtpldt0(X2,X1)),inference(fof_nnf,[status(thm)],[43])).
% fof(224, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|sdtpldt0(X3,X4)=sdtpldt0(X4,X3)),inference(variable_rename,[status(thm)],[223])).
% cnf(225,plain,(sdtpldt0(X1,X2)=sdtpldt0(X2,X1)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[224])).
% fof(229, plain,![X1]:![X2]:![X3]:(((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|~(aNaturalNumber0(X3)))|((~(sdtpldt0(X1,X2)=sdtpldt0(X1,X3))&~(sdtpldt0(X2,X1)=sdtpldt0(X3,X1)))|X2=X3)),inference(fof_nnf,[status(thm)],[45])).
% fof(230, plain,![X4]:![X5]:![X6]:(((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|~(aNaturalNumber0(X6)))|((~(sdtpldt0(X4,X5)=sdtpldt0(X4,X6))&~(sdtpldt0(X5,X4)=sdtpldt0(X6,X4)))|X5=X6)),inference(variable_rename,[status(thm)],[229])).
% fof(231, plain,![X4]:![X5]:![X6]:(((~(sdtpldt0(X4,X5)=sdtpldt0(X4,X6))|X5=X6)|((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|~(aNaturalNumber0(X6))))&((~(sdtpldt0(X5,X4)=sdtpldt0(X6,X4))|X5=X6)|((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|~(aNaturalNumber0(X6))))),inference(distribute,[status(thm)],[230])).
% cnf(232,plain,(X2=X1|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~aNaturalNumber0(X3)|sdtpldt0(X2,X3)!=sdtpldt0(X1,X3)),inference(split_conjunct,[status(thm)],[231])).
% cnf(233,plain,(X2=X1|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~aNaturalNumber0(X3)|sdtpldt0(X3,X2)!=sdtpldt0(X3,X1)),inference(split_conjunct,[status(thm)],[231])).
% fof(236, 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)],[47])).
% fof(237, 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)],[236])).
% fof(238, 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)],[237])).
% fof(239, 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)],[238])).
% cnf(240,plain,(X3=sdtmndt0(X1,X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~sdtlseqdt0(X2,X1)|sdtpldt0(X2,X3)!=X1|~aNaturalNumber0(X3)),inference(split_conjunct,[status(thm)],[239])).
% cnf(242,plain,(aNaturalNumber0(X3)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~sdtlseqdt0(X2,X1)|X3!=sdtmndt0(X1,X2)),inference(split_conjunct,[status(thm)],[239])).
% cnf(245,plain,(sdtmndt0(X1,X2)=X3|sdtpldt0(X2,X3)!=X1|~aNaturalNumber0(X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[240,181])).
% cnf(248,plain,(sdtsldt0(X1,X2)=X3|sz00=X2|sdtasdt0(X2,X3)!=X1|~aNaturalNumber0(X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[117,112])).
% cnf(251,plain,(sz00=X3|sz00=X2|sdtasdt0(X1,sdtasdt0(X3,X3))!=sdtasdt0(X2,X2)|~isPrime0(X1)|~iLess0(X2,xn)|~aNaturalNumber0(X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[141,160])).
% cnf(259,plain,(aNaturalNumber0(sdtasdt0(xn,xn))|~aNaturalNumber0(sdtasdt0(xm,xm))|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[57,142,theory(equality)])).
% cnf(265,plain,(aNaturalNumber0(sdtasdt0(xn,xn))|~aNaturalNumber0(sdtasdt0(xm,xm))|$false),inference(rw,[status(thm)],[259,136,theory(equality)])).
% cnf(266,plain,(aNaturalNumber0(sdtasdt0(xn,xn))|~aNaturalNumber0(sdtasdt0(xm,xm))),inference(cn,[status(thm)],[265,theory(equality)])).
% cnf(284,plain,(aNaturalNumber0(sdtasdt0(xm,xm))|~aNaturalNumber0(sdtasdt0(xq,xq))|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[57,147,theory(equality)])).
% cnf(285,plain,(aNaturalNumber0(sdtasdt0(xm,xm))|~aNaturalNumber0(sdtasdt0(xq,xq))|$false),inference(rw,[status(thm)],[284,136,theory(equality)])).
% cnf(286,plain,(aNaturalNumber0(sdtasdt0(xm,xm))|~aNaturalNumber0(sdtasdt0(xq,xq))),inference(cn,[status(thm)],[285,theory(equality)])).
% cnf(357,plain,(xm=xn|iLess0(xm,xn)|~aNaturalNumber0(xn)|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[104,148,theory(equality)])).
% cnf(362,plain,(xm=xn|iLess0(xm,xn)|$false|~aNaturalNumber0(xm)),inference(rw,[status(thm)],[357,138,theory(equality)])).
% cnf(363,plain,(xm=xn|iLess0(xm,xn)|$false|$false),inference(rw,[status(thm)],[362,137,theory(equality)])).
% cnf(364,plain,(xm=xn|iLess0(xm,xn)),inference(cn,[status(thm)],[363,theory(equality)])).
% cnf(365,plain,(iLess0(xm,xn)),inference(sr,[status(thm)],[364,149,theory(equality)])).
% cnf(391,plain,(sz00=xn|sdtlseqdt0(xp,xn)|~aNaturalNumber0(xn)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[125,144,theory(equality)])).
% cnf(393,plain,(sz00=xn|sdtlseqdt0(xp,xn)|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[391,138,theory(equality)])).
% cnf(394,plain,(sz00=xn|sdtlseqdt0(xp,xn)|$false|$false),inference(rw,[status(thm)],[393,136,theory(equality)])).
% cnf(395,plain,(sz00=xn|sdtlseqdt0(xp,xn)),inference(cn,[status(thm)],[394,theory(equality)])).
% cnf(396,plain,(sdtlseqdt0(xp,xn)),inference(sr,[status(thm)],[395,135,theory(equality)])).
% cnf(416,plain,(sz00=X1|sdtlseqdt0(X2,sdtasdt0(X1,X2))|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(spm,[status(thm)],[101,60,theory(equality)])).
% cnf(432,plain,(aNaturalNumber0(esk4_2(X1,X1))|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[180,80,theory(equality)])).
% cnf(454,plain,(sdtpldt0(X1,esk4_2(X1,X1))=X1|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[179,80,theory(equality)])).
% cnf(474,plain,(X1=sz00|sdtpldt0(X2,X1)!=X2|~aNaturalNumber0(X2)|~aNaturalNumber0(sz00)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[233,199,theory(equality)])).
% cnf(483,plain,(X1=sz00|sdtpldt0(X2,X1)!=X2|~aNaturalNumber0(X2)|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[474,54,theory(equality)])).
% cnf(484,plain,(X1=sz00|sdtpldt0(X2,X1)!=X2|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[483,theory(equality)])).
% cnf(506,plain,(sdtlseqdt0(X1,sdtpldt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(sdtpldt0(X1,X2))),inference(er,[status(thm)],[181,theory(equality)])).
% cnf(507,plain,(sdtlseqdt0(sz00,X1)|X2!=X1|~aNaturalNumber0(X2)|~aNaturalNumber0(sz00)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[181,198,theory(equality)])).
% cnf(511,plain,(sdtlseqdt0(sz00,X1)|X2!=X1|~aNaturalNumber0(X2)|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[507,54,theory(equality)])).
% cnf(512,plain,(sdtlseqdt0(sz00,X1)|X2!=X1|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[511,theory(equality)])).
% cnf(513,plain,(sdtlseqdt0(sz00,X1)|~aNaturalNumber0(X1)),inference(er,[status(thm)],[512,theory(equality)])).
% cnf(517,plain,(sdtmndt0(sdtpldt0(X1,X2),X1)=X2|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(sdtpldt0(X1,X2))),inference(er,[status(thm)],[245,theory(equality)])).
% cnf(528,plain,(doDivides0(X1,sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(sdtasdt0(X1,X2))),inference(er,[status(thm)],[112,theory(equality)])).
% cnf(529,plain,(doDivides0(sz10,X1)|X2!=X1|~aNaturalNumber0(X2)|~aNaturalNumber0(sz10)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[112,216,theory(equality)])).
% cnf(530,plain,(doDivides0(xp,X1)|sdtasdt0(xm,xm)!=X1|~aNaturalNumber0(sdtasdt0(xq,xq))|~aNaturalNumber0(xp)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[112,147,theory(equality)])).
% cnf(533,plain,(doDivides0(X1,X2)|X1!=X2|~aNaturalNumber0(sz10)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(spm,[status(thm)],[112,217,theory(equality)])).
% cnf(535,plain,(doDivides0(X1,X2)|sdtasdt0(X3,X1)!=X2|~aNaturalNumber0(X3)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(spm,[status(thm)],[112,60,theory(equality)])).
% cnf(537,plain,(doDivides0(sz10,X1)|X2!=X1|~aNaturalNumber0(X2)|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[529,212,theory(equality)])).
% cnf(538,plain,(doDivides0(sz10,X1)|X2!=X1|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[537,theory(equality)])).
% cnf(539,plain,(doDivides0(sz10,X1)|~aNaturalNumber0(X1)),inference(er,[status(thm)],[538,theory(equality)])).
% cnf(540,plain,(doDivides0(xp,X1)|sdtasdt0(xm,xm)!=X1|~aNaturalNumber0(sdtasdt0(xq,xq))|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[530,136,theory(equality)])).
% cnf(541,plain,(doDivides0(xp,X1)|sdtasdt0(xm,xm)!=X1|~aNaturalNumber0(sdtasdt0(xq,xq))|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[540,theory(equality)])).
% cnf(546,plain,(doDivides0(X1,X2)|X1!=X2|$false|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(rw,[status(thm)],[533,212,theory(equality)])).
% cnf(547,plain,(doDivides0(X1,X2)|X1!=X2|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(cn,[status(thm)],[546,theory(equality)])).
% cnf(548,plain,(doDivides0(X1,X1)|~aNaturalNumber0(X1)),inference(er,[status(thm)],[547,theory(equality)])).
% cnf(600,plain,(sz00=X1|aNaturalNumber0(sdtsldt0(X2,X1))|~doDivides0(X1,X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(er,[status(thm)],[119,theory(equality)])).
% cnf(601,plain,(sz00=xp|aNaturalNumber0(X1)|xq!=X1|~doDivides0(xp,xn)|~aNaturalNumber0(xp)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[119,146,theory(equality)])).
% cnf(602,plain,(sz00=xp|aNaturalNumber0(X1)|xq!=X1|$false|~aNaturalNumber0(xp)|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[601,144,theory(equality)])).
% cnf(603,plain,(sz00=xp|aNaturalNumber0(X1)|xq!=X1|$false|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[602,136,theory(equality)])).
% cnf(604,plain,(sz00=xp|aNaturalNumber0(X1)|xq!=X1|$false|$false|$false),inference(rw,[status(thm)],[603,138,theory(equality)])).
% cnf(605,plain,(sz00=xp|aNaturalNumber0(X1)|xq!=X1),inference(cn,[status(thm)],[604,theory(equality)])).
% cnf(606,plain,(aNaturalNumber0(X1)|xq!=X1),inference(sr,[status(thm)],[605,133,theory(equality)])).
% cnf(610,plain,(sz00=xp|X1=sdtasdt0(xm,xm)|sdtasdt0(xp,X1)!=sdtasdt0(xn,xn)|~aNaturalNumber0(sdtasdt0(xm,xm))|~aNaturalNumber0(X1)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[74,142,theory(equality)])).
% cnf(628,plain,(sz00=xp|X1=sdtasdt0(xm,xm)|sdtasdt0(xp,X1)!=sdtasdt0(xn,xn)|~aNaturalNumber0(sdtasdt0(xm,xm))|~aNaturalNumber0(X1)|$false),inference(rw,[status(thm)],[610,136,theory(equality)])).
% cnf(629,plain,(sz00=xp|X1=sdtasdt0(xm,xm)|sdtasdt0(xp,X1)!=sdtasdt0(xn,xn)|~aNaturalNumber0(sdtasdt0(xm,xm))|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[628,theory(equality)])).
% cnf(630,plain,(X1=sdtasdt0(xm,xm)|sdtasdt0(xp,X1)!=sdtasdt0(xn,xn)|~aNaturalNumber0(sdtasdt0(xm,xm))|~aNaturalNumber0(X1)),inference(sr,[status(thm)],[629,133,theory(equality)])).
% cnf(648,plain,(sdtasdt0(X1,sdtsldt0(X2,X1))=X2|sz00=X1|~doDivides0(X1,X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(er,[status(thm)],[118,theory(equality)])).
% cnf(671,plain,(sdtasdt0(sz00,X2)=sdtasdt0(sz00,sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[63,67,theory(equality)])).
% cnf(686,plain,(sdtasdt0(sz00,X2)=sdtasdt0(sz00,sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)|$false),inference(rw,[status(thm)],[671,54,theory(equality)])).
% cnf(687,plain,(sdtasdt0(sz00,X2)=sdtasdt0(sz00,sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[686,theory(equality)])).
% cnf(692,plain,(sdtsldt0(sdtasdt0(X1,X2),X1)=X2|sz00=X1|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(sdtasdt0(X1,X2))),inference(er,[status(thm)],[248,theory(equality)])).
% cnf(903,plain,(sdtsldt0(sdtasdt0(X1,xn),xp)=sdtasdt0(X1,sdtsldt0(xn,xp))|sz00=xp|~aNaturalNumber0(X1)|~aNaturalNumber0(xp)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[129,144,theory(equality)])).
% cnf(905,plain,(sdtsldt0(sdtasdt0(X1,xn),xp)=sdtasdt0(X1,xq)|sz00=xp|~aNaturalNumber0(X1)|~aNaturalNumber0(xp)|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[903,146,theory(equality)])).
% cnf(906,plain,(sdtsldt0(sdtasdt0(X1,xn),xp)=sdtasdt0(X1,xq)|sz00=xp|~aNaturalNumber0(X1)|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[905,136,theory(equality)])).
% cnf(907,plain,(sdtsldt0(sdtasdt0(X1,xn),xp)=sdtasdt0(X1,xq)|sz00=xp|~aNaturalNumber0(X1)|$false|$false),inference(rw,[status(thm)],[906,138,theory(equality)])).
% cnf(908,plain,(sdtsldt0(sdtasdt0(X1,xn),xp)=sdtasdt0(X1,xq)|sz00=xp|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[907,theory(equality)])).
% cnf(909,plain,(sdtsldt0(sdtasdt0(X1,xn),xp)=sdtasdt0(X1,xq)|~aNaturalNumber0(X1)),inference(sr,[status(thm)],[908,133,theory(equality)])).
% cnf(964,plain,(sz00=X1|sz00=xm|sdtasdt0(X2,sdtasdt0(X1,X1))!=sdtasdt0(xm,xm)|~isPrime0(X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(xm)|~aNaturalNumber0(X2)),inference(spm,[status(thm)],[251,365,theory(equality)])).
% cnf(965,plain,(sz00=X1|sz00=xm|sdtasdt0(X2,sdtasdt0(X1,X1))!=sdtasdt0(xm,xm)|~isPrime0(X2)|~aNaturalNumber0(X1)|$false|~aNaturalNumber0(X2)),inference(rw,[status(thm)],[964,137,theory(equality)])).
% cnf(966,plain,(sz00=X1|sz00=xm|sdtasdt0(X2,sdtasdt0(X1,X1))!=sdtasdt0(xm,xm)|~isPrime0(X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(cn,[status(thm)],[965,theory(equality)])).
% cnf(967,plain,(sz00=X1|sdtasdt0(X2,sdtasdt0(X1,X1))!=sdtasdt0(xm,xm)|~isPrime0(X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(sr,[status(thm)],[966,134,theory(equality)])).
% cnf(974,plain,(sdtlseqdt0(X1,xn)|~sdtlseqdt0(X1,xp)|~aNaturalNumber0(xp)|~aNaturalNumber0(xn)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[86,396,theory(equality)])).
% cnf(995,plain,(sdtlseqdt0(X1,xn)|~sdtlseqdt0(X1,xp)|$false|~aNaturalNumber0(xn)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[974,136,theory(equality)])).
% cnf(996,plain,(sdtlseqdt0(X1,xn)|~sdtlseqdt0(X1,xp)|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[995,138,theory(equality)])).
% cnf(997,plain,(sdtlseqdt0(X1,xn)|~sdtlseqdt0(X1,xp)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[996,theory(equality)])).
% cnf(1010,plain,(aNaturalNumber0(sdtasdt0(xn,xn))|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[266,57,theory(equality)])).
% cnf(1015,plain,(aNaturalNumber0(sdtasdt0(xn,xn))|$false),inference(rw,[status(thm)],[1010,137,theory(equality)])).
% cnf(1016,plain,(aNaturalNumber0(sdtasdt0(xn,xn))),inference(cn,[status(thm)],[1015,theory(equality)])).
% cnf(1017,plain,(aNaturalNumber0(xq)),inference(er,[status(thm)],[606,theory(equality)])).
% cnf(1141,plain,(aNaturalNumber0(sdtasdt0(xm,xm))|~aNaturalNumber0(xq)),inference(spm,[status(thm)],[286,57,theory(equality)])).
% cnf(1146,plain,(aNaturalNumber0(sdtasdt0(xm,xm))|$false),inference(rw,[status(thm)],[1141,1017,theory(equality)])).
% cnf(1147,plain,(aNaturalNumber0(sdtasdt0(xm,xm))),inference(cn,[status(thm)],[1146,theory(equality)])).
% cnf(1360,plain,(sdtlseqdt0(sz00,xn)|~aNaturalNumber0(sz00)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[997,513,theory(equality)])).
% cnf(1368,plain,(sdtlseqdt0(sz00,xn)|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[1360,54,theory(equality)])).
% cnf(1369,plain,(sdtlseqdt0(sz00,xn)|$false|$false),inference(rw,[status(thm)],[1368,136,theory(equality)])).
% cnf(1370,plain,(sdtlseqdt0(sz00,xn)),inference(cn,[status(thm)],[1369,theory(equality)])).
% cnf(1378,plain,(xn=sz00|~sdtlseqdt0(xn,sz00)|~aNaturalNumber0(sz00)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[83,1370,theory(equality)])).
% cnf(1382,plain,(aNaturalNumber0(esk4_2(sz00,xn))|~aNaturalNumber0(sz00)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[180,1370,theory(equality)])).
% cnf(1383,plain,(sdtpldt0(sz00,esk4_2(sz00,xn))=xn|~aNaturalNumber0(sz00)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[179,1370,theory(equality)])).
% cnf(1387,plain,(xn=sz00|~sdtlseqdt0(xn,sz00)|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[1378,54,theory(equality)])).
% cnf(1388,plain,(xn=sz00|~sdtlseqdt0(xn,sz00)|$false|$false),inference(rw,[status(thm)],[1387,138,theory(equality)])).
% cnf(1389,plain,(xn=sz00|~sdtlseqdt0(xn,sz00)),inference(cn,[status(thm)],[1388,theory(equality)])).
% cnf(1390,plain,(~sdtlseqdt0(xn,sz00)),inference(sr,[status(thm)],[1389,135,theory(equality)])).
% cnf(1403,plain,(aNaturalNumber0(esk4_2(sz00,xn))|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[1382,54,theory(equality)])).
% cnf(1404,plain,(aNaturalNumber0(esk4_2(sz00,xn))|$false|$false),inference(rw,[status(thm)],[1403,138,theory(equality)])).
% cnf(1405,plain,(aNaturalNumber0(esk4_2(sz00,xn))),inference(cn,[status(thm)],[1404,theory(equality)])).
% cnf(1406,plain,(sdtpldt0(sz00,esk4_2(sz00,xn))=xn|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[1383,54,theory(equality)])).
% cnf(1407,plain,(sdtpldt0(sz00,esk4_2(sz00,xn))=xn|$false|$false),inference(rw,[status(thm)],[1406,138,theory(equality)])).
% cnf(1408,plain,(sdtpldt0(sz00,esk4_2(sz00,xn))=xn),inference(cn,[status(thm)],[1407,theory(equality)])).
% cnf(1476,plain,(xn=esk4_2(sz00,xn)|~aNaturalNumber0(esk4_2(sz00,xn))),inference(spm,[status(thm)],[198,1408,theory(equality)])).
% cnf(1508,plain,(xn=esk4_2(sz00,xn)|$false),inference(rw,[status(thm)],[1476,1405,theory(equality)])).
% cnf(1509,plain,(xn=esk4_2(sz00,xn)),inference(cn,[status(thm)],[1508,theory(equality)])).
% cnf(1510,plain,(sdtpldt0(sz00,xn)=xn),inference(rw,[status(thm)],[1408,1509,theory(equality)])).
% cnf(1515,plain,(X1=sz00|sdtpldt0(X1,xn)!=xn|~aNaturalNumber0(xn)|~aNaturalNumber0(sz00)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[232,1510,theory(equality)])).
% cnf(1516,plain,(sdtmndt0(X1,sz00)=xn|xn!=X1|~aNaturalNumber0(xn)|~aNaturalNumber0(sz00)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[245,1510,theory(equality)])).
% cnf(1532,plain,(X1=sz00|sdtpldt0(X1,xn)!=xn|$false|~aNaturalNumber0(sz00)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[1515,138,theory(equality)])).
% cnf(1533,plain,(X1=sz00|sdtpldt0(X1,xn)!=xn|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[1532,54,theory(equality)])).
% cnf(1534,plain,(X1=sz00|sdtpldt0(X1,xn)!=xn|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[1533,theory(equality)])).
% cnf(1535,plain,(sdtmndt0(X1,sz00)=xn|xn!=X1|$false|~aNaturalNumber0(sz00)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[1516,138,theory(equality)])).
% cnf(1536,plain,(sdtmndt0(X1,sz00)=xn|xn!=X1|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[1535,54,theory(equality)])).
% cnf(1537,plain,(sdtmndt0(X1,sz00)=xn|xn!=X1|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[1536,theory(equality)])).
% cnf(1594,plain,(X1=sz00|sdtpldt0(xn,X1)!=xn|~aNaturalNumber0(X1)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[1534,225,theory(equality)])).
% cnf(1598,plain,(X1=sz00|sdtpldt0(xn,X1)!=xn|~aNaturalNumber0(X1)|$false),inference(rw,[status(thm)],[1594,138,theory(equality)])).
% cnf(1599,plain,(X1=sz00|sdtpldt0(xn,X1)!=xn|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[1598,theory(equality)])).
% cnf(1602,plain,(sdtmndt0(xn,sz00)=xn|~aNaturalNumber0(xn)),inference(er,[status(thm)],[1537,theory(equality)])).
% cnf(1603,plain,(sdtmndt0(xn,sz00)=xn|$false),inference(rw,[status(thm)],[1602,138,theory(equality)])).
% cnf(1604,plain,(sdtmndt0(xn,sz00)=xn),inference(cn,[status(thm)],[1603,theory(equality)])).
% cnf(1605,plain,(aNaturalNumber0(X1)|xn!=X1|~sdtlseqdt0(sz00,xn)|~aNaturalNumber0(sz00)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[242,1604,theory(equality)])).
% cnf(1607,plain,(aNaturalNumber0(X1)|xn!=X1|$false|~aNaturalNumber0(sz00)|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[1605,1370,theory(equality)])).
% cnf(1608,plain,(aNaturalNumber0(X1)|xn!=X1|$false|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[1607,54,theory(equality)])).
% cnf(1609,plain,(aNaturalNumber0(X1)|xn!=X1|$false|$false|$false),inference(rw,[status(thm)],[1608,138,theory(equality)])).
% cnf(1610,plain,(aNaturalNumber0(X1)|xn!=X1),inference(cn,[status(thm)],[1609,theory(equality)])).
% cnf(1664,plain,(sdtasdt0(X1,esk1_2(X1,X1))=X1|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[110,548,theory(equality)])).
% cnf(2756,plain,(esk4_2(xn,xn)=sz00|~aNaturalNumber0(esk4_2(xn,xn))|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[1599,454,theory(equality)])).
% cnf(2770,plain,(esk4_2(xn,xn)=sz00|~aNaturalNumber0(esk4_2(xn,xn))|$false),inference(rw,[status(thm)],[2756,138,theory(equality)])).
% cnf(2771,plain,(esk4_2(xn,xn)=sz00|~aNaturalNumber0(esk4_2(xn,xn))),inference(cn,[status(thm)],[2770,theory(equality)])).
% cnf(2778,plain,(esk4_2(xn,xn)=sz00|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[2771,432,theory(equality)])).
% cnf(2780,plain,(esk4_2(xn,xn)=sz00|$false),inference(rw,[status(thm)],[2778,138,theory(equality)])).
% cnf(2781,plain,(esk4_2(xn,xn)=sz00),inference(cn,[status(thm)],[2780,theory(equality)])).
% cnf(2786,plain,(sdtpldt0(xn,sz00)=xn|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[454,2781,theory(equality)])).
% cnf(2794,plain,(sdtpldt0(xn,sz00)=xn|$false),inference(rw,[status(thm)],[2786,138,theory(equality)])).
% cnf(2795,plain,(sdtpldt0(xn,sz00)=xn),inference(cn,[status(thm)],[2794,theory(equality)])).
% cnf(2824,plain,(sdtmndt0(X1,xn)=sz00|xn!=X1|~aNaturalNumber0(sz00)|~aNaturalNumber0(xn)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[245,2795,theory(equality)])).
% cnf(2827,plain,(doDivides0(X1,sz00)|~doDivides0(X1,xn)|~aNaturalNumber0(xn)|~aNaturalNumber0(sz00)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[210,2795,theory(equality)])).
% cnf(2828,plain,(sdtlseqdt0(xn,X1)|xn!=X1|~aNaturalNumber0(sz00)|~aNaturalNumber0(xn)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[181,2795,theory(equality)])).
% cnf(2851,plain,(sdtmndt0(X1,xn)=sz00|xn!=X1|$false|~aNaturalNumber0(xn)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[2824,54,theory(equality)])).
% cnf(2852,plain,(sdtmndt0(X1,xn)=sz00|xn!=X1|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[2851,138,theory(equality)])).
% cnf(2853,plain,(sdtmndt0(X1,xn)=sz00|xn!=X1|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[2852,theory(equality)])).
% cnf(2860,plain,(doDivides0(X1,sz00)|~doDivides0(X1,xn)|$false|~aNaturalNumber0(sz00)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[2827,138,theory(equality)])).
% cnf(2861,plain,(doDivides0(X1,sz00)|~doDivides0(X1,xn)|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[2860,54,theory(equality)])).
% cnf(2862,plain,(doDivides0(X1,sz00)|~doDivides0(X1,xn)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[2861,theory(equality)])).
% cnf(2863,plain,(sdtlseqdt0(xn,X1)|xn!=X1|$false|~aNaturalNumber0(xn)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[2828,54,theory(equality)])).
% cnf(2864,plain,(sdtlseqdt0(xn,X1)|xn!=X1|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[2863,138,theory(equality)])).
% cnf(2865,plain,(sdtlseqdt0(xn,X1)|xn!=X1|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[2864,theory(equality)])).
% cnf(2869,plain,(sdtlseqdt0(xn,X1)|xn!=X1),inference(csr,[status(thm)],[2865,1610])).
% cnf(2870,plain,(sdtlseqdt0(xn,xn)),inference(er,[status(thm)],[2869,theory(equality)])).
% cnf(2890,plain,(sdtmndt0(X1,xn)=sz00|xn!=X1),inference(csr,[status(thm)],[2853,1610])).
% cnf(2891,plain,(sdtmndt0(xn,xn)=sz00),inference(er,[status(thm)],[2890,theory(equality)])).
% cnf(2892,plain,(aNaturalNumber0(X1)|sz00!=X1|~sdtlseqdt0(xn,xn)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[242,2891,theory(equality)])).
% cnf(2894,plain,(aNaturalNumber0(X1)|sz00!=X1|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[2892,2870,theory(equality)])).
% cnf(2895,plain,(aNaturalNumber0(X1)|sz00!=X1|$false|$false),inference(rw,[status(thm)],[2894,138,theory(equality)])).
% cnf(2896,plain,(aNaturalNumber0(X1)|sz00!=X1),inference(cn,[status(thm)],[2895,theory(equality)])).
% cnf(2904,plain,(doDivides0(sz10,sz00)|~aNaturalNumber0(sz10)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[2862,539,theory(equality)])).
% cnf(2907,plain,(doDivides0(xn,sz00)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[2862,548,theory(equality)])).
% cnf(2914,plain,(doDivides0(sz10,sz00)|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[2904,212,theory(equality)])).
% cnf(2915,plain,(doDivides0(sz10,sz00)|$false|$false),inference(rw,[status(thm)],[2914,138,theory(equality)])).
% cnf(2916,plain,(doDivides0(sz10,sz00)),inference(cn,[status(thm)],[2915,theory(equality)])).
% cnf(2921,plain,(doDivides0(xn,sz00)|$false),inference(rw,[status(thm)],[2907,138,theory(equality)])).
% cnf(2922,plain,(doDivides0(xn,sz00)),inference(cn,[status(thm)],[2921,theory(equality)])).
% cnf(2967,plain,(aNaturalNumber0(esk1_2(sz10,sz00))|~aNaturalNumber0(sz10)|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[111,2916,theory(equality)])).
% cnf(2968,plain,(sdtasdt0(sz10,esk1_2(sz10,sz00))=sz00|~aNaturalNumber0(sz10)|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[110,2916,theory(equality)])).
% cnf(2972,plain,(aNaturalNumber0(esk1_2(sz10,sz00))|$false|~aNaturalNumber0(sz00)),inference(rw,[status(thm)],[2967,212,theory(equality)])).
% cnf(2973,plain,(aNaturalNumber0(esk1_2(sz10,sz00))|$false|$false),inference(rw,[status(thm)],[2972,54,theory(equality)])).
% cnf(2974,plain,(aNaturalNumber0(esk1_2(sz10,sz00))),inference(cn,[status(thm)],[2973,theory(equality)])).
% cnf(2975,plain,(sdtasdt0(sz10,esk1_2(sz10,sz00))=sz00|$false|~aNaturalNumber0(sz00)),inference(rw,[status(thm)],[2968,212,theory(equality)])).
% cnf(2976,plain,(sdtasdt0(sz10,esk1_2(sz10,sz00))=sz00|$false|$false),inference(rw,[status(thm)],[2975,54,theory(equality)])).
% cnf(2977,plain,(sdtasdt0(sz10,esk1_2(sz10,sz00))=sz00),inference(cn,[status(thm)],[2976,theory(equality)])).
% cnf(3016,plain,(aNaturalNumber0(esk1_2(xn,sz00))|~aNaturalNumber0(xn)|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[111,2922,theory(equality)])).
% cnf(3017,plain,(sdtasdt0(xn,esk1_2(xn,sz00))=sz00|~aNaturalNumber0(xn)|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[110,2922,theory(equality)])).
% cnf(3025,plain,(aNaturalNumber0(esk1_2(xn,sz00))|$false|~aNaturalNumber0(sz00)),inference(rw,[status(thm)],[3016,138,theory(equality)])).
% cnf(3026,plain,(aNaturalNumber0(esk1_2(xn,sz00))|$false|$false),inference(rw,[status(thm)],[3025,54,theory(equality)])).
% cnf(3027,plain,(aNaturalNumber0(esk1_2(xn,sz00))),inference(cn,[status(thm)],[3026,theory(equality)])).
% cnf(3028,plain,(sdtasdt0(xn,esk1_2(xn,sz00))=sz00|$false|~aNaturalNumber0(sz00)),inference(rw,[status(thm)],[3017,138,theory(equality)])).
% cnf(3029,plain,(sdtasdt0(xn,esk1_2(xn,sz00))=sz00|$false|$false),inference(rw,[status(thm)],[3028,54,theory(equality)])).
% cnf(3030,plain,(sdtasdt0(xn,esk1_2(xn,sz00))=sz00),inference(cn,[status(thm)],[3029,theory(equality)])).
% cnf(3082,plain,(sz00=sz10|sz00=esk1_2(sz10,sz00)|~aNaturalNumber0(sz10)|~aNaturalNumber0(esk1_2(sz10,sz00))),inference(spm,[status(thm)],[77,2977,theory(equality)])).
% cnf(3105,plain,(sz00=sz10|sz00=esk1_2(sz10,sz00)|$false|~aNaturalNumber0(esk1_2(sz10,sz00))),inference(rw,[status(thm)],[3082,212,theory(equality)])).
% cnf(3106,plain,(sz00=sz10|sz00=esk1_2(sz10,sz00)|$false|$false),inference(rw,[status(thm)],[3105,2974,theory(equality)])).
% cnf(3107,plain,(sz00=sz10|sz00=esk1_2(sz10,sz00)),inference(cn,[status(thm)],[3106,theory(equality)])).
% cnf(3108,plain,(esk1_2(sz10,sz00)=sz00),inference(sr,[status(thm)],[3107,211,theory(equality)])).
% cnf(3160,plain,(sdtasdt0(sz10,sz00)=sz00),inference(rw,[status(thm)],[2977,3108,theory(equality)])).
% cnf(3165,plain,(sdtasdt0(sz00,sz10)=sz00|~aNaturalNumber0(sz10)|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[60,3160,theory(equality)])).
% cnf(3180,plain,(sdtasdt0(sz00,sz10)=sz00|$false|~aNaturalNumber0(sz00)),inference(rw,[status(thm)],[3165,212,theory(equality)])).
% cnf(3181,plain,(sdtasdt0(sz00,sz10)=sz00|$false|$false),inference(rw,[status(thm)],[3180,54,theory(equality)])).
% cnf(3182,plain,(sdtasdt0(sz00,sz10)=sz00),inference(cn,[status(thm)],[3181,theory(equality)])).
% cnf(3522,plain,(sz00=esk1_2(xn,sz00)|sdtlseqdt0(xn,sz00)|~aNaturalNumber0(esk1_2(xn,sz00))|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[101,3030,theory(equality)])).
% cnf(3540,plain,(sz00=esk1_2(xn,sz00)|sdtlseqdt0(xn,sz00)|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[3522,3027,theory(equality)])).
% cnf(3541,plain,(sz00=esk1_2(xn,sz00)|sdtlseqdt0(xn,sz00)|$false|$false),inference(rw,[status(thm)],[3540,138,theory(equality)])).
% cnf(3542,plain,(sz00=esk1_2(xn,sz00)|sdtlseqdt0(xn,sz00)),inference(cn,[status(thm)],[3541,theory(equality)])).
% cnf(3543,plain,(esk1_2(xn,sz00)=sz00),inference(sr,[status(thm)],[3542,1390,theory(equality)])).
% cnf(3602,plain,(sdtasdt0(xn,sz00)=sz00),inference(rw,[status(thm)],[3030,3543,theory(equality)])).
% cnf(6876,plain,(sdtlseqdt0(X1,sdtpldt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[506,222])).
% cnf(7274,plain,(sdtmndt0(sdtpldt0(X1,X2),X1)=X2|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[517,222])).
% cnf(8016,plain,(doDivides0(X1,sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[528,57])).
% cnf(8206,plain,(doDivides0(xp,X1)|sdtasdt0(xm,xm)!=X1|~aNaturalNumber0(X1)|~aNaturalNumber0(xq)),inference(spm,[status(thm)],[541,57,theory(equality)])).
% cnf(8211,plain,(doDivides0(xp,X1)|sdtasdt0(xm,xm)!=X1|~aNaturalNumber0(X1)|$false),inference(rw,[status(thm)],[8206,1017,theory(equality)])).
% cnf(8212,plain,(doDivides0(xp,X1)|sdtasdt0(xm,xm)!=X1|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[8211,theory(equality)])).
% cnf(8213,plain,(doDivides0(xp,sdtasdt0(xm,xm))|~aNaturalNumber0(sdtasdt0(xm,xm))),inference(er,[status(thm)],[8212,theory(equality)])).
% cnf(8216,plain,(doDivides0(xp,sdtasdt0(xm,xm))|$false),inference(rw,[status(thm)],[8213,1147,theory(equality)])).
% cnf(8217,plain,(doDivides0(xp,sdtasdt0(xm,xm))),inference(cn,[status(thm)],[8216,theory(equality)])).
% cnf(8229,plain,(doDivides0(xp,xm)|~isPrime0(xp)|~aNaturalNumber0(xm)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[132,8217,theory(equality)])).
% cnf(8254,plain,(doDivides0(xp,xm)|$false|~aNaturalNumber0(xm)|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[8229,143,theory(equality)])).
% cnf(8255,plain,(doDivides0(xp,xm)|$false|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[8254,137,theory(equality)])).
% cnf(8256,plain,(doDivides0(xp,xm)|$false|$false|$false),inference(rw,[status(thm)],[8255,136,theory(equality)])).
% cnf(8257,plain,(doDivides0(xp,xm)),inference(cn,[status(thm)],[8256,theory(equality)])).
% cnf(8268,plain,(doDivides0(X1,xm)|~doDivides0(X1,xp)|~aNaturalNumber0(xp)|~aNaturalNumber0(xm)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[122,8257,theory(equality)])).
% cnf(8284,plain,(doDivides0(X1,xm)|~doDivides0(X1,xp)|$false|~aNaturalNumber0(xm)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[8268,136,theory(equality)])).
% cnf(8285,plain,(doDivides0(X1,xm)|~doDivides0(X1,xp)|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[8284,137,theory(equality)])).
% cnf(8286,plain,(doDivides0(X1,xm)|~doDivides0(X1,xp)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[8285,theory(equality)])).
% cnf(8845,plain,(doDivides0(sz10,xm)|~aNaturalNumber0(sz10)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[8286,539,theory(equality)])).
% cnf(8853,plain,(doDivides0(sz10,xm)|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[8845,212,theory(equality)])).
% cnf(8854,plain,(doDivides0(sz10,xm)|$false|$false),inference(rw,[status(thm)],[8853,136,theory(equality)])).
% cnf(8855,plain,(doDivides0(sz10,xm)),inference(cn,[status(thm)],[8854,theory(equality)])).
% cnf(8950,plain,(aNaturalNumber0(esk1_2(sz10,xm))|~aNaturalNumber0(sz10)|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[111,8855,theory(equality)])).
% cnf(8951,plain,(sdtasdt0(sz10,esk1_2(sz10,xm))=xm|~aNaturalNumber0(sz10)|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[110,8855,theory(equality)])).
% cnf(8959,plain,(aNaturalNumber0(esk1_2(sz10,xm))|$false|~aNaturalNumber0(xm)),inference(rw,[status(thm)],[8950,212,theory(equality)])).
% cnf(8960,plain,(aNaturalNumber0(esk1_2(sz10,xm))|$false|$false),inference(rw,[status(thm)],[8959,137,theory(equality)])).
% cnf(8961,plain,(aNaturalNumber0(esk1_2(sz10,xm))),inference(cn,[status(thm)],[8960,theory(equality)])).
% cnf(8962,plain,(sdtasdt0(sz10,esk1_2(sz10,xm))=xm|$false|~aNaturalNumber0(xm)),inference(rw,[status(thm)],[8951,212,theory(equality)])).
% cnf(8963,plain,(sdtasdt0(sz10,esk1_2(sz10,xm))=xm|$false|$false),inference(rw,[status(thm)],[8962,137,theory(equality)])).
% cnf(8964,plain,(sdtasdt0(sz10,esk1_2(sz10,xm))=xm),inference(cn,[status(thm)],[8963,theory(equality)])).
% cnf(9045,plain,(xm=esk1_2(sz10,xm)|~aNaturalNumber0(esk1_2(sz10,xm))),inference(spm,[status(thm)],[216,8964,theory(equality)])).
% cnf(9126,plain,(xm=esk1_2(sz10,xm)|$false),inference(rw,[status(thm)],[9045,8961,theory(equality)])).
% cnf(9127,plain,(xm=esk1_2(sz10,xm)),inference(cn,[status(thm)],[9126,theory(equality)])).
% cnf(9140,plain,(sdtasdt0(sz10,xm)=xm),inference(rw,[status(thm)],[8964,9127,theory(equality)])).
% cnf(9148,plain,(sz00=xm|sz10=X1|xm!=sdtasdt0(X1,xm)|~aNaturalNumber0(X1)|~aNaturalNumber0(sz10)|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[73,9140,theory(equality)])).
% cnf(9158,plain,(sz00=sz10|sdtlseqdt0(xm,xm)|~aNaturalNumber0(sz10)|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[416,9140,theory(equality)])).
% cnf(9164,plain,(doDivides0(xm,X1)|xm!=X1|~aNaturalNumber0(sz10)|~aNaturalNumber0(xm)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[535,9140,theory(equality)])).
% cnf(9177,plain,(sz00=xm|sz10=X1|xm!=sdtasdt0(X1,xm)|~aNaturalNumber0(X1)|$false|~aNaturalNumber0(xm)),inference(rw,[status(thm)],[9148,212,theory(equality)])).
% cnf(9178,plain,(sz00=xm|sz10=X1|xm!=sdtasdt0(X1,xm)|~aNaturalNumber0(X1)|$false|$false),inference(rw,[status(thm)],[9177,137,theory(equality)])).
% cnf(9179,plain,(sz00=xm|sz10=X1|xm!=sdtasdt0(X1,xm)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[9178,theory(equality)])).
% cnf(9180,plain,(sz10=X1|sdtasdt0(X1,xm)!=xm|~aNaturalNumber0(X1)),inference(sr,[status(thm)],[9179,134,theory(equality)])).
% cnf(9213,plain,(sz00=sz10|sdtlseqdt0(xm,xm)|$false|~aNaturalNumber0(xm)),inference(rw,[status(thm)],[9158,212,theory(equality)])).
% cnf(9214,plain,(sz00=sz10|sdtlseqdt0(xm,xm)|$false|$false),inference(rw,[status(thm)],[9213,137,theory(equality)])).
% cnf(9215,plain,(sz00=sz10|sdtlseqdt0(xm,xm)),inference(cn,[status(thm)],[9214,theory(equality)])).
% cnf(9216,plain,(sdtlseqdt0(xm,xm)),inference(sr,[status(thm)],[9215,211,theory(equality)])).
% cnf(9236,plain,(doDivides0(xm,X1)|xm!=X1|$false|~aNaturalNumber0(xm)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[9164,212,theory(equality)])).
% cnf(9237,plain,(doDivides0(xm,X1)|xm!=X1|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[9236,137,theory(equality)])).
% cnf(9238,plain,(doDivides0(xm,X1)|xm!=X1|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[9237,theory(equality)])).
% cnf(9261,plain,(aNaturalNumber0(esk4_2(xm,xm))|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[180,9216,theory(equality)])).
% cnf(9262,plain,(sdtpldt0(xm,esk4_2(xm,xm))=xm|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[179,9216,theory(equality)])).
% cnf(9267,plain,(aNaturalNumber0(esk4_2(xm,xm))|$false),inference(rw,[status(thm)],[9261,137,theory(equality)])).
% cnf(9268,plain,(aNaturalNumber0(esk4_2(xm,xm))),inference(cn,[status(thm)],[9267,theory(equality)])).
% cnf(9269,plain,(sdtpldt0(xm,esk4_2(xm,xm))=xm|$false),inference(rw,[status(thm)],[9262,137,theory(equality)])).
% cnf(9270,plain,(sdtpldt0(xm,esk4_2(xm,xm))=xm),inference(cn,[status(thm)],[9269,theory(equality)])).
% cnf(9510,plain,(esk4_2(xm,xm)=sz00|~aNaturalNumber0(xm)|~aNaturalNumber0(esk4_2(xm,xm))),inference(spm,[status(thm)],[484,9270,theory(equality)])).
% cnf(9531,plain,(esk4_2(xm,xm)=sz00|$false|~aNaturalNumber0(esk4_2(xm,xm))),inference(rw,[status(thm)],[9510,137,theory(equality)])).
% cnf(9532,plain,(esk4_2(xm,xm)=sz00|$false|$false),inference(rw,[status(thm)],[9531,9268,theory(equality)])).
% cnf(9533,plain,(esk4_2(xm,xm)=sz00),inference(cn,[status(thm)],[9532,theory(equality)])).
% cnf(9593,plain,(sdtpldt0(xm,sz00)=xm),inference(rw,[status(thm)],[9270,9533,theory(equality)])).
% cnf(9610,plain,(sdtpldt0(sz00,xm)=xm|~aNaturalNumber0(xm)|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[225,9593,theory(equality)])).
% cnf(9636,plain,(sdtpldt0(sz00,xm)=xm|$false|~aNaturalNumber0(sz00)),inference(rw,[status(thm)],[9610,137,theory(equality)])).
% cnf(9637,plain,(sdtpldt0(sz00,xm)=xm|$false|$false),inference(rw,[status(thm)],[9636,54,theory(equality)])).
% cnf(9638,plain,(sdtpldt0(sz00,xm)=xm),inference(cn,[status(thm)],[9637,theory(equality)])).
% cnf(9713,plain,(sdtlseqdt0(sz00,xm)|~aNaturalNumber0(xm)|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[6876,9638,theory(equality)])).
% cnf(9714,plain,(sdtmndt0(xm,sz00)=xm|~aNaturalNumber0(xm)|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[7274,9638,theory(equality)])).
% cnf(9746,plain,(sdtlseqdt0(sz00,xm)|$false|~aNaturalNumber0(sz00)),inference(rw,[status(thm)],[9713,137,theory(equality)])).
% cnf(9747,plain,(sdtlseqdt0(sz00,xm)|$false|$false),inference(rw,[status(thm)],[9746,54,theory(equality)])).
% cnf(9748,plain,(sdtlseqdt0(sz00,xm)),inference(cn,[status(thm)],[9747,theory(equality)])).
% cnf(9749,plain,(sdtmndt0(xm,sz00)=xm|$false|~aNaturalNumber0(sz00)),inference(rw,[status(thm)],[9714,137,theory(equality)])).
% cnf(9750,plain,(sdtmndt0(xm,sz00)=xm|$false|$false),inference(rw,[status(thm)],[9749,54,theory(equality)])).
% cnf(9751,plain,(sdtmndt0(xm,sz00)=xm),inference(cn,[status(thm)],[9750,theory(equality)])).
% cnf(9799,plain,(xm=sz00|~sdtlseqdt0(xm,sz00)|~aNaturalNumber0(sz00)|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[83,9748,theory(equality)])).
% cnf(9811,plain,(xm=sz00|~sdtlseqdt0(xm,sz00)|$false|~aNaturalNumber0(xm)),inference(rw,[status(thm)],[9799,54,theory(equality)])).
% cnf(9812,plain,(xm=sz00|~sdtlseqdt0(xm,sz00)|$false|$false),inference(rw,[status(thm)],[9811,137,theory(equality)])).
% cnf(9813,plain,(xm=sz00|~sdtlseqdt0(xm,sz00)),inference(cn,[status(thm)],[9812,theory(equality)])).
% cnf(9814,plain,(~sdtlseqdt0(xm,sz00)),inference(sr,[status(thm)],[9813,134,theory(equality)])).
% cnf(10022,plain,(aNaturalNumber0(X1)|xm!=X1|~sdtlseqdt0(sz00,xm)|~aNaturalNumber0(sz00)|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[242,9751,theory(equality)])).
% cnf(10026,plain,(aNaturalNumber0(X1)|xm!=X1|$false|~aNaturalNumber0(sz00)|~aNaturalNumber0(xm)),inference(rw,[status(thm)],[10022,9748,theory(equality)])).
% cnf(10027,plain,(aNaturalNumber0(X1)|xm!=X1|$false|$false|~aNaturalNumber0(xm)),inference(rw,[status(thm)],[10026,54,theory(equality)])).
% cnf(10028,plain,(aNaturalNumber0(X1)|xm!=X1|$false|$false|$false),inference(rw,[status(thm)],[10027,137,theory(equality)])).
% cnf(10029,plain,(aNaturalNumber0(X1)|xm!=X1),inference(cn,[status(thm)],[10028,theory(equality)])).
% cnf(10680,plain,(doDivides0(xm,X1)|xm!=X1),inference(csr,[status(thm)],[9238,10029])).
% cnf(10681,plain,(doDivides0(xm,xm)),inference(er,[status(thm)],[10680,theory(equality)])).
% cnf(10683,plain,(aNaturalNumber0(esk1_2(xm,xm))|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[111,10681,theory(equality)])).
% cnf(10684,plain,(sdtasdt0(xm,esk1_2(xm,xm))=xm|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[110,10681,theory(equality)])).
% cnf(10691,plain,(aNaturalNumber0(esk1_2(xm,xm))|$false),inference(rw,[status(thm)],[10683,137,theory(equality)])).
% cnf(10692,plain,(aNaturalNumber0(esk1_2(xm,xm))),inference(cn,[status(thm)],[10691,theory(equality)])).
% cnf(10693,plain,(sdtasdt0(xm,esk1_2(xm,xm))=xm|$false),inference(rw,[status(thm)],[10684,137,theory(equality)])).
% cnf(10694,plain,(sdtasdt0(xm,esk1_2(xm,xm))=xm),inference(cn,[status(thm)],[10693,theory(equality)])).
% cnf(11207,plain,(sz10=X1|sdtasdt0(xm,X1)!=xm|~aNaturalNumber0(X1)|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[9180,60,theory(equality)])).
% cnf(11215,plain,(sz10=X1|sdtasdt0(xm,X1)!=xm|~aNaturalNumber0(X1)|$false),inference(rw,[status(thm)],[11207,137,theory(equality)])).
% cnf(11216,plain,(sz10=X1|sdtasdt0(xm,X1)!=xm|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[11215,theory(equality)])).
% cnf(11558,plain,(sz00=xp|aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xn),xp))|~aNaturalNumber0(xp)|~aNaturalNumber0(sdtasdt0(xn,xn))),inference(spm,[status(thm)],[600,145,theory(equality)])).
% cnf(11599,plain,(sz00=xp|aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xn),xp))|$false|~aNaturalNumber0(sdtasdt0(xn,xn))),inference(rw,[status(thm)],[11558,136,theory(equality)])).
% cnf(11600,plain,(sz00=xp|aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xn),xp))|$false|$false),inference(rw,[status(thm)],[11599,1016,theory(equality)])).
% cnf(11601,plain,(sz00=xp|aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xn),xp))),inference(cn,[status(thm)],[11600,theory(equality)])).
% cnf(11602,plain,(aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xn),xp))),inference(sr,[status(thm)],[11601,133,theory(equality)])).
% cnf(11669,plain,(sz10=esk1_2(xm,xm)|~aNaturalNumber0(esk1_2(xm,xm))|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[11216,1664,theory(equality)])).
% cnf(11674,plain,(sz10=esk1_2(xm,xm)|$false|~aNaturalNumber0(xm)),inference(rw,[status(thm)],[11669,10692,theory(equality)])).
% cnf(11675,plain,(sz10=esk1_2(xm,xm)|$false|$false),inference(rw,[status(thm)],[11674,137,theory(equality)])).
% cnf(11676,plain,(sz10=esk1_2(xm,xm)),inference(cn,[status(thm)],[11675,theory(equality)])).
% cnf(11699,plain,(sdtasdt0(xm,sz10)=xm),inference(rw,[status(thm)],[10694,11676,theory(equality)])).
% cnf(11839,plain,(X1=sdtasdt0(xm,xm)|sdtasdt0(xp,X1)!=sdtasdt0(xn,xn)|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[630,1147,theory(equality)])).
% cnf(11840,plain,(X1=sdtasdt0(xm,xm)|sdtasdt0(xp,X1)!=sdtasdt0(xn,xn)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[11839,theory(equality)])).
% cnf(13329,plain,(sdtasdt0(xp,sdtsldt0(sdtasdt0(xn,xn),xp))=sdtasdt0(xn,xn)|sz00=xp|~aNaturalNumber0(xp)|~aNaturalNumber0(sdtasdt0(xn,xn))),inference(spm,[status(thm)],[648,145,theory(equality)])).
% cnf(13370,plain,(sdtasdt0(xp,sdtsldt0(sdtasdt0(xn,xn),xp))=sdtasdt0(xn,xn)|sz00=xp|$false|~aNaturalNumber0(sdtasdt0(xn,xn))),inference(rw,[status(thm)],[13329,136,theory(equality)])).
% cnf(13371,plain,(sdtasdt0(xp,sdtsldt0(sdtasdt0(xn,xn),xp))=sdtasdt0(xn,xn)|sz00=xp|$false|$false),inference(rw,[status(thm)],[13370,1016,theory(equality)])).
% cnf(13372,plain,(sdtasdt0(xp,sdtsldt0(sdtasdt0(xn,xn),xp))=sdtasdt0(xn,xn)|sz00=xp),inference(cn,[status(thm)],[13371,theory(equality)])).
% cnf(13373,plain,(sdtasdt0(xp,sdtsldt0(sdtasdt0(xn,xn),xp))=sdtasdt0(xn,xn)),inference(sr,[status(thm)],[13372,133,theory(equality)])).
% cnf(13934,plain,(sdtsldt0(sdtasdt0(xn,xn),xp)=sdtasdt0(xm,xm)|~aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xn),xp))),inference(spm,[status(thm)],[11840,13373,theory(equality)])).
% cnf(14023,plain,(sdtsldt0(sdtasdt0(xn,xn),xp)=sdtasdt0(xm,xm)|$false),inference(rw,[status(thm)],[13934,11602,theory(equality)])).
% cnf(14024,plain,(sdtsldt0(sdtasdt0(xn,xn),xp)=sdtasdt0(xm,xm)),inference(cn,[status(thm)],[14023,theory(equality)])).
% cnf(18336,plain,(sdtasdt0(sz00,xm)=sdtasdt0(sz00,sz10)|~aNaturalNumber0(sz10)|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[687,11699,theory(equality)])).
% cnf(18490,plain,(sdtasdt0(sz00,xm)=sz00|~aNaturalNumber0(sz10)|~aNaturalNumber0(xm)),inference(rw,[status(thm)],[18336,3182,theory(equality)])).
% cnf(18491,plain,(sdtasdt0(sz00,xm)=sz00|$false|~aNaturalNumber0(xm)),inference(rw,[status(thm)],[18490,212,theory(equality)])).
% cnf(18492,plain,(sdtasdt0(sz00,xm)=sz00|$false|$false),inference(rw,[status(thm)],[18491,137,theory(equality)])).
% cnf(18493,plain,(sdtasdt0(sz00,xm)=sz00),inference(cn,[status(thm)],[18492,theory(equality)])).
% cnf(18672,plain,(doDivides0(xm,X1)|sz00!=X1|~aNaturalNumber0(sz00)|~aNaturalNumber0(xm)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[535,18493,theory(equality)])).
% cnf(18749,plain,(doDivides0(xm,X1)|sz00!=X1|$false|~aNaturalNumber0(xm)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[18672,54,theory(equality)])).
% cnf(18750,plain,(doDivides0(xm,X1)|sz00!=X1|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[18749,137,theory(equality)])).
% cnf(18751,plain,(doDivides0(xm,X1)|sz00!=X1|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[18750,theory(equality)])).
% cnf(19815,plain,(sdtsldt0(sdtasdt0(X1,X2),X1)=X2|sz00=X1|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[692,57])).
% cnf(20173,plain,(doDivides0(xm,X1)|sz00!=X1),inference(csr,[status(thm)],[18751,2896])).
% cnf(20174,plain,(doDivides0(xm,sz00)),inference(er,[status(thm)],[20173,theory(equality)])).
% cnf(20176,plain,(aNaturalNumber0(esk1_2(xm,sz00))|~aNaturalNumber0(xm)|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[111,20174,theory(equality)])).
% cnf(20177,plain,(sdtasdt0(xm,esk1_2(xm,sz00))=sz00|~aNaturalNumber0(xm)|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[110,20174,theory(equality)])).
% cnf(20187,plain,(aNaturalNumber0(esk1_2(xm,sz00))|$false|~aNaturalNumber0(sz00)),inference(rw,[status(thm)],[20176,137,theory(equality)])).
% cnf(20188,plain,(aNaturalNumber0(esk1_2(xm,sz00))|$false|$false),inference(rw,[status(thm)],[20187,54,theory(equality)])).
% cnf(20189,plain,(aNaturalNumber0(esk1_2(xm,sz00))),inference(cn,[status(thm)],[20188,theory(equality)])).
% cnf(20190,plain,(sdtasdt0(xm,esk1_2(xm,sz00))=sz00|$false|~aNaturalNumber0(sz00)),inference(rw,[status(thm)],[20177,137,theory(equality)])).
% cnf(20191,plain,(sdtasdt0(xm,esk1_2(xm,sz00))=sz00|$false|$false),inference(rw,[status(thm)],[20190,54,theory(equality)])).
% cnf(20192,plain,(sdtasdt0(xm,esk1_2(xm,sz00))=sz00),inference(cn,[status(thm)],[20191,theory(equality)])).
% cnf(20223,plain,(sz00=esk1_2(xm,sz00)|sdtlseqdt0(xm,sz00)|~aNaturalNumber0(esk1_2(xm,sz00))|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[101,20192,theory(equality)])).
% cnf(20264,plain,(sz00=esk1_2(xm,sz00)|sdtlseqdt0(xm,sz00)|$false|~aNaturalNumber0(xm)),inference(rw,[status(thm)],[20223,20189,theory(equality)])).
% cnf(20265,plain,(sz00=esk1_2(xm,sz00)|sdtlseqdt0(xm,sz00)|$false|$false),inference(rw,[status(thm)],[20264,137,theory(equality)])).
% cnf(20266,plain,(sz00=esk1_2(xm,sz00)|sdtlseqdt0(xm,sz00)),inference(cn,[status(thm)],[20265,theory(equality)])).
% cnf(20267,plain,(esk1_2(xm,sz00)=sz00),inference(sr,[status(thm)],[20266,9814,theory(equality)])).
% cnf(73528,plain,(sdtasdt0(xn,xq)=sdtasdt0(xm,xm)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[14024,909,theory(equality)])).
% cnf(73549,plain,(sdtasdt0(xn,xq)=sdtasdt0(xm,xm)|$false),inference(rw,[status(thm)],[73528,138,theory(equality)])).
% cnf(73550,plain,(sdtasdt0(xn,xq)=sdtasdt0(xm,xm)),inference(cn,[status(thm)],[73549,theory(equality)])).
% cnf(73603,plain,(doDivides0(xm,sdtasdt0(xn,xq))|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[8016,73550,theory(equality)])).
% cnf(73609,plain,(sdtsldt0(sdtasdt0(xn,xq),xm)=xm|sz00=xm|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[19815,73550,theory(equality)])).
% cnf(73765,plain,(aNaturalNumber0(sdtasdt0(xn,xq))),inference(rw,[status(thm)],[1147,73550,theory(equality)])).
% cnf(73788,plain,(sdtasdt0(xp,sdtasdt0(xq,xq))=sdtasdt0(xn,xq)),inference(rw,[status(thm)],[147,73550,theory(equality)])).
% cnf(73839,plain,(doDivides0(xm,sdtasdt0(xn,xq))|$false),inference(rw,[status(thm)],[73603,137,theory(equality)])).
% cnf(73840,plain,(doDivides0(xm,sdtasdt0(xn,xq))),inference(cn,[status(thm)],[73839,theory(equality)])).
% cnf(73853,plain,(sdtsldt0(sdtasdt0(xn,xq),xm)=xm|sz00=xm|$false),inference(rw,[status(thm)],[73609,137,theory(equality)])).
% cnf(73854,plain,(sdtsldt0(sdtasdt0(xn,xq),xm)=xm|sz00=xm),inference(cn,[status(thm)],[73853,theory(equality)])).
% cnf(73855,plain,(sdtsldt0(sdtasdt0(xn,xq),xm)=xm),inference(sr,[status(thm)],[73854,134,theory(equality)])).
% cnf(77040,plain,(aNaturalNumber0(esk1_2(xm,sdtasdt0(xn,xq)))|~aNaturalNumber0(xm)|~aNaturalNumber0(sdtasdt0(xn,xq))),inference(spm,[status(thm)],[111,73840,theory(equality)])).
% cnf(77041,plain,(sdtasdt0(xm,esk1_2(xm,sdtasdt0(xn,xq)))=sdtasdt0(xn,xq)|~aNaturalNumber0(xm)|~aNaturalNumber0(sdtasdt0(xn,xq))),inference(spm,[status(thm)],[110,73840,theory(equality)])).
% cnf(77057,plain,(aNaturalNumber0(esk1_2(xm,sdtasdt0(xn,xq)))|$false|~aNaturalNumber0(sdtasdt0(xn,xq))),inference(rw,[status(thm)],[77040,137,theory(equality)])).
% cnf(77058,plain,(aNaturalNumber0(esk1_2(xm,sdtasdt0(xn,xq)))|$false|$false),inference(rw,[status(thm)],[77057,73765,theory(equality)])).
% cnf(77059,plain,(aNaturalNumber0(esk1_2(xm,sdtasdt0(xn,xq)))),inference(cn,[status(thm)],[77058,theory(equality)])).
% cnf(77060,plain,(sdtasdt0(xm,esk1_2(xm,sdtasdt0(xn,xq)))=sdtasdt0(xn,xq)|$false|~aNaturalNumber0(sdtasdt0(xn,xq))),inference(rw,[status(thm)],[77041,137,theory(equality)])).
% cnf(77061,plain,(sdtasdt0(xm,esk1_2(xm,sdtasdt0(xn,xq)))=sdtasdt0(xn,xq)|$false|$false),inference(rw,[status(thm)],[77060,73765,theory(equality)])).
% cnf(77062,plain,(sdtasdt0(xm,esk1_2(xm,sdtasdt0(xn,xq)))=sdtasdt0(xn,xq)),inference(cn,[status(thm)],[77061,theory(equality)])).
% cnf(81804,plain,(sdtsldt0(sdtasdt0(xn,xq),xm)=esk1_2(xm,sdtasdt0(xn,xq))|sz00=xm|~aNaturalNumber0(esk1_2(xm,sdtasdt0(xn,xq)))|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[19815,77062,theory(equality)])).
% cnf(81945,plain,(xm=esk1_2(xm,sdtasdt0(xn,xq))|sz00=xm|~aNaturalNumber0(esk1_2(xm,sdtasdt0(xn,xq)))|~aNaturalNumber0(xm)),inference(rw,[status(thm)],[81804,73855,theory(equality)])).
% cnf(81946,plain,(xm=esk1_2(xm,sdtasdt0(xn,xq))|sz00=xm|$false|~aNaturalNumber0(xm)),inference(rw,[status(thm)],[81945,77059,theory(equality)])).
% cnf(81947,plain,(xm=esk1_2(xm,sdtasdt0(xn,xq))|sz00=xm|$false|$false),inference(rw,[status(thm)],[81946,137,theory(equality)])).
% cnf(81948,plain,(xm=esk1_2(xm,sdtasdt0(xn,xq))|sz00=xm),inference(cn,[status(thm)],[81947,theory(equality)])).
% cnf(81949,plain,(esk1_2(xm,sdtasdt0(xn,xq))=xm),inference(sr,[status(thm)],[81948,134,theory(equality)])).
% cnf(91418,plain,(sz00=X1|sdtasdt0(X2,sdtasdt0(X1,X1))!=sdtasdt0(xn,xq)|~isPrime0(X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(rw,[status(thm)],[967,73550,theory(equality)])).
% cnf(91437,plain,(sz00=xq|~isPrime0(xp)|~aNaturalNumber0(xq)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[91418,73788,theory(equality)])).
% cnf(91467,plain,(sz00=xq|$false|~aNaturalNumber0(xq)|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[91437,143,theory(equality)])).
% cnf(91468,plain,(sz00=xq|$false|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[91467,1017,theory(equality)])).
% cnf(91469,plain,(sz00=xq|$false|$false|$false),inference(rw,[status(thm)],[91468,136,theory(equality)])).
% cnf(91470,plain,(sz00=xq),inference(cn,[status(thm)],[91469,theory(equality)])).
% cnf(91524,plain,(sz00=xm),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[81949,91470,theory(equality)]),3602,theory(equality)]),20267,theory(equality)])).
% cnf(91525,plain,($false),inference(sr,[status(thm)],[91524,134,theory(equality)])).
% cnf(91526,plain,($false),91525,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 2881
% # ...of these trivial : 179
% # ...subsumed : 1308
% # ...remaining for further processing: 1394
% # Other redundant clauses eliminated : 66
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 68
% # Backward-rewritten : 540
% # Generated clauses : 28414
% # ...of the previous two non-trivial : 24988
% # Contextual simplify-reflections : 438
% # Paramodulations : 28181
% # Factorizations : 10
% # Equation resolutions : 215
% # Current number of processed clauses: 699
% # Positive orientable unit clauses: 216
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 21
% # Non-unit-clauses : 462
% # Current number of unprocessed clauses: 12326
% # ...number of literals in the above : 62379
% # Clause-clause subsumption calls (NU) : 13309
% # Rec. Clause-clause subsumption calls : 7386
% # Unit Clause-clause subsumption calls : 315
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 142
% # Indexed BW rewrite successes : 92
% # Backwards rewriting index: 565 leaves, 1.24+/-1.124 terms/leaf
% # Paramod-from index: 384 leaves, 1.06+/-0.274 terms/leaf
% # Paramod-into index: 504 leaves, 1.19+/-0.954 terms/leaf
% # -------------------------------------------------
% # User time : 1.351 s
% # System time : 0.048 s
% # Total time : 1.399 s
% # Maximum resident set size: 0 pages
% PrfWatch: 2.68 CPU 3.04 WC
% FINAL PrfWatch: 2.68 CPU 3.04 WC
% SZS output end Solution for /tmp/SystemOnTPTP17699/NUM529+1.tptp
%
%------------------------------------------------------------------------------