%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PRO002+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 : n019.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 3.97s 0.98s
% Output : CNFRefutation 3.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 23
% Syntax : Number of formulae : 172 ( 40 unt; 0 def)
% Number of atoms : 490 ( 54 equ)
% Maximal formula atoms : 11 ( 2 avg)
% Number of connectives : 519 ( 201 ~; 211 |; 85 &)
% ( 3 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 18 ( 16 usr; 1 prp; 0-5 aty)
% Number of functors : 18 ( 18 usr; 7 con; 0-4 aty)
% Number of variables : 343 ( 30 sgn 140 !; 34 ?)
% Comments :
%------------------------------------------------------------------------------
fof(sos,axiom,
! [X0,X1] :
( ( ~ atomic(X0)
& occurrence_of(X1,X0) )
=> ? [X2] :
( subactivity_occurrence(X2,X1)
& root(X2,X0) ) ),
file('theBenchmark.p',sos) ).
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_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_05,axiom,
! [X18,X19] :
( root(X19,X18)
=> ? [X20] :
( atocc(X19,X20)
& subactivity(X20,X18) ) ),
file('theBenchmark.p',sos_05) ).
fof(sos_06,axiom,
! [X21,X22,X23] :
( min_precedes(X22,X23,X21)
=> ? [X24] :
( subactivity_occurrence(X23,X24)
& subactivity_occurrence(X22,X24)
& occurrence_of(X24,X21) ) ),
file('theBenchmark.p',sos_06) ).
fof(sos_08,axiom,
! [X28,X29,X30] :
( ( occurrence_of(X28,X30)
& occurrence_of(X28,X29) )
=> X29 = X30 ),
file('theBenchmark.p',sos_08) ).
fof(sos_10,axiom,
! [X35,X36,X37] :
( ( root_occ(X36,X35)
& occurrence_of(X35,X37) )
=> ~ ? [X38] : min_precedes(X38,X36,X37) ),
file('theBenchmark.p',sos_10) ).
fof(sos_11,axiom,
! [X39,X40] :
( subactivity_occurrence(X39,X40)
=> ( activity_occurrence(X40)
& activity_occurrence(X39) ) ),
file('theBenchmark.p',sos_11) ).
fof(sos_12,axiom,
! [X41] :
( activity_occurrence(X41)
=> ? [X42] :
( occurrence_of(X41,X42)
& activity(X42) ) ),
file('theBenchmark.p',sos_12) ).
fof(sos_13,axiom,
! [X43] :
( legal(X43)
=> arboreal(X43) ),
file('theBenchmark.p',sos_13) ).
fof(sos_14,axiom,
! [X44,X45] :
( atocc(X44,X45)
<=> ? [X46] :
( occurrence_of(X44,X46)
& atomic(X46)
& subactivity(X45,X46) ) ),
file('theBenchmark.p',sos_14) ).
fof(sos_17,axiom,
! [X53,X54] :
( root(X53,X54)
=> legal(X53) ),
file('theBenchmark.p',sos_17) ).
fof(sos_19,axiom,
! [X58,X59] :
( root_occ(X58,X59)
<=> ? [X60] :
( root(X58,X60)
& subactivity_occurrence(X58,X59)
& occurrence_of(X59,X60) ) ),
file('theBenchmark.p',sos_19) ).
fof(sos_22,axiom,
! [X65,X66,X67] :
( min_precedes(X65,X66,X67)
=> ~ root(X66,X67) ),
file('theBenchmark.p',sos_22) ).
fof(sos_25,axiom,
! [X75,X76,X77] :
( next_subocc(X75,X76,X77)
=> ( arboreal(X76)
& arboreal(X75) ) ),
file('theBenchmark.p',sos_25) ).
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_29,axiom,
! [X90,X91,X92,X93] :
( ( root_occ(X91,X92)
& root_occ(X90,X92)
& occurrence_of(X92,X93) )
=> X90 = X91 ),
file('theBenchmark.p',sos_29) ).
fof(sos_32,axiom,
! [X101] :
( occurrence_of(X101,tptp0)
=> ? [X102,X103] :
( next_subocc(X102,X103,tptp0)
& leaf_occ(X103,X101)
& ( occurrence_of(X103,tptp2)
| occurrence_of(X103,tptp3) )
& root_occ(X102,X101)
& occurrence_of(X102,tptp4) ) ),
file('theBenchmark.p',sos_32) ).
fof(sos_46,axiom,
! [X109,X110,X111,X112,X113] :
( send_message(X109,X110,X111,X112,X113)
=> ( X109 != tptp2
& X109 != tptp3
& X109 != tptp4 ) ),
file('theBenchmark.p',sos_46) ).
fof(sos_47,axiom,
! [X114,X115,X116,X117,X118,X119] :
( ( occurrence_of(X119,X114)
& send_message(X114,X115,X116,X117,X118) )
=> min_precedes(X117,X119,X118) ),
file('theBenchmark.p',sos_47) ).
fof(sos_48,axiom,
! [X120,X121,X122] :
( tptp1(X120,X121,X122)
=> ( root(X122,X121)
& ~ atomic(X121)
& ~ atomic(X120)
& activity(X120) ) ),
file('theBenchmark.p',sos_48) ).
fof(sos_49,axiom,
! [X123,X124,X125,X126] :
( ( occurrence_of(X126,X123)
& tptp1(X123,X124,X125) )
=> ? [X127,X128,X129,X130] :
( root_occ(X130,X126)
& occurrence_of(X130,X127)
& send_message(X127,X128,X129,X125,X124) ) ),
file('theBenchmark.p',sos_49) ).
fof(goals,conjecture,
~ ? [X133,X134,X135] :
( occurrence_of(X135,X133)
& tptp1(X133,tptp0,X134) ),
file('theBenchmark.p',goals) ).
fof(goals_neg,negated_conjecture,
~ ~ ? [X133,X134,X135] :
( occurrence_of(X135,X133)
& tptp1(X133,tptp0,X134) ),
inference(assume_negation,[status(cth)],[goals]) ).
fof(nnf_1,plain,
! [X0,X1] :
( ? [X2] :
( subactivity_occurrence(X2,X1)
& root(X2,X0) )
| atomic(X0)
| ~ occurrence_of(X1,X0) ),
inference(fof_nnf,[status(thm)],[sos]) ).
fof(sk_sos_sk,plain,
! [X0,X1] :
( ( subactivity_occurrence(sK0(X0,X1),X1)
& root(sK0(X0,X1),X0) )
| atomic(X0)
| ~ occurrence_of(X1,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X2,sK0(X0,X1))],[nnf_1]) ).
fof(sk_sos,plain,
( ! [VAR_0,VAR_1] :
( subactivity_occurrence(sK0(VAR_1,VAR_0),VAR_0)
| atomic(VAR_1)
| ~ occurrence_of(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( root(sK0(VAR_1,VAR_0),VAR_1)
| atomic(VAR_1)
| ~ occurrence_of(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_sk]) ).
cnf(c_42,plain,
( root(sK0(B,A),B)
| atomic(B)
| ~ occurrence_of(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos]) ).
fof(nnf_6,plain,
! [X18,X19] :
( ? [X20] :
( atocc(X19,X20)
& subactivity(X20,X18) )
| ~ root(X19,X18) ),
inference(fof_nnf,[status(thm)],[sos_05]) ).
fof(sk_sos_05_sk,plain,
! [X18,X19] :
( ( atocc(X19,sK1(X18,X19))
& subactivity(sK1(X18,X19),X18) )
| ~ root(X19,X18) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X20,sK1(X18,X19))],[nnf_6]) ).
fof(sk_sos_05,plain,
( ! [VAR_0,VAR_1] :
( atocc(VAR_0,sK1(VAR_1,VAR_0))
| ~ root(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( subactivity(sK1(VAR_1,VAR_0),VAR_1)
| ~ root(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_05_sk]) ).
cnf(c_43,plain,
( atocc(A,sK1(B,A))
| ~ root(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_05]) ).
cnf(c_46,plain,
( legal(A)
| ~ root(A,B) ),
inference(clausify,[status(thm)],[sos_17]) ).
cnf(c_48,plain,
( ~ root(A,C)
| ~ subactivity_occurrence(A,B)
| ~ occurrence_of(B,C)
| root_occ(A,B) ),
inference(clausify,[status(thm)],[sos_19]) ).
cnf(c_49,plain,
( ~ root(B,C)
| ~ min_precedes(A,B,C) ),
inference(clausify,[status(thm)],[sos_22]) ).
cnf(c_53,plain,
( root(C,B)
| ~ tptp1(A,B,C) ),
inference(clausify,[status(thm)],[sos_48]) ).
fof(nnf_13,plain,
! [X41] :
( ? [X42] :
( occurrence_of(X41,X42)
& activity(X42) )
| ~ activity_occurrence(X41) ),
inference(fof_nnf,[status(thm)],[sos_12]) ).
fof(sk_sos_12_sk,plain,
! [X41] :
( ( occurrence_of(X41,sK2(X41))
& activity(sK2(X41)) )
| ~ activity_occurrence(X41) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X42,sK2(X41))],[nnf_13]) ).
fof(sk_sos_12,plain,
( ! [VAR_0] :
( occurrence_of(VAR_0,sK2(VAR_0))
| ~ activity_occurrence(VAR_0) )
& ! [VAR_0] :
( activity(sK2(VAR_0))
| ~ activity_occurrence(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_12_sk]) ).
cnf(c_54,plain,
( occurrence_of(A,sK2(A))
| ~ activity_occurrence(A) ),
inference(split_conjunct,[status(thm)],[sk_sos_12]) ).
cnf(c_56,plain,
( activity_occurrence(A)
| ~ subactivity_occurrence(A,B) ),
inference(clausify,[status(thm)],[sos_11]) ).
cnf(c_85,plain,
( atomic(A)
| ~ occurrence_of(B,A)
| legal(sK0(A,B)) ),
inference(resolve,[status(thm)],[c_46,c_42]) ).
cnf(c_90,plain,
( legal(C)
| ~ tptp1(A,B,C) ),
inference(resolve,[status(thm)],[c_53,c_46]) ).
cnf(c_99,plain,
( arboreal(A)
| ~ legal(A) ),
inference(clausify,[status(thm)],[sos_13]) ).
cnf(c_101,plain,
( ~ min_precedes(D,B,C)
| ~ min_precedes(A,D,C)
| ~ next_subocc(A,B,C) ),
inference(clausify,[status(thm)],[sos_26]) ).
cnf(c_104,plain,
( arboreal(A)
| ~ next_subocc(A,B,C) ),
inference(clausify,[status(thm)],[sos_25]) ).
fof(nnf_33,plain,
! [X101] :
( ? [X102,X103] :
( next_subocc(X102,X103,tptp0)
& leaf_occ(X103,X101)
& ( occurrence_of(X103,tptp2)
| occurrence_of(X103,tptp3) )
& root_occ(X102,X101)
& occurrence_of(X102,tptp4) )
| ~ occurrence_of(X101,tptp0) ),
inference(fof_nnf,[status(thm)],[sos_32]) ).
fof(sk_sos_32_sk,plain,
! [X101] :
( ( next_subocc(sK3(X101),sK4(X101),tptp0)
& leaf_occ(sK4(X101),X101)
& ( occurrence_of(sK4(X101),tptp2)
| occurrence_of(sK4(X101),tptp3) )
& root_occ(sK3(X101),X101)
& occurrence_of(sK3(X101),tptp4) )
| ~ occurrence_of(X101,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4]),skolemize(X102,sK3(X101)),skolemize(X103,sK4(X101))],[nnf_33]) ).
fof(sk_sos_32,plain,
( ! [VAR_0] :
( next_subocc(sK3(VAR_0),sK4(VAR_0),tptp0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( leaf_occ(sK4(VAR_0),VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( occurrence_of(sK4(VAR_0),tptp2)
| occurrence_of(sK4(VAR_0),tptp3)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( root_occ(sK3(VAR_0),VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0] :
( occurrence_of(sK3(VAR_0),tptp4)
| ~ occurrence_of(VAR_0,tptp0) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_32_sk]) ).
cnf(c_106,plain,
( next_subocc(sK3(A),sK4(A),tptp0)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
fof(nnf_38,plain,
! [X123,X124,X125,X126] :
( ? [X127,X128,X129,X130] :
( root_occ(X130,X126)
& occurrence_of(X130,X127)
& send_message(X127,X128,X129,X125,X124) )
| ~ occurrence_of(X126,X123)
| ~ tptp1(X123,X124,X125) ),
inference(fof_nnf,[status(thm)],[sos_49]) ).
fof(sk_sos_49_sk,plain,
! [X123,X124,X125,X126] :
( ( root_occ(sK10(X123,X124,X125,X126),X126)
& occurrence_of(sK10(X123,X124,X125,X126),sK5(X123,X124,X125,X126))
& send_message(sK5(X123,X124,X125,X126),sK6(X123,X124,X125,X126),sK7(X123,X124,X125,X126),X125,X124) )
| ~ occurrence_of(X126,X123)
| ~ tptp1(X123,X124,X125) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK6,sK7,sK10]),skolemize(X127,sK5(X123,X124,X125,X126)),skolemize(X128,sK6(X123,X124,X125,X126)),skolemize(X129,sK7(X123,X124,X125,X126)),skolemize(X130,sK10(X123,X124,X125,X126))],[nnf_38]) ).
fof(sk_sos_49,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( root_occ(sK10(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(sK10(VAR_0,VAR_1,VAR_2,VAR_3),sK5(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(sK5(VAR_0,VAR_1,VAR_2,VAR_3),sK6(VAR_0,VAR_1,VAR_2,VAR_3),sK7(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_49_sk]) ).
cnf(c_107,plain,
( send_message(sK5(A,B,C,D),sK6(A,B,C,D),sK7(A,B,C,D),C,B)
| ~ occurrence_of(D,A)
| ~ tptp1(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
cnf(c_126,plain,
( min_precedes(D,F,E)
| ~ occurrence_of(F,A)
| ~ send_message(A,B,C,D,E) ),
inference(clausify,[status(thm)],[sos_47]) ).
cnf(c_127,plain,
( A != tptp2
| ~ send_message(A,B,C,D,E) ),
inference(clausify,[status(thm)],[sos_46]) ).
cnf(c_128,plain,
( A != tptp3
| ~ send_message(A,B,C,D,E) ),
inference(clausify,[status(thm)],[sos_46]) ).
cnf(c_142,plain,
( ~ occurrence_of(D,A)
| ~ tptp1(A,B,C)
| sK5(A,B,C,D) != tptp3 ),
inference(resolve,[status(thm)],[c_128,c_107]) ).
cnf(c_143,plain,
( ~ occurrence_of(D,A)
| ~ tptp1(A,B,C)
| sK5(A,B,C,D) != tptp2 ),
inference(resolve,[status(thm)],[c_127,c_107]) ).
cnf(c_144,plain,
( ~ occurrence_of(E,B)
| ~ tptp1(B,C,D)
| min_precedes(D,A,C)
| ~ occurrence_of(A,sK5(B,C,D,E)) ),
inference(resolve,[status(thm)],[c_126,c_107]) ).
cnf(c_161,plain,
( ~ tptp1(B,C,A)
| arboreal(A) ),
inference(resolve,[status(thm)],[c_99,c_90]) ).
cnf(c_164,plain,
( atomic(A)
| ~ occurrence_of(B,A)
| arboreal(sK0(A,B)) ),
inference(resolve,[status(thm)],[c_99,c_85]) ).
cnf(c_177,plain,
( subactivity_occurrence(sK0(B,A),A)
| atomic(B)
| ~ occurrence_of(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos]) ).
cnf(c_179,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_180,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]) ).
fof(nnf_7,plain,
! [X21,X22,X23] :
( ? [X24] :
( subactivity_occurrence(X23,X24)
& subactivity_occurrence(X22,X24)
& occurrence_of(X24,X21) )
| ~ min_precedes(X22,X23,X21) ),
inference(fof_nnf,[status(thm)],[sos_06]) ).
fof(sk_sos_06_sk,plain,
! [X21,X22,X23] :
( ( subactivity_occurrence(X23,sK8(X21,X22,X23))
& subactivity_occurrence(X22,sK8(X21,X22,X23))
& occurrence_of(sK8(X21,X22,X23),X21) )
| ~ min_precedes(X22,X23,X21) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X24,sK8(X21,X22,X23))],[nnf_7]) ).
fof(sk_sos_06,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( subactivity_occurrence(VAR_1,sK8(VAR_2,VAR_0,VAR_1))
| ~ min_precedes(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( subactivity_occurrence(VAR_0,sK8(VAR_2,VAR_0,VAR_1))
| ~ min_precedes(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( occurrence_of(sK8(VAR_2,VAR_0,VAR_1),VAR_2)
| ~ min_precedes(VAR_0,VAR_1,VAR_2) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_06_sk]) ).
cnf(c_181,plain,
( occurrence_of(sK8(C,A,B),C)
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_06]) ).
cnf(c_182,plain,
( subactivity_occurrence(A,sK8(C,A,B))
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_06]) ).
cnf(c_183,plain,
( subactivity_occurrence(B,sK8(C,A,B))
| ~ min_precedes(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_06]) ).
cnf(c_184,plain,
( C = B
| ~ occurrence_of(A,C)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_08]) ).
cnf(c_186,plain,
( ~ min_precedes(D,C,B)
| ~ root_occ(C,A)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_10]) ).
fof(nnf_15,plain,
! [X44,X45] :
( ( ! [X46] :
( ~ occurrence_of(X44,X46)
| ~ atomic(X46)
| ~ subactivity(X45,X46) )
| atocc(X44,X45) )
& ( ? [X136] :
( occurrence_of(X44,X136)
& atomic(X136)
& subactivity(X45,X136) )
| ~ atocc(X44,X45) ) ),
inference(fof_nnf,[status(thm)],[sos_14]) ).
fof(sk_sos_14_sk,plain,
! [X44,X45] :
( ( ! [X46] :
( ~ occurrence_of(X44,X46)
| ~ atomic(X46)
| ~ subactivity(X45,X46) )
| atocc(X44,X45) )
& ( ( occurrence_of(X44,sK9(X44,X45))
& atomic(sK9(X44,X45))
& subactivity(X45,sK9(X44,X45)) )
| ~ atocc(X44,X45) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(X136,sK9(X44,X45))],[nnf_15]) ).
fof(sk_sos_14,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( ~ occurrence_of(VAR_0,VAR_2)
| ~ atomic(VAR_2)
| ~ subactivity(VAR_1,VAR_2)
| atocc(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( occurrence_of(VAR_0,sK9(VAR_0,VAR_1))
| ~ atocc(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( atomic(sK9(VAR_0,VAR_1))
| ~ atocc(VAR_0,VAR_1) )
& ! [VAR_0,VAR_1] :
( subactivity(VAR_1,sK9(VAR_0,VAR_1))
| ~ atocc(VAR_0,VAR_1) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_14_sk]) ).
cnf(c_188,plain,
( occurrence_of(A,sK9(A,B))
| ~ atocc(A,B) ),
inference(split_conjunct,[status(thm)],[sk_sos_14]) ).
cnf(c_194,plain,
( subactivity_occurrence(A,B)
| ~ root_occ(A,B) ),
inference(clausify,[status(thm)],[sos_19]) ).
cnf(c_201,plain,
( D = C
| ~ root_occ(D,A)
| ~ root_occ(C,A)
| ~ occurrence_of(A,B) ),
inference(clausify,[status(thm)],[sos_29]) ).
cnf(c_205,plain,
( root_occ(sK3(A),A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
cnf(c_206,plain,
( occurrence_of(sK4(A),tptp2)
| occurrence_of(sK4(A),tptp3)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
cnf(c_207,plain,
( leaf_occ(sK4(A),A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
cnf(c_220,plain,
( ~ atomic(A)
| ~ tptp1(A,B,C) ),
inference(clausify,[status(thm)],[sos_48]) ).
cnf(c_222,plain,
( occurrence_of(sK10(A,B,C,D),sK5(A,B,C,D))
| ~ occurrence_of(D,A)
| ~ tptp1(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
cnf(c_223,plain,
( root_occ(sK10(A,B,C,D),D)
| ~ occurrence_of(D,A)
| ~ tptp1(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sos_49]) ).
fof(nnf_40,plain,
? [X133,X134,X135] :
( occurrence_of(X135,X133)
& tptp1(X133,tptp0,X134) ),
inference(fof_nnf,[status(thm)],[goals_neg]) ).
fof(sk_goals_neg,plain,
( occurrence_of(sK13,sK11)
& tptp1(sK11,tptp0,sK12) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12,sK13]),skolemize(X133,sK11),skolemize(X134,sK12),skolemize(X135,sK13)],[nnf_40]) ).
cnf(c_225,negated_conjecture,
tptp1(sK11,tptp0,sK12),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_226,negated_conjecture,
occurrence_of(sK13,sK11),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_227,plain,
( atomic(A)
| ~ occurrence_of(B,A)
| atocc(sK0(A,B),sK1(A,sK0(A,B))) ),
inference(resolve,[status(thm)],[c_43,c_42]) ).
cnf(c_230,plain,
( atomic(A)
| ~ occurrence_of(B,A)
| ~ subactivity_occurrence(sK0(A,B),C)
| ~ occurrence_of(C,A)
| root_occ(sK0(A,B),C) ),
inference(resolve,[status(thm)],[c_48,c_42]) ).
cnf(c_236,plain,
( ~ min_precedes(D,C,B)
| ~ tptp1(A,B,C) ),
inference(resolve,[status(thm)],[c_53,c_49]) ).
cnf(c_240,plain,
( ~ subactivity_occurrence(A,B)
| occurrence_of(A,sK2(A)) ),
inference(resolve,[status(thm)],[c_54,c_56]) ).
cnf(c_282,plain,
( ~ min_precedes(B,sK4(A),tptp0)
| ~ min_precedes(sK3(A),B,tptp0)
| ~ occurrence_of(A,tptp0) ),
inference(resolve,[status(thm)],[c_106,c_101]) ).
cnf(c_285,plain,
( arboreal(sK3(A))
| ~ occurrence_of(A,tptp0) ),
inference(resolve,[status(thm)],[c_106,c_104]) ).
cnf(c_288,plain,
( atomic(A)
| ~ subactivity_occurrence(sK0(A,B),B)
| ~ occurrence_of(B,A)
| root_occ(sK0(A,B),B) ),
inference(factor,[status(thm)],[c_230]) ).
cnf(c_314,plain,
( root_occ(sK10(sK11,tptp0,sK12,A),A)
| ~ occurrence_of(A,sK11) ),
inference(resolve,[status(thm)],[c_225,c_223]) ).
cnf(c_315,plain,
( occurrence_of(sK10(sK11,tptp0,sK12,A),sK5(sK11,tptp0,sK12,A))
| ~ occurrence_of(A,sK11) ),
inference(resolve,[status(thm)],[c_225,c_222]) ).
cnf(c_316,plain,
~ atomic(sK11),
inference(resolve,[status(thm)],[c_225,c_220]) ).
cnf(c_318,plain,
arboreal(sK12),
inference(resolve,[status(thm)],[c_225,c_161]) ).
cnf(c_326,plain,
( ~ occurrence_of(B,sK11)
| min_precedes(sK12,A,tptp0)
| ~ occurrence_of(A,sK5(sK11,tptp0,sK12,B)) ),
inference(resolve,[status(thm)],[c_225,c_144]) ).
cnf(c_327,plain,
( ~ occurrence_of(A,sK11)
| sK5(sK11,tptp0,sK12,A) != tptp2 ),
inference(resolve,[status(thm)],[c_225,c_143]) ).
cnf(c_328,plain,
( ~ occurrence_of(A,sK11)
| sK5(sK11,tptp0,sK12,A) != tptp3 ),
inference(resolve,[status(thm)],[c_225,c_142]) ).
cnf(c_336,plain,
( B = A
| ~ root_occ(B,sK13)
| ~ root_occ(A,sK13) ),
inference(resolve,[status(thm)],[c_226,c_201]) ).
cnf(c_2851,negated_conjecture,
( subactivity_occurrence(sK0(sK11,sK13),sK13)
| atomic(sK11) ),
inference(resolve,[status(thm)],[c_226,c_177]) ).
cnf(c_346,negated_conjecture,
subactivity_occurrence(sK0(sK11,sK13),sK13),
inference(resolve,[status(thm)],[c_316,c_2851]) ).
cnf(c_2852,negated_conjecture,
( atomic(sK11)
| arboreal(sK0(sK11,sK13)) ),
inference(resolve,[status(thm)],[c_226,c_164]) ).
cnf(c_348,negated_conjecture,
arboreal(sK0(sK11,sK13)),
inference(resolve,[status(thm)],[c_316,c_2852]) ).
cnf(c_2853,negated_conjecture,
( atomic(sK11)
| atocc(sK0(sK11,sK13),sK1(sK11,sK0(sK11,sK13))) ),
inference(resolve,[status(thm)],[c_227,c_226]) ).
cnf(c_364,negated_conjecture,
atocc(sK0(sK11,sK13),sK1(sK11,sK0(sK11,sK13))),
inference(resolve,[status(thm)],[c_316,c_2853]) ).
cnf(c_369,plain,
~ min_precedes(A,sK12,tptp0),
inference(resolve,[status(thm)],[c_236,c_225]) ).
cnf(c_2854,negated_conjecture,
( atomic(sK11)
| ~ subactivity_occurrence(sK0(sK11,sK13),sK13)
| root_occ(sK0(sK11,sK13),sK13) ),
inference(resolve,[status(thm)],[c_288,c_226]) ).
cnf(c_2855,negated_conjecture,
( atomic(sK11)
| root_occ(sK0(sK11,sK13),sK13) ),
inference(resolve,[status(thm)],[c_346,c_2854]) ).
cnf(c_386,negated_conjecture,
root_occ(sK0(sK11,sK13),sK13),
inference(resolve,[status(thm)],[c_316,c_2855]) ).
cnf(c_389,plain,
( sK12 = C
| min_precedes(sK12,C,B)
| min_precedes(C,sK12,B)
| ~ subactivity_occurrence(sK12,A)
| ~ subactivity_occurrence(C,A)
| ~ arboreal(C)
| ~ occurrence_of(A,B) ),
inference(resolve,[status(thm)],[c_318,c_180]) ).
cnf(c_391,plain,
root_occ(sK10(sK11,tptp0,sK12,sK13),sK13),
inference(resolve,[status(thm)],[c_314,c_226]) ).
cnf(c_392,plain,
occurrence_of(sK10(sK11,tptp0,sK12,sK13),sK5(sK11,tptp0,sK12,sK13)),
inference(resolve,[status(thm)],[c_315,c_226]) ).
cnf(c_394,plain,
sK5(sK11,tptp0,sK12,sK13) != tptp2,
inference(resolve,[status(thm)],[c_327,c_226]) ).
cnf(c_2856,plain,
( C = sK0(sK11,sK13)
| min_precedes(sK0(sK11,sK13),C,B)
| ~ leaf_occ(C,A)
| ~ subactivity_occurrence(sK0(sK11,sK13),A)
| ~ occurrence_of(A,B) ),
inference(resolve,[status(thm)],[c_348,c_179]) ).
cnf(c_397,plain,
( sK0(sK11,sK13) = C
| min_precedes(sK0(sK11,sK13),C,B)
| ~ leaf_occ(C,A)
| ~ subactivity_occurrence(sK0(sK11,sK13),A)
| ~ occurrence_of(A,B) ),
inference(copy,[status(thm)],[c_2856]) ).
cnf(c_403,plain,
occurrence_of(sK0(sK11,sK13),sK2(sK0(sK11,sK13))),
inference(resolve,[status(thm)],[c_346,c_240]) ).
cnf(c_410,plain,
sK5(sK11,tptp0,sK12,sK13) != tptp3,
inference(resolve,[status(thm)],[c_328,c_226]) ).
cnf(c_415,plain,
( sK0(sK11,sK13) = A
| ~ root_occ(A,sK13) ),
inference(resolve,[status(thm)],[c_386,c_336]) ).
cnf(c_2857,plain,
sK0(sK11,sK13) = sK10(sK11,tptp0,sK12,sK13),
inference(resolve,[status(thm)],[c_415,c_391]) ).
cnf(c_455,plain,
sK10(sK11,tptp0,sK12,sK13) = sK0(sK11,sK13),
inference(copy,[status(thm)],[c_2857]) ).
cnf(c_456,plain,
occurrence_of(sK0(sK11,sK13),sK5(sK11,tptp0,sK12,sK13)),
inference(paramod,[status(thm)],[c_455,c_392]) ).
cnf(c_2858,plain,
( ~ occurrence_of(sK13,sK11)
| min_precedes(sK12,sK0(sK11,sK13),tptp0) ),
inference(resolve,[status(thm)],[c_456,c_326]) ).
cnf(c_469,negated_conjecture,
min_precedes(sK12,sK0(sK11,sK13),tptp0),
inference(resolve,[status(thm)],[c_226,c_2858]) ).
cnf(c_477,plain,
( sK5(sK11,tptp0,sK12,sK13) = A
| ~ occurrence_of(sK0(sK11,sK13),A) ),
inference(resolve,[status(thm)],[c_456,c_184]) ).
cnf(c_511,plain,
subactivity_occurrence(sK0(sK11,sK13),sK8(tptp0,sK12,sK0(sK11,sK13))),
inference(resolve,[status(thm)],[c_469,c_183]) ).
cnf(c_512,plain,
subactivity_occurrence(sK12,sK8(tptp0,sK12,sK0(sK11,sK13))),
inference(resolve,[status(thm)],[c_469,c_182]) ).
cnf(c_513,plain,
occurrence_of(sK8(tptp0,sK12,sK0(sK11,sK13)),tptp0),
inference(resolve,[status(thm)],[c_469,c_181]) ).
cnf(c_630,plain,
occurrence_of(sK0(sK11,sK13),sK9(sK0(sK11,sK13),sK1(sK11,sK0(sK11,sK13)))),
inference(resolve,[status(thm)],[c_364,c_188]) ).
cnf(c_646,plain,
sK5(sK11,tptp0,sK12,sK13) = sK2(sK0(sK11,sK13)),
inference(resolve,[status(thm)],[c_403,c_477]) ).
cnf(c_659,plain,
( sK2(sK0(sK11,sK13)) = A
| ~ occurrence_of(sK0(sK11,sK13),A) ),
inference(resolve,[status(thm)],[c_403,c_184]) ).
cnf(c_682,plain,
sK2(sK0(sK11,sK13)) != tptp3,
inference(paramod,[status(thm)],[c_646,c_410]) ).
cnf(c_683,plain,
sK2(sK0(sK11,sK13)) != tptp2,
inference(paramod,[status(thm)],[c_646,c_394]) ).
cnf(c_739,plain,
arboreal(sK3(sK8(tptp0,sK12,sK0(sK11,sK13)))),
inference(resolve,[status(thm)],[c_513,c_285]) ).
cnf(c_742,plain,
( ~ min_precedes(A,sK4(sK8(tptp0,sK12,sK0(sK11,sK13))),tptp0)
| ~ min_precedes(sK3(sK8(tptp0,sK12,sK0(sK11,sK13))),A,tptp0) ),
inference(resolve,[status(thm)],[c_513,c_282]) ).
cnf(c_757,plain,
leaf_occ(sK4(sK8(tptp0,sK12,sK0(sK11,sK13))),sK8(tptp0,sK12,sK0(sK11,sK13))),
inference(resolve,[status(thm)],[c_513,c_207]) ).
cnf(c_758,plain,
( occurrence_of(sK4(sK8(tptp0,sK12,sK0(sK11,sK13))),tptp2)
| occurrence_of(sK4(sK8(tptp0,sK12,sK0(sK11,sK13))),tptp3) ),
inference(resolve,[status(thm)],[c_513,c_206]) ).
cnf(c_759,plain,
root_occ(sK3(sK8(tptp0,sK12,sK0(sK11,sK13))),sK8(tptp0,sK12,sK0(sK11,sK13))),
inference(resolve,[status(thm)],[c_513,c_205]) ).
cnf(c_765,plain,
( ~ min_precedes(B,A,tptp0)
| ~ root_occ(A,sK8(tptp0,sK12,sK0(sK11,sK13))) ),
inference(resolve,[status(thm)],[c_513,c_186]) ).
cnf(c_2859,plain,
( sK12 = A
| min_precedes(sK12,A,tptp0)
| min_precedes(A,sK12,tptp0)
| ~ subactivity_occurrence(sK12,sK8(tptp0,sK12,sK0(sK11,sK13)))
| ~ subactivity_occurrence(A,sK8(tptp0,sK12,sK0(sK11,sK13)))
| ~ arboreal(A) ),
inference(resolve,[status(thm)],[c_389,c_513]) ).
cnf(c_2860,plain,
( sK12 = A
| min_precedes(sK12,A,tptp0)
| min_precedes(A,sK12,tptp0)
| ~ subactivity_occurrence(A,sK8(tptp0,sK12,sK0(sK11,sK13)))
| ~ arboreal(A) ),
inference(resolve,[status(thm)],[c_512,c_2859]) ).
cnf(c_948,plain,
( sK12 = A
| min_precedes(sK12,A,tptp0)
| ~ subactivity_occurrence(A,sK8(tptp0,sK12,sK0(sK11,sK13)))
| ~ arboreal(A) ),
inference(resolve,[status(thm)],[c_369,c_2860]) ).
cnf(c_2861,plain,
( sK0(sK11,sK13) = A
| min_precedes(sK0(sK11,sK13),A,tptp0)
| ~ leaf_occ(A,sK8(tptp0,sK12,sK0(sK11,sK13)))
| ~ subactivity_occurrence(sK0(sK11,sK13),sK8(tptp0,sK12,sK0(sK11,sK13))) ),
inference(resolve,[status(thm)],[c_397,c_513]) ).
cnf(c_969,plain,
( sK0(sK11,sK13) = A
| min_precedes(sK0(sK11,sK13),A,tptp0)
| ~ leaf_occ(A,sK8(tptp0,sK12,sK0(sK11,sK13))) ),
inference(resolve,[status(thm)],[c_511,c_2861]) ).
cnf(c_1924,plain,
sK2(sK0(sK11,sK13)) = sK9(sK0(sK11,sK13),sK1(sK11,sK0(sK11,sK13))),
inference(resolve,[status(thm)],[c_630,c_659]) ).
cnf(c_1943,plain,
sK9(sK0(sK11,sK13),sK1(sK11,sK0(sK11,sK13))) != tptp2,
inference(paramod,[status(thm)],[c_1924,c_683]) ).
cnf(c_1944,plain,
sK9(sK0(sK11,sK13),sK1(sK11,sK0(sK11,sK13))) != tptp3,
inference(paramod,[status(thm)],[c_1924,c_682]) ).
cnf(c_2862,plain,
( sK12 = sK3(sK8(tptp0,sK12,sK0(sK11,sK13)))
| min_precedes(sK12,sK3(sK8(tptp0,sK12,sK0(sK11,sK13))),tptp0)
| ~ subactivity_occurrence(sK3(sK8(tptp0,sK12,sK0(sK11,sK13))),sK8(tptp0,sK12,sK0(sK11,sK13))) ),
inference(resolve,[status(thm)],[c_948,c_739]) ).
cnf(c_2033,plain,
( sK3(sK8(tptp0,sK12,sK0(sK11,sK13))) = sK12
| min_precedes(sK12,sK3(sK8(tptp0,sK12,sK0(sK11,sK13))),tptp0)
| ~ subactivity_occurrence(sK3(sK8(tptp0,sK12,sK0(sK11,sK13))),sK8(tptp0,sK12,sK0(sK11,sK13))) ),
inference(copy,[status(thm)],[c_2862]) ).
cnf(c_2378,plain,
~ min_precedes(A,sK3(sK8(tptp0,sK12,sK0(sK11,sK13))),tptp0),
inference(resolve,[status(thm)],[c_759,c_765]) ).
cnf(c_2384,plain,
subactivity_occurrence(sK3(sK8(tptp0,sK12,sK0(sK11,sK13))),sK8(tptp0,sK12,sK0(sK11,sK13))),
inference(resolve,[status(thm)],[c_759,c_194]) ).
cnf(c_2863,plain,
( sK3(sK8(tptp0,sK12,sK0(sK11,sK13))) = sK12
| min_precedes(sK12,sK3(sK8(tptp0,sK12,sK0(sK11,sK13))),tptp0) ),
inference(resolve,[status(thm)],[c_2384,c_2033]) ).
cnf(c_2390,plain,
sK3(sK8(tptp0,sK12,sK0(sK11,sK13))) = sK12,
inference(resolve,[status(thm)],[c_2378,c_2863]) ).
cnf(c_2411,plain,
( ~ min_precedes(A,sK4(sK8(tptp0,sK12,sK0(sK11,sK13))),tptp0)
| ~ min_precedes(sK12,A,tptp0) ),
inference(paramod,[status(thm)],[c_2390,c_742]) ).
cnf(c_2449,plain,
~ min_precedes(sK0(sK11,sK13),sK4(sK8(tptp0,sK12,sK0(sK11,sK13))),tptp0),
inference(resolve,[status(thm)],[c_2411,c_469]) ).
cnf(c_2542,plain,
( tptp3 = A
| ~ occurrence_of(sK4(sK8(tptp0,sK12,sK0(sK11,sK13))),A)
| occurrence_of(sK4(sK8(tptp0,sK12,sK0(sK11,sK13))),tptp2) ),
inference(resolve,[status(thm)],[c_758,c_184]) ).
cnf(c_2864,plain,
( sK0(sK11,sK13) = sK4(sK8(tptp0,sK12,sK0(sK11,sK13)))
| min_precedes(sK0(sK11,sK13),sK4(sK8(tptp0,sK12,sK0(sK11,sK13))),tptp0) ),
inference(resolve,[status(thm)],[c_969,c_757]) ).
cnf(c_2865,plain,
( sK4(sK8(tptp0,sK12,sK0(sK11,sK13))) = sK0(sK11,sK13)
| min_precedes(sK0(sK11,sK13),sK4(sK8(tptp0,sK12,sK0(sK11,sK13))),tptp0) ),
inference(copy,[status(thm)],[c_2864]) ).
cnf(c_2661,plain,
sK4(sK8(tptp0,sK12,sK0(sK11,sK13))) = sK0(sK11,sK13),
inference(resolve,[status(thm)],[c_2449,c_2865]) ).
cnf(c_2866,plain,
( tptp3 = A
| ~ occurrence_of(sK4(sK8(tptp0,sK12,sK0(sK11,sK13))),A)
| occurrence_of(sK0(sK11,sK13),tptp2) ),
inference(paramod,[status(thm)],[c_2661,c_2542]) ).
cnf(c_2668,plain,
( tptp3 = A
| ~ occurrence_of(sK0(sK11,sK13),A)
| occurrence_of(sK0(sK11,sK13),tptp2) ),
inference(paramod,[status(thm)],[c_2661,c_2866]) ).
cnf(c_2867,plain,
( tptp3 = sK9(sK0(sK11,sK13),sK1(sK11,sK0(sK11,sK13)))
| occurrence_of(sK0(sK11,sK13),tptp2) ),
inference(resolve,[status(thm)],[c_2668,c_630]) ).
cnf(c_2868,plain,
( sK9(sK0(sK11,sK13),sK1(sK11,sK0(sK11,sK13))) = tptp3
| occurrence_of(sK0(sK11,sK13),tptp2) ),
inference(copy,[status(thm)],[c_2867]) ).
cnf(c_2830,plain,
occurrence_of(sK0(sK11,sK13),tptp2),
inference(resolve,[status(thm)],[c_1944,c_2868]) ).
cnf(c_2846,plain,
( tptp2 = A
| ~ occurrence_of(sK0(sK11,sK13),A) ),
inference(resolve,[status(thm)],[c_2830,c_184]) ).
cnf(c_2869,plain,
tptp2 = sK9(sK0(sK11,sK13),sK1(sK11,sK0(sK11,sK13))),
inference(resolve,[status(thm)],[c_2846,c_630]) ).
cnf(c_2870,plain,
sK9(sK0(sK11,sK13),sK1(sK11,sK0(sK11,sK13))) = tptp2,
inference(copy,[status(thm)],[c_2869]) ).
cnf(c_2850,plain,
$false,
inference(resolve,[status(thm)],[c_1943,c_2870]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PRO002+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n019.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 04:54:49 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 434301 was started by sandbox2 on n019,
% 0.09/0.37 % Sat Sep 26 04:54:49 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.39
% 0.09/0.39 % From the command line: assign(max_seconds, 300).
% 3.97/0.98
% 3.97/0.98 % given #500 (A,wt=31): 561 precedes(A,f11(c2,f8(c2,tptp0),tptp0)) | -earlier(A,f11(c2,f8(c2,tptp0),tptp0)). [resolve(528,a,170,c)].
% 3.97/0.98
% 3.97/0.98 % SZS status Theorem for theBenchmark
% 3.97/0.98
% 3.97/0.98 % Proof 1 at 0.43 (+ 0.10) seconds.
% 3.97/0.98 % Length of proof is 128.
% 3.97/0.98 % Level of proof is 19.
% 3.97/0.98 % Maximum clause weight is 53.000.
% 3.97/0.98 % Given clauses 770.
% 3.97/0.98
% 3.97/0.98 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------