%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT326+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 : n018.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:14 AM UTC 2026
% Result : Theorem 3.66s 0.98s
% Output : CNFRefutation 3.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 17
% Syntax : Number of formulae : 221 ( 47 unt; 0 def)
% Number of atoms : 1133 ( 101 equ)
% Maximal formula atoms : 19 ( 5 avg)
% Number of connectives : 1524 ( 612 ~; 756 |; 115 &)
% ( 0 <=>; 41 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 26 ( 24 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-2 aty)
% Number of variables : 164 ( 5 sgn 34 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cc1_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( ( v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A) ) ) ),
file('theBenchmark.p',cc1_lattices) ).
fof(dt_l2_lattices,axiom,
! [A] :
( l2_lattices(A)
=> l1_struct_0(A) ),
file('theBenchmark.p',dt_l2_lattices) ).
fof(dt_l3_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( l2_lattices(A)
& l1_lattices(A) ) ),
file('theBenchmark.p',dt_l3_lattices) ).
fof(dt_m2_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_struct_0,axiom,
! [A] :
( ( l1_struct_0(A)
& ~ v3_struct_0(A) )
=> ~ v1_xboole_0(u1_struct_0(A)) ),
file('theBenchmark.p',fc1_struct_0) ).
fof(fc2_lattice2,axiom,
! [A] :
( ( l2_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A) )
=> ( v1_partfun1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_binop_1(u2_lattices(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))
& v1_relat_1(u2_lattices(A)) ) ),
file('theBenchmark.p',fc2_lattice2) ).
fof(fc2_realset1,axiom,
! [A,B] :
( ( v1_funct_1(A)
& v1_relat_1(A) )
=> ( v1_funct_1(k1_realset1(A,B))
& v1_relat_1(k1_realset1(A,B)) ) ),
file('theBenchmark.p',fc2_realset1) ).
fof(fc3_lattice2,axiom,
! [A] :
( ( l2_lattices(A)
& v5_lattices(A)
& ~ v3_struct_0(A) )
=> ( v1_partfun1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v2_binop_1(u2_lattices(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))
& v1_relat_1(u2_lattices(A)) ) ),
file('theBenchmark.p',fc3_lattice2) ).
fof(fc4_lattice2,axiom,
! [A] :
( ( l1_lattices(A)
& v6_lattices(A)
& ~ v3_struct_0(A) )
=> ( v1_partfun1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_binop_1(u1_lattices(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))
& v1_relat_1(u1_lattices(A)) ) ),
file('theBenchmark.p',fc4_lattice2) ).
fof(fc5_lattice2,axiom,
! [A] :
( ( l1_lattices(A)
& v7_lattices(A)
& ~ v3_struct_0(A) )
=> ( v1_partfun1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v2_binop_1(u1_lattices(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))
& v1_relat_1(u1_lattices(A)) ) ),
file('theBenchmark.p',fc5_lattice2) ).
fof(t1_filter_2,axiom,
! [A] :
( ~ v1_xboole_0(A)
=> ! [B] :
( ( m1_subset_1(B,k1_zfmisc_1(A))
& ~ v1_xboole_0(B) )
=> ! [C] :
( ( m2_relset_1(C,k2_zfmisc_1(A,A),A)
& v1_funct_2(C,k2_zfmisc_1(A,A),A)
& v1_funct_1(C) )
=> ! [D] :
( ( m2_relset_1(D,k2_zfmisc_1(B,B),B)
& v1_funct_2(D,k2_zfmisc_1(B,B),B)
& v1_funct_1(D) )
=> ( D = k1_realset1(C,B)
=> ( ( v2_binop_1(C,A)
=> v2_binop_1(D,B) )
& ( v3_binop_1(C,A)
=> v3_binop_1(D,B) )
& ( v1_binop_1(C,A)
=> v1_binop_1(D,B) ) ) ) ) ) ) ),
file('theBenchmark.p',t1_filter_2) ).
fof(t40_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> r1_lattice2(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) ),
file('theBenchmark.p',t40_lattice2) ).
fof(t41_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> r1_lattice2(u1_struct_0(A),u1_lattices(A),u2_lattices(A)) ),
file('theBenchmark.p',t41_lattice2) ).
fof(t5_filter_2,axiom,
! [A] :
( ~ v1_xboole_0(A)
=> ! [B] :
( ( m1_subset_1(B,k1_zfmisc_1(A))
& ~ v1_xboole_0(B) )
=> ! [C] :
( ( m2_relset_1(C,k2_zfmisc_1(A,A),A)
& v1_funct_2(C,k2_zfmisc_1(A,A),A)
& v1_funct_1(C) )
=> ! [D] :
( ( m2_relset_1(D,k2_zfmisc_1(A,A),A)
& v1_funct_2(D,k2_zfmisc_1(A,A),A)
& v1_funct_1(D) )
=> ! [E] :
( ( m2_relset_1(E,k2_zfmisc_1(B,B),B)
& v1_funct_2(E,k2_zfmisc_1(B,B),B)
& v1_funct_1(E) )
=> ! [F] :
( ( m2_relset_1(F,k2_zfmisc_1(B,B),B)
& v1_funct_2(F,k2_zfmisc_1(B,B),B)
& v1_funct_1(F) )
=> ( ( r1_lattice2(A,C,D)
& F = k1_realset1(D,B)
& E = k1_realset1(C,B) )
=> r1_lattice2(B,E,F) ) ) ) ) ) ) ),
file('theBenchmark.p',t5_filter_2) ).
fof(t62_filter_2,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m2_lattice4(B,A)
& ~ v1_xboole_0(B) )
=> ! [C] :
( ( m2_relset_1(C,k2_zfmisc_1(B,B),B)
& v1_funct_2(C,k2_zfmisc_1(B,B),B)
& v1_funct_1(C) )
=> ! [D] :
( ( m2_relset_1(D,k2_zfmisc_1(B,B),B)
& v1_funct_2(D,k2_zfmisc_1(B,B),B)
& v1_funct_1(D) )
=> ( ( D = k1_realset1(u1_lattices(A),B)
& C = k1_realset1(u2_lattices(A),B) )
=> ( r1_lattice2(B,D,C)
& r1_lattice2(B,C,D)
& v2_binop_1(D,B)
& v1_binop_1(D,B)
& v2_binop_1(C,B)
& v1_binop_1(C,B) ) ) ) ) ) ),
file('theBenchmark.p',t62_filter_2) ).
fof(t62_filter_2_neg,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m2_lattice4(B,A)
& ~ v1_xboole_0(B) )
=> ! [C] :
( ( m2_relset_1(C,k2_zfmisc_1(B,B),B)
& v1_funct_2(C,k2_zfmisc_1(B,B),B)
& v1_funct_1(C) )
=> ! [D] :
( ( m2_relset_1(D,k2_zfmisc_1(B,B),B)
& v1_funct_2(D,k2_zfmisc_1(B,B),B)
& v1_funct_1(D) )
=> ( ( D = k1_realset1(u1_lattices(A),B)
& C = k1_realset1(u2_lattices(A),B) )
=> ( r1_lattice2(B,D,C)
& r1_lattice2(B,C,D)
& v2_binop_1(D,B)
& v1_binop_1(D,B)
& v2_binop_1(C,B)
& v1_binop_1(C,B) ) ) ) ) ) ),
inference(assume_negation,[status(cth)],[t62_filter_2]) ).
cnf(c_70,plain,
( v7_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc1_lattices]) ).
cnf(c_71,plain,
( v6_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc1_lattices]) ).
cnf(c_72,plain,
( v5_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc1_lattices]) ).
cnf(c_73,plain,
( v4_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc1_lattices]) ).
cnf(c_74,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_78,plain,
( r1_lattice2(u1_struct_0(A),u2_lattices(A),u1_lattices(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t40_lattice2]) ).
cnf(c_79,plain,
( r1_lattice2(u1_struct_0(A),u1_lattices(A),u2_lattices(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t41_lattice2]) ).
fof(nnf_66,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( ( ~ r1_lattice2(B,D,C)
| ~ r1_lattice2(B,C,D)
| ~ v2_binop_1(D,B)
| ~ v1_binop_1(D,B)
| ~ v2_binop_1(C,B)
| ~ v1_binop_1(C,B) )
& k1_realset1(u1_lattices(A),B) = D
& k1_realset1(u2_lattices(A),B) = C
& m2_relset_1(D,k2_zfmisc_1(B,B),B)
& v1_funct_2(D,k2_zfmisc_1(B,B),B)
& v1_funct_1(D) )
& m2_relset_1(C,k2_zfmisc_1(B,B),B)
& v1_funct_2(C,k2_zfmisc_1(B,B),B)
& v1_funct_1(C) )
& m2_lattice4(B,A)
& ~ v1_xboole_0(B) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t62_filter_2_neg]) ).
fof(sk_t62_filter_2_neg,plain,
( ( ~ r1_lattice2(sK1,sK3,sK2)
| ~ r1_lattice2(sK1,sK2,sK3)
| ~ v2_binop_1(sK3,sK1)
| ~ v1_binop_1(sK3,sK1)
| ~ v2_binop_1(sK2,sK1)
| ~ v1_binop_1(sK2,sK1) )
& k1_realset1(u1_lattices(sK0),sK1) = sK3
& k1_realset1(u2_lattices(sK0),sK1) = sK2
& m2_relset_1(sK3,k2_zfmisc_1(sK1,sK1),sK1)
& v1_funct_2(sK3,k2_zfmisc_1(sK1,sK1),sK1)
& v1_funct_1(sK3)
& m2_relset_1(sK2,k2_zfmisc_1(sK1,sK1),sK1)
& v1_funct_2(sK2,k2_zfmisc_1(sK1,sK1),sK1)
& v1_funct_1(sK2)
& m2_lattice4(sK1,sK0)
& ~ v1_xboole_0(sK1)
& l3_lattices(sK0)
& v10_lattices(sK0)
& ~ v3_struct_0(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(A,sK0),skolemize(B,sK1),skolemize(C,sK2),skolemize(D,sK3)],[nnf_66]) ).
cnf(c_80,negated_conjecture,
v10_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t62_filter_2_neg]) ).
cnf(c_82,negated_conjecture,
( v4_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_80,c_73]) ).
cnf(c_89,plain,
( v1_binop_1(u2_lattices(A),u1_struct_0(A))
| ~ l2_lattices(A)
| ~ v4_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc2_lattice2]) ).
cnf(c_92,plain,
( v1_relat_1(u2_lattices(A))
| ~ l2_lattices(A)
| ~ v4_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc2_lattice2]) ).
cnf(c_97,plain,
( v1_binop_1(u1_lattices(A),u1_struct_0(A))
| ~ l1_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc4_lattice2]) ).
cnf(c_99,plain,
( v1_relat_1(u1_lattices(A))
| ~ l1_lattices(A)
| ~ v7_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc5_lattice2]) ).
cnf(c_102,plain,
( v2_binop_1(u1_lattices(A),u1_struct_0(A))
| ~ l1_lattices(A)
| ~ v7_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc5_lattice2]) ).
cnf(c_104,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_105,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_106,plain,
( v1_funct_1(u1_lattices(A))
| ~ l1_lattices(A) ),
inference(clausify,[status(thm)],[dt_u1_lattices]) ).
cnf(c_107,plain,
( l1_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_109,plain,
( ~ v1_xboole_0(u1_struct_0(A))
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_struct_0]) ).
cnf(c_111,plain,
( l1_struct_0(A)
| ~ l2_lattices(A) ),
inference(clausify,[status(thm)],[dt_l2_lattices]) ).
cnf(c_125,plain,
( v2_binop_1(u1_lattices(A),u1_struct_0(A))
| ~ v7_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(resolve,[status(thm)],[c_107,c_102]) ).
cnf(c_126,plain,
( v1_relat_1(u1_lattices(A))
| ~ v7_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(resolve,[status(thm)],[c_107,c_99]) ).
cnf(c_127,plain,
( v1_binop_1(u1_lattices(A),u1_struct_0(A))
| ~ v6_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(resolve,[status(thm)],[c_107,c_97]) ).
cnf(c_129,plain,
( m2_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
| ~ l3_lattices(A) ),
inference(resolve,[status(thm)],[c_107,c_104]) ).
cnf(c_130,plain,
( v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
| ~ l3_lattices(A) ),
inference(resolve,[status(thm)],[c_107,c_105]) ).
cnf(c_131,plain,
( v1_funct_1(u1_lattices(A))
| ~ l3_lattices(A) ),
inference(resolve,[status(thm)],[c_107,c_106]) ).
cnf(c_139,negated_conjecture,
( v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| v1_relat_1(u2_lattices(sK0))
| ~ l2_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_92,c_82]) ).
cnf(c_140,negated_conjecture,
( ~ l3_lattices(sK0)
| v1_relat_1(u2_lattices(sK0))
| ~ l2_lattices(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_139]) ).
cnf(c_141,negated_conjecture,
( v3_struct_0(sK0)
| ~ l3_lattices(sK0)
| v1_binop_1(u2_lattices(sK0),u1_struct_0(sK0))
| ~ l2_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_89,c_82]) ).
cnf(c_142,negated_conjecture,
( ~ l3_lattices(sK0)
| v1_binop_1(u2_lattices(sK0),u1_struct_0(sK0))
| ~ l2_lattices(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_141]) ).
cnf(c_160,plain,
( l2_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_162,plain,
( v1_funct_1(u2_lattices(A))
| ~ l2_lattices(A) ),
inference(clausify,[status(thm)],[dt_u2_lattices]) ).
cnf(c_163,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_164,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_172,plain,
( v1_funct_1(k1_realset1(A,B))
| ~ v1_funct_1(A)
| ~ v1_relat_1(A) ),
inference(clausify,[status(thm)],[fc2_realset1]) ).
cnf(c_174,plain,
( v2_binop_1(u2_lattices(A),u1_struct_0(A))
| ~ l2_lattices(A)
| ~ v5_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc3_lattice2]) ).
cnf(c_191,plain,
( v1_binop_1(D,B)
| ~ v1_binop_1(C,A)
| k1_realset1(C,B) != D
| ~ m2_relset_1(D,k2_zfmisc_1(B,B),B)
| ~ v1_funct_2(D,k2_zfmisc_1(B,B),B)
| ~ v1_funct_1(D)
| ~ m2_relset_1(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_1(C)
| ~ m1_subset_1(B,k1_zfmisc_1(A))
| v1_xboole_0(B)
| v1_xboole_0(A) ),
inference(clausify,[status(thm)],[t1_filter_2]) ).
cnf(c_193,plain,
( v2_binop_1(D,B)
| ~ v2_binop_1(C,A)
| k1_realset1(C,B) != D
| ~ m2_relset_1(D,k2_zfmisc_1(B,B),B)
| ~ v1_funct_2(D,k2_zfmisc_1(B,B),B)
| ~ v1_funct_1(D)
| ~ m2_relset_1(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_1(C)
| ~ m1_subset_1(B,k1_zfmisc_1(A))
| v1_xboole_0(B)
| v1_xboole_0(A) ),
inference(clausify,[status(thm)],[t1_filter_2]) ).
cnf(c_197,plain,
( r1_lattice2(B,E,F)
| ~ r1_lattice2(A,C,D)
| k1_realset1(D,B) != F
| k1_realset1(C,B) != E
| ~ m2_relset_1(F,k2_zfmisc_1(B,B),B)
| ~ v1_funct_2(F,k2_zfmisc_1(B,B),B)
| ~ v1_funct_1(F)
| ~ m2_relset_1(E,k2_zfmisc_1(B,B),B)
| ~ v1_funct_2(E,k2_zfmisc_1(B,B),B)
| ~ v1_funct_1(E)
| ~ m2_relset_1(D,k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(D,k2_zfmisc_1(A,A),A)
| ~ v1_funct_1(D)
| ~ m2_relset_1(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_1(C)
| ~ m1_subset_1(B,k1_zfmisc_1(A))
| v1_xboole_0(B)
| v1_xboole_0(A) ),
inference(clausify,[status(thm)],[t5_filter_2]) ).
cnf(c_202,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t62_filter_2_neg]) ).
cnf(c_203,negated_conjecture,
l3_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t62_filter_2_neg]) ).
cnf(c_204,negated_conjecture,
~ v1_xboole_0(sK1),
inference(split_conjunct,[status(thm)],[sk_t62_filter_2_neg]) ).
cnf(c_205,negated_conjecture,
m2_lattice4(sK1,sK0),
inference(split_conjunct,[status(thm)],[sk_t62_filter_2_neg]) ).
cnf(c_207,negated_conjecture,
v1_funct_2(sK2,k2_zfmisc_1(sK1,sK1),sK1),
inference(split_conjunct,[status(thm)],[sk_t62_filter_2_neg]) ).
cnf(c_208,negated_conjecture,
m2_relset_1(sK2,k2_zfmisc_1(sK1,sK1),sK1),
inference(split_conjunct,[status(thm)],[sk_t62_filter_2_neg]) ).
cnf(c_210,negated_conjecture,
v1_funct_2(sK3,k2_zfmisc_1(sK1,sK1),sK1),
inference(split_conjunct,[status(thm)],[sk_t62_filter_2_neg]) ).
cnf(c_211,negated_conjecture,
m2_relset_1(sK3,k2_zfmisc_1(sK1,sK1),sK1),
inference(split_conjunct,[status(thm)],[sk_t62_filter_2_neg]) ).
cnf(c_212,negated_conjecture,
k1_realset1(u2_lattices(sK0),sK1) = sK2,
inference(split_conjunct,[status(thm)],[sk_t62_filter_2_neg]) ).
cnf(c_213,negated_conjecture,
sK2 = k1_realset1(u2_lattices(sK0),sK1),
inference(copy,[status(thm)],[c_212]) ).
cnf(c_214,negated_conjecture,
k1_realset1(u1_lattices(sK0),sK1) = sK3,
inference(split_conjunct,[status(thm)],[sk_t62_filter_2_neg]) ).
cnf(c_215,negated_conjecture,
sK3 = k1_realset1(u1_lattices(sK0),sK1),
inference(copy,[status(thm)],[c_214]) ).
cnf(c_216,negated_conjecture,
( ~ r1_lattice2(sK1,sK3,sK2)
| ~ r1_lattice2(sK1,sK2,sK3)
| ~ v2_binop_1(sK3,sK1)
| ~ v1_binop_1(sK3,sK1)
| ~ v2_binop_1(sK2,sK1)
| ~ v1_binop_1(sK2,sK1) ),
inference(split_conjunct,[status(thm)],[sk_t62_filter_2_neg]) ).
cnf(c_873,negated_conjecture,
( ~ r1_lattice2(sK1,sK3,sK2)
| ~ r1_lattice2(sK1,sK2,sK3)
| ~ v2_binop_1(sK3,sK1)
| ~ v1_binop_1(sK3,sK1)
| ~ v2_binop_1(sK2,sK1)
| ~ v1_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1) ),
inference(paramod,[status(thm)],[c_213,c_216]) ).
cnf(c_874,negated_conjecture,
( ~ r1_lattice2(sK1,sK3,sK2)
| ~ r1_lattice2(sK1,sK2,sK3)
| ~ v2_binop_1(sK3,sK1)
| ~ v1_binop_1(sK3,sK1)
| ~ v2_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1)
| ~ v1_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1) ),
inference(paramod,[status(thm)],[c_213,c_873]) ).
cnf(c_875,negated_conjecture,
( ~ r1_lattice2(sK1,sK3,sK2)
| ~ r1_lattice2(sK1,sK2,sK3)
| ~ v2_binop_1(sK3,sK1)
| ~ v1_binop_1(k1_realset1(u1_lattices(sK0),sK1),sK1)
| ~ v2_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1)
| ~ v1_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1) ),
inference(paramod,[status(thm)],[c_215,c_874]) ).
cnf(c_876,negated_conjecture,
( ~ r1_lattice2(sK1,sK3,sK2)
| ~ r1_lattice2(sK1,sK2,sK3)
| ~ v2_binop_1(k1_realset1(u1_lattices(sK0),sK1),sK1)
| ~ v1_binop_1(k1_realset1(u1_lattices(sK0),sK1),sK1)
| ~ v2_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1)
| ~ v1_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1) ),
inference(paramod,[status(thm)],[c_215,c_875]) ).
cnf(c_877,negated_conjecture,
( ~ r1_lattice2(sK1,sK3,sK2)
| ~ r1_lattice2(sK1,k1_realset1(u2_lattices(sK0),sK1),sK3)
| ~ v2_binop_1(k1_realset1(u1_lattices(sK0),sK1),sK1)
| ~ v1_binop_1(k1_realset1(u1_lattices(sK0),sK1),sK1)
| ~ v2_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1)
| ~ v1_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1) ),
inference(paramod,[status(thm)],[c_213,c_876]) ).
cnf(c_878,negated_conjecture,
( ~ r1_lattice2(sK1,sK3,sK2)
| ~ r1_lattice2(sK1,k1_realset1(u2_lattices(sK0),sK1),k1_realset1(u1_lattices(sK0),sK1))
| ~ v2_binop_1(k1_realset1(u1_lattices(sK0),sK1),sK1)
| ~ v1_binop_1(k1_realset1(u1_lattices(sK0),sK1),sK1)
| ~ v2_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1)
| ~ v1_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1) ),
inference(paramod,[status(thm)],[c_215,c_877]) ).
cnf(c_879,negated_conjecture,
( ~ r1_lattice2(sK1,k1_realset1(u1_lattices(sK0),sK1),sK2)
| ~ r1_lattice2(sK1,k1_realset1(u2_lattices(sK0),sK1),k1_realset1(u1_lattices(sK0),sK1))
| ~ v2_binop_1(k1_realset1(u1_lattices(sK0),sK1),sK1)
| ~ v1_binop_1(k1_realset1(u1_lattices(sK0),sK1),sK1)
| ~ v2_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1)
| ~ v1_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1) ),
inference(paramod,[status(thm)],[c_215,c_878]) ).
cnf(c_217,negated_conjecture,
( ~ r1_lattice2(sK1,k1_realset1(u1_lattices(sK0),sK1),k1_realset1(u2_lattices(sK0),sK1))
| ~ r1_lattice2(sK1,k1_realset1(u2_lattices(sK0),sK1),k1_realset1(u1_lattices(sK0),sK1))
| ~ v2_binop_1(k1_realset1(u1_lattices(sK0),sK1),sK1)
| ~ v1_binop_1(k1_realset1(u1_lattices(sK0),sK1),sK1)
| ~ v2_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1)
| ~ v1_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1) ),
inference(paramod,[status(thm)],[c_213,c_879]) ).
cnf(c_218,negated_conjecture,
( r1_lattice2(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_80,c_79]) ).
cnf(c_880,negated_conjecture,
( r1_lattice2(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_202,c_218]) ).
cnf(c_219,negated_conjecture,
r1_lattice2(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0)),
inference(resolve,[status(thm)],[c_203,c_880]) ).
cnf(c_220,negated_conjecture,
( r1_lattice2(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_80,c_78]) ).
cnf(c_881,negated_conjecture,
( r1_lattice2(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_202,c_220]) ).
cnf(c_221,negated_conjecture,
r1_lattice2(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0)),
inference(resolve,[status(thm)],[c_203,c_881]) ).
cnf(c_228,negated_conjecture,
( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m2_lattice4(A,sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_80,c_74]) ).
cnf(c_882,negated_conjecture,
( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m2_lattice4(A,sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_202,c_228]) ).
cnf(c_229,negated_conjecture,
( m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m2_lattice4(A,sK0) ),
inference(resolve,[status(thm)],[c_203,c_882]) ).
cnf(c_234,negated_conjecture,
( v7_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_80,c_70]) ).
cnf(c_883,negated_conjecture,
( v7_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_203,c_234]) ).
cnf(c_235,negated_conjecture,
v7_lattices(sK0),
inference(resolve,[status(thm)],[c_202,c_883]) ).
cnf(c_236,negated_conjecture,
( v6_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_80,c_71]) ).
cnf(c_884,negated_conjecture,
( v6_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_203,c_236]) ).
cnf(c_237,negated_conjecture,
v6_lattices(sK0),
inference(resolve,[status(thm)],[c_202,c_884]) ).
cnf(c_238,negated_conjecture,
( v5_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_80,c_72]) ).
cnf(c_885,negated_conjecture,
( v5_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_203,c_238]) ).
cnf(c_239,negated_conjecture,
v5_lattices(sK0),
inference(resolve,[status(thm)],[c_202,c_885]) ).
cnf(c_241,plain,
( ~ l2_lattices(A)
| ~ v1_xboole_0(u1_struct_0(A))
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_109,c_111]) ).
cnf(c_886,negated_conjecture,
( ~ l3_lattices(sK0)
| v1_binop_1(u2_lattices(sK0),u1_struct_0(sK0))
| ~ l2_lattices(sK0) ),
inference(resolve,[status(thm)],[c_202,c_142]) ).
cnf(c_278,negated_conjecture,
( v1_binop_1(u2_lattices(sK0),u1_struct_0(sK0))
| ~ l2_lattices(sK0) ),
inference(resolve,[status(thm)],[c_203,c_886]) ).
cnf(c_887,negated_conjecture,
( ~ l3_lattices(sK0)
| v1_relat_1(u2_lattices(sK0))
| ~ l2_lattices(sK0) ),
inference(resolve,[status(thm)],[c_202,c_140]) ).
cnf(c_279,negated_conjecture,
( v1_relat_1(u2_lattices(sK0))
| ~ l2_lattices(sK0) ),
inference(resolve,[status(thm)],[c_203,c_887]) ).
cnf(c_280,negated_conjecture,
m2_relset_1(k1_realset1(u2_lattices(sK0),sK1),k2_zfmisc_1(sK1,sK1),sK1),
inference(paramod,[status(thm)],[c_213,c_208]) ).
cnf(c_281,negated_conjecture,
v1_funct_2(k1_realset1(u2_lattices(sK0),sK1),k2_zfmisc_1(sK1,sK1),sK1),
inference(paramod,[status(thm)],[c_213,c_207]) ).
cnf(c_283,negated_conjecture,
m2_relset_1(k1_realset1(u1_lattices(sK0),sK1),k2_zfmisc_1(sK1,sK1),sK1),
inference(paramod,[status(thm)],[c_215,c_211]) ).
cnf(c_284,negated_conjecture,
v1_funct_2(k1_realset1(u1_lattices(sK0),sK1),k2_zfmisc_1(sK1,sK1),sK1),
inference(paramod,[status(thm)],[c_215,c_210]) ).
cnf(c_360,plain,
l2_lattices(sK0),
inference(resolve,[status(thm)],[c_203,c_160]) ).
cnf(c_361,plain,
v1_funct_1(u1_lattices(sK0)),
inference(resolve,[status(thm)],[c_203,c_131]) ).
cnf(c_362,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_203,c_130]) ).
cnf(c_363,plain,
m2_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_203,c_129]) ).
cnf(c_364,negated_conjecture,
v1_relat_1(u2_lattices(sK0)),
inference(resolve,[status(thm)],[c_360,c_279]) ).
cnf(c_365,negated_conjecture,
v1_binop_1(u2_lattices(sK0),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_360,c_278]) ).
cnf(c_384,plain,
m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(sK0))),
inference(resolve,[status(thm)],[c_229,c_205]) ).
cnf(c_888,negated_conjecture,
( v1_relat_1(u1_lattices(sK0))
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_235,c_126]) ).
cnf(c_889,negated_conjecture,
( v1_relat_1(u1_lattices(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_203,c_888]) ).
cnf(c_385,negated_conjecture,
v1_relat_1(u1_lattices(sK0)),
inference(resolve,[status(thm)],[c_202,c_889]) ).
cnf(c_890,negated_conjecture,
( v2_binop_1(u1_lattices(sK0),u1_struct_0(sK0))
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_235,c_125]) ).
cnf(c_891,negated_conjecture,
( v2_binop_1(u1_lattices(sK0),u1_struct_0(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_203,c_890]) ).
cnf(c_386,negated_conjecture,
v2_binop_1(u1_lattices(sK0),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_202,c_891]) ).
cnf(c_892,negated_conjecture,
( v1_binop_1(u1_lattices(sK0),u1_struct_0(sK0))
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_237,c_127]) ).
cnf(c_893,negated_conjecture,
( v1_binop_1(u1_lattices(sK0),u1_struct_0(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_203,c_892]) ).
cnf(c_387,negated_conjecture,
v1_binop_1(u1_lattices(sK0),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_202,c_893]) ).
cnf(c_894,negated_conjecture,
( v2_binop_1(u2_lattices(sK0),u1_struct_0(sK0))
| ~ l2_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_239,c_174]) ).
cnf(c_895,negated_conjecture,
( v2_binop_1(u2_lattices(sK0),u1_struct_0(sK0))
| ~ l2_lattices(sK0) ),
inference(resolve,[status(thm)],[c_202,c_894]) ).
cnf(c_388,negated_conjecture,
v2_binop_1(u2_lattices(sK0),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_360,c_895]) ).
cnf(c_896,plain,
( ~ v1_xboole_0(u1_struct_0(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_360,c_241]) ).
cnf(c_466,negated_conjecture,
~ v1_xboole_0(u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_202,c_896]) ).
cnf(c_467,plain,
m2_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_360,c_164]) ).
cnf(c_468,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_360,c_163]) ).
cnf(c_469,plain,
v1_funct_1(u2_lattices(sK0)),
inference(resolve,[status(thm)],[c_360,c_162]) ).
cnf(c_897,negated_conjecture,
( v1_funct_1(k1_realset1(u2_lattices(sK0),A))
| ~ v1_funct_1(u2_lattices(sK0)) ),
inference(resolve,[status(thm)],[c_364,c_172]) ).
cnf(c_503,negated_conjecture,
v1_funct_1(k1_realset1(u2_lattices(sK0),A)),
inference(resolve,[status(thm)],[c_469,c_897]) ).
cnf(c_898,plain,
( v1_funct_1(k1_realset1(u1_lattices(sK0),A))
| ~ v1_funct_1(u1_lattices(sK0)) ),
inference(resolve,[status(thm)],[c_385,c_172]) ).
cnf(c_508,plain,
v1_funct_1(k1_realset1(u1_lattices(sK0),A)),
inference(resolve,[status(thm)],[c_361,c_898]) ).
cnf(c_899,plain,
( v2_binop_1(B,sK1)
| ~ v2_binop_1(A,u1_struct_0(sK0))
| k1_realset1(A,sK1) != B
| ~ m2_relset_1(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(B)
| ~ m2_relset_1(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_193,c_384]) ).
cnf(c_900,plain,
( v2_binop_1(A,sK1)
| ~ v2_binop_1(u1_lattices(sK0),u1_struct_0(sK0))
| k1_realset1(u1_lattices(sK0),sK1) != A
| ~ m2_relset_1(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(A)
| ~ m2_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_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_899,c_361]) ).
cnf(c_901,plain,
( v2_binop_1(A,sK1)
| ~ v2_binop_1(u1_lattices(sK0),u1_struct_0(sK0))
| k1_realset1(u1_lattices(sK0),sK1) != A
| ~ m2_relset_1(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(A)
| ~ m2_relset_1(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_900,c_362]) ).
cnf(c_902,plain,
( v2_binop_1(A,sK1)
| ~ v2_binop_1(u1_lattices(sK0),u1_struct_0(sK0))
| k1_realset1(u1_lattices(sK0),sK1) != A
| ~ m2_relset_1(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(A)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_901,c_363]) ).
cnf(c_903,plain,
( v2_binop_1(k1_realset1(u1_lattices(sK0),A),sK1)
| ~ v2_binop_1(u1_lattices(sK0),u1_struct_0(sK0))
| k1_realset1(u1_lattices(sK0),sK1) != k1_realset1(u1_lattices(sK0),A)
| ~ m2_relset_1(k1_realset1(u1_lattices(sK0),A),k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(k1_realset1(u1_lattices(sK0),A),k2_zfmisc_1(sK1,sK1),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_902,c_508]) ).
cnf(c_904,negated_conjecture,
( v2_binop_1(k1_realset1(u1_lattices(sK0),sK1),sK1)
| ~ v2_binop_1(u1_lattices(sK0),u1_struct_0(sK0))
| k1_realset1(u1_lattices(sK0),sK1) != k1_realset1(u1_lattices(sK0),sK1)
| ~ m2_relset_1(k1_realset1(u1_lattices(sK0),sK1),k2_zfmisc_1(sK1,sK1),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_903,c_284]) ).
cnf(c_905,negated_conjecture,
( v2_binop_1(k1_realset1(u1_lattices(sK0),sK1),sK1)
| ~ v2_binop_1(u1_lattices(sK0),u1_struct_0(sK0))
| k1_realset1(u1_lattices(sK0),sK1) != k1_realset1(u1_lattices(sK0),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_904,c_283]) ).
cnf(c_906,plain,
( v2_binop_1(k1_realset1(u1_lattices(sK0),sK1),sK1)
| ~ v2_binop_1(u1_lattices(sK0),u1_struct_0(sK0))
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(xxres,[status(thm)],[c_905]) ).
cnf(c_907,plain,
( v2_binop_1(k1_realset1(u1_lattices(sK0),sK1),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_906,c_386]) ).
cnf(c_908,plain,
( v2_binop_1(k1_realset1(u1_lattices(sK0),sK1),sK1)
| v1_xboole_0(sK1) ),
inference(resolve,[status(thm)],[c_466,c_907]) ).
cnf(c_811,negated_conjecture,
v2_binop_1(k1_realset1(u1_lattices(sK0),sK1),sK1),
inference(resolve,[status(thm)],[c_204,c_908]) ).
cnf(c_909,plain,
( v1_binop_1(B,sK1)
| ~ v1_binop_1(A,u1_struct_0(sK0))
| k1_realset1(A,sK1) != B
| ~ m2_relset_1(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(B)
| ~ m2_relset_1(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_191,c_384]) ).
cnf(c_910,plain,
( v1_binop_1(A,sK1)
| ~ v1_binop_1(u1_lattices(sK0),u1_struct_0(sK0))
| k1_realset1(u1_lattices(sK0),sK1) != A
| ~ m2_relset_1(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(A)
| ~ m2_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_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_909,c_361]) ).
cnf(c_911,plain,
( v1_binop_1(A,sK1)
| ~ v1_binop_1(u1_lattices(sK0),u1_struct_0(sK0))
| k1_realset1(u1_lattices(sK0),sK1) != A
| ~ m2_relset_1(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(A)
| ~ m2_relset_1(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_910,c_362]) ).
cnf(c_912,plain,
( v1_binop_1(A,sK1)
| ~ v1_binop_1(u1_lattices(sK0),u1_struct_0(sK0))
| k1_realset1(u1_lattices(sK0),sK1) != A
| ~ m2_relset_1(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(A)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_911,c_363]) ).
cnf(c_913,plain,
( v1_binop_1(k1_realset1(u1_lattices(sK0),A),sK1)
| ~ v1_binop_1(u1_lattices(sK0),u1_struct_0(sK0))
| k1_realset1(u1_lattices(sK0),sK1) != k1_realset1(u1_lattices(sK0),A)
| ~ m2_relset_1(k1_realset1(u1_lattices(sK0),A),k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(k1_realset1(u1_lattices(sK0),A),k2_zfmisc_1(sK1,sK1),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_912,c_508]) ).
cnf(c_914,negated_conjecture,
( v1_binop_1(k1_realset1(u1_lattices(sK0),sK1),sK1)
| ~ v1_binop_1(u1_lattices(sK0),u1_struct_0(sK0))
| k1_realset1(u1_lattices(sK0),sK1) != k1_realset1(u1_lattices(sK0),sK1)
| ~ m2_relset_1(k1_realset1(u1_lattices(sK0),sK1),k2_zfmisc_1(sK1,sK1),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_913,c_284]) ).
cnf(c_915,negated_conjecture,
( v1_binop_1(k1_realset1(u1_lattices(sK0),sK1),sK1)
| ~ v1_binop_1(u1_lattices(sK0),u1_struct_0(sK0))
| k1_realset1(u1_lattices(sK0),sK1) != k1_realset1(u1_lattices(sK0),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_914,c_283]) ).
cnf(c_916,plain,
( v1_binop_1(k1_realset1(u1_lattices(sK0),sK1),sK1)
| ~ v1_binop_1(u1_lattices(sK0),u1_struct_0(sK0))
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(xxres,[status(thm)],[c_915]) ).
cnf(c_917,plain,
( v1_binop_1(k1_realset1(u1_lattices(sK0),sK1),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_916,c_387]) ).
cnf(c_918,plain,
( v1_binop_1(k1_realset1(u1_lattices(sK0),sK1),sK1)
| v1_xboole_0(sK1) ),
inference(resolve,[status(thm)],[c_466,c_917]) ).
cnf(c_812,negated_conjecture,
v1_binop_1(k1_realset1(u1_lattices(sK0),sK1),sK1),
inference(resolve,[status(thm)],[c_204,c_918]) ).
cnf(c_919,negated_conjecture,
( ~ r1_lattice2(sK1,k1_realset1(u1_lattices(sK0),sK1),k1_realset1(u2_lattices(sK0),sK1))
| ~ r1_lattice2(sK1,k1_realset1(u2_lattices(sK0),sK1),k1_realset1(u1_lattices(sK0),sK1))
| ~ v2_binop_1(k1_realset1(u1_lattices(sK0),sK1),sK1)
| ~ v2_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1)
| ~ v1_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1) ),
inference(resolve,[status(thm)],[c_812,c_217]) ).
cnf(c_816,negated_conjecture,
( ~ r1_lattice2(sK1,k1_realset1(u1_lattices(sK0),sK1),k1_realset1(u2_lattices(sK0),sK1))
| ~ r1_lattice2(sK1,k1_realset1(u2_lattices(sK0),sK1),k1_realset1(u1_lattices(sK0),sK1))
| ~ v2_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1)
| ~ v1_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1) ),
inference(resolve,[status(thm)],[c_811,c_919]) ).
cnf(c_920,plain,
( r1_lattice2(sK1,C,D)
| ~ r1_lattice2(u1_struct_0(sK0),A,B)
| k1_realset1(B,sK1) != D
| k1_realset1(A,sK1) != C
| ~ m2_relset_1(D,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(D,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(D)
| ~ m2_relset_1(C,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(C,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(C)
| ~ m2_relset_1(B,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(B,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(B)
| ~ m2_relset_1(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_197,c_384]) ).
cnf(c_921,plain,
( r1_lattice2(sK1,B,C)
| ~ r1_lattice2(u1_struct_0(sK0),u1_lattices(sK0),A)
| k1_realset1(A,sK1) != C
| k1_realset1(u1_lattices(sK0),sK1) != B
| ~ m2_relset_1(C,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(C,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(C)
| ~ m2_relset_1(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(B)
| ~ m2_relset_1(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ m2_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_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_920,c_361]) ).
cnf(c_922,plain,
( r1_lattice2(sK1,B,C)
| ~ r1_lattice2(u1_struct_0(sK0),u1_lattices(sK0),A)
| k1_realset1(A,sK1) != C
| k1_realset1(u1_lattices(sK0),sK1) != B
| ~ m2_relset_1(C,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(C,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(C)
| ~ m2_relset_1(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(B)
| ~ m2_relset_1(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ m2_relset_1(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_921,c_362]) ).
cnf(c_923,plain,
( r1_lattice2(sK1,B,C)
| ~ r1_lattice2(u1_struct_0(sK0),u1_lattices(sK0),A)
| k1_realset1(A,sK1) != C
| k1_realset1(u1_lattices(sK0),sK1) != B
| ~ m2_relset_1(C,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(C,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(C)
| ~ m2_relset_1(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(B)
| ~ m2_relset_1(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_922,c_363]) ).
cnf(c_924,plain,
( r1_lattice2(sK1,A,B)
| ~ r1_lattice2(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0))
| k1_realset1(u2_lattices(sK0),sK1) != B
| k1_realset1(u1_lattices(sK0),sK1) != A
| ~ m2_relset_1(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(B)
| ~ m2_relset_1(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(A)
| ~ m2_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_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_923,c_469]) ).
cnf(c_925,plain,
( r1_lattice2(sK1,A,B)
| ~ r1_lattice2(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0))
| k1_realset1(u2_lattices(sK0),sK1) != B
| k1_realset1(u1_lattices(sK0),sK1) != A
| ~ m2_relset_1(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(B)
| ~ m2_relset_1(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(A)
| ~ m2_relset_1(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_924,c_468]) ).
cnf(c_926,plain,
( r1_lattice2(sK1,A,B)
| ~ r1_lattice2(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0))
| k1_realset1(u2_lattices(sK0),sK1) != B
| k1_realset1(u1_lattices(sK0),sK1) != A
| ~ m2_relset_1(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(B)
| ~ m2_relset_1(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(A)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_925,c_467]) ).
cnf(c_927,plain,
( r1_lattice2(sK1,k1_realset1(u1_lattices(sK0),A),B)
| ~ r1_lattice2(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0))
| k1_realset1(u2_lattices(sK0),sK1) != B
| k1_realset1(u1_lattices(sK0),sK1) != k1_realset1(u1_lattices(sK0),A)
| ~ m2_relset_1(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(B)
| ~ m2_relset_1(k1_realset1(u1_lattices(sK0),A),k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(k1_realset1(u1_lattices(sK0),A),k2_zfmisc_1(sK1,sK1),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_926,c_508]) ).
cnf(c_928,negated_conjecture,
( r1_lattice2(sK1,k1_realset1(u1_lattices(sK0),sK1),A)
| ~ r1_lattice2(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0))
| k1_realset1(u2_lattices(sK0),sK1) != A
| k1_realset1(u1_lattices(sK0),sK1) != k1_realset1(u1_lattices(sK0),sK1)
| ~ m2_relset_1(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(A)
| ~ m2_relset_1(k1_realset1(u1_lattices(sK0),sK1),k2_zfmisc_1(sK1,sK1),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_927,c_284]) ).
cnf(c_929,negated_conjecture,
( r1_lattice2(sK1,k1_realset1(u1_lattices(sK0),sK1),A)
| ~ r1_lattice2(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0))
| k1_realset1(u2_lattices(sK0),sK1) != A
| k1_realset1(u1_lattices(sK0),sK1) != k1_realset1(u1_lattices(sK0),sK1)
| ~ m2_relset_1(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(A)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_928,c_283]) ).
cnf(c_930,negated_conjecture,
( r1_lattice2(sK1,k1_realset1(u1_lattices(sK0),sK1),k1_realset1(u2_lattices(sK0),A))
| ~ r1_lattice2(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0))
| k1_realset1(u2_lattices(sK0),sK1) != k1_realset1(u2_lattices(sK0),A)
| k1_realset1(u1_lattices(sK0),sK1) != k1_realset1(u1_lattices(sK0),sK1)
| ~ m2_relset_1(k1_realset1(u2_lattices(sK0),A),k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(k1_realset1(u2_lattices(sK0),A),k2_zfmisc_1(sK1,sK1),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_929,c_503]) ).
cnf(c_931,negated_conjecture,
( r1_lattice2(sK1,k1_realset1(u1_lattices(sK0),sK1),k1_realset1(u2_lattices(sK0),sK1))
| ~ r1_lattice2(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0))
| k1_realset1(u2_lattices(sK0),sK1) != k1_realset1(u2_lattices(sK0),sK1)
| k1_realset1(u1_lattices(sK0),sK1) != k1_realset1(u1_lattices(sK0),sK1)
| ~ m2_relset_1(k1_realset1(u2_lattices(sK0),sK1),k2_zfmisc_1(sK1,sK1),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_930,c_281]) ).
cnf(c_932,negated_conjecture,
( r1_lattice2(sK1,k1_realset1(u1_lattices(sK0),sK1),k1_realset1(u2_lattices(sK0),sK1))
| ~ r1_lattice2(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0))
| k1_realset1(u2_lattices(sK0),sK1) != k1_realset1(u2_lattices(sK0),sK1)
| k1_realset1(u1_lattices(sK0),sK1) != k1_realset1(u1_lattices(sK0),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_931,c_280]) ).
cnf(c_933,plain,
( r1_lattice2(sK1,k1_realset1(u1_lattices(sK0),sK1),k1_realset1(u2_lattices(sK0),sK1))
| ~ r1_lattice2(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0))
| k1_realset1(u2_lattices(sK0),sK1) != k1_realset1(u2_lattices(sK0),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(xxres,[status(thm)],[c_932]) ).
cnf(c_934,plain,
( r1_lattice2(sK1,k1_realset1(u1_lattices(sK0),sK1),k1_realset1(u2_lattices(sK0),sK1))
| ~ r1_lattice2(u1_struct_0(sK0),u1_lattices(sK0),u2_lattices(sK0))
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(xxres,[status(thm)],[c_933]) ).
cnf(c_935,negated_conjecture,
( r1_lattice2(sK1,k1_realset1(u1_lattices(sK0),sK1),k1_realset1(u2_lattices(sK0),sK1))
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_934,c_219]) ).
cnf(c_936,negated_conjecture,
( r1_lattice2(sK1,k1_realset1(u1_lattices(sK0),sK1),k1_realset1(u2_lattices(sK0),sK1))
| v1_xboole_0(sK1) ),
inference(resolve,[status(thm)],[c_466,c_935]) ).
cnf(c_868,negated_conjecture,
r1_lattice2(sK1,k1_realset1(u1_lattices(sK0),sK1),k1_realset1(u2_lattices(sK0),sK1)),
inference(resolve,[status(thm)],[c_204,c_936]) ).
cnf(c_937,plain,
( r1_lattice2(sK1,C,D)
| ~ r1_lattice2(u1_struct_0(sK0),A,B)
| k1_realset1(B,sK1) != D
| k1_realset1(A,sK1) != C
| ~ m2_relset_1(D,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(D,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(D)
| ~ m2_relset_1(C,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(C,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(C)
| ~ m2_relset_1(B,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(B,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(B)
| ~ m2_relset_1(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_197,c_384]) ).
cnf(c_938,plain,
( r1_lattice2(sK1,B,C)
| ~ r1_lattice2(u1_struct_0(sK0),u2_lattices(sK0),A)
| k1_realset1(A,sK1) != C
| k1_realset1(u2_lattices(sK0),sK1) != B
| ~ m2_relset_1(C,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(C,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(C)
| ~ m2_relset_1(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(B)
| ~ m2_relset_1(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ m2_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_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_937,c_469]) ).
cnf(c_939,plain,
( r1_lattice2(sK1,B,C)
| ~ r1_lattice2(u1_struct_0(sK0),u2_lattices(sK0),A)
| k1_realset1(A,sK1) != C
| k1_realset1(u2_lattices(sK0),sK1) != B
| ~ m2_relset_1(C,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(C,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(C)
| ~ m2_relset_1(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(B)
| ~ m2_relset_1(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| ~ m2_relset_1(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_938,c_468]) ).
cnf(c_940,plain,
( r1_lattice2(sK1,B,C)
| ~ r1_lattice2(u1_struct_0(sK0),u2_lattices(sK0),A)
| k1_realset1(A,sK1) != C
| k1_realset1(u2_lattices(sK0),sK1) != B
| ~ m2_relset_1(C,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(C,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(C)
| ~ m2_relset_1(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(B)
| ~ m2_relset_1(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_939,c_467]) ).
cnf(c_941,plain,
( r1_lattice2(sK1,A,B)
| ~ r1_lattice2(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| k1_realset1(u1_lattices(sK0),sK1) != B
| k1_realset1(u2_lattices(sK0),sK1) != A
| ~ m2_relset_1(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(B)
| ~ m2_relset_1(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(A)
| ~ m2_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_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_940,c_361]) ).
cnf(c_942,plain,
( r1_lattice2(sK1,A,B)
| ~ r1_lattice2(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| k1_realset1(u1_lattices(sK0),sK1) != B
| k1_realset1(u2_lattices(sK0),sK1) != A
| ~ m2_relset_1(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(B)
| ~ m2_relset_1(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(A)
| ~ m2_relset_1(u1_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_941,c_362]) ).
cnf(c_943,plain,
( r1_lattice2(sK1,A,B)
| ~ r1_lattice2(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| k1_realset1(u1_lattices(sK0),sK1) != B
| k1_realset1(u2_lattices(sK0),sK1) != A
| ~ m2_relset_1(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(B)
| ~ m2_relset_1(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(A)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_942,c_363]) ).
cnf(c_944,plain,
( r1_lattice2(sK1,k1_realset1(u2_lattices(sK0),A),B)
| ~ r1_lattice2(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| k1_realset1(u1_lattices(sK0),sK1) != B
| k1_realset1(u2_lattices(sK0),sK1) != k1_realset1(u2_lattices(sK0),A)
| ~ m2_relset_1(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(B)
| ~ m2_relset_1(k1_realset1(u2_lattices(sK0),A),k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(k1_realset1(u2_lattices(sK0),A),k2_zfmisc_1(sK1,sK1),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_943,c_503]) ).
cnf(c_945,negated_conjecture,
( r1_lattice2(sK1,k1_realset1(u2_lattices(sK0),sK1),A)
| ~ r1_lattice2(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| k1_realset1(u1_lattices(sK0),sK1) != A
| k1_realset1(u2_lattices(sK0),sK1) != k1_realset1(u2_lattices(sK0),sK1)
| ~ m2_relset_1(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(A)
| ~ m2_relset_1(k1_realset1(u2_lattices(sK0),sK1),k2_zfmisc_1(sK1,sK1),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_944,c_281]) ).
cnf(c_946,negated_conjecture,
( r1_lattice2(sK1,k1_realset1(u2_lattices(sK0),sK1),A)
| ~ r1_lattice2(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| k1_realset1(u1_lattices(sK0),sK1) != A
| k1_realset1(u2_lattices(sK0),sK1) != k1_realset1(u2_lattices(sK0),sK1)
| ~ m2_relset_1(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(A)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_945,c_280]) ).
cnf(c_947,negated_conjecture,
( r1_lattice2(sK1,k1_realset1(u2_lattices(sK0),sK1),k1_realset1(u1_lattices(sK0),A))
| ~ r1_lattice2(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| k1_realset1(u1_lattices(sK0),sK1) != k1_realset1(u1_lattices(sK0),A)
| k1_realset1(u2_lattices(sK0),sK1) != k1_realset1(u2_lattices(sK0),sK1)
| ~ m2_relset_1(k1_realset1(u1_lattices(sK0),A),k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(k1_realset1(u1_lattices(sK0),A),k2_zfmisc_1(sK1,sK1),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_946,c_508]) ).
cnf(c_948,negated_conjecture,
( r1_lattice2(sK1,k1_realset1(u2_lattices(sK0),sK1),k1_realset1(u1_lattices(sK0),sK1))
| ~ r1_lattice2(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| k1_realset1(u1_lattices(sK0),sK1) != k1_realset1(u1_lattices(sK0),sK1)
| k1_realset1(u2_lattices(sK0),sK1) != k1_realset1(u2_lattices(sK0),sK1)
| ~ m2_relset_1(k1_realset1(u1_lattices(sK0),sK1),k2_zfmisc_1(sK1,sK1),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_947,c_284]) ).
cnf(c_949,negated_conjecture,
( r1_lattice2(sK1,k1_realset1(u2_lattices(sK0),sK1),k1_realset1(u1_lattices(sK0),sK1))
| ~ r1_lattice2(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| k1_realset1(u1_lattices(sK0),sK1) != k1_realset1(u1_lattices(sK0),sK1)
| k1_realset1(u2_lattices(sK0),sK1) != k1_realset1(u2_lattices(sK0),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_948,c_283]) ).
cnf(c_950,plain,
( r1_lattice2(sK1,k1_realset1(u2_lattices(sK0),sK1),k1_realset1(u1_lattices(sK0),sK1))
| ~ r1_lattice2(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| k1_realset1(u1_lattices(sK0),sK1) != k1_realset1(u1_lattices(sK0),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(xxres,[status(thm)],[c_949]) ).
cnf(c_951,plain,
( r1_lattice2(sK1,k1_realset1(u2_lattices(sK0),sK1),k1_realset1(u1_lattices(sK0),sK1))
| ~ r1_lattice2(u1_struct_0(sK0),u2_lattices(sK0),u1_lattices(sK0))
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(xxres,[status(thm)],[c_950]) ).
cnf(c_952,negated_conjecture,
( r1_lattice2(sK1,k1_realset1(u2_lattices(sK0),sK1),k1_realset1(u1_lattices(sK0),sK1))
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_951,c_221]) ).
cnf(c_953,negated_conjecture,
( r1_lattice2(sK1,k1_realset1(u2_lattices(sK0),sK1),k1_realset1(u1_lattices(sK0),sK1))
| v1_xboole_0(sK1) ),
inference(resolve,[status(thm)],[c_466,c_952]) ).
cnf(c_869,negated_conjecture,
r1_lattice2(sK1,k1_realset1(u2_lattices(sK0),sK1),k1_realset1(u1_lattices(sK0),sK1)),
inference(resolve,[status(thm)],[c_204,c_953]) ).
cnf(c_954,plain,
( v2_binop_1(B,sK1)
| ~ v2_binop_1(A,u1_struct_0(sK0))
| k1_realset1(A,sK1) != B
| ~ m2_relset_1(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(B)
| ~ m2_relset_1(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_193,c_384]) ).
cnf(c_955,plain,
( v2_binop_1(A,sK1)
| ~ v2_binop_1(u2_lattices(sK0),u1_struct_0(sK0))
| k1_realset1(u2_lattices(sK0),sK1) != A
| ~ m2_relset_1(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(A)
| ~ m2_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_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_954,c_469]) ).
cnf(c_956,plain,
( v2_binop_1(A,sK1)
| ~ v2_binop_1(u2_lattices(sK0),u1_struct_0(sK0))
| k1_realset1(u2_lattices(sK0),sK1) != A
| ~ m2_relset_1(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(A)
| ~ m2_relset_1(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_955,c_468]) ).
cnf(c_957,plain,
( v2_binop_1(A,sK1)
| ~ v2_binop_1(u2_lattices(sK0),u1_struct_0(sK0))
| k1_realset1(u2_lattices(sK0),sK1) != A
| ~ m2_relset_1(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(A)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_956,c_467]) ).
cnf(c_958,plain,
( v2_binop_1(k1_realset1(u2_lattices(sK0),A),sK1)
| ~ v2_binop_1(u2_lattices(sK0),u1_struct_0(sK0))
| k1_realset1(u2_lattices(sK0),sK1) != k1_realset1(u2_lattices(sK0),A)
| ~ m2_relset_1(k1_realset1(u2_lattices(sK0),A),k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(k1_realset1(u2_lattices(sK0),A),k2_zfmisc_1(sK1,sK1),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_957,c_503]) ).
cnf(c_959,negated_conjecture,
( v2_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1)
| ~ v2_binop_1(u2_lattices(sK0),u1_struct_0(sK0))
| k1_realset1(u2_lattices(sK0),sK1) != k1_realset1(u2_lattices(sK0),sK1)
| ~ m2_relset_1(k1_realset1(u2_lattices(sK0),sK1),k2_zfmisc_1(sK1,sK1),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_958,c_281]) ).
cnf(c_960,negated_conjecture,
( v2_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1)
| ~ v2_binop_1(u2_lattices(sK0),u1_struct_0(sK0))
| k1_realset1(u2_lattices(sK0),sK1) != k1_realset1(u2_lattices(sK0),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_959,c_280]) ).
cnf(c_961,plain,
( v2_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1)
| ~ v2_binop_1(u2_lattices(sK0),u1_struct_0(sK0))
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(xxres,[status(thm)],[c_960]) ).
cnf(c_962,plain,
( v2_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_961,c_388]) ).
cnf(c_963,plain,
( v2_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1)
| v1_xboole_0(sK1) ),
inference(resolve,[status(thm)],[c_466,c_962]) ).
cnf(c_870,negated_conjecture,
v2_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1),
inference(resolve,[status(thm)],[c_204,c_963]) ).
cnf(c_964,plain,
( v1_binop_1(B,sK1)
| ~ v1_binop_1(A,u1_struct_0(sK0))
| k1_realset1(A,sK1) != B
| ~ m2_relset_1(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(B,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(B)
| ~ m2_relset_1(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_2(A,k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| ~ v1_funct_1(A)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_191,c_384]) ).
cnf(c_965,plain,
( v1_binop_1(A,sK1)
| ~ v1_binop_1(u2_lattices(sK0),u1_struct_0(sK0))
| k1_realset1(u2_lattices(sK0),sK1) != A
| ~ m2_relset_1(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(A)
| ~ m2_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_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_964,c_469]) ).
cnf(c_966,plain,
( v1_binop_1(A,sK1)
| ~ v1_binop_1(u2_lattices(sK0),u1_struct_0(sK0))
| k1_realset1(u2_lattices(sK0),sK1) != A
| ~ m2_relset_1(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(A)
| ~ m2_relset_1(u2_lattices(sK0),k2_zfmisc_1(u1_struct_0(sK0),u1_struct_0(sK0)),u1_struct_0(sK0))
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_965,c_468]) ).
cnf(c_967,plain,
( v1_binop_1(A,sK1)
| ~ v1_binop_1(u2_lattices(sK0),u1_struct_0(sK0))
| k1_realset1(u2_lattices(sK0),sK1) != A
| ~ m2_relset_1(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(A,k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_1(A)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_966,c_467]) ).
cnf(c_968,plain,
( v1_binop_1(k1_realset1(u2_lattices(sK0),A),sK1)
| ~ v1_binop_1(u2_lattices(sK0),u1_struct_0(sK0))
| k1_realset1(u2_lattices(sK0),sK1) != k1_realset1(u2_lattices(sK0),A)
| ~ m2_relset_1(k1_realset1(u2_lattices(sK0),A),k2_zfmisc_1(sK1,sK1),sK1)
| ~ v1_funct_2(k1_realset1(u2_lattices(sK0),A),k2_zfmisc_1(sK1,sK1),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_967,c_503]) ).
cnf(c_969,negated_conjecture,
( v1_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1)
| ~ v1_binop_1(u2_lattices(sK0),u1_struct_0(sK0))
| k1_realset1(u2_lattices(sK0),sK1) != k1_realset1(u2_lattices(sK0),sK1)
| ~ m2_relset_1(k1_realset1(u2_lattices(sK0),sK1),k2_zfmisc_1(sK1,sK1),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_968,c_281]) ).
cnf(c_970,negated_conjecture,
( v1_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1)
| ~ v1_binop_1(u2_lattices(sK0),u1_struct_0(sK0))
| k1_realset1(u2_lattices(sK0),sK1) != k1_realset1(u2_lattices(sK0),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_969,c_280]) ).
cnf(c_971,plain,
( v1_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1)
| ~ v1_binop_1(u2_lattices(sK0),u1_struct_0(sK0))
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(xxres,[status(thm)],[c_970]) ).
cnf(c_972,negated_conjecture,
( v1_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1)
| v1_xboole_0(sK1)
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_971,c_365]) ).
cnf(c_973,negated_conjecture,
( v1_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1)
| v1_xboole_0(sK1) ),
inference(resolve,[status(thm)],[c_466,c_972]) ).
cnf(c_871,negated_conjecture,
v1_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1),
inference(resolve,[status(thm)],[c_204,c_973]) ).
cnf(c_974,negated_conjecture,
( ~ r1_lattice2(sK1,k1_realset1(u1_lattices(sK0),sK1),k1_realset1(u2_lattices(sK0),sK1))
| ~ r1_lattice2(sK1,k1_realset1(u2_lattices(sK0),sK1),k1_realset1(u1_lattices(sK0),sK1))
| ~ v2_binop_1(k1_realset1(u2_lattices(sK0),sK1),sK1) ),
inference(resolve,[status(thm)],[c_871,c_816]) ).
cnf(c_975,negated_conjecture,
( ~ r1_lattice2(sK1,k1_realset1(u1_lattices(sK0),sK1),k1_realset1(u2_lattices(sK0),sK1))
| ~ r1_lattice2(sK1,k1_realset1(u2_lattices(sK0),sK1),k1_realset1(u1_lattices(sK0),sK1)) ),
inference(resolve,[status(thm)],[c_870,c_974]) ).
cnf(c_976,negated_conjecture,
~ r1_lattice2(sK1,k1_realset1(u1_lattices(sK0),sK1),k1_realset1(u2_lattices(sK0),sK1)),
inference(resolve,[status(thm)],[c_869,c_975]) ).
cnf(c_872,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_868,c_976]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT326+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n018.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Fri Sep 25 20:56:07 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 2841124 was started by sandbox2 on n018,
% 0.09/0.37 % Fri Sep 25 20:56:07 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.39
% 0.09/0.39 % From the command line: assign(max_seconds, 300).
% 3.66/0.98
% 3.66/0.98 % SZS status Theorem for theBenchmark
% 3.66/0.98
% 3.66/0.98 % Proof 1 at 0.56 (+ 0.01) seconds.
% 3.66/0.98 % Length of proof is 114.
% 3.66/0.98 % Level of proof is 9.
% 3.66/0.98 % Maximum clause weight is 92.000.
% 3.66/0.98 % Given clauses 308.
% 3.66/0.98
% 3.66/0.98 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------