%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : PRO006+2 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art05.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:02:20 EST 2010
% Result : Theorem 209.75s
% Output : Solution 212.32s
% 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/SystemOnTPTP7063/PRO006+2.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% not found
% Adding ~C to TBU ... ~goals:
% ---- Iteration 1 (0 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_34:
% CSA axiom sos_34 found
% Looking for CSA axiom ... sos:
% CSA axiom sos found
% Looking for CSA axiom ... sos_33:
% CSA axiom sos_33 found
% ---- Iteration 2 (3 axioms selected)
% Looking for TBU SAT ... yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_22:
% CSA axiom sos_22 found
% Looking for CSA axiom ... sos_02:
% CSA axiom sos_02 found
% Looking for CSA axiom ... sos_13:
% CSA axiom sos_13 found
% ---- Iteration 3 (6 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_21:
% CSA axiom sos_21 found
% Looking for CSA axiom ... sos_24:
% CSA axiom sos_24 found
% Looking for CSA axiom ... sos_20:
% CSA axiom sos_20 found
% ---- Iteration 4 (9 axioms selected)
% Looking for TBU SAT ... yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_45:
% CSA axiom sos_45 found
% Looking for CSA axiom ... sos_01:
% CSA axiom sos_01 found
% Looking for CSA axiom ... sos_05:
% CSA axiom sos_05 found
% ---- Iteration 5 (12 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_09:
% CSA axiom sos_09 found
% Looking for CSA axiom ... sos_17:
% CSA axiom sos_17 found
% Looking for CSA axiom ... sos_18:
% CSA axiom sos_18 found
% ---- Iteration 6 (15 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_29:
% CSA axiom sos_29 found
% Looking for CSA axiom ... sos_31:
% CSA axiom sos_31 found
% Looking for CSA axiom ... sos_32:
% CSA axiom sos_32 found
% ---- Iteration 7 (18 axioms selected)
% Looking for TBU SAT ... yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_07:
% CSA axiom sos_07 found
% Looking for CSA axiom ... sos_19:
% CSA axiom sos_19 found
% Looking for CSA axiom ... sos_23:
% CSA axiom sos_23 found
% ---- Iteration 8 (21 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_25:
% sos_03:
% CSA axiom sos_03 found
% Looking for CSA axiom ... sos_04:
% CSA axiom sos_04 found
% Looking for CSA axiom ... sos_06:
% CSA axiom sos_06 found
% ---- Iteration 9 (24 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_25:
% sos_35:
% sos_36:
% sos_37:
% CSA axiom sos_37 found
% Looking for CSA axiom ... sos_38:
% sos_28:
% CSA axiom sos_28 found
% Looking for CSA axiom ... sos_27:
% CSA axiom sos_27 found
% ---- Iteration 10 (27 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_25:
% sos_35:
% sos_36:
% sos_38:
% sos_10:
% CSA axiom sos_10 found
% Looking for CSA axiom ... sos_11: CSA axiom sos_11 found
% Looking for CSA axiom ... sos_14:
% CSA axiom sos_14 found
% ---- Iteration 11 (30 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_25:
% sos_35:
% sos_36:
% sos_38:
% sos_26:
% CSA axiom sos_26 found
% Looking for CSA axiom ... sos_30:
% CSA axiom sos_30 found
% Looking for CSA axiom ... sos_39:
% CSA axiom sos_39 found
% ---- Iteration 12 (33 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ... not found
% Looking for CSA axiom ... sos_25:
% sos_35:
% sos_36:
% sos_38:
% sos_40:
% sos_41:
% CSA axiom sos_41 found
% Looking for CSA axiom ... sos_42:
% CSA axiom sos_42 found
% Looking for CSA axiom ... sos_43:
% CSA axiom sos_43 found
% ---- Iteration 13 (36 axioms selected)
% Looking for TBU SAT ...
% no
% Looking for TBU UNS ...
% yes - theorem proved
% ---- Selection completed
% Selected axioms are ... :sos_43:sos_42:sos_41:sos_39:sos_30:sos_26:sos_14:sos_11:sos_10:sos_27:sos_28:sos_37:sos_06:sos_04:sos_03:sos_23:sos_19:sos_07:sos_32:sos_31:sos_29:sos_18:sos_17:sos_09:sos_05:sos_01:sos_45:sos_20:sos_24:sos_21:sos_13:sos_02:sos_22:sos_33:sos:sos_34 (36)
% Unselected axioms are ... :sos_25:sos_35:sos_36:sos_38:sos_40:sos_44:sos_15:sos_16:sos_12:sos_08 (10)
% SZS status THM for /tmp/SystemOnTPTP7063/PRO006+2.tptp
% Looking for THM ...
% found
% SZS output start Solution for /tmp/SystemOnTPTP7063/PRO006+2.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=600 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 600s
% TreeLimitedRun: WC time limit is 1200s
% TreeLimitedRun: PID is 15444
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Preprocessing time : 0.017 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 1.93 CPU 2.02 WC
% # SZS output start CNFRefutation.
% fof(2, axiom,~(tptp1=tptp3),file('/tmp/SRASS.s.p', sos_42)).
% fof(5, axiom,![X1]:![X2]:((occurrence_of(X2,X1)&~(atomic(X1)))=>?[X3]:(root(X3,X1)&subactivity_occurrence(X3,X2))),file('/tmp/SRASS.s.p', sos_30)).
% fof(7, axiom,![X9]:![X10]:(leaf(X9,X10)<=>((root(X9,X10)|?[X11]:min_precedes(X11,X9,X10))&~(?[X12]:min_precedes(X9,X12,X10)))),file('/tmp/SRASS.s.p', sos_14)).
% fof(8, axiom,![X13]:![X14]:(leaf_occ(X13,X14)<=>?[X15]:((occurrence_of(X14,X15)&subactivity_occurrence(X13,X14))&leaf(X13,X15))),file('/tmp/SRASS.s.p', sos_11)).
% fof(9, axiom,![X16]:![X17]:(root_occ(X16,X17)<=>?[X18]:((occurrence_of(X17,X18)&subactivity_occurrence(X16,X17))&root(X16,X18))),file('/tmp/SRASS.s.p', sos_10)).
% fof(11, axiom,![X22]:![X23]:![X24]:![X25]:(((((occurrence_of(X23,X22)&arboreal(X24))&arboreal(X25))&subactivity_occurrence(X24,X23))&subactivity_occurrence(X25,X23))=>((min_precedes(X24,X25,X22)|min_precedes(X25,X24,X22))|X24=X25)),file('/tmp/SRASS.s.p', sos_28)).
% fof(14, axiom,![X29]:![X30]:![X31]:(next_subocc(X29,X30,X31)<=>(min_precedes(X29,X30,X31)&~(?[X32]:(min_precedes(X29,X32,X31)&min_precedes(X32,X30,X31))))),file('/tmp/SRASS.s.p', sos_04)).
% fof(15, axiom,![X33]:![X34]:![X35]:![X36]:((((occurrence_of(X35,X36)&~(atomic(X36)))&leaf_occ(X33,X35))&leaf_occ(X34,X35))=>X33=X34),file('/tmp/SRASS.s.p', sos_03)).
% fof(16, axiom,![X37]:![X38]:((leaf(X37,X38)&~(atomic(X38)))=>?[X39]:(occurrence_of(X39,X38)&leaf_occ(X37,X39))),file('/tmp/SRASS.s.p', sos_23)).
% fof(19, axiom,![X45]:(occurrence_of(X45,tptp0)=>?[X46]:?[X47]:((((occurrence_of(X46,tptp4)&root_occ(X46,X45))&occurrence_of(X47,tptp3))&leaf_occ(X47,X45))&next_subocc(X46,X47,tptp0))),file('/tmp/SRASS.s.p', sos_32)).
% fof(21, axiom,![X49]:![X50]:(occurrence_of(X50,X49)=>(activity(X49)&activity_occurrence(X50))),file('/tmp/SRASS.s.p', sos_29)).
% fof(22, axiom,![X51]:(activity_occurrence(X51)=>?[X52]:(activity(X52)&occurrence_of(X51,X52))),file('/tmp/SRASS.s.p', sos_18)).
% fof(25, axiom,![X56]:![X57]:![X58]:(next_subocc(X56,X57,X58)=>(arboreal(X56)&arboreal(X57))),file('/tmp/SRASS.s.p', sos_05)).
% fof(27, axiom,![X62]:![X63]:((((occurrence_of(X63,tptp0)&subactivity_occurrence(X62,X63))&arboreal(X62))&~(leaf_occ(X62,X63)))=>?[X64]:(occurrence_of(X64,tptp1)&next_subocc(X62,X64,tptp0))),file('/tmp/SRASS.s.p', sos_45)).
% fof(29, axiom,![X69]:![X70]:![X71]:(min_precedes(X70,X71,X69)=>?[X72]:((occurrence_of(X72,X69)&subactivity_occurrence(X70,X72))&subactivity_occurrence(X71,X72))),file('/tmp/SRASS.s.p', sos_24)).
% fof(30, axiom,![X73]:![X74]:![X75]:((occurrence_of(X73,X75)&leaf_occ(X74,X73))=>~(?[X76]:min_precedes(X74,X76,X75))),file('/tmp/SRASS.s.p', sos_21)).
% fof(31, axiom,![X77]:![X78]:(occurrence_of(X77,X78)=>(arboreal(X77)<=>atomic(X78))),file('/tmp/SRASS.s.p', sos_13)).
% fof(32, axiom,![X79]:![X80]:![X81]:![X82]:(((occurrence_of(X81,X82)&root_occ(X79,X81))&root_occ(X80,X81))=>X79=X80),file('/tmp/SRASS.s.p', sos_02)).
% fof(33, axiom,![X83]:![X84]:![X85]:((occurrence_of(X83,X84)&occurrence_of(X83,X85))=>X84=X85),file('/tmp/SRASS.s.p', sos_22)).
% fof(36, axiom,~(atomic(tptp0)),file('/tmp/SRASS.s.p', sos_34)).
% fof(37, conjecture,~(?[X90]:occurrence_of(X90,tptp0)),file('/tmp/SRASS.s.p', goals)).
% fof(38, negated_conjecture,~(~(?[X90]:occurrence_of(X90,tptp0))),inference(assume_negation,[status(cth)],[37])).
% fof(39, plain,![X1]:![X2]:((occurrence_of(X2,X1)&~(atomic(X1)))=>?[X3]:(root(X3,X1)&subactivity_occurrence(X3,X2))),inference(fof_simplification,[status(thm)],[5,theory(equality)])).
% fof(40, plain,![X33]:![X34]:![X35]:![X36]:((((occurrence_of(X35,X36)&~(atomic(X36)))&leaf_occ(X33,X35))&leaf_occ(X34,X35))=>X33=X34),inference(fof_simplification,[status(thm)],[15,theory(equality)])).
% fof(41, plain,![X37]:![X38]:((leaf(X37,X38)&~(atomic(X38)))=>?[X39]:(occurrence_of(X39,X38)&leaf_occ(X37,X39))),inference(fof_simplification,[status(thm)],[16,theory(equality)])).
% fof(44, plain,![X62]:![X63]:((((occurrence_of(X63,tptp0)&subactivity_occurrence(X62,X63))&arboreal(X62))&~(leaf_occ(X62,X63)))=>?[X64]:(occurrence_of(X64,tptp1)&next_subocc(X62,X64,tptp0))),inference(fof_simplification,[status(thm)],[27,theory(equality)])).
% fof(45, plain,~(atomic(tptp0)),inference(fof_simplification,[status(thm)],[36,theory(equality)])).
% cnf(47,plain,(tptp1!=tptp3),inference(split_conjunct,[status(thm)],[2])).
% fof(50, plain,![X1]:![X2]:((~(occurrence_of(X2,X1))|atomic(X1))|?[X3]:(root(X3,X1)&subactivity_occurrence(X3,X2))),inference(fof_nnf,[status(thm)],[39])).
% fof(51, plain,![X4]:![X5]:((~(occurrence_of(X5,X4))|atomic(X4))|?[X6]:(root(X6,X4)&subactivity_occurrence(X6,X5))),inference(variable_rename,[status(thm)],[50])).
% fof(52, plain,![X4]:![X5]:((~(occurrence_of(X5,X4))|atomic(X4))|(root(esk1_2(X4,X5),X4)&subactivity_occurrence(esk1_2(X4,X5),X5))),inference(skolemize,[status(esa)],[51])).
% fof(53, plain,![X4]:![X5]:((root(esk1_2(X4,X5),X4)|(~(occurrence_of(X5,X4))|atomic(X4)))&(subactivity_occurrence(esk1_2(X4,X5),X5)|(~(occurrence_of(X5,X4))|atomic(X4)))),inference(distribute,[status(thm)],[52])).
% cnf(54,plain,(atomic(X1)|subactivity_occurrence(esk1_2(X1,X2),X2)|~occurrence_of(X2,X1)),inference(split_conjunct,[status(thm)],[53])).
% cnf(55,plain,(atomic(X1)|root(esk1_2(X1,X2),X1)|~occurrence_of(X2,X1)),inference(split_conjunct,[status(thm)],[53])).
% fof(64, plain,![X9]:![X10]:((~(leaf(X9,X10))|((root(X9,X10)|?[X11]:min_precedes(X11,X9,X10))&![X12]:~(min_precedes(X9,X12,X10))))&(((~(root(X9,X10))&![X11]:~(min_precedes(X11,X9,X10)))|?[X12]:min_precedes(X9,X12,X10))|leaf(X9,X10))),inference(fof_nnf,[status(thm)],[7])).
% fof(65, plain,![X13]:![X14]:((~(leaf(X13,X14))|((root(X13,X14)|?[X15]:min_precedes(X15,X13,X14))&![X16]:~(min_precedes(X13,X16,X14))))&(((~(root(X13,X14))&![X17]:~(min_precedes(X17,X13,X14)))|?[X18]:min_precedes(X13,X18,X14))|leaf(X13,X14))),inference(variable_rename,[status(thm)],[64])).
% fof(66, plain,![X13]:![X14]:((~(leaf(X13,X14))|((root(X13,X14)|min_precedes(esk4_2(X13,X14),X13,X14))&![X16]:~(min_precedes(X13,X16,X14))))&(((~(root(X13,X14))&![X17]:~(min_precedes(X17,X13,X14)))|min_precedes(X13,esk5_2(X13,X14),X14))|leaf(X13,X14))),inference(skolemize,[status(esa)],[65])).
% fof(67, plain,![X13]:![X14]:![X16]:![X17]:((((~(min_precedes(X17,X13,X14))&~(root(X13,X14)))|min_precedes(X13,esk5_2(X13,X14),X14))|leaf(X13,X14))&((~(min_precedes(X13,X16,X14))&(root(X13,X14)|min_precedes(esk4_2(X13,X14),X13,X14)))|~(leaf(X13,X14)))),inference(shift_quantors,[status(thm)],[66])).
% fof(68, plain,![X13]:![X14]:![X16]:![X17]:((((~(min_precedes(X17,X13,X14))|min_precedes(X13,esk5_2(X13,X14),X14))|leaf(X13,X14))&((~(root(X13,X14))|min_precedes(X13,esk5_2(X13,X14),X14))|leaf(X13,X14)))&((~(min_precedes(X13,X16,X14))|~(leaf(X13,X14)))&((root(X13,X14)|min_precedes(esk4_2(X13,X14),X13,X14))|~(leaf(X13,X14))))),inference(distribute,[status(thm)],[67])).
% cnf(70,plain,(~leaf(X1,X2)|~min_precedes(X1,X3,X2)),inference(split_conjunct,[status(thm)],[68])).
% fof(73, plain,![X13]:![X14]:((~(leaf_occ(X13,X14))|?[X15]:((occurrence_of(X14,X15)&subactivity_occurrence(X13,X14))&leaf(X13,X15)))&(![X15]:((~(occurrence_of(X14,X15))|~(subactivity_occurrence(X13,X14)))|~(leaf(X13,X15)))|leaf_occ(X13,X14))),inference(fof_nnf,[status(thm)],[8])).
% fof(74, plain,![X16]:![X17]:((~(leaf_occ(X16,X17))|?[X18]:((occurrence_of(X17,X18)&subactivity_occurrence(X16,X17))&leaf(X16,X18)))&(![X19]:((~(occurrence_of(X17,X19))|~(subactivity_occurrence(X16,X17)))|~(leaf(X16,X19)))|leaf_occ(X16,X17))),inference(variable_rename,[status(thm)],[73])).
% fof(75, plain,![X16]:![X17]:((~(leaf_occ(X16,X17))|((occurrence_of(X17,esk6_2(X16,X17))&subactivity_occurrence(X16,X17))&leaf(X16,esk6_2(X16,X17))))&(![X19]:((~(occurrence_of(X17,X19))|~(subactivity_occurrence(X16,X17)))|~(leaf(X16,X19)))|leaf_occ(X16,X17))),inference(skolemize,[status(esa)],[74])).
% fof(76, plain,![X16]:![X17]:![X19]:((((~(occurrence_of(X17,X19))|~(subactivity_occurrence(X16,X17)))|~(leaf(X16,X19)))|leaf_occ(X16,X17))&(~(leaf_occ(X16,X17))|((occurrence_of(X17,esk6_2(X16,X17))&subactivity_occurrence(X16,X17))&leaf(X16,esk6_2(X16,X17))))),inference(shift_quantors,[status(thm)],[75])).
% fof(77, plain,![X16]:![X17]:![X19]:((((~(occurrence_of(X17,X19))|~(subactivity_occurrence(X16,X17)))|~(leaf(X16,X19)))|leaf_occ(X16,X17))&(((occurrence_of(X17,esk6_2(X16,X17))|~(leaf_occ(X16,X17)))&(subactivity_occurrence(X16,X17)|~(leaf_occ(X16,X17))))&(leaf(X16,esk6_2(X16,X17))|~(leaf_occ(X16,X17))))),inference(distribute,[status(thm)],[76])).
% cnf(78,plain,(leaf(X1,esk6_2(X1,X2))|~leaf_occ(X1,X2)),inference(split_conjunct,[status(thm)],[77])).
% cnf(79,plain,(subactivity_occurrence(X1,X2)|~leaf_occ(X1,X2)),inference(split_conjunct,[status(thm)],[77])).
% cnf(80,plain,(occurrence_of(X2,esk6_2(X1,X2))|~leaf_occ(X1,X2)),inference(split_conjunct,[status(thm)],[77])).
% fof(82, plain,![X16]:![X17]:((~(root_occ(X16,X17))|?[X18]:((occurrence_of(X17,X18)&subactivity_occurrence(X16,X17))&root(X16,X18)))&(![X18]:((~(occurrence_of(X17,X18))|~(subactivity_occurrence(X16,X17)))|~(root(X16,X18)))|root_occ(X16,X17))),inference(fof_nnf,[status(thm)],[9])).
% fof(83, plain,![X19]:![X20]:((~(root_occ(X19,X20))|?[X21]:((occurrence_of(X20,X21)&subactivity_occurrence(X19,X20))&root(X19,X21)))&(![X22]:((~(occurrence_of(X20,X22))|~(subactivity_occurrence(X19,X20)))|~(root(X19,X22)))|root_occ(X19,X20))),inference(variable_rename,[status(thm)],[82])).
% fof(84, plain,![X19]:![X20]:((~(root_occ(X19,X20))|((occurrence_of(X20,esk7_2(X19,X20))&subactivity_occurrence(X19,X20))&root(X19,esk7_2(X19,X20))))&(![X22]:((~(occurrence_of(X20,X22))|~(subactivity_occurrence(X19,X20)))|~(root(X19,X22)))|root_occ(X19,X20))),inference(skolemize,[status(esa)],[83])).
% fof(85, plain,![X19]:![X20]:![X22]:((((~(occurrence_of(X20,X22))|~(subactivity_occurrence(X19,X20)))|~(root(X19,X22)))|root_occ(X19,X20))&(~(root_occ(X19,X20))|((occurrence_of(X20,esk7_2(X19,X20))&subactivity_occurrence(X19,X20))&root(X19,esk7_2(X19,X20))))),inference(shift_quantors,[status(thm)],[84])).
% fof(86, plain,![X19]:![X20]:![X22]:((((~(occurrence_of(X20,X22))|~(subactivity_occurrence(X19,X20)))|~(root(X19,X22)))|root_occ(X19,X20))&(((occurrence_of(X20,esk7_2(X19,X20))|~(root_occ(X19,X20)))&(subactivity_occurrence(X19,X20)|~(root_occ(X19,X20))))&(root(X19,esk7_2(X19,X20))|~(root_occ(X19,X20))))),inference(distribute,[status(thm)],[85])).
% cnf(87,plain,(root(X1,esk7_2(X1,X2))|~root_occ(X1,X2)),inference(split_conjunct,[status(thm)],[86])).
% cnf(89,plain,(occurrence_of(X2,esk7_2(X1,X2))|~root_occ(X1,X2)),inference(split_conjunct,[status(thm)],[86])).
% cnf(90,plain,(root_occ(X1,X2)|~root(X1,X3)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,X3)),inference(split_conjunct,[status(thm)],[86])).
% fof(97, plain,![X22]:![X23]:![X24]:![X25]:(((((~(occurrence_of(X23,X22))|~(arboreal(X24)))|~(arboreal(X25)))|~(subactivity_occurrence(X24,X23)))|~(subactivity_occurrence(X25,X23)))|((min_precedes(X24,X25,X22)|min_precedes(X25,X24,X22))|X24=X25)),inference(fof_nnf,[status(thm)],[11])).
% fof(98, plain,![X26]:![X27]:![X28]:![X29]:(((((~(occurrence_of(X27,X26))|~(arboreal(X28)))|~(arboreal(X29)))|~(subactivity_occurrence(X28,X27)))|~(subactivity_occurrence(X29,X27)))|((min_precedes(X28,X29,X26)|min_precedes(X29,X28,X26))|X28=X29)),inference(variable_rename,[status(thm)],[97])).
% cnf(99,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)],[98])).
% fof(104, plain,![X29]:![X30]:![X31]:((~(next_subocc(X29,X30,X31))|(min_precedes(X29,X30,X31)&![X32]:(~(min_precedes(X29,X32,X31))|~(min_precedes(X32,X30,X31)))))&((~(min_precedes(X29,X30,X31))|?[X32]:(min_precedes(X29,X32,X31)&min_precedes(X32,X30,X31)))|next_subocc(X29,X30,X31))),inference(fof_nnf,[status(thm)],[14])).
% fof(105, plain,![X33]:![X34]:![X35]:((~(next_subocc(X33,X34,X35))|(min_precedes(X33,X34,X35)&![X36]:(~(min_precedes(X33,X36,X35))|~(min_precedes(X36,X34,X35)))))&((~(min_precedes(X33,X34,X35))|?[X37]:(min_precedes(X33,X37,X35)&min_precedes(X37,X34,X35)))|next_subocc(X33,X34,X35))),inference(variable_rename,[status(thm)],[104])).
% fof(106, plain,![X33]:![X34]:![X35]:((~(next_subocc(X33,X34,X35))|(min_precedes(X33,X34,X35)&![X36]:(~(min_precedes(X33,X36,X35))|~(min_precedes(X36,X34,X35)))))&((~(min_precedes(X33,X34,X35))|(min_precedes(X33,esk9_3(X33,X34,X35),X35)&min_precedes(esk9_3(X33,X34,X35),X34,X35)))|next_subocc(X33,X34,X35))),inference(skolemize,[status(esa)],[105])).
% fof(107, plain,![X33]:![X34]:![X35]:![X36]:((((~(min_precedes(X33,X36,X35))|~(min_precedes(X36,X34,X35)))&min_precedes(X33,X34,X35))|~(next_subocc(X33,X34,X35)))&((~(min_precedes(X33,X34,X35))|(min_precedes(X33,esk9_3(X33,X34,X35),X35)&min_precedes(esk9_3(X33,X34,X35),X34,X35)))|next_subocc(X33,X34,X35))),inference(shift_quantors,[status(thm)],[106])).
% fof(108, plain,![X33]:![X34]:![X35]:![X36]:((((~(min_precedes(X33,X36,X35))|~(min_precedes(X36,X34,X35)))|~(next_subocc(X33,X34,X35)))&(min_precedes(X33,X34,X35)|~(next_subocc(X33,X34,X35))))&(((min_precedes(X33,esk9_3(X33,X34,X35),X35)|~(min_precedes(X33,X34,X35)))|next_subocc(X33,X34,X35))&((min_precedes(esk9_3(X33,X34,X35),X34,X35)|~(min_precedes(X33,X34,X35)))|next_subocc(X33,X34,X35)))),inference(distribute,[status(thm)],[107])).
% cnf(111,plain,(min_precedes(X1,X2,X3)|~next_subocc(X1,X2,X3)),inference(split_conjunct,[status(thm)],[108])).
% cnf(112,plain,(~next_subocc(X1,X2,X3)|~min_precedes(X4,X2,X3)|~min_precedes(X1,X4,X3)),inference(split_conjunct,[status(thm)],[108])).
% fof(113, plain,![X33]:![X34]:![X35]:![X36]:((((~(occurrence_of(X35,X36))|atomic(X36))|~(leaf_occ(X33,X35)))|~(leaf_occ(X34,X35)))|X33=X34),inference(fof_nnf,[status(thm)],[40])).
% fof(114, plain,![X37]:![X38]:![X39]:![X40]:((((~(occurrence_of(X39,X40))|atomic(X40))|~(leaf_occ(X37,X39)))|~(leaf_occ(X38,X39)))|X37=X38),inference(variable_rename,[status(thm)],[113])).
% cnf(115,plain,(X1=X2|atomic(X4)|~leaf_occ(X2,X3)|~leaf_occ(X1,X3)|~occurrence_of(X3,X4)),inference(split_conjunct,[status(thm)],[114])).
% fof(116, plain,![X37]:![X38]:((~(leaf(X37,X38))|atomic(X38))|?[X39]:(occurrence_of(X39,X38)&leaf_occ(X37,X39))),inference(fof_nnf,[status(thm)],[41])).
% fof(117, plain,![X40]:![X41]:((~(leaf(X40,X41))|atomic(X41))|?[X42]:(occurrence_of(X42,X41)&leaf_occ(X40,X42))),inference(variable_rename,[status(thm)],[116])).
% fof(118, plain,![X40]:![X41]:((~(leaf(X40,X41))|atomic(X41))|(occurrence_of(esk10_2(X40,X41),X41)&leaf_occ(X40,esk10_2(X40,X41)))),inference(skolemize,[status(esa)],[117])).
% fof(119, plain,![X40]:![X41]:((occurrence_of(esk10_2(X40,X41),X41)|(~(leaf(X40,X41))|atomic(X41)))&(leaf_occ(X40,esk10_2(X40,X41))|(~(leaf(X40,X41))|atomic(X41)))),inference(distribute,[status(thm)],[118])).
% cnf(120,plain,(atomic(X1)|leaf_occ(X2,esk10_2(X2,X1))|~leaf(X2,X1)),inference(split_conjunct,[status(thm)],[119])).
% cnf(121,plain,(atomic(X1)|occurrence_of(esk10_2(X2,X1),X1)|~leaf(X2,X1)),inference(split_conjunct,[status(thm)],[119])).
% fof(130, plain,![X45]:(~(occurrence_of(X45,tptp0))|?[X46]:?[X47]:((((occurrence_of(X46,tptp4)&root_occ(X46,X45))&occurrence_of(X47,tptp3))&leaf_occ(X47,X45))&next_subocc(X46,X47,tptp0))),inference(fof_nnf,[status(thm)],[19])).
% fof(131, plain,![X48]:(~(occurrence_of(X48,tptp0))|?[X49]:?[X50]:((((occurrence_of(X49,tptp4)&root_occ(X49,X48))&occurrence_of(X50,tptp3))&leaf_occ(X50,X48))&next_subocc(X49,X50,tptp0))),inference(variable_rename,[status(thm)],[130])).
% fof(132, plain,![X48]:(~(occurrence_of(X48,tptp0))|((((occurrence_of(esk11_1(X48),tptp4)&root_occ(esk11_1(X48),X48))&occurrence_of(esk12_1(X48),tptp3))&leaf_occ(esk12_1(X48),X48))&next_subocc(esk11_1(X48),esk12_1(X48),tptp0))),inference(skolemize,[status(esa)],[131])).
% fof(133, plain,![X48]:(((((occurrence_of(esk11_1(X48),tptp4)|~(occurrence_of(X48,tptp0)))&(root_occ(esk11_1(X48),X48)|~(occurrence_of(X48,tptp0))))&(occurrence_of(esk12_1(X48),tptp3)|~(occurrence_of(X48,tptp0))))&(leaf_occ(esk12_1(X48),X48)|~(occurrence_of(X48,tptp0))))&(next_subocc(esk11_1(X48),esk12_1(X48),tptp0)|~(occurrence_of(X48,tptp0)))),inference(distribute,[status(thm)],[132])).
% cnf(134,plain,(next_subocc(esk11_1(X1),esk12_1(X1),tptp0)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[133])).
% cnf(135,plain,(leaf_occ(esk12_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[133])).
% cnf(136,plain,(occurrence_of(esk12_1(X1),tptp3)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[133])).
% cnf(137,plain,(root_occ(esk11_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[133])).
% cnf(138,plain,(occurrence_of(esk11_1(X1),tptp4)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[133])).
% fof(142, plain,![X49]:![X50]:(~(occurrence_of(X50,X49))|(activity(X49)&activity_occurrence(X50))),inference(fof_nnf,[status(thm)],[21])).
% fof(143, plain,![X51]:![X52]:(~(occurrence_of(X52,X51))|(activity(X51)&activity_occurrence(X52))),inference(variable_rename,[status(thm)],[142])).
% fof(144, plain,![X51]:![X52]:((activity(X51)|~(occurrence_of(X52,X51)))&(activity_occurrence(X52)|~(occurrence_of(X52,X51)))),inference(distribute,[status(thm)],[143])).
% cnf(145,plain,(activity_occurrence(X1)|~occurrence_of(X1,X2)),inference(split_conjunct,[status(thm)],[144])).
% fof(147, plain,![X51]:(~(activity_occurrence(X51))|?[X52]:(activity(X52)&occurrence_of(X51,X52))),inference(fof_nnf,[status(thm)],[22])).
% fof(148, plain,![X53]:(~(activity_occurrence(X53))|?[X54]:(activity(X54)&occurrence_of(X53,X54))),inference(variable_rename,[status(thm)],[147])).
% fof(149, plain,![X53]:(~(activity_occurrence(X53))|(activity(esk13_1(X53))&occurrence_of(X53,esk13_1(X53)))),inference(skolemize,[status(esa)],[148])).
% fof(150, plain,![X53]:((activity(esk13_1(X53))|~(activity_occurrence(X53)))&(occurrence_of(X53,esk13_1(X53))|~(activity_occurrence(X53)))),inference(distribute,[status(thm)],[149])).
% cnf(151,plain,(occurrence_of(X1,esk13_1(X1))|~activity_occurrence(X1)),inference(split_conjunct,[status(thm)],[150])).
% fof(159, plain,![X56]:![X57]:![X58]:(~(next_subocc(X56,X57,X58))|(arboreal(X56)&arboreal(X57))),inference(fof_nnf,[status(thm)],[25])).
% fof(160, plain,![X59]:![X60]:![X61]:(~(next_subocc(X59,X60,X61))|(arboreal(X59)&arboreal(X60))),inference(variable_rename,[status(thm)],[159])).
% fof(161, plain,![X59]:![X60]:![X61]:((arboreal(X59)|~(next_subocc(X59,X60,X61)))&(arboreal(X60)|~(next_subocc(X59,X60,X61)))),inference(distribute,[status(thm)],[160])).
% cnf(162,plain,(arboreal(X2)|~next_subocc(X1,X2,X3)),inference(split_conjunct,[status(thm)],[161])).
% cnf(163,plain,(arboreal(X1)|~next_subocc(X1,X2,X3)),inference(split_conjunct,[status(thm)],[161])).
% fof(167, plain,![X62]:![X63]:((((~(occurrence_of(X63,tptp0))|~(subactivity_occurrence(X62,X63)))|~(arboreal(X62)))|leaf_occ(X62,X63))|?[X64]:(occurrence_of(X64,tptp1)&next_subocc(X62,X64,tptp0))),inference(fof_nnf,[status(thm)],[44])).
% fof(168, plain,![X65]:![X66]:((((~(occurrence_of(X66,tptp0))|~(subactivity_occurrence(X65,X66)))|~(arboreal(X65)))|leaf_occ(X65,X66))|?[X67]:(occurrence_of(X67,tptp1)&next_subocc(X65,X67,tptp0))),inference(variable_rename,[status(thm)],[167])).
% fof(169, plain,![X65]:![X66]:((((~(occurrence_of(X66,tptp0))|~(subactivity_occurrence(X65,X66)))|~(arboreal(X65)))|leaf_occ(X65,X66))|(occurrence_of(esk14_2(X65,X66),tptp1)&next_subocc(X65,esk14_2(X65,X66),tptp0))),inference(skolemize,[status(esa)],[168])).
% fof(170, plain,![X65]:![X66]:((occurrence_of(esk14_2(X65,X66),tptp1)|(((~(occurrence_of(X66,tptp0))|~(subactivity_occurrence(X65,X66)))|~(arboreal(X65)))|leaf_occ(X65,X66)))&(next_subocc(X65,esk14_2(X65,X66),tptp0)|(((~(occurrence_of(X66,tptp0))|~(subactivity_occurrence(X65,X66)))|~(arboreal(X65)))|leaf_occ(X65,X66)))),inference(distribute,[status(thm)],[169])).
% cnf(171,plain,(leaf_occ(X1,X2)|next_subocc(X1,esk14_2(X1,X2),tptp0)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(split_conjunct,[status(thm)],[170])).
% cnf(172,plain,(leaf_occ(X1,X2)|occurrence_of(esk14_2(X1,X2),tptp1)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(split_conjunct,[status(thm)],[170])).
% fof(177, plain,![X69]:![X70]:![X71]:(~(min_precedes(X70,X71,X69))|?[X72]:((occurrence_of(X72,X69)&subactivity_occurrence(X70,X72))&subactivity_occurrence(X71,X72))),inference(fof_nnf,[status(thm)],[29])).
% fof(178, plain,![X73]:![X74]:![X75]:(~(min_precedes(X74,X75,X73))|?[X76]:((occurrence_of(X76,X73)&subactivity_occurrence(X74,X76))&subactivity_occurrence(X75,X76))),inference(variable_rename,[status(thm)],[177])).
% fof(179, plain,![X73]:![X74]:![X75]:(~(min_precedes(X74,X75,X73))|((occurrence_of(esk15_3(X73,X74,X75),X73)&subactivity_occurrence(X74,esk15_3(X73,X74,X75)))&subactivity_occurrence(X75,esk15_3(X73,X74,X75)))),inference(skolemize,[status(esa)],[178])).
% fof(180, plain,![X73]:![X74]:![X75]:(((occurrence_of(esk15_3(X73,X74,X75),X73)|~(min_precedes(X74,X75,X73)))&(subactivity_occurrence(X74,esk15_3(X73,X74,X75))|~(min_precedes(X74,X75,X73))))&(subactivity_occurrence(X75,esk15_3(X73,X74,X75))|~(min_precedes(X74,X75,X73)))),inference(distribute,[status(thm)],[179])).
% cnf(181,plain,(subactivity_occurrence(X2,esk15_3(X3,X1,X2))|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[180])).
% cnf(182,plain,(subactivity_occurrence(X1,esk15_3(X3,X1,X2))|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[180])).
% cnf(183,plain,(occurrence_of(esk15_3(X3,X1,X2),X3)|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[180])).
% fof(184, plain,![X73]:![X74]:![X75]:((~(occurrence_of(X73,X75))|~(leaf_occ(X74,X73)))|![X76]:~(min_precedes(X74,X76,X75))),inference(fof_nnf,[status(thm)],[30])).
% fof(185, plain,![X77]:![X78]:![X79]:((~(occurrence_of(X77,X79))|~(leaf_occ(X78,X77)))|![X80]:~(min_precedes(X78,X80,X79))),inference(variable_rename,[status(thm)],[184])).
% fof(186, plain,![X77]:![X78]:![X79]:![X80]:(~(min_precedes(X78,X80,X79))|(~(occurrence_of(X77,X79))|~(leaf_occ(X78,X77)))),inference(shift_quantors,[status(thm)],[185])).
% cnf(187,plain,(~leaf_occ(X1,X2)|~occurrence_of(X2,X3)|~min_precedes(X1,X4,X3)),inference(split_conjunct,[status(thm)],[186])).
% fof(188, plain,![X77]:![X78]:(~(occurrence_of(X77,X78))|((~(arboreal(X77))|atomic(X78))&(~(atomic(X78))|arboreal(X77)))),inference(fof_nnf,[status(thm)],[31])).
% fof(189, plain,![X79]:![X80]:(~(occurrence_of(X79,X80))|((~(arboreal(X79))|atomic(X80))&(~(atomic(X80))|arboreal(X79)))),inference(variable_rename,[status(thm)],[188])).
% fof(190, plain,![X79]:![X80]:(((~(arboreal(X79))|atomic(X80))|~(occurrence_of(X79,X80)))&((~(atomic(X80))|arboreal(X79))|~(occurrence_of(X79,X80)))),inference(distribute,[status(thm)],[189])).
% cnf(191,plain,(arboreal(X1)|~occurrence_of(X1,X2)|~atomic(X2)),inference(split_conjunct,[status(thm)],[190])).
% cnf(192,plain,(atomic(X2)|~occurrence_of(X1,X2)|~arboreal(X1)),inference(split_conjunct,[status(thm)],[190])).
% fof(193, plain,![X79]:![X80]:![X81]:![X82]:(((~(occurrence_of(X81,X82))|~(root_occ(X79,X81)))|~(root_occ(X80,X81)))|X79=X80),inference(fof_nnf,[status(thm)],[32])).
% fof(194, plain,![X83]:![X84]:![X85]:![X86]:(((~(occurrence_of(X85,X86))|~(root_occ(X83,X85)))|~(root_occ(X84,X85)))|X83=X84),inference(variable_rename,[status(thm)],[193])).
% cnf(195,plain,(X1=X2|~root_occ(X2,X3)|~root_occ(X1,X3)|~occurrence_of(X3,X4)),inference(split_conjunct,[status(thm)],[194])).
% fof(196, plain,![X83]:![X84]:![X85]:((~(occurrence_of(X83,X84))|~(occurrence_of(X83,X85)))|X84=X85),inference(fof_nnf,[status(thm)],[33])).
% fof(197, plain,![X86]:![X87]:![X88]:((~(occurrence_of(X86,X87))|~(occurrence_of(X86,X88)))|X87=X88),inference(variable_rename,[status(thm)],[196])).
% cnf(198,plain,(X1=X2|~occurrence_of(X3,X2)|~occurrence_of(X3,X1)),inference(split_conjunct,[status(thm)],[197])).
% cnf(203,plain,(~atomic(tptp0)),inference(split_conjunct,[status(thm)],[45])).
% fof(204, negated_conjecture,?[X90]:occurrence_of(X90,tptp0),inference(fof_nnf,[status(thm)],[38])).
% fof(205, negated_conjecture,?[X91]:occurrence_of(X91,tptp0),inference(variable_rename,[status(thm)],[204])).
% fof(206, negated_conjecture,occurrence_of(esk16_0,tptp0),inference(skolemize,[status(esa)],[205])).
% cnf(207,negated_conjecture,(occurrence_of(esk16_0,tptp0)),inference(split_conjunct,[status(thm)],[206])).
% cnf(208,negated_conjecture,(activity_occurrence(esk16_0)),inference(spm,[status(thm)],[145,207,theory(equality)])).
% cnf(217,negated_conjecture,(X1=tptp0|~occurrence_of(esk16_0,X1)),inference(spm,[status(thm)],[198,207,theory(equality)])).
% cnf(220,plain,(X1=esk13_1(X2)|~occurrence_of(X2,X1)|~activity_occurrence(X2)),inference(spm,[status(thm)],[198,151,theory(equality)])).
% cnf(221,plain,(subactivity_occurrence(esk12_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[79,135,theory(equality)])).
% cnf(231,plain,(atomic(tptp4)|~arboreal(esk11_1(X1))|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[192,138,theory(equality)])).
% cnf(247,plain,(arboreal(esk11_1(X1))|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[163,134,theory(equality)])).
% cnf(248,plain,(min_precedes(esk11_1(X1),esk12_1(X1),tptp0)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[111,134,theory(equality)])).
% cnf(249,plain,(arboreal(esk12_1(X1))|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[162,134,theory(equality)])).
% cnf(262,plain,(X1=esk11_1(X2)|~root_occ(X1,X2)|~occurrence_of(X2,X3)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[195,137,theory(equality)])).
% cnf(264,plain,(root_occ(esk1_2(X1,X2),X3)|atomic(X1)|~subactivity_occurrence(esk1_2(X1,X2),X3)|~occurrence_of(X3,X1)|~occurrence_of(X2,X1)),inference(spm,[status(thm)],[90,55,theory(equality)])).
% cnf(272,plain,(X1=esk12_1(X2)|atomic(X3)|~leaf_occ(X1,X2)|~occurrence_of(X2,X3)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[115,135,theory(equality)])).
% cnf(280,plain,(~min_precedes(X2,esk12_1(X1),tptp0)|~min_precedes(esk11_1(X1),X2,tptp0)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[112,134,theory(equality)])).
% cnf(283,plain,(X1=tptp1|leaf_occ(X2,X3)|~occurrence_of(esk14_2(X2,X3),X1)|~arboreal(X2)|~subactivity_occurrence(X2,X3)|~occurrence_of(X3,tptp0)),inference(spm,[status(thm)],[198,172,theory(equality)])).
% cnf(303,plain,(min_precedes(X1,esk14_2(X1,X2),tptp0)|leaf_occ(X1,X2)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[111,171,theory(equality)])).
% cnf(305,plain,(arboreal(esk14_2(X1,X2))|leaf_occ(X1,X2)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[162,171,theory(equality)])).
% cnf(307,plain,(X1=X2|min_precedes(X2,X1,X3)|min_precedes(X1,X2,X3)|~arboreal(X2)|~arboreal(X1)|~subactivity_occurrence(X1,esk15_3(X4,X5,X2))|~occurrence_of(esk15_3(X4,X5,X2),X3)|~min_precedes(X5,X2,X4)),inference(spm,[status(thm)],[99,181,theory(equality)])).
% cnf(311,negated_conjecture,(esk13_1(esk16_0)=tptp0|~activity_occurrence(esk16_0)),inference(spm,[status(thm)],[217,151,theory(equality)])).
% cnf(312,negated_conjecture,(esk7_2(X1,esk16_0)=tptp0|~root_occ(X1,esk16_0)),inference(spm,[status(thm)],[217,89,theory(equality)])).
% cnf(313,negated_conjecture,(esk6_2(X1,esk16_0)=tptp0|~leaf_occ(X1,esk16_0)),inference(spm,[status(thm)],[217,80,theory(equality)])).
% cnf(314,negated_conjecture,(esk13_1(esk16_0)=tptp0|$false),inference(rw,[status(thm)],[311,208,theory(equality)])).
% cnf(315,negated_conjecture,(esk13_1(esk16_0)=tptp0),inference(cn,[status(thm)],[314,theory(equality)])).
% cnf(345,negated_conjecture,(root(X1,tptp0)|~root_occ(X1,esk16_0)),inference(spm,[status(thm)],[87,312,theory(equality)])).
% cnf(357,negated_conjecture,(root_occ(X1,X2)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)|~root_occ(X1,esk16_0)),inference(spm,[status(thm)],[90,345,theory(equality)])).
% cnf(358,negated_conjecture,(leaf(X1,tptp0)|~leaf_occ(X1,esk16_0)),inference(spm,[status(thm)],[78,313,theory(equality)])).
% cnf(373,plain,(X1=esk13_1(X2)|~occurrence_of(X2,X1)),inference(csr,[status(thm)],[220,145])).
% cnf(375,plain,(X1=esk13_1(esk15_3(X1,X2,X3))|~min_precedes(X2,X3,X1)),inference(spm,[status(thm)],[373,183,theory(equality)])).
% cnf(380,plain,(esk7_2(X1,X2)=esk13_1(X2)|~root_occ(X1,X2)),inference(spm,[status(thm)],[373,89,theory(equality)])).
% cnf(381,plain,(esk6_2(X1,X2)=esk13_1(X2)|~leaf_occ(X1,X2)),inference(spm,[status(thm)],[373,80,theory(equality)])).
% cnf(452,plain,(atomic(tptp4)|~occurrence_of(X1,tptp0)),inference(csr,[status(thm)],[231,247])).
% cnf(453,negated_conjecture,(atomic(tptp4)),inference(spm,[status(thm)],[452,207,theory(equality)])).
% cnf(499,plain,(occurrence_of(X1,esk13_1(X1))|~root_occ(X2,X1)),inference(spm,[status(thm)],[89,380,theory(equality)])).
% cnf(501,plain,(occurrence_of(X1,esk13_1(X1))|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[499,137,theory(equality)])).
% cnf(596,plain,(leaf(X1,esk13_1(X2))|~leaf_occ(X1,X2)),inference(spm,[status(thm)],[78,381,theory(equality)])).
% cnf(674,plain,(~leaf(esk11_1(X1),tptp0)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[70,248,theory(equality)])).
% cnf(683,negated_conjecture,(~occurrence_of(X1,tptp0)|~leaf_occ(esk11_1(X1),esk16_0)),inference(spm,[status(thm)],[674,358,theory(equality)])).
% cnf(814,plain,(esk1_2(X1,X2)=esk11_1(X3)|atomic(X1)|~occurrence_of(X3,tptp0)|~occurrence_of(X3,X4)|~subactivity_occurrence(esk1_2(X1,X2),X3)|~occurrence_of(X3,X1)|~occurrence_of(X2,X1)),inference(spm,[status(thm)],[262,264,theory(equality)])).
% cnf(902,plain,(X1=esk12_1(esk10_2(X1,X2))|atomic(X3)|atomic(X2)|~occurrence_of(esk10_2(X1,X2),tptp0)|~occurrence_of(esk10_2(X1,X2),X3)|~leaf(X1,X2)),inference(spm,[status(thm)],[272,120,theory(equality)])).
% cnf(927,plain,(leaf(X1,X2)|~leaf_occ(X1,esk15_3(X2,X3,X4))|~min_precedes(X3,X4,X2)),inference(spm,[status(thm)],[596,375,theory(equality)])).
% cnf(936,negated_conjecture,(root_occ(esk11_1(esk16_0),X1)|~subactivity_occurrence(esk11_1(esk16_0),X1)|~occurrence_of(X1,tptp0)|~occurrence_of(esk16_0,tptp0)),inference(spm,[status(thm)],[357,137,theory(equality)])).
% cnf(939,negated_conjecture,(root_occ(esk11_1(esk16_0),X1)|~subactivity_occurrence(esk11_1(esk16_0),X1)|~occurrence_of(X1,tptp0)|$false),inference(rw,[status(thm)],[936,207,theory(equality)])).
% cnf(940,negated_conjecture,(root_occ(esk11_1(esk16_0),X1)|~subactivity_occurrence(esk11_1(esk16_0),X1)|~occurrence_of(X1,tptp0)),inference(cn,[status(thm)],[939,theory(equality)])).
% cnf(952,negated_conjecture,(esk11_1(esk16_0)=esk11_1(X1)|~occurrence_of(X1,tptp0)|~occurrence_of(X1,X2)|~subactivity_occurrence(esk11_1(esk16_0),X1)),inference(spm,[status(thm)],[262,940,theory(equality)])).
% cnf(1334,plain,(leaf_occ(X1,X3)|~leaf_occ(X1,X2)|~occurrence_of(X2,tptp0)|~arboreal(X1)|~subactivity_occurrence(X1,X3)|~occurrence_of(X3,tptp0)),inference(spm,[status(thm)],[187,303,theory(equality)])).
% cnf(1357,plain,(leaf_occ(esk12_1(X1),X2)|~arboreal(esk12_1(X1))|~subactivity_occurrence(esk12_1(X1),X2)|~occurrence_of(X1,tptp0)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[1334,135,theory(equality)])).
% cnf(1359,plain,(leaf_occ(esk12_1(X1),X2)|~subactivity_occurrence(esk12_1(X1),X2)|~occurrence_of(X1,tptp0)|~occurrence_of(X2,tptp0)),inference(csr,[status(thm)],[1357,249])).
% cnf(1395,plain,(esk12_1(esk15_3(X1,X2,X3))=X3|min_precedes(esk12_1(esk15_3(X1,X2,X3)),X3,X4)|min_precedes(X3,esk12_1(esk15_3(X1,X2,X3)),X4)|~arboreal(X3)|~arboreal(esk12_1(esk15_3(X1,X2,X3)))|~min_precedes(X2,X3,X1)|~occurrence_of(esk15_3(X1,X2,X3),X4)|~occurrence_of(esk15_3(X1,X2,X3),tptp0)),inference(spm,[status(thm)],[307,221,theory(equality)])).
% cnf(1405,negated_conjecture,(esk11_1(esk16_0)=esk11_1(esk15_3(X1,esk11_1(esk16_0),X2))|~occurrence_of(esk15_3(X1,esk11_1(esk16_0),X2),tptp0)|~occurrence_of(esk15_3(X1,esk11_1(esk16_0),X2),X3)|~min_precedes(esk11_1(esk16_0),X2,X1)),inference(spm,[status(thm)],[952,182,theory(equality)])).
% cnf(2082,plain,(leaf(esk12_1(X1),X2)|~min_precedes(X3,X4,X2)|~subactivity_occurrence(esk12_1(X1),esk15_3(X2,X3,X4))|~occurrence_of(X1,tptp0)|~occurrence_of(esk15_3(X2,X3,X4),tptp0)),inference(spm,[status(thm)],[927,1359,theory(equality)])).
% cnf(2134,plain,(leaf(esk12_1(X1),X2)|~min_precedes(esk12_1(X1),X3,X2)|~occurrence_of(esk15_3(X2,esk12_1(X1),X3),tptp0)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[2082,182,theory(equality)])).
% cnf(2135,plain,(leaf(esk12_1(esk15_3(X1,X2,X3)),X1)|~min_precedes(X2,X3,X1)|~occurrence_of(esk15_3(X1,X2,X3),tptp0)),inference(spm,[status(thm)],[2082,221,theory(equality)])).
% cnf(2174,plain,(~min_precedes(esk12_1(X1),X3,X2)|~occurrence_of(esk15_3(X2,esk12_1(X1),X3),tptp0)|~occurrence_of(X1,tptp0)),inference(csr,[status(thm)],[2134,70])).
% cnf(2175,plain,(~min_precedes(esk12_1(X1),X2,tptp0)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[2174,183,theory(equality)])).
% cnf(2788,plain,(esk1_2(X1,X2)=esk11_1(X2)|atomic(X1)|~occurrence_of(X2,tptp0)|~occurrence_of(X2,X3)|~occurrence_of(X2,X1)),inference(spm,[status(thm)],[814,54,theory(equality)])).
% cnf(3084,negated_conjecture,(esk1_2(X1,esk16_0)=esk11_1(esk16_0)|atomic(X1)|~occurrence_of(esk16_0,tptp0)|~occurrence_of(esk16_0,X1)),inference(spm,[status(thm)],[2788,207,theory(equality)])).
% cnf(3097,negated_conjecture,(esk1_2(X1,esk16_0)=esk11_1(esk16_0)|atomic(X1)|$false|~occurrence_of(esk16_0,X1)),inference(rw,[status(thm)],[3084,207,theory(equality)])).
% cnf(3098,negated_conjecture,(esk1_2(X1,esk16_0)=esk11_1(esk16_0)|atomic(X1)|~occurrence_of(esk16_0,X1)),inference(cn,[status(thm)],[3097,theory(equality)])).
% cnf(3100,negated_conjecture,(subactivity_occurrence(esk11_1(esk16_0),esk16_0)|atomic(X1)|~occurrence_of(esk16_0,X1)),inference(spm,[status(thm)],[54,3098,theory(equality)])).
% cnf(3138,negated_conjecture,(subactivity_occurrence(esk11_1(esk16_0),esk16_0)|atomic(esk13_1(esk16_0))|~activity_occurrence(esk16_0)),inference(spm,[status(thm)],[3100,151,theory(equality)])).
% cnf(3143,negated_conjecture,(subactivity_occurrence(esk11_1(esk16_0),esk16_0)|atomic(tptp0)|~activity_occurrence(esk16_0)),inference(rw,[status(thm)],[3138,315,theory(equality)])).
% cnf(3144,negated_conjecture,(subactivity_occurrence(esk11_1(esk16_0),esk16_0)|atomic(tptp0)|$false),inference(rw,[status(thm)],[3143,208,theory(equality)])).
% cnf(3145,negated_conjecture,(subactivity_occurrence(esk11_1(esk16_0),esk16_0)|atomic(tptp0)),inference(cn,[status(thm)],[3144,theory(equality)])).
% cnf(3146,negated_conjecture,(subactivity_occurrence(esk11_1(esk16_0),esk16_0)),inference(sr,[status(thm)],[3145,203,theory(equality)])).
% cnf(3588,plain,(esk12_1(esk10_2(X1,X2))=X1|atomic(X2)|~leaf(X1,X2)|~occurrence_of(esk10_2(X1,X2),tptp0)),inference(spm,[status(thm)],[902,121,theory(equality)])).
% cnf(4601,plain,(occurrence_of(X1,tptp3)|atomic(X2)|~occurrence_of(esk10_2(X1,X2),tptp0)|~leaf(X1,X2)),inference(spm,[status(thm)],[136,3588,theory(equality)])).
% cnf(4690,plain,(atomic(tptp0)|occurrence_of(X1,tptp3)|~leaf(X1,tptp0)),inference(spm,[status(thm)],[4601,121,theory(equality)])).
% cnf(4692,plain,(occurrence_of(X1,tptp3)|~leaf(X1,tptp0)),inference(sr,[status(thm)],[4690,203,theory(equality)])).
% cnf(4695,plain,(occurrence_of(esk12_1(esk15_3(tptp0,X1,X2)),tptp3)|~min_precedes(X1,X2,tptp0)|~occurrence_of(esk15_3(tptp0,X1,X2),tptp0)),inference(spm,[status(thm)],[4692,2135,theory(equality)])).
% cnf(5192,plain,(occurrence_of(esk12_1(esk15_3(tptp0,X1,X2)),tptp3)|~min_precedes(X1,X2,tptp0)),inference(csr,[status(thm)],[4695,183])).
% cnf(6826,plain,(esk12_1(esk15_3(X1,X2,X3))=X3|min_precedes(esk12_1(esk15_3(X1,X2,X3)),X3,X4)|min_precedes(X3,esk12_1(esk15_3(X1,X2,X3)),X4)|~arboreal(X3)|~min_precedes(X2,X3,X1)|~occurrence_of(esk15_3(X1,X2,X3),tptp0)|~occurrence_of(esk15_3(X1,X2,X3),X4)),inference(csr,[status(thm)],[1395,249])).
% cnf(6845,plain,(esk12_1(esk15_3(X1,X2,X3))=X3|min_precedes(X3,esk12_1(esk15_3(X1,X2,X3)),tptp0)|~occurrence_of(esk15_3(X1,X2,X3),tptp0)|~arboreal(X3)|~min_precedes(X2,X3,X1)),inference(spm,[status(thm)],[2175,6826,theory(equality)])).
% cnf(7188,negated_conjecture,(esk11_1(esk15_3(X1,esk11_1(esk16_0),X2))=esk11_1(esk16_0)|~min_precedes(esk11_1(esk16_0),X2,X1)|~occurrence_of(esk15_3(X1,esk11_1(esk16_0),X2),tptp0)),inference(spm,[status(thm)],[1405,501,theory(equality)])).
% cnf(11817,negated_conjecture,(occurrence_of(esk11_1(esk16_0),tptp4)|~occurrence_of(esk15_3(X1,esk11_1(esk16_0),X2),tptp0)|~min_precedes(esk11_1(esk16_0),X2,X1)),inference(spm,[status(thm)],[138,7188,theory(equality)])).
% cnf(11984,negated_conjecture,(occurrence_of(esk11_1(esk16_0),tptp4)|~min_precedes(esk11_1(esk16_0),X1,tptp0)),inference(spm,[status(thm)],[11817,183,theory(equality)])).
% cnf(11992,negated_conjecture,(occurrence_of(esk11_1(esk16_0),tptp4)|~occurrence_of(esk16_0,tptp0)),inference(spm,[status(thm)],[11984,248,theory(equality)])).
% cnf(11995,negated_conjecture,(occurrence_of(esk11_1(esk16_0),tptp4)|$false),inference(rw,[status(thm)],[11992,207,theory(equality)])).
% cnf(11996,negated_conjecture,(occurrence_of(esk11_1(esk16_0),tptp4)),inference(cn,[status(thm)],[11995,theory(equality)])).
% cnf(12076,negated_conjecture,(arboreal(esk11_1(esk16_0))|~atomic(tptp4)),inference(spm,[status(thm)],[191,11996,theory(equality)])).
% cnf(12091,negated_conjecture,(arboreal(esk11_1(esk16_0))|$false),inference(rw,[status(thm)],[12076,453,theory(equality)])).
% cnf(12092,negated_conjecture,(arboreal(esk11_1(esk16_0))),inference(cn,[status(thm)],[12091,theory(equality)])).
% cnf(19740,plain,(esk12_1(esk15_3(X2,X3,X1))=X1|~min_precedes(esk11_1(esk15_3(X2,X3,X1)),X1,tptp0)|~occurrence_of(esk15_3(X2,X3,X1),tptp0)|~arboreal(X1)|~min_precedes(X3,X1,X2)),inference(spm,[status(thm)],[280,6845,theory(equality)])).
% cnf(22522,negated_conjecture,(esk12_1(esk15_3(X1,esk11_1(esk16_0),X2))=X2|~arboreal(X2)|~min_precedes(esk11_1(esk16_0),X2,tptp0)|~min_precedes(esk11_1(esk16_0),X2,X1)|~occurrence_of(esk15_3(X1,esk11_1(esk16_0),X2),tptp0)),inference(spm,[status(thm)],[19740,7188,theory(equality)])).
% cnf(24053,negated_conjecture,(occurrence_of(X1,tptp3)|~min_precedes(esk11_1(esk16_0),X1,tptp0)|~arboreal(X1)|~occurrence_of(esk15_3(tptp0,esk11_1(esk16_0),X1),tptp0)),inference(spm,[status(thm)],[5192,22522,theory(equality)])).
% cnf(24078,negated_conjecture,(occurrence_of(X1,tptp3)|~arboreal(X1)|~min_precedes(esk11_1(esk16_0),X1,tptp0)),inference(csr,[status(thm)],[24053,183])).
% cnf(24079,negated_conjecture,(occurrence_of(esk14_2(esk11_1(esk16_0),X1),tptp3)|leaf_occ(esk11_1(esk16_0),X1)|~arboreal(esk14_2(esk11_1(esk16_0),X1))|~arboreal(esk11_1(esk16_0))|~subactivity_occurrence(esk11_1(esk16_0),X1)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[24078,303,theory(equality)])).
% cnf(24090,negated_conjecture,(occurrence_of(esk14_2(esk11_1(esk16_0),X1),tptp3)|leaf_occ(esk11_1(esk16_0),X1)|~arboreal(esk14_2(esk11_1(esk16_0),X1))|$false|~subactivity_occurrence(esk11_1(esk16_0),X1)|~occurrence_of(X1,tptp0)),inference(rw,[status(thm)],[24079,12092,theory(equality)])).
% cnf(24091,negated_conjecture,(occurrence_of(esk14_2(esk11_1(esk16_0),X1),tptp3)|leaf_occ(esk11_1(esk16_0),X1)|~arboreal(esk14_2(esk11_1(esk16_0),X1))|~subactivity_occurrence(esk11_1(esk16_0),X1)|~occurrence_of(X1,tptp0)),inference(cn,[status(thm)],[24090,theory(equality)])).
% cnf(25195,negated_conjecture,(leaf_occ(esk11_1(esk16_0),X1)|occurrence_of(esk14_2(esk11_1(esk16_0),X1),tptp3)|~subactivity_occurrence(esk11_1(esk16_0),X1)|~occurrence_of(X1,tptp0)|~arboreal(esk11_1(esk16_0))),inference(spm,[status(thm)],[24091,305,theory(equality)])).
% cnf(25196,negated_conjecture,(leaf_occ(esk11_1(esk16_0),X1)|occurrence_of(esk14_2(esk11_1(esk16_0),X1),tptp3)|~subactivity_occurrence(esk11_1(esk16_0),X1)|~occurrence_of(X1,tptp0)|$false),inference(rw,[status(thm)],[25195,12092,theory(equality)])).
% cnf(25197,negated_conjecture,(leaf_occ(esk11_1(esk16_0),X1)|occurrence_of(esk14_2(esk11_1(esk16_0),X1),tptp3)|~subactivity_occurrence(esk11_1(esk16_0),X1)|~occurrence_of(X1,tptp0)),inference(cn,[status(thm)],[25196,theory(equality)])).
% cnf(25210,negated_conjecture,(tptp3=tptp1|leaf_occ(esk11_1(esk16_0),X1)|~arboreal(esk11_1(esk16_0))|~subactivity_occurrence(esk11_1(esk16_0),X1)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[283,25197,theory(equality)])).
% cnf(25219,negated_conjecture,(tptp3=tptp1|leaf_occ(esk11_1(esk16_0),X1)|$false|~subactivity_occurrence(esk11_1(esk16_0),X1)|~occurrence_of(X1,tptp0)),inference(rw,[status(thm)],[25210,12092,theory(equality)])).
% cnf(25220,negated_conjecture,(tptp3=tptp1|leaf_occ(esk11_1(esk16_0),X1)|~subactivity_occurrence(esk11_1(esk16_0),X1)|~occurrence_of(X1,tptp0)),inference(cn,[status(thm)],[25219,theory(equality)])).
% cnf(25221,negated_conjecture,(leaf_occ(esk11_1(esk16_0),X1)|~subactivity_occurrence(esk11_1(esk16_0),X1)|~occurrence_of(X1,tptp0)),inference(sr,[status(thm)],[25220,47,theory(equality)])).
% cnf(25300,negated_conjecture,(~occurrence_of(esk16_0,tptp0)|~subactivity_occurrence(esk11_1(esk16_0),esk16_0)),inference(spm,[status(thm)],[683,25221,theory(equality)])).
% cnf(25470,negated_conjecture,($false|~subactivity_occurrence(esk11_1(esk16_0),esk16_0)),inference(rw,[status(thm)],[25300,207,theory(equality)])).
% cnf(25471,negated_conjecture,($false|$false),inference(rw,[status(thm)],[25470,3146,theory(equality)])).
% cnf(25472,negated_conjecture,($false),inference(cn,[status(thm)],[25471,theory(equality)])).
% cnf(25473,negated_conjecture,($false),25472,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 5556
% # ...of these trivial : 41
% # ...subsumed : 3753
% # ...remaining for further processing: 1762
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 108
% # Backward-rewritten : 23
% # Generated clauses : 16594
% # ...of the previous two non-trivial : 15069
% # Contextual simplify-reflections : 5505
% # Paramodulations : 16588
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 1561
% # Positive orientable unit clauses: 24
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 16
% # Non-unit-clauses : 1521
% # Current number of unprocessed clauses: 8381
% # ...number of literals in the above : 58723
% # Clause-clause subsumption calls (NU) : 210982
% # Rec. Clause-clause subsumption calls : 60851
% # Unit Clause-clause subsumption calls : 2352
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 15
% # Indexed BW rewrite successes : 15
% # Backwards rewriting index: 1000 leaves, 1.86+/-2.960 terms/leaf
% # Paramod-from index: 288 leaves, 1.22+/-0.744 terms/leaf
% # Paramod-into index: 853 leaves, 1.58+/-1.555 terms/leaf
% # -------------------------------------------------
% # User time : 1.708 s
% # System time : 0.042 s
% # Total time : 1.750 s
% # Maximum resident set size: 0 pages
% PrfWatch: 2.19 CPU 2.30 WC
% FINAL PrfWatch: 2.19 CPU 2.30 WC
% SZS output end Solution for /tmp/SystemOnTPTP7063/PRO006+2.tptp
%
%------------------------------------------------------------------------------