%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT311+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 : n009.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:09 AM UTC 2026
% Result : Theorem 108.57s 14.45s
% Output : CNFRefutation 108.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 21
% Syntax : Number of formulae : 157 ( 38 unt; 0 def)
% Number of atoms : 522 ( 71 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 600 ( 235 ~; 249 |; 79 &)
% ( 1 <=>; 36 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 1 prp; 0-3 aty)
% Number of functors : 21 ( 21 usr; 3 con; 0-3 aty)
% Number of variables : 116 ( 1 sgn 45 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
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(d3_filter_0,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> k2_filter_0(A,B) = a_2_0_filter_0(A,B) ) ),
file('theBenchmark.p',d3_filter_0) ).
fof(d4_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> k5_filter_2(A,B) = B ) ),
file('theBenchmark.p',d4_filter_2) ).
fof(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(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_k1_lattice2,axiom,
! [A] :
( l3_lattices(A)
=> ( l3_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) ) ),
file('theBenchmark.p',dt_k1_lattice2) ).
fof(dt_k5_filter_2,axiom,
! [A,B] :
( ( m1_subset_1(B,u1_struct_0(A))
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k5_filter_2(A,B),u1_struct_0(k1_lattice2(A))) ),
file('theBenchmark.p',dt_k5_filter_2) ).
fof(dt_k7_filter_2,axiom,
! [A,B] :
( ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k7_filter_2(A,B),k1_zfmisc_1(u1_struct_0(k1_lattice2(A)))) ),
file('theBenchmark.p',dt_k7_filter_2) ).
fof(dt_l3_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( l2_lattices(A)
& l1_lattices(A) ) ),
file('theBenchmark.p',dt_l3_lattices) ).
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(fc3_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)
& ~ v1_xboole_0(A) )
=> ( v3_lattices(g3_lattices(A,B,C))
& ~ v3_struct_0(g3_lattices(A,B,C)) ) ),
file('theBenchmark.p',fc3_lattices) ).
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_k2_filter_2,axiom,
! [A,B] :
( ( m1_subset_1(B,u1_struct_0(A))
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k2_filter_2(A,B) = k2_filter_0(A,B) ),
file('theBenchmark.p',redefinition_k2_filter_2) ).
fof(redefinition_k3_filter_2,axiom,
! [A,B] :
( ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
& ~ v1_xboole_0(B)
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k3_filter_2(A,B) = k3_filter_0(A,B) ),
file('theBenchmark.p',redefinition_k3_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(t29_filter_0,axiom,
! [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,k1_zfmisc_1(u1_struct_0(A)))
& ~ v1_xboole_0(C) )
=> ( r2_hidden(B,C)
=> r1_tarski(k2_filter_0(A,B),k3_filter_0(A,C)) ) ) ) ),
file('theBenchmark.p',t29_filter_0) ).
fof(t30_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(k1_lattice2(A),k5_filter_2(A,B)) = k2_filter_2(A,B)
& k18_filter_2(A,B) = k2_filter_2(k1_lattice2(A),k5_filter_2(A,B)) ) ) ),
file('theBenchmark.p',t30_filter_2) ).
fof(t37_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)))
& ~ v1_xboole_0(B) )
=> ! [C] :
( ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(k1_lattice2(A))))
& ~ v1_xboole_0(C) )
=> ( k3_filter_2(k1_lattice2(A),C) = k19_filter_2(A,k8_filter_2(A,C))
& k3_filter_2(A,k8_filter_2(A,C)) = k19_filter_2(k1_lattice2(A),C)
& k3_filter_2(A,B) = k19_filter_2(k1_lattice2(A),k7_filter_2(A,B))
& k3_filter_2(k1_lattice2(A),k7_filter_2(A,B)) = k19_filter_2(A,B) ) ) ) ),
file('theBenchmark.p',t37_filter_2) ).
fof(t5_subset,axiom,
! [A,B,C] :
~ ( v1_xboole_0(C)
& m1_subset_1(B,k1_zfmisc_1(C))
& r2_hidden(A,B) ),
file('theBenchmark.p',t5_subset) ).
fof(t40_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,k1_zfmisc_1(u1_struct_0(A)))
& ~ v1_xboole_0(C) )
=> ( r2_hidden(B,C)
=> r1_tarski(k18_filter_2(A,B),k19_filter_2(A,C)) ) ) ) ),
file('theBenchmark.p',t40_filter_2) ).
fof(t40_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,k1_zfmisc_1(u1_struct_0(A)))
& ~ v1_xboole_0(C) )
=> ( r2_hidden(B,C)
=> r1_tarski(k18_filter_2(A,B),k19_filter_2(A,C)) ) ) ) ),
inference(assume_negation,[status(cth)],[t40_filter_2]) ).
cnf(c_161,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_162,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_163,plain,
( v1_funct_1(u1_lattices(A))
| ~ l1_lattices(A) ),
inference(clausify,[status(thm)],[dt_u1_lattices]) ).
cnf(c_164,plain,
( l1_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_188,plain,
( m2_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
| ~ l3_lattices(A) ),
inference(resolve,[status(thm)],[c_164,c_161]) ).
cnf(c_189,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_191,plain,
( m1_relset_1(A,B,C)
| ~ m2_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_m2_relset_1]) ).
cnf(c_201,plain,
( ~ l2_lattices(A)
| m1_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ),
inference(resolve,[status(thm)],[c_191,c_189]) ).
cnf(c_202,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_203,plain,
( v1_funct_1(u2_lattices(A))
| ~ l2_lattices(A) ),
inference(clausify,[status(thm)],[dt_u2_lattices]) ).
cnf(c_204,plain,
( l2_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_236,plain,
( m1_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
| ~ l3_lattices(A) ),
inference(resolve,[status(thm)],[c_204,c_201]) ).
cnf(c_241,plain,
( v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
| ~ l3_lattices(A) ),
inference(resolve,[status(thm)],[c_204,c_202]) ).
cnf(c_242,plain,
( v1_funct_1(u2_lattices(A))
| ~ l3_lattices(A) ),
inference(resolve,[status(thm)],[c_204,c_203]) ).
cnf(c_266,plain,
( v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
| ~ l3_lattices(A) ),
inference(resolve,[status(thm)],[c_164,c_162]) ).
cnf(c_267,plain,
( v1_funct_1(u1_lattices(A))
| ~ l3_lattices(A) ),
inference(resolve,[status(thm)],[c_164,c_163]) ).
cnf(c_291,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_292,plain,
( g3_lattices(u1_struct_0(A),u1_lattices(A),u2_lattices(A)) = k1_lattice2(A)
| ~ l3_lattices(A) ),
inference(copy,[status(thm)],[c_291]) ).
cnf(c_293,plain,
( a_2_0_filter_0(A,B) = k2_filter_0(A,B)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d3_filter_0]) ).
cnf(c_294,plain,
( k2_filter_0(A,B) = a_2_0_filter_0(A,B)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_293]) ).
cnf(c_295,plain,
( k5_filter_2(A,B) = B
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d4_filter_2]) ).
cnf(c_296,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_298,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_299,plain,
( k18_filter_2(A,B) = 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(copy,[status(thm)],[c_298]) ).
cnf(c_301,plain,
( l3_lattices(k1_lattice2(A))
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_k1_lattice2]) ).
cnf(c_302,plain,
( m1_subset_1(k5_filter_2(A,B),u1_struct_0(k1_lattice2(A)))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k5_filter_2]) ).
cnf(c_303,plain,
( m1_subset_1(k7_filter_2(A,B),k1_zfmisc_1(u1_struct_0(k1_lattice2(A))))
| ~ 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)],[dt_k7_filter_2]) ).
cnf(c_313,plain,
( ~ v3_struct_0(g3_lattices(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)
| v1_xboole_0(A) ),
inference(clausify,[status(thm)],[fc3_lattices]) ).
cnf(c_320,plain,
( v10_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc6_lattice2]) ).
cnf(c_351,plain,
( k2_filter_2(A,B) = k2_filter_0(A,B)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[redefinition_k2_filter_2]) ).
cnf(c_352,plain,
( k3_filter_2(A,B) = k3_filter_0(A,B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[redefinition_k3_filter_2]) ).
cnf(c_353,plain,
( k3_filter_0(A,B) = k3_filter_2(A,B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_352]) ).
cnf(c_356,plain,
( r1_tarski(k2_filter_0(A,B),k3_filter_0(A,C))
| ~ r2_hidden(B,C)
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
| v1_xboole_0(C)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t29_filter_0]) ).
cnf(c_360,plain,
( k2_filter_2(k1_lattice2(A),k5_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)],[t30_filter_2]) ).
cnf(c_363,plain,
( k3_filter_2(k1_lattice2(A),k7_filter_2(A,B)) = k19_filter_2(A,B)
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(k1_lattice2(A))))
| v1_xboole_0(C)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t37_filter_2]) ).
cnf(c_372,plain,
( ~ v1_xboole_0(C)
| ~ m1_subset_1(B,k1_zfmisc_1(C))
| ~ r2_hidden(A,B) ),
inference(clausify,[status(thm)],[t5_subset]) ).
fof(nnf_100,plain,
? [A] :
( ? [B] :
( ? [C] :
( ~ r1_tarski(k18_filter_2(A,B),k19_filter_2(A,C))
& r2_hidden(B,C)
& m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
& ~ v1_xboole_0(C) )
& m1_subset_1(B,u1_struct_0(A)) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t40_filter_2_neg]) ).
fof(sk_t40_filter_2_neg,plain,
( ~ r1_tarski(k18_filter_2(sK0,sK1),k19_filter_2(sK0,sK2))
& r2_hidden(sK1,sK2)
& m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0)))
& ~ v1_xboole_0(sK2)
& 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_100]) ).
cnf(c_376,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t40_filter_2_neg]) ).
cnf(c_377,negated_conjecture,
v10_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t40_filter_2_neg]) ).
cnf(c_378,negated_conjecture,
l3_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t40_filter_2_neg]) ).
cnf(c_379,negated_conjecture,
m1_subset_1(sK1,u1_struct_0(sK0)),
inference(split_conjunct,[status(thm)],[sk_t40_filter_2_neg]) ).
cnf(c_380,negated_conjecture,
~ v1_xboole_0(sK2),
inference(split_conjunct,[status(thm)],[sk_t40_filter_2_neg]) ).
cnf(c_381,negated_conjecture,
m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0))),
inference(split_conjunct,[status(thm)],[sk_t40_filter_2_neg]) ).
cnf(c_382,negated_conjecture,
r2_hidden(sK1,sK2),
inference(split_conjunct,[status(thm)],[sk_t40_filter_2_neg]) ).
cnf(c_383,negated_conjecture,
~ r1_tarski(k18_filter_2(sK0,sK1),k19_filter_2(sK0,sK2)),
inference(split_conjunct,[status(thm)],[sk_t40_filter_2_neg]) ).
cnf(c_430,plain,
( ~ l3_lattices(A)
| m1_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ),
inference(resolve,[status(thm)],[c_191,c_188]) ).
cnf(c_448,plain,
( k3_filter_2(k1_lattice2(A),k7_filter_2(A,B)) = k19_filter_2(A,B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k1_lattice2(A))))
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(factor,[status(thm)],[c_363]) ).
cnf(c_5244,negated_conjecture,
( v10_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_377,c_320]) ).
cnf(c_5245,negated_conjecture,
( v10_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_376,c_5244]) ).
cnf(c_671,negated_conjecture,
v10_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_378,c_5245]) ).
cnf(c_687,plain,
l3_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_378,c_301]) ).
cnf(c_688,plain,
g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0)) = k1_lattice2(sK0),
inference(resolve,[status(thm)],[c_378,c_292]) ).
cnf(c_689,plain,
v1_funct_1(u1_lattices(sK0)),
inference(resolve,[status(thm)],[c_378,c_267]) ).
cnf(c_690,plain,
v1_funct_2(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_378,c_266]) ).
cnf(c_691,plain,
v1_funct_1(u2_lattices(sK0)),
inference(resolve,[status(thm)],[c_378,c_242]) ).
cnf(c_692,plain,
v1_funct_2(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_378,c_241]) ).
cnf(c_695,plain,
m1_relset_1(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_378,c_236]) ).
cnf(c_5246,negated_conjecture,
( k2_filter_2(k1_lattice2(sK0),k5_filter_2(sK0,sK1)) = k18_filter_2(sK0,sK1)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_379,c_360]) ).
cnf(c_5247,negated_conjecture,
( k2_filter_2(k1_lattice2(sK0),k5_filter_2(sK0,sK1)) = k18_filter_2(sK0,sK1)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_376,c_5246]) ).
cnf(c_5248,negated_conjecture,
( k2_filter_2(k1_lattice2(sK0),k5_filter_2(sK0,sK1)) = k18_filter_2(sK0,sK1)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_377,c_5247]) ).
cnf(c_697,negated_conjecture,
k2_filter_2(k1_lattice2(sK0),k5_filter_2(sK0,sK1)) = k18_filter_2(sK0,sK1),
inference(resolve,[status(thm)],[c_378,c_5248]) ).
cnf(c_5249,negated_conjecture,
( m1_subset_1(k5_filter_2(sK0,sK1),u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_379,c_302]) ).
cnf(c_5250,negated_conjecture,
( m1_subset_1(k5_filter_2(sK0,sK1),u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_376,c_5249]) ).
cnf(c_5251,negated_conjecture,
( m1_subset_1(k5_filter_2(sK0,sK1),u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_377,c_5250]) ).
cnf(c_700,negated_conjecture,
m1_subset_1(k5_filter_2(sK0,sK1),u1_struct_0(k1_lattice2(sK0))),
inference(resolve,[status(thm)],[c_378,c_5251]) ).
cnf(c_5252,negated_conjecture,
( k18_filter_2(sK0,sK1) = a_2_0_filter_2(sK0,sK1)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_379,c_299]) ).
cnf(c_5253,negated_conjecture,
( k18_filter_2(sK0,sK1) = a_2_0_filter_2(sK0,sK1)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_376,c_5252]) ).
cnf(c_5254,negated_conjecture,
( k18_filter_2(sK0,sK1) = a_2_0_filter_2(sK0,sK1)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_377,c_5253]) ).
cnf(c_701,negated_conjecture,
k18_filter_2(sK0,sK1) = a_2_0_filter_2(sK0,sK1),
inference(resolve,[status(thm)],[c_378,c_5254]) ).
cnf(c_5255,negated_conjecture,
( k5_filter_2(sK0,sK1) = sK1
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_379,c_295]) ).
cnf(c_5256,negated_conjecture,
( k5_filter_2(sK0,sK1) = sK1
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_376,c_5255]) ).
cnf(c_5257,negated_conjecture,
( k5_filter_2(sK0,sK1) = sK1
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_377,c_5256]) ).
cnf(c_702,negated_conjecture,
k5_filter_2(sK0,sK1) = sK1,
inference(resolve,[status(thm)],[c_378,c_5257]) ).
cnf(c_5258,negated_conjecture,
k2_filter_2(k1_lattice2(sK0),sK1) = k18_filter_2(sK0,sK1),
inference(paramod,[status(thm)],[c_702,c_697]) ).
cnf(c_708,negated_conjecture,
k2_filter_2(k1_lattice2(sK0),sK1) = a_2_0_filter_2(sK0,sK1),
inference(paramod,[status(thm)],[c_701,c_5258]) ).
cnf(c_709,negated_conjecture,
~ r1_tarski(a_2_0_filter_2(sK0,sK1),k19_filter_2(sK0,sK2)),
inference(paramod,[status(thm)],[c_701,c_383]) ).
cnf(c_710,negated_conjecture,
m1_subset_1(sK1,u1_struct_0(k1_lattice2(sK0))),
inference(paramod,[status(thm)],[c_702,c_700]) ).
cnf(c_5259,negated_conjecture,
( m1_subset_1(k7_filter_2(sK0,sK2),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_381,c_303]) ).
cnf(c_5260,negated_conjecture,
( m1_subset_1(k7_filter_2(sK0,sK2),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_376,c_5259]) ).
cnf(c_5261,negated_conjecture,
( m1_subset_1(k7_filter_2(sK0,sK2),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_377,c_5260]) ).
cnf(c_720,negated_conjecture,
m1_subset_1(k7_filter_2(sK0,sK2),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0)))),
inference(resolve,[status(thm)],[c_378,c_5261]) ).
cnf(c_5262,negated_conjecture,
( k7_filter_2(sK0,sK2) = sK2
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_381,c_296]) ).
cnf(c_5263,negated_conjecture,
( k7_filter_2(sK0,sK2) = sK2
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_376,c_5262]) ).
cnf(c_5264,negated_conjecture,
( k7_filter_2(sK0,sK2) = sK2
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_377,c_5263]) ).
cnf(c_721,negated_conjecture,
k7_filter_2(sK0,sK2) = sK2,
inference(resolve,[status(thm)],[c_378,c_5264]) ).
cnf(c_725,negated_conjecture,
m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0)))),
inference(paramod,[status(thm)],[c_721,c_720]) ).
cnf(c_728,plain,
( ~ v1_xboole_0(A)
| ~ m1_subset_1(sK2,k1_zfmisc_1(A)) ),
inference(resolve,[status(thm)],[c_382,c_372]) ).
cnf(c_5265,negated_conjecture,
( r1_tarski(k2_filter_0(A,sK1),k3_filter_0(A,sK2))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(A)))
| v1_xboole_0(sK2)
| ~ m1_subset_1(sK1,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_382,c_356]) ).
cnf(c_730,negated_conjecture,
( r1_tarski(k2_filter_0(A,sK1),k3_filter_0(A,sK2))
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(sK1,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_380,c_5265]) ).
cnf(c_812,plain,
m1_relset_1(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_430,c_378]) ).
cnf(c_836,plain,
~ v1_xboole_0(u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_728,c_381]) ).
cnf(c_5266,plain,
( k2_filter_2(k1_lattice2(sK0),sK1) = k2_filter_0(k1_lattice2(sK0),sK1)
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_710,c_351]) ).
cnf(c_5267,plain,
( a_2_0_filter_2(sK0,sK1) = k2_filter_0(k1_lattice2(sK0),sK1)
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(paramod,[status(thm)],[c_708,c_5266]) ).
cnf(c_5268,plain,
( k2_filter_0(k1_lattice2(sK0),sK1) = a_2_0_filter_2(sK0,sK1)
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(copy,[status(thm)],[c_5267]) ).
cnf(c_5269,plain,
( k2_filter_0(k1_lattice2(sK0),sK1) = a_2_0_filter_2(sK0,sK1)
| ~ l3_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_671,c_5268]) ).
cnf(c_1087,plain,
( k2_filter_0(k1_lattice2(sK0),sK1) = a_2_0_filter_2(sK0,sK1)
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_687,c_5269]) ).
cnf(c_5270,plain,
( k2_filter_0(k1_lattice2(sK0),sK1) = a_2_0_filter_0(k1_lattice2(sK0),sK1)
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_710,c_294]) ).
cnf(c_5271,plain,
( k2_filter_0(k1_lattice2(sK0),sK1) = a_2_0_filter_0(k1_lattice2(sK0),sK1)
| ~ l3_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_671,c_5270]) ).
cnf(c_1091,plain,
( k2_filter_0(k1_lattice2(sK0),sK1) = a_2_0_filter_0(k1_lattice2(sK0),sK1)
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_687,c_5271]) ).
cnf(c_5272,plain,
( k3_filter_2(k1_lattice2(sK0),k7_filter_2(sK0,sK2)) = k19_filter_2(sK0,sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0)))
| v1_xboole_0(sK2)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_725,c_448]) ).
cnf(c_5273,plain,
( k3_filter_2(k1_lattice2(sK0),sK2) = k19_filter_2(sK0,sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0)))
| v1_xboole_0(sK2)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(paramod,[status(thm)],[c_721,c_5272]) ).
cnf(c_5274,plain,
( k19_filter_2(sK0,sK2) = k3_filter_2(k1_lattice2(sK0),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0)))
| v1_xboole_0(sK2)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_5273]) ).
cnf(c_5275,negated_conjecture,
( k19_filter_2(sK0,sK2) = k3_filter_2(k1_lattice2(sK0),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0)))
| v1_xboole_0(sK2)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_376,c_5274]) ).
cnf(c_5276,negated_conjecture,
( k19_filter_2(sK0,sK2) = k3_filter_2(k1_lattice2(sK0),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0)))
| v1_xboole_0(sK2)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_377,c_5275]) ).
cnf(c_5277,negated_conjecture,
( k19_filter_2(sK0,sK2) = k3_filter_2(k1_lattice2(sK0),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0)))
| v1_xboole_0(sK2) ),
inference(resolve,[status(thm)],[c_378,c_5276]) ).
cnf(c_5278,negated_conjecture,
( k19_filter_2(sK0,sK2) = k3_filter_2(k1_lattice2(sK0),sK2)
| ~ m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_380,c_5277]) ).
cnf(c_1531,negated_conjecture,
k19_filter_2(sK0,sK2) = k3_filter_2(k1_lattice2(sK0),sK2),
inference(resolve,[status(thm)],[c_381,c_5278]) ).
cnf(c_5279,plain,
( k3_filter_0(k1_lattice2(sK0),sK2) = k3_filter_2(k1_lattice2(sK0),sK2)
| v1_xboole_0(sK2)
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_725,c_353]) ).
cnf(c_5280,plain,
( k3_filter_0(k1_lattice2(sK0),sK2) = k3_filter_2(k1_lattice2(sK0),sK2)
| v1_xboole_0(sK2)
| ~ l3_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_671,c_5279]) ).
cnf(c_5281,plain,
( k3_filter_0(k1_lattice2(sK0),sK2) = k3_filter_2(k1_lattice2(sK0),sK2)
| v1_xboole_0(sK2)
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_687,c_5280]) ).
cnf(c_1541,negated_conjecture,
( k3_filter_0(k1_lattice2(sK0),sK2) = k3_filter_2(k1_lattice2(sK0),sK2)
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_380,c_5281]) ).
cnf(c_1555,negated_conjecture,
~ r1_tarski(a_2_0_filter_2(sK0,sK1),k3_filter_2(k1_lattice2(sK0),sK2)),
inference(paramod,[status(thm)],[c_1531,c_709]) ).
cnf(c_5282,plain,
( ~ v3_struct_0(g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),A))
| ~ m1_relset_1(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ m1_relset_1(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(u1_lattices(sK0))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_690,c_313]) ).
cnf(c_5283,plain,
( ~ v3_struct_0(g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),A))
| ~ m1_relset_1(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ m1_relset_1(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(u1_lattices(sK0)) ),
inference(resolve,[status(thm)],[c_836,c_5282]) ).
cnf(c_5284,plain,
( ~ v3_struct_0(g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),A))
| ~ m1_relset_1(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ m1_relset_1(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_689,c_5283]) ).
cnf(c_3760,plain,
( ~ v3_struct_0(g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),A))
| ~ m1_relset_1(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(A) ),
inference(resolve,[status(thm)],[c_812,c_5284]) ).
cnf(c_5285,plain,
( ~ v3_struct_0(g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0)))
| ~ m1_relset_1(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(u2_lattices(sK0)) ),
inference(resolve,[status(thm)],[c_692,c_3760]) ).
cnf(c_5286,plain,
( ~ v3_struct_0(k1_lattice2(sK0))
| ~ m1_relset_1(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(u2_lattices(sK0)) ),
inference(paramod,[status(thm)],[c_688,c_5285]) ).
cnf(c_5287,plain,
( ~ v3_struct_0(k1_lattice2(sK0))
| ~ m1_relset_1(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_691,c_5286]) ).
cnf(c_3787,plain,
~ v3_struct_0(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_695,c_5287]) ).
cnf(c_4096,negated_conjecture,
k3_filter_0(k1_lattice2(sK0),sK2) = k3_filter_2(k1_lattice2(sK0),sK2),
inference(resolve,[status(thm)],[c_3787,c_1541]) ).
cnf(c_4110,plain,
k2_filter_0(k1_lattice2(sK0),sK1) = a_2_0_filter_0(k1_lattice2(sK0),sK1),
inference(resolve,[status(thm)],[c_3787,c_1091]) ).
cnf(c_5288,plain,
( a_2_0_filter_0(k1_lattice2(sK0),sK1) = a_2_0_filter_2(sK0,sK1)
| v3_struct_0(k1_lattice2(sK0)) ),
inference(paramod,[status(thm)],[c_4110,c_1087]) ).
cnf(c_5289,plain,
( a_2_0_filter_2(sK0,sK1) = a_2_0_filter_0(k1_lattice2(sK0),sK1)
| v3_struct_0(k1_lattice2(sK0)) ),
inference(copy,[status(thm)],[c_5288]) ).
cnf(c_4112,plain,
a_2_0_filter_2(sK0,sK1) = a_2_0_filter_0(k1_lattice2(sK0),sK1),
inference(resolve,[status(thm)],[c_3787,c_5289]) ).
cnf(c_4258,negated_conjecture,
~ r1_tarski(a_2_0_filter_0(k1_lattice2(sK0),sK1),k3_filter_2(k1_lattice2(sK0),sK2)),
inference(paramod,[status(thm)],[c_4112,c_1555]) ).
cnf(c_5290,plain,
( r1_tarski(k2_filter_0(k1_lattice2(sK0),sK1),k3_filter_0(k1_lattice2(sK0),sK2))
| ~ m1_subset_1(sK1,u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_730,c_725]) ).
cnf(c_5291,plain,
( r1_tarski(a_2_0_filter_0(k1_lattice2(sK0),sK1),k3_filter_0(k1_lattice2(sK0),sK2))
| ~ m1_subset_1(sK1,u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(paramod,[status(thm)],[c_4110,c_5290]) ).
cnf(c_5292,plain,
( r1_tarski(a_2_0_filter_0(k1_lattice2(sK0),sK1),k3_filter_2(k1_lattice2(sK0),sK2))
| ~ m1_subset_1(sK1,u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(paramod,[status(thm)],[c_4096,c_5291]) ).
cnf(c_5293,plain,
( r1_tarski(a_2_0_filter_0(k1_lattice2(sK0),sK1),k3_filter_2(k1_lattice2(sK0),sK2))
| ~ m1_subset_1(sK1,u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_3787,c_5292]) ).
cnf(c_5294,plain,
( r1_tarski(a_2_0_filter_0(k1_lattice2(sK0),sK1),k3_filter_2(k1_lattice2(sK0),sK2))
| ~ m1_subset_1(sK1,u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_671,c_5293]) ).
cnf(c_5295,plain,
( r1_tarski(a_2_0_filter_0(k1_lattice2(sK0),sK1),k3_filter_2(k1_lattice2(sK0),sK2))
| ~ m1_subset_1(sK1,u1_struct_0(k1_lattice2(sK0))) ),
inference(resolve,[status(thm)],[c_687,c_5294]) ).
cnf(c_5296,plain,
r1_tarski(a_2_0_filter_0(k1_lattice2(sK0),sK1),k3_filter_2(k1_lattice2(sK0),sK2)),
inference(resolve,[status(thm)],[c_710,c_5295]) ).
cnf(c_5243,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_4258,c_5296]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT311+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n009.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 20:44:15 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 2492788 was started by sandbox2 on n009,
% 0.09/0.37 % Fri Sep 25 20:44:15 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.40
% 0.09/0.40 % From the command line: assign(max_seconds, 300).
% 108.57/14.45
% 108.57/14.45 % given #500 (T,wt=7): 1632 v1_funct_1(u1_lattices(k1_lattice2(k1_lattice2(k1_lattice2(k1_lattice2(c14)))))). [resolve(1166,a,267,a)].
% 108.57/14.45
% 108.57/14.45 % given #1000 (T,wt=8): 4000 k7_filter_2(k1_lattice2(c14),f2(c14)) = f2(c14). [back_unit_del(2061),unit_del(a,3787)].
% 108.57/14.45
% 108.57/14.45 % SZS status Theorem for theBenchmark
% 108.57/14.45
% 108.57/14.45 % Proof 1 at 13.60 (+ 0.16) seconds.
% 108.57/14.45 % Length of proof is 101.
% 108.57/14.45 % Level of proof is 10.
% 108.57/14.45 % Maximum clause weight is 35.000.
% 108.57/14.45 % Given clauses 1104.
% 108.57/14.45
% 108.57/14.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------