%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : PRO010+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:10:14 EST 2010
% Result : Theorem 1.06s
% Output : Solution 1.06s
% 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/SystemOnTPTP18267/PRO010+3.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP18267/PRO010+3.tptp
% SZS output start Solution for /tmp/SystemOnTPTP18267/PRO010+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 18363
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.021 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(7, axiom,~(atomic(tptp0)),file('/tmp/SRASS.s.p', sos_51)).
% fof(8, axiom,![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))),file('/tmp/SRASS.s.p', sos_49)).
% fof(19, axiom,![X52]:![X53]:![X54]:((occurrence_of(X52,X53)&occurrence_of(X52,X54))=>X53=X54),file('/tmp/SRASS.s.p', sos_02)).
% fof(43, axiom,![X118]:![X119]:![X120]:(min_precedes(X119,X120,X118)=>?[X121]:?[X122]:(((subactivity(X121,X118)&subactivity(X122,X118))&atocc(X119,X121))&atocc(X120,X122))),file('/tmp/SRASS.s.p', sos_11)).
% fof(58, axiom,![X155]:![X156]:(atocc(X155,X156)<=>?[X157]:((subactivity(X156,X157)&atomic(X157))&occurrence_of(X155,X157))),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)&min_precedes(X167,X169,tptp0)))))&(occurrence_of(X168,tptp2)=>~(?[X170]:(occurrence_of(X170,tptp1)&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)&min_precedes(X167,X169,tptp0)))))&(occurrence_of(X168,tptp2)=>~(?[X170]:(occurrence_of(X170,tptp1)&min_precedes(X167,X170,tptp0))))))),inference(assume_negation,[status(cth)],[63])).
% fof(65, plain,~(atomic(tptp0)),inference(fof_simplification,[status(thm)],[7,theory(equality)])).
% cnf(99,plain,(~atomic(tptp0)),inference(split_conjunct,[status(thm)],[65])).
% fof(100, 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(fof_nnf,[status(thm)],[8])).
% fof(101, plain,![X25]:(~(occurrence_of(X25,tptp0))|?[X26]:?[X27]:?[X28]:((((((occurrence_of(X26,tptp3)&root_occ(X26,X25))&occurrence_of(X27,tptp4))&next_subocc(X26,X27,tptp0))&(occurrence_of(X28,tptp1)|occurrence_of(X28,tptp2)))&next_subocc(X27,X28,tptp0))&leaf_occ(X28,X25))),inference(variable_rename,[status(thm)],[100])).
% fof(102, plain,![X25]:(~(occurrence_of(X25,tptp0))|((((((occurrence_of(esk2_1(X25),tptp3)&root_occ(esk2_1(X25),X25))&occurrence_of(esk3_1(X25),tptp4))&next_subocc(esk2_1(X25),esk3_1(X25),tptp0))&(occurrence_of(esk4_1(X25),tptp1)|occurrence_of(esk4_1(X25),tptp2)))&next_subocc(esk3_1(X25),esk4_1(X25),tptp0))&leaf_occ(esk4_1(X25),X25))),inference(skolemize,[status(esa)],[101])).
% fof(103, plain,![X25]:(((((((occurrence_of(esk2_1(X25),tptp3)|~(occurrence_of(X25,tptp0)))&(root_occ(esk2_1(X25),X25)|~(occurrence_of(X25,tptp0))))&(occurrence_of(esk3_1(X25),tptp4)|~(occurrence_of(X25,tptp0))))&(next_subocc(esk2_1(X25),esk3_1(X25),tptp0)|~(occurrence_of(X25,tptp0))))&((occurrence_of(esk4_1(X25),tptp1)|occurrence_of(esk4_1(X25),tptp2))|~(occurrence_of(X25,tptp0))))&(next_subocc(esk3_1(X25),esk4_1(X25),tptp0)|~(occurrence_of(X25,tptp0))))&(leaf_occ(esk4_1(X25),X25)|~(occurrence_of(X25,tptp0)))),inference(distribute,[status(thm)],[102])).
% cnf(104,plain,(leaf_occ(esk4_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[103])).
% fof(141, plain,![X52]:![X53]:![X54]:((~(occurrence_of(X52,X53))|~(occurrence_of(X52,X54)))|X53=X54),inference(fof_nnf,[status(thm)],[19])).
% fof(142, plain,![X55]:![X56]:![X57]:((~(occurrence_of(X55,X56))|~(occurrence_of(X55,X57)))|X56=X57),inference(variable_rename,[status(thm)],[141])).
% cnf(143,plain,(X1=X2|~occurrence_of(X3,X2)|~occurrence_of(X3,X1)),inference(split_conjunct,[status(thm)],[142])).
% fof(232, plain,![X118]:![X119]:![X120]:(~(min_precedes(X119,X120,X118))|?[X121]:?[X122]:(((subactivity(X121,X118)&subactivity(X122,X118))&atocc(X119,X121))&atocc(X120,X122))),inference(fof_nnf,[status(thm)],[43])).
% fof(233, plain,![X123]:![X124]:![X125]:(~(min_precedes(X124,X125,X123))|?[X126]:?[X127]:(((subactivity(X126,X123)&subactivity(X127,X123))&atocc(X124,X126))&atocc(X125,X127))),inference(variable_rename,[status(thm)],[232])).
% fof(234, plain,![X123]:![X124]:![X125]:(~(min_precedes(X124,X125,X123))|(((subactivity(esk13_3(X123,X124,X125),X123)&subactivity(esk14_3(X123,X124,X125),X123))&atocc(X124,esk13_3(X123,X124,X125)))&atocc(X125,esk14_3(X123,X124,X125)))),inference(skolemize,[status(esa)],[233])).
% fof(235, plain,![X123]:![X124]:![X125]:((((subactivity(esk13_3(X123,X124,X125),X123)|~(min_precedes(X124,X125,X123)))&(subactivity(esk14_3(X123,X124,X125),X123)|~(min_precedes(X124,X125,X123))))&(atocc(X124,esk13_3(X123,X124,X125))|~(min_precedes(X124,X125,X123))))&(atocc(X125,esk14_3(X123,X124,X125))|~(min_precedes(X124,X125,X123)))),inference(distribute,[status(thm)],[234])).
% cnf(237,plain,(atocc(X1,esk13_3(X3,X1,X2))|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[235])).
% fof(291, plain,![X155]:![X156]:((~(atocc(X155,X156))|?[X157]:((subactivity(X156,X157)&atomic(X157))&occurrence_of(X155,X157)))&(![X157]:((~(subactivity(X156,X157))|~(atomic(X157)))|~(occurrence_of(X155,X157)))|atocc(X155,X156))),inference(fof_nnf,[status(thm)],[58])).
% fof(292, plain,![X158]:![X159]:((~(atocc(X158,X159))|?[X160]:((subactivity(X159,X160)&atomic(X160))&occurrence_of(X158,X160)))&(![X161]:((~(subactivity(X159,X161))|~(atomic(X161)))|~(occurrence_of(X158,X161)))|atocc(X158,X159))),inference(variable_rename,[status(thm)],[291])).
% fof(293, plain,![X158]:![X159]:((~(atocc(X158,X159))|((subactivity(X159,esk18_2(X158,X159))&atomic(esk18_2(X158,X159)))&occurrence_of(X158,esk18_2(X158,X159))))&(![X161]:((~(subactivity(X159,X161))|~(atomic(X161)))|~(occurrence_of(X158,X161)))|atocc(X158,X159))),inference(skolemize,[status(esa)],[292])).
% fof(294, plain,![X158]:![X159]:![X161]:((((~(subactivity(X159,X161))|~(atomic(X161)))|~(occurrence_of(X158,X161)))|atocc(X158,X159))&(~(atocc(X158,X159))|((subactivity(X159,esk18_2(X158,X159))&atomic(esk18_2(X158,X159)))&occurrence_of(X158,esk18_2(X158,X159))))),inference(shift_quantors,[status(thm)],[293])).
% fof(295, plain,![X158]:![X159]:![X161]:((((~(subactivity(X159,X161))|~(atomic(X161)))|~(occurrence_of(X158,X161)))|atocc(X158,X159))&(((subactivity(X159,esk18_2(X158,X159))|~(atocc(X158,X159)))&(atomic(esk18_2(X158,X159))|~(atocc(X158,X159))))&(occurrence_of(X158,esk18_2(X158,X159))|~(atocc(X158,X159))))),inference(distribute,[status(thm)],[294])).
% cnf(296,plain,(occurrence_of(X1,esk18_2(X1,X2))|~atocc(X1,X2)),inference(split_conjunct,[status(thm)],[295])).
% cnf(297,plain,(atomic(esk18_2(X1,X2))|~atocc(X1,X2)),inference(split_conjunct,[status(thm)],[295])).
% fof(320, negated_conjecture,?[X166]:(occurrence_of(X166,tptp0)&![X167]:![X168]:((~(leaf_occ(X168,X166))|(occurrence_of(X168,tptp1)&?[X169]:(occurrence_of(X169,tptp2)&min_precedes(X167,X169,tptp0))))|(occurrence_of(X168,tptp2)&?[X170]:(occurrence_of(X170,tptp1)&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)&min_precedes(X172,X174,tptp0))))|(occurrence_of(X173,tptp2)&?[X175]:(occurrence_of(X175,tptp1)&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)&min_precedes(X172,esk21_2(X172,X173),tptp0))))|(occurrence_of(X173,tptp2)&(occurrence_of(esk22_2(X172,X173),tptp1)&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)&min_precedes(X172,esk21_2(X172,X173),tptp0))))|(occurrence_of(X173,tptp2)&(occurrence_of(esk22_2(X172,X173),tptp1)&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))))&(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))))&(min_precedes(X172,esk22_2(X172,X173),tptp0)|(occurrence_of(esk21_2(X172,X173),tptp2)|~(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))))&(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(335,negated_conjecture,(X1=tptp0|~occurrence_of(esk20_0,X1)),inference(spm,[status(thm)],[143,325,theory(equality)])).
% cnf(628,negated_conjecture,(esk18_2(esk20_0,X1)=tptp0|~atocc(esk20_0,X1)),inference(spm,[status(thm)],[335,296,theory(equality)])).
% cnf(728,negated_conjecture,(atomic(tptp0)|~atocc(esk20_0,X1)),inference(spm,[status(thm)],[297,628,theory(equality)])).
% cnf(731,negated_conjecture,(~atocc(esk20_0,X1)),inference(sr,[status(thm)],[728,99,theory(equality)])).
% cnf(750,negated_conjecture,(~min_precedes(esk20_0,X2,X1)),inference(spm,[status(thm)],[731,237,theory(equality)])).
% cnf(758,negated_conjecture,(min_precedes(esk20_0,esk22_2(esk20_0,X1),tptp0)|~leaf_occ(X1,esk20_0)),inference(spm,[status(thm)],[750,326,theory(equality)])).
% cnf(761,negated_conjecture,(~leaf_occ(X1,esk20_0)),inference(sr,[status(thm)],[758,750,theory(equality)])).
% cnf(762,negated_conjecture,(~occurrence_of(esk20_0,tptp0)),inference(spm,[status(thm)],[761,104,theory(equality)])).
% cnf(763,negated_conjecture,($false),inference(rw,[status(thm)],[762,325,theory(equality)])).
% cnf(764,negated_conjecture,($false),inference(cn,[status(thm)],[763,theory(equality)])).
% cnf(765,negated_conjecture,($false),764,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 148
% # ...of these trivial : 0
% # ...subsumed : 11
% # ...remaining for further processing: 137
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 0
% # Backward-rewritten : 0
% # Generated clauses : 379
% # ...of the previous two non-trivial : 350
% # Contextual simplify-reflections : 1
% # Paramodulations : 379
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 137
% # Positive orientable unit clauses: 9
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 12
% # Non-unit-clauses : 116
% # Current number of unprocessed clauses: 313
% # ...number of literals in the above : 1195
% # Clause-clause subsumption calls (NU) : 270
% # Rec. Clause-clause subsumption calls : 188
% # 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: 112 leaves, 1.73+/-1.941 terms/leaf
% # Paramod-from index: 57 leaves, 1.02+/-0.131 terms/leaf
% # Paramod-into index: 104 leaves, 1.40+/-1.221 terms/leaf
% # -------------------------------------------------
% # User time : 0.035 s
% # System time : 0.004 s
% # Total time : 0.039 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.14 CPU 0.22 WC
% FINAL PrfWatch: 0.14 CPU 0.22 WC
% SZS output end Solution for /tmp/SystemOnTPTP18267/PRO010+3.tptp
%
%------------------------------------------------------------------------------