%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PRO012+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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 : Sun Sep 27 08:20:57 AM UTC 2026
% Result : Theorem 5.65s 1.26s
% Output : CNFRefutation 5.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 20
% Syntax : Number of formulae : 135 ( 30 unt; 0 def)
% Number of atoms : 417 ( 55 equ)
% Maximal formula atoms : 17 ( 3 avg)
% Number of connectives : 439 ( 157 ~; 187 |; 76 &)
% ( 2 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-3 aty)
% Number of variables : 213 ( 16 sgn 104 !; 19 ?)
% Comments :
%------------------------------------------------------------------------------
fof(sos,axiom,
! [X0,X1] :
( occurrence_of(X1,X0)
=> ( activity_occurrence(X1)
& activity(X0) ) ),
file('theBenchmark.p',sos) ).
fof(sos_01,axiom,
! [X2] :
( activity_occurrence(X2)
=> ? [X3] :
( occurrence_of(X2,X3)
& activity(X3) ) ),
file('theBenchmark.p',sos_01) ).
fof(sos_02,axiom,
! [X4,X5,X6] :
( ( occurrence_of(X4,X6)
& occurrence_of(X4,X5) )
=> X5 = X6 ),
file('theBenchmark.p',sos_02) ).
fof(sos_08,axiom,
! [X18] :
( legal(X18)
=> arboreal(X18) ),
file('theBenchmark.p',sos_08) ).
fof(sos_10,axiom,
! [X21,X22] :
( precedes(X21,X22)
<=> ( legal(X22)
& earlier(X21,X22) ) ),
file('theBenchmark.p',sos_10) ).
fof(sos_14,axiom,
! [X35,X36,X37] :
( min_precedes(X35,X36,X37)
=> ~ root(X36,X37) ),
file('theBenchmark.p',sos_14) ).
fof(sos_15,axiom,
! [X38,X39,X40] :
( min_precedes(X38,X39,X40)
=> precedes(X38,X39) ),
file('theBenchmark.p',sos_15) ).
fof(sos_16,axiom,
! [X41,X42] :
( root(X41,X42)
=> legal(X41) ),
file('theBenchmark.p',sos_16) ).
fof(sos_24,axiom,
! [X67,X68] :
( subactivity_occurrence(X67,X68)
=> ( activity_occurrence(X68)
& activity_occurrence(X67) ) ),
file('theBenchmark.p',sos_24) ).
fof(sos_25,axiom,
! [X69,X70,X71] :
( min_precedes(X70,X71,X69)
=> ? [X72] :
( subactivity_occurrence(X71,X72)
& subactivity_occurrence(X70,X72)
& occurrence_of(X72,X69) ) ),
file('theBenchmark.p',sos_25) ).
fof(sos_27,axiom,
! [X76,X77] :
( ( ~ atomic(X76)
& occurrence_of(X77,X76) )
=> ? [X78] :
( subactivity_occurrence(X78,X77)
& root(X78,X76) ) ),
file('theBenchmark.p',sos_27) ).
fof(sos_28,axiom,
! [X79,X80,X81,X82] :
( ( subactivity_occurrence(X82,X80)
& subactivity_occurrence(X81,X80)
& arboreal(X82)
& arboreal(X81)
& occurrence_of(X80,X79) )
=> ( X81 = X82
| min_precedes(X82,X81,X79)
| min_precedes(X81,X82,X79) ) ),
file('theBenchmark.p',sos_28) ).
fof(sos_29,axiom,
! [X83,X84,X85,X86] :
( ( subactivity_occurrence(X84,X86)
& occurrence_of(X86,X85)
& min_precedes(X83,X84,X85) )
=> subactivity_occurrence(X83,X86) ),
file('theBenchmark.p',sos_29) ).
fof(sos_33,axiom,
! [X99,X100] :
( root_occ(X99,X100)
<=> ? [X101] :
( root(X99,X101)
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,X101) ) ),
file('theBenchmark.p',sos_33) ).
fof(sos_35,axiom,
! [X105,X106,X107,X108] :
( ( root_occ(X106,X107)
& root_occ(X105,X107)
& occurrence_of(X107,X108) )
=> X105 = X106 ),
file('theBenchmark.p',sos_35) ).
fof(sos_49,axiom,
! [X161] :
( occurrence_of(X161,tptp0)
=> ? [X162,X163,X164] :
( ! [X165] :
( min_precedes(X162,X165,tptp0)
=> ( X165 = X164
| X165 = X163 ) )
& min_precedes(X163,X164,tptp0)
& ( occurrence_of(X164,tptp1)
| occurrence_of(X164,tptp2) )
& min_precedes(X162,X163,tptp0)
& occurrence_of(X163,tptp4)
& root_occ(X162,X161)
& occurrence_of(X162,tptp3) ) ),
file('theBenchmark.p',sos_49) ).
fof(goals,conjecture,
! [X166] :
( occurrence_of(X166,tptp0)
=> ? [X167,X168] :
( min_precedes(X167,X168,tptp0)
& ( occurrence_of(X168,tptp1)
| occurrence_of(X168,tptp2) )
& root_occ(X167,X166)
& occurrence_of(X167,tptp3) ) ),
file('theBenchmark.p',goals) ).
fof(goals_neg,negated_conjecture,
~ ! [X166] :
( occurrence_of(X166,tptp0)
=> ? [X167,X168] :
( min_precedes(X167,X168,tptp0)
& ( occurrence_of(X168,tptp1)
| occurrence_of(X168,tptp2) )
& root_occ(X167,X166)
& occurrence_of(X167,tptp3) ) ),
inference(assume_negation,[status(cth)],[goals]) ).
cnf(c_58,plain,
( activity_occurrence(A)
| ~ subactivity_occurrence(A,B) ),
inference(clausify,[status(thm)],[sos_24]) ).
fof(nnf_2,plain,
! [X2] :
( ? [X3] :
( occurrence_of(X2,X3)
& activity(X3) )
| ~ activity_occurrence(X2) ),
inference(fof_nnf,[status(thm)],[sos_01]) ).
fof(sk_sos_01_sk,plain,
! [X2] :
( ( occurrence_of(X2,sK0(X2))
& activity(sK0(X2)) )
| ~ activity_occurrence(X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X3,sK0(X2))],[nnf_2]) ).
fof(sk_sos_01,plain,
( ! [VAR_0] :
( occurrence_of(VAR_0,sK0(VAR_0))
| ~ activity_occurrence(VAR_0) )
& ! [VAR_0] :
( activity(sK0(VAR_0))
| ~ activity_occurrence(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_01_sk]) ).
cnf(c_59,plain,
( occurrence_of(A,sK0(A))
| ~ activity_occurrence(A) ),
inference(split_conjunct,[status(thm)],[sk_sos_01]) ).
cnf(c_60,plain,
( activity_occurrence(A)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos]) ).
cnf(c_74,plain,
( precedes(A,B)
| ~ min_precedes(A,B,C) ),
inference(clausify,[status(thm)],[sos_15]) ).
cnf(c_78,plain,
( legal(B)
| ~ precedes(A,B) ),
inference(clausify,[status(thm)],[sos_10]) ).
cnf(c_82,plain,
( ~ root(B,C)
| ~ min_precedes(A,B,C) ),
inference(clausify,[status(thm)],[sos_14]) ).
cnf(c_83,plain,
( legal(A)
| ~ root(A,B) ),
inference(clausify,[status(thm)],[sos_16]) ).
fof(nnf_28,plain,
! [X76,X77] :
( ? [X78] :
( subactivity_occurrence(X78,X77)
& root(X78,X76) )
| atomic(X76)
| ~ occurrence_of(X77,X76) ),
inference(fof_nnf,[status(thm)],[sos_27]) ).
fof(sk_sos_27_sk,plain,
! [X76,X77] :
( ( subactivity_occurrence(sK1(X76,X77),X77)
& root(sK1(X76,X77),X76) )
| atomic(X76)
| ~ occurrence_of(X77,X76) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X78,sK1(X76,X77))],[nnf_28]) ).
fof(sk_sos_27,plain,
( ! [VAR_0,VAR_1] :
( subactivity_occurrence(sK1(VAR_1,VAR_0),VAR_0)
| atomic(VAR_1)
| ~ occurrence_of(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( root(sK1(VAR_1,VAR_0),VAR_1)
| atomic(VAR_1)
| ~ occurrence_of(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_27_sk]) ).
cnf(c_89,plain,
( root(sK1(B,A),B)
| atomic(B)
| ~ occurrence_of(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_27]) ).
fof(nnf_34,plain,
! [X99,X100] :
( ( ! [X101] :
( ~ root(X99,X101)
| ~ subactivity_occurrence(X99,X100)
| ~ occurrence_of(X100,X101) )
| root_occ(X99,X100) )
& ( ? [X169] :
( root(X99,X169)
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,X169) )
| ~ root_occ(X99,X100) ) ),
inference(fof_nnf,[status(thm)],[sos_33]) ).
fof(sk_sos_33_sk,plain,
! [X99,X100] :
( ( ! [X101] :
( ~ root(X99,X101)
| ~ subactivity_occurrence(X99,X100)
| ~ occurrence_of(X100,X101) )
| root_occ(X99,X100) )
& ( ( root(X99,sK2(X99,X100))
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,sK2(X99,X100)) )
| ~ root_occ(X99,X100) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X169,sK2(X99,X100))],[nnf_34]) ).
fof(sk_sos_33,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( ~ root(VAR_0,VAR_2)
| ~ subactivity_occurrence(VAR_0,VAR_1)
| ~ occurrence_of(VAR_1,VAR_2)
| root_occ(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( root(VAR_0,sK2(VAR_0,VAR_1))
| ~ root_occ(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( subactivity_occurrence(VAR_0,VAR_1)
| ~ root_occ(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( occurrence_of(VAR_1,sK2(VAR_0,VAR_1))
| ~ root_occ(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_33_sk]) ).
cnf(c_90,plain,
( root(A,sK2(A,B))
| ~ root_occ(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_33]) ).
cnf(c_91,plain,
( ~ root(A,C)
| ~ subactivity_occurrence(A,B)
| ~ occurrence_of(B,C)
| root_occ(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_33]) ).
cnf(c_181,plain,
( ~ min_precedes(B,A,C)
| legal(A) ),
inference(resolve,[status(thm)],[c_78,c_74]) ).
cnf(c_186,plain,
( occurrence_of(A,sK0(A))
| ~ occurrence_of(A,B) ),
inference(resolve,[status(thm)],[c_60,c_59]) ).
cnf(c_188,plain,
( ~ subactivity_occurrence(A,B)
| occurrence_of(A,sK0(A)) ),
inference(resolve,[status(thm)],[c_59,c_58]) ).
cnf(c_189,plain,
( C = B
| ~ occurrence_of(A,C)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_02]) ).
cnf(c_195,plain,
( arboreal(A)
| ~ legal(A) ),
inference(clausify,[status(thm)],[sos_08]) ).
fof(nnf_26,plain,
! [X69,X70,X71] :
( ? [X72] :
( subactivity_occurrence(X71,X72)
& subactivity_occurrence(X70,X72)
& occurrence_of(X72,X69) )
| ~ min_precedes(X70,X71,X69) ),
inference(fof_nnf,[status(thm)],[sos_25]) ).
fof(sk_sos_25_sk,plain,
! [X69,X70,X71] :
( ( subactivity_occurrence(X71,sK3(X69,X70,X71))
& subactivity_occurrence(X70,sK3(X69,X70,X71))
& occurrence_of(sK3(X69,X70,X71),X69) )
| ~ min_precedes(X70,X71,X69) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X72,sK3(X69,X70,X71))],[nnf_26]) ).
fof(sk_sos_25,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( subactivity_occurrence(VAR_1,sK3(VAR_2,VAR_0,VAR_1))
| ~ min_precedes(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( subactivity_occurrence(VAR_0,sK3(VAR_2,VAR_0,VAR_1))
| ~ min_precedes(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( occurrence_of(sK3(VAR_2,VAR_0,VAR_1),VAR_2)
| ~ min_precedes(VAR_0,VAR_1,VAR_2) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_25_sk]) ).
cnf(c_207,plain,
( occurrence_of(sK3(C,A,B),C)
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_25]) ).
cnf(c_208,plain,
( subactivity_occurrence(A,sK3(C,A,B))
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_25]) ).
cnf(c_209,plain,
( subactivity_occurrence(B,sK3(C,A,B))
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_25]) ).
cnf(c_210,plain,
( subactivity_occurrence(sK1(B,A),A)
| atomic(B)
| ~ occurrence_of(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_27]) ).
cnf(c_211,plain,
( D = C
| min_precedes(D,C,B)
| min_precedes(C,D,B)
| ~ subactivity_occurrence(D,A)
| ~ subactivity_occurrence(C,A)
| ~ arboreal(D)
| ~ arboreal(C)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_28]) ).
cnf(c_212,plain,
( subactivity_occurrence(A,D)
| ~ subactivity_occurrence(B,D)
| ~ occurrence_of(D,C)
| ~ min_precedes(A,B,C) ),
inference(clausify,[status(thm)],[sos_29]) ).
cnf(c_218,plain,
( D = C
| ~ root_occ(D,A)
| ~ root_occ(C,A)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_35]) ).
fof(nnf_50,plain,
! [X161] :
( ? [X162,X163,X164] :
( ! [X165] :
( X165 = X164
| X165 = X163
| ~ min_precedes(X162,X165,tptp0) )
& min_precedes(X163,X164,tptp0)
& ( occurrence_of(X164,tptp1)
| occurrence_of(X164,tptp2) )
& min_precedes(X162,X163,tptp0)
& occurrence_of(X163,tptp4)
& root_occ(X162,X161)
& occurrence_of(X162,tptp3) )
| ~ occurrence_of(X161,tptp0) ),
inference(fof_nnf,[status(thm)],[sos_49]) ).
fof(sk_sos_49_sk,plain,
! [X161] :
( ( ! [X165] :
( X165 = sK6(X161)
| X165 = sK5(X161)
| ~ min_precedes(sK4(X161),X165,tptp0) )
& min_precedes(sK5(X161),sK6(X161),tptp0)
& ( occurrence_of(sK6(X161),tptp1)
| occurrence_of(sK6(X161),tptp2) )
& min_precedes(sK4(X161),sK5(X161),tptp0)
& occurrence_of(sK5(X161),tptp4)
& root_occ(sK4(X161),X161)
& occurrence_of(sK4(X161),tptp3) )
| ~ occurrence_of(X161,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6]),skolemize(X162,sK4(X161)),skolemize(X163,sK5(X161)),skolemize(X164,sK6(X161))],[nnf_50]) ).
fof(sk_sos_49,plain,
( ! [VAR_0,VAR_1] :
( VAR_1 = sK6(VAR_0)
| VAR_1 = sK5(VAR_0)
| ~ min_precedes(sK4(VAR_0),VAR_1,tptp0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( min_precedes(sK5(VAR_0),sK6(VAR_0),tptp0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( occurrence_of(sK6(VAR_0),tptp1)
| occurrence_of(sK6(VAR_0),tptp2)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( min_precedes(sK4(VAR_0),sK5(VAR_0),tptp0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( occurrence_of(sK5(VAR_0),tptp4)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( root_occ(sK4(VAR_0),VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( occurrence_of(sK4(VAR_0),tptp3)
| ~ occurrence_of(VAR_0,tptp0) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_49_sk]) ).
cnf(c_232,plain,
( occurrence_of(sK4(A),tptp3)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
cnf(c_233,plain,
( root_occ(sK4(A),A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
cnf(c_235,plain,
( min_precedes(sK4(A),sK5(A),tptp0)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
cnf(c_236,plain,
( occurrence_of(sK6(A),tptp1)
| occurrence_of(sK6(A),tptp2)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
cnf(c_237,plain,
( min_precedes(sK5(A),sK6(A),tptp0)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
fof(sos_51,axiom,
~ atomic(tptp0),
file('theBenchmark.p',sos_51) ).
cnf(c_240,plain,
~ atomic(tptp0),
inference(clausify,[status(thm)],[sos_51]) ).
fof(sos_59,axiom,
tptp3 != tptp2,
file('theBenchmark.p',sos_59) ).
cnf(c_248,plain,
tptp3 != tptp2,
inference(clausify,[status(thm)],[sos_59]) ).
fof(sos_60,axiom,
tptp3 != tptp1,
file('theBenchmark.p',sos_60) ).
cnf(c_249,plain,
tptp3 != tptp1,
inference(clausify,[status(thm)],[sos_60]) ).
fof(nnf_51,plain,
? [X166] :
( ! [X167,X168] :
( ~ min_precedes(X167,X168,tptp0)
| ( ~ occurrence_of(X168,tptp1)
& ~ occurrence_of(X168,tptp2) )
| ~ root_occ(X167,X166)
| ~ occurrence_of(X167,tptp3) )
& occurrence_of(X166,tptp0) ),
inference(fof_nnf,[status(thm)],[goals_neg]) ).
fof(sk_goals_neg_sk,plain,
( ! [X167,X168] :
( ~ min_precedes(X167,X168,tptp0)
| ( ~ occurrence_of(X168,tptp1)
& ~ occurrence_of(X168,tptp2) )
| ~ root_occ(X167,sK7)
| ~ occurrence_of(X167,tptp3) )
& occurrence_of(sK7,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X166,sK7)],[nnf_51]) ).
fof(sk_goals_neg,plain,
( ! [VAR_0,VAR_1] :
( ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp1)
| ~ root_occ(VAR_0,sK7)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp2)
| ~ root_occ(VAR_0,sK7)
| ~ occurrence_of(VAR_0,tptp3) )
& occurrence_of(sK7,tptp0) ),
inference(cnf_transformation,[status(thm)],[sk_goals_neg_sk]) ).
cnf(c_251,negated_conjecture,
occurrence_of(sK7,tptp0),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_252,negated_conjecture,
( ~ min_precedes(A,B,tptp0)
| ~ occurrence_of(B,tptp2)
| ~ root_occ(A,sK7)
| ~ occurrence_of(A,tptp3) ),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_253,negated_conjecture,
( ~ min_precedes(A,B,tptp0)
| ~ occurrence_of(B,tptp1)
| ~ root_occ(A,sK7)
| ~ occurrence_of(A,tptp3) ),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_290,plain,
( ~ min_precedes(C,sK1(B,A),B)
| atomic(B)
| ~ occurrence_of(A,B) ),
inference(resolve,[status(thm)],[c_89,c_82]) ).
cnf(c_294,plain,
( legal(A)
| ~ root_occ(A,B) ),
inference(resolve,[status(thm)],[c_90,c_83]) ).
cnf(c_298,plain,
( atomic(A)
| ~ occurrence_of(B,A)
| ~ subactivity_occurrence(sK1(A,B),C)
| ~ occurrence_of(C,A)
| root_occ(sK1(A,B),C) ),
inference(resolve,[status(thm)],[c_91,c_89]) ).
cnf(c_343,plain,
( atomic(A)
| ~ subactivity_occurrence(sK1(A,B),B)
| ~ occurrence_of(B,A)
| root_occ(sK1(A,B),B) ),
inference(factor,[status(thm)],[c_298]) ).
cnf(c_351,plain,
min_precedes(sK5(sK7),sK6(sK7),tptp0),
inference(resolve,[status(thm)],[c_251,c_237]) ).
cnf(c_352,plain,
( occurrence_of(sK6(sK7),tptp1)
| occurrence_of(sK6(sK7),tptp2) ),
inference(resolve,[status(thm)],[c_251,c_236]) ).
cnf(c_353,plain,
min_precedes(sK4(sK7),sK5(sK7),tptp0),
inference(resolve,[status(thm)],[c_251,c_235]) ).
cnf(c_355,plain,
root_occ(sK4(sK7),sK7),
inference(resolve,[status(thm)],[c_251,c_233]) ).
cnf(c_356,plain,
occurrence_of(sK4(sK7),tptp3),
inference(resolve,[status(thm)],[c_251,c_232]) ).
cnf(c_1315,negated_conjecture,
( subactivity_occurrence(sK1(tptp0,sK7),sK7)
| atomic(tptp0) ),
inference(resolve,[status(thm)],[c_251,c_210]) ).
cnf(c_357,negated_conjecture,
subactivity_occurrence(sK1(tptp0,sK7),sK7),
inference(resolve,[status(thm)],[c_240,c_1315]) ).
cnf(c_394,plain,
subactivity_occurrence(sK6(sK7),sK3(tptp0,sK5(sK7),sK6(sK7))),
inference(resolve,[status(thm)],[c_351,c_209]) ).
cnf(c_395,plain,
subactivity_occurrence(sK5(sK7),sK3(tptp0,sK5(sK7),sK6(sK7))),
inference(resolve,[status(thm)],[c_351,c_208]) ).
cnf(c_396,plain,
occurrence_of(sK3(tptp0,sK5(sK7),sK6(sK7)),tptp0),
inference(resolve,[status(thm)],[c_351,c_207]) ).
cnf(c_412,plain,
legal(sK6(sK7)),
inference(resolve,[status(thm)],[c_351,c_181]) ).
cnf(c_425,plain,
arboreal(sK6(sK7)),
inference(resolve,[status(thm)],[c_412,c_195]) ).
cnf(c_437,plain,
legal(sK4(sK7)),
inference(resolve,[status(thm)],[c_355,c_294]) ).
cnf(c_451,plain,
( tptp2 = A
| ~ occurrence_of(sK6(sK7),A)
| occurrence_of(sK6(sK7),tptp1) ),
inference(resolve,[status(thm)],[c_352,c_189]) ).
cnf(c_453,plain,
arboreal(sK4(sK7)),
inference(resolve,[status(thm)],[c_437,c_195]) ).
cnf(c_458,plain,
( tptp3 = A
| ~ occurrence_of(sK4(sK7),A) ),
inference(resolve,[status(thm)],[c_356,c_189]) ).
cnf(c_459,plain,
occurrence_of(sK4(sK7),sK0(sK4(sK7))),
inference(resolve,[status(thm)],[c_356,c_186]) ).
cnf(c_493,plain,
( subactivity_occurrence(sK4(sK7),A)
| ~ subactivity_occurrence(sK5(sK7),A)
| ~ occurrence_of(A,tptp0) ),
inference(resolve,[status(thm)],[c_353,c_212]) ).
cnf(c_1316,plain,
( atomic(tptp0)
| ~ occurrence_of(sK7,tptp0)
| root_occ(sK1(tptp0,sK7),sK7) ),
inference(resolve,[status(thm)],[c_357,c_343]) ).
cnf(c_1317,negated_conjecture,
( atomic(tptp0)
| root_occ(sK1(tptp0,sK7),sK7) ),
inference(resolve,[status(thm)],[c_251,c_1316]) ).
cnf(c_555,negated_conjecture,
root_occ(sK1(tptp0,sK7),sK7),
inference(resolve,[status(thm)],[c_240,c_1317]) ).
cnf(c_1318,negated_conjecture,
( B = A
| ~ root_occ(B,sK7)
| ~ root_occ(A,sK7) ),
inference(resolve,[status(thm)],[c_218,c_251]) ).
cnf(c_1319,negated_conjecture,
( A = sK4(sK7)
| ~ root_occ(A,sK7) ),
inference(resolve,[status(thm)],[c_1318,c_355]) ).
cnf(c_642,negated_conjecture,
sK1(tptp0,sK7) = sK4(sK7),
inference(resolve,[status(thm)],[c_1319,c_555]) ).
cnf(c_1320,plain,
( ~ min_precedes(A,sK4(sK7),tptp0)
| atomic(tptp0)
| ~ occurrence_of(sK7,tptp0) ),
inference(paramod,[status(thm)],[c_642,c_290]) ).
cnf(c_1321,negated_conjecture,
( ~ min_precedes(A,sK4(sK7),tptp0)
| atomic(tptp0) ),
inference(resolve,[status(thm)],[c_251,c_1320]) ).
cnf(c_702,negated_conjecture,
~ min_precedes(A,sK4(sK7),tptp0),
inference(resolve,[status(thm)],[c_240,c_1321]) ).
cnf(c_1322,plain,
tptp3 = sK0(sK4(sK7)),
inference(resolve,[status(thm)],[c_459,c_458]) ).
cnf(c_740,plain,
sK0(sK4(sK7)) = tptp3,
inference(copy,[status(thm)],[c_1322]) ).
cnf(c_1064,plain,
occurrence_of(sK6(sK7),sK0(sK6(sK7))),
inference(resolve,[status(thm)],[c_394,c_188]) ).
cnf(c_1323,plain,
( tptp2 = sK0(sK6(sK7))
| occurrence_of(sK6(sK7),tptp1) ),
inference(resolve,[status(thm)],[c_1064,c_451]) ).
cnf(c_1068,plain,
( sK0(sK6(sK7)) = tptp2
| occurrence_of(sK6(sK7),tptp1) ),
inference(copy,[status(thm)],[c_1323]) ).
cnf(c_1324,plain,
( subactivity_occurrence(sK4(sK7),sK3(tptp0,sK5(sK7),sK6(sK7)))
| ~ occurrence_of(sK3(tptp0,sK5(sK7),sK6(sK7)),tptp0) ),
inference(resolve,[status(thm)],[c_395,c_493]) ).
cnf(c_1112,plain,
subactivity_occurrence(sK4(sK7),sK3(tptp0,sK5(sK7),sK6(sK7))),
inference(resolve,[status(thm)],[c_396,c_1324]) ).
cnf(c_1325,plain,
( A = sK0(sK6(sK7))
| ~ occurrence_of(sK6(sK7),A) ),
inference(resolve,[status(thm)],[c_189,c_1064]) ).
cnf(c_1326,plain,
( sK0(sK6(sK7)) = tptp2
| tptp1 = sK0(sK6(sK7)) ),
inference(resolve,[status(thm)],[c_1325,c_1068]) ).
cnf(c_1227,plain,
( sK0(sK6(sK7)) = tptp2
| sK0(sK6(sK7)) = tptp1 ),
inference(copy,[status(thm)],[c_1326]) ).
cnf(c_1327,plain,
( B = A
| min_precedes(B,A,tptp0)
| min_precedes(A,B,tptp0)
| ~ subactivity_occurrence(B,sK3(tptp0,sK5(sK7),sK6(sK7)))
| ~ subactivity_occurrence(A,sK3(tptp0,sK5(sK7),sK6(sK7)))
| ~ arboreal(B)
| ~ arboreal(A) ),
inference(resolve,[status(thm)],[c_211,c_396]) ).
cnf(c_1328,plain,
( A = sK6(sK7)
| min_precedes(A,sK6(sK7),tptp0)
| min_precedes(sK6(sK7),A,tptp0)
| ~ subactivity_occurrence(A,sK3(tptp0,sK5(sK7),sK6(sK7)))
| ~ subactivity_occurrence(sK6(sK7),sK3(tptp0,sK5(sK7),sK6(sK7)))
| ~ arboreal(A) ),
inference(resolve,[status(thm)],[c_1327,c_425]) ).
cnf(c_1329,plain,
( sK4(sK7) = sK6(sK7)
| min_precedes(sK4(sK7),sK6(sK7),tptp0)
| min_precedes(sK6(sK7),sK4(sK7),tptp0)
| ~ subactivity_occurrence(sK4(sK7),sK3(tptp0,sK5(sK7),sK6(sK7)))
| ~ subactivity_occurrence(sK6(sK7),sK3(tptp0,sK5(sK7),sK6(sK7))) ),
inference(resolve,[status(thm)],[c_1328,c_453]) ).
cnf(c_1330,plain,
( sK4(sK7) = sK6(sK7)
| min_precedes(sK4(sK7),sK6(sK7),tptp0)
| min_precedes(sK6(sK7),sK4(sK7),tptp0)
| ~ subactivity_occurrence(sK4(sK7),sK3(tptp0,sK5(sK7),sK6(sK7))) ),
inference(resolve,[status(thm)],[c_1329,c_394]) ).
cnf(c_1331,plain,
( sK4(sK7) = sK6(sK7)
| min_precedes(sK4(sK7),sK6(sK7),tptp0)
| min_precedes(sK6(sK7),sK4(sK7),tptp0) ),
inference(resolve,[status(thm)],[c_1330,c_1112]) ).
cnf(c_1332,plain,
( sK6(sK7) = sK4(sK7)
| min_precedes(sK4(sK7),sK6(sK7),tptp0)
| min_precedes(sK6(sK7),sK4(sK7),tptp0) ),
inference(copy,[status(thm)],[c_1331]) ).
cnf(c_1245,plain,
( sK6(sK7) = sK4(sK7)
| min_precedes(sK4(sK7),sK6(sK7),tptp0) ),
inference(resolve,[status(thm)],[c_702,c_1332]) ).
cnf(c_1333,negated_conjecture,
( ~ occurrence_of(sK6(sK7),tptp1)
| ~ root_occ(sK4(sK7),sK7)
| ~ occurrence_of(sK4(sK7),tptp3)
| sK6(sK7) = sK4(sK7) ),
inference(resolve,[status(thm)],[c_1245,c_253]) ).
cnf(c_1334,negated_conjecture,
( ~ occurrence_of(sK6(sK7),tptp1)
| ~ root_occ(sK4(sK7),sK7)
| sK6(sK7) = sK4(sK7) ),
inference(resolve,[status(thm)],[c_356,c_1333]) ).
cnf(c_1257,negated_conjecture,
( ~ occurrence_of(sK6(sK7),tptp1)
| sK6(sK7) = sK4(sK7) ),
inference(resolve,[status(thm)],[c_355,c_1334]) ).
cnf(c_1335,negated_conjecture,
( ~ min_precedes(sK4(sK7),A,tptp0)
| ~ occurrence_of(A,tptp2)
| ~ root_occ(sK4(sK7),sK7) ),
inference(resolve,[status(thm)],[c_252,c_356]) ).
cnf(c_1336,negated_conjecture,
( ~ min_precedes(sK4(sK7),A,tptp0)
| ~ occurrence_of(A,tptp2) ),
inference(resolve,[status(thm)],[c_1335,c_355]) ).
cnf(c_1337,negated_conjecture,
( occurrence_of(sK6(sK7),tptp1)
| ~ min_precedes(sK4(sK7),sK6(sK7),tptp0) ),
inference(resolve,[status(thm)],[c_1336,c_352]) ).
cnf(c_1285,negated_conjecture,
( sK6(sK7) = sK4(sK7)
| occurrence_of(sK6(sK7),tptp1) ),
inference(resolve,[status(thm)],[c_1337,c_1245]) ).
cnf(c_1338,plain,
( sK6(sK7) = sK4(sK7)
| sK6(sK7) = sK4(sK7) ),
inference(resolve,[status(thm)],[c_1285,c_1257]) ).
cnf(c_1291,plain,
sK6(sK7) = sK4(sK7),
inference(copy,[status(thm)],[c_1338]) ).
cnf(c_1339,plain,
( sK0(sK6(sK7)) = tptp2
| sK0(sK4(sK7)) = tptp1 ),
inference(paramod,[status(thm)],[c_1291,c_1227]) ).
cnf(c_1340,plain,
( sK0(sK6(sK7)) = tptp2
| tptp3 = tptp1 ),
inference(paramod,[status(thm)],[c_740,c_1339]) ).
cnf(c_1341,plain,
( sK0(sK4(sK7)) = tptp2
| tptp3 = tptp1 ),
inference(paramod,[status(thm)],[c_1291,c_1340]) ).
cnf(c_1342,plain,
( tptp3 = tptp2
| tptp3 = tptp1 ),
inference(paramod,[status(thm)],[c_740,c_1341]) ).
cnf(c_1343,plain,
tptp3 = tptp2,
inference(resolve,[status(thm)],[c_249,c_1342]) ).
cnf(c_1314,plain,
$false,
inference(resolve,[status(thm)],[c_248,c_1343]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : PRO012+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n005.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Sat Sep 26 04:58:32 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.45 % Process 1238299 was started by sandbox2 on n005,
% 0.17/0.45 % Sat Sep 26 04:58:32 2026
% 0.17/0.45 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.17/0.47
% 0.17/0.47 % From the command line: assign(max_seconds, 300).
% 5.65/1.26
% 5.65/1.26 % SZS status Theorem for theBenchmark
% 5.65/1.26
% 5.65/1.26 % Proof 1 at 0.65 (+ 0.10) seconds.
% 5.65/1.26 % Length of proof is 84.
% 5.65/1.26 % Level of proof is 10.
% 5.65/1.26 % Maximum clause weight is 29.000.
% 5.65/1.26 % Given clauses 330.
% 5.65/1.26
% 5.65/1.26 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------