%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PRO016+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 : n004.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:59 AM UTC 2026
% Result : Theorem 22.08s 3.26s
% Output : CNFRefutation 22.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 15
% Syntax : Number of formulae : 128 ( 40 unt; 0 def)
% Number of atoms : 508 ( 15 equ)
% Maximal formula atoms : 88 ( 3 avg)
% Number of connectives : 603 ( 223 ~; 264 |; 97 &)
% ( 4 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 7 con; 0-2 aty)
% Number of variables : 191 ( 7 sgn 86 !; 21 ?)
% Comments :
%------------------------------------------------------------------------------
fof(sos_05,axiom,
! [X10,X11,X12] :
( ( earlier(X11,X12)
& earlier(X10,X11) )
=> earlier(X10,X12) ),
file('theBenchmark.p',sos_05) ).
fof(sos_07,axiom,
! [X16,X17] :
( occurrence_of(X16,X17)
=> ( arboreal(X16)
<=> atomic(X17) ) ),
file('theBenchmark.p',sos_07) ).
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_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_34,axiom,
! [X102,X103] :
( leaf_occ(X102,X103)
<=> ? [X104] :
( leaf(X102,X104)
& subactivity_occurrence(X102,X103)
& occurrence_of(X103,X104) ) ),
file('theBenchmark.p',sos_34) ).
fof(sos_36,axiom,
! [X109,X110,X111,X112] :
( ( leaf_occ(X110,X111)
& leaf_occ(X109,X111)
& ~ atomic(X112)
& occurrence_of(X111,X112) )
=> X109 = X110 ),
file('theBenchmark.p',sos_36) ).
fof(sos_37,axiom,
! [X113,X114,X115] :
( ( leaf_occ(X114,X113)
& occurrence_of(X113,X115) )
=> ~ ? [X116] : min_precedes(X114,X116,X115) ),
file('theBenchmark.p',sos_37) ).
fof(sos_40,axiom,
! [X126,X127,X128,X129] :
( ( next_subocc(X128,X126,X129)
& next_subocc(X127,X126,X129) )
=> X127 = X128 ),
file('theBenchmark.p',sos_40) ).
fof(sos_49,axiom,
! [X161,X162] :
( ( ~ leaf_occ(X161,X162)
& arboreal(X161)
& subactivity_occurrence(X161,X162)
& occurrence_of(X162,tptp0) )
=> ? [X163,X164,X165] :
( leaf_occ(X165,X162)
& next_subocc(X164,X165,tptp0)
& ( occurrence_of(X165,tptp2)
| occurrence_of(X165,tptp1) )
& next_subocc(X163,X164,tptp0)
& occurrence_of(X164,tptp4)
& next_subocc(X161,X163,tptp0)
& occurrence_of(X163,tptp3) ) ),
file('theBenchmark.p',sos_49) ).
fof(goals,conjecture,
! [X166,X167] :
( ( ~ leaf_occ(X166,X167)
& arboreal(X166)
& subactivity_occurrence(X166,X167)
& occurrence_of(X167,tptp0) )
=> ? [X168,X169] :
( ( occurrence_of(X169,tptp2)
=> ~ ? [X171] :
( min_precedes(X168,X171,tptp0)
& occurrence_of(X171,tptp1) ) )
& ( occurrence_of(X169,tptp1)
=> ~ ? [X170] :
( min_precedes(X168,X170,tptp0)
& occurrence_of(X170,tptp2) ) )
& leaf_occ(X169,X167)
& min_precedes(X168,X169,tptp0)
& ( occurrence_of(X169,tptp2)
| occurrence_of(X169,tptp1) )
& next_subocc(X166,X168,tptp0)
& occurrence_of(X168,tptp3) ) ),
file('theBenchmark.p',goals) ).
fof(goals_neg,negated_conjecture,
~ ! [X166,X167] :
( ( ~ leaf_occ(X166,X167)
& arboreal(X166)
& subactivity_occurrence(X166,X167)
& occurrence_of(X167,tptp0) )
=> ? [X168,X169] :
( ( occurrence_of(X169,tptp2)
=> ~ ? [X171] :
( min_precedes(X168,X171,tptp0)
& occurrence_of(X171,tptp1) ) )
& ( occurrence_of(X169,tptp1)
=> ~ ? [X170] :
( min_precedes(X168,X170,tptp0)
& occurrence_of(X170,tptp2) ) )
& leaf_occ(X169,X167)
& min_precedes(X168,X169,tptp0)
& ( occurrence_of(X169,tptp2)
| occurrence_of(X169,tptp1) )
& next_subocc(X166,X168,tptp0)
& occurrence_of(X168,tptp3) ) ),
inference(assume_negation,[status(cth)],[goals]) ).
cnf(c_74,plain,
( precedes(A,B)
| ~ min_precedes(A,B,C) ),
inference(clausify,[status(thm)],[sos_15]) ).
cnf(c_75,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_77,plain,
( ~ legal(B)
| ~ earlier(A,B)
| precedes(A,B) ),
inference(clausify,[status(thm)],[sos_10]) ).
cnf(c_78,plain,
( legal(B)
| ~ precedes(A,B) ),
inference(clausify,[status(thm)],[sos_10]) ).
cnf(c_79,plain,
( earlier(A,B)
| ~ precedes(A,B) ),
inference(clausify,[status(thm)],[sos_10]) ).
cnf(c_180,plain,
( ~ min_precedes(A,B,C)
| earlier(A,B) ),
inference(resolve,[status(thm)],[c_79,c_74]) ).
cnf(c_181,plain,
( ~ min_precedes(B,A,C)
| legal(A) ),
inference(resolve,[status(thm)],[c_78,c_74]) ).
cnf(c_183,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_77,c_75]) ).
cnf(c_191,plain,
( earlier(A,C)
| ~ earlier(B,C)
| ~ earlier(A,B) ),
inference(clausify,[status(thm)],[sos_05]) ).
cnf(c_194,plain,
( ~ atomic(B)
| arboreal(A)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_07]) ).
cnf(c_201,plain,
( min_precedes(A,B,C)
| ~ next_subocc(A,B,C) ),
inference(clausify,[status(thm)],[sos_22]) ).
cnf(c_202,plain,
( ~ min_precedes(D,B,C)
| ~ min_precedes(A,D,C)
| ~ next_subocc(A,B,C) ),
inference(clausify,[status(thm)],[sos_22]) ).
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_217,plain,
( subactivity_occurrence(A,B)
| ~ leaf_occ(A,B) ),
inference(clausify,[status(thm)],[sos_34]) ).
cnf(c_219,plain,
( D = C
| ~ leaf_occ(D,A)
| ~ leaf_occ(C,A)
| atomic(B)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_36]) ).
cnf(c_220,plain,
( ~ min_precedes(C,D,B)
| ~ leaf_occ(C,A)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_37]) ).
cnf(c_223,plain,
( D = A
| ~ next_subocc(D,B,C)
| ~ next_subocc(A,B,C) ),
inference(clausify,[status(thm)],[sos_40]) ).
fof(nnf_50,plain,
! [X161,X162] :
( ? [X163,X164,X165] :
( leaf_occ(X165,X162)
& next_subocc(X164,X165,tptp0)
& ( occurrence_of(X165,tptp2)
| occurrence_of(X165,tptp1) )
& next_subocc(X163,X164,tptp0)
& occurrence_of(X164,tptp4)
& next_subocc(X161,X163,tptp0)
& occurrence_of(X163,tptp3) )
| leaf_occ(X161,X162)
| ~ arboreal(X161)
| ~ subactivity_occurrence(X161,X162)
| ~ occurrence_of(X162,tptp0) ),
inference(fof_nnf,[status(thm)],[sos_49]) ).
fof(sk_sos_49_sk,plain,
! [X161,X162] :
( ( leaf_occ(sK2(X161,X162),X162)
& next_subocc(sK1(X161,X162),sK2(X161,X162),tptp0)
& ( occurrence_of(sK2(X161,X162),tptp2)
| occurrence_of(sK2(X161,X162),tptp1) )
& next_subocc(sK0(X161,X162),sK1(X161,X162),tptp0)
& occurrence_of(sK1(X161,X162),tptp4)
& next_subocc(X161,sK0(X161,X162),tptp0)
& occurrence_of(sK0(X161,X162),tptp3) )
| leaf_occ(X161,X162)
| ~ arboreal(X161)
| ~ subactivity_occurrence(X161,X162)
| ~ occurrence_of(X162,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X163,sK0(X161,X162)),skolemize(X164,sK1(X161,X162)),skolemize(X165,sK2(X161,X162))],[nnf_50]) ).
fof(sk_sos_49,plain,
( ! [VAR_0,VAR_1] :
( leaf_occ(sK2(VAR_1,VAR_0),VAR_0)
| 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(sK1(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),tptp2)
| occurrence_of(sK2(VAR_1,VAR_0),tptp1)
| 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(sK0(VAR_1,VAR_0),sK1(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(sK1(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,sK0(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(sK0(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_49_sk]) ).
cnf(c_233,plain,
( next_subocc(B,sK0(B,A),tptp0)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
cnf(c_234,plain,
( occurrence_of(sK1(B,A),tptp4)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
cnf(c_235,plain,
( next_subocc(sK0(B,A),sK1(B,A),tptp0)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
cnf(c_237,plain,
( next_subocc(sK1(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_49]) ).
cnf(c_238,plain,
( leaf_occ(sK2(B,A),A)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ 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_239,plain,
~ atomic(tptp0),
inference(clausify,[status(thm)],[sos_51]) ).
fof(sos_52,axiom,
atomic(tptp4),
file('theBenchmark.p',sos_52) ).
cnf(c_240,plain,
atomic(tptp4),
inference(clausify,[status(thm)],[sos_52]) ).
fof(nnf_51,plain,
? [X166,X167] :
( ! [X168,X169] :
( ( ? [X171] :
( min_precedes(X168,X171,tptp0)
& occurrence_of(X171,tptp1) )
& occurrence_of(X169,tptp2) )
| ( ? [X170] :
( min_precedes(X168,X170,tptp0)
& occurrence_of(X170,tptp2) )
& occurrence_of(X169,tptp1) )
| ~ leaf_occ(X169,X167)
| ~ min_precedes(X168,X169,tptp0)
| ( ~ occurrence_of(X169,tptp2)
& ~ occurrence_of(X169,tptp1) )
| ~ next_subocc(X166,X168,tptp0)
| ~ occurrence_of(X168,tptp3) )
& ~ leaf_occ(X166,X167)
& arboreal(X166)
& subactivity_occurrence(X166,X167)
& occurrence_of(X167,tptp0) ),
inference(fof_nnf,[status(thm)],[goals_neg]) ).
fof(sk_goals_neg_sk,plain,
( ! [X168,X169] :
( ( min_precedes(X168,sK8(X168,X169),tptp0)
& occurrence_of(sK8(X168,X169),tptp1)
& occurrence_of(X169,tptp2) )
| ( min_precedes(X168,sK7(X168,X169),tptp0)
& occurrence_of(sK7(X168,X169),tptp2)
& occurrence_of(X169,tptp1) )
| ~ leaf_occ(X169,sK3)
| ~ min_precedes(X168,X169,tptp0)
| ( ~ occurrence_of(X169,tptp2)
& ~ occurrence_of(X169,tptp1) )
| ~ next_subocc(sK4,X168,tptp0)
| ~ occurrence_of(X168,tptp3) )
& ~ leaf_occ(sK4,sK3)
& arboreal(sK4)
& subactivity_occurrence(sK4,sK3)
& occurrence_of(sK3,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK7,sK8]),skolemize(X166,sK4),skolemize(X167,sK3),skolemize(X170,sK7(X168,X169)),skolemize(X171,sK8(X168,X169))],[nnf_51]) ).
fof(sk_goals_neg,plain,
( ! [VAR_0,VAR_1] :
( min_precedes(VAR_0,sK8(VAR_0,VAR_1),tptp0)
| min_precedes(VAR_0,sK7(VAR_0,VAR_1),tptp0)
| ~ leaf_occ(VAR_1,sK3)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp2)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( occurrence_of(sK8(VAR_0,VAR_1),tptp1)
| min_precedes(VAR_0,sK7(VAR_0,VAR_1),tptp0)
| ~ leaf_occ(VAR_1,sK3)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp2)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( min_precedes(VAR_0,sK8(VAR_0,VAR_1),tptp0)
| occurrence_of(sK7(VAR_0,VAR_1),tptp2)
| ~ leaf_occ(VAR_1,sK3)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp2)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( occurrence_of(sK8(VAR_0,VAR_1),tptp1)
| occurrence_of(sK7(VAR_0,VAR_1),tptp2)
| ~ leaf_occ(VAR_1,sK3)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp2)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( min_precedes(VAR_0,sK8(VAR_0,VAR_1),tptp0)
| occurrence_of(VAR_1,tptp1)
| ~ leaf_occ(VAR_1,sK3)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp2)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( occurrence_of(sK8(VAR_0,VAR_1),tptp1)
| occurrence_of(VAR_1,tptp1)
| ~ leaf_occ(VAR_1,sK3)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp2)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( min_precedes(VAR_0,sK8(VAR_0,VAR_1),tptp0)
| min_precedes(VAR_0,sK7(VAR_0,VAR_1),tptp0)
| ~ leaf_occ(VAR_1,sK3)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp1)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( occurrence_of(sK8(VAR_0,VAR_1),tptp1)
| min_precedes(VAR_0,sK7(VAR_0,VAR_1),tptp0)
| ~ leaf_occ(VAR_1,sK3)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp1)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( occurrence_of(VAR_1,tptp2)
| min_precedes(VAR_0,sK7(VAR_0,VAR_1),tptp0)
| ~ leaf_occ(VAR_1,sK3)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp1)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( min_precedes(VAR_0,sK8(VAR_0,VAR_1),tptp0)
| occurrence_of(sK7(VAR_0,VAR_1),tptp2)
| ~ leaf_occ(VAR_1,sK3)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp1)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( occurrence_of(sK8(VAR_0,VAR_1),tptp1)
| occurrence_of(sK7(VAR_0,VAR_1),tptp2)
| ~ leaf_occ(VAR_1,sK3)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp1)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( occurrence_of(VAR_1,tptp2)
| occurrence_of(sK7(VAR_0,VAR_1),tptp2)
| ~ leaf_occ(VAR_1,sK3)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp1)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ~ leaf_occ(sK4,sK3)
& arboreal(sK4)
& subactivity_occurrence(sK4,sK3)
& occurrence_of(sK3,tptp0) ),
inference(cnf_transformation,[status(thm)],[sk_goals_neg_sk]) ).
cnf(c_251,negated_conjecture,
occurrence_of(sK3,tptp0),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_252,negated_conjecture,
subactivity_occurrence(sK4,sK3),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_253,negated_conjecture,
arboreal(sK4),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_254,negated_conjecture,
~ leaf_occ(sK4,sK3),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_365,plain,
( arboreal(A)
| ~ occurrence_of(A,tptp4) ),
inference(resolve,[status(thm)],[c_240,c_194]) ).
cnf(c_372,plain,
( leaf_occ(sK2(A,sK3),sK3)
| leaf_occ(A,sK3)
| ~ arboreal(A)
| ~ subactivity_occurrence(A,sK3) ),
inference(resolve,[status(thm)],[c_251,c_238]) ).
cnf(c_373,plain,
( next_subocc(sK1(A,sK3),sK2(A,sK3),tptp0)
| leaf_occ(A,sK3)
| ~ arboreal(A)
| ~ subactivity_occurrence(A,sK3) ),
inference(resolve,[status(thm)],[c_251,c_237]) ).
cnf(c_375,plain,
( next_subocc(sK0(A,sK3),sK1(A,sK3),tptp0)
| leaf_occ(A,sK3)
| ~ arboreal(A)
| ~ subactivity_occurrence(A,sK3) ),
inference(resolve,[status(thm)],[c_251,c_235]) ).
cnf(c_376,plain,
( occurrence_of(sK1(A,sK3),tptp4)
| leaf_occ(A,sK3)
| ~ arboreal(A)
| ~ subactivity_occurrence(A,sK3) ),
inference(resolve,[status(thm)],[c_251,c_234]) ).
cnf(c_377,plain,
( next_subocc(A,sK0(A,sK3),tptp0)
| leaf_occ(A,sK3)
| ~ arboreal(A)
| ~ subactivity_occurrence(A,sK3) ),
inference(resolve,[status(thm)],[c_251,c_233]) ).
cnf(c_386,plain,
( ~ min_precedes(A,B,tptp0)
| ~ leaf_occ(A,sK3) ),
inference(resolve,[status(thm)],[c_251,c_220]) ).
cnf(c_10014,negated_conjecture,
( B = A
| ~ leaf_occ(B,sK3)
| ~ leaf_occ(A,sK3)
| atomic(tptp0) ),
inference(resolve,[status(thm)],[c_251,c_219]) ).
cnf(c_387,negated_conjecture,
( B = A
| ~ leaf_occ(B,sK3)
| ~ leaf_occ(A,sK3) ),
inference(resolve,[status(thm)],[c_239,c_10014]) ).
cnf(c_389,plain,
( subactivity_occurrence(A,sK3)
| ~ subactivity_occurrence(B,sK3)
| ~ min_precedes(A,B,tptp0) ),
inference(resolve,[status(thm)],[c_251,c_212]) ).
cnf(c_10015,negated_conjecture,
( leaf_occ(sK2(sK4,sK3),sK3)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4)
| ~ occurrence_of(sK3,tptp0) ),
inference(resolve,[status(thm)],[c_252,c_238]) ).
cnf(c_10016,negated_conjecture,
( leaf_occ(sK2(sK4,sK3),sK3)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4) ),
inference(resolve,[status(thm)],[c_251,c_10015]) ).
cnf(c_10017,negated_conjecture,
( leaf_occ(sK2(sK4,sK3),sK3)
| leaf_occ(sK4,sK3) ),
inference(resolve,[status(thm)],[c_253,c_10016]) ).
cnf(c_403,negated_conjecture,
leaf_occ(sK2(sK4,sK3),sK3),
inference(resolve,[status(thm)],[c_254,c_10017]) ).
cnf(c_10018,negated_conjecture,
( next_subocc(sK1(sK4,sK3),sK2(sK4,sK3),tptp0)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4)
| ~ occurrence_of(sK3,tptp0) ),
inference(resolve,[status(thm)],[c_252,c_237]) ).
cnf(c_10019,negated_conjecture,
( next_subocc(sK1(sK4,sK3),sK2(sK4,sK3),tptp0)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4) ),
inference(resolve,[status(thm)],[c_251,c_10018]) ).
cnf(c_10020,negated_conjecture,
( next_subocc(sK1(sK4,sK3),sK2(sK4,sK3),tptp0)
| leaf_occ(sK4,sK3) ),
inference(resolve,[status(thm)],[c_253,c_10019]) ).
cnf(c_404,negated_conjecture,
next_subocc(sK1(sK4,sK3),sK2(sK4,sK3),tptp0),
inference(resolve,[status(thm)],[c_254,c_10020]) ).
cnf(c_10021,negated_conjecture,
( next_subocc(sK0(sK4,sK3),sK1(sK4,sK3),tptp0)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4)
| ~ occurrence_of(sK3,tptp0) ),
inference(resolve,[status(thm)],[c_252,c_235]) ).
cnf(c_10022,negated_conjecture,
( next_subocc(sK0(sK4,sK3),sK1(sK4,sK3),tptp0)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4) ),
inference(resolve,[status(thm)],[c_251,c_10021]) ).
cnf(c_10023,negated_conjecture,
( next_subocc(sK0(sK4,sK3),sK1(sK4,sK3),tptp0)
| leaf_occ(sK4,sK3) ),
inference(resolve,[status(thm)],[c_253,c_10022]) ).
cnf(c_406,negated_conjecture,
next_subocc(sK0(sK4,sK3),sK1(sK4,sK3),tptp0),
inference(resolve,[status(thm)],[c_254,c_10023]) ).
cnf(c_10024,negated_conjecture,
( occurrence_of(sK1(sK4,sK3),tptp4)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4)
| ~ occurrence_of(sK3,tptp0) ),
inference(resolve,[status(thm)],[c_252,c_234]) ).
cnf(c_10025,negated_conjecture,
( occurrence_of(sK1(sK4,sK3),tptp4)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4) ),
inference(resolve,[status(thm)],[c_251,c_10024]) ).
cnf(c_10026,negated_conjecture,
( occurrence_of(sK1(sK4,sK3),tptp4)
| leaf_occ(sK4,sK3) ),
inference(resolve,[status(thm)],[c_253,c_10025]) ).
cnf(c_407,negated_conjecture,
occurrence_of(sK1(sK4,sK3),tptp4),
inference(resolve,[status(thm)],[c_254,c_10026]) ).
cnf(c_650,plain,
( sK2(sK4,sK3) = A
| ~ leaf_occ(A,sK3) ),
inference(resolve,[status(thm)],[c_403,c_387]) ).
cnf(c_669,plain,
subactivity_occurrence(sK2(sK4,sK3),sK3),
inference(resolve,[status(thm)],[c_403,c_217]) ).
cnf(c_685,plain,
arboreal(sK1(sK4,sK3)),
inference(resolve,[status(thm)],[c_407,c_365]) ).
cnf(c_725,plain,
( next_subocc(sK1(sK1(sK4,sK3),sK3),sK2(sK1(sK4,sK3),sK3),tptp0)
| leaf_occ(sK1(sK4,sK3),sK3)
| ~ subactivity_occurrence(sK1(sK4,sK3),sK3) ),
inference(resolve,[status(thm)],[c_685,c_373]) ).
cnf(c_726,plain,
( leaf_occ(sK2(sK1(sK4,sK3),sK3),sK3)
| leaf_occ(sK1(sK4,sK3),sK3)
| ~ subactivity_occurrence(sK1(sK4,sK3),sK3) ),
inference(resolve,[status(thm)],[c_685,c_372]) ).
cnf(c_789,plain,
( occurrence_of(sK1(sK1(sK4,sK3),sK3),tptp4)
| leaf_occ(sK1(sK4,sK3),sK3)
| ~ subactivity_occurrence(sK1(sK4,sK3),sK3) ),
inference(resolve,[status(thm)],[c_376,c_685]) ).
cnf(c_866,plain,
( next_subocc(sK1(sK4,sK3),sK0(sK1(sK4,sK3),sK3),tptp0)
| leaf_occ(sK1(sK4,sK3),sK3)
| ~ subactivity_occurrence(sK1(sK4,sK3),sK3) ),
inference(resolve,[status(thm)],[c_377,c_685]) ).
cnf(c_1037,plain,
( sK1(sK4,sK3) = A
| ~ next_subocc(A,sK2(sK4,sK3),tptp0) ),
inference(resolve,[status(thm)],[c_404,c_223]) ).
cnf(c_1039,plain,
( ~ min_precedes(A,sK2(sK4,sK3),tptp0)
| ~ min_precedes(sK1(sK4,sK3),A,tptp0) ),
inference(resolve,[status(thm)],[c_404,c_202]) ).
cnf(c_1040,plain,
min_precedes(sK1(sK4,sK3),sK2(sK4,sK3),tptp0),
inference(resolve,[status(thm)],[c_404,c_201]) ).
cnf(c_1054,plain,
( sK0(sK4,sK3) = A
| ~ next_subocc(A,sK1(sK4,sK3),tptp0) ),
inference(resolve,[status(thm)],[c_406,c_223]) ).
cnf(c_1057,plain,
min_precedes(sK0(sK4,sK3),sK1(sK4,sK3),tptp0),
inference(resolve,[status(thm)],[c_406,c_201]) ).
cnf(c_10027,plain,
( subactivity_occurrence(sK1(sK4,sK3),sK3)
| ~ subactivity_occurrence(sK2(sK4,sK3),sK3) ),
inference(resolve,[status(thm)],[c_1040,c_389]) ).
cnf(c_1144,plain,
subactivity_occurrence(sK1(sK4,sK3),sK3),
inference(resolve,[status(thm)],[c_669,c_10027]) ).
cnf(c_1145,plain,
~ leaf_occ(sK1(sK4,sK3),sK3),
inference(resolve,[status(thm)],[c_1040,c_386]) ).
cnf(c_1193,plain,
( min_precedes(A,sK2(sK4,sK3),tptp0)
| ~ min_precedes(sK1(sK4,sK3),A,tptp0)
| ~ legal(sK2(sK4,sK3))
| ~ earlier(A,sK2(sK4,sK3)) ),
inference(resolve,[status(thm)],[c_1040,c_183]) ).
cnf(c_1197,plain,
legal(sK2(sK4,sK3)),
inference(resolve,[status(thm)],[c_1040,c_181]) ).
cnf(c_1198,plain,
earlier(sK1(sK4,sK3),sK2(sK4,sK3)),
inference(resolve,[status(thm)],[c_1040,c_180]) ).
cnf(c_10028,plain,
( next_subocc(sK1(sK4,sK3),sK0(sK1(sK4,sK3),sK3),tptp0)
| leaf_occ(sK1(sK4,sK3),sK3) ),
inference(resolve,[status(thm)],[c_1144,c_866]) ).
cnf(c_1212,plain,
next_subocc(sK1(sK4,sK3),sK0(sK1(sK4,sK3),sK3),tptp0),
inference(resolve,[status(thm)],[c_1145,c_10028]) ).
cnf(c_10029,plain,
( occurrence_of(sK1(sK1(sK4,sK3),sK3),tptp4)
| leaf_occ(sK1(sK4,sK3),sK3) ),
inference(resolve,[status(thm)],[c_1144,c_789]) ).
cnf(c_1213,plain,
occurrence_of(sK1(sK1(sK4,sK3),sK3),tptp4),
inference(resolve,[status(thm)],[c_1145,c_10029]) ).
cnf(c_10030,plain,
( leaf_occ(sK2(sK1(sK4,sK3),sK3),sK3)
| leaf_occ(sK1(sK4,sK3),sK3) ),
inference(resolve,[status(thm)],[c_1144,c_726]) ).
cnf(c_1214,plain,
leaf_occ(sK2(sK1(sK4,sK3),sK3),sK3),
inference(resolve,[status(thm)],[c_1145,c_10030]) ).
cnf(c_10031,plain,
( next_subocc(sK1(sK1(sK4,sK3),sK3),sK2(sK1(sK4,sK3),sK3),tptp0)
| leaf_occ(sK1(sK4,sK3),sK3) ),
inference(resolve,[status(thm)],[c_1144,c_725]) ).
cnf(c_1215,plain,
next_subocc(sK1(sK1(sK4,sK3),sK3),sK2(sK1(sK4,sK3),sK3),tptp0),
inference(resolve,[status(thm)],[c_1145,c_10031]) ).
cnf(c_1222,plain,
( min_precedes(A,sK2(sK4,sK3),tptp0)
| ~ min_precedes(sK1(sK4,sK3),A,tptp0)
| ~ earlier(A,sK2(sK4,sK3)) ),
inference(resolve,[status(thm)],[c_1197,c_1193]) ).
cnf(c_1323,plain,
( earlier(A,sK2(sK4,sK3))
| ~ earlier(A,sK1(sK4,sK3)) ),
inference(resolve,[status(thm)],[c_1198,c_191]) ).
cnf(c_1391,plain,
earlier(sK0(sK4,sK3),sK1(sK4,sK3)),
inference(resolve,[status(thm)],[c_1057,c_180]) ).
cnf(c_1595,plain,
earlier(sK0(sK4,sK3),sK2(sK4,sK3)),
inference(resolve,[status(thm)],[c_1323,c_1391]) ).
cnf(c_10032,plain,
sK2(sK4,sK3) = sK2(sK1(sK4,sK3),sK3),
inference(resolve,[status(thm)],[c_1214,c_650]) ).
cnf(c_2356,plain,
sK2(sK1(sK4,sK3),sK3) = sK2(sK4,sK3),
inference(copy,[status(thm)],[c_10032]) ).
cnf(c_2357,plain,
next_subocc(sK1(sK1(sK4,sK3),sK3),sK2(sK4,sK3),tptp0),
inference(paramod,[status(thm)],[c_2356,c_1215]) ).
cnf(c_3359,plain,
arboreal(sK1(sK1(sK4,sK3),sK3)),
inference(resolve,[status(thm)],[c_1213,c_365]) ).
cnf(c_3406,plain,
( next_subocc(sK0(sK1(sK1(sK4,sK3),sK3),sK3),sK1(sK1(sK1(sK4,sK3),sK3),sK3),tptp0)
| leaf_occ(sK1(sK1(sK4,sK3),sK3),sK3)
| ~ subactivity_occurrence(sK1(sK1(sK4,sK3),sK3),sK3) ),
inference(resolve,[status(thm)],[c_3359,c_375]) ).
cnf(c_4446,plain,
min_precedes(sK1(sK4,sK3),sK0(sK1(sK4,sK3),sK3),tptp0),
inference(resolve,[status(thm)],[c_1212,c_201]) ).
cnf(c_5598,plain,
~ min_precedes(sK0(sK1(sK4,sK3),sK3),sK2(sK4,sK3),tptp0),
inference(resolve,[status(thm)],[c_4446,c_1039]) ).
cnf(c_10033,plain,
( min_precedes(sK0(sK1(sK4,sK3),sK3),sK2(sK4,sK3),tptp0)
| ~ earlier(sK0(sK1(sK4,sK3),sK3),sK2(sK4,sK3)) ),
inference(resolve,[status(thm)],[c_1222,c_4446]) ).
cnf(c_9636,plain,
~ earlier(sK0(sK1(sK4,sK3),sK3),sK2(sK4,sK3)),
inference(resolve,[status(thm)],[c_5598,c_10033]) ).
cnf(c_10034,plain,
sK1(sK4,sK3) = sK1(sK1(sK4,sK3),sK3),
inference(resolve,[status(thm)],[c_2357,c_1037]) ).
cnf(c_10007,plain,
sK1(sK1(sK4,sK3),sK3) = sK1(sK4,sK3),
inference(copy,[status(thm)],[c_10034]) ).
cnf(c_10035,plain,
( next_subocc(sK0(sK1(sK1(sK4,sK3),sK3),sK3),sK1(sK1(sK1(sK4,sK3),sK3),sK3),tptp0)
| leaf_occ(sK1(sK1(sK4,sK3),sK3),sK3)
| ~ subactivity_occurrence(sK1(sK4,sK3),sK3) ),
inference(paramod,[status(thm)],[c_10007,c_3406]) ).
cnf(c_10036,plain,
( next_subocc(sK0(sK1(sK1(sK4,sK3),sK3),sK3),sK1(sK1(sK1(sK4,sK3),sK3),sK3),tptp0)
| leaf_occ(sK1(sK4,sK3),sK3)
| ~ subactivity_occurrence(sK1(sK4,sK3),sK3) ),
inference(paramod,[status(thm)],[c_10007,c_10035]) ).
cnf(c_10037,plain,
( next_subocc(sK0(sK1(sK4,sK3),sK3),sK1(sK1(sK1(sK4,sK3),sK3),sK3),tptp0)
| leaf_occ(sK1(sK4,sK3),sK3)
| ~ subactivity_occurrence(sK1(sK4,sK3),sK3) ),
inference(paramod,[status(thm)],[c_10007,c_10036]) ).
cnf(c_10038,plain,
( next_subocc(sK0(sK1(sK4,sK3),sK3),sK1(sK1(sK4,sK3),sK3),tptp0)
| leaf_occ(sK1(sK4,sK3),sK3)
| ~ subactivity_occurrence(sK1(sK4,sK3),sK3) ),
inference(paramod,[status(thm)],[c_10007,c_10037]) ).
cnf(c_10039,plain,
( next_subocc(sK0(sK1(sK4,sK3),sK3),sK1(sK4,sK3),tptp0)
| leaf_occ(sK1(sK4,sK3),sK3)
| ~ subactivity_occurrence(sK1(sK4,sK3),sK3) ),
inference(paramod,[status(thm)],[c_10007,c_10038]) ).
cnf(c_10040,plain,
( next_subocc(sK0(sK1(sK4,sK3),sK3),sK1(sK4,sK3),tptp0)
| leaf_occ(sK1(sK4,sK3),sK3) ),
inference(resolve,[status(thm)],[c_1144,c_10039]) ).
cnf(c_10008,plain,
next_subocc(sK0(sK1(sK4,sK3),sK3),sK1(sK4,sK3),tptp0),
inference(resolve,[status(thm)],[c_1145,c_10040]) ).
cnf(c_10041,plain,
sK0(sK4,sK3) = sK0(sK1(sK4,sK3),sK3),
inference(resolve,[status(thm)],[c_10008,c_1054]) ).
cnf(c_10012,plain,
sK0(sK1(sK4,sK3),sK3) = sK0(sK4,sK3),
inference(copy,[status(thm)],[c_10041]) ).
cnf(c_10042,plain,
~ earlier(sK0(sK4,sK3),sK2(sK4,sK3)),
inference(paramod,[status(thm)],[c_10012,c_9636]) ).
cnf(c_10013,plain,
$false,
inference(resolve,[status(thm)],[c_1595,c_10042]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO016+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n004.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sat Sep 26 05:00:23 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/0.35 % Process 860191 was started by sandbox2 on n004,
% 0.07/0.35 % Sat Sep 26 05:00:23 2026
% 0.07/0.35 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.12/0.36
% 0.12/0.36 % From the command line: assign(max_seconds, 300).
% 22.08/3.26
% 22.08/3.26 % Assigning unary symbol f1 kb_weight 0 and highest precedence (40).
% 22.08/3.26
% 22.08/3.26 % given #500 (T,wt=20): 1830 f12(tptp0,c2) = c1 | earlier(c1,f7(c1,tptp0)). [resolve(1713,b,180,b)].
% 22.08/3.26
% 22.08/3.26 % given #1000 (T,wt=25): 1815 f12(tptp0,c2) = c1 | -next_subocc(A,f7(c1,tptp0),tptp0) | -min_precedes(A,c1,tptp0). [resolve(1713,b,202,c)].
% 22.08/3.26
% 22.08/3.26 % given #1500 (W,wt=25): 7072 root_occ(c1,f10(tptp0,f17(c1,c2),f18(c1,c2))). [back_rewrite(6442),rewrite([7017(3)])].
% 22.08/3.26
% 22.08/3.26 % SZS status Theorem for theBenchmark
% 22.08/3.26
% 22.08/3.26 % Proof 1 at 2.09 (+ 0.44) seconds.
% 22.08/3.26 % Length of proof is 90.
% 22.08/3.26 % Level of proof is 11.
% 22.08/3.26 % Maximum clause weight is 60.000.
% 22.08/3.26 % Given clauses 1826.
% 22.08/3.26
% 22.08/3.26 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------