%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : PRO010+4 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:01:54 PM UTC 2026
% Result : Theorem 0.31s 1.61s
% Output : CNFRefutation 0.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 114
% Syntax : Number of formulae : 269 ( 41 unt; 0 def)
% Number of atoms : 847 ( 107 equ)
% Maximal formula atoms : 28 ( 3 avg)
% Number of connectives : 997 ( 419 ~; 416 |; 116 &)
% ( 7 <=>; 39 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 1 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 6 con; 0-3 aty)
% Number of variables : 656 ( 31 sgn 216 !; 27 ?)
% Comments :
%------------------------------------------------------------------------------
fof(goals,conjecture,
! [X106] :
( occurrence_of(X106,tptp0)
=> ? [X107,X108] :
( leaf_occ(X108,X106)
& ( occurrence_of(X108,tptp1)
=> ~ ? [X109] :
( occurrence_of(X109,tptp2)
& min_precedes(X107,X109,tptp0) ) )
& ( occurrence_of(X108,tptp2)
=> ~ ? [X110] :
( occurrence_of(X110,tptp1)
& min_precedes(X107,X110,tptp0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(sos_02,axiom,
! [X9,X10,X11,X12] :
( ( occurrence_of(X10,X9)
& subactivity_occurrence(X11,X10)
& leaf_occ(X12,X10)
& arboreal(X11)
& ~ min_precedes(X11,X12,X9) )
=> X12 = X11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_02) ).
fof(sos_22,axiom,
! [X66,X67,X68] :
( min_precedes(X66,X67,X68)
=> ~ root(X67,X68) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_22) ).
fof(sos_28,axiom,
! [X87,X88,X89,X90] :
( ( occurrence_of(X89,X90)
& ~ atomic(X90)
& leaf_occ(X87,X89)
& leaf_occ(X88,X89) )
=> X87 = X88 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_28) ).
fof(sos,axiom,
! [X1,X2] :
( ( occurrence_of(X2,X1)
& ~ atomic(X1) )
=> ? [X3] :
( root(X3,X1)
& subactivity_occurrence(X3,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos) ).
fof(sos_07,axiom,
! [X26,X27] :
( ( leaf(X26,X27)
& ~ atomic(X27) )
=> ? [X28] :
( occurrence_of(X28,X27)
& leaf_occ(X26,X28) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_07) ).
fof(sos_20,axiom,
! [X62,X63] :
( earlier(X62,X63)
=> ~ earlier(X63,X62) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_20) ).
fof(sos_26,axiom,
! [X79,X80,X81] :
( next_subocc(X79,X80,X81)
<=> ( min_precedes(X79,X80,X81)
& ~ ? [X82] :
( min_precedes(X79,X82,X81)
& min_precedes(X82,X80,X81) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_26) ).
fof(sos_31,axiom,
! [X98,X99,X100,X101] :
( ( min_precedes(X98,X99,X101)
& min_precedes(X98,X100,X101)
& precedes(X99,X100) )
=> min_precedes(X99,X100,X101) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_31) ).
fof(sos_23,axiom,
! [X69,X70,X71] :
( min_precedes(X69,X70,X71)
=> ? [X72] :
( root(X72,X71)
& min_precedes(X72,X70,X71) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_23) ).
fof(sos_01,axiom,
! [X4,X5,X6,X7,X8] :
( ( occurrence_of(X5,X4)
& root_occ(X7,X5)
& leaf_occ(X8,X5)
& subactivity_occurrence(X6,X5)
& min_precedes(X7,X6,X4)
& X6 != X8 )
=> min_precedes(X6,X8,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_01) ).
fof(sos_06,axiom,
! [X22,X23,X24] :
( min_precedes(X23,X24,X22)
=> ? [X25] :
( occurrence_of(X25,X22)
& subactivity_occurrence(X23,X25)
& subactivity_occurrence(X24,X25) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_06) ).
fof(sos_04,axiom,
! [X15,X16,X17,X18] :
( ( occurrence_of(X16,X15)
& arboreal(X17)
& arboreal(X18)
& subactivity_occurrence(X17,X16)
& subactivity_occurrence(X18,X16) )
=> ( min_precedes(X17,X18,X15)
| min_precedes(X18,X17,X15)
| X17 = X18 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_04) ).
fof(sos_15,axiom,
! [X48,X49] :
( leaf(X48,X49)
<=> ( ( root(X48,X49)
| ? [X50] : min_precedes(X50,X48,X49) )
& ~ ? [X51] : min_precedes(X48,X51,X49) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_15) ).
fof(sos_27,axiom,
! [X83,X84,X85,X86] :
( ( min_precedes(X83,X84,X85)
& occurrence_of(X86,X85)
& subactivity_occurrence(X84,X86) )
=> subactivity_occurrence(X83,X86) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_27) ).
fof(sos_09,axiom,
! [X32,X33,X34] :
( ( occurrence_of(X32,X34)
& leaf_occ(X33,X32) )
=> ~ ? [X35] : min_precedes(X33,X35,X34) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_09) ).
fof(sos_10,axiom,
! [X36,X37,X38] :
( ( occurrence_of(X36,X38)
& root_occ(X37,X36) )
=> ~ ? [X39] : min_precedes(X39,X37,X38) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_10) ).
fof(sos_24,axiom,
! [X73,X74,X75] :
( min_precedes(X73,X74,X75)
=> precedes(X73,X74) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_24) ).
fof(sos_25,axiom,
! [X76,X77,X78] :
( next_subocc(X76,X77,X78)
=> ( arboreal(X76)
& arboreal(X77) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_25) ).
fof(sos_32,axiom,
! [X102] :
( occurrence_of(X102,tptp0)
=> ? [X103,X104,X105] :
( occurrence_of(X103,tptp3)
& root_occ(X103,X102)
& occurrence_of(X104,tptp4)
& next_subocc(X103,X104,tptp0)
& ( occurrence_of(X105,tptp1)
| occurrence_of(X105,tptp2) )
& next_subocc(X104,X105,tptp0)
& leaf_occ(X105,X102) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_32) ).
fof(sos_18,axiom,
! [X56,X57] :
( leaf_occ(X56,X57)
<=> ? [X58] :
( occurrence_of(X57,X58)
& subactivity_occurrence(X56,X57)
& leaf(X56,X58) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_18) ).
fof(sos_19,axiom,
! [X59,X60] :
( root_occ(X59,X60)
<=> ? [X61] :
( occurrence_of(X60,X61)
& subactivity_occurrence(X59,X60)
& root(X59,X61) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_19) ).
fof(sos_29,axiom,
! [X91,X92,X93,X94] :
( ( occurrence_of(X93,X94)
& root_occ(X91,X93)
& root_occ(X92,X93) )
=> X91 = X92 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_29) ).
fof(sos_14,axiom,
! [X45,X46] :
( atocc(X45,X46)
<=> ? [X47] :
( subactivity(X46,X47)
& atomic(X47)
& occurrence_of(X45,X47) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_14) ).
fof(sos_05,axiom,
! [X19,X20] :
( root(X20,X19)
=> ? [X21] :
( subactivity(X21,X19)
& atocc(X20,X21) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_05) ).
fof(sos_30,axiom,
! [X95,X96,X97] :
( ( earlier(X95,X96)
& earlier(X96,X97) )
=> earlier(X95,X97) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_30) ).
fof(sos_08,axiom,
! [X29,X30,X31] :
( ( occurrence_of(X29,X30)
& occurrence_of(X29,X31) )
=> X30 = X31 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_08) ).
fof(sos_21,axiom,
! [X64,X65] :
( precedes(X64,X65)
<=> ( earlier(X64,X65)
& legal(X65) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_21) ).
fof(sos_16,axiom,
! [X52,X53] :
( occurrence_of(X52,X53)
=> ( arboreal(X52)
<=> atomic(X53) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_16) ).
fof(sos_12,axiom,
! [X42] :
( activity_occurrence(X42)
=> ? [X43] :
( activity(X43)
& occurrence_of(X42,X43) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_12) ).
fof(sos_17,axiom,
! [X54,X55] :
( root(X54,X55)
=> legal(X54) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_17) ).
fof(sos_11,axiom,
! [X40,X41] :
( subactivity_occurrence(X40,X41)
=> ( activity_occurrence(X40)
& activity_occurrence(X41) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_11) ).
fof(sos_03,axiom,
! [X13,X14] :
( occurrence_of(X14,X13)
=> ( activity(X13)
& activity_occurrence(X14) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_03) ).
fof(sos_13,axiom,
! [X44] :
( legal(X44)
=> arboreal(X44) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_13) ).
fof(sos_34,axiom,
~ atomic(tptp0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_34) ).
fof(sos_33,axiom,
activity(tptp0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_33) ).
fof(sos_37,axiom,
atomic(tptp2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_37) ).
fof(sos_36,axiom,
atomic(tptp1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_36) ).
fof(sos_35,axiom,
atomic(tptp4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_35) ).
fof(sos_38,axiom,
atomic(tptp3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_38) ).
fof(sos_44,axiom,
tptp1 != tptp2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_44) ).
fof(sos_41,axiom,
tptp4 != tptp2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_41) ).
fof(sos_43,axiom,
tptp3 != tptp2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_43) ).
fof(sos_40,axiom,
tptp4 != tptp1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_40) ).
fof(sos_42,axiom,
tptp3 != tptp1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_42) ).
fof(sos_39,axiom,
tptp4 != tptp3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_39) ).
fof(i_0_46,negated_conjecture,
~ ! [X106] :
( occurrence_of(X106,tptp0)
=> ? [X107,X108] :
( leaf_occ(X108,X106)
& ( occurrence_of(X108,tptp1)
=> ~ ? [X109] :
( occurrence_of(X109,tptp2)
& min_precedes(X107,X109,tptp0) ) )
& ( occurrence_of(X108,tptp2)
=> ~ ? [X110] :
( occurrence_of(X110,tptp1)
& min_precedes(X107,X110,tptp0) ) ) ) ),
inference(assume_negation,[status(cth)],[goals]) ).
fof(i_0_47,plain,
! [X9,X10,X11,X12] :
( ( occurrence_of(X10,X9)
& subactivity_occurrence(X11,X10)
& leaf_occ(X12,X10)
& arboreal(X11)
& ~ min_precedes(X11,X12,X9) )
=> X12 = X11 ),
inference(fof_simplification,[status(thm)],[sos_02]) ).
fof(i_0_48,plain,
! [X66,X67,X68] :
( min_precedes(X66,X67,X68)
=> ~ root(X67,X68) ),
inference(fof_simplification,[status(thm)],[sos_22]) ).
fof(i_0_49,plain,
! [X87,X88,X89,X90] :
( ( occurrence_of(X89,X90)
& ~ atomic(X90)
& leaf_occ(X87,X89)
& leaf_occ(X88,X89) )
=> X87 = X88 ),
inference(fof_simplification,[status(thm)],[sos_28]) ).
fof(i_0_50,plain,
! [X1,X2] :
( ( occurrence_of(X2,X1)
& ~ atomic(X1) )
=> ? [X3] :
( root(X3,X1)
& subactivity_occurrence(X3,X2) ) ),
inference(fof_simplification,[status(thm)],[sos]) ).
fof(i_0_51,plain,
! [X26,X27] :
( ( leaf(X26,X27)
& ~ atomic(X27) )
=> ? [X28] :
( occurrence_of(X28,X27)
& leaf_occ(X26,X28) ) ),
inference(fof_simplification,[status(thm)],[sos_07]) ).
fof(i_0_52,plain,
! [X62,X63] :
( earlier(X62,X63)
=> ~ earlier(X63,X62) ),
inference(fof_simplification,[status(thm)],[sos_20]) ).
fof(i_0_53,plain,
! [X312,X313,X314,X315,X316,X317,X318] :
( ( min_precedes(X312,X313,X314)
| ~ next_subocc(X312,X313,X314) )
& ( ~ min_precedes(X312,X315,X314)
| ~ min_precedes(X315,X313,X314)
| ~ next_subocc(X312,X313,X314) )
& ( min_precedes(X316,esk12_3(X316,X317,X318),X318)
| ~ min_precedes(X316,X317,X318)
| next_subocc(X316,X317,X318) )
& ( min_precedes(esk12_3(X316,X317,X318),X317,X318)
| ~ min_precedes(X316,X317,X318)
| next_subocc(X316,X317,X318) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_26])])])])])]) ).
fof(i_0_54,plain,
! [X335,X336,X337,X338] :
( ~ min_precedes(X335,X336,X338)
| ~ min_precedes(X335,X337,X338)
| ~ precedes(X336,X337)
| min_precedes(X336,X337,X338) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_31])]) ).
fof(i_0_55,plain,
! [X302,X303,X304] :
( ( root(esk11_3(X302,X303,X304),X304)
| ~ min_precedes(X302,X303,X304) )
& ( min_precedes(esk11_3(X302,X303,X304),X303,X304)
| ~ min_precedes(X302,X303,X304) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_23])])])]) ).
fof(i_0_56,plain,
! [X224,X225,X226,X227,X228] :
( ~ occurrence_of(X225,X224)
| ~ root_occ(X227,X225)
| ~ leaf_occ(X228,X225)
| ~ subactivity_occurrence(X226,X225)
| ~ min_precedes(X227,X226,X224)
| X226 = X228
| min_precedes(X226,X228,X224) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_01])]) ).
fof(i_0_57,plain,
! [X242,X243,X244] :
( ( occurrence_of(esk3_3(X242,X243,X244),X242)
| ~ min_precedes(X243,X244,X242) )
& ( subactivity_occurrence(X243,esk3_3(X242,X243,X244))
| ~ min_precedes(X243,X244,X242) )
& ( subactivity_occurrence(X244,esk3_3(X242,X243,X244))
| ~ min_precedes(X243,X244,X242) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_06])])])]) ).
fof(i_0_58,plain,
! [X235,X236,X237,X238] :
( ~ occurrence_of(X236,X235)
| ~ arboreal(X237)
| ~ arboreal(X238)
| ~ subactivity_occurrence(X237,X236)
| ~ subactivity_occurrence(X238,X236)
| min_precedes(X237,X238,X235)
| min_precedes(X238,X237,X235)
| X237 = X238 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_04])]) ).
fof(i_0_59,plain,
! [X271,X272,X274,X275,X276,X277] :
( ( root(X271,X272)
| min_precedes(esk7_2(X271,X272),X271,X272)
| ~ leaf(X271,X272) )
& ( ~ min_precedes(X271,X274,X272)
| ~ leaf(X271,X272) )
& ( ~ root(X275,X276)
| min_precedes(X275,esk8_2(X275,X276),X276)
| leaf(X275,X276) )
& ( ~ min_precedes(X277,X275,X276)
| min_precedes(X275,esk8_2(X275,X276),X276)
| leaf(X275,X276) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_15])])])])])]) ).
fof(i_0_60,negated_conjecture,
! [X344,X345] :
( occurrence_of(esk16_0,tptp0)
& ( occurrence_of(X345,tptp2)
| occurrence_of(X345,tptp1)
| ~ leaf_occ(X345,esk16_0) )
& ( occurrence_of(esk18_2(X344,X345),tptp1)
| occurrence_of(X345,tptp1)
| ~ leaf_occ(X345,esk16_0) )
& ( min_precedes(X344,esk18_2(X344,X345),tptp0)
| occurrence_of(X345,tptp1)
| ~ leaf_occ(X345,esk16_0) )
& ( occurrence_of(X345,tptp2)
| occurrence_of(esk17_2(X344,X345),tptp2)
| ~ leaf_occ(X345,esk16_0) )
& ( occurrence_of(esk18_2(X344,X345),tptp1)
| occurrence_of(esk17_2(X344,X345),tptp2)
| ~ leaf_occ(X345,esk16_0) )
& ( min_precedes(X344,esk18_2(X344,X345),tptp0)
| occurrence_of(esk17_2(X344,X345),tptp2)
| ~ leaf_occ(X345,esk16_0) )
& ( occurrence_of(X345,tptp2)
| min_precedes(X344,esk17_2(X344,X345),tptp0)
| ~ leaf_occ(X345,esk16_0) )
& ( occurrence_of(esk18_2(X344,X345),tptp1)
| min_precedes(X344,esk17_2(X344,X345),tptp0)
| ~ leaf_occ(X345,esk16_0) )
& ( min_precedes(X344,esk18_2(X344,X345),tptp0)
| min_precedes(X344,esk17_2(X344,X345),tptp0)
| ~ leaf_occ(X345,esk16_0) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_46])])])])]) ).
fof(i_0_61,plain,
! [X320,X321,X322,X323] :
( ~ min_precedes(X320,X321,X322)
| ~ occurrence_of(X323,X322)
| ~ subactivity_occurrence(X321,X323)
| subactivity_occurrence(X320,X323) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_27])]) ).
fof(i_0_62,plain,
! [X229,X230,X231,X232] :
( ~ occurrence_of(X230,X229)
| ~ subactivity_occurrence(X231,X230)
| ~ leaf_occ(X232,X230)
| ~ arboreal(X231)
| min_precedes(X231,X232,X229)
| X232 = X231 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_47])]) ).
fof(i_0_63,plain,
! [X252,X253,X254,X255] :
( ~ occurrence_of(X252,X254)
| ~ leaf_occ(X253,X252)
| ~ min_precedes(X253,X255,X254) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_09])])]) ).
fof(i_0_64,plain,
! [X256,X257,X258,X259] :
( ~ occurrence_of(X256,X258)
| ~ root_occ(X257,X256)
| ~ min_precedes(X259,X257,X258) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_10])])]) ).
fof(i_0_65,plain,
! [X299,X300,X301] :
( ~ min_precedes(X299,X300,X301)
| ~ root(X300,X301) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_48])]) ).
fof(i_0_66,plain,
! [X306,X307,X308] :
( ~ min_precedes(X306,X307,X308)
| precedes(X306,X307) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_24])]) ).
fof(i_0_67,plain,
! [X309,X310,X311] :
( ( arboreal(X309)
| ~ next_subocc(X309,X310,X311) )
& ( arboreal(X310)
| ~ next_subocc(X309,X310,X311) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_25])])]) ).
fof(i_0_68,plain,
! [X339] :
( ( occurrence_of(esk13_1(X339),tptp3)
| ~ occurrence_of(X339,tptp0) )
& ( root_occ(esk13_1(X339),X339)
| ~ occurrence_of(X339,tptp0) )
& ( occurrence_of(esk14_1(X339),tptp4)
| ~ occurrence_of(X339,tptp0) )
& ( next_subocc(esk13_1(X339),esk14_1(X339),tptp0)
| ~ occurrence_of(X339,tptp0) )
& ( occurrence_of(esk15_1(X339),tptp1)
| occurrence_of(esk15_1(X339),tptp2)
| ~ occurrence_of(X339,tptp0) )
& ( next_subocc(esk14_1(X339),esk15_1(X339),tptp0)
| ~ occurrence_of(X339,tptp0) )
& ( leaf_occ(esk15_1(X339),X339)
| ~ occurrence_of(X339,tptp0) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_32])])])]) ).
fof(i_0_69,plain,
! [X283,X284,X286,X287,X288] :
( ( occurrence_of(X284,esk9_2(X283,X284))
| ~ leaf_occ(X283,X284) )
& ( subactivity_occurrence(X283,X284)
| ~ leaf_occ(X283,X284) )
& ( leaf(X283,esk9_2(X283,X284))
| ~ leaf_occ(X283,X284) )
& ( ~ occurrence_of(X287,X288)
| ~ subactivity_occurrence(X286,X287)
| ~ leaf(X286,X288)
| leaf_occ(X286,X287) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_18])])])])])]) ).
fof(i_0_70,plain,
! [X289,X290,X292,X293,X294] :
( ( occurrence_of(X290,esk10_2(X289,X290))
| ~ root_occ(X289,X290) )
& ( subactivity_occurrence(X289,X290)
| ~ root_occ(X289,X290) )
& ( root(X289,esk10_2(X289,X290))
| ~ root_occ(X289,X290) )
& ( ~ occurrence_of(X293,X294)
| ~ subactivity_occurrence(X292,X293)
| ~ root(X292,X294)
| root_occ(X292,X293) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_19])])])])])]) ).
fof(i_0_71,plain,
! [X324,X325,X326,X327] :
( ~ occurrence_of(X326,X327)
| atomic(X327)
| ~ leaf_occ(X324,X326)
| ~ leaf_occ(X325,X326)
| X324 = X325 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_49])]) ).
fof(i_0_72,plain,
! [X328,X329,X330,X331] :
( ~ occurrence_of(X330,X331)
| ~ root_occ(X328,X330)
| ~ root_occ(X329,X330)
| X328 = X329 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_29])]) ).
fof(i_0_73,plain,
! [X221,X222] :
( ( root(esk1_2(X221,X222),X221)
| ~ occurrence_of(X222,X221)
| atomic(X221) )
& ( subactivity_occurrence(esk1_2(X221,X222),X222)
| ~ occurrence_of(X222,X221)
| atomic(X221) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_50])])])]) ).
fof(i_0_74,plain,
! [X246,X247] :
( ( occurrence_of(esk4_2(X246,X247),X247)
| ~ leaf(X246,X247)
| atomic(X247) )
& ( leaf_occ(X246,esk4_2(X246,X247))
| ~ leaf(X246,X247)
| atomic(X247) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_51])])])]) ).
fof(i_0_75,plain,
! [X265,X266,X268,X269,X270] :
( ( subactivity(X266,esk6_2(X265,X266))
| ~ atocc(X265,X266) )
& ( atomic(esk6_2(X265,X266))
| ~ atocc(X265,X266) )
& ( occurrence_of(X265,esk6_2(X265,X266))
| ~ atocc(X265,X266) )
& ( ~ subactivity(X269,X270)
| ~ atomic(X270)
| ~ occurrence_of(X268,X270)
| atocc(X268,X269) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_14])])])])])]) ).
fof(i_0_76,plain,
! [X239,X240] :
( ( subactivity(esk2_2(X239,X240),X239)
| ~ root(X240,X239) )
& ( atocc(X240,esk2_2(X239,X240))
| ~ root(X240,X239) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_05])])])]) ).
fof(i_0_77,plain,
! [X332,X333,X334] :
( ~ earlier(X332,X333)
| ~ earlier(X333,X334)
| earlier(X332,X334) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_30])]) ).
fof(i_0_78,plain,
! [X249,X250,X251] :
( ~ occurrence_of(X249,X250)
| ~ occurrence_of(X249,X251)
| X250 = X251 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_08])]) ).
fof(i_0_79,plain,
! [X295,X296] :
( ~ earlier(X295,X296)
| ~ earlier(X296,X295) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_52])]) ).
fof(i_0_80,plain,
! [X297,X298] :
( ( earlier(X297,X298)
| ~ precedes(X297,X298) )
& ( legal(X298)
| ~ precedes(X297,X298) )
& ( ~ earlier(X297,X298)
| ~ legal(X298)
| precedes(X297,X298) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_21])])]) ).
fof(i_0_81,plain,
! [X279,X280] :
( ( ~ arboreal(X279)
| atomic(X280)
| ~ occurrence_of(X279,X280) )
& ( ~ atomic(X280)
| arboreal(X279)
| ~ occurrence_of(X279,X280) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_16])])]) ).
fof(i_0_82,plain,
! [X262] :
( ( activity(esk5_1(X262))
| ~ activity_occurrence(X262) )
& ( occurrence_of(X262,esk5_1(X262))
| ~ activity_occurrence(X262) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_12])])])]) ).
fof(i_0_83,plain,
! [X281,X282] :
( ~ root(X281,X282)
| legal(X281) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_17])]) ).
fof(i_0_84,plain,
! [X260,X261] :
( ( activity_occurrence(X260)
| ~ subactivity_occurrence(X260,X261) )
& ( activity_occurrence(X261)
| ~ subactivity_occurrence(X260,X261) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_11])])]) ).
fof(i_0_85,plain,
! [X233,X234] :
( ( activity(X233)
| ~ occurrence_of(X234,X233) )
& ( activity_occurrence(X234)
| ~ occurrence_of(X234,X233) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_03])])]) ).
fof(i_0_86,plain,
! [X264] :
( ~ legal(X264)
| arboreal(X264) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_13])]) ).
fof(i_0_87,plain,
~ atomic(tptp0),
inference(fof_simplification,[status(thm)],[sos_34]) ).
cnf(i_0_88,plain,
( min_precedes(esk12_3(X1,X2,X3),X2,X3)
| next_subocc(X1,X2,X3)
| ~ min_precedes(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_89,plain,
( min_precedes(X1,esk12_3(X1,X2,X3),X3)
| next_subocc(X1,X2,X3)
| ~ min_precedes(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_90,plain,
( ~ min_precedes(X1,X2,X3)
| ~ min_precedes(X2,X4,X3)
| ~ next_subocc(X1,X4,X3) ),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_91,plain,
( min_precedes(X2,X4,X3)
| ~ min_precedes(X1,X2,X3)
| ~ min_precedes(X1,X4,X3)
| ~ precedes(X2,X4) ),
inference(split_conjunct,[status(thm)],[i_0_54]),
[final] ).
cnf(i_0_92,plain,
( min_precedes(esk11_3(X1,X2,X3),X2,X3)
| ~ min_precedes(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_93,plain,
( X5 = X4
| min_precedes(X5,X4,X2)
| ~ occurrence_of(X1,X2)
| ~ root_occ(X3,X1)
| ~ leaf_occ(X4,X1)
| ~ subactivity_occurrence(X5,X1)
| ~ min_precedes(X3,X5,X2) ),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_94,plain,
( root(esk11_3(X1,X2,X3),X3)
| ~ min_precedes(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_95,plain,
( occurrence_of(esk3_3(X1,X2,X3),X1)
| ~ min_precedes(X2,X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_96,plain,
( subactivity_occurrence(X1,esk3_3(X2,X1,X3))
| ~ min_precedes(X1,X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_97,plain,
( subactivity_occurrence(X1,esk3_3(X2,X3,X1))
| ~ min_precedes(X3,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_98,plain,
( min_precedes(X3,X4,X2)
| min_precedes(X4,X3,X2)
| X3 = X4
| ~ occurrence_of(X1,X2)
| ~ arboreal(X3)
| ~ arboreal(X4)
| ~ subactivity_occurrence(X3,X1)
| ~ subactivity_occurrence(X4,X1) ),
inference(split_conjunct,[status(thm)],[i_0_58]),
[final] ).
cnf(i_0_99,plain,
( min_precedes(X2,esk8_2(X2,X3),X3)
| leaf(X2,X3)
| ~ min_precedes(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_100,negated_conjecture,
( min_precedes(X1,esk18_2(X1,X2),tptp0)
| min_precedes(X1,esk17_2(X1,X2),tptp0)
| ~ leaf_occ(X2,esk16_0) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_101,plain,
( subactivity_occurrence(X1,X4)
| ~ min_precedes(X1,X2,X3)
| ~ occurrence_of(X4,X3)
| ~ subactivity_occurrence(X2,X4) ),
inference(split_conjunct,[status(thm)],[i_0_61]),
[final] ).
cnf(i_0_102,plain,
( min_precedes(X1,X2,X3)
| ~ next_subocc(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_103,negated_conjecture,
( occurrence_of(esk18_2(X1,X2),tptp1)
| min_precedes(X1,esk17_2(X1,X2),tptp0)
| ~ leaf_occ(X2,esk16_0) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_104,negated_conjecture,
( min_precedes(X1,esk18_2(X1,X2),tptp0)
| occurrence_of(esk17_2(X1,X2),tptp2)
| ~ leaf_occ(X2,esk16_0) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_105,plain,
( min_precedes(X3,X4,X2)
| X4 = X3
| ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X3,X1)
| ~ leaf_occ(X4,X1)
| ~ arboreal(X3) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_106,plain,
( ~ occurrence_of(X1,X2)
| ~ leaf_occ(X3,X1)
| ~ min_precedes(X3,X4,X2) ),
inference(split_conjunct,[status(thm)],[i_0_63]),
[final] ).
cnf(i_0_107,plain,
( ~ occurrence_of(X1,X2)
| ~ root_occ(X3,X1)
| ~ min_precedes(X4,X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_64]),
[final] ).
cnf(i_0_108,plain,
( root(X1,X2)
| min_precedes(esk7_2(X1,X2),X1,X2)
| ~ leaf(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_109,plain,
( min_precedes(X1,esk8_2(X1,X2),X2)
| leaf(X1,X2)
| ~ root(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_110,negated_conjecture,
( occurrence_of(X1,tptp2)
| min_precedes(X2,esk17_2(X2,X1),tptp0)
| ~ leaf_occ(X1,esk16_0) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_111,negated_conjecture,
( min_precedes(X1,esk18_2(X1,X2),tptp0)
| occurrence_of(X2,tptp1)
| ~ leaf_occ(X2,esk16_0) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_112,plain,
( ~ min_precedes(X1,X2,X3)
| ~ leaf(X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_113,plain,
( ~ min_precedes(X1,X2,X3)
| ~ root(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_65]),
[final] ).
cnf(i_0_114,plain,
( precedes(X1,X2)
| ~ min_precedes(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_66]),
[final] ).
cnf(i_0_115,negated_conjecture,
( occurrence_of(esk18_2(X1,X2),tptp1)
| occurrence_of(esk17_2(X1,X2),tptp2)
| ~ leaf_occ(X2,esk16_0) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_116,plain,
( arboreal(X1)
| ~ next_subocc(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_117,plain,
( arboreal(X1)
| ~ next_subocc(X2,X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_118,plain,
( next_subocc(esk14_1(X1),esk15_1(X1),tptp0)
| ~ occurrence_of(X1,tptp0) ),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_119,plain,
( next_subocc(esk13_1(X1),esk14_1(X1),tptp0)
| ~ occurrence_of(X1,tptp0) ),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_120,plain,
( leaf_occ(X3,X1)
| ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X3,X1)
| ~ leaf(X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_69]),
[final] ).
cnf(i_0_121,plain,
( root_occ(X3,X1)
| ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X3,X1)
| ~ root(X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_70]),
[final] ).
cnf(i_0_122,plain,
( atomic(X2)
| X3 = X4
| ~ occurrence_of(X1,X2)
| ~ leaf_occ(X3,X1)
| ~ leaf_occ(X4,X1) ),
inference(split_conjunct,[status(thm)],[i_0_71]),
[final] ).
cnf(i_0_123,negated_conjecture,
( occurrence_of(X1,tptp2)
| occurrence_of(esk17_2(X2,X1),tptp2)
| ~ leaf_occ(X1,esk16_0) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_124,negated_conjecture,
( occurrence_of(esk18_2(X1,X2),tptp1)
| occurrence_of(X2,tptp1)
| ~ leaf_occ(X2,esk16_0) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_125,plain,
( X3 = X4
| ~ occurrence_of(X1,X2)
| ~ root_occ(X3,X1)
| ~ root_occ(X4,X1) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_126,plain,
( subactivity_occurrence(esk1_2(X1,X2),X2)
| atomic(X1)
| ~ occurrence_of(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_127,plain,
( root(esk1_2(X1,X2),X1)
| atomic(X1)
| ~ occurrence_of(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_128,plain,
( occurrence_of(esk4_2(X1,X2),X2)
| atomic(X2)
| ~ leaf(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_74]),
[final] ).
cnf(i_0_129,plain,
( leaf_occ(X1,esk4_2(X1,X2))
| atomic(X2)
| ~ leaf(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_74]),
[final] ).
cnf(i_0_130,plain,
( atocc(X3,X1)
| ~ subactivity(X1,X2)
| ~ atomic(X2)
| ~ occurrence_of(X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_75]),
[final] ).
cnf(i_0_131,plain,
( subactivity(esk2_2(X1,X2),X1)
| ~ root(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_76]),
[final] ).
cnf(i_0_132,plain,
( leaf(X1,esk9_2(X1,X2))
| ~ leaf_occ(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_69]),
[final] ).
cnf(i_0_133,plain,
( atocc(X1,esk2_2(X2,X1))
| ~ root(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_76]),
[final] ).
cnf(i_0_134,plain,
( subactivity(X1,esk6_2(X2,X1))
| ~ atocc(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_75]),
[final] ).
cnf(i_0_135,plain,
( root(X1,esk10_2(X1,X2))
| ~ root_occ(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_70]),
[final] ).
cnf(i_0_136,plain,
( occurrence_of(X1,esk10_2(X2,X1))
| ~ root_occ(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_70]),
[final] ).
cnf(i_0_137,plain,
( occurrence_of(X1,esk9_2(X2,X1))
| ~ leaf_occ(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_69]),
[final] ).
cnf(i_0_138,plain,
( occurrence_of(X1,esk6_2(X1,X2))
| ~ atocc(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_75]),
[final] ).
cnf(i_0_139,plain,
( earlier(X1,X3)
| ~ earlier(X1,X2)
| ~ earlier(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_77]),
[final] ).
cnf(i_0_140,plain,
( occurrence_of(esk15_1(X1),tptp1)
| occurrence_of(esk15_1(X1),tptp2)
| ~ occurrence_of(X1,tptp0) ),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_141,plain,
( atomic(esk6_2(X1,X2))
| ~ atocc(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_75]),
[final] ).
cnf(i_0_142,plain,
( X2 = X3
| ~ occurrence_of(X1,X2)
| ~ occurrence_of(X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_78]),
[final] ).
cnf(i_0_143,negated_conjecture,
( occurrence_of(X1,tptp2)
| occurrence_of(X1,tptp1)
| ~ leaf_occ(X1,esk16_0) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_144,plain,
( ~ earlier(X1,X2)
| ~ earlier(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_79]),
[final] ).
cnf(i_0_145,plain,
( precedes(X1,X2)
| ~ earlier(X1,X2)
| ~ legal(X2) ),
inference(split_conjunct,[status(thm)],[i_0_80]),
[final] ).
cnf(i_0_146,plain,
( leaf_occ(esk15_1(X1),X1)
| ~ occurrence_of(X1,tptp0) ),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_147,plain,
( root_occ(esk13_1(X1),X1)
| ~ occurrence_of(X1,tptp0) ),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_148,plain,
( occurrence_of(esk14_1(X1),tptp4)
| ~ occurrence_of(X1,tptp0) ),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_149,plain,
( occurrence_of(esk13_1(X1),tptp3)
| ~ occurrence_of(X1,tptp0) ),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_150,plain,
( earlier(X1,X2)
| ~ precedes(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_80]),
[final] ).
cnf(i_0_151,plain,
( subactivity_occurrence(X1,X2)
| ~ leaf_occ(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_69]),
[final] ).
cnf(i_0_152,plain,
( subactivity_occurrence(X1,X2)
| ~ root_occ(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_70]),
[final] ).
cnf(i_0_153,plain,
( arboreal(X2)
| ~ atomic(X1)
| ~ occurrence_of(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_81]),
[final] ).
cnf(i_0_154,plain,
( atomic(X2)
| ~ arboreal(X1)
| ~ occurrence_of(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_81]),
[final] ).
cnf(i_0_155,plain,
( occurrence_of(X1,esk5_1(X1))
| ~ activity_occurrence(X1) ),
inference(split_conjunct,[status(thm)],[i_0_82]),
[final] ).
cnf(i_0_156,plain,
( legal(X1)
| ~ precedes(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_80]),
[final] ).
cnf(i_0_157,plain,
( legal(X1)
| ~ root(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_83]),
[final] ).
cnf(i_0_158,plain,
( activity_occurrence(X1)
| ~ subactivity_occurrence(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_84]),
[final] ).
cnf(i_0_159,plain,
( activity_occurrence(X1)
| ~ subactivity_occurrence(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_84]),
[final] ).
cnf(i_0_160,plain,
( activity_occurrence(X1)
| ~ occurrence_of(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_85]),
[final] ).
cnf(i_0_161,plain,
( activity(X1)
| ~ occurrence_of(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_85]),
[final] ).
cnf(i_0_162,plain,
( activity(esk5_1(X1))
| ~ activity_occurrence(X1) ),
inference(split_conjunct,[status(thm)],[i_0_82]),
[final] ).
cnf(i_0_163,plain,
( arboreal(X1)
| ~ legal(X1) ),
inference(split_conjunct,[status(thm)],[i_0_86]),
[final] ).
cnf(i_0_164,negated_conjecture,
occurrence_of(esk16_0,tptp0),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_165,plain,
~ atomic(tptp0),
inference(split_conjunct,[status(thm)],[i_0_87]),
[final] ).
cnf(i_0_166,plain,
activity(tptp0),
inference(split_conjunct,[status(thm)],[sos_33]),
[final] ).
cnf(i_0_167,plain,
atomic(tptp2),
inference(split_conjunct,[status(thm)],[sos_37]),
[final] ).
cnf(i_0_168,plain,
atomic(tptp1),
inference(split_conjunct,[status(thm)],[sos_36]),
[final] ).
cnf(i_0_169,plain,
atomic(tptp4),
inference(split_conjunct,[status(thm)],[sos_35]),
[final] ).
cnf(i_0_170,plain,
atomic(tptp3),
inference(split_conjunct,[status(thm)],[sos_38]),
[final] ).
cnf(i_0_171,plain,
tptp1 != tptp2,
inference(split_conjunct,[status(thm)],[sos_44]),
[final] ).
cnf(i_0_172,plain,
tptp4 != tptp2,
inference(split_conjunct,[status(thm)],[sos_41]),
[final] ).
cnf(i_0_173,plain,
tptp3 != tptp2,
inference(split_conjunct,[status(thm)],[sos_43]),
[final] ).
cnf(i_0_174,plain,
tptp4 != tptp1,
inference(split_conjunct,[status(thm)],[sos_40]),
[final] ).
cnf(i_0_175,plain,
tptp3 != tptp1,
inference(split_conjunct,[status(thm)],[sos_42]),
[final] ).
cnf(i_0_176,plain,
tptp4 != tptp3,
inference(split_conjunct,[status(thm)],[sos_39]),
[final] ).
cnf(i_0_177,axiom,
X1 = X1 ).
cnf(i_0_178,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_179,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_180,axiom,
( X1 != X2
| ~ min_precedes(X1,X3,X4)
| min_precedes(X2,X3,X4) ) ).
cnf(i_0_181,axiom,
( X1 != X2
| ~ min_precedes(X3,X1,X4)
| min_precedes(X3,X2,X4) ) ).
cnf(i_0_182,axiom,
( X1 != X2
| ~ min_precedes(X3,X4,X1)
| min_precedes(X3,X4,X2) ) ).
cnf(i_0_183,axiom,
( X1 != X2
| ~ leaf(X1,X3)
| leaf(X2,X3) ) ).
cnf(i_0_184,axiom,
( X1 != X2
| ~ leaf(X3,X1)
| leaf(X3,X2) ) ).
cnf(i_0_185,axiom,
( X1 != X2
| ~ atomic(X1)
| atomic(X2) ) ).
cnf(i_0_186,axiom,
( X1 != X2
| ~ atocc(X1,X3)
| atocc(X2,X3) ) ).
cnf(i_0_187,axiom,
( X1 != X2
| ~ atocc(X3,X1)
| atocc(X3,X2) ) ).
cnf(i_0_188,axiom,
( X1 != X2
| ~ subactivity(X1,X3)
| subactivity(X2,X3) ) ).
cnf(i_0_189,axiom,
( X1 != X2
| ~ subactivity(X3,X1)
| subactivity(X3,X2) ) ).
cnf(i_0_190,axiom,
( X1 != X2
| ~ earlier(X1,X3)
| earlier(X2,X3) ) ).
cnf(i_0_191,axiom,
( X1 != X2
| ~ earlier(X3,X1)
| earlier(X3,X2) ) ).
cnf(i_0_192,axiom,
( X1 != X2
| ~ legal(X1)
| legal(X2) ) ).
cnf(i_0_193,axiom,
( X1 != X2
| ~ activity_occurrence(X1)
| activity_occurrence(X2) ) ).
cnf(i_0_194,axiom,
( X1 != X2
| ~ activity(X1)
| activity(X2) ) ).
cnf(i_0_195,axiom,
( X1 != X2
| ~ next_subocc(X1,X3,X4)
| next_subocc(X2,X3,X4) ) ).
cnf(i_0_196,axiom,
( X1 != X2
| ~ next_subocc(X3,X1,X4)
| next_subocc(X3,X2,X4) ) ).
cnf(i_0_197,axiom,
( X1 != X2
| ~ next_subocc(X3,X4,X1)
| next_subocc(X3,X4,X2) ) ).
cnf(i_0_198,axiom,
( X1 != X2
| ~ precedes(X1,X3)
| precedes(X2,X3) ) ).
cnf(i_0_199,axiom,
( X1 != X2
| ~ precedes(X3,X1)
| precedes(X3,X2) ) ).
cnf(i_0_200,axiom,
( X1 != X2
| ~ occurrence_of(X1,X3)
| occurrence_of(X2,X3) ) ).
cnf(i_0_201,axiom,
( X1 != X2
| ~ occurrence_of(X3,X1)
| occurrence_of(X3,X2) ) ).
cnf(i_0_202,axiom,
( X1 != X2
| ~ root_occ(X1,X3)
| root_occ(X2,X3) ) ).
cnf(i_0_203,axiom,
( X1 != X2
| ~ root_occ(X3,X1)
| root_occ(X3,X2) ) ).
cnf(i_0_204,axiom,
( X1 != X2
| ~ leaf_occ(X1,X3)
| leaf_occ(X2,X3) ) ).
cnf(i_0_205,axiom,
( X1 != X2
| ~ leaf_occ(X3,X1)
| leaf_occ(X3,X2) ) ).
cnf(i_0_206,axiom,
( X1 != X2
| ~ subactivity_occurrence(X1,X3)
| subactivity_occurrence(X2,X3) ) ).
cnf(i_0_207,axiom,
( X1 != X2
| ~ subactivity_occurrence(X3,X1)
| subactivity_occurrence(X3,X2) ) ).
cnf(i_0_208,axiom,
( X1 != X2
| ~ root(X1,X3)
| root(X2,X3) ) ).
cnf(i_0_209,axiom,
( X1 != X2
| ~ root(X3,X1)
| root(X3,X2) ) ).
cnf(i_0_210,axiom,
( X1 != X2
| ~ arboreal(X1)
| arboreal(X2) ) ).
cnf(i_0_177_001,axiom,
X1 = X1 ).
cnf(i_0_178_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_179_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_180_004,axiom,
( X1 != X2
| ~ min_precedes(X1,X3,X4)
| min_precedes(X2,X3,X4) ) ).
cnf(i_0_181_005,axiom,
( X1 != X2
| ~ min_precedes(X3,X1,X4)
| min_precedes(X3,X2,X4) ) ).
cnf(i_0_182_006,axiom,
( X1 != X2
| ~ min_precedes(X3,X4,X1)
| min_precedes(X3,X4,X2) ) ).
cnf(i_0_183_007,axiom,
( X1 != X2
| ~ leaf(X1,X3)
| leaf(X2,X3) ) ).
cnf(i_0_184_008,axiom,
( X1 != X2
| ~ leaf(X3,X1)
| leaf(X3,X2) ) ).
cnf(i_0_185_009,axiom,
( X1 != X2
| ~ atomic(X1)
| atomic(X2) ) ).
cnf(i_0_186_010,axiom,
( X1 != X2
| ~ atocc(X1,X3)
| atocc(X2,X3) ) ).
cnf(i_0_187_011,axiom,
( X1 != X2
| ~ atocc(X3,X1)
| atocc(X3,X2) ) ).
cnf(i_0_188_012,axiom,
( X1 != X2
| ~ subactivity(X1,X3)
| subactivity(X2,X3) ) ).
cnf(i_0_189_013,axiom,
( X1 != X2
| ~ subactivity(X3,X1)
| subactivity(X3,X2) ) ).
cnf(i_0_190_014,axiom,
( X1 != X2
| ~ earlier(X1,X3)
| earlier(X2,X3) ) ).
cnf(i_0_191_015,axiom,
( X1 != X2
| ~ earlier(X3,X1)
| earlier(X3,X2) ) ).
cnf(i_0_192_016,axiom,
( X1 != X2
| ~ legal(X1)
| legal(X2) ) ).
cnf(i_0_193_017,axiom,
( X1 != X2
| ~ activity_occurrence(X1)
| activity_occurrence(X2) ) ).
cnf(i_0_194_018,axiom,
( X1 != X2
| ~ activity(X1)
| activity(X2) ) ).
cnf(i_0_195_019,axiom,
( X1 != X2
| ~ next_subocc(X1,X3,X4)
| next_subocc(X2,X3,X4) ) ).
cnf(i_0_196_020,axiom,
( X1 != X2
| ~ next_subocc(X3,X1,X4)
| next_subocc(X3,X2,X4) ) ).
cnf(i_0_197_021,axiom,
( X1 != X2
| ~ next_subocc(X3,X4,X1)
| next_subocc(X3,X4,X2) ) ).
cnf(i_0_198_022,axiom,
( X1 != X2
| ~ precedes(X1,X3)
| precedes(X2,X3) ) ).
cnf(i_0_199_023,axiom,
( X1 != X2
| ~ precedes(X3,X1)
| precedes(X3,X2) ) ).
cnf(i_0_200_024,axiom,
( X1 != X2
| ~ occurrence_of(X1,X3)
| occurrence_of(X2,X3) ) ).
cnf(i_0_201_025,axiom,
( X1 != X2
| ~ occurrence_of(X3,X1)
| occurrence_of(X3,X2) ) ).
cnf(i_0_202_026,axiom,
( X1 != X2
| ~ root_occ(X1,X3)
| root_occ(X2,X3) ) ).
cnf(i_0_203_027,axiom,
( X1 != X2
| ~ root_occ(X3,X1)
| root_occ(X3,X2) ) ).
cnf(i_0_204_028,axiom,
( X1 != X2
| ~ leaf_occ(X1,X3)
| leaf_occ(X2,X3) ) ).
cnf(i_0_205_029,axiom,
( X1 != X2
| ~ leaf_occ(X3,X1)
| leaf_occ(X3,X2) ) ).
cnf(i_0_206_030,axiom,
( X1 != X2
| ~ subactivity_occurrence(X1,X3)
| subactivity_occurrence(X2,X3) ) ).
cnf(i_0_207_031,axiom,
( X1 != X2
| ~ subactivity_occurrence(X3,X1)
| subactivity_occurrence(X3,X2) ) ).
cnf(i_0_208_032,axiom,
( X1 != X2
| ~ root(X1,X3)
| root(X2,X3) ) ).
cnf(i_0_209_033,axiom,
( X1 != X2
| ~ root(X3,X1)
| root(X3,X2) ) ).
cnf(i_0_210_034,axiom,
( X1 != X2
| ~ arboreal(X1)
| arboreal(X2) ) ).
cnf(i_0_211,plain,
leaf_occ(esk15_1(esk16_0),esk16_0),
inference(scs_inference,[],[i_0_164,i_0_146]) ).
cnf(i_0_212,plain,
( ~ occurrence_of(X1,tptp0)
| leaf_occ(esk15_1(X1),X1) ),
inference(rename_variables,[],[i_0_146]) ).
cnf(i_0_213,plain,
root_occ(esk13_1(esk16_0),esk16_0),
inference(scs_inference,[],[i_0_164,i_0_146,i_0_147]) ).
cnf(i_0_214,plain,
( ~ occurrence_of(X1,tptp0)
| root_occ(esk13_1(X1),X1) ),
inference(rename_variables,[],[i_0_147]) ).
cnf(i_0_215,plain,
subactivity_occurrence(esk15_1(esk16_0),esk16_0),
inference(scs_inference,[],[i_0_164,i_0_146,i_0_147,i_0_151]) ).
cnf(i_0_216,plain,
( ~ leaf_occ(X1,X2)
| subactivity_occurrence(X1,X2) ),
inference(rename_variables,[],[i_0_151]) ).
cnf(i_0_217,plain,
subactivity_occurrence(esk13_1(esk16_0),esk16_0),
inference(scs_inference,[],[i_0_164,i_0_146,i_0_147,i_0_151,i_0_152]) ).
cnf(i_0_218,plain,
( ~ root_occ(X1,X2)
| subactivity_occurrence(X1,X2) ),
inference(rename_variables,[],[i_0_152]) ).
cnf(i_0_219,plain,
~ min_precedes(esk15_1(esk16_0),X1,tptp0),
inference(scs_inference,[],[i_0_164,i_0_146,i_0_147,i_0_151,i_0_152,i_0_106]) ).
cnf(i_0_220,plain,
( ~ occurrence_of(X1,X2)
| ~ min_precedes(X3,X4,X2)
| ~ leaf_occ(X3,X1) ),
inference(rename_variables,[],[i_0_106]) ).
cnf(i_0_221,plain,
~ min_precedes(X1,esk13_1(esk16_0),tptp0),
inference(scs_inference,[],[i_0_164,i_0_146,i_0_147,i_0_151,i_0_152,i_0_106,i_0_107]) ).
cnf(i_0_222,plain,
( ~ occurrence_of(X1,X2)
| ~ min_precedes(X3,X4,X2)
| ~ root_occ(X4,X1) ),
inference(rename_variables,[],[i_0_107]) ).
cnf(i_0_223,plain,
~ arboreal(esk16_0),
inference(scs_inference,[],[i_0_164,i_0_165,i_0_146,i_0_147,i_0_151,i_0_152,i_0_106,i_0_107,i_0_154]) ).
cnf(i_0_224,plain,
( ~ occurrence_of(X1,X2)
| atomic(X2)
| ~ arboreal(X1) ),
inference(rename_variables,[],[i_0_154]) ).
cnf(i_0_225,plain,
tptp2 != tptp0,
inference(scs_inference,[],[i_0_164,i_0_165,i_0_167,i_0_146,i_0_147,i_0_151,i_0_152,i_0_106,i_0_107,i_0_154,i_0_185]) ).
cnf(i_0_226,plain,
~ next_subocc(esk16_0,X1,X2),
inference(scs_inference,[],[i_0_164,i_0_165,i_0_167,i_0_146,i_0_147,i_0_151,i_0_152,i_0_106,i_0_107,i_0_154,i_0_185,i_0_116]) ).
cnf(i_0_227,plain,
( arboreal(X1)
| ~ next_subocc(X1,X2,X3) ),
inference(rename_variables,[],[i_0_116]) ).
cnf(i_0_228,plain,
~ next_subocc(X1,esk16_0,X2),
inference(scs_inference,[],[i_0_164,i_0_165,i_0_167,i_0_146,i_0_147,i_0_151,i_0_152,i_0_106,i_0_107,i_0_154,i_0_185,i_0_116,i_0_117]) ).
cnf(i_0_229,plain,
( arboreal(X1)
| ~ next_subocc(X2,X1,X3) ),
inference(rename_variables,[],[i_0_117]) ).
cnf(i_0_230,plain,
min_precedes(esk15_1(esk16_0),esk18_2(esk15_1(esk16_0),esk15_1(esk16_0)),tptp0),
inference(scs_inference,[],[i_0_164,i_0_165,i_0_167,i_0_146,i_0_147,i_0_151,i_0_152,i_0_106,i_0_107,i_0_154,i_0_185,i_0_116,i_0_117,i_0_100]) ).
cnf(i_0_231,plain,
( min_precedes(X1,esk17_2(X1,X2),tptp0)
| min_precedes(X1,esk18_2(X1,X2),tptp0)
| ~ leaf_occ(X2,esk16_0) ),
inference(rename_variables,[],[i_0_100]) ).
cnf(i_0_232,plain,
occurrence_of(esk15_1(esk16_0),tptp2),
inference(scs_inference,[],[i_0_164,i_0_165,i_0_167,i_0_146,i_0_147,i_0_151,i_0_152,i_0_106,i_0_107,i_0_154,i_0_185,i_0_116,i_0_117,i_0_100,i_0_110]) ).
cnf(i_0_233,plain,
( min_precedes(X1,esk17_2(X1,X2),tptp0)
| ~ leaf_occ(X2,esk16_0)
| occurrence_of(X2,tptp2) ),
inference(rename_variables,[],[i_0_110]) ).
cnf(i_0_234,plain,
$false,
inference(scs_inference,[],[i_0_164,i_0_165,i_0_167,i_0_146,i_0_147,i_0_151,i_0_152,i_0_106,i_0_107,i_0_154,i_0_185,i_0_116,i_0_117,i_0_100,i_0_110,i_0_220]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : PRO010+4 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.11 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.32 % Computer : n009.cluster.edu
% 0.15/0.32 % Model : x86_64 x86_64
% 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32 % Memory : 8042.1875MB
% 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.32 % CPULimit : 300
% 0.15/0.32 % WCLimit : 300
% 0.15/0.32 % DateTime : Tue May 5 01:30:26 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.33 % start to proof: theBenchmark
% 0.31/1.61 % Version : CSE_E---1.7
% 0.31/1.61 % Problem : theBenchmark.p
% 0.31/1.61 % SZS status Theorem for theBenchmark.p
% 0.31/1.61 % SZS output start CNFRefutation
% See solution above
% 0.31/1.70 % Total time : 1.272s
%------------------------------------------------------------------------------