%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT322+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 : n016.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:44 PM UTC 2026
% Result : Theorem 47.11s 16.65s
% Output : CNFRefutation 48.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 50
% Number of leaves : 25
% Syntax : Number of formulae : 310 ( 67 unt; 0 def)
% Number of atoms : 1156 ( 165 equ)
% Maximal formula atoms : 20 ( 3 avg)
% Number of connectives : 1443 ( 597 ~; 665 |; 134 &)
% ( 11 <=>; 35 =>; 0 <=; 1 <~>)
% Maximal formula depth : 21 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 35 ( 33 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 2 con; 0-3 aty)
% Number of variables : 253 ( 249 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( ( v1_filter_2(B,A)
& B != k17_filter_2(A) )
<=> r2_filter_2(A,B) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( ( v1_filter_2(B,A)
& B != k17_filter_2(A) )
<=> r2_filter_2(A,B) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
! [A] :
( l3_lattices(A)
=> ( v3_lattices(A)
=> A = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k1_filter_0(A) = u1_struct_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [A] :
( l3_lattices(A)
=> k1_lattice2(A) = g3_lattices(u1_struct_0(A),u1_lattices(A),u2_lattices(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
=> k7_filter_2(A,B) = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k17_filter_2(A) = u1_struct_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
! [A,B] :
( ( m2_filter_2(B,A)
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m1_filter_2(k15_filter_2(A,B),k1_lattice2(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> m2_filter_2(k17_filter_2(A),A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [A] :
( l3_lattices(A)
=> ( l3_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [A] :
( l3_lattices(A)
=> ( l2_lattices(A)
& l1_lattices(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,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('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_lattice4(B,A)
=> m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f55,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_struct_0(A) )
=> ( v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f61,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)
& ~ v1_xboole_0(A) )
=> ( v3_lattices(g3_lattices(A,B,C))
& ~ v3_struct_0(g3_lattices(A,B,C)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f62,axiom,
! [A] :
( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v17_lattices(k1_lattice2(A))
& v16_lattices(k1_lattice2(A))
& v15_lattices(k1_lattice2(A))
& v14_lattices(k1_lattice2(A))
& v13_lattices(k1_lattice2(A))
& v12_lattices(k1_lattice2(A))
& v11_lattices(k1_lattice2(A))
& v10_lattices(k1_lattice2(A))
& v9_lattices(k1_lattice2(A))
& v8_lattices(k1_lattice2(A))
& v7_lattices(k1_lattice2(A))
& v6_lattices(k1_lattice2(A))
& v5_lattices(k1_lattice2(A))
& v4_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,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(f85,axiom,
! [A,B] :
( ( m2_filter_2(B,A)
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k15_filter_2(A,B) = k7_filter_2(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f86,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> k1_filter_2(A) = k1_filter_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f87,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(f88,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f92,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( r2_filter_2(A,B)
<=> v1_filter_0(k15_filter_2(A,B),k1_lattice2(A)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f94,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m2_filter_2(B,A)
=> ( v1_filter_2(B,A)
<=> v2_filter_0(k15_filter_2(A,B),k1_lattice2(A)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f96,axiom,
! [A] :
( ( l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_filter_0(B,A)
=> ( ( v2_filter_0(B,A)
& B != k1_filter_0(A) )
<=> v1_filter_0(B,A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f101,plain,
? [A] :
( ? [B] :
( ( ( v1_filter_2(B,A)
& B != k17_filter_2(A) )
<~> r2_filter_2(A,B) )
& m2_filter_2(B,A) )
& l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f102,plain,
? [A] :
( ? [B] :
( ( ~ r2_filter_2(A,B)
| ~ v1_filter_2(B,A)
| B = k17_filter_2(A) )
& ( r2_filter_2(A,B)
| ( v1_filter_2(B,A)
& B != k17_filter_2(A) ) )
& m2_filter_2(B,A) )
& l3_lattices(A)
& v17_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f101]) ).
fof(f103,plain,
( ( ~ r2_filter_2(sK0_skl,sK1_skl)
| ~ v1_filter_2(sK1_skl,sK0_skl)
| sK1_skl = k17_filter_2(sK0_skl) )
& ( r2_filter_2(sK0_skl,sK1_skl)
| ( v1_filter_2(sK1_skl,sK0_skl)
& sK1_skl != k17_filter_2(sK0_skl) ) )
& m2_filter_2(sK1_skl,sK0_skl)
& l3_lattices(sK0_skl)
& v17_lattices(sK0_skl)
& v10_lattices(sK0_skl)
& ~ v3_struct_0(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl)],[f102]) ).
fof(f104,plain,
~ v3_struct_0(sK0_skl),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f105,plain,
v10_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f106,plain,
v17_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f107,plain,
l3_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f108,plain,
m2_filter_2(sK1_skl,sK0_skl),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f109,plain,
( r2_filter_2(sK0_skl,sK1_skl)
| sK1_skl != k17_filter_2(sK0_skl) ),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f110,plain,
( r2_filter_2(sK0_skl,sK1_skl)
| v1_filter_2(sK1_skl,sK0_skl) ),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f111,plain,
( ~ r2_filter_2(sK0_skl,sK1_skl)
| ~ v1_filter_2(sK1_skl,sK0_skl)
| sK1_skl = k17_filter_2(sK0_skl) ),
inference(cnf_transformation,[status(thm)],[f103]) ).
fof(f112,plain,
! [A] :
( A = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A))
| ~ v3_lattices(A)
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f113,plain,
! [X0] :
( X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f163,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)],[f15]) ).
fof(f164,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)],[f163]) ).
fof(f165,plain,
! [A] :
( k1_lattice2(A) = g3_lattices(u1_struct_0(A),u1_lattices(A),u2_lattices(A))
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f166,plain,
! [X0] :
( k1_lattice2(X0) = g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f167,plain,
! [A] :
( ! [B] :
( k7_filter_2(A,B) = B
| ~ m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f168,plain,
! [X0,X1] :
( k7_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f169,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)],[f18]) ).
fof(f170,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)],[f169]) ).
fof(f174,plain,
! [A,B] :
( m1_filter_2(k15_filter_2(A,B),k1_lattice2(A))
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f20]) ).
fof(f175,plain,
! [X0,X1] :
( m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0))
| ~ m2_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f174]) ).
fof(f176,plain,
! [A] :
( m2_filter_2(k17_filter_2(A),A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f21]) ).
fof(f177,plain,
! [X0] :
( m2_filter_2(k17_filter_2(X0),X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f176]) ).
fof(f182,plain,
! [A] :
( ( l3_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A)) )
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f183,plain,
! [X0] :
( v3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f184,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f191,plain,
! [A] :
( ( l2_lattices(A)
& l1_lattices(A) )
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f192,plain,
! [X0] :
( l1_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f193,plain,
! [X0] :
( l2_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f191]) ).
fof(f200,plain,
! [A] :
( ! [B] :
( ( m2_lattice4(B,A)
& ~ v1_xboole_0(B) )
| ~ m2_filter_2(B,A) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f37]) ).
fof(f201,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ m2_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f202,plain,
! [X0,X1] :
( m2_lattice4(X1,X0)
| ~ m2_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f203,plain,
! [A] :
( ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
| ~ m2_lattice4(B,A) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f204,plain,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f203]) ).
fof(f207,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(f208,plain,
! [X0] :
( v1_funct_1(u1_lattices(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f207]) ).
fof(f209,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)],[f207]) ).
fof(f210,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)],[f207]) ).
fof(f211,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(f212,plain,
! [X0] :
( v1_funct_1(u2_lattices(X0))
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f211]) ).
fof(f213,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)],[f211]) ).
fof(f214,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)],[f211]) ).
fof(f243,plain,
! [A] :
( ( v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) )
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f55]) ).
fof(f244,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f243]) ).
fof(f262,plain,
! [A,B,C] :
( ( v3_lattices(g3_lattices(A,B,C))
& ~ v3_struct_0(g3_lattices(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)
| v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f61]) ).
fof(f263,plain,
! [X0,X1,X2] :
( ~ v3_struct_0(g3_lattices(X0,X1,X2))
| ~ m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f265,plain,
! [A] :
( ( v17_lattices(k1_lattice2(A))
& v16_lattices(k1_lattice2(A))
& v15_lattices(k1_lattice2(A))
& v14_lattices(k1_lattice2(A))
& v13_lattices(k1_lattice2(A))
& v12_lattices(k1_lattice2(A))
& v11_lattices(k1_lattice2(A))
& v10_lattices(k1_lattice2(A))
& v9_lattices(k1_lattice2(A))
& v8_lattices(k1_lattice2(A))
& v7_lattices(k1_lattice2(A))
& v6_lattices(k1_lattice2(A))
& v5_lattices(k1_lattice2(A))
& v4_lattices(k1_lattice2(A))
& v3_lattices(k1_lattice2(A))
& ~ v3_struct_0(k1_lattice2(A)) )
| ~ l3_lattices(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f62]) ).
fof(f274,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f265]) ).
fof(f281,plain,
! [X0] :
( v17_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f265]) ).
fof(f306,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)],[f67]) ).
fof(f307,plain,
! [X0,X1,X2,X3,X4,X5] :
( X1 = X3
| 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)],[f306]) ).
fof(f422,plain,
! [A,B] :
( k15_filter_2(A,B) = k7_filter_2(A,B)
| ~ m2_filter_2(B,A)
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f85]) ).
fof(f423,plain,
! [X0,X1] :
( k15_filter_2(X0,X1) = k7_filter_2(X0,X1)
| ~ m2_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f422]) ).
fof(f424,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)],[f86]) ).
fof(f425,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)],[f424]) ).
fof(f426,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)],[f87]) ).
fof(f427,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)],[f426]) ).
fof(f428,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)],[f427]) ).
fof(f429,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)],[f428]) ).
fof(f431,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)],[f88]) ).
fof(f432,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)],[f431]) ).
fof(f433,plain,
! [X0,X1,X2] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f432]) ).
fof(f441,plain,
! [A] :
( ! [B] :
( ( r2_filter_2(A,B)
<=> v1_filter_0(k15_filter_2(A,B),k1_lattice2(A)) )
| ~ m2_filter_2(B,A) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f92]) ).
fof(f442,plain,
! [A] :
( ! [B] :
( ( ( ~ v1_filter_0(k15_filter_2(A,B),k1_lattice2(A))
| r2_filter_2(A,B) )
& ( v1_filter_0(k15_filter_2(A,B),k1_lattice2(A))
| ~ r2_filter_2(A,B) ) )
| ~ m2_filter_2(B,A) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f441]) ).
fof(f443,plain,
! [X0,X1] :
( v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0))
| ~ r2_filter_2(X0,X1)
| ~ m2_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f442]) ).
fof(f444,plain,
! [X0,X1] :
( ~ v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0))
| r2_filter_2(X0,X1)
| ~ m2_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f442]) ).
fof(f449,plain,
! [A] :
( ! [B] :
( ( v1_filter_2(B,A)
<=> v2_filter_0(k15_filter_2(A,B),k1_lattice2(A)) )
| ~ m2_filter_2(B,A) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f94]) ).
fof(f450,plain,
! [A] :
( ! [B] :
( ( ( ~ v2_filter_0(k15_filter_2(A,B),k1_lattice2(A))
| v1_filter_2(B,A) )
& ( v2_filter_0(k15_filter_2(A,B),k1_lattice2(A))
| ~ v1_filter_2(B,A) ) )
| ~ m2_filter_2(B,A) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f449]) ).
fof(f451,plain,
! [X0,X1] :
( v2_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0))
| ~ v1_filter_2(X1,X0)
| ~ m2_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f450]) ).
fof(f452,plain,
! [X0,X1] :
( ~ v2_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0))
| v1_filter_2(X1,X0)
| ~ m2_filter_2(X1,X0)
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f450]) ).
fof(f456,plain,
! [A] :
( ! [B] :
( ( ( v2_filter_0(B,A)
& B != k1_filter_0(A) )
<=> v1_filter_0(B,A) )
| ~ m1_filter_0(B,A) )
| ~ l3_lattices(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f96]) ).
fof(f457,plain,
! [A] :
( ! [B] :
( ( ( ~ v1_filter_0(B,A)
| ( v2_filter_0(B,A)
& B != k1_filter_0(A) ) )
& ( v1_filter_0(B,A)
| ~ v2_filter_0(B,A)
| B = k1_filter_0(A) ) )
| ~ m1_filter_0(B,A) )
| ~ l3_lattices(A)
| ~ v17_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f456]) ).
fof(f458,plain,
! [X0,X1] :
( v1_filter_0(X1,X0)
| ~ v2_filter_0(X1,X0)
| X1 = k1_filter_0(X0)
| ~ m1_filter_0(X1,X0)
| ~ l3_lattices(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f457]) ).
fof(f459,plain,
! [X0,X1] :
( ~ v1_filter_0(X1,X0)
| X1 != k1_filter_0(X0)
| ~ m1_filter_0(X1,X0)
| ~ l3_lattices(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f457]) ).
fof(f460,plain,
! [X0,X1] :
( ~ v1_filter_0(X1,X0)
| v2_filter_0(X1,X0)
| ~ m1_filter_0(X1,X0)
| ~ l3_lattices(X0)
| ~ v17_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f457]) ).
fof(f472,plain,
( k17_filter_2(sK0_skl) = u1_struct_0(sK0_skl)
| ~ l3_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f170,f105]) ).
fof(f473,plain,
( k17_filter_2(sK0_skl) = u1_struct_0(sK0_skl)
| ~ l3_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f472,f104]) ).
fof(f474,plain,
( r2_filter_2(sK0_skl,sK1_skl)
| sK1_skl != u1_struct_0(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f475,f109]) ).
fof(f475,plain,
k17_filter_2(sK0_skl) = u1_struct_0(sK0_skl),
inference(forward_subsumption_resolution,[status(thm)],[f473,f107]) ).
fof(f476,plain,
( m2_filter_2(k17_filter_2(sK0_skl),sK0_skl)
| ~ l3_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f177,f105]) ).
fof(f477,plain,
( m2_filter_2(u1_struct_0(sK0_skl),sK0_skl)
| ~ l3_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f475,f476]) ).
fof(f478,plain,
( m2_filter_2(u1_struct_0(sK0_skl),sK0_skl)
| ~ l3_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f477,f104]) ).
fof(f479,plain,
m2_filter_2(u1_struct_0(sK0_skl),sK0_skl),
inference(forward_subsumption_resolution,[status(thm)],[f478,f107]) ).
fof(f480,plain,
( ~ v1_xboole_0(u1_struct_0(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f201,f479]) ).
fof(f482,plain,
( ~ v1_xboole_0(u1_struct_0(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f480,f104]) ).
fof(f486,plain,
( ~ v1_xboole_0(u1_struct_0(sK0_skl))
| ~ l3_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f482,f105]) ).
fof(f487,plain,
( v10_lattices(k1_lattice2(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v17_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f274,f105]) ).
fof(f488,plain,
( v10_lattices(k1_lattice2(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v17_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f487,f104]) ).
fof(f489,plain,
( v10_lattices(k1_lattice2(sK0_skl))
| ~ l3_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f488,f106]) ).
fof(f490,plain,
v10_lattices(k1_lattice2(sK0_skl)),
inference(resolution,[status(thm)],[f489,f107]) ).
fof(f491,plain,
( ~ r2_filter_2(sK0_skl,sK1_skl)
| ~ v1_filter_2(sK1_skl,sK0_skl)
| sK1_skl = u1_struct_0(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f475,f111]) ).
fof(f493,plain,
( v17_lattices(k1_lattice2(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v17_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f281,f105]) ).
fof(f494,plain,
( v17_lattices(k1_lattice2(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v17_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f493,f104]) ).
fof(f512,plain,
( v17_lattices(k1_lattice2(sK0_skl))
| ~ l3_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f494,f106]) ).
fof(f513,plain,
v17_lattices(k1_lattice2(sK0_skl)),
inference(resolution,[status(thm)],[f512,f107]) ).
fof(f528,plain,
( v1_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))
| ~ r2_filter_2(sK0_skl,sK1_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f443,f108]) ).
fof(f531,plain,
( v1_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))
| ~ r2_filter_2(sK0_skl,sK1_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f528,f104]) ).
fof(f534,plain,
( v2_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))
| ~ v1_filter_2(sK1_skl,sK0_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f451,f108]) ).
fof(f537,plain,
( v2_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))
| ~ v1_filter_2(sK1_skl,sK0_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f534,f104]) ).
fof(f539,plain,
( v1_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))
| ~ r2_filter_2(sK0_skl,sK1_skl)
| ~ l3_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f531,f105]) ).
fof(f540,plain,
( v2_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))
| ~ v1_filter_2(sK1_skl,sK0_skl)
| ~ l3_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f537,f105]) ).
fof(f541,plain,
( r2_filter_2(sK0_skl,sK1_skl)
| v2_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))
| ~ l3_lattices(sK0_skl) ),
inference(resolution,[status(thm)],[f540,f110]) ).
fof(f542,plain,
( r2_filter_2(sK0_skl,sK1_skl)
| v2_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f541,f107]) ).
fof(f828,plain,
l1_lattices(sK0_skl),
inference(resolution,[status(thm)],[f192,f107]) ).
fof(f878,plain,
l2_lattices(sK0_skl),
inference(resolution,[status(thm)],[f193,f107]) ).
fof(f909,plain,
v3_lattices(k1_lattice2(sK0_skl)),
inference(resolution,[status(thm)],[f183,f107]) ).
fof(f918,plain,
l3_lattices(k1_lattice2(sK0_skl)),
inference(resolution,[status(thm)],[f184,f107]) ).
fof(f943,plain,
( k1_lattice2(sK0_skl) = g3_lattices(u1_struct_0(k1_lattice2(sK0_skl)),u2_lattices(k1_lattice2(sK0_skl)),u1_lattices(k1_lattice2(sK0_skl)))
| ~ v3_lattices(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f918,f113]) ).
fof(f944,plain,
k1_lattice2(sK0_skl) = g3_lattices(u1_struct_0(k1_lattice2(sK0_skl)),u2_lattices(k1_lattice2(sK0_skl)),u1_lattices(k1_lattice2(sK0_skl))),
inference(forward_subsumption_resolution,[status(thm)],[f943,f909]) ).
fof(f1088,plain,
( k1_filter_0(k1_lattice2(sK0_skl)) = u1_struct_0(k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f164,f490]) ).
fof(f1090,plain,
( k1_filter_0(sK0_skl) = u1_struct_0(sK0_skl)
| ~ l3_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f164,f105]) ).
fof(f1096,plain,
( k1_filter_0(k1_lattice2(sK0_skl)) = u1_struct_0(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f1088,f918]) ).
fof(f1098,plain,
( k1_filter_0(sK0_skl) = u1_struct_0(sK0_skl)
| ~ l3_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1090,f104]) ).
fof(f1132,plain,
( ~ r2_filter_2(sK0_skl,sK1_skl)
| ~ v1_filter_2(sK1_skl,sK0_skl)
| sK1_skl = k1_filter_0(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f1137,f491]) ).
fof(f1133,plain,
( ~ v1_xboole_0(k1_filter_0(sK0_skl))
| ~ l3_lattices(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f1137,f486]) ).
fof(f1135,plain,
( r2_filter_2(sK0_skl,sK1_skl)
| sK1_skl != k1_filter_0(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f1137,f474]) ).
fof(f1137,plain,
k1_filter_0(sK0_skl) = u1_struct_0(sK0_skl),
inference(forward_subsumption_resolution,[status(thm)],[f1098,f107]) ).
fof(f1142,plain,
~ v1_xboole_0(k1_filter_0(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f1133,f107]) ).
fof(f1171,plain,
k1_lattice2(sK0_skl) = g3_lattices(u1_struct_0(sK0_skl),u1_lattices(sK0_skl),u2_lattices(sK0_skl)),
inference(resolution,[status(thm)],[f166,f107]) ).
fof(f1172,plain,
k1_lattice2(sK0_skl) = g3_lattices(k1_filter_0(sK0_skl),u1_lattices(sK0_skl),u2_lattices(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f1137,f1171]) ).
fof(f1174,plain,
! [X0] :
( k7_filter_2(sK0_skl,X0) = X0
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK0_skl)))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(paramodulation,[status(thm)],[f1137,f168]) ).
fof(f1175,plain,
! [X0] :
( k7_filter_2(sK0_skl,X0) = X0
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK0_skl)))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1174,f104]) ).
fof(f1234,plain,
v1_funct_1(u1_lattices(sK0_skl)),
inference(resolution,[status(thm)],[f208,f828]) ).
fof(f1249,plain,
( m1_filter_2(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f175,f108]) ).
fof(f1256,plain,
( m1_filter_2(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1249,f104]) ).
fof(f1276,plain,
( m1_filter_2(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))
| ~ l3_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1256,f105]) ).
fof(f1277,plain,
m1_filter_2(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl)),
inference(resolution,[status(thm)],[f1276,f107]) ).
fof(f1358,plain,
v1_funct_1(u2_lattices(sK0_skl)),
inference(resolution,[status(thm)],[f212,f878]) ).
fof(f1571,plain,
! [X0] :
( k7_filter_2(sK0_skl,X0) = X0
| ~ m1_subset_1(X0,k1_zfmisc_1(k1_filter_0(sK0_skl)))
| ~ l3_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1175,f105]) ).
fof(f1584,plain,
( m2_lattice4(sK1_skl,sK0_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f202,f108]) ).
fof(f1595,plain,
( m2_lattice4(sK1_skl,sK0_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1584,f104]) ).
fof(f1600,plain,
( m2_lattice4(sK1_skl,sK0_skl)
| ~ l3_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1595,f105]) ).
fof(f1601,plain,
m2_lattice4(sK1_skl,sK0_skl),
inference(resolution,[status(thm)],[f1600,f107]) ).
fof(f1602,plain,
( m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f1601,f204]) ).
fof(f1603,plain,
( m1_subset_1(sK1_skl,k1_zfmisc_1(k1_filter_0(sK0_skl)))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f1137,f1602]) ).
fof(f1604,plain,
( m1_subset_1(sK1_skl,k1_zfmisc_1(k1_filter_0(sK0_skl)))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1603,f104]) ).
fof(f1693,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)],[f209,f828]) ).
fof(f1702,plain,
v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f1137,f1693]) ).
fof(f1703,plain,
v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),u1_struct_0(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f1137,f1702]) ).
fof(f1704,plain,
v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f1137,f1703]) ).
fof(f1728,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)],[f210,f828]) ).
fof(f1737,plain,
m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f1137,f1728]) ).
fof(f1738,plain,
m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),u1_struct_0(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f1137,f1737]) ).
fof(f1739,plain,
m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f1137,f1738]) ).
fof(f1762,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)],[f213,f878]) ).
fof(f1772,plain,
v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(k1_filter_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f1137,f1762]) ).
fof(f1773,plain,
v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),u1_struct_0(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f1137,f1772]) ).
fof(f1774,plain,
v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f1137,f1773]) ).
fof(f1838,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)],[f214,f878]) ).
fof(f1848,plain,
m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(k1_filter_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f1137,f1838]) ).
fof(f1849,plain,
m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),u1_struct_0(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f1137,f1848]) ).
fof(f1850,plain,
m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f1137,f1849]) ).
fof(f2132,plain,
m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl)),
inference(resolution,[status(thm)],[f1739,f433]) ).
fof(f2181,plain,
( k1_filter_0(k1_lattice2(sK0_skl)) = u1_struct_0(k1_lattice2(sK0_skl))
| ~ l3_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f244,f1096]) ).
fof(f2187,plain,
( k1_filter_0(k1_lattice2(sK0_skl)) = u1_struct_0(k1_lattice2(sK0_skl))
| ~ l3_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f2181,f104]) ).
fof(f2197,plain,
k1_lattice2(sK0_skl) = g3_lattices(k1_filter_0(k1_lattice2(sK0_skl)),u2_lattices(k1_lattice2(sK0_skl)),u1_lattices(k1_lattice2(sK0_skl))),
inference(backward_demodulation,[status(thm)],[f2199,f944]) ).
fof(f2199,plain,
k1_filter_0(k1_lattice2(sK0_skl)) = u1_struct_0(k1_lattice2(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f2187,f107]) ).
fof(f2237,plain,
( m1_subset_1(sK1_skl,k1_zfmisc_1(k1_filter_0(sK0_skl)))
| ~ l3_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f1604,f105]) ).
fof(f2238,plain,
m1_subset_1(sK1_skl,k1_zfmisc_1(k1_filter_0(sK0_skl))),
inference(resolution,[status(thm)],[f2237,f107]) ).
fof(f2239,plain,
m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl)),
inference(resolution,[status(thm)],[f1850,f433]) ).
fof(f2307,plain,
( k7_filter_2(sK0_skl,sK1_skl) = sK1_skl
| ~ l3_lattices(sK0_skl) ),
inference(resolution,[status(thm)],[f2238,f1571]) ).
fof(f2309,plain,
k7_filter_2(sK0_skl,sK1_skl) = sK1_skl,
inference(forward_subsumption_resolution,[status(thm)],[f2307,f107]) ).
fof(f2661,plain,
! [X0] :
( ~ v3_struct_0(g3_lattices(k1_filter_0(sK0_skl),u1_lattices(sK0_skl),X0))
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_1(u1_lattices(sK0_skl))
| v1_xboole_0(k1_filter_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f263,f1704]) ).
fof(f2663,plain,
! [X0] :
( ~ v3_struct_0(g3_lattices(k1_filter_0(sK0_skl),u1_lattices(sK0_skl),X0))
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_1(u1_lattices(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2661,f1142]) ).
fof(f4120,plain,
! [X0,X1,X2,X3] :
( k1_filter_0(sK0_skl) = X1
| g3_lattices(k1_filter_0(sK0_skl),u1_lattices(sK0_skl),X0) != g3_lattices(X1,X2,X3)
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_1(u1_lattices(sK0_skl)) ),
inference(resolution,[status(thm)],[f307,f1704]) ).
fof(f4123,plain,
! [X0,X1,X2,X3] :
( k1_filter_0(sK0_skl) = X1
| g3_lattices(k1_filter_0(sK0_skl),u1_lattices(sK0_skl),X0) != g3_lattices(X1,X2,X3)
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4120,f1234]) ).
fof(f4666,plain,
( k15_filter_2(sK0_skl,sK1_skl) = k7_filter_2(sK0_skl,sK1_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f423,f108]) ).
fof(f4689,plain,
( k15_filter_2(sK0_skl,sK1_skl) = sK1_skl
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(forward_demodulation,[status(thm)],[f2309,f4666]) ).
fof(f4690,plain,
( k15_filter_2(sK0_skl,sK1_skl) = sK1_skl
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f4689,f104]) ).
fof(f4702,plain,
( k1_filter_2(k1_lattice2(sK0_skl)) = k1_filter_0(k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f425,f490]) ).
fof(f4704,plain,
( k1_filter_2(sK0_skl) = k1_filter_0(sK0_skl)
| ~ l3_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f425,f105]) ).
fof(f4716,plain,
( k1_filter_2(k1_lattice2(sK0_skl)) = k1_filter_0(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4702,f918]) ).
fof(f4718,plain,
( k1_filter_2(sK0_skl) = k1_filter_0(sK0_skl)
| ~ l3_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f4704,f104]) ).
fof(f4789,plain,
m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_2(sK0_skl)),
inference(backward_demodulation,[status(thm)],[f4848,f2239]) ).
fof(f4790,plain,
m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_2(sK0_skl)),
inference(backward_demodulation,[status(thm)],[f4848,f2132]) ).
fof(f4828,plain,
v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_2(sK0_skl)),
inference(backward_demodulation,[status(thm)],[f4848,f1774]) ).
fof(f4840,plain,
k1_lattice2(sK0_skl) = g3_lattices(k1_filter_2(sK0_skl),u1_lattices(sK0_skl),u2_lattices(sK0_skl)),
inference(backward_demodulation,[status(thm)],[f4848,f1172]) ).
fof(f4842,plain,
( r2_filter_2(sK0_skl,sK1_skl)
| sK1_skl != k1_filter_2(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f4848,f1135]) ).
fof(f4846,plain,
( ~ r2_filter_2(sK0_skl,sK1_skl)
| ~ v1_filter_2(sK1_skl,sK0_skl)
| sK1_skl = k1_filter_2(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f4848,f1132]) ).
fof(f4848,plain,
k1_filter_2(sK0_skl) = k1_filter_0(sK0_skl),
inference(forward_subsumption_resolution,[status(thm)],[f4718,f107]) ).
fof(f4852,plain,
m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_2(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f4848,f4789]) ).
fof(f4853,plain,
m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f4848,f4852]) ).
fof(f4854,plain,
m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_2(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f4848,f4790]) ).
fof(f4855,plain,
m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f4848,f4854]) ).
fof(f4862,plain,
v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_2(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f4848,f4828]) ).
fof(f4863,plain,
v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f4848,f4862]) ).
fof(f4906,plain,
( k15_filter_2(sK0_skl,sK1_skl) = sK1_skl
| ~ l3_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f4690,f105]) ).
fof(f4907,plain,
k15_filter_2(sK0_skl,sK1_skl) = sK1_skl,
inference(resolution,[status(thm)],[f4906,f107]) ).
fof(f4911,plain,
m1_filter_2(sK1_skl,k1_lattice2(sK0_skl)),
inference(backward_demodulation,[status(thm)],[f4907,f1277]) ).
fof(f4912,plain,
( r2_filter_2(sK0_skl,sK1_skl)
| v2_filter_0(sK1_skl,k1_lattice2(sK0_skl)) ),
inference(backward_demodulation,[status(thm)],[f4907,f542]) ).
fof(f4914,plain,
( v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| ~ r2_filter_2(sK0_skl,sK1_skl)
| ~ l3_lattices(sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f4907,f539]) ).
fof(f4915,plain,
( ~ v2_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| v1_filter_2(sK1_skl,sK0_skl)
| ~ m2_filter_2(sK1_skl,sK0_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(paramodulation,[status(thm)],[f4907,f452]) ).
fof(f4916,plain,
( ~ v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| r2_filter_2(sK0_skl,sK1_skl)
| ~ m2_filter_2(sK1_skl,sK0_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(paramodulation,[status(thm)],[f4907,f444]) ).
fof(f4918,plain,
( v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| ~ r2_filter_2(sK0_skl,sK1_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f4914,f107]) ).
fof(f4919,plain,
( ~ v2_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| v1_filter_2(sK1_skl,sK0_skl)
| ~ m2_filter_2(sK1_skl,sK0_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f4915,f104]) ).
fof(f4920,plain,
( ~ v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| r2_filter_2(sK0_skl,sK1_skl)
| ~ m2_filter_2(sK1_skl,sK0_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f4916,f104]) ).
fof(f4921,plain,
( m1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| ~ v10_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f4911,f429]) ).
fof(f4924,plain,
( m1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4921,f490]) ).
fof(f5753,plain,
( ~ l3_lattices(sK0_skl)
| v3_struct_0(sK0_skl)
| k1_filter_2(k1_lattice2(sK0_skl)) = k1_filter_0(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f4716,f244]) ).
fof(f5754,plain,
( ~ l3_lattices(sK0_skl)
| k1_filter_2(k1_lattice2(sK0_skl)) = k1_filter_0(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f5753,f104]) ).
fof(f5818,plain,
k1_lattice2(sK0_skl) = g3_lattices(k1_filter_2(k1_lattice2(sK0_skl)),u2_lattices(k1_lattice2(sK0_skl)),u1_lattices(k1_lattice2(sK0_skl))),
inference(backward_demodulation,[status(thm)],[f5830,f2197]) ).
fof(f5830,plain,
k1_filter_2(k1_lattice2(sK0_skl)) = k1_filter_0(k1_lattice2(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f5754,f107]) ).
fof(f6958,plain,
( m1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f4924,f918]) ).
fof(f6959,plain,
( ~ v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| v2_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| ~ v17_lattices(k1_lattice2(sK0_skl))
| ~ v10_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f6958,f460]) ).
fof(f6960,plain,
( ~ v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| sK1_skl != k1_filter_0(k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| ~ v17_lattices(k1_lattice2(sK0_skl))
| ~ v10_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f6958,f459]) ).
fof(f6961,plain,
( v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| ~ v2_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| sK1_skl = k1_filter_0(k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| ~ v17_lattices(k1_lattice2(sK0_skl))
| ~ v10_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f6958,f458]) ).
fof(f6965,plain,
( ~ v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| v2_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| ~ v17_lattices(k1_lattice2(sK0_skl))
| ~ v10_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f6959]) ).
fof(f6966,plain,
( ~ v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| v2_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| ~ v17_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f6965,f490]) ).
fof(f6967,plain,
( ~ v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| sK1_skl != k1_filter_2(k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| ~ v17_lattices(k1_lattice2(sK0_skl))
| ~ v10_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f5830,f6960]) ).
fof(f6968,plain,
( ~ v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| sK1_skl != k1_filter_2(k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| ~ v17_lattices(k1_lattice2(sK0_skl))
| ~ v10_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f6967]) ).
fof(f6969,plain,
( ~ v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| sK1_skl != k1_filter_2(k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| ~ v17_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f6968,f490]) ).
fof(f6970,plain,
( v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| ~ v2_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| sK1_skl = k1_filter_2(k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| ~ v17_lattices(k1_lattice2(sK0_skl))
| ~ v10_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f5830,f6961]) ).
fof(f6971,plain,
( v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| ~ v2_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| sK1_skl = k1_filter_2(k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| ~ v17_lattices(k1_lattice2(sK0_skl))
| ~ v10_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f6970]) ).
fof(f6972,plain,
( v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| ~ v2_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| sK1_skl = k1_filter_2(k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| ~ v17_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f6971,f490]) ).
fof(f9253,plain,
! [X0] :
( ~ v3_struct_0(g3_lattices(k1_filter_0(sK0_skl),u1_lattices(sK0_skl),X0))
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_1(u1_lattices(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f4848,f2663]) ).
fof(f9254,plain,
! [X0] :
( ~ v3_struct_0(g3_lattices(k1_filter_0(sK0_skl),u1_lattices(sK0_skl),X0))
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_1(u1_lattices(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f4848,f9253]) ).
fof(f9255,plain,
! [X0] :
( ~ v3_struct_0(g3_lattices(k1_filter_0(sK0_skl),u1_lattices(sK0_skl),X0))
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(u1_lattices(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f4848,f9254]) ).
fof(f9256,plain,
! [X0] :
( ~ v3_struct_0(g3_lattices(k1_filter_0(sK0_skl),u1_lattices(sK0_skl),X0))
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(u1_lattices(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f4848,f9255]) ).
fof(f9257,plain,
! [X0] :
( ~ v3_struct_0(g3_lattices(k1_filter_0(sK0_skl),u1_lattices(sK0_skl),X0))
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(u1_lattices(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f4848,f9256]) ).
fof(f9258,plain,
! [X0] :
( ~ v3_struct_0(g3_lattices(k1_filter_0(sK0_skl),u1_lattices(sK0_skl),X0))
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(u1_lattices(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f4848,f9257]) ).
fof(f9259,plain,
! [X0] :
( ~ v3_struct_0(g3_lattices(k1_filter_0(sK0_skl),u1_lattices(sK0_skl),X0))
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(u1_lattices(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f4848,f9258]) ).
fof(f9260,plain,
! [X0] :
( ~ v3_struct_0(g3_lattices(k1_filter_0(sK0_skl),u1_lattices(sK0_skl),X0))
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(u1_lattices(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f4848,f9259]) ).
fof(f9261,plain,
! [X0] :
( ~ v3_struct_0(g3_lattices(k1_filter_0(sK0_skl),u1_lattices(sK0_skl),X0))
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(u1_lattices(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f4848,f9260]) ).
fof(f9262,plain,
! [X0] :
( ~ v3_struct_0(g3_lattices(k1_filter_2(sK0_skl),u1_lattices(sK0_skl),X0))
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(u1_lattices(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f4848,f9261]) ).
fof(f9263,plain,
! [X0] :
( ~ v3_struct_0(g3_lattices(k1_filter_2(sK0_skl),u1_lattices(sK0_skl),X0))
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9262,f1234]) ).
fof(f9264,plain,
! [X0] :
( ~ v3_struct_0(g3_lattices(k1_filter_2(sK0_skl),u1_lattices(sK0_skl),X0))
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(X0) ),
inference(resolution,[status(thm)],[f9263,f4855]) ).
fof(f9673,plain,
! [X0,X1,X2,X3] :
( k1_filter_0(sK0_skl) = X1
| g3_lattices(k1_filter_0(sK0_skl),u1_lattices(sK0_skl),X0) != g3_lattices(X1,X2,X3)
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f4848,f4123]) ).
fof(f9674,plain,
! [X0,X1,X2,X3] :
( k1_filter_0(sK0_skl) = X1
| g3_lattices(k1_filter_0(sK0_skl),u1_lattices(sK0_skl),X0) != g3_lattices(X1,X2,X3)
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_0(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f4848,f9673]) ).
fof(f9675,plain,
! [X0,X1,X2,X3] :
( k1_filter_0(sK0_skl) = X1
| g3_lattices(k1_filter_0(sK0_skl),u1_lattices(sK0_skl),X0) != g3_lattices(X1,X2,X3)
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f4848,f9674]) ).
fof(f9676,plain,
! [X0,X1,X2,X3] :
( k1_filter_0(sK0_skl) = X1
| g3_lattices(k1_filter_0(sK0_skl),u1_lattices(sK0_skl),X0) != g3_lattices(X1,X2,X3)
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f4848,f9675]) ).
fof(f9677,plain,
! [X0,X1,X2,X3] :
( k1_filter_0(sK0_skl) = X1
| g3_lattices(k1_filter_0(sK0_skl),u1_lattices(sK0_skl),X0) != g3_lattices(X1,X2,X3)
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f4848,f9676]) ).
fof(f9678,plain,
! [X0,X1,X2,X3] :
( k1_filter_0(sK0_skl) = X1
| g3_lattices(k1_filter_0(sK0_skl),u1_lattices(sK0_skl),X0) != g3_lattices(X1,X2,X3)
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_0(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f4848,f9677]) ).
fof(f9679,plain,
! [X0,X1,X2,X3] :
( k1_filter_0(sK0_skl) = X1
| g3_lattices(k1_filter_0(sK0_skl),u1_lattices(sK0_skl),X0) != g3_lattices(X1,X2,X3)
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_0(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f4848,f9678]) ).
fof(f9680,plain,
! [X0,X1,X2,X3] :
( k1_filter_0(sK0_skl) = X1
| g3_lattices(k1_filter_0(sK0_skl),u1_lattices(sK0_skl),X0) != g3_lattices(X1,X2,X3)
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_0(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f4848,f9679]) ).
fof(f9681,plain,
! [X0,X1,X2,X3] :
( k1_filter_0(sK0_skl) = X1
| g3_lattices(k1_filter_0(sK0_skl),u1_lattices(sK0_skl),X0) != g3_lattices(X1,X2,X3)
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f4848,f9680]) ).
fof(f9682,plain,
! [X0,X1,X2,X3] :
( k1_filter_0(sK0_skl) = X1
| g3_lattices(k1_filter_2(sK0_skl),u1_lattices(sK0_skl),X0) != g3_lattices(X1,X2,X3)
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f4848,f9681]) ).
fof(f9683,plain,
! [X0,X1,X2,X3] :
( k1_filter_2(sK0_skl) = X1
| g3_lattices(k1_filter_2(sK0_skl),u1_lattices(sK0_skl),X0) != g3_lattices(X1,X2,X3)
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(X0)
| ~ m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f4848,f9682]) ).
fof(f9684,plain,
! [X0,X1,X2,X3] :
( k1_filter_2(sK0_skl) = X1
| g3_lattices(k1_filter_2(sK0_skl),u1_lattices(sK0_skl),X0) != g3_lattices(X1,X2,X3)
| ~ m1_relset_1(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f9683,f4855]) ).
fof(f9686,plain,
! [X0,X1,X2] :
( k1_filter_2(sK0_skl) = X0
| g3_lattices(k1_filter_2(sK0_skl),u1_lattices(sK0_skl),u2_lattices(sK0_skl)) != g3_lattices(X0,X1,X2)
| ~ m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(u2_lattices(sK0_skl)) ),
inference(resolution,[status(thm)],[f9684,f4863]) ).
fof(f9688,plain,
! [X0,X1,X2] :
( k1_filter_2(sK0_skl) = X0
| k1_lattice2(sK0_skl) != g3_lattices(X0,X1,X2)
| ~ m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(u2_lattices(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f4840,f9686]) ).
fof(f9689,plain,
! [X0,X1,X2] :
( k1_filter_2(sK0_skl) = X0
| k1_lattice2(sK0_skl) != g3_lattices(X0,X1,X2)
| ~ m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f9688,f1358]) ).
fof(f10327,plain,
( ~ v2_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| v1_filter_2(sK1_skl,sK0_skl)
| ~ m2_filter_2(sK1_skl,sK0_skl)
| ~ l3_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f4919,f105]) ).
fof(f10483,plain,
( ~ v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| r2_filter_2(sK0_skl,sK1_skl)
| ~ m2_filter_2(sK1_skl,sK0_skl)
| ~ l3_lattices(sK0_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f4920,f105]) ).
fof(f26489,plain,
( ~ v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| v2_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f6966,f513]) ).
fof(f26573,plain,
( ~ v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| sK1_skl != k1_filter_2(k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f6969,f513]) ).
fof(f26602,plain,
( v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| ~ v2_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| sK1_skl = k1_filter_2(k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f6972,f513]) ).
fof(f26603,plain,
( r2_filter_2(sK0_skl,sK1_skl)
| v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| sK1_skl = k1_filter_2(k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f26602,f4912]) ).
fof(f26604,plain,
( r2_filter_2(sK0_skl,sK1_skl)
| v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| sK1_skl = k1_filter_2(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f26603,f918]) ).
fof(f26626,plain,
( v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| sK1_skl = k1_filter_2(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f26604,f4918]) ).
fof(f26628,plain,
( v2_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl))
| sK1_skl = k1_filter_2(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f26626,f26489]) ).
fof(f26629,plain,
( r2_filter_2(sK0_skl,sK1_skl)
| ~ m2_filter_2(sK1_skl,sK0_skl)
| ~ l3_lattices(sK0_skl)
| sK1_skl = k1_filter_2(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f26626,f10483]) ).
fof(f26630,plain,
( v2_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl))
| sK1_skl = k1_filter_2(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f26628]) ).
fof(f26631,plain,
( v2_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| sK1_skl = k1_filter_2(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f26630,f918]) ).
fof(f26632,plain,
( r2_filter_2(sK0_skl,sK1_skl)
| ~ m2_filter_2(sK1_skl,sK0_skl)
| sK1_skl = k1_filter_2(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f26629,f107]) ).
fof(f26633,plain,
( v1_filter_2(sK1_skl,sK0_skl)
| ~ m2_filter_2(sK1_skl,sK0_skl)
| ~ l3_lattices(sK0_skl)
| sK1_skl = k1_filter_2(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f26631,f10327]) ).
fof(f26634,plain,
( v1_filter_2(sK1_skl,sK0_skl)
| ~ m2_filter_2(sK1_skl,sK0_skl)
| sK1_skl = k1_filter_2(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f26633,f107]) ).
fof(f26635,plain,
( r2_filter_2(sK0_skl,sK1_skl)
| sK1_skl = k1_filter_2(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f26632,f108]) ).
fof(f26636,plain,
( ~ l3_lattices(sK0_skl)
| v3_struct_0(sK0_skl)
| r2_filter_2(sK0_skl,sK1_skl)
| sK1_skl = k1_filter_2(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f26635,f244]) ).
fof(f26637,plain,
( ~ l3_lattices(sK0_skl)
| r2_filter_2(sK0_skl,sK1_skl)
| sK1_skl = k1_filter_2(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f26636,f104]) ).
fof(f26638,plain,
( r2_filter_2(sK0_skl,sK1_skl)
| sK1_skl = k1_filter_2(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f26637,f107]) ).
fof(f26643,plain,
( v1_filter_2(sK1_skl,sK0_skl)
| sK1_skl = k1_filter_2(k1_lattice2(sK0_skl))
| v3_struct_0(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f26634,f108]) ).
fof(f26644,plain,
( ~ l3_lattices(sK0_skl)
| v3_struct_0(sK0_skl)
| v1_filter_2(sK1_skl,sK0_skl)
| sK1_skl = k1_filter_2(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f26643,f244]) ).
fof(f26645,plain,
( ~ l3_lattices(sK0_skl)
| v1_filter_2(sK1_skl,sK0_skl)
| sK1_skl = k1_filter_2(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f26644,f104]) ).
fof(f26671,plain,
( v1_filter_2(sK1_skl,sK0_skl)
| sK1_skl = k1_filter_2(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f26645,f107]) ).
fof(f26673,plain,
( ~ r2_filter_2(sK0_skl,sK1_skl)
| sK1_skl = k1_filter_2(sK0_skl)
| sK1_skl = k1_filter_2(k1_lattice2(sK0_skl)) ),
inference(resolution,[status(thm)],[f26671,f4846]) ).
fof(f26674,plain,
( sK1_skl = k1_filter_2(sK0_skl)
| sK1_skl = k1_filter_2(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f26673,f26638]) ).
fof(f27014,plain,
( sK1_skl = k1_filter_2(sK0_skl)
| k1_lattice2(sK0_skl) = g3_lattices(sK1_skl,u2_lattices(k1_lattice2(sK0_skl)),u1_lattices(k1_lattice2(sK0_skl))) ),
inference(paramodulation,[status(thm)],[f26674,f5818]) ).
fof(f28781,plain,
( ~ v3_struct_0(g3_lattices(k1_filter_2(sK0_skl),u1_lattices(sK0_skl),u2_lattices(sK0_skl)))
| ~ m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(u2_lattices(sK0_skl)) ),
inference(resolution,[status(thm)],[f9264,f4863]) ).
fof(f28783,plain,
( ~ v3_struct_0(k1_lattice2(sK0_skl))
| ~ m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl))
| ~ v1_funct_1(u2_lattices(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f4840,f28781]) ).
fof(f28784,plain,
( ~ v3_struct_0(k1_lattice2(sK0_skl))
| ~ m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(k1_filter_2(sK0_skl),k1_filter_2(sK0_skl)),k1_filter_2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f28783,f1358]) ).
fof(f28846,plain,
( ~ v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| sK1_skl != k1_filter_2(k1_lattice2(sK0_skl))
| ~ l3_lattices(k1_lattice2(sK0_skl)) ),
inference(backward_subsumption_resolution,[status(thm)],[f26573,f29125]) ).
fof(f29125,plain,
~ v3_struct_0(k1_lattice2(sK0_skl)),
inference(forward_subsumption_resolution,[status(thm)],[f28784,f4853]) ).
fof(f29126,plain,
( ~ v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))
| sK1_skl != k1_filter_2(k1_lattice2(sK0_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f28846,f918]) ).
fof(f30295,plain,
sK1_skl = k1_filter_2(sK0_skl),
inference(backward_subsumption_resolution,[status(thm)],[f27014,f30296]) ).
fof(f30296,plain,
! [X0,X1,X2] :
( k1_filter_2(sK0_skl) = X0
| k1_lattice2(sK0_skl) != g3_lattices(X0,X1,X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f9689,f4853]) ).
fof(f30297,plain,
k1_filter_2(sK0_skl) = k1_filter_2(k1_lattice2(sK0_skl)),
inference(resolution,[status(thm)],[f30296,f5818]) ).
fof(f31017,plain,
( r2_filter_2(sK0_skl,sK1_skl)
| sK1_skl != sK1_skl ),
inference(backward_demodulation,[status(thm)],[f30295,f4842]) ).
fof(f31182,plain,
r2_filter_2(sK0_skl,sK1_skl),
inference(trivial_equality_resolution,[status(thm)],[f31017]) ).
fof(f31200,plain,
v1_filter_0(sK1_skl,k1_lattice2(sK0_skl)),
inference(backward_subsumption_resolution,[status(thm)],[f4918,f31182]) ).
fof(f31227,plain,
sK1_skl != k1_filter_2(k1_lattice2(sK0_skl)),
inference(backward_subsumption_resolution,[status(thm)],[f29126,f31200]) ).
fof(f31231,plain,
sK1_skl = k1_filter_2(k1_lattice2(sK0_skl)),
inference(forward_demodulation,[status(thm)],[f30295,f30297]) ).
fof(f31232,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f31231,f31227]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT322+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/10.44 % Computer : n016.cluster.edu
% 0.19/10.44 % Model : x86_64 x86_64
% 0.19/10.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/10.44 % Memory : 8046.5625MB
% 0.19/10.44 % OS : Linux 6.8.0-71-generic
% 0.19/10.44 % CPULimit : 300
% 0.19/10.44 % WCLimit : 300
% 0.19/10.44 % DateTime : Sun Sep 20 23:42:18 UTC 2026
% 0.19/10.44 % CPUTime :
% 0.19/10.46 % Drodi V4.1.1
% 47.11/16.65 % Refutation found
% 47.11/16.65 % SZS status Theorem for theBenchmark: Theorem is valid
% 47.11/16.65 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 48.87/16.74 % Elapsed time: 6.286271 seconds
% 48.87/16.74 % CPU time: 49.440879 seconds
% 48.87/16.74 % Total memory used: 452.186 MB
% 48.87/16.74 % Net memory used: 437.661 MB
%------------------------------------------------------------------------------