%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : PRO010+4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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 77.24s 77.51s
% Output : Proof 77.24s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(sos,axiom,
! [X0,X1] :
( ( ~ atomic(X0)
& occurrence_of(X1,X0) )
=> ? [X2] :
( subactivity_occurrence(X2,X1)
& root(X2,X0) ) ),
file('theBenchmark.p',sos) ).
fof(sos_01,axiom,
! [X3,X4,X5,X6,X7] :
( ( X5 != X7
& min_precedes(X6,X5,X3)
& subactivity_occurrence(X5,X4)
& leaf_occ(X7,X4)
& root_occ(X6,X4)
& occurrence_of(X4,X3) )
=> min_precedes(X5,X7,X3) ),
file('theBenchmark.p',sos_01) ).
fof(sos_02,axiom,
! [X8,X9,X10,X11] :
( ( ~ min_precedes(X10,X11,X8)
& arboreal(X10)
& leaf_occ(X11,X9)
& subactivity_occurrence(X10,X9)
& occurrence_of(X9,X8) )
=> X11 = X10 ),
file('theBenchmark.p',sos_02) ).
fof(sos_03,axiom,
! [X12,X13] :
( occurrence_of(X13,X12)
=> ( activity_occurrence(X13)
& activity(X12) ) ),
file('theBenchmark.p',sos_03) ).
fof(sos_04,axiom,
! [X14,X15,X16,X17] :
( ( subactivity_occurrence(X17,X15)
& subactivity_occurrence(X16,X15)
& arboreal(X17)
& arboreal(X16)
& occurrence_of(X15,X14) )
=> ( X16 = X17
| min_precedes(X17,X16,X14)
| min_precedes(X16,X17,X14) ) ),
file('theBenchmark.p',sos_04) ).
fof(sos_05,axiom,
! [X18,X19] :
( root(X19,X18)
=> ? [X20] :
( atocc(X19,X20)
& subactivity(X20,X18) ) ),
file('theBenchmark.p',sos_05) ).
fof(sos_06,axiom,
! [X21,X22,X23] :
( min_precedes(X22,X23,X21)
=> ? [X24] :
( subactivity_occurrence(X23,X24)
& subactivity_occurrence(X22,X24)
& occurrence_of(X24,X21) ) ),
file('theBenchmark.p',sos_06) ).
fof(sos_07,axiom,
! [X25,X26] :
( ( ~ atomic(X26)
& leaf(X25,X26) )
=> ? [X27] :
( leaf_occ(X25,X27)
& occurrence_of(X27,X26) ) ),
file('theBenchmark.p',sos_07) ).
fof(sos_08,axiom,
! [X28,X29,X30] :
( ( occurrence_of(X28,X30)
& occurrence_of(X28,X29) )
=> X29 = X30 ),
file('theBenchmark.p',sos_08) ).
fof(sos_09,axiom,
! [X31,X32,X33] :
( ( leaf_occ(X32,X31)
& occurrence_of(X31,X33) )
=> ~ ? [X34] : min_precedes(X32,X34,X33) ),
file('theBenchmark.p',sos_09) ).
fof(sos_10,axiom,
! [X35,X36,X37] :
( ( root_occ(X36,X35)
& occurrence_of(X35,X37) )
=> ~ ? [X38] : min_precedes(X38,X36,X37) ),
file('theBenchmark.p',sos_10) ).
fof(sos_11,axiom,
! [X39,X40] :
( subactivity_occurrence(X39,X40)
=> ( activity_occurrence(X40)
& activity_occurrence(X39) ) ),
file('theBenchmark.p',sos_11) ).
fof(sos_12,axiom,
! [X41] :
( activity_occurrence(X41)
=> ? [X42] :
( occurrence_of(X41,X42)
& activity(X42) ) ),
file('theBenchmark.p',sos_12) ).
fof(sos_13,axiom,
! [X43] :
( legal(X43)
=> arboreal(X43) ),
file('theBenchmark.p',sos_13) ).
fof(sos_14,axiom,
! [X44,X45] :
( atocc(X44,X45)
<=> ? [X46] :
( occurrence_of(X44,X46)
& atomic(X46)
& subactivity(X45,X46) ) ),
file('theBenchmark.p',sos_14) ).
fof(sos_15,axiom,
! [X47,X48] :
( leaf(X47,X48)
<=> ( ~ ? [X50] : min_precedes(X47,X50,X48)
& ( ? [X49] : min_precedes(X49,X47,X48)
| root(X47,X48) ) ) ),
file('theBenchmark.p',sos_15) ).
fof(sos_16,axiom,
! [X51,X52] :
( occurrence_of(X51,X52)
=> ( arboreal(X51)
<=> atomic(X52) ) ),
file('theBenchmark.p',sos_16) ).
fof(sos_17,axiom,
! [X53,X54] :
( root(X53,X54)
=> legal(X53) ),
file('theBenchmark.p',sos_17) ).
fof(sos_18,axiom,
! [X55,X56] :
( leaf_occ(X55,X56)
<=> ? [X57] :
( leaf(X55,X57)
& subactivity_occurrence(X55,X56)
& occurrence_of(X56,X57) ) ),
file('theBenchmark.p',sos_18) ).
fof(sos_19,axiom,
! [X58,X59] :
( root_occ(X58,X59)
<=> ? [X60] :
( root(X58,X60)
& subactivity_occurrence(X58,X59)
& occurrence_of(X59,X60) ) ),
file('theBenchmark.p',sos_19) ).
fof(sos_20,axiom,
! [X61,X62] :
( earlier(X61,X62)
=> ~ earlier(X62,X61) ),
file('theBenchmark.p',sos_20) ).
fof(sos_21,axiom,
! [X63,X64] :
( precedes(X63,X64)
<=> ( legal(X64)
& earlier(X63,X64) ) ),
file('theBenchmark.p',sos_21) ).
fof(sos_22,axiom,
! [X65,X66,X67] :
( min_precedes(X65,X66,X67)
=> ~ root(X66,X67) ),
file('theBenchmark.p',sos_22) ).
fof(sos_23,axiom,
! [X68,X69,X70] :
( min_precedes(X68,X69,X70)
=> ? [X71] :
( min_precedes(X71,X69,X70)
& root(X71,X70) ) ),
file('theBenchmark.p',sos_23) ).
fof(sos_24,axiom,
! [X72,X73,X74] :
( min_precedes(X72,X73,X74)
=> precedes(X72,X73) ),
file('theBenchmark.p',sos_24) ).
fof(sos_25,axiom,
! [X75,X76,X77] :
( next_subocc(X75,X76,X77)
=> ( arboreal(X76)
& arboreal(X75) ) ),
file('theBenchmark.p',sos_25) ).
fof(sos_26,axiom,
! [X78,X79,X80] :
( next_subocc(X78,X79,X80)
<=> ( ~ ? [X81] :
( min_precedes(X81,X79,X80)
& min_precedes(X78,X81,X80) )
& min_precedes(X78,X79,X80) ) ),
file('theBenchmark.p',sos_26) ).
fof(sos_27,axiom,
! [X82,X83,X84,X85] :
( ( subactivity_occurrence(X83,X85)
& occurrence_of(X85,X84)
& min_precedes(X82,X83,X84) )
=> subactivity_occurrence(X82,X85) ),
file('theBenchmark.p',sos_27) ).
fof(sos_28,axiom,
! [X86,X87,X88,X89] :
( ( leaf_occ(X87,X88)
& leaf_occ(X86,X88)
& ~ atomic(X89)
& occurrence_of(X88,X89) )
=> X86 = X87 ),
file('theBenchmark.p',sos_28) ).
fof(sos_29,axiom,
! [X90,X91,X92,X93] :
( ( root_occ(X91,X92)
& root_occ(X90,X92)
& occurrence_of(X92,X93) )
=> X90 = X91 ),
file('theBenchmark.p',sos_29) ).
fof(sos_30,axiom,
! [X94,X95,X96] :
( ( earlier(X95,X96)
& earlier(X94,X95) )
=> earlier(X94,X96) ),
file('theBenchmark.p',sos_30) ).
fof(sos_31,axiom,
! [X97,X98,X99,X100] :
( ( precedes(X98,X99)
& min_precedes(X97,X99,X100)
& min_precedes(X97,X98,X100) )
=> min_precedes(X98,X99,X100) ),
file('theBenchmark.p',sos_31) ).
fof(sos_32,axiom,
! [X101] :
( occurrence_of(X101,tptp0)
=> ? [X102,X103,X104] :
( leaf_occ(X104,X101)
& next_subocc(X103,X104,tptp0)
& ( occurrence_of(X104,tptp2)
| occurrence_of(X104,tptp1) )
& next_subocc(X102,X103,tptp0)
& occurrence_of(X103,tptp4)
& root_occ(X102,X101)
& occurrence_of(X102,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,
! [X105] :
( occurrence_of(X105,tptp0)
=> ? [X106,X107] :
( ( occurrence_of(X107,tptp2)
=> ~ ? [X109] :
( min_precedes(X106,X109,tptp0)
& occurrence_of(X109,tptp1) ) )
& ( occurrence_of(X107,tptp1)
=> ~ ? [X108] :
( min_precedes(X106,X108,tptp0)
& occurrence_of(X108,tptp2) ) )
& leaf_occ(X107,X105) ) ),
file('theBenchmark.p',goals) ).
fof(f_1_1,plain,
! [X0,X1] :
( ? [X2] :
( subactivity_occurrence(X2,X1)
& root(X2,X0) )
| atomic(X0)
| ~ occurrence_of(X1,X0) ),
inference(fof_nnf,[status(thm)],[sos]) ).
fof(f_1_2,plain,
! [U_2,U_1] :
( ? [U_0] :
( subactivity_occurrence(U_0,U_1)
& root(U_0,U_2) )
| atomic(U_2)
| ~ occurrence_of(U_1,U_2) ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
fof(f_1_3,plain,
! [U_2,U_1] :
( ( subactivity_occurrence(sK1(U_2,U_1),U_1)
& root(sK1(U_2,U_1),U_2) )
| atomic(U_2)
| ~ occurrence_of(U_1,U_2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_0,sK1(U_2,U_1))],[f_1_2]) ).
cnf(f_1_4,plain,
( root(sK1(U_2,U_1),U_2)
| atomic(U_2)
| ~ occurrence_of(U_1,U_2) ),
inference(clausify,[status(thm)],[f_1_3]) ).
cnf(f_1_5,plain,
( subactivity_occurrence(sK1(U_2,U_1),U_1)
| atomic(U_2)
| ~ occurrence_of(U_1,U_2) ),
inference(clausify,[status(thm)],[f_1_3]) ).
fof(f_2_1,plain,
! [X3,X4,X5,X6,X7] :
( min_precedes(X5,X7,X3)
| X5 = X7
| ~ min_precedes(X6,X5,X3)
| ~ subactivity_occurrence(X5,X4)
| ~ leaf_occ(X7,X4)
| ~ root_occ(X6,X4)
| ~ occurrence_of(X4,X3) ),
inference(fof_nnf,[status(thm)],[sos_01]) ).
fof(f_2_2,plain,
! [U_7,U_6,U_5,U_4,U_3] :
( min_precedes(U_5,U_3,U_7)
| U_5 = U_3
| ~ min_precedes(U_4,U_5,U_7)
| ~ subactivity_occurrence(U_5,U_6)
| ~ leaf_occ(U_3,U_6)
| ~ root_occ(U_4,U_6)
| ~ occurrence_of(U_6,U_7) ),
inference(variable_rename,[status(thm)],[f_2_1]) ).
cnf(f_2_3,plain,
( min_precedes(U_5,U_3,U_7)
| U_5 = U_3
| ~ min_precedes(U_4,U_5,U_7)
| ~ subactivity_occurrence(U_5,U_6)
| ~ leaf_occ(U_3,U_6)
| ~ root_occ(U_4,U_6)
| ~ occurrence_of(U_6,U_7) ),
inference(clausify,[status(thm)],[f_2_2]) ).
fof(f_3_1,plain,
! [X8,X9,X10,X11] :
( X11 = X10
| min_precedes(X10,X11,X8)
| ~ arboreal(X10)
| ~ leaf_occ(X11,X9)
| ~ subactivity_occurrence(X10,X9)
| ~ occurrence_of(X9,X8) ),
inference(fof_nnf,[status(thm)],[sos_02]) ).
fof(f_3_2,plain,
! [U_11,U_10,U_9,U_8] :
( U_8 = U_9
| min_precedes(U_9,U_8,U_11)
| ~ arboreal(U_9)
| ~ leaf_occ(U_8,U_10)
| ~ subactivity_occurrence(U_9,U_10)
| ~ occurrence_of(U_10,U_11) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
cnf(f_3_3,plain,
( U_8 = U_9
| min_precedes(U_9,U_8,U_11)
| ~ arboreal(U_9)
| ~ leaf_occ(U_8,U_10)
| ~ subactivity_occurrence(U_9,U_10)
| ~ occurrence_of(U_10,U_11) ),
inference(clausify,[status(thm)],[f_3_2]) ).
fof(f_4_1,plain,
! [X12,X13] :
( ( activity_occurrence(X13)
& activity(X12) )
| ~ occurrence_of(X13,X12) ),
inference(fof_nnf,[status(thm)],[sos_03]) ).
fof(f_4_2,plain,
! [U_13,U_12] :
( ( activity_occurrence(U_12)
& activity(U_13) )
| ~ occurrence_of(U_12,U_13) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
cnf(f_4_3,plain,
( activity(U_13)
| ~ occurrence_of(U_12,U_13) ),
inference(clausify,[status(thm)],[f_4_2]) ).
cnf(f_4_4,plain,
( activity_occurrence(U_12)
| ~ occurrence_of(U_12,U_13) ),
inference(clausify,[status(thm)],[f_4_2]) ).
fof(f_5_1,plain,
! [X14,X15,X16,X17] :
( X16 = X17
| min_precedes(X17,X16,X14)
| min_precedes(X16,X17,X14)
| ~ subactivity_occurrence(X17,X15)
| ~ subactivity_occurrence(X16,X15)
| ~ arboreal(X17)
| ~ arboreal(X16)
| ~ occurrence_of(X15,X14) ),
inference(fof_nnf,[status(thm)],[sos_04]) ).
fof(f_5_2,plain,
! [U_17,U_16,U_15,U_14] :
( U_15 = U_14
| min_precedes(U_14,U_15,U_17)
| min_precedes(U_15,U_14,U_17)
| ~ subactivity_occurrence(U_14,U_16)
| ~ subactivity_occurrence(U_15,U_16)
| ~ arboreal(U_14)
| ~ arboreal(U_15)
| ~ occurrence_of(U_16,U_17) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
cnf(f_5_3,plain,
( U_15 = U_14
| min_precedes(U_14,U_15,U_17)
| min_precedes(U_15,U_14,U_17)
| ~ subactivity_occurrence(U_14,U_16)
| ~ subactivity_occurrence(U_15,U_16)
| ~ arboreal(U_14)
| ~ arboreal(U_15)
| ~ occurrence_of(U_16,U_17) ),
inference(clausify,[status(thm)],[f_5_2]) ).
fof(f_6_1,plain,
! [X18,X19] :
( ? [X20] :
( atocc(X19,X20)
& subactivity(X20,X18) )
| ~ root(X19,X18) ),
inference(fof_nnf,[status(thm)],[sos_05]) ).
fof(f_6_2,plain,
! [U_20,U_19] :
( ? [U_18] :
( atocc(U_19,U_18)
& subactivity(U_18,U_20) )
| ~ root(U_19,U_20) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
fof(f_6_3,plain,
! [U_20,U_19] :
( ( atocc(U_19,sK2(U_20,U_19))
& subactivity(sK2(U_20,U_19),U_20) )
| ~ root(U_19,U_20) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_18,sK2(U_20,U_19))],[f_6_2]) ).
cnf(f_6_4,plain,
( subactivity(sK2(U_20,U_19),U_20)
| ~ root(U_19,U_20) ),
inference(clausify,[status(thm)],[f_6_3]) ).
cnf(f_6_5,plain,
( atocc(U_19,sK2(U_20,U_19))
| ~ root(U_19,U_20) ),
inference(clausify,[status(thm)],[f_6_3]) ).
fof(f_7_1,plain,
! [X21,X22,X23] :
( ? [X24] :
( subactivity_occurrence(X23,X24)
& subactivity_occurrence(X22,X24)
& occurrence_of(X24,X21) )
| ~ min_precedes(X22,X23,X21) ),
inference(fof_nnf,[status(thm)],[sos_06]) ).
fof(f_7_2,plain,
! [U_24,U_23,U_22] :
( ? [U_21] :
( subactivity_occurrence(U_22,U_21)
& subactivity_occurrence(U_23,U_21)
& occurrence_of(U_21,U_24) )
| ~ min_precedes(U_23,U_22,U_24) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
fof(f_7_3,plain,
! [U_24,U_23,U_22] :
( ( subactivity_occurrence(U_22,sK3(U_24,U_23,U_22))
& subactivity_occurrence(U_23,sK3(U_24,U_23,U_22))
& occurrence_of(sK3(U_24,U_23,U_22),U_24) )
| ~ min_precedes(U_23,U_22,U_24) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_21,sK3(U_24,U_23,U_22))],[f_7_2]) ).
cnf(f_7_4,plain,
( occurrence_of(sK3(U_24,U_23,U_22),U_24)
| ~ min_precedes(U_23,U_22,U_24) ),
inference(clausify,[status(thm)],[f_7_3]) ).
cnf(f_7_5,plain,
( subactivity_occurrence(U_23,sK3(U_24,U_23,U_22))
| ~ min_precedes(U_23,U_22,U_24) ),
inference(clausify,[status(thm)],[f_7_3]) ).
cnf(f_7_6,plain,
( subactivity_occurrence(U_22,sK3(U_24,U_23,U_22))
| ~ min_precedes(U_23,U_22,U_24) ),
inference(clausify,[status(thm)],[f_7_3]) ).
fof(f_8_1,plain,
! [X25,X26] :
( ? [X27] :
( leaf_occ(X25,X27)
& occurrence_of(X27,X26) )
| atomic(X26)
| ~ leaf(X25,X26) ),
inference(fof_nnf,[status(thm)],[sos_07]) ).
fof(f_8_2,plain,
! [U_27,U_26] :
( ? [U_25] :
( leaf_occ(U_27,U_25)
& occurrence_of(U_25,U_26) )
| atomic(U_26)
| ~ leaf(U_27,U_26) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
fof(f_8_3,plain,
! [U_27,U_26] :
( ( leaf_occ(U_27,sK4(U_27,U_26))
& occurrence_of(sK4(U_27,U_26),U_26) )
| atomic(U_26)
| ~ leaf(U_27,U_26) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_25,sK4(U_27,U_26))],[f_8_2]) ).
cnf(f_8_4,plain,
( occurrence_of(sK4(U_27,U_26),U_26)
| atomic(U_26)
| ~ leaf(U_27,U_26) ),
inference(clausify,[status(thm)],[f_8_3]) ).
cnf(f_8_5,plain,
( leaf_occ(U_27,sK4(U_27,U_26))
| atomic(U_26)
| ~ leaf(U_27,U_26) ),
inference(clausify,[status(thm)],[f_8_3]) ).
fof(f_9_1,plain,
! [X28,X29,X30] :
( X29 = X30
| ~ occurrence_of(X28,X30)
| ~ occurrence_of(X28,X29) ),
inference(fof_nnf,[status(thm)],[sos_08]) ).
fof(f_9_2,plain,
! [U_30,U_29,U_28] :
( U_29 = U_28
| ~ occurrence_of(U_30,U_28)
| ~ occurrence_of(U_30,U_29) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
cnf(f_9_3,plain,
( U_29 = U_28
| ~ occurrence_of(U_30,U_28)
| ~ occurrence_of(U_30,U_29) ),
inference(clausify,[status(thm)],[f_9_2]) ).
fof(f_10_1,plain,
! [X31,X32,X33] :
( ! [X34] : ~ min_precedes(X32,X34,X33)
| ~ leaf_occ(X32,X31)
| ~ occurrence_of(X31,X33) ),
inference(fof_nnf,[status(thm)],[sos_09]) ).
fof(f_10_2,plain,
! [U_34,U_33,U_32] :
( ! [U_31] : ~ min_precedes(U_33,U_31,U_32)
| ~ leaf_occ(U_33,U_34)
| ~ occurrence_of(U_34,U_32) ),
inference(variable_rename,[status(thm)],[f_10_1]) ).
cnf(f_10_3,plain,
( ~ min_precedes(U_33,U_31,U_32)
| ~ leaf_occ(U_33,U_34)
| ~ occurrence_of(U_34,U_32) ),
inference(clausify,[status(thm)],[f_10_2]) ).
fof(f_11_1,plain,
! [X35,X36,X37] :
( ! [X38] : ~ min_precedes(X38,X36,X37)
| ~ root_occ(X36,X35)
| ~ occurrence_of(X35,X37) ),
inference(fof_nnf,[status(thm)],[sos_10]) ).
fof(f_11_2,plain,
! [U_38,U_37,U_36] :
( ! [U_35] : ~ min_precedes(U_35,U_37,U_36)
| ~ root_occ(U_37,U_38)
| ~ occurrence_of(U_38,U_36) ),
inference(variable_rename,[status(thm)],[f_11_1]) ).
cnf(f_11_3,plain,
( ~ min_precedes(U_35,U_37,U_36)
| ~ root_occ(U_37,U_38)
| ~ occurrence_of(U_38,U_36) ),
inference(clausify,[status(thm)],[f_11_2]) ).
fof(f_12_1,plain,
! [X39,X40] :
( ( activity_occurrence(X40)
& activity_occurrence(X39) )
| ~ subactivity_occurrence(X39,X40) ),
inference(fof_nnf,[status(thm)],[sos_11]) ).
fof(f_12_2,plain,
! [U_40,U_39] :
( ( activity_occurrence(U_39)
& activity_occurrence(U_40) )
| ~ subactivity_occurrence(U_40,U_39) ),
inference(variable_rename,[status(thm)],[f_12_1]) ).
cnf(f_12_3,plain,
( activity_occurrence(U_40)
| ~ subactivity_occurrence(U_40,U_39) ),
inference(clausify,[status(thm)],[f_12_2]) ).
cnf(f_12_4,plain,
( activity_occurrence(U_39)
| ~ subactivity_occurrence(U_40,U_39) ),
inference(clausify,[status(thm)],[f_12_2]) ).
fof(f_13_1,plain,
! [X41] :
( ? [X42] :
( occurrence_of(X41,X42)
& activity(X42) )
| ~ activity_occurrence(X41) ),
inference(fof_nnf,[status(thm)],[sos_12]) ).
fof(f_13_2,plain,
! [U_42] :
( ? [U_41] :
( occurrence_of(U_42,U_41)
& activity(U_41) )
| ~ activity_occurrence(U_42) ),
inference(variable_rename,[status(thm)],[f_13_1]) ).
fof(f_13_3,plain,
! [U_42] :
( ( occurrence_of(U_42,sK5(U_42))
& activity(sK5(U_42)) )
| ~ activity_occurrence(U_42) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_41,sK5(U_42))],[f_13_2]) ).
cnf(f_13_4,plain,
( activity(sK5(U_42))
| ~ activity_occurrence(U_42) ),
inference(clausify,[status(thm)],[f_13_3]) ).
cnf(f_13_5,plain,
( occurrence_of(U_42,sK5(U_42))
| ~ activity_occurrence(U_42) ),
inference(clausify,[status(thm)],[f_13_3]) ).
fof(f_14_1,plain,
! [X43] :
( arboreal(X43)
| ~ legal(X43) ),
inference(fof_nnf,[status(thm)],[sos_13]) ).
fof(f_14_2,plain,
! [U_43] :
( arboreal(U_43)
| ~ legal(U_43) ),
inference(variable_rename,[status(thm)],[f_14_1]) ).
cnf(f_14_3,plain,
( arboreal(U_43)
| ~ legal(U_43) ),
inference(clausify,[status(thm)],[f_14_2]) ).
fof(f_15_1,plain,
! [X44,X45] :
( ( atocc(X44,X45)
| ! [X46] :
( ~ occurrence_of(X44,X46)
| ~ atomic(X46)
| ~ subactivity(X45,X46) ) )
& ( ? [X46] :
( occurrence_of(X44,X46)
& atomic(X46)
& subactivity(X45,X46) )
| ~ atocc(X44,X45) ) ),
inference(fof_nnf,[status(thm)],[sos_14]) ).
fof(f_15_2,plain,
! [U_47,U_46] :
( ( atocc(U_47,U_46)
| ! [U_45] :
( ~ occurrence_of(U_47,U_45)
| ~ atomic(U_45)
| ~ subactivity(U_46,U_45) ) )
& ( ? [U_44] :
( occurrence_of(U_47,U_44)
& atomic(U_44)
& subactivity(U_46,U_44) )
| ~ atocc(U_47,U_46) ) ),
inference(variable_rename,[status(thm)],[f_15_1]) ).
fof(f_15_3,plain,
( ! [U_51,U_49] :
( atocc(U_51,U_49)
| ! [U_45] :
( ~ occurrence_of(U_51,U_45)
| ~ atomic(U_45)
| ~ subactivity(U_49,U_45) ) )
& ! [U_50,U_48] :
( ? [U_44] :
( occurrence_of(U_50,U_44)
& atomic(U_44)
& subactivity(U_48,U_44) )
| ~ atocc(U_50,U_48) ) ),
inference(miniscope,[status(thm)],[f_15_2]) ).
fof(f_15_4,plain,
( ! [U_51,U_49] :
( atocc(U_51,U_49)
| ! [U_45] :
( ~ occurrence_of(U_51,U_45)
| ~ atomic(U_45)
| ~ subactivity(U_49,U_45) ) )
& ! [U_50,U_48] :
( ( occurrence_of(U_50,sK6(U_50,U_48))
& atomic(sK6(U_50,U_48))
& subactivity(U_48,sK6(U_50,U_48)) )
| ~ atocc(U_50,U_48) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_44,sK6(U_50,U_48))],[f_15_3]) ).
cnf(f_15_5,plain,
( subactivity(U_48,sK6(U_50,U_48))
| ~ atocc(U_50,U_48) ),
inference(clausify,[status(thm)],[f_15_4]) ).
cnf(f_15_6,plain,
( atomic(sK6(U_50,U_48))
| ~ atocc(U_50,U_48) ),
inference(clausify,[status(thm)],[f_15_4]) ).
cnf(f_15_7,plain,
( occurrence_of(U_50,sK6(U_50,U_48))
| ~ atocc(U_50,U_48) ),
inference(clausify,[status(thm)],[f_15_4]) ).
cnf(f_15_8,plain,
( atocc(U_51,U_49)
| ~ occurrence_of(U_51,U_45)
| ~ atomic(U_45)
| ~ subactivity(U_49,U_45) ),
inference(clausify,[status(thm)],[f_15_4]) ).
fof(f_16_1,plain,
! [X47,X48] :
( ( leaf(X47,X48)
| ? [X50] : min_precedes(X47,X50,X48)
| ( ! [X49] : ~ min_precedes(X49,X47,X48)
& ~ root(X47,X48) ) )
& ( ( ! [X50] : ~ min_precedes(X47,X50,X48)
& ( ? [X49] : min_precedes(X49,X47,X48)
| root(X47,X48) ) )
| ~ leaf(X47,X48) ) ),
inference(fof_nnf,[status(thm)],[sos_15]) ).
fof(f_16_2,plain,
! [U_57,U_56] :
( ( leaf(U_57,U_56)
| ? [U_55] : min_precedes(U_57,U_55,U_56)
| ( ! [U_54] : ~ min_precedes(U_54,U_57,U_56)
& ~ root(U_57,U_56) ) )
& ( ( ! [U_53] : ~ min_precedes(U_57,U_53,U_56)
& ( ? [U_52] : min_precedes(U_52,U_57,U_56)
| root(U_57,U_56) ) )
| ~ leaf(U_57,U_56) ) ),
inference(variable_rename,[status(thm)],[f_16_1]) ).
fof(f_16_3,plain,
( ! [U_61,U_59] :
( leaf(U_61,U_59)
| ? [U_55] : min_precedes(U_61,U_55,U_59)
| ( ! [U_54] : ~ min_precedes(U_54,U_61,U_59)
& ~ root(U_61,U_59) ) )
& ! [U_60,U_58] :
( ( ! [U_53] : ~ min_precedes(U_60,U_53,U_58)
& ( ? [U_52] : min_precedes(U_52,U_60,U_58)
| root(U_60,U_58) ) )
| ~ leaf(U_60,U_58) ) ),
inference(miniscope,[status(thm)],[f_16_2]) ).
fof(f_16_4,plain,
( ! [U_61,U_59] :
( leaf(U_61,U_59)
| ? [U_55] : min_precedes(U_61,U_55,U_59)
| ( ! [U_54] : ~ min_precedes(U_54,U_61,U_59)
& ~ root(U_61,U_59) ) )
& ! [U_60,U_58] :
( ( ! [U_53] : ~ min_precedes(U_60,U_53,U_58)
& ( min_precedes(sK7(U_60,U_58),U_60,U_58)
| root(U_60,U_58) ) )
| ~ leaf(U_60,U_58) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_52,sK7(U_60,U_58))],[f_16_3]) ).
fof(f_16_5,plain,
( ! [U_61,U_59] :
( leaf(U_61,U_59)
| min_precedes(U_61,sK8(U_61,U_59),U_59)
| ( ! [U_54] : ~ min_precedes(U_54,U_61,U_59)
& ~ root(U_61,U_59) ) )
& ! [U_60,U_58] :
( ( ! [U_53] : ~ min_precedes(U_60,U_53,U_58)
& ( min_precedes(sK7(U_60,U_58),U_60,U_58)
| root(U_60,U_58) ) )
| ~ leaf(U_60,U_58) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_55,sK8(U_61,U_59))],[f_16_4]) ).
cnf(f_16_6,plain,
( min_precedes(sK7(U_60,U_58),U_60,U_58)
| root(U_60,U_58)
| ~ leaf(U_60,U_58) ),
inference(clausify,[status(thm)],[f_16_5]) ).
cnf(f_16_7,plain,
( ~ min_precedes(U_60,U_53,U_58)
| ~ leaf(U_60,U_58) ),
inference(clausify,[status(thm)],[f_16_5]) ).
cnf(f_16_8,plain,
( ~ root(U_61,U_59)
| min_precedes(U_61,sK8(U_61,U_59),U_59)
| leaf(U_61,U_59) ),
inference(clausify,[status(thm)],[f_16_5]) ).
cnf(f_16_9,plain,
( ~ min_precedes(U_54,U_61,U_59)
| min_precedes(U_61,sK8(U_61,U_59),U_59)
| leaf(U_61,U_59) ),
inference(clausify,[status(thm)],[f_16_5]) ).
fof(f_17_1,plain,
! [X51,X52] :
( ( ( arboreal(X51)
| ~ atomic(X52) )
& ( atomic(X52)
| ~ arboreal(X51) ) )
| ~ occurrence_of(X51,X52) ),
inference(fof_nnf,[status(thm)],[sos_16]) ).
fof(f_17_2,plain,
! [U_63,U_62] :
( ( ( arboreal(U_63)
| ~ atomic(U_62) )
& ( atomic(U_62)
| ~ arboreal(U_63) ) )
| ~ occurrence_of(U_63,U_62) ),
inference(variable_rename,[status(thm)],[f_17_1]) ).
cnf(f_17_3,plain,
( atomic(U_62)
| ~ arboreal(U_63)
| ~ occurrence_of(U_63,U_62) ),
inference(clausify,[status(thm)],[f_17_2]) ).
cnf(f_17_4,plain,
( arboreal(U_63)
| ~ atomic(U_62)
| ~ occurrence_of(U_63,U_62) ),
inference(clausify,[status(thm)],[f_17_2]) ).
fof(f_18_1,plain,
! [X53,X54] :
( legal(X53)
| ~ root(X53,X54) ),
inference(fof_nnf,[status(thm)],[sos_17]) ).
fof(f_18_2,plain,
! [U_65,U_64] :
( legal(U_65)
| ~ root(U_65,U_64) ),
inference(variable_rename,[status(thm)],[f_18_1]) ).
fof(f_18_3,plain,
! [U_65] :
( ! [U_64] : ~ root(U_65,U_64)
| legal(U_65) ),
inference(miniscope,[status(thm)],[f_18_2]) ).
cnf(f_18_4,plain,
( ~ root(U_65,U_64)
| legal(U_65) ),
inference(clausify,[status(thm)],[f_18_3]) ).
fof(f_19_1,plain,
! [X55,X56] :
( ( leaf_occ(X55,X56)
| ! [X57] :
( ~ leaf(X55,X57)
| ~ subactivity_occurrence(X55,X56)
| ~ occurrence_of(X56,X57) ) )
& ( ? [X57] :
( leaf(X55,X57)
& subactivity_occurrence(X55,X56)
& occurrence_of(X56,X57) )
| ~ leaf_occ(X55,X56) ) ),
inference(fof_nnf,[status(thm)],[sos_18]) ).
fof(f_19_2,plain,
! [U_69,U_68] :
( ( leaf_occ(U_69,U_68)
| ! [U_67] :
( ~ leaf(U_69,U_67)
| ~ subactivity_occurrence(U_69,U_68)
| ~ occurrence_of(U_68,U_67) ) )
& ( ? [U_66] :
( leaf(U_69,U_66)
& subactivity_occurrence(U_69,U_68)
& occurrence_of(U_68,U_66) )
| ~ leaf_occ(U_69,U_68) ) ),
inference(variable_rename,[status(thm)],[f_19_1]) ).
fof(f_19_3,plain,
( ! [U_73,U_71] :
( leaf_occ(U_73,U_71)
| ! [U_67] :
( ~ leaf(U_73,U_67)
| ~ occurrence_of(U_71,U_67) )
| ~ subactivity_occurrence(U_73,U_71) )
& ! [U_72,U_70] :
( ( ? [U_66] :
( leaf(U_72,U_66)
& occurrence_of(U_70,U_66) )
& subactivity_occurrence(U_72,U_70) )
| ~ leaf_occ(U_72,U_70) ) ),
inference(miniscope,[status(thm)],[f_19_2]) ).
fof(f_19_4,plain,
( ! [U_73,U_71] :
( leaf_occ(U_73,U_71)
| ! [U_67] :
( ~ leaf(U_73,U_67)
| ~ occurrence_of(U_71,U_67) )
| ~ subactivity_occurrence(U_73,U_71) )
& ! [U_72,U_70] :
( ( leaf(U_72,sK9(U_72,U_70))
& occurrence_of(U_70,sK9(U_72,U_70))
& subactivity_occurrence(U_72,U_70) )
| ~ leaf_occ(U_72,U_70) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_66,sK9(U_72,U_70))],[f_19_3]) ).
cnf(f_19_5,plain,
( subactivity_occurrence(U_72,U_70)
| ~ leaf_occ(U_72,U_70) ),
inference(clausify,[status(thm)],[f_19_4]) ).
cnf(f_19_6,plain,
( occurrence_of(U_70,sK9(U_72,U_70))
| ~ leaf_occ(U_72,U_70) ),
inference(clausify,[status(thm)],[f_19_4]) ).
cnf(f_19_7,plain,
( leaf(U_72,sK9(U_72,U_70))
| ~ leaf_occ(U_72,U_70) ),
inference(clausify,[status(thm)],[f_19_4]) ).
cnf(f_19_8,plain,
( leaf_occ(U_73,U_71)
| ~ leaf(U_73,U_67)
| ~ occurrence_of(U_71,U_67)
| ~ subactivity_occurrence(U_73,U_71) ),
inference(clausify,[status(thm)],[f_19_4]) ).
fof(f_20_1,plain,
! [X58,X59] :
( ( root_occ(X58,X59)
| ! [X60] :
( ~ root(X58,X60)
| ~ subactivity_occurrence(X58,X59)
| ~ occurrence_of(X59,X60) ) )
& ( ? [X60] :
( root(X58,X60)
& subactivity_occurrence(X58,X59)
& occurrence_of(X59,X60) )
| ~ root_occ(X58,X59) ) ),
inference(fof_nnf,[status(thm)],[sos_19]) ).
fof(f_20_2,plain,
! [U_77,U_76] :
( ( root_occ(U_77,U_76)
| ! [U_75] :
( ~ root(U_77,U_75)
| ~ subactivity_occurrence(U_77,U_76)
| ~ occurrence_of(U_76,U_75) ) )
& ( ? [U_74] :
( root(U_77,U_74)
& subactivity_occurrence(U_77,U_76)
& occurrence_of(U_76,U_74) )
| ~ root_occ(U_77,U_76) ) ),
inference(variable_rename,[status(thm)],[f_20_1]) ).
fof(f_20_3,plain,
( ! [U_81,U_79] :
( root_occ(U_81,U_79)
| ! [U_75] :
( ~ root(U_81,U_75)
| ~ occurrence_of(U_79,U_75) )
| ~ subactivity_occurrence(U_81,U_79) )
& ! [U_80,U_78] :
( ( ? [U_74] :
( root(U_80,U_74)
& occurrence_of(U_78,U_74) )
& subactivity_occurrence(U_80,U_78) )
| ~ root_occ(U_80,U_78) ) ),
inference(miniscope,[status(thm)],[f_20_2]) ).
fof(f_20_4,plain,
( ! [U_81,U_79] :
( root_occ(U_81,U_79)
| ! [U_75] :
( ~ root(U_81,U_75)
| ~ occurrence_of(U_79,U_75) )
| ~ subactivity_occurrence(U_81,U_79) )
& ! [U_80,U_78] :
( ( root(U_80,sK10(U_80,U_78))
& occurrence_of(U_78,sK10(U_80,U_78))
& subactivity_occurrence(U_80,U_78) )
| ~ root_occ(U_80,U_78) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_74,sK10(U_80,U_78))],[f_20_3]) ).
cnf(f_20_5,plain,
( subactivity_occurrence(U_80,U_78)
| ~ root_occ(U_80,U_78) ),
inference(clausify,[status(thm)],[f_20_4]) ).
cnf(f_20_6,plain,
( occurrence_of(U_78,sK10(U_80,U_78))
| ~ root_occ(U_80,U_78) ),
inference(clausify,[status(thm)],[f_20_4]) ).
cnf(f_20_7,plain,
( root(U_80,sK10(U_80,U_78))
| ~ root_occ(U_80,U_78) ),
inference(clausify,[status(thm)],[f_20_4]) ).
cnf(f_20_8,plain,
( root_occ(U_81,U_79)
| ~ root(U_81,U_75)
| ~ occurrence_of(U_79,U_75)
| ~ subactivity_occurrence(U_81,U_79) ),
inference(clausify,[status(thm)],[f_20_4]) ).
fof(f_21_1,plain,
! [X61,X62] :
( ~ earlier(X62,X61)
| ~ earlier(X61,X62) ),
inference(fof_nnf,[status(thm)],[sos_20]) ).
fof(f_21_2,plain,
! [U_83,U_82] :
( ~ earlier(U_82,U_83)
| ~ earlier(U_83,U_82) ),
inference(variable_rename,[status(thm)],[f_21_1]) ).
cnf(f_21_3,plain,
( ~ earlier(U_82,U_83)
| ~ earlier(U_83,U_82) ),
inference(clausify,[status(thm)],[f_21_2]) ).
fof(f_22_1,plain,
! [X63,X64] :
( ( precedes(X63,X64)
| ~ legal(X64)
| ~ earlier(X63,X64) )
& ( ( legal(X64)
& earlier(X63,X64) )
| ~ precedes(X63,X64) ) ),
inference(fof_nnf,[status(thm)],[sos_21]) ).
fof(f_22_2,plain,
! [U_85,U_84] :
( ( precedes(U_85,U_84)
| ~ legal(U_84)
| ~ earlier(U_85,U_84) )
& ( ( legal(U_84)
& earlier(U_85,U_84) )
| ~ precedes(U_85,U_84) ) ),
inference(variable_rename,[status(thm)],[f_22_1]) ).
fof(f_22_3,plain,
( ! [U_89,U_87] :
( precedes(U_89,U_87)
| ~ legal(U_87)
| ~ earlier(U_89,U_87) )
& ! [U_88,U_86] :
( ( legal(U_86)
& earlier(U_88,U_86) )
| ~ precedes(U_88,U_86) ) ),
inference(miniscope,[status(thm)],[f_22_2]) ).
cnf(f_22_4,plain,
( earlier(U_88,U_86)
| ~ precedes(U_88,U_86) ),
inference(clausify,[status(thm)],[f_22_3]) ).
cnf(f_22_5,plain,
( legal(U_86)
| ~ precedes(U_88,U_86) ),
inference(clausify,[status(thm)],[f_22_3]) ).
cnf(f_22_6,plain,
( precedes(U_89,U_87)
| ~ legal(U_87)
| ~ earlier(U_89,U_87) ),
inference(clausify,[status(thm)],[f_22_3]) ).
fof(f_23_1,plain,
! [X65,X66,X67] :
( ~ root(X66,X67)
| ~ min_precedes(X65,X66,X67) ),
inference(fof_nnf,[status(thm)],[sos_22]) ).
fof(f_23_2,plain,
! [U_92,U_91,U_90] :
( ~ root(U_91,U_90)
| ~ min_precedes(U_92,U_91,U_90) ),
inference(variable_rename,[status(thm)],[f_23_1]) ).
cnf(f_23_3,plain,
( ~ root(U_91,U_90)
| ~ min_precedes(U_92,U_91,U_90) ),
inference(clausify,[status(thm)],[f_23_2]) ).
fof(f_24_1,plain,
! [X68,X69,X70] :
( ? [X71] :
( min_precedes(X71,X69,X70)
& root(X71,X70) )
| ~ min_precedes(X68,X69,X70) ),
inference(fof_nnf,[status(thm)],[sos_23]) ).
fof(f_24_2,plain,
! [U_96,U_95,U_94] :
( ? [U_93] :
( min_precedes(U_93,U_95,U_94)
& root(U_93,U_94) )
| ~ min_precedes(U_96,U_95,U_94) ),
inference(variable_rename,[status(thm)],[f_24_1]) ).
fof(f_24_3,plain,
! [U_96,U_95,U_94] :
( ( min_precedes(sK11(U_96,U_95,U_94),U_95,U_94)
& root(sK11(U_96,U_95,U_94),U_94) )
| ~ min_precedes(U_96,U_95,U_94) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_93,sK11(U_96,U_95,U_94))],[f_24_2]) ).
cnf(f_24_4,plain,
( root(sK11(U_96,U_95,U_94),U_94)
| ~ min_precedes(U_96,U_95,U_94) ),
inference(clausify,[status(thm)],[f_24_3]) ).
cnf(f_24_5,plain,
( min_precedes(sK11(U_96,U_95,U_94),U_95,U_94)
| ~ min_precedes(U_96,U_95,U_94) ),
inference(clausify,[status(thm)],[f_24_3]) ).
fof(f_25_1,plain,
! [X72,X73,X74] :
( precedes(X72,X73)
| ~ min_precedes(X72,X73,X74) ),
inference(fof_nnf,[status(thm)],[sos_24]) ).
fof(f_25_2,plain,
! [U_99,U_98,U_97] :
( precedes(U_99,U_98)
| ~ min_precedes(U_99,U_98,U_97) ),
inference(variable_rename,[status(thm)],[f_25_1]) ).
fof(f_25_3,plain,
! [U_99,U_98] :
( ! [U_97] : ~ min_precedes(U_99,U_98,U_97)
| precedes(U_99,U_98) ),
inference(miniscope,[status(thm)],[f_25_2]) ).
cnf(f_25_4,plain,
( ~ min_precedes(U_99,U_98,U_97)
| precedes(U_99,U_98) ),
inference(clausify,[status(thm)],[f_25_3]) ).
fof(f_26_1,plain,
! [X75,X76,X77] :
( ( arboreal(X76)
& arboreal(X75) )
| ~ next_subocc(X75,X76,X77) ),
inference(fof_nnf,[status(thm)],[sos_25]) ).
fof(f_26_2,plain,
! [U_102,U_101,U_100] :
( ( arboreal(U_101)
& arboreal(U_102) )
| ~ next_subocc(U_102,U_101,U_100) ),
inference(variable_rename,[status(thm)],[f_26_1]) ).
fof(f_26_3,plain,
! [U_102,U_101] :
( ! [U_100] : ~ next_subocc(U_102,U_101,U_100)
| ( arboreal(U_101)
& arboreal(U_102) ) ),
inference(miniscope,[status(thm)],[f_26_2]) ).
cnf(f_26_4,plain,
( arboreal(U_102)
| ~ next_subocc(U_102,U_101,U_100) ),
inference(clausify,[status(thm)],[f_26_3]) ).
cnf(f_26_5,plain,
( arboreal(U_101)
| ~ next_subocc(U_102,U_101,U_100) ),
inference(clausify,[status(thm)],[f_26_3]) ).
fof(f_27_1,plain,
! [X78,X79,X80] :
( ( next_subocc(X78,X79,X80)
| ? [X81] :
( min_precedes(X81,X79,X80)
& min_precedes(X78,X81,X80) )
| ~ min_precedes(X78,X79,X80) )
& ( ( ! [X81] :
( ~ min_precedes(X81,X79,X80)
| ~ min_precedes(X78,X81,X80) )
& min_precedes(X78,X79,X80) )
| ~ next_subocc(X78,X79,X80) ) ),
inference(fof_nnf,[status(thm)],[sos_26]) ).
fof(f_27_2,plain,
! [U_107,U_106,U_105] :
( ( next_subocc(U_107,U_106,U_105)
| ? [U_104] :
( min_precedes(U_104,U_106,U_105)
& min_precedes(U_107,U_104,U_105) )
| ~ min_precedes(U_107,U_106,U_105) )
& ( ( ! [U_103] :
( ~ min_precedes(U_103,U_106,U_105)
| ~ min_precedes(U_107,U_103,U_105) )
& min_precedes(U_107,U_106,U_105) )
| ~ next_subocc(U_107,U_106,U_105) ) ),
inference(variable_rename,[status(thm)],[f_27_1]) ).
fof(f_27_3,plain,
( ! [U_113,U_111,U_109] :
( next_subocc(U_113,U_111,U_109)
| ? [U_104] :
( min_precedes(U_104,U_111,U_109)
& min_precedes(U_113,U_104,U_109) )
| ~ min_precedes(U_113,U_111,U_109) )
& ! [U_112,U_110,U_108] :
( ( ! [U_103] :
( ~ min_precedes(U_103,U_110,U_108)
| ~ min_precedes(U_112,U_103,U_108) )
& min_precedes(U_112,U_110,U_108) )
| ~ next_subocc(U_112,U_110,U_108) ) ),
inference(miniscope,[status(thm)],[f_27_2]) ).
fof(f_27_4,plain,
( ! [U_113,U_111,U_109] :
( next_subocc(U_113,U_111,U_109)
| ( min_precedes(sK12(U_113,U_111,U_109),U_111,U_109)
& min_precedes(U_113,sK12(U_113,U_111,U_109),U_109) )
| ~ min_precedes(U_113,U_111,U_109) )
& ! [U_112,U_110,U_108] :
( ( ! [U_103] :
( ~ min_precedes(U_103,U_110,U_108)
| ~ min_precedes(U_112,U_103,U_108) )
& min_precedes(U_112,U_110,U_108) )
| ~ next_subocc(U_112,U_110,U_108) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(U_104,sK12(U_113,U_111,U_109))],[f_27_3]) ).
cnf(f_27_5,plain,
( min_precedes(U_112,U_110,U_108)
| ~ next_subocc(U_112,U_110,U_108) ),
inference(clausify,[status(thm)],[f_27_4]) ).
cnf(f_27_6,plain,
( ~ min_precedes(U_103,U_110,U_108)
| ~ min_precedes(U_112,U_103,U_108)
| ~ next_subocc(U_112,U_110,U_108) ),
inference(clausify,[status(thm)],[f_27_4]) ).
cnf(f_27_7,plain,
( min_precedes(U_113,sK12(U_113,U_111,U_109),U_109)
| ~ min_precedes(U_113,U_111,U_109)
| next_subocc(U_113,U_111,U_109) ),
inference(clausify,[status(thm)],[f_27_4]) ).
cnf(f_27_8,plain,
( min_precedes(sK12(U_113,U_111,U_109),U_111,U_109)
| ~ min_precedes(U_113,U_111,U_109)
| next_subocc(U_113,U_111,U_109) ),
inference(clausify,[status(thm)],[f_27_4]) ).
fof(f_28_1,plain,
! [X82,X83,X84,X85] :
( subactivity_occurrence(X82,X85)
| ~ subactivity_occurrence(X83,X85)
| ~ occurrence_of(X85,X84)
| ~ min_precedes(X82,X83,X84) ),
inference(fof_nnf,[status(thm)],[sos_27]) ).
fof(f_28_2,plain,
! [U_117,U_116,U_115,U_114] :
( subactivity_occurrence(U_117,U_114)
| ~ subactivity_occurrence(U_116,U_114)
| ~ occurrence_of(U_114,U_115)
| ~ min_precedes(U_117,U_116,U_115) ),
inference(variable_rename,[status(thm)],[f_28_1]) ).
cnf(f_28_3,plain,
( subactivity_occurrence(U_117,U_114)
| ~ subactivity_occurrence(U_116,U_114)
| ~ occurrence_of(U_114,U_115)
| ~ min_precedes(U_117,U_116,U_115) ),
inference(clausify,[status(thm)],[f_28_2]) ).
fof(f_29_1,plain,
! [X86,X87,X88,X89] :
( X86 = X87
| ~ leaf_occ(X87,X88)
| ~ leaf_occ(X86,X88)
| atomic(X89)
| ~ occurrence_of(X88,X89) ),
inference(fof_nnf,[status(thm)],[sos_28]) ).
fof(f_29_2,plain,
! [U_121,U_120,U_119,U_118] :
( U_121 = U_120
| ~ leaf_occ(U_120,U_119)
| ~ leaf_occ(U_121,U_119)
| atomic(U_118)
| ~ occurrence_of(U_119,U_118) ),
inference(variable_rename,[status(thm)],[f_29_1]) ).
fof(f_29_3,plain,
! [U_121,U_120] :
( ! [U_119] :
( ! [U_118] :
( atomic(U_118)
| ~ occurrence_of(U_119,U_118) )
| ~ leaf_occ(U_120,U_119)
| ~ leaf_occ(U_121,U_119) )
| U_121 = U_120 ),
inference(miniscope,[status(thm)],[f_29_2]) ).
cnf(f_29_4,plain,
( atomic(U_118)
| ~ occurrence_of(U_119,U_118)
| ~ leaf_occ(U_120,U_119)
| ~ leaf_occ(U_121,U_119)
| U_121 = U_120 ),
inference(clausify,[status(thm)],[f_29_3]) ).
fof(f_30_1,plain,
! [X90,X91,X92,X93] :
( X90 = X91
| ~ root_occ(X91,X92)
| ~ root_occ(X90,X92)
| ~ occurrence_of(X92,X93) ),
inference(fof_nnf,[status(thm)],[sos_29]) ).
fof(f_30_2,plain,
! [U_125,U_124,U_123,U_122] :
( U_125 = U_124
| ~ root_occ(U_124,U_123)
| ~ root_occ(U_125,U_123)
| ~ occurrence_of(U_123,U_122) ),
inference(variable_rename,[status(thm)],[f_30_1]) ).
fof(f_30_3,plain,
! [U_125,U_124] :
( ! [U_123] :
( ! [U_122] : ~ occurrence_of(U_123,U_122)
| ~ root_occ(U_124,U_123)
| ~ root_occ(U_125,U_123) )
| U_125 = U_124 ),
inference(miniscope,[status(thm)],[f_30_2]) ).
cnf(f_30_4,plain,
( ~ occurrence_of(U_123,U_122)
| ~ root_occ(U_124,U_123)
| ~ root_occ(U_125,U_123)
| U_125 = U_124 ),
inference(clausify,[status(thm)],[f_30_3]) ).
fof(f_31_1,plain,
! [X94,X95,X96] :
( earlier(X94,X96)
| ~ earlier(X95,X96)
| ~ earlier(X94,X95) ),
inference(fof_nnf,[status(thm)],[sos_30]) ).
fof(f_31_2,plain,
! [U_128,U_127,U_126] :
( earlier(U_128,U_126)
| ~ earlier(U_127,U_126)
| ~ earlier(U_128,U_127) ),
inference(variable_rename,[status(thm)],[f_31_1]) ).
cnf(f_31_3,plain,
( earlier(U_128,U_126)
| ~ earlier(U_127,U_126)
| ~ earlier(U_128,U_127) ),
inference(clausify,[status(thm)],[f_31_2]) ).
fof(f_32_1,plain,
! [X97,X98,X99,X100] :
( min_precedes(X98,X99,X100)
| ~ precedes(X98,X99)
| ~ min_precedes(X97,X99,X100)
| ~ min_precedes(X97,X98,X100) ),
inference(fof_nnf,[status(thm)],[sos_31]) ).
fof(f_32_2,plain,
! [U_132,U_131,U_130,U_129] :
( min_precedes(U_131,U_130,U_129)
| ~ precedes(U_131,U_130)
| ~ min_precedes(U_132,U_130,U_129)
| ~ min_precedes(U_132,U_131,U_129) ),
inference(variable_rename,[status(thm)],[f_32_1]) ).
cnf(f_32_3,plain,
( min_precedes(U_131,U_130,U_129)
| ~ precedes(U_131,U_130)
| ~ min_precedes(U_132,U_130,U_129)
| ~ min_precedes(U_132,U_131,U_129) ),
inference(clausify,[status(thm)],[f_32_2]) ).
fof(f_33_1,plain,
! [X101] :
( ? [X102,X103,X104] :
( leaf_occ(X104,X101)
& next_subocc(X103,X104,tptp0)
& ( occurrence_of(X104,tptp2)
| occurrence_of(X104,tptp1) )
& next_subocc(X102,X103,tptp0)
& occurrence_of(X103,tptp4)
& root_occ(X102,X101)
& occurrence_of(X102,tptp3) )
| ~ occurrence_of(X101,tptp0) ),
inference(fof_nnf,[status(thm)],[sos_32]) ).
fof(f_33_2,plain,
! [U_136] :
( ? [U_135,U_134,U_133] :
( leaf_occ(U_133,U_136)
& next_subocc(U_134,U_133,tptp0)
& ( occurrence_of(U_133,tptp2)
| occurrence_of(U_133,tptp1) )
& next_subocc(U_135,U_134,tptp0)
& occurrence_of(U_134,tptp4)
& root_occ(U_135,U_136)
& occurrence_of(U_135,tptp3) )
| ~ occurrence_of(U_136,tptp0) ),
inference(variable_rename,[status(thm)],[f_33_1]) ).
fof(f_33_3,plain,
! [U_136] :
( ? [U_135] :
( ? [U_134] :
( ? [U_133] :
( leaf_occ(U_133,U_136)
& next_subocc(U_134,U_133,tptp0)
& ( occurrence_of(U_133,tptp2)
| occurrence_of(U_133,tptp1) ) )
& next_subocc(U_135,U_134,tptp0)
& occurrence_of(U_134,tptp4) )
& root_occ(U_135,U_136)
& occurrence_of(U_135,tptp3) )
| ~ occurrence_of(U_136,tptp0) ),
inference(miniscope,[status(thm)],[f_33_2]) ).
fof(f_33_4,plain,
! [U_136] :
( ( ? [U_134] :
( ? [U_133] :
( leaf_occ(U_133,U_136)
& next_subocc(U_134,U_133,tptp0)
& ( occurrence_of(U_133,tptp2)
| occurrence_of(U_133,tptp1) ) )
& next_subocc(sK13(U_136),U_134,tptp0)
& occurrence_of(U_134,tptp4) )
& root_occ(sK13(U_136),U_136)
& occurrence_of(sK13(U_136),tptp3) )
| ~ occurrence_of(U_136,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(U_135,sK13(U_136))],[f_33_3]) ).
fof(f_33_5,plain,
! [U_136] :
( ( ? [U_133] :
( leaf_occ(U_133,U_136)
& next_subocc(sK14(U_136),U_133,tptp0)
& ( occurrence_of(U_133,tptp2)
| occurrence_of(U_133,tptp1) ) )
& next_subocc(sK13(U_136),sK14(U_136),tptp0)
& occurrence_of(sK14(U_136),tptp4)
& root_occ(sK13(U_136),U_136)
& occurrence_of(sK13(U_136),tptp3) )
| ~ occurrence_of(U_136,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_134,sK14(U_136))],[f_33_4]) ).
fof(f_33_6,plain,
! [U_136] :
( ( leaf_occ(sK15(U_136),U_136)
& next_subocc(sK14(U_136),sK15(U_136),tptp0)
& ( occurrence_of(sK15(U_136),tptp2)
| occurrence_of(sK15(U_136),tptp1) )
& next_subocc(sK13(U_136),sK14(U_136),tptp0)
& occurrence_of(sK14(U_136),tptp4)
& root_occ(sK13(U_136),U_136)
& occurrence_of(sK13(U_136),tptp3) )
| ~ occurrence_of(U_136,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(U_133,sK15(U_136))],[f_33_5]) ).
cnf(f_33_7,plain,
( occurrence_of(sK13(U_136),tptp3)
| ~ occurrence_of(U_136,tptp0) ),
inference(clausify,[status(thm)],[f_33_6]) ).
cnf(f_33_8,plain,
( root_occ(sK13(U_136),U_136)
| ~ occurrence_of(U_136,tptp0) ),
inference(clausify,[status(thm)],[f_33_6]) ).
cnf(f_33_9,plain,
( occurrence_of(sK14(U_136),tptp4)
| ~ occurrence_of(U_136,tptp0) ),
inference(clausify,[status(thm)],[f_33_6]) ).
cnf(f_33_10,plain,
( next_subocc(sK13(U_136),sK14(U_136),tptp0)
| ~ occurrence_of(U_136,tptp0) ),
inference(clausify,[status(thm)],[f_33_6]) ).
cnf(f_33_11,plain,
( occurrence_of(sK15(U_136),tptp2)
| occurrence_of(sK15(U_136),tptp1)
| ~ occurrence_of(U_136,tptp0) ),
inference(clausify,[status(thm)],[f_33_6]) ).
cnf(f_33_12,plain,
( next_subocc(sK14(U_136),sK15(U_136),tptp0)
| ~ occurrence_of(U_136,tptp0) ),
inference(clausify,[status(thm)],[f_33_6]) ).
cnf(f_33_13,plain,
( leaf_occ(sK15(U_136),U_136)
| ~ occurrence_of(U_136,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,
~ ! [X105] :
( occurrence_of(X105,tptp0)
=> ? [X106,X107] :
( ( occurrence_of(X107,tptp2)
=> ~ ? [X109] :
( min_precedes(X106,X109,tptp0)
& occurrence_of(X109,tptp1) ) )
& ( occurrence_of(X107,tptp1)
=> ~ ? [X108] :
( min_precedes(X106,X108,tptp0)
& occurrence_of(X108,tptp2) ) )
& leaf_occ(X107,X105) ) ),
inference(negate,[status(cth)],[goals]) ).
fof(f_46_2,negated_conjecture,
? [X105] :
( ! [X106,X107] :
( ( ? [X109] :
( min_precedes(X106,X109,tptp0)
& occurrence_of(X109,tptp1) )
& occurrence_of(X107,tptp2) )
| ( ? [X108] :
( min_precedes(X106,X108,tptp0)
& occurrence_of(X108,tptp2) )
& occurrence_of(X107,tptp1) )
| ~ leaf_occ(X107,X105) )
& occurrence_of(X105,tptp0) ),
inference(fof_nnf,[status(thm)],[f_46_1]) ).
fof(f_46_3,negated_conjecture,
? [U_141] :
( ! [U_140,U_139] :
( ( ? [U_138] :
( min_precedes(U_140,U_138,tptp0)
& occurrence_of(U_138,tptp1) )
& occurrence_of(U_139,tptp2) )
| ( ? [U_137] :
( min_precedes(U_140,U_137,tptp0)
& occurrence_of(U_137,tptp2) )
& occurrence_of(U_139,tptp1) )
| ~ leaf_occ(U_139,U_141) )
& occurrence_of(U_141,tptp0) ),
inference(variable_rename,[status(thm)],[f_46_2]) ).
fof(f_46_4,negated_conjecture,
( ! [U_140,U_139] :
( ( ? [U_138] :
( min_precedes(U_140,U_138,tptp0)
& occurrence_of(U_138,tptp1) )
& occurrence_of(U_139,tptp2) )
| ( ? [U_137] :
( min_precedes(U_140,U_137,tptp0)
& occurrence_of(U_137,tptp2) )
& occurrence_of(U_139,tptp1) )
| ~ leaf_occ(U_139,sK16) )
& occurrence_of(sK16,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(U_141,sK16)],[f_46_3]) ).
fof(f_46_5,negated_conjecture,
( ! [U_140,U_139] :
( ( ? [U_138] :
( min_precedes(U_140,U_138,tptp0)
& occurrence_of(U_138,tptp1) )
& occurrence_of(U_139,tptp2) )
| ( min_precedes(U_140,sK17(U_140,U_139),tptp0)
& occurrence_of(sK17(U_140,U_139),tptp2)
& occurrence_of(U_139,tptp1) )
| ~ leaf_occ(U_139,sK16) )
& occurrence_of(sK16,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(U_137,sK17(U_140,U_139))],[f_46_4]) ).
fof(f_46_6,negated_conjecture,
( ! [U_140,U_139] :
( ( min_precedes(U_140,sK18(U_140,U_139),tptp0)
& occurrence_of(sK18(U_140,U_139),tptp1)
& occurrence_of(U_139,tptp2) )
| ( min_precedes(U_140,sK17(U_140,U_139),tptp0)
& occurrence_of(sK17(U_140,U_139),tptp2)
& occurrence_of(U_139,tptp1) )
| ~ leaf_occ(U_139,sK16) )
& occurrence_of(sK16,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(U_138,sK18(U_140,U_139))],[f_46_5]) ).
cnf(f_46_7,negated_conjecture,
occurrence_of(sK16,tptp0),
inference(clausify,[status(thm)],[f_46_6]) ).
cnf(f_46_8,negated_conjecture,
( occurrence_of(U_139,tptp2)
| occurrence_of(U_139,tptp1)
| ~ leaf_occ(U_139,sK16) ),
inference(clausify,[status(thm)],[f_46_6]) ).
cnf(f_46_9,negated_conjecture,
( occurrence_of(sK18(U_140,U_139),tptp1)
| occurrence_of(U_139,tptp1)
| ~ leaf_occ(U_139,sK16) ),
inference(clausify,[status(thm)],[f_46_6]) ).
cnf(f_46_10,negated_conjecture,
( min_precedes(U_140,sK18(U_140,U_139),tptp0)
| occurrence_of(U_139,tptp1)
| ~ leaf_occ(U_139,sK16) ),
inference(clausify,[status(thm)],[f_46_6]) ).
cnf(f_46_11,negated_conjecture,
( occurrence_of(sK17(U_140,U_139),tptp2)
| occurrence_of(U_139,tptp2)
| ~ leaf_occ(U_139,sK16) ),
inference(clausify,[status(thm)],[f_46_6]) ).
cnf(f_46_12,negated_conjecture,
( min_precedes(U_140,sK17(U_140,U_139),tptp0)
| occurrence_of(U_139,tptp2)
| ~ leaf_occ(U_139,sK16) ),
inference(clausify,[status(thm)],[f_46_6]) ).
cnf(f_46_13,negated_conjecture,
( occurrence_of(sK18(U_140,U_139),tptp1)
| occurrence_of(sK17(U_140,U_139),tptp2)
| ~ leaf_occ(U_139,sK16) ),
inference(clausify,[status(thm)],[f_46_6]) ).
cnf(f_46_14,negated_conjecture,
( min_precedes(U_140,sK18(U_140,U_139),tptp0)
| occurrence_of(sK17(U_140,U_139),tptp2)
| ~ leaf_occ(U_139,sK16) ),
inference(clausify,[status(thm)],[f_46_6]) ).
cnf(f_46_15,negated_conjecture,
( occurrence_of(sK18(U_140,U_139),tptp1)
| min_precedes(U_140,sK17(U_140,U_139),tptp0)
| ~ leaf_occ(U_139,sK16) ),
inference(clausify,[status(thm)],[f_46_6]) ).
cnf(f_46_16,negated_conjecture,
( min_precedes(U_140,sK18(U_140,U_139),tptp0)
| min_precedes(U_140,sK17(U_140,U_139),tptp0)
| ~ leaf_occ(U_139,sK16) ),
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) = sK1(Eq_y_0,Eq_y_1)
| 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,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) = sK5(Eq_y_0)
| 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) = 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) = 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) = 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) = sK13(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_17,axiom,
( sK14(Eq_x_0) = sK14(Eq_y_0)
| 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,
( sK17(Eq_x_0,Eq_x_1) = sK17(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,
( sK18(Eq_x_0,Eq_x_1) = sK18(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_21,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_22,axiom,
( atomic(Eq_y_0)
| ~ atomic(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_23,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_24,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_25,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_26,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_27,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_28,axiom,
( arboreal(Eq_y_0)
| ~ arboreal(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_29,axiom,
( activity(Eq_y_0)
| ~ activity(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_30,axiom,
( activity_occurrence(Eq_y_0)
| ~ activity_occurrence(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_31,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_32,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_33,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_34,axiom,
( legal(Eq_y_0)
| ~ legal(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_35,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_36,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_37,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(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO010+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.03 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.38 % Computer : n018.cluster.edu
% 0.08/0.38 % Model : x86_64 x86_64
% 0.08/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.38 % Memory : 8046.5625MB
% 0.08/0.38 % OS : Linux 6.8.0-71-generic
% 0.08/0.38 % CPULimit : 300
% 0.08/0.38 % WCLimit : 300
% 0.08/0.38 % DateTime : Sat Sep 19 19:52:43 UTC 2026
% 0.08/0.38 % CPUTime :
% 77.24/77.51 % SZS status Theorem for theBenchmark
% 77.24/77.51 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------