%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PRO016+4 : 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 : 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:59 AM UTC 2026
% Result : Theorem 10.78s 2.89s
% Output : CNFRefutation 10.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 12
% Syntax : Number of formulae : 124 ( 42 unt; 0 def)
% Number of atoms : 517 ( 18 equ)
% Maximal formula atoms : 88 ( 4 avg)
% Number of connectives : 618 ( 225 ~; 282 |; 96 &)
% ( 3 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 7 con; 0-2 aty)
% Number of variables : 159 ( 2 sgn 74 !; 21 ?)
% Comments :
%------------------------------------------------------------------------------
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_09,axiom,
! [X31,X32,X33] :
( ( leaf_occ(X32,X31)
& occurrence_of(X31,X33) )
=> ~ ? [X34] : min_precedes(X32,X34,X33) ),
file('theBenchmark.p',sos_09) ).
fof(sos_16,axiom,
! [X51,X52] :
( occurrence_of(X51,X52)
=> ( arboreal(X51)
<=> atomic(X52) ) ),
file('theBenchmark.p',sos_16) ).
fof(sos_18,axiom,
! [X55,X56] :
( leaf_occ(X55,X56)
<=> ? [X57] :
( leaf(X55,X57)
& subactivity_occurrence(X55,X56)
& occurrence_of(X56,X57) ) ),
file('theBenchmark.p',sos_18) ).
fof(sos_26,axiom,
! [X78,X79,X80] :
( next_subocc(X78,X79,X80)
<=> ( ~ ? [X81] :
( min_precedes(X81,X79,X80)
& min_precedes(X78,X81,X80) )
& min_precedes(X78,X79,X80) ) ),
file('theBenchmark.p',sos_26) ).
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_28,axiom,
! [X86,X87,X88,X89] :
( ( leaf_occ(X87,X88)
& leaf_occ(X86,X88)
& ~ atomic(X89)
& occurrence_of(X88,X89) )
=> X86 = X87 ),
file('theBenchmark.p',sos_28) ).
fof(sos_32,axiom,
! [X101,X102] :
( ( ~ leaf_occ(X101,X102)
& arboreal(X101)
& subactivity_occurrence(X101,X102)
& occurrence_of(X102,tptp0) )
=> ? [X103,X104,X105] :
( leaf_occ(X105,X102)
& next_subocc(X104,X105,tptp0)
& ( occurrence_of(X105,tptp2)
| occurrence_of(X105,tptp1) )
& next_subocc(X103,X104,tptp0)
& occurrence_of(X104,tptp4)
& next_subocc(X101,X103,tptp0)
& occurrence_of(X103,tptp3) ) ),
file('theBenchmark.p',sos_32) ).
fof(goals,conjecture,
! [X106,X107] :
( ( ~ leaf_occ(X106,X107)
& arboreal(X106)
& subactivity_occurrence(X106,X107)
& occurrence_of(X107,tptp0) )
=> ? [X108,X109] :
( ( occurrence_of(X109,tptp2)
=> ~ ? [X111] :
( min_precedes(X108,X111,tptp0)
& occurrence_of(X111,tptp1) ) )
& ( occurrence_of(X109,tptp1)
=> ~ ? [X110] :
( min_precedes(X108,X110,tptp0)
& occurrence_of(X110,tptp2) ) )
& leaf_occ(X109,X107)
& min_precedes(X108,X109,tptp0)
& ( occurrence_of(X109,tptp2)
| occurrence_of(X109,tptp1) )
& next_subocc(X106,X108,tptp0)
& occurrence_of(X108,tptp3) ) ),
file('theBenchmark.p',goals) ).
fof(goals_neg,negated_conjecture,
~ ! [X106,X107] :
( ( ~ leaf_occ(X106,X107)
& arboreal(X106)
& subactivity_occurrence(X106,X107)
& occurrence_of(X107,tptp0) )
=> ? [X108,X109] :
( ( occurrence_of(X109,tptp2)
=> ~ ? [X111] :
( min_precedes(X108,X111,tptp0)
& occurrence_of(X111,tptp1) ) )
& ( occurrence_of(X109,tptp1)
=> ~ ? [X110] :
( min_precedes(X108,X110,tptp0)
& occurrence_of(X110,tptp2) ) )
& leaf_occ(X109,X107)
& min_precedes(X108,X109,tptp0)
& ( occurrence_of(X109,tptp2)
| occurrence_of(X109,tptp1) )
& next_subocc(X106,X108,tptp0)
& occurrence_of(X108,tptp3) ) ),
inference(assume_negation,[status(cth)],[goals]) ).
cnf(c_97,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_102,plain,
( ~ min_precedes(C,D,B)
| ~ leaf_occ(C,A)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_09]) ).
cnf(c_107,plain,
( ~ atomic(B)
| arboreal(A)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_16]) ).
cnf(c_109,plain,
( subactivity_occurrence(A,B)
| ~ leaf_occ(A,B) ),
inference(clausify,[status(thm)],[sos_18]) ).
cnf(c_118,plain,
( min_precedes(A,B,C)
| ~ next_subocc(A,B,C) ),
inference(clausify,[status(thm)],[sos_26]) ).
cnf(c_119,plain,
( ~ min_precedes(D,B,C)
| ~ min_precedes(A,D,C)
| ~ next_subocc(A,B,C) ),
inference(clausify,[status(thm)],[sos_26]) ).
cnf(c_122,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_123,plain,
( D = C
| ~ leaf_occ(D,A)
| ~ leaf_occ(C,A)
| atomic(B)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_28]) ).
fof(nnf_33,plain,
! [X101,X102] :
( ? [X103,X104,X105] :
( leaf_occ(X105,X102)
& next_subocc(X104,X105,tptp0)
& ( occurrence_of(X105,tptp2)
| occurrence_of(X105,tptp1) )
& next_subocc(X103,X104,tptp0)
& occurrence_of(X104,tptp4)
& next_subocc(X101,X103,tptp0)
& occurrence_of(X103,tptp3) )
| leaf_occ(X101,X102)
| ~ arboreal(X101)
| ~ subactivity_occurrence(X101,X102)
| ~ occurrence_of(X102,tptp0) ),
inference(fof_nnf,[status(thm)],[sos_32]) ).
fof(sk_sos_32_sk,plain,
! [X101,X102] :
( ( leaf_occ(sK2(X101,X102),X102)
& next_subocc(sK1(X101,X102),sK2(X101,X102),tptp0)
& ( occurrence_of(sK2(X101,X102),tptp2)
| occurrence_of(sK2(X101,X102),tptp1) )
& next_subocc(sK0(X101,X102),sK1(X101,X102),tptp0)
& occurrence_of(sK1(X101,X102),tptp4)
& next_subocc(X101,sK0(X101,X102),tptp0)
& occurrence_of(sK0(X101,X102),tptp3) )
| leaf_occ(X101,X102)
| ~ arboreal(X101)
| ~ subactivity_occurrence(X101,X102)
| ~ occurrence_of(X102,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X103,sK0(X101,X102)),skolemize(X104,sK1(X101,X102)),skolemize(X105,sK2(X101,X102))],[nnf_33]) ).
fof(sk_sos_32,plain,
( ! [VAR_0,VAR_1] :
( leaf_occ(sK2(VAR_1,VAR_0),VAR_0)
| leaf_occ(VAR_1,VAR_0)
| ~ arboreal(VAR_1)
| ~ subactivity_occurrence(VAR_1,VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0,VAR_1] :
( next_subocc(sK1(VAR_1,VAR_0),sK2(VAR_1,VAR_0),tptp0)
| leaf_occ(VAR_1,VAR_0)
| ~ arboreal(VAR_1)
| ~ subactivity_occurrence(VAR_1,VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0,VAR_1] :
( occurrence_of(sK2(VAR_1,VAR_0),tptp2)
| occurrence_of(sK2(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) )
& ! [VAR_0,VAR_1] :
( next_subocc(sK0(VAR_1,VAR_0),sK1(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(sK1(VAR_1,VAR_0),tptp4)
| leaf_occ(VAR_1,VAR_0)
| ~ arboreal(VAR_1)
| ~ subactivity_occurrence(VAR_1,VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0,VAR_1] :
( next_subocc(VAR_1,sK0(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(sK0(VAR_1,VAR_0),tptp3)
| leaf_occ(VAR_1,VAR_0)
| ~ arboreal(VAR_1)
| ~ subactivity_occurrence(VAR_1,VAR_0)
| ~ occurrence_of(VAR_0,tptp0) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_32_sk]) ).
cnf(c_127,plain,
( occurrence_of(sK0(B,A),tptp3)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
cnf(c_128,plain,
( next_subocc(B,sK0(B,A),tptp0)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
cnf(c_129,plain,
( occurrence_of(sK1(B,A),tptp4)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
cnf(c_130,plain,
( next_subocc(sK0(B,A),sK1(B,A),tptp0)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
cnf(c_132,plain,
( next_subocc(sK1(B,A),sK2(B,A),tptp0)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
cnf(c_133,plain,
( leaf_occ(sK2(B,A),A)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
fof(sos_34,axiom,
~ atomic(tptp0),
file('theBenchmark.p',sos_34) ).
cnf(c_134,plain,
~ atomic(tptp0),
inference(clausify,[status(thm)],[sos_34]) ).
fof(sos_35,axiom,
atomic(tptp4),
file('theBenchmark.p',sos_35) ).
cnf(c_135,plain,
atomic(tptp4),
inference(clausify,[status(thm)],[sos_35]) ).
fof(sos_38,axiom,
atomic(tptp3),
file('theBenchmark.p',sos_38) ).
cnf(c_138,plain,
atomic(tptp3),
inference(clausify,[status(thm)],[sos_38]) ).
fof(nnf_34,plain,
? [X106,X107] :
( ! [X108,X109] :
( ( ? [X111] :
( min_precedes(X108,X111,tptp0)
& occurrence_of(X111,tptp1) )
& occurrence_of(X109,tptp2) )
| ( ? [X110] :
( min_precedes(X108,X110,tptp0)
& occurrence_of(X110,tptp2) )
& occurrence_of(X109,tptp1) )
| ~ leaf_occ(X109,X107)
| ~ min_precedes(X108,X109,tptp0)
| ( ~ occurrence_of(X109,tptp2)
& ~ occurrence_of(X109,tptp1) )
| ~ next_subocc(X106,X108,tptp0)
| ~ occurrence_of(X108,tptp3) )
& ~ leaf_occ(X106,X107)
& arboreal(X106)
& subactivity_occurrence(X106,X107)
& occurrence_of(X107,tptp0) ),
inference(fof_nnf,[status(thm)],[goals_neg]) ).
fof(sk_goals_neg_sk,plain,
( ! [X108,X109] :
( ( min_precedes(X108,sK8(X108,X109),tptp0)
& occurrence_of(sK8(X108,X109),tptp1)
& occurrence_of(X109,tptp2) )
| ( min_precedes(X108,sK7(X108,X109),tptp0)
& occurrence_of(sK7(X108,X109),tptp2)
& occurrence_of(X109,tptp1) )
| ~ leaf_occ(X109,sK3)
| ~ min_precedes(X108,X109,tptp0)
| ( ~ occurrence_of(X109,tptp2)
& ~ occurrence_of(X109,tptp1) )
| ~ next_subocc(sK4,X108,tptp0)
| ~ occurrence_of(X108,tptp3) )
& ~ leaf_occ(sK4,sK3)
& arboreal(sK4)
& subactivity_occurrence(sK4,sK3)
& occurrence_of(sK3,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK7,sK8]),skolemize(X106,sK4),skolemize(X107,sK3),skolemize(X110,sK7(X108,X109)),skolemize(X111,sK8(X108,X109))],[nnf_34]) ).
fof(sk_goals_neg,plain,
( ! [VAR_0,VAR_1] :
( min_precedes(VAR_0,sK8(VAR_0,VAR_1),tptp0)
| min_precedes(VAR_0,sK7(VAR_0,VAR_1),tptp0)
| ~ leaf_occ(VAR_1,sK3)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp2)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( occurrence_of(sK8(VAR_0,VAR_1),tptp1)
| min_precedes(VAR_0,sK7(VAR_0,VAR_1),tptp0)
| ~ leaf_occ(VAR_1,sK3)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp2)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( min_precedes(VAR_0,sK8(VAR_0,VAR_1),tptp0)
| occurrence_of(sK7(VAR_0,VAR_1),tptp2)
| ~ leaf_occ(VAR_1,sK3)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp2)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( occurrence_of(sK8(VAR_0,VAR_1),tptp1)
| occurrence_of(sK7(VAR_0,VAR_1),tptp2)
| ~ leaf_occ(VAR_1,sK3)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp2)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( min_precedes(VAR_0,sK8(VAR_0,VAR_1),tptp0)
| occurrence_of(VAR_1,tptp1)
| ~ leaf_occ(VAR_1,sK3)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp2)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( occurrence_of(sK8(VAR_0,VAR_1),tptp1)
| occurrence_of(VAR_1,tptp1)
| ~ leaf_occ(VAR_1,sK3)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp2)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( min_precedes(VAR_0,sK8(VAR_0,VAR_1),tptp0)
| min_precedes(VAR_0,sK7(VAR_0,VAR_1),tptp0)
| ~ leaf_occ(VAR_1,sK3)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp1)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( occurrence_of(sK8(VAR_0,VAR_1),tptp1)
| min_precedes(VAR_0,sK7(VAR_0,VAR_1),tptp0)
| ~ leaf_occ(VAR_1,sK3)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp1)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( occurrence_of(VAR_1,tptp2)
| min_precedes(VAR_0,sK7(VAR_0,VAR_1),tptp0)
| ~ leaf_occ(VAR_1,sK3)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp1)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( min_precedes(VAR_0,sK8(VAR_0,VAR_1),tptp0)
| occurrence_of(sK7(VAR_0,VAR_1),tptp2)
| ~ leaf_occ(VAR_1,sK3)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp1)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( occurrence_of(sK8(VAR_0,VAR_1),tptp1)
| occurrence_of(sK7(VAR_0,VAR_1),tptp2)
| ~ leaf_occ(VAR_1,sK3)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp1)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( occurrence_of(VAR_1,tptp2)
| occurrence_of(sK7(VAR_0,VAR_1),tptp2)
| ~ leaf_occ(VAR_1,sK3)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp1)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ~ leaf_occ(sK4,sK3)
& arboreal(sK4)
& subactivity_occurrence(sK4,sK3)
& occurrence_of(sK3,tptp0) ),
inference(cnf_transformation,[status(thm)],[sk_goals_neg_sk]) ).
cnf(c_146,negated_conjecture,
occurrence_of(sK3,tptp0),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_147,negated_conjecture,
subactivity_occurrence(sK4,sK3),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_148,negated_conjecture,
arboreal(sK4),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_149,negated_conjecture,
~ leaf_occ(sK4,sK3),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_211,plain,
( arboreal(A)
| ~ occurrence_of(A,tptp4) ),
inference(resolve,[status(thm)],[c_135,c_107]) ).
cnf(c_217,plain,
( arboreal(A)
| ~ occurrence_of(A,tptp3) ),
inference(resolve,[status(thm)],[c_138,c_107]) ).
cnf(c_219,plain,
( leaf_occ(sK2(A,sK3),sK3)
| leaf_occ(A,sK3)
| ~ arboreal(A)
| ~ subactivity_occurrence(A,sK3) ),
inference(resolve,[status(thm)],[c_146,c_133]) ).
cnf(c_220,plain,
( next_subocc(sK1(A,sK3),sK2(A,sK3),tptp0)
| leaf_occ(A,sK3)
| ~ arboreal(A)
| ~ subactivity_occurrence(A,sK3) ),
inference(resolve,[status(thm)],[c_146,c_132]) ).
cnf(c_222,plain,
( next_subocc(sK0(A,sK3),sK1(A,sK3),tptp0)
| leaf_occ(A,sK3)
| ~ arboreal(A)
| ~ subactivity_occurrence(A,sK3) ),
inference(resolve,[status(thm)],[c_146,c_130]) ).
cnf(c_223,plain,
( occurrence_of(sK1(A,sK3),tptp4)
| leaf_occ(A,sK3)
| ~ arboreal(A)
| ~ subactivity_occurrence(A,sK3) ),
inference(resolve,[status(thm)],[c_146,c_129]) ).
cnf(c_7161,negated_conjecture,
( B = A
| ~ leaf_occ(B,sK3)
| ~ leaf_occ(A,sK3)
| atomic(tptp0) ),
inference(resolve,[status(thm)],[c_146,c_123]) ).
cnf(c_227,negated_conjecture,
( B = A
| ~ leaf_occ(B,sK3)
| ~ leaf_occ(A,sK3) ),
inference(resolve,[status(thm)],[c_134,c_7161]) ).
cnf(c_228,plain,
( subactivity_occurrence(A,sK3)
| ~ subactivity_occurrence(B,sK3)
| ~ min_precedes(A,B,tptp0) ),
inference(resolve,[status(thm)],[c_146,c_122]) ).
cnf(c_231,plain,
( ~ min_precedes(A,B,tptp0)
| ~ leaf_occ(A,sK3) ),
inference(resolve,[status(thm)],[c_146,c_102]) ).
cnf(c_233,plain,
( B = A
| min_precedes(B,A,tptp0)
| min_precedes(A,B,tptp0)
| ~ subactivity_occurrence(B,sK3)
| ~ subactivity_occurrence(A,sK3)
| ~ arboreal(B)
| ~ arboreal(A) ),
inference(resolve,[status(thm)],[c_146,c_97]) ).
cnf(c_7162,negated_conjecture,
( leaf_occ(sK2(sK4,sK3),sK3)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4)
| ~ occurrence_of(sK3,tptp0) ),
inference(resolve,[status(thm)],[c_147,c_133]) ).
cnf(c_7163,negated_conjecture,
( leaf_occ(sK2(sK4,sK3),sK3)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4) ),
inference(resolve,[status(thm)],[c_146,c_7162]) ).
cnf(c_7164,negated_conjecture,
( leaf_occ(sK2(sK4,sK3),sK3)
| leaf_occ(sK4,sK3) ),
inference(resolve,[status(thm)],[c_148,c_7163]) ).
cnf(c_239,negated_conjecture,
leaf_occ(sK2(sK4,sK3),sK3),
inference(resolve,[status(thm)],[c_149,c_7164]) ).
cnf(c_7165,negated_conjecture,
( next_subocc(sK1(sK4,sK3),sK2(sK4,sK3),tptp0)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4)
| ~ occurrence_of(sK3,tptp0) ),
inference(resolve,[status(thm)],[c_147,c_132]) ).
cnf(c_7166,negated_conjecture,
( next_subocc(sK1(sK4,sK3),sK2(sK4,sK3),tptp0)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4) ),
inference(resolve,[status(thm)],[c_146,c_7165]) ).
cnf(c_7167,negated_conjecture,
( next_subocc(sK1(sK4,sK3),sK2(sK4,sK3),tptp0)
| leaf_occ(sK4,sK3) ),
inference(resolve,[status(thm)],[c_148,c_7166]) ).
cnf(c_240,negated_conjecture,
next_subocc(sK1(sK4,sK3),sK2(sK4,sK3),tptp0),
inference(resolve,[status(thm)],[c_149,c_7167]) ).
cnf(c_7168,negated_conjecture,
( next_subocc(sK0(sK4,sK3),sK1(sK4,sK3),tptp0)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4)
| ~ occurrence_of(sK3,tptp0) ),
inference(resolve,[status(thm)],[c_147,c_130]) ).
cnf(c_7169,negated_conjecture,
( next_subocc(sK0(sK4,sK3),sK1(sK4,sK3),tptp0)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4) ),
inference(resolve,[status(thm)],[c_146,c_7168]) ).
cnf(c_7170,negated_conjecture,
( next_subocc(sK0(sK4,sK3),sK1(sK4,sK3),tptp0)
| leaf_occ(sK4,sK3) ),
inference(resolve,[status(thm)],[c_148,c_7169]) ).
cnf(c_242,negated_conjecture,
next_subocc(sK0(sK4,sK3),sK1(sK4,sK3),tptp0),
inference(resolve,[status(thm)],[c_149,c_7170]) ).
cnf(c_7171,negated_conjecture,
( occurrence_of(sK1(sK4,sK3),tptp4)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4)
| ~ occurrence_of(sK3,tptp0) ),
inference(resolve,[status(thm)],[c_147,c_129]) ).
cnf(c_7172,negated_conjecture,
( occurrence_of(sK1(sK4,sK3),tptp4)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4) ),
inference(resolve,[status(thm)],[c_146,c_7171]) ).
cnf(c_7173,negated_conjecture,
( occurrence_of(sK1(sK4,sK3),tptp4)
| leaf_occ(sK4,sK3) ),
inference(resolve,[status(thm)],[c_148,c_7172]) ).
cnf(c_243,negated_conjecture,
occurrence_of(sK1(sK4,sK3),tptp4),
inference(resolve,[status(thm)],[c_149,c_7173]) ).
cnf(c_7174,negated_conjecture,
( occurrence_of(sK0(sK4,sK3),tptp3)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4)
| ~ occurrence_of(sK3,tptp0) ),
inference(resolve,[status(thm)],[c_147,c_127]) ).
cnf(c_7175,negated_conjecture,
( occurrence_of(sK0(sK4,sK3),tptp3)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4) ),
inference(resolve,[status(thm)],[c_146,c_7174]) ).
cnf(c_7176,negated_conjecture,
( occurrence_of(sK0(sK4,sK3),tptp3)
| leaf_occ(sK4,sK3) ),
inference(resolve,[status(thm)],[c_148,c_7175]) ).
cnf(c_245,negated_conjecture,
occurrence_of(sK0(sK4,sK3),tptp3),
inference(resolve,[status(thm)],[c_149,c_7176]) ).
cnf(c_321,plain,
( sK2(sK4,sK3) = A
| ~ leaf_occ(A,sK3) ),
inference(resolve,[status(thm)],[c_239,c_227]) ).
cnf(c_342,plain,
subactivity_occurrence(sK2(sK4,sK3),sK3),
inference(resolve,[status(thm)],[c_239,c_109]) ).
cnf(c_350,plain,
arboreal(sK1(sK4,sK3)),
inference(resolve,[status(thm)],[c_243,c_211]) ).
cnf(c_373,plain,
arboreal(sK0(sK4,sK3)),
inference(resolve,[status(thm)],[c_245,c_217]) ).
cnf(c_425,plain,
( subactivity_occurrence(A,sK3)
| ~ occurrence_of(sK3,B)
| ~ min_precedes(A,sK2(sK4,sK3),B) ),
inference(resolve,[status(thm)],[c_342,c_122]) ).
cnf(c_472,plain,
( leaf_occ(sK2(sK0(sK4,sK3),sK3),sK3)
| leaf_occ(sK0(sK4,sK3),sK3)
| ~ subactivity_occurrence(sK0(sK4,sK3),sK3) ),
inference(resolve,[status(thm)],[c_219,c_373]) ).
cnf(c_480,plain,
( next_subocc(sK1(sK0(sK4,sK3),sK3),sK2(sK0(sK4,sK3),sK3),tptp0)
| leaf_occ(sK0(sK4,sK3),sK3)
| ~ subactivity_occurrence(sK0(sK4,sK3),sK3) ),
inference(resolve,[status(thm)],[c_220,c_373]) ).
cnf(c_482,plain,
( ~ min_precedes(A,sK2(sK4,sK3),tptp0)
| ~ min_precedes(sK1(sK4,sK3),A,tptp0) ),
inference(resolve,[status(thm)],[c_240,c_119]) ).
cnf(c_483,plain,
min_precedes(sK1(sK4,sK3),sK2(sK4,sK3),tptp0),
inference(resolve,[status(thm)],[c_240,c_118]) ).
cnf(c_495,plain,
( ~ min_precedes(A,sK1(sK4,sK3),tptp0)
| ~ min_precedes(sK0(sK4,sK3),A,tptp0) ),
inference(resolve,[status(thm)],[c_242,c_119]) ).
cnf(c_496,plain,
min_precedes(sK0(sK4,sK3),sK1(sK4,sK3),tptp0),
inference(resolve,[status(thm)],[c_242,c_118]) ).
cnf(c_502,plain,
( next_subocc(sK0(sK0(sK4,sK3),sK3),sK1(sK0(sK4,sK3),sK3),tptp0)
| leaf_occ(sK0(sK4,sK3),sK3)
| ~ subactivity_occurrence(sK0(sK4,sK3),sK3) ),
inference(resolve,[status(thm)],[c_222,c_373]) ).
cnf(c_7177,plain,
( subactivity_occurrence(sK1(sK4,sK3),sK3)
| ~ subactivity_occurrence(sK2(sK4,sK3),sK3) ),
inference(resolve,[status(thm)],[c_483,c_228]) ).
cnf(c_507,plain,
subactivity_occurrence(sK1(sK4,sK3),sK3),
inference(resolve,[status(thm)],[c_342,c_7177]) ).
cnf(c_536,plain,
( ~ min_precedes(A,sK1(sK4,sK3),tptp0)
| ~ next_subocc(A,sK2(sK4,sK3),tptp0) ),
inference(resolve,[status(thm)],[c_483,c_119]) ).
cnf(c_571,plain,
( occurrence_of(sK1(sK0(sK4,sK3),sK3),tptp4)
| leaf_occ(sK0(sK4,sK3),sK3)
| ~ subactivity_occurrence(sK0(sK4,sK3),sK3) ),
inference(resolve,[status(thm)],[c_223,c_373]) ).
cnf(c_573,plain,
~ leaf_occ(sK0(sK4,sK3),sK3),
inference(resolve,[status(thm)],[c_496,c_231]) ).
cnf(c_7178,plain,
( subactivity_occurrence(sK0(sK4,sK3),sK3)
| ~ subactivity_occurrence(sK1(sK4,sK3),sK3) ),
inference(resolve,[status(thm)],[c_496,c_228]) ).
cnf(c_575,plain,
subactivity_occurrence(sK0(sK4,sK3),sK3),
inference(resolve,[status(thm)],[c_507,c_7178]) ).
cnf(c_7179,plain,
( occurrence_of(sK1(sK0(sK4,sK3),sK3),tptp4)
| leaf_occ(sK0(sK4,sK3),sK3) ),
inference(resolve,[status(thm)],[c_575,c_571]) ).
cnf(c_604,plain,
occurrence_of(sK1(sK0(sK4,sK3),sK3),tptp4),
inference(resolve,[status(thm)],[c_573,c_7179]) ).
cnf(c_7180,plain,
( next_subocc(sK0(sK0(sK4,sK3),sK3),sK1(sK0(sK4,sK3),sK3),tptp0)
| leaf_occ(sK0(sK4,sK3),sK3) ),
inference(resolve,[status(thm)],[c_575,c_502]) ).
cnf(c_605,plain,
next_subocc(sK0(sK0(sK4,sK3),sK3),sK1(sK0(sK4,sK3),sK3),tptp0),
inference(resolve,[status(thm)],[c_573,c_7180]) ).
cnf(c_7181,plain,
( next_subocc(sK1(sK0(sK4,sK3),sK3),sK2(sK0(sK4,sK3),sK3),tptp0)
| leaf_occ(sK0(sK4,sK3),sK3) ),
inference(resolve,[status(thm)],[c_575,c_480]) ).
cnf(c_607,plain,
next_subocc(sK1(sK0(sK4,sK3),sK3),sK2(sK0(sK4,sK3),sK3),tptp0),
inference(resolve,[status(thm)],[c_573,c_7181]) ).
cnf(c_7182,plain,
( leaf_occ(sK2(sK0(sK4,sK3),sK3),sK3)
| leaf_occ(sK0(sK4,sK3),sK3) ),
inference(resolve,[status(thm)],[c_575,c_472]) ).
cnf(c_608,plain,
leaf_occ(sK2(sK0(sK4,sK3),sK3),sK3),
inference(resolve,[status(thm)],[c_573,c_7182]) ).
cnf(c_7183,plain,
( next_subocc(sK0(sK4,sK3),sK0(sK0(sK4,sK3),sK3),tptp0)
| leaf_occ(sK0(sK4,sK3),sK3)
| ~ arboreal(sK0(sK4,sK3))
| ~ occurrence_of(sK3,tptp0) ),
inference(resolve,[status(thm)],[c_575,c_128]) ).
cnf(c_7184,negated_conjecture,
( next_subocc(sK0(sK4,sK3),sK0(sK0(sK4,sK3),sK3),tptp0)
| leaf_occ(sK0(sK4,sK3),sK3)
| ~ arboreal(sK0(sK4,sK3)) ),
inference(resolve,[status(thm)],[c_146,c_7183]) ).
cnf(c_7185,negated_conjecture,
( next_subocc(sK0(sK4,sK3),sK0(sK0(sK4,sK3),sK3),tptp0)
| leaf_occ(sK0(sK4,sK3),sK3) ),
inference(resolve,[status(thm)],[c_373,c_7184]) ).
cnf(c_616,negated_conjecture,
next_subocc(sK0(sK4,sK3),sK0(sK0(sK4,sK3),sK3),tptp0),
inference(resolve,[status(thm)],[c_573,c_7185]) ).
cnf(c_7186,plain,
( A = sK1(sK4,sK3)
| min_precedes(A,sK1(sK4,sK3),tptp0)
| min_precedes(sK1(sK4,sK3),A,tptp0)
| ~ subactivity_occurrence(A,sK3)
| ~ subactivity_occurrence(sK1(sK4,sK3),sK3)
| ~ arboreal(A) ),
inference(resolve,[status(thm)],[c_233,c_350]) ).
cnf(c_7187,plain,
( sK1(sK4,sK3) = A
| min_precedes(A,sK1(sK4,sK3),tptp0)
| min_precedes(sK1(sK4,sK3),A,tptp0)
| ~ subactivity_occurrence(A,sK3)
| ~ subactivity_occurrence(sK1(sK4,sK3),sK3)
| ~ arboreal(A) ),
inference(copy,[status(thm)],[c_7186]) ).
cnf(c_644,plain,
( sK1(sK4,sK3) = A
| min_precedes(A,sK1(sK4,sK3),tptp0)
| min_precedes(sK1(sK4,sK3),A,tptp0)
| ~ subactivity_occurrence(A,sK3)
| ~ arboreal(A) ),
inference(resolve,[status(thm)],[c_507,c_7187]) ).
cnf(c_963,plain,
arboreal(sK1(sK0(sK4,sK3),sK3)),
inference(resolve,[status(thm)],[c_604,c_211]) ).
cnf(c_7188,plain,
sK2(sK4,sK3) = sK2(sK0(sK4,sK3),sK3),
inference(resolve,[status(thm)],[c_608,c_321]) ).
cnf(c_998,plain,
sK2(sK0(sK4,sK3),sK3) = sK2(sK4,sK3),
inference(copy,[status(thm)],[c_7188]) ).
cnf(c_999,plain,
next_subocc(sK1(sK0(sK4,sK3),sK3),sK2(sK4,sK3),tptp0),
inference(paramod,[status(thm)],[c_998,c_607]) ).
cnf(c_1817,plain,
~ min_precedes(sK1(sK0(sK4,sK3),sK3),sK1(sK4,sK3),tptp0),
inference(resolve,[status(thm)],[c_999,c_536]) ).
cnf(c_1819,plain,
min_precedes(sK1(sK0(sK4,sK3),sK3),sK2(sK4,sK3),tptp0),
inference(resolve,[status(thm)],[c_999,c_118]) ).
cnf(c_2222,plain,
~ min_precedes(sK1(sK4,sK3),sK1(sK0(sK4,sK3),sK3),tptp0),
inference(resolve,[status(thm)],[c_1819,c_482]) ).
cnf(c_7189,plain,
( subactivity_occurrence(sK1(sK0(sK4,sK3),sK3),sK3)
| ~ occurrence_of(sK3,tptp0) ),
inference(resolve,[status(thm)],[c_1819,c_425]) ).
cnf(c_2223,negated_conjecture,
subactivity_occurrence(sK1(sK0(sK4,sK3),sK3),sK3),
inference(resolve,[status(thm)],[c_146,c_7189]) ).
cnf(c_3198,plain,
min_precedes(sK0(sK4,sK3),sK0(sK0(sK4,sK3),sK3),tptp0),
inference(resolve,[status(thm)],[c_616,c_118]) ).
cnf(c_3608,plain,
~ min_precedes(sK0(sK0(sK4,sK3),sK3),sK1(sK4,sK3),tptp0),
inference(resolve,[status(thm)],[c_3198,c_495]) ).
cnf(c_6772,plain,
min_precedes(sK0(sK0(sK4,sK3),sK3),sK1(sK0(sK4,sK3),sK3),tptp0),
inference(resolve,[status(thm)],[c_605,c_118]) ).
cnf(c_7190,plain,
( sK1(sK4,sK3) = sK1(sK0(sK4,sK3),sK3)
| min_precedes(sK1(sK0(sK4,sK3),sK3),sK1(sK4,sK3),tptp0)
| min_precedes(sK1(sK4,sK3),sK1(sK0(sK4,sK3),sK3),tptp0)
| ~ subactivity_occurrence(sK1(sK0(sK4,sK3),sK3),sK3) ),
inference(resolve,[status(thm)],[c_644,c_963]) ).
cnf(c_7191,plain,
( sK1(sK0(sK4,sK3),sK3) = sK1(sK4,sK3)
| min_precedes(sK1(sK0(sK4,sK3),sK3),sK1(sK4,sK3),tptp0)
| min_precedes(sK1(sK4,sK3),sK1(sK0(sK4,sK3),sK3),tptp0)
| ~ subactivity_occurrence(sK1(sK0(sK4,sK3),sK3),sK3) ),
inference(copy,[status(thm)],[c_7190]) ).
cnf(c_7192,plain,
( sK1(sK0(sK4,sK3),sK3) = sK1(sK4,sK3)
| min_precedes(sK1(sK0(sK4,sK3),sK3),sK1(sK4,sK3),tptp0)
| min_precedes(sK1(sK4,sK3),sK1(sK0(sK4,sK3),sK3),tptp0) ),
inference(resolve,[status(thm)],[c_2223,c_7191]) ).
cnf(c_7193,plain,
( sK1(sK0(sK4,sK3),sK3) = sK1(sK4,sK3)
| min_precedes(sK1(sK0(sK4,sK3),sK3),sK1(sK4,sK3),tptp0) ),
inference(resolve,[status(thm)],[c_2222,c_7192]) ).
cnf(c_7120,plain,
sK1(sK0(sK4,sK3),sK3) = sK1(sK4,sK3),
inference(resolve,[status(thm)],[c_1817,c_7193]) ).
cnf(c_7194,plain,
min_precedes(sK0(sK0(sK4,sK3),sK3),sK1(sK4,sK3),tptp0),
inference(paramod,[status(thm)],[c_7120,c_6772]) ).
cnf(c_7160,plain,
$false,
inference(resolve,[status(thm)],[c_3608,c_7194]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO016+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/1.40 % Computer : n002.cluster.edu
% 0.11/1.40 % Model : x86_64 x86_64
% 0.11/1.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/1.40 % Memory : 8046.5625MB
% 0.11/1.40 % OS : Linux 6.8.0-71-generic
% 0.11/1.40 % CPULimit : 300
% 0.11/1.40 % WCLimit : 300
% 0.11/1.40 % DateTime : Sat Sep 26 05:03:23 UTC 2026
% 0.11/1.41 % CPUTime :
% 0.11/1.41 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/1.41 % Process 881723 was started by sandbox on n002,
% 0.11/1.41 % Sat Sep 26 05:03:23 2026
% 0.11/1.41 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.11/1.41
% 0.11/1.41 % From the command line: assign(max_seconds, 300).
% 10.78/2.89
% 10.78/2.89 % Assigning unary symbol f5 kb_weight 0 and highest precedence (36).
% 10.78/2.89
% 10.78/2.89 % given #500 (F,wt=22): 1832 -root_occ(f8(f14(c1,c2),tptp0),c2). [resolve(1083,a,230,b)].
% 10.78/2.89
% 10.78/2.89 % given #1000 (T,wt=20): 4106 -precedes(f15(c1,c2),c1) | f1(tptp0,c2) = c1. [resolve(4064,a,721,a)].
% 10.78/2.89
% 10.78/2.89 % SZS status Theorem for theBenchmark
% 10.78/2.89
% 10.78/2.89 % Proof 1 at 1.15 (+ 0.30) seconds.
% 10.78/2.89 % Length of proof is 80.
% 10.78/2.89 % Level of proof is 12.
% 10.78/2.89 % Maximum clause weight is 39.000.
% 10.78/2.89 % Given clauses 1401.
% 10.78/2.89
% 10.78/2.89 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------