%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SET794+4 : TPTP v5.0.0. Released v3.2.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 : Thu Dec 30 00:08:08 EST 2010
% Result : Theorem 0.93s
% Output : Solution 0.93s
% 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/SystemOnTPTP29473/SET794+4.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP29473/SET794+4.tptp
% SZS output start Solution for /tmp/SystemOnTPTP29473/SET794+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 29569
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% # Preprocessing time : 0.020 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:![X2]:![X3]:(least(X3,X1,X2)<=>(member(X3,X2)&![X4]:(member(X4,X2)=>apply(X1,X3,X4)))),file('/tmp/SRASS.s.p', least)).
% fof(2, axiom,![X1]:![X2]:![X3]:(min(X3,X1,X2)<=>(member(X3,X2)&![X4]:((member(X4,X2)&apply(X1,X4,X3))=>X3=X4))),file('/tmp/SRASS.s.p', min)).
% fof(3, axiom,![X1]:![X2]:(total_order(X1,X2)<=>(order(X1,X2)&![X4]:![X5]:((member(X4,X2)&member(X5,X2))=>(apply(X1,X4,X5)|apply(X1,X5,X4))))),file('/tmp/SRASS.s.p', total_order)).
% fof(11, conjecture,![X1]:![X2]:![X3]:((total_order(X1,X2)&min(X3,X1,X2))=>least(X3,X1,X2)),file('/tmp/SRASS.s.p', thIV6)).
% fof(12, negated_conjecture,~(![X1]:![X2]:![X3]:((total_order(X1,X2)&min(X3,X1,X2))=>least(X3,X1,X2))),inference(assume_negation,[status(cth)],[11])).
% fof(15, plain,![X1]:![X2]:![X3]:((~(least(X3,X1,X2))|(member(X3,X2)&![X4]:(~(member(X4,X2))|apply(X1,X3,X4))))&((~(member(X3,X2))|?[X4]:(member(X4,X2)&~(apply(X1,X3,X4))))|least(X3,X1,X2))),inference(fof_nnf,[status(thm)],[1])).
% fof(16, plain,![X5]:![X6]:![X7]:((~(least(X7,X5,X6))|(member(X7,X6)&![X8]:(~(member(X8,X6))|apply(X5,X7,X8))))&((~(member(X7,X6))|?[X9]:(member(X9,X6)&~(apply(X5,X7,X9))))|least(X7,X5,X6))),inference(variable_rename,[status(thm)],[15])).
% fof(17, plain,![X5]:![X6]:![X7]:((~(least(X7,X5,X6))|(member(X7,X6)&![X8]:(~(member(X8,X6))|apply(X5,X7,X8))))&((~(member(X7,X6))|(member(esk1_3(X5,X6,X7),X6)&~(apply(X5,X7,esk1_3(X5,X6,X7)))))|least(X7,X5,X6))),inference(skolemize,[status(esa)],[16])).
% fof(18, plain,![X5]:![X6]:![X7]:![X8]:((((~(member(X8,X6))|apply(X5,X7,X8))&member(X7,X6))|~(least(X7,X5,X6)))&((~(member(X7,X6))|(member(esk1_3(X5,X6,X7),X6)&~(apply(X5,X7,esk1_3(X5,X6,X7)))))|least(X7,X5,X6))),inference(shift_quantors,[status(thm)],[17])).
% fof(19, plain,![X5]:![X6]:![X7]:![X8]:((((~(member(X8,X6))|apply(X5,X7,X8))|~(least(X7,X5,X6)))&(member(X7,X6)|~(least(X7,X5,X6))))&(((member(esk1_3(X5,X6,X7),X6)|~(member(X7,X6)))|least(X7,X5,X6))&((~(apply(X5,X7,esk1_3(X5,X6,X7)))|~(member(X7,X6)))|least(X7,X5,X6)))),inference(distribute,[status(thm)],[18])).
% cnf(20,plain,(least(X1,X2,X3)|~member(X1,X3)|~apply(X2,X1,esk1_3(X2,X3,X1))),inference(split_conjunct,[status(thm)],[19])).
% cnf(21,plain,(least(X1,X2,X3)|member(esk1_3(X2,X3,X1),X3)|~member(X1,X3)),inference(split_conjunct,[status(thm)],[19])).
% fof(24, plain,![X1]:![X2]:![X3]:((~(min(X3,X1,X2))|(member(X3,X2)&![X4]:((~(member(X4,X2))|~(apply(X1,X4,X3)))|X3=X4)))&((~(member(X3,X2))|?[X4]:((member(X4,X2)&apply(X1,X4,X3))&~(X3=X4)))|min(X3,X1,X2))),inference(fof_nnf,[status(thm)],[2])).
% fof(25, plain,![X5]:![X6]:![X7]:((~(min(X7,X5,X6))|(member(X7,X6)&![X8]:((~(member(X8,X6))|~(apply(X5,X8,X7)))|X7=X8)))&((~(member(X7,X6))|?[X9]:((member(X9,X6)&apply(X5,X9,X7))&~(X7=X9)))|min(X7,X5,X6))),inference(variable_rename,[status(thm)],[24])).
% fof(26, plain,![X5]:![X6]:![X7]:((~(min(X7,X5,X6))|(member(X7,X6)&![X8]:((~(member(X8,X6))|~(apply(X5,X8,X7)))|X7=X8)))&((~(member(X7,X6))|((member(esk2_3(X5,X6,X7),X6)&apply(X5,esk2_3(X5,X6,X7),X7))&~(X7=esk2_3(X5,X6,X7))))|min(X7,X5,X6))),inference(skolemize,[status(esa)],[25])).
% fof(27, plain,![X5]:![X6]:![X7]:![X8]:(((((~(member(X8,X6))|~(apply(X5,X8,X7)))|X7=X8)&member(X7,X6))|~(min(X7,X5,X6)))&((~(member(X7,X6))|((member(esk2_3(X5,X6,X7),X6)&apply(X5,esk2_3(X5,X6,X7),X7))&~(X7=esk2_3(X5,X6,X7))))|min(X7,X5,X6))),inference(shift_quantors,[status(thm)],[26])).
% fof(28, plain,![X5]:![X6]:![X7]:![X8]:(((((~(member(X8,X6))|~(apply(X5,X8,X7)))|X7=X8)|~(min(X7,X5,X6)))&(member(X7,X6)|~(min(X7,X5,X6))))&((((member(esk2_3(X5,X6,X7),X6)|~(member(X7,X6)))|min(X7,X5,X6))&((apply(X5,esk2_3(X5,X6,X7),X7)|~(member(X7,X6)))|min(X7,X5,X6)))&((~(X7=esk2_3(X5,X6,X7))|~(member(X7,X6)))|min(X7,X5,X6)))),inference(distribute,[status(thm)],[27])).
% cnf(32,plain,(member(X1,X3)|~min(X1,X2,X3)),inference(split_conjunct,[status(thm)],[28])).
% cnf(33,plain,(X1=X4|~min(X1,X2,X3)|~apply(X2,X4,X1)|~member(X4,X3)),inference(split_conjunct,[status(thm)],[28])).
% fof(34, plain,![X1]:![X2]:((~(total_order(X1,X2))|(order(X1,X2)&![X4]:![X5]:((~(member(X4,X2))|~(member(X5,X2)))|(apply(X1,X4,X5)|apply(X1,X5,X4)))))&((~(order(X1,X2))|?[X4]:?[X5]:((member(X4,X2)&member(X5,X2))&(~(apply(X1,X4,X5))&~(apply(X1,X5,X4)))))|total_order(X1,X2))),inference(fof_nnf,[status(thm)],[3])).
% fof(35, plain,![X6]:![X7]:((~(total_order(X6,X7))|(order(X6,X7)&![X8]:![X9]:((~(member(X8,X7))|~(member(X9,X7)))|(apply(X6,X8,X9)|apply(X6,X9,X8)))))&((~(order(X6,X7))|?[X10]:?[X11]:((member(X10,X7)&member(X11,X7))&(~(apply(X6,X10,X11))&~(apply(X6,X11,X10)))))|total_order(X6,X7))),inference(variable_rename,[status(thm)],[34])).
% fof(36, plain,![X6]:![X7]:((~(total_order(X6,X7))|(order(X6,X7)&![X8]:![X9]:((~(member(X8,X7))|~(member(X9,X7)))|(apply(X6,X8,X9)|apply(X6,X9,X8)))))&((~(order(X6,X7))|((member(esk3_2(X6,X7),X7)&member(esk4_2(X6,X7),X7))&(~(apply(X6,esk3_2(X6,X7),esk4_2(X6,X7)))&~(apply(X6,esk4_2(X6,X7),esk3_2(X6,X7))))))|total_order(X6,X7))),inference(skolemize,[status(esa)],[35])).
% fof(37, plain,![X6]:![X7]:![X8]:![X9]:(((((~(member(X8,X7))|~(member(X9,X7)))|(apply(X6,X8,X9)|apply(X6,X9,X8)))&order(X6,X7))|~(total_order(X6,X7)))&((~(order(X6,X7))|((member(esk3_2(X6,X7),X7)&member(esk4_2(X6,X7),X7))&(~(apply(X6,esk3_2(X6,X7),esk4_2(X6,X7)))&~(apply(X6,esk4_2(X6,X7),esk3_2(X6,X7))))))|total_order(X6,X7))),inference(shift_quantors,[status(thm)],[36])).
% fof(38, plain,![X6]:![X7]:![X8]:![X9]:(((((~(member(X8,X7))|~(member(X9,X7)))|(apply(X6,X8,X9)|apply(X6,X9,X8)))|~(total_order(X6,X7)))&(order(X6,X7)|~(total_order(X6,X7))))&((((member(esk3_2(X6,X7),X7)|~(order(X6,X7)))|total_order(X6,X7))&((member(esk4_2(X6,X7),X7)|~(order(X6,X7)))|total_order(X6,X7)))&(((~(apply(X6,esk3_2(X6,X7),esk4_2(X6,X7)))|~(order(X6,X7)))|total_order(X6,X7))&((~(apply(X6,esk4_2(X6,X7),esk3_2(X6,X7)))|~(order(X6,X7)))|total_order(X6,X7))))),inference(distribute,[status(thm)],[37])).
% cnf(44,plain,(apply(X1,X3,X4)|apply(X1,X4,X3)|~total_order(X1,X2)|~member(X3,X2)|~member(X4,X2)),inference(split_conjunct,[status(thm)],[38])).
% fof(106, negated_conjecture,?[X1]:?[X2]:?[X3]:((total_order(X1,X2)&min(X3,X1,X2))&~(least(X3,X1,X2))),inference(fof_nnf,[status(thm)],[12])).
% fof(107, negated_conjecture,?[X4]:?[X5]:?[X6]:((total_order(X4,X5)&min(X6,X4,X5))&~(least(X6,X4,X5))),inference(variable_rename,[status(thm)],[106])).
% fof(108, negated_conjecture,((total_order(esk11_0,esk12_0)&min(esk13_0,esk11_0,esk12_0))&~(least(esk13_0,esk11_0,esk12_0))),inference(skolemize,[status(esa)],[107])).
% cnf(109,negated_conjecture,(~least(esk13_0,esk11_0,esk12_0)),inference(split_conjunct,[status(thm)],[108])).
% cnf(110,negated_conjecture,(min(esk13_0,esk11_0,esk12_0)),inference(split_conjunct,[status(thm)],[108])).
% cnf(111,negated_conjecture,(total_order(esk11_0,esk12_0)),inference(split_conjunct,[status(thm)],[108])).
% cnf(181,negated_conjecture,(member(esk13_0,esk12_0)),inference(spm,[status(thm)],[32,110,theory(equality)])).
% cnf(183,negated_conjecture,(esk13_0=X1|~apply(esk11_0,X1,esk13_0)|~member(X1,esk12_0)),inference(spm,[status(thm)],[33,110,theory(equality)])).
% cnf(184,negated_conjecture,(apply(esk11_0,X1,X2)|apply(esk11_0,X2,X1)|~member(X1,esk12_0)|~member(X2,esk12_0)),inference(spm,[status(thm)],[44,111,theory(equality)])).
% cnf(277,negated_conjecture,(apply(esk11_0,X1,esk13_0)|apply(esk11_0,esk13_0,X1)|~member(X1,esk12_0)),inference(spm,[status(thm)],[184,181,theory(equality)])).
% cnf(297,negated_conjecture,(apply(esk11_0,esk13_0,esk13_0)),inference(spm,[status(thm)],[277,181,theory(equality)])).
% cnf(307,negated_conjecture,(apply(esk11_0,esk13_0,esk1_3(X1,esk12_0,X2))|apply(esk11_0,esk1_3(X1,esk12_0,X2),esk13_0)|least(X2,X1,esk12_0)|~member(X2,esk12_0)),inference(spm,[status(thm)],[277,21,theory(equality)])).
% cnf(339,negated_conjecture,(esk13_0=esk1_3(X1,esk12_0,X2)|apply(esk11_0,esk13_0,esk1_3(X1,esk12_0,X2))|least(X2,X1,esk12_0)|~member(esk1_3(X1,esk12_0,X2),esk12_0)|~member(X2,esk12_0)),inference(spm,[status(thm)],[183,307,theory(equality)])).
% cnf(362,negated_conjecture,(esk1_3(X1,esk12_0,X2)=esk13_0|apply(esk11_0,esk13_0,esk1_3(X1,esk12_0,X2))|least(X2,X1,esk12_0)|~member(X2,esk12_0)),inference(csr,[status(thm)],[339,21])).
% cnf(363,negated_conjecture,(least(esk13_0,esk11_0,esk12_0)|esk1_3(esk11_0,esk12_0,esk13_0)=esk13_0|~member(esk13_0,esk12_0)),inference(spm,[status(thm)],[20,362,theory(equality)])).
% cnf(366,negated_conjecture,(least(esk13_0,esk11_0,esk12_0)|esk1_3(esk11_0,esk12_0,esk13_0)=esk13_0|$false),inference(rw,[status(thm)],[363,181,theory(equality)])).
% cnf(367,negated_conjecture,(least(esk13_0,esk11_0,esk12_0)|esk1_3(esk11_0,esk12_0,esk13_0)=esk13_0),inference(cn,[status(thm)],[366,theory(equality)])).
% cnf(368,negated_conjecture,(esk1_3(esk11_0,esk12_0,esk13_0)=esk13_0),inference(sr,[status(thm)],[367,109,theory(equality)])).
% cnf(369,negated_conjecture,(least(esk13_0,esk11_0,esk12_0)|~apply(esk11_0,esk13_0,esk13_0)|~member(esk13_0,esk12_0)),inference(spm,[status(thm)],[20,368,theory(equality)])).
% cnf(372,negated_conjecture,(least(esk13_0,esk11_0,esk12_0)|$false|~member(esk13_0,esk12_0)),inference(rw,[status(thm)],[369,297,theory(equality)])).
% cnf(373,negated_conjecture,(least(esk13_0,esk11_0,esk12_0)|$false|$false),inference(rw,[status(thm)],[372,181,theory(equality)])).
% cnf(374,negated_conjecture,(least(esk13_0,esk11_0,esk12_0)),inference(cn,[status(thm)],[373,theory(equality)])).
% cnf(375,negated_conjecture,($false),inference(sr,[status(thm)],[374,109,theory(equality)])).
% cnf(376,negated_conjecture,($false),375,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 246
% # ...of these trivial : 0
% # ...subsumed : 0
% # ...remaining for further processing: 246
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 0
% # Backward-rewritten : 0
% # Generated clauses : 170
% # ...of the previous two non-trivial : 150
% # Contextual simplify-reflections : 7
% # Paramodulations : 170
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 136
% # Positive orientable unit clauses: 7
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 1
% # Non-unit-clauses : 128
% # Current number of unprocessed clauses: 124
% # ...number of literals in the above : 898
% # Clause-clause subsumption calls (NU) : 330
% # Rec. Clause-clause subsumption calls : 153
% # Unit Clause-clause subsumption calls : 15
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 1
% # Indexed BW rewrite successes : 0
% # Backwards rewriting index: 102 leaves, 1.65+/-1.824 terms/leaf
% # Paramod-from index: 38 leaves, 1.13+/-0.800 terms/leaf
% # Paramod-into index: 87 leaves, 1.29+/-0.909 terms/leaf
% # -------------------------------------------------
% # User time : 0.046 s
% # System time : 0.003 s
% # Total time : 0.049 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.14 CPU 0.22 WC
% FINAL PrfWatch: 0.14 CPU 0.22 WC
% SZS output end Solution for /tmp/SystemOnTPTP29473/SET794+4.tptp
%
%------------------------------------------------------------------------------