%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PRO003+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:53 AM UTC 2026
% Result : Theorem 168.42s 22.82s
% Output : CNFRefutation 168.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 14
% Syntax : Number of formulae : 88 ( 31 unt; 0 def)
% Number of atoms : 248 ( 25 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 261 ( 101 ~; 94 |; 54 &)
% ( 3 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-3 aty)
% Number of variables : 156 ( 5 sgn 76 !; 16 ?)
% 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_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_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_38,axiom,
! [X117,X118,X119] :
( ( root_occ(X118,X117)
& occurrence_of(X117,X119) )
=> ~ ? [X120] : min_precedes(X120,X118,X119) ),
file('theBenchmark.p',sos_38) ).
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] :
( ( root_occ(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_84,plain,
( legal(A)
| ~ root(A,B) ),
inference(clausify,[status(thm)],[sos_16]) ).
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,sK0(X99,X100))
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,sK0(X99,X100)) )
| ~ root_occ(X99,X100) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X168,sK0(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,sK0(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,sK0(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,sK0(A,B))
| ~ 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,sK1(X69,X70,X71))
& subactivity_occurrence(X70,sK1(X69,X70,X71))
& occurrence_of(sK1(X69,X70,X71),X69) )
| ~ min_precedes(X70,X71,X69) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X72,sK1(X69,X70,X71))],[nnf_26]) ).
fof(sk_sos_25,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( subactivity_occurrence(VAR_1,sK1(VAR_2,VAR_0,VAR_1))
| ~ min_precedes(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( subactivity_occurrence(VAR_0,sK1(VAR_2,VAR_0,VAR_1))
| ~ min_precedes(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( occurrence_of(sK1(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(sK1(C,A,B),C)
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_25]) ).
cnf(c_209,plain,
( subactivity_occurrence(A,sK1(C,A,B))
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_25]) ).
cnf(c_210,plain,
( subactivity_occurrence(B,sK1(C,A,B))
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_25]) ).
cnf(c_218,plain,
( subactivity_occurrence(A,B)
| ~ leaf_occ(A,B) ),
inference(clausify,[status(thm)],[sos_34]) ).
cnf(c_222,plain,
( ~ min_precedes(D,C,B)
| ~ root_occ(C,A)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_38]) ).
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(sK2(X161),sK3(X161),tptp0)
& leaf_occ(sK3(X161),X161)
& occurrence_of(sK3(X161),tptp3)
& root_occ(sK2(X161),X161)
& occurrence_of(sK2(X161),tptp4) )
| ~ occurrence_of(X161,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3]),skolemize(X162,sK2(X161)),skolemize(X163,sK3(X161))],[nnf_50]) ).
fof(sk_sos_49,plain,
( ! [VAR_0] :
( next_subocc(sK2(VAR_0),sK3(VAR_0),tptp0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( leaf_occ(sK3(VAR_0),VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( occurrence_of(sK3(VAR_0),tptp3)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( root_occ(sK2(VAR_0),VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( occurrence_of(sK2(VAR_0),tptp4)
| ~ occurrence_of(VAR_0,tptp0) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_49_sk]) ).
cnf(c_234,plain,
( root_occ(sK2(A),A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
cnf(c_235,plain,
( occurrence_of(sK3(A),tptp3)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
cnf(c_236,plain,
( leaf_occ(sK3(A),A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
cnf(c_237,plain,
( next_subocc(sK2(A),sK3(A),tptp0)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
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) )
| ~ root_occ(X164,X165)
| ~ occurrence_of(X165,tptp0) ),
inference(fof_nnf,[status(thm)],[sos_62]) ).
fof(sk_sos_62_sk,plain,
! [X164,X165] :
( ( next_subocc(X164,sK4(X164,X165),tptp0)
& occurrence_of(sK4(X164,X165),tptp1) )
| ~ root_occ(X164,X165)
| ~ occurrence_of(X165,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X166,sK4(X164,X165))],[nnf_51]) ).
fof(sk_sos_62,plain,
( ! [VAR_0,VAR_1] :
( next_subocc(VAR_1,sK4(VAR_1,VAR_0),tptp0)
| ~ root_occ(VAR_1,VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0,VAR_1] :
( occurrence_of(sK4(VAR_1,VAR_0),tptp1)
| ~ root_occ(VAR_1,VAR_0)
| ~ occurrence_of(VAR_0,tptp0) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_62_sk]) ).
cnf(c_253,plain,
( occurrence_of(sK4(B,A),tptp1)
| ~ root_occ(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_62]) ).
cnf(c_254,plain,
( next_subocc(B,sK4(B,A),tptp0)
| ~ root_occ(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(sK5,tptp0),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X167,sK5)],[nnf_52]) ).
cnf(c_255,negated_conjecture,
occurrence_of(sK5,tptp0),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_296,plain,
( legal(A)
| ~ root_occ(A,B) ),
inference(resolve,[status(thm)],[c_91,c_84]) ).
cnf(c_361,plain,
( next_subocc(A,sK4(A,sK5),tptp0)
| ~ root_occ(A,sK5) ),
inference(resolve,[status(thm)],[c_255,c_254]) ).
cnf(c_362,plain,
( occurrence_of(sK4(A,sK5),tptp1)
| ~ root_occ(A,sK5) ),
inference(resolve,[status(thm)],[c_255,c_253]) ).
cnf(c_366,plain,
root_occ(sK2(sK5),sK5),
inference(resolve,[status(thm)],[c_255,c_234]) ).
cnf(c_374,plain,
( ~ min_precedes(B,A,tptp0)
| ~ root_occ(A,sK5) ),
inference(resolve,[status(thm)],[c_255,c_222]) ).
cnf(c_547,plain,
~ min_precedes(A,sK2(sK5),tptp0),
inference(resolve,[status(thm)],[c_366,c_374]) ).
cnf(c_548,plain,
occurrence_of(sK4(sK2(sK5),sK5),tptp1),
inference(resolve,[status(thm)],[c_366,c_362]) ).
cnf(c_549,plain,
next_subocc(sK2(sK5),sK4(sK2(sK5),sK5),tptp0),
inference(resolve,[status(thm)],[c_366,c_361]) ).
cnf(c_556,plain,
legal(sK2(sK5)),
inference(resolve,[status(thm)],[c_366,c_296]) ).
cnf(c_580,plain,
arboreal(sK2(sK5)),
inference(resolve,[status(thm)],[c_556,c_196]) ).
cnf(c_21310,plain,
( C = sK2(sK5)
| min_precedes(C,sK2(sK5),B)
| ~ root_occ(C,A)
| ~ subactivity_occurrence(sK2(sK5),A)
| ~ occurrence_of(A,B) ),
inference(resolve,[status(thm)],[c_580,c_226]) ).
cnf(c_588,plain,
( sK2(sK5) = C
| min_precedes(C,sK2(sK5),B)
| ~ root_occ(C,A)
| ~ subactivity_occurrence(sK2(sK5),A)
| ~ occurrence_of(A,B) ),
inference(copy,[status(thm)],[c_21310]) ).
cnf(c_980,plain,
( tptp1 = A
| ~ occurrence_of(sK4(sK2(sK5),sK5),A) ),
inference(resolve,[status(thm)],[c_548,c_190]) ).
cnf(c_1535,plain,
( sK4(sK2(sK5),sK5) = A
| ~ subactivity_occurrence(A,B)
| ~ subactivity_occurrence(sK4(sK2(sK5),sK5),B)
| ~ occurrence_of(B,tptp0)
| ~ next_subocc(sK2(sK5),A,tptp0) ),
inference(resolve,[status(thm)],[c_549,c_223]) ).
cnf(c_1537,plain,
min_precedes(sK2(sK5),sK4(sK2(sK5),sK5),tptp0),
inference(resolve,[status(thm)],[c_549,c_202]) ).
cnf(c_1987,plain,
subactivity_occurrence(sK4(sK2(sK5),sK5),sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5))),
inference(resolve,[status(thm)],[c_1537,c_210]) ).
cnf(c_1988,plain,
subactivity_occurrence(sK2(sK5),sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5))),
inference(resolve,[status(thm)],[c_1537,c_209]) ).
cnf(c_1989,plain,
occurrence_of(sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5)),tptp0),
inference(resolve,[status(thm)],[c_1537,c_208]) ).
cnf(c_21311,plain,
( sK2(sK5) = A
| min_precedes(A,sK2(sK5),tptp0)
| ~ root_occ(A,sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5)))
| ~ subactivity_occurrence(sK2(sK5),sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5))) ),
inference(resolve,[status(thm)],[c_1989,c_588]) ).
cnf(c_21312,plain,
( sK2(sK5) = A
| min_precedes(A,sK2(sK5),tptp0)
| ~ root_occ(A,sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5))) ),
inference(resolve,[status(thm)],[c_1988,c_21311]) ).
cnf(c_4507,plain,
( sK2(sK5) = A
| ~ root_occ(A,sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5))) ),
inference(resolve,[status(thm)],[c_547,c_21312]) ).
cnf(c_4614,plain,
next_subocc(sK2(sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5))),sK3(sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5))),tptp0),
inference(resolve,[status(thm)],[c_1989,c_237]) ).
cnf(c_4615,plain,
leaf_occ(sK3(sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5))),sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5))),
inference(resolve,[status(thm)],[c_1989,c_236]) ).
cnf(c_4616,plain,
occurrence_of(sK3(sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5))),tptp3),
inference(resolve,[status(thm)],[c_1989,c_235]) ).
cnf(c_4617,plain,
root_occ(sK2(sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5))),sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5))),
inference(resolve,[status(thm)],[c_1989,c_234]) ).
cnf(c_21313,plain,
( sK4(sK2(sK5),sK5) = A
| ~ subactivity_occurrence(A,sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5)))
| ~ subactivity_occurrence(sK4(sK2(sK5),sK5),sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5)))
| ~ next_subocc(sK2(sK5),A,tptp0) ),
inference(resolve,[status(thm)],[c_1535,c_1989]) ).
cnf(c_10369,plain,
( sK4(sK2(sK5),sK5) = A
| ~ subactivity_occurrence(A,sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5)))
| ~ next_subocc(sK2(sK5),A,tptp0) ),
inference(resolve,[status(thm)],[c_1987,c_21313]) ).
cnf(c_20999,plain,
subactivity_occurrence(sK3(sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5))),sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5))),
inference(resolve,[status(thm)],[c_4615,c_218]) ).
cnf(c_21314,plain,
sK2(sK5) = sK2(sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5))),
inference(resolve,[status(thm)],[c_4617,c_4507]) ).
cnf(c_21011,plain,
sK2(sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5))) = sK2(sK5),
inference(copy,[status(thm)],[c_21314]) ).
cnf(c_21012,plain,
next_subocc(sK2(sK5),sK3(sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5))),tptp0),
inference(paramod,[status(thm)],[c_21011,c_4614]) ).
cnf(c_21315,plain,
( sK4(sK2(sK5),sK5) = sK3(sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5)))
| ~ subactivity_occurrence(sK3(sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5))),sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5))) ),
inference(resolve,[status(thm)],[c_21012,c_10369]) ).
cnf(c_21316,plain,
( sK3(sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5))) = sK4(sK2(sK5),sK5)
| ~ subactivity_occurrence(sK3(sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5))),sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5))) ),
inference(copy,[status(thm)],[c_21315]) ).
cnf(c_21036,plain,
sK3(sK1(tptp0,sK2(sK5),sK4(sK2(sK5),sK5))) = sK4(sK2(sK5),sK5),
inference(resolve,[status(thm)],[c_20999,c_21316]) ).
cnf(c_21248,plain,
occurrence_of(sK4(sK2(sK5),sK5),tptp3),
inference(paramod,[status(thm)],[c_21036,c_4616]) ).
cnf(c_21317,plain,
tptp1 = tptp3,
inference(resolve,[status(thm)],[c_21248,c_980]) ).
cnf(c_21318,plain,
tptp3 = tptp1,
inference(copy,[status(thm)],[c_21317]) ).
cnf(c_21309,plain,
$false,
inference(resolve,[status(thm)],[c_248,c_21318]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO003+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.12/0.38 % Computer : n002.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sat Sep 26 04:57:50 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.39 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/0.39 % Process 877176 was started by sandbox2 on n002,
% 0.12/0.39 % Sat Sep 26 04:57:50 2026
% 0.12/0.39 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.12/0.40
% 0.12/0.40 % From the command line: assign(max_seconds, 300).
% 168.42/22.82
% 168.42/22.82 % given #500 (W,wt=23): 1550 -subactivity_occurrence(f18(c1),f17(c1)) | -root_occ(A,f17(c1)) | f18(c1) = A. [resolve(619,c,505,a),flip(c)].
% 168.42/22.82
% 168.42/22.82 % given #1000 (T,wt=30): 1295 atocc(f17(c1),f4(f4(tptp4,f17(c1)),f17(c1))). [resolve(681,a,282,a),unit_del(a,556)].
% 168.42/22.82
% 168.42/22.82 % given #1500 (F,wt=38): 6079 -root_occ(f19(f17(c1),f10(tptp0,f17(c1),f18(c1))),f10(tptp0,f17(c1),f7(f17(c1),tptp0))). [resolve(6048,a,4416,b)].
% 168.42/22.82
% 168.42/22.82 % given #2000 (T,wt=37): 4677 -occurrence_of(A,tptp0) | subactivity_occurrence(A,f17(c1)) | -subactivity_occurrence(f13(tptp0,tptp4,A,f17(c1)),A) | -subactivity_occurrence(f16(f18(c1),tptp0),f17(c1)). [resolve(599,d,789,a),unit_del(d,238)].
% 168.42/22.82
% 168.42/22.82 % given #2500 (F,wt=50): 13646 -legal(f18(f10(tptp0,f17(c1),f7(f17(c1),tptp0)))) | -min_precedes(A,f18(f10(tptp0,f17(c1),f7(f17(c1),tptp0))),f4(tptp3,f18(c1))). [resolve(8062,a,281,a)].
% 168.42/22.82
% 168.42/22.82 % given #3000 (T,wt=41): 4716 occurrence_of(f18(f11(tptp0,f17(c1))),f9(f18(f11(tptp0,f17(c1))),f4(tptp3,f18(c1)))). [resolve(2548,a,207,a)].
% 168.42/22.82
% 168.42/22.82 % given #3500 (A,wt=52): 1785 -occurrence_of(A,B) | subactivity_occurrence(f10(tptp0,f17(c1),f18(c1)),A) | subactivity_occurrence(f13(tptp0,B,f10(tptp0,f17(c1),f18(c1)),A),A) | -occurrence_of(C,tptp0) | -occurrence_of(D,B) | -subactivity_occurrence(C,D). [resolve(769,a,261,a),unit_del(f,238)].
% 168.42/22.82
% 168.42/22.82 % SZS status Theorem for theBenchmark
% 168.42/22.82
% 168.42/22.82 % Proof 1 at 5.26 (+ 0.88) seconds.
% 168.42/22.82 % Length of proof is 63.
% 168.42/22.82 % Level of proof is 11.
% 168.42/22.82 % Maximum clause weight is 45.000.
% 168.42/22.82 % Given clauses 3749.
% 168.42/22.82
% 168.42/22.82 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------