%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NUM518+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 : art11.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 3.00GHz @ 3000MHz
% Memory : 2006MB
% OS : Linux 2.6.31.5-127.fc12.i686.PAE
% CPULimit : 300s
% DateTime : Wed Dec 29 19:56:06 EST 2010
% Result : Theorem 11.64s
% Output : Solution 11.64s
% 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/SystemOnTPTP3668/NUM518+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP3668/NUM518+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP3668/NUM518+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 3800
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% PrfWatch: 1.94 CPU 2.03 WC
% PrfWatch: 3.92 CPU 4.03 WC
% PrfWatch: 5.92 CPU 6.04 WC
% # Preprocessing time : 0.018 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 7.90 CPU 8.04 WC
% PrfWatch: 9.89 CPU 10.05 WC
% # SZS output start CNFRefutation.
% fof(1, axiom,aNaturalNumber0(sz00),file('/tmp/SRASS.s.p', mSortsC)).
% fof(2, axiom,(aNaturalNumber0(sz10)&~(sz10=sz00)),file('/tmp/SRASS.s.p', mSortsC_01)).
% fof(3, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>aNaturalNumber0(sdtpldt0(X1,X2))),file('/tmp/SRASS.s.p', mSortsB)).
% fof(4, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>aNaturalNumber0(sdtasdt0(X1,X2))),file('/tmp/SRASS.s.p', mSortsB_02)).
% fof(5, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>sdtpldt0(X1,X2)=sdtpldt0(X2,X1)),file('/tmp/SRASS.s.p', mAddComm)).
% fof(7, axiom,![X1]:(aNaturalNumber0(X1)=>(sdtpldt0(X1,sz00)=X1&X1=sdtpldt0(sz00,X1))),file('/tmp/SRASS.s.p', m_AddZero)).
% fof(8, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>sdtasdt0(X1,X2)=sdtasdt0(X2,X1)),file('/tmp/SRASS.s.p', mMulComm)).
% fof(9, axiom,![X1]:![X2]:![X3]:(((aNaturalNumber0(X1)&aNaturalNumber0(X2))&aNaturalNumber0(X3))=>sdtasdt0(sdtasdt0(X1,X2),X3)=sdtasdt0(X1,sdtasdt0(X2,X3))),file('/tmp/SRASS.s.p', mMulAsso)).
% fof(10, axiom,![X1]:(aNaturalNumber0(X1)=>(sdtasdt0(X1,sz10)=X1&X1=sdtasdt0(sz10,X1))),file('/tmp/SRASS.s.p', m_MulUnit)).
% fof(11, axiom,![X1]:(aNaturalNumber0(X1)=>(sdtasdt0(X1,sz00)=sz00&sz00=sdtasdt0(sz00,X1))),file('/tmp/SRASS.s.p', m_MulZero)).
% fof(13, 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(14, axiom,![X1]:(aNaturalNumber0(X1)=>(~(X1=sz00)=>![X2]:![X3]:((aNaturalNumber0(X2)&aNaturalNumber0(X3))=>((sdtasdt0(X1,X2)=sdtasdt0(X1,X3)|sdtasdt0(X2,X1)=sdtasdt0(X3,X1))=>X2=X3)))),file('/tmp/SRASS.s.p', mMulCanc)).
% fof(15, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>(sdtpldt0(X1,X2)=sz00=>(X1=sz00&X2=sz00))),file('/tmp/SRASS.s.p', mZeroAdd)).
% fof(16, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>(sdtasdt0(X1,X2)=sz00=>(X1=sz00|X2=sz00))),file('/tmp/SRASS.s.p', mZeroMul)).
% fof(17, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>(sdtlseqdt0(X1,X2)<=>?[X3]:(aNaturalNumber0(X3)&sdtpldt0(X1,X3)=X2))),file('/tmp/SRASS.s.p', mDefLE)).
% fof(19, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>((sdtlseqdt0(X1,X2)&sdtlseqdt0(X2,X1))=>X1=X2)),file('/tmp/SRASS.s.p', mLEAsym)).
% fof(20, 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(21, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>(sdtlseqdt0(X1,X2)|(~(X2=X1)&sdtlseqdt0(X2,X1)))),file('/tmp/SRASS.s.p', mLETotal)).
% fof(25, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>(~(X1=sz00)=>sdtlseqdt0(X2,sdtasdt0(X2,X1)))),file('/tmp/SRASS.s.p', mMonMul2)).
% fof(27, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>(doDivides0(X1,X2)<=>?[X3]:(aNaturalNumber0(X3)&X2=sdtasdt0(X1,X3)))),file('/tmp/SRASS.s.p', mDefDiv)).
% fof(28, 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(29, 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(30, axiom,![X1]:![X2]:![X3]:(((aNaturalNumber0(X1)&aNaturalNumber0(X2))&aNaturalNumber0(X3))=>((doDivides0(X1,X2)&doDivides0(X1,X3))=>doDivides0(X1,sdtpldt0(X2,X3)))),file('/tmp/SRASS.s.p', mDivSum)).
% fof(31, axiom,![X1]:![X2]:![X3]:(((aNaturalNumber0(X1)&aNaturalNumber0(X2))&aNaturalNumber0(X3))=>((doDivides0(X1,X2)&doDivides0(X1,sdtpldt0(X2,X3)))=>doDivides0(X1,X3))),file('/tmp/SRASS.s.p', mDivMin)).
% fof(36, axiom,((aNaturalNumber0(xn)&aNaturalNumber0(xm))&aNaturalNumber0(xp)),file('/tmp/SRASS.s.p', m__1837)).
% fof(38, axiom,(isPrime0(xp)&doDivides0(xp,sdtasdt0(xn,xm))),file('/tmp/SRASS.s.p', m__1860)).
% fof(39, axiom,~(sdtlseqdt0(xp,xn)),file('/tmp/SRASS.s.p', m__1870)).
% fof(41, axiom,(((~(xn=xp)&sdtlseqdt0(xn,xp))&~(xm=xp))&sdtlseqdt0(xm,xp)),file('/tmp/SRASS.s.p', m__2287)).
% fof(45, axiom,((aNaturalNumber0(xr)&doDivides0(xr,xk))&isPrime0(xr)),file('/tmp/SRASS.s.p', m__2342)).
% fof(46, axiom,(sdtlseqdt0(xr,xk)&doDivides0(xr,sdtasdt0(xn,xm))),file('/tmp/SRASS.s.p', m__2362)).
% fof(49, axiom,doDivides0(xr,xn),file('/tmp/SRASS.s.p', m__2487)).
% fof(50, axiom,(~(sdtsldt0(xn,xr)=xn)&sdtlseqdt0(sdtsldt0(xn,xr),xn)),file('/tmp/SRASS.s.p', m__2504)).
% fof(52, axiom,(doDivides0(xp,sdtsldt0(xn,xr))|doDivides0(xp,xm)),file('/tmp/SRASS.s.p', m__2645)).
% fof(53, 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(56, conjecture,(doDivides0(xp,xn)|doDivides0(xp,xm)),file('/tmp/SRASS.s.p', m__)).
% fof(57, negated_conjecture,~((doDivides0(xp,xn)|doDivides0(xp,xm))),inference(assume_negation,[status(cth)],[56])).
% fof(58, plain,~(sdtlseqdt0(xp,xn)),inference(fof_simplification,[status(thm)],[39,theory(equality)])).
% cnf(62,plain,(aNaturalNumber0(sz00)),inference(split_conjunct,[status(thm)],[1])).
% cnf(63,plain,(sz10!=sz00),inference(split_conjunct,[status(thm)],[2])).
% cnf(64,plain,(aNaturalNumber0(sz10)),inference(split_conjunct,[status(thm)],[2])).
% fof(65, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|aNaturalNumber0(sdtpldt0(X1,X2))),inference(fof_nnf,[status(thm)],[3])).
% fof(66, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|aNaturalNumber0(sdtpldt0(X3,X4))),inference(variable_rename,[status(thm)],[65])).
% cnf(67,plain,(aNaturalNumber0(sdtpldt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[66])).
% fof(68, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|aNaturalNumber0(sdtasdt0(X1,X2))),inference(fof_nnf,[status(thm)],[4])).
% fof(69, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|aNaturalNumber0(sdtasdt0(X3,X4))),inference(variable_rename,[status(thm)],[68])).
% cnf(70,plain,(aNaturalNumber0(sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[69])).
% fof(71, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|sdtpldt0(X1,X2)=sdtpldt0(X2,X1)),inference(fof_nnf,[status(thm)],[5])).
% fof(72, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|sdtpldt0(X3,X4)=sdtpldt0(X4,X3)),inference(variable_rename,[status(thm)],[71])).
% cnf(73,plain,(sdtpldt0(X1,X2)=sdtpldt0(X2,X1)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[72])).
% fof(77, plain,![X1]:(~(aNaturalNumber0(X1))|(sdtpldt0(X1,sz00)=X1&X1=sdtpldt0(sz00,X1))),inference(fof_nnf,[status(thm)],[7])).
% fof(78, plain,![X2]:(~(aNaturalNumber0(X2))|(sdtpldt0(X2,sz00)=X2&X2=sdtpldt0(sz00,X2))),inference(variable_rename,[status(thm)],[77])).
% fof(79, plain,![X2]:((sdtpldt0(X2,sz00)=X2|~(aNaturalNumber0(X2)))&(X2=sdtpldt0(sz00,X2)|~(aNaturalNumber0(X2)))),inference(distribute,[status(thm)],[78])).
% cnf(80,plain,(X1=sdtpldt0(sz00,X1)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[79])).
% cnf(81,plain,(sdtpldt0(X1,sz00)=X1|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[79])).
% fof(82, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|sdtasdt0(X1,X2)=sdtasdt0(X2,X1)),inference(fof_nnf,[status(thm)],[8])).
% fof(83, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|sdtasdt0(X3,X4)=sdtasdt0(X4,X3)),inference(variable_rename,[status(thm)],[82])).
% cnf(84,plain,(sdtasdt0(X1,X2)=sdtasdt0(X2,X1)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[83])).
% fof(85, plain,![X1]:![X2]:![X3]:(((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|~(aNaturalNumber0(X3)))|sdtasdt0(sdtasdt0(X1,X2),X3)=sdtasdt0(X1,sdtasdt0(X2,X3))),inference(fof_nnf,[status(thm)],[9])).
% fof(86, 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)],[85])).
% cnf(87,plain,(sdtasdt0(sdtasdt0(X1,X2),X3)=sdtasdt0(X1,sdtasdt0(X2,X3))|~aNaturalNumber0(X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[86])).
% fof(88, plain,![X1]:(~(aNaturalNumber0(X1))|(sdtasdt0(X1,sz10)=X1&X1=sdtasdt0(sz10,X1))),inference(fof_nnf,[status(thm)],[10])).
% fof(89, plain,![X2]:(~(aNaturalNumber0(X2))|(sdtasdt0(X2,sz10)=X2&X2=sdtasdt0(sz10,X2))),inference(variable_rename,[status(thm)],[88])).
% fof(90, plain,![X2]:((sdtasdt0(X2,sz10)=X2|~(aNaturalNumber0(X2)))&(X2=sdtasdt0(sz10,X2)|~(aNaturalNumber0(X2)))),inference(distribute,[status(thm)],[89])).
% cnf(91,plain,(X1=sdtasdt0(sz10,X1)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[90])).
% cnf(92,plain,(sdtasdt0(X1,sz10)=X1|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[90])).
% fof(93, plain,![X1]:(~(aNaturalNumber0(X1))|(sdtasdt0(X1,sz00)=sz00&sz00=sdtasdt0(sz00,X1))),inference(fof_nnf,[status(thm)],[11])).
% fof(94, plain,![X2]:(~(aNaturalNumber0(X2))|(sdtasdt0(X2,sz00)=sz00&sz00=sdtasdt0(sz00,X2))),inference(variable_rename,[status(thm)],[93])).
% fof(95, plain,![X2]:((sdtasdt0(X2,sz00)=sz00|~(aNaturalNumber0(X2)))&(sz00=sdtasdt0(sz00,X2)|~(aNaturalNumber0(X2)))),inference(distribute,[status(thm)],[94])).
% cnf(96,plain,(sz00=sdtasdt0(sz00,X1)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[95])).
% cnf(97,plain,(sdtasdt0(X1,sz00)=sz00|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[95])).
% fof(103, 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)],[13])).
% fof(104, 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)],[103])).
% fof(105, 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)],[104])).
% cnf(107,plain,(X2=X1|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~aNaturalNumber0(X3)|sdtpldt0(X3,X2)!=sdtpldt0(X3,X1)),inference(split_conjunct,[status(thm)],[105])).
% fof(108, plain,![X1]:(~(aNaturalNumber0(X1))|(X1=sz00|![X2]:![X3]:((~(aNaturalNumber0(X2))|~(aNaturalNumber0(X3)))|((~(sdtasdt0(X1,X2)=sdtasdt0(X1,X3))&~(sdtasdt0(X2,X1)=sdtasdt0(X3,X1)))|X2=X3)))),inference(fof_nnf,[status(thm)],[14])).
% fof(109, 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)],[108])).
% fof(110, 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)],[109])).
% fof(111, 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)],[110])).
% cnf(113,plain,(X1=sz00|X3=X2|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~aNaturalNumber0(X3)|sdtasdt0(X1,X3)!=sdtasdt0(X1,X2)),inference(split_conjunct,[status(thm)],[111])).
% fof(114, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|(~(sdtpldt0(X1,X2)=sz00)|(X1=sz00&X2=sz00))),inference(fof_nnf,[status(thm)],[15])).
% fof(115, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|(~(sdtpldt0(X3,X4)=sz00)|(X3=sz00&X4=sz00))),inference(variable_rename,[status(thm)],[114])).
% fof(116, plain,![X3]:![X4]:(((X3=sz00|~(sdtpldt0(X3,X4)=sz00))|(~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4))))&((X4=sz00|~(sdtpldt0(X3,X4)=sz00))|(~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4))))),inference(distribute,[status(thm)],[115])).
% cnf(117,plain,(X1=sz00|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|sdtpldt0(X2,X1)!=sz00),inference(split_conjunct,[status(thm)],[116])).
% cnf(118,plain,(X2=sz00|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|sdtpldt0(X2,X1)!=sz00),inference(split_conjunct,[status(thm)],[116])).
% fof(119, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|(~(sdtasdt0(X1,X2)=sz00)|(X1=sz00|X2=sz00))),inference(fof_nnf,[status(thm)],[16])).
% fof(120, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|(~(sdtasdt0(X3,X4)=sz00)|(X3=sz00|X4=sz00))),inference(variable_rename,[status(thm)],[119])).
% cnf(121,plain,(X1=sz00|X2=sz00|sdtasdt0(X2,X1)!=sz00|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(split_conjunct,[status(thm)],[120])).
% fof(122, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|((~(sdtlseqdt0(X1,X2))|?[X3]:(aNaturalNumber0(X3)&sdtpldt0(X1,X3)=X2))&(![X3]:(~(aNaturalNumber0(X3))|~(sdtpldt0(X1,X3)=X2))|sdtlseqdt0(X1,X2)))),inference(fof_nnf,[status(thm)],[17])).
% fof(123, 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)],[122])).
% fof(124, plain,![X4]:![X5]:((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|((~(sdtlseqdt0(X4,X5))|(aNaturalNumber0(esk1_2(X4,X5))&sdtpldt0(X4,esk1_2(X4,X5))=X5))&(![X7]:(~(aNaturalNumber0(X7))|~(sdtpldt0(X4,X7)=X5))|sdtlseqdt0(X4,X5)))),inference(skolemize,[status(esa)],[123])).
% fof(125, plain,![X4]:![X5]:![X7]:((((~(aNaturalNumber0(X7))|~(sdtpldt0(X4,X7)=X5))|sdtlseqdt0(X4,X5))&(~(sdtlseqdt0(X4,X5))|(aNaturalNumber0(esk1_2(X4,X5))&sdtpldt0(X4,esk1_2(X4,X5))=X5)))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))),inference(shift_quantors,[status(thm)],[124])).
% fof(126, plain,![X4]:![X5]:![X7]:((((~(aNaturalNumber0(X7))|~(sdtpldt0(X4,X7)=X5))|sdtlseqdt0(X4,X5))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5))))&(((aNaturalNumber0(esk1_2(X4,X5))|~(sdtlseqdt0(X4,X5)))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5))))&((sdtpldt0(X4,esk1_2(X4,X5))=X5|~(sdtlseqdt0(X4,X5)))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))))),inference(distribute,[status(thm)],[125])).
% cnf(127,plain,(sdtpldt0(X2,esk1_2(X2,X1))=X1|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~sdtlseqdt0(X2,X1)),inference(split_conjunct,[status(thm)],[126])).
% cnf(128,plain,(aNaturalNumber0(esk1_2(X2,X1))|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~sdtlseqdt0(X2,X1)),inference(split_conjunct,[status(thm)],[126])).
% cnf(129,plain,(sdtlseqdt0(X2,X1)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|sdtpldt0(X2,X3)!=X1|~aNaturalNumber0(X3)),inference(split_conjunct,[status(thm)],[126])).
% fof(133, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|((~(sdtlseqdt0(X1,X2))|~(sdtlseqdt0(X2,X1)))|X1=X2)),inference(fof_nnf,[status(thm)],[19])).
% fof(134, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|((~(sdtlseqdt0(X3,X4))|~(sdtlseqdt0(X4,X3)))|X3=X4)),inference(variable_rename,[status(thm)],[133])).
% cnf(135,plain,(X1=X2|~sdtlseqdt0(X2,X1)|~sdtlseqdt0(X1,X2)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[134])).
% fof(136, plain,![X1]:![X2]:![X3]:(((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|~(aNaturalNumber0(X3)))|((~(sdtlseqdt0(X1,X2))|~(sdtlseqdt0(X2,X3)))|sdtlseqdt0(X1,X3))),inference(fof_nnf,[status(thm)],[20])).
% fof(137, plain,![X4]:![X5]:![X6]:(((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|~(aNaturalNumber0(X6)))|((~(sdtlseqdt0(X4,X5))|~(sdtlseqdt0(X5,X6)))|sdtlseqdt0(X4,X6))),inference(variable_rename,[status(thm)],[136])).
% cnf(138,plain,(sdtlseqdt0(X1,X2)|~sdtlseqdt0(X3,X2)|~sdtlseqdt0(X1,X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X3)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[137])).
% fof(139, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|(sdtlseqdt0(X1,X2)|(~(X2=X1)&sdtlseqdt0(X2,X1)))),inference(fof_nnf,[status(thm)],[21])).
% fof(140, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|(sdtlseqdt0(X3,X4)|(~(X4=X3)&sdtlseqdt0(X4,X3)))),inference(variable_rename,[status(thm)],[139])).
% fof(141, plain,![X3]:![X4]:(((~(X4=X3)|sdtlseqdt0(X3,X4))|(~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4))))&((sdtlseqdt0(X4,X3)|sdtlseqdt0(X3,X4))|(~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4))))),inference(distribute,[status(thm)],[140])).
% cnf(142,plain,(sdtlseqdt0(X2,X1)|sdtlseqdt0(X1,X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(split_conjunct,[status(thm)],[141])).
% fof(164, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|(X1=sz00|sdtlseqdt0(X2,sdtasdt0(X2,X1)))),inference(fof_nnf,[status(thm)],[25])).
% fof(165, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|(X3=sz00|sdtlseqdt0(X4,sdtasdt0(X4,X3)))),inference(variable_rename,[status(thm)],[164])).
% cnf(166,plain,(sdtlseqdt0(X1,sdtasdt0(X1,X2))|X2=sz00|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(split_conjunct,[status(thm)],[165])).
% fof(170, 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)],[27])).
% fof(171, 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)],[170])).
% fof(172, plain,![X4]:![X5]:((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|((~(doDivides0(X4,X5))|(aNaturalNumber0(esk2_2(X4,X5))&X5=sdtasdt0(X4,esk2_2(X4,X5))))&(![X7]:(~(aNaturalNumber0(X7))|~(X5=sdtasdt0(X4,X7)))|doDivides0(X4,X5)))),inference(skolemize,[status(esa)],[171])).
% fof(173, plain,![X4]:![X5]:![X7]:((((~(aNaturalNumber0(X7))|~(X5=sdtasdt0(X4,X7)))|doDivides0(X4,X5))&(~(doDivides0(X4,X5))|(aNaturalNumber0(esk2_2(X4,X5))&X5=sdtasdt0(X4,esk2_2(X4,X5)))))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))),inference(shift_quantors,[status(thm)],[172])).
% fof(174, plain,![X4]:![X5]:![X7]:((((~(aNaturalNumber0(X7))|~(X5=sdtasdt0(X4,X7)))|doDivides0(X4,X5))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5))))&(((aNaturalNumber0(esk2_2(X4,X5))|~(doDivides0(X4,X5)))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5))))&((X5=sdtasdt0(X4,esk2_2(X4,X5))|~(doDivides0(X4,X5)))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))))),inference(distribute,[status(thm)],[173])).
% cnf(175,plain,(X1=sdtasdt0(X2,esk2_2(X2,X1))|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~doDivides0(X2,X1)),inference(split_conjunct,[status(thm)],[174])).
% cnf(176,plain,(aNaturalNumber0(esk2_2(X2,X1))|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~doDivides0(X2,X1)),inference(split_conjunct,[status(thm)],[174])).
% cnf(177,plain,(doDivides0(X2,X1)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|X1!=sdtasdt0(X2,X3)|~aNaturalNumber0(X3)),inference(split_conjunct,[status(thm)],[174])).
% fof(178, 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)],[28])).
% fof(179, 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)],[178])).
% fof(180, 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)],[179])).
% fof(181, 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)],[180])).
% cnf(182,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)],[181])).
% cnf(184,plain,(X2=sz00|aNaturalNumber0(X3)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~doDivides0(X2,X1)|X3!=sdtsldt0(X1,X2)),inference(split_conjunct,[status(thm)],[181])).
% fof(185, plain,![X1]:![X2]:![X3]:(((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|~(aNaturalNumber0(X3)))|((~(doDivides0(X1,X2))|~(doDivides0(X2,X3)))|doDivides0(X1,X3))),inference(fof_nnf,[status(thm)],[29])).
% fof(186, plain,![X4]:![X5]:![X6]:(((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|~(aNaturalNumber0(X6)))|((~(doDivides0(X4,X5))|~(doDivides0(X5,X6)))|doDivides0(X4,X6))),inference(variable_rename,[status(thm)],[185])).
% cnf(187,plain,(doDivides0(X1,X2)|~doDivides0(X3,X2)|~doDivides0(X1,X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X3)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[186])).
% fof(188, plain,![X1]:![X2]:![X3]:(((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|~(aNaturalNumber0(X3)))|((~(doDivides0(X1,X2))|~(doDivides0(X1,X3)))|doDivides0(X1,sdtpldt0(X2,X3)))),inference(fof_nnf,[status(thm)],[30])).
% fof(189, plain,![X4]:![X5]:![X6]:(((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|~(aNaturalNumber0(X6)))|((~(doDivides0(X4,X5))|~(doDivides0(X4,X6)))|doDivides0(X4,sdtpldt0(X5,X6)))),inference(variable_rename,[status(thm)],[188])).
% cnf(190,plain,(doDivides0(X1,sdtpldt0(X2,X3))|~doDivides0(X1,X3)|~doDivides0(X1,X2)|~aNaturalNumber0(X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[189])).
% fof(191, plain,![X1]:![X2]:![X3]:(((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|~(aNaturalNumber0(X3)))|((~(doDivides0(X1,X2))|~(doDivides0(X1,sdtpldt0(X2,X3))))|doDivides0(X1,X3))),inference(fof_nnf,[status(thm)],[31])).
% fof(192, 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)],[191])).
% cnf(193,plain,(doDivides0(X1,X2)|~doDivides0(X1,sdtpldt0(X3,X2))|~doDivides0(X1,X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X3)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[192])).
% cnf(220,plain,(aNaturalNumber0(xp)),inference(split_conjunct,[status(thm)],[36])).
% cnf(221,plain,(aNaturalNumber0(xm)),inference(split_conjunct,[status(thm)],[36])).
% cnf(222,plain,(aNaturalNumber0(xn)),inference(split_conjunct,[status(thm)],[36])).
% cnf(226,plain,(doDivides0(xp,sdtasdt0(xn,xm))),inference(split_conjunct,[status(thm)],[38])).
% cnf(228,plain,(~sdtlseqdt0(xp,xn)),inference(split_conjunct,[status(thm)],[58])).
% cnf(230,plain,(sdtlseqdt0(xm,xp)),inference(split_conjunct,[status(thm)],[41])).
% cnf(231,plain,(xm!=xp),inference(split_conjunct,[status(thm)],[41])).
% cnf(232,plain,(sdtlseqdt0(xn,xp)),inference(split_conjunct,[status(thm)],[41])).
% cnf(242,plain,(aNaturalNumber0(xr)),inference(split_conjunct,[status(thm)],[45])).
% cnf(243,plain,(doDivides0(xr,sdtasdt0(xn,xm))),inference(split_conjunct,[status(thm)],[46])).
% cnf(248,plain,(doDivides0(xr,xn)),inference(split_conjunct,[status(thm)],[49])).
% cnf(249,plain,(sdtlseqdt0(sdtsldt0(xn,xr),xn)),inference(split_conjunct,[status(thm)],[50])).
% cnf(250,plain,(sdtsldt0(xn,xr)!=xn),inference(split_conjunct,[status(thm)],[50])).
% cnf(252,plain,(doDivides0(xp,xm)|doDivides0(xp,sdtsldt0(xn,xr))),inference(split_conjunct,[status(thm)],[52])).
% fof(253, 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)],[53])).
% fof(254, 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)],[253])).
% fof(255, 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)],[254])).
% fof(256, 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)],[255])).
% cnf(257,plain,(X3=sdtmndt0(X1,X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~sdtlseqdt0(X2,X1)|sdtpldt0(X2,X3)!=X1|~aNaturalNumber0(X3)),inference(split_conjunct,[status(thm)],[256])).
% cnf(259,plain,(aNaturalNumber0(X3)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~sdtlseqdt0(X2,X1)|X3!=sdtmndt0(X1,X2)),inference(split_conjunct,[status(thm)],[256])).
% fof(264, negated_conjecture,(~(doDivides0(xp,xn))&~(doDivides0(xp,xm))),inference(fof_nnf,[status(thm)],[57])).
% cnf(265,negated_conjecture,(~doDivides0(xp,xm)),inference(split_conjunct,[status(thm)],[264])).
% cnf(266,negated_conjecture,(~doDivides0(xp,xn)),inference(split_conjunct,[status(thm)],[264])).
% cnf(268,plain,(doDivides0(xp,sdtsldt0(xn,xr))),inference(sr,[status(thm)],[252,265,theory(equality)])).
% cnf(270,plain,(sdtmndt0(X1,X2)=X3|sdtpldt0(X2,X3)!=X1|~aNaturalNumber0(X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[257,129])).
% cnf(273,plain,(sdtsldt0(X1,X2)=X3|sz00=X2|sdtasdt0(X2,X3)!=X1|~aNaturalNumber0(X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[182,177])).
% cnf(383,plain,(aNaturalNumber0(esk2_2(xr,xn))|~aNaturalNumber0(xr)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[176,248,theory(equality)])).
% cnf(384,plain,(aNaturalNumber0(esk2_2(xr,sdtasdt0(xn,xm)))|~aNaturalNumber0(xr)|~aNaturalNumber0(sdtasdt0(xn,xm))),inference(spm,[status(thm)],[176,243,theory(equality)])).
% cnf(385,plain,(aNaturalNumber0(esk2_2(xp,sdtsldt0(xn,xr)))|~aNaturalNumber0(xp)|~aNaturalNumber0(sdtsldt0(xn,xr))),inference(spm,[status(thm)],[176,268,theory(equality)])).
% cnf(390,plain,(aNaturalNumber0(esk2_2(xr,xn))|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[383,242,theory(equality)])).
% cnf(391,plain,(aNaturalNumber0(esk2_2(xr,xn))|$false|$false),inference(rw,[status(thm)],[390,222,theory(equality)])).
% cnf(392,plain,(aNaturalNumber0(esk2_2(xr,xn))),inference(cn,[status(thm)],[391,theory(equality)])).
% cnf(393,plain,(aNaturalNumber0(esk2_2(xr,sdtasdt0(xn,xm)))|$false|~aNaturalNumber0(sdtasdt0(xn,xm))),inference(rw,[status(thm)],[384,242,theory(equality)])).
% cnf(394,plain,(aNaturalNumber0(esk2_2(xr,sdtasdt0(xn,xm)))|~aNaturalNumber0(sdtasdt0(xn,xm))),inference(cn,[status(thm)],[393,theory(equality)])).
% cnf(395,plain,(aNaturalNumber0(esk2_2(xp,sdtsldt0(xn,xr)))|$false|~aNaturalNumber0(sdtsldt0(xn,xr))),inference(rw,[status(thm)],[385,220,theory(equality)])).
% cnf(396,plain,(aNaturalNumber0(esk2_2(xp,sdtsldt0(xn,xr)))|~aNaturalNumber0(sdtsldt0(xn,xr))),inference(cn,[status(thm)],[395,theory(equality)])).
% cnf(460,plain,(aNaturalNumber0(esk1_2(xm,xp))|~aNaturalNumber0(xm)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[128,230,theory(equality)])).
% cnf(461,plain,(aNaturalNumber0(esk1_2(xn,xp))|~aNaturalNumber0(xn)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[128,232,theory(equality)])).
% cnf(471,plain,(aNaturalNumber0(esk1_2(xm,xp))|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[460,221,theory(equality)])).
% cnf(472,plain,(aNaturalNumber0(esk1_2(xm,xp))|$false|$false),inference(rw,[status(thm)],[471,220,theory(equality)])).
% cnf(473,plain,(aNaturalNumber0(esk1_2(xm,xp))),inference(cn,[status(thm)],[472,theory(equality)])).
% cnf(474,plain,(aNaturalNumber0(esk1_2(xn,xp))|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[461,222,theory(equality)])).
% cnf(475,plain,(aNaturalNumber0(esk1_2(xn,xp))|$false|$false),inference(rw,[status(thm)],[474,220,theory(equality)])).
% cnf(476,plain,(aNaturalNumber0(esk1_2(xn,xp))),inference(cn,[status(thm)],[475,theory(equality)])).
% cnf(484,plain,(sz00=X1|sdtlseqdt0(sz00,sz00)|~aNaturalNumber0(X1)|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[166,96,theory(equality)])).
% cnf(486,plain,(sz00=X1|sdtlseqdt0(X2,sdtasdt0(X1,X2))|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(spm,[status(thm)],[166,84,theory(equality)])).
% cnf(490,plain,(sz00=X1|sdtlseqdt0(sz00,sz00)|~aNaturalNumber0(X1)|$false),inference(rw,[status(thm)],[484,62,theory(equality)])).
% cnf(491,plain,(sz00=X1|sdtlseqdt0(sz00,sz00)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[490,theory(equality)])).
% cnf(498,plain,(sdtasdt0(xr,esk2_2(xr,xn))=xn|~aNaturalNumber0(xr)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[175,248,theory(equality)])).
% cnf(499,plain,(sdtasdt0(xr,esk2_2(xr,sdtasdt0(xn,xm)))=sdtasdt0(xn,xm)|~aNaturalNumber0(xr)|~aNaturalNumber0(sdtasdt0(xn,xm))),inference(spm,[status(thm)],[175,243,theory(equality)])).
% cnf(500,plain,(sdtasdt0(xp,esk2_2(xp,sdtsldt0(xn,xr)))=sdtsldt0(xn,xr)|~aNaturalNumber0(xp)|~aNaturalNumber0(sdtsldt0(xn,xr))),inference(spm,[status(thm)],[175,268,theory(equality)])).
% cnf(505,plain,(sdtasdt0(xr,esk2_2(xr,xn))=xn|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[498,242,theory(equality)])).
% cnf(506,plain,(sdtasdt0(xr,esk2_2(xr,xn))=xn|$false|$false),inference(rw,[status(thm)],[505,222,theory(equality)])).
% cnf(507,plain,(sdtasdt0(xr,esk2_2(xr,xn))=xn),inference(cn,[status(thm)],[506,theory(equality)])).
% cnf(508,plain,(sdtasdt0(xr,esk2_2(xr,sdtasdt0(xn,xm)))=sdtasdt0(xn,xm)|$false|~aNaturalNumber0(sdtasdt0(xn,xm))),inference(rw,[status(thm)],[499,242,theory(equality)])).
% cnf(509,plain,(sdtasdt0(xr,esk2_2(xr,sdtasdt0(xn,xm)))=sdtasdt0(xn,xm)|~aNaturalNumber0(sdtasdt0(xn,xm))),inference(cn,[status(thm)],[508,theory(equality)])).
% cnf(510,plain,(sdtasdt0(xp,esk2_2(xp,sdtsldt0(xn,xr)))=sdtsldt0(xn,xr)|$false|~aNaturalNumber0(sdtsldt0(xn,xr))),inference(rw,[status(thm)],[500,220,theory(equality)])).
% cnf(511,plain,(sdtasdt0(xp,esk2_2(xp,sdtsldt0(xn,xr)))=sdtsldt0(xn,xr)|~aNaturalNumber0(sdtsldt0(xn,xr))),inference(cn,[status(thm)],[510,theory(equality)])).
% cnf(520,plain,(xn=sdtsldt0(xn,xr)|~sdtlseqdt0(xn,sdtsldt0(xn,xr))|~aNaturalNumber0(sdtsldt0(xn,xr))|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[135,249,theory(equality)])).
% cnf(522,plain,(sdtasdt0(X1,X2)=X1|sz00=X2|~sdtlseqdt0(sdtasdt0(X1,X2),X1)|~aNaturalNumber0(X1)|~aNaturalNumber0(sdtasdt0(X1,X2))|~aNaturalNumber0(X2)),inference(spm,[status(thm)],[135,166,theory(equality)])).
% cnf(538,plain,(xn=sdtsldt0(xn,xr)|~sdtlseqdt0(xn,sdtsldt0(xn,xr))|~aNaturalNumber0(sdtsldt0(xn,xr))|$false),inference(rw,[status(thm)],[520,222,theory(equality)])).
% cnf(539,plain,(xn=sdtsldt0(xn,xr)|~sdtlseqdt0(xn,sdtsldt0(xn,xr))|~aNaturalNumber0(sdtsldt0(xn,xr))),inference(cn,[status(thm)],[538,theory(equality)])).
% cnf(540,plain,(~sdtlseqdt0(xn,sdtsldt0(xn,xr))|~aNaturalNumber0(sdtsldt0(xn,xr))),inference(sr,[status(thm)],[539,250,theory(equality)])).
% cnf(543,plain,(doDivides0(X1,sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(sdtasdt0(X1,X2))),inference(er,[status(thm)],[177,theory(equality)])).
% cnf(544,plain,(doDivides0(sz10,X1)|X2!=X1|~aNaturalNumber0(X2)|~aNaturalNumber0(sz10)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[177,91,theory(equality)])).
% cnf(546,plain,(doDivides0(X1,X2)|X1!=X2|~aNaturalNumber0(sz10)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(spm,[status(thm)],[177,92,theory(equality)])).
% cnf(548,plain,(doDivides0(X1,X2)|sdtasdt0(X3,X1)!=X2|~aNaturalNumber0(X3)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(spm,[status(thm)],[177,84,theory(equality)])).
% cnf(550,plain,(doDivides0(sz10,X1)|X2!=X1|~aNaturalNumber0(X2)|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[544,64,theory(equality)])).
% cnf(551,plain,(doDivides0(sz10,X1)|X2!=X1|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[550,theory(equality)])).
% cnf(552,plain,(doDivides0(sz10,X1)|~aNaturalNumber0(X1)),inference(er,[status(thm)],[551,theory(equality)])).
% cnf(555,plain,(doDivides0(X1,X2)|X1!=X2|$false|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(rw,[status(thm)],[546,64,theory(equality)])).
% cnf(556,plain,(doDivides0(X1,X2)|X1!=X2|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(cn,[status(thm)],[555,theory(equality)])).
% cnf(557,plain,(doDivides0(X1,X1)|~aNaturalNumber0(X1)),inference(er,[status(thm)],[556,theory(equality)])).
% cnf(580,plain,(doDivides0(X1,xn)|~doDivides0(X1,xr)|~aNaturalNumber0(xr)|~aNaturalNumber0(xn)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[187,248,theory(equality)])).
% cnf(587,plain,(doDivides0(X1,xn)|~doDivides0(X1,xr)|$false|~aNaturalNumber0(xn)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[580,242,theory(equality)])).
% cnf(588,plain,(doDivides0(X1,xn)|~doDivides0(X1,xr)|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[587,222,theory(equality)])).
% cnf(589,plain,(doDivides0(X1,xn)|~doDivides0(X1,xr)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[588,theory(equality)])).
% cnf(604,plain,(doDivides0(xp,sdtpldt0(X1,sdtasdt0(xn,xm)))|~doDivides0(xp,X1)|~aNaturalNumber0(sdtasdt0(xn,xm))|~aNaturalNumber0(X1)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[190,226,theory(equality)])).
% cnf(615,plain,(doDivides0(xp,sdtpldt0(X1,sdtasdt0(xn,xm)))|~doDivides0(xp,X1)|~aNaturalNumber0(sdtasdt0(xn,xm))|~aNaturalNumber0(X1)|$false),inference(rw,[status(thm)],[604,220,theory(equality)])).
% cnf(616,plain,(doDivides0(xp,sdtpldt0(X1,sdtasdt0(xn,xm)))|~doDivides0(xp,X1)|~aNaturalNumber0(sdtasdt0(xn,xm))|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[615,theory(equality)])).
% cnf(621,plain,(doDivides0(X1,X2)|~doDivides0(X1,sdtpldt0(X2,X3))|~doDivides0(X1,X3)|~aNaturalNumber0(X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[193,73,theory(equality)])).
% cnf(630,plain,(sdtlseqdt0(sz00,X1)|X2!=X1|~aNaturalNumber0(X2)|~aNaturalNumber0(sz00)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[129,80,theory(equality)])).
% cnf(634,plain,(sdtlseqdt0(sz00,X1)|X2!=X1|~aNaturalNumber0(X2)|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[630,62,theory(equality)])).
% cnf(635,plain,(sdtlseqdt0(sz00,X1)|X2!=X1|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[634,theory(equality)])).
% cnf(636,plain,(sdtlseqdt0(sz00,X1)|~aNaturalNumber0(X1)),inference(er,[status(thm)],[635,theory(equality)])).
% cnf(640,plain,(aNaturalNumber0(sdtmndt0(X1,X2))|~sdtlseqdt0(X2,X1)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(er,[status(thm)],[259,theory(equality)])).
% cnf(660,plain,(sdtpldt0(xm,esk1_2(xm,xp))=xp|~aNaturalNumber0(xm)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[127,230,theory(equality)])).
% cnf(661,plain,(sdtpldt0(xn,esk1_2(xn,xp))=xp|~aNaturalNumber0(xn)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[127,232,theory(equality)])).
% cnf(666,plain,(sdtpldt0(X1,esk1_2(X1,X2))=X2|sdtlseqdt0(X2,X1)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(spm,[status(thm)],[127,142,theory(equality)])).
% cnf(672,plain,(sdtpldt0(xm,esk1_2(xm,xp))=xp|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[660,221,theory(equality)])).
% cnf(673,plain,(sdtpldt0(xm,esk1_2(xm,xp))=xp|$false|$false),inference(rw,[status(thm)],[672,220,theory(equality)])).
% cnf(674,plain,(sdtpldt0(xm,esk1_2(xm,xp))=xp),inference(cn,[status(thm)],[673,theory(equality)])).
% cnf(675,plain,(sdtpldt0(xn,esk1_2(xn,xp))=xp|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[661,222,theory(equality)])).
% cnf(676,plain,(sdtpldt0(xn,esk1_2(xn,xp))=xp|$false|$false),inference(rw,[status(thm)],[675,220,theory(equality)])).
% cnf(677,plain,(sdtpldt0(xn,esk1_2(xn,xp))=xp),inference(cn,[status(thm)],[676,theory(equality)])).
% cnf(682,plain,(sz00=X1|aNaturalNumber0(sdtsldt0(X2,X1))|~doDivides0(X1,X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(er,[status(thm)],[184,theory(equality)])).
% cnf(712,plain,(sdtmndt0(sdtpldt0(X1,X2),X1)=X2|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(sdtpldt0(X1,X2))),inference(er,[status(thm)],[270,theory(equality)])).
% cnf(726,plain,(sz00=X1|X2=sz10|sdtasdt0(X1,X2)!=X1|~aNaturalNumber0(sz10)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[113,92,theory(equality)])).
% cnf(738,plain,(sz00=X1|X2=sz10|sdtasdt0(X1,X2)!=X1|$false|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[726,64,theory(equality)])).
% cnf(739,plain,(sz00=X1|X2=sz10|sdtasdt0(X1,X2)!=X1|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[738,theory(equality)])).
% cnf(751,plain,(sdtlseqdt0(X1,xp)|~sdtlseqdt0(X1,xm)|~aNaturalNumber0(xm)|~aNaturalNumber0(xp)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[138,230,theory(equality)])).
% cnf(752,plain,(sdtlseqdt0(X1,xp)|~sdtlseqdt0(X1,xn)|~aNaturalNumber0(xn)|~aNaturalNumber0(xp)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[138,232,theory(equality)])).
% cnf(763,plain,(sdtlseqdt0(X1,xp)|~sdtlseqdt0(X1,xm)|$false|~aNaturalNumber0(xp)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[751,221,theory(equality)])).
% cnf(764,plain,(sdtlseqdt0(X1,xp)|~sdtlseqdt0(X1,xm)|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[763,220,theory(equality)])).
% cnf(765,plain,(sdtlseqdt0(X1,xp)|~sdtlseqdt0(X1,xm)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[764,theory(equality)])).
% cnf(766,plain,(sdtlseqdt0(X1,xp)|~sdtlseqdt0(X1,xn)|$false|~aNaturalNumber0(xp)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[752,222,theory(equality)])).
% cnf(767,plain,(sdtlseqdt0(X1,xp)|~sdtlseqdt0(X1,xn)|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[766,220,theory(equality)])).
% cnf(768,plain,(sdtlseqdt0(X1,xp)|~sdtlseqdt0(X1,xn)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[767,theory(equality)])).
% cnf(809,plain,(aNaturalNumber0(sdtasdt0(X1,sdtasdt0(X2,X3)))|~aNaturalNumber0(X3)|~aNaturalNumber0(sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[70,87,theory(equality)])).
% cnf(816,plain,(sdtasdt0(sz00,X2)=sdtasdt0(sz00,sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[87,96,theory(equality)])).
% cnf(827,plain,(sdtasdt0(sz00,X2)=sdtasdt0(sz00,sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)|$false),inference(rw,[status(thm)],[816,62,theory(equality)])).
% cnf(828,plain,(sdtasdt0(sz00,X2)=sdtasdt0(sz00,sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[827,theory(equality)])).
% cnf(920,plain,(sdtsldt0(sdtasdt0(X1,X2),X1)=X2|sz00=X1|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(sdtasdt0(X1,X2))),inference(er,[status(thm)],[273,theory(equality)])).
% cnf(1421,plain,(aNaturalNumber0(esk2_2(sz10,X1))|~aNaturalNumber0(sz10)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[176,552,theory(equality)])).
% cnf(1422,plain,(sdtasdt0(sz10,esk2_2(sz10,X1))=X1|~aNaturalNumber0(sz10)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[175,552,theory(equality)])).
% cnf(1432,plain,(aNaturalNumber0(esk2_2(sz10,X1))|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[1421,64,theory(equality)])).
% cnf(1433,plain,(aNaturalNumber0(esk2_2(sz10,X1))|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[1432,theory(equality)])).
% cnf(1434,plain,(sdtasdt0(sz10,esk2_2(sz10,X1))=X1|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[1422,64,theory(equality)])).
% cnf(1435,plain,(sdtasdt0(sz10,esk2_2(sz10,X1))=X1|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[1434,theory(equality)])).
% cnf(1835,plain,(doDivides0(sz10,xn)|~aNaturalNumber0(sz10)|~aNaturalNumber0(xr)),inference(spm,[status(thm)],[589,552,theory(equality)])).
% cnf(1842,plain,(doDivides0(sz10,xn)|$false|~aNaturalNumber0(xr)),inference(rw,[status(thm)],[1835,64,theory(equality)])).
% cnf(1843,plain,(doDivides0(sz10,xn)|$false|$false),inference(rw,[status(thm)],[1842,242,theory(equality)])).
% cnf(1844,plain,(doDivides0(sz10,xn)),inference(cn,[status(thm)],[1843,theory(equality)])).
% cnf(1849,plain,(aNaturalNumber0(esk2_2(sz10,xn))|~aNaturalNumber0(sz10)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[176,1844,theory(equality)])).
% cnf(1850,plain,(sdtasdt0(sz10,esk2_2(sz10,xn))=xn|~aNaturalNumber0(sz10)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[175,1844,theory(equality)])).
% cnf(1857,plain,(aNaturalNumber0(esk2_2(sz10,xn))|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[1849,64,theory(equality)])).
% cnf(1858,plain,(aNaturalNumber0(esk2_2(sz10,xn))|$false|$false),inference(rw,[status(thm)],[1857,222,theory(equality)])).
% cnf(1859,plain,(aNaturalNumber0(esk2_2(sz10,xn))),inference(cn,[status(thm)],[1858,theory(equality)])).
% cnf(1860,plain,(sdtasdt0(sz10,esk2_2(sz10,xn))=xn|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[1850,64,theory(equality)])).
% cnf(1861,plain,(sdtasdt0(sz10,esk2_2(sz10,xn))=xn|$false|$false),inference(rw,[status(thm)],[1860,222,theory(equality)])).
% cnf(1862,plain,(sdtasdt0(sz10,esk2_2(sz10,xn))=xn),inference(cn,[status(thm)],[1861,theory(equality)])).
% cnf(2102,plain,(xn=esk2_2(sz10,xn)|~aNaturalNumber0(esk2_2(sz10,xn))),inference(spm,[status(thm)],[91,1862,theory(equality)])).
% cnf(2153,plain,(xn=esk2_2(sz10,xn)|$false),inference(rw,[status(thm)],[2102,1859,theory(equality)])).
% cnf(2154,plain,(xn=esk2_2(sz10,xn)),inference(cn,[status(thm)],[2153,theory(equality)])).
% cnf(2155,plain,(sdtasdt0(sz10,xn)=xn),inference(rw,[status(thm)],[1862,2154,theory(equality)])).
% cnf(2165,plain,(sdtsldt0(X1,sz10)=xn|sz00=sz10|xn!=X1|~aNaturalNumber0(xn)|~aNaturalNumber0(sz10)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[273,2155,theory(equality)])).
% cnf(2198,plain,(sdtsldt0(X1,sz10)=xn|sz00=sz10|xn!=X1|$false|~aNaturalNumber0(sz10)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[2165,222,theory(equality)])).
% cnf(2199,plain,(sdtsldt0(X1,sz10)=xn|sz00=sz10|xn!=X1|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[2198,64,theory(equality)])).
% cnf(2200,plain,(sdtsldt0(X1,sz10)=xn|sz00=sz10|xn!=X1|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[2199,theory(equality)])).
% cnf(2201,plain,(sdtsldt0(X1,sz10)=xn|xn!=X1|~aNaturalNumber0(X1)),inference(sr,[status(thm)],[2200,63,theory(equality)])).
% cnf(2235,plain,(sdtsldt0(xn,sz10)=xn|~aNaturalNumber0(xn)),inference(er,[status(thm)],[2201,theory(equality)])).
% cnf(2236,plain,(sdtsldt0(xn,sz10)=xn|$false),inference(rw,[status(thm)],[2235,222,theory(equality)])).
% cnf(2237,plain,(sdtsldt0(xn,sz10)=xn),inference(cn,[status(thm)],[2236,theory(equality)])).
% cnf(2238,plain,(sz00=sz10|aNaturalNumber0(X1)|xn!=X1|~doDivides0(sz10,xn)|~aNaturalNumber0(sz10)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[184,2237,theory(equality)])).
% cnf(2240,plain,(sz00=sz10|aNaturalNumber0(X1)|xn!=X1|$false|~aNaturalNumber0(sz10)|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[2238,1844,theory(equality)])).
% cnf(2241,plain,(sz00=sz10|aNaturalNumber0(X1)|xn!=X1|$false|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[2240,64,theory(equality)])).
% cnf(2242,plain,(sz00=sz10|aNaturalNumber0(X1)|xn!=X1|$false|$false|$false),inference(rw,[status(thm)],[2241,222,theory(equality)])).
% cnf(2243,plain,(sz00=sz10|aNaturalNumber0(X1)|xn!=X1),inference(cn,[status(thm)],[2242,theory(equality)])).
% cnf(2244,plain,(aNaturalNumber0(X1)|xn!=X1),inference(sr,[status(thm)],[2243,63,theory(equality)])).
% cnf(2624,plain,(sz00=esk1_2(xm,xp)|sdtlseqdt0(sz00,sz00)),inference(spm,[status(thm)],[491,473,theory(equality)])).
% cnf(2637,plain,(aNaturalNumber0(esk2_2(xr,sdtasdt0(xn,xm)))|~aNaturalNumber0(xm)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[394,70,theory(equality)])).
% cnf(2638,plain,(aNaturalNumber0(esk2_2(xr,sdtasdt0(xn,xm)))|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[2637,221,theory(equality)])).
% cnf(2639,plain,(aNaturalNumber0(esk2_2(xr,sdtasdt0(xn,xm)))|$false|$false),inference(rw,[status(thm)],[2638,222,theory(equality)])).
% cnf(2640,plain,(aNaturalNumber0(esk2_2(xr,sdtasdt0(xn,xm)))),inference(cn,[status(thm)],[2639,theory(equality)])).
% cnf(2645,plain,(sdtpldt0(xm,sz00)=xp|sdtlseqdt0(sz00,sz00)),inference(spm,[status(thm)],[674,2624,theory(equality)])).
% cnf(2656,plain,(sdtlseqdt0(sz00,xp)|~aNaturalNumber0(sz00)|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[765,636,theory(equality)])).
% cnf(2665,plain,(sdtlseqdt0(sz00,xp)|$false|~aNaturalNumber0(xm)),inference(rw,[status(thm)],[2656,62,theory(equality)])).
% cnf(2666,plain,(sdtlseqdt0(sz00,xp)|$false|$false),inference(rw,[status(thm)],[2665,221,theory(equality)])).
% cnf(2667,plain,(sdtlseqdt0(sz00,xp)),inference(cn,[status(thm)],[2666,theory(equality)])).
% cnf(2765,plain,(aNaturalNumber0(esk1_2(sz00,xp))|~aNaturalNumber0(sz00)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[128,2667,theory(equality)])).
% cnf(2766,plain,(sdtpldt0(sz00,esk1_2(sz00,xp))=xp|~aNaturalNumber0(sz00)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[127,2667,theory(equality)])).
% cnf(2782,plain,(aNaturalNumber0(esk1_2(sz00,xp))|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[2765,62,theory(equality)])).
% cnf(2783,plain,(aNaturalNumber0(esk1_2(sz00,xp))|$false|$false),inference(rw,[status(thm)],[2782,220,theory(equality)])).
% cnf(2784,plain,(aNaturalNumber0(esk1_2(sz00,xp))),inference(cn,[status(thm)],[2783,theory(equality)])).
% cnf(2785,plain,(sdtpldt0(sz00,esk1_2(sz00,xp))=xp|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[2766,62,theory(equality)])).
% cnf(2786,plain,(sdtpldt0(sz00,esk1_2(sz00,xp))=xp|$false|$false),inference(rw,[status(thm)],[2785,220,theory(equality)])).
% cnf(2787,plain,(sdtpldt0(sz00,esk1_2(sz00,xp))=xp),inference(cn,[status(thm)],[2786,theory(equality)])).
% cnf(3042,plain,(xp=esk1_2(sz00,xp)|~aNaturalNumber0(esk1_2(sz00,xp))),inference(spm,[status(thm)],[80,2787,theory(equality)])).
% cnf(3074,plain,(xp=esk1_2(sz00,xp)|$false),inference(rw,[status(thm)],[3042,2784,theory(equality)])).
% cnf(3075,plain,(xp=esk1_2(sz00,xp)),inference(cn,[status(thm)],[3074,theory(equality)])).
% cnf(3077,plain,(sdtpldt0(sz00,xp)=xp),inference(rw,[status(thm)],[2787,3075,theory(equality)])).
% cnf(3086,plain,(sdtmndt0(X1,sz00)=xp|xp!=X1|~aNaturalNumber0(xp)|~aNaturalNumber0(sz00)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[270,3077,theory(equality)])).
% cnf(3112,plain,(sdtmndt0(X1,sz00)=xp|xp!=X1|$false|~aNaturalNumber0(sz00)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[3086,220,theory(equality)])).
% cnf(3113,plain,(sdtmndt0(X1,sz00)=xp|xp!=X1|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[3112,62,theory(equality)])).
% cnf(3114,plain,(sdtmndt0(X1,sz00)=xp|xp!=X1|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[3113,theory(equality)])).
% cnf(3163,plain,(sdtlseqdt0(X1,xp)|sdtlseqdt0(xn,X1)|~aNaturalNumber0(X1)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[768,142,theory(equality)])).
% cnf(3183,plain,(sdtlseqdt0(X1,xp)|sdtlseqdt0(xn,X1)|~aNaturalNumber0(X1)|$false),inference(rw,[status(thm)],[3163,222,theory(equality)])).
% cnf(3184,plain,(sdtlseqdt0(X1,xp)|sdtlseqdt0(xn,X1)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[3183,theory(equality)])).
% cnf(3713,plain,(xp=xm|sdtlseqdt0(sz00,sz00)|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[81,2645,theory(equality)])).
% cnf(3755,plain,(xp=xm|sdtlseqdt0(sz00,sz00)|$false),inference(rw,[status(thm)],[3713,221,theory(equality)])).
% cnf(3756,plain,(xp=xm|sdtlseqdt0(sz00,sz00)),inference(cn,[status(thm)],[3755,theory(equality)])).
% cnf(3757,plain,(sdtlseqdt0(sz00,sz00)),inference(sr,[status(thm)],[3756,231,theory(equality)])).
% cnf(3766,plain,(aNaturalNumber0(esk1_2(sz00,sz00))|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[128,3757,theory(equality)])).
% cnf(3767,plain,(sdtpldt0(sz00,esk1_2(sz00,sz00))=sz00|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[127,3757,theory(equality)])).
% cnf(3789,plain,(aNaturalNumber0(esk1_2(sz00,sz00))|$false),inference(rw,[status(thm)],[3766,62,theory(equality)])).
% cnf(3790,plain,(aNaturalNumber0(esk1_2(sz00,sz00))),inference(cn,[status(thm)],[3789,theory(equality)])).
% cnf(3791,plain,(sdtpldt0(sz00,esk1_2(sz00,sz00))=sz00|$false),inference(rw,[status(thm)],[3767,62,theory(equality)])).
% cnf(3792,plain,(sdtpldt0(sz00,esk1_2(sz00,sz00))=sz00),inference(cn,[status(thm)],[3791,theory(equality)])).
% cnf(3795,plain,(sz00=esk1_2(sz00,sz00)|~aNaturalNumber0(sz00)|~aNaturalNumber0(esk1_2(sz00,sz00))),inference(spm,[status(thm)],[117,3792,theory(equality)])).
% cnf(3806,plain,(sz00=esk1_2(sz00,sz00)|$false|~aNaturalNumber0(esk1_2(sz00,sz00))),inference(rw,[status(thm)],[3795,62,theory(equality)])).
% cnf(3807,plain,(sz00=esk1_2(sz00,sz00)|$false|$false),inference(rw,[status(thm)],[3806,3790,theory(equality)])).
% cnf(3808,plain,(sz00=esk1_2(sz00,sz00)),inference(cn,[status(thm)],[3807,theory(equality)])).
% cnf(3842,plain,(sdtpldt0(sz00,sz00)=sz00),inference(rw,[status(thm)],[3792,3808,theory(equality)])).
% cnf(3854,plain,(sdtmndt0(X1,sz00)=sz00|sz00!=X1|~aNaturalNumber0(sz00)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[270,3842,theory(equality)])).
% cnf(3873,plain,(sdtmndt0(X1,sz00)=sz00|sz00!=X1|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[3854,62,theory(equality)])).
% cnf(3874,plain,(sdtmndt0(X1,sz00)=sz00|sz00!=X1|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[3873,theory(equality)])).
% cnf(3991,plain,(sdtmndt0(sz00,sz00)=sz00|~aNaturalNumber0(sz00)),inference(er,[status(thm)],[3874,theory(equality)])).
% cnf(3992,plain,(sdtmndt0(sz00,sz00)=sz00|$false),inference(rw,[status(thm)],[3991,62,theory(equality)])).
% cnf(3993,plain,(sdtmndt0(sz00,sz00)=sz00),inference(cn,[status(thm)],[3992,theory(equality)])).
% cnf(3994,plain,(aNaturalNumber0(X1)|sz00!=X1|~sdtlseqdt0(sz00,sz00)|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[259,3993,theory(equality)])).
% cnf(3996,plain,(aNaturalNumber0(X1)|sz00!=X1|$false|~aNaturalNumber0(sz00)),inference(rw,[status(thm)],[3994,3757,theory(equality)])).
% cnf(3997,plain,(aNaturalNumber0(X1)|sz00!=X1|$false|$false),inference(rw,[status(thm)],[3996,62,theory(equality)])).
% cnf(3998,plain,(aNaturalNumber0(X1)|sz00!=X1),inference(cn,[status(thm)],[3997,theory(equality)])).
% cnf(4524,plain,(sdtmndt0(xp,sz00)=xp|~aNaturalNumber0(xp)),inference(er,[status(thm)],[3114,theory(equality)])).
% cnf(4525,plain,(sdtmndt0(xp,sz00)=xp|$false),inference(rw,[status(thm)],[4524,220,theory(equality)])).
% cnf(4526,plain,(sdtmndt0(xp,sz00)=xp),inference(cn,[status(thm)],[4525,theory(equality)])).
% cnf(4527,plain,(aNaturalNumber0(X1)|xp!=X1|~sdtlseqdt0(sz00,xp)|~aNaturalNumber0(sz00)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[259,4526,theory(equality)])).
% cnf(4529,plain,(aNaturalNumber0(X1)|xp!=X1|$false|~aNaturalNumber0(sz00)|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[4527,2667,theory(equality)])).
% cnf(4530,plain,(aNaturalNumber0(X1)|xp!=X1|$false|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[4529,62,theory(equality)])).
% cnf(4531,plain,(aNaturalNumber0(X1)|xp!=X1|$false|$false|$false),inference(rw,[status(thm)],[4530,220,theory(equality)])).
% cnf(4532,plain,(aNaturalNumber0(X1)|xp!=X1),inference(cn,[status(thm)],[4531,theory(equality)])).
% cnf(4762,plain,(sz00=sz10|sdtlseqdt0(xn,xn)|~aNaturalNumber0(sz10)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[486,2155,theory(equality)])).
% cnf(4771,plain,(sz00=sz10|sdtlseqdt0(xn,xn)|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[4762,64,theory(equality)])).
% cnf(4772,plain,(sz00=sz10|sdtlseqdt0(xn,xn)|$false|$false),inference(rw,[status(thm)],[4771,222,theory(equality)])).
% cnf(4773,plain,(sz00=sz10|sdtlseqdt0(xn,xn)),inference(cn,[status(thm)],[4772,theory(equality)])).
% cnf(4774,plain,(sdtlseqdt0(xn,xn)),inference(sr,[status(thm)],[4773,63,theory(equality)])).
% cnf(4783,plain,(aNaturalNumber0(esk1_2(xn,xn))|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[128,4774,theory(equality)])).
% cnf(4784,plain,(sdtpldt0(xn,esk1_2(xn,xn))=xn|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[127,4774,theory(equality)])).
% cnf(4787,plain,(aNaturalNumber0(esk1_2(xn,xn))|$false),inference(rw,[status(thm)],[4783,222,theory(equality)])).
% cnf(4788,plain,(aNaturalNumber0(esk1_2(xn,xn))),inference(cn,[status(thm)],[4787,theory(equality)])).
% cnf(4789,plain,(sdtpldt0(xn,esk1_2(xn,xn))=xn|$false),inference(rw,[status(thm)],[4784,222,theory(equality)])).
% cnf(4790,plain,(sdtpldt0(xn,esk1_2(xn,xn))=xn),inference(cn,[status(thm)],[4789,theory(equality)])).
% cnf(4802,plain,(esk1_2(xn,xn)=X1|xn!=sdtpldt0(xn,X1)|~aNaturalNumber0(xn)|~aNaturalNumber0(X1)|~aNaturalNumber0(esk1_2(xn,xn))),inference(spm,[status(thm)],[107,4790,theory(equality)])).
% cnf(4804,plain,(doDivides0(X1,esk1_2(xn,xn))|~doDivides0(X1,xn)|~aNaturalNumber0(xn)|~aNaturalNumber0(esk1_2(xn,xn))|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[193,4790,theory(equality)])).
% cnf(4828,plain,(esk1_2(xn,xn)=X1|xn!=sdtpldt0(xn,X1)|$false|~aNaturalNumber0(X1)|~aNaturalNumber0(esk1_2(xn,xn))),inference(rw,[status(thm)],[4802,222,theory(equality)])).
% cnf(4829,plain,(esk1_2(xn,xn)=X1|xn!=sdtpldt0(xn,X1)|$false|~aNaturalNumber0(X1)|$false),inference(rw,[status(thm)],[4828,4788,theory(equality)])).
% cnf(4830,plain,(esk1_2(xn,xn)=X1|xn!=sdtpldt0(xn,X1)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[4829,theory(equality)])).
% cnf(4834,plain,(doDivides0(X1,esk1_2(xn,xn))|~doDivides0(X1,xn)|$false|~aNaturalNumber0(esk1_2(xn,xn))|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[4804,222,theory(equality)])).
% cnf(4835,plain,(doDivides0(X1,esk1_2(xn,xn))|~doDivides0(X1,xn)|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[4834,4788,theory(equality)])).
% cnf(4836,plain,(doDivides0(X1,esk1_2(xn,xn))|~doDivides0(X1,xn)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[4835,theory(equality)])).
% cnf(4853,plain,(doDivides0(sz10,esk1_2(xn,xn))|~aNaturalNumber0(sz10)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[4836,552,theory(equality)])).
% cnf(4855,plain,(doDivides0(xn,esk1_2(xn,xn))|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[4836,557,theory(equality)])).
% cnf(4862,plain,(doDivides0(sz10,esk1_2(xn,xn))|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[4853,64,theory(equality)])).
% cnf(4863,plain,(doDivides0(sz10,esk1_2(xn,xn))|$false|$false),inference(rw,[status(thm)],[4862,222,theory(equality)])).
% cnf(4864,plain,(doDivides0(sz10,esk1_2(xn,xn))),inference(cn,[status(thm)],[4863,theory(equality)])).
% cnf(4867,plain,(doDivides0(xn,esk1_2(xn,xn))|$false),inference(rw,[status(thm)],[4855,222,theory(equality)])).
% cnf(4868,plain,(doDivides0(xn,esk1_2(xn,xn))),inference(cn,[status(thm)],[4867,theory(equality)])).
% cnf(4926,plain,(aNaturalNumber0(esk2_2(sz10,esk1_2(xn,xn)))|~aNaturalNumber0(sz10)|~aNaturalNumber0(esk1_2(xn,xn))),inference(spm,[status(thm)],[176,4864,theory(equality)])).
% cnf(4927,plain,(sdtasdt0(sz10,esk2_2(sz10,esk1_2(xn,xn)))=esk1_2(xn,xn)|~aNaturalNumber0(sz10)|~aNaturalNumber0(esk1_2(xn,xn))),inference(spm,[status(thm)],[175,4864,theory(equality)])).
% cnf(4934,plain,(aNaturalNumber0(esk2_2(sz10,esk1_2(xn,xn)))|$false|~aNaturalNumber0(esk1_2(xn,xn))),inference(rw,[status(thm)],[4926,64,theory(equality)])).
% cnf(4935,plain,(aNaturalNumber0(esk2_2(sz10,esk1_2(xn,xn)))|$false|$false),inference(rw,[status(thm)],[4934,4788,theory(equality)])).
% cnf(4936,plain,(aNaturalNumber0(esk2_2(sz10,esk1_2(xn,xn)))),inference(cn,[status(thm)],[4935,theory(equality)])).
% cnf(4937,plain,(sdtasdt0(sz10,esk2_2(sz10,esk1_2(xn,xn)))=esk1_2(xn,xn)|$false|~aNaturalNumber0(esk1_2(xn,xn))),inference(rw,[status(thm)],[4927,64,theory(equality)])).
% cnf(4938,plain,(sdtasdt0(sz10,esk2_2(sz10,esk1_2(xn,xn)))=esk1_2(xn,xn)|$false|$false),inference(rw,[status(thm)],[4937,4788,theory(equality)])).
% cnf(4939,plain,(sdtasdt0(sz10,esk2_2(sz10,esk1_2(xn,xn)))=esk1_2(xn,xn)),inference(cn,[status(thm)],[4938,theory(equality)])).
% cnf(5415,plain,(esk1_2(xn,xn)=esk2_2(sz10,esk1_2(xn,xn))|~aNaturalNumber0(esk2_2(sz10,esk1_2(xn,xn)))),inference(spm,[status(thm)],[91,4939,theory(equality)])).
% cnf(5478,plain,(esk1_2(xn,xn)=esk2_2(sz10,esk1_2(xn,xn))|$false),inference(rw,[status(thm)],[5415,4936,theory(equality)])).
% cnf(5479,plain,(esk1_2(xn,xn)=esk2_2(sz10,esk1_2(xn,xn))),inference(cn,[status(thm)],[5478,theory(equality)])).
% cnf(5590,plain,(sdtasdt0(xr,esk2_2(xr,sdtasdt0(xn,xm)))=sdtasdt0(xn,xm)|~aNaturalNumber0(xm)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[509,70,theory(equality)])).
% cnf(5591,plain,(sdtasdt0(xr,esk2_2(xr,sdtasdt0(xn,xm)))=sdtasdt0(xn,xm)|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[5590,221,theory(equality)])).
% cnf(5592,plain,(sdtasdt0(xr,esk2_2(xr,sdtasdt0(xn,xm)))=sdtasdt0(xn,xm)|$false|$false),inference(rw,[status(thm)],[5591,222,theory(equality)])).
% cnf(5593,plain,(sdtasdt0(xr,esk2_2(xr,sdtasdt0(xn,xm)))=sdtasdt0(xn,xm)),inference(cn,[status(thm)],[5592,theory(equality)])).
% cnf(5614,plain,(aNaturalNumber0(sdtasdt0(xn,xm))|~aNaturalNumber0(esk2_2(xr,sdtasdt0(xn,xm)))|~aNaturalNumber0(xr)),inference(spm,[status(thm)],[70,5593,theory(equality)])).
% cnf(5641,plain,(aNaturalNumber0(sdtasdt0(xn,xm))|$false|~aNaturalNumber0(xr)),inference(rw,[status(thm)],[5614,2640,theory(equality)])).
% cnf(5642,plain,(aNaturalNumber0(sdtasdt0(xn,xm))|$false|$false),inference(rw,[status(thm)],[5641,242,theory(equality)])).
% cnf(5643,plain,(aNaturalNumber0(sdtasdt0(xn,xm))),inference(cn,[status(thm)],[5642,theory(equality)])).
% cnf(5696,plain,(sdtasdt0(sz10,esk1_2(xn,xn))=esk1_2(xn,xn)),inference(rw,[status(thm)],[4939,5479,theory(equality)])).
% cnf(5784,plain,(esk1_2(xn,xn)=sz00|~aNaturalNumber0(sz00)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[4830,81,theory(equality)])).
% cnf(5788,plain,(esk1_2(xn,xn)=sz00|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[5784,62,theory(equality)])).
% cnf(5789,plain,(esk1_2(xn,xn)=sz00|$false|$false),inference(rw,[status(thm)],[5788,222,theory(equality)])).
% cnf(5790,plain,(esk1_2(xn,xn)=sz00),inference(cn,[status(thm)],[5789,theory(equality)])).
% cnf(5807,plain,(sdtasdt0(sz10,sz00)=esk1_2(xn,xn)),inference(rw,[status(thm)],[5696,5790,theory(equality)])).
% cnf(5808,plain,(sdtasdt0(sz10,sz00)=sz00),inference(rw,[status(thm)],[5807,5790,theory(equality)])).
% cnf(5820,plain,(doDivides0(xn,sz00)),inference(rw,[status(thm)],[4868,5790,theory(equality)])).
% cnf(5831,plain,(sdtpldt0(xn,sz00)=xn),inference(rw,[status(thm)],[4790,5790,theory(equality)])).
% cnf(5841,plain,(aNaturalNumber0(esk2_2(xn,sz00))|~aNaturalNumber0(xn)|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[176,5820,theory(equality)])).
% cnf(5842,plain,(sdtasdt0(xn,esk2_2(xn,sz00))=sz00|~aNaturalNumber0(xn)|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[175,5820,theory(equality)])).
% cnf(5849,plain,(aNaturalNumber0(esk2_2(xn,sz00))|$false|~aNaturalNumber0(sz00)),inference(rw,[status(thm)],[5841,222,theory(equality)])).
% cnf(5850,plain,(aNaturalNumber0(esk2_2(xn,sz00))|$false|$false),inference(rw,[status(thm)],[5849,62,theory(equality)])).
% cnf(5851,plain,(aNaturalNumber0(esk2_2(xn,sz00))),inference(cn,[status(thm)],[5850,theory(equality)])).
% cnf(5852,plain,(sdtasdt0(xn,esk2_2(xn,sz00))=sz00|$false|~aNaturalNumber0(sz00)),inference(rw,[status(thm)],[5842,222,theory(equality)])).
% cnf(5853,plain,(sdtasdt0(xn,esk2_2(xn,sz00))=sz00|$false|$false),inference(rw,[status(thm)],[5852,62,theory(equality)])).
% cnf(5854,plain,(sdtasdt0(xn,esk2_2(xn,sz00))=sz00),inference(cn,[status(thm)],[5853,theory(equality)])).
% cnf(5909,plain,(sdtpldt0(sz00,xn)=xn|~aNaturalNumber0(xn)|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[73,5831,theory(equality)])).
% cnf(5926,plain,(sdtpldt0(sz00,xn)=xn|$false|~aNaturalNumber0(sz00)),inference(rw,[status(thm)],[5909,222,theory(equality)])).
% cnf(5927,plain,(sdtpldt0(sz00,xn)=xn|$false|$false),inference(rw,[status(thm)],[5926,62,theory(equality)])).
% cnf(5928,plain,(sdtpldt0(sz00,xn)=xn),inference(cn,[status(thm)],[5927,theory(equality)])).
% cnf(5981,plain,(sdtlseqdt0(sz00,X1)|xn!=X1|~aNaturalNumber0(xn)|~aNaturalNumber0(sz00)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[129,5928,theory(equality)])).
% cnf(6013,plain,(sdtlseqdt0(sz00,X1)|xn!=X1|$false|~aNaturalNumber0(sz00)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[5981,222,theory(equality)])).
% cnf(6014,plain,(sdtlseqdt0(sz00,X1)|xn!=X1|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[6013,62,theory(equality)])).
% cnf(6015,plain,(sdtlseqdt0(sz00,X1)|xn!=X1|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[6014,theory(equality)])).
% cnf(6033,plain,(sz00=xn|sz00=esk2_2(xn,sz00)|~aNaturalNumber0(xn)|~aNaturalNumber0(esk2_2(xn,sz00))),inference(spm,[status(thm)],[121,5854,theory(equality)])).
% cnf(6059,plain,(sz00=xn|sz00=esk2_2(xn,sz00)|$false|~aNaturalNumber0(esk2_2(xn,sz00))),inference(rw,[status(thm)],[6033,222,theory(equality)])).
% cnf(6060,plain,(sz00=xn|sz00=esk2_2(xn,sz00)|$false|$false),inference(rw,[status(thm)],[6059,5851,theory(equality)])).
% cnf(6061,plain,(sz00=xn|sz00=esk2_2(xn,sz00)),inference(cn,[status(thm)],[6060,theory(equality)])).
% cnf(6127,plain,(sdtasdt0(xn,sz00)=sz00|xn=sz00),inference(spm,[status(thm)],[5854,6061,theory(equality)])).
% cnf(6137,plain,(sdtasdt0(sz00,sz10)=sz00|~aNaturalNumber0(sz10)|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[84,5808,theory(equality)])).
% cnf(6147,plain,(doDivides0(sz10,X1)|sz00!=X1|~aNaturalNumber0(sz00)|~aNaturalNumber0(sz10)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[177,5808,theory(equality)])).
% cnf(6153,plain,(sdtasdt0(sz00,sz10)=sz00|$false|~aNaturalNumber0(sz00)),inference(rw,[status(thm)],[6137,64,theory(equality)])).
% cnf(6154,plain,(sdtasdt0(sz00,sz10)=sz00|$false|$false),inference(rw,[status(thm)],[6153,62,theory(equality)])).
% cnf(6155,plain,(sdtasdt0(sz00,sz10)=sz00),inference(cn,[status(thm)],[6154,theory(equality)])).
% cnf(6187,plain,(doDivides0(sz10,X1)|sz00!=X1|$false|~aNaturalNumber0(sz10)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[6147,62,theory(equality)])).
% cnf(6188,plain,(doDivides0(sz10,X1)|sz00!=X1|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[6187,64,theory(equality)])).
% cnf(6189,plain,(doDivides0(sz10,X1)|sz00!=X1|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[6188,theory(equality)])).
% cnf(6213,plain,(doDivides0(sz00,X1)|sz00!=X1|~aNaturalNumber0(sz10)|~aNaturalNumber0(sz00)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[177,6155,theory(equality)])).
% cnf(6250,plain,(doDivides0(sz00,X1)|sz00!=X1|$false|~aNaturalNumber0(sz00)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[6213,64,theory(equality)])).
% cnf(6251,plain,(doDivides0(sz00,X1)|sz00!=X1|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[6250,62,theory(equality)])).
% cnf(6252,plain,(doDivides0(sz00,X1)|sz00!=X1|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[6251,theory(equality)])).
% cnf(6274,plain,(sdtasdt0(sz00,xn)=sz00|xn=sz00|~aNaturalNumber0(xn)|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[84,6127,theory(equality)])).
% cnf(6288,plain,(sdtasdt0(sz00,xn)=sz00|xn=sz00|$false|~aNaturalNumber0(sz00)),inference(rw,[status(thm)],[6274,222,theory(equality)])).
% cnf(6289,plain,(sdtasdt0(sz00,xn)=sz00|xn=sz00|$false|$false),inference(rw,[status(thm)],[6288,62,theory(equality)])).
% cnf(6290,plain,(sdtasdt0(sz00,xn)=sz00|xn=sz00),inference(cn,[status(thm)],[6289,theory(equality)])).
% cnf(6503,plain,(doDivides0(sz10,X1)|sz00!=X1),inference(csr,[status(thm)],[6189,3998])).
% cnf(6506,plain,(doDivides0(sz00,X1)|sz00!=X1),inference(csr,[status(thm)],[6252,3998])).
% cnf(6670,plain,(sdtlseqdt0(sz00,X1)|xn!=X1),inference(csr,[status(thm)],[6015,2244])).
% cnf(6671,plain,(sdtlseqdt0(sz00,xn)),inference(er,[status(thm)],[6670,theory(equality)])).
% cnf(6765,plain,(sdtlseqdt0(X1,xn)|~sdtlseqdt0(X1,sz00)|~aNaturalNumber0(sz00)|~aNaturalNumber0(xn)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[138,6671,theory(equality)])).
% cnf(6793,plain,(sdtlseqdt0(X1,xn)|~sdtlseqdt0(X1,sz00)|$false|~aNaturalNumber0(xn)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[6765,62,theory(equality)])).
% cnf(6794,plain,(sdtlseqdt0(X1,xn)|~sdtlseqdt0(X1,sz00)|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[6793,222,theory(equality)])).
% cnf(6795,plain,(sdtlseqdt0(X1,xn)|~sdtlseqdt0(X1,sz00)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[6794,theory(equality)])).
% cnf(6998,plain,(sdtasdt0(X1,X2)=X1|sz00=X2|~sdtlseqdt0(sdtasdt0(X1,X2),X1)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[522,70])).
% cnf(7012,plain,(sdtasdt0(xp,X1)=xp|sz00=X1|sdtlseqdt0(xn,sdtasdt0(xp,X1))|~aNaturalNumber0(xp)|~aNaturalNumber0(X1)|~aNaturalNumber0(sdtasdt0(xp,X1))),inference(spm,[status(thm)],[6998,3184,theory(equality)])).
% cnf(7038,plain,(sdtasdt0(xp,X1)=xp|sz00=X1|sdtlseqdt0(xn,sdtasdt0(xp,X1))|$false|~aNaturalNumber0(X1)|~aNaturalNumber0(sdtasdt0(xp,X1))),inference(rw,[status(thm)],[7012,220,theory(equality)])).
% cnf(7039,plain,(sdtasdt0(xp,X1)=xp|sz00=X1|sdtlseqdt0(xn,sdtasdt0(xp,X1))|~aNaturalNumber0(X1)|~aNaturalNumber0(sdtasdt0(xp,X1))),inference(cn,[status(thm)],[7038,theory(equality)])).
% cnf(7091,plain,(doDivides0(X1,sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[543,70])).
% cnf(7119,plain,(doDivides0(X1,sz00)|~aNaturalNumber0(sz00)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[7091,97,theory(equality)])).
% cnf(7181,plain,(doDivides0(X1,sz00)|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[7119,62,theory(equality)])).
% cnf(7182,plain,(doDivides0(X1,sz00)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[7181,theory(equality)])).
% cnf(7403,plain,(doDivides0(esk2_2(xr,xn),X1)|xn!=X1|~aNaturalNumber0(xr)|~aNaturalNumber0(esk2_2(xr,xn))|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[548,507,theory(equality)])).
% cnf(7411,plain,(doDivides0(xn,X1)|xn!=X1|~aNaturalNumber0(sz10)|~aNaturalNumber0(xn)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[548,2155,theory(equality)])).
% cnf(7425,plain,(doDivides0(esk2_2(xr,xn),X1)|xn!=X1|$false|~aNaturalNumber0(esk2_2(xr,xn))|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[7403,242,theory(equality)])).
% cnf(7426,plain,(doDivides0(esk2_2(xr,xn),X1)|xn!=X1|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[7425,392,theory(equality)])).
% cnf(7427,plain,(doDivides0(esk2_2(xr,xn),X1)|xn!=X1|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[7426,theory(equality)])).
% cnf(7446,plain,(doDivides0(xn,X1)|xn!=X1|$false|~aNaturalNumber0(xn)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[7411,64,theory(equality)])).
% cnf(7447,plain,(doDivides0(xn,X1)|xn!=X1|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[7446,222,theory(equality)])).
% cnf(7448,plain,(doDivides0(xn,X1)|xn!=X1|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[7447,theory(equality)])).
% cnf(7560,plain,(doDivides0(xn,X1)|xn!=X1),inference(csr,[status(thm)],[7448,2244])).
% cnf(7561,plain,(doDivides0(xn,xn)),inference(er,[status(thm)],[7560,theory(equality)])).
% cnf(7563,plain,(aNaturalNumber0(esk2_2(xn,xn))|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[176,7561,theory(equality)])).
% cnf(7564,plain,(sdtasdt0(xn,esk2_2(xn,xn))=xn|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[175,7561,theory(equality)])).
% cnf(7571,plain,(aNaturalNumber0(esk2_2(xn,xn))|$false),inference(rw,[status(thm)],[7563,222,theory(equality)])).
% cnf(7572,plain,(aNaturalNumber0(esk2_2(xn,xn))),inference(cn,[status(thm)],[7571,theory(equality)])).
% cnf(7573,plain,(sdtasdt0(xn,esk2_2(xn,xn))=xn|$false),inference(rw,[status(thm)],[7564,222,theory(equality)])).
% cnf(7574,plain,(sdtasdt0(xn,esk2_2(xn,xn))=xn),inference(cn,[status(thm)],[7573,theory(equality)])).
% cnf(7586,plain,(sz00=xn|esk2_2(xn,xn)=X1|xn!=sdtasdt0(xn,X1)|~aNaturalNumber0(X1)|~aNaturalNumber0(esk2_2(xn,xn))|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[113,7574,theory(equality)])).
% cnf(7595,plain,(doDivides0(esk2_2(xn,xn),X1)|xn!=X1|~aNaturalNumber0(xn)|~aNaturalNumber0(esk2_2(xn,xn))|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[548,7574,theory(equality)])).
% cnf(7620,plain,(sz00=xn|esk2_2(xn,xn)=X1|xn!=sdtasdt0(xn,X1)|~aNaturalNumber0(X1)|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[7586,7572,theory(equality)])).
% cnf(7621,plain,(sz00=xn|esk2_2(xn,xn)=X1|xn!=sdtasdt0(xn,X1)|~aNaturalNumber0(X1)|$false|$false),inference(rw,[status(thm)],[7620,222,theory(equality)])).
% cnf(7622,plain,(sz00=xn|esk2_2(xn,xn)=X1|xn!=sdtasdt0(xn,X1)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[7621,theory(equality)])).
% cnf(7648,plain,(doDivides0(esk2_2(xn,xn),X1)|xn!=X1|$false|~aNaturalNumber0(esk2_2(xn,xn))|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[7595,222,theory(equality)])).
% cnf(7649,plain,(doDivides0(esk2_2(xn,xn),X1)|xn!=X1|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[7648,7572,theory(equality)])).
% cnf(7650,plain,(doDivides0(esk2_2(xn,xn),X1)|xn!=X1|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[7649,theory(equality)])).
% cnf(7931,plain,(doDivides0(esk2_2(xn,xn),X1)|xn!=X1),inference(csr,[status(thm)],[7650,2244])).
% cnf(7932,plain,(doDivides0(esk2_2(xn,xn),xn)),inference(er,[status(thm)],[7931,theory(equality)])).
% cnf(7935,plain,(aNaturalNumber0(esk2_2(esk2_2(xn,xn),xn))|~aNaturalNumber0(esk2_2(xn,xn))|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[176,7932,theory(equality)])).
% cnf(7936,plain,(sdtasdt0(esk2_2(xn,xn),esk2_2(esk2_2(xn,xn),xn))=xn|~aNaturalNumber0(esk2_2(xn,xn))|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[175,7932,theory(equality)])).
% cnf(7946,plain,(aNaturalNumber0(esk2_2(esk2_2(xn,xn),xn))|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[7935,7572,theory(equality)])).
% cnf(7947,plain,(aNaturalNumber0(esk2_2(esk2_2(xn,xn),xn))|$false|$false),inference(rw,[status(thm)],[7946,222,theory(equality)])).
% cnf(7948,plain,(aNaturalNumber0(esk2_2(esk2_2(xn,xn),xn))),inference(cn,[status(thm)],[7947,theory(equality)])).
% cnf(7949,plain,(sdtasdt0(esk2_2(xn,xn),esk2_2(esk2_2(xn,xn),xn))=xn|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[7936,7572,theory(equality)])).
% cnf(7950,plain,(sdtasdt0(esk2_2(xn,xn),esk2_2(esk2_2(xn,xn),xn))=xn|$false|$false),inference(rw,[status(thm)],[7949,222,theory(equality)])).
% cnf(7951,plain,(sdtasdt0(esk2_2(xn,xn),esk2_2(esk2_2(xn,xn),xn))=xn),inference(cn,[status(thm)],[7950,theory(equality)])).
% cnf(8029,plain,(sz00=esk2_2(esk2_2(xn,xn),xn)|sdtlseqdt0(esk2_2(xn,xn),xn)|~aNaturalNumber0(esk2_2(esk2_2(xn,xn),xn))|~aNaturalNumber0(esk2_2(xn,xn))),inference(spm,[status(thm)],[166,7951,theory(equality)])).
% cnf(8045,plain,(doDivides0(esk2_2(esk2_2(xn,xn),xn),X1)|xn!=X1|~aNaturalNumber0(esk2_2(xn,xn))|~aNaturalNumber0(esk2_2(esk2_2(xn,xn),xn))|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[548,7951,theory(equality)])).
% cnf(8050,plain,(sz00=esk2_2(esk2_2(xn,xn),xn)|sdtlseqdt0(esk2_2(xn,xn),xn)|$false|~aNaturalNumber0(esk2_2(xn,xn))),inference(rw,[status(thm)],[8029,7948,theory(equality)])).
% cnf(8051,plain,(sz00=esk2_2(esk2_2(xn,xn),xn)|sdtlseqdt0(esk2_2(xn,xn),xn)|$false|$false),inference(rw,[status(thm)],[8050,7572,theory(equality)])).
% cnf(8052,plain,(sz00=esk2_2(esk2_2(xn,xn),xn)|sdtlseqdt0(esk2_2(xn,xn),xn)),inference(cn,[status(thm)],[8051,theory(equality)])).
% cnf(8100,plain,(doDivides0(esk2_2(esk2_2(xn,xn),xn),X1)|xn!=X1|$false|~aNaturalNumber0(esk2_2(esk2_2(xn,xn),xn))|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[8045,7572,theory(equality)])).
% cnf(8101,plain,(doDivides0(esk2_2(esk2_2(xn,xn),xn),X1)|xn!=X1|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[8100,7948,theory(equality)])).
% cnf(8102,plain,(doDivides0(esk2_2(esk2_2(xn,xn),xn),X1)|xn!=X1|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[8101,theory(equality)])).
% cnf(8337,plain,(sz00=esk2_2(sz10,X1)|sdtlseqdt0(sz10,X1)|~aNaturalNumber0(esk2_2(sz10,X1))|~aNaturalNumber0(sz10)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[166,1435,theory(equality)])).
% cnf(8353,plain,(doDivides0(esk2_2(sz10,X1),X2)|X1!=X2|~aNaturalNumber0(sz10)|~aNaturalNumber0(esk2_2(sz10,X1))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[548,1435,theory(equality)])).
% cnf(8364,plain,(sz00=esk2_2(sz10,X1)|sdtlseqdt0(sz10,X1)|~aNaturalNumber0(esk2_2(sz10,X1))|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[8337,64,theory(equality)])).
% cnf(8365,plain,(sz00=esk2_2(sz10,X1)|sdtlseqdt0(sz10,X1)|~aNaturalNumber0(esk2_2(sz10,X1))|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[8364,theory(equality)])).
% cnf(8401,plain,(doDivides0(esk2_2(sz10,X1),X2)|X1!=X2|$false|~aNaturalNumber0(esk2_2(sz10,X1))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[8353,64,theory(equality)])).
% cnf(8402,plain,(doDivides0(esk2_2(sz10,X1),X2)|X1!=X2|~aNaturalNumber0(esk2_2(sz10,X1))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[8401,theory(equality)])).
% cnf(8403,plain,(doDivides0(esk2_2(sz10,X1),X1)|~aNaturalNumber0(esk2_2(sz10,X1))|~aNaturalNumber0(X1)),inference(er,[status(thm)],[8402,theory(equality)])).
% cnf(9383,plain,(doDivides0(esk2_2(esk2_2(xn,xn),xn),X1)|xn!=X1),inference(csr,[status(thm)],[8102,2244])).
% cnf(9384,plain,(doDivides0(esk2_2(esk2_2(xn,xn),xn),xn)),inference(er,[status(thm)],[9383,theory(equality)])).
% cnf(9392,plain,(doDivides0(sz00,xn)|sdtlseqdt0(esk2_2(xn,xn),xn)),inference(spm,[status(thm)],[9384,8052,theory(equality)])).
% cnf(10137,plain,(doDivides0(xp,sdtpldt0(X1,sdtasdt0(xn,xm)))|~doDivides0(xp,X1)|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[616,5643,theory(equality)])).
% cnf(10138,plain,(doDivides0(xp,sdtpldt0(X1,sdtasdt0(xn,xm)))|~doDivides0(xp,X1)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[10137,theory(equality)])).
% cnf(10140,plain,(doDivides0(xp,sdtpldt0(sz00,sdtasdt0(xn,xm)))|~aNaturalNumber0(sz00)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[10138,7182,theory(equality)])).
% cnf(10141,plain,(doDivides0(xp,sdtpldt0(xp,sdtasdt0(xn,xm)))|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[10138,557,theory(equality)])).
% cnf(10147,plain,(doDivides0(xp,sdtpldt0(sz00,sdtasdt0(xn,xm)))|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[10140,62,theory(equality)])).
% cnf(10148,plain,(doDivides0(xp,sdtpldt0(sz00,sdtasdt0(xn,xm)))|$false|$false),inference(rw,[status(thm)],[10147,220,theory(equality)])).
% cnf(10149,plain,(doDivides0(xp,sdtpldt0(sz00,sdtasdt0(xn,xm)))),inference(cn,[status(thm)],[10148,theory(equality)])).
% cnf(10150,plain,(doDivides0(xp,sdtpldt0(xp,sdtasdt0(xn,xm)))|$false),inference(rw,[status(thm)],[10141,220,theory(equality)])).
% cnf(10151,plain,(doDivides0(xp,sdtpldt0(xp,sdtasdt0(xn,xm)))),inference(cn,[status(thm)],[10150,theory(equality)])).
% cnf(10601,plain,(doDivides0(xp,xp)|~doDivides0(xp,sdtasdt0(xn,xm))|~aNaturalNumber0(sdtasdt0(xn,xm))|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[621,10151,theory(equality)])).
% cnf(10603,plain,(doDivides0(xp,sz00)|~doDivides0(xp,sdtasdt0(xn,xm))|~aNaturalNumber0(sdtasdt0(xn,xm))|~aNaturalNumber0(sz00)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[621,10149,theory(equality)])).
% cnf(10700,plain,(doDivides0(xp,xp)|$false|~aNaturalNumber0(sdtasdt0(xn,xm))|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[10601,226,theory(equality)])).
% cnf(10701,plain,(doDivides0(xp,xp)|$false|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[10700,5643,theory(equality)])).
% cnf(10702,plain,(doDivides0(xp,xp)|$false|$false|$false),inference(rw,[status(thm)],[10701,220,theory(equality)])).
% cnf(10703,plain,(doDivides0(xp,xp)),inference(cn,[status(thm)],[10702,theory(equality)])).
% cnf(10709,plain,(doDivides0(xp,sz00)|$false|~aNaturalNumber0(sdtasdt0(xn,xm))|~aNaturalNumber0(sz00)|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[10603,226,theory(equality)])).
% cnf(10710,plain,(doDivides0(xp,sz00)|$false|$false|~aNaturalNumber0(sz00)|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[10709,5643,theory(equality)])).
% cnf(10711,plain,(doDivides0(xp,sz00)|$false|$false|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[10710,62,theory(equality)])).
% cnf(10712,plain,(doDivides0(xp,sz00)|$false|$false|$false|$false),inference(rw,[status(thm)],[10711,220,theory(equality)])).
% cnf(10713,plain,(doDivides0(xp,sz00)),inference(cn,[status(thm)],[10712,theory(equality)])).
% cnf(10798,plain,(aNaturalNumber0(esk2_2(xp,xp))|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[176,10703,theory(equality)])).
% cnf(10799,plain,(sdtasdt0(xp,esk2_2(xp,xp))=xp|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[175,10703,theory(equality)])).
% cnf(10808,plain,(aNaturalNumber0(esk2_2(xp,xp))|$false),inference(rw,[status(thm)],[10798,220,theory(equality)])).
% cnf(10809,plain,(aNaturalNumber0(esk2_2(xp,xp))),inference(cn,[status(thm)],[10808,theory(equality)])).
% cnf(10810,plain,(sdtasdt0(xp,esk2_2(xp,xp))=xp|$false),inference(rw,[status(thm)],[10799,220,theory(equality)])).
% cnf(10811,plain,(sdtasdt0(xp,esk2_2(xp,xp))=xp),inference(cn,[status(thm)],[10810,theory(equality)])).
% cnf(10825,plain,(aNaturalNumber0(esk2_2(xp,sz00))|~aNaturalNumber0(xp)|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[176,10713,theory(equality)])).
% cnf(10826,plain,(sdtasdt0(xp,esk2_2(xp,sz00))=sz00|~aNaturalNumber0(xp)|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[175,10713,theory(equality)])).
% cnf(10834,plain,(aNaturalNumber0(esk2_2(xp,sz00))|$false|~aNaturalNumber0(sz00)),inference(rw,[status(thm)],[10825,220,theory(equality)])).
% cnf(10835,plain,(aNaturalNumber0(esk2_2(xp,sz00))|$false|$false),inference(rw,[status(thm)],[10834,62,theory(equality)])).
% cnf(10836,plain,(aNaturalNumber0(esk2_2(xp,sz00))),inference(cn,[status(thm)],[10835,theory(equality)])).
% cnf(10837,plain,(sdtasdt0(xp,esk2_2(xp,sz00))=sz00|$false|~aNaturalNumber0(sz00)),inference(rw,[status(thm)],[10826,220,theory(equality)])).
% cnf(10838,plain,(sdtasdt0(xp,esk2_2(xp,sz00))=sz00|$false|$false),inference(rw,[status(thm)],[10837,62,theory(equality)])).
% cnf(10839,plain,(sdtasdt0(xp,esk2_2(xp,sz00))=sz00),inference(cn,[status(thm)],[10838,theory(equality)])).
% cnf(10866,plain,(doDivides0(esk2_2(xp,xp),X1)|xp!=X1|~aNaturalNumber0(xp)|~aNaturalNumber0(esk2_2(xp,xp))|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[548,10811,theory(equality)])).
% cnf(10921,plain,(doDivides0(esk2_2(xp,xp),X1)|xp!=X1|$false|~aNaturalNumber0(esk2_2(xp,xp))|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[10866,220,theory(equality)])).
% cnf(10922,plain,(doDivides0(esk2_2(xp,xp),X1)|xp!=X1|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[10921,10809,theory(equality)])).
% cnf(10923,plain,(doDivides0(esk2_2(xp,xp),X1)|xp!=X1|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[10922,theory(equality)])).
% cnf(10944,plain,(sz00=esk2_2(xp,sz00)|sdtlseqdt0(xp,sz00)|~aNaturalNumber0(esk2_2(xp,sz00))|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[166,10839,theory(equality)])).
% cnf(10969,plain,(sz00=esk2_2(xp,sz00)|sdtlseqdt0(xp,sz00)|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[10944,10836,theory(equality)])).
% cnf(10970,plain,(sz00=esk2_2(xp,sz00)|sdtlseqdt0(xp,sz00)|$false|$false),inference(rw,[status(thm)],[10969,220,theory(equality)])).
% cnf(10971,plain,(sz00=esk2_2(xp,sz00)|sdtlseqdt0(xp,sz00)),inference(cn,[status(thm)],[10970,theory(equality)])).
% cnf(11972,plain,(aNaturalNumber0(sdtmndt0(xp,xn))|~aNaturalNumber0(xn)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[640,232,theory(equality)])).
% cnf(12126,plain,(aNaturalNumber0(sdtmndt0(xp,xn))|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[11972,222,theory(equality)])).
% cnf(12127,plain,(aNaturalNumber0(sdtmndt0(xp,xn))|$false|$false),inference(rw,[status(thm)],[12126,220,theory(equality)])).
% cnf(12128,plain,(aNaturalNumber0(sdtmndt0(xp,xn))),inference(cn,[status(thm)],[12127,theory(equality)])).
% cnf(12460,plain,(sdtasdt0(xp,sz00)=sz00|sdtlseqdt0(xp,sz00)),inference(spm,[status(thm)],[10839,10971,theory(equality)])).
% cnf(12780,plain,(sdtlseqdt0(xp,xn)|sdtasdt0(xp,sz00)=sz00|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[6795,12460,theory(equality)])).
% cnf(12818,plain,(sdtlseqdt0(xp,xn)|sdtasdt0(xp,sz00)=sz00|$false),inference(rw,[status(thm)],[12780,220,theory(equality)])).
% cnf(12819,plain,(sdtlseqdt0(xp,xn)|sdtasdt0(xp,sz00)=sz00),inference(cn,[status(thm)],[12818,theory(equality)])).
% cnf(12820,plain,(sdtasdt0(xp,sz00)=sz00),inference(sr,[status(thm)],[12819,228,theory(equality)])).
% cnf(13467,plain,(doDivides0(esk2_2(xp,xp),X1)|xp!=X1),inference(csr,[status(thm)],[10923,4532])).
% cnf(13468,plain,(doDivides0(esk2_2(xp,xp),xp)),inference(er,[status(thm)],[13467,theory(equality)])).
% cnf(13569,plain,(sz00=xr|aNaturalNumber0(sdtsldt0(xn,xr))|~aNaturalNumber0(xr)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[682,248,theory(equality)])).
% cnf(13626,plain,(sz00=xr|aNaturalNumber0(sdtsldt0(xn,xr))|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[13569,242,theory(equality)])).
% cnf(13627,plain,(sz00=xr|aNaturalNumber0(sdtsldt0(xn,xr))|$false|$false),inference(rw,[status(thm)],[13626,222,theory(equality)])).
% cnf(13628,plain,(sz00=xr|aNaturalNumber0(sdtsldt0(xn,xr))),inference(cn,[status(thm)],[13627,theory(equality)])).
% cnf(14343,plain,(esk2_2(xn,xn)=sz10|xn=sz00|~aNaturalNumber0(sz10)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[7622,92,theory(equality)])).
% cnf(14350,plain,(esk2_2(xn,xn)=sz10|xn=sz00|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[14343,64,theory(equality)])).
% cnf(14351,plain,(esk2_2(xn,xn)=sz10|xn=sz00|$false|$false),inference(rw,[status(thm)],[14350,222,theory(equality)])).
% cnf(14352,plain,(esk2_2(xn,xn)=sz10|xn=sz00),inference(cn,[status(thm)],[14351,theory(equality)])).
% cnf(14388,plain,(doDivides0(sz00,xn)|sdtlseqdt0(sz10,xn)|xn=sz00),inference(spm,[status(thm)],[9392,14352,theory(equality)])).
% cnf(14620,plain,(doDivides0(sz00,xn)|sdtlseqdt0(sz10,xn)),inference(csr,[status(thm)],[14388,6506])).
% cnf(14625,plain,(doDivides0(X1,xn)|sdtlseqdt0(sz10,xn)|~doDivides0(X1,sz00)|~aNaturalNumber0(sz00)|~aNaturalNumber0(xn)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[187,14620,theory(equality)])).
% cnf(14641,plain,(doDivides0(X1,xn)|sdtlseqdt0(sz10,xn)|~doDivides0(X1,sz00)|$false|~aNaturalNumber0(xn)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[14625,62,theory(equality)])).
% cnf(14642,plain,(doDivides0(X1,xn)|sdtlseqdt0(sz10,xn)|~doDivides0(X1,sz00)|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[14641,222,theory(equality)])).
% cnf(14643,plain,(doDivides0(X1,xn)|sdtlseqdt0(sz10,xn)|~doDivides0(X1,sz00)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[14642,theory(equality)])).
% cnf(14691,plain,(sdtmndt0(sdtpldt0(X1,X2),X1)=X2|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[712,67])).
% cnf(14714,plain,(sdtmndt0(xp,xn)=esk1_2(xn,xp)|~aNaturalNumber0(esk1_2(xn,xp))|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[14691,677,theory(equality)])).
% cnf(14777,plain,(sdtmndt0(xp,xn)=esk1_2(xn,xp)|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[14714,476,theory(equality)])).
% cnf(14778,plain,(sdtmndt0(xp,xn)=esk1_2(xn,xp)|$false|$false),inference(rw,[status(thm)],[14777,222,theory(equality)])).
% cnf(14779,plain,(sdtmndt0(xp,xn)=esk1_2(xn,xp)),inference(cn,[status(thm)],[14778,theory(equality)])).
% cnf(14997,plain,(sdtpldt0(xn,sdtmndt0(xp,xn))=xp|sdtlseqdt0(xp,xn)|~aNaturalNumber0(xn)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[666,14779,theory(equality)])).
% cnf(15011,plain,(sdtpldt0(xn,sdtmndt0(xp,xn))=xp|sdtlseqdt0(xp,xn)|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[14997,222,theory(equality)])).
% cnf(15012,plain,(sdtpldt0(xn,sdtmndt0(xp,xn))=xp|sdtlseqdt0(xp,xn)|$false|$false),inference(rw,[status(thm)],[15011,220,theory(equality)])).
% cnf(15013,plain,(sdtpldt0(xn,sdtmndt0(xp,xn))=xp|sdtlseqdt0(xp,xn)),inference(cn,[status(thm)],[15012,theory(equality)])).
% cnf(15014,plain,(sdtpldt0(xn,sdtmndt0(xp,xn))=xp),inference(sr,[status(thm)],[15013,228,theory(equality)])).
% cnf(15085,plain,(sdtlseqdt0(xn,X1)|xp!=X1|~aNaturalNumber0(sdtmndt0(xp,xn))|~aNaturalNumber0(xn)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[129,15014,theory(equality)])).
% cnf(15144,plain,(sdtlseqdt0(xn,X1)|xp!=X1|$false|~aNaturalNumber0(xn)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[15085,12128,theory(equality)])).
% cnf(15145,plain,(sdtlseqdt0(xn,X1)|xp!=X1|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[15144,222,theory(equality)])).
% cnf(15146,plain,(sdtlseqdt0(xn,X1)|xp!=X1|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[15145,theory(equality)])).
% cnf(15188,plain,(sdtlseqdt0(xn,X1)|xp!=X1),inference(csr,[status(thm)],[15146,4532])).
% cnf(16066,plain,(esk2_2(xp,xp)=sz10|sz00=xp|~aNaturalNumber0(esk2_2(xp,xp))|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[739,10811,theory(equality)])).
% cnf(16109,plain,(esk2_2(xp,xp)=sz10|sz00=xp|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[16066,10809,theory(equality)])).
% cnf(16110,plain,(esk2_2(xp,xp)=sz10|sz00=xp|$false|$false),inference(rw,[status(thm)],[16109,220,theory(equality)])).
% cnf(16111,plain,(esk2_2(xp,xp)=sz10|sz00=xp),inference(cn,[status(thm)],[16110,theory(equality)])).
% cnf(16158,plain,(doDivides0(sz10,xp)|xp=sz00),inference(spm,[status(thm)],[13468,16111,theory(equality)])).
% cnf(16173,plain,(doDivides0(sz10,xp)),inference(csr,[status(thm)],[16158,6503])).
% cnf(16175,plain,(aNaturalNumber0(esk2_2(sz10,xp))|~aNaturalNumber0(sz10)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[176,16173,theory(equality)])).
% cnf(16176,plain,(sdtasdt0(sz10,esk2_2(sz10,xp))=xp|~aNaturalNumber0(sz10)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[175,16173,theory(equality)])).
% cnf(16185,plain,(aNaturalNumber0(esk2_2(sz10,xp))|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[16175,64,theory(equality)])).
% cnf(16186,plain,(aNaturalNumber0(esk2_2(sz10,xp))|$false|$false),inference(rw,[status(thm)],[16185,220,theory(equality)])).
% cnf(16187,plain,(aNaturalNumber0(esk2_2(sz10,xp))),inference(cn,[status(thm)],[16186,theory(equality)])).
% cnf(16188,plain,(sdtasdt0(sz10,esk2_2(sz10,xp))=xp|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[16176,64,theory(equality)])).
% cnf(16189,plain,(sdtasdt0(sz10,esk2_2(sz10,xp))=xp|$false|$false),inference(rw,[status(thm)],[16188,220,theory(equality)])).
% cnf(16190,plain,(sdtasdt0(sz10,esk2_2(sz10,xp))=xp),inference(cn,[status(thm)],[16189,theory(equality)])).
% cnf(16280,plain,(xp=esk2_2(sz10,xp)|~aNaturalNumber0(esk2_2(sz10,xp))),inference(spm,[status(thm)],[91,16190,theory(equality)])).
% cnf(16365,plain,(xp=esk2_2(sz10,xp)|$false),inference(rw,[status(thm)],[16280,16187,theory(equality)])).
% cnf(16366,plain,(xp=esk2_2(sz10,xp)),inference(cn,[status(thm)],[16365,theory(equality)])).
% cnf(16375,plain,(sdtasdt0(sz10,xp)=xp),inference(rw,[status(thm)],[16190,16366,theory(equality)])).
% cnf(27603,plain,(aNaturalNumber0(sdtasdt0(X1,sdtasdt0(X2,X3)))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(X3)),inference(csr,[status(thm)],[809,70])).
% cnf(27641,plain,(aNaturalNumber0(sdtasdt0(X1,xp))|~aNaturalNumber0(xp)|~aNaturalNumber0(sz10)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[27603,16375,theory(equality)])).
% cnf(27764,plain,(aNaturalNumber0(sdtasdt0(X1,xp))|$false|~aNaturalNumber0(sz10)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[27641,220,theory(equality)])).
% cnf(27765,plain,(aNaturalNumber0(sdtasdt0(X1,xp))|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[27764,64,theory(equality)])).
% cnf(27766,plain,(aNaturalNumber0(sdtasdt0(X1,xp))|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[27765,theory(equality)])).
% cnf(27851,plain,(aNaturalNumber0(sdtasdt0(xp,X1))|~aNaturalNumber0(X1)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[27766,84,theory(equality)])).
% cnf(27872,plain,(aNaturalNumber0(sdtasdt0(xp,X1))|~aNaturalNumber0(X1)|$false),inference(rw,[status(thm)],[27851,220,theory(equality)])).
% cnf(27873,plain,(aNaturalNumber0(sdtasdt0(xp,X1))|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[27872,theory(equality)])).
% cnf(32669,plain,(doDivides0(X1,xn)|sdtlseqdt0(sz10,xn)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[14643,7182])).
% cnf(32676,negated_conjecture,(sdtlseqdt0(sz10,xn)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[266,32669,theory(equality)])).
% cnf(32707,negated_conjecture,(sdtlseqdt0(sz10,xn)|$false),inference(rw,[status(thm)],[32676,220,theory(equality)])).
% cnf(32708,negated_conjecture,(sdtlseqdt0(sz10,xn)),inference(cn,[status(thm)],[32707,theory(equality)])).
% cnf(32738,negated_conjecture,(aNaturalNumber0(esk1_2(sz10,xn))|~aNaturalNumber0(sz10)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[128,32708,theory(equality)])).
% cnf(32739,negated_conjecture,(sdtpldt0(sz10,esk1_2(sz10,xn))=xn|~aNaturalNumber0(sz10)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[127,32708,theory(equality)])).
% cnf(32768,negated_conjecture,(aNaturalNumber0(esk1_2(sz10,xn))|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[32738,64,theory(equality)])).
% cnf(32769,negated_conjecture,(aNaturalNumber0(esk1_2(sz10,xn))|$false|$false),inference(rw,[status(thm)],[32768,222,theory(equality)])).
% cnf(32770,negated_conjecture,(aNaturalNumber0(esk1_2(sz10,xn))),inference(cn,[status(thm)],[32769,theory(equality)])).
% cnf(32771,negated_conjecture,(sdtpldt0(sz10,esk1_2(sz10,xn))=xn|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[32739,64,theory(equality)])).
% cnf(32772,negated_conjecture,(sdtpldt0(sz10,esk1_2(sz10,xn))=xn|$false|$false),inference(rw,[status(thm)],[32771,222,theory(equality)])).
% cnf(32773,negated_conjecture,(sdtpldt0(sz10,esk1_2(sz10,xn))=xn),inference(cn,[status(thm)],[32772,theory(equality)])).
% cnf(33559,negated_conjecture,(sz00=sz10|xn!=sz00|~aNaturalNumber0(sz10)|~aNaturalNumber0(esk1_2(sz10,xn))),inference(spm,[status(thm)],[118,32773,theory(equality)])).
% cnf(33601,negated_conjecture,(sz00=sz10|xn!=sz00|$false|~aNaturalNumber0(esk1_2(sz10,xn))),inference(rw,[status(thm)],[33559,64,theory(equality)])).
% cnf(33602,negated_conjecture,(sz00=sz10|xn!=sz00|$false|$false),inference(rw,[status(thm)],[33601,32770,theory(equality)])).
% cnf(33603,negated_conjecture,(sz00=sz10|xn!=sz00),inference(cn,[status(thm)],[33602,theory(equality)])).
% cnf(33604,negated_conjecture,(xn!=sz00),inference(sr,[status(thm)],[33603,63,theory(equality)])).
% cnf(33725,plain,(sdtasdt0(sz00,xn)=sz00),inference(sr,[status(thm)],[6290,33604,theory(equality)])).
% cnf(46087,plain,(doDivides0(esk2_2(xr,xn),X1)|xn!=X1),inference(csr,[status(thm)],[7427,2244])).
% cnf(46088,plain,(doDivides0(esk2_2(xr,xn),xn)),inference(er,[status(thm)],[46087,theory(equality)])).
% cnf(75795,plain,(sdtsldt0(sdtasdt0(X1,X2),X1)=X2|sz00=X1|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[920,70])).
% cnf(75805,plain,(sdtsldt0(xn,xr)=esk2_2(xr,xn)|sz00=xr|~aNaturalNumber0(esk2_2(xr,xn))|~aNaturalNumber0(xr)),inference(spm,[status(thm)],[75795,507,theory(equality)])).
% cnf(75875,plain,(sdtsldt0(xn,xr)=esk2_2(xr,xn)|sz00=xr|$false|~aNaturalNumber0(xr)),inference(rw,[status(thm)],[75805,392,theory(equality)])).
% cnf(75876,plain,(sdtsldt0(xn,xr)=esk2_2(xr,xn)|sz00=xr|$false|$false),inference(rw,[status(thm)],[75875,242,theory(equality)])).
% cnf(75877,plain,(sdtsldt0(xn,xr)=esk2_2(xr,xn)|sz00=xr),inference(cn,[status(thm)],[75876,theory(equality)])).
% cnf(80791,plain,(doDivides0(sdtsldt0(xn,xr),xn)|xr=sz00),inference(spm,[status(thm)],[46088,75877,theory(equality)])).
% cnf(292963,plain,(sdtasdt0(xp,X1)=xp|sz00=X1|sdtlseqdt0(xn,sdtasdt0(xp,X1))|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[7039,27873])).
% cnf(292964,plain,(sz00=X1|sdtlseqdt0(xn,sdtasdt0(xp,X1))|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[292963,15188])).
% cnf(349754,plain,(esk2_2(sz10,X1)=sz00|sdtlseqdt0(sz10,X1)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[8365,1433])).
% cnf(359064,plain,(doDivides0(esk2_2(sz10,X1),X1)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[8403,1433])).
% cnf(359144,plain,(doDivides0(sz00,X1)|sdtlseqdt0(sz10,X1)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[359064,349754,theory(equality)])).
% cnf(359407,plain,(doDivides0(sz00,xn)|sdtlseqdt0(sz10,xr)|~aNaturalNumber0(sz00)|~aNaturalNumber0(xr)),inference(spm,[status(thm)],[589,359144,theory(equality)])).
% cnf(359477,plain,(doDivides0(sz00,xn)|sdtlseqdt0(sz10,xr)|$false|~aNaturalNumber0(xr)),inference(rw,[status(thm)],[359407,62,theory(equality)])).
% cnf(359478,plain,(doDivides0(sz00,xn)|sdtlseqdt0(sz10,xr)|$false|$false),inference(rw,[status(thm)],[359477,242,theory(equality)])).
% cnf(359479,plain,(doDivides0(sz00,xn)|sdtlseqdt0(sz10,xr)),inference(cn,[status(thm)],[359478,theory(equality)])).
% cnf(359649,plain,(aNaturalNumber0(esk2_2(sz00,xn))|sdtlseqdt0(sz10,xr)|~aNaturalNumber0(sz00)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[176,359479,theory(equality)])).
% cnf(359650,plain,(sdtasdt0(sz00,esk2_2(sz00,xn))=xn|sdtlseqdt0(sz10,xr)|~aNaturalNumber0(sz00)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[175,359479,theory(equality)])).
% cnf(359673,plain,(aNaturalNumber0(esk2_2(sz00,xn))|sdtlseqdt0(sz10,xr)|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[359649,62,theory(equality)])).
% cnf(359674,plain,(aNaturalNumber0(esk2_2(sz00,xn))|sdtlseqdt0(sz10,xr)|$false|$false),inference(rw,[status(thm)],[359673,222,theory(equality)])).
% cnf(359675,plain,(aNaturalNumber0(esk2_2(sz00,xn))|sdtlseqdt0(sz10,xr)),inference(cn,[status(thm)],[359674,theory(equality)])).
% cnf(359676,plain,(sdtasdt0(sz00,esk2_2(sz00,xn))=xn|sdtlseqdt0(sz10,xr)|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[359650,62,theory(equality)])).
% cnf(359677,plain,(sdtasdt0(sz00,esk2_2(sz00,xn))=xn|sdtlseqdt0(sz10,xr)|$false|$false),inference(rw,[status(thm)],[359676,222,theory(equality)])).
% cnf(359678,plain,(sdtasdt0(sz00,esk2_2(sz00,xn))=xn|sdtlseqdt0(sz10,xr)),inference(cn,[status(thm)],[359677,theory(equality)])).
% cnf(368504,plain,(xn=sz00|sdtlseqdt0(sz10,xr)|~aNaturalNumber0(esk2_2(sz00,xn))),inference(spm,[status(thm)],[96,359678,theory(equality)])).
% cnf(368805,plain,(sdtlseqdt0(sz10,xr)|~aNaturalNumber0(esk2_2(sz00,xn))),inference(sr,[status(thm)],[368504,33604,theory(equality)])).
% cnf(368886,plain,(sdtlseqdt0(sz10,xr)),inference(csr,[status(thm)],[368805,359675])).
% cnf(368894,plain,(aNaturalNumber0(esk1_2(sz10,xr))|~aNaturalNumber0(sz10)|~aNaturalNumber0(xr)),inference(spm,[status(thm)],[128,368886,theory(equality)])).
% cnf(368895,plain,(sdtpldt0(sz10,esk1_2(sz10,xr))=xr|~aNaturalNumber0(sz10)|~aNaturalNumber0(xr)),inference(spm,[status(thm)],[127,368886,theory(equality)])).
% cnf(368940,plain,(aNaturalNumber0(esk1_2(sz10,xr))|$false|~aNaturalNumber0(xr)),inference(rw,[status(thm)],[368894,64,theory(equality)])).
% cnf(368941,plain,(aNaturalNumber0(esk1_2(sz10,xr))|$false|$false),inference(rw,[status(thm)],[368940,242,theory(equality)])).
% cnf(368942,plain,(aNaturalNumber0(esk1_2(sz10,xr))),inference(cn,[status(thm)],[368941,theory(equality)])).
% cnf(368943,plain,(sdtpldt0(sz10,esk1_2(sz10,xr))=xr|$false|~aNaturalNumber0(xr)),inference(rw,[status(thm)],[368895,64,theory(equality)])).
% cnf(368944,plain,(sdtpldt0(sz10,esk1_2(sz10,xr))=xr|$false|$false),inference(rw,[status(thm)],[368943,242,theory(equality)])).
% cnf(368945,plain,(sdtpldt0(sz10,esk1_2(sz10,xr))=xr),inference(cn,[status(thm)],[368944,theory(equality)])).
% cnf(369017,plain,(sz00=sz10|xr!=sz00|~aNaturalNumber0(sz10)|~aNaturalNumber0(esk1_2(sz10,xr))),inference(spm,[status(thm)],[118,368945,theory(equality)])).
% cnf(369133,plain,(sz00=sz10|xr!=sz00|$false|~aNaturalNumber0(esk1_2(sz10,xr))),inference(rw,[status(thm)],[369017,64,theory(equality)])).
% cnf(369134,plain,(sz00=sz10|xr!=sz00|$false|$false),inference(rw,[status(thm)],[369133,368942,theory(equality)])).
% cnf(369135,plain,(sz00=sz10|xr!=sz00),inference(cn,[status(thm)],[369134,theory(equality)])).
% cnf(369136,plain,(xr!=sz00),inference(sr,[status(thm)],[369135,63,theory(equality)])).
% cnf(369823,plain,(aNaturalNumber0(sdtsldt0(xn,xr))),inference(sr,[status(thm)],[13628,369136,theory(equality)])).
% cnf(369848,plain,(doDivides0(sdtsldt0(xn,xr),xn)),inference(sr,[status(thm)],[80791,369136,theory(equality)])).
% cnf(370096,plain,(~sdtlseqdt0(xn,sdtsldt0(xn,xr))|$false),inference(rw,[status(thm)],[540,369823,theory(equality)])).
% cnf(370097,plain,(~sdtlseqdt0(xn,sdtsldt0(xn,xr))),inference(cn,[status(thm)],[370096,theory(equality)])).
% cnf(370098,plain,(sdtasdt0(xp,esk2_2(xp,sdtsldt0(xn,xr)))=sdtsldt0(xn,xr)|$false),inference(rw,[status(thm)],[511,369823,theory(equality)])).
% cnf(370099,plain,(sdtasdt0(xp,esk2_2(xp,sdtsldt0(xn,xr)))=sdtsldt0(xn,xr)),inference(cn,[status(thm)],[370098,theory(equality)])).
% cnf(370106,plain,(aNaturalNumber0(esk2_2(xp,sdtsldt0(xn,xr)))|$false),inference(rw,[status(thm)],[396,369823,theory(equality)])).
% cnf(370107,plain,(aNaturalNumber0(esk2_2(xp,sdtsldt0(xn,xr)))),inference(cn,[status(thm)],[370106,theory(equality)])).
% cnf(371311,plain,(sz00=esk2_2(xp,sdtsldt0(xn,xr))|sdtlseqdt0(xn,sdtsldt0(xn,xr))|~aNaturalNumber0(esk2_2(xp,sdtsldt0(xn,xr)))),inference(spm,[status(thm)],[292964,370099,theory(equality)])).
% cnf(371904,plain,(sz00=esk2_2(xp,sdtsldt0(xn,xr))|sdtlseqdt0(xn,sdtsldt0(xn,xr))|$false),inference(rw,[status(thm)],[371311,370107,theory(equality)])).
% cnf(371905,plain,(sz00=esk2_2(xp,sdtsldt0(xn,xr))|sdtlseqdt0(xn,sdtsldt0(xn,xr))),inference(cn,[status(thm)],[371904,theory(equality)])).
% cnf(371906,plain,(esk2_2(xp,sdtsldt0(xn,xr))=sz00),inference(sr,[status(thm)],[371905,370097,theory(equality)])).
% cnf(371924,plain,(sz00=sdtsldt0(xn,xr)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[370099,371906,theory(equality)]),12820,theory(equality)])).
% cnf(371935,plain,(doDivides0(sz00,xn)),inference(rw,[status(thm)],[369848,371924,theory(equality)])).
% cnf(371993,plain,(aNaturalNumber0(esk2_2(sz00,xn))|~aNaturalNumber0(sz00)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[176,371935,theory(equality)])).
% cnf(371994,plain,(sdtasdt0(sz00,esk2_2(sz00,xn))=xn|~aNaturalNumber0(sz00)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[175,371935,theory(equality)])).
% cnf(372016,plain,(aNaturalNumber0(esk2_2(sz00,xn))|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[371993,62,theory(equality)])).
% cnf(372017,plain,(aNaturalNumber0(esk2_2(sz00,xn))|$false|$false),inference(rw,[status(thm)],[372016,222,theory(equality)])).
% cnf(372018,plain,(aNaturalNumber0(esk2_2(sz00,xn))),inference(cn,[status(thm)],[372017,theory(equality)])).
% cnf(372019,plain,(sdtasdt0(sz00,esk2_2(sz00,xn))=xn|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[371994,62,theory(equality)])).
% cnf(372020,plain,(sdtasdt0(sz00,esk2_2(sz00,xn))=xn|$false|$false),inference(rw,[status(thm)],[372019,222,theory(equality)])).
% cnf(372021,plain,(sdtasdt0(sz00,esk2_2(sz00,xn))=xn),inference(cn,[status(thm)],[372020,theory(equality)])).
% cnf(372251,plain,(sdtasdt0(sz00,xn)=sdtasdt0(sz00,esk2_2(sz00,xn))|~aNaturalNumber0(esk2_2(sz00,xn))|~aNaturalNumber0(sz00)),inference(spm,[status(thm)],[828,372021,theory(equality)])).
% cnf(372439,plain,(sz00=sdtasdt0(sz00,esk2_2(sz00,xn))|~aNaturalNumber0(esk2_2(sz00,xn))|~aNaturalNumber0(sz00)),inference(rw,[status(thm)],[372251,33725,theory(equality)])).
% cnf(372440,plain,(sz00=xn|~aNaturalNumber0(esk2_2(sz00,xn))|~aNaturalNumber0(sz00)),inference(rw,[status(thm)],[372439,372021,theory(equality)])).
% cnf(372441,plain,(sz00=xn|$false|~aNaturalNumber0(sz00)),inference(rw,[status(thm)],[372440,372018,theory(equality)])).
% cnf(372442,plain,(sz00=xn|$false|$false),inference(rw,[status(thm)],[372441,62,theory(equality)])).
% cnf(372443,plain,(sz00=xn),inference(cn,[status(thm)],[372442,theory(equality)])).
% cnf(372444,plain,($false),inference(sr,[status(thm)],[372443,33604,theory(equality)])).
% cnf(372445,plain,($false),372444,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 8331
% # ...of these trivial : 687
% # ...subsumed : 3536
% # ...remaining for further processing: 4108
% # Other redundant clauses eliminated : 81
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 215
% # Backward-rewritten : 907
% # Generated clauses : 114687
% # ...of the previous two non-trivial : 98007
% # Contextual simplify-reflections : 1623
% # Paramodulations : 114077
% # Factorizations : 18
% # Equation resolutions : 365
% # Current number of processed clauses: 2667
% # Positive orientable unit clauses: 1118
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 98
% # Non-unit-clauses : 1451
% # Current number of unprocessed clauses: 66964
% # ...number of literals in the above : 308298
% # Clause-clause subsumption calls (NU) : 53963
% # Rec. Clause-clause subsumption calls : 22270
% # Unit Clause-clause subsumption calls : 1683
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 1216
% # Indexed BW rewrite successes : 259
% # Backwards rewriting index: 2464 leaves, 1.22+/-0.994 terms/leaf
% # Paramod-from index: 1511 leaves, 1.24+/-0.995 terms/leaf
% # Paramod-into index: 2300 leaves, 1.21+/-0.957 terms/leaf
% # -------------------------------------------------
% # User time : 5.638 s
% # System time : 0.206 s
% # Total time : 5.844 s
% # Maximum resident set size: 0 pages
% PrfWatch: 10.47 CPU 10.69 WC
% FINAL PrfWatch: 10.47 CPU 10.69 WC
% SZS output end Solution for /tmp/SystemOnTPTP3668/NUM518+1.tptp
%
%------------------------------------------------------------------------------