%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT385+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 : n018.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:50:30 AM UTC 2026
% Result : Theorem 0.09s 0.45s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 3
% Syntax : Number of formulae : 18 ( 6 unt; 0 def)
% Number of atoms : 324 ( 9 equ)
% Maximal formula atoms : 159 ( 18 avg)
% Number of connectives : 430 ( 124 ~; 146 |; 140 &)
% ( 0 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 53 ( 10 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 4 con; 0-3 aty)
% Number of variables : 114 ( 1 sgn 101 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(m__1123,axiom,
( isOn0(xf,xU)
& szRzazndt0(xf) = xU
& szDzozmdt0(xf) = szRzazndt0(xf)
& isMonotone0(xf)
& ! [W0,W1] :
( ( aElementOf0(W1,szDzozmdt0(xf))
& aElementOf0(W0,szDzozmdt0(xf)) )
=> ( sdtlseqdt0(W0,W1)
=> sdtlseqdt0(sdtlpdtrp0(xf,W0),sdtlpdtrp0(xf,W1)) ) )
& aFunction0(xf)
& aCompleteLattice0(xU)
& ! [W0] :
( ( aSubsetOf0(W0,xU)
| ( ! [W1] :
( aElementOf0(W1,W0)
=> aElementOf0(W1,xU) )
& aSet0(W0) ) )
=> ? [W1] :
( ? [W2] :
( aSupremumOfIn0(W2,W0,xU)
& ! [W3] :
( ( aUpperBoundOfIn0(W3,W0,xU)
| ( ! [W4] :
( aElementOf0(W4,W0)
=> sdtlseqdt0(W4,W3) )
& aElementOf0(W3,xU) ) )
=> sdtlseqdt0(W2,W3) )
& aUpperBoundOfIn0(W2,W0,xU)
& ! [W3] :
( aElementOf0(W3,W0)
=> sdtlseqdt0(W3,W2) )
& aElementOf0(W2,xU)
& aElementOf0(W2,xU) )
& aInfimumOfIn0(W1,W0,xU)
& ! [W2] :
( ( aLowerBoundOfIn0(W2,W0,xU)
| ( ! [W3] :
( aElementOf0(W3,W0)
=> sdtlseqdt0(W2,W3) )
& aElementOf0(W2,xU) ) )
=> sdtlseqdt0(W2,W1) )
& aLowerBoundOfIn0(W1,W0,xU)
& ! [W2] :
( aElementOf0(W2,W0)
=> sdtlseqdt0(W1,W2) )
& aElementOf0(W1,xU)
& aElementOf0(W1,xU) ) )
& aSet0(xU) ),
file('theBenchmark.p',m__1123) ).
fof(m__1244,axiom,
( xP = cS1241(xU,xf,xT)
& ! [W0] :
( ( ( ( aUpperBoundOfIn0(W0,xT,xU)
| ! [W1] :
( aElementOf0(W1,xT)
=> sdtlseqdt0(W1,W0) ) )
& sdtlseqdt0(sdtlpdtrp0(xf,W0),W0)
& aElementOf0(W0,xU) )
=> aElementOf0(W0,xP) )
& ( aElementOf0(W0,xP)
=> ( aUpperBoundOfIn0(W0,xT,xU)
& ! [W1] :
( aElementOf0(W1,xT)
=> sdtlseqdt0(W1,W0) )
& sdtlseqdt0(sdtlpdtrp0(xf,W0),W0)
& aElementOf0(W0,xU) ) ) )
& aSet0(xP) ),
file('theBenchmark.p',m__1244) ).
fof(m__,conjecture,
? [W0] :
( aInfimumOfIn0(W0,xP,xU)
| ( ! [W1] :
( ( aLowerBoundOfIn0(W1,xP,xU)
& ! [W2] :
( aElementOf0(W2,xP)
=> sdtlseqdt0(W1,W2) )
& aElementOf0(W1,xU) )
=> sdtlseqdt0(W1,W0) )
& ( aLowerBoundOfIn0(W0,xP,xU)
| ( ! [W1] :
( aElementOf0(W1,xP)
=> sdtlseqdt0(W0,W1) )
& aElementOf0(W0,xU) ) )
& aElementOf0(W0,xU) ) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ? [W0] :
( aInfimumOfIn0(W0,xP,xU)
| ( ! [W1] :
( ( aLowerBoundOfIn0(W1,xP,xU)
& ! [W2] :
( aElementOf0(W2,xP)
=> sdtlseqdt0(W1,W2) )
& aElementOf0(W1,xU) )
=> sdtlseqdt0(W1,W0) )
& ( aLowerBoundOfIn0(W0,xP,xU)
| ( ! [W1] :
( aElementOf0(W1,xP)
=> sdtlseqdt0(W0,W1) )
& aElementOf0(W0,xU) ) )
& aElementOf0(W0,xU) ) ),
inference(assume_negation,[status(cth)],[m__]) ).
fof(nnf_24,plain,
( isOn0(xf,xU)
& szRzazndt0(xf) = xU
& szRzazndt0(xf) = szDzozmdt0(xf)
& isMonotone0(xf)
& ! [W0,W1] :
( sdtlseqdt0(sdtlpdtrp0(xf,W0),sdtlpdtrp0(xf,W1))
| ~ sdtlseqdt0(W0,W1)
| ~ aElementOf0(W1,szDzozmdt0(xf))
| ~ aElementOf0(W0,szDzozmdt0(xf)) )
& aFunction0(xf)
& aCompleteLattice0(xU)
& ! [X0] :
( ? [X2] :
( ? [W2] :
( aSupremumOfIn0(W2,X0,xU)
& ! [W3] :
( sdtlseqdt0(W2,W3)
| ( ~ aUpperBoundOfIn0(W3,X0,xU)
& ( ? [W4] :
( ~ sdtlseqdt0(W4,W3)
& aElementOf0(W4,X0) )
| ~ aElementOf0(W3,xU) ) ) )
& aUpperBoundOfIn0(W2,X0,xU)
& ! [X6] :
( sdtlseqdt0(X6,W2)
| ~ aElementOf0(X6,X0) )
& aElementOf0(W2,xU)
& aElementOf0(W2,xU) )
& aInfimumOfIn0(X2,X0,xU)
& ! [X4] :
( sdtlseqdt0(X4,X2)
| ( ~ aLowerBoundOfIn0(X4,X0,xU)
& ( ? [X5] :
( ~ sdtlseqdt0(X4,X5)
& aElementOf0(X5,X0) )
| ~ aElementOf0(X4,xU) ) ) )
& aLowerBoundOfIn0(X2,X0,xU)
& ! [X3] :
( sdtlseqdt0(X2,X3)
| ~ aElementOf0(X3,X0) )
& aElementOf0(X2,xU)
& aElementOf0(X2,xU) )
| ( ~ aSubsetOf0(X0,xU)
& ( ? [X1] :
( ~ aElementOf0(X1,xU)
& aElementOf0(X1,X0) )
| ~ aSet0(X0) ) ) )
& aSet0(xU) ),
inference(fof_nnf,[status(thm)],[m__1123]) ).
fof(sk_m__1123_sk,plain,
( isOn0(xf,xU)
& szRzazndt0(xf) = xU
& szRzazndt0(xf) = szDzozmdt0(xf)
& isMonotone0(xf)
& ! [W0,W1] :
( sdtlseqdt0(sdtlpdtrp0(xf,W0),sdtlpdtrp0(xf,W1))
| ~ sdtlseqdt0(W0,W1)
| ~ aElementOf0(W1,szDzozmdt0(xf))
| ~ aElementOf0(W0,szDzozmdt0(xf)) )
& aFunction0(xf)
& aCompleteLattice0(xU)
& ! [X0] :
( ( aSupremumOfIn0(sK3(X0),X0,xU)
& ! [W3] :
( sdtlseqdt0(sK3(X0),W3)
| ( ~ aUpperBoundOfIn0(W3,X0,xU)
& ( ( ~ sdtlseqdt0(sK4(X0,W3),W3)
& aElementOf0(sK4(X0,W3),X0) )
| ~ aElementOf0(W3,xU) ) ) )
& aUpperBoundOfIn0(sK3(X0),X0,xU)
& ! [X6] :
( sdtlseqdt0(X6,sK3(X0))
| ~ aElementOf0(X6,X0) )
& aElementOf0(sK3(X0),xU)
& aElementOf0(sK3(X0),xU)
& aInfimumOfIn0(sK1(X0),X0,xU)
& ! [X4] :
( sdtlseqdt0(X4,sK1(X0))
| ( ~ aLowerBoundOfIn0(X4,X0,xU)
& ( ( ~ sdtlseqdt0(X4,sK2(X0,X4))
& aElementOf0(sK2(X0,X4),X0) )
| ~ aElementOf0(X4,xU) ) ) )
& aLowerBoundOfIn0(sK1(X0),X0,xU)
& ! [X3] :
( sdtlseqdt0(sK1(X0),X3)
| ~ aElementOf0(X3,X0) )
& aElementOf0(sK1(X0),xU)
& aElementOf0(sK1(X0),xU) )
| ( ~ aSubsetOf0(X0,xU)
& ( ( ~ aElementOf0(sK0(X0),xU)
& aElementOf0(sK0(X0),X0) )
| ~ aSet0(X0) ) ) )
& aSet0(xU) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4]),skolemize(X1,sK0(X0)),skolemize(X2,sK1(X0)),skolemize(X5,sK2(X0,X4)),skolemize(W2,sK3(X0)),skolemize(W4,sK4(X0,W3))],[nnf_24]) ).
fof(sk_m__1123,plain,
( isOn0(xf,xU)
& szRzazndt0(xf) = xU
& szRzazndt0(xf) = szDzozmdt0(xf)
& isMonotone0(xf)
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(sdtlpdtrp0(xf,VAR_0),sdtlpdtrp0(xf,VAR_1))
| ~ sdtlseqdt0(VAR_0,VAR_1)
| ~ aElementOf0(VAR_1,szDzozmdt0(xf))
| ~ aElementOf0(VAR_0,szDzozmdt0(xf)) )
& aFunction0(xf)
& aCompleteLattice0(xU)
& ! [VAR_0] :
( aSupremumOfIn0(sK3(VAR_0),VAR_0,xU)
| ~ aSubsetOf0(VAR_0,xU) )
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(sK3(VAR_0),VAR_1)
| ~ aUpperBoundOfIn0(VAR_1,VAR_0,xU)
| ~ aSubsetOf0(VAR_0,xU) )
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(sK3(VAR_0),VAR_1)
| ~ sdtlseqdt0(sK4(VAR_0,VAR_1),VAR_1)
| ~ aElementOf0(VAR_1,xU)
| ~ aSubsetOf0(VAR_0,xU) )
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(sK3(VAR_0),VAR_1)
| aElementOf0(sK4(VAR_0,VAR_1),VAR_0)
| ~ aElementOf0(VAR_1,xU)
| ~ aSubsetOf0(VAR_0,xU) )
& ! [VAR_0] :
( aUpperBoundOfIn0(sK3(VAR_0),VAR_0,xU)
| ~ aSubsetOf0(VAR_0,xU) )
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(VAR_1,sK3(VAR_0))
| ~ aElementOf0(VAR_1,VAR_0)
| ~ aSubsetOf0(VAR_0,xU) )
& ! [VAR_0] :
( aElementOf0(sK3(VAR_0),xU)
| ~ aSubsetOf0(VAR_0,xU) )
& ! [VAR_0] :
( aInfimumOfIn0(sK1(VAR_0),VAR_0,xU)
| ~ aSubsetOf0(VAR_0,xU) )
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(VAR_1,sK1(VAR_0))
| ~ aLowerBoundOfIn0(VAR_1,VAR_0,xU)
| ~ aSubsetOf0(VAR_0,xU) )
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(VAR_1,sK1(VAR_0))
| ~ sdtlseqdt0(VAR_1,sK2(VAR_0,VAR_1))
| ~ aElementOf0(VAR_1,xU)
| ~ aSubsetOf0(VAR_0,xU) )
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(VAR_1,sK1(VAR_0))
| aElementOf0(sK2(VAR_0,VAR_1),VAR_0)
| ~ aElementOf0(VAR_1,xU)
| ~ aSubsetOf0(VAR_0,xU) )
& ! [VAR_0] :
( aLowerBoundOfIn0(sK1(VAR_0),VAR_0,xU)
| ~ aSubsetOf0(VAR_0,xU) )
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(sK1(VAR_0),VAR_1)
| ~ aElementOf0(VAR_1,VAR_0)
| ~ aSubsetOf0(VAR_0,xU) )
& ! [VAR_0] :
( aElementOf0(sK1(VAR_0),xU)
| ~ aSubsetOf0(VAR_0,xU) )
& ! [VAR_0] :
( aSupremumOfIn0(sK3(VAR_0),VAR_0,xU)
| ~ aElementOf0(sK0(VAR_0),xU)
| ~ aSet0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(sK3(VAR_0),VAR_1)
| ~ aUpperBoundOfIn0(VAR_1,VAR_0,xU)
| ~ aElementOf0(sK0(VAR_0),xU)
| ~ aSet0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(sK3(VAR_0),VAR_1)
| ~ sdtlseqdt0(sK4(VAR_0,VAR_1),VAR_1)
| ~ aElementOf0(VAR_1,xU)
| ~ aElementOf0(sK0(VAR_0),xU)
| ~ aSet0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(sK3(VAR_0),VAR_1)
| aElementOf0(sK4(VAR_0,VAR_1),VAR_0)
| ~ aElementOf0(VAR_1,xU)
| ~ aElementOf0(sK0(VAR_0),xU)
| ~ aSet0(VAR_0) )
& ! [VAR_0] :
( aUpperBoundOfIn0(sK3(VAR_0),VAR_0,xU)
| ~ aElementOf0(sK0(VAR_0),xU)
| ~ aSet0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(VAR_1,sK3(VAR_0))
| ~ aElementOf0(VAR_1,VAR_0)
| ~ aElementOf0(sK0(VAR_0),xU)
| ~ aSet0(VAR_0) )
& ! [VAR_0] :
( aElementOf0(sK3(VAR_0),xU)
| ~ aElementOf0(sK0(VAR_0),xU)
| ~ aSet0(VAR_0) )
& ! [VAR_0] :
( aInfimumOfIn0(sK1(VAR_0),VAR_0,xU)
| ~ aElementOf0(sK0(VAR_0),xU)
| ~ aSet0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(VAR_1,sK1(VAR_0))
| ~ aLowerBoundOfIn0(VAR_1,VAR_0,xU)
| ~ aElementOf0(sK0(VAR_0),xU)
| ~ aSet0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(VAR_1,sK1(VAR_0))
| ~ sdtlseqdt0(VAR_1,sK2(VAR_0,VAR_1))
| ~ aElementOf0(VAR_1,xU)
| ~ aElementOf0(sK0(VAR_0),xU)
| ~ aSet0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(VAR_1,sK1(VAR_0))
| aElementOf0(sK2(VAR_0,VAR_1),VAR_0)
| ~ aElementOf0(VAR_1,xU)
| ~ aElementOf0(sK0(VAR_0),xU)
| ~ aSet0(VAR_0) )
& ! [VAR_0] :
( aLowerBoundOfIn0(sK1(VAR_0),VAR_0,xU)
| ~ aElementOf0(sK0(VAR_0),xU)
| ~ aSet0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(sK1(VAR_0),VAR_1)
| ~ aElementOf0(VAR_1,VAR_0)
| ~ aElementOf0(sK0(VAR_0),xU)
| ~ aSet0(VAR_0) )
& ! [VAR_0] :
( aElementOf0(sK1(VAR_0),xU)
| ~ aElementOf0(sK0(VAR_0),xU)
| ~ aSet0(VAR_0) )
& ! [VAR_0] :
( aSupremumOfIn0(sK3(VAR_0),VAR_0,xU)
| aElementOf0(sK0(VAR_0),VAR_0)
| ~ aSet0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(sK3(VAR_0),VAR_1)
| ~ aUpperBoundOfIn0(VAR_1,VAR_0,xU)
| aElementOf0(sK0(VAR_0),VAR_0)
| ~ aSet0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(sK3(VAR_0),VAR_1)
| ~ sdtlseqdt0(sK4(VAR_0,VAR_1),VAR_1)
| ~ aElementOf0(VAR_1,xU)
| aElementOf0(sK0(VAR_0),VAR_0)
| ~ aSet0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(sK3(VAR_0),VAR_1)
| aElementOf0(sK4(VAR_0,VAR_1),VAR_0)
| ~ aElementOf0(VAR_1,xU)
| aElementOf0(sK0(VAR_0),VAR_0)
| ~ aSet0(VAR_0) )
& ! [VAR_0] :
( aUpperBoundOfIn0(sK3(VAR_0),VAR_0,xU)
| aElementOf0(sK0(VAR_0),VAR_0)
| ~ aSet0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(VAR_1,sK3(VAR_0))
| ~ aElementOf0(VAR_1,VAR_0)
| aElementOf0(sK0(VAR_0),VAR_0)
| ~ aSet0(VAR_0) )
& ! [VAR_0] :
( aElementOf0(sK3(VAR_0),xU)
| aElementOf0(sK0(VAR_0),VAR_0)
| ~ aSet0(VAR_0) )
& ! [VAR_0] :
( aInfimumOfIn0(sK1(VAR_0),VAR_0,xU)
| aElementOf0(sK0(VAR_0),VAR_0)
| ~ aSet0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(VAR_1,sK1(VAR_0))
| ~ aLowerBoundOfIn0(VAR_1,VAR_0,xU)
| aElementOf0(sK0(VAR_0),VAR_0)
| ~ aSet0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(VAR_1,sK1(VAR_0))
| ~ sdtlseqdt0(VAR_1,sK2(VAR_0,VAR_1))
| ~ aElementOf0(VAR_1,xU)
| aElementOf0(sK0(VAR_0),VAR_0)
| ~ aSet0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(VAR_1,sK1(VAR_0))
| aElementOf0(sK2(VAR_0,VAR_1),VAR_0)
| ~ aElementOf0(VAR_1,xU)
| aElementOf0(sK0(VAR_0),VAR_0)
| ~ aSet0(VAR_0) )
& ! [VAR_0] :
( aLowerBoundOfIn0(sK1(VAR_0),VAR_0,xU)
| aElementOf0(sK0(VAR_0),VAR_0)
| ~ aSet0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sdtlseqdt0(sK1(VAR_0),VAR_1)
| ~ aElementOf0(VAR_1,VAR_0)
| aElementOf0(sK0(VAR_0),VAR_0)
| ~ aSet0(VAR_0) )
& ! [VAR_0] :
( aElementOf0(sK1(VAR_0),xU)
| aElementOf0(sK0(VAR_0),VAR_0)
| ~ aSet0(VAR_0) )
& aSet0(xU) ),
inference(cnf_transformation,[status(thm)],[sk_m__1123_sk]) ).
cnf(c_93,plain,
( aInfimumOfIn0(sK1(A),A,xU)
| aElementOf0(sK0(A),A)
| ~ aSet0(A) ),
inference(split_conjunct,[status(thm)],[sk_m__1123]) ).
cnf(c_107,plain,
( aInfimumOfIn0(sK1(A),A,xU)
| ~ aElementOf0(sK0(A),xU)
| ~ aSet0(A) ),
inference(split_conjunct,[status(thm)],[sk_m__1123]) ).
cnf(c_144,plain,
aSet0(xP),
inference(clausify,[status(thm)],[m__1244]) ).
cnf(c_145,plain,
( aElementOf0(A,xU)
| ~ aElementOf0(A,xP) ),
inference(clausify,[status(thm)],[m__1244]) ).
cnf(c_166,negated_conjecture,
~ aInfimumOfIn0(A,xP,xU),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_422,plain,
( aInfimumOfIn0(sK1(xP),xP,xU)
| aElementOf0(sK0(xP),xP) ),
inference(resolve,[status(thm)],[c_144,c_93]) ).
cnf(c_222,negated_conjecture,
aElementOf0(sK0(xP),xP),
inference(resolve,[status(thm)],[c_166,c_422]) ).
cnf(c_311,plain,
aElementOf0(sK0(xP),xU),
inference(resolve,[status(thm)],[c_222,c_145]) ).
cnf(c_423,plain,
( aInfimumOfIn0(sK1(xP),xP,xU)
| ~ aSet0(xP) ),
inference(resolve,[status(thm)],[c_311,c_107]) ).
cnf(c_424,plain,
aInfimumOfIn0(sK1(xP),xP,xU),
inference(resolve,[status(thm)],[c_144,c_423]) ).
cnf(c_421,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_166,c_424]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT385+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.37 % Computer : n018.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 21:41:05 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.38 % Process 2912336 was started by sandbox2 on n018,
% 0.09/0.38 % Fri Sep 25 21:41:05 2026
% 0.09/0.38 % 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).
% 0.09/0.45
% 0.09/0.45 % SZS status Theorem for theBenchmark
% 0.09/0.45
% 0.09/0.45 % Proof 1 at 0.03 (+ 0.01) seconds.
% 0.09/0.45 % Length of proof is 11.
% 0.09/0.45 % Level of proof is 4.
% 0.09/0.45 % Maximum clause weight is 21.000.
% 0.09/0.45 % Given clauses 156.
% 0.09/0.45
% 0.09/0.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------