%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : PRO003+4 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n016.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:51 PM UTC 2026
% Result : Theorem 154.30s 89.93s
% Output : CNFRefutation 155.00s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named i_0_5182)
% Comments :
%------------------------------------------------------------------------------
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/sandbox/benchmark/theBenchmark.p',sos_02) ).
fof(sos_22,axiom,
! [X66,X67,X68] :
( min_precedes(X66,X67,X68)
=> ~ root(X67,X68) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',sos_07) ).
fof(sos_20,axiom,
! [X62,X63] :
( earlier(X62,X63)
=> ~ earlier(X63,X62) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_20) ).
fof(goals,conjecture,
~ ? [X108] : occurrence_of(X108,tptp0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',sos_10) ).
fof(sos_45,axiom,
! [X105,X106] :
( ( occurrence_of(X106,tptp0)
& root_occ(X105,X106) )
=> ? [X107] :
( occurrence_of(X107,tptp1)
& next_subocc(X105,X107,tptp0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_45) ).
fof(sos_24,axiom,
! [X73,X74,X75] :
( min_precedes(X73,X74,X75)
=> precedes(X73,X74) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_24) ).
fof(sos_25,axiom,
! [X76,X77,X78] :
( next_subocc(X76,X77,X78)
=> ( arboreal(X76)
& arboreal(X77) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_25) ).
fof(sos_32,axiom,
! [X102] :
( occurrence_of(X102,tptp0)
=> ? [X103,X104] :
( occurrence_of(X103,tptp4)
& root_occ(X103,X102)
& occurrence_of(X104,tptp3)
& leaf_occ(X104,X102)
& next_subocc(X103,X104,tptp0) ) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',sos_14) ).
fof(sos_05,axiom,
! [X19,X20] :
( root(X20,X19)
=> ? [X21] :
( subactivity(X21,X19)
& atocc(X20,X21) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_05) ).
fof(sos_30,axiom,
! [X95,X96,X97] :
( ( earlier(X95,X96)
& earlier(X96,X97) )
=> earlier(X95,X97) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',sos_08) ).
fof(sos_21,axiom,
! [X64,X65] :
( precedes(X64,X65)
<=> ( earlier(X64,X65)
& legal(X65) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_21) ).
fof(sos_16,axiom,
! [X52,X53] :
( occurrence_of(X52,X53)
=> ( arboreal(X52)
<=> atomic(X53) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_16) ).
fof(sos_12,axiom,
! [X42] :
( activity_occurrence(X42)
=> ? [X43] :
( activity(X43)
& occurrence_of(X42,X43) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_12) ).
fof(sos_17,axiom,
! [X54,X55] :
( root(X54,X55)
=> legal(X54) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_17) ).
fof(sos_11,axiom,
! [X40,X41] :
( subactivity_occurrence(X40,X41)
=> ( activity_occurrence(X40)
& activity_occurrence(X41) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_11) ).
fof(sos_03,axiom,
! [X13,X14] :
( occurrence_of(X14,X13)
=> ( activity(X13)
& activity_occurrence(X14) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_03) ).
fof(sos_13,axiom,
! [X44] :
( legal(X44)
=> arboreal(X44) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_13) ).
fof(sos_34,axiom,
~ atomic(tptp0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_34) ).
fof(sos_33,axiom,
activity(tptp0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_33) ).
fof(sos_38,axiom,
atomic(tptp1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_38) ).
fof(sos_37,axiom,
atomic(tptp2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_37) ).
fof(sos_36,axiom,
atomic(tptp3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_36) ).
fof(sos_35,axiom,
atomic(tptp4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_35) ).
fof(sos_43,axiom,
tptp1 != tptp2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_43) ).
fof(sos_42,axiom,
tptp1 != tptp3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_42) ).
fof(sos_39,axiom,
tptp4 != tptp1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_39) ).
fof(sos_44,axiom,
tptp3 != tptp2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_44) ).
fof(sos_41,axiom,
tptp4 != tptp2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_41) ).
fof(sos_40,axiom,
tptp4 != tptp3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_40) ).
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,negated_conjecture,
~ ~ ? [X108] : occurrence_of(X108,tptp0),
inference(assume_negation,[status(cth)],[goals]) ).
fof(i_0_54,plain,
! [X308,X309,X310,X311,X312,X313,X314] :
( ( min_precedes(X308,X309,X310)
| ~ next_subocc(X308,X309,X310) )
& ( ~ min_precedes(X308,X311,X310)
| ~ min_precedes(X311,X309,X310)
| ~ next_subocc(X308,X309,X310) )
& ( min_precedes(X312,esk12_3(X312,X313,X314),X314)
| ~ min_precedes(X312,X313,X314)
| next_subocc(X312,X313,X314) )
& ( min_precedes(esk12_3(X312,X313,X314),X313,X314)
| ~ min_precedes(X312,X313,X314)
| next_subocc(X312,X313,X314) ) ),
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_55,plain,
! [X331,X332,X333,X334] :
( ~ min_precedes(X331,X332,X334)
| ~ min_precedes(X331,X333,X334)
| ~ precedes(X332,X333)
| min_precedes(X332,X333,X334) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_31])]) ).
fof(i_0_56,plain,
! [X298,X299,X300] :
( ( root(esk11_3(X298,X299,X300),X300)
| ~ min_precedes(X298,X299,X300) )
& ( min_precedes(esk11_3(X298,X299,X300),X299,X300)
| ~ min_precedes(X298,X299,X300) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_23])])])]) ).
fof(i_0_57,plain,
! [X220,X221,X222,X223,X224] :
( ~ occurrence_of(X221,X220)
| ~ root_occ(X223,X221)
| ~ leaf_occ(X224,X221)
| ~ subactivity_occurrence(X222,X221)
| ~ min_precedes(X223,X222,X220)
| X222 = X224
| min_precedes(X222,X224,X220) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_01])]) ).
fof(i_0_58,plain,
! [X238,X239,X240] :
( ( occurrence_of(esk3_3(X238,X239,X240),X238)
| ~ min_precedes(X239,X240,X238) )
& ( subactivity_occurrence(X239,esk3_3(X238,X239,X240))
| ~ min_precedes(X239,X240,X238) )
& ( subactivity_occurrence(X240,esk3_3(X238,X239,X240))
| ~ min_precedes(X239,X240,X238) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_06])])])]) ).
fof(i_0_59,plain,
! [X231,X232,X233,X234] :
( ~ occurrence_of(X232,X231)
| ~ arboreal(X233)
| ~ arboreal(X234)
| ~ subactivity_occurrence(X233,X232)
| ~ subactivity_occurrence(X234,X232)
| min_precedes(X233,X234,X231)
| min_precedes(X234,X233,X231)
| X233 = X234 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_04])]) ).
fof(i_0_60,plain,
! [X267,X268,X270,X271,X272,X273] :
( ( root(X267,X268)
| min_precedes(esk7_2(X267,X268),X267,X268)
| ~ leaf(X267,X268) )
& ( ~ min_precedes(X267,X270,X268)
| ~ leaf(X267,X268) )
& ( ~ root(X271,X272)
| min_precedes(X271,esk8_2(X271,X272),X272)
| leaf(X271,X272) )
& ( ~ min_precedes(X273,X271,X272)
| min_precedes(X271,esk8_2(X271,X272),X272)
| leaf(X271,X272) ) ),
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_61,plain,
! [X316,X317,X318,X319] :
( ~ min_precedes(X316,X317,X318)
| ~ occurrence_of(X319,X318)
| ~ subactivity_occurrence(X317,X319)
| subactivity_occurrence(X316,X319) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_27])]) ).
fof(i_0_62,plain,
! [X225,X226,X227,X228] :
( ~ occurrence_of(X226,X225)
| ~ subactivity_occurrence(X227,X226)
| ~ leaf_occ(X228,X226)
| ~ arboreal(X227)
| min_precedes(X227,X228,X225)
| X228 = X227 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_47])]) ).
fof(i_0_63,plain,
! [X248,X249,X250,X251] :
( ~ occurrence_of(X248,X250)
| ~ leaf_occ(X249,X248)
| ~ min_precedes(X249,X251,X250) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_09])])]) ).
fof(i_0_64,plain,
! [X252,X253,X254,X255] :
( ~ occurrence_of(X252,X254)
| ~ root_occ(X253,X252)
| ~ min_precedes(X255,X253,X254) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_10])])]) ).
fof(i_0_65,plain,
! [X295,X296,X297] :
( ~ min_precedes(X295,X296,X297)
| ~ root(X296,X297) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_48])]) ).
fof(i_0_66,plain,
! [X338,X339] :
( ( occurrence_of(esk15_1(X338),tptp1)
| ~ occurrence_of(X339,tptp0)
| ~ root_occ(X338,X339) )
& ( next_subocc(X338,esk15_1(X338),tptp0)
| ~ occurrence_of(X339,tptp0)
| ~ root_occ(X338,X339) ) ),
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_45])])])])])]) ).
fof(i_0_67,plain,
! [X302,X303,X304] :
( ~ min_precedes(X302,X303,X304)
| precedes(X302,X303) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_24])]) ).
fof(i_0_68,plain,
! [X305,X306,X307] :
( ( arboreal(X305)
| ~ next_subocc(X305,X306,X307) )
& ( arboreal(X306)
| ~ next_subocc(X305,X306,X307) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_25])])]) ).
fof(i_0_69,plain,
! [X335] :
( ( occurrence_of(esk13_1(X335),tptp4)
| ~ occurrence_of(X335,tptp0) )
& ( root_occ(esk13_1(X335),X335)
| ~ occurrence_of(X335,tptp0) )
& ( occurrence_of(esk14_1(X335),tptp3)
| ~ occurrence_of(X335,tptp0) )
& ( leaf_occ(esk14_1(X335),X335)
| ~ occurrence_of(X335,tptp0) )
& ( next_subocc(esk13_1(X335),esk14_1(X335),tptp0)
| ~ occurrence_of(X335,tptp0) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_32])])])]) ).
fof(i_0_70,plain,
! [X279,X280,X282,X283,X284] :
( ( occurrence_of(X280,esk9_2(X279,X280))
| ~ leaf_occ(X279,X280) )
& ( subactivity_occurrence(X279,X280)
| ~ leaf_occ(X279,X280) )
& ( leaf(X279,esk9_2(X279,X280))
| ~ leaf_occ(X279,X280) )
& ( ~ occurrence_of(X283,X284)
| ~ subactivity_occurrence(X282,X283)
| ~ leaf(X282,X284)
| leaf_occ(X282,X283) ) ),
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_71,plain,
! [X285,X286,X288,X289,X290] :
( ( occurrence_of(X286,esk10_2(X285,X286))
| ~ root_occ(X285,X286) )
& ( subactivity_occurrence(X285,X286)
| ~ root_occ(X285,X286) )
& ( root(X285,esk10_2(X285,X286))
| ~ root_occ(X285,X286) )
& ( ~ occurrence_of(X289,X290)
| ~ subactivity_occurrence(X288,X289)
| ~ root(X288,X290)
| root_occ(X288,X289) ) ),
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_72,plain,
! [X320,X321,X322,X323] :
( ~ occurrence_of(X322,X323)
| atomic(X323)
| ~ leaf_occ(X320,X322)
| ~ leaf_occ(X321,X322)
| X320 = X321 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_49])]) ).
fof(i_0_73,plain,
! [X324,X325,X326,X327] :
( ~ occurrence_of(X326,X327)
| ~ root_occ(X324,X326)
| ~ root_occ(X325,X326)
| X324 = X325 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_29])]) ).
fof(i_0_74,plain,
! [X217,X218] :
( ( root(esk1_2(X217,X218),X217)
| ~ occurrence_of(X218,X217)
| atomic(X217) )
& ( subactivity_occurrence(esk1_2(X217,X218),X218)
| ~ occurrence_of(X218,X217)
| atomic(X217) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_50])])])]) ).
fof(i_0_75,plain,
! [X242,X243] :
( ( occurrence_of(esk4_2(X242,X243),X243)
| ~ leaf(X242,X243)
| atomic(X243) )
& ( leaf_occ(X242,esk4_2(X242,X243))
| ~ leaf(X242,X243)
| atomic(X243) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_51])])])]) ).
fof(i_0_76,plain,
! [X261,X262,X264,X265,X266] :
( ( subactivity(X262,esk6_2(X261,X262))
| ~ atocc(X261,X262) )
& ( atomic(esk6_2(X261,X262))
| ~ atocc(X261,X262) )
& ( occurrence_of(X261,esk6_2(X261,X262))
| ~ atocc(X261,X262) )
& ( ~ subactivity(X265,X266)
| ~ atomic(X266)
| ~ occurrence_of(X264,X266)
| atocc(X264,X265) ) ),
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_77,plain,
! [X235,X236] :
( ( subactivity(esk2_2(X235,X236),X235)
| ~ root(X236,X235) )
& ( atocc(X236,esk2_2(X235,X236))
| ~ root(X236,X235) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_05])])])]) ).
fof(i_0_78,plain,
! [X328,X329,X330] :
( ~ earlier(X328,X329)
| ~ earlier(X329,X330)
| earlier(X328,X330) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_30])]) ).
fof(i_0_79,plain,
! [X245,X246,X247] :
( ~ occurrence_of(X245,X246)
| ~ occurrence_of(X245,X247)
| X246 = X247 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_08])]) ).
fof(i_0_80,plain,
! [X291,X292] :
( ~ earlier(X291,X292)
| ~ earlier(X292,X291) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_52])]) ).
fof(i_0_81,plain,
! [X293,X294] :
( ( earlier(X293,X294)
| ~ precedes(X293,X294) )
& ( legal(X294)
| ~ precedes(X293,X294) )
& ( ~ earlier(X293,X294)
| ~ legal(X294)
| precedes(X293,X294) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_21])])]) ).
fof(i_0_82,plain,
! [X275,X276] :
( ( ~ arboreal(X275)
| atomic(X276)
| ~ occurrence_of(X275,X276) )
& ( ~ atomic(X276)
| arboreal(X275)
| ~ occurrence_of(X275,X276) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_16])])]) ).
fof(i_0_83,plain,
! [X258] :
( ( activity(esk5_1(X258))
| ~ activity_occurrence(X258) )
& ( occurrence_of(X258,esk5_1(X258))
| ~ activity_occurrence(X258) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_12])])])]) ).
fof(i_0_84,plain,
! [X277,X278] :
( ~ root(X277,X278)
| legal(X277) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_17])]) ).
fof(i_0_85,plain,
! [X256,X257] :
( ( activity_occurrence(X256)
| ~ subactivity_occurrence(X256,X257) )
& ( activity_occurrence(X257)
| ~ subactivity_occurrence(X256,X257) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_11])])]) ).
fof(i_0_86,plain,
! [X229,X230] :
( ( activity(X229)
| ~ occurrence_of(X230,X229) )
& ( activity_occurrence(X230)
| ~ occurrence_of(X230,X229) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_03])])]) ).
fof(i_0_87,plain,
! [X260] :
( ~ legal(X260)
| arboreal(X260) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_13])]) ).
fof(i_0_88,negated_conjecture,
occurrence_of(esk16_0,tptp0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_53])])]) ).
fof(i_0_89,plain,
~ atomic(tptp0),
inference(fof_simplification,[status(thm)],[sos_34]) ).
cnf(i_0_90,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_54]),
[final] ).
cnf(i_0_91,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_54]),
[final] ).
cnf(i_0_92,plain,
( ~ min_precedes(X1,X2,X3)
| ~ min_precedes(X2,X4,X3)
| ~ next_subocc(X1,X4,X3) ),
inference(split_conjunct,[status(thm)],[i_0_54]),
[final] ).
cnf(i_0_93,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_55]),
[final] ).
cnf(i_0_94,plain,
( min_precedes(esk11_3(X1,X2,X3),X2,X3)
| ~ min_precedes(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_95,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_57]),
[final] ).
cnf(i_0_96,plain,
( root(esk11_3(X1,X2,X3),X3)
| ~ min_precedes(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_97,plain,
( occurrence_of(esk3_3(X1,X2,X3),X1)
| ~ min_precedes(X2,X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_58]),
[final] ).
cnf(i_0_98,plain,
( subactivity_occurrence(X1,esk3_3(X2,X1,X3))
| ~ min_precedes(X1,X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_58]),
[final] ).
cnf(i_0_99,plain,
( subactivity_occurrence(X1,esk3_3(X2,X3,X1))
| ~ min_precedes(X3,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_58]),
[final] ).
cnf(i_0_100,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_59]),
[final] ).
cnf(i_0_101,plain,
( min_precedes(X2,esk8_2(X2,X3),X3)
| leaf(X2,X3)
| ~ min_precedes(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_102,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_103,plain,
( min_precedes(X1,X2,X3)
| ~ next_subocc(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_54]),
[final] ).
cnf(i_0_104,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_105,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_106,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_107,plain,
( root(X1,X2)
| min_precedes(esk7_2(X1,X2),X1,X2)
| ~ leaf(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_108,plain,
( min_precedes(X1,esk8_2(X1,X2),X2)
| leaf(X1,X2)
| ~ root(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_109,plain,
( ~ min_precedes(X1,X2,X3)
| ~ leaf(X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_110,plain,
( ~ min_precedes(X1,X2,X3)
| ~ root(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_65]),
[final] ).
cnf(i_0_111,plain,
( next_subocc(X1,esk15_1(X1),tptp0)
| ~ occurrence_of(X2,tptp0)
| ~ root_occ(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_66]),
[final] ).
cnf(i_0_112,plain,
( precedes(X1,X2)
| ~ min_precedes(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_113,plain,
( arboreal(X1)
| ~ next_subocc(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_114,plain,
( arboreal(X1)
| ~ next_subocc(X2,X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_115,plain,
( next_subocc(esk13_1(X1),esk14_1(X1),tptp0)
| ~ occurrence_of(X1,tptp0) ),
inference(split_conjunct,[status(thm)],[i_0_69]),
[final] ).
cnf(i_0_116,plain,
( leaf_occ(X3,X1)
| ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X3,X1)
| ~ leaf(X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_70]),
[final] ).
cnf(i_0_117,plain,
( root_occ(X3,X1)
| ~ occurrence_of(X1,X2)
| ~ subactivity_occurrence(X3,X1)
| ~ root(X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_71]),
[final] ).
cnf(i_0_118,plain,
( atomic(X2)
| X3 = X4
| ~ occurrence_of(X1,X2)
| ~ leaf_occ(X3,X1)
| ~ leaf_occ(X4,X1) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_119,plain,
( X3 = X4
| ~ occurrence_of(X1,X2)
| ~ root_occ(X3,X1)
| ~ root_occ(X4,X1) ),
inference(split_conjunct,[status(thm)],[i_0_73]),
[final] ).
cnf(i_0_120,plain,
( subactivity_occurrence(esk1_2(X1,X2),X2)
| atomic(X1)
| ~ occurrence_of(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_74]),
[final] ).
cnf(i_0_121,plain,
( root(esk1_2(X1,X2),X1)
| atomic(X1)
| ~ occurrence_of(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_74]),
[final] ).
cnf(i_0_122,plain,
( occurrence_of(esk4_2(X1,X2),X2)
| atomic(X2)
| ~ leaf(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_75]),
[final] ).
cnf(i_0_123,plain,
( leaf_occ(X1,esk4_2(X1,X2))
| atomic(X2)
| ~ leaf(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_75]),
[final] ).
cnf(i_0_124,plain,
( atocc(X3,X1)
| ~ subactivity(X1,X2)
| ~ atomic(X2)
| ~ occurrence_of(X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_76]),
[final] ).
cnf(i_0_125,plain,
( subactivity(esk2_2(X1,X2),X1)
| ~ root(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_77]),
[final] ).
cnf(i_0_126,plain,
( leaf(X1,esk9_2(X1,X2))
| ~ leaf_occ(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_70]),
[final] ).
cnf(i_0_127,plain,
( atocc(X1,esk2_2(X2,X1))
| ~ root(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_77]),
[final] ).
cnf(i_0_128,plain,
( subactivity(X1,esk6_2(X2,X1))
| ~ atocc(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_76]),
[final] ).
cnf(i_0_129,plain,
( root(X1,esk10_2(X1,X2))
| ~ root_occ(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_71]),
[final] ).
cnf(i_0_130,plain,
( occurrence_of(X1,esk10_2(X2,X1))
| ~ root_occ(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_71]),
[final] ).
cnf(i_0_131,plain,
( occurrence_of(X1,esk9_2(X2,X1))
| ~ leaf_occ(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_70]),
[final] ).
cnf(i_0_132,plain,
( occurrence_of(X1,esk6_2(X1,X2))
| ~ atocc(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_76]),
[final] ).
cnf(i_0_133,plain,
( occurrence_of(esk15_1(X1),tptp1)
| ~ occurrence_of(X2,tptp0)
| ~ root_occ(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_66]),
[final] ).
cnf(i_0_134,plain,
( earlier(X1,X3)
| ~ earlier(X1,X2)
| ~ earlier(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_78]),
[final] ).
cnf(i_0_135,plain,
( atomic(esk6_2(X1,X2))
| ~ atocc(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_76]),
[final] ).
cnf(i_0_136,plain,
( X2 = X3
| ~ occurrence_of(X1,X2)
| ~ occurrence_of(X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_79]),
[final] ).
cnf(i_0_137,plain,
( ~ earlier(X1,X2)
| ~ earlier(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_80]),
[final] ).
cnf(i_0_138,plain,
( precedes(X1,X2)
| ~ earlier(X1,X2)
| ~ legal(X2) ),
inference(split_conjunct,[status(thm)],[i_0_81]),
[final] ).
cnf(i_0_139,plain,
( leaf_occ(esk14_1(X1),X1)
| ~ occurrence_of(X1,tptp0) ),
inference(split_conjunct,[status(thm)],[i_0_69]),
[final] ).
cnf(i_0_140,plain,
( root_occ(esk13_1(X1),X1)
| ~ occurrence_of(X1,tptp0) ),
inference(split_conjunct,[status(thm)],[i_0_69]),
[final] ).
cnf(i_0_141,plain,
( occurrence_of(esk14_1(X1),tptp3)
| ~ occurrence_of(X1,tptp0) ),
inference(split_conjunct,[status(thm)],[i_0_69]),
[final] ).
cnf(i_0_142,plain,
( occurrence_of(esk13_1(X1),tptp4)
| ~ occurrence_of(X1,tptp0) ),
inference(split_conjunct,[status(thm)],[i_0_69]),
[final] ).
cnf(i_0_143,plain,
( earlier(X1,X2)
| ~ precedes(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_81]),
[final] ).
cnf(i_0_144,plain,
( subactivity_occurrence(X1,X2)
| ~ leaf_occ(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_70]),
[final] ).
cnf(i_0_145,plain,
( subactivity_occurrence(X1,X2)
| ~ root_occ(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_71]),
[final] ).
cnf(i_0_146,plain,
( arboreal(X2)
| ~ atomic(X1)
| ~ occurrence_of(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_82]),
[final] ).
cnf(i_0_147,plain,
( atomic(X2)
| ~ arboreal(X1)
| ~ occurrence_of(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_82]),
[final] ).
cnf(i_0_148,plain,
( occurrence_of(X1,esk5_1(X1))
| ~ activity_occurrence(X1) ),
inference(split_conjunct,[status(thm)],[i_0_83]),
[final] ).
cnf(i_0_149,plain,
( legal(X1)
| ~ precedes(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_81]),
[final] ).
cnf(i_0_150,plain,
( legal(X1)
| ~ root(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_84]),
[final] ).
cnf(i_0_151,plain,
( activity_occurrence(X1)
| ~ subactivity_occurrence(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_85]),
[final] ).
cnf(i_0_152,plain,
( activity_occurrence(X1)
| ~ subactivity_occurrence(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_85]),
[final] ).
cnf(i_0_153,plain,
( activity_occurrence(X1)
| ~ occurrence_of(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_86]),
[final] ).
cnf(i_0_154,plain,
( activity(X1)
| ~ occurrence_of(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_86]),
[final] ).
cnf(i_0_155,plain,
( activity(esk5_1(X1))
| ~ activity_occurrence(X1) ),
inference(split_conjunct,[status(thm)],[i_0_83]),
[final] ).
cnf(i_0_156,plain,
( arboreal(X1)
| ~ legal(X1) ),
inference(split_conjunct,[status(thm)],[i_0_87]),
[final] ).
cnf(i_0_157,negated_conjecture,
occurrence_of(esk16_0,tptp0),
inference(split_conjunct,[status(thm)],[i_0_88]),
[final] ).
cnf(i_0_158,plain,
~ atomic(tptp0),
inference(split_conjunct,[status(thm)],[i_0_89]),
[final] ).
cnf(i_0_159,plain,
activity(tptp0),
inference(split_conjunct,[status(thm)],[sos_33]),
[final] ).
cnf(i_0_160,plain,
atomic(tptp1),
inference(split_conjunct,[status(thm)],[sos_38]),
[final] ).
cnf(i_0_161,plain,
atomic(tptp2),
inference(split_conjunct,[status(thm)],[sos_37]),
[final] ).
cnf(i_0_162,plain,
atomic(tptp3),
inference(split_conjunct,[status(thm)],[sos_36]),
[final] ).
cnf(i_0_163,plain,
atomic(tptp4),
inference(split_conjunct,[status(thm)],[sos_35]),
[final] ).
cnf(i_0_164,plain,
tptp1 != tptp2,
inference(split_conjunct,[status(thm)],[sos_43]),
[final] ).
cnf(i_0_165,plain,
tptp1 != tptp3,
inference(split_conjunct,[status(thm)],[sos_42]),
[final] ).
cnf(i_0_166,plain,
tptp4 != tptp1,
inference(split_conjunct,[status(thm)],[sos_39]),
[final] ).
cnf(i_0_167,plain,
tptp3 != tptp2,
inference(split_conjunct,[status(thm)],[sos_44]),
[final] ).
cnf(i_0_168,plain,
tptp4 != tptp2,
inference(split_conjunct,[status(thm)],[sos_41]),
[final] ).
cnf(i_0_169,plain,
tptp4 != tptp3,
inference(split_conjunct,[status(thm)],[sos_40]),
[final] ).
cnf(i_0_170,axiom,
X1 = X1 ).
cnf(i_0_171,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_172,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_173,axiom,
( X1 != X2
| ~ min_precedes(X1,X3,X4)
| min_precedes(X2,X3,X4) ) ).
cnf(i_0_174,axiom,
( X1 != X2
| ~ min_precedes(X3,X1,X4)
| min_precedes(X3,X2,X4) ) ).
cnf(i_0_175,axiom,
( X1 != X2
| ~ min_precedes(X3,X4,X1)
| min_precedes(X3,X4,X2) ) ).
cnf(i_0_176,axiom,
( X1 != X2
| ~ leaf(X1,X3)
| leaf(X2,X3) ) ).
cnf(i_0_177,axiom,
( X1 != X2
| ~ leaf(X3,X1)
| leaf(X3,X2) ) ).
cnf(i_0_178,axiom,
( X1 != X2
| ~ atomic(X1)
| atomic(X2) ) ).
cnf(i_0_179,axiom,
( X1 != X2
| ~ atocc(X1,X3)
| atocc(X2,X3) ) ).
cnf(i_0_180,axiom,
( X1 != X2
| ~ atocc(X3,X1)
| atocc(X3,X2) ) ).
cnf(i_0_181,axiom,
( X1 != X2
| ~ subactivity(X1,X3)
| subactivity(X2,X3) ) ).
cnf(i_0_182,axiom,
( X1 != X2
| ~ subactivity(X3,X1)
| subactivity(X3,X2) ) ).
cnf(i_0_183,axiom,
( X1 != X2
| ~ earlier(X1,X3)
| earlier(X2,X3) ) ).
cnf(i_0_184,axiom,
( X1 != X2
| ~ earlier(X3,X1)
| earlier(X3,X2) ) ).
cnf(i_0_185,axiom,
( X1 != X2
| ~ legal(X1)
| legal(X2) ) ).
cnf(i_0_186,axiom,
( X1 != X2
| ~ activity_occurrence(X1)
| activity_occurrence(X2) ) ).
cnf(i_0_187,axiom,
( X1 != X2
| ~ activity(X1)
| activity(X2) ) ).
cnf(i_0_188,axiom,
( X1 != X2
| ~ next_subocc(X1,X3,X4)
| next_subocc(X2,X3,X4) ) ).
cnf(i_0_189,axiom,
( X1 != X2
| ~ next_subocc(X3,X1,X4)
| next_subocc(X3,X2,X4) ) ).
cnf(i_0_190,axiom,
( X1 != X2
| ~ next_subocc(X3,X4,X1)
| next_subocc(X3,X4,X2) ) ).
cnf(i_0_191,axiom,
( X1 != X2
| ~ precedes(X1,X3)
| precedes(X2,X3) ) ).
cnf(i_0_192,axiom,
( X1 != X2
| ~ precedes(X3,X1)
| precedes(X3,X2) ) ).
cnf(i_0_193,axiom,
( X1 != X2
| ~ occurrence_of(X1,X3)
| occurrence_of(X2,X3) ) ).
cnf(i_0_194,axiom,
( X1 != X2
| ~ occurrence_of(X3,X1)
| occurrence_of(X3,X2) ) ).
cnf(i_0_195,axiom,
( X1 != X2
| ~ root_occ(X1,X3)
| root_occ(X2,X3) ) ).
cnf(i_0_196,axiom,
( X1 != X2
| ~ root_occ(X3,X1)
| root_occ(X3,X2) ) ).
cnf(i_0_197,axiom,
( X1 != X2
| ~ leaf_occ(X1,X3)
| leaf_occ(X2,X3) ) ).
cnf(i_0_198,axiom,
( X1 != X2
| ~ leaf_occ(X3,X1)
| leaf_occ(X3,X2) ) ).
cnf(i_0_199,axiom,
( X1 != X2
| ~ subactivity_occurrence(X1,X3)
| subactivity_occurrence(X2,X3) ) ).
cnf(i_0_200,axiom,
( X1 != X2
| ~ subactivity_occurrence(X3,X1)
| subactivity_occurrence(X3,X2) ) ).
cnf(i_0_201,axiom,
( X1 != X2
| ~ root(X1,X3)
| root(X2,X3) ) ).
cnf(i_0_202,axiom,
( X1 != X2
| ~ root(X3,X1)
| root(X3,X2) ) ).
cnf(i_0_203,axiom,
( X1 != X2
| ~ arboreal(X1)
| arboreal(X2) ) ).
cnf(i_0_5195,plain,
root(esk13_1(esk16_0),tptp0),
inference(scs_inference,[],[i_0_5184,i_0_4632,i_0_201]) ).
cnf(i_0_5196,plain,
next_subocc(esk1_2(tptp0,esk16_0),esk14_1(esk16_0),tptp0),
inference(scs_inference,[],[i_0_5182,i_0_5184,i_0_4632,i_0_4624,i_0_201,i_0_188]) ).
cnf(i_0_5197,plain,
occurrence_of(esk1_2(tptp0,esk16_0),tptp4),
inference(scs_inference,[],[i_0_5182,i_0_5184,i_0_4632,i_0_4624,i_0_4622,i_0_201,i_0_188,i_0_193]) ).
cnf(i_0_5198,plain,
legal(esk13_1(esk16_0)),
inference(scs_inference,[],[i_0_5182,i_0_5184,i_0_4632,i_0_4624,i_0_4622,i_0_201,i_0_188,i_0_193,i_0_150]) ).
cnf(i_0_4738,plain,
~ leaf(esk1_2(tptp0,esk16_0),tptp0),
inference(scs_inference,[],[i_0_157,i_0_4711,i_0_4719,i_0_4630,i_0_4699,i_0_4622,i_0_212,i_0_166,i_0_171,i_0_136,i_0_93,i_0_116]) ).
cnf(i_0_4742,plain,
~ earlier(esk14_1(esk16_0),esk14_1(esk16_0)),
inference(scs_inference,[],[i_0_157,i_0_4711,i_0_4706,i_0_4725,i_0_4719,i_0_4630,i_0_4699,i_0_4622,i_0_212,i_0_166,i_0_171,i_0_136,i_0_93,i_0_116,i_0_92,i_0_138]) ).
cnf(i_0_4781,plain,
min_precedes(esk13_1(esk16_0),esk14_1(esk16_0),tptp0),
inference(equality_inference,[],[4778]) ).
cnf(i_0_4787,plain,
precedes(esk13_1(esk16_0),esk14_1(esk16_0)),
inference(equality_inference,[],[4786]) ).
cnf(i_0_4934,plain,
~ leaf(esk1_2(tptp0,esk16_0),esk5_1(esk16_0)),
inference(scs_inference,[],[i_0_4711,i_0_4616,i_0_4630,i_0_116]) ).
cnf(i_0_4936,plain,
~ min_precedes(esk14_1(esk16_0),X1,esk5_1(esk16_0)),
inference(scs_inference,[],[i_0_4711,i_0_4616,i_0_204,i_0_4630,i_0_116,i_0_105]) ).
cnf(i_0_4938,plain,
~ min_precedes(X1,esk1_2(tptp0,esk16_0),esk5_1(esk16_0)),
inference(scs_inference,[],[i_0_4711,i_0_4638,i_0_4616,i_0_204,i_0_4630,i_0_116,i_0_105,i_0_106]) ).
cnf(i_0_5183,plain,
min_precedes(esk1_2(tptp0,esk16_0),esk14_1(esk16_0),tptp0),
inference(scs_inference,[],[i_0_5177,i_0_4824]) ).
cnf(i_0_5208,plain,
~ occurrence_of(esk1_2(tptp0,esk16_0),tptp3),
inference(scs_inference,[],[i_0_169,i_0_5197,i_0_136]) ).
cnf(i_0_5213,plain,
~ occurrence_of(esk1_2(tptp0,esk16_0),tptp1),
inference(scs_inference,[],[i_0_5197,i_0_5184,i_0_4732,i_0_198,i_0_136]) ).
cnf(i_0_4731,plain,
leaf(esk14_1(esk16_0),tptp0),
inference(equality_inference,[],[4729]) ).
cnf(i_0_4745,plain,
subactivity_occurrence(esk1_2(tptp0,esk16_0),esk16_0),
inference(equality_inference,[],[4744]) ).
cnf(i_0_4765,plain,
min_precedes(esk13_1(esk16_0),esk14_1(esk16_0),esk5_1(esk16_0)),
inference(equality_inference,[],[4761]) ).
cnf(i_0_4777,plain,
min_precedes(esk13_1(esk16_0),esk14_1(esk16_0),esk5_1(esk16_0)),
inference(equality_inference,[],[4773]) ).
cnf(i_0_4799,plain,
subactivity_occurrence(esk1_2(tptp0,esk16_0),esk16_0),
inference(equality_inference,[],[4798]) ).
cnf(i_0_4843,plain,
min_precedes(esk13_1(esk16_0),esk14_1(esk16_0),esk5_1(esk16_0)),
inference(equality_inference,[],[4842]) ).
cnf(i_0_4946,plain,
~ next_subocc(X1,esk1_2(tptp0,esk16_0),esk5_1(esk16_0)),
inference(scs_inference,[],[i_0_4938,i_0_103]) ).
cnf(i_0_4948,plain,
leaf(esk14_1(esk16_0),esk5_1(esk16_0)),
inference(scs_inference,[],[i_0_4938,i_0_4936,i_0_4725,i_0_103,i_0_101]) ).
cnf(i_0_4949,plain,
~ min_precedes(esk14_1(esk16_0),X1,esk5_1(esk16_0)),
inference(rename_variables,[],[i_0_4936]) ).
cnf(i_0_4955,plain,
~ next_subocc(esk14_1(esk16_0),X1,esk5_1(esk16_0)),
inference(scs_inference,[],[i_0_4936,i_0_103]) ).
cnf(i_0_4989,plain,
~ min_precedes(esk14_1(esk16_0),X1,esk5_1(esk16_0)),
inference(rename_variables,[],[i_0_4936]) ).
cnf(i_0_4991,plain,
~ min_precedes(esk14_1(esk16_0),X1,esk5_1(esk16_0)),
inference(rename_variables,[],[i_0_4936]) ).
cnf(i_0_5027,plain,
~ min_precedes(X1,esk1_2(tptp0,esk16_0),esk5_1(esk16_0)),
inference(rename_variables,[],[i_0_4938]) ).
cnf(i_0_5030,plain,
~ min_precedes(esk14_1(esk16_0),X1,esk5_1(esk16_0)),
inference(rename_variables,[],[i_0_4936]) ).
cnf(i_0_5043,plain,
~ min_precedes(esk14_1(esk16_0),X1,esk5_1(esk16_0)),
inference(rename_variables,[],[i_0_4936]) ).
cnf(i_0_5048,plain,
~ min_precedes(X1,esk1_2(tptp0,esk16_0),esk5_1(esk16_0)),
inference(rename_variables,[],[i_0_4938]) ).
cnf(i_0_5085,plain,
~ min_precedes(X1,esk1_2(tptp0,esk16_0),esk5_1(esk16_0)),
inference(rename_variables,[],[i_0_4938]) ).
cnf(i_0_5087,plain,
~ min_precedes(esk14_1(esk16_0),X1,esk5_1(esk16_0)),
inference(rename_variables,[],[i_0_4936]) ).
cnf(i_0_5136,plain,
~ min_precedes(X1,esk1_2(tptp0,esk16_0),esk5_1(esk16_0)),
inference(rename_variables,[],[i_0_4938]) ).
cnf(i_0_5156,plain,
~ min_precedes(X1,esk1_2(tptp0,esk16_0),esk5_1(esk16_0)),
inference(rename_variables,[],[i_0_4938]) ).
cnf(i_0_5169,plain,
~ min_precedes(X1,esk1_2(tptp0,esk16_0),esk5_1(esk16_0)),
inference(rename_variables,[],[i_0_4938]) ).
cnf(i_0_5179,plain,
min_precedes(esk1_2(tptp0,esk16_0),esk14_1(esk16_0),esk5_1(esk16_0)),
inference(scs_inference,[],[i_0_4693,i_0_4936,i_0_4640,i_0_4628,i_0_208,i_0_4630,i_0_4616,i_0_156,i_0_100]) ).
cnf(i_0_5180,plain,
~ min_precedes(esk14_1(esk16_0),X1,esk5_1(esk16_0)),
inference(rename_variables,[],[i_0_4936]) ).
cnf(i_0_5191,plain,
~ min_precedes(esk14_1(esk16_0),X1,esk5_1(esk16_0)),
inference(rename_variables,[],[i_0_4936]) ).
cnf(i_0_4954,plain,
leaf(esk14_1(esk16_0),esk5_1(esk16_0)),
inference(equality_inference,[],[4951]) ).
cnf(i_0_5186,plain,
precedes(esk1_2(tptp0,esk16_0),esk14_1(esk16_0)),
inference(scs_inference,[],[i_0_5179,i_0_112]) ).
cnf(i_0_5188,plain,
~ occurrence_of(esk1_2(tptp0,esk16_0),tptp0),
inference(scs_inference,[],[i_0_5177,i_0_5179,i_0_158,i_0_112,i_0_147]) ).
cnf(i_0_5207,plain,
min_precedes(esk13_1(esk16_0),esk8_2(esk13_1(esk16_0),tptp0),tptp0),
inference(scs_inference,[],[i_0_5195,i_0_4898]) ).
cnf(i_0_5194,plain,
precedes(esk1_2(tptp0,esk16_0),esk14_1(esk16_0)),
inference(equality_inference,[],[5190]) ).
cnf(c_0_5215,plain,
( root(esk1_2(X1,X2),X1)
| atomic(X1)
| ~ occurrence_of(X2,X1) ),
i_0_121 ).
cnf(c_0_5216,negated_conjecture,
occurrence_of(esk16_0,tptp0),
i_0_157 ).
cnf(c_0_5217,plain,
~ atomic(tptp0),
i_0_158 ).
cnf(c_0_5218,plain,
( root_occ(X1,X2)
| ~ occurrence_of(X2,X3)
| ~ subactivity_occurrence(X1,X2)
| ~ root(X1,X3) ),
i_0_117 ).
cnf(c_0_5219,negated_conjecture,
root(esk1_2(tptp0,esk16_0),tptp0),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_5215,c_0_5216]),c_0_5217]) ).
cnf(c_0_5220,plain,
( X1 = X2
| ~ occurrence_of(X3,X4)
| ~ root_occ(X1,X3)
| ~ root_occ(X2,X3) ),
i_0_119 ).
cnf(c_0_5221,plain,
( root_occ(esk1_2(tptp0,esk16_0),X1)
| ~ subactivity_occurrence(esk1_2(tptp0,esk16_0),X1)
| ~ occurrence_of(X1,tptp0) ),
inference(spm,[status(thm)],[c_0_5218,c_0_5219]) ).
cnf(c_0_5222,plain,
( subactivity_occurrence(X1,X2)
| ~ min_precedes(X1,X3,X4)
| ~ occurrence_of(X2,X4)
| ~ subactivity_occurrence(X3,X2) ),
i_0_102 ).
cnf(c_0_5223,plain,
min_precedes(esk1_2(tptp0,esk16_0),esk14_1(esk16_0),tptp0),
i_0_5183 ).
cnf(c_0_5224,plain,
( leaf_occ(X1,esk4_2(X1,X2))
| atomic(X2)
| ~ leaf(X1,X2) ),
i_0_123 ).
cnf(c_0_5225,plain,
leaf(esk14_1(esk16_0),tptp0),
i_0_4731 ).
cnf(c_0_5226,plain,
( X1 = esk1_2(tptp0,esk16_0)
| ~ subactivity_occurrence(esk1_2(tptp0,esk16_0),X2)
| ~ root_occ(X1,X2)
| ~ occurrence_of(X2,tptp0)
| ~ occurrence_of(X2,X3) ),
inference(spm,[status(thm)],[c_0_5220,c_0_5221]) ).
cnf(c_0_5227,plain,
( subactivity_occurrence(esk1_2(tptp0,esk16_0),X1)
| ~ subactivity_occurrence(esk14_1(esk16_0),X1)
| ~ occurrence_of(X1,tptp0) ),
inference(spm,[status(thm)],[c_0_5222,c_0_5223]) ).
cnf(c_0_5228,plain,
( subactivity_occurrence(X1,X2)
| ~ leaf_occ(X1,X2) ),
i_0_144 ).
cnf(c_0_5229,plain,
leaf_occ(esk14_1(esk16_0),esk4_2(esk14_1(esk16_0),tptp0)),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_5224,c_0_5225]),c_0_5217]) ).
cnf(c_0_5230,plain,
( occurrence_of(esk4_2(X1,X2),X2)
| atomic(X2)
| ~ leaf(X1,X2) ),
i_0_122 ).
cnf(c_0_5231,plain,
( X1 = esk1_2(tptp0,esk16_0)
| ~ subactivity_occurrence(esk14_1(esk16_0),X2)
| ~ root_occ(X1,X2)
| ~ occurrence_of(X2,tptp0)
| ~ occurrence_of(X2,X3) ),
inference(spm,[status(thm)],[c_0_5226,c_0_5227]) ).
cnf(c_0_5232,plain,
subactivity_occurrence(esk14_1(esk16_0),esk4_2(esk14_1(esk16_0),tptp0)),
inference(spm,[status(thm)],[c_0_5228,c_0_5229]) ).
cnf(c_0_5233,plain,
occurrence_of(esk4_2(esk14_1(esk16_0),tptp0),tptp0),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_5230,c_0_5225]),c_0_5217]) ).
cnf(c_0_5234,plain,
( next_subocc(X1,esk15_1(X1),tptp0)
| ~ occurrence_of(X2,tptp0)
| ~ root_occ(X1,X2) ),
i_0_111 ).
cnf(c_0_5235,plain,
( X1 = esk1_2(tptp0,esk16_0)
| ~ root_occ(X1,esk4_2(esk14_1(esk16_0),tptp0))
| ~ occurrence_of(esk4_2(esk14_1(esk16_0),tptp0),X2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_5231,c_0_5232]),c_0_5233])]) ).
cnf(c_0_5236,plain,
( root_occ(esk13_1(X1),X1)
| ~ occurrence_of(X1,tptp0) ),
i_0_140 ).
cnf(c_0_5237,plain,
( X1 = X2
| ~ occurrence_of(X3,X1)
| ~ occurrence_of(X3,X2) ),
i_0_136 ).
cnf(c_0_5238,plain,
( occurrence_of(X1,esk10_2(X2,X1))
| ~ root_occ(X2,X1) ),
i_0_130 ).
cnf(c_0_5239,plain,
( subactivity_occurrence(esk1_2(X1,X2),X2)
| atomic(X1)
| ~ occurrence_of(X2,X1) ),
i_0_120 ).
cnf(c_0_5240,plain,
( occurrence_of(esk3_3(X1,X2,X3),X1)
| ~ min_precedes(X2,X3,X1) ),
i_0_97 ).
cnf(c_0_5241,plain,
( min_precedes(X1,X2,X3)
| ~ next_subocc(X1,X2,X3) ),
i_0_103 ).
cnf(c_0_5242,negated_conjecture,
( next_subocc(X1,esk15_1(X1),tptp0)
| ~ root_occ(X1,esk16_0) ),
inference(spm,[status(thm)],[c_0_5234,c_0_5216]) ).
cnf(c_0_5243,plain,
( esk13_1(esk4_2(esk14_1(esk16_0),tptp0)) = esk1_2(tptp0,esk16_0)
| ~ occurrence_of(esk4_2(esk14_1(esk16_0),tptp0),X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_5235,c_0_5236]),c_0_5233])]) ).
cnf(c_0_5244,plain,
subactivity_occurrence(esk1_2(tptp0,esk16_0),esk16_0),
i_0_4745 ).
cnf(c_0_5245,plain,
( X1 = esk10_2(X2,X3)
| ~ root_occ(X2,X3)
| ~ occurrence_of(X3,X1) ),
inference(spm,[status(thm)],[c_0_5237,c_0_5238]) ).
cnf(c_0_5246,plain,
( atomic(X1)
| subactivity_occurrence(esk1_2(X1,esk3_3(X1,X2,X3)),esk3_3(X1,X2,X3))
| ~ min_precedes(X2,X3,X1) ),
inference(spm,[status(thm)],[c_0_5239,c_0_5240]) ).
cnf(c_0_5247,plain,
( min_precedes(X1,esk15_1(X1),tptp0)
| ~ root_occ(X1,esk16_0) ),
inference(spm,[status(thm)],[c_0_5241,c_0_5242]) ).
cnf(c_0_5248,plain,
esk13_1(esk4_2(esk14_1(esk16_0),tptp0)) = esk1_2(tptp0,esk16_0),
inference(spm,[status(thm)],[c_0_5243,c_0_5233]) ).
cnf(c_0_5249,plain,
( X1 = esk1_2(tptp0,esk16_0)
| ~ root_occ(X1,esk16_0)
| ~ occurrence_of(esk16_0,X2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_5226,c_0_5244]),c_0_5216])]) ).
cnf(c_0_5250,plain,
( X1 = esk10_2(esk1_2(tptp0,esk16_0),X2)
| ~ subactivity_occurrence(esk1_2(tptp0,esk16_0),X2)
| ~ occurrence_of(X2,tptp0)
| ~ occurrence_of(X2,X1) ),
inference(spm,[status(thm)],[c_0_5245,c_0_5221]) ).
cnf(c_0_5251,plain,
( subactivity_occurrence(X1,esk3_3(X2,X1,X3))
| ~ min_precedes(X1,X3,X2) ),
i_0_98 ).
cnf(c_0_5252,plain,
( activity_occurrence(X1)
| ~ subactivity_occurrence(X2,X1) ),
i_0_152 ).
cnf(c_0_5253,plain,
( subactivity_occurrence(esk1_2(tptp0,esk3_3(tptp0,X1,esk15_1(X1))),esk3_3(tptp0,X1,esk15_1(X1)))
| ~ root_occ(X1,esk16_0) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_5246,c_0_5247]),c_0_5217]) ).
cnf(c_0_5254,plain,
( next_subocc(X1,esk15_1(X1),tptp0)
| ~ root_occ(X1,esk4_2(esk14_1(esk16_0),tptp0)) ),
inference(spm,[status(thm)],[c_0_5234,c_0_5233]) ).
cnf(c_0_5255,plain,
root_occ(esk1_2(tptp0,esk16_0),esk4_2(esk14_1(esk16_0),tptp0)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_5236,c_0_5248]),c_0_5233])]) ).
cnf(c_0_5256,plain,
( esk13_1(esk16_0) = esk1_2(tptp0,esk16_0)
| ~ occurrence_of(esk16_0,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_5249,c_0_5236]),c_0_5216])]) ).
cnf(c_0_5257,plain,
( X1 = esk10_2(esk1_2(tptp0,esk16_0),esk3_3(X2,esk1_2(tptp0,esk16_0),X3))
| ~ occurrence_of(esk3_3(X2,esk1_2(tptp0,esk16_0),X3),tptp0)
| ~ occurrence_of(esk3_3(X2,esk1_2(tptp0,esk16_0),X3),X1)
| ~ min_precedes(esk1_2(tptp0,esk16_0),X3,X2) ),
inference(spm,[status(thm)],[c_0_5250,c_0_5251]) ).
cnf(c_0_5258,plain,
( occurrence_of(X1,esk5_1(X1))
| ~ activity_occurrence(X1) ),
i_0_148 ).
cnf(c_0_5259,plain,
( activity_occurrence(esk3_3(tptp0,X1,esk15_1(X1)))
| ~ root_occ(X1,esk16_0) ),
inference(spm,[status(thm)],[c_0_5252,c_0_5253]) ).
cnf(c_0_5260,plain,
next_subocc(esk1_2(tptp0,esk16_0),esk15_1(esk1_2(tptp0,esk16_0)),tptp0),
inference(spm,[status(thm)],[c_0_5254,c_0_5255]) ).
cnf(c_0_5261,negated_conjecture,
esk13_1(esk16_0) = esk1_2(tptp0,esk16_0),
inference(spm,[status(thm)],[c_0_5256,c_0_5216]) ).
cnf(c_0_5262,plain,
( activity_occurrence(X1)
| ~ occurrence_of(X1,X2) ),
i_0_153 ).
cnf(c_0_5263,plain,
( X1 = esk10_2(esk1_2(tptp0,esk16_0),esk3_3(tptp0,esk1_2(tptp0,esk16_0),X2))
| ~ occurrence_of(esk3_3(tptp0,esk1_2(tptp0,esk16_0),X2),X1)
| ~ min_precedes(esk1_2(tptp0,esk16_0),X2,tptp0) ),
inference(spm,[status(thm)],[c_0_5257,c_0_5240]) ).
cnf(c_0_5264,plain,
( occurrence_of(esk3_3(tptp0,X1,esk15_1(X1)),esk5_1(esk3_3(tptp0,X1,esk15_1(X1))))
| ~ root_occ(X1,esk16_0) ),
inference(spm,[status(thm)],[c_0_5258,c_0_5259]) ).
cnf(c_0_5265,plain,
min_precedes(esk1_2(tptp0,esk16_0),esk15_1(esk1_2(tptp0,esk16_0)),tptp0),
inference(spm,[status(thm)],[c_0_5241,c_0_5260]) ).
cnf(c_0_5266,plain,
root_occ(esk1_2(tptp0,esk16_0),esk16_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_5236,c_0_5261]),c_0_5216])]) ).
cnf(c_0_5267,plain,
( X1 = esk13_1(X2)
| ~ root_occ(X1,X2)
| ~ occurrence_of(X2,tptp0)
| ~ occurrence_of(X2,X3) ),
inference(spm,[status(thm)],[c_0_5220,c_0_5236]) ).
cnf(c_0_5268,plain,
( activity_occurrence(esk3_3(X1,X2,X3))
| ~ min_precedes(X2,X3,X1) ),
inference(spm,[status(thm)],[c_0_5262,c_0_5240]) ).
cnf(c_0_5269,plain,
( esk10_2(esk1_2(tptp0,esk16_0),esk3_3(tptp0,esk1_2(tptp0,esk16_0),X1)) = tptp0
| ~ min_precedes(esk1_2(tptp0,esk16_0),X1,tptp0) ),
inference(spm,[status(thm)],[c_0_5263,c_0_5240]) ).
cnf(c_0_5270,plain,
esk10_2(esk1_2(tptp0,esk16_0),esk3_3(tptp0,esk1_2(tptp0,esk16_0),esk15_1(esk1_2(tptp0,esk16_0)))) = esk5_1(esk3_3(tptp0,esk1_2(tptp0,esk16_0),esk15_1(esk1_2(tptp0,esk16_0)))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_5263,c_0_5264]),c_0_5265]),c_0_5266])]) ).
cnf(c_0_5271,plain,
( X1 = esk13_1(esk3_3(tptp0,X2,X3))
| ~ root_occ(X1,esk3_3(tptp0,X2,X3))
| ~ occurrence_of(esk3_3(tptp0,X2,X3),X4)
| ~ min_precedes(X2,X3,tptp0) ),
inference(spm,[status(thm)],[c_0_5267,c_0_5240]) ).
cnf(c_0_5272,plain,
( occurrence_of(esk3_3(X1,X2,X3),esk5_1(esk3_3(X1,X2,X3)))
| ~ min_precedes(X2,X3,X1) ),
inference(spm,[status(thm)],[c_0_5258,c_0_5268]) ).
cnf(c_0_5273,plain,
esk5_1(esk3_3(tptp0,esk1_2(tptp0,esk16_0),esk15_1(esk1_2(tptp0,esk16_0)))) = tptp0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_5269,c_0_5270]),c_0_5265])]) ).
cnf(c_0_5274,plain,
( esk13_1(esk3_3(tptp0,X1,X2)) = esk1_2(tptp0,esk16_0)
| ~ subactivity_occurrence(esk1_2(tptp0,esk16_0),esk3_3(tptp0,X1,X2))
| ~ occurrence_of(esk3_3(tptp0,X1,X2),X3)
| ~ min_precedes(X1,X2,tptp0) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_5271,c_0_5221]),c_0_5240]) ).
cnf(c_0_5275,plain,
( X1 = esk1_2(tptp0,esk16_0)
| ~ root_occ(X1,esk3_3(X2,esk1_2(tptp0,esk16_0),X3))
| ~ occurrence_of(esk3_3(X2,esk1_2(tptp0,esk16_0),X3),tptp0)
| ~ occurrence_of(esk3_3(X2,esk1_2(tptp0,esk16_0),X3),X4)
| ~ min_precedes(esk1_2(tptp0,esk16_0),X3,X2) ),
inference(spm,[status(thm)],[c_0_5226,c_0_5251]) ).
cnf(c_0_5276,plain,
occurrence_of(esk3_3(tptp0,esk1_2(tptp0,esk16_0),esk15_1(esk1_2(tptp0,esk16_0))),tptp0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_5272,c_0_5273]),c_0_5265])]) ).
cnf(c_0_5277,plain,
( occurrence_of(esk15_1(X1),tptp1)
| ~ occurrence_of(X2,tptp0)
| ~ root_occ(X1,X2) ),
i_0_133 ).
cnf(c_0_5278,plain,
( X1 = X2
| min_precedes(X1,X2,X3)
| ~ occurrence_of(X4,X3)
| ~ root_occ(X5,X4)
| ~ leaf_occ(X2,X4)
| ~ subactivity_occurrence(X1,X4)
| ~ min_precedes(X5,X1,X3) ),
i_0_95 ).
cnf(c_0_5279,plain,
( esk13_1(esk3_3(tptp0,esk1_2(tptp0,esk16_0),X1)) = esk1_2(tptp0,esk16_0)
| ~ occurrence_of(esk3_3(tptp0,esk1_2(tptp0,esk16_0),X1),X2)
| ~ min_precedes(esk1_2(tptp0,esk16_0),X1,tptp0) ),
inference(spm,[status(thm)],[c_0_5274,c_0_5251]) ).
cnf(c_0_5280,plain,
( ~ min_precedes(X1,X2,X3)
| ~ min_precedes(X2,X4,X3)
| ~ next_subocc(X1,X4,X3) ),
i_0_92 ).
cnf(c_0_5281,plain,
( next_subocc(esk13_1(X1),esk14_1(X1),tptp0)
| ~ occurrence_of(X1,tptp0) ),
i_0_115 ).
cnf(c_0_5282,plain,
( X1 = esk1_2(tptp0,esk16_0)
| ~ root_occ(X1,esk3_3(tptp0,esk1_2(tptp0,esk16_0),esk15_1(esk1_2(tptp0,esk16_0))))
| ~ occurrence_of(esk3_3(tptp0,esk1_2(tptp0,esk16_0),esk15_1(esk1_2(tptp0,esk16_0))),X2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_5275,c_0_5276]),c_0_5265])]) ).
cnf(c_0_5283,plain,
( occurrence_of(esk15_1(X1),tptp1)
| ~ root_occ(X1,esk4_2(esk14_1(esk16_0),tptp0)) ),
inference(spm,[status(thm)],[c_0_5277,c_0_5233]) ).
cnf(c_0_5284,plain,
( occurrence_of(esk14_1(X1),tptp3)
| ~ occurrence_of(X1,tptp0) ),
i_0_141 ).
cnf(c_0_5285,plain,
( esk15_1(esk1_2(tptp0,esk16_0)) = X1
| min_precedes(esk15_1(esk1_2(tptp0,esk16_0)),X1,tptp0)
| ~ subactivity_occurrence(esk15_1(esk1_2(tptp0,esk16_0)),X2)
| ~ leaf_occ(X1,X2)
| ~ root_occ(esk1_2(tptp0,esk16_0),X2)
| ~ occurrence_of(X2,tptp0) ),
inference(spm,[status(thm)],[c_0_5278,c_0_5265]) ).
cnf(c_0_5286,plain,
( subactivity_occurrence(X1,esk3_3(X2,X3,X1))
| ~ min_precedes(X3,X1,X2) ),
i_0_99 ).
cnf(c_0_5287,plain,
( esk13_1(esk3_3(tptp0,esk1_2(tptp0,esk16_0),X1)) = esk1_2(tptp0,esk16_0)
| ~ min_precedes(esk1_2(tptp0,esk16_0),X1,tptp0) ),
inference(spm,[status(thm)],[c_0_5279,c_0_5272]) ).
cnf(c_0_5288,plain,
( ~ occurrence_of(X1,tptp0)
| ~ min_precedes(X2,esk14_1(X1),tptp0)
| ~ min_precedes(esk13_1(X1),X2,tptp0) ),
inference(spm,[status(thm)],[c_0_5280,c_0_5281]) ).
cnf(c_0_5289,plain,
( esk13_1(esk3_3(tptp0,esk1_2(tptp0,esk16_0),esk15_1(esk1_2(tptp0,esk16_0)))) = esk1_2(tptp0,esk16_0)
| ~ occurrence_of(esk3_3(tptp0,esk1_2(tptp0,esk16_0),esk15_1(esk1_2(tptp0,esk16_0))),X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_5282,c_0_5236]),c_0_5276])]) ).
cnf(c_0_5290,plain,
( occurrence_of(esk15_1(esk1_2(tptp0,esk16_0)),tptp1)
| ~ subactivity_occurrence(esk1_2(tptp0,esk16_0),esk4_2(esk14_1(esk16_0),tptp0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_5283,c_0_5221]),c_0_5233])]) ).
cnf(c_0_5291,negated_conjecture,
( occurrence_of(esk15_1(X1),tptp1)
| ~ root_occ(X1,esk16_0) ),
inference(spm,[status(thm)],[c_0_5277,c_0_5216]) ).
cnf(c_0_5292,plain,
( activity_occurrence(esk14_1(X1))
| ~ occurrence_of(X1,tptp0) ),
inference(spm,[status(thm)],[c_0_5262,c_0_5284]) ).
cnf(c_0_5293,plain,
( esk15_1(esk1_2(tptp0,esk16_0)) = X1
| min_precedes(esk15_1(esk1_2(tptp0,esk16_0)),X1,tptp0)
| ~ leaf_occ(X1,esk3_3(X2,X3,esk15_1(esk1_2(tptp0,esk16_0))))
| ~ root_occ(esk1_2(tptp0,esk16_0),esk3_3(X2,X3,esk15_1(esk1_2(tptp0,esk16_0))))
| ~ occurrence_of(esk3_3(X2,X3,esk15_1(esk1_2(tptp0,esk16_0))),tptp0)
| ~ min_precedes(X3,esk15_1(esk1_2(tptp0,esk16_0)),X2) ),
inference(spm,[status(thm)],[c_0_5285,c_0_5286]) ).
cnf(c_0_5294,plain,
( root_occ(esk1_2(tptp0,esk16_0),esk3_3(tptp0,esk1_2(tptp0,esk16_0),X1))
| ~ min_precedes(esk1_2(tptp0,esk16_0),X1,tptp0) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_5236,c_0_5287]),c_0_5240]) ).
cnf(c_0_5295,plain,
( ~ root_occ(esk13_1(X1),esk16_0)
| ~ occurrence_of(X1,tptp0)
| ~ min_precedes(esk15_1(esk13_1(X1)),esk14_1(X1),tptp0) ),
inference(spm,[status(thm)],[c_0_5288,c_0_5247]) ).
cnf(c_0_5296,plain,
esk13_1(esk3_3(tptp0,esk1_2(tptp0,esk16_0),esk15_1(esk1_2(tptp0,esk16_0)))) = esk1_2(tptp0,esk16_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_5289,c_0_5272]),c_0_5265])]) ).
cnf(c_0_5297,plain,
occurrence_of(esk15_1(esk1_2(tptp0,esk16_0)),tptp1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_5290,c_0_5227]),c_0_5232]),c_0_5233])]) ).
cnf(c_0_5298,plain,
( activity_occurrence(esk15_1(X1))
| ~ root_occ(X1,esk16_0) ),
inference(spm,[status(thm)],[c_0_5262,c_0_5291]) ).
cnf(c_0_5299,plain,
( X1 = tptp3
| ~ occurrence_of(esk14_1(X2),X1)
| ~ occurrence_of(X2,tptp0) ),
inference(spm,[status(thm)],[c_0_5237,c_0_5284]) ).
cnf(c_0_5300,plain,
( occurrence_of(esk14_1(X1),esk5_1(esk14_1(X1)))
| ~ occurrence_of(X1,tptp0) ),
inference(spm,[status(thm)],[c_0_5258,c_0_5292]) ).
cnf(c_0_5301,plain,
( esk15_1(esk1_2(tptp0,esk16_0)) = X1
| min_precedes(esk15_1(esk1_2(tptp0,esk16_0)),X1,tptp0)
| ~ leaf_occ(X1,esk3_3(tptp0,esk1_2(tptp0,esk16_0),esk15_1(esk1_2(tptp0,esk16_0)))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_5293,c_0_5294]),c_0_5276]),c_0_5265])]) ).
cnf(c_0_5302,plain,
( leaf_occ(esk14_1(X1),X1)
| ~ occurrence_of(X1,tptp0) ),
i_0_139 ).
cnf(c_0_5303,plain,
~ min_precedes(esk15_1(esk1_2(tptp0,esk16_0)),esk14_1(esk3_3(tptp0,esk1_2(tptp0,esk16_0),esk15_1(esk1_2(tptp0,esk16_0)))),tptp0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_5295,c_0_5296]),c_0_5266]),c_0_5276])]) ).
cnf(c_0_5304,plain,
( X1 = tptp1
| ~ occurrence_of(esk15_1(esk1_2(tptp0,esk16_0)),X1) ),
inference(spm,[status(thm)],[c_0_5237,c_0_5297]) ).
cnf(c_0_5305,plain,
( occurrence_of(esk15_1(X1),esk5_1(esk15_1(X1)))
| ~ root_occ(X1,esk16_0) ),
inference(spm,[status(thm)],[c_0_5258,c_0_5298]) ).
cnf(c_0_5306,plain,
( esk5_1(esk14_1(X1)) = tptp3
| ~ occurrence_of(X1,tptp0) ),
inference(spm,[status(thm)],[c_0_5299,c_0_5300]) ).
cnf(c_0_5307,plain,
esk14_1(esk3_3(tptp0,esk1_2(tptp0,esk16_0),esk15_1(esk1_2(tptp0,esk16_0)))) = esk15_1(esk1_2(tptp0,esk16_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_5301,c_0_5302]),c_0_5276])]),c_0_5303]) ).
cnf(c_0_5308,plain,
esk5_1(esk15_1(esk1_2(tptp0,esk16_0))) = tptp1,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_5304,c_0_5305]),c_0_5266])]) ).
cnf(c_0_5309,plain,
tptp1 != tptp3,
i_0_165 ).
cnf(c_0_5310,plain,
$false,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_5306,c_0_5307]),c_0_5308]),c_0_5276])]),c_0_5309]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : PRO003+4 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n016.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 01:30:21 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 154.30/89.93 % Version : CSE_E---1.7
% 154.30/89.93 % Problem : theBenchmark.p
% 154.30/89.93 % SZS status Theorem for theBenchmark.p
% 154.30/89.93 % SZS output start CNFRefutation
% See solution above
% 155.00/90.65 % Total time : 88.875s
%------------------------------------------------------------------------------