%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT309+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 : n006.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:09 AM UTC 2026
% Result : Theorem 12.44s 2.22s
% Output : CNFRefutation 12.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 17
% Syntax : Number of formulae : 139 ( 32 unt; 0 def)
% Number of atoms : 517 ( 72 equ)
% Maximal formula atoms : 21 ( 3 avg)
% Number of connectives : 622 ( 244 ~; 267 |; 80 &)
% ( 2 <=>; 29 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 2 con; 0-2 aty)
% Number of variables : 101 ( 0 sgn 46 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d4_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> k5_filter_2(A,B) = B ) ),
file('theBenchmark.p',d4_filter_2) ).
fof(d6_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> k7_filter_2(A,B) = B ) ),
file('theBenchmark.p',d6_filter_2) ).
fof(d7_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k1_lattice2(A))))
=> k8_filter_2(A,B) = B ) ),
file('theBenchmark.p',d7_filter_2) ).
fof(dt_k14_filter_2,axiom,
! [A,B] :
( ( m1_filter_0(B,k1_lattice2(A))
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m2_filter_2(k14_filter_2(A,B),A) ),
file('theBenchmark.p',dt_k14_filter_2) ).
fof(dt_k1_lattice2,axiom,
! [A] :
( l3_lattices(A)
=> ( l3_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) ) ),
file('theBenchmark.p',dt_k1_lattice2) ).
fof(dt_k5_filter_2,axiom,
! [A,B] :
( ( m1_subset_1(B,u1_struct_0(A))
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k5_filter_2(A,B),u1_struct_0(k1_lattice2(A))) ),
file('theBenchmark.p',dt_k5_filter_2) ).
fof(dt_k8_filter_2,axiom,
! [A,B] :
( ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k1_lattice2(A))))
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k8_filter_2(A,B),k1_zfmisc_1(u1_struct_0(A))) ),
file('theBenchmark.p',dt_k8_filter_2) ).
fof(dt_m1_filter_0,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_filter_0(B,A)
=> ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
& ~ v1_xboole_0(B) ) ) ),
file('theBenchmark.p',dt_m1_filter_0) ).
fof(fc1_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_struct_0(A) )
=> ( v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ),
file('theBenchmark.p',fc1_lattice2) ).
fof(fc6_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v10_lattices(k1_lattice2(A))
& v9_lattices(k1_lattice2(A))
& v8_lattices(k1_lattice2(A))
& v7_lattices(k1_lattice2(A))
& v6_lattices(k1_lattice2(A))
& v5_lattices(k1_lattice2(A))
& v4_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ),
file('theBenchmark.p',fc6_lattice2) ).
fof(redefinition_k14_filter_2,axiom,
! [A,B] :
( ( m1_filter_0(B,k1_lattice2(A))
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k14_filter_2(A,B) = k8_filter_2(A,B) ),
file('theBenchmark.p',redefinition_k14_filter_2) ).
fof(redefinition_k15_filter_2,axiom,
! [A,B] :
( ( m2_filter_2(B,A)
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k15_filter_2(A,B) = k7_filter_2(A,B) ),
file('theBenchmark.p',redefinition_k15_filter_2) ).
fof(t24_filter_0,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ~ ( ! [C] :
( m1_filter_0(C,A)
=> ~ ( v1_filter_0(C,A)
& r2_hidden(B,C) ) )
& B != k5_lattices(A)
& l3_lattices(A)
& v13_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ) ) ),
file('theBenchmark.p',t24_filter_0) ).
fof(t33_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( r2_filter_2(A,B)
<=> v1_filter_0(k15_filter_2(A,B),k1_lattice2(A)) ) ) ),
file('theBenchmark.p',t33_filter_2) ).
fof(t64_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v14_lattices(A)
<=> v13_lattices(k1_lattice2(A)) ) ),
file('theBenchmark.p',t64_lattice2) ).
fof(t79_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& v14_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k6_lattices(A) = k5_lattices(k1_lattice2(A)) ),
file('theBenchmark.p',t79_lattice2) ).
fof(t36_filter_2,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ~ ( ! [C] :
( m2_filter_2(C,A)
=> ~ ( r2_filter_2(A,C)
& r2_hidden(B,C) ) )
& B != k6_lattices(A)
& v14_lattices(A) ) ) ),
file('theBenchmark.p',t36_filter_2) ).
fof(t36_filter_2_neg,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ~ ( ! [C] :
( m2_filter_2(C,A)
=> ~ ( r2_filter_2(A,C)
& r2_hidden(B,C) ) )
& B != k6_lattices(A)
& v14_lattices(A) ) ) ),
inference(assume_negation,[status(cth)],[t36_filter_2]) ).
cnf(c_99,plain,
( v13_lattices(k1_lattice2(A))
| ~ v14_lattices(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t64_lattice2]) ).
cnf(c_101,plain,
( k5_lattices(k1_lattice2(A)) = k6_lattices(A)
| ~ l3_lattices(A)
| ~ v14_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t79_lattice2]) ).
fof(nnf_95,plain,
? [A] :
( ? [B] :
( ! [C] :
( ~ r2_filter_2(A,C)
| ~ r2_hidden(B,C)
| ~ m2_filter_2(C,A) )
& k6_lattices(A) != B
& v14_lattices(A)
& m1_subset_1(B,u1_struct_0(A)) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t36_filter_2_neg]) ).
fof(sk_t36_filter_2_neg,plain,
( ! [C] :
( ~ r2_filter_2(sK0,C)
| ~ r2_hidden(sK1,C)
| ~ m2_filter_2(C,sK0) )
& k6_lattices(sK0) != sK1
& v14_lattices(sK0)
& m1_subset_1(sK1,u1_struct_0(sK0))
& l3_lattices(sK0)
& v10_lattices(sK0)
& ~ v3_struct_0(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(A,sK0),skolemize(B,sK1)],[nnf_95]) ).
cnf(c_102,negated_conjecture,
v14_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t36_filter_2_neg]) ).
cnf(c_257,negated_conjecture,
( v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_102,c_99]) ).
cnf(c_258,negated_conjecture,
( k5_lattices(k1_lattice2(sK0)) = k6_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_102,c_101]) ).
cnf(c_261,negated_conjecture,
( ~ r2_filter_2(sK0,A)
| ~ r2_hidden(sK1,A)
| ~ m2_filter_2(A,sK0) ),
inference(split_conjunct,[status(thm)],[sk_t36_filter_2_neg]) ).
cnf(c_262,negated_conjecture,
k6_lattices(sK0) != sK1,
inference(split_conjunct,[status(thm)],[sk_t36_filter_2_neg]) ).
cnf(c_263,negated_conjecture,
m1_subset_1(sK1,u1_struct_0(sK0)),
inference(split_conjunct,[status(thm)],[sk_t36_filter_2_neg]) ).
cnf(c_264,negated_conjecture,
l3_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t36_filter_2_neg]) ).
cnf(c_265,negated_conjecture,
v10_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t36_filter_2_neg]) ).
cnf(c_266,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t36_filter_2_neg]) ).
cnf(c_272,plain,
( ~ v1_filter_0(k15_filter_2(A,B),k1_lattice2(A))
| r2_filter_2(A,B)
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t33_filter_2]) ).
fof(nnf_84,plain,
! [A] :
( ! [B] :
( ? [C] :
( v1_filter_0(C,A)
& r2_hidden(B,C)
& m1_filter_0(C,A) )
| k5_lattices(A) = B
| ~ l3_lattices(A)
| ~ v13_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ m1_subset_1(B,u1_struct_0(A)) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t24_filter_0]) ).
fof(sk_t24_filter_0_sk,plain,
! [A] :
( ! [B] :
( ( v1_filter_0(sK2(A,B),A)
& r2_hidden(B,sK2(A,B))
& m1_filter_0(sK2(A,B),A) )
| k5_lattices(A) = B
| ~ l3_lattices(A)
| ~ v13_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ m1_subset_1(B,u1_struct_0(A)) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(C,sK2(A,B))],[nnf_84]) ).
fof(sk_t24_filter_0,plain,
( ! [VAR_0,VAR_1] :
( v1_filter_0(sK2(VAR_0,VAR_1),VAR_0)
| k5_lattices(VAR_0) = VAR_1
| ~ v13_lattices(VAR_0)
| ~ m1_subset_1(VAR_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(VAR_1,sK2(VAR_0,VAR_1))
| k5_lattices(VAR_0) = VAR_1
| ~ v13_lattices(VAR_0)
| ~ m1_subset_1(VAR_1,u1_struct_0(VAR_0))
| ~ l3_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1] :
( m1_filter_0(sK2(VAR_0,VAR_1),VAR_0)
| k5_lattices(VAR_0) = VAR_1
| ~ v13_lattices(VAR_0)
| ~ m1_subset_1(VAR_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_t24_filter_0_sk]) ).
cnf(c_275,plain,
( v1_filter_0(sK2(A,B),A)
| k5_lattices(A) = B
| ~ v13_lattices(A)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(split_conjunct,[status(thm)],[sk_t24_filter_0]) ).
cnf(c_276,plain,
( r2_hidden(B,sK2(A,B))
| k5_lattices(A) = B
| ~ v13_lattices(A)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(split_conjunct,[status(thm)],[sk_t24_filter_0]) ).
cnf(c_277,plain,
( m1_filter_0(sK2(A,B),A)
| k5_lattices(A) = B
| ~ v13_lattices(A)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(split_conjunct,[status(thm)],[sk_t24_filter_0]) ).
cnf(c_279,plain,
( k15_filter_2(A,B) = k7_filter_2(A,B)
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[redefinition_k15_filter_2]) ).
cnf(c_280,plain,
( k7_filter_2(A,B) = k15_filter_2(A,B)
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_279]) ).
cnf(c_281,plain,
( k14_filter_2(A,B) = k8_filter_2(A,B)
| ~ m1_filter_0(B,k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[redefinition_k14_filter_2]) ).
cnf(c_307,plain,
( v10_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc6_lattice2]) ).
cnf(c_314,plain,
( ~ v3_struct_0(k1_lattice2(A))
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_lattice2]) ).
cnf(c_328,plain,
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_filter_0(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_m1_filter_0]) ).
cnf(c_332,plain,
( m1_subset_1(k8_filter_2(A,B),k1_zfmisc_1(u1_struct_0(A)))
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k1_lattice2(A))))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k8_filter_2]) ).
cnf(c_336,plain,
( m1_subset_1(k5_filter_2(A,B),u1_struct_0(k1_lattice2(A)))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k5_filter_2]) ).
cnf(c_337,plain,
( l3_lattices(k1_lattice2(A))
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_k1_lattice2]) ).
cnf(c_338,plain,
( m2_filter_2(k14_filter_2(A,B),A)
| ~ m1_filter_0(B,k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k14_filter_2]) ).
cnf(c_340,plain,
( k8_filter_2(A,B) = B
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k1_lattice2(A))))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d7_filter_2]) ).
cnf(c_341,plain,
( k7_filter_2(A,B) = B
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d6_filter_2]) ).
cnf(c_342,plain,
( k5_filter_2(A,B) = B
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d4_filter_2]) ).
cnf(c_10440,negated_conjecture,
( k5_lattices(k1_lattice2(sK0)) = k6_lattices(sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_266,c_258]) ).
cnf(c_10441,negated_conjecture,
( k5_lattices(k1_lattice2(sK0)) = k6_lattices(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_265,c_10440]) ).
cnf(c_378,negated_conjecture,
k5_lattices(k1_lattice2(sK0)) = k6_lattices(sK0),
inference(resolve,[status(thm)],[c_264,c_10441]) ).
cnf(c_10442,negated_conjecture,
( v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_266,c_257]) ).
cnf(c_10443,negated_conjecture,
( v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_265,c_10442]) ).
cnf(c_379,negated_conjecture,
v13_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_264,c_10443]) ).
cnf(c_10444,negated_conjecture,
( ~ v1_filter_0(k15_filter_2(sK0,A),k1_lattice2(sK0))
| r2_filter_2(sK0,A)
| ~ m2_filter_2(A,sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_272,c_265]) ).
cnf(c_10445,negated_conjecture,
( ~ v1_filter_0(k15_filter_2(sK0,A),k1_lattice2(sK0))
| r2_filter_2(sK0,A)
| ~ m2_filter_2(A,sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_266,c_10444]) ).
cnf(c_396,negated_conjecture,
( ~ v1_filter_0(k15_filter_2(sK0,A),k1_lattice2(sK0))
| r2_filter_2(sK0,A)
| ~ m2_filter_2(A,sK0) ),
inference(resolve,[status(thm)],[c_264,c_10445]) ).
cnf(c_10446,negated_conjecture,
( k7_filter_2(sK0,A) = k15_filter_2(sK0,A)
| ~ m2_filter_2(A,sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_280,c_265]) ).
cnf(c_10447,negated_conjecture,
( k7_filter_2(sK0,A) = k15_filter_2(sK0,A)
| ~ m2_filter_2(A,sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_266,c_10446]) ).
cnf(c_408,negated_conjecture,
( k7_filter_2(sK0,A) = k15_filter_2(sK0,A)
| ~ m2_filter_2(A,sK0) ),
inference(resolve,[status(thm)],[c_264,c_10447]) ).
cnf(c_10448,negated_conjecture,
( k14_filter_2(sK0,A) = k8_filter_2(sK0,A)
| ~ m1_filter_0(A,k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_281,c_265]) ).
cnf(c_10449,negated_conjecture,
( k14_filter_2(sK0,A) = k8_filter_2(sK0,A)
| ~ m1_filter_0(A,k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_266,c_10448]) ).
cnf(c_409,negated_conjecture,
( k14_filter_2(sK0,A) = k8_filter_2(sK0,A)
| ~ m1_filter_0(A,k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_264,c_10449]) ).
cnf(c_10450,negated_conjecture,
( v10_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_307,c_265]) ).
cnf(c_10451,negated_conjecture,
( v10_lattices(k1_lattice2(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_266,c_10450]) ).
cnf(c_487,negated_conjecture,
v10_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_264,c_10451]) ).
cnf(c_10452,negated_conjecture,
( ~ v3_struct_0(k1_lattice2(sK0))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_314,c_264]) ).
cnf(c_510,negated_conjecture,
~ v3_struct_0(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_266,c_10452]) ).
cnf(c_10453,negated_conjecture,
( m1_subset_1(k8_filter_2(sK0,A),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_332,c_265]) ).
cnf(c_10454,negated_conjecture,
( m1_subset_1(k8_filter_2(sK0,A),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_266,c_10453]) ).
cnf(c_613,negated_conjecture,
( m1_subset_1(k8_filter_2(sK0,A),k1_zfmisc_1(u1_struct_0(sK0)))
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0)))) ),
inference(resolve,[status(thm)],[c_264,c_10454]) ).
cnf(c_10455,negated_conjecture,
( m1_subset_1(k5_filter_2(sK0,sK1),u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_336,c_263]) ).
cnf(c_10456,negated_conjecture,
( m1_subset_1(k5_filter_2(sK0,sK1),u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_266,c_10455]) ).
cnf(c_10457,negated_conjecture,
( m1_subset_1(k5_filter_2(sK0,sK1),u1_struct_0(k1_lattice2(sK0)))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_265,c_10456]) ).
cnf(c_639,negated_conjecture,
m1_subset_1(k5_filter_2(sK0,sK1),u1_struct_0(k1_lattice2(sK0))),
inference(resolve,[status(thm)],[c_264,c_10457]) ).
cnf(c_645,plain,
l3_lattices(k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_337,c_264]) ).
cnf(c_10458,negated_conjecture,
( k8_filter_2(sK0,A) = A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_340,c_265]) ).
cnf(c_10459,negated_conjecture,
( k8_filter_2(sK0,A) = A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_266,c_10458]) ).
cnf(c_666,negated_conjecture,
( k8_filter_2(sK0,A) = A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0)))) ),
inference(resolve,[status(thm)],[c_264,c_10459]) ).
cnf(c_10460,negated_conjecture,
( k7_filter_2(sK0,A) = A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_341,c_265]) ).
cnf(c_10461,negated_conjecture,
( k7_filter_2(sK0,A) = A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0)))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_266,c_10460]) ).
cnf(c_675,negated_conjecture,
( k7_filter_2(sK0,A) = A
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK0))) ),
inference(resolve,[status(thm)],[c_264,c_10461]) ).
cnf(c_10462,negated_conjecture,
( k5_filter_2(sK0,sK1) = sK1
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_342,c_263]) ).
cnf(c_10463,negated_conjecture,
( k5_filter_2(sK0,sK1) = sK1
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_266,c_10462]) ).
cnf(c_10464,negated_conjecture,
( k5_filter_2(sK0,sK1) = sK1
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_265,c_10463]) ).
cnf(c_690,negated_conjecture,
k5_filter_2(sK0,sK1) = sK1,
inference(resolve,[status(thm)],[c_264,c_10464]) ).
cnf(c_691,negated_conjecture,
m1_subset_1(sK1,u1_struct_0(k1_lattice2(sK0))),
inference(paramod,[status(thm)],[c_690,c_639]) ).
cnf(c_10465,plain,
( m1_filter_0(sK2(k1_lattice2(sK0),sK1),k1_lattice2(sK0))
| k5_lattices(k1_lattice2(sK0)) = sK1
| ~ v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_691,c_277]) ).
cnf(c_10466,plain,
( m1_filter_0(sK2(k1_lattice2(sK0),sK1),k1_lattice2(sK0))
| k6_lattices(sK0) = sK1
| ~ v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(paramod,[status(thm)],[c_378,c_10465]) ).
cnf(c_10467,plain,
( m1_filter_0(sK2(k1_lattice2(sK0),sK1),k1_lattice2(sK0))
| k6_lattices(sK0) = sK1
| ~ v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_510,c_10466]) ).
cnf(c_10468,plain,
( m1_filter_0(sK2(k1_lattice2(sK0),sK1),k1_lattice2(sK0))
| k6_lattices(sK0) = sK1
| ~ v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_487,c_10467]) ).
cnf(c_10469,plain,
( m1_filter_0(sK2(k1_lattice2(sK0),sK1),k1_lattice2(sK0))
| k6_lattices(sK0) = sK1
| ~ v13_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_645,c_10468]) ).
cnf(c_10470,negated_conjecture,
( m1_filter_0(sK2(k1_lattice2(sK0),sK1),k1_lattice2(sK0))
| k6_lattices(sK0) = sK1 ),
inference(resolve,[status(thm)],[c_379,c_10469]) ).
cnf(c_1899,negated_conjecture,
m1_filter_0(sK2(k1_lattice2(sK0),sK1),k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_262,c_10470]) ).
cnf(c_10471,plain,
( r2_hidden(sK1,sK2(k1_lattice2(sK0),sK1))
| k5_lattices(k1_lattice2(sK0)) = sK1
| ~ v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_691,c_276]) ).
cnf(c_10472,plain,
( r2_hidden(sK1,sK2(k1_lattice2(sK0),sK1))
| k6_lattices(sK0) = sK1
| ~ v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(paramod,[status(thm)],[c_378,c_10471]) ).
cnf(c_10473,plain,
( r2_hidden(sK1,sK2(k1_lattice2(sK0),sK1))
| k6_lattices(sK0) = sK1
| ~ v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_510,c_10472]) ).
cnf(c_10474,plain,
( r2_hidden(sK1,sK2(k1_lattice2(sK0),sK1))
| k6_lattices(sK0) = sK1
| ~ v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_487,c_10473]) ).
cnf(c_10475,plain,
( r2_hidden(sK1,sK2(k1_lattice2(sK0),sK1))
| k6_lattices(sK0) = sK1
| ~ v13_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_645,c_10474]) ).
cnf(c_10476,negated_conjecture,
( r2_hidden(sK1,sK2(k1_lattice2(sK0),sK1))
| k6_lattices(sK0) = sK1 ),
inference(resolve,[status(thm)],[c_379,c_10475]) ).
cnf(c_1900,negated_conjecture,
r2_hidden(sK1,sK2(k1_lattice2(sK0),sK1)),
inference(resolve,[status(thm)],[c_262,c_10476]) ).
cnf(c_10477,plain,
( v1_filter_0(sK2(k1_lattice2(sK0),sK1),k1_lattice2(sK0))
| k5_lattices(k1_lattice2(sK0)) = sK1
| ~ v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_691,c_275]) ).
cnf(c_10478,plain,
( v1_filter_0(sK2(k1_lattice2(sK0),sK1),k1_lattice2(sK0))
| k6_lattices(sK0) = sK1
| ~ v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(paramod,[status(thm)],[c_378,c_10477]) ).
cnf(c_10479,plain,
( v1_filter_0(sK2(k1_lattice2(sK0),sK1),k1_lattice2(sK0))
| k6_lattices(sK0) = sK1
| ~ v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_510,c_10478]) ).
cnf(c_10480,plain,
( v1_filter_0(sK2(k1_lattice2(sK0),sK1),k1_lattice2(sK0))
| k6_lattices(sK0) = sK1
| ~ v13_lattices(k1_lattice2(sK0))
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_487,c_10479]) ).
cnf(c_10481,plain,
( v1_filter_0(sK2(k1_lattice2(sK0),sK1),k1_lattice2(sK0))
| k6_lattices(sK0) = sK1
| ~ v13_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_645,c_10480]) ).
cnf(c_10482,negated_conjecture,
( v1_filter_0(sK2(k1_lattice2(sK0),sK1),k1_lattice2(sK0))
| k6_lattices(sK0) = sK1 ),
inference(resolve,[status(thm)],[c_379,c_10481]) ).
cnf(c_1901,negated_conjecture,
v1_filter_0(sK2(k1_lattice2(sK0),sK1),k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_262,c_10482]) ).
cnf(c_3264,plain,
k14_filter_2(sK0,sK2(k1_lattice2(sK0),sK1)) = k8_filter_2(sK0,sK2(k1_lattice2(sK0),sK1)),
inference(resolve,[status(thm)],[c_1899,c_409]) ).
cnf(c_10483,plain,
( m2_filter_2(k14_filter_2(sK0,sK2(k1_lattice2(sK0),sK1)),sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_1899,c_338]) ).
cnf(c_10484,plain,
( m2_filter_2(k8_filter_2(sK0,sK2(k1_lattice2(sK0),sK1)),sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(paramod,[status(thm)],[c_3264,c_10483]) ).
cnf(c_10485,negated_conjecture,
( m2_filter_2(k8_filter_2(sK0,sK2(k1_lattice2(sK0),sK1)),sK0)
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_266,c_10484]) ).
cnf(c_10486,negated_conjecture,
( m2_filter_2(k8_filter_2(sK0,sK2(k1_lattice2(sK0),sK1)),sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_265,c_10485]) ).
cnf(c_3265,negated_conjecture,
m2_filter_2(k8_filter_2(sK0,sK2(k1_lattice2(sK0),sK1)),sK0),
inference(resolve,[status(thm)],[c_264,c_10486]) ).
cnf(c_10487,plain,
( m1_subset_1(sK2(k1_lattice2(sK0),sK1),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| v3_struct_0(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_1899,c_328]) ).
cnf(c_10488,plain,
( m1_subset_1(sK2(k1_lattice2(sK0),sK1),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| ~ l3_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_510,c_10487]) ).
cnf(c_10489,plain,
( m1_subset_1(sK2(k1_lattice2(sK0),sK1),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0))))
| ~ l3_lattices(k1_lattice2(sK0)) ),
inference(resolve,[status(thm)],[c_487,c_10488]) ).
cnf(c_3266,plain,
m1_subset_1(sK2(k1_lattice2(sK0),sK1),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0)))),
inference(resolve,[status(thm)],[c_645,c_10489]) ).
cnf(c_9108,plain,
k7_filter_2(sK0,k8_filter_2(sK0,sK2(k1_lattice2(sK0),sK1))) = k15_filter_2(sK0,k8_filter_2(sK0,sK2(k1_lattice2(sK0),sK1))),
inference(resolve,[status(thm)],[c_3265,c_408]) ).
cnf(c_9110,plain,
( ~ v1_filter_0(k15_filter_2(sK0,k8_filter_2(sK0,sK2(k1_lattice2(sK0),sK1))),k1_lattice2(sK0))
| r2_filter_2(sK0,k8_filter_2(sK0,sK2(k1_lattice2(sK0),sK1))) ),
inference(resolve,[status(thm)],[c_3265,c_396]) ).
cnf(c_9111,plain,
( ~ r2_filter_2(sK0,k8_filter_2(sK0,sK2(k1_lattice2(sK0),sK1)))
| ~ r2_hidden(sK1,k8_filter_2(sK0,sK2(k1_lattice2(sK0),sK1))) ),
inference(resolve,[status(thm)],[c_3265,c_261]) ).
cnf(c_10415,plain,
k8_filter_2(sK0,sK2(k1_lattice2(sK0),sK1)) = sK2(k1_lattice2(sK0),sK1),
inference(resolve,[status(thm)],[c_3266,c_666]) ).
cnf(c_10490,plain,
m1_subset_1(k8_filter_2(sK0,sK2(k1_lattice2(sK0),sK1)),k1_zfmisc_1(u1_struct_0(sK0))),
inference(resolve,[status(thm)],[c_3266,c_613]) ).
cnf(c_10416,plain,
m1_subset_1(sK2(k1_lattice2(sK0),sK1),k1_zfmisc_1(u1_struct_0(sK0))),
inference(paramod,[status(thm)],[c_10415,c_10490]) ).
cnf(c_10491,plain,
( ~ r2_filter_2(sK0,k8_filter_2(sK0,sK2(k1_lattice2(sK0),sK1)))
| ~ r2_hidden(sK1,sK2(k1_lattice2(sK0),sK1)) ),
inference(paramod,[status(thm)],[c_10415,c_9111]) ).
cnf(c_10492,plain,
( ~ r2_filter_2(sK0,sK2(k1_lattice2(sK0),sK1))
| ~ r2_hidden(sK1,sK2(k1_lattice2(sK0),sK1)) ),
inference(paramod,[status(thm)],[c_10415,c_10491]) ).
cnf(c_10421,plain,
~ r2_filter_2(sK0,sK2(k1_lattice2(sK0),sK1)),
inference(resolve,[status(thm)],[c_1900,c_10492]) ).
cnf(c_10493,plain,
( ~ v1_filter_0(k15_filter_2(sK0,k8_filter_2(sK0,sK2(k1_lattice2(sK0),sK1))),k1_lattice2(sK0))
| r2_filter_2(sK0,sK2(k1_lattice2(sK0),sK1)) ),
inference(paramod,[status(thm)],[c_10415,c_9110]) ).
cnf(c_10494,plain,
( ~ v1_filter_0(k15_filter_2(sK0,sK2(k1_lattice2(sK0),sK1)),k1_lattice2(sK0))
| r2_filter_2(sK0,sK2(k1_lattice2(sK0),sK1)) ),
inference(paramod,[status(thm)],[c_10415,c_10493]) ).
cnf(c_10422,plain,
~ v1_filter_0(k15_filter_2(sK0,sK2(k1_lattice2(sK0),sK1)),k1_lattice2(sK0)),
inference(resolve,[status(thm)],[c_10421,c_10494]) ).
cnf(c_10495,plain,
k7_filter_2(sK0,sK2(k1_lattice2(sK0),sK1)) = k15_filter_2(sK0,k8_filter_2(sK0,sK2(k1_lattice2(sK0),sK1))),
inference(paramod,[status(thm)],[c_10415,c_9108]) ).
cnf(c_10423,plain,
k7_filter_2(sK0,sK2(k1_lattice2(sK0),sK1)) = k15_filter_2(sK0,sK2(k1_lattice2(sK0),sK1)),
inference(paramod,[status(thm)],[c_10415,c_10495]) ).
cnf(c_10496,plain,
k7_filter_2(sK0,sK2(k1_lattice2(sK0),sK1)) = sK2(k1_lattice2(sK0),sK1),
inference(resolve,[status(thm)],[c_10416,c_675]) ).
cnf(c_10435,plain,
k15_filter_2(sK0,sK2(k1_lattice2(sK0),sK1)) = sK2(k1_lattice2(sK0),sK1),
inference(paramod,[status(thm)],[c_10423,c_10496]) ).
cnf(c_10497,plain,
~ v1_filter_0(sK2(k1_lattice2(sK0),sK1),k1_lattice2(sK0)),
inference(paramod,[status(thm)],[c_10435,c_10422]) ).
cnf(c_10439,plain,
$false,
inference(resolve,[status(thm)],[c_1901,c_10497]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT309+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.10/0.37 % Computer : n006.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:42:26 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 3676808 was started by sandbox2 on n006,
% 0.10/0.37 % Fri Sep 25 20:42:26 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.39
% 0.10/0.39 % From the command line: assign(max_seconds, 300).
% 12.44/2.22
% 12.44/2.22 % given #500 (T,wt=18): 1976 -r2_hidden(A,f11(c5)) | m1_subset_1(A,u1_struct_0(c5)). [resolve(807,a,271,b)].
% 12.44/2.22
% 12.44/2.22 % given #1000 (A,wt=26): 513 v1_xboole_0(A) | -m1_subset_1(A,k1_zfmisc_1(u1_struct_0(c15))) | -v1_xboole_0(k7_filter_2(c15,A)). [resolve(315,b,265,a),unit_del(a,266),unit_del(b,264)].
% 12.44/2.22
% 12.44/2.22 % given #1500 (W,wt=24): 6556 -r2_hidden(A,f8(c14)) | m1_subset_1(A,u1_struct_0(k1_lattice2(c14))). [resolve(1946,a,271,b)].
% 12.44/2.22
% 12.44/2.22 % given #2000 (F,wt=28): 8815 -v10_lattices(c13) | -v1_xboole_0(k8_filter_2(c13,f11(k1_lattice2(c13)))). [resolve(1450,a,503,c),unit_del(b,1451)].
% 12.44/2.22
% 12.44/2.22 % SZS status Theorem for theBenchmark
% 12.44/2.22
% 12.44/2.22 % Proof 1 at 1.41 (+ 0.35) seconds.
% 12.44/2.22 % Length of proof is 75.
% 12.44/2.22 % Level of proof is 10.
% 12.44/2.22 % Maximum clause weight is 44.000.
% 12.44/2.22 % Given clauses 2465.
% 12.44/2.22
% 12.44/2.22 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------