%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PRO009+1 : 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 : n010.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:56 AM UTC 2026
% Result : Theorem 1.59s 0.61s
% Output : CNFRefutation 1.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 13
% Syntax : Number of formulae : 107 ( 24 unt; 0 def)
% Number of atoms : 376 ( 25 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 434 ( 165 ~; 177 |; 78 &)
% ( 5 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-2 aty)
% Number of variables : 198 ( 19 sgn 95 !; 20 ?)
% 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_10,axiom,
! [X21,X22] :
( precedes(X21,X22)
<=> ( legal(X22)
& earlier(X21,X22) ) ),
file('theBenchmark.p',sos_10) ).
fof(sos_14,axiom,
! [X35,X36,X37] :
( min_precedes(X35,X36,X37)
=> ~ root(X36,X37) ),
file('theBenchmark.p',sos_14) ).
fof(sos_15,axiom,
! [X38,X39,X40] :
( min_precedes(X38,X39,X40)
=> precedes(X38,X39) ),
file('theBenchmark.p',sos_15) ).
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_28,axiom,
! [X79,X80,X81,X82] :
( ( subactivity_occurrence(X82,X80)
& subactivity_occurrence(X81,X80)
& arboreal(X82)
& arboreal(X81)
& occurrence_of(X80,X79) )
=> ( X81 = X82
| min_precedes(X82,X81,X79)
| min_precedes(X81,X82,X79) ) ),
file('theBenchmark.p',sos_28) ).
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] :
( occurrence_of(X105,tptp0)
=> ? [X106,X107,X108] :
( leaf_occ(X108,X105)
& next_subocc(X107,X108,tptp0)
& ( occurrence_of(X108,tptp1)
| occurrence_of(X108,tptp2) )
& next_subocc(X106,X107,tptp0)
& occurrence_of(X107,tptp4)
& root_occ(X106,X105)
& occurrence_of(X106,tptp3) ) ),
file('theBenchmark.p',sos_35) ).
fof(goals,conjecture,
! [X109] :
( occurrence_of(X109,tptp0)
=> ? [X110,X111] :
( leaf_occ(X111,X109)
& min_precedes(X110,X111,tptp0)
& ( occurrence_of(X111,tptp1)
| occurrence_of(X111,tptp2) )
& root_occ(X110,X109)
& occurrence_of(X110,tptp3) ) ),
file('theBenchmark.p',goals) ).
fof(goals_neg,negated_conjecture,
~ ! [X109] :
( occurrence_of(X109,tptp0)
=> ? [X110,X111] :
( leaf_occ(X111,X109)
& min_precedes(X110,X111,tptp0)
& ( occurrence_of(X111,tptp1)
| occurrence_of(X111,tptp2) )
& root_occ(X110,X109)
& occurrence_of(X110,tptp3) ) ),
inference(assume_negation,[status(cth)],[goals]) ).
cnf(c_60,plain,
( precedes(A,B)
| ~ min_precedes(A,B,C) ),
inference(clausify,[status(thm)],[sos_15]) ).
cnf(c_64,plain,
( legal(B)
| ~ precedes(A,B) ),
inference(clausify,[status(thm)],[sos_10]) ).
cnf(c_68,plain,
( ~ root(B,C)
| ~ min_precedes(A,B,C) ),
inference(clausify,[status(thm)],[sos_14]) ).
cnf(c_69,plain,
( legal(A)
| ~ root(A,B) ),
inference(clausify,[status(thm)],[sos_16]) ).
fof(nnf_22,plain,
! [X56,X57] :
( ( ? [X59] : min_precedes(X56,X59,X57)
| ( ! [X58] : ~ min_precedes(X58,X56,X57)
& ~ root(X56,X57) )
| leaf(X56,X57) )
& ( ( ! [X113] : ~ min_precedes(X56,X113,X57)
& ( ? [X112] : min_precedes(X112,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,sK3(X56,X57),X57)
| ( ! [X58] : ~ min_precedes(X58,X56,X57)
& ~ root(X56,X57) )
| leaf(X56,X57) )
& ( ( ! [X113] : ~ min_precedes(X56,X113,X57)
& ( min_precedes(sK0(X56,X57),X56,X57)
| root(X56,X57) ) )
| ~ leaf(X56,X57) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK3]),skolemize(X112,sK0(X56,X57)),skolemize(X59,sK3(X56,X57))],[nnf_22]) ).
fof(sk_sos_21,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( min_precedes(VAR_0,sK3(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,sK3(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(sK0(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_71,plain,
( min_precedes(sK0(A,B),A,B)
| root(A,B)
| ~ leaf(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_21]) ).
fof(nnf_34,plain,
! [X99,X100] :
( ( ! [X101] :
( ~ root(X99,X101)
| ~ subactivity_occurrence(X99,X100)
| ~ occurrence_of(X100,X101) )
| root_occ(X99,X100) )
& ( ? [X113] :
( root(X99,X113)
& subactivity_occurrence(X99,X100)
& occurrence_of(X100,X113) )
| ~ 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(X113,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_76,plain,
( root(A,sK1(A,B))
| ~ root_occ(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_33]) ).
cnf(c_92,plain,
( ~ min_precedes(C,A,B)
| min_precedes(sK0(A,B),A,B)
| ~ leaf(A,B) ),
inference(resolve,[status(thm)],[c_71,c_68]) ).
fof(nnf_35,plain,
! [X102,X103] :
( ( ! [X104] :
( ~ leaf(X102,X104)
| ~ subactivity_occurrence(X102,X103)
| ~ occurrence_of(X103,X104) )
| leaf_occ(X102,X103) )
& ( ? [X113] :
( leaf(X102,X113)
& subactivity_occurrence(X102,X103)
& occurrence_of(X103,X113) )
| ~ leaf_occ(X102,X103) ) ),
inference(fof_nnf,[status(thm)],[sos_34]) ).
fof(sk_sos_34_sk,plain,
! [X102,X103] :
( ( ! [X104] :
( ~ leaf(X102,X104)
| ~ subactivity_occurrence(X102,X103)
| ~ occurrence_of(X103,X104) )
| leaf_occ(X102,X103) )
& ( ( leaf(X102,sK2(X102,X103))
& subactivity_occurrence(X102,X103)
& occurrence_of(X103,sK2(X102,X103)) )
| ~ leaf_occ(X102,X103) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X113,sK2(X102,X103))],[nnf_35]) ).
fof(sk_sos_34,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( ~ leaf(VAR_0,VAR_2)
| ~ subactivity_occurrence(VAR_0,VAR_1)
| ~ occurrence_of(VAR_1,VAR_2)
| leaf_occ(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( leaf(VAR_0,sK2(VAR_0,VAR_1))
| ~ leaf_occ(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( subactivity_occurrence(VAR_0,VAR_1)
| ~ leaf_occ(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( occurrence_of(VAR_1,sK2(VAR_0,VAR_1))
| ~ leaf_occ(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_34_sk]) ).
cnf(c_95,plain,
( leaf(A,sK2(A,B))
| ~ leaf_occ(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_34]) ).
cnf(c_96,plain,
( min_precedes(A,sK3(A,B),B)
| ~ min_precedes(C,A,B)
| leaf(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_21]) ).
cnf(c_97,plain,
( ~ min_precedes(A,C,B)
| ~ leaf(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_21]) ).
cnf(c_100,plain,
( min_precedes(A,B,C)
| ~ next_subocc(A,B,C) ),
inference(clausify,[status(thm)],[sos_22]) ).
fof(nnf_36,plain,
! [X105] :
( ? [X106,X107,X108] :
( leaf_occ(X108,X105)
& next_subocc(X107,X108,tptp0)
& ( occurrence_of(X108,tptp1)
| occurrence_of(X108,tptp2) )
& next_subocc(X106,X107,tptp0)
& occurrence_of(X107,tptp4)
& root_occ(X106,X105)
& occurrence_of(X106,tptp3) )
| ~ occurrence_of(X105,tptp0) ),
inference(fof_nnf,[status(thm)],[sos_35]) ).
fof(sk_sos_35_sk,plain,
! [X105] :
( ( leaf_occ(sK5(X105),X105)
& next_subocc(sK4(X105),sK5(X105),tptp0)
& ( occurrence_of(sK5(X105),tptp1)
| occurrence_of(sK5(X105),tptp2) )
& next_subocc(sK7(X105),sK4(X105),tptp0)
& occurrence_of(sK4(X105),tptp4)
& root_occ(sK7(X105),X105)
& occurrence_of(sK7(X105),tptp3) )
| ~ occurrence_of(X105,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK4,sK5]),skolemize(X106,sK7(X105)),skolemize(X107,sK4(X105)),skolemize(X108,sK5(X105))],[nnf_36]) ).
fof(sk_sos_35,plain,
( ! [VAR_0] :
( leaf_occ(sK5(VAR_0),VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( next_subocc(sK4(VAR_0),sK5(VAR_0),tptp0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( occurrence_of(sK5(VAR_0),tptp1)
| occurrence_of(sK5(VAR_0),tptp2)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( next_subocc(sK7(VAR_0),sK4(VAR_0),tptp0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( occurrence_of(sK4(VAR_0),tptp4)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( root_occ(sK7(VAR_0),VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( occurrence_of(sK7(VAR_0),tptp3)
| ~ occurrence_of(VAR_0,tptp0) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_35_sk]) ).
cnf(c_103,plain,
( next_subocc(sK4(A),sK5(A),tptp0)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_35]) ).
cnf(c_104,plain,
( min_precedes(sK4(A),sK5(A),tptp0)
| ~ occurrence_of(A,tptp0) ),
inference(resolve,[status(thm)],[c_103,c_100]) ).
cnf(c_126,plain,
( ~ min_precedes(C,A,sK1(A,B))
| ~ root_occ(A,B) ),
inference(resolve,[status(thm)],[c_76,c_68]) ).
cnf(c_127,plain,
( legal(A)
| ~ root_occ(A,B) ),
inference(resolve,[status(thm)],[c_76,c_69]) ).
fof(nnf_37,plain,
? [X109] :
( ! [X110,X111] :
( ~ leaf_occ(X111,X109)
| ~ min_precedes(X110,X111,tptp0)
| ( ~ occurrence_of(X111,tptp1)
& ~ occurrence_of(X111,tptp2) )
| ~ root_occ(X110,X109)
| ~ occurrence_of(X110,tptp3) )
& occurrence_of(X109,tptp0) ),
inference(fof_nnf,[status(thm)],[goals_neg]) ).
fof(sk_goals_neg_sk,plain,
( ! [X110,X111] :
( ~ leaf_occ(X111,sK6)
| ~ min_precedes(X110,X111,tptp0)
| ( ~ occurrence_of(X111,tptp1)
& ~ occurrence_of(X111,tptp2) )
| ~ root_occ(X110,sK6)
| ~ occurrence_of(X110,tptp3) )
& occurrence_of(sK6,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(X109,sK6)],[nnf_37]) ).
fof(sk_goals_neg,plain,
( ! [VAR_0,VAR_1] :
( ~ leaf_occ(VAR_1,sK6)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp1)
| ~ root_occ(VAR_0,sK6)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( ~ leaf_occ(VAR_1,sK6)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp2)
| ~ root_occ(VAR_0,sK6)
| ~ occurrence_of(VAR_0,tptp3) )
& occurrence_of(sK6,tptp0) ),
inference(cnf_transformation,[status(thm)],[sk_goals_neg_sk]) ).
cnf(c_167,negated_conjecture,
( ~ leaf_occ(B,sK6)
| ~ min_precedes(A,B,tptp0)
| ~ occurrence_of(B,tptp1)
| ~ root_occ(A,sK6)
| ~ occurrence_of(A,tptp3) ),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_168,negated_conjecture,
( ~ leaf_occ(B,sK6)
| ~ min_precedes(A,B,tptp0)
| ~ occurrence_of(B,tptp2)
| ~ root_occ(A,sK6)
| ~ occurrence_of(A,tptp3) ),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_169,negated_conjecture,
occurrence_of(sK6,tptp0),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_181,plain,
( leaf_occ(sK5(A),A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_35]) ).
cnf(c_182,plain,
( occurrence_of(sK5(A),tptp1)
| occurrence_of(sK5(A),tptp2)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_35]) ).
cnf(c_184,plain,
( root_occ(sK7(A),A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_35]) ).
cnf(c_185,plain,
( occurrence_of(sK7(A),tptp3)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_35]) ).
cnf(c_186,plain,
( subactivity_occurrence(A,B)
| ~ leaf_occ(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_34]) ).
cnf(c_187,plain,
( occurrence_of(B,sK2(A,B))
| ~ leaf_occ(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_34]) ).
cnf(c_188,plain,
( subactivity_occurrence(A,B)
| ~ root_occ(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_33]) ).
cnf(c_189,plain,
( occurrence_of(B,sK1(A,B))
| ~ root_occ(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_33]) ).
cnf(c_192,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_28]) ).
cnf(c_204,plain,
( arboreal(A)
| ~ legal(A) ),
inference(clausify,[status(thm)],[sos_08]) ).
cnf(c_210,plain,
( C = B
| ~ occurrence_of(A,C)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_02]) ).
cnf(c_218,plain,
( ~ min_precedes(B,A,C)
| legal(A) ),
inference(resolve,[status(thm)],[c_64,c_60]) ).
cnf(c_237,plain,
( ~ min_precedes(D,B,C)
| min_precedes(sK0(B,C),B,C)
| min_precedes(B,sK3(B,C),C)
| ~ min_precedes(A,B,C) ),
inference(resolve,[status(thm)],[c_96,c_92]) ).
cnf(c_239,plain,
( ~ leaf_occ(A,C)
| ~ min_precedes(A,B,sK2(A,C)) ),
inference(resolve,[status(thm)],[c_97,c_95]) ).
cnf(c_270,plain,
( min_precedes(sK0(B,C),B,C)
| min_precedes(B,sK3(B,C),C)
| ~ min_precedes(A,B,C) ),
inference(factor,[status(thm)],[c_237]) ).
cnf(c_281,plain,
min_precedes(sK4(sK6),sK5(sK6),tptp0),
inference(resolve,[status(thm)],[c_169,c_104]) ).
cnf(c_282,plain,
leaf_occ(sK5(sK6),sK6),
inference(resolve,[status(thm)],[c_181,c_169]) ).
cnf(c_283,plain,
( occurrence_of(sK5(sK6),tptp1)
| occurrence_of(sK5(sK6),tptp2) ),
inference(resolve,[status(thm)],[c_182,c_169]) ).
cnf(c_285,plain,
root_occ(sK7(sK6),sK6),
inference(resolve,[status(thm)],[c_184,c_169]) ).
cnf(c_286,plain,
occurrence_of(sK7(sK6),tptp3),
inference(resolve,[status(thm)],[c_185,c_169]) ).
cnf(c_806,negated_conjecture,
( A = tptp0
| ~ occurrence_of(sK6,A) ),
inference(resolve,[status(thm)],[c_210,c_169]) ).
cnf(c_289,negated_conjecture,
( tptp0 = A
| ~ occurrence_of(sK6,A) ),
inference(copy,[status(thm)],[c_806]) ).
cnf(c_320,plain,
occurrence_of(sK6,sK2(sK5(sK6),sK6)),
inference(resolve,[status(thm)],[c_282,c_187]) ).
cnf(c_321,plain,
subactivity_occurrence(sK5(sK6),sK6),
inference(resolve,[status(thm)],[c_282,c_186]) ).
cnf(c_330,plain,
occurrence_of(sK6,sK1(sK7(sK6),sK6)),
inference(resolve,[status(thm)],[c_285,c_189]) ).
cnf(c_331,plain,
subactivity_occurrence(sK7(sK6),sK6),
inference(resolve,[status(thm)],[c_285,c_188]) ).
cnf(c_334,plain,
legal(sK7(sK6)),
inference(resolve,[status(thm)],[c_285,c_127]) ).
cnf(c_360,plain,
arboreal(sK7(sK6)),
inference(resolve,[status(thm)],[c_334,c_204]) ).
cnf(c_514,plain,
( min_precedes(sK0(sK5(sK6),tptp0),sK5(sK6),tptp0)
| min_precedes(sK5(sK6),sK3(sK5(sK6),tptp0),tptp0) ),
inference(resolve,[status(thm)],[c_281,c_270]) ).
cnf(c_523,plain,
legal(sK5(sK6)),
inference(resolve,[status(thm)],[c_281,c_218]) ).
cnf(c_565,plain,
arboreal(sK5(sK6)),
inference(resolve,[status(thm)],[c_523,c_204]) ).
cnf(c_807,negated_conjecture,
( B = A
| min_precedes(B,A,tptp0)
| min_precedes(A,B,tptp0)
| ~ subactivity_occurrence(B,sK6)
| ~ subactivity_occurrence(A,sK6)
| ~ arboreal(B)
| ~ arboreal(A) ),
inference(resolve,[status(thm)],[c_192,c_169]) ).
cnf(c_808,negated_conjecture,
( A = sK7(sK6)
| min_precedes(A,sK7(sK6),tptp0)
| min_precedes(sK7(sK6),A,tptp0)
| ~ subactivity_occurrence(A,sK6)
| ~ subactivity_occurrence(sK7(sK6),sK6)
| ~ arboreal(A) ),
inference(resolve,[status(thm)],[c_807,c_360]) ).
cnf(c_809,negated_conjecture,
( sK5(sK6) = sK7(sK6)
| min_precedes(sK5(sK6),sK7(sK6),tptp0)
| min_precedes(sK7(sK6),sK5(sK6),tptp0)
| ~ subactivity_occurrence(sK5(sK6),sK6)
| ~ subactivity_occurrence(sK7(sK6),sK6) ),
inference(resolve,[status(thm)],[c_808,c_565]) ).
cnf(c_810,negated_conjecture,
( sK5(sK6) = sK7(sK6)
| min_precedes(sK5(sK6),sK7(sK6),tptp0)
| min_precedes(sK7(sK6),sK5(sK6),tptp0)
| ~ subactivity_occurrence(sK5(sK6),sK6) ),
inference(resolve,[status(thm)],[c_809,c_331]) ).
cnf(c_567,negated_conjecture,
( sK5(sK6) = sK7(sK6)
| min_precedes(sK5(sK6),sK7(sK6),tptp0)
| min_precedes(sK7(sK6),sK5(sK6),tptp0) ),
inference(resolve,[status(thm)],[c_810,c_321]) ).
cnf(c_811,plain,
tptp0 = sK2(sK5(sK6),sK6),
inference(resolve,[status(thm)],[c_320,c_289]) ).
cnf(c_620,plain,
sK2(sK5(sK6),sK6) = tptp0,
inference(copy,[status(thm)],[c_811]) ).
cnf(c_812,plain,
tptp0 = sK1(sK7(sK6),sK6),
inference(resolve,[status(thm)],[c_330,c_289]) ).
cnf(c_637,plain,
sK1(sK7(sK6),sK6) = tptp0,
inference(copy,[status(thm)],[c_812]) ).
cnf(c_813,plain,
( ~ leaf_occ(sK5(sK6),sK6)
| ~ min_precedes(sK5(sK6),A,tptp0) ),
inference(paramod,[status(thm)],[c_620,c_239]) ).
cnf(c_672,plain,
~ min_precedes(sK5(sK6),A,tptp0),
inference(resolve,[status(thm)],[c_282,c_813]) ).
cnf(c_674,negated_conjecture,
( sK5(sK6) = sK7(sK6)
| min_precedes(sK7(sK6),sK5(sK6),tptp0) ),
inference(resolve,[status(thm)],[c_672,c_567]) ).
cnf(c_677,plain,
min_precedes(sK0(sK5(sK6),tptp0),sK5(sK6),tptp0),
inference(resolve,[status(thm)],[c_672,c_514]) ).
cnf(c_814,plain,
( ~ min_precedes(A,sK7(sK6),tptp0)
| ~ root_occ(sK7(sK6),sK6) ),
inference(paramod,[status(thm)],[c_637,c_126]) ).
cnf(c_678,plain,
~ min_precedes(A,sK7(sK6),tptp0),
inference(resolve,[status(thm)],[c_285,c_814]) ).
cnf(c_815,negated_conjecture,
( ~ leaf_occ(sK5(sK6),sK6)
| ~ occurrence_of(sK5(sK6),tptp1)
| ~ root_occ(sK7(sK6),sK6)
| ~ occurrence_of(sK7(sK6),tptp3)
| sK5(sK6) = sK7(sK6) ),
inference(resolve,[status(thm)],[c_674,c_167]) ).
cnf(c_816,negated_conjecture,
( ~ leaf_occ(sK5(sK6),sK6)
| ~ occurrence_of(sK5(sK6),tptp1)
| ~ root_occ(sK7(sK6),sK6)
| sK5(sK6) = sK7(sK6) ),
inference(resolve,[status(thm)],[c_286,c_815]) ).
cnf(c_817,negated_conjecture,
( ~ leaf_occ(sK5(sK6),sK6)
| ~ occurrence_of(sK5(sK6),tptp1)
| sK5(sK6) = sK7(sK6) ),
inference(resolve,[status(thm)],[c_285,c_816]) ).
cnf(c_787,negated_conjecture,
( ~ occurrence_of(sK5(sK6),tptp1)
| sK5(sK6) = sK7(sK6) ),
inference(resolve,[status(thm)],[c_282,c_817]) ).
cnf(c_818,negated_conjecture,
( ~ leaf_occ(A,sK6)
| ~ min_precedes(sK7(sK6),A,tptp0)
| ~ occurrence_of(A,tptp2)
| ~ root_occ(sK7(sK6),sK6) ),
inference(resolve,[status(thm)],[c_168,c_286]) ).
cnf(c_819,negated_conjecture,
( ~ leaf_occ(A,sK6)
| ~ min_precedes(sK7(sK6),A,tptp0)
| ~ occurrence_of(A,tptp2) ),
inference(resolve,[status(thm)],[c_818,c_285]) ).
cnf(c_820,negated_conjecture,
( occurrence_of(sK5(sK6),tptp1)
| ~ leaf_occ(sK5(sK6),sK6)
| ~ min_precedes(sK7(sK6),sK5(sK6),tptp0) ),
inference(resolve,[status(thm)],[c_819,c_283]) ).
cnf(c_821,negated_conjecture,
( sK5(sK6) = sK7(sK6)
| occurrence_of(sK5(sK6),tptp1)
| ~ leaf_occ(sK5(sK6),sK6) ),
inference(resolve,[status(thm)],[c_820,c_674]) ).
cnf(c_801,negated_conjecture,
( sK5(sK6) = sK7(sK6)
| occurrence_of(sK5(sK6),tptp1) ),
inference(resolve,[status(thm)],[c_821,c_282]) ).
cnf(c_822,plain,
( sK5(sK6) = sK7(sK6)
| sK5(sK6) = sK7(sK6) ),
inference(resolve,[status(thm)],[c_801,c_787]) ).
cnf(c_804,plain,
sK5(sK6) = sK7(sK6),
inference(copy,[status(thm)],[c_822]) ).
cnf(c_823,plain,
min_precedes(sK0(sK7(sK6),tptp0),sK5(sK6),tptp0),
inference(paramod,[status(thm)],[c_804,c_677]) ).
cnf(c_824,plain,
min_precedes(sK0(sK7(sK6),tptp0),sK7(sK6),tptp0),
inference(paramod,[status(thm)],[c_804,c_823]) ).
cnf(c_805,plain,
$false,
inference(resolve,[status(thm)],[c_678,c_824]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO009+1 : 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/0.35 % Computer : n010.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sat Sep 26 04:58:29 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.35 % Process 2521327 was started by sandbox2 on n010,
% 0.10/0.35 % Sat Sep 26 04:58:29 2026
% 0.10/0.35 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.37
% 0.10/0.37 % From the command line: assign(max_seconds, 300).
% 1.59/0.61
% 1.59/0.61 % SZS status Theorem for theBenchmark
% 1.59/0.61
% 1.59/0.61 % Proof 1 at 0.20 (+ 0.03) seconds.
% 1.59/0.61 % Length of proof is 72.
% 1.59/0.61 % Level of proof is 10.
% 1.59/0.61 % Maximum clause weight is 31.000.
% 1.59/0.61 % Given clauses 264.
% 1.59/0.61
% 1.59/0.61 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------