%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : PRO010+2 : 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 : n009.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 167.32s 167.70s
% Output : Proof 168.34s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(sos,axiom,
! [X0,X1,X2,X3] :
( ( min_precedes(X1,X2,X3)
& min_precedes(X0,X1,X3) )
=> min_precedes(X0,X2,X3) ),
file('theBenchmark.p',sos) ).
fof(sos_01,axiom,
! [X4,X5,X6] :
( ( earlier(X5,X6)
& earlier(X4,X5) )
=> earlier(X4,X6) ),
file('theBenchmark.p',sos_01) ).
fof(sos_02,axiom,
! [X7,X8,X9,X10] :
( ( root_occ(X8,X9)
& root_occ(X7,X9)
& occurrence_of(X9,X10) )
=> X7 = X8 ),
file('theBenchmark.p',sos_02) ).
fof(sos_03,axiom,
! [X11,X12,X13,X14] :
( ( leaf_occ(X12,X13)
& leaf_occ(X11,X13)
& ~ atomic(X14)
& occurrence_of(X13,X14) )
=> X11 = X12 ),
file('theBenchmark.p',sos_03) ).
fof(sos_04,axiom,
! [X15,X16,X17] :
( next_subocc(X15,X16,X17)
<=> ( ~ ? [X18] :
( min_precedes(X18,X16,X17)
& min_precedes(X15,X18,X17) )
& min_precedes(X15,X16,X17) ) ),
file('theBenchmark.p',sos_04) ).
fof(sos_05,axiom,
! [X19,X20,X21] :
( next_subocc(X19,X20,X21)
=> ( arboreal(X20)
& arboreal(X19) ) ),
file('theBenchmark.p',sos_05) ).
fof(sos_06,axiom,
! [X22,X23,X24] :
( min_precedes(X22,X23,X24)
=> precedes(X22,X23) ),
file('theBenchmark.p',sos_06) ).
fof(sos_07,axiom,
! [X25,X26,X27] :
( min_precedes(X25,X26,X27)
=> ~ root(X26,X27) ),
file('theBenchmark.p',sos_07) ).
fof(sos_08,axiom,
! [X28,X29] :
( precedes(X28,X29)
<=> ( legal(X29)
& earlier(X28,X29) ) ),
file('theBenchmark.p',sos_08) ).
fof(sos_09,axiom,
! [X30,X31] :
( earlier(X30,X31)
=> ~ earlier(X31,X30) ),
file('theBenchmark.p',sos_09) ).
fof(sos_10,axiom,
! [X32,X33] :
( root_occ(X32,X33)
<=> ? [X34] :
( root(X32,X34)
& subactivity_occurrence(X32,X33)
& occurrence_of(X33,X34) ) ),
file('theBenchmark.p',sos_10) ).
fof(sos_11,axiom,
! [X35,X36] :
( leaf_occ(X35,X36)
<=> ? [X37] :
( leaf(X35,X37)
& subactivity_occurrence(X35,X36)
& occurrence_of(X36,X37) ) ),
file('theBenchmark.p',sos_11) ).
fof(sos_12,axiom,
! [X38,X39] :
( root(X38,X39)
=> legal(X38) ),
file('theBenchmark.p',sos_12) ).
fof(sos_13,axiom,
! [X40,X41] :
( occurrence_of(X40,X41)
=> ( arboreal(X40)
<=> atomic(X41) ) ),
file('theBenchmark.p',sos_13) ).
fof(sos_14,axiom,
! [X42,X43] :
( leaf(X42,X43)
<=> ( ~ ? [X45] : min_precedes(X42,X45,X43)
& ( ? [X44] : min_precedes(X44,X42,X43)
| root(X42,X43) ) ) ),
file('theBenchmark.p',sos_14) ).
fof(sos_15,axiom,
! [X46,X47] :
( atocc(X46,X47)
<=> ? [X48] :
( occurrence_of(X46,X48)
& atomic(X48)
& subactivity(X47,X48) ) ),
file('theBenchmark.p',sos_15) ).
fof(sos_16,axiom,
! [X49,X50] :
( ( legal(X49)
& atocc(X49,X50) )
=> root(X49,X50) ),
file('theBenchmark.p',sos_16) ).
fof(sos_17,axiom,
! [X51] :
( legal(X51)
=> arboreal(X51) ),
file('theBenchmark.p',sos_17) ).
fof(sos_18,axiom,
! [X52] :
( activity_occurrence(X52)
=> ? [X53] :
( occurrence_of(X52,X53)
& activity(X53) ) ),
file('theBenchmark.p',sos_18) ).
fof(sos_19,axiom,
! [X54,X55] :
( subactivity_occurrence(X54,X55)
=> ( activity_occurrence(X55)
& activity_occurrence(X54) ) ),
file('theBenchmark.p',sos_19) ).
fof(sos_20,axiom,
! [X56,X57,X58] :
( ( root_occ(X57,X56)
& occurrence_of(X56,X58) )
=> ~ ? [X59] : min_precedes(X59,X57,X58) ),
file('theBenchmark.p',sos_20) ).
fof(sos_21,axiom,
! [X60,X61,X62] :
( ( leaf_occ(X61,X60)
& occurrence_of(X60,X62) )
=> ~ ? [X63] : min_precedes(X61,X63,X62) ),
file('theBenchmark.p',sos_21) ).
fof(sos_22,axiom,
! [X64,X65,X66] :
( ( occurrence_of(X64,X66)
& occurrence_of(X64,X65) )
=> X65 = X66 ),
file('theBenchmark.p',sos_22) ).
fof(sos_23,axiom,
! [X67,X68] :
( ( ~ atomic(X68)
& leaf(X67,X68) )
=> ? [X69] :
( leaf_occ(X67,X69)
& occurrence_of(X69,X68) ) ),
file('theBenchmark.p',sos_23) ).
fof(sos_24,axiom,
! [X70,X71,X72] :
( min_precedes(X71,X72,X70)
=> ? [X73] :
( subactivity_occurrence(X72,X73)
& subactivity_occurrence(X71,X73)
& occurrence_of(X73,X70) ) ),
file('theBenchmark.p',sos_24) ).
fof(sos_25,axiom,
! [X74,X75] :
( ( ~ atomic(X75)
& leaf(X74,X75) )
=> ? [X76] :
( leaf_occ(X74,X76)
& occurrence_of(X76,X75) ) ),
file('theBenchmark.p',sos_25) ).
fof(sos_26,axiom,
! [X77,X78,X79] :
( min_precedes(X78,X79,X77)
=> ? [X80,X81] :
( atocc(X79,X81)
& atocc(X78,X80)
& subactivity(X81,X77)
& subactivity(X80,X77) ) ),
file('theBenchmark.p',sos_26) ).
fof(sos_27,axiom,
! [X82,X83] :
( root(X83,X82)
=> ? [X84] :
( atocc(X83,X84)
& subactivity(X84,X82) ) ),
file('theBenchmark.p',sos_27) ).
fof(sos_28,axiom,
! [X85,X86,X87,X88] :
( ( subactivity_occurrence(X88,X86)
& subactivity_occurrence(X87,X86)
& arboreal(X88)
& arboreal(X87)
& occurrence_of(X86,X85) )
=> ( X87 = X88
| min_precedes(X88,X87,X85)
| min_precedes(X87,X88,X85) ) ),
file('theBenchmark.p',sos_28) ).
fof(sos_29,axiom,
! [X89,X90] :
( occurrence_of(X90,X89)
=> ( activity_occurrence(X90)
& activity(X89) ) ),
file('theBenchmark.p',sos_29) ).
fof(sos_30,axiom,
! [X91,X92] :
( ( ~ atomic(X91)
& occurrence_of(X92,X91) )
=> ? [X93] :
( subactivity_occurrence(X93,X92)
& root(X93,X91) ) ),
file('theBenchmark.p',sos_30) ).
fof(sos_31,axiom,
! [X94] :
( activity(X94)
=> subactivity(X94,X94) ),
file('theBenchmark.p',sos_31) ).
fof(sos_32,axiom,
! [X95] :
( occurrence_of(X95,tptp0)
=> ? [X96,X97,X98] :
( leaf_occ(X98,X95)
& next_subocc(X97,X98,tptp0)
& ( occurrence_of(X98,tptp2)
| occurrence_of(X98,tptp1) )
& next_subocc(X96,X97,tptp0)
& occurrence_of(X97,tptp4)
& root_occ(X96,X95)
& occurrence_of(X96,tptp3) ) ),
file('theBenchmark.p',sos_32) ).
fof(sos_33,axiom,
activity(tptp0),
file('theBenchmark.p',sos_33) ).
fof(sos_34,axiom,
~ atomic(tptp0),
file('theBenchmark.p',sos_34) ).
fof(sos_35,axiom,
atomic(tptp4),
file('theBenchmark.p',sos_35) ).
fof(sos_36,axiom,
atomic(tptp1),
file('theBenchmark.p',sos_36) ).
fof(sos_37,axiom,
atomic(tptp2),
file('theBenchmark.p',sos_37) ).
fof(sos_38,axiom,
atomic(tptp3),
file('theBenchmark.p',sos_38) ).
fof(sos_39,axiom,
tptp4 != tptp3,
file('theBenchmark.p',sos_39) ).
fof(sos_40,axiom,
tptp4 != tptp1,
file('theBenchmark.p',sos_40) ).
fof(sos_41,axiom,
tptp4 != tptp2,
file('theBenchmark.p',sos_41) ).
fof(sos_42,axiom,
tptp3 != tptp1,
file('theBenchmark.p',sos_42) ).
fof(sos_43,axiom,
tptp3 != tptp2,
file('theBenchmark.p',sos_43) ).
fof(sos_44,axiom,
tptp1 != tptp2,
file('theBenchmark.p',sos_44) ).
fof(goals,conjecture,
! [X99] :
( occurrence_of(X99,tptp0)
=> ? [X100,X101] :
( ( occurrence_of(X101,tptp2)
=> ~ ? [X103] :
( min_precedes(X100,X103,tptp0)
& occurrence_of(X103,tptp1) ) )
& ( occurrence_of(X101,tptp1)
=> ~ ? [X102] :
( min_precedes(X100,X102,tptp0)
& occurrence_of(X102,tptp2) ) )
& leaf_occ(X101,X99) ) ),
file('theBenchmark.p',goals) ).
fof(f_1_1,plain,
! [X0,X1,X2,X3] :
( min_precedes(X0,X2,X3)
| ~ min_precedes(X1,X2,X3)
| ~ min_precedes(X0,X1,X3) ),
inference(fof_nnf,[status(thm)],[sos]) ).
fof(f_1_2,plain,
! [U_3,U_2,U_1,U_0] :
( min_precedes(U_3,U_1,U_0)
| ~ min_precedes(U_2,U_1,U_0)
| ~ min_precedes(U_3,U_2,U_0) ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
cnf(f_1_3,plain,
( min_precedes(U_3,U_1,U_0)
| ~ min_precedes(U_2,U_1,U_0)
| ~ min_precedes(U_3,U_2,U_0) ),
inference(clausify,[status(thm)],[f_1_2]) ).
fof(f_2_1,plain,
! [X4,X5,X6] :
( earlier(X4,X6)
| ~ earlier(X5,X6)
| ~ earlier(X4,X5) ),
inference(fof_nnf,[status(thm)],[sos_01]) ).
fof(f_2_2,plain,
! [U_6,U_5,U_4] :
( earlier(U_6,U_4)
| ~ earlier(U_5,U_4)
| ~ earlier(U_6,U_5) ),
inference(variable_rename,[status(thm)],[f_2_1]) ).
cnf(f_2_3,plain,
( earlier(U_6,U_4)
| ~ earlier(U_5,U_4)
| ~ earlier(U_6,U_5) ),
inference(clausify,[status(thm)],[f_2_2]) ).
fof(f_3_1,plain,
! [X7,X8,X9,X10] :
( X7 = X8
| ~ root_occ(X8,X9)
| ~ root_occ(X7,X9)
| ~ occurrence_of(X9,X10) ),
inference(fof_nnf,[status(thm)],[sos_02]) ).
fof(f_3_2,plain,
! [U_10,U_9,U_8,U_7] :
( U_10 = U_9
| ~ root_occ(U_9,U_8)
| ~ root_occ(U_10,U_8)
| ~ occurrence_of(U_8,U_7) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
fof(f_3_3,plain,
! [U_10,U_9] :
( ! [U_8] :
( ! [U_7] : ~ occurrence_of(U_8,U_7)
| ~ root_occ(U_9,U_8)
| ~ root_occ(U_10,U_8) )
| U_10 = U_9 ),
inference(miniscope,[status(thm)],[f_3_2]) ).
cnf(f_3_4,plain,
( ~ occurrence_of(U_8,U_7)
| ~ root_occ(U_9,U_8)
| ~ root_occ(U_10,U_8)
| U_10 = U_9 ),
inference(clausify,[status(thm)],[f_3_3]) ).
fof(f_4_1,plain,
! [X11,X12,X13,X14] :
( X11 = X12
| ~ leaf_occ(X12,X13)
| ~ leaf_occ(X11,X13)
| atomic(X14)
| ~ occurrence_of(X13,X14) ),
inference(fof_nnf,[status(thm)],[sos_03]) ).
fof(f_4_2,plain,
! [U_14,U_13,U_12,U_11] :
( U_14 = U_13
| ~ leaf_occ(U_13,U_12)
| ~ leaf_occ(U_14,U_12)
| atomic(U_11)
| ~ occurrence_of(U_12,U_11) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
fof(f_4_3,plain,
! [U_14,U_13] :
( ! [U_12] :
( ! [U_11] :
( atomic(U_11)
| ~ occurrence_of(U_12,U_11) )
| ~ leaf_occ(U_13,U_12)
| ~ leaf_occ(U_14,U_12) )
| U_14 = U_13 ),
inference(miniscope,[status(thm)],[f_4_2]) ).
cnf(f_4_4,plain,
( atomic(U_11)
| ~ occurrence_of(U_12,U_11)
| ~ leaf_occ(U_13,U_12)
| ~ leaf_occ(U_14,U_12)
| U_14 = U_13 ),
inference(clausify,[status(thm)],[f_4_3]) ).
fof(f_5_1,plain,
! [X15,X16,X17] :
( ( next_subocc(X15,X16,X17)
| ? [X18] :
( min_precedes(X18,X16,X17)
& min_precedes(X15,X18,X17) )
| ~ min_precedes(X15,X16,X17) )
& ( ( ! [X18] :
( ~ min_precedes(X18,X16,X17)
| ~ min_precedes(X15,X18,X17) )
& min_precedes(X15,X16,X17) )
| ~ next_subocc(X15,X16,X17) ) ),
inference(fof_nnf,[status(thm)],[sos_04]) ).
fof(f_5_2,plain,
! [U_19,U_18,U_17] :
( ( next_subocc(U_19,U_18,U_17)
| ? [U_16] :
( min_precedes(U_16,U_18,U_17)
& min_precedes(U_19,U_16,U_17) )
| ~ min_precedes(U_19,U_18,U_17) )
& ( ( ! [U_15] :
( ~ min_precedes(U_15,U_18,U_17)
| ~ min_precedes(U_19,U_15,U_17) )
& min_precedes(U_19,U_18,U_17) )
| ~ next_subocc(U_19,U_18,U_17) ) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
fof(f_5_3,plain,
( ! [U_25,U_23,U_21] :
( next_subocc(U_25,U_23,U_21)
| ? [U_16] :
( min_precedes(U_16,U_23,U_21)
& min_precedes(U_25,U_16,U_21) )
| ~ min_precedes(U_25,U_23,U_21) )
& ! [U_24,U_22,U_20] :
( ( ! [U_15] :
( ~ min_precedes(U_15,U_22,U_20)
| ~ min_precedes(U_24,U_15,U_20) )
& min_precedes(U_24,U_22,U_20) )
| ~ next_subocc(U_24,U_22,U_20) ) ),
inference(miniscope,[status(thm)],[f_5_2]) ).
fof(f_5_4,plain,
( ! [U_25,U_23,U_21] :
( next_subocc(U_25,U_23,U_21)
| ( min_precedes(sK1(U_25,U_23,U_21),U_23,U_21)
& min_precedes(U_25,sK1(U_25,U_23,U_21),U_21) )
| ~ min_precedes(U_25,U_23,U_21) )
& ! [U_24,U_22,U_20] :
( ( ! [U_15] :
( ~ min_precedes(U_15,U_22,U_20)
| ~ min_precedes(U_24,U_15,U_20) )
& min_precedes(U_24,U_22,U_20) )
| ~ next_subocc(U_24,U_22,U_20) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_16,sK1(U_25,U_23,U_21))],[f_5_3]) ).
cnf(f_5_5,plain,
( min_precedes(U_24,U_22,U_20)
| ~ next_subocc(U_24,U_22,U_20) ),
inference(clausify,[status(thm)],[f_5_4]) ).
cnf(f_5_6,plain,
( ~ min_precedes(U_15,U_22,U_20)
| ~ min_precedes(U_24,U_15,U_20)
| ~ next_subocc(U_24,U_22,U_20) ),
inference(clausify,[status(thm)],[f_5_4]) ).
cnf(f_5_7,plain,
( min_precedes(U_25,sK1(U_25,U_23,U_21),U_21)
| ~ min_precedes(U_25,U_23,U_21)
| next_subocc(U_25,U_23,U_21) ),
inference(clausify,[status(thm)],[f_5_4]) ).
cnf(f_5_8,plain,
( min_precedes(sK1(U_25,U_23,U_21),U_23,U_21)
| ~ min_precedes(U_25,U_23,U_21)
| next_subocc(U_25,U_23,U_21) ),
inference(clausify,[status(thm)],[f_5_4]) ).
fof(f_6_1,plain,
! [X19,X20,X21] :
( ( arboreal(X20)
& arboreal(X19) )
| ~ next_subocc(X19,X20,X21) ),
inference(fof_nnf,[status(thm)],[sos_05]) ).
fof(f_6_2,plain,
! [U_28,U_27,U_26] :
( ( arboreal(U_27)
& arboreal(U_28) )
| ~ next_subocc(U_28,U_27,U_26) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
fof(f_6_3,plain,
! [U_28,U_27] :
( ! [U_26] : ~ next_subocc(U_28,U_27,U_26)
| ( arboreal(U_27)
& arboreal(U_28) ) ),
inference(miniscope,[status(thm)],[f_6_2]) ).
cnf(f_6_4,plain,
( arboreal(U_28)
| ~ next_subocc(U_28,U_27,U_26) ),
inference(clausify,[status(thm)],[f_6_3]) ).
cnf(f_6_5,plain,
( arboreal(U_27)
| ~ next_subocc(U_28,U_27,U_26) ),
inference(clausify,[status(thm)],[f_6_3]) ).
fof(f_7_1,plain,
! [X22,X23,X24] :
( precedes(X22,X23)
| ~ min_precedes(X22,X23,X24) ),
inference(fof_nnf,[status(thm)],[sos_06]) ).
fof(f_7_2,plain,
! [U_31,U_30,U_29] :
( precedes(U_31,U_30)
| ~ min_precedes(U_31,U_30,U_29) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
fof(f_7_3,plain,
! [U_31,U_30] :
( ! [U_29] : ~ min_precedes(U_31,U_30,U_29)
| precedes(U_31,U_30) ),
inference(miniscope,[status(thm)],[f_7_2]) ).
cnf(f_7_4,plain,
( ~ min_precedes(U_31,U_30,U_29)
| precedes(U_31,U_30) ),
inference(clausify,[status(thm)],[f_7_3]) ).
fof(f_8_1,plain,
! [X25,X26,X27] :
( ~ root(X26,X27)
| ~ min_precedes(X25,X26,X27) ),
inference(fof_nnf,[status(thm)],[sos_07]) ).
fof(f_8_2,plain,
! [U_34,U_33,U_32] :
( ~ root(U_33,U_32)
| ~ min_precedes(U_34,U_33,U_32) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
cnf(f_8_3,plain,
( ~ root(U_33,U_32)
| ~ min_precedes(U_34,U_33,U_32) ),
inference(clausify,[status(thm)],[f_8_2]) ).
fof(f_9_1,plain,
! [X28,X29] :
( ( precedes(X28,X29)
| ~ legal(X29)
| ~ earlier(X28,X29) )
& ( ( legal(X29)
& earlier(X28,X29) )
| ~ precedes(X28,X29) ) ),
inference(fof_nnf,[status(thm)],[sos_08]) ).
fof(f_9_2,plain,
! [U_36,U_35] :
( ( precedes(U_36,U_35)
| ~ legal(U_35)
| ~ earlier(U_36,U_35) )
& ( ( legal(U_35)
& earlier(U_36,U_35) )
| ~ precedes(U_36,U_35) ) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
fof(f_9_3,plain,
( ! [U_40,U_38] :
( precedes(U_40,U_38)
| ~ legal(U_38)
| ~ earlier(U_40,U_38) )
& ! [U_39,U_37] :
( ( legal(U_37)
& earlier(U_39,U_37) )
| ~ precedes(U_39,U_37) ) ),
inference(miniscope,[status(thm)],[f_9_2]) ).
cnf(f_9_4,plain,
( earlier(U_39,U_37)
| ~ precedes(U_39,U_37) ),
inference(clausify,[status(thm)],[f_9_3]) ).
cnf(f_9_5,plain,
( legal(U_37)
| ~ precedes(U_39,U_37) ),
inference(clausify,[status(thm)],[f_9_3]) ).
cnf(f_9_6,plain,
( precedes(U_40,U_38)
| ~ legal(U_38)
| ~ earlier(U_40,U_38) ),
inference(clausify,[status(thm)],[f_9_3]) ).
fof(f_10_1,plain,
! [X30,X31] :
( ~ earlier(X31,X30)
| ~ earlier(X30,X31) ),
inference(fof_nnf,[status(thm)],[sos_09]) ).
fof(f_10_2,plain,
! [U_42,U_41] :
( ~ earlier(U_41,U_42)
| ~ earlier(U_42,U_41) ),
inference(variable_rename,[status(thm)],[f_10_1]) ).
cnf(f_10_3,plain,
( ~ earlier(U_41,U_42)
| ~ earlier(U_42,U_41) ),
inference(clausify,[status(thm)],[f_10_2]) ).
fof(f_11_1,plain,
! [X32,X33] :
( ( root_occ(X32,X33)
| ! [X34] :
( ~ root(X32,X34)
| ~ subactivity_occurrence(X32,X33)
| ~ occurrence_of(X33,X34) ) )
& ( ? [X34] :
( root(X32,X34)
& subactivity_occurrence(X32,X33)
& occurrence_of(X33,X34) )
| ~ root_occ(X32,X33) ) ),
inference(fof_nnf,[status(thm)],[sos_10]) ).
fof(f_11_2,plain,
! [U_46,U_45] :
( ( root_occ(U_46,U_45)
| ! [U_44] :
( ~ root(U_46,U_44)
| ~ subactivity_occurrence(U_46,U_45)
| ~ occurrence_of(U_45,U_44) ) )
& ( ? [U_43] :
( root(U_46,U_43)
& subactivity_occurrence(U_46,U_45)
& occurrence_of(U_45,U_43) )
| ~ root_occ(U_46,U_45) ) ),
inference(variable_rename,[status(thm)],[f_11_1]) ).
fof(f_11_3,plain,
( ! [U_50,U_48] :
( root_occ(U_50,U_48)
| ! [U_44] :
( ~ root(U_50,U_44)
| ~ occurrence_of(U_48,U_44) )
| ~ subactivity_occurrence(U_50,U_48) )
& ! [U_49,U_47] :
( ( ? [U_43] :
( root(U_49,U_43)
& occurrence_of(U_47,U_43) )
& subactivity_occurrence(U_49,U_47) )
| ~ root_occ(U_49,U_47) ) ),
inference(miniscope,[status(thm)],[f_11_2]) ).
fof(f_11_4,plain,
( ! [U_50,U_48] :
( root_occ(U_50,U_48)
| ! [U_44] :
( ~ root(U_50,U_44)
| ~ occurrence_of(U_48,U_44) )
| ~ subactivity_occurrence(U_50,U_48) )
& ! [U_49,U_47] :
( ( root(U_49,sK2(U_49,U_47))
& occurrence_of(U_47,sK2(U_49,U_47))
& subactivity_occurrence(U_49,U_47) )
| ~ root_occ(U_49,U_47) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_43,sK2(U_49,U_47))],[f_11_3]) ).
cnf(f_11_5,plain,
( subactivity_occurrence(U_49,U_47)
| ~ root_occ(U_49,U_47) ),
inference(clausify,[status(thm)],[f_11_4]) ).
cnf(f_11_6,plain,
( occurrence_of(U_47,sK2(U_49,U_47))
| ~ root_occ(U_49,U_47) ),
inference(clausify,[status(thm)],[f_11_4]) ).
cnf(f_11_7,plain,
( root(U_49,sK2(U_49,U_47))
| ~ root_occ(U_49,U_47) ),
inference(clausify,[status(thm)],[f_11_4]) ).
cnf(f_11_8,plain,
( root_occ(U_50,U_48)
| ~ root(U_50,U_44)
| ~ occurrence_of(U_48,U_44)
| ~ subactivity_occurrence(U_50,U_48) ),
inference(clausify,[status(thm)],[f_11_4]) ).
fof(f_12_1,plain,
! [X35,X36] :
( ( leaf_occ(X35,X36)
| ! [X37] :
( ~ leaf(X35,X37)
| ~ subactivity_occurrence(X35,X36)
| ~ occurrence_of(X36,X37) ) )
& ( ? [X37] :
( leaf(X35,X37)
& subactivity_occurrence(X35,X36)
& occurrence_of(X36,X37) )
| ~ leaf_occ(X35,X36) ) ),
inference(fof_nnf,[status(thm)],[sos_11]) ).
fof(f_12_2,plain,
! [U_54,U_53] :
( ( leaf_occ(U_54,U_53)
| ! [U_52] :
( ~ leaf(U_54,U_52)
| ~ subactivity_occurrence(U_54,U_53)
| ~ occurrence_of(U_53,U_52) ) )
& ( ? [U_51] :
( leaf(U_54,U_51)
& subactivity_occurrence(U_54,U_53)
& occurrence_of(U_53,U_51) )
| ~ leaf_occ(U_54,U_53) ) ),
inference(variable_rename,[status(thm)],[f_12_1]) ).
fof(f_12_3,plain,
( ! [U_58,U_56] :
( leaf_occ(U_58,U_56)
| ! [U_52] :
( ~ leaf(U_58,U_52)
| ~ occurrence_of(U_56,U_52) )
| ~ subactivity_occurrence(U_58,U_56) )
& ! [U_57,U_55] :
( ( ? [U_51] :
( leaf(U_57,U_51)
& occurrence_of(U_55,U_51) )
& subactivity_occurrence(U_57,U_55) )
| ~ leaf_occ(U_57,U_55) ) ),
inference(miniscope,[status(thm)],[f_12_2]) ).
fof(f_12_4,plain,
( ! [U_58,U_56] :
( leaf_occ(U_58,U_56)
| ! [U_52] :
( ~ leaf(U_58,U_52)
| ~ occurrence_of(U_56,U_52) )
| ~ subactivity_occurrence(U_58,U_56) )
& ! [U_57,U_55] :
( ( leaf(U_57,sK3(U_57,U_55))
& occurrence_of(U_55,sK3(U_57,U_55))
& subactivity_occurrence(U_57,U_55) )
| ~ leaf_occ(U_57,U_55) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_51,sK3(U_57,U_55))],[f_12_3]) ).
cnf(f_12_5,plain,
( subactivity_occurrence(U_57,U_55)
| ~ leaf_occ(U_57,U_55) ),
inference(clausify,[status(thm)],[f_12_4]) ).
cnf(f_12_6,plain,
( occurrence_of(U_55,sK3(U_57,U_55))
| ~ leaf_occ(U_57,U_55) ),
inference(clausify,[status(thm)],[f_12_4]) ).
cnf(f_12_7,plain,
( leaf(U_57,sK3(U_57,U_55))
| ~ leaf_occ(U_57,U_55) ),
inference(clausify,[status(thm)],[f_12_4]) ).
cnf(f_12_8,plain,
( leaf_occ(U_58,U_56)
| ~ leaf(U_58,U_52)
| ~ occurrence_of(U_56,U_52)
| ~ subactivity_occurrence(U_58,U_56) ),
inference(clausify,[status(thm)],[f_12_4]) ).
fof(f_13_1,plain,
! [X38,X39] :
( legal(X38)
| ~ root(X38,X39) ),
inference(fof_nnf,[status(thm)],[sos_12]) ).
fof(f_13_2,plain,
! [U_60,U_59] :
( legal(U_60)
| ~ root(U_60,U_59) ),
inference(variable_rename,[status(thm)],[f_13_1]) ).
fof(f_13_3,plain,
! [U_60] :
( ! [U_59] : ~ root(U_60,U_59)
| legal(U_60) ),
inference(miniscope,[status(thm)],[f_13_2]) ).
cnf(f_13_4,plain,
( ~ root(U_60,U_59)
| legal(U_60) ),
inference(clausify,[status(thm)],[f_13_3]) ).
fof(f_14_1,plain,
! [X40,X41] :
( ( ( arboreal(X40)
| ~ atomic(X41) )
& ( atomic(X41)
| ~ arboreal(X40) ) )
| ~ occurrence_of(X40,X41) ),
inference(fof_nnf,[status(thm)],[sos_13]) ).
fof(f_14_2,plain,
! [U_62,U_61] :
( ( ( arboreal(U_62)
| ~ atomic(U_61) )
& ( atomic(U_61)
| ~ arboreal(U_62) ) )
| ~ occurrence_of(U_62,U_61) ),
inference(variable_rename,[status(thm)],[f_14_1]) ).
cnf(f_14_3,plain,
( atomic(U_61)
| ~ arboreal(U_62)
| ~ occurrence_of(U_62,U_61) ),
inference(clausify,[status(thm)],[f_14_2]) ).
cnf(f_14_4,plain,
( arboreal(U_62)
| ~ atomic(U_61)
| ~ occurrence_of(U_62,U_61) ),
inference(clausify,[status(thm)],[f_14_2]) ).
fof(f_15_1,plain,
! [X42,X43] :
( ( leaf(X42,X43)
| ? [X45] : min_precedes(X42,X45,X43)
| ( ! [X44] : ~ min_precedes(X44,X42,X43)
& ~ root(X42,X43) ) )
& ( ( ! [X45] : ~ min_precedes(X42,X45,X43)
& ( ? [X44] : min_precedes(X44,X42,X43)
| root(X42,X43) ) )
| ~ leaf(X42,X43) ) ),
inference(fof_nnf,[status(thm)],[sos_14]) ).
fof(f_15_2,plain,
! [U_68,U_67] :
( ( leaf(U_68,U_67)
| ? [U_66] : min_precedes(U_68,U_66,U_67)
| ( ! [U_65] : ~ min_precedes(U_65,U_68,U_67)
& ~ root(U_68,U_67) ) )
& ( ( ! [U_64] : ~ min_precedes(U_68,U_64,U_67)
& ( ? [U_63] : min_precedes(U_63,U_68,U_67)
| root(U_68,U_67) ) )
| ~ leaf(U_68,U_67) ) ),
inference(variable_rename,[status(thm)],[f_15_1]) ).
fof(f_15_3,plain,
( ! [U_72,U_70] :
( leaf(U_72,U_70)
| ? [U_66] : min_precedes(U_72,U_66,U_70)
| ( ! [U_65] : ~ min_precedes(U_65,U_72,U_70)
& ~ root(U_72,U_70) ) )
& ! [U_71,U_69] :
( ( ! [U_64] : ~ min_precedes(U_71,U_64,U_69)
& ( ? [U_63] : min_precedes(U_63,U_71,U_69)
| root(U_71,U_69) ) )
| ~ leaf(U_71,U_69) ) ),
inference(miniscope,[status(thm)],[f_15_2]) ).
fof(f_15_4,plain,
( ! [U_72,U_70] :
( leaf(U_72,U_70)
| ? [U_66] : min_precedes(U_72,U_66,U_70)
| ( ! [U_65] : ~ min_precedes(U_65,U_72,U_70)
& ~ root(U_72,U_70) ) )
& ! [U_71,U_69] :
( ( ! [U_64] : ~ min_precedes(U_71,U_64,U_69)
& ( min_precedes(sK4(U_71,U_69),U_71,U_69)
| root(U_71,U_69) ) )
| ~ leaf(U_71,U_69) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_63,sK4(U_71,U_69))],[f_15_3]) ).
fof(f_15_5,plain,
( ! [U_72,U_70] :
( leaf(U_72,U_70)
| min_precedes(U_72,sK5(U_72,U_70),U_70)
| ( ! [U_65] : ~ min_precedes(U_65,U_72,U_70)
& ~ root(U_72,U_70) ) )
& ! [U_71,U_69] :
( ( ! [U_64] : ~ min_precedes(U_71,U_64,U_69)
& ( min_precedes(sK4(U_71,U_69),U_71,U_69)
| root(U_71,U_69) ) )
| ~ leaf(U_71,U_69) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_66,sK5(U_72,U_70))],[f_15_4]) ).
cnf(f_15_6,plain,
( min_precedes(sK4(U_71,U_69),U_71,U_69)
| root(U_71,U_69)
| ~ leaf(U_71,U_69) ),
inference(clausify,[status(thm)],[f_15_5]) ).
cnf(f_15_7,plain,
( ~ min_precedes(U_71,U_64,U_69)
| ~ leaf(U_71,U_69) ),
inference(clausify,[status(thm)],[f_15_5]) ).
cnf(f_15_8,plain,
( ~ root(U_72,U_70)
| min_precedes(U_72,sK5(U_72,U_70),U_70)
| leaf(U_72,U_70) ),
inference(clausify,[status(thm)],[f_15_5]) ).
cnf(f_15_9,plain,
( ~ min_precedes(U_65,U_72,U_70)
| min_precedes(U_72,sK5(U_72,U_70),U_70)
| leaf(U_72,U_70) ),
inference(clausify,[status(thm)],[f_15_5]) ).
fof(f_16_1,plain,
! [X46,X47] :
( ( atocc(X46,X47)
| ! [X48] :
( ~ occurrence_of(X46,X48)
| ~ atomic(X48)
| ~ subactivity(X47,X48) ) )
& ( ? [X48] :
( occurrence_of(X46,X48)
& atomic(X48)
& subactivity(X47,X48) )
| ~ atocc(X46,X47) ) ),
inference(fof_nnf,[status(thm)],[sos_15]) ).
fof(f_16_2,plain,
! [U_76,U_75] :
( ( atocc(U_76,U_75)
| ! [U_74] :
( ~ occurrence_of(U_76,U_74)
| ~ atomic(U_74)
| ~ subactivity(U_75,U_74) ) )
& ( ? [U_73] :
( occurrence_of(U_76,U_73)
& atomic(U_73)
& subactivity(U_75,U_73) )
| ~ atocc(U_76,U_75) ) ),
inference(variable_rename,[status(thm)],[f_16_1]) ).
fof(f_16_3,plain,
( ! [U_80,U_78] :
( atocc(U_80,U_78)
| ! [U_74] :
( ~ occurrence_of(U_80,U_74)
| ~ atomic(U_74)
| ~ subactivity(U_78,U_74) ) )
& ! [U_79,U_77] :
( ? [U_73] :
( occurrence_of(U_79,U_73)
& atomic(U_73)
& subactivity(U_77,U_73) )
| ~ atocc(U_79,U_77) ) ),
inference(miniscope,[status(thm)],[f_16_2]) ).
fof(f_16_4,plain,
( ! [U_80,U_78] :
( atocc(U_80,U_78)
| ! [U_74] :
( ~ occurrence_of(U_80,U_74)
| ~ atomic(U_74)
| ~ subactivity(U_78,U_74) ) )
& ! [U_79,U_77] :
( ( occurrence_of(U_79,sK6(U_79,U_77))
& atomic(sK6(U_79,U_77))
& subactivity(U_77,sK6(U_79,U_77)) )
| ~ atocc(U_79,U_77) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_73,sK6(U_79,U_77))],[f_16_3]) ).
cnf(f_16_5,plain,
( subactivity(U_77,sK6(U_79,U_77))
| ~ atocc(U_79,U_77) ),
inference(clausify,[status(thm)],[f_16_4]) ).
cnf(f_16_6,plain,
( atomic(sK6(U_79,U_77))
| ~ atocc(U_79,U_77) ),
inference(clausify,[status(thm)],[f_16_4]) ).
cnf(f_16_7,plain,
( occurrence_of(U_79,sK6(U_79,U_77))
| ~ atocc(U_79,U_77) ),
inference(clausify,[status(thm)],[f_16_4]) ).
cnf(f_16_8,plain,
( atocc(U_80,U_78)
| ~ occurrence_of(U_80,U_74)
| ~ atomic(U_74)
| ~ subactivity(U_78,U_74) ),
inference(clausify,[status(thm)],[f_16_4]) ).
fof(f_17_1,plain,
! [X49,X50] :
( root(X49,X50)
| ~ legal(X49)
| ~ atocc(X49,X50) ),
inference(fof_nnf,[status(thm)],[sos_16]) ).
fof(f_17_2,plain,
! [U_82,U_81] :
( root(U_82,U_81)
| ~ legal(U_82)
| ~ atocc(U_82,U_81) ),
inference(variable_rename,[status(thm)],[f_17_1]) ).
cnf(f_17_3,plain,
( root(U_82,U_81)
| ~ legal(U_82)
| ~ atocc(U_82,U_81) ),
inference(clausify,[status(thm)],[f_17_2]) ).
fof(f_18_1,plain,
! [X51] :
( arboreal(X51)
| ~ legal(X51) ),
inference(fof_nnf,[status(thm)],[sos_17]) ).
fof(f_18_2,plain,
! [U_83] :
( arboreal(U_83)
| ~ legal(U_83) ),
inference(variable_rename,[status(thm)],[f_18_1]) ).
cnf(f_18_3,plain,
( arboreal(U_83)
| ~ legal(U_83) ),
inference(clausify,[status(thm)],[f_18_2]) ).
fof(f_19_1,plain,
! [X52] :
( ? [X53] :
( occurrence_of(X52,X53)
& activity(X53) )
| ~ activity_occurrence(X52) ),
inference(fof_nnf,[status(thm)],[sos_18]) ).
fof(f_19_2,plain,
! [U_85] :
( ? [U_84] :
( occurrence_of(U_85,U_84)
& activity(U_84) )
| ~ activity_occurrence(U_85) ),
inference(variable_rename,[status(thm)],[f_19_1]) ).
fof(f_19_3,plain,
! [U_85] :
( ( occurrence_of(U_85,sK7(U_85))
& activity(sK7(U_85)) )
| ~ activity_occurrence(U_85) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_84,sK7(U_85))],[f_19_2]) ).
cnf(f_19_4,plain,
( activity(sK7(U_85))
| ~ activity_occurrence(U_85) ),
inference(clausify,[status(thm)],[f_19_3]) ).
cnf(f_19_5,plain,
( occurrence_of(U_85,sK7(U_85))
| ~ activity_occurrence(U_85) ),
inference(clausify,[status(thm)],[f_19_3]) ).
fof(f_20_1,plain,
! [X54,X55] :
( ( activity_occurrence(X55)
& activity_occurrence(X54) )
| ~ subactivity_occurrence(X54,X55) ),
inference(fof_nnf,[status(thm)],[sos_19]) ).
fof(f_20_2,plain,
! [U_87,U_86] :
( ( activity_occurrence(U_86)
& activity_occurrence(U_87) )
| ~ subactivity_occurrence(U_87,U_86) ),
inference(variable_rename,[status(thm)],[f_20_1]) ).
cnf(f_20_3,plain,
( activity_occurrence(U_87)
| ~ subactivity_occurrence(U_87,U_86) ),
inference(clausify,[status(thm)],[f_20_2]) ).
cnf(f_20_4,plain,
( activity_occurrence(U_86)
| ~ subactivity_occurrence(U_87,U_86) ),
inference(clausify,[status(thm)],[f_20_2]) ).
fof(f_21_1,plain,
! [X56,X57,X58] :
( ! [X59] : ~ min_precedes(X59,X57,X58)
| ~ root_occ(X57,X56)
| ~ occurrence_of(X56,X58) ),
inference(fof_nnf,[status(thm)],[sos_20]) ).
fof(f_21_2,plain,
! [U_91,U_90,U_89] :
( ! [U_88] : ~ min_precedes(U_88,U_90,U_89)
| ~ root_occ(U_90,U_91)
| ~ occurrence_of(U_91,U_89) ),
inference(variable_rename,[status(thm)],[f_21_1]) ).
cnf(f_21_3,plain,
( ~ min_precedes(U_88,U_90,U_89)
| ~ root_occ(U_90,U_91)
| ~ occurrence_of(U_91,U_89) ),
inference(clausify,[status(thm)],[f_21_2]) ).
fof(f_22_1,plain,
! [X60,X61,X62] :
( ! [X63] : ~ min_precedes(X61,X63,X62)
| ~ leaf_occ(X61,X60)
| ~ occurrence_of(X60,X62) ),
inference(fof_nnf,[status(thm)],[sos_21]) ).
fof(f_22_2,plain,
! [U_95,U_94,U_93] :
( ! [U_92] : ~ min_precedes(U_94,U_92,U_93)
| ~ leaf_occ(U_94,U_95)
| ~ occurrence_of(U_95,U_93) ),
inference(variable_rename,[status(thm)],[f_22_1]) ).
cnf(f_22_3,plain,
( ~ min_precedes(U_94,U_92,U_93)
| ~ leaf_occ(U_94,U_95)
| ~ occurrence_of(U_95,U_93) ),
inference(clausify,[status(thm)],[f_22_2]) ).
fof(f_23_1,plain,
! [X64,X65,X66] :
( X65 = X66
| ~ occurrence_of(X64,X66)
| ~ occurrence_of(X64,X65) ),
inference(fof_nnf,[status(thm)],[sos_22]) ).
fof(f_23_2,plain,
! [U_98,U_97,U_96] :
( U_97 = U_96
| ~ occurrence_of(U_98,U_96)
| ~ occurrence_of(U_98,U_97) ),
inference(variable_rename,[status(thm)],[f_23_1]) ).
cnf(f_23_3,plain,
( U_97 = U_96
| ~ occurrence_of(U_98,U_96)
| ~ occurrence_of(U_98,U_97) ),
inference(clausify,[status(thm)],[f_23_2]) ).
fof(f_24_1,plain,
! [X67,X68] :
( ? [X69] :
( leaf_occ(X67,X69)
& occurrence_of(X69,X68) )
| atomic(X68)
| ~ leaf(X67,X68) ),
inference(fof_nnf,[status(thm)],[sos_23]) ).
fof(f_24_2,plain,
! [U_101,U_100] :
( ? [U_99] :
( leaf_occ(U_101,U_99)
& occurrence_of(U_99,U_100) )
| atomic(U_100)
| ~ leaf(U_101,U_100) ),
inference(variable_rename,[status(thm)],[f_24_1]) ).
fof(f_24_3,plain,
! [U_101,U_100] :
( ( leaf_occ(U_101,sK8(U_101,U_100))
& occurrence_of(sK8(U_101,U_100),U_100) )
| atomic(U_100)
| ~ leaf(U_101,U_100) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_99,sK8(U_101,U_100))],[f_24_2]) ).
cnf(f_24_4,plain,
( occurrence_of(sK8(U_101,U_100),U_100)
| atomic(U_100)
| ~ leaf(U_101,U_100) ),
inference(clausify,[status(thm)],[f_24_3]) ).
cnf(f_24_5,plain,
( leaf_occ(U_101,sK8(U_101,U_100))
| atomic(U_100)
| ~ leaf(U_101,U_100) ),
inference(clausify,[status(thm)],[f_24_3]) ).
fof(f_25_1,plain,
! [X70,X71,X72] :
( ? [X73] :
( subactivity_occurrence(X72,X73)
& subactivity_occurrence(X71,X73)
& occurrence_of(X73,X70) )
| ~ min_precedes(X71,X72,X70) ),
inference(fof_nnf,[status(thm)],[sos_24]) ).
fof(f_25_2,plain,
! [U_105,U_104,U_103] :
( ? [U_102] :
( subactivity_occurrence(U_103,U_102)
& subactivity_occurrence(U_104,U_102)
& occurrence_of(U_102,U_105) )
| ~ min_precedes(U_104,U_103,U_105) ),
inference(variable_rename,[status(thm)],[f_25_1]) ).
fof(f_25_3,plain,
! [U_105,U_104,U_103] :
( ( subactivity_occurrence(U_103,sK9(U_105,U_104,U_103))
& subactivity_occurrence(U_104,sK9(U_105,U_104,U_103))
& occurrence_of(sK9(U_105,U_104,U_103),U_105) )
| ~ min_precedes(U_104,U_103,U_105) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_102,sK9(U_105,U_104,U_103))],[f_25_2]) ).
cnf(f_25_4,plain,
( occurrence_of(sK9(U_105,U_104,U_103),U_105)
| ~ min_precedes(U_104,U_103,U_105) ),
inference(clausify,[status(thm)],[f_25_3]) ).
cnf(f_25_5,plain,
( subactivity_occurrence(U_104,sK9(U_105,U_104,U_103))
| ~ min_precedes(U_104,U_103,U_105) ),
inference(clausify,[status(thm)],[f_25_3]) ).
cnf(f_25_6,plain,
( subactivity_occurrence(U_103,sK9(U_105,U_104,U_103))
| ~ min_precedes(U_104,U_103,U_105) ),
inference(clausify,[status(thm)],[f_25_3]) ).
fof(f_26_1,plain,
! [X74,X75] :
( ? [X76] :
( leaf_occ(X74,X76)
& occurrence_of(X76,X75) )
| atomic(X75)
| ~ leaf(X74,X75) ),
inference(fof_nnf,[status(thm)],[sos_25]) ).
fof(f_26_2,plain,
! [U_108,U_107] :
( ? [U_106] :
( leaf_occ(U_108,U_106)
& occurrence_of(U_106,U_107) )
| atomic(U_107)
| ~ leaf(U_108,U_107) ),
inference(variable_rename,[status(thm)],[f_26_1]) ).
fof(f_26_3,plain,
! [U_108,U_107] :
( ( leaf_occ(U_108,sK10(U_108,U_107))
& occurrence_of(sK10(U_108,U_107),U_107) )
| atomic(U_107)
| ~ leaf(U_108,U_107) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_106,sK10(U_108,U_107))],[f_26_2]) ).
cnf(f_26_4,plain,
( occurrence_of(sK10(U_108,U_107),U_107)
| atomic(U_107)
| ~ leaf(U_108,U_107) ),
inference(clausify,[status(thm)],[f_26_3]) ).
cnf(f_26_5,plain,
( leaf_occ(U_108,sK10(U_108,U_107))
| atomic(U_107)
| ~ leaf(U_108,U_107) ),
inference(clausify,[status(thm)],[f_26_3]) ).
fof(f_27_1,plain,
! [X77,X78,X79] :
( ? [X80,X81] :
( atocc(X79,X81)
& atocc(X78,X80)
& subactivity(X81,X77)
& subactivity(X80,X77) )
| ~ min_precedes(X78,X79,X77) ),
inference(fof_nnf,[status(thm)],[sos_26]) ).
fof(f_27_2,plain,
! [U_113,U_112,U_111] :
( ? [U_110,U_109] :
( atocc(U_111,U_109)
& atocc(U_112,U_110)
& subactivity(U_109,U_113)
& subactivity(U_110,U_113) )
| ~ min_precedes(U_112,U_111,U_113) ),
inference(variable_rename,[status(thm)],[f_27_1]) ).
fof(f_27_3,plain,
! [U_113,U_112,U_111] :
( ( ? [U_110] :
( atocc(U_112,U_110)
& subactivity(U_110,U_113) )
& ? [U_109] :
( atocc(U_111,U_109)
& subactivity(U_109,U_113) ) )
| ~ min_precedes(U_112,U_111,U_113) ),
inference(miniscope,[status(thm)],[f_27_2]) ).
fof(f_27_4,plain,
! [U_113,U_112,U_111] :
( ( ? [U_110] :
( atocc(U_112,U_110)
& subactivity(U_110,U_113) )
& atocc(U_111,sK11(U_113,U_112,U_111))
& subactivity(sK11(U_113,U_112,U_111),U_113) )
| ~ min_precedes(U_112,U_111,U_113) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_109,sK11(U_113,U_112,U_111))],[f_27_3]) ).
fof(f_27_5,plain,
! [U_113,U_112,U_111] :
( ( atocc(U_112,sK12(U_113,U_112,U_111))
& subactivity(sK12(U_113,U_112,U_111),U_113)
& atocc(U_111,sK11(U_113,U_112,U_111))
& subactivity(sK11(U_113,U_112,U_111),U_113) )
| ~ min_precedes(U_112,U_111,U_113) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(U_110,sK12(U_113,U_112,U_111))],[f_27_4]) ).
cnf(f_27_6,plain,
( subactivity(sK11(U_113,U_112,U_111),U_113)
| ~ min_precedes(U_112,U_111,U_113) ),
inference(clausify,[status(thm)],[f_27_5]) ).
cnf(f_27_7,plain,
( atocc(U_111,sK11(U_113,U_112,U_111))
| ~ min_precedes(U_112,U_111,U_113) ),
inference(clausify,[status(thm)],[f_27_5]) ).
cnf(f_27_8,plain,
( subactivity(sK12(U_113,U_112,U_111),U_113)
| ~ min_precedes(U_112,U_111,U_113) ),
inference(clausify,[status(thm)],[f_27_5]) ).
cnf(f_27_9,plain,
( atocc(U_112,sK12(U_113,U_112,U_111))
| ~ min_precedes(U_112,U_111,U_113) ),
inference(clausify,[status(thm)],[f_27_5]) ).
fof(f_28_1,plain,
! [X82,X83] :
( ? [X84] :
( atocc(X83,X84)
& subactivity(X84,X82) )
| ~ root(X83,X82) ),
inference(fof_nnf,[status(thm)],[sos_27]) ).
fof(f_28_2,plain,
! [U_116,U_115] :
( ? [U_114] :
( atocc(U_115,U_114)
& subactivity(U_114,U_116) )
| ~ root(U_115,U_116) ),
inference(variable_rename,[status(thm)],[f_28_1]) ).
fof(f_28_3,plain,
! [U_116,U_115] :
( ( atocc(U_115,sK13(U_116,U_115))
& subactivity(sK13(U_116,U_115),U_116) )
| ~ root(U_115,U_116) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(U_114,sK13(U_116,U_115))],[f_28_2]) ).
cnf(f_28_4,plain,
( subactivity(sK13(U_116,U_115),U_116)
| ~ root(U_115,U_116) ),
inference(clausify,[status(thm)],[f_28_3]) ).
cnf(f_28_5,plain,
( atocc(U_115,sK13(U_116,U_115))
| ~ root(U_115,U_116) ),
inference(clausify,[status(thm)],[f_28_3]) ).
fof(f_29_1,plain,
! [X85,X86,X87,X88] :
( X87 = X88
| min_precedes(X88,X87,X85)
| min_precedes(X87,X88,X85)
| ~ subactivity_occurrence(X88,X86)
| ~ subactivity_occurrence(X87,X86)
| ~ arboreal(X88)
| ~ arboreal(X87)
| ~ occurrence_of(X86,X85) ),
inference(fof_nnf,[status(thm)],[sos_28]) ).
fof(f_29_2,plain,
! [U_120,U_119,U_118,U_117] :
( U_118 = U_117
| min_precedes(U_117,U_118,U_120)
| min_precedes(U_118,U_117,U_120)
| ~ subactivity_occurrence(U_117,U_119)
| ~ subactivity_occurrence(U_118,U_119)
| ~ arboreal(U_117)
| ~ arboreal(U_118)
| ~ occurrence_of(U_119,U_120) ),
inference(variable_rename,[status(thm)],[f_29_1]) ).
cnf(f_29_3,plain,
( U_118 = U_117
| min_precedes(U_117,U_118,U_120)
| min_precedes(U_118,U_117,U_120)
| ~ subactivity_occurrence(U_117,U_119)
| ~ subactivity_occurrence(U_118,U_119)
| ~ arboreal(U_117)
| ~ arboreal(U_118)
| ~ occurrence_of(U_119,U_120) ),
inference(clausify,[status(thm)],[f_29_2]) ).
fof(f_30_1,plain,
! [X89,X90] :
( ( activity_occurrence(X90)
& activity(X89) )
| ~ occurrence_of(X90,X89) ),
inference(fof_nnf,[status(thm)],[sos_29]) ).
fof(f_30_2,plain,
! [U_122,U_121] :
( ( activity_occurrence(U_121)
& activity(U_122) )
| ~ occurrence_of(U_121,U_122) ),
inference(variable_rename,[status(thm)],[f_30_1]) ).
cnf(f_30_3,plain,
( activity(U_122)
| ~ occurrence_of(U_121,U_122) ),
inference(clausify,[status(thm)],[f_30_2]) ).
cnf(f_30_4,plain,
( activity_occurrence(U_121)
| ~ occurrence_of(U_121,U_122) ),
inference(clausify,[status(thm)],[f_30_2]) ).
fof(f_31_1,plain,
! [X91,X92] :
( ? [X93] :
( subactivity_occurrence(X93,X92)
& root(X93,X91) )
| atomic(X91)
| ~ occurrence_of(X92,X91) ),
inference(fof_nnf,[status(thm)],[sos_30]) ).
fof(f_31_2,plain,
! [U_125,U_124] :
( ? [U_123] :
( subactivity_occurrence(U_123,U_124)
& root(U_123,U_125) )
| atomic(U_125)
| ~ occurrence_of(U_124,U_125) ),
inference(variable_rename,[status(thm)],[f_31_1]) ).
fof(f_31_3,plain,
! [U_125,U_124] :
( ( subactivity_occurrence(sK14(U_125,U_124),U_124)
& root(sK14(U_125,U_124),U_125) )
| atomic(U_125)
| ~ occurrence_of(U_124,U_125) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_123,sK14(U_125,U_124))],[f_31_2]) ).
cnf(f_31_4,plain,
( root(sK14(U_125,U_124),U_125)
| atomic(U_125)
| ~ occurrence_of(U_124,U_125) ),
inference(clausify,[status(thm)],[f_31_3]) ).
cnf(f_31_5,plain,
( subactivity_occurrence(sK14(U_125,U_124),U_124)
| atomic(U_125)
| ~ occurrence_of(U_124,U_125) ),
inference(clausify,[status(thm)],[f_31_3]) ).
fof(f_32_1,plain,
! [X94] :
( subactivity(X94,X94)
| ~ activity(X94) ),
inference(fof_nnf,[status(thm)],[sos_31]) ).
fof(f_32_2,plain,
! [U_126] :
( subactivity(U_126,U_126)
| ~ activity(U_126) ),
inference(variable_rename,[status(thm)],[f_32_1]) ).
cnf(f_32_3,plain,
( subactivity(U_126,U_126)
| ~ activity(U_126) ),
inference(clausify,[status(thm)],[f_32_2]) ).
fof(f_33_1,plain,
! [X95] :
( ? [X96,X97,X98] :
( leaf_occ(X98,X95)
& next_subocc(X97,X98,tptp0)
& ( occurrence_of(X98,tptp2)
| occurrence_of(X98,tptp1) )
& next_subocc(X96,X97,tptp0)
& occurrence_of(X97,tptp4)
& root_occ(X96,X95)
& occurrence_of(X96,tptp3) )
| ~ occurrence_of(X95,tptp0) ),
inference(fof_nnf,[status(thm)],[sos_32]) ).
fof(f_33_2,plain,
! [U_130] :
( ? [U_129,U_128,U_127] :
( leaf_occ(U_127,U_130)
& next_subocc(U_128,U_127,tptp0)
& ( occurrence_of(U_127,tptp2)
| occurrence_of(U_127,tptp1) )
& next_subocc(U_129,U_128,tptp0)
& occurrence_of(U_128,tptp4)
& root_occ(U_129,U_130)
& occurrence_of(U_129,tptp3) )
| ~ occurrence_of(U_130,tptp0) ),
inference(variable_rename,[status(thm)],[f_33_1]) ).
fof(f_33_3,plain,
! [U_130] :
( ? [U_129] :
( ? [U_128] :
( ? [U_127] :
( leaf_occ(U_127,U_130)
& next_subocc(U_128,U_127,tptp0)
& ( occurrence_of(U_127,tptp2)
| occurrence_of(U_127,tptp1) ) )
& next_subocc(U_129,U_128,tptp0)
& occurrence_of(U_128,tptp4) )
& root_occ(U_129,U_130)
& occurrence_of(U_129,tptp3) )
| ~ occurrence_of(U_130,tptp0) ),
inference(miniscope,[status(thm)],[f_33_2]) ).
fof(f_33_4,plain,
! [U_130] :
( ( ? [U_128] :
( ? [U_127] :
( leaf_occ(U_127,U_130)
& next_subocc(U_128,U_127,tptp0)
& ( occurrence_of(U_127,tptp2)
| occurrence_of(U_127,tptp1) ) )
& next_subocc(sK15(U_130),U_128,tptp0)
& occurrence_of(U_128,tptp4) )
& root_occ(sK15(U_130),U_130)
& occurrence_of(sK15(U_130),tptp3) )
| ~ occurrence_of(U_130,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(U_129,sK15(U_130))],[f_33_3]) ).
fof(f_33_5,plain,
! [U_130] :
( ( ? [U_127] :
( leaf_occ(U_127,U_130)
& next_subocc(sK16(U_130),U_127,tptp0)
& ( occurrence_of(U_127,tptp2)
| occurrence_of(U_127,tptp1) ) )
& next_subocc(sK15(U_130),sK16(U_130),tptp0)
& occurrence_of(sK16(U_130),tptp4)
& root_occ(sK15(U_130),U_130)
& occurrence_of(sK15(U_130),tptp3) )
| ~ occurrence_of(U_130,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(U_128,sK16(U_130))],[f_33_4]) ).
fof(f_33_6,plain,
! [U_130] :
( ( leaf_occ(sK17(U_130),U_130)
& next_subocc(sK16(U_130),sK17(U_130),tptp0)
& ( occurrence_of(sK17(U_130),tptp2)
| occurrence_of(sK17(U_130),tptp1) )
& next_subocc(sK15(U_130),sK16(U_130),tptp0)
& occurrence_of(sK16(U_130),tptp4)
& root_occ(sK15(U_130),U_130)
& occurrence_of(sK15(U_130),tptp3) )
| ~ occurrence_of(U_130,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(U_127,sK17(U_130))],[f_33_5]) ).
cnf(f_33_7,plain,
( occurrence_of(sK15(U_130),tptp3)
| ~ occurrence_of(U_130,tptp0) ),
inference(clausify,[status(thm)],[f_33_6]) ).
cnf(f_33_8,plain,
( root_occ(sK15(U_130),U_130)
| ~ occurrence_of(U_130,tptp0) ),
inference(clausify,[status(thm)],[f_33_6]) ).
cnf(f_33_9,plain,
( occurrence_of(sK16(U_130),tptp4)
| ~ occurrence_of(U_130,tptp0) ),
inference(clausify,[status(thm)],[f_33_6]) ).
cnf(f_33_10,plain,
( next_subocc(sK15(U_130),sK16(U_130),tptp0)
| ~ occurrence_of(U_130,tptp0) ),
inference(clausify,[status(thm)],[f_33_6]) ).
cnf(f_33_11,plain,
( occurrence_of(sK17(U_130),tptp2)
| occurrence_of(sK17(U_130),tptp1)
| ~ occurrence_of(U_130,tptp0) ),
inference(clausify,[status(thm)],[f_33_6]) ).
cnf(f_33_12,plain,
( next_subocc(sK16(U_130),sK17(U_130),tptp0)
| ~ occurrence_of(U_130,tptp0) ),
inference(clausify,[status(thm)],[f_33_6]) ).
cnf(f_33_13,plain,
( leaf_occ(sK17(U_130),U_130)
| ~ occurrence_of(U_130,tptp0) ),
inference(clausify,[status(thm)],[f_33_6]) ).
fof(f_34_1,plain,
activity(tptp0),
inference(fof_nnf,[status(thm)],[sos_33]) ).
cnf(f_34_2,plain,
activity(tptp0),
inference(clausify,[status(thm)],[f_34_1]) ).
fof(f_35_1,plain,
~ atomic(tptp0),
inference(fof_nnf,[status(thm)],[sos_34]) ).
cnf(f_35_2,plain,
~ atomic(tptp0),
inference(clausify,[status(thm)],[f_35_1]) ).
fof(f_36_1,plain,
atomic(tptp4),
inference(fof_nnf,[status(thm)],[sos_35]) ).
cnf(f_36_2,plain,
atomic(tptp4),
inference(clausify,[status(thm)],[f_36_1]) ).
fof(f_37_1,plain,
atomic(tptp1),
inference(fof_nnf,[status(thm)],[sos_36]) ).
cnf(f_37_2,plain,
atomic(tptp1),
inference(clausify,[status(thm)],[f_37_1]) ).
fof(f_38_1,plain,
atomic(tptp2),
inference(fof_nnf,[status(thm)],[sos_37]) ).
cnf(f_38_2,plain,
atomic(tptp2),
inference(clausify,[status(thm)],[f_38_1]) ).
fof(f_39_1,plain,
atomic(tptp3),
inference(fof_nnf,[status(thm)],[sos_38]) ).
cnf(f_39_2,plain,
atomic(tptp3),
inference(clausify,[status(thm)],[f_39_1]) ).
fof(f_40_1,plain,
tptp4 != tptp3,
inference(fof_nnf,[status(thm)],[sos_39]) ).
cnf(f_40_2,plain,
tptp4 != tptp3,
inference(clausify,[status(thm)],[f_40_1]) ).
fof(f_41_1,plain,
tptp4 != tptp1,
inference(fof_nnf,[status(thm)],[sos_40]) ).
cnf(f_41_2,plain,
tptp4 != tptp1,
inference(clausify,[status(thm)],[f_41_1]) ).
fof(f_42_1,plain,
tptp4 != tptp2,
inference(fof_nnf,[status(thm)],[sos_41]) ).
cnf(f_42_2,plain,
tptp4 != tptp2,
inference(clausify,[status(thm)],[f_42_1]) ).
fof(f_43_1,plain,
tptp3 != tptp1,
inference(fof_nnf,[status(thm)],[sos_42]) ).
cnf(f_43_2,plain,
tptp3 != tptp1,
inference(clausify,[status(thm)],[f_43_1]) ).
fof(f_44_1,plain,
tptp3 != tptp2,
inference(fof_nnf,[status(thm)],[sos_43]) ).
cnf(f_44_2,plain,
tptp3 != tptp2,
inference(clausify,[status(thm)],[f_44_1]) ).
fof(f_45_1,plain,
tptp1 != tptp2,
inference(fof_nnf,[status(thm)],[sos_44]) ).
cnf(f_45_2,plain,
tptp1 != tptp2,
inference(clausify,[status(thm)],[f_45_1]) ).
fof(f_46_1,negated_conjecture,
~ ! [X99] :
( occurrence_of(X99,tptp0)
=> ? [X100,X101] :
( ( occurrence_of(X101,tptp2)
=> ~ ? [X103] :
( min_precedes(X100,X103,tptp0)
& occurrence_of(X103,tptp1) ) )
& ( occurrence_of(X101,tptp1)
=> ~ ? [X102] :
( min_precedes(X100,X102,tptp0)
& occurrence_of(X102,tptp2) ) )
& leaf_occ(X101,X99) ) ),
inference(negate,[status(cth)],[goals]) ).
fof(f_46_2,negated_conjecture,
? [X99] :
( ! [X100,X101] :
( ( ? [X103] :
( min_precedes(X100,X103,tptp0)
& occurrence_of(X103,tptp1) )
& occurrence_of(X101,tptp2) )
| ( ? [X102] :
( min_precedes(X100,X102,tptp0)
& occurrence_of(X102,tptp2) )
& occurrence_of(X101,tptp1) )
| ~ leaf_occ(X101,X99) )
& occurrence_of(X99,tptp0) ),
inference(fof_nnf,[status(thm)],[f_46_1]) ).
fof(f_46_3,negated_conjecture,
? [U_135] :
( ! [U_134,U_133] :
( ( ? [U_132] :
( min_precedes(U_134,U_132,tptp0)
& occurrence_of(U_132,tptp1) )
& occurrence_of(U_133,tptp2) )
| ( ? [U_131] :
( min_precedes(U_134,U_131,tptp0)
& occurrence_of(U_131,tptp2) )
& occurrence_of(U_133,tptp1) )
| ~ leaf_occ(U_133,U_135) )
& occurrence_of(U_135,tptp0) ),
inference(variable_rename,[status(thm)],[f_46_2]) ).
fof(f_46_4,negated_conjecture,
( ! [U_134,U_133] :
( ( ? [U_132] :
( min_precedes(U_134,U_132,tptp0)
& occurrence_of(U_132,tptp1) )
& occurrence_of(U_133,tptp2) )
| ( ? [U_131] :
( min_precedes(U_134,U_131,tptp0)
& occurrence_of(U_131,tptp2) )
& occurrence_of(U_133,tptp1) )
| ~ leaf_occ(U_133,sK18) )
& occurrence_of(sK18,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(U_135,sK18)],[f_46_3]) ).
fof(f_46_5,negated_conjecture,
( ! [U_134,U_133] :
( ( ? [U_132] :
( min_precedes(U_134,U_132,tptp0)
& occurrence_of(U_132,tptp1) )
& occurrence_of(U_133,tptp2) )
| ( min_precedes(U_134,sK19(U_134,U_133),tptp0)
& occurrence_of(sK19(U_134,U_133),tptp2)
& occurrence_of(U_133,tptp1) )
| ~ leaf_occ(U_133,sK18) )
& occurrence_of(sK18,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(U_131,sK19(U_134,U_133))],[f_46_4]) ).
fof(f_46_6,negated_conjecture,
( ! [U_134,U_133] :
( ( min_precedes(U_134,sK20(U_134,U_133),tptp0)
& occurrence_of(sK20(U_134,U_133),tptp1)
& occurrence_of(U_133,tptp2) )
| ( min_precedes(U_134,sK19(U_134,U_133),tptp0)
& occurrence_of(sK19(U_134,U_133),tptp2)
& occurrence_of(U_133,tptp1) )
| ~ leaf_occ(U_133,sK18) )
& occurrence_of(sK18,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(U_132,sK20(U_134,U_133))],[f_46_5]) ).
cnf(f_46_7,negated_conjecture,
occurrence_of(sK18,tptp0),
inference(clausify,[status(thm)],[f_46_6]) ).
cnf(f_46_8,negated_conjecture,
( occurrence_of(U_133,tptp2)
| occurrence_of(U_133,tptp1)
| ~ leaf_occ(U_133,sK18) ),
inference(clausify,[status(thm)],[f_46_6]) ).
cnf(f_46_9,negated_conjecture,
( occurrence_of(sK20(U_134,U_133),tptp1)
| occurrence_of(U_133,tptp1)
| ~ leaf_occ(U_133,sK18) ),
inference(clausify,[status(thm)],[f_46_6]) ).
cnf(f_46_10,negated_conjecture,
( min_precedes(U_134,sK20(U_134,U_133),tptp0)
| occurrence_of(U_133,tptp1)
| ~ leaf_occ(U_133,sK18) ),
inference(clausify,[status(thm)],[f_46_6]) ).
cnf(f_46_11,negated_conjecture,
( occurrence_of(sK19(U_134,U_133),tptp2)
| occurrence_of(U_133,tptp2)
| ~ leaf_occ(U_133,sK18) ),
inference(clausify,[status(thm)],[f_46_6]) ).
cnf(f_46_12,negated_conjecture,
( min_precedes(U_134,sK19(U_134,U_133),tptp0)
| occurrence_of(U_133,tptp2)
| ~ leaf_occ(U_133,sK18) ),
inference(clausify,[status(thm)],[f_46_6]) ).
cnf(f_46_13,negated_conjecture,
( occurrence_of(sK20(U_134,U_133),tptp1)
| occurrence_of(sK19(U_134,U_133),tptp2)
| ~ leaf_occ(U_133,sK18) ),
inference(clausify,[status(thm)],[f_46_6]) ).
cnf(f_46_14,negated_conjecture,
( min_precedes(U_134,sK20(U_134,U_133),tptp0)
| occurrence_of(sK19(U_134,U_133),tptp2)
| ~ leaf_occ(U_133,sK18) ),
inference(clausify,[status(thm)],[f_46_6]) ).
cnf(f_46_15,negated_conjecture,
( occurrence_of(sK20(U_134,U_133),tptp1)
| min_precedes(U_134,sK19(U_134,U_133),tptp0)
| ~ leaf_occ(U_133,sK18) ),
inference(clausify,[status(thm)],[f_46_6]) ).
cnf(f_46_16,negated_conjecture,
( min_precedes(U_134,sK20(U_134,U_133),tptp0)
| min_precedes(U_134,sK19(U_134,U_133),tptp0)
| ~ leaf_occ(U_133,sK18) ),
inference(clausify,[status(thm)],[f_46_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,Eq_x_1,Eq_x_2) = sK1(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_5,axiom,
( sK2(Eq_x_0,Eq_x_1) = sK2(Eq_y_0,Eq_y_1)
| 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) = sK3(Eq_y_0,Eq_y_1)
| 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) = sK5(Eq_y_0,Eq_y_1)
| 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) = sK7(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_11,axiom,
( sK8(Eq_x_0,Eq_x_1) = sK8(Eq_y_0,Eq_y_1)
| 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,Eq_x_2) = sK9(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_13,axiom,
( sK10(Eq_x_0,Eq_x_1) = sK10(Eq_y_0,Eq_y_1)
| 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,Eq_x_2) = sK11(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_15,axiom,
( sK12(Eq_x_0,Eq_x_1,Eq_x_2) = sK12(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_16,axiom,
( sK13(Eq_x_0,Eq_x_1) = sK13(Eq_y_0,Eq_y_1)
| 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) = sK15(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_19,axiom,
( sK16(Eq_x_0) = sK16(Eq_y_0)
| 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,
( sK19(Eq_x_0,Eq_x_1) = sK19(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_22,axiom,
( sK20(Eq_x_0,Eq_x_1) = sK20(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_23,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_24,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_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,
( 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_27,axiom,
( atomic(Eq_y_0)
| ~ atomic(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_28,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(equality_29,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_30,axiom,
( arboreal(Eq_y_0)
| ~ arboreal(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_31,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_32,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_33,axiom,
( legal(Eq_y_0)
| ~ legal(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_34,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_35,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_36,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_37,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_38,axiom,
( activity_occurrence(Eq_y_0)
| ~ activity_occurrence(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_39,axiom,
( activity(Eq_y_0)
| ~ activity(Eq_x_0)
| 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+2 : 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.09/0.38 % Computer : n009.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Sat Sep 19 19:51:57 UTC 2026
% 0.09/0.38 % CPUTime :
% 167.32/167.70 % SZS status Theorem for theBenchmark
% 167.32/167.70 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------