%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT343+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 : n004.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:50 PM UTC 2026
% Result : Theorem 2.52s 0.83s
% Output : CNFRefutation 2.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 78
% Syntax : Number of formulae : 352 ( 41 unt; 53 def)
% Number of atoms : 1107 ( 46 equ)
% Maximal formula atoms : 13 ( 3 avg)
% Number of connectives : 1240 ( 485 ~; 539 |; 132 &)
% ( 56 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 83 ( 81 usr; 54 prp; 0-3 aty)
% Number of functors : 26 ( 26 usr; 7 con; 0-4 aty)
% Number of variables : 226 ( 217 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ! [B] :
( m1_subset_1(B,u1_conlat_1(A))
=> ! [C] :
( m1_subset_1(C,u2_conlat_1(A))
=> ( l3_conlat_1(k8_funct_2(u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k5_conlat_2(A),C),A)
& v9_conlat_1(k8_funct_2(u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k5_conlat_2(A),C),A)
& ~ v7_conlat_1(k8_funct_2(u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k5_conlat_2(A),C),A)
& l3_conlat_1(k8_funct_2(u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k4_conlat_2(A),B),A)
& v9_conlat_1(k8_funct_2(u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k4_conlat_2(A),B),A)
& ~ v7_conlat_1(k8_funct_2(u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k4_conlat_2(A),B),A) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ! [B] :
( m1_subset_1(B,u1_conlat_1(A))
=> ! [C] :
( m1_subset_1(C,u2_conlat_1(A))
=> ( l3_conlat_1(k8_funct_2(u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k5_conlat_2(A),C),A)
& v9_conlat_1(k8_funct_2(u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k5_conlat_2(A),C),A)
& ~ v7_conlat_1(k8_funct_2(u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k5_conlat_2(A),C),A)
& l3_conlat_1(k8_funct_2(u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k4_conlat_2(A),B),A)
& v9_conlat_1(k8_funct_2(u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k4_conlat_2(A),B),A)
& ~ v7_conlat_1(k8_funct_2(u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k4_conlat_2(A),B),A) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,axiom,
! [A] :
( l3_lattices(A)
=> ( v3_lattices(A)
=> A = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ! [B] :
( ~ v1_xboole_0(B)
=> ( m1_conlat_1(B,A)
<=> ! [C] :
( r2_hidden(C,B)
=> ( l3_conlat_1(C,A)
& v9_conlat_1(C,A)
& ~ v7_conlat_1(C,A) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> k11_conlat_1(A) = g3_lattices(k8_conlat_1(A),k10_conlat_1(A),k9_conlat_1(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ( m2_relset_1(k10_conlat_1(A),k2_zfmisc_1(k8_conlat_1(A),k8_conlat_1(A)),k8_conlat_1(A))
& v1_funct_2(k10_conlat_1(A),k2_zfmisc_1(k8_conlat_1(A),k8_conlat_1(A)),k8_conlat_1(A))
& v1_funct_1(k10_conlat_1(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ( l3_lattices(k11_conlat_1(A))
& v3_lattices(k11_conlat_1(A))
& ~ v3_struct_0(k11_conlat_1(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ( m2_relset_1(k4_conlat_2(A),u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)))
& v1_funct_2(k4_conlat_2(A),u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)))
& v1_funct_1(k4_conlat_2(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ( m2_relset_1(k5_conlat_2(A),u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)))
& v1_funct_2(k5_conlat_2(A),u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)))
& v1_funct_1(k5_conlat_2(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> m1_conlat_1(k8_conlat_1(A),A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
! [A,B,C,D] :
( ( m1_subset_1(D,A)
& m1_relset_1(C,A,B)
& v1_funct_2(C,A,B)
& v1_funct_1(C)
& ~ v1_xboole_0(A) )
=> m1_subset_1(k8_funct_2(A,B,C,D),B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ( m2_relset_1(k9_conlat_1(A),k2_zfmisc_1(k8_conlat_1(A),k8_conlat_1(A)),k8_conlat_1(A))
& v1_funct_2(k9_conlat_1(A),k2_zfmisc_1(k8_conlat_1(A),k8_conlat_1(A)),k8_conlat_1(A))
& v1_funct_1(k9_conlat_1(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
! [A] :
( l2_conlat_1(A)
=> l1_conlat_1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ! [B] :
( m1_conlat_1(B,A)
=> ~ v1_xboole_0(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,axiom,
! [A] :
? [B] : m1_subset_1(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f56,axiom,
! [A] :
( ( l1_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ~ v1_xboole_0(u2_conlat_1(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f61,axiom,
! [A] :
( ( l1_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ~ v1_xboole_0(u1_conlat_1(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,axiom,
! [A,B,C] :
( ( m1_relset_1(C,k2_zfmisc_1(A,A),A)
& v1_funct_2(C,k2_zfmisc_1(A,A),A)
& v1_funct_1(C)
& m1_relset_1(B,k2_zfmisc_1(A,A),A)
& v1_funct_2(B,k2_zfmisc_1(A,A),A)
& v1_funct_1(B) )
=> ! [D,E,F] :
( g3_lattices(A,B,C) = g3_lattices(D,E,F)
=> ( C = F
& B = E
& A = D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f72,axiom,
? [A] :
( v15_lattices(A)
& v14_lattices(A)
& v13_lattices(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& v3_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,axiom,
! [A,B] :
? [C] :
( v1_funct_2(C,A,B)
& v1_funct_1(C)
& v1_relat_1(C)
& m1_relset_1(C,A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f83,axiom,
? [A] :
( v3_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f86,axiom,
? [A] :
( v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& v3_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f87,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> k8_conlat_1(A) = k7_conlat_1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f89,axiom,
! [A,B,C] :
( m2_relset_1(C,A,B)
<=> m1_relset_1(C,A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f92,axiom,
! [A,B] :
( m1_subset_1(A,B)
=> ( r2_hidden(A,B)
| v1_xboole_0(B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f97,axiom,
! [A,B] :
~ ( v1_xboole_0(B)
& r2_hidden(A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f99,plain,
? [A] :
( ? [B] :
( ? [C] :
( ( ~ l3_conlat_1(k8_funct_2(u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k5_conlat_2(A),C),A)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k5_conlat_2(A),C),A)
| v7_conlat_1(k8_funct_2(u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k5_conlat_2(A),C),A)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k4_conlat_2(A),B),A)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k4_conlat_2(A),B),A)
| v7_conlat_1(k8_funct_2(u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k4_conlat_2(A),B),A) )
& m1_subset_1(C,u2_conlat_1(A)) )
& m1_subset_1(B,u1_conlat_1(A)) )
& l2_conlat_1(A)
& ~ v3_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f100,plain,
( ( ~ l3_conlat_1(k8_funct_2(u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k5_conlat_2(sK0_skl),sK2_skl),sK0_skl)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k5_conlat_2(sK0_skl),sK2_skl),sK0_skl)
| v7_conlat_1(k8_funct_2(u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k5_conlat_2(sK0_skl),sK2_skl),sK0_skl)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k4_conlat_2(sK0_skl),sK1_skl),sK0_skl)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k4_conlat_2(sK0_skl),sK1_skl),sK0_skl)
| v7_conlat_1(k8_funct_2(u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k4_conlat_2(sK0_skl),sK1_skl),sK0_skl) )
& m1_subset_1(sK2_skl,u2_conlat_1(sK0_skl))
& m1_subset_1(sK1_skl,u1_conlat_1(sK0_skl))
& l2_conlat_1(sK0_skl)
& ~ v3_conlat_1(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)],[f99]) ).
fof(f101,plain,
~ v3_conlat_1(sK0_skl),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f102,plain,
l2_conlat_1(sK0_skl),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f103,plain,
m1_subset_1(sK1_skl,u1_conlat_1(sK0_skl)),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f104,plain,
m1_subset_1(sK2_skl,u2_conlat_1(sK0_skl)),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f105,plain,
( ~ l3_conlat_1(k8_funct_2(u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k5_conlat_2(sK0_skl),sK2_skl),sK0_skl)
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k5_conlat_2(sK0_skl),sK2_skl),sK0_skl)
| v7_conlat_1(k8_funct_2(u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k5_conlat_2(sK0_skl),sK2_skl),sK0_skl)
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k4_conlat_2(sK0_skl),sK1_skl),sK0_skl)
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k4_conlat_2(sK0_skl),sK1_skl),sK0_skl)
| v7_conlat_1(k8_funct_2(u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k4_conlat_2(sK0_skl),sK1_skl),sK0_skl) ),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f106,plain,
! [A] :
( A = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A))
| ~ v3_lattices(A)
| ~ l3_lattices(A) ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f107,plain,
! [X0] :
( X0 = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f146,plain,
! [A] :
( ! [B] :
( ( m1_conlat_1(B,A)
<=> ! [C] :
( ( l3_conlat_1(C,A)
& v9_conlat_1(C,A)
& ~ v7_conlat_1(C,A) )
| ~ r2_hidden(C,B) ) )
| v1_xboole_0(B) )
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f14]) ).
fof(f147,plain,
! [A] :
( ! [B] :
( ( ( ? [C] :
( ( ~ l3_conlat_1(C,A)
| ~ v9_conlat_1(C,A)
| v7_conlat_1(C,A) )
& r2_hidden(C,B) )
| m1_conlat_1(B,A) )
& ( ! [C] :
( ( l3_conlat_1(C,A)
& v9_conlat_1(C,A)
& ~ v7_conlat_1(C,A) )
| ~ r2_hidden(C,B) )
| ~ m1_conlat_1(B,A) ) )
| v1_xboole_0(B) )
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(NNF_transformation,[status(thm)],[f146]) ).
fof(f148,plain,
! [A] :
( ! [B] :
( ( ( ( ( ~ l3_conlat_1(sK3_skl(B,A),A)
| ~ v9_conlat_1(sK3_skl(B,A),A)
| v7_conlat_1(sK3_skl(B,A),A) )
& r2_hidden(sK3_skl(B,A),B) )
| m1_conlat_1(B,A) )
& ( ! [C] :
( ( l3_conlat_1(C,A)
& v9_conlat_1(C,A)
& ~ v7_conlat_1(C,A) )
| ~ r2_hidden(C,B) )
| ~ m1_conlat_1(B,A) ) )
| v1_xboole_0(B) )
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(C,sK3_skl(B,A))],[f147]) ).
fof(f149,plain,
! [X0,X1,X2] :
( ~ v7_conlat_1(X2,X0)
| ~ r2_hidden(X2,X1)
| ~ m1_conlat_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f150,plain,
! [X0,X1,X2] :
( v9_conlat_1(X2,X0)
| ~ r2_hidden(X2,X1)
| ~ m1_conlat_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f151,plain,
! [X0,X1,X2] :
( l3_conlat_1(X2,X0)
| ~ r2_hidden(X2,X1)
| ~ m1_conlat_1(X1,X0)
| v1_xboole_0(X1)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f148]) ).
fof(f154,plain,
! [A] :
( k11_conlat_1(A) = g3_lattices(k8_conlat_1(A),k10_conlat_1(A),k9_conlat_1(A))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f155,plain,
! [X0] :
( k11_conlat_1(X0) = g3_lattices(k8_conlat_1(X0),k10_conlat_1(X0),k9_conlat_1(X0))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f159,plain,
! [A] :
( ( m2_relset_1(k10_conlat_1(A),k2_zfmisc_1(k8_conlat_1(A),k8_conlat_1(A)),k8_conlat_1(A))
& v1_funct_2(k10_conlat_1(A),k2_zfmisc_1(k8_conlat_1(A),k8_conlat_1(A)),k8_conlat_1(A))
& v1_funct_1(k10_conlat_1(A)) )
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f17]) ).
fof(f160,plain,
! [X0] :
( v1_funct_1(k10_conlat_1(X0))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f161,plain,
! [X0] :
( v1_funct_2(k10_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f162,plain,
! [X0] :
( m2_relset_1(k10_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f163,plain,
! [A] :
( ( l3_lattices(k11_conlat_1(A))
& v3_lattices(k11_conlat_1(A))
& ~ v3_struct_0(k11_conlat_1(A)) )
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f165,plain,
! [X0] :
( v3_lattices(k11_conlat_1(X0))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f166,plain,
! [X0] :
( l3_lattices(k11_conlat_1(X0))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f167,plain,
! [A] :
( ( m2_relset_1(k4_conlat_2(A),u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)))
& v1_funct_2(k4_conlat_2(A),u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)))
& v1_funct_1(k4_conlat_2(A)) )
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f168,plain,
! [X0] :
( v1_funct_1(k4_conlat_2(X0))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f169,plain,
! [X0] :
( v1_funct_2(k4_conlat_2(X0),u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f170,plain,
! [X0] :
( m2_relset_1(k4_conlat_2(X0),u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f171,plain,
! [A] :
( ( m2_relset_1(k5_conlat_2(A),u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)))
& v1_funct_2(k5_conlat_2(A),u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)))
& v1_funct_1(k5_conlat_2(A)) )
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f172,plain,
! [X0] :
( v1_funct_1(k5_conlat_2(X0))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f173,plain,
! [X0] :
( v1_funct_2(k5_conlat_2(X0),u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f174,plain,
! [X0] :
( m2_relset_1(k5_conlat_2(X0),u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f177,plain,
! [A] :
( m1_conlat_1(k8_conlat_1(A),A)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f26]) ).
fof(f178,plain,
! [X0] :
( m1_conlat_1(k8_conlat_1(X0),X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f177]) ).
fof(f179,plain,
! [A,B,C,D] :
( m1_subset_1(k8_funct_2(A,B,C,D),B)
| ~ m1_subset_1(D,A)
| ~ m1_relset_1(C,A,B)
| ~ v1_funct_2(C,A,B)
| ~ v1_funct_1(C)
| v1_xboole_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f180,plain,
! [X0,X1,X2,X3] :
( m1_subset_1(k8_funct_2(X0,X2,X1,X3),X2)
| ~ m1_subset_1(X3,X0)
| ~ m1_relset_1(X1,X0,X2)
| ~ v1_funct_2(X1,X0,X2)
| ~ v1_funct_1(X1)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[status(thm)],[f179]) ).
fof(f181,plain,
! [A] :
( ( m2_relset_1(k9_conlat_1(A),k2_zfmisc_1(k8_conlat_1(A),k8_conlat_1(A)),k8_conlat_1(A))
& v1_funct_2(k9_conlat_1(A),k2_zfmisc_1(k8_conlat_1(A),k8_conlat_1(A)),k8_conlat_1(A))
& v1_funct_1(k9_conlat_1(A)) )
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f182,plain,
! [X0] :
( v1_funct_1(k9_conlat_1(X0))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f183,plain,
! [X0] :
( v1_funct_2(k9_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f184,plain,
! [X0] :
( m2_relset_1(k9_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f181]) ).
fof(f187,plain,
! [A] :
( l1_conlat_1(A)
| ~ l2_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f32]) ).
fof(f188,plain,
! [X0] :
( l1_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f187]) ).
fof(f194,plain,
! [A] :
( ! [B] :
( ~ v1_xboole_0(B)
| ~ m1_conlat_1(B,A) )
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f195,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ m1_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f194]) ).
fof(f226,plain,
! [A] : m1_subset_1(sK13_skl(A),A),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(B,sK13_skl(A))],[f54]) ).
fof(f227,plain,
! [X0] : m1_subset_1(sK13_skl(X0),X0),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f230,plain,
! [A] :
( ~ v1_xboole_0(u2_conlat_1(A))
| ~ l1_conlat_1(A)
| v3_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f56]) ).
fof(f231,plain,
! [X0] :
( ~ v1_xboole_0(u2_conlat_1(X0))
| ~ l1_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f230]) ).
fof(f250,plain,
! [A] :
( ~ v1_xboole_0(u1_conlat_1(A))
| ~ l1_conlat_1(A)
| v3_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f61]) ).
fof(f251,plain,
! [X0] :
( ~ v1_xboole_0(u1_conlat_1(X0))
| ~ l1_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f250]) ).
fof(f304,plain,
! [A,B,C] :
( ! [D,E,F] :
( ( C = F
& B = E
& A = D )
| g3_lattices(A,B,C) != g3_lattices(D,E,F) )
| ~ m1_relset_1(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(C,k2_zfmisc_1(A,A),A)
| ~ v1_funct_1(C)
| ~ m1_relset_1(B,k2_zfmisc_1(A,A),A)
| ~ v1_funct_2(B,k2_zfmisc_1(A,A),A)
| ~ v1_funct_1(B) ),
inference(pre_NNF_transformation,[status(thm)],[f71]) ).
fof(f305,plain,
! [X0,X1,X2,X3,X4,X5] :
( X1 = X3
| g3_lattices(X1,X0,X2) != g3_lattices(X3,X4,X5)
| ~ m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X2)
| ~ m1_relset_1(X0,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)
| ~ v1_funct_1(X0) ),
inference(cnf_transformation,[status(thm)],[f304]) ).
fof(f308,plain,
( v15_lattices(sK15_skl)
& v14_lattices(sK15_skl)
& v13_lattices(sK15_skl)
& v10_lattices(sK15_skl)
& v9_lattices(sK15_skl)
& v8_lattices(sK15_skl)
& v7_lattices(sK15_skl)
& v6_lattices(sK15_skl)
& v5_lattices(sK15_skl)
& v4_lattices(sK15_skl)
& v3_lattices(sK15_skl)
& ~ v3_struct_0(sK15_skl)
& l3_lattices(sK15_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(A,sK15_skl)],[f72]) ).
fof(f310,plain,
~ v3_struct_0(sK15_skl),
inference(cnf_transformation,[status(thm)],[f308]) ).
fof(f312,plain,
v4_lattices(sK15_skl),
inference(cnf_transformation,[status(thm)],[f308]) ).
fof(f313,plain,
v5_lattices(sK15_skl),
inference(cnf_transformation,[status(thm)],[f308]) ).
fof(f314,plain,
v6_lattices(sK15_skl),
inference(cnf_transformation,[status(thm)],[f308]) ).
fof(f315,plain,
v7_lattices(sK15_skl),
inference(cnf_transformation,[status(thm)],[f308]) ).
fof(f327,plain,
! [A,B] :
( v1_funct_2(sK17_skl(B,A),A,B)
& v1_funct_1(sK17_skl(B,A))
& v1_relat_1(sK17_skl(B,A))
& m1_relset_1(sK17_skl(B,A),A,B) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(C,sK17_skl(B,A))],[f74]) ).
fof(f328,plain,
! [X0,X1] : m1_relset_1(sK17_skl(X0,X1),X1,X0),
inference(cnf_transformation,[status(thm)],[f327]) ).
fof(f330,plain,
! [X0,X1] : v1_funct_1(sK17_skl(X0,X1)),
inference(cnf_transformation,[status(thm)],[f327]) ).
fof(f357,plain,
( v3_lattices(sK26_skl)
& ~ v3_struct_0(sK26_skl)
& l3_lattices(sK26_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl]),skolemize(A,sK26_skl)],[f83]) ).
fof(f359,plain,
~ v3_struct_0(sK26_skl),
inference(cnf_transformation,[status(thm)],[f357]) ).
fof(f369,plain,
( v10_lattices(sK29_skl)
& v9_lattices(sK29_skl)
& v8_lattices(sK29_skl)
& v7_lattices(sK29_skl)
& v6_lattices(sK29_skl)
& v5_lattices(sK29_skl)
& v4_lattices(sK29_skl)
& v3_lattices(sK29_skl)
& ~ v3_struct_0(sK29_skl)
& l3_lattices(sK29_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl]),skolemize(A,sK29_skl)],[f86]) ).
fof(f371,plain,
~ v3_struct_0(sK29_skl),
inference(cnf_transformation,[status(thm)],[f369]) ).
fof(f373,plain,
v4_lattices(sK29_skl),
inference(cnf_transformation,[status(thm)],[f369]) ).
fof(f374,plain,
v5_lattices(sK29_skl),
inference(cnf_transformation,[status(thm)],[f369]) ).
fof(f375,plain,
v6_lattices(sK29_skl),
inference(cnf_transformation,[status(thm)],[f369]) ).
fof(f376,plain,
v7_lattices(sK29_skl),
inference(cnf_transformation,[status(thm)],[f369]) ).
fof(f380,plain,
! [A] :
( k8_conlat_1(A) = k7_conlat_1(A)
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f87]) ).
fof(f381,plain,
! [X0] :
( k8_conlat_1(X0) = k7_conlat_1(X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f380]) ).
fof(f384,plain,
! [A,B,C] :
( ( ~ m1_relset_1(C,A,B)
| m2_relset_1(C,A,B) )
& ( m1_relset_1(C,A,B)
| ~ m2_relset_1(C,A,B) ) ),
inference(NNF_transformation,[status(thm)],[f89]) ).
fof(f385,plain,
( ! [A,B,C] :
( ~ m1_relset_1(C,A,B)
| m2_relset_1(C,A,B) )
& ! [A,B,C] :
( m1_relset_1(C,A,B)
| ~ m2_relset_1(C,A,B) ) ),
inference(miniscoping,[status(thm)],[f384]) ).
fof(f386,plain,
! [X0,X1,X2] :
( m1_relset_1(X0,X1,X2)
| ~ m2_relset_1(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f385]) ).
fof(f392,plain,
! [A,B] :
( r2_hidden(A,B)
| v1_xboole_0(B)
| ~ m1_subset_1(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f92]) ).
fof(f393,plain,
! [X0,X1] :
( r2_hidden(X0,X1)
| v1_xboole_0(X1)
| ~ m1_subset_1(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f392]) ).
fof(f406,plain,
! [A,B] :
( ~ v1_xboole_0(B)
| ~ r2_hidden(A,B) ),
inference(pre_NNF_transformation,[status(thm)],[f97]) ).
fof(f407,plain,
! [B] :
( ~ v1_xboole_0(B)
| ! [A] : ~ r2_hidden(A,B) ),
inference(miniscoping,[status(thm)],[f406]) ).
fof(f408,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ r2_hidden(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f407]) ).
fof(f412,definition,
( sQ0_spl
<=> v7_conlat_1(k8_funct_2(u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k4_conlat_2(sK0_skl),sK1_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f413,plain,
( ~ sQ0_spl
| v7_conlat_1(k8_funct_2(u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k4_conlat_2(sK0_skl),sK1_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f412]) ).
fof(f415,definition,
( sQ1_spl
<=> v9_conlat_1(k8_funct_2(u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k4_conlat_2(sK0_skl),sK1_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f417,plain,
( sQ1_spl
| ~ v9_conlat_1(k8_funct_2(u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k4_conlat_2(sK0_skl),sK1_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f415]) ).
fof(f418,definition,
( sQ2_spl
<=> l3_conlat_1(k8_funct_2(u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k4_conlat_2(sK0_skl),sK1_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f420,plain,
( sQ2_spl
| ~ l3_conlat_1(k8_funct_2(u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k4_conlat_2(sK0_skl),sK1_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f418]) ).
fof(f421,definition,
( sQ3_spl
<=> v7_conlat_1(k8_funct_2(u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k5_conlat_2(sK0_skl),sK2_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f422,plain,
( ~ sQ3_spl
| v7_conlat_1(k8_funct_2(u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k5_conlat_2(sK0_skl),sK2_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f421]) ).
fof(f424,definition,
( sQ4_spl
<=> v9_conlat_1(k8_funct_2(u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k5_conlat_2(sK0_skl),sK2_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f426,plain,
( sQ4_spl
| ~ v9_conlat_1(k8_funct_2(u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k5_conlat_2(sK0_skl),sK2_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f424]) ).
fof(f427,definition,
( sQ5_spl
<=> l3_conlat_1(k8_funct_2(u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k5_conlat_2(sK0_skl),sK2_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f429,plain,
( sQ5_spl
| ~ l3_conlat_1(k8_funct_2(u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k5_conlat_2(sK0_skl),sK2_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f427]) ).
fof(f430,plain,
( ~ sQ5_spl
| ~ sQ4_spl
| sQ3_spl
| ~ sQ2_spl
| ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f105,f412,f415,f418,f421,f424,f427]) ).
fof(f497,plain,
l1_conlat_1(sK0_skl),
inference(resolution,[status(thm)],[f188,f102]) ).
fof(f511,plain,
( ~ v1_xboole_0(u1_conlat_1(sK0_skl))
| v3_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f497,f251]) ).
fof(f512,plain,
( ~ v1_xboole_0(u2_conlat_1(sK0_skl))
| v3_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f497,f231]) ).
fof(f513,definition,
( sQ20_spl
<=> v3_conlat_1(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f514,plain,
( ~ sQ20_spl
| v3_conlat_1(sK0_skl) ),
inference(component_clause,[status(thm)],[f513]) ).
fof(f516,definition,
( sQ21_spl
<=> v1_xboole_0(u1_conlat_1(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f519,plain,
( ~ sQ21_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f511,f513,f516]) ).
fof(f520,definition,
( sQ22_spl
<=> v1_xboole_0(u2_conlat_1(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f523,plain,
( ~ sQ22_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f512,f513,f520]) ).
fof(f524,plain,
( ~ sQ20_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f514,f101]) ).
fof(f525,plain,
~ sQ20_spl,
inference(contradiction_clause,[status(thm)],[f524]) ).
fof(f546,plain,
! [X0,X1,X2] :
( l3_conlat_1(X2,X0)
| ~ r2_hidden(X2,X1)
| ~ m1_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f151,f408]) ).
fof(f547,plain,
! [X0,X1,X2] :
( v9_conlat_1(X2,X0)
| ~ r2_hidden(X2,X1)
| ~ m1_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f150,f408]) ).
fof(f548,plain,
! [X0,X1,X2] :
( ~ v7_conlat_1(X2,X0)
| ~ r2_hidden(X2,X1)
| ~ m1_conlat_1(X1,X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f149,f408]) ).
fof(f568,plain,
( k11_conlat_1(sK0_skl) = g3_lattices(k8_conlat_1(sK0_skl),k10_conlat_1(sK0_skl),k9_conlat_1(sK0_skl))
| ~ l2_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f155,f101]) ).
fof(f569,definition,
( sQ25_spl
<=> l2_conlat_1(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f571,plain,
( sQ25_spl
| ~ l2_conlat_1(sK0_skl) ),
inference(component_clause,[status(thm)],[f569]) ).
fof(f572,definition,
( sQ26_spl
<=> k11_conlat_1(sK0_skl) = g3_lattices(k8_conlat_1(sK0_skl),k10_conlat_1(sK0_skl),k9_conlat_1(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f573,plain,
( ~ sQ26_spl
| k11_conlat_1(sK0_skl) = g3_lattices(k8_conlat_1(sK0_skl),k10_conlat_1(sK0_skl),k9_conlat_1(sK0_skl)) ),
inference(component_clause,[status(thm)],[f572]) ).
fof(f575,plain,
( sQ26_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f568,f569,f572]) ).
fof(f576,plain,
( sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f571,f102]) ).
fof(f577,plain,
sQ25_spl,
inference(contradiction_clause,[status(thm)],[f576]) ).
fof(f581,definition,
( sQ27_spl
<=> v1_funct_1(k10_conlat_1(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f583,plain,
( sQ27_spl
| ~ v1_funct_1(k10_conlat_1(sK0_skl)) ),
inference(component_clause,[status(thm)],[f581]) ).
fof(f584,definition,
( sQ28_spl
<=> v1_funct_2(k10_conlat_1(sK0_skl),k2_zfmisc_1(k8_conlat_1(sK0_skl),k8_conlat_1(sK0_skl)),k8_conlat_1(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f585,plain,
( ~ sQ28_spl
| v1_funct_2(k10_conlat_1(sK0_skl),k2_zfmisc_1(k8_conlat_1(sK0_skl),k8_conlat_1(sK0_skl)),k8_conlat_1(sK0_skl)) ),
inference(component_clause,[status(thm)],[f584]) ).
fof(f586,plain,
( sQ28_spl
| ~ v1_funct_2(k10_conlat_1(sK0_skl),k2_zfmisc_1(k8_conlat_1(sK0_skl),k8_conlat_1(sK0_skl)),k8_conlat_1(sK0_skl)) ),
inference(component_clause,[status(thm)],[f584]) ).
fof(f587,definition,
( sQ29_spl
<=> m1_relset_1(k10_conlat_1(sK0_skl),k2_zfmisc_1(k8_conlat_1(sK0_skl),k8_conlat_1(sK0_skl)),k8_conlat_1(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f588,plain,
( ~ sQ29_spl
| m1_relset_1(k10_conlat_1(sK0_skl),k2_zfmisc_1(k8_conlat_1(sK0_skl),k8_conlat_1(sK0_skl)),k8_conlat_1(sK0_skl)) ),
inference(component_clause,[status(thm)],[f587]) ).
fof(f589,plain,
( sQ29_spl
| ~ m1_relset_1(k10_conlat_1(sK0_skl),k2_zfmisc_1(k8_conlat_1(sK0_skl),k8_conlat_1(sK0_skl)),k8_conlat_1(sK0_skl)) ),
inference(component_clause,[status(thm)],[f587]) ).
fof(f590,definition,
( sQ30_spl
<=> v1_funct_1(k9_conlat_1(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f592,plain,
( sQ30_spl
| ~ v1_funct_1(k9_conlat_1(sK0_skl)) ),
inference(component_clause,[status(thm)],[f590]) ).
fof(f593,definition,
( sQ31_spl
<=> v1_funct_2(k9_conlat_1(sK0_skl),k2_zfmisc_1(k8_conlat_1(sK0_skl),k8_conlat_1(sK0_skl)),k8_conlat_1(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f594,plain,
( ~ sQ31_spl
| v1_funct_2(k9_conlat_1(sK0_skl),k2_zfmisc_1(k8_conlat_1(sK0_skl),k8_conlat_1(sK0_skl)),k8_conlat_1(sK0_skl)) ),
inference(component_clause,[status(thm)],[f593]) ).
fof(f599,definition,
( sQ33_spl
<=> l3_lattices(k11_conlat_1(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f601,plain,
( sQ33_spl
| ~ l3_lattices(k11_conlat_1(sK0_skl)) ),
inference(component_clause,[status(thm)],[f599]) ).
fof(f603,definition,
( sQ34_spl
<=> v3_lattices(k11_conlat_1(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f604,plain,
( ~ sQ34_spl
| v3_lattices(k11_conlat_1(sK0_skl)) ),
inference(component_clause,[status(thm)],[f603]) ).
fof(f605,plain,
( sQ34_spl
| ~ v3_lattices(k11_conlat_1(sK0_skl)) ),
inference(component_clause,[status(thm)],[f603]) ).
fof(f607,plain,
( sQ30_spl
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f592,f182]) ).
fof(f608,plain,
( sQ30_spl
| ~ sQ25_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f607,f513,f569,f590]) ).
fof(f609,plain,
( sQ27_spl
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f583,f160]) ).
fof(f610,plain,
( sQ27_spl
| ~ sQ25_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f609,f513,f569,f581]) ).
fof(f611,plain,
( ~ sQ34_spl
| k11_conlat_1(sK0_skl) = g3_lattices(u1_struct_0(k11_conlat_1(sK0_skl)),u2_lattices(k11_conlat_1(sK0_skl)),u1_lattices(k11_conlat_1(sK0_skl)))
| ~ l3_lattices(k11_conlat_1(sK0_skl)) ),
inference(resolution,[status(thm)],[f604,f107]) ).
fof(f612,definition,
( sQ35_spl
<=> k11_conlat_1(sK0_skl) = g3_lattices(u1_struct_0(k11_conlat_1(sK0_skl)),u2_lattices(k11_conlat_1(sK0_skl)),u1_lattices(k11_conlat_1(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f613,plain,
( ~ sQ35_spl
| k11_conlat_1(sK0_skl) = g3_lattices(u1_struct_0(k11_conlat_1(sK0_skl)),u2_lattices(k11_conlat_1(sK0_skl)),u1_lattices(k11_conlat_1(sK0_skl))) ),
inference(component_clause,[status(thm)],[f612]) ).
fof(f615,plain,
( ~ sQ34_spl
| sQ35_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f611,f599,f612,f603]) ).
fof(f617,plain,
( sQ29_spl
| ~ m2_relset_1(k10_conlat_1(sK0_skl),k2_zfmisc_1(k8_conlat_1(sK0_skl),k8_conlat_1(sK0_skl)),k8_conlat_1(sK0_skl)) ),
inference(resolution,[status(thm)],[f589,f386]) ).
fof(f642,plain,
( sQ33_spl
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f601,f166]) ).
fof(f643,plain,
( sQ33_spl
| ~ sQ25_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f642,f513,f569,f599]) ).
fof(f655,plain,
( sQ28_spl
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f161,f586]) ).
fof(f656,plain,
( sQ28_spl
| ~ sQ25_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f655,f513,f569,f584]) ).
fof(f657,plain,
( sQ29_spl
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f162,f617]) ).
fof(f658,plain,
( sQ29_spl
| ~ sQ25_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f657,f513,f569,f587]) ).
fof(f760,plain,
( sQ34_spl
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f605,f165]) ).
fof(f761,plain,
( sQ34_spl
| ~ sQ25_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f760,f513,f569,f603]) ).
fof(f772,plain,
! [X0,X1,X2] :
( ~ v7_conlat_1(X0,X2)
| ~ m1_conlat_1(X1,X2)
| ~ l2_conlat_1(X2)
| v3_conlat_1(X2)
| v1_xboole_0(X1)
| ~ m1_subset_1(X0,X1) ),
inference(resolution,[status(thm)],[f393,f548]) ).
fof(f773,plain,
! [X0,X1,X2] :
( v9_conlat_1(X0,X2)
| ~ m1_conlat_1(X1,X2)
| ~ l2_conlat_1(X2)
| v3_conlat_1(X2)
| v1_xboole_0(X1)
| ~ m1_subset_1(X0,X1) ),
inference(resolution,[status(thm)],[f393,f547]) ).
fof(f774,plain,
! [X0,X1,X2] :
( l3_conlat_1(X0,X2)
| ~ m1_conlat_1(X1,X2)
| ~ l2_conlat_1(X2)
| v3_conlat_1(X2)
| v1_xboole_0(X1)
| ~ m1_subset_1(X0,X1) ),
inference(resolution,[status(thm)],[f393,f546]) ).
fof(f791,plain,
( v1_funct_2(k9_conlat_1(sK0_skl),k2_zfmisc_1(k8_conlat_1(sK0_skl),k8_conlat_1(sK0_skl)),k8_conlat_1(sK0_skl))
| ~ l2_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f183,f101]) ).
fof(f792,plain,
( sQ31_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f791,f569,f593]) ).
fof(f796,plain,
( m2_relset_1(k9_conlat_1(sK0_skl),k2_zfmisc_1(k8_conlat_1(sK0_skl),k8_conlat_1(sK0_skl)),k8_conlat_1(sK0_skl))
| ~ l2_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f184,f101]) ).
fof(f797,definition,
( sQ61_spl
<=> m2_relset_1(k9_conlat_1(sK0_skl),k2_zfmisc_1(k8_conlat_1(sK0_skl),k8_conlat_1(sK0_skl)),k8_conlat_1(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f798,plain,
( ~ sQ61_spl
| m2_relset_1(k9_conlat_1(sK0_skl),k2_zfmisc_1(k8_conlat_1(sK0_skl),k8_conlat_1(sK0_skl)),k8_conlat_1(sK0_skl)) ),
inference(component_clause,[status(thm)],[f797]) ).
fof(f800,plain,
( sQ61_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f796,f569,f797]) ).
fof(f860,plain,
! [X0,X1,X2] :
( ~ v7_conlat_1(X0,X2)
| ~ m1_conlat_1(X1,X2)
| ~ l2_conlat_1(X2)
| v3_conlat_1(X2)
| ~ m1_subset_1(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f772,f195]) ).
fof(f861,plain,
! [X0,X1,X2] :
( v9_conlat_1(X0,X2)
| ~ m1_conlat_1(X1,X2)
| ~ l2_conlat_1(X2)
| v3_conlat_1(X2)
| ~ m1_subset_1(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f773,f195]) ).
fof(f862,plain,
( k8_conlat_1(sK0_skl) = k7_conlat_1(sK0_skl)
| ~ l2_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f381,f101]) ).
fof(f863,definition,
( sQ70_spl
<=> k8_conlat_1(sK0_skl) = k7_conlat_1(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f864,plain,
( ~ sQ70_spl
| k8_conlat_1(sK0_skl) = k7_conlat_1(sK0_skl) ),
inference(component_clause,[status(thm)],[f863]) ).
fof(f866,plain,
( sQ70_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f862,f569,f863]) ).
fof(f867,plain,
( ~ sQ61_spl
| ~ sQ70_spl
| m2_relset_1(k9_conlat_1(sK0_skl),k2_zfmisc_1(k8_conlat_1(sK0_skl),k8_conlat_1(sK0_skl)),k7_conlat_1(sK0_skl)) ),
inference(backward_demodulation,[status(thm)],[f864,f798]) ).
fof(f870,plain,
( ~ sQ70_spl
| m1_conlat_1(k7_conlat_1(sK0_skl),sK0_skl)
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl) ),
inference(paramodulation,[status(thm)],[f864,f178]) ).
fof(f877,plain,
( ~ sQ61_spl
| ~ sQ70_spl
| m2_relset_1(k9_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k8_conlat_1(sK0_skl)),k7_conlat_1(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f864,f867]) ).
fof(f878,plain,
( ~ sQ61_spl
| ~ sQ70_spl
| m2_relset_1(k9_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k7_conlat_1(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f864,f877]) ).
fof(f879,definition,
( sQ71_spl
<=> m1_conlat_1(k7_conlat_1(sK0_skl),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f880,plain,
( ~ sQ71_spl
| m1_conlat_1(k7_conlat_1(sK0_skl),sK0_skl) ),
inference(component_clause,[status(thm)],[f879]) ).
fof(f882,plain,
( ~ sQ70_spl
| sQ71_spl
| ~ sQ25_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f870,f513,f569,f879,f863]) ).
fof(f928,plain,
( ~ sQ26_spl
| ~ sQ70_spl
| k11_conlat_1(sK0_skl) = g3_lattices(k7_conlat_1(sK0_skl),k10_conlat_1(sK0_skl),k9_conlat_1(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f864,f573]) ).
fof(f934,definition,
( sQ79_spl
<=> m1_relset_1(k10_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k7_conlat_1(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f936,plain,
( sQ79_spl
| ~ m1_relset_1(k10_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k7_conlat_1(sK0_skl)) ),
inference(component_clause,[status(thm)],[f934]) ).
fof(f940,definition,
( sQ81_spl
<=> m1_relset_1(k9_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k7_conlat_1(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f942,plain,
( sQ81_spl
| ~ m1_relset_1(k9_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k7_conlat_1(sK0_skl)) ),
inference(component_clause,[status(thm)],[f940]) ).
fof(f953,plain,
( ~ sQ31_spl
| ~ sQ70_spl
| v1_funct_2(k9_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k8_conlat_1(sK0_skl)),k8_conlat_1(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f864,f594]) ).
fof(f954,plain,
( ~ sQ31_spl
| ~ sQ70_spl
| v1_funct_2(k9_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k8_conlat_1(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f864,f953]) ).
fof(f955,plain,
( ~ sQ31_spl
| ~ sQ70_spl
| v1_funct_2(k9_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k7_conlat_1(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f864,f954]) ).
fof(f956,plain,
( ~ sQ29_spl
| ~ sQ70_spl
| m1_relset_1(k10_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k8_conlat_1(sK0_skl)),k8_conlat_1(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f864,f588]) ).
fof(f957,plain,
( ~ sQ29_spl
| ~ sQ70_spl
| m1_relset_1(k10_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k8_conlat_1(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f864,f956]) ).
fof(f958,plain,
( ~ sQ29_spl
| ~ sQ70_spl
| m1_relset_1(k10_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k7_conlat_1(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f864,f957]) ).
fof(f964,plain,
( ~ sQ28_spl
| ~ sQ70_spl
| v1_funct_2(k10_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k8_conlat_1(sK0_skl)),k8_conlat_1(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f864,f585]) ).
fof(f965,plain,
( ~ sQ28_spl
| ~ sQ70_spl
| v1_funct_2(k10_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k8_conlat_1(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f864,f964]) ).
fof(f966,plain,
( ~ sQ28_spl
| ~ sQ70_spl
| v1_funct_2(k10_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k7_conlat_1(sK0_skl)) ),
inference(forward_demodulation,[status(thm)],[f864,f965]) ).
fof(f970,plain,
! [X0,X1,X2] :
( l3_conlat_1(X0,X2)
| ~ m1_conlat_1(X1,X2)
| ~ l2_conlat_1(X2)
| v3_conlat_1(X2)
| ~ m1_subset_1(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f774,f195]) ).
fof(f971,plain,
! [X0,X1] :
( l3_conlat_1(X0,sK0_skl)
| ~ m1_conlat_1(X1,sK0_skl)
| ~ l2_conlat_1(sK0_skl)
| ~ m1_subset_1(X0,X1) ),
inference(resolution,[status(thm)],[f970,f101]) ).
fof(f972,definition,
! [X0,X1] :
( sQ83_spl
<=> ( l3_conlat_1(X0,sK0_skl)
| ~ m1_conlat_1(X1,sK0_skl)
| ~ m1_subset_1(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f973,plain,
! [X0,X1] :
( ~ sQ83_spl
| l3_conlat_1(X0,sK0_skl)
| ~ m1_conlat_1(X1,sK0_skl)
| ~ m1_subset_1(X0,X1) ),
inference(component_clause,[status(thm)],[f972]) ).
fof(f975,plain,
( ~ sQ25_spl
| sQ83_spl ),
inference(split_clause,[status(thm)],[f971,f972,f569]) ).
fof(f1048,plain,
! [X0] :
( sQ5_spl
| ~ sQ83_spl
| ~ m1_conlat_1(X0,sK0_skl)
| ~ m1_subset_1(k8_funct_2(u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k5_conlat_2(sK0_skl),sK2_skl),X0) ),
inference(resolution,[status(thm)],[f973,f429]) ).
fof(f1060,plain,
( sQ81_spl
| ~ m2_relset_1(k9_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k7_conlat_1(sK0_skl)) ),
inference(resolution,[status(thm)],[f942,f386]) ).
fof(f1061,plain,
( sQ81_spl
| ~ sQ61_spl
| ~ sQ70_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1060,f878]) ).
fof(f1062,plain,
( sQ81_spl
| ~ sQ61_spl
| ~ sQ70_spl ),
inference(contradiction_clause,[status(thm)],[f1061]) ).
fof(f1065,plain,
( sQ79_spl
| ~ sQ29_spl
| ~ sQ70_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f936,f958]) ).
fof(f1066,plain,
( sQ79_spl
| ~ sQ29_spl
| ~ sQ70_spl ),
inference(contradiction_clause,[status(thm)],[f1065]) ).
fof(f1163,plain,
( sQ5_spl
| ~ sQ83_spl
| ~ m1_subset_1(sK2_skl,u2_conlat_1(sK0_skl))
| ~ m1_relset_1(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)))
| ~ v1_funct_2(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)))
| ~ v1_funct_1(k5_conlat_2(sK0_skl))
| v1_xboole_0(u2_conlat_1(sK0_skl))
| ~ m1_conlat_1(u1_struct_0(k11_conlat_1(sK0_skl)),sK0_skl) ),
inference(resolution,[status(thm)],[f1048,f180]) ).
fof(f1167,definition,
( sQ107_spl
<=> m1_conlat_1(u1_struct_0(k11_conlat_1(sK0_skl)),sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f1169,plain,
( sQ107_spl
| ~ m1_conlat_1(u1_struct_0(k11_conlat_1(sK0_skl)),sK0_skl) ),
inference(component_clause,[status(thm)],[f1167]) ).
fof(f1170,definition,
( sQ108_spl
<=> v1_funct_1(k5_conlat_2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f1172,plain,
( sQ108_spl
| ~ v1_funct_1(k5_conlat_2(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1170]) ).
fof(f1173,definition,
( sQ109_spl
<=> v1_funct_2(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f1175,plain,
( sQ109_spl
| ~ v1_funct_2(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl))) ),
inference(component_clause,[status(thm)],[f1173]) ).
fof(f1176,definition,
( sQ110_spl
<=> m1_relset_1(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f1178,plain,
( sQ110_spl
| ~ m1_relset_1(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl))) ),
inference(component_clause,[status(thm)],[f1176]) ).
fof(f1179,definition,
( sQ111_spl
<=> m1_subset_1(sK2_skl,u2_conlat_1(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition]) ).
fof(f1181,plain,
( sQ111_spl
| ~ m1_subset_1(sK2_skl,u2_conlat_1(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1179]) ).
fof(f1182,plain,
( sQ5_spl
| ~ sQ83_spl
| ~ sQ111_spl
| ~ sQ110_spl
| ~ sQ109_spl
| ~ sQ108_spl
| sQ22_spl
| ~ sQ107_spl ),
inference(split_clause,[status(thm)],[f1163,f1167,f520,f1170,f1173,f1176,f1179,f972,f427]) ).
fof(f1183,plain,
( sQ111_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1181,f104]) ).
fof(f1184,plain,
sQ111_spl,
inference(contradiction_clause,[status(thm)],[f1183]) ).
fof(f1185,plain,
( sQ108_spl
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f1172,f172]) ).
fof(f1186,plain,
( sQ108_spl
| ~ sQ25_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f1185,f513,f569,f1170]) ).
fof(f1187,plain,
! [X0] :
( sQ4_spl
| ~ m1_conlat_1(X0,sK0_skl)
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl)
| ~ m1_subset_1(k8_funct_2(u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k5_conlat_2(sK0_skl),sK2_skl),X0) ),
inference(resolution,[status(thm)],[f426,f861]) ).
fof(f1189,definition,
! [X0] :
( sQ112_spl
<=> ( ~ m1_conlat_1(X0,sK0_skl)
| ~ m1_subset_1(k8_funct_2(u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k5_conlat_2(sK0_skl),sK2_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f1190,plain,
! [X0] :
( ~ sQ112_spl
| ~ m1_conlat_1(X0,sK0_skl)
| ~ m1_subset_1(k8_funct_2(u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k5_conlat_2(sK0_skl),sK2_skl),X0) ),
inference(component_clause,[status(thm)],[f1189]) ).
fof(f1192,plain,
( sQ4_spl
| ~ sQ25_spl
| sQ20_spl
| sQ112_spl ),
inference(split_clause,[status(thm)],[f1187,f1189,f513,f569,f424]) ).
fof(f1231,plain,
! [X0] :
( ~ sQ3_spl
| ~ m1_conlat_1(X0,sK0_skl)
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl)
| ~ m1_subset_1(k8_funct_2(u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k5_conlat_2(sK0_skl),sK2_skl),X0) ),
inference(resolution,[status(thm)],[f422,f860]) ).
fof(f1233,plain,
( ~ sQ3_spl
| ~ sQ25_spl
| sQ20_spl
| sQ112_spl ),
inference(split_clause,[status(thm)],[f1231,f1189,f513,f569,f421]) ).
fof(f1235,plain,
! [X0] :
( ~ sQ83_spl
| sQ2_spl
| ~ m1_conlat_1(X0,sK0_skl)
| ~ m1_subset_1(k8_funct_2(u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k4_conlat_2(sK0_skl),sK1_skl),X0) ),
inference(resolution,[status(thm)],[f420,f973]) ).
fof(f1290,plain,
( sQ110_spl
| ~ m2_relset_1(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl))) ),
inference(resolution,[status(thm)],[f1178,f386]) ).
fof(f1291,plain,
( sQ109_spl
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f1175,f173]) ).
fof(f1292,plain,
( sQ109_spl
| ~ sQ25_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f1291,f513,f569,f1173]) ).
fof(f1293,plain,
( sQ110_spl
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f1290,f174]) ).
fof(f1295,plain,
( sQ110_spl
| ~ sQ25_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f1293,f513,f569,f1176]) ).
fof(f1344,plain,
( ~ sQ112_spl
| ~ m1_subset_1(sK2_skl,u2_conlat_1(sK0_skl))
| ~ m1_relset_1(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)))
| ~ v1_funct_2(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)))
| ~ v1_funct_1(k5_conlat_2(sK0_skl))
| v1_xboole_0(u2_conlat_1(sK0_skl))
| ~ m1_conlat_1(u1_struct_0(k11_conlat_1(sK0_skl)),sK0_skl) ),
inference(resolution,[status(thm)],[f1190,f180]) ).
fof(f1348,plain,
( ~ sQ112_spl
| ~ sQ111_spl
| ~ sQ110_spl
| ~ sQ109_spl
| ~ sQ108_spl
| sQ22_spl
| ~ sQ107_spl ),
inference(split_clause,[status(thm)],[f1344,f1167,f520,f1170,f1173,f1176,f1179,f1189]) ).
fof(f1383,definition,
( sQ137_spl
<=> v3_struct_0(sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f1384,plain,
( ~ sQ137_spl
| v3_struct_0(sK15_skl) ),
inference(component_clause,[status(thm)],[f1383]) ).
fof(f1438,plain,
( ~ sQ83_spl
| sQ2_spl
| ~ m1_subset_1(sK1_skl,u1_conlat_1(sK0_skl))
| ~ m1_relset_1(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)))
| ~ v1_funct_2(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)))
| ~ v1_funct_1(k4_conlat_2(sK0_skl))
| v1_xboole_0(u1_conlat_1(sK0_skl))
| ~ m1_conlat_1(u1_struct_0(k11_conlat_1(sK0_skl)),sK0_skl) ),
inference(resolution,[status(thm)],[f1235,f180]) ).
fof(f1442,definition,
( sQ144_spl
<=> v1_funct_1(k4_conlat_2(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ144_spl])],[split_symbol_definition]) ).
fof(f1444,plain,
( sQ144_spl
| ~ v1_funct_1(k4_conlat_2(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1442]) ).
fof(f1445,definition,
( sQ145_spl
<=> v1_funct_2(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f1447,plain,
( sQ145_spl
| ~ v1_funct_2(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl))) ),
inference(component_clause,[status(thm)],[f1445]) ).
fof(f1448,definition,
( sQ146_spl
<=> m1_relset_1(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).
fof(f1450,plain,
( sQ146_spl
| ~ m1_relset_1(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl))) ),
inference(component_clause,[status(thm)],[f1448]) ).
fof(f1451,definition,
( sQ147_spl
<=> m1_subset_1(sK1_skl,u1_conlat_1(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition]) ).
fof(f1453,plain,
( sQ147_spl
| ~ m1_subset_1(sK1_skl,u1_conlat_1(sK0_skl)) ),
inference(component_clause,[status(thm)],[f1451]) ).
fof(f1454,plain,
( ~ sQ83_spl
| sQ2_spl
| ~ sQ147_spl
| ~ sQ146_spl
| ~ sQ145_spl
| ~ sQ144_spl
| sQ21_spl
| ~ sQ107_spl ),
inference(split_clause,[status(thm)],[f1438,f1167,f516,f1442,f1445,f1448,f1451,f418,f972]) ).
fof(f1455,plain,
( sQ147_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1453,f103]) ).
fof(f1456,plain,
sQ147_spl,
inference(contradiction_clause,[status(thm)],[f1455]) ).
fof(f1457,plain,
( sQ144_spl
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f1444,f168]) ).
fof(f1458,plain,
( sQ144_spl
| ~ sQ25_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f1457,f513,f569,f1442]) ).
fof(f1459,plain,
( sQ146_spl
| ~ m2_relset_1(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl))) ),
inference(resolution,[status(thm)],[f1450,f386]) ).
fof(f1460,plain,
( sQ145_spl
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f1447,f169]) ).
fof(f1461,plain,
( sQ145_spl
| ~ sQ25_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f1460,f513,f569,f1445]) ).
fof(f1462,plain,
( sQ146_spl
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl) ),
inference(resolution,[status(thm)],[f1459,f170]) ).
fof(f1464,plain,
( sQ146_spl
| ~ sQ25_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f1462,f513,f569,f1448]) ).
fof(f1472,plain,
! [X0] :
( sQ1_spl
| ~ m1_conlat_1(X0,sK0_skl)
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl)
| ~ m1_subset_1(k8_funct_2(u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k4_conlat_2(sK0_skl),sK1_skl),X0) ),
inference(resolution,[status(thm)],[f417,f861]) ).
fof(f1474,definition,
! [X0] :
( sQ149_spl
<=> ( ~ m1_conlat_1(X0,sK0_skl)
| ~ m1_subset_1(k8_funct_2(u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k4_conlat_2(sK0_skl),sK1_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition]) ).
fof(f1475,plain,
! [X0] :
( ~ sQ149_spl
| ~ m1_conlat_1(X0,sK0_skl)
| ~ m1_subset_1(k8_funct_2(u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k4_conlat_2(sK0_skl),sK1_skl),X0) ),
inference(component_clause,[status(thm)],[f1474]) ).
fof(f1477,plain,
( sQ1_spl
| ~ sQ25_spl
| sQ20_spl
| sQ149_spl ),
inference(split_clause,[status(thm)],[f1472,f1474,f513,f569,f415]) ).
fof(f1482,plain,
! [X0] :
( ~ sQ0_spl
| ~ m1_conlat_1(X0,sK0_skl)
| ~ l2_conlat_1(sK0_skl)
| v3_conlat_1(sK0_skl)
| ~ m1_subset_1(k8_funct_2(u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)),k4_conlat_2(sK0_skl),sK1_skl),X0) ),
inference(resolution,[status(thm)],[f413,f860]) ).
fof(f1484,plain,
( ~ sQ0_spl
| ~ sQ25_spl
| sQ20_spl
| sQ149_spl ),
inference(split_clause,[status(thm)],[f1482,f1474,f513,f569,f412]) ).
fof(f1616,plain,
( ~ sQ149_spl
| ~ m1_subset_1(sK1_skl,u1_conlat_1(sK0_skl))
| ~ m1_relset_1(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)))
| ~ v1_funct_2(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)))
| ~ v1_funct_1(k4_conlat_2(sK0_skl))
| v1_xboole_0(u1_conlat_1(sK0_skl))
| ~ m1_conlat_1(u1_struct_0(k11_conlat_1(sK0_skl)),sK0_skl) ),
inference(resolution,[status(thm)],[f1475,f180]) ).
fof(f1620,plain,
( ~ sQ149_spl
| ~ sQ147_spl
| ~ sQ146_spl
| ~ sQ145_spl
| ~ sQ144_spl
| sQ21_spl
| ~ sQ107_spl ),
inference(split_clause,[status(thm)],[f1616,f1167,f516,f1442,f1445,f1448,f1451,f1474]) ).
fof(f1638,definition,
! [X0] :
( sQ172_spl
<=> ~ m1_subset_1(X0,sK3_skl(k1_zfmisc_1(k1_xboole_0),sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition]) ).
fof(f1639,plain,
! [X0] :
( ~ sQ172_spl
| ~ m1_subset_1(X0,sK3_skl(k1_zfmisc_1(k1_xboole_0),sK0_skl)) ),
inference(component_clause,[status(thm)],[f1638]) ).
fof(f1677,plain,
! [X0,X1,X2,X3] :
( ~ sQ31_spl
| ~ sQ70_spl
| k7_conlat_1(sK0_skl) = X1
| g3_lattices(k7_conlat_1(sK0_skl),X0,k9_conlat_1(sK0_skl)) != g3_lattices(X1,X2,X3)
| ~ m1_relset_1(k9_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k7_conlat_1(sK0_skl))
| ~ v1_funct_1(k9_conlat_1(sK0_skl))
| ~ m1_relset_1(X0,k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k7_conlat_1(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k7_conlat_1(sK0_skl))
| ~ v1_funct_1(X0) ),
inference(resolution,[status(thm)],[f305,f955]) ).
fof(f1713,definition,
! [X0,X1,X2,X3] :
( sQ181_spl
<=> ( k7_conlat_1(sK0_skl) = X1
| g3_lattices(k7_conlat_1(sK0_skl),X0,k9_conlat_1(sK0_skl)) != g3_lattices(X1,X2,X3)
| ~ m1_relset_1(X0,k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k7_conlat_1(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k7_conlat_1(sK0_skl))
| ~ v1_funct_1(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition]) ).
fof(f1714,plain,
! [X0,X1,X2,X3] :
( ~ sQ181_spl
| k7_conlat_1(sK0_skl) = X1
| g3_lattices(k7_conlat_1(sK0_skl),X0,k9_conlat_1(sK0_skl)) != g3_lattices(X1,X2,X3)
| ~ m1_relset_1(X0,k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k7_conlat_1(sK0_skl))
| ~ v1_funct_2(X0,k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k7_conlat_1(sK0_skl))
| ~ v1_funct_1(X0) ),
inference(component_clause,[status(thm)],[f1713]) ).
fof(f1716,plain,
( ~ sQ31_spl
| ~ sQ70_spl
| ~ sQ81_spl
| ~ sQ30_spl
| sQ181_spl ),
inference(split_clause,[status(thm)],[f1677,f1713,f590,f940,f863,f593]) ).
fof(f1857,plain,
( ~ sQ172_spl
| $false ),
inference(resolution,[status(thm)],[f1639,f227]) ).
fof(f1860,plain,
~ sQ172_spl,
inference(contradiction_clause,[status(thm)],[f1857]) ).
fof(f1980,definition,
( sQ210_spl
<=> v3_struct_0(sK26_skl) ),
introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition]) ).
fof(f1981,plain,
( ~ sQ210_spl
| v3_struct_0(sK26_skl) ),
inference(component_clause,[status(thm)],[f1980]) ).
fof(f2046,definition,
( sQ224_spl
<=> v3_struct_0(sK29_skl) ),
introduced(definition,[new_symbols(definition,[sQ224_spl])],[split_symbol_definition]) ).
fof(f2047,plain,
( ~ sQ224_spl
| v3_struct_0(sK29_skl) ),
inference(component_clause,[status(thm)],[f2046]) ).
fof(f2242,plain,
! [X0,X1,X2] :
( ~ sQ28_spl
| ~ sQ70_spl
| ~ sQ181_spl
| k7_conlat_1(sK0_skl) = X0
| g3_lattices(k7_conlat_1(sK0_skl),k10_conlat_1(sK0_skl),k9_conlat_1(sK0_skl)) != g3_lattices(X0,X1,X2)
| ~ m1_relset_1(k10_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k7_conlat_1(sK0_skl))
| ~ v1_funct_1(k10_conlat_1(sK0_skl)) ),
inference(resolution,[status(thm)],[f1714,f966]) ).
fof(f2245,definition,
! [X0,X1,X2] :
( sQ243_spl
<=> ( k7_conlat_1(sK0_skl) = X0
| g3_lattices(k7_conlat_1(sK0_skl),k10_conlat_1(sK0_skl),k9_conlat_1(sK0_skl)) != g3_lattices(X0,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[sQ243_spl])],[split_symbol_definition]) ).
fof(f2246,plain,
! [X0,X1,X2] :
( ~ sQ243_spl
| k7_conlat_1(sK0_skl) = X0
| g3_lattices(k7_conlat_1(sK0_skl),k10_conlat_1(sK0_skl),k9_conlat_1(sK0_skl)) != g3_lattices(X0,X1,X2) ),
inference(component_clause,[status(thm)],[f2245]) ).
fof(f2248,plain,
( ~ sQ28_spl
| ~ sQ70_spl
| ~ sQ181_spl
| sQ243_spl
| ~ sQ79_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f2242,f581,f934,f2245,f1713,f863,f584]) ).
fof(f2249,definition,
( sQ244_spl
<=> v1_funct_1(sK17_skl(k7_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ244_spl])],[split_symbol_definition]) ).
fof(f2251,plain,
( sQ244_spl
| ~ v1_funct_1(sK17_skl(k7_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f2249]) ).
fof(f2252,definition,
( sQ245_spl
<=> m1_relset_1(sK17_skl(k7_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl))),k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k7_conlat_1(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ245_spl])],[split_symbol_definition]) ).
fof(f2254,plain,
( sQ245_spl
| ~ m1_relset_1(sK17_skl(k7_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl))),k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k7_conlat_1(sK0_skl)) ),
inference(component_clause,[status(thm)],[f2252]) ).
fof(f2259,plain,
! [X0,X1,X2] :
( ~ sQ243_spl
| ~ sQ26_spl
| ~ sQ70_spl
| k7_conlat_1(sK0_skl) = X0
| k11_conlat_1(sK0_skl) != g3_lattices(X0,X1,X2) ),
inference(forward_demodulation,[status(thm)],[f928,f2246]) ).
fof(f2260,plain,
( sQ245_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2254,f328]) ).
fof(f2261,plain,
sQ245_spl,
inference(contradiction_clause,[status(thm)],[f2260]) ).
fof(f2262,plain,
( sQ244_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2251,f330]) ).
fof(f2263,plain,
sQ244_spl,
inference(contradiction_clause,[status(thm)],[f2262]) ).
fof(f2264,plain,
( ~ sQ35_spl
| ~ sQ243_spl
| ~ sQ26_spl
| ~ sQ70_spl
| k7_conlat_1(sK0_skl) = u1_struct_0(k11_conlat_1(sK0_skl)) ),
inference(resolution,[status(thm)],[f2259,f613]) ).
fof(f2300,definition,
( sQ255_spl
<=> k11_conlat_1(sK0_skl) = k11_conlat_1(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ255_spl])],[split_symbol_definition]) ).
fof(f2302,plain,
( sQ255_spl
| k11_conlat_1(sK0_skl) != k11_conlat_1(sK0_skl) ),
inference(component_clause,[status(thm)],[f2300]) ).
fof(f2311,plain,
( sQ255_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f2302]) ).
fof(f2312,plain,
sQ255_spl,
inference(contradiction_clause,[status(thm)],[f2311]) ).
fof(f2346,definition,
( sQ258_spl
<=> v7_lattices(sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition]) ).
fof(f2348,plain,
( sQ258_spl
| ~ v7_lattices(sK15_skl) ),
inference(component_clause,[status(thm)],[f2346]) ).
fof(f2368,definition,
( sQ264_spl
<=> v6_lattices(sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ264_spl])],[split_symbol_definition]) ).
fof(f2370,plain,
( sQ264_spl
| ~ v6_lattices(sK15_skl) ),
inference(component_clause,[status(thm)],[f2368]) ).
fof(f2382,definition,
( sQ267_spl
<=> v5_lattices(sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ267_spl])],[split_symbol_definition]) ).
fof(f2384,plain,
( sQ267_spl
| ~ v5_lattices(sK15_skl) ),
inference(component_clause,[status(thm)],[f2382]) ).
fof(f2404,definition,
( sQ273_spl
<=> v4_lattices(sK15_skl) ),
introduced(definition,[new_symbols(definition,[sQ273_spl])],[split_symbol_definition]) ).
fof(f2406,plain,
( sQ273_spl
| ~ v4_lattices(sK15_skl) ),
inference(component_clause,[status(thm)],[f2404]) ).
fof(f2463,plain,
( sQ273_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2406,f312]) ).
fof(f2464,plain,
sQ273_spl,
inference(contradiction_clause,[status(thm)],[f2463]) ).
fof(f2465,plain,
( sQ267_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2384,f313]) ).
fof(f2466,plain,
sQ267_spl,
inference(contradiction_clause,[status(thm)],[f2465]) ).
fof(f2467,plain,
( sQ264_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2370,f314]) ).
fof(f2468,plain,
sQ264_spl,
inference(contradiction_clause,[status(thm)],[f2467]) ).
fof(f2469,plain,
( sQ258_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2348,f315]) ).
fof(f2470,plain,
sQ258_spl,
inference(contradiction_clause,[status(thm)],[f2469]) ).
fof(f2507,plain,
( ~ sQ137_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1384,f310]) ).
fof(f2508,plain,
~ sQ137_spl,
inference(contradiction_clause,[status(thm)],[f2507]) ).
fof(f3000,plain,
( ~ sQ210_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1981,f359]) ).
fof(f3001,plain,
~ sQ210_spl,
inference(contradiction_clause,[status(thm)],[f3000]) ).
fof(f3102,definition,
( sQ369_spl
<=> v7_lattices(sK29_skl) ),
introduced(definition,[new_symbols(definition,[sQ369_spl])],[split_symbol_definition]) ).
fof(f3104,plain,
( sQ369_spl
| ~ v7_lattices(sK29_skl) ),
inference(component_clause,[status(thm)],[f3102]) ).
fof(f3124,definition,
( sQ375_spl
<=> v6_lattices(sK29_skl) ),
introduced(definition,[new_symbols(definition,[sQ375_spl])],[split_symbol_definition]) ).
fof(f3126,plain,
( sQ375_spl
| ~ v6_lattices(sK29_skl) ),
inference(component_clause,[status(thm)],[f3124]) ).
fof(f3138,definition,
( sQ378_spl
<=> v5_lattices(sK29_skl) ),
introduced(definition,[new_symbols(definition,[sQ378_spl])],[split_symbol_definition]) ).
fof(f3140,plain,
( sQ378_spl
| ~ v5_lattices(sK29_skl) ),
inference(component_clause,[status(thm)],[f3138]) ).
fof(f3160,definition,
( sQ384_spl
<=> v4_lattices(sK29_skl) ),
introduced(definition,[new_symbols(definition,[sQ384_spl])],[split_symbol_definition]) ).
fof(f3162,plain,
( sQ384_spl
| ~ v4_lattices(sK29_skl) ),
inference(component_clause,[status(thm)],[f3160]) ).
fof(f3219,plain,
( sQ384_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3162,f373]) ).
fof(f3220,plain,
sQ384_spl,
inference(contradiction_clause,[status(thm)],[f3219]) ).
fof(f3221,plain,
( sQ378_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3140,f374]) ).
fof(f3222,plain,
sQ378_spl,
inference(contradiction_clause,[status(thm)],[f3221]) ).
fof(f3223,plain,
( sQ375_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3126,f375]) ).
fof(f3224,plain,
sQ375_spl,
inference(contradiction_clause,[status(thm)],[f3223]) ).
fof(f3225,plain,
( sQ369_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3104,f376]) ).
fof(f3226,plain,
sQ369_spl,
inference(contradiction_clause,[status(thm)],[f3225]) ).
fof(f3263,plain,
( ~ sQ224_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2047,f371]) ).
fof(f3264,plain,
~ sQ224_spl,
inference(contradiction_clause,[status(thm)],[f3263]) ).
fof(f3316,plain,
( sQ107_spl
| ~ sQ35_spl
| ~ sQ243_spl
| ~ sQ26_spl
| ~ sQ70_spl
| ~ m1_conlat_1(k7_conlat_1(sK0_skl),sK0_skl) ),
inference(backward_demodulation,[status(thm)],[f2264,f1169]) ).
fof(f3360,plain,
( sQ107_spl
| ~ sQ35_spl
| ~ sQ243_spl
| ~ sQ26_spl
| ~ sQ70_spl
| ~ sQ71_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3316,f880]) ).
fof(f3361,plain,
( sQ107_spl
| ~ sQ35_spl
| ~ sQ243_spl
| ~ sQ26_spl
| ~ sQ70_spl
| ~ sQ71_spl ),
inference(contradiction_clause,[status(thm)],[f3360]) ).
fof(f3362,plain,
$false,
inference(sat_refutation,[status(thm)],[f430,f519,f523,f525,f575,f577,f608,f610,f615,f643,f656,f658,f761,f792,f800,f866,f882,f975,f1062,f1066,f1182,f1184,f1186,f1192,f1233,f1292,f1295,f1348,f1454,f1456,f1458,f1461,f1464,f1477,f1484,f1620,f1716,f1860,f2248,f2261,f2263,f2312,f2464,f2466,f2468,f2470,f2508,f3001,f3220,f3222,f3224,f3226,f3264,f3361]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT343+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n004.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Sun Sep 20 23:43:20 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.46 % Drodi V4.1.1
% 2.52/0.83 % Refutation found
% 2.52/0.83 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.52/0.83 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.52/0.86 % Elapsed time: 0.400545 seconds
% 2.52/0.86 % CPU time: 2.790444 seconds
% 2.52/0.86 % Total memory used: 129.538 MB
% 2.52/0.86 % Net memory used: 127.907 MB
%------------------------------------------------------------------------------