%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : PRO008+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 : art02.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Wed Dec 29 21:08:35 EST 2010
% Result : Theorem 6.81s
% Output : Solution 6.81s
% 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/SystemOnTPTP12516/PRO008+4.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP12516/PRO008+4.tptp
% SZS output start Solution for /tmp/SystemOnTPTP12516/PRO008+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 12612
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% PrfWatch: 1.92 CPU 2.01 WC
% PrfWatch: 3.91 CPU 4.01 WC
% # Preprocessing time : 0.020 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(4, axiom,![X13]:![X14]:![X15]:![X16]:(((min_precedes(X13,X14,X15)&occurrence_of(X16,X15))&subactivity_occurrence(X14,X16))=>subactivity_occurrence(X13,X16)),file('/tmp/SRASS.s.p', sos_27)).
% fof(6, axiom,![X22]:(occurrence_of(X22,tptp0)=>?[X23]:?[X24]:?[X25]:((((((occurrence_of(X23,tptp3)&root_occ(X23,X22))&occurrence_of(X24,tptp4))&next_subocc(X23,X24,tptp0))&(occurrence_of(X25,tptp1)|occurrence_of(X25,tptp2)))&next_subocc(X24,X25,tptp0))&leaf_occ(X25,X22))),file('/tmp/SRASS.s.p', sos_32)).
% fof(7, axiom,![X26]:![X27]:(root_occ(X26,X27)<=>?[X28]:((occurrence_of(X27,X28)&subactivity_occurrence(X26,X27))&root(X26,X28))),file('/tmp/SRASS.s.p', sos_19)).
% fof(10, axiom,~(tptp1=tptp2),file('/tmp/SRASS.s.p', sos_44)).
% fof(11, axiom,![X29]:![X30]:(leaf_occ(X29,X30)<=>?[X31]:((occurrence_of(X30,X31)&subactivity_occurrence(X29,X30))&leaf(X29,X31))),file('/tmp/SRASS.s.p', sos_18)).
% fof(12, axiom,![X32]:![X33]:![X34]:![X35]:(((occurrence_of(X34,X35)&root_occ(X32,X34))&root_occ(X33,X34))=>X32=X33),file('/tmp/SRASS.s.p', sos_29)).
% fof(13, axiom,![X36]:![X37]:![X38]:![X39]:(((((occurrence_of(X37,X36)&subactivity_occurrence(X38,X37))&leaf_occ(X39,X37))&arboreal(X38))&~(min_precedes(X38,X39,X36)))=>X39=X38),file('/tmp/SRASS.s.p', sos_02)).
% fof(14, axiom,![X40]:![X41]:![X42]:![X43]:(((((occurrence_of(X41,X40)&arboreal(X42))&arboreal(X43))&subactivity_occurrence(X42,X41))&subactivity_occurrence(X43,X41))=>((min_precedes(X42,X43,X40)|min_precedes(X43,X42,X40))|X42=X43)),file('/tmp/SRASS.s.p', sos_04)).
% fof(15, axiom,~(atomic(tptp0)),file('/tmp/SRASS.s.p', sos_34)).
% fof(16, axiom,atomic(tptp1),file('/tmp/SRASS.s.p', sos_36)).
% fof(17, axiom,atomic(tptp2),file('/tmp/SRASS.s.p', sos_37)).
% fof(19, axiom,![X44]:![X45]:![X46]:((occurrence_of(X44,X45)&occurrence_of(X44,X46))=>X45=X46),file('/tmp/SRASS.s.p', sos_08)).
% fof(23, axiom,![X52]:![X53]:![X54]:(min_precedes(X52,X53,X54)=>?[X55]:(root(X55,X54)&min_precedes(X55,X53,X54))),file('/tmp/SRASS.s.p', sos_23)).
% fof(25, axiom,![X59]:![X60]:![X61]:(next_subocc(X59,X60,X61)<=>(min_precedes(X59,X60,X61)&~(?[X62]:(min_precedes(X59,X62,X61)&min_precedes(X62,X60,X61))))),file('/tmp/SRASS.s.p', sos_26)).
% fof(27, axiom,![X67]:![X68]:((leaf(X67,X68)&~(atomic(X68)))=>?[X69]:(occurrence_of(X69,X68)&leaf_occ(X67,X69))),file('/tmp/SRASS.s.p', sos_07)).
% fof(28, axiom,![X70]:![X71]:((occurrence_of(X71,X70)&~(atomic(X70)))=>?[X72]:(root(X72,X70)&subactivity_occurrence(X72,X71))),file('/tmp/SRASS.s.p', sos)).
% fof(29, axiom,![X73]:![X74]:![X75]:![X76]:((((occurrence_of(X75,X76)&~(atomic(X76)))&leaf_occ(X73,X75))&leaf_occ(X74,X75))=>X73=X74),file('/tmp/SRASS.s.p', sos_28)).
% fof(31, axiom,~(tptp4=tptp1),file('/tmp/SRASS.s.p', sos_40)).
% fof(32, axiom,~(tptp4=tptp2),file('/tmp/SRASS.s.p', sos_41)).
% fof(33, axiom,![X77]:![X78]:(occurrence_of(X77,X78)=>(arboreal(X77)<=>atomic(X78))),file('/tmp/SRASS.s.p', sos_16)).
% fof(37, axiom,atomic(tptp4),file('/tmp/SRASS.s.p', sos_35)).
% fof(41, axiom,![X94]:![X95]:(occurrence_of(X95,X94)=>(activity(X94)&activity_occurrence(X95))),file('/tmp/SRASS.s.p', sos_03)).
% fof(42, axiom,![X96]:(activity_occurrence(X96)=>?[X97]:(activity(X97)&occurrence_of(X96,X97))),file('/tmp/SRASS.s.p', sos_12)).
% fof(46, conjecture,![X106]:(occurrence_of(X106,tptp0)=>?[X107]:?[X108]:((((((occurrence_of(X107,tptp3)&root_occ(X107,X106))&(occurrence_of(X108,tptp1)|occurrence_of(X108,tptp2)))&min_precedes(X107,X108,tptp0))&leaf_occ(X108,X106))&(occurrence_of(X108,tptp1)=>~(?[X109]:((occurrence_of(X109,tptp2)&subactivity_occurrence(X109,X106))&min_precedes(X107,X109,tptp0)))))&(occurrence_of(X108,tptp2)=>~(?[X110]:((occurrence_of(X110,tptp1)&subactivity_occurrence(X110,X106))&min_precedes(X107,X110,tptp0)))))),file('/tmp/SRASS.s.p', goals)).
% fof(47, negated_conjecture,~(![X106]:(occurrence_of(X106,tptp0)=>?[X107]:?[X108]:((((((occurrence_of(X107,tptp3)&root_occ(X107,X106))&(occurrence_of(X108,tptp1)|occurrence_of(X108,tptp2)))&min_precedes(X107,X108,tptp0))&leaf_occ(X108,X106))&(occurrence_of(X108,tptp1)=>~(?[X109]:((occurrence_of(X109,tptp2)&subactivity_occurrence(X109,X106))&min_precedes(X107,X109,tptp0)))))&(occurrence_of(X108,tptp2)=>~(?[X110]:((occurrence_of(X110,tptp1)&subactivity_occurrence(X110,X106))&min_precedes(X107,X110,tptp0))))))),inference(assume_negation,[status(cth)],[46])).
% fof(48, plain,![X36]:![X37]:![X38]:![X39]:(((((occurrence_of(X37,X36)&subactivity_occurrence(X38,X37))&leaf_occ(X39,X37))&arboreal(X38))&~(min_precedes(X38,X39,X36)))=>X39=X38),inference(fof_simplification,[status(thm)],[13,theory(equality)])).
% fof(49, plain,~(atomic(tptp0)),inference(fof_simplification,[status(thm)],[15,theory(equality)])).
% fof(51, plain,![X67]:![X68]:((leaf(X67,X68)&~(atomic(X68)))=>?[X69]:(occurrence_of(X69,X68)&leaf_occ(X67,X69))),inference(fof_simplification,[status(thm)],[27,theory(equality)])).
% fof(52, plain,![X70]:![X71]:((occurrence_of(X71,X70)&~(atomic(X70)))=>?[X72]:(root(X72,X70)&subactivity_occurrence(X72,X71))),inference(fof_simplification,[status(thm)],[28,theory(equality)])).
% fof(53, plain,![X73]:![X74]:![X75]:![X76]:((((occurrence_of(X75,X76)&~(atomic(X76)))&leaf_occ(X73,X75))&leaf_occ(X74,X75))=>X73=X74),inference(fof_simplification,[status(thm)],[29,theory(equality)])).
% fof(70, plain,![X13]:![X14]:![X15]:![X16]:(((~(min_precedes(X13,X14,X15))|~(occurrence_of(X16,X15)))|~(subactivity_occurrence(X14,X16)))|subactivity_occurrence(X13,X16)),inference(fof_nnf,[status(thm)],[4])).
% fof(71, plain,![X17]:![X18]:![X19]:![X20]:(((~(min_precedes(X17,X18,X19))|~(occurrence_of(X20,X19)))|~(subactivity_occurrence(X18,X20)))|subactivity_occurrence(X17,X20)),inference(variable_rename,[status(thm)],[70])).
% cnf(72,plain,(subactivity_occurrence(X1,X2)|~subactivity_occurrence(X3,X2)|~occurrence_of(X2,X4)|~min_precedes(X1,X3,X4)),inference(split_conjunct,[status(thm)],[71])).
% fof(76, plain,![X22]:(~(occurrence_of(X22,tptp0))|?[X23]:?[X24]:?[X25]:((((((occurrence_of(X23,tptp3)&root_occ(X23,X22))&occurrence_of(X24,tptp4))&next_subocc(X23,X24,tptp0))&(occurrence_of(X25,tptp1)|occurrence_of(X25,tptp2)))&next_subocc(X24,X25,tptp0))&leaf_occ(X25,X22))),inference(fof_nnf,[status(thm)],[6])).
% fof(77, plain,![X26]:(~(occurrence_of(X26,tptp0))|?[X27]:?[X28]:?[X29]:((((((occurrence_of(X27,tptp3)&root_occ(X27,X26))&occurrence_of(X28,tptp4))&next_subocc(X27,X28,tptp0))&(occurrence_of(X29,tptp1)|occurrence_of(X29,tptp2)))&next_subocc(X28,X29,tptp0))&leaf_occ(X29,X26))),inference(variable_rename,[status(thm)],[76])).
% fof(78, plain,![X26]:(~(occurrence_of(X26,tptp0))|((((((occurrence_of(esk2_1(X26),tptp3)&root_occ(esk2_1(X26),X26))&occurrence_of(esk3_1(X26),tptp4))&next_subocc(esk2_1(X26),esk3_1(X26),tptp0))&(occurrence_of(esk4_1(X26),tptp1)|occurrence_of(esk4_1(X26),tptp2)))&next_subocc(esk3_1(X26),esk4_1(X26),tptp0))&leaf_occ(esk4_1(X26),X26))),inference(skolemize,[status(esa)],[77])).
% fof(79, plain,![X26]:(((((((occurrence_of(esk2_1(X26),tptp3)|~(occurrence_of(X26,tptp0)))&(root_occ(esk2_1(X26),X26)|~(occurrence_of(X26,tptp0))))&(occurrence_of(esk3_1(X26),tptp4)|~(occurrence_of(X26,tptp0))))&(next_subocc(esk2_1(X26),esk3_1(X26),tptp0)|~(occurrence_of(X26,tptp0))))&((occurrence_of(esk4_1(X26),tptp1)|occurrence_of(esk4_1(X26),tptp2))|~(occurrence_of(X26,tptp0))))&(next_subocc(esk3_1(X26),esk4_1(X26),tptp0)|~(occurrence_of(X26,tptp0))))&(leaf_occ(esk4_1(X26),X26)|~(occurrence_of(X26,tptp0)))),inference(distribute,[status(thm)],[78])).
% cnf(80,plain,(leaf_occ(esk4_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[79])).
% cnf(81,plain,(next_subocc(esk3_1(X1),esk4_1(X1),tptp0)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[79])).
% cnf(82,plain,(occurrence_of(esk4_1(X1),tptp2)|occurrence_of(esk4_1(X1),tptp1)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[79])).
% cnf(83,plain,(next_subocc(esk2_1(X1),esk3_1(X1),tptp0)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[79])).
% cnf(84,plain,(occurrence_of(esk3_1(X1),tptp4)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[79])).
% cnf(85,plain,(root_occ(esk2_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[79])).
% cnf(86,plain,(occurrence_of(esk2_1(X1),tptp3)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[79])).
% fof(87, plain,![X26]:![X27]:((~(root_occ(X26,X27))|?[X28]:((occurrence_of(X27,X28)&subactivity_occurrence(X26,X27))&root(X26,X28)))&(![X28]:((~(occurrence_of(X27,X28))|~(subactivity_occurrence(X26,X27)))|~(root(X26,X28)))|root_occ(X26,X27))),inference(fof_nnf,[status(thm)],[7])).
% fof(88, plain,![X29]:![X30]:((~(root_occ(X29,X30))|?[X31]:((occurrence_of(X30,X31)&subactivity_occurrence(X29,X30))&root(X29,X31)))&(![X32]:((~(occurrence_of(X30,X32))|~(subactivity_occurrence(X29,X30)))|~(root(X29,X32)))|root_occ(X29,X30))),inference(variable_rename,[status(thm)],[87])).
% fof(89, plain,![X29]:![X30]:((~(root_occ(X29,X30))|((occurrence_of(X30,esk5_2(X29,X30))&subactivity_occurrence(X29,X30))&root(X29,esk5_2(X29,X30))))&(![X32]:((~(occurrence_of(X30,X32))|~(subactivity_occurrence(X29,X30)))|~(root(X29,X32)))|root_occ(X29,X30))),inference(skolemize,[status(esa)],[88])).
% fof(90, plain,![X29]:![X30]:![X32]:((((~(occurrence_of(X30,X32))|~(subactivity_occurrence(X29,X30)))|~(root(X29,X32)))|root_occ(X29,X30))&(~(root_occ(X29,X30))|((occurrence_of(X30,esk5_2(X29,X30))&subactivity_occurrence(X29,X30))&root(X29,esk5_2(X29,X30))))),inference(shift_quantors,[status(thm)],[89])).
% fof(91, plain,![X29]:![X30]:![X32]:((((~(occurrence_of(X30,X32))|~(subactivity_occurrence(X29,X30)))|~(root(X29,X32)))|root_occ(X29,X30))&(((occurrence_of(X30,esk5_2(X29,X30))|~(root_occ(X29,X30)))&(subactivity_occurrence(X29,X30)|~(root_occ(X29,X30))))&(root(X29,esk5_2(X29,X30))|~(root_occ(X29,X30))))),inference(distribute,[status(thm)],[90])).
% cnf(95,plain,(root_occ(X1,X2)|~root(X1,X3)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,X3)),inference(split_conjunct,[status(thm)],[91])).
% cnf(98,plain,(tptp1!=tptp2),inference(split_conjunct,[status(thm)],[10])).
% fof(99, plain,![X29]:![X30]:((~(leaf_occ(X29,X30))|?[X31]:((occurrence_of(X30,X31)&subactivity_occurrence(X29,X30))&leaf(X29,X31)))&(![X31]:((~(occurrence_of(X30,X31))|~(subactivity_occurrence(X29,X30)))|~(leaf(X29,X31)))|leaf_occ(X29,X30))),inference(fof_nnf,[status(thm)],[11])).
% fof(100, plain,![X32]:![X33]:((~(leaf_occ(X32,X33))|?[X34]:((occurrence_of(X33,X34)&subactivity_occurrence(X32,X33))&leaf(X32,X34)))&(![X35]:((~(occurrence_of(X33,X35))|~(subactivity_occurrence(X32,X33)))|~(leaf(X32,X35)))|leaf_occ(X32,X33))),inference(variable_rename,[status(thm)],[99])).
% fof(101, plain,![X32]:![X33]:((~(leaf_occ(X32,X33))|((occurrence_of(X33,esk6_2(X32,X33))&subactivity_occurrence(X32,X33))&leaf(X32,esk6_2(X32,X33))))&(![X35]:((~(occurrence_of(X33,X35))|~(subactivity_occurrence(X32,X33)))|~(leaf(X32,X35)))|leaf_occ(X32,X33))),inference(skolemize,[status(esa)],[100])).
% fof(102, plain,![X32]:![X33]:![X35]:((((~(occurrence_of(X33,X35))|~(subactivity_occurrence(X32,X33)))|~(leaf(X32,X35)))|leaf_occ(X32,X33))&(~(leaf_occ(X32,X33))|((occurrence_of(X33,esk6_2(X32,X33))&subactivity_occurrence(X32,X33))&leaf(X32,esk6_2(X32,X33))))),inference(shift_quantors,[status(thm)],[101])).
% fof(103, plain,![X32]:![X33]:![X35]:((((~(occurrence_of(X33,X35))|~(subactivity_occurrence(X32,X33)))|~(leaf(X32,X35)))|leaf_occ(X32,X33))&(((occurrence_of(X33,esk6_2(X32,X33))|~(leaf_occ(X32,X33)))&(subactivity_occurrence(X32,X33)|~(leaf_occ(X32,X33))))&(leaf(X32,esk6_2(X32,X33))|~(leaf_occ(X32,X33))))),inference(distribute,[status(thm)],[102])).
% cnf(104,plain,(leaf(X1,esk6_2(X1,X2))|~leaf_occ(X1,X2)),inference(split_conjunct,[status(thm)],[103])).
% cnf(105,plain,(subactivity_occurrence(X1,X2)|~leaf_occ(X1,X2)),inference(split_conjunct,[status(thm)],[103])).
% cnf(106,plain,(occurrence_of(X2,esk6_2(X1,X2))|~leaf_occ(X1,X2)),inference(split_conjunct,[status(thm)],[103])).
% fof(108, plain,![X32]:![X33]:![X34]:![X35]:(((~(occurrence_of(X34,X35))|~(root_occ(X32,X34)))|~(root_occ(X33,X34)))|X32=X33),inference(fof_nnf,[status(thm)],[12])).
% fof(109, plain,![X36]:![X37]:![X38]:![X39]:(((~(occurrence_of(X38,X39))|~(root_occ(X36,X38)))|~(root_occ(X37,X38)))|X36=X37),inference(variable_rename,[status(thm)],[108])).
% cnf(110,plain,(X1=X2|~root_occ(X2,X3)|~root_occ(X1,X3)|~occurrence_of(X3,X4)),inference(split_conjunct,[status(thm)],[109])).
% fof(111, plain,![X36]:![X37]:![X38]:![X39]:(((((~(occurrence_of(X37,X36))|~(subactivity_occurrence(X38,X37)))|~(leaf_occ(X39,X37)))|~(arboreal(X38)))|min_precedes(X38,X39,X36))|X39=X38),inference(fof_nnf,[status(thm)],[48])).
% fof(112, plain,![X40]:![X41]:![X42]:![X43]:(((((~(occurrence_of(X41,X40))|~(subactivity_occurrence(X42,X41)))|~(leaf_occ(X43,X41)))|~(arboreal(X42)))|min_precedes(X42,X43,X40))|X43=X42),inference(variable_rename,[status(thm)],[111])).
% cnf(113,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)],[112])).
% fof(114, plain,![X40]:![X41]:![X42]:![X43]:(((((~(occurrence_of(X41,X40))|~(arboreal(X42)))|~(arboreal(X43)))|~(subactivity_occurrence(X42,X41)))|~(subactivity_occurrence(X43,X41)))|((min_precedes(X42,X43,X40)|min_precedes(X43,X42,X40))|X42=X43)),inference(fof_nnf,[status(thm)],[14])).
% fof(115, plain,![X44]:![X45]:![X46]:![X47]:(((((~(occurrence_of(X45,X44))|~(arboreal(X46)))|~(arboreal(X47)))|~(subactivity_occurrence(X46,X45)))|~(subactivity_occurrence(X47,X45)))|((min_precedes(X46,X47,X44)|min_precedes(X47,X46,X44))|X46=X47)),inference(variable_rename,[status(thm)],[114])).
% cnf(116,plain,(X1=X2|min_precedes(X2,X1,X3)|min_precedes(X1,X2,X3)|~subactivity_occurrence(X2,X4)|~subactivity_occurrence(X1,X4)|~arboreal(X2)|~arboreal(X1)|~occurrence_of(X4,X3)),inference(split_conjunct,[status(thm)],[115])).
% cnf(117,plain,(~atomic(tptp0)),inference(split_conjunct,[status(thm)],[49])).
% cnf(118,plain,(atomic(tptp1)),inference(split_conjunct,[status(thm)],[16])).
% cnf(119,plain,(atomic(tptp2)),inference(split_conjunct,[status(thm)],[17])).
% fof(121, plain,![X44]:![X45]:![X46]:((~(occurrence_of(X44,X45))|~(occurrence_of(X44,X46)))|X45=X46),inference(fof_nnf,[status(thm)],[19])).
% fof(122, plain,![X47]:![X48]:![X49]:((~(occurrence_of(X47,X48))|~(occurrence_of(X47,X49)))|X48=X49),inference(variable_rename,[status(thm)],[121])).
% cnf(123,plain,(X1=X2|~occurrence_of(X3,X2)|~occurrence_of(X3,X1)),inference(split_conjunct,[status(thm)],[122])).
% fof(133, plain,![X52]:![X53]:![X54]:(~(min_precedes(X52,X53,X54))|?[X55]:(root(X55,X54)&min_precedes(X55,X53,X54))),inference(fof_nnf,[status(thm)],[23])).
% fof(134, plain,![X56]:![X57]:![X58]:(~(min_precedes(X56,X57,X58))|?[X59]:(root(X59,X58)&min_precedes(X59,X57,X58))),inference(variable_rename,[status(thm)],[133])).
% fof(135, plain,![X56]:![X57]:![X58]:(~(min_precedes(X56,X57,X58))|(root(esk7_3(X56,X57,X58),X58)&min_precedes(esk7_3(X56,X57,X58),X57,X58))),inference(skolemize,[status(esa)],[134])).
% fof(136, plain,![X56]:![X57]:![X58]:((root(esk7_3(X56,X57,X58),X58)|~(min_precedes(X56,X57,X58)))&(min_precedes(esk7_3(X56,X57,X58),X57,X58)|~(min_precedes(X56,X57,X58)))),inference(distribute,[status(thm)],[135])).
% cnf(137,plain,(min_precedes(esk7_3(X1,X2,X3),X2,X3)|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[136])).
% cnf(138,plain,(root(esk7_3(X1,X2,X3),X3)|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[136])).
% fof(142, plain,![X59]:![X60]:![X61]:((~(next_subocc(X59,X60,X61))|(min_precedes(X59,X60,X61)&![X62]:(~(min_precedes(X59,X62,X61))|~(min_precedes(X62,X60,X61)))))&((~(min_precedes(X59,X60,X61))|?[X62]:(min_precedes(X59,X62,X61)&min_precedes(X62,X60,X61)))|next_subocc(X59,X60,X61))),inference(fof_nnf,[status(thm)],[25])).
% fof(143, plain,![X63]:![X64]:![X65]:((~(next_subocc(X63,X64,X65))|(min_precedes(X63,X64,X65)&![X66]:(~(min_precedes(X63,X66,X65))|~(min_precedes(X66,X64,X65)))))&((~(min_precedes(X63,X64,X65))|?[X67]:(min_precedes(X63,X67,X65)&min_precedes(X67,X64,X65)))|next_subocc(X63,X64,X65))),inference(variable_rename,[status(thm)],[142])).
% fof(144, plain,![X63]:![X64]:![X65]:((~(next_subocc(X63,X64,X65))|(min_precedes(X63,X64,X65)&![X66]:(~(min_precedes(X63,X66,X65))|~(min_precedes(X66,X64,X65)))))&((~(min_precedes(X63,X64,X65))|(min_precedes(X63,esk8_3(X63,X64,X65),X65)&min_precedes(esk8_3(X63,X64,X65),X64,X65)))|next_subocc(X63,X64,X65))),inference(skolemize,[status(esa)],[143])).
% fof(145, plain,![X63]:![X64]:![X65]:![X66]:((((~(min_precedes(X63,X66,X65))|~(min_precedes(X66,X64,X65)))&min_precedes(X63,X64,X65))|~(next_subocc(X63,X64,X65)))&((~(min_precedes(X63,X64,X65))|(min_precedes(X63,esk8_3(X63,X64,X65),X65)&min_precedes(esk8_3(X63,X64,X65),X64,X65)))|next_subocc(X63,X64,X65))),inference(shift_quantors,[status(thm)],[144])).
% fof(146, plain,![X63]:![X64]:![X65]:![X66]:((((~(min_precedes(X63,X66,X65))|~(min_precedes(X66,X64,X65)))|~(next_subocc(X63,X64,X65)))&(min_precedes(X63,X64,X65)|~(next_subocc(X63,X64,X65))))&(((min_precedes(X63,esk8_3(X63,X64,X65),X65)|~(min_precedes(X63,X64,X65)))|next_subocc(X63,X64,X65))&((min_precedes(esk8_3(X63,X64,X65),X64,X65)|~(min_precedes(X63,X64,X65)))|next_subocc(X63,X64,X65)))),inference(distribute,[status(thm)],[145])).
% cnf(149,plain,(min_precedes(X1,X2,X3)|~next_subocc(X1,X2,X3)),inference(split_conjunct,[status(thm)],[146])).
% cnf(150,plain,(~next_subocc(X1,X2,X3)|~min_precedes(X4,X2,X3)|~min_precedes(X1,X4,X3)),inference(split_conjunct,[status(thm)],[146])).
% fof(154, plain,![X67]:![X68]:((~(leaf(X67,X68))|atomic(X68))|?[X69]:(occurrence_of(X69,X68)&leaf_occ(X67,X69))),inference(fof_nnf,[status(thm)],[51])).
% fof(155, plain,![X70]:![X71]:((~(leaf(X70,X71))|atomic(X71))|?[X72]:(occurrence_of(X72,X71)&leaf_occ(X70,X72))),inference(variable_rename,[status(thm)],[154])).
% fof(156, plain,![X70]:![X71]:((~(leaf(X70,X71))|atomic(X71))|(occurrence_of(esk9_2(X70,X71),X71)&leaf_occ(X70,esk9_2(X70,X71)))),inference(skolemize,[status(esa)],[155])).
% fof(157, plain,![X70]:![X71]:((occurrence_of(esk9_2(X70,X71),X71)|(~(leaf(X70,X71))|atomic(X71)))&(leaf_occ(X70,esk9_2(X70,X71))|(~(leaf(X70,X71))|atomic(X71)))),inference(distribute,[status(thm)],[156])).
% cnf(158,plain,(atomic(X1)|leaf_occ(X2,esk9_2(X2,X1))|~leaf(X2,X1)),inference(split_conjunct,[status(thm)],[157])).
% cnf(159,plain,(atomic(X1)|occurrence_of(esk9_2(X2,X1),X1)|~leaf(X2,X1)),inference(split_conjunct,[status(thm)],[157])).
% fof(160, plain,![X70]:![X71]:((~(occurrence_of(X71,X70))|atomic(X70))|?[X72]:(root(X72,X70)&subactivity_occurrence(X72,X71))),inference(fof_nnf,[status(thm)],[52])).
% fof(161, plain,![X73]:![X74]:((~(occurrence_of(X74,X73))|atomic(X73))|?[X75]:(root(X75,X73)&subactivity_occurrence(X75,X74))),inference(variable_rename,[status(thm)],[160])).
% fof(162, plain,![X73]:![X74]:((~(occurrence_of(X74,X73))|atomic(X73))|(root(esk10_2(X73,X74),X73)&subactivity_occurrence(esk10_2(X73,X74),X74))),inference(skolemize,[status(esa)],[161])).
% fof(163, plain,![X73]:![X74]:((root(esk10_2(X73,X74),X73)|(~(occurrence_of(X74,X73))|atomic(X73)))&(subactivity_occurrence(esk10_2(X73,X74),X74)|(~(occurrence_of(X74,X73))|atomic(X73)))),inference(distribute,[status(thm)],[162])).
% cnf(164,plain,(atomic(X1)|subactivity_occurrence(esk10_2(X1,X2),X2)|~occurrence_of(X2,X1)),inference(split_conjunct,[status(thm)],[163])).
% cnf(165,plain,(atomic(X1)|root(esk10_2(X1,X2),X1)|~occurrence_of(X2,X1)),inference(split_conjunct,[status(thm)],[163])).
% fof(166, plain,![X73]:![X74]:![X75]:![X76]:((((~(occurrence_of(X75,X76))|atomic(X76))|~(leaf_occ(X73,X75)))|~(leaf_occ(X74,X75)))|X73=X74),inference(fof_nnf,[status(thm)],[53])).
% fof(167, plain,![X77]:![X78]:![X79]:![X80]:((((~(occurrence_of(X79,X80))|atomic(X80))|~(leaf_occ(X77,X79)))|~(leaf_occ(X78,X79)))|X77=X78),inference(variable_rename,[status(thm)],[166])).
% cnf(168,plain,(X1=X2|atomic(X4)|~leaf_occ(X2,X3)|~leaf_occ(X1,X3)|~occurrence_of(X3,X4)),inference(split_conjunct,[status(thm)],[167])).
% cnf(170,plain,(tptp4!=tptp1),inference(split_conjunct,[status(thm)],[31])).
% cnf(171,plain,(tptp4!=tptp2),inference(split_conjunct,[status(thm)],[32])).
% fof(172, plain,![X77]:![X78]:(~(occurrence_of(X77,X78))|((~(arboreal(X77))|atomic(X78))&(~(atomic(X78))|arboreal(X77)))),inference(fof_nnf,[status(thm)],[33])).
% fof(173, plain,![X79]:![X80]:(~(occurrence_of(X79,X80))|((~(arboreal(X79))|atomic(X80))&(~(atomic(X80))|arboreal(X79)))),inference(variable_rename,[status(thm)],[172])).
% fof(174, plain,![X79]:![X80]:(((~(arboreal(X79))|atomic(X80))|~(occurrence_of(X79,X80)))&((~(atomic(X80))|arboreal(X79))|~(occurrence_of(X79,X80)))),inference(distribute,[status(thm)],[173])).
% cnf(175,plain,(arboreal(X1)|~occurrence_of(X1,X2)|~atomic(X2)),inference(split_conjunct,[status(thm)],[174])).
% cnf(192,plain,(atomic(tptp4)),inference(split_conjunct,[status(thm)],[37])).
% fof(204, plain,![X94]:![X95]:(~(occurrence_of(X95,X94))|(activity(X94)&activity_occurrence(X95))),inference(fof_nnf,[status(thm)],[41])).
% fof(205, plain,![X96]:![X97]:(~(occurrence_of(X97,X96))|(activity(X96)&activity_occurrence(X97))),inference(variable_rename,[status(thm)],[204])).
% fof(206, plain,![X96]:![X97]:((activity(X96)|~(occurrence_of(X97,X96)))&(activity_occurrence(X97)|~(occurrence_of(X97,X96)))),inference(distribute,[status(thm)],[205])).
% cnf(207,plain,(activity_occurrence(X1)|~occurrence_of(X1,X2)),inference(split_conjunct,[status(thm)],[206])).
% fof(209, plain,![X96]:(~(activity_occurrence(X96))|?[X97]:(activity(X97)&occurrence_of(X96,X97))),inference(fof_nnf,[status(thm)],[42])).
% fof(210, plain,![X98]:(~(activity_occurrence(X98))|?[X99]:(activity(X99)&occurrence_of(X98,X99))),inference(variable_rename,[status(thm)],[209])).
% fof(211, plain,![X98]:(~(activity_occurrence(X98))|(activity(esk13_1(X98))&occurrence_of(X98,esk13_1(X98)))),inference(skolemize,[status(esa)],[210])).
% fof(212, plain,![X98]:((activity(esk13_1(X98))|~(activity_occurrence(X98)))&(occurrence_of(X98,esk13_1(X98))|~(activity_occurrence(X98)))),inference(distribute,[status(thm)],[211])).
% cnf(213,plain,(occurrence_of(X1,esk13_1(X1))|~activity_occurrence(X1)),inference(split_conjunct,[status(thm)],[212])).
% fof(236, negated_conjecture,?[X106]:(occurrence_of(X106,tptp0)&![X107]:![X108]:((((((~(occurrence_of(X107,tptp3))|~(root_occ(X107,X106)))|(~(occurrence_of(X108,tptp1))&~(occurrence_of(X108,tptp2))))|~(min_precedes(X107,X108,tptp0)))|~(leaf_occ(X108,X106)))|(occurrence_of(X108,tptp1)&?[X109]:((occurrence_of(X109,tptp2)&subactivity_occurrence(X109,X106))&min_precedes(X107,X109,tptp0))))|(occurrence_of(X108,tptp2)&?[X110]:((occurrence_of(X110,tptp1)&subactivity_occurrence(X110,X106))&min_precedes(X107,X110,tptp0))))),inference(fof_nnf,[status(thm)],[47])).
% fof(237, negated_conjecture,?[X111]:(occurrence_of(X111,tptp0)&![X112]:![X113]:((((((~(occurrence_of(X112,tptp3))|~(root_occ(X112,X111)))|(~(occurrence_of(X113,tptp1))&~(occurrence_of(X113,tptp2))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,X111)))|(occurrence_of(X113,tptp1)&?[X114]:((occurrence_of(X114,tptp2)&subactivity_occurrence(X114,X111))&min_precedes(X112,X114,tptp0))))|(occurrence_of(X113,tptp2)&?[X115]:((occurrence_of(X115,tptp1)&subactivity_occurrence(X115,X111))&min_precedes(X112,X115,tptp0))))),inference(variable_rename,[status(thm)],[236])).
% fof(238, negated_conjecture,(occurrence_of(esk16_0,tptp0)&![X112]:![X113]:((((((~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0)))|(~(occurrence_of(X113,tptp1))&~(occurrence_of(X113,tptp2))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0)))|(occurrence_of(X113,tptp1)&((occurrence_of(esk17_2(X112,X113),tptp2)&subactivity_occurrence(esk17_2(X112,X113),esk16_0))&min_precedes(X112,esk17_2(X112,X113),tptp0))))|(occurrence_of(X113,tptp2)&((occurrence_of(esk18_2(X112,X113),tptp1)&subactivity_occurrence(esk18_2(X112,X113),esk16_0))&min_precedes(X112,esk18_2(X112,X113),tptp0))))),inference(skolemize,[status(esa)],[237])).
% fof(239, negated_conjecture,![X112]:![X113]:(((((((~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0)))|(~(occurrence_of(X113,tptp1))&~(occurrence_of(X113,tptp2))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0)))|(occurrence_of(X113,tptp1)&((occurrence_of(esk17_2(X112,X113),tptp2)&subactivity_occurrence(esk17_2(X112,X113),esk16_0))&min_precedes(X112,esk17_2(X112,X113),tptp0))))|(occurrence_of(X113,tptp2)&((occurrence_of(esk18_2(X112,X113),tptp1)&subactivity_occurrence(esk18_2(X112,X113),esk16_0))&min_precedes(X112,esk18_2(X112,X113),tptp0))))&occurrence_of(esk16_0,tptp0)),inference(shift_quantors,[status(thm)],[238])).
% fof(240, negated_conjecture,![X112]:![X113]:(((((occurrence_of(X113,tptp2)|(occurrence_of(X113,tptp1)|(((~(occurrence_of(X113,tptp1))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0)))))&(((occurrence_of(esk18_2(X112,X113),tptp1)|(occurrence_of(X113,tptp1)|(((~(occurrence_of(X113,tptp1))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0)))))&(subactivity_occurrence(esk18_2(X112,X113),esk16_0)|(occurrence_of(X113,tptp1)|(((~(occurrence_of(X113,tptp1))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0))))))&(min_precedes(X112,esk18_2(X112,X113),tptp0)|(occurrence_of(X113,tptp1)|(((~(occurrence_of(X113,tptp1))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0)))))))&((((occurrence_of(X113,tptp2)|(occurrence_of(esk17_2(X112,X113),tptp2)|(((~(occurrence_of(X113,tptp1))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0)))))&(((occurrence_of(esk18_2(X112,X113),tptp1)|(occurrence_of(esk17_2(X112,X113),tptp2)|(((~(occurrence_of(X113,tptp1))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0)))))&(subactivity_occurrence(esk18_2(X112,X113),esk16_0)|(occurrence_of(esk17_2(X112,X113),tptp2)|(((~(occurrence_of(X113,tptp1))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0))))))&(min_precedes(X112,esk18_2(X112,X113),tptp0)|(occurrence_of(esk17_2(X112,X113),tptp2)|(((~(occurrence_of(X113,tptp1))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0)))))))&((occurrence_of(X113,tptp2)|(subactivity_occurrence(esk17_2(X112,X113),esk16_0)|(((~(occurrence_of(X113,tptp1))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0)))))&(((occurrence_of(esk18_2(X112,X113),tptp1)|(subactivity_occurrence(esk17_2(X112,X113),esk16_0)|(((~(occurrence_of(X113,tptp1))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0)))))&(subactivity_occurrence(esk18_2(X112,X113),esk16_0)|(subactivity_occurrence(esk17_2(X112,X113),esk16_0)|(((~(occurrence_of(X113,tptp1))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0))))))&(min_precedes(X112,esk18_2(X112,X113),tptp0)|(subactivity_occurrence(esk17_2(X112,X113),esk16_0)|(((~(occurrence_of(X113,tptp1))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0))))))))&((occurrence_of(X113,tptp2)|(min_precedes(X112,esk17_2(X112,X113),tptp0)|(((~(occurrence_of(X113,tptp1))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0)))))&(((occurrence_of(esk18_2(X112,X113),tptp1)|(min_precedes(X112,esk17_2(X112,X113),tptp0)|(((~(occurrence_of(X113,tptp1))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0)))))&(subactivity_occurrence(esk18_2(X112,X113),esk16_0)|(min_precedes(X112,esk17_2(X112,X113),tptp0)|(((~(occurrence_of(X113,tptp1))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0))))))&(min_precedes(X112,esk18_2(X112,X113),tptp0)|(min_precedes(X112,esk17_2(X112,X113),tptp0)|(((~(occurrence_of(X113,tptp1))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0)))))))))&(((occurrence_of(X113,tptp2)|(occurrence_of(X113,tptp1)|(((~(occurrence_of(X113,tptp2))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0)))))&(((occurrence_of(esk18_2(X112,X113),tptp1)|(occurrence_of(X113,tptp1)|(((~(occurrence_of(X113,tptp2))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0)))))&(subactivity_occurrence(esk18_2(X112,X113),esk16_0)|(occurrence_of(X113,tptp1)|(((~(occurrence_of(X113,tptp2))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0))))))&(min_precedes(X112,esk18_2(X112,X113),tptp0)|(occurrence_of(X113,tptp1)|(((~(occurrence_of(X113,tptp2))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0)))))))&((((occurrence_of(X113,tptp2)|(occurrence_of(esk17_2(X112,X113),tptp2)|(((~(occurrence_of(X113,tptp2))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0)))))&(((occurrence_of(esk18_2(X112,X113),tptp1)|(occurrence_of(esk17_2(X112,X113),tptp2)|(((~(occurrence_of(X113,tptp2))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0)))))&(subactivity_occurrence(esk18_2(X112,X113),esk16_0)|(occurrence_of(esk17_2(X112,X113),tptp2)|(((~(occurrence_of(X113,tptp2))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0))))))&(min_precedes(X112,esk18_2(X112,X113),tptp0)|(occurrence_of(esk17_2(X112,X113),tptp2)|(((~(occurrence_of(X113,tptp2))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0)))))))&((occurrence_of(X113,tptp2)|(subactivity_occurrence(esk17_2(X112,X113),esk16_0)|(((~(occurrence_of(X113,tptp2))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0)))))&(((occurrence_of(esk18_2(X112,X113),tptp1)|(subactivity_occurrence(esk17_2(X112,X113),esk16_0)|(((~(occurrence_of(X113,tptp2))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0)))))&(subactivity_occurrence(esk18_2(X112,X113),esk16_0)|(subactivity_occurrence(esk17_2(X112,X113),esk16_0)|(((~(occurrence_of(X113,tptp2))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0))))))&(min_precedes(X112,esk18_2(X112,X113),tptp0)|(subactivity_occurrence(esk17_2(X112,X113),esk16_0)|(((~(occurrence_of(X113,tptp2))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0))))))))&((occurrence_of(X113,tptp2)|(min_precedes(X112,esk17_2(X112,X113),tptp0)|(((~(occurrence_of(X113,tptp2))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0)))))&(((occurrence_of(esk18_2(X112,X113),tptp1)|(min_precedes(X112,esk17_2(X112,X113),tptp0)|(((~(occurrence_of(X113,tptp2))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0)))))&(subactivity_occurrence(esk18_2(X112,X113),esk16_0)|(min_precedes(X112,esk17_2(X112,X113),tptp0)|(((~(occurrence_of(X113,tptp2))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0))))))&(min_precedes(X112,esk18_2(X112,X113),tptp0)|(min_precedes(X112,esk17_2(X112,X113),tptp0)|(((~(occurrence_of(X113,tptp2))|(~(occurrence_of(X112,tptp3))|~(root_occ(X112,esk16_0))))|~(min_precedes(X112,X113,tptp0)))|~(leaf_occ(X113,esk16_0))))))))))&occurrence_of(esk16_0,tptp0)),inference(distribute,[status(thm)],[239])).
% cnf(241,negated_conjecture,(occurrence_of(esk16_0,tptp0)),inference(split_conjunct,[status(thm)],[240])).
% cnf(254,negated_conjecture,(occurrence_of(X1,tptp1)|min_precedes(X2,esk18_2(X2,X1),tptp0)|~leaf_occ(X1,esk16_0)|~min_precedes(X2,X1,tptp0)|~root_occ(X2,esk16_0)|~occurrence_of(X2,tptp3)|~occurrence_of(X1,tptp2)),inference(split_conjunct,[status(thm)],[240])).
% cnf(255,negated_conjecture,(occurrence_of(X1,tptp1)|subactivity_occurrence(esk18_2(X2,X1),esk16_0)|~leaf_occ(X1,esk16_0)|~min_precedes(X2,X1,tptp0)|~root_occ(X2,esk16_0)|~occurrence_of(X2,tptp3)|~occurrence_of(X1,tptp2)),inference(split_conjunct,[status(thm)],[240])).
% cnf(256,negated_conjecture,(occurrence_of(X1,tptp1)|occurrence_of(esk18_2(X2,X1),tptp1)|~leaf_occ(X1,esk16_0)|~min_precedes(X2,X1,tptp0)|~root_occ(X2,esk16_0)|~occurrence_of(X2,tptp3)|~occurrence_of(X1,tptp2)),inference(split_conjunct,[status(thm)],[240])).
% cnf(261,negated_conjecture,(min_precedes(X2,esk17_2(X2,X1),tptp0)|occurrence_of(X1,tptp2)|~leaf_occ(X1,esk16_0)|~min_precedes(X2,X1,tptp0)|~root_occ(X2,esk16_0)|~occurrence_of(X2,tptp3)|~occurrence_of(X1,tptp1)),inference(split_conjunct,[status(thm)],[240])).
% cnf(265,negated_conjecture,(subactivity_occurrence(esk17_2(X2,X1),esk16_0)|occurrence_of(X1,tptp2)|~leaf_occ(X1,esk16_0)|~min_precedes(X2,X1,tptp0)|~root_occ(X2,esk16_0)|~occurrence_of(X2,tptp3)|~occurrence_of(X1,tptp1)),inference(split_conjunct,[status(thm)],[240])).
% cnf(269,negated_conjecture,(occurrence_of(esk17_2(X2,X1),tptp2)|occurrence_of(X1,tptp2)|~leaf_occ(X1,esk16_0)|~min_precedes(X2,X1,tptp0)|~root_occ(X2,esk16_0)|~occurrence_of(X2,tptp3)|~occurrence_of(X1,tptp1)),inference(split_conjunct,[status(thm)],[240])).
% cnf(276,negated_conjecture,(activity_occurrence(esk16_0)),inference(spm,[status(thm)],[207,241,theory(equality)])).
% cnf(279,negated_conjecture,(occurrence_of(esk2_1(esk16_0),tptp3)),inference(spm,[status(thm)],[86,241,theory(equality)])).
% cnf(280,negated_conjecture,(occurrence_of(esk3_1(esk16_0),tptp4)),inference(spm,[status(thm)],[84,241,theory(equality)])).
% cnf(281,negated_conjecture,(leaf_occ(esk4_1(esk16_0),esk16_0)),inference(spm,[status(thm)],[80,241,theory(equality)])).
% cnf(282,negated_conjecture,(root_occ(esk2_1(esk16_0),esk16_0)),inference(spm,[status(thm)],[85,241,theory(equality)])).
% cnf(288,negated_conjecture,(X1=tptp0|~occurrence_of(esk16_0,X1)),inference(spm,[status(thm)],[123,241,theory(equality)])).
% cnf(289,plain,(X1=esk13_1(X2)|~occurrence_of(X2,X1)|~activity_occurrence(X2)),inference(spm,[status(thm)],[123,213,theory(equality)])).
% cnf(290,negated_conjecture,(next_subocc(esk2_1(esk16_0),esk3_1(esk16_0),tptp0)),inference(spm,[status(thm)],[83,241,theory(equality)])).
% cnf(291,negated_conjecture,(next_subocc(esk3_1(esk16_0),esk4_1(esk16_0),tptp0)),inference(spm,[status(thm)],[81,241,theory(equality)])).
% cnf(292,negated_conjecture,(occurrence_of(esk4_1(esk16_0),tptp2)|occurrence_of(esk4_1(esk16_0),tptp1)),inference(spm,[status(thm)],[82,241,theory(equality)])).
% cnf(293,negated_conjecture,(atomic(tptp0)|subactivity_occurrence(esk10_2(tptp0,esk16_0),esk16_0)),inference(spm,[status(thm)],[164,241,theory(equality)])).
% cnf(294,plain,(atomic(esk13_1(X1))|subactivity_occurrence(esk10_2(esk13_1(X1),X1),X1)|~activity_occurrence(X1)),inference(spm,[status(thm)],[164,213,theory(equality)])).
% cnf(295,negated_conjecture,(subactivity_occurrence(esk10_2(tptp0,esk16_0),esk16_0)),inference(sr,[status(thm)],[293,117,theory(equality)])).
% cnf(296,negated_conjecture,(atomic(tptp0)|root(esk10_2(tptp0,esk16_0),tptp0)),inference(spm,[status(thm)],[165,241,theory(equality)])).
% cnf(297,plain,(atomic(esk13_1(X1))|root(esk10_2(esk13_1(X1),X1),esk13_1(X1))|~activity_occurrence(X1)),inference(spm,[status(thm)],[165,213,theory(equality)])).
% cnf(298,negated_conjecture,(root(esk10_2(tptp0,esk16_0),tptp0)),inference(sr,[status(thm)],[296,117,theory(equality)])).
% cnf(311,negated_conjecture,(activity_occurrence(esk3_1(esk16_0))),inference(spm,[status(thm)],[207,280,theory(equality)])).
% cnf(312,negated_conjecture,(arboreal(esk3_1(esk16_0))|~atomic(tptp4)),inference(spm,[status(thm)],[175,280,theory(equality)])).
% cnf(313,negated_conjecture,(X1=tptp4|~occurrence_of(esk3_1(esk16_0),X1)),inference(spm,[status(thm)],[123,280,theory(equality)])).
% cnf(318,negated_conjecture,(arboreal(esk3_1(esk16_0))|$false),inference(rw,[status(thm)],[312,192,theory(equality)])).
% cnf(319,negated_conjecture,(arboreal(esk3_1(esk16_0))),inference(cn,[status(thm)],[318,theory(equality)])).
% cnf(324,negated_conjecture,(esk13_1(esk16_0)=tptp0|~activity_occurrence(esk16_0)),inference(spm,[status(thm)],[288,213,theory(equality)])).
% cnf(325,negated_conjecture,(esk13_1(esk16_0)=tptp0|$false),inference(rw,[status(thm)],[324,276,theory(equality)])).
% cnf(326,negated_conjecture,(esk13_1(esk16_0)=tptp0),inference(cn,[status(thm)],[325,theory(equality)])).
% cnf(330,negated_conjecture,(esk13_1(esk3_1(esk16_0))=tptp4|~activity_occurrence(esk3_1(esk16_0))),inference(spm,[status(thm)],[313,213,theory(equality)])).
% cnf(331,negated_conjecture,(esk13_1(esk3_1(esk16_0))=tptp4|$false),inference(rw,[status(thm)],[330,311,theory(equality)])).
% cnf(332,negated_conjecture,(esk13_1(esk3_1(esk16_0))=tptp4),inference(cn,[status(thm)],[331,theory(equality)])).
% cnf(333,plain,(X1=esk13_1(X2)|~occurrence_of(X2,X1)),inference(csr,[status(thm)],[289,207])).
% cnf(392,negated_conjecture,(subactivity_occurrence(esk4_1(esk16_0),esk16_0)),inference(spm,[status(thm)],[105,281,theory(equality)])).
% cnf(393,negated_conjecture,(leaf(esk4_1(esk16_0),esk6_2(esk4_1(esk16_0),esk16_0))),inference(spm,[status(thm)],[104,281,theory(equality)])).
% cnf(394,negated_conjecture,(esk4_1(esk16_0)=X1|min_precedes(X1,esk4_1(esk16_0),X2)|~arboreal(X1)|~subactivity_occurrence(X1,esk16_0)|~occurrence_of(esk16_0,X2)),inference(spm,[status(thm)],[113,281,theory(equality)])).
% cnf(395,negated_conjecture,(occurrence_of(esk16_0,esk6_2(esk4_1(esk16_0),esk16_0))),inference(spm,[status(thm)],[106,281,theory(equality)])).
% cnf(399,negated_conjecture,(X1=esk2_1(esk16_0)|~root_occ(X1,esk16_0)|~occurrence_of(esk16_0,X2)),inference(spm,[status(thm)],[110,282,theory(equality)])).
% cnf(401,negated_conjecture,(occurrence_of(X1,tptp1)|min_precedes(esk2_1(esk16_0),esk18_2(esk2_1(esk16_0),X1),tptp0)|~leaf_occ(X1,esk16_0)|~occurrence_of(esk2_1(esk16_0),tptp3)|~occurrence_of(X1,tptp2)|~min_precedes(esk2_1(esk16_0),X1,tptp0)),inference(spm,[status(thm)],[254,282,theory(equality)])).
% cnf(402,negated_conjecture,(occurrence_of(X1,tptp2)|min_precedes(esk2_1(esk16_0),esk17_2(esk2_1(esk16_0),X1),tptp0)|~leaf_occ(X1,esk16_0)|~occurrence_of(esk2_1(esk16_0),tptp3)|~occurrence_of(X1,tptp1)|~min_precedes(esk2_1(esk16_0),X1,tptp0)),inference(spm,[status(thm)],[261,282,theory(equality)])).
% cnf(403,negated_conjecture,(occurrence_of(esk18_2(esk2_1(esk16_0),X1),tptp1)|occurrence_of(X1,tptp1)|~leaf_occ(X1,esk16_0)|~occurrence_of(esk2_1(esk16_0),tptp3)|~occurrence_of(X1,tptp2)|~min_precedes(esk2_1(esk16_0),X1,tptp0)),inference(spm,[status(thm)],[256,282,theory(equality)])).
% cnf(404,negated_conjecture,(subactivity_occurrence(esk18_2(esk2_1(esk16_0),X1),esk16_0)|occurrence_of(X1,tptp1)|~leaf_occ(X1,esk16_0)|~occurrence_of(esk2_1(esk16_0),tptp3)|~occurrence_of(X1,tptp2)|~min_precedes(esk2_1(esk16_0),X1,tptp0)),inference(spm,[status(thm)],[255,282,theory(equality)])).
% cnf(405,negated_conjecture,(occurrence_of(esk17_2(esk2_1(esk16_0),X1),tptp2)|occurrence_of(X1,tptp2)|~leaf_occ(X1,esk16_0)|~occurrence_of(esk2_1(esk16_0),tptp3)|~occurrence_of(X1,tptp1)|~min_precedes(esk2_1(esk16_0),X1,tptp0)),inference(spm,[status(thm)],[269,282,theory(equality)])).
% cnf(406,negated_conjecture,(subactivity_occurrence(esk17_2(esk2_1(esk16_0),X1),esk16_0)|occurrence_of(X1,tptp2)|~leaf_occ(X1,esk16_0)|~occurrence_of(esk2_1(esk16_0),tptp3)|~occurrence_of(X1,tptp1)|~min_precedes(esk2_1(esk16_0),X1,tptp0)),inference(spm,[status(thm)],[265,282,theory(equality)])).
% cnf(425,negated_conjecture,(occurrence_of(X1,tptp1)|min_precedes(esk2_1(esk16_0),esk18_2(esk2_1(esk16_0),X1),tptp0)|~leaf_occ(X1,esk16_0)|$false|~occurrence_of(X1,tptp2)|~min_precedes(esk2_1(esk16_0),X1,tptp0)),inference(rw,[status(thm)],[401,279,theory(equality)])).
% cnf(426,negated_conjecture,(occurrence_of(X1,tptp1)|min_precedes(esk2_1(esk16_0),esk18_2(esk2_1(esk16_0),X1),tptp0)|~leaf_occ(X1,esk16_0)|~occurrence_of(X1,tptp2)|~min_precedes(esk2_1(esk16_0),X1,tptp0)),inference(cn,[status(thm)],[425,theory(equality)])).
% cnf(427,negated_conjecture,(occurrence_of(X1,tptp2)|min_precedes(esk2_1(esk16_0),esk17_2(esk2_1(esk16_0),X1),tptp0)|~leaf_occ(X1,esk16_0)|$false|~occurrence_of(X1,tptp1)|~min_precedes(esk2_1(esk16_0),X1,tptp0)),inference(rw,[status(thm)],[402,279,theory(equality)])).
% cnf(428,negated_conjecture,(occurrence_of(X1,tptp2)|min_precedes(esk2_1(esk16_0),esk17_2(esk2_1(esk16_0),X1),tptp0)|~leaf_occ(X1,esk16_0)|~occurrence_of(X1,tptp1)|~min_precedes(esk2_1(esk16_0),X1,tptp0)),inference(cn,[status(thm)],[427,theory(equality)])).
% cnf(429,negated_conjecture,(occurrence_of(esk18_2(esk2_1(esk16_0),X1),tptp1)|occurrence_of(X1,tptp1)|~leaf_occ(X1,esk16_0)|$false|~occurrence_of(X1,tptp2)|~min_precedes(esk2_1(esk16_0),X1,tptp0)),inference(rw,[status(thm)],[403,279,theory(equality)])).
% cnf(430,negated_conjecture,(occurrence_of(esk18_2(esk2_1(esk16_0),X1),tptp1)|occurrence_of(X1,tptp1)|~leaf_occ(X1,esk16_0)|~occurrence_of(X1,tptp2)|~min_precedes(esk2_1(esk16_0),X1,tptp0)),inference(cn,[status(thm)],[429,theory(equality)])).
% cnf(431,negated_conjecture,(subactivity_occurrence(esk18_2(esk2_1(esk16_0),X1),esk16_0)|occurrence_of(X1,tptp1)|~leaf_occ(X1,esk16_0)|$false|~occurrence_of(X1,tptp2)|~min_precedes(esk2_1(esk16_0),X1,tptp0)),inference(rw,[status(thm)],[404,279,theory(equality)])).
% cnf(432,negated_conjecture,(subactivity_occurrence(esk18_2(esk2_1(esk16_0),X1),esk16_0)|occurrence_of(X1,tptp1)|~leaf_occ(X1,esk16_0)|~occurrence_of(X1,tptp2)|~min_precedes(esk2_1(esk16_0),X1,tptp0)),inference(cn,[status(thm)],[431,theory(equality)])).
% cnf(433,negated_conjecture,(occurrence_of(esk17_2(esk2_1(esk16_0),X1),tptp2)|occurrence_of(X1,tptp2)|~leaf_occ(X1,esk16_0)|$false|~occurrence_of(X1,tptp1)|~min_precedes(esk2_1(esk16_0),X1,tptp0)),inference(rw,[status(thm)],[405,279,theory(equality)])).
% cnf(434,negated_conjecture,(occurrence_of(esk17_2(esk2_1(esk16_0),X1),tptp2)|occurrence_of(X1,tptp2)|~leaf_occ(X1,esk16_0)|~occurrence_of(X1,tptp1)|~min_precedes(esk2_1(esk16_0),X1,tptp0)),inference(cn,[status(thm)],[433,theory(equality)])).
% cnf(435,negated_conjecture,(subactivity_occurrence(esk17_2(esk2_1(esk16_0),X1),esk16_0)|occurrence_of(X1,tptp2)|~leaf_occ(X1,esk16_0)|$false|~occurrence_of(X1,tptp1)|~min_precedes(esk2_1(esk16_0),X1,tptp0)),inference(rw,[status(thm)],[406,279,theory(equality)])).
% cnf(436,negated_conjecture,(subactivity_occurrence(esk17_2(esk2_1(esk16_0),X1),esk16_0)|occurrence_of(X1,tptp2)|~leaf_occ(X1,esk16_0)|~occurrence_of(X1,tptp1)|~min_precedes(esk2_1(esk16_0),X1,tptp0)),inference(cn,[status(thm)],[435,theory(equality)])).
% cnf(492,negated_conjecture,(root_occ(esk10_2(tptp0,esk16_0),X1)|~subactivity_occurrence(esk10_2(tptp0,esk16_0),X1)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[95,298,theory(equality)])).
% cnf(495,negated_conjecture,(root_occ(esk10_2(tptp0,esk16_0),esk16_0)|~subactivity_occurrence(esk10_2(tptp0,esk16_0),esk16_0)),inference(spm,[status(thm)],[492,241,theory(equality)])).
% cnf(496,negated_conjecture,(root_occ(esk10_2(tptp0,esk16_0),esk16_0)|$false),inference(rw,[status(thm)],[495,295,theory(equality)])).
% cnf(497,negated_conjecture,(root_occ(esk10_2(tptp0,esk16_0),esk16_0)),inference(cn,[status(thm)],[496,theory(equality)])).
% cnf(532,negated_conjecture,(esk10_2(tptp0,esk16_0)=esk2_1(esk16_0)|~occurrence_of(esk16_0,X1)),inference(spm,[status(thm)],[399,497,theory(equality)])).
% cnf(534,negated_conjecture,(esk10_2(tptp0,esk16_0)=esk2_1(esk16_0)|~activity_occurrence(esk16_0)),inference(spm,[status(thm)],[532,213,theory(equality)])).
% cnf(536,negated_conjecture,(esk10_2(tptp0,esk16_0)=esk2_1(esk16_0)|$false),inference(rw,[status(thm)],[534,276,theory(equality)])).
% cnf(537,negated_conjecture,(esk10_2(tptp0,esk16_0)=esk2_1(esk16_0)),inference(cn,[status(thm)],[536,theory(equality)])).
% cnf(543,negated_conjecture,(root_occ(esk2_1(esk16_0),X1)|~subactivity_occurrence(esk10_2(tptp0,esk16_0),X1)|~occurrence_of(X1,tptp0)),inference(rw,[status(thm)],[492,537,theory(equality)])).
% cnf(544,negated_conjecture,(root_occ(esk2_1(esk16_0),X1)|~subactivity_occurrence(esk2_1(esk16_0),X1)|~occurrence_of(X1,tptp0)),inference(rw,[status(thm)],[543,537,theory(equality)])).
% cnf(558,negated_conjecture,(min_precedes(esk2_1(esk16_0),esk3_1(esk16_0),tptp0)),inference(spm,[status(thm)],[149,290,theory(equality)])).
% cnf(564,negated_conjecture,(min_precedes(esk3_1(esk16_0),esk4_1(esk16_0),tptp0)),inference(spm,[status(thm)],[149,291,theory(equality)])).
% cnf(565,negated_conjecture,(~min_precedes(X1,esk4_1(esk16_0),tptp0)|~min_precedes(esk3_1(esk16_0),X1,tptp0)),inference(spm,[status(thm)],[150,291,theory(equality)])).
% cnf(625,negated_conjecture,(esk6_2(esk4_1(esk16_0),esk16_0)=esk13_1(esk16_0)),inference(spm,[status(thm)],[333,395,theory(equality)])).
% cnf(629,negated_conjecture,(esk6_2(esk4_1(esk16_0),esk16_0)=tptp0),inference(rw,[status(thm)],[625,326,theory(equality)])).
% cnf(681,negated_conjecture,(subactivity_occurrence(esk2_1(esk16_0),X1)|~subactivity_occurrence(esk3_1(esk16_0),X1)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[72,558,theory(equality)])).
% cnf(751,negated_conjecture,(occurrence_of(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp1)|occurrence_of(esk4_1(esk16_0),tptp1)|~occurrence_of(esk4_1(esk16_0),tptp2)|~min_precedes(esk2_1(esk16_0),esk4_1(esk16_0),tptp0)),inference(spm,[status(thm)],[430,281,theory(equality)])).
% cnf(752,negated_conjecture,(subactivity_occurrence(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk16_0)|occurrence_of(esk4_1(esk16_0),tptp1)|~occurrence_of(esk4_1(esk16_0),tptp2)|~min_precedes(esk2_1(esk16_0),esk4_1(esk16_0),tptp0)),inference(spm,[status(thm)],[432,281,theory(equality)])).
% cnf(754,negated_conjecture,(root(esk7_3(esk3_1(esk16_0),esk4_1(esk16_0),tptp0),tptp0)),inference(spm,[status(thm)],[138,564,theory(equality)])).
% cnf(755,negated_conjecture,(min_precedes(esk7_3(esk3_1(esk16_0),esk4_1(esk16_0),tptp0),esk4_1(esk16_0),tptp0)),inference(spm,[status(thm)],[137,564,theory(equality)])).
% cnf(766,negated_conjecture,(subactivity_occurrence(esk3_1(esk16_0),X1)|~subactivity_occurrence(esk4_1(esk16_0),X1)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[72,564,theory(equality)])).
% cnf(777,plain,(root_occ(esk10_2(esk13_1(X1),X1),X2)|atomic(esk13_1(X1))|~subactivity_occurrence(esk10_2(esk13_1(X1),X1),X2)|~occurrence_of(X2,esk13_1(X1))|~activity_occurrence(X1)),inference(spm,[status(thm)],[95,297,theory(equality)])).
% cnf(852,negated_conjecture,(subactivity_occurrence(esk3_1(esk16_0),esk16_0)|~subactivity_occurrence(esk4_1(esk16_0),esk16_0)),inference(spm,[status(thm)],[766,241,theory(equality)])).
% cnf(853,negated_conjecture,(subactivity_occurrence(esk3_1(esk16_0),esk16_0)|$false),inference(rw,[status(thm)],[852,392,theory(equality)])).
% cnf(854,negated_conjecture,(subactivity_occurrence(esk3_1(esk16_0),esk16_0)),inference(cn,[status(thm)],[853,theory(equality)])).
% cnf(858,negated_conjecture,(X1=esk3_1(esk16_0)|min_precedes(X1,esk3_1(esk16_0),X2)|min_precedes(esk3_1(esk16_0),X1,X2)|~arboreal(esk3_1(esk16_0))|~arboreal(X1)|~subactivity_occurrence(X1,esk16_0)|~occurrence_of(esk16_0,X2)),inference(spm,[status(thm)],[116,854,theory(equality)])).
% cnf(862,negated_conjecture,(X1=esk3_1(esk16_0)|min_precedes(X1,esk3_1(esk16_0),X2)|min_precedes(esk3_1(esk16_0),X1,X2)|$false|~arboreal(X1)|~subactivity_occurrence(X1,esk16_0)|~occurrence_of(esk16_0,X2)),inference(rw,[status(thm)],[858,319,theory(equality)])).
% cnf(863,negated_conjecture,(X1=esk3_1(esk16_0)|min_precedes(X1,esk3_1(esk16_0),X2)|min_precedes(esk3_1(esk16_0),X1,X2)|~arboreal(X1)|~subactivity_occurrence(X1,esk16_0)|~occurrence_of(esk16_0,X2)),inference(cn,[status(thm)],[862,theory(equality)])).
% cnf(883,negated_conjecture,(leaf(esk4_1(esk16_0),tptp0)),inference(rw,[status(thm)],[393,629,theory(equality)])).
% cnf(884,negated_conjecture,(atomic(tptp0)|leaf_occ(esk4_1(esk16_0),esk9_2(esk4_1(esk16_0),tptp0))),inference(spm,[status(thm)],[158,883,theory(equality)])).
% cnf(885,negated_conjecture,(atomic(tptp0)|occurrence_of(esk9_2(esk4_1(esk16_0),tptp0),tptp0)),inference(spm,[status(thm)],[159,883,theory(equality)])).
% cnf(888,negated_conjecture,(leaf_occ(esk4_1(esk16_0),esk9_2(esk4_1(esk16_0),tptp0))),inference(sr,[status(thm)],[884,117,theory(equality)])).
% cnf(889,negated_conjecture,(occurrence_of(esk9_2(esk4_1(esk16_0),tptp0),tptp0)),inference(sr,[status(thm)],[885,117,theory(equality)])).
% cnf(891,negated_conjecture,(activity_occurrence(esk9_2(esk4_1(esk16_0),tptp0))),inference(spm,[status(thm)],[207,889,theory(equality)])).
% cnf(898,negated_conjecture,(tptp0=esk13_1(esk9_2(esk4_1(esk16_0),tptp0))),inference(spm,[status(thm)],[333,889,theory(equality)])).
% cnf(900,negated_conjecture,(occurrence_of(esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),tptp4)),inference(spm,[status(thm)],[84,889,theory(equality)])).
% cnf(901,negated_conjecture,(leaf_occ(esk4_1(esk9_2(esk4_1(esk16_0),tptp0)),esk9_2(esk4_1(esk16_0),tptp0))),inference(spm,[status(thm)],[80,889,theory(equality)])).
% cnf(902,negated_conjecture,(root_occ(esk2_1(esk9_2(esk4_1(esk16_0),tptp0)),esk9_2(esk4_1(esk16_0),tptp0))),inference(spm,[status(thm)],[85,889,theory(equality)])).
% cnf(904,negated_conjecture,(next_subocc(esk2_1(esk9_2(esk4_1(esk16_0),tptp0)),esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),tptp0)),inference(spm,[status(thm)],[83,889,theory(equality)])).
% cnf(905,negated_conjecture,(next_subocc(esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),esk4_1(esk9_2(esk4_1(esk16_0),tptp0)),tptp0)),inference(spm,[status(thm)],[81,889,theory(equality)])).
% cnf(906,negated_conjecture,(root_occ(esk2_1(esk16_0),esk9_2(esk4_1(esk16_0),tptp0))|~subactivity_occurrence(esk2_1(esk16_0),esk9_2(esk4_1(esk16_0),tptp0))),inference(spm,[status(thm)],[544,889,theory(equality)])).
% cnf(909,negated_conjecture,(subactivity_occurrence(esk2_1(esk16_0),esk9_2(esk4_1(esk16_0),tptp0))|~subactivity_occurrence(esk3_1(esk16_0),esk9_2(esk4_1(esk16_0),tptp0))),inference(spm,[status(thm)],[681,889,theory(equality)])).
% cnf(912,negated_conjecture,(subactivity_occurrence(esk3_1(esk16_0),esk9_2(esk4_1(esk16_0),tptp0))|~subactivity_occurrence(esk4_1(esk16_0),esk9_2(esk4_1(esk16_0),tptp0))),inference(spm,[status(thm)],[766,889,theory(equality)])).
% cnf(987,plain,(atomic(esk13_1(X1))|root_occ(esk10_2(esk13_1(X1),X1),X1)|~activity_occurrence(X1)|~subactivity_occurrence(esk10_2(esk13_1(X1),X1),X1)),inference(spm,[status(thm)],[777,213,theory(equality)])).
% cnf(1011,negated_conjecture,(subactivity_occurrence(esk4_1(esk16_0),esk9_2(esk4_1(esk16_0),tptp0))),inference(spm,[status(thm)],[105,888,theory(equality)])).
% cnf(1015,negated_conjecture,(X1=esk4_1(esk16_0)|atomic(X2)|~leaf_occ(X1,esk9_2(esk4_1(esk16_0),tptp0))|~occurrence_of(esk9_2(esk4_1(esk16_0),tptp0),X2)),inference(spm,[status(thm)],[168,888,theory(equality)])).
% cnf(1031,negated_conjecture,(occurrence_of(esk4_1(esk16_0),tptp1)|min_precedes(esk2_1(esk16_0),esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp0)|~occurrence_of(esk4_1(esk16_0),tptp2)|~min_precedes(esk2_1(esk16_0),esk4_1(esk16_0),tptp0)),inference(spm,[status(thm)],[426,281,theory(equality)])).
% cnf(1033,negated_conjecture,(arboreal(esk3_1(esk9_2(esk4_1(esk16_0),tptp0)))|~atomic(tptp4)),inference(spm,[status(thm)],[175,900,theory(equality)])).
% cnf(1040,negated_conjecture,(arboreal(esk3_1(esk9_2(esk4_1(esk16_0),tptp0)))|$false),inference(rw,[status(thm)],[1033,192,theory(equality)])).
% cnf(1041,negated_conjecture,(arboreal(esk3_1(esk9_2(esk4_1(esk16_0),tptp0)))),inference(cn,[status(thm)],[1040,theory(equality)])).
% cnf(1050,negated_conjecture,(subactivity_occurrence(esk3_1(esk16_0),esk9_2(esk4_1(esk16_0),tptp0))|$false),inference(rw,[status(thm)],[912,1011,theory(equality)])).
% cnf(1051,negated_conjecture,(subactivity_occurrence(esk3_1(esk16_0),esk9_2(esk4_1(esk16_0),tptp0))),inference(cn,[status(thm)],[1050,theory(equality)])).
% cnf(1140,plain,(atomic(esk13_1(X1))|root_occ(esk10_2(esk13_1(X1),X1),X1)|~activity_occurrence(X1)),inference(csr,[status(thm)],[987,294])).
% cnf(1168,plain,(X1=esk10_2(esk13_1(X2),X2)|atomic(esk13_1(X2))|~root_occ(X1,X2)|~occurrence_of(X2,X3)|~activity_occurrence(X2)),inference(spm,[status(thm)],[110,1140,theory(equality)])).
% cnf(1392,plain,(X1=esk10_2(esk13_1(X2),X2)|atomic(esk13_1(X2))|~root_occ(X1,X2)|~occurrence_of(X2,X3)),inference(csr,[status(thm)],[1168,207])).
% cnf(1430,negated_conjecture,(occurrence_of(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp2)|occurrence_of(esk4_1(esk16_0),tptp2)|~occurrence_of(esk4_1(esk16_0),tptp1)|~min_precedes(esk2_1(esk16_0),esk4_1(esk16_0),tptp0)),inference(spm,[status(thm)],[434,281,theory(equality)])).
% cnf(1431,negated_conjecture,(subactivity_occurrence(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk16_0)|occurrence_of(esk4_1(esk16_0),tptp2)|~occurrence_of(esk4_1(esk16_0),tptp1)|~min_precedes(esk2_1(esk16_0),esk4_1(esk16_0),tptp0)),inference(spm,[status(thm)],[436,281,theory(equality)])).
% cnf(1435,negated_conjecture,(subactivity_occurrence(esk2_1(esk16_0),esk9_2(esk4_1(esk16_0),tptp0))|$false),inference(rw,[status(thm)],[909,1051,theory(equality)])).
% cnf(1436,negated_conjecture,(subactivity_occurrence(esk2_1(esk16_0),esk9_2(esk4_1(esk16_0),tptp0))),inference(cn,[status(thm)],[1435,theory(equality)])).
% cnf(1444,negated_conjecture,(root_occ(esk2_1(esk16_0),esk9_2(esk4_1(esk16_0),tptp0))|$false),inference(rw,[status(thm)],[906,1436,theory(equality)])).
% cnf(1445,negated_conjecture,(root_occ(esk2_1(esk16_0),esk9_2(esk4_1(esk16_0),tptp0))),inference(cn,[status(thm)],[1444,theory(equality)])).
% cnf(1452,negated_conjecture,(esk2_1(esk16_0)=esk10_2(esk13_1(esk9_2(esk4_1(esk16_0),tptp0)),esk9_2(esk4_1(esk16_0),tptp0))|atomic(esk13_1(esk9_2(esk4_1(esk16_0),tptp0)))|~occurrence_of(esk9_2(esk4_1(esk16_0),tptp0),X1)),inference(spm,[status(thm)],[1392,1445,theory(equality)])).
% cnf(1456,negated_conjecture,(esk2_1(esk16_0)=esk10_2(tptp0,esk9_2(esk4_1(esk16_0),tptp0))|atomic(esk13_1(esk9_2(esk4_1(esk16_0),tptp0)))|~occurrence_of(esk9_2(esk4_1(esk16_0),tptp0),X1)),inference(rw,[status(thm)],[1452,898,theory(equality)])).
% cnf(1457,negated_conjecture,(esk2_1(esk16_0)=esk10_2(tptp0,esk9_2(esk4_1(esk16_0),tptp0))|atomic(tptp0)|~occurrence_of(esk9_2(esk4_1(esk16_0),tptp0),X1)),inference(rw,[status(thm)],[1456,898,theory(equality)])).
% cnf(1458,negated_conjecture,(esk10_2(tptp0,esk9_2(esk4_1(esk16_0),tptp0))=esk2_1(esk16_0)|~occurrence_of(esk9_2(esk4_1(esk16_0),tptp0),X1)),inference(sr,[status(thm)],[1457,117,theory(equality)])).
% cnf(1465,negated_conjecture,(occurrence_of(esk4_1(esk16_0),tptp2)|min_precedes(esk2_1(esk16_0),esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp0)|~occurrence_of(esk4_1(esk16_0),tptp1)|~min_precedes(esk2_1(esk16_0),esk4_1(esk16_0),tptp0)),inference(spm,[status(thm)],[428,281,theory(equality)])).
% cnf(1534,negated_conjecture,(esk10_2(tptp0,esk9_2(esk4_1(esk16_0),tptp0))=esk2_1(esk16_0)|~activity_occurrence(esk9_2(esk4_1(esk16_0),tptp0))),inference(spm,[status(thm)],[1458,213,theory(equality)])).
% cnf(1536,negated_conjecture,(esk10_2(tptp0,esk9_2(esk4_1(esk16_0),tptp0))=esk2_1(esk16_0)|$false),inference(rw,[status(thm)],[1534,891,theory(equality)])).
% cnf(1537,negated_conjecture,(esk10_2(tptp0,esk9_2(esk4_1(esk16_0),tptp0))=esk2_1(esk16_0)),inference(cn,[status(thm)],[1536,theory(equality)])).
% cnf(1593,negated_conjecture,(root_occ(esk7_3(esk3_1(esk16_0),esk4_1(esk16_0),tptp0),X1)|~subactivity_occurrence(esk7_3(esk3_1(esk16_0),esk4_1(esk16_0),tptp0),X1)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[95,754,theory(equality)])).
% cnf(1633,negated_conjecture,(root_occ(esk7_3(esk3_1(esk16_0),esk4_1(esk16_0),tptp0),esk16_0)|~subactivity_occurrence(esk7_3(esk3_1(esk16_0),esk4_1(esk16_0),tptp0),esk16_0)),inference(spm,[status(thm)],[1593,241,theory(equality)])).
% cnf(2475,negated_conjecture,(subactivity_occurrence(esk7_3(esk3_1(esk16_0),esk4_1(esk16_0),tptp0),X1)|~subactivity_occurrence(esk4_1(esk16_0),X1)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[72,755,theory(equality)])).
% cnf(2509,negated_conjecture,(subactivity_occurrence(esk7_3(esk3_1(esk16_0),esk4_1(esk16_0),tptp0),esk16_0)|~subactivity_occurrence(esk4_1(esk16_0),esk16_0)),inference(spm,[status(thm)],[2475,241,theory(equality)])).
% cnf(2514,negated_conjecture,(subactivity_occurrence(esk7_3(esk3_1(esk16_0),esk4_1(esk16_0),tptp0),esk16_0)|$false),inference(rw,[status(thm)],[2509,392,theory(equality)])).
% cnf(2515,negated_conjecture,(subactivity_occurrence(esk7_3(esk3_1(esk16_0),esk4_1(esk16_0),tptp0),esk16_0)),inference(cn,[status(thm)],[2514,theory(equality)])).
% cnf(2525,negated_conjecture,(root_occ(esk7_3(esk3_1(esk16_0),esk4_1(esk16_0),tptp0),esk16_0)|$false),inference(rw,[status(thm)],[1633,2515,theory(equality)])).
% cnf(2526,negated_conjecture,(root_occ(esk7_3(esk3_1(esk16_0),esk4_1(esk16_0),tptp0),esk16_0)),inference(cn,[status(thm)],[2525,theory(equality)])).
% cnf(2536,negated_conjecture,(esk7_3(esk3_1(esk16_0),esk4_1(esk16_0),tptp0)=esk10_2(esk13_1(esk16_0),esk16_0)|atomic(esk13_1(esk16_0))|~occurrence_of(esk16_0,X1)),inference(spm,[status(thm)],[1392,2526,theory(equality)])).
% cnf(2565,negated_conjecture,(esk7_3(esk3_1(esk16_0),esk4_1(esk16_0),tptp0)=esk2_1(esk16_0)|atomic(esk13_1(esk16_0))|~occurrence_of(esk16_0,X1)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[2536,326,theory(equality)]),537,theory(equality)])).
% cnf(2566,negated_conjecture,(esk7_3(esk3_1(esk16_0),esk4_1(esk16_0),tptp0)=esk2_1(esk16_0)|atomic(tptp0)|~occurrence_of(esk16_0,X1)),inference(rw,[status(thm)],[2565,326,theory(equality)])).
% cnf(2567,negated_conjecture,(esk7_3(esk3_1(esk16_0),esk4_1(esk16_0),tptp0)=esk2_1(esk16_0)|~occurrence_of(esk16_0,X1)),inference(sr,[status(thm)],[2566,117,theory(equality)])).
% cnf(2573,negated_conjecture,(esk4_1(esk9_2(esk4_1(esk16_0),tptp0))=esk4_1(esk16_0)|atomic(X1)|~occurrence_of(esk9_2(esk4_1(esk16_0),tptp0),X1)),inference(spm,[status(thm)],[1015,901,theory(equality)])).
% cnf(2608,negated_conjecture,(esk7_3(esk3_1(esk16_0),esk4_1(esk16_0),tptp0)=esk2_1(esk16_0)|~activity_occurrence(esk16_0)),inference(spm,[status(thm)],[2567,213,theory(equality)])).
% cnf(2610,negated_conjecture,(esk7_3(esk3_1(esk16_0),esk4_1(esk16_0),tptp0)=esk2_1(esk16_0)|$false),inference(rw,[status(thm)],[2608,276,theory(equality)])).
% cnf(2611,negated_conjecture,(esk7_3(esk3_1(esk16_0),esk4_1(esk16_0),tptp0)=esk2_1(esk16_0)),inference(cn,[status(thm)],[2610,theory(equality)])).
% cnf(2622,negated_conjecture,(esk4_1(esk9_2(esk4_1(esk16_0),tptp0))=esk4_1(esk16_0)|atomic(esk13_1(esk9_2(esk4_1(esk16_0),tptp0)))|~activity_occurrence(esk9_2(esk4_1(esk16_0),tptp0))),inference(spm,[status(thm)],[2573,213,theory(equality)])).
% cnf(2624,negated_conjecture,(esk4_1(esk9_2(esk4_1(esk16_0),tptp0))=esk4_1(esk16_0)|atomic(tptp0)|~activity_occurrence(esk9_2(esk4_1(esk16_0),tptp0))),inference(rw,[status(thm)],[2622,898,theory(equality)])).
% cnf(2625,negated_conjecture,(esk4_1(esk9_2(esk4_1(esk16_0),tptp0))=esk4_1(esk16_0)|atomic(tptp0)|$false),inference(rw,[status(thm)],[2624,891,theory(equality)])).
% cnf(2626,negated_conjecture,(esk4_1(esk9_2(esk4_1(esk16_0),tptp0))=esk4_1(esk16_0)|atomic(tptp0)),inference(cn,[status(thm)],[2625,theory(equality)])).
% cnf(2627,negated_conjecture,(esk4_1(esk9_2(esk4_1(esk16_0),tptp0))=esk4_1(esk16_0)),inference(sr,[status(thm)],[2626,117,theory(equality)])).
% cnf(2655,negated_conjecture,(min_precedes(esk2_1(esk16_0),esk4_1(esk16_0),tptp0)),inference(rw,[status(thm)],[755,2611,theory(equality)])).
% cnf(3020,negated_conjecture,(esk2_1(esk9_2(esk4_1(esk16_0),tptp0))=esk10_2(esk13_1(esk9_2(esk4_1(esk16_0),tptp0)),esk9_2(esk4_1(esk16_0),tptp0))|atomic(esk13_1(esk9_2(esk4_1(esk16_0),tptp0)))|~occurrence_of(esk9_2(esk4_1(esk16_0),tptp0),X1)),inference(spm,[status(thm)],[1392,902,theory(equality)])).
% cnf(3024,negated_conjecture,(esk2_1(esk9_2(esk4_1(esk16_0),tptp0))=esk2_1(esk16_0)|atomic(esk13_1(esk9_2(esk4_1(esk16_0),tptp0)))|~occurrence_of(esk9_2(esk4_1(esk16_0),tptp0),X1)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[3020,898,theory(equality)]),1537,theory(equality)])).
% cnf(3025,negated_conjecture,(esk2_1(esk9_2(esk4_1(esk16_0),tptp0))=esk2_1(esk16_0)|atomic(tptp0)|~occurrence_of(esk9_2(esk4_1(esk16_0),tptp0),X1)),inference(rw,[status(thm)],[3024,898,theory(equality)])).
% cnf(3026,negated_conjecture,(esk2_1(esk9_2(esk4_1(esk16_0),tptp0))=esk2_1(esk16_0)|~occurrence_of(esk9_2(esk4_1(esk16_0),tptp0),X1)),inference(sr,[status(thm)],[3025,117,theory(equality)])).
% cnf(3049,negated_conjecture,(esk2_1(esk9_2(esk4_1(esk16_0),tptp0))=esk2_1(esk16_0)|~activity_occurrence(esk9_2(esk4_1(esk16_0),tptp0))),inference(spm,[status(thm)],[3026,213,theory(equality)])).
% cnf(3051,negated_conjecture,(esk2_1(esk9_2(esk4_1(esk16_0),tptp0))=esk2_1(esk16_0)|$false),inference(rw,[status(thm)],[3049,891,theory(equality)])).
% cnf(3052,negated_conjecture,(esk2_1(esk9_2(esk4_1(esk16_0),tptp0))=esk2_1(esk16_0)),inference(cn,[status(thm)],[3051,theory(equality)])).
% cnf(3317,negated_conjecture,(occurrence_of(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp1)|occurrence_of(esk4_1(esk16_0),tptp1)|~occurrence_of(esk4_1(esk16_0),tptp2)|$false),inference(rw,[status(thm)],[751,2655,theory(equality)])).
% cnf(3318,negated_conjecture,(occurrence_of(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp1)|occurrence_of(esk4_1(esk16_0),tptp1)|~occurrence_of(esk4_1(esk16_0),tptp2)),inference(cn,[status(thm)],[3317,theory(equality)])).
% cnf(3319,negated_conjecture,(occurrence_of(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp1)|occurrence_of(esk4_1(esk16_0),tptp1)),inference(csr,[status(thm)],[3318,292])).
% cnf(3321,negated_conjecture,(arboreal(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)))|occurrence_of(esk4_1(esk16_0),tptp1)|~atomic(tptp1)),inference(spm,[status(thm)],[175,3319,theory(equality)])).
% cnf(3327,negated_conjecture,(tptp1=esk13_1(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)))|occurrence_of(esk4_1(esk16_0),tptp1)),inference(spm,[status(thm)],[333,3319,theory(equality)])).
% cnf(3328,negated_conjecture,(arboreal(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)))|occurrence_of(esk4_1(esk16_0),tptp1)|$false),inference(rw,[status(thm)],[3321,118,theory(equality)])).
% cnf(3329,negated_conjecture,(arboreal(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)))|occurrence_of(esk4_1(esk16_0),tptp1)),inference(cn,[status(thm)],[3328,theory(equality)])).
% cnf(3421,negated_conjecture,(subactivity_occurrence(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk16_0)|occurrence_of(esk4_1(esk16_0),tptp1)|~occurrence_of(esk4_1(esk16_0),tptp2)|$false),inference(rw,[status(thm)],[752,2655,theory(equality)])).
% cnf(3422,negated_conjecture,(subactivity_occurrence(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk16_0)|occurrence_of(esk4_1(esk16_0),tptp1)|~occurrence_of(esk4_1(esk16_0),tptp2)),inference(cn,[status(thm)],[3421,theory(equality)])).
% cnf(3423,negated_conjecture,(subactivity_occurrence(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk16_0)|occurrence_of(esk4_1(esk16_0),tptp1)),inference(csr,[status(thm)],[3422,292])).
% cnf(3427,negated_conjecture,(esk4_1(esk16_0)=esk18_2(esk2_1(esk16_0),esk4_1(esk16_0))|min_precedes(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk4_1(esk16_0),X1)|occurrence_of(esk4_1(esk16_0),tptp1)|~arboreal(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)))|~occurrence_of(esk16_0,X1)),inference(spm,[status(thm)],[394,3423,theory(equality)])).
% cnf(3429,negated_conjecture,(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk3_1(esk16_0)|min_precedes(esk3_1(esk16_0),esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),X1)|min_precedes(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk3_1(esk16_0),X1)|occurrence_of(esk4_1(esk16_0),tptp1)|~arboreal(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)))|~occurrence_of(esk16_0,X1)),inference(spm,[status(thm)],[863,3423,theory(equality)])).
% cnf(3524,negated_conjecture,(occurrence_of(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp2)|occurrence_of(esk4_1(esk16_0),tptp2)|~occurrence_of(esk4_1(esk16_0),tptp1)|$false),inference(rw,[status(thm)],[1430,2655,theory(equality)])).
% cnf(3525,negated_conjecture,(occurrence_of(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp2)|occurrence_of(esk4_1(esk16_0),tptp2)|~occurrence_of(esk4_1(esk16_0),tptp1)),inference(cn,[status(thm)],[3524,theory(equality)])).
% cnf(3526,negated_conjecture,(occurrence_of(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp2)|occurrence_of(esk4_1(esk16_0),tptp2)),inference(csr,[status(thm)],[3525,292])).
% cnf(3528,negated_conjecture,(arboreal(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)))|occurrence_of(esk4_1(esk16_0),tptp2)|~atomic(tptp2)),inference(spm,[status(thm)],[175,3526,theory(equality)])).
% cnf(3534,negated_conjecture,(tptp2=esk13_1(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)))|occurrence_of(esk4_1(esk16_0),tptp2)),inference(spm,[status(thm)],[333,3526,theory(equality)])).
% cnf(3535,negated_conjecture,(arboreal(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)))|occurrence_of(esk4_1(esk16_0),tptp2)|$false),inference(rw,[status(thm)],[3528,119,theory(equality)])).
% cnf(3536,negated_conjecture,(arboreal(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)))|occurrence_of(esk4_1(esk16_0),tptp2)),inference(cn,[status(thm)],[3535,theory(equality)])).
% cnf(3545,negated_conjecture,(subactivity_occurrence(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk16_0)|occurrence_of(esk4_1(esk16_0),tptp2)|~occurrence_of(esk4_1(esk16_0),tptp1)|$false),inference(rw,[status(thm)],[1431,2655,theory(equality)])).
% cnf(3546,negated_conjecture,(subactivity_occurrence(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk16_0)|occurrence_of(esk4_1(esk16_0),tptp2)|~occurrence_of(esk4_1(esk16_0),tptp1)),inference(cn,[status(thm)],[3545,theory(equality)])).
% cnf(3547,negated_conjecture,(subactivity_occurrence(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk16_0)|occurrence_of(esk4_1(esk16_0),tptp2)),inference(csr,[status(thm)],[3546,292])).
% cnf(3551,negated_conjecture,(esk4_1(esk16_0)=esk17_2(esk2_1(esk16_0),esk4_1(esk16_0))|min_precedes(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk4_1(esk16_0),X1)|occurrence_of(esk4_1(esk16_0),tptp2)|~arboreal(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)))|~occurrence_of(esk16_0,X1)),inference(spm,[status(thm)],[394,3547,theory(equality)])).
% cnf(3553,negated_conjecture,(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk3_1(esk16_0)|min_precedes(esk3_1(esk16_0),esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),X1)|min_precedes(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk3_1(esk16_0),X1)|occurrence_of(esk4_1(esk16_0),tptp2)|~arboreal(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)))|~occurrence_of(esk16_0,X1)),inference(spm,[status(thm)],[863,3547,theory(equality)])).
% cnf(6020,negated_conjecture,(next_subocc(esk2_1(esk16_0),esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),tptp0)),inference(rw,[status(thm)],[904,3052,theory(equality)])).
% cnf(6023,negated_conjecture,(~min_precedes(X1,esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),tptp0)|~min_precedes(esk2_1(esk16_0),X1,tptp0)),inference(spm,[status(thm)],[150,6020,theory(equality)])).
% cnf(6029,negated_conjecture,(~min_precedes(esk3_1(esk16_0),esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),tptp0)),inference(spm,[status(thm)],[6023,558,theory(equality)])).
% cnf(6068,negated_conjecture,(occurrence_of(esk4_1(esk16_0),tptp1)|min_precedes(esk2_1(esk16_0),esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp0)|~occurrence_of(esk4_1(esk16_0),tptp2)|$false),inference(rw,[status(thm)],[1031,2655,theory(equality)])).
% cnf(6069,negated_conjecture,(occurrence_of(esk4_1(esk16_0),tptp1)|min_precedes(esk2_1(esk16_0),esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp0)|~occurrence_of(esk4_1(esk16_0),tptp2)),inference(cn,[status(thm)],[6068,theory(equality)])).
% cnf(6070,negated_conjecture,(occurrence_of(esk4_1(esk16_0),tptp1)|min_precedes(esk2_1(esk16_0),esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp0)),inference(csr,[status(thm)],[6069,292])).
% cnf(6088,negated_conjecture,(occurrence_of(esk4_1(esk16_0),tptp1)|~min_precedes(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),tptp0)),inference(spm,[status(thm)],[6023,6070,theory(equality)])).
% cnf(6092,negated_conjecture,(next_subocc(esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),esk4_1(esk16_0),tptp0)),inference(rw,[status(thm)],[905,2627,theory(equality)])).
% cnf(6094,negated_conjecture,(min_precedes(esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),esk4_1(esk16_0),tptp0)),inference(spm,[status(thm)],[149,6092,theory(equality)])).
% cnf(6095,negated_conjecture,(~min_precedes(X1,esk4_1(esk16_0),tptp0)|~min_precedes(esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),X1,tptp0)),inference(spm,[status(thm)],[150,6092,theory(equality)])).
% cnf(6100,negated_conjecture,(~min_precedes(esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),esk3_1(esk16_0),tptp0)),inference(spm,[status(thm)],[6095,564,theory(equality)])).
% cnf(6177,negated_conjecture,(subactivity_occurrence(esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),X1)|~subactivity_occurrence(esk4_1(esk16_0),X1)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[72,6094,theory(equality)])).
% cnf(6189,negated_conjecture,(subactivity_occurrence(esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),esk16_0)|~subactivity_occurrence(esk4_1(esk16_0),esk16_0)),inference(spm,[status(thm)],[6177,241,theory(equality)])).
% cnf(6197,negated_conjecture,(subactivity_occurrence(esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),esk16_0)|$false),inference(rw,[status(thm)],[6189,392,theory(equality)])).
% cnf(6198,negated_conjecture,(subactivity_occurrence(esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),esk16_0)),inference(cn,[status(thm)],[6197,theory(equality)])).
% cnf(6233,negated_conjecture,(esk3_1(esk9_2(esk4_1(esk16_0),tptp0))=esk3_1(esk16_0)|min_precedes(esk3_1(esk16_0),esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),X1)|min_precedes(esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),esk3_1(esk16_0),X1)|~arboreal(esk3_1(esk9_2(esk4_1(esk16_0),tptp0)))|~occurrence_of(esk16_0,X1)),inference(spm,[status(thm)],[863,6198,theory(equality)])).
% cnf(6242,negated_conjecture,(esk3_1(esk9_2(esk4_1(esk16_0),tptp0))=esk3_1(esk16_0)|min_precedes(esk3_1(esk16_0),esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),X1)|min_precedes(esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),esk3_1(esk16_0),X1)|$false|~occurrence_of(esk16_0,X1)),inference(rw,[status(thm)],[6233,1041,theory(equality)])).
% cnf(6243,negated_conjecture,(esk3_1(esk9_2(esk4_1(esk16_0),tptp0))=esk3_1(esk16_0)|min_precedes(esk3_1(esk16_0),esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),X1)|min_precedes(esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),esk3_1(esk16_0),X1)|~occurrence_of(esk16_0,X1)),inference(cn,[status(thm)],[6242,theory(equality)])).
% cnf(6325,negated_conjecture,(occurrence_of(esk4_1(esk16_0),tptp2)|min_precedes(esk2_1(esk16_0),esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp0)|~occurrence_of(esk4_1(esk16_0),tptp1)|$false),inference(rw,[status(thm)],[1465,2655,theory(equality)])).
% cnf(6326,negated_conjecture,(occurrence_of(esk4_1(esk16_0),tptp2)|min_precedes(esk2_1(esk16_0),esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp0)|~occurrence_of(esk4_1(esk16_0),tptp1)),inference(cn,[status(thm)],[6325,theory(equality)])).
% cnf(6327,negated_conjecture,(occurrence_of(esk4_1(esk16_0),tptp2)|min_precedes(esk2_1(esk16_0),esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp0)),inference(csr,[status(thm)],[6326,292])).
% cnf(6345,negated_conjecture,(occurrence_of(esk4_1(esk16_0),tptp2)|~min_precedes(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),tptp0)),inference(spm,[status(thm)],[6023,6327,theory(equality)])).
% cnf(18591,negated_conjecture,(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk4_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp1)|min_precedes(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk4_1(esk16_0),X1)|~occurrence_of(esk16_0,X1)),inference(csr,[status(thm)],[3427,3329])).
% cnf(18592,negated_conjecture,(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk4_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp1)|min_precedes(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk4_1(esk16_0),esk13_1(esk16_0))|~activity_occurrence(esk16_0)),inference(spm,[status(thm)],[18591,213,theory(equality)])).
% cnf(18595,negated_conjecture,(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk4_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp1)|min_precedes(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk4_1(esk16_0),tptp0)|~activity_occurrence(esk16_0)),inference(rw,[status(thm)],[18592,326,theory(equality)])).
% cnf(18596,negated_conjecture,(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk4_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp1)|min_precedes(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk4_1(esk16_0),tptp0)|$false),inference(rw,[status(thm)],[18595,276,theory(equality)])).
% cnf(18597,negated_conjecture,(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk4_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp1)|min_precedes(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk4_1(esk16_0),tptp0)),inference(cn,[status(thm)],[18596,theory(equality)])).
% cnf(18858,negated_conjecture,(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk3_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp1)|min_precedes(esk3_1(esk16_0),esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),X1)|min_precedes(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk3_1(esk16_0),X1)|~occurrence_of(esk16_0,X1)),inference(csr,[status(thm)],[3429,3329])).
% cnf(18859,negated_conjecture,(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk3_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp1)|min_precedes(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk3_1(esk16_0),esk13_1(esk16_0))|min_precedes(esk3_1(esk16_0),esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk13_1(esk16_0))|~activity_occurrence(esk16_0)),inference(spm,[status(thm)],[18858,213,theory(equality)])).
% cnf(18862,negated_conjecture,(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk3_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp1)|min_precedes(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk3_1(esk16_0),tptp0)|min_precedes(esk3_1(esk16_0),esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk13_1(esk16_0))|~activity_occurrence(esk16_0)),inference(rw,[status(thm)],[18859,326,theory(equality)])).
% cnf(18863,negated_conjecture,(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk3_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp1)|min_precedes(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk3_1(esk16_0),tptp0)|min_precedes(esk3_1(esk16_0),esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp0)|~activity_occurrence(esk16_0)),inference(rw,[status(thm)],[18862,326,theory(equality)])).
% cnf(18864,negated_conjecture,(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk3_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp1)|min_precedes(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk3_1(esk16_0),tptp0)|min_precedes(esk3_1(esk16_0),esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp0)|$false),inference(rw,[status(thm)],[18863,276,theory(equality)])).
% cnf(18865,negated_conjecture,(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk3_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp1)|min_precedes(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk3_1(esk16_0),tptp0)|min_precedes(esk3_1(esk16_0),esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp0)),inference(cn,[status(thm)],[18864,theory(equality)])).
% cnf(20320,negated_conjecture,(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk4_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp2)|min_precedes(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk4_1(esk16_0),X1)|~occurrence_of(esk16_0,X1)),inference(csr,[status(thm)],[3551,3536])).
% cnf(20321,negated_conjecture,(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk4_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp2)|min_precedes(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk4_1(esk16_0),esk13_1(esk16_0))|~activity_occurrence(esk16_0)),inference(spm,[status(thm)],[20320,213,theory(equality)])).
% cnf(20324,negated_conjecture,(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk4_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp2)|min_precedes(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk4_1(esk16_0),tptp0)|~activity_occurrence(esk16_0)),inference(rw,[status(thm)],[20321,326,theory(equality)])).
% cnf(20325,negated_conjecture,(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk4_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp2)|min_precedes(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk4_1(esk16_0),tptp0)|$false),inference(rw,[status(thm)],[20324,276,theory(equality)])).
% cnf(20326,negated_conjecture,(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk4_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp2)|min_precedes(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk4_1(esk16_0),tptp0)),inference(cn,[status(thm)],[20325,theory(equality)])).
% cnf(20420,negated_conjecture,(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk3_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp2)|min_precedes(esk3_1(esk16_0),esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),X1)|min_precedes(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk3_1(esk16_0),X1)|~occurrence_of(esk16_0,X1)),inference(csr,[status(thm)],[3553,3536])).
% cnf(20421,negated_conjecture,(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk3_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp2)|min_precedes(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk3_1(esk16_0),esk13_1(esk16_0))|min_precedes(esk3_1(esk16_0),esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk13_1(esk16_0))|~activity_occurrence(esk16_0)),inference(spm,[status(thm)],[20420,213,theory(equality)])).
% cnf(20424,negated_conjecture,(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk3_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp2)|min_precedes(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk3_1(esk16_0),tptp0)|min_precedes(esk3_1(esk16_0),esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk13_1(esk16_0))|~activity_occurrence(esk16_0)),inference(rw,[status(thm)],[20421,326,theory(equality)])).
% cnf(20425,negated_conjecture,(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk3_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp2)|min_precedes(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk3_1(esk16_0),tptp0)|min_precedes(esk3_1(esk16_0),esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp0)|~activity_occurrence(esk16_0)),inference(rw,[status(thm)],[20424,326,theory(equality)])).
% cnf(20426,negated_conjecture,(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk3_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp2)|min_precedes(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk3_1(esk16_0),tptp0)|min_precedes(esk3_1(esk16_0),esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp0)|$false),inference(rw,[status(thm)],[20425,276,theory(equality)])).
% cnf(20427,negated_conjecture,(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk3_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp2)|min_precedes(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk3_1(esk16_0),tptp0)|min_precedes(esk3_1(esk16_0),esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp0)),inference(cn,[status(thm)],[20426,theory(equality)])).
% cnf(27090,negated_conjecture,(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk4_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp1)|~min_precedes(esk3_1(esk16_0),esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp0)),inference(spm,[status(thm)],[565,18597,theory(equality)])).
% cnf(27307,negated_conjecture,(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk4_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp2)|~min_precedes(esk3_1(esk16_0),esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp0)),inference(spm,[status(thm)],[565,20326,theory(equality)])).
% cnf(64211,negated_conjecture,(esk3_1(esk9_2(esk4_1(esk16_0),tptp0))=esk3_1(esk16_0)|min_precedes(esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),esk3_1(esk16_0),esk13_1(esk16_0))|min_precedes(esk3_1(esk16_0),esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),esk13_1(esk16_0))|~activity_occurrence(esk16_0)),inference(spm,[status(thm)],[6243,213,theory(equality)])).
% cnf(64214,negated_conjecture,(esk3_1(esk9_2(esk4_1(esk16_0),tptp0))=esk3_1(esk16_0)|min_precedes(esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),esk3_1(esk16_0),tptp0)|min_precedes(esk3_1(esk16_0),esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),esk13_1(esk16_0))|~activity_occurrence(esk16_0)),inference(rw,[status(thm)],[64211,326,theory(equality)])).
% cnf(64215,negated_conjecture,(esk3_1(esk9_2(esk4_1(esk16_0),tptp0))=esk3_1(esk16_0)|min_precedes(esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),esk3_1(esk16_0),tptp0)|min_precedes(esk3_1(esk16_0),esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),tptp0)|~activity_occurrence(esk16_0)),inference(rw,[status(thm)],[64214,326,theory(equality)])).
% cnf(64216,negated_conjecture,(esk3_1(esk9_2(esk4_1(esk16_0),tptp0))=esk3_1(esk16_0)|min_precedes(esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),esk3_1(esk16_0),tptp0)|min_precedes(esk3_1(esk16_0),esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),tptp0)|$false),inference(rw,[status(thm)],[64215,276,theory(equality)])).
% cnf(64217,negated_conjecture,(esk3_1(esk9_2(esk4_1(esk16_0),tptp0))=esk3_1(esk16_0)|min_precedes(esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),esk3_1(esk16_0),tptp0)|min_precedes(esk3_1(esk16_0),esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),tptp0)),inference(cn,[status(thm)],[64216,theory(equality)])).
% cnf(64218,negated_conjecture,(esk3_1(esk9_2(esk4_1(esk16_0),tptp0))=esk3_1(esk16_0)|min_precedes(esk3_1(esk16_0),esk3_1(esk9_2(esk4_1(esk16_0),tptp0)),tptp0)),inference(sr,[status(thm)],[64217,6100,theory(equality)])).
% cnf(64219,negated_conjecture,(esk3_1(esk9_2(esk4_1(esk16_0),tptp0))=esk3_1(esk16_0)),inference(sr,[status(thm)],[64218,6029,theory(equality)])).
% cnf(64705,negated_conjecture,(occurrence_of(esk4_1(esk16_0),tptp2)|~min_precedes(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk3_1(esk16_0),tptp0)),inference(rw,[status(thm)],[6345,64219,theory(equality)])).
% cnf(64742,negated_conjecture,(occurrence_of(esk4_1(esk16_0),tptp1)|~min_precedes(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),esk3_1(esk16_0),tptp0)),inference(rw,[status(thm)],[6088,64219,theory(equality)])).
% cnf(89805,negated_conjecture,(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk3_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp1)|min_precedes(esk3_1(esk16_0),esk18_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp0)),inference(csr,[status(thm)],[18865,64742])).
% cnf(89823,negated_conjecture,(esk18_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk4_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp1)|esk18_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk3_1(esk16_0)),inference(spm,[status(thm)],[27090,89805,theory(equality)])).
% cnf(89840,negated_conjecture,(esk13_1(esk3_1(esk16_0))=tptp1|occurrence_of(esk4_1(esk16_0),tptp1)|esk18_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk4_1(esk16_0)),inference(spm,[status(thm)],[3327,89823,theory(equality)])).
% cnf(90452,negated_conjecture,(tptp4=tptp1|occurrence_of(esk4_1(esk16_0),tptp1)|esk18_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk4_1(esk16_0)),inference(rw,[status(thm)],[89840,332,theory(equality)])).
% cnf(90453,negated_conjecture,(occurrence_of(esk4_1(esk16_0),tptp1)|esk18_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk4_1(esk16_0)),inference(sr,[status(thm)],[90452,170,theory(equality)])).
% cnf(90715,negated_conjecture,(occurrence_of(esk4_1(esk16_0),tptp1)),inference(spm,[status(thm)],[3319,90453,theory(equality)])).
% cnf(91472,negated_conjecture,(tptp1=esk13_1(esk4_1(esk16_0))),inference(spm,[status(thm)],[333,90715,theory(equality)])).
% cnf(92137,negated_conjecture,(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk3_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp2)|min_precedes(esk3_1(esk16_0),esk17_2(esk2_1(esk16_0),esk4_1(esk16_0)),tptp0)),inference(csr,[status(thm)],[20427,64705])).
% cnf(92155,negated_conjecture,(esk17_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk4_1(esk16_0)|occurrence_of(esk4_1(esk16_0),tptp2)|esk17_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk3_1(esk16_0)),inference(spm,[status(thm)],[27307,92137,theory(equality)])).
% cnf(92163,negated_conjecture,(esk13_1(esk3_1(esk16_0))=tptp2|occurrence_of(esk4_1(esk16_0),tptp2)|esk17_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk4_1(esk16_0)),inference(spm,[status(thm)],[3534,92155,theory(equality)])).
% cnf(92755,negated_conjecture,(tptp4=tptp2|occurrence_of(esk4_1(esk16_0),tptp2)|esk17_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk4_1(esk16_0)),inference(rw,[status(thm)],[92163,332,theory(equality)])).
% cnf(92756,negated_conjecture,(occurrence_of(esk4_1(esk16_0),tptp2)|esk17_2(esk2_1(esk16_0),esk4_1(esk16_0))=esk4_1(esk16_0)),inference(sr,[status(thm)],[92755,171,theory(equality)])).
% cnf(93007,negated_conjecture,(esk13_1(esk4_1(esk16_0))=tptp2|occurrence_of(esk4_1(esk16_0),tptp2)),inference(spm,[status(thm)],[3534,92756,theory(equality)])).
% cnf(93497,negated_conjecture,(tptp1=tptp2|occurrence_of(esk4_1(esk16_0),tptp2)),inference(rw,[status(thm)],[93007,91472,theory(equality)])).
% cnf(93498,negated_conjecture,(occurrence_of(esk4_1(esk16_0),tptp2)),inference(sr,[status(thm)],[93497,98,theory(equality)])).
% cnf(93700,negated_conjecture,(tptp2=esk13_1(esk4_1(esk16_0))),inference(spm,[status(thm)],[333,93498,theory(equality)])).
% cnf(93924,negated_conjecture,(tptp2=tptp1),inference(rw,[status(thm)],[93700,91472,theory(equality)])).
% cnf(93925,negated_conjecture,($false),inference(sr,[status(thm)],[93924,98,theory(equality)])).
% cnf(93926,negated_conjecture,($false),93925,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 9471
% # ...of these trivial : 316
% # ...subsumed : 2622
% # ...remaining for further processing: 6533
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 184
% # Backward-rewritten : 2328
% # Generated clauses : 39339
% # ...of the previous two non-trivial : 26295
% # Contextual simplify-reflections : 321
% # Paramodulations : 39337
% # Factorizations : 2
% # Equation resolutions : 0
% # Current number of processed clauses: 4021
% # Positive orientable unit clauses: 735
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 1066
% # Non-unit-clauses : 2220
% # Current number of unprocessed clauses: 8949
% # ...number of literals in the above : 28523
% # Clause-clause subsumption calls (NU) : 104763
% # Rec. Clause-clause subsumption calls : 82666
% # Unit Clause-clause subsumption calls : 163058
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 5860
% # Indexed BW rewrite successes : 85
% # Backwards rewriting index: 1277 leaves, 3.05+/-5.682 terms/leaf
% # Paramod-from index: 476 leaves, 2.28+/-3.842 terms/leaf
% # Paramod-into index: 1066 leaves, 3.28+/-6.142 terms/leaf
% # -------------------------------------------------
% # User time : 4.693 s
% # System time : 0.082 s
% # Total time : 4.775 s
% # Maximum resident set size: 0 pages
% PrfWatch: 5.89 CPU 6.02 WC
% PrfWatch: 5.89 CPU 6.05 WC
% FINAL PrfWatch: 5.89 CPU 6.05 WC
% SZS output end Solution for /tmp/SystemOnTPTP12516/PRO008+4.tptp
%
%------------------------------------------------------------------------------