%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : PRO006+3 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art04.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Wed Dec 29 21:03:33 EST 2010
% Result : Theorem 12.10s
% Output : Solution 12.10s
% 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/SystemOnTPTP32132/PRO006+3.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP32132/PRO006+3.tptp
% SZS output start Solution for /tmp/SystemOnTPTP32132/PRO006+3.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 32228
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% PrfWatch: 1.93 CPU 2.02 WC
% PrfWatch: 3.92 CPU 4.03 WC
% PrfWatch: 5.54 CPU 6.03 WC
% PrfWatch: 7.17 CPU 8.04 WC
% # Preprocessing time : 0.022 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 9.17 CPU 10.04 WC
% # SZS output start CNFRefutation.
% fof(1, axiom,~(atomic(tptp0)),file('/tmp/SRASS.s.p', sos_51)).
% fof(3, axiom,![X1]:![X2]:![X3]:((occurrence_of(X1,X2)&occurrence_of(X1,X3))=>X2=X3),file('/tmp/SRASS.s.p', sos_02)).
% fof(6, axiom,![X9]:![X10]:![X11]:((subactivity_occurrence(X9,X10)&subactivity_occurrence(X10,X11))=>subactivity_occurrence(X9,X11)),file('/tmp/SRASS.s.p', sos_31)).
% fof(7, axiom,![X12]:![X13]:![X14]:![X15]:(((occurrence_of(X14,X15)&root_occ(X12,X14))&root_occ(X13,X14))=>X12=X13),file('/tmp/SRASS.s.p', sos_35)).
% fof(8, axiom,![X16]:![X17]:![X18]:(min_precedes(X17,X18,X16)=>?[X19]:((occurrence_of(X19,X16)&subactivity_occurrence(X17,X19))&subactivity_occurrence(X18,X19))),file('/tmp/SRASS.s.p', sos_25)).
% fof(13, axiom,![X35]:![X36]:(occurrence_of(X35,X36)=>(arboreal(X35)<=>atomic(X36))),file('/tmp/SRASS.s.p', sos_07)).
% fof(14, axiom,![X37]:![X38]:![X39]:![X40]:((((occurrence_of(X39,X37)&occurrence_of(X40,X38))&subactivity(X37,X38))&~(subactivity_occurrence(X39,X40)))=>?[X41]:(subactivity_occurrence(X41,X40)&~(subactivity_occurrence(X41,X39)))),file('/tmp/SRASS.s.p', sos_32)).
% fof(15, axiom,![X42]:![X43]:((((occurrence_of(X43,tptp0)&subactivity_occurrence(X42,X43))&arboreal(X42))&~(leaf_occ(X42,X43)))=>?[X44]:(occurrence_of(X44,tptp1)&next_subocc(X42,X44,tptp0))),file('/tmp/SRASS.s.p', sos_62)).
% fof(16, axiom,![X45]:(activity(X45)=>subactivity(X45,X45)),file('/tmp/SRASS.s.p', sos_03)).
% fof(17, axiom,![X46]:(occurrence_of(X46,tptp0)=>?[X47]:?[X48]:((((occurrence_of(X47,tptp4)&root_occ(X47,X46))&occurrence_of(X48,tptp3))&leaf_occ(X48,X46))&next_subocc(X47,X48,tptp0))),file('/tmp/SRASS.s.p', sos_49)).
% fof(18, axiom,![X49]:![X50]:((leaf(X49,X50)&~(atomic(X50)))=>?[X51]:(occurrence_of(X51,X50)&leaf_occ(X49,X51))),file('/tmp/SRASS.s.p', sos_45)).
% fof(19, axiom,atomic(tptp4),file('/tmp/SRASS.s.p', sos_52)).
% fof(24, axiom,![X55]:![X56]:![X57]:![X58]:((((occurrence_of(X57,X58)&~(atomic(X58)))&leaf_occ(X55,X57))&leaf_occ(X56,X57))=>X55=X56),file('/tmp/SRASS.s.p', sos_36)).
% fof(27, axiom,![X68]:![X69]:(occurrence_of(X69,X68)=>(activity(X68)&activity_occurrence(X69))),file('/tmp/SRASS.s.p', sos)).
% fof(28, axiom,![X70]:(activity_occurrence(X70)=>?[X71]:(activity(X71)&occurrence_of(X70,X71))),file('/tmp/SRASS.s.p', sos_01)).
% fof(29, axiom,![X72]:![X73]:![X74]:(next_subocc(X72,X73,X74)<=>(min_precedes(X72,X73,X74)&~(?[X75]:(min_precedes(X72,X75,X74)&min_precedes(X75,X73,X74))))),file('/tmp/SRASS.s.p', sos_22)).
% fof(33, axiom,![X84]:![X85]:(root(X85,X84)=>?[X86]:(subactivity(X86,X84)&atocc(X85,X86))),file('/tmp/SRASS.s.p', sos_12)).
% fof(37, axiom,![X95]:![X96]:(root_occ(X95,X96)<=>?[X97]:((occurrence_of(X96,X97)&subactivity_occurrence(X95,X96))&root(X95,X97))),file('/tmp/SRASS.s.p', sos_33)).
% fof(38, axiom,![X98]:![X99]:![X100]:![X101]:(((((occurrence_of(X99,X98)&subactivity_occurrence(X100,X99))&root_occ(X101,X99))&arboreal(X100))&~(min_precedes(X101,X100,X98)))=>X101=X100),file('/tmp/SRASS.s.p', sos_42)).
% fof(39, axiom,![X102]:![X103]:![X104]:![X105]:(((((occurrence_of(X103,X102)&subactivity_occurrence(X104,X103))&leaf_occ(X105,X103))&arboreal(X104))&~(min_precedes(X104,X105,X102)))=>X105=X104),file('/tmp/SRASS.s.p', sos_43)).
% fof(43, axiom,![X120]:![X121]:![X122]:(min_precedes(X120,X121,X122)=>~(root(X121,X122))),file('/tmp/SRASS.s.p', sos_14)).
% fof(45, axiom,![X126]:![X127]:((occurrence_of(X127,X126)&~(atomic(X126)))=>?[X128]:(root(X128,X126)&subactivity_occurrence(X128,X127))),file('/tmp/SRASS.s.p', sos_27)).
% fof(47, axiom,![X133]:![X134]:(leaf_occ(X133,X134)<=>?[X135]:((occurrence_of(X134,X135)&subactivity_occurrence(X133,X134))&leaf(X133,X135))),file('/tmp/SRASS.s.p', sos_34)).
% fof(48, axiom,![X136]:![X137]:![X138]:(min_precedes(X136,X137,X138)=>arboreal(X136)),file('/tmp/SRASS.s.p', sos_46)).
% fof(49, axiom,![X139]:![X140]:![X141]:(min_precedes(X140,X141,X139)=>?[X142]:?[X143]:(((subactivity(X142,X139)&subactivity(X143,X139))&atocc(X140,X142))&atocc(X141,X143))),file('/tmp/SRASS.s.p', sos_11)).
% fof(53, axiom,![X155]:![X156]:(leaf(X155,X156)<=>((root(X155,X156)|?[X157]:min_precedes(X157,X155,X156))&~(?[X158]:min_precedes(X155,X158,X156)))),file('/tmp/SRASS.s.p', sos_21)).
% fof(54, axiom,![X159]:![X160]:(atocc(X159,X160)<=>?[X161]:((subactivity(X160,X161)&atomic(X161))&occurrence_of(X159,X161))),file('/tmp/SRASS.s.p', sos_23)).
% fof(56, axiom,~(tptp4=tptp1),file('/tmp/SRASS.s.p', sos_56)).
% fof(59, axiom,~(tptp1=tptp3),file('/tmp/SRASS.s.p', sos_59)).
% fof(64, conjecture,~(?[X168]:occurrence_of(X168,tptp0)),file('/tmp/SRASS.s.p', goals)).
% fof(65, negated_conjecture,~(~(?[X168]:occurrence_of(X168,tptp0))),inference(assume_negation,[status(cth)],[64])).
% fof(66, plain,~(atomic(tptp0)),inference(fof_simplification,[status(thm)],[1,theory(equality)])).
% fof(69, plain,![X37]:![X38]:![X39]:![X40]:((((occurrence_of(X39,X37)&occurrence_of(X40,X38))&subactivity(X37,X38))&~(subactivity_occurrence(X39,X40)))=>?[X41]:(subactivity_occurrence(X41,X40)&~(subactivity_occurrence(X41,X39)))),inference(fof_simplification,[status(thm)],[14,theory(equality)])).
% fof(70, plain,![X42]:![X43]:((((occurrence_of(X43,tptp0)&subactivity_occurrence(X42,X43))&arboreal(X42))&~(leaf_occ(X42,X43)))=>?[X44]:(occurrence_of(X44,tptp1)&next_subocc(X42,X44,tptp0))),inference(fof_simplification,[status(thm)],[15,theory(equality)])).
% fof(71, plain,![X49]:![X50]:((leaf(X49,X50)&~(atomic(X50)))=>?[X51]:(occurrence_of(X51,X50)&leaf_occ(X49,X51))),inference(fof_simplification,[status(thm)],[18,theory(equality)])).
% fof(72, plain,![X55]:![X56]:![X57]:![X58]:((((occurrence_of(X57,X58)&~(atomic(X58)))&leaf_occ(X55,X57))&leaf_occ(X56,X57))=>X55=X56),inference(fof_simplification,[status(thm)],[24,theory(equality)])).
% fof(73, plain,![X98]:![X99]:![X100]:![X101]:(((((occurrence_of(X99,X98)&subactivity_occurrence(X100,X99))&root_occ(X101,X99))&arboreal(X100))&~(min_precedes(X101,X100,X98)))=>X101=X100),inference(fof_simplification,[status(thm)],[38,theory(equality)])).
% fof(74, plain,![X102]:![X103]:![X104]:![X105]:(((((occurrence_of(X103,X102)&subactivity_occurrence(X104,X103))&leaf_occ(X105,X103))&arboreal(X104))&~(min_precedes(X104,X105,X102)))=>X105=X104),inference(fof_simplification,[status(thm)],[39,theory(equality)])).
% fof(75, plain,![X120]:![X121]:![X122]:(min_precedes(X120,X121,X122)=>~(root(X121,X122))),inference(fof_simplification,[status(thm)],[43,theory(equality)])).
% fof(77, plain,![X126]:![X127]:((occurrence_of(X127,X126)&~(atomic(X126)))=>?[X128]:(root(X128,X126)&subactivity_occurrence(X128,X127))),inference(fof_simplification,[status(thm)],[45,theory(equality)])).
% cnf(79,plain,(~atomic(tptp0)),inference(split_conjunct,[status(thm)],[66])).
% fof(81, plain,![X1]:![X2]:![X3]:((~(occurrence_of(X1,X2))|~(occurrence_of(X1,X3)))|X2=X3),inference(fof_nnf,[status(thm)],[3])).
% fof(82, plain,![X4]:![X5]:![X6]:((~(occurrence_of(X4,X5))|~(occurrence_of(X4,X6)))|X5=X6),inference(variable_rename,[status(thm)],[81])).
% cnf(83,plain,(X1=X2|~occurrence_of(X3,X2)|~occurrence_of(X3,X1)),inference(split_conjunct,[status(thm)],[82])).
% fof(90, plain,![X9]:![X10]:![X11]:((~(subactivity_occurrence(X9,X10))|~(subactivity_occurrence(X10,X11)))|subactivity_occurrence(X9,X11)),inference(fof_nnf,[status(thm)],[6])).
% fof(91, plain,![X12]:![X13]:![X14]:((~(subactivity_occurrence(X12,X13))|~(subactivity_occurrence(X13,X14)))|subactivity_occurrence(X12,X14)),inference(variable_rename,[status(thm)],[90])).
% cnf(92,plain,(subactivity_occurrence(X1,X2)|~subactivity_occurrence(X3,X2)|~subactivity_occurrence(X1,X3)),inference(split_conjunct,[status(thm)],[91])).
% fof(93, plain,![X12]:![X13]:![X14]:![X15]:(((~(occurrence_of(X14,X15))|~(root_occ(X12,X14)))|~(root_occ(X13,X14)))|X12=X13),inference(fof_nnf,[status(thm)],[7])).
% fof(94, plain,![X16]:![X17]:![X18]:![X19]:(((~(occurrence_of(X18,X19))|~(root_occ(X16,X18)))|~(root_occ(X17,X18)))|X16=X17),inference(variable_rename,[status(thm)],[93])).
% cnf(95,plain,(X1=X2|~root_occ(X2,X3)|~root_occ(X1,X3)|~occurrence_of(X3,X4)),inference(split_conjunct,[status(thm)],[94])).
% fof(96, plain,![X16]:![X17]:![X18]:(~(min_precedes(X17,X18,X16))|?[X19]:((occurrence_of(X19,X16)&subactivity_occurrence(X17,X19))&subactivity_occurrence(X18,X19))),inference(fof_nnf,[status(thm)],[8])).
% fof(97, plain,![X20]:![X21]:![X22]:(~(min_precedes(X21,X22,X20))|?[X23]:((occurrence_of(X23,X20)&subactivity_occurrence(X21,X23))&subactivity_occurrence(X22,X23))),inference(variable_rename,[status(thm)],[96])).
% fof(98, plain,![X20]:![X21]:![X22]:(~(min_precedes(X21,X22,X20))|((occurrence_of(esk1_3(X20,X21,X22),X20)&subactivity_occurrence(X21,esk1_3(X20,X21,X22)))&subactivity_occurrence(X22,esk1_3(X20,X21,X22)))),inference(skolemize,[status(esa)],[97])).
% fof(99, plain,![X20]:![X21]:![X22]:(((occurrence_of(esk1_3(X20,X21,X22),X20)|~(min_precedes(X21,X22,X20)))&(subactivity_occurrence(X21,esk1_3(X20,X21,X22))|~(min_precedes(X21,X22,X20))))&(subactivity_occurrence(X22,esk1_3(X20,X21,X22))|~(min_precedes(X21,X22,X20)))),inference(distribute,[status(thm)],[98])).
% cnf(101,plain,(subactivity_occurrence(X1,esk1_3(X3,X1,X2))|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[99])).
% cnf(102,plain,(occurrence_of(esk1_3(X3,X1,X2),X3)|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[99])).
% fof(117, plain,![X35]:![X36]:(~(occurrence_of(X35,X36))|((~(arboreal(X35))|atomic(X36))&(~(atomic(X36))|arboreal(X35)))),inference(fof_nnf,[status(thm)],[13])).
% fof(118, plain,![X37]:![X38]:(~(occurrence_of(X37,X38))|((~(arboreal(X37))|atomic(X38))&(~(atomic(X38))|arboreal(X37)))),inference(variable_rename,[status(thm)],[117])).
% fof(119, plain,![X37]:![X38]:(((~(arboreal(X37))|atomic(X38))|~(occurrence_of(X37,X38)))&((~(atomic(X38))|arboreal(X37))|~(occurrence_of(X37,X38)))),inference(distribute,[status(thm)],[118])).
% cnf(120,plain,(arboreal(X1)|~occurrence_of(X1,X2)|~atomic(X2)),inference(split_conjunct,[status(thm)],[119])).
% fof(122, plain,![X37]:![X38]:![X39]:![X40]:((((~(occurrence_of(X39,X37))|~(occurrence_of(X40,X38)))|~(subactivity(X37,X38)))|subactivity_occurrence(X39,X40))|?[X41]:(subactivity_occurrence(X41,X40)&~(subactivity_occurrence(X41,X39)))),inference(fof_nnf,[status(thm)],[69])).
% fof(123, plain,![X42]:![X43]:![X44]:![X45]:((((~(occurrence_of(X44,X42))|~(occurrence_of(X45,X43)))|~(subactivity(X42,X43)))|subactivity_occurrence(X44,X45))|?[X46]:(subactivity_occurrence(X46,X45)&~(subactivity_occurrence(X46,X44)))),inference(variable_rename,[status(thm)],[122])).
% fof(124, plain,![X42]:![X43]:![X44]:![X45]:((((~(occurrence_of(X44,X42))|~(occurrence_of(X45,X43)))|~(subactivity(X42,X43)))|subactivity_occurrence(X44,X45))|(subactivity_occurrence(esk2_4(X42,X43,X44,X45),X45)&~(subactivity_occurrence(esk2_4(X42,X43,X44,X45),X44)))),inference(skolemize,[status(esa)],[123])).
% fof(125, plain,![X42]:![X43]:![X44]:![X45]:((subactivity_occurrence(esk2_4(X42,X43,X44,X45),X45)|(((~(occurrence_of(X44,X42))|~(occurrence_of(X45,X43)))|~(subactivity(X42,X43)))|subactivity_occurrence(X44,X45)))&(~(subactivity_occurrence(esk2_4(X42,X43,X44,X45),X44))|(((~(occurrence_of(X44,X42))|~(occurrence_of(X45,X43)))|~(subactivity(X42,X43)))|subactivity_occurrence(X44,X45)))),inference(distribute,[status(thm)],[124])).
% cnf(126,plain,(subactivity_occurrence(X1,X2)|~subactivity(X3,X4)|~occurrence_of(X2,X4)|~occurrence_of(X1,X3)|~subactivity_occurrence(esk2_4(X3,X4,X1,X2),X1)),inference(split_conjunct,[status(thm)],[125])).
% cnf(127,plain,(subactivity_occurrence(X1,X2)|subactivity_occurrence(esk2_4(X3,X4,X1,X2),X2)|~subactivity(X3,X4)|~occurrence_of(X2,X4)|~occurrence_of(X1,X3)),inference(split_conjunct,[status(thm)],[125])).
% fof(128, plain,![X42]:![X43]:((((~(occurrence_of(X43,tptp0))|~(subactivity_occurrence(X42,X43)))|~(arboreal(X42)))|leaf_occ(X42,X43))|?[X44]:(occurrence_of(X44,tptp1)&next_subocc(X42,X44,tptp0))),inference(fof_nnf,[status(thm)],[70])).
% fof(129, plain,![X45]:![X46]:((((~(occurrence_of(X46,tptp0))|~(subactivity_occurrence(X45,X46)))|~(arboreal(X45)))|leaf_occ(X45,X46))|?[X47]:(occurrence_of(X47,tptp1)&next_subocc(X45,X47,tptp0))),inference(variable_rename,[status(thm)],[128])).
% fof(130, plain,![X45]:![X46]:((((~(occurrence_of(X46,tptp0))|~(subactivity_occurrence(X45,X46)))|~(arboreal(X45)))|leaf_occ(X45,X46))|(occurrence_of(esk3_2(X45,X46),tptp1)&next_subocc(X45,esk3_2(X45,X46),tptp0))),inference(skolemize,[status(esa)],[129])).
% fof(131, plain,![X45]:![X46]:((occurrence_of(esk3_2(X45,X46),tptp1)|(((~(occurrence_of(X46,tptp0))|~(subactivity_occurrence(X45,X46)))|~(arboreal(X45)))|leaf_occ(X45,X46)))&(next_subocc(X45,esk3_2(X45,X46),tptp0)|(((~(occurrence_of(X46,tptp0))|~(subactivity_occurrence(X45,X46)))|~(arboreal(X45)))|leaf_occ(X45,X46)))),inference(distribute,[status(thm)],[130])).
% cnf(132,plain,(leaf_occ(X1,X2)|next_subocc(X1,esk3_2(X1,X2),tptp0)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(split_conjunct,[status(thm)],[131])).
% cnf(133,plain,(leaf_occ(X1,X2)|occurrence_of(esk3_2(X1,X2),tptp1)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(split_conjunct,[status(thm)],[131])).
% fof(134, plain,![X45]:(~(activity(X45))|subactivity(X45,X45)),inference(fof_nnf,[status(thm)],[16])).
% fof(135, plain,![X46]:(~(activity(X46))|subactivity(X46,X46)),inference(variable_rename,[status(thm)],[134])).
% cnf(136,plain,(subactivity(X1,X1)|~activity(X1)),inference(split_conjunct,[status(thm)],[135])).
% fof(137, plain,![X46]:(~(occurrence_of(X46,tptp0))|?[X47]:?[X48]:((((occurrence_of(X47,tptp4)&root_occ(X47,X46))&occurrence_of(X48,tptp3))&leaf_occ(X48,X46))&next_subocc(X47,X48,tptp0))),inference(fof_nnf,[status(thm)],[17])).
% fof(138, plain,![X49]:(~(occurrence_of(X49,tptp0))|?[X50]:?[X51]:((((occurrence_of(X50,tptp4)&root_occ(X50,X49))&occurrence_of(X51,tptp3))&leaf_occ(X51,X49))&next_subocc(X50,X51,tptp0))),inference(variable_rename,[status(thm)],[137])).
% fof(139, plain,![X49]:(~(occurrence_of(X49,tptp0))|((((occurrence_of(esk4_1(X49),tptp4)&root_occ(esk4_1(X49),X49))&occurrence_of(esk5_1(X49),tptp3))&leaf_occ(esk5_1(X49),X49))&next_subocc(esk4_1(X49),esk5_1(X49),tptp0))),inference(skolemize,[status(esa)],[138])).
% fof(140, plain,![X49]:(((((occurrence_of(esk4_1(X49),tptp4)|~(occurrence_of(X49,tptp0)))&(root_occ(esk4_1(X49),X49)|~(occurrence_of(X49,tptp0))))&(occurrence_of(esk5_1(X49),tptp3)|~(occurrence_of(X49,tptp0))))&(leaf_occ(esk5_1(X49),X49)|~(occurrence_of(X49,tptp0))))&(next_subocc(esk4_1(X49),esk5_1(X49),tptp0)|~(occurrence_of(X49,tptp0)))),inference(distribute,[status(thm)],[139])).
% cnf(141,plain,(next_subocc(esk4_1(X1),esk5_1(X1),tptp0)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[140])).
% cnf(142,plain,(leaf_occ(esk5_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[140])).
% cnf(143,plain,(occurrence_of(esk5_1(X1),tptp3)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[140])).
% cnf(144,plain,(root_occ(esk4_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[140])).
% cnf(145,plain,(occurrence_of(esk4_1(X1),tptp4)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[140])).
% fof(146, plain,![X49]:![X50]:((~(leaf(X49,X50))|atomic(X50))|?[X51]:(occurrence_of(X51,X50)&leaf_occ(X49,X51))),inference(fof_nnf,[status(thm)],[71])).
% fof(147, plain,![X52]:![X53]:((~(leaf(X52,X53))|atomic(X53))|?[X54]:(occurrence_of(X54,X53)&leaf_occ(X52,X54))),inference(variable_rename,[status(thm)],[146])).
% fof(148, plain,![X52]:![X53]:((~(leaf(X52,X53))|atomic(X53))|(occurrence_of(esk6_2(X52,X53),X53)&leaf_occ(X52,esk6_2(X52,X53)))),inference(skolemize,[status(esa)],[147])).
% fof(149, plain,![X52]:![X53]:((occurrence_of(esk6_2(X52,X53),X53)|(~(leaf(X52,X53))|atomic(X53)))&(leaf_occ(X52,esk6_2(X52,X53))|(~(leaf(X52,X53))|atomic(X53)))),inference(distribute,[status(thm)],[148])).
% cnf(150,plain,(atomic(X1)|leaf_occ(X2,esk6_2(X2,X1))|~leaf(X2,X1)),inference(split_conjunct,[status(thm)],[149])).
% cnf(151,plain,(atomic(X1)|occurrence_of(esk6_2(X2,X1),X1)|~leaf(X2,X1)),inference(split_conjunct,[status(thm)],[149])).
% cnf(152,plain,(atomic(tptp4)),inference(split_conjunct,[status(thm)],[19])).
% fof(159, plain,![X55]:![X56]:![X57]:![X58]:((((~(occurrence_of(X57,X58))|atomic(X58))|~(leaf_occ(X55,X57)))|~(leaf_occ(X56,X57)))|X55=X56),inference(fof_nnf,[status(thm)],[72])).
% fof(160, plain,![X59]:![X60]:![X61]:![X62]:((((~(occurrence_of(X61,X62))|atomic(X62))|~(leaf_occ(X59,X61)))|~(leaf_occ(X60,X61)))|X59=X60),inference(variable_rename,[status(thm)],[159])).
% cnf(161,plain,(X1=X2|atomic(X4)|~leaf_occ(X2,X3)|~leaf_occ(X1,X3)|~occurrence_of(X3,X4)),inference(split_conjunct,[status(thm)],[160])).
% fof(168, plain,![X68]:![X69]:(~(occurrence_of(X69,X68))|(activity(X68)&activity_occurrence(X69))),inference(fof_nnf,[status(thm)],[27])).
% fof(169, plain,![X70]:![X71]:(~(occurrence_of(X71,X70))|(activity(X70)&activity_occurrence(X71))),inference(variable_rename,[status(thm)],[168])).
% fof(170, plain,![X70]:![X71]:((activity(X70)|~(occurrence_of(X71,X70)))&(activity_occurrence(X71)|~(occurrence_of(X71,X70)))),inference(distribute,[status(thm)],[169])).
% cnf(171,plain,(activity_occurrence(X1)|~occurrence_of(X1,X2)),inference(split_conjunct,[status(thm)],[170])).
% cnf(172,plain,(activity(X2)|~occurrence_of(X1,X2)),inference(split_conjunct,[status(thm)],[170])).
% fof(173, plain,![X70]:(~(activity_occurrence(X70))|?[X71]:(activity(X71)&occurrence_of(X70,X71))),inference(fof_nnf,[status(thm)],[28])).
% fof(174, plain,![X72]:(~(activity_occurrence(X72))|?[X73]:(activity(X73)&occurrence_of(X72,X73))),inference(variable_rename,[status(thm)],[173])).
% fof(175, plain,![X72]:(~(activity_occurrence(X72))|(activity(esk7_1(X72))&occurrence_of(X72,esk7_1(X72)))),inference(skolemize,[status(esa)],[174])).
% fof(176, plain,![X72]:((activity(esk7_1(X72))|~(activity_occurrence(X72)))&(occurrence_of(X72,esk7_1(X72))|~(activity_occurrence(X72)))),inference(distribute,[status(thm)],[175])).
% cnf(177,plain,(occurrence_of(X1,esk7_1(X1))|~activity_occurrence(X1)),inference(split_conjunct,[status(thm)],[176])).
% cnf(178,plain,(activity(esk7_1(X1))|~activity_occurrence(X1)),inference(split_conjunct,[status(thm)],[176])).
% fof(179, plain,![X72]:![X73]:![X74]:((~(next_subocc(X72,X73,X74))|(min_precedes(X72,X73,X74)&![X75]:(~(min_precedes(X72,X75,X74))|~(min_precedes(X75,X73,X74)))))&((~(min_precedes(X72,X73,X74))|?[X75]:(min_precedes(X72,X75,X74)&min_precedes(X75,X73,X74)))|next_subocc(X72,X73,X74))),inference(fof_nnf,[status(thm)],[29])).
% fof(180, plain,![X76]:![X77]:![X78]:((~(next_subocc(X76,X77,X78))|(min_precedes(X76,X77,X78)&![X79]:(~(min_precedes(X76,X79,X78))|~(min_precedes(X79,X77,X78)))))&((~(min_precedes(X76,X77,X78))|?[X80]:(min_precedes(X76,X80,X78)&min_precedes(X80,X77,X78)))|next_subocc(X76,X77,X78))),inference(variable_rename,[status(thm)],[179])).
% fof(181, plain,![X76]:![X77]:![X78]:((~(next_subocc(X76,X77,X78))|(min_precedes(X76,X77,X78)&![X79]:(~(min_precedes(X76,X79,X78))|~(min_precedes(X79,X77,X78)))))&((~(min_precedes(X76,X77,X78))|(min_precedes(X76,esk8_3(X76,X77,X78),X78)&min_precedes(esk8_3(X76,X77,X78),X77,X78)))|next_subocc(X76,X77,X78))),inference(skolemize,[status(esa)],[180])).
% fof(182, plain,![X76]:![X77]:![X78]:![X79]:((((~(min_precedes(X76,X79,X78))|~(min_precedes(X79,X77,X78)))&min_precedes(X76,X77,X78))|~(next_subocc(X76,X77,X78)))&((~(min_precedes(X76,X77,X78))|(min_precedes(X76,esk8_3(X76,X77,X78),X78)&min_precedes(esk8_3(X76,X77,X78),X77,X78)))|next_subocc(X76,X77,X78))),inference(shift_quantors,[status(thm)],[181])).
% fof(183, plain,![X76]:![X77]:![X78]:![X79]:((((~(min_precedes(X76,X79,X78))|~(min_precedes(X79,X77,X78)))|~(next_subocc(X76,X77,X78)))&(min_precedes(X76,X77,X78)|~(next_subocc(X76,X77,X78))))&(((min_precedes(X76,esk8_3(X76,X77,X78),X78)|~(min_precedes(X76,X77,X78)))|next_subocc(X76,X77,X78))&((min_precedes(esk8_3(X76,X77,X78),X77,X78)|~(min_precedes(X76,X77,X78)))|next_subocc(X76,X77,X78)))),inference(distribute,[status(thm)],[182])).
% cnf(186,plain,(min_precedes(X1,X2,X3)|~next_subocc(X1,X2,X3)),inference(split_conjunct,[status(thm)],[183])).
% cnf(187,plain,(~next_subocc(X1,X2,X3)|~min_precedes(X4,X2,X3)|~min_precedes(X1,X4,X3)),inference(split_conjunct,[status(thm)],[183])).
% fof(200, plain,![X84]:![X85]:(~(root(X85,X84))|?[X86]:(subactivity(X86,X84)&atocc(X85,X86))),inference(fof_nnf,[status(thm)],[33])).
% fof(201, plain,![X87]:![X88]:(~(root(X88,X87))|?[X89]:(subactivity(X89,X87)&atocc(X88,X89))),inference(variable_rename,[status(thm)],[200])).
% fof(202, plain,![X87]:![X88]:(~(root(X88,X87))|(subactivity(esk9_2(X87,X88),X87)&atocc(X88,esk9_2(X87,X88)))),inference(skolemize,[status(esa)],[201])).
% fof(203, plain,![X87]:![X88]:((subactivity(esk9_2(X87,X88),X87)|~(root(X88,X87)))&(atocc(X88,esk9_2(X87,X88))|~(root(X88,X87)))),inference(distribute,[status(thm)],[202])).
% cnf(204,plain,(atocc(X1,esk9_2(X2,X1))|~root(X1,X2)),inference(split_conjunct,[status(thm)],[203])).
% fof(217, plain,![X95]:![X96]:((~(root_occ(X95,X96))|?[X97]:((occurrence_of(X96,X97)&subactivity_occurrence(X95,X96))&root(X95,X97)))&(![X97]:((~(occurrence_of(X96,X97))|~(subactivity_occurrence(X95,X96)))|~(root(X95,X97)))|root_occ(X95,X96))),inference(fof_nnf,[status(thm)],[37])).
% fof(218, plain,![X98]:![X99]:((~(root_occ(X98,X99))|?[X100]:((occurrence_of(X99,X100)&subactivity_occurrence(X98,X99))&root(X98,X100)))&(![X101]:((~(occurrence_of(X99,X101))|~(subactivity_occurrence(X98,X99)))|~(root(X98,X101)))|root_occ(X98,X99))),inference(variable_rename,[status(thm)],[217])).
% fof(219, plain,![X98]:![X99]:((~(root_occ(X98,X99))|((occurrence_of(X99,esk10_2(X98,X99))&subactivity_occurrence(X98,X99))&root(X98,esk10_2(X98,X99))))&(![X101]:((~(occurrence_of(X99,X101))|~(subactivity_occurrence(X98,X99)))|~(root(X98,X101)))|root_occ(X98,X99))),inference(skolemize,[status(esa)],[218])).
% fof(220, plain,![X98]:![X99]:![X101]:((((~(occurrence_of(X99,X101))|~(subactivity_occurrence(X98,X99)))|~(root(X98,X101)))|root_occ(X98,X99))&(~(root_occ(X98,X99))|((occurrence_of(X99,esk10_2(X98,X99))&subactivity_occurrence(X98,X99))&root(X98,esk10_2(X98,X99))))),inference(shift_quantors,[status(thm)],[219])).
% fof(221, plain,![X98]:![X99]:![X101]:((((~(occurrence_of(X99,X101))|~(subactivity_occurrence(X98,X99)))|~(root(X98,X101)))|root_occ(X98,X99))&(((occurrence_of(X99,esk10_2(X98,X99))|~(root_occ(X98,X99)))&(subactivity_occurrence(X98,X99)|~(root_occ(X98,X99))))&(root(X98,esk10_2(X98,X99))|~(root_occ(X98,X99))))),inference(distribute,[status(thm)],[220])).
% cnf(222,plain,(root(X1,esk10_2(X1,X2))|~root_occ(X1,X2)),inference(split_conjunct,[status(thm)],[221])).
% cnf(223,plain,(subactivity_occurrence(X1,X2)|~root_occ(X1,X2)),inference(split_conjunct,[status(thm)],[221])).
% cnf(224,plain,(occurrence_of(X2,esk10_2(X1,X2))|~root_occ(X1,X2)),inference(split_conjunct,[status(thm)],[221])).
% cnf(225,plain,(root_occ(X1,X2)|~root(X1,X3)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,X3)),inference(split_conjunct,[status(thm)],[221])).
% fof(226, plain,![X98]:![X99]:![X100]:![X101]:(((((~(occurrence_of(X99,X98))|~(subactivity_occurrence(X100,X99)))|~(root_occ(X101,X99)))|~(arboreal(X100)))|min_precedes(X101,X100,X98))|X101=X100),inference(fof_nnf,[status(thm)],[73])).
% fof(227, plain,![X102]:![X103]:![X104]:![X105]:(((((~(occurrence_of(X103,X102))|~(subactivity_occurrence(X104,X103)))|~(root_occ(X105,X103)))|~(arboreal(X104)))|min_precedes(X105,X104,X102))|X105=X104),inference(variable_rename,[status(thm)],[226])).
% cnf(228,plain,(X1=X2|min_precedes(X1,X2,X3)|~arboreal(X2)|~root_occ(X1,X4)|~subactivity_occurrence(X2,X4)|~occurrence_of(X4,X3)),inference(split_conjunct,[status(thm)],[227])).
% fof(229, plain,![X102]:![X103]:![X104]:![X105]:(((((~(occurrence_of(X103,X102))|~(subactivity_occurrence(X104,X103)))|~(leaf_occ(X105,X103)))|~(arboreal(X104)))|min_precedes(X104,X105,X102))|X105=X104),inference(fof_nnf,[status(thm)],[74])).
% fof(230, plain,![X106]:![X107]:![X108]:![X109]:(((((~(occurrence_of(X107,X106))|~(subactivity_occurrence(X108,X107)))|~(leaf_occ(X109,X107)))|~(arboreal(X108)))|min_precedes(X108,X109,X106))|X109=X108),inference(variable_rename,[status(thm)],[229])).
% cnf(231,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)],[230])).
% fof(244, plain,![X120]:![X121]:![X122]:(~(min_precedes(X120,X121,X122))|~(root(X121,X122))),inference(fof_nnf,[status(thm)],[75])).
% fof(245, plain,![X123]:![X124]:![X125]:(~(min_precedes(X123,X124,X125))|~(root(X124,X125))),inference(variable_rename,[status(thm)],[244])).
% cnf(246,plain,(~root(X1,X2)|~min_precedes(X3,X1,X2)),inference(split_conjunct,[status(thm)],[245])).
% fof(253, plain,![X126]:![X127]:((~(occurrence_of(X127,X126))|atomic(X126))|?[X128]:(root(X128,X126)&subactivity_occurrence(X128,X127))),inference(fof_nnf,[status(thm)],[77])).
% fof(254, plain,![X129]:![X130]:((~(occurrence_of(X130,X129))|atomic(X129))|?[X131]:(root(X131,X129)&subactivity_occurrence(X131,X130))),inference(variable_rename,[status(thm)],[253])).
% fof(255, plain,![X129]:![X130]:((~(occurrence_of(X130,X129))|atomic(X129))|(root(esk13_2(X129,X130),X129)&subactivity_occurrence(esk13_2(X129,X130),X130))),inference(skolemize,[status(esa)],[254])).
% fof(256, plain,![X129]:![X130]:((root(esk13_2(X129,X130),X129)|(~(occurrence_of(X130,X129))|atomic(X129)))&(subactivity_occurrence(esk13_2(X129,X130),X130)|(~(occurrence_of(X130,X129))|atomic(X129)))),inference(distribute,[status(thm)],[255])).
% cnf(257,plain,(atomic(X1)|subactivity_occurrence(esk13_2(X1,X2),X2)|~occurrence_of(X2,X1)),inference(split_conjunct,[status(thm)],[256])).
% cnf(258,plain,(atomic(X1)|root(esk13_2(X1,X2),X1)|~occurrence_of(X2,X1)),inference(split_conjunct,[status(thm)],[256])).
% fof(262, plain,![X133]:![X134]:((~(leaf_occ(X133,X134))|?[X135]:((occurrence_of(X134,X135)&subactivity_occurrence(X133,X134))&leaf(X133,X135)))&(![X135]:((~(occurrence_of(X134,X135))|~(subactivity_occurrence(X133,X134)))|~(leaf(X133,X135)))|leaf_occ(X133,X134))),inference(fof_nnf,[status(thm)],[47])).
% fof(263, plain,![X136]:![X137]:((~(leaf_occ(X136,X137))|?[X138]:((occurrence_of(X137,X138)&subactivity_occurrence(X136,X137))&leaf(X136,X138)))&(![X139]:((~(occurrence_of(X137,X139))|~(subactivity_occurrence(X136,X137)))|~(leaf(X136,X139)))|leaf_occ(X136,X137))),inference(variable_rename,[status(thm)],[262])).
% fof(264, plain,![X136]:![X137]:((~(leaf_occ(X136,X137))|((occurrence_of(X137,esk14_2(X136,X137))&subactivity_occurrence(X136,X137))&leaf(X136,esk14_2(X136,X137))))&(![X139]:((~(occurrence_of(X137,X139))|~(subactivity_occurrence(X136,X137)))|~(leaf(X136,X139)))|leaf_occ(X136,X137))),inference(skolemize,[status(esa)],[263])).
% fof(265, plain,![X136]:![X137]:![X139]:((((~(occurrence_of(X137,X139))|~(subactivity_occurrence(X136,X137)))|~(leaf(X136,X139)))|leaf_occ(X136,X137))&(~(leaf_occ(X136,X137))|((occurrence_of(X137,esk14_2(X136,X137))&subactivity_occurrence(X136,X137))&leaf(X136,esk14_2(X136,X137))))),inference(shift_quantors,[status(thm)],[264])).
% fof(266, plain,![X136]:![X137]:![X139]:((((~(occurrence_of(X137,X139))|~(subactivity_occurrence(X136,X137)))|~(leaf(X136,X139)))|leaf_occ(X136,X137))&(((occurrence_of(X137,esk14_2(X136,X137))|~(leaf_occ(X136,X137)))&(subactivity_occurrence(X136,X137)|~(leaf_occ(X136,X137))))&(leaf(X136,esk14_2(X136,X137))|~(leaf_occ(X136,X137))))),inference(distribute,[status(thm)],[265])).
% cnf(267,plain,(leaf(X1,esk14_2(X1,X2))|~leaf_occ(X1,X2)),inference(split_conjunct,[status(thm)],[266])).
% cnf(269,plain,(occurrence_of(X2,esk14_2(X1,X2))|~leaf_occ(X1,X2)),inference(split_conjunct,[status(thm)],[266])).
% fof(271, plain,![X136]:![X137]:![X138]:(~(min_precedes(X136,X137,X138))|arboreal(X136)),inference(fof_nnf,[status(thm)],[48])).
% fof(272, plain,![X139]:![X140]:![X141]:(~(min_precedes(X139,X140,X141))|arboreal(X139)),inference(variable_rename,[status(thm)],[271])).
% cnf(273,plain,(arboreal(X1)|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[272])).
% fof(274, plain,![X139]:![X140]:![X141]:(~(min_precedes(X140,X141,X139))|?[X142]:?[X143]:(((subactivity(X142,X139)&subactivity(X143,X139))&atocc(X140,X142))&atocc(X141,X143))),inference(fof_nnf,[status(thm)],[49])).
% fof(275, plain,![X144]:![X145]:![X146]:(~(min_precedes(X145,X146,X144))|?[X147]:?[X148]:(((subactivity(X147,X144)&subactivity(X148,X144))&atocc(X145,X147))&atocc(X146,X148))),inference(variable_rename,[status(thm)],[274])).
% fof(276, plain,![X144]:![X145]:![X146]:(~(min_precedes(X145,X146,X144))|(((subactivity(esk15_3(X144,X145,X146),X144)&subactivity(esk16_3(X144,X145,X146),X144))&atocc(X145,esk15_3(X144,X145,X146)))&atocc(X146,esk16_3(X144,X145,X146)))),inference(skolemize,[status(esa)],[275])).
% fof(277, plain,![X144]:![X145]:![X146]:((((subactivity(esk15_3(X144,X145,X146),X144)|~(min_precedes(X145,X146,X144)))&(subactivity(esk16_3(X144,X145,X146),X144)|~(min_precedes(X145,X146,X144))))&(atocc(X145,esk15_3(X144,X145,X146))|~(min_precedes(X145,X146,X144))))&(atocc(X146,esk16_3(X144,X145,X146))|~(min_precedes(X145,X146,X144)))),inference(distribute,[status(thm)],[276])).
% cnf(278,plain,(atocc(X2,esk16_3(X3,X1,X2))|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[277])).
% fof(291, plain,![X155]:![X156]:((~(leaf(X155,X156))|((root(X155,X156)|?[X157]:min_precedes(X157,X155,X156))&![X158]:~(min_precedes(X155,X158,X156))))&(((~(root(X155,X156))&![X157]:~(min_precedes(X157,X155,X156)))|?[X158]:min_precedes(X155,X158,X156))|leaf(X155,X156))),inference(fof_nnf,[status(thm)],[53])).
% fof(292, plain,![X159]:![X160]:((~(leaf(X159,X160))|((root(X159,X160)|?[X161]:min_precedes(X161,X159,X160))&![X162]:~(min_precedes(X159,X162,X160))))&(((~(root(X159,X160))&![X163]:~(min_precedes(X163,X159,X160)))|?[X164]:min_precedes(X159,X164,X160))|leaf(X159,X160))),inference(variable_rename,[status(thm)],[291])).
% fof(293, plain,![X159]:![X160]:((~(leaf(X159,X160))|((root(X159,X160)|min_precedes(esk17_2(X159,X160),X159,X160))&![X162]:~(min_precedes(X159,X162,X160))))&(((~(root(X159,X160))&![X163]:~(min_precedes(X163,X159,X160)))|min_precedes(X159,esk18_2(X159,X160),X160))|leaf(X159,X160))),inference(skolemize,[status(esa)],[292])).
% fof(294, plain,![X159]:![X160]:![X162]:![X163]:((((~(min_precedes(X163,X159,X160))&~(root(X159,X160)))|min_precedes(X159,esk18_2(X159,X160),X160))|leaf(X159,X160))&((~(min_precedes(X159,X162,X160))&(root(X159,X160)|min_precedes(esk17_2(X159,X160),X159,X160)))|~(leaf(X159,X160)))),inference(shift_quantors,[status(thm)],[293])).
% fof(295, plain,![X159]:![X160]:![X162]:![X163]:((((~(min_precedes(X163,X159,X160))|min_precedes(X159,esk18_2(X159,X160),X160))|leaf(X159,X160))&((~(root(X159,X160))|min_precedes(X159,esk18_2(X159,X160),X160))|leaf(X159,X160)))&((~(min_precedes(X159,X162,X160))|~(leaf(X159,X160)))&((root(X159,X160)|min_precedes(esk17_2(X159,X160),X159,X160))|~(leaf(X159,X160))))),inference(distribute,[status(thm)],[294])).
% cnf(297,plain,(~leaf(X1,X2)|~min_precedes(X1,X3,X2)),inference(split_conjunct,[status(thm)],[295])).
% cnf(299,plain,(leaf(X1,X2)|min_precedes(X1,esk18_2(X1,X2),X2)|~min_precedes(X3,X1,X2)),inference(split_conjunct,[status(thm)],[295])).
% fof(300, plain,![X159]:![X160]:((~(atocc(X159,X160))|?[X161]:((subactivity(X160,X161)&atomic(X161))&occurrence_of(X159,X161)))&(![X161]:((~(subactivity(X160,X161))|~(atomic(X161)))|~(occurrence_of(X159,X161)))|atocc(X159,X160))),inference(fof_nnf,[status(thm)],[54])).
% fof(301, plain,![X162]:![X163]:((~(atocc(X162,X163))|?[X164]:((subactivity(X163,X164)&atomic(X164))&occurrence_of(X162,X164)))&(![X165]:((~(subactivity(X163,X165))|~(atomic(X165)))|~(occurrence_of(X162,X165)))|atocc(X162,X163))),inference(variable_rename,[status(thm)],[300])).
% fof(302, plain,![X162]:![X163]:((~(atocc(X162,X163))|((subactivity(X163,esk19_2(X162,X163))&atomic(esk19_2(X162,X163)))&occurrence_of(X162,esk19_2(X162,X163))))&(![X165]:((~(subactivity(X163,X165))|~(atomic(X165)))|~(occurrence_of(X162,X165)))|atocc(X162,X163))),inference(skolemize,[status(esa)],[301])).
% fof(303, plain,![X162]:![X163]:![X165]:((((~(subactivity(X163,X165))|~(atomic(X165)))|~(occurrence_of(X162,X165)))|atocc(X162,X163))&(~(atocc(X162,X163))|((subactivity(X163,esk19_2(X162,X163))&atomic(esk19_2(X162,X163)))&occurrence_of(X162,esk19_2(X162,X163))))),inference(shift_quantors,[status(thm)],[302])).
% fof(304, plain,![X162]:![X163]:![X165]:((((~(subactivity(X163,X165))|~(atomic(X165)))|~(occurrence_of(X162,X165)))|atocc(X162,X163))&(((subactivity(X163,esk19_2(X162,X163))|~(atocc(X162,X163)))&(atomic(esk19_2(X162,X163))|~(atocc(X162,X163))))&(occurrence_of(X162,esk19_2(X162,X163))|~(atocc(X162,X163))))),inference(distribute,[status(thm)],[303])).
% cnf(305,plain,(occurrence_of(X1,esk19_2(X1,X2))|~atocc(X1,X2)),inference(split_conjunct,[status(thm)],[304])).
% cnf(306,plain,(atomic(esk19_2(X1,X2))|~atocc(X1,X2)),inference(split_conjunct,[status(thm)],[304])).
% cnf(308,plain,(atocc(X1,X2)|~occurrence_of(X1,X3)|~atomic(X3)|~subactivity(X2,X3)),inference(split_conjunct,[status(thm)],[304])).
% cnf(314,plain,(tptp4!=tptp1),inference(split_conjunct,[status(thm)],[56])).
% cnf(317,plain,(tptp1!=tptp3),inference(split_conjunct,[status(thm)],[59])).
% fof(326, negated_conjecture,?[X168]:occurrence_of(X168,tptp0),inference(fof_nnf,[status(thm)],[65])).
% fof(327, negated_conjecture,?[X169]:occurrence_of(X169,tptp0),inference(variable_rename,[status(thm)],[326])).
% fof(328, negated_conjecture,occurrence_of(esk20_0,tptp0),inference(skolemize,[status(esa)],[327])).
% cnf(329,negated_conjecture,(occurrence_of(esk20_0,tptp0)),inference(split_conjunct,[status(thm)],[328])).
% cnf(330,negated_conjecture,(X1=tptp0|~occurrence_of(esk20_0,X1)),inference(spm,[status(thm)],[83,329,theory(equality)])).
% cnf(335,plain,(subactivity(esk7_1(X1),esk7_1(X1))|~activity_occurrence(X1)),inference(spm,[status(thm)],[136,178,theory(equality)])).
% cnf(337,plain,(X1=esk7_1(X2)|~occurrence_of(X2,X1)|~activity_occurrence(X2)),inference(spm,[status(thm)],[83,177,theory(equality)])).
% cnf(354,plain,(activity_occurrence(X1)|~atocc(X1,X2)),inference(spm,[status(thm)],[171,305,theory(equality)])).
% cnf(355,plain,(arboreal(X1)|~atomic(esk19_2(X1,X2))|~atocc(X1,X2)),inference(spm,[status(thm)],[120,305,theory(equality)])).
% cnf(359,plain,(subactivity_occurrence(esk4_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[223,144,theory(equality)])).
% cnf(360,plain,(X1=esk4_1(X2)|~root_occ(X1,X2)|~occurrence_of(X2,X3)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[95,144,theory(equality)])).
% cnf(364,plain,(X1=tptp4|~occurrence_of(esk4_1(X2),X1)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[83,145,theory(equality)])).
% cnf(365,plain,(activity(tptp4)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[172,145,theory(equality)])).
% cnf(396,plain,(min_precedes(esk4_1(X1),esk5_1(X1),tptp0)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[186,141,theory(equality)])).
% cnf(397,plain,(~min_precedes(X2,esk5_1(X1),tptp0)|~min_precedes(esk4_1(X1),X2,tptp0)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[187,141,theory(equality)])).
% cnf(412,plain,(X1=esk5_1(X2)|atomic(X3)|~leaf_occ(X1,X2)|~occurrence_of(X2,X3)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[161,142,theory(equality)])).
% cnf(417,plain,(root_occ(esk13_2(X1,X2),X3)|atomic(X1)|~subactivity_occurrence(esk13_2(X1,X2),X3)|~occurrence_of(X3,X1)|~occurrence_of(X2,X1)),inference(spm,[status(thm)],[225,258,theory(equality)])).
% cnf(446,plain,(esk5_1(X1)=X2|min_precedes(X2,esk5_1(X1),X3)|~arboreal(X2)|~subactivity_occurrence(X2,X1)|~occurrence_of(X1,X3)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[231,142,theory(equality)])).
% cnf(456,plain,(esk4_1(X1)=X2|min_precedes(esk4_1(X1),X2,X3)|~arboreal(X2)|~subactivity_occurrence(X2,X1)|~occurrence_of(X1,X3)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[228,144,theory(equality)])).
% cnf(481,plain,(min_precedes(X1,esk3_2(X1,X2),tptp0)|leaf_occ(X1,X2)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[186,132,theory(equality)])).
% cnf(512,plain,(subactivity_occurrence(X1,X1)|~subactivity(X2,X3)|~occurrence_of(X1,X3)|~occurrence_of(X1,X2)),inference(spm,[status(thm)],[126,127,theory(equality)])).
% cnf(529,negated_conjecture,(esk14_2(X1,esk20_0)=tptp0|~leaf_occ(X1,esk20_0)),inference(spm,[status(thm)],[330,269,theory(equality)])).
% cnf(530,negated_conjecture,(esk10_2(X1,esk20_0)=tptp0|~root_occ(X1,esk20_0)),inference(spm,[status(thm)],[330,224,theory(equality)])).
% cnf(554,plain,(X1=esk7_1(X2)|~occurrence_of(X2,X1)),inference(csr,[status(thm)],[337,171])).
% cnf(558,plain,(tptp3=esk7_1(esk5_1(X1))|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[554,143,theory(equality)])).
% cnf(560,plain,(tptp1=esk7_1(esk3_2(X1,X2))|leaf_occ(X1,X2)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[554,133,theory(equality)])).
% cnf(561,plain,(X1=esk7_1(esk1_3(X1,X2,X3))|~min_precedes(X2,X3,X1)),inference(spm,[status(thm)],[554,102,theory(equality)])).
% cnf(562,plain,(esk19_2(X1,X2)=esk7_1(X1)|~atocc(X1,X2)),inference(spm,[status(thm)],[554,305,theory(equality)])).
% cnf(563,plain,(esk14_2(X1,X2)=esk7_1(X2)|~leaf_occ(X1,X2)),inference(spm,[status(thm)],[554,269,theory(equality)])).
% cnf(570,plain,(activity_occurrence(X1)|~root(X1,X2)),inference(spm,[status(thm)],[354,204,theory(equality)])).
% cnf(602,negated_conjecture,(leaf(X1,tptp0)|~leaf_occ(X1,esk20_0)),inference(spm,[status(thm)],[267,529,theory(equality)])).
% cnf(605,negated_conjecture,(root(X1,tptp0)|~root_occ(X1,esk20_0)),inference(spm,[status(thm)],[222,530,theory(equality)])).
% cnf(610,negated_conjecture,(root(esk4_1(esk20_0),tptp0)|~occurrence_of(esk20_0,tptp0)),inference(spm,[status(thm)],[605,144,theory(equality)])).
% cnf(611,negated_conjecture,(root(esk4_1(esk20_0),tptp0)|$false),inference(rw,[status(thm)],[610,329,theory(equality)])).
% cnf(612,negated_conjecture,(root(esk4_1(esk20_0),tptp0)),inference(cn,[status(thm)],[611,theory(equality)])).
% cnf(614,negated_conjecture,(activity_occurrence(esk4_1(esk20_0))),inference(spm,[status(thm)],[570,612,theory(equality)])).
% cnf(682,plain,(leaf(X1,esk7_1(X2))|~leaf_occ(X1,X2)),inference(spm,[status(thm)],[267,563,theory(equality)])).
% cnf(698,negated_conjecture,(activity(tptp4)),inference(spm,[status(thm)],[365,329,theory(equality)])).
% cnf(704,negated_conjecture,(subactivity(tptp4,tptp4)),inference(spm,[status(thm)],[136,698,theory(equality)])).
% cnf(706,negated_conjecture,(atocc(X1,tptp4)|~occurrence_of(X1,tptp4)|~atomic(tptp4)),inference(spm,[status(thm)],[308,704,theory(equality)])).
% cnf(707,negated_conjecture,(atocc(X1,tptp4)|~occurrence_of(X1,tptp4)|$false),inference(rw,[status(thm)],[706,152,theory(equality)])).
% cnf(708,negated_conjecture,(atocc(X1,tptp4)|~occurrence_of(X1,tptp4)),inference(cn,[status(thm)],[707,theory(equality)])).
% cnf(715,plain,(arboreal(X1)|~atocc(X1,X2)),inference(csr,[status(thm)],[355,306])).
% cnf(716,plain,(arboreal(X1)|~min_precedes(X3,X1,X2)),inference(spm,[status(thm)],[715,278,theory(equality)])).
% cnf(786,plain,(subactivity_occurrence(X1,X2)|~subactivity_occurrence(X1,esk4_1(X2))|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[92,359,theory(equality)])).
% cnf(808,negated_conjecture,(arboreal(X1)|~occurrence_of(X1,tptp4)),inference(spm,[status(thm)],[715,708,theory(equality)])).
% cnf(890,plain,(occurrence_of(X1,esk7_1(X1))|~atocc(X1,X2)),inference(spm,[status(thm)],[305,562,theory(equality)])).
% cnf(896,plain,(occurrence_of(X1,esk7_1(X1))|~root(X1,X2)),inference(spm,[status(thm)],[890,204,theory(equality)])).
% cnf(945,negated_conjecture,(occurrence_of(esk4_1(esk20_0),esk7_1(esk4_1(esk20_0)))),inference(spm,[status(thm)],[896,612,theory(equality)])).
% cnf(955,negated_conjecture,(esk7_1(esk4_1(esk20_0))=tptp4|~occurrence_of(esk20_0,tptp0)),inference(spm,[status(thm)],[364,945,theory(equality)])).
% cnf(962,negated_conjecture,(esk7_1(esk4_1(esk20_0))=tptp4|$false),inference(rw,[status(thm)],[955,329,theory(equality)])).
% cnf(963,negated_conjecture,(esk7_1(esk4_1(esk20_0))=tptp4),inference(cn,[status(thm)],[962,theory(equality)])).
% cnf(977,negated_conjecture,(occurrence_of(esk4_1(esk20_0),tptp4)),inference(rw,[status(thm)],[945,963,theory(equality)])).
% cnf(1115,plain,(~root(esk5_1(X1),tptp0)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[246,396,theory(equality)])).
% cnf(1244,plain,(X1=esk5_1(esk6_2(X1,X2))|atomic(X3)|atomic(X2)|~occurrence_of(esk6_2(X1,X2),tptp0)|~occurrence_of(esk6_2(X1,X2),X3)|~leaf(X1,X2)),inference(spm,[status(thm)],[412,150,theory(equality)])).
% cnf(1314,plain,(esk13_2(X1,X2)=esk4_1(X3)|atomic(X1)|~occurrence_of(X3,tptp0)|~occurrence_of(X3,X4)|~subactivity_occurrence(esk13_2(X1,X2),X3)|~occurrence_of(X3,X1)|~occurrence_of(X2,X1)),inference(spm,[status(thm)],[360,417,theory(equality)])).
% cnf(1411,plain,(leaf(X1,X2)|~leaf_occ(X1,esk1_3(X2,X3,X4))|~min_precedes(X3,X4,X2)),inference(spm,[status(thm)],[682,561,theory(equality)])).
% cnf(1804,plain,(esk5_1(X2)=X1|~min_precedes(esk4_1(X2),X1,tptp0)|~occurrence_of(X2,tptp0)|~arboreal(X1)|~subactivity_occurrence(X1,X2)),inference(spm,[status(thm)],[397,446,theory(equality)])).
% cnf(1989,plain,(leaf(esk5_1(esk1_3(X1,X2,X3)),X1)|~min_precedes(X2,X3,X1)|~occurrence_of(esk1_3(X1,X2,X3),tptp0)),inference(spm,[status(thm)],[1411,142,theory(equality)])).
% cnf(2132,plain,(subactivity_occurrence(X1,X1)|~occurrence_of(X1,esk7_1(X2))|~activity_occurrence(X2)),inference(spm,[status(thm)],[512,335,theory(equality)])).
% cnf(2214,plain,(subactivity_occurrence(X1,X1)|~activity_occurrence(X1)),inference(spm,[status(thm)],[2132,177,theory(equality)])).
% cnf(2227,negated_conjecture,(subactivity_occurrence(esk4_1(esk20_0),esk4_1(esk20_0))),inference(spm,[status(thm)],[2214,614,theory(equality)])).
% cnf(2272,negated_conjecture,(subactivity_occurrence(esk4_1(esk20_0),esk20_0)|~occurrence_of(esk20_0,tptp0)),inference(spm,[status(thm)],[786,2227,theory(equality)])).
% cnf(2277,negated_conjecture,(subactivity_occurrence(esk4_1(esk20_0),esk20_0)|$false),inference(rw,[status(thm)],[2272,329,theory(equality)])).
% cnf(2278,negated_conjecture,(subactivity_occurrence(esk4_1(esk20_0),esk20_0)),inference(cn,[status(thm)],[2277,theory(equality)])).
% cnf(2320,plain,(leaf(esk3_2(X1,X2),tptp0)|min_precedes(esk3_2(X1,X2),esk18_2(esk3_2(X1,X2),tptp0),tptp0)|leaf_occ(X1,X2)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[299,481,theory(equality)])).
% cnf(6799,plain,(esk5_1(esk6_2(X1,X2))=X1|atomic(X2)|~leaf(X1,X2)|~occurrence_of(esk6_2(X1,X2),tptp0)),inference(spm,[status(thm)],[1244,151,theory(equality)])).
% cnf(7322,plain,(esk13_2(X1,X2)=esk4_1(X2)|atomic(X1)|~occurrence_of(X2,tptp0)|~occurrence_of(X2,X3)|~occurrence_of(X2,X1)),inference(spm,[status(thm)],[1314,257,theory(equality)])).
% cnf(8076,plain,(esk5_1(X2)=X1|~min_precedes(esk4_1(X2),X1,tptp0)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(csr,[status(thm)],[1804,716])).
% cnf(8082,plain,(esk5_1(X1)=X2|esk4_1(X1)=X2|~subactivity_occurrence(X2,X1)|~occurrence_of(X1,tptp0)|~arboreal(X2)),inference(spm,[status(thm)],[8076,456,theory(equality)])).
% cnf(8179,negated_conjecture,(esk13_2(X1,esk20_0)=esk4_1(esk20_0)|atomic(X1)|~occurrence_of(esk20_0,tptp0)|~occurrence_of(esk20_0,X1)),inference(spm,[status(thm)],[7322,329,theory(equality)])).
% cnf(8202,negated_conjecture,(esk13_2(X1,esk20_0)=esk4_1(esk20_0)|atomic(X1)|$false|~occurrence_of(esk20_0,X1)),inference(rw,[status(thm)],[8179,329,theory(equality)])).
% cnf(8203,negated_conjecture,(esk13_2(X1,esk20_0)=esk4_1(esk20_0)|atomic(X1)|~occurrence_of(esk20_0,X1)),inference(cn,[status(thm)],[8202,theory(equality)])).
% cnf(8205,negated_conjecture,(root(esk4_1(esk20_0),X1)|atomic(X1)|~occurrence_of(esk20_0,X1)),inference(spm,[status(thm)],[258,8203,theory(equality)])).
% cnf(8708,plain,(esk4_1(esk1_3(X1,X2,X3))=X2|esk5_1(esk1_3(X1,X2,X3))=X2|~arboreal(X2)|~occurrence_of(esk1_3(X1,X2,X3),tptp0)|~min_precedes(X2,X3,X1)),inference(spm,[status(thm)],[8082,101,theory(equality)])).
% cnf(10655,plain,(esk7_1(X1)=tptp3|atomic(X2)|~occurrence_of(esk6_2(X1,X2),tptp0)|~leaf(X1,X2)),inference(spm,[status(thm)],[558,6799,theory(equality)])).
% cnf(10662,plain,(atomic(X2)|~root(X1,tptp0)|~occurrence_of(esk6_2(X1,X2),tptp0)|~leaf(X1,X2)),inference(spm,[status(thm)],[1115,6799,theory(equality)])).
% cnf(10736,plain,(atomic(tptp0)|~root(X1,tptp0)|~leaf(X1,tptp0)),inference(spm,[status(thm)],[10662,151,theory(equality)])).
% cnf(10737,plain,(~root(X1,tptp0)|~leaf(X1,tptp0)),inference(sr,[status(thm)],[10736,79,theory(equality)])).
% cnf(10740,negated_conjecture,(~root(X1,tptp0)|~leaf_occ(X1,esk20_0)),inference(spm,[status(thm)],[10737,602,theory(equality)])).
% cnf(10746,negated_conjecture,(atomic(tptp0)|~leaf_occ(esk4_1(esk20_0),esk20_0)|~occurrence_of(esk20_0,tptp0)),inference(spm,[status(thm)],[10740,8205,theory(equality)])).
% cnf(10750,negated_conjecture,(atomic(tptp0)|~leaf_occ(esk4_1(esk20_0),esk20_0)|$false),inference(rw,[status(thm)],[10746,329,theory(equality)])).
% cnf(10751,negated_conjecture,(atomic(tptp0)|~leaf_occ(esk4_1(esk20_0),esk20_0)),inference(cn,[status(thm)],[10750,theory(equality)])).
% cnf(10752,negated_conjecture,(~leaf_occ(esk4_1(esk20_0),esk20_0)),inference(sr,[status(thm)],[10751,79,theory(equality)])).
% cnf(12342,plain,(esk7_1(X1)=tptp3|atomic(tptp0)|~leaf(X1,tptp0)),inference(spm,[status(thm)],[10655,151,theory(equality)])).
% cnf(12343,plain,(esk7_1(X1)=tptp3|~leaf(X1,tptp0)),inference(sr,[status(thm)],[12342,79,theory(equality)])).
% cnf(12379,plain,(tptp3=tptp1|leaf_occ(X1,X2)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)|~leaf(esk3_2(X1,X2),tptp0)),inference(spm,[status(thm)],[560,12343,theory(equality)])).
% cnf(12466,plain,(leaf_occ(X1,X2)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)|~leaf(esk3_2(X1,X2),tptp0)),inference(sr,[status(thm)],[12379,317,theory(equality)])).
% cnf(19281,plain,(leaf_occ(X1,X2)|min_precedes(esk3_2(X1,X2),esk18_2(esk3_2(X1,X2),tptp0),tptp0)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(csr,[status(thm)],[2320,12466])).
% cnf(105991,plain,(esk4_1(esk1_3(X1,X2,X3))=X2|esk5_1(esk1_3(X1,X2,X3))=X2|~min_precedes(X2,X3,X1)|~occurrence_of(esk1_3(X1,X2,X3),tptp0)),inference(csr,[status(thm)],[8708,273])).
% cnf(106187,plain,(leaf(X2,X1)|esk4_1(esk1_3(X1,X2,X3))=X2|~min_precedes(X2,X3,X1)|~occurrence_of(esk1_3(X1,X2,X3),tptp0)),inference(spm,[status(thm)],[1989,105991,theory(equality)])).
% cnf(143033,plain,(esk4_1(esk1_3(X1,X2,X3))=X2|~min_precedes(X2,X3,X1)|~occurrence_of(esk1_3(X1,X2,X3),tptp0)),inference(csr,[status(thm)],[106187,297])).
% cnf(143147,plain,(X1=tptp4|~occurrence_of(X3,X1)|~occurrence_of(esk1_3(X2,X3,X4),tptp0)|~min_precedes(X3,X4,X2)),inference(spm,[status(thm)],[364,143033,theory(equality)])).
% cnf(144844,plain,(X1=tptp4|~min_precedes(X2,X3,tptp0)|~occurrence_of(X2,X1)),inference(spm,[status(thm)],[143147,102,theory(equality)])).
% cnf(144904,plain,(X1=tptp4|leaf_occ(X2,X3)|~occurrence_of(esk3_2(X2,X3),X1)|~arboreal(X2)|~subactivity_occurrence(X2,X3)|~occurrence_of(X3,tptp0)),inference(spm,[status(thm)],[144844,19281,theory(equality)])).
% cnf(158555,plain,(tptp1=tptp4|leaf_occ(X1,X2)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[144904,133,theory(equality)])).
% cnf(158556,plain,(leaf_occ(X1,X2)|~arboreal(X1)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)),inference(sr,[status(thm)],[158555,314,theory(equality)])).
% cnf(158571,negated_conjecture,(leaf_occ(X1,X2)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,tptp0)|~occurrence_of(X1,tptp4)),inference(spm,[status(thm)],[158556,808,theory(equality)])).
% cnf(158609,negated_conjecture,(~subactivity_occurrence(esk4_1(esk20_0),esk20_0)|~occurrence_of(esk20_0,tptp0)|~occurrence_of(esk4_1(esk20_0),tptp4)),inference(spm,[status(thm)],[10752,158571,theory(equality)])).
% cnf(158832,negated_conjecture,($false|~occurrence_of(esk20_0,tptp0)|~occurrence_of(esk4_1(esk20_0),tptp4)),inference(rw,[status(thm)],[158609,2278,theory(equality)])).
% cnf(158833,negated_conjecture,($false|$false|~occurrence_of(esk4_1(esk20_0),tptp4)),inference(rw,[status(thm)],[158832,329,theory(equality)])).
% cnf(158834,negated_conjecture,($false|$false|$false),inference(rw,[status(thm)],[158833,977,theory(equality)])).
% cnf(158835,negated_conjecture,($false),inference(cn,[status(thm)],[158834,theory(equality)])).
% cnf(158836,negated_conjecture,($false),158835,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 21644
% # ...of these trivial : 45
% # ...subsumed : 17507
% # ...remaining for further processing: 4092
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 657
% # Backward-rewritten : 9
% # Generated clauses : 114361
% # ...of the previous two non-trivial : 108101
% # Contextual simplify-reflections : 19393
% # Paramodulations : 114357
% # Factorizations : 4
% # Equation resolutions : 0
% # Current number of processed clauses: 3426
% # Positive orientable unit clauses: 40
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 32
% # Non-unit-clauses : 3354
% # Current number of unprocessed clauses: 66925
% # ...number of literals in the above : 505717
% # Clause-clause subsumption calls (NU) : 791778
% # Rec. Clause-clause subsumption calls : 279195
% # Unit Clause-clause subsumption calls : 1618
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 6
% # Indexed BW rewrite successes : 6
% # Backwards rewriting index: 1607 leaves, 2.42+/-4.613 terms/leaf
% # Paramod-from index: 560 leaves, 1.20+/-0.763 terms/leaf
% # Paramod-into index: 1296 leaves, 1.93+/-2.994 terms/leaf
% # -------------------------------------------------
% # User time : 8.323 s
% # System time : 0.185 s
% # Total time : 8.508 s
% # Maximum resident set size: 0 pages
% PrfWatch: 11.13 CPU 12.04 WC
% FINAL PrfWatch: 11.13 CPU 12.04 WC
% SZS output end Solution for /tmp/SystemOnTPTP32132/PRO006+3.tptp
%
%------------------------------------------------------------------------------