%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : PUZ128+2 : TPTP v5.0.0. Released v4.0.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 : Wed Dec 29 21:36:30 EST 2010
% Result : Theorem 1.10s
% Output : Solution 1.10s
% 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/SystemOnTPTP19268/PUZ128+2.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP19268/PUZ128+2.tptp
% SZS output start Solution for /tmp/SystemOnTPTP19268/PUZ128+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 19400
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Preprocessing time : 0.011 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,?[X1]:?[X2]:?[X3]:?[X4]:?[X5]:((((((((((((((parent(X1)&relation(X1,of,'Oedipus'))&'Iokaste'=X1)&parent(X2))&relation(X2,of,'Polyneikes'))&'Iokaste'=X2)&parent(X3))&relation(X3,of,'Polyneikes'))&'Oedipus'=X3)&parent(X4))&relation(X4,of,'Thersandros'))&'Polyneikes'=X4)&patricide(X5))&'Oedipus'=X5)&~(?[X6]:(patricide(X6)&'Thersandros'=X6))),file('/tmp/SRASS.s.p', background)).
% fof(2, conjecture,?[X1]:?[X2]:?[X3]:?[X4]:((((((((parent(X1)&patricide(X2))&parent(X3))&$true)&~(?[X5]:(patricide(X5)&X4=X5)))&relation(X3,of,X4))&X2=X3)&relation(X1,of,X2))&'Iokaste'=X1),file('/tmp/SRASS.s.p', prove)).
% fof(3, negated_conjecture,~(?[X1]:?[X2]:?[X3]:?[X4]:((((((((parent(X1)&patricide(X2))&parent(X3))&$true)&~(?[X5]:(patricide(X5)&X4=X5)))&relation(X3,of,X4))&X2=X3)&relation(X1,of,X2))&'Iokaste'=X1)),inference(assume_negation,[status(cth)],[2])).
% fof(4, negated_conjecture,~(?[X1]:?[X2]:?[X3]:?[X4]:(((((((parent(X1)&patricide(X2))&parent(X3))&~(?[X5]:(patricide(X5)&X4=X5)))&relation(X3,of,X4))&X2=X3)&relation(X1,of,X2))&'Iokaste'=X1)),inference(fof_simplification,[status(thm)],[3,theory(equality)])).
% fof(5, plain,?[X1]:?[X2]:?[X3]:?[X4]:?[X5]:((((((((((((((parent(X1)&relation(X1,of,'Oedipus'))&'Iokaste'=X1)&parent(X2))&relation(X2,of,'Polyneikes'))&'Iokaste'=X2)&parent(X3))&relation(X3,of,'Polyneikes'))&'Oedipus'=X3)&parent(X4))&relation(X4,of,'Thersandros'))&'Polyneikes'=X4)&patricide(X5))&'Oedipus'=X5)&![X6]:(~(patricide(X6))|~('Thersandros'=X6))),inference(fof_nnf,[status(thm)],[1])).
% fof(6, plain,?[X7]:?[X8]:?[X9]:?[X10]:?[X11]:((((((((((((((parent(X7)&relation(X7,of,'Oedipus'))&'Iokaste'=X7)&parent(X8))&relation(X8,of,'Polyneikes'))&'Iokaste'=X8)&parent(X9))&relation(X9,of,'Polyneikes'))&'Oedipus'=X9)&parent(X10))&relation(X10,of,'Thersandros'))&'Polyneikes'=X10)&patricide(X11))&'Oedipus'=X11)&![X12]:(~(patricide(X12))|~('Thersandros'=X12))),inference(variable_rename,[status(thm)],[5])).
% fof(7, plain,((((((((((((((parent(esk1_0)&relation(esk1_0,of,'Oedipus'))&'Iokaste'=esk1_0)&parent(esk2_0))&relation(esk2_0,of,'Polyneikes'))&'Iokaste'=esk2_0)&parent(esk3_0))&relation(esk3_0,of,'Polyneikes'))&'Oedipus'=esk3_0)&parent(esk4_0))&relation(esk4_0,of,'Thersandros'))&'Polyneikes'=esk4_0)&patricide(esk5_0))&'Oedipus'=esk5_0)&![X12]:(~(patricide(X12))|~('Thersandros'=X12))),inference(skolemize,[status(esa)],[6])).
% fof(8, plain,![X12]:((~(patricide(X12))|~('Thersandros'=X12))&(((((((((((((parent(esk1_0)&relation(esk1_0,of,'Oedipus'))&'Iokaste'=esk1_0)&parent(esk2_0))&relation(esk2_0,of,'Polyneikes'))&'Iokaste'=esk2_0)&parent(esk3_0))&relation(esk3_0,of,'Polyneikes'))&'Oedipus'=esk3_0)&parent(esk4_0))&relation(esk4_0,of,'Thersandros'))&'Polyneikes'=esk4_0)&patricide(esk5_0))&'Oedipus'=esk5_0)),inference(shift_quantors,[status(thm)],[7])).
% cnf(9,plain,('Oedipus'=esk5_0),inference(split_conjunct,[status(thm)],[8])).
% cnf(10,plain,(patricide(esk5_0)),inference(split_conjunct,[status(thm)],[8])).
% cnf(11,plain,('Polyneikes'=esk4_0),inference(split_conjunct,[status(thm)],[8])).
% cnf(12,plain,(relation(esk4_0,of,'Thersandros')),inference(split_conjunct,[status(thm)],[8])).
% cnf(13,plain,(parent(esk4_0)),inference(split_conjunct,[status(thm)],[8])).
% cnf(14,plain,('Oedipus'=esk3_0),inference(split_conjunct,[status(thm)],[8])).
% cnf(15,plain,(relation(esk3_0,of,'Polyneikes')),inference(split_conjunct,[status(thm)],[8])).
% cnf(16,plain,(parent(esk3_0)),inference(split_conjunct,[status(thm)],[8])).
% cnf(17,plain,('Iokaste'=esk2_0),inference(split_conjunct,[status(thm)],[8])).
% cnf(18,plain,(relation(esk2_0,of,'Polyneikes')),inference(split_conjunct,[status(thm)],[8])).
% cnf(20,plain,('Iokaste'=esk1_0),inference(split_conjunct,[status(thm)],[8])).
% cnf(21,plain,(relation(esk1_0,of,'Oedipus')),inference(split_conjunct,[status(thm)],[8])).
% cnf(22,plain,(parent(esk1_0)),inference(split_conjunct,[status(thm)],[8])).
% cnf(23,plain,('Thersandros'!=X1|~patricide(X1)),inference(split_conjunct,[status(thm)],[8])).
% fof(24, negated_conjecture,![X1]:![X2]:![X3]:![X4]:(((((((~(parent(X1))|~(patricide(X2)))|~(parent(X3)))|?[X5]:(patricide(X5)&X4=X5))|~(relation(X3,of,X4)))|~(X2=X3))|~(relation(X1,of,X2)))|~('Iokaste'=X1)),inference(fof_nnf,[status(thm)],[4])).
% fof(25, negated_conjecture,![X6]:![X7]:![X8]:![X9]:(((((((~(parent(X6))|~(patricide(X7)))|~(parent(X8)))|?[X10]:(patricide(X10)&X9=X10))|~(relation(X8,of,X9)))|~(X7=X8))|~(relation(X6,of,X7)))|~('Iokaste'=X6)),inference(variable_rename,[status(thm)],[24])).
% fof(26, negated_conjecture,![X6]:![X7]:![X8]:![X9]:(((((((~(parent(X6))|~(patricide(X7)))|~(parent(X8)))|(patricide(esk6_4(X6,X7,X8,X9))&X9=esk6_4(X6,X7,X8,X9)))|~(relation(X8,of,X9)))|~(X7=X8))|~(relation(X6,of,X7)))|~('Iokaste'=X6)),inference(skolemize,[status(esa)],[25])).
% fof(27, negated_conjecture,![X6]:![X7]:![X8]:![X9]:((((((patricide(esk6_4(X6,X7,X8,X9))|((~(parent(X6))|~(patricide(X7)))|~(parent(X8))))|~(relation(X8,of,X9)))|~(X7=X8))|~(relation(X6,of,X7)))|~('Iokaste'=X6))&(((((X9=esk6_4(X6,X7,X8,X9)|((~(parent(X6))|~(patricide(X7)))|~(parent(X8))))|~(relation(X8,of,X9)))|~(X7=X8))|~(relation(X6,of,X7)))|~('Iokaste'=X6))),inference(distribute,[status(thm)],[26])).
% cnf(28,negated_conjecture,(X4=esk6_4(X1,X2,X3,X4)|'Iokaste'!=X1|~relation(X1,of,X2)|X2!=X3|~relation(X3,of,X4)|~parent(X3)|~patricide(X2)|~parent(X1)),inference(split_conjunct,[status(thm)],[27])).
% cnf(29,negated_conjecture,(patricide(esk6_4(X1,X2,X3,X4))|'Iokaste'!=X1|~relation(X1,of,X2)|X2!=X3|~relation(X3,of,X4)|~parent(X3)|~patricide(X2)|~parent(X1)),inference(split_conjunct,[status(thm)],[27])).
% cnf(30,plain,(esk2_0=esk1_0),inference(rw,[status(thm)],[17,20,theory(equality)])).
% cnf(32,plain,(parent(esk2_0)),inference(rw,[status(thm)],[22,30,theory(equality)])).
% cnf(34,plain,(esk5_0=esk3_0),inference(rw,[status(thm)],[9,14,theory(equality)])).
% cnf(35,plain,(patricide(esk3_0)),inference(rw,[status(thm)],[10,34,theory(equality)])).
% cnf(36,plain,(relation(esk2_0,of,esk3_0)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[21,30,theory(equality)]),14,theory(equality)])).
% cnf(37,plain,(relation(esk2_0,of,esk4_0)),inference(rw,[status(thm)],[18,11,theory(equality)])).
% cnf(38,plain,(relation(esk3_0,of,esk4_0)),inference(rw,[status(thm)],[15,11,theory(equality)])).
% cnf(39,negated_conjecture,(patricide(esk6_4(X1,X2,X3,X4))|X2!=X3|esk2_0!=X1|~parent(X3)|~parent(X1)|~patricide(X2)|~relation(X3,of,X4)|~relation(X1,of,X2)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[29,20,theory(equality)]),30,theory(equality)])).
% cnf(40,negated_conjecture,(patricide(esk6_4(X1,X2,X2,X3))|esk2_0!=X1|~patricide(X2)|~relation(X2,of,X3)|~relation(X1,of,X2)|~parent(X2)|~parent(X1)),inference(er,[status(thm)],[39,theory(equality)])).
% cnf(41,negated_conjecture,(esk6_4(X1,X2,X3,X4)=X4|X2!=X3|esk2_0!=X1|~parent(X3)|~parent(X1)|~patricide(X2)|~relation(X3,of,X4)|~relation(X1,of,X2)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[28,20,theory(equality)]),30,theory(equality)])).
% cnf(42,negated_conjecture,(esk6_4(X1,X2,X2,X3)=X3|esk2_0!=X1|~patricide(X2)|~relation(X2,of,X3)|~relation(X1,of,X2)|~parent(X2)|~parent(X1)),inference(er,[status(thm)],[41,theory(equality)])).
% cnf(44,negated_conjecture,('Thersandros'!=esk6_4(X1,X2,X2,X3)|esk2_0!=X1|~patricide(X2)|~relation(X2,of,X3)|~relation(X1,of,X2)|~parent(X2)|~parent(X1)),inference(spm,[status(thm)],[23,40,theory(equality)])).
% cnf(45,negated_conjecture,(patricide(X3)|esk2_0!=X1|~patricide(X2)|~relation(X2,of,X3)|~relation(X1,of,X2)|~parent(X2)|~parent(X1)),inference(spm,[status(thm)],[40,42,theory(equality)])).
% cnf(46,negated_conjecture,(X3!='Thersandros'|esk2_0!=X1|~patricide(X2)|~relation(X2,of,X3)|~relation(X1,of,X2)|~parent(X2)|~parent(X1)),inference(spm,[status(thm)],[44,42,theory(equality)])).
% cnf(47,negated_conjecture,(esk2_0!=X1|~patricide(esk4_0)|~relation(X1,of,esk4_0)|~parent(esk4_0)|~parent(X1)),inference(spm,[status(thm)],[46,12,theory(equality)])).
% cnf(51,negated_conjecture,(esk2_0!=X1|~patricide(esk4_0)|~relation(X1,of,esk4_0)|$false|~parent(X1)),inference(rw,[status(thm)],[47,13,theory(equality)])).
% cnf(52,negated_conjecture,(esk2_0!=X1|~patricide(esk4_0)|~relation(X1,of,esk4_0)|~parent(X1)),inference(cn,[status(thm)],[51,theory(equality)])).
% cnf(61,negated_conjecture,(patricide(esk4_0)|esk2_0!=X1|~patricide(esk3_0)|~relation(X1,of,esk3_0)|~parent(esk3_0)|~parent(X1)),inference(spm,[status(thm)],[45,38,theory(equality)])).
% cnf(66,negated_conjecture,(patricide(esk4_0)|esk2_0!=X1|$false|~relation(X1,of,esk3_0)|~parent(esk3_0)|~parent(X1)),inference(rw,[status(thm)],[61,35,theory(equality)])).
% cnf(67,negated_conjecture,(patricide(esk4_0)|esk2_0!=X1|$false|~relation(X1,of,esk3_0)|$false|~parent(X1)),inference(rw,[status(thm)],[66,16,theory(equality)])).
% cnf(68,negated_conjecture,(patricide(esk4_0)|esk2_0!=X1|~relation(X1,of,esk3_0)|~parent(X1)),inference(cn,[status(thm)],[67,theory(equality)])).
% cnf(74,negated_conjecture,(patricide(esk4_0)|~parent(esk2_0)),inference(spm,[status(thm)],[68,36,theory(equality)])).
% cnf(75,negated_conjecture,(patricide(esk4_0)|$false),inference(rw,[status(thm)],[74,32,theory(equality)])).
% cnf(76,negated_conjecture,(patricide(esk4_0)),inference(cn,[status(thm)],[75,theory(equality)])).
% cnf(79,negated_conjecture,(esk2_0!=X1|$false|~relation(X1,of,esk4_0)|~parent(X1)),inference(rw,[status(thm)],[52,76,theory(equality)])).
% cnf(80,negated_conjecture,(esk2_0!=X1|~relation(X1,of,esk4_0)|~parent(X1)),inference(cn,[status(thm)],[79,theory(equality)])).
% cnf(82,negated_conjecture,(~parent(esk2_0)),inference(spm,[status(thm)],[80,37,theory(equality)])).
% cnf(85,negated_conjecture,($false),inference(rw,[status(thm)],[82,32,theory(equality)])).
% cnf(86,negated_conjecture,($false),inference(cn,[status(thm)],[85,theory(equality)])).
% cnf(87,negated_conjecture,($false),86,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 45
% # ...of these trivial : 1
% # ...subsumed : 0
% # ...remaining for further processing: 44
% # Other redundant clauses eliminated : 2
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 0
% # Backward-rewritten : 3
% # Generated clauses : 18
% # ...of the previous two non-trivial : 18
% # Contextual simplify-reflections : 0
% # Paramodulations : 16
% # Factorizations : 0
% # Equation resolutions : 2
% # Current number of processed clauses: 23
% # Positive orientable unit clauses: 14
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 2
% # Non-unit-clauses : 7
% # Current number of unprocessed clauses: 6
% # ...number of literals in the above : 25
% # Clause-clause subsumption calls (NU) : 17
% # Rec. Clause-clause subsumption calls : 14
% # Unit Clause-clause subsumption calls : 0
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 5
% # Indexed BW rewrite successes : 3
% # Backwards rewriting index: 24 leaves, 1.33+/-0.799 terms/leaf
% # Paramod-from index: 15 leaves, 1.07+/-0.249 terms/leaf
% # Paramod-into index: 22 leaves, 1.09+/-0.287 terms/leaf
% # -------------------------------------------------
% # User time : 0.011 s
% # System time : 0.003 s
% # Total time : 0.014 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.09 CPU 0.18 WC
% FINAL PrfWatch: 0.09 CPU 0.18 WC
% SZS output end Solution for /tmp/SystemOnTPTP19268/PUZ128+2.tptp
%
%------------------------------------------------------------------------------