%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT312+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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:10 AM UTC 2026
% Result : Theorem 34.46s 5.52s
% Output : CNFRefutation 34.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 25
% Syntax : Number of formulae : 176 ( 38 unt; 0 def)
% Number of atoms : 639 ( 100 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 747 ( 284 ~; 335 |; 83 &)
% ( 1 <=>; 44 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 20 ( 18 usr; 1 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 3 con; 0-2 aty)
% Number of variables : 133 ( 1 sgn 52 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
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_k18_filter_2,axiom,
! [A,B] :
( ( m1_subset_1(B,u1_struct_0(A))
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m2_filter_2(k18_filter_2(A,B),A) ),
file('theBenchmark.p',dt_k18_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_k6_domain_1,axiom,
! [A,B] :
( ( m1_subset_1(B,A)
& ~ v1_xboole_0(A) )
=> m1_subset_1(k6_domain_1(A,B),k1_zfmisc_1(A)) ),
file('theBenchmark.p',dt_k6_domain_1) ).
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_l1_lattices,axiom,
! [A] :
( l1_lattices(A)
=> l1_struct_0(A) ),
file('theBenchmark.p',dt_l1_lattices) ).
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(fc1_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_struct_0(A) )
=> ( v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ),
file('theBenchmark.p',fc1_lattice2) ).
fof(fc1_struct_0,axiom,
! [A] :
( ( l1_struct_0(A)
& ~ v3_struct_0(A) )
=> ~ v1_xboole_0(u1_struct_0(A)) ),
file('theBenchmark.p',fc1_struct_0) ).
fof(fc6_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v10_lattices(k1_lattice2(A))
& v9_lattices(k1_lattice2(A))
& v8_lattices(k1_lattice2(A))
& v7_lattices(k1_lattice2(A))
& v6_lattices(k1_lattice2(A))
& v5_lattices(k1_lattice2(A))
& v4_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ),
file('theBenchmark.p',fc6_lattice2) ).
fof(redefinition_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_k6_domain_1,axiom,
! [A,B] :
( ( m1_subset_1(B,A)
& ~ v1_xboole_0(A) )
=> k6_domain_1(A,B) = k1_tarski(B) ),
file('theBenchmark.p',redefinition_k6_domain_1) ).
fof(redefinition_r1_filter_2,axiom,
! [A,B,C] :
( ( m1_subset_1(C,k1_zfmisc_1(A))
& m1_subset_1(B,k1_zfmisc_1(A))
& ~ v1_xboole_0(A) )
=> ( r1_filter_2(A,B,C)
<=> B = C ) ),
file('theBenchmark.p',redefinition_r1_filter_2) ).
fof(reflexivity_r1_filter_2,axiom,
! [A,B,C] :
( ( m1_subset_1(C,k1_zfmisc_1(A))
& m1_subset_1(B,k1_zfmisc_1(A))
& ~ v1_xboole_0(A) )
=> r1_filter_2(A,B,B) ),
file('theBenchmark.p',reflexivity_r1_filter_2) ).
fof(t30_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) )
=> ( C = k6_domain_1(u1_struct_0(A),B)
=> k3_filter_0(A,C) = k2_filter_0(A,B) ) ) ) ),
file('theBenchmark.p',t30_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(t41_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) )
=> ( r1_filter_2(u1_struct_0(A),C,k6_domain_1(u1_struct_0(A),B))
=> r1_filter_2(u1_struct_0(A),k19_filter_2(A,C),k18_filter_2(A,B)) ) ) ) ),
file('theBenchmark.p',t41_filter_2) ).
fof(t41_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) )
=> ( r1_filter_2(u1_struct_0(A),C,k6_domain_1(u1_struct_0(A),B))
=> r1_filter_2(u1_struct_0(A),k19_filter_2(A,C),k18_filter_2(A,B)) ) ) ) ),
inference(assume_negation,[status(cth)],[t41_filter_2]) ).
cnf(c_143,plain,
( m2_filter_2(k18_filter_2(A,B),A)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k18_filter_2]) ).
cnf(c_144,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_175,plain,
( l1_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_176,plain,
( l1_struct_0(A)
| ~ l1_lattices(A) ),
inference(clausify,[status(thm)],[dt_l1_lattices]) ).
cnf(c_177,plain,
( ~ v1_xboole_0(u1_struct_0(A))
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_struct_0]) ).
cnf(c_180,plain,
( ~ l3_lattices(A)
| l1_struct_0(A) ),
inference(resolve,[status(thm)],[c_176,c_175]) ).
cnf(c_185,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_189,plain,
( ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| m2_lattice4(k18_filter_2(A,B),A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_144,c_143]) ).
cnf(c_263,plain,
( ~ l3_lattices(A)
| ~ v1_xboole_0(u1_struct_0(A))
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_177,c_180]) ).
fof(nnf_111,plain,
? [A] :
( ? [B] :
( ? [C] :
( ~ r1_filter_2(u1_struct_0(A),k19_filter_2(A,C),k18_filter_2(A,B))
& r1_filter_2(u1_struct_0(A),C,k6_domain_1(u1_struct_0(A),B))
& 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)],[t41_filter_2_neg]) ).
fof(sk_t41_filter_2_neg,plain,
( ~ r1_filter_2(u1_struct_0(sK0),k19_filter_2(sK0,sK1),k18_filter_2(sK0,sK2))
& r1_filter_2(u1_struct_0(sK0),sK1,k6_domain_1(u1_struct_0(sK0),sK2))
& m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK0)))
& ~ v1_xboole_0(sK1)
& m1_subset_1(sK2,u1_struct_0(sK0))
& l3_lattices(sK0)
& v10_lattices(sK0)
& ~ v3_struct_0(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK2,sK1]),skolemize(A,sK0),skolemize(B,sK2),skolemize(C,sK1)],[nnf_111]) ).
cnf(c_300,negated_conjecture,
~ r1_filter_2(u1_struct_0(sK0),k19_filter_2(sK0,sK1),k18_filter_2(sK0,sK2)),
inference(split_conjunct,[status(thm)],[sk_t41_filter_2_neg]) ).
cnf(c_301,negated_conjecture,
r1_filter_2(u1_struct_0(sK0),sK1,k6_domain_1(u1_struct_0(sK0),sK2)),
inference(split_conjunct,[status(thm)],[sk_t41_filter_2_neg]) ).
cnf(c_302,negated_conjecture,
m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK0))),
inference(split_conjunct,[status(thm)],[sk_t41_filter_2_neg]) ).
cnf(c_303,negated_conjecture,
~ v1_xboole_0(sK1),
inference(split_conjunct,[status(thm)],[sk_t41_filter_2_neg]) ).
cnf(c_304,negated_conjecture,
m1_subset_1(sK2,u1_struct_0(sK0)),
inference(split_conjunct,[status(thm)],[sk_t41_filter_2_neg]) ).
cnf(c_305,negated_conjecture,
l3_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t41_filter_2_neg]) ).
cnf(c_306,negated_conjecture,
v10_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t41_filter_2_neg]) ).
cnf(c_307,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t41_filter_2_neg]) ).
cnf(c_318,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_321,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_322,plain,
( k3_filter_0(A,C) = k2_filter_0(A,B)
| k6_domain_1(u1_struct_0(A),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)],[t30_filter_0]) ).
cnf(c_328,plain,
( r1_filter_2(A,B,B)
| ~ m1_subset_1(C,k1_zfmisc_1(A))
| ~ m1_subset_1(B,k1_zfmisc_1(A))
| v1_xboole_0(A) ),
inference(clausify,[status(thm)],[reflexivity_r1_filter_2]) ).
cnf(c_330,plain,
( C = B
| ~ r1_filter_2(A,B,C)
| ~ m1_subset_1(C,k1_zfmisc_1(A))
| ~ m1_subset_1(B,k1_zfmisc_1(A))
| v1_xboole_0(A) ),
inference(clausify,[status(thm)],[redefinition_r1_filter_2]) ).
cnf(c_331,plain,
( k1_tarski(B) = k6_domain_1(A,B)
| ~ m1_subset_1(B,A)
| v1_xboole_0(A) ),
inference(clausify,[status(thm)],[redefinition_k6_domain_1]) ).
cnf(c_332,plain,
( k6_domain_1(A,B) = k1_tarski(B)
| ~ m1_subset_1(B,A)
| v1_xboole_0(A) ),
inference(copy,[status(thm)],[c_331]) ).
cnf(c_333,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_334,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_333]) ).
cnf(c_335,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_370,plain,
( v10_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc6_lattice2]) ).
cnf(c_384,plain,
( ~ v3_struct_0(k1_lattice2(A))
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_lattice2]) ).
cnf(c_390,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_391,plain,
( m1_subset_1(k6_domain_1(A,B),k1_zfmisc_1(A))
| ~ m1_subset_1(B,A)
| v1_xboole_0(A) ),
inference(clausify,[status(thm)],[dt_k6_domain_1]) ).
cnf(c_392,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_393,plain,
( l3_lattices(k1_lattice2(A))
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_k1_lattice2]) ).
cnf(c_395,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_396,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_395]) ).
cnf(c_398,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_399,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_400,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_401,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_400]) ).
cnf(c_433,plain,
( ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| m1_subset_1(k18_filter_2(A,B),k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_185,c_189]) ).
cnf(c_15935,plain,
( ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| m1_subset_1(k18_filter_2(A,B),k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_433]) ).
cnf(c_15936,plain,
( ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A)
| m1_subset_1(k18_filter_2(A,B),k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_15935]) ).
cnf(c_15937,plain,
( ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| m1_subset_1(k18_filter_2(A,B),k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_15936]) ).
cnf(c_15938,plain,
( ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| m1_subset_1(k18_filter_2(A,B),k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_15937]) ).
cnf(c_15939,plain,
( ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| m1_subset_1(k18_filter_2(A,B),k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_15938]) ).
cnf(c_434,plain,
( ~ m1_subset_1(B,u1_struct_0(A))
| m1_subset_1(k18_filter_2(A,B),k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_15939]) ).
cnf(c_461,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_318]) ).
cnf(c_462,plain,
( r1_filter_2(A,B,B)
| ~ m1_subset_1(B,k1_zfmisc_1(A))
| v1_xboole_0(A) ),
inference(factor,[status(thm)],[c_328]) ).
cnf(c_15940,negated_conjecture,
( ~ v1_xboole_0(u1_struct_0(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_305,c_263]) ).
cnf(c_527,negated_conjecture,
~ v1_xboole_0(u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_307,c_15940]) ).
cnf(c_15941,negated_conjecture,
( k2_filter_2(k1_lattice2(sK0),k5_filter_2(sK0,sK2)) = k18_filter_2(sK0,sK2)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_321,c_304]) ).
cnf(c_15942,negated_conjecture,
( k2_filter_2(k1_lattice2(sK0),k5_filter_2(sK0,sK2)) = k18_filter_2(sK0,sK2)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_307,c_15941]) ).
cnf(c_15943,negated_conjecture,
( k2_filter_2(k1_lattice2(sK0),k5_filter_2(sK0,sK2)) = k18_filter_2(sK0,sK2)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_306,c_15942]) ).
cnf(c_588,negated_conjecture,
k2_filter_2(k1_lattice2(sK0),k5_filter_2(sK0,sK2)) = k18_filter_2(sK0,sK2),
inference(resolve,[status(thm)],[c_305,c_15943]) ).
cnf(c_595,plain,
( k3_filter_0(A,k6_domain_1(u1_struct_0(A),B)) = k2_filter_0(A,B)
| ~ m1_subset_1(k6_domain_1(u1_struct_0(A),B),k1_zfmisc_1(u1_struct_0(A)))
| v1_xboole_0(k6_domain_1(u1_struct_0(A),B))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(xxres,[status(thm)],[c_322]) ).
cnf(c_15944,negated_conjecture,
( k6_domain_1(u1_struct_0(sK0),sK2) = sK1
| ~ m1_subset_1(k6_domain_1(u1_struct_0(sK0),sK2),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK0)))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_330,c_301]) ).
cnf(c_15945,negated_conjecture,
( k6_domain_1(u1_struct_0(sK0),sK2) = sK1
| ~ m1_subset_1(k6_domain_1(u1_struct_0(sK0),sK2),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_527,c_15944]) ).
cnf(c_656,negated_conjecture,
( k6_domain_1(u1_struct_0(sK0),sK2) = sK1
| ~ m1_subset_1(k6_domain_1(u1_struct_0(sK0),sK2),k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_302,c_15945]) ).
cnf(c_15946,negated_conjecture,
( k6_domain_1(u1_struct_0(sK0),sK2) = k1_tarski(sK2)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_332,c_304]) ).
cnf(c_657,negated_conjecture,
k6_domain_1(u1_struct_0(sK0),sK2) = k1_tarski(sK2),
inference(resolve,[status(thm)],[c_527,c_15946]) ).
cnf(c_15947,negated_conjecture,
( k6_domain_1(u1_struct_0(sK0),sK2) = sK1
| ~ m1_subset_1(k1_tarski(sK2),k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(paramod,[status(thm)],[c_657,c_656]) ).
cnf(c_664,negated_conjecture,
( k1_tarski(sK2) = sK1
| ~ m1_subset_1(k1_tarski(sK2),k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(paramod,[status(thm)],[c_657,c_15947]) ).
cnf(c_15948,negated_conjecture,
( v10_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_370,c_306]) ).
cnf(c_15949,negated_conjecture,
( v10_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_307,c_15948]) ).
cnf(c_907,negated_conjecture,
v10_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_305,c_15949]) ).
cnf(c_15950,negated_conjecture,
( ~ v3_struct_0(k1_lattice2(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_384,c_305]) ).
cnf(c_950,negated_conjecture,
~ v3_struct_0(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_307,c_15950]) ).
cnf(c_15951,negated_conjecture,
( m1_subset_1(k7_filter_2(sK0,sK1),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_390,c_302]) ).
cnf(c_15952,negated_conjecture,
( m1_subset_1(k7_filter_2(sK0,sK1),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_307,c_15951]) ).
cnf(c_15953,negated_conjecture,
( m1_subset_1(k7_filter_2(sK0,sK1),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_306,c_15952]) ).
cnf(c_1092,negated_conjecture,
m1_subset_1(k7_filter_2(sK0,sK1),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0)))),
inference(resolve,[status(thm)],[c_305,c_15953]) ).
cnf(c_15954,negated_conjecture,
( m1_subset_1(k6_domain_1(u1_struct_0(sK0),sK2),k1_zfmisc_1(u1_struct_0(sK0)))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_391,c_304]) ).
cnf(c_15955,negated_conjecture,
( m1_subset_1(k1_tarski(sK2),k1_zfmisc_1(u1_struct_0(sK0)))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(paramod,[status(thm)],[c_657,c_15954]) ).
cnf(c_1098,negated_conjecture,
m1_subset_1(k1_tarski(sK2),k1_zfmisc_1(u1_struct_0(sK0))),
inference(resolve,[status(thm)],[c_527,c_15955]) ).
cnf(c_1106,negated_conjecture,
k1_tarski(sK2) = sK1,
inference(resolve,[status(thm)],[c_1098,c_664]) ).
cnf(c_15956,negated_conjecture,
( m1_subset_1(k5_filter_2(sK0,sK2),u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_392,c_304]) ).
cnf(c_15957,negated_conjecture,
( m1_subset_1(k5_filter_2(sK0,sK2),u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_307,c_15956]) ).
cnf(c_15958,negated_conjecture,
( m1_subset_1(k5_filter_2(sK0,sK2),u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_306,c_15957]) ).
cnf(c_1116,negated_conjecture,
m1_subset_1(k5_filter_2(sK0,sK2),u1_struct_0(k1_lattice2(sK0))),
inference(resolve,[status(thm)],[c_305,c_15958]) ).
cnf(c_1121,plain,
l3_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_393,c_305]) ).
cnf(c_15959,negated_conjecture,
( k18_filter_2(sK0,sK2) = a_2_0_filter_2(sK0,sK2)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_396,c_304]) ).
cnf(c_15960,negated_conjecture,
( k18_filter_2(sK0,sK2) = a_2_0_filter_2(sK0,sK2)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_307,c_15959]) ).
cnf(c_15961,negated_conjecture,
( k18_filter_2(sK0,sK2) = a_2_0_filter_2(sK0,sK2)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_306,c_15960]) ).
cnf(c_1147,negated_conjecture,
k18_filter_2(sK0,sK2) = a_2_0_filter_2(sK0,sK2),
inference(resolve,[status(thm)],[c_305,c_15961]) ).
cnf(c_1148,negated_conjecture,
k2_filter_2(k1_lattice2(sK0),k5_filter_2(sK0,sK2)) = a_2_0_filter_2(sK0,sK2),
inference(paramod,[status(thm)],[c_1147,c_588]) ).
cnf(c_1150,negated_conjecture,
~ r1_filter_2(u1_struct_0(sK0),k19_filter_2(sK0,sK1),a_2_0_filter_2(sK0,sK2)),
inference(paramod,[status(thm)],[c_1147,c_300]) ).
cnf(c_15962,negated_conjecture,
( k7_filter_2(sK0,sK1) = sK1
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_398,c_302]) ).
cnf(c_15963,negated_conjecture,
( k7_filter_2(sK0,sK1) = sK1
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_307,c_15962]) ).
cnf(c_15964,negated_conjecture,
( k7_filter_2(sK0,sK1) = sK1
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_306,c_15963]) ).
cnf(c_1166,negated_conjecture,
k7_filter_2(sK0,sK1) = sK1,
inference(resolve,[status(thm)],[c_305,c_15964]) ).
cnf(c_1170,negated_conjecture,
m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0)))),
inference(paramod,[status(thm)],[c_1166,c_1092]) ).
cnf(c_15965,negated_conjecture,
( k5_filter_2(sK0,sK2) = sK2
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_399,c_304]) ).
cnf(c_15966,negated_conjecture,
( k5_filter_2(sK0,sK2) = sK2
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_307,c_15965]) ).
cnf(c_15967,negated_conjecture,
( k5_filter_2(sK0,sK2) = sK2
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_306,c_15966]) ).
cnf(c_1179,negated_conjecture,
k5_filter_2(sK0,sK2) = sK2,
inference(resolve,[status(thm)],[c_305,c_15967]) ).
cnf(c_1180,negated_conjecture,
k2_filter_2(k1_lattice2(sK0),sK2) = a_2_0_filter_2(sK0,sK2),
inference(paramod,[status(thm)],[c_1179,c_1148]) ).
cnf(c_1181,negated_conjecture,
m1_subset_1(sK2,u1_struct_0(k1_lattice2(sK0))),
inference(paramod,[status(thm)],[c_1179,c_1116]) ).
cnf(c_15968,negated_conjecture,
( m1_subset_1(k18_filter_2(sK0,sK2),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_434,c_304]) ).
cnf(c_15969,negated_conjecture,
( m1_subset_1(a_2_0_filter_2(sK0,sK2),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(paramod,[status(thm)],[c_1147,c_15968]) ).
cnf(c_15970,negated_conjecture,
( m1_subset_1(a_2_0_filter_2(sK0,sK2),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_307,c_15969]) ).
cnf(c_15971,negated_conjecture,
( m1_subset_1(a_2_0_filter_2(sK0,sK2),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_306,c_15970]) ).
cnf(c_1278,negated_conjecture,
m1_subset_1(a_2_0_filter_2(sK0,sK2),k1_zfmisc_1(u1_struct_0(sK0))),
inference(resolve,[status(thm)],[c_305,c_15971]) ).
cnf(c_15972,negated_conjecture,
( k3_filter_2(k1_lattice2(sK0),k7_filter_2(sK0,sK1)) = k19_filter_2(sK0,sK1)
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| v1_xboole_0(sK1)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_461,c_302]) ).
cnf(c_15973,negated_conjecture,
( k3_filter_2(k1_lattice2(sK0),sK1) = k19_filter_2(sK0,sK1)
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| v1_xboole_0(sK1)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(paramod,[status(thm)],[c_1166,c_15972]) ).
cnf(c_15974,negated_conjecture,
( k3_filter_2(k1_lattice2(sK0),sK1) = k19_filter_2(sK0,sK1)
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| v1_xboole_0(sK1)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_307,c_15973]) ).
cnf(c_15975,negated_conjecture,
( k3_filter_2(k1_lattice2(sK0),sK1) = k19_filter_2(sK0,sK1)
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| v1_xboole_0(sK1)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_306,c_15974]) ).
cnf(c_15976,negated_conjecture,
( k3_filter_2(k1_lattice2(sK0),sK1) = k19_filter_2(sK0,sK1)
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| v1_xboole_0(sK1) ),
inference(resolve,[status(thm)],[c_305,c_15975]) ).
cnf(c_15977,negated_conjecture,
( k3_filter_2(k1_lattice2(sK0),sK1) = k19_filter_2(sK0,sK1)
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0)))) ),
inference(resolve,[status(thm)],[c_303,c_15976]) ).
cnf(c_1397,negated_conjecture,
k3_filter_2(k1_lattice2(sK0),sK1) = k19_filter_2(sK0,sK1),
inference(resolve,[status(thm)],[c_1170,c_15977]) ).
cnf(c_15978,plain,
( ~ v1_xboole_0(u1_struct_0(k1_lattice2(sK0)))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_1121,c_263]) ).
cnf(c_1930,plain,
~ v1_xboole_0(u1_struct_0(k1_lattice2(sK0))),
inference(resolve,[status(thm)],[c_950,c_15978]) ).
cnf(c_15979,plain,
( k2_filter_0(k1_lattice2(sK0),sK2) = a_2_0_filter_0(k1_lattice2(sK0),sK2)
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_1181,c_401]) ).
cnf(c_15980,plain,
( k2_filter_0(k1_lattice2(sK0),sK2) = a_2_0_filter_0(k1_lattice2(sK0),sK2)
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_950,c_15979]) ).
cnf(c_15981,plain,
( k2_filter_0(k1_lattice2(sK0),sK2) = a_2_0_filter_0(k1_lattice2(sK0),sK2)
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_907,c_15980]) ).
cnf(c_2952,plain,
k2_filter_0(k1_lattice2(sK0),sK2) = a_2_0_filter_0(k1_lattice2(sK0),sK2),
inference(resolve,[status(thm)],[c_1121,c_15981]) ).
cnf(c_15982,plain,
( k2_filter_2(k1_lattice2(sK0),sK2) = k2_filter_0(k1_lattice2(sK0),sK2)
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_1181,c_335]) ).
cnf(c_15983,plain,
( a_2_0_filter_2(sK0,sK2) = k2_filter_0(k1_lattice2(sK0),sK2)
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(paramod,[status(thm)],[c_1180,c_15982]) ).
cnf(c_15984,plain,
( a_2_0_filter_2(sK0,sK2) = a_2_0_filter_0(k1_lattice2(sK0),sK2)
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(paramod,[status(thm)],[c_2952,c_15983]) ).
cnf(c_15985,plain,
( a_2_0_filter_0(k1_lattice2(sK0),sK2) = a_2_0_filter_2(sK0,sK2)
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(copy,[status(thm)],[c_15984]) ).
cnf(c_15986,plain,
( a_2_0_filter_0(k1_lattice2(sK0),sK2) = a_2_0_filter_2(sK0,sK2)
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_950,c_15985]) ).
cnf(c_15987,plain,
( a_2_0_filter_0(k1_lattice2(sK0),sK2) = a_2_0_filter_2(sK0,sK2)
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_907,c_15986]) ).
cnf(c_2961,plain,
a_2_0_filter_0(k1_lattice2(sK0),sK2) = a_2_0_filter_2(sK0,sK2),
inference(resolve,[status(thm)],[c_1121,c_15987]) ).
cnf(c_15988,plain,
( k6_domain_1(u1_struct_0(k1_lattice2(sK0)),sK2) = k1_tarski(sK2)
| v1_xboole_0(u1_struct_0(k1_lattice2(sK0))) ),
inference(resolve,[status(thm)],[c_1181,c_332]) ).
cnf(c_15989,plain,
( k6_domain_1(u1_struct_0(k1_lattice2(sK0)),sK2) = sK1
| v1_xboole_0(u1_struct_0(k1_lattice2(sK0))) ),
inference(paramod,[status(thm)],[c_1106,c_15988]) ).
cnf(c_2962,plain,
k6_domain_1(u1_struct_0(k1_lattice2(sK0)),sK2) = sK1,
inference(resolve,[status(thm)],[c_1930,c_15989]) ).
cnf(c_2976,plain,
k2_filter_0(k1_lattice2(sK0),sK2) = a_2_0_filter_2(sK0,sK2),
inference(paramod,[status(thm)],[c_2961,c_2952]) ).
cnf(c_15990,plain,
( r1_filter_2(u1_struct_0(sK0),a_2_0_filter_2(sK0,sK2),a_2_0_filter_2(sK0,sK2))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_1278,c_462]) ).
cnf(c_4993,plain,
r1_filter_2(u1_struct_0(sK0),a_2_0_filter_2(sK0,sK2),a_2_0_filter_2(sK0,sK2)),
inference(resolve,[status(thm)],[c_527,c_15990]) ).
cnf(c_15991,plain,
( k3_filter_0(k1_lattice2(sK0),k6_domain_1(u1_struct_0(k1_lattice2(sK0)),sK2)) = k2_filter_0(k1_lattice2(sK0),sK2)
| ~ m1_subset_1(k6_domain_1(u1_struct_0(k1_lattice2(sK0)),sK2),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| v1_xboole_0(k6_domain_1(u1_struct_0(k1_lattice2(sK0)),sK2))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_595,c_1181]) ).
cnf(c_15992,plain,
( k3_filter_0(k1_lattice2(sK0),k6_domain_1(u1_struct_0(k1_lattice2(sK0)),sK2)) = k2_filter_0(k1_lattice2(sK0),sK2)
| ~ m1_subset_1(k6_domain_1(u1_struct_0(k1_lattice2(sK0)),sK2),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| v1_xboole_0(sK1)
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(paramod,[status(thm)],[c_2962,c_15991]) ).
cnf(c_15993,plain,
( k3_filter_0(k1_lattice2(sK0),k6_domain_1(u1_struct_0(k1_lattice2(sK0)),sK2)) = k2_filter_0(k1_lattice2(sK0),sK2)
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| v1_xboole_0(sK1)
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(paramod,[status(thm)],[c_2962,c_15992]) ).
cnf(c_15994,plain,
( k3_filter_0(k1_lattice2(sK0),sK1) = k2_filter_0(k1_lattice2(sK0),sK2)
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| v1_xboole_0(sK1)
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(paramod,[status(thm)],[c_2962,c_15993]) ).
cnf(c_15995,plain,
( k3_filter_0(k1_lattice2(sK0),sK1) = a_2_0_filter_2(sK0,sK2)
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| v1_xboole_0(sK1)
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(paramod,[status(thm)],[c_2976,c_15994]) ).
cnf(c_15996,plain,
( k3_filter_0(k1_lattice2(sK0),sK1) = a_2_0_filter_2(sK0,sK2)
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| v1_xboole_0(sK1)
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_950,c_15995]) ).
cnf(c_15997,plain,
( k3_filter_0(k1_lattice2(sK0),sK1) = a_2_0_filter_2(sK0,sK2)
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| v1_xboole_0(sK1)
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_907,c_15996]) ).
cnf(c_15998,plain,
( k3_filter_0(k1_lattice2(sK0),sK1) = a_2_0_filter_2(sK0,sK2)
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| v1_xboole_0(sK1) ),
inference(resolve,[status(thm)],[c_1121,c_15997]) ).
cnf(c_15999,negated_conjecture,
( k3_filter_0(k1_lattice2(sK0),sK1) = a_2_0_filter_2(sK0,sK2)
| ~ m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0)))) ),
inference(resolve,[status(thm)],[c_303,c_15998]) ).
cnf(c_6173,negated_conjecture,
k3_filter_0(k1_lattice2(sK0),sK1) = a_2_0_filter_2(sK0,sK2),
inference(resolve,[status(thm)],[c_1170,c_15999]) ).
cnf(c_16000,plain,
( k3_filter_0(k1_lattice2(sK0),sK1) = k3_filter_2(k1_lattice2(sK0),sK1)
| v1_xboole_0(sK1)
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_1170,c_334]) ).
cnf(c_16001,plain,
( a_2_0_filter_2(sK0,sK2) = k3_filter_2(k1_lattice2(sK0),sK1)
| v1_xboole_0(sK1)
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(paramod,[status(thm)],[c_6173,c_16000]) ).
cnf(c_16002,plain,
( a_2_0_filter_2(sK0,sK2) = k19_filter_2(sK0,sK1)
| v1_xboole_0(sK1)
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(paramod,[status(thm)],[c_1397,c_16001]) ).
cnf(c_16003,plain,
( k19_filter_2(sK0,sK1) = a_2_0_filter_2(sK0,sK2)
| v1_xboole_0(sK1)
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(copy,[status(thm)],[c_16002]) ).
cnf(c_16004,plain,
( k19_filter_2(sK0,sK1) = a_2_0_filter_2(sK0,sK2)
| v1_xboole_0(sK1)
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_950,c_16003]) ).
cnf(c_16005,plain,
( k19_filter_2(sK0,sK1) = a_2_0_filter_2(sK0,sK2)
| v1_xboole_0(sK1)
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_907,c_16004]) ).
cnf(c_16006,plain,
( k19_filter_2(sK0,sK1) = a_2_0_filter_2(sK0,sK2)
| v1_xboole_0(sK1) ),
inference(resolve,[status(thm)],[c_1121,c_16005]) ).
cnf(c_15918,negated_conjecture,
k19_filter_2(sK0,sK1) = a_2_0_filter_2(sK0,sK2),
inference(resolve,[status(thm)],[c_303,c_16006]) ).
cnf(c_16007,negated_conjecture,
~ r1_filter_2(u1_struct_0(sK0),a_2_0_filter_2(sK0,sK2),a_2_0_filter_2(sK0,sK2)),
inference(paramod,[status(thm)],[c_15918,c_1150]) ).
cnf(c_15934,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_4993,c_16007]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT312+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.38 % Computer : n005.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Fri Sep 25 20:44:19 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.38 % Process 171058 was started by sandbox on n005,
% 0.09/0.38 % Fri Sep 25 20:44:19 2026
% 0.09/0.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.41
% 0.09/0.41 % From the command line: assign(max_seconds, 300).
% 34.46/5.52
% 34.46/5.52 % given #500 (A,wt=26): 518 m1_subset_1(k2_filter_0(c16,A),k1_zfmisc_1(u1_struct_0(c16))) | -m1_subset_1(A,u1_struct_0(c16)). [resolve(305,a,282,c),unit_del(a,307),unit_del(b,306)].
% 34.46/5.52
% 34.46/5.52 % given #1000 (F,wt=44): 4270 -v1_xboole_0(k2_filter_2(k1_lattice2(k1_lattice2(c15)),f4(u1_struct_0(k1_lattice2(k1_lattice2(c15)))))). [resolve(3701,a,386,a)].
% 34.46/5.52
% 34.46/5.52 % given #1500 (T,wt=22): 7823 -r1_filter_2(k1_zfmisc_1(A),k1_tarski(k1_xboole_0),k1_zfmisc_1(A)) | k1_tarski(k1_xboole_0) = k1_zfmisc_1(A). [resolve(2150,a,655,b),flip(c),unit_del(a,383)].
% 34.46/5.52
% 34.46/5.52 % given #2000 (T,wt=24): 7175 -r1_filter_2(u1_struct_0(c16),f1(c16),u1_struct_0(c16)) | r1_filter_2(u1_struct_0(c16),u1_struct_0(c16),f1(c16)). [resolve(630,b,519,a),unit_del(a,527)].
% 34.46/5.52
% 34.46/5.52 % given #2500 (W,wt=25): 9243 r1_filter_2(a_2_0_filter_2(c16,c17),k1_tarski(f4(c18)),k1_tarski(f4(c18))). [resolve(4304,a,462,b),unit_del(a,1149)].
% 34.46/5.52
% 34.46/5.52 % SZS status Theorem for theBenchmark
% 34.46/5.52
% 34.46/5.52 % Proof 1 at 4.08 (+ 0.69) seconds.
% 34.46/5.52 % Length of proof is 100.
% 34.46/5.52 % Level of proof is 11.
% 34.46/5.52 % Maximum clause weight is 53.000.
% 34.46/5.52 % Given clauses 2608.
% 34.46/5.52
% 34.46/5.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------