%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : PRO002+4 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art06.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Wed Dec 29 20:58:03 EST 2010
% Result : Theorem 23.01s
% Output : Solution 23.01s
% 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/SystemOnTPTP23383/PRO002+4.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP23383/PRO002+4.tptp
% SZS output start Solution for /tmp/SystemOnTPTP23383/PRO002+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 23479
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% PrfWatch: 1.94 CPU 2.02 WC
% PrfWatch: 3.55 CPU 4.02 WC
% PrfWatch: 5.19 CPU 6.03 WC
% PrfWatch: 7.19 CPU 8.03 WC
% PrfWatch: 9.18 CPU 10.04 WC
% PrfWatch: 11.17 CPU 12.04 WC
% PrfWatch: 13.17 CPU 14.05 WC
% PrfWatch: 15.16 CPU 16.05 WC
% PrfWatch: 17.15 CPU 18.06 WC
% # Preprocessing time : 0.019 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 19.14 CPU 20.06 WC
% PrfWatch: 21.14 CPU 22.06 WC
% # SZS output start CNFRefutation.
% fof(2, axiom,~(atomic(tptp0)),file('/tmp/SRASS.s.p', sos_34)).
% fof(4, axiom,![X3]:![X4]:![X5]:![X6]:((tptp1(X3,X4,X5)&occurrence_of(X6,X3))=>?[X7]:?[X8]:?[X9]:?[X10]:((send_message(X7,X8,X9,X5,X4)&occurrence_of(X10,X7))&root_occ(X10,X6))),file('/tmp/SRASS.s.p', sos_49)).
% fof(5, axiom,![X11]:![X12]:![X13]:((occurrence_of(X11,X12)&occurrence_of(X11,X13))=>X12=X13),file('/tmp/SRASS.s.p', sos_08)).
% fof(6, axiom,![X14]:![X15]:![X16]:![X17]:![X18]:![X19]:((send_message(X14,X15,X16,X17,X18)&occurrence_of(X19,X14))=>min_precedes(X17,X19,X18)),file('/tmp/SRASS.s.p', sos_47)).
% fof(8, axiom,![X24]:![X25]:![X26]:![X27]:(((occurrence_of(X26,X27)&root_occ(X24,X26))&root_occ(X25,X26))=>X24=X25),file('/tmp/SRASS.s.p', sos_29)).
% fof(9, axiom,![X28]:![X29]:![X30]:(min_precedes(X29,X30,X28)=>?[X31]:((occurrence_of(X31,X28)&subactivity_occurrence(X29,X31))&subactivity_occurrence(X30,X31))),file('/tmp/SRASS.s.p', sos_06)).
% fof(10, axiom,![X32]:![X33]:![X34]:![X35]:(((min_precedes(X32,X33,X34)&occurrence_of(X35,X34))&subactivity_occurrence(X33,X35))=>subactivity_occurrence(X32,X35)),file('/tmp/SRASS.s.p', sos_27)).
% fof(12, axiom,![X40]:![X41]:![X42]:(tptp1(X40,X41,X42)=>(((activity(X40)&~(atomic(X40)))&~(atomic(X41)))&root(X42,X41))),file('/tmp/SRASS.s.p', sos_48)).
% fof(14, axiom,![X45]:![X46]:((occurrence_of(X46,X45)&~(atomic(X45)))=>?[X47]:(root(X47,X45)&subactivity_occurrence(X47,X46))),file('/tmp/SRASS.s.p', sos)).
% fof(15, axiom,![X48]:![X49]:(root_occ(X48,X49)<=>?[X50]:((occurrence_of(X49,X50)&subactivity_occurrence(X48,X49))&root(X48,X50))),file('/tmp/SRASS.s.p', sos_19)).
% fof(16, axiom,![X51]:![X52]:((leaf(X51,X52)&~(atomic(X52)))=>?[X53]:(occurrence_of(X53,X52)&leaf_occ(X51,X53))),file('/tmp/SRASS.s.p', sos_07)).
% fof(17, axiom,![X54]:![X55]:![X56]:![X57]:((((occurrence_of(X56,X57)&~(atomic(X57)))&leaf_occ(X54,X56))&leaf_occ(X55,X56))=>X54=X55),file('/tmp/SRASS.s.p', sos_28)).
% fof(22, axiom,![X58]:(occurrence_of(X58,tptp0)=>?[X59]:?[X60]:((((occurrence_of(X59,tptp4)&root_occ(X59,X58))&(occurrence_of(X60,tptp3)|occurrence_of(X60,tptp2)))&leaf_occ(X60,X58))&next_subocc(X59,X60,tptp0))),file('/tmp/SRASS.s.p', sos_32)).
% fof(25, axiom,![X66]:![X67]:(occurrence_of(X67,X66)=>(activity(X66)&activity_occurrence(X67))),file('/tmp/SRASS.s.p', sos_03)).
% fof(26, axiom,![X68]:(activity_occurrence(X68)=>?[X69]:(activity(X69)&occurrence_of(X68,X69))),file('/tmp/SRASS.s.p', sos_12)).
% fof(27, axiom,![X70]:![X71]:![X72]:![X73]:![X74]:(send_message(X70,X71,X72,X73,X74)=>((~(X70=tptp4)&~(X70=tptp3))&~(X70=tptp2))),file('/tmp/SRASS.s.p', sos_46)).
% fof(30, axiom,![X84]:![X85]:![X86]:![X87]:(((((occurrence_of(X85,X84)&subactivity_occurrence(X86,X85))&leaf_occ(X87,X85))&arboreal(X86))&~(min_precedes(X86,X87,X84)))=>X87=X86),file('/tmp/SRASS.s.p', sos_02)).
% fof(32, axiom,![X90]:![X91]:(leaf(X90,X91)<=>((root(X90,X91)|?[X92]:min_precedes(X92,X90,X91))&~(?[X93]:min_precedes(X90,X93,X91)))),file('/tmp/SRASS.s.p', sos_15)).
% fof(35, axiom,![X99]:![X100]:![X101]:(min_precedes(X99,X100,X101)=>?[X102]:(root(X102,X101)&min_precedes(X102,X100,X101))),file('/tmp/SRASS.s.p', sos_23)).
% fof(37, axiom,![X106]:![X107]:(leaf_occ(X106,X107)<=>?[X108]:((occurrence_of(X107,X108)&subactivity_occurrence(X106,X107))&leaf(X106,X108))),file('/tmp/SRASS.s.p', sos_18)).
% fof(38, axiom,![X109]:![X110]:![X111]:(min_precedes(X109,X110,X111)=>precedes(X109,X110)),file('/tmp/SRASS.s.p', sos_24)).
% fof(39, axiom,![X112]:![X113]:![X114]:(next_subocc(X112,X113,X114)<=>(min_precedes(X112,X113,X114)&~(?[X115]:(min_precedes(X112,X115,X114)&min_precedes(X115,X113,X114))))),file('/tmp/SRASS.s.p', sos_26)).
% fof(48, axiom,![X123]:(legal(X123)=>arboreal(X123)),file('/tmp/SRASS.s.p', sos_13)).
% fof(49, axiom,![X124]:![X125]:![X126]:(next_subocc(X124,X125,X126)=>(arboreal(X124)&arboreal(X125))),file('/tmp/SRASS.s.p', sos_25)).
% fof(51, axiom,![X132]:![X133]:(precedes(X132,X133)<=>(earlier(X132,X133)&legal(X133))),file('/tmp/SRASS.s.p', sos_21)).
% fof(52, conjecture,~(?[X134]:?[X135]:?[X136]:(tptp1(X134,tptp0,X135)&occurrence_of(X136,X134))),file('/tmp/SRASS.s.p', goals)).
% fof(53, negated_conjecture,~(~(?[X134]:?[X135]:?[X136]:(tptp1(X134,tptp0,X135)&occurrence_of(X136,X134)))),inference(assume_negation,[status(cth)],[52])).
% fof(55, plain,~(atomic(tptp0)),inference(fof_simplification,[status(thm)],[2,theory(equality)])).
% fof(56, plain,![X40]:![X41]:![X42]:(tptp1(X40,X41,X42)=>(((activity(X40)&~(atomic(X40)))&~(atomic(X41)))&root(X42,X41))),inference(fof_simplification,[status(thm)],[12,theory(equality)])).
% fof(57, plain,![X45]:![X46]:((occurrence_of(X46,X45)&~(atomic(X45)))=>?[X47]:(root(X47,X45)&subactivity_occurrence(X47,X46))),inference(fof_simplification,[status(thm)],[14,theory(equality)])).
% fof(58, plain,![X51]:![X52]:((leaf(X51,X52)&~(atomic(X52)))=>?[X53]:(occurrence_of(X53,X52)&leaf_occ(X51,X53))),inference(fof_simplification,[status(thm)],[16,theory(equality)])).
% fof(59, plain,![X54]:![X55]:![X56]:![X57]:((((occurrence_of(X56,X57)&~(atomic(X57)))&leaf_occ(X54,X56))&leaf_occ(X55,X56))=>X54=X55),inference(fof_simplification,[status(thm)],[17,theory(equality)])).
% fof(61, plain,![X84]:![X85]:![X86]:![X87]:(((((occurrence_of(X85,X84)&subactivity_occurrence(X86,X85))&leaf_occ(X87,X85))&arboreal(X86))&~(min_precedes(X86,X87,X84)))=>X87=X86),inference(fof_simplification,[status(thm)],[30,theory(equality)])).
% cnf(65,plain,(~atomic(tptp0)),inference(split_conjunct,[status(thm)],[55])).
% fof(67, plain,![X3]:![X4]:![X5]:![X6]:((~(tptp1(X3,X4,X5))|~(occurrence_of(X6,X3)))|?[X7]:?[X8]:?[X9]:?[X10]:((send_message(X7,X8,X9,X5,X4)&occurrence_of(X10,X7))&root_occ(X10,X6))),inference(fof_nnf,[status(thm)],[4])).
% fof(68, plain,![X11]:![X12]:![X13]:![X14]:((~(tptp1(X11,X12,X13))|~(occurrence_of(X14,X11)))|?[X15]:?[X16]:?[X17]:?[X18]:((send_message(X15,X16,X17,X13,X12)&occurrence_of(X18,X15))&root_occ(X18,X14))),inference(variable_rename,[status(thm)],[67])).
% fof(69, plain,![X11]:![X12]:![X13]:![X14]:((~(tptp1(X11,X12,X13))|~(occurrence_of(X14,X11)))|((send_message(esk1_4(X11,X12,X13,X14),esk2_4(X11,X12,X13,X14),esk3_4(X11,X12,X13,X14),X13,X12)&occurrence_of(esk4_4(X11,X12,X13,X14),esk1_4(X11,X12,X13,X14)))&root_occ(esk4_4(X11,X12,X13,X14),X14))),inference(skolemize,[status(esa)],[68])).
% fof(70, plain,![X11]:![X12]:![X13]:![X14]:(((send_message(esk1_4(X11,X12,X13,X14),esk2_4(X11,X12,X13,X14),esk3_4(X11,X12,X13,X14),X13,X12)|(~(tptp1(X11,X12,X13))|~(occurrence_of(X14,X11))))&(occurrence_of(esk4_4(X11,X12,X13,X14),esk1_4(X11,X12,X13,X14))|(~(tptp1(X11,X12,X13))|~(occurrence_of(X14,X11)))))&(root_occ(esk4_4(X11,X12,X13,X14),X14)|(~(tptp1(X11,X12,X13))|~(occurrence_of(X14,X11))))),inference(distribute,[status(thm)],[69])).
% cnf(71,plain,(root_occ(esk4_4(X2,X3,X4,X1),X1)|~occurrence_of(X1,X2)|~tptp1(X2,X3,X4)),inference(split_conjunct,[status(thm)],[70])).
% cnf(72,plain,(occurrence_of(esk4_4(X2,X3,X4,X1),esk1_4(X2,X3,X4,X1))|~occurrence_of(X1,X2)|~tptp1(X2,X3,X4)),inference(split_conjunct,[status(thm)],[70])).
% cnf(73,plain,(send_message(esk1_4(X2,X3,X4,X1),esk2_4(X2,X3,X4,X1),esk3_4(X2,X3,X4,X1),X4,X3)|~occurrence_of(X1,X2)|~tptp1(X2,X3,X4)),inference(split_conjunct,[status(thm)],[70])).
% fof(74, plain,![X11]:![X12]:![X13]:((~(occurrence_of(X11,X12))|~(occurrence_of(X11,X13)))|X12=X13),inference(fof_nnf,[status(thm)],[5])).
% fof(75, plain,![X14]:![X15]:![X16]:((~(occurrence_of(X14,X15))|~(occurrence_of(X14,X16)))|X15=X16),inference(variable_rename,[status(thm)],[74])).
% cnf(76,plain,(X1=X2|~occurrence_of(X3,X2)|~occurrence_of(X3,X1)),inference(split_conjunct,[status(thm)],[75])).
% fof(77, plain,![X14]:![X15]:![X16]:![X17]:![X18]:![X19]:((~(send_message(X14,X15,X16,X17,X18))|~(occurrence_of(X19,X14)))|min_precedes(X17,X19,X18)),inference(fof_nnf,[status(thm)],[6])).
% fof(78, plain,![X20]:![X21]:![X22]:![X23]:![X24]:![X25]:((~(send_message(X20,X21,X22,X23,X24))|~(occurrence_of(X25,X20)))|min_precedes(X23,X25,X24)),inference(variable_rename,[status(thm)],[77])).
% cnf(79,plain,(min_precedes(X1,X2,X3)|~occurrence_of(X2,X4)|~send_message(X4,X5,X6,X1,X3)),inference(split_conjunct,[status(thm)],[78])).
% fof(84, plain,![X24]:![X25]:![X26]:![X27]:(((~(occurrence_of(X26,X27))|~(root_occ(X24,X26)))|~(root_occ(X25,X26)))|X24=X25),inference(fof_nnf,[status(thm)],[8])).
% fof(85, plain,![X28]:![X29]:![X30]:![X31]:(((~(occurrence_of(X30,X31))|~(root_occ(X28,X30)))|~(root_occ(X29,X30)))|X28=X29),inference(variable_rename,[status(thm)],[84])).
% cnf(86,plain,(X1=X2|~root_occ(X2,X3)|~root_occ(X1,X3)|~occurrence_of(X3,X4)),inference(split_conjunct,[status(thm)],[85])).
% fof(87, plain,![X28]:![X29]:![X30]:(~(min_precedes(X29,X30,X28))|?[X31]:((occurrence_of(X31,X28)&subactivity_occurrence(X29,X31))&subactivity_occurrence(X30,X31))),inference(fof_nnf,[status(thm)],[9])).
% fof(88, plain,![X32]:![X33]:![X34]:(~(min_precedes(X33,X34,X32))|?[X35]:((occurrence_of(X35,X32)&subactivity_occurrence(X33,X35))&subactivity_occurrence(X34,X35))),inference(variable_rename,[status(thm)],[87])).
% fof(89, plain,![X32]:![X33]:![X34]:(~(min_precedes(X33,X34,X32))|((occurrence_of(esk5_3(X32,X33,X34),X32)&subactivity_occurrence(X33,esk5_3(X32,X33,X34)))&subactivity_occurrence(X34,esk5_3(X32,X33,X34)))),inference(skolemize,[status(esa)],[88])).
% fof(90, plain,![X32]:![X33]:![X34]:(((occurrence_of(esk5_3(X32,X33,X34),X32)|~(min_precedes(X33,X34,X32)))&(subactivity_occurrence(X33,esk5_3(X32,X33,X34))|~(min_precedes(X33,X34,X32))))&(subactivity_occurrence(X34,esk5_3(X32,X33,X34))|~(min_precedes(X33,X34,X32)))),inference(distribute,[status(thm)],[89])).
% cnf(91,plain,(subactivity_occurrence(X2,esk5_3(X3,X1,X2))|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[90])).
% cnf(92,plain,(subactivity_occurrence(X1,esk5_3(X3,X1,X2))|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[90])).
% cnf(93,plain,(occurrence_of(esk5_3(X3,X1,X2),X3)|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[90])).
% fof(94, plain,![X32]:![X33]:![X34]:![X35]:(((~(min_precedes(X32,X33,X34))|~(occurrence_of(X35,X34)))|~(subactivity_occurrence(X33,X35)))|subactivity_occurrence(X32,X35)),inference(fof_nnf,[status(thm)],[10])).
% fof(95, plain,![X36]:![X37]:![X38]:![X39]:(((~(min_precedes(X36,X37,X38))|~(occurrence_of(X39,X38)))|~(subactivity_occurrence(X37,X39)))|subactivity_occurrence(X36,X39)),inference(variable_rename,[status(thm)],[94])).
% cnf(96,plain,(subactivity_occurrence(X1,X2)|~subactivity_occurrence(X3,X2)|~occurrence_of(X2,X4)|~min_precedes(X1,X3,X4)),inference(split_conjunct,[status(thm)],[95])).
% fof(101, plain,![X40]:![X41]:![X42]:(~(tptp1(X40,X41,X42))|(((activity(X40)&~(atomic(X40)))&~(atomic(X41)))&root(X42,X41))),inference(fof_nnf,[status(thm)],[56])).
% fof(102, plain,![X43]:![X44]:![X45]:(~(tptp1(X43,X44,X45))|(((activity(X43)&~(atomic(X43)))&~(atomic(X44)))&root(X45,X44))),inference(variable_rename,[status(thm)],[101])).
% fof(103, plain,![X43]:![X44]:![X45]:((((activity(X43)|~(tptp1(X43,X44,X45)))&(~(atomic(X43))|~(tptp1(X43,X44,X45))))&(~(atomic(X44))|~(tptp1(X43,X44,X45))))&(root(X45,X44)|~(tptp1(X43,X44,X45)))),inference(distribute,[status(thm)],[102])).
% cnf(104,plain,(root(X3,X2)|~tptp1(X1,X2,X3)),inference(split_conjunct,[status(thm)],[103])).
% cnf(106,plain,(~tptp1(X1,X2,X3)|~atomic(X1)),inference(split_conjunct,[status(thm)],[103])).
% fof(113, plain,![X45]:![X46]:((~(occurrence_of(X46,X45))|atomic(X45))|?[X47]:(root(X47,X45)&subactivity_occurrence(X47,X46))),inference(fof_nnf,[status(thm)],[57])).
% fof(114, plain,![X48]:![X49]:((~(occurrence_of(X49,X48))|atomic(X48))|?[X50]:(root(X50,X48)&subactivity_occurrence(X50,X49))),inference(variable_rename,[status(thm)],[113])).
% fof(115, plain,![X48]:![X49]:((~(occurrence_of(X49,X48))|atomic(X48))|(root(esk6_2(X48,X49),X48)&subactivity_occurrence(esk6_2(X48,X49),X49))),inference(skolemize,[status(esa)],[114])).
% fof(116, plain,![X48]:![X49]:((root(esk6_2(X48,X49),X48)|(~(occurrence_of(X49,X48))|atomic(X48)))&(subactivity_occurrence(esk6_2(X48,X49),X49)|(~(occurrence_of(X49,X48))|atomic(X48)))),inference(distribute,[status(thm)],[115])).
% cnf(117,plain,(atomic(X1)|subactivity_occurrence(esk6_2(X1,X2),X2)|~occurrence_of(X2,X1)),inference(split_conjunct,[status(thm)],[116])).
% cnf(118,plain,(atomic(X1)|root(esk6_2(X1,X2),X1)|~occurrence_of(X2,X1)),inference(split_conjunct,[status(thm)],[116])).
% fof(119, plain,![X48]:![X49]:((~(root_occ(X48,X49))|?[X50]:((occurrence_of(X49,X50)&subactivity_occurrence(X48,X49))&root(X48,X50)))&(![X50]:((~(occurrence_of(X49,X50))|~(subactivity_occurrence(X48,X49)))|~(root(X48,X50)))|root_occ(X48,X49))),inference(fof_nnf,[status(thm)],[15])).
% fof(120, plain,![X51]:![X52]:((~(root_occ(X51,X52))|?[X53]:((occurrence_of(X52,X53)&subactivity_occurrence(X51,X52))&root(X51,X53)))&(![X54]:((~(occurrence_of(X52,X54))|~(subactivity_occurrence(X51,X52)))|~(root(X51,X54)))|root_occ(X51,X52))),inference(variable_rename,[status(thm)],[119])).
% fof(121, plain,![X51]:![X52]:((~(root_occ(X51,X52))|((occurrence_of(X52,esk7_2(X51,X52))&subactivity_occurrence(X51,X52))&root(X51,esk7_2(X51,X52))))&(![X54]:((~(occurrence_of(X52,X54))|~(subactivity_occurrence(X51,X52)))|~(root(X51,X54)))|root_occ(X51,X52))),inference(skolemize,[status(esa)],[120])).
% fof(122, plain,![X51]:![X52]:![X54]:((((~(occurrence_of(X52,X54))|~(subactivity_occurrence(X51,X52)))|~(root(X51,X54)))|root_occ(X51,X52))&(~(root_occ(X51,X52))|((occurrence_of(X52,esk7_2(X51,X52))&subactivity_occurrence(X51,X52))&root(X51,esk7_2(X51,X52))))),inference(shift_quantors,[status(thm)],[121])).
% fof(123, plain,![X51]:![X52]:![X54]:((((~(occurrence_of(X52,X54))|~(subactivity_occurrence(X51,X52)))|~(root(X51,X54)))|root_occ(X51,X52))&(((occurrence_of(X52,esk7_2(X51,X52))|~(root_occ(X51,X52)))&(subactivity_occurrence(X51,X52)|~(root_occ(X51,X52))))&(root(X51,esk7_2(X51,X52))|~(root_occ(X51,X52))))),inference(distribute,[status(thm)],[122])).
% cnf(127,plain,(root_occ(X1,X2)|~root(X1,X3)|~subactivity_occurrence(X1,X2)|~occurrence_of(X2,X3)),inference(split_conjunct,[status(thm)],[123])).
% fof(128, plain,![X51]:![X52]:((~(leaf(X51,X52))|atomic(X52))|?[X53]:(occurrence_of(X53,X52)&leaf_occ(X51,X53))),inference(fof_nnf,[status(thm)],[58])).
% fof(129, plain,![X54]:![X55]:((~(leaf(X54,X55))|atomic(X55))|?[X56]:(occurrence_of(X56,X55)&leaf_occ(X54,X56))),inference(variable_rename,[status(thm)],[128])).
% fof(130, plain,![X54]:![X55]:((~(leaf(X54,X55))|atomic(X55))|(occurrence_of(esk8_2(X54,X55),X55)&leaf_occ(X54,esk8_2(X54,X55)))),inference(skolemize,[status(esa)],[129])).
% fof(131, plain,![X54]:![X55]:((occurrence_of(esk8_2(X54,X55),X55)|(~(leaf(X54,X55))|atomic(X55)))&(leaf_occ(X54,esk8_2(X54,X55))|(~(leaf(X54,X55))|atomic(X55)))),inference(distribute,[status(thm)],[130])).
% cnf(132,plain,(atomic(X1)|leaf_occ(X2,esk8_2(X2,X1))|~leaf(X2,X1)),inference(split_conjunct,[status(thm)],[131])).
% cnf(133,plain,(atomic(X1)|occurrence_of(esk8_2(X2,X1),X1)|~leaf(X2,X1)),inference(split_conjunct,[status(thm)],[131])).
% fof(134, plain,![X54]:![X55]:![X56]:![X57]:((((~(occurrence_of(X56,X57))|atomic(X57))|~(leaf_occ(X54,X56)))|~(leaf_occ(X55,X56)))|X54=X55),inference(fof_nnf,[status(thm)],[59])).
% fof(135, plain,![X58]:![X59]:![X60]:![X61]:((((~(occurrence_of(X60,X61))|atomic(X61))|~(leaf_occ(X58,X60)))|~(leaf_occ(X59,X60)))|X58=X59),inference(variable_rename,[status(thm)],[134])).
% cnf(136,plain,(X1=X2|atomic(X4)|~leaf_occ(X2,X3)|~leaf_occ(X1,X3)|~occurrence_of(X3,X4)),inference(split_conjunct,[status(thm)],[135])).
% fof(141, plain,![X58]:(~(occurrence_of(X58,tptp0))|?[X59]:?[X60]:((((occurrence_of(X59,tptp4)&root_occ(X59,X58))&(occurrence_of(X60,tptp3)|occurrence_of(X60,tptp2)))&leaf_occ(X60,X58))&next_subocc(X59,X60,tptp0))),inference(fof_nnf,[status(thm)],[22])).
% fof(142, plain,![X61]:(~(occurrence_of(X61,tptp0))|?[X62]:?[X63]:((((occurrence_of(X62,tptp4)&root_occ(X62,X61))&(occurrence_of(X63,tptp3)|occurrence_of(X63,tptp2)))&leaf_occ(X63,X61))&next_subocc(X62,X63,tptp0))),inference(variable_rename,[status(thm)],[141])).
% fof(143, plain,![X61]:(~(occurrence_of(X61,tptp0))|((((occurrence_of(esk9_1(X61),tptp4)&root_occ(esk9_1(X61),X61))&(occurrence_of(esk10_1(X61),tptp3)|occurrence_of(esk10_1(X61),tptp2)))&leaf_occ(esk10_1(X61),X61))&next_subocc(esk9_1(X61),esk10_1(X61),tptp0))),inference(skolemize,[status(esa)],[142])).
% fof(144, plain,![X61]:(((((occurrence_of(esk9_1(X61),tptp4)|~(occurrence_of(X61,tptp0)))&(root_occ(esk9_1(X61),X61)|~(occurrence_of(X61,tptp0))))&((occurrence_of(esk10_1(X61),tptp3)|occurrence_of(esk10_1(X61),tptp2))|~(occurrence_of(X61,tptp0))))&(leaf_occ(esk10_1(X61),X61)|~(occurrence_of(X61,tptp0))))&(next_subocc(esk9_1(X61),esk10_1(X61),tptp0)|~(occurrence_of(X61,tptp0)))),inference(distribute,[status(thm)],[143])).
% cnf(145,plain,(next_subocc(esk9_1(X1),esk10_1(X1),tptp0)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[144])).
% cnf(146,plain,(leaf_occ(esk10_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[144])).
% cnf(147,plain,(occurrence_of(esk10_1(X1),tptp2)|occurrence_of(esk10_1(X1),tptp3)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[144])).
% cnf(148,plain,(root_occ(esk9_1(X1),X1)|~occurrence_of(X1,tptp0)),inference(split_conjunct,[status(thm)],[144])).
% fof(156, plain,![X66]:![X67]:(~(occurrence_of(X67,X66))|(activity(X66)&activity_occurrence(X67))),inference(fof_nnf,[status(thm)],[25])).
% fof(157, plain,![X68]:![X69]:(~(occurrence_of(X69,X68))|(activity(X68)&activity_occurrence(X69))),inference(variable_rename,[status(thm)],[156])).
% fof(158, plain,![X68]:![X69]:((activity(X68)|~(occurrence_of(X69,X68)))&(activity_occurrence(X69)|~(occurrence_of(X69,X68)))),inference(distribute,[status(thm)],[157])).
% cnf(159,plain,(activity_occurrence(X1)|~occurrence_of(X1,X2)),inference(split_conjunct,[status(thm)],[158])).
% fof(161, plain,![X68]:(~(activity_occurrence(X68))|?[X69]:(activity(X69)&occurrence_of(X68,X69))),inference(fof_nnf,[status(thm)],[26])).
% fof(162, plain,![X70]:(~(activity_occurrence(X70))|?[X71]:(activity(X71)&occurrence_of(X70,X71))),inference(variable_rename,[status(thm)],[161])).
% fof(163, plain,![X70]:(~(activity_occurrence(X70))|(activity(esk11_1(X70))&occurrence_of(X70,esk11_1(X70)))),inference(skolemize,[status(esa)],[162])).
% fof(164, plain,![X70]:((activity(esk11_1(X70))|~(activity_occurrence(X70)))&(occurrence_of(X70,esk11_1(X70))|~(activity_occurrence(X70)))),inference(distribute,[status(thm)],[163])).
% cnf(165,plain,(occurrence_of(X1,esk11_1(X1))|~activity_occurrence(X1)),inference(split_conjunct,[status(thm)],[164])).
% fof(167, plain,![X70]:![X71]:![X72]:![X73]:![X74]:(~(send_message(X70,X71,X72,X73,X74))|((~(X70=tptp4)&~(X70=tptp3))&~(X70=tptp2))),inference(fof_nnf,[status(thm)],[27])).
% fof(168, plain,![X75]:![X76]:![X77]:![X78]:![X79]:(~(send_message(X75,X76,X77,X78,X79))|((~(X75=tptp4)&~(X75=tptp3))&~(X75=tptp2))),inference(variable_rename,[status(thm)],[167])).
% fof(169, plain,![X75]:![X76]:![X77]:![X78]:![X79]:(((~(X75=tptp4)|~(send_message(X75,X76,X77,X78,X79)))&(~(X75=tptp3)|~(send_message(X75,X76,X77,X78,X79))))&(~(X75=tptp2)|~(send_message(X75,X76,X77,X78,X79)))),inference(distribute,[status(thm)],[168])).
% cnf(170,plain,(~send_message(X1,X2,X3,X4,X5)|X1!=tptp2),inference(split_conjunct,[status(thm)],[169])).
% cnf(171,plain,(~send_message(X1,X2,X3,X4,X5)|X1!=tptp3),inference(split_conjunct,[status(thm)],[169])).
% fof(179, plain,![X84]:![X85]:![X86]:![X87]:(((((~(occurrence_of(X85,X84))|~(subactivity_occurrence(X86,X85)))|~(leaf_occ(X87,X85)))|~(arboreal(X86)))|min_precedes(X86,X87,X84))|X87=X86),inference(fof_nnf,[status(thm)],[61])).
% fof(180, plain,![X88]:![X89]:![X90]:![X91]:(((((~(occurrence_of(X89,X88))|~(subactivity_occurrence(X90,X89)))|~(leaf_occ(X91,X89)))|~(arboreal(X90)))|min_precedes(X90,X91,X88))|X91=X90),inference(variable_rename,[status(thm)],[179])).
% cnf(181,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)],[180])).
% fof(187, plain,![X90]:![X91]:((~(leaf(X90,X91))|((root(X90,X91)|?[X92]:min_precedes(X92,X90,X91))&![X93]:~(min_precedes(X90,X93,X91))))&(((~(root(X90,X91))&![X92]:~(min_precedes(X92,X90,X91)))|?[X93]:min_precedes(X90,X93,X91))|leaf(X90,X91))),inference(fof_nnf,[status(thm)],[32])).
% fof(188, plain,![X94]:![X95]:((~(leaf(X94,X95))|((root(X94,X95)|?[X96]:min_precedes(X96,X94,X95))&![X97]:~(min_precedes(X94,X97,X95))))&(((~(root(X94,X95))&![X98]:~(min_precedes(X98,X94,X95)))|?[X99]:min_precedes(X94,X99,X95))|leaf(X94,X95))),inference(variable_rename,[status(thm)],[187])).
% fof(189, plain,![X94]:![X95]:((~(leaf(X94,X95))|((root(X94,X95)|min_precedes(esk12_2(X94,X95),X94,X95))&![X97]:~(min_precedes(X94,X97,X95))))&(((~(root(X94,X95))&![X98]:~(min_precedes(X98,X94,X95)))|min_precedes(X94,esk13_2(X94,X95),X95))|leaf(X94,X95))),inference(skolemize,[status(esa)],[188])).
% fof(190, plain,![X94]:![X95]:![X97]:![X98]:((((~(min_precedes(X98,X94,X95))&~(root(X94,X95)))|min_precedes(X94,esk13_2(X94,X95),X95))|leaf(X94,X95))&((~(min_precedes(X94,X97,X95))&(root(X94,X95)|min_precedes(esk12_2(X94,X95),X94,X95)))|~(leaf(X94,X95)))),inference(shift_quantors,[status(thm)],[189])).
% fof(191, plain,![X94]:![X95]:![X97]:![X98]:((((~(min_precedes(X98,X94,X95))|min_precedes(X94,esk13_2(X94,X95),X95))|leaf(X94,X95))&((~(root(X94,X95))|min_precedes(X94,esk13_2(X94,X95),X95))|leaf(X94,X95)))&((~(min_precedes(X94,X97,X95))|~(leaf(X94,X95)))&((root(X94,X95)|min_precedes(esk12_2(X94,X95),X94,X95))|~(leaf(X94,X95))))),inference(distribute,[status(thm)],[190])).
% cnf(193,plain,(~leaf(X1,X2)|~min_precedes(X1,X3,X2)),inference(split_conjunct,[status(thm)],[191])).
% fof(202, plain,![X99]:![X100]:![X101]:(~(min_precedes(X99,X100,X101))|?[X102]:(root(X102,X101)&min_precedes(X102,X100,X101))),inference(fof_nnf,[status(thm)],[35])).
% fof(203, plain,![X103]:![X104]:![X105]:(~(min_precedes(X103,X104,X105))|?[X106]:(root(X106,X105)&min_precedes(X106,X104,X105))),inference(variable_rename,[status(thm)],[202])).
% fof(204, plain,![X103]:![X104]:![X105]:(~(min_precedes(X103,X104,X105))|(root(esk14_3(X103,X104,X105),X105)&min_precedes(esk14_3(X103,X104,X105),X104,X105))),inference(skolemize,[status(esa)],[203])).
% fof(205, plain,![X103]:![X104]:![X105]:((root(esk14_3(X103,X104,X105),X105)|~(min_precedes(X103,X104,X105)))&(min_precedes(esk14_3(X103,X104,X105),X104,X105)|~(min_precedes(X103,X104,X105)))),inference(distribute,[status(thm)],[204])).
% cnf(206,plain,(min_precedes(esk14_3(X1,X2,X3),X2,X3)|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[205])).
% fof(214, plain,![X106]:![X107]:((~(leaf_occ(X106,X107))|?[X108]:((occurrence_of(X107,X108)&subactivity_occurrence(X106,X107))&leaf(X106,X108)))&(![X108]:((~(occurrence_of(X107,X108))|~(subactivity_occurrence(X106,X107)))|~(leaf(X106,X108)))|leaf_occ(X106,X107))),inference(fof_nnf,[status(thm)],[37])).
% fof(215, plain,![X109]:![X110]:((~(leaf_occ(X109,X110))|?[X111]:((occurrence_of(X110,X111)&subactivity_occurrence(X109,X110))&leaf(X109,X111)))&(![X112]:((~(occurrence_of(X110,X112))|~(subactivity_occurrence(X109,X110)))|~(leaf(X109,X112)))|leaf_occ(X109,X110))),inference(variable_rename,[status(thm)],[214])).
% fof(216, plain,![X109]:![X110]:((~(leaf_occ(X109,X110))|((occurrence_of(X110,esk16_2(X109,X110))&subactivity_occurrence(X109,X110))&leaf(X109,esk16_2(X109,X110))))&(![X112]:((~(occurrence_of(X110,X112))|~(subactivity_occurrence(X109,X110)))|~(leaf(X109,X112)))|leaf_occ(X109,X110))),inference(skolemize,[status(esa)],[215])).
% fof(217, plain,![X109]:![X110]:![X112]:((((~(occurrence_of(X110,X112))|~(subactivity_occurrence(X109,X110)))|~(leaf(X109,X112)))|leaf_occ(X109,X110))&(~(leaf_occ(X109,X110))|((occurrence_of(X110,esk16_2(X109,X110))&subactivity_occurrence(X109,X110))&leaf(X109,esk16_2(X109,X110))))),inference(shift_quantors,[status(thm)],[216])).
% fof(218, plain,![X109]:![X110]:![X112]:((((~(occurrence_of(X110,X112))|~(subactivity_occurrence(X109,X110)))|~(leaf(X109,X112)))|leaf_occ(X109,X110))&(((occurrence_of(X110,esk16_2(X109,X110))|~(leaf_occ(X109,X110)))&(subactivity_occurrence(X109,X110)|~(leaf_occ(X109,X110))))&(leaf(X109,esk16_2(X109,X110))|~(leaf_occ(X109,X110))))),inference(distribute,[status(thm)],[217])).
% cnf(219,plain,(leaf(X1,esk16_2(X1,X2))|~leaf_occ(X1,X2)),inference(split_conjunct,[status(thm)],[218])).
% cnf(221,plain,(occurrence_of(X2,esk16_2(X1,X2))|~leaf_occ(X1,X2)),inference(split_conjunct,[status(thm)],[218])).
% fof(223, plain,![X109]:![X110]:![X111]:(~(min_precedes(X109,X110,X111))|precedes(X109,X110)),inference(fof_nnf,[status(thm)],[38])).
% fof(224, plain,![X112]:![X113]:![X114]:(~(min_precedes(X112,X113,X114))|precedes(X112,X113)),inference(variable_rename,[status(thm)],[223])).
% cnf(225,plain,(precedes(X1,X2)|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[224])).
% fof(226, plain,![X112]:![X113]:![X114]:((~(next_subocc(X112,X113,X114))|(min_precedes(X112,X113,X114)&![X115]:(~(min_precedes(X112,X115,X114))|~(min_precedes(X115,X113,X114)))))&((~(min_precedes(X112,X113,X114))|?[X115]:(min_precedes(X112,X115,X114)&min_precedes(X115,X113,X114)))|next_subocc(X112,X113,X114))),inference(fof_nnf,[status(thm)],[39])).
% fof(227, plain,![X116]:![X117]:![X118]:((~(next_subocc(X116,X117,X118))|(min_precedes(X116,X117,X118)&![X119]:(~(min_precedes(X116,X119,X118))|~(min_precedes(X119,X117,X118)))))&((~(min_precedes(X116,X117,X118))|?[X120]:(min_precedes(X116,X120,X118)&min_precedes(X120,X117,X118)))|next_subocc(X116,X117,X118))),inference(variable_rename,[status(thm)],[226])).
% fof(228, plain,![X116]:![X117]:![X118]:((~(next_subocc(X116,X117,X118))|(min_precedes(X116,X117,X118)&![X119]:(~(min_precedes(X116,X119,X118))|~(min_precedes(X119,X117,X118)))))&((~(min_precedes(X116,X117,X118))|(min_precedes(X116,esk17_3(X116,X117,X118),X118)&min_precedes(esk17_3(X116,X117,X118),X117,X118)))|next_subocc(X116,X117,X118))),inference(skolemize,[status(esa)],[227])).
% fof(229, plain,![X116]:![X117]:![X118]:![X119]:((((~(min_precedes(X116,X119,X118))|~(min_precedes(X119,X117,X118)))&min_precedes(X116,X117,X118))|~(next_subocc(X116,X117,X118)))&((~(min_precedes(X116,X117,X118))|(min_precedes(X116,esk17_3(X116,X117,X118),X118)&min_precedes(esk17_3(X116,X117,X118),X117,X118)))|next_subocc(X116,X117,X118))),inference(shift_quantors,[status(thm)],[228])).
% fof(230, plain,![X116]:![X117]:![X118]:![X119]:((((~(min_precedes(X116,X119,X118))|~(min_precedes(X119,X117,X118)))|~(next_subocc(X116,X117,X118)))&(min_precedes(X116,X117,X118)|~(next_subocc(X116,X117,X118))))&(((min_precedes(X116,esk17_3(X116,X117,X118),X118)|~(min_precedes(X116,X117,X118)))|next_subocc(X116,X117,X118))&((min_precedes(esk17_3(X116,X117,X118),X117,X118)|~(min_precedes(X116,X117,X118)))|next_subocc(X116,X117,X118)))),inference(distribute,[status(thm)],[229])).
% cnf(231,plain,(next_subocc(X1,X2,X3)|min_precedes(esk17_3(X1,X2,X3),X2,X3)|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[230])).
% cnf(232,plain,(next_subocc(X1,X2,X3)|min_precedes(X1,esk17_3(X1,X2,X3),X3)|~min_precedes(X1,X2,X3)),inference(split_conjunct,[status(thm)],[230])).
% cnf(233,plain,(min_precedes(X1,X2,X3)|~next_subocc(X1,X2,X3)),inference(split_conjunct,[status(thm)],[230])).
% cnf(234,plain,(~next_subocc(X1,X2,X3)|~min_precedes(X4,X2,X3)|~min_precedes(X1,X4,X3)),inference(split_conjunct,[status(thm)],[230])).
% fof(253, plain,![X123]:(~(legal(X123))|arboreal(X123)),inference(fof_nnf,[status(thm)],[48])).
% fof(254, plain,![X124]:(~(legal(X124))|arboreal(X124)),inference(variable_rename,[status(thm)],[253])).
% cnf(255,plain,(arboreal(X1)|~legal(X1)),inference(split_conjunct,[status(thm)],[254])).
% fof(256, plain,![X124]:![X125]:![X126]:(~(next_subocc(X124,X125,X126))|(arboreal(X124)&arboreal(X125))),inference(fof_nnf,[status(thm)],[49])).
% fof(257, plain,![X127]:![X128]:![X129]:(~(next_subocc(X127,X128,X129))|(arboreal(X127)&arboreal(X128))),inference(variable_rename,[status(thm)],[256])).
% fof(258, plain,![X127]:![X128]:![X129]:((arboreal(X127)|~(next_subocc(X127,X128,X129)))&(arboreal(X128)|~(next_subocc(X127,X128,X129)))),inference(distribute,[status(thm)],[257])).
% cnf(259,plain,(arboreal(X2)|~next_subocc(X1,X2,X3)),inference(split_conjunct,[status(thm)],[258])).
% fof(268, plain,![X132]:![X133]:((~(precedes(X132,X133))|(earlier(X132,X133)&legal(X133)))&((~(earlier(X132,X133))|~(legal(X133)))|precedes(X132,X133))),inference(fof_nnf,[status(thm)],[51])).
% fof(269, plain,![X134]:![X135]:((~(precedes(X134,X135))|(earlier(X134,X135)&legal(X135)))&((~(earlier(X134,X135))|~(legal(X135)))|precedes(X134,X135))),inference(variable_rename,[status(thm)],[268])).
% fof(270, plain,![X134]:![X135]:(((earlier(X134,X135)|~(precedes(X134,X135)))&(legal(X135)|~(precedes(X134,X135))))&((~(earlier(X134,X135))|~(legal(X135)))|precedes(X134,X135))),inference(distribute,[status(thm)],[269])).
% cnf(272,plain,(legal(X2)|~precedes(X1,X2)),inference(split_conjunct,[status(thm)],[270])).
% fof(274, negated_conjecture,?[X134]:?[X135]:?[X136]:(tptp1(X134,tptp0,X135)&occurrence_of(X136,X134)),inference(fof_nnf,[status(thm)],[53])).
% fof(275, negated_conjecture,?[X137]:?[X138]:?[X139]:(tptp1(X137,tptp0,X138)&occurrence_of(X139,X137)),inference(variable_rename,[status(thm)],[274])).
% fof(276, negated_conjecture,(tptp1(esk19_0,tptp0,esk20_0)&occurrence_of(esk21_0,esk19_0)),inference(skolemize,[status(esa)],[275])).
% cnf(277,negated_conjecture,(occurrence_of(esk21_0,esk19_0)),inference(split_conjunct,[status(thm)],[276])).
% cnf(278,negated_conjecture,(tptp1(esk19_0,tptp0,esk20_0)),inference(split_conjunct,[status(thm)],[276])).
% cnf(280,negated_conjecture,(~atomic(esk19_0)),inference(spm,[status(thm)],[106,278,theory(equality)])).
% cnf(285,negated_conjecture,(root(esk20_0,tptp0)),inference(spm,[status(thm)],[104,278,theory(equality)])).
% cnf(287,plain,(X1=esk11_1(X2)|~occurrence_of(X2,X1)|~activity_occurrence(X2)),inference(spm,[status(thm)],[76,165,theory(equality)])).
% cnf(309,plain,(X1=esk9_1(X2)|~root_occ(X1,X2)|~occurrence_of(X2,X3)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[86,148,theory(equality)])).
% cnf(333,plain,(min_precedes(esk9_1(X1),esk10_1(X1),tptp0)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[233,145,theory(equality)])).
% cnf(334,plain,(~min_precedes(X2,esk10_1(X1),tptp0)|~min_precedes(esk9_1(X1),X2,tptp0)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[234,145,theory(equality)])).
% cnf(351,plain,(X1=esk4_4(X2,X3,X4,X5)|~root_occ(X1,X5)|~occurrence_of(X5,X6)|~occurrence_of(X5,X2)|~tptp1(X2,X3,X4)),inference(spm,[status(thm)],[86,71,theory(equality)])).
% cnf(352,plain,(X1=esk10_1(X2)|atomic(X3)|~leaf_occ(X1,X2)|~occurrence_of(X2,X3)|~occurrence_of(X2,tptp0)),inference(spm,[status(thm)],[136,146,theory(equality)])).
% cnf(356,plain,(root_occ(esk6_2(X1,X2),X3)|atomic(X1)|~subactivity_occurrence(esk6_2(X1,X2),X3)|~occurrence_of(X3,X1)|~occurrence_of(X2,X1)),inference(spm,[status(thm)],[127,118,theory(equality)])).
% cnf(359,plain,(precedes(esk14_3(X1,X2,X3),X2)|~min_precedes(X1,X2,X3)),inference(spm,[status(thm)],[225,206,theory(equality)])).
% cnf(373,plain,(esk10_1(X1)=X2|min_precedes(X2,esk10_1(X1),X3)|~arboreal(X2)|~subactivity_occurrence(X2,X1)|~occurrence_of(X1,X3)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[181,146,theory(equality)])).
% cnf(414,plain,(tptp3!=esk1_4(X1,X2,X3,X4)|~occurrence_of(X4,X1)|~tptp1(X1,X2,X3)),inference(spm,[status(thm)],[171,73,theory(equality)])).
% cnf(415,plain,(tptp2!=esk1_4(X1,X2,X3,X4)|~occurrence_of(X4,X1)|~tptp1(X1,X2,X3)),inference(spm,[status(thm)],[170,73,theory(equality)])).
% cnf(418,plain,(min_precedes(X1,X2,X3)|~occurrence_of(X2,esk1_4(X4,X3,X1,X5))|~occurrence_of(X5,X4)|~tptp1(X4,X3,X1)),inference(spm,[status(thm)],[79,73,theory(equality)])).
% cnf(432,negated_conjecture,(root_occ(esk20_0,X1)|~subactivity_occurrence(esk20_0,X1)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[127,285,theory(equality)])).
% cnf(445,plain,(X1=esk11_1(X2)|~occurrence_of(X2,X1)),inference(csr,[status(thm)],[287,159])).
% cnf(447,plain,(tptp2=esk11_1(esk10_1(X1))|occurrence_of(esk10_1(X1),tptp3)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[445,147,theory(equality)])).
% cnf(450,plain,(X1=esk11_1(esk5_3(X1,X2,X3))|~min_precedes(X2,X3,X1)),inference(spm,[status(thm)],[445,93,theory(equality)])).
% cnf(451,plain,(esk1_4(X1,X2,X3,X4)=esk11_1(esk4_4(X1,X2,X3,X4))|~occurrence_of(X4,X1)|~tptp1(X1,X2,X3)),inference(spm,[status(thm)],[445,72,theory(equality)])).
% cnf(453,plain,(esk16_2(X1,X2)=esk11_1(X2)|~leaf_occ(X1,X2)),inference(spm,[status(thm)],[445,221,theory(equality)])).
% cnf(534,plain,(leaf(X1,esk11_1(X2))|~leaf_occ(X1,X2)),inference(spm,[status(thm)],[219,453,theory(equality)])).
% cnf(535,plain,(occurrence_of(X1,esk11_1(X1))|~leaf_occ(X2,X1)),inference(spm,[status(thm)],[221,453,theory(equality)])).
% cnf(571,plain,(occurrence_of(X1,esk11_1(X1))|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[535,146,theory(equality)])).
% cnf(676,negated_conjecture,(esk20_0=esk9_1(X1)|~occurrence_of(X1,tptp0)|~occurrence_of(X1,X2)|~subactivity_occurrence(esk20_0,X1)),inference(spm,[status(thm)],[309,432,theory(equality)])).
% cnf(739,negated_conjecture,(esk9_1(X1)=esk20_0|~subactivity_occurrence(esk20_0,X1)|~occurrence_of(X1,tptp0)),inference(spm,[status(thm)],[676,571,theory(equality)])).
% cnf(836,negated_conjecture,(~min_precedes(X1,esk10_1(X2),tptp0)|~min_precedes(esk20_0,X1,tptp0)|~occurrence_of(X2,tptp0)|~subactivity_occurrence(esk20_0,X2)),inference(spm,[status(thm)],[334,739,theory(equality)])).
% cnf(953,plain,(X1=esk10_1(esk8_2(X1,X2))|atomic(X3)|atomic(X2)|~occurrence_of(esk8_2(X1,X2),tptp0)|~occurrence_of(esk8_2(X1,X2),X3)|~leaf(X1,X2)),inference(spm,[status(thm)],[352,132,theory(equality)])).
% cnf(997,plain,(leaf(X1,X2)|~leaf_occ(X1,esk5_3(X2,X3,X4))|~min_precedes(X3,X4,X2)),inference(spm,[status(thm)],[534,450,theory(equality)])).
% cnf(1016,plain,(esk6_2(X1,X2)=esk4_4(X3,X4,X5,X6)|atomic(X1)|~occurrence_of(X6,X7)|~occurrence_of(X6,X3)|~tptp1(X3,X4,X5)|~subactivity_occurrence(esk6_2(X1,X2),X6)|~occurrence_of(X6,X1)|~occurrence_of(X2,X1)),inference(spm,[status(thm)],[351,356,theory(equality)])).
% cnf(1102,plain,(legal(X1)|~min_precedes(X2,X1,X3)),inference(spm,[status(thm)],[272,359,theory(equality)])).
% cnf(1107,plain,(legal(esk17_3(X1,X2,X3))|next_subocc(X1,X2,X3)|~min_precedes(X1,X2,X3)),inference(spm,[status(thm)],[1102,232,theory(equality)])).
% cnf(1439,plain,(leaf(esk10_1(esk5_3(X1,X2,X3)),X1)|~min_precedes(X2,X3,X1)|~occurrence_of(esk5_3(X1,X2,X3),tptp0)),inference(spm,[status(thm)],[997,146,theory(equality)])).
% cnf(1808,plain,(min_precedes(X1,esk4_4(X2,X3,X1,X4),X3)|~occurrence_of(X4,X2)|~tptp1(X2,X3,X1)),inference(spm,[status(thm)],[418,72,theory(equality)])).
% cnf(3164,negated_conjecture,(esk10_1(X1)=X2|~subactivity_occurrence(esk20_0,X1)|~min_precedes(esk20_0,X2,tptp0)|~occurrence_of(X1,tptp0)|~arboreal(X2)|~subactivity_occurrence(X2,X1)),inference(spm,[status(thm)],[836,373,theory(equality)])).
% cnf(5090,plain,(esk10_1(esk8_2(X1,X2))=X1|atomic(X2)|~leaf(X1,X2)|~occurrence_of(esk8_2(X1,X2),tptp0)),inference(spm,[status(thm)],[953,133,theory(equality)])).
% cnf(5477,plain,(esk6_2(X1,X2)=esk4_4(X3,X4,X5,X2)|atomic(X1)|~occurrence_of(X2,X6)|~occurrence_of(X2,X3)|~occurrence_of(X2,X1)|~tptp1(X3,X4,X5)),inference(spm,[status(thm)],[1016,117,theory(equality)])).
% cnf(5851,plain,(arboreal(esk17_3(X1,X2,X3))|next_subocc(X1,X2,X3)|~min_precedes(X1,X2,X3)),inference(spm,[status(thm)],[255,1107,theory(equality)])).
% cnf(8110,plain,(esk11_1(X1)=tptp2|occurrence_of(X1,tptp3)|atomic(X2)|~occurrence_of(esk8_2(X1,X2),tptp0)|~leaf(X1,X2)),inference(spm,[status(thm)],[447,5090,theory(equality)])).
% cnf(11826,plain,(esk11_1(X1)=tptp2|occurrence_of(X1,tptp3)|atomic(tptp0)|~leaf(X1,tptp0)),inference(spm,[status(thm)],[8110,133,theory(equality)])).
% cnf(11827,plain,(esk11_1(X1)=tptp2|occurrence_of(X1,tptp3)|~leaf(X1,tptp0)),inference(sr,[status(thm)],[11826,65,theory(equality)])).
% cnf(12588,negated_conjecture,(esk10_1(X1)=X2|~arboreal(X2)|~subactivity_occurrence(X2,X1)|~min_precedes(esk20_0,X2,tptp0)|~occurrence_of(X1,tptp0)),inference(csr,[status(thm)],[3164,96])).
% cnf(12597,negated_conjecture,(esk10_1(esk5_3(X1,X2,X3))=X3|~arboreal(X3)|~min_precedes(esk20_0,X3,tptp0)|~occurrence_of(esk5_3(X1,X2,X3),tptp0)|~min_precedes(X2,X3,X1)),inference(spm,[status(thm)],[12588,91,theory(equality)])).
% cnf(12598,negated_conjecture,(esk10_1(esk5_3(X1,X2,X3))=X2|~arboreal(X2)|~min_precedes(esk20_0,X2,tptp0)|~occurrence_of(esk5_3(X1,X2,X3),tptp0)|~min_precedes(X2,X3,X1)),inference(spm,[status(thm)],[12588,92,theory(equality)])).
% cnf(18713,negated_conjecture,(min_precedes(esk9_1(esk5_3(X1,X2,X3)),X3,tptp0)|~occurrence_of(esk5_3(X1,X2,X3),tptp0)|~arboreal(X3)|~min_precedes(esk20_0,X3,tptp0)|~min_precedes(X2,X3,X1)),inference(spm,[status(thm)],[333,12597,theory(equality)])).
% cnf(18806,negated_conjecture,(leaf(X3,X1)|~min_precedes(X2,X3,X1)|~occurrence_of(esk5_3(X1,X2,X3),tptp0)|~arboreal(X3)|~min_precedes(esk20_0,X3,tptp0)),inference(spm,[status(thm)],[1439,12597,theory(equality)])).
% cnf(18817,negated_conjecture,(leaf(X1,tptp0)|~arboreal(X1)|~min_precedes(esk20_0,X1,tptp0)|~min_precedes(X2,X1,tptp0)),inference(spm,[status(thm)],[18806,93,theory(equality)])).
% cnf(19068,negated_conjecture,(leaf(X2,X1)|~min_precedes(X2,X3,X1)|~occurrence_of(esk5_3(X1,X2,X3),tptp0)|~arboreal(X2)|~min_precedes(esk20_0,X2,tptp0)),inference(spm,[status(thm)],[1439,12598,theory(equality)])).
% cnf(19100,negated_conjecture,(~arboreal(X2)|~min_precedes(esk20_0,X2,tptp0)|~min_precedes(X2,X3,X1)|~occurrence_of(esk5_3(X1,X2,X3),tptp0)),inference(csr,[status(thm)],[19068,193])).
% cnf(19101,negated_conjecture,(~arboreal(X1)|~min_precedes(esk20_0,X1,tptp0)|~min_precedes(X1,X2,tptp0)),inference(spm,[status(thm)],[19100,93,theory(equality)])).
% cnf(19108,negated_conjecture,(next_subocc(X1,X2,tptp0)|~arboreal(esk17_3(X1,X2,tptp0))|~min_precedes(esk20_0,esk17_3(X1,X2,tptp0),tptp0)|~min_precedes(X1,X2,tptp0)),inference(spm,[status(thm)],[19101,231,theory(equality)])).
% cnf(22317,negated_conjecture,(esk6_2(X1,esk21_0)=esk4_4(X2,X3,X4,esk21_0)|atomic(X1)|~occurrence_of(esk21_0,X2)|~occurrence_of(esk21_0,X1)|~tptp1(X2,X3,X4)),inference(spm,[status(thm)],[5477,277,theory(equality)])).
% cnf(22337,plain,(esk6_2(X1,X2)=esk4_4(X3,X4,X5,X2)|atomic(X1)|~occurrence_of(X2,X3)|~occurrence_of(X2,X1)|~tptp1(X3,X4,X5)|~activity_occurrence(X2)),inference(spm,[status(thm)],[5477,165,theory(equality)])).
% cnf(22426,negated_conjecture,(min_precedes(X1,esk6_2(X4,esk21_0),X3)|atomic(X4)|~occurrence_of(esk21_0,X2)|~tptp1(X2,X3,X1)|~occurrence_of(esk21_0,X4)),inference(spm,[status(thm)],[1808,22317,theory(equality)])).
% cnf(23513,negated_conjecture,(min_precedes(esk20_0,esk6_2(X1,esk21_0),tptp0)|atomic(X1)|~occurrence_of(esk21_0,esk19_0)|~occurrence_of(esk21_0,X1)),inference(spm,[status(thm)],[22426,278,theory(equality)])).
% cnf(23514,negated_conjecture,(min_precedes(esk20_0,esk6_2(X1,esk21_0),tptp0)|atomic(X1)|$false|~occurrence_of(esk21_0,X1)),inference(rw,[status(thm)],[23513,277,theory(equality)])).
% cnf(23515,negated_conjecture,(min_precedes(esk20_0,esk6_2(X1,esk21_0),tptp0)|atomic(X1)|~occurrence_of(esk21_0,X1)),inference(cn,[status(thm)],[23514,theory(equality)])).
% cnf(24975,plain,(esk6_2(X1,X2)=esk4_4(X3,X4,X5,X2)|atomic(X1)|~occurrence_of(X2,X3)|~occurrence_of(X2,X1)|~tptp1(X3,X4,X5)),inference(csr,[status(thm)],[22337,159])).
% cnf(25002,plain,(esk11_1(esk6_2(X5,X4))=esk1_4(X1,X2,X3,X4)|atomic(X5)|~occurrence_of(X4,X1)|~tptp1(X1,X2,X3)|~occurrence_of(X4,X5)),inference(spm,[status(thm)],[451,24975,theory(equality)])).
% cnf(31584,plain,(atomic(X5)|esk11_1(esk6_2(X5,X4))!=tptp3|~occurrence_of(X4,X1)|~tptp1(X1,X2,X3)|~occurrence_of(X4,X5)),inference(spm,[status(thm)],[414,25002,theory(equality)])).
% cnf(31585,plain,(atomic(X5)|esk11_1(esk6_2(X5,X4))!=tptp2|~occurrence_of(X4,X1)|~tptp1(X1,X2,X3)|~occurrence_of(X4,X5)),inference(spm,[status(thm)],[415,25002,theory(equality)])).
% cnf(31783,plain,(atomic(X1)|occurrence_of(esk6_2(X1,X2),tptp3)|~occurrence_of(X2,X3)|~occurrence_of(X2,X1)|~tptp1(X3,X4,X5)|~leaf(esk6_2(X1,X2),tptp0)),inference(spm,[status(thm)],[31585,11827,theory(equality)])).
% cnf(40917,negated_conjecture,(next_subocc(X1,X2,tptp0)|~min_precedes(esk20_0,esk17_3(X1,X2,tptp0),tptp0)|~min_precedes(X1,X2,tptp0)),inference(csr,[status(thm)],[19108,5851])).
% cnf(40918,negated_conjecture,(next_subocc(esk20_0,X1,tptp0)|~min_precedes(esk20_0,X1,tptp0)),inference(spm,[status(thm)],[40917,232,theory(equality)])).
% cnf(40922,negated_conjecture,(arboreal(X1)|~min_precedes(esk20_0,X1,tptp0)),inference(spm,[status(thm)],[259,40918,theory(equality)])).
% cnf(194787,negated_conjecture,(min_precedes(esk9_1(esk5_3(X1,X2,X3)),X3,tptp0)|~min_precedes(esk20_0,X3,tptp0)|~min_precedes(X2,X3,X1)|~occurrence_of(esk5_3(X1,X2,X3),tptp0)),inference(csr,[status(thm)],[18713,40922])).
% cnf(194876,negated_conjecture,(leaf(X1,tptp0)|~arboreal(X1)|~min_precedes(esk20_0,X1,tptp0)|~min_precedes(X3,X1,X2)|~occurrence_of(esk5_3(X2,X3,X1),tptp0)),inference(spm,[status(thm)],[18817,194787,theory(equality)])).
% cnf(194988,negated_conjecture,(leaf(X1,tptp0)|~min_precedes(esk20_0,X1,tptp0)|~min_precedes(X3,X1,X2)|~occurrence_of(esk5_3(X2,X3,X1),tptp0)),inference(csr,[status(thm)],[194876,40922])).
% cnf(194989,negated_conjecture,(leaf(X1,tptp0)|~min_precedes(esk20_0,X1,tptp0)|~min_precedes(X2,X1,tptp0)),inference(spm,[status(thm)],[194988,93,theory(equality)])).
% cnf(194992,negated_conjecture,(leaf(esk6_2(X1,esk21_0),tptp0)|atomic(X1)|~min_precedes(esk20_0,esk6_2(X1,esk21_0),tptp0)|~occurrence_of(esk21_0,X1)),inference(spm,[status(thm)],[194989,23515,theory(equality)])).
% cnf(195470,negated_conjecture,(leaf(esk6_2(X1,esk21_0),tptp0)|atomic(X1)|~occurrence_of(esk21_0,X1)),inference(csr,[status(thm)],[194992,23515])).
% cnf(195609,negated_conjecture,(occurrence_of(esk6_2(X1,esk21_0),tptp3)|atomic(X1)|~occurrence_of(esk21_0,X2)|~occurrence_of(esk21_0,X1)|~tptp1(X2,X3,X4)),inference(spm,[status(thm)],[31783,195470,theory(equality)])).
% cnf(196439,negated_conjecture,(occurrence_of(esk6_2(X1,esk21_0),tptp3)|atomic(X1)|~occurrence_of(esk21_0,esk19_0)|~occurrence_of(esk21_0,X1)),inference(spm,[status(thm)],[195609,278,theory(equality)])).
% cnf(196440,negated_conjecture,(occurrence_of(esk6_2(X1,esk21_0),tptp3)|atomic(X1)|$false|~occurrence_of(esk21_0,X1)),inference(rw,[status(thm)],[196439,277,theory(equality)])).
% cnf(196441,negated_conjecture,(occurrence_of(esk6_2(X1,esk21_0),tptp3)|atomic(X1)|~occurrence_of(esk21_0,X1)),inference(cn,[status(thm)],[196440,theory(equality)])).
% cnf(196459,negated_conjecture,(tptp3=esk11_1(esk6_2(X1,esk21_0))|atomic(X1)|~occurrence_of(esk21_0,X1)),inference(spm,[status(thm)],[445,196441,theory(equality)])).
% cnf(196971,negated_conjecture,(atomic(X1)|~occurrence_of(esk21_0,X2)|~occurrence_of(esk21_0,X1)|~tptp1(X2,X3,X4)),inference(spm,[status(thm)],[31584,196459,theory(equality)])).
% cnf(197100,negated_conjecture,(atomic(X1)|~occurrence_of(esk21_0,esk19_0)|~occurrence_of(esk21_0,X1)),inference(spm,[status(thm)],[196971,278,theory(equality)])).
% cnf(197101,negated_conjecture,(atomic(X1)|$false|~occurrence_of(esk21_0,X1)),inference(rw,[status(thm)],[197100,277,theory(equality)])).
% cnf(197102,negated_conjecture,(atomic(X1)|~occurrence_of(esk21_0,X1)),inference(cn,[status(thm)],[197101,theory(equality)])).
% cnf(197117,negated_conjecture,(~occurrence_of(esk21_0,esk19_0)),inference(spm,[status(thm)],[280,197102,theory(equality)])).
% cnf(197144,negated_conjecture,($false),inference(rw,[status(thm)],[197117,277,theory(equality)])).
% cnf(197145,negated_conjecture,($false),inference(cn,[status(thm)],[197144,theory(equality)])).
% cnf(197146,negated_conjecture,($false),197145,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 28381
% # ...of these trivial : 8
% # ...subsumed : 20873
% # ...remaining for further processing: 7500
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 1242
% # Backward-rewritten : 877
% # Generated clauses : 131564
% # ...of the previous two non-trivial : 125162
% # Contextual simplify-reflections : 36963
% # Paramodulations : 131257
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 5244
% # Positive orientable unit clauses: 45
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 42
% # Non-unit-clauses : 5157
% # Current number of unprocessed clauses: 59249
% # ...number of literals in the above : 495202
% # Clause-clause subsumption calls (NU) : 9718992
% # Rec. Clause-clause subsumption calls : 1878012
% # Unit Clause-clause subsumption calls : 73104
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 27
% # Indexed BW rewrite successes : 27
% # Backwards rewriting index: 2677 leaves, 2.55+/-7.196 terms/leaf
% # Paramod-from index: 508 leaves, 1.23+/-0.744 terms/leaf
% # Paramod-into index: 2009 leaves, 2.05+/-3.681 terms/leaf
% # -------------------------------------------------
% # User time : 18.594 s
% # System time : 0.293 s
% # Total time : 18.887 s
% # Maximum resident set size: 0 pages
% PrfWatch: 22.07 CPU 23.03 WC
% FINAL PrfWatch: 22.07 CPU 23.03 WC
% SZS output end Solution for /tmp/SystemOnTPTP23383/PRO002+4.tptp
%
%------------------------------------------------------------------------------