%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : PRO009+1 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art01.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:08:45 EST 2010
% Result : Theorem 0s
% Output : Solution 0s
% 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/SystemOnTPTP5474/PRO009+1.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_35:
% CSA axiom sos_35 found
% Looking for CSA axiom ... sos_45:
% CSA axiom sos_45 found
% Looking for CSA axiom ... sos_46:
% CSA axiom sos_46 found
% ---- Iteration 2 (3 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ... not found
% Looking for CSA axiom ... sos_47:
% CSA axiom sos_47 found
% Looking for CSA axiom ... sos_25:
% CSA axiom sos_25 found
% Looking for CSA axiom ... sos_29:
% CSA axiom sos_29 found
% ---- Iteration 3 (6 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_37:
% CSA axiom sos_37 found
% Looking for CSA axiom ... sos_39:
% CSA axiom sos_39 found
% Looking for CSA axiom ... sos_40:
% CSA axiom sos_40 found
% ---- Iteration 4 (9 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_41:
% CSA axiom sos_41 found
% Looking for CSA axiom ... sos_33:
% CSA axiom sos_33 found
% Looking for CSA axiom ... sos_36:
% CSA axiom sos_36 found
% ---- Iteration 5 (12 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_31:
% CSA axiom sos_31 found
% Looking for CSA axiom ... sos_19:
% CSA axiom sos_19 found
% Looking for CSA axiom ... sos_34:
% CSA axiom sos_34 found
% ---- Iteration 6 (15 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_13:
% CSA axiom sos_13 found
% Looking for CSA axiom ... sos_14:
% CSA axiom sos_14 found
% Looking for CSA axiom ... sos_02:
% CSA axiom sos_02 found
% ---- Iteration 7 (18 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_15:
% CSA axiom sos_15 found
% Looking for CSA axiom ... sos_18:
% CSA axiom sos_18 found
% Looking for CSA axiom ... sos_20:
% CSA axiom sos_20 found
% ---- Iteration 8 (21 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_26:
% CSA axiom sos_26 found
% Looking for CSA axiom ... sos_27:
% CSA axiom sos_27 found
% ---- Iteration 9 (24 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_42:
% CSA axiom sos_42 found
% Looking for CSA axiom ... sos_43:
% CSA axiom sos_43 found
% Looking for CSA axiom ... sos_44:
% CSA axiom sos_44 found
% ---- Iteration 10 (27 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_04:
% CSA axiom sos_04 found
% Looking for CSA axiom ... sos_05:
% CSA axiom sos_05 found
% Looking for CSA axiom ... sos_21:
% CSA axiom sos_21 found
% ---- Iteration 11 (30 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sos_32:
% CSA axiom sos_32 found
% Looking for CSA axiom ... sos_11:
% CSA axiom sos_11 found
% Looking for CSA axiom ... sos_07: CSA axiom sos_07 found
% ---- Iteration 12 (33 axioms selected)
% Looking for TBU SAT ... yes
% Looking for TBU model ... not found
% Looking for CSA axiom ... sos_28: CSA axiom sos_28 found
% Looking for CSA axiom ... sos: CSA axiom sos found
% Looking for CSA axiom ... sos_01: CSA axiom sos_01 found
% ---- Iteration 13 (36 axioms selected)
% Looking for TBU SAT ... no
% Looking for TBU UNS ... yes - theorem proved
% ---- Selection completed
% Selected axioms are ... :sos_01:sos:sos_28:sos_07:sos_11:sos_32:sos_21:sos_05:sos_04:sos_44:sos_43:sos_42:sos_27:sos_26:sos_22:sos_20:sos_18:sos_15:sos_02:sos_14:sos_13:sos_34:sos_19:sos_31:sos_36:sos_33:sos_41:sos_40:sos_39:sos_37:sos_29:sos_25:sos_47:sos_46:sos_45:sos_35 (36)
% Unselected axioms are ... :sos_38:sos_03:sos_06:sos_16:sos_24:sos_30:sos_17:sos_08:sos_09:sos_10:sos_12:sos_23 (12)
% SZS status THM for /tmp/SystemOnTPTP5474/PRO009+1.tptp
% Looking for THM ... found
% SZS output start Solution for /tmp/SystemOnTPTP5474/PRO009+1.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 11011
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% PrfWatch: 1.96 CPU 2.02 WC
% # Preprocessing time : 0.017 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:(activity_occurrence(X1)=>?[X2]:(activity(X2)&occurrence_of(X1,X2))),file('/tmp/SRASS.s.p', sos_01)).
% fof(2, axiom,![X3]:![X4]:(occurrence_of(X4,X3)=>(activity(X3)&activity_occurrence(X4))),file('/tmp/SRASS.s.p', sos)).
% fof(3, axiom,![X5]:![X6]:![X7]:![X8]:(((((occurrence_of(X6,X5)&arboreal(X7))&arboreal(X8))&subactivity_occurrence(X7,X6))&subactivity_occurrence(X8,X6))=>((min_precedes(X7,X8,X5)|min_precedes(X8,X7,X5))|X7=X8)),file('/tmp/SRASS.s.p', sos_28)).
% fof(4, axiom,![X9]:![X10]:(occurrence_of(X9,X10)=>(arboreal(X9)<=>atomic(X10))),file('/tmp/SRASS.s.p', sos_07)).
% fof(7, axiom,![X21]:![X22]:(leaf(X21,X22)<=>((root(X21,X22)|?[X23]:min_precedes(X23,X21,X22))&~(?[X24]:min_precedes(X21,X24,X22)))),file('/tmp/SRASS.s.p', sos_21)).
% fof(15, axiom,![X36]:![X37]:![X38]:(next_subocc(X36,X37,X38)<=>(min_precedes(X36,X37,X38)&~(?[X39]:(min_precedes(X36,X39,X38)&min_precedes(X39,X37,X38))))),file('/tmp/SRASS.s.p', sos_22)).
% fof(19, axiom,![X51]:![X52]:![X53]:((occurrence_of(X51,X52)&occurrence_of(X51,X53))=>X52=X53),file('/tmp/SRASS.s.p', sos_02)).
% fof(22, axiom,![X61]:![X62]:(leaf_occ(X61,X62)<=>?[X63]:((occurrence_of(X62,X63)&subactivity_occurrence(X61,X62))&leaf(X61,X63))),file('/tmp/SRASS.s.p', sos_34)).
% fof(26, axiom,![X70]:![X71]:(root_occ(X70,X71)<=>?[X72]:((occurrence_of(X71,X72)&subactivity_occurrence(X70,X71))&root(X70,X72))),file('/tmp/SRASS.s.p', sos_33)).
% fof(27, axiom,atomic(tptp3),file('/tmp/SRASS.s.p', sos_41)).
% fof(28, axiom,atomic(tptp1),file('/tmp/SRASS.s.p', sos_40)).
% fof(29, axiom,atomic(tptp2),file('/tmp/SRASS.s.p', sos_39)).
% fof(32, axiom,![X77]:![X78]:![X79]:(min_precedes(X78,X79,X77)=>?[X80]:((occurrence_of(X80,X77)&subactivity_occurrence(X78,X80))&subactivity_occurrence(X79,X80))),file('/tmp/SRASS.s.p', sos_25)).
% fof(36, axiom,![X81]:(occurrence_of(X81,tptp0)=>?[X82]:?[X83]:?[X84]:((((((occurrence_of(X82,tptp3)&root_occ(X82,X81))&occurrence_of(X83,tptp4))&next_subocc(X82,X83,tptp0))&(occurrence_of(X84,tptp2)|occurrence_of(X84,tptp1)))&next_subocc(X83,X84,tptp0))&leaf_occ(X84,X81))),file('/tmp/SRASS.s.p', sos_35)).
% fof(37, conjecture,![X85]:(occurrence_of(X85,tptp0)=>?[X86]:?[X87]:((((occurrence_of(X86,tptp3)&root_occ(X86,X85))&(occurrence_of(X87,tptp2)|occurrence_of(X87,tptp1)))&min_precedes(X86,X87,tptp0))&leaf_occ(X87,X85))),file('/tmp/SRASS.s.p', goals)).
% fof(38, negated_conjecture,~(![X85]:(occurrence_of(X85,tptp0)=>?[X86]:?[X87]:((((occurrence_of(X86,tptp3)&root_occ(X86,X85))&(occurrence_of(X87,tptp2)|occurrence_of(X87,tptp1)))&min_precedes(X86,X87,tptp0))&leaf_occ(X87,X85)))),inference(assume_negation,[status(cth)],[37])).
% fof(46, plain,![X1]:(~(activity_occurrence(X1))|?[X2]:(activity(X2)&occurrence_of(X1,X2))),inference(fof_nnf,[status(thm)],[1])).
% fof(47, plain,![X3]:(~(activity_occurrence(X3))|?[X4]:(activity(X4)&occurrence_of(X3,X4))),inference(variable_rename,[status(thm)],[46])).
% fof(48, plain,![X3]:(~(activity_occurrence(X3))|(activity(esk1_1(X3))&occurrence_of(X3,esk1_1(X3)))),inference(skolemize,[status(esa)],[47])).
% fof(49, plain,![X3]:((activity(esk1_1(X3))|~(activity_occurrence(X3)))&(occurrence_of(X3,esk1_1(X3))|~(activity_occurrence(X3)))),inference(distribute,[status(thm)],[48])).
% cnf(50,plain,(occurrence_of(X1,esk1_1(X1))|~activity_occurrence(X1)),inference(split_conjunct,[status(thm)],[49])).
% fof(52, plain,![X3]:![X4]:(~(occurrence_of(X4,X3))|(activity(X3)&activity_occurrence(X4))),inference(fof_nnf,[status(thm)],[2])).
% fof(53, plain,![X5]:![X6]:(~(occurrence_of(X6,X5))|(activity(X5)&activity_occurrence(X6))),inference(variable_rename,[status(thm)],[52])).
% fof(54, plain,![X5]:![X6]:((activity(X5)|~(occurrence_of(X6,X5)))&(activity_occurrence(X6)|~(occurrence_of(X6,X5)))),inference(distribute,[status(thm)],[53])).
% cnf(55,plain,(activity_occurrence(X1)|~occurrence_of(X1,X2)),inference(split_conjunct,[status(thm)],[54])).
% fof(57, plain,![X5]:![X6]:![X7]:![X8]:(((((~(occurrence_of(X6,X5))|~(arboreal(X7)))|~(arboreal(X8)))|~(subactivity_occurrence(X7,X6)))|~(subactivity_occurrence(X8,X6)))|((min_precedes(X7,X8,X5)|min_precedes(X8,X7,X5))|X7=X8)),inference(fof_nnf,[status(thm)],[3])).
% fof(58, plain,![X9]:![X10]:![X11]:![X12]:(((((~(occurrence_of(X10,X9))|~(arboreal(X11)))|~(arboreal(X12)))|~(subactivity_occurrence(X11,X10)))|~(subactivity_occurrence(X12,X10)))|((min_precedes(X11,X12,X9)|min_precedes(X12,X11,X9))|X11=X12)),inference(variable_rename,[status(thm)],[57])).
% cnf(59,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)],[58])).
% fof(60, plain,![X9]:![X10]:(~(occurrence_of(X9,X10))|((~(arboreal(X9))|atomic(X10))&(~(atomic(X10))|arboreal(X9)))),inference(fof_nnf,[status(thm)],[4])).
% fof(61, plain,![X11]:![X12]:(~(occurrence_of(X11,X12))|((~(arboreal(X11))|atomic(X12))&(~(atomic(X12))|arboreal(X11)))),inference(variable_rename,[status(thm)],[60])).
% fof(62, plain,![X11]:![X12]:(((~(arboreal(X11))|atomic(X12))|~(occurrence_of(X11,X12)))&((~(atomic(X12))|arboreal(X11))|~(occurrence_of(X11,X12)))),inference(distribute,[status(thm)],[61])).
% cnf(63,plain,(arboreal(X1)|~occurrence_of(X1,X2)|~atomic(X2)),inference(split_conjunct,[status(thm)],[62])).
% fof(79, plain,![X21]:![X22]:((~(leaf(X21,X22))|((root(X21,X22)|?[X23]:min_precedes(X23,X21,X22))&![X24]:~(min_precedes(X21,X24,X22))))&(((~(root(X21,X22))&![X23]:~(min_precedes(X23,X21,X22)))|?[X24]:min_precedes(X21,X24,X22))|leaf(X21,X22))),inference(fof_nnf,[status(thm)],[7])).
% fof(80, plain,![X25]:![X26]:((~(leaf(X25,X26))|((root(X25,X26)|?[X27]:min_precedes(X27,X25,X26))&![X28]:~(min_precedes(X25,X28,X26))))&(((~(root(X25,X26))&![X29]:~(min_precedes(X29,X25,X26)))|?[X30]:min_precedes(X25,X30,X26))|leaf(X25,X26))),inference(variable_rename,[status(thm)],[79])).
% fof(81, plain,![X25]:![X26]:((~(leaf(X25,X26))|((root(X25,X26)|min_precedes(esk5_2(X25,X26),X25,X26))&![X28]:~(min_precedes(X25,X28,X26))))&(((~(root(X25,X26))&![X29]:~(min_precedes(X29,X25,X26)))|min_precedes(X25,esk6_2(X25,X26),X26))|leaf(X25,X26))),inference(skolemize,[status(esa)],[80])).
% fof(82, plain,![X25]:![X26]:![X28]:![X29]:((((~(min_precedes(X29,X25,X26))&~(root(X25,X26)))|min_precedes(X25,esk6_2(X25,X26),X26))|leaf(X25,X26))&((~(min_precedes(X25,X28,X26))&(root(X25,X26)|min_precedes(esk5_2(X25,X26),X25,X26)))|~(leaf(X25,X26)))),inference(shift_quantors,[status(thm)],[81])).
% fof(83, plain,![X25]:![X26]:![X28]:![X29]:((((~(min_precedes(X29,X25,X26))|min_precedes(X25,esk6_2(X25,X26),X26))|leaf(X25,X26))&((~(root(X25,X26))|min_precedes(X25,esk6_2(X25,X26),X26))|leaf(X25,X26)))&((~(min_precedes(X25,X28,X26))|~(leaf(X25,X26)))&((root(X25,X26)|min_precedes(esk5_2(X25,X26),X25,X26))|~(leaf(X25,X26))))),inference(distribute,[status(thm)],[82])).
% cnf(85,plain,(~leaf(X1,X2)|~min_precedes(X1,X3,X2)),inference(split_conjunct,[status(thm)],[83])).
% fof(109, plain,![X36]:![X37]:![X38]:((~(next_subocc(X36,X37,X38))|(min_precedes(X36,X37,X38)&![X39]:(~(min_precedes(X36,X39,X38))|~(min_precedes(X39,X37,X38)))))&((~(min_precedes(X36,X37,X38))|?[X39]:(min_precedes(X36,X39,X38)&min_precedes(X39,X37,X38)))|next_subocc(X36,X37,X38))),inference(fof_nnf,[status(thm)],[15])).
% fof(110, plain,![X40]:![X41]:![X42]:((~(next_subocc(X40,X41,X42))|(min_precedes(X40,X41,X42)&![X43]:(~(min_precedes(X40,X43,X42))|~(min_precedes(X43,X41,X42)))))&((~(min_precedes(X40,X41,X42))|?[X44]:(min_precedes(X40,X44,X42)&min_precedes(X44,X41,X42)))|next_subocc(X40,X41,X42))),inference(variable_rename,[status(thm)],[109])).
% fof(111, plain,![X40]:![X41]:![X42]:((~(next_subocc(X40,X41,X42))|(min_precedes(X40,X41,X42)&![X43]:(~(min_precedes(X40,X43,X42))|~(min_precedes(X43,X41,X42)))))&((~(min_precedes(X40,X41,X42))|(min_precedes(X40,esk9_3(X40,X41,X42),X42)&min_precedes(esk9_3(X40,X41,X42),X41,X42)))|next_subocc(X40,X41,X42))),inference(skolemize,[status(esa)],[110])).
% fof(112, plain,![X40]:![X41]:![X42]:![X43]:((((~(min_precedes(X40,X43,X42))|~(min_precedes(X43,X41,X42)))&min_precedes(X40,X41,X42))|~(next_subocc(X40,X41,X42)))&((~(min_precedes(X40,X41,X42))|(min_precedes(X40,esk9_3(X40,X41,X42),X42)&min_precedes(esk9_3(X40,X41,X42),X41,X42)))|next_subocc(X40,X41,X42))),inference(shift_quantors,[status(thm)],[111])).
% fof(113, plain,![X40]:![X41]:![X42]:![X43]:((((~(min_precedes(X40,X43,X42))|~(min_precedes(X43,X41,X42)))|~(next_subocc(X40,X41,X42)))&(min_precedes(X40,X41,X42)|~(next_subocc(X40,X41,X42))))&(((min_precedes(X40,esk9_3(X40,X41,X42),X42)|~(min_precedes(X40,X41,X42)))|next_subocc(X40,X41,X42))&((min_precedes(esk9_3(X40,X41,X42),X41,X42)|~(min_precedes(X40,X41,X42)))|next_subocc(X40,X41,X42)))),inference(distribute,[status(thm)],[112])).
% cnf(116,plain,(min_precedes(X1,X2,X3)|~next_subocc(X1,X2,X3)),inference(split_conjunct,[status(thm)],[113])).
% fof(127, plain,![X51]:![X52]:![X53]:((~(occurrence_of(X51,X52))|~(occurrence_of(X51,X53)))|X52=X53),inference(fof_nnf,[status(thm)],[19])).
% fof(128, plain,![X54]:![X55]:![X56]:((~(occurrence_of(X54,X55))|~(occurrence_of(X54,X56)))|X55=X56),inference(variable_rename,[status(thm)],[127])).
% cnf(129,plain,(X1=X2|~occurrence_of(X3,X2)|~occurrence_of(X3,X1)),inference(split_conjunct,[status(thm)],[128])).
% fof(139, plain,![X61]:![X62]:((~(leaf_occ(X61,X62))|?[X63]:((occurrence_of(X62,X63)&subactivity_occurrence(X61,X62))&leaf(X61,X63)))&(![X63]:((~(occurrence_of(X62,X63))|~(subactivity_occurrence(X61,X62)))|~(leaf(X61,X63)))|leaf_occ(X61,X62))),inference(fof_nnf,[status(thm)],[22])).
% fof(140, plain,![X64]:![X65]:((~(leaf_occ(X64,X65))|?[X66]:((occurrence_of(X65,X66)&subactivity_occurrence(X64,X65))&leaf(X64,X66)))&(![X67]:((~(occurrence_of(X65,X67))|~(subactivity_occurrence(X64,X65)))|~(leaf(X64,X67)))|leaf_occ(X64,X65))),inference(variable_rename,[status(thm)],[139])).
% fof(141, plain,![X64]:![X65]:((~(leaf_occ(X64,X65))|((occurrence_of(X65,esk11_2(X64,X65))&subactivity_occurrence(X64,X65))&leaf(X64,esk11_2(X64,X65))))&(![X67]:((~(occurrence_of(X65,X67))|~(subactivity_occurrence(X64,X65)))|~(leaf(X64,X67)))|leaf_occ(X64,X65))),inference(skolemize,[status(esa)],[140])).
% fof(142, plain,![X64]:![X65]:![X67]:((((~(occurrence_of(X65,X67))|~(subactivity_occurrence(X64,X65)))|~(leaf(X64,X67)))|leaf_occ(X64,X65))&(~(leaf_occ(X64,X65))|((occurrence_of(X65,esk11_2(X64,X65))&subactivity_occurrence(X64,X65))&leaf(X64,esk11_2(X64,X65))))),inference(shift_quantors,[status(thm)],[141])).
% fof(143, plain,![X64]:![X65]:![X67]:((((~(occurrence_of(X65,X67))|~(subactivity_occurrence(X64,X65)))|~(leaf(X64,X67)))|leaf_occ(X64,X65))&(((occurrence_of(X65,esk11_2(X64,X65))|~(leaf_occ(X64,X65)))&(subactivity_occurrence(X64,X65)|~(leaf_occ(X64,X65))))&(leaf(X64,esk11_2(X64,X65))|~(leaf_occ(X64,X65))))),inference(distribute,[status(thm)],[142])).
% cnf(144,plain,(leaf(X1,esk11_2(X1,X2))|~leaf_occ(X1,X2)),inference(split_conjunct,[status(thm)],[143])).
% cnf(145,plain,(subactivity_occurrence(X1,X2)|~leaf_occ(X1,X2)),inference(split_conjunct,[status(thm)],[143])).
% cnf(146,plain,(occurrence_of(X2,esk11_2(X1,X2))|~leaf_occ(X1,X2)),inference(split_conjunct,[status(thm)],[143])).
% cnf(147,plain,(leaf_occ(X1,X2)|~leaf(X1,X3)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,X3)),inference(split_conjunct,[status(thm)],[143])).
% fof(155, plain,![X70]:![X71]:((~(root_occ(X70,X71))|?[X72]:((occurrence_of(X71,X72)&subactivity_occurrence(X70,X71))&root(X70,X72)))&(![X72]:((~(occurrence_of(X71,X72))|~(subactivity_occurrence(X70,X71)))|~(root(X70,X72)))|root_occ(X70,X71))),inference(fof_nnf,[status(thm)],[26])).
% fof(156, plain,![X73]:![X74]:((~(root_occ(X73,X74))|?[X75]:((occurrence_of(X74,X75)&subactivity_occurrence(X73,X74))&root(X73,X75)))&(![X76]:((~(occurrence_of(X74,X76))|~(subactivity_occurrence(X73,X74)))|~(root(X73,X76)))|root_occ(X73,X74))),inference(variable_rename,[status(thm)],[155])).
% fof(157, plain,![X73]:![X74]:((~(root_occ(X73,X74))|((occurrence_of(X74,esk12_2(X73,X74))&subactivity_occurrence(X73,X74))&root(X73,esk12_2(X73,X74))))&(![X76]:((~(occurrence_of(X74,X76))|~(subactivity_occurrence(X73,X74)))|~(root(X73,X76)))|root_occ(X73,X74))),inference(skolemize,[status(esa)],[156])).
% fof(158, plain,![X73]:![X74]:![X76]:((((~(occurrence_of(X74,X76))|~(subactivity_occurrence(X73,X74)))|~(root(X73,X76)))|root_occ(X73,X74))&(~(root_occ(X73,X74))|((occurrence_of(X74,esk12_2(X73,X74))&subactivity_occurrence(X73,X74))&root(X73,esk12_2(X73,X74))))),inference(shift_quantors,[status(thm)],[157])).
% fof(159, plain,![X73]:![X74]:![X76]:((((~(occurrence_of(X74,X76))|~(subactivity_occurrence(X73,X74)))|~(root(X73,X76)))|root_occ(X73,X74))&(((occurrence_of(X74,esk12_2(X73,X74))|~(root_occ(X73,X74)))&(subactivity_occurrence(X73,X74)|~(root_occ(X73,X74))))&(root(X73,esk12_2(X73,X74))|~(root_occ(X73,X74))))),inference(distribute,[status(thm)],[158])).
% cnf(161,plain,(subactivity_occurrence(X1,X2)|~root_occ(X1,X2)),inference(split_conjunct,[status(thm)],[159])).
% cnf(164,plain,(atomic(tptp3)),inference(split_conjunct,[status(thm)],[27])).
% cnf(165,plain,(atomic(tptp1)),inference(split_conjunct,[status(thm)],[28])).
% cnf(166,plain,(atomic(tptp2)),inference(split_conjunct,[status(thm)],[29])).
% fof(171, plain,![X77]:![X78]:![X79]:(~(min_precedes(X78,X79,X77))|?[X80]:((occurrence_of(X80,X77)&subactivity_occurrence(X78,X80))&subactivity_occurrence(X79,X80))),inference(fof_nnf,[status(thm)],[32])).
% fof(172, plain,![X81]:![X82]:![X83]:(~(min_precedes(X82,X83,X81))|?[X84]:((occurrence_of(X84,X81)&subactivity_occurrence(X82,X84))&subactivity_occurrence(X83,X84))),inference(variable_rename,[status(thm)],[171])).
% fof(173, plain,![X81]:![X82]:![X83]:(~(min_precedes(X82,X83,X81))|((occurrence_of(esk13_3(X81,X82,X83),X81)&subactivity_occurrence(X82,esk13_3(X81,X82,X83)))&subactivity_occurrence(X83,esk13_3(X81,X82,X83)))),inference(skolemize,[status(esa)],[172])).
% fof(174, plain,![X81]:![X82]:![X83]:(((occurrence_of(esk13_3(X81,X82,X83),X81)|~(min_precedes(X82,X83,X81)))&(subactivity_occurrence(X82,esk13_3(X81,X82,X83))|~(min_precedes(X82,X83,X81))))&(subactivity_occurrence(X83,esk13_3(X81,X82,X83))|~(min_precedes(X82,X83,X81)))),inference(distribute,[status(thm)],[173])).
% cnf(176,plain,(subactivity_occurrence(X1,esk13_3(X3,X1,X2))|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[174])).
% cnf(177,plain,(occurrence_of(esk13_3(X3,X1,X2),X3)|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[174])).
% fof(181, plain,![X81]:(~(occurrence_of(X81,tptp0))|?[X82]:?[X83]:?[X84]:((((((occurrence_of(X82,tptp3)&root_occ(X82,X81))&occurrence_of(X83,tptp4))&next_subocc(X82,X83,tptp0))&(occurrence_of(X84,tptp2)|occurrence_of(X84,tptp1)))&next_subocc(X83,X84,tptp0))&leaf_occ(X84,X81))),inference(fof_nnf,[status(thm)],[36])).
% fof(182, plain,![X85]:(~(occurrence_of(X85,tptp0))|?[X86]:?[X87]:?[X88]:((((((occurrence_of(X86,tptp3)&root_occ(X86,X85))&occurrence_of(X87,tptp4))&next_subocc(X86,X87,tptp0))&(occurrence_of(X88,tptp2)|occurrence_of(X88,tptp1)))&next_subocc(X87,X88,tptp0))&leaf_occ(X88,X85))),inference(variable_rename,[status(thm)],[181])).
% fof(183, plain,![X85]:(~(occurrence_of(X85,tptp0))|((((((occurrence_of(esk14_1(X85),tptp3)&root_occ(esk14_1(X85),X85))&occurrence_of(esk15_1(X85),tptp4))&next_subocc(esk14_1(X85),esk15_1(X85),tptp0))&(occurrence_of(esk16_1(X85),tptp2)|occurrence_of(esk16_1(X85),tptp1)))&next_subocc(esk15_1(X85),esk16_1(X85),tptp0))&leaf_occ(esk16_1(X85),X85))),inference(skolemize,[status(esa)],[182])).
% fof(184, plain,![X85]:(((((((occurrence_of(esk14_1(X85),tptp3)|~(occurrence_of(X85,tptp0)))&(root_occ(esk14_1(X85),X85)|~(occurrence_of(X85,tptp0))))&(occurrence_of(esk15_1(X85),tptp4)|~(occurrence_of(X85,tptp0))))&(next_subocc(esk14_1(X85),esk15_1(X85),tptp0)|~(occurrence_of(X85,tptp0))))&((occurrence_of(esk16_1(X85),tptp2)|occurrence_of(esk16_1(X85),tptp1))|~(occurrence_of(X85,tptp0))))&(next_subocc(esk15_1(X85),esk16_1(X85),tptp0)|~(occurrence_of(X85,tptp0))))&(leaf_occ(esk16_1(X85),X85)|~(occurrence_of(X85,tptp0)))),inference(distribute,[status(thm)],[183])).
% cnf(185,plain,(leaf_occ(esk16_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[184])).
% cnf(187,plain,(occurrence_of(esk16_1(X1),tptp1)|occurrence_of(esk16_1(X1),tptp2)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[184])).
% cnf(188,plain,(next_subocc(esk14_1(X1),esk15_1(X1),tptp0)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[184])).
% cnf(190,plain,(root_occ(esk14_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[184])).
% cnf(191,plain,(occurrence_of(esk14_1(X1),tptp3)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[184])).
% fof(192, negated_conjecture,?[X85]:(occurrence_of(X85,tptp0)&![X86]:![X87]:((((~(occurrence_of(X86,tptp3))|~(root_occ(X86,X85)))|(~(occurrence_of(X87,tptp2))&~(occurrence_of(X87,tptp1))))|~(min_precedes(X86,X87,tptp0)))|~(leaf_occ(X87,X85)))),inference(fof_nnf,[status(thm)],[38])).
% fof(193, negated_conjecture,?[X88]:(occurrence_of(X88,tptp0)&![X89]:![X90]:((((~(occurrence_of(X89,tptp3))|~(root_occ(X89,X88)))|(~(occurrence_of(X90,tptp2))&~(occurrence_of(X90,tptp1))))|~(min_precedes(X89,X90,tptp0)))|~(leaf_occ(X90,X88)))),inference(variable_rename,[status(thm)],[192])).
% fof(194, negated_conjecture,(occurrence_of(esk17_0,tptp0)&![X89]:![X90]:((((~(occurrence_of(X89,tptp3))|~(root_occ(X89,esk17_0)))|(~(occurrence_of(X90,tptp2))&~(occurrence_of(X90,tptp1))))|~(min_precedes(X89,X90,tptp0)))|~(leaf_occ(X90,esk17_0)))),inference(skolemize,[status(esa)],[193])).
% fof(195, negated_conjecture,![X89]:![X90]:(((((~(occurrence_of(X89,tptp3))|~(root_occ(X89,esk17_0)))|(~(occurrence_of(X90,tptp2))&~(occurrence_of(X90,tptp1))))|~(min_precedes(X89,X90,tptp0)))|~(leaf_occ(X90,esk17_0)))&occurrence_of(esk17_0,tptp0)),inference(shift_quantors,[status(thm)],[194])).
% fof(196, negated_conjecture,![X89]:![X90]:(((((~(occurrence_of(X90,tptp2))|(~(occurrence_of(X89,tptp3))|~(root_occ(X89,esk17_0))))|~(min_precedes(X89,X90,tptp0)))|~(leaf_occ(X90,esk17_0)))&(((~(occurrence_of(X90,tptp1))|(~(occurrence_of(X89,tptp3))|~(root_occ(X89,esk17_0))))|~(min_precedes(X89,X90,tptp0)))|~(leaf_occ(X90,esk17_0))))&occurrence_of(esk17_0,tptp0)),inference(distribute,[status(thm)],[195])).
% cnf(197,negated_conjecture,(occurrence_of(esk17_0,tptp0)),inference(split_conjunct,[status(thm)],[196])).
% cnf(198,negated_conjecture,(~leaf_occ(X1,esk17_0)|~min_precedes(X2,X1,tptp0)|~root_occ(X2,esk17_0)|~occurrence_of(X2,tptp3)|~occurrence_of(X1,tptp1)),inference(split_conjunct,[status(thm)],[196])).
% cnf(199,negated_conjecture,(~leaf_occ(X1,esk17_0)|~min_precedes(X2,X1,tptp0)|~root_occ(X2,esk17_0)|~occurrence_of(X2,tptp3)|~occurrence_of(X1,tptp2)),inference(split_conjunct,[status(thm)],[196])).
% cnf(207,plain,(subactivity_occurrence(esk16_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[145,185,theory(equality)])).
% cnf(210,plain,(subactivity_occurrence(esk14_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[161,190,theory(equality)])).
% cnf(213,negated_conjecture,(X1=tptp0|~occurrence_of(esk17_0,X1)),inference(spm,[status(thm)],[129,197,theory(equality)])).
% cnf(217,plain,(X1=esk1_1(X2)|~occurrence_of(X2,X1)|~activity_occurrence(X2)),inference(spm,[status(thm)],[129,50,theory(equality)])).
% cnf(228,plain,(arboreal(esk16_1(X1))|occurrence_of(esk16_1(X1),tptp1)|~atomic(tptp2)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[63,187,theory(equality)])).
% cnf(230,plain,(arboreal(esk14_1(X1))|~atomic(tptp3)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[63,191,theory(equality)])).
% cnf(235,plain,(arboreal(esk16_1(X1))|occurrence_of(esk16_1(X1),tptp1)|$false|~occurrence_of(X1,tptp0)),inference(rw,[status(thm)],[228,166,theory(equality)])).
% cnf(236,plain,(arboreal(esk16_1(X1))|occurrence_of(esk16_1(X1),tptp1)|~occurrence_of(X1,tptp0)),inference(cn,[status(thm)],[235,theory(equality)])).
% cnf(237,plain,(arboreal(esk14_1(X1))|$false|~occurrence_of(X1,tptp0)),inference(rw,[status(thm)],[230,164,theory(equality)])).
% cnf(238,plain,(arboreal(esk14_1(X1))|~occurrence_of(X1,tptp0)),inference(cn,[status(thm)],[237,theory(equality)])).
% cnf(250,plain,(min_precedes(esk14_1(X1),esk15_1(X1),tptp0)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[116,188,theory(equality)])).
% cnf(325,negated_conjecture,(esk11_2(X1,esk17_0)=tptp0|~leaf_occ(X1,esk17_0)),inference(spm,[status(thm)],[213,146,theory(equality)])).
% cnf(363,plain,(X1=esk16_1(X2)|min_precedes(esk16_1(X2),X1,X3)|min_precedes(X1,esk16_1(X2),X3)|~subactivity_occurrence(X1,X2)|~arboreal(esk16_1(X2))|~arboreal(X1)|~occurrence_of(X2,X3)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[59,207,theory(equality)])).
% cnf(368,negated_conjecture,(leaf(X1,tptp0)|~leaf_occ(X1,esk17_0)),inference(spm,[status(thm)],[144,325,theory(equality)])).
% cnf(373,negated_conjecture,(leaf_occ(X1,X2)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)|~leaf_occ(X1,esk17_0)),inference(spm,[status(thm)],[147,368,theory(equality)])).
% cnf(378,plain,(X1=esk14_1(X2)|min_precedes(esk14_1(X2),X1,X3)|min_precedes(X1,esk14_1(X2),X3)|~subactivity_occurrence(X1,X2)|~arboreal(esk14_1(X2))|~arboreal(X1)|~occurrence_of(X2,X3)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[59,210,theory(equality)])).
% cnf(420,negated_conjecture,(leaf_occ(esk16_1(esk17_0),X1)|~subactivity_occurrence(esk16_1(esk17_0),X1)|~occurrence_of(X1,tptp0)|~occurrence_of(esk17_0,tptp0)),inference(spm,[status(thm)],[373,185,theory(equality)])).
% cnf(421,negated_conjecture,(leaf_occ(esk16_1(esk17_0),X1)|~subactivity_occurrence(esk16_1(esk17_0),X1)|~occurrence_of(X1,tptp0)|$false),inference(rw,[status(thm)],[420,197,theory(equality)])).
% cnf(422,negated_conjecture,(leaf_occ(esk16_1(esk17_0),X1)|~subactivity_occurrence(esk16_1(esk17_0),X1)|~occurrence_of(X1,tptp0)),inference(cn,[status(thm)],[421,theory(equality)])).
% cnf(464,plain,(X1=esk1_1(X2)|~occurrence_of(X2,X1)),inference(csr,[status(thm)],[217,55])).
% cnf(470,plain,(X1=esk1_1(esk13_3(X1,X2,X3))|~min_precedes(X2,X3,X1)),inference(spm,[status(thm)],[464,177,theory(equality)])).
% cnf(473,plain,(esk11_2(X1,X2)=esk1_1(X2)|~leaf_occ(X1,X2)),inference(spm,[status(thm)],[464,146,theory(equality)])).
% cnf(577,plain,(leaf(X1,esk1_1(X2))|~leaf_occ(X1,X2)),inference(spm,[status(thm)],[144,473,theory(equality)])).
% cnf(970,plain,(leaf(X1,X2)|~leaf_occ(X1,esk13_3(X2,X3,X4))|~min_precedes(X3,X4,X2)),inference(spm,[status(thm)],[577,470,theory(equality)])).
% cnf(1731,negated_conjecture,(leaf(esk16_1(esk17_0),X1)|~min_precedes(X2,X3,X1)|~subactivity_occurrence(esk16_1(esk17_0),esk13_3(X1,X2,X3))|~occurrence_of(esk13_3(X1,X2,X3),tptp0)),inference(spm,[status(thm)],[970,422,theory(equality)])).
% cnf(1910,plain,(X1=esk16_1(X2)|min_precedes(X1,esk16_1(X2),X3)|min_precedes(esk16_1(X2),X1,X3)|occurrence_of(esk16_1(X2),tptp1)|~subactivity_occurrence(X1,X2)|~arboreal(X1)|~occurrence_of(X2,tptp0)|~occurrence_of(X2,X3)),inference(spm,[status(thm)],[363,236,theory(equality)])).
% cnf(1974,plain,(X1=esk14_1(X2)|min_precedes(esk14_1(X2),X1,X3)|min_precedes(X1,esk14_1(X2),X3)|~subactivity_occurrence(X1,X2)|~arboreal(X1)|~occurrence_of(X2,tptp0)|~occurrence_of(X2,X3)),inference(csr,[status(thm)],[378,238])).
% cnf(1975,negated_conjecture,(X1=esk14_1(esk17_0)|min_precedes(X1,esk14_1(esk17_0),X2)|min_precedes(esk14_1(esk17_0),X1,X2)|~subactivity_occurrence(X1,esk17_0)|~arboreal(X1)|~occurrence_of(esk17_0,X2)),inference(spm,[status(thm)],[1974,197,theory(equality)])).
% cnf(7184,negated_conjecture,(esk16_1(esk17_0)=esk14_1(esk17_0)|min_precedes(esk14_1(esk17_0),esk16_1(esk17_0),X1)|min_precedes(esk16_1(esk17_0),esk14_1(esk17_0),X1)|~arboreal(esk16_1(esk17_0))|~occurrence_of(esk17_0,X1)|~occurrence_of(esk17_0,tptp0)),inference(spm,[status(thm)],[1975,207,theory(equality)])).
% cnf(7229,negated_conjecture,(esk16_1(esk17_0)=esk14_1(esk17_0)|min_precedes(esk14_1(esk17_0),esk16_1(esk17_0),X1)|min_precedes(esk16_1(esk17_0),esk14_1(esk17_0),X1)|~arboreal(esk16_1(esk17_0))|~occurrence_of(esk17_0,X1)|$false),inference(rw,[status(thm)],[7184,197,theory(equality)])).
% cnf(7230,negated_conjecture,(esk16_1(esk17_0)=esk14_1(esk17_0)|min_precedes(esk14_1(esk17_0),esk16_1(esk17_0),X1)|min_precedes(esk16_1(esk17_0),esk14_1(esk17_0),X1)|~arboreal(esk16_1(esk17_0))|~occurrence_of(esk17_0,X1)),inference(cn,[status(thm)],[7229,theory(equality)])).
% cnf(7723,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|min_precedes(esk16_1(esk17_0),esk14_1(esk17_0),tptp0)|~root_occ(esk14_1(esk17_0),esk17_0)|~leaf_occ(esk16_1(esk17_0),esk17_0)|~occurrence_of(esk14_1(esk17_0),tptp3)|~occurrence_of(esk16_1(esk17_0),tptp1)|~arboreal(esk16_1(esk17_0))|~occurrence_of(esk17_0,tptp0)),inference(spm,[status(thm)],[198,7230,theory(equality)])).
% cnf(7732,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|min_precedes(esk16_1(esk17_0),esk14_1(esk17_0),tptp0)|~root_occ(esk14_1(esk17_0),esk17_0)|~leaf_occ(esk16_1(esk17_0),esk17_0)|~occurrence_of(esk14_1(esk17_0),tptp3)|~occurrence_of(esk16_1(esk17_0),tptp1)|~arboreal(esk16_1(esk17_0))|$false),inference(rw,[status(thm)],[7723,197,theory(equality)])).
% cnf(7733,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|min_precedes(esk16_1(esk17_0),esk14_1(esk17_0),tptp0)|~root_occ(esk14_1(esk17_0),esk17_0)|~leaf_occ(esk16_1(esk17_0),esk17_0)|~occurrence_of(esk14_1(esk17_0),tptp3)|~occurrence_of(esk16_1(esk17_0),tptp1)|~arboreal(esk16_1(esk17_0))),inference(cn,[status(thm)],[7732,theory(equality)])).
% cnf(11904,negated_conjecture,(leaf(esk16_1(esk17_0),X1)|~min_precedes(esk16_1(esk17_0),X2,X1)|~occurrence_of(esk13_3(X1,esk16_1(esk17_0),X2),tptp0)),inference(spm,[status(thm)],[1731,176,theory(equality)])).
% cnf(12003,negated_conjecture,(~min_precedes(esk16_1(esk17_0),X2,X1)|~occurrence_of(esk13_3(X1,esk16_1(esk17_0),X2),tptp0)),inference(csr,[status(thm)],[11904,85])).
% cnf(12004,negated_conjecture,(~min_precedes(esk16_1(esk17_0),X1,tptp0)),inference(spm,[status(thm)],[12003,177,theory(equality)])).
% cnf(16121,negated_conjecture,(X1=esk16_1(esk17_0)|min_precedes(esk16_1(esk17_0),X1,X2)|min_precedes(X1,esk16_1(esk17_0),X2)|occurrence_of(esk16_1(esk17_0),tptp1)|~subactivity_occurrence(X1,esk17_0)|~arboreal(X1)|~occurrence_of(esk17_0,X2)),inference(spm,[status(thm)],[1910,197,theory(equality)])).
% cnf(20721,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|min_precedes(esk14_1(esk17_0),esk16_1(esk17_0),X1)|min_precedes(esk16_1(esk17_0),esk14_1(esk17_0),X1)|occurrence_of(esk16_1(esk17_0),tptp1)|~arboreal(esk14_1(esk17_0))|~occurrence_of(esk17_0,X1)|~occurrence_of(esk17_0,tptp0)),inference(spm,[status(thm)],[16121,210,theory(equality)])).
% cnf(20796,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|min_precedes(esk14_1(esk17_0),esk16_1(esk17_0),X1)|min_precedes(esk16_1(esk17_0),esk14_1(esk17_0),X1)|occurrence_of(esk16_1(esk17_0),tptp1)|~arboreal(esk14_1(esk17_0))|~occurrence_of(esk17_0,X1)|$false),inference(rw,[status(thm)],[20721,197,theory(equality)])).
% cnf(20797,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|min_precedes(esk14_1(esk17_0),esk16_1(esk17_0),X1)|min_precedes(esk16_1(esk17_0),esk14_1(esk17_0),X1)|occurrence_of(esk16_1(esk17_0),tptp1)|~arboreal(esk14_1(esk17_0))|~occurrence_of(esk17_0,X1)),inference(cn,[status(thm)],[20796,theory(equality)])).
% cnf(21267,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|min_precedes(esk16_1(esk17_0),esk14_1(esk17_0),tptp0)|occurrence_of(esk16_1(esk17_0),tptp1)|~root_occ(esk14_1(esk17_0),esk17_0)|~leaf_occ(esk16_1(esk17_0),esk17_0)|~occurrence_of(esk14_1(esk17_0),tptp3)|~occurrence_of(esk16_1(esk17_0),tptp2)|~arboreal(esk14_1(esk17_0))|~occurrence_of(esk17_0,tptp0)),inference(spm,[status(thm)],[199,20797,theory(equality)])).
% cnf(21277,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|min_precedes(esk16_1(esk17_0),esk14_1(esk17_0),tptp0)|occurrence_of(esk16_1(esk17_0),tptp1)|~root_occ(esk14_1(esk17_0),esk17_0)|~leaf_occ(esk16_1(esk17_0),esk17_0)|~occurrence_of(esk14_1(esk17_0),tptp3)|~occurrence_of(esk16_1(esk17_0),tptp2)|~arboreal(esk14_1(esk17_0))|$false),inference(rw,[status(thm)],[21267,197,theory(equality)])).
% cnf(21278,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|min_precedes(esk16_1(esk17_0),esk14_1(esk17_0),tptp0)|occurrence_of(esk16_1(esk17_0),tptp1)|~root_occ(esk14_1(esk17_0),esk17_0)|~leaf_occ(esk16_1(esk17_0),esk17_0)|~occurrence_of(esk14_1(esk17_0),tptp3)|~occurrence_of(esk16_1(esk17_0),tptp2)|~arboreal(esk14_1(esk17_0))),inference(cn,[status(thm)],[21277,theory(equality)])).
% cnf(21279,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|occurrence_of(esk16_1(esk17_0),tptp1)|~root_occ(esk14_1(esk17_0),esk17_0)|~leaf_occ(esk16_1(esk17_0),esk17_0)|~occurrence_of(esk14_1(esk17_0),tptp3)|~occurrence_of(esk16_1(esk17_0),tptp2)|~arboreal(esk14_1(esk17_0))),inference(sr,[status(thm)],[21278,12004,theory(equality)])).
% cnf(21408,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|occurrence_of(esk16_1(esk17_0),tptp1)|~root_occ(esk14_1(esk17_0),esk17_0)|~leaf_occ(esk16_1(esk17_0),esk17_0)|~occurrence_of(esk14_1(esk17_0),tptp3)|~occurrence_of(esk16_1(esk17_0),tptp2)|~occurrence_of(esk17_0,tptp0)),inference(spm,[status(thm)],[21279,238,theory(equality)])).
% cnf(21409,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|occurrence_of(esk16_1(esk17_0),tptp1)|~root_occ(esk14_1(esk17_0),esk17_0)|~leaf_occ(esk16_1(esk17_0),esk17_0)|~occurrence_of(esk14_1(esk17_0),tptp3)|~occurrence_of(esk16_1(esk17_0),tptp2)|$false),inference(rw,[status(thm)],[21408,197,theory(equality)])).
% cnf(21410,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|occurrence_of(esk16_1(esk17_0),tptp1)|~root_occ(esk14_1(esk17_0),esk17_0)|~leaf_occ(esk16_1(esk17_0),esk17_0)|~occurrence_of(esk14_1(esk17_0),tptp3)|~occurrence_of(esk16_1(esk17_0),tptp2)),inference(cn,[status(thm)],[21409,theory(equality)])).
% cnf(21411,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|occurrence_of(esk16_1(esk17_0),tptp1)|~leaf_occ(esk16_1(esk17_0),esk17_0)|~occurrence_of(esk14_1(esk17_0),tptp3)|~occurrence_of(esk16_1(esk17_0),tptp2)|~occurrence_of(esk17_0,tptp0)),inference(spm,[status(thm)],[21410,190,theory(equality)])).
% cnf(21413,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|occurrence_of(esk16_1(esk17_0),tptp1)|~leaf_occ(esk16_1(esk17_0),esk17_0)|~occurrence_of(esk14_1(esk17_0),tptp3)|~occurrence_of(esk16_1(esk17_0),tptp2)|$false),inference(rw,[status(thm)],[21411,197,theory(equality)])).
% cnf(21414,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|occurrence_of(esk16_1(esk17_0),tptp1)|~leaf_occ(esk16_1(esk17_0),esk17_0)|~occurrence_of(esk14_1(esk17_0),tptp3)|~occurrence_of(esk16_1(esk17_0),tptp2)),inference(cn,[status(thm)],[21413,theory(equality)])).
% cnf(21494,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|occurrence_of(esk16_1(esk17_0),tptp1)|~occurrence_of(esk14_1(esk17_0),tptp3)|~occurrence_of(esk16_1(esk17_0),tptp2)|~occurrence_of(esk17_0,tptp0)),inference(spm,[status(thm)],[21414,185,theory(equality)])).
% cnf(21496,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|occurrence_of(esk16_1(esk17_0),tptp1)|~occurrence_of(esk14_1(esk17_0),tptp3)|~occurrence_of(esk16_1(esk17_0),tptp2)|$false),inference(rw,[status(thm)],[21494,197,theory(equality)])).
% cnf(21497,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|occurrence_of(esk16_1(esk17_0),tptp1)|~occurrence_of(esk14_1(esk17_0),tptp3)|~occurrence_of(esk16_1(esk17_0),tptp2)),inference(cn,[status(thm)],[21496,theory(equality)])).
% cnf(21500,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|occurrence_of(esk16_1(esk17_0),tptp1)|~occurrence_of(esk16_1(esk17_0),tptp2)|~occurrence_of(esk17_0,tptp0)),inference(spm,[status(thm)],[21497,191,theory(equality)])).
% cnf(21501,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|occurrence_of(esk16_1(esk17_0),tptp1)|~occurrence_of(esk16_1(esk17_0),tptp2)|$false),inference(rw,[status(thm)],[21500,197,theory(equality)])).
% cnf(21502,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|occurrence_of(esk16_1(esk17_0),tptp1)|~occurrence_of(esk16_1(esk17_0),tptp2)),inference(cn,[status(thm)],[21501,theory(equality)])).
% cnf(21503,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|occurrence_of(esk16_1(esk17_0),tptp1)|~occurrence_of(esk17_0,tptp0)),inference(spm,[status(thm)],[21502,187,theory(equality)])).
% cnf(21504,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|occurrence_of(esk16_1(esk17_0),tptp1)|$false),inference(rw,[status(thm)],[21503,197,theory(equality)])).
% cnf(21505,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|occurrence_of(esk16_1(esk17_0),tptp1)),inference(cn,[status(thm)],[21504,theory(equality)])).
% cnf(21507,negated_conjecture,(arboreal(esk16_1(esk17_0))|esk14_1(esk17_0)=esk16_1(esk17_0)|~atomic(tptp1)),inference(spm,[status(thm)],[63,21505,theory(equality)])).
% cnf(21518,negated_conjecture,(arboreal(esk16_1(esk17_0))|esk14_1(esk17_0)=esk16_1(esk17_0)|$false),inference(rw,[status(thm)],[21507,165,theory(equality)])).
% cnf(21519,negated_conjecture,(arboreal(esk16_1(esk17_0))|esk14_1(esk17_0)=esk16_1(esk17_0)),inference(cn,[status(thm)],[21518,theory(equality)])).
% cnf(31466,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|~root_occ(esk14_1(esk17_0),esk17_0)|~leaf_occ(esk16_1(esk17_0),esk17_0)|~occurrence_of(esk14_1(esk17_0),tptp3)|~occurrence_of(esk16_1(esk17_0),tptp1)|~arboreal(esk16_1(esk17_0))),inference(sr,[status(thm)],[7733,12004,theory(equality)])).
% cnf(31467,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|~root_occ(esk14_1(esk17_0),esk17_0)|~leaf_occ(esk16_1(esk17_0),esk17_0)|~occurrence_of(esk14_1(esk17_0),tptp3)|~occurrence_of(esk16_1(esk17_0),tptp1)),inference(csr,[status(thm)],[31466,21519])).
% cnf(31468,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|~root_occ(esk14_1(esk17_0),esk17_0)|~leaf_occ(esk16_1(esk17_0),esk17_0)|~occurrence_of(esk14_1(esk17_0),tptp3)),inference(csr,[status(thm)],[31467,21505])).
% cnf(31469,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|~leaf_occ(esk16_1(esk17_0),esk17_0)|~occurrence_of(esk14_1(esk17_0),tptp3)|~occurrence_of(esk17_0,tptp0)),inference(spm,[status(thm)],[31468,190,theory(equality)])).
% cnf(31471,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|~leaf_occ(esk16_1(esk17_0),esk17_0)|~occurrence_of(esk14_1(esk17_0),tptp3)|$false),inference(rw,[status(thm)],[31469,197,theory(equality)])).
% cnf(31472,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|~leaf_occ(esk16_1(esk17_0),esk17_0)|~occurrence_of(esk14_1(esk17_0),tptp3)),inference(cn,[status(thm)],[31471,theory(equality)])).
% cnf(31475,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|~occurrence_of(esk14_1(esk17_0),tptp3)|~occurrence_of(esk17_0,tptp0)),inference(spm,[status(thm)],[31472,185,theory(equality)])).
% cnf(31477,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|~occurrence_of(esk14_1(esk17_0),tptp3)|$false),inference(rw,[status(thm)],[31475,197,theory(equality)])).
% cnf(31478,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|~occurrence_of(esk14_1(esk17_0),tptp3)),inference(cn,[status(thm)],[31477,theory(equality)])).
% cnf(31508,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|~occurrence_of(esk17_0,tptp0)),inference(spm,[status(thm)],[31478,191,theory(equality)])).
% cnf(31509,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)|$false),inference(rw,[status(thm)],[31508,197,theory(equality)])).
% cnf(31510,negated_conjecture,(esk14_1(esk17_0)=esk16_1(esk17_0)),inference(cn,[status(thm)],[31509,theory(equality)])).
% cnf(31517,negated_conjecture,(min_precedes(esk16_1(esk17_0),esk15_1(esk17_0),tptp0)|~occurrence_of(esk17_0,tptp0)),inference(spm,[status(thm)],[250,31510,theory(equality)])).
% cnf(32167,negated_conjecture,(min_precedes(esk16_1(esk17_0),esk15_1(esk17_0),tptp0)|$false),inference(rw,[status(thm)],[31517,197,theory(equality)])).
% cnf(32168,negated_conjecture,(min_precedes(esk16_1(esk17_0),esk15_1(esk17_0),tptp0)),inference(cn,[status(thm)],[32167,theory(equality)])).
% cnf(32169,negated_conjecture,($false),inference(sr,[status(thm)],[32168,12004,theory(equality)])).
% cnf(32170,negated_conjecture,($false),32169,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 5744
% # ...of these trivial : 1
% # ...subsumed : 3986
% # ...remaining for further processing: 1757
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 182
% # Backward-rewritten : 352
% # Generated clauses : 20787
% # ...of the previous two non-trivial : 20038
% # Contextual simplify-reflections : 4879
% # Paramodulations : 20787
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 1154
% # Positive orientable unit clauses: 13
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 12
% # Non-unit-clauses : 1129
% # Current number of unprocessed clauses: 10462
% # ...number of literals in the above : 85181
% # Clause-clause subsumption calls (NU) : 213884
% # Rec. Clause-clause subsumption calls : 56851
% # Unit Clause-clause subsumption calls : 246
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 6
% # Indexed BW rewrite successes : 6
% # Backwards rewriting index: 989 leaves, 1.87+/-2.691 terms/leaf
% # Paramod-from index: 259 leaves, 1.24+/-0.799 terms/leaf
% # Paramod-into index: 748 leaves, 1.58+/-1.765 terms/leaf
% # -------------------------------------------------
% # User time : 1.952 s
% # System time : 0.039 s
% # Total time : 1.991 s
% # Maximum resident set size: 0 pages
% PrfWatch: 2.62 CPU 2.69 WC
% FINAL PrfWatch: 2.62 CPU 2.69 WC
% SZS output end Solution for /tmp/SystemOnTPTP5474/PRO009+1.tptp
%
%------------------------------------------------------------------------------