%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PRO012+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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.84s 1.25s
% Output : CNFRefutation 5.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 14
% Syntax : Number of formulae : 100 ( 24 unt; 0 def)
% Number of atoms : 320 ( 30 equ)
% Maximal formula atoms : 17 ( 3 avg)
% Number of connectives : 348 ( 128 ~; 140 |; 64 &)
% ( 2 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-3 aty)
% Number of variables : 175 ( 11 sgn 86 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(sos_02,axiom,
! [X4,X5,X6] :
( ( occurrence_of(X4,X6)
& occurrence_of(X4,X5) )
=> X5 = X6 ),
file('theBenchmark.p',sos_02) ).
fof(sos_04,axiom,
! [X8,X9] :
( earlier(X8,X9)
=> ~ earlier(X9,X8) ),
file('theBenchmark.p',sos_04) ).
fof(sos_05,axiom,
! [X10,X11,X12] :
( ( earlier(X11,X12)
& earlier(X10,X11) )
=> earlier(X10,X12) ),
file('theBenchmark.p',sos_05) ).
fof(sos_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_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_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] :
( occurrence_of(X105,tptp0)
=> ? [X106,X107,X108] :
( ! [X109] :
( min_precedes(X106,X109,tptp0)
=> ( X109 = X108
| X109 = X107 ) )
& min_precedes(X107,X108,tptp0)
& ( occurrence_of(X108,tptp1)
| occurrence_of(X108,tptp2) )
& min_precedes(X106,X107,tptp0)
& occurrence_of(X107,tptp4)
& root_occ(X106,X105)
& occurrence_of(X106,tptp3) ) ),
file('theBenchmark.p',sos_35) ).
fof(goals,conjecture,
! [X110] :
( occurrence_of(X110,tptp0)
=> ? [X111,X112] :
( min_precedes(X111,X112,tptp0)
& ( occurrence_of(X112,tptp1)
| occurrence_of(X112,tptp2) )
& root_occ(X111,X110)
& occurrence_of(X111,tptp3) ) ),
file('theBenchmark.p',goals) ).
fof(goals_neg,negated_conjecture,
~ ! [X110] :
( occurrence_of(X110,tptp0)
=> ? [X111,X112] :
( min_precedes(X111,X112,tptp0)
& ( occurrence_of(X112,tptp1)
| occurrence_of(X112,tptp2) )
& root_occ(X111,X110)
& occurrence_of(X111,tptp3) ) ),
inference(assume_negation,[status(cth)],[goals]) ).
cnf(c_60,plain,
( precedes(A,B)
| ~ min_precedes(A,B,C) ),
inference(clausify,[status(thm)],[sos_15]) ).
cnf(c_64,plain,
( legal(B)
| ~ precedes(A,B) ),
inference(clausify,[status(thm)],[sos_10]) ).
cnf(c_65,plain,
( earlier(A,B)
| ~ precedes(A,B) ),
inference(clausify,[status(thm)],[sos_10]) ).
cnf(c_68,plain,
( ~ root(B,C)
| ~ min_precedes(A,B,C) ),
inference(clausify,[status(thm)],[sos_14]) ).
cnf(c_69,plain,
( legal(A)
| ~ root(A,B) ),
inference(clausify,[status(thm)],[sos_16]) ).
fof(nnf_34,plain,
! [X99,X100] :
( ( ! [X101] :
( ~ root(X99,X101)
| ~ subactivity_occurrence(X99,X100)
| ~ occurrence_of(X100,X101) )
| root_occ(X99,X100) )
& ( ? [X113] :
( root(X99,X113)
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,X113) )
| ~ 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,sK0(X99,X100))
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,sK0(X99,X100)) )
| ~ root_occ(X99,X100) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X113,sK0(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,sK0(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,sK0(VAR_0,VAR_1))
| ~ root_occ(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_33_sk]) ).
cnf(c_76,plain,
( root(A,sK0(A,B))
| ~ root_occ(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_33]) ).
cnf(c_120,plain,
( ~ min_precedes(C,A,sK0(A,B))
| ~ root_occ(A,B) ),
inference(resolve,[status(thm)],[c_76,c_68]) ).
cnf(c_121,plain,
( legal(A)
| ~ root_occ(A,B) ),
inference(resolve,[status(thm)],[c_76,c_69]) ).
fof(nnf_37,plain,
? [X110] :
( ! [X111,X112] :
( ~ min_precedes(X111,X112,tptp0)
| ( ~ occurrence_of(X112,tptp1)
& ~ occurrence_of(X112,tptp2) )
| ~ root_occ(X111,X110)
| ~ occurrence_of(X111,tptp3) )
& occurrence_of(X110,tptp0) ),
inference(fof_nnf,[status(thm)],[goals_neg]) ).
fof(sk_goals_neg_sk,plain,
( ! [X111,X112] :
( ~ min_precedes(X111,X112,tptp0)
| ( ~ occurrence_of(X112,tptp1)
& ~ occurrence_of(X112,tptp2) )
| ~ root_occ(X111,sK1)
| ~ occurrence_of(X111,tptp3) )
& occurrence_of(sK1,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X110,sK1)],[nnf_37]) ).
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,sK1)
| ~ 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,sK1)
| ~ occurrence_of(VAR_0,tptp3) )
& occurrence_of(sK1,tptp0) ),
inference(cnf_transformation,[status(thm)],[sk_goals_neg_sk]) ).
cnf(c_161,negated_conjecture,
( ~ min_precedes(A,B,tptp0)
| ~ occurrence_of(B,tptp1)
| ~ root_occ(A,sK1)
| ~ occurrence_of(A,tptp3) ),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_162,negated_conjecture,
( ~ min_precedes(A,B,tptp0)
| ~ occurrence_of(B,tptp2)
| ~ root_occ(A,sK1)
| ~ occurrence_of(A,tptp3) ),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_163,negated_conjecture,
occurrence_of(sK1,tptp0),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
fof(nnf_36,plain,
! [X105] :
( ? [X106,X107,X108] :
( ! [X109] :
( X109 = X108
| X109 = X107
| ~ min_precedes(X106,X109,tptp0) )
& min_precedes(X107,X108,tptp0)
& ( occurrence_of(X108,tptp1)
| occurrence_of(X108,tptp2) )
& min_precedes(X106,X107,tptp0)
& occurrence_of(X107,tptp4)
& root_occ(X106,X105)
& occurrence_of(X106,tptp3) )
| ~ occurrence_of(X105,tptp0) ),
inference(fof_nnf,[status(thm)],[sos_35]) ).
fof(sk_sos_35_sk,plain,
! [X105] :
( ( ! [X109] :
( X109 = sK3(X105)
| X109 = sK2(X105)
| ~ min_precedes(sK4(X105),X109,tptp0) )
& min_precedes(sK2(X105),sK3(X105),tptp0)
& ( occurrence_of(sK3(X105),tptp1)
| occurrence_of(sK3(X105),tptp2) )
& min_precedes(sK4(X105),sK2(X105),tptp0)
& occurrence_of(sK2(X105),tptp4)
& root_occ(sK4(X105),X105)
& occurrence_of(sK4(X105),tptp3) )
| ~ occurrence_of(X105,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK2,sK3]),skolemize(X106,sK4(X105)),skolemize(X107,sK2(X105)),skolemize(X108,sK3(X105))],[nnf_36]) ).
fof(sk_sos_35,plain,
( ! [VAR_0,VAR_1] :
( VAR_1 = sK3(VAR_0)
| VAR_1 = sK2(VAR_0)
| ~ min_precedes(sK4(VAR_0),VAR_1,tptp0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( min_precedes(sK2(VAR_0),sK3(VAR_0),tptp0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( occurrence_of(sK3(VAR_0),tptp1)
| occurrence_of(sK3(VAR_0),tptp2)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( min_precedes(sK4(VAR_0),sK2(VAR_0),tptp0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( occurrence_of(sK2(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_35_sk]) ).
cnf(c_177,plain,
( min_precedes(sK2(A),sK3(A),tptp0)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_35]) ).
cnf(c_178,plain,
( occurrence_of(sK3(A),tptp1)
| occurrence_of(sK3(A),tptp2)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_35]) ).
cnf(c_179,plain,
( min_precedes(sK4(A),sK2(A),tptp0)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_35]) ).
cnf(c_181,plain,
( root_occ(sK4(A),A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_35]) ).
cnf(c_182,plain,
( occurrence_of(sK4(A),tptp3)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_35]) ).
cnf(c_186,plain,
( occurrence_of(B,sK0(A,B))
| ~ root_occ(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_33]) ).
cnf(c_188,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_189,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]) ).
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,sK5(X69,X70,X71))
& subactivity_occurrence(X70,sK5(X69,X70,X71))
& occurrence_of(sK5(X69,X70,X71),X69) )
| ~ min_precedes(X70,X71,X69) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X72,sK5(X69,X70,X71))],[nnf_26]) ).
fof(sk_sos_25,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( subactivity_occurrence(VAR_1,sK5(VAR_2,VAR_0,VAR_1))
| ~ min_precedes(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( subactivity_occurrence(VAR_0,sK5(VAR_2,VAR_0,VAR_1))
| ~ min_precedes(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( occurrence_of(sK5(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_191,plain,
( subactivity_occurrence(B,sK5(C,A,B))
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_25]) ).
cnf(c_192,plain,
( subactivity_occurrence(A,sK5(C,A,B))
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_25]) ).
cnf(c_193,plain,
( occurrence_of(sK5(C,A,B),C)
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_25]) ).
cnf(c_201,plain,
( arboreal(A)
| ~ legal(A) ),
inference(clausify,[status(thm)],[sos_08]) ).
cnf(c_205,plain,
( earlier(A,C)
| ~ earlier(B,C)
| ~ earlier(A,B) ),
inference(clausify,[status(thm)],[sos_05]) ).
cnf(c_206,plain,
( ~ earlier(B,A)
| ~ earlier(A,B) ),
inference(clausify,[status(thm)],[sos_04]) ).
cnf(c_207,plain,
( C = B
| ~ occurrence_of(A,C)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_02]) ).
cnf(c_215,plain,
( ~ min_precedes(B,A,C)
| legal(A) ),
inference(resolve,[status(thm)],[c_64,c_60]) ).
cnf(c_216,plain,
( ~ min_precedes(A,B,C)
| earlier(A,B) ),
inference(resolve,[status(thm)],[c_65,c_60]) ).
cnf(c_263,plain,
~ earlier(A,A),
inference(factor,[status(thm)],[c_206]) ).
cnf(c_277,plain,
min_precedes(sK2(sK1),sK3(sK1),tptp0),
inference(resolve,[status(thm)],[c_177,c_163]) ).
cnf(c_278,plain,
( occurrence_of(sK3(sK1),tptp1)
| occurrence_of(sK3(sK1),tptp2) ),
inference(resolve,[status(thm)],[c_178,c_163]) ).
cnf(c_279,plain,
min_precedes(sK4(sK1),sK2(sK1),tptp0),
inference(resolve,[status(thm)],[c_179,c_163]) ).
cnf(c_281,plain,
root_occ(sK4(sK1),sK1),
inference(resolve,[status(thm)],[c_181,c_163]) ).
cnf(c_282,plain,
occurrence_of(sK4(sK1),tptp3),
inference(resolve,[status(thm)],[c_182,c_163]) ).
cnf(c_1287,negated_conjecture,
( A = tptp0
| ~ occurrence_of(sK1,A) ),
inference(resolve,[status(thm)],[c_207,c_163]) ).
cnf(c_285,negated_conjecture,
( tptp0 = A
| ~ occurrence_of(sK1,A) ),
inference(copy,[status(thm)],[c_1287]) ).
cnf(c_315,plain,
occurrence_of(sK1,sK0(sK4(sK1),sK1)),
inference(resolve,[status(thm)],[c_281,c_186]) ).
cnf(c_319,plain,
legal(sK4(sK1)),
inference(resolve,[status(thm)],[c_281,c_121]) ).
cnf(c_325,plain,
arboreal(sK4(sK1)),
inference(resolve,[status(thm)],[c_319,c_201]) ).
cnf(c_433,plain,
earlier(sK2(sK1),sK3(sK1)),
inference(resolve,[status(thm)],[c_277,c_216]) ).
cnf(c_434,plain,
legal(sK3(sK1)),
inference(resolve,[status(thm)],[c_277,c_215]) ).
cnf(c_448,plain,
occurrence_of(sK5(tptp0,sK2(sK1),sK3(sK1)),tptp0),
inference(resolve,[status(thm)],[c_277,c_193]) ).
cnf(c_449,plain,
subactivity_occurrence(sK2(sK1),sK5(tptp0,sK2(sK1),sK3(sK1))),
inference(resolve,[status(thm)],[c_277,c_192]) ).
cnf(c_450,plain,
subactivity_occurrence(sK3(sK1),sK5(tptp0,sK2(sK1),sK3(sK1))),
inference(resolve,[status(thm)],[c_277,c_191]) ).
cnf(c_472,plain,
arboreal(sK3(sK1)),
inference(resolve,[status(thm)],[c_434,c_201]) ).
cnf(c_497,plain,
earlier(sK4(sK1),sK2(sK1)),
inference(resolve,[status(thm)],[c_279,c_216]) ).
cnf(c_514,plain,
( subactivity_occurrence(sK4(sK1),A)
| ~ subactivity_occurrence(sK2(sK1),A)
| ~ occurrence_of(A,tptp0) ),
inference(resolve,[status(thm)],[c_279,c_188]) ).
cnf(c_1288,plain,
( earlier(sK4(sK1),A)
| ~ earlier(sK2(sK1),A) ),
inference(resolve,[status(thm)],[c_205,c_497]) ).
cnf(c_546,plain,
earlier(sK4(sK1),sK3(sK1)),
inference(resolve,[status(thm)],[c_1288,c_433]) ).
cnf(c_1289,plain,
tptp0 = sK0(sK4(sK1),sK1),
inference(resolve,[status(thm)],[c_315,c_285]) ).
cnf(c_581,plain,
sK0(sK4(sK1),sK1) = tptp0,
inference(copy,[status(thm)],[c_1289]) ).
cnf(c_1290,plain,
( ~ min_precedes(A,sK4(sK1),tptp0)
| ~ root_occ(sK4(sK1),sK1) ),
inference(paramod,[status(thm)],[c_581,c_120]) ).
cnf(c_602,plain,
~ min_precedes(A,sK4(sK1),tptp0),
inference(resolve,[status(thm)],[c_281,c_1290]) ).
cnf(c_1291,plain,
( subactivity_occurrence(sK4(sK1),sK5(tptp0,sK2(sK1),sK3(sK1)))
| ~ occurrence_of(sK5(tptp0,sK2(sK1),sK3(sK1)),tptp0) ),
inference(resolve,[status(thm)],[c_449,c_514]) ).
cnf(c_1042,plain,
subactivity_occurrence(sK4(sK1),sK5(tptp0,sK2(sK1),sK3(sK1))),
inference(resolve,[status(thm)],[c_448,c_1291]) ).
cnf(c_1292,plain,
( B = A
| min_precedes(B,A,tptp0)
| min_precedes(A,B,tptp0)
| ~ subactivity_occurrence(B,sK5(tptp0,sK2(sK1),sK3(sK1)))
| ~ subactivity_occurrence(A,sK5(tptp0,sK2(sK1),sK3(sK1)))
| ~ arboreal(B)
| ~ arboreal(A) ),
inference(resolve,[status(thm)],[c_189,c_448]) ).
cnf(c_1293,plain,
( A = sK3(sK1)
| min_precedes(A,sK3(sK1),tptp0)
| min_precedes(sK3(sK1),A,tptp0)
| ~ subactivity_occurrence(A,sK5(tptp0,sK2(sK1),sK3(sK1)))
| ~ subactivity_occurrence(sK3(sK1),sK5(tptp0,sK2(sK1),sK3(sK1)))
| ~ arboreal(A) ),
inference(resolve,[status(thm)],[c_1292,c_472]) ).
cnf(c_1294,plain,
( sK4(sK1) = sK3(sK1)
| min_precedes(sK4(sK1),sK3(sK1),tptp0)
| min_precedes(sK3(sK1),sK4(sK1),tptp0)
| ~ subactivity_occurrence(sK4(sK1),sK5(tptp0,sK2(sK1),sK3(sK1)))
| ~ subactivity_occurrence(sK3(sK1),sK5(tptp0,sK2(sK1),sK3(sK1))) ),
inference(resolve,[status(thm)],[c_1293,c_325]) ).
cnf(c_1295,plain,
( sK4(sK1) = sK3(sK1)
| min_precedes(sK4(sK1),sK3(sK1),tptp0)
| min_precedes(sK3(sK1),sK4(sK1),tptp0)
| ~ subactivity_occurrence(sK4(sK1),sK5(tptp0,sK2(sK1),sK3(sK1))) ),
inference(resolve,[status(thm)],[c_1294,c_450]) ).
cnf(c_1296,plain,
( sK4(sK1) = sK3(sK1)
| min_precedes(sK4(sK1),sK3(sK1),tptp0)
| min_precedes(sK3(sK1),sK4(sK1),tptp0) ),
inference(resolve,[status(thm)],[c_1295,c_1042]) ).
cnf(c_1297,plain,
( sK3(sK1) = sK4(sK1)
| min_precedes(sK4(sK1),sK3(sK1),tptp0)
| min_precedes(sK3(sK1),sK4(sK1),tptp0) ),
inference(copy,[status(thm)],[c_1296]) ).
cnf(c_1162,plain,
( sK3(sK1) = sK4(sK1)
| min_precedes(sK4(sK1),sK3(sK1),tptp0) ),
inference(resolve,[status(thm)],[c_602,c_1297]) ).
cnf(c_1298,negated_conjecture,
( ~ occurrence_of(sK3(sK1),tptp1)
| ~ root_occ(sK4(sK1),sK1)
| ~ occurrence_of(sK4(sK1),tptp3)
| sK3(sK1) = sK4(sK1) ),
inference(resolve,[status(thm)],[c_1162,c_161]) ).
cnf(c_1299,negated_conjecture,
( ~ occurrence_of(sK3(sK1),tptp1)
| ~ root_occ(sK4(sK1),sK1)
| sK3(sK1) = sK4(sK1) ),
inference(resolve,[status(thm)],[c_282,c_1298]) ).
cnf(c_1184,negated_conjecture,
( ~ occurrence_of(sK3(sK1),tptp1)
| sK3(sK1) = sK4(sK1) ),
inference(resolve,[status(thm)],[c_281,c_1299]) ).
cnf(c_1300,negated_conjecture,
( ~ min_precedes(sK4(sK1),A,tptp0)
| ~ occurrence_of(A,tptp2)
| ~ root_occ(sK4(sK1),sK1) ),
inference(resolve,[status(thm)],[c_162,c_282]) ).
cnf(c_1301,negated_conjecture,
( ~ min_precedes(sK4(sK1),A,tptp0)
| ~ occurrence_of(A,tptp2) ),
inference(resolve,[status(thm)],[c_1300,c_281]) ).
cnf(c_1302,negated_conjecture,
( occurrence_of(sK3(sK1),tptp1)
| ~ min_precedes(sK4(sK1),sK3(sK1),tptp0) ),
inference(resolve,[status(thm)],[c_1301,c_278]) ).
cnf(c_1200,negated_conjecture,
( sK3(sK1) = sK4(sK1)
| occurrence_of(sK3(sK1),tptp1) ),
inference(resolve,[status(thm)],[c_1302,c_1162]) ).
cnf(c_1303,plain,
( sK3(sK1) = sK4(sK1)
| sK3(sK1) = sK4(sK1) ),
inference(resolve,[status(thm)],[c_1200,c_1184]) ).
cnf(c_1204,plain,
sK3(sK1) = sK4(sK1),
inference(copy,[status(thm)],[c_1303]) ).
cnf(c_1304,plain,
earlier(sK4(sK1),sK4(sK1)),
inference(paramod,[status(thm)],[c_1204,c_546]) ).
cnf(c_1286,plain,
$false,
inference(resolve,[status(thm)],[c_263,c_1304]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : PRO012+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.44 % Computer : n019.cluster.edu
% 0.19/0.44 % Model : x86_64 x86_64
% 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.44 % Memory : 8046.5625MB
% 0.19/0.44 % OS : Linux 6.8.0-71-generic
% 0.19/0.44 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.44 % DateTime : Sat Sep 26 04:58:49 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.19/0.45 % Process 439498 was started by sandbox on n019,
% 0.19/0.45 % Sat Sep 26 04:58:49 2026
% 0.19/0.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.19/0.47
% 0.19/0.47 % From the command line: assign(max_seconds, 300).
% 5.84/1.25
% 5.84/1.25 % SZS status Theorem for theBenchmark
% 5.84/1.25
% 5.84/1.25 % Proof 1 at 0.66 (+ 0.09) seconds.
% 5.84/1.25 % Length of proof is 69.
% 5.84/1.25 % Level of proof is 9.
% 5.84/1.25 % Maximum clause weight is 29.000.
% 5.84/1.25 % Given clauses 321.
% 5.84/1.25
% 5.84/1.25 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------