%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SEU255+1 : TPTP v5.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art02.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 02:31:42 EST 2010
% Result : Theorem 1.03s
% Output : Solution 1.03s
% 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/SystemOnTPTP10244/SEU255+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP10244/SEU255+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP10244/SEU255+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 10340
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.014 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:![X2]:(relation(X1)=>relation(relation_restriction(X1,X2))),file('/tmp/SRASS.s.p', dt_k2_wellord1)).
% fof(3, axiom,![X1]:![X2]:![X3]:(relation(X3)=>(in(X1,relation_restriction(X3,X2))<=>(in(X1,X3)&in(X1,cartesian_product2(X2,X2))))),file('/tmp/SRASS.s.p', t16_wellord1)).
% fof(5, axiom,![X1]:(relation(X1)=>(antisymmetric(X1)<=>![X2]:![X3]:((in(ordered_pair(X2,X3),X1)&in(ordered_pair(X3,X2),X1))=>X2=X3))),file('/tmp/SRASS.s.p', l3_wellord1)).
% fof(20, axiom,![X1]:![X2]:ordered_pair(X1,X2)=unordered_pair(unordered_pair(X1,X2),singleton(X1)),file('/tmp/SRASS.s.p', d5_tarski)).
% fof(22, axiom,![X1]:![X2]:unordered_pair(X1,X2)=unordered_pair(X2,X1),file('/tmp/SRASS.s.p', commutativity_k2_tarski)).
% fof(33, conjecture,![X1]:![X2]:(relation(X2)=>(antisymmetric(X2)=>antisymmetric(relation_restriction(X2,X1)))),file('/tmp/SRASS.s.p', t25_wellord1)).
% fof(34, negated_conjecture,~(![X1]:![X2]:(relation(X2)=>(antisymmetric(X2)=>antisymmetric(relation_restriction(X2,X1))))),inference(assume_negation,[status(cth)],[33])).
% fof(38, plain,![X1]:![X2]:(~(relation(X1))|relation(relation_restriction(X1,X2))),inference(fof_nnf,[status(thm)],[1])).
% fof(39, plain,![X3]:![X4]:(~(relation(X3))|relation(relation_restriction(X3,X4))),inference(variable_rename,[status(thm)],[38])).
% cnf(40,plain,(relation(relation_restriction(X1,X2))|~relation(X1)),inference(split_conjunct,[status(thm)],[39])).
% fof(44, plain,![X1]:![X2]:![X3]:(~(relation(X3))|((~(in(X1,relation_restriction(X3,X2)))|(in(X1,X3)&in(X1,cartesian_product2(X2,X2))))&((~(in(X1,X3))|~(in(X1,cartesian_product2(X2,X2))))|in(X1,relation_restriction(X3,X2))))),inference(fof_nnf,[status(thm)],[3])).
% fof(45, plain,![X4]:![X5]:![X6]:(~(relation(X6))|((~(in(X4,relation_restriction(X6,X5)))|(in(X4,X6)&in(X4,cartesian_product2(X5,X5))))&((~(in(X4,X6))|~(in(X4,cartesian_product2(X5,X5))))|in(X4,relation_restriction(X6,X5))))),inference(variable_rename,[status(thm)],[44])).
% fof(46, plain,![X4]:![X5]:![X6]:((((in(X4,X6)|~(in(X4,relation_restriction(X6,X5))))|~(relation(X6)))&((in(X4,cartesian_product2(X5,X5))|~(in(X4,relation_restriction(X6,X5))))|~(relation(X6))))&(((~(in(X4,X6))|~(in(X4,cartesian_product2(X5,X5))))|in(X4,relation_restriction(X6,X5)))|~(relation(X6)))),inference(distribute,[status(thm)],[45])).
% cnf(49,plain,(in(X2,X1)|~relation(X1)|~in(X2,relation_restriction(X1,X3))),inference(split_conjunct,[status(thm)],[46])).
% fof(54, plain,![X1]:(~(relation(X1))|((~(antisymmetric(X1))|![X2]:![X3]:((~(in(ordered_pair(X2,X3),X1))|~(in(ordered_pair(X3,X2),X1)))|X2=X3))&(?[X2]:?[X3]:((in(ordered_pair(X2,X3),X1)&in(ordered_pair(X3,X2),X1))&~(X2=X3))|antisymmetric(X1)))),inference(fof_nnf,[status(thm)],[5])).
% fof(55, plain,![X4]:(~(relation(X4))|((~(antisymmetric(X4))|![X5]:![X6]:((~(in(ordered_pair(X5,X6),X4))|~(in(ordered_pair(X6,X5),X4)))|X5=X6))&(?[X7]:?[X8]:((in(ordered_pair(X7,X8),X4)&in(ordered_pair(X8,X7),X4))&~(X7=X8))|antisymmetric(X4)))),inference(variable_rename,[status(thm)],[54])).
% fof(56, plain,![X4]:(~(relation(X4))|((~(antisymmetric(X4))|![X5]:![X6]:((~(in(ordered_pair(X5,X6),X4))|~(in(ordered_pair(X6,X5),X4)))|X5=X6))&(((in(ordered_pair(esk2_1(X4),esk3_1(X4)),X4)&in(ordered_pair(esk3_1(X4),esk2_1(X4)),X4))&~(esk2_1(X4)=esk3_1(X4)))|antisymmetric(X4)))),inference(skolemize,[status(esa)],[55])).
% fof(57, plain,![X4]:![X5]:![X6]:(((((~(in(ordered_pair(X5,X6),X4))|~(in(ordered_pair(X6,X5),X4)))|X5=X6)|~(antisymmetric(X4)))&(((in(ordered_pair(esk2_1(X4),esk3_1(X4)),X4)&in(ordered_pair(esk3_1(X4),esk2_1(X4)),X4))&~(esk2_1(X4)=esk3_1(X4)))|antisymmetric(X4)))|~(relation(X4))),inference(shift_quantors,[status(thm)],[56])).
% fof(58, plain,![X4]:![X5]:![X6]:(((((~(in(ordered_pair(X5,X6),X4))|~(in(ordered_pair(X6,X5),X4)))|X5=X6)|~(antisymmetric(X4)))|~(relation(X4)))&((((in(ordered_pair(esk2_1(X4),esk3_1(X4)),X4)|antisymmetric(X4))|~(relation(X4)))&((in(ordered_pair(esk3_1(X4),esk2_1(X4)),X4)|antisymmetric(X4))|~(relation(X4))))&((~(esk2_1(X4)=esk3_1(X4))|antisymmetric(X4))|~(relation(X4))))),inference(distribute,[status(thm)],[57])).
% cnf(59,plain,(antisymmetric(X1)|~relation(X1)|esk2_1(X1)!=esk3_1(X1)),inference(split_conjunct,[status(thm)],[58])).
% cnf(60,plain,(antisymmetric(X1)|in(ordered_pair(esk3_1(X1),esk2_1(X1)),X1)|~relation(X1)),inference(split_conjunct,[status(thm)],[58])).
% cnf(61,plain,(antisymmetric(X1)|in(ordered_pair(esk2_1(X1),esk3_1(X1)),X1)|~relation(X1)),inference(split_conjunct,[status(thm)],[58])).
% cnf(62,plain,(X2=X3|~relation(X1)|~antisymmetric(X1)|~in(ordered_pair(X3,X2),X1)|~in(ordered_pair(X2,X3),X1)),inference(split_conjunct,[status(thm)],[58])).
% fof(110, plain,![X3]:![X4]:ordered_pair(X3,X4)=unordered_pair(unordered_pair(X3,X4),singleton(X3)),inference(variable_rename,[status(thm)],[20])).
% cnf(111,plain,(ordered_pair(X1,X2)=unordered_pair(unordered_pair(X1,X2),singleton(X1))),inference(split_conjunct,[status(thm)],[110])).
% fof(114, plain,![X3]:![X4]:unordered_pair(X3,X4)=unordered_pair(X4,X3),inference(variable_rename,[status(thm)],[22])).
% cnf(115,plain,(unordered_pair(X1,X2)=unordered_pair(X2,X1)),inference(split_conjunct,[status(thm)],[114])).
% fof(130, negated_conjecture,?[X1]:?[X2]:(relation(X2)&(antisymmetric(X2)&~(antisymmetric(relation_restriction(X2,X1))))),inference(fof_nnf,[status(thm)],[34])).
% fof(131, negated_conjecture,?[X3]:?[X4]:(relation(X4)&(antisymmetric(X4)&~(antisymmetric(relation_restriction(X4,X3))))),inference(variable_rename,[status(thm)],[130])).
% fof(132, negated_conjecture,(relation(esk10_0)&(antisymmetric(esk10_0)&~(antisymmetric(relation_restriction(esk10_0,esk9_0))))),inference(skolemize,[status(esa)],[131])).
% cnf(133,negated_conjecture,(~antisymmetric(relation_restriction(esk10_0,esk9_0))),inference(split_conjunct,[status(thm)],[132])).
% cnf(134,negated_conjecture,(antisymmetric(esk10_0)),inference(split_conjunct,[status(thm)],[132])).
% cnf(135,negated_conjecture,(relation(esk10_0)),inference(split_conjunct,[status(thm)],[132])).
% cnf(136,plain,(antisymmetric(X1)|in(unordered_pair(unordered_pair(esk2_1(X1),esk3_1(X1)),singleton(esk2_1(X1))),X1)|~relation(X1)),inference(rw,[status(thm)],[61,111,theory(equality)]),['unfolding']).
% cnf(137,plain,(antisymmetric(X1)|in(unordered_pair(unordered_pair(esk3_1(X1),esk2_1(X1)),singleton(esk3_1(X1))),X1)|~relation(X1)),inference(rw,[status(thm)],[60,111,theory(equality)]),['unfolding']).
% cnf(138,plain,(X2=X3|~relation(X1)|~antisymmetric(X1)|~in(unordered_pair(unordered_pair(X3,X2),singleton(X3)),X1)|~in(unordered_pair(unordered_pair(X2,X3),singleton(X2)),X1)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[62,111,theory(equality)]),111,theory(equality)]),['unfolding']).
% cnf(163,plain,(X1=X2|~antisymmetric(X3)|~in(unordered_pair(singleton(X2),unordered_pair(X2,X1)),X3)|~in(unordered_pair(unordered_pair(X1,X2),singleton(X1)),X3)|~relation(X3)),inference(spm,[status(thm)],[138,115,theory(equality)])).
% cnf(165,plain,(antisymmetric(X1)|in(unordered_pair(singleton(esk2_1(X1)),unordered_pair(esk2_1(X1),esk3_1(X1))),X1)|~relation(X1)),inference(rw,[status(thm)],[136,115,theory(equality)])).
% cnf(167,plain,(in(unordered_pair(singleton(esk2_1(relation_restriction(X1,X2))),unordered_pair(esk2_1(relation_restriction(X1,X2)),esk3_1(relation_restriction(X1,X2)))),X1)|antisymmetric(relation_restriction(X1,X2))|~relation(X1)|~relation(relation_restriction(X1,X2))),inference(spm,[status(thm)],[49,165,theory(equality)])).
% cnf(171,plain,(antisymmetric(X1)|in(unordered_pair(singleton(esk3_1(X1)),unordered_pair(esk2_1(X1),esk3_1(X1))),X1)|~relation(X1)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[137,115,theory(equality)]),115,theory(equality)])).
% cnf(173,plain,(in(unordered_pair(singleton(esk3_1(relation_restriction(X1,X2))),unordered_pair(esk2_1(relation_restriction(X1,X2)),esk3_1(relation_restriction(X1,X2)))),X1)|antisymmetric(relation_restriction(X1,X2))|~relation(X1)|~relation(relation_restriction(X1,X2))),inference(spm,[status(thm)],[49,171,theory(equality)])).
% cnf(345,plain,(antisymmetric(relation_restriction(X1,X2))|in(unordered_pair(singleton(esk2_1(relation_restriction(X1,X2))),unordered_pair(esk2_1(relation_restriction(X1,X2)),esk3_1(relation_restriction(X1,X2)))),X1)|~relation(X1)),inference(csr,[status(thm)],[167,40])).
% cnf(353,plain,(esk3_1(relation_restriction(X1,X2))=esk2_1(relation_restriction(X1,X2))|antisymmetric(relation_restriction(X1,X2))|~antisymmetric(X1)|~in(unordered_pair(unordered_pair(esk3_1(relation_restriction(X1,X2)),esk2_1(relation_restriction(X1,X2))),singleton(esk3_1(relation_restriction(X1,X2)))),X1)|~relation(X1)),inference(spm,[status(thm)],[163,345,theory(equality)])).
% cnf(539,plain,(antisymmetric(relation_restriction(X1,X2))|in(unordered_pair(singleton(esk3_1(relation_restriction(X1,X2))),unordered_pair(esk2_1(relation_restriction(X1,X2)),esk3_1(relation_restriction(X1,X2)))),X1)|~relation(X1)),inference(csr,[status(thm)],[173,40])).
% cnf(2923,plain,(esk3_1(relation_restriction(X1,X2))=esk2_1(relation_restriction(X1,X2))|antisymmetric(relation_restriction(X1,X2))|~antisymmetric(X1)|~in(unordered_pair(singleton(esk3_1(relation_restriction(X1,X2))),unordered_pair(esk2_1(relation_restriction(X1,X2)),esk3_1(relation_restriction(X1,X2)))),X1)|~relation(X1)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[353,115,theory(equality)]),115,theory(equality)])).
% cnf(2924,plain,(esk3_1(relation_restriction(X1,X2))=esk2_1(relation_restriction(X1,X2))|antisymmetric(relation_restriction(X1,X2))|~antisymmetric(X1)|~relation(X1)),inference(csr,[status(thm)],[2923,539])).
% cnf(2925,plain,(antisymmetric(relation_restriction(X1,X2))|~relation(relation_restriction(X1,X2))|~antisymmetric(X1)|~relation(X1)),inference(spm,[status(thm)],[59,2924,theory(equality)])).
% cnf(2962,plain,(antisymmetric(relation_restriction(X1,X2))|~antisymmetric(X1)|~relation(X1)),inference(csr,[status(thm)],[2925,40])).
% cnf(2963,negated_conjecture,(~antisymmetric(esk10_0)|~relation(esk10_0)),inference(spm,[status(thm)],[133,2962,theory(equality)])).
% cnf(2980,negated_conjecture,($false|~relation(esk10_0)),inference(rw,[status(thm)],[2963,134,theory(equality)])).
% cnf(2981,negated_conjecture,($false|$false),inference(rw,[status(thm)],[2980,135,theory(equality)])).
% cnf(2982,negated_conjecture,($false),inference(cn,[status(thm)],[2981,theory(equality)])).
% cnf(2983,negated_conjecture,($false),2982,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 397
% # ...of these trivial : 3
% # ...subsumed : 253
% # ...remaining for further processing: 141
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 4
% # Backward-rewritten : 6
% # Generated clauses : 1833
% # ...of the previous two non-trivial : 1485
% # Contextual simplify-reflections : 305
% # Paramodulations : 1819
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 125
% # Positive orientable unit clauses: 19
% # Positive unorientable unit clauses: 2
% # Negative unit clauses : 13
% # Non-unit-clauses : 91
% # Current number of unprocessed clauses: 1095
% # ...number of literals in the above : 6819
% # Clause-clause subsumption calls (NU) : 5948
% # Rec. Clause-clause subsumption calls : 3116
% # Unit Clause-clause subsumption calls : 438
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 6
% # Indexed BW rewrite successes : 6
% # Backwards rewriting index: 117 leaves, 1.79+/-1.517 terms/leaf
% # Paramod-from index: 46 leaves, 1.54+/-0.949 terms/leaf
% # Paramod-into index: 108 leaves, 1.66+/-1.328 terms/leaf
% # -------------------------------------------------
% # User time : 0.092 s
% # System time : 0.005 s
% # Total time : 0.097 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.21 CPU 0.30 WC
% FINAL PrfWatch: 0.21 CPU 0.30 WC
% SZS output end Solution for /tmp/SystemOnTPTP10244/SEU255+1.tptp
%
%------------------------------------------------------------------------------