%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : PRO010+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 : art03.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 21:10:05 EST 2010
% Result : Theorem 0.98s
% Output : Solution 0.98s
% 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/SystemOnTPTP18008/PRO010+2.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP18008/PRO010+2.tptp
% SZS output start Solution for /tmp/SystemOnTPTP18008/PRO010+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 18104
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.017 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(6, axiom,~(atomic(tptp0)),file('/tmp/SRASS.s.p', sos_34)).
% fof(7, axiom,![X17]:(occurrence_of(X17,tptp0)=>?[X18]:?[X19]:?[X20]:((((((occurrence_of(X18,tptp3)&root_occ(X18,X17))&occurrence_of(X19,tptp4))&next_subocc(X18,X19,tptp0))&(occurrence_of(X20,tptp1)|occurrence_of(X20,tptp2)))&next_subocc(X19,X20,tptp0))&leaf_occ(X20,X17))),file('/tmp/SRASS.s.p', sos_32)).
% fof(18, axiom,![X44]:![X45]:![X46]:((occurrence_of(X44,X45)&occurrence_of(X44,X46))=>X45=X46),file('/tmp/SRASS.s.p', sos_22)).
% fof(29, axiom,![X62]:![X63]:![X64]:(min_precedes(X63,X64,X62)=>?[X65]:?[X66]:(((subactivity(X65,X62)&subactivity(X66,X62))&atocc(X63,X65))&atocc(X64,X66))),file('/tmp/SRASS.s.p', sos_26)).
% fof(42, axiom,![X92]:![X93]:(atocc(X92,X93)<=>?[X94]:((subactivity(X93,X94)&atomic(X94))&occurrence_of(X92,X94))),file('/tmp/SRASS.s.p', sos_15)).
% fof(46, conjecture,![X100]:(occurrence_of(X100,tptp0)=>?[X101]:?[X102]:((leaf_occ(X102,X100)&(occurrence_of(X102,tptp1)=>~(?[X103]:(occurrence_of(X103,tptp2)&min_precedes(X101,X103,tptp0)))))&(occurrence_of(X102,tptp2)=>~(?[X104]:(occurrence_of(X104,tptp1)&min_precedes(X101,X104,tptp0)))))),file('/tmp/SRASS.s.p', goals)).
% fof(47, negated_conjecture,~(![X100]:(occurrence_of(X100,tptp0)=>?[X101]:?[X102]:((leaf_occ(X102,X100)&(occurrence_of(X102,tptp1)=>~(?[X103]:(occurrence_of(X103,tptp2)&min_precedes(X101,X103,tptp0)))))&(occurrence_of(X102,tptp2)=>~(?[X104]:(occurrence_of(X104,tptp1)&min_precedes(X101,X104,tptp0))))))),inference(assume_negation,[status(cth)],[46])).
% fof(48, plain,~(atomic(tptp0)),inference(fof_simplification,[status(thm)],[6,theory(equality)])).
% cnf(74,plain,(~atomic(tptp0)),inference(split_conjunct,[status(thm)],[48])).
% fof(75, plain,![X17]:(~(occurrence_of(X17,tptp0))|?[X18]:?[X19]:?[X20]:((((((occurrence_of(X18,tptp3)&root_occ(X18,X17))&occurrence_of(X19,tptp4))&next_subocc(X18,X19,tptp0))&(occurrence_of(X20,tptp1)|occurrence_of(X20,tptp2)))&next_subocc(X19,X20,tptp0))&leaf_occ(X20,X17))),inference(fof_nnf,[status(thm)],[7])).
% fof(76, plain,![X21]:(~(occurrence_of(X21,tptp0))|?[X22]:?[X23]:?[X24]:((((((occurrence_of(X22,tptp3)&root_occ(X22,X21))&occurrence_of(X23,tptp4))&next_subocc(X22,X23,tptp0))&(occurrence_of(X24,tptp1)|occurrence_of(X24,tptp2)))&next_subocc(X23,X24,tptp0))&leaf_occ(X24,X21))),inference(variable_rename,[status(thm)],[75])).
% fof(77, plain,![X21]:(~(occurrence_of(X21,tptp0))|((((((occurrence_of(esk2_1(X21),tptp3)&root_occ(esk2_1(X21),X21))&occurrence_of(esk3_1(X21),tptp4))&next_subocc(esk2_1(X21),esk3_1(X21),tptp0))&(occurrence_of(esk4_1(X21),tptp1)|occurrence_of(esk4_1(X21),tptp2)))&next_subocc(esk3_1(X21),esk4_1(X21),tptp0))&leaf_occ(esk4_1(X21),X21))),inference(skolemize,[status(esa)],[76])).
% fof(78, plain,![X21]:(((((((occurrence_of(esk2_1(X21),tptp3)|~(occurrence_of(X21,tptp0)))&(root_occ(esk2_1(X21),X21)|~(occurrence_of(X21,tptp0))))&(occurrence_of(esk3_1(X21),tptp4)|~(occurrence_of(X21,tptp0))))&(next_subocc(esk2_1(X21),esk3_1(X21),tptp0)|~(occurrence_of(X21,tptp0))))&((occurrence_of(esk4_1(X21),tptp1)|occurrence_of(esk4_1(X21),tptp2))|~(occurrence_of(X21,tptp0))))&(next_subocc(esk3_1(X21),esk4_1(X21),tptp0)|~(occurrence_of(X21,tptp0))))&(leaf_occ(esk4_1(X21),X21)|~(occurrence_of(X21,tptp0)))),inference(distribute,[status(thm)],[77])).
% cnf(79,plain,(leaf_occ(esk4_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[78])).
% fof(128, plain,![X44]:![X45]:![X46]:((~(occurrence_of(X44,X45))|~(occurrence_of(X44,X46)))|X45=X46),inference(fof_nnf,[status(thm)],[18])).
% fof(129, plain,![X47]:![X48]:![X49]:((~(occurrence_of(X47,X48))|~(occurrence_of(X47,X49)))|X48=X49),inference(variable_rename,[status(thm)],[128])).
% cnf(130,plain,(X1=X2|~occurrence_of(X3,X2)|~occurrence_of(X3,X1)),inference(split_conjunct,[status(thm)],[129])).
% fof(159, plain,![X62]:![X63]:![X64]:(~(min_precedes(X63,X64,X62))|?[X65]:?[X66]:(((subactivity(X65,X62)&subactivity(X66,X62))&atocc(X63,X65))&atocc(X64,X66))),inference(fof_nnf,[status(thm)],[29])).
% fof(160, plain,![X67]:![X68]:![X69]:(~(min_precedes(X68,X69,X67))|?[X70]:?[X71]:(((subactivity(X70,X67)&subactivity(X71,X67))&atocc(X68,X70))&atocc(X69,X71))),inference(variable_rename,[status(thm)],[159])).
% fof(161, plain,![X67]:![X68]:![X69]:(~(min_precedes(X68,X69,X67))|(((subactivity(esk11_3(X67,X68,X69),X67)&subactivity(esk12_3(X67,X68,X69),X67))&atocc(X68,esk11_3(X67,X68,X69)))&atocc(X69,esk12_3(X67,X68,X69)))),inference(skolemize,[status(esa)],[160])).
% fof(162, plain,![X67]:![X68]:![X69]:((((subactivity(esk11_3(X67,X68,X69),X67)|~(min_precedes(X68,X69,X67)))&(subactivity(esk12_3(X67,X68,X69),X67)|~(min_precedes(X68,X69,X67))))&(atocc(X68,esk11_3(X67,X68,X69))|~(min_precedes(X68,X69,X67))))&(atocc(X69,esk12_3(X67,X68,X69))|~(min_precedes(X68,X69,X67)))),inference(distribute,[status(thm)],[161])).
% cnf(164,plain,(atocc(X1,esk11_3(X3,X1,X2))|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[162])).
% fof(220, plain,![X92]:![X93]:((~(atocc(X92,X93))|?[X94]:((subactivity(X93,X94)&atomic(X94))&occurrence_of(X92,X94)))&(![X94]:((~(subactivity(X93,X94))|~(atomic(X94)))|~(occurrence_of(X92,X94)))|atocc(X92,X93))),inference(fof_nnf,[status(thm)],[42])).
% fof(221, plain,![X95]:![X96]:((~(atocc(X95,X96))|?[X97]:((subactivity(X96,X97)&atomic(X97))&occurrence_of(X95,X97)))&(![X98]:((~(subactivity(X96,X98))|~(atomic(X98)))|~(occurrence_of(X95,X98)))|atocc(X95,X96))),inference(variable_rename,[status(thm)],[220])).
% fof(222, plain,![X95]:![X96]:((~(atocc(X95,X96))|((subactivity(X96,esk17_2(X95,X96))&atomic(esk17_2(X95,X96)))&occurrence_of(X95,esk17_2(X95,X96))))&(![X98]:((~(subactivity(X96,X98))|~(atomic(X98)))|~(occurrence_of(X95,X98)))|atocc(X95,X96))),inference(skolemize,[status(esa)],[221])).
% fof(223, plain,![X95]:![X96]:![X98]:((((~(subactivity(X96,X98))|~(atomic(X98)))|~(occurrence_of(X95,X98)))|atocc(X95,X96))&(~(atocc(X95,X96))|((subactivity(X96,esk17_2(X95,X96))&atomic(esk17_2(X95,X96)))&occurrence_of(X95,esk17_2(X95,X96))))),inference(shift_quantors,[status(thm)],[222])).
% fof(224, plain,![X95]:![X96]:![X98]:((((~(subactivity(X96,X98))|~(atomic(X98)))|~(occurrence_of(X95,X98)))|atocc(X95,X96))&(((subactivity(X96,esk17_2(X95,X96))|~(atocc(X95,X96)))&(atomic(esk17_2(X95,X96))|~(atocc(X95,X96))))&(occurrence_of(X95,esk17_2(X95,X96))|~(atocc(X95,X96))))),inference(distribute,[status(thm)],[223])).
% cnf(225,plain,(occurrence_of(X1,esk17_2(X1,X2))|~atocc(X1,X2)),inference(split_conjunct,[status(thm)],[224])).
% cnf(226,plain,(atomic(esk17_2(X1,X2))|~atocc(X1,X2)),inference(split_conjunct,[status(thm)],[224])).
% fof(241, negated_conjecture,?[X100]:(occurrence_of(X100,tptp0)&![X101]:![X102]:((~(leaf_occ(X102,X100))|(occurrence_of(X102,tptp1)&?[X103]:(occurrence_of(X103,tptp2)&min_precedes(X101,X103,tptp0))))|(occurrence_of(X102,tptp2)&?[X104]:(occurrence_of(X104,tptp1)&min_precedes(X101,X104,tptp0))))),inference(fof_nnf,[status(thm)],[47])).
% fof(242, negated_conjecture,?[X105]:(occurrence_of(X105,tptp0)&![X106]:![X107]:((~(leaf_occ(X107,X105))|(occurrence_of(X107,tptp1)&?[X108]:(occurrence_of(X108,tptp2)&min_precedes(X106,X108,tptp0))))|(occurrence_of(X107,tptp2)&?[X109]:(occurrence_of(X109,tptp1)&min_precedes(X106,X109,tptp0))))),inference(variable_rename,[status(thm)],[241])).
% fof(243, negated_conjecture,(occurrence_of(esk18_0,tptp0)&![X106]:![X107]:((~(leaf_occ(X107,esk18_0))|(occurrence_of(X107,tptp1)&(occurrence_of(esk19_2(X106,X107),tptp2)&min_precedes(X106,esk19_2(X106,X107),tptp0))))|(occurrence_of(X107,tptp2)&(occurrence_of(esk20_2(X106,X107),tptp1)&min_precedes(X106,esk20_2(X106,X107),tptp0))))),inference(skolemize,[status(esa)],[242])).
% fof(244, negated_conjecture,![X106]:![X107]:(((~(leaf_occ(X107,esk18_0))|(occurrence_of(X107,tptp1)&(occurrence_of(esk19_2(X106,X107),tptp2)&min_precedes(X106,esk19_2(X106,X107),tptp0))))|(occurrence_of(X107,tptp2)&(occurrence_of(esk20_2(X106,X107),tptp1)&min_precedes(X106,esk20_2(X106,X107),tptp0))))&occurrence_of(esk18_0,tptp0)),inference(shift_quantors,[status(thm)],[243])).
% fof(245, negated_conjecture,![X106]:![X107]:((((occurrence_of(X107,tptp2)|(occurrence_of(X107,tptp1)|~(leaf_occ(X107,esk18_0))))&((occurrence_of(esk20_2(X106,X107),tptp1)|(occurrence_of(X107,tptp1)|~(leaf_occ(X107,esk18_0))))&(min_precedes(X106,esk20_2(X106,X107),tptp0)|(occurrence_of(X107,tptp1)|~(leaf_occ(X107,esk18_0))))))&(((occurrence_of(X107,tptp2)|(occurrence_of(esk19_2(X106,X107),tptp2)|~(leaf_occ(X107,esk18_0))))&((occurrence_of(esk20_2(X106,X107),tptp1)|(occurrence_of(esk19_2(X106,X107),tptp2)|~(leaf_occ(X107,esk18_0))))&(min_precedes(X106,esk20_2(X106,X107),tptp0)|(occurrence_of(esk19_2(X106,X107),tptp2)|~(leaf_occ(X107,esk18_0))))))&((occurrence_of(X107,tptp2)|(min_precedes(X106,esk19_2(X106,X107),tptp0)|~(leaf_occ(X107,esk18_0))))&((occurrence_of(esk20_2(X106,X107),tptp1)|(min_precedes(X106,esk19_2(X106,X107),tptp0)|~(leaf_occ(X107,esk18_0))))&(min_precedes(X106,esk20_2(X106,X107),tptp0)|(min_precedes(X106,esk19_2(X106,X107),tptp0)|~(leaf_occ(X107,esk18_0))))))))&occurrence_of(esk18_0,tptp0)),inference(distribute,[status(thm)],[244])).
% cnf(246,negated_conjecture,(occurrence_of(esk18_0,tptp0)),inference(split_conjunct,[status(thm)],[245])).
% cnf(247,negated_conjecture,(min_precedes(X2,esk19_2(X2,X1),tptp0)|min_precedes(X2,esk20_2(X2,X1),tptp0)|~leaf_occ(X1,esk18_0)),inference(split_conjunct,[status(thm)],[245])).
% cnf(256,negated_conjecture,(X1=tptp0|~occurrence_of(esk18_0,X1)),inference(spm,[status(thm)],[130,246,theory(equality)])).
% cnf(453,negated_conjecture,(esk17_2(esk18_0,X1)=tptp0|~atocc(esk18_0,X1)),inference(spm,[status(thm)],[256,225,theory(equality)])).
% cnf(563,negated_conjecture,(atomic(tptp0)|~atocc(esk18_0,X1)),inference(spm,[status(thm)],[226,453,theory(equality)])).
% cnf(566,negated_conjecture,(~atocc(esk18_0,X1)),inference(sr,[status(thm)],[563,74,theory(equality)])).
% cnf(570,negated_conjecture,(~min_precedes(esk18_0,X2,X1)),inference(spm,[status(thm)],[566,164,theory(equality)])).
% cnf(577,negated_conjecture,(min_precedes(esk18_0,esk20_2(esk18_0,X1),tptp0)|~leaf_occ(X1,esk18_0)),inference(spm,[status(thm)],[570,247,theory(equality)])).
% cnf(580,negated_conjecture,(~leaf_occ(X1,esk18_0)),inference(sr,[status(thm)],[577,570,theory(equality)])).
% cnf(581,negated_conjecture,(~occurrence_of(esk18_0,tptp0)),inference(spm,[status(thm)],[580,79,theory(equality)])).
% cnf(582,negated_conjecture,($false),inference(rw,[status(thm)],[581,246,theory(equality)])).
% cnf(583,negated_conjecture,($false),inference(cn,[status(thm)],[582,theory(equality)])).
% cnf(584,negated_conjecture,($false),583,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 125
% # ...of these trivial : 0
% # ...subsumed : 7
% # ...remaining for further processing: 118
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 0
% # Backward-rewritten : 0
% # Generated clauses : 277
% # ...of the previous two non-trivial : 248
% # Contextual simplify-reflections : 1
% # Paramodulations : 277
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 118
% # Positive orientable unit clauses: 9
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 12
% # Non-unit-clauses : 97
% # Current number of unprocessed clauses: 215
% # ...number of literals in the above : 690
% # Clause-clause subsumption calls (NU) : 96
% # Rec. Clause-clause subsumption calls : 91
% # Unit Clause-clause subsumption calls : 16
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 0
% # Indexed BW rewrite successes : 0
% # Backwards rewriting index: 106 leaves, 1.57+/-1.259 terms/leaf
% # Paramod-from index: 54 leaves, 1.06+/-0.229 terms/leaf
% # Paramod-into index: 98 leaves, 1.36+/-0.918 terms/leaf
% # -------------------------------------------------
% # User time : 0.028 s
% # System time : 0.003 s
% # Total time : 0.031 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.13 CPU 0.21 WC
% FINAL PrfWatch: 0.13 CPU 0.21 WC
% SZS output end Solution for /tmp/SystemOnTPTP18008/PRO010+2.tptp
%
%------------------------------------------------------------------------------