%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT343+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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:03:46 PM UTC 2026
% Result : Theorem 62.82s 8.47s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT343+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n013.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Sun Sep 20 23:43:20 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.46 % Drodi V4.1.1
% 62.82/8.47 % Refutation found
% 62.82/8.47 % SZS status Theorem for theBenchmark: Theorem is valid
% 62.82/8.47 % SZS output start CNFRefutation for theBenchmark
% 62.82/8.47 fof(f1,conjecture,(
% 62.82/8.47 (! [A] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A) )=> (! [B] :( m1_subset_1(B,u1_conlat_1(A))=> (! [C] :( m1_subset_1(C,u2_conlat_1(A))=> ( ~ v7_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)& l3_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(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)& l3_conlat_1(k8_funct_2(u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k5_conlat_2(A),C),A) ) ) )) )) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f2,negated_conjecture,(
% 62.82/8.47 ~((! [A] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A) )=> (! [B] :( m1_subset_1(B,u1_conlat_1(A))=> (! [C] :( m1_subset_1(C,u2_conlat_1(A))=> ( ~ v7_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)& l3_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(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)& l3_conlat_1(k8_funct_2(u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k5_conlat_2(A),C),A) ) ) )) )) ))),
% 62.82/8.47 inference(negated_conjecture,[status(cth)],[f1])).
% 62.82/8.47 fof(f3,axiom,(
% 62.82/8.47 (! [A] :( l3_lattices(A)=> ( v3_lattices(A)=> A = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) ) ) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f5,axiom,(
% 62.82/8.47 (! [A,B,C] :( m1_relset_1(C,A,B)=> ( ( v1_funct_1(C)& v1_partfun1(C,A,B) )=> ( v1_funct_1(C)& v1_funct_2(C,A,B) ) ) ) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f12,axiom,(
% 62.82/8.47 (! [A,B] :( ~ v1_xboole_0(B)=> (! [C] :( m1_relset_1(C,A,B)=> ( ( v1_funct_1(C)& v1_funct_2(C,A,B) )=> ( v1_funct_1(C)& v1_partfun1(C,A,B)& v1_funct_2(C,A,B) ) ) ) )) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f14,axiom,(
% 62.82/8.47 (! [A] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A) )=> (! [B] :( ~ v1_xboole_0(B)=> ( m1_conlat_1(B,A)<=> (! [C] :( r2_hidden(C,B)=> ( ~ v7_conlat_1(C,A)& v9_conlat_1(C,A)& l3_conlat_1(C,A) ) ) )) ) )) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f15,axiom,(
% 62.82/8.47 (! [A] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A) )=> k11_conlat_1(A) = g3_lattices(k8_conlat_1(A),k10_conlat_1(A),k9_conlat_1(A)) ) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f16,axiom,(
% 62.82/8.47 (! [A,B,C] :( ( v1_funct_1(B)& v1_funct_2(B,k2_zfmisc_1(A,A),A)& m1_relset_1(B,k2_zfmisc_1(A,A),A)& v1_funct_1(C)& v1_funct_2(C,k2_zfmisc_1(A,A),A)& m1_relset_1(C,k2_zfmisc_1(A,A),A) )=> ( v3_lattices(g3_lattices(A,B,C))& l3_lattices(g3_lattices(A,B,C)) ) ) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f17,axiom,(
% 62.82/8.47 (! [A] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A) )=> ( v1_funct_1(k10_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))& m2_relset_1(k10_conlat_1(A),k2_zfmisc_1(k8_conlat_1(A),k8_conlat_1(A)),k8_conlat_1(A)) ) ) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f18,axiom,(
% 62.82/8.47 (! [A] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A) )=> ( ~ v3_struct_0(k11_conlat_1(A))& v3_lattices(k11_conlat_1(A))& l3_lattices(k11_conlat_1(A)) ) ) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f23,axiom,(
% 62.82/8.47 (! [A] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A) )=> ( v1_funct_1(k4_conlat_2(A))& v1_funct_2(k4_conlat_2(A),u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)))& m2_relset_1(k4_conlat_2(A),u1_conlat_1(A),u1_struct_0(k11_conlat_1(A))) ) ) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f24,axiom,(
% 62.82/8.47 (! [A] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A) )=> ( v1_funct_1(k5_conlat_2(A))& v1_funct_2(k5_conlat_2(A),u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)))& m2_relset_1(k5_conlat_2(A),u2_conlat_1(A),u1_struct_0(k11_conlat_1(A))) ) ) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f25,axiom,(
% 62.82/8.47 (! [A] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A) )=> ~ v1_xboole_0(k7_conlat_1(A)) ) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f26,axiom,(
% 62.82/8.47 (! [A] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A) )=> m1_conlat_1(k8_conlat_1(A),A) ) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f27,axiom,(
% 62.82/8.47 (! [A,B,C,D] :( ( ~ v1_xboole_0(A)& v1_funct_1(C)& v1_funct_2(C,A,B)& m1_relset_1(C,A,B)& m1_subset_1(D,A) )=> m1_subset_1(k8_funct_2(A,B,C,D),B) ) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f28,axiom,(
% 62.82/8.47 (! [A] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A) )=> ( v1_funct_1(k9_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))& m2_relset_1(k9_conlat_1(A),k2_zfmisc_1(k8_conlat_1(A),k8_conlat_1(A)),k8_conlat_1(A)) ) ) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f30,axiom,(
% 62.82/8.47 (! [A] :( l1_lattices(A)=> l1_struct_0(A) ) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f32,axiom,(
% 62.82/8.47 (! [A] :( l2_conlat_1(A)=> l1_conlat_1(A) ) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f33,axiom,(
% 62.82/8.47 (! [A] :( l2_lattices(A)=> l1_struct_0(A) ) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f35,axiom,(
% 62.82/8.47 (! [A] :( l3_lattices(A)=> ( l1_lattices(A)& l2_lattices(A) ) ) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f36,axiom,(
% 62.82/8.47 (! [A] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A) )=> (! [B] :( m1_conlat_1(B,A)=> ~ v1_xboole_0(B) ) )) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f45,axiom,(
% 62.82/8.47 (? [A] : l1_conlat_1(A) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f49,axiom,(
% 62.82/8.47 (? [A] : l2_lattices(A) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f51,axiom,(
% 62.82/8.47 (? [A] : l3_lattices(A) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f56,axiom,(
% 62.82/8.47 (! [A] :( ( ~ v3_conlat_1(A)& l1_conlat_1(A) )=> ~ v1_xboole_0(u2_conlat_1(A)) ) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f59,axiom,(
% 62.82/8.47 (! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f61,axiom,(
% 62.82/8.47 (! [A] :( ( ~ v3_conlat_1(A)& l1_conlat_1(A) )=> ~ v1_xboole_0(u1_conlat_1(A)) ) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f71,axiom,(
% 62.82/8.47 (! [A,B,C] :( ( v1_funct_1(B)& v1_funct_2(B,k2_zfmisc_1(A,A),A)& m1_relset_1(B,k2_zfmisc_1(A,A),A)& v1_funct_1(C)& v1_funct_2(C,k2_zfmisc_1(A,A),A)& m1_relset_1(C,k2_zfmisc_1(A,A),A) )=> (! [D,E,F] :( g3_lattices(A,B,C) = g3_lattices(D,E,F)=> ( A = D& B = E& C = F ) ) )) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f72,axiom,(
% 62.82/8.47 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v3_lattices(A)& v4_lattices(A)& v5_lattices(A)& v6_lattices(A)& v7_lattices(A)& v8_lattices(A)& v9_lattices(A)& v10_lattices(A)& v13_lattices(A)& v14_lattices(A)& v15_lattices(A) ) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f74,axiom,(
% 62.82/8.47 (! [A,B] :(? [C] :( m1_relset_1(C,A,B)& v1_relat_1(C)& v1_funct_1(C)& v1_funct_2(C,A,B) ) ))),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f80,axiom,(
% 62.82/8.47 (? [A] :( l3_lattices(A)& v3_lattices(A) ) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f83,axiom,(
% 62.82/8.47 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v3_lattices(A) ) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f86,axiom,(
% 62.82/8.47 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v3_lattices(A)& v4_lattices(A)& v5_lattices(A)& v6_lattices(A)& v7_lattices(A)& v8_lattices(A)& v9_lattices(A)& v10_lattices(A) ) )),
% 62.82/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.47 fof(f87,axiom,(
% 62.82/8.47 (! [A] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A) )=> k8_conlat_1(A) = k7_conlat_1(A) ) )),
% 62.82/8.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.48 fof(f89,axiom,(
% 62.82/8.48 (! [A,B,C] :( m2_relset_1(C,A,B)<=> m1_relset_1(C,A,B) ) )),
% 62.82/8.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.48 fof(f92,axiom,(
% 62.82/8.48 (! [A,B] :( m1_subset_1(A,B)=> ( v1_xboole_0(B)| r2_hidden(A,B) ) ) )),
% 62.82/8.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.48 fof(f97,axiom,(
% 62.82/8.48 (! [A,B] :~ ( r2_hidden(A,B)& v1_xboole_0(B) ) )),
% 62.82/8.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 62.82/8.48 fof(f99,plain,(
% 62.82/8.48 (?[A]: ((~v3_conlat_1(A)&l2_conlat_1(A))&(?[B]: (m1_subset_1(B,u1_conlat_1(A))&(?[C]: (m1_subset_1(C,u2_conlat_1(A))&(((((v7_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))|~l3_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(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))|~l3_conlat_1(k8_funct_2(u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)),k5_conlat_2(A),C),A))))))))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 62.82/8.48 fof(f100,plain,(
% 62.82/8.48 ((~v3_conlat_1(sK0_skl)&l2_conlat_1(sK0_skl))&(m1_subset_1(sK1_skl,u1_conlat_1(sK0_skl))&(m1_subset_1(sK2_skl,u2_conlat_1(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)|~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))|~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))|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))|~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))|~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)))))),
% 62.82/8.48 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])).
% 62.82/8.48 fof(f101,plain,(
% 62.82/8.48 ~v3_conlat_1(sK0_skl)),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f100])).
% 62.82/8.48 fof(f102,plain,(
% 62.82/8.48 l2_conlat_1(sK0_skl)),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f100])).
% 62.82/8.48 fof(f103,plain,(
% 62.82/8.48 m1_subset_1(sK1_skl,u1_conlat_1(sK0_skl))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f100])).
% 62.82/8.48 fof(f104,plain,(
% 62.82/8.48 m1_subset_1(sK2_skl,u2_conlat_1(sK0_skl))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f100])).
% 62.82/8.48 fof(f105,plain,(
% 62.82/8.48 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)|~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)|~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)|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)|~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)|~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)),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f100])).
% 62.82/8.48 fof(f106,plain,(
% 62.82/8.48 ![A]: (~l3_lattices(A)|(~v3_lattices(A)|A=g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A))))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 62.82/8.48 fof(f107,plain,(
% 62.82/8.48 ![X0]: (~l3_lattices(X0)|~v3_lattices(X0)|X0=g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f106])).
% 62.82/8.48 fof(f110,plain,(
% 62.82/8.48 ![A,B,C]: (~m1_relset_1(C,A,B)|((~v1_funct_1(C)|~v1_partfun1(C,A,B))|(v1_funct_1(C)&v1_funct_2(C,A,B))))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 62.82/8.48 fof(f112,plain,(
% 62.82/8.48 ![X0,X1,X2]: (~m1_relset_1(X0,X1,X2)|~v1_funct_1(X0)|~v1_partfun1(X0,X1,X2)|v1_funct_2(X0,X1,X2))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f110])).
% 62.82/8.48 fof(f136,plain,(
% 62.82/8.48 ![A,B]: (v1_xboole_0(B)|(![C]: (~m1_relset_1(C,A,B)|((~v1_funct_1(C)|~v1_funct_2(C,A,B))|((v1_funct_1(C)&v1_partfun1(C,A,B))&v1_funct_2(C,A,B))))))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 62.82/8.48 fof(f137,plain,(
% 62.82/8.48 ![B]: (v1_xboole_0(B)|(![A,C]: (~m1_relset_1(C,A,B)|((~v1_funct_1(C)|~v1_funct_2(C,A,B))|((v1_funct_1(C)&v1_partfun1(C,A,B))&v1_funct_2(C,A,B))))))),
% 62.82/8.48 inference(miniscoping,[status(thm)],[f136])).
% 62.82/8.48 fof(f139,plain,(
% 62.82/8.48 ![X0,X1,X2]: (v1_xboole_0(X0)|~m1_relset_1(X1,X2,X0)|~v1_funct_1(X1)|~v1_funct_2(X1,X2,X0)|v1_partfun1(X1,X2,X0))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f137])).
% 62.82/8.48 fof(f146,plain,(
% 62.82/8.48 ![A]: ((v3_conlat_1(A)|~l2_conlat_1(A))|(![B]: (v1_xboole_0(B)|(m1_conlat_1(B,A)<=>(![C]: (~r2_hidden(C,B)|((~v7_conlat_1(C,A)&v9_conlat_1(C,A))&l3_conlat_1(C,A))))))))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 62.82/8.48 fof(f147,plain,(
% 62.82/8.48 ![A]: ((v3_conlat_1(A)|~l2_conlat_1(A))|(![B]: (v1_xboole_0(B)|((~m1_conlat_1(B,A)|(![C]: (~r2_hidden(C,B)|((~v7_conlat_1(C,A)&v9_conlat_1(C,A))&l3_conlat_1(C,A)))))&(m1_conlat_1(B,A)|(?[C]: (r2_hidden(C,B)&((v7_conlat_1(C,A)|~v9_conlat_1(C,A))|~l3_conlat_1(C,A)))))))))),
% 62.82/8.48 inference(NNF_transformation,[status(thm)],[f146])).
% 62.82/8.48 fof(f148,plain,(
% 62.82/8.48 ![A]: ((v3_conlat_1(A)|~l2_conlat_1(A))|(![B]: (v1_xboole_0(B)|((~m1_conlat_1(B,A)|(![C]: (~r2_hidden(C,B)|((~v7_conlat_1(C,A)&v9_conlat_1(C,A))&l3_conlat_1(C,A)))))&(m1_conlat_1(B,A)|(r2_hidden(sK3_skl(B,A),B)&((v7_conlat_1(sK3_skl(B,A),A)|~v9_conlat_1(sK3_skl(B,A),A))|~l3_conlat_1(sK3_skl(B,A),A))))))))),
% 62.82/8.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(C,sK3_skl(B,A))],[f147])).
% 62.82/8.48 fof(f149,plain,(
% 62.82/8.48 ![X0,X1,X2]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|v1_xboole_0(X1)|~m1_conlat_1(X1,X0)|~r2_hidden(X2,X1)|~v7_conlat_1(X2,X0))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f148])).
% 62.82/8.48 fof(f150,plain,(
% 62.82/8.48 ![X0,X1,X2]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|v1_xboole_0(X1)|~m1_conlat_1(X1,X0)|~r2_hidden(X2,X1)|v9_conlat_1(X2,X0))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f148])).
% 62.82/8.48 fof(f151,plain,(
% 62.82/8.48 ![X0,X1,X2]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|v1_xboole_0(X1)|~m1_conlat_1(X1,X0)|~r2_hidden(X2,X1)|l3_conlat_1(X2,X0))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f148])).
% 62.82/8.48 fof(f154,plain,(
% 62.82/8.48 ![A]: ((v3_conlat_1(A)|~l2_conlat_1(A))|k11_conlat_1(A)=g3_lattices(k8_conlat_1(A),k10_conlat_1(A),k9_conlat_1(A)))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 62.82/8.48 fof(f155,plain,(
% 62.82/8.48 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|k11_conlat_1(X0)=g3_lattices(k8_conlat_1(X0),k10_conlat_1(X0),k9_conlat_1(X0)))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f154])).
% 62.82/8.48 fof(f156,plain,(
% 62.82/8.48 ![A,B,C]: ((((((~v1_funct_1(B)|~v1_funct_2(B,k2_zfmisc_1(A,A),A))|~m1_relset_1(B,k2_zfmisc_1(A,A),A))|~v1_funct_1(C))|~v1_funct_2(C,k2_zfmisc_1(A,A),A))|~m1_relset_1(C,k2_zfmisc_1(A,A),A))|(v3_lattices(g3_lattices(A,B,C))&l3_lattices(g3_lattices(A,B,C))))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 62.82/8.48 fof(f157,plain,(
% 62.82/8.48 ![X0,X1,X2]: (~v1_funct_1(X0)|~v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)|~m1_relset_1(X0,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X2)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|v3_lattices(g3_lattices(X1,X0,X2)))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f156])).
% 62.82/8.48 fof(f159,plain,(
% 62.82/8.48 ![A]: ((v3_conlat_1(A)|~l2_conlat_1(A))|((v1_funct_1(k10_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)))&m2_relset_1(k10_conlat_1(A),k2_zfmisc_1(k8_conlat_1(A),k8_conlat_1(A)),k8_conlat_1(A))))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 62.82/8.48 fof(f160,plain,(
% 62.82/8.48 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|v1_funct_1(k10_conlat_1(X0)))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f159])).
% 62.82/8.48 fof(f161,plain,(
% 62.82/8.48 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|v1_funct_2(k10_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0)))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f159])).
% 62.82/8.48 fof(f162,plain,(
% 62.82/8.48 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|m2_relset_1(k10_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0)))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f159])).
% 62.82/8.48 fof(f163,plain,(
% 62.82/8.48 ![A]: ((v3_conlat_1(A)|~l2_conlat_1(A))|((~v3_struct_0(k11_conlat_1(A))&v3_lattices(k11_conlat_1(A)))&l3_lattices(k11_conlat_1(A))))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 62.82/8.48 fof(f166,plain,(
% 62.82/8.48 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|l3_lattices(k11_conlat_1(X0)))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f163])).
% 62.82/8.48 fof(f167,plain,(
% 62.82/8.48 ![A]: ((v3_conlat_1(A)|~l2_conlat_1(A))|((v1_funct_1(k4_conlat_2(A))&v1_funct_2(k4_conlat_2(A),u1_conlat_1(A),u1_struct_0(k11_conlat_1(A))))&m2_relset_1(k4_conlat_2(A),u1_conlat_1(A),u1_struct_0(k11_conlat_1(A)))))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 62.82/8.48 fof(f168,plain,(
% 62.82/8.48 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|v1_funct_1(k4_conlat_2(X0)))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f167])).
% 62.82/8.48 fof(f169,plain,(
% 62.82/8.48 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|v1_funct_2(k4_conlat_2(X0),u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0))))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f167])).
% 62.82/8.48 fof(f170,plain,(
% 62.82/8.48 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|m2_relset_1(k4_conlat_2(X0),u1_conlat_1(X0),u1_struct_0(k11_conlat_1(X0))))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f167])).
% 62.82/8.48 fof(f171,plain,(
% 62.82/8.48 ![A]: ((v3_conlat_1(A)|~l2_conlat_1(A))|((v1_funct_1(k5_conlat_2(A))&v1_funct_2(k5_conlat_2(A),u2_conlat_1(A),u1_struct_0(k11_conlat_1(A))))&m2_relset_1(k5_conlat_2(A),u2_conlat_1(A),u1_struct_0(k11_conlat_1(A)))))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 62.82/8.48 fof(f172,plain,(
% 62.82/8.48 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|v1_funct_1(k5_conlat_2(X0)))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f171])).
% 62.82/8.48 fof(f173,plain,(
% 62.82/8.48 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|v1_funct_2(k5_conlat_2(X0),u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0))))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f171])).
% 62.82/8.48 fof(f174,plain,(
% 62.82/8.48 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|m2_relset_1(k5_conlat_2(X0),u2_conlat_1(X0),u1_struct_0(k11_conlat_1(X0))))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f171])).
% 62.82/8.48 fof(f175,plain,(
% 62.82/8.48 ![A]: ((v3_conlat_1(A)|~l2_conlat_1(A))|~v1_xboole_0(k7_conlat_1(A)))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 62.82/8.48 fof(f176,plain,(
% 62.82/8.48 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|~v1_xboole_0(k7_conlat_1(X0)))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f175])).
% 62.82/8.48 fof(f177,plain,(
% 62.82/8.48 ![A]: ((v3_conlat_1(A)|~l2_conlat_1(A))|m1_conlat_1(k8_conlat_1(A),A))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 62.82/8.48 fof(f178,plain,(
% 62.82/8.48 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|m1_conlat_1(k8_conlat_1(X0),X0))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f177])).
% 62.82/8.48 fof(f179,plain,(
% 62.82/8.48 ![A,B,C,D]: (((((v1_xboole_0(A)|~v1_funct_1(C))|~v1_funct_2(C,A,B))|~m1_relset_1(C,A,B))|~m1_subset_1(D,A))|m1_subset_1(k8_funct_2(A,B,C,D),B))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 62.82/8.48 fof(f180,plain,(
% 62.82/8.48 ![X0,X1,X2,X3]: (v1_xboole_0(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,X0,X2)|~m1_relset_1(X1,X0,X2)|~m1_subset_1(X3,X0)|m1_subset_1(k8_funct_2(X0,X2,X1,X3),X2))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f179])).
% 62.82/8.48 fof(f181,plain,(
% 62.82/8.48 ![A]: ((v3_conlat_1(A)|~l2_conlat_1(A))|((v1_funct_1(k9_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)))&m2_relset_1(k9_conlat_1(A),k2_zfmisc_1(k8_conlat_1(A),k8_conlat_1(A)),k8_conlat_1(A))))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 62.82/8.48 fof(f182,plain,(
% 62.82/8.48 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|v1_funct_1(k9_conlat_1(X0)))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f181])).
% 62.82/8.48 fof(f183,plain,(
% 62.82/8.48 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|v1_funct_2(k9_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0)))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f181])).
% 62.82/8.48 fof(f184,plain,(
% 62.82/8.48 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|m2_relset_1(k9_conlat_1(X0),k2_zfmisc_1(k8_conlat_1(X0),k8_conlat_1(X0)),k8_conlat_1(X0)))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f181])).
% 62.82/8.48 fof(f185,plain,(
% 62.82/8.48 ![A]: (~l1_lattices(A)|l1_struct_0(A))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 62.82/8.48 fof(f186,plain,(
% 62.82/8.48 ![X0]: (~l1_lattices(X0)|l1_struct_0(X0))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f185])).
% 62.82/8.48 fof(f187,plain,(
% 62.82/8.48 ![A]: (~l2_conlat_1(A)|l1_conlat_1(A))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 62.82/8.48 fof(f188,plain,(
% 62.82/8.48 ![X0]: (~l2_conlat_1(X0)|l1_conlat_1(X0))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f187])).
% 62.82/8.48 fof(f189,plain,(
% 62.82/8.48 ![A]: (~l2_lattices(A)|l1_struct_0(A))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 62.82/8.48 fof(f190,plain,(
% 62.82/8.48 ![X0]: (~l2_lattices(X0)|l1_struct_0(X0))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f189])).
% 62.82/8.48 fof(f191,plain,(
% 62.82/8.48 ![A]: (~l3_lattices(A)|(l1_lattices(A)&l2_lattices(A)))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 62.82/8.48 fof(f192,plain,(
% 62.82/8.48 ![X0]: (~l3_lattices(X0)|l1_lattices(X0))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f191])).
% 62.82/8.48 fof(f193,plain,(
% 62.82/8.48 ![X0]: (~l3_lattices(X0)|l2_lattices(X0))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f191])).
% 62.82/8.48 fof(f194,plain,(
% 62.82/8.48 ![A]: ((v3_conlat_1(A)|~l2_conlat_1(A))|(![B]: (~m1_conlat_1(B,A)|~v1_xboole_0(B))))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 62.82/8.48 fof(f195,plain,(
% 62.82/8.48 ![X0,X1]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|~m1_conlat_1(X1,X0)|~v1_xboole_0(X1))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f194])).
% 62.82/8.48 fof(f206,plain,(
% 62.82/8.48 l1_conlat_1(sK4_skl)),
% 62.82/8.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(A,sK4_skl)],[f45])).
% 62.82/8.48 fof(f207,plain,(
% 62.82/8.48 l1_conlat_1(sK4_skl)),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f206])).
% 62.82/8.48 fof(f214,plain,(
% 62.82/8.48 l2_lattices(sK8_skl)),
% 62.82/8.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(A,sK8_skl)],[f49])).
% 62.82/8.48 fof(f215,plain,(
% 62.82/8.48 l2_lattices(sK8_skl)),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f214])).
% 62.82/8.48 fof(f219,plain,(
% 62.82/8.48 l3_lattices(sK10_skl)),
% 62.82/8.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(A,sK10_skl)],[f51])).
% 62.82/8.48 fof(f220,plain,(
% 62.82/8.48 l3_lattices(sK10_skl)),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f219])).
% 62.82/8.48 fof(f230,plain,(
% 62.82/8.48 ![A]: ((v3_conlat_1(A)|~l1_conlat_1(A))|~v1_xboole_0(u2_conlat_1(A)))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f56])).
% 62.82/8.48 fof(f231,plain,(
% 62.82/8.48 ![X0]: (v3_conlat_1(X0)|~l1_conlat_1(X0)|~v1_xboole_0(u2_conlat_1(X0)))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f230])).
% 62.82/8.48 fof(f248,plain,(
% 62.82/8.48 ![X0]: (~v1_xboole_0(k1_zfmisc_1(X0)))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f59])).
% 62.82/8.48 fof(f250,plain,(
% 62.82/8.48 ![A]: ((v3_conlat_1(A)|~l1_conlat_1(A))|~v1_xboole_0(u1_conlat_1(A)))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f61])).
% 62.82/8.48 fof(f251,plain,(
% 62.82/8.48 ![X0]: (v3_conlat_1(X0)|~l1_conlat_1(X0)|~v1_xboole_0(u1_conlat_1(X0)))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f250])).
% 62.82/8.48 fof(f304,plain,(
% 62.82/8.48 ![A,B,C]: ((((((~v1_funct_1(B)|~v1_funct_2(B,k2_zfmisc_1(A,A),A))|~m1_relset_1(B,k2_zfmisc_1(A,A),A))|~v1_funct_1(C))|~v1_funct_2(C,k2_zfmisc_1(A,A),A))|~m1_relset_1(C,k2_zfmisc_1(A,A),A))|(![D,E,F]: (~g3_lattices(A,B,C)=g3_lattices(D,E,F)|((A=D&B=E)&C=F))))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f71])).
% 62.82/8.48 fof(f305,plain,(
% 62.82/8.48 ![X0,X1,X2,X3,X4,X5]: (~v1_funct_1(X0)|~v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)|~m1_relset_1(X0,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X2)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~g3_lattices(X1,X0,X2)=g3_lattices(X3,X4,X5)|X1=X3)),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f304])).
% 62.82/8.48 fof(f308,plain,(
% 62.82/8.48 ((((((((((((l3_lattices(sK15_skl)&~v3_struct_0(sK15_skl))&v3_lattices(sK15_skl))&v4_lattices(sK15_skl))&v5_lattices(sK15_skl))&v6_lattices(sK15_skl))&v7_lattices(sK15_skl))&v8_lattices(sK15_skl))&v9_lattices(sK15_skl))&v10_lattices(sK15_skl))&v13_lattices(sK15_skl))&v14_lattices(sK15_skl))&v15_lattices(sK15_skl))),
% 62.82/8.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(A,sK15_skl)],[f72])).
% 62.82/8.48 fof(f309,plain,(
% 62.82/8.48 l3_lattices(sK15_skl)),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f308])).
% 62.82/8.48 fof(f310,plain,(
% 62.82/8.48 ~v3_struct_0(sK15_skl)),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f308])).
% 62.82/8.48 fof(f327,plain,(
% 62.82/8.48 ![A,B]: (((m1_relset_1(sK17_skl(B,A),A,B)&v1_relat_1(sK17_skl(B,A)))&v1_funct_1(sK17_skl(B,A)))&v1_funct_2(sK17_skl(B,A),A,B))),
% 62.82/8.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(C,sK17_skl(B,A))],[f74])).
% 62.82/8.48 fof(f328,plain,(
% 62.82/8.48 ![X0,X1]: (m1_relset_1(sK17_skl(X0,X1),X1,X0))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f327])).
% 62.82/8.48 fof(f330,plain,(
% 62.82/8.48 ![X0,X1]: (v1_funct_1(sK17_skl(X0,X1)))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f327])).
% 62.82/8.48 fof(f347,plain,(
% 62.82/8.48 (l3_lattices(sK23_skl)&v3_lattices(sK23_skl))),
% 62.82/8.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(A,sK23_skl)],[f80])).
% 62.82/8.48 fof(f348,plain,(
% 62.82/8.48 l3_lattices(sK23_skl)),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f347])).
% 62.82/8.48 fof(f357,plain,(
% 62.82/8.48 ((l3_lattices(sK26_skl)&~v3_struct_0(sK26_skl))&v3_lattices(sK26_skl))),
% 62.82/8.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl]),skolemize(A,sK26_skl)],[f83])).
% 62.82/8.48 fof(f358,plain,(
% 62.82/8.48 l3_lattices(sK26_skl)),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f357])).
% 62.82/8.48 fof(f359,plain,(
% 62.82/8.48 ~v3_struct_0(sK26_skl)),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f357])).
% 62.82/8.48 fof(f369,plain,(
% 62.82/8.48 (((((((((l3_lattices(sK29_skl)&~v3_struct_0(sK29_skl))&v3_lattices(sK29_skl))&v4_lattices(sK29_skl))&v5_lattices(sK29_skl))&v6_lattices(sK29_skl))&v7_lattices(sK29_skl))&v8_lattices(sK29_skl))&v9_lattices(sK29_skl))&v10_lattices(sK29_skl))),
% 62.82/8.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl]),skolemize(A,sK29_skl)],[f86])).
% 62.82/8.48 fof(f370,plain,(
% 62.82/8.48 l3_lattices(sK29_skl)),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f369])).
% 62.82/8.48 fof(f371,plain,(
% 62.82/8.48 ~v3_struct_0(sK29_skl)),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f369])).
% 62.82/8.48 fof(f380,plain,(
% 62.82/8.48 ![A]: ((v3_conlat_1(A)|~l2_conlat_1(A))|k8_conlat_1(A)=k7_conlat_1(A))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f87])).
% 62.82/8.48 fof(f381,plain,(
% 62.82/8.48 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|k8_conlat_1(X0)=k7_conlat_1(X0))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f380])).
% 62.82/8.48 fof(f384,plain,(
% 62.82/8.48 ![A,B,C]: ((~m2_relset_1(C,A,B)|m1_relset_1(C,A,B))&(m2_relset_1(C,A,B)|~m1_relset_1(C,A,B)))),
% 62.82/8.48 inference(NNF_transformation,[status(thm)],[f89])).
% 62.82/8.48 fof(f385,plain,(
% 62.82/8.48 (![A,B,C]: (~m2_relset_1(C,A,B)|m1_relset_1(C,A,B)))&(![A,B,C]: (m2_relset_1(C,A,B)|~m1_relset_1(C,A,B)))),
% 62.82/8.48 inference(miniscoping,[status(thm)],[f384])).
% 62.82/8.48 fof(f386,plain,(
% 62.82/8.48 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_relset_1(X0,X1,X2))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f385])).
% 62.82/8.48 fof(f392,plain,(
% 62.82/8.48 ![A,B]: (~m1_subset_1(A,B)|(v1_xboole_0(B)|r2_hidden(A,B)))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f92])).
% 62.82/8.48 fof(f393,plain,(
% 62.82/8.48 ![X0,X1]: (~m1_subset_1(X0,X1)|v1_xboole_0(X1)|r2_hidden(X0,X1))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f392])).
% 62.82/8.48 fof(f406,plain,(
% 62.82/8.48 ![A,B]: (~r2_hidden(A,B)|~v1_xboole_0(B))),
% 62.82/8.48 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 62.82/8.48 fof(f407,plain,(
% 62.82/8.48 ![B]: ((![A]: ~r2_hidden(A,B))|~v1_xboole_0(B))),
% 62.82/8.48 inference(miniscoping,[status(thm)],[f406])).
% 62.82/8.48 fof(f408,plain,(
% 62.82/8.48 ![X0,X1]: (~r2_hidden(X0,X1)|~v1_xboole_0(X1))),
% 62.82/8.48 inference(cnf_transformation,[status(thm)],[f407])).
% 62.82/8.48 fof(f412,definition,(
% 62.82/8.48 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))),
% 62.82/8.48 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 62.82/8.48 fof(f413,plain,(
% 62.82/8.48 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)|~sQ0_spl),
% 62.82/8.48 inference(component_clause,[status(thm)],[f412])).
% 62.82/8.48 fof(f415,definition,(
% 62.82/8.48 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))),
% 62.82/8.48 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 62.82/8.48 fof(f417,plain,(
% 62.82/8.48 ~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)|sQ1_spl),
% 62.82/8.48 inference(component_clause,[status(thm)],[f415])).
% 62.82/8.48 fof(f418,definition,(
% 62.82/8.48 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))),
% 62.82/8.48 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 62.82/8.48 fof(f420,plain,(
% 62.82/8.48 ~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)|sQ2_spl),
% 62.82/8.48 inference(component_clause,[status(thm)],[f418])).
% 62.82/8.48 fof(f421,definition,(
% 62.82/8.48 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))),
% 62.82/8.48 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 62.82/8.48 fof(f422,plain,(
% 62.82/8.48 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)|~sQ3_spl),
% 62.82/8.48 inference(component_clause,[status(thm)],[f421])).
% 62.82/8.48 fof(f424,definition,(
% 62.82/8.48 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))),
% 62.82/8.48 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 62.82/8.48 fof(f426,plain,(
% 62.82/8.48 ~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)|sQ4_spl),
% 62.82/8.48 inference(component_clause,[status(thm)],[f424])).
% 62.82/8.48 fof(f427,definition,(
% 62.82/8.48 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))),
% 62.82/8.48 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 62.82/8.48 fof(f429,plain,(
% 62.82/8.48 ~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)|sQ5_spl),
% 62.82/8.48 inference(component_clause,[status(thm)],[f427])).
% 62.82/8.48 fof(f430,plain,(
% 62.82/8.48 sQ0_spl|~sQ1_spl|~sQ2_spl|sQ3_spl|~sQ4_spl|~sQ5_spl),
% 62.82/8.48 inference(split_clause,[status(thm)],[f105,f412,f415,f418,f421,f424,f427])).
% 62.82/8.48 fof(f477,plain,(
% 62.82/8.48 l1_conlat_1(sK0_skl)),
% 62.82/8.48 inference(resolution,[status(thm)],[f188,f102])).
% 62.82/8.48 fof(f478,plain,(
% 62.82/8.48 l1_lattices(sK29_skl)),
% 62.82/8.48 inference(resolution,[status(thm)],[f192,f370])).
% 62.82/8.48 fof(f479,plain,(
% 62.82/8.48 l1_lattices(sK26_skl)),
% 62.82/8.48 inference(resolution,[status(thm)],[f192,f358])).
% 62.82/8.48 fof(f480,plain,(
% 62.82/8.48 l1_lattices(sK23_skl)),
% 62.82/8.48 inference(resolution,[status(thm)],[f192,f348])).
% 62.82/8.48 fof(f481,plain,(
% 62.82/8.48 l1_lattices(sK15_skl)),
% 62.82/8.48 inference(resolution,[status(thm)],[f192,f309])).
% 62.82/8.48 fof(f482,plain,(
% 62.82/8.48 l1_lattices(sK10_skl)),
% 62.82/8.48 inference(resolution,[status(thm)],[f192,f220])).
% 62.82/8.48 fof(f484,plain,(
% 62.82/8.48 l2_lattices(sK29_skl)),
% 62.82/8.48 inference(resolution,[status(thm)],[f193,f370])).
% 62.82/8.48 fof(f485,plain,(
% 62.82/8.48 l2_lattices(sK26_skl)),
% 62.82/8.48 inference(resolution,[status(thm)],[f193,f358])).
% 62.82/8.48 fof(f486,plain,(
% 62.82/8.48 l2_lattices(sK23_skl)),
% 62.82/8.48 inference(resolution,[status(thm)],[f193,f348])).
% 62.82/8.48 fof(f487,plain,(
% 62.82/8.48 l2_lattices(sK15_skl)),
% 62.82/8.48 inference(resolution,[status(thm)],[f193,f309])).
% 62.82/8.48 fof(f488,plain,(
% 62.82/8.48 l2_lattices(sK10_skl)),
% 62.82/8.48 inference(resolution,[status(thm)],[f193,f220])).
% 62.82/8.48 fof(f495,plain,(
% 62.82/8.48 ![X0,X1,X2]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|~m1_conlat_1(X1,X0)|~r2_hidden(X2,X1)|l3_conlat_1(X2,X0))),
% 62.82/8.48 inference(backward_subsumption_resolution,[status(thm)],[f151,f408])).
% 62.82/8.48 fof(f496,plain,(
% 62.82/8.48 ![X0,X1,X2]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|~m1_conlat_1(X1,X0)|~r2_hidden(X2,X1)|v9_conlat_1(X2,X0))),
% 62.82/8.48 inference(backward_subsumption_resolution,[status(thm)],[f150,f408])).
% 62.82/8.48 fof(f497,plain,(
% 62.82/8.48 ![X0,X1,X2]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|~m1_conlat_1(X1,X0)|~r2_hidden(X2,X1)|~v7_conlat_1(X2,X0))),
% 62.82/8.48 inference(backward_subsumption_resolution,[status(thm)],[f149,f408])).
% 62.82/8.48 fof(f525,plain,(
% 62.82/8.48 ~l2_conlat_1(sK0_skl)|k8_conlat_1(sK0_skl)=k7_conlat_1(sK0_skl)),
% 62.82/8.48 inference(resolution,[status(thm)],[f381,f101])).
% 62.82/8.48 fof(f527,definition,(
% 62.82/8.48 sQ16_spl <=> (l2_conlat_1(sK0_skl))),
% 62.82/8.48 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 62.82/8.48 fof(f529,plain,(
% 62.82/8.48 ~l2_conlat_1(sK0_skl)|sQ16_spl),
% 62.82/8.48 inference(component_clause,[status(thm)],[f527])).
% 62.82/8.48 fof(f530,definition,(
% 62.82/8.48 sQ17_spl <=> (k8_conlat_1(sK0_skl)=k7_conlat_1(sK0_skl))),
% 62.82/8.48 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 62.82/8.48 fof(f531,plain,(
% 62.82/8.48 k8_conlat_1(sK0_skl)=k7_conlat_1(sK0_skl)|~sQ17_spl),
% 62.82/8.48 inference(component_clause,[status(thm)],[f530])).
% 62.82/8.48 fof(f533,plain,(
% 62.82/8.48 ~sQ16_spl|sQ17_spl),
% 62.82/8.48 inference(split_clause,[status(thm)],[f525,f527,f530])).
% 62.82/8.48 fof(f535,plain,(
% 62.82/8.48 $false|sQ16_spl),
% 62.82/8.48 inference(forward_subsumption_resolution,[status(thm)],[f529,f102])).
% 62.82/8.48 fof(f536,plain,(
% 62.82/8.48 sQ16_spl),
% 62.82/8.48 inference(contradiction_clause,[status(thm)],[f535])).
% 62.82/8.48 fof(f537,plain,(
% 62.82/8.48 v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)|m1_conlat_1(k7_conlat_1(sK0_skl),sK0_skl)|~sQ17_spl),
% 62.82/8.48 inference(paramodulation,[status(thm)],[f531,f178])).
% 62.82/8.48 fof(f538,definition,(
% 62.82/8.48 sQ18_spl <=> (v3_conlat_1(sK0_skl))),
% 62.82/8.48 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 62.82/8.48 fof(f539,plain,(
% 62.82/8.48 v3_conlat_1(sK0_skl)|~sQ18_spl),
% 62.82/8.48 inference(component_clause,[status(thm)],[f538])).
% 62.82/8.48 fof(f541,definition,(
% 62.82/8.48 sQ19_spl <=> (m1_conlat_1(k7_conlat_1(sK0_skl),sK0_skl))),
% 62.82/8.48 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 62.82/8.48 fof(f542,plain,(
% 62.82/8.48 m1_conlat_1(k7_conlat_1(sK0_skl),sK0_skl)|~sQ19_spl),
% 62.82/8.48 inference(component_clause,[status(thm)],[f541])).
% 62.82/8.48 fof(f544,plain,(
% 62.82/8.48 sQ18_spl|~sQ16_spl|sQ19_spl|~sQ17_spl),
% 62.82/8.48 inference(split_clause,[status(thm)],[f537,f538,f527,f541,f530])).
% 62.82/8.48 fof(f545,plain,(
% 62.82/8.48 $false|~sQ18_spl),
% 62.82/8.48 inference(forward_subsumption_resolution,[status(thm)],[f539,f101])).
% 62.82/8.48 fof(f546,plain,(
% 62.82/8.48 ~sQ18_spl),
% 62.82/8.48 inference(contradiction_clause,[status(thm)],[f545])).
% 62.82/8.48 fof(f771,plain,(
% 62.82/8.48 ~l2_conlat_1(sK0_skl)|k11_conlat_1(sK0_skl)=g3_lattices(k8_conlat_1(sK0_skl),k10_conlat_1(sK0_skl),k9_conlat_1(sK0_skl))),
% 62.82/8.48 inference(resolution,[status(thm)],[f155,f101])).
% 62.82/8.48 fof(f773,definition,(
% 62.82/8.48 sQ64_spl <=> (k11_conlat_1(sK0_skl)=g3_lattices(k8_conlat_1(sK0_skl),k10_conlat_1(sK0_skl),k9_conlat_1(sK0_skl)))),
% 62.82/8.48 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 62.82/8.48 fof(f774,plain,(
% 62.82/8.48 k11_conlat_1(sK0_skl)=g3_lattices(k8_conlat_1(sK0_skl),k10_conlat_1(sK0_skl),k9_conlat_1(sK0_skl))|~sQ64_spl),
% 62.82/8.49 inference(component_clause,[status(thm)],[f773])).
% 62.82/8.49 fof(f776,plain,(
% 62.82/8.49 ~sQ16_spl|sQ64_spl),
% 62.82/8.49 inference(split_clause,[status(thm)],[f771,f527,f773])).
% 62.82/8.49 fof(f778,plain,(
% 62.82/8.49 k11_conlat_1(sK0_skl)=g3_lattices(k7_conlat_1(sK0_skl),k10_conlat_1(sK0_skl),k9_conlat_1(sK0_skl))|~sQ17_spl|~sQ64_spl),
% 62.82/8.49 inference(forward_demodulation,[status(thm)],[f531,f774])).
% 62.82/8.49 fof(f795,plain,(
% 62.82/8.49 ~v1_funct_1(k10_conlat_1(sK0_skl))|~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))|~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(k9_conlat_1(sK0_skl))|~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))|~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))|v3_lattices(k11_conlat_1(sK0_skl))|~sQ17_spl|~sQ64_spl),
% 62.82/8.49 inference(paramodulation,[status(thm)],[f778,f157])).
% 62.82/8.49 fof(f796,definition,(
% 62.82/8.49 sQ66_spl <=> (v1_funct_1(k10_conlat_1(sK0_skl)))),
% 62.82/8.49 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 62.82/8.49 fof(f798,plain,(
% 62.82/8.49 ~v1_funct_1(k10_conlat_1(sK0_skl))|sQ66_spl),
% 62.82/8.49 inference(component_clause,[status(thm)],[f796])).
% 62.82/8.49 fof(f799,definition,(
% 62.82/8.49 sQ67_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)))),
% 62.82/8.49 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 62.82/8.49 fof(f801,plain,(
% 62.82/8.49 ~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))|sQ67_spl),
% 62.82/8.49 inference(component_clause,[status(thm)],[f799])).
% 62.82/8.49 fof(f802,definition,(
% 62.82/8.49 sQ68_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)))),
% 62.82/8.49 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 62.82/8.49 fof(f804,plain,(
% 62.82/8.49 ~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))|sQ68_spl),
% 62.82/8.49 inference(component_clause,[status(thm)],[f802])).
% 62.82/8.49 fof(f805,definition,(
% 62.82/8.49 sQ69_spl <=> (v1_funct_1(k9_conlat_1(sK0_skl)))),
% 62.82/8.49 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 62.82/8.49 fof(f806,plain,(
% 62.82/8.49 v1_funct_1(k9_conlat_1(sK0_skl))|~sQ69_spl),
% 62.82/8.49 inference(component_clause,[status(thm)],[f805])).
% 62.82/8.49 fof(f807,plain,(
% 62.82/8.49 ~v1_funct_1(k9_conlat_1(sK0_skl))|sQ69_spl),
% 62.82/8.49 inference(component_clause,[status(thm)],[f805])).
% 62.82/8.49 fof(f808,definition,(
% 62.82/8.49 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)))),
% 62.82/8.49 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 62.82/8.49 fof(f810,plain,(
% 62.82/8.49 ~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))|sQ70_spl),
% 62.82/8.49 inference(component_clause,[status(thm)],[f808])).
% 62.82/8.49 fof(f811,definition,(
% 62.82/8.49 sQ71_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)))),
% 62.82/8.49 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 62.82/8.49 fof(f812,plain,(
% 62.82/8.49 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))|~sQ71_spl),
% 62.82/8.49 inference(component_clause,[status(thm)],[f811])).
% 62.82/8.49 fof(f813,plain,(
% 62.82/8.49 ~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))|sQ71_spl),
% 62.82/8.49 inference(component_clause,[status(thm)],[f811])).
% 62.82/8.49 fof(f814,definition,(
% 62.82/8.49 sQ72_spl <=> (v3_lattices(k11_conlat_1(sK0_skl)))),
% 62.82/8.49 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 62.82/8.49 fof(f815,plain,(
% 62.82/8.49 v3_lattices(k11_conlat_1(sK0_skl))|~sQ72_spl),
% 62.82/8.49 inference(component_clause,[status(thm)],[f814])).
% 62.82/8.49 fof(f817,plain,(
% 62.82/8.49 ~sQ66_spl|~sQ67_spl|~sQ68_spl|~sQ69_spl|~sQ70_spl|~sQ71_spl|sQ72_spl|~sQ17_spl|~sQ64_spl),
% 62.82/8.49 inference(split_clause,[status(thm)],[f795,f796,f799,f802,f805,f808,f811,f814,f530,f773])).
% 62.82/8.49 fof(f818,plain,(
% 62.82/8.49 ~l3_lattices(k11_conlat_1(sK0_skl))|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)))|~sQ72_spl),
% 62.82/8.49 inference(resolution,[status(thm)],[f815,f107])).
% 62.82/8.49 fof(f819,definition,(
% 62.82/8.49 sQ73_spl <=> (l3_lattices(k11_conlat_1(sK0_skl)))),
% 62.82/8.49 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 62.82/8.49 fof(f822,definition,(
% 62.82/8.49 sQ74_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))))),
% 62.82/8.49 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 62.82/8.49 fof(f823,plain,(
% 62.82/8.49 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)))|~sQ74_spl),
% 62.82/8.49 inference(component_clause,[status(thm)],[f822])).
% 62.82/8.49 fof(f825,plain,(
% 62.82/8.49 ~sQ73_spl|sQ74_spl|~sQ72_spl),
% 62.82/8.49 inference(split_clause,[status(thm)],[f818,f819,f822,f814])).
% 62.82/8.49 fof(f841,plain,(
% 62.82/8.49 v3_conlat_1(sK0_skl)|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))),
% 62.82/8.49 inference(resolution,[status(thm)],[f161,f102])).
% 62.82/8.49 fof(f846,definition,(
% 62.82/8.49 sQ78_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)))),
% 62.82/8.49 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 62.82/8.49 fof(f847,plain,(
% 62.82/8.49 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))|~sQ78_spl),
% 62.82/8.49 inference(component_clause,[status(thm)],[f846])).
% 62.82/8.49 fof(f849,plain,(
% 62.82/8.49 sQ18_spl|sQ78_spl),
% 62.82/8.49 inference(split_clause,[status(thm)],[f841,f538,f846])).
% 62.82/8.49 fof(f850,plain,(
% 62.82/8.49 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))|~sQ17_spl|~sQ78_spl),
% 62.82/8.49 inference(forward_demodulation,[status(thm)],[f531,f847])).
% 62.82/8.49 fof(f851,plain,(
% 62.82/8.49 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))|~sQ17_spl|~sQ78_spl),
% 62.82/8.49 inference(forward_demodulation,[status(thm)],[f531,f850])).
% 62.82/8.49 fof(f852,plain,(
% 62.82/8.49 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))|~sQ17_spl|~sQ78_spl),
% 62.82/8.49 inference(forward_demodulation,[status(thm)],[f531,f851])).
% 62.82/8.49 fof(f854,plain,(
% 62.82/8.49 v3_conlat_1(sK0_skl)|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))),
% 62.82/8.49 inference(resolution,[status(thm)],[f162,f102])).
% 62.82/8.49 fof(f859,definition,(
% 62.82/8.49 sQ80_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)))),
% 62.82/8.49 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 62.82/8.49 fof(f860,plain,(
% 62.82/8.49 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))|~sQ80_spl),
% 62.82/8.49 inference(component_clause,[status(thm)],[f859])).
% 62.82/8.49 fof(f862,plain,(
% 62.82/8.49 sQ18_spl|sQ80_spl),
% 62.82/8.49 inference(split_clause,[status(thm)],[f854,f538,f859])).
% 62.82/8.49 fof(f863,plain,(
% 62.82/8.49 m2_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))|~sQ17_spl|~sQ80_spl),
% 62.82/8.49 inference(forward_demodulation,[status(thm)],[f531,f860])).
% 62.82/8.49 fof(f864,plain,(
% 62.82/8.49 m2_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))|~sQ17_spl|~sQ80_spl),
% 62.82/8.49 inference(forward_demodulation,[status(thm)],[f531,f863])).
% 62.82/8.49 fof(f865,plain,(
% 62.82/8.49 m2_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))|~sQ17_spl|~sQ80_spl),
% 62.82/8.49 inference(forward_demodulation,[status(thm)],[f531,f864])).
% 62.82/8.49 fof(f866,plain,(
% 62.82/8.49 v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)|sQ69_spl),
% 62.82/8.49 inference(resolution,[status(thm)],[f807,f182])).
% 62.82/8.49 fof(f867,plain,(
% 62.82/8.49 sQ18_spl|~sQ16_spl|sQ69_spl),
% 62.82/8.49 inference(split_clause,[status(thm)],[f866,f538,f527,f805])).
% 62.82/8.49 fof(f868,plain,(
% 62.82/8.49 v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)|sQ66_spl),
% 62.82/8.49 inference(resolution,[status(thm)],[f798,f160])).
% 62.82/8.49 fof(f869,plain,(
% 62.82/8.49 sQ18_spl|~sQ16_spl|sQ66_spl),
% 62.82/8.49 inference(split_clause,[status(thm)],[f868,f538,f527,f796])).
% 62.82/8.49 fof(f870,plain,(
% 62.82/8.49 ![X0,X1]: (v1_xboole_0(X0)|~m1_relset_1(k9_conlat_1(sK0_skl),X1,X0)|~v1_funct_2(k9_conlat_1(sK0_skl),X1,X0)|v1_partfun1(k9_conlat_1(sK0_skl),X1,X0)|~sQ69_spl)),
% 62.82/8.49 inference(resolution,[status(thm)],[f806,f139])).
% 62.82/8.49 fof(f877,plain,(
% 62.82/8.49 ~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))|sQ71_spl),
% 62.82/8.49 inference(resolution,[status(thm)],[f813,f386])).
% 62.82/8.49 fof(f879,definition,(
% 62.82/8.49 sQ82_spl <=> (v1_partfun1(k9_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k7_conlat_1(sK0_skl)))),
% 62.82/8.49 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 62.82/8.49 fof(f883,plain,(
% 62.82/8.49 ~m2_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))|sQ68_spl),
% 62.82/8.49 inference(resolution,[status(thm)],[f804,f386])).
% 62.82/8.49 fof(f884,plain,(
% 62.82/8.49 $false|~sQ17_spl|~sQ78_spl|sQ67_spl),
% 62.82/8.49 inference(forward_subsumption_resolution,[status(thm)],[f801,f852])).
% 62.82/8.49 fof(f885,plain,(
% 62.82/8.49 ~sQ17_spl|~sQ78_spl|sQ67_spl),
% 62.82/8.49 inference(contradiction_clause,[status(thm)],[f884])).
% 62.82/8.49 fof(f932,plain,(
% 62.82/8.49 l1_struct_0(sK10_skl)),
% 62.82/8.49 inference(resolution,[status(thm)],[f186,f482])).
% 62.82/8.49 fof(f933,plain,(
% 62.82/8.49 l1_struct_0(sK15_skl)),
% 62.82/8.49 inference(resolution,[status(thm)],[f186,f481])).
% 62.82/8.49 fof(f934,plain,(
% 62.82/8.49 l1_struct_0(sK23_skl)),
% 62.82/8.49 inference(resolution,[status(thm)],[f186,f480])).
% 62.82/8.49 fof(f935,plain,(
% 62.82/8.49 l1_struct_0(sK26_skl)),
% 62.82/8.49 inference(resolution,[status(thm)],[f186,f479])).
% 62.82/8.49 fof(f936,plain,(
% 62.82/8.49 l1_struct_0(sK29_skl)),
% 62.82/8.49 inference(resolution,[status(thm)],[f186,f478])).
% 62.82/8.49 fof(f950,plain,(
% 62.82/8.49 v3_conlat_1(sK0_skl)|l3_lattices(k11_conlat_1(sK0_skl))),
% 62.82/8.49 inference(resolution,[status(thm)],[f166,f102])).
% 62.82/8.49 fof(f955,plain,(
% 62.82/8.49 sQ18_spl|sQ73_spl),
% 62.82/8.49 inference(split_clause,[status(thm)],[f950,f538,f819])).
% 62.82/8.49 fof(f957,plain,(
% 62.82/8.49 v3_conlat_1(sK0_skl)|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))),
% 62.82/8.49 inference(resolution,[status(thm)],[f183,f102])).
% 62.82/8.49 fof(f962,definition,(
% 62.82/8.49 sQ93_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)))),
% 62.82/8.49 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 62.82/8.49 fof(f963,plain,(
% 62.82/8.49 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))|~sQ93_spl),
% 62.82/8.49 inference(component_clause,[status(thm)],[f962])).
% 62.82/8.49 fof(f965,plain,(
% 62.82/8.49 sQ18_spl|sQ93_spl),
% 62.82/8.49 inference(split_clause,[status(thm)],[f957,f538,f962])).
% 62.82/8.49 fof(f966,plain,(
% 62.82/8.49 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))|~sQ17_spl|~sQ93_spl),
% 62.82/8.49 inference(forward_demodulation,[status(thm)],[f531,f963])).
% 62.82/8.49 fof(f967,plain,(
% 62.82/8.49 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))|~sQ17_spl|~sQ93_spl),
% 62.82/8.49 inference(forward_demodulation,[status(thm)],[f531,f966])).
% 62.82/8.49 fof(f968,plain,(
% 62.82/8.49 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))|~sQ17_spl|~sQ93_spl),
% 62.82/8.49 inference(forward_demodulation,[status(thm)],[f531,f967])).
% 62.82/8.49 fof(f982,plain,(
% 62.82/8.49 l1_struct_0(sK8_skl)),
% 62.82/8.49 inference(resolution,[status(thm)],[f190,f215])).
% 62.82/8.49 fof(f993,plain,(
% 62.82/8.49 v3_conlat_1(sK0_skl)|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))),
% 62.82/8.49 inference(resolution,[status(thm)],[f184,f102])).
% 62.82/8.49 fof(f998,definition,(
% 62.82/8.49 sQ95_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)))),
% 62.82/8.49 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 62.82/8.49 fof(f999,plain,(
% 62.82/8.49 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))|~sQ95_spl),
% 62.82/8.49 inference(component_clause,[status(thm)],[f998])).
% 62.82/8.49 fof(f1001,plain,(
% 62.82/8.49 sQ18_spl|sQ95_spl),
% 62.82/8.49 inference(split_clause,[status(thm)],[f993,f538,f998])).
% 62.82/8.49 fof(f1002,plain,(
% 62.82/8.49 m2_relset_1(k9_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k8_conlat_1(sK0_skl)),k8_conlat_1(sK0_skl))|~sQ17_spl|~sQ95_spl),
% 62.82/8.49 inference(forward_demodulation,[status(thm)],[f531,f999])).
% 62.82/8.49 fof(f1003,plain,(
% 62.82/8.49 m2_relset_1(k9_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k8_conlat_1(sK0_skl))|~sQ17_spl|~sQ95_spl),
% 62.82/8.49 inference(forward_demodulation,[status(thm)],[f531,f1002])).
% 62.82/8.49 fof(f1004,plain,(
% 62.82/8.49 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))|~sQ17_spl|~sQ95_spl),
% 62.82/8.49 inference(forward_demodulation,[status(thm)],[f531,f1003])).
% 62.82/8.49 fof(f1005,plain,(
% 62.82/8.49 $false|sQ71_spl|~sQ17_spl|~sQ95_spl),
% 62.82/8.49 inference(forward_subsumption_resolution,[status(thm)],[f1004,f877])).
% 62.82/8.49 fof(f1006,plain,(
% 62.82/8.49 sQ71_spl|~sQ17_spl|~sQ95_spl),
% 62.82/8.49 inference(contradiction_clause,[status(thm)],[f1005])).
% 62.82/8.50 fof(f1014,plain,(
% 62.82/8.50 $false|~sQ17_spl|~sQ80_spl|sQ68_spl),
% 62.82/8.50 inference(forward_subsumption_resolution,[status(thm)],[f883,f865])).
% 62.82/8.50 fof(f1015,plain,(
% 62.82/8.50 ~sQ17_spl|~sQ80_spl|sQ68_spl),
% 62.82/8.50 inference(contradiction_clause,[status(thm)],[f1014])).
% 62.82/8.50 fof(f1016,plain,(
% 62.82/8.50 $false|~sQ17_spl|~sQ93_spl|sQ70_spl),
% 62.82/8.50 inference(forward_subsumption_resolution,[status(thm)],[f810,f968])).
% 62.82/8.50 fof(f1017,plain,(
% 62.82/8.50 ~sQ17_spl|~sQ93_spl|sQ70_spl),
% 62.82/8.50 inference(contradiction_clause,[status(thm)],[f1016])).
% 62.82/8.50 fof(f1051,plain,(
% 62.82/8.50 v1_xboole_0(k7_conlat_1(sK0_skl))|~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_partfun1(k9_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k7_conlat_1(sK0_skl))|~sQ69_spl|~sQ17_spl|~sQ93_spl),
% 62.82/8.50 inference(resolution,[status(thm)],[f870,f968])).
% 62.82/8.50 fof(f1053,definition,(
% 62.82/8.50 sQ103_spl <=> (v1_xboole_0(k7_conlat_1(sK0_skl)))),
% 62.82/8.50 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 62.82/8.50 fof(f1054,plain,(
% 62.82/8.50 v1_xboole_0(k7_conlat_1(sK0_skl))|~sQ103_spl),
% 62.82/8.50 inference(component_clause,[status(thm)],[f1053])).
% 62.82/8.50 fof(f1056,plain,(
% 62.82/8.50 sQ103_spl|~sQ71_spl|sQ82_spl|~sQ69_spl|~sQ17_spl|~sQ93_spl),
% 62.82/8.50 inference(split_clause,[status(thm)],[f1051,f1053,f811,f879,f805,f530,f962])).
% 62.82/8.50 fof(f1069,plain,(
% 62.82/8.50 v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)|~sQ103_spl),
% 62.82/8.50 inference(resolution,[status(thm)],[f1054,f176])).
% 62.82/8.50 fof(f1073,plain,(
% 62.82/8.50 sQ18_spl|~sQ16_spl|~sQ103_spl),
% 62.82/8.50 inference(split_clause,[status(thm)],[f1069,f538,f527,f1053])).
% 62.82/8.50 fof(f1390,plain,(
% 62.82/8.50 ![X0,X1,X2,X3]: (v1_xboole_0(X0)|r2_hidden(k8_funct_2(X1,X0,X2,X3),X0)|v1_xboole_0(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,X1,X0)|~m1_relset_1(X2,X1,X0)|~m1_subset_1(X3,X1))),
% 62.82/8.50 inference(resolution,[status(thm)],[f393,f180])).
% 62.82/8.50 fof(f1398,definition,(
% 62.82/8.50 sQ145_spl <=> (v1_xboole_0(u2_conlat_1(sK0_skl)))),
% 62.82/8.50 introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition])).
% 62.82/8.50 fof(f1399,plain,(
% 62.82/8.50 v1_xboole_0(u2_conlat_1(sK0_skl))|~sQ145_spl),
% 62.82/8.50 inference(component_clause,[status(thm)],[f1398])).
% 62.82/8.50 fof(f1405,definition,(
% 62.82/8.50 sQ147_spl <=> (v1_xboole_0(u1_conlat_1(sK0_skl)))),
% 62.82/8.50 introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition])).
% 62.82/8.50 fof(f1406,plain,(
% 62.82/8.50 v1_xboole_0(u1_conlat_1(sK0_skl))|~sQ147_spl),
% 62.82/8.50 inference(component_clause,[status(thm)],[f1405])).
% 62.82/8.50 fof(f1420,plain,(
% 62.82/8.50 v3_conlat_1(sK0_skl)|~l1_conlat_1(sK0_skl)|~sQ147_spl),
% 62.82/8.50 inference(resolution,[status(thm)],[f1406,f251])).
% 62.82/8.50 fof(f1425,definition,(
% 62.82/8.50 sQ149_spl <=> (l1_conlat_1(sK0_skl))),
% 62.82/8.50 introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition])).
% 62.82/8.50 fof(f1427,plain,(
% 62.82/8.50 ~l1_conlat_1(sK0_skl)|sQ149_spl),
% 62.82/8.50 inference(component_clause,[status(thm)],[f1425])).
% 62.82/8.50 fof(f1428,plain,(
% 62.82/8.50 sQ18_spl|~sQ149_spl|~sQ147_spl),
% 62.82/8.50 inference(split_clause,[status(thm)],[f1420,f538,f1425,f1405])).
% 62.82/8.50 fof(f1436,plain,(
% 62.82/8.50 $false|sQ149_spl),
% 62.82/8.50 inference(forward_subsumption_resolution,[status(thm)],[f1427,f477])).
% 62.82/8.50 fof(f1437,plain,(
% 62.82/8.50 sQ149_spl),
% 62.82/8.50 inference(contradiction_clause,[status(thm)],[f1436])).
% 62.82/8.50 fof(f1438,plain,(
% 62.82/8.50 v3_conlat_1(sK0_skl)|~l1_conlat_1(sK0_skl)|~sQ145_spl),
% 62.82/8.50 inference(resolution,[status(thm)],[f1399,f231])).
% 62.82/8.50 fof(f1443,plain,(
% 62.82/8.50 sQ18_spl|~sQ149_spl|~sQ145_spl),
% 62.82/8.50 inference(split_clause,[status(thm)],[f1438,f538,f1425,f1398])).
% 62.82/8.50 fof(f1464,plain,(
% 62.82/8.50 ![X0,X1,X2,X3,X4]: (v1_xboole_0(X0)|v1_xboole_0(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,X1,X0)|~m1_relset_1(X2,X1,X0)|~m1_subset_1(X3,X1)|v3_conlat_1(X4)|~l2_conlat_1(X4)|~m1_conlat_1(X0,X4)|~v7_conlat_1(k8_funct_2(X1,X0,X2,X3),X4))),
% 62.82/8.50 inference(resolution,[status(thm)],[f1390,f497])).
% 62.82/8.50 fof(f1465,plain,(
% 62.82/8.50 ![X0,X1,X2,X3,X4]: (v1_xboole_0(X0)|v1_xboole_0(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,X1,X0)|~m1_relset_1(X2,X1,X0)|~m1_subset_1(X3,X1)|v3_conlat_1(X4)|~l2_conlat_1(X4)|~m1_conlat_1(X0,X4)|v9_conlat_1(k8_funct_2(X1,X0,X2,X3),X4))),
% 62.82/8.50 inference(resolution,[status(thm)],[f1390,f496])).
% 62.82/8.50 fof(f1466,plain,(
% 62.82/8.50 ![X0,X1,X2,X3,X4]: (v1_xboole_0(X0)|v1_xboole_0(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,X1,X0)|~m1_relset_1(X2,X1,X0)|~m1_subset_1(X3,X1)|v3_conlat_1(X4)|~l2_conlat_1(X4)|~m1_conlat_1(X0,X4)|l3_conlat_1(k8_funct_2(X1,X0,X2,X3),X4))),
% 62.82/8.50 inference(resolution,[status(thm)],[f1390,f495])).
% 62.82/8.50 fof(f1469,plain,(
% 62.82/8.50 ![X0,X1,X2,X3,X4]: (v1_xboole_0(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,X0,X2)|~m1_relset_1(X1,X0,X2)|~m1_subset_1(X3,X0)|v3_conlat_1(X4)|~l2_conlat_1(X4)|~m1_conlat_1(X2,X4)|~v7_conlat_1(k8_funct_2(X0,X2,X1,X3),X4))),
% 62.82/8.50 inference(forward_subsumption_resolution,[status(thm)],[f1464,f195])).
% 62.82/8.50 fof(f1470,plain,(
% 62.82/8.50 ![X0,X1,X2,X3,X4]: (v1_xboole_0(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,X0,X2)|~m1_relset_1(X1,X0,X2)|~m1_subset_1(X3,X0)|v3_conlat_1(X4)|~l2_conlat_1(X4)|~m1_conlat_1(X2,X4)|v9_conlat_1(k8_funct_2(X0,X2,X1,X3),X4))),
% 62.82/8.50 inference(forward_subsumption_resolution,[status(thm)],[f1465,f195])).
% 62.82/8.50 fof(f1471,plain,(
% 62.82/8.50 ![X0,X1,X2,X3,X4]: (v1_xboole_0(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,X0,X2)|~m1_relset_1(X1,X0,X2)|~m1_subset_1(X3,X0)|v3_conlat_1(X4)|~l2_conlat_1(X4)|~m1_conlat_1(X2,X4)|l3_conlat_1(k8_funct_2(X0,X2,X1,X3),X4))),
% 62.82/8.50 inference(forward_subsumption_resolution,[status(thm)],[f1466,f195])).
% 62.82/8.50 fof(f1523,plain,(
% 62.82/8.50 ![X0,X1,X2,X3]: (v1_xboole_0(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,X0,X2)|~m1_relset_1(X1,X0,X2)|~m1_subset_1(X3,X0)|v3_conlat_1(sK0_skl)|~m1_conlat_1(X2,sK0_skl)|~v7_conlat_1(k8_funct_2(X0,X2,X1,X3),sK0_skl))),
% 62.82/8.50 inference(resolution,[status(thm)],[f1469,f102])).
% 62.82/8.50 fof(f1528,definition,(
% 62.82/8.50 ![X0,X1,X2,X3]: (sQ160_spl <=> (v1_xboole_0(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,X0,X2)|~m1_relset_1(X1,X0,X2)|~m1_subset_1(X3,X0)|~m1_conlat_1(X2,sK0_skl)|~v7_conlat_1(k8_funct_2(X0,X2,X1,X3),sK0_skl)))),
% 62.82/8.50 introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition])).
% 62.82/8.50 fof(f1529,plain,(
% 62.82/8.50 ![X0,X1,X2,X3]: (v1_xboole_0(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,X0,X2)|~m1_relset_1(X1,X0,X2)|~m1_subset_1(X3,X0)|~m1_conlat_1(X2,sK0_skl)|~v7_conlat_1(k8_funct_2(X0,X2,X1,X3),sK0_skl)|~sQ160_spl)),
% 62.82/8.50 inference(component_clause,[status(thm)],[f1528])).
% 62.82/8.50 fof(f1531,plain,(
% 62.82/8.50 sQ160_spl|sQ18_spl),
% 62.82/8.50 inference(split_clause,[status(thm)],[f1523,f1528,f538])).
% 62.82/8.50 fof(f1545,plain,(
% 62.82/8.50 ![X0,X1,X2,X3]: (v1_xboole_0(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,X0,X2)|~m1_relset_1(X1,X0,X2)|~m1_subset_1(X3,X0)|v3_conlat_1(sK0_skl)|~m1_conlat_1(X2,sK0_skl)|v9_conlat_1(k8_funct_2(X0,X2,X1,X3),sK0_skl))),
% 62.82/8.50 inference(resolution,[status(thm)],[f1470,f102])).
% 62.82/8.50 fof(f1550,definition,(
% 62.82/8.50 ![X0,X1,X2,X3]: (sQ164_spl <=> (v1_xboole_0(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,X0,X2)|~m1_relset_1(X1,X0,X2)|~m1_subset_1(X3,X0)|~m1_conlat_1(X2,sK0_skl)|v9_conlat_1(k8_funct_2(X0,X2,X1,X3),sK0_skl)))),
% 62.82/8.50 introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition])).
% 62.82/8.50 fof(f1551,plain,(
% 62.82/8.50 ![X0,X1,X2,X3]: (v1_xboole_0(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,X0,X2)|~m1_relset_1(X1,X0,X2)|~m1_subset_1(X3,X0)|~m1_conlat_1(X2,sK0_skl)|v9_conlat_1(k8_funct_2(X0,X2,X1,X3),sK0_skl)|~sQ164_spl)),
% 62.82/8.50 inference(component_clause,[status(thm)],[f1550])).
% 62.82/8.50 fof(f1553,plain,(
% 62.82/8.50 sQ164_spl|sQ18_spl),
% 62.82/8.50 inference(split_clause,[status(thm)],[f1545,f1550,f538])).
% 62.82/8.50 fof(f1555,plain,(
% 62.82/8.50 ![X0,X1,X2,X3]: (v1_xboole_0(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,X0,X2)|~m1_relset_1(X1,X0,X2)|~m1_subset_1(X3,X0)|v3_conlat_1(sK0_skl)|~m1_conlat_1(X2,sK0_skl)|l3_conlat_1(k8_funct_2(X0,X2,X1,X3),sK0_skl))),
% 62.82/8.50 inference(resolution,[status(thm)],[f1471,f102])).
% 62.82/8.50 fof(f1560,definition,(
% 62.82/8.50 ![X0,X1,X2,X3]: (sQ166_spl <=> (v1_xboole_0(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,X0,X2)|~m1_relset_1(X1,X0,X2)|~m1_subset_1(X3,X0)|~m1_conlat_1(X2,sK0_skl)|l3_conlat_1(k8_funct_2(X0,X2,X1,X3),sK0_skl)))),
% 62.82/8.50 introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition])).
% 62.82/8.50 fof(f1561,plain,(
% 62.82/8.50 ![X0,X1,X2,X3]: (v1_xboole_0(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,X0,X2)|~m1_relset_1(X1,X0,X2)|~m1_subset_1(X3,X0)|~m1_conlat_1(X2,sK0_skl)|l3_conlat_1(k8_funct_2(X0,X2,X1,X3),sK0_skl)|~sQ166_spl)),
% 62.82/8.50 inference(component_clause,[status(thm)],[f1560])).
% 62.82/8.50 fof(f1563,plain,(
% 62.82/8.50 sQ166_spl|sQ18_spl),
% 62.82/8.50 inference(split_clause,[status(thm)],[f1555,f1560,f538])).
% 62.82/8.50 fof(f1829,plain,(
% 62.82/8.50 v1_xboole_0(u1_conlat_1(sK0_skl))|~v1_funct_1(k4_conlat_2(sK0_skl))|~v1_funct_2(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),u1_struct_0(k11_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)))|~m1_subset_1(sK1_skl,u1_conlat_1(sK0_skl))|~m1_conlat_1(u1_struct_0(k11_conlat_1(sK0_skl)),sK0_skl)|~sQ160_spl|~sQ0_spl),
% 62.82/8.50 inference(resolution,[status(thm)],[f1529,f413])).
% 62.82/8.50 fof(f1830,plain,(
% 62.82/8.50 v1_xboole_0(u2_conlat_1(sK0_skl))|~v1_funct_1(k5_conlat_2(sK0_skl))|~v1_funct_2(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),u1_struct_0(k11_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)))|~m1_subset_1(sK2_skl,u2_conlat_1(sK0_skl))|~m1_conlat_1(u1_struct_0(k11_conlat_1(sK0_skl)),sK0_skl)|~sQ160_spl|~sQ3_spl),
% 62.82/8.50 inference(resolution,[status(thm)],[f1529,f422])).
% 62.82/8.50 fof(f1831,definition,(
% 62.82/8.50 sQ212_spl <=> (v1_funct_1(k4_conlat_2(sK0_skl)))),
% 62.82/8.50 introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition])).
% 62.82/8.50 fof(f1833,plain,(
% 62.82/8.50 ~v1_funct_1(k4_conlat_2(sK0_skl))|sQ212_spl),
% 62.82/8.50 inference(component_clause,[status(thm)],[f1831])).
% 62.82/8.50 fof(f1834,definition,(
% 62.82/8.50 sQ213_spl <=> (v1_funct_2(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl))))),
% 62.82/8.50 introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition])).
% 62.82/8.50 fof(f1836,plain,(
% 62.82/8.50 ~v1_funct_2(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)))|sQ213_spl),
% 62.82/8.50 inference(component_clause,[status(thm)],[f1834])).
% 62.82/8.50 fof(f1837,definition,(
% 62.82/8.50 sQ214_spl <=> (m1_relset_1(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl))))),
% 62.82/8.50 introduced(definition,[new_symbols(definition,[sQ214_spl])],[split_symbol_definition])).
% 62.82/8.50 fof(f1839,plain,(
% 62.82/8.50 ~m1_relset_1(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)))|sQ214_spl),
% 62.82/8.50 inference(component_clause,[status(thm)],[f1837])).
% 62.82/8.50 fof(f1840,definition,(
% 62.82/8.50 sQ215_spl <=> (m1_subset_1(sK1_skl,u1_conlat_1(sK0_skl)))),
% 62.82/8.50 introduced(definition,[new_symbols(definition,[sQ215_spl])],[split_symbol_definition])).
% 62.82/8.50 fof(f1842,plain,(
% 62.82/8.50 ~m1_subset_1(sK1_skl,u1_conlat_1(sK0_skl))|sQ215_spl),
% 62.82/8.50 inference(component_clause,[status(thm)],[f1840])).
% 62.82/8.50 fof(f1843,definition,(
% 62.82/8.50 sQ216_spl <=> (m1_conlat_1(u1_struct_0(k11_conlat_1(sK0_skl)),sK0_skl))),
% 62.82/8.50 introduced(definition,[new_symbols(definition,[sQ216_spl])],[split_symbol_definition])).
% 62.82/8.50 fof(f1845,plain,(
% 62.82/8.50 ~m1_conlat_1(u1_struct_0(k11_conlat_1(sK0_skl)),sK0_skl)|sQ216_spl),
% 62.82/8.50 inference(component_clause,[status(thm)],[f1843])).
% 62.82/8.50 fof(f1846,plain,(
% 62.82/8.50 sQ147_spl|~sQ212_spl|~sQ213_spl|~sQ214_spl|~sQ215_spl|~sQ216_spl|~sQ160_spl|~sQ0_spl),
% 62.82/8.50 inference(split_clause,[status(thm)],[f1829,f1405,f1831,f1834,f1837,f1840,f1843,f1528,f412])).
% 62.82/8.50 fof(f1847,definition,(
% 62.82/8.50 sQ217_spl <=> (v1_funct_1(k5_conlat_2(sK0_skl)))),
% 62.82/8.50 introduced(definition,[new_symbols(definition,[sQ217_spl])],[split_symbol_definition])).
% 62.82/8.50 fof(f1849,plain,(
% 62.82/8.50 ~v1_funct_1(k5_conlat_2(sK0_skl))|sQ217_spl),
% 62.82/8.50 inference(component_clause,[status(thm)],[f1847])).
% 62.82/8.50 fof(f1850,definition,(
% 62.82/8.50 sQ218_spl <=> (v1_funct_2(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl))))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ218_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f1852,plain,(
% 62.82/8.51 ~v1_funct_2(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)))|sQ218_spl),
% 62.82/8.51 inference(component_clause,[status(thm)],[f1850])).
% 62.82/8.51 fof(f1853,definition,(
% 62.82/8.51 sQ219_spl <=> (m1_relset_1(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl))))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f1855,plain,(
% 62.82/8.51 ~m1_relset_1(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),u1_struct_0(k11_conlat_1(sK0_skl)))|sQ219_spl),
% 62.82/8.51 inference(component_clause,[status(thm)],[f1853])).
% 62.82/8.51 fof(f1856,definition,(
% 62.82/8.51 sQ220_spl <=> (m1_subset_1(sK2_skl,u2_conlat_1(sK0_skl)))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ220_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f1858,plain,(
% 62.82/8.51 ~m1_subset_1(sK2_skl,u2_conlat_1(sK0_skl))|sQ220_spl),
% 62.82/8.51 inference(component_clause,[status(thm)],[f1856])).
% 62.82/8.51 fof(f1859,plain,(
% 62.82/8.51 sQ145_spl|~sQ217_spl|~sQ218_spl|~sQ219_spl|~sQ220_spl|~sQ216_spl|~sQ160_spl|~sQ3_spl),
% 62.82/8.51 inference(split_clause,[status(thm)],[f1830,f1398,f1847,f1850,f1853,f1856,f1843,f1528,f421])).
% 62.82/8.51 fof(f1860,plain,(
% 62.82/8.51 $false|sQ220_spl),
% 62.82/8.51 inference(forward_subsumption_resolution,[status(thm)],[f1858,f104])).
% 62.82/8.51 fof(f1861,plain,(
% 62.82/8.51 sQ220_spl),
% 62.82/8.51 inference(contradiction_clause,[status(thm)],[f1860])).
% 62.82/8.51 fof(f1862,plain,(
% 62.82/8.51 $false|sQ215_spl),
% 62.82/8.51 inference(forward_subsumption_resolution,[status(thm)],[f1842,f103])).
% 62.82/8.51 fof(f1863,plain,(
% 62.82/8.51 sQ215_spl),
% 62.82/8.51 inference(contradiction_clause,[status(thm)],[f1862])).
% 62.82/8.51 fof(f1864,plain,(
% 62.82/8.51 v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)|sQ217_spl),
% 62.82/8.51 inference(resolution,[status(thm)],[f1849,f172])).
% 62.82/8.51 fof(f1865,plain,(
% 62.82/8.51 sQ18_spl|~sQ16_spl|sQ217_spl),
% 62.82/8.51 inference(split_clause,[status(thm)],[f1864,f538,f527,f1847])).
% 62.82/8.51 fof(f1866,plain,(
% 62.82/8.51 v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)|sQ212_spl),
% 62.82/8.51 inference(resolution,[status(thm)],[f1833,f168])).
% 62.82/8.51 fof(f1867,plain,(
% 62.82/8.51 sQ18_spl|~sQ16_spl|sQ212_spl),
% 62.82/8.51 inference(split_clause,[status(thm)],[f1866,f538,f527,f1831])).
% 62.82/8.51 fof(f2076,plain,(
% 62.82/8.51 v1_xboole_0(u1_conlat_1(sK0_skl))|~v1_funct_1(k4_conlat_2(sK0_skl))|~v1_funct_2(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),u1_struct_0(k11_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)))|~m1_subset_1(sK1_skl,u1_conlat_1(sK0_skl))|~m1_conlat_1(u1_struct_0(k11_conlat_1(sK0_skl)),sK0_skl)|~sQ164_spl|sQ1_spl),
% 62.82/8.51 inference(resolution,[status(thm)],[f1551,f417])).
% 62.82/8.51 fof(f2077,plain,(
% 62.82/8.51 v1_xboole_0(u2_conlat_1(sK0_skl))|~v1_funct_1(k5_conlat_2(sK0_skl))|~v1_funct_2(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),u1_struct_0(k11_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)))|~m1_subset_1(sK2_skl,u2_conlat_1(sK0_skl))|~m1_conlat_1(u1_struct_0(k11_conlat_1(sK0_skl)),sK0_skl)|~sQ164_spl|sQ4_spl),
% 62.82/8.51 inference(resolution,[status(thm)],[f1551,f426])).
% 62.82/8.51 fof(f2078,plain,(
% 62.82/8.51 sQ147_spl|~sQ212_spl|~sQ213_spl|~sQ214_spl|~sQ215_spl|~sQ216_spl|~sQ164_spl|sQ1_spl),
% 62.82/8.51 inference(split_clause,[status(thm)],[f2076,f1405,f1831,f1834,f1837,f1840,f1843,f1550,f415])).
% 62.82/8.51 fof(f2079,plain,(
% 62.82/8.51 sQ145_spl|~sQ217_spl|~sQ218_spl|~sQ219_spl|~sQ220_spl|~sQ216_spl|~sQ164_spl|sQ4_spl),
% 62.82/8.51 inference(split_clause,[status(thm)],[f2077,f1398,f1847,f1850,f1853,f1856,f1843,f1550,f424])).
% 62.82/8.51 fof(f2080,plain,(
% 62.82/8.51 v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)|sQ218_spl),
% 62.82/8.51 inference(resolution,[status(thm)],[f1852,f173])).
% 62.82/8.51 fof(f2082,plain,(
% 62.82/8.51 sQ18_spl|~sQ16_spl|sQ218_spl),
% 62.82/8.51 inference(split_clause,[status(thm)],[f2080,f538,f527,f1850])).
% 62.82/8.51 fof(f2088,plain,(
% 62.82/8.51 v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)|sQ213_spl),
% 62.82/8.51 inference(resolution,[status(thm)],[f1836,f169])).
% 62.82/8.51 fof(f2090,plain,(
% 62.82/8.51 sQ18_spl|~sQ16_spl|sQ213_spl),
% 62.82/8.51 inference(split_clause,[status(thm)],[f2088,f538,f527,f1834])).
% 62.82/8.51 fof(f2147,plain,(
% 62.82/8.51 ![X0,X1,X2,X3,X4,X5]: (~v1_funct_1(X0)|~v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)|~m1_relset_1(X0,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X2)|~m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~g3_lattices(X1,X0,X2)=g3_lattices(X3,X4,X5)|X1=X3|~m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X2)|~v1_partfun1(X2,k2_zfmisc_1(X1,X1),X1))),
% 62.82/8.51 inference(resolution,[status(thm)],[f305,f112])).
% 62.82/8.51 fof(f2158,definition,(
% 62.82/8.51 ![X0,X1,X2,X3]: (sQ256_spl <=> (~v1_funct_1(X0)|~v1_funct_2(X0,k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k7_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))|~g3_lattices(k7_conlat_1(sK0_skl),X0,k9_conlat_1(sK0_skl))=g3_lattices(X1,X2,X3)|k7_conlat_1(sK0_skl)=X1))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f2159,plain,(
% 62.82/8.51 ![X0,X1,X2,X3]: (~v1_funct_1(X0)|~v1_funct_2(X0,k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k7_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))|~g3_lattices(k7_conlat_1(sK0_skl),X0,k9_conlat_1(sK0_skl))=g3_lattices(X1,X2,X3)|k7_conlat_1(sK0_skl)=X1|~sQ256_spl)),
% 62.82/8.51 inference(component_clause,[status(thm)],[f2158])).
% 62.82/8.51 fof(f2167,plain,(
% 62.82/8.51 ![X0,X1,X2,X3,X4,X5]: (~v1_funct_1(X0)|~v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)|~m1_relset_1(X0,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X2)|~m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~g3_lattices(X1,X0,X2)=g3_lattices(X3,X4,X5)|X1=X3|~v1_partfun1(X2,k2_zfmisc_1(X1,X1),X1))),
% 62.82/8.51 inference(duplicate_literals_removal,[status(thm)],[f2147])).
% 62.82/8.51 fof(f2322,plain,(
% 62.82/8.51 ![X0,X1,X2]: (~v1_funct_1(k10_conlat_1(sK0_skl))|~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))|~g3_lattices(k7_conlat_1(sK0_skl),k10_conlat_1(sK0_skl),k9_conlat_1(sK0_skl))=g3_lattices(X0,X1,X2)|k7_conlat_1(sK0_skl)=X0|~sQ256_spl|~sQ17_spl|~sQ78_spl)),
% 62.82/8.51 inference(resolution,[status(thm)],[f2159,f852])).
% 62.82/8.51 fof(f2329,definition,(
% 62.82/8.51 ![X0,X1,X2]: (sQ277_spl <=> (~g3_lattices(k7_conlat_1(sK0_skl),k10_conlat_1(sK0_skl),k9_conlat_1(sK0_skl))=g3_lattices(X0,X1,X2)|k7_conlat_1(sK0_skl)=X0))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ277_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f2330,plain,(
% 62.82/8.51 ![X0,X1,X2]: (~g3_lattices(k7_conlat_1(sK0_skl),k10_conlat_1(sK0_skl),k9_conlat_1(sK0_skl))=g3_lattices(X0,X1,X2)|k7_conlat_1(sK0_skl)=X0|~sQ277_spl)),
% 62.82/8.51 inference(component_clause,[status(thm)],[f2329])).
% 62.82/8.51 fof(f2332,plain,(
% 62.82/8.51 ~sQ66_spl|~sQ68_spl|sQ277_spl|~sQ256_spl|~sQ17_spl|~sQ78_spl),
% 62.82/8.51 inference(split_clause,[status(thm)],[f2322,f796,f802,f2329,f2158,f530,f846])).
% 62.82/8.51 fof(f2338,plain,(
% 62.82/8.51 ![X0,X1,X2]: (~k11_conlat_1(sK0_skl)=g3_lattices(X0,X1,X2)|k7_conlat_1(sK0_skl)=X0|~sQ17_spl|~sQ64_spl|~sQ277_spl)),
% 62.82/8.51 inference(forward_demodulation,[status(thm)],[f778,f2330])).
% 62.82/8.51 fof(f2339,plain,(
% 62.82/8.51 k7_conlat_1(sK0_skl)=u1_struct_0(k11_conlat_1(sK0_skl))|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl),
% 62.82/8.51 inference(resolution,[status(thm)],[f2338,f823])).
% 62.82/8.51 fof(f2343,definition,(
% 62.82/8.51 sQ279_spl <=> (k11_conlat_1(sK0_skl)=k11_conlat_1(sK0_skl))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ279_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f2345,plain,(
% 62.82/8.51 ~k11_conlat_1(sK0_skl)=k11_conlat_1(sK0_skl)|sQ279_spl),
% 62.82/8.51 inference(component_clause,[status(thm)],[f2343])).
% 62.82/8.51 fof(f2354,plain,(
% 62.82/8.51 $false|sQ279_spl),
% 62.82/8.51 inference(trivial_equality_resolution,[status(thm)],[f2345])).
% 62.82/8.51 fof(f2355,plain,(
% 62.82/8.51 sQ279_spl),
% 62.82/8.51 inference(contradiction_clause,[status(thm)],[f2354])).
% 62.82/8.51 fof(f2358,plain,(
% 62.82/8.51 ~m1_relset_1(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),k7_conlat_1(sK0_skl))|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl|sQ214_spl),
% 62.82/8.51 inference(backward_demodulation,[status(thm)],[f2339,f1839])).
% 62.82/8.51 fof(f2359,plain,(
% 62.82/8.51 ~m1_relset_1(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),k7_conlat_1(sK0_skl))|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl|sQ219_spl),
% 62.82/8.51 inference(backward_demodulation,[status(thm)],[f2339,f1855])).
% 62.82/8.51 fof(f2360,plain,(
% 62.82/8.51 ~m1_conlat_1(k7_conlat_1(sK0_skl),sK0_skl)|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl|sQ216_spl),
% 62.82/8.51 inference(backward_demodulation,[status(thm)],[f2339,f1845])).
% 62.82/8.51 fof(f2386,plain,(
% 62.82/8.51 ~l3_conlat_1(k8_funct_2(u1_conlat_1(sK0_skl),k7_conlat_1(sK0_skl),k4_conlat_2(sK0_skl),sK1_skl),sK0_skl)|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl|sQ2_spl),
% 62.82/8.51 inference(backward_demodulation,[status(thm)],[f2339,f420])).
% 62.82/8.51 fof(f2388,plain,(
% 62.82/8.51 ~l3_conlat_1(k8_funct_2(u2_conlat_1(sK0_skl),k7_conlat_1(sK0_skl),k5_conlat_2(sK0_skl),sK2_skl),sK0_skl)|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl|sQ5_spl),
% 62.82/8.51 inference(backward_demodulation,[status(thm)],[f2339,f429])).
% 62.82/8.51 fof(f2391,plain,(
% 62.82/8.51 v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)|m2_relset_1(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),k7_conlat_1(sK0_skl))|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl),
% 62.82/8.51 inference(paramodulation,[status(thm)],[f2339,f174])).
% 62.82/8.51 fof(f2392,plain,(
% 62.82/8.51 v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)|v1_funct_2(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),k7_conlat_1(sK0_skl))|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl),
% 62.82/8.51 inference(paramodulation,[status(thm)],[f2339,f173])).
% 62.82/8.51 fof(f2393,plain,(
% 62.82/8.51 v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)|m2_relset_1(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),k7_conlat_1(sK0_skl))|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl),
% 62.82/8.51 inference(paramodulation,[status(thm)],[f2339,f170])).
% 62.82/8.51 fof(f2394,plain,(
% 62.82/8.51 v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)|v1_funct_2(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),k7_conlat_1(sK0_skl))|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl),
% 62.82/8.51 inference(paramodulation,[status(thm)],[f2339,f169])).
% 62.82/8.51 fof(f2425,plain,(
% 62.82/8.51 $false|~sQ19_spl|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl|sQ216_spl),
% 62.82/8.51 inference(forward_subsumption_resolution,[status(thm)],[f2360,f542])).
% 62.82/8.51 fof(f2426,plain,(
% 62.82/8.51 ~sQ19_spl|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl|sQ216_spl),
% 62.82/8.51 inference(contradiction_clause,[status(thm)],[f2425])).
% 62.82/8.51 fof(f2460,definition,(
% 62.82/8.51 sQ284_spl <=> (m2_relset_1(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ284_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f2461,plain,(
% 62.82/8.51 m2_relset_1(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),k7_conlat_1(sK0_skl))|~sQ284_spl),
% 62.82/8.51 inference(component_clause,[status(thm)],[f2460])).
% 62.82/8.51 fof(f2463,plain,(
% 62.82/8.51 sQ18_spl|~sQ16_spl|sQ284_spl|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl),
% 62.82/8.51 inference(split_clause,[status(thm)],[f2391,f538,f527,f2460,f530,f773,f2329,f822])).
% 62.82/8.51 fof(f2464,definition,(
% 62.82/8.51 sQ285_spl <=> (v1_funct_2(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ285_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f2467,plain,(
% 62.82/8.51 sQ18_spl|~sQ16_spl|sQ285_spl|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl),
% 62.82/8.51 inference(split_clause,[status(thm)],[f2392,f538,f527,f2464,f530,f773,f2329,f822])).
% 62.82/8.51 fof(f2468,definition,(
% 62.82/8.51 sQ286_spl <=> (m2_relset_1(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ286_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f2469,plain,(
% 62.82/8.51 m2_relset_1(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),k7_conlat_1(sK0_skl))|~sQ286_spl),
% 62.82/8.51 inference(component_clause,[status(thm)],[f2468])).
% 62.82/8.51 fof(f2471,plain,(
% 62.82/8.51 sQ18_spl|~sQ16_spl|sQ286_spl|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl),
% 62.82/8.51 inference(split_clause,[status(thm)],[f2393,f538,f527,f2468,f530,f773,f2329,f822])).
% 62.82/8.51 fof(f2472,definition,(
% 62.82/8.51 sQ287_spl <=> (v1_funct_2(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ287_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f2475,plain,(
% 62.82/8.51 sQ18_spl|~sQ16_spl|sQ287_spl|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl),
% 62.82/8.51 inference(split_clause,[status(thm)],[f2394,f538,f527,f2472,f530,f773,f2329,f822])).
% 62.82/8.51 fof(f2631,definition,(
% 62.82/8.51 sQ315_spl <=> (l1_conlat_1(sK4_skl))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ315_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f2633,plain,(
% 62.82/8.51 ~l1_conlat_1(sK4_skl)|sQ315_spl),
% 62.82/8.51 inference(component_clause,[status(thm)],[f2631])).
% 62.82/8.51 fof(f2638,plain,(
% 62.82/8.51 $false|sQ315_spl),
% 62.82/8.51 inference(forward_subsumption_resolution,[status(thm)],[f2633,f207])).
% 62.82/8.51 fof(f2639,plain,(
% 62.82/8.51 sQ315_spl),
% 62.82/8.51 inference(contradiction_clause,[status(thm)],[f2638])).
% 62.82/8.51 fof(f2732,definition,(
% 62.82/8.51 sQ330_spl <=> (m1_relset_1(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ330_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f2734,plain,(
% 62.82/8.51 ~m1_relset_1(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),k7_conlat_1(sK0_skl))|sQ330_spl),
% 62.82/8.51 inference(component_clause,[status(thm)],[f2732])).
% 62.82/8.51 fof(f2766,plain,(
% 62.82/8.51 ~m2_relset_1(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),k7_conlat_1(sK0_skl))|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl|sQ214_spl),
% 62.82/8.51 inference(resolution,[status(thm)],[f2358,f386])).
% 62.82/8.51 fof(f2767,plain,(
% 62.82/8.51 ~m2_relset_1(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),k7_conlat_1(sK0_skl))|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl|sQ219_spl),
% 62.82/8.51 inference(resolution,[status(thm)],[f2359,f386])).
% 62.82/8.51 fof(f2770,definition,(
% 62.82/8.51 sQ336_spl <=> (m1_relset_1(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ336_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f2772,plain,(
% 62.82/8.51 ~m1_relset_1(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),k7_conlat_1(sK0_skl))|sQ336_spl),
% 62.82/8.51 inference(component_clause,[status(thm)],[f2770])).
% 62.82/8.51 fof(f2880,definition,(
% 62.82/8.51 sQ352_spl <=> (v3_struct_0(sK15_skl))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ352_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f2881,plain,(
% 62.82/8.51 v3_struct_0(sK15_skl)|~sQ352_spl),
% 62.82/8.51 inference(component_clause,[status(thm)],[f2880])).
% 62.82/8.51 fof(f2883,definition,(
% 62.82/8.51 sQ353_spl <=> (l1_struct_0(sK15_skl))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ353_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f2885,plain,(
% 62.82/8.51 ~l1_struct_0(sK15_skl)|sQ353_spl),
% 62.82/8.51 inference(component_clause,[status(thm)],[f2883])).
% 62.82/8.51 fof(f2890,definition,(
% 62.82/8.51 sQ355_spl <=> (l1_lattices(sK15_skl))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ355_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f2892,plain,(
% 62.82/8.51 ~l1_lattices(sK15_skl)|sQ355_spl),
% 62.82/8.51 inference(component_clause,[status(thm)],[f2890])).
% 62.82/8.51 fof(f2916,definition,(
% 62.82/8.51 sQ361_spl <=> (l2_lattices(sK15_skl))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ361_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f2918,plain,(
% 62.82/8.51 ~l2_lattices(sK15_skl)|sQ361_spl),
% 62.82/8.51 inference(component_clause,[status(thm)],[f2916])).
% 62.82/8.51 fof(f2991,plain,(
% 62.82/8.51 $false|~sQ352_spl),
% 62.82/8.51 inference(forward_subsumption_resolution,[status(thm)],[f2881,f310])).
% 62.82/8.51 fof(f2992,plain,(
% 62.82/8.51 ~sQ352_spl),
% 62.82/8.51 inference(contradiction_clause,[status(thm)],[f2991])).
% 62.82/8.51 fof(f2993,plain,(
% 62.82/8.51 $false|sQ361_spl),
% 62.82/8.51 inference(forward_subsumption_resolution,[status(thm)],[f2918,f487])).
% 62.82/8.51 fof(f2994,plain,(
% 62.82/8.51 sQ361_spl),
% 62.82/8.51 inference(contradiction_clause,[status(thm)],[f2993])).
% 62.82/8.51 fof(f2995,plain,(
% 62.82/8.51 $false|sQ355_spl),
% 62.82/8.51 inference(forward_subsumption_resolution,[status(thm)],[f2892,f481])).
% 62.82/8.51 fof(f2996,plain,(
% 62.82/8.51 sQ355_spl),
% 62.82/8.51 inference(contradiction_clause,[status(thm)],[f2995])).
% 62.82/8.51 fof(f2997,plain,(
% 62.82/8.51 $false|sQ353_spl),
% 62.82/8.51 inference(forward_subsumption_resolution,[status(thm)],[f2885,f933])).
% 62.82/8.51 fof(f2998,plain,(
% 62.82/8.51 sQ353_spl),
% 62.82/8.51 inference(contradiction_clause,[status(thm)],[f2997])).
% 62.82/8.51 fof(f3054,definition,(
% 62.82/8.51 sQ383_spl <=> (v1_xboole_0(k1_zfmisc_1(k7_conlat_1(sK0_skl))))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ383_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f3055,plain,(
% 62.82/8.51 v1_xboole_0(k1_zfmisc_1(k7_conlat_1(sK0_skl)))|~sQ383_spl),
% 62.82/8.51 inference(component_clause,[status(thm)],[f3054])).
% 62.82/8.51 fof(f3061,plain,(
% 62.82/8.51 $false|~sQ383_spl),
% 62.82/8.51 inference(forward_subsumption_resolution,[status(thm)],[f3055,f248])).
% 62.82/8.51 fof(f3062,plain,(
% 62.82/8.51 ~sQ383_spl),
% 62.82/8.51 inference(contradiction_clause,[status(thm)],[f3061])).
% 62.82/8.51 fof(f3267,definition,(
% 62.82/8.51 sQ419_spl <=> (l1_struct_0(sK23_skl))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ419_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f3269,plain,(
% 62.82/8.51 ~l1_struct_0(sK23_skl)|sQ419_spl),
% 62.82/8.51 inference(component_clause,[status(thm)],[f3267])).
% 62.82/8.51 fof(f3277,definition,(
% 62.82/8.51 sQ422_spl <=> (l1_lattices(sK23_skl))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ422_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f3279,plain,(
% 62.82/8.51 ~l1_lattices(sK23_skl)|sQ422_spl),
% 62.82/8.51 inference(component_clause,[status(thm)],[f3277])).
% 62.82/8.51 fof(f3309,definition,(
% 62.82/8.51 sQ430_spl <=> (l2_lattices(sK23_skl))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ430_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f3311,plain,(
% 62.82/8.51 ~l2_lattices(sK23_skl)|sQ430_spl),
% 62.82/8.51 inference(component_clause,[status(thm)],[f3309])).
% 62.82/8.51 fof(f3387,plain,(
% 62.82/8.51 $false|sQ430_spl),
% 62.82/8.51 inference(forward_subsumption_resolution,[status(thm)],[f3311,f486])).
% 62.82/8.51 fof(f3388,plain,(
% 62.82/8.51 sQ430_spl),
% 62.82/8.51 inference(contradiction_clause,[status(thm)],[f3387])).
% 62.82/8.51 fof(f3389,plain,(
% 62.82/8.51 $false|sQ422_spl),
% 62.82/8.51 inference(forward_subsumption_resolution,[status(thm)],[f3279,f480])).
% 62.82/8.51 fof(f3390,plain,(
% 62.82/8.51 sQ422_spl),
% 62.82/8.51 inference(contradiction_clause,[status(thm)],[f3389])).
% 62.82/8.51 fof(f3391,plain,(
% 62.82/8.51 $false|sQ419_spl),
% 62.82/8.51 inference(forward_subsumption_resolution,[status(thm)],[f3269,f934])).
% 62.82/8.51 fof(f3392,plain,(
% 62.82/8.51 sQ419_spl),
% 62.82/8.51 inference(contradiction_clause,[status(thm)],[f3391])).
% 62.82/8.51 fof(f3476,definition,(
% 62.82/8.51 sQ453_spl <=> (v3_struct_0(sK26_skl))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ453_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f3477,plain,(
% 62.82/8.51 v3_struct_0(sK26_skl)|~sQ453_spl),
% 62.82/8.51 inference(component_clause,[status(thm)],[f3476])).
% 62.82/8.51 fof(f3479,definition,(
% 62.82/8.51 sQ454_spl <=> (l1_struct_0(sK26_skl))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ454_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f3481,plain,(
% 62.82/8.51 ~l1_struct_0(sK26_skl)|sQ454_spl),
% 62.82/8.51 inference(component_clause,[status(thm)],[f3479])).
% 62.82/8.51 fof(f3486,definition,(
% 62.82/8.51 sQ456_spl <=> (l1_lattices(sK26_skl))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ456_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f3488,plain,(
% 62.82/8.51 ~l1_lattices(sK26_skl)|sQ456_spl),
% 62.82/8.51 inference(component_clause,[status(thm)],[f3486])).
% 62.82/8.51 fof(f3512,definition,(
% 62.82/8.51 sQ462_spl <=> (l2_lattices(sK26_skl))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ462_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f3514,plain,(
% 62.82/8.51 ~l2_lattices(sK26_skl)|sQ462_spl),
% 62.82/8.51 inference(component_clause,[status(thm)],[f3512])).
% 62.82/8.51 fof(f3587,plain,(
% 62.82/8.51 $false|~sQ453_spl),
% 62.82/8.51 inference(forward_subsumption_resolution,[status(thm)],[f3477,f359])).
% 62.82/8.51 fof(f3588,plain,(
% 62.82/8.51 ~sQ453_spl),
% 62.82/8.51 inference(contradiction_clause,[status(thm)],[f3587])).
% 62.82/8.51 fof(f3589,plain,(
% 62.82/8.51 $false|sQ462_spl),
% 62.82/8.51 inference(forward_subsumption_resolution,[status(thm)],[f3514,f485])).
% 62.82/8.51 fof(f3590,plain,(
% 62.82/8.51 sQ462_spl),
% 62.82/8.51 inference(contradiction_clause,[status(thm)],[f3589])).
% 62.82/8.51 fof(f3591,plain,(
% 62.82/8.51 $false|sQ456_spl),
% 62.82/8.51 inference(forward_subsumption_resolution,[status(thm)],[f3488,f479])).
% 62.82/8.51 fof(f3592,plain,(
% 62.82/8.51 sQ456_spl),
% 62.82/8.51 inference(contradiction_clause,[status(thm)],[f3591])).
% 62.82/8.51 fof(f3593,plain,(
% 62.82/8.51 $false|sQ454_spl),
% 62.82/8.51 inference(forward_subsumption_resolution,[status(thm)],[f3481,f935])).
% 62.82/8.51 fof(f3594,plain,(
% 62.82/8.51 sQ454_spl),
% 62.82/8.51 inference(contradiction_clause,[status(thm)],[f3593])).
% 62.82/8.51 fof(f3662,definition,(
% 62.82/8.51 sQ480_spl <=> (v3_struct_0(sK29_skl))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ480_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f3663,plain,(
% 62.82/8.51 v3_struct_0(sK29_skl)|~sQ480_spl),
% 62.82/8.51 inference(component_clause,[status(thm)],[f3662])).
% 62.82/8.51 fof(f3665,definition,(
% 62.82/8.51 sQ481_spl <=> (l1_struct_0(sK29_skl))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ481_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f3667,plain,(
% 62.82/8.51 ~l1_struct_0(sK29_skl)|sQ481_spl),
% 62.82/8.51 inference(component_clause,[status(thm)],[f3665])).
% 62.82/8.51 fof(f3672,definition,(
% 62.82/8.51 sQ483_spl <=> (l1_lattices(sK29_skl))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ483_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f3674,plain,(
% 62.82/8.51 ~l1_lattices(sK29_skl)|sQ483_spl),
% 62.82/8.51 inference(component_clause,[status(thm)],[f3672])).
% 62.82/8.51 fof(f3698,definition,(
% 62.82/8.51 sQ489_spl <=> (l2_lattices(sK29_skl))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ489_spl])],[split_symbol_definition])).
% 62.82/8.51 fof(f3700,plain,(
% 62.82/8.51 ~l2_lattices(sK29_skl)|sQ489_spl),
% 62.82/8.51 inference(component_clause,[status(thm)],[f3698])).
% 62.82/8.51 fof(f3773,plain,(
% 62.82/8.51 $false|~sQ480_spl),
% 62.82/8.51 inference(forward_subsumption_resolution,[status(thm)],[f3663,f371])).
% 62.82/8.51 fof(f3774,plain,(
% 62.82/8.51 ~sQ480_spl),
% 62.82/8.51 inference(contradiction_clause,[status(thm)],[f3773])).
% 62.82/8.51 fof(f3775,plain,(
% 62.82/8.51 $false|sQ489_spl),
% 62.82/8.51 inference(forward_subsumption_resolution,[status(thm)],[f3700,f484])).
% 62.82/8.51 fof(f3776,plain,(
% 62.82/8.51 sQ489_spl),
% 62.82/8.51 inference(contradiction_clause,[status(thm)],[f3775])).
% 62.82/8.51 fof(f3777,plain,(
% 62.82/8.51 $false|sQ483_spl),
% 62.82/8.51 inference(forward_subsumption_resolution,[status(thm)],[f3674,f478])).
% 62.82/8.51 fof(f3778,plain,(
% 62.82/8.51 sQ483_spl),
% 62.82/8.51 inference(contradiction_clause,[status(thm)],[f3777])).
% 62.82/8.51 fof(f3779,plain,(
% 62.82/8.51 $false|sQ481_spl),
% 62.82/8.51 inference(forward_subsumption_resolution,[status(thm)],[f3667,f936])).
% 62.82/8.51 fof(f3780,plain,(
% 62.82/8.51 sQ481_spl),
% 62.82/8.51 inference(contradiction_clause,[status(thm)],[f3779])).
% 62.82/8.51 fof(f4403,plain,(
% 62.82/8.51 $false|~sQ286_spl|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl|sQ214_spl),
% 62.82/8.51 inference(forward_subsumption_resolution,[status(thm)],[f2766,f2469])).
% 62.82/8.51 fof(f4404,plain,(
% 62.82/8.51 ~sQ286_spl|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl|sQ214_spl),
% 62.82/8.51 inference(contradiction_clause,[status(thm)],[f4403])).
% 62.82/8.51 fof(f4406,plain,(
% 62.82/8.51 $false|~sQ284_spl|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl|sQ219_spl),
% 62.82/8.51 inference(forward_subsumption_resolution,[status(thm)],[f2767,f2461])).
% 62.82/8.51 fof(f4407,plain,(
% 62.82/8.51 ~sQ284_spl|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl|sQ219_spl),
% 62.82/8.51 inference(contradiction_clause,[status(thm)],[f4406])).
% 62.82/8.51 fof(f5596,definition,(
% 62.82/8.51 sQ769_spl <=> (l1_struct_0(sK8_skl))),
% 62.82/8.51 introduced(definition,[new_symbols(definition,[sQ769_spl])],[split_symbol_definition])).
% 62.82/8.53 fof(f5598,plain,(
% 62.82/8.53 ~l1_struct_0(sK8_skl)|sQ769_spl),
% 62.82/8.53 inference(component_clause,[status(thm)],[f5596])).
% 62.82/8.53 fof(f5607,plain,(
% 62.82/8.53 $false|sQ769_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f5598,f982])).
% 62.82/8.53 fof(f5608,plain,(
% 62.82/8.53 sQ769_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f5607])).
% 62.82/8.53 fof(f5632,definition,(
% 62.82/8.53 sQ775_spl <=> (l1_struct_0(sK10_skl))),
% 62.82/8.53 introduced(definition,[new_symbols(definition,[sQ775_spl])],[split_symbol_definition])).
% 62.82/8.53 fof(f5634,plain,(
% 62.82/8.53 ~l1_struct_0(sK10_skl)|sQ775_spl),
% 62.82/8.53 inference(component_clause,[status(thm)],[f5632])).
% 62.82/8.53 fof(f5643,plain,(
% 62.82/8.53 $false|sQ775_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f5634,f932])).
% 62.82/8.53 fof(f5644,plain,(
% 62.82/8.53 sQ775_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f5643])).
% 62.82/8.53 fof(f6244,plain,(
% 62.82/8.53 ![X0,X1,X2,X3]: (~v1_funct_1(X0)|~v1_funct_2(X0,k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k7_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_1(k9_conlat_1(sK0_skl))|~g3_lattices(k7_conlat_1(sK0_skl),X0,k9_conlat_1(sK0_skl))=g3_lattices(X1,X2,X3)|k7_conlat_1(sK0_skl)=X1|~v1_partfun1(k9_conlat_1(sK0_skl),k2_zfmisc_1(k7_conlat_1(sK0_skl),k7_conlat_1(sK0_skl)),k7_conlat_1(sK0_skl))|~sQ71_spl)),
% 62.82/8.53 inference(resolution,[status(thm)],[f2167,f812])).
% 62.82/8.53 fof(f6250,plain,(
% 62.82/8.53 sQ256_spl|~sQ69_spl|~sQ82_spl|~sQ71_spl),
% 62.82/8.53 inference(split_clause,[status(thm)],[f6244,f2158,f805,f879,f811])).
% 62.82/8.53 fof(f6847,plain,(
% 62.82/8.53 ~m2_relset_1(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),k7_conlat_1(sK0_skl))|sQ330_spl),
% 62.82/8.53 inference(resolution,[status(thm)],[f2734,f386])).
% 62.82/8.53 fof(f6848,plain,(
% 62.82/8.53 $false|~sQ286_spl|sQ330_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f6847,f2469])).
% 62.82/8.53 fof(f6849,plain,(
% 62.82/8.53 ~sQ286_spl|sQ330_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f6848])).
% 62.82/8.53 fof(f6860,plain,(
% 62.82/8.53 ~m2_relset_1(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),k7_conlat_1(sK0_skl))|sQ336_spl),
% 62.82/8.53 inference(resolution,[status(thm)],[f2772,f386])).
% 62.82/8.53 fof(f6861,plain,(
% 62.82/8.53 $false|~sQ284_spl|sQ336_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f6860,f2461])).
% 62.82/8.53 fof(f6862,plain,(
% 62.82/8.53 ~sQ284_spl|sQ336_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f6861])).
% 62.82/8.53 fof(f7163,definition,(
% 62.82/8.53 sQ960_spl <=> (v1_xboole_0(k1_zfmisc_1(u1_conlat_1(sK0_skl))))),
% 62.82/8.53 introduced(definition,[new_symbols(definition,[sQ960_spl])],[split_symbol_definition])).
% 62.82/8.53 fof(f7164,plain,(
% 62.82/8.53 v1_xboole_0(k1_zfmisc_1(u1_conlat_1(sK0_skl)))|~sQ960_spl),
% 62.82/8.53 inference(component_clause,[status(thm)],[f7163])).
% 62.82/8.53 fof(f7173,definition,(
% 62.82/8.53 sQ961_spl <=> (v1_xboole_0(k1_zfmisc_1(u2_conlat_1(sK0_skl))))),
% 62.82/8.53 introduced(definition,[new_symbols(definition,[sQ961_spl])],[split_symbol_definition])).
% 62.82/8.53 fof(f7174,plain,(
% 62.82/8.53 v1_xboole_0(k1_zfmisc_1(u2_conlat_1(sK0_skl)))|~sQ961_spl),
% 62.82/8.53 inference(component_clause,[status(thm)],[f7173])).
% 62.82/8.53 fof(f7255,definition,(
% 62.82/8.53 sQ966_spl <=> (v1_xboole_0(k1_zfmisc_1(u1_conlat_1(sK7_skl))))),
% 62.82/8.53 introduced(definition,[new_symbols(definition,[sQ966_spl])],[split_symbol_definition])).
% 62.82/8.53 fof(f7256,plain,(
% 62.82/8.53 v1_xboole_0(k1_zfmisc_1(u1_conlat_1(sK7_skl)))|~sQ966_spl),
% 62.82/8.53 inference(component_clause,[status(thm)],[f7255])).
% 62.82/8.53 fof(f7263,definition,(
% 62.82/8.53 sQ967_spl <=> (v1_xboole_0(k1_zfmisc_1(u1_conlat_1(sK4_skl))))),
% 62.82/8.53 introduced(definition,[new_symbols(definition,[sQ967_spl])],[split_symbol_definition])).
% 62.82/8.53 fof(f7264,plain,(
% 62.82/8.53 v1_xboole_0(k1_zfmisc_1(u1_conlat_1(sK4_skl)))|~sQ967_spl),
% 62.82/8.53 inference(component_clause,[status(thm)],[f7263])).
% 62.82/8.53 fof(f7271,definition,(
% 62.82/8.53 sQ968_spl <=> (v1_xboole_0(k1_zfmisc_1(u2_conlat_1(sK7_skl))))),
% 62.82/8.53 introduced(definition,[new_symbols(definition,[sQ968_spl])],[split_symbol_definition])).
% 62.82/8.53 fof(f7272,plain,(
% 62.82/8.53 v1_xboole_0(k1_zfmisc_1(u2_conlat_1(sK7_skl)))|~sQ968_spl),
% 62.82/8.53 inference(component_clause,[status(thm)],[f7271])).
% 62.82/8.53 fof(f7405,plain,(
% 62.82/8.53 $false|~sQ961_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f7174,f248])).
% 62.82/8.53 fof(f7406,plain,(
% 62.82/8.53 ~sQ961_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f7405])).
% 62.82/8.53 fof(f7407,plain,(
% 62.82/8.53 $false|~sQ960_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f7164,f248])).
% 62.82/8.53 fof(f7408,plain,(
% 62.82/8.53 ~sQ960_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f7407])).
% 62.82/8.53 fof(f7409,plain,(
% 62.82/8.53 $false|~sQ968_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f7272,f248])).
% 62.82/8.53 fof(f7410,plain,(
% 62.82/8.53 ~sQ968_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f7409])).
% 62.82/8.53 fof(f7411,plain,(
% 62.82/8.53 $false|~sQ966_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f7256,f248])).
% 62.82/8.53 fof(f7412,plain,(
% 62.82/8.53 ~sQ966_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f7411])).
% 62.82/8.53 fof(f7417,plain,(
% 62.82/8.53 $false|~sQ967_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f7264,f248])).
% 62.82/8.53 fof(f7418,plain,(
% 62.82/8.53 ~sQ967_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f7417])).
% 62.82/8.53 fof(f7596,definition,(
% 62.82/8.53 sQ1017_spl <=> (v1_xboole_0(k1_zfmisc_1(u2_conlat_1(sK4_skl))))),
% 62.82/8.53 introduced(definition,[new_symbols(definition,[sQ1017_spl])],[split_symbol_definition])).
% 62.82/8.53 fof(f7597,plain,(
% 62.82/8.53 v1_xboole_0(k1_zfmisc_1(u2_conlat_1(sK4_skl)))|~sQ1017_spl),
% 62.82/8.53 inference(component_clause,[status(thm)],[f7596])).
% 62.82/8.53 fof(f7604,plain,(
% 62.82/8.53 $false|~sQ1017_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f7597,f248])).
% 62.82/8.53 fof(f7605,plain,(
% 62.82/8.53 ~sQ1017_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f7604])).
% 62.82/8.53 fof(f8281,definition,(
% 62.82/8.53 sQ1120_spl <=> (v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(sK19_skl))))),
% 62.82/8.53 introduced(definition,[new_symbols(definition,[sQ1120_spl])],[split_symbol_definition])).
% 62.82/8.53 fof(f8282,plain,(
% 62.82/8.53 v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(sK19_skl)))|~sQ1120_spl),
% 62.82/8.53 inference(component_clause,[status(thm)],[f8281])).
% 62.82/8.53 fof(f8296,plain,(
% 62.82/8.53 $false|~sQ1120_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f8282,f248])).
% 62.82/8.53 fof(f8297,plain,(
% 62.82/8.53 ~sQ1120_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f8296])).
% 62.82/8.53 fof(f9524,definition,(
% 62.82/8.53 sQ1192_spl <=> (v1_xboole_0(k1_zfmisc_1(k7_conlat_1(sK7_skl))))),
% 62.82/8.53 introduced(definition,[new_symbols(definition,[sQ1192_spl])],[split_symbol_definition])).
% 62.82/8.53 fof(f9525,plain,(
% 62.82/8.53 v1_xboole_0(k1_zfmisc_1(k7_conlat_1(sK7_skl)))|~sQ1192_spl),
% 62.82/8.53 inference(component_clause,[status(thm)],[f9524])).
% 62.82/8.53 fof(f9532,plain,(
% 62.82/8.53 $false|~sQ1192_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f9525,f248])).
% 62.82/8.53 fof(f9533,plain,(
% 62.82/8.53 ~sQ1192_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f9532])).
% 62.82/8.53 fof(f11506,definition,(
% 62.82/8.53 sQ1381_spl <=> (v1_funct_1(sK17_skl(sK19_skl,k2_zfmisc_1(sK19_skl,sK19_skl))))),
% 62.82/8.53 introduced(definition,[new_symbols(definition,[sQ1381_spl])],[split_symbol_definition])).
% 62.82/8.53 fof(f11508,plain,(
% 62.82/8.53 ~v1_funct_1(sK17_skl(sK19_skl,k2_zfmisc_1(sK19_skl,sK19_skl)))|sQ1381_spl),
% 62.82/8.53 inference(component_clause,[status(thm)],[f11506])).
% 62.82/8.53 fof(f11509,definition,(
% 62.82/8.53 sQ1382_spl <=> (m1_relset_1(sK17_skl(sK19_skl,k2_zfmisc_1(sK19_skl,sK19_skl)),k2_zfmisc_1(sK19_skl,sK19_skl),sK19_skl))),
% 62.82/8.53 introduced(definition,[new_symbols(definition,[sQ1382_spl])],[split_symbol_definition])).
% 62.82/8.53 fof(f11511,plain,(
% 62.82/8.53 ~m1_relset_1(sK17_skl(sK19_skl,k2_zfmisc_1(sK19_skl,sK19_skl)),k2_zfmisc_1(sK19_skl,sK19_skl),sK19_skl)|sQ1382_spl),
% 62.82/8.53 inference(component_clause,[status(thm)],[f11509])).
% 62.82/8.53 fof(f11517,plain,(
% 62.82/8.53 $false|sQ1382_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f11511,f328])).
% 62.82/8.53 fof(f11518,plain,(
% 62.82/8.53 sQ1382_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f11517])).
% 62.82/8.53 fof(f11519,plain,(
% 62.82/8.53 $false|sQ1381_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f11508,f330])).
% 62.82/8.53 fof(f11520,plain,(
% 62.82/8.53 sQ1381_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f11519])).
% 62.82/8.53 fof(f12479,definition,(
% 62.82/8.53 sQ1528_spl <=> (v1_xboole_0(k1_zfmisc_1(u1_struct_0(k11_conlat_1(sK7_skl)))))),
% 62.82/8.53 introduced(definition,[new_symbols(definition,[sQ1528_spl])],[split_symbol_definition])).
% 62.82/8.53 fof(f12480,plain,(
% 62.82/8.53 v1_xboole_0(k1_zfmisc_1(u1_struct_0(k11_conlat_1(sK7_skl))))|~sQ1528_spl),
% 62.82/8.53 inference(component_clause,[status(thm)],[f12479])).
% 62.82/8.53 fof(f12494,plain,(
% 62.82/8.53 $false|~sQ1528_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f12480,f248])).
% 62.82/8.53 fof(f12495,plain,(
% 62.82/8.53 ~sQ1528_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f12494])).
% 62.82/8.53 fof(f12922,definition,(
% 62.82/8.53 sQ1580_spl <=> (v1_xboole_0(k1_zfmisc_1(sK13_skl(k1_zfmisc_1(u1_struct_0(k11_conlat_1(sK7_skl)))))))),
% 62.82/8.53 introduced(definition,[new_symbols(definition,[sQ1580_spl])],[split_symbol_definition])).
% 62.82/8.53 fof(f12923,plain,(
% 62.82/8.53 v1_xboole_0(k1_zfmisc_1(sK13_skl(k1_zfmisc_1(u1_struct_0(k11_conlat_1(sK7_skl))))))|~sQ1580_spl),
% 62.82/8.53 inference(component_clause,[status(thm)],[f12922])).
% 62.82/8.53 fof(f12937,plain,(
% 62.82/8.53 $false|~sQ1580_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f12923,f248])).
% 62.82/8.53 fof(f12938,plain,(
% 62.82/8.53 ~sQ1580_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f12937])).
% 62.82/8.53 fof(f13192,definition,(
% 62.82/8.53 sQ1605_spl <=> (v1_xboole_0(k1_zfmisc_1(sK3_skl(k1_zfmisc_1(u1_struct_0(k11_conlat_1(sK7_skl))),sK0_skl))))),
% 62.82/8.53 introduced(definition,[new_symbols(definition,[sQ1605_spl])],[split_symbol_definition])).
% 62.82/8.53 fof(f13193,plain,(
% 62.82/8.53 v1_xboole_0(k1_zfmisc_1(sK3_skl(k1_zfmisc_1(u1_struct_0(k11_conlat_1(sK7_skl))),sK0_skl)))|~sQ1605_spl),
% 62.82/8.53 inference(component_clause,[status(thm)],[f13192])).
% 62.82/8.53 fof(f13207,plain,(
% 62.82/8.53 $false|~sQ1605_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f13193,f248])).
% 62.82/8.53 fof(f13208,plain,(
% 62.82/8.53 ~sQ1605_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f13207])).
% 62.82/8.53 fof(f13288,definition,(
% 62.82/8.53 sQ1622_spl <=> (v1_xboole_0(k1_zfmisc_1(sK13_skl(sK18_skl(k1_zfmisc_1(u1_struct_0(k11_conlat_1(sK7_skl))))))))),
% 62.82/8.53 introduced(definition,[new_symbols(definition,[sQ1622_spl])],[split_symbol_definition])).
% 62.82/8.53 fof(f13289,plain,(
% 62.82/8.53 v1_xboole_0(k1_zfmisc_1(sK13_skl(sK18_skl(k1_zfmisc_1(u1_struct_0(k11_conlat_1(sK7_skl)))))))|~sQ1622_spl),
% 62.82/8.53 inference(component_clause,[status(thm)],[f13288])).
% 62.82/8.53 fof(f13303,plain,(
% 62.82/8.53 $false|~sQ1622_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f13289,f248])).
% 62.82/8.53 fof(f13304,plain,(
% 62.82/8.53 ~sQ1622_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f13303])).
% 62.82/8.53 fof(f13371,definition,(
% 62.82/8.53 sQ1634_spl <=> (l2_lattices(sK8_skl))),
% 62.82/8.53 introduced(definition,[new_symbols(definition,[sQ1634_spl])],[split_symbol_definition])).
% 62.82/8.53 fof(f13373,plain,(
% 62.82/8.53 ~l2_lattices(sK8_skl)|sQ1634_spl),
% 62.82/8.53 inference(component_clause,[status(thm)],[f13371])).
% 62.82/8.53 fof(f13388,definition,(
% 62.82/8.53 sQ1639_spl <=> (v1_funct_1(sK17_skl(u1_struct_0(sK8_skl),k2_zfmisc_1(u1_struct_0(sK8_skl),u1_struct_0(sK8_skl)))))),
% 62.82/8.53 introduced(definition,[new_symbols(definition,[sQ1639_spl])],[split_symbol_definition])).
% 62.82/8.53 fof(f13390,plain,(
% 62.82/8.53 ~v1_funct_1(sK17_skl(u1_struct_0(sK8_skl),k2_zfmisc_1(u1_struct_0(sK8_skl),u1_struct_0(sK8_skl))))|sQ1639_spl),
% 62.82/8.53 inference(component_clause,[status(thm)],[f13388])).
% 62.82/8.53 fof(f13391,definition,(
% 62.82/8.53 sQ1640_spl <=> (m1_relset_1(sK17_skl(u1_struct_0(sK8_skl),k2_zfmisc_1(u1_struct_0(sK8_skl),u1_struct_0(sK8_skl))),k2_zfmisc_1(u1_struct_0(sK8_skl),u1_struct_0(sK8_skl)),u1_struct_0(sK8_skl)))),
% 62.82/8.53 introduced(definition,[new_symbols(definition,[sQ1640_spl])],[split_symbol_definition])).
% 62.82/8.53 fof(f13393,plain,(
% 62.82/8.53 ~m1_relset_1(sK17_skl(u1_struct_0(sK8_skl),k2_zfmisc_1(u1_struct_0(sK8_skl),u1_struct_0(sK8_skl))),k2_zfmisc_1(u1_struct_0(sK8_skl),u1_struct_0(sK8_skl)),u1_struct_0(sK8_skl))|sQ1640_spl),
% 62.82/8.53 inference(component_clause,[status(thm)],[f13391])).
% 62.82/8.53 fof(f13399,plain,(
% 62.82/8.53 $false|sQ1640_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f13393,f328])).
% 62.82/8.53 fof(f13400,plain,(
% 62.82/8.53 sQ1640_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f13399])).
% 62.82/8.53 fof(f13401,plain,(
% 62.82/8.53 $false|sQ1639_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f13390,f330])).
% 62.82/8.53 fof(f13402,plain,(
% 62.82/8.53 sQ1639_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f13401])).
% 62.82/8.53 fof(f13403,plain,(
% 62.82/8.53 $false|sQ1634_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f13373,f215])).
% 62.82/8.53 fof(f13404,plain,(
% 62.82/8.53 sQ1634_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f13403])).
% 62.82/8.53 fof(f13415,definition,(
% 62.82/8.53 sQ1644_spl <=> (l2_lattices(sK10_skl))),
% 62.82/8.53 introduced(definition,[new_symbols(definition,[sQ1644_spl])],[split_symbol_definition])).
% 62.82/8.53 fof(f13417,plain,(
% 62.82/8.53 ~l2_lattices(sK10_skl)|sQ1644_spl),
% 62.82/8.53 inference(component_clause,[status(thm)],[f13415])).
% 62.82/8.53 fof(f13428,definition,(
% 62.82/8.53 sQ1648_spl <=> (l1_lattices(sK10_skl))),
% 62.82/8.53 introduced(definition,[new_symbols(definition,[sQ1648_spl])],[split_symbol_definition])).
% 62.82/8.53 fof(f13430,plain,(
% 62.82/8.53 ~l1_lattices(sK10_skl)|sQ1648_spl),
% 62.82/8.53 inference(component_clause,[status(thm)],[f13428])).
% 62.82/8.53 fof(f13432,definition,(
% 62.82/8.53 sQ1649_spl <=> (v1_funct_1(sK17_skl(u1_struct_0(sK10_skl),k2_zfmisc_1(u1_struct_0(sK10_skl),u1_struct_0(sK10_skl)))))),
% 62.82/8.53 introduced(definition,[new_symbols(definition,[sQ1649_spl])],[split_symbol_definition])).
% 62.82/8.53 fof(f13434,plain,(
% 62.82/8.53 ~v1_funct_1(sK17_skl(u1_struct_0(sK10_skl),k2_zfmisc_1(u1_struct_0(sK10_skl),u1_struct_0(sK10_skl))))|sQ1649_spl),
% 62.82/8.53 inference(component_clause,[status(thm)],[f13432])).
% 62.82/8.53 fof(f13435,definition,(
% 62.82/8.53 sQ1650_spl <=> (m1_relset_1(sK17_skl(u1_struct_0(sK10_skl),k2_zfmisc_1(u1_struct_0(sK10_skl),u1_struct_0(sK10_skl))),k2_zfmisc_1(u1_struct_0(sK10_skl),u1_struct_0(sK10_skl)),u1_struct_0(sK10_skl)))),
% 62.82/8.53 introduced(definition,[new_symbols(definition,[sQ1650_spl])],[split_symbol_definition])).
% 62.82/8.53 fof(f13437,plain,(
% 62.82/8.53 ~m1_relset_1(sK17_skl(u1_struct_0(sK10_skl),k2_zfmisc_1(u1_struct_0(sK10_skl),u1_struct_0(sK10_skl))),k2_zfmisc_1(u1_struct_0(sK10_skl),u1_struct_0(sK10_skl)),u1_struct_0(sK10_skl))|sQ1650_spl),
% 62.82/8.53 inference(component_clause,[status(thm)],[f13435])).
% 62.82/8.53 fof(f13443,plain,(
% 62.82/8.53 $false|sQ1650_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f13437,f328])).
% 62.82/8.53 fof(f13444,plain,(
% 62.82/8.53 sQ1650_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f13443])).
% 62.82/8.53 fof(f13445,plain,(
% 62.82/8.53 $false|sQ1649_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f13434,f330])).
% 62.82/8.53 fof(f13446,plain,(
% 62.82/8.53 sQ1649_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f13445])).
% 62.82/8.53 fof(f13447,plain,(
% 62.82/8.53 $false|sQ1648_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f13430,f482])).
% 62.82/8.53 fof(f13448,plain,(
% 62.82/8.53 sQ1648_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f13447])).
% 62.82/8.53 fof(f13449,plain,(
% 62.82/8.53 $false|sQ1644_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f13417,f488])).
% 62.82/8.53 fof(f13450,plain,(
% 62.82/8.53 sQ1644_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f13449])).
% 62.82/8.53 fof(f13573,definition,(
% 62.82/8.53 sQ1660_spl <=> (v1_funct_1(sK17_skl(u1_struct_0(sK15_skl),k2_zfmisc_1(u1_struct_0(sK15_skl),u1_struct_0(sK15_skl)))))),
% 62.82/8.53 introduced(definition,[new_symbols(definition,[sQ1660_spl])],[split_symbol_definition])).
% 62.82/8.53 fof(f13575,plain,(
% 62.82/8.53 ~v1_funct_1(sK17_skl(u1_struct_0(sK15_skl),k2_zfmisc_1(u1_struct_0(sK15_skl),u1_struct_0(sK15_skl))))|sQ1660_spl),
% 62.82/8.53 inference(component_clause,[status(thm)],[f13573])).
% 62.82/8.53 fof(f13576,definition,(
% 62.82/8.53 sQ1661_spl <=> (m1_relset_1(sK17_skl(u1_struct_0(sK15_skl),k2_zfmisc_1(u1_struct_0(sK15_skl),u1_struct_0(sK15_skl))),k2_zfmisc_1(u1_struct_0(sK15_skl),u1_struct_0(sK15_skl)),u1_struct_0(sK15_skl)))),
% 62.82/8.53 introduced(definition,[new_symbols(definition,[sQ1661_spl])],[split_symbol_definition])).
% 62.82/8.53 fof(f13578,plain,(
% 62.82/8.53 ~m1_relset_1(sK17_skl(u1_struct_0(sK15_skl),k2_zfmisc_1(u1_struct_0(sK15_skl),u1_struct_0(sK15_skl))),k2_zfmisc_1(u1_struct_0(sK15_skl),u1_struct_0(sK15_skl)),u1_struct_0(sK15_skl))|sQ1661_spl),
% 62.82/8.53 inference(component_clause,[status(thm)],[f13576])).
% 62.82/8.53 fof(f13584,plain,(
% 62.82/8.53 $false|sQ1661_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f13578,f328])).
% 62.82/8.53 fof(f13585,plain,(
% 62.82/8.53 sQ1661_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f13584])).
% 62.82/8.53 fof(f13586,plain,(
% 62.82/8.53 $false|sQ1660_spl),
% 62.82/8.53 inference(forward_subsumption_resolution,[status(thm)],[f13575,f330])).
% 62.82/8.53 fof(f13587,plain,(
% 62.82/8.53 sQ1660_spl),
% 62.82/8.53 inference(contradiction_clause,[status(thm)],[f13586])).
% 62.82/8.53 fof(f14089,plain,(
% 62.82/8.53 v1_xboole_0(u1_conlat_1(sK0_skl))|~v1_funct_1(k4_conlat_2(sK0_skl))|~v1_funct_2(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),k7_conlat_1(sK0_skl))|~m1_relset_1(k4_conlat_2(sK0_skl),u1_conlat_1(sK0_skl),k7_conlat_1(sK0_skl))|~m1_subset_1(sK1_skl,u1_conlat_1(sK0_skl))|~m1_conlat_1(k7_conlat_1(sK0_skl),sK0_skl)|~sQ166_spl|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl|sQ2_spl),
% 62.82/8.53 inference(resolution,[status(thm)],[f1561,f2386])).
% 62.82/8.53 fof(f14090,plain,(
% 62.82/8.53 v1_xboole_0(u2_conlat_1(sK0_skl))|~v1_funct_1(k5_conlat_2(sK0_skl))|~v1_funct_2(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),k7_conlat_1(sK0_skl))|~m1_relset_1(k5_conlat_2(sK0_skl),u2_conlat_1(sK0_skl),k7_conlat_1(sK0_skl))|~m1_subset_1(sK2_skl,u2_conlat_1(sK0_skl))|~m1_conlat_1(k7_conlat_1(sK0_skl),sK0_skl)|~sQ166_spl|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl|sQ5_spl),
% 62.82/8.53 inference(resolution,[status(thm)],[f1561,f2388])).
% 62.82/8.53 fof(f14093,plain,(
% 62.82/8.53 sQ147_spl|~sQ212_spl|~sQ287_spl|~sQ330_spl|~sQ215_spl|~sQ19_spl|~sQ166_spl|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl|sQ2_spl),
% 62.82/8.53 inference(split_clause,[status(thm)],[f14089,f1405,f1831,f2472,f2732,f1840,f541,f1560,f530,f773,f2329,f822,f418])).
% 62.82/8.53 fof(f14094,plain,(
% 62.82/8.53 sQ145_spl|~sQ217_spl|~sQ285_spl|~sQ336_spl|~sQ220_spl|~sQ19_spl|~sQ166_spl|~sQ17_spl|~sQ64_spl|~sQ277_spl|~sQ74_spl|sQ5_spl),
% 62.82/8.53 inference(split_clause,[status(thm)],[f14090,f1398,f1847,f2464,f2770,f1856,f541,f1560,f530,f773,f2329,f822,f427])).
% 62.82/8.53 fof(f14103,plain,(
% 62.82/8.53 $false),
% 62.82/8.53 inference(sat_refutation,[status(thm)],[f430,f533,f536,f544,f546,f776,f817,f825,f849,f862,f867,f869,f885,f955,f965,f1001,f1006,f1015,f1017,f1056,f1073,f1428,f1437,f1443,f1531,f1553,f1563,f1846,f1859,f1861,f1863,f1865,f1867,f2078,f2079,f2082,f2090,f2332,f2355,f2426,f2463,f2467,f2471,f2475,f2639,f2992,f2994,f2996,f2998,f3062,f3388,f3390,f3392,f3588,f3590,f3592,f3594,f3774,f3776,f3778,f3780,f4404,f4407,f5608,f5644,f6250,f6849,f6862,f7406,f7408,f7410,f7412,f7418,f7605,f8297,f9533,f11518,f11520,f12495,f12938,f13208,f13304,f13400,f13402,f13404,f13444,f13446,f13448,f13450,f13585,f13587,f14093,f14094])).
% 62.82/8.55 % SZS output end CNFRefutation for theBenchmark.p
% 62.82/8.61 % Elapsed time: 8.154888 seconds
% 62.82/8.61 % CPU time: 63.940793 seconds
% 62.82/8.61 % Total memory used: 482.452 MB
% 62.82/8.61 % Net memory used: 464.210 MB
%------------------------------------------------------------------------------