%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : PRO011+3 : 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:11:09 EST 2010
% Result : Theorem 1.07s
% Output : Solution 1.07s
% 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/SystemOnTPTP18785/PRO011+3.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP18785/PRO011+3.tptp
% SZS output start Solution for /tmp/SystemOnTPTP18785/PRO011+3.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 18881
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.022 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(14, axiom,~(atomic(tptp0)),file('/tmp/SRASS.s.p', sos_51)).
% fof(15, axiom,![X50]:(occurrence_of(X50,tptp0)=>?[X51]:?[X52]:?[X53]:((((((occurrence_of(X51,tptp3)&root_occ(X51,X50))&occurrence_of(X52,tptp4))&next_subocc(X51,X52,tptp0))&(occurrence_of(X53,tptp1)|occurrence_of(X53,tptp2)))&next_subocc(X52,X53,tptp0))&leaf_occ(X53,X50))),file('/tmp/SRASS.s.p', sos_49)).
% fof(22, axiom,![X65]:![X66]:![X67]:((occurrence_of(X65,X66)&occurrence_of(X65,X67))=>X66=X67),file('/tmp/SRASS.s.p', sos_02)).
% fof(48, axiom,![X135]:![X136]:![X137]:(min_precedes(X136,X137,X135)=>?[X138]:?[X139]:(((subactivity(X138,X135)&subactivity(X139,X135))&atocc(X136,X138))&atocc(X137,X139))),file('/tmp/SRASS.s.p', sos_11)).
% fof(56, axiom,![X150]:![X151]:(atocc(X150,X151)<=>?[X152]:((subactivity(X151,X152)&atomic(X152))&occurrence_of(X150,X152))),file('/tmp/SRASS.s.p', sos_23)).
% fof(63, conjecture,![X166]:(occurrence_of(X166,tptp0)=>?[X167]:?[X168]:((leaf_occ(X168,X166)&(occurrence_of(X168,tptp1)=>~(?[X169]:((occurrence_of(X169,tptp2)&subactivity_occurrence(X169,X166))&min_precedes(X167,X169,tptp0)))))&(occurrence_of(X168,tptp2)=>~(?[X170]:((occurrence_of(X170,tptp1)&subactivity_occurrence(X170,X166))&min_precedes(X167,X170,tptp0)))))),file('/tmp/SRASS.s.p', goals)).
% fof(64, negated_conjecture,~(![X166]:(occurrence_of(X166,tptp0)=>?[X167]:?[X168]:((leaf_occ(X168,X166)&(occurrence_of(X168,tptp1)=>~(?[X169]:((occurrence_of(X169,tptp2)&subactivity_occurrence(X169,X166))&min_precedes(X167,X169,tptp0)))))&(occurrence_of(X168,tptp2)=>~(?[X170]:((occurrence_of(X170,tptp1)&subactivity_occurrence(X170,X166))&min_precedes(X167,X170,tptp0))))))),inference(assume_negation,[status(cth)],[63])).
% fof(67, plain,~(atomic(tptp0)),inference(fof_simplification,[status(thm)],[14,theory(equality)])).
% cnf(129,plain,(~atomic(tptp0)),inference(split_conjunct,[status(thm)],[67])).
% fof(130, plain,![X50]:(~(occurrence_of(X50,tptp0))|?[X51]:?[X52]:?[X53]:((((((occurrence_of(X51,tptp3)&root_occ(X51,X50))&occurrence_of(X52,tptp4))&next_subocc(X51,X52,tptp0))&(occurrence_of(X53,tptp1)|occurrence_of(X53,tptp2)))&next_subocc(X52,X53,tptp0))&leaf_occ(X53,X50))),inference(fof_nnf,[status(thm)],[15])).
% fof(131, plain,![X54]:(~(occurrence_of(X54,tptp0))|?[X55]:?[X56]:?[X57]:((((((occurrence_of(X55,tptp3)&root_occ(X55,X54))&occurrence_of(X56,tptp4))&next_subocc(X55,X56,tptp0))&(occurrence_of(X57,tptp1)|occurrence_of(X57,tptp2)))&next_subocc(X56,X57,tptp0))&leaf_occ(X57,X54))),inference(variable_rename,[status(thm)],[130])).
% fof(132, plain,![X54]:(~(occurrence_of(X54,tptp0))|((((((occurrence_of(esk4_1(X54),tptp3)&root_occ(esk4_1(X54),X54))&occurrence_of(esk5_1(X54),tptp4))&next_subocc(esk4_1(X54),esk5_1(X54),tptp0))&(occurrence_of(esk6_1(X54),tptp1)|occurrence_of(esk6_1(X54),tptp2)))&next_subocc(esk5_1(X54),esk6_1(X54),tptp0))&leaf_occ(esk6_1(X54),X54))),inference(skolemize,[status(esa)],[131])).
% fof(133, plain,![X54]:(((((((occurrence_of(esk4_1(X54),tptp3)|~(occurrence_of(X54,tptp0)))&(root_occ(esk4_1(X54),X54)|~(occurrence_of(X54,tptp0))))&(occurrence_of(esk5_1(X54),tptp4)|~(occurrence_of(X54,tptp0))))&(next_subocc(esk4_1(X54),esk5_1(X54),tptp0)|~(occurrence_of(X54,tptp0))))&((occurrence_of(esk6_1(X54),tptp1)|occurrence_of(esk6_1(X54),tptp2))|~(occurrence_of(X54,tptp0))))&(next_subocc(esk5_1(X54),esk6_1(X54),tptp0)|~(occurrence_of(X54,tptp0))))&(leaf_occ(esk6_1(X54),X54)|~(occurrence_of(X54,tptp0)))),inference(distribute,[status(thm)],[132])).
% cnf(134,plain,(leaf_occ(esk6_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[133])).
% fof(153, plain,![X65]:![X66]:![X67]:((~(occurrence_of(X65,X66))|~(occurrence_of(X65,X67)))|X66=X67),inference(fof_nnf,[status(thm)],[22])).
% fof(154, plain,![X68]:![X69]:![X70]:((~(occurrence_of(X68,X69))|~(occurrence_of(X68,X70)))|X69=X70),inference(variable_rename,[status(thm)],[153])).
% cnf(155,plain,(X1=X2|~occurrence_of(X3,X2)|~occurrence_of(X3,X1)),inference(split_conjunct,[status(thm)],[154])).
% fof(255, plain,![X135]:![X136]:![X137]:(~(min_precedes(X136,X137,X135))|?[X138]:?[X139]:(((subactivity(X138,X135)&subactivity(X139,X135))&atocc(X136,X138))&atocc(X137,X139))),inference(fof_nnf,[status(thm)],[48])).
% fof(256, plain,![X140]:![X141]:![X142]:(~(min_precedes(X141,X142,X140))|?[X143]:?[X144]:(((subactivity(X143,X140)&subactivity(X144,X140))&atocc(X141,X143))&atocc(X142,X144))),inference(variable_rename,[status(thm)],[255])).
% fof(257, plain,![X140]:![X141]:![X142]:(~(min_precedes(X141,X142,X140))|(((subactivity(esk15_3(X140,X141,X142),X140)&subactivity(esk16_3(X140,X141,X142),X140))&atocc(X141,esk15_3(X140,X141,X142)))&atocc(X142,esk16_3(X140,X141,X142)))),inference(skolemize,[status(esa)],[256])).
% fof(258, plain,![X140]:![X141]:![X142]:((((subactivity(esk15_3(X140,X141,X142),X140)|~(min_precedes(X141,X142,X140)))&(subactivity(esk16_3(X140,X141,X142),X140)|~(min_precedes(X141,X142,X140))))&(atocc(X141,esk15_3(X140,X141,X142))|~(min_precedes(X141,X142,X140))))&(atocc(X142,esk16_3(X140,X141,X142))|~(min_precedes(X141,X142,X140)))),inference(distribute,[status(thm)],[257])).
% cnf(260,plain,(atocc(X1,esk15_3(X3,X1,X2))|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[258])).
% fof(285, plain,![X150]:![X151]:((~(atocc(X150,X151))|?[X152]:((subactivity(X151,X152)&atomic(X152))&occurrence_of(X150,X152)))&(![X152]:((~(subactivity(X151,X152))|~(atomic(X152)))|~(occurrence_of(X150,X152)))|atocc(X150,X151))),inference(fof_nnf,[status(thm)],[56])).
% fof(286, plain,![X153]:![X154]:((~(atocc(X153,X154))|?[X155]:((subactivity(X154,X155)&atomic(X155))&occurrence_of(X153,X155)))&(![X156]:((~(subactivity(X154,X156))|~(atomic(X156)))|~(occurrence_of(X153,X156)))|atocc(X153,X154))),inference(variable_rename,[status(thm)],[285])).
% fof(287, plain,![X153]:![X154]:((~(atocc(X153,X154))|((subactivity(X154,esk18_2(X153,X154))&atomic(esk18_2(X153,X154)))&occurrence_of(X153,esk18_2(X153,X154))))&(![X156]:((~(subactivity(X154,X156))|~(atomic(X156)))|~(occurrence_of(X153,X156)))|atocc(X153,X154))),inference(skolemize,[status(esa)],[286])).
% fof(288, plain,![X153]:![X154]:![X156]:((((~(subactivity(X154,X156))|~(atomic(X156)))|~(occurrence_of(X153,X156)))|atocc(X153,X154))&(~(atocc(X153,X154))|((subactivity(X154,esk18_2(X153,X154))&atomic(esk18_2(X153,X154)))&occurrence_of(X153,esk18_2(X153,X154))))),inference(shift_quantors,[status(thm)],[287])).
% fof(289, plain,![X153]:![X154]:![X156]:((((~(subactivity(X154,X156))|~(atomic(X156)))|~(occurrence_of(X153,X156)))|atocc(X153,X154))&(((subactivity(X154,esk18_2(X153,X154))|~(atocc(X153,X154)))&(atomic(esk18_2(X153,X154))|~(atocc(X153,X154))))&(occurrence_of(X153,esk18_2(X153,X154))|~(atocc(X153,X154))))),inference(distribute,[status(thm)],[288])).
% cnf(290,plain,(occurrence_of(X1,esk18_2(X1,X2))|~atocc(X1,X2)),inference(split_conjunct,[status(thm)],[289])).
% cnf(291,plain,(atomic(esk18_2(X1,X2))|~atocc(X1,X2)),inference(split_conjunct,[status(thm)],[289])).
% fof(320, negated_conjecture,?[X166]:(occurrence_of(X166,tptp0)&![X167]:![X168]:((~(leaf_occ(X168,X166))|(occurrence_of(X168,tptp1)&?[X169]:((occurrence_of(X169,tptp2)&subactivity_occurrence(X169,X166))&min_precedes(X167,X169,tptp0))))|(occurrence_of(X168,tptp2)&?[X170]:((occurrence_of(X170,tptp1)&subactivity_occurrence(X170,X166))&min_precedes(X167,X170,tptp0))))),inference(fof_nnf,[status(thm)],[64])).
% fof(321, negated_conjecture,?[X171]:(occurrence_of(X171,tptp0)&![X172]:![X173]:((~(leaf_occ(X173,X171))|(occurrence_of(X173,tptp1)&?[X174]:((occurrence_of(X174,tptp2)&subactivity_occurrence(X174,X171))&min_precedes(X172,X174,tptp0))))|(occurrence_of(X173,tptp2)&?[X175]:((occurrence_of(X175,tptp1)&subactivity_occurrence(X175,X171))&min_precedes(X172,X175,tptp0))))),inference(variable_rename,[status(thm)],[320])).
% fof(322, negated_conjecture,(occurrence_of(esk20_0,tptp0)&![X172]:![X173]:((~(leaf_occ(X173,esk20_0))|(occurrence_of(X173,tptp1)&((occurrence_of(esk21_2(X172,X173),tptp2)&subactivity_occurrence(esk21_2(X172,X173),esk20_0))&min_precedes(X172,esk21_2(X172,X173),tptp0))))|(occurrence_of(X173,tptp2)&((occurrence_of(esk22_2(X172,X173),tptp1)&subactivity_occurrence(esk22_2(X172,X173),esk20_0))&min_precedes(X172,esk22_2(X172,X173),tptp0))))),inference(skolemize,[status(esa)],[321])).
% fof(323, negated_conjecture,![X172]:![X173]:(((~(leaf_occ(X173,esk20_0))|(occurrence_of(X173,tptp1)&((occurrence_of(esk21_2(X172,X173),tptp2)&subactivity_occurrence(esk21_2(X172,X173),esk20_0))&min_precedes(X172,esk21_2(X172,X173),tptp0))))|(occurrence_of(X173,tptp2)&((occurrence_of(esk22_2(X172,X173),tptp1)&subactivity_occurrence(esk22_2(X172,X173),esk20_0))&min_precedes(X172,esk22_2(X172,X173),tptp0))))&occurrence_of(esk20_0,tptp0)),inference(shift_quantors,[status(thm)],[322])).
% fof(324, negated_conjecture,![X172]:![X173]:((((occurrence_of(X173,tptp2)|(occurrence_of(X173,tptp1)|~(leaf_occ(X173,esk20_0))))&(((occurrence_of(esk22_2(X172,X173),tptp1)|(occurrence_of(X173,tptp1)|~(leaf_occ(X173,esk20_0))))&(subactivity_occurrence(esk22_2(X172,X173),esk20_0)|(occurrence_of(X173,tptp1)|~(leaf_occ(X173,esk20_0)))))&(min_precedes(X172,esk22_2(X172,X173),tptp0)|(occurrence_of(X173,tptp1)|~(leaf_occ(X173,esk20_0))))))&((((occurrence_of(X173,tptp2)|(occurrence_of(esk21_2(X172,X173),tptp2)|~(leaf_occ(X173,esk20_0))))&(((occurrence_of(esk22_2(X172,X173),tptp1)|(occurrence_of(esk21_2(X172,X173),tptp2)|~(leaf_occ(X173,esk20_0))))&(subactivity_occurrence(esk22_2(X172,X173),esk20_0)|(occurrence_of(esk21_2(X172,X173),tptp2)|~(leaf_occ(X173,esk20_0)))))&(min_precedes(X172,esk22_2(X172,X173),tptp0)|(occurrence_of(esk21_2(X172,X173),tptp2)|~(leaf_occ(X173,esk20_0))))))&((occurrence_of(X173,tptp2)|(subactivity_occurrence(esk21_2(X172,X173),esk20_0)|~(leaf_occ(X173,esk20_0))))&(((occurrence_of(esk22_2(X172,X173),tptp1)|(subactivity_occurrence(esk21_2(X172,X173),esk20_0)|~(leaf_occ(X173,esk20_0))))&(subactivity_occurrence(esk22_2(X172,X173),esk20_0)|(subactivity_occurrence(esk21_2(X172,X173),esk20_0)|~(leaf_occ(X173,esk20_0)))))&(min_precedes(X172,esk22_2(X172,X173),tptp0)|(subactivity_occurrence(esk21_2(X172,X173),esk20_0)|~(leaf_occ(X173,esk20_0)))))))&((occurrence_of(X173,tptp2)|(min_precedes(X172,esk21_2(X172,X173),tptp0)|~(leaf_occ(X173,esk20_0))))&(((occurrence_of(esk22_2(X172,X173),tptp1)|(min_precedes(X172,esk21_2(X172,X173),tptp0)|~(leaf_occ(X173,esk20_0))))&(subactivity_occurrence(esk22_2(X172,X173),esk20_0)|(min_precedes(X172,esk21_2(X172,X173),tptp0)|~(leaf_occ(X173,esk20_0)))))&(min_precedes(X172,esk22_2(X172,X173),tptp0)|(min_precedes(X172,esk21_2(X172,X173),tptp0)|~(leaf_occ(X173,esk20_0))))))))&occurrence_of(esk20_0,tptp0)),inference(distribute,[status(thm)],[323])).
% cnf(325,negated_conjecture,(occurrence_of(esk20_0,tptp0)),inference(split_conjunct,[status(thm)],[324])).
% cnf(326,negated_conjecture,(min_precedes(X2,esk21_2(X2,X1),tptp0)|min_precedes(X2,esk22_2(X2,X1),tptp0)|~leaf_occ(X1,esk20_0)),inference(split_conjunct,[status(thm)],[324])).
% cnf(342,negated_conjecture,(X1=tptp0|~occurrence_of(esk20_0,X1)),inference(spm,[status(thm)],[155,325,theory(equality)])).
% cnf(663,negated_conjecture,(esk18_2(esk20_0,X1)=tptp0|~atocc(esk20_0,X1)),inference(spm,[status(thm)],[342,290,theory(equality)])).
% cnf(790,negated_conjecture,(atomic(tptp0)|~atocc(esk20_0,X1)),inference(spm,[status(thm)],[291,663,theory(equality)])).
% cnf(793,negated_conjecture,(~atocc(esk20_0,X1)),inference(sr,[status(thm)],[790,129,theory(equality)])).
% cnf(797,negated_conjecture,(~min_precedes(esk20_0,X2,X1)),inference(spm,[status(thm)],[793,260,theory(equality)])).
% cnf(805,negated_conjecture,(min_precedes(esk20_0,esk22_2(esk20_0,X1),tptp0)|~leaf_occ(X1,esk20_0)),inference(spm,[status(thm)],[797,326,theory(equality)])).
% cnf(808,negated_conjecture,(~leaf_occ(X1,esk20_0)),inference(sr,[status(thm)],[805,797,theory(equality)])).
% cnf(809,negated_conjecture,(~occurrence_of(esk20_0,tptp0)),inference(spm,[status(thm)],[808,134,theory(equality)])).
% cnf(810,negated_conjecture,($false),inference(rw,[status(thm)],[809,325,theory(equality)])).
% cnf(811,negated_conjecture,($false),inference(cn,[status(thm)],[810,theory(equality)])).
% cnf(812,negated_conjecture,($false),811,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 160
% # ...of these trivial : 0
% # ...subsumed : 13
% # ...remaining for further processing: 147
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 0
% # Backward-rewritten : 0
% # Generated clauses : 415
% # ...of the previous two non-trivial : 386
% # Contextual simplify-reflections : 1
% # Paramodulations : 415
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 147
% # Positive orientable unit clauses: 9
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 12
% # Non-unit-clauses : 126
% # Current number of unprocessed clauses: 344
% # ...number of literals in the above : 1336
% # Clause-clause subsumption calls (NU) : 306
% # Rec. Clause-clause subsumption calls : 223
% # Unit Clause-clause subsumption calls : 25
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 0
% # Indexed BW rewrite successes : 0
% # Backwards rewriting index: 117 leaves, 1.75+/-1.849 terms/leaf
% # Paramod-from index: 60 leaves, 1.05+/-0.218 terms/leaf
% # Paramod-into index: 109 leaves, 1.46+/-1.216 terms/leaf
% # -------------------------------------------------
% # User time : 0.036 s
% # System time : 0.007 s
% # Total time : 0.043 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.14 CPU 0.23 WC
% FINAL PrfWatch: 0.14 CPU 0.23 WC
% SZS output end Solution for /tmp/SystemOnTPTP18785/PRO011+3.tptp
%
%------------------------------------------------------------------------------