%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT312+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 : n010.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:38 PM UTC 2026
% Result : Theorem 44.82s 6.29s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT312+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.50 % Computer : n010.cluster.edu
% 0.09/0.50 % Model : x86_64 x86_64
% 0.09/0.50 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.50 % Memory : 8046.5625MB
% 0.09/0.50 % OS : Linux 6.8.0-71-generic
% 0.09/0.50 % CPULimit : 300
% 0.09/0.50 % WCLimit : 300
% 0.09/0.50 % DateTime : Sun Sep 20 23:33:56 UTC 2026
% 0.09/0.51 % CPUTime :
% 0.09/0.52 % Drodi V4.1.1
% 44.82/6.29 % Refutation found
% 44.82/6.29 % SZS status Theorem for theBenchmark: Theorem is valid
% 44.82/6.29 % SZS output start CNFRefutation for theBenchmark
% 44.82/6.29 fof(f1,conjecture,(
% 44.82/6.29 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> (! [C] :( ( ~ v1_xboole_0(C)& m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) )=> ( r1_filter_2(u1_struct_0(A),C,k6_domain_1(u1_struct_0(A),B))=> r1_filter_2(u1_struct_0(A),k19_filter_2(A,C),k18_filter_2(A,B)) ) ) )) )) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f2,negated_conjecture,(
% 44.82/6.29 ~((! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> (! [C] :( ( ~ v1_xboole_0(C)& m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) )=> ( r1_filter_2(u1_struct_0(A),C,k6_domain_1(u1_struct_0(A),B))=> r1_filter_2(u1_struct_0(A),k19_filter_2(A,C),k18_filter_2(A,B)) ) ) )) )) ))),
% 44.82/6.29 inference(negated_conjecture,[status(cth)],[f1])).
% 44.82/6.29 fof(f6,axiom,(
% 44.82/6.29 (! [A] :( l3_lattices(A)=> ( ( ~ v3_struct_0(A)& v10_lattices(A) )=> ( ~ v3_struct_0(A)& v4_lattices(A)& v5_lattices(A)& v6_lattices(A)& v7_lattices(A)& v8_lattices(A)& v9_lattices(A) ) ) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f7,axiom,(
% 44.82/6.29 (! [A] :( ~ v1_realset1(A)=> ~ v1_xboole_0(A) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f13,axiom,(
% 44.82/6.29 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> k5_filter_2(A,B) = B ) )) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f14,axiom,(
% 44.82/6.29 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))=> k7_filter_2(A,B) = B ) )) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f16,axiom,(
% 44.82/6.29 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> k18_filter_2(A,B) = a_2_0_filter_2(A,B) ) )) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f18,axiom,(
% 44.82/6.29 (! [A,B] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A)& m1_subset_1(B,u1_struct_0(A)) )=> m2_filter_2(k18_filter_2(A,B),A) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f20,axiom,(
% 44.82/6.29 (! [A] :( l3_lattices(A)=> ( v3_lattices(k1_lattice2(A))& l3_lattices(k1_lattice2(A)) ) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f29,axiom,(
% 44.82/6.29 (! [A,B] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A)& m1_subset_1(B,u1_struct_0(A)) )=> m1_subset_1(k5_filter_2(A,B),u1_struct_0(k1_lattice2(A))) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f30,axiom,(
% 44.82/6.29 (! [A,B] :( ( ~ v1_xboole_0(A)& m1_subset_1(B,A) )=> m1_subset_1(k6_domain_1(A,B),k1_zfmisc_1(A)) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f31,axiom,(
% 44.82/6.29 (! [A,B] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A)& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )=> m1_subset_1(k7_filter_2(A,B),k1_zfmisc_1(u1_struct_0(k1_lattice2(A)))) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f33,axiom,(
% 44.82/6.29 (! [A] :( l1_lattices(A)=> l1_struct_0(A) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f35,axiom,(
% 44.82/6.29 (! [A] :( l2_lattices(A)=> l1_struct_0(A) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f36,axiom,(
% 44.82/6.29 (! [A] :( l3_lattices(A)=> ( l1_lattices(A)& l2_lattices(A) ) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f41,axiom,(
% 44.82/6.29 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m2_filter_2(B,A)=> ( ~ v1_xboole_0(B)& m2_lattice4(B,A) ) ) )) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f42,axiom,(
% 44.82/6.29 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m2_lattice4(B,A)=> m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) )) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f44,axiom,(
% 44.82/6.29 (! [A] :( l1_lattices(A)=> ( v1_funct_1(u1_lattices(A))& v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))& m2_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f46,axiom,(
% 44.82/6.29 (! [A] :( l2_lattices(A)=> ( v1_funct_1(u2_lattices(A))& v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))& m2_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f47,axiom,(
% 44.82/6.29 (? [A] : l1_lattices(A) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f48,axiom,(
% 44.82/6.29 (? [A] : l1_struct_0(A) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f49,axiom,(
% 44.82/6.29 (? [A] : l2_lattices(A) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f50,axiom,(
% 44.82/6.29 (? [A] : l3_lattices(A) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f54,axiom,(
% 44.82/6.29 (! [A] :(? [B] : m1_subset_1(B,A) ))),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f59,axiom,(
% 44.82/6.29 (! [A] :( ( ~ v3_struct_0(A)& l3_lattices(A) )=> ( ~ v3_struct_0(k1_lattice2(A))& v3_lattices(k1_lattice2(A)) ) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f60,axiom,(
% 44.82/6.29 (! [A] :( ( ~ v3_struct_0(A)& l1_struct_0(A) )=> ~ v1_xboole_0(u1_struct_0(A)) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f61,axiom,(
% 44.82/6.29 (! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f65,axiom,(
% 44.82/6.29 (! [A] : ~ v1_xboole_0(k1_tarski(A)) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f72,axiom,(
% 44.82/6.29 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> ( ~ v3_struct_0(k1_lattice2(A))& v3_lattices(k1_lattice2(A))& v4_lattices(k1_lattice2(A))& v5_lattices(k1_lattice2(A))& v6_lattices(k1_lattice2(A))& v7_lattices(k1_lattice2(A))& v8_lattices(k1_lattice2(A))& v9_lattices(k1_lattice2(A))& v10_lattices(k1_lattice2(A)) ) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f74,axiom,(
% 44.82/6.29 (! [A,B,C] :( ( ~ v3_struct_0(B)& v10_lattices(B)& l3_lattices(B)& m1_subset_1(C,u1_struct_0(B)) )=> ( r2_hidden(A,a_2_0_filter_2(B,C))<=> (? [D] :( m1_subset_1(D,u1_struct_0(B))& A = D& r3_lattices(B,D,C) ) )) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f78,axiom,(
% 44.82/6.29 (? [A] :( ~ v1_xboole_0(A)& v1_realset1(A) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f79,axiom,(
% 44.82/6.29 (! [A] :( ~ v1_xboole_0(A)=> (? [B] :( m1_subset_1(B,k1_zfmisc_1(A))& ~ v1_xboole_0(B) ) )) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f80,axiom,(
% 44.82/6.29 (? [A] : v1_xboole_0(A) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f82,axiom,(
% 44.82/6.29 (? [A] :( ~ v1_xboole_0(A)& ~ v1_realset1(A) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f84,axiom,(
% 44.82/6.29 (? [A] : ~ v1_xboole_0(A) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f86,axiom,(
% 44.82/6.29 (? [A] :( l3_lattices(A)& v3_lattices(A) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f87,axiom,(
% 44.82/6.29 (? [A] :( l1_struct_0(A)& ~ v3_struct_0(A) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f89,axiom,(
% 44.82/6.29 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v3_lattices(A) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f91,axiom,(
% 44.82/6.29 (! [A,B] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A)& m1_subset_1(B,u1_struct_0(A)) )=> k2_filter_2(A,B) = k2_filter_0(A,B) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f92,axiom,(
% 44.82/6.29 (! [A,B] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A)& ~ v1_xboole_0(B)& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )=> k3_filter_2(A,B) = k3_filter_0(A,B) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f93,axiom,(
% 44.82/6.29 (! [A,B] :( ( ~ v1_xboole_0(A)& m1_subset_1(B,A) )=> k6_domain_1(A,B) = k1_tarski(B) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f95,axiom,(
% 44.82/6.29 (! [A,B,C] :( m2_relset_1(C,A,B)<=> m1_relset_1(C,A,B) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f96,axiom,(
% 44.82/6.29 (! [A,B,C] :( ( ~ v1_xboole_0(A)& m1_subset_1(B,k1_zfmisc_1(A))& m1_subset_1(C,k1_zfmisc_1(A)) )=> ( r1_filter_2(A,B,C)<=> B = C ) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f100,axiom,(
% 44.82/6.29 (! [A,B,C] :( ( ~ v3_struct_0(A)& v6_lattices(A)& v8_lattices(A)& v9_lattices(A)& l3_lattices(A)& m1_subset_1(B,u1_struct_0(A))& m1_subset_1(C,u1_struct_0(A)) )=> r3_lattices(A,B,B) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f103,axiom,(
% 44.82/6.29 (! [A,B] :( m1_subset_1(A,B)=> ( v1_xboole_0(B)| r2_hidden(A,B) ) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f105,axiom,(
% 44.82/6.29 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> (! [C] :( ( ~ v1_xboole_0(C)& m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) )=> ( C = k6_domain_1(u1_struct_0(A),B)=> k3_filter_0(A,C) = k2_filter_0(A,B) ) ) )) )) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f106,axiom,(
% 44.82/6.29 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> ( k18_filter_2(A,B) = k2_filter_2(k1_lattice2(A),k5_filter_2(A,B))& k18_filter_2(k1_lattice2(A),k5_filter_2(A,B)) = k2_filter_2(A,B) ) ) )) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f107,axiom,(
% 44.82/6.29 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( ( ~ v1_xboole_0(B)& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) )=> (! [C] :( ( ~ v1_xboole_0(C)& m1_subset_1(C,k1_zfmisc_1(u1_struct_0(k1_lattice2(A)))) )=> ( k3_filter_2(k1_lattice2(A),k7_filter_2(A,B)) = k19_filter_2(A,B)& k3_filter_2(A,B) = k19_filter_2(k1_lattice2(A),k7_filter_2(A,B))& k3_filter_2(A,k8_filter_2(A,C)) = k19_filter_2(k1_lattice2(A),C)& k3_filter_2(k1_lattice2(A),C) = k19_filter_2(A,k8_filter_2(A,C)) ) ) )) )) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f110,axiom,(
% 44.82/6.29 (! [A,B,C] :~ ( r2_hidden(A,B)& m1_subset_1(B,k1_zfmisc_1(C))& v1_xboole_0(C) ) )),
% 44.82/6.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 44.82/6.29 fof(f114,plain,(
% 44.82/6.29 (?[A]: (((~v3_struct_0(A)&v10_lattices(A))&l3_lattices(A))&(?[B]: (m1_subset_1(B,u1_struct_0(A))&(?[C]: ((~v1_xboole_0(C)&m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))))&(r1_filter_2(u1_struct_0(A),C,k6_domain_1(u1_struct_0(A),B))&~r1_filter_2(u1_struct_0(A),k19_filter_2(A,C),k18_filter_2(A,B)))))))))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 44.82/6.29 fof(f115,plain,(
% 44.82/6.29 (((~v3_struct_0(sK0_skl)&v10_lattices(sK0_skl))&l3_lattices(sK0_skl))&(m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))&((~v1_xboole_0(sK2_skl)&m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl))))&(r1_filter_2(u1_struct_0(sK0_skl),sK2_skl,k6_domain_1(u1_struct_0(sK0_skl),sK1_skl))&~r1_filter_2(u1_struct_0(sK0_skl),k19_filter_2(sK0_skl,sK2_skl),k18_filter_2(sK0_skl,sK1_skl))))))),
% 44.82/6.29 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)],[f114])).
% 44.82/6.29 fof(f116,plain,(
% 44.82/6.29 ~v3_struct_0(sK0_skl)),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f115])).
% 44.82/6.29 fof(f117,plain,(
% 44.82/6.29 v10_lattices(sK0_skl)),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f115])).
% 44.82/6.29 fof(f118,plain,(
% 44.82/6.29 l3_lattices(sK0_skl)),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f115])).
% 44.82/6.29 fof(f119,plain,(
% 44.82/6.29 m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f115])).
% 44.82/6.29 fof(f120,plain,(
% 44.82/6.29 ~v1_xboole_0(sK2_skl)),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f115])).
% 44.82/6.29 fof(f121,plain,(
% 44.82/6.29 m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f115])).
% 44.82/6.29 fof(f122,plain,(
% 44.82/6.29 r1_filter_2(u1_struct_0(sK0_skl),sK2_skl,k6_domain_1(u1_struct_0(sK0_skl),sK1_skl))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f115])).
% 44.82/6.29 fof(f123,plain,(
% 44.82/6.29 ~r1_filter_2(u1_struct_0(sK0_skl),k19_filter_2(sK0_skl,sK2_skl),k18_filter_2(sK0_skl,sK1_skl))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f115])).
% 44.82/6.29 fof(f130,plain,(
% 44.82/6.29 ![A]: (~l3_lattices(A)|((v3_struct_0(A)|~v10_lattices(A))|((((((~v3_struct_0(A)&v4_lattices(A))&v5_lattices(A))&v6_lattices(A))&v7_lattices(A))&v8_lattices(A))&v9_lattices(A))))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 44.82/6.29 fof(f134,plain,(
% 44.82/6.29 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v10_lattices(X0)|v6_lattices(X0))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f130])).
% 44.82/6.29 fof(f136,plain,(
% 44.82/6.29 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v10_lattices(X0)|v8_lattices(X0))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f130])).
% 44.82/6.29 fof(f137,plain,(
% 44.82/6.29 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v10_lattices(X0)|v9_lattices(X0))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f130])).
% 44.82/6.29 fof(f138,plain,(
% 44.82/6.29 ![A]: (v1_realset1(A)|~v1_xboole_0(A))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 44.82/6.29 fof(f139,plain,(
% 44.82/6.29 ![X0]: (v1_realset1(X0)|~v1_xboole_0(X0))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f138])).
% 44.82/6.29 fof(f154,plain,(
% 44.82/6.29 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m1_subset_1(B,u1_struct_0(A))|k5_filter_2(A,B)=B)))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 44.82/6.29 fof(f155,plain,(
% 44.82/6.29 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|k5_filter_2(X0,X1)=X1)),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f154])).
% 44.82/6.29 fof(f156,plain,(
% 44.82/6.29 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))|k7_filter_2(A,B)=B)))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 44.82/6.29 fof(f157,plain,(
% 44.82/6.29 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|k7_filter_2(X0,X1)=X1)),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f156])).
% 44.82/6.29 fof(f160,plain,(
% 44.82/6.29 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m1_subset_1(B,u1_struct_0(A))|k18_filter_2(A,B)=a_2_0_filter_2(A,B))))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 44.82/6.29 fof(f161,plain,(
% 44.82/6.29 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|k18_filter_2(X0,X1)=a_2_0_filter_2(X0,X1))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f160])).
% 44.82/6.29 fof(f165,plain,(
% 44.82/6.29 ![A,B]: ((((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|~m1_subset_1(B,u1_struct_0(A)))|m2_filter_2(k18_filter_2(A,B),A))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 44.82/6.29 fof(f166,plain,(
% 44.82/6.29 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|m2_filter_2(k18_filter_2(X0,X1),X0))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f165])).
% 44.82/6.29 fof(f169,plain,(
% 44.82/6.29 ![A]: (~l3_lattices(A)|(v3_lattices(k1_lattice2(A))&l3_lattices(k1_lattice2(A))))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 44.82/6.29 fof(f171,plain,(
% 44.82/6.29 ![X0]: (~l3_lattices(X0)|l3_lattices(k1_lattice2(X0)))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f169])).
% 44.82/6.29 fof(f180,plain,(
% 44.82/6.29 ![A,B]: ((((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|~m1_subset_1(B,u1_struct_0(A)))|m1_subset_1(k5_filter_2(A,B),u1_struct_0(k1_lattice2(A))))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 44.82/6.29 fof(f181,plain,(
% 44.82/6.29 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|m1_subset_1(k5_filter_2(X0,X1),u1_struct_0(k1_lattice2(X0))))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f180])).
% 44.82/6.29 fof(f182,plain,(
% 44.82/6.29 ![A,B]: ((v1_xboole_0(A)|~m1_subset_1(B,A))|m1_subset_1(k6_domain_1(A,B),k1_zfmisc_1(A)))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 44.82/6.29 fof(f183,plain,(
% 44.82/6.29 ![X0,X1]: (v1_xboole_0(X0)|~m1_subset_1(X1,X0)|m1_subset_1(k6_domain_1(X0,X1),k1_zfmisc_1(X0)))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f182])).
% 44.82/6.29 fof(f184,plain,(
% 44.82/6.29 ![A,B]: ((((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))))|m1_subset_1(k7_filter_2(A,B),k1_zfmisc_1(u1_struct_0(k1_lattice2(A)))))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 44.82/6.29 fof(f185,plain,(
% 44.82/6.29 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|m1_subset_1(k7_filter_2(X0,X1),k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f184])).
% 44.82/6.29 fof(f188,plain,(
% 44.82/6.29 ![A]: (~l1_lattices(A)|l1_struct_0(A))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 44.82/6.29 fof(f189,plain,(
% 44.82/6.29 ![X0]: (~l1_lattices(X0)|l1_struct_0(X0))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f188])).
% 44.82/6.29 fof(f190,plain,(
% 44.82/6.29 ![A]: (~l2_lattices(A)|l1_struct_0(A))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 44.82/6.29 fof(f191,plain,(
% 44.82/6.29 ![X0]: (~l2_lattices(X0)|l1_struct_0(X0))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f190])).
% 44.82/6.29 fof(f192,plain,(
% 44.82/6.29 ![A]: (~l3_lattices(A)|(l1_lattices(A)&l2_lattices(A)))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 44.82/6.29 fof(f193,plain,(
% 44.82/6.29 ![X0]: (~l3_lattices(X0)|l1_lattices(X0))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f192])).
% 44.82/6.29 fof(f194,plain,(
% 44.82/6.29 ![X0]: (~l3_lattices(X0)|l2_lattices(X0))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f192])).
% 44.82/6.29 fof(f201,plain,(
% 44.82/6.29 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m2_filter_2(B,A)|(~v1_xboole_0(B)&m2_lattice4(B,A)))))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 44.82/6.29 fof(f203,plain,(
% 44.82/6.29 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_filter_2(X1,X0)|m2_lattice4(X1,X0))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f201])).
% 44.82/6.29 fof(f204,plain,(
% 44.82/6.29 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m2_lattice4(B,A)|m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))))))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 44.82/6.29 fof(f205,plain,(
% 44.82/6.29 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_lattice4(X1,X0)|m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f204])).
% 44.82/6.29 fof(f208,plain,(
% 44.82/6.29 ![A]: (~l1_lattices(A)|((v1_funct_1(u1_lattices(A))&v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)))&m2_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f44])).
% 44.82/6.29 fof(f211,plain,(
% 44.82/6.29 ![X0]: (~l1_lattices(X0)|m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f208])).
% 44.82/6.29 fof(f212,plain,(
% 44.82/6.29 ![A]: (~l2_lattices(A)|((v1_funct_1(u2_lattices(A))&v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)))&m2_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 44.82/6.29 fof(f215,plain,(
% 44.82/6.29 ![X0]: (~l2_lattices(X0)|m2_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f212])).
% 44.82/6.29 fof(f216,plain,(
% 44.82/6.29 l1_lattices(sK3_skl)),
% 44.82/6.29 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(A,sK3_skl)],[f47])).
% 44.82/6.29 fof(f217,plain,(
% 44.82/6.29 l1_lattices(sK3_skl)),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f216])).
% 44.82/6.29 fof(f218,plain,(
% 44.82/6.29 l1_struct_0(sK4_skl)),
% 44.82/6.29 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(A,sK4_skl)],[f48])).
% 44.82/6.29 fof(f219,plain,(
% 44.82/6.29 l1_struct_0(sK4_skl)),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f218])).
% 44.82/6.29 fof(f220,plain,(
% 44.82/6.29 l2_lattices(sK5_skl)),
% 44.82/6.29 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(A,sK5_skl)],[f49])).
% 44.82/6.29 fof(f221,plain,(
% 44.82/6.29 l2_lattices(sK5_skl)),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f220])).
% 44.82/6.29 fof(f222,plain,(
% 44.82/6.29 l3_lattices(sK6_skl)),
% 44.82/6.29 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(A,sK6_skl)],[f50])).
% 44.82/6.29 fof(f223,plain,(
% 44.82/6.29 l3_lattices(sK6_skl)),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f222])).
% 44.82/6.29 fof(f232,plain,(
% 44.82/6.29 ![A]: m1_subset_1(sK10_skl(A),A)),
% 44.82/6.29 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(B,sK10_skl(A))],[f54])).
% 44.82/6.29 fof(f233,plain,(
% 44.82/6.29 ![X0]: (m1_subset_1(sK10_skl(X0),X0))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f232])).
% 44.82/6.29 fof(f244,plain,(
% 44.82/6.29 ![A]: ((v3_struct_0(A)|~l3_lattices(A))|(~v3_struct_0(k1_lattice2(A))&v3_lattices(k1_lattice2(A))))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f59])).
% 44.82/6.29 fof(f245,plain,(
% 44.82/6.29 ![X0]: (v3_struct_0(X0)|~l3_lattices(X0)|~v3_struct_0(k1_lattice2(X0)))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f244])).
% 44.82/6.29 fof(f247,plain,(
% 44.82/6.29 ![A]: ((v3_struct_0(A)|~l1_struct_0(A))|~v1_xboole_0(u1_struct_0(A)))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f60])).
% 44.82/6.29 fof(f248,plain,(
% 44.82/6.29 ![X0]: (v3_struct_0(X0)|~l1_struct_0(X0)|~v1_xboole_0(u1_struct_0(X0)))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f247])).
% 44.82/6.29 fof(f249,plain,(
% 44.82/6.29 ![X0]: (~v1_xboole_0(k1_zfmisc_1(X0)))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f61])).
% 44.82/6.29 fof(f259,plain,(
% 44.82/6.29 ![X0]: (~v1_xboole_0(k1_tarski(X0)))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f65])).
% 44.82/6.29 fof(f287,plain,(
% 44.82/6.29 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|((((((((~v3_struct_0(k1_lattice2(A))&v3_lattices(k1_lattice2(A)))&v4_lattices(k1_lattice2(A)))&v5_lattices(k1_lattice2(A)))&v6_lattices(k1_lattice2(A)))&v7_lattices(k1_lattice2(A)))&v8_lattices(k1_lattice2(A)))&v9_lattices(k1_lattice2(A)))&v10_lattices(k1_lattice2(A))))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f72])).
% 44.82/6.29 fof(f296,plain,(
% 44.82/6.29 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v10_lattices(k1_lattice2(X0)))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f287])).
% 44.82/6.29 fof(f305,plain,(
% 44.82/6.29 ![A,B,C]: ((((v3_struct_0(B)|~v10_lattices(B))|~l3_lattices(B))|~m1_subset_1(C,u1_struct_0(B)))|(r2_hidden(A,a_2_0_filter_2(B,C))<=>(?[D]: ((m1_subset_1(D,u1_struct_0(B))&A=D)&r3_lattices(B,D,C)))))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f74])).
% 44.82/6.29 fof(f306,plain,(
% 44.82/6.29 ![A,B,C]: ((((v3_struct_0(B)|~v10_lattices(B))|~l3_lattices(B))|~m1_subset_1(C,u1_struct_0(B)))|((~r2_hidden(A,a_2_0_filter_2(B,C))|(?[D]: ((m1_subset_1(D,u1_struct_0(B))&A=D)&r3_lattices(B,D,C))))&(r2_hidden(A,a_2_0_filter_2(B,C))|(![D]: ((~m1_subset_1(D,u1_struct_0(B))|~A=D)|~r3_lattices(B,D,C))))))),
% 44.82/6.29 inference(NNF_transformation,[status(thm)],[f305])).
% 44.82/6.29 fof(f307,plain,(
% 44.82/6.29 ![B,C]: ((((v3_struct_0(B)|~v10_lattices(B))|~l3_lattices(B))|~m1_subset_1(C,u1_struct_0(B)))|((![A]: (~r2_hidden(A,a_2_0_filter_2(B,C))|(?[D]: ((m1_subset_1(D,u1_struct_0(B))&A=D)&r3_lattices(B,D,C)))))&(![A]: (r2_hidden(A,a_2_0_filter_2(B,C))|(![D]: ((~m1_subset_1(D,u1_struct_0(B))|~A=D)|~r3_lattices(B,D,C)))))))),
% 44.82/6.29 inference(miniscoping,[status(thm)],[f306])).
% 44.82/6.29 fof(f308,plain,(
% 44.82/6.29 ![B,C]: ((((v3_struct_0(B)|~v10_lattices(B))|~l3_lattices(B))|~m1_subset_1(C,u1_struct_0(B)))|((![A]: (~r2_hidden(A,a_2_0_filter_2(B,C))|((m1_subset_1(sK15_skl(A,C,B),u1_struct_0(B))&A=sK15_skl(A,C,B))&r3_lattices(B,sK15_skl(A,C,B),C))))&(![A]: (r2_hidden(A,a_2_0_filter_2(B,C))|(![D]: ((~m1_subset_1(D,u1_struct_0(B))|~A=D)|~r3_lattices(B,D,C)))))))),
% 44.82/6.29 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(D,sK15_skl(A,C,B))],[f307])).
% 44.82/6.29 fof(f312,plain,(
% 44.82/6.29 ![X0,X1,X2,X3]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|r2_hidden(X2,a_2_0_filter_2(X0,X1))|~m1_subset_1(X3,u1_struct_0(X0))|~X2=X3|~r3_lattices(X0,X3,X1))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f308])).
% 44.82/6.29 fof(f324,plain,(
% 44.82/6.29 (~v1_xboole_0(sK18_skl)&v1_realset1(sK18_skl))),
% 44.82/6.29 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(A,sK18_skl)],[f78])).
% 44.82/6.29 fof(f325,plain,(
% 44.82/6.29 ~v1_xboole_0(sK18_skl)),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f324])).
% 44.82/6.29 fof(f327,plain,(
% 44.82/6.29 ![A]: (v1_xboole_0(A)|(?[B]: (m1_subset_1(B,k1_zfmisc_1(A))&~v1_xboole_0(B))))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f79])).
% 44.82/6.29 fof(f328,plain,(
% 44.82/6.29 ![A]: (v1_xboole_0(A)|(m1_subset_1(sK19_skl(A),k1_zfmisc_1(A))&~v1_xboole_0(sK19_skl(A))))),
% 44.82/6.29 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl]),skolemize(B,sK19_skl(A))],[f327])).
% 44.82/6.29 fof(f329,plain,(
% 44.82/6.29 ![X0]: (v1_xboole_0(X0)|m1_subset_1(sK19_skl(X0),k1_zfmisc_1(X0)))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f328])).
% 44.82/6.29 fof(f330,plain,(
% 44.82/6.29 ![X0]: (v1_xboole_0(X0)|~v1_xboole_0(sK19_skl(X0)))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f328])).
% 44.82/6.29 fof(f331,plain,(
% 44.82/6.29 v1_xboole_0(sK20_skl)),
% 44.82/6.29 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(A,sK20_skl)],[f80])).
% 44.82/6.29 fof(f332,plain,(
% 44.82/6.29 v1_xboole_0(sK20_skl)),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f331])).
% 44.82/6.29 fof(f337,plain,(
% 44.82/6.29 (~v1_xboole_0(sK22_skl)&~v1_realset1(sK22_skl))),
% 44.82/6.29 inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(A,sK22_skl)],[f82])).
% 44.82/6.29 fof(f338,plain,(
% 44.82/6.29 ~v1_xboole_0(sK22_skl)),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f337])).
% 44.82/6.29 fof(f339,plain,(
% 44.82/6.29 ~v1_realset1(sK22_skl)),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f337])).
% 44.82/6.29 fof(f343,plain,(
% 44.82/6.29 ~v1_xboole_0(sK24_skl)),
% 44.82/6.29 inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(A,sK24_skl)],[f84])).
% 44.82/6.29 fof(f344,plain,(
% 44.82/6.29 ~v1_xboole_0(sK24_skl)),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f343])).
% 44.82/6.29 fof(f349,plain,(
% 44.82/6.29 (l3_lattices(sK26_skl)&v3_lattices(sK26_skl))),
% 44.82/6.29 inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl]),skolemize(A,sK26_skl)],[f86])).
% 44.82/6.29 fof(f350,plain,(
% 44.82/6.29 l3_lattices(sK26_skl)),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f349])).
% 44.82/6.29 fof(f352,plain,(
% 44.82/6.29 (l1_struct_0(sK27_skl)&~v3_struct_0(sK27_skl))),
% 44.82/6.29 inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl]),skolemize(A,sK27_skl)],[f87])).
% 44.82/6.29 fof(f353,plain,(
% 44.82/6.29 l1_struct_0(sK27_skl)),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f352])).
% 44.82/6.29 fof(f359,plain,(
% 44.82/6.29 ((l3_lattices(sK29_skl)&~v3_struct_0(sK29_skl))&v3_lattices(sK29_skl))),
% 44.82/6.29 inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl]),skolemize(A,sK29_skl)],[f89])).
% 44.82/6.29 fof(f360,plain,(
% 44.82/6.29 l3_lattices(sK29_skl)),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f359])).
% 44.82/6.29 fof(f374,plain,(
% 44.82/6.29 ![A,B]: ((((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|~m1_subset_1(B,u1_struct_0(A)))|k2_filter_2(A,B)=k2_filter_0(A,B))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f91])).
% 44.82/6.29 fof(f375,plain,(
% 44.82/6.29 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|k2_filter_2(X0,X1)=k2_filter_0(X0,X1))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f374])).
% 44.82/6.29 fof(f376,plain,(
% 44.82/6.29 ![A,B]: (((((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|v1_xboole_0(B))|~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))))|k3_filter_2(A,B)=k3_filter_0(A,B))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f92])).
% 44.82/6.29 fof(f377,plain,(
% 44.82/6.29 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v1_xboole_0(X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|k3_filter_2(X0,X1)=k3_filter_0(X0,X1))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f376])).
% 44.82/6.29 fof(f378,plain,(
% 44.82/6.29 ![A,B]: ((v1_xboole_0(A)|~m1_subset_1(B,A))|k6_domain_1(A,B)=k1_tarski(B))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f93])).
% 44.82/6.29 fof(f379,plain,(
% 44.82/6.29 ![X0,X1]: (v1_xboole_0(X0)|~m1_subset_1(X1,X0)|k6_domain_1(X0,X1)=k1_tarski(X1))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f378])).
% 44.82/6.29 fof(f385,plain,(
% 44.82/6.29 ![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)))),
% 44.82/6.29 inference(NNF_transformation,[status(thm)],[f95])).
% 44.82/6.29 fof(f386,plain,(
% 44.82/6.29 (![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)))),
% 44.82/6.29 inference(miniscoping,[status(thm)],[f385])).
% 44.82/6.29 fof(f387,plain,(
% 44.82/6.29 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_relset_1(X0,X1,X2))),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f386])).
% 44.82/6.29 fof(f389,plain,(
% 44.82/6.29 ![A,B,C]: (((v1_xboole_0(A)|~m1_subset_1(B,k1_zfmisc_1(A)))|~m1_subset_1(C,k1_zfmisc_1(A)))|(r1_filter_2(A,B,C)<=>B=C))),
% 44.82/6.29 inference(pre_NNF_transformation,[status(thm)],[f96])).
% 44.82/6.29 fof(f390,plain,(
% 44.82/6.29 ![A,B,C]: (((v1_xboole_0(A)|~m1_subset_1(B,k1_zfmisc_1(A)))|~m1_subset_1(C,k1_zfmisc_1(A)))|((~r1_filter_2(A,B,C)|B=C)&(r1_filter_2(A,B,C)|~B=C)))),
% 44.82/6.29 inference(NNF_transformation,[status(thm)],[f389])).
% 44.82/6.29 fof(f391,plain,(
% 44.82/6.29 ![X0,X1,X2]: (v1_xboole_0(X0)|~m1_subset_1(X1,k1_zfmisc_1(X0))|~m1_subset_1(X2,k1_zfmisc_1(X0))|~r1_filter_2(X0,X1,X2)|X1=X2)),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f390])).
% 44.82/6.29 fof(f392,plain,(
% 44.82/6.29 ![X0,X1,X2]: (v1_xboole_0(X0)|~m1_subset_1(X1,k1_zfmisc_1(X0))|~m1_subset_1(X2,k1_zfmisc_1(X0))|r1_filter_2(X0,X1,X2)|~X1=X2)),
% 44.82/6.29 inference(cnf_transformation,[status(thm)],[f390])).
% 44.82/6.30 fof(f402,plain,(
% 44.82/6.30 ![A,B,C]: (((((((v3_struct_0(A)|~v6_lattices(A))|~v8_lattices(A))|~v9_lattices(A))|~l3_lattices(A))|~m1_subset_1(B,u1_struct_0(A)))|~m1_subset_1(C,u1_struct_0(A)))|r3_lattices(A,B,B))),
% 44.82/6.30 inference(pre_NNF_transformation,[status(thm)],[f100])).
% 44.82/6.30 fof(f403,plain,(
% 44.82/6.30 ![A,B]: (((((((v3_struct_0(A)|~v6_lattices(A))|~v8_lattices(A))|~v9_lattices(A))|~l3_lattices(A))|~m1_subset_1(B,u1_struct_0(A)))|(![C]: ~m1_subset_1(C,u1_struct_0(A))))|r3_lattices(A,B,B))),
% 44.82/6.30 inference(miniscoping,[status(thm)],[f402])).
% 44.82/6.30 fof(f404,plain,(
% 44.82/6.30 ![X0,X1,X2]: (v3_struct_0(X0)|~v6_lattices(X0)|~v8_lattices(X0)|~v9_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|r3_lattices(X0,X1,X1))),
% 44.82/6.30 inference(cnf_transformation,[status(thm)],[f403])).
% 44.82/6.30 fof(f409,plain,(
% 44.82/6.30 ![A,B]: (~m1_subset_1(A,B)|(v1_xboole_0(B)|r2_hidden(A,B)))),
% 44.82/6.30 inference(pre_NNF_transformation,[status(thm)],[f103])).
% 44.82/6.30 fof(f410,plain,(
% 44.82/6.30 ![X0,X1]: (~m1_subset_1(X0,X1)|v1_xboole_0(X1)|r2_hidden(X0,X1))),
% 44.82/6.30 inference(cnf_transformation,[status(thm)],[f409])).
% 44.82/6.30 fof(f416,plain,(
% 44.82/6.30 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m1_subset_1(B,u1_struct_0(A))|(![C]: ((v1_xboole_0(C)|~m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))))|(~C=k6_domain_1(u1_struct_0(A),B)|k3_filter_0(A,C)=k2_filter_0(A,B)))))))),
% 44.82/6.30 inference(pre_NNF_transformation,[status(thm)],[f105])).
% 44.82/6.30 fof(f417,plain,(
% 44.82/6.30 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|v1_xboole_0(X2)|~m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))|~X2=k6_domain_1(u1_struct_0(X0),X1)|k3_filter_0(X0,X2)=k2_filter_0(X0,X1))),
% 44.82/6.30 inference(cnf_transformation,[status(thm)],[f416])).
% 44.82/6.30 fof(f418,plain,(
% 44.82/6.30 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m1_subset_1(B,u1_struct_0(A))|(k18_filter_2(A,B)=k2_filter_2(k1_lattice2(A),k5_filter_2(A,B))&k18_filter_2(k1_lattice2(A),k5_filter_2(A,B))=k2_filter_2(A,B)))))),
% 44.82/6.30 inference(pre_NNF_transformation,[status(thm)],[f106])).
% 44.82/6.30 fof(f419,plain,(
% 44.82/6.30 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|k18_filter_2(X0,X1)=k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1)))),
% 44.82/6.30 inference(cnf_transformation,[status(thm)],[f418])).
% 44.82/6.30 fof(f421,plain,(
% 44.82/6.30 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: ((v1_xboole_0(B)|~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))))|(![C]: ((v1_xboole_0(C)|~m1_subset_1(C,k1_zfmisc_1(u1_struct_0(k1_lattice2(A)))))|(((k3_filter_2(k1_lattice2(A),k7_filter_2(A,B))=k19_filter_2(A,B)&k3_filter_2(A,B)=k19_filter_2(k1_lattice2(A),k7_filter_2(A,B)))&k3_filter_2(A,k8_filter_2(A,C))=k19_filter_2(k1_lattice2(A),C))&k3_filter_2(k1_lattice2(A),C)=k19_filter_2(A,k8_filter_2(A,C))))))))),
% 44.82/6.30 inference(pre_NNF_transformation,[status(thm)],[f107])).
% 44.82/6.30 fof(f422,plain,(
% 44.82/6.30 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v1_xboole_0(X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|v1_xboole_0(X2)|~m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0))))|k3_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1))=k19_filter_2(X0,X1))),
% 44.82/6.30 inference(cnf_transformation,[status(thm)],[f421])).
% 44.82/6.30 fof(f433,plain,(
% 44.82/6.30 ![A,B,C]: ((~r2_hidden(A,B)|~m1_subset_1(B,k1_zfmisc_1(C)))|~v1_xboole_0(C))),
% 44.82/6.30 inference(pre_NNF_transformation,[status(thm)],[f110])).
% 44.82/6.30 fof(f434,plain,(
% 44.82/6.30 ![C]: ((![B]: ((![A]: ~r2_hidden(A,B))|~m1_subset_1(B,k1_zfmisc_1(C))))|~v1_xboole_0(C))),
% 44.82/6.30 inference(miniscoping,[status(thm)],[f433])).
% 44.82/6.30 fof(f435,plain,(
% 44.82/6.30 ![X0,X1,X2]: (~r2_hidden(X0,X1)|~m1_subset_1(X1,k1_zfmisc_1(X2))|~v1_xboole_0(X2))),
% 44.82/6.30 inference(cnf_transformation,[status(thm)],[f434])).
% 44.82/6.30 fof(f446,plain,(
% 44.82/6.30 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|r2_hidden(X2,a_2_0_filter_2(X0,X1))|~m1_subset_1(X2,u1_struct_0(X0))|~r3_lattices(X0,X2,X1))),
% 44.82/6.30 inference(destructive_equality_resolution,[status(thm)],[f312])).
% 44.82/6.30 fof(f447,plain,(
% 44.82/6.30 ![X0,X2]: (v1_xboole_0(X0)|~m1_subset_1(X2,k1_zfmisc_1(X0))|~m1_subset_1(X2,k1_zfmisc_1(X0))|r1_filter_2(X0,X2,X2))),
% 44.82/6.30 inference(destructive_equality_resolution,[status(thm)],[f392])).
% 44.82/6.30 fof(f448,plain,(
% 44.82/6.30 ![X0,X1]: (v1_xboole_0(X0)|~m1_subset_1(X1,k1_zfmisc_1(X0))|r1_filter_2(X0,X1,X1))),
% 44.82/6.30 inference(duplicate_literals_removal,[status(thm)],[f447])).
% 44.82/6.30 fof(f449,plain,(
% 44.82/6.30 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|v1_xboole_0(k6_domain_1(u1_struct_0(X0),X1))|~m1_subset_1(k6_domain_1(u1_struct_0(X0),X1),k1_zfmisc_1(u1_struct_0(X0)))|k3_filter_0(X0,k6_domain_1(u1_struct_0(X0),X1))=k2_filter_0(X0,X1))),
% 44.82/6.30 inference(destructive_equality_resolution,[status(thm)],[f417])).
% 44.82/6.30 fof(f451,definition,(
% 44.82/6.30 sQ0_spl <=> (v3_struct_0(sK0_skl))),
% 44.82/6.30 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 44.82/6.30 fof(f452,plain,(
% 44.82/6.30 v3_struct_0(sK0_skl)|~sQ0_spl),
% 44.82/6.30 inference(component_clause,[status(thm)],[f451])).
% 44.82/6.30 fof(f454,definition,(
% 44.82/6.30 sQ1_spl <=> (v10_lattices(sK0_skl))),
% 44.82/6.30 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 44.82/6.30 fof(f456,plain,(
% 44.82/6.30 ~v10_lattices(sK0_skl)|sQ1_spl),
% 44.82/6.30 inference(component_clause,[status(thm)],[f454])).
% 44.82/6.30 fof(f466,plain,(
% 44.82/6.30 $false|sQ1_spl),
% 44.82/6.30 inference(forward_subsumption_resolution,[status(thm)],[f456,f117])).
% 44.82/6.30 fof(f467,plain,(
% 44.82/6.30 sQ1_spl),
% 44.82/6.30 inference(contradiction_clause,[status(thm)],[f466])).
% 44.82/6.30 fof(f468,plain,(
% 44.82/6.30 $false|~sQ0_spl),
% 44.82/6.30 inference(forward_subsumption_resolution,[status(thm)],[f452,f116])).
% 44.82/6.30 fof(f469,plain,(
% 44.82/6.30 ~sQ0_spl),
% 44.82/6.30 inference(contradiction_clause,[status(thm)],[f468])).
% 44.82/6.30 fof(f470,plain,(
% 44.82/6.30 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|v6_lattices(sK0_skl)),
% 44.82/6.30 inference(resolution,[status(thm)],[f134,f118])).
% 44.82/6.30 fof(f471,definition,(
% 44.82/6.30 sQ4_spl <=> (v6_lattices(sK0_skl))),
% 44.82/6.30 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 44.82/6.30 fof(f474,plain,(
% 44.82/6.30 sQ0_spl|~sQ1_spl|sQ4_spl),
% 44.82/6.30 inference(split_clause,[status(thm)],[f470,f451,f454,f471])).
% 44.82/6.30 fof(f476,plain,(
% 44.82/6.30 v1_xboole_0(u1_struct_0(sK0_skl))|k6_domain_1(u1_struct_0(sK0_skl),sK1_skl)=k1_tarski(sK1_skl)),
% 44.82/6.30 inference(resolution,[status(thm)],[f379,f119])).
% 44.82/6.30 fof(f484,definition,(
% 44.82/6.30 sQ7_spl <=> (v1_xboole_0(u1_struct_0(sK0_skl)))),
% 44.82/6.30 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 44.82/6.30 fof(f487,definition,(
% 44.82/6.30 sQ8_spl <=> (k6_domain_1(u1_struct_0(sK0_skl),sK1_skl)=k1_tarski(sK1_skl))),
% 44.82/6.30 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 44.82/6.30 fof(f488,plain,(
% 44.82/6.30 k6_domain_1(u1_struct_0(sK0_skl),sK1_skl)=k1_tarski(sK1_skl)|~sQ8_spl),
% 44.82/6.30 inference(component_clause,[status(thm)],[f487])).
% 44.82/6.30 fof(f490,plain,(
% 44.82/6.30 sQ7_spl|sQ8_spl),
% 44.82/6.30 inference(split_clause,[status(thm)],[f476,f484,f487])).
% 44.82/6.30 fof(f493,plain,(
% 44.82/6.30 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|k18_filter_2(sK0_skl,sK1_skl)=a_2_0_filter_2(sK0_skl,sK1_skl)),
% 44.82/6.30 inference(resolution,[status(thm)],[f161,f119])).
% 44.82/6.30 fof(f494,definition,(
% 44.82/6.30 sQ9_spl <=> (l3_lattices(sK0_skl))),
% 44.82/6.30 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 44.82/6.30 fof(f496,plain,(
% 44.82/6.30 ~l3_lattices(sK0_skl)|sQ9_spl),
% 44.82/6.30 inference(component_clause,[status(thm)],[f494])).
% 44.82/6.30 fof(f497,definition,(
% 44.82/6.30 sQ10_spl <=> (k18_filter_2(sK0_skl,sK1_skl)=a_2_0_filter_2(sK0_skl,sK1_skl))),
% 44.82/6.30 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 44.82/6.30 fof(f498,plain,(
% 44.82/6.30 k18_filter_2(sK0_skl,sK1_skl)=a_2_0_filter_2(sK0_skl,sK1_skl)|~sQ10_spl),
% 44.82/6.30 inference(component_clause,[status(thm)],[f497])).
% 44.82/6.30 fof(f500,plain,(
% 44.82/6.30 sQ0_spl|~sQ1_spl|~sQ9_spl|sQ10_spl),
% 44.82/6.30 inference(split_clause,[status(thm)],[f493,f451,f454,f494,f497])).
% 44.82/6.30 fof(f501,plain,(
% 44.82/6.30 $false|sQ9_spl),
% 44.82/6.30 inference(forward_subsumption_resolution,[status(thm)],[f496,f118])).
% 44.82/6.30 fof(f502,plain,(
% 44.82/6.30 sQ9_spl),
% 44.82/6.30 inference(contradiction_clause,[status(thm)],[f501])).
% 44.82/6.30 fof(f503,plain,(
% 44.82/6.30 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m2_filter_2(k18_filter_2(sK0_skl,sK1_skl),sK0_skl)),
% 44.82/6.30 inference(resolution,[status(thm)],[f166,f119])).
% 44.82/6.30 fof(f504,definition,(
% 44.82/6.30 sQ11_spl <=> (m2_filter_2(k18_filter_2(sK0_skl,sK1_skl),sK0_skl))),
% 44.82/6.30 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 44.82/6.30 fof(f505,plain,(
% 44.82/6.30 m2_filter_2(k18_filter_2(sK0_skl,sK1_skl),sK0_skl)|~sQ11_spl),
% 44.82/6.30 inference(component_clause,[status(thm)],[f504])).
% 44.82/6.30 fof(f507,plain,(
% 44.82/6.30 sQ0_spl|~sQ1_spl|~sQ9_spl|sQ11_spl),
% 44.82/6.30 inference(split_clause,[status(thm)],[f503,f451,f454,f494,f504])).
% 44.82/6.30 fof(f509,plain,(
% 44.82/6.30 v1_xboole_0(u1_struct_0(sK0_skl))|m1_subset_1(k6_domain_1(u1_struct_0(sK0_skl),sK1_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 44.82/6.30 inference(resolution,[status(thm)],[f183,f119])).
% 44.82/6.30 fof(f514,definition,(
% 44.82/6.30 sQ13_spl <=> (m1_subset_1(k6_domain_1(u1_struct_0(sK0_skl),sK1_skl),k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 44.82/6.30 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 44.82/6.30 fof(f517,plain,(
% 44.82/6.30 sQ7_spl|sQ13_spl),
% 44.82/6.30 inference(split_clause,[status(thm)],[f509,f484,f514])).
% 44.82/6.30 fof(f520,plain,(
% 44.82/6.30 v1_xboole_0(u1_struct_0(sK0_skl))|~m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~m1_subset_1(k6_domain_1(u1_struct_0(sK0_skl),sK1_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|sK2_skl=k6_domain_1(u1_struct_0(sK0_skl),sK1_skl)),
% 44.82/6.30 inference(resolution,[status(thm)],[f391,f122])).
% 44.82/6.30 fof(f525,definition,(
% 44.82/6.30 sQ15_spl <=> (m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 44.82/6.30 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 44.82/6.30 fof(f526,plain,(
% 44.82/6.30 m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ15_spl),
% 44.82/6.30 inference(component_clause,[status(thm)],[f525])).
% 44.82/6.30 fof(f527,plain,(
% 44.82/6.30 ~m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))|sQ15_spl),
% 44.82/6.30 inference(component_clause,[status(thm)],[f525])).
% 44.82/6.30 fof(f528,definition,(
% 44.82/6.30 sQ16_spl <=> (sK2_skl=k6_domain_1(u1_struct_0(sK0_skl),sK1_skl))),
% 44.82/6.30 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 44.82/6.30 fof(f529,plain,(
% 44.82/6.30 sK2_skl=k6_domain_1(u1_struct_0(sK0_skl),sK1_skl)|~sQ16_spl),
% 44.82/6.30 inference(component_clause,[status(thm)],[f528])).
% 44.82/6.30 fof(f531,plain,(
% 44.82/6.30 sQ7_spl|~sQ15_spl|~sQ13_spl|sQ16_spl),
% 44.82/6.30 inference(split_clause,[status(thm)],[f520,f484,f525,f514,f528])).
% 44.82/6.30 fof(f566,plain,(
% 44.82/6.30 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|v8_lattices(sK0_skl)),
% 44.82/6.30 inference(resolution,[status(thm)],[f136,f118])).
% 44.82/6.30 fof(f571,definition,(
% 44.82/6.30 sQ25_spl <=> (v8_lattices(sK0_skl))),
% 44.82/6.30 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 44.82/6.30 fof(f574,plain,(
% 44.82/6.30 sQ0_spl|~sQ1_spl|sQ25_spl),
% 44.82/6.30 inference(split_clause,[status(thm)],[f566,f451,f454,f571])).
% 44.82/6.30 fof(f576,plain,(
% 44.82/6.30 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|v9_lattices(sK0_skl)),
% 44.82/6.30 inference(resolution,[status(thm)],[f137,f118])).
% 44.82/6.30 fof(f581,definition,(
% 44.82/6.30 sQ27_spl <=> (v9_lattices(sK0_skl))),
% 44.82/6.30 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 44.82/6.30 fof(f584,plain,(
% 44.82/6.30 sQ0_spl|~sQ1_spl|sQ27_spl),
% 44.82/6.30 inference(split_clause,[status(thm)],[f576,f451,f454,f581])).
% 44.82/6.30 fof(f616,definition,(
% 44.82/6.30 sQ33_spl <=> (m1_subset_1(k18_filter_2(sK0_skl,sK1_skl),k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 44.82/6.30 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 44.82/6.30 fof(f617,plain,(
% 44.82/6.30 m1_subset_1(k18_filter_2(sK0_skl,sK1_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ33_spl),
% 44.82/6.30 inference(component_clause,[status(thm)],[f616])).
% 44.82/6.30 fof(f619,definition,(
% 44.82/6.30 sQ34_spl <=> (m1_subset_1(k19_filter_2(sK0_skl,sK2_skl),k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 44.82/6.30 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 44.82/6.30 fof(f620,plain,(
% 44.82/6.30 m1_subset_1(k19_filter_2(sK0_skl,sK2_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ34_spl),
% 44.82/6.30 inference(component_clause,[status(thm)],[f619])).
% 44.82/6.30 fof(f621,plain,(
% 44.82/6.30 ~m1_subset_1(k19_filter_2(sK0_skl,sK2_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|sQ34_spl),
% 44.82/6.30 inference(component_clause,[status(thm)],[f619])).
% 44.82/6.30 fof(f646,plain,(
% 44.82/6.30 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|k5_filter_2(sK0_skl,sK1_skl)=sK1_skl),
% 44.82/6.30 inference(resolution,[status(thm)],[f155,f119])).
% 44.82/6.30 fof(f647,definition,(
% 44.82/6.30 sQ37_spl <=> (k5_filter_2(sK0_skl,sK1_skl)=sK1_skl)),
% 44.82/6.30 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 44.82/6.30 fof(f648,plain,(
% 44.82/6.30 k5_filter_2(sK0_skl,sK1_skl)=sK1_skl|~sQ37_spl),
% 44.82/6.30 inference(component_clause,[status(thm)],[f647])).
% 44.82/6.30 fof(f650,plain,(
% 44.82/6.30 sQ0_spl|~sQ1_spl|~sQ9_spl|sQ37_spl),
% 44.82/6.30 inference(split_clause,[status(thm)],[f646,f451,f454,f494,f647])).
% 44.82/6.30 fof(f651,plain,(
% 44.82/6.30 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|k7_filter_2(sK0_skl,sK2_skl)=sK2_skl),
% 44.82/6.30 inference(resolution,[status(thm)],[f157,f121])).
% 44.82/6.30 fof(f652,definition,(
% 44.82/6.30 sQ38_spl <=> (k7_filter_2(sK0_skl,sK2_skl)=sK2_skl)),
% 44.82/6.30 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 44.82/6.30 fof(f653,plain,(
% 44.82/6.30 k7_filter_2(sK0_skl,sK2_skl)=sK2_skl|~sQ38_spl),
% 44.82/6.30 inference(component_clause,[status(thm)],[f652])).
% 44.82/6.30 fof(f655,plain,(
% 44.82/6.30 sQ0_spl|~sQ1_spl|~sQ9_spl|sQ38_spl),
% 44.82/6.30 inference(split_clause,[status(thm)],[f651,f451,f454,f494,f652])).
% 44.82/6.30 fof(f727,plain,(
% 44.82/6.30 $false|sQ15_spl),
% 44.82/6.30 inference(forward_subsumption_resolution,[status(thm)],[f121,f527])).
% 44.82/6.30 fof(f728,plain,(
% 44.82/6.30 sQ15_spl),
% 44.82/6.30 inference(contradiction_clause,[status(thm)],[f727])).
% 44.82/6.30 fof(f798,plain,(
% 44.82/6.30 v1_realset1(sK20_skl)),
% 44.82/6.30 inference(resolution,[status(thm)],[f332,f139])).
% 44.82/6.30 fof(f820,plain,(
% 44.82/6.30 l3_lattices(k1_lattice2(sK6_skl))),
% 44.82/6.30 inference(resolution,[status(thm)],[f171,f223])).
% 44.82/6.30 fof(f821,plain,(
% 44.82/6.30 l3_lattices(k1_lattice2(sK0_skl))),
% 44.82/6.30 inference(resolution,[status(thm)],[f171,f118])).
% 44.82/6.30 fof(f864,plain,(
% 44.82/6.30 sK2_skl=k1_tarski(sK1_skl)|~sQ16_spl|~sQ8_spl),
% 44.82/6.30 inference(forward_demodulation,[status(thm)],[f529,f488])).
% 44.82/6.30 fof(f933,plain,(
% 44.82/6.30 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m1_subset_1(k5_filter_2(sK0_skl,sK1_skl),u1_struct_0(k1_lattice2(sK0_skl)))),
% 44.82/6.30 inference(resolution,[status(thm)],[f181,f119])).
% 44.82/6.30 fof(f934,definition,(
% 44.82/6.30 sQ70_spl <=> (m1_subset_1(k5_filter_2(sK0_skl,sK1_skl),u1_struct_0(k1_lattice2(sK0_skl))))),
% 44.82/6.30 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 44.82/6.30 fof(f935,plain,(
% 44.82/6.30 m1_subset_1(k5_filter_2(sK0_skl,sK1_skl),u1_struct_0(k1_lattice2(sK0_skl)))|~sQ70_spl),
% 44.82/6.30 inference(component_clause,[status(thm)],[f934])).
% 44.82/6.30 fof(f937,plain,(
% 44.82/6.31 sQ0_spl|~sQ1_spl|~sQ9_spl|sQ70_spl),
% 44.82/6.31 inference(split_clause,[status(thm)],[f933,f451,f454,f494,f934])).
% 44.82/6.31 fof(f938,plain,(
% 44.82/6.31 m1_subset_1(sK1_skl,u1_struct_0(k1_lattice2(sK0_skl)))|~sQ37_spl|~sQ70_spl),
% 44.82/6.31 inference(forward_demodulation,[status(thm)],[f648,f935])).
% 44.82/6.31 fof(f940,definition,(
% 44.82/6.31 sQ71_spl <=> (l3_lattices(k1_lattice2(sK0_skl)))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f942,plain,(
% 44.82/6.31 ~l3_lattices(k1_lattice2(sK0_skl))|sQ71_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f940])).
% 44.82/6.31 fof(f947,plain,(
% 44.82/6.31 $false|sQ71_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f942,f821])).
% 44.82/6.31 fof(f948,plain,(
% 44.82/6.31 sQ71_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f947])).
% 44.82/6.31 fof(f958,definition,(
% 44.82/6.31 sQ73_spl <=> (v3_struct_0(k1_lattice2(sK0_skl)))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f959,plain,(
% 44.82/6.31 v3_struct_0(k1_lattice2(sK0_skl))|~sQ73_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f958])).
% 44.82/6.31 fof(f961,definition,(
% 44.82/6.31 sQ74_spl <=> (v10_lattices(k1_lattice2(sK0_skl)))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f1018,plain,(
% 44.82/6.31 l1_struct_0(sK3_skl)),
% 44.82/6.31 inference(resolution,[status(thm)],[f189,f217])).
% 44.82/6.31 fof(f1019,plain,(
% 44.82/6.31 l1_struct_0(sK5_skl)),
% 44.82/6.31 inference(resolution,[status(thm)],[f191,f221])).
% 44.82/6.31 fof(f1020,plain,(
% 44.82/6.31 l1_lattices(k1_lattice2(sK0_skl))),
% 44.82/6.31 inference(resolution,[status(thm)],[f193,f821])).
% 44.82/6.31 fof(f1021,plain,(
% 44.82/6.31 l1_lattices(sK6_skl)),
% 44.82/6.31 inference(resolution,[status(thm)],[f193,f223])).
% 44.82/6.31 fof(f1022,plain,(
% 44.82/6.31 l1_lattices(sK0_skl)),
% 44.82/6.31 inference(resolution,[status(thm)],[f193,f118])).
% 44.82/6.31 fof(f1025,plain,(
% 44.82/6.31 l2_lattices(sK0_skl)),
% 44.82/6.31 inference(resolution,[status(thm)],[f194,f118])).
% 44.82/6.31 fof(f1060,plain,(
% 44.82/6.31 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m1_subset_1(k7_filter_2(sK0_skl,sK2_skl),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0_skl))))|~sQ15_spl),
% 44.82/6.31 inference(resolution,[status(thm)],[f526,f185])).
% 44.82/6.31 fof(f1070,definition,(
% 44.82/6.31 sQ89_spl <=> (m1_subset_1(k7_filter_2(sK0_skl,sK2_skl),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0_skl)))))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f1071,plain,(
% 44.82/6.31 m1_subset_1(k7_filter_2(sK0_skl,sK2_skl),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0_skl))))|~sQ89_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f1070])).
% 44.82/6.31 fof(f1073,plain,(
% 44.82/6.31 sQ0_spl|~sQ1_spl|~sQ9_spl|sQ89_spl|~sQ15_spl),
% 44.82/6.31 inference(split_clause,[status(thm)],[f1060,f451,f454,f494,f1070,f525])).
% 44.82/6.31 fof(f1074,definition,(
% 44.82/6.31 sQ90_spl <=> (v1_xboole_0(sK2_skl))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f1075,plain,(
% 44.82/6.31 v1_xboole_0(sK2_skl)|~sQ90_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f1074])).
% 44.82/6.31 fof(f1095,plain,(
% 44.82/6.31 $false|~sQ90_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f1075,f120])).
% 44.82/6.31 fof(f1096,plain,(
% 44.82/6.31 ~sQ90_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f1095])).
% 44.82/6.31 fof(f1097,plain,(
% 44.82/6.31 m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0_skl))))|~sQ38_spl|~sQ89_spl),
% 44.82/6.31 inference(forward_demodulation,[status(thm)],[f653,f1071])).
% 44.82/6.31 fof(f1098,plain,(
% 44.82/6.31 l2_lattices(sK26_skl)),
% 44.82/6.31 inference(resolution,[status(thm)],[f350,f194])).
% 44.82/6.31 fof(f1100,plain,(
% 44.82/6.31 l3_lattices(k1_lattice2(sK26_skl))),
% 44.82/6.31 inference(resolution,[status(thm)],[f350,f171])).
% 44.82/6.31 fof(f1154,plain,(
% 44.82/6.31 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m2_lattice4(k18_filter_2(sK0_skl,sK1_skl),sK0_skl)|~sQ11_spl),
% 44.82/6.31 inference(resolution,[status(thm)],[f203,f505])).
% 44.82/6.31 fof(f1155,definition,(
% 44.82/6.31 sQ105_spl <=> (m2_lattice4(k18_filter_2(sK0_skl,sK1_skl),sK0_skl))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f1156,plain,(
% 44.82/6.31 m2_lattice4(k18_filter_2(sK0_skl,sK1_skl),sK0_skl)|~sQ105_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f1155])).
% 44.82/6.31 fof(f1158,plain,(
% 44.82/6.31 sQ0_spl|~sQ1_spl|~sQ9_spl|sQ105_spl|~sQ11_spl),
% 44.82/6.31 inference(split_clause,[status(thm)],[f1154,f451,f454,f494,f1155,f504])).
% 44.82/6.31 fof(f1179,plain,(
% 44.82/6.31 l1_struct_0(k1_lattice2(sK0_skl))),
% 44.82/6.31 inference(resolution,[status(thm)],[f1020,f189])).
% 44.82/6.31 fof(f1187,plain,(
% 44.82/6.31 v1_xboole_0(u1_struct_0(k1_lattice2(sK0_skl)))|m1_subset_1(k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),sK1_skl),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0_skl))))|~sQ37_spl|~sQ70_spl),
% 44.82/6.31 inference(resolution,[status(thm)],[f938,f183])).
% 44.82/6.31 fof(f1188,plain,(
% 44.82/6.31 v1_xboole_0(u1_struct_0(k1_lattice2(sK0_skl)))|k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),sK1_skl)=k1_tarski(sK1_skl)|~sQ37_spl|~sQ70_spl),
% 44.82/6.31 inference(resolution,[status(thm)],[f938,f379])).
% 44.82/6.31 fof(f1217,definition,(
% 44.82/6.31 sQ117_spl <=> (v1_xboole_0(u1_struct_0(k1_lattice2(sK0_skl))))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f1218,plain,(
% 44.82/6.31 v1_xboole_0(u1_struct_0(k1_lattice2(sK0_skl)))|~sQ117_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f1217])).
% 44.82/6.31 fof(f1220,definition,(
% 44.82/6.31 sQ118_spl <=> (m1_subset_1(k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),sK1_skl),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0_skl)))))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f1221,plain,(
% 44.82/6.31 m1_subset_1(k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),sK1_skl),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0_skl))))|~sQ118_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f1220])).
% 44.82/6.31 fof(f1223,plain,(
% 44.82/6.31 sQ117_spl|sQ118_spl|~sQ37_spl|~sQ70_spl),
% 44.82/6.31 inference(split_clause,[status(thm)],[f1187,f1217,f1220,f647,f934])).
% 44.82/6.31 fof(f1224,definition,(
% 44.82/6.31 sQ119_spl <=> (k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),sK1_skl)=k1_tarski(sK1_skl))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f1225,plain,(
% 44.82/6.31 k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),sK1_skl)=k1_tarski(sK1_skl)|~sQ119_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f1224])).
% 44.82/6.31 fof(f1227,plain,(
% 44.82/6.31 sQ117_spl|sQ119_spl|~sQ37_spl|~sQ70_spl),
% 44.82/6.31 inference(split_clause,[status(thm)],[f1188,f1217,f1224,f647,f934])).
% 44.82/6.31 fof(f1247,plain,(
% 44.82/6.31 l2_lattices(sK29_skl)),
% 44.82/6.31 inference(resolution,[status(thm)],[f360,f194])).
% 44.82/6.31 fof(f1297,plain,(
% 44.82/6.31 m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))),
% 44.82/6.31 inference(resolution,[status(thm)],[f211,f1022])).
% 44.82/6.31 fof(f1303,plain,(
% 44.82/6.31 m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))),
% 44.82/6.31 inference(resolution,[status(thm)],[f215,f1025])).
% 44.82/6.31 fof(f1674,plain,(
% 44.82/6.31 m1_subset_1(k1_tarski(sK1_skl),k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0_skl))))|~sQ119_spl|~sQ118_spl),
% 44.82/6.31 inference(forward_demodulation,[status(thm)],[f1225,f1221])).
% 44.82/6.31 fof(f1759,plain,(
% 44.82/6.31 v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|~sQ73_spl),
% 44.82/6.31 inference(resolution,[status(thm)],[f245,f959])).
% 44.82/6.31 fof(f1760,plain,(
% 44.82/6.31 sQ0_spl|~sQ9_spl|~sQ73_spl),
% 44.82/6.31 inference(split_clause,[status(thm)],[f1759,f451,f494,f958])).
% 44.82/6.31 fof(f2321,plain,(
% 44.82/6.31 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m1_subset_1(k18_filter_2(sK0_skl,sK1_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ105_spl),
% 44.82/6.31 inference(resolution,[status(thm)],[f1156,f205])).
% 44.82/6.31 fof(f2322,plain,(
% 44.82/6.31 sQ0_spl|~sQ1_spl|~sQ9_spl|sQ33_spl|~sQ105_spl),
% 44.82/6.31 inference(split_clause,[status(thm)],[f2321,f451,f454,f494,f616,f1155])).
% 44.82/6.31 fof(f2620,plain,(
% 44.82/6.31 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|v10_lattices(k1_lattice2(sK0_skl))),
% 44.82/6.31 inference(resolution,[status(thm)],[f296,f118])).
% 44.82/6.31 fof(f2642,plain,(
% 44.82/6.31 sQ0_spl|~sQ1_spl|sQ74_spl),
% 44.82/6.31 inference(split_clause,[status(thm)],[f2620,f451,f454,f961])).
% 44.82/6.31 fof(f2644,definition,(
% 44.82/6.31 sQ314_spl <=> (m1_subset_1(sK1_skl,u1_struct_0(sK0_skl)))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ314_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f2645,plain,(
% 44.82/6.31 m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))|~sQ314_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f2644])).
% 44.82/6.31 fof(f2646,plain,(
% 44.82/6.31 ~m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))|sQ314_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f2644])).
% 44.82/6.31 fof(f2766,plain,(
% 44.82/6.31 l1_struct_0(sK6_skl)),
% 44.82/6.31 inference(resolution,[status(thm)],[f1021,f189])).
% 44.82/6.31 fof(f2791,plain,(
% 44.82/6.31 $false|sQ314_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f119,f2646])).
% 44.82/6.31 fof(f2792,plain,(
% 44.82/6.31 sQ314_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f2791])).
% 44.82/6.31 fof(f2984,plain,(
% 44.82/6.31 l1_struct_0(sK26_skl)),
% 44.82/6.31 inference(resolution,[status(thm)],[f1098,f191])).
% 44.82/6.31 fof(f3267,plain,(
% 44.82/6.31 l1_struct_0(sK29_skl)),
% 44.82/6.31 inference(resolution,[status(thm)],[f1247,f191])).
% 44.82/6.31 fof(f3578,plain,(
% 44.82/6.31 v3_struct_0(k1_lattice2(sK0_skl))|~v10_lattices(k1_lattice2(sK0_skl))|~l3_lattices(k1_lattice2(sK0_skl))|k2_filter_2(k1_lattice2(sK0_skl),sK1_skl)=k2_filter_0(k1_lattice2(sK0_skl),sK1_skl)|~sQ37_spl|~sQ70_spl),
% 44.82/6.31 inference(resolution,[status(thm)],[f375,f938])).
% 44.82/6.31 fof(f3579,definition,(
% 44.82/6.31 sQ442_spl <=> (k2_filter_2(k1_lattice2(sK0_skl),sK1_skl)=k2_filter_0(k1_lattice2(sK0_skl),sK1_skl))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ442_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f3580,plain,(
% 44.82/6.31 k2_filter_2(k1_lattice2(sK0_skl),sK1_skl)=k2_filter_0(k1_lattice2(sK0_skl),sK1_skl)|~sQ442_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f3579])).
% 44.82/6.31 fof(f3582,plain,(
% 44.82/6.31 sQ73_spl|~sQ74_spl|~sQ71_spl|sQ442_spl|~sQ37_spl|~sQ70_spl),
% 44.82/6.31 inference(split_clause,[status(thm)],[f3578,f958,f961,f940,f3579,f647,f934])).
% 44.82/6.31 fof(f3586,plain,(
% 44.82/6.31 v3_struct_0(k1_lattice2(sK0_skl))|~v10_lattices(k1_lattice2(sK0_skl))|~l3_lattices(k1_lattice2(sK0_skl))|v1_xboole_0(sK2_skl)|k3_filter_2(k1_lattice2(sK0_skl),sK2_skl)=k3_filter_0(k1_lattice2(sK0_skl),sK2_skl)|~sQ38_spl|~sQ89_spl),
% 44.82/6.31 inference(resolution,[status(thm)],[f377,f1097])).
% 44.82/6.31 fof(f3594,definition,(
% 44.82/6.31 sQ444_spl <=> (k3_filter_2(k1_lattice2(sK0_skl),sK2_skl)=k3_filter_0(k1_lattice2(sK0_skl),sK2_skl))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ444_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f3595,plain,(
% 44.82/6.31 k3_filter_2(k1_lattice2(sK0_skl),sK2_skl)=k3_filter_0(k1_lattice2(sK0_skl),sK2_skl)|~sQ444_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f3594])).
% 44.82/6.31 fof(f3597,plain,(
% 44.82/6.31 sQ73_spl|~sQ74_spl|~sQ71_spl|sQ90_spl|sQ444_spl|~sQ38_spl|~sQ89_spl),
% 44.82/6.31 inference(split_clause,[status(thm)],[f3586,f958,f961,f940,f1074,f3594,f652,f1070])).
% 44.82/6.31 fof(f3671,definition,(
% 44.82/6.31 sQ453_spl <=> (m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ453_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f3673,plain,(
% 44.82/6.31 ~m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|sQ453_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f3671])).
% 44.82/6.31 fof(f3677,definition,(
% 44.82/6.31 sQ455_spl <=> (m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ455_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f3679,plain,(
% 44.82/6.31 ~m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|sQ455_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f3677])).
% 44.82/6.31 fof(f3781,plain,(
% 44.82/6.31 ![X0,X1]: (v3_struct_0(X0)|~v6_lattices(X0)|~v8_lattices(X0)|~v9_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|r3_lattices(X0,X1,X1))),
% 44.82/6.31 inference(resolution,[status(thm)],[f404,f233])).
% 44.82/6.31 fof(f3801,plain,(
% 44.82/6.31 ![X0]: (v1_xboole_0(X0)|r2_hidden(sK10_skl(X0),X0))),
% 44.82/6.31 inference(resolution,[status(thm)],[f410,f233])).
% 44.82/6.31 fof(f4032,plain,(
% 44.82/6.31 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v1_xboole_0(X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|v1_xboole_0(sK19_skl(u1_struct_0(k1_lattice2(X0))))|k3_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1))=k19_filter_2(X0,X1)|v1_xboole_0(u1_struct_0(k1_lattice2(X0))))),
% 44.82/6.31 inference(resolution,[status(thm)],[f422,f329])).
% 44.82/6.31 fof(f4040,plain,(
% 44.82/6.31 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v1_xboole_0(X1)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|k3_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1))=k19_filter_2(X0,X1)|v1_xboole_0(u1_struct_0(k1_lattice2(X0))))),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f4032,f330])).
% 44.82/6.31 fof(f4096,plain,(
% 44.82/6.31 v3_struct_0(k1_lattice2(sK0_skl))|~l1_struct_0(k1_lattice2(sK0_skl))|~sQ117_spl),
% 44.82/6.31 inference(resolution,[status(thm)],[f1218,f248])).
% 44.82/6.31 fof(f4101,definition,(
% 44.82/6.31 sQ504_spl <=> (l1_struct_0(k1_lattice2(sK0_skl)))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ504_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f4103,plain,(
% 44.82/6.31 ~l1_struct_0(k1_lattice2(sK0_skl))|sQ504_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f4101])).
% 44.82/6.31 fof(f4104,plain,(
% 44.82/6.31 sQ73_spl|~sQ504_spl|~sQ117_spl),
% 44.82/6.31 inference(split_clause,[status(thm)],[f4096,f958,f4101,f1217])).
% 44.82/6.31 fof(f4154,plain,(
% 44.82/6.31 m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0_skl))))|~sQ16_spl|~sQ8_spl|~sQ119_spl|~sQ118_spl),
% 44.82/6.31 inference(forward_demodulation,[status(thm)],[f864,f1674])).
% 44.82/6.31 fof(f4156,plain,(
% 44.82/6.31 k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),sK1_skl)=sK2_skl|~sQ16_spl|~sQ8_spl|~sQ119_spl),
% 44.82/6.31 inference(forward_demodulation,[status(thm)],[f864,f1225])).
% 44.82/6.31 fof(f4234,plain,(
% 44.82/6.31 ![X0]: (~r2_hidden(X0,k18_filter_2(sK0_skl,sK1_skl))|~v1_xboole_0(u1_struct_0(sK0_skl))|~sQ33_spl)),
% 44.82/6.31 inference(resolution,[status(thm)],[f435,f617])).
% 44.82/6.31 fof(f4243,definition,(
% 44.82/6.31 ![X0]: (sQ512_spl <=> (~r2_hidden(X0,k18_filter_2(sK0_skl,sK1_skl))))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ512_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f4244,plain,(
% 44.82/6.31 ![X0]: (~r2_hidden(X0,k18_filter_2(sK0_skl,sK1_skl))|~sQ512_spl)),
% 44.82/6.31 inference(component_clause,[status(thm)],[f4243])).
% 44.82/6.31 fof(f4246,plain,(
% 44.82/6.31 sQ512_spl|~sQ7_spl|~sQ33_spl),
% 44.82/6.31 inference(split_clause,[status(thm)],[f4234,f4243,f484,f616])).
% 44.82/6.31 fof(f4247,definition,(
% 44.82/6.31 ![X0]: (sQ513_spl <=> (~r2_hidden(X0,k1_tarski(sK20_skl))))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ513_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f4248,plain,(
% 44.82/6.31 ![X0]: (~r2_hidden(X0,k1_tarski(sK20_skl))|~sQ513_spl)),
% 44.82/6.31 inference(component_clause,[status(thm)],[f4247])).
% 44.82/6.31 fof(f4254,definition,(
% 44.82/6.31 ![X0]: (sQ515_spl <=> (~r2_hidden(X0,k1_tarski(sK2_skl))))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ515_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f4255,plain,(
% 44.82/6.31 ![X0]: (~r2_hidden(X0,k1_tarski(sK2_skl))|~sQ515_spl)),
% 44.82/6.31 inference(component_clause,[status(thm)],[f4254])).
% 44.82/6.31 fof(f4587,plain,(
% 44.82/6.31 l2_lattices(k1_lattice2(sK6_skl))),
% 44.82/6.31 inference(resolution,[status(thm)],[f820,f194])).
% 44.82/6.31 fof(f4677,plain,(
% 44.82/6.31 l2_lattices(k1_lattice2(sK26_skl))),
% 44.82/6.31 inference(resolution,[status(thm)],[f1100,f194])).
% 44.82/6.31 fof(f6435,definition,(
% 44.82/6.31 sQ861_spl <=> (l1_struct_0(sK6_skl))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ861_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f6437,plain,(
% 44.82/6.31 ~l1_struct_0(sK6_skl)|sQ861_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f6435])).
% 44.82/6.31 fof(f6923,definition,(
% 44.82/6.31 sQ948_spl <=> (l1_struct_0(sK26_skl))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ948_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f6925,plain,(
% 44.82/6.31 ~l1_struct_0(sK26_skl)|sQ948_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f6923])).
% 44.82/6.31 fof(f6961,definition,(
% 44.82/6.31 sQ949_spl <=> (l1_struct_0(sK29_skl))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ949_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f6963,plain,(
% 44.82/6.31 ~l1_struct_0(sK29_skl)|sQ949_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f6961])).
% 44.82/6.31 fof(f7213,definition,(
% 44.82/6.31 sQ969_spl <=> (m1_subset_1(sK1_skl,u1_struct_0(k1_lattice2(sK0_skl))))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ969_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f7215,plain,(
% 44.82/6.31 ~m1_subset_1(sK1_skl,u1_struct_0(k1_lattice2(sK0_skl)))|sQ969_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f7213])).
% 44.82/6.31 fof(f7228,plain,(
% 44.82/6.31 $false|~sQ37_spl|~sQ70_spl|sQ969_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f7215,f938])).
% 44.82/6.31 fof(f7229,plain,(
% 44.82/6.31 ~sQ37_spl|~sQ70_spl|sQ969_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f7228])).
% 44.82/6.31 fof(f7329,plain,(
% 44.82/6.31 $false|sQ504_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f4103,f1179])).
% 44.82/6.31 fof(f7330,plain,(
% 44.82/6.31 sQ504_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f7329])).
% 44.82/6.31 fof(f7341,definition,(
% 44.82/6.31 sQ985_spl <=> (v1_xboole_0(sK24_skl))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ985_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f7342,plain,(
% 44.82/6.31 v1_xboole_0(sK24_skl)|~sQ985_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f7341])).
% 44.82/6.31 fof(f7368,plain,(
% 44.82/6.31 $false|~sQ985_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f7342,f344])).
% 44.82/6.31 fof(f7369,plain,(
% 44.82/6.31 ~sQ985_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f7368])).
% 44.82/6.31 fof(f7381,definition,(
% 44.82/6.31 sQ992_spl <=> (v1_xboole_0(sK22_skl))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ992_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f7382,plain,(
% 44.82/6.31 v1_xboole_0(sK22_skl)|~sQ992_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f7381])).
% 44.82/6.31 fof(f7408,plain,(
% 44.82/6.31 $false|~sQ992_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f7382,f338])).
% 44.82/6.31 fof(f7409,plain,(
% 44.82/6.31 ~sQ992_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f7408])).
% 44.82/6.31 fof(f7421,definition,(
% 44.82/6.31 sQ999_spl <=> (v1_xboole_0(sK18_skl))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ999_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f7422,plain,(
% 44.82/6.31 v1_xboole_0(sK18_skl)|~sQ999_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f7421])).
% 44.82/6.31 fof(f7448,plain,(
% 44.82/6.31 $false|~sQ999_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f7422,f325])).
% 44.82/6.31 fof(f7449,plain,(
% 44.82/6.31 ~sQ999_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f7448])).
% 44.82/6.31 fof(f8455,plain,(
% 44.82/6.31 l1_struct_0(k1_lattice2(sK6_skl))),
% 44.82/6.31 inference(resolution,[status(thm)],[f4587,f191])).
% 44.82/6.31 fof(f8574,definition,(
% 44.82/6.31 sQ1166_spl <=> (v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK27_skl))))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ1166_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f8575,plain,(
% 44.82/6.31 v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK27_skl)))|~sQ1166_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f8574])).
% 44.82/6.31 fof(f8589,plain,(
% 44.82/6.31 $false|~sQ1166_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f8575,f249])).
% 44.82/6.31 fof(f8590,plain,(
% 44.82/6.31 ~sQ1166_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f8589])).
% 44.82/6.31 fof(f8599,plain,(
% 44.82/6.31 $false|sQ949_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f6963,f3267])).
% 44.82/6.31 fof(f8600,plain,(
% 44.82/6.31 sQ949_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f8599])).
% 44.82/6.31 fof(f8601,plain,(
% 44.82/6.31 $false|sQ948_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f6925,f2984])).
% 44.82/6.31 fof(f8602,plain,(
% 44.82/6.31 sQ948_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f8601])).
% 44.82/6.31 fof(f8612,plain,(
% 44.82/6.31 $false|sQ861_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f6437,f2766])).
% 44.82/6.31 fof(f8613,plain,(
% 44.82/6.31 sQ861_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f8612])).
% 44.82/6.31 fof(f9491,definition,(
% 44.82/6.31 sQ1181_spl <=> (l3_lattices(sK6_skl))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ1181_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f9493,plain,(
% 44.82/6.31 ~l3_lattices(sK6_skl)|sQ1181_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f9491])).
% 44.82/6.31 fof(f9495,plain,(
% 44.82/6.31 $false|sQ1181_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f9493,f223])).
% 44.82/6.31 fof(f9496,plain,(
% 44.82/6.31 sQ1181_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f9495])).
% 44.82/6.31 fof(f9965,plain,(
% 44.82/6.31 m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))),
% 44.82/6.31 inference(resolution,[status(thm)],[f1303,f387])).
% 44.82/6.31 fof(f9967,plain,(
% 44.82/6.31 $false|sQ455_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f9965,f3679])).
% 44.82/6.31 fof(f9968,plain,(
% 44.82/6.31 sQ455_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f9967])).
% 44.82/6.31 fof(f10112,plain,(
% 44.82/6.31 m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))),
% 44.82/6.31 inference(resolution,[status(thm)],[f1297,f387])).
% 44.82/6.31 fof(f10114,plain,(
% 44.82/6.31 $false|sQ453_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f10112,f3673])).
% 44.82/6.31 fof(f10115,plain,(
% 44.82/6.31 sQ453_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f10114])).
% 44.82/6.31 fof(f10150,plain,(
% 44.82/6.31 l1_struct_0(k1_lattice2(sK26_skl))),
% 44.82/6.31 inference(resolution,[status(thm)],[f4677,f191])).
% 44.82/6.31 fof(f10699,definition,(
% 44.82/6.31 sQ1297_spl <=> (m1_subset_1(sK10_skl(u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ1297_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f10701,plain,(
% 44.82/6.31 ~m1_subset_1(sK10_skl(u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|sQ1297_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f10699])).
% 44.82/6.31 fof(f10714,plain,(
% 44.82/6.31 $false|sQ1297_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f10701,f233])).
% 44.82/6.31 fof(f10715,plain,(
% 44.82/6.31 sQ1297_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f10714])).
% 44.82/6.31 fof(f10720,plain,(
% 44.82/6.31 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|k18_filter_2(sK0_skl,sK1_skl)=k2_filter_2(k1_lattice2(sK0_skl),k5_filter_2(sK0_skl,sK1_skl))|~sQ314_spl),
% 44.82/6.31 inference(resolution,[status(thm)],[f2645,f419])).
% 44.82/6.31 fof(f10738,definition,(
% 44.82/6.31 sQ1302_spl <=> (k18_filter_2(sK0_skl,sK1_skl)=k2_filter_2(k1_lattice2(sK0_skl),k5_filter_2(sK0_skl,sK1_skl)))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ1302_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f10739,plain,(
% 44.82/6.31 k18_filter_2(sK0_skl,sK1_skl)=k2_filter_2(k1_lattice2(sK0_skl),k5_filter_2(sK0_skl,sK1_skl))|~sQ1302_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f10738])).
% 44.82/6.31 fof(f10741,plain,(
% 44.82/6.31 sQ0_spl|~sQ1_spl|~sQ9_spl|sQ1302_spl|~sQ314_spl),
% 44.82/6.31 inference(split_clause,[status(thm)],[f10720,f451,f454,f494,f10738,f2644])).
% 44.82/6.31 fof(f10778,plain,(
% 44.82/6.31 k18_filter_2(sK0_skl,sK1_skl)=k2_filter_0(k1_lattice2(sK0_skl),sK1_skl)|~sQ37_spl|~sQ1302_spl|~sQ442_spl),
% 44.82/6.31 inference(backward_demodulation,[status(thm)],[f10779,f3580])).
% 44.82/6.31 fof(f10779,plain,(
% 44.82/6.31 k18_filter_2(sK0_skl,sK1_skl)=k2_filter_2(k1_lattice2(sK0_skl),sK1_skl)|~sQ37_spl|~sQ1302_spl),
% 44.82/6.31 inference(forward_demodulation,[status(thm)],[f648,f10739])).
% 44.82/6.31 fof(f10863,definition,(
% 44.82/6.31 sQ1311_spl <=> (k3_filter_2(k1_lattice2(sK0_skl),k7_filter_2(sK0_skl,sK2_skl))=k19_filter_2(sK0_skl,sK2_skl))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ1311_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f10864,plain,(
% 44.82/6.31 k3_filter_2(k1_lattice2(sK0_skl),k7_filter_2(sK0_skl,sK2_skl))=k19_filter_2(sK0_skl,sK2_skl)|~sQ1311_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f10863])).
% 44.82/6.31 fof(f10872,plain,(
% 44.82/6.31 k19_filter_2(sK0_skl,sK2_skl)=k3_filter_0(k1_lattice2(sK0_skl),sK2_skl)|~sQ38_spl|~sQ1311_spl|~sQ444_spl),
% 44.82/6.31 inference(backward_demodulation,[status(thm)],[f10873,f3595])).
% 44.82/6.31 fof(f10873,plain,(
% 44.82/6.31 k3_filter_2(k1_lattice2(sK0_skl),sK2_skl)=k19_filter_2(sK0_skl,sK2_skl)|~sQ38_spl|~sQ1311_spl),
% 44.82/6.31 inference(forward_demodulation,[status(thm)],[f653,f10864])).
% 44.82/6.31 fof(f11293,plain,(
% 44.82/6.31 v3_struct_0(sK0_skl)|~v6_lattices(sK0_skl)|~v8_lattices(sK0_skl)|~v9_lattices(sK0_skl)|~l3_lattices(sK0_skl)|r3_lattices(sK0_skl,sK1_skl,sK1_skl)|~sQ314_spl),
% 44.82/6.31 inference(resolution,[status(thm)],[f3781,f2645])).
% 44.82/6.31 fof(f11297,definition,(
% 44.82/6.31 sQ1370_spl <=> (r3_lattices(sK0_skl,sK1_skl,sK1_skl))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ1370_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f11298,plain,(
% 44.82/6.31 r3_lattices(sK0_skl,sK1_skl,sK1_skl)|~sQ1370_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f11297])).
% 44.82/6.31 fof(f11300,plain,(
% 44.82/6.31 sQ0_spl|~sQ4_spl|~sQ25_spl|~sQ27_spl|~sQ9_spl|sQ1370_spl|~sQ314_spl),
% 44.82/6.31 inference(split_clause,[status(thm)],[f11293,f451,f471,f571,f581,f494,f11297,f2644])).
% 44.82/6.31 fof(f11869,definition,(
% 44.82/6.31 sQ1448_spl <=> (v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK4_skl))))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ1448_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f11870,plain,(
% 44.82/6.31 v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK4_skl)))|~sQ1448_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f11869])).
% 44.82/6.31 fof(f11884,plain,(
% 44.82/6.31 $false|~sQ1448_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f11870,f249])).
% 44.82/6.31 fof(f11885,plain,(
% 44.82/6.31 ~sQ1448_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f11884])).
% 44.82/6.31 fof(f11943,definition,(
% 44.82/6.31 sQ1463_spl <=> (k1_lattice2(sK0_skl)=k1_lattice2(sK0_skl))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ1463_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f11945,plain,(
% 44.82/6.31 ~k1_lattice2(sK0_skl)=k1_lattice2(sK0_skl)|sQ1463_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f11943])).
% 44.82/6.31 fof(f11950,plain,(
% 44.82/6.31 $false|sQ1463_spl),
% 44.82/6.31 inference(trivial_equality_resolution,[status(thm)],[f11945])).
% 44.82/6.31 fof(f11951,plain,(
% 44.82/6.31 sQ1463_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f11950])).
% 44.82/6.31 fof(f12706,plain,(
% 44.82/6.31 v3_struct_0(k1_lattice2(sK0_skl))|~v10_lattices(k1_lattice2(sK0_skl))|~l3_lattices(k1_lattice2(sK0_skl))|~m1_subset_1(sK1_skl,u1_struct_0(k1_lattice2(sK0_skl)))|v1_xboole_0(k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),sK1_skl))|~m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0_skl))))|k3_filter_0(k1_lattice2(sK0_skl),k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),sK1_skl))=k2_filter_0(k1_lattice2(sK0_skl),sK1_skl)|~sQ16_spl|~sQ8_spl|~sQ119_spl),
% 44.82/6.31 inference(paramodulation,[status(thm)],[f4156,f449])).
% 44.82/6.31 fof(f12707,definition,(
% 44.82/6.31 sQ1488_spl <=> (v1_xboole_0(k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),sK1_skl)))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ1488_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f12708,plain,(
% 44.82/6.31 v1_xboole_0(k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),sK1_skl))|~sQ1488_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f12707])).
% 44.82/6.31 fof(f12710,definition,(
% 44.82/6.31 sQ1489_spl <=> (m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0_skl)))))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ1489_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f12712,plain,(
% 44.82/6.31 ~m1_subset_1(sK2_skl,k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0_skl))))|sQ1489_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f12710])).
% 44.82/6.31 fof(f12713,definition,(
% 44.82/6.31 sQ1490_spl <=> (k3_filter_0(k1_lattice2(sK0_skl),k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),sK1_skl))=k2_filter_0(k1_lattice2(sK0_skl),sK1_skl))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ1490_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f12714,plain,(
% 44.82/6.31 k3_filter_0(k1_lattice2(sK0_skl),k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),sK1_skl))=k2_filter_0(k1_lattice2(sK0_skl),sK1_skl)|~sQ1490_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f12713])).
% 44.82/6.31 fof(f12716,plain,(
% 44.82/6.31 sQ73_spl|~sQ74_spl|~sQ71_spl|~sQ969_spl|sQ1488_spl|~sQ1489_spl|sQ1490_spl|~sQ16_spl|~sQ8_spl|~sQ119_spl),
% 44.82/6.31 inference(split_clause,[status(thm)],[f12706,f958,f961,f940,f7213,f12707,f12710,f12713,f528,f487,f1224])).
% 44.82/6.31 fof(f12717,plain,(
% 44.82/6.31 k3_filter_0(k1_lattice2(sK0_skl),sK2_skl)=k2_filter_0(k1_lattice2(sK0_skl),sK1_skl)|~sQ16_spl|~sQ8_spl|~sQ119_spl|~sQ1490_spl),
% 44.82/6.31 inference(forward_demodulation,[status(thm)],[f4156,f12714])).
% 44.82/6.31 fof(f12718,plain,(
% 44.82/6.31 k18_filter_2(sK0_skl,sK1_skl)=k19_filter_2(sK0_skl,sK2_skl)|~sQ38_spl|~sQ1311_spl|~sQ444_spl|~sQ16_spl|~sQ8_spl|~sQ119_spl|~sQ1490_spl|~sQ37_spl|~sQ1302_spl|~sQ442_spl),
% 44.82/6.31 inference(backward_demodulation,[status(thm)],[f12719,f10778])).
% 44.82/6.31 fof(f12719,plain,(
% 44.82/6.31 k19_filter_2(sK0_skl,sK2_skl)=k2_filter_0(k1_lattice2(sK0_skl),sK1_skl)|~sQ38_spl|~sQ1311_spl|~sQ444_spl|~sQ16_spl|~sQ8_spl|~sQ119_spl|~sQ1490_spl),
% 44.82/6.31 inference(forward_demodulation,[status(thm)],[f10872,f12717])).
% 44.82/6.31 fof(f12720,plain,(
% 44.82/6.31 $false|~sQ16_spl|~sQ8_spl|~sQ119_spl|~sQ118_spl|sQ1489_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f12712,f4154])).
% 44.82/6.31 fof(f12721,plain,(
% 44.82/6.31 ~sQ16_spl|~sQ8_spl|~sQ119_spl|~sQ118_spl|sQ1489_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f12720])).
% 44.82/6.31 fof(f12722,plain,(
% 44.82/6.31 v1_xboole_0(sK2_skl)|~sQ16_spl|~sQ8_spl|~sQ119_spl|~sQ1488_spl),
% 44.82/6.31 inference(forward_demodulation,[status(thm)],[f4156,f12708])).
% 44.82/6.31 fof(f12723,plain,(
% 44.82/6.31 $false|~sQ16_spl|~sQ8_spl|~sQ119_spl|~sQ1488_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f12722,f120])).
% 44.82/6.31 fof(f12724,plain,(
% 44.82/6.31 ~sQ16_spl|~sQ8_spl|~sQ119_spl|~sQ1488_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f12723])).
% 44.82/6.31 fof(f12727,plain,(
% 44.82/6.31 m1_subset_1(k19_filter_2(sK0_skl,sK2_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ38_spl|~sQ1311_spl|~sQ444_spl|~sQ16_spl|~sQ8_spl|~sQ119_spl|~sQ1490_spl|~sQ37_spl|~sQ1302_spl|~sQ442_spl|~sQ33_spl),
% 44.82/6.31 inference(backward_demodulation,[status(thm)],[f12718,f617])).
% 44.82/6.31 fof(f12729,plain,(
% 44.82/6.31 ~r1_filter_2(u1_struct_0(sK0_skl),k19_filter_2(sK0_skl,sK2_skl),k19_filter_2(sK0_skl,sK2_skl))|~sQ38_spl|~sQ1311_spl|~sQ444_spl|~sQ16_spl|~sQ8_spl|~sQ119_spl|~sQ1490_spl|~sQ37_spl|~sQ1302_spl|~sQ442_spl),
% 44.82/6.31 inference(backward_demodulation,[status(thm)],[f12718,f123])).
% 44.82/6.31 fof(f12779,plain,(
% 44.82/6.31 $false|sQ34_spl|~sQ38_spl|~sQ1311_spl|~sQ444_spl|~sQ16_spl|~sQ8_spl|~sQ119_spl|~sQ1490_spl|~sQ37_spl|~sQ1302_spl|~sQ442_spl|~sQ33_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f12727,f621])).
% 44.82/6.31 fof(f12780,plain,(
% 44.82/6.31 sQ34_spl|~sQ38_spl|~sQ1311_spl|~sQ444_spl|~sQ16_spl|~sQ8_spl|~sQ119_spl|~sQ1490_spl|~sQ37_spl|~sQ1302_spl|~sQ442_spl|~sQ33_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f12779])).
% 44.82/6.31 fof(f12805,plain,(
% 44.82/6.31 v1_xboole_0(u1_struct_0(sK0_skl))|r1_filter_2(u1_struct_0(sK0_skl),k19_filter_2(sK0_skl,sK2_skl),k19_filter_2(sK0_skl,sK2_skl))|~sQ34_spl),
% 44.82/6.31 inference(resolution,[status(thm)],[f620,f448])).
% 44.82/6.31 fof(f12848,definition,(
% 44.82/6.31 sQ1500_spl <=> (r1_filter_2(u1_struct_0(sK0_skl),k19_filter_2(sK0_skl,sK2_skl),k19_filter_2(sK0_skl,sK2_skl)))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ1500_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f12849,plain,(
% 44.82/6.31 r1_filter_2(u1_struct_0(sK0_skl),k19_filter_2(sK0_skl,sK2_skl),k19_filter_2(sK0_skl,sK2_skl))|~sQ1500_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f12848])).
% 44.82/6.31 fof(f12851,plain,(
% 44.82/6.31 sQ7_spl|sQ1500_spl|~sQ34_spl),
% 44.82/6.31 inference(split_clause,[status(thm)],[f12805,f484,f12848,f619])).
% 44.82/6.31 fof(f13339,definition,(
% 44.82/6.31 sQ1568_spl <=> (m1_subset_1(sK10_skl(u1_struct_0(k1_lattice2(sK0_skl))),u1_struct_0(k1_lattice2(sK0_skl))))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ1568_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f13341,plain,(
% 44.82/6.31 ~m1_subset_1(sK10_skl(u1_struct_0(k1_lattice2(sK0_skl))),u1_struct_0(k1_lattice2(sK0_skl)))|sQ1568_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f13339])).
% 44.82/6.31 fof(f13354,plain,(
% 44.82/6.31 $false|sQ1568_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f13341,f233])).
% 44.82/6.31 fof(f13355,plain,(
% 44.82/6.31 sQ1568_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f13354])).
% 44.82/6.31 fof(f13363,definition,(
% 44.82/6.31 sQ1572_spl <=> (l1_struct_0(sK5_skl))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ1572_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f13365,plain,(
% 44.82/6.31 ~l1_struct_0(sK5_skl)|sQ1572_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f13363])).
% 44.82/6.31 fof(f13416,plain,(
% 44.82/6.31 $false|sQ1572_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f13365,f1019])).
% 44.82/6.31 fof(f13417,plain,(
% 44.82/6.31 sQ1572_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f13416])).
% 44.82/6.31 fof(f13423,definition,(
% 44.82/6.31 sQ1573_spl <=> (l1_struct_0(sK3_skl))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ1573_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f13425,plain,(
% 44.82/6.31 ~l1_struct_0(sK3_skl)|sQ1573_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f13423])).
% 44.82/6.31 fof(f13476,plain,(
% 44.82/6.31 $false|sQ1573_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f13425,f1018])).
% 44.82/6.31 fof(f13477,plain,(
% 44.82/6.31 sQ1573_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f13476])).
% 44.82/6.31 fof(f13483,definition,(
% 44.82/6.31 sQ1574_spl <=> (l1_struct_0(sK27_skl))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ1574_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f13485,plain,(
% 44.82/6.31 ~l1_struct_0(sK27_skl)|sQ1574_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f13483])).
% 44.82/6.31 fof(f13522,plain,(
% 44.82/6.31 $false|sQ1574_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f13485,f353])).
% 44.82/6.31 fof(f13523,plain,(
% 44.82/6.31 sQ1574_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f13522])).
% 44.82/6.31 fof(f14059,definition,(
% 44.82/6.31 sQ1613_spl <=> (sK22_skl=sK20_skl)),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ1613_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f14060,plain,(
% 44.82/6.31 sK22_skl=sK20_skl|~sQ1613_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f14059])).
% 44.82/6.31 fof(f14260,plain,(
% 44.82/6.31 ~v1_realset1(sK20_skl)|~sQ1613_spl),
% 44.82/6.31 inference(backward_demodulation,[status(thm)],[f14060,f339])).
% 44.82/6.31 fof(f14796,plain,(
% 44.82/6.31 $false|~sQ1613_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f798,f14260])).
% 44.82/6.31 fof(f14797,plain,(
% 44.82/6.31 ~sQ1613_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f14796])).
% 44.82/6.31 fof(f15763,definition,(
% 44.82/6.31 sQ1657_spl <=> (l1_struct_0(k1_lattice2(sK26_skl)))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ1657_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f15765,plain,(
% 44.82/6.31 ~l1_struct_0(k1_lattice2(sK26_skl))|sQ1657_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f15763])).
% 44.82/6.31 fof(f15867,plain,(
% 44.82/6.31 $false|sQ1657_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f15765,f10150])).
% 44.82/6.31 fof(f15868,plain,(
% 44.82/6.31 sQ1657_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f15867])).
% 44.82/6.31 fof(f15874,definition,(
% 44.82/6.31 sQ1658_spl <=> (l1_struct_0(k1_lattice2(sK6_skl)))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ1658_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f15876,plain,(
% 44.82/6.31 ~l1_struct_0(k1_lattice2(sK6_skl))|sQ1658_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f15874])).
% 44.82/6.31 fof(f15978,plain,(
% 44.82/6.31 $false|sQ1658_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f15876,f8455])).
% 44.82/6.31 fof(f15979,plain,(
% 44.82/6.31 sQ1658_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f15978])).
% 44.82/6.31 fof(f16085,plain,(
% 44.82/6.31 v1_xboole_0(k1_tarski(sK20_skl))|~sQ513_spl),
% 44.82/6.31 inference(resolution,[status(thm)],[f3801,f4248])).
% 44.82/6.31 fof(f16086,plain,(
% 44.82/6.31 v1_xboole_0(k1_tarski(sK2_skl))|~sQ515_spl),
% 44.82/6.31 inference(resolution,[status(thm)],[f3801,f4255])).
% 44.82/6.31 fof(f16102,plain,(
% 44.82/6.31 $false|~sQ513_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f16085,f259])).
% 44.82/6.31 fof(f16103,plain,(
% 44.82/6.31 ~sQ513_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f16102])).
% 44.82/6.31 fof(f16104,plain,(
% 44.82/6.31 $false|~sQ515_spl),
% 44.82/6.31 inference(forward_subsumption_resolution,[status(thm)],[f16086,f259])).
% 44.82/6.31 fof(f16105,plain,(
% 44.82/6.31 ~sQ515_spl),
% 44.82/6.31 inference(contradiction_clause,[status(thm)],[f16104])).
% 44.82/6.31 fof(f16181,plain,(
% 44.82/6.31 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))|r2_hidden(sK1_skl,a_2_0_filter_2(sK0_skl,sK1_skl))|~m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))|~sQ1370_spl),
% 44.82/6.31 inference(resolution,[status(thm)],[f11298,f446])).
% 44.82/6.31 fof(f16187,definition,(
% 44.82/6.31 sQ1667_spl <=> (r2_hidden(sK1_skl,a_2_0_filter_2(sK0_skl,sK1_skl)))),
% 44.82/6.31 introduced(definition,[new_symbols(definition,[sQ1667_spl])],[split_symbol_definition])).
% 44.82/6.31 fof(f16188,plain,(
% 44.82/6.31 r2_hidden(sK1_skl,a_2_0_filter_2(sK0_skl,sK1_skl))|~sQ1667_spl),
% 44.82/6.31 inference(component_clause,[status(thm)],[f16187])).
% 44.82/6.31 fof(f16190,plain,(
% 44.82/6.31 sQ0_spl|~sQ1_spl|~sQ9_spl|~sQ314_spl|sQ1667_spl|~sQ1370_spl),
% 44.82/6.31 inference(split_clause,[status(thm)],[f16181,f451,f454,f494,f2644,f16187,f11297])).
% 44.82/6.31 fof(f16198,plain,(
% 44.82/6.31 r2_hidden(sK1_skl,k18_filter_2(sK0_skl,sK1_skl))|~sQ10_spl|~sQ1667_spl),
% 44.82/6.31 inference(forward_demodulation,[status(thm)],[f498,f16188])).
% 42.82/6.36 fof(f16199,plain,(
% 42.82/6.36 $false|~sQ512_spl|~sQ10_spl|~sQ1667_spl),
% 42.82/6.36 inference(forward_subsumption_resolution,[status(thm)],[f16198,f4244])).
% 42.82/6.36 fof(f16200,plain,(
% 42.82/6.36 ~sQ512_spl|~sQ10_spl|~sQ1667_spl),
% 42.82/6.36 inference(contradiction_clause,[status(thm)],[f16199])).
% 42.82/6.36 fof(f16338,definition,(
% 42.82/6.36 sQ1688_spl <=> (l1_struct_0(sK4_skl))),
% 42.82/6.36 introduced(definition,[new_symbols(definition,[sQ1688_spl])],[split_symbol_definition])).
% 42.82/6.36 fof(f16340,plain,(
% 42.82/6.36 ~l1_struct_0(sK4_skl)|sQ1688_spl),
% 42.82/6.36 inference(component_clause,[status(thm)],[f16338])).
% 42.82/6.36 fof(f16371,plain,(
% 42.82/6.36 $false|sQ1688_spl),
% 42.82/6.36 inference(forward_subsumption_resolution,[status(thm)],[f16340,f219])).
% 42.82/6.36 fof(f16372,plain,(
% 42.82/6.36 sQ1688_spl),
% 42.82/6.36 inference(contradiction_clause,[status(thm)],[f16371])).
% 42.82/6.36 fof(f16411,plain,(
% 42.82/6.36 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|v1_xboole_0(sK2_skl)|k3_filter_2(k1_lattice2(sK0_skl),k7_filter_2(sK0_skl,sK2_skl))=k19_filter_2(sK0_skl,sK2_skl)|v1_xboole_0(u1_struct_0(k1_lattice2(sK0_skl)))|~sQ15_spl),
% 42.82/6.36 inference(resolution,[status(thm)],[f4040,f526])).
% 42.82/6.36 fof(f16426,plain,(
% 42.82/6.36 sQ0_spl|~sQ1_spl|~sQ9_spl|sQ90_spl|sQ1311_spl|sQ117_spl|~sQ15_spl),
% 42.82/6.36 inference(split_clause,[status(thm)],[f16411,f451,f454,f494,f1074,f10863,f1217,f525])).
% 42.82/6.36 fof(f16449,plain,(
% 42.82/6.36 $false|~sQ1500_spl|~sQ38_spl|~sQ1311_spl|~sQ444_spl|~sQ16_spl|~sQ8_spl|~sQ119_spl|~sQ1490_spl|~sQ37_spl|~sQ1302_spl|~sQ442_spl),
% 42.82/6.36 inference(forward_subsumption_resolution,[status(thm)],[f12729,f12849])).
% 42.82/6.36 fof(f16450,plain,(
% 42.82/6.36 ~sQ1500_spl|~sQ38_spl|~sQ1311_spl|~sQ444_spl|~sQ16_spl|~sQ8_spl|~sQ119_spl|~sQ1490_spl|~sQ37_spl|~sQ1302_spl|~sQ442_spl),
% 42.82/6.36 inference(contradiction_clause,[status(thm)],[f16449])).
% 42.82/6.36 fof(f16451,plain,(
% 42.82/6.36 $false),
% 42.82/6.36 inference(sat_refutation,[status(thm)],[f467,f469,f474,f490,f500,f502,f507,f517,f531,f574,f584,f650,f655,f728,f937,f948,f1073,f1096,f1158,f1223,f1227,f1760,f2322,f2642,f2792,f3582,f3597,f4104,f4246,f7229,f7330,f7369,f7409,f7449,f8590,f8600,f8602,f8613,f9496,f9968,f10115,f10715,f10741,f11300,f11885,f11951,f12716,f12721,f12724,f12780,f12851,f13355,f13417,f13477,f13523,f14797,f15868,f15979,f16103,f16105,f16190,f16200,f16372,f16426,f16450])).
% 42.82/6.36 % SZS output end CNFRefutation for theBenchmark.p
% 42.82/6.38 % Elapsed time: 5.854978 seconds
% 42.82/6.38 % CPU time: 46.092484 seconds
% 42.82/6.38 % Total memory used: 464.497 MB
% 42.82/6.38 % Net memory used: 444.207 MB
%------------------------------------------------------------------------------