%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : LAT296+1 : TPTP v9.2.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:37:57 PM UTC 2026
% Result : Theorem 226.05s 80.69s
% Output : CNFRefutation 234.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 123
% Syntax : Number of formulae : 600 ( 290 unt; 0 def)
% Number of atoms : 2046 ( 152 equ)
% Maximal formula atoms : 45 ( 3 avg)
% Number of connectives : 2299 ( 853 ~; 835 |; 503 &)
% ( 4 <=>; 104 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 36 ( 34 usr; 1 prp; 0-3 aty)
% Number of functors : 35 ( 35 usr; 22 con; 0-3 aty)
% Number of variables : 719 ( 53 sgn 208 !; 33 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d21_lattices,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v11_lattices(X1)
& v16_lattices(X1)
& l3_lattices(X1) )
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ( X3 = k7_lattices(X1,X2)
<=> r2_lattices(X1,X3,X2) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d21_lattices) ).
fof(fc3_lattices,axiom,
! [X1,X2,X3] :
( ( ~ v1_xboole_0(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
& m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)
& v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
& m1_relset_1(X3,k2_zfmisc_1(X1,X1),X1) )
=> ( ~ v3_struct_0(g3_lattices(X1,X2,X3))
& v3_lattices(g3_lattices(X1,X2,X3)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc3_lattices) ).
fof(t11_filter_2,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v15_lattices(X1)
& v16_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& v10_lattices(X2)
& v15_lattices(X2)
& v16_lattices(X2)
& l3_lattices(X2) )
=> ( g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1)) = g3_lattices(u1_struct_0(X2),u2_lattices(X2),u1_lattices(X2))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X1))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(X2))
=> ! [X6] :
( m1_subset_1(X6,u1_struct_0(X2))
=> ( ( X3 = X5
& X4 = X6
& r2_lattices(X1,X3,X4) )
=> r2_lattices(X2,X5,X6) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t11_filter_2) ).
fof(fc5_lattice2,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v7_lattices(X1)
& l1_lattices(X1) )
=> ( v1_relat_1(u1_lattices(X1))
& v1_funct_1(u1_lattices(X1))
& v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
& v2_binop_1(u1_lattices(X1),u1_struct_0(X1))
& v1_partfun1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc5_lattice2) ).
fof(fc4_lattice2,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v6_lattices(X1)
& l1_lattices(X1) )
=> ( v1_relat_1(u1_lattices(X1))
& v1_funct_1(u1_lattices(X1))
& v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
& v1_binop_1(u1_lattices(X1),u1_struct_0(X1))
& v1_partfun1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc4_lattice2) ).
fof(fc3_lattice2,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v5_lattices(X1)
& l2_lattices(X1) )
=> ( v1_relat_1(u2_lattices(X1))
& v1_funct_1(u2_lattices(X1))
& v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
& v2_binop_1(u2_lattices(X1),u1_struct_0(X1))
& v1_partfun1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc3_lattice2) ).
fof(fc2_lattice2,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v4_lattices(X1)
& l2_lattices(X1) )
=> ( v1_relat_1(u2_lattices(X1))
& v1_funct_1(u2_lattices(X1))
& v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
& v1_binop_1(u2_lattices(X1),u1_struct_0(X1))
& v1_partfun1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc2_lattice2) ).
fof(t12_filter_2,conjecture,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& v10_lattices(X2)
& v17_lattices(X2)
& l3_lattices(X2) )
=> ( g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1)) = g3_lattices(u1_struct_0(X2),u2_lattices(X2),u1_lattices(X2))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X2))
=> ( X3 = X4
=> k7_lattices(X1,X3) = k7_lattices(X2,X4) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_filter_2) ).
fof(dt_k7_lattices,axiom,
! [X1,X2] :
( ( ~ v3_struct_0(X1)
& l3_lattices(X1)
& m1_subset_1(X2,u1_struct_0(X1)) )
=> m1_subset_1(k7_lattices(X1,X2),u1_struct_0(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k7_lattices) ).
fof(cc2_lattices,axiom,
! [X1] :
( l3_lattices(X1)
=> ( ( ~ v3_struct_0(X1)
& v4_lattices(X1)
& v5_lattices(X1)
& v6_lattices(X1)
& v7_lattices(X1)
& v8_lattices(X1)
& v9_lattices(X1) )
=> ( ~ v3_struct_0(X1)
& v10_lattices(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc2_lattices) ).
fof(fc4_subset_1,axiom,
! [X1,X2] :
( ( ~ v1_xboole_0(X1)
& ~ v1_xboole_0(X2) )
=> ~ v1_xboole_0(k2_zfmisc_1(X1,X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc4_subset_1) ).
fof(rc5_struct_0,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& l1_struct_0(X1) )
=> ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
& ~ v1_xboole_0(X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc5_struct_0) ).
fof(antisymmetry_r2_hidden,axiom,
! [X1,X2] :
( r2_hidden(X1,X2)
=> ~ r2_hidden(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(cc6_lattices,axiom,
! [X1] :
( l3_lattices(X1)
=> ( ( ~ v3_struct_0(X1)
& v11_lattices(X1)
& v15_lattices(X1)
& v16_lattices(X1) )
=> ( ~ v3_struct_0(X1)
& v17_lattices(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc6_lattices) ).
fof(rc1_subset_1,axiom,
! [X1] :
( ~ v1_xboole_0(X1)
=> ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(X1))
& ~ v1_xboole_0(X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_subset_1) ).
fof(cc7_lattices,axiom,
! [X1] :
( l3_lattices(X1)
=> ( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v11_lattices(X1) )
=> ( ~ v3_struct_0(X1)
& v4_lattices(X1)
& v5_lattices(X1)
& v6_lattices(X1)
& v7_lattices(X1)
& v8_lattices(X1)
& v9_lattices(X1)
& v10_lattices(X1)
& v12_lattices(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc7_lattices) ).
fof(cc3_lattices,axiom,
! [X1] :
( l3_lattices(X1)
=> ( ( ~ v3_struct_0(X1)
& v13_lattices(X1)
& v14_lattices(X1) )
=> ( ~ v3_struct_0(X1)
& v15_lattices(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc3_lattices) ).
fof(fc1_struct_0,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& l1_struct_0(X1) )
=> ~ v1_xboole_0(u1_struct_0(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(cc5_lattices,axiom,
! [X1] :
( l3_lattices(X1)
=> ( ( ~ v3_struct_0(X1)
& v17_lattices(X1) )
=> ( ~ v3_struct_0(X1)
& v11_lattices(X1)
& v13_lattices(X1)
& v14_lattices(X1)
& v15_lattices(X1)
& v16_lattices(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc5_lattices) ).
fof(cc4_lattices,axiom,
! [X1] :
( l3_lattices(X1)
=> ( ( ~ v3_struct_0(X1)
& v15_lattices(X1) )
=> ( ~ v3_struct_0(X1)
& v13_lattices(X1)
& v14_lattices(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc4_lattices) ).
fof(cc1_lattices,axiom,
! [X1] :
( l3_lattices(X1)
=> ( ( ~ v3_struct_0(X1)
& v10_lattices(X1) )
=> ( ~ v3_struct_0(X1)
& v4_lattices(X1)
& v5_lattices(X1)
& v6_lattices(X1)
& v7_lattices(X1)
& v8_lattices(X1)
& v9_lattices(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_lattices) ).
fof(fc1_subset_1,axiom,
! [X1] : ~ v1_xboole_0(k1_zfmisc_1(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(rc2_xboole_0,axiom,
? [X1] : ~ v1_xboole_0(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(rc9_lattices,axiom,
? [X1] :
( l3_lattices(X1)
& ~ v3_struct_0(X1)
& v3_lattices(X1)
& v4_lattices(X1)
& v5_lattices(X1)
& v6_lattices(X1)
& v7_lattices(X1)
& v8_lattices(X1)
& v9_lattices(X1)
& v10_lattices(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc9_lattices) ).
fof(rc6_lattices,axiom,
? [X1] :
( l3_lattices(X1)
& ~ v3_struct_0(X1)
& v3_lattices(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc6_lattices) ).
fof(rc3_struct_0,axiom,
? [X1] :
( l1_struct_0(X1)
& ~ v3_struct_0(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc3_struct_0) ).
fof(rc13_lattices,axiom,
? [X1] :
( l3_lattices(X1)
& ~ v3_struct_0(X1)
& v3_lattices(X1)
& v4_lattices(X1)
& v5_lattices(X1)
& v6_lattices(X1)
& v7_lattices(X1)
& v8_lattices(X1)
& v9_lattices(X1)
& v10_lattices(X1)
& v11_lattices(X1)
& v13_lattices(X1)
& v14_lattices(X1)
& v15_lattices(X1)
& v16_lattices(X1)
& v17_lattices(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc13_lattices) ).
fof(rc12_lattices,axiom,
? [X1] :
( l3_lattices(X1)
& ~ v3_struct_0(X1)
& v3_lattices(X1)
& v4_lattices(X1)
& v5_lattices(X1)
& v6_lattices(X1)
& v7_lattices(X1)
& v8_lattices(X1)
& v9_lattices(X1)
& v10_lattices(X1)
& v13_lattices(X1)
& v14_lattices(X1)
& v15_lattices(X1)
& v16_lattices(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc12_lattices) ).
fof(rc11_lattices,axiom,
? [X1] :
( l3_lattices(X1)
& ~ v3_struct_0(X1)
& v3_lattices(X1)
& v4_lattices(X1)
& v5_lattices(X1)
& v6_lattices(X1)
& v7_lattices(X1)
& v8_lattices(X1)
& v9_lattices(X1)
& v10_lattices(X1)
& v13_lattices(X1)
& v14_lattices(X1)
& v15_lattices(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc11_lattices) ).
fof(rc10_lattices,axiom,
? [X1] :
( l3_lattices(X1)
& ~ v3_struct_0(X1)
& v3_lattices(X1)
& v4_lattices(X1)
& v5_lattices(X1)
& v6_lattices(X1)
& v7_lattices(X1)
& v8_lattices(X1)
& v9_lattices(X1)
& v10_lattices(X1)
& v11_lattices(X1)
& v12_lattices(X1)
& v13_lattices(X1)
& v14_lattices(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc10_lattices) ).
fof(free_g3_lattices,axiom,
! [X1,X2,X3] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
& m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)
& v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
& m1_relset_1(X3,k2_zfmisc_1(X1,X1),X1) )
=> ! [X4,X5,X6] :
( g3_lattices(X1,X2,X3) = g3_lattices(X4,X5,X6)
=> ( X1 = X4
& X2 = X5
& X3 = X6 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',free_g3_lattices) ).
fof(dt_g3_lattices,axiom,
! [X1,X2,X3] :
( ( v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
& m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)
& v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
& m1_relset_1(X3,k2_zfmisc_1(X1,X1),X1) )
=> ( v3_lattices(g3_lattices(X1,X2,X3))
& l3_lattices(g3_lattices(X1,X2,X3)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_g3_lattices) ).
fof(dt_m2_relset_1,axiom,
! [X1,X2,X3] :
( m2_relset_1(X3,X1,X2)
=> m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X1,X2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(redefinition_m2_relset_1,axiom,
! [X1,X2,X3] :
( m2_relset_1(X3,X1,X2)
<=> m1_relset_1(X3,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(dt_u1_lattices,axiom,
! [X1] :
( l1_lattices(X1)
=> ( v1_funct_1(u1_lattices(X1))
& v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
& m2_relset_1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_u1_lattices) ).
fof(dt_u2_lattices,axiom,
! [X1] :
( l2_lattices(X1)
=> ( v1_funct_1(u2_lattices(X1))
& v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
& m2_relset_1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_u2_lattices) ).
fof(cc1_relset_1,axiom,
! [X1,X2,X3] :
( m1_subset_1(X3,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))
=> v1_relat_1(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(abstractness_v3_lattices,axiom,
! [X1] :
( l3_lattices(X1)
=> ( v3_lattices(X1)
=> X1 = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',abstractness_v3_lattices) ).
fof(existence_m2_relset_1,axiom,
! [X1,X2] :
? [X3] : m2_relset_1(X3,X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_m2_relset_1) ).
fof(existence_m1_relset_1,axiom,
! [X1,X2] :
? [X3] : m1_relset_1(X3,X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_m1_relset_1) ).
fof(t4_subset,axiom,
! [X1,X2,X3] :
( ( r2_hidden(X1,X2)
& m1_subset_1(X2,k1_zfmisc_1(X3)) )
=> m1_subset_1(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
fof(t5_subset,axiom,
! [X1,X2,X3] :
~ ( r2_hidden(X1,X2)
& m1_subset_1(X2,k1_zfmisc_1(X3))
& v1_xboole_0(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_subset) ).
fof(t3_subset,axiom,
! [X1,X2] :
( m1_subset_1(X1,k1_zfmisc_1(X2))
<=> r1_tarski(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_subset) ).
fof(t2_subset,axiom,
! [X1,X2] :
( m1_subset_1(X1,X2)
=> ( v1_xboole_0(X2)
| r2_hidden(X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_subset) ).
fof(t1_subset,axiom,
! [X1,X2] :
( r2_hidden(X1,X2)
=> m1_subset_1(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_subset) ).
fof(t7_boole,axiom,
! [X1,X2] :
~ ( r2_hidden(X1,X2)
& v1_xboole_0(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(rc2_subset_1,axiom,
! [X1] :
? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(X1))
& v1_xboole_0(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_subset_1) ).
fof(cc2_funct_1,axiom,
! [X1] :
( ( v1_relat_1(X1)
& v1_xboole_0(X1)
& v1_funct_1(X1) )
=> ( v1_relat_1(X1)
& v1_funct_1(X1)
& v2_funct_1(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc2_funct_1) ).
fof(existence_m1_subset_1,axiom,
! [X1] :
? [X2] : m1_subset_1(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_m1_subset_1) ).
fof(t8_boole,axiom,
! [X1,X2] :
~ ( v1_xboole_0(X1)
& X1 != X2
& v1_xboole_0(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_boole) ).
fof(reflexivity_r1_tarski,axiom,
! [X1,X2] : r1_tarski(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(dt_l3_lattices,axiom,
! [X1] :
( l3_lattices(X1)
=> ( l1_lattices(X1)
& l2_lattices(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(dt_l2_lattices,axiom,
! [X1] :
( l2_lattices(X1)
=> l1_struct_0(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l2_lattices) ).
fof(dt_l1_lattices,axiom,
! [X1] :
( l1_lattices(X1)
=> l1_struct_0(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_lattices) ).
fof(cc1_funct_1,axiom,
! [X1] :
( v1_xboole_0(X1)
=> v1_funct_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_funct_1) ).
fof(t6_boole,axiom,
! [X1] :
( v1_xboole_0(X1)
=> X1 = k1_xboole_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_boole) ).
fof(existence_l2_lattices,axiom,
? [X1] : l2_lattices(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_l2_lattices) ).
fof(existence_l1_struct_0,axiom,
? [X1] : l1_struct_0(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_l1_struct_0) ).
fof(existence_l1_lattices,axiom,
? [X1] : l1_lattices(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_l1_lattices) ).
fof(rc3_funct_1,axiom,
? [X1] :
( v1_relat_1(X1)
& v1_funct_1(X1)
& v2_funct_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc3_funct_1) ).
fof(rc2_funct_1,axiom,
? [X1] :
( v1_relat_1(X1)
& v1_xboole_0(X1)
& v1_funct_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_funct_1) ).
fof(rc1_funct_1,axiom,
? [X1] :
( v1_relat_1(X1)
& v1_funct_1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_funct_1) ).
fof(rc1_xboole_0,axiom,
? [X1] : v1_xboole_0(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_xboole_0) ).
fof(rc3_lattices,axiom,
? [X1] :
( l3_lattices(X1)
& v3_lattices(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc3_lattices) ).
fof(existence_l3_lattices,axiom,
? [X1] : l3_lattices(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_l3_lattices) ).
fof(fc1_xboole_0,axiom,
v1_xboole_0(k1_xboole_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_xboole_0) ).
fof(i_0_66,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v11_lattices(X1)
& v16_lattices(X1)
& l3_lattices(X1) )
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ( X3 = k7_lattices(X1,X2)
<=> r2_lattices(X1,X3,X2) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[d21_lattices]) ).
fof(i_0_67,plain,
! [X1,X2,X3] :
( ( ~ v1_xboole_0(X1)
& v1_funct_1(X2)
& v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
& m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)
& v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
& m1_relset_1(X3,k2_zfmisc_1(X1,X1),X1) )
=> ( ~ v3_struct_0(g3_lattices(X1,X2,X3))
& v3_lattices(g3_lattices(X1,X2,X3)) ) ),
inference(fof_simplification,[status(thm)],[fc3_lattices]) ).
fof(i_0_68,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v15_lattices(X1)
& v16_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& v10_lattices(X2)
& v15_lattices(X2)
& v16_lattices(X2)
& l3_lattices(X2) )
=> ( g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1)) = g3_lattices(u1_struct_0(X2),u2_lattices(X2),u1_lattices(X2))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X1))
=> ! [X5] :
( m1_subset_1(X5,u1_struct_0(X2))
=> ! [X6] :
( m1_subset_1(X6,u1_struct_0(X2))
=> ( ( X3 = X5
& X4 = X6
& r2_lattices(X1,X3,X4) )
=> r2_lattices(X2,X5,X6) ) ) ) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[t11_filter_2]) ).
fof(i_0_69,plain,
! [X137,X138,X139] :
( ( X139 != k7_lattices(X137,X138)
| r2_lattices(X137,X139,X138)
| ~ m1_subset_1(X139,u1_struct_0(X137))
| v3_struct_0(X137)
| ~ v10_lattices(X137)
| ~ v11_lattices(X137)
| ~ v16_lattices(X137)
| ~ l3_lattices(X137)
| ~ m1_subset_1(X138,u1_struct_0(X137))
| v3_struct_0(X137)
| ~ l3_lattices(X137) )
& ( ~ r2_lattices(X137,X139,X138)
| X139 = k7_lattices(X137,X138)
| ~ m1_subset_1(X139,u1_struct_0(X137))
| v3_struct_0(X137)
| ~ v10_lattices(X137)
| ~ v11_lattices(X137)
| ~ v16_lattices(X137)
| ~ l3_lattices(X137)
| ~ m1_subset_1(X138,u1_struct_0(X137))
| v3_struct_0(X137)
| ~ l3_lattices(X137) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_66])])])]) ).
fof(i_0_70,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v7_lattices(X1)
& l1_lattices(X1) )
=> ( v1_relat_1(u1_lattices(X1))
& v1_funct_1(u1_lattices(X1))
& v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
& v2_binop_1(u1_lattices(X1),u1_struct_0(X1))
& v1_partfun1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)) ) ),
inference(fof_simplification,[status(thm)],[fc5_lattice2]) ).
fof(i_0_71,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v6_lattices(X1)
& l1_lattices(X1) )
=> ( v1_relat_1(u1_lattices(X1))
& v1_funct_1(u1_lattices(X1))
& v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
& v1_binop_1(u1_lattices(X1),u1_struct_0(X1))
& v1_partfun1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)) ) ),
inference(fof_simplification,[status(thm)],[fc4_lattice2]) ).
fof(i_0_72,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v5_lattices(X1)
& l2_lattices(X1) )
=> ( v1_relat_1(u2_lattices(X1))
& v1_funct_1(u2_lattices(X1))
& v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
& v2_binop_1(u2_lattices(X1),u1_struct_0(X1))
& v1_partfun1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)) ) ),
inference(fof_simplification,[status(thm)],[fc3_lattice2]) ).
fof(i_0_73,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v4_lattices(X1)
& l2_lattices(X1) )
=> ( v1_relat_1(u2_lattices(X1))
& v1_funct_1(u2_lattices(X1))
& v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
& v1_binop_1(u2_lattices(X1),u1_struct_0(X1))
& v1_partfun1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1)) ) ),
inference(fof_simplification,[status(thm)],[fc2_lattice2]) ).
fof(i_0_74,negated_conjecture,
~ ! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v17_lattices(X1)
& l3_lattices(X1) )
=> ! [X2] :
( ( ~ v3_struct_0(X2)
& v10_lattices(X2)
& v17_lattices(X2)
& l3_lattices(X2) )
=> ( g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1)) = g3_lattices(u1_struct_0(X2),u2_lattices(X2),u1_lattices(X2))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X1))
=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X2))
=> ( X3 = X4
=> k7_lattices(X1,X3) = k7_lattices(X2,X4) ) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[t12_filter_2])]) ).
fof(i_0_75,plain,
! [X1,X2] :
( ( ~ v3_struct_0(X1)
& l3_lattices(X1)
& m1_subset_1(X2,u1_struct_0(X1)) )
=> m1_subset_1(k7_lattices(X1,X2),u1_struct_0(X1)) ),
inference(fof_simplification,[status(thm)],[dt_k7_lattices]) ).
fof(i_0_76,plain,
! [X1] :
( l3_lattices(X1)
=> ( ( ~ v3_struct_0(X1)
& v4_lattices(X1)
& v5_lattices(X1)
& v6_lattices(X1)
& v7_lattices(X1)
& v8_lattices(X1)
& v9_lattices(X1) )
=> ( ~ v3_struct_0(X1)
& v10_lattices(X1) ) ) ),
inference(fof_simplification,[status(thm)],[cc2_lattices]) ).
fof(i_0_77,plain,
! [X1,X2] :
( ( ~ v1_xboole_0(X1)
& ~ v1_xboole_0(X2) )
=> ~ v1_xboole_0(k2_zfmisc_1(X1,X2)) ),
inference(fof_simplification,[status(thm)],[fc4_subset_1]) ).
fof(i_0_78,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& l1_struct_0(X1) )
=> ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X1)))
& ~ v1_xboole_0(X2) ) ),
inference(fof_simplification,[status(thm)],[rc5_struct_0]) ).
fof(i_0_79,plain,
! [X1,X2] :
( r2_hidden(X1,X2)
=> ~ r2_hidden(X2,X1) ),
inference(fof_simplification,[status(thm)],[antisymmetry_r2_hidden]) ).
fof(i_0_80,plain,
! [X1] :
( l3_lattices(X1)
=> ( ( ~ v3_struct_0(X1)
& v11_lattices(X1)
& v15_lattices(X1)
& v16_lattices(X1) )
=> ( ~ v3_struct_0(X1)
& v17_lattices(X1) ) ) ),
inference(fof_simplification,[status(thm)],[cc6_lattices]) ).
fof(i_0_81,plain,
! [X1] :
( ~ v1_xboole_0(X1)
=> ? [X2] :
( m1_subset_1(X2,k1_zfmisc_1(X1))
& ~ v1_xboole_0(X2) ) ),
inference(fof_simplification,[status(thm)],[rc1_subset_1]) ).
fof(i_0_82,plain,
! [X1] :
( l3_lattices(X1)
=> ( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v11_lattices(X1) )
=> ( ~ v3_struct_0(X1)
& v4_lattices(X1)
& v5_lattices(X1)
& v6_lattices(X1)
& v7_lattices(X1)
& v8_lattices(X1)
& v9_lattices(X1)
& v10_lattices(X1)
& v12_lattices(X1) ) ) ),
inference(fof_simplification,[status(thm)],[cc7_lattices]) ).
fof(i_0_83,plain,
! [X1] :
( l3_lattices(X1)
=> ( ( ~ v3_struct_0(X1)
& v13_lattices(X1)
& v14_lattices(X1) )
=> ( ~ v3_struct_0(X1)
& v15_lattices(X1) ) ) ),
inference(fof_simplification,[status(thm)],[cc3_lattices]) ).
fof(i_0_84,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& l1_struct_0(X1) )
=> ~ v1_xboole_0(u1_struct_0(X1)) ),
inference(fof_simplification,[status(thm)],[fc1_struct_0]) ).
fof(i_0_85,plain,
! [X1] :
( l3_lattices(X1)
=> ( ( ~ v3_struct_0(X1)
& v17_lattices(X1) )
=> ( ~ v3_struct_0(X1)
& v11_lattices(X1)
& v13_lattices(X1)
& v14_lattices(X1)
& v15_lattices(X1)
& v16_lattices(X1) ) ) ),
inference(fof_simplification,[status(thm)],[cc5_lattices]) ).
fof(i_0_86,plain,
! [X1] :
( l3_lattices(X1)
=> ( ( ~ v3_struct_0(X1)
& v15_lattices(X1) )
=> ( ~ v3_struct_0(X1)
& v13_lattices(X1)
& v14_lattices(X1) ) ) ),
inference(fof_simplification,[status(thm)],[cc4_lattices]) ).
fof(i_0_87,plain,
! [X1] :
( l3_lattices(X1)
=> ( ( ~ v3_struct_0(X1)
& v10_lattices(X1) )
=> ( ~ v3_struct_0(X1)
& v4_lattices(X1)
& v5_lattices(X1)
& v6_lattices(X1)
& v7_lattices(X1)
& v8_lattices(X1)
& v9_lattices(X1) ) ) ),
inference(fof_simplification,[status(thm)],[cc1_lattices]) ).
fof(i_0_88,plain,
! [X1] : ~ v1_xboole_0(k1_zfmisc_1(X1)),
inference(fof_simplification,[status(thm)],[fc1_subset_1]) ).
fof(i_0_89,plain,
? [X1] : ~ v1_xboole_0(X1),
inference(fof_simplification,[status(thm)],[rc2_xboole_0]) ).
fof(i_0_90,plain,
? [X1] :
( l3_lattices(X1)
& ~ v3_struct_0(X1)
& v3_lattices(X1)
& v4_lattices(X1)
& v5_lattices(X1)
& v6_lattices(X1)
& v7_lattices(X1)
& v8_lattices(X1)
& v9_lattices(X1)
& v10_lattices(X1) ),
inference(fof_simplification,[status(thm)],[rc9_lattices]) ).
fof(i_0_91,plain,
? [X1] :
( l3_lattices(X1)
& ~ v3_struct_0(X1)
& v3_lattices(X1) ),
inference(fof_simplification,[status(thm)],[rc6_lattices]) ).
fof(i_0_92,plain,
? [X1] :
( l1_struct_0(X1)
& ~ v3_struct_0(X1) ),
inference(fof_simplification,[status(thm)],[rc3_struct_0]) ).
fof(i_0_93,plain,
? [X1] :
( l3_lattices(X1)
& ~ v3_struct_0(X1)
& v3_lattices(X1)
& v4_lattices(X1)
& v5_lattices(X1)
& v6_lattices(X1)
& v7_lattices(X1)
& v8_lattices(X1)
& v9_lattices(X1)
& v10_lattices(X1)
& v11_lattices(X1)
& v13_lattices(X1)
& v14_lattices(X1)
& v15_lattices(X1)
& v16_lattices(X1)
& v17_lattices(X1) ),
inference(fof_simplification,[status(thm)],[rc13_lattices]) ).
fof(i_0_94,plain,
? [X1] :
( l3_lattices(X1)
& ~ v3_struct_0(X1)
& v3_lattices(X1)
& v4_lattices(X1)
& v5_lattices(X1)
& v6_lattices(X1)
& v7_lattices(X1)
& v8_lattices(X1)
& v9_lattices(X1)
& v10_lattices(X1)
& v13_lattices(X1)
& v14_lattices(X1)
& v15_lattices(X1)
& v16_lattices(X1) ),
inference(fof_simplification,[status(thm)],[rc12_lattices]) ).
fof(i_0_95,plain,
? [X1] :
( l3_lattices(X1)
& ~ v3_struct_0(X1)
& v3_lattices(X1)
& v4_lattices(X1)
& v5_lattices(X1)
& v6_lattices(X1)
& v7_lattices(X1)
& v8_lattices(X1)
& v9_lattices(X1)
& v10_lattices(X1)
& v13_lattices(X1)
& v14_lattices(X1)
& v15_lattices(X1) ),
inference(fof_simplification,[status(thm)],[rc11_lattices]) ).
fof(i_0_96,plain,
? [X1] :
( l3_lattices(X1)
& ~ v3_struct_0(X1)
& v3_lattices(X1)
& v4_lattices(X1)
& v5_lattices(X1)
& v6_lattices(X1)
& v7_lattices(X1)
& v8_lattices(X1)
& v9_lattices(X1)
& v10_lattices(X1)
& v11_lattices(X1)
& v12_lattices(X1)
& v13_lattices(X1)
& v14_lattices(X1) ),
inference(fof_simplification,[status(thm)],[rc10_lattices]) ).
fof(i_0_97,plain,
! [X169,X170,X171] :
( ( ~ v3_struct_0(g3_lattices(X169,X170,X171))
| v1_xboole_0(X169)
| ~ v1_funct_1(X170)
| ~ v1_funct_2(X170,k2_zfmisc_1(X169,X169),X169)
| ~ m1_relset_1(X170,k2_zfmisc_1(X169,X169),X169)
| ~ v1_funct_1(X171)
| ~ v1_funct_2(X171,k2_zfmisc_1(X169,X169),X169)
| ~ m1_relset_1(X171,k2_zfmisc_1(X169,X169),X169) )
& ( v3_lattices(g3_lattices(X169,X170,X171))
| v1_xboole_0(X169)
| ~ v1_funct_1(X170)
| ~ v1_funct_2(X170,k2_zfmisc_1(X169,X169),X169)
| ~ m1_relset_1(X170,k2_zfmisc_1(X169,X169),X169)
| ~ v1_funct_1(X171)
| ~ v1_funct_2(X171,k2_zfmisc_1(X169,X169),X169)
| ~ m1_relset_1(X171,k2_zfmisc_1(X169,X169),X169) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_67])])]) ).
fof(i_0_98,plain,
! [X176,X177,X178,X179,X180,X181] :
( ( X176 = X179
| g3_lattices(X176,X177,X178) != g3_lattices(X179,X180,X181)
| ~ v1_funct_1(X177)
| ~ v1_funct_2(X177,k2_zfmisc_1(X176,X176),X176)
| ~ m1_relset_1(X177,k2_zfmisc_1(X176,X176),X176)
| ~ v1_funct_1(X178)
| ~ v1_funct_2(X178,k2_zfmisc_1(X176,X176),X176)
| ~ m1_relset_1(X178,k2_zfmisc_1(X176,X176),X176) )
& ( X177 = X180
| g3_lattices(X176,X177,X178) != g3_lattices(X179,X180,X181)
| ~ v1_funct_1(X177)
| ~ v1_funct_2(X177,k2_zfmisc_1(X176,X176),X176)
| ~ m1_relset_1(X177,k2_zfmisc_1(X176,X176),X176)
| ~ v1_funct_1(X178)
| ~ v1_funct_2(X178,k2_zfmisc_1(X176,X176),X176)
| ~ m1_relset_1(X178,k2_zfmisc_1(X176,X176),X176) )
& ( X178 = X181
| g3_lattices(X176,X177,X178) != g3_lattices(X179,X180,X181)
| ~ v1_funct_1(X177)
| ~ v1_funct_2(X177,k2_zfmisc_1(X176,X176),X176)
| ~ m1_relset_1(X177,k2_zfmisc_1(X176,X176),X176)
| ~ v1_funct_1(X178)
| ~ v1_funct_2(X178,k2_zfmisc_1(X176,X176),X176)
| ~ m1_relset_1(X178,k2_zfmisc_1(X176,X176),X176) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[free_g3_lattices])])])]) ).
fof(i_0_99,plain,
! [X140,X141,X142] :
( ( v3_lattices(g3_lattices(X140,X141,X142))
| ~ v1_funct_1(X141)
| ~ v1_funct_2(X141,k2_zfmisc_1(X140,X140),X140)
| ~ m1_relset_1(X141,k2_zfmisc_1(X140,X140),X140)
| ~ v1_funct_1(X142)
| ~ v1_funct_2(X142,k2_zfmisc_1(X140,X140),X140)
| ~ m1_relset_1(X142,k2_zfmisc_1(X140,X140),X140) )
& ( l3_lattices(g3_lattices(X140,X141,X142))
| ~ v1_funct_1(X141)
| ~ v1_funct_2(X141,k2_zfmisc_1(X140,X140),X140)
| ~ m1_relset_1(X141,k2_zfmisc_1(X140,X140),X140)
| ~ v1_funct_1(X142)
| ~ v1_funct_2(X142,k2_zfmisc_1(X140,X140),X140)
| ~ m1_relset_1(X142,k2_zfmisc_1(X140,X140),X140) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[dt_g3_lattices])])]) ).
fof(i_0_100,plain,
! [X205,X206,X207,X208,X209,X210] :
( v3_struct_0(X205)
| ~ v10_lattices(X205)
| ~ v15_lattices(X205)
| ~ v16_lattices(X205)
| ~ l3_lattices(X205)
| v3_struct_0(X206)
| ~ v10_lattices(X206)
| ~ v15_lattices(X206)
| ~ v16_lattices(X206)
| ~ l3_lattices(X206)
| g3_lattices(u1_struct_0(X205),u2_lattices(X205),u1_lattices(X205)) != g3_lattices(u1_struct_0(X206),u2_lattices(X206),u1_lattices(X206))
| ~ m1_subset_1(X207,u1_struct_0(X205))
| ~ m1_subset_1(X208,u1_struct_0(X205))
| ~ m1_subset_1(X209,u1_struct_0(X206))
| ~ m1_subset_1(X210,u1_struct_0(X206))
| X207 != X209
| X208 != X210
| ~ r2_lattices(X205,X207,X208)
| r2_lattices(X206,X209,X210) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_68])])]) ).
cnf(i_0_101,plain,
( X2 = k7_lattices(X1,X3)
| v3_struct_0(X1)
| v3_struct_0(X1)
| ~ r2_lattices(X1,X2,X3)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ v10_lattices(X1)
| ~ v11_lattices(X1)
| ~ v16_lattices(X1)
| ~ l3_lattices(X1)
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_69]) ).
cnf(i_0_102,plain,
( r2_lattices(X2,X1,X3)
| v3_struct_0(X2)
| v3_struct_0(X2)
| X1 != k7_lattices(X2,X3)
| ~ m1_subset_1(X1,u1_struct_0(X2))
| ~ v10_lattices(X2)
| ~ v11_lattices(X2)
| ~ v16_lattices(X2)
| ~ l3_lattices(X2)
| ~ m1_subset_1(X3,u1_struct_0(X2))
| ~ l3_lattices(X2) ),
inference(split_conjunct,[status(thm)],[i_0_69]) ).
fof(i_0_103,plain,
! [X148,X149,X150] :
( ~ m2_relset_1(X150,X148,X149)
| m1_subset_1(X150,k1_zfmisc_1(k2_zfmisc_1(X148,X149))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[dt_m2_relset_1])]) ).
fof(i_0_104,plain,
! [X201,X202,X203] :
( ( ~ m2_relset_1(X203,X201,X202)
| m1_relset_1(X203,X201,X202) )
& ( ~ m1_relset_1(X203,X201,X202)
| m2_relset_1(X203,X201,X202) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[redefinition_m2_relset_1])]) ).
fof(i_0_105,plain,
! [X175] :
( ( v1_relat_1(u1_lattices(X175))
| v3_struct_0(X175)
| ~ v7_lattices(X175)
| ~ l1_lattices(X175) )
& ( v1_funct_1(u1_lattices(X175))
| v3_struct_0(X175)
| ~ v7_lattices(X175)
| ~ l1_lattices(X175) )
& ( v1_funct_2(u1_lattices(X175),k2_zfmisc_1(u1_struct_0(X175),u1_struct_0(X175)),u1_struct_0(X175))
| v3_struct_0(X175)
| ~ v7_lattices(X175)
| ~ l1_lattices(X175) )
& ( v2_binop_1(u1_lattices(X175),u1_struct_0(X175))
| v3_struct_0(X175)
| ~ v7_lattices(X175)
| ~ l1_lattices(X175) )
& ( v1_partfun1(u1_lattices(X175),k2_zfmisc_1(u1_struct_0(X175),u1_struct_0(X175)),u1_struct_0(X175))
| v3_struct_0(X175)
| ~ v7_lattices(X175)
| ~ l1_lattices(X175) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_70])])]) ).
fof(i_0_106,plain,
! [X172] :
( ( v1_relat_1(u1_lattices(X172))
| v3_struct_0(X172)
| ~ v6_lattices(X172)
| ~ l1_lattices(X172) )
& ( v1_funct_1(u1_lattices(X172))
| v3_struct_0(X172)
| ~ v6_lattices(X172)
| ~ l1_lattices(X172) )
& ( v1_funct_2(u1_lattices(X172),k2_zfmisc_1(u1_struct_0(X172),u1_struct_0(X172)),u1_struct_0(X172))
| v3_struct_0(X172)
| ~ v6_lattices(X172)
| ~ l1_lattices(X172) )
& ( v1_binop_1(u1_lattices(X172),u1_struct_0(X172))
| v3_struct_0(X172)
| ~ v6_lattices(X172)
| ~ l1_lattices(X172) )
& ( v1_partfun1(u1_lattices(X172),k2_zfmisc_1(u1_struct_0(X172),u1_struct_0(X172)),u1_struct_0(X172))
| v3_struct_0(X172)
| ~ v6_lattices(X172)
| ~ l1_lattices(X172) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_71])])]) ).
fof(i_0_107,plain,
! [X168] :
( ( v1_relat_1(u2_lattices(X168))
| v3_struct_0(X168)
| ~ v5_lattices(X168)
| ~ l2_lattices(X168) )
& ( v1_funct_1(u2_lattices(X168))
| v3_struct_0(X168)
| ~ v5_lattices(X168)
| ~ l2_lattices(X168) )
& ( v1_funct_2(u2_lattices(X168),k2_zfmisc_1(u1_struct_0(X168),u1_struct_0(X168)),u1_struct_0(X168))
| v3_struct_0(X168)
| ~ v5_lattices(X168)
| ~ l2_lattices(X168) )
& ( v2_binop_1(u2_lattices(X168),u1_struct_0(X168))
| v3_struct_0(X168)
| ~ v5_lattices(X168)
| ~ l2_lattices(X168) )
& ( v1_partfun1(u2_lattices(X168),k2_zfmisc_1(u1_struct_0(X168),u1_struct_0(X168)),u1_struct_0(X168))
| v3_struct_0(X168)
| ~ v5_lattices(X168)
| ~ l2_lattices(X168) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_72])])]) ).
fof(i_0_108,plain,
! [X167] :
( ( v1_relat_1(u2_lattices(X167))
| v3_struct_0(X167)
| ~ v4_lattices(X167)
| ~ l2_lattices(X167) )
& ( v1_funct_1(u2_lattices(X167))
| v3_struct_0(X167)
| ~ v4_lattices(X167)
| ~ l2_lattices(X167) )
& ( v1_funct_2(u2_lattices(X167),k2_zfmisc_1(u1_struct_0(X167),u1_struct_0(X167)),u1_struct_0(X167))
| v3_struct_0(X167)
| ~ v4_lattices(X167)
| ~ l2_lattices(X167) )
& ( v1_binop_1(u2_lattices(X167),u1_struct_0(X167))
| v3_struct_0(X167)
| ~ v4_lattices(X167)
| ~ l2_lattices(X167) )
& ( v1_partfun1(u2_lattices(X167),k2_zfmisc_1(u1_struct_0(X167),u1_struct_0(X167)),u1_struct_0(X167))
| v3_struct_0(X167)
| ~ v4_lattices(X167)
| ~ l2_lattices(X167) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_73])])]) ).
fof(i_0_109,negated_conjecture,
( ~ v3_struct_0(esk1_0)
& v10_lattices(esk1_0)
& v17_lattices(esk1_0)
& l3_lattices(esk1_0)
& ~ v3_struct_0(esk2_0)
& v10_lattices(esk2_0)
& v17_lattices(esk2_0)
& l3_lattices(esk2_0)
& g3_lattices(u1_struct_0(esk1_0),u2_lattices(esk1_0),u1_lattices(esk1_0)) = g3_lattices(u1_struct_0(esk2_0),u2_lattices(esk2_0),u1_lattices(esk2_0))
& m1_subset_1(esk3_0,u1_struct_0(esk1_0))
& m1_subset_1(esk4_0,u1_struct_0(esk2_0))
& esk3_0 = esk4_0
& k7_lattices(esk1_0,esk3_0) != k7_lattices(esk2_0,esk4_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_74])])]) ).
fof(i_0_110,plain,
! [X151] :
( ( v1_funct_1(u1_lattices(X151))
| ~ l1_lattices(X151) )
& ( v1_funct_2(u1_lattices(X151),k2_zfmisc_1(u1_struct_0(X151),u1_struct_0(X151)),u1_struct_0(X151))
| ~ l1_lattices(X151) )
& ( m2_relset_1(u1_lattices(X151),k2_zfmisc_1(u1_struct_0(X151),u1_struct_0(X151)),u1_struct_0(X151))
| ~ l1_lattices(X151) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[dt_u1_lattices])])]) ).
fof(i_0_111,plain,
! [X152] :
( ( v1_funct_1(u2_lattices(X152))
| ~ l2_lattices(X152) )
& ( v1_funct_2(u2_lattices(X152),k2_zfmisc_1(u1_struct_0(X152),u1_struct_0(X152)),u1_struct_0(X152))
| ~ l2_lattices(X152) )
& ( m2_relset_1(u2_lattices(X152),k2_zfmisc_1(u1_struct_0(X152),u1_struct_0(X152)),u1_struct_0(X152))
| ~ l2_lattices(X152) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[dt_u2_lattices])])]) ).
fof(i_0_112,plain,
! [X127,X128,X129] :
( ~ m1_subset_1(X129,k1_zfmisc_1(k2_zfmisc_1(X127,X128)))
| v1_relat_1(X129) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cc1_relset_1])]) ).
fof(i_0_113,plain,
! [X143,X144] :
( v3_struct_0(X143)
| ~ l3_lattices(X143)
| ~ m1_subset_1(X144,u1_struct_0(X143))
| m1_subset_1(k7_lattices(X143,X144),u1_struct_0(X143)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_75])]) ).
fof(i_0_114,plain,
! [X122] :
( ~ l3_lattices(X122)
| ~ v3_lattices(X122)
| X122 = g3_lattices(u1_struct_0(X122),u2_lattices(X122),u1_lattices(X122)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[abstractness_v3_lattices])]) ).
fof(i_0_115,plain,
! [X162,X163] : m2_relset_1(esk11_2(X162,X163),X162,X163),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[existence_m2_relset_1])]) ).
fof(i_0_116,plain,
! [X157,X158] : m1_relset_1(esk9_2(X157,X158),X157,X158),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[existence_m1_relset_1])]) ).
fof(i_0_117,plain,
! [X217,X218,X219] :
( ~ r2_hidden(X217,X218)
| ~ m1_subset_1(X218,k1_zfmisc_1(X219))
| m1_subset_1(X217,X219) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t4_subset])]) ).
fof(i_0_118,plain,
! [X220,X221,X222] :
( ~ r2_hidden(X220,X221)
| ~ m1_subset_1(X221,k1_zfmisc_1(X222))
| ~ v1_xboole_0(X222) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t5_subset])]) ).
fof(i_0_119,plain,
! [X131] :
( ( ~ v3_struct_0(X131)
| v3_struct_0(X131)
| ~ v4_lattices(X131)
| ~ v5_lattices(X131)
| ~ v6_lattices(X131)
| ~ v7_lattices(X131)
| ~ v8_lattices(X131)
| ~ v9_lattices(X131)
| ~ l3_lattices(X131) )
& ( v10_lattices(X131)
| v3_struct_0(X131)
| ~ v4_lattices(X131)
| ~ v5_lattices(X131)
| ~ v6_lattices(X131)
| ~ v7_lattices(X131)
| ~ v8_lattices(X131)
| ~ v9_lattices(X131)
| ~ l3_lattices(X131) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_76])])]) ).
fof(i_0_120,plain,
! [X173,X174] :
( v1_xboole_0(X173)
| v1_xboole_0(X174)
| ~ v1_xboole_0(k2_zfmisc_1(X173,X174)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_77])]) ).
fof(i_0_121,plain,
! [X197] :
( ( m1_subset_1(esk25_1(X197),k1_zfmisc_1(u1_struct_0(X197)))
| v3_struct_0(X197)
| ~ l1_struct_0(X197) )
& ( ~ v1_xboole_0(esk25_1(X197))
| v3_struct_0(X197)
| ~ l1_struct_0(X197) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_78])])])]) ).
fof(i_0_122,plain,
! [X215,X216] :
( ( ~ m1_subset_1(X215,k1_zfmisc_1(X216))
| r1_tarski(X215,X216) )
& ( ~ r1_tarski(X215,X216)
| m1_subset_1(X215,k1_zfmisc_1(X216)) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t3_subset])]) ).
fof(i_0_123,plain,
! [X123,X124] :
( ~ r2_hidden(X123,X124)
| ~ r2_hidden(X124,X123) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_79])]) ).
fof(i_0_124,plain,
! [X213,X214] :
( ~ m1_subset_1(X213,X214)
| v1_xboole_0(X214)
| r2_hidden(X213,X214) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t2_subset])]) ).
fof(i_0_125,plain,
! [X135] :
( ( ~ v3_struct_0(X135)
| v3_struct_0(X135)
| ~ v11_lattices(X135)
| ~ v15_lattices(X135)
| ~ v16_lattices(X135)
| ~ l3_lattices(X135) )
& ( v17_lattices(X135)
| v3_struct_0(X135)
| ~ v11_lattices(X135)
| ~ v15_lattices(X135)
| ~ v16_lattices(X135)
| ~ l3_lattices(X135) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_80])])]) ).
fof(i_0_126,plain,
! [X211,X212] :
( ~ r2_hidden(X211,X212)
| m1_subset_1(X211,X212) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t1_subset])]) ).
fof(i_0_127,plain,
! [X187] :
( ( m1_subset_1(esk17_1(X187),k1_zfmisc_1(X187))
| v1_xboole_0(X187) )
& ( ~ v1_xboole_0(esk17_1(X187))
| v1_xboole_0(X187) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_81])])])]) ).
fof(i_0_128,plain,
! [X136] :
( ( ~ v3_struct_0(X136)
| v3_struct_0(X136)
| ~ v10_lattices(X136)
| ~ v11_lattices(X136)
| ~ l3_lattices(X136) )
& ( v4_lattices(X136)
| v3_struct_0(X136)
| ~ v10_lattices(X136)
| ~ v11_lattices(X136)
| ~ l3_lattices(X136) )
& ( v5_lattices(X136)
| v3_struct_0(X136)
| ~ v10_lattices(X136)
| ~ v11_lattices(X136)
| ~ l3_lattices(X136) )
& ( v6_lattices(X136)
| v3_struct_0(X136)
| ~ v10_lattices(X136)
| ~ v11_lattices(X136)
| ~ l3_lattices(X136) )
& ( v7_lattices(X136)
| v3_struct_0(X136)
| ~ v10_lattices(X136)
| ~ v11_lattices(X136)
| ~ l3_lattices(X136) )
& ( v8_lattices(X136)
| v3_struct_0(X136)
| ~ v10_lattices(X136)
| ~ v11_lattices(X136)
| ~ l3_lattices(X136) )
& ( v9_lattices(X136)
| v3_struct_0(X136)
| ~ v10_lattices(X136)
| ~ v11_lattices(X136)
| ~ l3_lattices(X136) )
& ( v10_lattices(X136)
| v3_struct_0(X136)
| ~ v10_lattices(X136)
| ~ v11_lattices(X136)
| ~ l3_lattices(X136) )
& ( v12_lattices(X136)
| v3_struct_0(X136)
| ~ v10_lattices(X136)
| ~ v11_lattices(X136)
| ~ l3_lattices(X136) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_82])])]) ).
fof(i_0_129,plain,
! [X132] :
( ( ~ v3_struct_0(X132)
| v3_struct_0(X132)
| ~ v13_lattices(X132)
| ~ v14_lattices(X132)
| ~ l3_lattices(X132) )
& ( v15_lattices(X132)
| v3_struct_0(X132)
| ~ v13_lattices(X132)
| ~ v14_lattices(X132)
| ~ l3_lattices(X132) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_83])])]) ).
fof(i_0_130,plain,
! [X224,X225] :
( ~ r2_hidden(X224,X225)
| ~ v1_xboole_0(X225) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t7_boole])]) ).
fof(i_0_131,plain,
! [X165] :
( v3_struct_0(X165)
| ~ l1_struct_0(X165)
| ~ v1_xboole_0(u1_struct_0(X165)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_84])]) ).
fof(i_0_132,plain,
! [X191] :
( m1_subset_1(esk20_1(X191),k1_zfmisc_1(X191))
& v1_xboole_0(esk20_1(X191)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc2_subset_1])]) ).
fof(i_0_133,plain,
! [X130] :
( ( v1_relat_1(X130)
| ~ v1_relat_1(X130)
| ~ v1_xboole_0(X130)
| ~ v1_funct_1(X130) )
& ( v1_funct_1(X130)
| ~ v1_relat_1(X130)
| ~ v1_xboole_0(X130)
| ~ v1_funct_1(X130) )
& ( v2_funct_1(X130)
| ~ v1_relat_1(X130)
| ~ v1_xboole_0(X130)
| ~ v1_funct_1(X130) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cc2_funct_1])])]) ).
fof(i_0_134,plain,
! [X134] :
( ( ~ v3_struct_0(X134)
| v3_struct_0(X134)
| ~ v17_lattices(X134)
| ~ l3_lattices(X134) )
& ( v11_lattices(X134)
| v3_struct_0(X134)
| ~ v17_lattices(X134)
| ~ l3_lattices(X134) )
& ( v13_lattices(X134)
| v3_struct_0(X134)
| ~ v17_lattices(X134)
| ~ l3_lattices(X134) )
& ( v14_lattices(X134)
| v3_struct_0(X134)
| ~ v17_lattices(X134)
| ~ l3_lattices(X134) )
& ( v15_lattices(X134)
| v3_struct_0(X134)
| ~ v17_lattices(X134)
| ~ l3_lattices(X134) )
& ( v16_lattices(X134)
| v3_struct_0(X134)
| ~ v17_lattices(X134)
| ~ l3_lattices(X134) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_85])])]) ).
fof(i_0_135,plain,
! [X133] :
( ( ~ v3_struct_0(X133)
| v3_struct_0(X133)
| ~ v15_lattices(X133)
| ~ l3_lattices(X133) )
& ( v13_lattices(X133)
| v3_struct_0(X133)
| ~ v15_lattices(X133)
| ~ l3_lattices(X133) )
& ( v14_lattices(X133)
| v3_struct_0(X133)
| ~ v15_lattices(X133)
| ~ l3_lattices(X133) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_86])])]) ).
fof(i_0_136,plain,
! [X126] :
( ( ~ v3_struct_0(X126)
| v3_struct_0(X126)
| ~ v10_lattices(X126)
| ~ l3_lattices(X126) )
& ( v4_lattices(X126)
| v3_struct_0(X126)
| ~ v10_lattices(X126)
| ~ l3_lattices(X126) )
& ( v5_lattices(X126)
| v3_struct_0(X126)
| ~ v10_lattices(X126)
| ~ l3_lattices(X126) )
& ( v6_lattices(X126)
| v3_struct_0(X126)
| ~ v10_lattices(X126)
| ~ l3_lattices(X126) )
& ( v7_lattices(X126)
| v3_struct_0(X126)
| ~ v10_lattices(X126)
| ~ l3_lattices(X126) )
& ( v8_lattices(X126)
| v3_struct_0(X126)
| ~ v10_lattices(X126)
| ~ l3_lattices(X126) )
& ( v9_lattices(X126)
| v3_struct_0(X126)
| ~ v10_lattices(X126)
| ~ l3_lattices(X126) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_87])])]) ).
fof(i_0_137,plain,
! [X160] : m1_subset_1(esk10_1(X160),X160),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[existence_m1_subset_1])]) ).
fof(i_0_138,plain,
! [X166] : ~ v1_xboole_0(k1_zfmisc_1(X166)),
inference(variable_rename,[status(thm)],[i_0_88]) ).
fof(i_0_139,plain,
! [X226,X227] :
( ~ v1_xboole_0(X226)
| X226 = X227
| ~ v1_xboole_0(X227) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t8_boole])]) ).
fof(i_0_140,plain,
! [X204] : r1_tarski(X204,X204),
inference(variable_rename,[status(thm)],[inference(fof_simplification,[status(thm)],[reflexivity_r1_tarski])]) ).
fof(i_0_141,plain,
! [X147] :
( ( l1_lattices(X147)
| ~ l3_lattices(X147) )
& ( l2_lattices(X147)
| ~ l3_lattices(X147) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[dt_l3_lattices])])]) ).
fof(i_0_142,plain,
! [X146] :
( ~ l2_lattices(X146)
| l1_struct_0(X146) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[dt_l2_lattices])]) ).
fof(i_0_143,plain,
! [X145] :
( ~ l1_lattices(X145)
| l1_struct_0(X145) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[dt_l1_lattices])]) ).
fof(i_0_144,plain,
! [X125] :
( ~ v1_xboole_0(X125)
| v1_funct_1(X125) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cc1_funct_1])]) ).
fof(i_0_145,plain,
! [X223] :
( ~ v1_xboole_0(X223)
| X223 = k1_xboole_0 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t6_boole])]) ).
fof(i_0_146,plain,
~ v1_xboole_0(esk21_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[i_0_89])]) ).
fof(i_0_147,plain,
( l3_lattices(esk27_0)
& ~ v3_struct_0(esk27_0)
& v3_lattices(esk27_0)
& v4_lattices(esk27_0)
& v5_lattices(esk27_0)
& v6_lattices(esk27_0)
& v7_lattices(esk27_0)
& v8_lattices(esk27_0)
& v9_lattices(esk27_0)
& v10_lattices(esk27_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[i_0_90])]) ).
fof(i_0_148,plain,
( l3_lattices(esk26_0)
& ~ v3_struct_0(esk26_0)
& v3_lattices(esk26_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[i_0_91])]) ).
fof(i_0_149,plain,
( l1_struct_0(esk24_0)
& ~ v3_struct_0(esk24_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[i_0_92])]) ).
fof(i_0_150,plain,
( l3_lattices(esk15_0)
& ~ v3_struct_0(esk15_0)
& v3_lattices(esk15_0)
& v4_lattices(esk15_0)
& v5_lattices(esk15_0)
& v6_lattices(esk15_0)
& v7_lattices(esk15_0)
& v8_lattices(esk15_0)
& v9_lattices(esk15_0)
& v10_lattices(esk15_0)
& v11_lattices(esk15_0)
& v13_lattices(esk15_0)
& v14_lattices(esk15_0)
& v15_lattices(esk15_0)
& v16_lattices(esk15_0)
& v17_lattices(esk15_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[i_0_93])]) ).
fof(i_0_151,plain,
( l3_lattices(esk14_0)
& ~ v3_struct_0(esk14_0)
& v3_lattices(esk14_0)
& v4_lattices(esk14_0)
& v5_lattices(esk14_0)
& v6_lattices(esk14_0)
& v7_lattices(esk14_0)
& v8_lattices(esk14_0)
& v9_lattices(esk14_0)
& v10_lattices(esk14_0)
& v13_lattices(esk14_0)
& v14_lattices(esk14_0)
& v15_lattices(esk14_0)
& v16_lattices(esk14_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[i_0_94])]) ).
fof(i_0_152,plain,
( l3_lattices(esk13_0)
& ~ v3_struct_0(esk13_0)
& v3_lattices(esk13_0)
& v4_lattices(esk13_0)
& v5_lattices(esk13_0)
& v6_lattices(esk13_0)
& v7_lattices(esk13_0)
& v8_lattices(esk13_0)
& v9_lattices(esk13_0)
& v10_lattices(esk13_0)
& v13_lattices(esk13_0)
& v14_lattices(esk13_0)
& v15_lattices(esk13_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[i_0_95])]) ).
fof(i_0_153,plain,
( l3_lattices(esk12_0)
& ~ v3_struct_0(esk12_0)
& v3_lattices(esk12_0)
& v4_lattices(esk12_0)
& v5_lattices(esk12_0)
& v6_lattices(esk12_0)
& v7_lattices(esk12_0)
& v8_lattices(esk12_0)
& v9_lattices(esk12_0)
& v10_lattices(esk12_0)
& v11_lattices(esk12_0)
& v12_lattices(esk12_0)
& v13_lattices(esk12_0)
& v14_lattices(esk12_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[i_0_96])]) ).
fof(i_0_154,plain,
l2_lattices(esk7_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[existence_l2_lattices])]) ).
fof(i_0_155,plain,
l1_struct_0(esk6_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[existence_l1_struct_0])]) ).
fof(i_0_156,plain,
l1_lattices(esk5_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[existence_l1_lattices])]) ).
fof(i_0_157,plain,
( v1_relat_1(esk22_0)
& v1_funct_1(esk22_0)
& v2_funct_1(esk22_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc3_funct_1])]) ).
fof(i_0_158,plain,
( v1_relat_1(esk19_0)
& v1_xboole_0(esk19_0)
& v1_funct_1(esk19_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc2_funct_1])]) ).
fof(i_0_159,plain,
( v1_relat_1(esk16_0)
& v1_funct_1(esk16_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc1_funct_1])]) ).
fof(i_0_160,plain,
v1_xboole_0(esk18_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc1_xboole_0])]) ).
fof(i_0_161,plain,
( l3_lattices(esk23_0)
& v3_lattices(esk23_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc3_lattices])]) ).
fof(i_0_162,plain,
l3_lattices(esk8_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[existence_l3_lattices])]) ).
cnf(i_0_163,plain,
( v1_xboole_0(X1)
| ~ v3_struct_0(g3_lattices(X1,X2,X3))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
| ~ m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
| ~ m1_relset_1(X3,k2_zfmisc_1(X1,X1),X1) ),
inference(split_conjunct,[status(thm)],[i_0_97]),
[final] ).
cnf(i_0_164,plain,
( X1 = X2
| g3_lattices(X1,X3,X4) != g3_lattices(X2,X5,X6)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
| ~ m1_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
| ~ m1_relset_1(X4,k2_zfmisc_1(X1,X1),X1) ),
inference(split_conjunct,[status(thm)],[i_0_98]),
[final] ).
cnf(i_0_165,plain,
( X1 = X2
| g3_lattices(X3,X1,X4) != g3_lattices(X5,X2,X6)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X3,X3),X3)
| ~ m1_relset_1(X1,k2_zfmisc_1(X3,X3),X3)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,k2_zfmisc_1(X3,X3),X3)
| ~ m1_relset_1(X4,k2_zfmisc_1(X3,X3),X3) ),
inference(split_conjunct,[status(thm)],[i_0_98]),
[final] ).
cnf(i_0_166,plain,
( X1 = X2
| g3_lattices(X3,X4,X1) != g3_lattices(X5,X6,X2)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,k2_zfmisc_1(X3,X3),X3)
| ~ m1_relset_1(X4,k2_zfmisc_1(X3,X3),X3)
| ~ v1_funct_1(X1)
| ~ v1_funct_2(X1,k2_zfmisc_1(X3,X3),X3)
| ~ m1_relset_1(X1,k2_zfmisc_1(X3,X3),X3) ),
inference(split_conjunct,[status(thm)],[i_0_98]),
[final] ).
cnf(i_0_167,plain,
( v3_lattices(g3_lattices(X1,X2,X3))
| v1_xboole_0(X1)
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
| ~ m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
| ~ m1_relset_1(X3,k2_zfmisc_1(X1,X1),X1) ),
inference(split_conjunct,[status(thm)],[i_0_97]),
[final] ).
cnf(i_0_168,plain,
( v3_lattices(g3_lattices(X1,X2,X3))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
| ~ m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
| ~ m1_relset_1(X3,k2_zfmisc_1(X1,X1),X1) ),
inference(split_conjunct,[status(thm)],[i_0_99]),
[final] ).
cnf(i_0_169,plain,
( l3_lattices(g3_lattices(X1,X2,X3))
| ~ v1_funct_1(X2)
| ~ v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
| ~ m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
| ~ m1_relset_1(X3,k2_zfmisc_1(X1,X1),X1) ),
inference(split_conjunct,[status(thm)],[i_0_99]),
[final] ).
cnf(i_0_170,plain,
( v3_struct_0(X1)
| v3_struct_0(X2)
| r2_lattices(X2,X5,X6)
| ~ v10_lattices(X1)
| ~ v15_lattices(X1)
| ~ v16_lattices(X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X2)
| ~ v15_lattices(X2)
| ~ v16_lattices(X2)
| ~ l3_lattices(X2)
| g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1)) != g3_lattices(u1_struct_0(X2),u2_lattices(X2),u1_lattices(X2))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X5,u1_struct_0(X2))
| ~ m1_subset_1(X6,u1_struct_0(X2))
| X3 != X5
| X4 != X6
| ~ r2_lattices(X1,X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_100]),
[final] ).
cnf(i_0_171,plain,
( X2 = k7_lattices(X1,X3)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ v11_lattices(X1)
| ~ v16_lattices(X1)
| ~ r2_lattices(X1,X2,X3)
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1)) ),
inference(cn,[status(thm)],[i_0_101]),
[final] ).
cnf(i_0_172,plain,
( v3_struct_0(X2)
| r2_lattices(X2,X1,X3)
| X1 != k7_lattices(X2,X3)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2)
| ~ v11_lattices(X2)
| ~ v16_lattices(X2)
| ~ m1_subset_1(X3,u1_struct_0(X2))
| ~ m1_subset_1(X1,u1_struct_0(X2)) ),
inference(cn,[status(thm)],[i_0_102]),
[final] ).
cnf(i_0_173,plain,
( m1_subset_1(X1,k1_zfmisc_1(k2_zfmisc_1(X2,X3)))
| ~ m2_relset_1(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_103]),
[final] ).
cnf(i_0_174,plain,
( m2_relset_1(X1,X2,X3)
| ~ m1_relset_1(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_104]),
[final] ).
cnf(i_0_175,plain,
( m1_relset_1(X1,X2,X3)
| ~ m2_relset_1(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_104]),
[final] ).
cnf(i_0_176,plain,
( v1_partfun1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v7_lattices(X1)
| ~ l1_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_105]),
[final] ).
cnf(i_0_177,plain,
( v1_partfun1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v6_lattices(X1)
| ~ l1_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_106]),
[final] ).
cnf(i_0_178,plain,
( v1_partfun1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v5_lattices(X1)
| ~ l2_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_107]),
[final] ).
cnf(i_0_179,plain,
( v1_partfun1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v4_lattices(X1)
| ~ l2_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_108]),
[final] ).
cnf(i_0_180,plain,
( v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v7_lattices(X1)
| ~ l1_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_105]),
[final] ).
cnf(i_0_181,plain,
( v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v6_lattices(X1)
| ~ l1_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_106]),
[final] ).
cnf(i_0_182,plain,
( v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v5_lattices(X1)
| ~ l2_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_107]),
[final] ).
cnf(i_0_183,plain,
( v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v4_lattices(X1)
| ~ l2_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_108]),
[final] ).
cnf(i_0_184,negated_conjecture,
g3_lattices(u1_struct_0(esk1_0),u2_lattices(esk1_0),u1_lattices(esk1_0)) = g3_lattices(u1_struct_0(esk2_0),u2_lattices(esk2_0),u1_lattices(esk2_0)),
inference(split_conjunct,[status(thm)],[i_0_109]),
[final] ).
cnf(i_0_185,plain,
( m2_relset_1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l1_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_110]),
[final] ).
cnf(i_0_186,plain,
( m2_relset_1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l2_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_111]),
[final] ).
cnf(i_0_187,plain,
( v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l1_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_110]),
[final] ).
cnf(i_0_188,plain,
( v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l2_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_111]),
[final] ).
cnf(i_0_189,plain,
( v1_relat_1(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(k2_zfmisc_1(X2,X3))) ),
inference(split_conjunct,[status(thm)],[i_0_112]),
[final] ).
cnf(i_0_190,plain,
( v3_struct_0(X1)
| m1_subset_1(k7_lattices(X1,X2),u1_struct_0(X1))
| ~ l3_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1)) ),
inference(split_conjunct,[status(thm)],[i_0_113]),
[final] ).
cnf(i_0_191,plain,
( X1 = g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
| ~ l3_lattices(X1)
| ~ v3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_114]),
[final] ).
cnf(i_0_192,plain,
m2_relset_1(esk11_2(X1,X2),X1,X2),
inference(split_conjunct,[status(thm)],[i_0_115]),
[final] ).
cnf(i_0_193,plain,
m1_relset_1(esk9_2(X1,X2),X1,X2),
inference(split_conjunct,[status(thm)],[i_0_116]),
[final] ).
cnf(i_0_194,plain,
( m1_subset_1(X1,X3)
| ~ r2_hidden(X1,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X3)) ),
inference(split_conjunct,[status(thm)],[i_0_117]),
[final] ).
cnf(i_0_195,plain,
( ~ r2_hidden(X1,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X3))
| ~ v1_xboole_0(X3) ),
inference(split_conjunct,[status(thm)],[i_0_118]),
[final] ).
cnf(i_0_196,plain,
( v10_lattices(X1)
| v3_struct_0(X1)
| ~ v4_lattices(X1)
| ~ v5_lattices(X1)
| ~ v6_lattices(X1)
| ~ v7_lattices(X1)
| ~ v8_lattices(X1)
| ~ v9_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_119]),
[final] ).
cnf(i_0_197,plain,
( v1_xboole_0(X1)
| v1_xboole_0(X2)
| ~ v1_xboole_0(k2_zfmisc_1(X1,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_120]),
[final] ).
cnf(i_0_198,plain,
( m1_subset_1(esk25_1(X1),k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ l1_struct_0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_121]),
[final] ).
cnf(i_0_199,plain,
( r1_tarski(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_122]),
[final] ).
cnf(i_0_200,plain,
( v2_binop_1(u1_lattices(X1),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v7_lattices(X1)
| ~ l1_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_105]),
[final] ).
cnf(i_0_201,plain,
( v2_binop_1(u2_lattices(X1),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v5_lattices(X1)
| ~ l2_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_107]),
[final] ).
cnf(i_0_202,plain,
( v1_binop_1(u1_lattices(X1),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v6_lattices(X1)
| ~ l1_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_106]),
[final] ).
cnf(i_0_203,plain,
( v1_binop_1(u2_lattices(X1),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v4_lattices(X1)
| ~ l2_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_108]),
[final] ).
cnf(i_0_204,plain,
( ~ r2_hidden(X1,X2)
| ~ r2_hidden(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_123]),
[final] ).
cnf(i_0_205,plain,
( m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r1_tarski(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_122]),
[final] ).
cnf(i_0_206,plain,
( v1_xboole_0(X2)
| r2_hidden(X1,X2)
| ~ m1_subset_1(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_124]),
[final] ).
cnf(i_0_207,plain,
( v17_lattices(X1)
| v3_struct_0(X1)
| ~ v11_lattices(X1)
| ~ v15_lattices(X1)
| ~ v16_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_125]),
[final] ).
cnf(i_0_208,plain,
( m1_subset_1(X1,X2)
| ~ r2_hidden(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_126]),
[final] ).
cnf(i_0_209,negated_conjecture,
k7_lattices(esk1_0,esk3_0) != k7_lattices(esk2_0,esk4_0),
inference(split_conjunct,[status(thm)],[i_0_109]),
[final] ).
cnf(i_0_210,plain,
( m1_subset_1(esk17_1(X1),k1_zfmisc_1(X1))
| v1_xboole_0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_127]),
[final] ).
cnf(i_0_211,plain,
( v12_lattices(X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v11_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_128]),
[final] ).
cnf(i_0_212,plain,
( v15_lattices(X1)
| v3_struct_0(X1)
| ~ v13_lattices(X1)
| ~ v14_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_129]),
[final] ).
cnf(i_0_213,plain,
( v9_lattices(X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v11_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_128]),
[final] ).
cnf(i_0_214,plain,
( v8_lattices(X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v11_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_128]),
[final] ).
cnf(i_0_215,plain,
( v7_lattices(X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v11_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_128]),
[final] ).
cnf(i_0_216,plain,
( v6_lattices(X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v11_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_128]),
[final] ).
cnf(i_0_217,plain,
( v5_lattices(X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v11_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_128]),
[final] ).
cnf(i_0_218,plain,
( v4_lattices(X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v11_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_128]),
[final] ).
cnf(i_0_219,plain,
( ~ r2_hidden(X1,X2)
| ~ v1_xboole_0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_130]),
[final] ).
cnf(i_0_220,plain,
( v1_relat_1(u1_lattices(X1))
| v3_struct_0(X1)
| ~ v7_lattices(X1)
| ~ l1_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_105]),
[final] ).
cnf(i_0_221,plain,
( v1_relat_1(u1_lattices(X1))
| v3_struct_0(X1)
| ~ v6_lattices(X1)
| ~ l1_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_106]),
[final] ).
cnf(i_0_222,plain,
( v1_relat_1(u2_lattices(X1))
| v3_struct_0(X1)
| ~ v5_lattices(X1)
| ~ l2_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_107]),
[final] ).
cnf(i_0_223,plain,
( v1_relat_1(u2_lattices(X1))
| v3_struct_0(X1)
| ~ v4_lattices(X1)
| ~ l2_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_108]),
[final] ).
cnf(i_0_224,plain,
( v1_funct_1(u1_lattices(X1))
| v3_struct_0(X1)
| ~ v7_lattices(X1)
| ~ l1_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_105]),
[final] ).
cnf(i_0_225,plain,
( v1_funct_1(u1_lattices(X1))
| v3_struct_0(X1)
| ~ v6_lattices(X1)
| ~ l1_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_106]),
[final] ).
cnf(i_0_226,plain,
( v1_funct_1(u2_lattices(X1))
| v3_struct_0(X1)
| ~ v5_lattices(X1)
| ~ l2_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_107]),
[final] ).
cnf(i_0_227,plain,
( v1_funct_1(u2_lattices(X1))
| v3_struct_0(X1)
| ~ v4_lattices(X1)
| ~ l2_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_108]),
[final] ).
cnf(i_0_228,plain,
( v3_struct_0(X1)
| ~ v1_xboole_0(esk25_1(X1))
| ~ l1_struct_0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_121]),
[final] ).
cnf(i_0_229,plain,
( v3_struct_0(X1)
| ~ l1_struct_0(X1)
| ~ v1_xboole_0(u1_struct_0(X1)) ),
inference(split_conjunct,[status(thm)],[i_0_131]),
[final] ).
cnf(i_0_230,plain,
m1_subset_1(esk20_1(X1),k1_zfmisc_1(X1)),
inference(split_conjunct,[status(thm)],[i_0_132]),
[final] ).
cnf(i_0_231,plain,
( v2_funct_1(X1)
| ~ v1_relat_1(X1)
| ~ v1_xboole_0(X1)
| ~ v1_funct_1(X1) ),
inference(split_conjunct,[status(thm)],[i_0_133]),
[final] ).
cnf(i_0_232,plain,
( v16_lattices(X1)
| v3_struct_0(X1)
| ~ v17_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_134]),
[final] ).
cnf(i_0_233,plain,
( v11_lattices(X1)
| v3_struct_0(X1)
| ~ v17_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_134]),
[final] ).
cnf(i_0_234,plain,
( v15_lattices(X1)
| v3_struct_0(X1)
| ~ v17_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_134]),
[final] ).
cnf(i_0_235,plain,
( v14_lattices(X1)
| v3_struct_0(X1)
| ~ v15_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_135]),
[final] ).
cnf(i_0_236,plain,
( v14_lattices(X1)
| v3_struct_0(X1)
| ~ v17_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_134]),
[final] ).
cnf(i_0_237,plain,
( v13_lattices(X1)
| v3_struct_0(X1)
| ~ v15_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_135]),
[final] ).
cnf(i_0_238,plain,
( v13_lattices(X1)
| v3_struct_0(X1)
| ~ v17_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_134]),
[final] ).
cnf(i_0_239,plain,
( v9_lattices(X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_136]),
[final] ).
cnf(i_0_240,plain,
( v8_lattices(X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_136]),
[final] ).
cnf(i_0_241,plain,
( v7_lattices(X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_136]),
[final] ).
cnf(i_0_242,plain,
( v6_lattices(X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_136]),
[final] ).
cnf(i_0_243,plain,
( v5_lattices(X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_136]),
[final] ).
cnf(i_0_244,plain,
( v4_lattices(X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_136]),
[final] ).
cnf(i_0_245,plain,
( v1_xboole_0(X1)
| ~ v1_xboole_0(esk17_1(X1)) ),
inference(split_conjunct,[status(thm)],[i_0_127]),
[final] ).
cnf(i_0_246,plain,
m1_subset_1(esk10_1(X1),X1),
inference(split_conjunct,[status(thm)],[i_0_137]),
[final] ).
cnf(i_0_247,plain,
( v1_funct_1(u1_lattices(X1))
| ~ l1_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_110]),
[final] ).
cnf(i_0_248,plain,
( v1_funct_1(u2_lattices(X1))
| ~ l2_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_111]),
[final] ).
cnf(i_0_249,plain,
~ v1_xboole_0(k1_zfmisc_1(X1)),
inference(split_conjunct,[status(thm)],[i_0_138]),
[final] ).
cnf(i_0_250,plain,
( X1 = X2
| ~ v1_xboole_0(X1)
| ~ v1_xboole_0(X2) ),
inference(split_conjunct,[status(thm)],[i_0_139]),
[final] ).
cnf(i_0_251,negated_conjecture,
m1_subset_1(esk4_0,u1_struct_0(esk2_0)),
inference(split_conjunct,[status(thm)],[i_0_109]),
[final] ).
cnf(i_0_252,negated_conjecture,
m1_subset_1(esk3_0,u1_struct_0(esk1_0)),
inference(split_conjunct,[status(thm)],[i_0_109]),
[final] ).
cnf(i_0_253,plain,
r1_tarski(X1,X1),
inference(split_conjunct,[status(thm)],[i_0_140]),
[final] ).
cnf(i_0_254,plain,
( l2_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_255,plain,
( l1_struct_0(X1)
| ~ l2_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_142]),
[final] ).
cnf(i_0_256,plain,
( l1_struct_0(X1)
| ~ l1_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_143]),
[final] ).
cnf(i_0_257,plain,
( l1_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_258,plain,
( v1_funct_1(X1)
| ~ v1_xboole_0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_144]),
[final] ).
cnf(i_0_259,plain,
v1_xboole_0(esk20_1(X1)),
inference(split_conjunct,[status(thm)],[i_0_132]),
[final] ).
cnf(i_0_260,plain,
( X1 = k1_xboole_0
| ~ v1_xboole_0(X1) ),
inference(split_conjunct,[status(thm)],[i_0_145]),
[final] ).
cnf(i_0_261,plain,
~ v1_xboole_0(esk21_0),
inference(split_conjunct,[status(thm)],[i_0_146]),
[final] ).
cnf(i_0_262,plain,
~ v3_struct_0(esk27_0),
inference(split_conjunct,[status(thm)],[i_0_147]),
[final] ).
cnf(i_0_263,plain,
~ v3_struct_0(esk26_0),
inference(split_conjunct,[status(thm)],[i_0_148]),
[final] ).
cnf(i_0_264,plain,
~ v3_struct_0(esk24_0),
inference(split_conjunct,[status(thm)],[i_0_149]),
[final] ).
cnf(i_0_265,plain,
~ v3_struct_0(esk15_0),
inference(split_conjunct,[status(thm)],[i_0_150]),
[final] ).
cnf(i_0_266,plain,
~ v3_struct_0(esk14_0),
inference(split_conjunct,[status(thm)],[i_0_151]),
[final] ).
cnf(i_0_267,plain,
~ v3_struct_0(esk13_0),
inference(split_conjunct,[status(thm)],[i_0_152]),
[final] ).
cnf(i_0_268,plain,
~ v3_struct_0(esk12_0),
inference(split_conjunct,[status(thm)],[i_0_153]),
[final] ).
cnf(i_0_269,negated_conjecture,
~ v3_struct_0(esk2_0),
inference(split_conjunct,[status(thm)],[i_0_109]),
[final] ).
cnf(i_0_270,negated_conjecture,
~ v3_struct_0(esk1_0),
inference(split_conjunct,[status(thm)],[i_0_109]),
[final] ).
cnf(i_0_271,plain,
l2_lattices(esk7_0),
inference(split_conjunct,[status(thm)],[i_0_154]),
[final] ).
cnf(i_0_272,plain,
l1_struct_0(esk24_0),
inference(split_conjunct,[status(thm)],[i_0_149]),
[final] ).
cnf(i_0_273,plain,
l1_struct_0(esk6_0),
inference(split_conjunct,[status(thm)],[i_0_155]),
[final] ).
cnf(i_0_274,plain,
l1_lattices(esk5_0),
inference(split_conjunct,[status(thm)],[i_0_156]),
[final] ).
cnf(i_0_275,plain,
v12_lattices(esk12_0),
inference(split_conjunct,[status(thm)],[i_0_153]),
[final] ).
cnf(i_0_276,plain,
v16_lattices(esk15_0),
inference(split_conjunct,[status(thm)],[i_0_150]),
[final] ).
cnf(i_0_277,plain,
v16_lattices(esk14_0),
inference(split_conjunct,[status(thm)],[i_0_151]),
[final] ).
cnf(i_0_278,plain,
v11_lattices(esk15_0),
inference(split_conjunct,[status(thm)],[i_0_150]),
[final] ).
cnf(i_0_279,plain,
v11_lattices(esk12_0),
inference(split_conjunct,[status(thm)],[i_0_153]),
[final] ).
cnf(i_0_280,plain,
v15_lattices(esk15_0),
inference(split_conjunct,[status(thm)],[i_0_150]),
[final] ).
cnf(i_0_281,plain,
v15_lattices(esk14_0),
inference(split_conjunct,[status(thm)],[i_0_151]),
[final] ).
cnf(i_0_282,plain,
v15_lattices(esk13_0),
inference(split_conjunct,[status(thm)],[i_0_152]),
[final] ).
cnf(i_0_283,plain,
v14_lattices(esk15_0),
inference(split_conjunct,[status(thm)],[i_0_150]),
[final] ).
cnf(i_0_284,plain,
v14_lattices(esk14_0),
inference(split_conjunct,[status(thm)],[i_0_151]),
[final] ).
cnf(i_0_285,plain,
v14_lattices(esk13_0),
inference(split_conjunct,[status(thm)],[i_0_152]),
[final] ).
cnf(i_0_286,plain,
v14_lattices(esk12_0),
inference(split_conjunct,[status(thm)],[i_0_153]),
[final] ).
cnf(i_0_287,plain,
v13_lattices(esk15_0),
inference(split_conjunct,[status(thm)],[i_0_150]),
[final] ).
cnf(i_0_288,plain,
v13_lattices(esk14_0),
inference(split_conjunct,[status(thm)],[i_0_151]),
[final] ).
cnf(i_0_289,plain,
v13_lattices(esk13_0),
inference(split_conjunct,[status(thm)],[i_0_152]),
[final] ).
cnf(i_0_290,plain,
v13_lattices(esk12_0),
inference(split_conjunct,[status(thm)],[i_0_153]),
[final] ).
cnf(i_0_291,plain,
v2_funct_1(esk22_0),
inference(split_conjunct,[status(thm)],[i_0_157]),
[final] ).
cnf(i_0_292,plain,
v1_relat_1(esk22_0),
inference(split_conjunct,[status(thm)],[i_0_157]),
[final] ).
cnf(i_0_293,plain,
v1_relat_1(esk19_0),
inference(split_conjunct,[status(thm)],[i_0_158]),
[final] ).
cnf(i_0_294,plain,
v1_relat_1(esk16_0),
inference(split_conjunct,[status(thm)],[i_0_159]),
[final] ).
cnf(i_0_295,plain,
v9_lattices(esk27_0),
inference(split_conjunct,[status(thm)],[i_0_147]),
[final] ).
cnf(i_0_296,plain,
v9_lattices(esk15_0),
inference(split_conjunct,[status(thm)],[i_0_150]),
[final] ).
cnf(i_0_297,plain,
v9_lattices(esk14_0),
inference(split_conjunct,[status(thm)],[i_0_151]),
[final] ).
cnf(i_0_298,plain,
v9_lattices(esk13_0),
inference(split_conjunct,[status(thm)],[i_0_152]),
[final] ).
cnf(i_0_299,plain,
v9_lattices(esk12_0),
inference(split_conjunct,[status(thm)],[i_0_153]),
[final] ).
cnf(i_0_300,plain,
v8_lattices(esk27_0),
inference(split_conjunct,[status(thm)],[i_0_147]),
[final] ).
cnf(i_0_301,plain,
v8_lattices(esk15_0),
inference(split_conjunct,[status(thm)],[i_0_150]),
[final] ).
cnf(i_0_302,plain,
v8_lattices(esk14_0),
inference(split_conjunct,[status(thm)],[i_0_151]),
[final] ).
cnf(i_0_303,plain,
v8_lattices(esk13_0),
inference(split_conjunct,[status(thm)],[i_0_152]),
[final] ).
cnf(i_0_304,plain,
v8_lattices(esk12_0),
inference(split_conjunct,[status(thm)],[i_0_153]),
[final] ).
cnf(i_0_305,plain,
v7_lattices(esk27_0),
inference(split_conjunct,[status(thm)],[i_0_147]),
[final] ).
cnf(i_0_306,plain,
v7_lattices(esk15_0),
inference(split_conjunct,[status(thm)],[i_0_150]),
[final] ).
cnf(i_0_307,plain,
v7_lattices(esk14_0),
inference(split_conjunct,[status(thm)],[i_0_151]),
[final] ).
cnf(i_0_308,plain,
v7_lattices(esk13_0),
inference(split_conjunct,[status(thm)],[i_0_152]),
[final] ).
cnf(i_0_309,plain,
v7_lattices(esk12_0),
inference(split_conjunct,[status(thm)],[i_0_153]),
[final] ).
cnf(i_0_310,plain,
v6_lattices(esk27_0),
inference(split_conjunct,[status(thm)],[i_0_147]),
[final] ).
cnf(i_0_311,plain,
v6_lattices(esk15_0),
inference(split_conjunct,[status(thm)],[i_0_150]),
[final] ).
cnf(i_0_312,plain,
v6_lattices(esk14_0),
inference(split_conjunct,[status(thm)],[i_0_151]),
[final] ).
cnf(i_0_313,plain,
v6_lattices(esk13_0),
inference(split_conjunct,[status(thm)],[i_0_152]),
[final] ).
cnf(i_0_314,plain,
v6_lattices(esk12_0),
inference(split_conjunct,[status(thm)],[i_0_153]),
[final] ).
cnf(i_0_315,plain,
v5_lattices(esk27_0),
inference(split_conjunct,[status(thm)],[i_0_147]),
[final] ).
cnf(i_0_316,plain,
v5_lattices(esk15_0),
inference(split_conjunct,[status(thm)],[i_0_150]),
[final] ).
cnf(i_0_317,plain,
v5_lattices(esk14_0),
inference(split_conjunct,[status(thm)],[i_0_151]),
[final] ).
cnf(i_0_318,plain,
v5_lattices(esk13_0),
inference(split_conjunct,[status(thm)],[i_0_152]),
[final] ).
cnf(i_0_319,plain,
v5_lattices(esk12_0),
inference(split_conjunct,[status(thm)],[i_0_153]),
[final] ).
cnf(i_0_320,plain,
v4_lattices(esk27_0),
inference(split_conjunct,[status(thm)],[i_0_147]),
[final] ).
cnf(i_0_321,plain,
v4_lattices(esk15_0),
inference(split_conjunct,[status(thm)],[i_0_150]),
[final] ).
cnf(i_0_322,plain,
v4_lattices(esk14_0),
inference(split_conjunct,[status(thm)],[i_0_151]),
[final] ).
cnf(i_0_323,plain,
v4_lattices(esk13_0),
inference(split_conjunct,[status(thm)],[i_0_152]),
[final] ).
cnf(i_0_324,plain,
v4_lattices(esk12_0),
inference(split_conjunct,[status(thm)],[i_0_153]),
[final] ).
cnf(i_0_325,plain,
v1_funct_1(esk22_0),
inference(split_conjunct,[status(thm)],[i_0_157]),
[final] ).
cnf(i_0_326,plain,
v1_funct_1(esk19_0),
inference(split_conjunct,[status(thm)],[i_0_158]),
[final] ).
cnf(i_0_327,plain,
v1_funct_1(esk16_0),
inference(split_conjunct,[status(thm)],[i_0_159]),
[final] ).
cnf(i_0_328,plain,
v1_xboole_0(esk19_0),
inference(split_conjunct,[status(thm)],[i_0_158]),
[final] ).
cnf(i_0_329,plain,
v1_xboole_0(esk18_0),
inference(split_conjunct,[status(thm)],[i_0_160]),
[final] ).
cnf(i_0_330,plain,
v1_xboole_0(k1_xboole_0),
inference(split_conjunct,[status(thm)],[fc1_xboole_0]),
[final] ).
cnf(i_0_331,plain,
v3_lattices(esk27_0),
inference(split_conjunct,[status(thm)],[i_0_147]),
[final] ).
cnf(i_0_332,plain,
v3_lattices(esk26_0),
inference(split_conjunct,[status(thm)],[i_0_148]),
[final] ).
cnf(i_0_333,plain,
v3_lattices(esk23_0),
inference(split_conjunct,[status(thm)],[i_0_161]),
[final] ).
cnf(i_0_334,plain,
v3_lattices(esk15_0),
inference(split_conjunct,[status(thm)],[i_0_150]),
[final] ).
cnf(i_0_335,plain,
v3_lattices(esk14_0),
inference(split_conjunct,[status(thm)],[i_0_151]),
[final] ).
cnf(i_0_336,plain,
v3_lattices(esk13_0),
inference(split_conjunct,[status(thm)],[i_0_152]),
[final] ).
cnf(i_0_337,plain,
v3_lattices(esk12_0),
inference(split_conjunct,[status(thm)],[i_0_153]),
[final] ).
cnf(i_0_338,plain,
l3_lattices(esk27_0),
inference(split_conjunct,[status(thm)],[i_0_147]),
[final] ).
cnf(i_0_339,plain,
l3_lattices(esk26_0),
inference(split_conjunct,[status(thm)],[i_0_148]),
[final] ).
cnf(i_0_340,plain,
l3_lattices(esk23_0),
inference(split_conjunct,[status(thm)],[i_0_161]),
[final] ).
cnf(i_0_341,plain,
l3_lattices(esk15_0),
inference(split_conjunct,[status(thm)],[i_0_150]),
[final] ).
cnf(i_0_342,plain,
l3_lattices(esk14_0),
inference(split_conjunct,[status(thm)],[i_0_151]),
[final] ).
cnf(i_0_343,plain,
l3_lattices(esk13_0),
inference(split_conjunct,[status(thm)],[i_0_152]),
[final] ).
cnf(i_0_344,plain,
l3_lattices(esk12_0),
inference(split_conjunct,[status(thm)],[i_0_153]),
[final] ).
cnf(i_0_345,plain,
l3_lattices(esk8_0),
inference(split_conjunct,[status(thm)],[i_0_162]),
[final] ).
cnf(i_0_346,negated_conjecture,
l3_lattices(esk2_0),
inference(split_conjunct,[status(thm)],[i_0_109]),
[final] ).
cnf(i_0_347,negated_conjecture,
l3_lattices(esk1_0),
inference(split_conjunct,[status(thm)],[i_0_109]),
[final] ).
cnf(i_0_348,plain,
v17_lattices(esk15_0),
inference(split_conjunct,[status(thm)],[i_0_150]),
[final] ).
cnf(i_0_349,negated_conjecture,
v17_lattices(esk2_0),
inference(split_conjunct,[status(thm)],[i_0_109]),
[final] ).
cnf(i_0_350,negated_conjecture,
v17_lattices(esk1_0),
inference(split_conjunct,[status(thm)],[i_0_109]),
[final] ).
cnf(i_0_351,plain,
v10_lattices(esk27_0),
inference(split_conjunct,[status(thm)],[i_0_147]),
[final] ).
cnf(i_0_352,plain,
v10_lattices(esk15_0),
inference(split_conjunct,[status(thm)],[i_0_150]),
[final] ).
cnf(i_0_353,plain,
v10_lattices(esk14_0),
inference(split_conjunct,[status(thm)],[i_0_151]),
[final] ).
cnf(i_0_354,plain,
v10_lattices(esk13_0),
inference(split_conjunct,[status(thm)],[i_0_152]),
[final] ).
cnf(i_0_355,plain,
v10_lattices(esk12_0),
inference(split_conjunct,[status(thm)],[i_0_153]),
[final] ).
cnf(i_0_356,negated_conjecture,
v10_lattices(esk2_0),
inference(split_conjunct,[status(thm)],[i_0_109]),
[final] ).
cnf(i_0_357,negated_conjecture,
v10_lattices(esk1_0),
inference(split_conjunct,[status(thm)],[i_0_109]),
[final] ).
cnf(i_0_358,negated_conjecture,
esk3_0 = esk4_0,
inference(split_conjunct,[status(thm)],[i_0_109]),
[final] ).
cnf(i_0_359,axiom,
X1 = X1 ).
cnf(i_0_360,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_361,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_362,axiom,
( X1 != X2
| g3_lattices(X1,X3,X4) = g3_lattices(X2,X3,X4) ) ).
cnf(i_0_363,axiom,
( X1 != X2
| g3_lattices(X3,X1,X4) = g3_lattices(X3,X2,X4) ) ).
cnf(i_0_364,axiom,
( X1 != X2
| g3_lattices(X3,X4,X1) = g3_lattices(X3,X4,X2) ) ).
cnf(i_0_365,axiom,
( X1 != X2
| k7_lattices(X1,X3) = k7_lattices(X2,X3) ) ).
cnf(i_0_366,axiom,
( X1 != X2
| k7_lattices(X3,X1) = k7_lattices(X3,X2) ) ).
cnf(i_0_367,axiom,
( X1 != X2
| ~ v1_xboole_0(X1)
| v1_xboole_0(X2) ) ).
cnf(i_0_368,axiom,
( X1 != X2
| ~ v15_lattices(X1)
| v15_lattices(X2) ) ).
cnf(i_0_369,axiom,
( X1 != X2
| ~ v16_lattices(X1)
| v16_lattices(X2) ) ).
cnf(i_0_370,axiom,
( X1 != X2
| ~ m1_subset_1(X1,X3)
| m1_subset_1(X2,X3) ) ).
cnf(i_0_371,axiom,
( X1 != X2
| ~ m1_subset_1(X3,X1)
| m1_subset_1(X3,X2) ) ).
cnf(i_0_372,axiom,
( X1 != X2
| ~ v11_lattices(X1)
| v11_lattices(X2) ) ).
cnf(i_0_373,axiom,
( X1 != X2
| ~ m2_relset_1(X1,X3,X4)
| m2_relset_1(X2,X3,X4) ) ).
cnf(i_0_374,axiom,
( X1 != X2
| ~ m2_relset_1(X3,X1,X4)
| m2_relset_1(X3,X2,X4) ) ).
cnf(i_0_375,axiom,
( X1 != X2
| ~ m2_relset_1(X3,X4,X1)
| m2_relset_1(X3,X4,X2) ) ).
cnf(i_0_376,axiom,
( X1 != X2
| ~ v1_partfun1(X1,X3,X4)
| v1_partfun1(X2,X3,X4) ) ).
cnf(i_0_377,axiom,
( X1 != X2
| ~ v1_partfun1(X3,X1,X4)
| v1_partfun1(X3,X2,X4) ) ).
cnf(i_0_378,axiom,
( X1 != X2
| ~ v1_partfun1(X3,X4,X1)
| v1_partfun1(X3,X4,X2) ) ).
cnf(i_0_379,axiom,
( X1 != X2
| ~ v7_lattices(X1)
| v7_lattices(X2) ) ).
cnf(i_0_380,axiom,
( X1 != X2
| ~ l1_lattices(X1)
| l1_lattices(X2) ) ).
cnf(i_0_381,axiom,
( X1 != X2
| ~ v6_lattices(X1)
| v6_lattices(X2) ) ).
cnf(i_0_382,axiom,
( X1 != X2
| ~ v5_lattices(X1)
| v5_lattices(X2) ) ).
cnf(i_0_383,axiom,
( X1 != X2
| ~ v3_struct_0(X1)
| v3_struct_0(X2) ) ).
cnf(i_0_384,axiom,
( X1 != X2
| ~ l2_lattices(X1)
| l2_lattices(X2) ) ).
cnf(i_0_385,axiom,
( X1 != X2
| ~ v4_lattices(X1)
| v4_lattices(X2) ) ).
cnf(i_0_386,axiom,
( X1 != X2
| ~ v1_relat_1(X1)
| v1_relat_1(X2) ) ).
cnf(i_0_387,axiom,
( X1 != X2
| ~ r2_hidden(X1,X3)
| r2_hidden(X2,X3) ) ).
cnf(i_0_388,axiom,
( X1 != X2
| ~ r2_hidden(X3,X1)
| r2_hidden(X3,X2) ) ).
cnf(i_0_389,axiom,
( X1 != X2
| ~ v8_lattices(X1)
| v8_lattices(X2) ) ).
cnf(i_0_390,axiom,
( X1 != X2
| ~ v9_lattices(X1)
| v9_lattices(X2) ) ).
cnf(i_0_391,axiom,
( X1 != X2
| ~ l1_struct_0(X1)
| l1_struct_0(X2) ) ).
cnf(i_0_392,axiom,
( X1 != X2
| ~ r1_tarski(X1,X3)
| r1_tarski(X2,X3) ) ).
cnf(i_0_393,axiom,
( X1 != X2
| ~ r1_tarski(X3,X1)
| r1_tarski(X3,X2) ) ).
cnf(i_0_394,axiom,
( X1 != X2
| ~ v2_binop_1(X1,X3)
| v2_binop_1(X2,X3) ) ).
cnf(i_0_395,axiom,
( X1 != X2
| ~ v2_binop_1(X3,X1)
| v2_binop_1(X3,X2) ) ).
cnf(i_0_396,axiom,
( X1 != X2
| ~ v1_binop_1(X1,X3)
| v1_binop_1(X2,X3) ) ).
cnf(i_0_397,axiom,
( X1 != X2
| ~ v1_binop_1(X3,X1)
| v1_binop_1(X3,X2) ) ).
cnf(i_0_398,axiom,
( X1 != X2
| ~ v1_funct_1(X1)
| v1_funct_1(X2) ) ).
cnf(i_0_399,axiom,
( X1 != X2
| ~ v17_lattices(X1)
| v17_lattices(X2) ) ).
cnf(i_0_400,axiom,
( X1 != X2
| ~ v12_lattices(X1)
| v12_lattices(X2) ) ).
cnf(i_0_401,axiom,
( X1 != X2
| ~ v13_lattices(X1)
| v13_lattices(X2) ) ).
cnf(i_0_402,axiom,
( X1 != X2
| ~ v14_lattices(X1)
| v14_lattices(X2) ) ).
cnf(i_0_403,axiom,
( X1 != X2
| ~ v2_funct_1(X1)
| v2_funct_1(X2) ) ).
cnf(i_0_404,axiom,
( X1 != X2
| ~ v1_funct_2(X1,X3,X4)
| v1_funct_2(X2,X3,X4) ) ).
cnf(i_0_405,axiom,
( X1 != X2
| ~ v1_funct_2(X3,X1,X4)
| v1_funct_2(X3,X2,X4) ) ).
cnf(i_0_406,axiom,
( X1 != X2
| ~ v1_funct_2(X3,X4,X1)
| v1_funct_2(X3,X4,X2) ) ).
cnf(i_0_407,axiom,
( X1 != X2
| ~ m1_relset_1(X1,X3,X4)
| m1_relset_1(X2,X3,X4) ) ).
cnf(i_0_408,axiom,
( X1 != X2
| ~ m1_relset_1(X3,X1,X4)
| m1_relset_1(X3,X2,X4) ) ).
cnf(i_0_409,axiom,
( X1 != X2
| ~ m1_relset_1(X3,X4,X1)
| m1_relset_1(X3,X4,X2) ) ).
cnf(i_0_410,axiom,
( X1 != X2
| ~ v3_lattices(X1)
| v3_lattices(X2) ) ).
cnf(i_0_411,axiom,
( X1 != X2
| ~ l3_lattices(X1)
| l3_lattices(X2) ) ).
cnf(i_0_412,axiom,
( X1 != X2
| ~ r2_lattices(X1,X3,X4)
| r2_lattices(X2,X3,X4) ) ).
cnf(i_0_413,axiom,
( X1 != X2
| ~ r2_lattices(X3,X1,X4)
| r2_lattices(X3,X2,X4) ) ).
cnf(i_0_414,axiom,
( X1 != X2
| ~ r2_lattices(X3,X4,X1)
| r2_lattices(X3,X4,X2) ) ).
cnf(i_0_415,axiom,
( X1 != X2
| ~ v10_lattices(X1)
| v10_lattices(X2) ) ).
cnf(i_0_421,plain,
m2_relset_1(esk9_2(X1,X2),X1,X2),
inference(scs_inference,[],[i_0_184,i_0_193,i_0_360,i_0_174]) ).
cnf(i_0_423,plain,
m1_relset_1(esk11_2(X1,X2),X1,X2),
inference(scs_inference,[],[i_0_184,i_0_192,i_0_193,i_0_360,i_0_174,i_0_175]) ).
cnf(i_0_425,plain,
v1_relat_1(esk20_1(k2_zfmisc_1(X1,X2))),
inference(scs_inference,[],[i_0_184,i_0_192,i_0_193,i_0_230,i_0_360,i_0_174,i_0_175,i_0_189]) ).
cnf(i_0_426,plain,
m1_subset_1(esk20_1(X1),k1_zfmisc_1(X1)),
inference(rename_variables,[],[i_0_230]) ).
cnf(i_0_444,plain,
m1_subset_1(esk20_1(X1),k1_zfmisc_1(X1)),
inference(rename_variables,[],[i_0_230]) ).
cnf(i_0_447,plain,
m1_subset_1(esk20_1(X1),k1_zfmisc_1(X1)),
inference(rename_variables,[],[i_0_230]) ).
cnf(i_0_506,plain,
v1_relat_1(esk10_1(k1_zfmisc_1(k2_zfmisc_1(X1,X2)))),
inference(scs_inference,[],[i_0_246,i_0_189]) ).
cnf(i_0_507,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_510,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_524,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_527,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_562,plain,
v1_xboole_0(esk20_1(X1)),
inference(rename_variables,[],[i_0_259]) ).
cnf(i_0_564,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_567,plain,
~ r2_hidden(X1,esk18_0),
inference(scs_inference,[],[i_0_329,i_0_219]) ).
cnf(i_0_569,plain,
l2_lattices(esk27_0),
inference(scs_inference,[],[i_0_338,i_0_329,i_0_219,i_0_254]) ).
cnf(i_0_571,plain,
l1_struct_0(esk27_0),
inference(scs_inference,[],[i_0_338,i_0_329,i_0_219,i_0_254,i_0_255]) ).
cnf(i_0_573,plain,
l1_lattices(esk27_0),
inference(scs_inference,[],[i_0_338,i_0_329,i_0_219,i_0_254,i_0_255,i_0_257]) ).
cnf(i_0_575,plain,
v1_funct_1(esk20_1(X1)),
inference(scs_inference,[],[i_0_338,i_0_329,i_0_259,i_0_219,i_0_254,i_0_255,i_0_257,i_0_258]) ).
cnf(i_0_577,plain,
r2_hidden(esk10_1(k1_zfmisc_1(X1)),k1_zfmisc_1(X1)),
inference(scs_inference,[],[i_0_338,i_0_246,i_0_329,i_0_249,i_0_259,i_0_219,i_0_254,i_0_255,i_0_257,i_0_258,i_0_206]) ).
cnf(i_0_578,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_580,plain,
~ r2_hidden(X1,esk20_1(esk18_0)),
inference(scs_inference,[],[i_0_338,i_0_230,i_0_246,i_0_329,i_0_249,i_0_259,i_0_219,i_0_254,i_0_255,i_0_257,i_0_258,i_0_206,i_0_195]) ).
cnf(i_0_581,plain,
m1_subset_1(esk20_1(X1),k1_zfmisc_1(X1)),
inference(rename_variables,[],[i_0_230]) ).
cnf(i_0_583,plain,
esk18_0 != k1_zfmisc_1(X1),
inference(scs_inference,[],[i_0_338,i_0_230,i_0_246,i_0_329,i_0_249,i_0_259,i_0_219,i_0_254,i_0_255,i_0_257,i_0_258,i_0_206,i_0_195,i_0_367]) ).
cnf(i_0_589,plain,
v1_xboole_0(esk20_1(X1)),
inference(rename_variables,[],[i_0_259]) ).
cnf(i_0_603,plain,
~ r2_hidden(X1,esk20_1(X2)),
inference(scs_inference,[],[i_0_259,i_0_219]) ).
cnf(i_0_605,plain,
l2_lattices(esk26_0),
inference(scs_inference,[],[i_0_339,i_0_259,i_0_219,i_0_254]) ).
cnf(i_0_607,plain,
l1_struct_0(esk26_0),
inference(scs_inference,[],[i_0_339,i_0_259,i_0_219,i_0_254,i_0_255]) ).
cnf(i_0_609,plain,
l1_lattices(esk26_0),
inference(scs_inference,[],[i_0_339,i_0_259,i_0_219,i_0_254,i_0_255,i_0_257]) ).
cnf(i_0_611,plain,
~ r2_hidden(X1,esk10_1(k1_zfmisc_1(esk20_1(X2)))),
inference(scs_inference,[],[i_0_339,i_0_246,i_0_259,i_0_219,i_0_254,i_0_255,i_0_257,i_0_195]) ).
cnf(i_0_612,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_614,plain,
esk20_1(X1) != esk21_0,
inference(scs_inference,[],[i_0_339,i_0_246,i_0_261,i_0_259,i_0_219,i_0_254,i_0_255,i_0_257,i_0_195,i_0_367]) ).
cnf(i_0_620,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_626,plain,
l2_lattices(esk23_0),
inference(scs_inference,[],[i_0_340,i_0_254]) ).
cnf(i_0_628,plain,
l1_lattices(esk23_0),
inference(scs_inference,[],[i_0_340,i_0_254,i_0_257]) ).
cnf(i_0_630,plain,
l1_struct_0(esk23_0),
inference(scs_inference,[],[i_0_340,i_0_254,i_0_257,i_0_255]) ).
cnf(i_0_632,plain,
~ r2_hidden(X1,esk10_1(k1_zfmisc_1(esk19_0))),
inference(scs_inference,[],[i_0_328,i_0_340,i_0_246,i_0_254,i_0_257,i_0_255,i_0_195]) ).
cnf(i_0_633,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_635,plain,
esk19_0 != k1_zfmisc_1(X1),
inference(scs_inference,[],[i_0_328,i_0_340,i_0_246,i_0_249,i_0_254,i_0_257,i_0_255,i_0_195,i_0_367]) ).
cnf(i_0_652,plain,
l2_lattices(esk14_0),
inference(scs_inference,[],[i_0_342,i_0_254]) ).
cnf(i_0_654,plain,
l1_lattices(esk14_0),
inference(scs_inference,[],[i_0_342,i_0_254,i_0_257]) ).
cnf(i_0_656,plain,
l1_struct_0(esk14_0),
inference(scs_inference,[],[i_0_342,i_0_254,i_0_257,i_0_255]) ).
cnf(i_0_658,plain,
~ r2_hidden(X1,esk10_1(k1_zfmisc_1(esk18_0))),
inference(scs_inference,[],[i_0_329,i_0_342,i_0_246,i_0_254,i_0_257,i_0_255,i_0_195]) ).
cnf(i_0_659,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_661,plain,
k1_xboole_0 != k1_zfmisc_1(X1),
inference(scs_inference,[],[i_0_329,i_0_330,i_0_342,i_0_246,i_0_249,i_0_254,i_0_257,i_0_255,i_0_195,i_0_367]) ).
cnf(i_0_678,plain,
l2_lattices(esk13_0),
inference(scs_inference,[],[i_0_343,i_0_254]) ).
cnf(i_0_680,plain,
l1_lattices(esk13_0),
inference(scs_inference,[],[i_0_343,i_0_254,i_0_257]) ).
cnf(i_0_682,plain,
l1_struct_0(esk13_0),
inference(scs_inference,[],[i_0_343,i_0_254,i_0_257,i_0_255]) ).
cnf(i_0_688,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_698,plain,
l2_lattices(esk8_0),
inference(scs_inference,[],[i_0_345,i_0_254]) ).
cnf(i_0_700,plain,
l1_lattices(esk8_0),
inference(scs_inference,[],[i_0_345,i_0_254,i_0_257]) ).
cnf(i_0_702,plain,
l1_struct_0(esk8_0),
inference(scs_inference,[],[i_0_345,i_0_254,i_0_257,i_0_255]) ).
cnf(i_0_704,plain,
esk20_1(X1) != k1_zfmisc_1(X2),
inference(scs_inference,[],[i_0_259,i_0_345,i_0_249,i_0_254,i_0_257,i_0_255,i_0_367]) ).
cnf(i_0_708,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_716,plain,
l2_lattices(esk12_0),
inference(scs_inference,[],[i_0_344,i_0_254]) ).
cnf(i_0_718,plain,
l1_lattices(esk12_0),
inference(scs_inference,[],[i_0_344,i_0_254,i_0_257]) ).
cnf(i_0_720,plain,
l1_struct_0(esk12_0),
inference(scs_inference,[],[i_0_344,i_0_254,i_0_257,i_0_255]) ).
cnf(i_0_729,plain,
l2_lattices(esk15_0),
inference(scs_inference,[],[i_0_341,i_0_254]) ).
cnf(i_0_731,plain,
l1_lattices(esk15_0),
inference(scs_inference,[],[i_0_341,i_0_254,i_0_257]) ).
cnf(i_0_733,plain,
l1_struct_0(esk15_0),
inference(scs_inference,[],[i_0_341,i_0_254,i_0_257,i_0_255]) ).
cnf(i_0_980,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_1034,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_1065,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_1112,plain,
v1_xboole_0(esk20_1(X1)),
inference(rename_variables,[],[i_0_259]) ).
cnf(i_0_1199,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_1206,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_1209,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_1214,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_1221,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_1227,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_1408,plain,
v1_xboole_0(esk20_1(X1)),
inference(rename_variables,[],[i_0_259]) ).
cnf(i_0_1412,plain,
v1_xboole_0(esk20_1(X1)),
inference(rename_variables,[],[i_0_259]) ).
cnf(i_0_1416,plain,
v1_xboole_0(esk20_1(X1)),
inference(rename_variables,[],[i_0_259]) ).
cnf(i_0_1420,plain,
v1_xboole_0(esk20_1(X1)),
inference(rename_variables,[],[i_0_259]) ).
cnf(i_0_1424,plain,
v1_xboole_0(esk20_1(X1)),
inference(rename_variables,[],[i_0_259]) ).
cnf(i_0_1428,plain,
v1_xboole_0(esk20_1(X1)),
inference(rename_variables,[],[i_0_259]) ).
cnf(i_0_1432,plain,
v1_xboole_0(esk20_1(X1)),
inference(rename_variables,[],[i_0_259]) ).
cnf(i_0_1436,plain,
v1_xboole_0(esk20_1(X1)),
inference(rename_variables,[],[i_0_259]) ).
cnf(i_0_1440,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_1447,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_1479,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_1485,plain,
r1_tarski(X1,X1),
inference(rename_variables,[],[i_0_253]) ).
cnf(i_0_1487,plain,
r1_tarski(X1,X1),
inference(rename_variables,[],[i_0_253]) ).
cnf(i_0_1507,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_1554,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_1557,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_1602,plain,
m2_relset_1(esk11_2(X1,X2),X1,X2),
inference(rename_variables,[],[i_0_192]) ).
cnf(i_0_1604,plain,
m2_relset_1(esk11_2(X1,X2),X1,X2),
inference(rename_variables,[],[i_0_192]) ).
cnf(i_0_1608,plain,
m1_relset_1(esk9_2(X1,X2),X1,X2),
inference(rename_variables,[],[i_0_193]) ).
cnf(i_0_1610,plain,
m1_relset_1(esk9_2(X1,X2),X1,X2),
inference(rename_variables,[],[i_0_193]) ).
cnf(i_0_1621,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_1651,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_1708,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_1730,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_1806,plain,
m1_subset_1(esk20_1(X1),k1_zfmisc_1(X1)),
inference(rename_variables,[],[i_0_230]) ).
cnf(i_0_1813,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_1881,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_1900,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_1956,plain,
r1_tarski(X1,X1),
inference(rename_variables,[],[i_0_253]) ).
cnf(i_0_1974,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_2042,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_2114,plain,
r1_tarski(X1,X1),
inference(rename_variables,[],[i_0_253]) ).
cnf(i_0_2144,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_2203,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_2217,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_2340,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_2383,plain,
r1_tarski(X1,X1),
inference(rename_variables,[],[i_0_253]) ).
cnf(i_0_2444,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_2505,plain,
r1_tarski(X1,X1),
inference(rename_variables,[],[i_0_253]) ).
cnf(i_0_2572,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_2588,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_2619,plain,
r1_tarski(X1,X1),
inference(rename_variables,[],[i_0_253]) ).
cnf(i_0_2643,plain,
m1_subset_1(esk10_1(X1),X1),
inference(rename_variables,[],[i_0_246]) ).
cnf(i_0_428,plain,
r1_tarski(esk20_1(X1),X1),
inference(scs_inference,[],[i_0_184,i_0_192,i_0_193,i_0_230,i_0_426,i_0_360,i_0_174,i_0_175,i_0_189,i_0_199]) ).
cnf(i_0_430,plain,
~ r2_hidden(X1,esk19_0),
inference(scs_inference,[],[i_0_184,i_0_192,i_0_193,i_0_230,i_0_426,i_0_328,i_0_360,i_0_174,i_0_175,i_0_189,i_0_199,i_0_219]) ).
cnf(i_0_432,plain,
l2_lattices(esk2_0),
inference(scs_inference,[],[i_0_184,i_0_346,i_0_192,i_0_193,i_0_230,i_0_426,i_0_328,i_0_360,i_0_174,i_0_175,i_0_189,i_0_199,i_0_219,i_0_254]) ).
cnf(i_0_434,plain,
l1_struct_0(esk7_0),
inference(scs_inference,[],[i_0_184,i_0_346,i_0_192,i_0_193,i_0_230,i_0_426,i_0_271,i_0_328,i_0_360,i_0_174,i_0_175,i_0_189,i_0_199,i_0_219,i_0_254,i_0_255]) ).
cnf(i_0_436,plain,
l1_struct_0(esk5_0),
inference(scs_inference,[],[i_0_184,i_0_346,i_0_192,i_0_193,i_0_230,i_0_426,i_0_271,i_0_274,i_0_328,i_0_360,i_0_174,i_0_175,i_0_189,i_0_199,i_0_219,i_0_254,i_0_255,i_0_256]) ).
cnf(i_0_438,plain,
l1_lattices(esk2_0),
inference(scs_inference,[],[i_0_184,i_0_346,i_0_192,i_0_193,i_0_230,i_0_426,i_0_271,i_0_274,i_0_328,i_0_360,i_0_174,i_0_175,i_0_189,i_0_199,i_0_219,i_0_254,i_0_255,i_0_256,i_0_257]) ).
cnf(i_0_440,plain,
v1_funct_1(esk18_0),
inference(scs_inference,[],[i_0_184,i_0_346,i_0_192,i_0_193,i_0_230,i_0_426,i_0_271,i_0_274,i_0_328,i_0_329,i_0_360,i_0_174,i_0_175,i_0_189,i_0_199,i_0_219,i_0_254,i_0_255,i_0_256,i_0_257,i_0_258]) ).
cnf(i_0_442,plain,
esk19_0 != esk21_0,
inference(scs_inference,[],[i_0_184,i_0_346,i_0_192,i_0_193,i_0_230,i_0_426,i_0_261,i_0_271,i_0_274,i_0_328,i_0_329,i_0_360,i_0_174,i_0_175,i_0_189,i_0_199,i_0_219,i_0_254,i_0_255,i_0_256,i_0_257,i_0_258,i_0_367]) ).
cnf(i_0_443,plain,
~ r2_hidden(X1,esk20_1(esk19_0)),
inference(scs_inference,[],[i_0_184,i_0_346,i_0_192,i_0_193,i_0_230,i_0_426,i_0_261,i_0_271,i_0_274,i_0_328,i_0_329,i_0_360,i_0_174,i_0_175,i_0_189,i_0_199,i_0_219,i_0_254,i_0_255,i_0_256,i_0_257,i_0_258,i_0_367,i_0_195]) ).
cnf(i_0_446,plain,
r2_hidden(esk20_1(X1),k1_zfmisc_1(X1)),
inference(scs_inference,[],[i_0_184,i_0_346,i_0_192,i_0_193,i_0_230,i_0_426,i_0_444,i_0_261,i_0_271,i_0_274,i_0_328,i_0_329,i_0_249,i_0_360,i_0_174,i_0_175,i_0_189,i_0_199,i_0_219,i_0_254,i_0_255,i_0_256,i_0_257,i_0_258,i_0_367,i_0_195,i_0_206]) ).
cnf(i_0_449,plain,
m1_subset_1(k7_lattices(esk2_0,esk4_0),u1_struct_0(esk2_0)),
inference(scs_inference,[],[i_0_184,i_0_269,i_0_346,i_0_251,i_0_192,i_0_193,i_0_230,i_0_426,i_0_444,i_0_261,i_0_271,i_0_274,i_0_328,i_0_329,i_0_249,i_0_360,i_0_174,i_0_175,i_0_189,i_0_199,i_0_219,i_0_254,i_0_255,i_0_256,i_0_257,i_0_258,i_0_367,i_0_195,i_0_206,i_0_190]) ).
cnf(i_0_451,plain,
v2_funct_1(esk19_0),
inference(scs_inference,[],[i_0_184,i_0_269,i_0_346,i_0_251,i_0_192,i_0_193,i_0_230,i_0_426,i_0_444,i_0_261,i_0_271,i_0_274,i_0_293,i_0_326,i_0_328,i_0_329,i_0_249,i_0_360,i_0_174,i_0_175,i_0_189,i_0_199,i_0_219,i_0_254,i_0_255,i_0_256,i_0_257,i_0_258,i_0_367,i_0_195,i_0_206,i_0_190,i_0_231]) ).
cnf(i_0_453,plain,
v16_lattices(esk2_0),
inference(scs_inference,[],[i_0_184,i_0_269,i_0_346,i_0_349,i_0_251,i_0_192,i_0_193,i_0_230,i_0_426,i_0_444,i_0_261,i_0_271,i_0_274,i_0_293,i_0_326,i_0_328,i_0_329,i_0_249,i_0_360,i_0_174,i_0_175,i_0_189,i_0_199,i_0_219,i_0_254,i_0_255,i_0_256,i_0_257,i_0_258,i_0_367,i_0_195,i_0_206,i_0_190,i_0_231,i_0_232]) ).
cnf(i_0_455,plain,
v11_lattices(esk2_0),
inference(scs_inference,[],[i_0_184,i_0_269,i_0_346,i_0_349,i_0_251,i_0_192,i_0_193,i_0_230,i_0_426,i_0_444,i_0_261,i_0_271,i_0_274,i_0_293,i_0_326,i_0_328,i_0_329,i_0_249,i_0_360,i_0_174,i_0_175,i_0_189,i_0_199,i_0_219,i_0_254,i_0_255,i_0_256,i_0_257,i_0_258,i_0_367,i_0_195,i_0_206,i_0_190,i_0_231,i_0_232,i_0_233]) ).
cnf(i_0_457,plain,
v15_lattices(esk2_0),
inference(scs_inference,[],[i_0_184,i_0_269,i_0_346,i_0_349,i_0_251,i_0_192,i_0_193,i_0_230,i_0_426,i_0_444,i_0_261,i_0_271,i_0_274,i_0_293,i_0_326,i_0_328,i_0_329,i_0_249,i_0_360,i_0_174,i_0_175,i_0_189,i_0_199,i_0_219,i_0_254,i_0_255,i_0_256,i_0_257,i_0_258,i_0_367,i_0_195,i_0_206,i_0_190,i_0_231,i_0_232,i_0_233,i_0_234]) ).
cnf(i_0_459,plain,
v14_lattices(esk2_0),
inference(scs_inference,[],[i_0_184,i_0_269,i_0_346,i_0_349,i_0_251,i_0_192,i_0_193,i_0_230,i_0_426,i_0_444,i_0_261,i_0_271,i_0_274,i_0_293,i_0_326,i_0_328,i_0_329,i_0_249,i_0_360,i_0_174,i_0_175,i_0_189,i_0_199,i_0_219,i_0_254,i_0_255,i_0_256,i_0_257,i_0_258,i_0_367,i_0_195,i_0_206,i_0_190,i_0_231,i_0_232,i_0_233,i_0_234,i_0_235]) ).
cnf(i_0_461,plain,
v14_lattices(esk1_0),
inference(scs_inference,[],[i_0_184,i_0_269,i_0_270,i_0_346,i_0_347,i_0_349,i_0_350,i_0_251,i_0_192,i_0_193,i_0_230,i_0_426,i_0_444,i_0_261,i_0_271,i_0_274,i_0_293,i_0_326,i_0_328,i_0_329,i_0_249,i_0_360,i_0_174,i_0_175,i_0_189,i_0_199,i_0_219,i_0_254,i_0_255,i_0_256,i_0_257,i_0_258,i_0_367,i_0_195,i_0_206,i_0_190,i_0_231,i_0_232,i_0_233,i_0_234,i_0_235,i_0_236]) ).
cnf(c_0_490,plain,
( m1_relset_1(X1,X2,X3)
| ~ m2_relset_1(X1,X2,X3) ),
i_0_175 ).
cnf(c_0_491,plain,
( m2_relset_1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l1_lattices(X1) ),
i_0_185 ).
cnf(c_0_492,plain,
( X1 = X2
| g3_lattices(X1,X3,X4) != g3_lattices(X2,X5,X6)
| ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
| ~ m1_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
| ~ m1_relset_1(X4,k2_zfmisc_1(X1,X1),X1) ),
i_0_164 ).
cnf(c_0_493,plain,
( m1_relset_1(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l1_lattices(X1) ),
inference(spm,[status(thm)],[c_0_490,c_0_491]) ).
cnf(c_0_494,plain,
( v1_funct_1(u1_lattices(X1))
| ~ l1_lattices(X1) ),
i_0_247 ).
cnf(c_0_495,plain,
( v1_funct_2(u1_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l1_lattices(X1) ),
i_0_187 ).
cnf(c_0_496,plain,
( m2_relset_1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l2_lattices(X1) ),
i_0_186 ).
cnf(c_0_497,plain,
( u1_struct_0(X1) = X2
| g3_lattices(u1_struct_0(X1),X3,u1_lattices(X1)) != g3_lattices(X2,X4,X5)
| ~ l1_lattices(X1)
| ~ m1_relset_1(X3,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ v1_funct_2(X3,k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ v1_funct_1(X3) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_492,c_0_493]),c_0_494]),c_0_495]) ).
cnf(c_0_498,plain,
( m1_relset_1(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l2_lattices(X1) ),
inference(spm,[status(thm)],[c_0_490,c_0_496]) ).
cnf(c_0_499,plain,
( v1_funct_1(u2_lattices(X1))
| ~ l2_lattices(X1) ),
i_0_248 ).
cnf(c_0_500,plain,
( v1_funct_2(u2_lattices(X1),k2_zfmisc_1(u1_struct_0(X1),u1_struct_0(X1)),u1_struct_0(X1))
| ~ l2_lattices(X1) ),
i_0_188 ).
cnf(c_0_501,plain,
( u1_struct_0(X1) = X2
| g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1)) != g3_lattices(X2,X3,X4)
| ~ l2_lattices(X1)
| ~ l1_lattices(X1) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_497,c_0_498]),c_0_499]),c_0_500]) ).
cnf(c_0_502,negated_conjecture,
g3_lattices(u1_struct_0(esk1_0),u2_lattices(esk1_0),u1_lattices(esk1_0)) = g3_lattices(u1_struct_0(esk2_0),u2_lattices(esk2_0),u1_lattices(esk2_0)),
i_0_184 ).
cnf(c_0_503,negated_conjecture,
( u1_struct_0(esk1_0) = X1
| g3_lattices(u1_struct_0(esk2_0),u2_lattices(esk2_0),u1_lattices(esk2_0)) != g3_lattices(X1,X2,X3)
| ~ l2_lattices(esk1_0)
| ~ l1_lattices(esk1_0) ),
inference(spm,[status(thm)],[c_0_501,c_0_502]) ).
cnf(c_0_504,plain,
( v3_struct_0(X1)
| v3_struct_0(X2)
| r2_lattices(X2,X3,X4)
| ~ v10_lattices(X1)
| ~ v15_lattices(X1)
| ~ v16_lattices(X1)
| ~ l3_lattices(X1)
| ~ v10_lattices(X2)
| ~ v15_lattices(X2)
| ~ v16_lattices(X2)
| ~ l3_lattices(X2)
| g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1)) != g3_lattices(u1_struct_0(X2),u2_lattices(X2),u1_lattices(X2))
| ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ m1_subset_1(X6,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X2))
| ~ m1_subset_1(X4,u1_struct_0(X2))
| X5 != X3
| X6 != X4
| ~ r2_lattices(X1,X5,X6) ),
i_0_170 ).
cnf(c_0_505,negated_conjecture,
m1_subset_1(esk3_0,u1_struct_0(esk1_0)),
i_0_252 ).
cnf(c_0_506,negated_conjecture,
esk3_0 = esk4_0,
i_0_358 ).
cnf(c_0_507,plain,
( v16_lattices(X1)
| v3_struct_0(X1)
| ~ v17_lattices(X1)
| ~ l3_lattices(X1) ),
i_0_232 ).
cnf(c_0_508,negated_conjecture,
v17_lattices(esk1_0),
i_0_350 ).
cnf(c_0_509,negated_conjecture,
l3_lattices(esk1_0),
i_0_347 ).
cnf(c_0_510,negated_conjecture,
~ v3_struct_0(esk1_0),
i_0_270 ).
cnf(c_0_511,plain,
( v15_lattices(X1)
| v3_struct_0(X1)
| ~ v17_lattices(X1)
| ~ l3_lattices(X1) ),
i_0_234 ).
cnf(c_0_512,plain,
( v3_struct_0(X1)
| r2_lattices(X1,X2,X3)
| X2 != k7_lattices(X1,X3)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ v11_lattices(X1)
| ~ v16_lattices(X1)
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1)) ),
i_0_172 ).
cnf(c_0_513,plain,
( v3_struct_0(X1)
| m1_subset_1(k7_lattices(X1,X2),u1_struct_0(X1))
| ~ l3_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1)) ),
i_0_190 ).
cnf(c_0_514,plain,
( v11_lattices(X1)
| v3_struct_0(X1)
| ~ v17_lattices(X1)
| ~ l3_lattices(X1) ),
i_0_233 ).
cnf(c_0_515,negated_conjecture,
( u1_struct_0(esk1_0) = u1_struct_0(esk2_0)
| ~ l2_lattices(esk1_0)
| ~ l1_lattices(esk1_0) ),
inference(er,[status(thm)],[c_0_503]) ).
cnf(c_0_516,plain,
( l2_lattices(X1)
| ~ l3_lattices(X1) ),
i_0_254 ).
cnf(c_0_517,plain,
( r2_lattices(X1,X2,X3)
| v3_struct_0(X1)
| v3_struct_0(X4)
| g3_lattices(u1_struct_0(X4),u2_lattices(X4),u1_lattices(X4)) != g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
| ~ m1_subset_1(X3,u1_struct_0(X4))
| ~ m1_subset_1(X2,u1_struct_0(X4))
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ v16_lattices(X1)
| ~ v16_lattices(X4)
| ~ v15_lattices(X1)
| ~ v15_lattices(X4)
| ~ v10_lattices(X1)
| ~ v10_lattices(X4)
| ~ r2_lattices(X4,X2,X3)
| ~ l3_lattices(X1)
| ~ l3_lattices(X4) ),
inference(er,[status(thm)],[inference(er,[status(thm)],[c_0_504])]) ).
cnf(c_0_518,negated_conjecture,
m1_subset_1(esk4_0,u1_struct_0(esk1_0)),
inference(rw,[status(thm)],[c_0_505,c_0_506]) ).
cnf(c_0_519,negated_conjecture,
v16_lattices(esk1_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_507,c_0_508]),c_0_509])]),c_0_510]) ).
cnf(c_0_520,negated_conjecture,
v15_lattices(esk1_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_511,c_0_508]),c_0_509])]),c_0_510]) ).
cnf(c_0_521,negated_conjecture,
v10_lattices(esk1_0),
i_0_357 ).
cnf(c_0_522,plain,
( r2_lattices(X1,k7_lattices(X1,X2),X2)
| v3_struct_0(X1)
| ~ v11_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ v16_lattices(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(csr,[status(thm)],[inference(er,[status(thm)],[c_0_512]),c_0_513]) ).
cnf(c_0_523,negated_conjecture,
v11_lattices(esk1_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_514,c_0_508]),c_0_509])]),c_0_510]) ).
cnf(c_0_524,plain,
( u1_struct_0(esk1_0) = u1_struct_0(esk2_0)
| ~ l1_lattices(esk1_0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_515,c_0_516]),c_0_509])]) ).
cnf(c_0_525,plain,
( l1_lattices(X1)
| ~ l3_lattices(X1) ),
i_0_257 ).
cnf(c_0_526,negated_conjecture,
( r2_lattices(X1,X2,esk4_0)
| v3_struct_0(X1)
| g3_lattices(u1_struct_0(esk2_0),u2_lattices(esk2_0),u1_lattices(esk2_0)) != g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
| ~ m1_subset_1(X2,u1_struct_0(esk1_0))
| ~ m1_subset_1(esk4_0,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ v16_lattices(X1)
| ~ v15_lattices(X1)
| ~ v10_lattices(X1)
| ~ r2_lattices(esk1_0,X2,esk4_0)
| ~ l3_lattices(X1) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_517,c_0_518]),c_0_502]),c_0_519]),c_0_520]),c_0_521]),c_0_509])]),c_0_510]) ).
cnf(c_0_527,negated_conjecture,
m1_subset_1(k7_lattices(esk1_0,esk4_0),u1_struct_0(esk1_0)),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_513,c_0_518]),c_0_509])]),c_0_510]) ).
cnf(c_0_528,negated_conjecture,
r2_lattices(esk1_0,k7_lattices(esk1_0,esk4_0),esk4_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_522,c_0_518]),c_0_523]),c_0_519]),c_0_521]),c_0_509])]),c_0_510]) ).
cnf(c_0_529,plain,
u1_struct_0(esk1_0) = u1_struct_0(esk2_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_524,c_0_525]),c_0_509])]) ).
cnf(c_0_530,plain,
( X1 = k7_lattices(X2,X3)
| v3_struct_0(X2)
| ~ v10_lattices(X2)
| ~ l3_lattices(X2)
| ~ v11_lattices(X2)
| ~ v16_lattices(X2)
| ~ r2_lattices(X2,X1,X3)
| ~ m1_subset_1(X3,u1_struct_0(X2))
| ~ m1_subset_1(X1,u1_struct_0(X2)) ),
i_0_171 ).
cnf(c_0_531,negated_conjecture,
m1_subset_1(esk4_0,u1_struct_0(esk2_0)),
i_0_251 ).
cnf(c_0_532,plain,
v11_lattices(esk2_0),
i_0_455 ).
cnf(c_0_533,plain,
v16_lattices(esk2_0),
i_0_453 ).
cnf(c_0_534,negated_conjecture,
v10_lattices(esk2_0),
i_0_356 ).
cnf(c_0_535,negated_conjecture,
l3_lattices(esk2_0),
i_0_346 ).
cnf(c_0_536,negated_conjecture,
~ v3_struct_0(esk2_0),
i_0_269 ).
cnf(c_0_537,negated_conjecture,
( r2_lattices(X1,k7_lattices(esk1_0,esk4_0),esk4_0)
| v3_struct_0(X1)
| g3_lattices(u1_struct_0(esk2_0),u2_lattices(esk2_0),u1_lattices(esk2_0)) != g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
| ~ m1_subset_1(k7_lattices(esk1_0,esk4_0),u1_struct_0(X1))
| ~ m1_subset_1(esk4_0,u1_struct_0(X1))
| ~ v16_lattices(X1)
| ~ v15_lattices(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_526,c_0_527]),c_0_528])]) ).
cnf(c_0_538,negated_conjecture,
m1_subset_1(k7_lattices(esk1_0,esk4_0),u1_struct_0(esk2_0)),
inference(rw,[status(thm)],[c_0_527,c_0_529]) ).
cnf(c_0_539,plain,
v15_lattices(esk2_0),
i_0_457 ).
cnf(c_0_540,negated_conjecture,
k7_lattices(esk1_0,esk3_0) != k7_lattices(esk2_0,esk4_0),
i_0_209 ).
cnf(c_0_541,negated_conjecture,
( X1 = k7_lattices(esk2_0,esk4_0)
| ~ m1_subset_1(X1,u1_struct_0(esk2_0))
| ~ r2_lattices(esk2_0,X1,esk4_0) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_530,c_0_531]),c_0_532]),c_0_533]),c_0_534]),c_0_535])]),c_0_536]) ).
cnf(c_0_542,negated_conjecture,
r2_lattices(esk2_0,k7_lattices(esk1_0,esk4_0),esk4_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_537,c_0_538]),c_0_531]),c_0_533]),c_0_539]),c_0_534]),c_0_535])]),c_0_536]) ).
cnf(c_0_543,negated_conjecture,
k7_lattices(esk1_0,esk4_0) != k7_lattices(esk2_0,esk4_0),
inference(rw,[status(thm)],[c_0_540,c_0_506]) ).
cnf(c_0_544,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_541,c_0_542]),c_0_538])]),c_0_543]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.06 % Problem : LAT296+1 : TPTP v9.2.1. Released v3.4.0.
% 0.00/0.06 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.07/0.24 % Computer : n012.cluster.edu
% 0.07/0.24 % Model : x86_64 x86_64
% 0.07/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.24 % Memory : 8042.1875MB
% 0.07/0.24 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.24 % CPULimit : 300
% 0.07/0.24 % WCLimit : 300
% 0.07/0.24 % DateTime : Mon May 4 21:03:15 EDT 2026
% 0.07/0.24 % CPUTime :
% 0.07/0.25 % start to proof: theBenchmark
% 226.05/80.69 % Version : CSE_E---1.7
% 226.05/80.69 % Problem : theBenchmark.p
% 226.05/80.69 % SZS status Theorem for theBenchmark.p
% 226.05/80.69 % SZS output start CNFRefutation
% See solution above
% 234.64/89.28 % Total time : 77.715s
%------------------------------------------------------------------------------