%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : RNG091+2 : 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 22:30:07 EST 2010
% Result : Theorem 0.95s
% Output : Solution 0.95s
% 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/SystemOnTPTP9144/RNG091+2.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP9144/RNG091+2.tptp
% SZS output start Solution for /tmp/SystemOnTPTP9144/RNG091+2.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 9240
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.017 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(16, axiom,(aElementOf0(sdtpldt0(xk,xm),xI)&aElementOf0(sdtpldt0(xl,xn),xJ)),file('/tmp/SRASS.s.p', m__994)).
% fof(17, axiom,(aElementOf0(sdtasdt0(xz,xk),xI)&aElementOf0(sdtasdt0(xz,xl),xJ)),file('/tmp/SRASS.s.p', m__1021)).
% fof(18, axiom,sdtpldt0(xx,xy)=sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn)),file('/tmp/SRASS.s.p', m__1061)).
% fof(19, axiom,sdtasdt0(xz,xx)=sdtpldt0(sdtasdt0(xz,xk),sdtasdt0(xz,xl)),file('/tmp/SRASS.s.p', m__1098)).
% fof(33, conjecture,((?[X1]:?[X2]:((aElementOf0(X1,xI)&aElementOf0(X2,xJ))&sdtpldt0(X1,X2)=sdtpldt0(xx,xy))|aElementOf0(sdtpldt0(xx,xy),sdtpldt1(xI,xJ)))&(?[X1]:?[X2]:((aElementOf0(X1,xI)&aElementOf0(X2,xJ))&sdtpldt0(X1,X2)=sdtasdt0(xz,xx))|aElementOf0(sdtasdt0(xz,xx),sdtpldt1(xI,xJ)))),file('/tmp/SRASS.s.p', m__)).
% fof(34, negated_conjecture,~(((?[X1]:?[X2]:((aElementOf0(X1,xI)&aElementOf0(X2,xJ))&sdtpldt0(X1,X2)=sdtpldt0(xx,xy))|aElementOf0(sdtpldt0(xx,xy),sdtpldt1(xI,xJ)))&(?[X1]:?[X2]:((aElementOf0(X1,xI)&aElementOf0(X2,xJ))&sdtpldt0(X1,X2)=sdtasdt0(xz,xx))|aElementOf0(sdtasdt0(xz,xx),sdtpldt1(xI,xJ))))),inference(assume_negation,[status(cth)],[33])).
% cnf(128,plain,(aElementOf0(sdtpldt0(xl,xn),xJ)),inference(split_conjunct,[status(thm)],[16])).
% cnf(129,plain,(aElementOf0(sdtpldt0(xk,xm),xI)),inference(split_conjunct,[status(thm)],[16])).
% cnf(130,plain,(aElementOf0(sdtasdt0(xz,xl),xJ)),inference(split_conjunct,[status(thm)],[17])).
% cnf(131,plain,(aElementOf0(sdtasdt0(xz,xk),xI)),inference(split_conjunct,[status(thm)],[17])).
% cnf(132,plain,(sdtpldt0(xx,xy)=sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn))),inference(split_conjunct,[status(thm)],[18])).
% cnf(133,plain,(sdtasdt0(xz,xx)=sdtpldt0(sdtasdt0(xz,xk),sdtasdt0(xz,xl))),inference(split_conjunct,[status(thm)],[19])).
% fof(184, negated_conjecture,((![X1]:![X2]:((~(aElementOf0(X1,xI))|~(aElementOf0(X2,xJ)))|~(sdtpldt0(X1,X2)=sdtpldt0(xx,xy)))&~(aElementOf0(sdtpldt0(xx,xy),sdtpldt1(xI,xJ))))|(![X1]:![X2]:((~(aElementOf0(X1,xI))|~(aElementOf0(X2,xJ)))|~(sdtpldt0(X1,X2)=sdtasdt0(xz,xx)))&~(aElementOf0(sdtasdt0(xz,xx),sdtpldt1(xI,xJ))))),inference(fof_nnf,[status(thm)],[34])).
% fof(185, negated_conjecture,((![X3]:![X4]:((~(aElementOf0(X3,xI))|~(aElementOf0(X4,xJ)))|~(sdtpldt0(X3,X4)=sdtpldt0(xx,xy)))&~(aElementOf0(sdtpldt0(xx,xy),sdtpldt1(xI,xJ))))|(![X5]:![X6]:((~(aElementOf0(X5,xI))|~(aElementOf0(X6,xJ)))|~(sdtpldt0(X5,X6)=sdtasdt0(xz,xx)))&~(aElementOf0(sdtasdt0(xz,xx),sdtpldt1(xI,xJ))))),inference(variable_rename,[status(thm)],[184])).
% fof(186, negated_conjecture,![X3]:![X4]:![X5]:![X6]:((((~(aElementOf0(X5,xI))|~(aElementOf0(X6,xJ)))|~(sdtpldt0(X5,X6)=sdtasdt0(xz,xx)))&~(aElementOf0(sdtasdt0(xz,xx),sdtpldt1(xI,xJ))))|(((~(aElementOf0(X3,xI))|~(aElementOf0(X4,xJ)))|~(sdtpldt0(X3,X4)=sdtpldt0(xx,xy)))&~(aElementOf0(sdtpldt0(xx,xy),sdtpldt1(xI,xJ))))),inference(shift_quantors,[status(thm)],[185])).
% fof(187, negated_conjecture,![X3]:![X4]:![X5]:![X6]:(((((~(aElementOf0(X3,xI))|~(aElementOf0(X4,xJ)))|~(sdtpldt0(X3,X4)=sdtpldt0(xx,xy)))|((~(aElementOf0(X5,xI))|~(aElementOf0(X6,xJ)))|~(sdtpldt0(X5,X6)=sdtasdt0(xz,xx))))&(~(aElementOf0(sdtpldt0(xx,xy),sdtpldt1(xI,xJ)))|((~(aElementOf0(X5,xI))|~(aElementOf0(X6,xJ)))|~(sdtpldt0(X5,X6)=sdtasdt0(xz,xx)))))&((((~(aElementOf0(X3,xI))|~(aElementOf0(X4,xJ)))|~(sdtpldt0(X3,X4)=sdtpldt0(xx,xy)))|~(aElementOf0(sdtasdt0(xz,xx),sdtpldt1(xI,xJ))))&(~(aElementOf0(sdtpldt0(xx,xy),sdtpldt1(xI,xJ)))|~(aElementOf0(sdtasdt0(xz,xx),sdtpldt1(xI,xJ)))))),inference(distribute,[status(thm)],[186])).
% cnf(191,negated_conjecture,(sdtpldt0(X1,X2)!=sdtasdt0(xz,xx)|~aElementOf0(X2,xJ)|~aElementOf0(X1,xI)|sdtpldt0(X3,X4)!=sdtpldt0(xx,xy)|~aElementOf0(X4,xJ)|~aElementOf0(X3,xI)),inference(split_conjunct,[status(thm)],[187])).
% fof(503, plain,(~(epred1_0)<=>![X3]:![X4]:((~(sdtpldt0(xx,xy)=sdtpldt0(X3,X4))|~(aElementOf0(X3,xI)))|~(aElementOf0(X4,xJ)))),introduced(definition),['split']).
% cnf(504,plain,(epred1_0|~aElementOf0(X3,xI)|~aElementOf0(X4,xJ)|sdtpldt0(xx,xy)!=sdtpldt0(X3,X4)),inference(split_equiv,[status(thm)],[503])).
% fof(505, plain,(~(epred2_0)<=>![X1]:![X2]:((~(sdtasdt0(xz,xx)=sdtpldt0(X1,X2))|~(aElementOf0(X1,xI)))|~(aElementOf0(X2,xJ)))),introduced(definition),['split']).
% cnf(506,plain,(epred2_0|~aElementOf0(X1,xI)|~aElementOf0(X2,xJ)|sdtasdt0(xz,xx)!=sdtpldt0(X1,X2)),inference(split_equiv,[status(thm)],[505])).
% cnf(507,negated_conjecture,(~epred2_0|~epred1_0),inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[191,503,theory(equality)]),505,theory(equality)]),['split']).
% cnf(689,negated_conjecture,(epred1_0|~aElementOf0(sdtpldt0(xk,xm),xI)|~aElementOf0(sdtpldt0(xl,xn),xJ)),inference(spm,[status(thm)],[504,132,theory(equality)])).
% cnf(710,negated_conjecture,(epred1_0|$false|~aElementOf0(sdtpldt0(xl,xn),xJ)),inference(rw,[status(thm)],[689,129,theory(equality)])).
% cnf(711,negated_conjecture,(epred1_0|$false|$false),inference(rw,[status(thm)],[710,128,theory(equality)])).
% cnf(712,negated_conjecture,(epred1_0),inference(cn,[status(thm)],[711,theory(equality)])).
% cnf(713,negated_conjecture,(~epred2_0|$false),inference(rw,[status(thm)],[507,712,theory(equality)])).
% cnf(714,negated_conjecture,(~epred2_0),inference(cn,[status(thm)],[713,theory(equality)])).
% cnf(716,negated_conjecture,(~aElementOf0(X1,xI)|~aElementOf0(X2,xJ)|sdtasdt0(xz,xx)!=sdtpldt0(X1,X2)),inference(sr,[status(thm)],[506,714,theory(equality)])).
% cnf(721,negated_conjecture,(~aElementOf0(sdtasdt0(xz,xk),xI)|~aElementOf0(sdtasdt0(xz,xl),xJ)),inference(spm,[status(thm)],[716,133,theory(equality)])).
% cnf(732,negated_conjecture,($false|~aElementOf0(sdtasdt0(xz,xl),xJ)),inference(rw,[status(thm)],[721,131,theory(equality)])).
% cnf(733,negated_conjecture,($false|$false),inference(rw,[status(thm)],[732,130,theory(equality)])).
% cnf(734,negated_conjecture,($false),inference(cn,[status(thm)],[733,theory(equality)])).
% cnf(735,negated_conjecture,($false),734,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 123
% # ...of these trivial : 0
% # ...subsumed : 9
% # ...remaining for further processing: 114
% # Other redundant clauses eliminated : 3
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 1
% # Backward-rewritten : 3
% # Generated clauses : 305
% # ...of the previous two non-trivial : 262
% # Contextual simplify-reflections : 0
% # Paramodulations : 292
% # Factorizations : 0
% # Equation resolutions : 10
% # Current number of processed clauses: 109
% # Positive orientable unit clauses: 41
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 2
% # Non-unit-clauses : 66
% # Current number of unprocessed clauses: 207
% # ...number of literals in the above : 942
% # Clause-clause subsumption calls (NU) : 121
% # Rec. Clause-clause subsumption calls : 93
% # Unit Clause-clause subsumption calls : 27
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 2
% # Indexed BW rewrite successes : 2
% # Backwards rewriting index: 148 leaves, 1.25+/-0.999 terms/leaf
% # Paramod-from index: 69 leaves, 1.04+/-0.204 terms/leaf
% # Paramod-into index: 126 leaves, 1.10+/-0.426 terms/leaf
% # -------------------------------------------------
% # User time : 0.027 s
% # System time : 0.006 s
% # Total time : 0.033 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.14 CPU 0.21 WC
% FINAL PrfWatch: 0.14 CPU 0.21 WC
% SZS output end Solution for /tmp/SystemOnTPTP9144/RNG091+2.tptp
%
%------------------------------------------------------------------------------