%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT317+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 : n012.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:11 AM UTC 2026
% Result : Theorem 4.28s 1.00s
% Output : CNFRefutation 4.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 18
% Syntax : Number of formulae : 159 ( 33 unt; 0 def)
% Number of atoms : 595 ( 55 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 692 ( 256 ~; 340 |; 62 &)
% ( 2 <=>; 32 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 22 ( 20 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 3 con; 0-3 aty)
% Number of variables : 116 ( 1 sgn 39 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d13_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)))
& ~ v1_xboole_0(B) )
=> ! [C] :
( ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
& ~ v1_xboole_0(C) )
=> k20_filter_2(A,B,C) = a_3_0_filter_2(A,B,C) ) ) ),
file('theBenchmark.p',d13_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_l2_lattices,axiom,
! [A] :
( l2_lattices(A)
=> l1_struct_0(A) ),
file('theBenchmark.p',dt_l2_lattices) ).
fof(dt_l3_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( l2_lattices(A)
& l1_lattices(A) ) ),
file('theBenchmark.p',dt_l3_lattices) ).
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(fc1_struct_0,axiom,
! [A] :
( ( l1_struct_0(A)
& ~ v3_struct_0(A) )
=> ~ v1_xboole_0(u1_struct_0(A)) ),
file('theBenchmark.p',fc1_struct_0) ).
fof(fc6_lattice2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v10_lattices(k1_lattice2(A))
& v9_lattices(k1_lattice2(A))
& v8_lattices(k1_lattice2(A))
& v7_lattices(k1_lattice2(A))
& v6_lattices(k1_lattice2(A))
& v5_lattices(k1_lattice2(A))
& v4_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ),
file('theBenchmark.p',fc6_lattice2) ).
fof(redefinition_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(reflexivity_r1_tarski,axiom,
! [A,B] : r1_tarski(A,A),
file('theBenchmark.p',reflexivity_r1_tarski) ).
fof(t3_subset,axiom,
! [A,B] :
( m1_subset_1(A,k1_zfmisc_1(B))
<=> r1_tarski(A,B) ),
file('theBenchmark.p',t3_subset) ).
fof(t45_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)))
& ~ v1_xboole_0(B) )
=> ! [C] :
( ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
& ~ v1_xboole_0(C) )
=> ! [D] :
( ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(k1_lattice2(A))))
& ~ v1_xboole_0(D) )
=> ! [E] :
( ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(k1_lattice2(A))))
& ~ v1_xboole_0(E) )
=> ( k20_filter_2(A,k8_filter_2(A,D),k8_filter_2(A,E)) = k5_filter_0(k1_lattice2(A),D,E)
& k20_filter_2(k1_lattice2(A),D,E) = k5_filter_0(A,k8_filter_2(A,D),k8_filter_2(A,E))
& k20_filter_2(k1_lattice2(A),k7_filter_2(A,B),k7_filter_2(A,C)) = k5_filter_0(A,B,C)
& k20_filter_2(A,B,C) = k5_filter_0(k1_lattice2(A),k7_filter_2(A,B),k7_filter_2(A,C)) ) ) ) ) ) ),
file('theBenchmark.p',t45_filter_2) ).
fof(t49_filter_0,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_filter_0(B,A)
=> ! [C] :
( m1_filter_0(C,A)
=> ( r1_tarski(C,k5_filter_0(A,B,C))
& r1_tarski(B,k5_filter_0(A,B,C)) ) ) ) ),
file('theBenchmark.p',t49_filter_0) ).
fof(t51_filter_2,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ! [C] :
( m2_filter_2(C,A)
=> ( r1_tarski(C,k20_filter_2(A,B,C))
& r1_tarski(B,k20_filter_2(A,B,C)) ) ) ) ),
file('theBenchmark.p',t51_filter_2) ).
fof(t51_filter_2_neg,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ! [C] :
( m2_filter_2(C,A)
=> ( r1_tarski(C,k20_filter_2(A,B,C))
& r1_tarski(B,k20_filter_2(A,B,C)) ) ) ) ),
inference(assume_negation,[status(cth)],[t51_filter_2]) ).
cnf(c_121,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_122,plain,
( ~ v1_xboole_0(B)
| ~ 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_123,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_124,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]) ).
fof(nnf_119,plain,
? [A] :
( ? [B] :
( ? [C] :
( ( ~ r1_tarski(C,k20_filter_2(A,B,C))
| ~ r1_tarski(B,k20_filter_2(A,B,C)) )
& m2_filter_2(C,A) )
& m2_filter_2(B,A) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t51_filter_2_neg]) ).
fof(sk_t51_filter_2_neg,plain,
( ( ~ r1_tarski(sK2,k20_filter_2(sK1,sK0,sK2))
| ~ r1_tarski(sK0,k20_filter_2(sK1,sK0,sK2)) )
& m2_filter_2(sK2,sK1)
& m2_filter_2(sK0,sK1)
& l3_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_119]) ).
cnf(c_125,negated_conjecture,
m2_filter_2(sK0,sK1),
inference(split_conjunct,[status(thm)],[sk_t51_filter_2_neg]) ).
cnf(c_126,negated_conjecture,
m2_filter_2(sK2,sK1),
inference(split_conjunct,[status(thm)],[sk_t51_filter_2_neg]) ).
cnf(c_196,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_199,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_125,c_123]) ).
cnf(c_200,negated_conjecture,
( m1_filter_2(k15_filter_2(sK1,sK2),k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_126,c_123]) ).
cnf(c_204,plain,
( ~ v1_xboole_0(u1_struct_0(A))
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_struct_0]) ).
cnf(c_206,plain,
( l1_struct_0(A)
| ~ l2_lattices(A) ),
inference(clausify,[status(thm)],[dt_l2_lattices]) ).
cnf(c_209,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_212,negated_conjecture,
( m2_lattice4(sK0,sK1)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_125,c_121]) ).
cnf(c_213,negated_conjecture,
( m2_lattice4(sK2,sK1)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_126,c_121]) ).
cnf(c_237,plain,
( ~ v1_xboole_0(u1_struct_0(A))
| v3_struct_0(A)
| ~ l2_lattices(A) ),
inference(resolve,[status(thm)],[c_206,c_204]) ).
cnf(c_261,plain,
( a_3_0_filter_2(A,B,C) = k20_filter_2(A,B,C)
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
| v1_xboole_0(C)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d13_filter_2]) ).
cnf(c_262,plain,
( k20_filter_2(A,B,C) = a_3_0_filter_2(A,B,C)
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
| v1_xboole_0(C)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_261]) ).
cnf(c_270,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_274,plain,
( l3_lattices(k1_lattice2(A))
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_k1_lattice2]) ).
cnf(c_283,plain,
( l2_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_298,plain,
( ~ v3_struct_0(k1_lattice2(A))
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc1_lattice2]) ).
cnf(c_308,plain,
( v10_lattices(k1_lattice2(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc6_lattice2]) ).
cnf(c_347,plain,
r1_tarski(A,A),
inference(clausify,[status(thm)],[reflexivity_r1_tarski]) ).
cnf(c_353,plain,
( ~ r1_tarski(A,B)
| m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[t3_subset]) ).
cnf(c_354,plain,
( k5_filter_0(k1_lattice2(A),k7_filter_2(A,B),k7_filter_2(A,C)) = k20_filter_2(A,B,C)
| ~ m1_subset_1(E,k1_zfmisc_1(u1_struct_0(k1_lattice2(A))))
| v1_xboole_0(E)
| ~ m1_subset_1(D,k1_zfmisc_1(u1_struct_0(k1_lattice2(A))))
| v1_xboole_0(D)
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
| v1_xboole_0(C)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t45_filter_2]) ).
cnf(c_360,plain,
( r1_tarski(B,k5_filter_0(A,B,C))
| ~ m1_filter_0(C,A)
| ~ m1_filter_0(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t49_filter_0]) ).
cnf(c_361,plain,
( r1_tarski(C,k5_filter_0(A,B,C))
| ~ m1_filter_0(C,A)
| ~ m1_filter_0(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[t49_filter_0]) ).
cnf(c_367,negated_conjecture,
~ v3_struct_0(sK1),
inference(split_conjunct,[status(thm)],[sk_t51_filter_2_neg]) ).
cnf(c_368,negated_conjecture,
v10_lattices(sK1),
inference(split_conjunct,[status(thm)],[sk_t51_filter_2_neg]) ).
cnf(c_369,negated_conjecture,
l3_lattices(sK1),
inference(split_conjunct,[status(thm)],[sk_t51_filter_2_neg]) ).
cnf(c_370,negated_conjecture,
( ~ r1_tarski(sK2,k20_filter_2(sK1,sK0,sK2))
| ~ r1_tarski(sK0,k20_filter_2(sK1,sK0,sK2)) ),
inference(split_conjunct,[status(thm)],[sk_t51_filter_2_neg]) ).
cnf(c_375,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_125,c_124]) ).
cnf(c_3731,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_375]) ).
cnf(c_3732,negated_conjecture,
( k7_filter_2(sK1,sK0) = k15_filter_2(sK1,sK0)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_367,c_3731]) ).
cnf(c_3733,negated_conjecture,
( k7_filter_2(sK1,sK0) = k15_filter_2(sK1,sK0)
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_368,c_3732]) ).
cnf(c_376,negated_conjecture,
k7_filter_2(sK1,sK0) = k15_filter_2(sK1,sK0),
inference(resolve,[status(thm)],[c_369,c_3733]) ).
cnf(c_377,negated_conjecture,
( ~ v1_xboole_0(sK0)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_125,c_122]) ).
cnf(c_3734,negated_conjecture,
( ~ v1_xboole_0(sK0)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_367,c_377]) ).
cnf(c_3735,negated_conjecture,
( ~ v1_xboole_0(sK0)
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_368,c_3734]) ).
cnf(c_378,negated_conjecture,
~ v1_xboole_0(sK0),
inference(resolve,[status(thm)],[c_369,c_3735]) ).
cnf(c_379,negated_conjecture,
( k15_filter_2(sK1,sK2) = k7_filter_2(sK1,sK2)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_126,c_124]) ).
cnf(c_3736,negated_conjecture,
( k7_filter_2(sK1,sK2) = k15_filter_2(sK1,sK2)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_379]) ).
cnf(c_3737,negated_conjecture,
( k7_filter_2(sK1,sK2) = k15_filter_2(sK1,sK2)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_367,c_3736]) ).
cnf(c_3738,negated_conjecture,
( k7_filter_2(sK1,sK2) = k15_filter_2(sK1,sK2)
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_368,c_3737]) ).
cnf(c_380,negated_conjecture,
k7_filter_2(sK1,sK2) = k15_filter_2(sK1,sK2),
inference(resolve,[status(thm)],[c_369,c_3738]) ).
cnf(c_381,negated_conjecture,
( ~ v1_xboole_0(sK2)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_126,c_122]) ).
cnf(c_3739,negated_conjecture,
( ~ v1_xboole_0(sK2)
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_367,c_381]) ).
cnf(c_3740,negated_conjecture,
( ~ v1_xboole_0(sK2)
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_368,c_3739]) ).
cnf(c_382,negated_conjecture,
~ v1_xboole_0(sK2),
inference(resolve,[status(thm)],[c_369,c_3740]) ).
cnf(c_450,negated_conjecture,
( 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))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_199,c_196]) ).
cnf(c_3741,negated_conjecture,
( 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))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_367,c_450]) ).
cnf(c_3742,negated_conjecture,
( 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))
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_368,c_3741]) ).
cnf(c_451,negated_conjecture,
( 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_369,c_3742]) ).
cnf(c_454,negated_conjecture,
( m1_filter_0(k15_filter_2(sK1,sK2),k1_lattice2(sK1))
| ~ l3_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) ),
inference(resolve,[status(thm)],[c_200,c_196]) ).
cnf(c_3743,negated_conjecture,
( m1_filter_0(k15_filter_2(sK1,sK2),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_367,c_454]) ).
cnf(c_3744,negated_conjecture,
( m1_filter_0(k15_filter_2(sK1,sK2),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1))
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_368,c_3743]) ).
cnf(c_455,negated_conjecture,
( m1_filter_0(k15_filter_2(sK1,sK2),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| ~ v10_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_369,c_3744]) ).
cnf(c_464,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_212,c_209]) ).
cnf(c_3745,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_464]) ).
cnf(c_3746,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_3745]) ).
cnf(c_3747,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_3746]) ).
cnf(c_3748,negated_conjecture,
( m1_subset_1(sK0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_367,c_3747]) ).
cnf(c_3749,negated_conjecture,
( m1_subset_1(sK0,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_368,c_3748]) ).
cnf(c_465,negated_conjecture,
m1_subset_1(sK0,k1_zfmisc_1(u1_struct_0(sK1))),
inference(resolve,[status(thm)],[c_369,c_3749]) ).
cnf(c_466,negated_conjecture,
( m1_subset_1(sK2,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_213,c_209]) ).
cnf(c_3750,negated_conjecture,
( m1_subset_1(sK2,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_466]) ).
cnf(c_3751,negated_conjecture,
( m1_subset_1(sK2,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_3750]) ).
cnf(c_3752,negated_conjecture,
( m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(copy,[status(thm)],[c_3751]) ).
cnf(c_3753,negated_conjecture,
( m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_367,c_3752]) ).
cnf(c_3754,negated_conjecture,
( m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1)))
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_368,c_3753]) ).
cnf(c_467,negated_conjecture,
m1_subset_1(sK2,k1_zfmisc_1(u1_struct_0(sK1))),
inference(resolve,[status(thm)],[c_369,c_3754]) ).
cnf(c_3755,plain,
( k5_filter_0(k1_lattice2(A),k7_filter_2(A,B),k7_filter_2(A,C)) = k20_filter_2(A,B,C)
| ~ m1_subset_1(D,k1_zfmisc_1(u1_struct_0(k1_lattice2(A))))
| ~ m1_subset_1(D,k1_zfmisc_1(u1_struct_0(k1_lattice2(A))))
| v1_xboole_0(D)
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
| v1_xboole_0(C)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(factor,[status(thm)],[c_354]) ).
cnf(c_524,plain,
( k5_filter_0(k1_lattice2(A),k7_filter_2(A,B),k7_filter_2(A,C)) = k20_filter_2(A,B,C)
| ~ m1_subset_1(D,k1_zfmisc_1(u1_struct_0(k1_lattice2(A))))
| v1_xboole_0(D)
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A)))
| v1_xboole_0(C)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_3755]) ).
cnf(c_945,plain,
m1_subset_1(A,k1_zfmisc_1(A)),
inference(resolve,[status(thm)],[c_353,c_347]) ).
cnf(c_3756,negated_conjecture,
( v10_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_368,c_308]) ).
cnf(c_3757,negated_conjecture,
( v10_lattices(k1_lattice2(sK1))
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_367,c_3756]) ).
cnf(c_1007,negated_conjecture,
v10_lattices(k1_lattice2(sK1)),
inference(resolve,[status(thm)],[c_369,c_3757]) ).
cnf(c_1012,negated_conjecture,
( m1_filter_0(k15_filter_2(sK1,sK2),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_1007,c_455]) ).
cnf(c_1014,negated_conjecture,
( m1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_1007,c_451]) ).
cnf(c_3758,negated_conjecture,
( ~ v3_struct_0(k1_lattice2(sK1))
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_369,c_298]) ).
cnf(c_1015,negated_conjecture,
~ v3_struct_0(k1_lattice2(sK1)),
inference(resolve,[status(thm)],[c_367,c_3758]) ).
cnf(c_1018,plain,
l3_lattices(k1_lattice2(sK1)),
inference(resolve,[status(thm)],[c_369,c_274]) ).
cnf(c_3759,negated_conjecture,
( m1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_1015,c_1014]) ).
cnf(c_1108,negated_conjecture,
m1_filter_0(k15_filter_2(sK1,sK0),k1_lattice2(sK1)),
inference(resolve,[status(thm)],[c_1018,c_3759]) ).
cnf(c_3760,negated_conjecture,
( m1_filter_0(k15_filter_2(sK1,sK2),k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_1015,c_1012]) ).
cnf(c_1110,negated_conjecture,
m1_filter_0(k15_filter_2(sK1,sK2),k1_lattice2(sK1)),
inference(resolve,[status(thm)],[c_1018,c_3760]) ).
cnf(c_3761,negated_conjecture,
( k7_filter_2(sK1,sK0) = sK0
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_465,c_270]) ).
cnf(c_3762,negated_conjecture,
( k15_filter_2(sK1,sK0) = sK0
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(paramod,[status(thm)],[c_376,c_3761]) ).
cnf(c_3763,negated_conjecture,
( k15_filter_2(sK1,sK0) = sK0
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_367,c_3762]) ).
cnf(c_3764,negated_conjecture,
( k15_filter_2(sK1,sK0) = sK0
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_368,c_3763]) ).
cnf(c_1165,negated_conjecture,
k15_filter_2(sK1,sK0) = sK0,
inference(resolve,[status(thm)],[c_369,c_3764]) ).
cnf(c_1283,negated_conjecture,
m1_filter_0(sK0,k1_lattice2(sK1)),
inference(paramod,[status(thm)],[c_1165,c_1108]) ).
cnf(c_1284,negated_conjecture,
k7_filter_2(sK1,sK0) = sK0,
inference(paramod,[status(thm)],[c_1165,c_376]) ).
cnf(c_3765,negated_conjecture,
( k7_filter_2(sK1,sK2) = sK2
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_467,c_270]) ).
cnf(c_3766,negated_conjecture,
( k15_filter_2(sK1,sK2) = sK2
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1)
| v3_struct_0(sK1) ),
inference(paramod,[status(thm)],[c_380,c_3765]) ).
cnf(c_3767,negated_conjecture,
( k15_filter_2(sK1,sK2) = sK2
| ~ l3_lattices(sK1)
| ~ v10_lattices(sK1) ),
inference(resolve,[status(thm)],[c_367,c_3766]) ).
cnf(c_3768,negated_conjecture,
( k15_filter_2(sK1,sK2) = sK2
| ~ l3_lattices(sK1) ),
inference(resolve,[status(thm)],[c_368,c_3767]) ).
cnf(c_1308,negated_conjecture,
k15_filter_2(sK1,sK2) = sK2,
inference(resolve,[status(thm)],[c_369,c_3768]) ).
cnf(c_3769,negated_conjecture,
( k20_filter_2(sK1,A,B) = a_3_0_filter_2(sK1,A,B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| v1_xboole_0(B)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| v1_xboole_0(A)
| ~ l3_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_262,c_368]) ).
cnf(c_3770,negated_conjecture,
( k20_filter_2(sK1,A,B) = a_3_0_filter_2(sK1,A,B)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| v1_xboole_0(B)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| v1_xboole_0(A)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_3769,c_369]) ).
cnf(c_3771,negated_conjecture,
( k20_filter_2(sK1,sK0,A) = a_3_0_filter_2(sK1,sK0,A)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| v1_xboole_0(A)
| v1_xboole_0(sK0)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_3770,c_465]) ).
cnf(c_3772,negated_conjecture,
( k20_filter_2(sK1,sK0,sK2) = a_3_0_filter_2(sK1,sK0,sK2)
| v1_xboole_0(sK2)
| v1_xboole_0(sK0)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_3771,c_467]) ).
cnf(c_3773,negated_conjecture,
( k20_filter_2(sK1,sK0,sK2) = a_3_0_filter_2(sK1,sK0,sK2)
| v1_xboole_0(sK2)
| v1_xboole_0(sK0) ),
inference(resolve,[status(thm)],[c_367,c_3772]) ).
cnf(c_3774,negated_conjecture,
( k20_filter_2(sK1,sK0,sK2) = a_3_0_filter_2(sK1,sK0,sK2)
| v1_xboole_0(sK2) ),
inference(resolve,[status(thm)],[c_378,c_3773]) ).
cnf(c_1468,negated_conjecture,
k20_filter_2(sK1,sK0,sK2) = a_3_0_filter_2(sK1,sK0,sK2),
inference(resolve,[status(thm)],[c_382,c_3774]) ).
cnf(c_1474,negated_conjecture,
m1_filter_0(sK2,k1_lattice2(sK1)),
inference(paramod,[status(thm)],[c_1308,c_1110]) ).
cnf(c_1475,negated_conjecture,
k7_filter_2(sK1,sK2) = sK2,
inference(paramod,[status(thm)],[c_1308,c_380]) ).
cnf(c_3775,negated_conjecture,
( ~ r1_tarski(sK2,k20_filter_2(sK1,sK0,sK2))
| ~ r1_tarski(sK0,a_3_0_filter_2(sK1,sK0,sK2)) ),
inference(paramod,[status(thm)],[c_1468,c_370]) ).
cnf(c_1508,negated_conjecture,
( ~ r1_tarski(sK2,a_3_0_filter_2(sK1,sK0,sK2))
| ~ r1_tarski(sK0,a_3_0_filter_2(sK1,sK0,sK2)) ),
inference(paramod,[status(thm)],[c_1468,c_3775]) ).
cnf(c_2407,plain,
l2_lattices(k1_lattice2(sK1)),
inference(resolve,[status(thm)],[c_1018,c_283]) ).
cnf(c_3776,plain,
( ~ v1_xboole_0(u1_struct_0(k1_lattice2(sK1)))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_2407,c_237]) ).
cnf(c_2627,plain,
~ v1_xboole_0(u1_struct_0(k1_lattice2(sK1))),
inference(resolve,[status(thm)],[c_1015,c_3776]) ).
cnf(c_3777,negated_conjecture,
( k5_filter_0(k1_lattice2(sK1),k7_filter_2(sK1,A),k7_filter_2(sK1,B)) = k20_filter_2(sK1,A,B)
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK1))))
| v1_xboole_0(C)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| v1_xboole_0(B)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| v1_xboole_0(A)
| ~ l3_lattices(sK1)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_524,c_368]) ).
cnf(c_3778,negated_conjecture,
( k5_filter_0(k1_lattice2(sK1),k7_filter_2(sK1,A),k7_filter_2(sK1,B)) = k20_filter_2(sK1,A,B)
| ~ m1_subset_1(C,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK1))))
| v1_xboole_0(C)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(sK1)))
| v1_xboole_0(B)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| v1_xboole_0(A)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_3777,c_369]) ).
cnf(c_3779,negated_conjecture,
( k5_filter_0(k1_lattice2(sK1),k7_filter_2(sK1,sK0),k7_filter_2(sK1,A)) = k20_filter_2(sK1,sK0,A)
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK1))))
| v1_xboole_0(B)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(sK1)))
| v1_xboole_0(A)
| v1_xboole_0(sK0)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_3778,c_465]) ).
cnf(c_3780,negated_conjecture,
( k5_filter_0(k1_lattice2(sK1),k7_filter_2(sK1,sK0),k7_filter_2(sK1,sK2)) = k20_filter_2(sK1,sK0,sK2)
| ~ m1_subset_1(A,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK1))))
| v1_xboole_0(A)
| v1_xboole_0(sK2)
| v1_xboole_0(sK0)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_3779,c_467]) ).
cnf(c_3781,negated_conjecture,
( k5_filter_0(k1_lattice2(sK1),k7_filter_2(sK1,sK0),k7_filter_2(sK1,sK2)) = k20_filter_2(sK1,sK0,sK2)
| v1_xboole_0(u1_struct_0(k1_lattice2(sK1)))
| v1_xboole_0(sK2)
| v1_xboole_0(sK0)
| v3_struct_0(sK1) ),
inference(resolve,[status(thm)],[c_3780,c_945]) ).
cnf(c_3782,negated_conjecture,
( k5_filter_0(k1_lattice2(sK1),sK0,k7_filter_2(sK1,sK2)) = k20_filter_2(sK1,sK0,sK2)
| v1_xboole_0(u1_struct_0(k1_lattice2(sK1)))
| v1_xboole_0(sK2)
| v1_xboole_0(sK0)
| v3_struct_0(sK1) ),
inference(paramod,[status(thm)],[c_1284,c_3781]) ).
cnf(c_3783,negated_conjecture,
( k5_filter_0(k1_lattice2(sK1),sK0,sK2) = k20_filter_2(sK1,sK0,sK2)
| v1_xboole_0(u1_struct_0(k1_lattice2(sK1)))
| v1_xboole_0(sK2)
| v1_xboole_0(sK0)
| v3_struct_0(sK1) ),
inference(paramod,[status(thm)],[c_1475,c_3782]) ).
cnf(c_3784,negated_conjecture,
( k5_filter_0(k1_lattice2(sK1),sK0,sK2) = a_3_0_filter_2(sK1,sK0,sK2)
| v1_xboole_0(u1_struct_0(k1_lattice2(sK1)))
| v1_xboole_0(sK2)
| v1_xboole_0(sK0)
| v3_struct_0(sK1) ),
inference(paramod,[status(thm)],[c_1468,c_3783]) ).
cnf(c_3785,negated_conjecture,
( k5_filter_0(k1_lattice2(sK1),sK0,sK2) = a_3_0_filter_2(sK1,sK0,sK2)
| v1_xboole_0(u1_struct_0(k1_lattice2(sK1)))
| v1_xboole_0(sK2)
| v1_xboole_0(sK0) ),
inference(resolve,[status(thm)],[c_367,c_3784]) ).
cnf(c_3786,negated_conjecture,
( k5_filter_0(k1_lattice2(sK1),sK0,sK2) = a_3_0_filter_2(sK1,sK0,sK2)
| v1_xboole_0(u1_struct_0(k1_lattice2(sK1)))
| v1_xboole_0(sK2) ),
inference(resolve,[status(thm)],[c_378,c_3785]) ).
cnf(c_3787,negated_conjecture,
( k5_filter_0(k1_lattice2(sK1),sK0,sK2) = a_3_0_filter_2(sK1,sK0,sK2)
| v1_xboole_0(u1_struct_0(k1_lattice2(sK1))) ),
inference(resolve,[status(thm)],[c_382,c_3786]) ).
cnf(c_2933,negated_conjecture,
k5_filter_0(k1_lattice2(sK1),sK0,sK2) = a_3_0_filter_2(sK1,sK0,sK2),
inference(resolve,[status(thm)],[c_2627,c_3787]) ).
cnf(c_3788,plain,
( r1_tarski(B,k5_filter_0(k1_lattice2(sK1),A,B))
| ~ m1_filter_0(B,k1_lattice2(sK1))
| ~ m1_filter_0(A,k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_361,c_1007]) ).
cnf(c_3789,plain,
( r1_tarski(B,k5_filter_0(k1_lattice2(sK1),A,B))
| ~ m1_filter_0(B,k1_lattice2(sK1))
| ~ m1_filter_0(A,k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_3788,c_1018]) ).
cnf(c_3790,negated_conjecture,
( r1_tarski(A,k5_filter_0(k1_lattice2(sK1),sK0,A))
| ~ m1_filter_0(A,k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_3789,c_1283]) ).
cnf(c_3791,negated_conjecture,
( r1_tarski(sK2,k5_filter_0(k1_lattice2(sK1),sK0,sK2))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_3790,c_1474]) ).
cnf(c_3792,negated_conjecture,
( r1_tarski(sK2,a_3_0_filter_2(sK1,sK0,sK2))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(paramod,[status(thm)],[c_2933,c_3791]) ).
cnf(c_3726,negated_conjecture,
r1_tarski(sK2,a_3_0_filter_2(sK1,sK0,sK2)),
inference(resolve,[status(thm)],[c_1015,c_3792]) ).
cnf(c_3793,plain,
( r1_tarski(A,k5_filter_0(k1_lattice2(sK1),A,B))
| ~ m1_filter_0(B,k1_lattice2(sK1))
| ~ m1_filter_0(A,k1_lattice2(sK1))
| ~ l3_lattices(k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_360,c_1007]) ).
cnf(c_3794,plain,
( r1_tarski(A,k5_filter_0(k1_lattice2(sK1),A,B))
| ~ m1_filter_0(B,k1_lattice2(sK1))
| ~ m1_filter_0(A,k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_3793,c_1018]) ).
cnf(c_3795,negated_conjecture,
( r1_tarski(sK0,k5_filter_0(k1_lattice2(sK1),sK0,A))
| ~ m1_filter_0(A,k1_lattice2(sK1))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_3794,c_1283]) ).
cnf(c_3796,negated_conjecture,
( r1_tarski(sK0,k5_filter_0(k1_lattice2(sK1),sK0,sK2))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(resolve,[status(thm)],[c_3795,c_1474]) ).
cnf(c_3797,negated_conjecture,
( r1_tarski(sK0,a_3_0_filter_2(sK1,sK0,sK2))
| v3_struct_0(k1_lattice2(sK1)) ),
inference(paramod,[status(thm)],[c_2933,c_3796]) ).
cnf(c_3728,negated_conjecture,
r1_tarski(sK0,a_3_0_filter_2(sK1,sK0,sK2)),
inference(resolve,[status(thm)],[c_1015,c_3797]) ).
cnf(c_3798,negated_conjecture,
~ r1_tarski(sK2,a_3_0_filter_2(sK1,sK0,sK2)),
inference(resolve,[status(thm)],[c_3728,c_1508]) ).
cnf(c_3730,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_3726,c_3798]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT317+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n012.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Fri Sep 25 20:47:50 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.34 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.34 % Process 2971711 was started by sandbox2 on n012,
% 0.08/0.34 % Fri Sep 25 20:47:50 2026
% 0.08/0.34 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.08/0.36
% 0.08/0.36 % From the command line: assign(max_seconds, 300).
% 4.28/1.00
% 4.28/1.00 % SZS status Theorem for theBenchmark
% 4.28/1.00
% 4.28/1.00 % Proof 1 at 0.54 (+ 0.08) seconds.
% 4.28/1.00 % Length of proof is 88.
% 4.28/1.00 % Level of proof is 9.
% 4.28/1.00 % Maximum clause weight is 70.000.
% 4.28/1.00 % Given clauses 329.
% 4.28/1.00
% 4.28/1.00 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------