%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT343+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:50:19 AM UTC 2026
% Result : Theorem 143.26s 19.70s
% Output : CNFRefutation 143.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 20
% Syntax : Number of formulae : 163 ( 39 unt; 0 def)
% Number of atoms : 506 ( 37 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 560 ( 217 ~; 248 |; 65 &)
% ( 2 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 27 ( 25 usr; 1 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 3 con; 0-4 aty)
% Number of variables : 141 ( 18 sgn 38 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(abstractness_v3_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( v3_lattices(A)
=> A = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) ) ),
file('theBenchmark.p',abstractness_v3_lattices) ).
fof(d18_conlat_1,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ! [B] :
( ~ v1_xboole_0(B)
=> ( m1_conlat_1(B,A)
<=> ! [C] :
( r2_hidden(C,B)
=> ( l3_conlat_1(C,A)
& v9_conlat_1(C,A)
& ~ v7_conlat_1(C,A) ) ) ) ) ),
file('theBenchmark.p',d18_conlat_1) ).
fof(d23_conlat_1,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> k11_conlat_1(A) = g3_lattices(k8_conlat_1(A),k10_conlat_1(A),k9_conlat_1(A)) ),
file('theBenchmark.p',d23_conlat_1) ).
fof(dt_k10_conlat_1,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ( m2_relset_1(k10_conlat_1(A),k2_zfmisc_1(k8_conlat_1(A),k8_conlat_1(A)),k8_conlat_1(A))
& v1_funct_2(k10_conlat_1(A),k2_zfmisc_1(k8_conlat_1(A),k8_conlat_1(A)),k8_conlat_1(A))
& v1_funct_1(k10_conlat_1(A)) ) ),
file('theBenchmark.p',dt_k10_conlat_1) ).
fof(dt_k11_conlat_1,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ( l3_lattices(k11_conlat_1(A))
& v3_lattices(k11_conlat_1(A))
& ~ v3_struct_0(k11_conlat_1(A)) ) ),
file('theBenchmark.p',dt_k11_conlat_1) ).
fof(dt_k4_conlat_2,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ( m2_relset_1(k4_conlat_2(A),u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)))
& v1_funct_2(k4_conlat_2(A),u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)))
& v1_funct_1(k4_conlat_2(A)) ) ),
file('theBenchmark.p',dt_k4_conlat_2) ).
fof(dt_k5_conlat_2,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ( m2_relset_1(k5_conlat_2(A),u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)))
& v1_funct_2(k5_conlat_2(A),u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)))
& v1_funct_1(k5_conlat_2(A)) ) ),
file('theBenchmark.p',dt_k5_conlat_2) ).
fof(dt_k8_conlat_1,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> m1_conlat_1(k8_conlat_1(A),A) ),
file('theBenchmark.p',dt_k8_conlat_1) ).
fof(dt_k8_funct_2,axiom,
! [A,B,C,D] :
( ( m1_subset_1(D,A)
& m1_relset_1(C,A,B)
& v1_funct_2(C,A,B)
& v1_funct_1(C)
& ~ v1_xboole_0(A) )
=> m1_subset_1(k8_funct_2(A,B,C,D),B) ),
file('theBenchmark.p',dt_k8_funct_2) ).
fof(dt_k9_conlat_1,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ( m2_relset_1(k9_conlat_1(A),k2_zfmisc_1(k8_conlat_1(A),k8_conlat_1(A)),k8_conlat_1(A))
& v1_funct_2(k9_conlat_1(A),k2_zfmisc_1(k8_conlat_1(A),k8_conlat_1(A)),k8_conlat_1(A))
& v1_funct_1(k9_conlat_1(A)) ) ),
file('theBenchmark.p',dt_k9_conlat_1) ).
fof(dt_l2_conlat_1,axiom,
! [A] :
( l2_conlat_1(A)
=> l1_conlat_1(A) ),
file('theBenchmark.p',dt_l2_conlat_1) ).
fof(fc1_conlat_1,axiom,
! [A] :
( ( l1_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ~ v1_xboole_0(u2_conlat_1(A)) ),
file('theBenchmark.p',fc1_conlat_1) ).
fof(fc2_conlat_1,axiom,
! [A] :
( ( l1_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ~ v1_xboole_0(u1_conlat_1(A)) ),
file('theBenchmark.p',fc2_conlat_1) ).
fof(fc3_conlat_1,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ~ v1_xboole_0(k7_conlat_1(A)) ),
file('theBenchmark.p',fc3_conlat_1) ).
fof(fc5_conlat_1,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ( v4_lattice3(k11_conlat_1(A))
& v10_lattices(k11_conlat_1(A))
& v9_lattices(k11_conlat_1(A))
& v8_lattices(k11_conlat_1(A))
& v7_lattices(k11_conlat_1(A))
& v6_lattices(k11_conlat_1(A))
& v5_lattices(k11_conlat_1(A))
& v4_lattices(k11_conlat_1(A))
& v3_lattices(k11_conlat_1(A))
& ~ v3_struct_0(k11_conlat_1(A)) ) ),
file('theBenchmark.p',fc5_conlat_1) ).
fof(free_g3_lattices,axiom,
! [A,B,C] :
( ( m1_relset_1(C,k2_zfmisc_1(A,A),A)
& v1_funct_2(C,k2_zfmisc_1(A,A),A)
& v1_funct_1(C)
& m1_relset_1(B,k2_zfmisc_1(A,A),A)
& v1_funct_2(B,k2_zfmisc_1(A,A),A)
& v1_funct_1(B) )
=> ! [D,E,F] :
( g3_lattices(A,B,C) = g3_lattices(D,E,F)
=> ( C = F
& B = E
& A = D ) ) ),
file('theBenchmark.p',free_g3_lattices) ).
fof(redefinition_k8_conlat_1,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> k8_conlat_1(A) = k7_conlat_1(A) ),
file('theBenchmark.p',redefinition_k8_conlat_1) ).
fof(redefinition_m2_relset_1,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('theBenchmark.p',redefinition_m2_relset_1) ).
fof(t2_subset,axiom,
! [A,B] :
( m1_subset_1(A,B)
=> ( r2_hidden(A,B)
| v1_xboole_0(B) ) ),
file('theBenchmark.p',t2_subset) ).
fof(t11_conlat_2,conjecture,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ! [B] :
( m1_subset_1(B,u1_conlat_1(A))
=> ! [C] :
( m1_subset_1(C,u2_conlat_1(A))
=> ( l3_conlat_1(k8_funct_2(u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k5_conlat_2(A),C),A)
& v9_conlat_1(k8_funct_2(u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k5_conlat_2(A),C),A)
& ~ v7_conlat_1(k8_funct_2(u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k5_conlat_2(A),C),A)
& l3_conlat_1(k8_funct_2(u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k4_conlat_2(A),B),A)
& v9_conlat_1(k8_funct_2(u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k4_conlat_2(A),B),A)
& ~ v7_conlat_1(k8_funct_2(u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k4_conlat_2(A),B),A) ) ) ) ),
file('theBenchmark.p',t11_conlat_2) ).
fof(t11_conlat_2_neg,negated_conjecture,
~ ! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ! [B] :
( m1_subset_1(B,u1_conlat_1(A))
=> ! [C] :
( m1_subset_1(C,u2_conlat_1(A))
=> ( l3_conlat_1(k8_funct_2(u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k5_conlat_2(A),C),A)
& v9_conlat_1(k8_funct_2(u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k5_conlat_2(A),C),A)
& ~ v7_conlat_1(k8_funct_2(u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k5_conlat_2(A),C),A)
& l3_conlat_1(k8_funct_2(u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k4_conlat_2(A),B),A)
& v9_conlat_1(k8_funct_2(u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k4_conlat_2(A),B),A)
& ~ v7_conlat_1(k8_funct_2(u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k4_conlat_2(A),B),A) ) ) ) ),
inference(assume_negation,[status(cth)],[t11_conlat_2]) ).
cnf(c_99,plain,
( l1_conlat_1(A)
| ~ l2_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_l2_conlat_1]) ).
cnf(c_100,plain,
( m2_relset_1(k9_conlat_1(A),k2_zfmisc_1(k8_conlat_1(A),k8_conlat_1(A)),k8_conlat_1(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k9_conlat_1]) ).
cnf(c_101,plain,
( v1_funct_2(k9_conlat_1(A),k2_zfmisc_1(k8_conlat_1(A),k8_conlat_1(A)),k8_conlat_1(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k9_conlat_1]) ).
cnf(c_102,plain,
( v1_funct_1(k9_conlat_1(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k9_conlat_1]) ).
cnf(c_103,plain,
( m1_conlat_1(k8_conlat_1(A),A)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k8_conlat_1]) ).
cnf(c_105,plain,
( m2_relset_1(k5_conlat_2(A),u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k5_conlat_2]) ).
cnf(c_106,plain,
( v1_funct_2(k5_conlat_2(A),u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k5_conlat_2]) ).
cnf(c_107,plain,
( v1_funct_1(k5_conlat_2(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k5_conlat_2]) ).
cnf(c_108,plain,
( m2_relset_1(k4_conlat_2(A),u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k4_conlat_2]) ).
cnf(c_109,plain,
( v1_funct_2(k4_conlat_2(A),u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k4_conlat_2]) ).
cnf(c_110,plain,
( v1_funct_1(k4_conlat_2(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k4_conlat_2]) ).
cnf(c_111,plain,
( l3_lattices(k11_conlat_1(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k11_conlat_1]) ).
cnf(c_114,plain,
( m2_relset_1(k10_conlat_1(A),k2_zfmisc_1(k8_conlat_1(A),k8_conlat_1(A)),k8_conlat_1(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k10_conlat_1]) ).
cnf(c_115,plain,
( v1_funct_2(k10_conlat_1(A),k2_zfmisc_1(k8_conlat_1(A),k8_conlat_1(A)),k8_conlat_1(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k10_conlat_1]) ).
cnf(c_116,plain,
( v1_funct_1(k10_conlat_1(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[dt_k10_conlat_1]) ).
cnf(c_117,plain,
( g3_lattices(k8_conlat_1(A),k10_conlat_1(A),k9_conlat_1(A)) = k11_conlat_1(A)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[d23_conlat_1]) ).
cnf(c_120,plain,
( l3_conlat_1(C,A)
| ~ r2_hidden(C,B)
| ~ m1_conlat_1(B,A)
| v1_xboole_0(B)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[d18_conlat_1]) ).
cnf(c_121,plain,
( v9_conlat_1(C,A)
| ~ r2_hidden(C,B)
| ~ m1_conlat_1(B,A)
| v1_xboole_0(B)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[d18_conlat_1]) ).
cnf(c_122,plain,
( ~ v7_conlat_1(C,A)
| ~ r2_hidden(C,B)
| ~ m1_conlat_1(B,A)
| v1_xboole_0(B)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[d18_conlat_1]) ).
cnf(c_137,plain,
( ~ v1_xboole_0(k7_conlat_1(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[fc3_conlat_1]) ).
cnf(c_148,plain,
( v3_lattices(k11_conlat_1(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[fc5_conlat_1]) ).
cnf(c_160,plain,
( k7_conlat_1(A) = k8_conlat_1(A)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[redefinition_k8_conlat_1]) ).
fof(nnf_96,plain,
? [A] :
( ? [B] :
( ? [C] :
( ( ~ l3_conlat_1(k8_funct_2(u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k5_conlat_2(A),C),A)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k5_conlat_2(A),C),A)
| v7_conlat_1(k8_funct_2(u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k5_conlat_2(A),C),A)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k4_conlat_2(A),B),A)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k4_conlat_2(A),B),A)
| v7_conlat_1(k8_funct_2(u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k4_conlat_2(A),B),A) )
& m1_subset_1(C,u2_conlat_1(A)) )
& m1_subset_1(B,u1_conlat_1(A)) )
& l2_conlat_1(A)
& ~ v3_conlat_1(A) ),
inference(fof_nnf,[status(thm)],[t11_conlat_2_neg]) ).
fof(sk_t11_conlat_2_neg,plain,
( ( ~ l3_conlat_1(k8_funct_2(u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k5_conlat_2(sK0),sK2),sK0)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k5_conlat_2(sK0),sK2),sK0)
| v7_conlat_1(k8_funct_2(u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k5_conlat_2(sK0),sK2),sK0)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k4_conlat_2(sK0),sK1),sK0)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k4_conlat_2(sK0),sK1),sK0)
| v7_conlat_1(k8_funct_2(u1_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k4_conlat_2(sK0),sK1),sK0) )
& m1_subset_1(sK2,u2_conlat_1(sK0))
& m1_subset_1(sK1,u1_conlat_1(sK0))
& l2_conlat_1(sK0)
& ~ v3_conlat_1(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(A,sK0),skolemize(B,sK1),skolemize(C,sK2)],[nnf_96]) ).
cnf(c_161,negated_conjecture,
l2_conlat_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t11_conlat_2_neg]) ).
cnf(c_169,negated_conjecture,
( l3_lattices(k11_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_161,c_111]) ).
cnf(c_182,plain,
( g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) = A
| ~ v3_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[abstractness_v3_lattices]) ).
cnf(c_193,plain,
( ~ v1_xboole_0(u2_conlat_1(A))
| ~ l1_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[fc1_conlat_1]) ).
cnf(c_194,plain,
( ~ v1_xboole_0(u1_conlat_1(A))
| ~ l1_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[fc2_conlat_1]) ).
cnf(c_200,negated_conjecture,
l1_conlat_1(sK0),
inference(resolve,[status(thm)],[c_161,c_99]) ).
cnf(c_205,plain,
( m1_relset_1(A,B,C)
| ~ m2_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_m2_relset_1]) ).
cnf(c_211,negated_conjecture,
( m2_relset_1(k9_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_161,c_100]) ).
cnf(c_212,negated_conjecture,
( m2_relset_1(k5_conlat_2(sK0),u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_161,c_105]) ).
cnf(c_213,negated_conjecture,
( m2_relset_1(k4_conlat_2(sK0),u1_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_161,c_108]) ).
cnf(c_214,negated_conjecture,
( m2_relset_1(k10_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_161,c_114]) ).
cnf(c_379,negated_conjecture,
( v3_conlat_1(sK0)
| g3_lattices(u1_struct_0(k11_conlat_1(sK0)),u2_lattices(k11_conlat_1(sK0)),u1_lattices(k11_conlat_1(sK0))) = k11_conlat_1(sK0)
| ~ v3_lattices(k11_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_182,c_169]) ).
cnf(c_470,plain,
( m1_subset_1(k8_funct_2(A,C,B,D),C)
| ~ m1_subset_1(D,A)
| ~ m1_relset_1(B,A,C)
| ~ v1_funct_2(B,A,C)
| ~ v1_funct_1(B)
| v1_xboole_0(A) ),
inference(clausify,[status(thm)],[dt_k8_funct_2]) ).
cnf(c_477,plain,
( D = B
| g3_lattices(D,E,F) != g3_lattices(B,A,C)
| ~ m1_relset_1(C,k2_zfmisc_1(B,B),B)
| ~ v1_funct_2(C,k2_zfmisc_1(B,B),B)
| ~ v1_funct_1(C)
| ~ m1_relset_1(A,k2_zfmisc_1(B,B),B)
| ~ v1_funct_2(A,k2_zfmisc_1(B,B),B)
| ~ v1_funct_1(A) ),
inference(clausify,[status(thm)],[free_g3_lattices]) ).
cnf(c_519,plain,
( r2_hidden(A,B)
| v1_xboole_0(B)
| ~ m1_subset_1(A,B) ),
inference(clausify,[status(thm)],[t2_subset]) ).
cnf(c_525,negated_conjecture,
~ v3_conlat_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t11_conlat_2_neg]) ).
cnf(c_526,negated_conjecture,
m1_subset_1(sK1,u1_conlat_1(sK0)),
inference(split_conjunct,[status(thm)],[sk_t11_conlat_2_neg]) ).
cnf(c_527,negated_conjecture,
m1_subset_1(sK2,u2_conlat_1(sK0)),
inference(split_conjunct,[status(thm)],[sk_t11_conlat_2_neg]) ).
cnf(c_528,negated_conjecture,
( ~ l3_conlat_1(k8_funct_2(u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k5_conlat_2(sK0),sK2),sK0)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k5_conlat_2(sK0),sK2),sK0)
| v7_conlat_1(k8_funct_2(u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k5_conlat_2(sK0),sK2),sK0)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k4_conlat_2(sK0),sK1),sK0)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k4_conlat_2(sK0),sK1),sK0)
| v7_conlat_1(k8_funct_2(u1_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k4_conlat_2(sK0),sK1),sK0) ),
inference(split_conjunct,[status(thm)],[sk_t11_conlat_2_neg]) ).
cnf(c_563,negated_conjecture,
( k7_conlat_1(sK0) = k8_conlat_1(sK0)
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_161,c_160]) ).
cnf(c_564,negated_conjecture,
k7_conlat_1(sK0) = k8_conlat_1(sK0),
inference(resolve,[status(thm)],[c_525,c_563]) ).
cnf(c_585,negated_conjecture,
( v3_lattices(k11_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_161,c_148]) ).
cnf(c_586,negated_conjecture,
v3_lattices(k11_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_525,c_585]) ).
cnf(c_589,negated_conjecture,
( ~ v1_xboole_0(k7_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_161,c_137]) ).
cnf(c_13073,negated_conjecture,
( ~ v1_xboole_0(k8_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(paramod,[status(thm)],[c_564,c_589]) ).
cnf(c_590,negated_conjecture,
~ v1_xboole_0(k8_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_525,c_13073]) ).
cnf(c_601,negated_conjecture,
( v1_funct_2(k9_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_161,c_101]) ).
cnf(c_602,negated_conjecture,
v1_funct_2(k9_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_525,c_601]) ).
cnf(c_603,negated_conjecture,
( v1_funct_1(k9_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_161,c_102]) ).
cnf(c_604,negated_conjecture,
v1_funct_1(k9_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_525,c_603]) ).
cnf(c_605,negated_conjecture,
( m1_conlat_1(k8_conlat_1(sK0),sK0)
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_161,c_103]) ).
cnf(c_606,negated_conjecture,
m1_conlat_1(k8_conlat_1(sK0),sK0),
inference(resolve,[status(thm)],[c_525,c_605]) ).
cnf(c_607,negated_conjecture,
( v1_funct_2(k5_conlat_2(sK0),u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_161,c_106]) ).
cnf(c_608,negated_conjecture,
v1_funct_2(k5_conlat_2(sK0),u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0))),
inference(resolve,[status(thm)],[c_525,c_607]) ).
cnf(c_609,negated_conjecture,
( v1_funct_1(k5_conlat_2(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_161,c_107]) ).
cnf(c_610,negated_conjecture,
v1_funct_1(k5_conlat_2(sK0)),
inference(resolve,[status(thm)],[c_525,c_609]) ).
cnf(c_611,negated_conjecture,
( v1_funct_2(k4_conlat_2(sK0),u1_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_161,c_109]) ).
cnf(c_612,negated_conjecture,
v1_funct_2(k4_conlat_2(sK0),u1_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0))),
inference(resolve,[status(thm)],[c_525,c_611]) ).
cnf(c_613,negated_conjecture,
( v1_funct_1(k4_conlat_2(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_161,c_110]) ).
cnf(c_614,negated_conjecture,
v1_funct_1(k4_conlat_2(sK0)),
inference(resolve,[status(thm)],[c_525,c_613]) ).
cnf(c_615,negated_conjecture,
( v1_funct_2(k10_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_161,c_115]) ).
cnf(c_616,negated_conjecture,
v1_funct_2(k10_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_525,c_615]) ).
cnf(c_617,negated_conjecture,
( v1_funct_1(k10_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_161,c_116]) ).
cnf(c_618,negated_conjecture,
v1_funct_1(k10_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_525,c_617]) ).
cnf(c_619,negated_conjecture,
( g3_lattices(k8_conlat_1(sK0),k10_conlat_1(sK0),k9_conlat_1(sK0)) = k11_conlat_1(sK0)
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_161,c_117]) ).
cnf(c_620,negated_conjecture,
g3_lattices(k8_conlat_1(sK0),k10_conlat_1(sK0),k9_conlat_1(sK0)) = k11_conlat_1(sK0),
inference(resolve,[status(thm)],[c_525,c_619]) ).
cnf(c_625,negated_conjecture,
( l3_conlat_1(B,sK0)
| ~ r2_hidden(B,A)
| ~ m1_conlat_1(A,sK0)
| v1_xboole_0(A)
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_161,c_120]) ).
cnf(c_626,negated_conjecture,
( l3_conlat_1(B,sK0)
| ~ r2_hidden(B,A)
| ~ m1_conlat_1(A,sK0)
| v1_xboole_0(A) ),
inference(resolve,[status(thm)],[c_525,c_625]) ).
cnf(c_627,negated_conjecture,
( v9_conlat_1(B,sK0)
| ~ r2_hidden(B,A)
| ~ m1_conlat_1(A,sK0)
| v1_xboole_0(A)
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_161,c_121]) ).
cnf(c_628,negated_conjecture,
( v9_conlat_1(B,sK0)
| ~ r2_hidden(B,A)
| ~ m1_conlat_1(A,sK0)
| v1_xboole_0(A) ),
inference(resolve,[status(thm)],[c_525,c_627]) ).
cnf(c_629,negated_conjecture,
( ~ v7_conlat_1(B,sK0)
| ~ r2_hidden(B,A)
| ~ m1_conlat_1(A,sK0)
| v1_xboole_0(A)
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_161,c_122]) ).
cnf(c_630,negated_conjecture,
( ~ v7_conlat_1(B,sK0)
| ~ r2_hidden(B,A)
| ~ m1_conlat_1(A,sK0)
| v1_xboole_0(A) ),
inference(resolve,[status(thm)],[c_525,c_629]) ).
cnf(c_653,negated_conjecture,
( ~ v1_xboole_0(u1_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_200,c_194]) ).
cnf(c_654,negated_conjecture,
~ v1_xboole_0(u1_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_525,c_653]) ).
cnf(c_655,negated_conjecture,
( ~ v1_xboole_0(u2_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_200,c_193]) ).
cnf(c_656,negated_conjecture,
~ v1_xboole_0(u2_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_525,c_655]) ).
cnf(c_669,negated_conjecture,
( m1_relset_1(k9_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_211,c_205]) ).
cnf(c_670,negated_conjecture,
m1_relset_1(k9_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_525,c_669]) ).
cnf(c_673,negated_conjecture,
( m1_relset_1(k5_conlat_2(sK0),u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_212,c_205]) ).
cnf(c_674,negated_conjecture,
m1_relset_1(k5_conlat_2(sK0),u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0))),
inference(resolve,[status(thm)],[c_525,c_673]) ).
cnf(c_677,negated_conjecture,
( m1_relset_1(k4_conlat_2(sK0),u1_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_213,c_205]) ).
cnf(c_678,negated_conjecture,
m1_relset_1(k4_conlat_2(sK0),u1_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0))),
inference(resolve,[status(thm)],[c_525,c_677]) ).
cnf(c_681,negated_conjecture,
( m1_relset_1(k10_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_214,c_205]) ).
cnf(c_682,negated_conjecture,
m1_relset_1(k10_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_525,c_681]) ).
cnf(c_13074,negated_conjecture,
( v3_conlat_1(sK0)
| g3_lattices(u1_struct_0(k11_conlat_1(sK0)),u2_lattices(k11_conlat_1(sK0)),u1_lattices(k11_conlat_1(sK0))) = k11_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_586,c_379]) ).
cnf(c_768,negated_conjecture,
g3_lattices(u1_struct_0(k11_conlat_1(sK0)),u2_lattices(k11_conlat_1(sK0)),u1_lattices(k11_conlat_1(sK0))) = k11_conlat_1(sK0),
inference(resolve,[status(thm)],[c_525,c_13074]) ).
cnf(c_13075,negated_conjecture,
( m1_subset_1(k8_funct_2(u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k5_conlat_2(sK0),A),u1_struct_0(k11_conlat_1(sK0)))
| ~ m1_subset_1(A,u2_conlat_1(sK0))
| ~ m1_relset_1(k5_conlat_2(sK0),u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)))
| ~ v1_funct_1(k5_conlat_2(sK0))
| v1_xboole_0(u2_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_608,c_470]) ).
cnf(c_13076,negated_conjecture,
( m1_subset_1(k8_funct_2(u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k5_conlat_2(sK0),A),u1_struct_0(k11_conlat_1(sK0)))
| ~ m1_subset_1(A,u2_conlat_1(sK0))
| ~ m1_relset_1(k5_conlat_2(sK0),u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)))
| ~ v1_funct_1(k5_conlat_2(sK0)) ),
inference(resolve,[status(thm)],[c_656,c_13075]) ).
cnf(c_13077,negated_conjecture,
( m1_subset_1(k8_funct_2(u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k5_conlat_2(sK0),A),u1_struct_0(k11_conlat_1(sK0)))
| ~ m1_subset_1(A,u2_conlat_1(sK0))
| ~ m1_relset_1(k5_conlat_2(sK0),u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0))) ),
inference(resolve,[status(thm)],[c_610,c_13076]) ).
cnf(c_3753,negated_conjecture,
( m1_subset_1(k8_funct_2(u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k5_conlat_2(sK0),A),u1_struct_0(k11_conlat_1(sK0)))
| ~ m1_subset_1(A,u2_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_674,c_13077]) ).
cnf(c_13078,negated_conjecture,
( m1_subset_1(k8_funct_2(u1_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k4_conlat_2(sK0),A),u1_struct_0(k11_conlat_1(sK0)))
| ~ m1_subset_1(A,u1_conlat_1(sK0))
| ~ m1_relset_1(k4_conlat_2(sK0),u1_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)))
| ~ v1_funct_1(k4_conlat_2(sK0))
| v1_xboole_0(u1_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_612,c_470]) ).
cnf(c_13079,negated_conjecture,
( m1_subset_1(k8_funct_2(u1_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k4_conlat_2(sK0),A),u1_struct_0(k11_conlat_1(sK0)))
| ~ m1_subset_1(A,u1_conlat_1(sK0))
| ~ m1_relset_1(k4_conlat_2(sK0),u1_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)))
| ~ v1_funct_1(k4_conlat_2(sK0)) ),
inference(resolve,[status(thm)],[c_654,c_13078]) ).
cnf(c_13080,negated_conjecture,
( m1_subset_1(k8_funct_2(u1_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k4_conlat_2(sK0),A),u1_struct_0(k11_conlat_1(sK0)))
| ~ m1_subset_1(A,u1_conlat_1(sK0))
| ~ m1_relset_1(k4_conlat_2(sK0),u1_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0))) ),
inference(resolve,[status(thm)],[c_614,c_13079]) ).
cnf(c_3839,negated_conjecture,
( m1_subset_1(k8_funct_2(u1_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k4_conlat_2(sK0),A),u1_struct_0(k11_conlat_1(sK0)))
| ~ m1_subset_1(A,u1_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_678,c_13080]) ).
cnf(c_13081,plain,
( A = k8_conlat_1(sK0)
| g3_lattices(A,B,C) != k11_conlat_1(sK0)
| ~ m1_relset_1(k9_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0))
| ~ v1_funct_2(k9_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0))
| ~ v1_funct_1(k9_conlat_1(sK0))
| ~ m1_relset_1(k10_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0))
| ~ v1_funct_2(k10_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0))
| ~ v1_funct_1(k10_conlat_1(sK0)) ),
inference(paramod,[status(thm)],[c_620,c_477]) ).
cnf(c_13082,plain,
( k8_conlat_1(sK0) = A
| g3_lattices(A,B,C) != k11_conlat_1(sK0)
| ~ m1_relset_1(k9_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0))
| ~ v1_funct_2(k9_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0))
| ~ v1_funct_1(k9_conlat_1(sK0))
| ~ m1_relset_1(k10_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0))
| ~ v1_funct_2(k10_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0))
| ~ v1_funct_1(k10_conlat_1(sK0)) ),
inference(copy,[status(thm)],[c_13081]) ).
cnf(c_13083,negated_conjecture,
( k8_conlat_1(sK0) = A
| g3_lattices(A,B,C) != k11_conlat_1(sK0)
| ~ m1_relset_1(k9_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0))
| ~ v1_funct_2(k9_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0))
| ~ v1_funct_1(k9_conlat_1(sK0))
| ~ m1_relset_1(k10_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0))
| ~ v1_funct_2(k10_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_618,c_13082]) ).
cnf(c_13084,negated_conjecture,
( k8_conlat_1(sK0) = A
| g3_lattices(A,B,C) != k11_conlat_1(sK0)
| ~ m1_relset_1(k9_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0))
| ~ v1_funct_2(k9_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0))
| ~ v1_funct_1(k9_conlat_1(sK0))
| ~ m1_relset_1(k10_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_616,c_13083]) ).
cnf(c_13085,negated_conjecture,
( k8_conlat_1(sK0) = A
| g3_lattices(A,B,C) != k11_conlat_1(sK0)
| ~ m1_relset_1(k9_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0))
| ~ v1_funct_2(k9_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0))
| ~ v1_funct_1(k9_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_682,c_13084]) ).
cnf(c_13086,negated_conjecture,
( k8_conlat_1(sK0) = A
| g3_lattices(A,B,C) != k11_conlat_1(sK0)
| ~ m1_relset_1(k9_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0))
| ~ v1_funct_2(k9_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_604,c_13085]) ).
cnf(c_13087,negated_conjecture,
( k8_conlat_1(sK0) = A
| g3_lattices(A,B,C) != k11_conlat_1(sK0)
| ~ m1_relset_1(k9_conlat_1(sK0),k2_zfmisc_1(k8_conlat_1(sK0),k8_conlat_1(sK0)),k8_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_602,c_13086]) ).
cnf(c_4067,negated_conjecture,
( k8_conlat_1(sK0) = A
| g3_lattices(A,B,C) != k11_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_670,c_13087]) ).
cnf(c_13088,negated_conjecture,
( l3_conlat_1(A,sK0)
| ~ r2_hidden(A,k8_conlat_1(sK0))
| v1_xboole_0(k8_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_626,c_606]) ).
cnf(c_4079,negated_conjecture,
( l3_conlat_1(A,sK0)
| ~ r2_hidden(A,k8_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_590,c_13088]) ).
cnf(c_13089,negated_conjecture,
( v9_conlat_1(A,sK0)
| ~ r2_hidden(A,k8_conlat_1(sK0))
| v1_xboole_0(k8_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_628,c_606]) ).
cnf(c_4082,negated_conjecture,
( v9_conlat_1(A,sK0)
| ~ r2_hidden(A,k8_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_590,c_13089]) ).
cnf(c_13090,negated_conjecture,
( ~ v7_conlat_1(A,sK0)
| ~ r2_hidden(A,k8_conlat_1(sK0))
| v1_xboole_0(k8_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_630,c_606]) ).
cnf(c_4085,negated_conjecture,
( ~ v7_conlat_1(A,sK0)
| ~ r2_hidden(A,k8_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_590,c_13090]) ).
cnf(c_13091,negated_conjecture,
k8_conlat_1(sK0) = u1_struct_0(k11_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_4067,c_768]) ).
cnf(c_6912,negated_conjecture,
u1_struct_0(k11_conlat_1(sK0)) = k8_conlat_1(sK0),
inference(copy,[status(thm)],[c_13091]) ).
cnf(c_13092,negated_conjecture,
( m1_subset_1(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),A),u1_struct_0(k11_conlat_1(sK0)))
| ~ m1_subset_1(A,u1_conlat_1(sK0)) ),
inference(paramod,[status(thm)],[c_6912,c_3839]) ).
cnf(c_7112,negated_conjecture,
( m1_subset_1(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),A),k8_conlat_1(sK0))
| ~ m1_subset_1(A,u1_conlat_1(sK0)) ),
inference(paramod,[status(thm)],[c_6912,c_13092]) ).
cnf(c_13093,negated_conjecture,
( m1_subset_1(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),A),u1_struct_0(k11_conlat_1(sK0)))
| ~ m1_subset_1(A,u2_conlat_1(sK0)) ),
inference(paramod,[status(thm)],[c_6912,c_3753]) ).
cnf(c_7114,negated_conjecture,
( m1_subset_1(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),A),k8_conlat_1(sK0))
| ~ m1_subset_1(A,u2_conlat_1(sK0)) ),
inference(paramod,[status(thm)],[c_6912,c_13093]) ).
cnf(c_13094,negated_conjecture,
( ~ l3_conlat_1(k8_funct_2(u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k5_conlat_2(sK0),sK2),sK0)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k5_conlat_2(sK0),sK2),sK0)
| v7_conlat_1(k8_funct_2(u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k5_conlat_2(sK0),sK2),sK0)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k4_conlat_2(sK0),sK1),sK0)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k4_conlat_2(sK0),sK1),sK0)
| v7_conlat_1(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),sK1),sK0) ),
inference(paramod,[status(thm)],[c_6912,c_528]) ).
cnf(c_13095,negated_conjecture,
( ~ l3_conlat_1(k8_funct_2(u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k5_conlat_2(sK0),sK2),sK0)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k5_conlat_2(sK0),sK2),sK0)
| v7_conlat_1(k8_funct_2(u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k5_conlat_2(sK0),sK2),sK0)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k4_conlat_2(sK0),sK1),sK0)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),sK1),sK0)
| v7_conlat_1(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),sK1),sK0) ),
inference(paramod,[status(thm)],[c_6912,c_13094]) ).
cnf(c_13096,negated_conjecture,
( ~ l3_conlat_1(k8_funct_2(u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k5_conlat_2(sK0),sK2),sK0)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k5_conlat_2(sK0),sK2),sK0)
| v7_conlat_1(k8_funct_2(u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k5_conlat_2(sK0),sK2),sK0)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),sK1),sK0)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),sK1),sK0)
| v7_conlat_1(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),sK1),sK0) ),
inference(paramod,[status(thm)],[c_6912,c_13095]) ).
cnf(c_13097,negated_conjecture,
( ~ l3_conlat_1(k8_funct_2(u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k5_conlat_2(sK0),sK2),sK0)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k5_conlat_2(sK0),sK2),sK0)
| v7_conlat_1(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),sK2),sK0)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),sK1),sK0)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),sK1),sK0)
| v7_conlat_1(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),sK1),sK0) ),
inference(paramod,[status(thm)],[c_6912,c_13096]) ).
cnf(c_13098,negated_conjecture,
( ~ l3_conlat_1(k8_funct_2(u2_conlat_1(sK0),u1_struct_0(k11_conlat_1(sK0)),k5_conlat_2(sK0),sK2),sK0)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),sK2),sK0)
| v7_conlat_1(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),sK2),sK0)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),sK1),sK0)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),sK1),sK0)
| v7_conlat_1(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),sK1),sK0) ),
inference(paramod,[status(thm)],[c_6912,c_13097]) ).
cnf(c_7130,negated_conjecture,
( ~ l3_conlat_1(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),sK2),sK0)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),sK2),sK0)
| v7_conlat_1(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),sK2),sK0)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),sK1),sK0)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),sK1),sK0)
| v7_conlat_1(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),sK1),sK0) ),
inference(paramod,[status(thm)],[c_6912,c_13098]) ).
cnf(c_13012,plain,
m1_subset_1(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),sK1),k8_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_7112,c_526]) ).
cnf(c_13099,plain,
( r2_hidden(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),sK1),k8_conlat_1(sK0))
| v1_xboole_0(k8_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_13012,c_519]) ).
cnf(c_13015,negated_conjecture,
r2_hidden(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),sK1),k8_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_590,c_13099]) ).
cnf(c_13024,plain,
~ v7_conlat_1(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),sK1),sK0),
inference(resolve,[status(thm)],[c_13015,c_4085]) ).
cnf(c_13025,plain,
v9_conlat_1(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),sK1),sK0),
inference(resolve,[status(thm)],[c_13015,c_4082]) ).
cnf(c_13026,plain,
l3_conlat_1(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),sK1),sK0),
inference(resolve,[status(thm)],[c_13015,c_4079]) ).
cnf(c_13100,negated_conjecture,
( ~ l3_conlat_1(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),sK2),sK0)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),sK2),sK0)
| v7_conlat_1(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),sK2),sK0)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),sK1),sK0)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),sK1),sK0) ),
inference(resolve,[status(thm)],[c_13024,c_7130]) ).
cnf(c_13101,negated_conjecture,
( ~ l3_conlat_1(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),sK2),sK0)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),sK2),sK0)
| v7_conlat_1(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),sK2),sK0)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(sK0),k8_conlat_1(sK0),k4_conlat_2(sK0),sK1),sK0) ),
inference(resolve,[status(thm)],[c_13025,c_13100]) ).
cnf(c_13032,negated_conjecture,
( ~ l3_conlat_1(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),sK2),sK0)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),sK2),sK0)
| v7_conlat_1(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),sK2),sK0) ),
inference(resolve,[status(thm)],[c_13026,c_13101]) ).
cnf(c_13052,plain,
m1_subset_1(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),sK2),k8_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_7114,c_527]) ).
cnf(c_13102,plain,
( r2_hidden(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),sK2),k8_conlat_1(sK0))
| v1_xboole_0(k8_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_13052,c_519]) ).
cnf(c_13055,negated_conjecture,
r2_hidden(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),sK2),k8_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_590,c_13102]) ).
cnf(c_13064,plain,
~ v7_conlat_1(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),sK2),sK0),
inference(resolve,[status(thm)],[c_13055,c_4085]) ).
cnf(c_13065,plain,
v9_conlat_1(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),sK2),sK0),
inference(resolve,[status(thm)],[c_13055,c_4082]) ).
cnf(c_13066,plain,
l3_conlat_1(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),sK2),sK0),
inference(resolve,[status(thm)],[c_13055,c_4079]) ).
cnf(c_13103,negated_conjecture,
( ~ l3_conlat_1(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),sK2),sK0)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),sK2),sK0) ),
inference(resolve,[status(thm)],[c_13064,c_13032]) ).
cnf(c_13104,negated_conjecture,
~ l3_conlat_1(k8_funct_2(u2_conlat_1(sK0),k8_conlat_1(sK0),k5_conlat_2(sK0),sK2),sK0),
inference(resolve,[status(thm)],[c_13065,c_13103]) ).
cnf(c_13072,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_13066,c_13104]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT343+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n010.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Fri Sep 25 21:06:16 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.44 % Process 1672008 was started by sandbox2 on n010,
% 0.17/0.44 % Fri Sep 25 21:06:16 2026
% 0.17/0.44 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.17/0.47
% 0.17/0.47 % From the command line: assign(max_seconds, 300).
% 143.26/19.70
% 143.26/19.70 % given #500 (T,wt=20): 4349 v3_struct_0(c2) | -r2_hidden(A,f12(c2)) | m1_subset_1(A,u1_struct_0(c2)). [resolve(700,b,520,b)].
% 143.26/19.70
% 143.26/19.70 % given #1000 (F,wt=43): 6790 -v1_funct_2(u1_lattices(c13),k2_zfmisc_1(u1_struct_0(c12),u1_struct_0(c12)),u1_struct_0(c12)) | -m1_relset_1(u1_lattices(c13),k2_zfmisc_1(u1_struct_0(c12),u1_struct_0(c12)),u1_struct_0(c12)) | -v3_struct_0(g3_lattices(u1_struct_0(c12),u2_lattices(c12),u1_lattices(c13))). [resolve(2522,a,358,a)].
% 143.26/19.70
% 143.26/19.70 % given #1500 (T,wt=29): 2813 v1_xboole_0(A) | -m1_subset_1(B,A) | m1_subset_1(k8_funct_2(A,C,f8(A,C),B),C). [resolve(492,a,470,d),unit_del(b,493),unit_del(c,494)].
% 143.26/19.70
% 143.26/19.70 % SZS status Theorem for theBenchmark
% 143.26/19.70
% 143.26/19.70 % Proof 1 at 2.51 (+ 0.51) seconds.
% 143.26/19.70 % Length of proof is 128.
% 143.26/19.70 % Level of proof is 12.
% 143.26/19.70 % Maximum clause weight is 86.000.
% 143.26/19.70 % Given clauses 1755.
% 143.26/19.70
% 143.26/19.70 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------