%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : PRO003+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 : art09.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 20:58:47 EST 2010
% Result : Theorem 21.75s
% Output : Solution 21.75s
% 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/SystemOnTPTP4980/PRO003+3.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP4980/PRO003+3.tptp
% SZS output start Solution for /tmp/SystemOnTPTP4980/PRO003+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 5076
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% PrfWatch: 1.92 CPU 2.01 WC
% PrfWatch: 3.91 CPU 4.01 WC
% PrfWatch: 5.91 CPU 6.02 WC
% PrfWatch: 7.90 CPU 8.02 WC
% PrfWatch: 9.89 CPU 10.03 WC
% PrfWatch: 11.89 CPU 12.03 WC
% PrfWatch: 13.87 CPU 14.04 WC
% PrfWatch: 15.49 CPU 16.04 WC
% # Preprocessing time : 0.021 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 17.13 CPU 18.05 WC
% PrfWatch: 19.12 CPU 20.05 WC
% # SZS output start CNFRefutation.
% fof(1, axiom,~(atomic(tptp0)),file('/tmp/SRASS.s.p', sos_51)).
% fof(3, axiom,![X1]:![X2]:![X3]:((occurrence_of(X1,X2)&occurrence_of(X1,X3))=>X2=X3),file('/tmp/SRASS.s.p', sos_02)).
% fof(4, axiom,![X4]:![X5]:((occurrence_of(X5,tptp0)&root_occ(X4,X5))=>?[X6]:(occurrence_of(X6,tptp1)&next_subocc(X4,X6,tptp0))),file('/tmp/SRASS.s.p', sos_62)).
% fof(7, axiom,![X12]:![X13]:![X14]:((subactivity_occurrence(X12,X13)&subactivity_occurrence(X13,X14))=>subactivity_occurrence(X12,X14)),file('/tmp/SRASS.s.p', sos_31)).
% fof(8, axiom,![X15]:![X16]:![X17]:![X18]:(((occurrence_of(X17,X18)&root_occ(X15,X17))&root_occ(X16,X17))=>X15=X16),file('/tmp/SRASS.s.p', sos_35)).
% fof(9, axiom,![X19]:![X20]:![X21]:(min_precedes(X20,X21,X19)=>?[X22]:((occurrence_of(X22,X19)&subactivity_occurrence(X20,X22))&subactivity_occurrence(X21,X22))),file('/tmp/SRASS.s.p', sos_25)).
% fof(11, axiom,![X27]:![X28]:![X29]:(next_subocc(X27,X28,X29)<=>(min_precedes(X27,X28,X29)&~(?[X30]:(min_precedes(X27,X30,X29)&min_precedes(X30,X28,X29))))),file('/tmp/SRASS.s.p', sos_22)).
% fof(15, axiom,![X42]:![X43]:![X44]:![X45]:((((occurrence_of(X44,X42)&occurrence_of(X45,X43))&subactivity(X42,X43))&~(subactivity_occurrence(X44,X45)))=>?[X46]:(subactivity_occurrence(X46,X45)&~(subactivity_occurrence(X46,X44)))),file('/tmp/SRASS.s.p', sos_32)).
% fof(16, axiom,![X47]:(activity(X47)=>subactivity(X47,X47)),file('/tmp/SRASS.s.p', sos_03)).
% fof(17, axiom,![X48]:![X49]:(occurrence_of(X48,X49)=>(arboreal(X48)<=>atomic(X49))),file('/tmp/SRASS.s.p', sos_07)).
% fof(19, axiom,![X53]:(occurrence_of(X53,tptp0)=>?[X54]:?[X55]:((((occurrence_of(X54,tptp4)&root_occ(X54,X53))&occurrence_of(X55,tptp3))&leaf_occ(X55,X53))&next_subocc(X54,X55,tptp0))),file('/tmp/SRASS.s.p', sos_49)).
% fof(20, axiom,![X56]:![X57]:(root_occ(X56,X57)<=>?[X58]:((occurrence_of(X57,X58)&subactivity_occurrence(X56,X57))&root(X56,X58))),file('/tmp/SRASS.s.p', sos_33)).
% fof(21, axiom,![X59]:![X60]:((leaf(X59,X60)&~(atomic(X60)))=>?[X61]:(occurrence_of(X61,X60)&leaf_occ(X59,X61))),file('/tmp/SRASS.s.p', sos_45)).
% fof(27, axiom,![X65]:![X66]:![X67]:![X68]:((((occurrence_of(X67,X68)&~(atomic(X68)))&leaf_occ(X65,X67))&leaf_occ(X66,X67))=>X65=X66),file('/tmp/SRASS.s.p', sos_36)).
% fof(30, axiom,![X78]:![X79]:(occurrence_of(X79,X78)=>(activity(X78)&activity_occurrence(X79))),file('/tmp/SRASS.s.p', sos)).
% fof(31, axiom,![X80]:(activity_occurrence(X80)=>?[X81]:(activity(X81)&occurrence_of(X80,X81))),file('/tmp/SRASS.s.p', sos_01)).
% fof(35, axiom,~(tptp1=tptp3),file('/tmp/SRASS.s.p', sos_59)).
% fof(42, axiom,![X100]:![X101]:![X102]:![X103]:(((((occurrence_of(X101,X100)&subactivity_occurrence(X102,X101))&root_occ(X103,X101))&arboreal(X102))&~(min_precedes(X103,X102,X100)))=>X103=X102),file('/tmp/SRASS.s.p', sos_42)).
% fof(46, axiom,![X118]:![X119]:![X120]:(min_precedes(X118,X119,X120)=>~(root(X119,X120))),file('/tmp/SRASS.s.p', sos_14)).
% fof(47, axiom,![X121]:![X122]:(subactivity_occurrence(X121,X122)=>(activity_occurrence(X121)&activity_occurrence(X122))),file('/tmp/SRASS.s.p', sos_24)).
% fof(49, axiom,![X126]:![X127]:((occurrence_of(X127,X126)&~(atomic(X126)))=>?[X128]:(root(X128,X126)&subactivity_occurrence(X128,X127))),file('/tmp/SRASS.s.p', sos_27)).
% fof(51, axiom,![X133]:![X134]:(leaf_occ(X133,X134)<=>?[X135]:((occurrence_of(X134,X135)&subactivity_occurrence(X133,X134))&leaf(X133,X135))),file('/tmp/SRASS.s.p', sos_34)).
% fof(52, axiom,![X136]:![X137]:![X138]:![X139]:(((((occurrence_of(X137,X136)&subactivity_occurrence(X138,X137))&leaf_occ(X139,X137))&arboreal(X138))&~(min_precedes(X138,X139,X136)))=>X139=X138),file('/tmp/SRASS.s.p', sos_43)).
% fof(53, axiom,![X140]:![X141]:![X142]:(min_precedes(X141,X142,X140)=>?[X143]:?[X144]:(((subactivity(X143,X140)&subactivity(X144,X140))&atocc(X141,X143))&atocc(X142,X144))),file('/tmp/SRASS.s.p', sos_11)).
% fof(58, axiom,![X160]:![X161]:(atocc(X160,X161)<=>?[X162]:((subactivity(X161,X162)&atomic(X162))&occurrence_of(X160,X162))),file('/tmp/SRASS.s.p', sos_23)).
% fof(64, conjecture,~(?[X168]:occurrence_of(X168,tptp0)),file('/tmp/SRASS.s.p', goals)).
% fof(65, negated_conjecture,~(~(?[X168]:occurrence_of(X168,tptp0))),inference(assume_negation,[status(cth)],[64])).
% fof(66, plain,~(atomic(tptp0)),inference(fof_simplification,[status(thm)],[1,theory(equality)])).
% fof(69, plain,![X42]:![X43]:![X44]:![X45]:((((occurrence_of(X44,X42)&occurrence_of(X45,X43))&subactivity(X42,X43))&~(subactivity_occurrence(X44,X45)))=>?[X46]:(subactivity_occurrence(X46,X45)&~(subactivity_occurrence(X46,X44)))),inference(fof_simplification,[status(thm)],[15,theory(equality)])).
% fof(70, plain,![X59]:![X60]:((leaf(X59,X60)&~(atomic(X60)))=>?[X61]:(occurrence_of(X61,X60)&leaf_occ(X59,X61))),inference(fof_simplification,[status(thm)],[21,theory(equality)])).
% fof(71, plain,![X65]:![X66]:![X67]:![X68]:((((occurrence_of(X67,X68)&~(atomic(X68)))&leaf_occ(X65,X67))&leaf_occ(X66,X67))=>X65=X66),inference(fof_simplification,[status(thm)],[27,theory(equality)])).
% fof(72, plain,![X100]:![X101]:![X102]:![X103]:(((((occurrence_of(X101,X100)&subactivity_occurrence(X102,X101))&root_occ(X103,X101))&arboreal(X102))&~(min_precedes(X103,X102,X100)))=>X103=X102),inference(fof_simplification,[status(thm)],[42,theory(equality)])).
% fof(73, plain,![X118]:![X119]:![X120]:(min_precedes(X118,X119,X120)=>~(root(X119,X120))),inference(fof_simplification,[status(thm)],[46,theory(equality)])).
% fof(75, plain,![X126]:![X127]:((occurrence_of(X127,X126)&~(atomic(X126)))=>?[X128]:(root(X128,X126)&subactivity_occurrence(X128,X127))),inference(fof_simplification,[status(thm)],[49,theory(equality)])).
% fof(77, plain,![X136]:![X137]:![X138]:![X139]:(((((occurrence_of(X137,X136)&subactivity_occurrence(X138,X137))&leaf_occ(X139,X137))&arboreal(X138))&~(min_precedes(X138,X139,X136)))=>X139=X138),inference(fof_simplification,[status(thm)],[52,theory(equality)])).
% cnf(78,plain,(~atomic(tptp0)),inference(split_conjunct,[status(thm)],[66])).
% fof(80, plain,![X1]:![X2]:![X3]:((~(occurrence_of(X1,X2))|~(occurrence_of(X1,X3)))|X2=X3),inference(fof_nnf,[status(thm)],[3])).
% fof(81, plain,![X4]:![X5]:![X6]:((~(occurrence_of(X4,X5))|~(occurrence_of(X4,X6)))|X5=X6),inference(variable_rename,[status(thm)],[80])).
% cnf(82,plain,(X1=X2|~occurrence_of(X3,X2)|~occurrence_of(X3,X1)),inference(split_conjunct,[status(thm)],[81])).
% fof(83, plain,![X4]:![X5]:((~(occurrence_of(X5,tptp0))|~(root_occ(X4,X5)))|?[X6]:(occurrence_of(X6,tptp1)&next_subocc(X4,X6,tptp0))),inference(fof_nnf,[status(thm)],[4])).
% fof(84, plain,![X7]:![X8]:((~(occurrence_of(X8,tptp0))|~(root_occ(X7,X8)))|?[X9]:(occurrence_of(X9,tptp1)&next_subocc(X7,X9,tptp0))),inference(variable_rename,[status(thm)],[83])).
% fof(85, plain,![X7]:![X8]:((~(occurrence_of(X8,tptp0))|~(root_occ(X7,X8)))|(occurrence_of(esk1_2(X7,X8),tptp1)&next_subocc(X7,esk1_2(X7,X8),tptp0))),inference(skolemize,[status(esa)],[84])).
% fof(86, plain,![X7]:![X8]:((occurrence_of(esk1_2(X7,X8),tptp1)|(~(occurrence_of(X8,tptp0))|~(root_occ(X7,X8))))&(next_subocc(X7,esk1_2(X7,X8),tptp0)|(~(occurrence_of(X8,tptp0))|~(root_occ(X7,X8))))),inference(distribute,[status(thm)],[85])).
% cnf(87,plain,(next_subocc(X1,esk1_2(X1,X2),tptp0)|~root_occ(X1,X2)|~occurrence_of(X2,tptp0)),inference(split_conjunct,[status(thm)],[86])).
% cnf(88,plain,(occurrence_of(esk1_2(X1,X2),tptp1)|~root_occ(X1,X2)|~occurrence_of(X2,tptp0)),inference(split_conjunct,[status(thm)],[86])).
% fof(95, plain,![X12]:![X13]:![X14]:((~(subactivity_occurrence(X12,X13))|~(subactivity_occurrence(X13,X14)))|subactivity_occurrence(X12,X14)),inference(fof_nnf,[status(thm)],[7])).
% fof(96, plain,![X15]:![X16]:![X17]:((~(subactivity_occurrence(X15,X16))|~(subactivity_occurrence(X16,X17)))|subactivity_occurrence(X15,X17)),inference(variable_rename,[status(thm)],[95])).
% cnf(97,plain,(subactivity_occurrence(X1,X2)|~subactivity_occurrence(X3,X2)|~subactivity_occurrence(X1,X3)),inference(split_conjunct,[status(thm)],[96])).
% fof(98, plain,![X15]:![X16]:![X17]:![X18]:(((~(occurrence_of(X17,X18))|~(root_occ(X15,X17)))|~(root_occ(X16,X17)))|X15=X16),inference(fof_nnf,[status(thm)],[8])).
% fof(99, plain,![X19]:![X20]:![X21]:![X22]:(((~(occurrence_of(X21,X22))|~(root_occ(X19,X21)))|~(root_occ(X20,X21)))|X19=X20),inference(variable_rename,[status(thm)],[98])).
% cnf(100,plain,(X1=X2|~root_occ(X2,X3)|~root_occ(X1,X3)|~occurrence_of(X3,X4)),inference(split_conjunct,[status(thm)],[99])).
% fof(101, plain,![X19]:![X20]:![X21]:(~(min_precedes(X20,X21,X19))|?[X22]:((occurrence_of(X22,X19)&subactivity_occurrence(X20,X22))&subactivity_occurrence(X21,X22))),inference(fof_nnf,[status(thm)],[9])).
% fof(102, plain,![X23]:![X24]:![X25]:(~(min_precedes(X24,X25,X23))|?[X26]:((occurrence_of(X26,X23)&subactivity_occurrence(X24,X26))&subactivity_occurrence(X25,X26))),inference(variable_rename,[status(thm)],[101])).
% fof(103, plain,![X23]:![X24]:![X25]:(~(min_precedes(X24,X25,X23))|((occurrence_of(esk2_3(X23,X24,X25),X23)&subactivity_occurrence(X24,esk2_3(X23,X24,X25)))&subactivity_occurrence(X25,esk2_3(X23,X24,X25)))),inference(skolemize,[status(esa)],[102])).
% fof(104, plain,![X23]:![X24]:![X25]:(((occurrence_of(esk2_3(X23,X24,X25),X23)|~(min_precedes(X24,X25,X23)))&(subactivity_occurrence(X24,esk2_3(X23,X24,X25))|~(min_precedes(X24,X25,X23))))&(subactivity_occurrence(X25,esk2_3(X23,X24,X25))|~(min_precedes(X24,X25,X23)))),inference(distribute,[status(thm)],[103])).
% cnf(105,plain,(subactivity_occurrence(X2,esk2_3(X3,X1,X2))|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[104])).
% cnf(107,plain,(occurrence_of(esk2_3(X3,X1,X2),X3)|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[104])).
% fof(111, plain,![X27]:![X28]:![X29]:((~(next_subocc(X27,X28,X29))|(min_precedes(X27,X28,X29)&![X30]:(~(min_precedes(X27,X30,X29))|~(min_precedes(X30,X28,X29)))))&((~(min_precedes(X27,X28,X29))|?[X30]:(min_precedes(X27,X30,X29)&min_precedes(X30,X28,X29)))|next_subocc(X27,X28,X29))),inference(fof_nnf,[status(thm)],[11])).
% fof(112, plain,![X31]:![X32]:![X33]:((~(next_subocc(X31,X32,X33))|(min_precedes(X31,X32,X33)&![X34]:(~(min_precedes(X31,X34,X33))|~(min_precedes(X34,X32,X33)))))&((~(min_precedes(X31,X32,X33))|?[X35]:(min_precedes(X31,X35,X33)&min_precedes(X35,X32,X33)))|next_subocc(X31,X32,X33))),inference(variable_rename,[status(thm)],[111])).
% fof(113, plain,![X31]:![X32]:![X33]:((~(next_subocc(X31,X32,X33))|(min_precedes(X31,X32,X33)&![X34]:(~(min_precedes(X31,X34,X33))|~(min_precedes(X34,X32,X33)))))&((~(min_precedes(X31,X32,X33))|(min_precedes(X31,esk3_3(X31,X32,X33),X33)&min_precedes(esk3_3(X31,X32,X33),X32,X33)))|next_subocc(X31,X32,X33))),inference(skolemize,[status(esa)],[112])).
% fof(114, plain,![X31]:![X32]:![X33]:![X34]:((((~(min_precedes(X31,X34,X33))|~(min_precedes(X34,X32,X33)))&min_precedes(X31,X32,X33))|~(next_subocc(X31,X32,X33)))&((~(min_precedes(X31,X32,X33))|(min_precedes(X31,esk3_3(X31,X32,X33),X33)&min_precedes(esk3_3(X31,X32,X33),X32,X33)))|next_subocc(X31,X32,X33))),inference(shift_quantors,[status(thm)],[113])).
% fof(115, plain,![X31]:![X32]:![X33]:![X34]:((((~(min_precedes(X31,X34,X33))|~(min_precedes(X34,X32,X33)))|~(next_subocc(X31,X32,X33)))&(min_precedes(X31,X32,X33)|~(next_subocc(X31,X32,X33))))&(((min_precedes(X31,esk3_3(X31,X32,X33),X33)|~(min_precedes(X31,X32,X33)))|next_subocc(X31,X32,X33))&((min_precedes(esk3_3(X31,X32,X33),X32,X33)|~(min_precedes(X31,X32,X33)))|next_subocc(X31,X32,X33)))),inference(distribute,[status(thm)],[114])).
% cnf(118,plain,(min_precedes(X1,X2,X3)|~next_subocc(X1,X2,X3)),inference(split_conjunct,[status(thm)],[115])).
% cnf(119,plain,(~next_subocc(X1,X2,X3)|~min_precedes(X4,X2,X3)|~min_precedes(X1,X4,X3)),inference(split_conjunct,[status(thm)],[115])).
% fof(131, plain,![X42]:![X43]:![X44]:![X45]:((((~(occurrence_of(X44,X42))|~(occurrence_of(X45,X43)))|~(subactivity(X42,X43)))|subactivity_occurrence(X44,X45))|?[X46]:(subactivity_occurrence(X46,X45)&~(subactivity_occurrence(X46,X44)))),inference(fof_nnf,[status(thm)],[69])).
% fof(132, plain,![X47]:![X48]:![X49]:![X50]:((((~(occurrence_of(X49,X47))|~(occurrence_of(X50,X48)))|~(subactivity(X47,X48)))|subactivity_occurrence(X49,X50))|?[X51]:(subactivity_occurrence(X51,X50)&~(subactivity_occurrence(X51,X49)))),inference(variable_rename,[status(thm)],[131])).
% fof(133, plain,![X47]:![X48]:![X49]:![X50]:((((~(occurrence_of(X49,X47))|~(occurrence_of(X50,X48)))|~(subactivity(X47,X48)))|subactivity_occurrence(X49,X50))|(subactivity_occurrence(esk4_4(X47,X48,X49,X50),X50)&~(subactivity_occurrence(esk4_4(X47,X48,X49,X50),X49)))),inference(skolemize,[status(esa)],[132])).
% fof(134, plain,![X47]:![X48]:![X49]:![X50]:((subactivity_occurrence(esk4_4(X47,X48,X49,X50),X50)|(((~(occurrence_of(X49,X47))|~(occurrence_of(X50,X48)))|~(subactivity(X47,X48)))|subactivity_occurrence(X49,X50)))&(~(subactivity_occurrence(esk4_4(X47,X48,X49,X50),X49))|(((~(occurrence_of(X49,X47))|~(occurrence_of(X50,X48)))|~(subactivity(X47,X48)))|subactivity_occurrence(X49,X50)))),inference(distribute,[status(thm)],[133])).
% cnf(135,plain,(subactivity_occurrence(X1,X2)|~subactivity(X3,X4)|~occurrence_of(X2,X4)|~occurrence_of(X1,X3)|~subactivity_occurrence(esk4_4(X3,X4,X1,X2),X1)),inference(split_conjunct,[status(thm)],[134])).
% cnf(136,plain,(subactivity_occurrence(X1,X2)|subactivity_occurrence(esk4_4(X3,X4,X1,X2),X2)|~subactivity(X3,X4)|~occurrence_of(X2,X4)|~occurrence_of(X1,X3)),inference(split_conjunct,[status(thm)],[134])).
% fof(137, plain,![X47]:(~(activity(X47))|subactivity(X47,X47)),inference(fof_nnf,[status(thm)],[16])).
% fof(138, plain,![X48]:(~(activity(X48))|subactivity(X48,X48)),inference(variable_rename,[status(thm)],[137])).
% cnf(139,plain,(subactivity(X1,X1)|~activity(X1)),inference(split_conjunct,[status(thm)],[138])).
% fof(140, plain,![X48]:![X49]:(~(occurrence_of(X48,X49))|((~(arboreal(X48))|atomic(X49))&(~(atomic(X49))|arboreal(X48)))),inference(fof_nnf,[status(thm)],[17])).
% fof(141, plain,![X50]:![X51]:(~(occurrence_of(X50,X51))|((~(arboreal(X50))|atomic(X51))&(~(atomic(X51))|arboreal(X50)))),inference(variable_rename,[status(thm)],[140])).
% fof(142, plain,![X50]:![X51]:(((~(arboreal(X50))|atomic(X51))|~(occurrence_of(X50,X51)))&((~(atomic(X51))|arboreal(X50))|~(occurrence_of(X50,X51)))),inference(distribute,[status(thm)],[141])).
% cnf(143,plain,(arboreal(X1)|~occurrence_of(X1,X2)|~atomic(X2)),inference(split_conjunct,[status(thm)],[142])).
% fof(150, plain,![X53]:(~(occurrence_of(X53,tptp0))|?[X54]:?[X55]:((((occurrence_of(X54,tptp4)&root_occ(X54,X53))&occurrence_of(X55,tptp3))&leaf_occ(X55,X53))&next_subocc(X54,X55,tptp0))),inference(fof_nnf,[status(thm)],[19])).
% fof(151, plain,![X56]:(~(occurrence_of(X56,tptp0))|?[X57]:?[X58]:((((occurrence_of(X57,tptp4)&root_occ(X57,X56))&occurrence_of(X58,tptp3))&leaf_occ(X58,X56))&next_subocc(X57,X58,tptp0))),inference(variable_rename,[status(thm)],[150])).
% fof(152, plain,![X56]:(~(occurrence_of(X56,tptp0))|((((occurrence_of(esk5_1(X56),tptp4)&root_occ(esk5_1(X56),X56))&occurrence_of(esk6_1(X56),tptp3))&leaf_occ(esk6_1(X56),X56))&next_subocc(esk5_1(X56),esk6_1(X56),tptp0))),inference(skolemize,[status(esa)],[151])).
% fof(153, plain,![X56]:(((((occurrence_of(esk5_1(X56),tptp4)|~(occurrence_of(X56,tptp0)))&(root_occ(esk5_1(X56),X56)|~(occurrence_of(X56,tptp0))))&(occurrence_of(esk6_1(X56),tptp3)|~(occurrence_of(X56,tptp0))))&(leaf_occ(esk6_1(X56),X56)|~(occurrence_of(X56,tptp0))))&(next_subocc(esk5_1(X56),esk6_1(X56),tptp0)|~(occurrence_of(X56,tptp0)))),inference(distribute,[status(thm)],[152])).
% cnf(154,plain,(next_subocc(esk5_1(X1),esk6_1(X1),tptp0)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[153])).
% cnf(155,plain,(leaf_occ(esk6_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[153])).
% cnf(156,plain,(occurrence_of(esk6_1(X1),tptp3)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[153])).
% cnf(157,plain,(root_occ(esk5_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[153])).
% fof(159, plain,![X56]:![X57]:((~(root_occ(X56,X57))|?[X58]:((occurrence_of(X57,X58)&subactivity_occurrence(X56,X57))&root(X56,X58)))&(![X58]:((~(occurrence_of(X57,X58))|~(subactivity_occurrence(X56,X57)))|~(root(X56,X58)))|root_occ(X56,X57))),inference(fof_nnf,[status(thm)],[20])).
% fof(160, plain,![X59]:![X60]:((~(root_occ(X59,X60))|?[X61]:((occurrence_of(X60,X61)&subactivity_occurrence(X59,X60))&root(X59,X61)))&(![X62]:((~(occurrence_of(X60,X62))|~(subactivity_occurrence(X59,X60)))|~(root(X59,X62)))|root_occ(X59,X60))),inference(variable_rename,[status(thm)],[159])).
% fof(161, plain,![X59]:![X60]:((~(root_occ(X59,X60))|((occurrence_of(X60,esk7_2(X59,X60))&subactivity_occurrence(X59,X60))&root(X59,esk7_2(X59,X60))))&(![X62]:((~(occurrence_of(X60,X62))|~(subactivity_occurrence(X59,X60)))|~(root(X59,X62)))|root_occ(X59,X60))),inference(skolemize,[status(esa)],[160])).
% fof(162, plain,![X59]:![X60]:![X62]:((((~(occurrence_of(X60,X62))|~(subactivity_occurrence(X59,X60)))|~(root(X59,X62)))|root_occ(X59,X60))&(~(root_occ(X59,X60))|((occurrence_of(X60,esk7_2(X59,X60))&subactivity_occurrence(X59,X60))&root(X59,esk7_2(X59,X60))))),inference(shift_quantors,[status(thm)],[161])).
% fof(163, plain,![X59]:![X60]:![X62]:((((~(occurrence_of(X60,X62))|~(subactivity_occurrence(X59,X60)))|~(root(X59,X62)))|root_occ(X59,X60))&(((occurrence_of(X60,esk7_2(X59,X60))|~(root_occ(X59,X60)))&(subactivity_occurrence(X59,X60)|~(root_occ(X59,X60))))&(root(X59,esk7_2(X59,X60))|~(root_occ(X59,X60))))),inference(distribute,[status(thm)],[162])).
% cnf(164,plain,(root(X1,esk7_2(X1,X2))|~root_occ(X1,X2)),inference(split_conjunct,[status(thm)],[163])).
% cnf(165,plain,(subactivity_occurrence(X1,X2)|~root_occ(X1,X2)),inference(split_conjunct,[status(thm)],[163])).
% cnf(166,plain,(occurrence_of(X2,esk7_2(X1,X2))|~root_occ(X1,X2)),inference(split_conjunct,[status(thm)],[163])).
% cnf(167,plain,(root_occ(X1,X2)|~root(X1,X3)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,X3)),inference(split_conjunct,[status(thm)],[163])).
% fof(168, plain,![X59]:![X60]:((~(leaf(X59,X60))|atomic(X60))|?[X61]:(occurrence_of(X61,X60)&leaf_occ(X59,X61))),inference(fof_nnf,[status(thm)],[70])).
% fof(169, plain,![X62]:![X63]:((~(leaf(X62,X63))|atomic(X63))|?[X64]:(occurrence_of(X64,X63)&leaf_occ(X62,X64))),inference(variable_rename,[status(thm)],[168])).
% fof(170, plain,![X62]:![X63]:((~(leaf(X62,X63))|atomic(X63))|(occurrence_of(esk8_2(X62,X63),X63)&leaf_occ(X62,esk8_2(X62,X63)))),inference(skolemize,[status(esa)],[169])).
% fof(171, plain,![X62]:![X63]:((occurrence_of(esk8_2(X62,X63),X63)|(~(leaf(X62,X63))|atomic(X63)))&(leaf_occ(X62,esk8_2(X62,X63))|(~(leaf(X62,X63))|atomic(X63)))),inference(distribute,[status(thm)],[170])).
% cnf(172,plain,(atomic(X1)|leaf_occ(X2,esk8_2(X2,X1))|~leaf(X2,X1)),inference(split_conjunct,[status(thm)],[171])).
% cnf(173,plain,(atomic(X1)|occurrence_of(esk8_2(X2,X1),X1)|~leaf(X2,X1)),inference(split_conjunct,[status(thm)],[171])).
% fof(181, plain,![X65]:![X66]:![X67]:![X68]:((((~(occurrence_of(X67,X68))|atomic(X68))|~(leaf_occ(X65,X67)))|~(leaf_occ(X66,X67)))|X65=X66),inference(fof_nnf,[status(thm)],[71])).
% fof(182, plain,![X69]:![X70]:![X71]:![X72]:((((~(occurrence_of(X71,X72))|atomic(X72))|~(leaf_occ(X69,X71)))|~(leaf_occ(X70,X71)))|X69=X70),inference(variable_rename,[status(thm)],[181])).
% cnf(183,plain,(X1=X2|atomic(X4)|~leaf_occ(X2,X3)|~leaf_occ(X1,X3)|~occurrence_of(X3,X4)),inference(split_conjunct,[status(thm)],[182])).
% fof(190, plain,![X78]:![X79]:(~(occurrence_of(X79,X78))|(activity(X78)&activity_occurrence(X79))),inference(fof_nnf,[status(thm)],[30])).
% fof(191, plain,![X80]:![X81]:(~(occurrence_of(X81,X80))|(activity(X80)&activity_occurrence(X81))),inference(variable_rename,[status(thm)],[190])).
% fof(192, plain,![X80]:![X81]:((activity(X80)|~(occurrence_of(X81,X80)))&(activity_occurrence(X81)|~(occurrence_of(X81,X80)))),inference(distribute,[status(thm)],[191])).
% cnf(193,plain,(activity_occurrence(X1)|~occurrence_of(X1,X2)),inference(split_conjunct,[status(thm)],[192])).
% fof(195, plain,![X80]:(~(activity_occurrence(X80))|?[X81]:(activity(X81)&occurrence_of(X80,X81))),inference(fof_nnf,[status(thm)],[31])).
% fof(196, plain,![X82]:(~(activity_occurrence(X82))|?[X83]:(activity(X83)&occurrence_of(X82,X83))),inference(variable_rename,[status(thm)],[195])).
% fof(197, plain,![X82]:(~(activity_occurrence(X82))|(activity(esk9_1(X82))&occurrence_of(X82,esk9_1(X82)))),inference(skolemize,[status(esa)],[196])).
% fof(198, plain,![X82]:((activity(esk9_1(X82))|~(activity_occurrence(X82)))&(occurrence_of(X82,esk9_1(X82))|~(activity_occurrence(X82)))),inference(distribute,[status(thm)],[197])).
% cnf(199,plain,(occurrence_of(X1,esk9_1(X1))|~activity_occurrence(X1)),inference(split_conjunct,[status(thm)],[198])).
% cnf(200,plain,(activity(esk9_1(X1))|~activity_occurrence(X1)),inference(split_conjunct,[status(thm)],[198])).
% cnf(208,plain,(tptp1!=tptp3),inference(split_conjunct,[status(thm)],[35])).
% fof(231, plain,![X100]:![X101]:![X102]:![X103]:(((((~(occurrence_of(X101,X100))|~(subactivity_occurrence(X102,X101)))|~(root_occ(X103,X101)))|~(arboreal(X102)))|min_precedes(X103,X102,X100))|X103=X102),inference(fof_nnf,[status(thm)],[72])).
% fof(232, plain,![X104]:![X105]:![X106]:![X107]:(((((~(occurrence_of(X105,X104))|~(subactivity_occurrence(X106,X105)))|~(root_occ(X107,X105)))|~(arboreal(X106)))|min_precedes(X107,X106,X104))|X107=X106),inference(variable_rename,[status(thm)],[231])).
% cnf(233,plain,(X1=X2|min_precedes(X1,X2,X3)|~arboreal(X2)|~root_occ(X1,X4)|~subactivity_occurrence(X2,X4)|~occurrence_of(X4,X3)),inference(split_conjunct,[status(thm)],[232])).
% fof(246, plain,![X118]:![X119]:![X120]:(~(min_precedes(X118,X119,X120))|~(root(X119,X120))),inference(fof_nnf,[status(thm)],[73])).
% fof(247, plain,![X121]:![X122]:![X123]:(~(min_precedes(X121,X122,X123))|~(root(X122,X123))),inference(variable_rename,[status(thm)],[246])).
% cnf(248,plain,(~root(X1,X2)|~min_precedes(X3,X1,X2)),inference(split_conjunct,[status(thm)],[247])).
% fof(249, plain,![X121]:![X122]:(~(subactivity_occurrence(X121,X122))|(activity_occurrence(X121)&activity_occurrence(X122))),inference(fof_nnf,[status(thm)],[47])).
% fof(250, plain,![X123]:![X124]:(~(subactivity_occurrence(X123,X124))|(activity_occurrence(X123)&activity_occurrence(X124))),inference(variable_rename,[status(thm)],[249])).
% fof(251, plain,![X123]:![X124]:((activity_occurrence(X123)|~(subactivity_occurrence(X123,X124)))&(activity_occurrence(X124)|~(subactivity_occurrence(X123,X124)))),inference(distribute,[status(thm)],[250])).
% cnf(253,plain,(activity_occurrence(X1)|~subactivity_occurrence(X1,X2)),inference(split_conjunct,[status(thm)],[251])).
% fof(260, plain,![X126]:![X127]:((~(occurrence_of(X127,X126))|atomic(X126))|?[X128]:(root(X128,X126)&subactivity_occurrence(X128,X127))),inference(fof_nnf,[status(thm)],[75])).
% fof(261, plain,![X129]:![X130]:((~(occurrence_of(X130,X129))|atomic(X129))|?[X131]:(root(X131,X129)&subactivity_occurrence(X131,X130))),inference(variable_rename,[status(thm)],[260])).
% fof(262, plain,![X129]:![X130]:((~(occurrence_of(X130,X129))|atomic(X129))|(root(esk13_2(X129,X130),X129)&subactivity_occurrence(esk13_2(X129,X130),X130))),inference(skolemize,[status(esa)],[261])).
% fof(263, plain,![X129]:![X130]:((root(esk13_2(X129,X130),X129)|(~(occurrence_of(X130,X129))|atomic(X129)))&(subactivity_occurrence(esk13_2(X129,X130),X130)|(~(occurrence_of(X130,X129))|atomic(X129)))),inference(distribute,[status(thm)],[262])).
% cnf(264,plain,(atomic(X1)|subactivity_occurrence(esk13_2(X1,X2),X2)|~occurrence_of(X2,X1)),inference(split_conjunct,[status(thm)],[263])).
% cnf(265,plain,(atomic(X1)|root(esk13_2(X1,X2),X1)|~occurrence_of(X2,X1)),inference(split_conjunct,[status(thm)],[263])).
% fof(269, plain,![X133]:![X134]:((~(leaf_occ(X133,X134))|?[X135]:((occurrence_of(X134,X135)&subactivity_occurrence(X133,X134))&leaf(X133,X135)))&(![X135]:((~(occurrence_of(X134,X135))|~(subactivity_occurrence(X133,X134)))|~(leaf(X133,X135)))|leaf_occ(X133,X134))),inference(fof_nnf,[status(thm)],[51])).
% fof(270, plain,![X136]:![X137]:((~(leaf_occ(X136,X137))|?[X138]:((occurrence_of(X137,X138)&subactivity_occurrence(X136,X137))&leaf(X136,X138)))&(![X139]:((~(occurrence_of(X137,X139))|~(subactivity_occurrence(X136,X137)))|~(leaf(X136,X139)))|leaf_occ(X136,X137))),inference(variable_rename,[status(thm)],[269])).
% fof(271, plain,![X136]:![X137]:((~(leaf_occ(X136,X137))|((occurrence_of(X137,esk14_2(X136,X137))&subactivity_occurrence(X136,X137))&leaf(X136,esk14_2(X136,X137))))&(![X139]:((~(occurrence_of(X137,X139))|~(subactivity_occurrence(X136,X137)))|~(leaf(X136,X139)))|leaf_occ(X136,X137))),inference(skolemize,[status(esa)],[270])).
% fof(272, plain,![X136]:![X137]:![X139]:((((~(occurrence_of(X137,X139))|~(subactivity_occurrence(X136,X137)))|~(leaf(X136,X139)))|leaf_occ(X136,X137))&(~(leaf_occ(X136,X137))|((occurrence_of(X137,esk14_2(X136,X137))&subactivity_occurrence(X136,X137))&leaf(X136,esk14_2(X136,X137))))),inference(shift_quantors,[status(thm)],[271])).
% fof(273, plain,![X136]:![X137]:![X139]:((((~(occurrence_of(X137,X139))|~(subactivity_occurrence(X136,X137)))|~(leaf(X136,X139)))|leaf_occ(X136,X137))&(((occurrence_of(X137,esk14_2(X136,X137))|~(leaf_occ(X136,X137)))&(subactivity_occurrence(X136,X137)|~(leaf_occ(X136,X137))))&(leaf(X136,esk14_2(X136,X137))|~(leaf_occ(X136,X137))))),inference(distribute,[status(thm)],[272])).
% cnf(274,plain,(leaf(X1,esk14_2(X1,X2))|~leaf_occ(X1,X2)),inference(split_conjunct,[status(thm)],[273])).
% cnf(276,plain,(occurrence_of(X2,esk14_2(X1,X2))|~leaf_occ(X1,X2)),inference(split_conjunct,[status(thm)],[273])).
% fof(278, plain,![X136]:![X137]:![X138]:![X139]:(((((~(occurrence_of(X137,X136))|~(subactivity_occurrence(X138,X137)))|~(leaf_occ(X139,X137)))|~(arboreal(X138)))|min_precedes(X138,X139,X136))|X139=X138),inference(fof_nnf,[status(thm)],[77])).
% fof(279, plain,![X140]:![X141]:![X142]:![X143]:(((((~(occurrence_of(X141,X140))|~(subactivity_occurrence(X142,X141)))|~(leaf_occ(X143,X141)))|~(arboreal(X142)))|min_precedes(X142,X143,X140))|X143=X142),inference(variable_rename,[status(thm)],[278])).
% cnf(280,plain,(X1=X2|min_precedes(X2,X1,X3)|~arboreal(X2)|~leaf_occ(X1,X4)|~subactivity_occurrence(X2,X4)|~occurrence_of(X4,X3)),inference(split_conjunct,[status(thm)],[279])).
% fof(281, plain,![X140]:![X141]:![X142]:(~(min_precedes(X141,X142,X140))|?[X143]:?[X144]:(((subactivity(X143,X140)&subactivity(X144,X140))&atocc(X141,X143))&atocc(X142,X144))),inference(fof_nnf,[status(thm)],[53])).
% fof(282, plain,![X145]:![X146]:![X147]:(~(min_precedes(X146,X147,X145))|?[X148]:?[X149]:(((subactivity(X148,X145)&subactivity(X149,X145))&atocc(X146,X148))&atocc(X147,X149))),inference(variable_rename,[status(thm)],[281])).
% fof(283, plain,![X145]:![X146]:![X147]:(~(min_precedes(X146,X147,X145))|(((subactivity(esk15_3(X145,X146,X147),X145)&subactivity(esk16_3(X145,X146,X147),X145))&atocc(X146,esk15_3(X145,X146,X147)))&atocc(X147,esk16_3(X145,X146,X147)))),inference(skolemize,[status(esa)],[282])).
% fof(284, plain,![X145]:![X146]:![X147]:((((subactivity(esk15_3(X145,X146,X147),X145)|~(min_precedes(X146,X147,X145)))&(subactivity(esk16_3(X145,X146,X147),X145)|~(min_precedes(X146,X147,X145))))&(atocc(X146,esk15_3(X145,X146,X147))|~(min_precedes(X146,X147,X145))))&(atocc(X147,esk16_3(X145,X146,X147))|~(min_precedes(X146,X147,X145)))),inference(distribute,[status(thm)],[283])).
% cnf(285,plain,(atocc(X2,esk16_3(X3,X1,X2))|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[284])).
% fof(307, plain,![X160]:![X161]:((~(atocc(X160,X161))|?[X162]:((subactivity(X161,X162)&atomic(X162))&occurrence_of(X160,X162)))&(![X162]:((~(subactivity(X161,X162))|~(atomic(X162)))|~(occurrence_of(X160,X162)))|atocc(X160,X161))),inference(fof_nnf,[status(thm)],[58])).
% fof(308, plain,![X163]:![X164]:((~(atocc(X163,X164))|?[X165]:((subactivity(X164,X165)&atomic(X165))&occurrence_of(X163,X165)))&(![X166]:((~(subactivity(X164,X166))|~(atomic(X166)))|~(occurrence_of(X163,X166)))|atocc(X163,X164))),inference(variable_rename,[status(thm)],[307])).
% fof(309, plain,![X163]:![X164]:((~(atocc(X163,X164))|((subactivity(X164,esk19_2(X163,X164))&atomic(esk19_2(X163,X164)))&occurrence_of(X163,esk19_2(X163,X164))))&(![X166]:((~(subactivity(X164,X166))|~(atomic(X166)))|~(occurrence_of(X163,X166)))|atocc(X163,X164))),inference(skolemize,[status(esa)],[308])).
% fof(310, plain,![X163]:![X164]:![X166]:((((~(subactivity(X164,X166))|~(atomic(X166)))|~(occurrence_of(X163,X166)))|atocc(X163,X164))&(~(atocc(X163,X164))|((subactivity(X164,esk19_2(X163,X164))&atomic(esk19_2(X163,X164)))&occurrence_of(X163,esk19_2(X163,X164))))),inference(shift_quantors,[status(thm)],[309])).
% fof(311, plain,![X163]:![X164]:![X166]:((((~(subactivity(X164,X166))|~(atomic(X166)))|~(occurrence_of(X163,X166)))|atocc(X163,X164))&(((subactivity(X164,esk19_2(X163,X164))|~(atocc(X163,X164)))&(atomic(esk19_2(X163,X164))|~(atocc(X163,X164))))&(occurrence_of(X163,esk19_2(X163,X164))|~(atocc(X163,X164))))),inference(distribute,[status(thm)],[310])).
% cnf(312,plain,(occurrence_of(X1,esk19_2(X1,X2))|~atocc(X1,X2)),inference(split_conjunct,[status(thm)],[311])).
% cnf(313,plain,(atomic(esk19_2(X1,X2))|~atocc(X1,X2)),inference(split_conjunct,[status(thm)],[311])).
% fof(325, negated_conjecture,?[X168]:occurrence_of(X168,tptp0),inference(fof_nnf,[status(thm)],[65])).
% fof(326, negated_conjecture,?[X169]:occurrence_of(X169,tptp0),inference(variable_rename,[status(thm)],[325])).
% fof(327, negated_conjecture,occurrence_of(esk20_0,tptp0),inference(skolemize,[status(esa)],[326])).
% cnf(328,negated_conjecture,(occurrence_of(esk20_0,tptp0)),inference(split_conjunct,[status(thm)],[327])).
% cnf(329,negated_conjecture,(X1=tptp0|~occurrence_of(esk20_0,X1)),inference(spm,[status(thm)],[82,328,theory(equality)])).
% cnf(332,negated_conjecture,(activity_occurrence(esk20_0)),inference(spm,[status(thm)],[193,328,theory(equality)])).
% cnf(334,plain,(subactivity(esk9_1(X1),esk9_1(X1))|~activity_occurrence(X1)),inference(spm,[status(thm)],[139,200,theory(equality)])).
% cnf(336,plain,(X1=esk9_1(X2)|~occurrence_of(X2,X1)|~activity_occurrence(X2)),inference(spm,[status(thm)],[82,199,theory(equality)])).
% cnf(354,plain,(arboreal(X1)|~atomic(esk19_2(X1,X2))|~atocc(X1,X2)),inference(spm,[status(thm)],[143,312,theory(equality)])).
% cnf(358,plain,(subactivity_occurrence(esk5_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[165,157,theory(equality)])).
% cnf(359,plain,(X1=esk5_1(X2)|~root_occ(X1,X2)|~occurrence_of(X2,X3)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[100,157,theory(equality)])).
% cnf(410,plain,(X1=esk6_1(X2)|atomic(X3)|~leaf_occ(X1,X2)|~occurrence_of(X2,X3)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[183,155,theory(equality)])).
% cnf(419,plain,(activity_occurrence(esk13_2(X1,X2))|atomic(X1)|~occurrence_of(X2,X1)),inference(spm,[status(thm)],[253,264,theory(equality)])).
% cnf(423,plain,(root_occ(esk13_2(X1,X2),X3)|atomic(X1)|~subactivity_occurrence(esk13_2(X1,X2),X3)|~occurrence_of(X3,X1)|~occurrence_of(X2,X1)),inference(spm,[status(thm)],[167,265,theory(equality)])).
% cnf(425,plain,(min_precedes(X1,esk1_2(X1,X2),tptp0)|~root_occ(X1,X2)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[118,87,theory(equality)])).
% cnf(458,plain,(esk6_1(X1)=X2|min_precedes(X2,esk6_1(X1),X3)|~arboreal(X2)|~subactivity_occurrence(X2,X1)|~occurrence_of(X1,X3)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[280,155,theory(equality)])).
% cnf(462,plain,(X1=X2|min_precedes(X1,X2,X3)|~arboreal(X2)|~root_occ(X1,esk2_3(X4,X5,X2))|~occurrence_of(esk2_3(X4,X5,X2),X3)|~min_precedes(X5,X2,X4)),inference(spm,[status(thm)],[233,105,theory(equality)])).
% cnf(518,plain,(subactivity_occurrence(X1,X1)|~subactivity(X2,X3)|~occurrence_of(X1,X3)|~occurrence_of(X1,X2)),inference(spm,[status(thm)],[135,136,theory(equality)])).
% cnf(536,negated_conjecture,(esk9_1(esk20_0)=tptp0|~activity_occurrence(esk20_0)),inference(spm,[status(thm)],[329,199,theory(equality)])).
% cnf(538,negated_conjecture,(esk9_1(esk20_0)=tptp0|$false),inference(rw,[status(thm)],[536,332,theory(equality)])).
% cnf(539,negated_conjecture,(esk9_1(esk20_0)=tptp0),inference(cn,[status(thm)],[538,theory(equality)])).
% cnf(560,plain,(X1=esk9_1(X2)|~occurrence_of(X2,X1)),inference(csr,[status(thm)],[336,193])).
% cnf(564,plain,(tptp3=esk9_1(esk6_1(X1))|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[560,156,theory(equality)])).
% cnf(566,plain,(X1=esk9_1(esk2_3(X1,X2,X3))|~min_precedes(X2,X3,X1)),inference(spm,[status(thm)],[560,107,theory(equality)])).
% cnf(567,plain,(tptp1=esk9_1(esk1_2(X1,X2))|~root_occ(X1,X2)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[560,88,theory(equality)])).
% cnf(569,plain,(esk14_2(X1,X2)=esk9_1(X2)|~leaf_occ(X1,X2)),inference(spm,[status(thm)],[560,276,theory(equality)])).
% cnf(570,plain,(esk7_2(X1,X2)=esk9_1(X2)|~root_occ(X1,X2)),inference(spm,[status(thm)],[560,166,theory(equality)])).
% cnf(685,plain,(leaf(X1,esk9_1(X2))|~leaf_occ(X1,X2)),inference(spm,[status(thm)],[274,569,theory(equality)])).
% cnf(691,plain,(root(X1,esk9_1(X2))|~root_occ(X1,X2)),inference(spm,[status(thm)],[164,570,theory(equality)])).
% cnf(723,plain,(arboreal(X1)|~atocc(X1,X2)),inference(csr,[status(thm)],[354,313])).
% cnf(724,plain,(arboreal(X1)|~min_precedes(X3,X1,X2)),inference(spm,[status(thm)],[723,285,theory(equality)])).
% cnf(780,plain,(subactivity_occurrence(X1,X2)|~subactivity_occurrence(X1,esk5_1(X2))|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[97,358,theory(equality)])).
% cnf(1168,plain,(X1=esk6_1(esk8_2(X1,X2))|atomic(X3)|atomic(X2)|~occurrence_of(esk8_2(X1,X2),tptp0)|~occurrence_of(esk8_2(X1,X2),X3)|~leaf(X1,X2)),inference(spm,[status(thm)],[410,172,theory(equality)])).
% cnf(1334,plain,(esk13_2(X1,X2)=esk5_1(X3)|atomic(X1)|~occurrence_of(X3,tptp0)|~occurrence_of(X3,X4)|~subactivity_occurrence(esk13_2(X1,X2),X3)|~occurrence_of(X3,X1)|~occurrence_of(X2,X1)),inference(spm,[status(thm)],[359,423,theory(equality)])).
% cnf(1468,plain,(leaf(X1,X2)|~leaf_occ(X1,esk2_3(X2,X3,X4))|~min_precedes(X3,X4,X2)),inference(spm,[status(thm)],[685,566,theory(equality)])).
% cnf(1469,plain,(root(X1,X2)|~root_occ(X1,esk2_3(X2,X3,X4))|~min_precedes(X3,X4,X2)),inference(spm,[status(thm)],[691,566,theory(equality)])).
% cnf(1811,plain,(esk6_1(X2)=X1|~min_precedes(X4,X1,X3)|~next_subocc(X4,esk6_1(X2),X3)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)|~occurrence_of(X2,X3)),inference(spm,[status(thm)],[119,458,theory(equality)])).
% cnf(1933,plain,(X1=X2|min_precedes(X1,X2,X3)|~min_precedes(X5,X2,X4)|~root_occ(X1,esk2_3(X4,X5,X2))|~occurrence_of(esk2_3(X4,X5,X2),X3)),inference(csr,[status(thm)],[462,724])).
% cnf(1936,plain,(esk5_1(esk2_3(X1,X2,X3))=X3|min_precedes(esk5_1(esk2_3(X1,X2,X3)),X3,X4)|~min_precedes(X2,X3,X1)|~occurrence_of(esk2_3(X1,X2,X3),X4)|~occurrence_of(esk2_3(X1,X2,X3),tptp0)),inference(spm,[status(thm)],[1933,157,theory(equality)])).
% cnf(2093,plain,(leaf(esk6_1(esk2_3(X1,X2,X3)),X1)|~min_precedes(X2,X3,X1)|~occurrence_of(esk2_3(X1,X2,X3),tptp0)),inference(spm,[status(thm)],[1468,155,theory(equality)])).
% cnf(2096,plain,(root(esk5_1(esk2_3(X1,X2,X3)),X1)|~min_precedes(X2,X3,X1)|~occurrence_of(esk2_3(X1,X2,X3),tptp0)),inference(spm,[status(thm)],[1469,157,theory(equality)])).
% cnf(2272,plain,(subactivity_occurrence(X1,X1)|~occurrence_of(X1,esk9_1(X2))|~activity_occurrence(X2)),inference(spm,[status(thm)],[518,334,theory(equality)])).
% cnf(2386,plain,(subactivity_occurrence(X1,X1)|~activity_occurrence(X1)),inference(spm,[status(thm)],[2272,199,theory(equality)])).
% cnf(6819,plain,(esk6_1(esk8_2(X1,X2))=X1|atomic(X2)|~leaf(X1,X2)|~occurrence_of(esk8_2(X1,X2),tptp0)),inference(spm,[status(thm)],[1168,173,theory(equality)])).
% cnf(7288,plain,(esk13_2(X1,X2)=esk5_1(X2)|atomic(X1)|~occurrence_of(X2,tptp0)|~occurrence_of(X2,X3)|~occurrence_of(X2,X1)),inference(spm,[status(thm)],[1334,264,theory(equality)])).
% cnf(8763,negated_conjecture,(esk13_2(X1,esk20_0)=esk5_1(esk20_0)|atomic(X1)|~occurrence_of(esk20_0,tptp0)|~occurrence_of(esk20_0,X1)),inference(spm,[status(thm)],[7288,328,theory(equality)])).
% cnf(8787,negated_conjecture,(esk13_2(X1,esk20_0)=esk5_1(esk20_0)|atomic(X1)|$false|~occurrence_of(esk20_0,X1)),inference(rw,[status(thm)],[8763,328,theory(equality)])).
% cnf(8788,negated_conjecture,(esk13_2(X1,esk20_0)=esk5_1(esk20_0)|atomic(X1)|~occurrence_of(esk20_0,X1)),inference(cn,[status(thm)],[8787,theory(equality)])).
% cnf(8791,negated_conjecture,(activity_occurrence(esk5_1(esk20_0))|atomic(X1)|~occurrence_of(esk20_0,X1)),inference(spm,[status(thm)],[419,8788,theory(equality)])).
% cnf(8793,negated_conjecture,(root_occ(esk5_1(esk20_0),X2)|atomic(X1)|~subactivity_occurrence(esk5_1(esk20_0),X2)|~occurrence_of(X2,X1)|~occurrence_of(esk20_0,X1)),inference(spm,[status(thm)],[423,8788,theory(equality)])).
% cnf(8871,negated_conjecture,(activity_occurrence(esk5_1(esk20_0))|atomic(esk9_1(esk20_0))|~activity_occurrence(esk20_0)),inference(spm,[status(thm)],[8791,199,theory(equality)])).
% cnf(8878,negated_conjecture,(activity_occurrence(esk5_1(esk20_0))|atomic(tptp0)|~activity_occurrence(esk20_0)),inference(rw,[status(thm)],[8871,539,theory(equality)])).
% cnf(8879,negated_conjecture,(activity_occurrence(esk5_1(esk20_0))|atomic(tptp0)|$false),inference(rw,[status(thm)],[8878,332,theory(equality)])).
% cnf(8880,negated_conjecture,(activity_occurrence(esk5_1(esk20_0))|atomic(tptp0)),inference(cn,[status(thm)],[8879,theory(equality)])).
% cnf(8881,negated_conjecture,(activity_occurrence(esk5_1(esk20_0))),inference(sr,[status(thm)],[8880,78,theory(equality)])).
% cnf(8893,negated_conjecture,(subactivity_occurrence(esk5_1(esk20_0),esk5_1(esk20_0))),inference(spm,[status(thm)],[2386,8881,theory(equality)])).
% cnf(8905,negated_conjecture,(subactivity_occurrence(esk5_1(esk20_0),esk20_0)|~occurrence_of(esk20_0,tptp0)),inference(spm,[status(thm)],[780,8893,theory(equality)])).
% cnf(8909,negated_conjecture,(subactivity_occurrence(esk5_1(esk20_0),esk20_0)|$false),inference(rw,[status(thm)],[8905,328,theory(equality)])).
% cnf(8910,negated_conjecture,(subactivity_occurrence(esk5_1(esk20_0),esk20_0)),inference(cn,[status(thm)],[8909,theory(equality)])).
% cnf(11588,plain,(esk9_1(X1)=tptp3|atomic(X2)|~occurrence_of(esk8_2(X1,X2),tptp0)|~leaf(X1,X2)),inference(spm,[status(thm)],[564,6819,theory(equality)])).
% cnf(12051,plain,(esk6_1(X2)=X1|~min_precedes(X4,X1,X3)|~subactivity_occurrence(X1,X2)|~next_subocc(X4,esk6_1(X2),X3)|~occurrence_of(X2,tptp0)|~occurrence_of(X2,X3)),inference(csr,[status(thm)],[1811,724])).
% cnf(12054,plain,(esk6_1(X1)=X2|~min_precedes(esk5_1(X1),X2,tptp0)|~subactivity_occurrence(X2,X1)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[12051,154,theory(equality)])).
% cnf(13195,plain,(esk9_1(X1)=tptp3|atomic(tptp0)|~leaf(X1,tptp0)),inference(spm,[status(thm)],[11588,173,theory(equality)])).
% cnf(13196,plain,(esk9_1(X1)=tptp3|~leaf(X1,tptp0)),inference(sr,[status(thm)],[13195,78,theory(equality)])).
% cnf(13302,plain,(tptp3=tptp1|~root_occ(X1,X2)|~occurrence_of(X2,tptp0)|~leaf(esk1_2(X1,X2),tptp0)),inference(spm,[status(thm)],[567,13196,theory(equality)])).
% cnf(13396,plain,(~root_occ(X1,X2)|~occurrence_of(X2,tptp0)|~leaf(esk1_2(X1,X2),tptp0)),inference(sr,[status(thm)],[13302,208,theory(equality)])).
% cnf(13530,plain,(esk6_1(esk2_3(X1,X2,X3))=X3|esk5_1(esk2_3(X1,X2,X3))=X3|~subactivity_occurrence(X3,esk2_3(X1,X2,X3))|~occurrence_of(esk2_3(X1,X2,X3),tptp0)|~min_precedes(X2,X3,X1)),inference(spm,[status(thm)],[12054,1936,theory(equality)])).
% cnf(103189,negated_conjecture,(root_occ(esk5_1(esk20_0),esk20_0)|atomic(tptp0)|~subactivity_occurrence(esk5_1(esk20_0),esk20_0)|~occurrence_of(esk20_0,tptp0)),inference(spm,[status(thm)],[8793,328,theory(equality)])).
% cnf(103221,negated_conjecture,(root_occ(esk5_1(esk20_0),esk20_0)|atomic(tptp0)|$false|~occurrence_of(esk20_0,tptp0)),inference(rw,[status(thm)],[103189,8910,theory(equality)])).
% cnf(103222,negated_conjecture,(root_occ(esk5_1(esk20_0),esk20_0)|atomic(tptp0)|$false|$false),inference(rw,[status(thm)],[103221,328,theory(equality)])).
% cnf(103223,negated_conjecture,(root_occ(esk5_1(esk20_0),esk20_0)|atomic(tptp0)),inference(cn,[status(thm)],[103222,theory(equality)])).
% cnf(103224,negated_conjecture,(root_occ(esk5_1(esk20_0),esk20_0)),inference(sr,[status(thm)],[103223,78,theory(equality)])).
% cnf(205664,plain,(esk6_1(esk2_3(X1,X2,X3))=X3|esk5_1(esk2_3(X1,X2,X3))=X3|~min_precedes(X2,X3,X1)|~occurrence_of(esk2_3(X1,X2,X3),tptp0)),inference(csr,[status(thm)],[13530,105])).
% cnf(206011,plain,(leaf(X3,X1)|esk5_1(esk2_3(X1,X2,X3))=X3|~min_precedes(X2,X3,X1)|~occurrence_of(esk2_3(X1,X2,X3),tptp0)),inference(spm,[status(thm)],[2093,205664,theory(equality)])).
% cnf(269572,plain,(root(X3,X1)|leaf(X3,X1)|~min_precedes(X2,X3,X1)|~occurrence_of(esk2_3(X1,X2,X3),tptp0)),inference(spm,[status(thm)],[2096,206011,theory(equality)])).
% cnf(270145,plain,(leaf(X3,X1)|~min_precedes(X2,X3,X1)|~occurrence_of(esk2_3(X1,X2,X3),tptp0)),inference(csr,[status(thm)],[269572,248])).
% cnf(270146,plain,(leaf(X1,tptp0)|~min_precedes(X2,X1,tptp0)),inference(spm,[status(thm)],[270145,107,theory(equality)])).
% cnf(270279,plain,(leaf(esk1_2(X1,X2),tptp0)|~root_occ(X1,X2)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[270146,425,theory(equality)])).
% cnf(270378,plain,(~root_occ(X1,X2)|~occurrence_of(X2,tptp0)),inference(csr,[status(thm)],[270279,13396])).
% cnf(270399,negated_conjecture,(~occurrence_of(esk20_0,tptp0)),inference(spm,[status(thm)],[270378,103224,theory(equality)])).
% cnf(270448,negated_conjecture,($false),inference(rw,[status(thm)],[270399,328,theory(equality)])).
% cnf(270449,negated_conjecture,($false),inference(cn,[status(thm)],[270448,theory(equality)])).
% cnf(270450,negated_conjecture,($false),270449,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 31323
% # ...of these trivial : 63
% # ...subsumed : 25640
% # ...remaining for further processing: 5620
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 1321
% # Backward-rewritten : 30
% # Generated clauses : 199641
% # ...of the previous two non-trivial : 189646
% # Contextual simplify-reflections : 33409
% # Paramodulations : 199634
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 4266
% # Positive orientable unit clauses: 40
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 31
% # Non-unit-clauses : 4195
% # Current number of unprocessed clauses: 104068
% # ...number of literals in the above : 857675
% # Clause-clause subsumption calls (NU) : 1858454
% # Rec. Clause-clause subsumption calls : 523132
% # Unit Clause-clause subsumption calls : 2451
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 18
% # Indexed BW rewrite successes : 15
% # Backwards rewriting index: 1865 leaves, 2.48+/-5.061 terms/leaf
% # Paramod-from index: 651 leaves, 1.22+/-0.817 terms/leaf
% # Paramod-into index: 1500 leaves, 1.97+/-3.250 terms/leaf
% # -------------------------------------------------
% # User time : 15.885 s
% # System time : 0.373 s
% # Total time : 16.258 s
% # Maximum resident set size: 0 pages
% PrfWatch: 20.77 CPU 21.73 WC
% FINAL PrfWatch: 20.77 CPU 21.73 WC
% SZS output end Solution for /tmp/SystemOnTPTP4980/PRO003+3.tptp
%
%------------------------------------------------------------------------------