%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT301+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 : n010.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:06 AM UTC 2026
% Result : Theorem 0.80s 0.50s
% Output : CNFRefutation 0.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 13
% Syntax : Number of formulae : 82 ( 16 unt; 0 def)
% Number of atoms : 329 ( 20 equ)
% Maximal formula atoms : 12 ( 4 avg)
% Number of connectives : 399 ( 152 ~; 170 |; 52 &)
% ( 2 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 2 con; 0-2 aty)
% Number of variables : 44 ( 0 sgn 23 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d6_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> k7_filter_2(A,B) = B ) ),
file('theBenchmark.p',d6_filter_2) ).
fof(dt_k15_filter_2,axiom,
! [A,B] :
( ( m2_filter_2(B,A)
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m1_filter_2(k15_filter_2(A,B),k1_lattice2(A)) ),
file('theBenchmark.p',dt_k15_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_m2_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( m2_lattice4(B,A)
& ~ v1_xboole_0(B) ) ) ),
file('theBenchmark.p',dt_m2_filter_2) ).
fof(dt_m2_lattice4,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_lattice4(B,A)
=> m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ),
file('theBenchmark.p',dt_m2_lattice4) ).
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(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_k15_filter_2,axiom,
! [A,B] :
( ( m2_filter_2(B,A)
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k15_filter_2(A,B) = k7_filter_2(A,B) ),
file('theBenchmark.p',redefinition_k15_filter_2) ).
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(t12_filter_0,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_filter_0(B,A)
=> ( ( l3_lattices(A)
& v14_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> r2_hidden(k6_lattices(A),B) ) ) ),
file('theBenchmark.p',t12_filter_0) ).
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(t78_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& v13_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k5_lattices(A) = k6_lattices(k1_lattice2(A)) ),
file('theBenchmark.p',t78_lattice2) ).
fof(t25_filter_2,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( v13_lattices(A)
=> r2_hidden(k5_lattices(A),B) ) ) ),
file('theBenchmark.p',t25_filter_2) ).
fof(t25_filter_2_neg,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( v13_lattices(A)
=> r2_hidden(k5_lattices(A),B) ) ) ),
inference(assume_negation,[status(cth)],[t25_filter_2]) ).
cnf(c_89,plain,
( m2_lattice4(B,A)
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_m2_filter_2]) ).
cnf(c_91,plain,
( m1_filter_2(k15_filter_2(A,B),k1_lattice2(A))
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k15_filter_2]) ).
cnf(c_92,plain,
( k15_filter_2(A,B) = k7_filter_2(A,B)
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[redefinition_k15_filter_2]) ).
fof(nnf_87,plain,
? [A] :
( ? [B] :
( ~ r2_hidden(k5_lattices(A),B)
& v13_lattices(A)
& m2_filter_2(B,A) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t25_filter_2_neg]) ).
fof(sk_t25_filter_2_neg,plain,
( ~ r2_hidden(k5_lattices(sK1),sK0)
& v13_lattices(sK1)
& m2_filter_2(sK0,sK1)
& l3_lattices(sK1)
& v10_lattices(sK1)
& ~ v3_struct_0(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK0]),skolemize(A,sK1),skolemize(B,sK0)],[nnf_87]) ).
cnf(c_93,negated_conjecture,
m2_filter_2(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_t25_filter_2_neg]) ).
cnf(c_94,plain,
( k6_lattices(k1_lattice2(A)) = k5_lattices(A)
| ~ l3_lattices(A)
| ~ v13_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t78_lattice2]) ).
cnf(c_95,negated_conjecture,
v13_lattices(sK1),
inference(split_conjunct,[status(thm)],[sk_t25_filter_2_neg]) ).
cnf(c_97,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_140,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_143,negated_conjecture,
( m1_filter_2(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_93,c_91]) ).
cnf(c_172,negated_conjecture,
( ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1)
| m1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_140,c_143]) ).
cnf(c_177,plain,
( r2_hidden(k6_lattices(A),B)
| ~ v14_lattices(A)
| ~ m1_filter_0(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t12_filter_0]) ).
cnf(c_178,plain,
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ m2_lattice4(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_m2_lattice4]) ).
cnf(c_182,negated_conjecture,
( m2_lattice4(sK0,sK1)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_93,c_89]) ).
cnf(c_240,negated_conjecture,
( ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1)
| m1_subset_1(sK0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_178,c_182]) ).
cnf(c_805,negated_conjecture,
( ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| m1_subset_1(sK0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_240]) ).
cnf(c_806,negated_conjecture,
( ~ l3_lattices(sK1)
| m1_subset_1(sK0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_805]) ).
cnf(c_241,negated_conjecture,
( m1_subset_1(sK0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_806]) ).
cnf(c_267,negated_conjecture,
( v14_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_97,c_95]) ).
cnf(c_270,negated_conjecture,
( k6_lattices(k1_lattice2(sK1)) = k5_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_94,c_95]) ).
cnf(c_280,plain,
( k7_filter_2(A,B) = B
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d6_filter_2]) ).
cnf(c_282,plain,
( l3_lattices(k1_lattice2(A))
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_k1_lattice2]) ).
cnf(c_288,plain,
( ~ v3_struct_0(k1_lattice2(A))
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_lattice2]) ).
cnf(c_298,plain,
( v10_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc6_lattice2]) ).
cnf(c_341,negated_conjecture,
~ v3_struct_0(sK1),
inference(split_conjunct,[status(thm)],[sk_t25_filter_2_neg]) ).
cnf(c_342,negated_conjecture,
v10_lattices(sK1),
inference(split_conjunct,[status(thm)],[sk_t25_filter_2_neg]) ).
cnf(c_343,negated_conjecture,
l3_lattices(sK1),
inference(split_conjunct,[status(thm)],[sk_t25_filter_2_neg]) ).
cnf(c_344,negated_conjecture,
~ r2_hidden(k5_lattices(sK1),sK0),
inference(split_conjunct,[status(thm)],[sk_t25_filter_2_neg]) ).
cnf(c_349,negated_conjecture,
( k15_filter_2(sK1,sK0) = k7_filter_2(sK1,sK0)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_93,c_92]) ).
cnf(c_807,negated_conjecture,
( k7_filter_2(sK1,sK0) = k15_filter_2(sK1,sK0)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_349]) ).
cnf(c_808,negated_conjecture,
( k7_filter_2(sK1,sK0) = k15_filter_2(sK1,sK0)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_341,c_807]) ).
cnf(c_809,negated_conjecture,
( k7_filter_2(sK1,sK0) = k15_filter_2(sK1,sK0)
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_342,c_808]) ).
cnf(c_350,negated_conjecture,
k7_filter_2(sK1,sK0) = k15_filter_2(sK1,sK0),
inference(resolve,[status(thm)],[c_343,c_809]) ).
cnf(c_389,negated_conjecture,
( ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1))
| r2_hidden(k6_lattices(k1_lattice2(sK1)),k15_filter_2(sK1,sK0))
| ~ v14_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_177,c_172]) ).
cnf(c_810,negated_conjecture,
( ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| r2_hidden(k6_lattices(k1_lattice2(sK1)),k15_filter_2(sK1,sK0))
| ~ v14_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(copy,[status(thm)],[c_389]) ).
cnf(c_811,negated_conjecture,
( ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1)
| ~ l3_lattices(k1_lattice2(sK1))
| r2_hidden(k6_lattices(k1_lattice2(sK1)),k15_filter_2(sK1,sK0))
| ~ v14_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(copy,[status(thm)],[c_810]) ).
cnf(c_812,negated_conjecture,
( ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1)
| r2_hidden(k6_lattices(k1_lattice2(sK1)),k15_filter_2(sK1,sK0))
| ~ v14_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(copy,[status(thm)],[c_811]) ).
cnf(c_813,negated_conjecture,
( ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| r2_hidden(k6_lattices(k1_lattice2(sK1)),k15_filter_2(sK1,sK0))
| ~ v14_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_341,c_812]) ).
cnf(c_814,negated_conjecture,
( ~ l3_lattices(sK1)
| r2_hidden(k6_lattices(k1_lattice2(sK1)),k15_filter_2(sK1,sK0))
| ~ v14_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_342,c_813]) ).
cnf(c_390,negated_conjecture,
( r2_hidden(k6_lattices(k1_lattice2(sK1)),k15_filter_2(sK1,sK0))
| ~ v14_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_343,c_814]) ).
cnf(c_815,negated_conjecture,
( k6_lattices(k1_lattice2(sK1)) = k5_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_341,c_270]) ).
cnf(c_816,negated_conjecture,
( k6_lattices(k1_lattice2(sK1)) = k5_lattices(sK1)
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_342,c_815]) ).
cnf(c_410,negated_conjecture,
k6_lattices(k1_lattice2(sK1)) = k5_lattices(sK1),
inference(resolve,[status(thm)],[c_343,c_816]) ).
cnf(c_817,negated_conjecture,
( v14_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_341,c_267]) ).
cnf(c_818,negated_conjecture,
( v14_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_342,c_817]) ).
cnf(c_411,negated_conjecture,
v14_lattices(k1_lattice2(sK1)),
inference(resolve,[status(thm)],[c_343,c_818]) ).
cnf(c_819,negated_conjecture,
( m1_subset_1(sK0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_341,c_241]) ).
cnf(c_820,negated_conjecture,
( m1_subset_1(sK0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_342,c_819]) ).
cnf(c_412,negated_conjecture,
m1_subset_1(sK0,k1_zfmisc_1(u1_struct_0(sK1))),
inference(resolve,[status(thm)],[c_343,c_820]) ).
cnf(c_821,negated_conjecture,
( r2_hidden(k5_lattices(sK1),k15_filter_2(sK1,sK0))
| ~ v14_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(paramod,[status(thm)],[c_410,c_390]) ).
cnf(c_414,negated_conjecture,
( r2_hidden(k5_lattices(sK1),k15_filter_2(sK1,sK0))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_411,c_821]) ).
cnf(c_822,negated_conjecture,
( v10_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_342,c_298]) ).
cnf(c_823,negated_conjecture,
( v10_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_341,c_822]) ).
cnf(c_553,negated_conjecture,
v10_lattices(k1_lattice2(sK1)),
inference(resolve,[status(thm)],[c_343,c_823]) ).
cnf(c_569,negated_conjecture,
( r2_hidden(k5_lattices(sK1),k15_filter_2(sK1,sK0))
| ~ l3_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_553,c_414]) ).
cnf(c_572,plain,
l3_lattices(k1_lattice2(sK1)),
inference(resolve,[status(thm)],[c_343,c_282]) ).
cnf(c_588,negated_conjecture,
( r2_hidden(k5_lattices(sK1),k15_filter_2(sK1,sK0))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_572,c_569]) ).
cnf(c_824,negated_conjecture,
( k7_filter_2(sK1,sK0) = sK0
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_412,c_280]) ).
cnf(c_825,negated_conjecture,
( k15_filter_2(sK1,sK0) = sK0
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(paramod,[status(thm)],[c_350,c_824]) ).
cnf(c_826,negated_conjecture,
( k15_filter_2(sK1,sK0) = sK0
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_341,c_825]) ).
cnf(c_827,negated_conjecture,
( k15_filter_2(sK1,sK0) = sK0
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_342,c_826]) ).
cnf(c_666,negated_conjecture,
k15_filter_2(sK1,sK0) = sK0,
inference(resolve,[status(thm)],[c_343,c_827]) ).
cnf(c_828,negated_conjecture,
( r2_hidden(k5_lattices(sK1),sK0)
| v3_struct_0(k1_lattice2(sK1)) ),
inference(paramod,[status(thm)],[c_666,c_588]) ).
cnf(c_668,negated_conjecture,
v3_struct_0(k1_lattice2(sK1)),
inference(resolve,[status(thm)],[c_344,c_828]) ).
cnf(c_829,negated_conjecture,
( ~ l3_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_668,c_288]) ).
cnf(c_830,negated_conjecture,
~ l3_lattices(sK1),
inference(resolve,[status(thm)],[c_341,c_829]) ).
cnf(c_804,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_343,c_830]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT301+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.35 % Computer : n010.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Fri Sep 25 20:37:45 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.13/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.36 % Process 1609964 was started by sandbox2 on n010,
% 0.13/0.36 % Fri Sep 25 20:37:45 2026
% 0.13/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.13/0.38
% 0.13/0.38 % From the command line: assign(max_seconds, 300).
% 0.80/0.50
% 0.80/0.50 % SZS status Theorem for theBenchmark
% 0.80/0.50
% 0.80/0.50 % Proof 1 at 0.10 (+ 0.01) seconds.
% 0.80/0.50 % Length of proof is 53.
% 0.80/0.50 % Level of proof is 10.
% 0.80/0.50 % Maximum clause weight is 34.000.
% 0.80/0.50 % Given clauses 202.
% 0.80/0.50
% 0.80/0.50 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------