%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT308+3 : 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 : n014.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:08 AM UTC 2026
% Result : Theorem 192.56s 33.58s
% Output : CNFRefutation 192.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 13
% Syntax : Number of formulae : 124 ( 25 unt; 0 def)
% Number of atoms : 499 ( 29 equ)
% Maximal formula atoms : 9 ( 4 avg)
% Number of connectives : 654 ( 279 ~; 283 |; 54 &)
% ( 6 <=>; 32 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-3 aty)
% Number of variables : 92 ( 0 sgn 34 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d2_subset_1,axiom,
! [A,B] :
( ( v1_xboole_0(A)
=> ( m1_subset_1(B,A)
<=> v1_xboole_0(B) ) )
& ( ~ v1_xboole_0(A)
=> ( m1_subset_1(B,A)
<=> r2_hidden(B,A) ) ) ),
file('theBenchmark.p',d2_subset_1) ).
fof(t3_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_subset_1(C,u1_struct_0(A))
=> ! [D] :
( m1_subset_1(D,u1_struct_0(A))
=> ( r3_lattices(A,B,C)
=> ( r3_lattices(A,B,k3_lattices(A,C,D))
& r3_lattices(A,B,k3_lattices(A,D,C)) ) ) ) ) ) ),
file('theBenchmark.p',t3_filter_0) ).
fof(t15_filter_0,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m1_filter_0(u1_struct_0(A),A) ),
file('theBenchmark.p',t15_filter_0) ).
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(t29_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))
=> ( r2_hidden(B,k18_filter_2(A,C))
<=> r3_lattices(A,B,C) ) ) ) ),
file('theBenchmark.p',t29_filter_2) ).
fof(d3_lattices,axiom,
! [A] :
( ( l2_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( r1_lattices(A,B,C)
<=> k1_lattices(A,B,C) = C ) ) ) ),
file('theBenchmark.p',d3_lattices) ).
fof(d10_lattices,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_struct_0(A) )
=> ( v10_lattices(A)
<=> ( v9_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v8_lattices(A)
& v5_lattices(A)
& v4_lattices(A) ) ) ),
file('theBenchmark.p',d10_lattices) ).
fof(t17_lattices,axiom,
! [A] :
( ( l3_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v6_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> k1_lattices(A,B,B) = B ) ),
file('theBenchmark.p',t17_lattices) ).
fof(t26_lattices,axiom,
! [A] :
( ( l2_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( ( r1_lattices(A,C,B)
& r1_lattices(A,B,C) )
=> B = C ) ) ) ),
file('theBenchmark.p',t26_lattices) ).
fof(dt_l3_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( l2_lattices(A)
& l1_lattices(A) ) ),
file('theBenchmark.p',dt_l3_lattices) ).
fof(redefinition_r3_lattices,axiom,
! [A,B,C] :
( ( m1_subset_1(C,u1_struct_0(A))
& m1_subset_1(B,u1_struct_0(A))
& l3_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v6_lattices(A)
& ~ v3_struct_0(A) )
=> ( r3_lattices(A,B,C)
<=> r1_lattices(A,B,C) ) ),
file('theBenchmark.p',redefinition_r3_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(t35_filter_2,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ~ ( k18_filter_2(A,B) = u1_struct_0(A)
& ~ ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> k3_lattices(A,B,C) = B ) ) ) ),
file('theBenchmark.p',t35_filter_2) ).
fof(t35_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))
=> ~ ( k18_filter_2(A,B) = u1_struct_0(A)
& ~ ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> k3_lattices(A,B,C) = B ) ) ) ),
inference(assume_negation,[status(cth)],[t35_filter_2]) ).
cnf(c_991,plain,
( k1_lattices(A,B,C) != C
| r1_lattices(A,B,C)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l2_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d3_lattices]) ).
cnf(c_1018,plain,
( v4_lattices(A)
| ~ v10_lattices(A)
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d10_lattices]) ).
cnf(c_1020,plain,
( v8_lattices(A)
| ~ v10_lattices(A)
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d10_lattices]) ).
cnf(c_1021,plain,
( v6_lattices(A)
| ~ v10_lattices(A)
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d10_lattices]) ).
cnf(c_1023,plain,
( v9_lattices(A)
| ~ v10_lattices(A)
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d10_lattices]) ).
cnf(c_1054,plain,
( k1_lattices(A,B,B) = B
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v9_lattices(A)
| ~ v8_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t17_lattices]) ).
cnf(c_1061,plain,
( C = B
| ~ r1_lattices(A,C,B)
| ~ r1_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)],[t26_lattices]) ).
cnf(c_1088,plain,
( l2_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_1091,plain,
( r1_lattices(A,B,C)
| ~ r3_lattices(A,B,C)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v9_lattices(A)
| ~ v8_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[redefinition_r3_lattices]) ).
cnf(c_1092,plain,
( ~ r1_lattices(A,B,C)
| r3_lattices(A,B,C)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v9_lattices(A)
| ~ v8_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[redefinition_r3_lattices]) ).
cnf(c_1095,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_1648,plain,
( r2_hidden(B,A)
| ~ m1_subset_1(B,A)
| v1_xboole_0(A) ),
inference(clausify,[status(thm)],[d2_subset_1]) ).
cnf(c_1705,plain,
( r3_lattices(A,B,k3_lattices(A,C,D))
| ~ r3_lattices(A,B,C)
| ~ m1_subset_1(D,u1_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(clausify,[status(thm)],[t3_filter_0]) ).
cnf(c_1750,plain,
( m1_filter_0(u1_struct_0(A),A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t15_filter_0]) ).
cnf(c_1755,plain,
( ~ v1_xboole_0(B)
| ~ 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_1895,plain,
( r3_lattices(A,B,C)
| ~ r2_hidden(B,k18_filter_2(A,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)],[t29_filter_2]) ).
fof(nnf_519,plain,
? [A] :
( ? [B] :
( k18_filter_2(A,B) = u1_struct_0(A)
& ? [C] :
( k3_lattices(A,B,C) != B
& 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)],[t35_filter_2_neg]) ).
fof(sk_t35_filter_2_neg,plain,
( k18_filter_2(sK0,sK1) = u1_struct_0(sK0)
& k3_lattices(sK0,sK1,sK2) != sK1
& 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_519]) ).
cnf(c_1900,negated_conjecture,
~ v3_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t35_filter_2_neg]) ).
cnf(c_1901,negated_conjecture,
v10_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t35_filter_2_neg]) ).
cnf(c_1902,negated_conjecture,
l3_lattices(sK0),
inference(split_conjunct,[status(thm)],[sk_t35_filter_2_neg]) ).
cnf(c_1903,negated_conjecture,
m1_subset_1(sK1,u1_struct_0(sK0)),
inference(split_conjunct,[status(thm)],[sk_t35_filter_2_neg]) ).
cnf(c_1904,negated_conjecture,
m1_subset_1(sK2,u1_struct_0(sK0)),
inference(split_conjunct,[status(thm)],[sk_t35_filter_2_neg]) ).
cnf(c_1905,negated_conjecture,
k3_lattices(sK0,sK1,sK2) != sK1,
inference(split_conjunct,[status(thm)],[sk_t35_filter_2_neg]) ).
cnf(c_1906,negated_conjecture,
k18_filter_2(sK0,sK1) = u1_struct_0(sK0),
inference(split_conjunct,[status(thm)],[sk_t35_filter_2_neg]) ).
cnf(c_56618,negated_conjecture,
( v9_lattices(sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_1901,c_1023]) ).
cnf(c_56619,negated_conjecture,
( v9_lattices(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1900,c_56618]) ).
cnf(c_3090,negated_conjecture,
v9_lattices(sK0),
inference(resolve,[status(thm)],[c_1902,c_56619]) ).
cnf(c_56620,negated_conjecture,
( v6_lattices(sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_1901,c_1021]) ).
cnf(c_56621,negated_conjecture,
( v6_lattices(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1900,c_56620]) ).
cnf(c_3092,negated_conjecture,
v6_lattices(sK0),
inference(resolve,[status(thm)],[c_1902,c_56621]) ).
cnf(c_56622,negated_conjecture,
( v8_lattices(sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_1901,c_1020]) ).
cnf(c_56623,negated_conjecture,
( v8_lattices(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1900,c_56622]) ).
cnf(c_3093,negated_conjecture,
v8_lattices(sK0),
inference(resolve,[status(thm)],[c_1902,c_56623]) ).
cnf(c_56624,negated_conjecture,
( v4_lattices(sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_1901,c_1018]) ).
cnf(c_56625,negated_conjecture,
( v4_lattices(sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1900,c_56624]) ).
cnf(c_3095,negated_conjecture,
v4_lattices(sK0),
inference(resolve,[status(thm)],[c_1902,c_56625]) ).
cnf(c_3261,plain,
l2_lattices(sK0),
inference(resolve,[status(thm)],[c_1902,c_1088]) ).
cnf(c_56626,negated_conjecture,
( m1_subset_1(k3_lattices(sK0,sK1,A),u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l2_lattices(sK0)
| ~ v4_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_1903,c_1095]) ).
cnf(c_56627,negated_conjecture,
( m1_subset_1(k3_lattices(sK0,sK1,A),u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l2_lattices(sK0)
| ~ v4_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1900,c_56626]) ).
cnf(c_56628,negated_conjecture,
( m1_subset_1(k3_lattices(sK0,sK1,A),u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l2_lattices(sK0) ),
inference(resolve,[status(thm)],[c_3095,c_56627]) ).
cnf(c_7804,negated_conjecture,
( m1_subset_1(k3_lattices(sK0,sK1,A),u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_3261,c_56628]) ).
cnf(c_56629,negated_conjecture,
( r1_lattices(sK0,A,sK1)
| ~ r3_lattices(sK0,A,sK1)
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0)
| ~ v8_lattices(sK0)
| ~ v6_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_1903,c_1091]) ).
cnf(c_56630,negated_conjecture,
( r1_lattices(sK0,A,sK1)
| ~ r3_lattices(sK0,A,sK1)
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0)
| ~ v8_lattices(sK0)
| ~ v6_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1900,c_56629]) ).
cnf(c_56631,negated_conjecture,
( r1_lattices(sK0,A,sK1)
| ~ r3_lattices(sK0,A,sK1)
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0)
| ~ v8_lattices(sK0) ),
inference(resolve,[status(thm)],[c_3092,c_56630]) ).
cnf(c_56632,negated_conjecture,
( r1_lattices(sK0,A,sK1)
| ~ r3_lattices(sK0,A,sK1)
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0) ),
inference(resolve,[status(thm)],[c_3093,c_56631]) ).
cnf(c_56633,negated_conjecture,
( r1_lattices(sK0,A,sK1)
| ~ r3_lattices(sK0,A,sK1)
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_3090,c_56632]) ).
cnf(c_7811,negated_conjecture,
( r1_lattices(sK0,A,sK1)
| ~ r3_lattices(sK0,A,sK1)
| ~ m1_subset_1(A,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_1902,c_56633]) ).
cnf(c_56634,negated_conjecture,
( k1_lattices(sK0,sK1,sK1) = sK1
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0)
| ~ v8_lattices(sK0)
| ~ v6_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_1903,c_1054]) ).
cnf(c_56635,negated_conjecture,
( k1_lattices(sK0,sK1,sK1) = sK1
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0)
| ~ v8_lattices(sK0)
| ~ v6_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1900,c_56634]) ).
cnf(c_56636,negated_conjecture,
( k1_lattices(sK0,sK1,sK1) = sK1
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0)
| ~ v8_lattices(sK0) ),
inference(resolve,[status(thm)],[c_3092,c_56635]) ).
cnf(c_56637,negated_conjecture,
( k1_lattices(sK0,sK1,sK1) = sK1
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0) ),
inference(resolve,[status(thm)],[c_3093,c_56636]) ).
cnf(c_56638,negated_conjecture,
( k1_lattices(sK0,sK1,sK1) = sK1
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_3090,c_56637]) ).
cnf(c_7843,negated_conjecture,
k1_lattices(sK0,sK1,sK1) = sK1,
inference(resolve,[status(thm)],[c_1902,c_56638]) ).
cnf(c_56639,plain,
( r1_lattices(sK0,sK1,sK1)
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l2_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_7843,c_991]) ).
cnf(c_56640,plain,
( r1_lattices(sK0,sK1,sK1)
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l2_lattices(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_56639]) ).
cnf(c_56641,negated_conjecture,
( r1_lattices(sK0,sK1,sK1)
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l2_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1900,c_56640]) ).
cnf(c_56642,negated_conjecture,
( r1_lattices(sK0,sK1,sK1)
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_3261,c_56641]) ).
cnf(c_13413,negated_conjecture,
r1_lattices(sK0,sK1,sK1),
inference(resolve,[status(thm)],[c_1903,c_56642]) ).
cnf(c_56643,plain,
( r3_lattices(sK0,sK1,sK1)
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0)
| ~ v8_lattices(sK0)
| ~ v6_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_13413,c_1092]) ).
cnf(c_56644,plain,
( r3_lattices(sK0,sK1,sK1)
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0)
| ~ v8_lattices(sK0)
| ~ v6_lattices(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_56643]) ).
cnf(c_56645,negated_conjecture,
( r3_lattices(sK0,sK1,sK1)
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0)
| ~ v8_lattices(sK0)
| ~ v6_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1900,c_56644]) ).
cnf(c_56646,negated_conjecture,
( r3_lattices(sK0,sK1,sK1)
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0)
| ~ v8_lattices(sK0) ),
inference(resolve,[status(thm)],[c_3092,c_56645]) ).
cnf(c_56647,negated_conjecture,
( r3_lattices(sK0,sK1,sK1)
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0) ),
inference(resolve,[status(thm)],[c_3093,c_56646]) ).
cnf(c_56648,negated_conjecture,
( r3_lattices(sK0,sK1,sK1)
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_3090,c_56647]) ).
cnf(c_56649,negated_conjecture,
( r3_lattices(sK0,sK1,sK1)
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_1902,c_56648]) ).
cnf(c_13417,negated_conjecture,
r3_lattices(sK0,sK1,sK1),
inference(resolve,[status(thm)],[c_1903,c_56649]) ).
cnf(c_56650,plain,
( r3_lattices(sK0,sK1,k3_lattices(sK0,sK1,A))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,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_1705,c_13417]) ).
cnf(c_56651,plain,
( r3_lattices(sK0,sK1,k3_lattices(sK0,sK1,A))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_56650]) ).
cnf(c_56652,negated_conjecture,
( r3_lattices(sK0,sK1,k3_lattices(sK0,sK1,A))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1900,c_56651]) ).
cnf(c_56653,negated_conjecture,
( r3_lattices(sK0,sK1,k3_lattices(sK0,sK1,A))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1901,c_56652]) ).
cnf(c_56654,negated_conjecture,
( r3_lattices(sK0,sK1,k3_lattices(sK0,sK1,A))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_1902,c_56653]) ).
cnf(c_22305,negated_conjecture,
( r3_lattices(sK0,sK1,k3_lattices(sK0,sK1,A))
| ~ m1_subset_1(A,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_1903,c_56654]) ).
cnf(c_56655,negated_conjecture,
( m1_filter_0(u1_struct_0(sK0),sK0)
| ~ l3_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_1750,c_1901]) ).
cnf(c_56656,negated_conjecture,
( m1_filter_0(u1_struct_0(sK0),sK0)
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1900,c_56655]) ).
cnf(c_28085,negated_conjecture,
m1_filter_0(u1_struct_0(sK0),sK0),
inference(resolve,[status(thm)],[c_1902,c_56656]) ).
cnf(c_56657,plain,
( ~ v1_xboole_0(u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_1755,c_28085]) ).
cnf(c_56658,negated_conjecture,
( ~ v1_xboole_0(u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1900,c_56657]) ).
cnf(c_56659,negated_conjecture,
( ~ v1_xboole_0(u1_struct_0(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1901,c_56658]) ).
cnf(c_28435,negated_conjecture,
~ v1_xboole_0(u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_1902,c_56659]) ).
cnf(c_56660,negated_conjecture,
( r3_lattices(sK0,A,sK1)
| ~ r2_hidden(A,k18_filter_2(sK0,sK1))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_1895,c_1903]) ).
cnf(c_56661,negated_conjecture,
( r3_lattices(sK0,A,sK1)
| ~ r2_hidden(A,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0)
| v3_struct_0(sK0) ),
inference(paramod,[status(thm)],[c_1906,c_56660]) ).
cnf(c_56662,negated_conjecture,
( r3_lattices(sK0,A,sK1)
| ~ r2_hidden(A,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v10_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1900,c_56661]) ).
cnf(c_56663,negated_conjecture,
( r3_lattices(sK0,A,sK1)
| ~ r2_hidden(A,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1901,c_56662]) ).
cnf(c_31774,negated_conjecture,
( r3_lattices(sK0,A,sK1)
| ~ r2_hidden(A,u1_struct_0(sK0))
| ~ m1_subset_1(A,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_1902,c_56663]) ).
cnf(c_43771,plain,
m1_subset_1(k3_lattices(sK0,sK1,sK2),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_7804,c_1904]) ).
cnf(c_56664,plain,
( r2_hidden(k3_lattices(sK0,sK1,sK2),u1_struct_0(sK0))
| v1_xboole_0(u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_43771,c_1648]) ).
cnf(c_43793,plain,
r2_hidden(k3_lattices(sK0,sK1,sK2),u1_struct_0(sK0)),
inference(resolve,[status(thm)],[c_28435,c_56664]) ).
cnf(c_46730,plain,
r3_lattices(sK0,sK1,k3_lattices(sK0,sK1,sK2)),
inference(resolve,[status(thm)],[c_22305,c_1904]) ).
cnf(c_56665,plain,
( r1_lattices(sK0,sK1,k3_lattices(sK0,sK1,sK2))
| ~ m1_subset_1(k3_lattices(sK0,sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0)
| ~ v8_lattices(sK0)
| ~ v6_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_46730,c_1091]) ).
cnf(c_56666,negated_conjecture,
( r1_lattices(sK0,sK1,k3_lattices(sK0,sK1,sK2))
| ~ m1_subset_1(k3_lattices(sK0,sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0)
| ~ v8_lattices(sK0)
| ~ v6_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1900,c_56665]) ).
cnf(c_56667,negated_conjecture,
( r1_lattices(sK0,sK1,k3_lattices(sK0,sK1,sK2))
| ~ m1_subset_1(k3_lattices(sK0,sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0)
| ~ v8_lattices(sK0) ),
inference(resolve,[status(thm)],[c_3092,c_56666]) ).
cnf(c_56668,negated_conjecture,
( r1_lattices(sK0,sK1,k3_lattices(sK0,sK1,sK2))
| ~ m1_subset_1(k3_lattices(sK0,sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0)
| ~ v9_lattices(sK0) ),
inference(resolve,[status(thm)],[c_3093,c_56667]) ).
cnf(c_56669,negated_conjecture,
( r1_lattices(sK0,sK1,k3_lattices(sK0,sK1,sK2))
| ~ m1_subset_1(k3_lattices(sK0,sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ l3_lattices(sK0) ),
inference(resolve,[status(thm)],[c_3090,c_56668]) ).
cnf(c_56670,negated_conjecture,
( r1_lattices(sK0,sK1,k3_lattices(sK0,sK1,sK2))
| ~ m1_subset_1(k3_lattices(sK0,sK1,sK2),u1_struct_0(sK0))
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_1902,c_56669]) ).
cnf(c_56671,negated_conjecture,
( r1_lattices(sK0,sK1,k3_lattices(sK0,sK1,sK2))
| ~ m1_subset_1(k3_lattices(sK0,sK1,sK2),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_1903,c_56670]) ).
cnf(c_46738,negated_conjecture,
r1_lattices(sK0,sK1,k3_lattices(sK0,sK1,sK2)),
inference(resolve,[status(thm)],[c_43771,c_56671]) ).
cnf(c_56672,plain,
( sK1 = k3_lattices(sK0,sK1,sK2)
| ~ r1_lattices(sK0,k3_lattices(sK0,sK1,sK2),sK1)
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ m1_subset_1(k3_lattices(sK0,sK1,sK2),u1_struct_0(sK0))
| ~ l2_lattices(sK0)
| ~ v4_lattices(sK0)
| v3_struct_0(sK0) ),
inference(resolve,[status(thm)],[c_46738,c_1061]) ).
cnf(c_56673,plain,
( k3_lattices(sK0,sK1,sK2) = sK1
| ~ r1_lattices(sK0,k3_lattices(sK0,sK1,sK2),sK1)
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ m1_subset_1(k3_lattices(sK0,sK1,sK2),u1_struct_0(sK0))
| ~ l2_lattices(sK0)
| ~ v4_lattices(sK0)
| v3_struct_0(sK0) ),
inference(copy,[status(thm)],[c_56672]) ).
cnf(c_56674,negated_conjecture,
( k3_lattices(sK0,sK1,sK2) = sK1
| ~ r1_lattices(sK0,k3_lattices(sK0,sK1,sK2),sK1)
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ m1_subset_1(k3_lattices(sK0,sK1,sK2),u1_struct_0(sK0))
| ~ l2_lattices(sK0)
| ~ v4_lattices(sK0) ),
inference(resolve,[status(thm)],[c_1900,c_56673]) ).
cnf(c_56675,negated_conjecture,
( k3_lattices(sK0,sK1,sK2) = sK1
| ~ r1_lattices(sK0,k3_lattices(sK0,sK1,sK2),sK1)
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ m1_subset_1(k3_lattices(sK0,sK1,sK2),u1_struct_0(sK0))
| ~ l2_lattices(sK0) ),
inference(resolve,[status(thm)],[c_3095,c_56674]) ).
cnf(c_56676,negated_conjecture,
( k3_lattices(sK0,sK1,sK2) = sK1
| ~ r1_lattices(sK0,k3_lattices(sK0,sK1,sK2),sK1)
| ~ m1_subset_1(sK1,u1_struct_0(sK0))
| ~ m1_subset_1(k3_lattices(sK0,sK1,sK2),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_3261,c_56675]) ).
cnf(c_56677,negated_conjecture,
( k3_lattices(sK0,sK1,sK2) = sK1
| ~ r1_lattices(sK0,k3_lattices(sK0,sK1,sK2),sK1)
| ~ m1_subset_1(sK1,u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_43771,c_56676]) ).
cnf(c_56678,negated_conjecture,
( k3_lattices(sK0,sK1,sK2) = sK1
| ~ r1_lattices(sK0,k3_lattices(sK0,sK1,sK2),sK1) ),
inference(resolve,[status(thm)],[c_1903,c_56677]) ).
cnf(c_46739,negated_conjecture,
~ r1_lattices(sK0,k3_lattices(sK0,sK1,sK2),sK1),
inference(resolve,[status(thm)],[c_1905,c_56678]) ).
cnf(c_56679,plain,
( r1_lattices(sK0,k3_lattices(sK0,sK1,sK2),sK1)
| ~ r3_lattices(sK0,k3_lattices(sK0,sK1,sK2),sK1) ),
inference(resolve,[status(thm)],[c_7811,c_43771]) ).
cnf(c_53813,plain,
~ r3_lattices(sK0,k3_lattices(sK0,sK1,sK2),sK1),
inference(resolve,[status(thm)],[c_46739,c_56679]) ).
cnf(c_56680,plain,
( r3_lattices(sK0,k3_lattices(sK0,sK1,sK2),sK1)
| ~ r2_hidden(k3_lattices(sK0,sK1,sK2),u1_struct_0(sK0)) ),
inference(resolve,[status(thm)],[c_31774,c_43771]) ).
cnf(c_56681,plain,
r3_lattices(sK0,k3_lattices(sK0,sK1,sK2),sK1),
inference(resolve,[status(thm)],[c_43793,c_56680]) ).
cnf(c_56617,plain,
$false,
inference(resolve,[status(thm)],[c_53813,c_56681]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT308+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.02 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.38 % Computer : n014.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Fri Sep 25 20:41:53 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.39 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.39 % Process 1052486 was started by sandbox on n014,
% 0.09/0.39 % Fri Sep 25 20:41:53 2026
% 0.09/0.39 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 192.56/33.58
% 192.56/33.58 % SInE (scan): 357 to sos (tol 1.5x), 164 to usable (tol 2.0x), 13100 zapped, of 13621 axioms (depth 3).
% 192.56/33.58
% 192.56/33.58 % From the command line: assign(max_seconds, 300).
% 192.56/33.58
% 192.56/33.58 % given #500 (T,wt=17): 17715 v1_xboole_0(u1_struct_0(c20)) | -r2_hidden(u1_struct_0(c20),c22). [resolve(8220,b,1642,b)].
% 192.56/33.58
% 192.56/33.58 % given #1000 (A,wt=115): 1797 -l3_lattices(A) | v3_lattices(k1_lattice2(A)) # tptp_name(dt_k1_lattice2) # sine_depth(2). [clausify(62)].
% 192.56/33.58
% 192.56/33.58 % given #1500 (W,wt=18): 30689 -r1_tarski(f24(c15),A) | r2_hidden(k6_lattices(c15),A). [resolve(30079,a,520,b)].
% 192.56/33.58
% 192.56/33.58 % given #2000 (F,wt=26): 35985 -r2_hidden(k18_filter_2(c20,c22),k7_lattices(c20,c22)) | -r2_hidden(u1_struct_0(c20),k6_lattices(c19)) | -r2_hidden(u1_struct_0(c19),c22). [resolve(34047,b,28594,a)].
% 192.56/33.58
% 192.56/33.58 % given #2500 (W,wt=18): 38548 -v3_filter_0(k8_filter_1(c20,c13)) | v14_lattices(k8_filter_1(c20,c13)). [back_unit_del(28295),unit_del(a,38495)].
% 192.56/33.58
% 192.56/33.58 % given #3000 (F,wt=26): 40474 -r2_hidden(u1_struct_0(c20),k6_lattices(c14)) | -r2_hidden(u1_struct_0(c14),k6_lattices(c13)) | -r2_hidden(f24(c13),k15_lattice3(c20,A)). [resolve(40014,c,30147,a)].
% 192.56/33.58
% 192.56/33.58 % given #3500 (T,wt=20): 38671 m1_filter_2(A,k8_filter_1(c20,c15)) | -m1_filter_0(A,k8_filter_1(c20,c15)). [resolve(38493,a,1602,b),unit_del(a,27400),unit_del(b,24998)].
% 192.56/33.58
% 192.56/33.58 % given #4000 (F,wt=17): 42268 -r1_tarski(u1_struct_0(c20),k3_lattices(c20,c22,c22)). [resolve(42069,a,626,a)].
% 192.56/33.58
% 192.56/33.58 % given #4500 (T,wt=18): 45413 -r1_tarski(A,f165(c20)) | r1_tarski(A,u1_struct_0(c20)). [resolve(45389,a,536,b)].
% 192.56/33.58
% 192.56/33.58 % given #5000 (F,wt=26): 42210 -r2_hidden(k3_lattices(c20,c21,c21),f2(k15_lattice3(c20,A),u1_struct_0(c20))). [resolve(42051,a,31686,a)].
% 192.56/33.58
% 192.56/33.58 % given #5500 (T,wt=19): 51265 r2_hidden(A,k1_zfmisc_1(k1_xboole_0)) | -r2_hidden(A,f39(A,k1_xboole_0)). [resolve(51174,b,1642,b)].
% 192.56/33.58
% 192.56/33.58 % given #6000 (A,wt=45): 2634 v3_struct_0(c1) | -v10_lattices(c1) | -m1_subset_1(A,u1_struct_0(c1)) | -v3_filter_0(c1) | -m1_subset_1(B,u1_struct_0(c1)) | k4_filter_0(c1,A,A) = B | -r3_lattices(c1,k4_lattices(c1,A,B),A) | -r3_lattices(c1,f143(c1,A,A,B),B). [factor(2368,c,d)].
% 192.56/33.58
% 192.56/33.58 % SZS status Theorem for theBenchmark
% 192.56/33.58
% 192.56/33.58 % Proof 1 at 23.95 (+ 3.31) seconds.
% 192.56/33.58 % Length of proof is 57.
% 192.56/33.58 % Level of proof is 11.
% 192.56/33.58 % Maximum clause weight is 120.000.
% 192.56/33.58 % Given clauses 6317.
% 192.56/33.58
% 192.56/33.58 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------