%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LCL672+1.001 : 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 : n015.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 07:59:27 AM UTC 2026
% Result : Theorem 2.41s 0.72s
% Output : CNFRefutation 2.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 2
% Syntax : Number of formulae : 38 ( 14 unt; 0 def)
% Number of atoms : 406 ( 0 equ)
% Maximal formula atoms : 90 ( 10 avg)
% Number of connectives : 665 ( 297 ~; 297 |; 71 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-3 aty)
% Number of variables : 215 ( 0 sgn 147 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(reflexivity,axiom,
! [X] : r1(X,X),
file('theBenchmark.p',reflexivity) ).
fof(main,conjecture,
~ ? [X] :
~ ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ! [X] : ~ r1(Y,X)
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p1(Y)
& ~ ! [X] :
( ~ ! [Y] :
( ~ p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) ) ),
file('theBenchmark.p',main) ).
fof(main_neg,negated_conjecture,
~ ~ ? [X] :
~ ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ! [X] : ~ r1(Y,X)
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p1(Y)
& ~ ! [X] :
( ~ ! [Y] :
( ~ p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) ) ),
inference(assume_negation,[status(cth)],[main]) ).
fof(nnf_3,plain,
? [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [X25] :
( ? [X28] :
( ~ p1(X28)
& r1(X25,X28) )
& ? [X26] :
( ! [X27] :
( p1(X27)
| ~ r1(X26,X27) )
& r1(X25,X26) )
& r1(X,X25) )
& ? [X24] :
( ~ p2(X24)
& r1(X,X24) )
& ( ! [X23] :
( p1(X23)
| ~ r1(X,X23) )
| ! [X21] :
( ? [X22] : r1(X21,X22)
| ~ r1(X,X21) )
| ! [X20] :
( p2(X20)
| ~ r1(X,X20) ) )
& ( ! [X19] :
( p1(X19)
| ~ r1(X,X19) )
| ! [X13] :
( ! [X17] :
( ? [X18] :
( ~ p1(X18)
& r1(X17,X18) )
| ~ r1(X13,X17) )
| ! [X14] :
( ? [X15] :
( ! [X16] :
( p1(X16)
| ~ r1(X15,X16) )
& r1(X14,X15) )
| ~ r1(X13,X14) )
| ~ r1(X,X13) )
| ! [X12] :
( p2(X12)
| ~ r1(X,X12) ) )
& ( ! [X11] :
( p1(X11)
| ~ r1(X,X11) )
| ! [X6] :
( ! [X7] :
( ! [X10] :
( p1(X10)
| ~ r1(X7,X10) )
| ! [X8] :
( ? [X9] :
( ~ p1(X9)
& r1(X8,X9) )
| ~ r1(X7,X8) )
| ~ r1(X6,X7) )
| ~ r1(X,X6) )
| ! [X5] :
( p2(X5)
| ~ r1(X,X5) ) )
& ( ! [X4] :
( p1(X4)
| ~ r1(X,X4) )
| ! [X1] :
( ~ p1(X1)
| ! [X2] :
( ? [X3] :
( p1(X3)
& r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X,X1) )
| ! [X0] :
( p2(X0)
| ~ r1(X,X0) ) ) ),
inference(fof_nnf,[status(thm)],[main_neg]) ).
fof(sk_main_neg_sk,plain,
( ~ p1(sK3)
& r1(sK1,sK3)
& ~ p1(sK4)
& r1(sK5,sK4)
& ! [X27] :
( p1(X27)
| ~ r1(sK6,X27) )
& r1(sK5,sK6)
& r1(sK1,sK5)
& ~ p2(sK0)
& r1(sK1,sK0)
& ( ! [X23] :
( p1(X23)
| ~ r1(sK1,X23) )
| ! [X21] :
( r1(X21,sK10(X21))
| ~ r1(sK1,X21) )
| ! [X20] :
( p2(X20)
| ~ r1(sK1,X20) ) )
& ( ! [X19] :
( p1(X19)
| ~ r1(sK1,X19) )
| ! [X13] :
( ! [X17] :
( ( ~ p1(sK9(X13,X17))
& r1(X17,sK9(X13,X17)) )
| ~ r1(X13,X17) )
| ! [X14] :
( ( ! [X16] :
( p1(X16)
| ~ r1(sK8(X13,X14),X16) )
& r1(X14,sK8(X13,X14)) )
| ~ r1(X13,X14) )
| ~ r1(sK1,X13) )
| ! [X12] :
( p2(X12)
| ~ r1(sK1,X12) ) )
& ( ! [X11] :
( p1(X11)
| ~ r1(sK1,X11) )
| ! [X6] :
( ! [X7] :
( ! [X10] :
( p1(X10)
| ~ r1(X7,X10) )
| ! [X8] :
( ( ~ p1(sK2(X6,X7,X8))
& r1(X8,sK2(X6,X7,X8)) )
| ~ r1(X7,X8) )
| ~ r1(X6,X7) )
| ~ r1(sK1,X6) )
| ! [X5] :
( p2(X5)
| ~ r1(sK1,X5) ) )
& ( ! [X4] :
( p1(X4)
| ~ r1(sK1,X4) )
| ! [X1] :
( ~ p1(X1)
| ! [X2] :
( ( p1(sK7(X1,X2))
& r1(X2,sK7(X1,X2)) )
| ~ r1(X1,X2) )
| ~ r1(sK1,X1) )
| ! [X0] :
( p2(X0)
| ~ r1(sK1,X0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK7,sK2,sK8,sK9,sK10,sK0,sK5,sK6,sK4,sK3]),skolemize(X,sK1),skolemize(X3,sK7(X1,X2)),skolemize(X9,sK2(X6,X7,X8)),skolemize(X15,sK8(X13,X14)),skolemize(X18,sK9(X13,X17)),skolemize(X22,sK10(X21)),skolemize(X24,sK0),skolemize(X25,sK5),skolemize(X26,sK6),skolemize(X28,sK4),skolemize(Y,sK3)],[nnf_3]) ).
fof(sk_main_neg,plain,
( ~ p1(sK3)
& r1(sK1,sK3)
& ~ p1(sK4)
& r1(sK5,sK4)
& ! [VAR_0] :
( p1(VAR_0)
| ~ r1(sK6,VAR_0) )
& r1(sK5,sK6)
& r1(sK1,sK5)
& ~ p2(sK0)
& r1(sK1,sK0)
& ! [VAR_0,VAR_1,VAR_2] :
( p1(VAR_2)
| ~ r1(sK1,VAR_2)
| r1(VAR_1,sK10(VAR_1))
| ~ r1(sK1,VAR_1)
| p2(VAR_0)
| ~ r1(sK1,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( p1(VAR_5)
| ~ r1(sK1,VAR_5)
| ~ p1(sK9(VAR_1,VAR_4))
| ~ r1(VAR_1,VAR_4)
| p1(VAR_3)
| ~ r1(sK8(VAR_1,VAR_2),VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(sK1,VAR_1)
| p2(VAR_0)
| ~ r1(sK1,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( p1(VAR_5)
| ~ r1(sK1,VAR_5)
| r1(VAR_4,sK9(VAR_1,VAR_4))
| ~ r1(VAR_1,VAR_4)
| p1(VAR_3)
| ~ r1(sK8(VAR_1,VAR_2),VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(sK1,VAR_1)
| p2(VAR_0)
| ~ r1(sK1,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( p1(VAR_4)
| ~ r1(sK1,VAR_4)
| ~ p1(sK9(VAR_1,VAR_3))
| ~ r1(VAR_1,VAR_3)
| r1(VAR_2,sK8(VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(sK1,VAR_1)
| p2(VAR_0)
| ~ r1(sK1,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( p1(VAR_4)
| ~ r1(sK1,VAR_4)
| r1(VAR_3,sK9(VAR_1,VAR_3))
| ~ r1(VAR_1,VAR_3)
| r1(VAR_2,sK8(VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(sK1,VAR_1)
| p2(VAR_0)
| ~ r1(sK1,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( p1(VAR_5)
| ~ r1(sK1,VAR_5)
| p1(VAR_4)
| ~ r1(VAR_2,VAR_4)
| ~ p1(sK2(VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(sK1,VAR_1)
| p2(VAR_0)
| ~ r1(sK1,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( p1(VAR_5)
| ~ r1(sK1,VAR_5)
| p1(VAR_4)
| ~ r1(VAR_2,VAR_4)
| r1(VAR_3,sK2(VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(sK1,VAR_1)
| p2(VAR_0)
| ~ r1(sK1,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p1(VAR_3)
| ~ r1(sK1,VAR_3)
| ~ p1(VAR_1)
| p1(sK7(VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(sK1,VAR_1)
| p2(VAR_0)
| ~ r1(sK1,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p1(VAR_3)
| ~ r1(sK1,VAR_3)
| ~ p1(VAR_1)
| r1(VAR_2,sK7(VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(sK1,VAR_1)
| p2(VAR_0)
| ~ r1(sK1,VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_main_neg_sk]) ).
cnf(c_4,negated_conjecture,
~ p2(sK0),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_10,negated_conjecture,
( p1(F)
| ~ r1(sK1,F)
| p1(E)
| ~ r1(C,E)
| ~ p1(sK2(B,C,D))
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(sK1,B)
| p2(A)
| ~ r1(sK1,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_11,negated_conjecture,
( p1(F)
| ~ r1(sK1,F)
| p1(E)
| ~ r1(C,E)
| r1(D,sK2(B,C,D))
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(sK1,B)
| p2(A)
| ~ r1(sK1,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_16,negated_conjecture,
( p1(E)
| ~ r1(sK1,E)
| p1(D)
| ~ r1(B,D)
| r1(C,sK2(A,B,C))
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK1,A)
| ~ r1(sK1,sK0) ),
inference(resolve,[status(thm)],[c_4,c_11]) ).
cnf(c_17,negated_conjecture,
( p1(E)
| ~ r1(sK1,E)
| p1(D)
| ~ r1(B,D)
| ~ p1(sK2(A,B,C))
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK1,A)
| ~ r1(sK1,sK0) ),
inference(resolve,[status(thm)],[c_4,c_10]) ).
cnf(c_23,negated_conjecture,
~ p1(sK3),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_24,negated_conjecture,
r1(sK1,sK3),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_25,negated_conjecture,
~ p1(sK4),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_26,negated_conjecture,
r1(sK5,sK4),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_27,negated_conjecture,
( p1(A)
| ~ r1(sK6,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_28,negated_conjecture,
r1(sK5,sK6),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_29,negated_conjecture,
r1(sK1,sK5),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_30,negated_conjecture,
r1(sK1,sK0),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_32,plain,
r1(A,A),
inference(clausify,[status(thm)],[reflexivity]) ).
cnf(c_124,negated_conjecture,
( p1(E)
| ~ r1(sK1,E)
| p1(D)
| ~ r1(B,D)
| ~ p1(sK2(A,B,C))
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK1,A) ),
inference(resolve,[status(thm)],[c_30,c_17]) ).
cnf(c_125,negated_conjecture,
( p1(E)
| ~ r1(sK1,E)
| p1(D)
| ~ r1(B,D)
| r1(C,sK2(A,B,C))
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK1,A) ),
inference(resolve,[status(thm)],[c_30,c_16]) ).
cnf(c_1748,negated_conjecture,
( p1(D)
| ~ r1(sK1,D)
| p1(C)
| ~ r1(A,C)
| ~ p1(sK2(sK1,A,B))
| ~ r1(A,B)
| ~ r1(sK1,A) ),
inference(resolve,[status(thm)],[c_124,c_32]) ).
cnf(c_1749,negated_conjecture,
( p1(C)
| ~ r1(sK1,C)
| p1(B)
| ~ r1(sK5,B)
| ~ p1(sK2(sK1,sK5,A))
| ~ r1(sK5,A) ),
inference(resolve,[status(thm)],[c_1748,c_29]) ).
cnf(c_1750,negated_conjecture,
( p1(B)
| ~ r1(sK1,B)
| p1(A)
| ~ r1(sK5,A)
| ~ p1(sK2(sK1,sK5,sK6)) ),
inference(resolve,[status(thm)],[c_1749,c_28]) ).
cnf(c_1751,negated_conjecture,
( p1(A)
| ~ r1(sK1,A)
| p1(sK4)
| ~ p1(sK2(sK1,sK5,sK6)) ),
inference(resolve,[status(thm)],[c_1750,c_26]) ).
cnf(c_1752,negated_conjecture,
( p1(A)
| ~ r1(sK1,A)
| ~ p1(sK2(sK1,sK5,sK6)) ),
inference(resolve,[status(thm)],[c_1751,c_25]) ).
cnf(c_1753,negated_conjecture,
( p1(sK3)
| ~ p1(sK2(sK1,sK5,sK6)) ),
inference(resolve,[status(thm)],[c_1752,c_24]) ).
cnf(c_1566,negated_conjecture,
~ p1(sK2(sK1,sK5,sK6)),
inference(resolve,[status(thm)],[c_1753,c_23]) ).
cnf(c_1754,negated_conjecture,
( p1(D)
| ~ r1(sK1,D)
| p1(C)
| ~ r1(A,C)
| r1(B,sK2(sK1,A,B))
| ~ r1(A,B)
| ~ r1(sK1,A) ),
inference(resolve,[status(thm)],[c_125,c_32]) ).
cnf(c_1755,negated_conjecture,
( p1(C)
| ~ r1(sK1,C)
| p1(B)
| ~ r1(sK5,B)
| r1(A,sK2(sK1,sK5,A))
| ~ r1(sK5,A) ),
inference(resolve,[status(thm)],[c_1754,c_29]) ).
cnf(c_1756,negated_conjecture,
( p1(B)
| ~ r1(sK1,B)
| p1(A)
| ~ r1(sK5,A)
| r1(sK6,sK2(sK1,sK5,sK6)) ),
inference(resolve,[status(thm)],[c_1755,c_28]) ).
cnf(c_1757,negated_conjecture,
( p1(A)
| ~ r1(sK1,A)
| p1(sK4)
| r1(sK6,sK2(sK1,sK5,sK6)) ),
inference(resolve,[status(thm)],[c_1756,c_26]) ).
cnf(c_1758,negated_conjecture,
( p1(sK3)
| p1(sK4)
| r1(sK6,sK2(sK1,sK5,sK6)) ),
inference(resolve,[status(thm)],[c_1757,c_24]) ).
cnf(c_1759,negated_conjecture,
( p1(sK3)
| r1(sK6,sK2(sK1,sK5,sK6)) ),
inference(resolve,[status(thm)],[c_25,c_1758]) ).
cnf(c_1581,negated_conjecture,
r1(sK6,sK2(sK1,sK5,sK6)),
inference(resolve,[status(thm)],[c_23,c_1759]) ).
cnf(c_1760,negated_conjecture,
~ r1(sK6,sK2(sK1,sK5,sK6)),
inference(resolve,[status(thm)],[c_27,c_1566]) ).
cnf(c_1747,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1581,c_1760]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL672+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n015.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Fri Sep 25 23:15:42 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 2516905 was started by sandbox on n015,
% 0.09/0.37 % Fri Sep 25 23:15:42 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.38
% 0.09/0.38 % From the command line: assign(max_seconds, 300).
% 2.41/0.72
% 2.41/0.72 % Assigning unary symbol f5 kb_weight 0 and highest precedence (13).
% 2.41/0.72
% 2.41/0.72 % SZS status Theorem for theBenchmark
% 2.41/0.72
% 2.41/0.72 % Proof 1 at 0.25 (+ 0.07) seconds.
% 2.41/0.72 % Length of proof is 21.
% 2.41/0.72 % Level of proof is 5.
% 2.41/0.72 % Maximum clause weight is 38.000.
% 2.41/0.72 % Given clauses 156.
% 2.41/0.72
% 2.41/0.72 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------