%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT324+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 : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:50:13 AM UTC 2026
% Result : Theorem 178.49s 29.61s
% Output : CNFRefutation 178.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 24
% Syntax : Number of formulae : 215 ( 44 unt; 0 def)
% Number of atoms : 879 ( 119 equ)
% Maximal formula atoms : 34 ( 4 avg)
% Number of connectives : 1098 ( 434 ~; 494 |; 126 &)
% ( 3 <=>; 41 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 34 ( 32 usr; 1 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 3 con; 0-3 aty)
% Number of variables : 237 ( 22 sgn 74 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(abstractness_v3_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( v3_lattices(A)
=> A = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) ) ),
file('theBenchmark.p',abstractness_v3_lattices) ).
fof(d2_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(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(d7_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(k1_lattice2(A))))
=> k8_filter_2(A,B) = B ) ),
file('theBenchmark.p',d7_filter_2) ).
fof(dt_k14_filter_2,axiom,
! [A,B] :
( ( m1_filter_0(B,k1_lattice2(A))
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m2_filter_2(k14_filter_2(A,B),A) ),
file('theBenchmark.p',dt_k14_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_l3_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( l2_lattices(A)
& l1_lattices(A) ) ),
file('theBenchmark.p',dt_l3_lattices) ).
fof(dt_m1_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_filter_2(B,A)
=> ( m2_lattice4(B,A)
& ~ v1_xboole_0(B) ) ) ),
file('theBenchmark.p',dt_m1_filter_2) ).
fof(dt_m2_lattice4,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_lattice4(B,A)
=> m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ),
file('theBenchmark.p',dt_m2_lattice4) ).
fof(dt_u1_lattices,axiom,
! [A] :
( l1_lattices(A)
=> ( m2_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_1(u1_lattices(A)) ) ),
file('theBenchmark.p',dt_u1_lattices) ).
fof(dt_u2_lattices,axiom,
! [A] :
( l2_lattices(A)
=> ( m2_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_1(u2_lattices(A)) ) ),
file('theBenchmark.p',dt_u2_lattices) ).
fof(fc1_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_struct_0(A) )
=> ( v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ),
file('theBenchmark.p',fc1_lattice2) ).
fof(fc4_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v17_lattices(k1_lattice2(A))
& v16_lattices(k1_lattice2(A))
& v15_lattices(k1_lattice2(A))
& v14_lattices(k1_lattice2(A))
& v13_lattices(k1_lattice2(A))
& v12_lattices(k1_lattice2(A))
& v11_lattices(k1_lattice2(A))
& v10_lattices(k1_lattice2(A))
& v9_lattices(k1_lattice2(A))
& v8_lattices(k1_lattice2(A))
& v7_lattices(k1_lattice2(A))
& v6_lattices(k1_lattice2(A))
& v5_lattices(k1_lattice2(A))
& v4_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ),
file('theBenchmark.p',fc4_filter_2) ).
fof(fc6_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v10_lattices(k1_lattice2(A))
& v9_lattices(k1_lattice2(A))
& v8_lattices(k1_lattice2(A))
& v7_lattices(k1_lattice2(A))
& v6_lattices(k1_lattice2(A))
& v5_lattices(k1_lattice2(A))
& v4_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ),
file('theBenchmark.p',fc6_lattice2) ).
fof(free_g3_lattices,axiom,
! [A,B,C] :
( ( m1_relset_1(C,k2_zfmisc_1(A,A),A)
& v1_funct_2(C,k2_zfmisc_1(A,A),A)
& v1_funct_1(C)
& m1_relset_1(B,k2_zfmisc_1(A,A),A)
& v1_funct_2(B,k2_zfmisc_1(A,A),A)
& v1_funct_1(B) )
=> ! [D,E,F] :
( g3_lattices(A,B,C) = g3_lattices(D,E,F)
=> ( C = F
& B = E
& A = D ) ) ),
file('theBenchmark.p',free_g3_lattices) ).
fof(redefinition_k14_filter_2,axiom,
! [A,B] :
( ( m1_filter_0(B,k1_lattice2(A))
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k14_filter_2(A,B) = k8_filter_2(A,B) ),
file('theBenchmark.p',redefinition_k14_filter_2) ).
fof(redefinition_k15_filter_2,axiom,
! [A,B] :
( ( m2_filter_2(B,A)
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k15_filter_2(A,B) = k7_filter_2(A,B) ),
file('theBenchmark.p',redefinition_k15_filter_2) ).
fof(redefinition_m1_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_filter_2(B,A)
<=> m1_filter_0(B,A) ) ),
file('theBenchmark.p',redefinition_m1_filter_2) ).
fof(redefinition_m2_relset_1,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('theBenchmark.p',redefinition_m2_relset_1) ).
fof(t33_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( r2_filter_2(A,B)
<=> v1_filter_0(k15_filter_2(A,B),k1_lattice2(A)) ) ) ),
file('theBenchmark.p',t33_filter_2) ).
fof(t60_filter_0,axiom,
! [A] :
( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ~ ( ! [D] :
( m1_filter_0(D,A)
=> ~ ( ( ( r2_hidden(C,D)
& ~ r2_hidden(B,D) )
| ( ~ r2_hidden(C,D)
& r2_hidden(B,D) ) )
& v1_filter_0(D,A) ) )
& B != C ) ) ) ),
file('theBenchmark.p',t60_filter_0) ).
fof(t60_filter_2,conjecture,
! [A] :
( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ~ ( ! [D] :
( m2_filter_2(D,A)
=> ~ ( ( ( r2_hidden(C,D)
& ~ r2_hidden(B,D) )
| ( ~ r2_hidden(C,D)
& r2_hidden(B,D) ) )
& r2_filter_2(A,D) ) )
& B != C ) ) ) ),
file('theBenchmark.p',t60_filter_2) ).
fof(t60_filter_2_neg,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ~ ( ! [D] :
( m2_filter_2(D,A)
=> ~ ( ( ( r2_hidden(C,D)
& ~ r2_hidden(B,D) )
| ( ~ r2_hidden(C,D)
& r2_hidden(B,D) ) )
& r2_filter_2(A,D) ) )
& B != C ) ) ) ),
inference(assume_negation,[status(cth)],[t60_filter_2]) ).
cnf(c_100,plain,
( g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) = A
| ~ v3_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[abstractness_v3_lattices]) ).
cnf(c_101,plain,
( v3_lattices(k1_lattice2(A))
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_k1_lattice2]) ).
cnf(c_162,plain,
( ~ m1_filter_0(B,A)
| m1_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[redefinition_m1_filter_2]) ).
cnf(c_164,plain,
( m2_lattice4(B,A)
| ~ m1_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_m1_filter_2]) ).
cnf(c_167,plain,
( l1_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_169,plain,
( v1_funct_1(u1_lattices(A))
| ~ l1_lattices(A) ),
inference(clausify,[status(thm)],[dt_u1_lattices]) ).
cnf(c_170,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_171,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_189,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_192,plain,
( ~ m1_filter_0(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| m2_lattice4(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_164,c_162]) ).
cnf(c_196,plain,
( m1_relset_1(A,B,C)
| ~ m2_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_m2_relset_1]) ).
cnf(c_198,plain,
( ~ l3_lattices(A)
| m2_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_171,c_167]) ).
cnf(c_201,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_203,plain,
( l2_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_211,plain,
( m1_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
| ~ l2_lattices(A) ),
inference(resolve,[status(thm)],[c_201,c_196]) ).
cnf(c_213,plain,
( v1_funct_1(u2_lattices(A))
| ~ l2_lattices(A) ),
inference(clausify,[status(thm)],[dt_u2_lattices]) ).
cnf(c_214,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_230,plain,
( ~ l3_lattices(A)
| v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ),
inference(resolve,[status(thm)],[c_214,c_203]) ).
cnf(c_231,plain,
( ~ l3_lattices(A)
| v1_funct_1(u2_lattices(A)) ),
inference(resolve,[status(thm)],[c_213,c_203]) ).
cnf(c_233,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_203,c_211]) ).
cnf(c_247,plain,
( ~ m1_filter_0(B,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,k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_189,c_192]) ).
cnf(c_20478,plain,
( ~ m1_filter_0(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_247]) ).
cnf(c_20479,plain,
( ~ m1_filter_0(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A)
| m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_20478]) ).
cnf(c_20480,plain,
( ~ m1_filter_0(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_20479]) ).
cnf(c_20481,plain,
( ~ m1_filter_0(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_20480]) ).
cnf(c_20482,plain,
( ~ m1_filter_0(B,A)
| ~ l3_lattices(A)
| m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_20481]) ).
cnf(c_248,plain,
( ~ m1_filter_0(B,A)
| m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_20482]) ).
cnf(c_255,plain,
( ~ l3_lattices(A)
| v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ),
inference(resolve,[status(thm)],[c_170,c_167]) ).
cnf(c_256,plain,
( ~ l3_lattices(A)
| v1_funct_1(u1_lattices(A)) ),
inference(resolve,[status(thm)],[c_169,c_167]) ).
cnf(c_264,plain,
( g3_lattices(u1_struct_0(k1_lattice2(A)),u2_lattices(k1_lattice2(A)),u1_lattices(k1_lattice2(A))) = k1_lattice2(A)
| ~ l3_lattices(k1_lattice2(A))
| ~ l3_lattices(A) ),
inference(resolve,[status(thm)],[c_101,c_100]) ).
fof(nnf_98,plain,
? [A] :
( ? [B] :
( ? [C] :
( ! [D] :
( ( ( ~ r2_hidden(C,D)
| r2_hidden(B,D) )
& ( r2_hidden(C,D)
| ~ r2_hidden(B,D) ) )
| ~ r2_filter_2(A,D)
| ~ m2_filter_2(D,A) )
& C != B
& m1_subset_1(C,u1_struct_0(A)) )
& m1_subset_1(B,u1_struct_0(A)) )
& l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t60_filter_2_neg]) ).
fof(sk_t60_filter_2_neg_sk,plain,
( ! [D] :
( ( ( ~ r2_hidden(sK2,D)
| r2_hidden(sK1,D) )
& ( r2_hidden(sK2,D)
| ~ r2_hidden(sK1,D) ) )
| ~ r2_filter_2(sK0,D)
| ~ m2_filter_2(D,sK0) )
& sK2 != sK1
& m1_subset_1(sK2,u1_struct_0(sK0))
& m1_subset_1(sK1,u1_struct_0(sK0))
& l3_lattices(sK0)
& v17_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_98]) ).
fof(sk_t60_filter_2_neg,plain,
( ! [VAR_0] :
( ~ r2_hidden(sK2,VAR_0)
| r2_hidden(sK1,VAR_0)
| ~ r2_filter_2(sK0,VAR_0)
| ~ m2_filter_2(VAR_0,sK0) )
& ! [VAR_0] :
( r2_hidden(sK2,VAR_0)
| ~ r2_hidden(sK1,VAR_0)
| ~ r2_filter_2(sK0,VAR_0)
| ~ m2_filter_2(VAR_0,sK0) )
& sK2 != sK1
& m1_subset_1(sK2,u1_struct_0(sK0))
& m1_subset_1(sK1,u1_struct_0(sK0))
& l3_lattices(sK0)
& v17_lattices(sK0)
& v10_lattices(sK0)
& ~ v3_struct_0(sK0) ),
inference(cnf_transformation,[status(thm)],[sk_t60_filter_2_neg_sk]) ).
cnf(c_266,negated_conjecture,
( ~ r2_hidden(sK2,A)
| r2_hidden(sK1,A)
| ~ r2_filter_2(sK0,A)
| ~ m2_filter_2(A,sK0) ),
inference(split_conjunct,[status(thm)],[sk_t60_filter_2_neg]) ).
cnf(c_267,negated_conjecture,
( r2_hidden(sK2,A)
| ~ r2_hidden(sK1,A)
| ~ r2_filter_2(sK0,A)
| ~ m2_filter_2(A,sK0) ),
inference(split_conjunct,[status(thm)],[sk_t60_filter_2_neg]) ).
cnf(c_268,negated_conjecture,
sK2 != sK1,
inference(split_conjunct,[status(thm)],[sk_t60_filter_2_neg]) ).
cnf(c_269,negated_conjecture,
m1_subset_1(sK2,u1_struct_0(sK0)),
inference(split_conjunct,[status(thm)],[sk_t60_filter_2_neg]) ).
cnf(c_270,negated_conjecture,
m1_subset_1(sK1,u1_struct_0(sK0)),
inference(split_conjunct,[status(thm)],[sk_t60_filter_2_neg]) ).
cnf(c_271,negated_conjecture,
l3_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t60_filter_2_neg]) ).
cnf(c_272,negated_conjecture,
v17_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t60_filter_2_neg]) ).
cnf(c_273,negated_conjecture,
v10_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t60_filter_2_neg]) ).
cnf(c_274,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t60_filter_2_neg]) ).
fof(nnf_94,plain,
! [A] :
( ! [B] :
( ! [C] :
( ? [D] :
( ( ( r2_hidden(C,D)
& ~ r2_hidden(B,D) )
| ( ~ r2_hidden(C,D)
& r2_hidden(B,D) ) )
& v1_filter_0(D,A)
& m1_filter_0(D,A) )
| C = B
| ~ m1_subset_1(C,u1_struct_0(A)) )
| ~ m1_subset_1(B,u1_struct_0(A)) )
| ~ l3_lattices(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t60_filter_0]) ).
fof(sk_t60_filter_0_sk,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ( r2_hidden(C,sK3(A,B,C))
& ~ r2_hidden(B,sK3(A,B,C)) )
| ( ~ r2_hidden(C,sK3(A,B,C))
& r2_hidden(B,sK3(A,B,C)) ) )
& v1_filter_0(sK3(A,B,C),A)
& m1_filter_0(sK3(A,B,C),A) )
| C = B
| ~ m1_subset_1(C,u1_struct_0(A)) )
| ~ m1_subset_1(B,u1_struct_0(A)) )
| ~ l3_lattices(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(D,sK3(A,B,C))],[nnf_94]) ).
fof(sk_t60_filter_0,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( ~ r2_hidden(VAR_1,sK3(VAR_0,VAR_1,VAR_2))
| ~ r2_hidden(VAR_2,sK3(VAR_0,VAR_1,VAR_2))
| VAR_2 = VAR_1
| ~ m1_subset_1(VAR_2,u1_struct_0(VAR_0))
| ~ m1_subset_1(VAR_1,u1_struct_0(VAR_0))
| ~ l3_lattices(VAR_0)
| ~ v17_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( r2_hidden(VAR_2,sK3(VAR_0,VAR_1,VAR_2))
| r2_hidden(VAR_1,sK3(VAR_0,VAR_1,VAR_2))
| VAR_2 = VAR_1
| ~ m1_subset_1(VAR_2,u1_struct_0(VAR_0))
| ~ m1_subset_1(VAR_1,u1_struct_0(VAR_0))
| ~ l3_lattices(VAR_0)
| ~ v17_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( v1_filter_0(sK3(VAR_0,VAR_1,VAR_2),VAR_0)
| VAR_2 = VAR_1
| ~ m1_subset_1(VAR_2,u1_struct_0(VAR_0))
| ~ m1_subset_1(VAR_1,u1_struct_0(VAR_0))
| ~ l3_lattices(VAR_0)
| ~ v17_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( m1_filter_0(sK3(VAR_0,VAR_1,VAR_2),VAR_0)
| VAR_2 = VAR_1
| ~ m1_subset_1(VAR_2,u1_struct_0(VAR_0))
| ~ m1_subset_1(VAR_1,u1_struct_0(VAR_0))
| ~ l3_lattices(VAR_0)
| ~ v17_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_t60_filter_0_sk]) ).
cnf(c_278,plain,
( ~ r2_hidden(B,sK3(A,B,C))
| ~ r2_hidden(C,sK3(A,B,C))
| C = B
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(split_conjunct,[status(thm)],[sk_t60_filter_0]) ).
cnf(c_279,plain,
( r2_hidden(C,sK3(A,B,C))
| r2_hidden(B,sK3(A,B,C))
| C = B
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(split_conjunct,[status(thm)],[sk_t60_filter_0]) ).
cnf(c_280,plain,
( v1_filter_0(sK3(A,B,C),A)
| C = B
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(split_conjunct,[status(thm)],[sk_t60_filter_0]) ).
cnf(c_281,plain,
( m1_filter_0(sK3(A,B,C),A)
| C = B
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(split_conjunct,[status(thm)],[sk_t60_filter_0]) ).
cnf(c_284,plain,
( ~ v1_filter_0(k15_filter_2(A,B),k1_lattice2(A))
| r2_filter_2(A,B)
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t33_filter_2]) ).
cnf(c_288,plain,
( k15_filter_2(A,B) = k7_filter_2(A,B)
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[redefinition_k15_filter_2]) ).
cnf(c_289,plain,
( k7_filter_2(A,B) = k15_filter_2(A,B)
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_288]) ).
cnf(c_290,plain,
( k14_filter_2(A,B) = k8_filter_2(A,B)
| ~ m1_filter_0(B,k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[redefinition_k14_filter_2]) ).
cnf(c_357,plain,
( D = B
| g3_lattices(D,E,F) != g3_lattices(B,A,C)
| ~ m1_relset_1(C,k2_zfmisc_1(B,B),B)
| ~ v1_funct_2(C,k2_zfmisc_1(B,B),B)
| ~ v1_funct_1(C)
| ~ m1_relset_1(A,k2_zfmisc_1(B,B),B)
| ~ v1_funct_2(A,k2_zfmisc_1(B,B),B)
| ~ v1_funct_1(A) ),
inference(clausify,[status(thm)],[free_g3_lattices]) ).
cnf(c_358,plain,
( v10_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc6_lattice2]) ).
cnf(c_366,plain,
( v17_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc4_filter_2]) ).
cnf(c_374,plain,
( ~ v3_struct_0(k1_lattice2(A))
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_lattice2]) ).
cnf(c_385,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_386,plain,
( l3_lattices(k1_lattice2(A))
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_k1_lattice2]) ).
cnf(c_387,plain,
( m2_filter_2(k14_filter_2(A,B),A)
| ~ m1_filter_0(B,k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k14_filter_2]) ).
cnf(c_389,plain,
( k8_filter_2(A,B) = B
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k1_lattice2(A))))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d7_filter_2]) ).
cnf(c_390,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_391,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_392,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_393,plain,
( g3_lattices(u1_struct_0(A),u1_lattices(A),u2_lattices(A)) = k1_lattice2(A)
| ~ l3_lattices(A) ),
inference(copy,[status(thm)],[c_392]) ).
cnf(c_443,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_196,c_198]) ).
cnf(c_475,plain,
( g3_lattices(u1_struct_0(k1_lattice2(sK0)),u2_lattices(k1_lattice2(sK0)),u1_lattices(k1_lattice2(sK0))) = k1_lattice2(sK0)
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_271,c_264]) ).
cnf(c_476,plain,
v1_funct_1(u1_lattices(sK0)),
inference(resolve,[status(thm)],[c_271,c_256]) ).
cnf(c_477,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_271,c_255]) ).
cnf(c_487,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_271,c_233]) ).
cnf(c_489,plain,
v1_funct_1(u2_lattices(sK0)),
inference(resolve,[status(thm)],[c_271,c_231]) ).
cnf(c_490,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_271,c_230]) ).
cnf(c_20483,negated_conjecture,
( ~ v1_filter_0(k15_filter_2(sK0,A),k1_lattice2(sK0))
| r2_filter_2(sK0,A)
| ~ m2_filter_2(A,sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_284,c_273]) ).
cnf(c_20484,negated_conjecture,
( ~ v1_filter_0(k15_filter_2(sK0,A),k1_lattice2(sK0))
| r2_filter_2(sK0,A)
| ~ m2_filter_2(A,sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_274,c_20483]) ).
cnf(c_520,negated_conjecture,
( ~ v1_filter_0(k15_filter_2(sK0,A),k1_lattice2(sK0))
| r2_filter_2(sK0,A)
| ~ m2_filter_2(A,sK0) ),
inference(resolve,[status(thm)],[c_271,c_20484]) ).
cnf(c_20485,negated_conjecture,
( k7_filter_2(sK0,A) = k15_filter_2(sK0,A)
| ~ m2_filter_2(A,sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_289,c_273]) ).
cnf(c_20486,negated_conjecture,
( k7_filter_2(sK0,A) = k15_filter_2(sK0,A)
| ~ m2_filter_2(A,sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_274,c_20485]) ).
cnf(c_527,negated_conjecture,
( k7_filter_2(sK0,A) = k15_filter_2(sK0,A)
| ~ m2_filter_2(A,sK0) ),
inference(resolve,[status(thm)],[c_271,c_20486]) ).
cnf(c_20487,negated_conjecture,
( k14_filter_2(sK0,A) = k8_filter_2(sK0,A)
| ~ m1_filter_0(A,k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_290,c_273]) ).
cnf(c_20488,negated_conjecture,
( k14_filter_2(sK0,A) = k8_filter_2(sK0,A)
| ~ m1_filter_0(A,k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_274,c_20487]) ).
cnf(c_528,negated_conjecture,
( k14_filter_2(sK0,A) = k8_filter_2(sK0,A)
| ~ m1_filter_0(A,k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_271,c_20488]) ).
cnf(c_20489,negated_conjecture,
( v10_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_358,c_273]) ).
cnf(c_20490,negated_conjecture,
( v10_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_274,c_20489]) ).
cnf(c_782,negated_conjecture,
v10_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_271,c_20490]) ).
cnf(c_20491,negated_conjecture,
( v17_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v17_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_366,c_273]) ).
cnf(c_20492,negated_conjecture,
( v17_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v17_lattices(sK0) ),
inference(resolve,[status(thm)],[c_274,c_20491]) ).
cnf(c_20493,negated_conjecture,
( v17_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_272,c_20492]) ).
cnf(c_836,negated_conjecture,
v17_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_271,c_20493]) ).
cnf(c_20494,negated_conjecture,
( ~ v3_struct_0(k1_lattice2(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_374,c_271]) ).
cnf(c_896,negated_conjecture,
~ v3_struct_0(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_274,c_20494]) ).
cnf(c_20495,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_385,c_270]) ).
cnf(c_20496,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_274,c_20495]) ).
cnf(c_20497,negated_conjecture,
( m1_subset_1(k5_filter_2(sK0,sK1),u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_273,c_20496]) ).
cnf(c_1099,negated_conjecture,
m1_subset_1(k5_filter_2(sK0,sK1),u1_struct_0(k1_lattice2(sK0))),
inference(resolve,[status(thm)],[c_271,c_20497]) ).
cnf(c_20498,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_385,c_269]) ).
cnf(c_20499,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_274,c_20498]) ).
cnf(c_20500,negated_conjecture,
( m1_subset_1(k5_filter_2(sK0,sK2),u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_273,c_20499]) ).
cnf(c_1100,negated_conjecture,
m1_subset_1(k5_filter_2(sK0,sK2),u1_struct_0(k1_lattice2(sK0))),
inference(resolve,[status(thm)],[c_271,c_20500]) ).
cnf(c_1115,plain,
l3_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_386,c_271]) ).
cnf(c_1133,plain,
g3_lattices(u1_struct_0(k1_lattice2(sK0)),u2_lattices(k1_lattice2(sK0)),u1_lattices(k1_lattice2(sK0))) = k1_lattice2(sK0),
inference(resolve,[status(thm)],[c_1115,c_475]) ).
cnf(c_20501,negated_conjecture,
( k8_filter_2(sK0,A) = A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_389,c_273]) ).
cnf(c_20502,negated_conjecture,
( k8_filter_2(sK0,A) = A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_274,c_20501]) ).
cnf(c_1168,negated_conjecture,
( k8_filter_2(sK0,A) = A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0)))) ),
inference(resolve,[status(thm)],[c_271,c_20502]) ).
cnf(c_20503,negated_conjecture,
( k7_filter_2(sK0,A) = A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_390,c_273]) ).
cnf(c_20504,negated_conjecture,
( k7_filter_2(sK0,A) = A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_274,c_20503]) ).
cnf(c_1210,negated_conjecture,
( k7_filter_2(sK0,A) = A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_271,c_20504]) ).
cnf(c_20505,negated_conjecture,
( k5_filter_2(sK0,sK1) = sK1
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_391,c_270]) ).
cnf(c_20506,negated_conjecture,
( k5_filter_2(sK0,sK1) = sK1
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_274,c_20505]) ).
cnf(c_20507,negated_conjecture,
( k5_filter_2(sK0,sK1) = sK1
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_273,c_20506]) ).
cnf(c_1264,negated_conjecture,
k5_filter_2(sK0,sK1) = sK1,
inference(resolve,[status(thm)],[c_271,c_20507]) ).
cnf(c_20508,negated_conjecture,
( k5_filter_2(sK0,sK2) = sK2
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_391,c_269]) ).
cnf(c_20509,negated_conjecture,
( k5_filter_2(sK0,sK2) = sK2
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_274,c_20508]) ).
cnf(c_20510,negated_conjecture,
( k5_filter_2(sK0,sK2) = sK2
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_273,c_20509]) ).
cnf(c_1265,negated_conjecture,
k5_filter_2(sK0,sK2) = sK2,
inference(resolve,[status(thm)],[c_271,c_20510]) ).
cnf(c_1272,negated_conjecture,
m1_subset_1(sK1,u1_struct_0(k1_lattice2(sK0))),
inference(paramod,[status(thm)],[c_1264,c_1099]) ).
cnf(c_1273,negated_conjecture,
m1_subset_1(sK2,u1_struct_0(k1_lattice2(sK0))),
inference(paramod,[status(thm)],[c_1265,c_1100]) ).
cnf(c_1288,plain,
g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0)) = k1_lattice2(sK0),
inference(resolve,[status(thm)],[c_393,c_271]) ).
cnf(c_1387,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_443,c_271]) ).
cnf(c_20511,plain,
( C = A
| g3_lattices(C,D,E) != g3_lattices(A,u1_lattices(sK0),B)
| ~ m1_relset_1(B,k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(B,k2_zfmisc_1(A,A),A)
| ~ v1_funct_1(B)
| ~ m1_relset_1(u1_lattices(sK0),k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(u1_lattices(sK0),k2_zfmisc_1(A,A),A) ),
inference(resolve,[status(thm)],[c_476,c_357]) ).
cnf(c_1504,plain,
( C = A
| g3_lattices(A,u1_lattices(sK0),B) != g3_lattices(C,D,E)
| ~ m1_relset_1(B,k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(B,k2_zfmisc_1(A,A),A)
| ~ v1_funct_1(B)
| ~ m1_relset_1(u1_lattices(sK0),k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(u1_lattices(sK0),k2_zfmisc_1(A,A),A) ),
inference(copy,[status(thm)],[c_20511]) ).
cnf(c_20512,plain,
( m1_filter_0(sK3(k1_lattice2(sK0),A,B),k1_lattice2(sK0))
| B = A
| ~ m1_subset_1(B,u1_struct_0(k1_lattice2(sK0)))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v17_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_281,c_782]) ).
cnf(c_20513,plain,
( m1_filter_0(sK3(k1_lattice2(sK0),A,B),k1_lattice2(sK0))
| B = A
| ~ m1_subset_1(B,u1_struct_0(k1_lattice2(sK0)))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_20512,c_836]) ).
cnf(c_20514,plain,
( m1_filter_0(sK3(k1_lattice2(sK0),A,B),k1_lattice2(sK0))
| B = A
| ~ m1_subset_1(B,u1_struct_0(k1_lattice2(sK0)))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK0)))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_20513,c_1115]) ).
cnf(c_20515,plain,
( m1_filter_0(sK3(k1_lattice2(sK0),sK1,A),k1_lattice2(sK0))
| A = sK1
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK0)))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_20514,c_1272]) ).
cnf(c_20516,plain,
( m1_filter_0(sK3(k1_lattice2(sK0),sK1,sK2),k1_lattice2(sK0))
| sK2 = sK1
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_20515,c_1273]) ).
cnf(c_20517,plain,
( m1_filter_0(sK3(k1_lattice2(sK0),sK1,sK2),k1_lattice2(sK0))
| sK2 = sK1 ),
inference(resolve,[status(thm)],[c_896,c_20516]) ).
cnf(c_4418,negated_conjecture,
m1_filter_0(sK3(k1_lattice2(sK0),sK1,sK2),k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_268,c_20517]) ).
cnf(c_20518,plain,
( v1_filter_0(sK3(k1_lattice2(sK0),A,B),k1_lattice2(sK0))
| B = A
| ~ m1_subset_1(B,u1_struct_0(k1_lattice2(sK0)))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v17_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_280,c_782]) ).
cnf(c_20519,plain,
( v1_filter_0(sK3(k1_lattice2(sK0),A,B),k1_lattice2(sK0))
| B = A
| ~ m1_subset_1(B,u1_struct_0(k1_lattice2(sK0)))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_20518,c_836]) ).
cnf(c_20520,plain,
( v1_filter_0(sK3(k1_lattice2(sK0),A,B),k1_lattice2(sK0))
| B = A
| ~ m1_subset_1(B,u1_struct_0(k1_lattice2(sK0)))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK0)))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_20519,c_1115]) ).
cnf(c_20521,plain,
( v1_filter_0(sK3(k1_lattice2(sK0),sK1,A),k1_lattice2(sK0))
| A = sK1
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK0)))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_20520,c_1272]) ).
cnf(c_20522,plain,
( v1_filter_0(sK3(k1_lattice2(sK0),sK1,sK2),k1_lattice2(sK0))
| sK2 = sK1
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_20521,c_1273]) ).
cnf(c_20523,plain,
( v1_filter_0(sK3(k1_lattice2(sK0),sK1,sK2),k1_lattice2(sK0))
| sK2 = sK1 ),
inference(resolve,[status(thm)],[c_896,c_20522]) ).
cnf(c_4422,negated_conjecture,
v1_filter_0(sK3(k1_lattice2(sK0),sK1,sK2),k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_268,c_20523]) ).
cnf(c_20524,plain,
( r2_hidden(B,sK3(k1_lattice2(sK0),A,B))
| r2_hidden(A,sK3(k1_lattice2(sK0),A,B))
| B = A
| ~ m1_subset_1(B,u1_struct_0(k1_lattice2(sK0)))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v17_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_279,c_782]) ).
cnf(c_20525,plain,
( r2_hidden(B,sK3(k1_lattice2(sK0),A,B))
| r2_hidden(A,sK3(k1_lattice2(sK0),A,B))
| B = A
| ~ m1_subset_1(B,u1_struct_0(k1_lattice2(sK0)))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_20524,c_836]) ).
cnf(c_20526,plain,
( r2_hidden(B,sK3(k1_lattice2(sK0),A,B))
| r2_hidden(A,sK3(k1_lattice2(sK0),A,B))
| B = A
| ~ m1_subset_1(B,u1_struct_0(k1_lattice2(sK0)))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK0)))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_20525,c_1115]) ).
cnf(c_20527,plain,
( r2_hidden(A,sK3(k1_lattice2(sK0),sK1,A))
| r2_hidden(sK1,sK3(k1_lattice2(sK0),sK1,A))
| A = sK1
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK0)))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_20526,c_1272]) ).
cnf(c_20528,plain,
( r2_hidden(sK2,sK3(k1_lattice2(sK0),sK1,sK2))
| r2_hidden(sK1,sK3(k1_lattice2(sK0),sK1,sK2))
| sK2 = sK1
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_20527,c_1273]) ).
cnf(c_20529,plain,
( r2_hidden(sK2,sK3(k1_lattice2(sK0),sK1,sK2))
| r2_hidden(sK1,sK3(k1_lattice2(sK0),sK1,sK2))
| sK2 = sK1 ),
inference(resolve,[status(thm)],[c_896,c_20528]) ).
cnf(c_4426,negated_conjecture,
( r2_hidden(sK2,sK3(k1_lattice2(sK0),sK1,sK2))
| r2_hidden(sK1,sK3(k1_lattice2(sK0),sK1,sK2)) ),
inference(resolve,[status(thm)],[c_268,c_20529]) ).
cnf(c_11498,plain,
k14_filter_2(sK0,sK3(k1_lattice2(sK0),sK1,sK2)) = k8_filter_2(sK0,sK3(k1_lattice2(sK0),sK1,sK2)),
inference(resolve,[status(thm)],[c_4418,c_528]) ).
cnf(c_20530,plain,
( m2_filter_2(k14_filter_2(sK0,sK3(k1_lattice2(sK0),sK1,sK2)),sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_4418,c_387]) ).
cnf(c_20531,plain,
( m2_filter_2(k8_filter_2(sK0,sK3(k1_lattice2(sK0),sK1,sK2)),sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(paramod,[status(thm)],[c_11498,c_20530]) ).
cnf(c_20532,negated_conjecture,
( m2_filter_2(k8_filter_2(sK0,sK3(k1_lattice2(sK0),sK1,sK2)),sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_274,c_20531]) ).
cnf(c_20533,negated_conjecture,
( m2_filter_2(k8_filter_2(sK0,sK3(k1_lattice2(sK0),sK1,sK2)),sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_273,c_20532]) ).
cnf(c_11499,negated_conjecture,
m2_filter_2(k8_filter_2(sK0,sK3(k1_lattice2(sK0),sK1,sK2)),sK0),
inference(resolve,[status(thm)],[c_271,c_20533]) ).
cnf(c_20534,plain,
( m1_subset_1(sK3(k1_lattice2(sK0),sK1,sK2),k1_zfmisc_1(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_4418,c_248]) ).
cnf(c_20535,plain,
( m1_subset_1(sK3(k1_lattice2(sK0),sK1,sK2),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_896,c_20534]) ).
cnf(c_20536,plain,
( m1_subset_1(sK3(k1_lattice2(sK0),sK1,sK2),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_782,c_20535]) ).
cnf(c_11500,plain,
m1_subset_1(sK3(k1_lattice2(sK0),sK1,sK2),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0)))),
inference(resolve,[status(thm)],[c_1115,c_20536]) ).
cnf(c_20537,plain,
( A = u1_struct_0(sK0)
| g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0)) != g3_lattices(A,B,C)
| ~ 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))
| ~ m1_relset_1(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ 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_1504,c_490]) ).
cnf(c_20538,plain,
( A = u1_struct_0(sK0)
| k1_lattice2(sK0) != g3_lattices(A,B,C)
| ~ 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))
| ~ m1_relset_1(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)) ),
inference(paramod,[status(thm)],[c_1288,c_20537]) ).
cnf(c_20539,plain,
( A = u1_struct_0(sK0)
| g3_lattices(A,B,C) != 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))
| ~ m1_relset_1(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)) ),
inference(copy,[status(thm)],[c_20538]) ).
cnf(c_20540,plain,
( u1_struct_0(sK0) = A
| g3_lattices(A,B,C) != 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))
| ~ m1_relset_1(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)) ),
inference(copy,[status(thm)],[c_20539]) ).
cnf(c_20541,plain,
( u1_struct_0(sK0) = A
| g3_lattices(A,B,C) != 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))
| ~ 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_477,c_20540]) ).
cnf(c_20542,plain,
( u1_struct_0(sK0) = A
| g3_lattices(A,B,C) != 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(resolve,[status(thm)],[c_1387,c_20541]) ).
cnf(c_20543,plain,
( u1_struct_0(sK0) = A
| g3_lattices(A,B,C) != 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_489,c_20542]) ).
cnf(c_15906,plain,
( u1_struct_0(sK0) = A
| g3_lattices(A,B,C) != k1_lattice2(sK0) ),
inference(resolve,[status(thm)],[c_487,c_20543]) ).
cnf(c_20544,plain,
u1_struct_0(sK0) = u1_struct_0(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_15906,c_1133]) ).
cnf(c_15907,plain,
u1_struct_0(k1_lattice2(sK0)) = u1_struct_0(sK0),
inference(copy,[status(thm)],[c_20544]) ).
cnf(c_15971,plain,
m1_subset_1(sK3(k1_lattice2(sK0),sK1,sK2),k1_zfmisc_1(u1_struct_0(sK0))),
inference(paramod,[status(thm)],[c_15907,c_11500]) ).
cnf(c_16079,negated_conjecture,
( k8_filter_2(sK0,A) = A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(paramod,[status(thm)],[c_15907,c_1168]) ).
cnf(c_16210,plain,
k7_filter_2(sK0,sK3(k1_lattice2(sK0),sK1,sK2)) = sK3(k1_lattice2(sK0),sK1,sK2),
inference(resolve,[status(thm)],[c_15971,c_1210]) ).
cnf(c_16249,plain,
k8_filter_2(sK0,sK3(k1_lattice2(sK0),sK1,sK2)) = sK3(k1_lattice2(sK0),sK1,sK2),
inference(resolve,[status(thm)],[c_16079,c_15971]) ).
cnf(c_16269,negated_conjecture,
m2_filter_2(sK3(k1_lattice2(sK0),sK1,sK2),sK0),
inference(paramod,[status(thm)],[c_16249,c_11499]) ).
cnf(c_20545,plain,
k7_filter_2(sK0,sK3(k1_lattice2(sK0),sK1,sK2)) = k15_filter_2(sK0,sK3(k1_lattice2(sK0),sK1,sK2)),
inference(resolve,[status(thm)],[c_16269,c_527]) ).
cnf(c_20546,plain,
sK3(k1_lattice2(sK0),sK1,sK2) = k15_filter_2(sK0,sK3(k1_lattice2(sK0),sK1,sK2)),
inference(paramod,[status(thm)],[c_16210,c_20545]) ).
cnf(c_16279,plain,
k15_filter_2(sK0,sK3(k1_lattice2(sK0),sK1,sK2)) = sK3(k1_lattice2(sK0),sK1,sK2),
inference(copy,[status(thm)],[c_20546]) ).
cnf(c_20547,plain,
( ~ v1_filter_0(k15_filter_2(sK0,sK3(k1_lattice2(sK0),sK1,sK2)),k1_lattice2(sK0))
| r2_filter_2(sK0,sK3(k1_lattice2(sK0),sK1,sK2)) ),
inference(resolve,[status(thm)],[c_16269,c_520]) ).
cnf(c_20548,plain,
( ~ v1_filter_0(sK3(k1_lattice2(sK0),sK1,sK2),k1_lattice2(sK0))
| r2_filter_2(sK0,sK3(k1_lattice2(sK0),sK1,sK2)) ),
inference(paramod,[status(thm)],[c_16279,c_20547]) ).
cnf(c_16280,plain,
r2_filter_2(sK0,sK3(k1_lattice2(sK0),sK1,sK2)),
inference(resolve,[status(thm)],[c_4422,c_20548]) ).
cnf(c_20549,negated_conjecture,
( r2_hidden(sK2,sK3(k1_lattice2(sK0),sK1,sK2))
| ~ r2_hidden(sK1,sK3(k1_lattice2(sK0),sK1,sK2))
| ~ r2_filter_2(sK0,sK3(k1_lattice2(sK0),sK1,sK2)) ),
inference(resolve,[status(thm)],[c_16269,c_267]) ).
cnf(c_16281,negated_conjecture,
( r2_hidden(sK2,sK3(k1_lattice2(sK0),sK1,sK2))
| ~ r2_hidden(sK1,sK3(k1_lattice2(sK0),sK1,sK2)) ),
inference(resolve,[status(thm)],[c_16280,c_20549]) ).
cnf(c_20550,negated_conjecture,
( r2_hidden(sK1,sK3(k1_lattice2(sK0),sK1,sK2))
| ~ r2_filter_2(sK0,sK3(k1_lattice2(sK0),sK1,sK2))
| ~ m2_filter_2(sK3(k1_lattice2(sK0),sK1,sK2),sK0)
| r2_hidden(sK1,sK3(k1_lattice2(sK0),sK1,sK2)) ),
inference(resolve,[status(thm)],[c_4426,c_266]) ).
cnf(c_20551,negated_conjecture,
( ~ r2_filter_2(sK0,sK3(k1_lattice2(sK0),sK1,sK2))
| ~ m2_filter_2(sK3(k1_lattice2(sK0),sK1,sK2),sK0)
| r2_hidden(sK1,sK3(k1_lattice2(sK0),sK1,sK2)) ),
inference(copy,[status(thm)],[c_20550]) ).
cnf(c_20552,negated_conjecture,
( ~ r2_filter_2(sK0,sK3(k1_lattice2(sK0),sK1,sK2))
| r2_hidden(sK1,sK3(k1_lattice2(sK0),sK1,sK2)) ),
inference(resolve,[status(thm)],[c_16269,c_20551]) ).
cnf(c_20470,negated_conjecture,
r2_hidden(sK1,sK3(k1_lattice2(sK0),sK1,sK2)),
inference(resolve,[status(thm)],[c_16280,c_20552]) ).
cnf(c_20471,negated_conjecture,
r2_hidden(sK2,sK3(k1_lattice2(sK0),sK1,sK2)),
inference(resolve,[status(thm)],[c_20470,c_16281]) ).
cnf(c_20553,plain,
( ~ r2_hidden(sK2,sK3(k1_lattice2(sK0),sK1,sK2))
| sK2 = sK1
| ~ m1_subset_1(sK2,u1_struct_0(k1_lattice2(sK0)))
| ~ m1_subset_1(sK1,u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v17_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_20470,c_278]) ).
cnf(c_20554,plain,
( ~ r2_hidden(sK2,sK3(k1_lattice2(sK0),sK1,sK2))
| sK2 = sK1
| ~ m1_subset_1(sK2,u1_struct_0(k1_lattice2(sK0)))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v17_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(paramod,[status(thm)],[c_15907,c_20553]) ).
cnf(c_20555,plain,
( ~ r2_hidden(sK2,sK3(k1_lattice2(sK0),sK1,sK2))
| sK2 = sK1
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v17_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(paramod,[status(thm)],[c_15907,c_20554]) ).
cnf(c_20556,plain,
( ~ r2_hidden(sK2,sK3(k1_lattice2(sK0),sK1,sK2))
| sK2 = sK1
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v17_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_896,c_20555]) ).
cnf(c_20557,plain,
( ~ r2_hidden(sK2,sK3(k1_lattice2(sK0),sK1,sK2))
| sK2 = sK1
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v17_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_782,c_20556]) ).
cnf(c_20558,plain,
( ~ r2_hidden(sK2,sK3(k1_lattice2(sK0),sK1,sK2))
| sK2 = sK1
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_836,c_20557]) ).
cnf(c_20559,plain,
( ~ r2_hidden(sK2,sK3(k1_lattice2(sK0),sK1,sK2))
| sK2 = sK1
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_1115,c_20558]) ).
cnf(c_20560,negated_conjecture,
( ~ r2_hidden(sK2,sK3(k1_lattice2(sK0),sK1,sK2))
| sK2 = sK1
| ~ m1_subset_1(sK2,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_270,c_20559]) ).
cnf(c_20561,negated_conjecture,
( ~ r2_hidden(sK2,sK3(k1_lattice2(sK0),sK1,sK2))
| sK2 = sK1 ),
inference(resolve,[status(thm)],[c_269,c_20560]) ).
cnf(c_20562,negated_conjecture,
~ r2_hidden(sK2,sK3(k1_lattice2(sK0),sK1,sK2)),
inference(resolve,[status(thm)],[c_268,c_20561]) ).
cnf(c_20477,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_20471,c_20562]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT324+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.13/5.80 % Computer : n010.cluster.edu
% 0.13/5.80 % Model : x86_64 x86_64
% 0.13/5.80 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/5.80 % Memory : 8046.5625MB
% 0.13/5.80 % OS : Linux 6.8.0-71-generic
% 0.13/5.81 % CPULimit : 300
% 0.13/5.81 % WCLimit : 300
% 0.13/5.81 % DateTime : Fri Sep 25 20:53:22 UTC 2026
% 0.13/5.81 % CPUTime :
% 0.13/5.81 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/5.81 % Process 1639290 was started by sandbox on n010,
% 0.13/5.81 % Fri Sep 25 20:53:22 2026
% 0.13/5.81 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.13/5.84
% 0.13/5.84 % From the command line: assign(max_seconds, 300).
% 178.49/29.61
% 178.49/29.61 % given #500 (F,wt=13): 2849 -v1_xboole_0(f1(c17)). [resolve(964,a,1022,a)].
% 178.49/29.61
% 178.49/29.61 % given #1000 (T,wt=21): 705 -m1_filter_0(A,k1_lattice2(c5)) | k14_filter_2(c5,A) = k8_filter_2(c5,A). [resolve(347,a,290,b),unit_del(a,353),unit_del(b,354)].
% 178.49/29.61
% 178.49/29.61 % given #1500 (F,wt=21): 8662 -r2_hidden(u1_struct_0(c8),f4(f1(c8))). [resolve(7977,a,408,b)].
% 178.49/29.61
% 178.49/29.61 % given #2000 (T,wt=23): 12051 r2_hidden(k8_filter_2(c8,f5(c8)),k1_zfmisc_1(u1_struct_0(c8))). [resolve(7535,a,286,a),unit_del(a,373)].
% 178.49/29.61
% 178.49/29.61 % given #2500 (A,wt=38): 1215 v3_struct_0(A) | -v10_lattices(A) | -l3_lattices(A) | k7_filter_2(A,f9(u1_struct_0(A))) = f9(u1_struct_0(A)) | v1_xboole_0(u1_struct_0(A)). [resolve(390,d,311,b)].
% 178.49/29.61
% 178.49/29.61 % given #3000 (T,wt=27): 4558 m1_subset_1(f6(c7),k1_zfmisc_1(u1_struct_0(k1_lattice2(c7)))). [resolve(667,a,384,d),rewrite([4557(10)]),unit_del(a,334),unit_del(b,328),unit_del(c,335)].
% 178.49/29.61
% 178.49/29.61 % given #3500 (A,wt=36): 1561 -v1_funct_2(u2_lattices(c18),k2_zfmisc_1(A,A),A) | -m1_relset_1(u2_lattices(c18),k2_zfmisc_1(A,A),A) | l3_lattices(g3_lattices(A,u2_lattices(c18),u2_lattices(c18))). [resolve(489,a,463,a)].
% 178.49/29.61
% 178.49/29.61 % given #4000 (F,wt=49): 18115 -v1_funct_2(u2_lattices(c8),k2_zfmisc_1(u1_struct_0(c18),u1_struct_0(c18)),u1_struct_0(c18)) | -m1_relset_1(u2_lattices(c8),k2_zfmisc_1(u1_struct_0(c18),u1_struct_0(c18)),u1_struct_0(c18)) | -v3_struct_0(g3_lattices(u1_struct_0(c18),u2_lattices(c8),u2_lattices(k1_lattice2(c18)))). [resolve(16406,a,652,a)].
% 178.49/29.61
% 178.49/29.61 % given #4500 (W,wt=28): 19443 m1_subset_1(f4(f1(k1_lattice2(c7))),u1_struct_0(k1_lattice2(c7))). [resolve(4861,a,2943,b),unit_del(a,4857)].
% 178.49/29.61
% 178.49/29.61 % SZS status Theorem for theBenchmark
% 178.49/29.61
% 178.49/29.61 % Proof 1 at 6.20 (+ 1.37) seconds.
% 178.49/29.61 % Length of proof is 123.
% 178.49/29.61 % Level of proof is 14.
% 178.49/29.61 % Maximum clause weight is 56.000.
% 178.49/29.61 % Given clauses 4574.
% 178.49/29.61
% 178.49/29.61 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------