%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PRO014+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 : n014.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 4.01s 0.94s
% Output : CNFRefutation 4.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 13
% Syntax : Number of formulae : 121 ( 29 unt; 0 def)
% Number of atoms : 427 ( 14 equ)
% Maximal formula atoms : 36 ( 3 avg)
% Number of connectives : 492 ( 186 ~; 218 |; 75 &)
% ( 3 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 7 con; 0-2 aty)
% Number of variables : 161 ( 5 sgn 69 !; 16 ?)
% 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_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_43,axiom,
! [X138,X139,X140,X141] :
( ( ~ min_precedes(X140,X141,X138)
& arboreal(X140)
& leaf_occ(X141,X139)
& subactivity_occurrence(X140,X139)
& occurrence_of(X139,X138) )
=> X141 = X140 ),
file('theBenchmark.p',sos_43) ).
fof(sos_45,axiom,
! [X145,X146] :
( ( ~ atomic(X146)
& leaf(X145,X146) )
=> ? [X147] :
( leaf_occ(X145,X147)
& occurrence_of(X147,X146) ) ),
file('theBenchmark.p',sos_45) ).
fof(sos_49,axiom,
! [X161,X162] :
( ( ~ leaf_occ(X161,X162)
& arboreal(X161)
& subactivity_occurrence(X161,X162)
& occurrence_of(X162,tptp0) )
=> ? [X163,X164,X165] :
( leaf(X165,tptp0)
& next_subocc(X164,X165,tptp0)
& ( occurrence_of(X165,tptp1)
| occurrence_of(X165,tptp2) )
& 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] :
( leaf(X169,tptp0)
& min_precedes(X168,X169,tptp0)
& ( occurrence_of(X169,tptp1)
| occurrence_of(X169,tptp2) )
& 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] :
( leaf(X169,tptp0)
& min_precedes(X168,X169,tptp0)
& ( occurrence_of(X169,tptp1)
| occurrence_of(X169,tptp2) )
& 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]) ).
fof(nnf_51,plain,
? [X166,X167] :
( ! [X168,X169] :
( ~ leaf(X169,tptp0)
| ~ min_precedes(X168,X169,tptp0)
| ( ~ occurrence_of(X169,tptp1)
& ~ occurrence_of(X169,tptp2) )
| ~ 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] :
( ~ leaf(X169,tptp0)
| ~ min_precedes(X168,X169,tptp0)
| ( ~ occurrence_of(X169,tptp1)
& ~ occurrence_of(X169,tptp2) )
| ~ next_subocc(sK0,X168,tptp0)
| ~ occurrence_of(X168,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(X166,sK0),skolemize(X167,sK1)],[nnf_51]) ).
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_165,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_166,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_167,negated_conjecture,
~ leaf_occ(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_168,negated_conjecture,
arboreal(sK0),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_169,negated_conjecture,
subactivity_occurrence(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_170,negated_conjecture,
occurrence_of(sK1,tptp0),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
fof(sos_51,axiom,
~ atomic(tptp0),
file('theBenchmark.p',sos_51) ).
cnf(c_181,plain,
~ atomic(tptp0),
inference(clausify,[status(thm)],[sos_51]) ).
fof(nnf_50,plain,
! [X161,X162] :
( ? [X163,X164,X165] :
( leaf(X165,tptp0)
& next_subocc(X164,X165,tptp0)
& ( occurrence_of(X165,tptp1)
| occurrence_of(X165,tptp2) )
& 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(sK2(X161,X162),tptp0)
& next_subocc(sK3(X161,X162),sK2(X161,X162),tptp0)
& ( occurrence_of(sK2(X161,X162),tptp1)
| occurrence_of(sK2(X161,X162),tptp2) )
& next_subocc(sK4(X161,X162),sK3(X161,X162),tptp0)
& occurrence_of(sK3(X161,X162),tptp4)
& next_subocc(X161,sK4(X161,X162),tptp0)
& occurrence_of(sK4(X161,X162),tptp3) )
| leaf_occ(X161,X162)
| ~ arboreal(X161)
| ~ subactivity_occurrence(X161,X162)
| ~ occurrence_of(X162,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK3,sK2]),skolemize(X163,sK4(X161,X162)),skolemize(X164,sK3(X161,X162)),skolemize(X165,sK2(X161,X162))],[nnf_50]) ).
fof(sk_sos_49,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_49_sk]) ).
cnf(c_182,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_49]) ).
cnf(c_183,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_49]) ).
cnf(c_184,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_49]) ).
cnf(c_185,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_49]) ).
cnf(c_187,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_49]) ).
cnf(c_188,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_49]) ).
fof(nnf_46,plain,
! [X145,X146] :
( ? [X147] :
( leaf_occ(X145,X147)
& occurrence_of(X147,X146) )
| atomic(X146)
| ~ leaf(X145,X146) ),
inference(fof_nnf,[status(thm)],[sos_45]) ).
fof(sk_sos_45_sk,plain,
! [X145,X146] :
( ( leaf_occ(X145,sK5(X145,X146))
& occurrence_of(sK5(X145,X146),X146) )
| atomic(X146)
| ~ leaf(X145,X146) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X147,sK5(X145,X146))],[nnf_46]) ).
fof(sk_sos_45,plain,
( ! [VAR_0,VAR_1] :
( leaf_occ(VAR_0,sK5(VAR_0,VAR_1))
| atomic(VAR_1)
| ~ leaf(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( occurrence_of(sK5(VAR_0,VAR_1),VAR_1)
| atomic(VAR_1)
| ~ leaf(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_45_sk]) ).
cnf(c_192,plain,
( leaf_occ(A,sK5(A,B))
| atomic(B)
| ~ leaf(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_45]) ).
cnf(c_193,plain,
( occurrence_of(sK5(A,B),B)
| atomic(B)
| ~ leaf(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_45]) ).
cnf(c_196,plain,
( D = C
| min_precedes(C,D,B)
| ~ arboreal(C)
| ~ leaf_occ(D,A)
| ~ subactivity_occurrence(C,A)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_43]) ).
cnf(c_207,plain,
( subactivity_occurrence(A,B)
| ~ leaf_occ(A,B) ),
inference(clausify,[status(thm)],[sos_34]) ).
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_223,plain,
( min_precedes(A,B,C)
| ~ next_subocc(A,B,C) ),
inference(clausify,[status(thm)],[sos_22]) ).
cnf(c_235,plain,
( earlier(A,C)
| ~ earlier(B,C)
| ~ earlier(A,B) ),
inference(clausify,[status(thm)],[sos_05]) ).
cnf(c_236,plain,
( ~ earlier(B,A)
| ~ earlier(A,B) ),
inference(clausify,[status(thm)],[sos_04]) ).
cnf(c_243,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_245,plain,
( ~ min_precedes(B,A,C)
| legal(A) ),
inference(resolve,[status(thm)],[c_78,c_74]) ).
cnf(c_246,plain,
( ~ min_precedes(A,B,C)
| earlier(A,B) ),
inference(resolve,[status(thm)],[c_79,c_74]) ).
cnf(c_1496,negated_conjecture,
( leaf(sK2(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0)
| ~ occurrence_of(sK1,tptp0) ),
inference(resolve,[status(thm)],[c_182,c_169]) ).
cnf(c_1497,negated_conjecture,
( leaf(sK2(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0) ),
inference(resolve,[status(thm)],[c_170,c_1496]) ).
cnf(c_1498,negated_conjecture,
( leaf(sK2(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1) ),
inference(resolve,[status(thm)],[c_168,c_1497]) ).
cnf(c_284,negated_conjecture,
leaf(sK2(sK0,sK1),tptp0),
inference(resolve,[status(thm)],[c_167,c_1498]) ).
cnf(c_1499,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_183,c_169]) ).
cnf(c_1500,negated_conjecture,
( next_subocc(sK3(sK0,sK1),sK2(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0) ),
inference(resolve,[status(thm)],[c_170,c_1499]) ).
cnf(c_1501,negated_conjecture,
( next_subocc(sK3(sK0,sK1),sK2(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1) ),
inference(resolve,[status(thm)],[c_168,c_1500]) ).
cnf(c_285,negated_conjecture,
next_subocc(sK3(sK0,sK1),sK2(sK0,sK1),tptp0),
inference(resolve,[status(thm)],[c_167,c_1501]) ).
cnf(c_1502,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_184,c_169]) ).
cnf(c_1503,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_170,c_1502]) ).
cnf(c_1504,negated_conjecture,
( occurrence_of(sK2(sK0,sK1),tptp1)
| occurrence_of(sK2(sK0,sK1),tptp2)
| leaf_occ(sK0,sK1) ),
inference(resolve,[status(thm)],[c_168,c_1503]) ).
cnf(c_286,negated_conjecture,
( occurrence_of(sK2(sK0,sK1),tptp1)
| occurrence_of(sK2(sK0,sK1),tptp2) ),
inference(resolve,[status(thm)],[c_167,c_1504]) ).
cnf(c_1505,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_185,c_169]) ).
cnf(c_1506,negated_conjecture,
( next_subocc(sK4(sK0,sK1),sK3(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0) ),
inference(resolve,[status(thm)],[c_170,c_1505]) ).
cnf(c_1507,negated_conjecture,
( next_subocc(sK4(sK0,sK1),sK3(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1) ),
inference(resolve,[status(thm)],[c_168,c_1506]) ).
cnf(c_287,negated_conjecture,
next_subocc(sK4(sK0,sK1),sK3(sK0,sK1),tptp0),
inference(resolve,[status(thm)],[c_167,c_1507]) ).
cnf(c_1508,negated_conjecture,
( next_subocc(sK0,sK4(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0)
| ~ occurrence_of(sK1,tptp0) ),
inference(resolve,[status(thm)],[c_187,c_169]) ).
cnf(c_1509,negated_conjecture,
( next_subocc(sK0,sK4(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0) ),
inference(resolve,[status(thm)],[c_170,c_1508]) ).
cnf(c_1510,negated_conjecture,
( next_subocc(sK0,sK4(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1) ),
inference(resolve,[status(thm)],[c_168,c_1509]) ).
cnf(c_289,negated_conjecture,
next_subocc(sK0,sK4(sK0,sK1),tptp0),
inference(resolve,[status(thm)],[c_167,c_1510]) ).
cnf(c_1511,negated_conjecture,
( occurrence_of(sK4(sK0,sK1),tptp3)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0)
| ~ occurrence_of(sK1,tptp0) ),
inference(resolve,[status(thm)],[c_188,c_169]) ).
cnf(c_1512,negated_conjecture,
( occurrence_of(sK4(sK0,sK1),tptp3)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0) ),
inference(resolve,[status(thm)],[c_170,c_1511]) ).
cnf(c_1513,negated_conjecture,
( occurrence_of(sK4(sK0,sK1),tptp3)
| leaf_occ(sK0,sK1) ),
inference(resolve,[status(thm)],[c_168,c_1512]) ).
cnf(c_290,negated_conjecture,
occurrence_of(sK4(sK0,sK1),tptp3),
inference(resolve,[status(thm)],[c_167,c_1513]) ).
cnf(c_1514,plain,
( occurrence_of(sK5(sK2(sK0,sK1),tptp0),tptp0)
| atomic(tptp0) ),
inference(resolve,[status(thm)],[c_284,c_193]) ).
cnf(c_333,plain,
occurrence_of(sK5(sK2(sK0,sK1),tptp0),tptp0),
inference(resolve,[status(thm)],[c_181,c_1514]) ).
cnf(c_1515,plain,
( leaf_occ(sK2(sK0,sK1),sK5(sK2(sK0,sK1),tptp0))
| atomic(tptp0) ),
inference(resolve,[status(thm)],[c_284,c_192]) ).
cnf(c_334,plain,
leaf_occ(sK2(sK0,sK1),sK5(sK2(sK0,sK1),tptp0)),
inference(resolve,[status(thm)],[c_181,c_1515]) ).
cnf(c_417,plain,
min_precedes(sK0,sK4(sK0,sK1),tptp0),
inference(resolve,[status(thm)],[c_289,c_223]) ).
cnf(c_1516,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_289,c_166]) ).
cnf(c_421,negated_conjecture,
( ~ leaf(A,tptp0)
| ~ min_precedes(sK4(sK0,sK1),A,tptp0)
| ~ occurrence_of(A,tptp2) ),
inference(resolve,[status(thm)],[c_290,c_1516]) ).
cnf(c_1517,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_289,c_165]) ).
cnf(c_422,negated_conjecture,
( ~ leaf(A,tptp0)
| ~ min_precedes(sK4(sK0,sK1),A,tptp0)
| ~ occurrence_of(A,tptp1) ),
inference(resolve,[status(thm)],[c_290,c_1517]) ).
cnf(c_425,plain,
earlier(sK0,sK4(sK0,sK1)),
inference(resolve,[status(thm)],[c_417,c_246]) ).
cnf(c_445,plain,
( subactivity_occurrence(sK0,A)
| ~ subactivity_occurrence(sK4(sK0,sK1),A)
| ~ occurrence_of(A,tptp0) ),
inference(resolve,[status(thm)],[c_417,c_212]) ).
cnf(c_484,plain,
min_precedes(sK3(sK0,sK1),sK2(sK0,sK1),tptp0),
inference(resolve,[status(thm)],[c_285,c_223]) ).
cnf(c_489,plain,
min_precedes(sK4(sK0,sK1),sK3(sK0,sK1),tptp0),
inference(resolve,[status(thm)],[c_287,c_223]) ).
cnf(c_497,plain,
earlier(sK3(sK0,sK1),sK2(sK0,sK1)),
inference(resolve,[status(thm)],[c_484,c_246]) ).
cnf(c_498,plain,
legal(sK2(sK0,sK1)),
inference(resolve,[status(thm)],[c_484,c_245]) ).
cnf(c_516,plain,
( subactivity_occurrence(sK3(sK0,sK1),A)
| ~ subactivity_occurrence(sK2(sK0,sK1),A)
| ~ occurrence_of(A,tptp0) ),
inference(resolve,[status(thm)],[c_484,c_212]) ).
cnf(c_549,plain,
earlier(sK4(sK0,sK1),sK3(sK0,sK1)),
inference(resolve,[status(thm)],[c_489,c_246]) ).
cnf(c_568,plain,
( subactivity_occurrence(sK4(sK0,sK1),A)
| ~ subactivity_occurrence(sK3(sK0,sK1),A)
| ~ occurrence_of(A,tptp0) ),
inference(resolve,[status(thm)],[c_489,c_212]) ).
cnf(c_1518,plain,
( earlier(sK4(sK0,sK1),A)
| ~ earlier(sK3(sK0,sK1),A) ),
inference(resolve,[status(thm)],[c_235,c_549]) ).
cnf(c_590,plain,
earlier(sK4(sK0,sK1),sK2(sK0,sK1)),
inference(resolve,[status(thm)],[c_1518,c_497]) ).
cnf(c_620,plain,
~ earlier(sK2(sK0,sK1),sK4(sK0,sK1)),
inference(resolve,[status(thm)],[c_590,c_236]) ).
cnf(c_1034,plain,
subactivity_occurrence(sK2(sK0,sK1),sK5(sK2(sK0,sK1),tptp0)),
inference(resolve,[status(thm)],[c_334,c_207]) ).
cnf(c_1519,plain,
( subactivity_occurrence(sK3(sK0,sK1),sK5(sK2(sK0,sK1),tptp0))
| ~ occurrence_of(sK5(sK2(sK0,sK1),tptp0),tptp0) ),
inference(resolve,[status(thm)],[c_1034,c_516]) ).
cnf(c_1159,plain,
subactivity_occurrence(sK3(sK0,sK1),sK5(sK2(sK0,sK1),tptp0)),
inference(resolve,[status(thm)],[c_333,c_1519]) ).
cnf(c_1520,plain,
( subactivity_occurrence(sK4(sK0,sK1),sK5(sK2(sK0,sK1),tptp0))
| ~ occurrence_of(sK5(sK2(sK0,sK1),tptp0),tptp0) ),
inference(resolve,[status(thm)],[c_1159,c_568]) ).
cnf(c_1206,plain,
subactivity_occurrence(sK4(sK0,sK1),sK5(sK2(sK0,sK1),tptp0)),
inference(resolve,[status(thm)],[c_333,c_1520]) ).
cnf(c_1521,plain,
( subactivity_occurrence(sK0,sK5(sK2(sK0,sK1),tptp0))
| ~ occurrence_of(sK5(sK2(sK0,sK1),tptp0),tptp0) ),
inference(resolve,[status(thm)],[c_1206,c_445]) ).
cnf(c_1227,plain,
subactivity_occurrence(sK0,sK5(sK2(sK0,sK1),tptp0)),
inference(resolve,[status(thm)],[c_333,c_1521]) ).
cnf(c_1522,plain,
( B = A
| min_precedes(A,B,tptp0)
| ~ arboreal(A)
| ~ leaf_occ(B,sK5(sK2(sK0,sK1),tptp0))
| ~ subactivity_occurrence(A,sK5(sK2(sK0,sK1),tptp0)) ),
inference(resolve,[status(thm)],[c_196,c_333]) ).
cnf(c_1523,plain,
( A = sK0
| min_precedes(sK0,A,tptp0)
| ~ arboreal(sK0)
| ~ leaf_occ(A,sK5(sK2(sK0,sK1),tptp0)) ),
inference(resolve,[status(thm)],[c_1522,c_1227]) ).
cnf(c_1524,plain,
( sK2(sK0,sK1) = sK0
| min_precedes(sK0,sK2(sK0,sK1),tptp0)
| ~ arboreal(sK0) ),
inference(resolve,[status(thm)],[c_1523,c_334]) ).
cnf(c_1270,negated_conjecture,
( sK2(sK0,sK1) = sK0
| min_precedes(sK0,sK2(sK0,sK1),tptp0) ),
inference(resolve,[status(thm)],[c_1524,c_168]) ).
cnf(c_1525,plain,
( min_precedes(sK4(sK0,sK1),sK2(sK0,sK1),B)
| ~ min_precedes(A,sK2(sK0,sK1),B)
| ~ min_precedes(A,sK4(sK0,sK1),B)
| ~ legal(sK2(sK0,sK1)) ),
inference(resolve,[status(thm)],[c_243,c_590]) ).
cnf(c_1526,plain,
( min_precedes(sK4(sK0,sK1),sK2(sK0,sK1),B)
| ~ min_precedes(A,sK2(sK0,sK1),B)
| ~ min_precedes(A,sK4(sK0,sK1),B) ),
inference(resolve,[status(thm)],[c_1525,c_498]) ).
cnf(c_1527,plain,
( min_precedes(sK4(sK0,sK1),sK2(sK0,sK1),tptp0)
| ~ min_precedes(sK0,sK2(sK0,sK1),tptp0) ),
inference(resolve,[status(thm)],[c_1526,c_417]) ).
cnf(c_1306,plain,
( sK2(sK0,sK1) = sK0
| min_precedes(sK4(sK0,sK1),sK2(sK0,sK1),tptp0) ),
inference(resolve,[status(thm)],[c_1527,c_1270]) ).
cnf(c_1528,plain,
( ~ leaf(sK2(sK0,sK1),tptp0)
| ~ occurrence_of(sK2(sK0,sK1),tptp1)
| sK2(sK0,sK1) = sK0 ),
inference(resolve,[status(thm)],[c_1306,c_422]) ).
cnf(c_1347,plain,
( ~ occurrence_of(sK2(sK0,sK1),tptp1)
| sK2(sK0,sK1) = sK0 ),
inference(resolve,[status(thm)],[c_284,c_1528]) ).
cnf(c_1529,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_421,c_286]) ).
cnf(c_1530,plain,
( sK2(sK0,sK1) = sK0
| occurrence_of(sK2(sK0,sK1),tptp1)
| ~ leaf(sK2(sK0,sK1),tptp0) ),
inference(resolve,[status(thm)],[c_1529,c_1306]) ).
cnf(c_1381,plain,
( sK2(sK0,sK1) = sK0
| occurrence_of(sK2(sK0,sK1),tptp1) ),
inference(resolve,[status(thm)],[c_1530,c_284]) ).
cnf(c_1531,plain,
( sK2(sK0,sK1) = sK0
| sK2(sK0,sK1) = sK0 ),
inference(resolve,[status(thm)],[c_1381,c_1347]) ).
cnf(c_1382,plain,
sK2(sK0,sK1) = sK0,
inference(copy,[status(thm)],[c_1531]) ).
cnf(c_1532,plain,
~ earlier(sK0,sK4(sK0,sK1)),
inference(paramod,[status(thm)],[c_1382,c_620]) ).
cnf(c_1495,plain,
$false,
inference(resolve,[status(thm)],[c_425,c_1532]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO014+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.10/0.36 % Computer : n014.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 04:59:03 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 2190675 was started by sandbox2 on n014,
% 0.10/0.37 % Sat Sep 26 04:59:03 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.13/0.38
% 0.13/0.38 % From the command line: assign(max_seconds, 300).
% 4.01/0.94
% 4.01/0.94 % Assigning unary symbol f1 kb_weight 0 and highest precedence (39).
% 4.01/0.94
% 4.01/0.94 % SZS status Theorem for theBenchmark
% 4.01/0.94
% 4.01/0.94 % Proof 1 at 0.47 (+ 0.07) seconds.
% 4.01/0.94 % Length of proof is 73.
% 4.01/0.94 % Level of proof is 12.
% 4.01/0.94 % Maximum clause weight is 31.000.
% 4.01/0.94 % Given clauses 418.
% 4.01/0.94
% 4.01/0.94 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------