%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NUM500+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 : art03.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:37:47 EST 2010
% Result : Theorem 1.13s
% Output : Solution 1.13s
% 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/SystemOnTPTP4312/NUM500+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP4312/NUM500+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP4312/NUM500+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 4408
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.021 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,aNaturalNumber0(sz00),file('/tmp/SRASS.s.p', mSortsC)).
% fof(4, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>aNaturalNumber0(sdtasdt0(X1,X2))),file('/tmp/SRASS.s.p', mSortsB_02)).
% 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(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,(isPrime0(xp)&doDivides0(xp,sdtasdt0(xn,xm))),file('/tmp/SRASS.s.p', m__1860)).
% fof(42, axiom,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(48, conjecture,?[X1]:((aNaturalNumber0(X1)&doDivides0(X1,xk))&isPrime0(X1)),file('/tmp/SRASS.s.p', m__)).
% fof(49, negated_conjecture,~(?[X1]:((aNaturalNumber0(X1)&doDivides0(X1,xk))&isPrime0(X1))),inference(assume_negation,[status(cth)],[48])).
% cnf(54,plain,(aNaturalNumber0(sz00)),inference(split_conjunct,[status(thm)],[1])).
% fof(60, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|aNaturalNumber0(sdtasdt0(X1,X2))),inference(fof_nnf,[status(thm)],[4])).
% fof(61, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|aNaturalNumber0(sdtasdt0(X3,X4))),inference(variable_rename,[status(thm)],[60])).
% cnf(62,plain,(aNaturalNumber0(sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[61])).
% fof(170, 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(171, 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)],[170])).
% fof(172, 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)],[171])).
% fof(173, 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)],[172])).
% cnf(176,plain,(X2=sz00|aNaturalNumber0(X3)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~doDivides0(X2,X1)|X3!=sdtsldt0(X1,X2)),inference(split_conjunct,[status(thm)],[173])).
% fof(193, 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(194, 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)],[193])).
% fof(195, 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)],[194])).
% fof(196, 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)],[195])).
% fof(197, 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)],[196])).
% cnf(203,plain,(~aNaturalNumber0(X1)|~isPrime0(X1)|X1!=sz00),inference(split_conjunct,[status(thm)],[197])).
% fof(205, plain,![X1]:(((~(aNaturalNumber0(X1))|X1=sz00)|X1=sz10)|?[X2]:((aNaturalNumber0(X2)&doDivides0(X2,X1))&isPrime0(X2))),inference(fof_nnf,[status(thm)],[35])).
% fof(206, plain,![X3]:(((~(aNaturalNumber0(X3))|X3=sz00)|X3=sz10)|?[X4]:((aNaturalNumber0(X4)&doDivides0(X4,X3))&isPrime0(X4))),inference(variable_rename,[status(thm)],[205])).
% fof(207, 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)],[206])).
% fof(208, 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)],[207])).
% cnf(209,plain,(X1=sz10|X1=sz00|isPrime0(esk4_1(X1))|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[208])).
% cnf(210,plain,(X1=sz10|X1=sz00|doDivides0(esk4_1(X1),X1)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[208])).
% cnf(211,plain,(X1=sz10|X1=sz00|aNaturalNumber0(esk4_1(X1))|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[208])).
% cnf(212,plain,(aNaturalNumber0(xp)),inference(split_conjunct,[status(thm)],[36])).
% cnf(213,plain,(aNaturalNumber0(xm)),inference(split_conjunct,[status(thm)],[36])).
% cnf(214,plain,(aNaturalNumber0(xn)),inference(split_conjunct,[status(thm)],[36])).
% cnf(218,plain,(doDivides0(xp,sdtasdt0(xn,xm))),inference(split_conjunct,[status(thm)],[38])).
% cnf(219,plain,(isPrime0(xp)),inference(split_conjunct,[status(thm)],[38])).
% cnf(226,plain,(xk=sdtsldt0(sdtasdt0(xn,xm),xp)),inference(split_conjunct,[status(thm)],[42])).
% fof(227, plain,(~(xk=sz00)&~(xk=sz10)),inference(fof_nnf,[status(thm)],[43])).
% cnf(228,plain,(xk!=sz10),inference(split_conjunct,[status(thm)],[227])).
% cnf(229,plain,(xk!=sz00),inference(split_conjunct,[status(thm)],[227])).
% fof(243, negated_conjecture,![X1]:((~(aNaturalNumber0(X1))|~(doDivides0(X1,xk)))|~(isPrime0(X1))),inference(fof_nnf,[status(thm)],[49])).
% fof(244, negated_conjecture,![X2]:((~(aNaturalNumber0(X2))|~(doDivides0(X2,xk)))|~(isPrime0(X2))),inference(variable_rename,[status(thm)],[243])).
% cnf(245,negated_conjecture,(~isPrime0(X1)|~doDivides0(X1,xk)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[244])).
% cnf(253,plain,(~isPrime0(sz00)|~aNaturalNumber0(sz00)),inference(er,[status(thm)],[203,theory(equality)])).
% cnf(254,plain,(~isPrime0(sz00)|$false),inference(rw,[status(thm)],[253,54,theory(equality)])).
% cnf(255,plain,(~isPrime0(sz00)),inference(cn,[status(thm)],[254,theory(equality)])).
% cnf(311,negated_conjecture,(sz00=xk|sz10=xk|~isPrime0(esk4_1(xk))|~aNaturalNumber0(esk4_1(xk))|~aNaturalNumber0(xk)),inference(spm,[status(thm)],[245,210,theory(equality)])).
% cnf(314,negated_conjecture,(xk=sz10|~isPrime0(esk4_1(xk))|~aNaturalNumber0(esk4_1(xk))|~aNaturalNumber0(xk)),inference(sr,[status(thm)],[311,229,theory(equality)])).
% cnf(315,negated_conjecture,(~isPrime0(esk4_1(xk))|~aNaturalNumber0(esk4_1(xk))|~aNaturalNumber0(xk)),inference(sr,[status(thm)],[314,228,theory(equality)])).
% cnf(446,plain,(sz00=X1|aNaturalNumber0(sdtsldt0(X2,X1))|~doDivides0(X1,X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)),inference(er,[status(thm)],[176,theory(equality)])).
% cnf(4880,plain,(sz00=xp|aNaturalNumber0(sdtsldt0(sdtasdt0(xn,xm),xp))|~aNaturalNumber0(xp)|~aNaturalNumber0(sdtasdt0(xn,xm))),inference(spm,[status(thm)],[446,218,theory(equality)])).
% cnf(4891,plain,(sz00=xp|aNaturalNumber0(xk)|~aNaturalNumber0(xp)|~aNaturalNumber0(sdtasdt0(xn,xm))),inference(rw,[status(thm)],[4880,226,theory(equality)])).
% cnf(4892,plain,(sz00=xp|aNaturalNumber0(xk)|$false|~aNaturalNumber0(sdtasdt0(xn,xm))),inference(rw,[status(thm)],[4891,212,theory(equality)])).
% cnf(4893,plain,(sz00=xp|aNaturalNumber0(xk)|~aNaturalNumber0(sdtasdt0(xn,xm))),inference(cn,[status(thm)],[4892,theory(equality)])).
% cnf(4913,plain,(xp=sz00|aNaturalNumber0(xk)|~aNaturalNumber0(xm)|~aNaturalNumber0(xn)),inference(spm,[status(thm)],[4893,62,theory(equality)])).
% cnf(4914,plain,(xp=sz00|aNaturalNumber0(xk)|$false|~aNaturalNumber0(xn)),inference(rw,[status(thm)],[4913,213,theory(equality)])).
% cnf(4915,plain,(xp=sz00|aNaturalNumber0(xk)|$false|$false),inference(rw,[status(thm)],[4914,214,theory(equality)])).
% cnf(4916,plain,(xp=sz00|aNaturalNumber0(xk)),inference(cn,[status(thm)],[4915,theory(equality)])).
% cnf(4917,negated_conjecture,(xp=sz00|~isPrime0(esk4_1(xk))|~aNaturalNumber0(esk4_1(xk))),inference(spm,[status(thm)],[315,4916,theory(equality)])).
% cnf(4920,negated_conjecture,(xp=sz00|sz00=xk|sz10=xk|~aNaturalNumber0(esk4_1(xk))|~aNaturalNumber0(xk)),inference(spm,[status(thm)],[4917,209,theory(equality)])).
% cnf(4921,negated_conjecture,(xp=sz00|xk=sz10|~aNaturalNumber0(esk4_1(xk))|~aNaturalNumber0(xk)),inference(sr,[status(thm)],[4920,229,theory(equality)])).
% cnf(4922,negated_conjecture,(xp=sz00|~aNaturalNumber0(esk4_1(xk))|~aNaturalNumber0(xk)),inference(sr,[status(thm)],[4921,228,theory(equality)])).
% cnf(4928,negated_conjecture,(xp=sz00|~aNaturalNumber0(esk4_1(xk))),inference(csr,[status(thm)],[4922,4916])).
% cnf(4930,negated_conjecture,(xp=sz00|sz00=xk|sz10=xk|~aNaturalNumber0(xk)),inference(spm,[status(thm)],[4928,211,theory(equality)])).
% cnf(4931,negated_conjecture,(xp=sz00|xk=sz10|~aNaturalNumber0(xk)),inference(sr,[status(thm)],[4930,229,theory(equality)])).
% cnf(4932,negated_conjecture,(xp=sz00|~aNaturalNumber0(xk)),inference(sr,[status(thm)],[4931,228,theory(equality)])).
% cnf(4933,negated_conjecture,(xp=sz00),inference(csr,[status(thm)],[4932,4916])).
% cnf(5123,plain,(isPrime0(sz00)),inference(rw,[status(thm)],[219,4933,theory(equality)])).
% cnf(5124,plain,($false),inference(sr,[status(thm)],[5123,255,theory(equality)])).
% cnf(5125,plain,($false),5124,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 587
% # ...of these trivial : 0
% # ...subsumed : 197
% # ...remaining for further processing: 390
% # Other redundant clauses eliminated : 29
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 7
% # Backward-rewritten : 158
% # Generated clauses : 1941
% # ...of the previous two non-trivial : 1783
% # Contextual simplify-reflections : 98
% # Paramodulations : 1881
% # Factorizations : 4
% # Equation resolutions : 56
% # Current number of processed clauses: 146
% # Positive orientable unit clauses: 10
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 5
% # Non-unit-clauses : 131
% # Current number of unprocessed clauses: 632
% # ...number of literals in the above : 2947
% # Clause-clause subsumption calls (NU) : 2198
% # Rec. Clause-clause subsumption calls : 1260
% # Unit Clause-clause subsumption calls : 5
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 13
% # Indexed BW rewrite successes : 8
% # Backwards rewriting index: 127 leaves, 1.39+/-0.964 terms/leaf
% # Paramod-from index: 72 leaves, 1.11+/-0.356 terms/leaf
% # Paramod-into index: 106 leaves, 1.26+/-0.872 terms/leaf
% # -------------------------------------------------
% # User time : 0.120 s
% # System time : 0.008 s
% # Total time : 0.128 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.28 CPU 0.37 WC
% FINAL PrfWatch: 0.28 CPU 0.37 WC
% SZS output end Solution for /tmp/SystemOnTPTP4312/NUM500+1.tptp
%
%------------------------------------------------------------------------------