%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT306+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 : n012.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:08 AM UTC 2026
% Result : Theorem 90.18s 11.83s
% Output : CNFRefutation 90.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 29
% Syntax : Number of formulae : 175 ( 44 unt; 0 def)
% Number of atoms : 547 ( 77 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 604 ( 232 ~; 262 |; 70 &)
% ( 4 <=>; 36 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 24 ( 22 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 1 con; 0-2 aty)
% Number of variables : 135 ( 1 sgn 56 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
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(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(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(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_k5_lattices,axiom,
! [A] :
( ( l1_lattices(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k5_lattices(A),u1_struct_0(A)) ),
file('theBenchmark.p',dt_k5_lattices) ).
fof(dt_k6_lattices,axiom,
! [A] :
( ( l2_lattices(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k6_lattices(A),u1_struct_0(A)) ),
file('theBenchmark.p',dt_k6_lattices) ).
fof(dt_l2_lattices,axiom,
! [A] :
( l2_lattices(A)
=> l1_struct_0(A) ),
file('theBenchmark.p',dt_l2_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_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_tarski,axiom,
! [A,B] : r1_tarski(A,A),
file('theBenchmark.p',reflexivity_r1_tarski) ).
fof(t1_subset,axiom,
! [A,B] :
( r2_hidden(A,B)
=> m1_subset_1(A,B) ),
file('theBenchmark.p',t1_subset) ).
fof(t20_filter_0,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( ( l3_lattices(A)
& v13_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k1_filter_0(A) = k2_filter_0(A,k5_lattices(A)) ) ),
file('theBenchmark.p',t20_filter_0) ).
fof(t2_subset,axiom,
! [A,B] :
( m1_subset_1(A,B)
=> ( r2_hidden(A,B)
| v1_xboole_0(B) ) ),
file('theBenchmark.p',t2_subset) ).
fof(t2_tarski,axiom,
! [A,B] :
( ! [C] :
( r2_hidden(C,A)
<=> r2_hidden(C,B) )
=> A = B ),
file('theBenchmark.p',t2_tarski) ).
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(t3_subset,axiom,
! [A,B] :
( m1_subset_1(A,k1_zfmisc_1(B))
<=> r1_tarski(A,B) ),
file('theBenchmark.p',t3_subset) ).
fof(t4_subset,axiom,
! [A,B,C] :
( ( m1_subset_1(B,k1_zfmisc_1(C))
& r2_hidden(A,B) )
=> m1_subset_1(A,C) ),
file('theBenchmark.p',t4_subset) ).
fof(t64_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v14_lattices(A)
<=> v13_lattices(k1_lattice2(A)) ) ),
file('theBenchmark.p',t64_lattice2) ).
fof(t79_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& v14_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k6_lattices(A) = k5_lattices(k1_lattice2(A)) ),
file('theBenchmark.p',t79_lattice2) ).
fof(t32_filter_2,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v14_lattices(A)
=> r1_filter_2(u1_struct_0(A),k17_filter_2(A),k18_filter_2(A,k6_lattices(A))) ) ),
file('theBenchmark.p',t32_filter_2) ).
fof(t32_filter_2_neg,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v14_lattices(A)
=> r1_filter_2(u1_struct_0(A),k17_filter_2(A),k18_filter_2(A,k6_lattices(A))) ) ),
inference(assume_negation,[status(cth)],[t32_filter_2]) ).
cnf(c_109,plain,
( v13_lattices(k1_lattice2(A))
| ~ v14_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t64_lattice2]) ).
cnf(c_111,plain,
( k5_lattices(k1_lattice2(A)) = k6_lattices(A)
| ~ l3_lattices(A)
| ~ v14_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t79_lattice2]) ).
fof(nnf_105,plain,
? [A] :
( ~ r1_filter_2(u1_struct_0(A),k17_filter_2(A),k18_filter_2(A,k6_lattices(A)))
& v14_lattices(A)
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t32_filter_2_neg]) ).
fof(sk_t32_filter_2_neg,plain,
( ~ r1_filter_2(u1_struct_0(sK0),k17_filter_2(sK0),k18_filter_2(sK0,k6_lattices(sK0)))
& v14_lattices(sK0)
& l3_lattices(sK0)
& v10_lattices(sK0)
& ~ v3_struct_0(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(A,sK0)],[nnf_105]) ).
cnf(c_112,negated_conjecture,
v14_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t32_filter_2_neg]) ).
cnf(c_190,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_193,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_212,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_214,plain,
( l1_struct_0(A)
| ~ l2_lattices(A) ),
inference(clausify,[status(thm)],[dt_l2_lattices]) ).
cnf(c_219,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_223,plain,
( m2_lattice4(k18_filter_2(A,B),A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_193,c_190]) ).
cnf(c_241,plain,
( 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)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_223,c_219]) ).
cnf(c_20261,plain,
( 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)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_241]) ).
cnf(c_20262,plain,
( 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)
| ~ l3_lattices(A)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_20261]) ).
cnf(c_20263,plain,
( 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)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_20262]) ).
cnf(c_20264,plain,
( m1_subset_1(k18_filter_2(A,B),k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_20263]) ).
cnf(c_20265,plain,
( m1_subset_1(k18_filter_2(A,B),k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_20264]) ).
cnf(c_242,plain,
( m1_subset_1(k18_filter_2(A,B),k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_20265]) ).
cnf(c_310,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_314,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_315,plain,
( k17_filter_2(A) = u1_struct_0(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d8_filter_2]) ).
cnf(c_316,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_317,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_316]) ).
cnf(c_319,plain,
( l3_lattices(k1_lattice2(A))
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_k1_lattice2]) ).
cnf(c_320,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_321,plain,
( m1_subset_1(k5_lattices(A),u1_struct_0(A))
| ~ l1_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k5_lattices]) ).
cnf(c_322,plain,
( m1_subset_1(k6_lattices(A),u1_struct_0(A))
| ~ l2_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k6_lattices]) ).
cnf(c_323,plain,
( l1_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_324,plain,
( l2_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_338,plain,
( ~ v3_struct_0(k1_lattice2(A))
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_lattice2]) ).
cnf(c_345,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,
( 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_388,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_390,plain,
r1_tarski(A,A),
inference(clausify,[status(thm)],[reflexivity_r1_tarski]) ).
cnf(c_392,plain,
( m1_subset_1(A,B)
| ~ r2_hidden(A,B) ),
inference(clausify,[status(thm)],[t1_subset]) ).
cnf(c_393,plain,
( k2_filter_0(A,k5_lattices(A)) = k1_filter_0(A)
| ~ v13_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t20_filter_0]) ).
cnf(c_394,plain,
( k1_filter_0(A) = k2_filter_0(A,k5_lattices(A))
| ~ v13_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_393]) ).
cnf(c_395,plain,
( r2_hidden(A,B)
| v1_xboole_0(B)
| ~ m1_subset_1(A,B) ),
inference(clausify,[status(thm)],[t2_subset]) ).
fof(nnf_95,plain,
! [A,B] :
( B = A
| ? [C] :
( ( ~ r2_hidden(C,B)
| ~ r2_hidden(C,A) )
& ( r2_hidden(C,B)
| r2_hidden(C,A) ) ) ),
inference(fof_nnf,[status(thm)],[t2_tarski]) ).
fof(sk_t2_tarski_sk,plain,
! [A,B] :
( B = A
| ( ( ~ r2_hidden(sK1(A,B),B)
| ~ r2_hidden(sK1(A,B),A) )
& ( r2_hidden(sK1(A,B),B)
| r2_hidden(sK1(A,B),A) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(C,sK1(A,B))],[nnf_95]) ).
fof(sk_t2_tarski,plain,
( ! [VAR_0,VAR_1] :
( VAR_1 = VAR_0
| ~ r2_hidden(sK1(VAR_0,VAR_1),VAR_1)
| ~ r2_hidden(sK1(VAR_0,VAR_1),VAR_0) )
& ! [VAR_0,VAR_1] :
( VAR_1 = VAR_0
| r2_hidden(sK1(VAR_0,VAR_1),VAR_1)
| r2_hidden(sK1(VAR_0,VAR_1),VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_t2_tarski_sk]) ).
cnf(c_396,plain,
( B = A
| r2_hidden(sK1(A,B),B)
| r2_hidden(sK1(A,B),A) ),
inference(split_conjunct,[status(thm)],[sk_t2_tarski]) ).
cnf(c_397,plain,
( B = A
| ~ r2_hidden(sK1(A,B),B)
| ~ r2_hidden(sK1(A,B),A) ),
inference(split_conjunct,[status(thm)],[sk_t2_tarski]) ).
cnf(c_398,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_402,plain,
( ~ r1_tarski(A,B)
| m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[t3_subset]) ).
cnf(c_403,plain,
( m1_subset_1(A,C)
| ~ m1_subset_1(B,k1_zfmisc_1(C))
| ~ r2_hidden(A,B) ),
inference(clausify,[status(thm)],[t4_subset]) ).
cnf(c_408,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t32_filter_2_neg]) ).
cnf(c_409,negated_conjecture,
v10_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t32_filter_2_neg]) ).
cnf(c_410,negated_conjecture,
l3_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t32_filter_2_neg]) ).
cnf(c_411,negated_conjecture,
~ r1_filter_2(u1_struct_0(sK0),k17_filter_2(sK0),k18_filter_2(sK0,k6_lattices(sK0))),
inference(split_conjunct,[status(thm)],[sk_t32_filter_2_neg]) ).
cnf(c_418,negated_conjecture,
( k5_lattices(k1_lattice2(sK0)) = k6_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_112,c_111]) ).
cnf(c_20266,negated_conjecture,
( k6_lattices(sK0) = k5_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_418]) ).
cnf(c_20267,negated_conjecture,
( k6_lattices(sK0) = k5_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_408,c_20266]) ).
cnf(c_20268,negated_conjecture,
( k6_lattices(sK0) = k5_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_409,c_20267]) ).
cnf(c_419,negated_conjecture,
k6_lattices(sK0) = k5_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_410,c_20268]) ).
cnf(c_420,negated_conjecture,
( v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_112,c_109]) ).
cnf(c_20269,negated_conjecture,
( v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_408,c_420]) ).
cnf(c_20270,negated_conjecture,
( v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_409,c_20269]) ).
cnf(c_421,negated_conjecture,
v13_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_410,c_20270]) ).
cnf(c_492,plain,
( ~ l2_lattices(A)
| ~ v1_xboole_0(u1_struct_0(A))
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_212,c_214]) ).
cnf(c_525,negated_conjecture,
~ r1_filter_2(u1_struct_0(sK0),k17_filter_2(sK0),k18_filter_2(sK0,k5_lattices(k1_lattice2(sK0)))),
inference(paramod,[status(thm)],[c_419,c_411]) ).
cnf(c_658,plain,
( m1_subset_1(sK1(A,B),A)
| B = A
| r2_hidden(sK1(A,B),B) ),
inference(resolve,[status(thm)],[c_396,c_392]) ).
cnf(c_679,plain,
m1_subset_1(A,k1_zfmisc_1(A)),
inference(resolve,[status(thm)],[c_402,c_390]) ).
cnf(c_20271,negated_conjecture,
( v10_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_409,c_345]) ).
cnf(c_20272,negated_conjecture,
( v10_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_408,c_20271]) ).
cnf(c_695,negated_conjecture,
v10_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_410,c_20272]) ).
cnf(c_20273,negated_conjecture,
( k17_filter_2(sK0) = u1_struct_0(sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_409,c_315]) ).
cnf(c_20274,negated_conjecture,
( k17_filter_2(sK0) = u1_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_408,c_20273]) ).
cnf(c_698,negated_conjecture,
k17_filter_2(sK0) = u1_struct_0(sK0),
inference(resolve,[status(thm)],[c_410,c_20274]) ).
cnf(c_707,negated_conjecture,
~ r1_filter_2(u1_struct_0(sK0),u1_struct_0(sK0),k18_filter_2(sK0,k5_lattices(k1_lattice2(sK0)))),
inference(paramod,[status(thm)],[c_698,c_525]) ).
cnf(c_20275,negated_conjecture,
( ~ v3_struct_0(k1_lattice2(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_410,c_338]) ).
cnf(c_709,negated_conjecture,
~ v3_struct_0(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_408,c_20275]) ).
cnf(c_710,plain,
l2_lattices(sK0),
inference(resolve,[status(thm)],[c_410,c_324]) ).
cnf(c_712,plain,
l3_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_410,c_319]) ).
cnf(c_20276,negated_conjecture,
( k1_filter_0(k1_lattice2(sK0)) = k2_filter_0(k1_lattice2(sK0),k5_lattices(k1_lattice2(sK0)))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_421,c_394]) ).
cnf(c_20277,negated_conjecture,
( k1_filter_0(k1_lattice2(sK0)) = k2_filter_0(k1_lattice2(sK0),k5_lattices(k1_lattice2(sK0)))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_709,c_20276]) ).
cnf(c_20278,negated_conjecture,
( k1_filter_0(k1_lattice2(sK0)) = k2_filter_0(k1_lattice2(sK0),k5_lattices(k1_lattice2(sK0)))
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_695,c_20277]) ).
cnf(c_715,negated_conjecture,
k1_filter_0(k1_lattice2(sK0)) = k2_filter_0(k1_lattice2(sK0),k5_lattices(k1_lattice2(sK0))),
inference(resolve,[status(thm)],[c_712,c_20278]) ).
cnf(c_20279,plain,
( ~ v1_xboole_0(u1_struct_0(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_710,c_492]) ).
cnf(c_832,negated_conjecture,
~ v1_xboole_0(u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_408,c_20279]) ).
cnf(c_20280,plain,
( m1_subset_1(k6_lattices(sK0),u1_struct_0(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_710,c_322]) ).
cnf(c_20281,plain,
( m1_subset_1(k5_lattices(k1_lattice2(sK0)),u1_struct_0(sK0))
| v3_struct_0(sK0) ),
inference(paramod,[status(thm)],[c_419,c_20280]) ).
cnf(c_837,negated_conjecture,
m1_subset_1(k5_lattices(k1_lattice2(sK0)),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_408,c_20281]) ).
cnf(c_20282,plain,
( k1_filter_0(k1_lattice2(sK0)) = u1_struct_0(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_695,c_310]) ).
cnf(c_20283,plain,
( k2_filter_0(k1_lattice2(sK0),k5_lattices(k1_lattice2(sK0))) = u1_struct_0(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(paramod,[status(thm)],[c_715,c_20282]) ).
cnf(c_20284,plain,
( k2_filter_0(k1_lattice2(sK0),k5_lattices(k1_lattice2(sK0))) = u1_struct_0(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_709,c_20283]) ).
cnf(c_909,plain,
k2_filter_0(k1_lattice2(sK0),k5_lattices(k1_lattice2(sK0))) = u1_struct_0(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_712,c_20284]) ).
cnf(c_933,plain,
l2_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_712,c_324]) ).
cnf(c_934,plain,
l1_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_712,c_323]) ).
cnf(c_20285,plain,
( ~ v1_xboole_0(u1_struct_0(k1_lattice2(sK0)))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_933,c_492]) ).
cnf(c_1043,plain,
~ v1_xboole_0(u1_struct_0(k1_lattice2(sK0))),
inference(resolve,[status(thm)],[c_709,c_20285]) ).
cnf(c_20286,plain,
( m1_subset_1(k5_lattices(k1_lattice2(sK0)),u1_struct_0(k1_lattice2(sK0)))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_934,c_321]) ).
cnf(c_1055,plain,
m1_subset_1(k5_lattices(k1_lattice2(sK0)),u1_struct_0(k1_lattice2(sK0))),
inference(resolve,[status(thm)],[c_709,c_20286]) ).
cnf(c_1061,plain,
( B != A
| r1_filter_2(A,A,B)
| ~ m1_subset_1(B,k1_zfmisc_1(A))
| v1_xboole_0(A) ),
inference(resolve,[status(thm)],[c_679,c_388]) ).
cnf(c_20287,plain,
( k2_filter_2(k1_lattice2(sK0),k5_filter_2(sK0,k5_lattices(k1_lattice2(sK0)))) = k18_filter_2(sK0,k5_lattices(k1_lattice2(sK0)))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_837,c_398]) ).
cnf(c_20288,negated_conjecture,
( k2_filter_2(k1_lattice2(sK0),k5_filter_2(sK0,k5_lattices(k1_lattice2(sK0)))) = k18_filter_2(sK0,k5_lattices(k1_lattice2(sK0)))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_408,c_20287]) ).
cnf(c_20289,negated_conjecture,
( k2_filter_2(k1_lattice2(sK0),k5_filter_2(sK0,k5_lattices(k1_lattice2(sK0)))) = k18_filter_2(sK0,k5_lattices(k1_lattice2(sK0)))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_409,c_20288]) ).
cnf(c_1901,negated_conjecture,
k2_filter_2(k1_lattice2(sK0),k5_filter_2(sK0,k5_lattices(k1_lattice2(sK0)))) = k18_filter_2(sK0,k5_lattices(k1_lattice2(sK0))),
inference(resolve,[status(thm)],[c_410,c_20289]) ).
cnf(c_20290,plain,
( k18_filter_2(sK0,k5_lattices(k1_lattice2(sK0))) = a_2_0_filter_2(sK0,k5_lattices(k1_lattice2(sK0)))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_837,c_317]) ).
cnf(c_20291,negated_conjecture,
( k18_filter_2(sK0,k5_lattices(k1_lattice2(sK0))) = a_2_0_filter_2(sK0,k5_lattices(k1_lattice2(sK0)))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_408,c_20290]) ).
cnf(c_20292,negated_conjecture,
( k18_filter_2(sK0,k5_lattices(k1_lattice2(sK0))) = a_2_0_filter_2(sK0,k5_lattices(k1_lattice2(sK0)))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_409,c_20291]) ).
cnf(c_1905,negated_conjecture,
k18_filter_2(sK0,k5_lattices(k1_lattice2(sK0))) = a_2_0_filter_2(sK0,k5_lattices(k1_lattice2(sK0))),
inference(resolve,[status(thm)],[c_410,c_20292]) ).
cnf(c_20293,plain,
( k5_filter_2(sK0,k5_lattices(k1_lattice2(sK0))) = k5_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_837,c_314]) ).
cnf(c_20294,negated_conjecture,
( k5_filter_2(sK0,k5_lattices(k1_lattice2(sK0))) = k5_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_408,c_20293]) ).
cnf(c_20295,negated_conjecture,
( k5_filter_2(sK0,k5_lattices(k1_lattice2(sK0))) = k5_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_409,c_20294]) ).
cnf(c_1906,negated_conjecture,
k5_filter_2(sK0,k5_lattices(k1_lattice2(sK0))) = k5_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_410,c_20295]) ).
cnf(c_20296,plain,
( m1_subset_1(k18_filter_2(sK0,k5_lattices(k1_lattice2(sK0))),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_837,c_242]) ).
cnf(c_20297,plain,
( m1_subset_1(a_2_0_filter_2(sK0,k5_lattices(k1_lattice2(sK0))),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(paramod,[status(thm)],[c_1905,c_20296]) ).
cnf(c_20298,negated_conjecture,
( m1_subset_1(a_2_0_filter_2(sK0,k5_lattices(k1_lattice2(sK0))),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_408,c_20297]) ).
cnf(c_20299,negated_conjecture,
( m1_subset_1(a_2_0_filter_2(sK0,k5_lattices(k1_lattice2(sK0))),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_409,c_20298]) ).
cnf(c_1911,negated_conjecture,
m1_subset_1(a_2_0_filter_2(sK0,k5_lattices(k1_lattice2(sK0))),k1_zfmisc_1(u1_struct_0(sK0))),
inference(resolve,[status(thm)],[c_410,c_20299]) ).
cnf(c_20300,negated_conjecture,
k2_filter_2(k1_lattice2(sK0),k5_lattices(k1_lattice2(sK0))) = k18_filter_2(sK0,k5_lattices(k1_lattice2(sK0))),
inference(paramod,[status(thm)],[c_1906,c_1901]) ).
cnf(c_1913,negated_conjecture,
k2_filter_2(k1_lattice2(sK0),k5_lattices(k1_lattice2(sK0))) = a_2_0_filter_2(sK0,k5_lattices(k1_lattice2(sK0))),
inference(paramod,[status(thm)],[c_1905,c_20300]) ).
cnf(c_1914,negated_conjecture,
~ r1_filter_2(u1_struct_0(sK0),u1_struct_0(sK0),a_2_0_filter_2(sK0,k5_lattices(k1_lattice2(sK0)))),
inference(paramod,[status(thm)],[c_1905,c_707]) ).
cnf(c_2063,plain,
( m1_subset_1(sK1(B,A),C)
| ~ m1_subset_1(A,k1_zfmisc_1(C))
| m1_subset_1(sK1(B,A),B)
| A = B ),
inference(resolve,[status(thm)],[c_658,c_403]) ).
cnf(c_2072,plain,
( ~ m1_subset_1(A,k1_zfmisc_1(B))
| m1_subset_1(sK1(B,A),B)
| A = B ),
inference(factor,[status(thm)],[c_2063]) ).
cnf(c_20301,plain,
( k2_filter_2(k1_lattice2(sK0),k5_lattices(k1_lattice2(sK0))) = k2_filter_0(k1_lattice2(sK0),k5_lattices(k1_lattice2(sK0)))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_1055,c_384]) ).
cnf(c_20302,plain,
( a_2_0_filter_2(sK0,k5_lattices(k1_lattice2(sK0))) = k2_filter_0(k1_lattice2(sK0),k5_lattices(k1_lattice2(sK0)))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(paramod,[status(thm)],[c_1913,c_20301]) ).
cnf(c_20303,plain,
( a_2_0_filter_2(sK0,k5_lattices(k1_lattice2(sK0))) = 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_909,c_20302]) ).
cnf(c_20304,plain,
( a_2_0_filter_2(sK0,k5_lattices(k1_lattice2(sK0))) = u1_struct_0(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_709,c_20303]) ).
cnf(c_20305,plain,
( a_2_0_filter_2(sK0,k5_lattices(k1_lattice2(sK0))) = u1_struct_0(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_695,c_20304]) ).
cnf(c_2997,plain,
a_2_0_filter_2(sK0,k5_lattices(k1_lattice2(sK0))) = u1_struct_0(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_712,c_20305]) ).
cnf(c_3010,negated_conjecture,
~ r1_filter_2(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(k1_lattice2(sK0))),
inference(paramod,[status(thm)],[c_2997,c_1914]) ).
cnf(c_3012,negated_conjecture,
m1_subset_1(u1_struct_0(k1_lattice2(sK0)),k1_zfmisc_1(u1_struct_0(sK0))),
inference(paramod,[status(thm)],[c_2997,c_1911]) ).
cnf(c_20306,plain,
( u1_struct_0(k1_lattice2(sK0)) != u1_struct_0(sK0)
| r1_filter_2(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(k1_lattice2(sK0)))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_1061,c_3012]) ).
cnf(c_20307,plain,
( u1_struct_0(k1_lattice2(sK0)) != u1_struct_0(sK0)
| r1_filter_2(u1_struct_0(sK0),u1_struct_0(sK0),u1_struct_0(k1_lattice2(sK0))) ),
inference(resolve,[status(thm)],[c_832,c_20306]) ).
cnf(c_8706,negated_conjecture,
u1_struct_0(k1_lattice2(sK0)) != u1_struct_0(sK0),
inference(resolve,[status(thm)],[c_3010,c_20307]) ).
cnf(c_20308,plain,
( m1_subset_1(sK1(u1_struct_0(sK0),u1_struct_0(k1_lattice2(sK0))),u1_struct_0(sK0))
| u1_struct_0(k1_lattice2(sK0)) = u1_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_2072,c_3012]) ).
cnf(c_20095,plain,
m1_subset_1(sK1(u1_struct_0(sK0),u1_struct_0(k1_lattice2(sK0))),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_8706,c_20308]) ).
cnf(c_20309,plain,
( r2_hidden(sK1(u1_struct_0(sK0),u1_struct_0(k1_lattice2(sK0))),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_20095,c_395]) ).
cnf(c_20235,plain,
r2_hidden(sK1(u1_struct_0(sK0),u1_struct_0(k1_lattice2(sK0))),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_832,c_20309]) ).
cnf(c_20310,plain,
( m1_subset_1(k5_filter_2(sK0,sK1(u1_struct_0(sK0),u1_struct_0(k1_lattice2(sK0)))),u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_20095,c_320]) ).
cnf(c_20311,negated_conjecture,
( m1_subset_1(k5_filter_2(sK0,sK1(u1_struct_0(sK0),u1_struct_0(k1_lattice2(sK0)))),u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_408,c_20310]) ).
cnf(c_20312,negated_conjecture,
( m1_subset_1(k5_filter_2(sK0,sK1(u1_struct_0(sK0),u1_struct_0(k1_lattice2(sK0)))),u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_409,c_20311]) ).
cnf(c_20237,negated_conjecture,
m1_subset_1(k5_filter_2(sK0,sK1(u1_struct_0(sK0),u1_struct_0(k1_lattice2(sK0)))),u1_struct_0(k1_lattice2(sK0))),
inference(resolve,[status(thm)],[c_410,c_20312]) ).
cnf(c_20313,plain,
( k5_filter_2(sK0,sK1(u1_struct_0(sK0),u1_struct_0(k1_lattice2(sK0)))) = sK1(u1_struct_0(sK0),u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_20095,c_314]) ).
cnf(c_20314,negated_conjecture,
( k5_filter_2(sK0,sK1(u1_struct_0(sK0),u1_struct_0(k1_lattice2(sK0)))) = sK1(u1_struct_0(sK0),u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_408,c_20313]) ).
cnf(c_20315,negated_conjecture,
( k5_filter_2(sK0,sK1(u1_struct_0(sK0),u1_struct_0(k1_lattice2(sK0)))) = sK1(u1_struct_0(sK0),u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_409,c_20314]) ).
cnf(c_20239,negated_conjecture,
k5_filter_2(sK0,sK1(u1_struct_0(sK0),u1_struct_0(k1_lattice2(sK0)))) = sK1(u1_struct_0(sK0),u1_struct_0(k1_lattice2(sK0))),
inference(resolve,[status(thm)],[c_410,c_20315]) ).
cnf(c_20247,negated_conjecture,
m1_subset_1(sK1(u1_struct_0(sK0),u1_struct_0(k1_lattice2(sK0))),u1_struct_0(k1_lattice2(sK0))),
inference(paramod,[status(thm)],[c_20239,c_20237]) ).
cnf(c_20316,plain,
( u1_struct_0(k1_lattice2(sK0)) = u1_struct_0(sK0)
| ~ r2_hidden(sK1(u1_struct_0(sK0),u1_struct_0(k1_lattice2(sK0))),u1_struct_0(k1_lattice2(sK0))) ),
inference(resolve,[status(thm)],[c_20235,c_397]) ).
cnf(c_20257,plain,
~ r2_hidden(sK1(u1_struct_0(sK0),u1_struct_0(k1_lattice2(sK0))),u1_struct_0(k1_lattice2(sK0))),
inference(resolve,[status(thm)],[c_8706,c_20316]) ).
cnf(c_20317,plain,
( r2_hidden(sK1(u1_struct_0(sK0),u1_struct_0(k1_lattice2(sK0))),u1_struct_0(k1_lattice2(sK0)))
| v1_xboole_0(u1_struct_0(k1_lattice2(sK0))) ),
inference(resolve,[status(thm)],[c_20247,c_395]) ).
cnf(c_20318,plain,
r2_hidden(sK1(u1_struct_0(sK0),u1_struct_0(k1_lattice2(sK0))),u1_struct_0(k1_lattice2(sK0))),
inference(resolve,[status(thm)],[c_1043,c_20317]) ).
cnf(c_20260,plain,
$false,
inference(resolve,[status(thm)],[c_20257,c_20318]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LAT306+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.02 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Fri Sep 25 20:40:05 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.03/0.30 % Process 2952789 was started by sandbox2 on n012,
% 0.03/0.30 % Fri Sep 25 20:40:05 2026
% 0.03/0.30 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.03/0.32
% 0.03/0.32 % From the command line: assign(max_seconds, 300).
% 90.18/11.83
% 90.18/11.83 % given #500 (T,wt=5): 1687 r1_tarski(f6(c14),u1_struct_0(c14)). [resolve(637,a,401,a)].
% 90.18/11.83
% 90.18/11.83 % given #1000 (T,wt=7): 4044 r1_tarski(k2_filter_0(c15,k5_lattices(c15)),u1_struct_0(c15)). [resolve(1424,a,401,a)].
% 90.18/11.83
% 90.18/11.83 % given #1500 (T,wt=9): 5346 r2_hidden(k5_lattices(k1_lattice2(k1_lattice2(c13))),u1_struct_0(k1_lattice2(k1_lattice2(c13)))). [resolve(1266,a,395,a),unit_del(a,1250)].
% 90.18/11.83
% 90.18/11.83 % given #2000 (T,wt=9): 9003 v1_xboole_0(f6(c5)) | -v1_xboole_0(k2_filter_2(c5,f4(f6(c5)))). [resolve(7155,b,256,d),unit_del(b,358),unit_del(c,361),unit_del(d,357)].
% 90.18/11.83
% 90.18/11.83 % given #2500 (T,wt=8): 11036 l2_lattices(g3_lattices(u1_struct_0(c15),u1_lattices(c15),u1_lattices(c15))). [resolve(11023,a,324,a)].
% 90.18/11.83
% 90.18/11.83 % given #3000 (T,wt=10): 12164 r2_hidden(k2_filter_0(c14,f4(f13(c14))),k1_zfmisc_1(u1_struct_0(k1_lattice2(c14)))). [resolve(7509,a,395,a),unit_del(a,339)].
% 90.18/11.83
% 90.18/11.83 % given #3500 (A,wt=22): 1642 v1_funct_2(u2_lattices(k1_lattice2(k1_lattice2(k1_lattice2(c14)))),k2_zfmisc_1(u1_struct_0(k1_lattice2(k1_lattice2(k1_lattice2(c14)))),u1_struct_0(k1_lattice2(k1_lattice2(k1_lattice2(c14))))),u1_struct_0(k1_lattice2(k1_lattice2(k1_lattice2(c14))))). [resolve(1474,a,330,a)].
% 90.18/11.83
% 90.18/11.83 % given #4000 (T,wt=11): 15467 r1_lattices(k1_lattice2(c14),f4(f13(k1_lattice2(c14))),f4(f13(k1_lattice2(c14)))). [resolve(7737,a,529,f),unit_del(a,620),unit_del(b,633),unit_del(c,632),unit_del(d,623),unit_del(e,7111),unit_del(g,631)].
% 90.18/11.83
% 90.18/11.83 % SZS status Theorem for theBenchmark
% 90.18/11.83
% 90.18/11.83 % Proof 1 at 10.81 (+ 0.46) seconds.
% 90.18/11.83 % Length of proof is 111.
% 90.18/11.83 % Level of proof is 13.
% 90.18/11.83 % Maximum clause weight is 20.000.
% 90.18/11.83 % Given clauses 4332.
% 90.18/11.83
% 90.18/11.83 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------