%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PRO014+4 : 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 : n008.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:58 AM UTC 2026
% Result : Theorem 0.23s 6.00s
% Output : CNFRefutation 0.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 15
% Syntax : Number of formulae : 147 ( 44 unt; 0 def)
% Number of atoms : 469 ( 23 equ)
% Maximal formula atoms : 36 ( 3 avg)
% Number of connectives : 517 ( 195 ~; 232 |; 75 &)
% ( 4 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 7 con; 0-2 aty)
% Number of variables : 165 ( 6 sgn 71 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(sos_02,axiom,
! [X8,X9,X10,X11] :
( ( ~ min_precedes(X10,X11,X8)
& arboreal(X10)
& leaf_occ(X11,X9)
& subactivity_occurrence(X10,X9)
& occurrence_of(X9,X8) )
=> X11 = X10 ),
file('theBenchmark.p',sos_02) ).
fof(sos_07,axiom,
! [X25,X26] :
( ( ~ atomic(X26)
& leaf(X25,X26) )
=> ? [X27] :
( leaf_occ(X25,X27)
& occurrence_of(X27,X26) ) ),
file('theBenchmark.p',sos_07) ).
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_20,axiom,
! [X61,X62] :
( earlier(X61,X62)
=> ~ earlier(X62,X61) ),
file('theBenchmark.p',sos_20) ).
fof(sos_21,axiom,
! [X63,X64] :
( precedes(X63,X64)
<=> ( legal(X64)
& earlier(X63,X64) ) ),
file('theBenchmark.p',sos_21) ).
fof(sos_24,axiom,
! [X72,X73,X74] :
( min_precedes(X72,X73,X74)
=> precedes(X72,X73) ),
file('theBenchmark.p',sos_24) ).
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_30,axiom,
! [X94,X95,X96] :
( ( earlier(X95,X96)
& earlier(X94,X95) )
=> earlier(X94,X96) ),
file('theBenchmark.p',sos_30) ).
fof(sos_31,axiom,
! [X97,X98,X99,X100] :
( ( precedes(X98,X99)
& min_precedes(X97,X99,X100)
& min_precedes(X97,X98,X100) )
=> min_precedes(X98,X99,X100) ),
file('theBenchmark.p',sos_31) ).
fof(sos_32,axiom,
! [X101,X102] :
( ( ~ leaf_occ(X101,X102)
& arboreal(X101)
& subactivity_occurrence(X101,X102)
& occurrence_of(X102,tptp0) )
=> ? [X103,X104,X105] :
( leaf(X105,tptp0)
& next_subocc(X104,X105,tptp0)
& ( occurrence_of(X105,tptp1)
| occurrence_of(X105,tptp2) )
& 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] :
( leaf(X109,tptp0)
& min_precedes(X108,X109,tptp0)
& ( occurrence_of(X109,tptp1)
| occurrence_of(X109,tptp2) )
& 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] :
( leaf(X109,tptp0)
& min_precedes(X108,X109,tptp0)
& ( occurrence_of(X109,tptp1)
| occurrence_of(X109,tptp2) )
& next_subocc(X106,X108,tptp0)
& occurrence_of(X108,tptp3) ) ),
inference(assume_negation,[status(cth)],[goals]) ).
cnf(c_55,plain,
( legal(B)
| ~ precedes(A,B) ),
inference(clausify,[status(thm)],[sos_21]) ).
cnf(c_57,plain,
( ~ legal(B)
| ~ earlier(A,B)
| precedes(A,B) ),
inference(clausify,[status(thm)],[sos_21]) ).
cnf(c_70,plain,
( ~ precedes(C,B)
| ~ earlier(A,B)
| precedes(A,B) ),
inference(resolve,[status(thm)],[c_57,c_55]) ).
fof(nnf_34,plain,
? [X106,X107] :
( ! [X108,X109] :
( ~ leaf(X109,tptp0)
| ~ min_precedes(X108,X109,tptp0)
| ( ~ occurrence_of(X109,tptp1)
& ~ occurrence_of(X109,tptp2) )
| ~ 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] :
( ~ leaf(X109,tptp0)
| ~ min_precedes(X108,X109,tptp0)
| ( ~ occurrence_of(X109,tptp1)
& ~ occurrence_of(X109,tptp2) )
| ~ next_subocc(sK0,X108,tptp0)
| ~ occurrence_of(X108,tptp3) )
& ~ leaf_occ(sK0,sK1)
& arboreal(sK0)
& subactivity_occurrence(sK0,sK1)
& occurrence_of(sK1,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK0]),skolemize(X106,sK0),skolemize(X107,sK1)],[nnf_34]) ).
fof(sk_goals_neg,plain,
( ! [VAR_0,VAR_1] :
( ~ leaf(VAR_1,tptp0)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp1)
| ~ next_subocc(sK0,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( ~ leaf(VAR_1,tptp0)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp2)
| ~ next_subocc(sK0,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ~ leaf_occ(sK0,sK1)
& arboreal(sK0)
& subactivity_occurrence(sK0,sK1)
& occurrence_of(sK1,tptp0) ),
inference(cnf_transformation,[status(thm)],[sk_goals_neg_sk]) ).
cnf(c_90,negated_conjecture,
( ~ leaf(B,tptp0)
| ~ min_precedes(A,B,tptp0)
| ~ occurrence_of(B,tptp1)
| ~ next_subocc(sK0,A,tptp0)
| ~ occurrence_of(A,tptp3) ),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_91,negated_conjecture,
( ~ leaf(B,tptp0)
| ~ min_precedes(A,B,tptp0)
| ~ occurrence_of(B,tptp2)
| ~ next_subocc(sK0,A,tptp0)
| ~ occurrence_of(A,tptp3) ),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_92,negated_conjecture,
~ leaf_occ(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_93,negated_conjecture,
arboreal(sK0),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_94,negated_conjecture,
subactivity_occurrence(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_95,negated_conjecture,
occurrence_of(sK1,tptp0),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
fof(sos_38,axiom,
atomic(tptp3),
file('theBenchmark.p',sos_38) ).
cnf(c_102,plain,
atomic(tptp3),
inference(clausify,[status(thm)],[sos_38]) ).
fof(sos_34,axiom,
~ atomic(tptp0),
file('theBenchmark.p',sos_34) ).
cnf(c_106,plain,
~ atomic(tptp0),
inference(clausify,[status(thm)],[sos_34]) ).
fof(nnf_33,plain,
! [X101,X102] :
( ? [X103,X104,X105] :
( leaf(X105,tptp0)
& next_subocc(X104,X105,tptp0)
& ( occurrence_of(X105,tptp1)
| occurrence_of(X105,tptp2) )
& 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(sK2(X101,X102),tptp0)
& next_subocc(sK3(X101,X102),sK2(X101,X102),tptp0)
& ( occurrence_of(sK2(X101,X102),tptp1)
| occurrence_of(sK2(X101,X102),tptp2) )
& next_subocc(sK4(X101,X102),sK3(X101,X102),tptp0)
& occurrence_of(sK3(X101,X102),tptp4)
& next_subocc(X101,sK4(X101,X102),tptp0)
& occurrence_of(sK4(X101,X102),tptp3) )
| leaf_occ(X101,X102)
| ~ arboreal(X101)
| ~ subactivity_occurrence(X101,X102)
| ~ occurrence_of(X102,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK3,sK2]),skolemize(X103,sK4(X101,X102)),skolemize(X104,sK3(X101,X102)),skolemize(X105,sK2(X101,X102))],[nnf_33]) ).
fof(sk_sos_32,plain,
( ! [VAR_0,VAR_1] :
( leaf(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] :
( next_subocc(sK3(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),tptp1)
| occurrence_of(sK2(VAR_1,VAR_0),tptp2)
| 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(sK4(VAR_1,VAR_0),sK3(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(sK3(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,sK4(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(sK4(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_107,plain,
( leaf(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_108,plain,
( next_subocc(sK3(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_109,plain,
( occurrence_of(sK2(B,A),tptp1)
| occurrence_of(sK2(B,A),tptp2)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
cnf(c_110,plain,
( next_subocc(sK4(B,A),sK3(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_112,plain,
( next_subocc(B,sK4(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_113,plain,
( occurrence_of(sK4(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_114,plain,
( min_precedes(B,D,C)
| ~ precedes(B,D)
| ~ min_precedes(A,D,C)
| ~ min_precedes(A,B,C) ),
inference(clausify,[status(thm)],[sos_31]) ).
cnf(c_115,plain,
( earlier(A,C)
| ~ earlier(B,C)
| ~ earlier(A,B) ),
inference(clausify,[status(thm)],[sos_30]) ).
cnf(c_118,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_122,plain,
( min_precedes(A,B,C)
| ~ next_subocc(A,B,C) ),
inference(clausify,[status(thm)],[sos_26]) ).
cnf(c_125,plain,
( precedes(A,B)
| ~ min_precedes(A,B,C) ),
inference(clausify,[status(thm)],[sos_24]) ).
cnf(c_127,plain,
( earlier(A,B)
| ~ precedes(A,B) ),
inference(clausify,[status(thm)],[sos_21]) ).
cnf(c_128,plain,
( ~ earlier(B,A)
| ~ earlier(A,B) ),
inference(clausify,[status(thm)],[sos_20]) ).
cnf(c_133,plain,
( subactivity_occurrence(A,B)
| ~ leaf_occ(A,B) ),
inference(clausify,[status(thm)],[sos_18]) ).
cnf(c_135,plain,
( ~ atomic(B)
| arboreal(A)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_16]) ).
fof(nnf_8,plain,
! [X25,X26] :
( ? [X27] :
( leaf_occ(X25,X27)
& occurrence_of(X27,X26) )
| atomic(X26)
| ~ leaf(X25,X26) ),
inference(fof_nnf,[status(thm)],[sos_07]) ).
fof(sk_sos_07_sk,plain,
! [X25,X26] :
( ( leaf_occ(X25,sK5(X25,X26))
& occurrence_of(sK5(X25,X26),X26) )
| atomic(X26)
| ~ leaf(X25,X26) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X27,sK5(X25,X26))],[nnf_8]) ).
fof(sk_sos_07,plain,
( ! [VAR_0,VAR_1] :
( leaf_occ(VAR_0,sK5(VAR_0,VAR_1))
| atomic(VAR_1)
| ~ leaf(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( occurrence_of(sK5(VAR_0,VAR_1),VAR_1)
| atomic(VAR_1)
| ~ leaf(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_07_sk]) ).
cnf(c_144,plain,
( leaf_occ(A,sK5(A,B))
| atomic(B)
| ~ leaf(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_07]) ).
cnf(c_145,plain,
( occurrence_of(sK5(A,B),B)
| atomic(B)
| ~ leaf(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_07]) ).
cnf(c_150,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_02]) ).
cnf(c_160,plain,
~ earlier(A,A),
inference(factor,[status(thm)],[c_128]) ).
cnf(c_764,negated_conjecture,
( leaf(sK2(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0)
| ~ occurrence_of(sK1,tptp0) ),
inference(resolve,[status(thm)],[c_107,c_94]) ).
cnf(c_765,negated_conjecture,
( leaf(sK2(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0) ),
inference(resolve,[status(thm)],[c_95,c_764]) ).
cnf(c_766,negated_conjecture,
( leaf(sK2(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1) ),
inference(resolve,[status(thm)],[c_93,c_765]) ).
cnf(c_167,negated_conjecture,
leaf(sK2(sK0,sK1),tptp0),
inference(resolve,[status(thm)],[c_92,c_766]) ).
cnf(c_767,negated_conjecture,
( next_subocc(sK3(sK0,sK1),sK2(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0)
| ~ occurrence_of(sK1,tptp0) ),
inference(resolve,[status(thm)],[c_108,c_94]) ).
cnf(c_768,negated_conjecture,
( next_subocc(sK3(sK0,sK1),sK2(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0) ),
inference(resolve,[status(thm)],[c_95,c_767]) ).
cnf(c_769,negated_conjecture,
( next_subocc(sK3(sK0,sK1),sK2(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1) ),
inference(resolve,[status(thm)],[c_93,c_768]) ).
cnf(c_168,negated_conjecture,
next_subocc(sK3(sK0,sK1),sK2(sK0,sK1),tptp0),
inference(resolve,[status(thm)],[c_92,c_769]) ).
cnf(c_770,negated_conjecture,
( occurrence_of(sK2(sK0,sK1),tptp1)
| occurrence_of(sK2(sK0,sK1),tptp2)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0)
| ~ occurrence_of(sK1,tptp0) ),
inference(resolve,[status(thm)],[c_109,c_94]) ).
cnf(c_771,negated_conjecture,
( occurrence_of(sK2(sK0,sK1),tptp1)
| occurrence_of(sK2(sK0,sK1),tptp2)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0) ),
inference(resolve,[status(thm)],[c_95,c_770]) ).
cnf(c_772,negated_conjecture,
( occurrence_of(sK2(sK0,sK1),tptp1)
| occurrence_of(sK2(sK0,sK1),tptp2)
| leaf_occ(sK0,sK1) ),
inference(resolve,[status(thm)],[c_93,c_771]) ).
cnf(c_169,negated_conjecture,
( occurrence_of(sK2(sK0,sK1),tptp1)
| occurrence_of(sK2(sK0,sK1),tptp2) ),
inference(resolve,[status(thm)],[c_92,c_772]) ).
cnf(c_773,negated_conjecture,
( next_subocc(sK4(sK0,sK1),sK3(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0)
| ~ occurrence_of(sK1,tptp0) ),
inference(resolve,[status(thm)],[c_110,c_94]) ).
cnf(c_774,negated_conjecture,
( next_subocc(sK4(sK0,sK1),sK3(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0) ),
inference(resolve,[status(thm)],[c_95,c_773]) ).
cnf(c_775,negated_conjecture,
( next_subocc(sK4(sK0,sK1),sK3(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1) ),
inference(resolve,[status(thm)],[c_93,c_774]) ).
cnf(c_170,negated_conjecture,
next_subocc(sK4(sK0,sK1),sK3(sK0,sK1),tptp0),
inference(resolve,[status(thm)],[c_92,c_775]) ).
cnf(c_776,negated_conjecture,
( next_subocc(sK0,sK4(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0)
| ~ occurrence_of(sK1,tptp0) ),
inference(resolve,[status(thm)],[c_112,c_94]) ).
cnf(c_777,negated_conjecture,
( next_subocc(sK0,sK4(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0) ),
inference(resolve,[status(thm)],[c_95,c_776]) ).
cnf(c_778,negated_conjecture,
( next_subocc(sK0,sK4(sK0,sK1),tptp0)
| leaf_occ(sK0,sK1) ),
inference(resolve,[status(thm)],[c_93,c_777]) ).
cnf(c_172,negated_conjecture,
next_subocc(sK0,sK4(sK0,sK1),tptp0),
inference(resolve,[status(thm)],[c_92,c_778]) ).
cnf(c_779,negated_conjecture,
( occurrence_of(sK4(sK0,sK1),tptp3)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0)
| ~ occurrence_of(sK1,tptp0) ),
inference(resolve,[status(thm)],[c_113,c_94]) ).
cnf(c_780,negated_conjecture,
( occurrence_of(sK4(sK0,sK1),tptp3)
| leaf_occ(sK0,sK1)
| ~ arboreal(sK0) ),
inference(resolve,[status(thm)],[c_95,c_779]) ).
cnf(c_781,negated_conjecture,
( occurrence_of(sK4(sK0,sK1),tptp3)
| leaf_occ(sK0,sK1) ),
inference(resolve,[status(thm)],[c_93,c_780]) ).
cnf(c_173,negated_conjecture,
occurrence_of(sK4(sK0,sK1),tptp3),
inference(resolve,[status(thm)],[c_92,c_781]) ).
cnf(c_180,plain,
~ precedes(A,A),
inference(resolve,[status(thm)],[c_127,c_160]) ).
cnf(c_782,plain,
( occurrence_of(sK5(sK2(sK0,sK1),tptp0),tptp0)
| atomic(tptp0) ),
inference(resolve,[status(thm)],[c_167,c_145]) ).
cnf(c_208,plain,
occurrence_of(sK5(sK2(sK0,sK1),tptp0),tptp0),
inference(resolve,[status(thm)],[c_106,c_782]) ).
cnf(c_783,plain,
( leaf_occ(sK2(sK0,sK1),sK5(sK2(sK0,sK1),tptp0))
| atomic(tptp0) ),
inference(resolve,[status(thm)],[c_167,c_144]) ).
cnf(c_209,plain,
leaf_occ(sK2(sK0,sK1),sK5(sK2(sK0,sK1),tptp0)),
inference(resolve,[status(thm)],[c_106,c_783]) ).
cnf(c_784,plain,
( ~ atomic(tptp3)
| arboreal(sK4(sK0,sK1)) ),
inference(resolve,[status(thm)],[c_173,c_135]) ).
cnf(c_246,plain,
arboreal(sK4(sK0,sK1)),
inference(resolve,[status(thm)],[c_102,c_784]) ).
cnf(c_271,plain,
min_precedes(sK0,sK4(sK0,sK1),tptp0),
inference(resolve,[status(thm)],[c_172,c_122]) ).
cnf(c_785,negated_conjecture,
( ~ leaf(A,tptp0)
| ~ min_precedes(sK4(sK0,sK1),A,tptp0)
| ~ occurrence_of(A,tptp2)
| ~ occurrence_of(sK4(sK0,sK1),tptp3) ),
inference(resolve,[status(thm)],[c_172,c_91]) ).
cnf(c_273,negated_conjecture,
( ~ leaf(A,tptp0)
| ~ min_precedes(sK4(sK0,sK1),A,tptp0)
| ~ occurrence_of(A,tptp2) ),
inference(resolve,[status(thm)],[c_173,c_785]) ).
cnf(c_786,negated_conjecture,
( ~ leaf(A,tptp0)
| ~ min_precedes(sK4(sK0,sK1),A,tptp0)
| ~ occurrence_of(A,tptp1)
| ~ occurrence_of(sK4(sK0,sK1),tptp3) ),
inference(resolve,[status(thm)],[c_172,c_90]) ).
cnf(c_274,negated_conjecture,
( ~ leaf(A,tptp0)
| ~ min_precedes(sK4(sK0,sK1),A,tptp0)
| ~ occurrence_of(A,tptp1) ),
inference(resolve,[status(thm)],[c_173,c_786]) ).
cnf(c_283,plain,
precedes(sK0,sK4(sK0,sK1)),
inference(resolve,[status(thm)],[c_271,c_125]) ).
cnf(c_284,plain,
( subactivity_occurrence(sK0,A)
| ~ subactivity_occurrence(sK4(sK0,sK1),A)
| ~ occurrence_of(A,tptp0) ),
inference(resolve,[status(thm)],[c_271,c_118]) ).
cnf(c_295,plain,
earlier(sK0,sK4(sK0,sK1)),
inference(resolve,[status(thm)],[c_283,c_127]) ).
cnf(c_296,plain,
~ earlier(sK4(sK0,sK1),sK0),
inference(resolve,[status(thm)],[c_295,c_128]) ).
cnf(c_298,plain,
( earlier(sK0,A)
| ~ earlier(sK4(sK0,sK1),A) ),
inference(resolve,[status(thm)],[c_295,c_115]) ).
cnf(c_300,plain,
min_precedes(sK3(sK0,sK1),sK2(sK0,sK1),tptp0),
inference(resolve,[status(thm)],[c_168,c_122]) ).
cnf(c_303,plain,
min_precedes(sK4(sK0,sK1),sK3(sK0,sK1),tptp0),
inference(resolve,[status(thm)],[c_170,c_122]) ).
cnf(c_305,plain,
~ precedes(sK4(sK0,sK1),sK0),
inference(resolve,[status(thm)],[c_127,c_296]) ).
cnf(c_308,plain,
~ min_precedes(sK4(sK0,sK1),sK0,A),
inference(resolve,[status(thm)],[c_125,c_305]) ).
cnf(c_318,plain,
precedes(sK3(sK0,sK1),sK2(sK0,sK1)),
inference(resolve,[status(thm)],[c_300,c_125]) ).
cnf(c_319,plain,
( subactivity_occurrence(sK3(sK0,sK1),A)
| ~ subactivity_occurrence(sK2(sK0,sK1),A)
| ~ occurrence_of(A,tptp0) ),
inference(resolve,[status(thm)],[c_300,c_118]) ).
cnf(c_333,plain,
earlier(sK3(sK0,sK1),sK2(sK0,sK1)),
inference(resolve,[status(thm)],[c_318,c_127]) ).
cnf(c_345,plain,
precedes(sK4(sK0,sK1),sK3(sK0,sK1)),
inference(resolve,[status(thm)],[c_303,c_125]) ).
cnf(c_346,plain,
( subactivity_occurrence(sK4(sK0,sK1),A)
| ~ subactivity_occurrence(sK3(sK0,sK1),A)
| ~ occurrence_of(A,tptp0) ),
inference(resolve,[status(thm)],[c_303,c_118]) ).
cnf(c_360,plain,
earlier(sK4(sK0,sK1),sK3(sK0,sK1)),
inference(resolve,[status(thm)],[c_345,c_127]) ).
cnf(c_364,plain,
earlier(sK0,sK3(sK0,sK1)),
inference(resolve,[status(thm)],[c_360,c_298]) ).
cnf(c_787,plain,
( earlier(sK4(sK0,sK1),A)
| ~ earlier(sK3(sK0,sK1),A) ),
inference(resolve,[status(thm)],[c_115,c_360]) ).
cnf(c_368,plain,
earlier(sK4(sK0,sK1),sK2(sK0,sK1)),
inference(resolve,[status(thm)],[c_787,c_333]) ).
cnf(c_788,plain,
( earlier(sK0,A)
| ~ earlier(sK3(sK0,sK1),A) ),
inference(resolve,[status(thm)],[c_115,c_364]) ).
cnf(c_376,plain,
earlier(sK0,sK2(sK0,sK1)),
inference(resolve,[status(thm)],[c_788,c_333]) ).
cnf(c_789,plain,
( ~ precedes(A,sK2(sK0,sK1))
| precedes(sK0,sK2(sK0,sK1)) ),
inference(resolve,[status(thm)],[c_70,c_376]) ).
cnf(c_384,plain,
precedes(sK0,sK2(sK0,sK1)),
inference(resolve,[status(thm)],[c_789,c_318]) ).
cnf(c_790,plain,
( ~ precedes(A,sK2(sK0,sK1))
| precedes(sK4(sK0,sK1),sK2(sK0,sK1)) ),
inference(resolve,[status(thm)],[c_70,c_368]) ).
cnf(c_397,plain,
precedes(sK4(sK0,sK1),sK2(sK0,sK1)),
inference(resolve,[status(thm)],[c_790,c_384]) ).
cnf(c_420,plain,
subactivity_occurrence(sK2(sK0,sK1),sK5(sK2(sK0,sK1),tptp0)),
inference(resolve,[status(thm)],[c_209,c_133]) ).
cnf(c_791,plain,
( subactivity_occurrence(sK3(sK0,sK1),sK5(sK2(sK0,sK1),tptp0))
| ~ occurrence_of(sK5(sK2(sK0,sK1),tptp0),tptp0) ),
inference(resolve,[status(thm)],[c_420,c_319]) ).
cnf(c_599,plain,
subactivity_occurrence(sK3(sK0,sK1),sK5(sK2(sK0,sK1),tptp0)),
inference(resolve,[status(thm)],[c_208,c_791]) ).
cnf(c_792,plain,
( subactivity_occurrence(sK4(sK0,sK1),sK5(sK2(sK0,sK1),tptp0))
| ~ occurrence_of(sK5(sK2(sK0,sK1),tptp0),tptp0) ),
inference(resolve,[status(thm)],[c_599,c_346]) ).
cnf(c_626,plain,
subactivity_occurrence(sK4(sK0,sK1),sK5(sK2(sK0,sK1),tptp0)),
inference(resolve,[status(thm)],[c_208,c_792]) ).
cnf(c_793,plain,
( subactivity_occurrence(sK0,sK5(sK2(sK0,sK1),tptp0))
| ~ occurrence_of(sK5(sK2(sK0,sK1),tptp0),tptp0) ),
inference(resolve,[status(thm)],[c_626,c_284]) ).
cnf(c_635,plain,
subactivity_occurrence(sK0,sK5(sK2(sK0,sK1),tptp0)),
inference(resolve,[status(thm)],[c_208,c_793]) ).
cnf(c_794,plain,
( B = A
| min_precedes(A,B,tptp0)
| ~ arboreal(A)
| ~ leaf_occ(B,sK5(sK2(sK0,sK1),tptp0))
| ~ subactivity_occurrence(A,sK5(sK2(sK0,sK1),tptp0)) ),
inference(resolve,[status(thm)],[c_150,c_208]) ).
cnf(c_795,plain,
( A = sK4(sK0,sK1)
| min_precedes(sK4(sK0,sK1),A,tptp0)
| ~ arboreal(sK4(sK0,sK1))
| ~ leaf_occ(A,sK5(sK2(sK0,sK1),tptp0)) ),
inference(resolve,[status(thm)],[c_794,c_626]) ).
cnf(c_796,plain,
( sK2(sK0,sK1) = sK4(sK0,sK1)
| min_precedes(sK4(sK0,sK1),sK2(sK0,sK1),tptp0)
| ~ arboreal(sK4(sK0,sK1)) ),
inference(resolve,[status(thm)],[c_795,c_209]) ).
cnf(c_644,plain,
( sK2(sK0,sK1) = sK4(sK0,sK1)
| min_precedes(sK4(sK0,sK1),sK2(sK0,sK1),tptp0) ),
inference(resolve,[status(thm)],[c_796,c_246]) ).
cnf(c_797,plain,
( B = A
| min_precedes(A,B,tptp0)
| ~ arboreal(A)
| ~ leaf_occ(B,sK5(sK2(sK0,sK1),tptp0))
| ~ subactivity_occurrence(A,sK5(sK2(sK0,sK1),tptp0)) ),
inference(resolve,[status(thm)],[c_150,c_208]) ).
cnf(c_798,plain,
( A = sK0
| min_precedes(sK0,A,tptp0)
| ~ arboreal(sK0)
| ~ leaf_occ(A,sK5(sK2(sK0,sK1),tptp0)) ),
inference(resolve,[status(thm)],[c_797,c_635]) ).
cnf(c_799,plain,
( sK2(sK0,sK1) = sK0
| min_precedes(sK0,sK2(sK0,sK1),tptp0)
| ~ arboreal(sK0) ),
inference(resolve,[status(thm)],[c_798,c_209]) ).
cnf(c_653,negated_conjecture,
( sK2(sK0,sK1) = sK0
| min_precedes(sK0,sK2(sK0,sK1),tptp0) ),
inference(resolve,[status(thm)],[c_799,c_93]) ).
cnf(c_800,plain,
( min_precedes(sK4(sK0,sK1),A,tptp0)
| ~ precedes(sK4(sK0,sK1),A)
| ~ min_precedes(sK0,A,tptp0) ),
inference(resolve,[status(thm)],[c_114,c_271]) ).
cnf(c_801,plain,
( sK2(sK0,sK1) = sK0
| min_precedes(sK4(sK0,sK1),sK2(sK0,sK1),tptp0)
| ~ precedes(sK4(sK0,sK1),sK2(sK0,sK1)) ),
inference(resolve,[status(thm)],[c_800,c_653]) ).
cnf(c_675,plain,
( sK2(sK0,sK1) = sK0
| min_precedes(sK4(sK0,sK1),sK2(sK0,sK1),tptp0) ),
inference(resolve,[status(thm)],[c_801,c_397]) ).
cnf(c_802,plain,
( ~ leaf(sK2(sK0,sK1),tptp0)
| ~ occurrence_of(sK2(sK0,sK1),tptp1)
| sK2(sK0,sK1) = sK0 ),
inference(resolve,[status(thm)],[c_675,c_274]) ).
cnf(c_691,plain,
( ~ occurrence_of(sK2(sK0,sK1),tptp1)
| sK2(sK0,sK1) = sK0 ),
inference(resolve,[status(thm)],[c_167,c_802]) ).
cnf(c_803,plain,
( occurrence_of(sK2(sK0,sK1),tptp1)
| ~ leaf(sK2(sK0,sK1),tptp0)
| ~ min_precedes(sK4(sK0,sK1),sK2(sK0,sK1),tptp0) ),
inference(resolve,[status(thm)],[c_273,c_169]) ).
cnf(c_804,plain,
( sK2(sK0,sK1) = sK0
| occurrence_of(sK2(sK0,sK1),tptp1)
| ~ leaf(sK2(sK0,sK1),tptp0) ),
inference(resolve,[status(thm)],[c_803,c_675]) ).
cnf(c_707,plain,
( sK2(sK0,sK1) = sK0
| occurrence_of(sK2(sK0,sK1),tptp1) ),
inference(resolve,[status(thm)],[c_804,c_167]) ).
cnf(c_805,plain,
( sK2(sK0,sK1) = sK0
| sK2(sK0,sK1) = sK0 ),
inference(resolve,[status(thm)],[c_707,c_691]) ).
cnf(c_708,plain,
sK2(sK0,sK1) = sK0,
inference(copy,[status(thm)],[c_805]) ).
cnf(c_806,plain,
( sK2(sK0,sK1) = sK4(sK0,sK1)
| min_precedes(sK4(sK0,sK1),sK0,tptp0) ),
inference(paramod,[status(thm)],[c_708,c_644]) ).
cnf(c_807,plain,
( sK0 = sK4(sK0,sK1)
| min_precedes(sK4(sK0,sK1),sK0,tptp0) ),
inference(paramod,[status(thm)],[c_708,c_806]) ).
cnf(c_808,plain,
( sK4(sK0,sK1) = sK0
| min_precedes(sK4(sK0,sK1),sK0,tptp0) ),
inference(copy,[status(thm)],[c_807]) ).
cnf(c_718,plain,
sK4(sK0,sK1) = sK0,
inference(resolve,[status(thm)],[c_308,c_808]) ).
cnf(c_809,plain,
precedes(sK0,sK2(sK0,sK1)),
inference(paramod,[status(thm)],[c_718,c_397]) ).
cnf(c_810,plain,
precedes(sK0,sK0),
inference(paramod,[status(thm)],[c_708,c_809]) ).
cnf(c_763,plain,
$false,
inference(resolve,[status(thm)],[c_180,c_810]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : PRO014+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/5.66 % Computer : n008.cluster.edu
% 0.19/5.66 % Model : x86_64 x86_64
% 0.19/5.66 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/5.66 % Memory : 8046.5625MB
% 0.19/5.66 % OS : Linux 6.8.0-71-generic
% 0.19/5.66 % CPULimit : 300
% 0.19/5.66 % WCLimit : 300
% 0.19/5.66 % DateTime : Sat Sep 26 05:00:32 UTC 2026
% 0.19/5.67 % CPUTime :
% 0.19/5.67 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.19/5.67 % Process 2813143 was started by sandbox2 on n008,
% 0.19/5.67 % Sat Sep 26 05:00:32 2026
% 0.19/5.67 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.19/5.69
% 0.19/5.69 % From the command line: assign(max_seconds, 300).
% 0.23/6.00
% 0.23/6.00 % Assigning unary symbol f5 kb_weight 0 and highest precedence (35).
% 0.23/6.00
% 0.23/6.00 % SZS status Theorem for theBenchmark
% 0.23/6.00
% 0.23/6.00 % Proof 1 at 0.23 (+ 0.06) seconds.
% 0.23/6.00 % Length of proof is 88.
% 0.23/6.00 % Level of proof is 15.
% 0.23/6.00 % Maximum clause weight is 31.000.
% 0.23/6.00 % Given clauses 341.
% 0.23/6.00
% 0.23/6.00 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------