%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT332+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /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 : Thu Sep 24 01:02:47 PM UTC 2026
% Result : Theorem 76.86s 15.19s
% Output : CNFRefutation 68.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 22
% Syntax : Number of formulae : 174 ( 45 unt; 0 def)
% Number of atoms : 591 ( 113 equ)
% Maximal formula atoms : 26 ( 3 avg)
% Number of connectives : 650 ( 233 ~; 274 |; 113 &)
% ( 4 <=>; 26 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 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 : 155 ( 148 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,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(negated_conjecture,[status(cth)],[f1]) ).
fof(f6,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k1_filter_0(A) = u1_struct_0(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A] :
( v1_relat_1(A)
=> ! [B] : k1_realset1(A,B) = k7_relat_1(A,k2_zfmisc_1(B,B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k17_filter_2(A) = u1_struct_0(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m1_filter_2(k1_filter_2(A),A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [A,B,C] :
( m1_relset_1(C,A,B)
=> m1_subset_1(k4_relset_1(A,B,C),k1_zfmisc_1(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [A] :
( l1_lattices(A)
=> l1_struct_0(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [A] :
( l3_lattices(A)
=> ( l2_lattices(A)
& l1_lattices(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_filter_2(B,A)
=> ( m2_lattice4(B,A)
& ~ v1_xboole_0(B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [A] :
( ( l1_struct_0(A)
& ~ v3_struct_0(A) )
=> ~ v1_xboole_0(u1_struct_0(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f59,axiom,
! [A] :
( ( l2_lattices(A)
& v4_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))
& v1_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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [A] :
( ( l1_lattices(A)
& v6_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))
& v1_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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f83,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k1_filter_2(A) = k1_filter_0(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f84,axiom,
! [A,B,C] :
( m1_relset_1(C,A,B)
=> k4_relset_1(A,B,C) = k1_relat_1(C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f87,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f94,axiom,
! [A,B] :
( m1_subset_1(A,k1_zfmisc_1(B))
<=> r1_tarski(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f100,axiom,
! [A,B] :
( v1_relat_1(B)
=> ( r1_tarski(k1_relat_1(B),A)
=> k7_relat_1(B,A) = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f101,plain,
? [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)) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f102,plain,
( ( k23_filter_2(sK0_skl,k1_filter_2(sK0_skl)) != g3_lattices(u1_struct_0(sK0_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl))
| k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)) != g3_lattices(u1_struct_0(sK0_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl)) )
& l3_lattices(sK0_skl)
& v10_lattices(sK0_skl)
& ~ v3_struct_0(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(A,sK0_skl)],[f101]) ).
fof(f103,plain,
~ v3_struct_0(sK0_skl),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f104,plain,
v10_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f105,plain,
l3_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f106,plain,
( k23_filter_2(sK0_skl,k1_filter_2(sK0_skl)) != g3_lattices(u1_struct_0(sK0_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl))
| k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)) != g3_lattices(u1_struct_0(sK0_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl)) ),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f113,plain,
! [A] :
( ( v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A) )
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f115,plain,
! [X0] :
( v4_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f117,plain,
! [X0] :
( v6_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f113]) ).
fof(f131,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( 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) ) )
| ~ m2_nat_lat(C,A) )
| ~ m2_lattice4(B,A)
| v1_xboole_0(B) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f132,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ! [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) )
| 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) )
| C != k23_filter_2(A,B) ) )
| ~ m2_nat_lat(C,A) )
| ~ m2_lattice4(B,A)
| v1_xboole_0(B) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f131]) ).
fof(f133,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( ( ! [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) )
| C = k23_filter_2(A,B) )
& ( ( C = g3_lattices(B,sK1_skl(C,B,A),sK2_skl(C,B,A))
& sK2_skl(C,B,A) = k1_realset1(u1_lattices(A),B)
& sK1_skl(C,B,A) = k1_realset1(u2_lattices(A),B)
& m2_relset_1(sK2_skl(C,B,A),k2_zfmisc_1(B,B),B)
& v1_funct_2(sK2_skl(C,B,A),k2_zfmisc_1(B,B),B)
& v1_funct_1(sK2_skl(C,B,A))
& m2_relset_1(sK1_skl(C,B,A),k2_zfmisc_1(B,B),B)
& v1_funct_2(sK1_skl(C,B,A),k2_zfmisc_1(B,B),B)
& v1_funct_1(sK1_skl(C,B,A)) )
| C != k23_filter_2(A,B) ) )
| ~ 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,[sK1_skl,sK2_skl]),skolemize(D,sK1_skl(C,B,A)),skolemize(E,sK2_skl(C,B,A))],[f132]) ).
fof(f140,plain,
! [X0,X1,X2] :
( sK1_skl(X2,X1,X0) = k1_realset1(u2_lattices(X0),X1)
| X2 != k23_filter_2(X0,X1)
| ~ m2_nat_lat(X2,X0)
| ~ m2_lattice4(X1,X0)
| v1_xboole_0(X1)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f141,plain,
! [X0,X1,X2] :
( sK2_skl(X2,X1,X0) = k1_realset1(u1_lattices(X0),X1)
| X2 != k23_filter_2(X0,X1)
| ~ m2_nat_lat(X2,X0)
| ~ m2_lattice4(X1,X0)
| v1_xboole_0(X1)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f142,plain,
! [X0,X1,X2] :
( X2 = g3_lattices(X1,sK1_skl(X2,X1,X0),sK2_skl(X2,X1,X0))
| X2 != k23_filter_2(X0,X1)
| ~ m2_nat_lat(X2,X0)
| ~ m2_lattice4(X1,X0)
| v1_xboole_0(X1)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f152,plain,
! [A] :
( k1_filter_0(A) = u1_struct_0(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f153,plain,
! [X0] :
( k1_filter_0(X0) = u1_struct_0(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f152]) ).
fof(f154,plain,
! [A] :
( ! [B] : k1_realset1(A,B) = k7_relat_1(A,k2_zfmisc_1(B,B))
| ~ v1_relat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f13]) ).
fof(f155,plain,
! [X0,X1] :
( k1_realset1(X0,X1) = k7_relat_1(X0,k2_zfmisc_1(X1,X1))
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f156,plain,
! [A] :
( k17_filter_2(A) = u1_struct_0(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f157,plain,
! [X0] :
( k17_filter_2(X0) = u1_struct_0(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f156]) ).
fof(f165,plain,
! [A] :
( m1_filter_2(k1_filter_2(A),A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f166,plain,
! [X0] :
( m1_filter_2(k1_filter_2(X0),X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f167,plain,
! [A,B] :
( 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(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f168,plain,
! [X0,X1] :
( m2_nat_lat(k23_filter_2(X0,X1),X0)
| ~ m2_lattice4(X1,X0)
| v1_xboole_0(X1)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f169,plain,
! [A,B,C] :
( m1_subset_1(k4_relset_1(A,B,C),k1_zfmisc_1(A))
| ~ m1_relset_1(C,A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f25]) ).
fof(f170,plain,
! [X0,X1,X2] :
( m1_subset_1(k4_relset_1(X1,X2,X0),k1_zfmisc_1(X1))
| ~ m1_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f177,plain,
! [A] :
( l1_struct_0(A)
| ~ l1_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f178,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f177]) ).
fof(f181,plain,
! [A] :
( ( l2_lattices(A)
& l1_lattices(A) )
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f182,plain,
! [X0] :
( l1_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f183,plain,
! [X0] :
( l2_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f187,plain,
! [A] :
( ! [B] :
( ( m2_lattice4(B,A)
& ~ v1_xboole_0(B) )
| ~ m1_filter_2(B,A) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f189,plain,
! [X0,X1] :
( m2_lattice4(X1,X0)
| ~ m1_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f187]) ).
fof(f201,plain,
! [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)) )
| ~ l1_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f204,plain,
! [X0] :
( m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f205,plain,
! [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)) )
| ~ l2_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f208,plain,
! [X0] :
( m2_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f205]) ).
fof(f241,plain,
! [A] :
( ~ v1_xboole_0(u1_struct_0(A))
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f56]) ).
fof(f242,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| ~ l1_struct_0(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f241]) ).
fof(f245,plain,
! [A] :
( ( v1_partfun1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_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)) )
| ~ l2_lattices(A)
| ~ v4_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f59]) ).
fof(f246,plain,
! [X0] :
( v1_relat_1(u2_lattices(X0))
| ~ l2_lattices(X0)
| ~ v4_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f245]) ).
fof(f268,plain,
! [A] :
( ( v1_partfun1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_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)) )
| ~ l1_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f64]) ).
fof(f269,plain,
! [X0] :
( v1_relat_1(u1_lattices(X0))
| ~ l1_lattices(X0)
| ~ v6_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f268]) ).
fof(f359,plain,
! [A] :
( k1_filter_2(A) = k1_filter_0(A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f83]) ).
fof(f360,plain,
! [X0] :
( k1_filter_2(X0) = k1_filter_0(X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f359]) ).
fof(f361,plain,
! [A,B,C] :
( k4_relset_1(A,B,C) = k1_relat_1(C)
| ~ m1_relset_1(C,A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f84]) ).
fof(f362,plain,
! [X0,X1,X2] :
( k4_relset_1(X1,X2,X0) = k1_relat_1(X0)
| ~ m1_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f361]) ).
fof(f371,plain,
! [A,B,C] :
( ( ~ m1_relset_1(C,A,B)
| m2_relset_1(C,A,B) )
& ( m1_relset_1(C,A,B)
| ~ m2_relset_1(C,A,B) ) ),
inference(NNF_transformation,[status(thm)],[f87]) ).
fof(f372,plain,
( ! [A,B,C] :
( ~ m1_relset_1(C,A,B)
| m2_relset_1(C,A,B) )
& ! [A,B,C] :
( m1_relset_1(C,A,B)
| ~ m2_relset_1(C,A,B) ) ),
inference(miniscoping,[status(thm)],[f371]) ).
fof(f373,plain,
! [X0,X1,X2] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f372]) ).
fof(f390,plain,
! [A,B] :
( ( ~ r1_tarski(A,B)
| m1_subset_1(A,k1_zfmisc_1(B)) )
& ( r1_tarski(A,B)
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ) ),
inference(NNF_transformation,[status(thm)],[f94]) ).
fof(f391,plain,
( ! [A,B] :
( ~ r1_tarski(A,B)
| m1_subset_1(A,k1_zfmisc_1(B)) )
& ! [A,B] :
( r1_tarski(A,B)
| ~ m1_subset_1(A,k1_zfmisc_1(B)) ) ),
inference(miniscoping,[status(thm)],[f390]) ).
fof(f392,plain,
! [X0,X1] :
( r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ),
inference(cnf_transformation,[status(thm)],[f391]) ).
fof(f408,plain,
! [A,B] :
( k7_relat_1(B,A) = B
| ~ r1_tarski(k1_relat_1(B),A)
| ~ v1_relat_1(B) ),
inference(pre_NNF_transformation,[status(thm)],[f100]) ).
fof(f409,plain,
! [B] :
( ! [A] :
( k7_relat_1(B,A) = B
| ~ r1_tarski(k1_relat_1(B),A) )
| ~ v1_relat_1(B) ),
inference(miniscoping,[status(thm)],[f408]) ).
fof(f410,plain,
! [X0,X1] :
( k7_relat_1(X0,X1) = X0
| ~ r1_tarski(k1_relat_1(X0),X1)
| ~ v1_relat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f409]) ).
fof(f422,plain,
! [X0,X1] :
( sK1_skl(k23_filter_2(X0,X1),X1,X0) = k1_realset1(u2_lattices(X0),X1)
| ~ m2_nat_lat(k23_filter_2(X0,X1),X0)
| ~ m2_lattice4(X1,X0)
| v1_xboole_0(X1)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f140]) ).
fof(f423,plain,
! [X0,X1] :
( sK2_skl(k23_filter_2(X0,X1),X1,X0) = k1_realset1(u1_lattices(X0),X1)
| ~ m2_nat_lat(k23_filter_2(X0,X1),X0)
| ~ m2_lattice4(X1,X0)
| v1_xboole_0(X1)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f141]) ).
fof(f424,plain,
! [X0,X1] :
( k23_filter_2(X0,X1) = g3_lattices(X1,sK1_skl(k23_filter_2(X0,X1),X1,X0),sK2_skl(k23_filter_2(X0,X1),X1,X0))
| ~ m2_nat_lat(k23_filter_2(X0,X1),X0)
| ~ m2_lattice4(X1,X0)
| v1_xboole_0(X1)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f142]) ).
fof(f432,plain,
( k17_filter_2(sK0_skl) = u1_struct_0(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f157,f105]) ).
fof(f433,plain,
( k17_filter_2(sK0_skl) = u1_struct_0(sK0_skl)
| ~ v10_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f432,f103]) ).
fof(f434,plain,
k17_filter_2(sK0_skl) = u1_struct_0(sK0_skl),
inference(forward_subsumption_resolution,[status(thm)],[f433,f104]) ).
fof(f438,plain,
( k23_filter_2(sK0_skl,k1_filter_2(sK0_skl)) != g3_lattices(u1_struct_0(sK0_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl))
| k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)) != g3_lattices(k17_filter_2(sK0_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f434,f106]) ).
fof(f439,plain,
( k23_filter_2(sK0_skl,k1_filter_2(sK0_skl)) != g3_lattices(k17_filter_2(sK0_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl))
| k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)) != g3_lattices(k17_filter_2(sK0_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f434,f438]) ).
fof(f446,plain,
( m1_filter_2(k1_filter_2(sK0_skl),sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f166,f105]) ).
fof(f447,plain,
( m1_filter_2(k1_filter_2(sK0_skl),sK0_skl)
| ~ v10_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f446,f103]) ).
fof(f448,plain,
m1_filter_2(k1_filter_2(sK0_skl),sK0_skl),
inference(forward_subsumption_resolution,[status(thm)],[f447,f104]) ).
fof(f452,plain,
( k1_filter_2(sK0_skl) = k1_filter_0(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f360,f105]) ).
fof(f453,plain,
( k1_filter_2(sK0_skl) = k1_filter_0(sK0_skl)
| ~ v10_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f452,f103]) ).
fof(f454,plain,
k1_filter_2(sK0_skl) = k1_filter_0(sK0_skl),
inference(forward_subsumption_resolution,[status(thm)],[f453,f104]) ).
fof(f458,plain,
( v4_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f115,f105]) ).
fof(f459,plain,
( v4_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f458,f103]) ).
fof(f464,plain,
( v6_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f117,f105]) ).
fof(f465,plain,
( v6_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f464,f103]) ).
fof(f466,plain,
v4_lattices(sK0_skl),
inference(forward_subsumption_resolution,[status(thm)],[f459,f104]) ).
fof(f468,plain,
v6_lattices(sK0_skl),
inference(forward_subsumption_resolution,[status(thm)],[f465,f104]) ).
fof(f562,plain,
l1_lattices(sK0_skl),
inference(resolution,[status(thm)],[f182,f105]) ).
fof(f567,plain,
l1_struct_0(sK0_skl),
inference(resolution,[status(thm)],[f562,f178]) ).
fof(f572,plain,
( k1_filter_0(sK0_skl) = u1_struct_0(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f153,f105]) ).
fof(f577,plain,
( k1_filter_2(sK0_skl) = u1_struct_0(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f454,f572]) ).
fof(f578,plain,
( k1_filter_2(sK0_skl) = k17_filter_2(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f434,f577]) ).
fof(f579,plain,
( k1_filter_2(sK0_skl) = k17_filter_2(sK0_skl)
| ~ v10_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f578,f103]) ).
fof(f584,plain,
m1_filter_2(k17_filter_2(sK0_skl),sK0_skl),
inference(backward_demodulation,[status(thm)],[f586,f448]) ).
fof(f585,plain,
( k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)) != g3_lattices(k17_filter_2(sK0_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl))
| k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)) != g3_lattices(k17_filter_2(sK0_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl)) ),
inference(backward_demodulation,[status(thm)],[f586,f439]) ).
fof(f586,plain,
k1_filter_2(sK0_skl) = k17_filter_2(sK0_skl),
inference(forward_subsumption_resolution,[status(thm)],[f579,f104]) ).
fof(f587,plain,
k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)) != g3_lattices(k17_filter_2(sK0_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl)),
inference(duplicate_literals_removal,[status(thm)],[f585]) ).
fof(f597,plain,
l2_lattices(sK0_skl),
inference(resolution,[status(thm)],[f183,f105]) ).
fof(f609,plain,
! [X0,X1] :
( k23_filter_2(X0,X1) = g3_lattices(X1,sK1_skl(k23_filter_2(X0,X1),X1,X0),sK2_skl(k23_filter_2(X0,X1),X1,X0))
| ~ m2_lattice4(X1,X0)
| v1_xboole_0(X1)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f424,f168]) ).
fof(f610,plain,
! [X0,X1] :
( sK2_skl(k23_filter_2(X0,X1),X1,X0) = k1_realset1(u1_lattices(X0),X1)
| ~ m2_lattice4(X1,X0)
| v1_xboole_0(X1)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f423,f168]) ).
fof(f611,plain,
! [X0,X1] :
( sK1_skl(k23_filter_2(X0,X1),X1,X0) = k1_realset1(u2_lattices(X0),X1)
| ~ m2_lattice4(X1,X0)
| v1_xboole_0(X1)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f422,f168]) ).
fof(f664,plain,
( m2_lattice4(k17_filter_2(sK0_skl),sK0_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f189,f584]) ).
fof(f666,plain,
( m2_lattice4(k17_filter_2(sK0_skl),sK0_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f664,f103]) ).
fof(f683,plain,
( m2_lattice4(k17_filter_2(sK0_skl),sK0_skl)
| ~ l3_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f666,f104]) ).
fof(f684,plain,
m2_lattice4(k17_filter_2(sK0_skl),sK0_skl),
inference(resolution,[status(thm)],[f683,f105]) ).
fof(f764,plain,
m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)),
inference(resolution,[status(thm)],[f204,f562]) ).
fof(f770,plain,
m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k17_filter_2(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f434,f764]) ).
fof(f771,plain,
m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k17_filter_2(sK0_skl),k17_filter_2(sK0_skl)),u1_struct_0(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f434,f770]) ).
fof(f772,plain,
m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k17_filter_2(sK0_skl),k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f434,f771]) ).
fof(f838,plain,
m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)),
inference(resolution,[status(thm)],[f208,f597]) ).
fof(f841,plain,
m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(k17_filter_2(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f434,f838]) ).
fof(f842,plain,
m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(k17_filter_2(sK0_skl),k17_filter_2(sK0_skl)),u1_struct_0(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f434,f841]) ).
fof(f843,plain,
m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(k17_filter_2(sK0_skl),k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f434,f842]) ).
fof(f961,plain,
m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(k17_filter_2(sK0_skl),k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl)),
inference(resolution,[status(thm)],[f373,f843]) ).
fof(f964,plain,
m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k17_filter_2(sK0_skl),k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl)),
inference(resolution,[status(thm)],[f373,f772]) ).
fof(f999,plain,
( ~ v1_xboole_0(k17_filter_2(sK0_skl))
| ~ l1_struct_0(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(paramodulation,[status(thm)],[f434,f242]) ).
fof(f1001,plain,
( ~ v1_xboole_0(k17_filter_2(sK0_skl))
| ~ l1_struct_0(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f999,f103]) ).
fof(f1006,plain,
( v1_relat_1(u2_lattices(sK0_skl))
| ~ v4_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f246,f597]) ).
fof(f1010,plain,
( v1_relat_1(u2_lattices(sK0_skl))
| ~ v4_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1006,f103]) ).
fof(f1014,plain,
~ v1_xboole_0(k17_filter_2(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f1001,f567]) ).
fof(f1015,plain,
v1_relat_1(u2_lattices(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f1010,f466]) ).
fof(f1018,plain,
! [X0] : k1_realset1(u2_lattices(sK0_skl),X0) = k7_relat_1(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0)),
inference(resolution,[status(thm)],[f1015,f155]) ).
fof(f1353,plain,
( v1_relat_1(u1_lattices(sK0_skl))
| ~ v6_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f269,f562]) ).
fof(f1359,plain,
( v1_relat_1(u1_lattices(sK0_skl))
| ~ v6_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1353,f103]) ).
fof(f1362,plain,
v1_relat_1(u1_lattices(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f1359,f468]) ).
fof(f1367,plain,
! [X0] : k1_realset1(u1_lattices(sK0_skl),X0) = k7_relat_1(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0)),
inference(resolution,[status(thm)],[f1362,f155]) ).
fof(f2203,plain,
( k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)) = g3_lattices(k17_filter_2(sK0_skl),sK1_skl(k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl),sK0_skl),sK2_skl(k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl),sK0_skl))
| v1_xboole_0(k17_filter_2(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f609,f684]) ).
fof(f2209,plain,
( k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)) = g3_lattices(k17_filter_2(sK0_skl),sK1_skl(k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl),sK0_skl),sK2_skl(k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl),sK0_skl))
| v1_xboole_0(k17_filter_2(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2203,f103]) ).
fof(f2303,plain,
( sK2_skl(k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl),sK0_skl) = k1_realset1(u1_lattices(sK0_skl),k17_filter_2(sK0_skl))
| v1_xboole_0(k17_filter_2(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f610,f684]) ).
fof(f2309,plain,
( sK2_skl(k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl),sK0_skl) = k1_realset1(u1_lattices(sK0_skl),k17_filter_2(sK0_skl))
| v1_xboole_0(k17_filter_2(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2303,f103]) ).
fof(f2315,plain,
( sK1_skl(k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl),sK0_skl) = k1_realset1(u2_lattices(sK0_skl),k17_filter_2(sK0_skl))
| v1_xboole_0(k17_filter_2(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f611,f684]) ).
fof(f2321,plain,
( sK1_skl(k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl),sK0_skl) = k1_realset1(u2_lattices(sK0_skl),k17_filter_2(sK0_skl))
| v1_xboole_0(k17_filter_2(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2315,f103]) ).
fof(f3428,plain,
k4_relset_1(k2_zfmisc_1(k17_filter_2(sK0_skl),k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl),u2_lattices(sK0_skl)) = k1_relat_1(u2_lattices(sK0_skl)),
inference(resolution,[status(thm)],[f961,f362]) ).
fof(f3431,plain,
m1_subset_1(k4_relset_1(k2_zfmisc_1(k17_filter_2(sK0_skl),k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl),u2_lattices(sK0_skl)),k1_zfmisc_1(k2_zfmisc_1(k17_filter_2(sK0_skl),k17_filter_2(sK0_skl)))),
inference(resolution,[status(thm)],[f961,f170]) ).
fof(f3567,plain,
k4_relset_1(k2_zfmisc_1(k17_filter_2(sK0_skl),k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl),u1_lattices(sK0_skl)) = k1_relat_1(u1_lattices(sK0_skl)),
inference(resolution,[status(thm)],[f964,f362]) ).
fof(f3570,plain,
m1_subset_1(k4_relset_1(k2_zfmisc_1(k17_filter_2(sK0_skl),k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl),u1_lattices(sK0_skl)),k1_zfmisc_1(k2_zfmisc_1(k17_filter_2(sK0_skl),k17_filter_2(sK0_skl)))),
inference(resolution,[status(thm)],[f964,f170]) ).
fof(f14032,plain,
( k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)) = g3_lattices(k17_filter_2(sK0_skl),sK1_skl(k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl),sK0_skl),sK2_skl(k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl),sK0_skl))
| v1_xboole_0(k17_filter_2(sK0_skl))
| ~ l3_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2209,f104]) ).
fof(f14407,plain,
( sK2_skl(k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl),sK0_skl) = k1_realset1(u1_lattices(sK0_skl),k17_filter_2(sK0_skl))
| v1_xboole_0(k17_filter_2(sK0_skl))
| ~ l3_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2309,f104]) ).
fof(f14505,plain,
( sK1_skl(k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl),sK0_skl) = k1_realset1(u2_lattices(sK0_skl),k17_filter_2(sK0_skl))
| v1_xboole_0(k17_filter_2(sK0_skl))
| ~ l3_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2321,f104]) ).
fof(f18726,plain,
m1_subset_1(k1_relat_1(u2_lattices(sK0_skl)),k1_zfmisc_1(k2_zfmisc_1(k17_filter_2(sK0_skl),k17_filter_2(sK0_skl)))),
inference(forward_demodulation,[status(thm)],[f3428,f3431]) ).
fof(f18733,plain,
r1_tarski(k1_relat_1(u2_lattices(sK0_skl)),k2_zfmisc_1(k17_filter_2(sK0_skl),k17_filter_2(sK0_skl))),
inference(resolution,[status(thm)],[f18726,f392]) ).
fof(f19138,plain,
( k7_relat_1(u2_lattices(sK0_skl),k2_zfmisc_1(k17_filter_2(sK0_skl),k17_filter_2(sK0_skl))) = u2_lattices(sK0_skl)
| ~ v1_relat_1(u2_lattices(sK0_skl)) ),
inference(resolution,[status(thm)],[f18733,f410]) ).
fof(f19141,plain,
( k1_realset1(u2_lattices(sK0_skl),k17_filter_2(sK0_skl)) = u2_lattices(sK0_skl)
| ~ v1_relat_1(u2_lattices(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f1018,f19138]) ).
fof(f19142,plain,
k1_realset1(u2_lattices(sK0_skl),k17_filter_2(sK0_skl)) = u2_lattices(sK0_skl),
inference(forward_subsumption_resolution,[status(thm)],[f19141,f1015]) ).
fof(f19143,plain,
( sK1_skl(k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl),sK0_skl) = u2_lattices(sK0_skl)
| v1_xboole_0(k17_filter_2(sK0_skl))
| ~ l3_lattices(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f19142,f14505]) ).
fof(f19217,plain,
( sK1_skl(k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl),sK0_skl) = u2_lattices(sK0_skl)
| v1_xboole_0(k17_filter_2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f19143,f105]) ).
fof(f19572,plain,
m1_subset_1(k1_relat_1(u1_lattices(sK0_skl)),k1_zfmisc_1(k2_zfmisc_1(k17_filter_2(sK0_skl),k17_filter_2(sK0_skl)))),
inference(forward_demodulation,[status(thm)],[f3567,f3570]) ).
fof(f19579,plain,
r1_tarski(k1_relat_1(u1_lattices(sK0_skl)),k2_zfmisc_1(k17_filter_2(sK0_skl),k17_filter_2(sK0_skl))),
inference(resolution,[status(thm)],[f19572,f392]) ).
fof(f19805,plain,
( k7_relat_1(u1_lattices(sK0_skl),k2_zfmisc_1(k17_filter_2(sK0_skl),k17_filter_2(sK0_skl))) = u1_lattices(sK0_skl)
| ~ v1_relat_1(u1_lattices(sK0_skl)) ),
inference(resolution,[status(thm)],[f19579,f410]) ).
fof(f19808,plain,
( k1_realset1(u1_lattices(sK0_skl),k17_filter_2(sK0_skl)) = u1_lattices(sK0_skl)
| ~ v1_relat_1(u1_lattices(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f1367,f19805]) ).
fof(f19809,plain,
k1_realset1(u1_lattices(sK0_skl),k17_filter_2(sK0_skl)) = u1_lattices(sK0_skl),
inference(forward_subsumption_resolution,[status(thm)],[f19808,f1362]) ).
fof(f19810,plain,
( sK2_skl(k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl),sK0_skl) = u1_lattices(sK0_skl)
| v1_xboole_0(k17_filter_2(sK0_skl))
| ~ l3_lattices(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f19809,f14407]) ).
fof(f19944,plain,
( sK2_skl(k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl),sK0_skl) = u1_lattices(sK0_skl)
| v1_xboole_0(k17_filter_2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f19810,f105]) ).
fof(f45653,plain,
( k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)) = g3_lattices(k17_filter_2(sK0_skl),u2_lattices(sK0_skl),sK2_skl(k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl),sK0_skl))
| v1_xboole_0(k17_filter_2(sK0_skl))
| ~ l3_lattices(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f45654,f14032]) ).
fof(f45654,plain,
sK1_skl(k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl),sK0_skl) = u2_lattices(sK0_skl),
inference(forward_subsumption_resolution,[status(thm)],[f19217,f1014]) ).
fof(f45655,plain,
( k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)) = g3_lattices(k17_filter_2(sK0_skl),u2_lattices(sK0_skl),sK2_skl(k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl),sK0_skl))
| v1_xboole_0(k17_filter_2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f45653,f105]) ).
fof(f45749,plain,
sK2_skl(k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)),k17_filter_2(sK0_skl),sK0_skl) = u1_lattices(sK0_skl),
inference(forward_subsumption_resolution,[status(thm)],[f19944,f1014]) ).
fof(f46420,plain,
( k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)) = g3_lattices(k17_filter_2(sK0_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl))
| v1_xboole_0(k17_filter_2(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f45749,f45655]) ).
fof(f46429,plain,
k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)) != k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)),
inference(backward_demodulation,[status(thm)],[f46430,f587]) ).
fof(f46430,plain,
k23_filter_2(sK0_skl,k17_filter_2(sK0_skl)) = g3_lattices(k17_filter_2(sK0_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f46420,f1014]) ).
fof(f46458,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f46429]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT332+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/5.37 % Computer : n001.cluster.edu
% 0.11/5.37 % Model : x86_64 x86_64
% 0.11/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.37 % Memory : 8046.5625MB
% 0.11/5.37 % OS : Linux 6.8.0-71-generic
% 0.11/5.37 % CPULimit : 300
% 0.11/5.37 % WCLimit : 300
% 0.11/5.37 % DateTime : Sun Sep 20 23:46:03 UTC 2026
% 0.11/5.37 % CPUTime :
% 0.11/5.39 % Drodi V4.1.1
% 76.86/15.19 % Refutation found
% 76.86/15.19 % SZS status Theorem for theBenchmark: Theorem is valid
% 76.86/15.19 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.83/15.47 % Elapsed time: 10.081985 seconds
% 4.83/15.47 % CPU time: 78.237410 seconds
% 4.83/15.47 % Total memory used: 471.469 MB
% 4.83/15.47 % Net memory used: 445.028 MB
%------------------------------------------------------------------------------