%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : RNG047+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 : art05.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:05:30 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/SystemOnTPTP14146/RNG047+2.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP14146/RNG047+2.tptp
% SZS output start Solution for /tmp/SystemOnTPTP14146/RNG047+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 14242
% 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(4, axiom,![X1]:![X2]:((aNaturalNumber0(X1)&aNaturalNumber0(X2))=>(szszuzczcdt0(X1)=szszuzczcdt0(X2)=>X1=X2)),file('/tmp/SRASS.s.p', mSuccEqu)).
% fof(5, axiom,![X1]:(aVector0(X1)=>aNaturalNumber0(aDimensionOf0(X1))),file('/tmp/SRASS.s.p', mDimNat)).
% fof(8, axiom,(aDimensionOf0(xs)=aDimensionOf0(xt)&~(aDimensionOf0(xt)=sz00)),file('/tmp/SRASS.s.p', m__1329_01)).
% fof(35, conjecture,(((aVector0(sziznziztdt0(xs))&szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs)))=aDimensionOf0(xs))&![X1]:(aNaturalNumber0(X1)=>sdtlbdtrb0(sziznziztdt0(xs),X1)=sdtlbdtrb0(xs,X1)))=>(((aVector0(sziznziztdt0(xt))&szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt)))=aDimensionOf0(xt))&![X1]:(aNaturalNumber0(X1)=>sdtlbdtrb0(sziznziztdt0(xt),X1)=sdtlbdtrb0(xt,X1)))=>aDimensionOf0(sziznziztdt0(xs))=aDimensionOf0(sziznziztdt0(xt)))),file('/tmp/SRASS.s.p', m__)).
% fof(36, negated_conjecture,~((((aVector0(sziznziztdt0(xs))&szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs)))=aDimensionOf0(xs))&![X1]:(aNaturalNumber0(X1)=>sdtlbdtrb0(sziznziztdt0(xs),X1)=sdtlbdtrb0(xs,X1)))=>(((aVector0(sziznziztdt0(xt))&szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt)))=aDimensionOf0(xt))&![X1]:(aNaturalNumber0(X1)=>sdtlbdtrb0(sziznziztdt0(xt),X1)=sdtlbdtrb0(xt,X1)))=>aDimensionOf0(sziznziztdt0(xs))=aDimensionOf0(sziznziztdt0(xt))))),inference(assume_negation,[status(cth)],[35])).
% fof(54, plain,![X1]:![X2]:((~(aNaturalNumber0(X1))|~(aNaturalNumber0(X2)))|(~(szszuzczcdt0(X1)=szszuzczcdt0(X2))|X1=X2)),inference(fof_nnf,[status(thm)],[4])).
% fof(55, plain,![X3]:![X4]:((~(aNaturalNumber0(X3))|~(aNaturalNumber0(X4)))|(~(szszuzczcdt0(X3)=szszuzczcdt0(X4))|X3=X4)),inference(variable_rename,[status(thm)],[54])).
% cnf(56,plain,(X1=X2|szszuzczcdt0(X1)!=szszuzczcdt0(X2)|~aNaturalNumber0(X2)|~aNaturalNumber0(X1)),inference(split_conjunct,[status(thm)],[55])).
% fof(57, plain,![X1]:(~(aVector0(X1))|aNaturalNumber0(aDimensionOf0(X1))),inference(fof_nnf,[status(thm)],[5])).
% fof(58, plain,![X2]:(~(aVector0(X2))|aNaturalNumber0(aDimensionOf0(X2))),inference(variable_rename,[status(thm)],[57])).
% cnf(59,plain,(aNaturalNumber0(aDimensionOf0(X1))|~aVector0(X1)),inference(split_conjunct,[status(thm)],[58])).
% cnf(73,plain,(aDimensionOf0(xs)=aDimensionOf0(xt)),inference(split_conjunct,[status(thm)],[8])).
% fof(163, negated_conjecture,(((aVector0(sziznziztdt0(xs))&szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs)))=aDimensionOf0(xs))&![X1]:(~(aNaturalNumber0(X1))|sdtlbdtrb0(sziznziztdt0(xs),X1)=sdtlbdtrb0(xs,X1)))&(((aVector0(sziznziztdt0(xt))&szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt)))=aDimensionOf0(xt))&![X1]:(~(aNaturalNumber0(X1))|sdtlbdtrb0(sziznziztdt0(xt),X1)=sdtlbdtrb0(xt,X1)))&~(aDimensionOf0(sziznziztdt0(xs))=aDimensionOf0(sziznziztdt0(xt))))),inference(fof_nnf,[status(thm)],[36])).
% fof(164, negated_conjecture,(((aVector0(sziznziztdt0(xs))&szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs)))=aDimensionOf0(xs))&![X2]:(~(aNaturalNumber0(X2))|sdtlbdtrb0(sziznziztdt0(xs),X2)=sdtlbdtrb0(xs,X2)))&(((aVector0(sziznziztdt0(xt))&szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt)))=aDimensionOf0(xt))&![X3]:(~(aNaturalNumber0(X3))|sdtlbdtrb0(sziznziztdt0(xt),X3)=sdtlbdtrb0(xt,X3)))&~(aDimensionOf0(sziznziztdt0(xs))=aDimensionOf0(sziznziztdt0(xt))))),inference(variable_rename,[status(thm)],[163])).
% fof(165, negated_conjecture,![X2]:![X3]:((((~(aNaturalNumber0(X3))|sdtlbdtrb0(sziznziztdt0(xt),X3)=sdtlbdtrb0(xt,X3))&(aVector0(sziznziztdt0(xt))&szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt)))=aDimensionOf0(xt)))&~(aDimensionOf0(sziznziztdt0(xs))=aDimensionOf0(sziznziztdt0(xt))))&((~(aNaturalNumber0(X2))|sdtlbdtrb0(sziznziztdt0(xs),X2)=sdtlbdtrb0(xs,X2))&(aVector0(sziznziztdt0(xs))&szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs)))=aDimensionOf0(xs)))),inference(shift_quantors,[status(thm)],[164])).
% cnf(166,negated_conjecture,(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs)))=aDimensionOf0(xs)),inference(split_conjunct,[status(thm)],[165])).
% cnf(167,negated_conjecture,(aVector0(sziznziztdt0(xs))),inference(split_conjunct,[status(thm)],[165])).
% cnf(169,negated_conjecture,(aDimensionOf0(sziznziztdt0(xs))!=aDimensionOf0(sziznziztdt0(xt))),inference(split_conjunct,[status(thm)],[165])).
% cnf(170,negated_conjecture,(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xt)))=aDimensionOf0(xt)),inference(split_conjunct,[status(thm)],[165])).
% cnf(171,negated_conjecture,(aVector0(sziznziztdt0(xt))),inference(split_conjunct,[status(thm)],[165])).
% cnf(173,negated_conjecture,(szszuzczcdt0(aDimensionOf0(sziznziztdt0(xs)))=aDimensionOf0(xt)),inference(rw,[status(thm)],[166,73,theory(equality)])).
% cnf(200,negated_conjecture,(X1=aDimensionOf0(sziznziztdt0(xs))|szszuzczcdt0(X1)!=aDimensionOf0(xt)|~aNaturalNumber0(aDimensionOf0(sziznziztdt0(xs)))|~aNaturalNumber0(X1)),inference(spm,[status(thm)],[56,173,theory(equality)])).
% cnf(578,negated_conjecture,(X1=aDimensionOf0(sziznziztdt0(xs))|szszuzczcdt0(X1)!=aDimensionOf0(xt)|~aNaturalNumber0(X1)|~aVector0(sziznziztdt0(xs))),inference(spm,[status(thm)],[200,59,theory(equality)])).
% cnf(579,negated_conjecture,(X1=aDimensionOf0(sziznziztdt0(xs))|szszuzczcdt0(X1)!=aDimensionOf0(xt)|~aNaturalNumber0(X1)|$false),inference(rw,[status(thm)],[578,167,theory(equality)])).
% cnf(580,negated_conjecture,(X1=aDimensionOf0(sziznziztdt0(xs))|szszuzczcdt0(X1)!=aDimensionOf0(xt)|~aNaturalNumber0(X1)),inference(cn,[status(thm)],[579,theory(equality)])).
% cnf(582,negated_conjecture,(aDimensionOf0(sziznziztdt0(xt))=aDimensionOf0(sziznziztdt0(xs))|~aNaturalNumber0(aDimensionOf0(sziznziztdt0(xt)))),inference(spm,[status(thm)],[580,170,theory(equality)])).
% cnf(583,negated_conjecture,(~aNaturalNumber0(aDimensionOf0(sziznziztdt0(xt)))),inference(sr,[status(thm)],[582,169,theory(equality)])).
% cnf(584,negated_conjecture,(~aVector0(sziznziztdt0(xt))),inference(spm,[status(thm)],[583,59,theory(equality)])).
% cnf(585,negated_conjecture,($false),inference(rw,[status(thm)],[584,171,theory(equality)])).
% cnf(586,negated_conjecture,($false),inference(cn,[status(thm)],[585,theory(equality)])).
% cnf(587,negated_conjecture,($false),586,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 72
% # ...of these trivial : 2
% # ...subsumed : 3
% # ...remaining for further processing: 67
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 1
% # Backward-rewritten : 2
% # Generated clauses : 249
% # ...of the previous two non-trivial : 233
% # Contextual simplify-reflections : 0
% # Paramodulations : 242
% # Factorizations : 2
% # Equation resolutions : 5
% # Current number of processed clauses: 64
% # Positive orientable unit clauses: 12
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 3
% # Non-unit-clauses : 49
% # Current number of unprocessed clauses: 218
% # ...number of literals in the above : 1042
% # Clause-clause subsumption calls (NU) : 238
% # Rec. Clause-clause subsumption calls : 85
% # Unit Clause-clause subsumption calls : 0
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 4
% # Indexed BW rewrite successes : 2
% # Backwards rewriting index: 78 leaves, 1.47+/-1.337 terms/leaf
% # Paramod-from index: 41 leaves, 1.17+/-0.436 terms/leaf
% # Paramod-into index: 62 leaves, 1.35+/-1.064 terms/leaf
% # -------------------------------------------------
% # User time : 0.023 s
% # System time : 0.006 s
% # Total time : 0.029 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.12 CPU 0.20 WC
% FINAL PrfWatch: 0.12 CPU 0.20 WC
% SZS output end Solution for /tmp/SystemOnTPTP14146/RNG047+2.tptp
%
%------------------------------------------------------------------------------