%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : PRO004+4 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art06.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:00:17 EST 2010
% Result : Theorem 5.62s
% Output : Solution 5.62s
% 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/SystemOnTPTP24196/PRO004+4.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP24196/PRO004+4.tptp
% SZS output start Solution for /tmp/SystemOnTPTP24196/PRO004+4.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 24292
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% PrfWatch: 1.92 CPU 2.01 WC
% # Preprocessing time : 0.019 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 3.91 CPU 4.01 WC
% # SZS output start CNFRefutation.
% fof(1, axiom,~(atomic(tptp0)),file('/tmp/SRASS.s.p', sos_34)).
% fof(3, axiom,![X1]:![X2]:![X3]:((occurrence_of(X1,X2)&occurrence_of(X1,X3))=>X2=X3),file('/tmp/SRASS.s.p', sos_08)).
% fof(4, axiom,![X4]:![X5]:![X6]:![X7]:(((occurrence_of(X6,X7)&root_occ(X4,X6))&root_occ(X5,X6))=>X4=X5),file('/tmp/SRASS.s.p', sos_29)).
% fof(5, axiom,![X8]:![X9]:((((occurrence_of(X9,tptp0)&subactivity_occurrence(X8,X9))&arboreal(X8))&~(leaf_occ(X8,X9)))=>root_occ(X8,X9)),file('/tmp/SRASS.s.p', sos_45)).
% fof(7, axiom,![X12]:![X13]:![X14]:(min_precedes(X13,X14,X12)=>?[X15]:((occurrence_of(X15,X12)&subactivity_occurrence(X13,X15))&subactivity_occurrence(X14,X15))),file('/tmp/SRASS.s.p', sos_06)).
% fof(11, axiom,![X28]:![X29]:(occurrence_of(X28,X29)=>(arboreal(X28)<=>atomic(X29))),file('/tmp/SRASS.s.p', sos_16)).
% fof(14, axiom,![X35]:(occurrence_of(X35,tptp0)=>?[X36]:?[X37]:((((occurrence_of(X36,tptp4)&root_occ(X36,X35))&occurrence_of(X37,tptp3))&leaf_occ(X37,X35))&next_subocc(X36,X37,tptp0))),file('/tmp/SRASS.s.p', sos_32)).
% fof(15, axiom,![X38]:![X39]:((((occurrence_of(X39,tptp0)&subactivity_occurrence(X38,X39))&arboreal(X38))&~(leaf_occ(X38,X39)))=>?[X40]:(occurrence_of(X40,tptp1)&next_subocc(X38,X40,tptp0))),file('/tmp/SRASS.s.p', sos_47)).
% fof(18, axiom,![X45]:![X46]:((leaf(X45,X46)&~(atomic(X46)))=>?[X47]:(occurrence_of(X47,X46)&leaf_occ(X45,X47))),file('/tmp/SRASS.s.p', sos_07)).
% fof(22, axiom,atomic(tptp1),file('/tmp/SRASS.s.p', sos_38)).
% fof(24, axiom,![X50]:![X51]:![X52]:![X53]:((((occurrence_of(X52,X53)&~(atomic(X53)))&leaf_occ(X50,X52))&leaf_occ(X51,X52))=>X50=X51),file('/tmp/SRASS.s.p', sos_28)).
% fof(25, axiom,![X54]:![X55]:(occurrence_of(X55,X54)=>(activity(X54)&activity_occurrence(X55))),file('/tmp/SRASS.s.p', sos_03)).
% fof(26, axiom,![X56]:(activity_occurrence(X56)=>?[X57]:(activity(X57)&occurrence_of(X56,X57))),file('/tmp/SRASS.s.p', sos_12)).
% fof(28, axiom,![X62]:![X63]:(root(X63,X62)=>?[X64]:(subactivity(X64,X62)&atocc(X63,X64))),file('/tmp/SRASS.s.p', sos_05)).
% fof(30, axiom,![X70]:![X71]:![X72]:![X73]:(((((occurrence_of(X71,X70)&subactivity_occurrence(X72,X71))&leaf_occ(X73,X71))&arboreal(X72))&~(min_precedes(X72,X73,X70)))=>X73=X72),file('/tmp/SRASS.s.p', sos_02)).
% fof(31, axiom,![X74]:![X75]:(root_occ(X74,X75)<=>?[X76]:((occurrence_of(X75,X76)&subactivity_occurrence(X74,X75))&root(X74,X76))),file('/tmp/SRASS.s.p', sos_19)).
% fof(32, axiom,![X77]:![X78]:((occurrence_of(X78,X77)&~(atomic(X77)))=>?[X79]:(root(X79,X77)&subactivity_occurrence(X79,X78))),file('/tmp/SRASS.s.p', sos)).
% fof(33, axiom,![X80]:![X81]:(leaf_occ(X80,X81)<=>?[X82]:((occurrence_of(X81,X82)&subactivity_occurrence(X80,X81))&leaf(X80,X82))),file('/tmp/SRASS.s.p', sos_18)).
% fof(34, axiom,![X83]:![X84]:![X85]:(min_precedes(X83,X84,X85)=>~(root(X84,X85))),file('/tmp/SRASS.s.p', sos_22)).
% fof(37, axiom,![X93]:![X94]:![X95]:(next_subocc(X93,X94,X95)<=>(min_precedes(X93,X94,X95)&~(?[X96]:(min_precedes(X93,X96,X95)&min_precedes(X96,X94,X95))))),file('/tmp/SRASS.s.p', sos_26)).
% fof(42, axiom,~(tptp1=tptp3),file('/tmp/SRASS.s.p', sos_42)).
% fof(45, axiom,![X101]:![X102]:(atocc(X101,X102)<=>?[X103]:((subactivity(X102,X103)&atomic(X103))&occurrence_of(X101,X103))),file('/tmp/SRASS.s.p', sos_14)).
% fof(46, axiom,![X104]:![X105]:(leaf(X104,X105)<=>((root(X104,X105)|?[X106]:min_precedes(X106,X104,X105))&~(?[X107]:min_precedes(X104,X107,X105)))),file('/tmp/SRASS.s.p', sos_15)).
% fof(49, conjecture,~(?[X112]:occurrence_of(X112,tptp0)),file('/tmp/SRASS.s.p', goals)).
% fof(50, negated_conjecture,~(~(?[X112]:occurrence_of(X112,tptp0))),inference(assume_negation,[status(cth)],[49])).
% fof(51, plain,~(atomic(tptp0)),inference(fof_simplification,[status(thm)],[1,theory(equality)])).
% fof(52, plain,![X8]:![X9]:((((occurrence_of(X9,tptp0)&subactivity_occurrence(X8,X9))&arboreal(X8))&~(leaf_occ(X8,X9)))=>root_occ(X8,X9)),inference(fof_simplification,[status(thm)],[5,theory(equality)])).
% fof(55, plain,![X38]:![X39]:((((occurrence_of(X39,tptp0)&subactivity_occurrence(X38,X39))&arboreal(X38))&~(leaf_occ(X38,X39)))=>?[X40]:(occurrence_of(X40,tptp1)&next_subocc(X38,X40,tptp0))),inference(fof_simplification,[status(thm)],[15,theory(equality)])).
% fof(56, plain,![X45]:![X46]:((leaf(X45,X46)&~(atomic(X46)))=>?[X47]:(occurrence_of(X47,X46)&leaf_occ(X45,X47))),inference(fof_simplification,[status(thm)],[18,theory(equality)])).
% fof(57, plain,![X50]:![X51]:![X52]:![X53]:((((occurrence_of(X52,X53)&~(atomic(X53)))&leaf_occ(X50,X52))&leaf_occ(X51,X52))=>X50=X51),inference(fof_simplification,[status(thm)],[24,theory(equality)])).
% fof(58, plain,![X70]:![X71]:![X72]:![X73]:(((((occurrence_of(X71,X70)&subactivity_occurrence(X72,X71))&leaf_occ(X73,X71))&arboreal(X72))&~(min_precedes(X72,X73,X70)))=>X73=X72),inference(fof_simplification,[status(thm)],[30,theory(equality)])).
% fof(59, plain,![X77]:![X78]:((occurrence_of(X78,X77)&~(atomic(X77)))=>?[X79]:(root(X79,X77)&subactivity_occurrence(X79,X78))),inference(fof_simplification,[status(thm)],[32,theory(equality)])).
% fof(60, plain,![X83]:![X84]:![X85]:(min_precedes(X83,X84,X85)=>~(root(X84,X85))),inference(fof_simplification,[status(thm)],[34,theory(equality)])).
% cnf(61,plain,(~atomic(tptp0)),inference(split_conjunct,[status(thm)],[51])).
% fof(63, plain,![X1]:![X2]:![X3]:((~(occurrence_of(X1,X2))|~(occurrence_of(X1,X3)))|X2=X3),inference(fof_nnf,[status(thm)],[3])).
% fof(64, plain,![X4]:![X5]:![X6]:((~(occurrence_of(X4,X5))|~(occurrence_of(X4,X6)))|X5=X6),inference(variable_rename,[status(thm)],[63])).
% cnf(65,plain,(X1=X2|~occurrence_of(X3,X2)|~occurrence_of(X3,X1)),inference(split_conjunct,[status(thm)],[64])).
% fof(66, plain,![X4]:![X5]:![X6]:![X7]:(((~(occurrence_of(X6,X7))|~(root_occ(X4,X6)))|~(root_occ(X5,X6)))|X4=X5),inference(fof_nnf,[status(thm)],[4])).
% fof(67, plain,![X8]:![X9]:![X10]:![X11]:(((~(occurrence_of(X10,X11))|~(root_occ(X8,X10)))|~(root_occ(X9,X10)))|X8=X9),inference(variable_rename,[status(thm)],[66])).
% cnf(68,plain,(X1=X2|~root_occ(X2,X3)|~root_occ(X1,X3)|~occurrence_of(X3,X4)),inference(split_conjunct,[status(thm)],[67])).
% fof(69, plain,![X8]:![X9]:((((~(occurrence_of(X9,tptp0))|~(subactivity_occurrence(X8,X9)))|~(arboreal(X8)))|leaf_occ(X8,X9))|root_occ(X8,X9)),inference(fof_nnf,[status(thm)],[52])).
% fof(70, plain,![X10]:![X11]:((((~(occurrence_of(X11,tptp0))|~(subactivity_occurrence(X10,X11)))|~(arboreal(X10)))|leaf_occ(X10,X11))|root_occ(X10,X11)),inference(variable_rename,[status(thm)],[69])).
% cnf(71,plain,(root_occ(X1,X2)|leaf_occ(X1,X2)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(split_conjunct,[status(thm)],[70])).
% fof(75, plain,![X12]:![X13]:![X14]:(~(min_precedes(X13,X14,X12))|?[X15]:((occurrence_of(X15,X12)&subactivity_occurrence(X13,X15))&subactivity_occurrence(X14,X15))),inference(fof_nnf,[status(thm)],[7])).
% fof(76, plain,![X16]:![X17]:![X18]:(~(min_precedes(X17,X18,X16))|?[X19]:((occurrence_of(X19,X16)&subactivity_occurrence(X17,X19))&subactivity_occurrence(X18,X19))),inference(variable_rename,[status(thm)],[75])).
% fof(77, plain,![X16]:![X17]:![X18]:(~(min_precedes(X17,X18,X16))|((occurrence_of(esk1_3(X16,X17,X18),X16)&subactivity_occurrence(X17,esk1_3(X16,X17,X18)))&subactivity_occurrence(X18,esk1_3(X16,X17,X18)))),inference(skolemize,[status(esa)],[76])).
% fof(78, plain,![X16]:![X17]:![X18]:(((occurrence_of(esk1_3(X16,X17,X18),X16)|~(min_precedes(X17,X18,X16)))&(subactivity_occurrence(X17,esk1_3(X16,X17,X18))|~(min_precedes(X17,X18,X16))))&(subactivity_occurrence(X18,esk1_3(X16,X17,X18))|~(min_precedes(X17,X18,X16)))),inference(distribute,[status(thm)],[77])).
% cnf(79,plain,(subactivity_occurrence(X2,esk1_3(X3,X1,X2))|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[78])).
% cnf(80,plain,(subactivity_occurrence(X1,esk1_3(X3,X1,X2))|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[78])).
% cnf(81,plain,(occurrence_of(esk1_3(X3,X1,X2),X3)|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[78])).
% fof(93, plain,![X28]:![X29]:(~(occurrence_of(X28,X29))|((~(arboreal(X28))|atomic(X29))&(~(atomic(X29))|arboreal(X28)))),inference(fof_nnf,[status(thm)],[11])).
% fof(94, plain,![X30]:![X31]:(~(occurrence_of(X30,X31))|((~(arboreal(X30))|atomic(X31))&(~(atomic(X31))|arboreal(X30)))),inference(variable_rename,[status(thm)],[93])).
% fof(95, plain,![X30]:![X31]:(((~(arboreal(X30))|atomic(X31))|~(occurrence_of(X30,X31)))&((~(atomic(X31))|arboreal(X30))|~(occurrence_of(X30,X31)))),inference(distribute,[status(thm)],[94])).
% cnf(96,plain,(arboreal(X1)|~occurrence_of(X1,X2)|~atomic(X2)),inference(split_conjunct,[status(thm)],[95])).
% fof(104, plain,![X35]:(~(occurrence_of(X35,tptp0))|?[X36]:?[X37]:((((occurrence_of(X36,tptp4)&root_occ(X36,X35))&occurrence_of(X37,tptp3))&leaf_occ(X37,X35))&next_subocc(X36,X37,tptp0))),inference(fof_nnf,[status(thm)],[14])).
% fof(105, plain,![X38]:(~(occurrence_of(X38,tptp0))|?[X39]:?[X40]:((((occurrence_of(X39,tptp4)&root_occ(X39,X38))&occurrence_of(X40,tptp3))&leaf_occ(X40,X38))&next_subocc(X39,X40,tptp0))),inference(variable_rename,[status(thm)],[104])).
% fof(106, plain,![X38]:(~(occurrence_of(X38,tptp0))|((((occurrence_of(esk2_1(X38),tptp4)&root_occ(esk2_1(X38),X38))&occurrence_of(esk3_1(X38),tptp3))&leaf_occ(esk3_1(X38),X38))&next_subocc(esk2_1(X38),esk3_1(X38),tptp0))),inference(skolemize,[status(esa)],[105])).
% fof(107, plain,![X38]:(((((occurrence_of(esk2_1(X38),tptp4)|~(occurrence_of(X38,tptp0)))&(root_occ(esk2_1(X38),X38)|~(occurrence_of(X38,tptp0))))&(occurrence_of(esk3_1(X38),tptp3)|~(occurrence_of(X38,tptp0))))&(leaf_occ(esk3_1(X38),X38)|~(occurrence_of(X38,tptp0))))&(next_subocc(esk2_1(X38),esk3_1(X38),tptp0)|~(occurrence_of(X38,tptp0)))),inference(distribute,[status(thm)],[106])).
% cnf(108,plain,(next_subocc(esk2_1(X1),esk3_1(X1),tptp0)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[107])).
% cnf(109,plain,(leaf_occ(esk3_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[107])).
% cnf(110,plain,(occurrence_of(esk3_1(X1),tptp3)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[107])).
% cnf(111,plain,(root_occ(esk2_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[107])).
% cnf(112,plain,(occurrence_of(esk2_1(X1),tptp4)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[107])).
% fof(113, plain,![X38]:![X39]:((((~(occurrence_of(X39,tptp0))|~(subactivity_occurrence(X38,X39)))|~(arboreal(X38)))|leaf_occ(X38,X39))|?[X40]:(occurrence_of(X40,tptp1)&next_subocc(X38,X40,tptp0))),inference(fof_nnf,[status(thm)],[55])).
% fof(114, plain,![X41]:![X42]:((((~(occurrence_of(X42,tptp0))|~(subactivity_occurrence(X41,X42)))|~(arboreal(X41)))|leaf_occ(X41,X42))|?[X43]:(occurrence_of(X43,tptp1)&next_subocc(X41,X43,tptp0))),inference(variable_rename,[status(thm)],[113])).
% fof(115, plain,![X41]:![X42]:((((~(occurrence_of(X42,tptp0))|~(subactivity_occurrence(X41,X42)))|~(arboreal(X41)))|leaf_occ(X41,X42))|(occurrence_of(esk4_2(X41,X42),tptp1)&next_subocc(X41,esk4_2(X41,X42),tptp0))),inference(skolemize,[status(esa)],[114])).
% fof(116, plain,![X41]:![X42]:((occurrence_of(esk4_2(X41,X42),tptp1)|(((~(occurrence_of(X42,tptp0))|~(subactivity_occurrence(X41,X42)))|~(arboreal(X41)))|leaf_occ(X41,X42)))&(next_subocc(X41,esk4_2(X41,X42),tptp0)|(((~(occurrence_of(X42,tptp0))|~(subactivity_occurrence(X41,X42)))|~(arboreal(X41)))|leaf_occ(X41,X42)))),inference(distribute,[status(thm)],[115])).
% cnf(117,plain,(leaf_occ(X1,X2)|next_subocc(X1,esk4_2(X1,X2),tptp0)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(split_conjunct,[status(thm)],[116])).
% cnf(118,plain,(leaf_occ(X1,X2)|occurrence_of(esk4_2(X1,X2),tptp1)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(split_conjunct,[status(thm)],[116])).
% fof(127, plain,![X45]:![X46]:((~(leaf(X45,X46))|atomic(X46))|?[X47]:(occurrence_of(X47,X46)&leaf_occ(X45,X47))),inference(fof_nnf,[status(thm)],[56])).
% fof(128, plain,![X48]:![X49]:((~(leaf(X48,X49))|atomic(X49))|?[X50]:(occurrence_of(X50,X49)&leaf_occ(X48,X50))),inference(variable_rename,[status(thm)],[127])).
% fof(129, plain,![X48]:![X49]:((~(leaf(X48,X49))|atomic(X49))|(occurrence_of(esk5_2(X48,X49),X49)&leaf_occ(X48,esk5_2(X48,X49)))),inference(skolemize,[status(esa)],[128])).
% fof(130, plain,![X48]:![X49]:((occurrence_of(esk5_2(X48,X49),X49)|(~(leaf(X48,X49))|atomic(X49)))&(leaf_occ(X48,esk5_2(X48,X49))|(~(leaf(X48,X49))|atomic(X49)))),inference(distribute,[status(thm)],[129])).
% cnf(131,plain,(atomic(X1)|leaf_occ(X2,esk5_2(X2,X1))|~leaf(X2,X1)),inference(split_conjunct,[status(thm)],[130])).
% cnf(132,plain,(atomic(X1)|occurrence_of(esk5_2(X2,X1),X1)|~leaf(X2,X1)),inference(split_conjunct,[status(thm)],[130])).
% cnf(136,plain,(atomic(tptp1)),inference(split_conjunct,[status(thm)],[22])).
% fof(142, plain,![X50]:![X51]:![X52]:![X53]:((((~(occurrence_of(X52,X53))|atomic(X53))|~(leaf_occ(X50,X52)))|~(leaf_occ(X51,X52)))|X50=X51),inference(fof_nnf,[status(thm)],[57])).
% fof(143, plain,![X54]:![X55]:![X56]:![X57]:((((~(occurrence_of(X56,X57))|atomic(X57))|~(leaf_occ(X54,X56)))|~(leaf_occ(X55,X56)))|X54=X55),inference(variable_rename,[status(thm)],[142])).
% cnf(144,plain,(X1=X2|atomic(X4)|~leaf_occ(X2,X3)|~leaf_occ(X1,X3)|~occurrence_of(X3,X4)),inference(split_conjunct,[status(thm)],[143])).
% fof(145, plain,![X54]:![X55]:(~(occurrence_of(X55,X54))|(activity(X54)&activity_occurrence(X55))),inference(fof_nnf,[status(thm)],[25])).
% fof(146, plain,![X56]:![X57]:(~(occurrence_of(X57,X56))|(activity(X56)&activity_occurrence(X57))),inference(variable_rename,[status(thm)],[145])).
% fof(147, plain,![X56]:![X57]:((activity(X56)|~(occurrence_of(X57,X56)))&(activity_occurrence(X57)|~(occurrence_of(X57,X56)))),inference(distribute,[status(thm)],[146])).
% cnf(148,plain,(activity_occurrence(X1)|~occurrence_of(X1,X2)),inference(split_conjunct,[status(thm)],[147])).
% fof(150, plain,![X56]:(~(activity_occurrence(X56))|?[X57]:(activity(X57)&occurrence_of(X56,X57))),inference(fof_nnf,[status(thm)],[26])).
% fof(151, plain,![X58]:(~(activity_occurrence(X58))|?[X59]:(activity(X59)&occurrence_of(X58,X59))),inference(variable_rename,[status(thm)],[150])).
% fof(152, plain,![X58]:(~(activity_occurrence(X58))|(activity(esk6_1(X58))&occurrence_of(X58,esk6_1(X58)))),inference(skolemize,[status(esa)],[151])).
% fof(153, plain,![X58]:((activity(esk6_1(X58))|~(activity_occurrence(X58)))&(occurrence_of(X58,esk6_1(X58))|~(activity_occurrence(X58)))),inference(distribute,[status(thm)],[152])).
% cnf(154,plain,(occurrence_of(X1,esk6_1(X1))|~activity_occurrence(X1)),inference(split_conjunct,[status(thm)],[153])).
% fof(159, plain,![X62]:![X63]:(~(root(X63,X62))|?[X64]:(subactivity(X64,X62)&atocc(X63,X64))),inference(fof_nnf,[status(thm)],[28])).
% fof(160, plain,![X65]:![X66]:(~(root(X66,X65))|?[X67]:(subactivity(X67,X65)&atocc(X66,X67))),inference(variable_rename,[status(thm)],[159])).
% fof(161, plain,![X65]:![X66]:(~(root(X66,X65))|(subactivity(esk7_2(X65,X66),X65)&atocc(X66,esk7_2(X65,X66)))),inference(skolemize,[status(esa)],[160])).
% fof(162, plain,![X65]:![X66]:((subactivity(esk7_2(X65,X66),X65)|~(root(X66,X65)))&(atocc(X66,esk7_2(X65,X66))|~(root(X66,X65)))),inference(distribute,[status(thm)],[161])).
% cnf(163,plain,(atocc(X1,esk7_2(X2,X1))|~root(X1,X2)),inference(split_conjunct,[status(thm)],[162])).
% fof(168, plain,![X70]:![X71]:![X72]:![X73]:(((((~(occurrence_of(X71,X70))|~(subactivity_occurrence(X72,X71)))|~(leaf_occ(X73,X71)))|~(arboreal(X72)))|min_precedes(X72,X73,X70))|X73=X72),inference(fof_nnf,[status(thm)],[58])).
% fof(169, plain,![X74]:![X75]:![X76]:![X77]:(((((~(occurrence_of(X75,X74))|~(subactivity_occurrence(X76,X75)))|~(leaf_occ(X77,X75)))|~(arboreal(X76)))|min_precedes(X76,X77,X74))|X77=X76),inference(variable_rename,[status(thm)],[168])).
% cnf(170,plain,(X1=X2|min_precedes(X2,X1,X3)|~arboreal(X2)|~leaf_occ(X1,X4)|~subactivity_occurrence(X2,X4)|~occurrence_of(X4,X3)),inference(split_conjunct,[status(thm)],[169])).
% fof(171, plain,![X74]:![X75]:((~(root_occ(X74,X75))|?[X76]:((occurrence_of(X75,X76)&subactivity_occurrence(X74,X75))&root(X74,X76)))&(![X76]:((~(occurrence_of(X75,X76))|~(subactivity_occurrence(X74,X75)))|~(root(X74,X76)))|root_occ(X74,X75))),inference(fof_nnf,[status(thm)],[31])).
% fof(172, plain,![X77]:![X78]:((~(root_occ(X77,X78))|?[X79]:((occurrence_of(X78,X79)&subactivity_occurrence(X77,X78))&root(X77,X79)))&(![X80]:((~(occurrence_of(X78,X80))|~(subactivity_occurrence(X77,X78)))|~(root(X77,X80)))|root_occ(X77,X78))),inference(variable_rename,[status(thm)],[171])).
% fof(173, plain,![X77]:![X78]:((~(root_occ(X77,X78))|((occurrence_of(X78,esk8_2(X77,X78))&subactivity_occurrence(X77,X78))&root(X77,esk8_2(X77,X78))))&(![X80]:((~(occurrence_of(X78,X80))|~(subactivity_occurrence(X77,X78)))|~(root(X77,X80)))|root_occ(X77,X78))),inference(skolemize,[status(esa)],[172])).
% fof(174, plain,![X77]:![X78]:![X80]:((((~(occurrence_of(X78,X80))|~(subactivity_occurrence(X77,X78)))|~(root(X77,X80)))|root_occ(X77,X78))&(~(root_occ(X77,X78))|((occurrence_of(X78,esk8_2(X77,X78))&subactivity_occurrence(X77,X78))&root(X77,esk8_2(X77,X78))))),inference(shift_quantors,[status(thm)],[173])).
% fof(175, plain,![X77]:![X78]:![X80]:((((~(occurrence_of(X78,X80))|~(subactivity_occurrence(X77,X78)))|~(root(X77,X80)))|root_occ(X77,X78))&(((occurrence_of(X78,esk8_2(X77,X78))|~(root_occ(X77,X78)))&(subactivity_occurrence(X77,X78)|~(root_occ(X77,X78))))&(root(X77,esk8_2(X77,X78))|~(root_occ(X77,X78))))),inference(distribute,[status(thm)],[174])).
% cnf(176,plain,(root(X1,esk8_2(X1,X2))|~root_occ(X1,X2)),inference(split_conjunct,[status(thm)],[175])).
% cnf(178,plain,(occurrence_of(X2,esk8_2(X1,X2))|~root_occ(X1,X2)),inference(split_conjunct,[status(thm)],[175])).
% cnf(179,plain,(root_occ(X1,X2)|~root(X1,X3)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,X3)),inference(split_conjunct,[status(thm)],[175])).
% fof(180, plain,![X77]:![X78]:((~(occurrence_of(X78,X77))|atomic(X77))|?[X79]:(root(X79,X77)&subactivity_occurrence(X79,X78))),inference(fof_nnf,[status(thm)],[59])).
% fof(181, plain,![X80]:![X81]:((~(occurrence_of(X81,X80))|atomic(X80))|?[X82]:(root(X82,X80)&subactivity_occurrence(X82,X81))),inference(variable_rename,[status(thm)],[180])).
% fof(182, plain,![X80]:![X81]:((~(occurrence_of(X81,X80))|atomic(X80))|(root(esk9_2(X80,X81),X80)&subactivity_occurrence(esk9_2(X80,X81),X81))),inference(skolemize,[status(esa)],[181])).
% fof(183, plain,![X80]:![X81]:((root(esk9_2(X80,X81),X80)|(~(occurrence_of(X81,X80))|atomic(X80)))&(subactivity_occurrence(esk9_2(X80,X81),X81)|(~(occurrence_of(X81,X80))|atomic(X80)))),inference(distribute,[status(thm)],[182])).
% cnf(184,plain,(atomic(X1)|subactivity_occurrence(esk9_2(X1,X2),X2)|~occurrence_of(X2,X1)),inference(split_conjunct,[status(thm)],[183])).
% cnf(185,plain,(atomic(X1)|root(esk9_2(X1,X2),X1)|~occurrence_of(X2,X1)),inference(split_conjunct,[status(thm)],[183])).
% fof(186, plain,![X80]:![X81]:((~(leaf_occ(X80,X81))|?[X82]:((occurrence_of(X81,X82)&subactivity_occurrence(X80,X81))&leaf(X80,X82)))&(![X82]:((~(occurrence_of(X81,X82))|~(subactivity_occurrence(X80,X81)))|~(leaf(X80,X82)))|leaf_occ(X80,X81))),inference(fof_nnf,[status(thm)],[33])).
% fof(187, plain,![X83]:![X84]:((~(leaf_occ(X83,X84))|?[X85]:((occurrence_of(X84,X85)&subactivity_occurrence(X83,X84))&leaf(X83,X85)))&(![X86]:((~(occurrence_of(X84,X86))|~(subactivity_occurrence(X83,X84)))|~(leaf(X83,X86)))|leaf_occ(X83,X84))),inference(variable_rename,[status(thm)],[186])).
% fof(188, plain,![X83]:![X84]:((~(leaf_occ(X83,X84))|((occurrence_of(X84,esk10_2(X83,X84))&subactivity_occurrence(X83,X84))&leaf(X83,esk10_2(X83,X84))))&(![X86]:((~(occurrence_of(X84,X86))|~(subactivity_occurrence(X83,X84)))|~(leaf(X83,X86)))|leaf_occ(X83,X84))),inference(skolemize,[status(esa)],[187])).
% fof(189, plain,![X83]:![X84]:![X86]:((((~(occurrence_of(X84,X86))|~(subactivity_occurrence(X83,X84)))|~(leaf(X83,X86)))|leaf_occ(X83,X84))&(~(leaf_occ(X83,X84))|((occurrence_of(X84,esk10_2(X83,X84))&subactivity_occurrence(X83,X84))&leaf(X83,esk10_2(X83,X84))))),inference(shift_quantors,[status(thm)],[188])).
% fof(190, plain,![X83]:![X84]:![X86]:((((~(occurrence_of(X84,X86))|~(subactivity_occurrence(X83,X84)))|~(leaf(X83,X86)))|leaf_occ(X83,X84))&(((occurrence_of(X84,esk10_2(X83,X84))|~(leaf_occ(X83,X84)))&(subactivity_occurrence(X83,X84)|~(leaf_occ(X83,X84))))&(leaf(X83,esk10_2(X83,X84))|~(leaf_occ(X83,X84))))),inference(distribute,[status(thm)],[189])).
% cnf(191,plain,(leaf(X1,esk10_2(X1,X2))|~leaf_occ(X1,X2)),inference(split_conjunct,[status(thm)],[190])).
% cnf(193,plain,(occurrence_of(X2,esk10_2(X1,X2))|~leaf_occ(X1,X2)),inference(split_conjunct,[status(thm)],[190])).
% fof(195, plain,![X83]:![X84]:![X85]:(~(min_precedes(X83,X84,X85))|~(root(X84,X85))),inference(fof_nnf,[status(thm)],[60])).
% fof(196, plain,![X86]:![X87]:![X88]:(~(min_precedes(X86,X87,X88))|~(root(X87,X88))),inference(variable_rename,[status(thm)],[195])).
% cnf(197,plain,(~root(X1,X2)|~min_precedes(X3,X1,X2)),inference(split_conjunct,[status(thm)],[196])).
% fof(207, plain,![X93]:![X94]:![X95]:((~(next_subocc(X93,X94,X95))|(min_precedes(X93,X94,X95)&![X96]:(~(min_precedes(X93,X96,X95))|~(min_precedes(X96,X94,X95)))))&((~(min_precedes(X93,X94,X95))|?[X96]:(min_precedes(X93,X96,X95)&min_precedes(X96,X94,X95)))|next_subocc(X93,X94,X95))),inference(fof_nnf,[status(thm)],[37])).
% fof(208, plain,![X97]:![X98]:![X99]:((~(next_subocc(X97,X98,X99))|(min_precedes(X97,X98,X99)&![X100]:(~(min_precedes(X97,X100,X99))|~(min_precedes(X100,X98,X99)))))&((~(min_precedes(X97,X98,X99))|?[X101]:(min_precedes(X97,X101,X99)&min_precedes(X101,X98,X99)))|next_subocc(X97,X98,X99))),inference(variable_rename,[status(thm)],[207])).
% fof(209, plain,![X97]:![X98]:![X99]:((~(next_subocc(X97,X98,X99))|(min_precedes(X97,X98,X99)&![X100]:(~(min_precedes(X97,X100,X99))|~(min_precedes(X100,X98,X99)))))&((~(min_precedes(X97,X98,X99))|(min_precedes(X97,esk12_3(X97,X98,X99),X99)&min_precedes(esk12_3(X97,X98,X99),X98,X99)))|next_subocc(X97,X98,X99))),inference(skolemize,[status(esa)],[208])).
% fof(210, plain,![X97]:![X98]:![X99]:![X100]:((((~(min_precedes(X97,X100,X99))|~(min_precedes(X100,X98,X99)))&min_precedes(X97,X98,X99))|~(next_subocc(X97,X98,X99)))&((~(min_precedes(X97,X98,X99))|(min_precedes(X97,esk12_3(X97,X98,X99),X99)&min_precedes(esk12_3(X97,X98,X99),X98,X99)))|next_subocc(X97,X98,X99))),inference(shift_quantors,[status(thm)],[209])).
% fof(211, plain,![X97]:![X98]:![X99]:![X100]:((((~(min_precedes(X97,X100,X99))|~(min_precedes(X100,X98,X99)))|~(next_subocc(X97,X98,X99)))&(min_precedes(X97,X98,X99)|~(next_subocc(X97,X98,X99))))&(((min_precedes(X97,esk12_3(X97,X98,X99),X99)|~(min_precedes(X97,X98,X99)))|next_subocc(X97,X98,X99))&((min_precedes(esk12_3(X97,X98,X99),X98,X99)|~(min_precedes(X97,X98,X99)))|next_subocc(X97,X98,X99)))),inference(distribute,[status(thm)],[210])).
% cnf(214,plain,(min_precedes(X1,X2,X3)|~next_subocc(X1,X2,X3)),inference(split_conjunct,[status(thm)],[211])).
% cnf(222,plain,(tptp1!=tptp3),inference(split_conjunct,[status(thm)],[42])).
% fof(225, plain,![X101]:![X102]:((~(atocc(X101,X102))|?[X103]:((subactivity(X102,X103)&atomic(X103))&occurrence_of(X101,X103)))&(![X103]:((~(subactivity(X102,X103))|~(atomic(X103)))|~(occurrence_of(X101,X103)))|atocc(X101,X102))),inference(fof_nnf,[status(thm)],[45])).
% fof(226, plain,![X104]:![X105]:((~(atocc(X104,X105))|?[X106]:((subactivity(X105,X106)&atomic(X106))&occurrence_of(X104,X106)))&(![X107]:((~(subactivity(X105,X107))|~(atomic(X107)))|~(occurrence_of(X104,X107)))|atocc(X104,X105))),inference(variable_rename,[status(thm)],[225])).
% fof(227, plain,![X104]:![X105]:((~(atocc(X104,X105))|((subactivity(X105,esk13_2(X104,X105))&atomic(esk13_2(X104,X105)))&occurrence_of(X104,esk13_2(X104,X105))))&(![X107]:((~(subactivity(X105,X107))|~(atomic(X107)))|~(occurrence_of(X104,X107)))|atocc(X104,X105))),inference(skolemize,[status(esa)],[226])).
% fof(228, plain,![X104]:![X105]:![X107]:((((~(subactivity(X105,X107))|~(atomic(X107)))|~(occurrence_of(X104,X107)))|atocc(X104,X105))&(~(atocc(X104,X105))|((subactivity(X105,esk13_2(X104,X105))&atomic(esk13_2(X104,X105)))&occurrence_of(X104,esk13_2(X104,X105))))),inference(shift_quantors,[status(thm)],[227])).
% fof(229, plain,![X104]:![X105]:![X107]:((((~(subactivity(X105,X107))|~(atomic(X107)))|~(occurrence_of(X104,X107)))|atocc(X104,X105))&(((subactivity(X105,esk13_2(X104,X105))|~(atocc(X104,X105)))&(atomic(esk13_2(X104,X105))|~(atocc(X104,X105))))&(occurrence_of(X104,esk13_2(X104,X105))|~(atocc(X104,X105))))),inference(distribute,[status(thm)],[228])).
% cnf(230,plain,(occurrence_of(X1,esk13_2(X1,X2))|~atocc(X1,X2)),inference(split_conjunct,[status(thm)],[229])).
% cnf(231,plain,(atomic(esk13_2(X1,X2))|~atocc(X1,X2)),inference(split_conjunct,[status(thm)],[229])).
% cnf(232,plain,(subactivity(X2,esk13_2(X1,X2))|~atocc(X1,X2)),inference(split_conjunct,[status(thm)],[229])).
% cnf(233,plain,(atocc(X1,X2)|~occurrence_of(X1,X3)|~atomic(X3)|~subactivity(X2,X3)),inference(split_conjunct,[status(thm)],[229])).
% fof(234, plain,![X104]:![X105]:((~(leaf(X104,X105))|((root(X104,X105)|?[X106]:min_precedes(X106,X104,X105))&![X107]:~(min_precedes(X104,X107,X105))))&(((~(root(X104,X105))&![X106]:~(min_precedes(X106,X104,X105)))|?[X107]:min_precedes(X104,X107,X105))|leaf(X104,X105))),inference(fof_nnf,[status(thm)],[46])).
% fof(235, plain,![X108]:![X109]:((~(leaf(X108,X109))|((root(X108,X109)|?[X110]:min_precedes(X110,X108,X109))&![X111]:~(min_precedes(X108,X111,X109))))&(((~(root(X108,X109))&![X112]:~(min_precedes(X112,X108,X109)))|?[X113]:min_precedes(X108,X113,X109))|leaf(X108,X109))),inference(variable_rename,[status(thm)],[234])).
% fof(236, plain,![X108]:![X109]:((~(leaf(X108,X109))|((root(X108,X109)|min_precedes(esk14_2(X108,X109),X108,X109))&![X111]:~(min_precedes(X108,X111,X109))))&(((~(root(X108,X109))&![X112]:~(min_precedes(X112,X108,X109)))|min_precedes(X108,esk15_2(X108,X109),X109))|leaf(X108,X109))),inference(skolemize,[status(esa)],[235])).
% fof(237, plain,![X108]:![X109]:![X111]:![X112]:((((~(min_precedes(X112,X108,X109))&~(root(X108,X109)))|min_precedes(X108,esk15_2(X108,X109),X109))|leaf(X108,X109))&((~(min_precedes(X108,X111,X109))&(root(X108,X109)|min_precedes(esk14_2(X108,X109),X108,X109)))|~(leaf(X108,X109)))),inference(shift_quantors,[status(thm)],[236])).
% fof(238, plain,![X108]:![X109]:![X111]:![X112]:((((~(min_precedes(X112,X108,X109))|min_precedes(X108,esk15_2(X108,X109),X109))|leaf(X108,X109))&((~(root(X108,X109))|min_precedes(X108,esk15_2(X108,X109),X109))|leaf(X108,X109)))&((~(min_precedes(X108,X111,X109))|~(leaf(X108,X109)))&((root(X108,X109)|min_precedes(esk14_2(X108,X109),X108,X109))|~(leaf(X108,X109))))),inference(distribute,[status(thm)],[237])).
% cnf(240,plain,(~leaf(X1,X2)|~min_precedes(X1,X3,X2)),inference(split_conjunct,[status(thm)],[238])).
% fof(252, negated_conjecture,?[X112]:occurrence_of(X112,tptp0),inference(fof_nnf,[status(thm)],[50])).
% fof(253, negated_conjecture,?[X113]:occurrence_of(X113,tptp0),inference(variable_rename,[status(thm)],[252])).
% fof(254, negated_conjecture,occurrence_of(esk16_0,tptp0),inference(skolemize,[status(esa)],[253])).
% cnf(255,negated_conjecture,(occurrence_of(esk16_0,tptp0)),inference(split_conjunct,[status(thm)],[254])).
% cnf(256,negated_conjecture,(X1=tptp0|~occurrence_of(esk16_0,X1)),inference(spm,[status(thm)],[65,255,theory(equality)])).
% cnf(259,negated_conjecture,(activity_occurrence(esk16_0)),inference(spm,[status(thm)],[148,255,theory(equality)])).
% cnf(261,plain,(X1=esk6_1(X2)|~occurrence_of(X2,X1)|~activity_occurrence(X2)),inference(spm,[status(thm)],[65,154,theory(equality)])).
% cnf(279,plain,(arboreal(X1)|~atomic(esk13_2(X1,X2))|~atocc(X1,X2)),inference(spm,[status(thm)],[96,230,theory(equality)])).
% cnf(284,plain,(X1=esk2_1(X2)|~root_occ(X1,X2)|~occurrence_of(X2,X3)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[68,111,theory(equality)])).
% cnf(288,plain,(X1=tptp4|~occurrence_of(esk2_1(X2),X1)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[65,112,theory(equality)])).
% cnf(312,plain,(atocc(X1,X2)|~occurrence_of(X1,esk13_2(X3,X2))|~atomic(esk13_2(X3,X2))|~atocc(X3,X2)),inference(spm,[status(thm)],[233,232,theory(equality)])).
% cnf(316,plain,(min_precedes(esk2_1(X1),esk3_1(X1),tptp0)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[214,108,theory(equality)])).
% cnf(325,plain,(X1=esk3_1(X2)|atomic(X3)|~leaf_occ(X1,X2)|~occurrence_of(X2,X3)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[144,109,theory(equality)])).
% cnf(331,plain,(root_occ(esk9_2(X1,X2),X3)|atomic(X1)|~subactivity_occurrence(esk9_2(X1,X2),X3)|~occurrence_of(X3,X1)|~occurrence_of(X2,X1)),inference(spm,[status(thm)],[179,185,theory(equality)])).
% cnf(341,plain,(esk3_1(X1)=X2|min_precedes(X2,esk3_1(X1),X3)|~arboreal(X2)|~subactivity_occurrence(X2,X1)|~occurrence_of(X1,X3)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[170,109,theory(equality)])).
% cnf(371,plain,(arboreal(esk4_2(X1,X2))|leaf_occ(X1,X2)|~atomic(tptp1)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[96,118,theory(equality)])).
% cnf(372,plain,(X1=tptp1|leaf_occ(X2,X3)|~occurrence_of(esk4_2(X2,X3),X1)|~arboreal(X2)|~subactivity_occurrence(X2,X3)|~occurrence_of(X3,tptp0)),inference(spm,[status(thm)],[65,118,theory(equality)])).
% cnf(375,plain,(arboreal(esk4_2(X1,X2))|leaf_occ(X1,X2)|$false|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(rw,[status(thm)],[371,136,theory(equality)])).
% cnf(376,plain,(arboreal(esk4_2(X1,X2))|leaf_occ(X1,X2)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(cn,[status(thm)],[375,theory(equality)])).
% cnf(392,plain,(min_precedes(X1,esk4_2(X1,X2),tptp0)|leaf_occ(X1,X2)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[214,117,theory(equality)])).
% cnf(399,negated_conjecture,(esk10_2(X1,esk16_0)=tptp0|~leaf_occ(X1,esk16_0)),inference(spm,[status(thm)],[256,193,theory(equality)])).
% cnf(400,negated_conjecture,(esk8_2(X1,esk16_0)=tptp0|~root_occ(X1,esk16_0)),inference(spm,[status(thm)],[256,178,theory(equality)])).
% cnf(401,negated_conjecture,(esk6_1(esk16_0)=tptp0|~activity_occurrence(esk16_0)),inference(spm,[status(thm)],[256,154,theory(equality)])).
% cnf(402,negated_conjecture,(esk6_1(esk16_0)=tptp0|$false),inference(rw,[status(thm)],[401,259,theory(equality)])).
% cnf(403,negated_conjecture,(esk6_1(esk16_0)=tptp0),inference(cn,[status(thm)],[402,theory(equality)])).
% cnf(414,plain,(X1=esk6_1(X2)|~occurrence_of(X2,X1)),inference(csr,[status(thm)],[261,148])).
% cnf(419,plain,(tptp4=esk6_1(esk2_1(X1))|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[414,112,theory(equality)])).
% cnf(420,plain,(X1=esk6_1(esk1_3(X1,X2,X3))|~min_precedes(X2,X3,X1)),inference(spm,[status(thm)],[414,81,theory(equality)])).
% cnf(421,plain,(esk13_2(X1,X2)=esk6_1(X1)|~atocc(X1,X2)),inference(spm,[status(thm)],[414,230,theory(equality)])).
% cnf(422,plain,(esk10_2(X1,X2)=esk6_1(X2)|~leaf_occ(X1,X2)),inference(spm,[status(thm)],[414,193,theory(equality)])).
% cnf(423,plain,(esk8_2(X1,X2)=esk6_1(X2)|~root_occ(X1,X2)),inference(spm,[status(thm)],[414,178,theory(equality)])).
% cnf(446,negated_conjecture,(leaf(X1,tptp0)|~leaf_occ(X1,esk16_0)),inference(spm,[status(thm)],[191,399,theory(equality)])).
% cnf(449,negated_conjecture,(root(X1,tptp0)|~root_occ(X1,esk16_0)),inference(spm,[status(thm)],[176,400,theory(equality)])).
% cnf(461,negated_conjecture,(root_occ(X1,X2)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)|~root_occ(X1,esk16_0)),inference(spm,[status(thm)],[179,449,theory(equality)])).
% cnf(507,plain,(leaf(X1,esk6_1(X2))|~leaf_occ(X1,X2)),inference(spm,[status(thm)],[191,422,theory(equality)])).
% cnf(511,plain,(root(X1,esk6_1(X2))|~root_occ(X1,X2)),inference(spm,[status(thm)],[176,423,theory(equality)])).
% cnf(598,plain,(arboreal(X1)|~atocc(X1,X2)),inference(csr,[status(thm)],[279,231])).
% cnf(656,plain,(occurrence_of(X1,esk6_1(X1))|~atocc(X1,X2)),inference(spm,[status(thm)],[230,421,theory(equality)])).
% cnf(661,plain,(occurrence_of(X1,esk6_1(X1))|~root(X1,X2)),inference(spm,[status(thm)],[656,163,theory(equality)])).
% cnf(664,plain,(occurrence_of(X1,esk6_1(X1))|~root_occ(X1,X2)),inference(spm,[status(thm)],[661,176,theory(equality)])).
% cnf(729,plain,(atocc(X1,X2)|~atocc(X3,X2)|~occurrence_of(X1,esk13_2(X3,X2))),inference(csr,[status(thm)],[312,231])).
% cnf(731,plain,(atocc(X1,X2)|~atocc(X3,X2)|~occurrence_of(X1,esk6_1(X3))),inference(spm,[status(thm)],[729,421,theory(equality)])).
% cnf(785,plain,(~root(esk3_1(X1),tptp0)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[197,316,theory(equality)])).
% cnf(842,plain,(X1=esk3_1(esk5_2(X1,X2))|atomic(X3)|atomic(X2)|~occurrence_of(esk5_2(X1,X2),tptp0)|~occurrence_of(esk5_2(X1,X2),X3)|~leaf(X1,X2)),inference(spm,[status(thm)],[325,131,theory(equality)])).
% cnf(909,plain,(leaf(X1,X2)|~leaf_occ(X1,esk1_3(X2,X3,X4))|~min_precedes(X3,X4,X2)),inference(spm,[status(thm)],[507,420,theory(equality)])).
% cnf(910,plain,(root(X1,X2)|~root_occ(X1,esk1_3(X2,X3,X4))|~min_precedes(X3,X4,X2)),inference(spm,[status(thm)],[511,420,theory(equality)])).
% cnf(928,plain,(esk9_2(X1,X2)=esk2_1(X3)|atomic(X1)|~occurrence_of(X3,tptp0)|~occurrence_of(X3,X4)|~subactivity_occurrence(esk9_2(X1,X2),X3)|~occurrence_of(X3,X1)|~occurrence_of(X2,X1)),inference(spm,[status(thm)],[284,331,theory(equality)])).
% cnf(1125,plain,(root(X1,X2)|leaf_occ(X1,esk1_3(X2,X3,X4))|~min_precedes(X3,X4,X2)|~arboreal(X1)|~subactivity_occurrence(X1,esk1_3(X2,X3,X4))|~occurrence_of(esk1_3(X2,X3,X4),tptp0)),inference(spm,[status(thm)],[910,71,theory(equality)])).
% cnf(1188,plain,(atocc(X1,X2)|~atocc(esk2_1(X3),X2)|~occurrence_of(X1,tptp4)|~occurrence_of(X3,tptp0)),inference(spm,[status(thm)],[731,419,theory(equality)])).
% cnf(1200,negated_conjecture,(root_occ(esk2_1(esk16_0),X1)|~subactivity_occurrence(esk2_1(esk16_0),X1)|~occurrence_of(X1,tptp0)|~occurrence_of(esk16_0,tptp0)),inference(spm,[status(thm)],[461,111,theory(equality)])).
% cnf(1202,negated_conjecture,(root_occ(esk2_1(esk16_0),X1)|~subactivity_occurrence(esk2_1(esk16_0),X1)|~occurrence_of(X1,tptp0)|$false),inference(rw,[status(thm)],[1200,255,theory(equality)])).
% cnf(1203,negated_conjecture,(root_occ(esk2_1(esk16_0),X1)|~subactivity_occurrence(esk2_1(esk16_0),X1)|~occurrence_of(X1,tptp0)),inference(cn,[status(thm)],[1202,theory(equality)])).
% cnf(2126,negated_conjecture,(root(esk2_1(esk16_0),X1)|~min_precedes(X2,X3,X1)|~subactivity_occurrence(esk2_1(esk16_0),esk1_3(X1,X2,X3))|~occurrence_of(esk1_3(X1,X2,X3),tptp0)),inference(spm,[status(thm)],[910,1203,theory(equality)])).
% cnf(2132,negated_conjecture,(occurrence_of(esk2_1(esk16_0),esk6_1(esk2_1(esk16_0)))|~subactivity_occurrence(esk2_1(esk16_0),X1)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[664,1203,theory(equality)])).
% cnf(2491,plain,(atocc(X1,esk7_2(X2,esk2_1(X3)))|~occurrence_of(X1,tptp4)|~occurrence_of(X3,tptp0)|~root(esk2_1(X3),X2)),inference(spm,[status(thm)],[1188,163,theory(equality)])).
% cnf(3239,plain,(esk3_1(esk5_2(X1,X2))=X1|atomic(X2)|~leaf(X1,X2)|~occurrence_of(esk5_2(X1,X2),tptp0)),inference(spm,[status(thm)],[842,132,theory(equality)])).
% cnf(3253,plain,(atomic(X2)|~root(X1,tptp0)|~occurrence_of(esk5_2(X1,X2),tptp0)|~leaf(X1,X2)),inference(spm,[status(thm)],[785,3239,theory(equality)])).
% cnf(3275,plain,(atomic(tptp0)|~root(X1,tptp0)|~leaf(X1,tptp0)),inference(spm,[status(thm)],[3253,132,theory(equality)])).
% cnf(3276,plain,(~root(X1,tptp0)|~leaf(X1,tptp0)),inference(sr,[status(thm)],[3275,61,theory(equality)])).
% cnf(3278,negated_conjecture,(~root(X1,tptp0)|~leaf_occ(X1,esk16_0)),inference(spm,[status(thm)],[3276,446,theory(equality)])).
% cnf(3281,negated_conjecture,(~leaf_occ(X1,esk16_0)|~root_occ(X1,esk16_0)),inference(spm,[status(thm)],[3278,449,theory(equality)])).
% cnf(3286,negated_conjecture,(~leaf_occ(esk2_1(esk16_0),esk16_0)|~occurrence_of(esk16_0,tptp0)),inference(spm,[status(thm)],[3281,111,theory(equality)])).
% cnf(3290,negated_conjecture,(~leaf_occ(esk2_1(esk16_0),esk16_0)|$false),inference(rw,[status(thm)],[3286,255,theory(equality)])).
% cnf(3291,negated_conjecture,(~leaf_occ(esk2_1(esk16_0),esk16_0)),inference(cn,[status(thm)],[3290,theory(equality)])).
% cnf(3462,plain,(esk9_2(X1,X2)=esk2_1(X2)|atomic(X1)|~occurrence_of(X2,tptp0)|~occurrence_of(X2,X3)|~occurrence_of(X2,X1)),inference(spm,[status(thm)],[928,184,theory(equality)])).
% cnf(4155,negated_conjecture,(esk9_2(X1,esk16_0)=esk2_1(esk16_0)|atomic(X1)|~occurrence_of(esk16_0,tptp0)|~occurrence_of(esk16_0,X1)),inference(spm,[status(thm)],[3462,255,theory(equality)])).
% cnf(4173,negated_conjecture,(esk9_2(X1,esk16_0)=esk2_1(esk16_0)|atomic(X1)|$false|~occurrence_of(esk16_0,X1)),inference(rw,[status(thm)],[4155,255,theory(equality)])).
% cnf(4174,negated_conjecture,(esk9_2(X1,esk16_0)=esk2_1(esk16_0)|atomic(X1)|~occurrence_of(esk16_0,X1)),inference(cn,[status(thm)],[4173,theory(equality)])).
% cnf(4180,negated_conjecture,(subactivity_occurrence(esk2_1(esk16_0),esk16_0)|atomic(X1)|~occurrence_of(esk16_0,X1)),inference(spm,[status(thm)],[184,4174,theory(equality)])).
% cnf(4281,negated_conjecture,(subactivity_occurrence(esk2_1(esk16_0),esk16_0)|atomic(esk6_1(esk16_0))|~activity_occurrence(esk16_0)),inference(spm,[status(thm)],[4180,154,theory(equality)])).
% cnf(4286,negated_conjecture,(subactivity_occurrence(esk2_1(esk16_0),esk16_0)|atomic(tptp0)|~activity_occurrence(esk16_0)),inference(rw,[status(thm)],[4281,403,theory(equality)])).
% cnf(4287,negated_conjecture,(subactivity_occurrence(esk2_1(esk16_0),esk16_0)|atomic(tptp0)|$false),inference(rw,[status(thm)],[4286,259,theory(equality)])).
% cnf(4288,negated_conjecture,(subactivity_occurrence(esk2_1(esk16_0),esk16_0)|atomic(tptp0)),inference(cn,[status(thm)],[4287,theory(equality)])).
% cnf(4289,negated_conjecture,(subactivity_occurrence(esk2_1(esk16_0),esk16_0)),inference(sr,[status(thm)],[4288,61,theory(equality)])).
% cnf(5978,plain,(leaf(X1,X2)|root(X1,X2)|~min_precedes(X3,X4,X2)|~arboreal(X1)|~subactivity_occurrence(X1,esk1_3(X2,X3,X4))|~occurrence_of(esk1_3(X2,X3,X4),tptp0)),inference(spm,[status(thm)],[909,1125,theory(equality)])).
% cnf(11349,negated_conjecture,(root(esk2_1(esk16_0),X1)|~min_precedes(esk2_1(esk16_0),X2,X1)|~occurrence_of(esk1_3(X1,esk2_1(esk16_0),X2),tptp0)),inference(spm,[status(thm)],[2126,80,theory(equality)])).
% cnf(11356,negated_conjecture,(occurrence_of(esk2_1(esk16_0),esk6_1(esk2_1(esk16_0)))|~occurrence_of(esk16_0,tptp0)),inference(spm,[status(thm)],[2132,4289,theory(equality)])).
% cnf(11358,negated_conjecture,(occurrence_of(esk2_1(esk16_0),esk6_1(esk2_1(esk16_0)))|$false),inference(rw,[status(thm)],[11356,255,theory(equality)])).
% cnf(11359,negated_conjecture,(occurrence_of(esk2_1(esk16_0),esk6_1(esk2_1(esk16_0)))),inference(cn,[status(thm)],[11358,theory(equality)])).
% cnf(11383,negated_conjecture,(esk6_1(esk2_1(esk16_0))=tptp4|~occurrence_of(esk16_0,tptp0)),inference(spm,[status(thm)],[288,11359,theory(equality)])).
% cnf(11409,negated_conjecture,(esk6_1(esk2_1(esk16_0))=tptp4|$false),inference(rw,[status(thm)],[11383,255,theory(equality)])).
% cnf(11410,negated_conjecture,(esk6_1(esk2_1(esk16_0))=tptp4),inference(cn,[status(thm)],[11409,theory(equality)])).
% cnf(11480,negated_conjecture,(occurrence_of(esk2_1(esk16_0),tptp4)),inference(rw,[status(thm)],[11359,11410,theory(equality)])).
% cnf(13049,negated_conjecture,(root(esk2_1(esk16_0),tptp0)|~min_precedes(esk2_1(esk16_0),X1,tptp0)),inference(spm,[status(thm)],[11349,81,theory(equality)])).
% cnf(13054,negated_conjecture,(root(esk2_1(esk16_0),tptp0)|~occurrence_of(esk16_0,tptp0)),inference(spm,[status(thm)],[13049,316,theory(equality)])).
% cnf(13059,negated_conjecture,(root(esk2_1(esk16_0),tptp0)|$false),inference(rw,[status(thm)],[13054,255,theory(equality)])).
% cnf(13060,negated_conjecture,(root(esk2_1(esk16_0),tptp0)),inference(cn,[status(thm)],[13059,theory(equality)])).
% cnf(14194,plain,(arboreal(X1)|~root(esk2_1(X3),X2)|~occurrence_of(X1,tptp4)|~occurrence_of(X3,tptp0)),inference(spm,[status(thm)],[598,2491,theory(equality)])).
% cnf(14247,negated_conjecture,(arboreal(X1)|~occurrence_of(X1,tptp4)|~occurrence_of(esk16_0,tptp0)),inference(spm,[status(thm)],[14194,13060,theory(equality)])).
% cnf(14252,negated_conjecture,(arboreal(X1)|~occurrence_of(X1,tptp4)|$false),inference(rw,[status(thm)],[14247,255,theory(equality)])).
% cnf(14253,negated_conjecture,(arboreal(X1)|~occurrence_of(X1,tptp4)),inference(cn,[status(thm)],[14252,theory(equality)])).
% cnf(42013,plain,(root(X1,X2)|leaf(X1,X2)|~min_precedes(X1,X3,X2)|~arboreal(X1)|~occurrence_of(esk1_3(X2,X1,X3),tptp0)),inference(spm,[status(thm)],[5978,80,theory(equality)])).
% cnf(42071,plain,(root(X1,X2)|~min_precedes(X1,X3,X2)|~arboreal(X1)|~occurrence_of(esk1_3(X2,X1,X3),tptp0)),inference(csr,[status(thm)],[42013,240])).
% cnf(42072,plain,(root(X1,tptp0)|~min_precedes(X1,X2,tptp0)|~arboreal(X1)),inference(spm,[status(thm)],[42071,81,theory(equality)])).
% cnf(42112,plain,(root(X1,tptp0)|esk3_1(X2)=X1|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[42072,341,theory(equality)])).
% cnf(42336,plain,(esk3_1(esk1_3(X1,X2,X3))=X3|root(X3,tptp0)|~arboreal(X3)|~occurrence_of(esk1_3(X1,X2,X3),tptp0)|~min_precedes(X2,X3,X1)),inference(spm,[status(thm)],[42112,79,theory(equality)])).
% cnf(52453,plain,(occurrence_of(X3,tptp3)|root(X3,tptp0)|~occurrence_of(esk1_3(X1,X2,X3),tptp0)|~min_precedes(X2,X3,X1)|~arboreal(X3)),inference(spm,[status(thm)],[110,42336,theory(equality)])).
% cnf(53221,plain,(root(X1,tptp0)|occurrence_of(X1,tptp3)|~min_precedes(X2,X1,tptp0)|~arboreal(X1)),inference(spm,[status(thm)],[52453,81,theory(equality)])).
% cnf(53252,plain,(occurrence_of(X1,tptp3)|~min_precedes(X2,X1,tptp0)|~arboreal(X1)),inference(csr,[status(thm)],[53221,197])).
% cnf(53290,plain,(occurrence_of(esk4_2(X1,X2),tptp3)|leaf_occ(X1,X2)|~arboreal(esk4_2(X1,X2))|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[53252,392,theory(equality)])).
% cnf(60733,plain,(leaf_occ(X1,X2)|occurrence_of(esk4_2(X1,X2),tptp3)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(csr,[status(thm)],[53290,376])).
% cnf(60758,plain,(tptp3=tptp1|leaf_occ(X1,X2)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[372,60733,theory(equality)])).
% cnf(60771,plain,(leaf_occ(X1,X2)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(sr,[status(thm)],[60758,222,theory(equality)])).
% cnf(60789,negated_conjecture,(leaf_occ(X1,X2)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)|~occurrence_of(X1,tptp4)),inference(spm,[status(thm)],[60771,14253,theory(equality)])).
% cnf(60857,negated_conjecture,(~subactivity_occurrence(esk2_1(esk16_0),esk16_0)|~occurrence_of(esk16_0,tptp0)|~occurrence_of(esk2_1(esk16_0),tptp4)),inference(spm,[status(thm)],[3291,60789,theory(equality)])).
% cnf(61086,negated_conjecture,($false|~occurrence_of(esk16_0,tptp0)|~occurrence_of(esk2_1(esk16_0),tptp4)),inference(rw,[status(thm)],[60857,4289,theory(equality)])).
% cnf(61087,negated_conjecture,($false|$false|~occurrence_of(esk2_1(esk16_0),tptp4)),inference(rw,[status(thm)],[61086,255,theory(equality)])).
% cnf(61088,negated_conjecture,($false|$false|$false),inference(rw,[status(thm)],[61087,11480,theory(equality)])).
% cnf(61089,negated_conjecture,($false),inference(cn,[status(thm)],[61088,theory(equality)])).
% cnf(61090,negated_conjecture,($false),61089,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 11314
% # ...of these trivial : 23
% # ...subsumed : 8425
% # ...remaining for further processing: 2866
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 420
% # Backward-rewritten : 31
% # Generated clauses : 37962
% # ...of the previous two non-trivial : 35584
% # Contextual simplify-reflections : 9143
% # Paramodulations : 37919
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 2397
% # Positive orientable unit clauses: 31
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 30
% # Non-unit-clauses : 2336
% # Current number of unprocessed clauses: 17315
% # ...number of literals in the above : 120385
% # Clause-clause subsumption calls (NU) : 654898
% # Rec. Clause-clause subsumption calls : 185349
% # Unit Clause-clause subsumption calls : 7108
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 19
% # Indexed BW rewrite successes : 17
% # Backwards rewriting index: 1299 leaves, 2.14+/-4.280 terms/leaf
% # Paramod-from index: 362 leaves, 1.15+/-0.381 terms/leaf
% # Paramod-into index: 1031 leaves, 1.79+/-2.430 terms/leaf
% # -------------------------------------------------
% # User time : 3.709 s
% # System time : 0.078 s
% # Total time : 3.787 s
% # Maximum resident set size: 0 pages
% PrfWatch: 4.75 CPU 4.87 WC
% FINAL PrfWatch: 4.75 CPU 4.87 WC
% SZS output end Solution for /tmp/SystemOnTPTP24196/PRO004+4.tptp
%
%------------------------------------------------------------------------------