%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT326+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 : 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:45 PM UTC 2026
% Result : Theorem 0.12s 0.42s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 74
% Syntax : Number of formulae : 323 ( 46 unt; 53 def)
% Number of atoms : 1280 ( 31 equ)
% Maximal formula atoms : 19 ( 3 avg)
% Number of connectives : 1601 ( 644 ~; 716 |; 148 &)
% ( 53 <=>; 40 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 79 ( 77 usr; 54 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 7 con; 0-2 aty)
% Number of variables : 155 ( 149 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m2_lattice4(B,A)
& ~ v1_xboole_0(B) )
=> ! [C] :
( ( m2_relset_1(C,k2_zfmisc_1(B,B),B)
& v1_funct_2(C,k2_zfmisc_1(B,B),B)
& v1_funct_1(C) )
=> ! [D] :
( ( m2_relset_1(D,k2_zfmisc_1(B,B),B)
& v1_funct_2(D,k2_zfmisc_1(B,B),B)
& v1_funct_1(D) )
=> ( ( D = k1_realset1(u1_lattices(A),B)
& C = k1_realset1(u2_lattices(A),B) )
=> ( r1_lattice2(B,D,C)
& r1_lattice2(B,C,D)
& v2_binop_1(D,B)
& v1_binop_1(D,B)
& v2_binop_1(C,B)
& v1_binop_1(C,B) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( m2_lattice4(B,A)
& ~ v1_xboole_0(B) )
=> ! [C] :
( ( m2_relset_1(C,k2_zfmisc_1(B,B),B)
& v1_funct_2(C,k2_zfmisc_1(B,B),B)
& v1_funct_1(C) )
=> ! [D] :
( ( m2_relset_1(D,k2_zfmisc_1(B,B),B)
& v1_funct_2(D,k2_zfmisc_1(B,B),B)
& v1_funct_1(D) )
=> ( ( D = k1_realset1(u1_lattices(A),B)
& C = k1_realset1(u2_lattices(A),B) )
=> ( r1_lattice2(B,D,C)
& r1_lattice2(B,C,D)
& v2_binop_1(D,B)
& v1_binop_1(D,B)
& v2_binop_1(C,B)
& v1_binop_1(C,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/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A] :
( l1_lattices(A)
=> l1_struct_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [A] :
( l3_lattices(A)
=> ( l2_lattices(A)
& l1_lattices(A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,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(f23,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(f25,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(f35,axiom,
! [A] :
( ( l1_struct_0(A)
& ~ v3_struct_0(A) )
=> ~ v1_xboole_0(u1_struct_0(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
v1_xboole_0(k1_xboole_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [A] :
( ( l2_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A) )
=> ( v1_partfun1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_binop_1(u2_lattices(A),u1_struct_0(A))
& v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_1(u2_lattices(A))
& v1_relat_1(u2_lattices(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [A] :
( ( l2_lattices(A)
& v5_lattices(A)
& ~ v3_struct_0(A) )
=> ( v1_partfun1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v2_binop_1(u2_lattices(A),u1_struct_0(A))
& v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_1(u2_lattices(A))
& v1_relat_1(u2_lattices(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [A] :
( ( l1_lattices(A)
& v6_lattices(A)
& ~ v3_struct_0(A) )
=> ( v1_partfun1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_binop_1(u1_lattices(A),u1_struct_0(A))
& v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_1(u1_lattices(A))
& v1_relat_1(u1_lattices(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [A] :
( ( l1_lattices(A)
& v7_lattices(A)
& ~ v3_struct_0(A) )
=> ( v1_partfun1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v2_binop_1(u1_lattices(A),u1_struct_0(A))
& v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_1(u1_lattices(A))
& v1_relat_1(u1_lattices(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,axiom,
? [A] : v1_xboole_0(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
? [A] :
( v1_funct_1(A)
& v1_xboole_0(A)
& v1_relat_1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,axiom,
! [A] :
( ~ v1_xboole_0(A)
=> ! [B] :
( ( m1_subset_1(B,k1_zfmisc_1(A))
& ~ v1_xboole_0(B) )
=> ! [C] :
( ( m2_relset_1(C,k2_zfmisc_1(A,A),A)
& v1_funct_2(C,k2_zfmisc_1(A,A),A)
& v1_funct_1(C) )
=> ! [D] :
( ( m2_relset_1(D,k2_zfmisc_1(B,B),B)
& v1_funct_2(D,k2_zfmisc_1(B,B),B)
& v1_funct_1(D) )
=> ( D = k1_realset1(C,B)
=> ( ( v2_binop_1(C,A)
=> v2_binop_1(D,B) )
& ( v3_binop_1(C,A)
=> v3_binop_1(D,B) )
& ( v1_binop_1(C,A)
=> v1_binop_1(D,B) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f61,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> r1_lattice2(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f62,axiom,
! [A] :
( ( l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) )
=> r1_lattice2(u1_struct_0(A),u1_lattices(A),u2_lattices(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [A] :
( ~ v1_xboole_0(A)
=> ! [B] :
( ( m1_subset_1(B,k1_zfmisc_1(A))
& ~ v1_xboole_0(B) )
=> ! [C] :
( ( m2_relset_1(C,k2_zfmisc_1(A,A),A)
& v1_funct_2(C,k2_zfmisc_1(A,A),A)
& v1_funct_1(C) )
=> ! [D] :
( ( m2_relset_1(D,k2_zfmisc_1(A,A),A)
& v1_funct_2(D,k2_zfmisc_1(A,A),A)
& v1_funct_1(D) )
=> ! [E] :
( ( m2_relset_1(E,k2_zfmisc_1(B,B),B)
& v1_funct_2(E,k2_zfmisc_1(B,B),B)
& v1_funct_1(E) )
=> ! [F] :
( ( m2_relset_1(F,k2_zfmisc_1(B,B),B)
& v1_funct_2(F,k2_zfmisc_1(B,B),B)
& v1_funct_1(F) )
=> ( ( r1_lattice2(A,C,D)
& F = k1_realset1(D,B)
& E = k1_realset1(C,B) )
=> r1_lattice2(B,E,F) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f68,axiom,
! [A,B] :
~ ( v1_xboole_0(B)
& A != B
& v1_xboole_0(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f69,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( ( ~ r1_lattice2(B,D,C)
| ~ r1_lattice2(B,C,D)
| ~ v2_binop_1(D,B)
| ~ v1_binop_1(D,B)
| ~ v2_binop_1(C,B)
| ~ v1_binop_1(C,B) )
& D = k1_realset1(u1_lattices(A),B)
& C = k1_realset1(u2_lattices(A),B)
& m2_relset_1(D,k2_zfmisc_1(B,B),B)
& v1_funct_2(D,k2_zfmisc_1(B,B),B)
& v1_funct_1(D) )
& m2_relset_1(C,k2_zfmisc_1(B,B),B)
& v1_funct_2(C,k2_zfmisc_1(B,B),B)
& v1_funct_1(C) )
& m2_lattice4(B,A)
& ~ v1_xboole_0(B) )
& l3_lattices(A)
& v10_lattices(A)
& ~ v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f70,plain,
( ( ~ r1_lattice2(sK1_skl,sK3_skl,sK2_skl)
| ~ r1_lattice2(sK1_skl,sK2_skl,sK3_skl)
| ~ v2_binop_1(sK3_skl,sK1_skl)
| ~ v1_binop_1(sK3_skl,sK1_skl)
| ~ v2_binop_1(sK2_skl,sK1_skl)
| ~ v1_binop_1(sK2_skl,sK1_skl) )
& sK3_skl = k1_realset1(u1_lattices(sK0_skl),sK1_skl)
& sK2_skl = k1_realset1(u2_lattices(sK0_skl),sK1_skl)
& m2_relset_1(sK3_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
& v1_funct_2(sK3_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
& v1_funct_1(sK3_skl)
& m2_relset_1(sK2_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
& v1_funct_2(sK2_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
& v1_funct_1(sK2_skl)
& m2_lattice4(sK1_skl,sK0_skl)
& ~ v1_xboole_0(sK1_skl)
& l3_lattices(sK0_skl)
& v10_lattices(sK0_skl)
& ~ v3_struct_0(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl),skolemize(D,sK3_skl)],[f69]) ).
fof(f71,plain,
~ v3_struct_0(sK0_skl),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f72,plain,
v10_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f73,plain,
l3_lattices(sK0_skl),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f74,plain,
~ v1_xboole_0(sK1_skl),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f75,plain,
m2_lattice4(sK1_skl,sK0_skl),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f76,plain,
v1_funct_1(sK2_skl),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f77,plain,
v1_funct_2(sK2_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f78,plain,
m2_relset_1(sK2_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f79,plain,
v1_funct_1(sK3_skl),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f80,plain,
v1_funct_2(sK3_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f81,plain,
m2_relset_1(sK3_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f82,plain,
sK2_skl = k1_realset1(u2_lattices(sK0_skl),sK1_skl),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f83,plain,
sK3_skl = k1_realset1(u1_lattices(sK0_skl),sK1_skl),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f84,plain,
( ~ r1_lattice2(sK1_skl,sK3_skl,sK2_skl)
| ~ r1_lattice2(sK1_skl,sK2_skl,sK3_skl)
| ~ v2_binop_1(sK3_skl,sK1_skl)
| ~ v1_binop_1(sK3_skl,sK1_skl)
| ~ v2_binop_1(sK2_skl,sK1_skl)
| ~ v1_binop_1(sK2_skl,sK1_skl) ),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f89,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(f91,plain,
! [X0] :
( v4_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f92,plain,
! [X0] :
( v5_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f93,plain,
! [X0] :
( v6_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f94,plain,
! [X0] :
( v7_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f112,plain,
! [A] :
( l1_struct_0(A)
| ~ l1_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f113,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f116,plain,
! [A] :
( ( l2_lattices(A)
& l1_lattices(A) )
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f117,plain,
! [X0] :
( l1_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f118,plain,
! [X0] :
( l2_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f119,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)],[f21]) ).
fof(f120,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)],[f119]) ).
fof(f123,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)],[f23]) ).
fof(f124,plain,
! [X0] :
( v1_funct_1(u1_lattices(X0))
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f123]) ).
fof(f125,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)],[f123]) ).
fof(f126,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)],[f123]) ).
fof(f127,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)],[f25]) ).
fof(f128,plain,
! [X0] :
( v1_funct_1(u2_lattices(X0))
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f127]) ).
fof(f129,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)],[f127]) ).
fof(f130,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)],[f127]) ).
fof(f151,plain,
! [A] :
( ~ v1_xboole_0(u1_struct_0(A))
| ~ l1_struct_0(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f152,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| ~ l1_struct_0(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f153,plain,
! [X0] : ~ v1_xboole_0(k1_zfmisc_1(X0)),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f154,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f155,plain,
! [A] :
( ( v1_partfun1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_binop_1(u2_lattices(A),u1_struct_0(A))
& v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_1(u2_lattices(A))
& v1_relat_1(u2_lattices(A)) )
| ~ l2_lattices(A)
| ~ v4_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f38]) ).
fof(f159,plain,
! [X0] :
( v1_binop_1(u2_lattices(X0),u1_struct_0(X0))
| ~ l2_lattices(X0)
| ~ v4_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f165,plain,
! [A] :
( ( v1_partfun1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v2_binop_1(u2_lattices(A),u1_struct_0(A))
& v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_1(u2_lattices(A))
& v1_relat_1(u2_lattices(A)) )
| ~ l2_lattices(A)
| ~ v5_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f169,plain,
! [X0] :
( v2_binop_1(u2_lattices(X0),u1_struct_0(X0))
| ~ l2_lattices(X0)
| ~ v5_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f175,plain,
! [A] :
( ( v1_partfun1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_binop_1(u1_lattices(A),u1_struct_0(A))
& v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_1(u1_lattices(A))
& v1_relat_1(u1_lattices(A)) )
| ~ l1_lattices(A)
| ~ v6_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f179,plain,
! [X0] :
( v1_binop_1(u1_lattices(X0),u1_struct_0(X0))
| ~ l1_lattices(X0)
| ~ v6_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f175]) ).
fof(f183,plain,
! [A] :
( ( v1_partfun1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v2_binop_1(u1_lattices(A),u1_struct_0(A))
& v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
& v1_funct_1(u1_lattices(A))
& v1_relat_1(u1_lattices(A)) )
| ~ l1_lattices(A)
| ~ v7_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f44]) ).
fof(f187,plain,
! [X0] :
( v2_binop_1(u1_lattices(X0),u1_struct_0(X0))
| ~ l1_lattices(X0)
| ~ v7_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f183]) ).
fof(f200,plain,
v1_xboole_0(sK15_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(A,sK15_skl)],[f48]) ).
fof(f201,plain,
v1_xboole_0(sK15_skl),
inference(cnf_transformation,[status(thm)],[f200]) ).
fof(f202,plain,
( v1_funct_1(sK16_skl)
& v1_xboole_0(sK16_skl)
& v1_relat_1(sK16_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(A,sK16_skl)],[f49]) ).
fof(f204,plain,
v1_xboole_0(sK16_skl),
inference(cnf_transformation,[status(thm)],[f202]) ).
fof(f228,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ( ( v2_binop_1(D,B)
| ~ v2_binop_1(C,A) )
& ( v3_binop_1(D,B)
| ~ v3_binop_1(C,A) )
& ( v1_binop_1(D,B)
| ~ v1_binop_1(C,A) ) )
| D != k1_realset1(C,B)
| ~ m2_relset_1(D,k2_zfmisc_1(B,B),B)
| ~ v1_funct_2(D,k2_zfmisc_1(B,B),B)
| ~ v1_funct_1(D) )
| ~ m2_relset_1(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_1(C) )
| ~ m1_subset_1(B,k1_zfmisc_1(A))
| v1_xboole_0(B) )
| v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f229,plain,
! [X0,X1,X2,X3] :
( v1_binop_1(X3,X1)
| ~ v1_binop_1(X2,X0)
| X3 != k1_realset1(X2,X1)
| ~ m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X1)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f228]) ).
fof(f231,plain,
! [X0,X1,X2,X3] :
( v2_binop_1(X3,X1)
| ~ v2_binop_1(X2,X0)
| X3 != k1_realset1(X2,X1)
| ~ m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X1)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f228]) ).
fof(f240,plain,
! [A] :
( r1_lattice2(u1_struct_0(A),u2_lattices(A),u1_lattices(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f61]) ).
fof(f241,plain,
! [X0] :
( r1_lattice2(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f242,plain,
! [A] :
( r1_lattice2(u1_struct_0(A),u1_lattices(A),u2_lattices(A))
| ~ l3_lattices(A)
| ~ v10_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f62]) ).
fof(f243,plain,
! [X0] :
( r1_lattice2(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0))
| ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f242]) ).
fof(f247,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( ! [F] :
( r1_lattice2(B,E,F)
| ~ r1_lattice2(A,C,D)
| F != k1_realset1(D,B)
| E != k1_realset1(C,B)
| ~ m2_relset_1(F,k2_zfmisc_1(B,B),B)
| ~ v1_funct_2(F,k2_zfmisc_1(B,B),B)
| ~ v1_funct_1(F) )
| ~ m2_relset_1(E,k2_zfmisc_1(B,B),B)
| ~ v1_funct_2(E,k2_zfmisc_1(B,B),B)
| ~ v1_funct_1(E) )
| ~ m2_relset_1(D,k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(D,k2_zfmisc_1(A,A),A)
| ~ v1_funct_1(D) )
| ~ m2_relset_1(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_1(C) )
| ~ m1_subset_1(B,k1_zfmisc_1(A))
| v1_xboole_0(B) )
| v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f64]) ).
fof(f248,plain,
! [X0,X1,X2,X3,X4,X5] :
( r1_lattice2(X1,X4,X5)
| ~ r1_lattice2(X0,X2,X3)
| X5 != k1_realset1(X3,X1)
| X4 != k1_realset1(X2,X1)
| ~ m2_relset_1(X5,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X5)
| ~ m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X4)
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X1)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f247]) ).
fof(f257,plain,
! [A,B] :
( ~ v1_xboole_0(B)
| A = B
| ~ v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f68]) ).
fof(f258,plain,
! [B] :
( ~ v1_xboole_0(B)
| ! [A] :
( A = B
| ~ v1_xboole_0(A) ) ),
inference(miniscoping,[status(thm)],[f257]) ).
fof(f259,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| X0 = X1
| ~ v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f258]) ).
fof(f260,definition,
( sQ0_spl
<=> v1_binop_1(sK2_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f262,plain,
( sQ0_spl
| ~ v1_binop_1(sK2_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f260]) ).
fof(f263,definition,
( sQ1_spl
<=> v2_binop_1(sK2_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f265,plain,
( sQ1_spl
| ~ v2_binop_1(sK2_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f263]) ).
fof(f266,definition,
( sQ2_spl
<=> v1_binop_1(sK3_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f268,plain,
( sQ2_spl
| ~ v1_binop_1(sK3_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f266]) ).
fof(f269,definition,
( sQ3_spl
<=> v2_binop_1(sK3_skl,sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f271,plain,
( sQ3_spl
| ~ v2_binop_1(sK3_skl,sK1_skl) ),
inference(component_clause,[status(thm)],[f269]) ).
fof(f272,definition,
( sQ4_spl
<=> r1_lattice2(sK1_skl,sK2_skl,sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f274,plain,
( sQ4_spl
| ~ r1_lattice2(sK1_skl,sK2_skl,sK3_skl) ),
inference(component_clause,[status(thm)],[f272]) ).
fof(f275,definition,
( sQ5_spl
<=> r1_lattice2(sK1_skl,sK3_skl,sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f277,plain,
( sQ5_spl
| ~ r1_lattice2(sK1_skl,sK3_skl,sK2_skl) ),
inference(component_clause,[status(thm)],[f275]) ).
fof(f278,plain,
( ~ sQ5_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ sQ2_spl
| ~ sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f84,f260,f263,f266,f269,f272,f275]) ).
fof(f279,plain,
! [X0,X1,X2] :
( v1_binop_1(k1_realset1(X2,X1),X1)
| ~ v1_binop_1(X2,X0)
| ~ m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(X2,X1))
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X1)
| v1_xboole_0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f229]) ).
fof(f281,plain,
! [X0,X1,X2] :
( v2_binop_1(k1_realset1(X2,X1),X1)
| ~ v2_binop_1(X2,X0)
| ~ m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(X2,X1))
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X1)
| v1_xboole_0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f231]) ).
fof(f282,plain,
! [X0,X1,X2,X3] :
( r1_lattice2(X1,k1_realset1(X2,X1),k1_realset1(X3,X1))
| ~ r1_lattice2(X0,X2,X3)
| ~ m2_relset_1(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(k1_realset1(X3,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(X3,X1))
| ~ m2_relset_1(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(k1_realset1(X2,X1),k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(k1_realset1(X2,X1))
| ~ m2_relset_1(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X3,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X3)
| ~ m2_relset_1(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| v1_xboole_0(X1)
| v1_xboole_0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f248]) ).
fof(f291,plain,
! [X0] :
( X0 = k1_xboole_0
| ~ v1_xboole_0(X0) ),
inference(resolution,[status(thm)],[f154,f259]) ).
fof(f293,plain,
! [X0] :
( X0 = sK15_skl
| ~ v1_xboole_0(X0) ),
inference(resolution,[status(thm)],[f201,f259]) ).
fof(f305,plain,
sK16_skl = k1_xboole_0,
inference(resolution,[status(thm)],[f291,f204]) ).
fof(f306,plain,
sK15_skl = k1_xboole_0,
inference(resolution,[status(thm)],[f291,f201]) ).
fof(f313,plain,
sK15_skl = sK16_skl,
inference(forward_demodulation,[status(thm)],[f305,f306]) ).
fof(f314,plain,
! [X0] :
( X0 = sK16_skl
| ~ v1_xboole_0(X0) ),
inference(forward_demodulation,[status(thm)],[f313,f293]) ).
fof(f318,definition,
( sQ10_spl
<=> v1_funct_1(u1_lattices(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f320,plain,
( sQ10_spl
| ~ v1_funct_1(u1_lattices(sK0_skl)) ),
inference(component_clause,[status(thm)],[f318]) ).
fof(f325,definition,
( sQ12_spl
<=> v1_funct_1(u2_lattices(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f327,plain,
( sQ12_spl
| ~ v1_funct_1(u2_lattices(sK0_skl)) ),
inference(component_clause,[status(thm)],[f325]) ).
fof(f332,plain,
( sQ12_spl
| ~ l2_lattices(sK0_skl) ),
inference(resolution,[status(thm)],[f327,f128]) ).
fof(f341,plain,
l1_lattices(sK0_skl),
inference(resolution,[status(thm)],[f117,f73]) ).
fof(f343,plain,
l1_struct_0(sK0_skl),
inference(resolution,[status(thm)],[f341,f113]) ).
fof(f344,plain,
( v4_lattices(sK0_skl)
| v3_struct_0(sK0_skl)
| ~ l3_lattices(sK0_skl) ),
inference(resolution,[status(thm)],[f91,f72]) ).
fof(f345,definition,
( sQ14_spl
<=> l3_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f347,plain,
( sQ14_spl
| ~ l3_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f345]) ).
fof(f348,definition,
( sQ15_spl
<=> v3_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f349,plain,
( ~ sQ15_spl
| v3_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f348]) ).
fof(f351,definition,
( sQ16_spl
<=> v4_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f354,plain,
( sQ16_spl
| sQ15_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f344,f345,f348,f351]) ).
fof(f355,plain,
( ~ sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f349,f71]) ).
fof(f356,plain,
~ sQ15_spl,
inference(contradiction_clause,[status(thm)],[f355]) ).
fof(f357,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f347,f73]) ).
fof(f358,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f357]) ).
fof(f359,plain,
( v5_lattices(sK0_skl)
| v3_struct_0(sK0_skl)
| ~ l3_lattices(sK0_skl) ),
inference(resolution,[status(thm)],[f92,f72]) ).
fof(f360,definition,
( sQ17_spl
<=> v5_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f363,plain,
( sQ17_spl
| sQ15_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f359,f345,f348,f360]) ).
fof(f364,plain,
( sQ10_spl
| ~ l1_lattices(sK0_skl) ),
inference(resolution,[status(thm)],[f320,f124]) ).
fof(f365,plain,
( sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f364,f341]) ).
fof(f366,plain,
sQ10_spl,
inference(contradiction_clause,[status(thm)],[f365]) ).
fof(f368,plain,
! [X0] :
( v1_binop_1(k1_realset1(u1_lattices(sK0_skl),sK1_skl),sK1_skl)
| ~ v1_binop_1(u1_lattices(sK0_skl),X0)
| ~ m2_relset_1(k1_realset1(u1_lattices(sK0_skl),sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(sK3_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(u1_lattices(sK0_skl),sK1_skl))
| ~ m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(u1_lattices(sK0_skl))
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(sK1_skl)
| v1_xboole_0(X0) ),
inference(paramodulation,[status(thm)],[f83,f279]) ).
fof(f369,plain,
! [X0] :
( v1_binop_1(k1_realset1(u2_lattices(sK0_skl),sK1_skl),sK1_skl)
| ~ v1_binop_1(u2_lattices(sK0_skl),X0)
| ~ m2_relset_1(k1_realset1(u2_lattices(sK0_skl),sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(sK2_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(u2_lattices(sK0_skl),sK1_skl))
| ~ m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(u2_lattices(sK0_skl))
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(sK1_skl)
| v1_xboole_0(X0) ),
inference(paramodulation,[status(thm)],[f82,f279]) ).
fof(f370,definition,
! [X0] :
( sQ18_spl
<=> ( ~ v1_binop_1(u1_lattices(sK0_skl),X0)
| ~ m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f371,plain,
! [X0] :
( ~ sQ18_spl
| ~ v1_binop_1(u1_lattices(sK0_skl),X0)
| ~ m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(component_clause,[status(thm)],[f370]) ).
fof(f373,definition,
( sQ19_spl
<=> v1_xboole_0(sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f374,plain,
( ~ sQ19_spl
| v1_xboole_0(sK1_skl) ),
inference(component_clause,[status(thm)],[f373]) ).
fof(f376,definition,
( sQ20_spl
<=> v1_funct_1(k1_realset1(u1_lattices(sK0_skl),sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f378,plain,
( sQ20_spl
| ~ v1_funct_1(k1_realset1(u1_lattices(sK0_skl),sK1_skl)) ),
inference(component_clause,[status(thm)],[f376]) ).
fof(f379,definition,
( sQ21_spl
<=> v1_funct_2(sK3_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f381,plain,
( sQ21_spl
| ~ v1_funct_2(sK3_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl) ),
inference(component_clause,[status(thm)],[f379]) ).
fof(f382,definition,
( sQ22_spl
<=> m2_relset_1(k1_realset1(u1_lattices(sK0_skl),sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f384,plain,
( sQ22_spl
| ~ m2_relset_1(k1_realset1(u1_lattices(sK0_skl),sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl) ),
inference(component_clause,[status(thm)],[f382]) ).
fof(f385,definition,
( sQ23_spl
<=> v1_binop_1(k1_realset1(u1_lattices(sK0_skl),sK1_skl),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f386,plain,
( ~ sQ23_spl
| v1_binop_1(k1_realset1(u1_lattices(sK0_skl),sK1_skl),sK1_skl) ),
inference(component_clause,[status(thm)],[f385]) ).
fof(f388,plain,
( sQ23_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ10_spl
| sQ19_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f368,f370,f373,f318,f376,f379,f382,f385]) ).
fof(f389,definition,
! [X0] :
( sQ24_spl
<=> ( ~ v1_binop_1(u2_lattices(sK0_skl),X0)
| ~ m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f390,plain,
! [X0] :
( ~ sQ24_spl
| ~ v1_binop_1(u2_lattices(sK0_skl),X0)
| ~ m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(component_clause,[status(thm)],[f389]) ).
fof(f392,definition,
( sQ25_spl
<=> v1_funct_1(k1_realset1(u2_lattices(sK0_skl),sK1_skl)) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f394,plain,
( sQ25_spl
| ~ v1_funct_1(k1_realset1(u2_lattices(sK0_skl),sK1_skl)) ),
inference(component_clause,[status(thm)],[f392]) ).
fof(f395,definition,
( sQ26_spl
<=> v1_funct_2(sK2_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f397,plain,
( sQ26_spl
| ~ v1_funct_2(sK2_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl) ),
inference(component_clause,[status(thm)],[f395]) ).
fof(f398,definition,
( sQ27_spl
<=> m2_relset_1(k1_realset1(u2_lattices(sK0_skl),sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f400,plain,
( sQ27_spl
| ~ m2_relset_1(k1_realset1(u2_lattices(sK0_skl),sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl) ),
inference(component_clause,[status(thm)],[f398]) ).
fof(f401,definition,
( sQ28_spl
<=> v1_binop_1(k1_realset1(u2_lattices(sK0_skl),sK1_skl),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f402,plain,
( ~ sQ28_spl
| v1_binop_1(k1_realset1(u2_lattices(sK0_skl),sK1_skl),sK1_skl) ),
inference(component_clause,[status(thm)],[f401]) ).
fof(f404,plain,
( sQ28_spl
| ~ sQ27_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ12_spl
| sQ19_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f369,f389,f373,f325,f392,f395,f398,f401]) ).
fof(f405,plain,
( ~ sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f374,f74]) ).
fof(f406,plain,
~ sQ19_spl,
inference(contradiction_clause,[status(thm)],[f405]) ).
fof(f407,plain,
( ~ sQ28_spl
| v1_binop_1(sK2_skl,sK1_skl) ),
inference(forward_demodulation,[status(thm)],[f82,f402]) ).
fof(f408,plain,
( sQ27_spl
| ~ m2_relset_1(sK2_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl) ),
inference(forward_demodulation,[status(thm)],[f82,f400]) ).
fof(f409,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f408,f78]) ).
fof(f410,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f409]) ).
fof(f411,plain,
( sQ26_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f397,f77]) ).
fof(f412,plain,
sQ26_spl,
inference(contradiction_clause,[status(thm)],[f411]) ).
fof(f413,plain,
( sQ25_spl
| ~ v1_funct_1(sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f82,f394]) ).
fof(f414,plain,
( sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f413,f76]) ).
fof(f415,plain,
sQ25_spl,
inference(contradiction_clause,[status(thm)],[f414]) ).
fof(f416,plain,
( ~ sQ23_spl
| v1_binop_1(sK3_skl,sK1_skl) ),
inference(forward_demodulation,[status(thm)],[f83,f386]) ).
fof(f417,plain,
( sQ22_spl
| ~ m2_relset_1(sK3_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl) ),
inference(forward_demodulation,[status(thm)],[f83,f384]) ).
fof(f418,plain,
( sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f417,f81]) ).
fof(f419,plain,
sQ22_spl,
inference(contradiction_clause,[status(thm)],[f418]) ).
fof(f420,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f381,f80]) ).
fof(f421,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f420]) ).
fof(f422,plain,
( sQ20_spl
| ~ v1_funct_1(sK3_skl) ),
inference(forward_demodulation,[status(thm)],[f83,f378]) ).
fof(f423,plain,
( sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f422,f79]) ).
fof(f424,plain,
sQ20_spl,
inference(contradiction_clause,[status(thm)],[f423]) ).
fof(f429,plain,
! [X0] :
( v2_binop_1(k1_realset1(u1_lattices(sK0_skl),sK1_skl),sK1_skl)
| ~ v2_binop_1(u1_lattices(sK0_skl),X0)
| ~ m2_relset_1(k1_realset1(u1_lattices(sK0_skl),sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(sK3_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(u1_lattices(sK0_skl),sK1_skl))
| ~ m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(u1_lattices(sK0_skl))
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(sK1_skl)
| v1_xboole_0(X0) ),
inference(paramodulation,[status(thm)],[f83,f281]) ).
fof(f430,plain,
! [X0] :
( v2_binop_1(k1_realset1(u2_lattices(sK0_skl),sK1_skl),sK1_skl)
| ~ v2_binop_1(u2_lattices(sK0_skl),X0)
| ~ m2_relset_1(k1_realset1(u2_lattices(sK0_skl),sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(sK2_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(u2_lattices(sK0_skl),sK1_skl))
| ~ m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(u2_lattices(sK0_skl))
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(sK1_skl)
| v1_xboole_0(X0) ),
inference(paramodulation,[status(thm)],[f82,f281]) ).
fof(f431,definition,
! [X0] :
( sQ29_spl
<=> ( ~ v2_binop_1(u1_lattices(sK0_skl),X0)
| ~ m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f432,plain,
! [X0] :
( ~ sQ29_spl
| ~ v2_binop_1(u1_lattices(sK0_skl),X0)
| ~ m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(component_clause,[status(thm)],[f431]) ).
fof(f434,definition,
( sQ30_spl
<=> v2_binop_1(k1_realset1(u1_lattices(sK0_skl),sK1_skl),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f435,plain,
( ~ sQ30_spl
| v2_binop_1(k1_realset1(u1_lattices(sK0_skl),sK1_skl),sK1_skl) ),
inference(component_clause,[status(thm)],[f434]) ).
fof(f437,plain,
( sQ30_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ10_spl
| sQ19_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f429,f431,f373,f318,f376,f379,f382,f434]) ).
fof(f438,definition,
! [X0] :
( sQ31_spl
<=> ( ~ v2_binop_1(u2_lattices(sK0_skl),X0)
| ~ m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f439,plain,
! [X0] :
( ~ sQ31_spl
| ~ v2_binop_1(u2_lattices(sK0_skl),X0)
| ~ m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(component_clause,[status(thm)],[f438]) ).
fof(f441,definition,
( sQ32_spl
<=> v2_binop_1(k1_realset1(u2_lattices(sK0_skl),sK1_skl),sK1_skl) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f442,plain,
( ~ sQ32_spl
| v2_binop_1(k1_realset1(u2_lattices(sK0_skl),sK1_skl),sK1_skl) ),
inference(component_clause,[status(thm)],[f441]) ).
fof(f444,plain,
( sQ32_spl
| ~ sQ27_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ12_spl
| sQ19_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f430,f438,f373,f325,f392,f395,f398,f441]) ).
fof(f445,plain,
( ~ sQ32_spl
| v2_binop_1(sK2_skl,sK1_skl) ),
inference(forward_demodulation,[status(thm)],[f82,f442]) ).
fof(f446,plain,
( ~ sQ30_spl
| v2_binop_1(sK3_skl,sK1_skl) ),
inference(forward_demodulation,[status(thm)],[f83,f435]) ).
fof(f447,plain,
! [X0,X1] :
( r1_lattice2(sK1_skl,k1_realset1(X1,sK1_skl),k1_realset1(u1_lattices(sK0_skl),sK1_skl))
| ~ r1_lattice2(X0,X1,u1_lattices(sK0_skl))
| ~ m2_relset_1(k1_realset1(u1_lattices(sK0_skl),sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(sK3_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(u1_lattices(sK0_skl),sK1_skl))
| ~ m2_relset_1(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(X1,sK1_skl))
| ~ m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(u1_lattices(sK0_skl))
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(sK1_skl)
| v1_xboole_0(X0) ),
inference(paramodulation,[status(thm)],[f83,f282]) ).
fof(f448,plain,
! [X0,X1] :
( r1_lattice2(sK1_skl,k1_realset1(X1,sK1_skl),k1_realset1(u2_lattices(sK0_skl),sK1_skl))
| ~ r1_lattice2(X0,X1,u2_lattices(sK0_skl))
| ~ m2_relset_1(k1_realset1(u2_lattices(sK0_skl),sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(sK2_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(u2_lattices(sK0_skl),sK1_skl))
| ~ m2_relset_1(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(X1,sK1_skl))
| ~ m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(u2_lattices(sK0_skl))
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(sK1_skl)
| v1_xboole_0(X0) ),
inference(paramodulation,[status(thm)],[f82,f282]) ).
fof(f449,definition,
! [X0,X1] :
( sQ33_spl
<=> ( r1_lattice2(sK1_skl,k1_realset1(X1,sK1_skl),k1_realset1(u1_lattices(sK0_skl),sK1_skl))
| ~ r1_lattice2(X0,X1,u1_lattices(sK0_skl))
| ~ m2_relset_1(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(X1,sK1_skl))
| ~ m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f450,plain,
! [X0,X1] :
( ~ sQ33_spl
| r1_lattice2(sK1_skl,k1_realset1(X1,sK1_skl),k1_realset1(u1_lattices(sK0_skl),sK1_skl))
| ~ r1_lattice2(X0,X1,u1_lattices(sK0_skl))
| ~ m2_relset_1(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(X1,sK1_skl))
| ~ m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(component_clause,[status(thm)],[f449]) ).
fof(f452,plain,
( ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ10_spl
| sQ19_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f447,f449,f373,f318,f376,f379,f382]) ).
fof(f453,definition,
! [X0,X1] :
( sQ34_spl
<=> ( r1_lattice2(sK1_skl,k1_realset1(X1,sK1_skl),k1_realset1(u2_lattices(sK0_skl),sK1_skl))
| ~ r1_lattice2(X0,X1,u2_lattices(sK0_skl))
| ~ m2_relset_1(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(X1,sK1_skl))
| ~ m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f454,plain,
! [X0,X1] :
( ~ sQ34_spl
| r1_lattice2(sK1_skl,k1_realset1(X1,sK1_skl),k1_realset1(u2_lattices(sK0_skl),sK1_skl))
| ~ r1_lattice2(X0,X1,u2_lattices(sK0_skl))
| ~ m2_relset_1(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(X1,sK1_skl))
| ~ m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(component_clause,[status(thm)],[f453]) ).
fof(f456,plain,
( ~ sQ27_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ12_spl
| sQ19_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f448,f453,f373,f325,f392,f395,f398]) ).
fof(f457,plain,
! [X0,X1] :
( ~ sQ33_spl
| r1_lattice2(sK1_skl,k1_realset1(X1,sK1_skl),sK3_skl)
| ~ r1_lattice2(X0,X1,u1_lattices(sK0_skl))
| ~ m2_relset_1(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(X1,sK1_skl))
| ~ m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(forward_demodulation,[status(thm)],[f83,f450]) ).
fof(f458,plain,
! [X0,X1] :
( ~ sQ34_spl
| r1_lattice2(sK1_skl,k1_realset1(X1,sK1_skl),sK2_skl)
| ~ r1_lattice2(X0,X1,u2_lattices(sK0_skl))
| ~ m2_relset_1(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(k1_realset1(X1,sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(X1,sK1_skl))
| ~ m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(X1)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(forward_demodulation,[status(thm)],[f82,f454]) ).
fof(f460,plain,
l2_lattices(sK0_skl),
inference(resolution,[status(thm)],[f118,f73]) ).
fof(f461,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f460,f332]) ).
fof(f462,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f461]) ).
fof(f467,plain,
( v6_lattices(sK0_skl)
| v3_struct_0(sK0_skl)
| ~ l3_lattices(sK0_skl) ),
inference(resolution,[status(thm)],[f93,f72]) ).
fof(f468,definition,
( sQ35_spl
<=> v6_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f471,plain,
( sQ35_spl
| sQ15_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f467,f345,f348,f468]) ).
fof(f472,plain,
( v7_lattices(sK0_skl)
| v3_struct_0(sK0_skl)
| ~ l3_lattices(sK0_skl) ),
inference(resolution,[status(thm)],[f94,f72]) ).
fof(f473,definition,
( sQ36_spl
<=> v7_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f476,plain,
( sQ36_spl
| sQ15_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f472,f345,f348,f473]) ).
fof(f482,plain,
( ~ sQ24_spl
| ~ l2_lattices(sK0_skl)
| ~ v1_binop_1(u2_lattices(sK0_skl),u1_struct_0(sK0_skl))
| ~ 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))
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))
| v1_xboole_0(u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f390,f129]) ).
fof(f483,definition,
( sQ38_spl
<=> v1_xboole_0(u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f484,plain,
( ~ sQ38_spl
| v1_xboole_0(u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f483]) ).
fof(f486,definition,
( sQ39_spl
<=> m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f488,plain,
( sQ39_spl
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl))) ),
inference(component_clause,[status(thm)],[f486]) ).
fof(f489,definition,
( sQ40_spl
<=> 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)) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f491,plain,
( sQ40_spl
| ~ 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(component_clause,[status(thm)],[f489]) ).
fof(f492,definition,
( sQ41_spl
<=> v1_binop_1(u2_lattices(sK0_skl),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f494,plain,
( sQ41_spl
| ~ v1_binop_1(u2_lattices(sK0_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f492]) ).
fof(f495,definition,
( sQ42_spl
<=> l2_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f497,plain,
( sQ42_spl
| ~ l2_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f495]) ).
fof(f498,plain,
( ~ sQ24_spl
| ~ sQ42_spl
| ~ sQ41_spl
| ~ sQ40_spl
| ~ sQ39_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f482,f483,f486,f489,f492,f495,f389]) ).
fof(f499,plain,
( sQ42_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f497,f460]) ).
fof(f500,plain,
sQ42_spl,
inference(contradiction_clause,[status(thm)],[f499]) ).
fof(f501,plain,
( ~ sQ38_spl
| u1_struct_0(sK0_skl) = sK16_skl ),
inference(resolution,[status(thm)],[f484,f314]) ).
fof(f504,plain,
( ~ sQ18_spl
| ~ l1_lattices(sK0_skl)
| ~ v1_binop_1(u1_lattices(sK0_skl),u1_struct_0(sK0_skl))
| ~ 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))
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))
| v1_xboole_0(u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f371,f125]) ).
fof(f505,definition,
( sQ43_spl
<=> 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)) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f507,plain,
( sQ43_spl
| ~ 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(component_clause,[status(thm)],[f505]) ).
fof(f508,definition,
( sQ44_spl
<=> v1_binop_1(u1_lattices(sK0_skl),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f510,plain,
( sQ44_spl
| ~ v1_binop_1(u1_lattices(sK0_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f508]) ).
fof(f511,definition,
( sQ45_spl
<=> l1_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f513,plain,
( sQ45_spl
| ~ l1_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f511]) ).
fof(f514,plain,
( ~ sQ18_spl
| ~ sQ45_spl
| ~ sQ44_spl
| ~ sQ43_spl
| ~ sQ39_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f504,f483,f486,f505,f508,f511,f370]) ).
fof(f515,plain,
( sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f513,f341]) ).
fof(f516,plain,
sQ45_spl,
inference(contradiction_clause,[status(thm)],[f515]) ).
fof(f537,definition,
( sQ46_spl
<=> v10_lattices(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f539,plain,
( sQ46_spl
| ~ v10_lattices(sK0_skl) ),
inference(component_clause,[status(thm)],[f537]) ).
fof(f616,plain,
( sQ46_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f539,f72]) ).
fof(f617,plain,
sQ46_spl,
inference(contradiction_clause,[status(thm)],[f616]) ).
fof(f618,plain,
( sQ41_spl
| ~ l2_lattices(sK0_skl)
| ~ v4_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f494,f159]) ).
fof(f619,plain,
( sQ41_spl
| ~ sQ42_spl
| ~ sQ16_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f618,f348,f351,f495,f492]) ).
fof(f620,plain,
( sQ39_spl
| ~ m2_lattice4(sK1_skl,sK0_skl)
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f488,f120]) ).
fof(f621,definition,
( sQ66_spl
<=> m2_lattice4(sK1_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f623,plain,
( sQ66_spl
| ~ m2_lattice4(sK1_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f621]) ).
fof(f624,plain,
( sQ39_spl
| ~ sQ66_spl
| ~ sQ14_spl
| ~ sQ46_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f620,f348,f537,f345,f621,f486]) ).
fof(f625,plain,
( sQ66_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f623,f75]) ).
fof(f626,plain,
sQ66_spl,
inference(contradiction_clause,[status(thm)],[f625]) ).
fof(f627,plain,
( sQ44_spl
| ~ l1_lattices(sK0_skl)
| ~ v6_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f510,f179]) ).
fof(f628,plain,
( sQ44_spl
| ~ sQ45_spl
| ~ sQ35_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f627,f348,f468,f511,f508]) ).
fof(f629,plain,
( ~ sQ29_spl
| ~ l1_lattices(sK0_skl)
| ~ v2_binop_1(u1_lattices(sK0_skl),u1_struct_0(sK0_skl))
| ~ 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))
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))
| v1_xboole_0(u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f432,f125]) ).
fof(f630,definition,
( sQ67_spl
<=> v2_binop_1(u1_lattices(sK0_skl),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f632,plain,
( sQ67_spl
| ~ v2_binop_1(u1_lattices(sK0_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f630]) ).
fof(f633,plain,
( ~ sQ29_spl
| ~ sQ45_spl
| ~ sQ67_spl
| ~ sQ43_spl
| ~ sQ39_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f629,f483,f486,f505,f630,f511,f431]) ).
fof(f634,plain,
( ~ sQ31_spl
| ~ l2_lattices(sK0_skl)
| ~ v2_binop_1(u2_lattices(sK0_skl),u1_struct_0(sK0_skl))
| ~ 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))
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))
| v1_xboole_0(u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f439,f129]) ).
fof(f635,definition,
( sQ68_spl
<=> v2_binop_1(u2_lattices(sK0_skl),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f637,plain,
( sQ68_spl
| ~ v2_binop_1(u2_lattices(sK0_skl),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f635]) ).
fof(f638,plain,
( ~ sQ31_spl
| ~ sQ42_spl
| ~ sQ68_spl
| ~ sQ40_spl
| ~ sQ39_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f634,f483,f486,f489,f635,f495,f438]) ).
fof(f652,plain,
( sQ67_spl
| ~ l1_lattices(sK0_skl)
| ~ v7_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f632,f187]) ).
fof(f653,plain,
( sQ67_spl
| ~ sQ45_spl
| ~ sQ36_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f652,f348,f473,f511,f630]) ).
fof(f654,plain,
( sQ68_spl
| ~ l2_lattices(sK0_skl)
| ~ v5_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f637,f169]) ).
fof(f655,plain,
( sQ68_spl
| ~ sQ42_spl
| ~ sQ17_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f654,f348,f360,f495,f635]) ).
fof(f678,plain,
! [X0] :
( ~ sQ33_spl
| r1_lattice2(sK1_skl,k1_realset1(u2_lattices(sK0_skl),sK1_skl),sK3_skl)
| ~ r1_lattice2(X0,u2_lattices(sK0_skl),u1_lattices(sK0_skl))
| ~ m2_relset_1(k1_realset1(u2_lattices(sK0_skl),sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(sK2_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(u2_lattices(sK0_skl),sK1_skl))
| ~ m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(u2_lattices(sK0_skl))
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(paramodulation,[status(thm)],[f82,f457]) ).
fof(f686,definition,
! [X0] :
( sQ74_spl
<=> ( ~ r1_lattice2(X0,u2_lattices(sK0_skl),u1_lattices(sK0_skl))
| ~ m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition]) ).
fof(f687,plain,
! [X0] :
( ~ sQ74_spl
| ~ r1_lattice2(X0,u2_lattices(sK0_skl),u1_lattices(sK0_skl))
| ~ m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(component_clause,[status(thm)],[f686]) ).
fof(f689,definition,
( sQ75_spl
<=> r1_lattice2(sK1_skl,k1_realset1(u2_lattices(sK0_skl),sK1_skl),sK3_skl) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f690,plain,
( ~ sQ75_spl
| r1_lattice2(sK1_skl,k1_realset1(u2_lattices(sK0_skl),sK1_skl),sK3_skl) ),
inference(component_clause,[status(thm)],[f689]) ).
fof(f692,plain,
( ~ sQ33_spl
| sQ75_spl
| ~ sQ27_spl
| ~ sQ26_spl
| ~ sQ25_spl
| ~ sQ12_spl
| sQ74_spl ),
inference(split_clause,[status(thm)],[f678,f686,f325,f392,f395,f398,f689,f449]) ).
fof(f694,plain,
( ~ sQ75_spl
| r1_lattice2(sK1_skl,sK2_skl,sK3_skl) ),
inference(forward_demodulation,[status(thm)],[f82,f690]) ).
fof(f698,plain,
! [X0] :
( ~ sQ34_spl
| r1_lattice2(sK1_skl,k1_realset1(u1_lattices(sK0_skl),sK1_skl),sK2_skl)
| ~ r1_lattice2(X0,u1_lattices(sK0_skl),u2_lattices(sK0_skl))
| ~ m2_relset_1(k1_realset1(u1_lattices(sK0_skl),sK1_skl),k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_2(sK3_skl,k2_zfmisc_1(sK1_skl,sK1_skl),sK1_skl)
| ~ v1_funct_1(k1_realset1(u1_lattices(sK0_skl),sK1_skl))
| ~ m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_1(u1_lattices(sK0_skl))
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(paramodulation,[status(thm)],[f83,f458]) ).
fof(f700,definition,
! [X0] :
( sQ76_spl
<=> ( ~ r1_lattice2(X0,u1_lattices(sK0_skl),u2_lattices(sK0_skl))
| ~ m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f701,plain,
! [X0] :
( ~ sQ76_spl
| ~ r1_lattice2(X0,u1_lattices(sK0_skl),u2_lattices(sK0_skl))
| ~ m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(X0,X0),X0)
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(X0))
| v1_xboole_0(X0) ),
inference(component_clause,[status(thm)],[f700]) ).
fof(f703,definition,
( sQ77_spl
<=> r1_lattice2(sK1_skl,k1_realset1(u1_lattices(sK0_skl),sK1_skl),sK2_skl) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f704,plain,
( ~ sQ77_spl
| r1_lattice2(sK1_skl,k1_realset1(u1_lattices(sK0_skl),sK1_skl),sK2_skl) ),
inference(component_clause,[status(thm)],[f703]) ).
fof(f706,plain,
( ~ sQ34_spl
| sQ77_spl
| ~ sQ22_spl
| ~ sQ21_spl
| ~ sQ20_spl
| ~ sQ10_spl
| sQ76_spl ),
inference(split_clause,[status(thm)],[f698,f700,f318,f376,f379,f382,f703,f453]) ).
fof(f716,plain,
( ~ sQ77_spl
| r1_lattice2(sK1_skl,sK3_skl,sK2_skl) ),
inference(forward_demodulation,[status(thm)],[f83,f704]) ).
fof(f717,plain,
( ~ sQ77_spl
| sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f716,f277]) ).
fof(f718,plain,
( ~ sQ77_spl
| sQ5_spl ),
inference(contradiction_clause,[status(thm)],[f717]) ).
fof(f719,plain,
( sQ4_spl
| ~ sQ75_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f274,f694]) ).
fof(f720,plain,
( sQ4_spl
| ~ sQ75_spl ),
inference(contradiction_clause,[status(thm)],[f719]) ).
fof(f721,plain,
( sQ3_spl
| ~ sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f271,f446]) ).
fof(f722,plain,
( sQ3_spl
| ~ sQ30_spl ),
inference(contradiction_clause,[status(thm)],[f721]) ).
fof(f724,plain,
( sQ2_spl
| ~ sQ23_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f268,f416]) ).
fof(f725,plain,
( sQ2_spl
| ~ sQ23_spl ),
inference(contradiction_clause,[status(thm)],[f724]) ).
fof(f727,plain,
( sQ1_spl
| ~ sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f265,f445]) ).
fof(f728,plain,
( sQ1_spl
| ~ sQ32_spl ),
inference(contradiction_clause,[status(thm)],[f727]) ).
fof(f730,plain,
( sQ0_spl
| ~ sQ28_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f262,f407]) ).
fof(f731,plain,
( sQ0_spl
| ~ sQ28_spl ),
inference(contradiction_clause,[status(thm)],[f730]) ).
fof(f770,plain,
( sQ40_spl
| ~ l2_lattices(sK0_skl) ),
inference(resolution,[status(thm)],[f491,f130]) ).
fof(f771,plain,
( sQ40_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f770,f495,f489]) ).
fof(f894,plain,
( ~ sQ38_spl
| ~ v1_xboole_0(sK16_skl)
| ~ l1_struct_0(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(paramodulation,[status(thm)],[f501,f152]) ).
fof(f895,definition,
( sQ95_spl
<=> l1_struct_0(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f897,plain,
( sQ95_spl
| ~ l1_struct_0(sK0_skl) ),
inference(component_clause,[status(thm)],[f895]) ).
fof(f898,definition,
( sQ96_spl
<=> v1_xboole_0(sK16_skl) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f900,plain,
( sQ96_spl
| ~ v1_xboole_0(sK16_skl) ),
inference(component_clause,[status(thm)],[f898]) ).
fof(f901,plain,
( ~ sQ38_spl
| ~ sQ96_spl
| ~ sQ95_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f894,f348,f895,f898,f483]) ).
fof(f902,plain,
( sQ95_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f897,f343]) ).
fof(f903,plain,
sQ95_spl,
inference(contradiction_clause,[status(thm)],[f902]) ).
fof(f904,plain,
( sQ96_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f900,f204]) ).
fof(f905,plain,
sQ96_spl,
inference(contradiction_clause,[status(thm)],[f904]) ).
fof(f914,plain,
( sQ43_spl
| ~ l1_lattices(sK0_skl) ),
inference(resolution,[status(thm)],[f507,f126]) ).
fof(f915,plain,
( sQ43_spl
| ~ sQ45_spl ),
inference(split_clause,[status(thm)],[f914,f511,f505]) ).
fof(f917,plain,
( ~ sQ74_spl
| ~ l2_lattices(sK0_skl)
| ~ r1_lattice2(u1_struct_0(sK0_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl))
| ~ 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))
| ~ 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))
| ~ 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))
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))
| v1_xboole_0(u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f687,f129]) ).
fof(f918,definition,
( sQ98_spl
<=> v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f920,plain,
( sQ98_spl
| ~ v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)) ),
inference(component_clause,[status(thm)],[f918]) ).
fof(f921,definition,
( sQ99_spl
<=> r1_lattice2(u1_struct_0(sK0_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition]) ).
fof(f923,plain,
( sQ99_spl
| ~ r1_lattice2(u1_struct_0(sK0_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl)) ),
inference(component_clause,[status(thm)],[f921]) ).
fof(f924,plain,
( ~ sQ74_spl
| ~ sQ42_spl
| ~ sQ99_spl
| ~ sQ43_spl
| ~ sQ98_spl
| ~ sQ40_spl
| ~ sQ39_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f917,f483,f486,f489,f918,f505,f921,f495,f686]) ).
fof(f925,plain,
( ~ sQ76_spl
| ~ l2_lattices(sK0_skl)
| ~ r1_lattice2(u1_struct_0(sK0_skl),u1_lattices(sK0_skl),u2_lattices(sK0_skl))
| ~ 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))
| ~ 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))
| ~ 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))
| ~ m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))
| v1_xboole_0(u1_struct_0(sK0_skl)) ),
inference(resolution,[status(thm)],[f701,f129]) ).
fof(f926,definition,
( sQ100_spl
<=> r1_lattice2(u1_struct_0(sK0_skl),u1_lattices(sK0_skl),u2_lattices(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f928,plain,
( sQ100_spl
| ~ r1_lattice2(u1_struct_0(sK0_skl),u1_lattices(sK0_skl),u2_lattices(sK0_skl)) ),
inference(component_clause,[status(thm)],[f926]) ).
fof(f929,plain,
( ~ sQ76_spl
| ~ sQ42_spl
| ~ sQ100_spl
| ~ sQ40_spl
| ~ sQ43_spl
| ~ sQ98_spl
| ~ sQ39_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f925,f483,f486,f918,f505,f489,f926,f495,f700]) ).
fof(f941,definition,
( sQ101_spl
<=> v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f942,plain,
( ~ sQ101_spl
| v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK0_skl))) ),
inference(component_clause,[status(thm)],[f941]) ).
fof(f952,plain,
( ~ sQ101_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f942,f153]) ).
fof(f953,plain,
~ sQ101_spl,
inference(contradiction_clause,[status(thm)],[f952]) ).
fof(f972,plain,
( sQ98_spl
| ~ l1_lattices(sK0_skl) ),
inference(resolution,[status(thm)],[f920,f125]) ).
fof(f973,plain,
( sQ98_spl
| ~ sQ45_spl ),
inference(split_clause,[status(thm)],[f972,f511,f918]) ).
fof(f974,plain,
( sQ99_spl
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f923,f241]) ).
fof(f975,plain,
( sQ99_spl
| ~ sQ14_spl
| ~ sQ46_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f974,f348,f537,f345,f921]) ).
fof(f977,plain,
( sQ100_spl
| ~ l3_lattices(sK0_skl)
| ~ v10_lattices(sK0_skl)
| v3_struct_0(sK0_skl) ),
inference(resolution,[status(thm)],[f928,f243]) ).
fof(f978,plain,
( sQ100_spl
| ~ sQ14_spl
| ~ sQ46_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f977,f348,f537,f345,f926]) ).
fof(f979,plain,
$false,
inference(sat_refutation,[status(thm)],[f278,f354,f356,f358,f363,f366,f388,f404,f406,f410,f412,f415,f419,f421,f424,f437,f444,f452,f456,f462,f471,f476,f498,f500,f514,f516,f617,f619,f624,f626,f628,f633,f638,f653,f655,f692,f706,f718,f720,f722,f725,f728,f731,f771,f901,f903,f905,f915,f924,f929,f953,f973,f975,f978]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT326+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n002.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sun Sep 20 23:41:01 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.37 % Drodi V4.1.1
% 0.12/0.42 % Refutation found
% 0.12/0.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/0.44 % Elapsed time: 0.074162 seconds
% 0.12/0.44 % CPU time: 0.324278 seconds
% 0.12/0.44 % Total memory used: 113.156 MB
% 0.12/0.44 % Net memory used: 112.948 MB
%------------------------------------------------------------------------------