%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NUM523+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 : 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:58:02 EST 2010
% Result : Theorem 1.28s
% Output : Solution 1.28s
% 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/SystemOnTPTP5064/NUM523+3.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP5064/NUM523+3.tptp
% SZS output start Solution for /tmp/SystemOnTPTP5064/NUM523+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 5196
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Preprocessing time : 0.020 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(3, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>aNaturalNumber0(sdtasdt0(X1,X2))),file('/tmp/SRASS.s.p', mSortsB_02)).
% fof(10, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>(doDivides0(X1,X2)<=>?[X3]:(aNaturalNumber0(X3)&X2=sdtasdt0(X1,X3)))),file('/tmp/SRASS.s.p', mDefDiv)).
% fof(14, axiom,![X1]:![X2]:![X3]:(((aNaturalNumber0(X1)&aNaturalNumber0(X2))&aNaturalNumber0(X3))=>((isPrime0(X3)&doDivides0(X3,sdtasdt0(X1,X2)))=>(doDivides0(X3,X1)|doDivides0(X3,X2)))),file('/tmp/SRASS.s.p', mPDP)).
% fof(15, axiom,(((((aNaturalNumber0(xn)&aNaturalNumber0(xm))&aNaturalNumber0(xp))&~(xn=sz00))&~(xm=sz00))&~(xp=sz00)),file('/tmp/SRASS.s.p', m__2987)).
% fof(17, axiom,sdtasdt0(xp,sdtasdt0(xm,xm))=sdtasdt0(xn,xn),file('/tmp/SRASS.s.p', m__3014)).
% fof(18, axiom,((~(xp=sz10)&![X1]:((aNaturalNumber0(X1)&(?[X2]:(aNaturalNumber0(X2)&xp=sdtasdt0(X1,X2))|doDivides0(X1,xp)))=>(X1=sz10|X1=xp)))&isPrime0(xp)),file('/tmp/SRASS.s.p', m__3025)).
% fof(44, conjecture,((?[X1]:(aNaturalNumber0(X1)&sdtasdt0(xn,xn)=sdtasdt0(xp,X1))|doDivides0(xp,sdtasdt0(xn,xn)))&(?[X1]:(aNaturalNumber0(X1)&xn=sdtasdt0(xp,X1))|doDivides0(xp,xn))),file('/tmp/SRASS.s.p', m__)).
% fof(45, negated_conjecture,~(((?[X1]:(aNaturalNumber0(X1)&sdtasdt0(xn,xn)=sdtasdt0(xp,X1))|doDivides0(xp,sdtasdt0(xn,xn)))&(?[X1]:(aNaturalNumber0(X1)&xn=sdtasdt0(xp,X1))|doDivides0(xp,xn)))),inference(assume_negation,[status(cth)],[44])).
% fof(51, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|aNaturalNumber0(sdtasdt0(X1,X2))),inference(fof_nnf,[status(thm)],[3])).
% fof(52, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|aNaturalNumber0(sdtasdt0(X3,X4))),inference(variable_rename,[status(thm)],[51])).
% cnf(53,plain,(aNaturalNumber0(sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[52])).
% fof(79, 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)],[10])).
% fof(80, 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)],[79])).
% fof(81, plain,![X4]:![X5]:((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|((~(doDivides0(X4,X5))|(aNaturalNumber0(esk1_2(X4,X5))&X5=sdtasdt0(X4,esk1_2(X4,X5))))&(![X7]:(~(aNaturalNumber0(X7))|~(X5=sdtasdt0(X4,X7)))|doDivides0(X4,X5)))),inference(skolemize,[status(esa)],[80])).
% fof(82, plain,![X4]:![X5]:![X7]:((((~(aNaturalNumber0(X7))|~(X5=sdtasdt0(X4,X7)))|doDivides0(X4,X5))&(~(doDivides0(X4,X5))|(aNaturalNumber0(esk1_2(X4,X5))&X5=sdtasdt0(X4,esk1_2(X4,X5)))))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))),inference(shift_quantors,[status(thm)],[81])).
% fof(83, plain,![X4]:![X5]:![X7]:((((~(aNaturalNumber0(X7))|~(X5=sdtasdt0(X4,X7)))|doDivides0(X4,X5))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5))))&(((aNaturalNumber0(esk1_2(X4,X5))|~(doDivides0(X4,X5)))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5))))&((X5=sdtasdt0(X4,esk1_2(X4,X5))|~(doDivides0(X4,X5)))|(~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))))),inference(distribute,[status(thm)],[82])).
% cnf(86,plain,(doDivides0(X2,X1)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|X1!=sdtasdt0(X2,X3)|~aNaturalNumber0(X3)),inference(split_conjunct,[status(thm)],[83])).
% fof(109, plain,![X1]:![X2]:![X3]:(((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|~(aNaturalNumber0(X3)))|((~(isPrime0(X3))|~(doDivides0(X3,sdtasdt0(X1,X2))))|(doDivides0(X3,X1)|doDivides0(X3,X2)))),inference(fof_nnf,[status(thm)],[14])).
% fof(110, plain,![X4]:![X5]:![X6]:(((~(aNaturalNumber0(X4))|~(aNaturalNumber0(X5)))|~(aNaturalNumber0(X6)))|((~(isPrime0(X6))|~(doDivides0(X6,sdtasdt0(X4,X5))))|(doDivides0(X6,X4)|doDivides0(X6,X5)))),inference(variable_rename,[status(thm)],[109])).
% cnf(111,plain,(doDivides0(X1,X2)|doDivides0(X1,X3)|~doDivides0(X1,sdtasdt0(X3,X2))|~isPrime0(X1)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|~aNaturalNumber0(X3)),inference(split_conjunct,[status(thm)],[110])).
% cnf(115,plain,(aNaturalNumber0(xp)),inference(split_conjunct,[status(thm)],[15])).
% cnf(116,plain,(aNaturalNumber0(xm)),inference(split_conjunct,[status(thm)],[15])).
% cnf(117,plain,(aNaturalNumber0(xn)),inference(split_conjunct,[status(thm)],[15])).
% cnf(129,plain,(sdtasdt0(xp,sdtasdt0(xm,xm))=sdtasdt0(xn,xn)),inference(split_conjunct,[status(thm)],[17])).
% fof(130, plain,((~(xp=sz10)&![X1]:((~(aNaturalNumber0(X1))|(![X2]:(~(aNaturalNumber0(X2))|~(xp=sdtasdt0(X1,X2)))&~(doDivides0(X1,xp))))|(X1=sz10|X1=xp)))&isPrime0(xp)),inference(fof_nnf,[status(thm)],[18])).
% fof(131, plain,((~(xp=sz10)&![X3]:((~(aNaturalNumber0(X3))|(![X4]:(~(aNaturalNumber0(X4))|~(xp=sdtasdt0(X3,X4)))&~(doDivides0(X3,xp))))|(X3=sz10|X3=xp)))&isPrime0(xp)),inference(variable_rename,[status(thm)],[130])).
% fof(132, plain,![X3]:![X4]:((((((~(aNaturalNumber0(X4))|~(xp=sdtasdt0(X3,X4)))&~(doDivides0(X3,xp)))|~(aNaturalNumber0(X3)))|(X3=sz10|X3=xp))&~(xp=sz10))&isPrime0(xp)),inference(shift_quantors,[status(thm)],[131])).
% fof(133, 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=sz10))&isPrime0(xp)),inference(distribute,[status(thm)],[132])).
% cnf(134,plain,(isPrime0(xp)),inference(split_conjunct,[status(thm)],[133])).
% fof(246, negated_conjecture,((![X1]:(~(aNaturalNumber0(X1))|~(sdtasdt0(xn,xn)=sdtasdt0(xp,X1)))&~(doDivides0(xp,sdtasdt0(xn,xn))))|(![X1]:(~(aNaturalNumber0(X1))|~(xn=sdtasdt0(xp,X1)))&~(doDivides0(xp,xn)))),inference(fof_nnf,[status(thm)],[45])).
% fof(247, negated_conjecture,((![X2]:(~(aNaturalNumber0(X2))|~(sdtasdt0(xn,xn)=sdtasdt0(xp,X2)))&~(doDivides0(xp,sdtasdt0(xn,xn))))|(![X3]:(~(aNaturalNumber0(X3))|~(xn=sdtasdt0(xp,X3)))&~(doDivides0(xp,xn)))),inference(variable_rename,[status(thm)],[246])).
% fof(248, negated_conjecture,![X2]:![X3]:(((~(aNaturalNumber0(X3))|~(xn=sdtasdt0(xp,X3)))&~(doDivides0(xp,xn)))|((~(aNaturalNumber0(X2))|~(sdtasdt0(xn,xn)=sdtasdt0(xp,X2)))&~(doDivides0(xp,sdtasdt0(xn,xn))))),inference(shift_quantors,[status(thm)],[247])).
% fof(249, negated_conjecture,![X2]:![X3]:((((~(aNaturalNumber0(X2))|~(sdtasdt0(xn,xn)=sdtasdt0(xp,X2)))|(~(aNaturalNumber0(X3))|~(xn=sdtasdt0(xp,X3))))&(~(doDivides0(xp,sdtasdt0(xn,xn)))|(~(aNaturalNumber0(X3))|~(xn=sdtasdt0(xp,X3)))))&(((~(aNaturalNumber0(X2))|~(sdtasdt0(xn,xn)=sdtasdt0(xp,X2)))|~(doDivides0(xp,xn)))&(~(doDivides0(xp,sdtasdt0(xn,xn)))|~(doDivides0(xp,xn))))),inference(distribute,[status(thm)],[248])).
% cnf(250,negated_conjecture,(~doDivides0(xp,xn)|~doDivides0(xp,sdtasdt0(xn,xn))),inference(split_conjunct,[status(thm)],[249])).
% cnf(288,plain,(aNaturalNumber0(sdtasdt0(xn,xn))|~aNaturalNumber0(sdtasdt0(xm,xm))|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[53,129,theory(equality)])).
% cnf(293,plain,(aNaturalNumber0(sdtasdt0(xn,xn))|~aNaturalNumber0(sdtasdt0(xm,xm))|$false),inference(rw,[status(thm)],[288,115,theory(equality)])).
% cnf(294,plain,(aNaturalNumber0(sdtasdt0(xn,xn))|~aNaturalNumber0(sdtasdt0(xm,xm))),inference(cn,[status(thm)],[293,theory(equality)])).
% cnf(468,plain,(doDivides0(X1,sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)|~aNaturalNumber0(sdtasdt0(X1,X2))),inference(er,[status(thm)],[86,theory(equality)])).
% cnf(469,plain,(doDivides0(xp,X1)|sdtasdt0(xn,xn)!=X1|~aNaturalNumber0(sdtasdt0(xm,xm))|~aNaturalNumber0(xp)|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[86,129,theory(equality)])).
% cnf(477,plain,(doDivides0(xp,X1)|sdtasdt0(xn,xn)!=X1|~aNaturalNumber0(sdtasdt0(xm,xm))|$false|~aNaturalNumber0(X1)),inference(rw,[status(thm)],[469,115,theory(equality)])).
% cnf(478,plain,(doDivides0(xp,X1)|sdtasdt0(xn,xn)!=X1|~aNaturalNumber0(sdtasdt0(xm,xm))|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[477,theory(equality)])).
% cnf(1284,plain,(aNaturalNumber0(sdtasdt0(xn,xn))|~aNaturalNumber0(xm)),inference(spm,[status(thm)],[294,53,theory(equality)])).
% cnf(1289,plain,(aNaturalNumber0(sdtasdt0(xn,xn))|$false),inference(rw,[status(thm)],[1284,116,theory(equality)])).
% cnf(1290,plain,(aNaturalNumber0(sdtasdt0(xn,xn))),inference(cn,[status(thm)],[1289,theory(equality)])).
% cnf(2352,negated_conjecture,(~doDivides0(xp,xn)|~aNaturalNumber0(sdtasdt0(xm,xm))|~aNaturalNumber0(sdtasdt0(xn,xn))),inference(spm,[status(thm)],[250,478,theory(equality)])).
% cnf(2375,negated_conjecture,(~doDivides0(xp,xn)|~aNaturalNumber0(sdtasdt0(xm,xm))|$false),inference(rw,[status(thm)],[2352,1290,theory(equality)])).
% cnf(2376,negated_conjecture,(~doDivides0(xp,xn)|~aNaturalNumber0(sdtasdt0(xm,xm))),inference(cn,[status(thm)],[2375,theory(equality)])).
% cnf(2591,plain,(doDivides0(X1,sdtasdt0(X1,X2))|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(csr,[status(thm)],[468,53])).
% cnf(2600,plain,(doDivides0(xp,sdtasdt0(xn,xn))|~aNaturalNumber0(sdtasdt0(xm,xm))|~aNaturalNumber0(xp)),inference(spm,[status(thm)],[2591,129,theory(equality)])).
% cnf(2614,plain,(doDivides0(xp,sdtasdt0(xn,xn))|~aNaturalNumber0(sdtasdt0(xm,xm))|$false),inference(rw,[status(thm)],[2600,115,theory(equality)])).
% cnf(2615,plain,(doDivides0(xp,sdtasdt0(xn,xn))|~aNaturalNumber0(sdtasdt0(xm,xm))),inference(cn,[status(thm)],[2614,theory(equality)])).
% cnf(2736,plain,(doDivides0(xp,xn)|~isPrime0(xp)|~aNaturalNumber0(xn)|~aNaturalNumber0(xp)|~aNaturalNumber0(sdtasdt0(xm,xm))),inference(spm,[status(thm)],[111,2615,theory(equality)])).
% cnf(2755,plain,(doDivides0(xp,xn)|$false|~aNaturalNumber0(xn)|~aNaturalNumber0(xp)|~aNaturalNumber0(sdtasdt0(xm,xm))),inference(rw,[status(thm)],[2736,134,theory(equality)])).
% cnf(2756,plain,(doDivides0(xp,xn)|$false|$false|~aNaturalNumber0(xp)|~aNaturalNumber0(sdtasdt0(xm,xm))),inference(rw,[status(thm)],[2755,117,theory(equality)])).
% cnf(2757,plain,(doDivides0(xp,xn)|$false|$false|$false|~aNaturalNumber0(sdtasdt0(xm,xm))),inference(rw,[status(thm)],[2756,115,theory(equality)])).
% cnf(2758,plain,(doDivides0(xp,xn)|~aNaturalNumber0(sdtasdt0(xm,xm))),inference(cn,[status(thm)],[2757,theory(equality)])).
% cnf(2765,plain,(~aNaturalNumber0(sdtasdt0(xm,xm))),inference(csr,[status(thm)],[2758,2376])).
% cnf(2769,plain,(~aNaturalNumber0(xm)),inference(spm,[status(thm)],[2765,53,theory(equality)])).
% cnf(2776,plain,($false),inference(rw,[status(thm)],[2769,116,theory(equality)])).
% cnf(2777,plain,($false),inference(cn,[status(thm)],[2776,theory(equality)])).
% cnf(2778,plain,($false),2777,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 537
% # ...of these trivial : 0
% # ...subsumed : 236
% # ...remaining for further processing: 301
% # Other redundant clauses eliminated : 20
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 12
% # Backward-rewritten : 15
% # Generated clauses : 1126
% # ...of the previous two non-trivial : 1022
% # Contextual simplify-reflections : 40
% # Paramodulations : 1083
% # Factorizations : 1
% # Equation resolutions : 39
% # Current number of processed clauses: 185
% # Positive orientable unit clauses: 21
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 20
% # Non-unit-clauses : 144
% # Current number of unprocessed clauses: 593
% # ...number of literals in the above : 3759
% # Clause-clause subsumption calls (NU) : 2621
% # Rec. Clause-clause subsumption calls : 987
% # Unit Clause-clause subsumption calls : 175
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 10
% # Indexed BW rewrite successes : 10
% # Backwards rewriting index: 157 leaves, 1.27+/-0.935 terms/leaf
% # Paramod-from index: 80 leaves, 1.07+/-0.263 terms/leaf
% # Paramod-into index: 128 leaves, 1.23+/-0.888 terms/leaf
% # -------------------------------------------------
% # User time : 0.084 s
% # System time : 0.004 s
% # Total time : 0.088 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.21 CPU 0.28 WC
% FINAL PrfWatch: 0.21 CPU 0.28 WC
% SZS output end Solution for /tmp/SystemOnTPTP5064/NUM523+3.tptp
%
%------------------------------------------------------------------------------