%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PRO002+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 : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:20:53 AM UTC 2026
% Result : Theorem 19.11s 3.20s
% Output : CNFRefutation 19.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 21
% Syntax : Number of formulae : 150 ( 38 unt; 0 def)
% Number of atoms : 408 ( 44 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 424 ( 166 ~; 168 |; 70 &)
% ( 2 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 1 prp; 0-5 aty)
% Number of functors : 16 ( 16 usr; 7 con; 0-4 aty)
% Number of variables : 305 ( 28 sgn 114 !; 29 ?)
% Comments :
%------------------------------------------------------------------------------
fof(sos_01,axiom,
! [X2] :
( activity_occurrence(X2)
=> ? [X3] :
( occurrence_of(X2,X3)
& activity(X3) ) ),
file('theBenchmark.p',sos_01) ).
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_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_18,axiom,
! [X45,X46,X47,X48] :
( ( precedes(X46,X47)
& min_precedes(X45,X47,X48)
& min_precedes(X45,X46,X48) )
=> min_precedes(X46,X47,X48) ),
file('theBenchmark.p',sos_18) ).
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_24,axiom,
! [X67,X68] :
( subactivity_occurrence(X67,X68)
=> ( activity_occurrence(X68)
& activity_occurrence(X67) ) ),
file('theBenchmark.p',sos_24) ).
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_27,axiom,
! [X76,X77] :
( ( ~ atomic(X76)
& occurrence_of(X77,X76) )
=> ? [X78] :
( subactivity_occurrence(X78,X77)
& root(X78,X76) ) ),
file('theBenchmark.p',sos_27) ).
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_35,axiom,
! [X105,X106,X107,X108] :
( ( root_occ(X106,X107)
& root_occ(X105,X107)
& occurrence_of(X107,X108) )
=> X105 = X106 ),
file('theBenchmark.p',sos_35) ).
fof(sos_42,axiom,
! [X134,X135,X136,X137] :
( ( ~ min_precedes(X137,X136,X134)
& arboreal(X136)
& root_occ(X137,X135)
& subactivity_occurrence(X136,X135)
& occurrence_of(X135,X134) )
=> X137 = X136 ),
file('theBenchmark.p',sos_42) ).
fof(sos_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_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_63,axiom,
! [X169,X170,X171,X172,X173] :
( send_message(X169,X170,X171,X172,X173)
=> ( X169 != tptp2
& X169 != tptp3
& X169 != tptp4 ) ),
file('theBenchmark.p',sos_63) ).
fof(sos_64,axiom,
! [X174,X175,X176,X177,X178,X179] :
( ( occurrence_of(X179,X174)
& send_message(X174,X175,X176,X177,X178) )
=> min_precedes(X177,X179,X178) ),
file('theBenchmark.p',sos_64) ).
fof(sos_65,axiom,
! [X180,X181,X182] :
( tptp1(X180,X181,X182)
=> ( root(X182,X181)
& ~ atomic(X181)
& ~ atomic(X180)
& activity(X180) ) ),
file('theBenchmark.p',sos_65) ).
fof(sos_66,axiom,
! [X183,X184,X185,X186] :
( ( occurrence_of(X186,X183)
& tptp1(X183,X184,X185) )
=> ? [X187,X188,X189,X190] :
( root_occ(X190,X186)
& occurrence_of(X190,X187)
& send_message(X187,X188,X189,X185,X184) ) ),
file('theBenchmark.p',sos_66) ).
fof(goals,conjecture,
~ ? [X193,X194,X195] :
( occurrence_of(X195,X193)
& tptp1(X193,tptp0,X194) ),
file('theBenchmark.p',goals) ).
fof(goals_neg,negated_conjecture,
~ ~ ? [X193,X194,X195] :
( occurrence_of(X195,X193)
& tptp1(X193,tptp0,X194) ),
inference(assume_negation,[status(cth)],[goals]) ).
cnf(c_66,plain,
( activity_occurrence(A)
| ~ subactivity_occurrence(A,B) ),
inference(clausify,[status(thm)],[sos_24]) ).
fof(nnf_2,plain,
! [X2] :
( ? [X3] :
( occurrence_of(X2,X3)
& activity(X3) )
| ~ activity_occurrence(X2) ),
inference(fof_nnf,[status(thm)],[sos_01]) ).
fof(sk_sos_01_sk,plain,
! [X2] :
( ( occurrence_of(X2,sK0(X2))
& activity(sK0(X2)) )
| ~ activity_occurrence(X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X3,sK0(X2))],[nnf_2]) ).
fof(sk_sos_01,plain,
( ! [VAR_0] :
( occurrence_of(VAR_0,sK0(VAR_0))
| ~ activity_occurrence(VAR_0) )
& ! [VAR_0] :
( activity(sK0(VAR_0))
| ~ activity_occurrence(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_01_sk]) ).
cnf(c_67,plain,
( occurrence_of(A,sK0(A))
| ~ activity_occurrence(A) ),
inference(split_conjunct,[status(thm)],[sk_sos_01]) ).
cnf(c_84,plain,
( precedes(A,B)
| ~ min_precedes(A,B,C) ),
inference(clausify,[status(thm)],[sos_15]) ).
cnf(c_85,plain,
( min_precedes(B,D,C)
| ~ precedes(B,D)
| ~ min_precedes(A,D,C)
| ~ min_precedes(A,B,C) ),
inference(clausify,[status(thm)],[sos_18]) ).
cnf(c_92,plain,
( ~ root(B,C)
| ~ min_precedes(A,B,C) ),
inference(clausify,[status(thm)],[sos_14]) ).
cnf(c_93,plain,
( legal(A)
| ~ root(A,B) ),
inference(clausify,[status(thm)],[sos_16]) ).
fof(nnf_28,plain,
! [X76,X77] :
( ? [X78] :
( subactivity_occurrence(X78,X77)
& root(X78,X76) )
| atomic(X76)
| ~ occurrence_of(X77,X76) ),
inference(fof_nnf,[status(thm)],[sos_27]) ).
fof(sk_sos_27_sk,plain,
! [X76,X77] :
( ( subactivity_occurrence(sK1(X76,X77),X77)
& root(sK1(X76,X77),X76) )
| atomic(X76)
| ~ occurrence_of(X77,X76) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X78,sK1(X76,X77))],[nnf_28]) ).
fof(sk_sos_27,plain,
( ! [VAR_0,VAR_1] :
( subactivity_occurrence(sK1(VAR_1,VAR_0),VAR_0)
| atomic(VAR_1)
| ~ occurrence_of(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( root(sK1(VAR_1,VAR_0),VAR_1)
| atomic(VAR_1)
| ~ occurrence_of(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_27_sk]) ).
cnf(c_99,plain,
( root(sK1(B,A),B)
| atomic(B)
| ~ occurrence_of(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_27]) ).
cnf(c_101,plain,
( ~ root(A,C)
| ~ subactivity_occurrence(A,B)
| ~ occurrence_of(B,C)
| root_occ(A,B) ),
inference(clausify,[status(thm)],[sos_33]) ).
cnf(c_104,plain,
( root(C,B)
| ~ tptp1(A,B,C) ),
inference(clausify,[status(thm)],[sos_65]) ).
fof(nnf_55,plain,
! [X183,X184,X185,X186] :
( ? [X187,X188,X189,X190] :
( root_occ(X190,X186)
& occurrence_of(X190,X187)
& send_message(X187,X188,X189,X185,X184) )
| ~ occurrence_of(X186,X183)
| ~ tptp1(X183,X184,X185) ),
inference(fof_nnf,[status(thm)],[sos_66]) ).
fof(sk_sos_66_sk,plain,
! [X183,X184,X185,X186] :
( ( root_occ(sK8(X183,X184,X185,X186),X186)
& occurrence_of(sK8(X183,X184,X185,X186),sK2(X183,X184,X185,X186))
& send_message(sK2(X183,X184,X185,X186),sK3(X183,X184,X185,X186),sK4(X183,X184,X185,X186),X185,X184) )
| ~ occurrence_of(X186,X183)
| ~ tptp1(X183,X184,X185) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4,sK8]),skolemize(X187,sK2(X183,X184,X185,X186)),skolemize(X188,sK3(X183,X184,X185,X186)),skolemize(X189,sK4(X183,X184,X185,X186)),skolemize(X190,sK8(X183,X184,X185,X186))],[nnf_55]) ).
fof(sk_sos_66,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( root_occ(sK8(VAR_0,VAR_1,VAR_2,VAR_3),VAR_3)
| ~ occurrence_of(VAR_3,VAR_0)
| ~ tptp1(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( occurrence_of(sK8(VAR_0,VAR_1,VAR_2,VAR_3),sK2(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ occurrence_of(VAR_3,VAR_0)
| ~ tptp1(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( send_message(sK2(VAR_0,VAR_1,VAR_2,VAR_3),sK3(VAR_0,VAR_1,VAR_2,VAR_3),sK4(VAR_0,VAR_1,VAR_2,VAR_3),VAR_2,VAR_1)
| ~ occurrence_of(VAR_3,VAR_0)
| ~ tptp1(VAR_0,VAR_1,VAR_2) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_66_sk]) ).
cnf(c_130,plain,
( send_message(sK2(A,B,C,D),sK3(A,B,C,D),sK4(A,B,C,D),C,B)
| ~ occurrence_of(D,A)
| ~ tptp1(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_66]) ).
cnf(c_131,plain,
( min_precedes(D,F,E)
| ~ occurrence_of(F,A)
| ~ send_message(A,B,C,D,E) ),
inference(clausify,[status(thm)],[sos_64]) ).
cnf(c_132,plain,
( A != tptp2
| ~ send_message(A,B,C,D,E) ),
inference(clausify,[status(thm)],[sos_63]) ).
cnf(c_133,plain,
( A != tptp3
| ~ send_message(A,B,C,D,E) ),
inference(clausify,[status(thm)],[sos_63]) ).
cnf(c_202,plain,
( sK2(A,B,C,D) != tptp3
| ~ occurrence_of(D,A)
| ~ tptp1(A,B,C) ),
inference(resolve,[status(thm)],[c_130,c_133]) ).
cnf(c_203,plain,
( sK2(A,B,C,D) != tptp2
| ~ occurrence_of(D,A)
| ~ tptp1(A,B,C) ),
inference(resolve,[status(thm)],[c_130,c_132]) ).
cnf(c_204,plain,
( min_precedes(C,E,B)
| ~ occurrence_of(E,sK2(A,B,C,D))
| ~ occurrence_of(D,A)
| ~ tptp1(A,B,C) ),
inference(resolve,[status(thm)],[c_130,c_131]) ).
cnf(c_220,plain,
( ~ min_precedes(D,C,B)
| ~ tptp1(A,B,C) ),
inference(resolve,[status(thm)],[c_104,c_92]) ).
cnf(c_221,plain,
( legal(C)
| ~ tptp1(A,B,C) ),
inference(resolve,[status(thm)],[c_104,c_93]) ).
cnf(c_227,plain,
( atomic(A)
| ~ occurrence_of(B,A)
| ~ subactivity_occurrence(sK1(A,B),C)
| ~ occurrence_of(C,A)
| root_occ(sK1(A,B),C) ),
inference(resolve,[status(thm)],[c_101,c_99]) ).
cnf(c_236,plain,
( legal(sK1(B,A))
| atomic(B)
| ~ occurrence_of(A,B) ),
inference(resolve,[status(thm)],[c_99,c_93]) ).
fof(nnf_57,plain,
? [X193,X194,X195] :
( occurrence_of(X195,X193)
& tptp1(X193,tptp0,X194) ),
inference(fof_nnf,[status(thm)],[goals_neg]) ).
fof(sk_goals_neg,plain,
( occurrence_of(sK5,sK6)
& tptp1(sK6,tptp0,sK7) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7,sK5]),skolemize(X193,sK6),skolemize(X194,sK7),skolemize(X195,sK5)],[nnf_57]) ).
cnf(c_271,negated_conjecture,
occurrence_of(sK5,sK6),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_272,negated_conjecture,
tptp1(sK6,tptp0,sK7),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_274,plain,
( root_occ(sK8(A,B,C,D),D)
| ~ occurrence_of(D,A)
| ~ tptp1(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_66]) ).
cnf(c_275,plain,
( occurrence_of(sK8(A,B,C,D),sK2(A,B,C,D))
| ~ occurrence_of(D,A)
| ~ tptp1(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_66]) ).
cnf(c_277,plain,
( ~ atomic(A)
| ~ tptp1(A,B,C) ),
inference(clausify,[status(thm)],[sos_65]) ).
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(sK9(X161),sK10(X161),tptp0)
& leaf_occ(sK10(X161),X161)
& ( occurrence_of(sK10(X161),tptp2)
| occurrence_of(sK10(X161),tptp3) )
& root_occ(sK9(X161),X161)
& occurrence_of(sK9(X161),tptp4) )
| ~ occurrence_of(X161,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10]),skolemize(X162,sK9(X161)),skolemize(X163,sK10(X161))],[nnf_50]) ).
fof(sk_sos_49,plain,
( ! [VAR_0] :
( next_subocc(sK9(VAR_0),sK10(VAR_0),tptp0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( leaf_occ(sK10(VAR_0),VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( occurrence_of(sK10(VAR_0),tptp2)
| occurrence_of(sK10(VAR_0),tptp3)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( root_occ(sK9(VAR_0),VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( occurrence_of(sK9(VAR_0),tptp4)
| ~ occurrence_of(VAR_0,tptp0) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_49_sk]) ).
cnf(c_290,plain,
( next_subocc(sK9(A),sK10(A),tptp0)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
cnf(c_291,plain,
( leaf_occ(sK10(A),A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
cnf(c_292,plain,
( occurrence_of(sK10(A),tptp2)
| occurrence_of(sK10(A),tptp3)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
cnf(c_293,plain,
( root_occ(sK9(A),A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
cnf(c_300,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]) ).
cnf(c_301,plain,
( D = C
| min_precedes(D,C,B)
| ~ arboreal(C)
| ~ root_occ(D,A)
| ~ subactivity_occurrence(C,A)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_42]) ).
cnf(c_308,plain,
( D = C
| ~ root_occ(D,A)
| ~ root_occ(C,A)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_35]) ).
cnf(c_316,plain,
( subactivity_occurrence(sK1(B,A),A)
| atomic(B)
| ~ occurrence_of(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_27]) ).
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,sK11(X69,X70,X71))
& subactivity_occurrence(X70,sK11(X69,X70,X71))
& occurrence_of(sK11(X69,X70,X71),X69) )
| ~ min_precedes(X70,X71,X69) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(X72,sK11(X69,X70,X71))],[nnf_26]) ).
fof(sk_sos_25,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( subactivity_occurrence(VAR_1,sK11(VAR_2,VAR_0,VAR_1))
| ~ min_precedes(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( subactivity_occurrence(VAR_0,sK11(VAR_2,VAR_0,VAR_1))
| ~ min_precedes(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( occurrence_of(sK11(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_317,plain,
( subactivity_occurrence(B,sK11(C,A,B))
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_25]) ).
cnf(c_318,plain,
( subactivity_occurrence(A,sK11(C,A,B))
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_25]) ).
cnf(c_319,plain,
( occurrence_of(sK11(C,A,B),C)
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_25]) ).
cnf(c_324,plain,
( ~ min_precedes(D,B,C)
| ~ min_precedes(A,D,C)
| ~ next_subocc(A,B,C) ),
inference(clausify,[status(thm)],[sos_22]) ).
cnf(c_325,plain,
( min_precedes(A,B,C)
| ~ next_subocc(A,B,C) ),
inference(clausify,[status(thm)],[sos_22]) ).
cnf(c_331,plain,
( arboreal(A)
| ~ legal(A) ),
inference(clausify,[status(thm)],[sos_08]) ).
cnf(c_337,plain,
( C = B
| ~ occurrence_of(A,C)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_02]) ).
cnf(c_338,plain,
( ~ subactivity_occurrence(A,B)
| occurrence_of(A,sK0(A)) ),
inference(resolve,[status(thm)],[c_67,c_66]) ).
cnf(c_341,plain,
( min_precedes(A,B,E)
| ~ min_precedes(D,B,E)
| ~ min_precedes(D,A,E)
| ~ min_precedes(A,B,C) ),
inference(resolve,[status(thm)],[c_84,c_85]) ).
cnf(c_391,plain,
( atomic(A)
| ~ subactivity_occurrence(sK1(A,B),B)
| ~ occurrence_of(B,A)
| root_occ(sK1(A,B),B) ),
inference(factor,[status(thm)],[c_227]) ).
cnf(c_434,plain,
( legal(sK1(sK6,sK5))
| atomic(sK6) ),
inference(resolve,[status(thm)],[c_271,c_236]) ).
cnf(c_453,plain,
( min_precedes(B,C,A)
| ~ occurrence_of(C,sK2(sK6,A,B,sK5))
| ~ tptp1(sK6,A,B) ),
inference(resolve,[status(thm)],[c_271,c_204]) ).
cnf(c_501,plain,
legal(sK7),
inference(resolve,[status(thm)],[c_272,c_221]) ).
cnf(c_502,plain,
~ min_precedes(A,sK7,tptp0),
inference(resolve,[status(thm)],[c_272,c_220]) ).
cnf(c_507,plain,
( sK2(sK6,tptp0,sK7,A) != tptp2
| ~ occurrence_of(A,sK6) ),
inference(resolve,[status(thm)],[c_272,c_203]) ).
cnf(c_508,plain,
( sK2(sK6,tptp0,sK7,A) != tptp3
| ~ occurrence_of(A,sK6) ),
inference(resolve,[status(thm)],[c_272,c_202]) ).
cnf(c_524,plain,
( root_occ(sK8(sK6,tptp0,sK7,A),A)
| ~ occurrence_of(A,sK6) ),
inference(resolve,[status(thm)],[c_274,c_272]) ).
cnf(c_526,plain,
( occurrence_of(sK8(sK6,tptp0,sK7,A),sK2(sK6,tptp0,sK7,A))
| ~ occurrence_of(A,sK6) ),
inference(resolve,[status(thm)],[c_275,c_272]) ).
cnf(c_528,plain,
~ atomic(sK6),
inference(resolve,[status(thm)],[c_277,c_272]) ).
cnf(c_558,plain,
legal(sK1(sK6,sK5)),
inference(resolve,[status(thm)],[c_528,c_434]) ).
cnf(c_595,plain,
( B = A
| ~ root_occ(B,sK5)
| ~ root_occ(A,sK5) ),
inference(resolve,[status(thm)],[c_308,c_271]) ).
cnf(c_11941,negated_conjecture,
( subactivity_occurrence(sK1(sK6,sK5),sK5)
| atomic(sK6) ),
inference(resolve,[status(thm)],[c_316,c_271]) ).
cnf(c_598,negated_conjecture,
subactivity_occurrence(sK1(sK6,sK5),sK5),
inference(resolve,[status(thm)],[c_528,c_11941]) ).
cnf(c_11942,negated_conjecture,
( atomic(sK6)
| ~ subactivity_occurrence(sK1(sK6,sK5),sK5)
| root_occ(sK1(sK6,sK5),sK5) ),
inference(resolve,[status(thm)],[c_391,c_271]) ).
cnf(c_11943,negated_conjecture,
( atomic(sK6)
| root_occ(sK1(sK6,sK5),sK5) ),
inference(resolve,[status(thm)],[c_598,c_11942]) ).
cnf(c_625,negated_conjecture,
root_occ(sK1(sK6,sK5),sK5),
inference(resolve,[status(thm)],[c_528,c_11943]) ).
cnf(c_648,plain,
arboreal(sK7),
inference(resolve,[status(thm)],[c_501,c_331]) ).
cnf(c_11944,plain,
( C = sK7
| min_precedes(C,sK7,B)
| ~ root_occ(C,A)
| ~ subactivity_occurrence(sK7,A)
| ~ occurrence_of(A,B) ),
inference(resolve,[status(thm)],[c_648,c_301]) ).
cnf(c_660,plain,
( sK7 = C
| min_precedes(C,sK7,B)
| ~ root_occ(C,A)
| ~ subactivity_occurrence(sK7,A)
| ~ occurrence_of(A,B) ),
inference(copy,[status(thm)],[c_11944]) ).
cnf(c_662,plain,
sK2(sK6,tptp0,sK7,sK5) != tptp2,
inference(resolve,[status(thm)],[c_507,c_271]) ).
cnf(c_669,plain,
arboreal(sK1(sK6,sK5)),
inference(resolve,[status(thm)],[c_558,c_331]) ).
cnf(c_11945,plain,
( C = sK1(sK6,sK5)
| min_precedes(sK1(sK6,sK5),C,B)
| ~ leaf_occ(C,A)
| ~ subactivity_occurrence(sK1(sK6,sK5),A)
| ~ occurrence_of(A,B) ),
inference(resolve,[status(thm)],[c_669,c_300]) ).
cnf(c_683,plain,
( sK1(sK6,sK5) = C
| min_precedes(sK1(sK6,sK5),C,B)
| ~ leaf_occ(C,A)
| ~ subactivity_occurrence(sK1(sK6,sK5),A)
| ~ occurrence_of(A,B) ),
inference(copy,[status(thm)],[c_11945]) ).
cnf(c_684,plain,
sK2(sK6,tptp0,sK7,sK5) != tptp3,
inference(resolve,[status(thm)],[c_508,c_271]) ).
cnf(c_924,plain,
occurrence_of(sK1(sK6,sK5),sK0(sK1(sK6,sK5))),
inference(resolve,[status(thm)],[c_598,c_338]) ).
cnf(c_932,plain,
( sK1(sK6,sK5) = A
| ~ root_occ(A,sK5) ),
inference(resolve,[status(thm)],[c_625,c_595]) ).
cnf(c_1036,plain,
root_occ(sK8(sK6,tptp0,sK7,sK5),sK5),
inference(resolve,[status(thm)],[c_524,c_271]) ).
cnf(c_11946,plain,
sK1(sK6,sK5) = sK8(sK6,tptp0,sK7,sK5),
inference(resolve,[status(thm)],[c_1036,c_932]) ).
cnf(c_1039,plain,
sK8(sK6,tptp0,sK7,sK5) = sK1(sK6,sK5),
inference(copy,[status(thm)],[c_11946]) ).
cnf(c_1107,plain,
( min_precedes(sK7,A,tptp0)
| ~ occurrence_of(A,sK2(sK6,tptp0,sK7,sK5)) ),
inference(resolve,[status(thm)],[c_453,c_272]) ).
cnf(c_11947,negated_conjecture,
occurrence_of(sK8(sK6,tptp0,sK7,sK5),sK2(sK6,tptp0,sK7,sK5)),
inference(resolve,[status(thm)],[c_526,c_271]) ).
cnf(c_2155,negated_conjecture,
occurrence_of(sK1(sK6,sK5),sK2(sK6,tptp0,sK7,sK5)),
inference(paramod,[status(thm)],[c_1039,c_11947]) ).
cnf(c_2156,plain,
min_precedes(sK7,sK1(sK6,sK5),tptp0),
inference(resolve,[status(thm)],[c_2155,c_1107]) ).
cnf(c_2183,plain,
( sK2(sK6,tptp0,sK7,sK5) = A
| ~ occurrence_of(sK1(sK6,sK5),A) ),
inference(resolve,[status(thm)],[c_2155,c_337]) ).
cnf(c_2225,plain,
( min_precedes(sK1(sK6,sK5),A,tptp0)
| ~ min_precedes(sK7,A,tptp0)
| ~ min_precedes(sK1(sK6,sK5),A,B) ),
inference(resolve,[status(thm)],[c_2156,c_341]) ).
cnf(c_2230,plain,
( ~ min_precedes(sK1(sK6,sK5),A,tptp0)
| ~ next_subocc(sK7,A,tptp0) ),
inference(resolve,[status(thm)],[c_2156,c_324]) ).
cnf(c_2233,plain,
occurrence_of(sK11(tptp0,sK7,sK1(sK6,sK5)),tptp0),
inference(resolve,[status(thm)],[c_2156,c_319]) ).
cnf(c_2234,plain,
subactivity_occurrence(sK7,sK11(tptp0,sK7,sK1(sK6,sK5))),
inference(resolve,[status(thm)],[c_2156,c_318]) ).
cnf(c_2235,plain,
subactivity_occurrence(sK1(sK6,sK5),sK11(tptp0,sK7,sK1(sK6,sK5))),
inference(resolve,[status(thm)],[c_2156,c_317]) ).
cnf(c_2383,plain,
sK2(sK6,tptp0,sK7,sK5) = sK0(sK1(sK6,sK5)),
inference(resolve,[status(thm)],[c_924,c_2183]) ).
cnf(c_2415,plain,
( sK0(sK1(sK6,sK5)) = A
| ~ occurrence_of(sK1(sK6,sK5),A) ),
inference(resolve,[status(thm)],[c_924,c_337]) ).
cnf(c_2491,plain,
sK0(sK1(sK6,sK5)) != tptp3,
inference(paramod,[status(thm)],[c_2383,c_684]) ).
cnf(c_2492,plain,
sK0(sK1(sK6,sK5)) != tptp2,
inference(paramod,[status(thm)],[c_2383,c_662]) ).
cnf(c_11948,plain,
( sK7 = A
| min_precedes(A,sK7,tptp0)
| ~ root_occ(A,sK11(tptp0,sK7,sK1(sK6,sK5)))
| ~ subactivity_occurrence(sK7,sK11(tptp0,sK7,sK1(sK6,sK5))) ),
inference(resolve,[status(thm)],[c_2233,c_660]) ).
cnf(c_11949,plain,
( sK7 = A
| min_precedes(A,sK7,tptp0)
| ~ root_occ(A,sK11(tptp0,sK7,sK1(sK6,sK5))) ),
inference(resolve,[status(thm)],[c_2234,c_11948]) ).
cnf(c_2696,plain,
( sK7 = A
| ~ root_occ(A,sK11(tptp0,sK7,sK1(sK6,sK5))) ),
inference(resolve,[status(thm)],[c_502,c_11949]) ).
cnf(c_2780,plain,
root_occ(sK9(sK11(tptp0,sK7,sK1(sK6,sK5))),sK11(tptp0,sK7,sK1(sK6,sK5))),
inference(resolve,[status(thm)],[c_2233,c_293]) ).
cnf(c_2781,plain,
( occurrence_of(sK10(sK11(tptp0,sK7,sK1(sK6,sK5))),tptp2)
| occurrence_of(sK10(sK11(tptp0,sK7,sK1(sK6,sK5))),tptp3) ),
inference(resolve,[status(thm)],[c_2233,c_292]) ).
cnf(c_2782,plain,
leaf_occ(sK10(sK11(tptp0,sK7,sK1(sK6,sK5))),sK11(tptp0,sK7,sK1(sK6,sK5))),
inference(resolve,[status(thm)],[c_2233,c_291]) ).
cnf(c_2783,plain,
next_subocc(sK9(sK11(tptp0,sK7,sK1(sK6,sK5))),sK10(sK11(tptp0,sK7,sK1(sK6,sK5))),tptp0),
inference(resolve,[status(thm)],[c_2233,c_290]) ).
cnf(c_11950,plain,
( sK1(sK6,sK5) = A
| min_precedes(sK1(sK6,sK5),A,tptp0)
| ~ leaf_occ(A,sK11(tptp0,sK7,sK1(sK6,sK5)))
| ~ subactivity_occurrence(sK1(sK6,sK5),sK11(tptp0,sK7,sK1(sK6,sK5))) ),
inference(resolve,[status(thm)],[c_683,c_2233]) ).
cnf(c_4722,plain,
( sK1(sK6,sK5) = A
| min_precedes(sK1(sK6,sK5),A,tptp0)
| ~ leaf_occ(A,sK11(tptp0,sK7,sK1(sK6,sK5))) ),
inference(resolve,[status(thm)],[c_2235,c_11950]) ).
cnf(c_11951,plain,
sK7 = sK9(sK11(tptp0,sK7,sK1(sK6,sK5))),
inference(resolve,[status(thm)],[c_2780,c_2696]) ).
cnf(c_10699,plain,
sK9(sK11(tptp0,sK7,sK1(sK6,sK5))) = sK7,
inference(copy,[status(thm)],[c_11951]) ).
cnf(c_10700,plain,
next_subocc(sK7,sK10(sK11(tptp0,sK7,sK1(sK6,sK5))),tptp0),
inference(paramod,[status(thm)],[c_10699,c_2783]) ).
cnf(c_10704,plain,
~ min_precedes(sK1(sK6,sK5),sK10(sK11(tptp0,sK7,sK1(sK6,sK5))),tptp0),
inference(resolve,[status(thm)],[c_10700,c_2230]) ).
cnf(c_10707,plain,
min_precedes(sK7,sK10(sK11(tptp0,sK7,sK1(sK6,sK5))),tptp0),
inference(resolve,[status(thm)],[c_10700,c_325]) ).
cnf(c_11952,plain,
( min_precedes(sK1(sK6,sK5),sK10(sK11(tptp0,sK7,sK1(sK6,sK5))),tptp0)
| ~ min_precedes(sK1(sK6,sK5),sK10(sK11(tptp0,sK7,sK1(sK6,sK5))),A) ),
inference(resolve,[status(thm)],[c_10707,c_2225]) ).
cnf(c_10781,plain,
~ min_precedes(sK1(sK6,sK5),sK10(sK11(tptp0,sK7,sK1(sK6,sK5))),A),
inference(resolve,[status(thm)],[c_10704,c_11952]) ).
cnf(c_11953,plain,
( sK1(sK6,sK5) = sK10(sK11(tptp0,sK7,sK1(sK6,sK5)))
| min_precedes(sK1(sK6,sK5),sK10(sK11(tptp0,sK7,sK1(sK6,sK5))),tptp0) ),
inference(resolve,[status(thm)],[c_4722,c_2782]) ).
cnf(c_11954,plain,
( sK10(sK11(tptp0,sK7,sK1(sK6,sK5))) = sK1(sK6,sK5)
| min_precedes(sK1(sK6,sK5),sK10(sK11(tptp0,sK7,sK1(sK6,sK5))),tptp0) ),
inference(copy,[status(thm)],[c_11953]) ).
cnf(c_11840,plain,
sK10(sK11(tptp0,sK7,sK1(sK6,sK5))) = sK1(sK6,sK5),
inference(resolve,[status(thm)],[c_10781,c_11954]) ).
cnf(c_11955,plain,
( occurrence_of(sK10(sK11(tptp0,sK7,sK1(sK6,sK5))),tptp2)
| occurrence_of(sK1(sK6,sK5),tptp3) ),
inference(paramod,[status(thm)],[c_11840,c_2781]) ).
cnf(c_11883,plain,
( occurrence_of(sK1(sK6,sK5),tptp2)
| occurrence_of(sK1(sK6,sK5),tptp3) ),
inference(paramod,[status(thm)],[c_11840,c_11955]) ).
cnf(c_11956,plain,
( sK0(sK1(sK6,sK5)) = tptp3
| occurrence_of(sK1(sK6,sK5),tptp2) ),
inference(resolve,[status(thm)],[c_11883,c_2415]) ).
cnf(c_11924,plain,
occurrence_of(sK1(sK6,sK5),tptp2),
inference(resolve,[status(thm)],[c_2491,c_11956]) ).
cnf(c_11957,plain,
sK0(sK1(sK6,sK5)) = tptp2,
inference(resolve,[status(thm)],[c_11924,c_2415]) ).
cnf(c_11940,plain,
$false,
inference(resolve,[status(thm)],[c_2492,c_11957]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO002+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.11/0.38 % Computer : n014.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sat Sep 26 04:54:17 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.38 % Process 2181175 was started by sandbox on n014,
% 0.11/0.38 % Sat Sep 26 04:54:17 2026
% 0.11/0.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.11/0.40
% 0.11/0.40 % From the command line: assign(max_seconds, 300).
% 19.11/3.20
% 19.11/3.20 % given #500 (T,wt=22): 1398 f9(c2,f1(c2)) = f1(c2). [resolve(790,a,721,a),flip(a)].
% 19.11/3.20
% 19.11/3.20 % given #1000 (T,wt=27): 3074 -subactivity_occurrence(f12(c1,c3),c2) | -subactivity_occurrence(f7(c2,tptp0),c2) | f12(c1,c3) = f7(c2,tptp0). [resolve(983,a,2104,a)].
% 19.11/3.20
% 19.11/3.20 % given #1500 (W,wt=31): 4767 legal(f7(f12(c1,c3),c1)) | -min_precedes(A,f12(c1,c3),f15(f12(c1,c3),c3)). [resolve(3824,b,938,a)].
% 19.11/3.20
% 19.11/3.20 % given #2000 (T,wt=29): 10699 f17(f10(tptp0,c2,f12(c1,c3))) = c2. [resolve(2780,a,2696,a),flip(a)].
% 19.11/3.20
% 19.11/3.20 % SZS status Theorem for theBenchmark
% 19.11/3.20
% 19.11/3.20 % Proof 1 at 2.25 (+ 0.49) seconds.
% 19.11/3.20 % Length of proof is 115.
% 19.11/3.20 % Level of proof is 18.
% 19.11/3.20 % Maximum clause weight is 38.000.
% 19.11/3.20 % Given clauses 2180.
% 19.11/3.20
% 19.11/3.20 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------