%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT323+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 : 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:13 AM UTC 2026
% Result : Theorem 7.70s 1.51s
% Output : CNFRefutation 7.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 16
% Syntax : Number of formulae : 131 ( 22 unt; 0 def)
% Number of atoms : 612 ( 28 equ)
% Maximal formula atoms : 20 ( 4 avg)
% Number of connectives : 802 ( 321 ~; 363 |; 81 &)
% ( 5 <=>; 32 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 28 ( 26 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-2 aty)
% Number of variables : 99 ( 0 sgn 33 !; 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(dt_k15_filter_2,axiom,
! [A,B] :
( ( m2_filter_2(B,A)
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m1_filter_2(k15_filter_2(A,B),k1_lattice2(A)) ),
file('theBenchmark.p',dt_k15_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_m2_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( m2_lattice4(B,A)
& ~ v1_xboole_0(B) ) ) ),
file('theBenchmark.p',dt_m2_filter_2) ).
fof(dt_m2_lattice4,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_lattice4(B,A)
=> m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ),
file('theBenchmark.p',dt_m2_lattice4) ).
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(fc4_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v17_lattices(k1_lattice2(A))
& v16_lattices(k1_lattice2(A))
& v15_lattices(k1_lattice2(A))
& v14_lattices(k1_lattice2(A))
& v13_lattices(k1_lattice2(A))
& v12_lattices(k1_lattice2(A))
& v11_lattices(k1_lattice2(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',fc4_filter_2) ).
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(l70_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> k7_lattices(k1_lattice2(A),k5_filter_2(A,B)) = k7_lattices(A,B) ) ),
file('theBenchmark.p',l70_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(redefinition_m1_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_filter_2(B,A)
<=> m1_filter_0(B,A) ) ),
file('theBenchmark.p',redefinition_m1_filter_2) ).
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(t59_filter_0,axiom,
! [A] :
( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_filter_0(B,A)
=> ( v1_filter_0(B,A)
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( r2_hidden(C,B)
<=> ~ r2_hidden(k7_lattices(A,C),B) ) ) ) ) ),
file('theBenchmark.p',t59_filter_0) ).
fof(t59_filter_2,conjecture,
! [A] :
( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( r2_filter_2(A,B)
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( r2_hidden(C,B)
<=> ~ r2_hidden(k7_lattices(A,C),B) ) ) ) ) ),
file('theBenchmark.p',t59_filter_2) ).
fof(t59_filter_2_neg,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( r2_filter_2(A,B)
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( r2_hidden(C,B)
<=> ~ r2_hidden(k7_lattices(A,C),B) ) ) ) ) ),
inference(assume_negation,[status(cth)],[t59_filter_2]) ).
cnf(c_97,plain,
( m2_lattice4(B,A)
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_m2_filter_2]) ).
cnf(c_99,plain,
( m1_filter_2(k15_filter_2(A,B),k1_lattice2(A))
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k15_filter_2]) ).
cnf(c_100,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_101,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_95,plain,
? [A] :
( ? [B] :
( ? [C] :
( ( r2_hidden(k7_lattices(A,C),B)
| ~ r2_hidden(C,B) )
& ( ~ r2_hidden(k7_lattices(A,C),B)
| r2_hidden(C,B) )
& m1_subset_1(C,u1_struct_0(A)) )
& r2_filter_2(A,B)
& m2_filter_2(B,A) )
& l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t59_filter_2_neg]) ).
fof(sk_t59_filter_2_neg,plain,
( ( r2_hidden(k7_lattices(sK1,sK2),sK0)
| ~ r2_hidden(sK2,sK0) )
& ( ~ r2_hidden(k7_lattices(sK1,sK2),sK0)
| r2_hidden(sK2,sK0) )
& m1_subset_1(sK2,u1_struct_0(sK1))
& r2_filter_2(sK1,sK0)
& m2_filter_2(sK0,sK1)
& l3_lattices(sK1)
& v17_lattices(sK1)
& v10_lattices(sK1)
& ~ v3_struct_0(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK0,sK2]),skolemize(A,sK1),skolemize(B,sK0),skolemize(C,sK2)],[nnf_95]) ).
cnf(c_103,negated_conjecture,
m2_filter_2(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_t59_filter_2_neg]) ).
cnf(c_231,plain,
( m1_filter_0(B,A)
| ~ m1_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[redefinition_m1_filter_2]) ).
cnf(c_234,negated_conjecture,
( m1_filter_2(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_103,c_99]) ).
cnf(c_246,plain,
( ~ r2_hidden(k7_lattices(A,C),B)
| ~ r2_hidden(C,B)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ v1_filter_0(B,A)
| ~ m1_filter_0(B,A)
| ~ l3_lattices(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t59_filter_0]) ).
cnf(c_247,plain,
( r2_hidden(k7_lattices(A,C),B)
| r2_hidden(C,B)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ v1_filter_0(B,A)
| ~ m1_filter_0(B,A)
| ~ l3_lattices(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t59_filter_0]) ).
cnf(c_251,negated_conjecture,
( ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1)
| m1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_231,c_234]) ).
cnf(c_254,plain,
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ m2_lattice4(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_m2_lattice4]) ).
cnf(c_263,negated_conjecture,
( m2_lattice4(sK0,sK1)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_103,c_97]) ).
cnf(c_287,negated_conjecture,
( r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| r2_hidden(A,k15_filter_2(sK1,sK0))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1)))
| ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_251,c_247]) ).
cnf(c_3439,negated_conjecture,
( r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| r2_hidden(A,k15_filter_2(sK1,sK0))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1)))
| ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(copy,[status(thm)],[c_287]) ).
cnf(c_3440,negated_conjecture,
( r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| r2_hidden(A,k15_filter_2(sK1,sK0))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1)))
| ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(copy,[status(thm)],[c_3439]) ).
cnf(c_288,negated_conjecture,
( r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| r2_hidden(A,k15_filter_2(sK1,sK0))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1)))
| ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(copy,[status(thm)],[c_3440]) ).
cnf(c_289,negated_conjecture,
( ~ r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| ~ r2_hidden(A,k15_filter_2(sK1,sK0))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1)))
| ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_251,c_246]) ).
cnf(c_3441,negated_conjecture,
( ~ r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| ~ r2_hidden(A,k15_filter_2(sK1,sK0))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1)))
| ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(copy,[status(thm)],[c_289]) ).
cnf(c_3442,negated_conjecture,
( ~ r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| ~ r2_hidden(A,k15_filter_2(sK1,sK0))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1)))
| ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(copy,[status(thm)],[c_3441]) ).
cnf(c_290,negated_conjecture,
( ~ r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| ~ r2_hidden(A,k15_filter_2(sK1,sK0))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1)))
| ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(copy,[status(thm)],[c_3442]) ).
cnf(c_351,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_352,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_354,plain,
( l3_lattices(k1_lattice2(A))
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_k1_lattice2]) ).
cnf(c_355,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_370,plain,
( ~ v3_struct_0(k1_lattice2(A))
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_lattice2]) ).
cnf(c_378,plain,
( v17_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc4_filter_2]) ).
cnf(c_380,plain,
( v10_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc6_lattice2]) ).
cnf(c_384,plain,
( k7_lattices(k1_lattice2(A),k5_filter_2(A,B)) = k7_lattices(A,B)
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[l70_filter_2]) ).
cnf(c_431,negated_conjecture,
~ v3_struct_0(sK1),
inference(split_conjunct,[status(thm)],[sk_t59_filter_2_neg]) ).
cnf(c_432,negated_conjecture,
v10_lattices(sK1),
inference(split_conjunct,[status(thm)],[sk_t59_filter_2_neg]) ).
cnf(c_433,negated_conjecture,
v17_lattices(sK1),
inference(split_conjunct,[status(thm)],[sk_t59_filter_2_neg]) ).
cnf(c_434,negated_conjecture,
l3_lattices(sK1),
inference(split_conjunct,[status(thm)],[sk_t59_filter_2_neg]) ).
cnf(c_435,negated_conjecture,
r2_filter_2(sK1,sK0),
inference(split_conjunct,[status(thm)],[sk_t59_filter_2_neg]) ).
cnf(c_436,negated_conjecture,
m1_subset_1(sK2,u1_struct_0(sK1)),
inference(split_conjunct,[status(thm)],[sk_t59_filter_2_neg]) ).
cnf(c_437,negated_conjecture,
( ~ r2_hidden(k7_lattices(sK1,sK2),sK0)
| r2_hidden(sK2,sK0) ),
inference(split_conjunct,[status(thm)],[sk_t59_filter_2_neg]) ).
cnf(c_438,negated_conjecture,
( r2_hidden(k7_lattices(sK1,sK2),sK0)
| ~ r2_hidden(sK2,sK0) ),
inference(split_conjunct,[status(thm)],[sk_t59_filter_2_neg]) ).
cnf(c_447,negated_conjecture,
( v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ r2_filter_2(sK1,sK0)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_103,c_101]) ).
cnf(c_3443,negated_conjecture,
( v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ r2_filter_2(sK1,sK0)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_431,c_447]) ).
cnf(c_3444,negated_conjecture,
( v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ r2_filter_2(sK1,sK0)
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_432,c_3443]) ).
cnf(c_3445,negated_conjecture,
( v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ r2_filter_2(sK1,sK0) ),
inference(resolve,[status(thm)],[c_434,c_3444]) ).
cnf(c_448,negated_conjecture,
v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1)),
inference(resolve,[status(thm)],[c_435,c_3445]) ).
cnf(c_449,negated_conjecture,
( k15_filter_2(sK1,sK0) = k7_filter_2(sK1,sK0)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_103,c_100]) ).
cnf(c_3446,negated_conjecture,
( k7_filter_2(sK1,sK0) = k15_filter_2(sK1,sK0)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_449]) ).
cnf(c_3447,negated_conjecture,
( k7_filter_2(sK1,sK0) = k15_filter_2(sK1,sK0)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_431,c_3446]) ).
cnf(c_3448,negated_conjecture,
( k7_filter_2(sK1,sK0) = k15_filter_2(sK1,sK0)
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_432,c_3447]) ).
cnf(c_450,negated_conjecture,
k7_filter_2(sK1,sK0) = k15_filter_2(sK1,sK0),
inference(resolve,[status(thm)],[c_434,c_3448]) ).
cnf(c_507,negated_conjecture,
( m1_subset_1(sK0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_263,c_254]) ).
cnf(c_3449,negated_conjecture,
( m1_subset_1(sK0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_507]) ).
cnf(c_3450,negated_conjecture,
( m1_subset_1(sK0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_3449]) ).
cnf(c_3451,negated_conjecture,
( m1_subset_1(sK0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_3450]) ).
cnf(c_3452,negated_conjecture,
( m1_subset_1(sK0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_431,c_3451]) ).
cnf(c_3453,negated_conjecture,
( m1_subset_1(sK0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_432,c_3452]) ).
cnf(c_508,negated_conjecture,
m1_subset_1(sK0,k1_zfmisc_1(u1_struct_0(sK1))),
inference(resolve,[status(thm)],[c_434,c_3453]) ).
cnf(c_3454,negated_conjecture,
( ~ r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| ~ r2_hidden(A,k15_filter_2(sK1,sK0))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1)))
| ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_431,c_290]) ).
cnf(c_3455,negated_conjecture,
( ~ r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| ~ r2_hidden(A,k15_filter_2(sK1,sK0))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1)))
| ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_432,c_3454]) ).
cnf(c_3456,negated_conjecture,
( ~ r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| ~ r2_hidden(A,k15_filter_2(sK1,sK0))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1)))
| ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_434,c_3455]) ).
cnf(c_528,negated_conjecture,
( ~ r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| ~ r2_hidden(A,k15_filter_2(sK1,sK0))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1)))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_448,c_3456]) ).
cnf(c_3457,negated_conjecture,
( r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| r2_hidden(A,k15_filter_2(sK1,sK0))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1)))
| ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_431,c_288]) ).
cnf(c_3458,negated_conjecture,
( r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| r2_hidden(A,k15_filter_2(sK1,sK0))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1)))
| ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_432,c_3457]) ).
cnf(c_3459,negated_conjecture,
( r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| r2_hidden(A,k15_filter_2(sK1,sK0))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1)))
| ~ v1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_434,c_3458]) ).
cnf(c_529,negated_conjecture,
( r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| r2_hidden(A,k15_filter_2(sK1,sK0))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1)))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_448,c_3459]) ).
cnf(c_3460,negated_conjecture,
( v10_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_432,c_380]) ).
cnf(c_3461,negated_conjecture,
( v10_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_431,c_3460]) ).
cnf(c_747,negated_conjecture,
v10_lattices(k1_lattice2(sK1)),
inference(resolve,[status(thm)],[c_434,c_3461]) ).
cnf(c_750,negated_conjecture,
( r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| r2_hidden(A,k15_filter_2(sK1,sK0))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1)))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_747,c_529]) ).
cnf(c_751,negated_conjecture,
( ~ r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| ~ r2_hidden(A,k15_filter_2(sK1,sK0))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1)))
| ~ v17_lattices(k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_747,c_528]) ).
cnf(c_3462,negated_conjecture,
( v17_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_433,c_378]) ).
cnf(c_3463,negated_conjecture,
( v17_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_431,c_3462]) ).
cnf(c_3464,negated_conjecture,
( v17_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_432,c_3463]) ).
cnf(c_754,negated_conjecture,
v17_lattices(k1_lattice2(sK1)),
inference(resolve,[status(thm)],[c_434,c_3464]) ).
cnf(c_761,negated_conjecture,
( ~ r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| ~ r2_hidden(A,k15_filter_2(sK1,sK0))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1)))
| ~ l3_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_754,c_751]) ).
cnf(c_762,negated_conjecture,
( r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| r2_hidden(A,k15_filter_2(sK1,sK0))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1)))
| ~ l3_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_754,c_750]) ).
cnf(c_3465,negated_conjecture,
( ~ v3_struct_0(k1_lattice2(sK1))
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_434,c_370]) ).
cnf(c_763,negated_conjecture,
~ v3_struct_0(k1_lattice2(sK1)),
inference(resolve,[status(thm)],[c_431,c_3465]) ).
cnf(c_766,plain,
l3_lattices(k1_lattice2(sK1)),
inference(resolve,[status(thm)],[c_434,c_354]) ).
cnf(c_3466,negated_conjecture,
( r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| r2_hidden(A,k15_filter_2(sK1,sK0))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1)))
| ~ l3_lattices(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_763,c_762]) ).
cnf(c_778,negated_conjecture,
( r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| r2_hidden(A,k15_filter_2(sK1,sK0))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1))) ),
inference(resolve,[status(thm)],[c_766,c_3466]) ).
cnf(c_3467,negated_conjecture,
( ~ r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| ~ r2_hidden(A,k15_filter_2(sK1,sK0))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1)))
| ~ l3_lattices(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_763,c_761]) ).
cnf(c_779,negated_conjecture,
( ~ r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| ~ r2_hidden(A,k15_filter_2(sK1,sK0))
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1))) ),
inference(resolve,[status(thm)],[c_766,c_3467]) ).
cnf(c_3468,negated_conjecture,
( k5_filter_2(sK1,sK2) = sK2
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_436,c_351]) ).
cnf(c_3469,negated_conjecture,
( k5_filter_2(sK1,sK2) = sK2
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_431,c_3468]) ).
cnf(c_3470,negated_conjecture,
( k5_filter_2(sK1,sK2) = sK2
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_432,c_3469]) ).
cnf(c_790,negated_conjecture,
k5_filter_2(sK1,sK2) = sK2,
inference(resolve,[status(thm)],[c_434,c_3470]) ).
cnf(c_3471,negated_conjecture,
( k7_lattices(k1_lattice2(sK1),k5_filter_2(sK1,A)) = k7_lattices(sK1,A)
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ l3_lattices(sK1)
| ~ v17_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_384,c_432]) ).
cnf(c_3472,negated_conjecture,
( k7_lattices(k1_lattice2(sK1),k5_filter_2(sK1,A)) = k7_lattices(sK1,A)
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ l3_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_3471,c_433]) ).
cnf(c_3473,negated_conjecture,
( k7_lattices(k1_lattice2(sK1),k5_filter_2(sK1,A)) = k7_lattices(sK1,A)
| ~ m1_subset_1(A,u1_struct_0(sK1))
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_3472,c_434]) ).
cnf(c_3474,negated_conjecture,
( k7_lattices(k1_lattice2(sK1),k5_filter_2(sK1,sK2)) = k7_lattices(sK1,sK2)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_3473,c_436]) ).
cnf(c_3475,negated_conjecture,
( k7_lattices(k1_lattice2(sK1),sK2) = k7_lattices(sK1,sK2)
| v3_struct_0(sK1) ),
inference(paramod,[status(thm)],[c_790,c_3474]) ).
cnf(c_791,negated_conjecture,
k7_lattices(k1_lattice2(sK1),sK2) = k7_lattices(sK1,sK2),
inference(resolve,[status(thm)],[c_431,c_3475]) ).
cnf(c_3476,negated_conjecture,
( m1_subset_1(k5_filter_2(sK1,A),u1_struct_0(k1_lattice2(sK1)))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| ~ l3_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_355,c_432]) ).
cnf(c_3477,negated_conjecture,
( m1_subset_1(k5_filter_2(sK1,A),u1_struct_0(k1_lattice2(sK1)))
| ~ m1_subset_1(A,u1_struct_0(sK1))
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_3476,c_434]) ).
cnf(c_3478,negated_conjecture,
( m1_subset_1(k5_filter_2(sK1,sK2),u1_struct_0(k1_lattice2(sK1)))
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_3477,c_436]) ).
cnf(c_3479,negated_conjecture,
( m1_subset_1(sK2,u1_struct_0(k1_lattice2(sK1)))
| v3_struct_0(sK1) ),
inference(paramod,[status(thm)],[c_790,c_3478]) ).
cnf(c_792,negated_conjecture,
m1_subset_1(sK2,u1_struct_0(k1_lattice2(sK1))),
inference(resolve,[status(thm)],[c_431,c_3479]) ).
cnf(c_3480,negated_conjecture,
( k7_filter_2(sK1,sK0) = sK0
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_508,c_352]) ).
cnf(c_3481,negated_conjecture,
( k15_filter_2(sK1,sK0) = sK0
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(paramod,[status(thm)],[c_450,c_3480]) ).
cnf(c_3482,negated_conjecture,
( k15_filter_2(sK1,sK0) = sK0
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_431,c_3481]) ).
cnf(c_3483,negated_conjecture,
( k15_filter_2(sK1,sK0) = sK0
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_432,c_3482]) ).
cnf(c_832,negated_conjecture,
k15_filter_2(sK1,sK0) = sK0,
inference(resolve,[status(thm)],[c_434,c_3483]) ).
cnf(c_3484,negated_conjecture,
( ~ r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| ~ r2_hidden(A,sK0)
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1))) ),
inference(paramod,[status(thm)],[c_832,c_779]) ).
cnf(c_834,negated_conjecture,
( ~ r2_hidden(k7_lattices(k1_lattice2(sK1),A),sK0)
| ~ r2_hidden(A,sK0)
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1))) ),
inference(paramod,[status(thm)],[c_832,c_3484]) ).
cnf(c_3485,negated_conjecture,
( r2_hidden(k7_lattices(k1_lattice2(sK1),A),k15_filter_2(sK1,sK0))
| r2_hidden(A,sK0)
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1))) ),
inference(paramod,[status(thm)],[c_832,c_778]) ).
cnf(c_835,negated_conjecture,
( r2_hidden(k7_lattices(k1_lattice2(sK1),A),sK0)
| r2_hidden(A,sK0)
| ~ m1_subset_1(A,u1_struct_0(k1_lattice2(sK1))) ),
inference(paramod,[status(thm)],[c_832,c_3485]) ).
cnf(c_3486,plain,
( ~ r2_hidden(k7_lattices(sK1,sK2),sK0)
| ~ r2_hidden(sK2,sK0)
| ~ m1_subset_1(sK2,u1_struct_0(k1_lattice2(sK1))) ),
inference(paramod,[status(thm)],[c_791,c_834]) ).
cnf(c_2110,plain,
( ~ r2_hidden(k7_lattices(sK1,sK2),sK0)
| ~ r2_hidden(sK2,sK0) ),
inference(resolve,[status(thm)],[c_792,c_3486]) ).
cnf(c_3487,negated_conjecture,
( r2_hidden(k7_lattices(k1_lattice2(sK1),sK2),sK0)
| r2_hidden(sK2,sK0) ),
inference(resolve,[status(thm)],[c_835,c_792]) ).
cnf(c_3433,negated_conjecture,
( r2_hidden(k7_lattices(sK1,sK2),sK0)
| r2_hidden(sK2,sK0) ),
inference(paramod,[status(thm)],[c_791,c_3487]) ).
cnf(c_3488,negated_conjecture,
( r2_hidden(sK2,sK0)
| r2_hidden(sK2,sK0) ),
inference(resolve,[status(thm)],[c_3433,c_437]) ).
cnf(c_3436,negated_conjecture,
r2_hidden(sK2,sK0),
inference(copy,[status(thm)],[c_3488]) ).
cnf(c_3437,plain,
~ r2_hidden(k7_lattices(sK1,sK2),sK0),
inference(resolve,[status(thm)],[c_3436,c_2110]) ).
cnf(c_3489,negated_conjecture,
r2_hidden(k7_lattices(sK1,sK2),sK0),
inference(resolve,[status(thm)],[c_3436,c_438]) ).
cnf(c_3438,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_3437,c_3489]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT323+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.36 % Computer : n001.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 20:57:28 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 30945 was started by sandbox2 on n001,
% 0.10/0.37 % Fri Sep 25 20:57:28 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).
% 7.70/1.51
% 7.70/1.51 % given #500 (A,wt=66): 576 -v1_funct_1(A) | -v1_funct_2(A,k2_zfmisc_1(B,B),B) | -m1_relset_1(A,k2_zfmisc_1(B,B),B) | -v1_funct_1(f7(k2_zfmisc_1(B,B),B)) | -v1_funct_2(f7(k2_zfmisc_1(B,B),B),k2_zfmisc_1(B,B),B) | g3_lattices(B,A,f7(k2_zfmisc_1(B,B),B)) != g3_lattices(C,D,E) | D = A. [resolve(382,f,280,a),flip(f)].
% 7.70/1.51
% 7.70/1.51 % given #1000 (W,wt=23): 3116 -v3_struct_0(g3_lattices(u1_struct_0(c7),u2_lattices(c7),u2_lattices(c7))). [resolve(881,a,512,d),unit_del(a,878),unit_del(b,880),unit_del(c,879)].
% 7.70/1.51
% 7.70/1.51 % SZS status Theorem for theBenchmark
% 7.70/1.51
% 7.70/1.51 % Proof 1 at 0.95 (+ 0.14) seconds.
% 7.70/1.51 % Length of proof is 77.
% 7.70/1.51 % Level of proof is 14.
% 7.70/1.51 % Maximum clause weight is 57.000.
% 7.70/1.51 % Given clauses 1062.
% 7.70/1.51
% 7.70/1.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------