%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : RNG108+4 : 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 22:43:44 EST 2010
% Result : Theorem 1.27s
% Output : Solution 1.27s
% 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/SystemOnTPTP13647/RNG108+4.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP13647/RNG108+4.tptp
% SZS output start Solution for /tmp/SystemOnTPTP13647/RNG108+4.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 13779
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% # Preprocessing time : 0.024 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,aElement0(sz00),file('/tmp/SRASS.s.p', mSortsC)).
% fof(10, axiom,![X1]:(aElement0(X1)=>(sdtasdt0(X1,sz00)=sz00&sz00=sdtasdt0(sz00,X1))),file('/tmp/SRASS.s.p', mMulZero)).
% fof(22, axiom,(aElement0(xa)&aElement0(xb)),file('/tmp/SRASS.s.p', m__2091)).
% fof(29, axiom,![X1]:(aElement0(X1)=>(sdtasdt0(X1,sz10)=X1&X1=sdtasdt0(sz10,X1))),file('/tmp/SRASS.s.p', mMulUnit)).
% fof(33, axiom,aElement0(sz10),file('/tmp/SRASS.s.p', mSortsC_01)).
% fof(43, conjecture,((((?[X1]:(aElement0(X1)&sdtasdt0(xa,X1)=sz00)|aElementOf0(sz00,slsdtgt0(xa)))&(?[X1]:(aElement0(X1)&sdtasdt0(xa,X1)=xa)|aElementOf0(xa,slsdtgt0(xa))))&(?[X1]:(aElement0(X1)&sdtasdt0(xb,X1)=sz00)|aElementOf0(sz00,slsdtgt0(xb))))&(?[X1]:(aElement0(X1)&sdtasdt0(xb,X1)=xb)|aElementOf0(xb,slsdtgt0(xb)))),file('/tmp/SRASS.s.p', m__)).
% fof(44, negated_conjecture,~(((((?[X1]:(aElement0(X1)&sdtasdt0(xa,X1)=sz00)|aElementOf0(sz00,slsdtgt0(xa)))&(?[X1]:(aElement0(X1)&sdtasdt0(xa,X1)=xa)|aElementOf0(xa,slsdtgt0(xa))))&(?[X1]:(aElement0(X1)&sdtasdt0(xb,X1)=sz00)|aElementOf0(sz00,slsdtgt0(xb))))&(?[X1]:(aElement0(X1)&sdtasdt0(xb,X1)=xb)|aElementOf0(xb,slsdtgt0(xb))))),inference(assume_negation,[status(cth)],[43])).
% cnf(49,plain,(aElement0(sz00)),inference(split_conjunct,[status(thm)],[1])).
% fof(78, plain,![X1]:(~(aElement0(X1))|(sdtasdt0(X1,sz00)=sz00&sz00=sdtasdt0(sz00,X1))),inference(fof_nnf,[status(thm)],[10])).
% fof(79, plain,![X2]:(~(aElement0(X2))|(sdtasdt0(X2,sz00)=sz00&sz00=sdtasdt0(sz00,X2))),inference(variable_rename,[status(thm)],[78])).
% fof(80, plain,![X2]:((sdtasdt0(X2,sz00)=sz00|~(aElement0(X2)))&(sz00=sdtasdt0(sz00,X2)|~(aElement0(X2)))),inference(distribute,[status(thm)],[79])).
% cnf(82,plain,(sdtasdt0(X1,sz00)=sz00|~aElement0(X1)),inference(split_conjunct,[status(thm)],[80])).
% cnf(169,plain,(aElement0(xb)),inference(split_conjunct,[status(thm)],[22])).
% cnf(170,plain,(aElement0(xa)),inference(split_conjunct,[status(thm)],[22])).
% fof(263, plain,![X1]:(~(aElement0(X1))|(sdtasdt0(X1,sz10)=X1&X1=sdtasdt0(sz10,X1))),inference(fof_nnf,[status(thm)],[29])).
% fof(264, plain,![X2]:(~(aElement0(X2))|(sdtasdt0(X2,sz10)=X2&X2=sdtasdt0(sz10,X2))),inference(variable_rename,[status(thm)],[263])).
% fof(265, plain,![X2]:((sdtasdt0(X2,sz10)=X2|~(aElement0(X2)))&(X2=sdtasdt0(sz10,X2)|~(aElement0(X2)))),inference(distribute,[status(thm)],[264])).
% cnf(267,plain,(sdtasdt0(X1,sz10)=X1|~aElement0(X1)),inference(split_conjunct,[status(thm)],[265])).
% cnf(282,plain,(aElement0(sz10)),inference(split_conjunct,[status(thm)],[33])).
% fof(310, negated_conjecture,((((![X1]:(~(aElement0(X1))|~(sdtasdt0(xa,X1)=sz00))&~(aElementOf0(sz00,slsdtgt0(xa))))|(![X1]:(~(aElement0(X1))|~(sdtasdt0(xa,X1)=xa))&~(aElementOf0(xa,slsdtgt0(xa)))))|(![X1]:(~(aElement0(X1))|~(sdtasdt0(xb,X1)=sz00))&~(aElementOf0(sz00,slsdtgt0(xb)))))|(![X1]:(~(aElement0(X1))|~(sdtasdt0(xb,X1)=xb))&~(aElementOf0(xb,slsdtgt0(xb))))),inference(fof_nnf,[status(thm)],[44])).
% fof(311, negated_conjecture,((((![X2]:(~(aElement0(X2))|~(sdtasdt0(xa,X2)=sz00))&~(aElementOf0(sz00,slsdtgt0(xa))))|(![X3]:(~(aElement0(X3))|~(sdtasdt0(xa,X3)=xa))&~(aElementOf0(xa,slsdtgt0(xa)))))|(![X4]:(~(aElement0(X4))|~(sdtasdt0(xb,X4)=sz00))&~(aElementOf0(sz00,slsdtgt0(xb)))))|(![X5]:(~(aElement0(X5))|~(sdtasdt0(xb,X5)=xb))&~(aElementOf0(xb,slsdtgt0(xb))))),inference(variable_rename,[status(thm)],[310])).
% fof(312, negated_conjecture,![X2]:![X3]:![X4]:![X5]:(((~(aElement0(X5))|~(sdtasdt0(xb,X5)=xb))&~(aElementOf0(xb,slsdtgt0(xb))))|(((~(aElement0(X4))|~(sdtasdt0(xb,X4)=sz00))&~(aElementOf0(sz00,slsdtgt0(xb))))|(((~(aElement0(X3))|~(sdtasdt0(xa,X3)=xa))&~(aElementOf0(xa,slsdtgt0(xa))))|((~(aElement0(X2))|~(sdtasdt0(xa,X2)=sz00))&~(aElementOf0(sz00,slsdtgt0(xa))))))),inference(shift_quantors,[status(thm)],[311])).
% fof(313, negated_conjecture,![X2]:![X3]:![X4]:![X5]:((((((((~(aElement0(X2))|~(sdtasdt0(xa,X2)=sz00))|(~(aElement0(X3))|~(sdtasdt0(xa,X3)=xa)))|(~(aElement0(X4))|~(sdtasdt0(xb,X4)=sz00)))|(~(aElement0(X5))|~(sdtasdt0(xb,X5)=xb)))&(((~(aElementOf0(sz00,slsdtgt0(xa)))|(~(aElement0(X3))|~(sdtasdt0(xa,X3)=xa)))|(~(aElement0(X4))|~(sdtasdt0(xb,X4)=sz00)))|(~(aElement0(X5))|~(sdtasdt0(xb,X5)=xb))))&(((((~(aElement0(X2))|~(sdtasdt0(xa,X2)=sz00))|~(aElementOf0(xa,slsdtgt0(xa))))|(~(aElement0(X4))|~(sdtasdt0(xb,X4)=sz00)))|(~(aElement0(X5))|~(sdtasdt0(xb,X5)=xb)))&(((~(aElementOf0(sz00,slsdtgt0(xa)))|~(aElementOf0(xa,slsdtgt0(xa))))|(~(aElement0(X4))|~(sdtasdt0(xb,X4)=sz00)))|(~(aElement0(X5))|~(sdtasdt0(xb,X5)=xb)))))&((((((~(aElement0(X2))|~(sdtasdt0(xa,X2)=sz00))|(~(aElement0(X3))|~(sdtasdt0(xa,X3)=xa)))|~(aElementOf0(sz00,slsdtgt0(xb))))|(~(aElement0(X5))|~(sdtasdt0(xb,X5)=xb)))&(((~(aElementOf0(sz00,slsdtgt0(xa)))|(~(aElement0(X3))|~(sdtasdt0(xa,X3)=xa)))|~(aElementOf0(sz00,slsdtgt0(xb))))|(~(aElement0(X5))|~(sdtasdt0(xb,X5)=xb))))&(((((~(aElement0(X2))|~(sdtasdt0(xa,X2)=sz00))|~(aElementOf0(xa,slsdtgt0(xa))))|~(aElementOf0(sz00,slsdtgt0(xb))))|(~(aElement0(X5))|~(sdtasdt0(xb,X5)=xb)))&(((~(aElementOf0(sz00,slsdtgt0(xa)))|~(aElementOf0(xa,slsdtgt0(xa))))|~(aElementOf0(sz00,slsdtgt0(xb))))|(~(aElement0(X5))|~(sdtasdt0(xb,X5)=xb))))))&(((((((~(aElement0(X2))|~(sdtasdt0(xa,X2)=sz00))|(~(aElement0(X3))|~(sdtasdt0(xa,X3)=xa)))|(~(aElement0(X4))|~(sdtasdt0(xb,X4)=sz00)))|~(aElementOf0(xb,slsdtgt0(xb))))&(((~(aElementOf0(sz00,slsdtgt0(xa)))|(~(aElement0(X3))|~(sdtasdt0(xa,X3)=xa)))|(~(aElement0(X4))|~(sdtasdt0(xb,X4)=sz00)))|~(aElementOf0(xb,slsdtgt0(xb)))))&(((((~(aElement0(X2))|~(sdtasdt0(xa,X2)=sz00))|~(aElementOf0(xa,slsdtgt0(xa))))|(~(aElement0(X4))|~(sdtasdt0(xb,X4)=sz00)))|~(aElementOf0(xb,slsdtgt0(xb))))&(((~(aElementOf0(sz00,slsdtgt0(xa)))|~(aElementOf0(xa,slsdtgt0(xa))))|(~(aElement0(X4))|~(sdtasdt0(xb,X4)=sz00)))|~(aElementOf0(xb,slsdtgt0(xb))))))&((((((~(aElement0(X2))|~(sdtasdt0(xa,X2)=sz00))|(~(aElement0(X3))|~(sdtasdt0(xa,X3)=xa)))|~(aElementOf0(sz00,slsdtgt0(xb))))|~(aElementOf0(xb,slsdtgt0(xb))))&(((~(aElementOf0(sz00,slsdtgt0(xa)))|(~(aElement0(X3))|~(sdtasdt0(xa,X3)=xa)))|~(aElementOf0(sz00,slsdtgt0(xb))))|~(aElementOf0(xb,slsdtgt0(xb)))))&(((((~(aElement0(X2))|~(sdtasdt0(xa,X2)=sz00))|~(aElementOf0(xa,slsdtgt0(xa))))|~(aElementOf0(sz00,slsdtgt0(xb))))|~(aElementOf0(xb,slsdtgt0(xb))))&(((~(aElementOf0(sz00,slsdtgt0(xa)))|~(aElementOf0(xa,slsdtgt0(xa))))|~(aElementOf0(sz00,slsdtgt0(xb))))|~(aElementOf0(xb,slsdtgt0(xb)))))))),inference(distribute,[status(thm)],[312])).
% cnf(329,negated_conjecture,(sdtasdt0(xb,X1)!=xb|~aElement0(X1)|sdtasdt0(xb,X2)!=sz00|~aElement0(X2)|sdtasdt0(xa,X3)!=xa|~aElement0(X3)|sdtasdt0(xa,X4)!=sz00|~aElement0(X4)),inference(split_conjunct,[status(thm)],[313])).
% fof(333, plain,(~(epred2_0)<=>![X1]:(~(sdtasdt0(xa,X1)=xa)|~(aElement0(X1)))),introduced(definition),['split']).
% cnf(334,plain,(epred2_0|~aElement0(X1)|sdtasdt0(xa,X1)!=xa),inference(split_equiv,[status(thm)],[333])).
% fof(338, plain,(~(epred4_0)<=>![X1]:(~(sdtasdt0(xb,X1)=sz00)|~(aElement0(X1)))),introduced(definition),['split']).
% cnf(339,plain,(epred4_0|~aElement0(X1)|sdtasdt0(xb,X1)!=sz00),inference(split_equiv,[status(thm)],[338])).
% fof(343, plain,(~(epred6_0)<=>![X1]:(~(sdtasdt0(xb,X1)=xb)|~(aElement0(X1)))),introduced(definition),['split']).
% cnf(344,plain,(epred6_0|~aElement0(X1)|sdtasdt0(xb,X1)!=xb),inference(split_equiv,[status(thm)],[343])).
% fof(367, plain,(~(epred14_0)<=>![X4]:(~(sdtasdt0(xa,X4)=sz00)|~(aElement0(X4)))),introduced(definition),['split']).
% cnf(368,plain,(epred14_0|~aElement0(X4)|sdtasdt0(xa,X4)!=sz00),inference(split_equiv,[status(thm)],[367])).
% cnf(369,negated_conjecture,(~epred6_0|~epred4_0|~epred2_0|~epred14_0),inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[329,367,theory(equality)]),333,theory(equality)]),338,theory(equality)]),343,theory(equality)]),['split']).
% cnf(374,negated_conjecture,(epred4_0|~aElement0(sz00)|~aElement0(xb)),inference(spm,[status(thm)],[339,82,theory(equality)])).
% cnf(375,negated_conjecture,(epred4_0|$false|~aElement0(xb)),inference(rw,[status(thm)],[374,49,theory(equality)])).
% cnf(376,negated_conjecture,(epred4_0|$false|$false),inference(rw,[status(thm)],[375,169,theory(equality)])).
% cnf(377,negated_conjecture,(epred4_0),inference(cn,[status(thm)],[376,theory(equality)])).
% cnf(383,negated_conjecture,(epred6_0|~aElement0(sz10)|~aElement0(xb)),inference(spm,[status(thm)],[344,267,theory(equality)])).
% cnf(384,negated_conjecture,(epred2_0|~aElement0(sz10)|~aElement0(xa)),inference(spm,[status(thm)],[334,267,theory(equality)])).
% cnf(388,negated_conjecture,(epred6_0|$false|~aElement0(xb)),inference(rw,[status(thm)],[383,282,theory(equality)])).
% cnf(389,negated_conjecture,(epred6_0|$false|$false),inference(rw,[status(thm)],[388,169,theory(equality)])).
% cnf(390,negated_conjecture,(epred6_0),inference(cn,[status(thm)],[389,theory(equality)])).
% cnf(391,negated_conjecture,(epred2_0|$false|~aElement0(xa)),inference(rw,[status(thm)],[384,282,theory(equality)])).
% cnf(392,negated_conjecture,(epred2_0|$false|$false),inference(rw,[status(thm)],[391,170,theory(equality)])).
% cnf(393,negated_conjecture,(epred2_0),inference(cn,[status(thm)],[392,theory(equality)])).
% cnf(397,negated_conjecture,(epred14_0|~aElement0(sz00)|~aElement0(xa)),inference(spm,[status(thm)],[368,82,theory(equality)])).
% cnf(401,negated_conjecture,(epred14_0|$false|~aElement0(xa)),inference(rw,[status(thm)],[397,49,theory(equality)])).
% cnf(402,negated_conjecture,(epred14_0|$false|$false),inference(rw,[status(thm)],[401,170,theory(equality)])).
% cnf(403,negated_conjecture,(epred14_0),inference(cn,[status(thm)],[402,theory(equality)])).
% cnf(1842,negated_conjecture,(~epred14_0|~epred6_0|$false|~epred2_0),inference(rw,[status(thm)],[369,377,theory(equality)])).
% cnf(1843,negated_conjecture,(~epred14_0|~epred6_0|~epred2_0),inference(cn,[status(thm)],[1842,theory(equality)])).
% cnf(1869,negated_conjecture,($false|~epred6_0|~epred2_0),inference(rw,[status(thm)],[1843,403,theory(equality)])).
% cnf(1870,negated_conjecture,($false|$false|~epred2_0),inference(rw,[status(thm)],[1869,390,theory(equality)])).
% cnf(1871,negated_conjecture,($false|$false|$false),inference(rw,[status(thm)],[1870,393,theory(equality)])).
% cnf(1872,negated_conjecture,($false),inference(cn,[status(thm)],[1871,theory(equality)])).
% cnf(1873,negated_conjecture,($false),1872,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 381
% # ...of these trivial : 5
% # ...subsumed : 0
% # ...remaining for further processing: 376
% # Other redundant clauses eliminated : 28
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 0
% # Backward-rewritten : 15
% # Generated clauses : 804
% # ...of the previous two non-trivial : 721
% # Contextual simplify-reflections : 0
% # Paramodulations : 739
% # Factorizations : 0
% # Equation resolutions : 40
% # Current number of processed clauses: 175
% # Positive orientable unit clauses: 23
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 11
% # Non-unit-clauses : 141
% # Current number of unprocessed clauses: 631
% # ...number of literals in the above : 3112
% # Clause-clause subsumption calls (NU) : 1509
% # Rec. Clause-clause subsumption calls : 555
% # Unit Clause-clause subsumption calls : 271
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 4
% # Indexed BW rewrite successes : 4
% # Backwards rewriting index: 176 leaves, 1.32+/-1.051 terms/leaf
% # Paramod-from index: 79 leaves, 1.06+/-0.243 terms/leaf
% # Paramod-into index: 154 leaves, 1.16+/-0.552 terms/leaf
% # -------------------------------------------------
% # User time : 0.076 s
% # System time : 0.005 s
% # Total time : 0.081 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.21 CPU 0.27 WC
% FINAL PrfWatch: 0.21 CPU 0.27 WC
% SZS output end Solution for /tmp/SystemOnTPTP13647/RNG108+4.tptp
%
%------------------------------------------------------------------------------