%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT303+1 : TPTP v9.3.1. Released v3.4.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:07 AM UTC 2026
% Result : Theorem 1.67s 0.63s
% Output : CNFRefutation 1.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 15
% Syntax : Number of formulae : 87 ( 24 unt; 0 def)
% Number of atoms : 253 ( 13 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 270 ( 104 ~; 97 |; 43 &)
% ( 3 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 2 con; 0-2 aty)
% Number of variables : 51 ( 0 sgn 24 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d4_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> k5_filter_2(A,B) = B ) ),
file('theBenchmark.p',d4_filter_2) ).
fof(dt_k1_lattice2,axiom,
! [A] :
( l3_lattices(A)
=> ( l3_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) ) ),
file('theBenchmark.p',dt_k1_lattice2) ).
fof(dt_k5_filter_2,axiom,
! [A,B] :
( ( m1_subset_1(B,u1_struct_0(A))
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k5_filter_2(A,B),u1_struct_0(k1_lattice2(A))) ),
file('theBenchmark.p',dt_k5_filter_2) ).
fof(dt_l1_lattices,axiom,
! [A] :
( l1_lattices(A)
=> l1_struct_0(A) ),
file('theBenchmark.p',dt_l1_lattices) ).
fof(dt_l2_lattices,axiom,
! [A] :
( l2_lattices(A)
=> l1_struct_0(A) ),
file('theBenchmark.p',dt_l2_lattices) ).
fof(dt_l3_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( l2_lattices(A)
& l1_lattices(A) ) ),
file('theBenchmark.p',dt_l3_lattices) ).
fof(fc1_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_struct_0(A) )
=> ( v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ),
file('theBenchmark.p',fc1_lattice2) ).
fof(fc1_struct_0,axiom,
! [A] :
( ( l1_struct_0(A)
& ~ v3_struct_0(A) )
=> ~ v1_xboole_0(u1_struct_0(A)) ),
file('theBenchmark.p',fc1_struct_0) ).
fof(fc6_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v10_lattices(k1_lattice2(A))
& v9_lattices(k1_lattice2(A))
& v8_lattices(k1_lattice2(A))
& v7_lattices(k1_lattice2(A))
& v6_lattices(k1_lattice2(A))
& v5_lattices(k1_lattice2(A))
& v4_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ),
file('theBenchmark.p',fc6_lattice2) ).
fof(redefinition_k6_domain_1,axiom,
! [A,B] :
( ( m1_subset_1(B,A)
& ~ v1_xboole_0(A) )
=> k6_domain_1(A,B) = k1_tarski(B) ),
file('theBenchmark.p',redefinition_k6_domain_1) ).
fof(redefinition_m1_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_filter_2(B,A)
<=> m1_filter_0(B,A) ) ),
file('theBenchmark.p',redefinition_m1_filter_2) ).
fof(t14_filter_0,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ( m1_filter_0(k6_domain_1(u1_struct_0(A),B),A)
=> v14_lattices(A) ) ) ),
file('theBenchmark.p',t14_filter_0) ).
fof(t21_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
<=> m1_filter_2(B,k1_lattice2(A)) ) ),
file('theBenchmark.p',t21_filter_2) ).
fof(t63_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v13_lattices(A)
<=> v14_lattices(k1_lattice2(A)) ) ),
file('theBenchmark.p',t63_lattice2) ).
fof(t27_filter_2,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ( m2_filter_2(k6_domain_1(u1_struct_0(A),B),A)
=> v13_lattices(A) ) ) ),
file('theBenchmark.p',t27_filter_2) ).
fof(t27_filter_2_neg,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ( m2_filter_2(k6_domain_1(u1_struct_0(A),B),A)
=> v13_lattices(A) ) ) ),
inference(assume_negation,[status(cth)],[t27_filter_2]) ).
cnf(c_94,plain,
( m1_filter_2(B,k1_lattice2(A))
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t21_filter_2]) ).
fof(nnf_90,plain,
? [A] :
( ? [B] :
( ~ v13_lattices(A)
& m2_filter_2(k6_domain_1(u1_struct_0(A),B),A)
& m1_subset_1(B,u1_struct_0(A)) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t27_filter_2_neg]) ).
fof(sk_t27_filter_2_neg,plain,
( ~ v13_lattices(sK0)
& m2_filter_2(k6_domain_1(u1_struct_0(sK0),sK1),sK0)
& m1_subset_1(sK1,u1_struct_0(sK0))
& l3_lattices(sK0)
& v10_lattices(sK0)
& ~ v3_struct_0(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(A,sK0),skolemize(B,sK1)],[nnf_90]) ).
cnf(c_96,negated_conjecture,
m2_filter_2(k6_domain_1(u1_struct_0(sK0),sK1),sK0),
inference(split_conjunct,[status(thm)],[sk_t27_filter_2_neg]) ).
cnf(c_172,plain,
( ~ v1_xboole_0(u1_struct_0(A))
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_struct_0]) ).
cnf(c_174,plain,
( l1_struct_0(A)
| ~ l2_lattices(A) ),
inference(clausify,[status(thm)],[dt_l2_lattices]) ).
cnf(c_175,plain,
( l1_struct_0(A)
| ~ l1_lattices(A) ),
inference(clausify,[status(thm)],[dt_l1_lattices]) ).
cnf(c_228,negated_conjecture,
( m1_filter_2(k6_domain_1(u1_struct_0(sK0),sK1),k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_96,c_94]) ).
cnf(c_235,negated_conjecture,
~ v13_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t27_filter_2_neg]) ).
cnf(c_236,negated_conjecture,
m1_subset_1(sK1,u1_struct_0(sK0)),
inference(split_conjunct,[status(thm)],[sk_t27_filter_2_neg]) ).
cnf(c_237,negated_conjecture,
l3_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t27_filter_2_neg]) ).
cnf(c_238,negated_conjecture,
v10_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t27_filter_2_neg]) ).
cnf(c_239,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t27_filter_2_neg]) ).
cnf(c_243,plain,
( ~ v14_lattices(k1_lattice2(A))
| v13_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t63_lattice2]) ).
cnf(c_249,plain,
( v14_lattices(A)
| ~ m1_filter_0(k6_domain_1(u1_struct_0(A),B),A)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t14_filter_0]) ).
cnf(c_251,plain,
( m1_filter_0(B,A)
| ~ m1_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[redefinition_m1_filter_2]) ).
cnf(c_252,plain,
( k1_tarski(B) = k6_domain_1(A,B)
| ~ m1_subset_1(B,A)
| v1_xboole_0(A) ),
inference(clausify,[status(thm)],[redefinition_k6_domain_1]) ).
cnf(c_253,plain,
( k6_domain_1(A,B) = k1_tarski(B)
| ~ m1_subset_1(B,A)
| v1_xboole_0(A) ),
inference(copy,[status(thm)],[c_252]) ).
cnf(c_284,plain,
( v10_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc6_lattice2]) ).
cnf(c_292,plain,
( ~ v3_struct_0(k1_lattice2(A))
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_lattice2]) ).
cnf(c_307,plain,
( l2_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_308,plain,
( l1_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_310,plain,
( m1_subset_1(k5_filter_2(A,B),u1_struct_0(k1_lattice2(A)))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k5_filter_2]) ).
cnf(c_311,plain,
( l3_lattices(k1_lattice2(A))
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_k1_lattice2]) ).
cnf(c_313,plain,
( k5_filter_2(A,B) = B
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d4_filter_2]) ).
cnf(c_342,plain,
( ~ v1_xboole_0(u1_struct_0(A))
| v3_struct_0(A)
| ~ l2_lattices(A) ),
inference(resolve,[status(thm)],[c_174,c_172]) ).
cnf(c_345,plain,
( ~ v1_xboole_0(u1_struct_0(A))
| v3_struct_0(A)
| ~ l1_lattices(A) ),
inference(resolve,[status(thm)],[c_175,c_172]) ).
cnf(c_1748,negated_conjecture,
( m1_filter_2(k6_domain_1(u1_struct_0(sK0),sK1),k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_239,c_228]) ).
cnf(c_1749,negated_conjecture,
( m1_filter_2(k6_domain_1(u1_struct_0(sK0),sK1),k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_238,c_1748]) ).
cnf(c_355,negated_conjecture,
m1_filter_2(k6_domain_1(u1_struct_0(sK0),sK1),k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_237,c_1749]) ).
cnf(c_1750,negated_conjecture,
( ~ v14_lattices(k1_lattice2(sK0))
| v13_lattices(sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_243,c_238]) ).
cnf(c_1751,negated_conjecture,
( ~ v14_lattices(k1_lattice2(sK0))
| v13_lattices(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_239,c_1750]) ).
cnf(c_1752,negated_conjecture,
( ~ v14_lattices(k1_lattice2(sK0))
| v13_lattices(sK0) ),
inference(resolve,[status(thm)],[c_237,c_1751]) ).
cnf(c_374,negated_conjecture,
~ v14_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_235,c_1752]) ).
cnf(c_381,plain,
( k6_domain_1(u1_struct_0(sK0),sK1) = k1_tarski(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_253,c_236]) ).
cnf(c_1753,negated_conjecture,
( v10_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_284,c_238]) ).
cnf(c_1754,negated_conjecture,
( v10_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_239,c_1753]) ).
cnf(c_471,negated_conjecture,
v10_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_237,c_1754]) ).
cnf(c_1755,negated_conjecture,
( ~ v3_struct_0(k1_lattice2(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_292,c_237]) ).
cnf(c_482,negated_conjecture,
~ v3_struct_0(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_239,c_1755]) ).
cnf(c_549,plain,
l2_lattices(sK0),
inference(resolve,[status(thm)],[c_307,c_237]) ).
cnf(c_1756,negated_conjecture,
( m1_subset_1(k5_filter_2(sK0,sK1),u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_310,c_236]) ).
cnf(c_1757,negated_conjecture,
( m1_subset_1(k5_filter_2(sK0,sK1),u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_239,c_1756]) ).
cnf(c_1758,negated_conjecture,
( m1_subset_1(k5_filter_2(sK0,sK1),u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_238,c_1757]) ).
cnf(c_566,negated_conjecture,
m1_subset_1(k5_filter_2(sK0,sK1),u1_struct_0(k1_lattice2(sK0))),
inference(resolve,[status(thm)],[c_237,c_1758]) ).
cnf(c_572,plain,
l3_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_311,c_237]) ).
cnf(c_1759,negated_conjecture,
( k5_filter_2(sK0,sK1) = sK1
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_313,c_236]) ).
cnf(c_1760,negated_conjecture,
( k5_filter_2(sK0,sK1) = sK1
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_239,c_1759]) ).
cnf(c_1761,negated_conjecture,
( k5_filter_2(sK0,sK1) = sK1
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_238,c_1760]) ).
cnf(c_580,negated_conjecture,
k5_filter_2(sK0,sK1) = sK1,
inference(resolve,[status(thm)],[c_237,c_1761]) ).
cnf(c_581,negated_conjecture,
m1_subset_1(sK1,u1_struct_0(k1_lattice2(sK0))),
inference(paramod,[status(thm)],[c_580,c_566]) ).
cnf(c_1762,negated_conjecture,
( m1_filter_0(k6_domain_1(u1_struct_0(sK0),sK1),k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_355,c_251]) ).
cnf(c_1763,negated_conjecture,
( m1_filter_0(k6_domain_1(u1_struct_0(sK0),sK1),k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_482,c_1762]) ).
cnf(c_1764,negated_conjecture,
( m1_filter_0(k6_domain_1(u1_struct_0(sK0),sK1),k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_471,c_1763]) ).
cnf(c_633,negated_conjecture,
m1_filter_0(k6_domain_1(u1_struct_0(sK0),sK1),k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_572,c_1764]) ).
cnf(c_1765,plain,
( ~ v1_xboole_0(u1_struct_0(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_549,c_342]) ).
cnf(c_719,negated_conjecture,
~ v1_xboole_0(u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_239,c_1765]) ).
cnf(c_722,plain,
k6_domain_1(u1_struct_0(sK0),sK1) = k1_tarski(sK1),
inference(resolve,[status(thm)],[c_719,c_381]) ).
cnf(c_729,negated_conjecture,
m1_filter_0(k1_tarski(sK1),k1_lattice2(sK0)),
inference(paramod,[status(thm)],[c_722,c_633]) ).
cnf(c_964,plain,
l1_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_572,c_308]) ).
cnf(c_1766,plain,
( ~ v1_xboole_0(u1_struct_0(k1_lattice2(sK0)))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_964,c_345]) ).
cnf(c_1088,plain,
~ v1_xboole_0(u1_struct_0(k1_lattice2(sK0))),
inference(resolve,[status(thm)],[c_482,c_1766]) ).
cnf(c_1767,plain,
( k6_domain_1(u1_struct_0(k1_lattice2(sK0)),sK1) = k1_tarski(sK1)
| v1_xboole_0(u1_struct_0(k1_lattice2(sK0))) ),
inference(resolve,[status(thm)],[c_581,c_253]) ).
cnf(c_1746,plain,
k6_domain_1(u1_struct_0(k1_lattice2(sK0)),sK1) = k1_tarski(sK1),
inference(resolve,[status(thm)],[c_1088,c_1767]) ).
cnf(c_1768,plain,
( v14_lattices(k1_lattice2(sK0))
| ~ m1_filter_0(k6_domain_1(u1_struct_0(k1_lattice2(sK0)),sK1),k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_581,c_249]) ).
cnf(c_1769,plain,
( v14_lattices(k1_lattice2(sK0))
| ~ m1_filter_0(k1_tarski(sK1),k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(paramod,[status(thm)],[c_1746,c_1768]) ).
cnf(c_1770,plain,
( v14_lattices(k1_lattice2(sK0))
| ~ m1_filter_0(k1_tarski(sK1),k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_482,c_1769]) ).
cnf(c_1771,plain,
( v14_lattices(k1_lattice2(sK0))
| ~ m1_filter_0(k1_tarski(sK1),k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_471,c_1770]) ).
cnf(c_1772,plain,
( v14_lattices(k1_lattice2(sK0))
| ~ m1_filter_0(k1_tarski(sK1),k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_572,c_1771]) ).
cnf(c_1773,plain,
v14_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_729,c_1772]) ).
cnf(c_1747,plain,
$false,
inference(resolve,[status(thm)],[c_374,c_1773]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT303+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n018.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 : Fri Sep 25 20:40:20 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 2821433 was started by sandbox2 on n018,
% 0.09/0.36 % Fri Sep 25 20:40:20 2026
% 0.09/0.36 % 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).
% 1.67/0.63
% 1.67/0.63 % SZS status Theorem for theBenchmark
% 1.67/0.63
% 1.67/0.63 % Proof 1 at 0.17 (+ 0.05) seconds.
% 1.67/0.63 % Length of proof is 58.
% 1.67/0.63 % Level of proof is 6.
% 1.67/0.63 % Maximum clause weight is 24.000.
% 1.67/0.63 % Given clauses 439.
% 1.67/0.63
% 1.67/0.63 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------