%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT337+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:17 AM UTC 2026
% Result : Theorem 23.42s 3.43s
% Output : CNFRefutation 23.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 7
% Syntax : Number of formulae : 114 ( 21 unt; 0 def)
% Number of atoms : 575 ( 0 equ)
% Maximal formula atoms : 17 ( 5 avg)
% Number of connectives : 816 ( 355 ~; 361 |; 78 &)
% ( 0 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 21 ( 20 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-3 aty)
% Number of variables : 71 ( 0 sgn 17 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cc5_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( ( v17_lattices(A)
& ~ v3_struct_0(A) )
=> ( v16_lattices(A)
& v15_lattices(A)
& v14_lattices(A)
& v13_lattices(A)
& v11_lattices(A)
& ~ v3_struct_0(A) ) ) ),
file('theBenchmark.p',cc5_lattices) ).
fof(cc6_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( ( v16_lattices(A)
& v15_lattices(A)
& v11_lattices(A)
& ~ v3_struct_0(A) )
=> ( v17_lattices(A)
& ~ v3_struct_0(A) ) ) ),
file('theBenchmark.p',cc6_lattices) ).
fof(cc7_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( ( v11_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v12_lattices(A)
& v10_lattices(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',cc7_lattices) ).
fof(dt_k22_filter_2,axiom,
! [A,B,C] :
( ( m1_subset_1(C,u1_struct_0(A))
& m1_subset_1(B,u1_struct_0(A))
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( m2_lattice4(k22_filter_2(A,B,C),A)
& ~ v1_xboole_0(k22_filter_2(A,B,C)) ) ),
file('theBenchmark.p',dt_k22_filter_2) ).
fof(t78_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m2_lattice4(B,A)
& ~ v1_xboole_0(B) )
=> ( v11_lattices(A)
=> v11_lattices(k23_filter_2(A,B)) ) ) ),
file('theBenchmark.p',t78_filter_2) ).
fof(t86_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( ( r3_lattices(A,B,C)
& v12_lattices(A)
& l3_lattices(A)
& v16_lattices(A)
& v15_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( l3_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
& v16_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
& v15_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
& v10_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
& ~ v3_struct_0(k23_filter_2(A,k22_filter_2(A,B,C))) ) ) ) ) ),
file('theBenchmark.p',t86_filter_2) ).
fof(t87_filter_2,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( ( r3_lattices(A,B,C)
& l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( l3_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
& v17_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
& v10_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
& ~ v3_struct_0(k23_filter_2(A,k22_filter_2(A,B,C))) ) ) ) ) ),
file('theBenchmark.p',t87_filter_2) ).
fof(t87_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] :
( m1_subset_1(C,u1_struct_0(A))
=> ( ( r3_lattices(A,B,C)
& l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( l3_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
& v17_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
& v10_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
& ~ v3_struct_0(k23_filter_2(A,k22_filter_2(A,B,C))) ) ) ) ) ),
inference(assume_negation,[status(cth)],[t87_filter_2]) ).
cnf(c_86,plain,
( ~ v3_struct_0(k23_filter_2(A,k22_filter_2(A,B,C)))
| ~ r3_lattices(A,B,C)
| ~ v12_lattices(A)
| ~ v16_lattices(A)
| ~ v15_lattices(A)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t86_filter_2]) ).
cnf(c_87,plain,
( v10_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
| ~ r3_lattices(A,B,C)
| ~ v12_lattices(A)
| ~ v16_lattices(A)
| ~ v15_lattices(A)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t86_filter_2]) ).
cnf(c_88,plain,
( v15_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
| ~ r3_lattices(A,B,C)
| ~ v12_lattices(A)
| ~ v16_lattices(A)
| ~ v15_lattices(A)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t86_filter_2]) ).
cnf(c_89,plain,
( v16_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
| ~ r3_lattices(A,B,C)
| ~ v12_lattices(A)
| ~ v16_lattices(A)
| ~ v15_lattices(A)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t86_filter_2]) ).
cnf(c_90,plain,
( l3_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
| ~ r3_lattices(A,B,C)
| ~ v12_lattices(A)
| ~ v16_lattices(A)
| ~ v15_lattices(A)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t86_filter_2]) ).
fof(nnf_82,plain,
? [A] :
( ? [B] :
( ? [C] :
( ( ~ l3_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
| ~ v17_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
| ~ v10_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
| v3_struct_0(k23_filter_2(A,k22_filter_2(A,B,C))) )
& r3_lattices(A,B,C)
& l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A)
& m1_subset_1(C,u1_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)],[t87_filter_2_neg]) ).
fof(sk_t87_filter_2_neg,plain,
( ( ~ l3_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v17_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v10_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| v3_struct_0(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2))) )
& r3_lattices(sK0,sK1,sK2)
& l3_lattices(sK0)
& v17_lattices(sK0)
& v10_lattices(sK0)
& ~ v3_struct_0(sK0)
& m1_subset_1(sK2,u1_struct_0(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,sK2]),skolemize(A,sK0),skolemize(B,sK1),skolemize(C,sK2)],[nnf_82]) ).
cnf(c_91,negated_conjecture,
r3_lattices(sK0,sK1,sK2),
inference(split_conjunct,[status(thm)],[sk_t87_filter_2_neg]) ).
cnf(c_187,plain,
( m2_lattice4(k22_filter_2(A,B,C),A)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k22_filter_2]) ).
cnf(c_200,plain,
( v11_lattices(k23_filter_2(A,B))
| ~ v11_lattices(A)
| ~ m2_lattice4(B,A)
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t78_filter_2]) ).
cnf(c_241,negated_conjecture,
( l3_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_91,c_90]) ).
cnf(c_242,negated_conjecture,
( v16_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_91,c_89]) ).
cnf(c_243,negated_conjecture,
( v15_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_91,c_88]) ).
cnf(c_244,negated_conjecture,
( v10_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_91,c_87]) ).
cnf(c_245,negated_conjecture,
( ~ v3_struct_0(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_91,c_86]) ).
cnf(c_333,plain,
( ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| v11_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
| ~ v11_lattices(A)
| v1_xboole_0(k22_filter_2(A,B,C))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_200,c_187]) ).
cnf(c_3167,plain,
( ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v11_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
| ~ v11_lattices(A)
| v1_xboole_0(k22_filter_2(A,B,C))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_333]) ).
cnf(c_3168,plain,
( ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| v11_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
| ~ v11_lattices(A)
| v1_xboole_0(k22_filter_2(A,B,C))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_3167]) ).
cnf(c_334,plain,
( ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| v11_lattices(k23_filter_2(A,k22_filter_2(A,B,C)))
| ~ v11_lattices(A)
| v1_xboole_0(k22_filter_2(A,B,C))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_3168]) ).
cnf(c_383,negated_conjecture,
( ~ l3_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v17_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v10_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| v3_struct_0(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2))) ),
inference(split_conjunct,[status(thm)],[sk_t87_filter_2_neg]) ).
cnf(c_384,negated_conjecture,
v17_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t87_filter_2_neg]) ).
cnf(c_385,negated_conjecture,
m1_subset_1(sK2,u1_struct_0(sK0)),
inference(split_conjunct,[status(thm)],[sk_t87_filter_2_neg]) ).
cnf(c_386,negated_conjecture,
m1_subset_1(sK1,u1_struct_0(sK0)),
inference(split_conjunct,[status(thm)],[sk_t87_filter_2_neg]) ).
cnf(c_387,negated_conjecture,
l3_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t87_filter_2_neg]) ).
cnf(c_388,negated_conjecture,
v10_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t87_filter_2_neg]) ).
cnf(c_389,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t87_filter_2_neg]) ).
cnf(c_483,plain,
( ~ v1_xboole_0(k22_filter_2(A,B,C))
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k22_filter_2]) ).
cnf(c_485,plain,
( v12_lattices(A)
| ~ v11_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc7_lattices]) ).
cnf(c_489,plain,
( v17_lattices(A)
| ~ v16_lattices(A)
| ~ v15_lattices(A)
| ~ v11_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc6_lattices]) ).
cnf(c_490,plain,
( v16_lattices(A)
| ~ v17_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc5_lattices]) ).
cnf(c_491,plain,
( v15_lattices(A)
| ~ v17_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc5_lattices]) ).
cnf(c_493,plain,
( v11_lattices(A)
| ~ v17_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc5_lattices]) ).
cnf(c_3169,negated_conjecture,
( ~ v3_struct_0(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_389,c_245]) ).
cnf(c_3170,negated_conjecture,
( ~ v3_struct_0(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_388,c_3169]) ).
cnf(c_3171,negated_conjecture,
( ~ v3_struct_0(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_387,c_3170]) ).
cnf(c_3172,negated_conjecture,
( ~ v3_struct_0(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_386,c_3171]) ).
cnf(c_579,negated_conjecture,
( ~ v3_struct_0(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0) ),
inference(resolve,[status(thm)],[c_385,c_3172]) ).
cnf(c_3173,negated_conjecture,
( v10_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_389,c_244]) ).
cnf(c_3174,negated_conjecture,
( v10_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_388,c_3173]) ).
cnf(c_3175,negated_conjecture,
( v10_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_387,c_3174]) ).
cnf(c_3176,negated_conjecture,
( v10_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_386,c_3175]) ).
cnf(c_580,negated_conjecture,
( v10_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0) ),
inference(resolve,[status(thm)],[c_385,c_3176]) ).
cnf(c_3177,negated_conjecture,
( v15_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_389,c_243]) ).
cnf(c_3178,negated_conjecture,
( v15_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_388,c_3177]) ).
cnf(c_3179,negated_conjecture,
( v15_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_387,c_3178]) ).
cnf(c_3180,negated_conjecture,
( v15_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_386,c_3179]) ).
cnf(c_581,negated_conjecture,
( v15_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0) ),
inference(resolve,[status(thm)],[c_385,c_3180]) ).
cnf(c_3181,negated_conjecture,
( v16_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_389,c_242]) ).
cnf(c_3182,negated_conjecture,
( v16_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_388,c_3181]) ).
cnf(c_3183,negated_conjecture,
( v16_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_387,c_3182]) ).
cnf(c_3184,negated_conjecture,
( v16_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_386,c_3183]) ).
cnf(c_582,negated_conjecture,
( v16_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0) ),
inference(resolve,[status(thm)],[c_385,c_3184]) ).
cnf(c_3185,negated_conjecture,
( l3_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_389,c_241]) ).
cnf(c_3186,negated_conjecture,
( l3_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_388,c_3185]) ).
cnf(c_3187,negated_conjecture,
( l3_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_387,c_3186]) ).
cnf(c_3188,negated_conjecture,
( l3_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0)
| ~ m1_subset_1(sK2,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_386,c_3187]) ).
cnf(c_583,negated_conjecture,
( l3_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v16_lattices(sK0)
| ~ v15_lattices(sK0) ),
inference(resolve,[status(thm)],[c_385,c_3188]) ).
cnf(c_3189,negated_conjecture,
( ~ v1_xboole_0(k22_filter_2(sK0,sK1,A))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_483,c_386]) ).
cnf(c_3190,negated_conjecture,
( ~ v1_xboole_0(k22_filter_2(sK0,sK1,A))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_389,c_3189]) ).
cnf(c_3191,negated_conjecture,
( ~ v1_xboole_0(k22_filter_2(sK0,sK1,A))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_388,c_3190]) ).
cnf(c_890,negated_conjecture,
( ~ v1_xboole_0(k22_filter_2(sK0,sK1,A))
| ~ m1_subset_1(A,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_387,c_3191]) ).
cnf(c_3192,negated_conjecture,
( v16_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_490,c_384]) ).
cnf(c_3193,negated_conjecture,
( v16_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_387,c_3192]) ).
cnf(c_900,negated_conjecture,
v16_lattices(sK0),
inference(resolve,[status(thm)],[c_389,c_3193]) ).
cnf(c_901,negated_conjecture,
( l3_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v15_lattices(sK0) ),
inference(resolve,[status(thm)],[c_900,c_583]) ).
cnf(c_902,negated_conjecture,
( v16_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v15_lattices(sK0) ),
inference(resolve,[status(thm)],[c_900,c_582]) ).
cnf(c_903,negated_conjecture,
( v15_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v15_lattices(sK0) ),
inference(resolve,[status(thm)],[c_900,c_581]) ).
cnf(c_904,negated_conjecture,
( v10_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v15_lattices(sK0) ),
inference(resolve,[status(thm)],[c_900,c_580]) ).
cnf(c_905,negated_conjecture,
( ~ v3_struct_0(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0)
| ~ v15_lattices(sK0) ),
inference(resolve,[status(thm)],[c_900,c_579]) ).
cnf(c_3194,negated_conjecture,
( v15_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_491,c_384]) ).
cnf(c_3195,negated_conjecture,
( v15_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_387,c_3194]) ).
cnf(c_906,negated_conjecture,
v15_lattices(sK0),
inference(resolve,[status(thm)],[c_389,c_3195]) ).
cnf(c_907,negated_conjecture,
( ~ v3_struct_0(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0) ),
inference(resolve,[status(thm)],[c_906,c_905]) ).
cnf(c_908,negated_conjecture,
( v10_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0) ),
inference(resolve,[status(thm)],[c_906,c_904]) ).
cnf(c_909,negated_conjecture,
( v15_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0) ),
inference(resolve,[status(thm)],[c_906,c_903]) ).
cnf(c_910,negated_conjecture,
( v16_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0) ),
inference(resolve,[status(thm)],[c_906,c_902]) ).
cnf(c_911,negated_conjecture,
( l3_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v12_lattices(sK0) ),
inference(resolve,[status(thm)],[c_906,c_901]) ).
cnf(c_3196,negated_conjecture,
( v11_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_493,c_384]) ).
cnf(c_3197,negated_conjecture,
( v11_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_387,c_3196]) ).
cnf(c_913,negated_conjecture,
v11_lattices(sK0),
inference(resolve,[status(thm)],[c_389,c_3197]) ).
cnf(c_3198,plain,
( v12_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_913,c_485]) ).
cnf(c_3199,negated_conjecture,
( v12_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_387,c_3198]) ).
cnf(c_3200,negated_conjecture,
( v12_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_389,c_3199]) ).
cnf(c_1179,negated_conjecture,
v12_lattices(sK0),
inference(resolve,[status(thm)],[c_388,c_3200]) ).
cnf(c_3201,negated_conjecture,
( ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| v11_lattices(k23_filter_2(sK0,k22_filter_2(sK0,A,B)))
| ~ v11_lattices(sK0)
| v1_xboole_0(k22_filter_2(sK0,A,B))
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_334,c_388]) ).
cnf(c_3202,negated_conjecture,
( ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| v11_lattices(k23_filter_2(sK0,k22_filter_2(sK0,A,B)))
| ~ v11_lattices(sK0)
| v1_xboole_0(k22_filter_2(sK0,A,B))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_3201,c_387]) ).
cnf(c_3203,negated_conjecture,
( ~ m1_subset_1(B,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| v11_lattices(k23_filter_2(sK0,k22_filter_2(sK0,A,B)))
| v1_xboole_0(k22_filter_2(sK0,A,B))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_3202,c_913]) ).
cnf(c_3204,negated_conjecture,
( ~ m1_subset_1(A,u1_struct_0(sK0))
| v11_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,A)))
| v1_xboole_0(k22_filter_2(sK0,sK1,A))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_3203,c_386]) ).
cnf(c_3205,negated_conjecture,
( v11_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| v1_xboole_0(k22_filter_2(sK0,sK1,sK2))
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_3204,c_385]) ).
cnf(c_1186,negated_conjecture,
( v11_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| v1_xboole_0(k22_filter_2(sK0,sK1,sK2)) ),
inference(resolve,[status(thm)],[c_389,c_3205]) ).
cnf(c_1193,negated_conjecture,
l3_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2))),
inference(resolve,[status(thm)],[c_1179,c_911]) ).
cnf(c_1194,negated_conjecture,
v16_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2))),
inference(resolve,[status(thm)],[c_1179,c_910]) ).
cnf(c_1195,negated_conjecture,
v15_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2))),
inference(resolve,[status(thm)],[c_1179,c_909]) ).
cnf(c_1196,negated_conjecture,
v10_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2))),
inference(resolve,[status(thm)],[c_1179,c_908]) ).
cnf(c_1197,negated_conjecture,
~ v3_struct_0(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2))),
inference(resolve,[status(thm)],[c_1179,c_907]) ).
cnf(c_3206,negated_conjecture,
( ~ l3_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v17_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v10_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2))) ),
inference(resolve,[status(thm)],[c_1197,c_383]) ).
cnf(c_3207,negated_conjecture,
( ~ l3_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v17_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2))) ),
inference(resolve,[status(thm)],[c_1196,c_3206]) ).
cnf(c_1198,negated_conjecture,
~ v17_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2))),
inference(resolve,[status(thm)],[c_1193,c_3207]) ).
cnf(c_1257,plain,
~ v1_xboole_0(k22_filter_2(sK0,sK1,sK2)),
inference(resolve,[status(thm)],[c_890,c_385]) ).
cnf(c_1264,negated_conjecture,
v11_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2))),
inference(resolve,[status(thm)],[c_1257,c_1186]) ).
cnf(c_3208,plain,
( v17_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v16_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v15_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| v3_struct_0(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ l3_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2))) ),
inference(resolve,[status(thm)],[c_1264,c_489]) ).
cnf(c_3209,negated_conjecture,
( v17_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v16_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v15_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| v3_struct_0(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2))) ),
inference(resolve,[status(thm)],[c_1193,c_3208]) ).
cnf(c_3210,negated_conjecture,
( v17_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v16_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v15_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2))) ),
inference(resolve,[status(thm)],[c_1197,c_3209]) ).
cnf(c_3211,negated_conjecture,
( v17_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2)))
| ~ v16_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2))) ),
inference(resolve,[status(thm)],[c_1195,c_3210]) ).
cnf(c_3212,negated_conjecture,
v17_lattices(k23_filter_2(sK0,k22_filter_2(sK0,sK1,sK2))),
inference(resolve,[status(thm)],[c_1194,c_3211]) ).
cnf(c_3166,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1198,c_3212]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT337+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.41 % Computer : n006.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.41 % CPULimit : 300
% 0.16/0.41 % WCLimit : 300
% 0.16/0.41 % DateTime : Fri Sep 25 21:01:40 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.42 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.16/0.42 % Process 3728238 was started by sandbox2 on n006,
% 0.16/0.42 % Fri Sep 25 21:01:40 2026
% 0.16/0.42 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.16/0.46
% 0.16/0.46 % From the command line: assign(max_seconds, 300).
% 23.42/3.43
% 23.42/3.43 % given #500 (T,wt=19): 1209 l3_lattices(f4(f7(c17))). [resolve(689,a,527,b),unit_del(a,697),unit_del(b,940)].
% 23.42/3.43
% 23.42/3.43 % SZS status Theorem for theBenchmark
% 23.42/3.43
% 23.42/3.43 % Proof 1 at 2.87 (+ 0.09) seconds.
% 23.42/3.43 % Length of proof is 65.
% 23.42/3.43 % Level of proof is 8.
% 23.42/3.43 % Maximum clause weight is 43.000.
% 23.42/3.43 % Given clauses 841.
% 23.42/3.43
% 23.42/3.43 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------