%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PRO012+4 : 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 : n007.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 0.23s 0.63s
% Output : CNFRefutation 0.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 16
% Syntax : Number of formulae : 114 ( 26 unt; 0 def)
% Number of atoms : 371 ( 29 equ)
% Maximal formula atoms : 17 ( 3 avg)
% Number of connectives : 405 ( 148 ~; 170 |; 70 &)
% ( 2 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 6 con; 0-3 aty)
% Number of variables : 199 ( 12 sgn 97 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(sos,axiom,
! [X0,X1] :
( ( ~ atomic(X0)
& occurrence_of(X1,X0) )
=> ? [X2] :
( subactivity_occurrence(X2,X1)
& root(X2,X0) ) ),
file('theBenchmark.p',sos) ).
fof(sos_04,axiom,
! [X14,X15,X16,X17] :
( ( subactivity_occurrence(X17,X15)
& subactivity_occurrence(X16,X15)
& arboreal(X17)
& arboreal(X16)
& occurrence_of(X15,X14) )
=> ( X16 = X17
| min_precedes(X17,X16,X14)
| min_precedes(X16,X17,X14) ) ),
file('theBenchmark.p',sos_04) ).
fof(sos_06,axiom,
! [X21,X22,X23] :
( min_precedes(X22,X23,X21)
=> ? [X24] :
( subactivity_occurrence(X23,X24)
& subactivity_occurrence(X22,X24)
& occurrence_of(X24,X21) ) ),
file('theBenchmark.p',sos_06) ).
fof(sos_13,axiom,
! [X43] :
( legal(X43)
=> arboreal(X43) ),
file('theBenchmark.p',sos_13) ).
fof(sos_17,axiom,
! [X53,X54] :
( root(X53,X54)
=> legal(X53) ),
file('theBenchmark.p',sos_17) ).
fof(sos_19,axiom,
! [X58,X59] :
( root_occ(X58,X59)
<=> ? [X60] :
( root(X58,X60)
& subactivity_occurrence(X58,X59)
& occurrence_of(X59,X60) ) ),
file('theBenchmark.p',sos_19) ).
fof(sos_20,axiom,
! [X61,X62] :
( earlier(X61,X62)
=> ~ earlier(X62,X61) ),
file('theBenchmark.p',sos_20) ).
fof(sos_21,axiom,
! [X63,X64] :
( precedes(X63,X64)
<=> ( legal(X64)
& earlier(X63,X64) ) ),
file('theBenchmark.p',sos_21) ).
fof(sos_22,axiom,
! [X65,X66,X67] :
( min_precedes(X65,X66,X67)
=> ~ root(X66,X67) ),
file('theBenchmark.p',sos_22) ).
fof(sos_24,axiom,
! [X72,X73,X74] :
( min_precedes(X72,X73,X74)
=> precedes(X72,X73) ),
file('theBenchmark.p',sos_24) ).
fof(sos_27,axiom,
! [X82,X83,X84,X85] :
( ( subactivity_occurrence(X83,X85)
& occurrence_of(X85,X84)
& min_precedes(X82,X83,X84) )
=> subactivity_occurrence(X82,X85) ),
file('theBenchmark.p',sos_27) ).
fof(sos_29,axiom,
! [X90,X91,X92,X93] :
( ( root_occ(X91,X92)
& root_occ(X90,X92)
& occurrence_of(X92,X93) )
=> X90 = X91 ),
file('theBenchmark.p',sos_29) ).
fof(sos_30,axiom,
! [X94,X95,X96] :
( ( earlier(X95,X96)
& earlier(X94,X95) )
=> earlier(X94,X96) ),
file('theBenchmark.p',sos_30) ).
fof(sos_32,axiom,
! [X101] :
( occurrence_of(X101,tptp0)
=> ? [X102,X103,X104] :
( ! [X105] :
( min_precedes(X102,X105,tptp0)
=> ( X105 = X104
| X105 = X103 ) )
& min_precedes(X103,X104,tptp0)
& ( occurrence_of(X104,tptp1)
| occurrence_of(X104,tptp2) )
& min_precedes(X102,X103,tptp0)
& occurrence_of(X103,tptp4)
& root_occ(X102,X101)
& occurrence_of(X102,tptp3) ) ),
file('theBenchmark.p',sos_32) ).
fof(goals,conjecture,
! [X106] :
( occurrence_of(X106,tptp0)
=> ? [X107,X108] :
( min_precedes(X107,X108,tptp0)
& ( occurrence_of(X108,tptp1)
| occurrence_of(X108,tptp2) )
& root_occ(X107,X106)
& occurrence_of(X107,tptp3) ) ),
file('theBenchmark.p',goals) ).
fof(goals_neg,negated_conjecture,
~ ! [X106] :
( occurrence_of(X106,tptp0)
=> ? [X107,X108] :
( min_precedes(X107,X108,tptp0)
& ( occurrence_of(X108,tptp1)
| occurrence_of(X108,tptp2) )
& root_occ(X107,X106)
& occurrence_of(X107,tptp3) ) ),
inference(assume_negation,[status(cth)],[goals]) ).
fof(nnf_1,plain,
! [X0,X1] :
( ? [X2] :
( subactivity_occurrence(X2,X1)
& root(X2,X0) )
| atomic(X0)
| ~ occurrence_of(X1,X0) ),
inference(fof_nnf,[status(thm)],[sos]) ).
fof(sk_sos_sk,plain,
! [X0,X1] :
( ( subactivity_occurrence(sK0(X0,X1),X1)
& root(sK0(X0,X1),X0) )
| atomic(X0)
| ~ occurrence_of(X1,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X2,sK0(X0,X1))],[nnf_1]) ).
fof(sk_sos,plain,
( ! [VAR_0,VAR_1] :
( subactivity_occurrence(sK0(VAR_1,VAR_0),VAR_0)
| atomic(VAR_1)
| ~ occurrence_of(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( root(sK0(VAR_1,VAR_0),VAR_1)
| atomic(VAR_1)
| ~ occurrence_of(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_sk]) ).
cnf(c_36,plain,
( root(sK0(B,A),B)
| atomic(B)
| ~ occurrence_of(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos]) ).
cnf(c_40,plain,
( legal(A)
| ~ root(A,B) ),
inference(clausify,[status(thm)],[sos_17]) ).
fof(nnf_20,plain,
! [X58,X59] :
( ( ! [X60] :
( ~ root(X58,X60)
| ~ subactivity_occurrence(X58,X59)
| ~ occurrence_of(X59,X60) )
| root_occ(X58,X59) )
& ( ? [X109] :
( root(X58,X109)
& subactivity_occurrence(X58,X59)
& occurrence_of(X59,X109) )
| ~ root_occ(X58,X59) ) ),
inference(fof_nnf,[status(thm)],[sos_19]) ).
fof(sk_sos_19_sk,plain,
! [X58,X59] :
( ( ! [X60] :
( ~ root(X58,X60)
| ~ subactivity_occurrence(X58,X59)
| ~ occurrence_of(X59,X60) )
| root_occ(X58,X59) )
& ( ( root(X58,sK1(X58,X59))
& subactivity_occurrence(X58,X59)
& occurrence_of(X59,sK1(X58,X59)) )
| ~ root_occ(X58,X59) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X109,sK1(X58,X59))],[nnf_20]) ).
fof(sk_sos_19,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,sK1(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,sK1(VAR_0,VAR_1))
| ~ root_occ(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_19_sk]) ).
cnf(c_41,plain,
( root(A,sK1(A,B))
| ~ root_occ(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_19]) ).
cnf(c_42,plain,
( ~ root(A,C)
| ~ subactivity_occurrence(A,B)
| ~ occurrence_of(B,C)
| root_occ(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_19]) ).
cnf(c_43,plain,
( ~ root(B,C)
| ~ min_precedes(A,B,C) ),
inference(clausify,[status(thm)],[sos_22]) ).
cnf(c_71,plain,
( legal(A)
| ~ root_occ(A,B) ),
inference(resolve,[status(thm)],[c_41,c_40]) ).
cnf(c_77,plain,
( legal(B)
| ~ precedes(A,B) ),
inference(clausify,[status(thm)],[sos_21]) ).
cnf(c_78,plain,
( arboreal(A)
| ~ legal(A) ),
inference(clausify,[status(thm)],[sos_13]) ).
cnf(c_133,plain,
( atomic(B)
| ~ occurrence_of(C,B)
| ~ min_precedes(A,sK0(B,C),B) ),
inference(resolve,[status(thm)],[c_43,c_36]) ).
cnf(c_135,plain,
( atomic(A)
| ~ occurrence_of(B,A)
| ~ subactivity_occurrence(sK0(A,B),C)
| ~ occurrence_of(C,A)
| root_occ(sK0(A,B),C) ),
inference(resolve,[status(thm)],[c_42,c_36]) ).
fof(nnf_34,plain,
? [X106] :
( ! [X107,X108] :
( ~ min_precedes(X107,X108,tptp0)
| ( ~ occurrence_of(X108,tptp1)
& ~ occurrence_of(X108,tptp2) )
| ~ root_occ(X107,X106)
| ~ occurrence_of(X107,tptp3) )
& occurrence_of(X106,tptp0) ),
inference(fof_nnf,[status(thm)],[goals_neg]) ).
fof(sk_goals_neg_sk,plain,
( ! [X107,X108] :
( ~ min_precedes(X107,X108,tptp0)
| ( ~ occurrence_of(X108,tptp1)
& ~ occurrence_of(X108,tptp2) )
| ~ root_occ(X107,sK2)
| ~ occurrence_of(X107,tptp3) )
& occurrence_of(sK2,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X106,sK2)],[nnf_34]) ).
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,sK2)
| ~ 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,sK2)
| ~ occurrence_of(VAR_0,tptp3) )
& occurrence_of(sK2,tptp0) ),
inference(cnf_transformation,[status(thm)],[sk_goals_neg_sk]) ).
cnf(c_139,negated_conjecture,
( ~ min_precedes(A,B,tptp0)
| ~ occurrence_of(B,tptp1)
| ~ root_occ(A,sK2)
| ~ occurrence_of(A,tptp3) ),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_140,negated_conjecture,
( ~ min_precedes(A,B,tptp0)
| ~ occurrence_of(B,tptp2)
| ~ root_occ(A,sK2)
| ~ occurrence_of(A,tptp3) ),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_141,negated_conjecture,
occurrence_of(sK2,tptp0),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
fof(sos_34,axiom,
~ atomic(tptp0),
file('theBenchmark.p',sos_34) ).
cnf(c_152,plain,
~ atomic(tptp0),
inference(clausify,[status(thm)],[sos_34]) ).
fof(nnf_33,plain,
! [X101] :
( ? [X102,X103,X104] :
( ! [X105] :
( X105 = X104
| X105 = X103
| ~ min_precedes(X102,X105,tptp0) )
& min_precedes(X103,X104,tptp0)
& ( occurrence_of(X104,tptp1)
| occurrence_of(X104,tptp2) )
& min_precedes(X102,X103,tptp0)
& occurrence_of(X103,tptp4)
& root_occ(X102,X101)
& occurrence_of(X102,tptp3) )
| ~ occurrence_of(X101,tptp0) ),
inference(fof_nnf,[status(thm)],[sos_32]) ).
fof(sk_sos_32_sk,plain,
! [X101] :
( ( ! [X105] :
( X105 = sK4(X101)
| X105 = sK3(X101)
| ~ min_precedes(sK5(X101),X105,tptp0) )
& min_precedes(sK3(X101),sK4(X101),tptp0)
& ( occurrence_of(sK4(X101),tptp1)
| occurrence_of(sK4(X101),tptp2) )
& min_precedes(sK5(X101),sK3(X101),tptp0)
& occurrence_of(sK3(X101),tptp4)
& root_occ(sK5(X101),X101)
& occurrence_of(sK5(X101),tptp3) )
| ~ occurrence_of(X101,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK3,sK4]),skolemize(X102,sK5(X101)),skolemize(X103,sK3(X101)),skolemize(X104,sK4(X101))],[nnf_33]) ).
fof(sk_sos_32,plain,
( ! [VAR_0,VAR_1] :
( VAR_1 = sK4(VAR_0)
| VAR_1 = sK3(VAR_0)
| ~ min_precedes(sK5(VAR_0),VAR_1,tptp0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( min_precedes(sK3(VAR_0),sK4(VAR_0),tptp0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( occurrence_of(sK4(VAR_0),tptp1)
| occurrence_of(sK4(VAR_0),tptp2)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( min_precedes(sK5(VAR_0),sK3(VAR_0),tptp0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( occurrence_of(sK3(VAR_0),tptp4)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( root_occ(sK5(VAR_0),VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( occurrence_of(sK5(VAR_0),tptp3)
| ~ occurrence_of(VAR_0,tptp0) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_32_sk]) ).
cnf(c_155,plain,
( min_precedes(sK3(A),sK4(A),tptp0)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
cnf(c_156,plain,
( occurrence_of(sK4(A),tptp1)
| occurrence_of(sK4(A),tptp2)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
cnf(c_157,plain,
( min_precedes(sK5(A),sK3(A),tptp0)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
cnf(c_159,plain,
( root_occ(sK5(A),A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
cnf(c_160,plain,
( occurrence_of(sK5(A),tptp3)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
cnf(c_162,plain,
( earlier(A,C)
| ~ earlier(B,C)
| ~ earlier(A,B) ),
inference(clausify,[status(thm)],[sos_30]) ).
cnf(c_163,plain,
( D = C
| ~ root_occ(D,A)
| ~ root_occ(C,A)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_29]) ).
cnf(c_165,plain,
( subactivity_occurrence(A,D)
| ~ subactivity_occurrence(B,D)
| ~ occurrence_of(D,C)
| ~ min_precedes(A,B,C) ),
inference(clausify,[status(thm)],[sos_27]) ).
cnf(c_166,plain,
( precedes(A,B)
| ~ min_precedes(A,B,C) ),
inference(clausify,[status(thm)],[sos_24]) ).
cnf(c_168,plain,
( earlier(A,B)
| ~ precedes(A,B) ),
inference(clausify,[status(thm)],[sos_21]) ).
cnf(c_169,plain,
( ~ earlier(B,A)
| ~ earlier(A,B) ),
inference(clausify,[status(thm)],[sos_20]) ).
fof(nnf_7,plain,
! [X21,X22,X23] :
( ? [X24] :
( subactivity_occurrence(X23,X24)
& subactivity_occurrence(X22,X24)
& occurrence_of(X24,X21) )
| ~ min_precedes(X22,X23,X21) ),
inference(fof_nnf,[status(thm)],[sos_06]) ).
fof(sk_sos_06_sk,plain,
! [X21,X22,X23] :
( ( subactivity_occurrence(X23,sK6(X21,X22,X23))
& subactivity_occurrence(X22,sK6(X21,X22,X23))
& occurrence_of(sK6(X21,X22,X23),X21) )
| ~ min_precedes(X22,X23,X21) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X24,sK6(X21,X22,X23))],[nnf_7]) ).
fof(sk_sos_06,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( subactivity_occurrence(VAR_1,sK6(VAR_2,VAR_0,VAR_1))
| ~ min_precedes(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( subactivity_occurrence(VAR_0,sK6(VAR_2,VAR_0,VAR_1))
| ~ min_precedes(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( occurrence_of(sK6(VAR_2,VAR_0,VAR_1),VAR_2)
| ~ min_precedes(VAR_0,VAR_1,VAR_2) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_06_sk]) ).
cnf(c_181,plain,
( subactivity_occurrence(B,sK6(C,A,B))
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_06]) ).
cnf(c_182,plain,
( subactivity_occurrence(A,sK6(C,A,B))
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_06]) ).
cnf(c_183,plain,
( occurrence_of(sK6(C,A,B),C)
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_06]) ).
cnf(c_184,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_04]) ).
cnf(c_187,plain,
( subactivity_occurrence(sK0(B,A),A)
| atomic(B)
| ~ occurrence_of(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos]) ).
cnf(c_197,plain,
( ~ precedes(B,A)
| arboreal(A) ),
inference(resolve,[status(thm)],[c_78,c_77]) ).
cnf(c_199,plain,
( ~ root_occ(A,B)
| arboreal(A) ),
inference(resolve,[status(thm)],[c_78,c_71]) ).
cnf(c_212,plain,
( atomic(A)
| ~ subactivity_occurrence(sK0(A,B),B)
| ~ occurrence_of(B,A)
| root_occ(sK0(A,B),B) ),
inference(factor,[status(thm)],[c_135]) ).
cnf(c_214,plain,
~ earlier(A,A),
inference(factor,[status(thm)],[c_169]) ).
cnf(c_219,plain,
min_precedes(sK3(sK2),sK4(sK2),tptp0),
inference(resolve,[status(thm)],[c_155,c_141]) ).
cnf(c_220,plain,
( occurrence_of(sK4(sK2),tptp1)
| occurrence_of(sK4(sK2),tptp2) ),
inference(resolve,[status(thm)],[c_156,c_141]) ).
cnf(c_221,plain,
min_precedes(sK5(sK2),sK3(sK2),tptp0),
inference(resolve,[status(thm)],[c_157,c_141]) ).
cnf(c_223,plain,
root_occ(sK5(sK2),sK2),
inference(resolve,[status(thm)],[c_159,c_141]) ).
cnf(c_224,plain,
occurrence_of(sK5(sK2),tptp3),
inference(resolve,[status(thm)],[c_160,c_141]) ).
cnf(c_632,negated_conjecture,
( subactivity_occurrence(sK0(tptp0,sK2),sK2)
| atomic(tptp0) ),
inference(resolve,[status(thm)],[c_187,c_141]) ).
cnf(c_227,negated_conjecture,
subactivity_occurrence(sK0(tptp0,sK2),sK2),
inference(resolve,[status(thm)],[c_152,c_632]) ).
cnf(c_237,plain,
arboreal(sK5(sK2)),
inference(resolve,[status(thm)],[c_223,c_199]) ).
cnf(c_633,plain,
( atomic(tptp0)
| ~ occurrence_of(sK2,tptp0)
| root_occ(sK0(tptp0,sK2),sK2) ),
inference(resolve,[status(thm)],[c_227,c_212]) ).
cnf(c_634,negated_conjecture,
( atomic(tptp0)
| root_occ(sK0(tptp0,sK2),sK2) ),
inference(resolve,[status(thm)],[c_141,c_633]) ).
cnf(c_289,negated_conjecture,
root_occ(sK0(tptp0,sK2),sK2),
inference(resolve,[status(thm)],[c_152,c_634]) ).
cnf(c_635,negated_conjecture,
( B = A
| ~ root_occ(B,sK2)
| ~ root_occ(A,sK2) ),
inference(resolve,[status(thm)],[c_163,c_141]) ).
cnf(c_636,negated_conjecture,
( A = sK5(sK2)
| ~ root_occ(A,sK2) ),
inference(resolve,[status(thm)],[c_635,c_223]) ).
cnf(c_305,negated_conjecture,
sK0(tptp0,sK2) = sK5(sK2),
inference(resolve,[status(thm)],[c_636,c_289]) ).
cnf(c_360,plain,
occurrence_of(sK6(tptp0,sK3(sK2),sK4(sK2)),tptp0),
inference(resolve,[status(thm)],[c_219,c_183]) ).
cnf(c_361,plain,
subactivity_occurrence(sK3(sK2),sK6(tptp0,sK3(sK2),sK4(sK2))),
inference(resolve,[status(thm)],[c_219,c_182]) ).
cnf(c_362,plain,
subactivity_occurrence(sK4(sK2),sK6(tptp0,sK3(sK2),sK4(sK2))),
inference(resolve,[status(thm)],[c_219,c_181]) ).
cnf(c_366,plain,
precedes(sK3(sK2),sK4(sK2)),
inference(resolve,[status(thm)],[c_219,c_166]) ).
cnf(c_390,plain,
arboreal(sK4(sK2)),
inference(resolve,[status(thm)],[c_366,c_197]) ).
cnf(c_391,plain,
earlier(sK3(sK2),sK4(sK2)),
inference(resolve,[status(thm)],[c_366,c_168]) ).
cnf(c_410,plain,
precedes(sK5(sK2),sK3(sK2)),
inference(resolve,[status(thm)],[c_221,c_166]) ).
cnf(c_411,plain,
( subactivity_occurrence(sK5(sK2),A)
| ~ subactivity_occurrence(sK3(sK2),A)
| ~ occurrence_of(A,tptp0) ),
inference(resolve,[status(thm)],[c_221,c_165]) ).
cnf(c_435,plain,
earlier(sK5(sK2),sK3(sK2)),
inference(resolve,[status(thm)],[c_410,c_168]) ).
cnf(c_637,plain,
( earlier(sK5(sK2),A)
| ~ earlier(sK3(sK2),A) ),
inference(resolve,[status(thm)],[c_162,c_435]) ).
cnf(c_439,plain,
earlier(sK5(sK2),sK4(sK2)),
inference(resolve,[status(thm)],[c_637,c_391]) ).
cnf(c_638,plain,
( atomic(tptp0)
| ~ occurrence_of(sK2,tptp0)
| ~ min_precedes(A,sK5(sK2),tptp0) ),
inference(paramod,[status(thm)],[c_305,c_133]) ).
cnf(c_639,negated_conjecture,
( atomic(tptp0)
| ~ min_precedes(A,sK5(sK2),tptp0) ),
inference(resolve,[status(thm)],[c_141,c_638]) ).
cnf(c_449,negated_conjecture,
~ min_precedes(A,sK5(sK2),tptp0),
inference(resolve,[status(thm)],[c_152,c_639]) ).
cnf(c_640,plain,
( subactivity_occurrence(sK5(sK2),sK6(tptp0,sK3(sK2),sK4(sK2)))
| ~ occurrence_of(sK6(tptp0,sK3(sK2),sK4(sK2)),tptp0) ),
inference(resolve,[status(thm)],[c_361,c_411]) ).
cnf(c_533,plain,
subactivity_occurrence(sK5(sK2),sK6(tptp0,sK3(sK2),sK4(sK2))),
inference(resolve,[status(thm)],[c_360,c_640]) ).
cnf(c_641,plain,
( B = A
| min_precedes(B,A,tptp0)
| min_precedes(A,B,tptp0)
| ~ subactivity_occurrence(B,sK6(tptp0,sK3(sK2),sK4(sK2)))
| ~ subactivity_occurrence(A,sK6(tptp0,sK3(sK2),sK4(sK2)))
| ~ arboreal(B)
| ~ arboreal(A) ),
inference(resolve,[status(thm)],[c_184,c_360]) ).
cnf(c_642,plain,
( A = sK4(sK2)
| min_precedes(A,sK4(sK2),tptp0)
| min_precedes(sK4(sK2),A,tptp0)
| ~ subactivity_occurrence(A,sK6(tptp0,sK3(sK2),sK4(sK2)))
| ~ subactivity_occurrence(sK4(sK2),sK6(tptp0,sK3(sK2),sK4(sK2)))
| ~ arboreal(A) ),
inference(resolve,[status(thm)],[c_641,c_390]) ).
cnf(c_643,plain,
( sK5(sK2) = sK4(sK2)
| min_precedes(sK5(sK2),sK4(sK2),tptp0)
| min_precedes(sK4(sK2),sK5(sK2),tptp0)
| ~ subactivity_occurrence(sK5(sK2),sK6(tptp0,sK3(sK2),sK4(sK2)))
| ~ subactivity_occurrence(sK4(sK2),sK6(tptp0,sK3(sK2),sK4(sK2))) ),
inference(resolve,[status(thm)],[c_642,c_237]) ).
cnf(c_644,plain,
( sK5(sK2) = sK4(sK2)
| min_precedes(sK5(sK2),sK4(sK2),tptp0)
| min_precedes(sK4(sK2),sK5(sK2),tptp0)
| ~ subactivity_occurrence(sK5(sK2),sK6(tptp0,sK3(sK2),sK4(sK2))) ),
inference(resolve,[status(thm)],[c_643,c_362]) ).
cnf(c_645,plain,
( sK5(sK2) = sK4(sK2)
| min_precedes(sK5(sK2),sK4(sK2),tptp0)
| min_precedes(sK4(sK2),sK5(sK2),tptp0) ),
inference(resolve,[status(thm)],[c_644,c_533]) ).
cnf(c_646,plain,
( sK4(sK2) = sK5(sK2)
| min_precedes(sK5(sK2),sK4(sK2),tptp0)
| min_precedes(sK4(sK2),sK5(sK2),tptp0) ),
inference(copy,[status(thm)],[c_645]) ).
cnf(c_571,plain,
( sK4(sK2) = sK5(sK2)
| min_precedes(sK5(sK2),sK4(sK2),tptp0) ),
inference(resolve,[status(thm)],[c_449,c_646]) ).
cnf(c_647,negated_conjecture,
( ~ occurrence_of(sK4(sK2),tptp1)
| ~ root_occ(sK5(sK2),sK2)
| ~ occurrence_of(sK5(sK2),tptp3)
| sK4(sK2) = sK5(sK2) ),
inference(resolve,[status(thm)],[c_571,c_139]) ).
cnf(c_648,negated_conjecture,
( ~ occurrence_of(sK4(sK2),tptp1)
| ~ root_occ(sK5(sK2),sK2)
| sK4(sK2) = sK5(sK2) ),
inference(resolve,[status(thm)],[c_224,c_647]) ).
cnf(c_586,negated_conjecture,
( ~ occurrence_of(sK4(sK2),tptp1)
| sK4(sK2) = sK5(sK2) ),
inference(resolve,[status(thm)],[c_223,c_648]) ).
cnf(c_649,negated_conjecture,
( ~ min_precedes(sK5(sK2),A,tptp0)
| ~ occurrence_of(A,tptp2)
| ~ root_occ(sK5(sK2),sK2) ),
inference(resolve,[status(thm)],[c_140,c_224]) ).
cnf(c_650,negated_conjecture,
( ~ min_precedes(sK5(sK2),A,tptp0)
| ~ occurrence_of(A,tptp2) ),
inference(resolve,[status(thm)],[c_649,c_223]) ).
cnf(c_651,negated_conjecture,
( occurrence_of(sK4(sK2),tptp1)
| ~ min_precedes(sK5(sK2),sK4(sK2),tptp0) ),
inference(resolve,[status(thm)],[c_650,c_220]) ).
cnf(c_596,negated_conjecture,
( sK4(sK2) = sK5(sK2)
| occurrence_of(sK4(sK2),tptp1) ),
inference(resolve,[status(thm)],[c_651,c_571]) ).
cnf(c_652,plain,
( sK4(sK2) = sK5(sK2)
| sK4(sK2) = sK5(sK2) ),
inference(resolve,[status(thm)],[c_596,c_586]) ).
cnf(c_599,plain,
sK4(sK2) = sK5(sK2),
inference(copy,[status(thm)],[c_652]) ).
cnf(c_653,plain,
earlier(sK5(sK2),sK5(sK2)),
inference(paramod,[status(thm)],[c_599,c_439]) ).
cnf(c_631,plain,
$false,
inference(resolve,[status(thm)],[c_214,c_653]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : PRO012+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n007.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Sat Sep 26 04:56:54 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.46 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.19/0.46 % Process 2826426 was started by sandbox2 on n007,
% 0.19/0.46 % Sat Sep 26 04:56:54 2026
% 0.19/0.46 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.19/0.47
% 0.19/0.47 % From the command line: assign(max_seconds, 300).
% 0.23/0.63
% 0.23/0.63 % SZS status Theorem for theBenchmark
% 0.23/0.63
% 0.23/0.63 % Proof 1 at 0.11 (+ 0.04) seconds.
% 0.23/0.63 % Length of proof is 75.
% 0.23/0.63 % Level of proof is 10.
% 0.23/0.63 % Maximum clause weight is 29.000.
% 0.23/0.63 % Given clauses 215.
% 0.23/0.63
% 0.23/0.63 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------