%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SEU224+2 : TPTP v5.0.0. Released v3.3.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 : 2006MB
% OS : Linux 2.6.31.5-127.fc12.i686.PAE
% CPULimit : 300s
% DateTime : Thu Dec 30 02:06:44 EST 2010
% Result : Theorem 3.36s
% Output : Solution 3.36s
% 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/SystemOnTPTP1817/SEU224+2.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP1817/SEU224+2.tptp
% SZS output start Solution for /tmp/SystemOnTPTP1817/SEU224+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 1949
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Preprocessing time : 0.050 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(5, axiom,![X1]:![X2]:![X3]:(relation(X3)=>(in(X1,relation_dom(relation_dom_restriction(X3,X2)))<=>(in(X1,X2)&in(X1,relation_dom(X3))))),file('/tmp/SRASS.s.p', t86_relat_1)).
% fof(239, conjecture,![X1]:![X2]:![X3]:((relation(X3)&function(X3))=>(in(X2,relation_dom(relation_dom_restriction(X3,X1)))<=>(in(X2,relation_dom(X3))&in(X2,X1)))),file('/tmp/SRASS.s.p', l82_funct_1)).
% fof(240, negated_conjecture,~(![X1]:![X2]:![X3]:((relation(X3)&function(X3))=>(in(X2,relation_dom(relation_dom_restriction(X3,X1)))<=>(in(X2,relation_dom(X3))&in(X2,X1))))),inference(assume_negation,[status(cth)],[239])).
% fof(283, plain,![X1]:![X2]:![X3]:(~(relation(X3))|((~(in(X1,relation_dom(relation_dom_restriction(X3,X2))))|(in(X1,X2)&in(X1,relation_dom(X3))))&((~(in(X1,X2))|~(in(X1,relation_dom(X3))))|in(X1,relation_dom(relation_dom_restriction(X3,X2)))))),inference(fof_nnf,[status(thm)],[5])).
% fof(284, plain,![X4]:![X5]:![X6]:(~(relation(X6))|((~(in(X4,relation_dom(relation_dom_restriction(X6,X5))))|(in(X4,X5)&in(X4,relation_dom(X6))))&((~(in(X4,X5))|~(in(X4,relation_dom(X6))))|in(X4,relation_dom(relation_dom_restriction(X6,X5)))))),inference(variable_rename,[status(thm)],[283])).
% fof(285, plain,![X4]:![X5]:![X6]:((((in(X4,X5)|~(in(X4,relation_dom(relation_dom_restriction(X6,X5)))))|~(relation(X6)))&((in(X4,relation_dom(X6))|~(in(X4,relation_dom(relation_dom_restriction(X6,X5)))))|~(relation(X6))))&(((~(in(X4,X5))|~(in(X4,relation_dom(X6))))|in(X4,relation_dom(relation_dom_restriction(X6,X5))))|~(relation(X6)))),inference(distribute,[status(thm)],[284])).
% cnf(286,plain,(in(X2,relation_dom(relation_dom_restriction(X1,X3)))|~relation(X1)|~in(X2,relation_dom(X1))|~in(X2,X3)),inference(split_conjunct,[status(thm)],[285])).
% cnf(287,plain,(in(X2,relation_dom(X1))|~relation(X1)|~in(X2,relation_dom(relation_dom_restriction(X1,X3)))),inference(split_conjunct,[status(thm)],[285])).
% cnf(288,plain,(in(X2,X3)|~relation(X1)|~in(X2,relation_dom(relation_dom_restriction(X1,X3)))),inference(split_conjunct,[status(thm)],[285])).
% fof(1276, negated_conjecture,?[X1]:?[X2]:?[X3]:((relation(X3)&function(X3))&((~(in(X2,relation_dom(relation_dom_restriction(X3,X1))))|(~(in(X2,relation_dom(X3)))|~(in(X2,X1))))&(in(X2,relation_dom(relation_dom_restriction(X3,X1)))|(in(X2,relation_dom(X3))&in(X2,X1))))),inference(fof_nnf,[status(thm)],[240])).
% fof(1277, negated_conjecture,?[X4]:?[X5]:?[X6]:((relation(X6)&function(X6))&((~(in(X5,relation_dom(relation_dom_restriction(X6,X4))))|(~(in(X5,relation_dom(X6)))|~(in(X5,X4))))&(in(X5,relation_dom(relation_dom_restriction(X6,X4)))|(in(X5,relation_dom(X6))&in(X5,X4))))),inference(variable_rename,[status(thm)],[1276])).
% fof(1278, negated_conjecture,((relation(esk82_0)&function(esk82_0))&((~(in(esk81_0,relation_dom(relation_dom_restriction(esk82_0,esk80_0))))|(~(in(esk81_0,relation_dom(esk82_0)))|~(in(esk81_0,esk80_0))))&(in(esk81_0,relation_dom(relation_dom_restriction(esk82_0,esk80_0)))|(in(esk81_0,relation_dom(esk82_0))&in(esk81_0,esk80_0))))),inference(skolemize,[status(esa)],[1277])).
% fof(1279, negated_conjecture,((relation(esk82_0)&function(esk82_0))&((~(in(esk81_0,relation_dom(relation_dom_restriction(esk82_0,esk80_0))))|(~(in(esk81_0,relation_dom(esk82_0)))|~(in(esk81_0,esk80_0))))&((in(esk81_0,relation_dom(esk82_0))|in(esk81_0,relation_dom(relation_dom_restriction(esk82_0,esk80_0))))&(in(esk81_0,esk80_0)|in(esk81_0,relation_dom(relation_dom_restriction(esk82_0,esk80_0))))))),inference(distribute,[status(thm)],[1278])).
% cnf(1280,negated_conjecture,(in(esk81_0,relation_dom(relation_dom_restriction(esk82_0,esk80_0)))|in(esk81_0,esk80_0)),inference(split_conjunct,[status(thm)],[1279])).
% cnf(1281,negated_conjecture,(in(esk81_0,relation_dom(relation_dom_restriction(esk82_0,esk80_0)))|in(esk81_0,relation_dom(esk82_0))),inference(split_conjunct,[status(thm)],[1279])).
% cnf(1282,negated_conjecture,(~in(esk81_0,esk80_0)|~in(esk81_0,relation_dom(esk82_0))|~in(esk81_0,relation_dom(relation_dom_restriction(esk82_0,esk80_0)))),inference(split_conjunct,[status(thm)],[1279])).
% cnf(1284,negated_conjecture,(relation(esk82_0)),inference(split_conjunct,[status(thm)],[1279])).
% cnf(1634,negated_conjecture,(in(esk81_0,esk80_0)|~relation(esk82_0)),inference(spm,[status(thm)],[288,1280,theory(equality)])).
% cnf(1637,negated_conjecture,(in(esk81_0,esk80_0)|$false),inference(rw,[status(thm)],[1634,1284,theory(equality)])).
% cnf(1638,negated_conjecture,(in(esk81_0,esk80_0)),inference(cn,[status(thm)],[1637,theory(equality)])).
% cnf(1650,negated_conjecture,(in(esk81_0,relation_dom(esk82_0))|~relation(esk82_0)),inference(spm,[status(thm)],[287,1281,theory(equality)])).
% cnf(1654,negated_conjecture,(in(esk81_0,relation_dom(esk82_0))|$false),inference(rw,[status(thm)],[1650,1284,theory(equality)])).
% cnf(1655,negated_conjecture,(in(esk81_0,relation_dom(esk82_0))),inference(cn,[status(thm)],[1654,theory(equality)])).
% cnf(7374,negated_conjecture,(~in(esk81_0,relation_dom(relation_dom_restriction(esk82_0,esk80_0)))|~in(esk81_0,relation_dom(esk82_0))|$false),inference(rw,[status(thm)],[1282,1638,theory(equality)])).
% cnf(7375,negated_conjecture,(~in(esk81_0,relation_dom(relation_dom_restriction(esk82_0,esk80_0)))|~in(esk81_0,relation_dom(esk82_0))),inference(cn,[status(thm)],[7374,theory(equality)])).
% cnf(7390,negated_conjecture,(~in(esk81_0,relation_dom(relation_dom_restriction(esk82_0,esk80_0)))|$false),inference(rw,[status(thm)],[7375,1655,theory(equality)])).
% cnf(7391,negated_conjecture,(~in(esk81_0,relation_dom(relation_dom_restriction(esk82_0,esk80_0)))),inference(cn,[status(thm)],[7390,theory(equality)])).
% cnf(7395,negated_conjecture,(~relation(esk82_0)|~in(esk81_0,relation_dom(esk82_0))|~in(esk81_0,esk80_0)),inference(spm,[status(thm)],[7391,286,theory(equality)])).
% cnf(7396,negated_conjecture,($false|~in(esk81_0,relation_dom(esk82_0))|~in(esk81_0,esk80_0)),inference(rw,[status(thm)],[7395,1284,theory(equality)])).
% cnf(7397,negated_conjecture,($false|$false|~in(esk81_0,esk80_0)),inference(rw,[status(thm)],[7396,1655,theory(equality)])).
% cnf(7398,negated_conjecture,($false|$false|$false),inference(rw,[status(thm)],[7397,1638,theory(equality)])).
% cnf(7399,negated_conjecture,($false),inference(cn,[status(thm)],[7398,theory(equality)])).
% cnf(7400,negated_conjecture,($false),7399,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 833
% # ...of these trivial : 6
% # ...subsumed : 29
% # ...remaining for further processing: 798
% # Other redundant clauses eliminated : 63
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 0
% # Backward-rewritten : 3
% # Generated clauses : 5321
% # ...of the previous two non-trivial : 5058
% # Contextual simplify-reflections : 18
% # Paramodulations : 5214
% # Factorizations : 14
% # Equation resolutions : 93
% # Current number of processed clauses: 396
% # Positive orientable unit clauses: 46
% # Positive unorientable unit clauses: 3
% # Negative unit clauses : 11
% # Non-unit-clauses : 336
% # Current number of unprocessed clauses: 5016
% # ...number of literals in the above : 25075
% # Clause-clause subsumption calls (NU) : 9348
% # Rec. Clause-clause subsumption calls : 2961
% # Unit Clause-clause subsumption calls : 94
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 66
% # Indexed BW rewrite successes : 56
% # Backwards rewriting index: 434 leaves, 1.67+/-2.965 terms/leaf
% # Paramod-from index: 185 leaves, 1.19+/-1.232 terms/leaf
% # Paramod-into index: 388 leaves, 1.48+/-2.385 terms/leaf
% # -------------------------------------------------
% # User time : 0.318 s
% # System time : 0.013 s
% # Total time : 0.331 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.59 CPU 0.65 WC
% FINAL PrfWatch: 0.59 CPU 0.65 WC
% SZS output end Solution for /tmp/SystemOnTPTP1817/SEU224+2.tptp
%
%------------------------------------------------------------------------------