%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT305+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.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:39 PM UTC 2026
% Result : Theorem 30.43s 14.49s
% Output : CNFRefutation 7.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 90
% Syntax : Number of formulae : 399 ( 79 unt; 58 def)
% Number of atoms : 1104 ( 40 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 1180 ( 475 ~; 509 |; 105 &)
% ( 62 <=>; 29 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 82 ( 80 usr; 59 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 12 con; 0-3 aty)
% Number of variables : 248 ( 230 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( r2_hidden(k4_lattices(A,C,B),k18_filter_2(A,B))
& r2_hidden(k4_lattices(A,B,C),k18_filter_2(A,B))
& r2_hidden(B,k18_filter_2(A,B)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ( r2_hidden(k4_lattices(A,C,B),k18_filter_2(A,B))
& r2_hidden(k4_lattices(A,B,C),k18_filter_2(A,B))
& r2_hidden(B,k18_filter_2(A,B)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f5,axiom,
! [A] :
( l3_lattices(A)
=> ( ( v10_lattices(A)
& ~ v3_struct_0(A) )
=> ( v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [A,B,C] :
( ( m1_subset_1(C,u1_struct_0(A))
& m1_subset_1(B,u1_struct_0(A))
& l1_lattices(A)
& v6_lattices(A)
& ~ v3_struct_0(A) )
=> k4_lattices(A,B,C) = k4_lattices(A,C,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> k18_filter_2(A,B) = a_2_0_filter_2(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [A,B,C] :
( ( m1_subset_1(C,u1_struct_0(A))
& m1_subset_1(B,u1_struct_0(A))
& l1_lattices(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k2_lattices(A,B,C),u1_struct_0(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [A,B,C] :
( ( m1_subset_1(C,u1_struct_0(A))
& m1_subset_1(B,u1_struct_0(A))
& l1_lattices(A)
& v6_lattices(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k4_lattices(A,B,C),u1_struct_0(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [A] :
( l1_lattices(A)
=> l1_struct_0(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,axiom,
! [A] :
( l2_lattices(A)
=> l1_struct_0(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,axiom,
! [A] :
( l3_lattices(A)
=> ( l2_lattices(A)
& l1_lattices(A) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [A] :
( l1_lattices(A)
=> ( m2_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_1(u1_lattices(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
? [A] : l1_lattices(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
? [A] : l1_struct_0(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
? [A] : l2_lattices(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
? [A] : l3_lattices(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [A] :
? [B] : m1_subset_1(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [A,B,C] :
( ( m1_subset_1(C,u1_struct_0(B))
& l3_lattices(B)
& v10_lattices(B)
& ~ v3_struct_0(B) )
=> ( r2_hidden(A,a_2_0_filter_2(B,C))
<=> ? [D] :
( r3_lattices(B,D,C)
& A = D
& m1_subset_1(D,u1_struct_0(B)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f58,axiom,
? [A] :
( v1_funct_1(A)
& v1_relat_1(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f61,axiom,
! [A] :
( ~ v1_xboole_0(A)
=> ? [B] :
( ~ v1_xboole_0(B)
& m1_subset_1(B,k1_zfmisc_1(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f63,axiom,
? [A] :
( v1_funct_1(A)
& v1_xboole_0(A)
& v1_relat_1(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f67,axiom,
? [A] :
( v2_funct_1(A)
& v1_funct_1(A)
& v1_relat_1(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f68,axiom,
? [A] :
( ~ v3_struct_0(A)
& l1_struct_0(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [A,B,C] :
( ( m1_subset_1(C,u1_struct_0(A))
& m1_subset_1(B,u1_struct_0(A))
& l1_lattices(A)
& v6_lattices(A)
& ~ v3_struct_0(A) )
=> k4_lattices(A,B,C) = k2_lattices(A,B,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f73,axiom,
! [A,B,C] :
( ( m1_subset_1(C,u1_struct_0(A))
& m1_subset_1(B,u1_struct_0(A))
& l3_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v6_lattices(A)
& ~ v3_struct_0(A) )
=> ( r3_lattices(A,B,C)
<=> r1_lattices(A,B,C) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f75,axiom,
! [A,B,C] :
( ( m1_subset_1(C,u1_struct_0(A))
& m1_subset_1(B,u1_struct_0(A))
& l3_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v6_lattices(A)
& ~ v3_struct_0(A) )
=> r3_lattices(A,B,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f76,axiom,
! [A,B] :
( r2_hidden(A,B)
=> m1_subset_1(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f77,axiom,
! [A] :
( ( l3_lattices(A)
& v8_lattices(A)
& v6_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(A))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> r1_lattices(A,k4_lattices(A,B,C),B) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f78,axiom,
! [A,B] :
( m1_subset_1(A,B)
=> ( r2_hidden(A,B)
| v1_xboole_0(B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f81,axiom,
! [A,B,C] :
( ( m1_subset_1(B,k1_zfmisc_1(C))
& r2_hidden(A,B) )
=> m1_subset_1(A,C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f82,axiom,
! [A,B,C] :
~ ( v1_xboole_0(C)
& m1_subset_1(B,k1_zfmisc_1(C))
& r2_hidden(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f83,axiom,
! [A] :
( v1_xboole_0(A)
=> A = k1_xboole_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f84,axiom,
! [A,B] :
~ ( v1_xboole_0(B)
& r2_hidden(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f86,plain,
? [A] :
( ? [B] :
( ? [C] :
( ( ~ r2_hidden(k4_lattices(A,C,B),k18_filter_2(A,B))
| ~ r2_hidden(k4_lattices(A,B,C),k18_filter_2(A,B))
| ~ r2_hidden(B,k18_filter_2(A,B)) )
& m1_subset_1(C,u1_struct_0(A)) )
& m1_subset_1(B,u1_struct_0(A)) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f87,plain,
( ( ~ r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK1_skl),k18_filter_2(sK0_skl,sK1_skl))
| ~ r2_hidden(k4_lattices(sK0_skl,sK1_skl,sK2_skl),k18_filter_2(sK0_skl,sK1_skl))
| ~ r2_hidden(sK1_skl,k18_filter_2(sK0_skl,sK1_skl)) )
& m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))
& m1_subset_1(sK1_skl,u1_struct_0(sK0_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]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl)],[f86]) ).
fof(f88,plain,
~ v3_struct_0(sK0_skl),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f89,plain,
v10_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f90,plain,
l3_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f91,plain,
m1_subset_1(sK1_skl,u1_struct_0(sK0_skl)),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f92,plain,
m1_subset_1(sK2_skl,u1_struct_0(sK0_skl)),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f93,plain,
( ~ r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK1_skl),k18_filter_2(sK0_skl,sK1_skl))
| ~ r2_hidden(k4_lattices(sK0_skl,sK1_skl,sK2_skl),k18_filter_2(sK0_skl,sK1_skl))
| ~ r2_hidden(sK1_skl,k18_filter_2(sK0_skl,sK1_skl)) ),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f98,plain,
! [A] :
( ( v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A) )
| ~ v10_lattices(A)
| v3_struct_0(A)
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5]) ).
fof(f102,plain,
! [X0] :
( v6_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f104,plain,
! [X0] :
( v8_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f105,plain,
! [X0] :
( v9_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f119,plain,
! [A,B,C] :
( k4_lattices(A,B,C) = k4_lattices(A,C,B)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l1_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f120,plain,
! [X0,X1,X2] :
( k4_lattices(X0,X1,X2) = k4_lattices(X0,X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_lattices(X0)
| ~ v6_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f119]) ).
fof(f126,plain,
! [A] :
( ! [B] :
( k18_filter_2(A,B) = a_2_0_filter_2(A,B)
| ~ m1_subset_1(B,u1_struct_0(A)) )
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f127,plain,
! [X0,X1] :
( k18_filter_2(X0,X1) = a_2_0_filter_2(X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f132,plain,
! [A,B,C] :
( m1_subset_1(k2_lattices(A,B,C),u1_struct_0(A))
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l1_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f133,plain,
! [X0,X1,X2] :
( m1_subset_1(k2_lattices(X0,X1,X2),u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f134,plain,
! [A,B,C] :
( m1_subset_1(k4_lattices(A,B,C),u1_struct_0(A))
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l1_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f135,plain,
! [X0,X1,X2] :
( m1_subset_1(k4_lattices(X0,X1,X2),u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_lattices(X0)
| ~ v6_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f136,plain,
! [A] :
( l1_struct_0(A)
| ~ l1_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f137,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f136]) ).
fof(f138,plain,
! [A] :
( l1_struct_0(A)
| ~ l2_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f139,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f140,plain,
! [A] :
( ( l2_lattices(A)
& l1_lattices(A) )
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f141,plain,
! [X0] :
( l1_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f150,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)],[f37]) ).
fof(f151,plain,
! [X0] :
( v1_funct_1(u1_lattices(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f154,plain,
l1_lattices(sK3_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(A,sK3_skl)],[f39]) ).
fof(f155,plain,
l1_lattices(sK3_skl),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f156,plain,
l1_struct_0(sK4_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(A,sK4_skl)],[f40]) ).
fof(f157,plain,
l1_struct_0(sK4_skl),
inference(cnf_transformation,[status(thm)],[f156]) ).
fof(f158,plain,
l2_lattices(sK5_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(A,sK5_skl)],[f41]) ).
fof(f159,plain,
l2_lattices(sK5_skl),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f160,plain,
l3_lattices(sK6_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(A,sK6_skl)],[f42]) ).
fof(f161,plain,
l3_lattices(sK6_skl),
inference(cnf_transformation,[status(thm)],[f160]) ).
fof(f164,plain,
! [A] : m1_subset_1(sK8_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(B,sK8_skl(A))],[f44]) ).
fof(f165,plain,
! [X0] : m1_subset_1(sK8_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f176,plain,
! [X0] : ~ v1_xboole_0(k1_zfmisc_1(X0)),
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f198,plain,
! [A,B,C] :
( ( r2_hidden(A,a_2_0_filter_2(B,C))
<=> ? [D] :
( r3_lattices(B,D,C)
& A = D
& m1_subset_1(D,u1_struct_0(B)) ) )
| ~ m1_subset_1(C,u1_struct_0(B))
| ~ l3_lattices(B)
| ~ v10_lattices(B)
| v3_struct_0(B) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f199,plain,
! [A,B,C] :
( ( ( ! [D] :
( ~ r3_lattices(B,D,C)
| A != D
| ~ m1_subset_1(D,u1_struct_0(B)) )
| r2_hidden(A,a_2_0_filter_2(B,C)) )
& ( ? [D] :
( r3_lattices(B,D,C)
& A = D
& m1_subset_1(D,u1_struct_0(B)) )
| ~ r2_hidden(A,a_2_0_filter_2(B,C)) ) )
| ~ m1_subset_1(C,u1_struct_0(B))
| ~ l3_lattices(B)
| ~ v10_lattices(B)
| v3_struct_0(B) ),
inference(NNF_transformation,[status(thm)],[f198]) ).
fof(f200,plain,
! [B,C] :
( ( ! [A] :
( ! [D] :
( ~ r3_lattices(B,D,C)
| A != D
| ~ m1_subset_1(D,u1_struct_0(B)) )
| r2_hidden(A,a_2_0_filter_2(B,C)) )
& ! [A] :
( ? [D] :
( r3_lattices(B,D,C)
& A = D
& m1_subset_1(D,u1_struct_0(B)) )
| ~ r2_hidden(A,a_2_0_filter_2(B,C)) ) )
| ~ m1_subset_1(C,u1_struct_0(B))
| ~ l3_lattices(B)
| ~ v10_lattices(B)
| v3_struct_0(B) ),
inference(miniscoping,[status(thm)],[f199]) ).
fof(f201,plain,
! [B,C] :
( ( ! [A] :
( ! [D] :
( ~ r3_lattices(B,D,C)
| A != D
| ~ m1_subset_1(D,u1_struct_0(B)) )
| r2_hidden(A,a_2_0_filter_2(B,C)) )
& ! [A] :
( ( r3_lattices(B,sK12_skl(A,C,B),C)
& A = sK12_skl(A,C,B)
& m1_subset_1(sK12_skl(A,C,B),u1_struct_0(B)) )
| ~ r2_hidden(A,a_2_0_filter_2(B,C)) ) )
| ~ m1_subset_1(C,u1_struct_0(B))
| ~ l3_lattices(B)
| ~ v10_lattices(B)
| v3_struct_0(B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(D,sK12_skl(A,C,B))],[f200]) ).
fof(f205,plain,
! [X0,X1,X2,X3] :
( ~ r3_lattices(X0,X3,X1)
| X2 != X3
| ~ m1_subset_1(X3,u1_struct_0(X0))
| r2_hidden(X2,a_2_0_filter_2(X0,X1))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f206,plain,
( v1_funct_1(sK13_skl)
& v1_relat_1(sK13_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(A,sK13_skl)],[f58]) ).
fof(f207,plain,
v1_relat_1(sK13_skl),
inference(cnf_transformation,[status(thm)],[f206]) ).
fof(f216,plain,
! [A] :
( ? [B] :
( ~ v1_xboole_0(B)
& m1_subset_1(B,k1_zfmisc_1(A)) )
| v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f61]) ).
fof(f217,plain,
! [A] :
( ( ~ v1_xboole_0(sK16_skl(A))
& m1_subset_1(sK16_skl(A),k1_zfmisc_1(A)) )
| v1_xboole_0(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(B,sK16_skl(A))],[f216]) ).
fof(f218,plain,
! [X0] :
( m1_subset_1(sK16_skl(X0),k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f217]) ).
fof(f219,plain,
! [X0] :
( ~ v1_xboole_0(sK16_skl(X0))
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f217]) ).
fof(f222,plain,
( v1_funct_1(sK18_skl)
& v1_xboole_0(sK18_skl)
& v1_relat_1(sK18_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(A,sK18_skl)],[f63]) ).
fof(f223,plain,
v1_relat_1(sK18_skl),
inference(cnf_transformation,[status(thm)],[f222]) ).
fof(f224,plain,
v1_xboole_0(sK18_skl),
inference(cnf_transformation,[status(thm)],[f222]) ).
fof(f234,plain,
( v2_funct_1(sK22_skl)
& v1_funct_1(sK22_skl)
& v1_relat_1(sK22_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(A,sK22_skl)],[f67]) ).
fof(f235,plain,
v1_relat_1(sK22_skl),
inference(cnf_transformation,[status(thm)],[f234]) ).
fof(f238,plain,
( ~ v3_struct_0(sK23_skl)
& l1_struct_0(sK23_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(A,sK23_skl)],[f68]) ).
fof(f239,plain,
l1_struct_0(sK23_skl),
inference(cnf_transformation,[status(thm)],[f238]) ).
fof(f240,plain,
~ v3_struct_0(sK23_skl),
inference(cnf_transformation,[status(thm)],[f238]) ).
fof(f247,plain,
! [A,B,C] :
( k4_lattices(A,B,C) = k2_lattices(A,B,C)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l1_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f71]) ).
fof(f248,plain,
! [X0,X1,X2] :
( k4_lattices(X0,X1,X2) = k2_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l1_lattices(X0)
| ~ v6_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f247]) ).
fof(f253,plain,
! [A,B,C] :
( ( r3_lattices(A,B,C)
<=> r1_lattices(A,B,C) )
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v9_lattices(A)
| ~ v8_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f73]) ).
fof(f254,plain,
! [A,B,C] :
( ( ( ~ r1_lattices(A,B,C)
| r3_lattices(A,B,C) )
& ( r1_lattices(A,B,C)
| ~ r3_lattices(A,B,C) ) )
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v9_lattices(A)
| ~ v8_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(NNF_transformation,[status(thm)],[f253]) ).
fof(f256,plain,
! [X0,X1,X2] :
( ~ r1_lattices(X0,X1,X2)
| r3_lattices(X0,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v9_lattices(X0)
| ~ v8_lattices(X0)
| ~ v6_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f254]) ).
fof(f259,plain,
! [A,B,C] :
( r3_lattices(A,B,B)
| ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v9_lattices(A)
| ~ v8_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f75]) ).
fof(f260,plain,
! [A,B] :
( r3_lattices(A,B,B)
| ! [C] : ~ m1_subset_1(C,u1_struct_0(A))
| ~ m1_subset_1(B,u1_struct_0(A))
| ~ l3_lattices(A)
| ~ v9_lattices(A)
| ~ v8_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(miniscoping,[status(thm)],[f259]) ).
fof(f261,plain,
! [X0,X1,X2] :
( r3_lattices(X0,X1,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v9_lattices(X0)
| ~ v8_lattices(X0)
| ~ v6_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f260]) ).
fof(f262,plain,
! [A,B] :
( m1_subset_1(A,B)
| ~ r2_hidden(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f76]) ).
fof(f263,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f262]) ).
fof(f264,plain,
! [A] :
( ! [B] :
( ! [C] :
( r1_lattices(A,k4_lattices(A,B,C),B)
| ~ m1_subset_1(C,u1_struct_0(A)) )
| ~ m1_subset_1(B,u1_struct_0(A)) )
| ~ l3_lattices(A)
| ~ v8_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f77]) ).
fof(f265,plain,
! [X0,X1,X2] :
( r1_lattices(X0,k4_lattices(X0,X1,X2),X1)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v8_lattices(X0)
| ~ v6_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f264]) ).
fof(f266,plain,
! [A,B] :
( r2_hidden(A,B)
| v1_xboole_0(B)
| ~ m1_subset_1(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f78]) ).
fof(f267,plain,
! [X0,X1] :
( r2_hidden(X0,X1)
| v1_xboole_0(X1)
| ~ m1_subset_1(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f266]) ).
fof(f277,plain,
! [A,B,C] :
( m1_subset_1(A,C)
| ~ m1_subset_1(B,k1_zfmisc_1(C))
| ~ r2_hidden(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f81]) ).
fof(f278,plain,
! [A,C] :
( m1_subset_1(A,C)
| ! [B] :
( ~ m1_subset_1(B,k1_zfmisc_1(C))
| ~ r2_hidden(A,B) ) ),
inference(miniscoping,[status(thm)],[f277]) ).
fof(f279,plain,
! [X0,X1,X2] :
( m1_subset_1(X0,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f278]) ).
fof(f280,plain,
! [A,B,C] :
( ~ v1_xboole_0(C)
| ~ m1_subset_1(B,k1_zfmisc_1(C))
| ~ r2_hidden(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f82]) ).
fof(f281,plain,
! [C] :
( ~ v1_xboole_0(C)
| ! [B] :
( ~ m1_subset_1(B,k1_zfmisc_1(C))
| ! [A] : ~ r2_hidden(A,B) ) ),
inference(miniscoping,[status(thm)],[f280]) ).
fof(f282,plain,
! [X0,X1,X2] :
( ~ v1_xboole_0(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X2))
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f281]) ).
fof(f283,plain,
! [A] :
( A = k1_xboole_0
| ~ v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f83]) ).
fof(f284,plain,
! [X0] :
( X0 = k1_xboole_0
| ~ v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f283]) ).
fof(f285,plain,
! [A,B] :
( ~ v1_xboole_0(B)
| ~ r2_hidden(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f84]) ).
fof(f286,plain,
! [B] :
( ~ v1_xboole_0(B)
| ! [A] : ~ r2_hidden(A,B) ),
inference(miniscoping,[status(thm)],[f285]) ).
fof(f287,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f286]) ).
fof(f291,definition,
( sQ0_spl
<=> r2_hidden(sK1_skl,k18_filter_2(sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f293,plain,
( sQ0_spl
| ~ r2_hidden(sK1_skl,k18_filter_2(sK0_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f291]) ).
fof(f294,definition,
( sQ1_spl
<=> r2_hidden(k4_lattices(sK0_skl,sK1_skl,sK2_skl),k18_filter_2(sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f296,plain,
( sQ1_spl
| ~ r2_hidden(k4_lattices(sK0_skl,sK1_skl,sK2_skl),k18_filter_2(sK0_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f294]) ).
fof(f297,definition,
( sQ2_spl
<=> r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK1_skl),k18_filter_2(sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f298,plain,
( ~ sQ2_spl
| r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK1_skl),k18_filter_2(sK0_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f297]) ).
fof(f299,plain,
( sQ2_spl
| ~ r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK1_skl),k18_filter_2(sK0_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f297]) ).
fof(f300,plain,
( ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f93,f291,f294,f297]) ).
fof(f301,plain,
! [X0,X1,X2] :
( ~ r3_lattices(X0,X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| r2_hidden(X2,a_2_0_filter_2(X0,X1))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f205]) ).
fof(f323,plain,
! [X0] :
( k4_lattices(sK0_skl,X0,sK2_skl) = k4_lattices(sK0_skl,sK2_skl,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl))
| ~ l1_lattices(sK0_skl)
| ~ v6_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f120,f92]) ).
fof(f324,plain,
! [X0] :
( k4_lattices(sK0_skl,X0,sK1_skl) = k4_lattices(sK0_skl,sK1_skl,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl))
| ~ l1_lattices(sK0_skl)
| ~ v6_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f120,f91]) ).
fof(f325,definition,
( sQ6_spl
<=> v3_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f326,plain,
( ~ sQ6_spl
| v3_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f325]) ).
fof(f328,definition,
( sQ7_spl
<=> v6_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f331,definition,
( sQ8_spl
<=> l1_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f333,plain,
( sQ8_spl
| ~ l1_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f331]) ).
fof(f334,definition,
! [X0] :
( sQ9_spl
<=> ( k4_lattices(sK0_skl,X0,sK2_skl) = k4_lattices(sK0_skl,sK2_skl,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f335,plain,
! [X0] :
( ~ sQ9_spl
| k4_lattices(sK0_skl,X0,sK2_skl) = k4_lattices(sK0_skl,sK2_skl,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f334]) ).
fof(f337,plain,
( sQ9_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f323,f325,f328,f331,f334]) ).
fof(f338,definition,
! [X0] :
( sQ10_spl
<=> ( k4_lattices(sK0_skl,X0,sK1_skl) = k4_lattices(sK0_skl,sK1_skl,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f339,plain,
! [X0] :
( ~ sQ10_spl
| k4_lattices(sK0_skl,X0,sK1_skl) = k4_lattices(sK0_skl,sK1_skl,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f338]) ).
fof(f341,plain,
( sQ10_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f324,f325,f328,f331,f338]) ).
fof(f342,plain,
( ~ sQ6_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f326,f88]) ).
fof(f343,plain,
~ sQ6_spl,
inference(contradiction_clause,[status(thm)],[f342]) ).
fof(f346,plain,
( k18_filter_2(sK0_skl,sK1_skl) = a_2_0_filter_2(sK0_skl,sK1_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f127,f91]) ).
fof(f347,definition,
( sQ11_spl
<=> v10_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f349,plain,
( sQ11_spl
| ~ v10_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f347]) ).
fof(f350,definition,
( sQ12_spl
<=> l3_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f352,plain,
( sQ12_spl
| ~ l3_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f350]) ).
fof(f357,definition,
( sQ14_spl
<=> k18_filter_2(sK0_skl,sK1_skl) = a_2_0_filter_2(sK0_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f358,plain,
( ~ sQ14_spl
| k18_filter_2(sK0_skl,sK1_skl) = a_2_0_filter_2(sK0_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f357]) ).
fof(f360,plain,
( sQ14_spl
| ~ sQ12_spl
| ~ sQ11_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f346,f325,f347,f350,f357]) ).
fof(f361,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f352,f90]) ).
fof(f362,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f361]) ).
fof(f363,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f349,f89]) ).
fof(f364,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f363]) ).
fof(f379,plain,
( ~ sQ10_spl
| k4_lattices(sK0_skl,sK2_skl,sK1_skl) = k4_lattices(sK0_skl,sK1_skl,sK2_skl) ),
inference(resolution,[status(thm)],[f339,f92]) ).
fof(f381,plain,
( sQ2_spl
| ~ sQ14_spl
| ~ r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK1_skl),a_2_0_filter_2(sK0_skl,sK1_skl)) ),
inference(backward_demodulation,[status(thm)],[f358,f299]) ).
fof(f383,plain,
( ~ sQ9_spl
| k4_lattices(sK0_skl,sK1_skl,sK2_skl) = k4_lattices(sK0_skl,sK2_skl,sK1_skl) ),
inference(resolution,[status(thm)],[f335,f91]) ).
fof(f385,plain,
! [X0] :
( m1_subset_1(k4_lattices(sK0_skl,sK1_skl,X0),u1_struct_0(sK0_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl))
| ~ l1_lattices(sK0_skl)
| ~ v6_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f135,f91]) ).
fof(f390,definition,
! [X0] :
( sQ18_spl
<=> ( m1_subset_1(k4_lattices(sK0_skl,sK1_skl,X0),u1_struct_0(sK0_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f391,plain,
! [X0] :
( ~ sQ18_spl
| m1_subset_1(k4_lattices(sK0_skl,sK1_skl,X0),u1_struct_0(sK0_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f390]) ).
fof(f393,plain,
( sQ18_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f385,f325,f328,f331,f390]) ).
fof(f394,plain,
( ~ sQ18_spl
| m1_subset_1(k4_lattices(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f391,f92]) ).
fof(f396,plain,
( ~ sQ18_spl
| ~ sQ10_spl
| m1_subset_1(k4_lattices(sK0_skl,sK2_skl,sK1_skl),u1_struct_0(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f379,f394]) ).
fof(f424,plain,
( v6_lattices(sK0_skl)
| v3_struct_0(sK0_skl)
| ~ l3_lattices(sK0_skl) ),
inference(resolution,[status(thm)],[f102,f89]) ).
fof(f425,plain,
( sQ7_spl
| sQ6_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f424,f350,f325,f328]) ).
fof(f431,plain,
( v8_lattices(sK0_skl)
| v3_struct_0(sK0_skl)
| ~ l3_lattices(sK0_skl) ),
inference(resolution,[status(thm)],[f104,f89]) ).
fof(f432,definition,
( sQ24_spl
<=> v8_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f435,plain,
( sQ24_spl
| sQ6_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f431,f350,f325,f432]) ).
fof(f462,plain,
( sQ1_spl
| ~ sQ14_spl
| ~ r2_hidden(k4_lattices(sK0_skl,sK1_skl,sK2_skl),a_2_0_filter_2(sK0_skl,sK1_skl)) ),
inference(forward_demodulation,[status(thm)],[f358,f296]) ).
fof(f463,plain,
( sQ0_spl
| ~ sQ14_spl
| ~ r2_hidden(sK1_skl,a_2_0_filter_2(sK0_skl,sK1_skl)) ),
inference(forward_demodulation,[status(thm)],[f358,f293]) ).
fof(f473,plain,
( sQ1_spl
| ~ sQ14_spl
| ~ sQ9_spl
| ~ r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK1_skl),a_2_0_filter_2(sK0_skl,sK1_skl)) ),
inference(backward_demodulation,[status(thm)],[f383,f462]) ).
fof(f480,plain,
l1_struct_0(sK3_skl),
inference(resolution,[status(thm)],[f137,f155]) ).
fof(f481,plain,
l1_struct_0(sK5_skl),
inference(resolution,[status(thm)],[f139,f159]) ).
fof(f482,plain,
l1_lattices(sK6_skl),
inference(resolution,[status(thm)],[f141,f161]) ).
fof(f483,plain,
l1_lattices(sK0_skl),
inference(resolution,[status(thm)],[f141,f90]) ).
fof(f484,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f483,f333]) ).
fof(f485,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f484]) ).
fof(f488,plain,
l1_struct_0(sK6_skl),
inference(resolution,[status(thm)],[f482,f137]) ).
fof(f489,plain,
l1_struct_0(sK0_skl),
inference(resolution,[status(thm)],[f483,f137]) ).
fof(f490,plain,
( v9_lattices(sK0_skl)
| v3_struct_0(sK0_skl)
| ~ l3_lattices(sK0_skl) ),
inference(resolution,[status(thm)],[f105,f89]) ).
fof(f491,definition,
( sQ29_spl
<=> v9_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f494,plain,
( sQ29_spl
| sQ6_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f490,f350,f325,f491]) ).
fof(f500,definition,
( sQ30_spl
<=> v1_relat_1(sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f502,plain,
( sQ30_spl
| ~ v1_relat_1(sK18_skl) ),
inference(component_clause,[status(thm)],[f500]) ).
fof(f521,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f502,f223]) ).
fof(f522,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f521]) ).
fof(f604,plain,
! [X0] :
( r2_hidden(sK8_skl(X0),X0)
| v1_xboole_0(X0) ),
inference(resolution,[status(thm)],[f165,f267]) ).
fof(f607,plain,
sK18_skl = k1_xboole_0,
inference(resolution,[status(thm)],[f284,f224]) ).
fof(f610,plain,
! [X0] :
( X0 = sK18_skl
| ~ v1_xboole_0(X0) ),
inference(backward_demodulation,[status(thm)],[f607,f284]) ).
fof(f707,definition,
( sQ53_spl
<=> v1_relat_1(sK22_skl) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f709,plain,
( sQ53_spl
| ~ v1_relat_1(sK22_skl) ),
inference(component_clause,[status(thm)],[f707]) ).
fof(f718,definition,
( sQ56_spl
<=> v1_relat_1(sK13_skl) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f720,plain,
( sQ56_spl
| ~ v1_relat_1(sK13_skl) ),
inference(component_clause,[status(thm)],[f718]) ).
fof(f725,plain,
( sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f720,f207]) ).
fof(f726,plain,
sQ56_spl,
inference(contradiction_clause,[status(thm)],[f725]) ).
fof(f727,plain,
( sQ53_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f709,f235]) ).
fof(f728,plain,
sQ53_spl,
inference(contradiction_clause,[status(thm)],[f727]) ).
fof(f730,definition,
( sQ58_spl
<=> v1_xboole_0(sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f732,plain,
( sQ58_spl
| ~ v1_xboole_0(sK18_skl) ),
inference(component_clause,[status(thm)],[f730]) ).
fof(f747,definition,
( sQ61_spl
<=> r2_hidden(k4_lattices(sK0_skl,sK1_skl,sK1_skl),sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f748,plain,
( ~ sQ61_spl
| r2_hidden(k4_lattices(sK0_skl,sK1_skl,sK1_skl),sK18_skl) ),
inference(component_clause,[status(thm)],[f747]) ).
fof(f761,definition,
( sQ62_spl
<=> r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK2_skl),sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f762,plain,
( ~ sQ62_spl
| r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK2_skl),sK18_skl) ),
inference(component_clause,[status(thm)],[f761]) ).
fof(f767,definition,
( sQ63_spl
<=> r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK1_skl),sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f768,plain,
( ~ sQ63_spl
| r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK1_skl),sK18_skl) ),
inference(component_clause,[status(thm)],[f767]) ).
fof(f773,plain,
( ~ sQ61_spl
| ~ v1_xboole_0(sK18_skl) ),
inference(resolution,[status(thm)],[f748,f287]) ).
fof(f774,plain,
( ~ sQ61_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f773,f224]) ).
fof(f775,plain,
~ sQ61_spl,
inference(contradiction_clause,[status(thm)],[f774]) ).
fof(f778,plain,
( ~ sQ62_spl
| ~ v1_xboole_0(sK18_skl) ),
inference(resolution,[status(thm)],[f762,f287]) ).
fof(f779,plain,
( ~ sQ62_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f778,f224]) ).
fof(f780,plain,
~ sQ62_spl,
inference(contradiction_clause,[status(thm)],[f779]) ).
fof(f783,plain,
( ~ sQ63_spl
| ~ v1_xboole_0(sK18_skl) ),
inference(resolution,[status(thm)],[f768,f287]) ).
fof(f784,plain,
( ~ sQ63_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f783,f224]) ).
fof(f785,plain,
~ sQ63_spl,
inference(contradiction_clause,[status(thm)],[f784]) ).
fof(f808,definition,
( sQ66_spl
<=> l3_lattices(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f810,plain,
( sQ66_spl
| ~ l3_lattices(sK6_skl) ),
inference(component_clause,[status(thm)],[f808]) ).
fof(f821,plain,
( sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f810,f161]) ).
fof(f822,plain,
sQ66_spl,
inference(contradiction_clause,[status(thm)],[f821]) ).
fof(f824,plain,
v1_funct_1(u1_lattices(sK0_skl)),
inference(resolution,[status(thm)],[f151,f483]) ).
fof(f825,plain,
v1_funct_1(u1_lattices(sK6_skl)),
inference(resolution,[status(thm)],[f151,f482]) ).
fof(f826,plain,
v1_funct_1(u1_lattices(sK3_skl)),
inference(resolution,[status(thm)],[f151,f155]) ).
fof(f890,definition,
( sQ76_spl
<=> r2_hidden(k4_lattices(sK0_skl,sK1_skl,sK8_skl(sK18_skl)),sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f891,plain,
( ~ sQ76_spl
| r2_hidden(k4_lattices(sK0_skl,sK1_skl,sK8_skl(sK18_skl)),sK18_skl) ),
inference(component_clause,[status(thm)],[f890]) ).
fof(f912,plain,
( ~ sQ76_spl
| ~ v1_xboole_0(sK18_skl) ),
inference(resolution,[status(thm)],[f891,f287]) ).
fof(f913,plain,
( ~ sQ76_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f912,f224]) ).
fof(f914,plain,
~ sQ76_spl,
inference(contradiction_clause,[status(thm)],[f913]) ).
fof(f919,definition,
( sQ77_spl
<=> r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK8_skl(sK18_skl)),sK18_skl) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f920,plain,
( ~ sQ77_spl
| r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK8_skl(sK18_skl)),sK18_skl) ),
inference(component_clause,[status(thm)],[f919]) ).
fof(f925,plain,
( ~ sQ77_spl
| ~ v1_xboole_0(sK18_skl) ),
inference(resolution,[status(thm)],[f920,f287]) ).
fof(f926,plain,
( ~ sQ77_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f925,f224]) ).
fof(f927,plain,
~ sQ77_spl,
inference(contradiction_clause,[status(thm)],[f926]) ).
fof(f1031,definition,
( sQ87_spl
<=> l1_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f1033,plain,
( sQ87_spl
| ~ l1_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f1031]) ).
fof(f1035,plain,
( sQ87_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1033,f489]) ).
fof(f1036,plain,
sQ87_spl,
inference(contradiction_clause,[status(thm)],[f1035]) ).
fof(f1037,plain,
! [X0] :
( m1_subset_1(k2_lattices(sK0_skl,sK2_skl,X0),u1_struct_0(sK0_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl))
| ~ l1_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f92,f133]) ).
fof(f1046,definition,
! [X0] :
( sQ88_spl
<=> ( m1_subset_1(k2_lattices(sK0_skl,sK2_skl,X0),u1_struct_0(sK0_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f1047,plain,
! [X0] :
( ~ sQ88_spl
| m1_subset_1(k2_lattices(sK0_skl,sK2_skl,X0),u1_struct_0(sK0_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1046]) ).
fof(f1049,plain,
( sQ88_spl
| ~ sQ8_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f1037,f325,f331,f1046]) ).
fof(f1266,plain,
! [X0] :
( r2_hidden(sK16_skl(X0),k1_zfmisc_1(X0))
| v1_xboole_0(k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(resolution,[status(thm)],[f218,f267]) ).
fof(f1267,plain,
! [X0] :
( r2_hidden(sK16_skl(X0),k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1266,f176]) ).
fof(f1316,definition,
( sQ121_spl
<=> v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f1317,plain,
( ~ sQ121_spl
| v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK0_skl))) ),
inference(component_clause,[status(thm)],[f1316]) ).
fof(f1323,plain,
( ~ sQ121_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1317,f176]) ).
fof(f1324,plain,
~ sQ121_spl,
inference(contradiction_clause,[status(thm)],[f1323]) ).
fof(f1352,plain,
( ~ sQ88_spl
| m1_subset_1(k2_lattices(sK0_skl,sK2_skl,sK1_skl),u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f1047,f91]) ).
fof(f1368,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ r2_hidden(X0,sK8_skl(k1_zfmisc_1(X1))) ),
inference(resolution,[status(thm)],[f282,f165]) ).
fof(f1385,definition,
! [X1] :
( sQ129_spl
<=> ~ v1_xboole_0(X1) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f1386,plain,
! [X0] :
( ~ sQ129_spl
| ~ v1_xboole_0(X0) ),
inference(component_clause,[status(thm)],[f1385]) ).
fof(f1397,plain,
( ~ sQ129_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f224,f1386]) ).
fof(f1399,plain,
~ sQ129_spl,
inference(contradiction_clause,[status(thm)],[f1397]) ).
fof(f1447,plain,
! [X0] :
( m1_subset_1(sK16_skl(X0),k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(resolution,[status(thm)],[f1267,f263]) ).
fof(f1481,plain,
! [X0] :
( v1_xboole_0(sK8_skl(k1_zfmisc_1(X0)))
| ~ v1_xboole_0(X0) ),
inference(resolution,[status(thm)],[f1368,f604]) ).
fof(f1482,plain,
v1_xboole_0(sK8_skl(k1_zfmisc_1(sK18_skl))),
inference(resolution,[status(thm)],[f1481,f224]) ).
fof(f1488,plain,
sK8_skl(k1_zfmisc_1(sK18_skl)) = sK18_skl,
inference(resolution,[status(thm)],[f1482,f610]) ).
fof(f1489,definition,
( sQ132_spl
<=> v1_relat_1(sK8_skl(k1_zfmisc_1(sK18_skl))) ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f1491,plain,
( sQ132_spl
| ~ v1_relat_1(sK8_skl(k1_zfmisc_1(sK18_skl))) ),
inference(component_clause,[status(thm)],[f1489]) ).
fof(f1510,definition,
( sQ135_spl
<=> v1_xboole_0(k1_zfmisc_1(sK18_skl)) ),
introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition]) ).
fof(f1511,plain,
( ~ sQ135_spl
| v1_xboole_0(k1_zfmisc_1(sK18_skl)) ),
inference(component_clause,[status(thm)],[f1510]) ).
fof(f1521,plain,
( ~ sQ135_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1511,f176]) ).
fof(f1522,plain,
~ sQ135_spl,
inference(contradiction_clause,[status(thm)],[f1521]) ).
fof(f1523,plain,
( sQ132_spl
| ~ v1_relat_1(sK18_skl) ),
inference(forward_demodulation,[status(thm)],[f1488,f1491]) ).
fof(f1524,plain,
( sQ132_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1523,f223]) ).
fof(f1525,plain,
sQ132_spl,
inference(contradiction_clause,[status(thm)],[f1524]) ).
fof(f1954,plain,
! [X0,X1] :
( v1_xboole_0(X1)
| m1_subset_1(X0,X1)
| ~ r2_hidden(X0,sK16_skl(X1)) ),
inference(resolution,[status(thm)],[f279,f1447]) ).
fof(f1966,plain,
! [X0] :
( v1_xboole_0(sK16_skl(X0))
| v1_xboole_0(X0)
| m1_subset_1(sK8_skl(sK16_skl(X0)),X0) ),
inference(resolution,[status(thm)],[f1954,f604]) ).
fof(f1967,plain,
! [X0] :
( v1_xboole_0(X0)
| m1_subset_1(sK8_skl(sK16_skl(X0)),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1966,f219]) ).
fof(f1971,plain,
! [X0,X1] :
( ~ v1_xboole_0(X0)
| ~ r2_hidden(X1,sK8_skl(sK16_skl(k1_zfmisc_1(X0))))
| v1_xboole_0(k1_zfmisc_1(X0)) ),
inference(resolution,[status(thm)],[f1967,f282]) ).
fof(f1989,plain,
! [X0] :
( r2_hidden(sK8_skl(sK16_skl(X0)),X0)
| v1_xboole_0(X0)
| v1_xboole_0(X0) ),
inference(resolution,[status(thm)],[f1967,f267]) ).
fof(f1996,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ r2_hidden(X0,sK8_skl(sK16_skl(k1_zfmisc_1(X1)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f1971,f176]) ).
fof(f2030,plain,
! [X0] :
( r2_hidden(sK8_skl(sK16_skl(X0)),X0)
| v1_xboole_0(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1989]) ).
fof(f2065,plain,
! [X0] :
( v1_xboole_0(sK8_skl(sK16_skl(k1_zfmisc_1(X0))))
| ~ v1_xboole_0(X0) ),
inference(resolution,[status(thm)],[f1996,f2030]) ).
fof(f2067,plain,
v1_xboole_0(sK8_skl(sK16_skl(k1_zfmisc_1(sK18_skl)))),
inference(resolution,[status(thm)],[f2065,f224]) ).
fof(f2074,plain,
sK8_skl(sK16_skl(k1_zfmisc_1(sK18_skl))) = sK18_skl,
inference(resolution,[status(thm)],[f2067,f610]) ).
fof(f2075,definition,
( sQ209_spl
<=> v1_relat_1(sK8_skl(sK16_skl(k1_zfmisc_1(sK18_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition]) ).
fof(f2077,plain,
( sQ209_spl
| ~ v1_relat_1(sK8_skl(sK16_skl(k1_zfmisc_1(sK18_skl)))) ),
inference(component_clause,[status(thm)],[f2075]) ).
fof(f2134,plain,
( sQ209_spl
| ~ v1_relat_1(sK18_skl) ),
inference(forward_demodulation,[status(thm)],[f2074,f2077]) ).
fof(f2135,plain,
( sQ209_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2134,f223]) ).
fof(f2136,plain,
sQ209_spl,
inference(contradiction_clause,[status(thm)],[f2135]) ).
fof(f2233,plain,
! [X0] :
( ~ r3_lattices(sK0_skl,X0,sK1_skl)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl))
| r2_hidden(X0,a_2_0_filter_2(sK0_skl,sK1_skl))
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f301,f91]) ).
fof(f2274,definition,
! [X0] :
( sQ235_spl
<=> ( ~ r3_lattices(sK0_skl,X0,sK1_skl)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl))
| r2_hidden(X0,a_2_0_filter_2(sK0_skl,sK1_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ235_spl])],[split_symbol_definition]) ).
fof(f2275,plain,
! [X0] :
( ~ sQ235_spl
| ~ r3_lattices(sK0_skl,X0,sK1_skl)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl))
| r2_hidden(X0,a_2_0_filter_2(sK0_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f2274]) ).
fof(f2277,plain,
( sQ235_spl
| ~ sQ12_spl
| ~ sQ11_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f2233,f325,f347,f350,f2274]) ).
fof(f2379,plain,
( ~ sQ18_spl
| ~ sQ10_spl
| ~ sQ235_spl
| ~ r3_lattices(sK0_skl,k4_lattices(sK0_skl,sK2_skl,sK1_skl),sK1_skl)
| r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK1_skl),a_2_0_filter_2(sK0_skl,sK1_skl)) ),
inference(resolution,[status(thm)],[f2275,f396]) ).
fof(f2383,plain,
( ~ sQ235_spl
| ~ r3_lattices(sK0_skl,sK1_skl,sK1_skl)
| r2_hidden(sK1_skl,a_2_0_filter_2(sK0_skl,sK1_skl)) ),
inference(resolution,[status(thm)],[f2275,f91]) ).
fof(f2413,definition,
( sQ259_spl
<=> r3_lattices(sK0_skl,k2_lattices(sK0_skl,sK2_skl,sK1_skl),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition]) ).
fof(f2424,definition,
( sQ262_spl
<=> r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK1_skl),a_2_0_filter_2(sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ262_spl])],[split_symbol_definition]) ).
fof(f2425,plain,
( ~ sQ262_spl
| r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK1_skl),a_2_0_filter_2(sK0_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f2424]) ).
fof(f2427,definition,
( sQ263_spl
<=> r3_lattices(sK0_skl,k4_lattices(sK0_skl,sK2_skl,sK1_skl),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ263_spl])],[split_symbol_definition]) ).
fof(f2429,plain,
( sQ263_spl
| ~ r3_lattices(sK0_skl,k4_lattices(sK0_skl,sK2_skl,sK1_skl),sK1_skl) ),
inference(component_clause,[status(thm)],[f2427]) ).
fof(f2430,plain,
( ~ sQ18_spl
| ~ sQ10_spl
| ~ sQ235_spl
| ~ sQ263_spl
| sQ262_spl ),
inference(split_clause,[status(thm)],[f2379,f2424,f2427,f2274,f338,f390]) ).
fof(f2452,definition,
( sQ270_spl
<=> r2_hidden(sK1_skl,a_2_0_filter_2(sK0_skl,sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ270_spl])],[split_symbol_definition]) ).
fof(f2453,plain,
( ~ sQ270_spl
| r2_hidden(sK1_skl,a_2_0_filter_2(sK0_skl,sK1_skl)) ),
inference(component_clause,[status(thm)],[f2452]) ).
fof(f2455,definition,
( sQ271_spl
<=> r3_lattices(sK0_skl,sK1_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ271_spl])],[split_symbol_definition]) ).
fof(f2457,plain,
( sQ271_spl
| ~ r3_lattices(sK0_skl,sK1_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f2455]) ).
fof(f2458,plain,
( ~ sQ235_spl
| ~ sQ271_spl
| sQ270_spl ),
inference(split_clause,[status(thm)],[f2383,f2452,f2455,f2274]) ).
fof(f2494,plain,
( ~ sQ262_spl
| sQ2_spl
| ~ sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2425,f381]) ).
fof(f2495,plain,
( ~ sQ262_spl
| sQ2_spl
| ~ sQ14_spl ),
inference(contradiction_clause,[status(thm)],[f2494]) ).
fof(f2496,plain,
( ~ sQ2_spl
| ~ sQ14_spl
| r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK1_skl),a_2_0_filter_2(sK0_skl,sK1_skl)) ),
inference(forward_demodulation,[status(thm)],[f358,f298]) ).
fof(f2503,definition,
( sQ282_spl
<=> m1_subset_1(sK1_skl,u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ282_spl])],[split_symbol_definition]) ).
fof(f2505,plain,
( sQ282_spl
| ~ m1_subset_1(sK1_skl,u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f2503]) ).
fof(f2518,plain,
( sQ282_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2505,f91]) ).
fof(f2519,plain,
sQ282_spl,
inference(contradiction_clause,[status(thm)],[f2518]) ).
fof(f2538,plain,
( sQ0_spl
| ~ sQ14_spl
| ~ sQ270_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f463,f2453]) ).
fof(f2539,plain,
( sQ0_spl
| ~ sQ14_spl
| ~ sQ270_spl ),
inference(contradiction_clause,[status(thm)],[f2538]) ).
fof(f2690,definition,
( sQ314_spl
<=> v3_struct_0(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ314_spl])],[split_symbol_definition]) ).
fof(f2691,plain,
( ~ sQ314_spl
| v3_struct_0(sK23_skl) ),
inference(component_clause,[status(thm)],[f2690]) ).
fof(f2704,plain,
( ~ sQ314_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2691,f240]) ).
fof(f2705,plain,
~ sQ314_spl,
inference(contradiction_clause,[status(thm)],[f2704]) ).
fof(f2986,definition,
( sQ372_spl
<=> m1_subset_1(sK2_skl,u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ372_spl])],[split_symbol_definition]) ).
fof(f2988,plain,
( sQ372_spl
| ~ m1_subset_1(sK2_skl,u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f2986]) ).
fof(f3001,plain,
( sQ372_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2988,f92]) ).
fof(f3002,plain,
sQ372_spl,
inference(contradiction_clause,[status(thm)],[f3001]) ).
fof(f3036,definition,
( sQ381_spl
<=> v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK4_skl))) ),
introduced(definition,[new_symbols(definition,[sQ381_spl])],[split_symbol_definition]) ).
fof(f3037,plain,
( ~ sQ381_spl
| v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK4_skl))) ),
inference(component_clause,[status(thm)],[f3036]) ).
fof(f3043,plain,
( ~ sQ381_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3037,f176]) ).
fof(f3044,plain,
~ sQ381_spl,
inference(contradiction_clause,[status(thm)],[f3043]) ).
fof(f3054,plain,
! [X0] :
( k4_lattices(sK0_skl,X0,sK1_skl) = k2_lattices(sK0_skl,X0,sK1_skl)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl))
| ~ l1_lattices(sK0_skl)
| ~ v6_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f248,f91]) ).
fof(f3097,definition,
! [X0] :
( sQ392_spl
<=> ( k4_lattices(sK0_skl,X0,sK1_skl) = k2_lattices(sK0_skl,X0,sK1_skl)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ392_spl])],[split_symbol_definition]) ).
fof(f3098,plain,
! [X0] :
( ~ sQ392_spl
| k4_lattices(sK0_skl,X0,sK1_skl) = k2_lattices(sK0_skl,X0,sK1_skl)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f3097]) ).
fof(f3100,plain,
( sQ392_spl
| ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f3054,f325,f328,f331,f3097]) ).
fof(f3190,plain,
! [X0] :
( ~ r1_lattices(sK0_skl,X0,sK1_skl)
| r3_lattices(sK0_skl,X0,sK1_skl)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v9_lattices(sK0_skl)
| ~ v8_lattices(sK0_skl)
| ~ v6_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f256,f91]) ).
fof(f3233,definition,
! [X0] :
( sQ418_spl
<=> ( ~ r1_lattices(sK0_skl,X0,sK1_skl)
| r3_lattices(sK0_skl,X0,sK1_skl)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ418_spl])],[split_symbol_definition]) ).
fof(f3234,plain,
! [X0] :
( ~ sQ418_spl
| ~ r1_lattices(sK0_skl,X0,sK1_skl)
| r3_lattices(sK0_skl,X0,sK1_skl)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f3233]) ).
fof(f3236,plain,
( sQ418_spl
| ~ sQ12_spl
| ~ sQ29_spl
| ~ sQ24_spl
| ~ sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f3190,f325,f328,f432,f491,f350,f3233]) ).
fof(f3390,plain,
( ~ sQ392_spl
| k4_lattices(sK0_skl,sK2_skl,sK1_skl) = k2_lattices(sK0_skl,sK2_skl,sK1_skl) ),
inference(resolution,[status(thm)],[f3098,f92]) ).
fof(f3416,definition,
( sQ445_spl
<=> l1_struct_0(sK4_skl) ),
introduced(definition,[new_symbols(definition,[sQ445_spl])],[split_symbol_definition]) ).
fof(f3418,plain,
( sQ445_spl
| ~ l1_struct_0(sK4_skl) ),
inference(component_clause,[status(thm)],[f3416]) ).
fof(f3427,plain,
( sQ445_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3418,f157]) ).
fof(f3428,plain,
sQ445_spl,
inference(contradiction_clause,[status(thm)],[f3427]) ).
fof(f3440,definition,
( sQ450_spl
<=> v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK23_skl))) ),
introduced(definition,[new_symbols(definition,[sQ450_spl])],[split_symbol_definition]) ).
fof(f3441,plain,
( ~ sQ450_spl
| v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK23_skl))) ),
inference(component_clause,[status(thm)],[f3440]) ).
fof(f3447,plain,
( ~ sQ450_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3441,f176]) ).
fof(f3448,plain,
~ sQ450_spl,
inference(contradiction_clause,[status(thm)],[f3447]) ).
fof(f3460,definition,
( sQ452_spl
<=> l1_struct_0(sK23_skl) ),
introduced(definition,[new_symbols(definition,[sQ452_spl])],[split_symbol_definition]) ).
fof(f3462,plain,
( sQ452_spl
| ~ l1_struct_0(sK23_skl) ),
inference(component_clause,[status(thm)],[f3460]) ).
fof(f3471,plain,
( sQ452_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3462,f239]) ).
fof(f3472,plain,
sQ452_spl,
inference(contradiction_clause,[status(thm)],[f3471]) ).
fof(f3485,definition,
( sQ457_spl
<=> v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK3_skl))) ),
introduced(definition,[new_symbols(definition,[sQ457_spl])],[split_symbol_definition]) ).
fof(f3486,plain,
( ~ sQ457_spl
| v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK3_skl))) ),
inference(component_clause,[status(thm)],[f3485]) ).
fof(f3492,plain,
( ~ sQ457_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3486,f176]) ).
fof(f3493,plain,
~ sQ457_spl,
inference(contradiction_clause,[status(thm)],[f3492]) ).
fof(f3505,definition,
( sQ459_spl
<=> l1_struct_0(sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ459_spl])],[split_symbol_definition]) ).
fof(f3507,plain,
( sQ459_spl
| ~ l1_struct_0(sK3_skl) ),
inference(component_clause,[status(thm)],[f3505]) ).
fof(f3516,plain,
( sQ459_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3507,f480]) ).
fof(f3517,plain,
sQ459_spl,
inference(contradiction_clause,[status(thm)],[f3516]) ).
fof(f3527,plain,
! [X0] :
( r3_lattices(sK0_skl,X0,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v9_lattices(sK0_skl)
| ~ v8_lattices(sK0_skl)
| ~ v6_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f261,f91]) ).
fof(f3535,definition,
! [X0] :
( sQ462_spl
<=> ( r3_lattices(sK0_skl,X0,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ462_spl])],[split_symbol_definition]) ).
fof(f3536,plain,
! [X0] :
( ~ sQ462_spl
| r3_lattices(sK0_skl,X0,X0)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f3535]) ).
fof(f3547,plain,
( sQ462_spl
| ~ sQ12_spl
| ~ sQ29_spl
| ~ sQ24_spl
| ~ sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f3527,f325,f328,f432,f491,f350,f3535]) ).
fof(f3561,plain,
! [X0] :
( r1_lattices(sK0_skl,k4_lattices(sK0_skl,sK1_skl,X0),sK1_skl)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl))
| ~ l3_lattices(sK0_skl)
| ~ v8_lattices(sK0_skl)
| ~ v6_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f265,f91]) ).
fof(f3605,definition,
! [X0] :
( sQ472_spl
<=> ( r1_lattices(sK0_skl,k4_lattices(sK0_skl,sK1_skl,X0),sK1_skl)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ472_spl])],[split_symbol_definition]) ).
fof(f3606,plain,
! [X0] :
( ~ sQ472_spl
| r1_lattices(sK0_skl,k4_lattices(sK0_skl,sK1_skl,X0),sK1_skl)
| ~ m1_subset_1(X0,u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f3605]) ).
fof(f3608,plain,
( sQ472_spl
| ~ sQ12_spl
| ~ sQ24_spl
| ~ sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f3561,f325,f328,f432,f350,f3605]) ).
fof(f3702,plain,
( ~ sQ462_spl
| r3_lattices(sK0_skl,sK1_skl,sK1_skl) ),
inference(resolution,[status(thm)],[f3536,f91]) ).
fof(f3710,plain,
( ~ sQ462_spl
| sQ271_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3702,f2457]) ).
fof(f3711,plain,
( ~ sQ462_spl
| sQ271_spl ),
inference(contradiction_clause,[status(thm)],[f3710]) ).
fof(f3843,definition,
( sQ492_spl
<=> r1_lattices(sK0_skl,k2_lattices(sK0_skl,sK2_skl,sK1_skl),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ492_spl])],[split_symbol_definition]) ).
fof(f4334,definition,
( sQ543_spl
<=> v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK5_skl))) ),
introduced(definition,[new_symbols(definition,[sQ543_spl])],[split_symbol_definition]) ).
fof(f4335,plain,
( ~ sQ543_spl
| v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK5_skl))) ),
inference(component_clause,[status(thm)],[f4334]) ).
fof(f4341,plain,
( ~ sQ543_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4335,f176]) ).
fof(f4342,plain,
~ sQ543_spl,
inference(contradiction_clause,[status(thm)],[f4341]) ).
fof(f4354,definition,
( sQ545_spl
<=> l1_struct_0(sK5_skl) ),
introduced(definition,[new_symbols(definition,[sQ545_spl])],[split_symbol_definition]) ).
fof(f4356,plain,
( sQ545_spl
| ~ l1_struct_0(sK5_skl) ),
inference(component_clause,[status(thm)],[f4354]) ).
fof(f4358,plain,
( sQ545_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4356,f481]) ).
fof(f4359,plain,
sQ545_spl,
inference(contradiction_clause,[status(thm)],[f4358]) ).
fof(f4371,definition,
( sQ548_spl
<=> v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK6_skl))) ),
introduced(definition,[new_symbols(definition,[sQ548_spl])],[split_symbol_definition]) ).
fof(f4372,plain,
( ~ sQ548_spl
| v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK6_skl))) ),
inference(component_clause,[status(thm)],[f4371]) ).
fof(f4378,plain,
( ~ sQ548_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4372,f176]) ).
fof(f4379,plain,
~ sQ548_spl,
inference(contradiction_clause,[status(thm)],[f4378]) ).
fof(f4391,definition,
( sQ550_spl
<=> l1_struct_0(sK6_skl) ),
introduced(definition,[new_symbols(definition,[sQ550_spl])],[split_symbol_definition]) ).
fof(f4393,plain,
( sQ550_spl
| ~ l1_struct_0(sK6_skl) ),
inference(component_clause,[status(thm)],[f4391]) ).
fof(f4395,plain,
( sQ550_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4393,f488]) ).
fof(f4396,plain,
sQ550_spl,
inference(contradiction_clause,[status(thm)],[f4395]) ).
fof(f4502,plain,
( ~ sQ472_spl
| r1_lattices(sK0_skl,k4_lattices(sK0_skl,sK1_skl,sK2_skl),sK1_skl) ),
inference(resolution,[status(thm)],[f3606,f92]) ).
fof(f4515,plain,
( ~ sQ472_spl
| ~ sQ9_spl
| r1_lattices(sK0_skl,k4_lattices(sK0_skl,sK2_skl,sK1_skl),sK1_skl) ),
inference(forward_demodulation,[status(thm)],[f383,f4502]) ).
fof(f4609,definition,
( sQ568_spl
<=> v1_funct_1(u1_lattices(sK3_skl)) ),
introduced(definition,[new_symbols(definition,[sQ568_spl])],[split_symbol_definition]) ).
fof(f4611,plain,
( sQ568_spl
| ~ v1_funct_1(u1_lattices(sK3_skl)) ),
inference(component_clause,[status(thm)],[f4609]) ).
fof(f4623,plain,
( sQ568_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4611,f826]) ).
fof(f4624,plain,
sQ568_spl,
inference(contradiction_clause,[status(thm)],[f4623]) ).
fof(f5289,plain,
( sQ58_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f732,f224]) ).
fof(f5290,plain,
sQ58_spl,
inference(contradiction_clause,[status(thm)],[f5289]) ).
fof(f7253,definition,
( sQ894_spl
<=> v1_funct_1(u1_lattices(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ894_spl])],[split_symbol_definition]) ).
fof(f7255,plain,
( sQ894_spl
| ~ v1_funct_1(u1_lattices(sK0_skl)) ),
inference(component_clause,[status(thm)],[f7253]) ).
fof(f7267,plain,
( sQ894_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7255,f824]) ).
fof(f7268,plain,
sQ894_spl,
inference(contradiction_clause,[status(thm)],[f7267]) ).
fof(f7280,definition,
( sQ898_spl
<=> v1_funct_1(u1_lattices(sK6_skl)) ),
introduced(definition,[new_symbols(definition,[sQ898_spl])],[split_symbol_definition]) ).
fof(f7282,plain,
( sQ898_spl
| ~ v1_funct_1(u1_lattices(sK6_skl)) ),
inference(component_clause,[status(thm)],[f7280]) ).
fof(f7294,plain,
( sQ898_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f7282,f825]) ).
fof(f7295,plain,
sQ898_spl,
inference(contradiction_clause,[status(thm)],[f7294]) ).
fof(f8131,plain,
( ~ sQ418_spl
| ~ sQ88_spl
| ~ r1_lattices(sK0_skl,k2_lattices(sK0_skl,sK2_skl,sK1_skl),sK1_skl)
| r3_lattices(sK0_skl,k2_lattices(sK0_skl,sK2_skl,sK1_skl),sK1_skl) ),
inference(resolution,[status(thm)],[f1352,f3234]) ).
fof(f8162,plain,
( ~ sQ418_spl
| ~ sQ88_spl
| ~ sQ492_spl
| sQ259_spl ),
inference(split_clause,[status(thm)],[f8131,f2413,f3843,f1046,f3233]) ).
fof(f11449,plain,
( ~ sQ472_spl
| ~ sQ9_spl
| ~ sQ392_spl
| r1_lattices(sK0_skl,k2_lattices(sK0_skl,sK2_skl,sK1_skl),sK1_skl) ),
inference(backward_demodulation,[status(thm)],[f3390,f4515]) ).
fof(f11454,plain,
( sQ263_spl
| ~ sQ392_spl
| ~ r3_lattices(sK0_skl,k2_lattices(sK0_skl,sK2_skl,sK1_skl),sK1_skl) ),
inference(backward_demodulation,[status(thm)],[f3390,f2429]) ).
fof(f11457,plain,
( sQ1_spl
| ~ sQ14_spl
| ~ sQ9_spl
| ~ sQ392_spl
| ~ r2_hidden(k2_lattices(sK0_skl,sK2_skl,sK1_skl),a_2_0_filter_2(sK0_skl,sK1_skl)) ),
inference(backward_demodulation,[status(thm)],[f3390,f473]) ).
fof(f11461,plain,
( ~ sQ472_spl
| ~ sQ9_spl
| ~ sQ392_spl
| sQ492_spl ),
inference(split_clause,[status(thm)],[f11449,f3843,f3097,f334,f3605]) ).
fof(f11464,plain,
( sQ263_spl
| ~ sQ392_spl
| ~ sQ259_spl ),
inference(split_clause,[status(thm)],[f11454,f2413,f3097,f2427]) ).
fof(f11661,plain,
( ~ sQ2_spl
| ~ sQ14_spl
| ~ sQ392_spl
| r2_hidden(k2_lattices(sK0_skl,sK2_skl,sK1_skl),a_2_0_filter_2(sK0_skl,sK1_skl)) ),
inference(forward_demodulation,[status(thm)],[f3390,f2496]) ).
fof(f11689,plain,
( ~ sQ2_spl
| ~ sQ14_spl
| ~ sQ392_spl
| sQ1_spl
| ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11661,f11457]) ).
fof(f11690,plain,
( ~ sQ2_spl
| ~ sQ14_spl
| ~ sQ392_spl
| sQ1_spl
| ~ sQ9_spl ),
inference(contradiction_clause,[status(thm)],[f11689]) ).
fof(f11691,plain,
$false,
inference(sat_refutation,[status(thm)],[f300,f337,f341,f343,f360,f362,f364,f393,f425,f435,f485,f494,f522,f726,f728,f775,f780,f785,f822,f914,f927,f1036,f1049,f1324,f1399,f1522,f1525,f2136,f2277,f2430,f2458,f2495,f2519,f2539,f2705,f3002,f3044,f3100,f3236,f3428,f3448,f3472,f3493,f3517,f3547,f3608,f3711,f4342,f4359,f4379,f4396,f4624,f5290,f7268,f7295,f8162,f11461,f11464,f11690]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT305+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/10.50 % Computer : n002.cluster.edu
% 0.20/10.50 % Model : x86_64 x86_64
% 0.20/10.50 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/10.50 % Memory : 8046.5625MB
% 0.20/10.50 % OS : Linux 6.8.0-71-generic
% 0.20/10.50 % CPULimit : 300
% 0.20/10.50 % WCLimit : 300
% 0.20/10.50 % DateTime : Sun Sep 20 23:34:13 UTC 2026
% 0.20/10.50 % CPUTime :
% 0.20/10.53 % Drodi V4.1.1
% 30.43/14.49 % Refutation found
% 30.43/14.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 30.43/14.49 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.08/15.03 % Elapsed time: 4.512110 seconds
% 2.08/15.03 % CPU time: 31.654816 seconds
% 2.08/15.03 % Total memory used: 326.613 MB
% 2.08/15.03 % Net memory used: 310.678 MB
%------------------------------------------------------------------------------