%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PRO014+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:58 AM UTC 2026
% Result : Theorem 7.08s 1.40s
% Output : CNFRefutation 7.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 12
% Syntax : Number of formulae : 125 ( 30 unt; 0 def)
% Number of atoms : 446 ( 20 equ)
% Maximal formula atoms : 36 ( 3 avg)
% Number of connectives : 510 ( 189 ~; 232 |; 76 &)
% ( 2 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 7 con; 0-3 aty)
% Number of variables : 169 ( 5 sgn 76 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
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_15,axiom,
! [X38,X39,X40] :
( min_precedes(X38,X39,X40)
=> precedes(X38,X39) ),
file('theBenchmark.p',sos_15) ).
fof(sos_18,axiom,
! [X45,X46,X47,X48] :
( ( precedes(X46,X47)
& min_precedes(X45,X47,X48)
& min_precedes(X45,X46,X48) )
=> min_precedes(X46,X47,X48) ),
file('theBenchmark.p',sos_18) ).
fof(sos_22,axiom,
! [X60,X61,X62] :
( next_subocc(X60,X61,X62)
<=> ( ~ ? [X63] :
( min_precedes(X63,X61,X62)
& min_precedes(X60,X63,X62) )
& min_precedes(X60,X61,X62) ) ),
file('theBenchmark.p',sos_22) ).
fof(sos_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_35,axiom,
! [X105,X106] :
( ( ~ leaf_occ(X105,X106)
& arboreal(X105)
& subactivity_occurrence(X105,X106)
& occurrence_of(X106,tptp0) )
=> ? [X107,X108,X109] :
( leaf(X109,tptp0)
& next_subocc(X108,X109,tptp0)
& ( occurrence_of(X109,tptp1)
| occurrence_of(X109,tptp2) )
& next_subocc(X107,X108,tptp0)
& occurrence_of(X108,tptp4)
& next_subocc(X105,X107,tptp0)
& occurrence_of(X107,tptp3) ) ),
file('theBenchmark.p',sos_35) ).
fof(goals,conjecture,
! [X110,X111] :
( ( ~ leaf_occ(X110,X111)
& arboreal(X110)
& subactivity_occurrence(X110,X111)
& occurrence_of(X111,tptp0) )
=> ? [X112,X113] :
( leaf(X113,tptp0)
& min_precedes(X112,X113,tptp0)
& ( occurrence_of(X113,tptp1)
| occurrence_of(X113,tptp2) )
& next_subocc(X110,X112,tptp0)
& occurrence_of(X112,tptp3) ) ),
file('theBenchmark.p',goals) ).
fof(goals_neg,negated_conjecture,
~ ! [X110,X111] :
( ( ~ leaf_occ(X110,X111)
& arboreal(X110)
& subactivity_occurrence(X110,X111)
& occurrence_of(X111,tptp0) )
=> ? [X112,X113] :
( leaf(X113,tptp0)
& min_precedes(X112,X113,tptp0)
& ( occurrence_of(X113,tptp1)
| occurrence_of(X113,tptp2) )
& next_subocc(X110,X112,tptp0)
& occurrence_of(X112,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_61,plain,
( min_precedes(B,D,C)
| ~ precedes(B,D)
| ~ min_precedes(A,D,C)
| ~ min_precedes(A,B,C) ),
inference(clausify,[status(thm)],[sos_18]) ).
cnf(c_63,plain,
( ~ legal(B)
| ~ earlier(A,B)
| precedes(A,B) ),
inference(clausify,[status(thm)],[sos_10]) ).
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]) ).
fof(nnf_37,plain,
? [X110,X111] :
( ! [X112,X113] :
( ~ leaf(X113,tptp0)
| ~ min_precedes(X112,X113,tptp0)
| ( ~ occurrence_of(X113,tptp1)
& ~ occurrence_of(X113,tptp2) )
| ~ next_subocc(X110,X112,tptp0)
| ~ occurrence_of(X112,tptp3) )
& ~ leaf_occ(X110,X111)
& arboreal(X110)
& subactivity_occurrence(X110,X111)
& occurrence_of(X111,tptp0) ),
inference(fof_nnf,[status(thm)],[goals_neg]) ).
fof(sk_goals_neg_sk,plain,
( ! [X112,X113] :
( ~ leaf(X113,tptp0)
| ~ min_precedes(X112,X113,tptp0)
| ( ~ occurrence_of(X113,tptp1)
& ~ occurrence_of(X113,tptp2) )
| ~ next_subocc(sK0,X112,tptp0)
| ~ occurrence_of(X112,tptp3) )
& ~ leaf_occ(sK0,sK1)
& arboreal(sK0)
& subactivity_occurrence(sK0,sK1)
& occurrence_of(sK1,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK0]),skolemize(X110,sK0),skolemize(X111,sK1)],[nnf_37]) ).
fof(sk_goals_neg,plain,
( ! [VAR_0,VAR_1] :
( ~ leaf(VAR_1,tptp0)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp1)
| ~ next_subocc(sK0,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( ~ leaf(VAR_1,tptp0)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp2)
| ~ next_subocc(sK0,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ~ leaf_occ(sK0,sK1)
& arboreal(sK0)
& subactivity_occurrence(sK0,sK1)
& occurrence_of(sK1,tptp0) ),
inference(cnf_transformation,[status(thm)],[sk_goals_neg_sk]) ).
cnf(c_151,negated_conjecture,
( ~ leaf(B,tptp0)
| ~ min_precedes(A,B,tptp0)
| ~ occurrence_of(B,tptp1)
| ~ next_subocc(sK0,A,tptp0)
| ~ occurrence_of(A,tptp3) ),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_152,negated_conjecture,
( ~ leaf(B,tptp0)
| ~ min_precedes(A,B,tptp0)
| ~ occurrence_of(B,tptp2)
| ~ next_subocc(sK0,A,tptp0)
| ~ occurrence_of(A,tptp3) ),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_153,negated_conjecture,
~ leaf_occ(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_154,negated_conjecture,
arboreal(sK0),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_155,negated_conjecture,
subactivity_occurrence(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_156,negated_conjecture,
occurrence_of(sK1,tptp0),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
fof(nnf_36,plain,
! [X105,X106] :
( ? [X107,X108,X109] :
( leaf(X109,tptp0)
& next_subocc(X108,X109,tptp0)
& ( occurrence_of(X109,tptp1)
| occurrence_of(X109,tptp2) )
& next_subocc(X107,X108,tptp0)
& occurrence_of(X108,tptp4)
& next_subocc(X105,X107,tptp0)
& occurrence_of(X107,tptp3) )
| leaf_occ(X105,X106)
| ~ arboreal(X105)
| ~ subactivity_occurrence(X105,X106)
| ~ occurrence_of(X106,tptp0) ),
inference(fof_nnf,[status(thm)],[sos_35]) ).
fof(sk_sos_35_sk,plain,
! [X105,X106] :
( ( leaf(sK2(X105,X106),tptp0)
& next_subocc(sK3(X105,X106),sK2(X105,X106),tptp0)
& ( occurrence_of(sK2(X105,X106),tptp1)
| occurrence_of(sK2(X105,X106),tptp2) )
& next_subocc(sK4(X105,X106),sK3(X105,X106),tptp0)
& occurrence_of(sK3(X105,X106),tptp4)
& next_subocc(X105,sK4(X105,X106),tptp0)
& occurrence_of(sK4(X105,X106),tptp3) )
| leaf_occ(X105,X106)
| ~ arboreal(X105)
| ~ subactivity_occurrence(X105,X106)
| ~ occurrence_of(X106,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK3,sK2]),skolemize(X107,sK4(X105,X106)),skolemize(X108,sK3(X105,X106)),skolemize(X109,sK2(X105,X106))],[nnf_36]) ).
fof(sk_sos_35,plain,
( ! [VAR_0,VAR_1] :
( leaf(sK2(VAR_1,VAR_0),tptp0)
| leaf_occ(VAR_1,VAR_0)
| ~ arboreal(VAR_1)
| ~ subactivity_occurrence(VAR_1,VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0,VAR_1] :
( next_subocc(sK3(VAR_1,VAR_0),sK2(VAR_1,VAR_0),tptp0)
| leaf_occ(VAR_1,VAR_0)
| ~ arboreal(VAR_1)
| ~ subactivity_occurrence(VAR_1,VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0,VAR_1] :
( occurrence_of(sK2(VAR_1,VAR_0),tptp1)
| occurrence_of(sK2(VAR_1,VAR_0),tptp2)
| leaf_occ(VAR_1,VAR_0)
| ~ arboreal(VAR_1)
| ~ subactivity_occurrence(VAR_1,VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0,VAR_1] :
( next_subocc(sK4(VAR_1,VAR_0),sK3(VAR_1,VAR_0),tptp0)
| leaf_occ(VAR_1,VAR_0)
| ~ arboreal(VAR_1)
| ~ subactivity_occurrence(VAR_1,VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0,VAR_1] :
( occurrence_of(sK3(VAR_1,VAR_0),tptp4)
| leaf_occ(VAR_1,VAR_0)
| ~ arboreal(VAR_1)
| ~ subactivity_occurrence(VAR_1,VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0,VAR_1] :
( next_subocc(VAR_1,sK4(VAR_1,VAR_0),tptp0)
| leaf_occ(VAR_1,VAR_0)
| ~ arboreal(VAR_1)
| ~ subactivity_occurrence(VAR_1,VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0,VAR_1] :
( occurrence_of(sK4(VAR_1,VAR_0),tptp3)
| leaf_occ(VAR_1,VAR_0)
| ~ arboreal(VAR_1)
| ~ subactivity_occurrence(VAR_1,VAR_0)
| ~ occurrence_of(VAR_0,tptp0) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_35_sk]) ).
cnf(c_168,plain,
( leaf(sK2(B,A),tptp0)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_35]) ).
cnf(c_169,plain,
( next_subocc(sK3(B,A),sK2(B,A),tptp0)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_35]) ).
cnf(c_170,plain,
( occurrence_of(sK2(B,A),tptp1)
| occurrence_of(sK2(B,A),tptp2)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_35]) ).
cnf(c_171,plain,
( next_subocc(sK4(B,A),sK3(B,A),tptp0)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_35]) ).
cnf(c_173,plain,
( next_subocc(B,sK4(B,A),tptp0)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_35]) ).
cnf(c_174,plain,
( occurrence_of(sK4(B,A),tptp3)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_35]) ).
cnf(c_182,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_183,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_185,plain,
( subactivity_occurrence(B,sK5(C,A,B))
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_25]) ).
cnf(c_186,plain,
( subactivity_occurrence(A,sK5(C,A,B))
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_25]) ).
cnf(c_187,plain,
( occurrence_of(sK5(C,A,B),C)
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_25]) ).
cnf(c_193,plain,
( min_precedes(A,B,C)
| ~ next_subocc(A,B,C) ),
inference(clausify,[status(thm)],[sos_22]) ).
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_213,plain,
( min_precedes(A,B,D)
| ~ min_precedes(C,B,D)
| ~ min_precedes(C,A,D)
| ~ legal(B)
| ~ earlier(A,B) ),
inference(resolve,[status(thm)],[c_63,c_61]) ).
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_2236,negated_conjecture,
( leaf(sK2(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0)
| ~ occurrence_of(sK1,tptp0) ),
inference(resolve,[status(thm)],[c_168,c_155]) ).
cnf(c_2237,negated_conjecture,
( leaf(sK2(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0) ),
inference(resolve,[status(thm)],[c_156,c_2236]) ).
cnf(c_2238,negated_conjecture,
( leaf(sK2(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1) ),
inference(resolve,[status(thm)],[c_154,c_2237]) ).
cnf(c_254,negated_conjecture,
leaf(sK2(sK0,sK1),tptp0),
inference(resolve,[status(thm)],[c_153,c_2238]) ).
cnf(c_2239,negated_conjecture,
( next_subocc(sK3(sK0,sK1),sK2(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0)
| ~ occurrence_of(sK1,tptp0) ),
inference(resolve,[status(thm)],[c_169,c_155]) ).
cnf(c_2240,negated_conjecture,
( next_subocc(sK3(sK0,sK1),sK2(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0) ),
inference(resolve,[status(thm)],[c_156,c_2239]) ).
cnf(c_2241,negated_conjecture,
( next_subocc(sK3(sK0,sK1),sK2(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1) ),
inference(resolve,[status(thm)],[c_154,c_2240]) ).
cnf(c_255,negated_conjecture,
next_subocc(sK3(sK0,sK1),sK2(sK0,sK1),tptp0),
inference(resolve,[status(thm)],[c_153,c_2241]) ).
cnf(c_2242,negated_conjecture,
( occurrence_of(sK2(sK0,sK1),tptp1)
| occurrence_of(sK2(sK0,sK1),tptp2)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0)
| ~ occurrence_of(sK1,tptp0) ),
inference(resolve,[status(thm)],[c_170,c_155]) ).
cnf(c_2243,negated_conjecture,
( occurrence_of(sK2(sK0,sK1),tptp1)
| occurrence_of(sK2(sK0,sK1),tptp2)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0) ),
inference(resolve,[status(thm)],[c_156,c_2242]) ).
cnf(c_2244,negated_conjecture,
( occurrence_of(sK2(sK0,sK1),tptp1)
| occurrence_of(sK2(sK0,sK1),tptp2)
| leaf_occ(sK0,sK1) ),
inference(resolve,[status(thm)],[c_154,c_2243]) ).
cnf(c_256,negated_conjecture,
( occurrence_of(sK2(sK0,sK1),tptp1)
| occurrence_of(sK2(sK0,sK1),tptp2) ),
inference(resolve,[status(thm)],[c_153,c_2244]) ).
cnf(c_2245,negated_conjecture,
( next_subocc(sK4(sK0,sK1),sK3(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0)
| ~ occurrence_of(sK1,tptp0) ),
inference(resolve,[status(thm)],[c_171,c_155]) ).
cnf(c_2246,negated_conjecture,
( next_subocc(sK4(sK0,sK1),sK3(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0) ),
inference(resolve,[status(thm)],[c_156,c_2245]) ).
cnf(c_2247,negated_conjecture,
( next_subocc(sK4(sK0,sK1),sK3(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1) ),
inference(resolve,[status(thm)],[c_154,c_2246]) ).
cnf(c_257,negated_conjecture,
next_subocc(sK4(sK0,sK1),sK3(sK0,sK1),tptp0),
inference(resolve,[status(thm)],[c_153,c_2247]) ).
cnf(c_2248,negated_conjecture,
( next_subocc(sK0,sK4(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0)
| ~ occurrence_of(sK1,tptp0) ),
inference(resolve,[status(thm)],[c_173,c_155]) ).
cnf(c_2249,negated_conjecture,
( next_subocc(sK0,sK4(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0) ),
inference(resolve,[status(thm)],[c_156,c_2248]) ).
cnf(c_2250,negated_conjecture,
( next_subocc(sK0,sK4(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1) ),
inference(resolve,[status(thm)],[c_154,c_2249]) ).
cnf(c_259,negated_conjecture,
next_subocc(sK0,sK4(sK0,sK1),tptp0),
inference(resolve,[status(thm)],[c_153,c_2250]) ).
cnf(c_2251,negated_conjecture,
( occurrence_of(sK4(sK0,sK1),tptp3)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0)
| ~ occurrence_of(sK1,tptp0) ),
inference(resolve,[status(thm)],[c_174,c_155]) ).
cnf(c_2252,negated_conjecture,
( occurrence_of(sK4(sK0,sK1),tptp3)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0) ),
inference(resolve,[status(thm)],[c_156,c_2251]) ).
cnf(c_2253,negated_conjecture,
( occurrence_of(sK4(sK0,sK1),tptp3)
| leaf_occ(sK0,sK1) ),
inference(resolve,[status(thm)],[c_154,c_2252]) ).
cnf(c_260,negated_conjecture,
occurrence_of(sK4(sK0,sK1),tptp3),
inference(resolve,[status(thm)],[c_153,c_2253]) ).
cnf(c_382,plain,
min_precedes(sK0,sK4(sK0,sK1),tptp0),
inference(resolve,[status(thm)],[c_259,c_193]) ).
cnf(c_2254,negated_conjecture,
( ~ leaf(A,tptp0)
| ~ min_precedes(sK4(sK0,sK1),A,tptp0)
| ~ occurrence_of(A,tptp2)
| ~ occurrence_of(sK4(sK0,sK1),tptp3) ),
inference(resolve,[status(thm)],[c_259,c_152]) ).
cnf(c_384,negated_conjecture,
( ~ leaf(A,tptp0)
| ~ min_precedes(sK4(sK0,sK1),A,tptp0)
| ~ occurrence_of(A,tptp2) ),
inference(resolve,[status(thm)],[c_260,c_2254]) ).
cnf(c_2255,negated_conjecture,
( ~ leaf(A,tptp0)
| ~ min_precedes(sK4(sK0,sK1),A,tptp0)
| ~ occurrence_of(A,tptp1)
| ~ occurrence_of(sK4(sK0,sK1),tptp3) ),
inference(resolve,[status(thm)],[c_259,c_151]) ).
cnf(c_385,negated_conjecture,
( ~ leaf(A,tptp0)
| ~ min_precedes(sK4(sK0,sK1),A,tptp0)
| ~ occurrence_of(A,tptp1) ),
inference(resolve,[status(thm)],[c_260,c_2255]) ).
cnf(c_388,plain,
earlier(sK0,sK4(sK0,sK1)),
inference(resolve,[status(thm)],[c_382,c_216]) ).
cnf(c_393,plain,
( min_precedes(sK4(sK0,sK1),A,tptp0)
| ~ min_precedes(sK0,A,tptp0)
| ~ legal(A)
| ~ earlier(sK4(sK0,sK1),A) ),
inference(resolve,[status(thm)],[c_382,c_213]) ).
cnf(c_408,plain,
( subactivity_occurrence(sK0,A)
| ~ subactivity_occurrence(sK4(sK0,sK1),A)
| ~ occurrence_of(A,tptp0) ),
inference(resolve,[status(thm)],[c_382,c_182]) ).
cnf(c_433,plain,
( earlier(sK0,A)
| ~ earlier(sK4(sK0,sK1),A) ),
inference(resolve,[status(thm)],[c_388,c_205]) ).
cnf(c_443,plain,
min_precedes(sK3(sK0,sK1),sK2(sK0,sK1),tptp0),
inference(resolve,[status(thm)],[c_255,c_193]) ).
cnf(c_445,plain,
min_precedes(sK4(sK0,sK1),sK3(sK0,sK1),tptp0),
inference(resolve,[status(thm)],[c_257,c_193]) ).
cnf(c_451,plain,
earlier(sK3(sK0,sK1),sK2(sK0,sK1)),
inference(resolve,[status(thm)],[c_443,c_216]) ).
cnf(c_452,plain,
legal(sK2(sK0,sK1)),
inference(resolve,[status(thm)],[c_443,c_215]) ).
cnf(c_467,plain,
occurrence_of(sK5(tptp0,sK3(sK0,sK1),sK2(sK0,sK1)),tptp0),
inference(resolve,[status(thm)],[c_443,c_187]) ).
cnf(c_468,plain,
subactivity_occurrence(sK3(sK0,sK1),sK5(tptp0,sK3(sK0,sK1),sK2(sK0,sK1))),
inference(resolve,[status(thm)],[c_443,c_186]) ).
cnf(c_469,plain,
subactivity_occurrence(sK2(sK0,sK1),sK5(tptp0,sK3(sK0,sK1),sK2(sK0,sK1))),
inference(resolve,[status(thm)],[c_443,c_185]) ).
cnf(c_485,plain,
arboreal(sK2(sK0,sK1)),
inference(resolve,[status(thm)],[c_452,c_201]) ).
cnf(c_500,plain,
earlier(sK4(sK0,sK1),sK3(sK0,sK1)),
inference(resolve,[status(thm)],[c_445,c_216]) ).
cnf(c_519,plain,
( subactivity_occurrence(sK4(sK0,sK1),A)
| ~ subactivity_occurrence(sK3(sK0,sK1),A)
| ~ occurrence_of(A,tptp0) ),
inference(resolve,[status(thm)],[c_445,c_182]) ).
cnf(c_534,plain,
earlier(sK0,sK3(sK0,sK1)),
inference(resolve,[status(thm)],[c_500,c_433]) ).
cnf(c_2256,plain,
( earlier(sK4(sK0,sK1),A)
| ~ earlier(sK3(sK0,sK1),A) ),
inference(resolve,[status(thm)],[c_205,c_500]) ).
cnf(c_539,plain,
earlier(sK4(sK0,sK1),sK2(sK0,sK1)),
inference(resolve,[status(thm)],[c_2256,c_451]) ).
cnf(c_2257,plain,
( earlier(sK0,A)
| ~ earlier(sK3(sK0,sK1),A) ),
inference(resolve,[status(thm)],[c_205,c_534]) ).
cnf(c_544,plain,
earlier(sK0,sK2(sK0,sK1)),
inference(resolve,[status(thm)],[c_2257,c_451]) ).
cnf(c_545,plain,
~ earlier(sK2(sK0,sK1),sK0),
inference(resolve,[status(thm)],[c_544,c_206]) ).
cnf(c_569,plain,
~ earlier(sK2(sK0,sK1),sK4(sK0,sK1)),
inference(resolve,[status(thm)],[c_539,c_206]) ).
cnf(c_2258,plain,
( subactivity_occurrence(sK4(sK0,sK1),sK5(tptp0,sK3(sK0,sK1),sK2(sK0,sK1)))
| ~ occurrence_of(sK5(tptp0,sK3(sK0,sK1),sK2(sK0,sK1)),tptp0) ),
inference(resolve,[status(thm)],[c_468,c_519]) ).
cnf(c_1503,plain,
subactivity_occurrence(sK4(sK0,sK1),sK5(tptp0,sK3(sK0,sK1),sK2(sK0,sK1))),
inference(resolve,[status(thm)],[c_467,c_2258]) ).
cnf(c_2259,plain,
( subactivity_occurrence(sK0,sK5(tptp0,sK3(sK0,sK1),sK2(sK0,sK1)))
| ~ occurrence_of(sK5(tptp0,sK3(sK0,sK1),sK2(sK0,sK1)),tptp0) ),
inference(resolve,[status(thm)],[c_1503,c_408]) ).
cnf(c_1754,plain,
subactivity_occurrence(sK0,sK5(tptp0,sK3(sK0,sK1),sK2(sK0,sK1))),
inference(resolve,[status(thm)],[c_467,c_2259]) ).
cnf(c_2260,plain,
( B = A
| min_precedes(B,A,tptp0)
| min_precedes(A,B,tptp0)
| ~ subactivity_occurrence(B,sK5(tptp0,sK3(sK0,sK1),sK2(sK0,sK1)))
| ~ subactivity_occurrence(A,sK5(tptp0,sK3(sK0,sK1),sK2(sK0,sK1)))
| ~ arboreal(B)
| ~ arboreal(A) ),
inference(resolve,[status(thm)],[c_183,c_467]) ).
cnf(c_2261,plain,
( A = sK2(sK0,sK1)
| min_precedes(A,sK2(sK0,sK1),tptp0)
| min_precedes(sK2(sK0,sK1),A,tptp0)
| ~ subactivity_occurrence(A,sK5(tptp0,sK3(sK0,sK1),sK2(sK0,sK1)))
| ~ subactivity_occurrence(sK2(sK0,sK1),sK5(tptp0,sK3(sK0,sK1),sK2(sK0,sK1)))
| ~ arboreal(A) ),
inference(resolve,[status(thm)],[c_2260,c_485]) ).
cnf(c_2262,negated_conjecture,
( sK0 = sK2(sK0,sK1)
| min_precedes(sK0,sK2(sK0,sK1),tptp0)
| min_precedes(sK2(sK0,sK1),sK0,tptp0)
| ~ subactivity_occurrence(sK0,sK5(tptp0,sK3(sK0,sK1),sK2(sK0,sK1)))
| ~ subactivity_occurrence(sK2(sK0,sK1),sK5(tptp0,sK3(sK0,sK1),sK2(sK0,sK1))) ),
inference(resolve,[status(thm)],[c_2261,c_154]) ).
cnf(c_2263,negated_conjecture,
( sK0 = sK2(sK0,sK1)
| min_precedes(sK0,sK2(sK0,sK1),tptp0)
| min_precedes(sK2(sK0,sK1),sK0,tptp0)
| ~ subactivity_occurrence(sK0,sK5(tptp0,sK3(sK0,sK1),sK2(sK0,sK1))) ),
inference(resolve,[status(thm)],[c_2262,c_469]) ).
cnf(c_2264,negated_conjecture,
( sK0 = sK2(sK0,sK1)
| min_precedes(sK0,sK2(sK0,sK1),tptp0)
| min_precedes(sK2(sK0,sK1),sK0,tptp0) ),
inference(resolve,[status(thm)],[c_2263,c_1754]) ).
cnf(c_1817,negated_conjecture,
( sK2(sK0,sK1) = sK0
| min_precedes(sK0,sK2(sK0,sK1),tptp0)
| min_precedes(sK2(sK0,sK1),sK0,tptp0) ),
inference(copy,[status(thm)],[c_2264]) ).
cnf(c_2265,plain,
( earlier(sK2(sK0,sK1),sK0)
| sK2(sK0,sK1) = sK0
| min_precedes(sK0,sK2(sK0,sK1),tptp0) ),
inference(resolve,[status(thm)],[c_1817,c_216]) ).
cnf(c_1880,plain,
( sK2(sK0,sK1) = sK0
| min_precedes(sK0,sK2(sK0,sK1),tptp0) ),
inference(resolve,[status(thm)],[c_545,c_2265]) ).
cnf(c_2266,plain,
( min_precedes(sK4(sK0,sK1),sK2(sK0,sK1),tptp0)
| ~ legal(sK2(sK0,sK1))
| ~ earlier(sK4(sK0,sK1),sK2(sK0,sK1))
| sK2(sK0,sK1) = sK0 ),
inference(resolve,[status(thm)],[c_1880,c_393]) ).
cnf(c_2267,plain,
( min_precedes(sK4(sK0,sK1),sK2(sK0,sK1),tptp0)
| ~ legal(sK2(sK0,sK1))
| sK2(sK0,sK1) = sK0 ),
inference(resolve,[status(thm)],[c_539,c_2266]) ).
cnf(c_1883,plain,
( min_precedes(sK4(sK0,sK1),sK2(sK0,sK1),tptp0)
| sK2(sK0,sK1) = sK0 ),
inference(resolve,[status(thm)],[c_452,c_2267]) ).
cnf(c_2268,plain,
( ~ leaf(sK2(sK0,sK1),tptp0)
| ~ occurrence_of(sK2(sK0,sK1),tptp1)
| sK2(sK0,sK1) = sK0 ),
inference(resolve,[status(thm)],[c_1883,c_385]) ).
cnf(c_1949,plain,
( ~ occurrence_of(sK2(sK0,sK1),tptp1)
| sK2(sK0,sK1) = sK0 ),
inference(resolve,[status(thm)],[c_254,c_2268]) ).
cnf(c_2269,plain,
( occurrence_of(sK2(sK0,sK1),tptp1)
| ~ leaf(sK2(sK0,sK1),tptp0)
| ~ min_precedes(sK4(sK0,sK1),sK2(sK0,sK1),tptp0) ),
inference(resolve,[status(thm)],[c_384,c_256]) ).
cnf(c_2270,plain,
( sK2(sK0,sK1) = sK0
| occurrence_of(sK2(sK0,sK1),tptp1)
| ~ leaf(sK2(sK0,sK1),tptp0) ),
inference(resolve,[status(thm)],[c_2269,c_1883]) ).
cnf(c_1985,plain,
( sK2(sK0,sK1) = sK0
| occurrence_of(sK2(sK0,sK1),tptp1) ),
inference(resolve,[status(thm)],[c_2270,c_254]) ).
cnf(c_2271,plain,
( sK2(sK0,sK1) = sK0
| sK2(sK0,sK1) = sK0 ),
inference(resolve,[status(thm)],[c_1985,c_1949]) ).
cnf(c_1986,plain,
sK2(sK0,sK1) = sK0,
inference(copy,[status(thm)],[c_2271]) ).
cnf(c_2272,plain,
~ earlier(sK0,sK4(sK0,sK1)),
inference(paramod,[status(thm)],[c_1986,c_569]) ).
cnf(c_2235,plain,
$false,
inference(resolve,[status(thm)],[c_388,c_2272]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO014+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.34 % Computer : n019.cluster.edu
% 0.10/0.34 % Model : x86_64 x86_64
% 0.10/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.34 % Memory : 8046.5625MB
% 0.10/0.34 % OS : Linux 6.8.0-71-generic
% 0.10/0.34 % CPULimit : 300
% 0.10/0.34 % WCLimit : 300
% 0.10/0.34 % DateTime : Sat Sep 26 04:59:21 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.35 % Process 440921 was started by sandbox on n019,
% 0.10/0.35 % Sat Sep 26 04:59:21 2026
% 0.10/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.37
% 0.10/0.37 % From the command line: assign(max_seconds, 300).
% 7.08/1.40
% 7.08/1.40 % Assigning unary symbol f1 kb_weight 0 and highest precedence (38).
% 7.08/1.40
% 7.08/1.40 % given #500 (A,wt=46): 411 -occurrence_of(A,f3(tptp0,c1,f16(c1,c2))) | -occurrence_of(B,tptp0) | subactivity_occurrence(A,B) | -subactivity_occurrence(f13(f3(tptp0,c1,f16(c1,c2)),tptp0,A,B),A). [resolve(382,a,136,e)].
% 7.08/1.40
% 7.08/1.40 % SZS status Theorem for theBenchmark
% 7.08/1.40
% 7.08/1.40 % Proof 1 at 0.91 (+ 0.09) seconds.
% 7.08/1.40 % Length of proof is 78.
% 7.08/1.40 % Level of proof is 13.
% 7.08/1.40 % Maximum clause weight is 31.000.
% 7.08/1.40 % Given clauses 558.
% 7.08/1.40
% 7.08/1.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------