%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT322+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 : n011.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:13 AM UTC 2026
% Result : Theorem 30.99s 4.93s
% Output : CNFRefutation 30.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 26
% Syntax : Number of formulae : 251 ( 37 unt; 0 def)
% Number of atoms : 1049 ( 136 equ)
% Maximal formula atoms : 20 ( 4 avg)
% Number of connectives : 1354 ( 556 ~; 655 |; 101 &)
% ( 8 <=>; 34 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 36 ( 34 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 2 con; 0-3 aty)
% Number of variables : 154 ( 19 sgn 47 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(abstractness_v3_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( v3_lattices(A)
=> A = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) ) ),
file('theBenchmark.p',abstractness_v3_lattices) ).
fof(d2_filter_0,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k1_filter_0(A) = u1_struct_0(A) ),
file('theBenchmark.p',d2_filter_0) ).
fof(d2_lattice2,axiom,
! [A] :
( l3_lattices(A)
=> k1_lattice2(A) = g3_lattices(u1_struct_0(A),u1_lattices(A),u2_lattices(A)) ),
file('theBenchmark.p',d2_lattice2) ).
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(d8_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k17_filter_2(A) = u1_struct_0(A) ),
file('theBenchmark.p',d8_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_k17_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m2_filter_2(k17_filter_2(A),A) ),
file('theBenchmark.p',dt_k17_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_l3_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( l2_lattices(A)
& l1_lattices(A) ) ),
file('theBenchmark.p',dt_l3_lattices) ).
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(dt_u1_lattices,axiom,
! [A] :
( l1_lattices(A)
=> ( m2_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_1(u1_lattices(A)) ) ),
file('theBenchmark.p',dt_u1_lattices) ).
fof(dt_u2_lattices,axiom,
! [A] :
( l2_lattices(A)
=> ( m2_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_1(u2_lattices(A)) ) ),
file('theBenchmark.p',dt_u2_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(fc4_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v17_lattices(k1_lattice2(A))
& v16_lattices(k1_lattice2(A))
& v15_lattices(k1_lattice2(A))
& v14_lattices(k1_lattice2(A))
& v13_lattices(k1_lattice2(A))
& v12_lattices(k1_lattice2(A))
& v11_lattices(k1_lattice2(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',fc4_filter_2) ).
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(free_g3_lattices,axiom,
! [A,B,C] :
( ( m1_relset_1(C,k2_zfmisc_1(A,A),A)
& v1_funct_2(C,k2_zfmisc_1(A,A),A)
& v1_funct_1(C)
& m1_relset_1(B,k2_zfmisc_1(A,A),A)
& v1_funct_2(B,k2_zfmisc_1(A,A),A)
& v1_funct_1(B) )
=> ! [D,E,F] :
( g3_lattices(A,B,C) = g3_lattices(D,E,F)
=> ( C = F
& B = E
& A = D ) ) ),
file('theBenchmark.p',free_g3_lattices) ).
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(redefinition_m2_relset_1,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('theBenchmark.p',redefinition_m2_relset_1) ).
fof(reflexivity_r1_tarski,axiom,
! [A,B] : r1_tarski(A,A),
file('theBenchmark.p',reflexivity_r1_tarski) ).
fof(t33_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( r2_filter_2(A,B)
<=> v1_filter_0(k15_filter_2(A,B),k1_lattice2(A)) ) ) ),
file('theBenchmark.p',t33_filter_2) ).
fof(t3_subset,axiom,
! [A,B] :
( m1_subset_1(A,k1_zfmisc_1(B))
<=> r1_tarski(A,B) ),
file('theBenchmark.p',t3_subset) ).
fof(t44_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( v1_filter_2(B,A)
<=> v2_filter_0(k15_filter_2(A,B),k1_lattice2(A)) ) ) ),
file('theBenchmark.p',t44_filter_2) ).
fof(t58_filter_0,axiom,
! [A] :
( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_filter_0(B,A)
=> ( ( v2_filter_0(B,A)
& B != k1_filter_0(A) )
<=> v1_filter_0(B,A) ) ) ),
file('theBenchmark.p',t58_filter_0) ).
fof(t58_filter_2,conjecture,
! [A] :
( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( ( v1_filter_2(B,A)
& B != k17_filter_2(A) )
<=> r2_filter_2(A,B) ) ) ),
file('theBenchmark.p',t58_filter_2) ).
fof(t58_filter_2_neg,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( ( v1_filter_2(B,A)
& B != k17_filter_2(A) )
<=> r2_filter_2(A,B) ) ) ),
inference(assume_negation,[status(cth)],[t58_filter_2]) ).
cnf(c_99,plain,
( m2_filter_2(k17_filter_2(A),A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k17_filter_2]) ).
cnf(c_100,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_102,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_104,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]) ).
cnf(c_105,plain,
( v1_filter_0(k15_filter_2(A,B),k1_lattice2(A))
| ~ r2_filter_2(A,B)
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t33_filter_2]) ).
cnf(c_106,plain,
( ~ v1_filter_0(k15_filter_2(A,B),k1_lattice2(A))
| r2_filter_2(A,B)
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t33_filter_2]) ).
cnf(c_107,plain,
( v2_filter_0(k15_filter_2(A,B),k1_lattice2(A))
| ~ v1_filter_2(B,A)
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t44_filter_2]) ).
cnf(c_108,plain,
( ~ v2_filter_0(k15_filter_2(A,B),k1_lattice2(A))
| v1_filter_2(B,A)
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t44_filter_2]) ).
fof(nnf_98,plain,
? [A] :
( ? [B] :
( ( ~ r2_filter_2(A,B)
| ~ v1_filter_2(B,A)
| k17_filter_2(A) = B )
& ( r2_filter_2(A,B)
| ( v1_filter_2(B,A)
& k17_filter_2(A) != B ) )
& m2_filter_2(B,A) )
& l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t58_filter_2_neg]) ).
fof(sk_t58_filter_2_neg_sk,plain,
( ( ~ r2_filter_2(sK1,sK0)
| ~ v1_filter_2(sK0,sK1)
| k17_filter_2(sK1) = sK0 )
& ( r2_filter_2(sK1,sK0)
| ( v1_filter_2(sK0,sK1)
& k17_filter_2(sK1) != sK0 ) )
& m2_filter_2(sK0,sK1)
& l3_lattices(sK1)
& v17_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_98]) ).
fof(sk_t58_filter_2_neg,plain,
( ( ~ r2_filter_2(sK1,sK0)
| ~ v1_filter_2(sK0,sK1)
| k17_filter_2(sK1) = sK0 )
& ( r2_filter_2(sK1,sK0)
| v1_filter_2(sK0,sK1) )
& ( r2_filter_2(sK1,sK0)
| k17_filter_2(sK1) != sK0 )
& m2_filter_2(sK0,sK1)
& l3_lattices(sK1)
& v17_lattices(sK1)
& v10_lattices(sK1)
& ~ v3_struct_0(sK1) ),
inference(cnf_transformation,[status(thm)],[sk_t58_filter_2_neg_sk]) ).
cnf(c_109,negated_conjecture,
m2_filter_2(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_t58_filter_2_neg]) ).
cnf(c_110,plain,
( g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) = A
| ~ v3_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[abstractness_v3_lattices]) ).
cnf(c_112,plain,
( v3_lattices(k1_lattice2(A))
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_k1_lattice2]) ).
cnf(c_237,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_239,plain,
( m1_filter_2(k15_filter_2(A,k17_filter_2(A)),k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_99,c_100]) ).
cnf(c_241,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_109,c_100]) ).
cnf(c_249,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_237,c_241]) ).
cnf(c_251,plain,
( ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| m1_filter_0(k15_filter_2(A,k17_filter_2(A)),k1_lattice2(A))
| ~ l3_lattices(k1_lattice2(A))
| ~ v10_lattices(k1_lattice2(A))
| v3_struct_0(k1_lattice2(A)) ),
inference(resolve,[status(thm)],[c_237,c_239]) ).
cnf(c_256,plain,
( v1_filter_0(B,A)
| ~ v2_filter_0(B,A)
| k1_filter_0(A) = B
| ~ m1_filter_0(B,A)
| ~ l3_lattices(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t58_filter_0]) ).
cnf(c_257,plain,
( ~ v1_filter_0(B,A)
| k1_filter_0(A) != B
| ~ m1_filter_0(B,A)
| ~ l3_lattices(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t58_filter_0]) ).
cnf(c_258,plain,
( ~ v1_filter_0(B,A)
| v2_filter_0(B,A)
| ~ m1_filter_0(B,A)
| ~ l3_lattices(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t58_filter_0]) ).
cnf(c_266,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_276,negated_conjecture,
( m2_lattice4(sK0,sK1)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_109,c_102]) ).
cnf(c_284,plain,
( m1_relset_1(A,B,C)
| ~ m2_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_m2_relset_1]) ).
cnf(c_287,plain,
( m2_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
| ~ l2_lattices(A) ),
inference(clausify,[status(thm)],[dt_u2_lattices]) ).
cnf(c_288,plain,
( m2_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
| ~ l1_lattices(A) ),
inference(clausify,[status(thm)],[dt_u1_lattices]) ).
cnf(c_291,plain,
( ~ r1_tarski(A,B)
| m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[t3_subset]) ).
cnf(c_292,plain,
r1_tarski(A,A),
inference(clausify,[status(thm)],[reflexivity_r1_tarski]) ).
cnf(c_293,plain,
m1_subset_1(A,k1_zfmisc_1(A)),
inference(resolve,[status(thm)],[c_292,c_291]) ).
cnf(c_298,plain,
( m1_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
| ~ l1_lattices(A) ),
inference(resolve,[status(thm)],[c_288,c_284]) ).
cnf(c_299,plain,
( m1_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
| ~ l2_lattices(A) ),
inference(resolve,[status(thm)],[c_287,c_284]) ).
cnf(c_353,plain,
( ~ l3_lattices(A)
| g3_lattices(u1_struct_0(k1_lattice2(A)),u2_lattices(k1_lattice2(A)),u1_lattices(k1_lattice2(A))) = k1_lattice2(A)
| ~ l3_lattices(k1_lattice2(A)) ),
inference(resolve,[status(thm)],[c_110,c_112]) ).
cnf(c_359,plain,
( k1_filter_0(A) = u1_struct_0(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d2_filter_0]) ).
cnf(c_360,plain,
( k1_lattice2(A) = g3_lattices(u1_struct_0(A),u1_lattices(A),u2_lattices(A))
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[d2_lattice2]) ).
cnf(c_361,plain,
( g3_lattices(u1_struct_0(A),u1_lattices(A),u2_lattices(A)) = k1_lattice2(A)
| ~ l3_lattices(A) ),
inference(copy,[status(thm)],[c_360]) ).
cnf(c_362,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_363,plain,
( u1_struct_0(A) = k17_filter_2(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d8_filter_2]) ).
cnf(c_364,plain,
( k17_filter_2(A) = u1_struct_0(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_363]) ).
cnf(c_366,plain,
( l3_lattices(k1_lattice2(A))
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_k1_lattice2]) ).
cnf(c_368,plain,
( l1_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_369,plain,
( l2_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_370,plain,
( v1_funct_1(u1_lattices(A))
| ~ l1_lattices(A) ),
inference(clausify,[status(thm)],[dt_u1_lattices]) ).
cnf(c_371,plain,
( v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
| ~ l1_lattices(A) ),
inference(clausify,[status(thm)],[dt_u1_lattices]) ).
cnf(c_372,plain,
( v1_funct_1(u2_lattices(A))
| ~ l2_lattices(A) ),
inference(clausify,[status(thm)],[dt_u2_lattices]) ).
cnf(c_373,plain,
( v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
| ~ l2_lattices(A) ),
inference(clausify,[status(thm)],[dt_u2_lattices]) ).
cnf(c_380,plain,
( ~ v3_struct_0(k1_lattice2(A))
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_lattice2]) ).
cnf(c_388,plain,
( v17_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc4_filter_2]) ).
cnf(c_390,plain,
( v10_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc6_lattice2]) ).
cnf(c_391,plain,
( D = B
| g3_lattices(D,E,F) != g3_lattices(B,A,C)
| ~ m1_relset_1(C,k2_zfmisc_1(B,B),B)
| ~ v1_funct_2(C,k2_zfmisc_1(B,B),B)
| ~ v1_funct_1(C)
| ~ m1_relset_1(A,k2_zfmisc_1(B,B),B)
| ~ v1_funct_2(A,k2_zfmisc_1(B,B),B)
| ~ v1_funct_1(A) ),
inference(clausify,[status(thm)],[free_g3_lattices]) ).
cnf(c_441,negated_conjecture,
~ v3_struct_0(sK1),
inference(split_conjunct,[status(thm)],[sk_t58_filter_2_neg]) ).
cnf(c_442,negated_conjecture,
v10_lattices(sK1),
inference(split_conjunct,[status(thm)],[sk_t58_filter_2_neg]) ).
cnf(c_443,negated_conjecture,
v17_lattices(sK1),
inference(split_conjunct,[status(thm)],[sk_t58_filter_2_neg]) ).
cnf(c_444,negated_conjecture,
l3_lattices(sK1),
inference(split_conjunct,[status(thm)],[sk_t58_filter_2_neg]) ).
cnf(c_445,negated_conjecture,
( r2_filter_2(sK1,sK0)
| k17_filter_2(sK1) != sK0 ),
inference(split_conjunct,[status(thm)],[sk_t58_filter_2_neg]) ).
cnf(c_446,negated_conjecture,
( r2_filter_2(sK1,sK0)
| v1_filter_2(sK0,sK1) ),
inference(split_conjunct,[status(thm)],[sk_t58_filter_2_neg]) ).
cnf(c_447,negated_conjecture,
( ~ r2_filter_2(sK1,sK0)
| ~ v1_filter_2(sK0,sK1)
| k17_filter_2(sK1) = sK0 ),
inference(split_conjunct,[status(thm)],[sk_t58_filter_2_neg]) ).
cnf(c_454,plain,
( ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| k15_filter_2(A,k17_filter_2(A)) = k7_filter_2(A,k17_filter_2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_104,c_99]) ).
cnf(c_11812,plain,
( ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| k7_filter_2(A,k17_filter_2(A)) = k15_filter_2(A,k17_filter_2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_454]) ).
cnf(c_11813,plain,
( ~ l3_lattices(A)
| ~ v10_lattices(A)
| k7_filter_2(A,k17_filter_2(A)) = k15_filter_2(A,k17_filter_2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_11812]) ).
cnf(c_11814,plain,
( ~ l3_lattices(A)
| k7_filter_2(A,k17_filter_2(A)) = k15_filter_2(A,k17_filter_2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_11813]) ).
cnf(c_455,plain,
( k7_filter_2(A,k17_filter_2(A)) = k15_filter_2(A,k17_filter_2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_11814]) ).
cnf(c_458,plain,
( ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| v1_filter_0(k15_filter_2(A,k17_filter_2(A)),k1_lattice2(A))
| ~ r2_filter_2(A,k17_filter_2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_105,c_99]) ).
cnf(c_11815,plain,
( ~ l3_lattices(A)
| ~ v10_lattices(A)
| v1_filter_0(k15_filter_2(A,k17_filter_2(A)),k1_lattice2(A))
| ~ r2_filter_2(A,k17_filter_2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_458]) ).
cnf(c_11816,plain,
( ~ l3_lattices(A)
| v1_filter_0(k15_filter_2(A,k17_filter_2(A)),k1_lattice2(A))
| ~ r2_filter_2(A,k17_filter_2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_11815]) ).
cnf(c_459,plain,
( v1_filter_0(k15_filter_2(A,k17_filter_2(A)),k1_lattice2(A))
| ~ r2_filter_2(A,k17_filter_2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_11816]) ).
cnf(c_472,negated_conjecture,
( ~ v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| v1_filter_2(sK0,sK1)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_109,c_108]) ).
cnf(c_11817,negated_conjecture,
( ~ v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| v1_filter_2(sK0,sK1)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_441,c_472]) ).
cnf(c_11818,negated_conjecture,
( ~ v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| v1_filter_2(sK0,sK1)
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_442,c_11817]) ).
cnf(c_473,negated_conjecture,
( ~ v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| v1_filter_2(sK0,sK1) ),
inference(resolve,[status(thm)],[c_444,c_11818]) ).
cnf(c_474,negated_conjecture,
( v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ v1_filter_2(sK0,sK1)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_109,c_107]) ).
cnf(c_11819,negated_conjecture,
( v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ v1_filter_2(sK0,sK1)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_441,c_474]) ).
cnf(c_11820,negated_conjecture,
( v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ v1_filter_2(sK0,sK1)
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_442,c_11819]) ).
cnf(c_475,negated_conjecture,
( v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ v1_filter_2(sK0,sK1) ),
inference(resolve,[status(thm)],[c_444,c_11820]) ).
cnf(c_476,negated_conjecture,
( ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| r2_filter_2(sK1,sK0)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_109,c_106]) ).
cnf(c_11821,negated_conjecture,
( ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| r2_filter_2(sK1,sK0)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_441,c_476]) ).
cnf(c_11822,negated_conjecture,
( ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| r2_filter_2(sK1,sK0)
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_442,c_11821]) ).
cnf(c_477,negated_conjecture,
( ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| r2_filter_2(sK1,sK0) ),
inference(resolve,[status(thm)],[c_444,c_11822]) ).
cnf(c_478,negated_conjecture,
( v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ r2_filter_2(sK1,sK0)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_109,c_105]) ).
cnf(c_11823,negated_conjecture,
( v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ r2_filter_2(sK1,sK0)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_441,c_478]) ).
cnf(c_11824,negated_conjecture,
( v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ r2_filter_2(sK1,sK0)
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_442,c_11823]) ).
cnf(c_479,negated_conjecture,
( v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ r2_filter_2(sK1,sK0) ),
inference(resolve,[status(thm)],[c_444,c_11824]) ).
cnf(c_480,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_109,c_104]) ).
cnf(c_11825,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_480]) ).
cnf(c_11826,negated_conjecture,
( k7_filter_2(sK1,sK0) = k15_filter_2(sK1,sK0)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_441,c_11825]) ).
cnf(c_11827,negated_conjecture,
( k7_filter_2(sK1,sK0) = k15_filter_2(sK1,sK0)
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_442,c_11826]) ).
cnf(c_481,negated_conjecture,
k7_filter_2(sK1,sK0) = k15_filter_2(sK1,sK0),
inference(resolve,[status(thm)],[c_444,c_11827]) ).
cnf(c_542,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))
| v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| k1_filter_0(k1_lattice2(sK1)) = k15_filter_2(sK1,sK0)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_256,c_249]) ).
cnf(c_11828,negated_conjecture,
( ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| k1_filter_0(k1_lattice2(sK1)) = k15_filter_2(sK1,sK0)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(copy,[status(thm)],[c_542]) ).
cnf(c_11829,negated_conjecture,
( ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1)
| ~ l3_lattices(k1_lattice2(sK1))
| v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| k1_filter_0(k1_lattice2(sK1)) = k15_filter_2(sK1,sK0)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(copy,[status(thm)],[c_11828]) ).
cnf(c_11830,negated_conjecture,
( ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1)
| v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| k1_filter_0(k1_lattice2(sK1)) = k15_filter_2(sK1,sK0)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(copy,[status(thm)],[c_11829]) ).
cnf(c_11831,negated_conjecture,
( ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| k1_filter_0(k1_lattice2(sK1)) = k15_filter_2(sK1,sK0)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_441,c_11830]) ).
cnf(c_11832,negated_conjecture,
( ~ l3_lattices(sK1)
| v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| k1_filter_0(k1_lattice2(sK1)) = k15_filter_2(sK1,sK0)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_442,c_11831]) ).
cnf(c_543,negated_conjecture,
( v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| k1_filter_0(k1_lattice2(sK1)) = k15_filter_2(sK1,sK0)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_444,c_11832]) ).
cnf(c_551,plain,
( ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(k1_lattice2(A))
| ~ v10_lattices(k1_lattice2(A))
| v3_struct_0(k1_lattice2(A))
| ~ v1_filter_0(k15_filter_2(A,k17_filter_2(A)),k1_lattice2(A))
| k1_filter_0(k1_lattice2(A)) != k15_filter_2(A,k17_filter_2(A))
| ~ l3_lattices(k1_lattice2(A))
| ~ v17_lattices(k1_lattice2(A))
| ~ v10_lattices(k1_lattice2(A))
| v3_struct_0(k1_lattice2(A)) ),
inference(resolve,[status(thm)],[c_257,c_251]) ).
cnf(c_11833,plain,
( ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(k1_lattice2(A))
| ~ v10_lattices(k1_lattice2(A))
| ~ v1_filter_0(k15_filter_2(A,k17_filter_2(A)),k1_lattice2(A))
| k1_filter_0(k1_lattice2(A)) != k15_filter_2(A,k17_filter_2(A))
| ~ l3_lattices(k1_lattice2(A))
| ~ v17_lattices(k1_lattice2(A))
| ~ v10_lattices(k1_lattice2(A))
| v3_struct_0(k1_lattice2(A)) ),
inference(copy,[status(thm)],[c_551]) ).
cnf(c_11834,plain,
( ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(k1_lattice2(A))
| ~ v1_filter_0(k15_filter_2(A,k17_filter_2(A)),k1_lattice2(A))
| k1_filter_0(k1_lattice2(A)) != k15_filter_2(A,k17_filter_2(A))
| ~ l3_lattices(k1_lattice2(A))
| ~ v17_lattices(k1_lattice2(A))
| ~ v10_lattices(k1_lattice2(A))
| v3_struct_0(k1_lattice2(A)) ),
inference(copy,[status(thm)],[c_11833]) ).
cnf(c_11835,plain,
( ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ v1_filter_0(k15_filter_2(A,k17_filter_2(A)),k1_lattice2(A))
| k1_filter_0(k1_lattice2(A)) != k15_filter_2(A,k17_filter_2(A))
| ~ l3_lattices(k1_lattice2(A))
| ~ v17_lattices(k1_lattice2(A))
| ~ v10_lattices(k1_lattice2(A))
| v3_struct_0(k1_lattice2(A)) ),
inference(copy,[status(thm)],[c_11834]) ).
cnf(c_11836,plain,
( ~ l3_lattices(A)
| ~ v10_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ v1_filter_0(k15_filter_2(A,k17_filter_2(A)),k1_lattice2(A))
| k1_filter_0(k1_lattice2(A)) != k15_filter_2(A,k17_filter_2(A))
| ~ l3_lattices(k1_lattice2(A))
| ~ v17_lattices(k1_lattice2(A))
| ~ v10_lattices(k1_lattice2(A))
| v3_struct_0(k1_lattice2(A)) ),
inference(copy,[status(thm)],[c_11835]) ).
cnf(c_11837,plain,
( ~ l3_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ v1_filter_0(k15_filter_2(A,k17_filter_2(A)),k1_lattice2(A))
| k1_filter_0(k1_lattice2(A)) != k15_filter_2(A,k17_filter_2(A))
| ~ l3_lattices(k1_lattice2(A))
| ~ v17_lattices(k1_lattice2(A))
| ~ v10_lattices(k1_lattice2(A))
| v3_struct_0(k1_lattice2(A)) ),
inference(copy,[status(thm)],[c_11836]) ).
cnf(c_552,plain,
( ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ v1_filter_0(k15_filter_2(A,k17_filter_2(A)),k1_lattice2(A))
| k1_filter_0(k1_lattice2(A)) != k15_filter_2(A,k17_filter_2(A))
| ~ l3_lattices(k1_lattice2(A))
| ~ v17_lattices(k1_lattice2(A))
| ~ v10_lattices(k1_lattice2(A))
| v3_struct_0(k1_lattice2(A)) ),
inference(copy,[status(thm)],[c_11837]) ).
cnf(c_568,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))
| ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_258,c_249]) ).
cnf(c_11838,negated_conjecture,
( ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(copy,[status(thm)],[c_568]) ).
cnf(c_11839,negated_conjecture,
( ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(copy,[status(thm)],[c_11838]) ).
cnf(c_11840,negated_conjecture,
( ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1)
| ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(copy,[status(thm)],[c_11839]) ).
cnf(c_11841,negated_conjecture,
( ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_441,c_11840]) ).
cnf(c_11842,negated_conjecture,
( ~ l3_lattices(sK1)
| ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_442,c_11841]) ).
cnf(c_569,negated_conjecture,
( ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_444,c_11842]) ).
cnf(c_582,negated_conjecture,
( m1_subset_1(sK0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_276,c_266]) ).
cnf(c_11843,negated_conjecture,
( m1_subset_1(sK0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_582]) ).
cnf(c_11844,negated_conjecture,
( m1_subset_1(sK0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_11843]) ).
cnf(c_11845,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_11844]) ).
cnf(c_11846,negated_conjecture,
( m1_subset_1(sK0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_441,c_11845]) ).
cnf(c_11847,negated_conjecture,
( m1_subset_1(sK0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_442,c_11846]) ).
cnf(c_583,negated_conjecture,
m1_subset_1(sK0,k1_zfmisc_1(u1_struct_0(sK1))),
inference(resolve,[status(thm)],[c_444,c_11847]) ).
cnf(c_607,plain,
( k7_filter_2(A,u1_struct_0(A)) = u1_struct_0(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_362,c_293]) ).
cnf(c_11848,negated_conjecture,
( v10_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_442,c_390]) ).
cnf(c_11849,negated_conjecture,
( v10_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_441,c_11848]) ).
cnf(c_967,negated_conjecture,
v10_lattices(k1_lattice2(sK1)),
inference(resolve,[status(thm)],[c_444,c_11849]) ).
cnf(c_11850,negated_conjecture,
( v17_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| ~ v17_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_442,c_388]) ).
cnf(c_11851,negated_conjecture,
( v17_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| ~ v17_lattices(sK1) ),
inference(resolve,[status(thm)],[c_441,c_11850]) ).
cnf(c_11852,negated_conjecture,
( v17_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_443,c_11851]) ).
cnf(c_968,negated_conjecture,
v17_lattices(k1_lattice2(sK1)),
inference(resolve,[status(thm)],[c_444,c_11852]) ).
cnf(c_11853,negated_conjecture,
( k17_filter_2(sK1) = u1_struct_0(sK1)
| ~ l3_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_442,c_364]) ).
cnf(c_11854,negated_conjecture,
( k17_filter_2(sK1) = u1_struct_0(sK1)
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_441,c_11853]) ).
cnf(c_974,negated_conjecture,
k17_filter_2(sK1) = u1_struct_0(sK1),
inference(resolve,[status(thm)],[c_444,c_11854]) ).
cnf(c_11855,negated_conjecture,
( ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_967,c_569]) ).
cnf(c_981,negated_conjecture,
( ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_968,c_11855]) ).
cnf(c_11856,negated_conjecture,
( v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| k1_filter_0(k1_lattice2(sK1)) = k15_filter_2(sK1,sK0)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_967,c_543]) ).
cnf(c_983,negated_conjecture,
( v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| k1_filter_0(k1_lattice2(sK1)) = k15_filter_2(sK1,sK0)
| ~ l3_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_968,c_11856]) ).
cnf(c_986,negated_conjecture,
( ~ r2_filter_2(sK1,sK0)
| ~ v1_filter_2(sK0,sK1)
| u1_struct_0(sK1) = sK0 ),
inference(paramod,[status(thm)],[c_974,c_447]) ).
cnf(c_987,negated_conjecture,
( r2_filter_2(sK1,sK0)
| u1_struct_0(sK1) != sK0 ),
inference(paramod,[status(thm)],[c_974,c_445]) ).
cnf(c_11857,negated_conjecture,
( ~ v3_struct_0(k1_lattice2(sK1))
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_444,c_380]) ).
cnf(c_992,negated_conjecture,
~ v3_struct_0(k1_lattice2(sK1)),
inference(resolve,[status(thm)],[c_441,c_11857]) ).
cnf(c_993,plain,
l2_lattices(sK1),
inference(resolve,[status(thm)],[c_444,c_369]) ).
cnf(c_994,plain,
l1_lattices(sK1),
inference(resolve,[status(thm)],[c_444,c_368]) ).
cnf(c_995,plain,
l3_lattices(k1_lattice2(sK1)),
inference(resolve,[status(thm)],[c_444,c_366]) ).
cnf(c_996,plain,
g3_lattices(u1_struct_0(sK1),u1_lattices(sK1),u2_lattices(sK1)) = k1_lattice2(sK1),
inference(resolve,[status(thm)],[c_444,c_361]) ).
cnf(c_11858,negated_conjecture,
( g3_lattices(u1_struct_0(k1_lattice2(sK1)),u2_lattices(k1_lattice2(sK1)),u1_lattices(k1_lattice2(sK1))) = k1_lattice2(sK1)
| ~ l3_lattices(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_444,c_353]) ).
cnf(c_997,negated_conjecture,
g3_lattices(u1_struct_0(k1_lattice2(sK1)),u2_lattices(k1_lattice2(sK1)),u1_lattices(k1_lattice2(sK1))) = k1_lattice2(sK1),
inference(resolve,[status(thm)],[c_995,c_11858]) ).
cnf(c_11859,negated_conjecture,
( v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| k1_filter_0(k1_lattice2(sK1)) = k15_filter_2(sK1,sK0)
| ~ l3_lattices(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_992,c_983]) ).
cnf(c_1002,negated_conjecture,
( v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| k1_filter_0(k1_lattice2(sK1)) = k15_filter_2(sK1,sK0) ),
inference(resolve,[status(thm)],[c_995,c_11859]) ).
cnf(c_11860,negated_conjecture,
( ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_992,c_981]) ).
cnf(c_1004,negated_conjecture,
( ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_995,c_11860]) ).
cnf(c_11861,negated_conjecture,
( k7_filter_2(sK1,k17_filter_2(sK1)) = k15_filter_2(sK1,k17_filter_2(sK1))
| ~ l3_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_455,c_442]) ).
cnf(c_11862,negated_conjecture,
( k7_filter_2(sK1,u1_struct_0(sK1)) = k15_filter_2(sK1,k17_filter_2(sK1))
| ~ l3_lattices(sK1)
| v3_struct_0(sK1) ),
inference(paramod,[status(thm)],[c_974,c_11861]) ).
cnf(c_11863,negated_conjecture,
( k7_filter_2(sK1,u1_struct_0(sK1)) = k15_filter_2(sK1,u1_struct_0(sK1))
| ~ l3_lattices(sK1)
| v3_struct_0(sK1) ),
inference(paramod,[status(thm)],[c_974,c_11862]) ).
cnf(c_11864,negated_conjecture,
( k7_filter_2(sK1,u1_struct_0(sK1)) = k15_filter_2(sK1,u1_struct_0(sK1))
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_441,c_11863]) ).
cnf(c_1026,negated_conjecture,
k7_filter_2(sK1,u1_struct_0(sK1)) = k15_filter_2(sK1,u1_struct_0(sK1)),
inference(resolve,[status(thm)],[c_444,c_11864]) ).
cnf(c_11865,negated_conjecture,
( v1_filter_0(k15_filter_2(sK1,k17_filter_2(sK1)),k1_lattice2(sK1))
| ~ r2_filter_2(sK1,k17_filter_2(sK1))
| ~ l3_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_459,c_442]) ).
cnf(c_11866,negated_conjecture,
( v1_filter_0(k15_filter_2(sK1,k17_filter_2(sK1)),k1_lattice2(sK1))
| ~ r2_filter_2(sK1,u1_struct_0(sK1))
| ~ l3_lattices(sK1)
| v3_struct_0(sK1) ),
inference(paramod,[status(thm)],[c_974,c_11865]) ).
cnf(c_11867,negated_conjecture,
( v1_filter_0(k15_filter_2(sK1,u1_struct_0(sK1)),k1_lattice2(sK1))
| ~ r2_filter_2(sK1,u1_struct_0(sK1))
| ~ l3_lattices(sK1)
| v3_struct_0(sK1) ),
inference(paramod,[status(thm)],[c_974,c_11866]) ).
cnf(c_11868,negated_conjecture,
( v1_filter_0(k15_filter_2(sK1,u1_struct_0(sK1)),k1_lattice2(sK1))
| ~ r2_filter_2(sK1,u1_struct_0(sK1))
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_441,c_11867]) ).
cnf(c_1044,negated_conjecture,
( v1_filter_0(k15_filter_2(sK1,u1_struct_0(sK1)),k1_lattice2(sK1))
| ~ r2_filter_2(sK1,u1_struct_0(sK1)) ),
inference(resolve,[status(thm)],[c_444,c_11868]) ).
cnf(c_1107,plain,
( r2_filter_2(sK1,sK0)
| v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_475,c_446]) ).
cnf(c_11869,negated_conjecture,
( ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| ~ v1_filter_0(k15_filter_2(sK1,k17_filter_2(sK1)),k1_lattice2(sK1))
| k1_filter_0(k1_lattice2(sK1)) != k15_filter_2(sK1,k17_filter_2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_552,c_442]) ).
cnf(c_11870,negated_conjecture,
( ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| ~ v1_filter_0(k15_filter_2(sK1,k17_filter_2(sK1)),k1_lattice2(sK1))
| k1_filter_0(k1_lattice2(sK1)) != k15_filter_2(sK1,u1_struct_0(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(paramod,[status(thm)],[c_974,c_11869]) ).
cnf(c_11871,negated_conjecture,
( ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| ~ v1_filter_0(k15_filter_2(sK1,u1_struct_0(sK1)),k1_lattice2(sK1))
| k1_filter_0(k1_lattice2(sK1)) != k15_filter_2(sK1,u1_struct_0(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(paramod,[status(thm)],[c_974,c_11870]) ).
cnf(c_11872,negated_conjecture,
( ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| ~ v1_filter_0(k15_filter_2(sK1,u1_struct_0(sK1)),k1_lattice2(sK1))
| k1_filter_0(k1_lattice2(sK1)) != k15_filter_2(sK1,u1_struct_0(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_992,c_11871]) ).
cnf(c_11873,negated_conjecture,
( ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| ~ v1_filter_0(k15_filter_2(sK1,u1_struct_0(sK1)),k1_lattice2(sK1))
| k1_filter_0(k1_lattice2(sK1)) != k15_filter_2(sK1,u1_struct_0(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_967,c_11872]) ).
cnf(c_11874,negated_conjecture,
( ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| ~ v1_filter_0(k15_filter_2(sK1,u1_struct_0(sK1)),k1_lattice2(sK1))
| k1_filter_0(k1_lattice2(sK1)) != k15_filter_2(sK1,u1_struct_0(sK1))
| ~ l3_lattices(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_968,c_11873]) ).
cnf(c_11875,negated_conjecture,
( ~ l3_lattices(sK1)
| v3_struct_0(sK1)
| ~ v1_filter_0(k15_filter_2(sK1,u1_struct_0(sK1)),k1_lattice2(sK1))
| k1_filter_0(k1_lattice2(sK1)) != k15_filter_2(sK1,u1_struct_0(sK1)) ),
inference(resolve,[status(thm)],[c_995,c_11874]) ).
cnf(c_11876,negated_conjecture,
( ~ l3_lattices(sK1)
| ~ v1_filter_0(k15_filter_2(sK1,u1_struct_0(sK1)),k1_lattice2(sK1))
| k1_filter_0(k1_lattice2(sK1)) != k15_filter_2(sK1,u1_struct_0(sK1)) ),
inference(resolve,[status(thm)],[c_441,c_11875]) ).
cnf(c_1216,negated_conjecture,
( ~ v1_filter_0(k15_filter_2(sK1,u1_struct_0(sK1)),k1_lattice2(sK1))
| k1_filter_0(k1_lattice2(sK1)) != k15_filter_2(sK1,u1_struct_0(sK1)) ),
inference(resolve,[status(thm)],[c_444,c_11876]) ).
cnf(c_11877,negated_conjecture,
( k7_filter_2(sK1,sK0) = sK0
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_583,c_362]) ).
cnf(c_11878,negated_conjecture,
( k15_filter_2(sK1,sK0) = sK0
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(paramod,[status(thm)],[c_481,c_11877]) ).
cnf(c_11879,negated_conjecture,
( k15_filter_2(sK1,sK0) = sK0
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_441,c_11878]) ).
cnf(c_11880,negated_conjecture,
( k15_filter_2(sK1,sK0) = sK0
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_442,c_11879]) ).
cnf(c_1317,negated_conjecture,
k15_filter_2(sK1,sK0) = sK0,
inference(resolve,[status(thm)],[c_444,c_11880]) ).
cnf(c_1318,plain,
( r2_filter_2(sK1,sK0)
| v2_filter_0(sK0,k1_lattice2(sK1)) ),
inference(paramod,[status(thm)],[c_1317,c_1107]) ).
cnf(c_11881,negated_conjecture,
( ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| v2_filter_0(sK0,k1_lattice2(sK1)) ),
inference(paramod,[status(thm)],[c_1317,c_1004]) ).
cnf(c_1319,negated_conjecture,
( ~ v1_filter_0(sK0,k1_lattice2(sK1))
| v2_filter_0(sK0,k1_lattice2(sK1)) ),
inference(paramod,[status(thm)],[c_1317,c_11881]) ).
cnf(c_11882,negated_conjecture,
( v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ v2_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| k1_filter_0(k1_lattice2(sK1)) = sK0 ),
inference(paramod,[status(thm)],[c_1317,c_1002]) ).
cnf(c_11883,negated_conjecture,
( v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ v2_filter_0(sK0,k1_lattice2(sK1))
| k1_filter_0(k1_lattice2(sK1)) = sK0 ),
inference(paramod,[status(thm)],[c_1317,c_11882]) ).
cnf(c_1321,negated_conjecture,
( v1_filter_0(sK0,k1_lattice2(sK1))
| ~ v2_filter_0(sK0,k1_lattice2(sK1))
| k1_filter_0(k1_lattice2(sK1)) = sK0 ),
inference(paramod,[status(thm)],[c_1317,c_11883]) ).
cnf(c_1324,negated_conjecture,
( v1_filter_0(sK0,k1_lattice2(sK1))
| ~ r2_filter_2(sK1,sK0) ),
inference(paramod,[status(thm)],[c_1317,c_479]) ).
cnf(c_1325,negated_conjecture,
( ~ v1_filter_0(sK0,k1_lattice2(sK1))
| r2_filter_2(sK1,sK0) ),
inference(paramod,[status(thm)],[c_1317,c_477]) ).
cnf(c_1327,negated_conjecture,
( ~ v2_filter_0(sK0,k1_lattice2(sK1))
| v1_filter_2(sK0,sK1) ),
inference(paramod,[status(thm)],[c_1317,c_473]) ).
cnf(c_11884,negated_conjecture,
( k7_filter_2(sK1,u1_struct_0(sK1)) = u1_struct_0(sK1)
| ~ l3_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_607,c_442]) ).
cnf(c_11885,negated_conjecture,
( k15_filter_2(sK1,u1_struct_0(sK1)) = u1_struct_0(sK1)
| ~ l3_lattices(sK1)
| v3_struct_0(sK1) ),
inference(paramod,[status(thm)],[c_1026,c_11884]) ).
cnf(c_11886,negated_conjecture,
( k15_filter_2(sK1,u1_struct_0(sK1)) = u1_struct_0(sK1)
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_441,c_11885]) ).
cnf(c_1397,negated_conjecture,
k15_filter_2(sK1,u1_struct_0(sK1)) = u1_struct_0(sK1),
inference(resolve,[status(thm)],[c_444,c_11886]) ).
cnf(c_11887,negated_conjecture,
( ~ v1_filter_0(k15_filter_2(sK1,u1_struct_0(sK1)),k1_lattice2(sK1))
| k1_filter_0(k1_lattice2(sK1)) != u1_struct_0(sK1) ),
inference(paramod,[status(thm)],[c_1397,c_1216]) ).
cnf(c_1407,negated_conjecture,
( ~ v1_filter_0(u1_struct_0(sK1),k1_lattice2(sK1))
| k1_filter_0(k1_lattice2(sK1)) != u1_struct_0(sK1) ),
inference(paramod,[status(thm)],[c_1397,c_11887]) ).
cnf(c_1413,negated_conjecture,
( v1_filter_0(u1_struct_0(sK1),k1_lattice2(sK1))
| ~ r2_filter_2(sK1,u1_struct_0(sK1)) ),
inference(paramod,[status(thm)],[c_1397,c_1044]) ).
cnf(c_1643,plain,
v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)),
inference(resolve,[status(thm)],[c_993,c_373]) ).
cnf(c_1644,plain,
v1_funct_1(u2_lattices(sK1)),
inference(resolve,[status(thm)],[c_993,c_372]) ).
cnf(c_1647,plain,
m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)),
inference(resolve,[status(thm)],[c_993,c_299]) ).
cnf(c_1649,plain,
v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)),
inference(resolve,[status(thm)],[c_994,c_371]) ).
cnf(c_1650,plain,
v1_funct_1(u1_lattices(sK1)),
inference(resolve,[status(thm)],[c_994,c_370]) ).
cnf(c_1651,plain,
m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)),
inference(resolve,[status(thm)],[c_994,c_298]) ).
cnf(c_11888,plain,
( k1_filter_0(k1_lattice2(sK1)) = u1_struct_0(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_967,c_359]) ).
cnf(c_11889,plain,
( k1_filter_0(k1_lattice2(sK1)) = u1_struct_0(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_992,c_11888]) ).
cnf(c_2472,plain,
k1_filter_0(k1_lattice2(sK1)) = u1_struct_0(k1_lattice2(sK1)),
inference(resolve,[status(thm)],[c_995,c_11889]) ).
cnf(c_2496,negated_conjecture,
( ~ v1_filter_0(u1_struct_0(sK1),k1_lattice2(sK1))
| u1_struct_0(k1_lattice2(sK1)) != u1_struct_0(sK1) ),
inference(paramod,[status(thm)],[c_2472,c_1407]) ).
cnf(c_2497,negated_conjecture,
( v1_filter_0(sK0,k1_lattice2(sK1))
| ~ v2_filter_0(sK0,k1_lattice2(sK1))
| u1_struct_0(k1_lattice2(sK1)) = sK0 ),
inference(paramod,[status(thm)],[c_2472,c_1321]) ).
cnf(c_3877,plain,
( v2_filter_0(sK0,k1_lattice2(sK1))
| v1_filter_0(sK0,k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_1324,c_1318]) ).
cnf(c_11890,plain,
( A = u1_struct_0(sK1)
| g3_lattices(A,B,C) != k1_lattice2(sK1)
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_1(u2_lattices(sK1))
| ~ m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_1(u1_lattices(sK1)) ),
inference(paramod,[status(thm)],[c_996,c_391]) ).
cnf(c_11891,plain,
( u1_struct_0(sK1) = A
| g3_lattices(A,B,C) != k1_lattice2(sK1)
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_1(u2_lattices(sK1))
| ~ m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_1(u1_lattices(sK1)) ),
inference(copy,[status(thm)],[c_11890]) ).
cnf(c_11892,plain,
( u1_struct_0(sK1) = A
| g3_lattices(A,B,C) != k1_lattice2(sK1)
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_1(u2_lattices(sK1))
| ~ m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_2(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
inference(resolve,[status(thm)],[c_1650,c_11891]) ).
cnf(c_11893,plain,
( u1_struct_0(sK1) = A
| g3_lattices(A,B,C) != k1_lattice2(sK1)
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_1(u2_lattices(sK1))
| ~ m1_relset_1(u1_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
inference(resolve,[status(thm)],[c_1649,c_11892]) ).
cnf(c_11894,plain,
( u1_struct_0(sK1) = A
| g3_lattices(A,B,C) != k1_lattice2(sK1)
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_1(u2_lattices(sK1)) ),
inference(resolve,[status(thm)],[c_1651,c_11893]) ).
cnf(c_11895,plain,
( u1_struct_0(sK1) = A
| g3_lattices(A,B,C) != k1_lattice2(sK1)
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1))
| ~ v1_funct_2(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
inference(resolve,[status(thm)],[c_1644,c_11894]) ).
cnf(c_11896,plain,
( u1_struct_0(sK1) = A
| g3_lattices(A,B,C) != k1_lattice2(sK1)
| ~ m1_relset_1(u2_lattices(sK1),k2_zfmisc_1(u1_struct_0(sK1),u1_struct_0(sK1)),u1_struct_0(sK1)) ),
inference(resolve,[status(thm)],[c_1643,c_11895]) ).
cnf(c_6151,plain,
( u1_struct_0(sK1) = A
| g3_lattices(A,B,C) != k1_lattice2(sK1) ),
inference(resolve,[status(thm)],[c_1647,c_11896]) ).
cnf(c_11897,plain,
u1_struct_0(sK1) = u1_struct_0(k1_lattice2(sK1)),
inference(resolve,[status(thm)],[c_6151,c_997]) ).
cnf(c_8212,plain,
u1_struct_0(k1_lattice2(sK1)) = u1_struct_0(sK1),
inference(copy,[status(thm)],[c_11897]) ).
cnf(c_8232,negated_conjecture,
( v1_filter_0(sK0,k1_lattice2(sK1))
| ~ v2_filter_0(sK0,k1_lattice2(sK1))
| u1_struct_0(sK1) = sK0 ),
inference(paramod,[status(thm)],[c_8212,c_2497]) ).
cnf(c_11898,negated_conjecture,
( ~ v1_filter_0(u1_struct_0(sK1),k1_lattice2(sK1))
| u1_struct_0(sK1) != u1_struct_0(sK1) ),
inference(paramod,[status(thm)],[c_8212,c_2496]) ).
cnf(c_8233,negated_conjecture,
~ v1_filter_0(u1_struct_0(sK1),k1_lattice2(sK1)),
inference(copy,[status(thm)],[c_11898]) ).
cnf(c_8256,negated_conjecture,
~ r2_filter_2(sK1,u1_struct_0(sK1)),
inference(resolve,[status(thm)],[c_8233,c_1413]) ).
cnf(c_11899,negated_conjecture,
( v1_filter_0(sK0,k1_lattice2(sK1))
| v1_filter_0(sK0,k1_lattice2(sK1))
| u1_struct_0(sK1) = sK0 ),
inference(resolve,[status(thm)],[c_8232,c_3877]) ).
cnf(c_11483,negated_conjecture,
( v1_filter_0(sK0,k1_lattice2(sK1))
| u1_struct_0(sK1) = sK0 ),
inference(copy,[status(thm)],[c_11899]) ).
cnf(c_11484,plain,
( r2_filter_2(sK1,sK0)
| u1_struct_0(sK1) = sK0 ),
inference(resolve,[status(thm)],[c_11483,c_1325]) ).
cnf(c_11485,plain,
( v2_filter_0(sK0,k1_lattice2(sK1))
| u1_struct_0(sK1) = sK0 ),
inference(resolve,[status(thm)],[c_11483,c_1319]) ).
cnf(c_11900,negated_conjecture,
( ~ v1_filter_2(sK0,sK1)
| u1_struct_0(sK1) = sK0
| u1_struct_0(sK1) = sK0 ),
inference(resolve,[status(thm)],[c_11484,c_986]) ).
cnf(c_11486,negated_conjecture,
( ~ v1_filter_2(sK0,sK1)
| u1_struct_0(sK1) = sK0 ),
inference(copy,[status(thm)],[c_11900]) ).
cnf(c_11487,plain,
( v1_filter_2(sK0,sK1)
| u1_struct_0(sK1) = sK0 ),
inference(resolve,[status(thm)],[c_11485,c_1327]) ).
cnf(c_11901,plain,
( u1_struct_0(sK1) = sK0
| u1_struct_0(sK1) = sK0 ),
inference(resolve,[status(thm)],[c_11487,c_11486]) ).
cnf(c_11488,plain,
u1_struct_0(sK1) = sK0,
inference(copy,[status(thm)],[c_11901]) ).
cnf(c_11708,negated_conjecture,
~ r2_filter_2(sK1,sK0),
inference(paramod,[status(thm)],[c_11488,c_8256]) ).
cnf(c_11902,negated_conjecture,
( r2_filter_2(sK1,sK0)
| sK0 != sK0 ),
inference(paramod,[status(thm)],[c_11488,c_987]) ).
cnf(c_11903,negated_conjecture,
r2_filter_2(sK1,sK0),
inference(copy,[status(thm)],[c_11902]) ).
cnf(c_11811,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_11708,c_11903]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT322+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.08/0.35 % Computer : n011.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Fri Sep 25 20:51:28 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.35 % Process 2856142 was started by sandbox2 on n011,
% 0.08/0.35 % Fri Sep 25 20:51:28 2026
% 0.08/0.35 % 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).
% 30.99/4.93
% 30.99/4.93 % given #500 (T,wt=15): 1601 v1_xboole_0(u1_struct_0(c14)) | -v3_struct_0(c14). [back_unit_del(1553),unit_del(b,1598),unit_del(c,1597),unit_del(d,1599)].
% 30.99/4.93
% 30.99/4.93 % given #1000 (A,wt=26): 1056 r2_filter_2(c7,f5(c7)) | -v1_filter_0(k15_filter_2(c7,f5(c7)),k1_lattice2(c7)). [resolve(461,b,405,a),unit_del(a,404),unit_del(b,403)].
% 30.99/4.93
% 30.99/4.93 % given #1500 (F,wt=30): 7154 -v17_lattices(k1_lattice2(c7)) | f1(k1_lattice2(c7)) != u1_struct_0(c7) | -v1_filter_0(f1(k1_lattice2(c7)),k1_lattice2(c7)). [back_rewrite(2045),rewrite([7123(9)])].
% 30.99/4.93
% 30.99/4.93 % given #2000 (F,wt=38): 10179 -r2_hidden(A,u2_lattices(c18)) | -v1_xboole_0(k2_zfmisc_1(k2_zfmisc_1(u1_struct_0(c18),u1_struct_0(c18)),u1_struct_0(c18))). [resolve(1648,a,437,b)].
% 30.99/4.93
% 30.99/4.93 % SZS status Theorem for theBenchmark
% 30.99/4.93
% 30.99/4.93 % Proof 1 at 3.45 (+ 0.40) seconds.
% 30.99/4.93 % Length of proof is 155.
% 30.99/4.93 % Level of proof is 16.
% 30.99/4.93 % Maximum clause weight is 50.000.
% 30.99/4.93 % Given clauses 2146.
% 30.99/4.93
% 30.99/4.93 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------