%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : PRO006+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 : art04.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:04:35 EST 2010
% Result : Theorem 34.31s
% Output : Solution 34.31s
% 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/SystemOnTPTP32427/PRO006+4.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP32427/PRO006+4.tptp
% SZS output start Solution for /tmp/SystemOnTPTP32427/PRO006+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 32523
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% PrfWatch: 1.93 CPU 2.02 WC
% PrfWatch: 3.92 CPU 4.03 WC
% PrfWatch: 5.91 CPU 6.03 WC
% PrfWatch: 7.90 CPU 8.04 WC
% PrfWatch: 9.90 CPU 10.04 WC
% PrfWatch: 11.89 CPU 12.05 WC
% PrfWatch: 13.50 CPU 14.05 WC
% PrfWatch: 15.15 CPU 16.06 WC
% PrfWatch: 17.14 CPU 18.06 WC
% PrfWatch: 19.14 CPU 20.06 WC
% PrfWatch: 21.13 CPU 22.07 WC
% PrfWatch: 23.12 CPU 24.07 WC
% PrfWatch: 25.11 CPU 26.08 WC
% PrfWatch: 27.11 CPU 28.08 WC
% # Preprocessing time : 0.019 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 29.11 CPU 30.09 WC
% PrfWatch: 31.09 CPU 32.09 WC
% PrfWatch: 33.08 CPU 34.10 WC
% # SZS output start CNFRefutation.
% fof(1, axiom,~(atomic(tptp0)),file('/tmp/SRASS.s.p', sos_34)).
% fof(3, axiom,![X1]:![X2]:![X3]:((occurrence_of(X1,X2)&occurrence_of(X1,X3))=>X2=X3),file('/tmp/SRASS.s.p', sos_08)).
% fof(4, axiom,![X4]:![X5]:![X6]:![X7]:(((occurrence_of(X6,X7)&root_occ(X4,X6))&root_occ(X5,X6))=>X4=X5),file('/tmp/SRASS.s.p', sos_29)).
% fof(5, axiom,![X8]:![X9]:![X10]:(min_precedes(X9,X10,X8)=>?[X11]:((occurrence_of(X11,X8)&subactivity_occurrence(X9,X11))&subactivity_occurrence(X10,X11))),file('/tmp/SRASS.s.p', sos_06)).
% fof(6, axiom,![X12]:![X13]:![X14]:((occurrence_of(X12,X14)&leaf_occ(X13,X12))=>~(?[X15]:min_precedes(X13,X15,X14))),file('/tmp/SRASS.s.p', sos_09)).
% fof(7, axiom,![X16]:![X17]:![X18]:![X19]:(((min_precedes(X16,X17,X18)&occurrence_of(X19,X18))&subactivity_occurrence(X17,X19))=>subactivity_occurrence(X16,X19)),file('/tmp/SRASS.s.p', sos_27)).
% fof(9, axiom,![X24]:![X25]:((((occurrence_of(X25,tptp0)&subactivity_occurrence(X24,X25))&arboreal(X24))&~(leaf_occ(X24,X25)))=>?[X26]:(occurrence_of(X26,tptp1)&next_subocc(X24,X26,tptp0))),file('/tmp/SRASS.s.p', sos_45)).
% fof(10, axiom,![X27]:![X28]:(occurrence_of(X27,X28)=>(arboreal(X27)<=>atomic(X28))),file('/tmp/SRASS.s.p', sos_16)).
% fof(13, axiom,![X34]:(occurrence_of(X34,tptp0)=>?[X35]:?[X36]:((((occurrence_of(X35,tptp4)&root_occ(X35,X34))&occurrence_of(X36,tptp3))&leaf_occ(X36,X34))&next_subocc(X35,X36,tptp0))),file('/tmp/SRASS.s.p', sos_32)).
% fof(14, axiom,![X37]:![X38]:((leaf(X37,X38)&~(atomic(X38)))=>?[X39]:(occurrence_of(X39,X38)&leaf_occ(X37,X39))),file('/tmp/SRASS.s.p', sos_07)).
% fof(15, axiom,![X40]:![X41]:![X42]:(min_precedes(X40,X41,X42)=>~(root(X41,X42))),file('/tmp/SRASS.s.p', sos_22)).
% fof(16, axiom,![X43]:![X44]:![X45]:(min_precedes(X43,X44,X45)=>?[X46]:(root(X46,X45)&min_precedes(X46,X44,X45))),file('/tmp/SRASS.s.p', sos_23)).
% fof(17, axiom,atomic(tptp4),file('/tmp/SRASS.s.p', sos_35)).
% fof(21, axiom,![X47]:![X48]:![X49]:(min_precedes(X47,X48,X49)=>precedes(X47,X48)),file('/tmp/SRASS.s.p', sos_24)).
% fof(22, axiom,![X50]:![X51]:![X52]:(next_subocc(X50,X51,X52)<=>(min_precedes(X50,X51,X52)&~(?[X53]:(min_precedes(X50,X53,X52)&min_precedes(X53,X51,X52))))),file('/tmp/SRASS.s.p', sos_26)).
% fof(23, axiom,![X54]:![X55]:![X56]:![X57]:((((occurrence_of(X56,X57)&~(atomic(X57)))&leaf_occ(X54,X56))&leaf_occ(X55,X56))=>X54=X55),file('/tmp/SRASS.s.p', sos_28)).
% fof(25, axiom,![X62]:![X63]:(occurrence_of(X63,X62)=>(activity(X62)&activity_occurrence(X63))),file('/tmp/SRASS.s.p', sos_03)).
% fof(26, axiom,![X64]:(activity_occurrence(X64)=>?[X65]:(activity(X65)&occurrence_of(X64,X65))),file('/tmp/SRASS.s.p', sos_12)).
% fof(27, axiom,![X66]:![X67]:![X68]:![X69]:(((((occurrence_of(X67,X66)&arboreal(X68))&arboreal(X69))&subactivity_occurrence(X68,X67))&subactivity_occurrence(X69,X67))=>((min_precedes(X68,X69,X66)|min_precedes(X69,X68,X66))|X68=X69)),file('/tmp/SRASS.s.p', sos_04)).
% fof(29, axiom,![X72]:![X73]:(root(X73,X72)=>?[X74]:(subactivity(X74,X72)&atocc(X73,X74))),file('/tmp/SRASS.s.p', sos_05)).
% fof(31, axiom,![X80]:![X81]:![X82]:![X83]:(((((occurrence_of(X81,X80)&subactivity_occurrence(X82,X81))&leaf_occ(X83,X81))&arboreal(X82))&~(min_precedes(X82,X83,X80)))=>X83=X82),file('/tmp/SRASS.s.p', sos_02)).
% fof(32, axiom,![X84]:(legal(X84)=>arboreal(X84)),file('/tmp/SRASS.s.p', sos_13)).
% fof(33, axiom,![X85]:![X86]:(root_occ(X85,X86)<=>?[X87]:((occurrence_of(X86,X87)&subactivity_occurrence(X85,X86))&root(X85,X87))),file('/tmp/SRASS.s.p', sos_19)).
% fof(34, axiom,![X88]:![X89]:![X90]:(next_subocc(X88,X89,X90)=>(arboreal(X88)&arboreal(X89))),file('/tmp/SRASS.s.p', sos_25)).
% fof(35, axiom,![X91]:![X92]:((occurrence_of(X92,X91)&~(atomic(X91)))=>?[X93]:(root(X93,X91)&subactivity_occurrence(X93,X92))),file('/tmp/SRASS.s.p', sos)).
% fof(36, axiom,![X94]:![X95]:(leaf_occ(X94,X95)<=>?[X96]:((occurrence_of(X95,X96)&subactivity_occurrence(X94,X95))&leaf(X94,X96))),file('/tmp/SRASS.s.p', sos_18)).
% fof(40, axiom,~(tptp1=tptp3),file('/tmp/SRASS.s.p', sos_42)).
% fof(43, axiom,![X97]:![X98]:(atocc(X97,X98)<=>?[X99]:((subactivity(X98,X99)&atomic(X99))&occurrence_of(X97,X99))),file('/tmp/SRASS.s.p', sos_14)).
% fof(44, axiom,![X100]:![X101]:(leaf(X100,X101)<=>((root(X100,X101)|?[X102]:min_precedes(X102,X100,X101))&~(?[X103]:min_precedes(X100,X103,X101)))),file('/tmp/SRASS.s.p', sos_15)).
% fof(46, axiom,![X106]:![X107]:(precedes(X106,X107)<=>(earlier(X106,X107)&legal(X107))),file('/tmp/SRASS.s.p', sos_21)).
% fof(47, conjecture,~(?[X108]:occurrence_of(X108,tptp0)),file('/tmp/SRASS.s.p', goals)).
% fof(48, negated_conjecture,~(~(?[X108]:occurrence_of(X108,tptp0))),inference(assume_negation,[status(cth)],[47])).
% fof(49, plain,~(atomic(tptp0)),inference(fof_simplification,[status(thm)],[1,theory(equality)])).
% fof(50, plain,![X24]:![X25]:((((occurrence_of(X25,tptp0)&subactivity_occurrence(X24,X25))&arboreal(X24))&~(leaf_occ(X24,X25)))=>?[X26]:(occurrence_of(X26,tptp1)&next_subocc(X24,X26,tptp0))),inference(fof_simplification,[status(thm)],[9,theory(equality)])).
% fof(52, plain,![X37]:![X38]:((leaf(X37,X38)&~(atomic(X38)))=>?[X39]:(occurrence_of(X39,X38)&leaf_occ(X37,X39))),inference(fof_simplification,[status(thm)],[14,theory(equality)])).
% fof(53, plain,![X40]:![X41]:![X42]:(min_precedes(X40,X41,X42)=>~(root(X41,X42))),inference(fof_simplification,[status(thm)],[15,theory(equality)])).
% fof(54, plain,![X54]:![X55]:![X56]:![X57]:((((occurrence_of(X56,X57)&~(atomic(X57)))&leaf_occ(X54,X56))&leaf_occ(X55,X56))=>X54=X55),inference(fof_simplification,[status(thm)],[23,theory(equality)])).
% fof(55, plain,![X80]:![X81]:![X82]:![X83]:(((((occurrence_of(X81,X80)&subactivity_occurrence(X82,X81))&leaf_occ(X83,X81))&arboreal(X82))&~(min_precedes(X82,X83,X80)))=>X83=X82),inference(fof_simplification,[status(thm)],[31,theory(equality)])).
% fof(56, plain,![X91]:![X92]:((occurrence_of(X92,X91)&~(atomic(X91)))=>?[X93]:(root(X93,X91)&subactivity_occurrence(X93,X92))),inference(fof_simplification,[status(thm)],[35,theory(equality)])).
% cnf(57,plain,(~atomic(tptp0)),inference(split_conjunct,[status(thm)],[49])).
% fof(59, plain,![X1]:![X2]:![X3]:((~(occurrence_of(X1,X2))|~(occurrence_of(X1,X3)))|X2=X3),inference(fof_nnf,[status(thm)],[3])).
% fof(60, plain,![X4]:![X5]:![X6]:((~(occurrence_of(X4,X5))|~(occurrence_of(X4,X6)))|X5=X6),inference(variable_rename,[status(thm)],[59])).
% cnf(61,plain,(X1=X2|~occurrence_of(X3,X2)|~occurrence_of(X3,X1)),inference(split_conjunct,[status(thm)],[60])).
% fof(62, plain,![X4]:![X5]:![X6]:![X7]:(((~(occurrence_of(X6,X7))|~(root_occ(X4,X6)))|~(root_occ(X5,X6)))|X4=X5),inference(fof_nnf,[status(thm)],[4])).
% fof(63, plain,![X8]:![X9]:![X10]:![X11]:(((~(occurrence_of(X10,X11))|~(root_occ(X8,X10)))|~(root_occ(X9,X10)))|X8=X9),inference(variable_rename,[status(thm)],[62])).
% cnf(64,plain,(X1=X2|~root_occ(X2,X3)|~root_occ(X1,X3)|~occurrence_of(X3,X4)),inference(split_conjunct,[status(thm)],[63])).
% fof(65, plain,![X8]:![X9]:![X10]:(~(min_precedes(X9,X10,X8))|?[X11]:((occurrence_of(X11,X8)&subactivity_occurrence(X9,X11))&subactivity_occurrence(X10,X11))),inference(fof_nnf,[status(thm)],[5])).
% fof(66, plain,![X12]:![X13]:![X14]:(~(min_precedes(X13,X14,X12))|?[X15]:((occurrence_of(X15,X12)&subactivity_occurrence(X13,X15))&subactivity_occurrence(X14,X15))),inference(variable_rename,[status(thm)],[65])).
% fof(67, plain,![X12]:![X13]:![X14]:(~(min_precedes(X13,X14,X12))|((occurrence_of(esk1_3(X12,X13,X14),X12)&subactivity_occurrence(X13,esk1_3(X12,X13,X14)))&subactivity_occurrence(X14,esk1_3(X12,X13,X14)))),inference(skolemize,[status(esa)],[66])).
% fof(68, plain,![X12]:![X13]:![X14]:(((occurrence_of(esk1_3(X12,X13,X14),X12)|~(min_precedes(X13,X14,X12)))&(subactivity_occurrence(X13,esk1_3(X12,X13,X14))|~(min_precedes(X13,X14,X12))))&(subactivity_occurrence(X14,esk1_3(X12,X13,X14))|~(min_precedes(X13,X14,X12)))),inference(distribute,[status(thm)],[67])).
% cnf(69,plain,(subactivity_occurrence(X2,esk1_3(X3,X1,X2))|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[68])).
% cnf(70,plain,(subactivity_occurrence(X1,esk1_3(X3,X1,X2))|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[68])).
% cnf(71,plain,(occurrence_of(esk1_3(X3,X1,X2),X3)|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[68])).
% fof(72, plain,![X12]:![X13]:![X14]:((~(occurrence_of(X12,X14))|~(leaf_occ(X13,X12)))|![X15]:~(min_precedes(X13,X15,X14))),inference(fof_nnf,[status(thm)],[6])).
% fof(73, plain,![X16]:![X17]:![X18]:((~(occurrence_of(X16,X18))|~(leaf_occ(X17,X16)))|![X19]:~(min_precedes(X17,X19,X18))),inference(variable_rename,[status(thm)],[72])).
% fof(74, plain,![X16]:![X17]:![X18]:![X19]:(~(min_precedes(X17,X19,X18))|(~(occurrence_of(X16,X18))|~(leaf_occ(X17,X16)))),inference(shift_quantors,[status(thm)],[73])).
% cnf(75,plain,(~leaf_occ(X1,X2)|~occurrence_of(X2,X3)|~min_precedes(X1,X4,X3)),inference(split_conjunct,[status(thm)],[74])).
% fof(76, plain,![X16]:![X17]:![X18]:![X19]:(((~(min_precedes(X16,X17,X18))|~(occurrence_of(X19,X18)))|~(subactivity_occurrence(X17,X19)))|subactivity_occurrence(X16,X19)),inference(fof_nnf,[status(thm)],[7])).
% fof(77, plain,![X20]:![X21]:![X22]:![X23]:(((~(min_precedes(X20,X21,X22))|~(occurrence_of(X23,X22)))|~(subactivity_occurrence(X21,X23)))|subactivity_occurrence(X20,X23)),inference(variable_rename,[status(thm)],[76])).
% cnf(78,plain,(subactivity_occurrence(X1,X2)|~subactivity_occurrence(X3,X2)|~occurrence_of(X2,X4)|~min_precedes(X1,X3,X4)),inference(split_conjunct,[status(thm)],[77])).
% fof(83, plain,![X24]:![X25]:((((~(occurrence_of(X25,tptp0))|~(subactivity_occurrence(X24,X25)))|~(arboreal(X24)))|leaf_occ(X24,X25))|?[X26]:(occurrence_of(X26,tptp1)&next_subocc(X24,X26,tptp0))),inference(fof_nnf,[status(thm)],[50])).
% fof(84, plain,![X27]:![X28]:((((~(occurrence_of(X28,tptp0))|~(subactivity_occurrence(X27,X28)))|~(arboreal(X27)))|leaf_occ(X27,X28))|?[X29]:(occurrence_of(X29,tptp1)&next_subocc(X27,X29,tptp0))),inference(variable_rename,[status(thm)],[83])).
% fof(85, plain,![X27]:![X28]:((((~(occurrence_of(X28,tptp0))|~(subactivity_occurrence(X27,X28)))|~(arboreal(X27)))|leaf_occ(X27,X28))|(occurrence_of(esk2_2(X27,X28),tptp1)&next_subocc(X27,esk2_2(X27,X28),tptp0))),inference(skolemize,[status(esa)],[84])).
% fof(86, plain,![X27]:![X28]:((occurrence_of(esk2_2(X27,X28),tptp1)|(((~(occurrence_of(X28,tptp0))|~(subactivity_occurrence(X27,X28)))|~(arboreal(X27)))|leaf_occ(X27,X28)))&(next_subocc(X27,esk2_2(X27,X28),tptp0)|(((~(occurrence_of(X28,tptp0))|~(subactivity_occurrence(X27,X28)))|~(arboreal(X27)))|leaf_occ(X27,X28)))),inference(distribute,[status(thm)],[85])).
% cnf(87,plain,(leaf_occ(X1,X2)|next_subocc(X1,esk2_2(X1,X2),tptp0)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(split_conjunct,[status(thm)],[86])).
% cnf(88,plain,(leaf_occ(X1,X2)|occurrence_of(esk2_2(X1,X2),tptp1)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(split_conjunct,[status(thm)],[86])).
% fof(89, plain,![X27]:![X28]:(~(occurrence_of(X27,X28))|((~(arboreal(X27))|atomic(X28))&(~(atomic(X28))|arboreal(X27)))),inference(fof_nnf,[status(thm)],[10])).
% fof(90, plain,![X29]:![X30]:(~(occurrence_of(X29,X30))|((~(arboreal(X29))|atomic(X30))&(~(atomic(X30))|arboreal(X29)))),inference(variable_rename,[status(thm)],[89])).
% fof(91, plain,![X29]:![X30]:(((~(arboreal(X29))|atomic(X30))|~(occurrence_of(X29,X30)))&((~(atomic(X30))|arboreal(X29))|~(occurrence_of(X29,X30)))),inference(distribute,[status(thm)],[90])).
% cnf(92,plain,(arboreal(X1)|~occurrence_of(X1,X2)|~atomic(X2)),inference(split_conjunct,[status(thm)],[91])).
% cnf(93,plain,(atomic(X2)|~occurrence_of(X1,X2)|~arboreal(X1)),inference(split_conjunct,[status(thm)],[91])).
% fof(100, plain,![X34]:(~(occurrence_of(X34,tptp0))|?[X35]:?[X36]:((((occurrence_of(X35,tptp4)&root_occ(X35,X34))&occurrence_of(X36,tptp3))&leaf_occ(X36,X34))&next_subocc(X35,X36,tptp0))),inference(fof_nnf,[status(thm)],[13])).
% fof(101, plain,![X37]:(~(occurrence_of(X37,tptp0))|?[X38]:?[X39]:((((occurrence_of(X38,tptp4)&root_occ(X38,X37))&occurrence_of(X39,tptp3))&leaf_occ(X39,X37))&next_subocc(X38,X39,tptp0))),inference(variable_rename,[status(thm)],[100])).
% fof(102, plain,![X37]:(~(occurrence_of(X37,tptp0))|((((occurrence_of(esk3_1(X37),tptp4)&root_occ(esk3_1(X37),X37))&occurrence_of(esk4_1(X37),tptp3))&leaf_occ(esk4_1(X37),X37))&next_subocc(esk3_1(X37),esk4_1(X37),tptp0))),inference(skolemize,[status(esa)],[101])).
% fof(103, plain,![X37]:(((((occurrence_of(esk3_1(X37),tptp4)|~(occurrence_of(X37,tptp0)))&(root_occ(esk3_1(X37),X37)|~(occurrence_of(X37,tptp0))))&(occurrence_of(esk4_1(X37),tptp3)|~(occurrence_of(X37,tptp0))))&(leaf_occ(esk4_1(X37),X37)|~(occurrence_of(X37,tptp0))))&(next_subocc(esk3_1(X37),esk4_1(X37),tptp0)|~(occurrence_of(X37,tptp0)))),inference(distribute,[status(thm)],[102])).
% cnf(104,plain,(next_subocc(esk3_1(X1),esk4_1(X1),tptp0)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[103])).
% cnf(105,plain,(leaf_occ(esk4_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[103])).
% cnf(106,plain,(occurrence_of(esk4_1(X1),tptp3)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[103])).
% cnf(107,plain,(root_occ(esk3_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[103])).
% cnf(108,plain,(occurrence_of(esk3_1(X1),tptp4)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[103])).
% fof(109, plain,![X37]:![X38]:((~(leaf(X37,X38))|atomic(X38))|?[X39]:(occurrence_of(X39,X38)&leaf_occ(X37,X39))),inference(fof_nnf,[status(thm)],[52])).
% fof(110, plain,![X40]:![X41]:((~(leaf(X40,X41))|atomic(X41))|?[X42]:(occurrence_of(X42,X41)&leaf_occ(X40,X42))),inference(variable_rename,[status(thm)],[109])).
% fof(111, plain,![X40]:![X41]:((~(leaf(X40,X41))|atomic(X41))|(occurrence_of(esk5_2(X40,X41),X41)&leaf_occ(X40,esk5_2(X40,X41)))),inference(skolemize,[status(esa)],[110])).
% fof(112, plain,![X40]:![X41]:((occurrence_of(esk5_2(X40,X41),X41)|(~(leaf(X40,X41))|atomic(X41)))&(leaf_occ(X40,esk5_2(X40,X41))|(~(leaf(X40,X41))|atomic(X41)))),inference(distribute,[status(thm)],[111])).
% cnf(113,plain,(atomic(X1)|leaf_occ(X2,esk5_2(X2,X1))|~leaf(X2,X1)),inference(split_conjunct,[status(thm)],[112])).
% cnf(114,plain,(atomic(X1)|occurrence_of(esk5_2(X2,X1),X1)|~leaf(X2,X1)),inference(split_conjunct,[status(thm)],[112])).
% fof(115, plain,![X40]:![X41]:![X42]:(~(min_precedes(X40,X41,X42))|~(root(X41,X42))),inference(fof_nnf,[status(thm)],[53])).
% fof(116, plain,![X43]:![X44]:![X45]:(~(min_precedes(X43,X44,X45))|~(root(X44,X45))),inference(variable_rename,[status(thm)],[115])).
% cnf(117,plain,(~root(X1,X2)|~min_precedes(X3,X1,X2)),inference(split_conjunct,[status(thm)],[116])).
% fof(118, plain,![X43]:![X44]:![X45]:(~(min_precedes(X43,X44,X45))|?[X46]:(root(X46,X45)&min_precedes(X46,X44,X45))),inference(fof_nnf,[status(thm)],[16])).
% fof(119, plain,![X47]:![X48]:![X49]:(~(min_precedes(X47,X48,X49))|?[X50]:(root(X50,X49)&min_precedes(X50,X48,X49))),inference(variable_rename,[status(thm)],[118])).
% fof(120, plain,![X47]:![X48]:![X49]:(~(min_precedes(X47,X48,X49))|(root(esk6_3(X47,X48,X49),X49)&min_precedes(esk6_3(X47,X48,X49),X48,X49))),inference(skolemize,[status(esa)],[119])).
% fof(121, plain,![X47]:![X48]:![X49]:((root(esk6_3(X47,X48,X49),X49)|~(min_precedes(X47,X48,X49)))&(min_precedes(esk6_3(X47,X48,X49),X48,X49)|~(min_precedes(X47,X48,X49)))),inference(distribute,[status(thm)],[120])).
% cnf(122,plain,(min_precedes(esk6_3(X1,X2,X3),X2,X3)|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[121])).
% cnf(123,plain,(root(esk6_3(X1,X2,X3),X3)|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[121])).
% cnf(124,plain,(atomic(tptp4)),inference(split_conjunct,[status(thm)],[17])).
% fof(128, plain,![X47]:![X48]:![X49]:(~(min_precedes(X47,X48,X49))|precedes(X47,X48)),inference(fof_nnf,[status(thm)],[21])).
% fof(129, plain,![X50]:![X51]:![X52]:(~(min_precedes(X50,X51,X52))|precedes(X50,X51)),inference(variable_rename,[status(thm)],[128])).
% cnf(130,plain,(precedes(X1,X2)|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[129])).
% fof(131, plain,![X50]:![X51]:![X52]:((~(next_subocc(X50,X51,X52))|(min_precedes(X50,X51,X52)&![X53]:(~(min_precedes(X50,X53,X52))|~(min_precedes(X53,X51,X52)))))&((~(min_precedes(X50,X51,X52))|?[X53]:(min_precedes(X50,X53,X52)&min_precedes(X53,X51,X52)))|next_subocc(X50,X51,X52))),inference(fof_nnf,[status(thm)],[22])).
% fof(132, plain,![X54]:![X55]:![X56]:((~(next_subocc(X54,X55,X56))|(min_precedes(X54,X55,X56)&![X57]:(~(min_precedes(X54,X57,X56))|~(min_precedes(X57,X55,X56)))))&((~(min_precedes(X54,X55,X56))|?[X58]:(min_precedes(X54,X58,X56)&min_precedes(X58,X55,X56)))|next_subocc(X54,X55,X56))),inference(variable_rename,[status(thm)],[131])).
% fof(133, plain,![X54]:![X55]:![X56]:((~(next_subocc(X54,X55,X56))|(min_precedes(X54,X55,X56)&![X57]:(~(min_precedes(X54,X57,X56))|~(min_precedes(X57,X55,X56)))))&((~(min_precedes(X54,X55,X56))|(min_precedes(X54,esk7_3(X54,X55,X56),X56)&min_precedes(esk7_3(X54,X55,X56),X55,X56)))|next_subocc(X54,X55,X56))),inference(skolemize,[status(esa)],[132])).
% fof(134, plain,![X54]:![X55]:![X56]:![X57]:((((~(min_precedes(X54,X57,X56))|~(min_precedes(X57,X55,X56)))&min_precedes(X54,X55,X56))|~(next_subocc(X54,X55,X56)))&((~(min_precedes(X54,X55,X56))|(min_precedes(X54,esk7_3(X54,X55,X56),X56)&min_precedes(esk7_3(X54,X55,X56),X55,X56)))|next_subocc(X54,X55,X56))),inference(shift_quantors,[status(thm)],[133])).
% fof(135, plain,![X54]:![X55]:![X56]:![X57]:((((~(min_precedes(X54,X57,X56))|~(min_precedes(X57,X55,X56)))|~(next_subocc(X54,X55,X56)))&(min_precedes(X54,X55,X56)|~(next_subocc(X54,X55,X56))))&(((min_precedes(X54,esk7_3(X54,X55,X56),X56)|~(min_precedes(X54,X55,X56)))|next_subocc(X54,X55,X56))&((min_precedes(esk7_3(X54,X55,X56),X55,X56)|~(min_precedes(X54,X55,X56)))|next_subocc(X54,X55,X56)))),inference(distribute,[status(thm)],[134])).
% cnf(136,plain,(next_subocc(X1,X2,X3)|min_precedes(esk7_3(X1,X2,X3),X2,X3)|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[135])).
% cnf(137,plain,(next_subocc(X1,X2,X3)|min_precedes(X1,esk7_3(X1,X2,X3),X3)|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[135])).
% cnf(138,plain,(min_precedes(X1,X2,X3)|~next_subocc(X1,X2,X3)),inference(split_conjunct,[status(thm)],[135])).
% cnf(139,plain,(~next_subocc(X1,X2,X3)|~min_precedes(X4,X2,X3)|~min_precedes(X1,X4,X3)),inference(split_conjunct,[status(thm)],[135])).
% fof(140, plain,![X54]:![X55]:![X56]:![X57]:((((~(occurrence_of(X56,X57))|atomic(X57))|~(leaf_occ(X54,X56)))|~(leaf_occ(X55,X56)))|X54=X55),inference(fof_nnf,[status(thm)],[54])).
% fof(141, plain,![X58]:![X59]:![X60]:![X61]:((((~(occurrence_of(X60,X61))|atomic(X61))|~(leaf_occ(X58,X60)))|~(leaf_occ(X59,X60)))|X58=X59),inference(variable_rename,[status(thm)],[140])).
% cnf(142,plain,(X1=X2|atomic(X4)|~leaf_occ(X2,X3)|~leaf_occ(X1,X3)|~occurrence_of(X3,X4)),inference(split_conjunct,[status(thm)],[141])).
% fof(146, plain,![X62]:![X63]:(~(occurrence_of(X63,X62))|(activity(X62)&activity_occurrence(X63))),inference(fof_nnf,[status(thm)],[25])).
% fof(147, plain,![X64]:![X65]:(~(occurrence_of(X65,X64))|(activity(X64)&activity_occurrence(X65))),inference(variable_rename,[status(thm)],[146])).
% fof(148, plain,![X64]:![X65]:((activity(X64)|~(occurrence_of(X65,X64)))&(activity_occurrence(X65)|~(occurrence_of(X65,X64)))),inference(distribute,[status(thm)],[147])).
% cnf(149,plain,(activity_occurrence(X1)|~occurrence_of(X1,X2)),inference(split_conjunct,[status(thm)],[148])).
% fof(151, plain,![X64]:(~(activity_occurrence(X64))|?[X65]:(activity(X65)&occurrence_of(X64,X65))),inference(fof_nnf,[status(thm)],[26])).
% fof(152, plain,![X66]:(~(activity_occurrence(X66))|?[X67]:(activity(X67)&occurrence_of(X66,X67))),inference(variable_rename,[status(thm)],[151])).
% fof(153, plain,![X66]:(~(activity_occurrence(X66))|(activity(esk8_1(X66))&occurrence_of(X66,esk8_1(X66)))),inference(skolemize,[status(esa)],[152])).
% fof(154, plain,![X66]:((activity(esk8_1(X66))|~(activity_occurrence(X66)))&(occurrence_of(X66,esk8_1(X66))|~(activity_occurrence(X66)))),inference(distribute,[status(thm)],[153])).
% cnf(155,plain,(occurrence_of(X1,esk8_1(X1))|~activity_occurrence(X1)),inference(split_conjunct,[status(thm)],[154])).
% fof(157, plain,![X66]:![X67]:![X68]:![X69]:(((((~(occurrence_of(X67,X66))|~(arboreal(X68)))|~(arboreal(X69)))|~(subactivity_occurrence(X68,X67)))|~(subactivity_occurrence(X69,X67)))|((min_precedes(X68,X69,X66)|min_precedes(X69,X68,X66))|X68=X69)),inference(fof_nnf,[status(thm)],[27])).
% fof(158, plain,![X70]:![X71]:![X72]:![X73]:(((((~(occurrence_of(X71,X70))|~(arboreal(X72)))|~(arboreal(X73)))|~(subactivity_occurrence(X72,X71)))|~(subactivity_occurrence(X73,X71)))|((min_precedes(X72,X73,X70)|min_precedes(X73,X72,X70))|X72=X73)),inference(variable_rename,[status(thm)],[157])).
% cnf(159,plain,(X1=X2|min_precedes(X2,X1,X3)|min_precedes(X1,X2,X3)|~subactivity_occurrence(X2,X4)|~subactivity_occurrence(X1,X4)|~arboreal(X2)|~arboreal(X1)|~occurrence_of(X4,X3)),inference(split_conjunct,[status(thm)],[158])).
% fof(165, plain,![X72]:![X73]:(~(root(X73,X72))|?[X74]:(subactivity(X74,X72)&atocc(X73,X74))),inference(fof_nnf,[status(thm)],[29])).
% fof(166, plain,![X75]:![X76]:(~(root(X76,X75))|?[X77]:(subactivity(X77,X75)&atocc(X76,X77))),inference(variable_rename,[status(thm)],[165])).
% fof(167, plain,![X75]:![X76]:(~(root(X76,X75))|(subactivity(esk9_2(X75,X76),X75)&atocc(X76,esk9_2(X75,X76)))),inference(skolemize,[status(esa)],[166])).
% fof(168, plain,![X75]:![X76]:((subactivity(esk9_2(X75,X76),X75)|~(root(X76,X75)))&(atocc(X76,esk9_2(X75,X76))|~(root(X76,X75)))),inference(distribute,[status(thm)],[167])).
% cnf(169,plain,(atocc(X1,esk9_2(X2,X1))|~root(X1,X2)),inference(split_conjunct,[status(thm)],[168])).
% cnf(170,plain,(subactivity(esk9_2(X2,X1),X2)|~root(X1,X2)),inference(split_conjunct,[status(thm)],[168])).
% fof(174, plain,![X80]:![X81]:![X82]:![X83]:(((((~(occurrence_of(X81,X80))|~(subactivity_occurrence(X82,X81)))|~(leaf_occ(X83,X81)))|~(arboreal(X82)))|min_precedes(X82,X83,X80))|X83=X82),inference(fof_nnf,[status(thm)],[55])).
% fof(175, plain,![X84]:![X85]:![X86]:![X87]:(((((~(occurrence_of(X85,X84))|~(subactivity_occurrence(X86,X85)))|~(leaf_occ(X87,X85)))|~(arboreal(X86)))|min_precedes(X86,X87,X84))|X87=X86),inference(variable_rename,[status(thm)],[174])).
% cnf(176,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)],[175])).
% fof(177, plain,![X84]:(~(legal(X84))|arboreal(X84)),inference(fof_nnf,[status(thm)],[32])).
% fof(178, plain,![X85]:(~(legal(X85))|arboreal(X85)),inference(variable_rename,[status(thm)],[177])).
% cnf(179,plain,(arboreal(X1)|~legal(X1)),inference(split_conjunct,[status(thm)],[178])).
% fof(180, plain,![X85]:![X86]:((~(root_occ(X85,X86))|?[X87]:((occurrence_of(X86,X87)&subactivity_occurrence(X85,X86))&root(X85,X87)))&(![X87]:((~(occurrence_of(X86,X87))|~(subactivity_occurrence(X85,X86)))|~(root(X85,X87)))|root_occ(X85,X86))),inference(fof_nnf,[status(thm)],[33])).
% fof(181, plain,![X88]:![X89]:((~(root_occ(X88,X89))|?[X90]:((occurrence_of(X89,X90)&subactivity_occurrence(X88,X89))&root(X88,X90)))&(![X91]:((~(occurrence_of(X89,X91))|~(subactivity_occurrence(X88,X89)))|~(root(X88,X91)))|root_occ(X88,X89))),inference(variable_rename,[status(thm)],[180])).
% fof(182, plain,![X88]:![X89]:((~(root_occ(X88,X89))|((occurrence_of(X89,esk10_2(X88,X89))&subactivity_occurrence(X88,X89))&root(X88,esk10_2(X88,X89))))&(![X91]:((~(occurrence_of(X89,X91))|~(subactivity_occurrence(X88,X89)))|~(root(X88,X91)))|root_occ(X88,X89))),inference(skolemize,[status(esa)],[181])).
% fof(183, plain,![X88]:![X89]:![X91]:((((~(occurrence_of(X89,X91))|~(subactivity_occurrence(X88,X89)))|~(root(X88,X91)))|root_occ(X88,X89))&(~(root_occ(X88,X89))|((occurrence_of(X89,esk10_2(X88,X89))&subactivity_occurrence(X88,X89))&root(X88,esk10_2(X88,X89))))),inference(shift_quantors,[status(thm)],[182])).
% fof(184, plain,![X88]:![X89]:![X91]:((((~(occurrence_of(X89,X91))|~(subactivity_occurrence(X88,X89)))|~(root(X88,X91)))|root_occ(X88,X89))&(((occurrence_of(X89,esk10_2(X88,X89))|~(root_occ(X88,X89)))&(subactivity_occurrence(X88,X89)|~(root_occ(X88,X89))))&(root(X88,esk10_2(X88,X89))|~(root_occ(X88,X89))))),inference(distribute,[status(thm)],[183])).
% cnf(185,plain,(root(X1,esk10_2(X1,X2))|~root_occ(X1,X2)),inference(split_conjunct,[status(thm)],[184])).
% cnf(186,plain,(subactivity_occurrence(X1,X2)|~root_occ(X1,X2)),inference(split_conjunct,[status(thm)],[184])).
% cnf(187,plain,(occurrence_of(X2,esk10_2(X1,X2))|~root_occ(X1,X2)),inference(split_conjunct,[status(thm)],[184])).
% cnf(188,plain,(root_occ(X1,X2)|~root(X1,X3)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,X3)),inference(split_conjunct,[status(thm)],[184])).
% fof(189, plain,![X88]:![X89]:![X90]:(~(next_subocc(X88,X89,X90))|(arboreal(X88)&arboreal(X89))),inference(fof_nnf,[status(thm)],[34])).
% fof(190, plain,![X91]:![X92]:![X93]:(~(next_subocc(X91,X92,X93))|(arboreal(X91)&arboreal(X92))),inference(variable_rename,[status(thm)],[189])).
% fof(191, plain,![X91]:![X92]:![X93]:((arboreal(X91)|~(next_subocc(X91,X92,X93)))&(arboreal(X92)|~(next_subocc(X91,X92,X93)))),inference(distribute,[status(thm)],[190])).
% cnf(192,plain,(arboreal(X2)|~next_subocc(X1,X2,X3)),inference(split_conjunct,[status(thm)],[191])).
% fof(194, plain,![X91]:![X92]:((~(occurrence_of(X92,X91))|atomic(X91))|?[X93]:(root(X93,X91)&subactivity_occurrence(X93,X92))),inference(fof_nnf,[status(thm)],[56])).
% fof(195, plain,![X94]:![X95]:((~(occurrence_of(X95,X94))|atomic(X94))|?[X96]:(root(X96,X94)&subactivity_occurrence(X96,X95))),inference(variable_rename,[status(thm)],[194])).
% fof(196, plain,![X94]:![X95]:((~(occurrence_of(X95,X94))|atomic(X94))|(root(esk11_2(X94,X95),X94)&subactivity_occurrence(esk11_2(X94,X95),X95))),inference(skolemize,[status(esa)],[195])).
% fof(197, plain,![X94]:![X95]:((root(esk11_2(X94,X95),X94)|(~(occurrence_of(X95,X94))|atomic(X94)))&(subactivity_occurrence(esk11_2(X94,X95),X95)|(~(occurrence_of(X95,X94))|atomic(X94)))),inference(distribute,[status(thm)],[196])).
% cnf(198,plain,(atomic(X1)|subactivity_occurrence(esk11_2(X1,X2),X2)|~occurrence_of(X2,X1)),inference(split_conjunct,[status(thm)],[197])).
% cnf(199,plain,(atomic(X1)|root(esk11_2(X1,X2),X1)|~occurrence_of(X2,X1)),inference(split_conjunct,[status(thm)],[197])).
% fof(200, plain,![X94]:![X95]:((~(leaf_occ(X94,X95))|?[X96]:((occurrence_of(X95,X96)&subactivity_occurrence(X94,X95))&leaf(X94,X96)))&(![X96]:((~(occurrence_of(X95,X96))|~(subactivity_occurrence(X94,X95)))|~(leaf(X94,X96)))|leaf_occ(X94,X95))),inference(fof_nnf,[status(thm)],[36])).
% fof(201, plain,![X97]:![X98]:((~(leaf_occ(X97,X98))|?[X99]:((occurrence_of(X98,X99)&subactivity_occurrence(X97,X98))&leaf(X97,X99)))&(![X100]:((~(occurrence_of(X98,X100))|~(subactivity_occurrence(X97,X98)))|~(leaf(X97,X100)))|leaf_occ(X97,X98))),inference(variable_rename,[status(thm)],[200])).
% fof(202, plain,![X97]:![X98]:((~(leaf_occ(X97,X98))|((occurrence_of(X98,esk12_2(X97,X98))&subactivity_occurrence(X97,X98))&leaf(X97,esk12_2(X97,X98))))&(![X100]:((~(occurrence_of(X98,X100))|~(subactivity_occurrence(X97,X98)))|~(leaf(X97,X100)))|leaf_occ(X97,X98))),inference(skolemize,[status(esa)],[201])).
% fof(203, plain,![X97]:![X98]:![X100]:((((~(occurrence_of(X98,X100))|~(subactivity_occurrence(X97,X98)))|~(leaf(X97,X100)))|leaf_occ(X97,X98))&(~(leaf_occ(X97,X98))|((occurrence_of(X98,esk12_2(X97,X98))&subactivity_occurrence(X97,X98))&leaf(X97,esk12_2(X97,X98))))),inference(shift_quantors,[status(thm)],[202])).
% fof(204, plain,![X97]:![X98]:![X100]:((((~(occurrence_of(X98,X100))|~(subactivity_occurrence(X97,X98)))|~(leaf(X97,X100)))|leaf_occ(X97,X98))&(((occurrence_of(X98,esk12_2(X97,X98))|~(leaf_occ(X97,X98)))&(subactivity_occurrence(X97,X98)|~(leaf_occ(X97,X98))))&(leaf(X97,esk12_2(X97,X98))|~(leaf_occ(X97,X98))))),inference(distribute,[status(thm)],[203])).
% cnf(205,plain,(leaf(X1,esk12_2(X1,X2))|~leaf_occ(X1,X2)),inference(split_conjunct,[status(thm)],[204])).
% cnf(206,plain,(subactivity_occurrence(X1,X2)|~leaf_occ(X1,X2)),inference(split_conjunct,[status(thm)],[204])).
% cnf(207,plain,(occurrence_of(X2,esk12_2(X1,X2))|~leaf_occ(X1,X2)),inference(split_conjunct,[status(thm)],[204])).
% cnf(212,plain,(tptp1!=tptp3),inference(split_conjunct,[status(thm)],[40])).
% fof(215, plain,![X97]:![X98]:((~(atocc(X97,X98))|?[X99]:((subactivity(X98,X99)&atomic(X99))&occurrence_of(X97,X99)))&(![X99]:((~(subactivity(X98,X99))|~(atomic(X99)))|~(occurrence_of(X97,X99)))|atocc(X97,X98))),inference(fof_nnf,[status(thm)],[43])).
% fof(216, plain,![X100]:![X101]:((~(atocc(X100,X101))|?[X102]:((subactivity(X101,X102)&atomic(X102))&occurrence_of(X100,X102)))&(![X103]:((~(subactivity(X101,X103))|~(atomic(X103)))|~(occurrence_of(X100,X103)))|atocc(X100,X101))),inference(variable_rename,[status(thm)],[215])).
% fof(217, plain,![X100]:![X101]:((~(atocc(X100,X101))|((subactivity(X101,esk13_2(X100,X101))&atomic(esk13_2(X100,X101)))&occurrence_of(X100,esk13_2(X100,X101))))&(![X103]:((~(subactivity(X101,X103))|~(atomic(X103)))|~(occurrence_of(X100,X103)))|atocc(X100,X101))),inference(skolemize,[status(esa)],[216])).
% fof(218, plain,![X100]:![X101]:![X103]:((((~(subactivity(X101,X103))|~(atomic(X103)))|~(occurrence_of(X100,X103)))|atocc(X100,X101))&(~(atocc(X100,X101))|((subactivity(X101,esk13_2(X100,X101))&atomic(esk13_2(X100,X101)))&occurrence_of(X100,esk13_2(X100,X101))))),inference(shift_quantors,[status(thm)],[217])).
% fof(219, plain,![X100]:![X101]:![X103]:((((~(subactivity(X101,X103))|~(atomic(X103)))|~(occurrence_of(X100,X103)))|atocc(X100,X101))&(((subactivity(X101,esk13_2(X100,X101))|~(atocc(X100,X101)))&(atomic(esk13_2(X100,X101))|~(atocc(X100,X101))))&(occurrence_of(X100,esk13_2(X100,X101))|~(atocc(X100,X101))))),inference(distribute,[status(thm)],[218])).
% cnf(220,plain,(occurrence_of(X1,esk13_2(X1,X2))|~atocc(X1,X2)),inference(split_conjunct,[status(thm)],[219])).
% cnf(221,plain,(atomic(esk13_2(X1,X2))|~atocc(X1,X2)),inference(split_conjunct,[status(thm)],[219])).
% cnf(222,plain,(subactivity(X2,esk13_2(X1,X2))|~atocc(X1,X2)),inference(split_conjunct,[status(thm)],[219])).
% cnf(223,plain,(atocc(X1,X2)|~occurrence_of(X1,X3)|~atomic(X3)|~subactivity(X2,X3)),inference(split_conjunct,[status(thm)],[219])).
% fof(224, plain,![X100]:![X101]:((~(leaf(X100,X101))|((root(X100,X101)|?[X102]:min_precedes(X102,X100,X101))&![X103]:~(min_precedes(X100,X103,X101))))&(((~(root(X100,X101))&![X102]:~(min_precedes(X102,X100,X101)))|?[X103]:min_precedes(X100,X103,X101))|leaf(X100,X101))),inference(fof_nnf,[status(thm)],[44])).
% fof(225, plain,![X104]:![X105]:((~(leaf(X104,X105))|((root(X104,X105)|?[X106]:min_precedes(X106,X104,X105))&![X107]:~(min_precedes(X104,X107,X105))))&(((~(root(X104,X105))&![X108]:~(min_precedes(X108,X104,X105)))|?[X109]:min_precedes(X104,X109,X105))|leaf(X104,X105))),inference(variable_rename,[status(thm)],[224])).
% fof(226, plain,![X104]:![X105]:((~(leaf(X104,X105))|((root(X104,X105)|min_precedes(esk14_2(X104,X105),X104,X105))&![X107]:~(min_precedes(X104,X107,X105))))&(((~(root(X104,X105))&![X108]:~(min_precedes(X108,X104,X105)))|min_precedes(X104,esk15_2(X104,X105),X105))|leaf(X104,X105))),inference(skolemize,[status(esa)],[225])).
% fof(227, plain,![X104]:![X105]:![X107]:![X108]:((((~(min_precedes(X108,X104,X105))&~(root(X104,X105)))|min_precedes(X104,esk15_2(X104,X105),X105))|leaf(X104,X105))&((~(min_precedes(X104,X107,X105))&(root(X104,X105)|min_precedes(esk14_2(X104,X105),X104,X105)))|~(leaf(X104,X105)))),inference(shift_quantors,[status(thm)],[226])).
% fof(228, plain,![X104]:![X105]:![X107]:![X108]:((((~(min_precedes(X108,X104,X105))|min_precedes(X104,esk15_2(X104,X105),X105))|leaf(X104,X105))&((~(root(X104,X105))|min_precedes(X104,esk15_2(X104,X105),X105))|leaf(X104,X105)))&((~(min_precedes(X104,X107,X105))|~(leaf(X104,X105)))&((root(X104,X105)|min_precedes(esk14_2(X104,X105),X104,X105))|~(leaf(X104,X105))))),inference(distribute,[status(thm)],[227])).
% cnf(230,plain,(~leaf(X1,X2)|~min_precedes(X1,X3,X2)),inference(split_conjunct,[status(thm)],[228])).
% cnf(232,plain,(leaf(X1,X2)|min_precedes(X1,esk15_2(X1,X2),X2)|~min_precedes(X3,X1,X2)),inference(split_conjunct,[status(thm)],[228])).
% fof(236, plain,![X106]:![X107]:((~(precedes(X106,X107))|(earlier(X106,X107)&legal(X107)))&((~(earlier(X106,X107))|~(legal(X107)))|precedes(X106,X107))),inference(fof_nnf,[status(thm)],[46])).
% fof(237, plain,![X108]:![X109]:((~(precedes(X108,X109))|(earlier(X108,X109)&legal(X109)))&((~(earlier(X108,X109))|~(legal(X109)))|precedes(X108,X109))),inference(variable_rename,[status(thm)],[236])).
% fof(238, plain,![X108]:![X109]:(((earlier(X108,X109)|~(precedes(X108,X109)))&(legal(X109)|~(precedes(X108,X109))))&((~(earlier(X108,X109))|~(legal(X109)))|precedes(X108,X109))),inference(distribute,[status(thm)],[237])).
% cnf(240,plain,(legal(X2)|~precedes(X1,X2)),inference(split_conjunct,[status(thm)],[238])).
% fof(242, negated_conjecture,?[X108]:occurrence_of(X108,tptp0),inference(fof_nnf,[status(thm)],[48])).
% fof(243, negated_conjecture,?[X109]:occurrence_of(X109,tptp0),inference(variable_rename,[status(thm)],[242])).
% fof(244, negated_conjecture,occurrence_of(esk16_0,tptp0),inference(skolemize,[status(esa)],[243])).
% cnf(245,negated_conjecture,(occurrence_of(esk16_0,tptp0)),inference(split_conjunct,[status(thm)],[244])).
% cnf(246,negated_conjecture,(X1=tptp0|~occurrence_of(esk16_0,X1)),inference(spm,[status(thm)],[61,245,theory(equality)])).
% cnf(249,negated_conjecture,(activity_occurrence(esk16_0)),inference(spm,[status(thm)],[149,245,theory(equality)])).
% cnf(251,plain,(X1=esk8_1(X2)|~occurrence_of(X2,X1)|~activity_occurrence(X2)),inference(spm,[status(thm)],[61,155,theory(equality)])).
% cnf(262,plain,(atomic(esk10_2(X1,X2))|~arboreal(X2)|~root_occ(X1,X2)),inference(spm,[status(thm)],[93,187,theory(equality)])).
% cnf(269,plain,(arboreal(X1)|~atomic(esk13_2(X1,X2))|~atocc(X1,X2)),inference(spm,[status(thm)],[92,220,theory(equality)])).
% cnf(273,plain,(subactivity_occurrence(esk3_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[186,107,theory(equality)])).
% cnf(274,plain,(X1=esk3_1(X2)|~root_occ(X1,X2)|~occurrence_of(X2,X3)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[64,107,theory(equality)])).
% cnf(275,plain,(subactivity_occurrence(esk4_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[206,105,theory(equality)])).
% cnf(277,plain,(arboreal(esk3_1(X1))|~atomic(tptp4)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[92,108,theory(equality)])).
% cnf(278,plain,(X1=tptp4|~occurrence_of(esk3_1(X2),X1)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[61,108,theory(equality)])).
% cnf(281,plain,(arboreal(esk3_1(X1))|$false|~occurrence_of(X1,tptp0)),inference(rw,[status(thm)],[277,124,theory(equality)])).
% cnf(282,plain,(arboreal(esk3_1(X1))|~occurrence_of(X1,tptp0)),inference(cn,[status(thm)],[281,theory(equality)])).
% cnf(294,plain,(X1=X2|~occurrence_of(esk1_3(X2,X3,X4),X1)|~min_precedes(X3,X4,X2)),inference(spm,[status(thm)],[61,71,theory(equality)])).
% cnf(302,plain,(atocc(X1,X2)|~occurrence_of(X1,esk13_2(X3,X2))|~atomic(esk13_2(X3,X2))|~atocc(X3,X2)),inference(spm,[status(thm)],[223,222,theory(equality)])).
% cnf(306,plain,(min_precedes(esk3_1(X1),esk4_1(X1),tptp0)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[138,104,theory(equality)])).
% cnf(307,plain,(~min_precedes(X2,esk4_1(X1),tptp0)|~min_precedes(esk3_1(X1),X2,tptp0)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[139,104,theory(equality)])).
% cnf(309,plain,(atocc(X1,esk9_2(X2,X3))|~occurrence_of(X1,X2)|~atomic(X2)|~root(X3,X2)),inference(spm,[status(thm)],[223,170,theory(equality)])).
% cnf(315,plain,(X1=esk4_1(X2)|atomic(X3)|~leaf_occ(X1,X2)|~occurrence_of(X2,X3)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[142,105,theory(equality)])).
% cnf(321,plain,(root_occ(esk11_2(X1,X2),X3)|atomic(X1)|~subactivity_occurrence(esk11_2(X1,X2),X3)|~occurrence_of(X3,X1)|~occurrence_of(X2,X1)),inference(spm,[status(thm)],[188,199,theory(equality)])).
% cnf(323,plain,(root_occ(esk6_3(X1,X2,X3),X4)|~subactivity_occurrence(esk6_3(X1,X2,X3),X4)|~occurrence_of(X4,X3)|~min_precedes(X1,X2,X3)),inference(spm,[status(thm)],[188,123,theory(equality)])).
% cnf(324,plain,(precedes(esk6_3(X1,X2,X3),X2)|~min_precedes(X1,X2,X3)),inference(spm,[status(thm)],[130,122,theory(equality)])).
% cnf(329,plain,(subactivity_occurrence(esk6_3(X1,X2,X3),X4)|~subactivity_occurrence(X2,X4)|~occurrence_of(X4,X3)|~min_precedes(X1,X2,X3)),inference(spm,[status(thm)],[78,122,theory(equality)])).
% cnf(331,plain,(esk4_1(X1)=X2|min_precedes(X2,esk4_1(X1),X3)|~arboreal(X2)|~subactivity_occurrence(X2,X1)|~occurrence_of(X1,X3)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[176,105,theory(equality)])).
% cnf(368,plain,(next_subocc(X1,X2,X3)|~leaf(esk7_3(X1,X2,X3),X3)|~min_precedes(X1,X2,X3)),inference(spm,[status(thm)],[230,136,theory(equality)])).
% cnf(372,plain,(subactivity_occurrence(esk7_3(X1,X2,X3),X4)|next_subocc(X1,X2,X3)|~subactivity_occurrence(X2,X4)|~occurrence_of(X4,X3)|~min_precedes(X1,X2,X3)),inference(spm,[status(thm)],[78,136,theory(equality)])).
% cnf(375,plain,(min_precedes(X1,esk2_2(X1,X2),tptp0)|leaf_occ(X1,X2)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[138,87,theory(equality)])).
% cnf(383,plain,(X1=esk11_2(X2,X3)|min_precedes(X1,esk11_2(X2,X3),X4)|min_precedes(esk11_2(X2,X3),X1,X4)|atomic(X2)|~arboreal(esk11_2(X2,X3))|~arboreal(X1)|~subactivity_occurrence(X1,X3)|~occurrence_of(X3,X4)|~occurrence_of(X3,X2)),inference(spm,[status(thm)],[159,198,theory(equality)])).
% cnf(384,plain,(X1=X2|min_precedes(X1,X2,X3)|min_precedes(X2,X1,X3)|~arboreal(X2)|~arboreal(X1)|~subactivity_occurrence(X1,esk1_3(X4,X5,X2))|~occurrence_of(esk1_3(X4,X5,X2),X3)|~min_precedes(X5,X2,X4)),inference(spm,[status(thm)],[159,69,theory(equality)])).
% cnf(385,plain,(X1=X2|min_precedes(X1,X2,X3)|min_precedes(X2,X1,X3)|~arboreal(X2)|~arboreal(X1)|~subactivity_occurrence(X1,esk1_3(X4,X2,X5))|~occurrence_of(esk1_3(X4,X2,X5),X3)|~min_precedes(X2,X5,X4)),inference(spm,[status(thm)],[159,70,theory(equality)])).
% cnf(386,negated_conjecture,(esk13_2(esk16_0,X1)=tptp0|~atocc(esk16_0,X1)),inference(spm,[status(thm)],[246,220,theory(equality)])).
% cnf(387,negated_conjecture,(esk12_2(X1,esk16_0)=tptp0|~leaf_occ(X1,esk16_0)),inference(spm,[status(thm)],[246,207,theory(equality)])).
% cnf(388,negated_conjecture,(esk10_2(X1,esk16_0)=tptp0|~root_occ(X1,esk16_0)),inference(spm,[status(thm)],[246,187,theory(equality)])).
% cnf(389,negated_conjecture,(esk8_1(esk16_0)=tptp0|~activity_occurrence(esk16_0)),inference(spm,[status(thm)],[246,155,theory(equality)])).
% cnf(390,negated_conjecture,(esk8_1(esk16_0)=tptp0|$false),inference(rw,[status(thm)],[389,249,theory(equality)])).
% cnf(391,negated_conjecture,(esk8_1(esk16_0)=tptp0),inference(cn,[status(thm)],[390,theory(equality)])).
% cnf(392,plain,(X1=esk8_1(X2)|~occurrence_of(X2,X1)),inference(csr,[status(thm)],[251,149])).
% cnf(395,plain,(tptp3=esk8_1(esk4_1(X1))|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[392,106,theory(equality)])).
% cnf(397,plain,(tptp1=esk8_1(esk2_2(X1,X2))|leaf_occ(X1,X2)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[392,88,theory(equality)])).
% cnf(398,plain,(X1=esk8_1(esk1_3(X1,X2,X3))|~min_precedes(X2,X3,X1)),inference(spm,[status(thm)],[392,71,theory(equality)])).
% cnf(399,plain,(esk13_2(X1,X2)=esk8_1(X1)|~atocc(X1,X2)),inference(spm,[status(thm)],[392,220,theory(equality)])).
% cnf(400,plain,(esk12_2(X1,X2)=esk8_1(X2)|~leaf_occ(X1,X2)),inference(spm,[status(thm)],[392,207,theory(equality)])).
% cnf(401,plain,(esk10_2(X1,X2)=esk8_1(X2)|~root_occ(X1,X2)),inference(spm,[status(thm)],[392,187,theory(equality)])).
% cnf(424,negated_conjecture,(atomic(tptp0)|~atocc(esk16_0,X1)),inference(spm,[status(thm)],[221,386,theory(equality)])).
% cnf(427,negated_conjecture,(~atocc(esk16_0,X1)),inference(sr,[status(thm)],[424,57,theory(equality)])).
% cnf(436,negated_conjecture,(leaf(X1,tptp0)|~leaf_occ(X1,esk16_0)),inference(spm,[status(thm)],[205,387,theory(equality)])).
% cnf(439,negated_conjecture,(root(X1,tptp0)|~root_occ(X1,esk16_0)),inference(spm,[status(thm)],[185,388,theory(equality)])).
% cnf(442,negated_conjecture,(root(esk3_1(esk16_0),tptp0)|~occurrence_of(esk16_0,tptp0)),inference(spm,[status(thm)],[439,107,theory(equality)])).
% cnf(443,negated_conjecture,(root(esk3_1(esk16_0),tptp0)|$false),inference(rw,[status(thm)],[442,245,theory(equality)])).
% cnf(444,negated_conjecture,(root(esk3_1(esk16_0),tptp0)),inference(cn,[status(thm)],[443,theory(equality)])).
% cnf(491,plain,(esk13_2(esk1_3(X1,X2,X3),X4)=X1|~min_precedes(X2,X3,X1)|~atocc(esk1_3(X1,X2,X3),X4)),inference(spm,[status(thm)],[294,220,theory(equality)])).
% cnf(498,plain,(leaf(X1,esk8_1(X2))|~leaf_occ(X1,X2)),inference(spm,[status(thm)],[205,400,theory(equality)])).
% cnf(499,plain,(occurrence_of(X1,esk8_1(X1))|~leaf_occ(X2,X1)),inference(spm,[status(thm)],[207,400,theory(equality)])).
% cnf(513,plain,(root(X1,esk8_1(X2))|~root_occ(X1,X2)),inference(spm,[status(thm)],[185,401,theory(equality)])).
% cnf(516,plain,(occurrence_of(X1,esk8_1(X1))|~root_occ(X2,X1)),inference(spm,[status(thm)],[187,401,theory(equality)])).
% cnf(546,plain,(occurrence_of(X1,esk8_1(X1))|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[499,105,theory(equality)])).
% cnf(558,plain,(atomic(esk8_1(X1))|~arboreal(X1)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[93,546,theory(equality)])).
% cnf(568,plain,(arboreal(X1)|~atocc(X1,X2)),inference(csr,[status(thm)],[269,221])).
% cnf(569,plain,(arboreal(X1)|~root(X1,X2)),inference(spm,[status(thm)],[568,169,theory(equality)])).
% cnf(570,plain,(arboreal(esk11_2(X1,X2))|atomic(X1)|~occurrence_of(X2,X1)),inference(spm,[status(thm)],[569,199,theory(equality)])).
% cnf(636,plain,(occurrence_of(X1,esk8_1(X1))|~atocc(X1,X2)),inference(spm,[status(thm)],[220,399,theory(equality)])).
% cnf(640,plain,(occurrence_of(X1,esk8_1(X1))|~root(X1,X2)),inference(spm,[status(thm)],[636,169,theory(equality)])).
% cnf(643,negated_conjecture,(occurrence_of(esk3_1(esk16_0),esk8_1(esk3_1(esk16_0)))),inference(spm,[status(thm)],[640,444,theory(equality)])).
% cnf(653,negated_conjecture,(esk8_1(esk3_1(esk16_0))=tptp4|~occurrence_of(esk16_0,tptp0)),inference(spm,[status(thm)],[278,643,theory(equality)])).
% cnf(660,negated_conjecture,(esk8_1(esk3_1(esk16_0))=tptp4|$false),inference(rw,[status(thm)],[653,245,theory(equality)])).
% cnf(661,negated_conjecture,(esk8_1(esk3_1(esk16_0))=tptp4),inference(cn,[status(thm)],[660,theory(equality)])).
% cnf(672,negated_conjecture,(occurrence_of(esk3_1(esk16_0),tptp4)),inference(rw,[status(thm)],[643,661,theory(equality)])).
% cnf(763,plain,(atocc(X1,X2)|~atocc(X3,X2)|~occurrence_of(X1,esk13_2(X3,X2))),inference(csr,[status(thm)],[302,221])).
% cnf(765,plain,(atocc(X1,X2)|~atocc(X3,X2)|~occurrence_of(X1,esk8_1(X3))),inference(spm,[status(thm)],[763,399,theory(equality)])).
% cnf(767,plain,(atocc(esk1_3(esk13_2(X1,X2),X3,X4),X2)|~atocc(X1,X2)|~min_precedes(X3,X4,esk13_2(X1,X2))),inference(spm,[status(thm)],[763,71,theory(equality)])).
% cnf(819,plain,(~root(esk4_1(X1),tptp0)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[117,306,theory(equality)])).
% cnf(820,plain,(leaf(esk4_1(X1),tptp0)|min_precedes(esk4_1(X1),esk15_2(esk4_1(X1),tptp0),tptp0)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[232,306,theory(equality)])).
% cnf(835,negated_conjecture,(~root(X2,X1)|~occurrence_of(esk16_0,X1)|~atomic(X1)),inference(spm,[status(thm)],[427,309,theory(equality)])).
% cnf(840,plain,(occurrence_of(X1,esk8_1(X1))|~root(X3,X2)|~occurrence_of(X1,X2)|~atomic(X2)),inference(spm,[status(thm)],[636,309,theory(equality)])).
% cnf(845,negated_conjecture,(~occurrence_of(esk16_0,esk10_2(X1,X2))|~atomic(esk10_2(X1,X2))|~root_occ(X1,X2)),inference(spm,[status(thm)],[835,185,theory(equality)])).
% cnf(865,negated_conjecture,(~root_occ(X1,X2)|~occurrence_of(esk16_0,esk10_2(X1,X2))|~arboreal(X2)),inference(spm,[status(thm)],[845,262,theory(equality)])).
% cnf(869,negated_conjecture,(~arboreal(X1)|~root_occ(X2,X1)|~occurrence_of(esk16_0,esk8_1(X1))),inference(spm,[status(thm)],[865,401,theory(equality)])).
% cnf(873,plain,(X1=esk4_1(esk5_2(X1,X2))|atomic(X3)|atomic(X2)|~occurrence_of(esk5_2(X1,X2),tptp0)|~occurrence_of(esk5_2(X1,X2),X3)|~leaf(X1,X2)),inference(spm,[status(thm)],[315,113,theory(equality)])).
% cnf(878,negated_conjecture,(~arboreal(X1)|~root_occ(X2,X1)|~occurrence_of(esk16_0,esk13_2(X1,X3))|~atocc(X1,X3)),inference(spm,[status(thm)],[869,399,theory(equality)])).
% cnf(938,plain,(leaf(X1,X2)|~leaf_occ(X1,esk1_3(X2,X3,X4))|~min_precedes(X3,X4,X2)),inference(spm,[status(thm)],[498,398,theory(equality)])).
% cnf(939,plain,(root(X1,X2)|~root_occ(X1,esk1_3(X2,X3,X4))|~min_precedes(X3,X4,X2)),inference(spm,[status(thm)],[513,398,theory(equality)])).
% cnf(947,plain,(esk11_2(X1,X2)=esk3_1(X3)|atomic(X1)|~occurrence_of(X3,tptp0)|~occurrence_of(X3,X4)|~subactivity_occurrence(esk11_2(X1,X2),X3)|~occurrence_of(X3,X1)|~occurrence_of(X2,X1)),inference(spm,[status(thm)],[274,321,theory(equality)])).
% cnf(957,plain,(occurrence_of(X1,esk8_1(X1))|atomic(X2)|~subactivity_occurrence(esk11_2(X2,X3),X1)|~occurrence_of(X1,X2)|~occurrence_of(X3,X2)),inference(spm,[status(thm)],[516,321,theory(equality)])).
% cnf(1007,plain,(esk6_3(X1,X2,X3)=esk3_1(X4)|~occurrence_of(X4,tptp0)|~occurrence_of(X4,X5)|~subactivity_occurrence(esk6_3(X1,X2,X3),X4)|~min_precedes(X1,X2,X3)|~occurrence_of(X4,X3)),inference(spm,[status(thm)],[274,323,theory(equality)])).
% cnf(1038,plain,(legal(X1)|~min_precedes(X2,X1,X3)),inference(spm,[status(thm)],[240,324,theory(equality)])).
% cnf(1047,plain,(legal(esk7_3(X1,X2,X3))|next_subocc(X1,X2,X3)|~min_precedes(X1,X2,X3)),inference(spm,[status(thm)],[1038,137,theory(equality)])).
% cnf(1093,plain,(esk4_1(X2)=X1|~min_precedes(esk3_1(X2),X1,tptp0)|~occurrence_of(X2,tptp0)|~arboreal(X1)|~subactivity_occurrence(X1,X2)),inference(spm,[status(thm)],[307,331,theory(equality)])).
% cnf(1175,plain,(leaf(esk4_1(esk1_3(X1,X2,X3)),X1)|~min_precedes(X2,X3,X1)|~occurrence_of(esk1_3(X1,X2,X3),tptp0)),inference(spm,[status(thm)],[938,105,theory(equality)])).
% cnf(1176,plain,(root(esk11_2(X1,X2),X3)|atomic(X1)|~min_precedes(X4,X5,X3)|~subactivity_occurrence(esk11_2(X1,X2),esk1_3(X3,X4,X5))|~occurrence_of(esk1_3(X3,X4,X5),X1)|~occurrence_of(X2,X1)),inference(spm,[status(thm)],[939,321,theory(equality)])).
% cnf(1178,plain,(root(esk3_1(esk1_3(X1,X2,X3)),X1)|~min_precedes(X2,X3,X1)|~occurrence_of(esk1_3(X1,X2,X3),tptp0)),inference(spm,[status(thm)],[939,107,theory(equality)])).
% cnf(1196,negated_conjecture,(~atocc(X1,X3)|~root_occ(X2,X1)|~occurrence_of(esk16_0,esk13_2(X1,X3))),inference(csr,[status(thm)],[878,568])).
% cnf(1198,negated_conjecture,(~atocc(X1,X2)|~root_occ(X3,X1)|~occurrence_of(esk16_0,esk8_1(X1))),inference(spm,[status(thm)],[1196,399,theory(equality)])).
% cnf(1206,negated_conjecture,(~atocc(esk1_3(X1,X2,X3),X4)|~root_occ(X5,esk1_3(X1,X2,X3))|~occurrence_of(esk16_0,X1)|~min_precedes(X2,X3,X1)),inference(spm,[status(thm)],[1198,398,theory(equality)])).
% cnf(1247,negated_conjecture,(atocc(X1,X2)|~atocc(esk3_1(esk16_0),X2)|~occurrence_of(X1,tptp4)),inference(spm,[status(thm)],[765,661,theory(equality)])).
% cnf(1542,negated_conjecture,(atocc(X1,esk9_2(X2,esk3_1(esk16_0)))|~occurrence_of(X1,tptp4)|~root(esk3_1(esk16_0),X2)),inference(spm,[status(thm)],[1247,169,theory(equality)])).
% cnf(1834,plain,(X1=esk11_2(X2,X3)|min_precedes(X1,esk11_2(X2,X3),X4)|min_precedes(esk11_2(X2,X3),X1,X4)|atomic(X2)|~arboreal(X1)|~subactivity_occurrence(X1,X3)|~occurrence_of(X3,X4)|~occurrence_of(X3,X2)),inference(csr,[status(thm)],[383,570])).
% cnf(1842,plain,(X1=esk11_2(X2,esk1_3(X3,X4,X1))|min_precedes(esk11_2(X2,esk1_3(X3,X4,X1)),X1,X5)|min_precedes(X1,esk11_2(X2,esk1_3(X3,X4,X1)),X5)|atomic(X2)|~arboreal(X1)|~occurrence_of(esk1_3(X3,X4,X1),X5)|~occurrence_of(esk1_3(X3,X4,X1),X2)|~min_precedes(X4,X1,X3)),inference(spm,[status(thm)],[1834,69,theory(equality)])).
% cnf(1855,plain,(esk3_1(esk1_3(X1,X2,X3))=X3|min_precedes(X3,esk3_1(esk1_3(X1,X2,X3)),X4)|min_precedes(esk3_1(esk1_3(X1,X2,X3)),X3,X4)|~arboreal(X3)|~arboreal(esk3_1(esk1_3(X1,X2,X3)))|~min_precedes(X2,X3,X1)|~occurrence_of(esk1_3(X1,X2,X3),X4)|~occurrence_of(esk1_3(X1,X2,X3),tptp0)),inference(spm,[status(thm)],[384,273,theory(equality)])).
% cnf(1867,plain,(esk3_1(esk1_3(X1,X2,X3))=X2|min_precedes(X2,esk3_1(esk1_3(X1,X2,X3)),X4)|min_precedes(esk3_1(esk1_3(X1,X2,X3)),X2,X4)|~arboreal(X2)|~arboreal(esk3_1(esk1_3(X1,X2,X3)))|~min_precedes(X2,X3,X1)|~occurrence_of(esk1_3(X1,X2,X3),X4)|~occurrence_of(esk1_3(X1,X2,X3),tptp0)),inference(spm,[status(thm)],[385,273,theory(equality)])).
% cnf(1985,plain,(occurrence_of(X1,esk8_1(X1))|~occurrence_of(X1,esk10_2(X2,X3))|~atomic(esk10_2(X2,X3))|~root_occ(X2,X3)),inference(spm,[status(thm)],[840,185,theory(equality)])).
% cnf(2619,plain,(esk4_1(X1)=esk7_3(esk3_1(X1),X2,tptp0)|next_subocc(esk3_1(X1),X2,tptp0)|~arboreal(esk7_3(esk3_1(X1),X2,tptp0))|~subactivity_occurrence(esk7_3(esk3_1(X1),X2,tptp0),X1)|~occurrence_of(X1,tptp0)|~min_precedes(esk3_1(X1),X2,tptp0)),inference(spm,[status(thm)],[1093,137,theory(equality)])).
% cnf(3204,plain,(leaf(esk4_1(X1),tptp0)|~leaf_occ(esk4_1(X1),X2)|~occurrence_of(X2,tptp0)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[75,820,theory(equality)])).
% cnf(3278,plain,(esk4_1(esk5_2(X1,X2))=X1|atomic(X2)|~leaf(X1,X2)|~occurrence_of(esk5_2(X1,X2),tptp0)),inference(spm,[status(thm)],[873,114,theory(equality)])).
% cnf(3291,plain,(esk8_1(X1)=tptp3|atomic(X2)|~occurrence_of(esk5_2(X1,X2),tptp0)|~leaf(X1,X2)),inference(spm,[status(thm)],[395,3278,theory(equality)])).
% cnf(3293,plain,(atomic(X2)|~root(X1,tptp0)|~occurrence_of(esk5_2(X1,X2),tptp0)|~leaf(X1,X2)),inference(spm,[status(thm)],[819,3278,theory(equality)])).
% cnf(3315,plain,(atomic(tptp0)|~root(X1,tptp0)|~leaf(X1,tptp0)),inference(spm,[status(thm)],[3293,114,theory(equality)])).
% cnf(3316,plain,(~root(X1,tptp0)|~leaf(X1,tptp0)),inference(sr,[status(thm)],[3315,57,theory(equality)])).
% cnf(3320,negated_conjecture,(~root(X1,tptp0)|~leaf_occ(X1,esk16_0)),inference(spm,[status(thm)],[3316,436,theory(equality)])).
% cnf(3323,negated_conjecture,(~leaf_occ(esk3_1(esk16_0),esk16_0)),inference(spm,[status(thm)],[3320,444,theory(equality)])).
% cnf(3577,plain,(esk11_2(X1,X2)=esk3_1(X2)|atomic(X1)|~occurrence_of(X2,tptp0)|~occurrence_of(X2,X3)|~occurrence_of(X2,X1)),inference(spm,[status(thm)],[947,198,theory(equality)])).
% cnf(3606,plain,(esk8_1(X1)=tptp3|atomic(tptp0)|~leaf(X1,tptp0)),inference(spm,[status(thm)],[3291,114,theory(equality)])).
% cnf(3607,plain,(esk8_1(X1)=tptp3|~leaf(X1,tptp0)),inference(sr,[status(thm)],[3606,57,theory(equality)])).
% cnf(3625,plain,(tptp3=tptp1|leaf_occ(X1,X2)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)|~leaf(esk2_2(X1,X2),tptp0)),inference(spm,[status(thm)],[397,3607,theory(equality)])).
% cnf(3665,plain,(leaf_occ(X1,X2)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)|~leaf(esk2_2(X1,X2),tptp0)),inference(sr,[status(thm)],[3625,212,theory(equality)])).
% cnf(3772,plain,(occurrence_of(X1,esk8_1(X1))|atomic(X2)|~occurrence_of(X1,X2)),inference(spm,[status(thm)],[957,198,theory(equality)])).
% cnf(3794,plain,(occurrence_of(esk1_3(X1,X2,X3),esk8_1(esk1_3(X1,X2,X3)))|atomic(X1)|~min_precedes(X2,X3,X1)),inference(spm,[status(thm)],[3772,71,theory(equality)])).
% cnf(4038,plain,(esk6_3(X1,X2,X3)=esk3_1(X4)|~min_precedes(X1,X2,X3)|~occurrence_of(X4,tptp0)|~occurrence_of(X4,X5)|~occurrence_of(X4,X3)|~subactivity_occurrence(X2,X4)),inference(spm,[status(thm)],[1007,329,theory(equality)])).
% cnf(4162,negated_conjecture,(esk11_2(X1,esk16_0)=esk3_1(esk16_0)|atomic(X1)|~occurrence_of(esk16_0,tptp0)|~occurrence_of(esk16_0,X1)),inference(spm,[status(thm)],[3577,245,theory(equality)])).
% cnf(4178,plain,(esk11_2(X1,X2)=esk3_1(X2)|atomic(X1)|~occurrence_of(X2,tptp0)|~occurrence_of(X2,X1)),inference(spm,[status(thm)],[3577,546,theory(equality)])).
% cnf(4181,negated_conjecture,(esk11_2(X1,esk16_0)=esk3_1(esk16_0)|atomic(X1)|$false|~occurrence_of(esk16_0,X1)),inference(rw,[status(thm)],[4162,245,theory(equality)])).
% cnf(4182,negated_conjecture,(esk11_2(X1,esk16_0)=esk3_1(esk16_0)|atomic(X1)|~occurrence_of(esk16_0,X1)),inference(cn,[status(thm)],[4181,theory(equality)])).
% cnf(4186,negated_conjecture,(subactivity_occurrence(esk3_1(esk16_0),esk16_0)|atomic(X1)|~occurrence_of(esk16_0,X1)),inference(spm,[status(thm)],[198,4182,theory(equality)])).
% cnf(4190,negated_conjecture,(root_occ(esk3_1(esk16_0),X2)|atomic(X1)|~subactivity_occurrence(esk3_1(esk16_0),X2)|~occurrence_of(X2,X1)|~occurrence_of(esk16_0,X1)),inference(spm,[status(thm)],[321,4182,theory(equality)])).
% cnf(4278,negated_conjecture,(subactivity_occurrence(esk3_1(esk16_0),esk16_0)|atomic(esk8_1(esk16_0))|~activity_occurrence(esk16_0)),inference(spm,[status(thm)],[4186,155,theory(equality)])).
% cnf(4283,negated_conjecture,(subactivity_occurrence(esk3_1(esk16_0),esk16_0)|atomic(tptp0)|~activity_occurrence(esk16_0)),inference(rw,[status(thm)],[4278,391,theory(equality)])).
% cnf(4284,negated_conjecture,(subactivity_occurrence(esk3_1(esk16_0),esk16_0)|atomic(tptp0)|$false),inference(rw,[status(thm)],[4283,249,theory(equality)])).
% cnf(4285,negated_conjecture,(subactivity_occurrence(esk3_1(esk16_0),esk16_0)|atomic(tptp0)),inference(cn,[status(thm)],[4284,theory(equality)])).
% cnf(4286,negated_conjecture,(subactivity_occurrence(esk3_1(esk16_0),esk16_0)),inference(sr,[status(thm)],[4285,57,theory(equality)])).
% cnf(4475,plain,(arboreal(esk7_3(X1,X2,X3))|next_subocc(X1,X2,X3)|~min_precedes(X1,X2,X3)),inference(spm,[status(thm)],[179,1047,theory(equality)])).
% cnf(6123,plain,(root(esk11_2(X1,X2),X3)|atomic(X1)|~min_precedes(X4,esk11_2(X1,X2),X3)|~occurrence_of(esk1_3(X3,X4,esk11_2(X1,X2)),X1)|~occurrence_of(X2,X1)),inference(spm,[status(thm)],[1176,69,theory(equality)])).
% cnf(6125,plain,(root(esk11_2(X1,esk1_3(X2,X3,X4)),X2)|atomic(X1)|~min_precedes(X3,X4,X2)|~occurrence_of(esk1_3(X2,X3,X4),X1)),inference(spm,[status(thm)],[1176,198,theory(equality)])).
% cnf(6255,negated_conjecture,(~min_precedes(X3,X4,esk13_2(X1,X2))|~root_occ(X5,esk1_3(esk13_2(X1,X2),X3,X4))|~occurrence_of(esk16_0,esk13_2(X1,X2))|~atocc(X1,X2)),inference(spm,[status(thm)],[1206,767,theory(equality)])).
% cnf(7160,plain,(leaf(esk4_1(X1),tptp0)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[3204,105,theory(equality)])).
% cnf(7711,negated_conjecture,(arboreal(X1)|~root(esk3_1(esk16_0),X2)|~occurrence_of(X1,tptp4)),inference(spm,[status(thm)],[568,1542,theory(equality)])).
% cnf(7732,negated_conjecture,(arboreal(X1)|~occurrence_of(X1,tptp4)),inference(spm,[status(thm)],[7711,444,theory(equality)])).
% cnf(9537,plain,(esk11_2(X3,esk1_3(X4,X5,X1))=X1|min_precedes(X1,esk11_2(X3,esk1_3(X4,X5,X1)),X2)|atomic(X3)|~root(X1,X2)|~arboreal(X1)|~min_precedes(X5,X1,X4)|~occurrence_of(esk1_3(X4,X5,X1),X2)|~occurrence_of(esk1_3(X4,X5,X1),X3)),inference(spm,[status(thm)],[117,1842,theory(equality)])).
% cnf(9744,plain,(esk3_1(esk1_3(X1,X2,X3))=X3|min_precedes(X3,esk3_1(esk1_3(X1,X2,X3)),X4)|min_precedes(esk3_1(esk1_3(X1,X2,X3)),X3,X4)|~arboreal(X3)|~min_precedes(X2,X3,X1)|~occurrence_of(esk1_3(X1,X2,X3),tptp0)|~occurrence_of(esk1_3(X1,X2,X3),X4)),inference(csr,[status(thm)],[1855,282])).
% cnf(9768,plain,(esk4_1(esk1_3(X1,X2,X3))=X3|esk3_1(esk1_3(X1,X2,X3))=X3|min_precedes(X3,esk3_1(esk1_3(X1,X2,X3)),tptp0)|~arboreal(X3)|~subactivity_occurrence(X3,esk1_3(X1,X2,X3))|~occurrence_of(esk1_3(X1,X2,X3),tptp0)|~min_precedes(X2,X3,X1)),inference(spm,[status(thm)],[1093,9744,theory(equality)])).
% cnf(9942,negated_conjecture,(~atocc(X1,X2)|~min_precedes(X3,X4,esk13_2(X1,X2))|~occurrence_of(esk16_0,esk13_2(X1,X2))|~occurrence_of(esk1_3(esk13_2(X1,X2),X3,X4),tptp0)),inference(spm,[status(thm)],[6255,107,theory(equality)])).
% cnf(9946,plain,(esk3_1(esk1_3(X1,X2,X3))=X2|min_precedes(X2,esk3_1(esk1_3(X1,X2,X3)),X4)|min_precedes(esk3_1(esk1_3(X1,X2,X3)),X2,X4)|~arboreal(X2)|~min_precedes(X2,X3,X1)|~occurrence_of(esk1_3(X1,X2,X3),tptp0)|~occurrence_of(esk1_3(X1,X2,X3),X4)),inference(csr,[status(thm)],[1867,282])).
% cnf(9956,plain,(esk3_1(esk1_3(X3,X1,X4))=X1|min_precedes(X1,esk3_1(esk1_3(X3,X1,X4)),X2)|~root(X1,X2)|~arboreal(X1)|~min_precedes(X1,X4,X3)|~occurrence_of(esk1_3(X3,X1,X4),tptp0)|~occurrence_of(esk1_3(X3,X1,X4),X2)),inference(spm,[status(thm)],[117,9946,theory(equality)])).
% cnf(9976,negated_conjecture,(~atocc(esk1_3(X1,X2,X3),X4)|~min_precedes(X5,X6,X1)|~occurrence_of(esk1_3(X1,X5,X6),tptp0)|~occurrence_of(esk16_0,X1)|~min_precedes(X2,X3,X1)),inference(spm,[status(thm)],[9942,491,theory(equality)])).
% cnf(10021,negated_conjecture,(~atocc(esk1_3(tptp0,X1,X2),X3)|~min_precedes(X4,X5,tptp0)|~min_precedes(X1,X2,tptp0)|~occurrence_of(esk16_0,tptp0)),inference(spm,[status(thm)],[9976,71,theory(equality)])).
% cnf(10022,negated_conjecture,(~atocc(esk1_3(tptp0,X1,X2),X3)|~min_precedes(X4,X5,tptp0)|~min_precedes(X1,X2,tptp0)|$false),inference(rw,[status(thm)],[10021,245,theory(equality)])).
% cnf(10023,negated_conjecture,(~atocc(esk1_3(tptp0,X1,X2),X3)|~min_precedes(X4,X5,tptp0)|~min_precedes(X1,X2,tptp0)),inference(cn,[status(thm)],[10022,theory(equality)])).
% fof(10025, plain,(~(epred1_0)<=>![X3]:![X2]:![X1]:(~(atocc(esk1_3(tptp0,X1,X2),X3))|~(min_precedes(X1,X2,tptp0)))),introduced(definition),['split']).
% cnf(10026,plain,(epred1_0|~min_precedes(X1,X2,tptp0)|~atocc(esk1_3(tptp0,X1,X2),X3)),inference(split_equiv,[status(thm)],[10025])).
% fof(10027, plain,(~(epred2_0)<=>![X5]:![X4]:~(min_precedes(X4,X5,tptp0))),introduced(definition),['split']).
% cnf(10028,plain,(epred2_0|~min_precedes(X4,X5,tptp0)),inference(split_equiv,[status(thm)],[10027])).
% cnf(10029,negated_conjecture,(~epred2_0|~epred1_0),inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[10023,10025,theory(equality)]),10027,theory(equality)]),['split']).
% cnf(10049,negated_conjecture,(epred2_0|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[10028,306,theory(equality)])).
% cnf(10058,negated_conjecture,(epred2_0),inference(spm,[status(thm)],[10049,245,theory(equality)])).
% cnf(10064,negated_conjecture,($false|~epred1_0),inference(rw,[status(thm)],[10029,10058,theory(equality)])).
% cnf(10065,negated_conjecture,(~epred1_0),inference(cn,[status(thm)],[10064,theory(equality)])).
% cnf(10066,negated_conjecture,(~min_precedes(X1,X2,tptp0)|~atocc(esk1_3(tptp0,X1,X2),X3)),inference(sr,[status(thm)],[10026,10065,theory(equality)])).
% cnf(10069,negated_conjecture,(~min_precedes(X1,X2,tptp0)|~root(X4,X3)|~occurrence_of(esk1_3(tptp0,X1,X2),X3)|~atomic(X3)),inference(spm,[status(thm)],[10066,309,theory(equality)])).
% cnf(10504,plain,(occurrence_of(X1,esk8_1(X1))|~root_occ(X2,X3)|~occurrence_of(X1,esk10_2(X2,X3))),inference(csr,[status(thm)],[1985,3772])).
% cnf(10513,plain,(occurrence_of(X1,esk8_1(X1))|~root_occ(X2,X3)|~occurrence_of(X1,esk8_1(X3))),inference(spm,[status(thm)],[10504,401,theory(equality)])).
% cnf(10537,plain,(occurrence_of(esk1_3(esk8_1(X1),X2,X3),esk8_1(esk1_3(esk8_1(X1),X2,X3)))|~root_occ(X4,X1)|~min_precedes(X2,X3,esk8_1(X1))),inference(spm,[status(thm)],[10513,71,theory(equality)])).
% cnf(14008,plain,(esk7_3(esk3_1(X1),X2,tptp0)=esk4_1(X1)|next_subocc(esk3_1(X1),X2,tptp0)|~subactivity_occurrence(esk7_3(esk3_1(X1),X2,tptp0),X1)|~min_precedes(esk3_1(X1),X2,tptp0)|~occurrence_of(X1,tptp0)),inference(csr,[status(thm)],[2619,4475])).
% cnf(14009,plain,(esk7_3(esk3_1(X1),X2,tptp0)=esk4_1(X1)|next_subocc(esk3_1(X1),X2,tptp0)|~min_precedes(esk3_1(X1),X2,tptp0)|~occurrence_of(X1,tptp0)|~subactivity_occurrence(X2,X1)),inference(spm,[status(thm)],[14008,372,theory(equality)])).
% cnf(23793,negated_conjecture,(atomic(tptp0)|~root(X1,esk8_1(esk1_3(tptp0,X2,X3)))|~min_precedes(X2,X3,tptp0)|~atomic(esk8_1(esk1_3(tptp0,X2,X3)))),inference(spm,[status(thm)],[10069,3794,theory(equality)])).
% cnf(23809,negated_conjecture,(~root(X1,esk8_1(esk1_3(tptp0,X2,X3)))|~min_precedes(X2,X3,tptp0)|~atomic(esk8_1(esk1_3(tptp0,X2,X3)))),inference(sr,[status(thm)],[23793,57,theory(equality)])).
% cnf(23900,negated_conjecture,(~min_precedes(X2,X3,tptp0)|~atomic(esk8_1(esk1_3(tptp0,X2,X3)))|~root_occ(X1,esk1_3(tptp0,X2,X3))),inference(spm,[status(thm)],[23809,513,theory(equality)])).
% cnf(24578,negated_conjecture,(~min_precedes(X1,X2,tptp0)|~root_occ(X3,esk1_3(tptp0,X1,X2))|~arboreal(esk1_3(tptp0,X1,X2))|~occurrence_of(esk1_3(tptp0,X1,X2),tptp0)),inference(spm,[status(thm)],[23900,558,theory(equality)])).
% cnf(24611,negated_conjecture,(~arboreal(esk1_3(tptp0,X1,X2))|~min_precedes(X1,X2,tptp0)|~root_occ(X3,esk1_3(tptp0,X1,X2))),inference(csr,[status(thm)],[24578,71])).
% cnf(24618,negated_conjecture,(~arboreal(esk1_3(tptp0,X1,X2))|~min_precedes(X1,X2,tptp0)|~occurrence_of(esk1_3(tptp0,X1,X2),tptp0)),inference(spm,[status(thm)],[24611,107,theory(equality)])).
% cnf(24621,negated_conjecture,(~arboreal(esk1_3(tptp0,X1,X2))|~min_precedes(X1,X2,tptp0)),inference(csr,[status(thm)],[24618,71])).
% cnf(24856,plain,(esk6_3(X1,esk4_1(X2),X3)=esk3_1(X2)|~min_precedes(X1,esk4_1(X2),X3)|~occurrence_of(X2,tptp0)|~occurrence_of(X2,X4)|~occurrence_of(X2,X3)),inference(spm,[status(thm)],[4038,275,theory(equality)])).
% cnf(24999,negated_conjecture,(root_occ(esk3_1(esk16_0),esk16_0)|atomic(tptp0)|~subactivity_occurrence(esk3_1(esk16_0),esk16_0)|~occurrence_of(esk16_0,tptp0)),inference(spm,[status(thm)],[4190,245,theory(equality)])).
% cnf(25023,negated_conjecture,(root_occ(esk3_1(esk16_0),esk16_0)|atomic(tptp0)|$false|~occurrence_of(esk16_0,tptp0)),inference(rw,[status(thm)],[24999,4286,theory(equality)])).
% cnf(25024,negated_conjecture,(root_occ(esk3_1(esk16_0),esk16_0)|atomic(tptp0)|$false|$false),inference(rw,[status(thm)],[25023,245,theory(equality)])).
% cnf(25025,negated_conjecture,(root_occ(esk3_1(esk16_0),esk16_0)|atomic(tptp0)),inference(cn,[status(thm)],[25024,theory(equality)])).
% cnf(25026,negated_conjecture,(root_occ(esk3_1(esk16_0),esk16_0)),inference(sr,[status(thm)],[25025,57,theory(equality)])).
% cnf(35423,plain,(atomic(X1)|~min_precedes(X4,esk11_2(X1,X2),X3)|~occurrence_of(esk1_3(X3,X4,esk11_2(X1,X2)),X1)|~occurrence_of(X2,X1)),inference(csr,[status(thm)],[6123,117])).
% cnf(35428,plain,(atomic(X1)|~min_precedes(X2,esk11_2(X1,X3),X1)|~occurrence_of(X3,X1)),inference(spm,[status(thm)],[35423,71,theory(equality)])).
% cnf(35430,plain,(atomic(X1)|~min_precedes(X2,esk3_1(X3),X1)|~occurrence_of(X3,X1)|~occurrence_of(X3,tptp0)),inference(spm,[status(thm)],[35428,4178,theory(equality)])).
% cnf(63390,plain,(esk6_3(X1,esk4_1(X2),X3)=esk3_1(X2)|~min_precedes(X1,esk4_1(X2),X3)|~occurrence_of(X2,tptp0)|~occurrence_of(X2,X3)),inference(spm,[status(thm)],[24856,546,theory(equality)])).
% cnf(64334,plain,(root(esk3_1(X2),X3)|~min_precedes(X1,esk4_1(X2),X3)|~occurrence_of(X2,tptp0)|~occurrence_of(X2,X3)),inference(spm,[status(thm)],[123,63390,theory(equality)])).
% cnf(64758,plain,(root(esk3_1(X1),tptp0)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[64334,306,theory(equality)])).
% cnf(64787,plain,(root_occ(esk3_1(X1),X2)|~subactivity_occurrence(esk3_1(X1),X2)|~occurrence_of(X2,tptp0)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[188,64758,theory(equality)])).
% cnf(68918,plain,(esk11_2(X3,esk1_3(X4,X5,X1))=X1|min_precedes(X1,esk11_2(X3,esk1_3(X4,X5,X1)),X2)|atomic(X3)|~root(X1,X2)|~min_precedes(X5,X1,X4)|~occurrence_of(esk1_3(X4,X5,X1),X2)|~occurrence_of(esk1_3(X4,X5,X1),X3)),inference(csr,[status(thm)],[9537,569])).
% cnf(68997,plain,(atomic(X1)|esk11_2(X1,esk1_3(X3,X4,X2))=X2|~occurrence_of(esk1_3(X3,X4,X2),X1)|~root(X2,X1)|~min_precedes(X4,X2,X3)),inference(spm,[status(thm)],[35428,68918,theory(equality)])).
% cnf(75732,plain,(esk4_1(esk1_3(X1,X2,X3))=X3|esk3_1(esk1_3(X1,X2,X3))=X3|min_precedes(X3,esk3_1(esk1_3(X1,X2,X3)),tptp0)|~arboreal(X3)|~min_precedes(X2,X3,X1)|~occurrence_of(esk1_3(X1,X2,X3),tptp0)),inference(csr,[status(thm)],[9768,69])).
% cnf(75793,plain,(atomic(tptp0)|esk3_1(esk1_3(X2,X3,X1))=X1|esk4_1(esk1_3(X2,X3,X1))=X1|~occurrence_of(esk1_3(X2,X3,X1),tptp0)|~arboreal(X1)|~min_precedes(X3,X1,X2)),inference(spm,[status(thm)],[35430,75732,theory(equality)])).
% cnf(75809,plain,(esk3_1(esk1_3(X2,X3,X1))=X1|esk4_1(esk1_3(X2,X3,X1))=X1|~occurrence_of(esk1_3(X2,X3,X1),tptp0)|~arboreal(X1)|~min_precedes(X3,X1,X2)),inference(sr,[status(thm)],[75793,57,theory(equality)])).
% cnf(82470,plain,(esk3_1(esk1_3(X3,X1,X4))=X1|min_precedes(X1,esk3_1(esk1_3(X3,X1,X4)),X2)|~root(X1,X2)|~min_precedes(X1,X4,X3)|~occurrence_of(esk1_3(X3,X1,X4),tptp0)|~occurrence_of(esk1_3(X3,X1,X4),X2)),inference(csr,[status(thm)],[9956,569])).
% cnf(85821,negated_conjecture,(occurrence_of(esk1_3(esk8_1(esk16_0),X1,X2),esk8_1(esk1_3(esk8_1(esk16_0),X1,X2)))|~min_precedes(X1,X2,esk8_1(esk16_0))),inference(spm,[status(thm)],[10537,25026,theory(equality)])).
% cnf(85847,negated_conjecture,(occurrence_of(esk1_3(tptp0,X1,X2),esk8_1(esk1_3(tptp0,X1,X2)))|~min_precedes(X1,X2,esk8_1(esk16_0))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[85821,391,theory(equality)]),391,theory(equality)])).
% cnf(85848,negated_conjecture,(occurrence_of(esk1_3(tptp0,X1,X2),esk8_1(esk1_3(tptp0,X1,X2)))|~min_precedes(X1,X2,tptp0)),inference(rw,[status(thm)],[85847,391,theory(equality)])).
% cnf(85905,negated_conjecture,(arboreal(esk1_3(tptp0,X1,X2))|~atomic(esk8_1(esk1_3(tptp0,X1,X2)))|~min_precedes(X1,X2,tptp0)),inference(spm,[status(thm)],[92,85848,theory(equality)])).
% cnf(86031,negated_conjecture,(~min_precedes(X1,X2,tptp0)|~atomic(esk8_1(esk1_3(tptp0,X1,X2)))),inference(csr,[status(thm)],[85905,24621])).
% cnf(87852,plain,(root(X4,X2)|atomic(X1)|~min_precedes(X3,X4,X2)|~occurrence_of(esk1_3(X2,X3,X4),X1)|~root(X4,X1)),inference(spm,[status(thm)],[6125,68997,theory(equality)])).
% cnf(87943,plain,(atomic(X1)|~root(X4,X1)|~min_precedes(X3,X4,X2)|~occurrence_of(esk1_3(X2,X3,X4),X1)),inference(csr,[status(thm)],[87852,117])).
% cnf(87955,negated_conjecture,(atomic(esk8_1(esk1_3(tptp0,X1,X2)))|~root(X2,esk8_1(esk1_3(tptp0,X1,X2)))|~min_precedes(X1,X2,tptp0)),inference(spm,[status(thm)],[87943,85848,theory(equality)])).
% cnf(88011,negated_conjecture,(~root(X2,esk8_1(esk1_3(tptp0,X1,X2)))|~min_precedes(X1,X2,tptp0)),inference(csr,[status(thm)],[87955,86031])).
% cnf(88021,negated_conjecture,(~min_precedes(X2,X1,tptp0)|~root_occ(X1,esk1_3(tptp0,X2,X1))),inference(spm,[status(thm)],[88011,513,theory(equality)])).
% cnf(88038,negated_conjecture,(~min_precedes(X1,esk3_1(X2),tptp0)|~subactivity_occurrence(esk3_1(X2),esk1_3(tptp0,X1,esk3_1(X2)))|~occurrence_of(esk1_3(tptp0,X1,esk3_1(X2)),tptp0)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[88021,64787,theory(equality)])).
% cnf(92358,negated_conjecture,(~subactivity_occurrence(esk3_1(X2),esk1_3(tptp0,X1,esk3_1(X2)))|~min_precedes(X1,esk3_1(X2),tptp0)|~occurrence_of(X2,tptp0)),inference(csr,[status(thm)],[88038,71])).
% cnf(92359,negated_conjecture,(~min_precedes(X1,esk3_1(X2),tptp0)|~occurrence_of(X2,tptp0)),inference(csr,[status(thm)],[92358,69])).
% cnf(92393,negated_conjecture,(esk3_1(esk1_3(X2,X1,X3))=X1|~occurrence_of(esk1_3(X2,X1,X3),tptp0)|~root(X1,tptp0)|~min_precedes(X1,X3,X2)),inference(spm,[status(thm)],[92359,82470,theory(equality)])).
% cnf(124448,plain,(next_subocc(esk3_1(X1),X2,tptp0)|~leaf(esk4_1(X1),tptp0)|~min_precedes(esk3_1(X1),X2,tptp0)|~subactivity_occurrence(X2,X1)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[368,14009,theory(equality)])).
% cnf(141646,plain,(next_subocc(esk3_1(X1),X2,tptp0)|~subactivity_occurrence(X2,X1)|~min_precedes(esk3_1(X1),X2,tptp0)|~occurrence_of(X1,tptp0)),inference(csr,[status(thm)],[124448,7160])).
% cnf(141650,plain,(arboreal(X1)|~subactivity_occurrence(X1,X2)|~min_precedes(esk3_1(X2),X1,tptp0)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[192,141646,theory(equality)])).
% cnf(141654,negated_conjecture,(arboreal(X1)|~subactivity_occurrence(X1,esk1_3(X2,X3,X4))|~min_precedes(X3,X1,tptp0)|~occurrence_of(esk1_3(X2,X3,X4),tptp0)|~root(X3,tptp0)|~min_precedes(X3,X4,X2)),inference(spm,[status(thm)],[141650,92393,theory(equality)])).
% cnf(141817,negated_conjecture,(arboreal(X1)|~root(X2,tptp0)|~min_precedes(X2,X1,tptp0)|~min_precedes(X2,X1,X3)|~occurrence_of(esk1_3(X3,X2,X1),tptp0)),inference(spm,[status(thm)],[141654,69,theory(equality)])).
% cnf(141824,negated_conjecture,(arboreal(X1)|~root(X2,tptp0)|~min_precedes(X2,X1,tptp0)),inference(spm,[status(thm)],[141817,71,theory(equality)])).
% cnf(141882,negated_conjecture,(arboreal(X1)|~root(esk6_3(X2,X1,tptp0),tptp0)|~min_precedes(X2,X1,tptp0)),inference(spm,[status(thm)],[141824,122,theory(equality)])).
% cnf(141994,negated_conjecture,(arboreal(X1)|~min_precedes(X2,X1,tptp0)),inference(csr,[status(thm)],[141882,123])).
% cnf(256762,plain,(leaf(X3,X1)|esk3_1(esk1_3(X1,X2,X3))=X3|~min_precedes(X2,X3,X1)|~occurrence_of(esk1_3(X1,X2,X3),tptp0)|~arboreal(X3)),inference(spm,[status(thm)],[1175,75809,theory(equality)])).
% cnf(335967,plain,(root(X3,X1)|leaf(X3,X1)|~min_precedes(X2,X3,X1)|~occurrence_of(esk1_3(X1,X2,X3),tptp0)|~arboreal(X3)),inference(spm,[status(thm)],[1178,256762,theory(equality)])).
% cnf(336545,plain,(leaf(X3,X1)|~arboreal(X3)|~min_precedes(X2,X3,X1)|~occurrence_of(esk1_3(X1,X2,X3),tptp0)),inference(csr,[status(thm)],[335967,117])).
% cnf(336546,plain,(leaf(X1,tptp0)|~arboreal(X1)|~min_precedes(X2,X1,tptp0)),inference(spm,[status(thm)],[336545,71,theory(equality)])).
% cnf(336547,plain,(leaf(X1,tptp0)|~min_precedes(X2,X1,tptp0)),inference(csr,[status(thm)],[336546,141994])).
% cnf(336681,plain,(leaf(esk2_2(X1,X2),tptp0)|leaf_occ(X1,X2)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[336547,375,theory(equality)])).
% cnf(336720,plain,(leaf_occ(X1,X2)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(csr,[status(thm)],[336681,3665])).
% cnf(336749,negated_conjecture,(leaf_occ(X1,X2)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)|~occurrence_of(X1,tptp4)),inference(spm,[status(thm)],[336720,7732,theory(equality)])).
% cnf(336918,negated_conjecture,(~subactivity_occurrence(esk3_1(esk16_0),esk16_0)|~occurrence_of(esk16_0,tptp0)|~occurrence_of(esk3_1(esk16_0),tptp4)),inference(spm,[status(thm)],[3323,336749,theory(equality)])).
% cnf(337549,negated_conjecture,($false|~occurrence_of(esk16_0,tptp0)|~occurrence_of(esk3_1(esk16_0),tptp4)),inference(rw,[status(thm)],[336918,4286,theory(equality)])).
% cnf(337550,negated_conjecture,($false|$false|~occurrence_of(esk3_1(esk16_0),tptp4)),inference(rw,[status(thm)],[337549,245,theory(equality)])).
% cnf(337551,negated_conjecture,($false|$false|$false),inference(rw,[status(thm)],[337550,672,theory(equality)])).
% cnf(337552,negated_conjecture,($false),inference(cn,[status(thm)],[337551,theory(equality)])).
% cnf(337553,negated_conjecture,($false),337552,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 42826
% # ...of these trivial : 14
% # ...subsumed : 34087
% # ...remaining for further processing: 8725
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 1559
% # Backward-rewritten : 32
% # Generated clauses : 223553
% # ...of the previous two non-trivial : 211026
% # Contextual simplify-reflections : 46997
% # Paramodulations : 223407
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 7061
% # Positive orientable unit clauses: 40
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 37
% # Non-unit-clauses : 6984
% # Current number of unprocessed clauses: 103524
% # ...number of literals in the above : 820690
% # Clause-clause subsumption calls (NU) : 12101533
% # Rec. Clause-clause subsumption calls : 2428034
% # Unit Clause-clause subsumption calls : 41277
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 22
% # Indexed BW rewrite successes : 21
% # Backwards rewriting index: 2816 leaves, 2.91+/-8.994 terms/leaf
% # Paramod-from index: 538 leaves, 1.28+/-0.773 terms/leaf
% # Paramod-into index: 2091 leaves, 2.29+/-4.431 terms/leaf
% # -------------------------------------------------
% # User time : 27.392 s
% # System time : 0.458 s
% # Total time : 27.850 s
% # Maximum resident set size: 0 pages
% PrfWatch: 33.33 CPU 34.38 WC
% FINAL PrfWatch: 33.33 CPU 34.38 WC
% SZS output end Solution for /tmp/SystemOnTPTP32427/PRO006+4.tptp
%
%------------------------------------------------------------------------------