%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT332+1 : 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 : n019.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:16 AM UTC 2026
% Result : Theorem 221.54s 28.69s
% Output : CNFRefutation 221.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 22
% Syntax : Number of formulae : 163 ( 40 unt; 0 def)
% Number of atoms : 725 ( 166 equ)
% Maximal formula atoms : 88 ( 4 avg)
% Number of connectives : 920 ( 358 ~; 443 |; 90 &)
% ( 3 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 31 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 27 ( 25 usr; 1 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 1 con; 0-3 aty)
% Number of variables : 197 ( 0 sgn 78 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cc1_lattices,axiom,
! [A] :
( l3_lattices(A)
=> ( ( v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A) ) ) ),
file('theBenchmark.p',cc1_lattices) ).
fof(d16_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m2_lattice4(B,A)
& ~ v1_xboole_0(B) )
=> ! [C] :
( m2_nat_lat(C,A)
=> ( C = k23_filter_2(A,B)
<=> ? [D] :
( ? [E] :
( C = g3_lattices(B,D,E)
& E = k1_realset1(u1_lattices(A),B)
& D = k1_realset1(u2_lattices(A),B)
& m2_relset_1(E,k2_zfmisc_1(B,B),B)
& v1_funct_2(E,k2_zfmisc_1(B,B),B)
& v1_funct_1(E) )
& m2_relset_1(D,k2_zfmisc_1(B,B),B)
& v1_funct_2(D,k2_zfmisc_1(B,B),B)
& v1_funct_1(D) ) ) ) ) ),
file('theBenchmark.p',d16_filter_2) ).
fof(d2_filter_0,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k1_filter_0(A) = u1_struct_0(A) ),
file('theBenchmark.p',d2_filter_0) ).
fof(d3_realset1,axiom,
! [A] :
( v1_relat_1(A)
=> ! [B] : k1_realset1(A,B) = k7_relat_1(A,k2_zfmisc_1(B,B)) ),
file('theBenchmark.p',d3_realset1) ).
fof(d8_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k17_filter_2(A) = u1_struct_0(A) ),
file('theBenchmark.p',d8_filter_2) ).
fof(dt_k17_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m2_filter_2(k17_filter_2(A),A) ),
file('theBenchmark.p',dt_k17_filter_2) ).
fof(dt_k23_filter_2,axiom,
! [A,B] :
( ( m2_lattice4(B,A)
& ~ v1_xboole_0(B)
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m2_nat_lat(k23_filter_2(A,B),A) ),
file('theBenchmark.p',dt_k23_filter_2) ).
fof(dt_k4_relset_1,axiom,
! [A,B,C] :
( m1_relset_1(C,A,B)
=> m1_subset_1(k4_relset_1(A,B,C),k1_zfmisc_1(A)) ),
file('theBenchmark.p',dt_k4_relset_1) ).
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_u1_lattices,axiom,
! [A] :
( l1_lattices(A)
=> ( m2_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_1(u1_lattices(A)) ) ),
file('theBenchmark.p',dt_u1_lattices) ).
fof(dt_u2_lattices,axiom,
! [A] :
( l2_lattices(A)
=> ( m2_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_1(u2_lattices(A)) ) ),
file('theBenchmark.p',dt_u2_lattices) ).
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(fc3_lattice2,axiom,
! [A] :
( ( l2_lattices(A)
& v5_lattices(A)
& ~ v3_struct_0(A) )
=> ( v1_partfun1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v2_binop_1(u2_lattices(A),u1_struct_0(A))
& v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_1(u2_lattices(A))
& v1_relat_1(u2_lattices(A)) ) ),
file('theBenchmark.p',fc3_lattice2) ).
fof(fc5_lattice2,axiom,
! [A] :
( ( l1_lattices(A)
& v7_lattices(A)
& ~ v3_struct_0(A) )
=> ( v1_partfun1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v2_binop_1(u1_lattices(A),u1_struct_0(A))
& v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_1(u1_lattices(A))
& v1_relat_1(u1_lattices(A)) ) ),
file('theBenchmark.p',fc5_lattice2) ).
fof(redefinition_k1_filter_2,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k1_filter_2(A) = k1_filter_0(A) ),
file('theBenchmark.p',redefinition_k1_filter_2) ).
fof(redefinition_k4_relset_1,axiom,
! [A,B,C] :
( m1_relset_1(C,A,B)
=> k4_relset_1(A,B,C) = k1_relat_1(C) ),
file('theBenchmark.p',redefinition_k4_relset_1) ).
fof(redefinition_m2_relset_1,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('theBenchmark.p',redefinition_m2_relset_1) ).
fof(t3_subset,axiom,
! [A,B] :
( m1_subset_1(A,k1_zfmisc_1(B))
<=> r1_tarski(A,B) ),
file('theBenchmark.p',t3_subset) ).
fof(t97_relat_1,axiom,
! [A,B] :
( v1_relat_1(B)
=> ( r1_tarski(k1_relat_1(B),A)
=> k7_relat_1(B,A) = B ) ),
file('theBenchmark.p',t97_relat_1) ).
fof(t72_filter_2,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( k23_filter_2(A,k1_filter_2(A)) = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A))
& k23_filter_2(A,k17_filter_2(A)) = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) ) ),
file('theBenchmark.p',t72_filter_2) ).
fof(t72_filter_2_neg,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( k23_filter_2(A,k1_filter_2(A)) = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A))
& k23_filter_2(A,k17_filter_2(A)) = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) ) ),
inference(assume_negation,[status(cth)],[t72_filter_2]) ).
cnf(c_128,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_130,plain,
( m2_nat_lat(k23_filter_2(A,B),A)
| ~ m2_lattice4(B,A)
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k23_filter_2]) ).
fof(nnf_8,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ! [D] :
( ! [E] :
( g3_lattices(B,D,E) != C
| k1_realset1(u1_lattices(A),B) != E
| k1_realset1(u2_lattices(A),B) != D
| ~ m2_relset_1(E,k2_zfmisc_1(B,B),B)
| ~ v1_funct_2(E,k2_zfmisc_1(B,B),B)
| ~ v1_funct_1(E) )
| ~ m2_relset_1(D,k2_zfmisc_1(B,B),B)
| ~ v1_funct_2(D,k2_zfmisc_1(B,B),B)
| ~ v1_funct_1(D) )
| k23_filter_2(A,B) = C )
& ( ? [X0] :
( ? [X1] :
( g3_lattices(B,X0,X1) = C
& k1_realset1(u1_lattices(A),B) = X1
& k1_realset1(u2_lattices(A),B) = X0
& m2_relset_1(X1,k2_zfmisc_1(B,B),B)
& v1_funct_2(X1,k2_zfmisc_1(B,B),B)
& v1_funct_1(X1) )
& m2_relset_1(X0,k2_zfmisc_1(B,B),B)
& v1_funct_2(X0,k2_zfmisc_1(B,B),B)
& v1_funct_1(X0) )
| k23_filter_2(A,B) != C ) )
| ~ m2_nat_lat(C,A) )
| ~ m2_lattice4(B,A)
| v1_xboole_0(B) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[d16_filter_2]) ).
fof(sk_d16_filter_2_sk,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ! [D] :
( ! [E] :
( g3_lattices(B,D,E) != C
| k1_realset1(u1_lattices(A),B) != E
| k1_realset1(u2_lattices(A),B) != D
| ~ m2_relset_1(E,k2_zfmisc_1(B,B),B)
| ~ v1_funct_2(E,k2_zfmisc_1(B,B),B)
| ~ v1_funct_1(E) )
| ~ m2_relset_1(D,k2_zfmisc_1(B,B),B)
| ~ v1_funct_2(D,k2_zfmisc_1(B,B),B)
| ~ v1_funct_1(D) )
| k23_filter_2(A,B) = C )
& ( ( g3_lattices(B,sK0(A,B,C),sK1(A,B,C)) = C
& k1_realset1(u1_lattices(A),B) = sK1(A,B,C)
& k1_realset1(u2_lattices(A),B) = sK0(A,B,C)
& m2_relset_1(sK1(A,B,C),k2_zfmisc_1(B,B),B)
& v1_funct_2(sK1(A,B,C),k2_zfmisc_1(B,B),B)
& v1_funct_1(sK1(A,B,C))
& m2_relset_1(sK0(A,B,C),k2_zfmisc_1(B,B),B)
& v1_funct_2(sK0(A,B,C),k2_zfmisc_1(B,B),B)
& v1_funct_1(sK0(A,B,C)) )
| k23_filter_2(A,B) != C ) )
| ~ m2_nat_lat(C,A) )
| ~ m2_lattice4(B,A)
| v1_xboole_0(B) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0(A,B,C)),skolemize(X1,sK1(A,B,C))],[nnf_8]) ).
fof(sk_d16_filter_2,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( g3_lattices(VAR_1,VAR_3,VAR_4) != VAR_2
| k1_realset1(u1_lattices(VAR_0),VAR_1) != VAR_4
| k1_realset1(u2_lattices(VAR_0),VAR_1) != VAR_3
| ~ m2_relset_1(VAR_4,k2_zfmisc_1(VAR_1,VAR_1),VAR_1)
| ~ v1_funct_2(VAR_4,k2_zfmisc_1(VAR_1,VAR_1),VAR_1)
| ~ v1_funct_1(VAR_4)
| ~ m2_relset_1(VAR_3,k2_zfmisc_1(VAR_1,VAR_1),VAR_1)
| ~ v1_funct_2(VAR_3,k2_zfmisc_1(VAR_1,VAR_1),VAR_1)
| ~ v1_funct_1(VAR_3)
| k23_filter_2(VAR_0,VAR_1) = VAR_2
| ~ m2_nat_lat(VAR_2,VAR_0)
| ~ m2_lattice4(VAR_1,VAR_0)
| v1_xboole_0(VAR_1)
| ~ l3_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( g3_lattices(VAR_1,sK0(VAR_0,VAR_1,VAR_2),sK1(VAR_0,VAR_1,VAR_2)) = VAR_2
| k23_filter_2(VAR_0,VAR_1) != VAR_2
| ~ m2_nat_lat(VAR_2,VAR_0)
| ~ m2_lattice4(VAR_1,VAR_0)
| v1_xboole_0(VAR_1)
| ~ l3_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( k1_realset1(u1_lattices(VAR_0),VAR_1) = sK1(VAR_0,VAR_1,VAR_2)
| k23_filter_2(VAR_0,VAR_1) != VAR_2
| ~ m2_nat_lat(VAR_2,VAR_0)
| ~ m2_lattice4(VAR_1,VAR_0)
| v1_xboole_0(VAR_1)
| ~ l3_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( k1_realset1(u2_lattices(VAR_0),VAR_1) = sK0(VAR_0,VAR_1,VAR_2)
| k23_filter_2(VAR_0,VAR_1) != VAR_2
| ~ m2_nat_lat(VAR_2,VAR_0)
| ~ m2_lattice4(VAR_1,VAR_0)
| v1_xboole_0(VAR_1)
| ~ l3_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( m2_relset_1(sK1(VAR_0,VAR_1,VAR_2),k2_zfmisc_1(VAR_1,VAR_1),VAR_1)
| k23_filter_2(VAR_0,VAR_1) != VAR_2
| ~ m2_nat_lat(VAR_2,VAR_0)
| ~ m2_lattice4(VAR_1,VAR_0)
| v1_xboole_0(VAR_1)
| ~ l3_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( v1_funct_2(sK1(VAR_0,VAR_1,VAR_2),k2_zfmisc_1(VAR_1,VAR_1),VAR_1)
| k23_filter_2(VAR_0,VAR_1) != VAR_2
| ~ m2_nat_lat(VAR_2,VAR_0)
| ~ m2_lattice4(VAR_1,VAR_0)
| v1_xboole_0(VAR_1)
| ~ l3_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( v1_funct_1(sK1(VAR_0,VAR_1,VAR_2))
| k23_filter_2(VAR_0,VAR_1) != VAR_2
| ~ m2_nat_lat(VAR_2,VAR_0)
| ~ m2_lattice4(VAR_1,VAR_0)
| v1_xboole_0(VAR_1)
| ~ l3_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( m2_relset_1(sK0(VAR_0,VAR_1,VAR_2),k2_zfmisc_1(VAR_1,VAR_1),VAR_1)
| k23_filter_2(VAR_0,VAR_1) != VAR_2
| ~ m2_nat_lat(VAR_2,VAR_0)
| ~ m2_lattice4(VAR_1,VAR_0)
| v1_xboole_0(VAR_1)
| ~ l3_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( v1_funct_2(sK0(VAR_0,VAR_1,VAR_2),k2_zfmisc_1(VAR_1,VAR_1),VAR_1)
| k23_filter_2(VAR_0,VAR_1) != VAR_2
| ~ m2_nat_lat(VAR_2,VAR_0)
| ~ m2_lattice4(VAR_1,VAR_0)
| v1_xboole_0(VAR_1)
| ~ l3_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( v1_funct_1(sK0(VAR_0,VAR_1,VAR_2))
| k23_filter_2(VAR_0,VAR_1) != VAR_2
| ~ m2_nat_lat(VAR_2,VAR_0)
| ~ m2_lattice4(VAR_1,VAR_0)
| v1_xboole_0(VAR_1)
| ~ l3_lattices(VAR_0)
| ~ v10_lattices(VAR_0)
| v3_struct_0(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_d16_filter_2_sk]) ).
cnf(c_132,plain,
( g3_lattices(B,sK0(A,B,C),sK1(A,B,C)) = C
| k23_filter_2(A,B) != C
| ~ m2_nat_lat(C,A)
| ~ m2_lattice4(B,A)
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(split_conjunct,[status(thm)],[sk_d16_filter_2]) ).
cnf(c_133,plain,
( k1_realset1(u1_lattices(A),B) = sK1(A,B,C)
| k23_filter_2(A,B) != C
| ~ m2_nat_lat(C,A)
| ~ m2_lattice4(B,A)
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(split_conjunct,[status(thm)],[sk_d16_filter_2]) ).
cnf(c_134,plain,
( k1_realset1(u2_lattices(A),B) = sK0(A,B,C)
| k23_filter_2(A,B) != C
| ~ m2_nat_lat(C,A)
| ~ m2_lattice4(B,A)
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(split_conjunct,[status(thm)],[sk_d16_filter_2]) ).
cnf(c_151,plain,
( ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| g3_lattices(B,sK0(A,B,C),sK1(A,B,C)) = C
| k23_filter_2(A,B) != C
| ~ m2_nat_lat(C,A)
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_132,c_128]) ).
cnf(c_155,plain,
( ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| k1_realset1(u1_lattices(A),B) = sK1(A,B,C)
| k23_filter_2(A,B) != C
| ~ m2_nat_lat(C,A)
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_133,c_128]) ).
cnf(c_159,plain,
( ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| k1_realset1(u2_lattices(A),B) = sK0(A,B,C)
| k23_filter_2(A,B) != C
| ~ m2_nat_lat(C,A)
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_134,c_128]) ).
cnf(c_30377,plain,
( ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| g3_lattices(B,sK0(A,B,C),sK1(A,B,C)) = C
| k23_filter_2(A,B) != C
| ~ m2_nat_lat(C,A)
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_151]) ).
cnf(c_30378,plain,
( ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| g3_lattices(B,sK0(A,B,C),sK1(A,B,C)) = C
| k23_filter_2(A,B) != C
| ~ m2_nat_lat(C,A)
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_30377]) ).
cnf(c_192,plain,
( ~ m2_filter_2(B,A)
| g3_lattices(B,sK0(A,B,C),sK1(A,B,C)) = C
| k23_filter_2(A,B) != C
| ~ m2_nat_lat(C,A)
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_30378]) ).
cnf(c_30379,plain,
( ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| sK1(A,B,C) = k1_realset1(u1_lattices(A),B)
| k23_filter_2(A,B) != C
| ~ m2_nat_lat(C,A)
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_155]) ).
cnf(c_30380,plain,
( ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| sK1(A,B,C) = k1_realset1(u1_lattices(A),B)
| k23_filter_2(A,B) != C
| ~ m2_nat_lat(C,A)
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_30379]) ).
cnf(c_30381,plain,
( ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| sK1(A,B,C) = k1_realset1(u1_lattices(A),B)
| k23_filter_2(A,B) != C
| ~ m2_nat_lat(C,A)
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_30380]) ).
cnf(c_196,plain,
( ~ m2_filter_2(B,A)
| sK1(A,B,C) = k1_realset1(u1_lattices(A),B)
| k23_filter_2(A,B) != C
| ~ m2_nat_lat(C,A)
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_30381]) ).
cnf(c_30382,plain,
( ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| sK0(A,B,C) = k1_realset1(u2_lattices(A),B)
| k23_filter_2(A,B) != C
| ~ m2_nat_lat(C,A)
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_159]) ).
cnf(c_30383,plain,
( ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| sK0(A,B,C) = k1_realset1(u2_lattices(A),B)
| k23_filter_2(A,B) != C
| ~ m2_nat_lat(C,A)
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_30382]) ).
cnf(c_30384,plain,
( ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| sK0(A,B,C) = k1_realset1(u2_lattices(A),B)
| k23_filter_2(A,B) != C
| ~ m2_nat_lat(C,A)
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_30383]) ).
cnf(c_200,plain,
( ~ m2_filter_2(B,A)
| sK0(A,B,C) = k1_realset1(u2_lattices(A),B)
| k23_filter_2(A,B) != C
| ~ m2_nat_lat(C,A)
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_30384]) ).
cnf(c_253,plain,
( ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| m2_nat_lat(k23_filter_2(A,B),A)
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(resolve,[status(thm)],[c_130,c_128]) ).
cnf(c_30385,plain,
( ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| m2_nat_lat(k23_filter_2(A,B),A)
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_253]) ).
cnf(c_30386,plain,
( ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| m2_nat_lat(k23_filter_2(A,B),A)
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_30385]) ).
cnf(c_254,plain,
( ~ m2_filter_2(B,A)
| m2_nat_lat(k23_filter_2(A,B),A)
| v1_xboole_0(B)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_30386]) ).
cnf(c_349,plain,
( v5_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc1_lattices]) ).
cnf(c_351,plain,
( v7_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[cc1_lattices]) ).
cnf(c_361,plain,
( k1_filter_0(A) = u1_struct_0(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d2_filter_0]) ).
cnf(c_362,plain,
( k7_relat_1(A,k2_zfmisc_1(B,B)) = k1_realset1(A,B)
| ~ v1_relat_1(A) ),
inference(clausify,[status(thm)],[d3_realset1]) ).
cnf(c_363,plain,
( u1_struct_0(A) = k17_filter_2(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[d8_filter_2]) ).
cnf(c_364,plain,
( k17_filter_2(A) = u1_struct_0(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_363]) ).
cnf(c_366,plain,
( m2_filter_2(k17_filter_2(A),A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[dt_k17_filter_2]) ).
cnf(c_369,plain,
( m1_subset_1(k4_relset_1(B,C,A),k1_zfmisc_1(B))
| ~ m1_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[dt_k4_relset_1]) ).
cnf(c_373,plain,
( l1_struct_0(A)
| ~ l2_lattices(A) ),
inference(clausify,[status(thm)],[dt_l2_lattices]) ).
cnf(c_374,plain,
( l1_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_375,plain,
( l2_lattices(A)
| ~ l3_lattices(A) ),
inference(clausify,[status(thm)],[dt_l3_lattices]) ).
cnf(c_386,plain,
( m2_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
| ~ l1_lattices(A) ),
inference(clausify,[status(thm)],[dt_u1_lattices]) ).
cnf(c_389,plain,
( m2_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
| ~ l2_lattices(A) ),
inference(clausify,[status(thm)],[dt_u2_lattices]) ).
cnf(c_402,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_406,plain,
( v1_relat_1(u2_lattices(A))
| ~ l2_lattices(A)
| ~ v5_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc3_lattice2]) ).
cnf(c_415,plain,
( v1_relat_1(u1_lattices(A))
| ~ l1_lattices(A)
| ~ v7_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[fc5_lattice2]) ).
cnf(c_458,plain,
( k1_filter_0(A) = k1_filter_2(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(clausify,[status(thm)],[redefinition_k1_filter_2]) ).
cnf(c_459,plain,
( k1_filter_2(A) = k1_filter_0(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(copy,[status(thm)],[c_458]) ).
cnf(c_460,plain,
( k1_relat_1(A) = k4_relset_1(B,C,A)
| ~ m1_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_k4_relset_1]) ).
cnf(c_461,plain,
( k4_relset_1(B,C,A) = k1_relat_1(A)
| ~ m1_relset_1(A,B,C) ),
inference(copy,[status(thm)],[c_460]) ).
cnf(c_465,plain,
( m1_relset_1(A,B,C)
| ~ m2_relset_1(A,B,C) ),
inference(clausify,[status(thm)],[redefinition_m2_relset_1]) ).
cnf(c_474,plain,
( r1_tarski(A,B)
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ),
inference(clausify,[status(thm)],[t3_subset]) ).
cnf(c_481,plain,
( k7_relat_1(A,B) = A
| ~ r1_tarski(k1_relat_1(A),B)
| ~ v1_relat_1(A) ),
inference(clausify,[status(thm)],[t97_relat_1]) ).
fof(nnf_98,plain,
? [A] :
( ( g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) != k23_filter_2(A,k1_filter_2(A))
| g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) != k23_filter_2(A,k17_filter_2(A)) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(fof_nnf,[status(thm)],[t72_filter_2_neg]) ).
fof(sk_t72_filter_2_neg,plain,
( ( g3_lattices(u1_struct_0(sK2),u2_lattices(sK2),u1_lattices(sK2)) != k23_filter_2(sK2,k1_filter_2(sK2))
| g3_lattices(u1_struct_0(sK2),u2_lattices(sK2),u1_lattices(sK2)) != k23_filter_2(sK2,k17_filter_2(sK2)) )
& l3_lattices(sK2)
& v10_lattices(sK2)
& ~ v3_struct_0(sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(A,sK2)],[nnf_98]) ).
cnf(c_482,negated_conjecture,
~ v3_struct_0(sK2),
inference(split_conjunct,[status(thm)],[sk_t72_filter_2_neg]) ).
cnf(c_483,negated_conjecture,
v10_lattices(sK2),
inference(split_conjunct,[status(thm)],[sk_t72_filter_2_neg]) ).
cnf(c_484,negated_conjecture,
l3_lattices(sK2),
inference(split_conjunct,[status(thm)],[sk_t72_filter_2_neg]) ).
cnf(c_485,negated_conjecture,
( g3_lattices(u1_struct_0(sK2),u2_lattices(sK2),u1_lattices(sK2)) != k23_filter_2(sK2,k1_filter_2(sK2))
| g3_lattices(u1_struct_0(sK2),u2_lattices(sK2),u1_lattices(sK2)) != k23_filter_2(sK2,k17_filter_2(sK2)) ),
inference(split_conjunct,[status(thm)],[sk_t72_filter_2_neg]) ).
cnf(c_30387,negated_conjecture,
( k1_filter_2(sK2) = k1_filter_0(sK2)
| ~ l3_lattices(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_483,c_459]) ).
cnf(c_30388,negated_conjecture,
( k1_filter_2(sK2) = k1_filter_0(sK2)
| ~ l3_lattices(sK2) ),
inference(resolve,[status(thm)],[c_482,c_30387]) ).
cnf(c_758,negated_conjecture,
k1_filter_2(sK2) = k1_filter_0(sK2),
inference(resolve,[status(thm)],[c_484,c_30388]) ).
cnf(c_30389,negated_conjecture,
( m2_filter_2(k17_filter_2(sK2),sK2)
| ~ l3_lattices(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_483,c_366]) ).
cnf(c_30390,negated_conjecture,
( m2_filter_2(k17_filter_2(sK2),sK2)
| ~ l3_lattices(sK2) ),
inference(resolve,[status(thm)],[c_482,c_30389]) ).
cnf(c_773,negated_conjecture,
m2_filter_2(k17_filter_2(sK2),sK2),
inference(resolve,[status(thm)],[c_484,c_30390]) ).
cnf(c_30391,negated_conjecture,
( k17_filter_2(sK2) = u1_struct_0(sK2)
| ~ l3_lattices(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_483,c_364]) ).
cnf(c_30392,negated_conjecture,
( k17_filter_2(sK2) = u1_struct_0(sK2)
| ~ l3_lattices(sK2) ),
inference(resolve,[status(thm)],[c_482,c_30391]) ).
cnf(c_774,negated_conjecture,
k17_filter_2(sK2) = u1_struct_0(sK2),
inference(resolve,[status(thm)],[c_484,c_30392]) ).
cnf(c_30393,negated_conjecture,
( k1_filter_0(sK2) = u1_struct_0(sK2)
| ~ l3_lattices(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_483,c_361]) ).
cnf(c_30394,negated_conjecture,
( k1_filter_0(sK2) = u1_struct_0(sK2)
| ~ l3_lattices(sK2) ),
inference(resolve,[status(thm)],[c_482,c_30393]) ).
cnf(c_775,negated_conjecture,
k1_filter_0(sK2) = u1_struct_0(sK2),
inference(resolve,[status(thm)],[c_484,c_30394]) ).
cnf(c_30395,negated_conjecture,
( v7_lattices(sK2)
| v3_struct_0(sK2)
| ~ l3_lattices(sK2) ),
inference(resolve,[status(thm)],[c_483,c_351]) ).
cnf(c_30396,negated_conjecture,
( v7_lattices(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_484,c_30395]) ).
cnf(c_778,negated_conjecture,
v7_lattices(sK2),
inference(resolve,[status(thm)],[c_482,c_30396]) ).
cnf(c_30397,negated_conjecture,
( v5_lattices(sK2)
| v3_struct_0(sK2)
| ~ l3_lattices(sK2) ),
inference(resolve,[status(thm)],[c_483,c_349]) ).
cnf(c_30398,negated_conjecture,
( v5_lattices(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_484,c_30397]) ).
cnf(c_780,negated_conjecture,
v5_lattices(sK2),
inference(resolve,[status(thm)],[c_482,c_30398]) ).
cnf(c_30399,negated_conjecture,
( g3_lattices(u1_struct_0(sK2),u2_lattices(sK2),u1_lattices(sK2)) != k23_filter_2(sK2,k1_filter_2(sK2))
| g3_lattices(u1_struct_0(sK2),u2_lattices(sK2),u1_lattices(sK2)) != k23_filter_2(sK2,u1_struct_0(sK2)) ),
inference(paramod,[status(thm)],[c_774,c_485]) ).
cnf(c_30400,negated_conjecture,
( g3_lattices(u1_struct_0(sK2),u2_lattices(sK2),u1_lattices(sK2)) != k23_filter_2(sK2,k1_filter_0(sK2))
| g3_lattices(u1_struct_0(sK2),u2_lattices(sK2),u1_lattices(sK2)) != k23_filter_2(sK2,u1_struct_0(sK2)) ),
inference(paramod,[status(thm)],[c_758,c_30399]) ).
cnf(c_30401,negated_conjecture,
( g3_lattices(u1_struct_0(sK2),u2_lattices(sK2),u1_lattices(sK2)) != k23_filter_2(sK2,u1_struct_0(sK2))
| g3_lattices(u1_struct_0(sK2),u2_lattices(sK2),u1_lattices(sK2)) != k23_filter_2(sK2,u1_struct_0(sK2)) ),
inference(paramod,[status(thm)],[c_775,c_30400]) ).
cnf(c_801,negated_conjecture,
g3_lattices(u1_struct_0(sK2),u2_lattices(sK2),u1_lattices(sK2)) != k23_filter_2(sK2,u1_struct_0(sK2)),
inference(copy,[status(thm)],[c_30401]) ).
cnf(c_802,negated_conjecture,
m2_filter_2(u1_struct_0(sK2),sK2),
inference(paramod,[status(thm)],[c_774,c_773]) ).
cnf(c_806,plain,
l2_lattices(sK2),
inference(resolve,[status(thm)],[c_484,c_375]) ).
cnf(c_807,plain,
l1_lattices(sK2),
inference(resolve,[status(thm)],[c_484,c_374]) ).
cnf(c_30402,plain,
( v1_relat_1(u1_lattices(sK2))
| ~ l1_lattices(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_778,c_415]) ).
cnf(c_30403,negated_conjecture,
( v1_relat_1(u1_lattices(sK2))
| ~ l1_lattices(sK2) ),
inference(resolve,[status(thm)],[c_482,c_30402]) ).
cnf(c_937,negated_conjecture,
v1_relat_1(u1_lattices(sK2)),
inference(resolve,[status(thm)],[c_807,c_30403]) ).
cnf(c_30404,plain,
( v1_relat_1(u2_lattices(sK2))
| ~ l2_lattices(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_780,c_406]) ).
cnf(c_30405,negated_conjecture,
( v1_relat_1(u2_lattices(sK2))
| ~ l2_lattices(sK2) ),
inference(resolve,[status(thm)],[c_482,c_30404]) ).
cnf(c_941,negated_conjecture,
v1_relat_1(u2_lattices(sK2)),
inference(resolve,[status(thm)],[c_806,c_30405]) ).
cnf(c_942,plain,
m2_relset_1(u2_lattices(sK2),k2_zfmisc_1(u1_struct_0(sK2),u1_struct_0(sK2)),u1_struct_0(sK2)),
inference(resolve,[status(thm)],[c_806,c_389]) ).
cnf(c_945,plain,
l1_struct_0(sK2),
inference(resolve,[status(thm)],[c_806,c_373]) ).
cnf(c_947,plain,
m2_relset_1(u1_lattices(sK2),k2_zfmisc_1(u1_struct_0(sK2),u1_struct_0(sK2)),u1_struct_0(sK2)),
inference(resolve,[status(thm)],[c_807,c_386]) ).
cnf(c_30406,plain,
( ~ v1_xboole_0(u1_struct_0(sK2))
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_945,c_402]) ).
cnf(c_964,negated_conjecture,
~ v1_xboole_0(u1_struct_0(sK2)),
inference(resolve,[status(thm)],[c_482,c_30406]) ).
cnf(c_1112,plain,
k7_relat_1(u1_lattices(sK2),k2_zfmisc_1(A,A)) = k1_realset1(u1_lattices(sK2),A),
inference(resolve,[status(thm)],[c_937,c_362]) ).
cnf(c_1117,plain,
k7_relat_1(u2_lattices(sK2),k2_zfmisc_1(A,A)) = k1_realset1(u2_lattices(sK2),A),
inference(resolve,[status(thm)],[c_941,c_362]) ).
cnf(c_30407,plain,
( m2_nat_lat(k23_filter_2(sK2,u1_struct_0(sK2)),sK2)
| v1_xboole_0(u1_struct_0(sK2))
| ~ l3_lattices(sK2)
| ~ v10_lattices(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_802,c_254]) ).
cnf(c_30408,negated_conjecture,
( m2_nat_lat(k23_filter_2(sK2,u1_struct_0(sK2)),sK2)
| v1_xboole_0(u1_struct_0(sK2))
| ~ l3_lattices(sK2)
| ~ v10_lattices(sK2) ),
inference(resolve,[status(thm)],[c_482,c_30407]) ).
cnf(c_30409,negated_conjecture,
( m2_nat_lat(k23_filter_2(sK2,u1_struct_0(sK2)),sK2)
| v1_xboole_0(u1_struct_0(sK2))
| ~ l3_lattices(sK2) ),
inference(resolve,[status(thm)],[c_483,c_30408]) ).
cnf(c_30410,negated_conjecture,
( m2_nat_lat(k23_filter_2(sK2,u1_struct_0(sK2)),sK2)
| v1_xboole_0(u1_struct_0(sK2)) ),
inference(resolve,[status(thm)],[c_484,c_30409]) ).
cnf(c_1800,negated_conjecture,
m2_nat_lat(k23_filter_2(sK2,u1_struct_0(sK2)),sK2),
inference(resolve,[status(thm)],[c_964,c_30410]) ).
cnf(c_30411,plain,
( sK0(sK2,u1_struct_0(sK2),A) = k1_realset1(u2_lattices(sK2),u1_struct_0(sK2))
| k23_filter_2(sK2,u1_struct_0(sK2)) != A
| ~ m2_nat_lat(A,sK2)
| v1_xboole_0(u1_struct_0(sK2))
| ~ l3_lattices(sK2)
| ~ v10_lattices(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_802,c_200]) ).
cnf(c_30412,negated_conjecture,
( sK0(sK2,u1_struct_0(sK2),A) = k1_realset1(u2_lattices(sK2),u1_struct_0(sK2))
| k23_filter_2(sK2,u1_struct_0(sK2)) != A
| ~ m2_nat_lat(A,sK2)
| v1_xboole_0(u1_struct_0(sK2))
| ~ l3_lattices(sK2)
| ~ v10_lattices(sK2) ),
inference(resolve,[status(thm)],[c_482,c_30411]) ).
cnf(c_30413,negated_conjecture,
( sK0(sK2,u1_struct_0(sK2),A) = k1_realset1(u2_lattices(sK2),u1_struct_0(sK2))
| k23_filter_2(sK2,u1_struct_0(sK2)) != A
| ~ m2_nat_lat(A,sK2)
| v1_xboole_0(u1_struct_0(sK2))
| ~ l3_lattices(sK2) ),
inference(resolve,[status(thm)],[c_483,c_30412]) ).
cnf(c_30414,negated_conjecture,
( sK0(sK2,u1_struct_0(sK2),A) = k1_realset1(u2_lattices(sK2),u1_struct_0(sK2))
| k23_filter_2(sK2,u1_struct_0(sK2)) != A
| ~ m2_nat_lat(A,sK2)
| v1_xboole_0(u1_struct_0(sK2)) ),
inference(resolve,[status(thm)],[c_484,c_30413]) ).
cnf(c_1810,negated_conjecture,
( sK0(sK2,u1_struct_0(sK2),A) = k1_realset1(u2_lattices(sK2),u1_struct_0(sK2))
| k23_filter_2(sK2,u1_struct_0(sK2)) != A
| ~ m2_nat_lat(A,sK2) ),
inference(resolve,[status(thm)],[c_964,c_30414]) ).
cnf(c_30415,plain,
( sK1(sK2,u1_struct_0(sK2),A) = k1_realset1(u1_lattices(sK2),u1_struct_0(sK2))
| k23_filter_2(sK2,u1_struct_0(sK2)) != A
| ~ m2_nat_lat(A,sK2)
| v1_xboole_0(u1_struct_0(sK2))
| ~ l3_lattices(sK2)
| ~ v10_lattices(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_802,c_196]) ).
cnf(c_30416,negated_conjecture,
( sK1(sK2,u1_struct_0(sK2),A) = k1_realset1(u1_lattices(sK2),u1_struct_0(sK2))
| k23_filter_2(sK2,u1_struct_0(sK2)) != A
| ~ m2_nat_lat(A,sK2)
| v1_xboole_0(u1_struct_0(sK2))
| ~ l3_lattices(sK2)
| ~ v10_lattices(sK2) ),
inference(resolve,[status(thm)],[c_482,c_30415]) ).
cnf(c_30417,negated_conjecture,
( sK1(sK2,u1_struct_0(sK2),A) = k1_realset1(u1_lattices(sK2),u1_struct_0(sK2))
| k23_filter_2(sK2,u1_struct_0(sK2)) != A
| ~ m2_nat_lat(A,sK2)
| v1_xboole_0(u1_struct_0(sK2))
| ~ l3_lattices(sK2) ),
inference(resolve,[status(thm)],[c_483,c_30416]) ).
cnf(c_30418,negated_conjecture,
( sK1(sK2,u1_struct_0(sK2),A) = k1_realset1(u1_lattices(sK2),u1_struct_0(sK2))
| k23_filter_2(sK2,u1_struct_0(sK2)) != A
| ~ m2_nat_lat(A,sK2)
| v1_xboole_0(u1_struct_0(sK2)) ),
inference(resolve,[status(thm)],[c_484,c_30417]) ).
cnf(c_1811,negated_conjecture,
( sK1(sK2,u1_struct_0(sK2),A) = k1_realset1(u1_lattices(sK2),u1_struct_0(sK2))
| k23_filter_2(sK2,u1_struct_0(sK2)) != A
| ~ m2_nat_lat(A,sK2) ),
inference(resolve,[status(thm)],[c_964,c_30418]) ).
cnf(c_30419,plain,
( g3_lattices(u1_struct_0(sK2),sK0(sK2,u1_struct_0(sK2),A),sK1(sK2,u1_struct_0(sK2),A)) = A
| k23_filter_2(sK2,u1_struct_0(sK2)) != A
| ~ m2_nat_lat(A,sK2)
| v1_xboole_0(u1_struct_0(sK2))
| ~ l3_lattices(sK2)
| ~ v10_lattices(sK2)
| v3_struct_0(sK2) ),
inference(resolve,[status(thm)],[c_802,c_192]) ).
cnf(c_30420,negated_conjecture,
( g3_lattices(u1_struct_0(sK2),sK0(sK2,u1_struct_0(sK2),A),sK1(sK2,u1_struct_0(sK2),A)) = A
| k23_filter_2(sK2,u1_struct_0(sK2)) != A
| ~ m2_nat_lat(A,sK2)
| v1_xboole_0(u1_struct_0(sK2))
| ~ l3_lattices(sK2)
| ~ v10_lattices(sK2) ),
inference(resolve,[status(thm)],[c_482,c_30419]) ).
cnf(c_30421,negated_conjecture,
( g3_lattices(u1_struct_0(sK2),sK0(sK2,u1_struct_0(sK2),A),sK1(sK2,u1_struct_0(sK2),A)) = A
| k23_filter_2(sK2,u1_struct_0(sK2)) != A
| ~ m2_nat_lat(A,sK2)
| v1_xboole_0(u1_struct_0(sK2))
| ~ l3_lattices(sK2) ),
inference(resolve,[status(thm)],[c_483,c_30420]) ).
cnf(c_30422,negated_conjecture,
( g3_lattices(u1_struct_0(sK2),sK0(sK2,u1_struct_0(sK2),A),sK1(sK2,u1_struct_0(sK2),A)) = A
| k23_filter_2(sK2,u1_struct_0(sK2)) != A
| ~ m2_nat_lat(A,sK2)
| v1_xboole_0(u1_struct_0(sK2)) ),
inference(resolve,[status(thm)],[c_484,c_30421]) ).
cnf(c_1812,negated_conjecture,
( g3_lattices(u1_struct_0(sK2),sK0(sK2,u1_struct_0(sK2),A),sK1(sK2,u1_struct_0(sK2),A)) = A
| k23_filter_2(sK2,u1_struct_0(sK2)) != A
| ~ m2_nat_lat(A,sK2) ),
inference(resolve,[status(thm)],[c_964,c_30422]) ).
cnf(c_7642,plain,
m1_relset_1(u2_lattices(sK2),k2_zfmisc_1(u1_struct_0(sK2),u1_struct_0(sK2)),u1_struct_0(sK2)),
inference(resolve,[status(thm)],[c_942,c_465]) ).
cnf(c_7691,plain,
m1_relset_1(u1_lattices(sK2),k2_zfmisc_1(u1_struct_0(sK2),u1_struct_0(sK2)),u1_struct_0(sK2)),
inference(resolve,[status(thm)],[c_947,c_465]) ).
cnf(c_30423,plain,
( sK0(sK2,u1_struct_0(sK2),k23_filter_2(sK2,u1_struct_0(sK2))) = k1_realset1(u2_lattices(sK2),u1_struct_0(sK2))
| k23_filter_2(sK2,u1_struct_0(sK2)) != k23_filter_2(sK2,u1_struct_0(sK2)) ),
inference(resolve,[status(thm)],[c_1810,c_1800]) ).
cnf(c_18240,plain,
sK0(sK2,u1_struct_0(sK2),k23_filter_2(sK2,u1_struct_0(sK2))) = k1_realset1(u2_lattices(sK2),u1_struct_0(sK2)),
inference(copy,[status(thm)],[c_30423]) ).
cnf(c_30424,plain,
( sK1(sK2,u1_struct_0(sK2),k23_filter_2(sK2,u1_struct_0(sK2))) = k1_realset1(u1_lattices(sK2),u1_struct_0(sK2))
| k23_filter_2(sK2,u1_struct_0(sK2)) != k23_filter_2(sK2,u1_struct_0(sK2)) ),
inference(resolve,[status(thm)],[c_1811,c_1800]) ).
cnf(c_18261,plain,
sK1(sK2,u1_struct_0(sK2),k23_filter_2(sK2,u1_struct_0(sK2))) = k1_realset1(u1_lattices(sK2),u1_struct_0(sK2)),
inference(copy,[status(thm)],[c_30424]) ).
cnf(c_30425,plain,
( g3_lattices(u1_struct_0(sK2),sK0(sK2,u1_struct_0(sK2),k23_filter_2(sK2,u1_struct_0(sK2))),sK1(sK2,u1_struct_0(sK2),k23_filter_2(sK2,u1_struct_0(sK2)))) = k23_filter_2(sK2,u1_struct_0(sK2))
| k23_filter_2(sK2,u1_struct_0(sK2)) != k23_filter_2(sK2,u1_struct_0(sK2)) ),
inference(resolve,[status(thm)],[c_1812,c_1800]) ).
cnf(c_30426,plain,
( g3_lattices(u1_struct_0(sK2),k1_realset1(u2_lattices(sK2),u1_struct_0(sK2)),sK1(sK2,u1_struct_0(sK2),k23_filter_2(sK2,u1_struct_0(sK2)))) = k23_filter_2(sK2,u1_struct_0(sK2))
| k23_filter_2(sK2,u1_struct_0(sK2)) != k23_filter_2(sK2,u1_struct_0(sK2)) ),
inference(paramod,[status(thm)],[c_18240,c_30425]) ).
cnf(c_30427,plain,
( g3_lattices(u1_struct_0(sK2),k1_realset1(u2_lattices(sK2),u1_struct_0(sK2)),k1_realset1(u1_lattices(sK2),u1_struct_0(sK2))) = k23_filter_2(sK2,u1_struct_0(sK2))
| k23_filter_2(sK2,u1_struct_0(sK2)) != k23_filter_2(sK2,u1_struct_0(sK2)) ),
inference(paramod,[status(thm)],[c_18261,c_30426]) ).
cnf(c_18282,plain,
g3_lattices(u1_struct_0(sK2),k1_realset1(u2_lattices(sK2),u1_struct_0(sK2)),k1_realset1(u1_lattices(sK2),u1_struct_0(sK2))) = k23_filter_2(sK2,u1_struct_0(sK2)),
inference(copy,[status(thm)],[c_30427]) ).
cnf(c_23341,plain,
k4_relset_1(k2_zfmisc_1(u1_struct_0(sK2),u1_struct_0(sK2)),u1_struct_0(sK2),u2_lattices(sK2)) = k1_relat_1(u2_lattices(sK2)),
inference(resolve,[status(thm)],[c_7642,c_461]) ).
cnf(c_30428,plain,
m1_subset_1(k4_relset_1(k2_zfmisc_1(u1_struct_0(sK2),u1_struct_0(sK2)),u1_struct_0(sK2),u2_lattices(sK2)),k1_zfmisc_1(k2_zfmisc_1(u1_struct_0(sK2),u1_struct_0(sK2)))),
inference(resolve,[status(thm)],[c_7642,c_369]) ).
cnf(c_23345,plain,
m1_subset_1(k1_relat_1(u2_lattices(sK2)),k1_zfmisc_1(k2_zfmisc_1(u1_struct_0(sK2),u1_struct_0(sK2)))),
inference(paramod,[status(thm)],[c_23341,c_30428]) ).
cnf(c_23375,plain,
k4_relset_1(k2_zfmisc_1(u1_struct_0(sK2),u1_struct_0(sK2)),u1_struct_0(sK2),u1_lattices(sK2)) = k1_relat_1(u1_lattices(sK2)),
inference(resolve,[status(thm)],[c_7691,c_461]) ).
cnf(c_30429,plain,
m1_subset_1(k4_relset_1(k2_zfmisc_1(u1_struct_0(sK2),u1_struct_0(sK2)),u1_struct_0(sK2),u1_lattices(sK2)),k1_zfmisc_1(k2_zfmisc_1(u1_struct_0(sK2),u1_struct_0(sK2)))),
inference(resolve,[status(thm)],[c_7691,c_369]) ).
cnf(c_23379,plain,
m1_subset_1(k1_relat_1(u1_lattices(sK2)),k1_zfmisc_1(k2_zfmisc_1(u1_struct_0(sK2),u1_struct_0(sK2)))),
inference(paramod,[status(thm)],[c_23375,c_30429]) ).
cnf(c_30279,plain,
r1_tarski(k1_relat_1(u2_lattices(sK2)),k2_zfmisc_1(u1_struct_0(sK2),u1_struct_0(sK2))),
inference(resolve,[status(thm)],[c_23345,c_474]) ).
cnf(c_30430,plain,
( k7_relat_1(u2_lattices(sK2),k2_zfmisc_1(u1_struct_0(sK2),u1_struct_0(sK2))) = u2_lattices(sK2)
| ~ v1_relat_1(u2_lattices(sK2)) ),
inference(resolve,[status(thm)],[c_30279,c_481]) ).
cnf(c_30431,plain,
( k1_realset1(u2_lattices(sK2),u1_struct_0(sK2)) = u2_lattices(sK2)
| ~ v1_relat_1(u2_lattices(sK2)) ),
inference(paramod,[status(thm)],[c_1117,c_30430]) ).
cnf(c_30320,plain,
k1_realset1(u2_lattices(sK2),u1_struct_0(sK2)) = u2_lattices(sK2),
inference(resolve,[status(thm)],[c_941,c_30431]) ).
cnf(c_30321,plain,
g3_lattices(u1_struct_0(sK2),u2_lattices(sK2),k1_realset1(u1_lattices(sK2),u1_struct_0(sK2))) = k23_filter_2(sK2,u1_struct_0(sK2)),
inference(paramod,[status(thm)],[c_30320,c_18282]) ).
cnf(c_30334,plain,
r1_tarski(k1_relat_1(u1_lattices(sK2)),k2_zfmisc_1(u1_struct_0(sK2),u1_struct_0(sK2))),
inference(resolve,[status(thm)],[c_23379,c_474]) ).
cnf(c_30432,plain,
( k7_relat_1(u1_lattices(sK2),k2_zfmisc_1(u1_struct_0(sK2),u1_struct_0(sK2))) = u1_lattices(sK2)
| ~ v1_relat_1(u1_lattices(sK2)) ),
inference(resolve,[status(thm)],[c_30334,c_481]) ).
cnf(c_30433,plain,
( k1_realset1(u1_lattices(sK2),u1_struct_0(sK2)) = u1_lattices(sK2)
| ~ v1_relat_1(u1_lattices(sK2)) ),
inference(paramod,[status(thm)],[c_1112,c_30432]) ).
cnf(c_30375,plain,
k1_realset1(u1_lattices(sK2),u1_struct_0(sK2)) = u1_lattices(sK2),
inference(resolve,[status(thm)],[c_937,c_30433]) ).
cnf(c_30434,plain,
g3_lattices(u1_struct_0(sK2),u2_lattices(sK2),u1_lattices(sK2)) = k23_filter_2(sK2,u1_struct_0(sK2)),
inference(paramod,[status(thm)],[c_30375,c_30321]) ).
cnf(c_30376,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_801,c_30434]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT332+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n019.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:58:04 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.36 % Process 3683239 was started by sandbox on n019,
% 0.10/0.36 % Fri Sep 25 20:58:04 2026
% 0.10/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.15/0.39
% 0.15/0.39 % From the command line: assign(max_seconds, 300).
% 221.54/28.69
% 221.54/28.69 % given #500 (T,wt=4): 1290 v5_lattices(f12(f9(c13))). [resolve(1243,a,426,b),unit_del(a,1244),unit_del(b,1242)].
% 221.54/28.69
% 221.54/28.69 % given #1000 (T,wt=5): 5244 v8_lattices(f12(f9(f9(c14)))). [resolve(5200,a,429,b),unit_del(a,5201),unit_del(b,5199)].
% 221.54/28.69
% 221.54/28.69 % given #1500 (T,wt=7): 4577 v7_lattices(k23_filter_2(f12(c14),f4(f12(c14)))). [resolve(1529,a,266,d),unit_del(a,765),unit_del(b,759),unit_del(c,1484),unit_del(d,4572)].
% 221.54/28.69
% 221.54/28.69 % given #2000 (T,wt=5): 10958 v5_lattices(f9(f9(f9(c13)))). [resolve(10895,a,349,c),unit_del(a,10894),unit_del(b,10896)].
% 221.54/28.69
% 221.54/28.69 % given #2500 (A,wt=22): 1460 -m2_nat_lat(A,c13) | k23_filter_2(c13,u1_struct_0(c13)) != A | v1_funct_2(f2(c13,u1_struct_0(c13),A),k2_zfmisc_1(u1_struct_0(c13),u1_struct_0(c13)),u1_struct_0(c13)). [resolve(720,a,208,h),unit_del(a,451),unit_del(b,457),unit_del(c,450),unit_del(d,961)].
% 221.54/28.69
% 221.54/28.69 % given #3000 (F,wt=8): 15901 -v1_xboole_0(u1_struct_0(k23_filter_2(f12(c14),u1_struct_0(f12(c14))))). [resolve(15895,a,402,b),unit_del(a,4537)].
% 221.54/28.69
% 221.54/28.69 % given #3500 (T,wt=9): 8507 v1_funct_1(k1_realset1(k1_realset1(k1_realset1(u1_lattices(c1),A),B),C)). [resolve(6394,a,405,a),unit_del(a,6393)].
% 221.54/28.69
% 221.54/28.69 % given #4000 (T,wt=10): 3467 r1_filter_2(u1_struct_0(c13),f8(c13),k1_xboole_0) | f8(c13) != k1_xboole_0. [resolve(748,b,716,a),flip(c),unit_del(a,961)].
% 221.54/28.69
% 221.54/28.69 % given #4500 (T,wt=9): 22001 v1_funct_1(k7_relat_1(u2_lattices(f12(k23_filter_2(c14,f4(c14)))),A)). [resolve(21951,a,410,a),unit_del(a,21956)].
% 221.54/28.69
% 221.54/28.69 % given #5000 (F,wt=45): 23223 -v1_funct_1(k7_relat_1(f10(k2_zfmisc_1(u1_struct_0(c12),u1_struct_0(c12)),u1_struct_0(c12)),A)) | -v1_funct_2(k7_relat_1(f10(k2_zfmisc_1(u1_struct_0(c12),u1_struct_0(c12)),u1_struct_0(c12)),A),k2_zfmisc_1(u1_struct_0(c12),u1_struct_0(c12)),u1_struct_0(c12)) | -v3_struct_0(g3_lattices(u1_struct_0(c12),u1_lattices(c12),k7_relat_1(f10(k2_zfmisc_1(u1_struct_0(c12),u1_struct_0(c12)),u1_struct_0(c12)),A))). [resolve(23205,c,8864,a)].
% 221.54/28.69
% 221.54/28.69 % given #5500 (A,wt=15): 3236 v1_xboole_0(A) | r1_filter_2(A,f13(A),f6(k1_zfmisc_1(A))) | f13(A) != f6(k1_zfmisc_1(A)). [resolve(731,b,397,a)].
% 221.54/28.69
% 221.54/28.69 % given #6000 (A,wt=31): 3422 v1_xboole_0(f11(f12(f12(c13)))) | f1(f12(f12(c13)),f11(f12(f12(c13))),k23_filter_2(f12(f12(c13)),f11(f12(f12(c13))))) = k1_realset1(u2_lattices(f12(f12(c13))),f11(f12(f12(c13)))). [back_unit_del(1837),unit_del(a,3359)].
% 221.54/28.69
% 221.54/28.69 % given #6500 (T,wt=7): 27631 v1_relat_1(u2_lattices(f9(f12(f9(f9(c14)))))). [resolve(27598,a,338,d),unit_del(a,27595),unit_del(b,27597),unit_del(c,27596)].
% 221.54/28.69
% 221.54/28.69 % given #7000 (A,wt=14): 3919 v1_xboole_0(f8(f9(f9(c13)))) | v9_lattices(k23_filter_2(f9(f9(c13)),f8(f9(f9(c13))))). [resolve(3842,a,302,b),unit_del(a,3843),unit_del(b,3841)].
% 221.54/28.69
% 221.54/28.69 % given #7500 (A,wt=21): 4184 v1_xboole_0(f8(k23_filter_2(c13,f7(c13)))) | m2_nat_lat(k23_filter_2(k23_filter_2(c13,f7(c13)),f8(k23_filter_2(c13,f7(c13)))),k23_filter_2(c13,f7(c13))). [back_unit_del(2296),unit_del(a,4164)].
% 221.54/28.69
% 221.54/28.69 % SZS status Theorem for theBenchmark
% 221.54/28.69
% 221.54/28.69 % Proof 1 at 26.98 (+ 0.61) seconds.
% 221.54/28.69 % Length of proof is 99.
% 221.54/28.69 % Level of proof is 10.
% 221.54/28.69 % Maximum clause weight is 31.000.
% 221.54/28.69 % Given clauses 7749.
% 221.54/28.69
% 221.54/28.69 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------