%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : PRO011+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 : art02.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:56 EST 2010
% Result : Theorem 0.97s
% Output : Solution 0.97s
% 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/SystemOnTPTP14071/PRO011+2.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP14071/PRO011+2.tptp
% SZS output start Solution for /tmp/SystemOnTPTP14071/PRO011+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 14167
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% # Preprocessing time : 0.018 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(8, axiom,~(atomic(tptp0)),file('/tmp/SRASS.s.p', sos_34)).
% fof(9, axiom,![X24]:(occurrence_of(X24,tptp0)=>?[X25]:?[X26]:?[X27]:((((((occurrence_of(X25,tptp3)&root_occ(X25,X24))&occurrence_of(X26,tptp4))&next_subocc(X25,X26,tptp0))&(occurrence_of(X27,tptp1)|occurrence_of(X27,tptp2)))&next_subocc(X26,X27,tptp0))&leaf_occ(X27,X24))),file('/tmp/SRASS.s.p', sos_32)).
% fof(20, axiom,![X50]:![X51]:![X52]:((occurrence_of(X50,X51)&occurrence_of(X50,X52))=>X51=X52),file('/tmp/SRASS.s.p', sos_22)).
% fof(33, axiom,![X74]:![X75]:![X76]:(min_precedes(X75,X76,X74)=>?[X77]:?[X78]:(((subactivity(X77,X74)&subactivity(X78,X74))&atocc(X75,X77))&atocc(X76,X78))),file('/tmp/SRASS.s.p', sos_26)).
% fof(41, axiom,![X89]:![X90]:(atocc(X89,X90)<=>?[X91]:((subactivity(X90,X91)&atomic(X91))&occurrence_of(X89,X91))),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)&subactivity_occurrence(X103,X100))&min_precedes(X101,X103,tptp0)))))&(occurrence_of(X102,tptp2)=>~(?[X104]:((occurrence_of(X104,tptp1)&subactivity_occurrence(X104,X100))&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)&subactivity_occurrence(X103,X100))&min_precedes(X101,X103,tptp0)))))&(occurrence_of(X102,tptp2)=>~(?[X104]:((occurrence_of(X104,tptp1)&subactivity_occurrence(X104,X100))&min_precedes(X101,X104,tptp0))))))),inference(assume_negation,[status(cth)],[46])).
% fof(48, plain,~(atomic(tptp0)),inference(fof_simplification,[status(thm)],[8,theory(equality)])).
% cnf(86,plain,(~atomic(tptp0)),inference(split_conjunct,[status(thm)],[48])).
% fof(87, plain,![X24]:(~(occurrence_of(X24,tptp0))|?[X25]:?[X26]:?[X27]:((((((occurrence_of(X25,tptp3)&root_occ(X25,X24))&occurrence_of(X26,tptp4))&next_subocc(X25,X26,tptp0))&(occurrence_of(X27,tptp1)|occurrence_of(X27,tptp2)))&next_subocc(X26,X27,tptp0))&leaf_occ(X27,X24))),inference(fof_nnf,[status(thm)],[9])).
% fof(88, plain,![X28]:(~(occurrence_of(X28,tptp0))|?[X29]:?[X30]:?[X31]:((((((occurrence_of(X29,tptp3)&root_occ(X29,X28))&occurrence_of(X30,tptp4))&next_subocc(X29,X30,tptp0))&(occurrence_of(X31,tptp1)|occurrence_of(X31,tptp2)))&next_subocc(X30,X31,tptp0))&leaf_occ(X31,X28))),inference(variable_rename,[status(thm)],[87])).
% fof(89, plain,![X28]:(~(occurrence_of(X28,tptp0))|((((((occurrence_of(esk3_1(X28),tptp3)&root_occ(esk3_1(X28),X28))&occurrence_of(esk4_1(X28),tptp4))&next_subocc(esk3_1(X28),esk4_1(X28),tptp0))&(occurrence_of(esk5_1(X28),tptp1)|occurrence_of(esk5_1(X28),tptp2)))&next_subocc(esk4_1(X28),esk5_1(X28),tptp0))&leaf_occ(esk5_1(X28),X28))),inference(skolemize,[status(esa)],[88])).
% fof(90, plain,![X28]:(((((((occurrence_of(esk3_1(X28),tptp3)|~(occurrence_of(X28,tptp0)))&(root_occ(esk3_1(X28),X28)|~(occurrence_of(X28,tptp0))))&(occurrence_of(esk4_1(X28),tptp4)|~(occurrence_of(X28,tptp0))))&(next_subocc(esk3_1(X28),esk4_1(X28),tptp0)|~(occurrence_of(X28,tptp0))))&((occurrence_of(esk5_1(X28),tptp1)|occurrence_of(esk5_1(X28),tptp2))|~(occurrence_of(X28,tptp0))))&(next_subocc(esk4_1(X28),esk5_1(X28),tptp0)|~(occurrence_of(X28,tptp0))))&(leaf_occ(esk5_1(X28),X28)|~(occurrence_of(X28,tptp0)))),inference(distribute,[status(thm)],[89])).
% cnf(91,plain,(leaf_occ(esk5_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[90])).
% fof(139, plain,![X50]:![X51]:![X52]:((~(occurrence_of(X50,X51))|~(occurrence_of(X50,X52)))|X51=X52),inference(fof_nnf,[status(thm)],[20])).
% fof(140, plain,![X53]:![X54]:![X55]:((~(occurrence_of(X53,X54))|~(occurrence_of(X53,X55)))|X54=X55),inference(variable_rename,[status(thm)],[139])).
% cnf(141,plain,(X1=X2|~occurrence_of(X3,X2)|~occurrence_of(X3,X1)),inference(split_conjunct,[status(thm)],[140])).
% fof(182, plain,![X74]:![X75]:![X76]:(~(min_precedes(X75,X76,X74))|?[X77]:?[X78]:(((subactivity(X77,X74)&subactivity(X78,X74))&atocc(X75,X77))&atocc(X76,X78))),inference(fof_nnf,[status(thm)],[33])).
% fof(183, plain,![X79]:![X80]:![X81]:(~(min_precedes(X80,X81,X79))|?[X82]:?[X83]:(((subactivity(X82,X79)&subactivity(X83,X79))&atocc(X80,X82))&atocc(X81,X83))),inference(variable_rename,[status(thm)],[182])).
% fof(184, plain,![X79]:![X80]:![X81]:(~(min_precedes(X80,X81,X79))|(((subactivity(esk13_3(X79,X80,X81),X79)&subactivity(esk14_3(X79,X80,X81),X79))&atocc(X80,esk13_3(X79,X80,X81)))&atocc(X81,esk14_3(X79,X80,X81)))),inference(skolemize,[status(esa)],[183])).
% fof(185, plain,![X79]:![X80]:![X81]:((((subactivity(esk13_3(X79,X80,X81),X79)|~(min_precedes(X80,X81,X79)))&(subactivity(esk14_3(X79,X80,X81),X79)|~(min_precedes(X80,X81,X79))))&(atocc(X80,esk13_3(X79,X80,X81))|~(min_precedes(X80,X81,X79))))&(atocc(X81,esk14_3(X79,X80,X81))|~(min_precedes(X80,X81,X79)))),inference(distribute,[status(thm)],[184])).
% cnf(187,plain,(atocc(X1,esk13_3(X3,X1,X2))|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[185])).
% fof(212, plain,![X89]:![X90]:((~(atocc(X89,X90))|?[X91]:((subactivity(X90,X91)&atomic(X91))&occurrence_of(X89,X91)))&(![X91]:((~(subactivity(X90,X91))|~(atomic(X91)))|~(occurrence_of(X89,X91)))|atocc(X89,X90))),inference(fof_nnf,[status(thm)],[41])).
% fof(213, plain,![X92]:![X93]:((~(atocc(X92,X93))|?[X94]:((subactivity(X93,X94)&atomic(X94))&occurrence_of(X92,X94)))&(![X95]:((~(subactivity(X93,X95))|~(atomic(X95)))|~(occurrence_of(X92,X95)))|atocc(X92,X93))),inference(variable_rename,[status(thm)],[212])).
% fof(214, plain,![X92]:![X93]:((~(atocc(X92,X93))|((subactivity(X93,esk16_2(X92,X93))&atomic(esk16_2(X92,X93)))&occurrence_of(X92,esk16_2(X92,X93))))&(![X95]:((~(subactivity(X93,X95))|~(atomic(X95)))|~(occurrence_of(X92,X95)))|atocc(X92,X93))),inference(skolemize,[status(esa)],[213])).
% fof(215, plain,![X92]:![X93]:![X95]:((((~(subactivity(X93,X95))|~(atomic(X95)))|~(occurrence_of(X92,X95)))|atocc(X92,X93))&(~(atocc(X92,X93))|((subactivity(X93,esk16_2(X92,X93))&atomic(esk16_2(X92,X93)))&occurrence_of(X92,esk16_2(X92,X93))))),inference(shift_quantors,[status(thm)],[214])).
% fof(216, plain,![X92]:![X93]:![X95]:((((~(subactivity(X93,X95))|~(atomic(X95)))|~(occurrence_of(X92,X95)))|atocc(X92,X93))&(((subactivity(X93,esk16_2(X92,X93))|~(atocc(X92,X93)))&(atomic(esk16_2(X92,X93))|~(atocc(X92,X93))))&(occurrence_of(X92,esk16_2(X92,X93))|~(atocc(X92,X93))))),inference(distribute,[status(thm)],[215])).
% cnf(217,plain,(occurrence_of(X1,esk16_2(X1,X2))|~atocc(X1,X2)),inference(split_conjunct,[status(thm)],[216])).
% cnf(218,plain,(atomic(esk16_2(X1,X2))|~atocc(X1,X2)),inference(split_conjunct,[status(thm)],[216])).
% fof(241, negated_conjecture,?[X100]:(occurrence_of(X100,tptp0)&![X101]:![X102]:((~(leaf_occ(X102,X100))|(occurrence_of(X102,tptp1)&?[X103]:((occurrence_of(X103,tptp2)&subactivity_occurrence(X103,X100))&min_precedes(X101,X103,tptp0))))|(occurrence_of(X102,tptp2)&?[X104]:((occurrence_of(X104,tptp1)&subactivity_occurrence(X104,X100))&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)&subactivity_occurrence(X108,X105))&min_precedes(X106,X108,tptp0))))|(occurrence_of(X107,tptp2)&?[X109]:((occurrence_of(X109,tptp1)&subactivity_occurrence(X109,X105))&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)&subactivity_occurrence(esk19_2(X106,X107),esk18_0))&min_precedes(X106,esk19_2(X106,X107),tptp0))))|(occurrence_of(X107,tptp2)&((occurrence_of(esk20_2(X106,X107),tptp1)&subactivity_occurrence(esk20_2(X106,X107),esk18_0))&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)&subactivity_occurrence(esk19_2(X106,X107),esk18_0))&min_precedes(X106,esk19_2(X106,X107),tptp0))))|(occurrence_of(X107,tptp2)&((occurrence_of(esk20_2(X106,X107),tptp1)&subactivity_occurrence(esk20_2(X106,X107),esk18_0))&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))))&(subactivity_occurrence(esk20_2(X106,X107),esk18_0)|(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))))&(subactivity_occurrence(esk20_2(X106,X107),esk18_0)|(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)|(subactivity_occurrence(esk19_2(X106,X107),esk18_0)|~(leaf_occ(X107,esk18_0))))&(((occurrence_of(esk20_2(X106,X107),tptp1)|(subactivity_occurrence(esk19_2(X106,X107),esk18_0)|~(leaf_occ(X107,esk18_0))))&(subactivity_occurrence(esk20_2(X106,X107),esk18_0)|(subactivity_occurrence(esk19_2(X106,X107),esk18_0)|~(leaf_occ(X107,esk18_0)))))&(min_precedes(X106,esk20_2(X106,X107),tptp0)|(subactivity_occurrence(esk19_2(X106,X107),esk18_0)|~(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))))&(subactivity_occurrence(esk20_2(X106,X107),esk18_0)|(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(263,negated_conjecture,(X1=tptp0|~occurrence_of(esk18_0,X1)),inference(spm,[status(thm)],[141,246,theory(equality)])).
% cnf(482,negated_conjecture,(esk16_2(esk18_0,X1)=tptp0|~atocc(esk18_0,X1)),inference(spm,[status(thm)],[263,217,theory(equality)])).
% cnf(614,negated_conjecture,(atomic(tptp0)|~atocc(esk18_0,X1)),inference(spm,[status(thm)],[218,482,theory(equality)])).
% cnf(617,negated_conjecture,(~atocc(esk18_0,X1)),inference(sr,[status(thm)],[614,86,theory(equality)])).
% cnf(621,negated_conjecture,(~min_precedes(esk18_0,X2,X1)),inference(spm,[status(thm)],[617,187,theory(equality)])).
% cnf(628,negated_conjecture,(min_precedes(esk18_0,esk20_2(esk18_0,X1),tptp0)|~leaf_occ(X1,esk18_0)),inference(spm,[status(thm)],[621,247,theory(equality)])).
% cnf(631,negated_conjecture,(~leaf_occ(X1,esk18_0)),inference(sr,[status(thm)],[628,621,theory(equality)])).
% cnf(632,negated_conjecture,(~occurrence_of(esk18_0,tptp0)),inference(spm,[status(thm)],[631,91,theory(equality)])).
% cnf(633,negated_conjecture,($false),inference(rw,[status(thm)],[632,246,theory(equality)])).
% cnf(634,negated_conjecture,($false),inference(cn,[status(thm)],[633,theory(equality)])).
% cnf(635,negated_conjecture,($false),634,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 136
% # ...of these trivial : 0
% # ...subsumed : 9
% # ...remaining for further processing: 127
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 0
% # Backward-rewritten : 0
% # Generated clauses : 307
% # ...of the previous two non-trivial : 272
% # Contextual simplify-reflections : 1
% # Paramodulations : 307
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 127
% # Positive orientable unit clauses: 9
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 12
% # Non-unit-clauses : 106
% # Current number of unprocessed clauses: 235
% # ...number of literals in the above : 787
% # Clause-clause subsumption calls (NU) : 130
% # Rec. Clause-clause subsumption calls : 124
% # Unit Clause-clause subsumption calls : 26
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 0
% # Indexed BW rewrite successes : 0
% # Backwards rewriting index: 109 leaves, 1.56+/-1.245 terms/leaf
% # Paramod-from index: 57 leaves, 1.05+/-0.223 terms/leaf
% # Paramod-into index: 101 leaves, 1.36+/-0.907 terms/leaf
% # -------------------------------------------------
% # User time : 0.029 s
% # System time : 0.004 s
% # Total time : 0.033 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.12 CPU 0.21 WC
% FINAL PrfWatch: 0.12 CPU 0.21 WC
% SZS output end Solution for /tmp/SystemOnTPTP14071/PRO011+2.tptp
%
%------------------------------------------------------------------------------