%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : CSR016+1 : TPTP v5.0.0. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art06.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 : Tue Dec 28 22:45:31 EST 2010
% Result : Theorem 1.19s
% Output : Solution 1.19s
% 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/SystemOnTPTP14430/CSR016+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP14430/CSR016+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP14430/CSR016+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 14526
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Preprocessing time : 0.022 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(8, axiom,plus(n0,n1)=n1,file('/tmp/SRASS.s.p', plus0_1)).
% fof(12, axiom,![X3]:(less(X3,n1)<=>less_or_equal(X3,n0)),file('/tmp/SRASS.s.p', less1)).
% fof(14, axiom,~(push=pull),file('/tmp/SRASS.s.p', push_not_pull)).
% fof(15, axiom,![X3]:![X5]:plus(X3,X5)=plus(X5,X3),file('/tmp/SRASS.s.p', symmetry_of_plus)).
% fof(16, axiom,![X4]:![X2]:![X1]:((happens(X4,X2)&initiates(X4,X1,X2))=>holdsAt(X1,plus(X2,n1))),file('/tmp/SRASS.s.p', happens_holds)).
% fof(21, axiom,![X4]:![X1]:![X2]:(initiates(X4,X1,X2)<=>((((X4=push&X1=forwards)&~(happens(pull,X2)))|((X4=pull&X1=backwards)&~(happens(push,X2))))|((X4=pull&X1=spinning)&happens(push,X2)))),file('/tmp/SRASS.s.p', initiates_all_defn)).
% fof(25, axiom,![X3]:![X5]:(less_or_equal(X3,X5)<=>(less(X3,X5)|X3=X5)),file('/tmp/SRASS.s.p', less_or_equal)).
% fof(26, axiom,![X3]:(less(X3,n2)<=>less_or_equal(X3,n1)),file('/tmp/SRASS.s.p', less2)).
% fof(30, axiom,![X4]:![X2]:(happens(X4,X2)<=>((((X4=push&X2=n0)|(X4=pull&X2=n1))|(X4=pull&X2=n2))|(X4=push&X2=n2))),file('/tmp/SRASS.s.p', happens_all_defn)).
% fof(31, axiom,![X3]:![X5]:(less(X3,X5)<=>(~(less(X5,X3))&~(X5=X3))),file('/tmp/SRASS.s.p', less_property)).
% fof(48, conjecture,holdsAt(forwards,n1),file('/tmp/SRASS.s.p', forwards_1)).
% fof(49, negated_conjecture,~(holdsAt(forwards,n1)),inference(assume_negation,[status(cth)],[48])).
% fof(59, plain,![X4]:![X1]:![X2]:(initiates(X4,X1,X2)<=>((((X4=push&X1=forwards)&~(happens(pull,X2)))|((X4=pull&X1=backwards)&~(happens(push,X2))))|((X4=pull&X1=spinning)&happens(push,X2)))),inference(fof_simplification,[status(thm)],[21,theory(equality)])).
% fof(62, plain,![X3]:![X5]:(less(X3,X5)<=>(~(less(X5,X3))&~(X5=X3))),inference(fof_simplification,[status(thm)],[31,theory(equality)])).
% fof(65, negated_conjecture,~(holdsAt(forwards,n1)),inference(fof_simplification,[status(thm)],[49,theory(equality)])).
% fof(66, plain,![X1]:![X4]:![X2]:(epred1_3(X2,X4,X1)<=>((((X4=push&X1=forwards)&~(happens(pull,X2)))|((X4=pull&X1=backwards)&~(happens(push,X2))))|((X4=pull&X1=spinning)&happens(push,X2)))),introduced(definition)).
% fof(69, plain,![X4]:![X1]:![X2]:(initiates(X4,X1,X2)<=>epred1_3(X2,X4,X1)),inference(apply_def,[status(esa)],[59,66,theory(equality)])).
% cnf(80,plain,(plus(n0,n1)=n1),inference(split_conjunct,[status(thm)],[8])).
% fof(96, plain,![X3]:((~(less(X3,n1))|less_or_equal(X3,n0))&(~(less_or_equal(X3,n0))|less(X3,n1))),inference(fof_nnf,[status(thm)],[12])).
% fof(97, plain,![X4]:((~(less(X4,n1))|less_or_equal(X4,n0))&(~(less_or_equal(X4,n0))|less(X4,n1))),inference(variable_rename,[status(thm)],[96])).
% cnf(98,plain,(less(X1,n1)|~less_or_equal(X1,n0)),inference(split_conjunct,[status(thm)],[97])).
% cnf(102,plain,(push!=pull),inference(split_conjunct,[status(thm)],[14])).
% fof(103, plain,![X6]:![X7]:plus(X6,X7)=plus(X7,X6),inference(variable_rename,[status(thm)],[15])).
% cnf(104,plain,(plus(X1,X2)=plus(X2,X1)),inference(split_conjunct,[status(thm)],[103])).
% fof(105, plain,![X4]:![X2]:![X1]:((~(happens(X4,X2))|~(initiates(X4,X1,X2)))|holdsAt(X1,plus(X2,n1))),inference(fof_nnf,[status(thm)],[16])).
% fof(106, plain,![X5]:![X6]:![X7]:((~(happens(X5,X6))|~(initiates(X5,X7,X6)))|holdsAt(X7,plus(X6,n1))),inference(variable_rename,[status(thm)],[105])).
% cnf(107,plain,(holdsAt(X1,plus(X2,n1))|~initiates(X3,X1,X2)|~happens(X3,X2)),inference(split_conjunct,[status(thm)],[106])).
% fof(121, plain,![X4]:![X1]:![X2]:((~(initiates(X4,X1,X2))|epred1_3(X2,X4,X1))&(~(epred1_3(X2,X4,X1))|initiates(X4,X1,X2))),inference(fof_nnf,[status(thm)],[69])).
% fof(122, plain,![X5]:![X6]:![X7]:((~(initiates(X5,X6,X7))|epred1_3(X7,X5,X6))&(~(epred1_3(X7,X5,X6))|initiates(X5,X6,X7))),inference(variable_rename,[status(thm)],[121])).
% cnf(123,plain,(initiates(X1,X2,X3)|~epred1_3(X3,X1,X2)),inference(split_conjunct,[status(thm)],[122])).
% fof(140, plain,![X3]:![X5]:((~(less_or_equal(X3,X5))|(less(X3,X5)|X3=X5))&((~(less(X3,X5))&~(X3=X5))|less_or_equal(X3,X5))),inference(fof_nnf,[status(thm)],[25])).
% fof(141, plain,![X6]:![X7]:((~(less_or_equal(X6,X7))|(less(X6,X7)|X6=X7))&((~(less(X6,X7))&~(X6=X7))|less_or_equal(X6,X7))),inference(variable_rename,[status(thm)],[140])).
% fof(142, plain,![X6]:![X7]:((~(less_or_equal(X6,X7))|(less(X6,X7)|X6=X7))&((~(less(X6,X7))|less_or_equal(X6,X7))&(~(X6=X7)|less_or_equal(X6,X7)))),inference(distribute,[status(thm)],[141])).
% cnf(143,plain,(less_or_equal(X1,X2)|X1!=X2),inference(split_conjunct,[status(thm)],[142])).
% cnf(144,plain,(less_or_equal(X1,X2)|~less(X1,X2)),inference(split_conjunct,[status(thm)],[142])).
% fof(146, plain,![X3]:((~(less(X3,n2))|less_or_equal(X3,n1))&(~(less_or_equal(X3,n1))|less(X3,n2))),inference(fof_nnf,[status(thm)],[26])).
% fof(147, plain,![X4]:((~(less(X4,n2))|less_or_equal(X4,n1))&(~(less_or_equal(X4,n1))|less(X4,n2))),inference(variable_rename,[status(thm)],[146])).
% cnf(148,plain,(less(X1,n2)|~less_or_equal(X1,n1)),inference(split_conjunct,[status(thm)],[147])).
% fof(153, plain,![X4]:![X2]:((~(happens(X4,X2))|((((X4=push&X2=n0)|(X4=pull&X2=n1))|(X4=pull&X2=n2))|(X4=push&X2=n2)))&(((((~(X4=push)|~(X2=n0))&(~(X4=pull)|~(X2=n1)))&(~(X4=pull)|~(X2=n2)))&(~(X4=push)|~(X2=n2)))|happens(X4,X2))),inference(fof_nnf,[status(thm)],[30])).
% fof(154, plain,![X5]:![X6]:((~(happens(X5,X6))|((((X5=push&X6=n0)|(X5=pull&X6=n1))|(X5=pull&X6=n2))|(X5=push&X6=n2)))&(((((~(X5=push)|~(X6=n0))&(~(X5=pull)|~(X6=n1)))&(~(X5=pull)|~(X6=n2)))&(~(X5=push)|~(X6=n2)))|happens(X5,X6))),inference(variable_rename,[status(thm)],[153])).
% fof(155, plain,![X5]:![X6]:(((((((X5=push|(X5=pull|(X5=pull|X5=push)))|~(happens(X5,X6)))&((X6=n2|(X5=pull|(X5=pull|X5=push)))|~(happens(X5,X6))))&(((X5=push|(X6=n2|(X5=pull|X5=push)))|~(happens(X5,X6)))&((X6=n2|(X6=n2|(X5=pull|X5=push)))|~(happens(X5,X6)))))&((((X5=push|(X5=pull|(X6=n1|X5=push)))|~(happens(X5,X6)))&((X6=n2|(X5=pull|(X6=n1|X5=push)))|~(happens(X5,X6))))&(((X5=push|(X6=n2|(X6=n1|X5=push)))|~(happens(X5,X6)))&((X6=n2|(X6=n2|(X6=n1|X5=push)))|~(happens(X5,X6))))))&(((((X5=push|(X5=pull|(X5=pull|X6=n0)))|~(happens(X5,X6)))&((X6=n2|(X5=pull|(X5=pull|X6=n0)))|~(happens(X5,X6))))&(((X5=push|(X6=n2|(X5=pull|X6=n0)))|~(happens(X5,X6)))&((X6=n2|(X6=n2|(X5=pull|X6=n0)))|~(happens(X5,X6)))))&((((X5=push|(X5=pull|(X6=n1|X6=n0)))|~(happens(X5,X6)))&((X6=n2|(X5=pull|(X6=n1|X6=n0)))|~(happens(X5,X6))))&(((X5=push|(X6=n2|(X6=n1|X6=n0)))|~(happens(X5,X6)))&((X6=n2|(X6=n2|(X6=n1|X6=n0)))|~(happens(X5,X6)))))))&(((((~(X5=push)|~(X6=n0))|happens(X5,X6))&((~(X5=pull)|~(X6=n1))|happens(X5,X6)))&((~(X5=pull)|~(X6=n2))|happens(X5,X6)))&((~(X5=push)|~(X6=n2))|happens(X5,X6)))),inference(distribute,[status(thm)],[154])).
% cnf(159,plain,(happens(X1,X2)|X2!=n0|X1!=push),inference(split_conjunct,[status(thm)],[155])).
% cnf(168,plain,(X1=push|X2=n1|X2=n2|X2=n2|~happens(X1,X2)),inference(split_conjunct,[status(thm)],[155])).
% fof(176, plain,![X3]:![X5]:((~(less(X3,X5))|(~(less(X5,X3))&~(X5=X3)))&((less(X5,X3)|X5=X3)|less(X3,X5))),inference(fof_nnf,[status(thm)],[62])).
% fof(177, plain,![X6]:![X7]:((~(less(X6,X7))|(~(less(X7,X6))&~(X7=X6)))&((less(X7,X6)|X7=X6)|less(X6,X7))),inference(variable_rename,[status(thm)],[176])).
% fof(178, plain,![X6]:![X7]:(((~(less(X7,X6))|~(less(X6,X7)))&(~(X7=X6)|~(less(X6,X7))))&((less(X7,X6)|X7=X6)|less(X6,X7))),inference(distribute,[status(thm)],[177])).
% cnf(180,plain,(~less(X1,X2)|X2!=X1),inference(split_conjunct,[status(thm)],[178])).
% cnf(241,negated_conjecture,(~holdsAt(forwards,n1)),inference(split_conjunct,[status(thm)],[65])).
% fof(242, plain,![X1]:![X4]:![X2]:((~(epred1_3(X2,X4,X1))|((((X4=push&X1=forwards)&~(happens(pull,X2)))|((X4=pull&X1=backwards)&~(happens(push,X2))))|((X4=pull&X1=spinning)&happens(push,X2))))&(((((~(X4=push)|~(X1=forwards))|happens(pull,X2))&((~(X4=pull)|~(X1=backwards))|happens(push,X2)))&((~(X4=pull)|~(X1=spinning))|~(happens(push,X2))))|epred1_3(X2,X4,X1))),inference(fof_nnf,[status(thm)],[66])).
% fof(243, plain,![X5]:![X6]:![X7]:((~(epred1_3(X7,X6,X5))|((((X6=push&X5=forwards)&~(happens(pull,X7)))|((X6=pull&X5=backwards)&~(happens(push,X7))))|((X6=pull&X5=spinning)&happens(push,X7))))&(((((~(X6=push)|~(X5=forwards))|happens(pull,X7))&((~(X6=pull)|~(X5=backwards))|happens(push,X7)))&((~(X6=pull)|~(X5=spinning))|~(happens(push,X7))))|epred1_3(X7,X6,X5))),inference(variable_rename,[status(thm)],[242])).
% fof(244, plain,![X5]:![X6]:![X7]:(((((((((X6=pull|(X6=pull|X6=push))|~(epred1_3(X7,X6,X5)))&((X5=spinning|(X6=pull|X6=push))|~(epred1_3(X7,X6,X5))))&((happens(push,X7)|(X6=pull|X6=push))|~(epred1_3(X7,X6,X5))))&((((X6=pull|(X5=backwards|X6=push))|~(epred1_3(X7,X6,X5)))&((X5=spinning|(X5=backwards|X6=push))|~(epred1_3(X7,X6,X5))))&((happens(push,X7)|(X5=backwards|X6=push))|~(epred1_3(X7,X6,X5)))))&((((X6=pull|(~(happens(push,X7))|X6=push))|~(epred1_3(X7,X6,X5)))&((X5=spinning|(~(happens(push,X7))|X6=push))|~(epred1_3(X7,X6,X5))))&((happens(push,X7)|(~(happens(push,X7))|X6=push))|~(epred1_3(X7,X6,X5)))))&((((((X6=pull|(X6=pull|X5=forwards))|~(epred1_3(X7,X6,X5)))&((X5=spinning|(X6=pull|X5=forwards))|~(epred1_3(X7,X6,X5))))&((happens(push,X7)|(X6=pull|X5=forwards))|~(epred1_3(X7,X6,X5))))&((((X6=pull|(X5=backwards|X5=forwards))|~(epred1_3(X7,X6,X5)))&((X5=spinning|(X5=backwards|X5=forwards))|~(epred1_3(X7,X6,X5))))&((happens(push,X7)|(X5=backwards|X5=forwards))|~(epred1_3(X7,X6,X5)))))&((((X6=pull|(~(happens(push,X7))|X5=forwards))|~(epred1_3(X7,X6,X5)))&((X5=spinning|(~(happens(push,X7))|X5=forwards))|~(epred1_3(X7,X6,X5))))&((happens(push,X7)|(~(happens(push,X7))|X5=forwards))|~(epred1_3(X7,X6,X5))))))&((((((X6=pull|(X6=pull|~(happens(pull,X7))))|~(epred1_3(X7,X6,X5)))&((X5=spinning|(X6=pull|~(happens(pull,X7))))|~(epred1_3(X7,X6,X5))))&((happens(push,X7)|(X6=pull|~(happens(pull,X7))))|~(epred1_3(X7,X6,X5))))&((((X6=pull|(X5=backwards|~(happens(pull,X7))))|~(epred1_3(X7,X6,X5)))&((X5=spinning|(X5=backwards|~(happens(pull,X7))))|~(epred1_3(X7,X6,X5))))&((happens(push,X7)|(X5=backwards|~(happens(pull,X7))))|~(epred1_3(X7,X6,X5)))))&((((X6=pull|(~(happens(push,X7))|~(happens(pull,X7))))|~(epred1_3(X7,X6,X5)))&((X5=spinning|(~(happens(push,X7))|~(happens(pull,X7))))|~(epred1_3(X7,X6,X5))))&((happens(push,X7)|(~(happens(push,X7))|~(happens(pull,X7))))|~(epred1_3(X7,X6,X5))))))&(((((~(X6=push)|~(X5=forwards))|happens(pull,X7))|epred1_3(X7,X6,X5))&(((~(X6=pull)|~(X5=backwards))|happens(push,X7))|epred1_3(X7,X6,X5)))&(((~(X6=pull)|~(X5=spinning))|~(happens(push,X7)))|epred1_3(X7,X6,X5)))),inference(distribute,[status(thm)],[243])).
% cnf(247,plain,(epred1_3(X1,X2,X3)|happens(pull,X1)|X3!=forwards|X2!=push),inference(split_conjunct,[status(thm)],[244])).
% cnf(342,plain,(less_or_equal(X1,X1)),inference(er,[status(thm)],[143,theory(equality)])).
% cnf(343,plain,(~less(X1,X1)),inference(er,[status(thm)],[180,theory(equality)])).
% cnf(345,plain,(happens(X1,n0)|push!=X1),inference(er,[status(thm)],[159,theory(equality)])).
% cnf(354,plain,(plus(n1,n0)=n1),inference(rw,[status(thm)],[80,104,theory(equality)])).
% cnf(419,plain,(epred1_3(X1,X2,forwards)|happens(pull,X1)|push!=X2),inference(er,[status(thm)],[247,theory(equality)])).
% cnf(505,plain,(less(n0,n1)),inference(spm,[status(thm)],[98,342,theory(equality)])).
% cnf(533,plain,(less_or_equal(n0,n1)),inference(spm,[status(thm)],[144,505,theory(equality)])).
% cnf(560,plain,(less(n0,n2)),inference(spm,[status(thm)],[148,533,theory(equality)])).
% cnf(576,plain,(happens(push,n0)),inference(er,[status(thm)],[345,theory(equality)])).
% cnf(1279,plain,(epred1_3(X1,push,forwards)|happens(pull,X1)),inference(er,[status(thm)],[419,theory(equality)])).
% cnf(1284,plain,(initiates(push,forwards,X1)|happens(pull,X1)),inference(spm,[status(thm)],[123,1279,theory(equality)])).
% cnf(1288,plain,(holdsAt(forwards,plus(X1,n1))|happens(pull,X1)|~happens(push,X1)),inference(spm,[status(thm)],[107,1284,theory(equality)])).
% cnf(7032,plain,(happens(pull,n0)|holdsAt(forwards,plus(n0,n1))),inference(spm,[status(thm)],[1288,576,theory(equality)])).
% cnf(7035,plain,(happens(pull,n0)|holdsAt(forwards,n1)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[7032,104,theory(equality)]),354,theory(equality)])).
% cnf(7036,plain,(happens(pull,n0)),inference(sr,[status(thm)],[7035,241,theory(equality)])).
% cnf(7037,plain,(n2=n0|push=pull|n1=n0),inference(spm,[status(thm)],[168,7036,theory(equality)])).
% cnf(7054,plain,(n0=n2|n0=n1),inference(sr,[status(thm)],[7037,102,theory(equality)])).
% cnf(7077,plain,(less(n2,n2)|n0=n1),inference(spm,[status(thm)],[560,7054,theory(equality)])).
% cnf(7115,plain,(n0=n1),inference(sr,[status(thm)],[7077,343,theory(equality)])).
% cnf(7190,plain,(less(n1,n1)),inference(rw,[status(thm)],[505,7115,theory(equality)])).
% cnf(7191,plain,($false),inference(sr,[status(thm)],[7190,343,theory(equality)])).
% cnf(7192,plain,($false),7191,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 895
% # ...of these trivial : 5
% # ...subsumed : 339
% # ...remaining for further processing: 551
% # Other redundant clauses eliminated : 2
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 36
% # Backward-rewritten : 67
% # Generated clauses : 3233
% # ...of the previous two non-trivial : 1128
% # Contextual simplify-reflections : 163
% # Paramodulations : 3201
% # Factorizations : 5
% # Equation resolutions : 27
% # Current number of processed clauses: 446
% # Positive orientable unit clauses: 92
% # Positive unorientable unit clauses: 1
% # Negative unit clauses : 46
% # Non-unit-clauses : 307
% # Current number of unprocessed clauses: 276
% # ...number of literals in the above : 1068
% # Clause-clause subsumption calls (NU) : 8830
% # Rec. Clause-clause subsumption calls : 4495
% # Unit Clause-clause subsumption calls : 1194
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 51
% # Indexed BW rewrite successes : 39
% # Backwards rewriting index: 281 leaves, 1.36+/-1.351 terms/leaf
% # Paramod-from index: 145 leaves, 1.03+/-0.182 terms/leaf
% # Paramod-into index: 228 leaves, 1.22+/-0.866 terms/leaf
% # -------------------------------------------------
% # User time : 0.156 s
% # System time : 0.009 s
% # Total time : 0.165 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.32 CPU 0.41 WC
% FINAL PrfWatch: 0.32 CPU 0.41 WC
% SZS output end Solution for /tmp/SystemOnTPTP14430/CSR016+1.tptp
%
%------------------------------------------------------------------------------