%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : LCL902+1 : TPTP v5.5.0. Released v5.5.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 : 2005MB
% OS : Linux 2.6.32.26-175.fc12.i686.PAE
% CPULimit : 300s
% DateTime : Mon Oct 22 19:09:37 EDT 2012
% Result : Theorem 0.71s
% Output : Solution 0.71s
% 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/SystemOnTPTP3439/LCL902+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP3439/LCL902+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP3439/LCL902+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.6/eproof_ram --print-statistics --auto --cpu-limit=60 --memory-limit=1024 --tstp-format /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 3553
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% # No SinE strategy applied
% # Auto-Ordering is analysing problem.
% # Problem is type HUSMGFFSF22MM
% # Auto-mode selected ordering type KBO6
% # Auto-mode selected ordering precedence scheme <invfreq>
% # Auto-mode selected weight ordering scheme <invfreqrank>
% #
% # Auto-Heuristic is analysing problem.
% # Problem is type HUSMGFFSF22MM
% # Auto-Mode selected heuristic H_____102_C18_F1_PI_AE_Q4_CS_SP_PS_S2S
% # and selection function SelectNewComplexAHP.
% #
% # Initializing proof state
% # Scanning for AC axioms
% # '+' is AC
% # AC handling enabled
% # Presaturation interreduction done
% # Proof found!
% # SZS status Theorem
% # Parsed axioms : 14
% # Removed by relevancy pruning/SinE : 0
% # Initial clauses : 15
% # Removed in clause preprocessing : 0
% # Initial clauses in saturation : 15
% # Processed clauses : 421
% # ...of these trivial : 69
% # ...subsumed : 167
% # ...remaining for further processing: 185
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 1
% # Backward-rewritten : 49
% # Generated clauses : 5336
% # ...of the previous two non-trivial : 2327
% # Contextual simplify-reflections : 0
% # Paramodulations : 5336
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 120
% # Positive orientable unit clauses: 81
% # Positive unorientable unit clauses: 3
% # Negative unit clauses : 0
% # Non-unit-clauses : 36
% # Current number of unprocessed clauses: 1397
% # ...number of literals in the above : 1619
% # Clause-clause subsumption calls (NU) : 506
% # Rec. Clause-clause subsumption calls : 506
% # Non-unit clause-clause subsumptions: 159
% # Unit Clause-clause subsumption calls : 33
% # Rewrite failures with RHS unbound : 0
% # BW rewrite match attempts : 181
% # BW rewrite match successes : 64
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:'==>'('==>'('==>'(X1,'1'),X1),X1)='0',file('/tmp/SRASS.s.p', sos_13)).
% fof(2, axiom,![X1]:'+'(X1,'1')='1',file('/tmp/SRASS.s.p', sos_12)).
% fof(4, axiom,![X5]:![X6]:![X7]:('>='(X5,X6)=>'>='('==>'(X7,X5),'==>'(X7,X6))),file('/tmp/SRASS.s.p', sos_11)).
% fof(5, axiom,![X8]:![X9]:(('>='(X8,X9)&'>='(X9,X8))=>X8=X9),file('/tmp/SRASS.s.p', sos_06)).
% fof(6, axiom,![X1]:![X10]:![X11]:'+'('+'(X1,X10),X11)='+'(X1,'+'(X10,X11)),file('/tmp/SRASS.s.p', sos_01)).
% fof(7, axiom,![X1]:![X10]:'+'(X1,X10)='+'(X10,X1),file('/tmp/SRASS.s.p', sos_02)).
% fof(8, axiom,![X1]:'>='(X1,X1),file('/tmp/SRASS.s.p', sos_04)).
% fof(10, axiom,![X15]:![X16]:![X17]:('>='('+'(X15,X16),X17)<=>'>='(X16,'==>'(X15,X17))),file('/tmp/SRASS.s.p', sos_07)).
% fof(11, axiom,![X1]:'+'(X1,'0')=X1,file('/tmp/SRASS.s.p', sos_03)).
% fof(12, axiom,![X1]:'>='(X1,'0'),file('/tmp/SRASS.s.p', sos_08)).
% fof(14, conjecture,![X21]:'==>'('==>'(X21,'1'),'1')=X21,file('/tmp/SRASS.s.p', goals_14)).
% fof(15, negated_conjecture,~(![X21]:'==>'('==>'(X21,'1'),'1')=X21),inference(assume_negation,[status(cth)],[14])).
% fof(16, plain,![X2]:'==>'('==>'('==>'(X2,'1'),X2),X2)='0',inference(variable_rename,[status(thm)],[1])).
% cnf(17,plain,('==>'('==>'('==>'(X1,'1'),X1),X1)='0'),inference(split_conjunct,[status(thm)],[16])).
% fof(18, plain,![X2]:'+'(X2,'1')='1',inference(variable_rename,[status(thm)],[2])).
% cnf(19,plain,('+'(X1,'1')='1'),inference(split_conjunct,[status(thm)],[18])).
% fof(25, plain,![X5]:![X6]:![X7]:(~('>='(X5,X6))|'>='('==>'(X7,X5),'==>'(X7,X6))),inference(fof_nnf,[status(thm)],[4])).
% fof(26, plain,![X5]:![X6]:(~('>='(X5,X6))|![X7]:'>='('==>'(X7,X5),'==>'(X7,X6))),inference(shift_quantors,[status(thm)],[25])).
% fof(27, plain,![X8]:![X9]:(~('>='(X8,X9))|![X10]:'>='('==>'(X10,X8),'==>'(X10,X9))),inference(variable_rename,[status(thm)],[26])).
% fof(28, plain,![X8]:![X9]:![X10]:(~('>='(X8,X9))|'>='('==>'(X10,X8),'==>'(X10,X9))),inference(shift_quantors,[status(thm)],[27])).
% cnf(29,plain,('>='('==>'(X1,X2),'==>'(X1,X3))|~'>='(X2,X3)),inference(split_conjunct,[status(thm)],[28])).
% fof(30, plain,![X8]:![X9]:((~('>='(X8,X9))|~('>='(X9,X8)))|X8=X9),inference(fof_nnf,[status(thm)],[5])).
% fof(31, plain,![X10]:![X11]:((~('>='(X10,X11))|~('>='(X11,X10)))|X10=X11),inference(variable_rename,[status(thm)],[30])).
% cnf(32,plain,(X1=X2|~'>='(X2,X1)|~'>='(X1,X2)),inference(split_conjunct,[status(thm)],[31])).
% fof(33, plain,![X12]:![X13]:![X14]:'+'('+'(X12,X13),X14)='+'(X12,'+'(X13,X14)),inference(variable_rename,[status(thm)],[6])).
% cnf(34,plain,('+'('+'(X1,X2),X3)='+'(X1,'+'(X2,X3))),inference(split_conjunct,[status(thm)],[33])).
% fof(35, plain,![X11]:![X12]:'+'(X11,X12)='+'(X12,X11),inference(variable_rename,[status(thm)],[7])).
% cnf(36,plain,('+'(X1,X2)='+'(X2,X1)),inference(split_conjunct,[status(thm)],[35])).
% fof(37, plain,![X2]:'>='(X2,X2),inference(variable_rename,[status(thm)],[8])).
% cnf(38,plain,('>='(X1,X1)),inference(split_conjunct,[status(thm)],[37])).
% fof(42, plain,![X15]:![X16]:![X17]:((~('>='('+'(X15,X16),X17))|'>='(X16,'==>'(X15,X17)))&(~('>='(X16,'==>'(X15,X17)))|'>='('+'(X15,X16),X17))),inference(fof_nnf,[status(thm)],[10])).
% fof(43, plain,(![X15]:![X16]:![X17]:(~('>='('+'(X15,X16),X17))|'>='(X16,'==>'(X15,X17)))&![X15]:![X16]:![X17]:(~('>='(X16,'==>'(X15,X17)))|'>='('+'(X15,X16),X17))),inference(shift_quantors,[status(thm)],[42])).
% fof(44, plain,(![X18]:![X19]:![X20]:(~('>='('+'(X18,X19),X20))|'>='(X19,'==>'(X18,X20)))&![X21]:![X22]:![X23]:(~('>='(X22,'==>'(X21,X23)))|'>='('+'(X21,X22),X23))),inference(variable_rename,[status(thm)],[43])).
% fof(45, plain,![X18]:![X19]:![X20]:![X21]:![X22]:![X23]:((~('>='('+'(X18,X19),X20))|'>='(X19,'==>'(X18,X20)))&(~('>='(X22,'==>'(X21,X23)))|'>='('+'(X21,X22),X23))),inference(shift_quantors,[status(thm)],[44])).
% cnf(46,plain,('>='('+'(X1,X2),X3)|~'>='(X2,'==>'(X1,X3))),inference(split_conjunct,[status(thm)],[45])).
% cnf(47,plain,('>='(X1,'==>'(X2,X3))|~'>='('+'(X2,X1),X3)),inference(split_conjunct,[status(thm)],[45])).
% fof(48, plain,![X2]:'+'(X2,'0')=X2,inference(variable_rename,[status(thm)],[11])).
% cnf(49,plain,('+'(X1,'0')=X1),inference(split_conjunct,[status(thm)],[48])).
% fof(50, plain,![X2]:'>='(X2,'0'),inference(variable_rename,[status(thm)],[12])).
% cnf(51,plain,('>='(X1,'0')),inference(split_conjunct,[status(thm)],[50])).
% fof(57, negated_conjecture,?[X21]:~('==>'('==>'(X21,'1'),'1')=X21),inference(fof_nnf,[status(thm)],[15])).
% fof(58, negated_conjecture,?[X22]:~('==>'('==>'(X22,'1'),'1')=X22),inference(variable_rename,[status(thm)],[57])).
% fof(59, negated_conjecture,~('==>'('==>'(esk1_0,'1'),'1')=esk1_0),inference(skolemize,[status(esa)],[58])).
% cnf(60,negated_conjecture,('==>'('==>'(esk1_0,'1'),'1')!=esk1_0),inference(split_conjunct,[status(thm)],[59])).
% cnf(74,plain,('+'('1',X1)='1'),inference(spm,[status(thm)],[19,36,theory(equality)])).
% cnf(92,plain,('>='('0','==>'(X1,X2))|~'>='(X1,X2)),inference(spm,[status(thm)],[47,49,theory(equality)])).
% cnf(94,plain,('>='(X1,'==>'(X2,X3))|~'>='('+'(X1,X2),X3)),inference(spm,[status(thm)],[47,36,theory(equality)])).
% cnf(102,plain,('>='('+'(X1,'==>'(X1,X2)),X2)),inference(spm,[status(thm)],[46,38,theory(equality)])).
% cnf(136,plain,('>='('0','==>'(X1,X1))),inference(spm,[status(thm)],[92,38,theory(equality)])).
% cnf(230,plain,('==>'(X1,X1)='0'|~'>='('==>'(X1,X1),'0')),inference(spm,[status(thm)],[32,136,theory(equality)])).
% cnf(241,plain,('==>'(X1,X1)='0'|$false),inference(rw,[status(thm)],[230,51,theory(equality)])).
% cnf(242,plain,('==>'(X1,X1)='0'),inference(cn,[status(thm)],[241,theory(equality)])).
% cnf(253,plain,('>='('+'(X1,X2),X1)|~'>='(X2,'0')),inference(spm,[status(thm)],[46,242,theory(equality)])).
% cnf(260,plain,('>='('+'(X1,X2),X1)|$false),inference(rw,[status(thm)],[253,51,theory(equality)])).
% cnf(261,plain,('>='('+'(X1,X2),X1)),inference(cn,[status(thm)],[260,theory(equality)])).
% cnf(377,plain,('>='('==>'(X1,'+'(X2,X3)),'==>'(X1,X2))),inference(spm,[status(thm)],[29,261,theory(equality)])).
% cnf(379,plain,('>='(X1,'==>'(X2,X1))),inference(spm,[status(thm)],[94,261,theory(equality)])).
% cnf(384,plain,('>='('1',X1)),inference(spm,[status(thm)],[261,19,theory(equality)])).
% cnf(395,plain,(X1='1'|~'>='(X1,'1')),inference(spm,[status(thm)],[32,384,theory(equality)])).
% cnf(744,plain,('+'(X1,'==>'(X1,'1'))='1'),inference(spm,[status(thm)],[395,102,theory(equality)])).
% cnf(758,plain,('>='('+'('==>'('==>'(X1,'1'),X1),'0'),X1)),inference(spm,[status(thm)],[102,17,theory(equality)])).
% cnf(770,plain,('>='('==>'('==>'(X1,'1'),X1),X1)),inference(rw,[status(thm)],[758,49,theory(equality)])).
% cnf(778,plain,('+'('1',X2)='+'(X1,'+'('==>'(X1,'1'),X2))),inference(spm,[status(thm)],[34,744,theory(equality)])).
% cnf(779,plain,('>='(X1,'==>'('==>'(X1,'1'),X2))|~'>='('1',X2)),inference(spm,[status(thm)],[94,744,theory(equality)])).
% cnf(797,plain,('1'='+'(X1,'+'('==>'(X1,'1'),X2))),inference(rw,[status(thm)],[778,74,theory(equality)])).
% cnf(798,plain,('>='(X1,'==>'('==>'(X1,'1'),X2))|$false),inference(rw,[status(thm)],[779,384,theory(equality)])).
% cnf(799,plain,('>='(X1,'==>'('==>'(X1,'1'),X2))),inference(cn,[status(thm)],[798,theory(equality)])).
% cnf(922,plain,(X1='==>'('==>'(X1,'1'),X1)|~'>='(X1,'==>'('==>'(X1,'1'),X1))),inference(spm,[status(thm)],[32,770,theory(equality)])).
% cnf(938,plain,(X1='==>'('==>'(X1,'1'),X1)|$false),inference(rw,[status(thm)],[922,379,theory(equality)])).
% cnf(939,plain,(X1='==>'('==>'(X1,'1'),X1)),inference(cn,[status(thm)],[938,theory(equality)])).
% cnf(2603,plain,('>='('==>'('==>'(X1,'1'),'+'(X1,X2)),X1)),inference(spm,[status(thm)],[377,939,theory(equality)])).
% cnf(8703,plain,(X1='==>'('==>'(X1,'1'),'+'(X1,X2))|~'>='(X1,'==>'('==>'(X1,'1'),'+'(X1,X2)))),inference(spm,[status(thm)],[32,2603,theory(equality)])).
% cnf(8754,plain,(X1='==>'('==>'(X1,'1'),'+'(X1,X2))|$false),inference(rw,[status(thm)],[8703,799,theory(equality)])).
% cnf(8755,plain,(X1='==>'('==>'(X1,'1'),'+'(X1,X2))),inference(cn,[status(thm)],[8754,theory(equality)])).
% cnf(8831,plain,('==>'('==>'(X1,'1'),'1')=X1),inference(spm,[status(thm)],[8755,797,theory(equality)])).
% cnf(9079,negated_conjecture,($false),inference(rw,[status(thm)],[60,8831,theory(equality)])).
% cnf(9080,negated_conjecture,($false),inference(cn,[status(thm)],[9079,theory(equality)])).
% cnf(9081,negated_conjecture,($false),9080,['proof']).
% # SZS output end CNFRefutation
% PrfWatch: 0.20 CPU 0.31 WC
% FINAL PrfWatch: 0.20 CPU 0.31 WC
% SZS output end Solution for /tmp/SystemOnTPTP3439/LCL902+1.tptp
%
%------------------------------------------------------------------------------