%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT302+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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:35 PM UTC 2026
% Result : Theorem 10.10s 1.83s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT302+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.39 % Computer : n003.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 20 23:32:45 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.19/0.41 % Drodi V4.1.1
% 10.10/1.83 % Refutation found
% 10.10/1.83 % SZS status Theorem for theBenchmark: Theorem is valid
% 10.10/1.83 % SZS output start CNFRefutation for theBenchmark
% 10.10/1.83 fof(f1,conjecture,(
% 10.10/1.83 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> ( v13_lattices(A)=> m2_filter_2(k6_domain_1(u1_struct_0(A),k5_lattices(A)),A) ) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f2,negated_conjecture,(
% 10.10/1.83 ~((! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> ( v13_lattices(A)=> m2_filter_2(k6_domain_1(u1_struct_0(A),k5_lattices(A)),A) ) ) ))),
% 10.10/1.83 inference(negated_conjecture,[status(cth)],[f1])).
% 10.10/1.83 fof(f15,axiom,(
% 10.10/1.83 (! [A] :( l3_lattices(A)=> ( v3_lattices(k1_lattice2(A))& l3_lattices(k1_lattice2(A)) ) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f20,axiom,(
% 10.10/1.83 (! [A] :( ( ~ v3_struct_0(A)& l1_lattices(A) )=> m1_subset_1(k5_lattices(A),u1_struct_0(A)) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f21,axiom,(
% 10.10/1.83 (! [A,B] :( ( ~ v1_xboole_0(A)& m1_subset_1(B,A) )=> m1_subset_1(k6_domain_1(A,B),k1_zfmisc_1(A)) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f22,axiom,(
% 10.10/1.83 (! [A] :( ( ~ v3_struct_0(A)& l2_lattices(A) )=> m1_subset_1(k6_lattices(A),u1_struct_0(A)) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f23,axiom,(
% 10.10/1.83 (! [A] :( l1_lattices(A)=> l1_struct_0(A) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f25,axiom,(
% 10.10/1.83 (! [A] :( l2_lattices(A)=> l1_struct_0(A) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f26,axiom,(
% 10.10/1.83 (! [A] :( l3_lattices(A)=> ( l1_lattices(A)& l2_lattices(A) ) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f37,axiom,(
% 10.10/1.83 (? [A] : l1_lattices(A) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f39,axiom,(
% 10.10/1.83 (? [A] : l2_lattices(A) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f40,axiom,(
% 10.10/1.83 (? [A] : l3_lattices(A) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f44,axiom,(
% 10.10/1.83 (! [A] :(? [B] : m1_subset_1(B,A) ))),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f48,axiom,(
% 10.10/1.83 (! [A] :( ( ~ v3_struct_0(A)& l3_lattices(A) )=> ( ~ v3_struct_0(k1_lattice2(A))& v3_lattices(k1_lattice2(A)) ) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f49,axiom,(
% 10.10/1.83 (! [A] :( ( ~ v3_struct_0(A)& l1_struct_0(A) )=> ~ v1_xboole_0(u1_struct_0(A)) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f50,axiom,(
% 10.10/1.83 (! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f60,axiom,(
% 10.10/1.83 (! [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)) ) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f62,axiom,(
% 10.10/1.83 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v3_lattices(A)& v4_lattices(A)& v5_lattices(A)& v6_lattices(A)& v7_lattices(A)& v8_lattices(A)& v9_lattices(A)& v10_lattices(A)& v13_lattices(A)& v14_lattices(A)& v15_lattices(A) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f65,axiom,(
% 10.10/1.83 (? [A] :( ~ v1_xboole_0(A)& v1_realset1(A) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f67,axiom,(
% 10.10/1.83 (? [A] : v1_xboole_0(A) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f68,axiom,(
% 10.10/1.83 (? [A] :( v1_relat_1(A)& v1_xboole_0(A)& v1_funct_1(A) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f69,axiom,(
% 10.10/1.83 (? [A] :( ~ v1_xboole_0(A)& ~ v1_realset1(A) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f70,axiom,(
% 10.10/1.83 (! [A] :(? [B] :( m1_subset_1(B,k1_zfmisc_1(A))& v1_xboole_0(B) ) ))),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f71,axiom,(
% 10.10/1.83 (? [A] : ~ v1_xboole_0(A) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f73,axiom,(
% 10.10/1.83 (? [A] :( l3_lattices(A)& v3_lattices(A) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f74,axiom,(
% 10.10/1.83 (? [A] :( l1_struct_0(A)& ~ v3_struct_0(A) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f76,axiom,(
% 10.10/1.83 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v3_lattices(A) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f77,axiom,(
% 10.10/1.83 (? [A] :( l3_lattices(A)& ~ v3_struct_0(A)& v3_lattices(A)& v4_lattices(A)& v5_lattices(A)& v6_lattices(A)& v7_lattices(A)& v8_lattices(A)& v9_lattices(A)& v10_lattices(A) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f78,axiom,(
% 10.10/1.83 (! [A,B] :( ( ~ v1_xboole_0(A)& m1_subset_1(B,A) )=> k6_domain_1(A,B) = k1_tarski(B) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f79,axiom,(
% 10.10/1.83 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_filter_2(B,A)<=> m1_filter_0(B,A) ) )) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f81,axiom,(
% 10.10/1.83 (! [A,B] : r1_tarski(A,A) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f82,axiom,(
% 10.10/1.83 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> ( ( ~ v3_struct_0(A)& v10_lattices(A)& v14_lattices(A)& l3_lattices(A) )=> m1_filter_0(k6_domain_1(u1_struct_0(A),k6_lattices(A)),A) ) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f83,axiom,(
% 10.10/1.83 (! [A,B] :( r2_hidden(A,B)=> m1_subset_1(A,B) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f84,axiom,(
% 10.10/1.83 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m2_filter_2(B,A)<=> m1_filter_2(B,k1_lattice2(A)) ) )) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f85,axiom,(
% 10.10/1.83 (! [A,B] :( m1_subset_1(A,B)=> ( v1_xboole_0(B)| r2_hidden(A,B) ) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f86,axiom,(
% 10.10/1.83 (! [A,B] :( m1_subset_1(A,k1_zfmisc_1(B))<=> r1_tarski(A,B) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f88,axiom,(
% 10.10/1.83 (! [A,B,C] :~ ( r2_hidden(A,B)& m1_subset_1(B,k1_zfmisc_1(C))& v1_xboole_0(C) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f89,axiom,(
% 10.10/1.83 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> ( v13_lattices(A)<=> v14_lattices(k1_lattice2(A)) ) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f90,axiom,(
% 10.10/1.83 (! [A] :( v1_xboole_0(A)=> A = k1_xboole_0 ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f91,axiom,(
% 10.10/1.83 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v13_lattices(A)& l3_lattices(A) )=> k5_lattices(A) = k6_lattices(k1_lattice2(A)) ) )),
% 10.10/1.83 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.10/1.83 fof(f94,plain,(
% 10.10/1.83 (?[A]: (((~v3_struct_0(A)&v10_lattices(A))&l3_lattices(A))&(v13_lattices(A)&~m2_filter_2(k6_domain_1(u1_struct_0(A),k5_lattices(A)),A))))),
% 10.10/1.83 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 10.10/1.83 fof(f95,plain,(
% 10.10/1.83 (((~v3_struct_0(sK0_skl)&v10_lattices(sK0_skl))&l3_lattices(sK0_skl))&(v13_lattices(sK0_skl)&~m2_filter_2(k6_domain_1(u1_struct_0(sK0_skl),k5_lattices(sK0_skl)),sK0_skl)))),
% 10.10/1.83 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(A,sK0_skl)],[f94])).
% 10.10/1.83 fof(f96,plain,(
% 10.10/1.83 ~v3_struct_0(sK0_skl)),
% 10.10/1.83 inference(cnf_transformation,[status(thm)],[f95])).
% 10.10/1.83 fof(f97,plain,(
% 10.10/1.83 v10_lattices(sK0_skl)),
% 10.10/1.83 inference(cnf_transformation,[status(thm)],[f95])).
% 10.10/1.83 fof(f98,plain,(
% 10.10/1.83 l3_lattices(sK0_skl)),
% 10.10/1.83 inference(cnf_transformation,[status(thm)],[f95])).
% 10.10/1.83 fof(f99,plain,(
% 10.10/1.83 v13_lattices(sK0_skl)),
% 10.10/1.83 inference(cnf_transformation,[status(thm)],[f95])).
% 10.10/1.83 fof(f100,plain,(
% 10.10/1.83 ~m2_filter_2(k6_domain_1(u1_struct_0(sK0_skl),k5_lattices(sK0_skl)),sK0_skl)),
% 10.10/1.83 inference(cnf_transformation,[status(thm)],[f95])).
% 10.10/1.83 fof(f139,plain,(
% 10.10/1.83 ![A]: (~l3_lattices(A)|(v3_lattices(k1_lattice2(A))&l3_lattices(k1_lattice2(A))))),
% 10.10/1.83 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 10.10/1.83 fof(f141,plain,(
% 10.10/1.83 ![X0]: (~l3_lattices(X0)|l3_lattices(k1_lattice2(X0)))),
% 10.10/1.83 inference(cnf_transformation,[status(thm)],[f139])).
% 10.10/1.83 fof(f142,plain,(
% 10.10/1.83 ![A]: ((v3_struct_0(A)|~l1_lattices(A))|m1_subset_1(k5_lattices(A),u1_struct_0(A)))),
% 10.10/1.83 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 10.10/1.83 fof(f143,plain,(
% 10.10/1.83 ![X0]: (v3_struct_0(X0)|~l1_lattices(X0)|m1_subset_1(k5_lattices(X0),u1_struct_0(X0)))),
% 10.10/1.83 inference(cnf_transformation,[status(thm)],[f142])).
% 10.10/1.83 fof(f144,plain,(
% 10.10/1.83 ![A,B]: ((v1_xboole_0(A)|~m1_subset_1(B,A))|m1_subset_1(k6_domain_1(A,B),k1_zfmisc_1(A)))),
% 10.10/1.83 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 10.10/1.83 fof(f145,plain,(
% 10.10/1.83 ![X0,X1]: (v1_xboole_0(X0)|~m1_subset_1(X1,X0)|m1_subset_1(k6_domain_1(X0,X1),k1_zfmisc_1(X0)))),
% 10.10/1.83 inference(cnf_transformation,[status(thm)],[f144])).
% 10.10/1.83 fof(f146,plain,(
% 10.10/1.83 ![A]: ((v3_struct_0(A)|~l2_lattices(A))|m1_subset_1(k6_lattices(A),u1_struct_0(A)))),
% 10.10/1.83 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 10.10/1.83 fof(f147,plain,(
% 10.10/1.83 ![X0]: (v3_struct_0(X0)|~l2_lattices(X0)|m1_subset_1(k6_lattices(X0),u1_struct_0(X0)))),
% 10.10/1.83 inference(cnf_transformation,[status(thm)],[f146])).
% 10.10/1.83 fof(f148,plain,(
% 10.10/1.83 ![A]: (~l1_lattices(A)|l1_struct_0(A))),
% 10.10/1.83 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 10.10/1.83 fof(f149,plain,(
% 10.10/1.83 ![X0]: (~l1_lattices(X0)|l1_struct_0(X0))),
% 10.10/1.83 inference(cnf_transformation,[status(thm)],[f148])).
% 10.10/1.83 fof(f150,plain,(
% 10.10/1.83 ![A]: (~l2_lattices(A)|l1_struct_0(A))),
% 10.10/1.83 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 10.10/1.83 fof(f151,plain,(
% 10.10/1.83 ![X0]: (~l2_lattices(X0)|l1_struct_0(X0))),
% 10.10/1.83 inference(cnf_transformation,[status(thm)],[f150])).
% 10.10/1.83 fof(f152,plain,(
% 10.10/1.83 ![A]: (~l3_lattices(A)|(l1_lattices(A)&l2_lattices(A)))),
% 10.10/1.83 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 10.10/1.83 fof(f153,plain,(
% 10.10/1.83 ![X0]: (~l3_lattices(X0)|l1_lattices(X0))),
% 10.10/1.83 inference(cnf_transformation,[status(thm)],[f152])).
% 10.10/1.83 fof(f154,plain,(
% 10.10/1.83 ![X0]: (~l3_lattices(X0)|l2_lattices(X0))),
% 10.10/1.83 inference(cnf_transformation,[status(thm)],[f152])).
% 10.10/1.83 fof(f176,plain,(
% 10.10/1.83 l1_lattices(sK1_skl)),
% 10.10/1.83 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(A,sK1_skl)],[f37])).
% 10.10/1.83 fof(f177,plain,(
% 10.10/1.83 l1_lattices(sK1_skl)),
% 10.10/1.83 inference(cnf_transformation,[status(thm)],[f176])).
% 10.10/1.83 fof(f180,plain,(
% 10.10/1.83 l2_lattices(sK3_skl)),
% 10.10/1.83 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(A,sK3_skl)],[f39])).
% 10.10/1.83 fof(f181,plain,(
% 10.10/1.83 l2_lattices(sK3_skl)),
% 10.10/1.83 inference(cnf_transformation,[status(thm)],[f180])).
% 10.10/1.83 fof(f182,plain,(
% 10.10/1.83 l3_lattices(sK4_skl)),
% 10.10/1.83 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(A,sK4_skl)],[f40])).
% 10.10/1.83 fof(f183,plain,(
% 10.10/1.83 l3_lattices(sK4_skl)),
% 10.10/1.83 inference(cnf_transformation,[status(thm)],[f182])).
% 10.10/1.83 fof(f192,plain,(
% 10.10/1.83 ![A]: m1_subset_1(sK8_skl(A),A)),
% 10.10/1.83 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(B,sK8_skl(A))],[f44])).
% 10.10/1.83 fof(f193,plain,(
% 10.10/1.83 ![X0]: (m1_subset_1(sK8_skl(X0),X0))),
% 10.10/1.83 inference(cnf_transformation,[status(thm)],[f192])).
% 10.10/1.83 fof(f202,plain,(
% 10.10/1.83 ![A]: ((v3_struct_0(A)|~l3_lattices(A))|(~v3_struct_0(k1_lattice2(A))&v3_lattices(k1_lattice2(A))))),
% 10.10/1.83 inference(pre_NNF_transformation,[status(thm)],[f48])).
% 10.10/1.83 fof(f203,plain,(
% 10.10/1.83 ![X0]: (v3_struct_0(X0)|~l3_lattices(X0)|~v3_struct_0(k1_lattice2(X0)))),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f202])).
% 10.10/1.84 fof(f205,plain,(
% 10.10/1.84 ![A]: ((v3_struct_0(A)|~l1_struct_0(A))|~v1_xboole_0(u1_struct_0(A)))),
% 10.10/1.84 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 10.10/1.84 fof(f206,plain,(
% 10.10/1.84 ![X0]: (v3_struct_0(X0)|~l1_struct_0(X0)|~v1_xboole_0(u1_struct_0(X0)))),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f205])).
% 10.10/1.84 fof(f207,plain,(
% 10.10/1.84 ![X0]: (~v1_xboole_0(k1_zfmisc_1(X0)))),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f50])).
% 10.10/1.84 fof(f243,plain,(
% 10.10/1.84 ![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))))),
% 10.10/1.84 inference(pre_NNF_transformation,[status(thm)],[f60])).
% 10.10/1.84 fof(f252,plain,(
% 10.10/1.84 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v10_lattices(k1_lattice2(X0)))),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f243])).
% 10.10/1.84 fof(f257,plain,(
% 10.10/1.84 ((((((((((((l3_lattices(sK12_skl)&~v3_struct_0(sK12_skl))&v3_lattices(sK12_skl))&v4_lattices(sK12_skl))&v5_lattices(sK12_skl))&v6_lattices(sK12_skl))&v7_lattices(sK12_skl))&v8_lattices(sK12_skl))&v9_lattices(sK12_skl))&v10_lattices(sK12_skl))&v13_lattices(sK12_skl))&v14_lattices(sK12_skl))&v15_lattices(sK12_skl))),
% 10.10/1.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(A,sK12_skl)],[f62])).
% 10.10/1.84 fof(f258,plain,(
% 10.10/1.84 l3_lattices(sK12_skl)),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f257])).
% 10.10/1.84 fof(f278,plain,(
% 10.10/1.84 (~v1_xboole_0(sK15_skl)&v1_realset1(sK15_skl))),
% 10.10/1.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(A,sK15_skl)],[f65])).
% 10.10/1.84 fof(f279,plain,(
% 10.10/1.84 ~v1_xboole_0(sK15_skl)),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f278])).
% 10.10/1.84 fof(f285,plain,(
% 10.10/1.84 v1_xboole_0(sK17_skl)),
% 10.10/1.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(A,sK17_skl)],[f67])).
% 10.10/1.84 fof(f286,plain,(
% 10.10/1.84 v1_xboole_0(sK17_skl)),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f285])).
% 10.10/1.84 fof(f287,plain,(
% 10.10/1.84 ((v1_relat_1(sK18_skl)&v1_xboole_0(sK18_skl))&v1_funct_1(sK18_skl))),
% 10.10/1.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(A,sK18_skl)],[f68])).
% 10.10/1.84 fof(f288,plain,(
% 10.10/1.84 v1_relat_1(sK18_skl)),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f287])).
% 10.10/1.84 fof(f289,plain,(
% 10.10/1.84 v1_xboole_0(sK18_skl)),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f287])).
% 10.10/1.84 fof(f291,plain,(
% 10.10/1.84 (~v1_xboole_0(sK19_skl)&~v1_realset1(sK19_skl))),
% 10.10/1.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl]),skolemize(A,sK19_skl)],[f69])).
% 10.10/1.84 fof(f292,plain,(
% 10.10/1.84 ~v1_xboole_0(sK19_skl)),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f291])).
% 10.10/1.84 fof(f294,plain,(
% 10.10/1.84 ![A]: (m1_subset_1(sK20_skl(A),k1_zfmisc_1(A))&v1_xboole_0(sK20_skl(A)))),
% 10.10/1.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(B,sK20_skl(A))],[f70])).
% 10.10/1.84 fof(f295,plain,(
% 10.10/1.84 ![X0]: (m1_subset_1(sK20_skl(X0),k1_zfmisc_1(X0)))),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f294])).
% 10.10/1.84 fof(f296,plain,(
% 10.10/1.84 ![X0]: (v1_xboole_0(sK20_skl(X0)))),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f294])).
% 10.10/1.84 fof(f297,plain,(
% 10.10/1.84 ~v1_xboole_0(sK21_skl)),
% 10.10/1.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(A,sK21_skl)],[f71])).
% 10.10/1.84 fof(f298,plain,(
% 10.10/1.84 ~v1_xboole_0(sK21_skl)),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f297])).
% 10.10/1.84 fof(f303,plain,(
% 10.10/1.84 (l3_lattices(sK23_skl)&v3_lattices(sK23_skl))),
% 10.10/1.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(A,sK23_skl)],[f73])).
% 10.10/1.84 fof(f304,plain,(
% 10.10/1.84 l3_lattices(sK23_skl)),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f303])).
% 10.10/1.84 fof(f306,plain,(
% 10.10/1.84 (l1_struct_0(sK24_skl)&~v3_struct_0(sK24_skl))),
% 10.10/1.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(A,sK24_skl)],[f74])).
% 10.10/1.84 fof(f307,plain,(
% 10.10/1.84 l1_struct_0(sK24_skl)),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f306])).
% 10.10/1.84 fof(f308,plain,(
% 10.10/1.84 ~v3_struct_0(sK24_skl)),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f306])).
% 10.10/1.84 fof(f313,plain,(
% 10.10/1.84 ((l3_lattices(sK26_skl)&~v3_struct_0(sK26_skl))&v3_lattices(sK26_skl))),
% 10.10/1.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl]),skolemize(A,sK26_skl)],[f76])).
% 10.10/1.84 fof(f314,plain,(
% 10.10/1.84 l3_lattices(sK26_skl)),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f313])).
% 10.10/1.84 fof(f317,plain,(
% 10.10/1.84 (((((((((l3_lattices(sK27_skl)&~v3_struct_0(sK27_skl))&v3_lattices(sK27_skl))&v4_lattices(sK27_skl))&v5_lattices(sK27_skl))&v6_lattices(sK27_skl))&v7_lattices(sK27_skl))&v8_lattices(sK27_skl))&v9_lattices(sK27_skl))&v10_lattices(sK27_skl))),
% 10.10/1.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl]),skolemize(A,sK27_skl)],[f77])).
% 10.10/1.84 fof(f318,plain,(
% 10.10/1.84 l3_lattices(sK27_skl)),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f317])).
% 10.10/1.84 fof(f328,plain,(
% 10.10/1.84 ![A,B]: ((v1_xboole_0(A)|~m1_subset_1(B,A))|k6_domain_1(A,B)=k1_tarski(B))),
% 10.10/1.84 inference(pre_NNF_transformation,[status(thm)],[f78])).
% 10.10/1.84 fof(f329,plain,(
% 10.10/1.84 ![X0,X1]: (v1_xboole_0(X0)|~m1_subset_1(X1,X0)|k6_domain_1(X0,X1)=k1_tarski(X1))),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f328])).
% 10.10/1.84 fof(f330,plain,(
% 10.10/1.84 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (m1_filter_2(B,A)<=>m1_filter_0(B,A))))),
% 10.10/1.84 inference(pre_NNF_transformation,[status(thm)],[f79])).
% 10.10/1.84 fof(f331,plain,(
% 10.10/1.84 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: ((~m1_filter_2(B,A)|m1_filter_0(B,A))&(m1_filter_2(B,A)|~m1_filter_0(B,A)))))),
% 10.10/1.84 inference(NNF_transformation,[status(thm)],[f330])).
% 10.10/1.84 fof(f332,plain,(
% 10.10/1.84 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|((![B]: (~m1_filter_2(B,A)|m1_filter_0(B,A)))&(![B]: (m1_filter_2(B,A)|~m1_filter_0(B,A)))))),
% 10.10/1.84 inference(miniscoping,[status(thm)],[f331])).
% 10.10/1.84 fof(f334,plain,(
% 10.10/1.84 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|m1_filter_2(X1,X0)|~m1_filter_0(X1,X0))),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f332])).
% 10.10/1.84 fof(f339,plain,(
% 10.10/1.84 ![A]: r1_tarski(A,A)),
% 10.10/1.84 inference(miniscoping,[status(thm)],[f81])).
% 10.10/1.84 fof(f340,plain,(
% 10.10/1.84 ![X0]: (r1_tarski(X0,X0))),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f339])).
% 10.10/1.84 fof(f341,plain,(
% 10.10/1.84 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|((((v3_struct_0(A)|~v10_lattices(A))|~v14_lattices(A))|~l3_lattices(A))|m1_filter_0(k6_domain_1(u1_struct_0(A),k6_lattices(A)),A)))),
% 10.10/1.84 inference(pre_NNF_transformation,[status(thm)],[f82])).
% 10.10/1.84 fof(f342,plain,(
% 10.10/1.84 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v3_struct_0(X0)|~v10_lattices(X0)|~v14_lattices(X0)|~l3_lattices(X0)|m1_filter_0(k6_domain_1(u1_struct_0(X0),k6_lattices(X0)),X0))),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f341])).
% 10.10/1.84 fof(f343,plain,(
% 10.10/1.84 ![A,B]: (~r2_hidden(A,B)|m1_subset_1(A,B))),
% 10.10/1.84 inference(pre_NNF_transformation,[status(thm)],[f83])).
% 10.10/1.84 fof(f344,plain,(
% 10.10/1.84 ![X0,X1]: (~r2_hidden(X0,X1)|m1_subset_1(X0,X1))),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f343])).
% 10.10/1.84 fof(f345,plain,(
% 10.10/1.84 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (m2_filter_2(B,A)<=>m1_filter_2(B,k1_lattice2(A)))))),
% 10.10/1.84 inference(pre_NNF_transformation,[status(thm)],[f84])).
% 10.10/1.84 fof(f346,plain,(
% 10.10/1.84 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: ((~m2_filter_2(B,A)|m1_filter_2(B,k1_lattice2(A)))&(m2_filter_2(B,A)|~m1_filter_2(B,k1_lattice2(A))))))),
% 10.10/1.84 inference(NNF_transformation,[status(thm)],[f345])).
% 10.10/1.84 fof(f347,plain,(
% 10.10/1.84 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|((![B]: (~m2_filter_2(B,A)|m1_filter_2(B,k1_lattice2(A))))&(![B]: (m2_filter_2(B,A)|~m1_filter_2(B,k1_lattice2(A))))))),
% 10.10/1.84 inference(miniscoping,[status(thm)],[f346])).
% 10.10/1.84 fof(f349,plain,(
% 10.10/1.84 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|m2_filter_2(X1,X0)|~m1_filter_2(X1,k1_lattice2(X0)))),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f347])).
% 10.10/1.84 fof(f350,plain,(
% 10.10/1.84 ![A,B]: (~m1_subset_1(A,B)|(v1_xboole_0(B)|r2_hidden(A,B)))),
% 10.10/1.84 inference(pre_NNF_transformation,[status(thm)],[f85])).
% 10.10/1.84 fof(f351,plain,(
% 10.10/1.84 ![X0,X1]: (~m1_subset_1(X0,X1)|v1_xboole_0(X1)|r2_hidden(X0,X1))),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f350])).
% 10.10/1.84 fof(f352,plain,(
% 10.10/1.84 ![A,B]: ((~m1_subset_1(A,k1_zfmisc_1(B))|r1_tarski(A,B))&(m1_subset_1(A,k1_zfmisc_1(B))|~r1_tarski(A,B)))),
% 10.10/1.84 inference(NNF_transformation,[status(thm)],[f86])).
% 10.10/1.84 fof(f353,plain,(
% 10.10/1.84 (![A,B]: (~m1_subset_1(A,k1_zfmisc_1(B))|r1_tarski(A,B)))&(![A,B]: (m1_subset_1(A,k1_zfmisc_1(B))|~r1_tarski(A,B)))),
% 10.10/1.84 inference(miniscoping,[status(thm)],[f352])).
% 10.10/1.84 fof(f354,plain,(
% 10.10/1.84 ![X0,X1]: (~m1_subset_1(X0,k1_zfmisc_1(X1))|r1_tarski(X0,X1))),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f353])).
% 10.10/1.84 fof(f355,plain,(
% 10.10/1.84 ![X0,X1]: (m1_subset_1(X0,k1_zfmisc_1(X1))|~r1_tarski(X0,X1))),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f353])).
% 10.10/1.84 fof(f359,plain,(
% 10.10/1.84 ![A,B,C]: ((~r2_hidden(A,B)|~m1_subset_1(B,k1_zfmisc_1(C)))|~v1_xboole_0(C))),
% 10.10/1.84 inference(pre_NNF_transformation,[status(thm)],[f88])).
% 10.10/1.84 fof(f360,plain,(
% 10.10/1.84 ![C]: ((![B]: ((![A]: ~r2_hidden(A,B))|~m1_subset_1(B,k1_zfmisc_1(C))))|~v1_xboole_0(C))),
% 10.10/1.84 inference(miniscoping,[status(thm)],[f359])).
% 10.10/1.84 fof(f361,plain,(
% 10.10/1.84 ![X0,X1,X2]: (~r2_hidden(X0,X1)|~m1_subset_1(X1,k1_zfmisc_1(X2))|~v1_xboole_0(X2))),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f360])).
% 10.10/1.84 fof(f362,plain,(
% 10.10/1.84 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(v13_lattices(A)<=>v14_lattices(k1_lattice2(A))))),
% 10.10/1.84 inference(pre_NNF_transformation,[status(thm)],[f89])).
% 10.10/1.84 fof(f363,plain,(
% 10.10/1.84 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|((~v13_lattices(A)|v14_lattices(k1_lattice2(A)))&(v13_lattices(A)|~v14_lattices(k1_lattice2(A)))))),
% 10.10/1.84 inference(NNF_transformation,[status(thm)],[f362])).
% 10.10/1.84 fof(f364,plain,(
% 10.10/1.84 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~v13_lattices(X0)|v14_lattices(k1_lattice2(X0)))),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f363])).
% 10.10/1.84 fof(f366,plain,(
% 10.10/1.84 ![A]: (~v1_xboole_0(A)|A=k1_xboole_0)),
% 10.10/1.84 inference(pre_NNF_transformation,[status(thm)],[f90])).
% 10.10/1.84 fof(f367,plain,(
% 10.10/1.84 ![X0]: (~v1_xboole_0(X0)|X0=k1_xboole_0)),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f366])).
% 10.10/1.84 fof(f368,plain,(
% 10.10/1.84 ![A]: ((((v3_struct_0(A)|~v10_lattices(A))|~v13_lattices(A))|~l3_lattices(A))|k5_lattices(A)=k6_lattices(k1_lattice2(A)))),
% 10.10/1.84 inference(pre_NNF_transformation,[status(thm)],[f91])).
% 10.10/1.84 fof(f369,plain,(
% 10.10/1.84 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~v13_lattices(X0)|~l3_lattices(X0)|k5_lattices(X0)=k6_lattices(k1_lattice2(X0)))),
% 10.10/1.84 inference(cnf_transformation,[status(thm)],[f368])).
% 10.10/1.84 fof(f376,plain,(
% 10.10/1.84 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~v14_lattices(X0)|m1_filter_0(k6_domain_1(u1_struct_0(X0),k6_lattices(X0)),X0))),
% 10.10/1.84 inference(duplicate_literals_removal,[status(thm)],[f342])).
% 10.10/1.84 fof(f377,plain,(
% 10.10/1.84 ![X0]: (v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|m2_filter_2(X0,sK0_skl)|~m1_filter_2(X0,k1_lattice2(sK0_skl)))),
% 10.10/1.84 inference(resolution,[status(thm)],[f349,f98])).
% 10.10/1.84 fof(f378,definition,(
% 10.10/1.84 sQ0_spl <=> (v3_struct_0(sK0_skl))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f379,plain,(
% 10.10/1.84 v3_struct_0(sK0_skl)|~sQ0_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f378])).
% 10.10/1.84 fof(f381,definition,(
% 10.10/1.84 sQ1_spl <=> (v10_lattices(sK0_skl))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f383,plain,(
% 10.10/1.84 ~v10_lattices(sK0_skl)|sQ1_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f381])).
% 10.10/1.84 fof(f384,definition,(
% 10.10/1.84 ![X0]: (sQ2_spl <=> (m2_filter_2(X0,sK0_skl)|~m1_filter_2(X0,k1_lattice2(sK0_skl))))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f385,plain,(
% 10.10/1.84 ![X0]: (m2_filter_2(X0,sK0_skl)|~m1_filter_2(X0,k1_lattice2(sK0_skl))|~sQ2_spl)),
% 10.10/1.84 inference(component_clause,[status(thm)],[f384])).
% 10.10/1.84 fof(f387,plain,(
% 10.10/1.84 sQ0_spl|~sQ1_spl|sQ2_spl),
% 10.10/1.84 inference(split_clause,[status(thm)],[f377,f378,f381,f384])).
% 10.10/1.84 fof(f388,plain,(
% 10.10/1.84 ~v10_lattices(sK0_skl)|~v13_lattices(sK0_skl)|~l3_lattices(sK0_skl)|k5_lattices(sK0_skl)=k6_lattices(k1_lattice2(sK0_skl))),
% 10.10/1.84 inference(resolution,[status(thm)],[f369,f96])).
% 10.10/1.84 fof(f389,definition,(
% 10.10/1.84 sQ3_spl <=> (v13_lattices(sK0_skl))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f391,plain,(
% 10.10/1.84 ~v13_lattices(sK0_skl)|sQ3_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f389])).
% 10.10/1.84 fof(f392,definition,(
% 10.10/1.84 sQ4_spl <=> (l3_lattices(sK0_skl))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f394,plain,(
% 10.10/1.84 ~l3_lattices(sK0_skl)|sQ4_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f392])).
% 10.10/1.84 fof(f395,definition,(
% 10.10/1.84 sQ5_spl <=> (k5_lattices(sK0_skl)=k6_lattices(k1_lattice2(sK0_skl)))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f396,plain,(
% 10.10/1.84 k5_lattices(sK0_skl)=k6_lattices(k1_lattice2(sK0_skl))|~sQ5_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f395])).
% 10.10/1.84 fof(f398,plain,(
% 10.10/1.84 ~sQ1_spl|~sQ3_spl|~sQ4_spl|sQ5_spl),
% 10.10/1.84 inference(split_clause,[status(thm)],[f388,f381,f389,f392,f395])).
% 10.10/1.84 fof(f399,plain,(
% 10.10/1.84 $false|sQ1_spl),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f383,f97])).
% 10.10/1.84 fof(f400,plain,(
% 10.10/1.84 sQ1_spl),
% 10.10/1.84 inference(contradiction_clause,[status(thm)],[f399])).
% 10.10/1.84 fof(f401,plain,(
% 10.10/1.84 $false|~sQ0_spl),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f379,f96])).
% 10.10/1.84 fof(f402,plain,(
% 10.10/1.84 ~sQ0_spl),
% 10.10/1.84 inference(contradiction_clause,[status(thm)],[f401])).
% 10.10/1.84 fof(f408,plain,(
% 10.10/1.84 $false|sQ4_spl),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f394,f98])).
% 10.10/1.84 fof(f409,plain,(
% 10.10/1.84 sQ4_spl),
% 10.10/1.84 inference(contradiction_clause,[status(thm)],[f408])).
% 10.10/1.84 fof(f410,plain,(
% 10.10/1.84 $false|sQ3_spl),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f391,f99])).
% 10.10/1.84 fof(f411,plain,(
% 10.10/1.84 sQ3_spl),
% 10.10/1.84 inference(contradiction_clause,[status(thm)],[f410])).
% 10.10/1.84 fof(f413,plain,(
% 10.10/1.84 ![X0]: (v1_xboole_0(u1_struct_0(X0))|k6_domain_1(u1_struct_0(X0),k5_lattices(X0))=k1_tarski(k5_lattices(X0))|v3_struct_0(X0)|~l1_lattices(X0))),
% 10.10/1.84 inference(resolution,[status(thm)],[f329,f143])).
% 10.10/1.84 fof(f464,definition,(
% 10.10/1.84 sQ18_spl <=> (l3_lattices(sK4_skl))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f466,plain,(
% 10.10/1.84 ~l3_lattices(sK4_skl)|sQ18_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f464])).
% 10.10/1.84 fof(f696,definition,(
% 10.10/1.84 sQ66_spl <=> (v1_relat_1(sK17_skl))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f698,plain,(
% 10.10/1.84 ~v1_relat_1(sK17_skl)|sQ66_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f696])).
% 10.10/1.84 fof(f765,plain,(
% 10.10/1.84 l1_struct_0(sK1_skl)),
% 10.10/1.84 inference(resolution,[status(thm)],[f149,f177])).
% 10.10/1.84 fof(f773,plain,(
% 10.10/1.84 l1_lattices(sK27_skl)),
% 10.10/1.84 inference(resolution,[status(thm)],[f153,f318])).
% 10.10/1.84 fof(f774,plain,(
% 10.10/1.84 l1_lattices(sK26_skl)),
% 10.10/1.84 inference(resolution,[status(thm)],[f153,f314])).
% 10.10/1.84 fof(f775,plain,(
% 10.10/1.84 l1_lattices(sK23_skl)),
% 10.10/1.84 inference(resolution,[status(thm)],[f153,f304])).
% 10.10/1.84 fof(f776,plain,(
% 10.10/1.84 l1_lattices(sK12_skl)),
% 10.10/1.84 inference(resolution,[status(thm)],[f153,f258])).
% 10.10/1.84 fof(f777,plain,(
% 10.10/1.84 l1_lattices(sK4_skl)),
% 10.10/1.84 inference(resolution,[status(thm)],[f153,f183])).
% 10.10/1.84 fof(f778,plain,(
% 10.10/1.84 l1_lattices(sK0_skl)),
% 10.10/1.84 inference(resolution,[status(thm)],[f153,f98])).
% 10.10/1.84 fof(f788,plain,(
% 10.10/1.84 l1_struct_0(sK26_skl)),
% 10.10/1.84 inference(resolution,[status(thm)],[f774,f149])).
% 10.10/1.84 fof(f797,plain,(
% 10.10/1.84 l1_struct_0(sK23_skl)),
% 10.10/1.84 inference(resolution,[status(thm)],[f775,f149])).
% 10.10/1.84 fof(f806,plain,(
% 10.10/1.84 l1_struct_0(sK12_skl)),
% 10.10/1.84 inference(resolution,[status(thm)],[f776,f149])).
% 10.10/1.84 fof(f815,plain,(
% 10.10/1.84 l1_struct_0(sK4_skl)),
% 10.10/1.84 inference(resolution,[status(thm)],[f777,f149])).
% 10.10/1.84 fof(f824,plain,(
% 10.10/1.84 l1_struct_0(sK0_skl)),
% 10.10/1.84 inference(resolution,[status(thm)],[f778,f149])).
% 10.10/1.84 fof(f825,plain,(
% 10.10/1.84 v1_xboole_0(u1_struct_0(sK0_skl))|k6_domain_1(u1_struct_0(sK0_skl),k5_lattices(sK0_skl))=k1_tarski(k5_lattices(sK0_skl))|v3_struct_0(sK0_skl)),
% 10.10/1.84 inference(resolution,[status(thm)],[f778,f413])).
% 10.10/1.84 fof(f826,definition,(
% 10.10/1.84 sQ85_spl <=> (v1_xboole_0(u1_struct_0(sK0_skl)))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f827,plain,(
% 10.10/1.84 v1_xboole_0(u1_struct_0(sK0_skl))|~sQ85_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f826])).
% 10.10/1.84 fof(f829,definition,(
% 10.10/1.84 sQ86_spl <=> (k6_domain_1(u1_struct_0(sK0_skl),k5_lattices(sK0_skl))=k1_tarski(k5_lattices(sK0_skl)))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f830,plain,(
% 10.10/1.84 k6_domain_1(u1_struct_0(sK0_skl),k5_lattices(sK0_skl))=k1_tarski(k5_lattices(sK0_skl))|~sQ86_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f829])).
% 10.10/1.84 fof(f832,plain,(
% 10.10/1.84 sQ85_spl|sQ86_spl|sQ0_spl),
% 10.10/1.84 inference(split_clause,[status(thm)],[f825,f826,f829,f378])).
% 10.10/1.84 fof(f921,plain,(
% 10.10/1.84 l2_lattices(sK27_skl)),
% 10.10/1.84 inference(resolution,[status(thm)],[f154,f318])).
% 10.10/1.84 fof(f922,plain,(
% 10.10/1.84 l2_lattices(sK26_skl)),
% 10.10/1.84 inference(resolution,[status(thm)],[f154,f314])).
% 10.10/1.84 fof(f924,plain,(
% 10.10/1.84 l2_lattices(sK12_skl)),
% 10.10/1.84 inference(resolution,[status(thm)],[f154,f258])).
% 10.10/1.84 fof(f926,plain,(
% 10.10/1.84 l2_lattices(sK0_skl)),
% 10.10/1.84 inference(resolution,[status(thm)],[f154,f98])).
% 10.10/1.84 fof(f930,plain,(
% 10.10/1.84 sK18_skl=k1_xboole_0),
% 10.10/1.84 inference(resolution,[status(thm)],[f367,f289])).
% 10.10/1.84 fof(f931,plain,(
% 10.10/1.84 sK17_skl=k1_xboole_0),
% 10.10/1.84 inference(resolution,[status(thm)],[f367,f286])).
% 10.10/1.84 fof(f933,plain,(
% 10.10/1.84 ![X0]: (~v1_xboole_0(X0)|X0=sK18_skl)),
% 10.10/1.84 inference(backward_demodulation,[status(thm)],[f930,f367])).
% 10.10/1.84 fof(f934,plain,(
% 10.10/1.84 sK18_skl=sK17_skl),
% 10.10/1.84 inference(backward_demodulation,[status(thm)],[f931,f930])).
% 10.10/1.84 fof(f940,plain,(
% 10.10/1.84 v1_relat_1(sK17_skl)),
% 10.10/1.84 inference(backward_demodulation,[status(thm)],[f934,f288])).
% 10.10/1.84 fof(f942,plain,(
% 10.10/1.84 ![X0]: (~l3_lattices(X0)|l2_lattices(k1_lattice2(X0)))),
% 10.10/1.84 inference(resolution,[status(thm)],[f141,f154])).
% 10.10/1.84 fof(f952,plain,(
% 10.10/1.84 v3_struct_0(k1_lattice2(sK0_skl))|~l2_lattices(k1_lattice2(sK0_skl))|m1_subset_1(k5_lattices(sK0_skl),u1_struct_0(k1_lattice2(sK0_skl)))|~sQ5_spl),
% 10.10/1.84 inference(paramodulation,[status(thm)],[f396,f147])).
% 10.10/1.84 fof(f993,definition,(
% 10.10/1.84 sQ115_spl <=> (v3_struct_0(k1_lattice2(sK0_skl)))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f994,plain,(
% 10.10/1.84 v3_struct_0(k1_lattice2(sK0_skl))|~sQ115_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f993])).
% 10.10/1.84 fof(f996,definition,(
% 10.10/1.84 sQ116_spl <=> (l2_lattices(k1_lattice2(sK0_skl)))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f997,plain,(
% 10.10/1.84 l2_lattices(k1_lattice2(sK0_skl))|~sQ116_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f996])).
% 10.10/1.84 fof(f998,plain,(
% 10.10/1.84 ~l2_lattices(k1_lattice2(sK0_skl))|sQ116_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f996])).
% 10.10/1.84 fof(f999,definition,(
% 10.10/1.84 sQ117_spl <=> (m1_subset_1(k5_lattices(sK0_skl),u1_struct_0(k1_lattice2(sK0_skl))))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f1000,plain,(
% 10.10/1.84 m1_subset_1(k5_lattices(sK0_skl),u1_struct_0(k1_lattice2(sK0_skl)))|~sQ117_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f999])).
% 10.10/1.84 fof(f1002,plain,(
% 10.10/1.84 sQ115_spl|~sQ116_spl|sQ117_spl|~sQ5_spl),
% 10.10/1.84 inference(split_clause,[status(thm)],[f952,f993,f996,f999,f395])).
% 10.10/1.84 fof(f1004,plain,(
% 10.10/1.84 v1_xboole_0(u1_struct_0(k1_lattice2(sK0_skl)))|k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),k5_lattices(sK0_skl))=k1_tarski(k5_lattices(sK0_skl))|~sQ117_spl),
% 10.10/1.84 inference(resolution,[status(thm)],[f1000,f329])).
% 10.10/1.84 fof(f1011,definition,(
% 10.10/1.84 sQ120_spl <=> (v1_xboole_0(u1_struct_0(k1_lattice2(sK0_skl))))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f1012,plain,(
% 10.10/1.84 v1_xboole_0(u1_struct_0(k1_lattice2(sK0_skl)))|~sQ120_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f1011])).
% 10.10/1.84 fof(f1015,definition,(
% 10.10/1.84 sQ121_spl <=> (k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),k5_lattices(sK0_skl))=k1_tarski(k5_lattices(sK0_skl)))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f1016,plain,(
% 10.10/1.84 k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),k5_lattices(sK0_skl))=k1_tarski(k5_lattices(sK0_skl))|~sQ121_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f1015])).
% 10.10/1.84 fof(f1018,plain,(
% 10.10/1.84 sQ120_spl|sQ121_spl|~sQ117_spl),
% 10.10/1.84 inference(split_clause,[status(thm)],[f1004,f1011,f1015,f999])).
% 10.10/1.84 fof(f1030,plain,(
% 10.10/1.84 ~m2_filter_2(k1_tarski(k5_lattices(sK0_skl)),sK0_skl)|~sQ86_spl),
% 10.10/1.84 inference(backward_demodulation,[status(thm)],[f830,f100])).
% 10.10/1.84 fof(f1048,plain,(
% 10.10/1.84 ![X0]: (~v1_xboole_0(X0)|X0=sK17_skl)),
% 10.10/1.84 inference(forward_demodulation,[status(thm)],[f934,f933])).
% 10.10/1.84 fof(f1053,plain,(
% 10.10/1.84 ~l3_lattices(sK0_skl)|sQ116_spl),
% 10.10/1.84 inference(resolution,[status(thm)],[f942,f998])).
% 10.10/1.84 fof(f1054,plain,(
% 10.10/1.84 ~sQ4_spl|sQ116_spl),
% 10.10/1.84 inference(split_clause,[status(thm)],[f1053,f392,f996])).
% 10.10/1.84 fof(f1056,plain,(
% 10.10/1.84 ![X0,X1]: (r1_tarski(k6_domain_1(X0,X1),X0)|v1_xboole_0(X0)|~m1_subset_1(X1,X0))),
% 10.10/1.84 inference(resolution,[status(thm)],[f354,f145])).
% 10.10/1.84 fof(f1057,plain,(
% 10.10/1.84 v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|~sQ115_spl),
% 10.10/1.84 inference(resolution,[status(thm)],[f203,f994])).
% 10.10/1.84 fof(f1060,plain,(
% 10.10/1.84 sQ0_spl|~sQ4_spl|~sQ115_spl),
% 10.10/1.84 inference(split_clause,[status(thm)],[f1057,f378,f392,f993])).
% 10.10/1.84 fof(f1072,plain,(
% 10.10/1.84 ![X0]: (v1_xboole_0(X0)|r2_hidden(sK8_skl(X0),X0))),
% 10.10/1.84 inference(resolution,[status(thm)],[f351,f193])).
% 10.10/1.84 fof(f1073,plain,(
% 10.10/1.84 ![X0,X1]: (v1_xboole_0(k1_zfmisc_1(X0))|r2_hidden(k6_domain_1(X0,X1),k1_zfmisc_1(X0))|v1_xboole_0(X0)|~m1_subset_1(X1,X0))),
% 10.10/1.84 inference(resolution,[status(thm)],[f351,f145])).
% 10.10/1.84 fof(f1078,plain,(
% 10.10/1.84 ![X0,X1]: (~m1_subset_1(X0,k1_zfmisc_1(X1))|~v1_xboole_0(X1)|v1_xboole_0(X0))),
% 10.10/1.84 inference(resolution,[status(thm)],[f361,f1072])).
% 10.10/1.84 fof(f1086,plain,(
% 10.10/1.84 l1_struct_0(sK3_skl)),
% 10.10/1.84 inference(resolution,[status(thm)],[f151,f181])).
% 10.10/1.84 fof(f1087,plain,(
% 10.10/1.84 v3_struct_0(sK0_skl)|~l1_struct_0(sK0_skl)|~sQ85_spl),
% 10.10/1.84 inference(resolution,[status(thm)],[f827,f206])).
% 10.10/1.84 fof(f1093,definition,(
% 10.10/1.84 sQ127_spl <=> (l1_struct_0(sK0_skl))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f1095,plain,(
% 10.10/1.84 ~l1_struct_0(sK0_skl)|sQ127_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f1093])).
% 10.10/1.84 fof(f1096,plain,(
% 10.10/1.84 sQ0_spl|~sQ127_spl|~sQ85_spl),
% 10.10/1.84 inference(split_clause,[status(thm)],[f1087,f378,f1093,f826])).
% 10.10/1.84 fof(f1098,plain,(
% 10.10/1.84 $false|sQ127_spl),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f1095,f824])).
% 10.10/1.84 fof(f1099,plain,(
% 10.10/1.84 sQ127_spl),
% 10.10/1.84 inference(contradiction_clause,[status(thm)],[f1098])).
% 10.10/1.84 fof(f1100,plain,(
% 10.10/1.84 l1_struct_0(k1_lattice2(sK0_skl))|~sQ116_spl),
% 10.10/1.84 inference(resolution,[status(thm)],[f997,f151])).
% 10.10/1.84 fof(f1103,definition,(
% 10.10/1.84 sQ128_spl <=> (l3_lattices(k1_lattice2(sK0_skl)))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f1105,plain,(
% 10.10/1.84 ~l3_lattices(k1_lattice2(sK0_skl))|sQ128_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f1103])).
% 10.10/1.84 fof(f1106,definition,(
% 10.10/1.84 sQ129_spl <=> (v10_lattices(k1_lattice2(sK0_skl)))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f1126,definition,(
% 10.10/1.84 sQ133_spl <=> (l1_struct_0(sK26_skl))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f1128,plain,(
% 10.10/1.84 ~l1_struct_0(sK26_skl)|sQ133_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f1126])).
% 10.10/1.84 fof(f1131,plain,(
% 10.10/1.84 $false|sQ133_spl),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f1128,f788])).
% 10.10/1.84 fof(f1132,plain,(
% 10.10/1.84 sQ133_spl),
% 10.10/1.84 inference(contradiction_clause,[status(thm)],[f1131])).
% 10.10/1.84 fof(f1139,definition,(
% 10.10/1.84 sQ134_spl <=> (v3_struct_0(sK24_skl))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f1140,plain,(
% 10.10/1.84 v3_struct_0(sK24_skl)|~sQ134_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f1139])).
% 10.10/1.84 fof(f1143,plain,(
% 10.10/1.84 $false|~sQ134_spl),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f1140,f308])).
% 10.10/1.84 fof(f1144,plain,(
% 10.10/1.84 ~sQ134_spl),
% 10.10/1.84 inference(contradiction_clause,[status(thm)],[f1143])).
% 10.10/1.84 fof(f1159,plain,(
% 10.10/1.84 ![X0]: (~v1_xboole_0(X0)|v1_xboole_0(sK8_skl(k1_zfmisc_1(X0))))),
% 10.10/1.84 inference(resolution,[status(thm)],[f1078,f193])).
% 10.10/1.84 fof(f1163,plain,(
% 10.10/1.84 v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|v10_lattices(k1_lattice2(sK0_skl))),
% 10.10/1.84 inference(resolution,[status(thm)],[f252,f97])).
% 10.10/1.84 fof(f1172,plain,(
% 10.10/1.84 sQ0_spl|~sQ4_spl|sQ129_spl),
% 10.10/1.84 inference(split_clause,[status(thm)],[f1163,f378,f392,f1106])).
% 10.10/1.84 fof(f1202,definition,(
% 10.10/1.84 sQ140_spl <=> (l2_lattices(sK0_skl))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f1204,plain,(
% 10.10/1.84 ~l2_lattices(sK0_skl)|sQ140_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f1202])).
% 10.10/1.84 fof(f1209,plain,(
% 10.10/1.84 $false|sQ140_spl),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f1204,f926])).
% 10.10/1.84 fof(f1210,plain,(
% 10.10/1.84 sQ140_spl),
% 10.10/1.84 inference(contradiction_clause,[status(thm)],[f1209])).
% 10.10/1.84 fof(f1211,plain,(
% 10.10/1.84 ~l3_lattices(sK0_skl)|sQ128_spl),
% 10.10/1.84 inference(resolution,[status(thm)],[f1105,f141])).
% 10.10/1.84 fof(f1212,plain,(
% 10.10/1.84 ~sQ4_spl|sQ128_spl),
% 10.10/1.84 inference(split_clause,[status(thm)],[f1211,f392,f1103])).
% 10.10/1.84 fof(f1232,definition,(
% 10.10/1.84 sQ145_spl <=> (l2_lattices(sK27_skl))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f1234,plain,(
% 10.10/1.84 ~l2_lattices(sK27_skl)|sQ145_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f1232])).
% 10.10/1.84 fof(f1239,plain,(
% 10.10/1.84 $false|sQ145_spl),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f1234,f921])).
% 10.10/1.84 fof(f1240,plain,(
% 10.10/1.84 sQ145_spl),
% 10.10/1.84 inference(contradiction_clause,[status(thm)],[f1239])).
% 10.10/1.84 fof(f1243,definition,(
% 10.10/1.84 sQ147_spl <=> (l2_lattices(sK26_skl))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f1245,plain,(
% 10.10/1.84 ~l2_lattices(sK26_skl)|sQ147_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f1243])).
% 10.10/1.84 fof(f1250,plain,(
% 10.10/1.84 $false|sQ147_spl),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f1245,f922])).
% 10.10/1.84 fof(f1251,plain,(
% 10.10/1.84 sQ147_spl),
% 10.10/1.84 inference(contradiction_clause,[status(thm)],[f1250])).
% 10.10/1.84 fof(f1301,plain,(
% 10.10/1.84 $false|sQ66_spl),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f698,f940])).
% 10.10/1.84 fof(f1302,plain,(
% 10.10/1.84 sQ66_spl),
% 10.10/1.84 inference(contradiction_clause,[status(thm)],[f1301])).
% 10.10/1.84 fof(f1505,plain,(
% 10.10/1.84 ![X0,X1]: (r2_hidden(k6_domain_1(X0,X1),k1_zfmisc_1(X0))|v1_xboole_0(X0)|~m1_subset_1(X1,X0))),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f1073,f207])).
% 10.10/1.84 fof(f1517,plain,(
% 10.10/1.84 ![X0]: (sK20_skl(X0)=sK17_skl)),
% 10.10/1.84 inference(resolution,[status(thm)],[f296,f1048])).
% 10.10/1.84 fof(f1587,plain,(
% 10.10/1.84 v3_struct_0(k1_lattice2(sK0_skl))|~l1_struct_0(k1_lattice2(sK0_skl))|~sQ120_spl),
% 10.10/1.84 inference(resolution,[status(thm)],[f1012,f206])).
% 10.10/1.84 fof(f1593,definition,(
% 10.10/1.84 sQ197_spl <=> (l1_struct_0(k1_lattice2(sK0_skl)))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f1595,plain,(
% 10.10/1.84 ~l1_struct_0(k1_lattice2(sK0_skl))|sQ197_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f1593])).
% 10.10/1.84 fof(f1596,plain,(
% 10.10/1.84 sQ115_spl|~sQ197_spl|~sQ120_spl),
% 10.10/1.84 inference(split_clause,[status(thm)],[f1587,f993,f1593,f1011])).
% 10.10/1.84 fof(f1598,plain,(
% 10.10/1.84 $false|~sQ116_spl|sQ197_spl),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f1595,f1100])).
% 10.10/1.84 fof(f1599,plain,(
% 10.10/1.84 ~sQ116_spl|sQ197_spl),
% 10.10/1.84 inference(contradiction_clause,[status(thm)],[f1598])).
% 10.10/1.84 fof(f1684,plain,(
% 10.10/1.84 ![X0]: (m1_subset_1(sK17_skl,k1_zfmisc_1(X0)))),
% 10.10/1.84 inference(forward_demodulation,[status(thm)],[f1517,f295])).
% 10.10/1.84 fof(f1691,definition,(
% 10.10/1.84 ![X0]: (sQ209_spl <=> (~v1_xboole_0(X0)))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ209_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f1692,plain,(
% 10.10/1.84 ![X0]: (~v1_xboole_0(X0)|~sQ209_spl)),
% 10.10/1.84 inference(component_clause,[status(thm)],[f1691])).
% 10.10/1.84 fof(f1714,plain,(
% 10.10/1.84 $false|~sQ209_spl),
% 10.10/1.84 inference(backward_subsumption_resolution,[status(thm)],[f286,f1692])).
% 10.10/1.84 fof(f1716,plain,(
% 10.10/1.84 ~sQ209_spl),
% 10.10/1.84 inference(contradiction_clause,[status(thm)],[f1714])).
% 10.10/1.84 fof(f1838,plain,(
% 10.10/1.84 ![X0,X1]: (~r2_hidden(X0,X1)|~m1_subset_1(X1,k1_zfmisc_1(sK17_skl)))),
% 10.10/1.84 inference(resolution,[status(thm)],[f361,f286])).
% 10.10/1.84 fof(f1853,definition,(
% 10.10/1.84 sQ231_spl <=> (v1_xboole_0(k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0_skl)))))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ231_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f1854,plain,(
% 10.10/1.84 v1_xboole_0(k1_zfmisc_1(u1_struct_0(k1_lattice2(sK0_skl))))|~sQ231_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f1853])).
% 10.10/1.84 fof(f2163,definition,(
% 10.10/1.84 sQ273_spl <=> (v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ273_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f2164,plain,(
% 10.10/1.84 v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ273_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f2163])).
% 10.10/1.84 fof(f2171,plain,(
% 10.10/1.84 $false|~sQ273_spl),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f2164,f207])).
% 10.10/1.84 fof(f2172,plain,(
% 10.10/1.84 ~sQ273_spl),
% 10.10/1.84 inference(contradiction_clause,[status(thm)],[f2171])).
% 10.10/1.84 fof(f2237,definition,(
% 10.10/1.84 sQ280_spl <=> (l1_lattices(sK0_skl))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ280_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f2239,plain,(
% 10.10/1.84 ~l1_lattices(sK0_skl)|sQ280_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f2237])).
% 10.10/1.84 fof(f2241,plain,(
% 10.10/1.84 $false|sQ280_spl),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f2239,f778])).
% 10.10/1.84 fof(f2242,plain,(
% 10.10/1.84 sQ280_spl),
% 10.10/1.84 inference(contradiction_clause,[status(thm)],[f2241])).
% 10.10/1.84 fof(f2302,plain,(
% 10.10/1.84 $false|~sQ231_spl),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f1854,f207])).
% 10.10/1.84 fof(f2303,plain,(
% 10.10/1.84 ~sQ231_spl),
% 10.10/1.84 inference(contradiction_clause,[status(thm)],[f2302])).
% 10.10/1.84 fof(f2331,definition,(
% 10.10/1.84 sQ297_spl <=> (l1_lattices(sK27_skl))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ297_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f2333,plain,(
% 10.10/1.84 ~l1_lattices(sK27_skl)|sQ297_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f2331])).
% 10.10/1.84 fof(f2335,plain,(
% 10.10/1.84 $false|sQ297_spl),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f2333,f773])).
% 10.10/1.84 fof(f2336,plain,(
% 10.10/1.84 sQ297_spl),
% 10.10/1.84 inference(contradiction_clause,[status(thm)],[f2335])).
% 10.10/1.84 fof(f2338,definition,(
% 10.10/1.84 sQ298_spl <=> (l1_lattices(sK26_skl))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ298_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f2340,plain,(
% 10.10/1.84 ~l1_lattices(sK26_skl)|sQ298_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f2338])).
% 10.10/1.84 fof(f2342,plain,(
% 10.10/1.84 $false|sQ298_spl),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f2340,f774])).
% 10.10/1.84 fof(f2343,plain,(
% 10.10/1.84 sQ298_spl),
% 10.10/1.84 inference(contradiction_clause,[status(thm)],[f2342])).
% 10.10/1.84 fof(f2612,definition,(
% 10.10/1.84 sQ345_spl <=> (l1_struct_0(sK3_skl))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ345_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f2614,plain,(
% 10.10/1.84 ~l1_struct_0(sK3_skl)|sQ345_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f2612])).
% 10.10/1.84 fof(f2616,plain,(
% 10.10/1.84 $false|sQ345_spl),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f2614,f1086])).
% 10.10/1.84 fof(f2617,plain,(
% 10.10/1.84 sQ345_spl),
% 10.10/1.84 inference(contradiction_clause,[status(thm)],[f2616])).
% 10.10/1.84 fof(f2628,definition,(
% 10.10/1.84 sQ346_spl <=> (l1_struct_0(sK12_skl))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ346_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f2630,plain,(
% 10.10/1.84 ~l1_struct_0(sK12_skl)|sQ346_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f2628])).
% 10.10/1.84 fof(f2632,plain,(
% 10.10/1.84 $false|sQ346_spl),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f2630,f806])).
% 10.10/1.84 fof(f2633,plain,(
% 10.10/1.84 sQ346_spl),
% 10.10/1.84 inference(contradiction_clause,[status(thm)],[f2632])).
% 10.10/1.84 fof(f2643,plain,(
% 10.10/1.84 ![X0]: (m1_subset_1(X0,k1_zfmisc_1(X0)))),
% 10.10/1.84 inference(resolution,[status(thm)],[f355,f340])).
% 10.10/1.84 fof(f2652,plain,(
% 10.10/1.84 ![X0]: (v1_xboole_0(k1_zfmisc_1(X0))|k6_domain_1(k1_zfmisc_1(X0),X0)=k1_tarski(X0))),
% 10.10/1.84 inference(resolution,[status(thm)],[f2643,f329])).
% 10.10/1.84 fof(f2656,plain,(
% 10.10/1.84 ![X0]: (k6_domain_1(k1_zfmisc_1(X0),X0)=k1_tarski(X0))),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f2652,f207])).
% 10.10/1.84 fof(f2669,definition,(
% 10.10/1.84 sQ349_spl <=> (m1_subset_1(sK8_skl(u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ349_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f2671,plain,(
% 10.10/1.84 ~m1_subset_1(sK8_skl(u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|sQ349_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f2669])).
% 10.10/1.84 fof(f2677,plain,(
% 10.10/1.84 $false|sQ349_spl),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f2671,f193])).
% 10.10/1.84 fof(f2678,plain,(
% 10.10/1.84 sQ349_spl),
% 10.10/1.84 inference(contradiction_clause,[status(thm)],[f2677])).
% 10.10/1.84 fof(f2682,plain,(
% 10.10/1.84 ![X0]: (v1_xboole_0(k1_zfmisc_1(X0))|~m1_subset_1(X0,k1_zfmisc_1(X0))|m1_subset_1(k1_tarski(X0),k1_zfmisc_1(k1_zfmisc_1(X0))))),
% 10.10/1.84 inference(paramodulation,[status(thm)],[f2656,f145])).
% 10.10/1.84 fof(f2684,plain,(
% 10.10/1.84 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(X0))|m1_subset_1(k1_tarski(X0),k1_zfmisc_1(k1_zfmisc_1(X0))))),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f2682,f207])).
% 10.10/1.84 fof(f2685,plain,(
% 10.10/1.84 ![X0]: (m1_subset_1(k1_tarski(X0),k1_zfmisc_1(k1_zfmisc_1(X0))))),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f2684,f2643])).
% 10.10/1.84 fof(f2690,plain,(
% 10.10/1.84 ![X0]: (v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(X0)))|k6_domain_1(k1_zfmisc_1(k1_zfmisc_1(X0)),k1_tarski(X0))=k1_tarski(k1_tarski(X0)))),
% 10.10/1.84 inference(resolution,[status(thm)],[f2685,f329])).
% 10.10/1.84 fof(f2694,plain,(
% 10.10/1.84 ![X0]: (k6_domain_1(k1_zfmisc_1(k1_zfmisc_1(X0)),k1_tarski(X0))=k1_tarski(k1_tarski(X0)))),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f2690,f207])).
% 10.10/1.84 fof(f2695,plain,(
% 10.10/1.84 ![X0]: (r1_tarski(k1_tarski(k1_tarski(X0)),k1_zfmisc_1(k1_zfmisc_1(X0)))|v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(X0)))|~m1_subset_1(k1_tarski(X0),k1_zfmisc_1(k1_zfmisc_1(X0))))),
% 10.10/1.84 inference(paramodulation,[status(thm)],[f2694,f1056])).
% 10.10/1.84 fof(f2697,plain,(
% 10.10/1.84 ![X0]: (r1_tarski(k1_tarski(k1_tarski(X0)),k1_zfmisc_1(k1_zfmisc_1(X0)))|~m1_subset_1(k1_tarski(X0),k1_zfmisc_1(k1_zfmisc_1(X0))))),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f2695,f207])).
% 10.10/1.84 fof(f2699,plain,(
% 10.10/1.84 ![X0]: (r1_tarski(k1_tarski(k1_tarski(X0)),k1_zfmisc_1(k1_zfmisc_1(X0))))),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f2697,f2685])).
% 10.10/1.84 fof(f2700,plain,(
% 10.10/1.84 ![X0]: (m1_subset_1(k1_tarski(k1_tarski(X0)),k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(X0)))))),
% 10.10/1.84 inference(resolution,[status(thm)],[f2699,f355])).
% 10.10/1.84 fof(f2702,plain,(
% 10.10/1.84 ![X0]: (r2_hidden(k6_domain_1(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(X0))),k1_tarski(k1_tarski(X0))),k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(X0)))))|v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(X0)))))),
% 10.10/1.84 inference(resolution,[status(thm)],[f2700,f1505])).
% 10.10/1.84 fof(f2705,plain,(
% 10.10/1.84 ![X0]: (v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(X0))))|k6_domain_1(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(X0))),k1_tarski(k1_tarski(X0)))=k1_tarski(k1_tarski(k1_tarski(X0))))),
% 10.10/1.84 inference(resolution,[status(thm)],[f2700,f329])).
% 10.10/1.84 fof(f2706,plain,(
% 10.10/1.84 ![X0]: (r2_hidden(k6_domain_1(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(X0))),k1_tarski(k1_tarski(X0))),k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(X0))))))),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f2702,f207])).
% 10.10/1.84 fof(f2709,plain,(
% 10.10/1.84 ![X0]: (k6_domain_1(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(X0))),k1_tarski(k1_tarski(X0)))=k1_tarski(k1_tarski(k1_tarski(X0))))),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f2705,f207])).
% 10.10/1.84 fof(f2747,plain,(
% 10.10/1.84 ![X0]: (r2_hidden(k1_tarski(k1_tarski(k1_tarski(X0))),k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(X0))))))),
% 10.10/1.84 inference(forward_demodulation,[status(thm)],[f2709,f2706])).
% 10.10/1.84 fof(f2750,plain,(
% 10.10/1.84 ![X0]: (m1_subset_1(k1_tarski(k1_tarski(k1_tarski(X0))),k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(X0))))))),
% 10.10/1.84 inference(resolution,[status(thm)],[f2747,f344])).
% 10.10/1.84 fof(f2753,plain,(
% 10.10/1.84 ![X0]: (r2_hidden(k6_domain_1(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(X0)))),k1_tarski(k1_tarski(k1_tarski(X0)))),k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(X0))))))|v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(X0))))))),
% 10.10/1.84 inference(resolution,[status(thm)],[f2750,f1505])).
% 10.10/1.84 fof(f2756,plain,(
% 10.10/1.84 ![X0]: (v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(X0)))))|k6_domain_1(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(X0)))),k1_tarski(k1_tarski(k1_tarski(X0))))=k1_tarski(k1_tarski(k1_tarski(k1_tarski(X0)))))),
% 10.10/1.84 inference(resolution,[status(thm)],[f2750,f329])).
% 10.10/1.84 fof(f2757,plain,(
% 10.10/1.84 ![X0]: (r2_hidden(k6_domain_1(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(X0)))),k1_tarski(k1_tarski(k1_tarski(X0)))),k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(X0)))))))),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f2753,f207])).
% 10.10/1.84 fof(f2759,plain,(
% 10.10/1.84 ![X0]: (k6_domain_1(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(X0)))),k1_tarski(k1_tarski(k1_tarski(X0))))=k1_tarski(k1_tarski(k1_tarski(k1_tarski(X0)))))),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f2756,f207])).
% 10.10/1.84 fof(f2835,plain,(
% 10.10/1.84 v1_xboole_0(sK8_skl(k1_zfmisc_1(sK17_skl)))),
% 10.10/1.84 inference(resolution,[status(thm)],[f1159,f286])).
% 10.10/1.84 fof(f2847,plain,(
% 10.10/1.84 sK8_skl(k1_zfmisc_1(sK17_skl))=sK17_skl),
% 10.10/1.84 inference(resolution,[status(thm)],[f2835,f1048])).
% 10.10/1.84 fof(f2848,definition,(
% 10.10/1.84 sQ361_spl <=> (v1_relat_1(sK8_skl(k1_zfmisc_1(sK17_skl))))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ361_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f2850,plain,(
% 10.10/1.84 ~v1_relat_1(sK8_skl(k1_zfmisc_1(sK17_skl)))|sQ361_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f2848])).
% 10.10/1.84 fof(f2865,definition,(
% 10.10/1.84 sQ363_spl <=> (v1_xboole_0(k1_zfmisc_1(sK17_skl)))),
% 10.10/1.84 introduced(definition,[new_symbols(definition,[sQ363_spl])],[split_symbol_definition])).
% 10.10/1.84 fof(f2866,plain,(
% 10.10/1.84 v1_xboole_0(k1_zfmisc_1(sK17_skl))|~sQ363_spl),
% 10.10/1.84 inference(component_clause,[status(thm)],[f2865])).
% 10.10/1.84 fof(f2876,plain,(
% 10.10/1.84 $false|~sQ363_spl),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f2866,f207])).
% 10.10/1.84 fof(f2877,plain,(
% 10.10/1.84 ~sQ363_spl),
% 10.10/1.84 inference(contradiction_clause,[status(thm)],[f2876])).
% 10.10/1.84 fof(f2878,plain,(
% 10.10/1.84 ~v1_relat_1(sK17_skl)|sQ361_spl),
% 10.10/1.84 inference(forward_demodulation,[status(thm)],[f2847,f2850])).
% 10.10/1.84 fof(f2879,plain,(
% 10.10/1.84 $false|sQ361_spl),
% 10.10/1.84 inference(forward_subsumption_resolution,[status(thm)],[f2878,f940])).
% 10.10/1.84 fof(f2880,plain,(
% 10.10/1.84 sQ361_spl),
% 10.10/1.84 inference(contradiction_clause,[status(thm)],[f2879])).
% 9.04/1.86 fof(f3013,definition,(
% 9.04/1.86 sQ379_spl <=> (m1_subset_1(sK8_skl(sK6_skl(sK0_skl)),sK6_skl(sK0_skl)))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ379_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f3015,plain,(
% 9.04/1.86 ~m1_subset_1(sK8_skl(sK6_skl(sK0_skl)),sK6_skl(sK0_skl))|sQ379_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f3013])).
% 9.04/1.86 fof(f3021,plain,(
% 9.04/1.86 $false|sQ379_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f3015,f193])).
% 9.04/1.86 fof(f3022,plain,(
% 9.04/1.86 sQ379_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f3021])).
% 9.04/1.86 fof(f3134,plain,(
% 9.04/1.86 ![X0]: (r2_hidden(k1_tarski(k1_tarski(k1_tarski(k1_tarski(X0)))),k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(X0)))))))),
% 9.04/1.86 inference(forward_demodulation,[status(thm)],[f2759,f2757])).
% 9.04/1.86 fof(f3187,plain,(
% 9.04/1.86 ![X0]: (~r2_hidden(X0,sK17_skl))),
% 9.04/1.86 inference(resolution,[status(thm)],[f1838,f1684])).
% 9.04/1.86 fof(f3387,definition,(
% 9.04/1.86 sQ421_spl <=> (l1_lattices(sK23_skl))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ421_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f3389,plain,(
% 9.04/1.86 ~l1_lattices(sK23_skl)|sQ421_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f3387])).
% 9.04/1.86 fof(f3391,plain,(
% 9.04/1.86 $false|sQ421_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f3389,f775])).
% 9.04/1.86 fof(f3392,plain,(
% 9.04/1.86 sQ421_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f3391])).
% 9.04/1.86 fof(f3448,plain,(
% 9.04/1.86 ![X0]: (v3_struct_0(k1_lattice2(X0))|~v10_lattices(k1_lattice2(X0))|~l3_lattices(k1_lattice2(X0))|m1_filter_0(k6_domain_1(u1_struct_0(k1_lattice2(X0)),k6_lattices(k1_lattice2(X0))),k1_lattice2(X0))|v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~v13_lattices(X0))),
% 9.04/1.86 inference(resolution,[status(thm)],[f376,f364])).
% 9.04/1.86 fof(f3450,plain,(
% 9.04/1.86 ![X0]: (~v10_lattices(k1_lattice2(X0))|~l3_lattices(k1_lattice2(X0))|m1_filter_0(k6_domain_1(u1_struct_0(k1_lattice2(X0)),k6_lattices(k1_lattice2(X0))),k1_lattice2(X0))|v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~v13_lattices(X0))),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f3448,f203])).
% 9.04/1.86 fof(f3689,definition,(
% 9.04/1.86 sQ472_spl <=> (l1_struct_0(sK24_skl))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ472_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f3691,plain,(
% 9.04/1.86 ~l1_struct_0(sK24_skl)|sQ472_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f3689])).
% 9.04/1.86 fof(f3708,plain,(
% 9.04/1.86 $false|sQ472_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f3691,f307])).
% 9.04/1.86 fof(f3709,plain,(
% 9.04/1.86 sQ472_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f3708])).
% 9.04/1.86 fof(f3729,definition,(
% 9.04/1.86 sQ480_spl <=> (l1_lattices(sK12_skl))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ480_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f3731,plain,(
% 9.04/1.86 ~l1_lattices(sK12_skl)|sQ480_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f3729])).
% 9.04/1.86 fof(f3733,plain,(
% 9.04/1.86 $false|sQ480_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f3731,f776])).
% 9.04/1.86 fof(f3734,plain,(
% 9.04/1.86 sQ480_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f3733])).
% 9.04/1.86 fof(f3803,definition,(
% 9.04/1.86 sQ489_spl <=> (v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK12_skl))))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ489_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f3804,plain,(
% 9.04/1.86 v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK12_skl)))|~sQ489_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f3803])).
% 9.04/1.86 fof(f3819,plain,(
% 9.04/1.86 $false|~sQ489_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f3804,f207])).
% 9.04/1.86 fof(f3820,plain,(
% 9.04/1.86 ~sQ489_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f3819])).
% 9.04/1.86 fof(f3861,definition,(
% 9.04/1.86 sQ499_spl <=> (v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK27_skl))))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ499_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f3862,plain,(
% 9.04/1.86 v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK27_skl)))|~sQ499_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f3861])).
% 9.04/1.86 fof(f3877,plain,(
% 9.04/1.86 $false|~sQ499_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f3862,f207])).
% 9.04/1.86 fof(f3878,plain,(
% 9.04/1.86 ~sQ499_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f3877])).
% 9.04/1.86 fof(f3998,definition,(
% 9.04/1.86 sQ527_spl <=> (l1_lattices(sK4_skl))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ527_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f4000,plain,(
% 9.04/1.86 ~l1_lattices(sK4_skl)|sQ527_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f3998])).
% 9.04/1.86 fof(f4002,plain,(
% 9.04/1.86 $false|sQ527_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f4000,f777])).
% 9.04/1.86 fof(f4003,plain,(
% 9.04/1.86 sQ527_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f4002])).
% 9.04/1.86 fof(f4459,definition,(
% 9.04/1.86 sQ574_spl <=> (k1_zfmisc_1(sK17_skl)=sK17_skl)),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ574_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f4460,plain,(
% 9.04/1.86 k1_zfmisc_1(sK17_skl)=sK17_skl|~sQ574_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f4459])).
% 9.04/1.86 fof(f4483,plain,(
% 9.04/1.86 $false|sQ18_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f466,f183])).
% 9.04/1.86 fof(f4484,plain,(
% 9.04/1.86 sQ18_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f4483])).
% 9.04/1.86 fof(f4572,plain,(
% 9.04/1.86 r2_hidden(k1_tarski(k1_tarski(k1_tarski(k1_tarski(sK17_skl)))),k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(sK17_skl)))))|~sQ574_spl),
% 9.04/1.86 inference(paramodulation,[status(thm)],[f4460,f3134])).
% 9.04/1.86 fof(f4619,definition,(
% 9.04/1.86 sQ580_spl <=> (r2_hidden(sK16_skl(sK17_skl),sK17_skl))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ580_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f4620,plain,(
% 9.04/1.86 r2_hidden(sK16_skl(sK17_skl),sK17_skl)|~sQ580_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f4619])).
% 9.04/1.86 fof(f4639,plain,(
% 9.04/1.86 r2_hidden(k1_tarski(k1_tarski(k1_tarski(k1_tarski(sK17_skl)))),k1_zfmisc_1(k1_zfmisc_1(k1_zfmisc_1(sK17_skl))))|~sQ574_spl),
% 9.04/1.86 inference(forward_demodulation,[status(thm)],[f4460,f4572])).
% 9.04/1.86 fof(f4640,plain,(
% 9.04/1.86 r2_hidden(k1_tarski(k1_tarski(k1_tarski(k1_tarski(sK17_skl)))),k1_zfmisc_1(k1_zfmisc_1(sK17_skl)))|~sQ574_spl),
% 9.04/1.86 inference(forward_demodulation,[status(thm)],[f4460,f4639])).
% 9.04/1.86 fof(f4641,plain,(
% 9.04/1.86 r2_hidden(k1_tarski(k1_tarski(k1_tarski(k1_tarski(sK17_skl)))),k1_zfmisc_1(sK17_skl))|~sQ574_spl),
% 9.04/1.86 inference(forward_demodulation,[status(thm)],[f4460,f4640])).
% 9.04/1.86 fof(f4642,plain,(
% 9.04/1.86 r2_hidden(k1_tarski(k1_tarski(k1_tarski(k1_tarski(sK17_skl)))),sK17_skl)|~sQ574_spl),
% 9.04/1.86 inference(forward_demodulation,[status(thm)],[f4460,f4641])).
% 9.04/1.86 fof(f4643,plain,(
% 9.04/1.86 $false|~sQ574_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f4642,f3187])).
% 9.04/1.86 fof(f4644,plain,(
% 9.04/1.86 ~sQ574_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f4643])).
% 9.04/1.86 fof(f4645,plain,(
% 9.04/1.86 $false|~sQ580_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f4620,f3187])).
% 9.04/1.86 fof(f4646,plain,(
% 9.04/1.86 ~sQ580_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f4645])).
% 9.04/1.86 fof(f4659,definition,(
% 9.04/1.86 sQ582_spl <=> (l1_struct_0(sK1_skl))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ582_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f4661,plain,(
% 9.04/1.86 ~l1_struct_0(sK1_skl)|sQ582_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f4659])).
% 9.04/1.86 fof(f4670,plain,(
% 9.04/1.86 $false|sQ582_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f4661,f765])).
% 9.04/1.86 fof(f4671,plain,(
% 9.04/1.86 sQ582_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f4670])).
% 9.04/1.86 fof(f4684,definition,(
% 9.04/1.86 sQ585_spl <=> (l1_struct_0(sK4_skl))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ585_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f4686,plain,(
% 9.04/1.86 ~l1_struct_0(sK4_skl)|sQ585_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f4684])).
% 9.04/1.86 fof(f4689,plain,(
% 9.04/1.86 $false|sQ585_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f4686,f815])).
% 9.04/1.86 fof(f4690,plain,(
% 9.04/1.86 sQ585_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f4689])).
% 9.04/1.86 fof(f4739,definition,(
% 9.04/1.86 sQ592_spl <=> (l1_struct_0(sK23_skl))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ592_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f4741,plain,(
% 9.04/1.86 ~l1_struct_0(sK23_skl)|sQ592_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f4739])).
% 9.04/1.86 fof(f4744,plain,(
% 9.04/1.86 $false|sQ592_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f4741,f797])).
% 9.04/1.86 fof(f4745,plain,(
% 9.04/1.86 sQ592_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f4744])).
% 9.04/1.86 fof(f5177,definition,(
% 9.04/1.86 sQ635_spl <=> (l2_lattices(sK12_skl))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ635_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f5179,plain,(
% 9.04/1.86 ~l2_lattices(sK12_skl)|sQ635_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f5177])).
% 9.04/1.86 fof(f5182,plain,(
% 9.04/1.86 $false|sQ635_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f5179,f924])).
% 9.04/1.86 fof(f5183,plain,(
% 9.04/1.86 sQ635_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f5182])).
% 9.04/1.86 fof(f5466,definition,(
% 9.04/1.86 sQ659_spl <=> (v1_xboole_0(k1_zfmisc_1(sK6_skl(sK0_skl))))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ659_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f5467,plain,(
% 9.04/1.86 v1_xboole_0(k1_zfmisc_1(sK6_skl(sK0_skl)))|~sQ659_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f5466])).
% 9.04/1.86 fof(f5477,plain,(
% 9.04/1.86 $false|~sQ659_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f5467,f207])).
% 9.04/1.86 fof(f5478,plain,(
% 9.04/1.86 ~sQ659_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f5477])).
% 9.04/1.86 fof(f5587,definition,(
% 9.04/1.86 sQ678_spl <=> (sK15_skl=sK17_skl)),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ678_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f5588,plain,(
% 9.04/1.86 sK15_skl=sK17_skl|~sQ678_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f5587])).
% 9.04/1.86 fof(f5595,definition,(
% 9.04/1.86 sQ680_spl <=> (v1_xboole_0(sK15_skl))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ680_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f5596,plain,(
% 9.04/1.86 v1_xboole_0(sK15_skl)|~sQ680_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f5595])).
% 9.04/1.86 fof(f5598,definition,(
% 9.04/1.86 sQ681_spl <=> (m1_subset_1(sK8_skl(sK15_skl),sK15_skl))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ681_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f5600,plain,(
% 9.04/1.86 ~m1_subset_1(sK8_skl(sK15_skl),sK15_skl)|sQ681_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f5598])).
% 9.04/1.86 fof(f5606,plain,(
% 9.04/1.86 $false|sQ681_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f5600,f193])).
% 9.04/1.86 fof(f5607,plain,(
% 9.04/1.86 sQ681_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f5606])).
% 9.04/1.86 fof(f5608,plain,(
% 9.04/1.86 $false|~sQ680_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f5596,f279])).
% 9.04/1.86 fof(f5609,plain,(
% 9.04/1.86 ~sQ680_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f5608])).
% 9.04/1.86 fof(f5617,definition,(
% 9.04/1.86 sQ684_spl <=> (sK19_skl=sK17_skl)),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ684_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f5618,plain,(
% 9.04/1.86 sK19_skl=sK17_skl|~sQ684_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f5617])).
% 9.04/1.86 fof(f5625,definition,(
% 9.04/1.86 sQ686_spl <=> (v1_xboole_0(sK19_skl))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ686_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f5626,plain,(
% 9.04/1.86 v1_xboole_0(sK19_skl)|~sQ686_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f5625])).
% 9.04/1.86 fof(f5628,definition,(
% 9.04/1.86 sQ687_spl <=> (m1_subset_1(sK8_skl(sK19_skl),sK19_skl))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ687_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f5630,plain,(
% 9.04/1.86 ~m1_subset_1(sK8_skl(sK19_skl),sK19_skl)|sQ687_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f5628])).
% 9.04/1.86 fof(f5636,plain,(
% 9.04/1.86 $false|sQ687_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f5630,f193])).
% 9.04/1.86 fof(f5637,plain,(
% 9.04/1.86 sQ687_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f5636])).
% 9.04/1.86 fof(f5638,plain,(
% 9.04/1.86 $false|~sQ686_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f5626,f292])).
% 9.04/1.86 fof(f5639,plain,(
% 9.04/1.86 ~sQ686_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f5638])).
% 9.04/1.86 fof(f5641,plain,(
% 9.04/1.86 ~v1_xboole_0(sK17_skl)|~sQ678_spl),
% 9.04/1.86 inference(backward_demodulation,[status(thm)],[f5588,f279])).
% 9.04/1.86 fof(f5645,plain,(
% 9.04/1.86 $false|~sQ678_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f5641,f286])).
% 9.04/1.86 fof(f5646,plain,(
% 9.04/1.86 ~sQ678_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f5645])).
% 9.04/1.86 fof(f5648,plain,(
% 9.04/1.86 ~v1_xboole_0(sK17_skl)|~sQ684_spl),
% 9.04/1.86 inference(backward_demodulation,[status(thm)],[f5618,f292])).
% 9.04/1.86 fof(f5652,plain,(
% 9.04/1.86 $false|~sQ684_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f5648,f286])).
% 9.04/1.86 fof(f5653,plain,(
% 9.04/1.86 ~sQ684_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f5652])).
% 9.04/1.86 fof(f5669,definition,(
% 9.04/1.86 sQ690_spl <=> (v1_xboole_0(k1_zfmisc_1(sK15_skl)))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ690_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f5670,plain,(
% 9.04/1.86 v1_xboole_0(k1_zfmisc_1(sK15_skl))|~sQ690_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f5669])).
% 9.04/1.86 fof(f5685,plain,(
% 9.04/1.86 $false|~sQ690_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f5670,f207])).
% 9.04/1.86 fof(f5686,plain,(
% 9.04/1.86 ~sQ690_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f5685])).
% 9.04/1.86 fof(f5695,definition,(
% 9.04/1.86 sQ695_spl <=> (v1_xboole_0(k1_zfmisc_1(sK19_skl)))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ695_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f5696,plain,(
% 9.04/1.86 v1_xboole_0(k1_zfmisc_1(sK19_skl))|~sQ695_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f5695])).
% 9.04/1.86 fof(f5711,plain,(
% 9.04/1.86 $false|~sQ695_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f5696,f207])).
% 9.04/1.86 fof(f5712,plain,(
% 9.04/1.86 ~sQ695_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f5711])).
% 9.04/1.86 fof(f5777,definition,(
% 9.04/1.86 sQ707_spl <=> (v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK26_skl))))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ707_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f5778,plain,(
% 9.04/1.86 v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK26_skl)))|~sQ707_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f5777])).
% 9.04/1.86 fof(f5793,plain,(
% 9.04/1.86 $false|~sQ707_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f5778,f207])).
% 9.04/1.86 fof(f5794,plain,(
% 9.04/1.86 ~sQ707_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f5793])).
% 9.04/1.86 fof(f5802,definition,(
% 9.04/1.86 sQ712_spl <=> (sK21_skl=sK17_skl)),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ712_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f5803,plain,(
% 9.04/1.86 sK21_skl=sK17_skl|~sQ712_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f5802])).
% 9.04/1.86 fof(f5810,definition,(
% 9.04/1.86 sQ714_spl <=> (v1_xboole_0(sK21_skl))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ714_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f5811,plain,(
% 9.04/1.86 v1_xboole_0(sK21_skl)|~sQ714_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f5810])).
% 9.04/1.86 fof(f5813,definition,(
% 9.04/1.86 sQ715_spl <=> (m1_subset_1(sK8_skl(sK21_skl),sK21_skl))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ715_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f5815,plain,(
% 9.04/1.86 ~m1_subset_1(sK8_skl(sK21_skl),sK21_skl)|sQ715_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f5813])).
% 9.04/1.86 fof(f5821,plain,(
% 9.04/1.86 $false|sQ715_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f5815,f193])).
% 9.04/1.86 fof(f5822,plain,(
% 9.04/1.86 sQ715_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f5821])).
% 9.04/1.86 fof(f5823,plain,(
% 9.04/1.86 $false|~sQ714_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f5811,f298])).
% 9.04/1.86 fof(f5824,plain,(
% 9.04/1.86 ~sQ714_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f5823])).
% 9.04/1.86 fof(f5834,plain,(
% 9.04/1.86 ~v1_xboole_0(sK17_skl)|~sQ712_spl),
% 9.04/1.86 inference(backward_demodulation,[status(thm)],[f5803,f298])).
% 9.04/1.86 fof(f5837,plain,(
% 9.04/1.86 $false|~sQ712_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f5834,f286])).
% 9.04/1.86 fof(f5838,plain,(
% 9.04/1.86 ~sQ712_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f5837])).
% 9.04/1.86 fof(f5850,definition,(
% 9.04/1.86 sQ718_spl <=> (v1_xboole_0(k1_zfmisc_1(sK21_skl)))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ718_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f5851,plain,(
% 9.04/1.86 v1_xboole_0(k1_zfmisc_1(sK21_skl))|~sQ718_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f5850])).
% 9.04/1.86 fof(f5866,plain,(
% 9.04/1.86 $false|~sQ718_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f5851,f207])).
% 9.04/1.86 fof(f5867,plain,(
% 9.04/1.86 ~sQ718_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f5866])).
% 9.04/1.86 fof(f5951,definition,(
% 9.04/1.86 sQ734_spl <=> (v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK0_skl)))))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ734_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f5952,plain,(
% 9.04/1.86 v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK0_skl))))|~sQ734_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f5951])).
% 9.04/1.86 fof(f5967,plain,(
% 9.04/1.86 $false|~sQ734_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f5952,f207])).
% 9.04/1.86 fof(f5968,plain,(
% 9.04/1.86 ~sQ734_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f5967])).
% 9.04/1.86 fof(f6152,plain,(
% 9.04/1.86 ![X0]: (~l3_lattices(k1_lattice2(X0))|m1_filter_0(k6_domain_1(u1_struct_0(k1_lattice2(X0)),k6_lattices(k1_lattice2(X0))),k1_lattice2(X0))|v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~v13_lattices(X0))),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f3450,f252])).
% 9.04/1.86 fof(f6154,plain,(
% 9.04/1.86 ~l3_lattices(k1_lattice2(sK0_skl))|m1_filter_0(k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),k6_lattices(k1_lattice2(sK0_skl))),k1_lattice2(sK0_skl))|v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)),
% 9.04/1.86 inference(resolution,[status(thm)],[f6152,f99])).
% 9.04/1.86 fof(f6159,definition,(
% 9.04/1.86 sQ766_spl <=> (m1_filter_0(k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),k6_lattices(k1_lattice2(sK0_skl))),k1_lattice2(sK0_skl)))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ766_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f6160,plain,(
% 9.04/1.86 m1_filter_0(k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),k6_lattices(k1_lattice2(sK0_skl))),k1_lattice2(sK0_skl))|~sQ766_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f6159])).
% 9.04/1.86 fof(f6162,plain,(
% 9.04/1.86 ~sQ128_spl|sQ766_spl|sQ0_spl|~sQ1_spl|~sQ4_spl),
% 9.04/1.86 inference(split_clause,[status(thm)],[f6154,f1103,f6159,f378,f381,f392])).
% 9.04/1.86 fof(f6163,plain,(
% 9.04/1.86 m1_filter_0(k6_domain_1(u1_struct_0(k1_lattice2(sK0_skl)),k5_lattices(sK0_skl)),k1_lattice2(sK0_skl))|~sQ5_spl|~sQ766_spl),
% 9.04/1.86 inference(forward_demodulation,[status(thm)],[f396,f6160])).
% 9.04/1.86 fof(f6164,plain,(
% 9.04/1.86 m1_filter_0(k1_tarski(k5_lattices(sK0_skl)),k1_lattice2(sK0_skl))|~sQ121_spl|~sQ5_spl|~sQ766_spl),
% 9.04/1.86 inference(forward_demodulation,[status(thm)],[f1016,f6163])).
% 9.04/1.86 fof(f6193,plain,(
% 9.04/1.86 v3_struct_0(k1_lattice2(sK0_skl))|~v10_lattices(k1_lattice2(sK0_skl))|~l3_lattices(k1_lattice2(sK0_skl))|m1_filter_2(k1_tarski(k5_lattices(sK0_skl)),k1_lattice2(sK0_skl))|~sQ121_spl|~sQ5_spl|~sQ766_spl),
% 9.04/1.86 inference(resolution,[status(thm)],[f6164,f334])).
% 9.04/1.86 fof(f6195,definition,(
% 9.04/1.86 sQ770_spl <=> (m1_filter_2(k1_tarski(k5_lattices(sK0_skl)),k1_lattice2(sK0_skl)))),
% 9.04/1.86 introduced(definition,[new_symbols(definition,[sQ770_spl])],[split_symbol_definition])).
% 9.04/1.86 fof(f6196,plain,(
% 9.04/1.86 m1_filter_2(k1_tarski(k5_lattices(sK0_skl)),k1_lattice2(sK0_skl))|~sQ770_spl),
% 9.04/1.86 inference(component_clause,[status(thm)],[f6195])).
% 9.04/1.86 fof(f6198,plain,(
% 9.04/1.86 sQ115_spl|~sQ129_spl|~sQ128_spl|sQ770_spl|~sQ121_spl|~sQ5_spl|~sQ766_spl),
% 9.04/1.86 inference(split_clause,[status(thm)],[f6193,f993,f1106,f1103,f6195,f1015,f395,f6159])).
% 9.04/1.86 fof(f6200,plain,(
% 9.04/1.86 m2_filter_2(k1_tarski(k5_lattices(sK0_skl)),sK0_skl)|~sQ770_spl|~sQ2_spl),
% 9.04/1.86 inference(resolution,[status(thm)],[f6196,f385])).
% 9.04/1.86 fof(f6203,plain,(
% 9.04/1.86 $false|~sQ86_spl|~sQ770_spl|~sQ2_spl),
% 9.04/1.86 inference(forward_subsumption_resolution,[status(thm)],[f6200,f1030])).
% 9.04/1.86 fof(f6204,plain,(
% 9.04/1.86 ~sQ86_spl|~sQ770_spl|~sQ2_spl),
% 9.04/1.86 inference(contradiction_clause,[status(thm)],[f6203])).
% 9.04/1.86 fof(f6205,plain,(
% 9.04/1.86 $false),
% 9.04/1.86 inference(sat_refutation,[status(thm)],[f387,f398,f400,f402,f409,f411,f832,f1002,f1018,f1054,f1060,f1096,f1099,f1132,f1144,f1172,f1210,f1212,f1240,f1251,f1302,f1596,f1599,f1716,f2172,f2242,f2303,f2336,f2343,f2617,f2633,f2678,f2877,f2880,f3022,f3392,f3709,f3734,f3820,f3878,f4003,f4484,f4644,f4646,f4671,f4690,f4745,f5183,f5478,f5607,f5609,f5637,f5639,f5646,f5653,f5686,f5712,f5794,f5822,f5824,f5838,f5867,f5968,f6162,f6198,f6204])).
% 9.04/1.86 % SZS output end CNFRefutation for theBenchmark.p
% 9.04/1.89 % Elapsed time: 1.471725 seconds
% 9.04/1.89 % CPU time: 11.175415 seconds
% 9.04/1.89 % Total memory used: 238.213 MB
% 9.04/1.89 % Net memory used: 234.181 MB
%------------------------------------------------------------------------------