%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT305+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 : n014.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 0.63s 0.50s
% Output : CNFRefutation 0.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 10
% Syntax : Number of formulae : 96 ( 17 unt; 0 def)
% Number of atoms : 428 ( 25 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 571 ( 239 ~; 255 |; 56 &)
% ( 2 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-3 aty)
% Number of variables : 112 ( 1 sgn 28 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cc1_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( ( v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A) ) ) ),
file('theBenchmark.p',cc1_lattices) ).
fof(commutativity_k4_lattices,axiom,
! [A,B,C] :
( ( m1_subset_1(C,u1_struct_0(A))
& m1_subset_1(B,u1_struct_0(A))
& l1_lattices(A)
& v6_lattices(A)
& ~ v3_struct_0(A) )
=> k4_lattices(A,B,C) = k4_lattices(A,C,B) ),
file('theBenchmark.p',commutativity_k4_lattices) ).
fof(d9_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> k18_filter_2(A,B) = a_2_0_filter_2(A,B) ) ),
file('theBenchmark.p',d9_filter_2) ).
fof(dt_k4_lattices,axiom,
! [A,B,C] :
( ( m1_subset_1(C,u1_struct_0(A))
& m1_subset_1(B,u1_struct_0(A))
& l1_lattices(A)
& v6_lattices(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k4_lattices(A,B,C),u1_struct_0(A)) ),
file('theBenchmark.p',dt_k4_lattices) ).
fof(dt_l3_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( l2_lattices(A)
& l1_lattices(A) ) ),
file('theBenchmark.p',dt_l3_lattices) ).
fof(fraenkel_a_2_0_filter_2,axiom,
! [A,B,C] :
( ( m1_subset_1(C,u1_struct_0(B))
& l3_lattices(B)
& v10_lattices(B)
& ~ v3_struct_0(B) )
=> ( r2_hidden(A,a_2_0_filter_2(B,C))
<=> ? [D] :
( r3_lattices(B,D,C)
& A = D
& m1_subset_1(D,u1_struct_0(B)) ) ) ),
file('theBenchmark.p',fraenkel_a_2_0_filter_2) ).
fof(redefinition_r3_lattices,axiom,
! [A,B,C] :
( ( m1_subset_1(C,u1_struct_0(A))
& m1_subset_1(B,u1_struct_0(A))
& l3_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v6_lattices(A)
& ~ v3_struct_0(A) )
=> ( r3_lattices(A,B,C)
<=> r1_lattices(A,B,C) ) ),
file('theBenchmark.p',redefinition_r3_lattices) ).
fof(reflexivity_r3_lattices,axiom,
! [A,B,C] :
( ( m1_subset_1(C,u1_struct_0(A))
& m1_subset_1(B,u1_struct_0(A))
& l3_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v6_lattices(A)
& ~ v3_struct_0(A) )
=> r3_lattices(A,B,B) ),
file('theBenchmark.p',reflexivity_r3_lattices) ).
fof(t23_lattices,axiom,
! [A] :
( ( l3_lattices(A)
& v8_lattices(A)
& v6_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> r1_lattices(A,k4_lattices(A,B,C),B) ) ) ),
file('theBenchmark.p',t23_lattices) ).
fof(t31_filter_2,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( r2_hidden(k4_lattices(A,C,B),k18_filter_2(A,B))
& r2_hidden(k4_lattices(A,B,C),k18_filter_2(A,B))
& r2_hidden(B,k18_filter_2(A,B)) ) ) ) ),
file('theBenchmark.p',t31_filter_2) ).
fof(t31_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))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( r2_hidden(k4_lattices(A,C,B),k18_filter_2(A,B))
& r2_hidden(k4_lattices(A,B,C),k18_filter_2(A,B))
& r2_hidden(B,k18_filter_2(A,B)) ) ) ) ),
inference(assume_negation,[status(cth)],[t31_filter_2]) ).
cnf(c_85,plain,
( v9_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc1_lattices]) ).
cnf(c_86,plain,
( v8_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc1_lattices]) ).
cnf(c_88,plain,
( v6_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc1_lattices]) ).
cnf(c_91,plain,
( a_2_0_filter_2(A,B) = k18_filter_2(A,B)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d9_filter_2]) ).
cnf(c_101,plain,
( ~ r3_lattices(A,D,B)
| D != C
| ~ m1_subset_1(D,u1_struct_0(A))
| r2_hidden(C,a_2_0_filter_2(A,B))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fraenkel_a_2_0_filter_2]) ).
fof(nnf_83,plain,
? [A] :
( ? [B] :
( ? [C] :
( ( ~ r2_hidden(k4_lattices(A,C,B),k18_filter_2(A,B))
| ~ r2_hidden(k4_lattices(A,B,C),k18_filter_2(A,B))
| ~ r2_hidden(B,k18_filter_2(A,B)) )
& m1_subset_1(C,u1_struct_0(A)) )
& m1_subset_1(B,u1_struct_0(A)) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t31_filter_2_neg]) ).
fof(sk_t31_filter_2_neg,plain,
( ( ~ r2_hidden(k4_lattices(sK0,sK2,sK1),k18_filter_2(sK0,sK1))
| ~ r2_hidden(k4_lattices(sK0,sK1,sK2),k18_filter_2(sK0,sK1))
| ~ r2_hidden(sK1,k18_filter_2(sK0,sK1)) )
& m1_subset_1(sK2,u1_struct_0(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,sK2]),skolemize(A,sK0),skolemize(B,sK1),skolemize(C,sK2)],[nnf_83]) ).
cnf(c_104,negated_conjecture,
v10_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t31_filter_2_neg]) ).
cnf(c_130,plain,
( l1_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_132,plain,
( m1_subset_1(k4_lattices(A,B,C),u1_struct_0(A))
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l1_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k4_lattices]) ).
cnf(c_135,plain,
( k4_lattices(A,C,B) = k4_lattices(A,B,C)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l1_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[commutativity_k4_lattices]) ).
cnf(c_172,plain,
( ~ r1_lattices(A,B,C)
| r3_lattices(A,B,C)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v9_lattices(A)
| ~ v8_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[redefinition_r3_lattices]) ).
cnf(c_174,plain,
( r1_lattices(A,k4_lattices(A,B,C),B)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v8_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t23_lattices]) ).
cnf(c_240,plain,
( r3_lattices(A,B,B)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v9_lattices(A)
| ~ v8_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[reflexivity_r3_lattices]) ).
cnf(c_250,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t31_filter_2_neg]) ).
cnf(c_251,negated_conjecture,
l3_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t31_filter_2_neg]) ).
cnf(c_252,negated_conjecture,
m1_subset_1(sK1,u1_struct_0(sK0)),
inference(split_conjunct,[status(thm)],[sk_t31_filter_2_neg]) ).
cnf(c_253,negated_conjecture,
m1_subset_1(sK2,u1_struct_0(sK0)),
inference(split_conjunct,[status(thm)],[sk_t31_filter_2_neg]) ).
cnf(c_254,negated_conjecture,
( ~ r2_hidden(k4_lattices(sK0,sK2,sK1),k18_filter_2(sK0,sK1))
| ~ r2_hidden(k4_lattices(sK0,sK1,sK2),k18_filter_2(sK0,sK1))
| ~ r2_hidden(sK1,k18_filter_2(sK0,sK1)) ),
inference(split_conjunct,[status(thm)],[sk_t31_filter_2_neg]) ).
cnf(c_259,negated_conjecture,
( ~ r3_lattices(sK0,C,A)
| C != B
| ~ m1_subset_1(C,u1_struct_0(sK0))
| r2_hidden(B,a_2_0_filter_2(sK0,A))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_104,c_101]) ).
cnf(c_890,negated_conjecture,
( ~ r3_lattices(sK0,C,A)
| C != B
| ~ m1_subset_1(C,u1_struct_0(sK0))
| r2_hidden(B,a_2_0_filter_2(sK0,A))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_250,c_259]) ).
cnf(c_260,negated_conjecture,
( ~ r3_lattices(sK0,C,A)
| C != B
| ~ m1_subset_1(C,u1_struct_0(sK0))
| r2_hidden(B,a_2_0_filter_2(sK0,A))
| ~ m1_subset_1(A,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_251,c_890]) ).
cnf(c_279,negated_conjecture,
( a_2_0_filter_2(sK0,A) = k18_filter_2(sK0,A)
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_104,c_91]) ).
cnf(c_891,negated_conjecture,
( k18_filter_2(sK0,A) = a_2_0_filter_2(sK0,A)
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_279]) ).
cnf(c_892,negated_conjecture,
( k18_filter_2(sK0,A) = a_2_0_filter_2(sK0,A)
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_250,c_891]) ).
cnf(c_280,negated_conjecture,
( k18_filter_2(sK0,A) = a_2_0_filter_2(sK0,A)
| ~ m1_subset_1(A,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_251,c_892]) ).
cnf(c_281,negated_conjecture,
( v9_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_104,c_85]) ).
cnf(c_893,negated_conjecture,
( v9_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_251,c_281]) ).
cnf(c_282,negated_conjecture,
v9_lattices(sK0),
inference(resolve,[status(thm)],[c_250,c_893]) ).
cnf(c_283,negated_conjecture,
( v8_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_104,c_86]) ).
cnf(c_894,negated_conjecture,
( v8_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_251,c_283]) ).
cnf(c_284,negated_conjecture,
v8_lattices(sK0),
inference(resolve,[status(thm)],[c_250,c_894]) ).
cnf(c_287,negated_conjecture,
( v6_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_104,c_88]) ).
cnf(c_895,negated_conjecture,
( v6_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_251,c_287]) ).
cnf(c_288,negated_conjecture,
v6_lattices(sK0),
inference(resolve,[status(thm)],[c_250,c_895]) ).
cnf(c_304,plain,
( m1_subset_1(k4_lattices(A,B,C),u1_struct_0(A))
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ v6_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(resolve,[status(thm)],[c_130,c_132]) ).
cnf(c_307,plain,
( k4_lattices(A,C,B) = k4_lattices(A,B,C)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ v6_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(resolve,[status(thm)],[c_130,c_135]) ).
cnf(c_335,plain,
( r3_lattices(A,k4_lattices(A,B,C),B)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ m1_subset_1(k4_lattices(A,B,C),u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v9_lattices(A)
| ~ v8_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v8_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_174,c_172]) ).
cnf(c_896,plain,
( r3_lattices(A,k4_lattices(A,B,C),B)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ m1_subset_1(k4_lattices(A,B,C),u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v9_lattices(A)
| ~ v8_lattices(A)
| ~ v6_lattices(A)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v8_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_335]) ).
cnf(c_897,plain,
( r3_lattices(A,k4_lattices(A,B,C),B)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ m1_subset_1(k4_lattices(A,B,C),u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v9_lattices(A)
| ~ v8_lattices(A)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v8_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_896]) ).
cnf(c_898,plain,
( r3_lattices(A,k4_lattices(A,B,C),B)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ m1_subset_1(k4_lattices(A,B,C),u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v9_lattices(A)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v8_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_897]) ).
cnf(c_899,plain,
( r3_lattices(A,k4_lattices(A,B,C),B)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ m1_subset_1(k4_lattices(A,B,C),u1_struct_0(A))
| ~ v9_lattices(A)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v8_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_898]) ).
cnf(c_336,plain,
( r3_lattices(A,k4_lattices(A,B,C),B)
| ~ m1_subset_1(k4_lattices(A,B,C),u1_struct_0(A))
| ~ v9_lattices(A)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v8_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_899]) ).
cnf(c_362,plain,
( r3_lattices(A,B,B)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v9_lattices(A)
| ~ v8_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(factor,[status(thm)],[c_240]) ).
cnf(c_363,plain,
( ~ r3_lattices(sK0,A,A)
| A != B
| r2_hidden(B,a_2_0_filter_2(sK0,A))
| ~ m1_subset_1(A,u1_struct_0(sK0)) ),
inference(factor,[status(thm)],[c_260]) ).
cnf(c_510,plain,
k18_filter_2(sK0,sK1) = a_2_0_filter_2(sK0,sK1),
inference(resolve,[status(thm)],[c_280,c_252]) ).
cnf(c_900,negated_conjecture,
( ~ r2_hidden(k4_lattices(sK0,sK2,sK1),k18_filter_2(sK0,sK1))
| ~ r2_hidden(k4_lattices(sK0,sK1,sK2),k18_filter_2(sK0,sK1))
| ~ r2_hidden(sK1,a_2_0_filter_2(sK0,sK1)) ),
inference(paramod,[status(thm)],[c_510,c_254]) ).
cnf(c_901,negated_conjecture,
( ~ r2_hidden(k4_lattices(sK0,sK2,sK1),k18_filter_2(sK0,sK1))
| ~ r2_hidden(k4_lattices(sK0,sK1,sK2),a_2_0_filter_2(sK0,sK1))
| ~ r2_hidden(sK1,a_2_0_filter_2(sK0,sK1)) ),
inference(paramod,[status(thm)],[c_510,c_900]) ).
cnf(c_514,negated_conjecture,
( ~ r2_hidden(k4_lattices(sK0,sK2,sK1),a_2_0_filter_2(sK0,sK1))
| ~ r2_hidden(k4_lattices(sK0,sK1,sK2),a_2_0_filter_2(sK0,sK1))
| ~ r2_hidden(sK1,a_2_0_filter_2(sK0,sK1)) ),
inference(paramod,[status(thm)],[c_510,c_901]) ).
cnf(c_902,negated_conjecture,
( m1_subset_1(k4_lattices(sK0,A,B),u1_struct_0(sK0))
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ v6_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_304,c_251]) ).
cnf(c_903,negated_conjecture,
( m1_subset_1(k4_lattices(sK0,A,B),u1_struct_0(sK0))
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_902,c_288]) ).
cnf(c_904,negated_conjecture,
( m1_subset_1(k4_lattices(sK0,sK1,A),u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_903,c_252]) ).
cnf(c_905,negated_conjecture,
( m1_subset_1(k4_lattices(sK0,sK1,sK2),u1_struct_0(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_904,c_253]) ).
cnf(c_525,negated_conjecture,
m1_subset_1(k4_lattices(sK0,sK1,sK2),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_250,c_905]) ).
cnf(c_906,negated_conjecture,
( k4_lattices(sK0,B,A) = k4_lattices(sK0,A,B)
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ v6_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_307,c_251]) ).
cnf(c_907,negated_conjecture,
( k4_lattices(sK0,B,A) = k4_lattices(sK0,A,B)
| ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_906,c_288]) ).
cnf(c_908,negated_conjecture,
( k4_lattices(sK0,A,sK2) = k4_lattices(sK0,sK2,A)
| ~ m1_subset_1(A,u1_struct_0(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_907,c_253]) ).
cnf(c_909,negated_conjecture,
( k4_lattices(sK0,sK1,sK2) = k4_lattices(sK0,sK2,sK1)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_908,c_252]) ).
cnf(c_910,negated_conjecture,
( k4_lattices(sK0,sK2,sK1) = k4_lattices(sK0,sK1,sK2)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_909]) ).
cnf(c_566,negated_conjecture,
k4_lattices(sK0,sK2,sK1) = k4_lattices(sK0,sK1,sK2),
inference(resolve,[status(thm)],[c_250,c_910]) ).
cnf(c_911,negated_conjecture,
( ~ r2_hidden(k4_lattices(sK0,sK1,sK2),a_2_0_filter_2(sK0,sK1))
| ~ r2_hidden(k4_lattices(sK0,sK1,sK2),a_2_0_filter_2(sK0,sK1))
| ~ r2_hidden(sK1,a_2_0_filter_2(sK0,sK1)) ),
inference(paramod,[status(thm)],[c_566,c_514]) ).
cnf(c_569,negated_conjecture,
( ~ r2_hidden(k4_lattices(sK0,sK1,sK2),a_2_0_filter_2(sK0,sK1))
| ~ r2_hidden(sK1,a_2_0_filter_2(sK0,sK1)) ),
inference(copy,[status(thm)],[c_911]) ).
cnf(c_912,negated_conjecture,
( r3_lattices(sK0,sK1,sK1)
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0)
| ~ v8_lattices(sK0)
| ~ v6_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_362,c_252]) ).
cnf(c_913,negated_conjecture,
( r3_lattices(sK0,sK1,sK1)
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0)
| ~ v8_lattices(sK0)
| ~ v6_lattices(sK0) ),
inference(resolve,[status(thm)],[c_250,c_912]) ).
cnf(c_914,negated_conjecture,
( r3_lattices(sK0,sK1,sK1)
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0)
| ~ v8_lattices(sK0) ),
inference(resolve,[status(thm)],[c_288,c_913]) ).
cnf(c_915,negated_conjecture,
( r3_lattices(sK0,sK1,sK1)
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0) ),
inference(resolve,[status(thm)],[c_284,c_914]) ).
cnf(c_916,negated_conjecture,
( r3_lattices(sK0,sK1,sK1)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_282,c_915]) ).
cnf(c_631,negated_conjecture,
r3_lattices(sK0,sK1,sK1),
inference(resolve,[status(thm)],[c_251,c_916]) ).
cnf(c_917,negated_conjecture,
( ~ r3_lattices(sK0,sK1,sK1)
| sK1 != A
| r2_hidden(A,a_2_0_filter_2(sK0,sK1)) ),
inference(resolve,[status(thm)],[c_363,c_252]) ).
cnf(c_918,plain,
( ~ r3_lattices(sK0,sK1,sK1)
| r2_hidden(sK1,a_2_0_filter_2(sK0,sK1)) ),
inference(xxres,[status(thm)],[c_917]) ).
cnf(c_644,plain,
r2_hidden(sK1,a_2_0_filter_2(sK0,sK1)),
inference(resolve,[status(thm)],[c_918,c_631]) ).
cnf(c_645,negated_conjecture,
~ r2_hidden(k4_lattices(sK0,sK1,sK2),a_2_0_filter_2(sK0,sK1)),
inference(resolve,[status(thm)],[c_644,c_569]) ).
cnf(c_919,plain,
( r3_lattices(sK0,k4_lattices(sK0,sK1,sK2),sK1)
| ~ v9_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v8_lattices(sK0)
| ~ v6_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_525,c_336]) ).
cnf(c_920,negated_conjecture,
( r3_lattices(sK0,k4_lattices(sK0,sK1,sK2),sK1)
| ~ v9_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v8_lattices(sK0)
| ~ v6_lattices(sK0) ),
inference(resolve,[status(thm)],[c_250,c_919]) ).
cnf(c_921,negated_conjecture,
( r3_lattices(sK0,k4_lattices(sK0,sK1,sK2),sK1)
| ~ v9_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v8_lattices(sK0) ),
inference(resolve,[status(thm)],[c_288,c_920]) ).
cnf(c_922,negated_conjecture,
( r3_lattices(sK0,k4_lattices(sK0,sK1,sK2),sK1)
| ~ v9_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_284,c_921]) ).
cnf(c_923,negated_conjecture,
( r3_lattices(sK0,k4_lattices(sK0,sK1,sK2),sK1)
| ~ v9_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_251,c_922]) ).
cnf(c_924,negated_conjecture,
( r3_lattices(sK0,k4_lattices(sK0,sK1,sK2),sK1)
| ~ v9_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_252,c_923]) ).
cnf(c_925,negated_conjecture,
( r3_lattices(sK0,k4_lattices(sK0,sK1,sK2),sK1)
| ~ v9_lattices(sK0) ),
inference(resolve,[status(thm)],[c_253,c_924]) ).
cnf(c_768,negated_conjecture,
r3_lattices(sK0,k4_lattices(sK0,sK1,sK2),sK1),
inference(resolve,[status(thm)],[c_282,c_925]) ).
cnf(c_926,negated_conjecture,
( ~ r3_lattices(sK0,B,sK1)
| B != A
| ~ m1_subset_1(B,u1_struct_0(sK0))
| r2_hidden(A,a_2_0_filter_2(sK0,sK1)) ),
inference(resolve,[status(thm)],[c_260,c_252]) ).
cnf(c_927,negated_conjecture,
( ~ r3_lattices(sK0,k4_lattices(sK0,sK1,sK2),sK1)
| k4_lattices(sK0,sK1,sK2) != A
| r2_hidden(A,a_2_0_filter_2(sK0,sK1)) ),
inference(resolve,[status(thm)],[c_926,c_525]) ).
cnf(c_928,plain,
( ~ r3_lattices(sK0,k4_lattices(sK0,sK1,sK2),sK1)
| r2_hidden(k4_lattices(sK0,sK1,sK2),a_2_0_filter_2(sK0,sK1)) ),
inference(xxres,[status(thm)],[c_927]) ).
cnf(c_929,plain,
r2_hidden(k4_lattices(sK0,sK1,sK2),a_2_0_filter_2(sK0,sK1)),
inference(resolve,[status(thm)],[c_928,c_768]) ).
cnf(c_889,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_645,c_929]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT305+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n014.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Fri Sep 25 20:39:47 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 1046576 was started by sandbox2 on n014,
% 0.08/0.36 % Fri Sep 25 20:39:47 2026
% 0.08/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.63/0.50
% 0.63/0.50 % SZS status Theorem for theBenchmark
% 0.63/0.50
% 0.63/0.50 % Proof 1 at 0.08 (+ 0.01) seconds.
% 0.63/0.50 % Length of proof is 53.
% 0.63/0.50 % Level of proof is 8.
% 0.63/0.50 % Maximum clause weight is 42.000.
% 0.63/0.50 % Given clauses 208.
% 0.63/0.50
% 0.63/0.50 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------