%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT297+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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:04 AM UTC 2026
% Result : Theorem 113.19s 15.78s
% Output : CNFRefutation 113.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 8
% Syntax : Number of formulae : 106 ( 23 unt; 0 def)
% Number of atoms : 493 ( 26 equ)
% Maximal formula atoms : 51 ( 4 avg)
% Number of connectives : 632 ( 245 ~; 289 |; 70 &)
% ( 4 <=>; 24 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 2 con; 0-3 aty)
% Number of variables : 148 ( 0 sgn 62 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cc1_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( ( v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A) ) ) ),
file('theBenchmark.p',cc1_lattices) ).
fof(d10_lattice4,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( m2_lattice4(B,A)
<=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ! [D] :
( m1_subset_1(D,u1_struct_0(A))
=> ( ( r2_hidden(D,B)
& r2_hidden(C,B) )
=> ( r2_hidden(k3_lattices(A,C,D),B)
& r2_hidden(k4_lattices(A,C,D),B) ) ) ) ) ) ) ),
file('theBenchmark.p',d10_lattice4) ).
fof(d9_lattices,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_struct_0(A) )
=> ( v9_lattices(A)
<=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> k2_lattices(A,B,k1_lattices(A,B,C)) = B ) ) ) ),
file('theBenchmark.p',d9_lattices) ).
fof(dt_k3_lattices,axiom,
! [A,B,C] :
( ( m1_subset_1(C,u1_struct_0(A))
& m1_subset_1(B,u1_struct_0(A))
& l2_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k3_lattices(A,B,C),u1_struct_0(A)) ),
file('theBenchmark.p',dt_k3_lattices) ).
fof(dt_l3_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( l2_lattices(A)
& l1_lattices(A) ) ),
file('theBenchmark.p',dt_l3_lattices) ).
fof(redefinition_k3_lattices,axiom,
! [A,B,C] :
( ( m1_subset_1(C,u1_struct_0(A))
& m1_subset_1(B,u1_struct_0(A))
& l2_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A) )
=> k3_lattices(A,B,C) = k1_lattices(A,B,C) ),
file('theBenchmark.p',redefinition_k3_lattices) ).
fof(redefinition_k4_lattices,axiom,
! [A,B,C] :
( ( m1_subset_1(C,u1_struct_0(A))
& m1_subset_1(B,u1_struct_0(A))
& l1_lattices(A)
& v6_lattices(A)
& ~ v3_struct_0(A) )
=> k4_lattices(A,B,C) = k2_lattices(A,B,C) ),
file('theBenchmark.p',redefinition_k4_lattices) ).
fof(t13_filter_2,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ! [D] :
( m1_subset_1(D,u1_struct_0(A))
=> ( ( r2_hidden(D,B)
& r2_hidden(C,B) )
<=> r2_hidden(k4_lattices(A,C,D),B) ) ) )
=> m2_lattice4(B,A) ) ) ),
file('theBenchmark.p',t13_filter_2) ).
fof(t13_filter_2_neg,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> ( ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ! [D] :
( m1_subset_1(D,u1_struct_0(A))
=> ( ( r2_hidden(D,B)
& r2_hidden(C,B) )
<=> r2_hidden(k4_lattices(A,C,D),B) ) ) )
=> m2_lattice4(B,A) ) ) ),
inference(assume_negation,[status(cth)],[t13_filter_2]) ).
cnf(c_86,plain,
( v9_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc1_lattices]) ).
cnf(c_89,plain,
( v6_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc1_lattices]) ).
cnf(c_91,plain,
( v4_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc1_lattices]) ).
fof(nnf_11,plain,
! [A] :
( ! [B] :
( ( ( ? [C] :
( ? [D] :
( ( ~ r2_hidden(k3_lattices(A,C,D),B)
| ~ r2_hidden(k4_lattices(A,C,D),B) )
& r2_hidden(D,B)
& r2_hidden(C,B)
& m1_subset_1(D,u1_struct_0(A)) )
& m1_subset_1(C,u1_struct_0(A)) )
| m2_lattice4(B,A) )
& ( ! [X0] :
( ! [X1] :
( ( r2_hidden(k3_lattices(A,X0,X1),B)
& r2_hidden(k4_lattices(A,X0,X1),B) )
| ~ r2_hidden(X1,B)
| ~ r2_hidden(X0,B)
| ~ m1_subset_1(X1,u1_struct_0(A)) )
| ~ m1_subset_1(X0,u1_struct_0(A)) )
| ~ m2_lattice4(B,A) ) )
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[d10_lattice4]) ).
fof(sk_d10_lattice4_sk,plain,
! [A] :
( ! [B] :
( ( ( ( ( ~ r2_hidden(k3_lattices(A,sK0(A,B),sK1(A,B)),B)
| ~ r2_hidden(k4_lattices(A,sK0(A,B),sK1(A,B)),B) )
& r2_hidden(sK1(A,B),B)
& r2_hidden(sK0(A,B),B)
& m1_subset_1(sK1(A,B),u1_struct_0(A))
& m1_subset_1(sK0(A,B),u1_struct_0(A)) )
| m2_lattice4(B,A) )
& ( ! [X0] :
( ! [X1] :
( ( r2_hidden(k3_lattices(A,X0,X1),B)
& r2_hidden(k4_lattices(A,X0,X1),B) )
| ~ r2_hidden(X1,B)
| ~ r2_hidden(X0,B)
| ~ m1_subset_1(X1,u1_struct_0(A)) )
| ~ m1_subset_1(X0,u1_struct_0(A)) )
| ~ m2_lattice4(B,A) ) )
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(C,sK0(A,B)),skolemize(D,sK1(A,B))],[nnf_11]) ).
fof(sk_d10_lattice4,plain,
( ! [VAR_0,VAR_1] :
( ~ r2_hidden(k3_lattices(VAR_0,sK0(VAR_0,VAR_1),sK1(VAR_0,VAR_1)),VAR_1)
| ~ r2_hidden(k4_lattices(VAR_0,sK0(VAR_0,VAR_1),sK1(VAR_0,VAR_1)),VAR_1)
| m2_lattice4(VAR_1,VAR_0)
| ~ m1_subset_1(VAR_1,k1_zfmisc_1(u1_struct_0(VAR_0)))
| ~ l3_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1] :
( r2_hidden(sK1(VAR_0,VAR_1),VAR_1)
| m2_lattice4(VAR_1,VAR_0)
| ~ m1_subset_1(VAR_1,k1_zfmisc_1(u1_struct_0(VAR_0)))
| ~ l3_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1] :
( r2_hidden(sK0(VAR_0,VAR_1),VAR_1)
| m2_lattice4(VAR_1,VAR_0)
| ~ m1_subset_1(VAR_1,k1_zfmisc_1(u1_struct_0(VAR_0)))
| ~ l3_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1] :
( m1_subset_1(sK1(VAR_0,VAR_1),u1_struct_0(VAR_0))
| m2_lattice4(VAR_1,VAR_0)
| ~ m1_subset_1(VAR_1,k1_zfmisc_1(u1_struct_0(VAR_0)))
| ~ l3_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1] :
( m1_subset_1(sK0(VAR_0,VAR_1),u1_struct_0(VAR_0))
| m2_lattice4(VAR_1,VAR_0)
| ~ m1_subset_1(VAR_1,k1_zfmisc_1(u1_struct_0(VAR_0)))
| ~ l3_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( r2_hidden(k3_lattices(VAR_0,VAR_2,VAR_3),VAR_1)
| ~ r2_hidden(VAR_3,VAR_1)
| ~ r2_hidden(VAR_2,VAR_1)
| ~ m1_subset_1(VAR_3,u1_struct_0(VAR_0))
| ~ m1_subset_1(VAR_2,u1_struct_0(VAR_0))
| ~ m2_lattice4(VAR_1,VAR_0)
| ~ m1_subset_1(VAR_1,k1_zfmisc_1(u1_struct_0(VAR_0)))
| ~ l3_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( r2_hidden(k4_lattices(VAR_0,VAR_2,VAR_3),VAR_1)
| ~ r2_hidden(VAR_3,VAR_1)
| ~ r2_hidden(VAR_2,VAR_1)
| ~ m1_subset_1(VAR_3,u1_struct_0(VAR_0))
| ~ m1_subset_1(VAR_2,u1_struct_0(VAR_0))
| ~ m2_lattice4(VAR_1,VAR_0)
| ~ m1_subset_1(VAR_1,k1_zfmisc_1(u1_struct_0(VAR_0)))
| ~ l3_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d10_lattice4_sk]) ).
cnf(c_94,plain,
( m1_subset_1(sK0(A,B),u1_struct_0(A))
| m2_lattice4(B,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(split_conjunct,[status(thm)],[sk_d10_lattice4]) ).
cnf(c_95,plain,
( m1_subset_1(sK1(A,B),u1_struct_0(A))
| m2_lattice4(B,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(split_conjunct,[status(thm)],[sk_d10_lattice4]) ).
cnf(c_96,plain,
( r2_hidden(sK0(A,B),B)
| m2_lattice4(B,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(split_conjunct,[status(thm)],[sk_d10_lattice4]) ).
cnf(c_97,plain,
( r2_hidden(sK1(A,B),B)
| m2_lattice4(B,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(split_conjunct,[status(thm)],[sk_d10_lattice4]) ).
cnf(c_98,plain,
( ~ r2_hidden(k3_lattices(A,sK0(A,B),sK1(A,B)),B)
| ~ r2_hidden(k4_lattices(A,sK0(A,B),sK1(A,B)),B)
| m2_lattice4(B,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(split_conjunct,[status(thm)],[sk_d10_lattice4]) ).
fof(nnf_84,plain,
? [A] :
( ? [B] :
( ~ m2_lattice4(B,A)
& ! [C] :
( ! [D] :
( ( ( ~ r2_hidden(k4_lattices(A,C,D),B)
| ( r2_hidden(D,B)
& r2_hidden(C,B) ) )
& ( r2_hidden(k4_lattices(A,C,D),B)
| ~ r2_hidden(D,B)
| ~ r2_hidden(C,B) ) )
| ~ m1_subset_1(D,u1_struct_0(A)) )
| ~ m1_subset_1(C,u1_struct_0(A)) )
& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t13_filter_2_neg]) ).
fof(sk_t13_filter_2_neg_sk,plain,
( ~ m2_lattice4(sK3,sK2)
& ! [C] :
( ! [D] :
( ( ( ~ r2_hidden(k4_lattices(sK2,C,D),sK3)
| ( r2_hidden(D,sK3)
& r2_hidden(C,sK3) ) )
& ( r2_hidden(k4_lattices(sK2,C,D),sK3)
| ~ r2_hidden(D,sK3)
| ~ r2_hidden(C,sK3) ) )
| ~ m1_subset_1(D,u1_struct_0(sK2)) )
| ~ m1_subset_1(C,u1_struct_0(sK2)) )
& m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK2)))
& l3_lattices(sK2)
& v10_lattices(sK2)
& ~ v3_struct_0(sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3]),skolemize(A,sK2),skolemize(B,sK3)],[nnf_84]) ).
fof(sk_t13_filter_2_neg,plain,
( ~ m2_lattice4(sK3,sK2)
& ! [VAR_0,VAR_1] :
( ~ r2_hidden(k4_lattices(sK2,VAR_0,VAR_1),sK3)
| r2_hidden(VAR_1,sK3)
| ~ m1_subset_1(VAR_1,u1_struct_0(sK2))
| ~ m1_subset_1(VAR_0,u1_struct_0(sK2)) )
& ! [VAR_0,VAR_1] :
( ~ r2_hidden(k4_lattices(sK2,VAR_0,VAR_1),sK3)
| r2_hidden(VAR_0,sK3)
| ~ m1_subset_1(VAR_1,u1_struct_0(sK2))
| ~ m1_subset_1(VAR_0,u1_struct_0(sK2)) )
& ! [VAR_0,VAR_1] :
( r2_hidden(k4_lattices(sK2,VAR_0,VAR_1),sK3)
| ~ r2_hidden(VAR_1,sK3)
| ~ r2_hidden(VAR_0,sK3)
| ~ m1_subset_1(VAR_1,u1_struct_0(sK2))
| ~ m1_subset_1(VAR_0,u1_struct_0(sK2)) )
& m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK2)))
& l3_lattices(sK2)
& v10_lattices(sK2)
& ~ v3_struct_0(sK2) ),
inference(cnf_transformation,[status(thm)],[sk_t13_filter_2_neg_sk]) ).
cnf(c_103,negated_conjecture,
v10_lattices(sK2),
inference(split_conjunct,[status(thm)],[sk_t13_filter_2_neg]) ).
cnf(c_118,negated_conjecture,
( v4_lattices(sK2)
| v3_struct_0(sK2)
| ~ l3_lattices(sK2) ),
inference(resolve,[status(thm)],[c_103,c_91]) ).
cnf(c_130,plain,
( k1_lattices(A,B,C) = k3_lattices(A,B,C)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l2_lattices(A)
| ~ v4_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[redefinition_k3_lattices]) ).
cnf(c_135,plain,
( m1_subset_1(k3_lattices(A,B,C),u1_struct_0(A))
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l2_lattices(A)
| ~ v4_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k3_lattices]) ).
cnf(c_138,plain,
( l1_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_160,plain,
( k2_lattices(A,B,C) = k4_lattices(A,B,C)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l1_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[redefinition_k4_lattices]) ).
cnf(c_221,plain,
( k2_lattices(A,B,k1_lattices(A,B,C)) = B
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ v9_lattices(A)
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d9_lattices]) ).
cnf(c_226,plain,
( l2_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_261,negated_conjecture,
~ v3_struct_0(sK2),
inference(split_conjunct,[status(thm)],[sk_t13_filter_2_neg]) ).
cnf(c_262,negated_conjecture,
l3_lattices(sK2),
inference(split_conjunct,[status(thm)],[sk_t13_filter_2_neg]) ).
cnf(c_263,negated_conjecture,
m1_subset_1(sK3,k1_zfmisc_1(u1_struct_0(sK2))),
inference(split_conjunct,[status(thm)],[sk_t13_filter_2_neg]) ).
cnf(c_264,negated_conjecture,
( r2_hidden(k4_lattices(sK2,A,B),sK3)
| ~ r2_hidden(B,sK3)
| ~ r2_hidden(A,sK3)
| ~ m1_subset_1(B,u1_struct_0(sK2))
| ~ m1_subset_1(A,u1_struct_0(sK2)) ),
inference(split_conjunct,[status(thm)],[sk_t13_filter_2_neg]) ).
cnf(c_266,negated_conjecture,
( ~ r2_hidden(k4_lattices(sK2,A,B),sK3)
| r2_hidden(B,sK3)
| ~ m1_subset_1(B,u1_struct_0(sK2))
| ~ m1_subset_1(A,u1_struct_0(sK2)) ),
inference(split_conjunct,[status(thm)],[sk_t13_filter_2_neg]) ).
cnf(c_267,negated_conjecture,
~ m2_lattice4(sK3,sK2),
inference(split_conjunct,[status(thm)],[sk_t13_filter_2_neg]) ).
cnf(c_276,negated_conjecture,
( ~ r2_hidden(k3_lattices(sK2,sK0(sK2,A),sK1(sK2,A)),A)
| ~ r2_hidden(k4_lattices(sK2,sK0(sK2,A),sK1(sK2,A)),A)
| m2_lattice4(A,sK2)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ l3_lattices(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_103,c_98]) ).
cnf(c_24045,negated_conjecture,
( ~ r2_hidden(k3_lattices(sK2,sK0(sK2,A),sK1(sK2,A)),A)
| ~ r2_hidden(k4_lattices(sK2,sK0(sK2,A),sK1(sK2,A)),A)
| m2_lattice4(A,sK2)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ l3_lattices(sK2) ),
inference(resolve,[status(thm)],[c_261,c_276]) ).
cnf(c_277,negated_conjecture,
( ~ r2_hidden(k3_lattices(sK2,sK0(sK2,A),sK1(sK2,A)),A)
| ~ r2_hidden(k4_lattices(sK2,sK0(sK2,A),sK1(sK2,A)),A)
| m2_lattice4(A,sK2)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK2))) ),
inference(resolve,[status(thm)],[c_262,c_24045]) ).
cnf(c_278,negated_conjecture,
( r2_hidden(sK1(sK2,A),A)
| m2_lattice4(A,sK2)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ l3_lattices(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_103,c_97]) ).
cnf(c_24046,negated_conjecture,
( r2_hidden(sK1(sK2,A),A)
| m2_lattice4(A,sK2)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ l3_lattices(sK2) ),
inference(resolve,[status(thm)],[c_261,c_278]) ).
cnf(c_279,negated_conjecture,
( r2_hidden(sK1(sK2,A),A)
| m2_lattice4(A,sK2)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK2))) ),
inference(resolve,[status(thm)],[c_262,c_24046]) ).
cnf(c_280,negated_conjecture,
( r2_hidden(sK0(sK2,A),A)
| m2_lattice4(A,sK2)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ l3_lattices(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_103,c_96]) ).
cnf(c_24047,negated_conjecture,
( r2_hidden(sK0(sK2,A),A)
| m2_lattice4(A,sK2)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ l3_lattices(sK2) ),
inference(resolve,[status(thm)],[c_261,c_280]) ).
cnf(c_281,negated_conjecture,
( r2_hidden(sK0(sK2,A),A)
| m2_lattice4(A,sK2)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK2))) ),
inference(resolve,[status(thm)],[c_262,c_24047]) ).
cnf(c_282,negated_conjecture,
( m1_subset_1(sK1(sK2,A),u1_struct_0(sK2))
| m2_lattice4(A,sK2)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ l3_lattices(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_103,c_95]) ).
cnf(c_24048,negated_conjecture,
( m1_subset_1(sK1(sK2,A),u1_struct_0(sK2))
| m2_lattice4(A,sK2)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ l3_lattices(sK2) ),
inference(resolve,[status(thm)],[c_261,c_282]) ).
cnf(c_283,negated_conjecture,
( m1_subset_1(sK1(sK2,A),u1_struct_0(sK2))
| m2_lattice4(A,sK2)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK2))) ),
inference(resolve,[status(thm)],[c_262,c_24048]) ).
cnf(c_284,negated_conjecture,
( m1_subset_1(sK0(sK2,A),u1_struct_0(sK2))
| m2_lattice4(A,sK2)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ l3_lattices(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_103,c_94]) ).
cnf(c_24049,negated_conjecture,
( m1_subset_1(sK0(sK2,A),u1_struct_0(sK2))
| m2_lattice4(A,sK2)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK2)))
| ~ l3_lattices(sK2) ),
inference(resolve,[status(thm)],[c_261,c_284]) ).
cnf(c_285,negated_conjecture,
( m1_subset_1(sK0(sK2,A),u1_struct_0(sK2))
| m2_lattice4(A,sK2)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK2))) ),
inference(resolve,[status(thm)],[c_262,c_24049]) ).
cnf(c_290,negated_conjecture,
( v9_lattices(sK2)
| v3_struct_0(sK2)
| ~ l3_lattices(sK2) ),
inference(resolve,[status(thm)],[c_103,c_86]) ).
cnf(c_24050,negated_conjecture,
( v9_lattices(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_262,c_290]) ).
cnf(c_291,negated_conjecture,
v9_lattices(sK2),
inference(resolve,[status(thm)],[c_261,c_24050]) ).
cnf(c_296,negated_conjecture,
( v6_lattices(sK2)
| v3_struct_0(sK2)
| ~ l3_lattices(sK2) ),
inference(resolve,[status(thm)],[c_103,c_89]) ).
cnf(c_24051,negated_conjecture,
( v6_lattices(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_262,c_296]) ).
cnf(c_297,negated_conjecture,
v6_lattices(sK2),
inference(resolve,[status(thm)],[c_261,c_24051]) ).
cnf(c_311,negated_conjecture,
( k1_lattices(sK2,A,B) = k3_lattices(sK2,A,B)
| ~ m1_subset_1(B,u1_struct_0(sK2))
| ~ m1_subset_1(A,u1_struct_0(sK2))
| ~ l2_lattices(sK2)
| v3_struct_0(sK2)
| v3_struct_0(sK2)
| ~ l3_lattices(sK2) ),
inference(resolve,[status(thm)],[c_118,c_130]) ).
cnf(c_24052,negated_conjecture,
( k1_lattices(sK2,A,B) = k3_lattices(sK2,A,B)
| ~ m1_subset_1(B,u1_struct_0(sK2))
| ~ m1_subset_1(A,u1_struct_0(sK2))
| ~ l2_lattices(sK2)
| v3_struct_0(sK2)
| ~ l3_lattices(sK2) ),
inference(copy,[status(thm)],[c_311]) ).
cnf(c_24053,negated_conjecture,
( k1_lattices(sK2,A,B) = k3_lattices(sK2,A,B)
| ~ m1_subset_1(B,u1_struct_0(sK2))
| ~ m1_subset_1(A,u1_struct_0(sK2))
| ~ l2_lattices(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_262,c_24052]) ).
cnf(c_312,negated_conjecture,
( k1_lattices(sK2,A,B) = k3_lattices(sK2,A,B)
| ~ m1_subset_1(B,u1_struct_0(sK2))
| ~ m1_subset_1(A,u1_struct_0(sK2))
| ~ l2_lattices(sK2) ),
inference(resolve,[status(thm)],[c_261,c_24053]) ).
cnf(c_316,negated_conjecture,
( m1_subset_1(k3_lattices(sK2,A,B),u1_struct_0(sK2))
| ~ m1_subset_1(B,u1_struct_0(sK2))
| ~ m1_subset_1(A,u1_struct_0(sK2))
| ~ l2_lattices(sK2)
| v3_struct_0(sK2)
| v3_struct_0(sK2)
| ~ l3_lattices(sK2) ),
inference(resolve,[status(thm)],[c_118,c_135]) ).
cnf(c_24054,negated_conjecture,
( m1_subset_1(k3_lattices(sK2,A,B),u1_struct_0(sK2))
| ~ m1_subset_1(B,u1_struct_0(sK2))
| ~ m1_subset_1(A,u1_struct_0(sK2))
| ~ l2_lattices(sK2)
| v3_struct_0(sK2)
| ~ l3_lattices(sK2) ),
inference(copy,[status(thm)],[c_316]) ).
cnf(c_24055,negated_conjecture,
( m1_subset_1(k3_lattices(sK2,A,B),u1_struct_0(sK2))
| ~ m1_subset_1(B,u1_struct_0(sK2))
| ~ m1_subset_1(A,u1_struct_0(sK2))
| ~ l2_lattices(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_262,c_24054]) ).
cnf(c_317,negated_conjecture,
( m1_subset_1(k3_lattices(sK2,A,B),u1_struct_0(sK2))
| ~ m1_subset_1(B,u1_struct_0(sK2))
| ~ m1_subset_1(A,u1_struct_0(sK2))
| ~ l2_lattices(sK2) ),
inference(resolve,[status(thm)],[c_261,c_24055]) ).
cnf(c_350,plain,
( ~ l3_lattices(A)
| k2_lattices(A,B,C) = k4_lattices(A,B,C)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_160,c_138]) ).
cnf(c_664,plain,
l2_lattices(sK2),
inference(resolve,[status(thm)],[c_262,c_226]) ).
cnf(c_672,negated_conjecture,
( m1_subset_1(k3_lattices(sK2,A,B),u1_struct_0(sK2))
| ~ m1_subset_1(B,u1_struct_0(sK2))
| ~ m1_subset_1(A,u1_struct_0(sK2)) ),
inference(resolve,[status(thm)],[c_664,c_317]) ).
cnf(c_674,negated_conjecture,
( k1_lattices(sK2,A,B) = k3_lattices(sK2,A,B)
| ~ m1_subset_1(B,u1_struct_0(sK2))
| ~ m1_subset_1(A,u1_struct_0(sK2)) ),
inference(resolve,[status(thm)],[c_664,c_312]) ).
cnf(c_24056,negated_conjecture,
( ~ r2_hidden(k3_lattices(sK2,sK0(sK2,sK3),sK1(sK2,sK3)),sK3)
| ~ r2_hidden(k4_lattices(sK2,sK0(sK2,sK3),sK1(sK2,sK3)),sK3)
| m2_lattice4(sK3,sK2) ),
inference(resolve,[status(thm)],[c_277,c_263]) ).
cnf(c_699,negated_conjecture,
( ~ r2_hidden(k3_lattices(sK2,sK0(sK2,sK3),sK1(sK2,sK3)),sK3)
| ~ r2_hidden(k4_lattices(sK2,sK0(sK2,sK3),sK1(sK2,sK3)),sK3) ),
inference(resolve,[status(thm)],[c_267,c_24056]) ).
cnf(c_24057,negated_conjecture,
( r2_hidden(sK1(sK2,sK3),sK3)
| m2_lattice4(sK3,sK2) ),
inference(resolve,[status(thm)],[c_279,c_263]) ).
cnf(c_703,negated_conjecture,
r2_hidden(sK1(sK2,sK3),sK3),
inference(resolve,[status(thm)],[c_267,c_24057]) ).
cnf(c_24058,negated_conjecture,
( r2_hidden(sK0(sK2,sK3),sK3)
| m2_lattice4(sK3,sK2) ),
inference(resolve,[status(thm)],[c_281,c_263]) ).
cnf(c_707,negated_conjecture,
r2_hidden(sK0(sK2,sK3),sK3),
inference(resolve,[status(thm)],[c_267,c_24058]) ).
cnf(c_24059,negated_conjecture,
( m1_subset_1(sK1(sK2,sK3),u1_struct_0(sK2))
| m2_lattice4(sK3,sK2) ),
inference(resolve,[status(thm)],[c_283,c_263]) ).
cnf(c_711,negated_conjecture,
m1_subset_1(sK1(sK2,sK3),u1_struct_0(sK2)),
inference(resolve,[status(thm)],[c_267,c_24059]) ).
cnf(c_24060,negated_conjecture,
( m1_subset_1(sK0(sK2,sK3),u1_struct_0(sK2))
| m2_lattice4(sK3,sK2) ),
inference(resolve,[status(thm)],[c_285,c_263]) ).
cnf(c_715,negated_conjecture,
m1_subset_1(sK0(sK2,sK3),u1_struct_0(sK2)),
inference(resolve,[status(thm)],[c_267,c_24060]) ).
cnf(c_24061,negated_conjecture,
( r2_hidden(k4_lattices(sK2,A,sK1(sK2,sK3)),sK3)
| ~ r2_hidden(A,sK3)
| ~ m1_subset_1(sK1(sK2,sK3),u1_struct_0(sK2))
| ~ m1_subset_1(A,u1_struct_0(sK2)) ),
inference(resolve,[status(thm)],[c_703,c_264]) ).
cnf(c_1381,negated_conjecture,
( r2_hidden(k4_lattices(sK2,A,sK1(sK2,sK3)),sK3)
| ~ r2_hidden(A,sK3)
| ~ m1_subset_1(A,u1_struct_0(sK2)) ),
inference(resolve,[status(thm)],[c_711,c_24061]) ).
cnf(c_24062,plain,
( k2_lattices(sK2,A,k1_lattices(sK2,A,sK1(sK2,sK3))) = A
| ~ m1_subset_1(A,u1_struct_0(sK2))
| ~ v9_lattices(sK2)
| ~ l3_lattices(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_711,c_221]) ).
cnf(c_24063,negated_conjecture,
( k2_lattices(sK2,A,k1_lattices(sK2,A,sK1(sK2,sK3))) = A
| ~ m1_subset_1(A,u1_struct_0(sK2))
| ~ v9_lattices(sK2)
| ~ l3_lattices(sK2) ),
inference(resolve,[status(thm)],[c_261,c_24062]) ).
cnf(c_24064,negated_conjecture,
( k2_lattices(sK2,A,k1_lattices(sK2,A,sK1(sK2,sK3))) = A
| ~ m1_subset_1(A,u1_struct_0(sK2))
| ~ v9_lattices(sK2) ),
inference(resolve,[status(thm)],[c_262,c_24063]) ).
cnf(c_1590,negated_conjecture,
( k2_lattices(sK2,A,k1_lattices(sK2,A,sK1(sK2,sK3))) = A
| ~ m1_subset_1(A,u1_struct_0(sK2)) ),
inference(resolve,[status(thm)],[c_291,c_24064]) ).
cnf(c_24065,plain,
( ~ l3_lattices(sK2)
| k2_lattices(sK2,sK0(sK2,sK3),A) = k4_lattices(sK2,sK0(sK2,sK3),A)
| ~ m1_subset_1(A,u1_struct_0(sK2))
| ~ v6_lattices(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_715,c_350]) ).
cnf(c_24066,negated_conjecture,
( ~ l3_lattices(sK2)
| k2_lattices(sK2,sK0(sK2,sK3),A) = k4_lattices(sK2,sK0(sK2,sK3),A)
| ~ m1_subset_1(A,u1_struct_0(sK2))
| ~ v6_lattices(sK2) ),
inference(resolve,[status(thm)],[c_261,c_24065]) ).
cnf(c_24067,negated_conjecture,
( ~ l3_lattices(sK2)
| k2_lattices(sK2,sK0(sK2,sK3),A) = k4_lattices(sK2,sK0(sK2,sK3),A)
| ~ m1_subset_1(A,u1_struct_0(sK2)) ),
inference(resolve,[status(thm)],[c_297,c_24066]) ).
cnf(c_1652,negated_conjecture,
( k2_lattices(sK2,sK0(sK2,sK3),A) = k4_lattices(sK2,sK0(sK2,sK3),A)
| ~ m1_subset_1(A,u1_struct_0(sK2)) ),
inference(resolve,[status(thm)],[c_262,c_24067]) ).
cnf(c_1670,plain,
( ~ r2_hidden(k4_lattices(sK2,sK0(sK2,sK3),A),sK3)
| r2_hidden(A,sK3)
| ~ m1_subset_1(A,u1_struct_0(sK2)) ),
inference(resolve,[status(thm)],[c_715,c_266]) ).
cnf(c_3159,plain,
( m1_subset_1(k3_lattices(sK2,sK0(sK2,sK3),A),u1_struct_0(sK2))
| ~ m1_subset_1(A,u1_struct_0(sK2)) ),
inference(resolve,[status(thm)],[c_672,c_715]) ).
cnf(c_4554,plain,
( k1_lattices(sK2,sK0(sK2,sK3),A) = k3_lattices(sK2,sK0(sK2,sK3),A)
| ~ m1_subset_1(A,u1_struct_0(sK2)) ),
inference(resolve,[status(thm)],[c_674,c_715]) ).
cnf(c_8184,plain,
m1_subset_1(k3_lattices(sK2,sK0(sK2,sK3),sK1(sK2,sK3)),u1_struct_0(sK2)),
inference(resolve,[status(thm)],[c_3159,c_711]) ).
cnf(c_24068,plain,
( r2_hidden(k4_lattices(sK2,sK0(sK2,sK3),sK1(sK2,sK3)),sK3)
| ~ r2_hidden(sK0(sK2,sK3),sK3) ),
inference(resolve,[status(thm)],[c_1381,c_715]) ).
cnf(c_9037,plain,
r2_hidden(k4_lattices(sK2,sK0(sK2,sK3),sK1(sK2,sK3)),sK3),
inference(resolve,[status(thm)],[c_707,c_24068]) ).
cnf(c_9046,negated_conjecture,
~ r2_hidden(k3_lattices(sK2,sK0(sK2,sK3),sK1(sK2,sK3)),sK3),
inference(resolve,[status(thm)],[c_9037,c_699]) ).
cnf(c_24069,plain,
( ~ r2_hidden(k4_lattices(sK2,sK0(sK2,sK3),k3_lattices(sK2,sK0(sK2,sK3),sK1(sK2,sK3))),sK3)
| r2_hidden(k3_lattices(sK2,sK0(sK2,sK3),sK1(sK2,sK3)),sK3) ),
inference(resolve,[status(thm)],[c_1670,c_8184]) ).
cnf(c_9321,plain,
~ r2_hidden(k4_lattices(sK2,sK0(sK2,sK3),k3_lattices(sK2,sK0(sK2,sK3),sK1(sK2,sK3))),sK3),
inference(resolve,[status(thm)],[c_9046,c_24069]) ).
cnf(c_14598,plain,
k2_lattices(sK2,sK0(sK2,sK3),k3_lattices(sK2,sK0(sK2,sK3),sK1(sK2,sK3))) = k4_lattices(sK2,sK0(sK2,sK3),k3_lattices(sK2,sK0(sK2,sK3),sK1(sK2,sK3))),
inference(resolve,[status(thm)],[c_1652,c_8184]) ).
cnf(c_14987,plain,
k1_lattices(sK2,sK0(sK2,sK3),sK1(sK2,sK3)) = k3_lattices(sK2,sK0(sK2,sK3),sK1(sK2,sK3)),
inference(resolve,[status(thm)],[c_4554,c_711]) ).
cnf(c_24070,plain,
k2_lattices(sK2,sK0(sK2,sK3),k1_lattices(sK2,sK0(sK2,sK3),sK1(sK2,sK3))) = sK0(sK2,sK3),
inference(resolve,[status(thm)],[c_1590,c_715]) ).
cnf(c_24071,plain,
k2_lattices(sK2,sK0(sK2,sK3),k3_lattices(sK2,sK0(sK2,sK3),sK1(sK2,sK3))) = sK0(sK2,sK3),
inference(paramod,[status(thm)],[c_14987,c_24070]) ).
cnf(c_24036,plain,
k4_lattices(sK2,sK0(sK2,sK3),k3_lattices(sK2,sK0(sK2,sK3),sK1(sK2,sK3))) = sK0(sK2,sK3),
inference(paramod,[status(thm)],[c_14598,c_24071]) ).
cnf(c_24072,plain,
~ r2_hidden(sK0(sK2,sK3),sK3),
inference(paramod,[status(thm)],[c_24036,c_9321]) ).
cnf(c_24044,plain,
$false,
inference(resolve,[status(thm)],[c_707,c_24072]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT297+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n001.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Fri Sep 25 20:40:26 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.38 % Process 4191717 was started by sandbox on n001,
% 0.10/0.38 % Fri Sep 25 20:40:26 2026
% 0.10/0.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.40
% 0.10/0.40 % From the command line: assign(max_seconds, 300).
% 113.19/15.78
% 113.19/15.78 % given #500 (T,wt=28): 1731 k2_lattices(c13,f6(c14),f6(c14)) = k4_lattices(c13,f6(c14),f6(c14)). [resolve(1717,a,422,c),unit_del(a,261),unit_del(b,297),unit_del(d,262)].
% 113.19/15.78
% 113.19/15.78 % given #1000 (W,wt=32): 3188 -r2_hidden(f2(c13,c14),f9(c13)) | r2_hidden(k3_lattices(c13,f2(c13,c14),f2(c13,c14)),f9(c13)). [resolve(730,a,711,a)].
% 113.19/15.78
% 113.19/15.78 % given #1500 (F,wt=48): 23529 -r2_hidden(k4_lattices(c13,k3_lattices(c13,f1(c13,c14),f2(c13,c14)),k1_lattices(c13,k4_lattices(c13,f6(c14),f6(c14)),f6(f12(c13)))),c14). [resolve(16858,a,9049,a)].
% 113.19/15.78
% 113.19/15.78 % SZS status Theorem for theBenchmark
% 113.19/15.78
% 113.19/15.78 % Proof 1 at 5.59 (+ 1.59) seconds.
% 113.19/15.78 % Length of proof is 71.
% 113.19/15.78 % Level of proof is 10.
% 113.19/15.78 % Maximum clause weight is 47.000.
% 113.19/15.78 % Given clauses 1974.
% 113.19/15.78
% 113.19/15.78 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------