%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PRO006+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 : n002.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:55 AM UTC 2026
% Result : Theorem 100.95s 15.31s
% Output : CNFRefutation 100.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 18
% Syntax : Number of formulae : 130 ( 45 unt; 0 def)
% Number of atoms : 365 ( 31 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 381 ( 146 ~; 157 |; 63 &)
% ( 3 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-3 aty)
% Number of variables : 204 ( 9 sgn 93 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(sos_02,axiom,
! [X4,X5,X6] :
( ( occurrence_of(X4,X6)
& occurrence_of(X4,X5) )
=> X5 = X6 ),
file('theBenchmark.p',sos_02) ).
fof(sos_08,axiom,
! [X18] :
( legal(X18)
=> arboreal(X18) ),
file('theBenchmark.p',sos_08) ).
fof(sos_14,axiom,
! [X35,X36,X37] :
( min_precedes(X35,X36,X37)
=> ~ root(X36,X37) ),
file('theBenchmark.p',sos_14) ).
fof(sos_16,axiom,
! [X41,X42] :
( root(X41,X42)
=> legal(X41) ),
file('theBenchmark.p',sos_16) ).
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_27,axiom,
! [X76,X77] :
( ( ~ atomic(X76)
& occurrence_of(X77,X76) )
=> ? [X78] :
( subactivity_occurrence(X78,X77)
& root(X78,X76) ) ),
file('theBenchmark.p',sos_27) ).
fof(sos_33,axiom,
! [X99,X100] :
( root_occ(X99,X100)
<=> ? [X101] :
( root(X99,X101)
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,X101) ) ),
file('theBenchmark.p',sos_33) ).
fof(sos_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_35,axiom,
! [X105,X106,X107,X108] :
( ( root_occ(X106,X107)
& root_occ(X105,X107)
& occurrence_of(X107,X108) )
=> X105 = X106 ),
file('theBenchmark.p',sos_35) ).
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_39,axiom,
! [X121,X122,X123,X124,X125] :
( ( subactivity_occurrence(X122,X125)
& subactivity_occurrence(X123,X125)
& occurrence_of(X125,X124)
& next_subocc(X121,X123,X124)
& next_subocc(X121,X122,X124) )
=> X122 = X123 ),
file('theBenchmark.p',sos_39) ).
fof(sos_42,axiom,
! [X134,X135,X136,X137] :
( ( ~ min_precedes(X137,X136,X134)
& arboreal(X136)
& root_occ(X137,X135)
& subactivity_occurrence(X136,X135)
& occurrence_of(X135,X134) )
=> X137 = X136 ),
file('theBenchmark.p',sos_42) ).
fof(sos_49,axiom,
! [X161] :
( occurrence_of(X161,tptp0)
=> ? [X162,X163] :
( next_subocc(X162,X163,tptp0)
& leaf_occ(X163,X161)
& occurrence_of(X163,tptp3)
& root_occ(X162,X161)
& occurrence_of(X162,tptp4) ) ),
file('theBenchmark.p',sos_49) ).
fof(sos_62,axiom,
! [X164,X165] :
( ( ~ leaf_occ(X164,X165)
& arboreal(X164)
& subactivity_occurrence(X164,X165)
& occurrence_of(X165,tptp0) )
=> ? [X166] :
( next_subocc(X164,X166,tptp0)
& occurrence_of(X166,tptp1) ) ),
file('theBenchmark.p',sos_62) ).
fof(goals,conjecture,
~ ? [X167] : occurrence_of(X167,tptp0),
file('theBenchmark.p',goals) ).
fof(goals_neg,negated_conjecture,
~ ~ ? [X167] : occurrence_of(X167,tptp0),
inference(assume_negation,[status(cth)],[goals]) ).
cnf(c_83,plain,
( ~ root(B,C)
| ~ min_precedes(A,B,C) ),
inference(clausify,[status(thm)],[sos_14]) ).
cnf(c_84,plain,
( legal(A)
| ~ root(A,B) ),
inference(clausify,[status(thm)],[sos_16]) ).
fof(nnf_28,plain,
! [X76,X77] :
( ? [X78] :
( subactivity_occurrence(X78,X77)
& root(X78,X76) )
| atomic(X76)
| ~ occurrence_of(X77,X76) ),
inference(fof_nnf,[status(thm)],[sos_27]) ).
fof(sk_sos_27_sk,plain,
! [X76,X77] :
( ( subactivity_occurrence(sK0(X76,X77),X77)
& root(sK0(X76,X77),X76) )
| atomic(X76)
| ~ occurrence_of(X77,X76) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X78,sK0(X76,X77))],[nnf_28]) ).
fof(sk_sos_27,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_27_sk]) ).
cnf(c_90,plain,
( root(sK0(B,A),B)
| atomic(B)
| ~ occurrence_of(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_27]) ).
fof(nnf_34,plain,
! [X99,X100] :
( ( ! [X101] :
( ~ root(X99,X101)
| ~ subactivity_occurrence(X99,X100)
| ~ occurrence_of(X100,X101) )
| root_occ(X99,X100) )
& ( ? [X168] :
( root(X99,X168)
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,X168) )
| ~ root_occ(X99,X100) ) ),
inference(fof_nnf,[status(thm)],[sos_33]) ).
fof(sk_sos_33_sk,plain,
! [X99,X100] :
( ( ! [X101] :
( ~ root(X99,X101)
| ~ subactivity_occurrence(X99,X100)
| ~ occurrence_of(X100,X101) )
| root_occ(X99,X100) )
& ( ( root(X99,sK1(X99,X100))
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,sK1(X99,X100)) )
| ~ root_occ(X99,X100) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X168,sK1(X99,X100))],[nnf_34]) ).
fof(sk_sos_33,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( ~ root(VAR_0,VAR_2)
| ~ subactivity_occurrence(VAR_0,VAR_1)
| ~ occurrence_of(VAR_1,VAR_2)
| root_occ(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( root(VAR_0,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_33_sk]) ).
cnf(c_91,plain,
( root(A,sK1(A,B))
| ~ root_occ(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_33]) ).
cnf(c_92,plain,
( ~ root(A,C)
| ~ subactivity_occurrence(A,B)
| ~ occurrence_of(B,C)
| root_occ(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_33]) ).
cnf(c_190,plain,
( C = B
| ~ occurrence_of(A,C)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_02]) ).
cnf(c_196,plain,
( arboreal(A)
| ~ legal(A) ),
inference(clausify,[status(thm)],[sos_08]) ).
cnf(c_202,plain,
( min_precedes(A,B,C)
| ~ next_subocc(A,B,C) ),
inference(clausify,[status(thm)],[sos_22]) ).
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,sK2(X69,X70,X71))
& subactivity_occurrence(X70,sK2(X69,X70,X71))
& occurrence_of(sK2(X69,X70,X71),X69) )
| ~ min_precedes(X70,X71,X69) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X72,sK2(X69,X70,X71))],[nnf_26]) ).
fof(sk_sos_25,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( subactivity_occurrence(VAR_1,sK2(VAR_2,VAR_0,VAR_1))
| ~ min_precedes(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( subactivity_occurrence(VAR_0,sK2(VAR_2,VAR_0,VAR_1))
| ~ min_precedes(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( occurrence_of(sK2(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_208,plain,
( occurrence_of(sK2(C,A,B),C)
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_25]) ).
cnf(c_209,plain,
( subactivity_occurrence(A,sK2(C,A,B))
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_25]) ).
cnf(c_210,plain,
( subactivity_occurrence(B,sK2(C,A,B))
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_25]) ).
cnf(c_211,plain,
( subactivity_occurrence(sK0(B,A),A)
| atomic(B)
| ~ occurrence_of(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_27]) ).
cnf(c_216,plain,
( subactivity_occurrence(A,B)
| ~ root_occ(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_33]) ).
cnf(c_218,plain,
( subactivity_occurrence(A,B)
| ~ leaf_occ(A,B) ),
inference(clausify,[status(thm)],[sos_34]) ).
cnf(c_219,plain,
( D = C
| ~ root_occ(D,A)
| ~ root_occ(C,A)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_35]) ).
cnf(c_221,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 = B
| ~ subactivity_occurrence(B,E)
| ~ subactivity_occurrence(D,E)
| ~ occurrence_of(E,C)
| ~ next_subocc(A,D,C)
| ~ next_subocc(A,B,C) ),
inference(clausify,[status(thm)],[sos_39]) ).
cnf(c_226,plain,
( D = C
| min_precedes(D,C,B)
| ~ arboreal(C)
| ~ root_occ(D,A)
| ~ subactivity_occurrence(C,A)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_42]) ).
fof(nnf_50,plain,
! [X161] :
( ? [X162,X163] :
( next_subocc(X162,X163,tptp0)
& leaf_occ(X163,X161)
& occurrence_of(X163,tptp3)
& root_occ(X162,X161)
& occurrence_of(X162,tptp4) )
| ~ occurrence_of(X161,tptp0) ),
inference(fof_nnf,[status(thm)],[sos_49]) ).
fof(sk_sos_49_sk,plain,
! [X161] :
( ( next_subocc(sK3(X161),sK4(X161),tptp0)
& leaf_occ(sK4(X161),X161)
& occurrence_of(sK4(X161),tptp3)
& root_occ(sK3(X161),X161)
& occurrence_of(sK3(X161),tptp4) )
| ~ occurrence_of(X161,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4]),skolemize(X162,sK3(X161)),skolemize(X163,sK4(X161))],[nnf_50]) ).
fof(sk_sos_49,plain,
( ! [VAR_0] :
( next_subocc(sK3(VAR_0),sK4(VAR_0),tptp0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( leaf_occ(sK4(VAR_0),VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( occurrence_of(sK4(VAR_0),tptp3)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( root_occ(sK3(VAR_0),VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( occurrence_of(sK3(VAR_0),tptp4)
| ~ occurrence_of(VAR_0,tptp0) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_49_sk]) ).
cnf(c_234,plain,
( root_occ(sK3(A),A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
cnf(c_235,plain,
( occurrence_of(sK4(A),tptp3)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
cnf(c_236,plain,
( leaf_occ(sK4(A),A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
cnf(c_237,plain,
( next_subocc(sK3(A),sK4(A),tptp0)
| ~ 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_238,plain,
~ atomic(tptp0),
inference(clausify,[status(thm)],[sos_51]) ).
fof(sos_59,axiom,
tptp1 != tptp3,
file('theBenchmark.p',sos_59) ).
cnf(c_247,plain,
tptp1 != tptp3,
inference(clausify,[status(thm)],[sos_59]) ).
cnf(c_248,plain,
tptp3 != tptp1,
inference(copy,[status(thm)],[c_247]) ).
fof(nnf_51,plain,
! [X164,X165] :
( ? [X166] :
( next_subocc(X164,X166,tptp0)
& occurrence_of(X166,tptp1) )
| leaf_occ(X164,X165)
| ~ arboreal(X164)
| ~ subactivity_occurrence(X164,X165)
| ~ occurrence_of(X165,tptp0) ),
inference(fof_nnf,[status(thm)],[sos_62]) ).
fof(sk_sos_62_sk,plain,
! [X164,X165] :
( ( next_subocc(X164,sK5(X164,X165),tptp0)
& occurrence_of(sK5(X164,X165),tptp1) )
| leaf_occ(X164,X165)
| ~ arboreal(X164)
| ~ subactivity_occurrence(X164,X165)
| ~ occurrence_of(X165,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X166,sK5(X164,X165))],[nnf_51]) ).
fof(sk_sos_62,plain,
( ! [VAR_0,VAR_1] :
( next_subocc(VAR_1,sK5(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(sK5(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) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_62_sk]) ).
cnf(c_253,plain,
( occurrence_of(sK5(B,A),tptp1)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_62]) ).
cnf(c_254,plain,
( next_subocc(B,sK5(B,A),tptp0)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_62]) ).
fof(nnf_52,plain,
? [X167] : occurrence_of(X167,tptp0),
inference(fof_nnf,[status(thm)],[goals_neg]) ).
fof(sk_goals_neg,plain,
occurrence_of(sK6,tptp0),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X167,sK6)],[nnf_52]) ).
cnf(c_255,negated_conjecture,
occurrence_of(sK6,tptp0),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_291,plain,
( legal(sK0(B,A))
| atomic(B)
| ~ occurrence_of(A,B) ),
inference(resolve,[status(thm)],[c_90,c_84]) ).
cnf(c_292,plain,
( ~ min_precedes(C,sK0(B,A),B)
| atomic(B)
| ~ occurrence_of(A,B) ),
inference(resolve,[status(thm)],[c_90,c_83]) ).
cnf(c_296,plain,
( legal(A)
| ~ root_occ(A,B) ),
inference(resolve,[status(thm)],[c_91,c_84]) ).
cnf(c_300,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_92,c_90]) ).
cnf(c_345,plain,
( atomic(A)
| ~ subactivity_occurrence(sK0(A,B),B)
| ~ occurrence_of(B,A)
| root_occ(sK0(A,B),B) ),
inference(factor,[status(thm)],[c_300]) ).
cnf(c_363,plain,
next_subocc(sK3(sK6),sK4(sK6),tptp0),
inference(resolve,[status(thm)],[c_255,c_237]) ).
cnf(c_366,plain,
root_occ(sK3(sK6),sK6),
inference(resolve,[status(thm)],[c_255,c_234]) ).
cnf(c_375,plain,
( ~ min_precedes(A,B,tptp0)
| ~ leaf_occ(A,sK6) ),
inference(resolve,[status(thm)],[c_255,c_221]) ).
cnf(c_377,plain,
( B = A
| ~ root_occ(B,sK6)
| ~ root_occ(A,sK6) ),
inference(resolve,[status(thm)],[c_255,c_219]) ).
cnf(c_19488,negated_conjecture,
( subactivity_occurrence(sK0(tptp0,sK6),sK6)
| atomic(tptp0) ),
inference(resolve,[status(thm)],[c_255,c_211]) ).
cnf(c_380,negated_conjecture,
subactivity_occurrence(sK0(tptp0,sK6),sK6),
inference(resolve,[status(thm)],[c_238,c_19488]) ).
cnf(c_19489,negated_conjecture,
( legal(sK0(tptp0,sK6))
| atomic(tptp0) ),
inference(resolve,[status(thm)],[c_291,c_255]) ).
cnf(c_444,negated_conjecture,
legal(sK0(tptp0,sK6)),
inference(resolve,[status(thm)],[c_238,c_19489]) ).
cnf(c_19490,negated_conjecture,
( ~ min_precedes(A,sK0(tptp0,sK6),tptp0)
| atomic(tptp0) ),
inference(resolve,[status(thm)],[c_292,c_255]) ).
cnf(c_445,negated_conjecture,
~ min_precedes(A,sK0(tptp0,sK6),tptp0),
inference(resolve,[status(thm)],[c_238,c_19490]) ).
cnf(c_19491,negated_conjecture,
( atomic(tptp0)
| ~ subactivity_occurrence(sK0(tptp0,sK6),sK6)
| root_occ(sK0(tptp0,sK6),sK6) ),
inference(resolve,[status(thm)],[c_345,c_255]) ).
cnf(c_19492,negated_conjecture,
( atomic(tptp0)
| root_occ(sK0(tptp0,sK6),sK6) ),
inference(resolve,[status(thm)],[c_380,c_19491]) ).
cnf(c_477,negated_conjecture,
root_occ(sK0(tptp0,sK6),sK6),
inference(resolve,[status(thm)],[c_238,c_19492]) ).
cnf(c_556,plain,
legal(sK3(sK6)),
inference(resolve,[status(thm)],[c_366,c_296]) ).
cnf(c_565,plain,
subactivity_occurrence(sK3(sK6),sK6),
inference(resolve,[status(thm)],[c_366,c_216]) ).
cnf(c_580,plain,
arboreal(sK3(sK6)),
inference(resolve,[status(thm)],[c_556,c_196]) ).
cnf(c_19493,plain,
( A = sK3(sK6)
| ~ root_occ(A,sK6) ),
inference(resolve,[status(thm)],[c_377,c_366]) ).
cnf(c_630,plain,
( sK3(sK6) = A
| ~ root_occ(A,sK6) ),
inference(copy,[status(thm)],[c_19493]) ).
cnf(c_643,plain,
arboreal(sK0(tptp0,sK6)),
inference(resolve,[status(thm)],[c_444,c_196]) ).
cnf(c_19494,plain,
( next_subocc(sK3(sK6),sK5(sK3(sK6),sK6),tptp0)
| leaf_occ(sK3(sK6),sK6)
| ~ arboreal(sK3(sK6))
| ~ occurrence_of(sK6,tptp0) ),
inference(resolve,[status(thm)],[c_565,c_254]) ).
cnf(c_19495,negated_conjecture,
( next_subocc(sK3(sK6),sK5(sK3(sK6),sK6),tptp0)
| leaf_occ(sK3(sK6),sK6)
| ~ arboreal(sK3(sK6)) ),
inference(resolve,[status(thm)],[c_255,c_19494]) ).
cnf(c_669,negated_conjecture,
( next_subocc(sK3(sK6),sK5(sK3(sK6),sK6),tptp0)
| leaf_occ(sK3(sK6),sK6) ),
inference(resolve,[status(thm)],[c_580,c_19495]) ).
cnf(c_19496,plain,
( occurrence_of(sK5(sK3(sK6),sK6),tptp1)
| leaf_occ(sK3(sK6),sK6)
| ~ arboreal(sK3(sK6))
| ~ occurrence_of(sK6,tptp0) ),
inference(resolve,[status(thm)],[c_565,c_253]) ).
cnf(c_19497,negated_conjecture,
( occurrence_of(sK5(sK3(sK6),sK6),tptp1)
| leaf_occ(sK3(sK6),sK6)
| ~ arboreal(sK3(sK6)) ),
inference(resolve,[status(thm)],[c_255,c_19496]) ).
cnf(c_670,negated_conjecture,
( occurrence_of(sK5(sK3(sK6),sK6),tptp1)
| leaf_occ(sK3(sK6),sK6) ),
inference(resolve,[status(thm)],[c_580,c_19497]) ).
cnf(c_19498,plain,
( C = sK0(tptp0,sK6)
| min_precedes(C,sK0(tptp0,sK6),B)
| ~ root_occ(C,A)
| ~ subactivity_occurrence(sK0(tptp0,sK6),A)
| ~ occurrence_of(A,B) ),
inference(resolve,[status(thm)],[c_643,c_226]) ).
cnf(c_692,plain,
( sK0(tptp0,sK6) = C
| min_precedes(C,sK0(tptp0,sK6),B)
| ~ root_occ(C,A)
| ~ subactivity_occurrence(sK0(tptp0,sK6),A)
| ~ occurrence_of(A,B) ),
inference(copy,[status(thm)],[c_19498]) ).
cnf(c_733,plain,
min_precedes(sK3(sK6),sK4(sK6),tptp0),
inference(resolve,[status(thm)],[c_363,c_202]) ).
cnf(c_741,plain,
~ leaf_occ(sK3(sK6),sK6),
inference(resolve,[status(thm)],[c_733,c_375]) ).
cnf(c_793,negated_conjecture,
occurrence_of(sK5(sK3(sK6),sK6),tptp1),
inference(resolve,[status(thm)],[c_741,c_670]) ).
cnf(c_794,negated_conjecture,
next_subocc(sK3(sK6),sK5(sK3(sK6),sK6),tptp0),
inference(resolve,[status(thm)],[c_741,c_669]) ).
cnf(c_827,plain,
sK3(sK6) = sK0(tptp0,sK6),
inference(resolve,[status(thm)],[c_630,c_477]) ).
cnf(c_19499,negated_conjecture,
next_subocc(sK0(tptp0,sK6),sK5(sK3(sK6),sK6),tptp0),
inference(paramod,[status(thm)],[c_827,c_794]) ).
cnf(c_833,negated_conjecture,
next_subocc(sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6),tptp0),
inference(paramod,[status(thm)],[c_827,c_19499]) ).
cnf(c_834,negated_conjecture,
occurrence_of(sK5(sK0(tptp0,sK6),sK6),tptp1),
inference(paramod,[status(thm)],[c_827,c_793]) ).
cnf(c_1346,plain,
( tptp1 = A
| ~ occurrence_of(sK5(sK0(tptp0,sK6),sK6),A) ),
inference(resolve,[status(thm)],[c_834,c_190]) ).
cnf(c_1821,plain,
( sK5(sK0(tptp0,sK6),sK6) = A
| ~ subactivity_occurrence(A,B)
| ~ subactivity_occurrence(sK5(sK0(tptp0,sK6),sK6),B)
| ~ occurrence_of(B,tptp0)
| ~ next_subocc(sK0(tptp0,sK6),A,tptp0) ),
inference(resolve,[status(thm)],[c_833,c_223]) ).
cnf(c_1823,plain,
min_precedes(sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6),tptp0),
inference(resolve,[status(thm)],[c_833,c_202]) ).
cnf(c_2036,plain,
subactivity_occurrence(sK5(sK0(tptp0,sK6),sK6),sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6))),
inference(resolve,[status(thm)],[c_1823,c_210]) ).
cnf(c_2037,plain,
subactivity_occurrence(sK0(tptp0,sK6),sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6))),
inference(resolve,[status(thm)],[c_1823,c_209]) ).
cnf(c_2038,plain,
occurrence_of(sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6)),tptp0),
inference(resolve,[status(thm)],[c_1823,c_208]) ).
cnf(c_19500,plain,
( sK0(tptp0,sK6) = A
| min_precedes(A,sK0(tptp0,sK6),tptp0)
| ~ root_occ(A,sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6)))
| ~ subactivity_occurrence(sK0(tptp0,sK6),sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6))) ),
inference(resolve,[status(thm)],[c_2038,c_692]) ).
cnf(c_19501,plain,
( sK0(tptp0,sK6) = A
| min_precedes(A,sK0(tptp0,sK6),tptp0)
| ~ root_occ(A,sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6))) ),
inference(resolve,[status(thm)],[c_2037,c_19500]) ).
cnf(c_4227,plain,
( sK0(tptp0,sK6) = A
| ~ root_occ(A,sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6))) ),
inference(resolve,[status(thm)],[c_445,c_19501]) ).
cnf(c_4313,plain,
next_subocc(sK3(sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6))),sK4(sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6))),tptp0),
inference(resolve,[status(thm)],[c_2038,c_237]) ).
cnf(c_4314,plain,
leaf_occ(sK4(sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6))),sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6))),
inference(resolve,[status(thm)],[c_2038,c_236]) ).
cnf(c_4315,plain,
occurrence_of(sK4(sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6))),tptp3),
inference(resolve,[status(thm)],[c_2038,c_235]) ).
cnf(c_4316,plain,
root_occ(sK3(sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6))),sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6))),
inference(resolve,[status(thm)],[c_2038,c_234]) ).
cnf(c_19502,plain,
( sK5(sK0(tptp0,sK6),sK6) = A
| ~ subactivity_occurrence(A,sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6)))
| ~ subactivity_occurrence(sK5(sK0(tptp0,sK6),sK6),sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6)))
| ~ next_subocc(sK0(tptp0,sK6),A,tptp0) ),
inference(resolve,[status(thm)],[c_1821,c_2038]) ).
cnf(c_10225,plain,
( sK5(sK0(tptp0,sK6),sK6) = A
| ~ subactivity_occurrence(A,sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6)))
| ~ next_subocc(sK0(tptp0,sK6),A,tptp0) ),
inference(resolve,[status(thm)],[c_2036,c_19502]) ).
cnf(c_19233,plain,
subactivity_occurrence(sK4(sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6))),sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6))),
inference(resolve,[status(thm)],[c_4314,c_218]) ).
cnf(c_19503,plain,
sK0(tptp0,sK6) = sK3(sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6))),
inference(resolve,[status(thm)],[c_4316,c_4227]) ).
cnf(c_19246,plain,
sK3(sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6))) = sK0(tptp0,sK6),
inference(copy,[status(thm)],[c_19503]) ).
cnf(c_19247,plain,
next_subocc(sK0(tptp0,sK6),sK4(sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6))),tptp0),
inference(paramod,[status(thm)],[c_19246,c_4313]) ).
cnf(c_19504,plain,
( sK5(sK0(tptp0,sK6),sK6) = sK4(sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6)))
| ~ subactivity_occurrence(sK4(sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6))),sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6))) ),
inference(resolve,[status(thm)],[c_19247,c_10225]) ).
cnf(c_19505,plain,
( sK4(sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6))) = sK5(sK0(tptp0,sK6),sK6)
| ~ subactivity_occurrence(sK4(sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6))),sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6))) ),
inference(copy,[status(thm)],[c_19504]) ).
cnf(c_19250,plain,
sK4(sK2(tptp0,sK0(tptp0,sK6),sK5(sK0(tptp0,sK6),sK6))) = sK5(sK0(tptp0,sK6),sK6),
inference(resolve,[status(thm)],[c_19233,c_19505]) ).
cnf(c_19437,plain,
occurrence_of(sK5(sK0(tptp0,sK6),sK6),tptp3),
inference(paramod,[status(thm)],[c_19250,c_4315]) ).
cnf(c_19506,plain,
tptp1 = tptp3,
inference(resolve,[status(thm)],[c_19437,c_1346]) ).
cnf(c_19507,plain,
tptp3 = tptp1,
inference(copy,[status(thm)],[c_19506]) ).
cnf(c_19487,plain,
$false,
inference(resolve,[status(thm)],[c_248,c_19507]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO006+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/1.40 % Computer : n002.cluster.edu
% 0.10/1.40 % Model : x86_64 x86_64
% 0.10/1.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/1.40 % Memory : 8046.5625MB
% 0.10/1.40 % OS : Linux 6.8.0-71-generic
% 0.10/1.40 % CPULimit : 300
% 0.10/1.40 % WCLimit : 300
% 0.10/1.40 % DateTime : Sat Sep 26 04:59:07 UTC 2026
% 0.10/1.40 % CPUTime :
% 0.10/1.41 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/1.41 % Process 878428 was started by sandbox2 on n002,
% 0.10/1.41 % Sat Sep 26 04:59:07 2026
% 0.10/1.41 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/1.42
% 0.10/1.42 % From the command line: assign(max_seconds, 300).
% 100.95/15.31
% 100.95/15.31 % given #500 (F,wt=22): 1935 -atocc(f7(f12(tptp0,c1),tptp0),tptp0). [back_unit_del(1893),unit_del(b,1924)].
% 100.95/15.31
% 100.95/15.31 % given #1000 (F,wt=34): 4224 -leaf_occ(f12(tptp0,c1),f10(tptp0,f12(tptp0,c1),f19(f12(tptp0,c1),c1))). [resolve(2038,a,860,a)].
% 100.95/15.31
% 100.95/15.31 % given #1500 (F,wt=35): 6674 -min_precedes(f12(tptp0,c1),f5(f12(tptp0,c1),f19(f12(tptp0,c1),c1),tptp0),A). [resolve(2040,a,2047,b),unit_del(b,2027)].
% 100.95/15.31
% 100.95/15.31 % given #2000 (T,wt=40): 6929 -occurrence_of(f5(f12(tptp0,c1),f18(f11(tptp0,f12(tptp0,c1))),tptp0),A) | atomic(A). [resolve(6836,a,194,b)].
% 100.95/15.31
% 100.95/15.31 % given #2500 (T,wt=43): 4228 -leaf_occ(A,f10(tptp0,f12(tptp0,c1),f19(f12(tptp0,c1),c1))) | min_precedes(f12(tptp0,c1),A,tptp0) | f12(tptp0,c1) = A. [resolve(2038,a,691,a),unit_del(a,2037)].
% 100.95/15.31
% 100.95/15.31 % given #3000 (T,wt=40): 15675 occurrence_of(f16(f7(f12(tptp0,c1),tptp0),tptp0),tptp0) | -leaf_occ(f7(f12(tptp0,c1),tptp0),f11(tptp0,f12(tptp0,c1))). [resolve(1930,a,1220,b)].
% 100.95/15.31
% 100.95/15.31 % given #3500 (T,wt=45): 18326 leaf_occ(f19(f12(tptp0,c1),c1),f16(f19(f12(tptp0,c1),c1),tptp0)) | -next_subocc(f12(tptp0,c1),f7(f19(f12(tptp0,c1),c1),tptp0),tptp0). [resolve(2060,a,2039,b)].
% 100.95/15.31
% 100.95/15.31 % SZS status Theorem for theBenchmark
% 100.95/15.31
% 100.95/15.31 % Proof 1 at 5.01 (+ 0.75) seconds.
% 100.95/15.31 % Length of proof is 90.
% 100.95/15.31 % Level of proof is 15.
% 100.95/15.31 % Maximum clause weight is 49.000.
% 100.95/15.31 % Given clauses 3604.
% 100.95/15.31
% 100.95/15.31 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------