%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : GEO085+1 : TPTP v5.0.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art01.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 : Wed Dec 29 04:20:31 EST 2010
% Result : Theorem 1.09s
% Output : Solution 1.09s
% 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/SystemOnTPTP5936/GEO085+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP5936/GEO085+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP5936/GEO085+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 6032
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% # Preprocessing time : 0.016 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:(open(X1)<=>?[X2]:end_point(X2,X1)),file('/tmp/SRASS.s.p', open_defn)).
% fof(3, axiom,![X1]:![X2]:(end_point(X2,X1)=>?[X3]:(end_point(X3,X1)&~(X2=X3))),file('/tmp/SRASS.s.p', c6)).
% fof(6, axiom,![X1]:(closed(X1)<=>~(?[X2]:end_point(X2,X1))),file('/tmp/SRASS.s.p', closed_defn)).
% fof(14, axiom,![X2]:![X1]:(inner_point(X2,X1)<=>(incident_c(X2,X1)&~(end_point(X2,X1)))),file('/tmp/SRASS.s.p', inner_point_defn)).
% fof(15, axiom,![X2]:![X1]:(end_point(X2,X1)<=>(incident_c(X2,X1)&![X5]:![X6]:((((part_of(X5,X1)&part_of(X6,X1))&incident_c(X2,X5))&incident_c(X2,X6))=>(part_of(X5,X6)|part_of(X6,X5))))),file('/tmp/SRASS.s.p', end_point_defn)).
% fof(17, conjecture,![X1]:(open(X1)=>?[X2]:?[X3]:((~(X2=X3)&end_point(X2,X1))&end_point(X3,X1))),file('/tmp/SRASS.s.p', theorem_2_7_1)).
% fof(18, negated_conjecture,~(![X1]:(open(X1)=>?[X2]:?[X3]:((~(X2=X3)&end_point(X2,X1))&end_point(X3,X1)))),inference(assume_negation,[status(cth)],[17])).
% fof(19, plain,![X2]:![X1]:(inner_point(X2,X1)<=>(incident_c(X2,X1)&~(end_point(X2,X1)))),inference(fof_simplification,[status(thm)],[14,theory(equality)])).
% fof(20, plain,![X1]:((~(open(X1))|?[X2]:end_point(X2,X1))&(![X2]:~(end_point(X2,X1))|open(X1))),inference(fof_nnf,[status(thm)],[1])).
% fof(21, plain,![X3]:((~(open(X3))|?[X4]:end_point(X4,X3))&(![X5]:~(end_point(X5,X3))|open(X3))),inference(variable_rename,[status(thm)],[20])).
% fof(22, plain,![X3]:((~(open(X3))|end_point(esk1_1(X3),X3))&(![X5]:~(end_point(X5,X3))|open(X3))),inference(skolemize,[status(esa)],[21])).
% fof(23, plain,![X3]:![X5]:((~(end_point(X5,X3))|open(X3))&(~(open(X3))|end_point(esk1_1(X3),X3))),inference(shift_quantors,[status(thm)],[22])).
% cnf(24,plain,(end_point(esk1_1(X1),X1)|~open(X1)),inference(split_conjunct,[status(thm)],[23])).
% fof(29, plain,![X1]:![X2]:(~(end_point(X2,X1))|?[X3]:(end_point(X3,X1)&~(X2=X3))),inference(fof_nnf,[status(thm)],[3])).
% fof(30, plain,![X4]:![X5]:(~(end_point(X5,X4))|?[X6]:(end_point(X6,X4)&~(X5=X6))),inference(variable_rename,[status(thm)],[29])).
% fof(31, plain,![X4]:![X5]:(~(end_point(X5,X4))|(end_point(esk2_2(X4,X5),X4)&~(X5=esk2_2(X4,X5)))),inference(skolemize,[status(esa)],[30])).
% fof(32, plain,![X4]:![X5]:((end_point(esk2_2(X4,X5),X4)|~(end_point(X5,X4)))&(~(X5=esk2_2(X4,X5))|~(end_point(X5,X4)))),inference(distribute,[status(thm)],[31])).
% cnf(33,plain,(~end_point(X1,X2)|X1!=esk2_2(X2,X1)),inference(split_conjunct,[status(thm)],[32])).
% cnf(34,plain,(end_point(esk2_2(X2,X1),X2)|~end_point(X1,X2)),inference(split_conjunct,[status(thm)],[32])).
% fof(44, plain,![X1]:((~(closed(X1))|![X2]:~(end_point(X2,X1)))&(?[X2]:end_point(X2,X1)|closed(X1))),inference(fof_nnf,[status(thm)],[6])).
% fof(45, plain,![X3]:((~(closed(X3))|![X4]:~(end_point(X4,X3)))&(?[X5]:end_point(X5,X3)|closed(X3))),inference(variable_rename,[status(thm)],[44])).
% fof(46, plain,![X3]:((~(closed(X3))|![X4]:~(end_point(X4,X3)))&(end_point(esk4_1(X3),X3)|closed(X3))),inference(skolemize,[status(esa)],[45])).
% fof(47, plain,![X3]:![X4]:((~(end_point(X4,X3))|~(closed(X3)))&(end_point(esk4_1(X3),X3)|closed(X3))),inference(shift_quantors,[status(thm)],[46])).
% cnf(48,plain,(closed(X1)|end_point(esk4_1(X1),X1)),inference(split_conjunct,[status(thm)],[47])).
% cnf(49,plain,(~closed(X1)|~end_point(X2,X1)),inference(split_conjunct,[status(thm)],[47])).
% fof(97, plain,![X2]:![X1]:((~(inner_point(X2,X1))|(incident_c(X2,X1)&~(end_point(X2,X1))))&((~(incident_c(X2,X1))|end_point(X2,X1))|inner_point(X2,X1))),inference(fof_nnf,[status(thm)],[19])).
% fof(98, plain,![X3]:![X4]:((~(inner_point(X3,X4))|(incident_c(X3,X4)&~(end_point(X3,X4))))&((~(incident_c(X3,X4))|end_point(X3,X4))|inner_point(X3,X4))),inference(variable_rename,[status(thm)],[97])).
% fof(99, plain,![X3]:![X4]:(((incident_c(X3,X4)|~(inner_point(X3,X4)))&(~(end_point(X3,X4))|~(inner_point(X3,X4))))&((~(incident_c(X3,X4))|end_point(X3,X4))|inner_point(X3,X4))),inference(distribute,[status(thm)],[98])).
% cnf(100,plain,(inner_point(X1,X2)|end_point(X1,X2)|~incident_c(X1,X2)),inference(split_conjunct,[status(thm)],[99])).
% cnf(101,plain,(~inner_point(X1,X2)|~end_point(X1,X2)),inference(split_conjunct,[status(thm)],[99])).
% fof(103, plain,![X2]:![X1]:((~(end_point(X2,X1))|(incident_c(X2,X1)&![X5]:![X6]:((((~(part_of(X5,X1))|~(part_of(X6,X1)))|~(incident_c(X2,X5)))|~(incident_c(X2,X6)))|(part_of(X5,X6)|part_of(X6,X5)))))&((~(incident_c(X2,X1))|?[X5]:?[X6]:((((part_of(X5,X1)&part_of(X6,X1))&incident_c(X2,X5))&incident_c(X2,X6))&(~(part_of(X5,X6))&~(part_of(X6,X5)))))|end_point(X2,X1))),inference(fof_nnf,[status(thm)],[15])).
% fof(104, plain,![X7]:![X8]:((~(end_point(X7,X8))|(incident_c(X7,X8)&![X9]:![X10]:((((~(part_of(X9,X8))|~(part_of(X10,X8)))|~(incident_c(X7,X9)))|~(incident_c(X7,X10)))|(part_of(X9,X10)|part_of(X10,X9)))))&((~(incident_c(X7,X8))|?[X11]:?[X12]:((((part_of(X11,X8)&part_of(X12,X8))&incident_c(X7,X11))&incident_c(X7,X12))&(~(part_of(X11,X12))&~(part_of(X12,X11)))))|end_point(X7,X8))),inference(variable_rename,[status(thm)],[103])).
% fof(105, plain,![X7]:![X8]:((~(end_point(X7,X8))|(incident_c(X7,X8)&![X9]:![X10]:((((~(part_of(X9,X8))|~(part_of(X10,X8)))|~(incident_c(X7,X9)))|~(incident_c(X7,X10)))|(part_of(X9,X10)|part_of(X10,X9)))))&((~(incident_c(X7,X8))|((((part_of(esk10_2(X7,X8),X8)&part_of(esk11_2(X7,X8),X8))&incident_c(X7,esk10_2(X7,X8)))&incident_c(X7,esk11_2(X7,X8)))&(~(part_of(esk10_2(X7,X8),esk11_2(X7,X8)))&~(part_of(esk11_2(X7,X8),esk10_2(X7,X8))))))|end_point(X7,X8))),inference(skolemize,[status(esa)],[104])).
% fof(106, plain,![X7]:![X8]:![X9]:![X10]:(((((((~(part_of(X9,X8))|~(part_of(X10,X8)))|~(incident_c(X7,X9)))|~(incident_c(X7,X10)))|(part_of(X9,X10)|part_of(X10,X9)))&incident_c(X7,X8))|~(end_point(X7,X8)))&((~(incident_c(X7,X8))|((((part_of(esk10_2(X7,X8),X8)&part_of(esk11_2(X7,X8),X8))&incident_c(X7,esk10_2(X7,X8)))&incident_c(X7,esk11_2(X7,X8)))&(~(part_of(esk10_2(X7,X8),esk11_2(X7,X8)))&~(part_of(esk11_2(X7,X8),esk10_2(X7,X8))))))|end_point(X7,X8))),inference(shift_quantors,[status(thm)],[105])).
% fof(107, plain,![X7]:![X8]:![X9]:![X10]:(((((((~(part_of(X9,X8))|~(part_of(X10,X8)))|~(incident_c(X7,X9)))|~(incident_c(X7,X10)))|(part_of(X9,X10)|part_of(X10,X9)))|~(end_point(X7,X8)))&(incident_c(X7,X8)|~(end_point(X7,X8))))&((((((part_of(esk10_2(X7,X8),X8)|~(incident_c(X7,X8)))|end_point(X7,X8))&((part_of(esk11_2(X7,X8),X8)|~(incident_c(X7,X8)))|end_point(X7,X8)))&((incident_c(X7,esk10_2(X7,X8))|~(incident_c(X7,X8)))|end_point(X7,X8)))&((incident_c(X7,esk11_2(X7,X8))|~(incident_c(X7,X8)))|end_point(X7,X8)))&(((~(part_of(esk10_2(X7,X8),esk11_2(X7,X8)))|~(incident_c(X7,X8)))|end_point(X7,X8))&((~(part_of(esk11_2(X7,X8),esk10_2(X7,X8)))|~(incident_c(X7,X8)))|end_point(X7,X8))))),inference(distribute,[status(thm)],[106])).
% cnf(114,plain,(incident_c(X1,X2)|~end_point(X1,X2)),inference(split_conjunct,[status(thm)],[107])).
% fof(122, negated_conjecture,?[X1]:(open(X1)&![X2]:![X3]:((X2=X3|~(end_point(X2,X1)))|~(end_point(X3,X1)))),inference(fof_nnf,[status(thm)],[18])).
% fof(123, negated_conjecture,?[X4]:(open(X4)&![X5]:![X6]:((X5=X6|~(end_point(X5,X4)))|~(end_point(X6,X4)))),inference(variable_rename,[status(thm)],[122])).
% fof(124, negated_conjecture,(open(esk14_0)&![X5]:![X6]:((X5=X6|~(end_point(X5,esk14_0)))|~(end_point(X6,esk14_0)))),inference(skolemize,[status(esa)],[123])).
% fof(125, negated_conjecture,![X5]:![X6]:(((X5=X6|~(end_point(X5,esk14_0)))|~(end_point(X6,esk14_0)))&open(esk14_0)),inference(shift_quantors,[status(thm)],[124])).
% cnf(126,negated_conjecture,(open(esk14_0)),inference(split_conjunct,[status(thm)],[125])).
% cnf(127,negated_conjecture,(X2=X1|~end_point(X1,esk14_0)|~end_point(X2,esk14_0)),inference(split_conjunct,[status(thm)],[125])).
% cnf(129,plain,(~closed(X1)|~open(X1)),inference(spm,[status(thm)],[49,24,theory(equality)])).
% cnf(130,plain,(incident_c(esk1_1(X1),X1)|~open(X1)),inference(spm,[status(thm)],[114,24,theory(equality)])).
% cnf(131,negated_conjecture,(X1=esk1_1(esk14_0)|~end_point(X1,esk14_0)|~open(esk14_0)),inference(spm,[status(thm)],[127,24,theory(equality)])).
% cnf(132,negated_conjecture,(X1=esk1_1(esk14_0)|~end_point(X1,esk14_0)|$false),inference(rw,[status(thm)],[131,126,theory(equality)])).
% cnf(133,negated_conjecture,(X1=esk1_1(esk14_0)|~end_point(X1,esk14_0)),inference(cn,[status(thm)],[132,theory(equality)])).
% cnf(139,plain,(~inner_point(esk1_1(X1),X1)|~open(X1)),inference(spm,[status(thm)],[101,24,theory(equality)])).
% cnf(152,plain,(inner_point(X2,X1)|esk2_2(X1,X2)!=X2|~incident_c(X2,X1)),inference(spm,[status(thm)],[33,100,theory(equality)])).
% cnf(231,negated_conjecture,(~closed(esk14_0)),inference(spm,[status(thm)],[129,126,theory(equality)])).
% cnf(239,negated_conjecture,(incident_c(esk1_1(esk14_0),esk14_0)),inference(spm,[status(thm)],[130,126,theory(equality)])).
% cnf(246,negated_conjecture,(esk4_1(esk14_0)=esk1_1(esk14_0)|closed(esk14_0)),inference(spm,[status(thm)],[133,48,theory(equality)])).
% cnf(249,negated_conjecture,(esk1_1(esk14_0)=esk4_1(esk14_0)),inference(sr,[status(thm)],[246,231,theory(equality)])).
% cnf(251,negated_conjecture,(~inner_point(esk4_1(esk14_0),esk14_0)|~open(esk14_0)),inference(spm,[status(thm)],[139,249,theory(equality)])).
% cnf(253,negated_conjecture,(incident_c(esk4_1(esk14_0),esk14_0)),inference(rw,[status(thm)],[239,249,theory(equality)])).
% cnf(254,negated_conjecture,(X1=esk4_1(esk14_0)|~end_point(X1,esk14_0)),inference(rw,[status(thm)],[133,249,theory(equality)])).
% cnf(257,negated_conjecture,(~inner_point(esk4_1(esk14_0),esk14_0)|$false),inference(rw,[status(thm)],[251,126,theory(equality)])).
% cnf(258,negated_conjecture,(~inner_point(esk4_1(esk14_0),esk14_0)),inference(cn,[status(thm)],[257,theory(equality)])).
% cnf(266,negated_conjecture,(esk2_2(esk14_0,X1)=esk4_1(esk14_0)|~end_point(X1,esk14_0)),inference(spm,[status(thm)],[254,34,theory(equality)])).
% cnf(282,negated_conjecture,(esk2_2(esk14_0,esk4_1(esk14_0))=esk4_1(esk14_0)|closed(esk14_0)),inference(spm,[status(thm)],[266,48,theory(equality)])).
% cnf(287,negated_conjecture,(esk2_2(esk14_0,esk4_1(esk14_0))=esk4_1(esk14_0)),inference(sr,[status(thm)],[282,231,theory(equality)])).
% cnf(291,negated_conjecture,(inner_point(esk4_1(esk14_0),esk14_0)|~incident_c(esk4_1(esk14_0),esk14_0)),inference(spm,[status(thm)],[152,287,theory(equality)])).
% cnf(294,negated_conjecture,(inner_point(esk4_1(esk14_0),esk14_0)|$false),inference(rw,[status(thm)],[291,253,theory(equality)])).
% cnf(295,negated_conjecture,(inner_point(esk4_1(esk14_0),esk14_0)),inference(cn,[status(thm)],[294,theory(equality)])).
% cnf(296,negated_conjecture,($false),inference(sr,[status(thm)],[295,258,theory(equality)])).
% cnf(297,negated_conjecture,($false),296,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 114
% # ...of these trivial : 0
% # ...subsumed : 4
% # ...remaining for further processing: 110
% # Other redundant clauses eliminated : 3
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 0
% # Backward-rewritten : 2
% # Generated clauses : 146
% # ...of the previous two non-trivial : 128
% # Contextual simplify-reflections : 0
% # Paramodulations : 132
% # Factorizations : 8
% # Equation resolutions : 6
% # Current number of processed clauses: 63
% # Positive orientable unit clauses: 8
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 2
% # Non-unit-clauses : 53
% # Current number of unprocessed clauses: 97
% # ...number of literals in the above : 429
% # Clause-clause subsumption calls (NU) : 121
% # Rec. Clause-clause subsumption calls : 101
% # Unit Clause-clause subsumption calls : 6
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 14
% # Indexed BW rewrite successes : 1
% # Backwards rewriting index: 56 leaves, 1.73+/-1.716 terms/leaf
% # Paramod-from index: 19 leaves, 1.21+/-0.521 terms/leaf
% # Paramod-into index: 47 leaves, 1.47+/-0.942 terms/leaf
% # -------------------------------------------------
% # User time : 0.023 s
% # System time : 0.004 s
% # Total time : 0.027 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.13 CPU 0.24 WC
% FINAL PrfWatch: 0.13 CPU 0.24 WC
% SZS output end Solution for /tmp/SystemOnTPTP5936/GEO085+1.tptp
%
%------------------------------------------------------------------------------