%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PRO005+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:54 AM UTC 2026
% Result : Theorem 40.59s 5.58s
% Output : CNFRefutation 40.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 21
% Syntax : Number of formulae : 129 ( 41 unt; 0 def)
% Number of atoms : 386 ( 22 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 402 ( 145 ~; 169 |; 71 &)
% ( 5 <=>; 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 : 14 ( 14 usr; 6 con; 0-3 aty)
% Number of variables : 210 ( 10 sgn 108 !; 23 ?)
% 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_07,axiom,
! [X16,X17] :
( occurrence_of(X16,X17)
=> ( arboreal(X16)
<=> atomic(X17) ) ),
file('theBenchmark.p',sos_07) ).
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_21,axiom,
! [X56,X57] :
( leaf(X56,X57)
<=> ( ~ ? [X59] : min_precedes(X56,X59,X57)
& ( ? [X58] : min_precedes(X58,X56,X57)
| root(X56,X57) ) ) ),
file('theBenchmark.p',sos_21) ).
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_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_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_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] :
( occurrence_of(X161,tptp0)
=> ? [X162,X163] :
( next_subocc(X162,X163,tptp0)
& leaf_occ(X163,X161)
& ( occurrence_of(X163,tptp2)
| 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) )
=> root_occ(X164,X165) ),
file('theBenchmark.p',sos_62) ).
fof(sos_63,axiom,
! [X166,X167] :
( ( ~ leaf_occ(X166,X167)
& arboreal(X166)
& subactivity_occurrence(X166,X167)
& occurrence_of(X167,tptp0) )
=> ? [X168] :
( next_subocc(X166,X168,tptp0)
& occurrence_of(X168,tptp1) ) ),
file('theBenchmark.p',sos_63) ).
fof(goals,conjecture,
~ ? [X169] : occurrence_of(X169,tptp0),
file('theBenchmark.p',goals) ).
fof(goals_neg,negated_conjecture,
~ ~ ? [X169] : occurrence_of(X169,tptp0),
inference(assume_negation,[status(cth)],[goals]) ).
cnf(c_85,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) )
& ( ? [X170] :
( root(X99,X170)
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,X170) )
| ~ 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(X170,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_92,plain,
( root(A,sK0(A,B))
| ~ root_occ(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_33]) ).
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,sK1(X145,X146))
& occurrence_of(sK1(X145,X146),X146) )
| atomic(X146)
| ~ leaf(X145,X146) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X147,sK1(X145,X146))],[nnf_46]) ).
fof(sk_sos_45,plain,
( ! [VAR_0,VAR_1] :
( leaf_occ(VAR_0,sK1(VAR_0,VAR_1))
| atomic(VAR_1)
| ~ leaf(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( occurrence_of(sK1(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_110,plain,
( leaf_occ(A,sK1(A,B))
| atomic(B)
| ~ leaf(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_45]) ).
cnf(c_111,plain,
( occurrence_of(sK1(A,B),B)
| atomic(B)
| ~ leaf(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_45]) ).
fof(nnf_22,plain,
! [X56,X57] :
( ( ? [X59] : min_precedes(X56,X59,X57)
| ( ! [X58] : ~ min_precedes(X58,X56,X57)
& ~ root(X56,X57) )
| leaf(X56,X57) )
& ( ( ! [X170] : ~ min_precedes(X56,X170,X57)
& ( ? [X171] : min_precedes(X171,X56,X57)
| root(X56,X57) ) )
| ~ leaf(X56,X57) ) ),
inference(fof_nnf,[status(thm)],[sos_21]) ).
fof(sk_sos_21_sk,plain,
! [X56,X57] :
( ( min_precedes(X56,sK2(X56,X57),X57)
| ( ! [X58] : ~ min_precedes(X58,X56,X57)
& ~ root(X56,X57) )
| leaf(X56,X57) )
& ( ( ! [X170] : ~ min_precedes(X56,X170,X57)
& ( min_precedes(sK8(X56,X57),X56,X57)
| root(X56,X57) ) )
| ~ leaf(X56,X57) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK2]),skolemize(X171,sK8(X56,X57)),skolemize(X59,sK2(X56,X57))],[nnf_22]) ).
fof(sk_sos_21,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( min_precedes(VAR_0,sK2(VAR_0,VAR_1),VAR_1)
| ~ min_precedes(VAR_2,VAR_0,VAR_1)
| leaf(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( min_precedes(VAR_0,sK2(VAR_0,VAR_1),VAR_1)
| ~ root(VAR_0,VAR_1)
| leaf(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ min_precedes(VAR_0,VAR_2,VAR_1)
| ~ leaf(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( min_precedes(sK8(VAR_0,VAR_1),VAR_0,VAR_1)
| root(VAR_0,VAR_1)
| ~ leaf(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_21_sk]) ).
cnf(c_114,plain,
( min_precedes(A,sK2(A,B),B)
| ~ min_precedes(C,A,B)
| leaf(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_21]) ).
cnf(c_123,plain,
( leaf_occ(B,sK1(B,C))
| atomic(C)
| min_precedes(B,sK2(B,C),C)
| ~ min_precedes(A,B,C) ),
inference(resolve,[status(thm)],[c_114,c_110]) ).
cnf(c_124,plain,
( occurrence_of(sK1(B,C),C)
| atomic(C)
| min_precedes(B,sK2(B,C),C)
| ~ min_precedes(A,B,C) ),
inference(resolve,[status(thm)],[c_114,c_111]) ).
cnf(c_191,plain,
( C = B
| ~ occurrence_of(A,C)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_02]) ).
cnf(c_196,plain,
( ~ atomic(B)
| arboreal(A)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_07]) ).
cnf(c_197,plain,
( arboreal(A)
| ~ legal(A) ),
inference(clausify,[status(thm)],[sos_08]) ).
cnf(c_203,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,sK3(X69,X70,X71))
& subactivity_occurrence(X70,sK3(X69,X70,X71))
& occurrence_of(sK3(X69,X70,X71),X69) )
| ~ min_precedes(X70,X71,X69) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X72,sK3(X69,X70,X71))],[nnf_26]) ).
fof(sk_sos_25,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( subactivity_occurrence(VAR_1,sK3(VAR_2,VAR_0,VAR_1))
| ~ min_precedes(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( subactivity_occurrence(VAR_0,sK3(VAR_2,VAR_0,VAR_1))
| ~ min_precedes(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( occurrence_of(sK3(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_209,plain,
( occurrence_of(sK3(C,A,B),C)
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_25]) ).
cnf(c_211,plain,
( subactivity_occurrence(B,sK3(C,A,B))
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_25]) ).
cnf(c_217,plain,
( subactivity_occurrence(A,B)
| ~ root_occ(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_33]) ).
cnf(c_219,plain,
( subactivity_occurrence(A,B)
| ~ leaf_occ(A,B) ),
inference(clausify,[status(thm)],[sos_34]) ).
cnf(c_222,plain,
( ~ min_precedes(C,D,B)
| ~ leaf_occ(C,A)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_37]) ).
cnf(c_223,plain,
( ~ min_precedes(D,C,B)
| ~ root_occ(C,A)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_38]) ).
cnf(c_228,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]) ).
fof(nnf_50,plain,
! [X161] :
( ? [X162,X163] :
( next_subocc(X162,X163,tptp0)
& leaf_occ(X163,X161)
& ( occurrence_of(X163,tptp2)
| 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(sK4(X161),sK5(X161),tptp0)
& leaf_occ(sK5(X161),X161)
& ( occurrence_of(sK5(X161),tptp2)
| occurrence_of(sK5(X161),tptp3) )
& root_occ(sK4(X161),X161)
& occurrence_of(sK4(X161),tptp4) )
| ~ occurrence_of(X161,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5]),skolemize(X162,sK4(X161)),skolemize(X163,sK5(X161))],[nnf_50]) ).
fof(sk_sos_49,plain,
( ! [VAR_0] :
( next_subocc(sK4(VAR_0),sK5(VAR_0),tptp0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( leaf_occ(sK5(VAR_0),VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( occurrence_of(sK5(VAR_0),tptp2)
| occurrence_of(sK5(VAR_0),tptp3)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( root_occ(sK4(VAR_0),VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( occurrence_of(sK4(VAR_0),tptp4)
| ~ occurrence_of(VAR_0,tptp0) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_49_sk]) ).
cnf(c_235,plain,
( root_occ(sK4(A),A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
cnf(c_236,plain,
( occurrence_of(sK5(A),tptp2)
| occurrence_of(sK5(A),tptp3)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
cnf(c_237,plain,
( leaf_occ(sK5(A),A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
cnf(c_238,plain,
( next_subocc(sK4(A),sK5(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_239,plain,
~ atomic(tptp0),
inference(clausify,[status(thm)],[sos_51]) ).
fof(sos_55,axiom,
atomic(tptp1),
file('theBenchmark.p',sos_55) ).
cnf(c_243,plain,
atomic(tptp1),
inference(clausify,[status(thm)],[sos_55]) ).
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(sos_60,axiom,
tptp1 != tptp2,
file('theBenchmark.p',sos_60) ).
cnf(c_249,plain,
tptp1 != tptp2,
inference(clausify,[status(thm)],[sos_60]) ).
cnf(c_250,plain,
tptp2 != tptp1,
inference(copy,[status(thm)],[c_249]) ).
cnf(c_252,plain,
( root_occ(B,A)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(clausify,[status(thm)],[sos_62]) ).
fof(nnf_52,plain,
! [X166,X167] :
( ? [X168] :
( next_subocc(X166,X168,tptp0)
& occurrence_of(X168,tptp1) )
| leaf_occ(X166,X167)
| ~ arboreal(X166)
| ~ subactivity_occurrence(X166,X167)
| ~ occurrence_of(X167,tptp0) ),
inference(fof_nnf,[status(thm)],[sos_63]) ).
fof(sk_sos_63_sk,plain,
! [X166,X167] :
( ( next_subocc(X166,sK6(X166,X167),tptp0)
& occurrence_of(sK6(X166,X167),tptp1) )
| leaf_occ(X166,X167)
| ~ arboreal(X166)
| ~ subactivity_occurrence(X166,X167)
| ~ occurrence_of(X167,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X168,sK6(X166,X167))],[nnf_52]) ).
fof(sk_sos_63,plain,
( ! [VAR_0,VAR_1] :
( next_subocc(VAR_1,sK6(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(sK6(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_63_sk]) ).
cnf(c_253,plain,
( occurrence_of(sK6(B,A),tptp1)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_63]) ).
cnf(c_254,plain,
( next_subocc(B,sK6(B,A),tptp0)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_63]) ).
fof(nnf_53,plain,
? [X169] : occurrence_of(X169,tptp0),
inference(fof_nnf,[status(thm)],[goals_neg]) ).
fof(sk_goals_neg,plain,
occurrence_of(sK7,tptp0),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X169,sK7)],[nnf_53]) ).
cnf(c_255,negated_conjecture,
occurrence_of(sK7,tptp0),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_296,plain,
( legal(A)
| ~ root_occ(A,B) ),
inference(resolve,[status(thm)],[c_92,c_85]) ).
cnf(c_360,plain,
( arboreal(A)
| ~ occurrence_of(A,tptp1) ),
inference(resolve,[status(thm)],[c_243,c_196]) ).
cnf(c_361,plain,
( next_subocc(A,sK6(A,sK7),tptp0)
| leaf_occ(A,sK7)
| ~ arboreal(A)
| ~ subactivity_occurrence(A,sK7) ),
inference(resolve,[status(thm)],[c_255,c_254]) ).
cnf(c_362,plain,
( occurrence_of(sK6(A,sK7),tptp1)
| leaf_occ(A,sK7)
| ~ arboreal(A)
| ~ subactivity_occurrence(A,sK7) ),
inference(resolve,[status(thm)],[c_255,c_253]) ).
cnf(c_364,plain,
next_subocc(sK4(sK7),sK5(sK7),tptp0),
inference(resolve,[status(thm)],[c_255,c_238]) ).
cnf(c_367,plain,
root_occ(sK4(sK7),sK7),
inference(resolve,[status(thm)],[c_255,c_235]) ).
cnf(c_376,plain,
( ~ min_precedes(A,B,tptp0)
| ~ leaf_occ(A,sK7) ),
inference(resolve,[status(thm)],[c_255,c_222]) ).
cnf(c_512,plain,
legal(sK4(sK7)),
inference(resolve,[status(thm)],[c_367,c_296]) ).
cnf(c_521,plain,
subactivity_occurrence(sK4(sK7),sK7),
inference(resolve,[status(thm)],[c_367,c_217]) ).
cnf(c_536,plain,
arboreal(sK4(sK7)),
inference(resolve,[status(thm)],[c_512,c_197]) ).
cnf(c_22690,plain,
( occurrence_of(sK6(sK4(sK7),sK7),tptp1)
| leaf_occ(sK4(sK7),sK7)
| ~ subactivity_occurrence(sK4(sK7),sK7) ),
inference(resolve,[status(thm)],[c_536,c_362]) ).
cnf(c_543,plain,
( occurrence_of(sK6(sK4(sK7),sK7),tptp1)
| leaf_occ(sK4(sK7),sK7) ),
inference(resolve,[status(thm)],[c_521,c_22690]) ).
cnf(c_22691,plain,
( next_subocc(sK4(sK7),sK6(sK4(sK7),sK7),tptp0)
| leaf_occ(sK4(sK7),sK7)
| ~ subactivity_occurrence(sK4(sK7),sK7) ),
inference(resolve,[status(thm)],[c_536,c_361]) ).
cnf(c_544,plain,
( next_subocc(sK4(sK7),sK6(sK4(sK7),sK7),tptp0)
| leaf_occ(sK4(sK7),sK7) ),
inference(resolve,[status(thm)],[c_521,c_22691]) ).
cnf(c_656,plain,
min_precedes(sK4(sK7),sK5(sK7),tptp0),
inference(resolve,[status(thm)],[c_364,c_203]) ).
cnf(c_738,plain,
~ leaf_occ(sK4(sK7),sK7),
inference(resolve,[status(thm)],[c_656,c_376]) ).
cnf(c_790,plain,
next_subocc(sK4(sK7),sK6(sK4(sK7),sK7),tptp0),
inference(resolve,[status(thm)],[c_738,c_544]) ).
cnf(c_791,plain,
occurrence_of(sK6(sK4(sK7),sK7),tptp1),
inference(resolve,[status(thm)],[c_738,c_543]) ).
cnf(c_1157,plain,
arboreal(sK6(sK4(sK7),sK7)),
inference(resolve,[status(thm)],[c_791,c_360]) ).
cnf(c_1189,plain,
( tptp1 = A
| ~ occurrence_of(sK6(sK4(sK7),sK7),A) ),
inference(resolve,[status(thm)],[c_791,c_191]) ).
cnf(c_22692,plain,
( C = sK6(sK4(sK7),sK7)
| min_precedes(sK6(sK4(sK7),sK7),C,B)
| ~ leaf_occ(C,A)
| ~ subactivity_occurrence(sK6(sK4(sK7),sK7),A)
| ~ occurrence_of(A,B) ),
inference(resolve,[status(thm)],[c_1157,c_228]) ).
cnf(c_1201,plain,
( sK6(sK4(sK7),sK7) = C
| min_precedes(sK6(sK4(sK7),sK7),C,B)
| ~ leaf_occ(C,A)
| ~ subactivity_occurrence(sK6(sK4(sK7),sK7),A)
| ~ occurrence_of(A,B) ),
inference(copy,[status(thm)],[c_22692]) ).
cnf(c_1818,plain,
min_precedes(sK4(sK7),sK6(sK4(sK7),sK7),tptp0),
inference(resolve,[status(thm)],[c_790,c_203]) ).
cnf(c_1994,plain,
( ~ root_occ(sK6(sK4(sK7),sK7),A)
| ~ occurrence_of(A,tptp0) ),
inference(resolve,[status(thm)],[c_1818,c_223]) ).
cnf(c_1996,plain,
subactivity_occurrence(sK6(sK4(sK7),sK7),sK3(tptp0,sK4(sK7),sK6(sK4(sK7),sK7))),
inference(resolve,[status(thm)],[c_1818,c_211]) ).
cnf(c_1998,plain,
occurrence_of(sK3(tptp0,sK4(sK7),sK6(sK4(sK7),sK7)),tptp0),
inference(resolve,[status(thm)],[c_1818,c_209]) ).
cnf(c_22693,plain,
( occurrence_of(sK1(sK6(sK4(sK7),sK7),tptp0),tptp0)
| atomic(tptp0)
| min_precedes(sK6(sK4(sK7),sK7),sK2(sK6(sK4(sK7),sK7),tptp0),tptp0) ),
inference(resolve,[status(thm)],[c_1818,c_124]) ).
cnf(c_2019,plain,
( occurrence_of(sK1(sK6(sK4(sK7),sK7),tptp0),tptp0)
| min_precedes(sK6(sK4(sK7),sK7),sK2(sK6(sK4(sK7),sK7),tptp0),tptp0) ),
inference(resolve,[status(thm)],[c_239,c_22693]) ).
cnf(c_22694,plain,
( leaf_occ(sK6(sK4(sK7),sK7),sK1(sK6(sK4(sK7),sK7),tptp0))
| atomic(tptp0)
| min_precedes(sK6(sK4(sK7),sK7),sK2(sK6(sK4(sK7),sK7),tptp0),tptp0) ),
inference(resolve,[status(thm)],[c_1818,c_123]) ).
cnf(c_2020,plain,
( leaf_occ(sK6(sK4(sK7),sK7),sK1(sK6(sK4(sK7),sK7),tptp0))
| min_precedes(sK6(sK4(sK7),sK7),sK2(sK6(sK4(sK7),sK7),tptp0),tptp0) ),
inference(resolve,[status(thm)],[c_239,c_22694]) ).
cnf(c_6254,plain,
~ root_occ(sK6(sK4(sK7),sK7),sK3(tptp0,sK4(sK7),sK6(sK4(sK7),sK7))),
inference(resolve,[status(thm)],[c_1998,c_1994]) ).
cnf(c_6417,plain,
( ~ min_precedes(A,B,tptp0)
| ~ leaf_occ(A,sK3(tptp0,sK4(sK7),sK6(sK4(sK7),sK7))) ),
inference(resolve,[status(thm)],[c_1998,c_222]) ).
cnf(c_22695,plain,
( root_occ(sK6(sK4(sK7),sK7),sK3(tptp0,sK4(sK7),sK6(sK4(sK7),sK7)))
| leaf_occ(sK6(sK4(sK7),sK7),sK3(tptp0,sK4(sK7),sK6(sK4(sK7),sK7)))
| ~ arboreal(sK6(sK4(sK7),sK7))
| ~ occurrence_of(sK3(tptp0,sK4(sK7),sK6(sK4(sK7),sK7)),tptp0) ),
inference(resolve,[status(thm)],[c_1996,c_252]) ).
cnf(c_22696,plain,
( root_occ(sK6(sK4(sK7),sK7),sK3(tptp0,sK4(sK7),sK6(sK4(sK7),sK7)))
| leaf_occ(sK6(sK4(sK7),sK7),sK3(tptp0,sK4(sK7),sK6(sK4(sK7),sK7)))
| ~ arboreal(sK6(sK4(sK7),sK7)) ),
inference(resolve,[status(thm)],[c_1998,c_22695]) ).
cnf(c_22697,plain,
( root_occ(sK6(sK4(sK7),sK7),sK3(tptp0,sK4(sK7),sK6(sK4(sK7),sK7)))
| leaf_occ(sK6(sK4(sK7),sK7),sK3(tptp0,sK4(sK7),sK6(sK4(sK7),sK7))) ),
inference(resolve,[status(thm)],[c_1157,c_22696]) ).
cnf(c_8571,plain,
leaf_occ(sK6(sK4(sK7),sK7),sK3(tptp0,sK4(sK7),sK6(sK4(sK7),sK7))),
inference(resolve,[status(thm)],[c_6254,c_22697]) ).
cnf(c_9446,plain,
~ min_precedes(sK6(sK4(sK7),sK7),A,tptp0),
inference(resolve,[status(thm)],[c_8571,c_6417]) ).
cnf(c_9462,plain,
leaf_occ(sK6(sK4(sK7),sK7),sK1(sK6(sK4(sK7),sK7),tptp0)),
inference(resolve,[status(thm)],[c_9446,c_2020]) ).
cnf(c_9463,plain,
occurrence_of(sK1(sK6(sK4(sK7),sK7),tptp0),tptp0),
inference(resolve,[status(thm)],[c_9446,c_2019]) ).
cnf(c_9729,plain,
leaf_occ(sK5(sK1(sK6(sK4(sK7),sK7),tptp0)),sK1(sK6(sK4(sK7),sK7),tptp0)),
inference(resolve,[status(thm)],[c_9463,c_237]) ).
cnf(c_9730,plain,
( occurrence_of(sK5(sK1(sK6(sK4(sK7),sK7),tptp0)),tptp2)
| occurrence_of(sK5(sK1(sK6(sK4(sK7),sK7),tptp0)),tptp3) ),
inference(resolve,[status(thm)],[c_9463,c_236]) ).
cnf(c_9775,plain,
subactivity_occurrence(sK6(sK4(sK7),sK7),sK1(sK6(sK4(sK7),sK7),tptp0)),
inference(resolve,[status(thm)],[c_9462,c_219]) ).
cnf(c_22698,plain,
( sK6(sK4(sK7),sK7) = A
| min_precedes(sK6(sK4(sK7),sK7),A,tptp0)
| ~ leaf_occ(A,sK1(sK6(sK4(sK7),sK7),tptp0))
| ~ subactivity_occurrence(sK6(sK4(sK7),sK7),sK1(sK6(sK4(sK7),sK7),tptp0)) ),
inference(resolve,[status(thm)],[c_1201,c_9463]) ).
cnf(c_22699,plain,
( sK6(sK4(sK7),sK7) = A
| min_precedes(sK6(sK4(sK7),sK7),A,tptp0)
| ~ leaf_occ(A,sK1(sK6(sK4(sK7),sK7),tptp0)) ),
inference(resolve,[status(thm)],[c_9775,c_22698]) ).
cnf(c_13738,plain,
( sK6(sK4(sK7),sK7) = A
| ~ leaf_occ(A,sK1(sK6(sK4(sK7),sK7),tptp0)) ),
inference(resolve,[status(thm)],[c_9446,c_22699]) ).
cnf(c_22700,plain,
sK6(sK4(sK7),sK7) = sK5(sK1(sK6(sK4(sK7),sK7),tptp0)),
inference(resolve,[status(thm)],[c_9729,c_13738]) ).
cnf(c_22545,plain,
sK5(sK1(sK6(sK4(sK7),sK7),tptp0)) = sK6(sK4(sK7),sK7),
inference(copy,[status(thm)],[c_22700]) ).
cnf(c_22701,plain,
( occurrence_of(sK5(sK1(sK6(sK4(sK7),sK7),tptp0)),tptp2)
| occurrence_of(sK6(sK4(sK7),sK7),tptp3) ),
inference(paramod,[status(thm)],[c_22545,c_9730]) ).
cnf(c_22546,plain,
( occurrence_of(sK6(sK4(sK7),sK7),tptp2)
| occurrence_of(sK6(sK4(sK7),sK7),tptp3) ),
inference(paramod,[status(thm)],[c_22545,c_22701]) ).
cnf(c_22702,plain,
( tptp1 = tptp3
| occurrence_of(sK6(sK4(sK7),sK7),tptp2) ),
inference(resolve,[status(thm)],[c_22546,c_1189]) ).
cnf(c_22703,plain,
( tptp3 = tptp1
| occurrence_of(sK6(sK4(sK7),sK7),tptp2) ),
inference(copy,[status(thm)],[c_22702]) ).
cnf(c_22596,plain,
occurrence_of(sK6(sK4(sK7),sK7),tptp2),
inference(resolve,[status(thm)],[c_248,c_22703]) ).
cnf(c_22704,plain,
tptp1 = tptp2,
inference(resolve,[status(thm)],[c_22596,c_1189]) ).
cnf(c_22705,plain,
tptp2 = tptp1,
inference(copy,[status(thm)],[c_22704]) ).
cnf(c_22689,plain,
$false,
inference(resolve,[status(thm)],[c_250,c_22705]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO005+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n018.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.38 % DateTime : Sat Sep 26 04:58:21 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.38 % Process 3757713 was started by sandbox on n018,
% 0.10/0.38 % Sat Sep 26 04:58:21 2026
% 0.10/0.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.39
% 0.10/0.39 % From the command line: assign(max_seconds, 300).
% 40.59/5.58
% 40.59/5.58 % given #500 (T,wt=23): 1956 -subactivity_occurrence(f17(c1),f18(c1)) | -leaf_occ(A,f18(c1)) | f17(c1) = A. [resolve(1024,c,536,a),flip(c)].
% 40.59/5.58
% 40.59/5.58 % given #1000 (W,wt=30): 1187 -root_occ(A,f19(f17(c1),c1)) | -root_occ(B,f19(f17(c1),c1)) | B = A. [resolve(791,a,220,a)].
% 40.59/5.58
% 40.59/5.58 % given #1500 (F,wt=58): 7187 -subactivity_occurrence(f13(tptp0,tptp1,c1,f19(f17(c1),f10(tptp0,f17(c1),f18(c1)))),c1) | -subactivity_occurrence(f10(tptp0,f17(c1),f19(f17(c1),c1)),f19(f17(c1),f10(tptp0,f17(c1),f18(c1)))). [resolve(7144,b,2112,a)].
% 40.59/5.58
% 40.59/5.58 % given #2000 (F,wt=31): 10072 -atocc(f19(f17(c1),f10(tptp0,f17(c1),f18(c1))),tptp0). [back_unit_del(10029),unit_del(b,10056)].
% 40.59/5.58
% 40.59/5.58 % given #2500 (T,wt=35): 8266 -occurrence_of(f16(f18(c1),tptp0),A) | -occurrence_of(f16(f18(c1),tptp0),tptp3) | atomic(A) | atocc(B,A) | -occurrence_of(B,tptp3). [resolve(8244,a,396,d)].
% 40.59/5.58
% 40.59/5.58 % given #3000 (A,wt=42): 1269 -occurrence_of(A,B) | -occurrence_of(C,tptp0) | subactivity_occurrence(A,C) | -subactivity_occurrence(f13(B,tptp0,A,C),A) | -occurrence_of(D,B) | atomic(B) | -subactivity_occurrence(D,f11(tptp0,f17(c1))). [resolve(831,a,268,f)].
% 40.59/5.58
% 40.59/5.58 % given #3500 (T,wt=37): 19597 f9(f18(c1),tptp3) = f1(f18(c1)) | -occurrence_of(c1,f4(f9(f18(c1),tptp2),f18(c1))). [resolve(12649,b,795,b)].
% 40.59/5.58
% 40.59/5.58 % given #4000 (W,wt=35): 21815 f9(f7(f17(c1),tptp0),tptp3) = tptp3 | f1(f7(f17(c1),tptp0)) = tptp2. [resolve(21773,a,8442,a)].
% 40.59/5.58
% 40.59/5.58 % SZS status Theorem for theBenchmark
% 40.59/5.58
% 40.59/5.58 % Proof 1 at 4.31 (+ 0.81) seconds.
% 40.59/5.58 % Length of proof is 88.
% 40.59/5.58 % Level of proof is 18.
% 40.59/5.58 % Maximum clause weight is 43.000.
% 40.59/5.58 % Given clauses 4142.
% 40.59/5.58
% 40.59/5.58 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------