%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT307+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 : n014.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 6.41s 1.45s
% Output : CNFRefutation 6.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 24
% Syntax : Number of formulae : 205 ( 41 unt; 0 def)
% Number of atoms : 760 ( 109 equ)
% Maximal formula atoms : 21 ( 3 avg)
% Number of connectives : 924 ( 369 ~; 425 |; 85 &)
% ( 4 <=>; 41 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 29 ( 27 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 2 con; 0-3 aty)
% Number of variables : 191 ( 18 sgn 61 !; 3 ?)
% 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(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_k15_filter_2,axiom,
! [A,B] :
( ( m2_filter_2(B,A)
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m1_filter_2(k15_filter_2(A,B),k1_lattice2(A)) ),
file('theBenchmark.p',dt_k15_filter_2) ).
fof(dt_k1_lattice2,axiom,
! [A] :
( l3_lattices(A)
=> ( l3_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) ) ),
file('theBenchmark.p',dt_k1_lattice2) ).
fof(dt_l3_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( l2_lattices(A)
& l1_lattices(A) ) ),
file('theBenchmark.p',dt_l3_lattices) ).
fof(dt_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_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( m2_lattice4(B,A)
& ~ v1_xboole_0(B) ) ) ),
file('theBenchmark.p',dt_m2_filter_2) ).
fof(dt_m2_lattice4,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_lattice4(B,A)
=> m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ),
file('theBenchmark.p',dt_m2_lattice4) ).
fof(dt_u1_lattices,axiom,
! [A] :
( l1_lattices(A)
=> ( m2_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_1(u1_lattices(A)) ) ),
file('theBenchmark.p',dt_u1_lattices) ).
fof(dt_u2_lattices,axiom,
! [A] :
( l2_lattices(A)
=> ( m2_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_1(u2_lattices(A)) ) ),
file('theBenchmark.p',dt_u2_lattices) ).
fof(fc1_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_struct_0(A) )
=> ( v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ),
file('theBenchmark.p',fc1_lattice2) ).
fof(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(t22_filter_0,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v13_lattices(A)
=> ! [B] :
( m1_filter_0(B,A)
=> ~ ( ! [C] :
( m1_filter_0(C,A)
=> ~ ( v1_filter_0(C,A)
& r1_tarski(B,C) ) )
& B != u1_struct_0(A) ) ) ) ),
file('theBenchmark.p',t22_filter_0) ).
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(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(t34_filter_2,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v14_lattices(A)
=> ! [B] :
( m2_filter_2(B,A)
=> ~ ( ! [C] :
( m2_filter_2(C,A)
=> ~ ( r2_filter_2(A,C)
& r1_tarski(B,C) ) )
& B != u1_struct_0(A) ) ) ) ),
file('theBenchmark.p',t34_filter_2) ).
fof(t34_filter_2_neg,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v14_lattices(A)
=> ! [B] :
( m2_filter_2(B,A)
=> ~ ( ! [C] :
( m2_filter_2(C,A)
=> ~ ( r2_filter_2(A,C)
& r1_tarski(B,C) ) )
& B != u1_struct_0(A) ) ) ) ),
inference(assume_negation,[status(cth)],[t34_filter_2]) ).
cnf(c_94,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]) ).
fof(nnf_90,plain,
? [A] :
( ? [B] :
( ! [C] :
( ~ r2_filter_2(A,C)
| ~ r1_tarski(B,C)
| ~ m2_filter_2(C,A) )
& u1_struct_0(A) != B
& m2_filter_2(B,A) )
& v14_lattices(A)
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t34_filter_2_neg]) ).
fof(sk_t34_filter_2_neg,plain,
( ! [C] :
( ~ r2_filter_2(sK0,C)
| ~ r1_tarski(sK2,C)
| ~ m2_filter_2(C,sK0) )
& u1_struct_0(sK0) != sK2
& m2_filter_2(sK2,sK0)
& v14_lattices(sK0)
& l3_lattices(sK0)
& v10_lattices(sK0)
& ~ v3_struct_0(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK2]),skolemize(A,sK0),skolemize(B,sK2)],[nnf_90]) ).
cnf(c_96,negated_conjecture,
v14_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t34_filter_2_neg]) ).
cnf(c_97,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_99,plain,
( v3_lattices(k1_lattice2(A))
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_k1_lattice2]) ).
cnf(c_170,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_171,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_173,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_175,plain,
( m1_filter_2(k15_filter_2(A,B),k1_lattice2(A))
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k15_filter_2]) ).
cnf(c_183,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_186,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_188,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_173,c_171]) ).
cnf(c_190,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_192,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_194,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,
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ 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) ),
inference(resolve,[status(thm)],[c_188,c_183]) ).
cnf(c_9669,plain,
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ m1_filter_0(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_198]) ).
cnf(c_9670,plain,
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ m1_filter_0(B,A)
| ~ l3_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_9669]) ).
cnf(c_9671,plain,
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ m1_filter_0(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_9670]) ).
cnf(c_9672,plain,
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| ~ m1_filter_0(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_9671]) ).
cnf(c_9673,plain,
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ m1_filter_0(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_9672]) ).
cnf(c_199,plain,
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_filter_0(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_9673]) ).
cnf(c_202,plain,
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_186,c_183]) ).
cnf(c_9674,plain,
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_202]) ).
cnf(c_9675,plain,
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_9674]) ).
cnf(c_203,plain,
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_9675]) ).
cnf(c_208,plain,
( m1_filter_0(k15_filter_2(A,B),k1_lattice2(A))
| ~ l3_lattices(k1_lattice2(A))
| ~ v10_lattices(k1_lattice2(A))
| v3_struct_0(k1_lattice2(A))
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_175,c_170]) ).
cnf(c_226,plain,
( ~ l3_lattices(A)
| g3_lattices(u1_struct_0(k1_lattice2(A)),u2_lattices(k1_lattice2(A)),u1_lattices(k1_lattice2(A))) = k1_lattice2(A)
| ~ l3_lattices(k1_lattice2(A)) ),
inference(resolve,[status(thm)],[c_97,c_99]) ).
cnf(c_230,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_231,plain,
( g3_lattices(u1_struct_0(A),u1_lattices(A),u2_lattices(A)) = k1_lattice2(A)
| ~ l3_lattices(A) ),
inference(copy,[status(thm)],[c_230]) ).
cnf(c_232,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_233,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_235,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_236,plain,
( l3_lattices(k1_lattice2(A))
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_k1_lattice2]) ).
cnf(c_239,plain,
( l1_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_240,plain,
( l2_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_243,plain,
( v1_funct_1(u1_lattices(A))
| ~ l1_lattices(A) ),
inference(clausify,[status(thm)],[dt_u1_lattices]) ).
cnf(c_244,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_245,plain,
( v1_funct_1(u2_lattices(A))
| ~ l2_lattices(A) ),
inference(clausify,[status(thm)],[dt_u2_lattices]) ).
cnf(c_246,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_255,plain,
( ~ v3_struct_0(k1_lattice2(A))
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_lattice2]) ).
cnf(c_261,plain,
( v10_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc6_lattice2]) ).
cnf(c_262,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_287,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_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]) ).
fof(nnf_80,plain,
! [A] :
( ! [B] :
( ? [C] :
( v1_filter_0(C,A)
& r1_tarski(B,C)
& m1_filter_0(C,A) )
| u1_struct_0(A) = B
| ~ m1_filter_0(B,A) )
| ~ v13_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t22_filter_0]) ).
fof(sk_t22_filter_0_sk,plain,
! [A] :
( ! [B] :
( ( v1_filter_0(sK1(A,B),A)
& r1_tarski(B,sK1(A,B))
& m1_filter_0(sK1(A,B),A) )
| u1_struct_0(A) = B
| ~ m1_filter_0(B,A) )
| ~ v13_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(C,sK1(A,B))],[nnf_80]) ).
fof(sk_t22_filter_0,plain,
( ! [VAR_0,VAR_1] :
( v1_filter_0(sK1(VAR_0,VAR_1),VAR_0)
| u1_struct_0(VAR_0) = VAR_1
| ~ m1_filter_0(VAR_1,VAR_0)
| ~ v13_lattices(VAR_0)
| ~ l3_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1] :
( r1_tarski(VAR_1,sK1(VAR_0,VAR_1))
| u1_struct_0(VAR_0) = VAR_1
| ~ m1_filter_0(VAR_1,VAR_0)
| ~ v13_lattices(VAR_0)
| ~ l3_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1] :
( m1_filter_0(sK1(VAR_0,VAR_1),VAR_0)
| u1_struct_0(VAR_0) = VAR_1
| ~ m1_filter_0(VAR_1,VAR_0)
| ~ v13_lattices(VAR_0)
| ~ l3_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_t22_filter_0_sk]) ).
cnf(c_292,plain,
( m1_filter_0(sK1(A,B),A)
| u1_struct_0(A) = B
| ~ m1_filter_0(B,A)
| ~ v13_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(split_conjunct,[status(thm)],[sk_t22_filter_0]) ).
cnf(c_293,plain,
( r1_tarski(B,sK1(A,B))
| u1_struct_0(A) = B
| ~ m1_filter_0(B,A)
| ~ v13_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(split_conjunct,[status(thm)],[sk_t22_filter_0]) ).
cnf(c_294,plain,
( v1_filter_0(sK1(A,B),A)
| u1_struct_0(A) = B
| ~ m1_filter_0(B,A)
| ~ v13_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(split_conjunct,[status(thm)],[sk_t22_filter_0]) ).
cnf(c_297,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_305,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t34_filter_2_neg]) ).
cnf(c_306,negated_conjecture,
v10_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t34_filter_2_neg]) ).
cnf(c_307,negated_conjecture,
l3_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t34_filter_2_neg]) ).
cnf(c_308,negated_conjecture,
m2_filter_2(sK2,sK0),
inference(split_conjunct,[status(thm)],[sk_t34_filter_2_neg]) ).
cnf(c_309,negated_conjecture,
u1_struct_0(sK0) != sK2,
inference(split_conjunct,[status(thm)],[sk_t34_filter_2_neg]) ).
cnf(c_310,negated_conjecture,
( ~ r2_filter_2(sK0,A)
| ~ r1_tarski(sK2,A)
| ~ m2_filter_2(A,sK0) ),
inference(split_conjunct,[status(thm)],[sk_t34_filter_2_neg]) ).
cnf(c_313,negated_conjecture,
( v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_96,c_94]) ).
cnf(c_9676,negated_conjecture,
( v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_305,c_313]) ).
cnf(c_9677,negated_conjecture,
( v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_306,c_9676]) ).
cnf(c_314,negated_conjecture,
v13_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_307,c_9677]) ).
cnf(c_349,plain,
( ~ l2_lattices(A)
| m1_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ),
inference(resolve,[status(thm)],[c_194,c_192]) ).
cnf(c_350,plain,
( ~ l1_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_194,c_190]) ).
cnf(c_9678,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_306,c_297]) ).
cnf(c_9679,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_305,c_9678]) ).
cnf(c_691,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_307,c_9679]) ).
cnf(c_9680,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_306,c_289]) ).
cnf(c_9681,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_305,c_9680]) ).
cnf(c_696,negated_conjecture,
( k7_filter_2(sK0,A) = k15_filter_2(sK0,A)
| ~ m2_filter_2(A,sK0) ),
inference(resolve,[status(thm)],[c_307,c_9681]) ).
cnf(c_9682,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_306,c_287]) ).
cnf(c_9683,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_305,c_9682]) ).
cnf(c_697,negated_conjecture,
( k14_filter_2(sK0,A) = k8_filter_2(sK0,A)
| ~ m1_filter_0(A,k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_307,c_9683]) ).
cnf(c_9684,negated_conjecture,
( v10_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_306,c_261]) ).
cnf(c_9685,negated_conjecture,
( v10_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_305,c_9684]) ).
cnf(c_699,negated_conjecture,
v10_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_307,c_9685]) ).
cnf(c_9686,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_306,c_233]) ).
cnf(c_9687,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_305,c_9686]) ).
cnf(c_709,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_307,c_9687]) ).
cnf(c_9688,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_306,c_232]) ).
cnf(c_9689,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_305,c_9688]) ).
cnf(c_710,negated_conjecture,
( k7_filter_2(sK0,A) = A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_307,c_9689]) ).
cnf(c_9690,negated_conjecture,
( ~ v3_struct_0(k1_lattice2(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_307,c_255]) ).
cnf(c_721,negated_conjecture,
~ v3_struct_0(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_305,c_9690]) ).
cnf(c_722,plain,
l2_lattices(sK0),
inference(resolve,[status(thm)],[c_307,c_240]) ).
cnf(c_723,plain,
l1_lattices(sK0),
inference(resolve,[status(thm)],[c_307,c_239]) ).
cnf(c_724,plain,
l3_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_307,c_236]) ).
cnf(c_725,plain,
g3_lattices(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0)) = k1_lattice2(sK0),
inference(resolve,[status(thm)],[c_307,c_231]) ).
cnf(c_9691,negated_conjecture,
( 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_307,c_226]) ).
cnf(c_726,negated_conjecture,
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_724,c_9691]) ).
cnf(c_9692,negated_conjecture,
( k7_filter_2(sK0,sK2) = k15_filter_2(sK0,sK2)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_308,c_289]) ).
cnf(c_9693,negated_conjecture,
( k7_filter_2(sK0,sK2) = k15_filter_2(sK0,sK2)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_305,c_9692]) ).
cnf(c_9694,negated_conjecture,
( k7_filter_2(sK0,sK2) = k15_filter_2(sK0,sK2)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_306,c_9693]) ).
cnf(c_732,negated_conjecture,
k7_filter_2(sK0,sK2) = k15_filter_2(sK0,sK2),
inference(resolve,[status(thm)],[c_307,c_9694]) ).
cnf(c_9695,negated_conjecture,
( m1_filter_0(k15_filter_2(sK0,sK2),k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_308,c_208]) ).
cnf(c_9696,negated_conjecture,
( m1_filter_0(k15_filter_2(sK0,sK2),k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_305,c_9695]) ).
cnf(c_9697,negated_conjecture,
( m1_filter_0(k15_filter_2(sK0,sK2),k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_306,c_9696]) ).
cnf(c_9698,negated_conjecture,
( m1_filter_0(k15_filter_2(sK0,sK2),k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_307,c_9697]) ).
cnf(c_9699,negated_conjecture,
( m1_filter_0(k15_filter_2(sK0,sK2),k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_721,c_9698]) ).
cnf(c_9700,negated_conjecture,
( m1_filter_0(k15_filter_2(sK0,sK2),k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_699,c_9699]) ).
cnf(c_735,negated_conjecture,
m1_filter_0(k15_filter_2(sK0,sK2),k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_724,c_9700]) ).
cnf(c_9701,negated_conjecture,
( m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_308,c_203]) ).
cnf(c_9702,negated_conjecture,
( m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_305,c_9701]) ).
cnf(c_9703,negated_conjecture,
( m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_306,c_9702]) ).
cnf(c_736,negated_conjecture,
m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK0))),
inference(resolve,[status(thm)],[c_307,c_9703]) ).
cnf(c_983,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_722,c_349]) ).
cnf(c_988,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_722,c_246]) ).
cnf(c_989,plain,
v1_funct_1(u2_lattices(sK0)),
inference(resolve,[status(thm)],[c_722,c_245]) ).
cnf(c_1032,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_723,c_350]) ).
cnf(c_1034,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_723,c_244]) ).
cnf(c_1035,plain,
v1_funct_1(u1_lattices(sK0)),
inference(resolve,[status(thm)],[c_723,c_243]) ).
cnf(c_9704,plain,
( v1_filter_0(sK1(k1_lattice2(sK0),k15_filter_2(sK0,sK2)),k1_lattice2(sK0))
| u1_struct_0(k1_lattice2(sK0)) = k15_filter_2(sK0,sK2)
| ~ v13_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_735,c_294]) ).
cnf(c_9705,plain,
( v1_filter_0(sK1(k1_lattice2(sK0),k15_filter_2(sK0,sK2)),k1_lattice2(sK0))
| u1_struct_0(k1_lattice2(sK0)) = k15_filter_2(sK0,sK2)
| ~ v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_721,c_9704]) ).
cnf(c_9706,plain,
( v1_filter_0(sK1(k1_lattice2(sK0),k15_filter_2(sK0,sK2)),k1_lattice2(sK0))
| u1_struct_0(k1_lattice2(sK0)) = k15_filter_2(sK0,sK2)
| ~ v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_699,c_9705]) ).
cnf(c_9707,plain,
( v1_filter_0(sK1(k1_lattice2(sK0),k15_filter_2(sK0,sK2)),k1_lattice2(sK0))
| u1_struct_0(k1_lattice2(sK0)) = k15_filter_2(sK0,sK2)
| ~ v13_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_724,c_9706]) ).
cnf(c_1918,negated_conjecture,
( v1_filter_0(sK1(k1_lattice2(sK0),k15_filter_2(sK0,sK2)),k1_lattice2(sK0))
| u1_struct_0(k1_lattice2(sK0)) = k15_filter_2(sK0,sK2) ),
inference(resolve,[status(thm)],[c_314,c_9707]) ).
cnf(c_9708,plain,
( r1_tarski(k15_filter_2(sK0,sK2),sK1(k1_lattice2(sK0),k15_filter_2(sK0,sK2)))
| u1_struct_0(k1_lattice2(sK0)) = k15_filter_2(sK0,sK2)
| ~ v13_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_735,c_293]) ).
cnf(c_9709,plain,
( r1_tarski(k15_filter_2(sK0,sK2),sK1(k1_lattice2(sK0),k15_filter_2(sK0,sK2)))
| u1_struct_0(k1_lattice2(sK0)) = k15_filter_2(sK0,sK2)
| ~ v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_721,c_9708]) ).
cnf(c_9710,plain,
( r1_tarski(k15_filter_2(sK0,sK2),sK1(k1_lattice2(sK0),k15_filter_2(sK0,sK2)))
| u1_struct_0(k1_lattice2(sK0)) = k15_filter_2(sK0,sK2)
| ~ v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_699,c_9709]) ).
cnf(c_9711,plain,
( r1_tarski(k15_filter_2(sK0,sK2),sK1(k1_lattice2(sK0),k15_filter_2(sK0,sK2)))
| u1_struct_0(k1_lattice2(sK0)) = k15_filter_2(sK0,sK2)
| ~ v13_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_724,c_9710]) ).
cnf(c_1919,negated_conjecture,
( r1_tarski(k15_filter_2(sK0,sK2),sK1(k1_lattice2(sK0),k15_filter_2(sK0,sK2)))
| u1_struct_0(k1_lattice2(sK0)) = k15_filter_2(sK0,sK2) ),
inference(resolve,[status(thm)],[c_314,c_9711]) ).
cnf(c_9712,plain,
( m1_filter_0(sK1(k1_lattice2(sK0),k15_filter_2(sK0,sK2)),k1_lattice2(sK0))
| u1_struct_0(k1_lattice2(sK0)) = k15_filter_2(sK0,sK2)
| ~ v13_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_735,c_292]) ).
cnf(c_9713,plain,
( m1_filter_0(sK1(k1_lattice2(sK0),k15_filter_2(sK0,sK2)),k1_lattice2(sK0))
| u1_struct_0(k1_lattice2(sK0)) = k15_filter_2(sK0,sK2)
| ~ v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_721,c_9712]) ).
cnf(c_9714,plain,
( m1_filter_0(sK1(k1_lattice2(sK0),k15_filter_2(sK0,sK2)),k1_lattice2(sK0))
| u1_struct_0(k1_lattice2(sK0)) = k15_filter_2(sK0,sK2)
| ~ v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_699,c_9713]) ).
cnf(c_9715,plain,
( m1_filter_0(sK1(k1_lattice2(sK0),k15_filter_2(sK0,sK2)),k1_lattice2(sK0))
| u1_struct_0(k1_lattice2(sK0)) = k15_filter_2(sK0,sK2)
| ~ v13_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_724,c_9714]) ).
cnf(c_1920,negated_conjecture,
( m1_filter_0(sK1(k1_lattice2(sK0),k15_filter_2(sK0,sK2)),k1_lattice2(sK0))
| u1_struct_0(k1_lattice2(sK0)) = k15_filter_2(sK0,sK2) ),
inference(resolve,[status(thm)],[c_314,c_9715]) ).
cnf(c_9716,plain,
( k7_filter_2(sK0,sK2) = sK2
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_736,c_232]) ).
cnf(c_9717,plain,
( k15_filter_2(sK0,sK2) = sK2
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(paramod,[status(thm)],[c_732,c_9716]) ).
cnf(c_9718,negated_conjecture,
( k15_filter_2(sK0,sK2) = sK2
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_305,c_9717]) ).
cnf(c_9719,negated_conjecture,
( k15_filter_2(sK0,sK2) = sK2
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_306,c_9718]) ).
cnf(c_2691,negated_conjecture,
k15_filter_2(sK0,sK2) = sK2,
inference(resolve,[status(thm)],[c_307,c_9719]) ).
cnf(c_9720,negated_conjecture,
( m1_filter_0(sK1(k1_lattice2(sK0),k15_filter_2(sK0,sK2)),k1_lattice2(sK0))
| u1_struct_0(k1_lattice2(sK0)) = sK2 ),
inference(paramod,[status(thm)],[c_2691,c_1920]) ).
cnf(c_2694,negated_conjecture,
( m1_filter_0(sK1(k1_lattice2(sK0),sK2),k1_lattice2(sK0))
| u1_struct_0(k1_lattice2(sK0)) = sK2 ),
inference(paramod,[status(thm)],[c_2691,c_9720]) ).
cnf(c_9721,negated_conjecture,
( r1_tarski(k15_filter_2(sK0,sK2),sK1(k1_lattice2(sK0),k15_filter_2(sK0,sK2)))
| u1_struct_0(k1_lattice2(sK0)) = sK2 ),
inference(paramod,[status(thm)],[c_2691,c_1919]) ).
cnf(c_9722,negated_conjecture,
( r1_tarski(sK2,sK1(k1_lattice2(sK0),k15_filter_2(sK0,sK2)))
| u1_struct_0(k1_lattice2(sK0)) = sK2 ),
inference(paramod,[status(thm)],[c_2691,c_9721]) ).
cnf(c_2695,negated_conjecture,
( r1_tarski(sK2,sK1(k1_lattice2(sK0),sK2))
| u1_struct_0(k1_lattice2(sK0)) = sK2 ),
inference(paramod,[status(thm)],[c_2691,c_9722]) ).
cnf(c_9723,negated_conjecture,
( v1_filter_0(sK1(k1_lattice2(sK0),k15_filter_2(sK0,sK2)),k1_lattice2(sK0))
| u1_struct_0(k1_lattice2(sK0)) = sK2 ),
inference(paramod,[status(thm)],[c_2691,c_1918]) ).
cnf(c_2696,negated_conjecture,
( v1_filter_0(sK1(k1_lattice2(sK0),sK2),k1_lattice2(sK0))
| u1_struct_0(k1_lattice2(sK0)) = sK2 ),
inference(paramod,[status(thm)],[c_2691,c_9723]) ).
cnf(c_9724,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_2(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))
| ~ v1_funct_1(u1_lattices(sK0)) ),
inference(paramod,[status(thm)],[c_725,c_262]) ).
cnf(c_9725,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_2(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))
| ~ v1_funct_1(u1_lattices(sK0)) ),
inference(copy,[status(thm)],[c_9724]) ).
cnf(c_9726,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_2(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_1035,c_9725]) ).
cnf(c_9727,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_2(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_1034,c_9726]) ).
cnf(c_9728,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_2(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_1032,c_9727]) ).
cnf(c_9729,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_2(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_989,c_9728]) ).
cnf(c_9730,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_988,c_9729]) ).
cnf(c_4338,plain,
( u1_struct_0(sK0) = A
| g3_lattices(A,B,C) != k1_lattice2(sK0) ),
inference(resolve,[status(thm)],[c_983,c_9730]) ).
cnf(c_9731,plain,
u1_struct_0(sK0) = u1_struct_0(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_4338,c_726]) ).
cnf(c_4827,plain,
u1_struct_0(k1_lattice2(sK0)) = u1_struct_0(sK0),
inference(copy,[status(thm)],[c_9731]) ).
cnf(c_9732,negated_conjecture,
( v1_filter_0(sK1(k1_lattice2(sK0),sK2),k1_lattice2(sK0))
| u1_struct_0(sK0) = sK2 ),
inference(paramod,[status(thm)],[c_4827,c_2696]) ).
cnf(c_4847,negated_conjecture,
v1_filter_0(sK1(k1_lattice2(sK0),sK2),k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_309,c_9732]) ).
cnf(c_9733,negated_conjecture,
( r1_tarski(sK2,sK1(k1_lattice2(sK0),sK2))
| u1_struct_0(sK0) = sK2 ),
inference(paramod,[status(thm)],[c_4827,c_2695]) ).
cnf(c_4848,negated_conjecture,
r1_tarski(sK2,sK1(k1_lattice2(sK0),sK2)),
inference(resolve,[status(thm)],[c_309,c_9733]) ).
cnf(c_9734,negated_conjecture,
( m1_filter_0(sK1(k1_lattice2(sK0),sK2),k1_lattice2(sK0))
| u1_struct_0(sK0) = sK2 ),
inference(paramod,[status(thm)],[c_4827,c_2694]) ).
cnf(c_4849,negated_conjecture,
m1_filter_0(sK1(k1_lattice2(sK0),sK2),k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_309,c_9734]) ).
cnf(c_4876,negated_conjecture,
( k8_filter_2(sK0,A) = A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(paramod,[status(thm)],[c_4827,c_709]) ).
cnf(c_4892,plain,
( ~ r2_filter_2(sK0,sK1(k1_lattice2(sK0),sK2))
| ~ m2_filter_2(sK1(k1_lattice2(sK0),sK2),sK0) ),
inference(resolve,[status(thm)],[c_4848,c_310]) ).
cnf(c_5796,plain,
k14_filter_2(sK0,sK1(k1_lattice2(sK0),sK2)) = k8_filter_2(sK0,sK1(k1_lattice2(sK0),sK2)),
inference(resolve,[status(thm)],[c_4849,c_697]) ).
cnf(c_9735,plain,
( m2_filter_2(k14_filter_2(sK0,sK1(k1_lattice2(sK0),sK2)),sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_4849,c_235]) ).
cnf(c_9736,plain,
( m2_filter_2(k8_filter_2(sK0,sK1(k1_lattice2(sK0),sK2)),sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(paramod,[status(thm)],[c_5796,c_9735]) ).
cnf(c_9737,negated_conjecture,
( m2_filter_2(k8_filter_2(sK0,sK1(k1_lattice2(sK0),sK2)),sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_305,c_9736]) ).
cnf(c_9738,negated_conjecture,
( m2_filter_2(k8_filter_2(sK0,sK1(k1_lattice2(sK0),sK2)),sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_306,c_9737]) ).
cnf(c_5800,negated_conjecture,
m2_filter_2(k8_filter_2(sK0,sK1(k1_lattice2(sK0),sK2)),sK0),
inference(resolve,[status(thm)],[c_307,c_9738]) ).
cnf(c_9739,plain,
( m1_subset_1(sK1(k1_lattice2(sK0),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_4849,c_199]) ).
cnf(c_9740,plain,
( m1_subset_1(sK1(k1_lattice2(sK0),sK2),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(paramod,[status(thm)],[c_4827,c_9739]) ).
cnf(c_9741,plain,
( m1_subset_1(sK1(k1_lattice2(sK0),sK2),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_721,c_9740]) ).
cnf(c_9742,plain,
( m1_subset_1(sK1(k1_lattice2(sK0),sK2),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_699,c_9741]) ).
cnf(c_5801,plain,
m1_subset_1(sK1(k1_lattice2(sK0),sK2),k1_zfmisc_1(u1_struct_0(sK0))),
inference(resolve,[status(thm)],[c_724,c_9742]) ).
cnf(c_6709,plain,
k7_filter_2(sK0,sK1(k1_lattice2(sK0),sK2)) = sK1(k1_lattice2(sK0),sK2),
inference(resolve,[status(thm)],[c_5801,c_710]) ).
cnf(c_9512,plain,
k8_filter_2(sK0,sK1(k1_lattice2(sK0),sK2)) = sK1(k1_lattice2(sK0),sK2),
inference(resolve,[status(thm)],[c_4876,c_5801]) ).
cnf(c_9529,negated_conjecture,
m2_filter_2(sK1(k1_lattice2(sK0),sK2),sK0),
inference(paramod,[status(thm)],[c_9512,c_5800]) ).
cnf(c_9537,plain,
~ r2_filter_2(sK0,sK1(k1_lattice2(sK0),sK2)),
inference(resolve,[status(thm)],[c_9529,c_4892]) ).
cnf(c_9743,plain,
k7_filter_2(sK0,sK1(k1_lattice2(sK0),sK2)) = k15_filter_2(sK0,sK1(k1_lattice2(sK0),sK2)),
inference(resolve,[status(thm)],[c_9529,c_696]) ).
cnf(c_9744,plain,
sK1(k1_lattice2(sK0),sK2) = k15_filter_2(sK0,sK1(k1_lattice2(sK0),sK2)),
inference(paramod,[status(thm)],[c_6709,c_9743]) ).
cnf(c_9667,plain,
k15_filter_2(sK0,sK1(k1_lattice2(sK0),sK2)) = sK1(k1_lattice2(sK0),sK2),
inference(copy,[status(thm)],[c_9744]) ).
cnf(c_9745,plain,
( ~ v1_filter_0(k15_filter_2(sK0,sK1(k1_lattice2(sK0),sK2)),k1_lattice2(sK0))
| r2_filter_2(sK0,sK1(k1_lattice2(sK0),sK2)) ),
inference(resolve,[status(thm)],[c_9529,c_691]) ).
cnf(c_9746,plain,
( ~ v1_filter_0(sK1(k1_lattice2(sK0),sK2),k1_lattice2(sK0))
| r2_filter_2(sK0,sK1(k1_lattice2(sK0),sK2)) ),
inference(paramod,[status(thm)],[c_9667,c_9745]) ).
cnf(c_9747,plain,
~ v1_filter_0(sK1(k1_lattice2(sK0),sK2),k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_9537,c_9746]) ).
cnf(c_9668,plain,
$false,
inference(resolve,[status(thm)],[c_4847,c_9747]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT307+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n014.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 20:41:02 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.36 % Process 1047645 was started by sandbox2 on n014,
% 0.10/0.36 % Fri Sep 25 20:41:02 2026
% 0.10/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.13/0.38
% 0.13/0.38 % From the command line: assign(max_seconds, 300).
% 6.41/1.45
% 6.41/1.45 % given #500 (A,wt=48): 506 -v1_funct_1(A) | -v1_funct_2(A,k2_zfmisc_1(B,B),B) | -m1_relset_1(A,k2_zfmisc_1(B,B),B) | -v1_funct_2(c10,k2_zfmisc_1(B,B),B) | -m1_relset_1(c10,k2_zfmisc_1(B,B),B) | g3_lattices(B,A,c10) != g3_lattices(C,D,E) | D = A. [resolve(279,a,263,d),flip(f)].
% 6.41/1.45
% 6.41/1.45 % given #1000 (F,wt=21): 4776 -r2_hidden(u1_struct_0(c14),f4(f8(c14))). [resolve(4008,a,228,b)].
% 6.41/1.45
% 6.41/1.45 % given #1500 (F,wt=32): 8682 -v10_lattices(g3_lattices(u1_struct_0(c15),u2_lattices(c15),u2_lattices(c15))) | -m1_filter_0(k1_xboole_0,g3_lattices(u1_struct_0(c15),u2_lattices(c15),u2_lattices(c15))). [resolve(8651,a,403,c),unit_del(a,8650)].
% 6.41/1.45
% 6.41/1.45 % SZS status Theorem for theBenchmark
% 6.41/1.45
% 6.41/1.45 % Proof 1 at 0.85 (+ 0.18) seconds.
% 6.41/1.45 % Length of proof is 120.
% 6.41/1.45 % Level of proof is 12.
% 6.41/1.45 % Maximum clause weight is 50.000.
% 6.41/1.45 % Given clauses 1816.
% 6.41/1.45
% 6.41/1.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------