%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NUM511+3 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art01.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Wed Dec 29 19:45:40 EST 2010
% Result : Theorem 9.51s
% Output : Solution 9.51s
% 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/SystemOnTPTP11034/NUM511+3.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP11034/NUM511+3.tptp
% SZS output start Solution for /tmp/SystemOnTPTP11034/NUM511+3.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 11130
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% PrfWatch: 1.92 CPU 2.03 WC
% PrfWatch: 3.90 CPU 4.04 WC
% # Preprocessing time : 0.034 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 5.90 CPU 6.04 WC
% PrfWatch: 7.89 CPU 8.05 WC
% # SZS output start CNFRefutation.
% fof(2, axiom,(aNaturalNumber0(sz10)&~(sz10=sz00)),file('/tmp/SRASS.s.p', mSortsC_01)).
% fof(4, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>aNaturalNumber0(sdtasdt0(X1,X2))),file('/tmp/SRASS.s.p', mSortsB_02)).
% fof(8, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>sdtasdt0(X1,X2)=sdtasdt0(X2,X1)),file('/tmp/SRASS.s.p', mMulComm)).
% fof(9, axiom,![X1]:![X2]:![X3]:(((aNaturalNumber0(X1)&aNaturalNumber0(X2))&aNaturalNumber0(X3))=>sdtasdt0(sdtasdt0(X1,X2),X3)=sdtasdt0(X1,sdtasdt0(X2,X3))),file('/tmp/SRASS.s.p', mMulAsso)).
% fof(10, axiom,![X1]:(aNaturalNumber0(X1)=>(sdtasdt0(X1,sz10)=X1&X1=sdtasdt0(sz10,X1))),file('/tmp/SRASS.s.p', m_MulUnit)).
% fof(12, axiom,![X1]:![X2]:![X3]:(((aNaturalNumber0(X1)&aNaturalNumber0(X2))&aNaturalNumber0(X3))=>(sdtasdt0(X1,sdtpldt0(X2,X3))=sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))&sdtasdt0(sdtpldt0(X2,X3),X1)=sdtpldt0(sdtasdt0(X2,X1),sdtasdt0(X3,X1)))),file('/tmp/SRASS.s.p', mAMDistr)).
% 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(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(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(32, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>((doDivides0(X1,X2)&~(X2=sz00))=>sdtlseqdt0(X1,X2))),file('/tmp/SRASS.s.p', mDivLE)).
% fof(33, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>((~(X1=sz00)&doDivides0(X1,X2))=>![X3]:(aNaturalNumber0(X3)=>sdtasdt0(X3,sdtsldt0(X2,X1))=sdtsldt0(sdtasdt0(X3,X2),X1)))),file('/tmp/SRASS.s.p', mDivAsso)).
% fof(34, axiom,![X1]:(aNaturalNumber0(X1)=>(isPrime0(X1)<=>((~(X1=sz00)&~(X1=sz10))&![X2]:((aNaturalNumber0(X2)&doDivides0(X2,X1))=>(X2=sz10|X2=X1))))),file('/tmp/SRASS.s.p', mDefPrime)).
% fof(35, axiom,![X1]:(((aNaturalNumber0(X1)&~(X1=sz00))&~(X1=sz10))=>?[X2]:((aNaturalNumber0(X2)&doDivides0(X2,X1))&isPrime0(X2))),file('/tmp/SRASS.s.p', mPrimDiv)).
% fof(36, axiom,((aNaturalNumber0(xn)&aNaturalNumber0(xm))&aNaturalNumber0(xp)),file('/tmp/SRASS.s.p', m__1837)).
% fof(38, axiom,(((((~(xp=sz00)&~(xp=sz10))&![X1]:((aNaturalNumber0(X1)&(?[X2]:(aNaturalNumber0(X2)&xp=sdtasdt0(X1,X2))|doDivides0(X1,xp)))=>(X1=sz10|X1=xp)))&isPrime0(xp))&?[X1]:(aNaturalNumber0(X1)&sdtasdt0(xn,xm)=sdtasdt0(xp,X1)))&doDivides0(xp,sdtasdt0(xn,xm))),file('/tmp/SRASS.s.p', m__1860)).
% fof(42, axiom,((aNaturalNumber0(xk)&sdtasdt0(xn,xm)=sdtasdt0(xp,xk))&xk=sdtsldt0(sdtasdt0(xn,xm),xp)),file('/tmp/SRASS.s.p', m__2306)).
% fof(43, axiom,~((xk=sz00|xk=sz10)),file('/tmp/SRASS.s.p', m__2315)).
% fof(45, axiom,((((((aNaturalNumber0(xr)&?[X1]:(aNaturalNumber0(X1)&xk=sdtasdt0(xr,X1)))&doDivides0(xr,xk))&~(xr=sz00))&~(xr=sz10))&![X1]:((aNaturalNumber0(X1)&(?[X2]:(aNaturalNumber0(X2)&xr=sdtasdt0(X1,X2))|doDivides0(X1,xr)))=>(X1=sz10|X1=xr)))&isPrime0(xr)),file('/tmp/SRASS.s.p', m__2342)).
% fof(46, axiom,((?[X1]:(aNaturalNumber0(X1)&sdtpldt0(xr,X1)=xk)&?[X1]:(aNaturalNumber0(X1)&sdtasdt0(xn,xm)=sdtasdt0(xr,X1)))&doDivides0(xr,sdtasdt0(xn,xm))),file('/tmp/SRASS.s.p', m__2362)).
% fof(49, axiom,(?[X1]:(aNaturalNumber0(X1)&xn=sdtasdt0(xr,X1))&doDivides0(xr,xn)),file('/tmp/SRASS.s.p', m__2487)).
% fof(50, axiom,((((~(((aNaturalNumber0(sdtsldt0(xn,xr))&xn=sdtasdt0(xr,sdtsldt0(xn,xr)))=>sdtsldt0(xn,xr)=xn))&aNaturalNumber0(sdtsldt0(xn,xr)))&xn=sdtasdt0(xr,sdtsldt0(xn,xr)))&?[X1]:(aNaturalNumber0(X1)&sdtpldt0(sdtsldt0(xn,xr),X1)=xn))&sdtlseqdt0(sdtsldt0(xn,xr),xn)),file('/tmp/SRASS.s.p', m__2504)).
% fof(54, conjecture,((aNaturalNumber0(sdtsldt0(xn,xr))&xn=sdtasdt0(xr,sdtsldt0(xn,xr)))=>(?[X1]:(aNaturalNumber0(X1)&sdtasdt0(sdtsldt0(xn,xr),xm)=sdtasdt0(xp,X1))|doDivides0(xp,sdtasdt0(sdtsldt0(xn,xr),xm)))),file('/tmp/SRASS.s.p', m__)).
% fof(55, negated_conjecture,~(((aNaturalNumber0(sdtsldt0(xn,xr))&xn=sdtasdt0(xr,sdtsldt0(xn,xr)))=>(?[X1]:(aNaturalNumber0(X1)&sdtasdt0(sdtsldt0(xn,xr),xm)=sdtasdt0(xp,X1))|doDivides0(xp,sdtasdt0(sdtsldt0(xn,xr),xm))))),inference(assume_negation,[status(cth)],[54])).
% cnf(60,plain,(aNaturalNumber0(sz10)),inference(split_conjunct,[status(thm)],[2])).
% fof(64, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|aNaturalNumber0(sdtasdt0(X1,X2))),inference(fof_nnf,[status(thm)],[4])).
% fof(65, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|aNaturalNumber0(sdtasdt0(X3,X4))),inference(variable_rename,[status(thm)],[64])).
% cnf(66,plain,(aNaturalNumber0(sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[65])).
% fof(78, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|sdtasdt0(X1,X2)=sdtasdt0(X2,X1)),inference(fof_nnf,[status(thm)],[8])).
% fof(79, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|sdtasdt0(X3,X4)=sdtasdt0(X4,X3)),inference(variable_rename,[status(thm)],[78])).
% cnf(80,plain,(sdtasdt0(X1,X2)=sdtasdt0(X2,X1)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[79])).
% fof(81, 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(82, 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)],[81])).
% cnf(83,plain,(sdtasdt0(sdtasdt0(X1,X2),X3)=sdtasdt0(X1,sdtasdt0(X2,X3))|~aNaturalNumber0(X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[82])).
% fof(84, plain,![X1]:(~(aNaturalNumber0(X1))|(sdtasdt0(X1,sz10)=X1&X1=sdtasdt0(sz10,X1))),inference(fof_nnf,[status(thm)],[10])).
% fof(85, plain,![X2]:(~(aNaturalNumber0(X2))|(sdtasdt0(X2,sz10)=X2&X2=sdtasdt0(sz10,X2))),inference(variable_rename,[status(thm)],[84])).
% fof(86, plain,![X2]:((sdtasdt0(X2,sz10)=X2|~(aNaturalNumber0(X2)))&(X2=sdtasdt0(sz10,X2)|~(aNaturalNumber0(X2)))),inference(distribute,[status(thm)],[85])).
% cnf(87,plain,(X1=sdtasdt0(sz10,X1)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[86])).
% cnf(88,plain,(sdtasdt0(X1,sz10)=X1|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[86])).
% fof(94, plain,![X1]:![X2]:![X3]:(((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|~(aNaturalNumber0(X3)))|(sdtasdt0(X1,sdtpldt0(X2,X3))=sdtpldt0(sdtasdt0(X1,X2),sdtasdt0(X1,X3))&sdtasdt0(sdtpldt0(X2,X3),X1)=sdtpldt0(sdtasdt0(X2,X1),sdtasdt0(X3,X1)))),inference(fof_nnf,[status(thm)],[12])).
% fof(95, plain,![X4]:![X5]:![X6]:(((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|~(aNaturalNumber0(X6)))|(sdtasdt0(X4,sdtpldt0(X5,X6))=sdtpldt0(sdtasdt0(X4,X5),sdtasdt0(X4,X6))&sdtasdt0(sdtpldt0(X5,X6),X4)=sdtpldt0(sdtasdt0(X5,X4),sdtasdt0(X6,X4)))),inference(variable_rename,[status(thm)],[94])).
% fof(96, plain,![X4]:![X5]:![X6]:((sdtasdt0(X4,sdtpldt0(X5,X6))=sdtpldt0(sdtasdt0(X4,X5),sdtasdt0(X4,X6))|((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|~(aNaturalNumber0(X6))))&(sdtasdt0(sdtpldt0(X5,X6),X4)=sdtpldt0(sdtasdt0(X5,X4),sdtasdt0(X6,X4))|((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|~(aNaturalNumber0(X6))))),inference(distribute,[status(thm)],[95])).
% cnf(97,plain,(sdtasdt0(sdtpldt0(X2,X1),X3)=sdtpldt0(sdtasdt0(X2,X3),sdtasdt0(X1,X3))|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~aNaturalNumber0(X3)),inference(split_conjunct,[status(thm)],[96])).
% fof(104, 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(105, 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)],[104])).
% fof(106, 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)],[105])).
% fof(107, 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)],[106])).
% cnf(108,plain,(X1=sz00|X3=X2|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~aNaturalNumber0(X3)|sdtasdt0(X3,X1)!=sdtasdt0(X2,X1)),inference(split_conjunct,[status(thm)],[107])).
% cnf(109,plain,(X1=sz00|X3=X2|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~aNaturalNumber0(X3)|sdtasdt0(X1,X3)!=sdtasdt0(X1,X2)),inference(split_conjunct,[status(thm)],[107])).
% fof(115, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|(~(sdtasdt0(X1,X2)=sz00)|(X1=sz00|X2=sz00))),inference(fof_nnf,[status(thm)],[16])).
% fof(116, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|(~(sdtasdt0(X3,X4)=sz00)|(X3=sz00|X4=sz00))),inference(variable_rename,[status(thm)],[115])).
% cnf(117,plain,(X1=sz00|X2=sz00|sdtasdt0(X2,X1)!=sz00|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(split_conjunct,[status(thm)],[116])).
% fof(118, 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(119, 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)],[118])).
% fof(120, 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)],[119])).
% fof(121, 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)],[120])).
% fof(122, 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)],[121])).
% cnf(123,plain,(sdtpldt0(X2,esk1_2(X2,X1))=X1|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~sdtlseqdt0(X2,X1)),inference(split_conjunct,[status(thm)],[122])).
% cnf(124,plain,(aNaturalNumber0(esk1_2(X2,X1))|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~sdtlseqdt0(X2,X1)),inference(split_conjunct,[status(thm)],[122])).
% fof(166, 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(167, 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)],[166])).
% fof(168, 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)],[167])).
% fof(169, 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)],[168])).
% fof(170, 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)],[169])).
% cnf(171,plain,(X1=sdtasdt0(X2,esk2_2(X2,X1))|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~doDivides0(X2,X1)),inference(split_conjunct,[status(thm)],[170])).
% cnf(172,plain,(aNaturalNumber0(esk2_2(X2,X1))|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~doDivides0(X2,X1)),inference(split_conjunct,[status(thm)],[170])).
% cnf(173,plain,(doDivides0(X2,X1)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|X1!=sdtasdt0(X2,X3)|~aNaturalNumber0(X3)),inference(split_conjunct,[status(thm)],[170])).
% fof(174, 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(175, 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)],[174])).
% fof(176, 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)],[175])).
% fof(177, 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)],[176])).
% cnf(178,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)],[177])).
% cnf(179,plain,(X2=sz00|X1=sdtasdt0(X2,X3)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~doDivides0(X2,X1)|X3!=sdtsldt0(X1,X2)),inference(split_conjunct,[status(thm)],[177])).
% cnf(180,plain,(X2=sz00|aNaturalNumber0(X3)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~doDivides0(X2,X1)|X3!=sdtsldt0(X1,X2)),inference(split_conjunct,[status(thm)],[177])).
% fof(181, 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(182, plain,![X4]:![X5]:![X6]:(((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|~(aNaturalNumber0(X6)))|((~(doDivides0(X4,X5))|~(doDivides0(X5,X6)))|doDivides0(X4,X6))),inference(variable_rename,[status(thm)],[181])).
% cnf(183,plain,(doDivides0(X1,X2)|~doDivides0(X3,X2)|~doDivides0(X1,X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X3)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[182])).
% fof(190, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|((~(doDivides0(X1,X2))|X2=sz00)|sdtlseqdt0(X1,X2))),inference(fof_nnf,[status(thm)],[32])).
% fof(191, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|((~(doDivides0(X3,X4))|X4=sz00)|sdtlseqdt0(X3,X4))),inference(variable_rename,[status(thm)],[190])).
% cnf(192,plain,(sdtlseqdt0(X1,X2)|X2=sz00|~doDivides0(X1,X2)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[191])).
% fof(193, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|((X1=sz00|~(doDivides0(X1,X2)))|![X3]:(~(aNaturalNumber0(X3))|sdtasdt0(X3,sdtsldt0(X2,X1))=sdtsldt0(sdtasdt0(X3,X2),X1)))),inference(fof_nnf,[status(thm)],[33])).
% fof(194, plain,![X4]:![X5]:((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|((X4=sz00|~(doDivides0(X4,X5)))|![X6]:(~(aNaturalNumber0(X6))|sdtasdt0(X6,sdtsldt0(X5,X4))=sdtsldt0(sdtasdt0(X6,X5),X4)))),inference(variable_rename,[status(thm)],[193])).
% fof(195, plain,![X4]:![X5]:![X6]:(((~(aNaturalNumber0(X6))|sdtasdt0(X6,sdtsldt0(X5,X4))=sdtsldt0(sdtasdt0(X6,X5),X4))|(X4=sz00|~(doDivides0(X4,X5))))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))),inference(shift_quantors,[status(thm)],[194])).
% cnf(196,plain,(X2=sz00|sdtasdt0(X3,sdtsldt0(X1,X2))=sdtsldt0(sdtasdt0(X3,X1),X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~doDivides0(X2,X1)|~aNaturalNumber0(X3)),inference(split_conjunct,[status(thm)],[195])).
% fof(197, plain,![X1]:(~(aNaturalNumber0(X1))|((~(isPrime0(X1))|((~(X1=sz00)&~(X1=sz10))&![X2]:((~(aNaturalNumber0(X2))|~(doDivides0(X2,X1)))|(X2=sz10|X2=X1))))&(((X1=sz00|X1=sz10)|?[X2]:((aNaturalNumber0(X2)&doDivides0(X2,X1))&(~(X2=sz10)&~(X2=X1))))|isPrime0(X1)))),inference(fof_nnf,[status(thm)],[34])).
% fof(198, plain,![X3]:(~(aNaturalNumber0(X3))|((~(isPrime0(X3))|((~(X3=sz00)&~(X3=sz10))&![X4]:((~(aNaturalNumber0(X4))|~(doDivides0(X4,X3)))|(X4=sz10|X4=X3))))&(((X3=sz00|X3=sz10)|?[X5]:((aNaturalNumber0(X5)&doDivides0(X5,X3))&(~(X5=sz10)&~(X5=X3))))|isPrime0(X3)))),inference(variable_rename,[status(thm)],[197])).
% fof(199, plain,![X3]:(~(aNaturalNumber0(X3))|((~(isPrime0(X3))|((~(X3=sz00)&~(X3=sz10))&![X4]:((~(aNaturalNumber0(X4))|~(doDivides0(X4,X3)))|(X4=sz10|X4=X3))))&(((X3=sz00|X3=sz10)|((aNaturalNumber0(esk3_1(X3))&doDivides0(esk3_1(X3),X3))&(~(esk3_1(X3)=sz10)&~(esk3_1(X3)=X3))))|isPrime0(X3)))),inference(skolemize,[status(esa)],[198])).
% fof(200, plain,![X3]:![X4]:((((((~(aNaturalNumber0(X4))|~(doDivides0(X4,X3)))|(X4=sz10|X4=X3))&(~(X3=sz00)&~(X3=sz10)))|~(isPrime0(X3)))&(((X3=sz00|X3=sz10)|((aNaturalNumber0(esk3_1(X3))&doDivides0(esk3_1(X3),X3))&(~(esk3_1(X3)=sz10)&~(esk3_1(X3)=X3))))|isPrime0(X3)))|~(aNaturalNumber0(X3))),inference(shift_quantors,[status(thm)],[199])).
% fof(201, plain,![X3]:![X4]:((((((~(aNaturalNumber0(X4))|~(doDivides0(X4,X3)))|(X4=sz10|X4=X3))|~(isPrime0(X3)))|~(aNaturalNumber0(X3)))&(((~(X3=sz00)|~(isPrime0(X3)))|~(aNaturalNumber0(X3)))&((~(X3=sz10)|~(isPrime0(X3)))|~(aNaturalNumber0(X3)))))&(((((aNaturalNumber0(esk3_1(X3))|(X3=sz00|X3=sz10))|isPrime0(X3))|~(aNaturalNumber0(X3)))&(((doDivides0(esk3_1(X3),X3)|(X3=sz00|X3=sz10))|isPrime0(X3))|~(aNaturalNumber0(X3))))&((((~(esk3_1(X3)=sz10)|(X3=sz00|X3=sz10))|isPrime0(X3))|~(aNaturalNumber0(X3)))&(((~(esk3_1(X3)=X3)|(X3=sz00|X3=sz10))|isPrime0(X3))|~(aNaturalNumber0(X3)))))),inference(distribute,[status(thm)],[200])).
% cnf(206,plain,(~aNaturalNumber0(X1)|~isPrime0(X1)|X1!=sz10),inference(split_conjunct,[status(thm)],[201])).
% fof(209, plain,![X1]:(((~(aNaturalNumber0(X1))|X1=sz00)|X1=sz10)|?[X2]:((aNaturalNumber0(X2)&doDivides0(X2,X1))&isPrime0(X2))),inference(fof_nnf,[status(thm)],[35])).
% fof(210, plain,![X3]:(((~(aNaturalNumber0(X3))|X3=sz00)|X3=sz10)|?[X4]:((aNaturalNumber0(X4)&doDivides0(X4,X3))&isPrime0(X4))),inference(variable_rename,[status(thm)],[209])).
% fof(211, plain,![X3]:(((~(aNaturalNumber0(X3))|X3=sz00)|X3=sz10)|((aNaturalNumber0(esk4_1(X3))&doDivides0(esk4_1(X3),X3))&isPrime0(esk4_1(X3)))),inference(skolemize,[status(esa)],[210])).
% fof(212, plain,![X3]:(((aNaturalNumber0(esk4_1(X3))|((~(aNaturalNumber0(X3))|X3=sz00)|X3=sz10))&(doDivides0(esk4_1(X3),X3)|((~(aNaturalNumber0(X3))|X3=sz00)|X3=sz10)))&(isPrime0(esk4_1(X3))|((~(aNaturalNumber0(X3))|X3=sz00)|X3=sz10))),inference(distribute,[status(thm)],[211])).
% cnf(213,plain,(X1=sz10|X1=sz00|isPrime0(esk4_1(X1))|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[212])).
% cnf(214,plain,(X1=sz10|X1=sz00|doDivides0(esk4_1(X1),X1)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[212])).
% cnf(215,plain,(X1=sz10|X1=sz00|aNaturalNumber0(esk4_1(X1))|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[212])).
% cnf(216,plain,(aNaturalNumber0(xp)),inference(split_conjunct,[status(thm)],[36])).
% cnf(217,plain,(aNaturalNumber0(xm)),inference(split_conjunct,[status(thm)],[36])).
% cnf(218,plain,(aNaturalNumber0(xn)),inference(split_conjunct,[status(thm)],[36])).
% fof(350, plain,(((((~(xp=sz00)&~(xp=sz10))&![X1]:((~(aNaturalNumber0(X1))|(![X2]:(~(aNaturalNumber0(X2))|~(xp=sdtasdt0(X1,X2)))&~(doDivides0(X1,xp))))|(X1=sz10|X1=xp)))&isPrime0(xp))&?[X1]:(aNaturalNumber0(X1)&sdtasdt0(xn,xm)=sdtasdt0(xp,X1)))&doDivides0(xp,sdtasdt0(xn,xm))),inference(fof_nnf,[status(thm)],[38])).
% fof(351, plain,(((((~(xp=sz00)&~(xp=sz10))&![X3]:((~(aNaturalNumber0(X3))|(![X4]:(~(aNaturalNumber0(X4))|~(xp=sdtasdt0(X3,X4)))&~(doDivides0(X3,xp))))|(X3=sz10|X3=xp)))&isPrime0(xp))&?[X5]:(aNaturalNumber0(X5)&sdtasdt0(xn,xm)=sdtasdt0(xp,X5)))&doDivides0(xp,sdtasdt0(xn,xm))),inference(variable_rename,[status(thm)],[350])).
% fof(352, plain,(((((~(xp=sz00)&~(xp=sz10))&![X3]:((~(aNaturalNumber0(X3))|(![X4]:(~(aNaturalNumber0(X4))|~(xp=sdtasdt0(X3,X4)))&~(doDivides0(X3,xp))))|(X3=sz10|X3=xp)))&isPrime0(xp))&(aNaturalNumber0(esk9_0)&sdtasdt0(xn,xm)=sdtasdt0(xp,esk9_0)))&doDivides0(xp,sdtasdt0(xn,xm))),inference(skolemize,[status(esa)],[351])).
% fof(353, plain,![X3]:![X4]:((((((((~(aNaturalNumber0(X4))|~(xp=sdtasdt0(X3,X4)))&~(doDivides0(X3,xp)))|~(aNaturalNumber0(X3)))|(X3=sz10|X3=xp))&(~(xp=sz00)&~(xp=sz10)))&isPrime0(xp))&(aNaturalNumber0(esk9_0)&sdtasdt0(xn,xm)=sdtasdt0(xp,esk9_0)))&doDivides0(xp,sdtasdt0(xn,xm))),inference(shift_quantors,[status(thm)],[352])).
% fof(354, plain,![X3]:![X4]:((((((((~(aNaturalNumber0(X4))|~(xp=sdtasdt0(X3,X4)))|~(aNaturalNumber0(X3)))|(X3=sz10|X3=xp))&((~(doDivides0(X3,xp))|~(aNaturalNumber0(X3)))|(X3=sz10|X3=xp)))&(~(xp=sz00)&~(xp=sz10)))&isPrime0(xp))&(aNaturalNumber0(esk9_0)&sdtasdt0(xn,xm)=sdtasdt0(xp,esk9_0)))&doDivides0(xp,sdtasdt0(xn,xm))),inference(distribute,[status(thm)],[353])).
% cnf(355,plain,(doDivides0(xp,sdtasdt0(xn,xm))),inference(split_conjunct,[status(thm)],[354])).
% cnf(360,plain,(xp!=sz00),inference(split_conjunct,[status(thm)],[354])).
% cnf(383,plain,(xk=sdtsldt0(sdtasdt0(xn,xm),xp)),inference(split_conjunct,[status(thm)],[42])).
% cnf(384,plain,(sdtasdt0(xn,xm)=sdtasdt0(xp,xk)),inference(split_conjunct,[status(thm)],[42])).
% cnf(385,plain,(aNaturalNumber0(xk)),inference(split_conjunct,[status(thm)],[42])).
% fof(386, plain,(~(xk=sz00)&~(xk=sz10)),inference(fof_nnf,[status(thm)],[43])).
% cnf(388,plain,(xk!=sz00),inference(split_conjunct,[status(thm)],[386])).
% fof(391, plain,((((((aNaturalNumber0(xr)&?[X1]:(aNaturalNumber0(X1)&xk=sdtasdt0(xr,X1)))&doDivides0(xr,xk))&~(xr=sz00))&~(xr=sz10))&![X1]:((~(aNaturalNumber0(X1))|(![X2]:(~(aNaturalNumber0(X2))|~(xr=sdtasdt0(X1,X2)))&~(doDivides0(X1,xr))))|(X1=sz10|X1=xr)))&isPrime0(xr)),inference(fof_nnf,[status(thm)],[45])).
% fof(392, plain,((((((aNaturalNumber0(xr)&?[X3]:(aNaturalNumber0(X3)&xk=sdtasdt0(xr,X3)))&doDivides0(xr,xk))&~(xr=sz00))&~(xr=sz10))&![X4]:((~(aNaturalNumber0(X4))|(![X5]:(~(aNaturalNumber0(X5))|~(xr=sdtasdt0(X4,X5)))&~(doDivides0(X4,xr))))|(X4=sz10|X4=xr)))&isPrime0(xr)),inference(variable_rename,[status(thm)],[391])).
% fof(393, plain,((((((aNaturalNumber0(xr)&(aNaturalNumber0(esk12_0)&xk=sdtasdt0(xr,esk12_0)))&doDivides0(xr,xk))&~(xr=sz00))&~(xr=sz10))&![X4]:((~(aNaturalNumber0(X4))|(![X5]:(~(aNaturalNumber0(X5))|~(xr=sdtasdt0(X4,X5)))&~(doDivides0(X4,xr))))|(X4=sz10|X4=xr)))&isPrime0(xr)),inference(skolemize,[status(esa)],[392])).
% fof(394, plain,![X4]:![X5]:((((((~(aNaturalNumber0(X5))|~(xr=sdtasdt0(X4,X5)))&~(doDivides0(X4,xr)))|~(aNaturalNumber0(X4)))|(X4=sz10|X4=xr))&((((aNaturalNumber0(xr)&(aNaturalNumber0(esk12_0)&xk=sdtasdt0(xr,esk12_0)))&doDivides0(xr,xk))&~(xr=sz00))&~(xr=sz10)))&isPrime0(xr)),inference(shift_quantors,[status(thm)],[393])).
% fof(395, plain,![X4]:![X5]:((((((~(aNaturalNumber0(X5))|~(xr=sdtasdt0(X4,X5)))|~(aNaturalNumber0(X4)))|(X4=sz10|X4=xr))&((~(doDivides0(X4,xr))|~(aNaturalNumber0(X4)))|(X4=sz10|X4=xr)))&((((aNaturalNumber0(xr)&(aNaturalNumber0(esk12_0)&xk=sdtasdt0(xr,esk12_0)))&doDivides0(xr,xk))&~(xr=sz00))&~(xr=sz10)))&isPrime0(xr)),inference(distribute,[status(thm)],[394])).
% cnf(397,plain,(xr!=sz10),inference(split_conjunct,[status(thm)],[395])).
% cnf(398,plain,(xr!=sz00),inference(split_conjunct,[status(thm)],[395])).
% cnf(399,plain,(doDivides0(xr,xk)),inference(split_conjunct,[status(thm)],[395])).
% cnf(400,plain,(xk=sdtasdt0(xr,esk12_0)),inference(split_conjunct,[status(thm)],[395])).
% cnf(401,plain,(aNaturalNumber0(esk12_0)),inference(split_conjunct,[status(thm)],[395])).
% cnf(402,plain,(aNaturalNumber0(xr)),inference(split_conjunct,[status(thm)],[395])).
% cnf(403,plain,(X1=xr|X1=sz10|~aNaturalNumber0(X1)|~doDivides0(X1,xr)),inference(split_conjunct,[status(thm)],[395])).
% cnf(404,plain,(X1=xr|X1=sz10|~aNaturalNumber0(X1)|xr!=sdtasdt0(X1,X2)|~aNaturalNumber0(X2)),inference(split_conjunct,[status(thm)],[395])).
% fof(405, plain,((?[X2]:(aNaturalNumber0(X2)&sdtpldt0(xr,X2)=xk)&?[X3]:(aNaturalNumber0(X3)&sdtasdt0(xn,xm)=sdtasdt0(xr,X3)))&doDivides0(xr,sdtasdt0(xn,xm))),inference(variable_rename,[status(thm)],[46])).
% fof(406, plain,(((aNaturalNumber0(esk13_0)&sdtpldt0(xr,esk13_0)=xk)&(aNaturalNumber0(esk14_0)&sdtasdt0(xn,xm)=sdtasdt0(xr,esk14_0)))&doDivides0(xr,sdtasdt0(xn,xm))),inference(skolemize,[status(esa)],[405])).
% cnf(407,plain,(doDivides0(xr,sdtasdt0(xn,xm))),inference(split_conjunct,[status(thm)],[406])).
% cnf(408,plain,(sdtasdt0(xn,xm)=sdtasdt0(xr,esk14_0)),inference(split_conjunct,[status(thm)],[406])).
% cnf(409,plain,(aNaturalNumber0(esk14_0)),inference(split_conjunct,[status(thm)],[406])).
% fof(430, plain,(?[X2]:(aNaturalNumber0(X2)&xn=sdtasdt0(xr,X2))&doDivides0(xr,xn)),inference(variable_rename,[status(thm)],[49])).
% fof(431, plain,((aNaturalNumber0(esk18_0)&xn=sdtasdt0(xr,esk18_0))&doDivides0(xr,xn)),inference(skolemize,[status(esa)],[430])).
% cnf(432,plain,(doDivides0(xr,xn)),inference(split_conjunct,[status(thm)],[431])).
% cnf(433,plain,(xn=sdtasdt0(xr,esk18_0)),inference(split_conjunct,[status(thm)],[431])).
% cnf(434,plain,(aNaturalNumber0(esk18_0)),inference(split_conjunct,[status(thm)],[431])).
% fof(435, plain,((((((aNaturalNumber0(sdtsldt0(xn,xr))&xn=sdtasdt0(xr,sdtsldt0(xn,xr)))&~(sdtsldt0(xn,xr)=xn))&aNaturalNumber0(sdtsldt0(xn,xr)))&xn=sdtasdt0(xr,sdtsldt0(xn,xr)))&?[X1]:(aNaturalNumber0(X1)&sdtpldt0(sdtsldt0(xn,xr),X1)=xn))&sdtlseqdt0(sdtsldt0(xn,xr),xn)),inference(fof_nnf,[status(thm)],[50])).
% fof(436, plain,((((((aNaturalNumber0(sdtsldt0(xn,xr))&xn=sdtasdt0(xr,sdtsldt0(xn,xr)))&~(sdtsldt0(xn,xr)=xn))&aNaturalNumber0(sdtsldt0(xn,xr)))&xn=sdtasdt0(xr,sdtsldt0(xn,xr)))&?[X2]:(aNaturalNumber0(X2)&sdtpldt0(sdtsldt0(xn,xr),X2)=xn))&sdtlseqdt0(sdtsldt0(xn,xr),xn)),inference(variable_rename,[status(thm)],[435])).
% fof(437, plain,((((((aNaturalNumber0(sdtsldt0(xn,xr))&xn=sdtasdt0(xr,sdtsldt0(xn,xr)))&~(sdtsldt0(xn,xr)=xn))&aNaturalNumber0(sdtsldt0(xn,xr)))&xn=sdtasdt0(xr,sdtsldt0(xn,xr)))&(aNaturalNumber0(esk19_0)&sdtpldt0(sdtsldt0(xn,xr),esk19_0)=xn))&sdtlseqdt0(sdtsldt0(xn,xr),xn)),inference(skolemize,[status(esa)],[436])).
% cnf(441,plain,(xn=sdtasdt0(xr,sdtsldt0(xn,xr))),inference(split_conjunct,[status(thm)],[437])).
% cnf(442,plain,(aNaturalNumber0(sdtsldt0(xn,xr))),inference(split_conjunct,[status(thm)],[437])).
% fof(457, negated_conjecture,((aNaturalNumber0(sdtsldt0(xn,xr))&xn=sdtasdt0(xr,sdtsldt0(xn,xr)))&(![X1]:(~(aNaturalNumber0(X1))|~(sdtasdt0(sdtsldt0(xn,xr),xm)=sdtasdt0(xp,X1)))&~(doDivides0(xp,sdtasdt0(sdtsldt0(xn,xr),xm))))),inference(fof_nnf,[status(thm)],[55])).
% fof(458, negated_conjecture,((aNaturalNumber0(sdtsldt0(xn,xr))&xn=sdtasdt0(xr,sdtsldt0(xn,xr)))&(![X2]:(~(aNaturalNumber0(X2))|~(sdtasdt0(sdtsldt0(xn,xr),xm)=sdtasdt0(xp,X2)))&~(doDivides0(xp,sdtasdt0(sdtsldt0(xn,xr),xm))))),inference(variable_rename,[status(thm)],[457])).
% fof(459, negated_conjecture,![X2]:(((~(aNaturalNumber0(X2))|~(sdtasdt0(sdtsldt0(xn,xr),xm)=sdtasdt0(xp,X2)))&~(doDivides0(xp,sdtasdt0(sdtsldt0(xn,xr),xm))))&(aNaturalNumber0(sdtsldt0(xn,xr))&xn=sdtasdt0(xr,sdtsldt0(xn,xr)))),inference(shift_quantors,[status(thm)],[458])).
% cnf(462,negated_conjecture,(~doDivides0(xp,sdtasdt0(sdtsldt0(xn,xr),xm))),inference(split_conjunct,[status(thm)],[459])).
% cnf(485,plain,(aNaturalNumber0(sdtasdt0(xn,xm))|~aNaturalNumber0(xk)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[66,384,theory(equality)])).
% cnf(486,plain,(aNaturalNumber0(sdtasdt0(xn,xm))|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[485,385,theory(equality)])).
% cnf(487,plain,(aNaturalNumber0(sdtasdt0(xn,xm))|$false|$false),inference(rw,[status(thm)],[486,216,theory(equality)])).
% cnf(488,plain,(aNaturalNumber0(sdtasdt0(xn,xm))),inference(cn,[status(thm)],[487,theory(equality)])).
% cnf(514,plain,(~isPrime0(sz10)|~aNaturalNumber0(sz10)),inference(er,[status(thm)],[206,theory(equality)])).
% cnf(515,plain,(~isPrime0(sz10)|$false),inference(rw,[status(thm)],[514,60,theory(equality)])).
% cnf(516,plain,(~isPrime0(sz10)),inference(cn,[status(thm)],[515,theory(equality)])).
% cnf(569,negated_conjecture,(~doDivides0(xp,sdtasdt0(xm,sdtsldt0(xn,xr)))|~aNaturalNumber0(sdtsldt0(xn,xr))|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[462,80,theory(equality)])).
% cnf(581,negated_conjecture,(~doDivides0(xp,sdtasdt0(xm,sdtsldt0(xn,xr)))|$false|~aNaturalNumber0(xm)),inference(rw,[status(thm)],[569,442,theory(equality)])).
% cnf(582,negated_conjecture,(~doDivides0(xp,sdtasdt0(xm,sdtsldt0(xn,xr)))|$false|$false),inference(rw,[status(thm)],[581,217,theory(equality)])).
% cnf(583,negated_conjecture,(~doDivides0(xp,sdtasdt0(xm,sdtsldt0(xn,xr)))),inference(cn,[status(thm)],[582,theory(equality)])).
% cnf(695,plain,(doDivides0(X1,sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(sdtasdt0(X1,X2))),inference(er,[status(thm)],[173,theory(equality)])).
% cnf(705,plain,(doDivides0(sz10,X1)|X2!=X1|~aNaturalNumber0(X2)|~aNaturalNumber0(sz10)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[173,87,theory(equality)])).
% cnf(709,plain,(doDivides0(X1,X2)|sdtasdt0(X3,X1)!=X2|~aNaturalNumber0(X3)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(spm,[status(thm)],[173,80,theory(equality)])).
% cnf(735,plain,(doDivides0(sz10,X1)|X2!=X1|~aNaturalNumber0(X2)|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[705,60,theory(equality)])).
% cnf(736,plain,(doDivides0(sz10,X1)|X2!=X1|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[735,theory(equality)])).
% cnf(737,plain,(doDivides0(sz10,X1)|~aNaturalNumber0(X1)),inference(er,[status(thm)],[736,theory(equality)])).
% cnf(803,plain,(xr=X1|sz10=X1|sdtasdt0(X2,X1)!=xr|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[404,80,theory(equality)])).
% cnf(822,plain,(xr=esk4_1(xr)|sz10=esk4_1(xr)|sz10=xr|sz00=xr|~aNaturalNumber0(esk4_1(xr))|~aNaturalNumber0(xr)),inference(spm,[status(thm)],[403,214,theory(equality)])).
% cnf(825,plain,(xr=esk4_1(xr)|sz10=esk4_1(xr)|sz10=xr|sz00=xr|~aNaturalNumber0(esk4_1(xr))|$false),inference(rw,[status(thm)],[822,402,theory(equality)])).
% cnf(826,plain,(xr=esk4_1(xr)|sz10=esk4_1(xr)|sz10=xr|sz00=xr|~aNaturalNumber0(esk4_1(xr))),inference(cn,[status(thm)],[825,theory(equality)])).
% cnf(827,plain,(esk4_1(xr)=xr|esk4_1(xr)=sz10|xr=sz00|~aNaturalNumber0(esk4_1(xr))),inference(sr,[status(thm)],[826,397,theory(equality)])).
% cnf(828,plain,(esk4_1(xr)=xr|esk4_1(xr)=sz10|~aNaturalNumber0(esk4_1(xr))),inference(sr,[status(thm)],[827,398,theory(equality)])).
% cnf(864,plain,(doDivides0(X1,xn)|~doDivides0(X1,xr)|~aNaturalNumber0(xr)|~aNaturalNumber0(xn)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[183,432,theory(equality)])).
% cnf(876,plain,(doDivides0(X1,xn)|~doDivides0(X1,xr)|$false|~aNaturalNumber0(xn)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[864,402,theory(equality)])).
% cnf(877,plain,(doDivides0(X1,xn)|~doDivides0(X1,xr)|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[876,218,theory(equality)])).
% cnf(878,plain,(doDivides0(X1,xn)|~doDivides0(X1,xr)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[877,theory(equality)])).
% cnf(986,plain,(sz00=xk|sz00=xp|sdtasdt0(xn,xm)!=sz00|~aNaturalNumber0(xp)|~aNaturalNumber0(xk)),inference(spm,[status(thm)],[117,384,theory(equality)])).
% cnf(1020,plain,(sz00=xk|sz00=xp|sdtasdt0(xn,xm)!=sz00|$false|~aNaturalNumber0(xk)),inference(rw,[status(thm)],[986,216,theory(equality)])).
% cnf(1021,plain,(sz00=xk|sz00=xp|sdtasdt0(xn,xm)!=sz00|$false|$false),inference(rw,[status(thm)],[1020,385,theory(equality)])).
% cnf(1022,plain,(sz00=xk|sz00=xp|sdtasdt0(xn,xm)!=sz00),inference(cn,[status(thm)],[1021,theory(equality)])).
% cnf(1023,plain,(sz00=xp|sdtasdt0(xn,xm)!=sz00),inference(sr,[status(thm)],[1022,388,theory(equality)])).
% cnf(1024,plain,(sdtasdt0(xn,xm)!=sz00),inference(sr,[status(thm)],[1023,360,theory(equality)])).
% cnf(1034,plain,(sz00=sdtasdt0(xn,xm)|sdtlseqdt0(xr,sdtasdt0(xn,xm))|~aNaturalNumber0(sdtasdt0(xn,xm))|~aNaturalNumber0(xr)),inference(spm,[status(thm)],[192,407,theory(equality)])).
% cnf(1049,plain,(sz00=sdtasdt0(xn,xm)|sdtlseqdt0(xr,sdtasdt0(xn,xm))|~aNaturalNumber0(sdtasdt0(xn,xm))|$false),inference(rw,[status(thm)],[1034,402,theory(equality)])).
% cnf(1050,plain,(sz00=sdtasdt0(xn,xm)|sdtlseqdt0(xr,sdtasdt0(xn,xm))|~aNaturalNumber0(sdtasdt0(xn,xm))),inference(cn,[status(thm)],[1049,theory(equality)])).
% cnf(1053,plain,(sz00=X1|aNaturalNumber0(sdtsldt0(X2,X1))|~doDivides0(X1,X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(er,[status(thm)],[180,theory(equality)])).
% cnf(1054,plain,(sz00=xp|aNaturalNumber0(X1)|xk!=X1|~doDivides0(xp,sdtasdt0(xn,xm))|~aNaturalNumber0(xp)|~aNaturalNumber0(sdtasdt0(xn,xm))),inference(spm,[status(thm)],[180,383,theory(equality)])).
% cnf(1055,plain,(sz00=xp|aNaturalNumber0(X1)|xk!=X1|$false|~aNaturalNumber0(xp)|~aNaturalNumber0(sdtasdt0(xn,xm))),inference(rw,[status(thm)],[1054,355,theory(equality)])).
% cnf(1056,plain,(sz00=xp|aNaturalNumber0(X1)|xk!=X1|$false|$false|~aNaturalNumber0(sdtasdt0(xn,xm))),inference(rw,[status(thm)],[1055,216,theory(equality)])).
% cnf(1057,plain,(sz00=xp|aNaturalNumber0(X1)|xk!=X1|~aNaturalNumber0(sdtasdt0(xn,xm))),inference(cn,[status(thm)],[1056,theory(equality)])).
% cnf(1058,plain,(aNaturalNumber0(X1)|xk!=X1|~aNaturalNumber0(sdtasdt0(xn,xm))),inference(sr,[status(thm)],[1057,360,theory(equality)])).
% cnf(1195,plain,(sdtasdt0(sdtasdt0(X2,X1),X3)=sdtasdt0(X1,sdtasdt0(X2,X3))|~aNaturalNumber0(X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[83,80,theory(equality)])).
% cnf(1534,plain,(sz00=xr|X1=esk18_0|sdtasdt0(xr,X1)!=xn|~aNaturalNumber0(esk18_0)|~aNaturalNumber0(X1)|~aNaturalNumber0(xr)),inference(spm,[status(thm)],[109,433,theory(equality)])).
% cnf(1538,plain,(sz00=xr|X1=esk14_0|sdtasdt0(xr,X1)!=sdtasdt0(xn,xm)|~aNaturalNumber0(esk14_0)|~aNaturalNumber0(X1)|~aNaturalNumber0(xr)),inference(spm,[status(thm)],[109,408,theory(equality)])).
% cnf(1564,plain,(sz00=xr|X1=esk18_0|sdtasdt0(xr,X1)!=xn|$false|~aNaturalNumber0(X1)|~aNaturalNumber0(xr)),inference(rw,[status(thm)],[1534,434,theory(equality)])).
% cnf(1565,plain,(sz00=xr|X1=esk18_0|sdtasdt0(xr,X1)!=xn|$false|~aNaturalNumber0(X1)|$false),inference(rw,[status(thm)],[1564,402,theory(equality)])).
% cnf(1566,plain,(sz00=xr|X1=esk18_0|sdtasdt0(xr,X1)!=xn|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[1565,theory(equality)])).
% cnf(1567,plain,(X1=esk18_0|sdtasdt0(xr,X1)!=xn|~aNaturalNumber0(X1)),inference(sr,[status(thm)],[1566,398,theory(equality)])).
% cnf(1577,plain,(sz00=xr|X1=esk14_0|sdtasdt0(xr,X1)!=sdtasdt0(xn,xm)|$false|~aNaturalNumber0(X1)|~aNaturalNumber0(xr)),inference(rw,[status(thm)],[1538,409,theory(equality)])).
% cnf(1578,plain,(sz00=xr|X1=esk14_0|sdtasdt0(xr,X1)!=sdtasdt0(xn,xm)|$false|~aNaturalNumber0(X1)|$false),inference(rw,[status(thm)],[1577,402,theory(equality)])).
% cnf(1579,plain,(sz00=xr|X1=esk14_0|sdtasdt0(xr,X1)!=sdtasdt0(xn,xm)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[1578,theory(equality)])).
% cnf(1580,plain,(X1=esk14_0|sdtasdt0(xr,X1)!=sdtasdt0(xn,xm)|~aNaturalNumber0(X1)),inference(sr,[status(thm)],[1579,398,theory(equality)])).
% cnf(1644,plain,(sdtasdt0(X1,sdtsldt0(X2,X1))=X2|sz00=X1|~doDivides0(X1,X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(er,[status(thm)],[179,theory(equality)])).
% cnf(1650,plain,(sdtsldt0(X1,X2)=X3|sz00=X2|sdtasdt0(X2,X3)!=X1|~aNaturalNumber0(X3)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[178,173])).
% cnf(1657,plain,(sdtsldt0(X1,xr)=esk12_0|sz00=xr|xk!=X1|~aNaturalNumber0(esk12_0)|~aNaturalNumber0(xr)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[1650,400,theory(equality)])).
% cnf(1684,plain,(sdtsldt0(X1,xr)=esk12_0|sz00=xr|xk!=X1|$false|~aNaturalNumber0(xr)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[1657,401,theory(equality)])).
% cnf(1685,plain,(sdtsldt0(X1,xr)=esk12_0|sz00=xr|xk!=X1|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[1684,402,theory(equality)])).
% cnf(1686,plain,(sdtsldt0(X1,xr)=esk12_0|sz00=xr|xk!=X1|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[1685,theory(equality)])).
% cnf(1687,plain,(sdtsldt0(X1,xr)=esk12_0|xk!=X1|~aNaturalNumber0(X1)),inference(sr,[status(thm)],[1686,398,theory(equality)])).
% cnf(1909,plain,(sdtpldt0(sdtasdt0(X1,sz10),X2)=sdtasdt0(sdtpldt0(X1,X2),sz10)|~aNaturalNumber0(sz10)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(spm,[status(thm)],[97,88,theory(equality)])).
% cnf(1957,plain,(sdtpldt0(sdtasdt0(X1,sz10),X2)=sdtasdt0(sdtpldt0(X1,X2),sz10)|$false|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(rw,[status(thm)],[1909,60,theory(equality)])).
% cnf(1958,plain,(sdtpldt0(sdtasdt0(X1,sz10),X2)=sdtasdt0(sdtpldt0(X1,X2),sz10)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(cn,[status(thm)],[1957,theory(equality)])).
% cnf(2030,plain,(sdtsldt0(sdtasdt0(X1,xk),xr)=sdtasdt0(X1,sdtsldt0(xk,xr))|sz00=xr|~aNaturalNumber0(X1)|~aNaturalNumber0(xr)|~aNaturalNumber0(xk)),inference(spm,[status(thm)],[196,399,theory(equality)])).
% cnf(2033,plain,(sdtsldt0(sdtasdt0(X1,xn),xr)=sdtasdt0(X1,sdtsldt0(xn,xr))|sz00=xr|~aNaturalNumber0(X1)|~aNaturalNumber0(xr)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[196,432,theory(equality)])).
% cnf(2036,plain,(sdtsldt0(sdtasdt0(X1,xk),xr)=sdtasdt0(X1,sdtsldt0(xk,xr))|sz00=xr|~aNaturalNumber0(X1)|$false|~aNaturalNumber0(xk)),inference(rw,[status(thm)],[2030,402,theory(equality)])).
% cnf(2037,plain,(sdtsldt0(sdtasdt0(X1,xk),xr)=sdtasdt0(X1,sdtsldt0(xk,xr))|sz00=xr|~aNaturalNumber0(X1)|$false|$false),inference(rw,[status(thm)],[2036,385,theory(equality)])).
% cnf(2038,plain,(sdtsldt0(sdtasdt0(X1,xk),xr)=sdtasdt0(X1,sdtsldt0(xk,xr))|sz00=xr|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[2037,theory(equality)])).
% cnf(2039,plain,(sdtsldt0(sdtasdt0(X1,xk),xr)=sdtasdt0(X1,sdtsldt0(xk,xr))|~aNaturalNumber0(X1)),inference(sr,[status(thm)],[2038,398,theory(equality)])).
% cnf(2048,plain,(sdtsldt0(sdtasdt0(X1,xn),xr)=sdtasdt0(X1,sdtsldt0(xn,xr))|sz00=xr|~aNaturalNumber0(X1)|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[2033,402,theory(equality)])).
% cnf(2049,plain,(sdtsldt0(sdtasdt0(X1,xn),xr)=sdtasdt0(X1,sdtsldt0(xn,xr))|sz00=xr|~aNaturalNumber0(X1)|$false|$false),inference(rw,[status(thm)],[2048,218,theory(equality)])).
% cnf(2050,plain,(sdtsldt0(sdtasdt0(X1,xn),xr)=sdtasdt0(X1,sdtsldt0(xn,xr))|sz00=xr|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[2049,theory(equality)])).
% cnf(2051,plain,(sdtsldt0(sdtasdt0(X1,xn),xr)=sdtasdt0(X1,sdtsldt0(xn,xr))|~aNaturalNumber0(X1)),inference(sr,[status(thm)],[2050,398,theory(equality)])).
% cnf(13055,plain,(doDivides0(sz10,xn)|~aNaturalNumber0(sz10)|~aNaturalNumber0(xr)),inference(spm,[status(thm)],[878,737,theory(equality)])).
% cnf(13064,plain,(doDivides0(sz10,xn)|$false|~aNaturalNumber0(xr)),inference(rw,[status(thm)],[13055,60,theory(equality)])).
% cnf(13065,plain,(doDivides0(sz10,xn)|$false|$false),inference(rw,[status(thm)],[13064,402,theory(equality)])).
% cnf(13066,plain,(doDivides0(sz10,xn)),inference(cn,[status(thm)],[13065,theory(equality)])).
% cnf(13071,plain,(aNaturalNumber0(esk2_2(sz10,xn))|~aNaturalNumber0(sz10)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[172,13066,theory(equality)])).
% cnf(13072,plain,(sdtasdt0(sz10,esk2_2(sz10,xn))=xn|~aNaturalNumber0(sz10)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[171,13066,theory(equality)])).
% cnf(13079,plain,(aNaturalNumber0(esk2_2(sz10,xn))|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[13071,60,theory(equality)])).
% cnf(13080,plain,(aNaturalNumber0(esk2_2(sz10,xn))|$false|$false),inference(rw,[status(thm)],[13079,218,theory(equality)])).
% cnf(13081,plain,(aNaturalNumber0(esk2_2(sz10,xn))),inference(cn,[status(thm)],[13080,theory(equality)])).
% cnf(13082,plain,(sdtasdt0(sz10,esk2_2(sz10,xn))=xn|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[13072,60,theory(equality)])).
% cnf(13083,plain,(sdtasdt0(sz10,esk2_2(sz10,xn))=xn|$false|$false),inference(rw,[status(thm)],[13082,218,theory(equality)])).
% cnf(13084,plain,(sdtasdt0(sz10,esk2_2(sz10,xn))=xn),inference(cn,[status(thm)],[13083,theory(equality)])).
% cnf(13105,plain,(sdtsldt0(xn,xr)=esk18_0|~aNaturalNumber0(sdtsldt0(xn,xr))),inference(spm,[status(thm)],[1567,441,theory(equality)])).
% cnf(13122,plain,(sdtsldt0(xn,xr)=esk18_0|$false),inference(rw,[status(thm)],[13105,442,theory(equality)])).
% cnf(13123,plain,(sdtsldt0(xn,xr)=esk18_0),inference(cn,[status(thm)],[13122,theory(equality)])).
% cnf(13135,negated_conjecture,(~doDivides0(xp,sdtasdt0(xm,esk18_0))),inference(rw,[status(thm)],[583,13123,theory(equality)])).
% cnf(14343,plain,(aNaturalNumber0(X1)|xk!=X1|$false),inference(rw,[status(thm)],[1058,488,theory(equality)])).
% cnf(14344,plain,(aNaturalNumber0(X1)|xk!=X1),inference(cn,[status(thm)],[14343,theory(equality)])).
% cnf(14488,plain,(xn=esk2_2(sz10,xn)|~aNaturalNumber0(esk2_2(sz10,xn))),inference(spm,[status(thm)],[87,13084,theory(equality)])).
% cnf(14887,plain,(xn=esk2_2(sz10,xn)|$false),inference(rw,[status(thm)],[14488,13081,theory(equality)])).
% cnf(14888,plain,(xn=esk2_2(sz10,xn)),inference(cn,[status(thm)],[14887,theory(equality)])).
% cnf(15572,plain,(sdtasdt0(sz10,xn)=xn),inference(rw,[status(thm)],[13084,14888,theory(equality)])).
% cnf(15575,plain,(sdtasdt0(xn,sz10)=xn|~aNaturalNumber0(sz10)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[80,15572,theory(equality)])).
% cnf(15710,plain,(sdtasdt0(xn,sz10)=xn|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[15575,60,theory(equality)])).
% cnf(15711,plain,(sdtasdt0(xn,sz10)=xn|$false|$false),inference(rw,[status(thm)],[15710,218,theory(equality)])).
% cnf(15712,plain,(sdtasdt0(xn,sz10)=xn),inference(cn,[status(thm)],[15711,theory(equality)])).
% cnf(17953,plain,(sdtsldt0(X1,xr)=esk12_0|xk!=X1),inference(csr,[status(thm)],[1687,14344])).
% cnf(17954,plain,(sdtsldt0(xk,xr)=esk12_0),inference(er,[status(thm)],[17953,theory(equality)])).
% cnf(17969,plain,(doDivides0(X1,sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[695,66])).
% cnf(25726,plain,(esk4_1(xr)=sz10|esk4_1(xr)=xr|sz10=xr|sz00=xr|~aNaturalNumber0(xr)),inference(spm,[status(thm)],[828,215,theory(equality)])).
% cnf(25727,plain,(esk4_1(xr)=sz10|esk4_1(xr)=xr|sz10=xr|sz00=xr|$false),inference(rw,[status(thm)],[25726,402,theory(equality)])).
% cnf(25728,plain,(esk4_1(xr)=sz10|esk4_1(xr)=xr|sz10=xr|sz00=xr),inference(cn,[status(thm)],[25727,theory(equality)])).
% cnf(25729,plain,(esk4_1(xr)=sz10|esk4_1(xr)=xr|xr=sz00),inference(sr,[status(thm)],[25728,397,theory(equality)])).
% cnf(25730,plain,(esk4_1(xr)=sz10|esk4_1(xr)=xr),inference(sr,[status(thm)],[25729,398,theory(equality)])).
% cnf(25734,plain,(sz10=xr|sz00=xr|doDivides0(xr,xr)|esk4_1(xr)=sz10|~aNaturalNumber0(xr)),inference(spm,[status(thm)],[214,25730,theory(equality)])).
% cnf(25743,plain,(sz10=xr|sz00=xr|doDivides0(xr,xr)|esk4_1(xr)=sz10|$false),inference(rw,[status(thm)],[25734,402,theory(equality)])).
% cnf(25744,plain,(sz10=xr|sz00=xr|doDivides0(xr,xr)|esk4_1(xr)=sz10),inference(cn,[status(thm)],[25743,theory(equality)])).
% cnf(25745,plain,(xr=sz00|doDivides0(xr,xr)|esk4_1(xr)=sz10),inference(sr,[status(thm)],[25744,397,theory(equality)])).
% cnf(25746,plain,(doDivides0(xr,xr)|esk4_1(xr)=sz10),inference(sr,[status(thm)],[25745,398,theory(equality)])).
% cnf(25750,plain,(sz10=xr|sz00=xr|isPrime0(sz10)|doDivides0(xr,xr)|~aNaturalNumber0(xr)),inference(spm,[status(thm)],[213,25746,theory(equality)])).
% cnf(25757,plain,(sz10=xr|sz00=xr|isPrime0(sz10)|doDivides0(xr,xr)|$false),inference(rw,[status(thm)],[25750,402,theory(equality)])).
% cnf(25758,plain,(sz10=xr|sz00=xr|isPrime0(sz10)|doDivides0(xr,xr)),inference(cn,[status(thm)],[25757,theory(equality)])).
% cnf(25759,plain,(xr=sz00|isPrime0(sz10)|doDivides0(xr,xr)),inference(sr,[status(thm)],[25758,397,theory(equality)])).
% cnf(25760,plain,(isPrime0(sz10)|doDivides0(xr,xr)),inference(sr,[status(thm)],[25759,398,theory(equality)])).
% cnf(25761,plain,(doDivides0(xr,xr)),inference(sr,[status(thm)],[25760,516,theory(equality)])).
% cnf(25769,plain,(aNaturalNumber0(esk2_2(xr,xr))|~aNaturalNumber0(xr)),inference(spm,[status(thm)],[172,25761,theory(equality)])).
% cnf(25770,plain,(sdtasdt0(xr,esk2_2(xr,xr))=xr|~aNaturalNumber0(xr)),inference(spm,[status(thm)],[171,25761,theory(equality)])).
% cnf(25782,plain,(aNaturalNumber0(esk2_2(xr,xr))|$false),inference(rw,[status(thm)],[25769,402,theory(equality)])).
% cnf(25783,plain,(aNaturalNumber0(esk2_2(xr,xr))),inference(cn,[status(thm)],[25782,theory(equality)])).
% cnf(25784,plain,(sdtasdt0(xr,esk2_2(xr,xr))=xr|$false),inference(rw,[status(thm)],[25770,402,theory(equality)])).
% cnf(25785,plain,(sdtasdt0(xr,esk2_2(xr,xr))=xr),inference(cn,[status(thm)],[25784,theory(equality)])).
% cnf(25822,plain,(sz10=esk2_2(xr,xr)|xr=esk2_2(xr,xr)|~aNaturalNumber0(xr)|~aNaturalNumber0(esk2_2(xr,xr))),inference(spm,[status(thm)],[803,25785,theory(equality)])).
% cnf(25924,plain,(doDivides0(esk2_2(xr,xr),X1)|xr!=X1|~aNaturalNumber0(xr)|~aNaturalNumber0(esk2_2(xr,xr))|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[709,25785,theory(equality)])).
% cnf(26023,plain,(sz10=esk2_2(xr,xr)|xr=esk2_2(xr,xr)|$false|~aNaturalNumber0(esk2_2(xr,xr))),inference(rw,[status(thm)],[25822,402,theory(equality)])).
% cnf(26024,plain,(sz10=esk2_2(xr,xr)|xr=esk2_2(xr,xr)|$false|$false),inference(rw,[status(thm)],[26023,25783,theory(equality)])).
% cnf(26025,plain,(sz10=esk2_2(xr,xr)|xr=esk2_2(xr,xr)),inference(cn,[status(thm)],[26024,theory(equality)])).
% cnf(26333,plain,(doDivides0(esk2_2(xr,xr),X1)|xr!=X1|$false|~aNaturalNumber0(esk2_2(xr,xr))|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[25924,402,theory(equality)])).
% cnf(26334,plain,(doDivides0(esk2_2(xr,xr),X1)|xr!=X1|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[26333,25783,theory(equality)])).
% cnf(26335,plain,(doDivides0(esk2_2(xr,xr),X1)|xr!=X1|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[26334,theory(equality)])).
% cnf(28703,plain,(sdtasdt0(xr,xr)=xr|esk2_2(xr,xr)=sz10),inference(spm,[status(thm)],[25785,26025,theory(equality)])).
% cnf(29251,plain,(sdtasdt0(xr,sz10)=xr|sdtasdt0(xr,xr)=xr),inference(spm,[status(thm)],[25785,28703,theory(equality)])).
% cnf(30015,plain,(doDivides0(esk2_2(xr,xr),xr)|~aNaturalNumber0(xr)),inference(er,[status(thm)],[26335,theory(equality)])).
% cnf(30016,plain,(doDivides0(esk2_2(xr,xr),xr)|$false),inference(rw,[status(thm)],[30015,402,theory(equality)])).
% cnf(30017,plain,(doDivides0(esk2_2(xr,xr),xr)),inference(cn,[status(thm)],[30016,theory(equality)])).
% cnf(30022,plain,(doDivides0(X1,xr)|~doDivides0(X1,esk2_2(xr,xr))|~aNaturalNumber0(esk2_2(xr,xr))|~aNaturalNumber0(xr)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[183,30017,theory(equality)])).
% cnf(30048,plain,(doDivides0(X1,xr)|~doDivides0(X1,esk2_2(xr,xr))|$false|~aNaturalNumber0(xr)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[30022,25783,theory(equality)])).
% cnf(30049,plain,(doDivides0(X1,xr)|~doDivides0(X1,esk2_2(xr,xr))|$false|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[30048,402,theory(equality)])).
% cnf(30050,plain,(doDivides0(X1,xr)|~doDivides0(X1,esk2_2(xr,xr))|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[30049,theory(equality)])).
% cnf(36423,plain,(sdtasdt0(xn,xm)=sz00|sdtlseqdt0(xr,sdtasdt0(xn,xm))|$false),inference(rw,[status(thm)],[1050,488,theory(equality)])).
% cnf(36424,plain,(sdtasdt0(xn,xm)=sz00|sdtlseqdt0(xr,sdtasdt0(xn,xm))),inference(cn,[status(thm)],[36423,theory(equality)])).
% cnf(36425,plain,(sdtlseqdt0(xr,sdtasdt0(xn,xm))),inference(sr,[status(thm)],[36424,1024,theory(equality)])).
% cnf(36430,plain,(aNaturalNumber0(esk1_2(xr,sdtasdt0(xn,xm)))|~aNaturalNumber0(xr)|~aNaturalNumber0(sdtasdt0(xn,xm))),inference(spm,[status(thm)],[124,36425,theory(equality)])).
% cnf(36431,plain,(sdtpldt0(xr,esk1_2(xr,sdtasdt0(xn,xm)))=sdtasdt0(xn,xm)|~aNaturalNumber0(xr)|~aNaturalNumber0(sdtasdt0(xn,xm))),inference(spm,[status(thm)],[123,36425,theory(equality)])).
% cnf(36447,plain,(aNaturalNumber0(esk1_2(xr,sdtasdt0(xn,xm)))|$false|~aNaturalNumber0(sdtasdt0(xn,xm))),inference(rw,[status(thm)],[36430,402,theory(equality)])).
% cnf(36448,plain,(aNaturalNumber0(esk1_2(xr,sdtasdt0(xn,xm)))|$false|$false),inference(rw,[status(thm)],[36447,488,theory(equality)])).
% cnf(36449,plain,(aNaturalNumber0(esk1_2(xr,sdtasdt0(xn,xm)))),inference(cn,[status(thm)],[36448,theory(equality)])).
% cnf(36450,plain,(sdtpldt0(xr,esk1_2(xr,sdtasdt0(xn,xm)))=sdtasdt0(xn,xm)|$false|~aNaturalNumber0(sdtasdt0(xn,xm))),inference(rw,[status(thm)],[36431,402,theory(equality)])).
% cnf(36451,plain,(sdtpldt0(xr,esk1_2(xr,sdtasdt0(xn,xm)))=sdtasdt0(xn,xm)|$false|$false),inference(rw,[status(thm)],[36450,488,theory(equality)])).
% cnf(36452,plain,(sdtpldt0(xr,esk1_2(xr,sdtasdt0(xn,xm)))=sdtasdt0(xn,xm)),inference(cn,[status(thm)],[36451,theory(equality)])).
% cnf(38345,plain,(sz00=xr|aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xr))|~aNaturalNumber0(xr)|~aNaturalNumber0(sdtasdt0(xn,xm))),inference(spm,[status(thm)],[1053,407,theory(equality)])).
% cnf(38469,plain,(sz00=xr|aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xr))|$false|~aNaturalNumber0(sdtasdt0(xn,xm))),inference(rw,[status(thm)],[38345,402,theory(equality)])).
% cnf(38470,plain,(sz00=xr|aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xr))|$false|$false),inference(rw,[status(thm)],[38469,488,theory(equality)])).
% cnf(38471,plain,(sz00=xr|aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xr))),inference(cn,[status(thm)],[38470,theory(equality)])).
% cnf(38472,plain,(aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xr))),inference(sr,[status(thm)],[38471,398,theory(equality)])).
% cnf(45791,plain,(doDivides0(sz10,xr)|~aNaturalNumber0(sz10)|~aNaturalNumber0(esk2_2(xr,xr))),inference(spm,[status(thm)],[30050,737,theory(equality)])).
% cnf(45797,plain,(doDivides0(sz10,xr)|$false|~aNaturalNumber0(esk2_2(xr,xr))),inference(rw,[status(thm)],[45791,60,theory(equality)])).
% cnf(45798,plain,(doDivides0(sz10,xr)|$false|$false),inference(rw,[status(thm)],[45797,25783,theory(equality)])).
% cnf(45799,plain,(doDivides0(sz10,xr)),inference(cn,[status(thm)],[45798,theory(equality)])).
% cnf(45804,plain,(aNaturalNumber0(esk2_2(sz10,xr))|~aNaturalNumber0(sz10)|~aNaturalNumber0(xr)),inference(spm,[status(thm)],[172,45799,theory(equality)])).
% cnf(45805,plain,(sdtasdt0(sz10,esk2_2(sz10,xr))=xr|~aNaturalNumber0(sz10)|~aNaturalNumber0(xr)),inference(spm,[status(thm)],[171,45799,theory(equality)])).
% cnf(45821,plain,(aNaturalNumber0(esk2_2(sz10,xr))|$false|~aNaturalNumber0(xr)),inference(rw,[status(thm)],[45804,60,theory(equality)])).
% cnf(45822,plain,(aNaturalNumber0(esk2_2(sz10,xr))|$false|$false),inference(rw,[status(thm)],[45821,402,theory(equality)])).
% cnf(45823,plain,(aNaturalNumber0(esk2_2(sz10,xr))),inference(cn,[status(thm)],[45822,theory(equality)])).
% cnf(45824,plain,(sdtasdt0(sz10,esk2_2(sz10,xr))=xr|$false|~aNaturalNumber0(xr)),inference(rw,[status(thm)],[45805,60,theory(equality)])).
% cnf(45825,plain,(sdtasdt0(sz10,esk2_2(sz10,xr))=xr|$false|$false),inference(rw,[status(thm)],[45824,402,theory(equality)])).
% cnf(45826,plain,(sdtasdt0(sz10,esk2_2(sz10,xr))=xr),inference(cn,[status(thm)],[45825,theory(equality)])).
% cnf(53494,plain,(xr=esk2_2(sz10,xr)|~aNaturalNumber0(esk2_2(sz10,xr))),inference(spm,[status(thm)],[87,45826,theory(equality)])).
% cnf(53954,plain,(xr=esk2_2(sz10,xr)|$false),inference(rw,[status(thm)],[53494,45823,theory(equality)])).
% cnf(53955,plain,(xr=esk2_2(sz10,xr)),inference(cn,[status(thm)],[53954,theory(equality)])).
% cnf(54893,plain,(sdtasdt0(sz10,xr)=xr),inference(rw,[status(thm)],[45826,53955,theory(equality)])).
% cnf(54900,plain,(sz00=xr|sz10=X1|xr!=sdtasdt0(X1,xr)|~aNaturalNumber0(X1)|~aNaturalNumber0(sz10)|~aNaturalNumber0(xr)),inference(spm,[status(thm)],[108,54893,theory(equality)])).
% cnf(55057,plain,(sz00=xr|sz10=X1|xr!=sdtasdt0(X1,xr)|~aNaturalNumber0(X1)|$false|~aNaturalNumber0(xr)),inference(rw,[status(thm)],[54900,60,theory(equality)])).
% cnf(55058,plain,(sz00=xr|sz10=X1|xr!=sdtasdt0(X1,xr)|~aNaturalNumber0(X1)|$false|$false),inference(rw,[status(thm)],[55057,402,theory(equality)])).
% cnf(55059,plain,(sz00=xr|sz10=X1|xr!=sdtasdt0(X1,xr)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[55058,theory(equality)])).
% cnf(55060,plain,(sz10=X1|sdtasdt0(X1,xr)!=xr|~aNaturalNumber0(X1)),inference(sr,[status(thm)],[55059,398,theory(equality)])).
% cnf(67192,plain,(sz10=xr|sdtasdt0(xr,sz10)=xr|~aNaturalNumber0(xr)),inference(spm,[status(thm)],[55060,29251,theory(equality)])).
% cnf(67203,plain,(sz10=xr|sdtasdt0(xr,sz10)=xr|$false),inference(rw,[status(thm)],[67192,402,theory(equality)])).
% cnf(67204,plain,(sz10=xr|sdtasdt0(xr,sz10)=xr),inference(cn,[status(thm)],[67203,theory(equality)])).
% cnf(67205,plain,(sdtasdt0(xr,sz10)=xr),inference(sr,[status(thm)],[67204,397,theory(equality)])).
% cnf(104702,plain,(sdtasdt0(xr,sdtsldt0(sdtasdt0(xn,xm),xr))=sdtasdt0(xn,xm)|sz00=xr|~aNaturalNumber0(xr)|~aNaturalNumber0(sdtasdt0(xn,xm))),inference(spm,[status(thm)],[1644,407,theory(equality)])).
% cnf(104838,plain,(sdtasdt0(xr,sdtsldt0(sdtasdt0(xn,xm),xr))=sdtasdt0(xn,xm)|sz00=xr|$false|~aNaturalNumber0(sdtasdt0(xn,xm))),inference(rw,[status(thm)],[104702,402,theory(equality)])).
% cnf(104839,plain,(sdtasdt0(xr,sdtsldt0(sdtasdt0(xn,xm),xr))=sdtasdt0(xn,xm)|sz00=xr|$false|$false),inference(rw,[status(thm)],[104838,488,theory(equality)])).
% cnf(104840,plain,(sdtasdt0(xr,sdtsldt0(sdtasdt0(xn,xm),xr))=sdtasdt0(xn,xm)|sz00=xr),inference(cn,[status(thm)],[104839,theory(equality)])).
% cnf(104841,plain,(sdtasdt0(xr,sdtsldt0(sdtasdt0(xn,xm),xr))=sdtasdt0(xn,xm)),inference(sr,[status(thm)],[104840,398,theory(equality)])).
% cnf(107782,plain,(sdtsldt0(sdtasdt0(xn,xm),xr)=esk14_0|~aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xr))),inference(spm,[status(thm)],[1580,104841,theory(equality)])).
% cnf(108571,plain,(sdtsldt0(sdtasdt0(xn,xm),xr)=esk14_0|$false),inference(rw,[status(thm)],[107782,38472,theory(equality)])).
% cnf(108572,plain,(sdtsldt0(sdtasdt0(xn,xm),xr)=esk14_0),inference(cn,[status(thm)],[108571,theory(equality)])).
% cnf(188704,plain,(sdtasdt0(sdtasdt0(xn,xm),sz10)=sdtpldt0(sdtasdt0(xr,sz10),esk1_2(xr,sdtasdt0(xn,xm)))|~aNaturalNumber0(xr)|~aNaturalNumber0(esk1_2(xr,sdtasdt0(xn,xm)))),inference(spm,[status(thm)],[1958,36452,theory(equality)])).
% cnf(189361,plain,(sdtasdt0(sdtasdt0(xn,xm),sz10)=sdtasdt0(xn,xm)|~aNaturalNumber0(xr)|~aNaturalNumber0(esk1_2(xr,sdtasdt0(xn,xm)))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[188704,67205,theory(equality)]),36452,theory(equality)])).
% cnf(189362,plain,(sdtasdt0(sdtasdt0(xn,xm),sz10)=sdtasdt0(xn,xm)|$false|~aNaturalNumber0(esk1_2(xr,sdtasdt0(xn,xm)))),inference(rw,[status(thm)],[189361,402,theory(equality)])).
% cnf(189363,plain,(sdtasdt0(sdtasdt0(xn,xm),sz10)=sdtasdt0(xn,xm)|$false|$false),inference(rw,[status(thm)],[189362,36449,theory(equality)])).
% cnf(189364,plain,(sdtasdt0(sdtasdt0(xn,xm),sz10)=sdtasdt0(xn,xm)),inference(cn,[status(thm)],[189363,theory(equality)])).
% cnf(209485,plain,(sdtasdt0(xn,xm)=sdtasdt0(xm,sdtasdt0(xn,sz10))|~aNaturalNumber0(sz10)|~aNaturalNumber0(xn)|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[1195,189364,theory(equality)])).
% cnf(210320,plain,(sdtasdt0(xn,xm)=sdtasdt0(xm,xn)|~aNaturalNumber0(sz10)|~aNaturalNumber0(xn)|~aNaturalNumber0(xm)),inference(rw,[status(thm)],[209485,15712,theory(equality)])).
% cnf(210321,plain,(sdtasdt0(xn,xm)=sdtasdt0(xm,xn)|$false|~aNaturalNumber0(xn)|~aNaturalNumber0(xm)),inference(rw,[status(thm)],[210320,60,theory(equality)])).
% cnf(210322,plain,(sdtasdt0(xn,xm)=sdtasdt0(xm,xn)|$false|$false|~aNaturalNumber0(xm)),inference(rw,[status(thm)],[210321,218,theory(equality)])).
% cnf(210323,plain,(sdtasdt0(xn,xm)=sdtasdt0(xm,xn)|$false|$false|$false),inference(rw,[status(thm)],[210322,217,theory(equality)])).
% cnf(210324,plain,(sdtasdt0(xn,xm)=sdtasdt0(xm,xn)),inference(cn,[status(thm)],[210323,theory(equality)])).
% cnf(223619,plain,(sdtsldt0(sdtasdt0(X1,xk),xr)=sdtasdt0(X1,esk12_0)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[2039,17954,theory(equality)])).
% cnf(223623,plain,(sdtsldt0(sdtasdt0(xn,xm),xr)=sdtasdt0(xp,esk12_0)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[223619,384,theory(equality)])).
% cnf(223650,plain,(esk14_0=sdtasdt0(xp,esk12_0)|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[223623,108572,theory(equality)])).
% cnf(223651,plain,(esk14_0=sdtasdt0(xp,esk12_0)|$false),inference(rw,[status(thm)],[223650,216,theory(equality)])).
% cnf(223652,plain,(esk14_0=sdtasdt0(xp,esk12_0)),inference(cn,[status(thm)],[223651,theory(equality)])).
% cnf(223748,plain,(doDivides0(xp,esk14_0)|~aNaturalNumber0(esk12_0)|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[17969,223652,theory(equality)])).
% cnf(224074,plain,(doDivides0(xp,esk14_0)|$false|~aNaturalNumber0(xp)),inference(rw,[status(thm)],[223748,401,theory(equality)])).
% cnf(224075,plain,(doDivides0(xp,esk14_0)|$false|$false),inference(rw,[status(thm)],[224074,216,theory(equality)])).
% cnf(224076,plain,(doDivides0(xp,esk14_0)),inference(cn,[status(thm)],[224075,theory(equality)])).
% cnf(226390,plain,(sdtsldt0(sdtasdt0(X1,xn),xr)=sdtasdt0(X1,esk18_0)|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[2051,13123,theory(equality)])).
% cnf(226394,plain,(sdtsldt0(sdtasdt0(xn,xm),xr)=sdtasdt0(xm,esk18_0)|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[226390,210324,theory(equality)])).
% cnf(226421,plain,(esk14_0=sdtasdt0(xm,esk18_0)|~aNaturalNumber0(xm)),inference(rw,[status(thm)],[226394,108572,theory(equality)])).
% cnf(226422,plain,(esk14_0=sdtasdt0(xm,esk18_0)|$false),inference(rw,[status(thm)],[226421,217,theory(equality)])).
% cnf(226423,plain,(esk14_0=sdtasdt0(xm,esk18_0)),inference(cn,[status(thm)],[226422,theory(equality)])).
% cnf(226779,negated_conjecture,($false),inference(rw,[status(thm)],[inference(rw,[status(thm)],[13135,226423,theory(equality)]),224076,theory(equality)])).
% cnf(226780,negated_conjecture,($false),inference(cn,[status(thm)],[226779,theory(equality)])).
% cnf(226781,negated_conjecture,($false),226780,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 3614
% # ...of these trivial : 154
% # ...subsumed : 1511
% # ...remaining for further processing: 1949
% # Other redundant clauses eliminated : 43
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 50
% # Backward-rewritten : 338
% # Generated clauses : 67139
% # ...of the previous two non-trivial : 62125
% # Contextual simplify-reflections : 465
% # Paramodulations : 66839
% # Factorizations : 8
% # Equation resolutions : 290
% # Current number of processed clauses: 1558
% # Positive orientable unit clauses: 543
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 67
% # Non-unit-clauses : 948
% # Current number of unprocessed clauses: 48750
% # ...number of literals in the above : 355319
% # Clause-clause subsumption calls (NU) : 45342
% # Rec. Clause-clause subsumption calls : 19246
% # Unit Clause-clause subsumption calls : 6997
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 1023
% # Indexed BW rewrite successes : 134
% # Backwards rewriting index: 1360 leaves, 1.17+/-1.266 terms/leaf
% # Paramod-from index: 812 leaves, 1.12+/-1.363 terms/leaf
% # Paramod-into index: 1231 leaves, 1.15+/-1.259 terms/leaf
% # -------------------------------------------------
% # User time : 4.164 s
% # System time : 0.158 s
% # Total time : 4.322 s
% # Maximum resident set size: 0 pages
% PrfWatch: 8.45 CPU 8.64 WC
% FINAL PrfWatch: 8.45 CPU 8.64 WC
% SZS output end Solution for /tmp/SystemOnTPTP11034/NUM511+3.tptp
%
%------------------------------------------------------------------------------