%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT331+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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 24.95s 3.59s
% Output : CNFRefutation 24.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 35
% Syntax : Number of formulae : 193 ( 36 unt; 26 def)
% Number of atoms : 739 ( 100 equ)
% Maximal formula atoms : 27 ( 3 avg)
% Number of connectives : 902 ( 356 ~; 395 |; 100 &)
% ( 31 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 39 ( 37 usr; 27 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 4 con; 0-3 aty)
% Number of variables : 141 ( 131 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l3_lattices(B)
& v10_lattices(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( m1_filter_2(C,A)
=> ! [D] :
( m1_filter_2(D,B)
=> ( ( C = D
& g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) = g3_lattices(u1_struct_0(B),u2_lattices(B),u1_lattices(B)) )
=> k8_filter_0(A,C) = k8_filter_0(B,D) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l3_lattices(B)
& v10_lattices(B)
& ~ v3_struct_0(B) )
=> ! [C] :
( m1_filter_2(C,A)
=> ! [D] :
( m1_filter_2(D,B)
=> ( ( C = D
& g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) = g3_lattices(u1_struct_0(B),u2_lattices(B),u1_lattices(B)) )
=> k8_filter_0(A,C) = k8_filter_0(B,D) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f10,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_filter_0(B,A)
=> ! [C] :
( ( l3_lattices(C)
& v10_lattices(C)
& ~ v3_struct_0(C) )
=> ( C = k8_filter_0(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/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [A,B] :
( ( m1_filter_0(B,A)
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( l3_lattices(k8_filter_0(A,B))
& v10_lattices(k8_filter_0(A,B))
& ~ v3_struct_0(k8_filter_0(A,B)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [A] :
( l3_lattices(A)
=> ( l2_lattices(A)
& l1_lattices(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,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/sandbox/benchmark/theBenchmark.p') ).
fof(f31,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/sandbox/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [A,B,C] :
( ( m1_relset_1(C,k2_zfmisc_1(A,A),A)
& v1_funct_2(C,k2_zfmisc_1(A,A),A)
& v1_funct_1(C)
& m1_relset_1(B,k2_zfmisc_1(A,A),A)
& v1_funct_2(B,k2_zfmisc_1(A,A),A)
& v1_funct_1(B) )
=> ! [D,E,F] :
( g3_lattices(A,B,C) = g3_lattices(D,E,F)
=> ( C = F
& B = E
& A = D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f69,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_filter_2(B,A)
<=> m1_filter_0(B,A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f70,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f80,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( k8_filter_0(A,C) != k8_filter_0(B,D)
& C = D
& g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) = g3_lattices(u1_struct_0(B),u2_lattices(B),u1_lattices(B))
& m1_filter_2(D,B) )
& m1_filter_2(C,A) )
& l3_lattices(B)
& v10_lattices(B)
& ~ v3_struct_0(B) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f81,plain,
( k8_filter_0(sK0_skl,sK2_skl) != k8_filter_0(sK1_skl,sK3_skl)
& sK2_skl = sK3_skl
& g3_lattices(u1_struct_0(sK0_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl)) = g3_lattices(u1_struct_0(sK1_skl),u2_lattices(sK1_skl),u1_lattices(sK1_skl))
& m1_filter_2(sK3_skl,sK1_skl)
& m1_filter_2(sK2_skl,sK0_skl)
& l3_lattices(sK1_skl)
& v10_lattices(sK1_skl)
& ~ v3_struct_0(sK1_skl)
& l3_lattices(sK0_skl)
& v10_lattices(sK0_skl)
& ~ v3_struct_0(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl),skolemize(D,sK3_skl)],[f80]) ).
fof(f82,plain,
~ v3_struct_0(sK0_skl),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f83,plain,
v10_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f84,plain,
l3_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f85,plain,
~ v3_struct_0(sK1_skl),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f86,plain,
v10_lattices(sK1_skl),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f87,plain,
l3_lattices(sK1_skl),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f88,plain,
m1_filter_2(sK2_skl,sK0_skl),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f89,plain,
m1_filter_2(sK3_skl,sK1_skl),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f90,plain,
g3_lattices(u1_struct_0(sK0_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl)) = g3_lattices(u1_struct_0(sK1_skl),u2_lattices(sK1_skl),u1_lattices(sK1_skl)),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f91,plain,
sK2_skl = sK3_skl,
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f92,plain,
k8_filter_0(sK0_skl,sK2_skl) != k8_filter_0(sK1_skl,sK3_skl),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f117,plain,
! [A] :
( ! [B] :
( ! [C] :
( ( C = k8_filter_0(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) ) )
| ~ l3_lattices(C)
| ~ v10_lattices(C)
| v3_struct_0(C) )
| ~ m1_filter_0(B,A) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f118,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 = k8_filter_0(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 != k8_filter_0(A,B) ) )
| ~ l3_lattices(C)
| ~ v10_lattices(C)
| v3_struct_0(C) )
| ~ m1_filter_0(B,A) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f117]) ).
fof(f119,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 = k8_filter_0(A,B) )
& ( ( C = g3_lattices(B,sK4_skl(C,B,A),sK5_skl(C,B,A))
& sK5_skl(C,B,A) = k1_realset1(u1_lattices(A),B)
& sK4_skl(C,B,A) = k1_realset1(u2_lattices(A),B)
& m2_relset_1(sK5_skl(C,B,A),k2_zfmisc_1(B,B),B)
& v1_funct_2(sK5_skl(C,B,A),k2_zfmisc_1(B,B),B)
& v1_funct_1(sK5_skl(C,B,A))
& m2_relset_1(sK4_skl(C,B,A),k2_zfmisc_1(B,B),B)
& v1_funct_2(sK4_skl(C,B,A),k2_zfmisc_1(B,B),B)
& v1_funct_1(sK4_skl(C,B,A)) )
| C != k8_filter_0(A,B) ) )
| ~ l3_lattices(C)
| ~ v10_lattices(C)
| v3_struct_0(C) )
| ~ m1_filter_0(B,A) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl]),skolemize(D,sK4_skl(C,B,A)),skolemize(E,sK5_skl(C,B,A))],[f118]) ).
fof(f126,plain,
! [X0,X1,X2] :
( sK4_skl(X2,X1,X0) = k1_realset1(u2_lattices(X0),X1)
| X2 != k8_filter_0(X0,X1)
| ~ l3_lattices(X2)
| ~ v10_lattices(X2)
| v3_struct_0(X2)
| ~ m1_filter_0(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f127,plain,
! [X0,X1,X2] :
( sK5_skl(X2,X1,X0) = k1_realset1(u1_lattices(X0),X1)
| X2 != k8_filter_0(X0,X1)
| ~ l3_lattices(X2)
| ~ v10_lattices(X2)
| v3_struct_0(X2)
| ~ m1_filter_0(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f128,plain,
! [X0,X1,X2] :
( X2 = g3_lattices(X1,sK4_skl(X2,X1,X0),sK5_skl(X2,X1,X0))
| X2 != k8_filter_0(X0,X1)
| ~ l3_lattices(X2)
| ~ v10_lattices(X2)
| v3_struct_0(X2)
| ~ m1_filter_0(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f138,plain,
! [A,B] :
( ( l3_lattices(k8_filter_0(A,B))
& v10_lattices(k8_filter_0(A,B))
& ~ v3_struct_0(k8_filter_0(A,B)) )
| ~ m1_filter_0(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f139,plain,
! [X0,X1] :
( ~ v3_struct_0(k8_filter_0(X0,X1))
| ~ m1_filter_0(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f140,plain,
! [X0,X1] :
( v10_lattices(k8_filter_0(X0,X1))
| ~ m1_filter_0(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f141,plain,
! [X0,X1] :
( l3_lattices(k8_filter_0(X0,X1))
| ~ m1_filter_0(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f146,plain,
! [A] :
( ( l2_lattices(A)
& l1_lattices(A) )
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f147,plain,
! [X0] :
( l1_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f148,plain,
! [X0] :
( l2_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f159,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)],[f29]) ).
fof(f160,plain,
! [X0] :
( v1_funct_1(u1_lattices(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f161,plain,
! [X0] :
( v1_funct_2(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)],[f159]) ).
fof(f162,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)],[f159]) ).
fof(f163,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)],[f31]) ).
fof(f164,plain,
! [X0] :
( v1_funct_1(u2_lattices(X0))
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f165,plain,
! [X0] :
( v1_funct_2(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)],[f163]) ).
fof(f166,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)],[f163]) ).
fof(f244,plain,
! [A,B,C] :
( ! [D,E,F] :
( ( C = F
& B = E
& A = D )
| g3_lattices(A,B,C) != g3_lattices(D,E,F) )
| ~ m1_relset_1(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_1(C)
| ~ m1_relset_1(B,k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(B,k2_zfmisc_1(A,A),A)
| ~ v1_funct_1(B) ),
inference(pre_NNF_transformation,[status(thm)],[f55]) ).
fof(f246,plain,
! [X0,X1,X2,X3,X4,X5] :
( X0 = X4
| g3_lattices(X1,X0,X2) != g3_lattices(X3,X4,X5)
| ~ m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X0,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X0) ),
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f247,plain,
! [X0,X1,X2,X3,X4,X5] :
( X2 = X5
| g3_lattices(X1,X0,X2) != g3_lattices(X3,X4,X5)
| ~ m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X0,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X0) ),
inference(cnf_transformation,[status(thm)],[f244]) ).
fof(f299,plain,
! [A] :
( ! [B] :
( m1_filter_2(B,A)
<=> m1_filter_0(B,A) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f69]) ).
fof(f300,plain,
! [A] :
( ! [B] :
( ( ~ m1_filter_0(B,A)
| m1_filter_2(B,A) )
& ( m1_filter_0(B,A)
| ~ m1_filter_2(B,A) ) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f299]) ).
fof(f301,plain,
! [A] :
( ( ! [B] :
( ~ m1_filter_0(B,A)
| m1_filter_2(B,A) )
& ! [B] :
( m1_filter_0(B,A)
| ~ m1_filter_2(B,A) ) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(miniscoping,[status(thm)],[f300]) ).
fof(f302,plain,
! [X0,X1] :
( m1_filter_0(X1,X0)
| ~ m1_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f301]) ).
fof(f304,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)],[f70]) ).
fof(f305,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)],[f304]) ).
fof(f306,plain,
! [X0,X1,X2] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f305]) ).
fof(f332,plain,
m1_filter_2(sK2_skl,sK1_skl),
inference(backward_demodulation,[status(thm)],[f91,f89]) ).
fof(f333,plain,
k8_filter_0(sK0_skl,sK2_skl) != k8_filter_0(sK1_skl,sK2_skl),
inference(forward_demodulation,[status(thm)],[f91,f92]) ).
fof(f341,plain,
! [X0,X1] :
( sK4_skl(k8_filter_0(X0,X1),X1,X0) = k1_realset1(u2_lattices(X0),X1)
| ~ l3_lattices(k8_filter_0(X0,X1))
| ~ v10_lattices(k8_filter_0(X0,X1))
| v3_struct_0(k8_filter_0(X0,X1))
| ~ m1_filter_0(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f126]) ).
fof(f342,plain,
! [X0,X1] :
( sK5_skl(k8_filter_0(X0,X1),X1,X0) = k1_realset1(u1_lattices(X0),X1)
| ~ l3_lattices(k8_filter_0(X0,X1))
| ~ v10_lattices(k8_filter_0(X0,X1))
| v3_struct_0(k8_filter_0(X0,X1))
| ~ m1_filter_0(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f127]) ).
fof(f343,plain,
! [X0,X1] :
( k8_filter_0(X0,X1) = g3_lattices(X1,sK4_skl(k8_filter_0(X0,X1),X1,X0),sK5_skl(k8_filter_0(X0,X1),X1,X0))
| ~ l3_lattices(k8_filter_0(X0,X1))
| ~ v10_lattices(k8_filter_0(X0,X1))
| v3_struct_0(k8_filter_0(X0,X1))
| ~ m1_filter_0(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f128]) ).
fof(f345,plain,
! [X0,X1] :
( k8_filter_0(X0,X1) = g3_lattices(X1,sK4_skl(k8_filter_0(X0,X1),X1,X0),sK5_skl(k8_filter_0(X0,X1),X1,X0))
| ~ l3_lattices(k8_filter_0(X0,X1))
| ~ v10_lattices(k8_filter_0(X0,X1))
| ~ m1_filter_0(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f343,f139]) ).
fof(f346,plain,
! [X0,X1] :
( sK5_skl(k8_filter_0(X0,X1),X1,X0) = k1_realset1(u1_lattices(X0),X1)
| ~ l3_lattices(k8_filter_0(X0,X1))
| ~ v10_lattices(k8_filter_0(X0,X1))
| ~ m1_filter_0(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f342,f139]) ).
fof(f347,plain,
! [X0,X1] :
( sK4_skl(k8_filter_0(X0,X1),X1,X0) = k1_realset1(u2_lattices(X0),X1)
| ~ l3_lattices(k8_filter_0(X0,X1))
| ~ v10_lattices(k8_filter_0(X0,X1))
| ~ m1_filter_0(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f341,f139]) ).
fof(f354,plain,
! [X0,X1] :
( k8_filter_0(X0,X1) = g3_lattices(X1,sK4_skl(k8_filter_0(X0,X1),X1,X0),sK5_skl(k8_filter_0(X0,X1),X1,X0))
| ~ l3_lattices(k8_filter_0(X0,X1))
| ~ m1_filter_0(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f345,f140]) ).
fof(f355,plain,
! [X0,X1] :
( sK5_skl(k8_filter_0(X0,X1),X1,X0) = k1_realset1(u1_lattices(X0),X1)
| ~ l3_lattices(k8_filter_0(X0,X1))
| ~ m1_filter_0(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f346,f140]) ).
fof(f356,plain,
! [X0,X1] :
( sK4_skl(k8_filter_0(X0,X1),X1,X0) = k1_realset1(u2_lattices(X0),X1)
| ~ l3_lattices(k8_filter_0(X0,X1))
| ~ m1_filter_0(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f347,f140]) ).
fof(f367,definition,
( sQ0_spl
<=> v3_struct_0(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f368,plain,
( ~ sQ0_spl
| v3_struct_0(sK1_skl) ),
inference(component_clause,[status(thm)],[f367]) ).
fof(f370,definition,
( sQ1_spl
<=> l3_lattices(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f372,plain,
( sQ1_spl
| ~ l3_lattices(sK1_skl) ),
inference(component_clause,[status(thm)],[f370]) ).
fof(f377,definition,
( sQ3_spl
<=> v3_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f378,plain,
( ~ sQ3_spl
| v3_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f377]) ).
fof(f380,definition,
( sQ4_spl
<=> l3_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f382,plain,
( sQ4_spl
| ~ l3_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f380]) ).
fof(f387,definition,
( sQ6_spl
<=> v10_lattices(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f389,plain,
( sQ6_spl
| ~ v10_lattices(sK1_skl) ),
inference(component_clause,[status(thm)],[f387]) ).
fof(f391,definition,
( sQ7_spl
<=> v10_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f393,plain,
( sQ7_spl
| ~ v10_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f391]) ).
fof(f395,plain,
( ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f378,f82]) ).
fof(f396,plain,
~ sQ3_spl,
inference(contradiction_clause,[status(thm)],[f395]) ).
fof(f408,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f368,f85]) ).
fof(f409,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f408]) ).
fof(f476,plain,
l1_lattices(sK0_skl),
inference(resolution,[status(thm)],[f147,f84]) ).
fof(f482,plain,
l2_lattices(sK0_skl),
inference(resolution,[status(thm)],[f148,f84]) ).
fof(f543,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f393,f83]) ).
fof(f544,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f543]) ).
fof(f545,plain,
( sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f389,f86]) ).
fof(f546,plain,
sQ6_spl,
inference(contradiction_clause,[status(thm)],[f545]) ).
fof(f639,definition,
( sQ47_spl
<=> v1_funct_1(u2_lattices(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f641,plain,
( sQ47_spl
| ~ v1_funct_1(u2_lattices(sK0_skl)) ),
inference(component_clause,[status(thm)],[f639]) ).
fof(f642,definition,
( sQ48_spl
<=> v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f644,plain,
( sQ48_spl
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f642]) ).
fof(f645,definition,
( sQ49_spl
<=> m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f647,plain,
( sQ49_spl
| ~ m1_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(component_clause,[status(thm)],[f645]) ).
fof(f648,definition,
( sQ50_spl
<=> v1_funct_1(u1_lattices(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f650,plain,
( sQ50_spl
| ~ v1_funct_1(u1_lattices(sK0_skl)) ),
inference(component_clause,[status(thm)],[f648]) ).
fof(f651,definition,
( sQ51_spl
<=> v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f653,plain,
( sQ51_spl
| ~ v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f651]) ).
fof(f654,definition,
( sQ52_spl
<=> m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f656,plain,
( sQ52_spl
| ~ m1_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(component_clause,[status(thm)],[f654]) ).
fof(f681,plain,
v1_funct_2(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)],[f161,f476]) ).
fof(f688,plain,
v1_funct_2(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)],[f165,f482]) ).
fof(f829,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f382,f84]) ).
fof(f830,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f829]) ).
fof(f831,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f372,f87]) ).
fof(f832,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f831]) ).
fof(f834,plain,
! [X0] :
( m1_filter_0(X0,sK1_skl)
| ~ m1_filter_2(X0,sK1_skl)
| ~ l3_lattices(sK1_skl)
| v3_struct_0(sK1_skl) ),
inference(resolution,[status(thm)],[f302,f86]) ).
fof(f835,plain,
! [X0] :
( m1_filter_0(X0,sK0_skl)
| ~ m1_filter_2(X0,sK0_skl)
| ~ l3_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f302,f83]) ).
fof(f846,definition,
! [X0] :
( sQ80_spl
<=> ( m1_filter_0(X0,sK1_skl)
| ~ m1_filter_2(X0,sK1_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f847,plain,
! [X0] :
( ~ sQ80_spl
| m1_filter_0(X0,sK1_skl)
| ~ m1_filter_2(X0,sK1_skl) ),
inference(component_clause,[status(thm)],[f846]) ).
fof(f849,plain,
( sQ80_spl
| ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f834,f367,f370,f846]) ).
fof(f850,definition,
! [X0] :
( sQ81_spl
<=> ( m1_filter_0(X0,sK0_skl)
| ~ m1_filter_2(X0,sK0_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f851,plain,
! [X0] :
( ~ sQ81_spl
| m1_filter_0(X0,sK0_skl)
| ~ m1_filter_2(X0,sK0_skl) ),
inference(component_clause,[status(thm)],[f850]) ).
fof(f853,plain,
( sQ81_spl
| ~ sQ4_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f835,f377,f380,f850]) ).
fof(f869,plain,
( u2_lattices(sK0_skl) = u2_lattices(sK1_skl)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))
| ~ v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))
| ~ v1_funct_1(u1_lattices(sK0_skl))
| ~ m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))
| ~ v1_funct_1(u2_lattices(sK0_skl)) ),
inference(resolution,[status(thm)],[f246,f90]) ).
fof(f874,definition,
( sQ85_spl
<=> u2_lattices(sK0_skl) = u2_lattices(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f875,plain,
( ~ sQ85_spl
| u2_lattices(sK0_skl) = u2_lattices(sK1_skl) ),
inference(component_clause,[status(thm)],[f874]) ).
fof(f877,plain,
( sQ85_spl
| ~ sQ52_spl
| ~ sQ51_spl
| ~ sQ50_spl
| ~ sQ49_spl
| ~ sQ48_spl
| ~ sQ47_spl ),
inference(split_clause,[status(thm)],[f869,f639,f642,f645,f648,f651,f654,f874]) ).
fof(f902,definition,
( sQ87_spl
<=> u1_lattices(sK0_skl) = u1_lattices(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f903,plain,
( ~ sQ87_spl
| u1_lattices(sK0_skl) = u1_lattices(sK1_skl) ),
inference(component_clause,[status(thm)],[f902]) ).
fof(f930,plain,
( u1_lattices(sK0_skl) = u1_lattices(sK1_skl)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))
| ~ v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))
| ~ v1_funct_1(u1_lattices(sK0_skl))
| ~ m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))
| ~ v1_funct_1(u2_lattices(sK0_skl)) ),
inference(resolution,[status(thm)],[f90,f247]) ).
fof(f943,plain,
( sQ87_spl
| ~ sQ52_spl
| ~ sQ51_spl
| ~ sQ50_spl
| ~ sQ49_spl
| ~ sQ48_spl
| ~ sQ47_spl ),
inference(split_clause,[status(thm)],[f930,f639,f642,f645,f648,f651,f654,f902]) ).
fof(f1004,plain,
( sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f653,f681]) ).
fof(f1005,plain,
sQ51_spl,
inference(contradiction_clause,[status(thm)],[f1004]) ).
fof(f1006,plain,
( sQ48_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f644,f688]) ).
fof(f1007,plain,
sQ48_spl,
inference(contradiction_clause,[status(thm)],[f1006]) ).
fof(f1100,plain,
( ~ sQ81_spl
| m1_filter_0(sK2_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f851,f88]) ).
fof(f1101,plain,
( ~ sQ81_spl
| l3_lattices(k8_filter_0(sK0_skl,sK2_skl))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f1100,f141]) ).
fof(f1103,definition,
( sQ121_spl
<=> l3_lattices(k8_filter_0(sK0_skl,sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f1104,plain,
( ~ sQ121_spl
| l3_lattices(k8_filter_0(sK0_skl,sK2_skl)) ),
inference(component_clause,[status(thm)],[f1103]) ).
fof(f1106,plain,
( ~ sQ81_spl
| sQ121_spl
| ~ sQ4_spl
| ~ sQ7_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f1101,f377,f391,f380,f1103,f850]) ).
fof(f1168,definition,
( sQ133_spl
<=> m1_filter_0(sK2_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f1170,plain,
( sQ133_spl
| ~ m1_filter_0(sK2_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f1168]) ).
fof(f1172,plain,
( sQ133_spl
| ~ sQ81_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1170,f1100]) ).
fof(f1173,plain,
( sQ133_spl
| ~ sQ81_spl ),
inference(contradiction_clause,[status(thm)],[f1172]) ).
fof(f1219,plain,
( ~ sQ121_spl
| k8_filter_0(sK0_skl,sK2_skl) = g3_lattices(sK2_skl,sK4_skl(k8_filter_0(sK0_skl,sK2_skl),sK2_skl,sK0_skl),sK5_skl(k8_filter_0(sK0_skl,sK2_skl),sK2_skl,sK0_skl))
| ~ m1_filter_0(sK2_skl,sK0_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f354,f1104]) ).
fof(f1220,definition,
( sQ141_spl
<=> k8_filter_0(sK0_skl,sK2_skl) = g3_lattices(sK2_skl,sK4_skl(k8_filter_0(sK0_skl,sK2_skl),sK2_skl,sK0_skl),sK5_skl(k8_filter_0(sK0_skl,sK2_skl),sK2_skl,sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f1221,plain,
( ~ sQ141_spl
| k8_filter_0(sK0_skl,sK2_skl) = g3_lattices(sK2_skl,sK4_skl(k8_filter_0(sK0_skl,sK2_skl),sK2_skl,sK0_skl),sK5_skl(k8_filter_0(sK0_skl,sK2_skl),sK2_skl,sK0_skl)) ),
inference(component_clause,[status(thm)],[f1220]) ).
fof(f1223,plain,
( ~ sQ121_spl
| sQ141_spl
| ~ sQ133_spl
| ~ sQ4_spl
| ~ sQ7_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f1219,f377,f391,f380,f1168,f1220,f1103]) ).
fof(f1296,plain,
( ~ sQ80_spl
| m1_filter_0(sK2_skl,sK1_skl) ),
inference(resolution,[status(thm)],[f847,f332]) ).
fof(f1297,plain,
( ~ sQ80_spl
| l3_lattices(k8_filter_0(sK1_skl,sK2_skl))
| ~ l3_lattices(sK1_skl)
| ~ v10_lattices(sK1_skl)
| v3_struct_0(sK1_skl) ),
inference(resolution,[status(thm)],[f1296,f141]) ).
fof(f1299,definition,
( sQ153_spl
<=> l3_lattices(k8_filter_0(sK1_skl,sK2_skl)) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f1300,plain,
( ~ sQ153_spl
| l3_lattices(k8_filter_0(sK1_skl,sK2_skl)) ),
inference(component_clause,[status(thm)],[f1299]) ).
fof(f1302,plain,
( ~ sQ80_spl
| sQ153_spl
| ~ sQ1_spl
| ~ sQ6_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1297,f367,f387,f370,f1299,f846]) ).
fof(f1307,plain,
( ~ sQ153_spl
| k8_filter_0(sK1_skl,sK2_skl) = g3_lattices(sK2_skl,sK4_skl(k8_filter_0(sK1_skl,sK2_skl),sK2_skl,sK1_skl),sK5_skl(k8_filter_0(sK1_skl,sK2_skl),sK2_skl,sK1_skl))
| ~ m1_filter_0(sK2_skl,sK1_skl)
| ~ l3_lattices(sK1_skl)
| ~ v10_lattices(sK1_skl)
| v3_struct_0(sK1_skl) ),
inference(resolution,[status(thm)],[f1300,f354]) ).
fof(f1320,definition,
( sQ155_spl
<=> m1_filter_0(sK2_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f1322,plain,
( sQ155_spl
| ~ m1_filter_0(sK2_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f1320]) ).
fof(f1323,definition,
( sQ156_spl
<=> k8_filter_0(sK1_skl,sK2_skl) = g3_lattices(sK2_skl,sK4_skl(k8_filter_0(sK1_skl,sK2_skl),sK2_skl,sK1_skl),sK5_skl(k8_filter_0(sK1_skl,sK2_skl),sK2_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition]) ).
fof(f1324,plain,
( ~ sQ156_spl
| k8_filter_0(sK1_skl,sK2_skl) = g3_lattices(sK2_skl,sK4_skl(k8_filter_0(sK1_skl,sK2_skl),sK2_skl,sK1_skl),sK5_skl(k8_filter_0(sK1_skl,sK2_skl),sK2_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f1323]) ).
fof(f1326,plain,
( ~ sQ153_spl
| sQ156_spl
| ~ sQ155_spl
| ~ sQ1_spl
| ~ sQ6_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1307,f367,f387,f370,f1320,f1323,f1299]) ).
fof(f1370,plain,
( sQ155_spl
| ~ sQ80_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1322,f1296]) ).
fof(f1371,plain,
( sQ155_spl
| ~ sQ80_spl ),
inference(contradiction_clause,[status(thm)],[f1370]) ).
fof(f1372,plain,
( ~ sQ153_spl
| sK5_skl(k8_filter_0(sK1_skl,sK2_skl),sK2_skl,sK1_skl) = k1_realset1(u1_lattices(sK1_skl),sK2_skl)
| ~ m1_filter_0(sK2_skl,sK1_skl)
| ~ l3_lattices(sK1_skl)
| ~ v10_lattices(sK1_skl)
| v3_struct_0(sK1_skl) ),
inference(resolution,[status(thm)],[f355,f1300]) ).
fof(f1373,plain,
( ~ sQ121_spl
| sK5_skl(k8_filter_0(sK0_skl,sK2_skl),sK2_skl,sK0_skl) = k1_realset1(u1_lattices(sK0_skl),sK2_skl)
| ~ m1_filter_0(sK2_skl,sK0_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f355,f1104]) ).
fof(f1374,definition,
( sQ168_spl
<=> sK5_skl(k8_filter_0(sK1_skl,sK2_skl),sK2_skl,sK1_skl) = k1_realset1(u1_lattices(sK1_skl),sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f1375,plain,
( ~ sQ168_spl
| sK5_skl(k8_filter_0(sK1_skl,sK2_skl),sK2_skl,sK1_skl) = k1_realset1(u1_lattices(sK1_skl),sK2_skl) ),
inference(component_clause,[status(thm)],[f1374]) ).
fof(f1377,plain,
( ~ sQ153_spl
| sQ168_spl
| ~ sQ155_spl
| ~ sQ1_spl
| ~ sQ6_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1372,f367,f387,f370,f1320,f1374,f1299]) ).
fof(f1378,definition,
( sQ169_spl
<=> sK5_skl(k8_filter_0(sK0_skl,sK2_skl),sK2_skl,sK0_skl) = k1_realset1(u1_lattices(sK0_skl),sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f1379,plain,
( ~ sQ169_spl
| sK5_skl(k8_filter_0(sK0_skl,sK2_skl),sK2_skl,sK0_skl) = k1_realset1(u1_lattices(sK0_skl),sK2_skl) ),
inference(component_clause,[status(thm)],[f1378]) ).
fof(f1381,plain,
( ~ sQ121_spl
| sQ169_spl
| ~ sQ133_spl
| ~ sQ4_spl
| ~ sQ7_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f1373,f377,f391,f380,f1168,f1378,f1103]) ).
fof(f1382,plain,
( ~ sQ141_spl
| ~ sQ169_spl
| k8_filter_0(sK0_skl,sK2_skl) = g3_lattices(sK2_skl,sK4_skl(k8_filter_0(sK0_skl,sK2_skl),sK2_skl,sK0_skl),k1_realset1(u1_lattices(sK0_skl),sK2_skl)) ),
inference(backward_demodulation,[status(thm)],[f1379,f1221]) ).
fof(f1383,plain,
( ~ sQ156_spl
| ~ sQ168_spl
| k8_filter_0(sK1_skl,sK2_skl) = g3_lattices(sK2_skl,sK4_skl(k8_filter_0(sK1_skl,sK2_skl),sK2_skl,sK1_skl),k1_realset1(u1_lattices(sK1_skl),sK2_skl)) ),
inference(backward_demodulation,[status(thm)],[f1375,f1324]) ).
fof(f1384,plain,
( ~ sQ153_spl
| sK4_skl(k8_filter_0(sK1_skl,sK2_skl),sK2_skl,sK1_skl) = k1_realset1(u2_lattices(sK1_skl),sK2_skl)
| ~ m1_filter_0(sK2_skl,sK1_skl)
| ~ l3_lattices(sK1_skl)
| ~ v10_lattices(sK1_skl)
| v3_struct_0(sK1_skl) ),
inference(resolution,[status(thm)],[f356,f1300]) ).
fof(f1385,plain,
( ~ sQ121_spl
| sK4_skl(k8_filter_0(sK0_skl,sK2_skl),sK2_skl,sK0_skl) = k1_realset1(u2_lattices(sK0_skl),sK2_skl)
| ~ m1_filter_0(sK2_skl,sK0_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f356,f1104]) ).
fof(f1386,definition,
( sQ170_spl
<=> sK4_skl(k8_filter_0(sK1_skl,sK2_skl),sK2_skl,sK1_skl) = k1_realset1(u2_lattices(sK1_skl),sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f1387,plain,
( ~ sQ170_spl
| sK4_skl(k8_filter_0(sK1_skl,sK2_skl),sK2_skl,sK1_skl) = k1_realset1(u2_lattices(sK1_skl),sK2_skl) ),
inference(component_clause,[status(thm)],[f1386]) ).
fof(f1389,plain,
( ~ sQ153_spl
| sQ170_spl
| ~ sQ155_spl
| ~ sQ1_spl
| ~ sQ6_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f1384,f367,f387,f370,f1320,f1386,f1299]) ).
fof(f1390,definition,
( sQ171_spl
<=> sK4_skl(k8_filter_0(sK0_skl,sK2_skl),sK2_skl,sK0_skl) = k1_realset1(u2_lattices(sK0_skl),sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ171_spl])],[split_symbol_definition]) ).
fof(f1391,plain,
( ~ sQ171_spl
| sK4_skl(k8_filter_0(sK0_skl,sK2_skl),sK2_skl,sK0_skl) = k1_realset1(u2_lattices(sK0_skl),sK2_skl) ),
inference(component_clause,[status(thm)],[f1390]) ).
fof(f1393,plain,
( ~ sQ121_spl
| sQ171_spl
| ~ sQ133_spl
| ~ sQ4_spl
| ~ sQ7_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f1385,f377,f391,f380,f1168,f1390,f1103]) ).
fof(f1394,plain,
( ~ sQ141_spl
| ~ sQ169_spl
| ~ sQ171_spl
| k8_filter_0(sK0_skl,sK2_skl) = g3_lattices(sK2_skl,k1_realset1(u2_lattices(sK0_skl),sK2_skl),k1_realset1(u1_lattices(sK0_skl),sK2_skl)) ),
inference(backward_demodulation,[status(thm)],[f1391,f1382]) ).
fof(f1395,plain,
( ~ sQ156_spl
| ~ sQ168_spl
| ~ sQ170_spl
| k8_filter_0(sK1_skl,sK2_skl) = g3_lattices(sK2_skl,k1_realset1(u2_lattices(sK1_skl),sK2_skl),k1_realset1(u1_lattices(sK1_skl),sK2_skl)) ),
inference(backward_demodulation,[status(thm)],[f1387,f1383]) ).
fof(f1769,plain,
v1_funct_1(u1_lattices(sK0_skl)),
inference(resolution,[status(thm)],[f160,f476]) ).
fof(f1784,plain,
v1_funct_1(u2_lattices(sK0_skl)),
inference(resolution,[status(thm)],[f164,f482]) ).
fof(f1790,plain,
( sQ47_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1784,f641]) ).
fof(f1791,plain,
sQ47_spl,
inference(contradiction_clause,[status(thm)],[f1790]) ).
fof(f1856,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)],[f162,f476]) ).
fof(f1913,plain,
( sQ50_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f650,f1769]) ).
fof(f1914,plain,
sQ50_spl,
inference(contradiction_clause,[status(thm)],[f1913]) ).
fof(f1925,plain,
( ~ sQ168_spl
| ~ sQ87_spl
| sK5_skl(k8_filter_0(sK1_skl,sK2_skl),sK2_skl,sK1_skl) = k1_realset1(u1_lattices(sK0_skl),sK2_skl) ),
inference(backward_demodulation,[status(thm)],[f903,f1375]) ).
fof(f2311,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)],[f166,f482]) ).
fof(f5319,plain,
( ~ sQ156_spl
| ~ sQ168_spl
| ~ sQ170_spl
| ~ sQ85_spl
| k8_filter_0(sK1_skl,sK2_skl) = g3_lattices(sK2_skl,k1_realset1(u2_lattices(sK0_skl),sK2_skl),k1_realset1(u1_lattices(sK1_skl),sK2_skl)) ),
inference(backward_demodulation,[status(thm)],[f875,f1395]) ).
fof(f10886,plain,
m1_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)],[f2311,f306]) ).
fof(f10887,plain,
( sQ49_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10886,f647]) ).
fof(f10888,plain,
sQ49_spl,
inference(contradiction_clause,[status(thm)],[f10887]) ).
fof(f10890,plain,
m1_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)],[f1856,f306]) ).
fof(f10891,plain,
( sQ52_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10890,f656]) ).
fof(f10892,plain,
sQ52_spl,
inference(contradiction_clause,[status(thm)],[f10891]) ).
fof(f10897,plain,
( ~ sQ168_spl
| ~ sQ87_spl
| k1_realset1(u1_lattices(sK1_skl),sK2_skl) = k1_realset1(u1_lattices(sK0_skl),sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f1375,f1925]) ).
fof(f11003,plain,
( ~ sQ156_spl
| ~ sQ168_spl
| ~ sQ170_spl
| ~ sQ85_spl
| ~ sQ87_spl
| k8_filter_0(sK1_skl,sK2_skl) = g3_lattices(sK2_skl,k1_realset1(u2_lattices(sK0_skl),sK2_skl),k1_realset1(u1_lattices(sK0_skl),sK2_skl)) ),
inference(forward_demodulation,[status(thm)],[f10897,f5319]) ).
fof(f11004,plain,
( ~ sQ156_spl
| ~ sQ168_spl
| ~ sQ170_spl
| ~ sQ85_spl
| ~ sQ87_spl
| ~ sQ141_spl
| ~ sQ169_spl
| ~ sQ171_spl
| k8_filter_0(sK1_skl,sK2_skl) = k8_filter_0(sK0_skl,sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f1394,f11003]) ).
fof(f11005,plain,
( ~ sQ156_spl
| ~ sQ168_spl
| ~ sQ170_spl
| ~ sQ85_spl
| ~ sQ87_spl
| ~ sQ141_spl
| ~ sQ169_spl
| ~ sQ171_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11004,f333]) ).
fof(f11006,plain,
( ~ sQ156_spl
| ~ sQ168_spl
| ~ sQ170_spl
| ~ sQ85_spl
| ~ sQ87_spl
| ~ sQ141_spl
| ~ sQ169_spl
| ~ sQ171_spl ),
inference(contradiction_clause,[status(thm)],[f11005]) ).
fof(f11007,plain,
$false,
inference(sat_refutation,[status(thm)],[f396,f409,f544,f546,f830,f832,f849,f853,f877,f943,f1005,f1007,f1106,f1173,f1223,f1302,f1326,f1371,f1377,f1381,f1389,f1393,f1791,f1914,f10888,f10892,f11006]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT331+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n018.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 20 23:41:58 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.37 % Drodi V4.1.1
% 24.95/3.59 % Refutation found
% 24.95/3.59 % SZS status Theorem for theBenchmark: Theorem is valid
% 24.95/3.59 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 16.40/3.90 % Elapsed time: 3.530497 seconds
% 16.40/3.90 % CPU time: 26.025908 seconds
% 16.40/3.90 % Total memory used: 413.745 MB
% 16.40/3.90 % Net memory used: 390.440 MB
%------------------------------------------------------------------------------