%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : PRO010+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 08:54:11 AM UTC 2026
% Result : Theorem 165.16s 165.47s
% Output : Proof 165.40s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(sos,axiom,
! [X0,X1] :
( occurrence_of(X1,X0)
=> ( activity_occurrence(X1)
& activity(X0) ) ),
file('theBenchmark.p',sos) ).
fof(sos_01,axiom,
! [X2] :
( activity_occurrence(X2)
=> ? [X3] :
( occurrence_of(X2,X3)
& activity(X3) ) ),
file('theBenchmark.p',sos_01) ).
fof(sos_02,axiom,
! [X4,X5,X6] :
( ( occurrence_of(X4,X6)
& occurrence_of(X4,X5) )
=> X5 = X6 ),
file('theBenchmark.p',sos_02) ).
fof(sos_03,axiom,
! [X7] :
( activity(X7)
=> subactivity(X7,X7) ),
file('theBenchmark.p',sos_03) ).
fof(sos_04,axiom,
! [X8,X9] :
( earlier(X8,X9)
=> ~ earlier(X9,X8) ),
file('theBenchmark.p',sos_04) ).
fof(sos_05,axiom,
! [X10,X11,X12] :
( ( earlier(X11,X12)
& earlier(X10,X11) )
=> earlier(X10,X12) ),
file('theBenchmark.p',sos_05) ).
fof(sos_06,axiom,
! [X13,X14,X15] :
( ( earlier(X15,X14)
& earlier(X13,X14) )
=> ( X13 = X15
| earlier(X13,X15)
| earlier(X15,X13) ) ),
file('theBenchmark.p',sos_06) ).
fof(sos_07,axiom,
! [X16,X17] :
( occurrence_of(X16,X17)
=> ( arboreal(X16)
<=> atomic(X17) ) ),
file('theBenchmark.p',sos_07) ).
fof(sos_08,axiom,
! [X18] :
( legal(X18)
=> arboreal(X18) ),
file('theBenchmark.p',sos_08) ).
fof(sos_09,axiom,
! [X19,X20] :
( ( earlier(X20,X19)
& legal(X19) )
=> legal(X20) ),
file('theBenchmark.p',sos_09) ).
fof(sos_10,axiom,
! [X21,X22] :
( precedes(X21,X22)
<=> ( legal(X22)
& earlier(X21,X22) ) ),
file('theBenchmark.p',sos_10) ).
fof(sos_11,axiom,
! [X23,X24,X25] :
( min_precedes(X24,X25,X23)
=> ? [X26,X27] :
( atocc(X25,X27)
& atocc(X24,X26)
& subactivity(X27,X23)
& subactivity(X26,X23) ) ),
file('theBenchmark.p',sos_11) ).
fof(sos_12,axiom,
! [X28,X29] :
( root(X29,X28)
=> ? [X30] :
( atocc(X29,X30)
& subactivity(X30,X28) ) ),
file('theBenchmark.p',sos_12) ).
fof(sos_13,axiom,
! [X31,X32,X33] :
( min_precedes(X31,X32,X33)
=> ? [X34] :
( min_precedes(X34,X32,X33)
& root(X34,X33) ) ),
file('theBenchmark.p',sos_13) ).
fof(sos_14,axiom,
! [X35,X36,X37] :
( min_precedes(X35,X36,X37)
=> ~ root(X36,X37) ),
file('theBenchmark.p',sos_14) ).
fof(sos_15,axiom,
! [X38,X39,X40] :
( min_precedes(X38,X39,X40)
=> precedes(X38,X39) ),
file('theBenchmark.p',sos_15) ).
fof(sos_16,axiom,
! [X41,X42] :
( root(X41,X42)
=> legal(X41) ),
file('theBenchmark.p',sos_16) ).
fof(sos_17,axiom,
! [X43,X44] :
( ( legal(X43)
& atocc(X43,X44) )
=> root(X43,X44) ),
file('theBenchmark.p',sos_17) ).
fof(sos_18,axiom,
! [X45,X46,X47,X48] :
( ( precedes(X46,X47)
& min_precedes(X45,X47,X48)
& min_precedes(X45,X46,X48) )
=> min_precedes(X46,X47,X48) ),
file('theBenchmark.p',sos_18) ).
fof(sos_19,axiom,
! [X49,X50,X51] :
( min_precedes(X49,X50,X51)
=> ~ atomic(X51) ),
file('theBenchmark.p',sos_19) ).
fof(sos_20,axiom,
! [X52,X53,X54,X55] :
( ( precedes(X53,X54)
& min_precedes(X54,X52,X55)
& min_precedes(X53,X52,X55) )
=> min_precedes(X53,X54,X55) ),
file('theBenchmark.p',sos_20) ).
fof(sos_21,axiom,
! [X56,X57] :
( leaf(X56,X57)
<=> ( ~ ? [X59] : min_precedes(X56,X59,X57)
& ( ? [X58] : min_precedes(X58,X56,X57)
| root(X56,X57) ) ) ),
file('theBenchmark.p',sos_21) ).
fof(sos_22,axiom,
! [X60,X61,X62] :
( next_subocc(X60,X61,X62)
<=> ( ~ ? [X63] :
( min_precedes(X63,X61,X62)
& min_precedes(X60,X63,X62) )
& min_precedes(X60,X61,X62) ) ),
file('theBenchmark.p',sos_22) ).
fof(sos_23,axiom,
! [X64,X65] :
( atocc(X64,X65)
<=> ? [X66] :
( occurrence_of(X64,X66)
& atomic(X66)
& subactivity(X65,X66) ) ),
file('theBenchmark.p',sos_23) ).
fof(sos_24,axiom,
! [X67,X68] :
( subactivity_occurrence(X67,X68)
=> ( activity_occurrence(X68)
& activity_occurrence(X67) ) ),
file('theBenchmark.p',sos_24) ).
fof(sos_25,axiom,
! [X69,X70,X71] :
( min_precedes(X70,X71,X69)
=> ? [X72] :
( subactivity_occurrence(X71,X72)
& subactivity_occurrence(X70,X72)
& occurrence_of(X72,X69) ) ),
file('theBenchmark.p',sos_25) ).
fof(sos_26,axiom,
! [X73,X74] :
( ( ~ atomic(X73)
& root(X74,X73) )
=> ? [X75] :
( subactivity_occurrence(X74,X75)
& occurrence_of(X75,X73) ) ),
file('theBenchmark.p',sos_26) ).
fof(sos_27,axiom,
! [X76,X77] :
( ( ~ atomic(X76)
& occurrence_of(X77,X76) )
=> ? [X78] :
( subactivity_occurrence(X78,X77)
& root(X78,X76) ) ),
file('theBenchmark.p',sos_27) ).
fof(sos_28,axiom,
! [X79,X80,X81,X82] :
( ( subactivity_occurrence(X82,X80)
& subactivity_occurrence(X81,X80)
& arboreal(X82)
& arboreal(X81)
& occurrence_of(X80,X79) )
=> ( X81 = X82
| min_precedes(X82,X81,X79)
| min_precedes(X81,X82,X79) ) ),
file('theBenchmark.p',sos_28) ).
fof(sos_29,axiom,
! [X83,X84,X85,X86] :
( ( subactivity_occurrence(X84,X86)
& occurrence_of(X86,X85)
& min_precedes(X83,X84,X85) )
=> subactivity_occurrence(X83,X86) ),
file('theBenchmark.p',sos_29) ).
fof(sos_30,axiom,
! [X87,X88,X89,X90] :
( ( subactivity_occurrence(X89,X90)
& ~ atomic(X87)
& occurrence_of(X90,X88)
& occurrence_of(X89,X87) )
=> subactivity(X87,X88) ),
file('theBenchmark.p',sos_30) ).
fof(sos_31,axiom,
! [X91,X92,X93] :
( ( subactivity_occurrence(X92,X93)
& subactivity_occurrence(X91,X92) )
=> subactivity_occurrence(X91,X93) ),
file('theBenchmark.p',sos_31) ).
fof(sos_32,axiom,
! [X94,X95,X96,X97] :
( ( ~ subactivity_occurrence(X96,X97)
& subactivity(X94,X95)
& occurrence_of(X97,X95)
& occurrence_of(X96,X94) )
=> ? [X98] :
( ~ subactivity_occurrence(X98,X96)
& subactivity_occurrence(X98,X97) ) ),
file('theBenchmark.p',sos_32) ).
fof(sos_33,axiom,
! [X99,X100] :
( root_occ(X99,X100)
<=> ? [X101] :
( root(X99,X101)
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,X101) ) ),
file('theBenchmark.p',sos_33) ).
fof(sos_34,axiom,
! [X102,X103] :
( leaf_occ(X102,X103)
<=> ? [X104] :
( leaf(X102,X104)
& subactivity_occurrence(X102,X103)
& occurrence_of(X103,X104) ) ),
file('theBenchmark.p',sos_34) ).
fof(sos_35,axiom,
! [X105,X106,X107,X108] :
( ( root_occ(X106,X107)
& root_occ(X105,X107)
& occurrence_of(X107,X108) )
=> X105 = X106 ),
file('theBenchmark.p',sos_35) ).
fof(sos_36,axiom,
! [X109,X110,X111,X112] :
( ( leaf_occ(X110,X111)
& leaf_occ(X109,X111)
& ~ atomic(X112)
& occurrence_of(X111,X112) )
=> X109 = X110 ),
file('theBenchmark.p',sos_36) ).
fof(sos_37,axiom,
! [X113,X114,X115] :
( ( leaf_occ(X114,X113)
& occurrence_of(X113,X115) )
=> ~ ? [X116] : min_precedes(X114,X116,X115) ),
file('theBenchmark.p',sos_37) ).
fof(sos_38,axiom,
! [X117,X118,X119] :
( ( root_occ(X118,X117)
& occurrence_of(X117,X119) )
=> ~ ? [X120] : min_precedes(X120,X118,X119) ),
file('theBenchmark.p',sos_38) ).
fof(sos_39,axiom,
! [X121,X122,X123,X124,X125] :
( ( subactivity_occurrence(X122,X125)
& subactivity_occurrence(X123,X125)
& occurrence_of(X125,X124)
& next_subocc(X121,X123,X124)
& next_subocc(X121,X122,X124) )
=> X122 = X123 ),
file('theBenchmark.p',sos_39) ).
fof(sos_40,axiom,
! [X126,X127,X128,X129] :
( ( next_subocc(X128,X126,X129)
& next_subocc(X127,X126,X129) )
=> X127 = X128 ),
file('theBenchmark.p',sos_40) ).
fof(sos_41,axiom,
! [X130,X131,X132,X133] :
( ( X131 != X132
& root_occ(X132,X130)
& leaf_occ(X131,X130)
& occurrence_of(X130,X133) )
=> min_precedes(X132,X131,X133) ),
file('theBenchmark.p',sos_41) ).
fof(sos_42,axiom,
! [X134,X135,X136,X137] :
( ( ~ min_precedes(X137,X136,X134)
& arboreal(X136)
& root_occ(X137,X135)
& subactivity_occurrence(X136,X135)
& occurrence_of(X135,X134) )
=> X137 = X136 ),
file('theBenchmark.p',sos_42) ).
fof(sos_43,axiom,
! [X138,X139,X140,X141] :
( ( ~ min_precedes(X140,X141,X138)
& arboreal(X140)
& leaf_occ(X141,X139)
& subactivity_occurrence(X140,X139)
& occurrence_of(X139,X138) )
=> X141 = X140 ),
file('theBenchmark.p',sos_43) ).
fof(sos_44,axiom,
! [X142,X143,X144] :
( next_subocc(X142,X143,X144)
=> ( arboreal(X143)
& arboreal(X142) ) ),
file('theBenchmark.p',sos_44) ).
fof(sos_45,axiom,
! [X145,X146] :
( ( ~ atomic(X146)
& leaf(X145,X146) )
=> ? [X147] :
( leaf_occ(X145,X147)
& occurrence_of(X147,X146) ) ),
file('theBenchmark.p',sos_45) ).
fof(sos_46,axiom,
! [X148,X149,X150] :
( min_precedes(X148,X149,X150)
=> arboreal(X148) ),
file('theBenchmark.p',sos_46) ).
fof(sos_47,axiom,
! [X151,X152,X153,X154,X155] :
( ( X153 != X154
& min_precedes(X153,X155,X151)
& subactivity_occurrence(X153,X152)
& leaf_occ(X155,X152)
& root_occ(X154,X152)
& occurrence_of(X152,X151) )
=> min_precedes(X154,X153,X151) ),
file('theBenchmark.p',sos_47) ).
fof(sos_48,axiom,
! [X156,X157,X158,X159,X160] :
( ( X158 != X160
& min_precedes(X159,X158,X156)
& subactivity_occurrence(X158,X157)
& leaf_occ(X160,X157)
& root_occ(X159,X157)
& occurrence_of(X157,X156) )
=> min_precedes(X158,X160,X156) ),
file('theBenchmark.p',sos_48) ).
fof(sos_49,axiom,
! [X161] :
( occurrence_of(X161,tptp0)
=> ? [X162,X163,X164] :
( leaf_occ(X164,X161)
& next_subocc(X163,X164,tptp0)
& ( occurrence_of(X164,tptp2)
| occurrence_of(X164,tptp1) )
& next_subocc(X162,X163,tptp0)
& occurrence_of(X163,tptp4)
& root_occ(X162,X161)
& occurrence_of(X162,tptp3) ) ),
file('theBenchmark.p',sos_49) ).
fof(sos_50,axiom,
activity(tptp0),
file('theBenchmark.p',sos_50) ).
fof(sos_51,axiom,
~ atomic(tptp0),
file('theBenchmark.p',sos_51) ).
fof(sos_52,axiom,
atomic(tptp4),
file('theBenchmark.p',sos_52) ).
fof(sos_53,axiom,
atomic(tptp1),
file('theBenchmark.p',sos_53) ).
fof(sos_54,axiom,
atomic(tptp2),
file('theBenchmark.p',sos_54) ).
fof(sos_55,axiom,
atomic(tptp3),
file('theBenchmark.p',sos_55) ).
fof(sos_56,axiom,
tptp4 != tptp3,
file('theBenchmark.p',sos_56) ).
fof(sos_57,axiom,
tptp4 != tptp1,
file('theBenchmark.p',sos_57) ).
fof(sos_58,axiom,
tptp4 != tptp2,
file('theBenchmark.p',sos_58) ).
fof(sos_59,axiom,
tptp3 != tptp1,
file('theBenchmark.p',sos_59) ).
fof(sos_60,axiom,
tptp3 != tptp2,
file('theBenchmark.p',sos_60) ).
fof(sos_61,axiom,
tptp1 != tptp2,
file('theBenchmark.p',sos_61) ).
fof(goals,conjecture,
! [X165] :
( occurrence_of(X165,tptp0)
=> ? [X166,X167] :
( ( occurrence_of(X167,tptp2)
=> ~ ? [X169] :
( min_precedes(X166,X169,tptp0)
& occurrence_of(X169,tptp1) ) )
& ( occurrence_of(X167,tptp1)
=> ~ ? [X168] :
( min_precedes(X166,X168,tptp0)
& occurrence_of(X168,tptp2) ) )
& leaf_occ(X167,X165) ) ),
file('theBenchmark.p',goals) ).
fof(f_1_1,plain,
! [X0,X1] :
( ( activity_occurrence(X1)
& activity(X0) )
| ~ occurrence_of(X1,X0) ),
inference(fof_nnf,[status(thm)],[sos]) ).
fof(f_1_2,plain,
! [U_1,U_0] :
( ( activity_occurrence(U_0)
& activity(U_1) )
| ~ occurrence_of(U_0,U_1) ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
cnf(f_1_3,plain,
( activity(U_1)
| ~ occurrence_of(U_0,U_1) ),
inference(clausify,[status(thm)],[f_1_2]) ).
cnf(f_1_4,plain,
( activity_occurrence(U_0)
| ~ occurrence_of(U_0,U_1) ),
inference(clausify,[status(thm)],[f_1_2]) ).
fof(f_2_1,plain,
! [X2] :
( ? [X3] :
( occurrence_of(X2,X3)
& activity(X3) )
| ~ activity_occurrence(X2) ),
inference(fof_nnf,[status(thm)],[sos_01]) ).
fof(f_2_2,plain,
! [U_3] :
( ? [U_2] :
( occurrence_of(U_3,U_2)
& activity(U_2) )
| ~ activity_occurrence(U_3) ),
inference(variable_rename,[status(thm)],[f_2_1]) ).
fof(f_2_3,plain,
! [U_3] :
( ( occurrence_of(U_3,sK1(U_3))
& activity(sK1(U_3)) )
| ~ activity_occurrence(U_3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_2,sK1(U_3))],[f_2_2]) ).
cnf(f_2_4,plain,
( activity(sK1(U_3))
| ~ activity_occurrence(U_3) ),
inference(clausify,[status(thm)],[f_2_3]) ).
cnf(f_2_5,plain,
( occurrence_of(U_3,sK1(U_3))
| ~ activity_occurrence(U_3) ),
inference(clausify,[status(thm)],[f_2_3]) ).
fof(f_3_1,plain,
! [X4,X5,X6] :
( X5 = X6
| ~ occurrence_of(X4,X6)
| ~ occurrence_of(X4,X5) ),
inference(fof_nnf,[status(thm)],[sos_02]) ).
fof(f_3_2,plain,
! [U_6,U_5,U_4] :
( U_5 = U_4
| ~ occurrence_of(U_6,U_4)
| ~ occurrence_of(U_6,U_5) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
cnf(f_3_3,plain,
( U_5 = U_4
| ~ occurrence_of(U_6,U_4)
| ~ occurrence_of(U_6,U_5) ),
inference(clausify,[status(thm)],[f_3_2]) ).
fof(f_4_1,plain,
! [X7] :
( subactivity(X7,X7)
| ~ activity(X7) ),
inference(fof_nnf,[status(thm)],[sos_03]) ).
fof(f_4_2,plain,
! [U_7] :
( subactivity(U_7,U_7)
| ~ activity(U_7) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
cnf(f_4_3,plain,
( subactivity(U_7,U_7)
| ~ activity(U_7) ),
inference(clausify,[status(thm)],[f_4_2]) ).
fof(f_5_1,plain,
! [X8,X9] :
( ~ earlier(X9,X8)
| ~ earlier(X8,X9) ),
inference(fof_nnf,[status(thm)],[sos_04]) ).
fof(f_5_2,plain,
! [U_9,U_8] :
( ~ earlier(U_8,U_9)
| ~ earlier(U_9,U_8) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
cnf(f_5_3,plain,
( ~ earlier(U_8,U_9)
| ~ earlier(U_9,U_8) ),
inference(clausify,[status(thm)],[f_5_2]) ).
fof(f_6_1,plain,
! [X10,X11,X12] :
( earlier(X10,X12)
| ~ earlier(X11,X12)
| ~ earlier(X10,X11) ),
inference(fof_nnf,[status(thm)],[sos_05]) ).
fof(f_6_2,plain,
! [U_12,U_11,U_10] :
( earlier(U_12,U_10)
| ~ earlier(U_11,U_10)
| ~ earlier(U_12,U_11) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
cnf(f_6_3,plain,
( earlier(U_12,U_10)
| ~ earlier(U_11,U_10)
| ~ earlier(U_12,U_11) ),
inference(clausify,[status(thm)],[f_6_2]) ).
fof(f_7_1,plain,
! [X13,X14,X15] :
( X13 = X15
| earlier(X13,X15)
| earlier(X15,X13)
| ~ earlier(X15,X14)
| ~ earlier(X13,X14) ),
inference(fof_nnf,[status(thm)],[sos_06]) ).
fof(f_7_2,plain,
! [U_15,U_14,U_13] :
( U_15 = U_13
| earlier(U_15,U_13)
| earlier(U_13,U_15)
| ~ earlier(U_13,U_14)
| ~ earlier(U_15,U_14) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
cnf(f_7_3,plain,
( U_15 = U_13
| earlier(U_15,U_13)
| earlier(U_13,U_15)
| ~ earlier(U_13,U_14)
| ~ earlier(U_15,U_14) ),
inference(clausify,[status(thm)],[f_7_2]) ).
fof(f_8_1,plain,
! [X16,X17] :
( ( ( arboreal(X16)
| ~ atomic(X17) )
& ( atomic(X17)
| ~ arboreal(X16) ) )
| ~ occurrence_of(X16,X17) ),
inference(fof_nnf,[status(thm)],[sos_07]) ).
fof(f_8_2,plain,
! [U_17,U_16] :
( ( ( arboreal(U_17)
| ~ atomic(U_16) )
& ( atomic(U_16)
| ~ arboreal(U_17) ) )
| ~ occurrence_of(U_17,U_16) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
cnf(f_8_3,plain,
( atomic(U_16)
| ~ arboreal(U_17)
| ~ occurrence_of(U_17,U_16) ),
inference(clausify,[status(thm)],[f_8_2]) ).
cnf(f_8_4,plain,
( arboreal(U_17)
| ~ atomic(U_16)
| ~ occurrence_of(U_17,U_16) ),
inference(clausify,[status(thm)],[f_8_2]) ).
fof(f_9_1,plain,
! [X18] :
( arboreal(X18)
| ~ legal(X18) ),
inference(fof_nnf,[status(thm)],[sos_08]) ).
fof(f_9_2,plain,
! [U_18] :
( arboreal(U_18)
| ~ legal(U_18) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
cnf(f_9_3,plain,
( arboreal(U_18)
| ~ legal(U_18) ),
inference(clausify,[status(thm)],[f_9_2]) ).
fof(f_10_1,plain,
! [X19,X20] :
( legal(X20)
| ~ earlier(X20,X19)
| ~ legal(X19) ),
inference(fof_nnf,[status(thm)],[sos_09]) ).
fof(f_10_2,plain,
! [U_20,U_19] :
( legal(U_19)
| ~ earlier(U_19,U_20)
| ~ legal(U_20) ),
inference(variable_rename,[status(thm)],[f_10_1]) ).
cnf(f_10_3,plain,
( legal(U_19)
| ~ earlier(U_19,U_20)
| ~ legal(U_20) ),
inference(clausify,[status(thm)],[f_10_2]) ).
fof(f_11_1,plain,
! [X21,X22] :
( ( precedes(X21,X22)
| ~ legal(X22)
| ~ earlier(X21,X22) )
& ( ( legal(X22)
& earlier(X21,X22) )
| ~ precedes(X21,X22) ) ),
inference(fof_nnf,[status(thm)],[sos_10]) ).
fof(f_11_2,plain,
! [U_22,U_21] :
( ( precedes(U_22,U_21)
| ~ legal(U_21)
| ~ earlier(U_22,U_21) )
& ( ( legal(U_21)
& earlier(U_22,U_21) )
| ~ precedes(U_22,U_21) ) ),
inference(variable_rename,[status(thm)],[f_11_1]) ).
fof(f_11_3,plain,
( ! [U_26,U_24] :
( precedes(U_26,U_24)
| ~ legal(U_24)
| ~ earlier(U_26,U_24) )
& ! [U_25,U_23] :
( ( legal(U_23)
& earlier(U_25,U_23) )
| ~ precedes(U_25,U_23) ) ),
inference(miniscope,[status(thm)],[f_11_2]) ).
cnf(f_11_4,plain,
( earlier(U_25,U_23)
| ~ precedes(U_25,U_23) ),
inference(clausify,[status(thm)],[f_11_3]) ).
cnf(f_11_5,plain,
( legal(U_23)
| ~ precedes(U_25,U_23) ),
inference(clausify,[status(thm)],[f_11_3]) ).
cnf(f_11_6,plain,
( precedes(U_26,U_24)
| ~ legal(U_24)
| ~ earlier(U_26,U_24) ),
inference(clausify,[status(thm)],[f_11_3]) ).
fof(f_12_1,plain,
! [X23,X24,X25] :
( ? [X26,X27] :
( atocc(X25,X27)
& atocc(X24,X26)
& subactivity(X27,X23)
& subactivity(X26,X23) )
| ~ min_precedes(X24,X25,X23) ),
inference(fof_nnf,[status(thm)],[sos_11]) ).
fof(f_12_2,plain,
! [U_31,U_30,U_29] :
( ? [U_28,U_27] :
( atocc(U_29,U_27)
& atocc(U_30,U_28)
& subactivity(U_27,U_31)
& subactivity(U_28,U_31) )
| ~ min_precedes(U_30,U_29,U_31) ),
inference(variable_rename,[status(thm)],[f_12_1]) ).
fof(f_12_3,plain,
! [U_31,U_30,U_29] :
( ( ? [U_28] :
( atocc(U_30,U_28)
& subactivity(U_28,U_31) )
& ? [U_27] :
( atocc(U_29,U_27)
& subactivity(U_27,U_31) ) )
| ~ min_precedes(U_30,U_29,U_31) ),
inference(miniscope,[status(thm)],[f_12_2]) ).
fof(f_12_4,plain,
! [U_31,U_30,U_29] :
( ( ? [U_28] :
( atocc(U_30,U_28)
& subactivity(U_28,U_31) )
& atocc(U_29,sK2(U_31,U_30,U_29))
& subactivity(sK2(U_31,U_30,U_29),U_31) )
| ~ min_precedes(U_30,U_29,U_31) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_27,sK2(U_31,U_30,U_29))],[f_12_3]) ).
fof(f_12_5,plain,
! [U_31,U_30,U_29] :
( ( atocc(U_30,sK3(U_31,U_30,U_29))
& subactivity(sK3(U_31,U_30,U_29),U_31)
& atocc(U_29,sK2(U_31,U_30,U_29))
& subactivity(sK2(U_31,U_30,U_29),U_31) )
| ~ min_precedes(U_30,U_29,U_31) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_28,sK3(U_31,U_30,U_29))],[f_12_4]) ).
cnf(f_12_6,plain,
( subactivity(sK2(U_31,U_30,U_29),U_31)
| ~ min_precedes(U_30,U_29,U_31) ),
inference(clausify,[status(thm)],[f_12_5]) ).
cnf(f_12_7,plain,
( atocc(U_29,sK2(U_31,U_30,U_29))
| ~ min_precedes(U_30,U_29,U_31) ),
inference(clausify,[status(thm)],[f_12_5]) ).
cnf(f_12_8,plain,
( subactivity(sK3(U_31,U_30,U_29),U_31)
| ~ min_precedes(U_30,U_29,U_31) ),
inference(clausify,[status(thm)],[f_12_5]) ).
cnf(f_12_9,plain,
( atocc(U_30,sK3(U_31,U_30,U_29))
| ~ min_precedes(U_30,U_29,U_31) ),
inference(clausify,[status(thm)],[f_12_5]) ).
fof(f_13_1,plain,
! [X28,X29] :
( ? [X30] :
( atocc(X29,X30)
& subactivity(X30,X28) )
| ~ root(X29,X28) ),
inference(fof_nnf,[status(thm)],[sos_12]) ).
fof(f_13_2,plain,
! [U_34,U_33] :
( ? [U_32] :
( atocc(U_33,U_32)
& subactivity(U_32,U_34) )
| ~ root(U_33,U_34) ),
inference(variable_rename,[status(thm)],[f_13_1]) ).
fof(f_13_3,plain,
! [U_34,U_33] :
( ( atocc(U_33,sK4(U_34,U_33))
& subactivity(sK4(U_34,U_33),U_34) )
| ~ root(U_33,U_34) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_32,sK4(U_34,U_33))],[f_13_2]) ).
cnf(f_13_4,plain,
( subactivity(sK4(U_34,U_33),U_34)
| ~ root(U_33,U_34) ),
inference(clausify,[status(thm)],[f_13_3]) ).
cnf(f_13_5,plain,
( atocc(U_33,sK4(U_34,U_33))
| ~ root(U_33,U_34) ),
inference(clausify,[status(thm)],[f_13_3]) ).
fof(f_14_1,plain,
! [X31,X32,X33] :
( ? [X34] :
( min_precedes(X34,X32,X33)
& root(X34,X33) )
| ~ min_precedes(X31,X32,X33) ),
inference(fof_nnf,[status(thm)],[sos_13]) ).
fof(f_14_2,plain,
! [U_38,U_37,U_36] :
( ? [U_35] :
( min_precedes(U_35,U_37,U_36)
& root(U_35,U_36) )
| ~ min_precedes(U_38,U_37,U_36) ),
inference(variable_rename,[status(thm)],[f_14_1]) ).
fof(f_14_3,plain,
! [U_38,U_37,U_36] :
( ( min_precedes(sK5(U_38,U_37,U_36),U_37,U_36)
& root(sK5(U_38,U_37,U_36),U_36) )
| ~ min_precedes(U_38,U_37,U_36) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_35,sK5(U_38,U_37,U_36))],[f_14_2]) ).
cnf(f_14_4,plain,
( root(sK5(U_38,U_37,U_36),U_36)
| ~ min_precedes(U_38,U_37,U_36) ),
inference(clausify,[status(thm)],[f_14_3]) ).
cnf(f_14_5,plain,
( min_precedes(sK5(U_38,U_37,U_36),U_37,U_36)
| ~ min_precedes(U_38,U_37,U_36) ),
inference(clausify,[status(thm)],[f_14_3]) ).
fof(f_15_1,plain,
! [X35,X36,X37] :
( ~ root(X36,X37)
| ~ min_precedes(X35,X36,X37) ),
inference(fof_nnf,[status(thm)],[sos_14]) ).
fof(f_15_2,plain,
! [U_41,U_40,U_39] :
( ~ root(U_40,U_39)
| ~ min_precedes(U_41,U_40,U_39) ),
inference(variable_rename,[status(thm)],[f_15_1]) ).
cnf(f_15_3,plain,
( ~ root(U_40,U_39)
| ~ min_precedes(U_41,U_40,U_39) ),
inference(clausify,[status(thm)],[f_15_2]) ).
fof(f_16_1,plain,
! [X38,X39,X40] :
( precedes(X38,X39)
| ~ min_precedes(X38,X39,X40) ),
inference(fof_nnf,[status(thm)],[sos_15]) ).
fof(f_16_2,plain,
! [U_44,U_43,U_42] :
( precedes(U_44,U_43)
| ~ min_precedes(U_44,U_43,U_42) ),
inference(variable_rename,[status(thm)],[f_16_1]) ).
fof(f_16_3,plain,
! [U_44,U_43] :
( ! [U_42] : ~ min_precedes(U_44,U_43,U_42)
| precedes(U_44,U_43) ),
inference(miniscope,[status(thm)],[f_16_2]) ).
cnf(f_16_4,plain,
( ~ min_precedes(U_44,U_43,U_42)
| precedes(U_44,U_43) ),
inference(clausify,[status(thm)],[f_16_3]) ).
fof(f_17_1,plain,
! [X41,X42] :
( legal(X41)
| ~ root(X41,X42) ),
inference(fof_nnf,[status(thm)],[sos_16]) ).
fof(f_17_2,plain,
! [U_46,U_45] :
( legal(U_46)
| ~ root(U_46,U_45) ),
inference(variable_rename,[status(thm)],[f_17_1]) ).
fof(f_17_3,plain,
! [U_46] :
( ! [U_45] : ~ root(U_46,U_45)
| legal(U_46) ),
inference(miniscope,[status(thm)],[f_17_2]) ).
cnf(f_17_4,plain,
( ~ root(U_46,U_45)
| legal(U_46) ),
inference(clausify,[status(thm)],[f_17_3]) ).
fof(f_18_1,plain,
! [X43,X44] :
( root(X43,X44)
| ~ legal(X43)
| ~ atocc(X43,X44) ),
inference(fof_nnf,[status(thm)],[sos_17]) ).
fof(f_18_2,plain,
! [U_48,U_47] :
( root(U_48,U_47)
| ~ legal(U_48)
| ~ atocc(U_48,U_47) ),
inference(variable_rename,[status(thm)],[f_18_1]) ).
cnf(f_18_3,plain,
( root(U_48,U_47)
| ~ legal(U_48)
| ~ atocc(U_48,U_47) ),
inference(clausify,[status(thm)],[f_18_2]) ).
fof(f_19_1,plain,
! [X45,X46,X47,X48] :
( min_precedes(X46,X47,X48)
| ~ precedes(X46,X47)
| ~ min_precedes(X45,X47,X48)
| ~ min_precedes(X45,X46,X48) ),
inference(fof_nnf,[status(thm)],[sos_18]) ).
fof(f_19_2,plain,
! [U_52,U_51,U_50,U_49] :
( min_precedes(U_51,U_50,U_49)
| ~ precedes(U_51,U_50)
| ~ min_precedes(U_52,U_50,U_49)
| ~ min_precedes(U_52,U_51,U_49) ),
inference(variable_rename,[status(thm)],[f_19_1]) ).
cnf(f_19_3,plain,
( min_precedes(U_51,U_50,U_49)
| ~ precedes(U_51,U_50)
| ~ min_precedes(U_52,U_50,U_49)
| ~ min_precedes(U_52,U_51,U_49) ),
inference(clausify,[status(thm)],[f_19_2]) ).
fof(f_20_1,plain,
! [X49,X50,X51] :
( ~ atomic(X51)
| ~ min_precedes(X49,X50,X51) ),
inference(fof_nnf,[status(thm)],[sos_19]) ).
fof(f_20_2,plain,
! [U_55,U_54,U_53] :
( ~ atomic(U_53)
| ~ min_precedes(U_55,U_54,U_53) ),
inference(variable_rename,[status(thm)],[f_20_1]) ).
cnf(f_20_3,plain,
( ~ atomic(U_53)
| ~ min_precedes(U_55,U_54,U_53) ),
inference(clausify,[status(thm)],[f_20_2]) ).
fof(f_21_1,plain,
! [X52,X53,X54,X55] :
( min_precedes(X53,X54,X55)
| ~ precedes(X53,X54)
| ~ min_precedes(X54,X52,X55)
| ~ min_precedes(X53,X52,X55) ),
inference(fof_nnf,[status(thm)],[sos_20]) ).
fof(f_21_2,plain,
! [U_59,U_58,U_57,U_56] :
( min_precedes(U_58,U_57,U_56)
| ~ precedes(U_58,U_57)
| ~ min_precedes(U_57,U_59,U_56)
| ~ min_precedes(U_58,U_59,U_56) ),
inference(variable_rename,[status(thm)],[f_21_1]) ).
cnf(f_21_3,plain,
( min_precedes(U_58,U_57,U_56)
| ~ precedes(U_58,U_57)
| ~ min_precedes(U_57,U_59,U_56)
| ~ min_precedes(U_58,U_59,U_56) ),
inference(clausify,[status(thm)],[f_21_2]) ).
fof(f_22_1,plain,
! [X56,X57] :
( ( leaf(X56,X57)
| ? [X59] : min_precedes(X56,X59,X57)
| ( ! [X58] : ~ min_precedes(X58,X56,X57)
& ~ root(X56,X57) ) )
& ( ( ! [X59] : ~ min_precedes(X56,X59,X57)
& ( ? [X58] : min_precedes(X58,X56,X57)
| root(X56,X57) ) )
| ~ leaf(X56,X57) ) ),
inference(fof_nnf,[status(thm)],[sos_21]) ).
fof(f_22_2,plain,
! [U_65,U_64] :
( ( leaf(U_65,U_64)
| ? [U_63] : min_precedes(U_65,U_63,U_64)
| ( ! [U_62] : ~ min_precedes(U_62,U_65,U_64)
& ~ root(U_65,U_64) ) )
& ( ( ! [U_61] : ~ min_precedes(U_65,U_61,U_64)
& ( ? [U_60] : min_precedes(U_60,U_65,U_64)
| root(U_65,U_64) ) )
| ~ leaf(U_65,U_64) ) ),
inference(variable_rename,[status(thm)],[f_22_1]) ).
fof(f_22_3,plain,
( ! [U_69,U_67] :
( leaf(U_69,U_67)
| ? [U_63] : min_precedes(U_69,U_63,U_67)
| ( ! [U_62] : ~ min_precedes(U_62,U_69,U_67)
& ~ root(U_69,U_67) ) )
& ! [U_68,U_66] :
( ( ! [U_61] : ~ min_precedes(U_68,U_61,U_66)
& ( ? [U_60] : min_precedes(U_60,U_68,U_66)
| root(U_68,U_66) ) )
| ~ leaf(U_68,U_66) ) ),
inference(miniscope,[status(thm)],[f_22_2]) ).
fof(f_22_4,plain,
( ! [U_69,U_67] :
( leaf(U_69,U_67)
| ? [U_63] : min_precedes(U_69,U_63,U_67)
| ( ! [U_62] : ~ min_precedes(U_62,U_69,U_67)
& ~ root(U_69,U_67) ) )
& ! [U_68,U_66] :
( ( ! [U_61] : ~ min_precedes(U_68,U_61,U_66)
& ( min_precedes(sK6(U_68,U_66),U_68,U_66)
| root(U_68,U_66) ) )
| ~ leaf(U_68,U_66) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_60,sK6(U_68,U_66))],[f_22_3]) ).
fof(f_22_5,plain,
( ! [U_69,U_67] :
( leaf(U_69,U_67)
| min_precedes(U_69,sK7(U_69,U_67),U_67)
| ( ! [U_62] : ~ min_precedes(U_62,U_69,U_67)
& ~ root(U_69,U_67) ) )
& ! [U_68,U_66] :
( ( ! [U_61] : ~ min_precedes(U_68,U_61,U_66)
& ( min_precedes(sK6(U_68,U_66),U_68,U_66)
| root(U_68,U_66) ) )
| ~ leaf(U_68,U_66) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_63,sK7(U_69,U_67))],[f_22_4]) ).
cnf(f_22_6,plain,
( min_precedes(sK6(U_68,U_66),U_68,U_66)
| root(U_68,U_66)
| ~ leaf(U_68,U_66) ),
inference(clausify,[status(thm)],[f_22_5]) ).
cnf(f_22_7,plain,
( ~ min_precedes(U_68,U_61,U_66)
| ~ leaf(U_68,U_66) ),
inference(clausify,[status(thm)],[f_22_5]) ).
cnf(f_22_8,plain,
( ~ root(U_69,U_67)
| min_precedes(U_69,sK7(U_69,U_67),U_67)
| leaf(U_69,U_67) ),
inference(clausify,[status(thm)],[f_22_5]) ).
cnf(f_22_9,plain,
( ~ min_precedes(U_62,U_69,U_67)
| min_precedes(U_69,sK7(U_69,U_67),U_67)
| leaf(U_69,U_67) ),
inference(clausify,[status(thm)],[f_22_5]) ).
fof(f_23_1,plain,
! [X60,X61,X62] :
( ( next_subocc(X60,X61,X62)
| ? [X63] :
( min_precedes(X63,X61,X62)
& min_precedes(X60,X63,X62) )
| ~ min_precedes(X60,X61,X62) )
& ( ( ! [X63] :
( ~ min_precedes(X63,X61,X62)
| ~ min_precedes(X60,X63,X62) )
& min_precedes(X60,X61,X62) )
| ~ next_subocc(X60,X61,X62) ) ),
inference(fof_nnf,[status(thm)],[sos_22]) ).
fof(f_23_2,plain,
! [U_74,U_73,U_72] :
( ( next_subocc(U_74,U_73,U_72)
| ? [U_71] :
( min_precedes(U_71,U_73,U_72)
& min_precedes(U_74,U_71,U_72) )
| ~ min_precedes(U_74,U_73,U_72) )
& ( ( ! [U_70] :
( ~ min_precedes(U_70,U_73,U_72)
| ~ min_precedes(U_74,U_70,U_72) )
& min_precedes(U_74,U_73,U_72) )
| ~ next_subocc(U_74,U_73,U_72) ) ),
inference(variable_rename,[status(thm)],[f_23_1]) ).
fof(f_23_3,plain,
( ! [U_80,U_78,U_76] :
( next_subocc(U_80,U_78,U_76)
| ? [U_71] :
( min_precedes(U_71,U_78,U_76)
& min_precedes(U_80,U_71,U_76) )
| ~ min_precedes(U_80,U_78,U_76) )
& ! [U_79,U_77,U_75] :
( ( ! [U_70] :
( ~ min_precedes(U_70,U_77,U_75)
| ~ min_precedes(U_79,U_70,U_75) )
& min_precedes(U_79,U_77,U_75) )
| ~ next_subocc(U_79,U_77,U_75) ) ),
inference(miniscope,[status(thm)],[f_23_2]) ).
fof(f_23_4,plain,
( ! [U_80,U_78,U_76] :
( next_subocc(U_80,U_78,U_76)
| ( min_precedes(sK8(U_80,U_78,U_76),U_78,U_76)
& min_precedes(U_80,sK8(U_80,U_78,U_76),U_76) )
| ~ min_precedes(U_80,U_78,U_76) )
& ! [U_79,U_77,U_75] :
( ( ! [U_70] :
( ~ min_precedes(U_70,U_77,U_75)
| ~ min_precedes(U_79,U_70,U_75) )
& min_precedes(U_79,U_77,U_75) )
| ~ next_subocc(U_79,U_77,U_75) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_71,sK8(U_80,U_78,U_76))],[f_23_3]) ).
cnf(f_23_5,plain,
( min_precedes(U_79,U_77,U_75)
| ~ next_subocc(U_79,U_77,U_75) ),
inference(clausify,[status(thm)],[f_23_4]) ).
cnf(f_23_6,plain,
( ~ min_precedes(U_70,U_77,U_75)
| ~ min_precedes(U_79,U_70,U_75)
| ~ next_subocc(U_79,U_77,U_75) ),
inference(clausify,[status(thm)],[f_23_4]) ).
cnf(f_23_7,plain,
( min_precedes(U_80,sK8(U_80,U_78,U_76),U_76)
| ~ min_precedes(U_80,U_78,U_76)
| next_subocc(U_80,U_78,U_76) ),
inference(clausify,[status(thm)],[f_23_4]) ).
cnf(f_23_8,plain,
( min_precedes(sK8(U_80,U_78,U_76),U_78,U_76)
| ~ min_precedes(U_80,U_78,U_76)
| next_subocc(U_80,U_78,U_76) ),
inference(clausify,[status(thm)],[f_23_4]) ).
fof(f_24_1,plain,
! [X64,X65] :
( ( atocc(X64,X65)
| ! [X66] :
( ~ occurrence_of(X64,X66)
| ~ atomic(X66)
| ~ subactivity(X65,X66) ) )
& ( ? [X66] :
( occurrence_of(X64,X66)
& atomic(X66)
& subactivity(X65,X66) )
| ~ atocc(X64,X65) ) ),
inference(fof_nnf,[status(thm)],[sos_23]) ).
fof(f_24_2,plain,
! [U_84,U_83] :
( ( atocc(U_84,U_83)
| ! [U_82] :
( ~ occurrence_of(U_84,U_82)
| ~ atomic(U_82)
| ~ subactivity(U_83,U_82) ) )
& ( ? [U_81] :
( occurrence_of(U_84,U_81)
& atomic(U_81)
& subactivity(U_83,U_81) )
| ~ atocc(U_84,U_83) ) ),
inference(variable_rename,[status(thm)],[f_24_1]) ).
fof(f_24_3,plain,
( ! [U_88,U_86] :
( atocc(U_88,U_86)
| ! [U_82] :
( ~ occurrence_of(U_88,U_82)
| ~ atomic(U_82)
| ~ subactivity(U_86,U_82) ) )
& ! [U_87,U_85] :
( ? [U_81] :
( occurrence_of(U_87,U_81)
& atomic(U_81)
& subactivity(U_85,U_81) )
| ~ atocc(U_87,U_85) ) ),
inference(miniscope,[status(thm)],[f_24_2]) ).
fof(f_24_4,plain,
( ! [U_88,U_86] :
( atocc(U_88,U_86)
| ! [U_82] :
( ~ occurrence_of(U_88,U_82)
| ~ atomic(U_82)
| ~ subactivity(U_86,U_82) ) )
& ! [U_87,U_85] :
( ( occurrence_of(U_87,sK9(U_87,U_85))
& atomic(sK9(U_87,U_85))
& subactivity(U_85,sK9(U_87,U_85)) )
| ~ atocc(U_87,U_85) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_81,sK9(U_87,U_85))],[f_24_3]) ).
cnf(f_24_5,plain,
( subactivity(U_85,sK9(U_87,U_85))
| ~ atocc(U_87,U_85) ),
inference(clausify,[status(thm)],[f_24_4]) ).
cnf(f_24_6,plain,
( atomic(sK9(U_87,U_85))
| ~ atocc(U_87,U_85) ),
inference(clausify,[status(thm)],[f_24_4]) ).
cnf(f_24_7,plain,
( occurrence_of(U_87,sK9(U_87,U_85))
| ~ atocc(U_87,U_85) ),
inference(clausify,[status(thm)],[f_24_4]) ).
cnf(f_24_8,plain,
( atocc(U_88,U_86)
| ~ occurrence_of(U_88,U_82)
| ~ atomic(U_82)
| ~ subactivity(U_86,U_82) ),
inference(clausify,[status(thm)],[f_24_4]) ).
fof(f_25_1,plain,
! [X67,X68] :
( ( activity_occurrence(X68)
& activity_occurrence(X67) )
| ~ subactivity_occurrence(X67,X68) ),
inference(fof_nnf,[status(thm)],[sos_24]) ).
fof(f_25_2,plain,
! [U_90,U_89] :
( ( activity_occurrence(U_89)
& activity_occurrence(U_90) )
| ~ subactivity_occurrence(U_90,U_89) ),
inference(variable_rename,[status(thm)],[f_25_1]) ).
cnf(f_25_3,plain,
( activity_occurrence(U_90)
| ~ subactivity_occurrence(U_90,U_89) ),
inference(clausify,[status(thm)],[f_25_2]) ).
cnf(f_25_4,plain,
( activity_occurrence(U_89)
| ~ subactivity_occurrence(U_90,U_89) ),
inference(clausify,[status(thm)],[f_25_2]) ).
fof(f_26_1,plain,
! [X69,X70,X71] :
( ? [X72] :
( subactivity_occurrence(X71,X72)
& subactivity_occurrence(X70,X72)
& occurrence_of(X72,X69) )
| ~ min_precedes(X70,X71,X69) ),
inference(fof_nnf,[status(thm)],[sos_25]) ).
fof(f_26_2,plain,
! [U_94,U_93,U_92] :
( ? [U_91] :
( subactivity_occurrence(U_92,U_91)
& subactivity_occurrence(U_93,U_91)
& occurrence_of(U_91,U_94) )
| ~ min_precedes(U_93,U_92,U_94) ),
inference(variable_rename,[status(thm)],[f_26_1]) ).
fof(f_26_3,plain,
! [U_94,U_93,U_92] :
( ( subactivity_occurrence(U_92,sK10(U_94,U_93,U_92))
& subactivity_occurrence(U_93,sK10(U_94,U_93,U_92))
& occurrence_of(sK10(U_94,U_93,U_92),U_94) )
| ~ min_precedes(U_93,U_92,U_94) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_91,sK10(U_94,U_93,U_92))],[f_26_2]) ).
cnf(f_26_4,plain,
( occurrence_of(sK10(U_94,U_93,U_92),U_94)
| ~ min_precedes(U_93,U_92,U_94) ),
inference(clausify,[status(thm)],[f_26_3]) ).
cnf(f_26_5,plain,
( subactivity_occurrence(U_93,sK10(U_94,U_93,U_92))
| ~ min_precedes(U_93,U_92,U_94) ),
inference(clausify,[status(thm)],[f_26_3]) ).
cnf(f_26_6,plain,
( subactivity_occurrence(U_92,sK10(U_94,U_93,U_92))
| ~ min_precedes(U_93,U_92,U_94) ),
inference(clausify,[status(thm)],[f_26_3]) ).
fof(f_27_1,plain,
! [X73,X74] :
( ? [X75] :
( subactivity_occurrence(X74,X75)
& occurrence_of(X75,X73) )
| atomic(X73)
| ~ root(X74,X73) ),
inference(fof_nnf,[status(thm)],[sos_26]) ).
fof(f_27_2,plain,
! [U_97,U_96] :
( ? [U_95] :
( subactivity_occurrence(U_96,U_95)
& occurrence_of(U_95,U_97) )
| atomic(U_97)
| ~ root(U_96,U_97) ),
inference(variable_rename,[status(thm)],[f_27_1]) ).
fof(f_27_3,plain,
! [U_97,U_96] :
( ( subactivity_occurrence(U_96,sK11(U_97,U_96))
& occurrence_of(sK11(U_97,U_96),U_97) )
| atomic(U_97)
| ~ root(U_96,U_97) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_95,sK11(U_97,U_96))],[f_27_2]) ).
cnf(f_27_4,plain,
( occurrence_of(sK11(U_97,U_96),U_97)
| atomic(U_97)
| ~ root(U_96,U_97) ),
inference(clausify,[status(thm)],[f_27_3]) ).
cnf(f_27_5,plain,
( subactivity_occurrence(U_96,sK11(U_97,U_96))
| atomic(U_97)
| ~ root(U_96,U_97) ),
inference(clausify,[status(thm)],[f_27_3]) ).
fof(f_28_1,plain,
! [X76,X77] :
( ? [X78] :
( subactivity_occurrence(X78,X77)
& root(X78,X76) )
| atomic(X76)
| ~ occurrence_of(X77,X76) ),
inference(fof_nnf,[status(thm)],[sos_27]) ).
fof(f_28_2,plain,
! [U_100,U_99] :
( ? [U_98] :
( subactivity_occurrence(U_98,U_99)
& root(U_98,U_100) )
| atomic(U_100)
| ~ occurrence_of(U_99,U_100) ),
inference(variable_rename,[status(thm)],[f_28_1]) ).
fof(f_28_3,plain,
! [U_100,U_99] :
( ( subactivity_occurrence(sK12(U_100,U_99),U_99)
& root(sK12(U_100,U_99),U_100) )
| atomic(U_100)
| ~ occurrence_of(U_99,U_100) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(U_98,sK12(U_100,U_99))],[f_28_2]) ).
cnf(f_28_4,plain,
( root(sK12(U_100,U_99),U_100)
| atomic(U_100)
| ~ occurrence_of(U_99,U_100) ),
inference(clausify,[status(thm)],[f_28_3]) ).
cnf(f_28_5,plain,
( subactivity_occurrence(sK12(U_100,U_99),U_99)
| atomic(U_100)
| ~ occurrence_of(U_99,U_100) ),
inference(clausify,[status(thm)],[f_28_3]) ).
fof(f_29_1,plain,
! [X79,X80,X81,X82] :
( X81 = X82
| min_precedes(X82,X81,X79)
| min_precedes(X81,X82,X79)
| ~ subactivity_occurrence(X82,X80)
| ~ subactivity_occurrence(X81,X80)
| ~ arboreal(X82)
| ~ arboreal(X81)
| ~ occurrence_of(X80,X79) ),
inference(fof_nnf,[status(thm)],[sos_28]) ).
fof(f_29_2,plain,
! [U_104,U_103,U_102,U_101] :
( U_102 = U_101
| min_precedes(U_101,U_102,U_104)
| min_precedes(U_102,U_101,U_104)
| ~ subactivity_occurrence(U_101,U_103)
| ~ subactivity_occurrence(U_102,U_103)
| ~ arboreal(U_101)
| ~ arboreal(U_102)
| ~ occurrence_of(U_103,U_104) ),
inference(variable_rename,[status(thm)],[f_29_1]) ).
cnf(f_29_3,plain,
( U_102 = U_101
| min_precedes(U_101,U_102,U_104)
| min_precedes(U_102,U_101,U_104)
| ~ subactivity_occurrence(U_101,U_103)
| ~ subactivity_occurrence(U_102,U_103)
| ~ arboreal(U_101)
| ~ arboreal(U_102)
| ~ occurrence_of(U_103,U_104) ),
inference(clausify,[status(thm)],[f_29_2]) ).
fof(f_30_1,plain,
! [X83,X84,X85,X86] :
( subactivity_occurrence(X83,X86)
| ~ subactivity_occurrence(X84,X86)
| ~ occurrence_of(X86,X85)
| ~ min_precedes(X83,X84,X85) ),
inference(fof_nnf,[status(thm)],[sos_29]) ).
fof(f_30_2,plain,
! [U_108,U_107,U_106,U_105] :
( subactivity_occurrence(U_108,U_105)
| ~ subactivity_occurrence(U_107,U_105)
| ~ occurrence_of(U_105,U_106)
| ~ min_precedes(U_108,U_107,U_106) ),
inference(variable_rename,[status(thm)],[f_30_1]) ).
cnf(f_30_3,plain,
( subactivity_occurrence(U_108,U_105)
| ~ subactivity_occurrence(U_107,U_105)
| ~ occurrence_of(U_105,U_106)
| ~ min_precedes(U_108,U_107,U_106) ),
inference(clausify,[status(thm)],[f_30_2]) ).
fof(f_31_1,plain,
! [X87,X88,X89,X90] :
( subactivity(X87,X88)
| ~ subactivity_occurrence(X89,X90)
| atomic(X87)
| ~ occurrence_of(X90,X88)
| ~ occurrence_of(X89,X87) ),
inference(fof_nnf,[status(thm)],[sos_30]) ).
fof(f_31_2,plain,
! [U_112,U_111,U_110,U_109] :
( subactivity(U_112,U_111)
| ~ subactivity_occurrence(U_110,U_109)
| atomic(U_112)
| ~ occurrence_of(U_109,U_111)
| ~ occurrence_of(U_110,U_112) ),
inference(variable_rename,[status(thm)],[f_31_1]) ).
fof(f_31_3,plain,
! [U_112,U_111] :
( ! [U_110] :
( ! [U_109] :
( ~ subactivity_occurrence(U_110,U_109)
| ~ occurrence_of(U_109,U_111) )
| ~ occurrence_of(U_110,U_112) )
| atomic(U_112)
| subactivity(U_112,U_111) ),
inference(miniscope,[status(thm)],[f_31_2]) ).
cnf(f_31_4,plain,
( ~ subactivity_occurrence(U_110,U_109)
| ~ occurrence_of(U_109,U_111)
| ~ occurrence_of(U_110,U_112)
| atomic(U_112)
| subactivity(U_112,U_111) ),
inference(clausify,[status(thm)],[f_31_3]) ).
fof(f_32_1,plain,
! [X91,X92,X93] :
( subactivity_occurrence(X91,X93)
| ~ subactivity_occurrence(X92,X93)
| ~ subactivity_occurrence(X91,X92) ),
inference(fof_nnf,[status(thm)],[sos_31]) ).
fof(f_32_2,plain,
! [U_115,U_114,U_113] :
( subactivity_occurrence(U_115,U_113)
| ~ subactivity_occurrence(U_114,U_113)
| ~ subactivity_occurrence(U_115,U_114) ),
inference(variable_rename,[status(thm)],[f_32_1]) ).
cnf(f_32_3,plain,
( subactivity_occurrence(U_115,U_113)
| ~ subactivity_occurrence(U_114,U_113)
| ~ subactivity_occurrence(U_115,U_114) ),
inference(clausify,[status(thm)],[f_32_2]) ).
fof(f_33_1,plain,
! [X94,X95,X96,X97] :
( ? [X98] :
( ~ subactivity_occurrence(X98,X96)
& subactivity_occurrence(X98,X97) )
| subactivity_occurrence(X96,X97)
| ~ subactivity(X94,X95)
| ~ occurrence_of(X97,X95)
| ~ occurrence_of(X96,X94) ),
inference(fof_nnf,[status(thm)],[sos_32]) ).
fof(f_33_2,plain,
! [U_120,U_119,U_118,U_117] :
( ? [U_116] :
( ~ subactivity_occurrence(U_116,U_118)
& subactivity_occurrence(U_116,U_117) )
| subactivity_occurrence(U_118,U_117)
| ~ subactivity(U_120,U_119)
| ~ occurrence_of(U_117,U_119)
| ~ occurrence_of(U_118,U_120) ),
inference(variable_rename,[status(thm)],[f_33_1]) ).
fof(f_33_3,plain,
! [U_120,U_119,U_118,U_117] :
( ( ~ subactivity_occurrence(sK13(U_120,U_119,U_118,U_117),U_118)
& subactivity_occurrence(sK13(U_120,U_119,U_118,U_117),U_117) )
| subactivity_occurrence(U_118,U_117)
| ~ subactivity(U_120,U_119)
| ~ occurrence_of(U_117,U_119)
| ~ occurrence_of(U_118,U_120) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(U_116,sK13(U_120,U_119,U_118,U_117))],[f_33_2]) ).
cnf(f_33_4,plain,
( subactivity_occurrence(sK13(U_120,U_119,U_118,U_117),U_117)
| subactivity_occurrence(U_118,U_117)
| ~ subactivity(U_120,U_119)
| ~ occurrence_of(U_117,U_119)
| ~ occurrence_of(U_118,U_120) ),
inference(clausify,[status(thm)],[f_33_3]) ).
cnf(f_33_5,plain,
( ~ subactivity_occurrence(sK13(U_120,U_119,U_118,U_117),U_118)
| subactivity_occurrence(U_118,U_117)
| ~ subactivity(U_120,U_119)
| ~ occurrence_of(U_117,U_119)
| ~ occurrence_of(U_118,U_120) ),
inference(clausify,[status(thm)],[f_33_3]) ).
fof(f_34_1,plain,
! [X99,X100] :
( ( root_occ(X99,X100)
| ! [X101] :
( ~ root(X99,X101)
| ~ subactivity_occurrence(X99,X100)
| ~ occurrence_of(X100,X101) ) )
& ( ? [X101] :
( root(X99,X101)
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,X101) )
| ~ root_occ(X99,X100) ) ),
inference(fof_nnf,[status(thm)],[sos_33]) ).
fof(f_34_2,plain,
! [U_124,U_123] :
( ( root_occ(U_124,U_123)
| ! [U_122] :
( ~ root(U_124,U_122)
| ~ subactivity_occurrence(U_124,U_123)
| ~ occurrence_of(U_123,U_122) ) )
& ( ? [U_121] :
( root(U_124,U_121)
& subactivity_occurrence(U_124,U_123)
& occurrence_of(U_123,U_121) )
| ~ root_occ(U_124,U_123) ) ),
inference(variable_rename,[status(thm)],[f_34_1]) ).
fof(f_34_3,plain,
( ! [U_128,U_126] :
( root_occ(U_128,U_126)
| ! [U_122] :
( ~ root(U_128,U_122)
| ~ occurrence_of(U_126,U_122) )
| ~ subactivity_occurrence(U_128,U_126) )
& ! [U_127,U_125] :
( ( ? [U_121] :
( root(U_127,U_121)
& occurrence_of(U_125,U_121) )
& subactivity_occurrence(U_127,U_125) )
| ~ root_occ(U_127,U_125) ) ),
inference(miniscope,[status(thm)],[f_34_2]) ).
fof(f_34_4,plain,
( ! [U_128,U_126] :
( root_occ(U_128,U_126)
| ! [U_122] :
( ~ root(U_128,U_122)
| ~ occurrence_of(U_126,U_122) )
| ~ subactivity_occurrence(U_128,U_126) )
& ! [U_127,U_125] :
( ( root(U_127,sK14(U_127,U_125))
& occurrence_of(U_125,sK14(U_127,U_125))
& subactivity_occurrence(U_127,U_125) )
| ~ root_occ(U_127,U_125) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_121,sK14(U_127,U_125))],[f_34_3]) ).
cnf(f_34_5,plain,
( subactivity_occurrence(U_127,U_125)
| ~ root_occ(U_127,U_125) ),
inference(clausify,[status(thm)],[f_34_4]) ).
cnf(f_34_6,plain,
( occurrence_of(U_125,sK14(U_127,U_125))
| ~ root_occ(U_127,U_125) ),
inference(clausify,[status(thm)],[f_34_4]) ).
cnf(f_34_7,plain,
( root(U_127,sK14(U_127,U_125))
| ~ root_occ(U_127,U_125) ),
inference(clausify,[status(thm)],[f_34_4]) ).
cnf(f_34_8,plain,
( root_occ(U_128,U_126)
| ~ root(U_128,U_122)
| ~ occurrence_of(U_126,U_122)
| ~ subactivity_occurrence(U_128,U_126) ),
inference(clausify,[status(thm)],[f_34_4]) ).
fof(f_35_1,plain,
! [X102,X103] :
( ( leaf_occ(X102,X103)
| ! [X104] :
( ~ leaf(X102,X104)
| ~ subactivity_occurrence(X102,X103)
| ~ occurrence_of(X103,X104) ) )
& ( ? [X104] :
( leaf(X102,X104)
& subactivity_occurrence(X102,X103)
& occurrence_of(X103,X104) )
| ~ leaf_occ(X102,X103) ) ),
inference(fof_nnf,[status(thm)],[sos_34]) ).
fof(f_35_2,plain,
! [U_132,U_131] :
( ( leaf_occ(U_132,U_131)
| ! [U_130] :
( ~ leaf(U_132,U_130)
| ~ subactivity_occurrence(U_132,U_131)
| ~ occurrence_of(U_131,U_130) ) )
& ( ? [U_129] :
( leaf(U_132,U_129)
& subactivity_occurrence(U_132,U_131)
& occurrence_of(U_131,U_129) )
| ~ leaf_occ(U_132,U_131) ) ),
inference(variable_rename,[status(thm)],[f_35_1]) ).
fof(f_35_3,plain,
( ! [U_136,U_134] :
( leaf_occ(U_136,U_134)
| ! [U_130] :
( ~ leaf(U_136,U_130)
| ~ occurrence_of(U_134,U_130) )
| ~ subactivity_occurrence(U_136,U_134) )
& ! [U_135,U_133] :
( ( ? [U_129] :
( leaf(U_135,U_129)
& occurrence_of(U_133,U_129) )
& subactivity_occurrence(U_135,U_133) )
| ~ leaf_occ(U_135,U_133) ) ),
inference(miniscope,[status(thm)],[f_35_2]) ).
fof(f_35_4,plain,
( ! [U_136,U_134] :
( leaf_occ(U_136,U_134)
| ! [U_130] :
( ~ leaf(U_136,U_130)
| ~ occurrence_of(U_134,U_130) )
| ~ subactivity_occurrence(U_136,U_134) )
& ! [U_135,U_133] :
( ( leaf(U_135,sK15(U_135,U_133))
& occurrence_of(U_133,sK15(U_135,U_133))
& subactivity_occurrence(U_135,U_133) )
| ~ leaf_occ(U_135,U_133) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(U_129,sK15(U_135,U_133))],[f_35_3]) ).
cnf(f_35_5,plain,
( subactivity_occurrence(U_135,U_133)
| ~ leaf_occ(U_135,U_133) ),
inference(clausify,[status(thm)],[f_35_4]) ).
cnf(f_35_6,plain,
( occurrence_of(U_133,sK15(U_135,U_133))
| ~ leaf_occ(U_135,U_133) ),
inference(clausify,[status(thm)],[f_35_4]) ).
cnf(f_35_7,plain,
( leaf(U_135,sK15(U_135,U_133))
| ~ leaf_occ(U_135,U_133) ),
inference(clausify,[status(thm)],[f_35_4]) ).
cnf(f_35_8,plain,
( leaf_occ(U_136,U_134)
| ~ leaf(U_136,U_130)
| ~ occurrence_of(U_134,U_130)
| ~ subactivity_occurrence(U_136,U_134) ),
inference(clausify,[status(thm)],[f_35_4]) ).
fof(f_36_1,plain,
! [X105,X106,X107,X108] :
( X105 = X106
| ~ root_occ(X106,X107)
| ~ root_occ(X105,X107)
| ~ occurrence_of(X107,X108) ),
inference(fof_nnf,[status(thm)],[sos_35]) ).
fof(f_36_2,plain,
! [U_140,U_139,U_138,U_137] :
( U_140 = U_139
| ~ root_occ(U_139,U_138)
| ~ root_occ(U_140,U_138)
| ~ occurrence_of(U_138,U_137) ),
inference(variable_rename,[status(thm)],[f_36_1]) ).
fof(f_36_3,plain,
! [U_140,U_139] :
( ! [U_138] :
( ! [U_137] : ~ occurrence_of(U_138,U_137)
| ~ root_occ(U_139,U_138)
| ~ root_occ(U_140,U_138) )
| U_140 = U_139 ),
inference(miniscope,[status(thm)],[f_36_2]) ).
cnf(f_36_4,plain,
( ~ occurrence_of(U_138,U_137)
| ~ root_occ(U_139,U_138)
| ~ root_occ(U_140,U_138)
| U_140 = U_139 ),
inference(clausify,[status(thm)],[f_36_3]) ).
fof(f_37_1,plain,
! [X109,X110,X111,X112] :
( X109 = X110
| ~ leaf_occ(X110,X111)
| ~ leaf_occ(X109,X111)
| atomic(X112)
| ~ occurrence_of(X111,X112) ),
inference(fof_nnf,[status(thm)],[sos_36]) ).
fof(f_37_2,plain,
! [U_144,U_143,U_142,U_141] :
( U_144 = U_143
| ~ leaf_occ(U_143,U_142)
| ~ leaf_occ(U_144,U_142)
| atomic(U_141)
| ~ occurrence_of(U_142,U_141) ),
inference(variable_rename,[status(thm)],[f_37_1]) ).
fof(f_37_3,plain,
! [U_144,U_143] :
( ! [U_142] :
( ! [U_141] :
( atomic(U_141)
| ~ occurrence_of(U_142,U_141) )
| ~ leaf_occ(U_143,U_142)
| ~ leaf_occ(U_144,U_142) )
| U_144 = U_143 ),
inference(miniscope,[status(thm)],[f_37_2]) ).
cnf(f_37_4,plain,
( atomic(U_141)
| ~ occurrence_of(U_142,U_141)
| ~ leaf_occ(U_143,U_142)
| ~ leaf_occ(U_144,U_142)
| U_144 = U_143 ),
inference(clausify,[status(thm)],[f_37_3]) ).
fof(f_38_1,plain,
! [X113,X114,X115] :
( ! [X116] : ~ min_precedes(X114,X116,X115)
| ~ leaf_occ(X114,X113)
| ~ occurrence_of(X113,X115) ),
inference(fof_nnf,[status(thm)],[sos_37]) ).
fof(f_38_2,plain,
! [U_148,U_147,U_146] :
( ! [U_145] : ~ min_precedes(U_147,U_145,U_146)
| ~ leaf_occ(U_147,U_148)
| ~ occurrence_of(U_148,U_146) ),
inference(variable_rename,[status(thm)],[f_38_1]) ).
cnf(f_38_3,plain,
( ~ min_precedes(U_147,U_145,U_146)
| ~ leaf_occ(U_147,U_148)
| ~ occurrence_of(U_148,U_146) ),
inference(clausify,[status(thm)],[f_38_2]) ).
fof(f_39_1,plain,
! [X117,X118,X119] :
( ! [X120] : ~ min_precedes(X120,X118,X119)
| ~ root_occ(X118,X117)
| ~ occurrence_of(X117,X119) ),
inference(fof_nnf,[status(thm)],[sos_38]) ).
fof(f_39_2,plain,
! [U_152,U_151,U_150] :
( ! [U_149] : ~ min_precedes(U_149,U_151,U_150)
| ~ root_occ(U_151,U_152)
| ~ occurrence_of(U_152,U_150) ),
inference(variable_rename,[status(thm)],[f_39_1]) ).
cnf(f_39_3,plain,
( ~ min_precedes(U_149,U_151,U_150)
| ~ root_occ(U_151,U_152)
| ~ occurrence_of(U_152,U_150) ),
inference(clausify,[status(thm)],[f_39_2]) ).
fof(f_40_1,plain,
! [X121,X122,X123,X124,X125] :
( X122 = X123
| ~ subactivity_occurrence(X122,X125)
| ~ subactivity_occurrence(X123,X125)
| ~ occurrence_of(X125,X124)
| ~ next_subocc(X121,X123,X124)
| ~ next_subocc(X121,X122,X124) ),
inference(fof_nnf,[status(thm)],[sos_39]) ).
fof(f_40_2,plain,
! [U_157,U_156,U_155,U_154,U_153] :
( U_156 = U_155
| ~ subactivity_occurrence(U_156,U_153)
| ~ subactivity_occurrence(U_155,U_153)
| ~ occurrence_of(U_153,U_154)
| ~ next_subocc(U_157,U_155,U_154)
| ~ next_subocc(U_157,U_156,U_154) ),
inference(variable_rename,[status(thm)],[f_40_1]) ).
fof(f_40_3,plain,
! [U_157,U_156,U_155] :
( ! [U_154] :
( ! [U_153] :
( ~ subactivity_occurrence(U_156,U_153)
| ~ subactivity_occurrence(U_155,U_153)
| ~ occurrence_of(U_153,U_154) )
| ~ next_subocc(U_157,U_155,U_154)
| ~ next_subocc(U_157,U_156,U_154) )
| U_156 = U_155 ),
inference(miniscope,[status(thm)],[f_40_2]) ).
cnf(f_40_4,plain,
( ~ subactivity_occurrence(U_156,U_153)
| ~ subactivity_occurrence(U_155,U_153)
| ~ occurrence_of(U_153,U_154)
| ~ next_subocc(U_157,U_155,U_154)
| ~ next_subocc(U_157,U_156,U_154)
| U_156 = U_155 ),
inference(clausify,[status(thm)],[f_40_3]) ).
fof(f_41_1,plain,
! [X126,X127,X128,X129] :
( X127 = X128
| ~ next_subocc(X128,X126,X129)
| ~ next_subocc(X127,X126,X129) ),
inference(fof_nnf,[status(thm)],[sos_40]) ).
fof(f_41_2,plain,
! [U_161,U_160,U_159,U_158] :
( U_160 = U_159
| ~ next_subocc(U_159,U_161,U_158)
| ~ next_subocc(U_160,U_161,U_158) ),
inference(variable_rename,[status(thm)],[f_41_1]) ).
fof(f_41_3,plain,
! [U_161,U_160,U_159] :
( ! [U_158] :
( ~ next_subocc(U_159,U_161,U_158)
| ~ next_subocc(U_160,U_161,U_158) )
| U_160 = U_159 ),
inference(miniscope,[status(thm)],[f_41_2]) ).
cnf(f_41_4,plain,
( ~ next_subocc(U_159,U_161,U_158)
| ~ next_subocc(U_160,U_161,U_158)
| U_160 = U_159 ),
inference(clausify,[status(thm)],[f_41_3]) ).
fof(f_42_1,plain,
! [X130,X131,X132,X133] :
( min_precedes(X132,X131,X133)
| X131 = X132
| ~ root_occ(X132,X130)
| ~ leaf_occ(X131,X130)
| ~ occurrence_of(X130,X133) ),
inference(fof_nnf,[status(thm)],[sos_41]) ).
fof(f_42_2,plain,
! [U_165,U_164,U_163,U_162] :
( min_precedes(U_163,U_164,U_162)
| U_164 = U_163
| ~ root_occ(U_163,U_165)
| ~ leaf_occ(U_164,U_165)
| ~ occurrence_of(U_165,U_162) ),
inference(variable_rename,[status(thm)],[f_42_1]) ).
cnf(f_42_3,plain,
( min_precedes(U_163,U_164,U_162)
| U_164 = U_163
| ~ root_occ(U_163,U_165)
| ~ leaf_occ(U_164,U_165)
| ~ occurrence_of(U_165,U_162) ),
inference(clausify,[status(thm)],[f_42_2]) ).
fof(f_43_1,plain,
! [X134,X135,X136,X137] :
( X137 = X136
| min_precedes(X137,X136,X134)
| ~ arboreal(X136)
| ~ root_occ(X137,X135)
| ~ subactivity_occurrence(X136,X135)
| ~ occurrence_of(X135,X134) ),
inference(fof_nnf,[status(thm)],[sos_42]) ).
fof(f_43_2,plain,
! [U_169,U_168,U_167,U_166] :
( U_166 = U_167
| min_precedes(U_166,U_167,U_169)
| ~ arboreal(U_167)
| ~ root_occ(U_166,U_168)
| ~ subactivity_occurrence(U_167,U_168)
| ~ occurrence_of(U_168,U_169) ),
inference(variable_rename,[status(thm)],[f_43_1]) ).
cnf(f_43_3,plain,
( U_166 = U_167
| min_precedes(U_166,U_167,U_169)
| ~ arboreal(U_167)
| ~ root_occ(U_166,U_168)
| ~ subactivity_occurrence(U_167,U_168)
| ~ occurrence_of(U_168,U_169) ),
inference(clausify,[status(thm)],[f_43_2]) ).
fof(f_44_1,plain,
! [X138,X139,X140,X141] :
( X141 = X140
| min_precedes(X140,X141,X138)
| ~ arboreal(X140)
| ~ leaf_occ(X141,X139)
| ~ subactivity_occurrence(X140,X139)
| ~ occurrence_of(X139,X138) ),
inference(fof_nnf,[status(thm)],[sos_43]) ).
fof(f_44_2,plain,
! [U_173,U_172,U_171,U_170] :
( U_170 = U_171
| min_precedes(U_171,U_170,U_173)
| ~ arboreal(U_171)
| ~ leaf_occ(U_170,U_172)
| ~ subactivity_occurrence(U_171,U_172)
| ~ occurrence_of(U_172,U_173) ),
inference(variable_rename,[status(thm)],[f_44_1]) ).
cnf(f_44_3,plain,
( U_170 = U_171
| min_precedes(U_171,U_170,U_173)
| ~ arboreal(U_171)
| ~ leaf_occ(U_170,U_172)
| ~ subactivity_occurrence(U_171,U_172)
| ~ occurrence_of(U_172,U_173) ),
inference(clausify,[status(thm)],[f_44_2]) ).
fof(f_45_1,plain,
! [X142,X143,X144] :
( ( arboreal(X143)
& arboreal(X142) )
| ~ next_subocc(X142,X143,X144) ),
inference(fof_nnf,[status(thm)],[sos_44]) ).
fof(f_45_2,plain,
! [U_176,U_175,U_174] :
( ( arboreal(U_175)
& arboreal(U_176) )
| ~ next_subocc(U_176,U_175,U_174) ),
inference(variable_rename,[status(thm)],[f_45_1]) ).
fof(f_45_3,plain,
! [U_176,U_175] :
( ! [U_174] : ~ next_subocc(U_176,U_175,U_174)
| ( arboreal(U_175)
& arboreal(U_176) ) ),
inference(miniscope,[status(thm)],[f_45_2]) ).
cnf(f_45_4,plain,
( arboreal(U_176)
| ~ next_subocc(U_176,U_175,U_174) ),
inference(clausify,[status(thm)],[f_45_3]) ).
cnf(f_45_5,plain,
( arboreal(U_175)
| ~ next_subocc(U_176,U_175,U_174) ),
inference(clausify,[status(thm)],[f_45_3]) ).
fof(f_46_1,plain,
! [X145,X146] :
( ? [X147] :
( leaf_occ(X145,X147)
& occurrence_of(X147,X146) )
| atomic(X146)
| ~ leaf(X145,X146) ),
inference(fof_nnf,[status(thm)],[sos_45]) ).
fof(f_46_2,plain,
! [U_179,U_178] :
( ? [U_177] :
( leaf_occ(U_179,U_177)
& occurrence_of(U_177,U_178) )
| atomic(U_178)
| ~ leaf(U_179,U_178) ),
inference(variable_rename,[status(thm)],[f_46_1]) ).
fof(f_46_3,plain,
! [U_179,U_178] :
( ( leaf_occ(U_179,sK16(U_179,U_178))
& occurrence_of(sK16(U_179,U_178),U_178) )
| atomic(U_178)
| ~ leaf(U_179,U_178) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(U_177,sK16(U_179,U_178))],[f_46_2]) ).
cnf(f_46_4,plain,
( occurrence_of(sK16(U_179,U_178),U_178)
| atomic(U_178)
| ~ leaf(U_179,U_178) ),
inference(clausify,[status(thm)],[f_46_3]) ).
cnf(f_46_5,plain,
( leaf_occ(U_179,sK16(U_179,U_178))
| atomic(U_178)
| ~ leaf(U_179,U_178) ),
inference(clausify,[status(thm)],[f_46_3]) ).
fof(f_47_1,plain,
! [X148,X149,X150] :
( arboreal(X148)
| ~ min_precedes(X148,X149,X150) ),
inference(fof_nnf,[status(thm)],[sos_46]) ).
fof(f_47_2,plain,
! [U_182,U_181,U_180] :
( arboreal(U_182)
| ~ min_precedes(U_182,U_181,U_180) ),
inference(variable_rename,[status(thm)],[f_47_1]) ).
fof(f_47_3,plain,
! [U_182] :
( ! [U_181,U_180] : ~ min_precedes(U_182,U_181,U_180)
| arboreal(U_182) ),
inference(miniscope,[status(thm)],[f_47_2]) ).
cnf(f_47_4,plain,
( ~ min_precedes(U_182,U_181,U_180)
| arboreal(U_182) ),
inference(clausify,[status(thm)],[f_47_3]) ).
fof(f_48_1,plain,
! [X151,X152,X153,X154,X155] :
( min_precedes(X154,X153,X151)
| X153 = X154
| ~ min_precedes(X153,X155,X151)
| ~ subactivity_occurrence(X153,X152)
| ~ leaf_occ(X155,X152)
| ~ root_occ(X154,X152)
| ~ occurrence_of(X152,X151) ),
inference(fof_nnf,[status(thm)],[sos_47]) ).
fof(f_48_2,plain,
! [U_187,U_186,U_185,U_184,U_183] :
( min_precedes(U_184,U_185,U_187)
| U_185 = U_184
| ~ min_precedes(U_185,U_183,U_187)
| ~ subactivity_occurrence(U_185,U_186)
| ~ leaf_occ(U_183,U_186)
| ~ root_occ(U_184,U_186)
| ~ occurrence_of(U_186,U_187) ),
inference(variable_rename,[status(thm)],[f_48_1]) ).
fof(f_48_3,plain,
! [U_187,U_186,U_185,U_184] :
( ! [U_183] :
( ~ min_precedes(U_185,U_183,U_187)
| ~ leaf_occ(U_183,U_186) )
| U_185 = U_184
| ~ subactivity_occurrence(U_185,U_186)
| ~ root_occ(U_184,U_186)
| ~ occurrence_of(U_186,U_187)
| min_precedes(U_184,U_185,U_187) ),
inference(miniscope,[status(thm)],[f_48_2]) ).
cnf(f_48_4,plain,
( ~ min_precedes(U_185,U_183,U_187)
| ~ leaf_occ(U_183,U_186)
| U_185 = U_184
| ~ subactivity_occurrence(U_185,U_186)
| ~ root_occ(U_184,U_186)
| ~ occurrence_of(U_186,U_187)
| min_precedes(U_184,U_185,U_187) ),
inference(clausify,[status(thm)],[f_48_3]) ).
fof(f_49_1,plain,
! [X156,X157,X158,X159,X160] :
( min_precedes(X158,X160,X156)
| X158 = X160
| ~ min_precedes(X159,X158,X156)
| ~ subactivity_occurrence(X158,X157)
| ~ leaf_occ(X160,X157)
| ~ root_occ(X159,X157)
| ~ occurrence_of(X157,X156) ),
inference(fof_nnf,[status(thm)],[sos_48]) ).
fof(f_49_2,plain,
! [U_192,U_191,U_190,U_189,U_188] :
( min_precedes(U_190,U_188,U_192)
| U_190 = U_188
| ~ min_precedes(U_189,U_190,U_192)
| ~ subactivity_occurrence(U_190,U_191)
| ~ leaf_occ(U_188,U_191)
| ~ root_occ(U_189,U_191)
| ~ occurrence_of(U_191,U_192) ),
inference(variable_rename,[status(thm)],[f_49_1]) ).
cnf(f_49_3,plain,
( min_precedes(U_190,U_188,U_192)
| U_190 = U_188
| ~ min_precedes(U_189,U_190,U_192)
| ~ subactivity_occurrence(U_190,U_191)
| ~ leaf_occ(U_188,U_191)
| ~ root_occ(U_189,U_191)
| ~ occurrence_of(U_191,U_192) ),
inference(clausify,[status(thm)],[f_49_2]) ).
fof(f_50_1,plain,
! [X161] :
( ? [X162,X163,X164] :
( leaf_occ(X164,X161)
& next_subocc(X163,X164,tptp0)
& ( occurrence_of(X164,tptp2)
| occurrence_of(X164,tptp1) )
& next_subocc(X162,X163,tptp0)
& occurrence_of(X163,tptp4)
& root_occ(X162,X161)
& occurrence_of(X162,tptp3) )
| ~ occurrence_of(X161,tptp0) ),
inference(fof_nnf,[status(thm)],[sos_49]) ).
fof(f_50_2,plain,
! [U_196] :
( ? [U_195,U_194,U_193] :
( leaf_occ(U_193,U_196)
& next_subocc(U_194,U_193,tptp0)
& ( occurrence_of(U_193,tptp2)
| occurrence_of(U_193,tptp1) )
& next_subocc(U_195,U_194,tptp0)
& occurrence_of(U_194,tptp4)
& root_occ(U_195,U_196)
& occurrence_of(U_195,tptp3) )
| ~ occurrence_of(U_196,tptp0) ),
inference(variable_rename,[status(thm)],[f_50_1]) ).
fof(f_50_3,plain,
! [U_196] :
( ? [U_195] :
( ? [U_194] :
( ? [U_193] :
( leaf_occ(U_193,U_196)
& next_subocc(U_194,U_193,tptp0)
& ( occurrence_of(U_193,tptp2)
| occurrence_of(U_193,tptp1) ) )
& next_subocc(U_195,U_194,tptp0)
& occurrence_of(U_194,tptp4) )
& root_occ(U_195,U_196)
& occurrence_of(U_195,tptp3) )
| ~ occurrence_of(U_196,tptp0) ),
inference(miniscope,[status(thm)],[f_50_2]) ).
fof(f_50_4,plain,
! [U_196] :
( ( ? [U_194] :
( ? [U_193] :
( leaf_occ(U_193,U_196)
& next_subocc(U_194,U_193,tptp0)
& ( occurrence_of(U_193,tptp2)
| occurrence_of(U_193,tptp1) ) )
& next_subocc(sK17(U_196),U_194,tptp0)
& occurrence_of(U_194,tptp4) )
& root_occ(sK17(U_196),U_196)
& occurrence_of(sK17(U_196),tptp3) )
| ~ occurrence_of(U_196,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(U_195,sK17(U_196))],[f_50_3]) ).
fof(f_50_5,plain,
! [U_196] :
( ( ? [U_193] :
( leaf_occ(U_193,U_196)
& next_subocc(sK18(U_196),U_193,tptp0)
& ( occurrence_of(U_193,tptp2)
| occurrence_of(U_193,tptp1) ) )
& next_subocc(sK17(U_196),sK18(U_196),tptp0)
& occurrence_of(sK18(U_196),tptp4)
& root_occ(sK17(U_196),U_196)
& occurrence_of(sK17(U_196),tptp3) )
| ~ occurrence_of(U_196,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(U_194,sK18(U_196))],[f_50_4]) ).
fof(f_50_6,plain,
! [U_196] :
( ( leaf_occ(sK19(U_196),U_196)
& next_subocc(sK18(U_196),sK19(U_196),tptp0)
& ( occurrence_of(sK19(U_196),tptp2)
| occurrence_of(sK19(U_196),tptp1) )
& next_subocc(sK17(U_196),sK18(U_196),tptp0)
& occurrence_of(sK18(U_196),tptp4)
& root_occ(sK17(U_196),U_196)
& occurrence_of(sK17(U_196),tptp3) )
| ~ occurrence_of(U_196,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(U_193,sK19(U_196))],[f_50_5]) ).
cnf(f_50_7,plain,
( occurrence_of(sK17(U_196),tptp3)
| ~ occurrence_of(U_196,tptp0) ),
inference(clausify,[status(thm)],[f_50_6]) ).
cnf(f_50_8,plain,
( root_occ(sK17(U_196),U_196)
| ~ occurrence_of(U_196,tptp0) ),
inference(clausify,[status(thm)],[f_50_6]) ).
cnf(f_50_9,plain,
( occurrence_of(sK18(U_196),tptp4)
| ~ occurrence_of(U_196,tptp0) ),
inference(clausify,[status(thm)],[f_50_6]) ).
cnf(f_50_10,plain,
( next_subocc(sK17(U_196),sK18(U_196),tptp0)
| ~ occurrence_of(U_196,tptp0) ),
inference(clausify,[status(thm)],[f_50_6]) ).
cnf(f_50_11,plain,
( occurrence_of(sK19(U_196),tptp2)
| occurrence_of(sK19(U_196),tptp1)
| ~ occurrence_of(U_196,tptp0) ),
inference(clausify,[status(thm)],[f_50_6]) ).
cnf(f_50_12,plain,
( next_subocc(sK18(U_196),sK19(U_196),tptp0)
| ~ occurrence_of(U_196,tptp0) ),
inference(clausify,[status(thm)],[f_50_6]) ).
cnf(f_50_13,plain,
( leaf_occ(sK19(U_196),U_196)
| ~ occurrence_of(U_196,tptp0) ),
inference(clausify,[status(thm)],[f_50_6]) ).
fof(f_51_1,plain,
activity(tptp0),
inference(fof_nnf,[status(thm)],[sos_50]) ).
cnf(f_51_2,plain,
activity(tptp0),
inference(clausify,[status(thm)],[f_51_1]) ).
fof(f_52_1,plain,
~ atomic(tptp0),
inference(fof_nnf,[status(thm)],[sos_51]) ).
cnf(f_52_2,plain,
~ atomic(tptp0),
inference(clausify,[status(thm)],[f_52_1]) ).
fof(f_53_1,plain,
atomic(tptp4),
inference(fof_nnf,[status(thm)],[sos_52]) ).
cnf(f_53_2,plain,
atomic(tptp4),
inference(clausify,[status(thm)],[f_53_1]) ).
fof(f_54_1,plain,
atomic(tptp1),
inference(fof_nnf,[status(thm)],[sos_53]) ).
cnf(f_54_2,plain,
atomic(tptp1),
inference(clausify,[status(thm)],[f_54_1]) ).
fof(f_55_1,plain,
atomic(tptp2),
inference(fof_nnf,[status(thm)],[sos_54]) ).
cnf(f_55_2,plain,
atomic(tptp2),
inference(clausify,[status(thm)],[f_55_1]) ).
fof(f_56_1,plain,
atomic(tptp3),
inference(fof_nnf,[status(thm)],[sos_55]) ).
cnf(f_56_2,plain,
atomic(tptp3),
inference(clausify,[status(thm)],[f_56_1]) ).
fof(f_57_1,plain,
tptp4 != tptp3,
inference(fof_nnf,[status(thm)],[sos_56]) ).
cnf(f_57_2,plain,
tptp4 != tptp3,
inference(clausify,[status(thm)],[f_57_1]) ).
fof(f_58_1,plain,
tptp4 != tptp1,
inference(fof_nnf,[status(thm)],[sos_57]) ).
cnf(f_58_2,plain,
tptp4 != tptp1,
inference(clausify,[status(thm)],[f_58_1]) ).
fof(f_59_1,plain,
tptp4 != tptp2,
inference(fof_nnf,[status(thm)],[sos_58]) ).
cnf(f_59_2,plain,
tptp4 != tptp2,
inference(clausify,[status(thm)],[f_59_1]) ).
fof(f_60_1,plain,
tptp3 != tptp1,
inference(fof_nnf,[status(thm)],[sos_59]) ).
cnf(f_60_2,plain,
tptp3 != tptp1,
inference(clausify,[status(thm)],[f_60_1]) ).
fof(f_61_1,plain,
tptp3 != tptp2,
inference(fof_nnf,[status(thm)],[sos_60]) ).
cnf(f_61_2,plain,
tptp3 != tptp2,
inference(clausify,[status(thm)],[f_61_1]) ).
fof(f_62_1,plain,
tptp1 != tptp2,
inference(fof_nnf,[status(thm)],[sos_61]) ).
cnf(f_62_2,plain,
tptp1 != tptp2,
inference(clausify,[status(thm)],[f_62_1]) ).
fof(f_63_1,negated_conjecture,
~ ! [X165] :
( occurrence_of(X165,tptp0)
=> ? [X166,X167] :
( ( occurrence_of(X167,tptp2)
=> ~ ? [X169] :
( min_precedes(X166,X169,tptp0)
& occurrence_of(X169,tptp1) ) )
& ( occurrence_of(X167,tptp1)
=> ~ ? [X168] :
( min_precedes(X166,X168,tptp0)
& occurrence_of(X168,tptp2) ) )
& leaf_occ(X167,X165) ) ),
inference(negate,[status(cth)],[goals]) ).
fof(f_63_2,negated_conjecture,
? [X165] :
( ! [X166,X167] :
( ( ? [X169] :
( min_precedes(X166,X169,tptp0)
& occurrence_of(X169,tptp1) )
& occurrence_of(X167,tptp2) )
| ( ? [X168] :
( min_precedes(X166,X168,tptp0)
& occurrence_of(X168,tptp2) )
& occurrence_of(X167,tptp1) )
| ~ leaf_occ(X167,X165) )
& occurrence_of(X165,tptp0) ),
inference(fof_nnf,[status(thm)],[f_63_1]) ).
fof(f_63_3,negated_conjecture,
? [U_201] :
( ! [U_200,U_199] :
( ( ? [U_198] :
( min_precedes(U_200,U_198,tptp0)
& occurrence_of(U_198,tptp1) )
& occurrence_of(U_199,tptp2) )
| ( ? [U_197] :
( min_precedes(U_200,U_197,tptp0)
& occurrence_of(U_197,tptp2) )
& occurrence_of(U_199,tptp1) )
| ~ leaf_occ(U_199,U_201) )
& occurrence_of(U_201,tptp0) ),
inference(variable_rename,[status(thm)],[f_63_2]) ).
fof(f_63_4,negated_conjecture,
( ! [U_200,U_199] :
( ( ? [U_198] :
( min_precedes(U_200,U_198,tptp0)
& occurrence_of(U_198,tptp1) )
& occurrence_of(U_199,tptp2) )
| ( ? [U_197] :
( min_precedes(U_200,U_197,tptp0)
& occurrence_of(U_197,tptp2) )
& occurrence_of(U_199,tptp1) )
| ~ leaf_occ(U_199,sK20) )
& occurrence_of(sK20,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(U_201,sK20)],[f_63_3]) ).
fof(f_63_5,negated_conjecture,
( ! [U_200,U_199] :
( ( ? [U_198] :
( min_precedes(U_200,U_198,tptp0)
& occurrence_of(U_198,tptp1) )
& occurrence_of(U_199,tptp2) )
| ( min_precedes(U_200,sK21(U_200,U_199),tptp0)
& occurrence_of(sK21(U_200,U_199),tptp2)
& occurrence_of(U_199,tptp1) )
| ~ leaf_occ(U_199,sK20) )
& occurrence_of(sK20,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21]),skolemize(U_197,sK21(U_200,U_199))],[f_63_4]) ).
fof(f_63_6,negated_conjecture,
( ! [U_200,U_199] :
( ( min_precedes(U_200,sK22(U_200,U_199),tptp0)
& occurrence_of(sK22(U_200,U_199),tptp1)
& occurrence_of(U_199,tptp2) )
| ( min_precedes(U_200,sK21(U_200,U_199),tptp0)
& occurrence_of(sK21(U_200,U_199),tptp2)
& occurrence_of(U_199,tptp1) )
| ~ leaf_occ(U_199,sK20) )
& occurrence_of(sK20,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(U_198,sK22(U_200,U_199))],[f_63_5]) ).
cnf(f_63_7,negated_conjecture,
occurrence_of(sK20,tptp0),
inference(clausify,[status(thm)],[f_63_6]) ).
cnf(f_63_8,negated_conjecture,
( occurrence_of(U_199,tptp2)
| occurrence_of(U_199,tptp1)
| ~ leaf_occ(U_199,sK20) ),
inference(clausify,[status(thm)],[f_63_6]) ).
cnf(f_63_9,negated_conjecture,
( occurrence_of(sK22(U_200,U_199),tptp1)
| occurrence_of(U_199,tptp1)
| ~ leaf_occ(U_199,sK20) ),
inference(clausify,[status(thm)],[f_63_6]) ).
cnf(f_63_10,negated_conjecture,
( min_precedes(U_200,sK22(U_200,U_199),tptp0)
| occurrence_of(U_199,tptp1)
| ~ leaf_occ(U_199,sK20) ),
inference(clausify,[status(thm)],[f_63_6]) ).
cnf(f_63_11,negated_conjecture,
( occurrence_of(sK21(U_200,U_199),tptp2)
| occurrence_of(U_199,tptp2)
| ~ leaf_occ(U_199,sK20) ),
inference(clausify,[status(thm)],[f_63_6]) ).
cnf(f_63_12,negated_conjecture,
( min_precedes(U_200,sK21(U_200,U_199),tptp0)
| occurrence_of(U_199,tptp2)
| ~ leaf_occ(U_199,sK20) ),
inference(clausify,[status(thm)],[f_63_6]) ).
cnf(f_63_13,negated_conjecture,
( occurrence_of(sK22(U_200,U_199),tptp1)
| occurrence_of(sK21(U_200,U_199),tptp2)
| ~ leaf_occ(U_199,sK20) ),
inference(clausify,[status(thm)],[f_63_6]) ).
cnf(f_63_14,negated_conjecture,
( min_precedes(U_200,sK22(U_200,U_199),tptp0)
| occurrence_of(sK21(U_200,U_199),tptp2)
| ~ leaf_occ(U_199,sK20) ),
inference(clausify,[status(thm)],[f_63_6]) ).
cnf(f_63_15,negated_conjecture,
( occurrence_of(sK22(U_200,U_199),tptp1)
| min_precedes(U_200,sK21(U_200,U_199),tptp0)
| ~ leaf_occ(U_199,sK20) ),
inference(clausify,[status(thm)],[f_63_6]) ).
cnf(f_63_16,negated_conjecture,
( min_precedes(U_200,sK22(U_200,U_199),tptp0)
| min_precedes(U_200,sK21(U_200,U_199),tptp0)
| ~ leaf_occ(U_199,sK20) ),
inference(clausify,[status(thm)],[f_63_6]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( sK1(Eq_x_0) = sK1(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( sK2(Eq_x_0,Eq_x_1,Eq_x_2) = sK2(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( sK3(Eq_x_0,Eq_x_1,Eq_x_2) = sK3(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( sK4(Eq_x_0,Eq_x_1) = sK4(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( sK5(Eq_x_0,Eq_x_1,Eq_x_2) = sK5(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( sK6(Eq_x_0,Eq_x_1) = sK6(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,axiom,
( sK7(Eq_x_0,Eq_x_1) = sK7(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_11,axiom,
( sK8(Eq_x_0,Eq_x_1,Eq_x_2) = sK8(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_12,axiom,
( sK9(Eq_x_0,Eq_x_1) = sK9(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_13,axiom,
( sK10(Eq_x_0,Eq_x_1,Eq_x_2) = sK10(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_14,axiom,
( sK11(Eq_x_0,Eq_x_1) = sK11(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_15,axiom,
( sK12(Eq_x_0,Eq_x_1) = sK12(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_16,axiom,
( sK13(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = sK13(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_17,axiom,
( sK14(Eq_x_0,Eq_x_1) = sK14(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_18,axiom,
( sK15(Eq_x_0,Eq_x_1) = sK15(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_19,axiom,
( sK16(Eq_x_0,Eq_x_1) = sK16(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_20,axiom,
( sK17(Eq_x_0) = sK17(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_21,axiom,
( sK18(Eq_x_0) = sK18(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_22,axiom,
( sK19(Eq_x_0) = sK19(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_23,axiom,
( sK21(Eq_x_0,Eq_x_1) = sK21(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_24,axiom,
( sK22(Eq_x_0,Eq_x_1) = sK22(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_25,axiom,
( occurrence_of(Eq_y_0,Eq_y_1)
| ~ occurrence_of(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_26,axiom,
( activity(Eq_y_0)
| ~ activity(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_27,axiom,
( activity_occurrence(Eq_y_0)
| ~ activity_occurrence(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_28,axiom,
( subactivity(Eq_y_0,Eq_y_1)
| ~ subactivity(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_29,axiom,
( earlier(Eq_y_0,Eq_y_1)
| ~ earlier(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_30,axiom,
( arboreal(Eq_y_0)
| ~ arboreal(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_31,axiom,
( atomic(Eq_y_0)
| ~ atomic(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_32,axiom,
( legal(Eq_y_0)
| ~ legal(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_33,axiom,
( precedes(Eq_y_0,Eq_y_1)
| ~ precedes(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_34,axiom,
( min_precedes(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ min_precedes(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_35,axiom,
( atocc(Eq_y_0,Eq_y_1)
| ~ atocc(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_36,axiom,
( root(Eq_y_0,Eq_y_1)
| ~ root(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_37,axiom,
( leaf(Eq_y_0,Eq_y_1)
| ~ leaf(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_38,axiom,
( next_subocc(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ next_subocc(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_39,axiom,
( subactivity_occurrence(Eq_y_0,Eq_y_1)
| ~ subactivity_occurrence(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_40,axiom,
( root_occ(Eq_y_0,Eq_y_1)
| ~ root_occ(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_41,axiom,
( leaf_occ(Eq_y_0,Eq_y_1)
| ~ leaf_occ(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO010+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n010.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Sat Sep 19 19:52:15 UTC 2026
% 0.08/0.35 % CPUTime :
% 165.16/165.47 % SZS status Theorem for theBenchmark
% 165.16/165.47 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------