%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT338+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 : n003.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:18 AM UTC 2026
% Result : Theorem 17.94s 3.06s
% Output : CNFRefutation 17.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 16
% Syntax : Number of formulae : 112 ( 22 unt; 0 def)
% Number of atoms : 353 ( 38 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 391 ( 150 ~; 166 |; 53 &)
% ( 2 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 29 ( 27 usr; 1 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 2 con; 0-3 aty)
% Number of variables : 112 ( 27 sgn 30 !; 2 ?)
% 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(d22_lattice3,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] : k16_lattice3(A,B) = k15_lattice3(A,a_2_1_lattice3(A,B)) ),
file('theBenchmark.p',d22_lattice3) ).
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_k15_lattice3,axiom,
! [A,B] :
( ( l3_lattices(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k15_lattice3(A,B),u1_struct_0(A)) ),
file('theBenchmark.p',dt_k15_lattice3) ).
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_l1_lattices,axiom,
! [A] :
( l1_lattices(A)
=> l1_struct_0(A) ),
file('theBenchmark.p',dt_l1_lattices) ).
fof(dt_l3_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( l2_lattices(A)
& l1_lattices(A) ) ),
file('theBenchmark.p',dt_l3_lattices) ).
fof(fc1_struct_0,axiom,
! [A] :
( ( l1_struct_0(A)
& ~ v3_struct_0(A) )
=> ~ v1_xboole_0(u1_struct_0(A)) ),
file('theBenchmark.p',fc1_struct_0) ).
fof(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_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(t35_conlat_1,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ! [B] :
( r2_hidden(B,k8_conlat_1(A))
<=> ( l3_conlat_1(B,A)
& v9_conlat_1(B,A)
& ~ v7_conlat_1(B,A)
& v6_conlat_1(B,A) ) ) ),
file('theBenchmark.p',t35_conlat_1) ).
fof(t4_conlat_2,conjecture,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k11_conlat_1(A))))
=> ( l3_conlat_1(k15_lattice3(k11_conlat_1(A),B),A)
& v9_conlat_1(k15_lattice3(k11_conlat_1(A),B),A)
& ~ v7_conlat_1(k15_lattice3(k11_conlat_1(A),B),A)
& l3_conlat_1(k16_lattice3(k11_conlat_1(A),B),A)
& v9_conlat_1(k16_lattice3(k11_conlat_1(A),B),A)
& ~ v7_conlat_1(k16_lattice3(k11_conlat_1(A),B),A) ) ) ),
file('theBenchmark.p',t4_conlat_2) ).
fof(t4_conlat_2_neg,negated_conjecture,
~ ! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k11_conlat_1(A))))
=> ( l3_conlat_1(k15_lattice3(k11_conlat_1(A),B),A)
& v9_conlat_1(k15_lattice3(k11_conlat_1(A),B),A)
& ~ v7_conlat_1(k15_lattice3(k11_conlat_1(A),B),A)
& l3_conlat_1(k16_lattice3(k11_conlat_1(A),B),A)
& v9_conlat_1(k16_lattice3(k11_conlat_1(A),B),A)
& ~ v7_conlat_1(k16_lattice3(k11_conlat_1(A),B),A) ) ) ),
inference(assume_negation,[status(cth)],[t4_conlat_2]) ).
cnf(c_109,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_110,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_111,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_114,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_117,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_118,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_119,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_120,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_145,plain,
( ~ v3_struct_0(k11_conlat_1(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[fc5_conlat_1]) ).
cnf(c_146,plain,
( v3_lattices(k11_conlat_1(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[fc5_conlat_1]) ).
cnf(c_164,plain,
( ~ v7_conlat_1(B,A)
| ~ r2_hidden(B,k8_conlat_1(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[t35_conlat_1]) ).
cnf(c_165,plain,
( v9_conlat_1(B,A)
| ~ r2_hidden(B,k8_conlat_1(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[t35_conlat_1]) ).
cnf(c_166,plain,
( l3_conlat_1(B,A)
| ~ r2_hidden(B,k8_conlat_1(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(clausify,[status(thm)],[t35_conlat_1]) ).
fof(nnf_105,plain,
? [A] :
( ? [B] :
( ( ~ l3_conlat_1(k15_lattice3(k11_conlat_1(A),B),A)
| ~ v9_conlat_1(k15_lattice3(k11_conlat_1(A),B),A)
| v7_conlat_1(k15_lattice3(k11_conlat_1(A),B),A)
| ~ l3_conlat_1(k16_lattice3(k11_conlat_1(A),B),A)
| ~ v9_conlat_1(k16_lattice3(k11_conlat_1(A),B),A)
| v7_conlat_1(k16_lattice3(k11_conlat_1(A),B),A) )
& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k11_conlat_1(A)))) )
& l2_conlat_1(A)
& ~ v3_conlat_1(A) ),
inference(fof_nnf,[status(thm)],[t4_conlat_2_neg]) ).
fof(sk_t4_conlat_2_neg,plain,
( ( ~ l3_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ v9_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| v7_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ l3_conlat_1(k16_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ v9_conlat_1(k16_lattice3(k11_conlat_1(sK0),sK1),sK0)
| v7_conlat_1(k16_lattice3(k11_conlat_1(sK0),sK1),sK0) )
& m1_subset_1(sK1,k1_zfmisc_1(u1_struct_0(k11_conlat_1(sK0))))
& l2_conlat_1(sK0)
& ~ v3_conlat_1(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(A,sK0),skolemize(B,sK1)],[nnf_105]) ).
cnf(c_168,negated_conjecture,
l2_conlat_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t4_conlat_2_neg]) ).
cnf(c_175,negated_conjecture,
( l3_lattices(k11_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_168,c_114]) ).
cnf(c_181,plain,
( l1_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_183,plain,
( m1_subset_1(k15_lattice3(A,B),u1_struct_0(A))
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k15_lattice3]) ).
cnf(c_185,plain,
( k15_lattice3(A,a_2_1_lattice3(A,B)) = k16_lattice3(A,B)
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d22_lattice3]) ).
cnf(c_196,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_235,plain,
( m1_relset_1(A,B,C)
| ~ m2_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_m2_relset_1]) ).
cnf(c_239,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_168,c_109]) ).
cnf(c_240,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_168,c_117]) ).
cnf(c_252,plain,
( l1_struct_0(A)
| ~ l1_lattices(A) ),
inference(clausify,[status(thm)],[dt_l1_lattices]) ).
cnf(c_259,negated_conjecture,
( v3_conlat_1(sK0)
| l1_lattices(k11_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_181,c_175]) ).
cnf(c_263,plain,
( ~ v1_xboole_0(u1_struct_0(A))
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_struct_0]) ).
cnf(c_273,negated_conjecture,
( l1_struct_0(k11_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_259,c_252]) ).
cnf(c_405,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_196,c_175]) ).
cnf(c_493,negated_conjecture,
( v3_conlat_1(sK0)
| k15_lattice3(k11_conlat_1(sK0),a_2_1_lattice3(k11_conlat_1(sK0),A)) = k16_lattice3(k11_conlat_1(sK0),A)
| v3_struct_0(k11_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_185,c_175]) ).
cnf(c_494,negated_conjecture,
( v3_conlat_1(sK0)
| k16_lattice3(k11_conlat_1(sK0),A) = k15_lattice3(k11_conlat_1(sK0),a_2_1_lattice3(k11_conlat_1(sK0),A))
| v3_struct_0(k11_conlat_1(sK0)) ),
inference(copy,[status(thm)],[c_493]) ).
cnf(c_515,negated_conjecture,
( v3_conlat_1(sK0)
| m1_subset_1(k15_lattice3(k11_conlat_1(sK0),A),u1_struct_0(k11_conlat_1(sK0)))
| v3_struct_0(k11_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_183,c_175]) ).
cnf(c_566,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_606,plain,
( r2_hidden(A,B)
| v1_xboole_0(B)
| ~ m1_subset_1(A,B) ),
inference(clausify,[status(thm)],[t2_subset]) ).
cnf(c_614,negated_conjecture,
~ v3_conlat_1(sK0),
inference(split_conjunct,[status(thm)],[sk_t4_conlat_2_neg]) ).
cnf(c_616,negated_conjecture,
( ~ l3_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ v9_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| v7_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ l3_conlat_1(k16_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ v9_conlat_1(k16_lattice3(k11_conlat_1(sK0),sK1),sK0)
| v7_conlat_1(k16_lattice3(k11_conlat_1(sK0),sK1),sK0) ),
inference(split_conjunct,[status(thm)],[sk_t4_conlat_2_neg]) ).
cnf(c_653,negated_conjecture,
( l3_conlat_1(A,sK0)
| ~ r2_hidden(A,k8_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_168,c_166]) ).
cnf(c_654,negated_conjecture,
( l3_conlat_1(A,sK0)
| ~ r2_hidden(A,k8_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_614,c_653]) ).
cnf(c_655,negated_conjecture,
( v9_conlat_1(A,sK0)
| ~ r2_hidden(A,k8_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_168,c_165]) ).
cnf(c_656,negated_conjecture,
( v9_conlat_1(A,sK0)
| ~ r2_hidden(A,k8_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_614,c_655]) ).
cnf(c_657,negated_conjecture,
( ~ v7_conlat_1(A,sK0)
| ~ r2_hidden(A,k8_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_168,c_164]) ).
cnf(c_658,negated_conjecture,
( ~ v7_conlat_1(A,sK0)
| ~ r2_hidden(A,k8_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_614,c_657]) ).
cnf(c_691,negated_conjecture,
( v3_lattices(k11_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_168,c_146]) ).
cnf(c_692,negated_conjecture,
v3_lattices(k11_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_614,c_691]) ).
cnf(c_693,negated_conjecture,
( ~ v3_struct_0(k11_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_168,c_145]) ).
cnf(c_694,negated_conjecture,
~ v3_struct_0(k11_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_614,c_693]) ).
cnf(c_707,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_168,c_110]) ).
cnf(c_708,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_614,c_707]) ).
cnf(c_709,negated_conjecture,
( v1_funct_1(k9_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_168,c_111]) ).
cnf(c_710,negated_conjecture,
v1_funct_1(k9_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_614,c_709]) ).
cnf(c_713,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_168,c_118]) ).
cnf(c_714,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_614,c_713]) ).
cnf(c_715,negated_conjecture,
( v1_funct_1(k10_conlat_1(sK0))
| v3_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_168,c_119]) ).
cnf(c_716,negated_conjecture,
v1_funct_1(k10_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_614,c_715]) ).
cnf(c_717,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_168,c_120]) ).
cnf(c_718,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_614,c_717]) ).
cnf(c_812,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_239,c_235]) ).
cnf(c_813,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_614,c_812]) ).
cnf(c_816,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_240,c_235]) ).
cnf(c_817,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_614,c_816]) ).
cnf(c_828,negated_conjecture,
( v3_conlat_1(sK0)
| ~ v1_xboole_0(u1_struct_0(k11_conlat_1(sK0)))
| v3_struct_0(k11_conlat_1(sK0)) ),
inference(resolve,[status(thm)],[c_263,c_273]) ).
cnf(c_10819,negated_conjecture,
( v3_conlat_1(sK0)
| ~ v1_xboole_0(u1_struct_0(k11_conlat_1(sK0))) ),
inference(resolve,[status(thm)],[c_694,c_828]) ).
cnf(c_829,negated_conjecture,
~ v1_xboole_0(u1_struct_0(k11_conlat_1(sK0))),
inference(resolve,[status(thm)],[c_614,c_10819]) ).
cnf(c_10820,negated_conjecture,
( v3_conlat_1(sK0)
| m1_subset_1(k15_lattice3(k11_conlat_1(sK0),A),u1_struct_0(k11_conlat_1(sK0))) ),
inference(resolve,[status(thm)],[c_694,c_515]) ).
cnf(c_936,negated_conjecture,
m1_subset_1(k15_lattice3(k11_conlat_1(sK0),A),u1_struct_0(k11_conlat_1(sK0))),
inference(resolve,[status(thm)],[c_614,c_10820]) ).
cnf(c_10821,negated_conjecture,
( v3_conlat_1(sK0)
| k16_lattice3(k11_conlat_1(sK0),A) = k15_lattice3(k11_conlat_1(sK0),a_2_1_lattice3(k11_conlat_1(sK0),A)) ),
inference(resolve,[status(thm)],[c_694,c_494]) ).
cnf(c_937,negated_conjecture,
k16_lattice3(k11_conlat_1(sK0),A) = k15_lattice3(k11_conlat_1(sK0),a_2_1_lattice3(k11_conlat_1(sK0),A)),
inference(resolve,[status(thm)],[c_614,c_10821]) ).
cnf(c_10822,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_692,c_405]) ).
cnf(c_938,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_614,c_10822]) ).
cnf(c_10823,negated_conjecture,
( ~ l3_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ v9_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| v7_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ l3_conlat_1(k16_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ v9_conlat_1(k16_lattice3(k11_conlat_1(sK0),sK1),sK0)
| v7_conlat_1(k15_lattice3(k11_conlat_1(sK0),a_2_1_lattice3(k11_conlat_1(sK0),sK1)),sK0) ),
inference(paramod,[status(thm)],[c_937,c_616]) ).
cnf(c_10824,negated_conjecture,
( ~ l3_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ v9_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| v7_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ l3_conlat_1(k16_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ v9_conlat_1(k15_lattice3(k11_conlat_1(sK0),a_2_1_lattice3(k11_conlat_1(sK0),sK1)),sK0)
| v7_conlat_1(k15_lattice3(k11_conlat_1(sK0),a_2_1_lattice3(k11_conlat_1(sK0),sK1)),sK0) ),
inference(paramod,[status(thm)],[c_937,c_10823]) ).
cnf(c_947,negated_conjecture,
( ~ l3_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ v9_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| v7_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ l3_conlat_1(k15_lattice3(k11_conlat_1(sK0),a_2_1_lattice3(k11_conlat_1(sK0),sK1)),sK0)
| ~ v9_conlat_1(k15_lattice3(k11_conlat_1(sK0),a_2_1_lattice3(k11_conlat_1(sK0),sK1)),sK0)
| v7_conlat_1(k15_lattice3(k11_conlat_1(sK0),a_2_1_lattice3(k11_conlat_1(sK0),sK1)),sK0) ),
inference(paramod,[status(thm)],[c_937,c_10824]) ).
cnf(c_10825,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_718,c_566]) ).
cnf(c_10826,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_10825]) ).
cnf(c_10827,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_716,c_10826]) ).
cnf(c_10828,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_714,c_10827]) ).
cnf(c_10829,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_817,c_10828]) ).
cnf(c_10830,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_710,c_10829]) ).
cnf(c_10831,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_708,c_10830]) ).
cnf(c_4549,negated_conjecture,
( k8_conlat_1(sK0) = A
| g3_lattices(A,B,C) != k11_conlat_1(sK0) ),
inference(resolve,[status(thm)],[c_813,c_10831]) ).
cnf(c_10832,negated_conjecture,
( r2_hidden(k15_lattice3(k11_conlat_1(sK0),A),u1_struct_0(k11_conlat_1(sK0)))
| v1_xboole_0(u1_struct_0(k11_conlat_1(sK0))) ),
inference(resolve,[status(thm)],[c_936,c_606]) ).
cnf(c_6157,negated_conjecture,
r2_hidden(k15_lattice3(k11_conlat_1(sK0),A),u1_struct_0(k11_conlat_1(sK0))),
inference(resolve,[status(thm)],[c_829,c_10832]) ).
cnf(c_8770,plain,
k8_conlat_1(sK0) = u1_struct_0(k11_conlat_1(sK0)),
inference(resolve,[status(thm)],[c_4549,c_938]) ).
cnf(c_9030,negated_conjecture,
( ~ v7_conlat_1(A,sK0)
| ~ r2_hidden(A,u1_struct_0(k11_conlat_1(sK0))) ),
inference(paramod,[status(thm)],[c_8770,c_658]) ).
cnf(c_9031,negated_conjecture,
( v9_conlat_1(A,sK0)
| ~ r2_hidden(A,u1_struct_0(k11_conlat_1(sK0))) ),
inference(paramod,[status(thm)],[c_8770,c_656]) ).
cnf(c_9032,negated_conjecture,
( l3_conlat_1(A,sK0)
| ~ r2_hidden(A,u1_struct_0(k11_conlat_1(sK0))) ),
inference(paramod,[status(thm)],[c_8770,c_654]) ).
cnf(c_10801,plain,
~ v7_conlat_1(k15_lattice3(k11_conlat_1(sK0),A),sK0),
inference(resolve,[status(thm)],[c_6157,c_9030]) ).
cnf(c_10833,negated_conjecture,
( ~ l3_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ v9_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| v7_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ l3_conlat_1(k15_lattice3(k11_conlat_1(sK0),a_2_1_lattice3(k11_conlat_1(sK0),sK1)),sK0)
| ~ v9_conlat_1(k15_lattice3(k11_conlat_1(sK0),a_2_1_lattice3(k11_conlat_1(sK0),sK1)),sK0) ),
inference(resolve,[status(thm)],[c_10801,c_947]) ).
cnf(c_10804,negated_conjecture,
( ~ l3_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ v9_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ l3_conlat_1(k15_lattice3(k11_conlat_1(sK0),a_2_1_lattice3(k11_conlat_1(sK0),sK1)),sK0)
| ~ v9_conlat_1(k15_lattice3(k11_conlat_1(sK0),a_2_1_lattice3(k11_conlat_1(sK0),sK1)),sK0) ),
inference(resolve,[status(thm)],[c_10801,c_10833]) ).
cnf(c_10811,plain,
v9_conlat_1(k15_lattice3(k11_conlat_1(sK0),A),sK0),
inference(resolve,[status(thm)],[c_9031,c_6157]) ).
cnf(c_10834,negated_conjecture,
( ~ l3_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ v9_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ l3_conlat_1(k15_lattice3(k11_conlat_1(sK0),a_2_1_lattice3(k11_conlat_1(sK0),sK1)),sK0) ),
inference(resolve,[status(thm)],[c_10811,c_10804]) ).
cnf(c_10814,negated_conjecture,
( ~ l3_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0)
| ~ l3_conlat_1(k15_lattice3(k11_conlat_1(sK0),a_2_1_lattice3(k11_conlat_1(sK0),sK1)),sK0) ),
inference(resolve,[status(thm)],[c_10811,c_10834]) ).
cnf(c_10815,plain,
l3_conlat_1(k15_lattice3(k11_conlat_1(sK0),A),sK0),
inference(resolve,[status(thm)],[c_9032,c_6157]) ).
cnf(c_10835,negated_conjecture,
~ l3_conlat_1(k15_lattice3(k11_conlat_1(sK0),sK1),sK0),
inference(resolve,[status(thm)],[c_10815,c_10814]) ).
cnf(c_10818,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_10815,c_10835]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT338+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n003.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Fri Sep 25 21:03:54 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 1068289 was started by sandbox2 on n003,
% 0.09/0.36 % Fri Sep 25 21:03:54 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.13/0.37
% 0.13/0.37 % From the command line: assign(max_seconds, 300).
% 17.94/3.06
% 17.94/3.06 % given #500 (F,wt=17): 6935 -m1_subset_1(u1_struct_0(c12),k1_zfmisc_1(A)) | -v1_xboole_0(A). [resolve(6107,a,610,a)].
% 17.94/3.06
% 17.94/3.06 % SZS status Theorem for theBenchmark
% 17.94/3.06
% 17.94/3.06 % Proof 1 at 2.09 (+ 0.43) seconds.
% 17.94/3.06 % Length of proof is 92.
% 17.94/3.06 % Level of proof is 11.
% 17.94/3.06 % Maximum clause weight is 65.000.
% 17.94/3.06 % Given clauses 974.
% 17.94/3.06
% 17.94/3.06 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------