%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : PRO012+4 : 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:12:10 EST 2010
% Result : Theorem 1.28s
% Output : Solution 1.28s
% 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/SystemOnTPTP14589/PRO012+4.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP14589/PRO012+4.tptp
% SZS output start Solution for /tmp/SystemOnTPTP14589/PRO012+4.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 14685
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.019 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(2, axiom,![X5]:(occurrence_of(X5,tptp0)=>?[X6]:?[X7]:?[X8]:((((((occurrence_of(X6,tptp3)&root_occ(X6,X5))&occurrence_of(X7,tptp4))&min_precedes(X6,X7,tptp0))&(occurrence_of(X8,tptp2)|occurrence_of(X8,tptp1)))&min_precedes(X7,X8,tptp0))&![X9]:(min_precedes(X6,X9,tptp0)=>(X9=X7|X9=X8)))),file('/tmp/SRASS.s.p', sos_32)).
% fof(6, axiom,![X10]:![X11]:![X12]:![X13]:(((occurrence_of(X12,X13)&root_occ(X10,X12))&root_occ(X11,X12))=>X10=X11),file('/tmp/SRASS.s.p', sos_29)).
% fof(7, axiom,![X14]:![X15]:![X16]:(min_precedes(X15,X16,X14)=>?[X17]:((occurrence_of(X17,X14)&subactivity_occurrence(X15,X17))&subactivity_occurrence(X16,X17))),file('/tmp/SRASS.s.p', sos_06)).
% fof(8, axiom,![X18]:![X19]:![X20]:![X21]:(((min_precedes(X18,X19,X20)&occurrence_of(X21,X20))&subactivity_occurrence(X19,X21))=>subactivity_occurrence(X18,X21)),file('/tmp/SRASS.s.p', sos_27)).
% fof(10, axiom,~(atomic(tptp0)),file('/tmp/SRASS.s.p', sos_34)).
% fof(14, axiom,![X26]:![X27]:![X28]:((occurrence_of(X26,X27)&occurrence_of(X26,X28))=>X27=X28),file('/tmp/SRASS.s.p', sos_08)).
% fof(20, axiom,![X34]:![X35]:(root_occ(X34,X35)<=>?[X36]:((occurrence_of(X35,X36)&subactivity_occurrence(X34,X35))&root(X34,X36))),file('/tmp/SRASS.s.p', sos_19)).
% fof(22, axiom,![X40]:![X41]:![X42]:(min_precedes(X40,X41,X42)=>?[X43]:(root(X43,X42)&min_precedes(X43,X41,X42))),file('/tmp/SRASS.s.p', sos_23)).
% fof(27, axiom,![X59]:![X60]:((occurrence_of(X60,X59)&~(atomic(X59)))=>?[X61]:(root(X61,X59)&subactivity_occurrence(X61,X60))),file('/tmp/SRASS.s.p', sos)).
% fof(40, axiom,![X94]:![X95]:(occurrence_of(X95,X94)=>(activity(X94)&activity_occurrence(X95))),file('/tmp/SRASS.s.p', sos_03)).
% fof(41, axiom,![X96]:(activity_occurrence(X96)=>?[X97]:(activity(X97)&occurrence_of(X96,X97))),file('/tmp/SRASS.s.p', sos_12)).
% fof(46, conjecture,![X107]:(occurrence_of(X107,tptp0)=>?[X108]:?[X109]:(((occurrence_of(X108,tptp3)&root_occ(X108,X107))&(occurrence_of(X109,tptp2)|occurrence_of(X109,tptp1)))&min_precedes(X108,X109,tptp0))),file('/tmp/SRASS.s.p', goals)).
% fof(47, negated_conjecture,~(![X107]:(occurrence_of(X107,tptp0)=>?[X108]:?[X109]:(((occurrence_of(X108,tptp3)&root_occ(X108,X107))&(occurrence_of(X109,tptp2)|occurrence_of(X109,tptp1)))&min_precedes(X108,X109,tptp0)))),inference(assume_negation,[status(cth)],[46])).
% fof(48, plain,~(atomic(tptp0)),inference(fof_simplification,[status(thm)],[10,theory(equality)])).
% fof(51, plain,![X59]:![X60]:((occurrence_of(X60,X59)&~(atomic(X59)))=>?[X61]:(root(X61,X59)&subactivity_occurrence(X61,X60))),inference(fof_simplification,[status(thm)],[27,theory(equality)])).
% fof(59, plain,![X5]:(~(occurrence_of(X5,tptp0))|?[X6]:?[X7]:?[X8]:((((((occurrence_of(X6,tptp3)&root_occ(X6,X5))&occurrence_of(X7,tptp4))&min_precedes(X6,X7,tptp0))&(occurrence_of(X8,tptp2)|occurrence_of(X8,tptp1)))&min_precedes(X7,X8,tptp0))&![X9]:(~(min_precedes(X6,X9,tptp0))|(X9=X7|X9=X8)))),inference(fof_nnf,[status(thm)],[2])).
% fof(60, plain,![X10]:(~(occurrence_of(X10,tptp0))|?[X11]:?[X12]:?[X13]:((((((occurrence_of(X11,tptp3)&root_occ(X11,X10))&occurrence_of(X12,tptp4))&min_precedes(X11,X12,tptp0))&(occurrence_of(X13,tptp2)|occurrence_of(X13,tptp1)))&min_precedes(X12,X13,tptp0))&![X14]:(~(min_precedes(X11,X14,tptp0))|(X14=X12|X14=X13)))),inference(variable_rename,[status(thm)],[59])).
% fof(61, plain,![X10]:(~(occurrence_of(X10,tptp0))|((((((occurrence_of(esk1_1(X10),tptp3)&root_occ(esk1_1(X10),X10))&occurrence_of(esk2_1(X10),tptp4))&min_precedes(esk1_1(X10),esk2_1(X10),tptp0))&(occurrence_of(esk3_1(X10),tptp2)|occurrence_of(esk3_1(X10),tptp1)))&min_precedes(esk2_1(X10),esk3_1(X10),tptp0))&![X14]:(~(min_precedes(esk1_1(X10),X14,tptp0))|(X14=esk2_1(X10)|X14=esk3_1(X10))))),inference(skolemize,[status(esa)],[60])).
% fof(62, plain,![X10]:![X14]:(((~(min_precedes(esk1_1(X10),X14,tptp0))|(X14=esk2_1(X10)|X14=esk3_1(X10)))&(((((occurrence_of(esk1_1(X10),tptp3)&root_occ(esk1_1(X10),X10))&occurrence_of(esk2_1(X10),tptp4))&min_precedes(esk1_1(X10),esk2_1(X10),tptp0))&(occurrence_of(esk3_1(X10),tptp2)|occurrence_of(esk3_1(X10),tptp1)))&min_precedes(esk2_1(X10),esk3_1(X10),tptp0)))|~(occurrence_of(X10,tptp0))),inference(shift_quantors,[status(thm)],[61])).
% fof(63, plain,![X10]:![X14]:(((~(min_precedes(esk1_1(X10),X14,tptp0))|(X14=esk2_1(X10)|X14=esk3_1(X10)))|~(occurrence_of(X10,tptp0)))&((((((occurrence_of(esk1_1(X10),tptp3)|~(occurrence_of(X10,tptp0)))&(root_occ(esk1_1(X10),X10)|~(occurrence_of(X10,tptp0))))&(occurrence_of(esk2_1(X10),tptp4)|~(occurrence_of(X10,tptp0))))&(min_precedes(esk1_1(X10),esk2_1(X10),tptp0)|~(occurrence_of(X10,tptp0))))&((occurrence_of(esk3_1(X10),tptp2)|occurrence_of(esk3_1(X10),tptp1))|~(occurrence_of(X10,tptp0))))&(min_precedes(esk2_1(X10),esk3_1(X10),tptp0)|~(occurrence_of(X10,tptp0))))),inference(distribute,[status(thm)],[62])).
% cnf(64,plain,(min_precedes(esk2_1(X1),esk3_1(X1),tptp0)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[63])).
% cnf(65,plain,(occurrence_of(esk3_1(X1),tptp1)|occurrence_of(esk3_1(X1),tptp2)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[63])).
% cnf(66,plain,(min_precedes(esk1_1(X1),esk2_1(X1),tptp0)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[63])).
% cnf(68,plain,(root_occ(esk1_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[63])).
% cnf(69,plain,(occurrence_of(esk1_1(X1),tptp3)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[63])).
% fof(74, plain,![X10]:![X11]:![X12]:![X13]:(((~(occurrence_of(X12,X13))|~(root_occ(X10,X12)))|~(root_occ(X11,X12)))|X10=X11),inference(fof_nnf,[status(thm)],[6])).
% fof(75, plain,![X14]:![X15]:![X16]:![X17]:(((~(occurrence_of(X16,X17))|~(root_occ(X14,X16)))|~(root_occ(X15,X16)))|X14=X15),inference(variable_rename,[status(thm)],[74])).
% cnf(76,plain,(X1=X2|~root_occ(X2,X3)|~root_occ(X1,X3)|~occurrence_of(X3,X4)),inference(split_conjunct,[status(thm)],[75])).
% fof(77, plain,![X14]:![X15]:![X16]:(~(min_precedes(X15,X16,X14))|?[X17]:((occurrence_of(X17,X14)&subactivity_occurrence(X15,X17))&subactivity_occurrence(X16,X17))),inference(fof_nnf,[status(thm)],[7])).
% fof(78, plain,![X18]:![X19]:![X20]:(~(min_precedes(X19,X20,X18))|?[X21]:((occurrence_of(X21,X18)&subactivity_occurrence(X19,X21))&subactivity_occurrence(X20,X21))),inference(variable_rename,[status(thm)],[77])).
% fof(79, plain,![X18]:![X19]:![X20]:(~(min_precedes(X19,X20,X18))|((occurrence_of(esk4_3(X18,X19,X20),X18)&subactivity_occurrence(X19,esk4_3(X18,X19,X20)))&subactivity_occurrence(X20,esk4_3(X18,X19,X20)))),inference(skolemize,[status(esa)],[78])).
% fof(80, plain,![X18]:![X19]:![X20]:(((occurrence_of(esk4_3(X18,X19,X20),X18)|~(min_precedes(X19,X20,X18)))&(subactivity_occurrence(X19,esk4_3(X18,X19,X20))|~(min_precedes(X19,X20,X18))))&(subactivity_occurrence(X20,esk4_3(X18,X19,X20))|~(min_precedes(X19,X20,X18)))),inference(distribute,[status(thm)],[79])).
% cnf(81,plain,(subactivity_occurrence(X2,esk4_3(X3,X1,X2))|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[80])).
% cnf(82,plain,(subactivity_occurrence(X1,esk4_3(X3,X1,X2))|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[80])).
% cnf(83,plain,(occurrence_of(esk4_3(X3,X1,X2),X3)|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[80])).
% fof(84, plain,![X18]:![X19]:![X20]:![X21]:(((~(min_precedes(X18,X19,X20))|~(occurrence_of(X21,X20)))|~(subactivity_occurrence(X19,X21)))|subactivity_occurrence(X18,X21)),inference(fof_nnf,[status(thm)],[8])).
% fof(85, plain,![X22]:![X23]:![X24]:![X25]:(((~(min_precedes(X22,X23,X24))|~(occurrence_of(X25,X24)))|~(subactivity_occurrence(X23,X25)))|subactivity_occurrence(X22,X25)),inference(variable_rename,[status(thm)],[84])).
% cnf(86,plain,(subactivity_occurrence(X1,X2)|~subactivity_occurrence(X3,X2)|~occurrence_of(X2,X4)|~min_precedes(X1,X3,X4)),inference(split_conjunct,[status(thm)],[85])).
% cnf(91,plain,(~atomic(tptp0)),inference(split_conjunct,[status(thm)],[48])).
% fof(95, plain,![X26]:![X27]:![X28]:((~(occurrence_of(X26,X27))|~(occurrence_of(X26,X28)))|X27=X28),inference(fof_nnf,[status(thm)],[14])).
% fof(96, plain,![X29]:![X30]:![X31]:((~(occurrence_of(X29,X30))|~(occurrence_of(X29,X31)))|X30=X31),inference(variable_rename,[status(thm)],[95])).
% cnf(97,plain,(X1=X2|~occurrence_of(X3,X2)|~occurrence_of(X3,X1)),inference(split_conjunct,[status(thm)],[96])).
% fof(105, plain,![X34]:![X35]:((~(root_occ(X34,X35))|?[X36]:((occurrence_of(X35,X36)&subactivity_occurrence(X34,X35))&root(X34,X36)))&(![X36]:((~(occurrence_of(X35,X36))|~(subactivity_occurrence(X34,X35)))|~(root(X34,X36)))|root_occ(X34,X35))),inference(fof_nnf,[status(thm)],[20])).
% fof(106, plain,![X37]:![X38]:((~(root_occ(X37,X38))|?[X39]:((occurrence_of(X38,X39)&subactivity_occurrence(X37,X38))&root(X37,X39)))&(![X40]:((~(occurrence_of(X38,X40))|~(subactivity_occurrence(X37,X38)))|~(root(X37,X40)))|root_occ(X37,X38))),inference(variable_rename,[status(thm)],[105])).
% fof(107, plain,![X37]:![X38]:((~(root_occ(X37,X38))|((occurrence_of(X38,esk5_2(X37,X38))&subactivity_occurrence(X37,X38))&root(X37,esk5_2(X37,X38))))&(![X40]:((~(occurrence_of(X38,X40))|~(subactivity_occurrence(X37,X38)))|~(root(X37,X40)))|root_occ(X37,X38))),inference(skolemize,[status(esa)],[106])).
% fof(108, plain,![X37]:![X38]:![X40]:((((~(occurrence_of(X38,X40))|~(subactivity_occurrence(X37,X38)))|~(root(X37,X40)))|root_occ(X37,X38))&(~(root_occ(X37,X38))|((occurrence_of(X38,esk5_2(X37,X38))&subactivity_occurrence(X37,X38))&root(X37,esk5_2(X37,X38))))),inference(shift_quantors,[status(thm)],[107])).
% fof(109, plain,![X37]:![X38]:![X40]:((((~(occurrence_of(X38,X40))|~(subactivity_occurrence(X37,X38)))|~(root(X37,X40)))|root_occ(X37,X38))&(((occurrence_of(X38,esk5_2(X37,X38))|~(root_occ(X37,X38)))&(subactivity_occurrence(X37,X38)|~(root_occ(X37,X38))))&(root(X37,esk5_2(X37,X38))|~(root_occ(X37,X38))))),inference(distribute,[status(thm)],[108])).
% cnf(113,plain,(root_occ(X1,X2)|~root(X1,X3)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,X3)),inference(split_conjunct,[status(thm)],[109])).
% fof(117, plain,![X40]:![X41]:![X42]:(~(min_precedes(X40,X41,X42))|?[X43]:(root(X43,X42)&min_precedes(X43,X41,X42))),inference(fof_nnf,[status(thm)],[22])).
% fof(118, plain,![X44]:![X45]:![X46]:(~(min_precedes(X44,X45,X46))|?[X47]:(root(X47,X46)&min_precedes(X47,X45,X46))),inference(variable_rename,[status(thm)],[117])).
% fof(119, plain,![X44]:![X45]:![X46]:(~(min_precedes(X44,X45,X46))|(root(esk6_3(X44,X45,X46),X46)&min_precedes(esk6_3(X44,X45,X46),X45,X46))),inference(skolemize,[status(esa)],[118])).
% fof(120, plain,![X44]:![X45]:![X46]:((root(esk6_3(X44,X45,X46),X46)|~(min_precedes(X44,X45,X46)))&(min_precedes(esk6_3(X44,X45,X46),X45,X46)|~(min_precedes(X44,X45,X46)))),inference(distribute,[status(thm)],[119])).
% cnf(121,plain,(min_precedes(esk6_3(X1,X2,X3),X2,X3)|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[120])).
% cnf(122,plain,(root(esk6_3(X1,X2,X3),X3)|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[120])).
% fof(141, plain,![X59]:![X60]:((~(occurrence_of(X60,X59))|atomic(X59))|?[X61]:(root(X61,X59)&subactivity_occurrence(X61,X60))),inference(fof_nnf,[status(thm)],[51])).
% fof(142, plain,![X62]:![X63]:((~(occurrence_of(X63,X62))|atomic(X62))|?[X64]:(root(X64,X62)&subactivity_occurrence(X64,X63))),inference(variable_rename,[status(thm)],[141])).
% fof(143, plain,![X62]:![X63]:((~(occurrence_of(X63,X62))|atomic(X62))|(root(esk8_2(X62,X63),X62)&subactivity_occurrence(esk8_2(X62,X63),X63))),inference(skolemize,[status(esa)],[142])).
% fof(144, plain,![X62]:![X63]:((root(esk8_2(X62,X63),X62)|(~(occurrence_of(X63,X62))|atomic(X62)))&(subactivity_occurrence(esk8_2(X62,X63),X63)|(~(occurrence_of(X63,X62))|atomic(X62)))),inference(distribute,[status(thm)],[143])).
% cnf(145,plain,(atomic(X1)|subactivity_occurrence(esk8_2(X1,X2),X2)|~occurrence_of(X2,X1)),inference(split_conjunct,[status(thm)],[144])).
% cnf(146,plain,(atomic(X1)|root(esk8_2(X1,X2),X1)|~occurrence_of(X2,X1)),inference(split_conjunct,[status(thm)],[144])).
% fof(202, plain,![X94]:![X95]:(~(occurrence_of(X95,X94))|(activity(X94)&activity_occurrence(X95))),inference(fof_nnf,[status(thm)],[40])).
% fof(203, plain,![X96]:![X97]:(~(occurrence_of(X97,X96))|(activity(X96)&activity_occurrence(X97))),inference(variable_rename,[status(thm)],[202])).
% fof(204, plain,![X96]:![X97]:((activity(X96)|~(occurrence_of(X97,X96)))&(activity_occurrence(X97)|~(occurrence_of(X97,X96)))),inference(distribute,[status(thm)],[203])).
% cnf(205,plain,(activity_occurrence(X1)|~occurrence_of(X1,X2)),inference(split_conjunct,[status(thm)],[204])).
% fof(207, plain,![X96]:(~(activity_occurrence(X96))|?[X97]:(activity(X97)&occurrence_of(X96,X97))),inference(fof_nnf,[status(thm)],[41])).
% fof(208, plain,![X98]:(~(activity_occurrence(X98))|?[X99]:(activity(X99)&occurrence_of(X98,X99))),inference(variable_rename,[status(thm)],[207])).
% fof(209, plain,![X98]:(~(activity_occurrence(X98))|(activity(esk13_1(X98))&occurrence_of(X98,esk13_1(X98)))),inference(skolemize,[status(esa)],[208])).
% fof(210, plain,![X98]:((activity(esk13_1(X98))|~(activity_occurrence(X98)))&(occurrence_of(X98,esk13_1(X98))|~(activity_occurrence(X98)))),inference(distribute,[status(thm)],[209])).
% cnf(211,plain,(occurrence_of(X1,esk13_1(X1))|~activity_occurrence(X1)),inference(split_conjunct,[status(thm)],[210])).
% fof(237, negated_conjecture,?[X107]:(occurrence_of(X107,tptp0)&![X108]:![X109]:(((~(occurrence_of(X108,tptp3))|~(root_occ(X108,X107)))|(~(occurrence_of(X109,tptp2))&~(occurrence_of(X109,tptp1))))|~(min_precedes(X108,X109,tptp0)))),inference(fof_nnf,[status(thm)],[47])).
% fof(238, negated_conjecture,?[X110]:(occurrence_of(X110,tptp0)&![X111]:![X112]:(((~(occurrence_of(X111,tptp3))|~(root_occ(X111,X110)))|(~(occurrence_of(X112,tptp2))&~(occurrence_of(X112,tptp1))))|~(min_precedes(X111,X112,tptp0)))),inference(variable_rename,[status(thm)],[237])).
% fof(239, negated_conjecture,(occurrence_of(esk16_0,tptp0)&![X111]:![X112]:(((~(occurrence_of(X111,tptp3))|~(root_occ(X111,esk16_0)))|(~(occurrence_of(X112,tptp2))&~(occurrence_of(X112,tptp1))))|~(min_precedes(X111,X112,tptp0)))),inference(skolemize,[status(esa)],[238])).
% fof(240, negated_conjecture,![X111]:![X112]:((((~(occurrence_of(X111,tptp3))|~(root_occ(X111,esk16_0)))|(~(occurrence_of(X112,tptp2))&~(occurrence_of(X112,tptp1))))|~(min_precedes(X111,X112,tptp0)))&occurrence_of(esk16_0,tptp0)),inference(shift_quantors,[status(thm)],[239])).
% fof(241, negated_conjecture,![X111]:![X112]:((((~(occurrence_of(X112,tptp2))|(~(occurrence_of(X111,tptp3))|~(root_occ(X111,esk16_0))))|~(min_precedes(X111,X112,tptp0)))&((~(occurrence_of(X112,tptp1))|(~(occurrence_of(X111,tptp3))|~(root_occ(X111,esk16_0))))|~(min_precedes(X111,X112,tptp0))))&occurrence_of(esk16_0,tptp0)),inference(distribute,[status(thm)],[240])).
% cnf(242,negated_conjecture,(occurrence_of(esk16_0,tptp0)),inference(split_conjunct,[status(thm)],[241])).
% cnf(243,negated_conjecture,(~min_precedes(X1,X2,tptp0)|~root_occ(X1,esk16_0)|~occurrence_of(X1,tptp3)|~occurrence_of(X2,tptp1)),inference(split_conjunct,[status(thm)],[241])).
% cnf(244,negated_conjecture,(~min_precedes(X1,X2,tptp0)|~root_occ(X1,esk16_0)|~occurrence_of(X1,tptp3)|~occurrence_of(X2,tptp2)),inference(split_conjunct,[status(thm)],[241])).
% cnf(248,negated_conjecture,(occurrence_of(esk1_1(esk16_0),tptp3)),inference(spm,[status(thm)],[69,242,theory(equality)])).
% cnf(250,negated_conjecture,(root_occ(esk1_1(esk16_0),esk16_0)),inference(spm,[status(thm)],[68,242,theory(equality)])).
% cnf(251,negated_conjecture,(activity_occurrence(esk16_0)),inference(spm,[status(thm)],[205,242,theory(equality)])).
% cnf(259,plain,(X1=esk13_1(X2)|~occurrence_of(X2,X1)|~activity_occurrence(X2)),inference(spm,[status(thm)],[97,211,theory(equality)])).
% cnf(260,negated_conjecture,(min_precedes(esk1_1(esk16_0),esk2_1(esk16_0),tptp0)),inference(spm,[status(thm)],[66,242,theory(equality)])).
% cnf(261,negated_conjecture,(min_precedes(esk2_1(esk16_0),esk3_1(esk16_0),tptp0)),inference(spm,[status(thm)],[64,242,theory(equality)])).
% cnf(262,negated_conjecture,(occurrence_of(esk3_1(esk16_0),tptp1)|occurrence_of(esk3_1(esk16_0),tptp2)),inference(spm,[status(thm)],[65,242,theory(equality)])).
% cnf(263,negated_conjecture,(atomic(tptp0)|subactivity_occurrence(esk8_2(tptp0,esk16_0),esk16_0)),inference(spm,[status(thm)],[145,242,theory(equality)])).
% cnf(264,plain,(atomic(esk13_1(X1))|subactivity_occurrence(esk8_2(esk13_1(X1),X1),X1)|~activity_occurrence(X1)),inference(spm,[status(thm)],[145,211,theory(equality)])).
% cnf(265,negated_conjecture,(subactivity_occurrence(esk8_2(tptp0,esk16_0),esk16_0)),inference(sr,[status(thm)],[263,91,theory(equality)])).
% cnf(266,negated_conjecture,(root(esk8_2(tptp0,esk16_0),tptp0)|atomic(tptp0)),inference(spm,[status(thm)],[146,242,theory(equality)])).
% cnf(267,plain,(root(esk8_2(esk13_1(X1),X1),esk13_1(X1))|atomic(esk13_1(X1))|~activity_occurrence(X1)),inference(spm,[status(thm)],[146,211,theory(equality)])).
% cnf(268,negated_conjecture,(root(esk8_2(tptp0,esk16_0),tptp0)),inference(sr,[status(thm)],[266,91,theory(equality)])).
% cnf(289,plain,(X1=esk13_1(X2)|~occurrence_of(X2,X1)),inference(csr,[status(thm)],[259,205])).
% cnf(344,negated_conjecture,(X1=esk1_1(esk16_0)|~root_occ(X1,esk16_0)|~occurrence_of(esk16_0,X2)),inference(spm,[status(thm)],[76,250,theory(equality)])).
% cnf(346,negated_conjecture,(~min_precedes(esk1_1(esk16_0),X1,tptp0)|~occurrence_of(X1,tptp2)|~occurrence_of(esk1_1(esk16_0),tptp3)),inference(spm,[status(thm)],[244,250,theory(equality)])).
% cnf(347,negated_conjecture,(~min_precedes(esk1_1(esk16_0),X1,tptp0)|~occurrence_of(X1,tptp1)|~occurrence_of(esk1_1(esk16_0),tptp3)),inference(spm,[status(thm)],[243,250,theory(equality)])).
% cnf(348,negated_conjecture,(~min_precedes(esk1_1(esk16_0),X1,tptp0)|~occurrence_of(X1,tptp2)|$false),inference(rw,[status(thm)],[346,248,theory(equality)])).
% cnf(349,negated_conjecture,(~min_precedes(esk1_1(esk16_0),X1,tptp0)|~occurrence_of(X1,tptp2)),inference(cn,[status(thm)],[348,theory(equality)])).
% cnf(350,negated_conjecture,(~min_precedes(esk1_1(esk16_0),X1,tptp0)|~occurrence_of(X1,tptp1)|$false),inference(rw,[status(thm)],[347,248,theory(equality)])).
% cnf(351,negated_conjecture,(~min_precedes(esk1_1(esk16_0),X1,tptp0)|~occurrence_of(X1,tptp1)),inference(cn,[status(thm)],[350,theory(equality)])).
% cnf(384,negated_conjecture,(root_occ(esk8_2(tptp0,esk16_0),X1)|~subactivity_occurrence(esk8_2(tptp0,esk16_0),X1)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[113,268,theory(equality)])).
% cnf(391,negated_conjecture,(root_occ(esk8_2(tptp0,esk16_0),esk16_0)|~subactivity_occurrence(esk8_2(tptp0,esk16_0),esk16_0)),inference(spm,[status(thm)],[384,242,theory(equality)])).
% cnf(392,negated_conjecture,(root_occ(esk8_2(tptp0,esk16_0),esk16_0)|$false),inference(rw,[status(thm)],[391,265,theory(equality)])).
% cnf(393,negated_conjecture,(root_occ(esk8_2(tptp0,esk16_0),esk16_0)),inference(cn,[status(thm)],[392,theory(equality)])).
% cnf(400,negated_conjecture,(esk8_2(tptp0,esk16_0)=esk1_1(esk16_0)|~occurrence_of(esk16_0,X1)),inference(spm,[status(thm)],[344,393,theory(equality)])).
% cnf(402,negated_conjecture,(esk8_2(tptp0,esk16_0)=esk1_1(esk16_0)|~activity_occurrence(esk16_0)),inference(spm,[status(thm)],[400,211,theory(equality)])).
% cnf(404,negated_conjecture,(esk8_2(tptp0,esk16_0)=esk1_1(esk16_0)|$false),inference(rw,[status(thm)],[402,251,theory(equality)])).
% cnf(405,negated_conjecture,(esk8_2(tptp0,esk16_0)=esk1_1(esk16_0)),inference(cn,[status(thm)],[404,theory(equality)])).
% cnf(410,negated_conjecture,(root_occ(esk1_1(esk16_0),X1)|~subactivity_occurrence(esk8_2(tptp0,esk16_0),X1)|~occurrence_of(X1,tptp0)),inference(rw,[status(thm)],[384,405,theory(equality)])).
% cnf(411,negated_conjecture,(root_occ(esk1_1(esk16_0),X1)|~subactivity_occurrence(esk1_1(esk16_0),X1)|~occurrence_of(X1,tptp0)),inference(rw,[status(thm)],[410,405,theory(equality)])).
% cnf(437,negated_conjecture,(subactivity_occurrence(esk1_1(esk16_0),X1)|~subactivity_occurrence(esk2_1(esk16_0),X1)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[86,260,theory(equality)])).
% cnf(443,negated_conjecture,(root(esk6_3(esk2_1(esk16_0),esk3_1(esk16_0),tptp0),tptp0)),inference(spm,[status(thm)],[122,261,theory(equality)])).
% cnf(444,negated_conjecture,(min_precedes(esk6_3(esk2_1(esk16_0),esk3_1(esk16_0),tptp0),esk3_1(esk16_0),tptp0)),inference(spm,[status(thm)],[121,261,theory(equality)])).
% cnf(449,negated_conjecture,(subactivity_occurrence(esk3_1(esk16_0),esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))),inference(spm,[status(thm)],[81,261,theory(equality)])).
% cnf(451,negated_conjecture,(subactivity_occurrence(esk2_1(esk16_0),esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))),inference(spm,[status(thm)],[82,261,theory(equality)])).
% cnf(455,negated_conjecture,(occurrence_of(esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)),tptp0)),inference(spm,[status(thm)],[83,261,theory(equality)])).
% cnf(499,negated_conjecture,(occurrence_of(esk3_1(esk16_0),tptp2)|~min_precedes(esk1_1(esk16_0),esk3_1(esk16_0),tptp0)),inference(spm,[status(thm)],[351,262,theory(equality)])).
% cnf(567,negated_conjecture,(~min_precedes(esk1_1(esk16_0),esk3_1(esk16_0),tptp0)),inference(csr,[status(thm)],[499,349])).
% cnf(669,plain,(root_occ(esk8_2(esk13_1(X1),X1),X2)|atomic(esk13_1(X1))|~subactivity_occurrence(esk8_2(esk13_1(X1),X1),X2)|~occurrence_of(X2,esk13_1(X1))|~activity_occurrence(X1)),inference(spm,[status(thm)],[113,267,theory(equality)])).
% cnf(800,plain,(atomic(esk13_1(X1))|root_occ(esk8_2(esk13_1(X1),X1),X1)|~activity_occurrence(X1)|~subactivity_occurrence(esk8_2(esk13_1(X1),X1),X1)),inference(spm,[status(thm)],[669,211,theory(equality)])).
% cnf(818,plain,(atomic(esk13_1(X1))|root_occ(esk8_2(esk13_1(X1),X1),X1)|~activity_occurrence(X1)),inference(csr,[status(thm)],[800,264])).
% cnf(824,plain,(X1=esk8_2(esk13_1(X2),X2)|atomic(esk13_1(X2))|~root_occ(X1,X2)|~occurrence_of(X2,X3)|~activity_occurrence(X2)),inference(spm,[status(thm)],[76,818,theory(equality)])).
% cnf(862,plain,(X1=esk8_2(esk13_1(X2),X2)|atomic(esk13_1(X2))|~root_occ(X1,X2)|~occurrence_of(X2,X3)),inference(csr,[status(thm)],[824,205])).
% cnf(973,negated_conjecture,(root_occ(esk6_3(esk2_1(esk16_0),esk3_1(esk16_0),tptp0),X1)|~subactivity_occurrence(esk6_3(esk2_1(esk16_0),esk3_1(esk16_0),tptp0),X1)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[113,443,theory(equality)])).
% cnf(994,negated_conjecture,(activity_occurrence(esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))),inference(spm,[status(thm)],[205,455,theory(equality)])).
% cnf(1001,negated_conjecture,(tptp0=esk13_1(esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))),inference(spm,[status(thm)],[289,455,theory(equality)])).
% cnf(1009,negated_conjecture,(root_occ(esk1_1(esk16_0),esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))|~subactivity_occurrence(esk1_1(esk16_0),esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))),inference(spm,[status(thm)],[411,455,theory(equality)])).
% cnf(1012,negated_conjecture,(subactivity_occurrence(esk1_1(esk16_0),esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))|~subactivity_occurrence(esk2_1(esk16_0),esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))),inference(spm,[status(thm)],[437,455,theory(equality)])).
% cnf(1036,negated_conjecture,(root_occ(esk6_3(esk2_1(esk16_0),esk3_1(esk16_0),tptp0),esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))|~subactivity_occurrence(esk6_3(esk2_1(esk16_0),esk3_1(esk16_0),tptp0),esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))),inference(spm,[status(thm)],[973,455,theory(equality)])).
% cnf(1246,negated_conjecture,(subactivity_occurrence(esk6_3(esk2_1(esk16_0),esk3_1(esk16_0),tptp0),X1)|~subactivity_occurrence(esk3_1(esk16_0),X1)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[86,444,theory(equality)])).
% cnf(1275,negated_conjecture,(subactivity_occurrence(esk6_3(esk2_1(esk16_0),esk3_1(esk16_0),tptp0),esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))|~subactivity_occurrence(esk3_1(esk16_0),esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))),inference(spm,[status(thm)],[1246,455,theory(equality)])).
% cnf(1277,negated_conjecture,(subactivity_occurrence(esk6_3(esk2_1(esk16_0),esk3_1(esk16_0),tptp0),esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))|$false),inference(rw,[status(thm)],[1275,449,theory(equality)])).
% cnf(1278,negated_conjecture,(subactivity_occurrence(esk6_3(esk2_1(esk16_0),esk3_1(esk16_0),tptp0),esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))),inference(cn,[status(thm)],[1277,theory(equality)])).
% cnf(2034,negated_conjecture,(subactivity_occurrence(esk1_1(esk16_0),esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))|$false),inference(rw,[status(thm)],[1012,451,theory(equality)])).
% cnf(2035,negated_conjecture,(subactivity_occurrence(esk1_1(esk16_0),esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))),inference(cn,[status(thm)],[2034,theory(equality)])).
% cnf(2039,negated_conjecture,(root_occ(esk1_1(esk16_0),esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))|$false),inference(rw,[status(thm)],[1009,2035,theory(equality)])).
% cnf(2040,negated_conjecture,(root_occ(esk1_1(esk16_0),esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))),inference(cn,[status(thm)],[2039,theory(equality)])).
% cnf(2047,negated_conjecture,(esk1_1(esk16_0)=esk8_2(esk13_1(esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0))),esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))|atomic(esk13_1(esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0))))|~occurrence_of(esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)),X1)),inference(spm,[status(thm)],[862,2040,theory(equality)])).
% cnf(2051,negated_conjecture,(esk1_1(esk16_0)=esk8_2(tptp0,esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))|atomic(esk13_1(esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0))))|~occurrence_of(esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)),X1)),inference(rw,[status(thm)],[2047,1001,theory(equality)])).
% cnf(2052,negated_conjecture,(esk1_1(esk16_0)=esk8_2(tptp0,esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))|atomic(tptp0)|~occurrence_of(esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)),X1)),inference(rw,[status(thm)],[2051,1001,theory(equality)])).
% cnf(2053,negated_conjecture,(esk8_2(tptp0,esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))=esk1_1(esk16_0)|~occurrence_of(esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)),X1)),inference(sr,[status(thm)],[2052,91,theory(equality)])).
% cnf(3116,negated_conjecture,(esk8_2(tptp0,esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))=esk1_1(esk16_0)|~activity_occurrence(esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))),inference(spm,[status(thm)],[2053,211,theory(equality)])).
% cnf(3118,negated_conjecture,(esk8_2(tptp0,esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))=esk1_1(esk16_0)|$false),inference(rw,[status(thm)],[3116,994,theory(equality)])).
% cnf(3119,negated_conjecture,(esk8_2(tptp0,esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))=esk1_1(esk16_0)),inference(cn,[status(thm)],[3118,theory(equality)])).
% cnf(7712,negated_conjecture,(root_occ(esk6_3(esk2_1(esk16_0),esk3_1(esk16_0),tptp0),esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))|$false),inference(rw,[status(thm)],[1036,1278,theory(equality)])).
% cnf(7713,negated_conjecture,(root_occ(esk6_3(esk2_1(esk16_0),esk3_1(esk16_0),tptp0),esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))),inference(cn,[status(thm)],[7712,theory(equality)])).
% cnf(7716,negated_conjecture,(esk6_3(esk2_1(esk16_0),esk3_1(esk16_0),tptp0)=esk8_2(esk13_1(esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0))),esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))|atomic(esk13_1(esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0))))|~occurrence_of(esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)),X1)),inference(spm,[status(thm)],[862,7713,theory(equality)])).
% cnf(7723,negated_conjecture,(esk6_3(esk2_1(esk16_0),esk3_1(esk16_0),tptp0)=esk1_1(esk16_0)|atomic(esk13_1(esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0))))|~occurrence_of(esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)),X1)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[7716,1001,theory(equality)]),3119,theory(equality)])).
% cnf(7724,negated_conjecture,(esk6_3(esk2_1(esk16_0),esk3_1(esk16_0),tptp0)=esk1_1(esk16_0)|atomic(tptp0)|~occurrence_of(esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)),X1)),inference(rw,[status(thm)],[7723,1001,theory(equality)])).
% cnf(7725,negated_conjecture,(esk6_3(esk2_1(esk16_0),esk3_1(esk16_0),tptp0)=esk1_1(esk16_0)|~occurrence_of(esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)),X1)),inference(sr,[status(thm)],[7724,91,theory(equality)])).
% cnf(7726,negated_conjecture,(esk6_3(esk2_1(esk16_0),esk3_1(esk16_0),tptp0)=esk1_1(esk16_0)|~activity_occurrence(esk4_3(tptp0,esk2_1(esk16_0),esk3_1(esk16_0)))),inference(spm,[status(thm)],[7725,211,theory(equality)])).
% cnf(7729,negated_conjecture,(esk6_3(esk2_1(esk16_0),esk3_1(esk16_0),tptp0)=esk1_1(esk16_0)|$false),inference(rw,[status(thm)],[7726,994,theory(equality)])).
% cnf(7730,negated_conjecture,(esk6_3(esk2_1(esk16_0),esk3_1(esk16_0),tptp0)=esk1_1(esk16_0)),inference(cn,[status(thm)],[7729,theory(equality)])).
% cnf(7861,negated_conjecture,(min_precedes(esk1_1(esk16_0),esk3_1(esk16_0),tptp0)),inference(rw,[status(thm)],[444,7730,theory(equality)])).
% cnf(7862,negated_conjecture,($false),inference(sr,[status(thm)],[7861,567,theory(equality)])).
% cnf(7863,negated_conjecture,($false),7862,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 1395
% # ...of these trivial : 56
% # ...subsumed : 337
% # ...remaining for further processing: 1002
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 7
% # Backward-rewritten : 428
% # Generated clauses : 3314
% # ...of the previous two non-trivial : 2487
% # Contextual simplify-reflections : 54
% # Paramodulations : 3311
% # Factorizations : 3
% # Equation resolutions : 0
% # Current number of processed clauses: 567
% # Positive orientable unit clauses: 141
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 99
% # Non-unit-clauses : 327
% # Current number of unprocessed clauses: 498
% # ...number of literals in the above : 1225
% # Clause-clause subsumption calls (NU) : 4406
% # Rec. Clause-clause subsumption calls : 3177
% # Unit Clause-clause subsumption calls : 2188
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 183
% # Indexed BW rewrite successes : 22
% # Backwards rewriting index: 477 leaves, 1.41+/-0.957 terms/leaf
% # Paramod-from index: 169 leaves, 1.26+/-0.664 terms/leaf
% # Paramod-into index: 363 leaves, 1.40+/-0.821 terms/leaf
% # -------------------------------------------------
% # User time : 0.244 s
% # System time : 0.010 s
% # Total time : 0.254 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.42 CPU 0.51 WC
% FINAL PrfWatch: 0.42 CPU 0.51 WC
% SZS output end Solution for /tmp/SystemOnTPTP14589/PRO012+4.tptp
%
%------------------------------------------------------------------------------