%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : LAT340+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 : n001.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:38:12 PM UTC 2026
% Result : Theorem 23.72s 16.01s
% Output : CNFRefutation 23.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 32
% Syntax : Number of formulae : 211 ( 40 unt; 0 def)
% Number of atoms : 940 ( 84 equ)
% Maximal formula atoms : 40 ( 4 avg)
% Number of connectives : 1127 ( 398 ~; 454 |; 192 &)
% ( 11 <=>; 72 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 33 ( 31 usr; 1 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 2 con; 0-3 aty)
% Number of variables : 299 ( 9 sgn 155 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(dt_k6_conlat_1,axiom,
! [X1] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1) )
=> ( v6_conlat_1(k6_conlat_1(X1),X1)
& ~ v7_conlat_1(k6_conlat_1(X1),X1)
& v9_conlat_1(k6_conlat_1(X1),X1)
& v11_conlat_1(k6_conlat_1(X1),X1)
& l3_conlat_1(k6_conlat_1(X1),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k6_conlat_1) ).
fof(t6_conlat_2,conjecture,
! [X1] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1) )
=> ( k3_conlat_2(X1,k2_subset_1(u1_struct_0(k11_conlat_1(X1)))) = k5_conlat_1(X1)
& k2_conlat_2(X1,k2_subset_1(u1_struct_0(k11_conlat_1(X1)))) = k6_conlat_1(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_conlat_2) ).
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(t1_conlat_2,axiom,
! [X1] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1) )
=> ( k5_lattices(k11_conlat_1(X1)) = k6_conlat_1(X1)
& k6_lattices(k11_conlat_1(X1)) = k5_conlat_1(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_conlat_2) ).
fof(dt_k11_conlat_1,axiom,
! [X1] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1) )
=> ( ~ v3_struct_0(k11_conlat_1(X1))
& v3_lattices(k11_conlat_1(X1))
& l3_lattices(k11_conlat_1(X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k11_conlat_1) ).
fof(d1_conlat_2,axiom,
! [X1] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1) )
=> ! [X2] :
( ( v6_conlat_1(X2,X1)
& ~ v7_conlat_1(X2,X1)
& v9_conlat_1(X2,X1)
& l3_conlat_1(X2,X1) )
=> k1_conlat_2(X1,X2) = X2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_conlat_2) ).
fof(dt_l1_lattices,axiom,
! [X1] :
( l1_lattices(X1)
=> l1_struct_0(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_lattices) ).
fof(fraenkel_a_2_1_lattice3,axiom,
! [X1,X2,X3] :
( ( ~ v3_struct_0(X2)
& l3_lattices(X2) )
=> ( r2_hidden(X1,a_2_1_lattice3(X2,X3))
<=> ? [X4] :
( m1_subset_1(X4,u1_struct_0(X2))
& X1 = X4
& r3_lattice3(X2,X4,X3) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fraenkel_a_2_1_lattice3) ).
fof(dt_k5_lattices,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& l1_lattices(X1) )
=> m1_subset_1(k5_lattices(X1),u1_struct_0(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k5_lattices) ).
fof(dt_k1_conlat_2,axiom,
! [X1,X2] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1)
& v6_conlat_1(X2,X1)
& ~ v7_conlat_1(X2,X1)
& v9_conlat_1(X2,X1)
& l3_conlat_1(X2,X1) )
=> m1_subset_1(k1_conlat_2(X1,X2),u1_struct_0(k11_conlat_1(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_conlat_2) ).
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(t6_boole,axiom,
! [X1] :
( v1_xboole_0(X1)
=> X1 = k1_xboole_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_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(t7_boole,axiom,
! [X1,X2] :
~ ( r2_hidden(X1,X2)
& v1_xboole_0(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(t2_tarski,axiom,
! [X1,X2] :
( ! [X3] :
( r2_hidden(X3,X1)
<=> r2_hidden(X3,X2) )
=> X1 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_tarski) ).
fof(d16_lattice3,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ! [X3] :
( r3_lattice3(X1,X2,X3)
<=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X1))
=> ( r2_hidden(X4,X3)
=> r1_lattices(X1,X2,X4) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d16_lattice3) ).
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(fc1_xboole_0,axiom,
v1_xboole_0(k1_xboole_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_xboole_0) ).
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(d24_conlat_1,axiom,
! [X1] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(k11_conlat_1(X1)))
=> k12_conlat_1(X1,X2) = X2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d24_conlat_1) ).
fof(dt_k12_conlat_1,axiom,
! [X1,X2] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1)
& m1_subset_1(X2,u1_struct_0(k11_conlat_1(X1))) )
=> ( v6_conlat_1(k12_conlat_1(X1,X2),X1)
& ~ v7_conlat_1(k12_conlat_1(X1,X2),X1)
& v9_conlat_1(k12_conlat_1(X1,X2),X1)
& l3_conlat_1(k12_conlat_1(X1,X2),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k12_conlat_1) ).
fof(t47_conlat_1,axiom,
! [X1] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(k11_conlat_1(X1)))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(k11_conlat_1(X1)))
=> ( r3_lattices(k11_conlat_1(X1),X2,X3)
<=> r2_conlat_1(X1,k12_conlat_1(X1,X2),k12_conlat_1(X1,X3)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t47_conlat_1) ).
fof(t34_conlat_1,axiom,
! [X1] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1) )
=> ! [X2] :
( ( ~ v7_conlat_1(X2,X1)
& v9_conlat_1(X2,X1)
& l3_conlat_1(X2,X1) )
=> ( r2_conlat_1(X1,X2,k5_conlat_1(X1))
& r2_conlat_1(X1,k6_conlat_1(X1),X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t34_conlat_1) ).
fof(d2_conlat_2,axiom,
! [X1] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k11_conlat_1(X1))))
=> k2_conlat_2(X1,X2) = k16_lattice3(k11_conlat_1(X1),X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_conlat_2) ).
fof(dt_k2_subset_1,axiom,
! [X1] : m1_subset_1(k2_subset_1(X1),k1_zfmisc_1(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_subset_1) ).
fof(d4_subset_1,axiom,
! [X1] : k2_subset_1(X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_subset_1) ).
fof(fc1_conlat_2,axiom,
! [X1] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1) )
=> ( ~ v3_struct_0(k11_conlat_1(X1))
& v3_lattices(k11_conlat_1(X1))
& v4_lattices(k11_conlat_1(X1))
& v5_lattices(k11_conlat_1(X1))
& v6_lattices(k11_conlat_1(X1))
& v7_lattices(k11_conlat_1(X1))
& v8_lattices(k11_conlat_1(X1))
& v9_lattices(k11_conlat_1(X1))
& v10_lattices(k11_conlat_1(X1))
& v13_lattices(k11_conlat_1(X1))
& v14_lattices(k11_conlat_1(X1))
& v15_lattices(k11_conlat_1(X1))
& v4_lattice3(k11_conlat_1(X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_conlat_2) ).
fof(redefinition_r3_lattices,axiom,
! [X1,X2,X3] :
( ( ~ v3_struct_0(X1)
& v6_lattices(X1)
& v8_lattices(X1)
& v9_lattices(X1)
& l3_lattices(X1)
& m1_subset_1(X2,u1_struct_0(X1))
& m1_subset_1(X3,u1_struct_0(X1)) )
=> ( r3_lattices(X1,X2,X3)
<=> r1_lattices(X1,X2,X3) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_r3_lattices) ).
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(d3_conlat_2,axiom,
! [X1] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k11_conlat_1(X1))))
=> k3_conlat_2(X1,X2) = k15_lattice3(k11_conlat_1(X1),X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_conlat_2) ).
fof(t51_lattice3,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v4_lattice3(X1)
& l3_lattices(X1) )
=> ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v14_lattices(X1)
& l3_lattices(X1)
& k6_lattices(X1) = k15_lattice3(X1,u1_struct_0(X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t51_lattice3) ).
fof(t34_lattice3,axiom,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v4_lattice3(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ! [X3] :
( X2 = k16_lattice3(X1,X3)
<=> ( r3_lattice3(X1,X2,X3)
& ! [X4] :
( m1_subset_1(X4,u1_struct_0(X1))
=> ( r3_lattice3(X1,X4,X3)
=> r3_lattices(X1,X4,X2) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t34_lattice3) ).
fof(c_0_32,plain,
! [X1] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1) )
=> ( v6_conlat_1(k6_conlat_1(X1),X1)
& ~ v7_conlat_1(k6_conlat_1(X1),X1)
& v9_conlat_1(k6_conlat_1(X1),X1)
& v11_conlat_1(k6_conlat_1(X1),X1)
& l3_conlat_1(k6_conlat_1(X1),X1) ) ),
inference(fof_simplification,[status(thm)],[dt_k6_conlat_1]) ).
fof(c_0_33,negated_conjecture,
~ ! [X1] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1) )
=> ( k3_conlat_2(X1,k2_subset_1(u1_struct_0(k11_conlat_1(X1)))) = k5_conlat_1(X1)
& k2_conlat_2(X1,k2_subset_1(u1_struct_0(k11_conlat_1(X1)))) = k6_conlat_1(X1) ) ),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[t6_conlat_2])]) ).
fof(c_0_34,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(c_0_35,plain,
! [X1] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1) )
=> ( k5_lattices(k11_conlat_1(X1)) = k6_conlat_1(X1)
& k6_lattices(k11_conlat_1(X1)) = k5_conlat_1(X1) ) ),
inference(fof_simplification,[status(thm)],[t1_conlat_2]) ).
fof(c_0_36,plain,
! [X1] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1) )
=> ( ~ v3_struct_0(k11_conlat_1(X1))
& v3_lattices(k11_conlat_1(X1))
& l3_lattices(k11_conlat_1(X1)) ) ),
inference(fof_simplification,[status(thm)],[dt_k11_conlat_1]) ).
fof(c_0_37,plain,
! [X1] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1) )
=> ! [X2] :
( ( v6_conlat_1(X2,X1)
& ~ v7_conlat_1(X2,X1)
& v9_conlat_1(X2,X1)
& l3_conlat_1(X2,X1) )
=> k1_conlat_2(X1,X2) = X2 ) ),
inference(fof_simplification,[status(thm)],[d1_conlat_2]) ).
fof(c_0_38,plain,
! [X273] :
( ( v6_conlat_1(k6_conlat_1(X273),X273)
| v3_conlat_1(X273)
| ~ l2_conlat_1(X273) )
& ( ~ v7_conlat_1(k6_conlat_1(X273),X273)
| v3_conlat_1(X273)
| ~ l2_conlat_1(X273) )
& ( v9_conlat_1(k6_conlat_1(X273),X273)
| v3_conlat_1(X273)
| ~ l2_conlat_1(X273) )
& ( v11_conlat_1(k6_conlat_1(X273),X273)
| v3_conlat_1(X273)
| ~ l2_conlat_1(X273) )
& ( l3_conlat_1(k6_conlat_1(X273),X273)
| v3_conlat_1(X273)
| ~ l2_conlat_1(X273) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_32])])]) ).
fof(c_0_39,negated_conjecture,
( ~ v3_conlat_1(esk1_0)
& l2_conlat_1(esk1_0)
& ( k3_conlat_2(esk1_0,k2_subset_1(u1_struct_0(k11_conlat_1(esk1_0)))) != k5_conlat_1(esk1_0)
| k2_conlat_2(esk1_0,k2_subset_1(u1_struct_0(k11_conlat_1(esk1_0)))) != k6_conlat_1(esk1_0) ) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_33])])]) ).
fof(c_0_40,plain,
! [X367] :
( ( m1_subset_1(esk30_1(X367),k1_zfmisc_1(u1_struct_0(X367)))
| v3_struct_0(X367)
| ~ l1_struct_0(X367) )
& ( ~ v1_xboole_0(esk30_1(X367))
| v3_struct_0(X367)
| ~ l1_struct_0(X367) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_34])])])]) ).
fof(c_0_41,plain,
! [X275] :
( ~ l1_lattices(X275)
| l1_struct_0(X275) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[dt_l1_lattices])]) ).
fof(c_0_42,plain,
! [X1,X2,X3] :
( ( ~ v3_struct_0(X2)
& l3_lattices(X2) )
=> ( r2_hidden(X1,a_2_1_lattice3(X2,X3))
<=> ? [X4] :
( m1_subset_1(X4,u1_struct_0(X2))
& X1 = X4
& r3_lattice3(X2,X4,X3) ) ) ),
inference(fof_simplification,[status(thm)],[fraenkel_a_2_1_lattice3]) ).
fof(c_0_43,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& l1_lattices(X1) )
=> m1_subset_1(k5_lattices(X1),u1_struct_0(X1)) ),
inference(fof_simplification,[status(thm)],[dt_k5_lattices]) ).
fof(c_0_44,plain,
! [X385] :
( ( k5_lattices(k11_conlat_1(X385)) = k6_conlat_1(X385)
| v3_conlat_1(X385)
| ~ l2_conlat_1(X385) )
& ( k6_lattices(k11_conlat_1(X385)) = k5_conlat_1(X385)
| v3_conlat_1(X385)
| ~ l2_conlat_1(X385) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_35])])]) ).
fof(c_0_45,plain,
! [X257] :
( ( ~ v3_struct_0(k11_conlat_1(X257))
| v3_conlat_1(X257)
| ~ l2_conlat_1(X257) )
& ( v3_lattices(k11_conlat_1(X257))
| v3_conlat_1(X257)
| ~ l2_conlat_1(X257) )
& ( l3_lattices(k11_conlat_1(X257))
| v3_conlat_1(X257)
| ~ l2_conlat_1(X257) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_36])])]) ).
fof(c_0_46,plain,
! [X1,X2] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1)
& v6_conlat_1(X2,X1)
& ~ v7_conlat_1(X2,X1)
& v9_conlat_1(X2,X1)
& l3_conlat_1(X2,X1) )
=> m1_subset_1(k1_conlat_2(X1,X2),u1_struct_0(k11_conlat_1(X1))) ),
inference(fof_simplification,[status(thm)],[dt_k1_conlat_2]) ).
fof(c_0_47,plain,
! [X240,X241] :
( v3_conlat_1(X240)
| ~ l2_conlat_1(X240)
| ~ v6_conlat_1(X241,X240)
| v7_conlat_1(X241,X240)
| ~ v9_conlat_1(X241,X240)
| ~ l3_conlat_1(X241,X240)
| k1_conlat_2(X240,X241) = X241 ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_37])])]) ).
cnf(c_0_48,plain,
( v9_conlat_1(k6_conlat_1(X1),X1)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_49,negated_conjecture,
l2_conlat_1(esk1_0),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
cnf(c_0_50,negated_conjecture,
~ v3_conlat_1(esk1_0),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
cnf(c_0_51,plain,
( v6_conlat_1(k6_conlat_1(X1),X1)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_52,plain,
( l3_conlat_1(k6_conlat_1(X1),X1)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_53,plain,
( m1_subset_1(esk30_1(X1),k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ l1_struct_0(X1) ),
inference(split_conjunct,[status(thm)],[c_0_40]) ).
cnf(c_0_54,plain,
( l1_struct_0(X1)
| ~ l1_lattices(X1) ),
inference(split_conjunct,[status(thm)],[c_0_41]) ).
fof(c_0_55,plain,
! [X278] :
( ( l1_lattices(X278)
| ~ l3_lattices(X278) )
& ( l2_lattices(X278)
| ~ l3_lattices(X278) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[dt_l3_lattices])])]) ).
fof(c_0_56,plain,
! [X320,X321,X322,X324,X325] :
( ( m1_subset_1(esk13_3(X320,X321,X322),u1_struct_0(X321))
| ~ r2_hidden(X320,a_2_1_lattice3(X321,X322))
| v3_struct_0(X321)
| ~ l3_lattices(X321) )
& ( X320 = esk13_3(X320,X321,X322)
| ~ r2_hidden(X320,a_2_1_lattice3(X321,X322))
| v3_struct_0(X321)
| ~ l3_lattices(X321) )
& ( r3_lattice3(X321,esk13_3(X320,X321,X322),X322)
| ~ r2_hidden(X320,a_2_1_lattice3(X321,X322))
| v3_struct_0(X321)
| ~ l3_lattices(X321) )
& ( ~ m1_subset_1(X325,u1_struct_0(X321))
| X320 != X325
| ~ r3_lattice3(X321,X325,X324)
| r2_hidden(X320,a_2_1_lattice3(X321,X324))
| v3_struct_0(X321)
| ~ l3_lattices(X321) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_42])])])])])]) ).
fof(c_0_57,plain,
! [X272] :
( v3_struct_0(X272)
| ~ l1_lattices(X272)
| m1_subset_1(k5_lattices(X272),u1_struct_0(X272)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_43])]) ).
cnf(c_0_58,plain,
( k5_lattices(k11_conlat_1(X1)) = k6_conlat_1(X1)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_44]) ).
cnf(c_0_59,plain,
( v3_conlat_1(X1)
| ~ v3_struct_0(k11_conlat_1(X1))
| ~ l2_conlat_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_45]) ).
fof(c_0_60,plain,
! [X413] :
( ~ v1_xboole_0(X413)
| X413 = k1_xboole_0 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t6_boole])]) ).
fof(c_0_61,plain,
! [X362] :
( m1_subset_1(esk26_1(X362),k1_zfmisc_1(X362))
& v1_xboole_0(esk26_1(X362)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc2_subset_1])]) ).
fof(c_0_62,plain,
! [X264,X265] :
( v3_conlat_1(X264)
| ~ l2_conlat_1(X264)
| ~ v6_conlat_1(X265,X264)
| v7_conlat_1(X265,X264)
| ~ v9_conlat_1(X265,X264)
| ~ l3_conlat_1(X265,X264)
| m1_subset_1(k1_conlat_2(X264,X265),u1_struct_0(k11_conlat_1(X264))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_46])]) ).
cnf(c_0_63,plain,
( v3_conlat_1(X1)
| v7_conlat_1(X2,X1)
| k1_conlat_2(X1,X2) = X2
| ~ l2_conlat_1(X1)
| ~ v6_conlat_1(X2,X1)
| ~ v9_conlat_1(X2,X1)
| ~ l3_conlat_1(X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_47]) ).
cnf(c_0_64,negated_conjecture,
v9_conlat_1(k6_conlat_1(esk1_0),esk1_0),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_48,c_0_49]),c_0_50]) ).
cnf(c_0_65,negated_conjecture,
v6_conlat_1(k6_conlat_1(esk1_0),esk1_0),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_51,c_0_49]),c_0_50]) ).
cnf(c_0_66,negated_conjecture,
l3_conlat_1(k6_conlat_1(esk1_0),esk1_0),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_52,c_0_49]),c_0_50]) ).
cnf(c_0_67,plain,
( m1_subset_1(esk30_1(X1),k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ l1_lattices(X1) ),
inference(spm,[status(thm)],[c_0_53,c_0_54]) ).
cnf(c_0_68,plain,
( l1_lattices(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[c_0_55]) ).
cnf(c_0_69,plain,
( l3_lattices(k11_conlat_1(X1))
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_45]) ).
fof(c_0_70,plain,
! [X414,X415] :
( ~ r2_hidden(X414,X415)
| ~ v1_xboole_0(X415) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t7_boole])]) ).
fof(c_0_71,plain,
! [X390,X391] :
( ( ~ r2_hidden(esk35_2(X390,X391),X390)
| ~ r2_hidden(esk35_2(X390,X391),X391)
| X390 = X391 )
& ( r2_hidden(esk35_2(X390,X391),X390)
| r2_hidden(esk35_2(X390,X391),X391)
| X390 = X391 ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t2_tarski])])])]) ).
cnf(c_0_72,plain,
( r2_hidden(X3,a_2_1_lattice3(X2,X4))
| v3_struct_0(X2)
| ~ m1_subset_1(X1,u1_struct_0(X2))
| X3 != X1
| ~ r3_lattice3(X2,X1,X4)
| ~ l3_lattices(X2) ),
inference(split_conjunct,[status(thm)],[c_0_56]) ).
cnf(c_0_73,plain,
( v3_struct_0(X1)
| m1_subset_1(k5_lattices(X1),u1_struct_0(X1))
| ~ l1_lattices(X1) ),
inference(split_conjunct,[status(thm)],[c_0_57]) ).
cnf(c_0_74,negated_conjecture,
k5_lattices(k11_conlat_1(esk1_0)) = k6_conlat_1(esk1_0),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_58,c_0_49]),c_0_50]) ).
cnf(c_0_75,negated_conjecture,
~ v3_struct_0(k11_conlat_1(esk1_0)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50,c_0_59]),c_0_49])]) ).
cnf(c_0_76,plain,
( X1 = k1_xboole_0
| ~ v1_xboole_0(X1) ),
inference(split_conjunct,[status(thm)],[c_0_60]) ).
cnf(c_0_77,plain,
v1_xboole_0(esk26_1(X1)),
inference(split_conjunct,[status(thm)],[c_0_61]) ).
fof(c_0_78,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ! [X3] :
( r3_lattice3(X1,X2,X3)
<=> ! [X4] :
( m1_subset_1(X4,u1_struct_0(X1))
=> ( r2_hidden(X4,X3)
=> r1_lattices(X1,X2,X4) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[d16_lattice3]) ).
cnf(c_0_79,plain,
( v3_conlat_1(X1)
| v7_conlat_1(X2,X1)
| m1_subset_1(k1_conlat_2(X1,X2),u1_struct_0(k11_conlat_1(X1)))
| ~ l2_conlat_1(X1)
| ~ v6_conlat_1(X2,X1)
| ~ v9_conlat_1(X2,X1)
| ~ l3_conlat_1(X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_62]) ).
cnf(c_0_80,negated_conjecture,
( k1_conlat_2(esk1_0,k6_conlat_1(esk1_0)) = k6_conlat_1(esk1_0)
| v7_conlat_1(k6_conlat_1(esk1_0),esk1_0) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_63,c_0_64]),c_0_65]),c_0_66]),c_0_49])]),c_0_50]) ).
fof(c_0_81,plain,
! [X410,X411,X412] :
( ~ r2_hidden(X410,X411)
| ~ m1_subset_1(X411,k1_zfmisc_1(X412))
| ~ v1_xboole_0(X412) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t5_subset])]) ).
cnf(c_0_82,plain,
( m1_subset_1(esk30_1(X1),k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ l3_lattices(X1) ),
inference(spm,[status(thm)],[c_0_67,c_0_68]) ).
cnf(c_0_83,negated_conjecture,
l3_lattices(k11_conlat_1(esk1_0)),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_69,c_0_49]),c_0_50]) ).
cnf(c_0_84,plain,
( ~ r2_hidden(X1,X2)
| ~ v1_xboole_0(X2) ),
inference(split_conjunct,[status(thm)],[c_0_70]) ).
cnf(c_0_85,plain,
( r2_hidden(esk35_2(X1,X2),X1)
| r2_hidden(esk35_2(X1,X2),X2)
| X1 = X2 ),
inference(split_conjunct,[status(thm)],[c_0_71]) ).
cnf(c_0_86,plain,
( v3_struct_0(X1)
| r2_hidden(X2,a_2_1_lattice3(X1,X3))
| ~ r3_lattice3(X1,X2,X3)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ l3_lattices(X1) ),
inference(er,[status(thm)],[c_0_72]) ).
cnf(c_0_87,negated_conjecture,
( m1_subset_1(k6_conlat_1(esk1_0),u1_struct_0(k11_conlat_1(esk1_0)))
| ~ l1_lattices(k11_conlat_1(esk1_0)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_73,c_0_74]),c_0_75]) ).
cnf(c_0_88,plain,
m1_subset_1(esk26_1(X1),k1_zfmisc_1(X1)),
inference(split_conjunct,[status(thm)],[c_0_61]) ).
cnf(c_0_89,plain,
esk26_1(X1) = k1_xboole_0,
inference(spm,[status(thm)],[c_0_76,c_0_77]) ).
fof(c_0_90,plain,
! [X234,X235,X236,X237,X238] :
( ( ~ r3_lattice3(X234,X235,X236)
| ~ m1_subset_1(X237,u1_struct_0(X234))
| ~ r2_hidden(X237,X236)
| r1_lattices(X234,X235,X237)
| ~ m1_subset_1(X235,u1_struct_0(X234))
| v3_struct_0(X234)
| ~ l3_lattices(X234) )
& ( m1_subset_1(esk2_3(X234,X235,X238),u1_struct_0(X234))
| r3_lattice3(X234,X235,X238)
| ~ m1_subset_1(X235,u1_struct_0(X234))
| v3_struct_0(X234)
| ~ l3_lattices(X234) )
& ( r2_hidden(esk2_3(X234,X235,X238),X238)
| r3_lattice3(X234,X235,X238)
| ~ m1_subset_1(X235,u1_struct_0(X234))
| v3_struct_0(X234)
| ~ l3_lattices(X234) )
& ( ~ r1_lattices(X234,X235,esk2_3(X234,X235,X238))
| r3_lattice3(X234,X235,X238)
| ~ m1_subset_1(X235,u1_struct_0(X234))
| v3_struct_0(X234)
| ~ l3_lattices(X234) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_78])])])])])]) ).
cnf(c_0_91,plain,
( v3_conlat_1(X1)
| ~ v7_conlat_1(k6_conlat_1(X1),X1)
| ~ l2_conlat_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_92,negated_conjecture,
( v7_conlat_1(k6_conlat_1(esk1_0),esk1_0)
| m1_subset_1(k6_conlat_1(esk1_0),u1_struct_0(k11_conlat_1(esk1_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_79,c_0_80]),c_0_64]),c_0_65]),c_0_66]),c_0_49])]),c_0_50]) ).
cnf(c_0_93,plain,
( ~ r2_hidden(X1,X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(X3))
| ~ v1_xboole_0(X3) ),
inference(split_conjunct,[status(thm)],[c_0_81]) ).
cnf(c_0_94,negated_conjecture,
m1_subset_1(esk30_1(k11_conlat_1(esk1_0)),k1_zfmisc_1(u1_struct_0(k11_conlat_1(esk1_0)))),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_82,c_0_83]),c_0_75]) ).
cnf(c_0_95,plain,
( X1 = X2
| r2_hidden(esk35_2(X1,X2),X2)
| ~ v1_xboole_0(X1) ),
inference(spm,[status(thm)],[c_0_84,c_0_85]) ).
cnf(c_0_96,plain,
v1_xboole_0(k1_xboole_0),
inference(split_conjunct,[status(thm)],[fc1_xboole_0]) ).
fof(c_0_97,plain,
! [X388,X389] :
( ~ m1_subset_1(X388,X389)
| v1_xboole_0(X389)
| r2_hidden(X388,X389) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t2_subset])]) ).
cnf(c_0_98,plain,
( m1_subset_1(esk13_3(X1,X2,X3),u1_struct_0(X2))
| v3_struct_0(X2)
| ~ r2_hidden(X1,a_2_1_lattice3(X2,X3))
| ~ l3_lattices(X2) ),
inference(split_conjunct,[status(thm)],[c_0_56]) ).
cnf(c_0_99,negated_conjecture,
( r2_hidden(k6_conlat_1(esk1_0),a_2_1_lattice3(k11_conlat_1(esk1_0),X1))
| ~ l1_lattices(k11_conlat_1(esk1_0))
| ~ r3_lattice3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_86,c_0_87]),c_0_83])]),c_0_75]) ).
cnf(c_0_100,plain,
m1_subset_1(k1_xboole_0,k1_zfmisc_1(X1)),
inference(rw,[status(thm)],[c_0_88,c_0_89]) ).
cnf(c_0_101,plain,
( r2_hidden(esk2_3(X1,X2,X3),X3)
| r3_lattice3(X1,X2,X3)
| v3_struct_0(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[c_0_90]) ).
cnf(c_0_102,negated_conjecture,
m1_subset_1(k6_conlat_1(esk1_0),u1_struct_0(k11_conlat_1(esk1_0))),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_91,c_0_92]),c_0_49])]),c_0_50]) ).
cnf(c_0_103,negated_conjecture,
( ~ v1_xboole_0(u1_struct_0(k11_conlat_1(esk1_0)))
| ~ r2_hidden(X1,esk30_1(k11_conlat_1(esk1_0))) ),
inference(spm,[status(thm)],[c_0_93,c_0_94]) ).
cnf(c_0_104,plain,
( k1_xboole_0 = X1
| r2_hidden(esk35_2(k1_xboole_0,X1),X1) ),
inference(spm,[status(thm)],[c_0_95,c_0_96]) ).
cnf(c_0_105,plain,
( v1_xboole_0(X2)
| r2_hidden(X1,X2)
| ~ m1_subset_1(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_97]) ).
cnf(c_0_106,negated_conjecture,
( m1_subset_1(esk13_3(k6_conlat_1(esk1_0),k11_conlat_1(esk1_0),X1),u1_struct_0(k11_conlat_1(esk1_0)))
| ~ l1_lattices(k11_conlat_1(esk1_0))
| ~ r3_lattice3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_98,c_0_99]),c_0_83])]),c_0_75]) ).
cnf(c_0_107,plain,
( ~ v1_xboole_0(X1)
| ~ r2_hidden(X2,k1_xboole_0) ),
inference(spm,[status(thm)],[c_0_93,c_0_100]) ).
cnf(c_0_108,negated_conjecture,
( r3_lattice3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1)
| r2_hidden(esk2_3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1),X1) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_101,c_0_102]),c_0_83])]),c_0_75]) ).
cnf(c_0_109,plain,
( v3_struct_0(X1)
| ~ v1_xboole_0(esk30_1(X1))
| ~ l1_struct_0(X1) ),
inference(split_conjunct,[status(thm)],[c_0_40]) ).
cnf(c_0_110,negated_conjecture,
( esk30_1(k11_conlat_1(esk1_0)) = k1_xboole_0
| ~ v1_xboole_0(u1_struct_0(k11_conlat_1(esk1_0))) ),
inference(spm,[status(thm)],[c_0_103,c_0_104]) ).
fof(c_0_111,plain,
! [X1] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(k11_conlat_1(X1)))
=> k12_conlat_1(X1,X2) = X2 ) ),
inference(fof_simplification,[status(thm)],[d24_conlat_1]) ).
fof(c_0_112,plain,
! [X1,X2] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1)
& m1_subset_1(X2,u1_struct_0(k11_conlat_1(X1))) )
=> ( v6_conlat_1(k12_conlat_1(X1,X2),X1)
& ~ v7_conlat_1(k12_conlat_1(X1,X2),X1)
& v9_conlat_1(k12_conlat_1(X1,X2),X1)
& l3_conlat_1(k12_conlat_1(X1,X2),X1) ) ),
inference(fof_simplification,[status(thm)],[dt_k12_conlat_1]) ).
cnf(c_0_113,negated_conjecture,
( v1_xboole_0(u1_struct_0(k11_conlat_1(esk1_0)))
| r2_hidden(esk13_3(k6_conlat_1(esk1_0),k11_conlat_1(esk1_0),X1),u1_struct_0(k11_conlat_1(esk1_0)))
| ~ l1_lattices(k11_conlat_1(esk1_0))
| ~ r3_lattice3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1) ),
inference(spm,[status(thm)],[c_0_105,c_0_106]) ).
cnf(c_0_114,negated_conjecture,
( r3_lattice3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),k1_xboole_0)
| ~ v1_xboole_0(X1) ),
inference(spm,[status(thm)],[c_0_107,c_0_108]) ).
cnf(c_0_115,negated_conjecture,
( ~ l1_struct_0(k11_conlat_1(esk1_0))
| ~ v1_xboole_0(u1_struct_0(k11_conlat_1(esk1_0))) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_109,c_0_110]),c_0_96])]),c_0_75]) ).
fof(c_0_116,plain,
! [X1] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(k11_conlat_1(X1)))
=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(k11_conlat_1(X1)))
=> ( r3_lattices(k11_conlat_1(X1),X2,X3)
<=> r2_conlat_1(X1,k12_conlat_1(X1,X2),k12_conlat_1(X1,X3)) ) ) ) ),
inference(fof_simplification,[status(thm)],[t47_conlat_1]) ).
fof(c_0_117,plain,
! [X244,X245] :
( v3_conlat_1(X244)
| ~ l2_conlat_1(X244)
| ~ m1_subset_1(X245,u1_struct_0(k11_conlat_1(X244)))
| k12_conlat_1(X244,X245) = X245 ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_111])])]) ).
fof(c_0_118,plain,
! [X1] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1) )
=> ! [X2] :
( ( ~ v7_conlat_1(X2,X1)
& v9_conlat_1(X2,X1)
& l3_conlat_1(X2,X1) )
=> ( r2_conlat_1(X1,X2,k5_conlat_1(X1))
& r2_conlat_1(X1,k6_conlat_1(X1),X2) ) ) ),
inference(fof_simplification,[status(thm)],[t34_conlat_1]) ).
fof(c_0_119,plain,
! [X258,X259] :
( ( v6_conlat_1(k12_conlat_1(X258,X259),X258)
| v3_conlat_1(X258)
| ~ l2_conlat_1(X258)
| ~ m1_subset_1(X259,u1_struct_0(k11_conlat_1(X258))) )
& ( ~ v7_conlat_1(k12_conlat_1(X258,X259),X258)
| v3_conlat_1(X258)
| ~ l2_conlat_1(X258)
| ~ m1_subset_1(X259,u1_struct_0(k11_conlat_1(X258))) )
& ( v9_conlat_1(k12_conlat_1(X258,X259),X258)
| v3_conlat_1(X258)
| ~ l2_conlat_1(X258)
| ~ m1_subset_1(X259,u1_struct_0(k11_conlat_1(X258))) )
& ( l3_conlat_1(k12_conlat_1(X258,X259),X258)
| v3_conlat_1(X258)
| ~ l2_conlat_1(X258)
| ~ m1_subset_1(X259,u1_struct_0(k11_conlat_1(X258))) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_112])])]) ).
cnf(c_0_120,plain,
( m1_subset_1(esk2_3(X1,X2,X3),u1_struct_0(X1))
| r3_lattice3(X1,X2,X3)
| v3_struct_0(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[c_0_90]) ).
fof(c_0_121,plain,
! [X1] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k11_conlat_1(X1))))
=> k2_conlat_2(X1,X2) = k16_lattice3(k11_conlat_1(X1),X2) ) ),
inference(fof_simplification,[status(thm)],[d2_conlat_2]) ).
fof(c_0_122,plain,
! [X268] : m1_subset_1(k2_subset_1(X268),k1_zfmisc_1(X268)),
inference(variable_rename,[status(thm)],[dt_k2_subset_1]) ).
fof(c_0_123,plain,
! [X250] : k2_subset_1(X250) = X250,
inference(variable_rename,[status(thm)],[d4_subset_1]) ).
fof(c_0_124,plain,
! [X1] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1) )
=> ( ~ v3_struct_0(k11_conlat_1(X1))
& v3_lattices(k11_conlat_1(X1))
& v4_lattices(k11_conlat_1(X1))
& v5_lattices(k11_conlat_1(X1))
& v6_lattices(k11_conlat_1(X1))
& v7_lattices(k11_conlat_1(X1))
& v8_lattices(k11_conlat_1(X1))
& v9_lattices(k11_conlat_1(X1))
& v10_lattices(k11_conlat_1(X1))
& v13_lattices(k11_conlat_1(X1))
& v14_lattices(k11_conlat_1(X1))
& v15_lattices(k11_conlat_1(X1))
& v4_lattice3(k11_conlat_1(X1)) ) ),
inference(fof_simplification,[status(thm)],[fc1_conlat_2]) ).
cnf(c_0_125,negated_conjecture,
( r2_hidden(k6_conlat_1(esk1_0),a_2_1_lattice3(k11_conlat_1(esk1_0),X1))
| ~ r3_lattice3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_86,c_0_102]),c_0_83])]),c_0_75]) ).
cnf(c_0_126,negated_conjecture,
( v1_xboole_0(u1_struct_0(k11_conlat_1(esk1_0)))
| r2_hidden(esk13_3(k6_conlat_1(esk1_0),k11_conlat_1(esk1_0),X1),u1_struct_0(k11_conlat_1(esk1_0)))
| ~ r3_lattice3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_113,c_0_68]),c_0_83])]) ).
cnf(c_0_127,negated_conjecture,
r3_lattice3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),k1_xboole_0),
inference(spm,[status(thm)],[c_0_114,c_0_96]) ).
cnf(c_0_128,negated_conjecture,
( ~ l1_lattices(k11_conlat_1(esk1_0))
| ~ v1_xboole_0(u1_struct_0(k11_conlat_1(esk1_0))) ),
inference(spm,[status(thm)],[c_0_115,c_0_54]) ).
fof(c_0_129,plain,
! [X1,X2,X3] :
( ( ~ v3_struct_0(X1)
& v6_lattices(X1)
& v8_lattices(X1)
& v9_lattices(X1)
& l3_lattices(X1)
& m1_subset_1(X2,u1_struct_0(X1))
& m1_subset_1(X3,u1_struct_0(X1)) )
=> ( r3_lattices(X1,X2,X3)
<=> r1_lattices(X1,X2,X3) ) ),
inference(fof_simplification,[status(thm)],[redefinition_r3_lattices]) ).
fof(c_0_130,plain,
! [X386,X387] :
( ~ r2_hidden(X386,X387)
| m1_subset_1(X386,X387) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t1_subset])]) ).
fof(c_0_131,plain,
! [X403,X404,X405] :
( ( ~ r3_lattices(k11_conlat_1(X403),X404,X405)
| r2_conlat_1(X403,k12_conlat_1(X403,X404),k12_conlat_1(X403,X405))
| ~ m1_subset_1(X405,u1_struct_0(k11_conlat_1(X403)))
| ~ m1_subset_1(X404,u1_struct_0(k11_conlat_1(X403)))
| v3_conlat_1(X403)
| ~ l2_conlat_1(X403) )
& ( ~ r2_conlat_1(X403,k12_conlat_1(X403,X404),k12_conlat_1(X403,X405))
| r3_lattices(k11_conlat_1(X403),X404,X405)
| ~ m1_subset_1(X405,u1_struct_0(k11_conlat_1(X403)))
| ~ m1_subset_1(X404,u1_struct_0(k11_conlat_1(X403)))
| v3_conlat_1(X403)
| ~ l2_conlat_1(X403) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_116])])])]) ).
cnf(c_0_132,plain,
( v3_conlat_1(X1)
| k12_conlat_1(X1,X2) = X2
| ~ l2_conlat_1(X1)
| ~ m1_subset_1(X2,u1_struct_0(k11_conlat_1(X1))) ),
inference(split_conjunct,[status(thm)],[c_0_117]) ).
fof(c_0_133,plain,
! [X393,X394] :
( ( r2_conlat_1(X393,X394,k5_conlat_1(X393))
| v7_conlat_1(X394,X393)
| ~ v9_conlat_1(X394,X393)
| ~ l3_conlat_1(X394,X393)
| v3_conlat_1(X393)
| ~ l2_conlat_1(X393) )
& ( r2_conlat_1(X393,k6_conlat_1(X393),X394)
| v7_conlat_1(X394,X393)
| ~ v9_conlat_1(X394,X393)
| ~ l3_conlat_1(X394,X393)
| v3_conlat_1(X393)
| ~ l2_conlat_1(X393) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_118])])])]) ).
cnf(c_0_134,plain,
( v9_conlat_1(k12_conlat_1(X1,X2),X1)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1)
| ~ m1_subset_1(X2,u1_struct_0(k11_conlat_1(X1))) ),
inference(split_conjunct,[status(thm)],[c_0_119]) ).
cnf(c_0_135,negated_conjecture,
( r3_lattice3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1)
| m1_subset_1(esk2_3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1),u1_struct_0(k11_conlat_1(esk1_0))) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_120,c_0_102]),c_0_83])]),c_0_75]) ).
cnf(c_0_136,plain,
( l3_conlat_1(k12_conlat_1(X1,X2),X1)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1)
| ~ m1_subset_1(X2,u1_struct_0(k11_conlat_1(X1))) ),
inference(split_conjunct,[status(thm)],[c_0_119]) ).
cnf(c_0_137,plain,
( v3_conlat_1(X1)
| ~ v7_conlat_1(k12_conlat_1(X1,X2),X1)
| ~ l2_conlat_1(X1)
| ~ m1_subset_1(X2,u1_struct_0(k11_conlat_1(X1))) ),
inference(split_conjunct,[status(thm)],[c_0_119]) ).
fof(c_0_138,plain,
! [X246,X247] :
( v3_conlat_1(X246)
| ~ l2_conlat_1(X246)
| ~ m1_subset_1(X247,k1_zfmisc_1(u1_struct_0(k11_conlat_1(X246))))
| k2_conlat_2(X246,X247) = k16_lattice3(k11_conlat_1(X246),X247) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_121])])]) ).
cnf(c_0_139,plain,
m1_subset_1(k2_subset_1(X1),k1_zfmisc_1(X1)),
inference(split_conjunct,[status(thm)],[c_0_122]) ).
cnf(c_0_140,plain,
k2_subset_1(X1) = X1,
inference(split_conjunct,[status(thm)],[c_0_123]) ).
fof(c_0_141,plain,
! [X1] :
( ( ~ v3_conlat_1(X1)
& l2_conlat_1(X1) )
=> ! [X2] :
( m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k11_conlat_1(X1))))
=> k3_conlat_2(X1,X2) = k15_lattice3(k11_conlat_1(X1),X2) ) ),
inference(fof_simplification,[status(thm)],[d3_conlat_2]) ).
fof(c_0_142,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v4_lattice3(X1)
& l3_lattices(X1) )
=> ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v14_lattices(X1)
& l3_lattices(X1)
& k6_lattices(X1) = k15_lattice3(X1,u1_struct_0(X1)) ) ),
inference(fof_simplification,[status(thm)],[t51_lattice3]) ).
fof(c_0_143,plain,
! [X305] :
( ( ~ v3_struct_0(k11_conlat_1(X305))
| v3_conlat_1(X305)
| ~ l2_conlat_1(X305) )
& ( v3_lattices(k11_conlat_1(X305))
| v3_conlat_1(X305)
| ~ l2_conlat_1(X305) )
& ( v4_lattices(k11_conlat_1(X305))
| v3_conlat_1(X305)
| ~ l2_conlat_1(X305) )
& ( v5_lattices(k11_conlat_1(X305))
| v3_conlat_1(X305)
| ~ l2_conlat_1(X305) )
& ( v6_lattices(k11_conlat_1(X305))
| v3_conlat_1(X305)
| ~ l2_conlat_1(X305) )
& ( v7_lattices(k11_conlat_1(X305))
| v3_conlat_1(X305)
| ~ l2_conlat_1(X305) )
& ( v8_lattices(k11_conlat_1(X305))
| v3_conlat_1(X305)
| ~ l2_conlat_1(X305) )
& ( v9_lattices(k11_conlat_1(X305))
| v3_conlat_1(X305)
| ~ l2_conlat_1(X305) )
& ( v10_lattices(k11_conlat_1(X305))
| v3_conlat_1(X305)
| ~ l2_conlat_1(X305) )
& ( v13_lattices(k11_conlat_1(X305))
| v3_conlat_1(X305)
| ~ l2_conlat_1(X305) )
& ( v14_lattices(k11_conlat_1(X305))
| v3_conlat_1(X305)
| ~ l2_conlat_1(X305) )
& ( v15_lattices(k11_conlat_1(X305))
| v3_conlat_1(X305)
| ~ l2_conlat_1(X305) )
& ( v4_lattice3(k11_conlat_1(X305))
| v3_conlat_1(X305)
| ~ l2_conlat_1(X305) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_124])])]) ).
cnf(c_0_144,plain,
( r1_lattices(X1,X2,X4)
| v3_struct_0(X1)
| ~ r3_lattice3(X1,X2,X3)
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ r2_hidden(X4,X3)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[c_0_90]) ).
cnf(c_0_145,negated_conjecture,
( m1_subset_1(esk13_3(k6_conlat_1(esk1_0),k11_conlat_1(esk1_0),X1),u1_struct_0(k11_conlat_1(esk1_0)))
| ~ r3_lattice3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_98,c_0_125]),c_0_83])]),c_0_75]) ).
cnf(c_0_146,negated_conjecture,
( v1_xboole_0(u1_struct_0(k11_conlat_1(esk1_0)))
| r2_hidden(esk13_3(k6_conlat_1(esk1_0),k11_conlat_1(esk1_0),k1_xboole_0),u1_struct_0(k11_conlat_1(esk1_0))) ),
inference(spm,[status(thm)],[c_0_126,c_0_127]) ).
cnf(c_0_147,negated_conjecture,
~ v1_xboole_0(u1_struct_0(k11_conlat_1(esk1_0))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_128,c_0_68]),c_0_83])]) ).
fof(c_0_148,plain,
! [X378,X379,X380] :
( ( ~ r3_lattices(X378,X379,X380)
| r1_lattices(X378,X379,X380)
| v3_struct_0(X378)
| ~ v6_lattices(X378)
| ~ v8_lattices(X378)
| ~ v9_lattices(X378)
| ~ l3_lattices(X378)
| ~ m1_subset_1(X379,u1_struct_0(X378))
| ~ m1_subset_1(X380,u1_struct_0(X378)) )
& ( ~ r1_lattices(X378,X379,X380)
| r3_lattices(X378,X379,X380)
| v3_struct_0(X378)
| ~ v6_lattices(X378)
| ~ v8_lattices(X378)
| ~ v9_lattices(X378)
| ~ l3_lattices(X378)
| ~ m1_subset_1(X379,u1_struct_0(X378))
| ~ m1_subset_1(X380,u1_struct_0(X378)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_129])])]) ).
cnf(c_0_149,plain,
( m1_subset_1(X1,X2)
| ~ r2_hidden(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_130]) ).
cnf(c_0_150,plain,
( r3_lattices(k11_conlat_1(X1),X2,X3)
| v3_conlat_1(X1)
| ~ r2_conlat_1(X1,k12_conlat_1(X1,X2),k12_conlat_1(X1,X3))
| ~ m1_subset_1(X3,u1_struct_0(k11_conlat_1(X1)))
| ~ m1_subset_1(X2,u1_struct_0(k11_conlat_1(X1)))
| ~ l2_conlat_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_131]) ).
cnf(c_0_151,negated_conjecture,
k12_conlat_1(esk1_0,k6_conlat_1(esk1_0)) = k6_conlat_1(esk1_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_132,c_0_102]),c_0_49])]),c_0_50]) ).
cnf(c_0_152,plain,
( r2_conlat_1(X1,k6_conlat_1(X1),X2)
| v7_conlat_1(X2,X1)
| v3_conlat_1(X1)
| ~ v9_conlat_1(X2,X1)
| ~ l3_conlat_1(X2,X1)
| ~ l2_conlat_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_133]) ).
cnf(c_0_153,negated_conjecture,
( v9_conlat_1(k12_conlat_1(esk1_0,esk2_3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1)),esk1_0)
| r3_lattice3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_134,c_0_135]),c_0_49])]),c_0_50]) ).
cnf(c_0_154,negated_conjecture,
( r3_lattice3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1)
| l3_conlat_1(k12_conlat_1(esk1_0,esk2_3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1)),esk1_0) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_136,c_0_135]),c_0_49])]),c_0_50]) ).
cnf(c_0_155,negated_conjecture,
( r3_lattice3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1)
| ~ v7_conlat_1(k12_conlat_1(esk1_0,esk2_3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1)),esk1_0) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_137,c_0_135]),c_0_49])]),c_0_50]) ).
cnf(c_0_156,plain,
( v3_conlat_1(X1)
| k2_conlat_2(X1,X2) = k16_lattice3(k11_conlat_1(X1),X2)
| ~ l2_conlat_1(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k11_conlat_1(X1)))) ),
inference(split_conjunct,[status(thm)],[c_0_138]) ).
cnf(c_0_157,plain,
m1_subset_1(X1,k1_zfmisc_1(X1)),
inference(rw,[status(thm)],[c_0_139,c_0_140]) ).
fof(c_0_158,plain,
! [X248,X249] :
( v3_conlat_1(X248)
| ~ l2_conlat_1(X248)
| ~ m1_subset_1(X249,k1_zfmisc_1(u1_struct_0(k11_conlat_1(X248))))
| k3_conlat_2(X248,X249) = k15_lattice3(k11_conlat_1(X248),X249) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_141])])]) ).
fof(c_0_159,plain,
! [X409] :
( ( ~ v3_struct_0(X409)
| v3_struct_0(X409)
| ~ v10_lattices(X409)
| ~ v4_lattice3(X409)
| ~ l3_lattices(X409) )
& ( v10_lattices(X409)
| v3_struct_0(X409)
| ~ v10_lattices(X409)
| ~ v4_lattice3(X409)
| ~ l3_lattices(X409) )
& ( v14_lattices(X409)
| v3_struct_0(X409)
| ~ v10_lattices(X409)
| ~ v4_lattice3(X409)
| ~ l3_lattices(X409) )
& ( l3_lattices(X409)
| v3_struct_0(X409)
| ~ v10_lattices(X409)
| ~ v4_lattice3(X409)
| ~ l3_lattices(X409) )
& ( k6_lattices(X409) = k15_lattice3(X409,u1_struct_0(X409))
| v3_struct_0(X409)
| ~ v10_lattices(X409)
| ~ v4_lattice3(X409)
| ~ l3_lattices(X409) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_142])])]) ).
cnf(c_0_160,plain,
( v4_lattice3(k11_conlat_1(X1))
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_143]) ).
cnf(c_0_161,plain,
( k6_lattices(k11_conlat_1(X1)) = k5_conlat_1(X1)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_44]) ).
cnf(c_0_162,plain,
( v10_lattices(k11_conlat_1(X1))
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_143]) ).
cnf(c_0_163,plain,
( v9_lattices(k11_conlat_1(X1))
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_143]) ).
cnf(c_0_164,plain,
( v8_lattices(k11_conlat_1(X1))
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_143]) ).
cnf(c_0_165,plain,
( v6_lattices(k11_conlat_1(X1))
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_143]) ).
cnf(c_0_166,negated_conjecture,
( r1_lattices(k11_conlat_1(esk1_0),X1,esk13_3(k6_conlat_1(esk1_0),k11_conlat_1(esk1_0),X2))
| ~ r3_lattice3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X2)
| ~ r3_lattice3(k11_conlat_1(esk1_0),X1,X3)
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(esk1_0)))
| ~ r2_hidden(esk13_3(k6_conlat_1(esk1_0),k11_conlat_1(esk1_0),X2),X3) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_144,c_0_145]),c_0_83])]),c_0_75]) ).
cnf(c_0_167,negated_conjecture,
r2_hidden(esk13_3(k6_conlat_1(esk1_0),k11_conlat_1(esk1_0),k1_xboole_0),u1_struct_0(k11_conlat_1(esk1_0))),
inference(sr,[status(thm)],[c_0_146,c_0_147]) ).
cnf(c_0_168,plain,
( X1 = esk13_3(X1,X2,X3)
| v3_struct_0(X2)
| ~ r2_hidden(X1,a_2_1_lattice3(X2,X3))
| ~ l3_lattices(X2) ),
inference(split_conjunct,[status(thm)],[c_0_56]) ).
fof(c_0_169,plain,
! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& v4_lattice3(X1)
& l3_lattices(X1) )
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X1))
=> ! [X3] :
( X2 = k16_lattice3(X1,X3)
<=> ( r3_lattice3(X1,X2,X3)
& ! [X4] :
( m1_subset_1(X4,u1_struct_0(X1))
=> ( r3_lattice3(X1,X4,X3)
=> r3_lattices(X1,X4,X2) ) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[t34_lattice3]) ).
cnf(c_0_170,plain,
( r1_lattices(X1,X2,X3)
| v3_struct_0(X1)
| ~ r3_lattices(X1,X2,X3)
| ~ v6_lattices(X1)
| ~ v8_lattices(X1)
| ~ v9_lattices(X1)
| ~ l3_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_148]) ).
cnf(c_0_171,negated_conjecture,
( r3_lattice3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1)
| m1_subset_1(esk2_3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1),X1) ),
inference(spm,[status(thm)],[c_0_149,c_0_108]) ).
cnf(c_0_172,negated_conjecture,
( r3_lattices(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1)
| ~ r2_conlat_1(esk1_0,k6_conlat_1(esk1_0),k12_conlat_1(esk1_0,X1))
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(esk1_0))) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_150,c_0_151]),c_0_102]),c_0_49])]),c_0_50]) ).
cnf(c_0_173,negated_conjecture,
( r2_conlat_1(esk1_0,k6_conlat_1(esk1_0),k12_conlat_1(esk1_0,esk2_3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1)))
| r3_lattice3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_152,c_0_153]),c_0_49])]),c_0_50]),c_0_154]),c_0_155]) ).
cnf(c_0_174,negated_conjecture,
( k3_conlat_2(esk1_0,k2_subset_1(u1_struct_0(k11_conlat_1(esk1_0)))) != k5_conlat_1(esk1_0)
| k2_conlat_2(esk1_0,k2_subset_1(u1_struct_0(k11_conlat_1(esk1_0)))) != k6_conlat_1(esk1_0) ),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
cnf(c_0_175,plain,
( k2_conlat_2(X1,u1_struct_0(k11_conlat_1(X1))) = k16_lattice3(k11_conlat_1(X1),u1_struct_0(k11_conlat_1(X1)))
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(spm,[status(thm)],[c_0_156,c_0_157]) ).
cnf(c_0_176,plain,
( v3_conlat_1(X1)
| k3_conlat_2(X1,X2) = k15_lattice3(k11_conlat_1(X1),X2)
| ~ l2_conlat_1(X1)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k11_conlat_1(X1)))) ),
inference(split_conjunct,[status(thm)],[c_0_158]) ).
cnf(c_0_177,plain,
( k6_lattices(X1) = k15_lattice3(X1,u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ v4_lattice3(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[c_0_159]) ).
cnf(c_0_178,negated_conjecture,
v4_lattice3(k11_conlat_1(esk1_0)),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_160,c_0_49]),c_0_50]) ).
cnf(c_0_179,negated_conjecture,
k6_lattices(k11_conlat_1(esk1_0)) = k5_conlat_1(esk1_0),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_161,c_0_49]),c_0_50]) ).
cnf(c_0_180,negated_conjecture,
v10_lattices(k11_conlat_1(esk1_0)),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_162,c_0_49]),c_0_50]) ).
cnf(c_0_181,plain,
( r3_lattices(X1,X2,X3)
| v3_struct_0(X1)
| ~ r1_lattices(X1,X2,X3)
| ~ v6_lattices(X1)
| ~ v8_lattices(X1)
| ~ v9_lattices(X1)
| ~ l3_lattices(X1)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_148]) ).
cnf(c_0_182,negated_conjecture,
v9_lattices(k11_conlat_1(esk1_0)),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_163,c_0_49]),c_0_50]) ).
cnf(c_0_183,negated_conjecture,
v8_lattices(k11_conlat_1(esk1_0)),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_164,c_0_49]),c_0_50]) ).
cnf(c_0_184,negated_conjecture,
v6_lattices(k11_conlat_1(esk1_0)),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_165,c_0_49]),c_0_50]) ).
cnf(c_0_185,negated_conjecture,
( r1_lattices(k11_conlat_1(esk1_0),X1,esk13_3(k6_conlat_1(esk1_0),k11_conlat_1(esk1_0),k1_xboole_0))
| ~ r3_lattice3(k11_conlat_1(esk1_0),X1,u1_struct_0(k11_conlat_1(esk1_0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(esk1_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_166,c_0_167]),c_0_127])]) ).
cnf(c_0_186,negated_conjecture,
( esk13_3(k6_conlat_1(esk1_0),k11_conlat_1(esk1_0),X1) = k6_conlat_1(esk1_0)
| ~ r3_lattice3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_168,c_0_125]),c_0_83])]),c_0_75]) ).
fof(c_0_187,plain,
! [X395,X396,X397,X398,X399] :
( ( r3_lattice3(X395,X396,X397)
| X396 != k16_lattice3(X395,X397)
| ~ m1_subset_1(X396,u1_struct_0(X395))
| v3_struct_0(X395)
| ~ v10_lattices(X395)
| ~ v4_lattice3(X395)
| ~ l3_lattices(X395) )
& ( ~ m1_subset_1(X398,u1_struct_0(X395))
| ~ r3_lattice3(X395,X398,X397)
| r3_lattices(X395,X398,X396)
| X396 != k16_lattice3(X395,X397)
| ~ m1_subset_1(X396,u1_struct_0(X395))
| v3_struct_0(X395)
| ~ v10_lattices(X395)
| ~ v4_lattice3(X395)
| ~ l3_lattices(X395) )
& ( m1_subset_1(esk36_3(X395,X396,X399),u1_struct_0(X395))
| ~ r3_lattice3(X395,X396,X399)
| X396 = k16_lattice3(X395,X399)
| ~ m1_subset_1(X396,u1_struct_0(X395))
| v3_struct_0(X395)
| ~ v10_lattices(X395)
| ~ v4_lattice3(X395)
| ~ l3_lattices(X395) )
& ( r3_lattice3(X395,esk36_3(X395,X396,X399),X399)
| ~ r3_lattice3(X395,X396,X399)
| X396 = k16_lattice3(X395,X399)
| ~ m1_subset_1(X396,u1_struct_0(X395))
| v3_struct_0(X395)
| ~ v10_lattices(X395)
| ~ v4_lattice3(X395)
| ~ l3_lattices(X395) )
& ( ~ r3_lattices(X395,esk36_3(X395,X396,X399),X396)
| ~ r3_lattice3(X395,X396,X399)
| X396 = k16_lattice3(X395,X399)
| ~ m1_subset_1(X396,u1_struct_0(X395))
| v3_struct_0(X395)
| ~ v10_lattices(X395)
| ~ v4_lattice3(X395)
| ~ l3_lattices(X395) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_169])])])])])]) ).
cnf(c_0_188,negated_conjecture,
( r1_lattices(X1,X2,esk2_3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),u1_struct_0(X1)))
| r3_lattice3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ r3_lattices(X1,X2,esk2_3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),u1_struct_0(X1)))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ v9_lattices(X1)
| ~ v8_lattices(X1)
| ~ v6_lattices(X1)
| ~ l3_lattices(X1) ),
inference(spm,[status(thm)],[c_0_170,c_0_171]) ).
cnf(c_0_189,negated_conjecture,
( r3_lattices(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),esk2_3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1))
| r3_lattice3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_172,c_0_173]),c_0_135]) ).
cnf(c_0_190,negated_conjecture,
( k3_conlat_2(esk1_0,u1_struct_0(k11_conlat_1(esk1_0))) != k5_conlat_1(esk1_0)
| k2_conlat_2(esk1_0,u1_struct_0(k11_conlat_1(esk1_0))) != k6_conlat_1(esk1_0) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_174,c_0_140]),c_0_140]) ).
cnf(c_0_191,negated_conjecture,
k2_conlat_2(esk1_0,u1_struct_0(k11_conlat_1(esk1_0))) = k16_lattice3(k11_conlat_1(esk1_0),u1_struct_0(k11_conlat_1(esk1_0))),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_175,c_0_49]),c_0_50]) ).
cnf(c_0_192,plain,
( k15_lattice3(k11_conlat_1(X1),u1_struct_0(k11_conlat_1(X1))) = k3_conlat_2(X1,u1_struct_0(k11_conlat_1(X1)))
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(spm,[status(thm)],[c_0_176,c_0_157]) ).
cnf(c_0_193,negated_conjecture,
k15_lattice3(k11_conlat_1(esk1_0),u1_struct_0(k11_conlat_1(esk1_0))) = k5_conlat_1(esk1_0),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_177,c_0_178]),c_0_179]),c_0_180]),c_0_83])]),c_0_75]) ).
cnf(c_0_194,negated_conjecture,
( r3_lattices(k11_conlat_1(esk1_0),X1,k6_conlat_1(esk1_0))
| ~ r1_lattices(k11_conlat_1(esk1_0),X1,k6_conlat_1(esk1_0))
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(esk1_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_181,c_0_102]),c_0_182]),c_0_183]),c_0_184]),c_0_83])]),c_0_75]) ).
cnf(c_0_195,negated_conjecture,
( r1_lattices(k11_conlat_1(esk1_0),X1,k6_conlat_1(esk1_0))
| ~ r3_lattice3(k11_conlat_1(esk1_0),X1,u1_struct_0(k11_conlat_1(esk1_0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(esk1_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_185,c_0_186]),c_0_127])]) ).
cnf(c_0_196,plain,
( m1_subset_1(esk36_3(X1,X2,X3),u1_struct_0(X1))
| X2 = k16_lattice3(X1,X3)
| v3_struct_0(X1)
| ~ r3_lattice3(X1,X2,X3)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ v10_lattices(X1)
| ~ v4_lattice3(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[c_0_187]) ).
cnf(c_0_197,plain,
( r3_lattice3(X1,esk36_3(X1,X2,X3),X3)
| X2 = k16_lattice3(X1,X3)
| v3_struct_0(X1)
| ~ r3_lattice3(X1,X2,X3)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ v10_lattices(X1)
| ~ v4_lattice3(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[c_0_187]) ).
cnf(c_0_198,plain,
( r3_lattice3(X1,X2,X3)
| v3_struct_0(X1)
| ~ r1_lattices(X1,X2,esk2_3(X1,X2,X3))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[c_0_90]) ).
cnf(c_0_199,negated_conjecture,
( r1_lattices(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),esk2_3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),u1_struct_0(k11_conlat_1(esk1_0))))
| r3_lattice3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),u1_struct_0(k11_conlat_1(esk1_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_188,c_0_189]),c_0_102]),c_0_182]),c_0_183]),c_0_184]),c_0_83])]),c_0_75]) ).
cnf(c_0_200,negated_conjecture,
( k16_lattice3(k11_conlat_1(esk1_0),u1_struct_0(k11_conlat_1(esk1_0))) != k6_conlat_1(esk1_0)
| k3_conlat_2(esk1_0,u1_struct_0(k11_conlat_1(esk1_0))) != k5_conlat_1(esk1_0) ),
inference(rw,[status(thm)],[c_0_190,c_0_191]) ).
cnf(c_0_201,negated_conjecture,
k3_conlat_2(esk1_0,u1_struct_0(k11_conlat_1(esk1_0))) = k5_conlat_1(esk1_0),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_192,c_0_49]),c_0_193]),c_0_50]) ).
cnf(c_0_202,plain,
( X2 = k16_lattice3(X1,X3)
| v3_struct_0(X1)
| ~ r3_lattices(X1,esk36_3(X1,X2,X3),X2)
| ~ r3_lattice3(X1,X2,X3)
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ v10_lattices(X1)
| ~ v4_lattice3(X1)
| ~ l3_lattices(X1) ),
inference(split_conjunct,[status(thm)],[c_0_187]) ).
cnf(c_0_203,negated_conjecture,
( r3_lattices(k11_conlat_1(esk1_0),X1,k6_conlat_1(esk1_0))
| ~ r3_lattice3(k11_conlat_1(esk1_0),X1,u1_struct_0(k11_conlat_1(esk1_0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(esk1_0))) ),
inference(spm,[status(thm)],[c_0_194,c_0_195]) ).
cnf(c_0_204,negated_conjecture,
( k16_lattice3(k11_conlat_1(esk1_0),X1) = k6_conlat_1(esk1_0)
| m1_subset_1(esk36_3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1),u1_struct_0(k11_conlat_1(esk1_0)))
| ~ r3_lattice3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_196,c_0_102]),c_0_178]),c_0_180]),c_0_83])]),c_0_75]) ).
cnf(c_0_205,negated_conjecture,
( k16_lattice3(k11_conlat_1(esk1_0),X1) = k6_conlat_1(esk1_0)
| r3_lattice3(k11_conlat_1(esk1_0),esk36_3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1),X1)
| ~ r3_lattice3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_197,c_0_102]),c_0_178]),c_0_180]),c_0_83])]),c_0_75]) ).
cnf(c_0_206,negated_conjecture,
r3_lattice3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),u1_struct_0(k11_conlat_1(esk1_0))),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_198,c_0_199]),c_0_102]),c_0_83])]),c_0_75]) ).
cnf(c_0_207,negated_conjecture,
k16_lattice3(k11_conlat_1(esk1_0),u1_struct_0(k11_conlat_1(esk1_0))) != k6_conlat_1(esk1_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_200,c_0_201])]) ).
cnf(c_0_208,negated_conjecture,
( k16_lattice3(k11_conlat_1(esk1_0),X1) = k6_conlat_1(esk1_0)
| ~ r3_lattice3(k11_conlat_1(esk1_0),esk36_3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1),u1_struct_0(k11_conlat_1(esk1_0)))
| ~ r3_lattice3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),X1) ),
inference(csr,[status(thm)],[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_202,c_0_203]),c_0_178]),c_0_102]),c_0_180]),c_0_83])]),c_0_75]),c_0_204]) ).
cnf(c_0_209,negated_conjecture,
r3_lattice3(k11_conlat_1(esk1_0),esk36_3(k11_conlat_1(esk1_0),k6_conlat_1(esk1_0),u1_struct_0(k11_conlat_1(esk1_0))),u1_struct_0(k11_conlat_1(esk1_0))),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_205,c_0_206]),c_0_207]) ).
cnf(c_0_210,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_208,c_0_209]),c_0_206])]),c_0_207]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : LAT340+1 : TPTP v9.2.1. Released v3.4.0.
% 0.00/0.11 % 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.15/0.32 % Computer : n001.cluster.edu
% 0.15/0.32 % Model : x86_64 x86_64
% 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32 % Memory : 8042.1875MB
% 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.32 % CPULimit : 300
% 0.15/0.32 % WCLimit : 300
% 0.15/0.32 % DateTime : Mon May 4 21:26:33 EDT 2026
% 0.15/0.32 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 23.72/16.01 % Version : CSE_E---1.7
% 23.72/16.01 % Problem : theBenchmark.p
% 23.72/16.01 % SZS status Theorem for theBenchmark.p
% 23.72/16.01 % SZS output start CNFRefutation
% See solution above
% 23.84/16.07 % Total time : 13.397s
%------------------------------------------------------------------------------