%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT305+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 : n011.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:36 PM UTC 2026
% Result : Theorem 4.55s 1.35s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT305+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n011.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Sun Sep 20 23:31:25 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.48 % Drodi V4.1.1
% 4.55/1.35 % Refutation found
% 4.55/1.35 % SZS status Theorem for theBenchmark: Theorem is valid
% 4.55/1.35 % SZS output start CNFRefutation for theBenchmark
% 4.55/1.35 fof(f1,conjecture,(
% 4.55/1.35 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> (! [C] :( m1_subset_1(C,u1_struct_0(A))=> ( r2_hidden(B,k18_filter_2(A,B))& r2_hidden(k4_lattices(A,B,C),k18_filter_2(A,B))& r2_hidden(k4_lattices(A,C,B),k18_filter_2(A,B)) ) ) )) )) )),
% 4.55/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.55/1.35 fof(f2,negated_conjecture,(
% 4.55/1.35 ~((! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> (! [C] :( m1_subset_1(C,u1_struct_0(A))=> ( r2_hidden(B,k18_filter_2(A,B))& r2_hidden(k4_lattices(A,B,C),k18_filter_2(A,B))& r2_hidden(k4_lattices(A,C,B),k18_filter_2(A,B)) ) ) )) )) ))),
% 4.55/1.35 inference(negated_conjecture,[status(cth)],[f1])).
% 4.55/1.35 fof(f3,axiom,(
% 4.55/1.35 (! [A,B] :( r2_hidden(A,B)=> ~ r2_hidden(B,A) ) )),
% 4.55/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.55/1.35 fof(f5,axiom,(
% 4.55/1.35 (! [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) ) ) ) )),
% 4.55/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.55/1.35 fof(f11,axiom,(
% 4.55/1.35 (! [A,B,C] :( ( ~ v3_struct_0(A)& v6_lattices(A)& l1_lattices(A)& m1_subset_1(B,u1_struct_0(A))& m1_subset_1(C,u1_struct_0(A)) )=> k4_lattices(A,B,C) = k4_lattices(A,C,B) ) )),
% 4.55/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.55/1.35 fof(f15,axiom,(
% 4.55/1.35 (! [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) ) )) )),
% 4.55/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.55/1.35 fof(f26,axiom,(
% 4.55/1.35 (! [A,B,C] :( ( ~ v3_struct_0(A)& v6_lattices(A)& l1_lattices(A)& m1_subset_1(B,u1_struct_0(A))& m1_subset_1(C,u1_struct_0(A)) )=> m1_subset_1(k4_lattices(A,B,C),u1_struct_0(A)) ) )),
% 4.55/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.55/1.35 fof(f28,axiom,(
% 4.55/1.35 (! [A] :( l1_lattices(A)=> l1_struct_0(A) ) )),
% 4.55/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.55/1.35 fof(f31,axiom,(
% 4.55/1.35 (! [A] :( l3_lattices(A)=> ( l1_lattices(A)& l2_lattices(A) ) ) )),
% 4.55/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.55/1.35 fof(f39,axiom,(
% 4.55/1.35 (? [A] : l1_lattices(A) )),
% 4.55/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.55/1.35 fof(f42,axiom,(
% 4.55/1.35 (? [A] : l3_lattices(A) )),
% 4.55/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.55/1.35 fof(f44,axiom,(
% 4.55/1.35 (! [A] :(? [B] : m1_subset_1(B,A) ))),
% 4.55/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.55/1.35 fof(f49,axiom,(
% 4.55/1.35 (! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) )),
% 4.55/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.55/1.35 fof(f50,axiom,(
% 4.55/1.35 v1_xboole_0(k1_xboole_0) ),
% 4.55/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.55/1.35 fof(f57,axiom,(
% 4.55/1.35 (! [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) ) )) ) )),
% 4.55/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.55/1.35 fof(f63,axiom,(
% 4.55/1.35 (? [A] :( v1_relat_1(A)& v1_xboole_0(A)& v1_funct_1(A) ) )),
% 4.55/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.55/1.35 fof(f65,axiom,(
% 4.55/1.35 (! [A] :(? [B] :( m1_subset_1(B,k1_zfmisc_1(A))& v1_xboole_0(B) ) ))),
% 4.55/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.55/1.35 fof(f73,axiom,(
% 4.55/1.35 (! [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,C)<=> r1_lattices(A,B,C) ) ) )),
% 4.55/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.55/1.35 fof(f74,axiom,(
% 4.55/1.35 (! [A,B] : r1_tarski(A,A) )),
% 4.55/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.55/1.35 fof(f75,axiom,(
% 4.55/1.35 (! [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) ) )),
% 4.55/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.55/1.35 fof(f77,axiom,(
% 4.55/1.35 (! [A] :( ( ~ v3_struct_0(A)& v6_lattices(A)& v8_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> (! [C] :( m1_subset_1(C,u1_struct_0(A))=> r1_lattices(A,k4_lattices(A,B,C),B) ) )) )) )),
% 4.55/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.55/1.35 fof(f78,axiom,(
% 4.55/1.35 (! [A,B] :( m1_subset_1(A,B)=> ( v1_xboole_0(B)| r2_hidden(A,B) ) ) )),
% 4.55/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.55/1.35 fof(f80,axiom,(
% 4.55/1.35 (! [A,B] :( m1_subset_1(A,k1_zfmisc_1(B))<=> r1_tarski(A,B) ) )),
% 4.55/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.55/1.35 fof(f82,axiom,(
% 4.55/1.35 (! [A,B,C] :~ ( r2_hidden(A,B)& m1_subset_1(B,k1_zfmisc_1(C))& v1_xboole_0(C) ) )),
% 4.55/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.55/1.35 fof(f83,axiom,(
% 4.55/1.35 (! [A] :( v1_xboole_0(A)=> A = k1_xboole_0 ) )),
% 4.55/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.55/1.35 fof(f84,axiom,(
% 4.55/1.35 (! [A,B] :~ ( r2_hidden(A,B)& v1_xboole_0(B) ) )),
% 4.55/1.35 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.55/1.35 fof(f86,plain,(
% 4.55/1.35 (?[A]: (((~v3_struct_0(A)&v10_lattices(A))&l3_lattices(A))&(?[B]: (m1_subset_1(B,u1_struct_0(A))&(?[C]: (m1_subset_1(C,u1_struct_0(A))&((~r2_hidden(B,k18_filter_2(A,B))|~r2_hidden(k4_lattices(A,B,C),k18_filter_2(A,B)))|~r2_hidden(k4_lattices(A,C,B),k18_filter_2(A,B)))))))))),
% 4.55/1.35 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 4.55/1.35 fof(f87,plain,(
% 4.55/1.35 (((~v3_struct_0(sK0_skl)&v10_lattices(sK0_skl))&l3_lattices(sK0_skl))&(m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))&(m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))&((~r2_hidden(sK1_skl,k18_filter_2(sK0_skl,sK1_skl))|~r2_hidden(k4_lattices(sK0_skl,sK1_skl,sK2_skl),k18_filter_2(sK0_skl,sK1_skl)))|~r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK1_skl),k18_filter_2(sK0_skl,sK1_skl))))))),
% 4.55/1.35 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)],[f86])).
% 4.55/1.35 fof(f88,plain,(
% 4.55/1.35 ~v3_struct_0(sK0_skl)),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f87])).
% 4.55/1.35 fof(f89,plain,(
% 4.55/1.35 v10_lattices(sK0_skl)),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f87])).
% 4.55/1.35 fof(f90,plain,(
% 4.55/1.35 l3_lattices(sK0_skl)),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f87])).
% 4.55/1.35 fof(f91,plain,(
% 4.55/1.35 m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f87])).
% 4.55/1.35 fof(f92,plain,(
% 4.55/1.35 m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f87])).
% 4.55/1.35 fof(f93,plain,(
% 4.55/1.35 ~r2_hidden(sK1_skl,k18_filter_2(sK0_skl,sK1_skl))|~r2_hidden(k4_lattices(sK0_skl,sK1_skl,sK2_skl),k18_filter_2(sK0_skl,sK1_skl))|~r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK1_skl),k18_filter_2(sK0_skl,sK1_skl))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f87])).
% 4.55/1.35 fof(f94,plain,(
% 4.55/1.35 ![A,B]: (~r2_hidden(A,B)|~r2_hidden(B,A))),
% 4.55/1.35 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 4.55/1.35 fof(f95,plain,(
% 4.55/1.35 ![X0,X1]: (~r2_hidden(X0,X1)|~r2_hidden(X1,X0))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f94])).
% 4.55/1.35 fof(f98,plain,(
% 4.55/1.35 ![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))))),
% 4.55/1.35 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 4.55/1.35 fof(f102,plain,(
% 4.55/1.35 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v10_lattices(X0)|v6_lattices(X0))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f98])).
% 4.55/1.35 fof(f104,plain,(
% 4.55/1.35 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v10_lattices(X0)|v8_lattices(X0))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f98])).
% 4.55/1.35 fof(f105,plain,(
% 4.55/1.35 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v10_lattices(X0)|v9_lattices(X0))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f98])).
% 4.55/1.35 fof(f119,plain,(
% 4.55/1.35 ![A,B,C]: (((((v3_struct_0(A)|~v6_lattices(A))|~l1_lattices(A))|~m1_subset_1(B,u1_struct_0(A)))|~m1_subset_1(C,u1_struct_0(A)))|k4_lattices(A,B,C)=k4_lattices(A,C,B))),
% 4.55/1.35 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 4.55/1.35 fof(f120,plain,(
% 4.55/1.35 ![X0,X1,X2]: (v3_struct_0(X0)|~v6_lattices(X0)|~l1_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|k4_lattices(X0,X1,X2)=k4_lattices(X0,X2,X1))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f119])).
% 4.55/1.35 fof(f126,plain,(
% 4.55/1.35 ![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))))),
% 4.55/1.35 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 4.55/1.35 fof(f127,plain,(
% 4.55/1.35 ![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))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f126])).
% 4.55/1.35 fof(f134,plain,(
% 4.55/1.35 ![A,B,C]: (((((v3_struct_0(A)|~v6_lattices(A))|~l1_lattices(A))|~m1_subset_1(B,u1_struct_0(A)))|~m1_subset_1(C,u1_struct_0(A)))|m1_subset_1(k4_lattices(A,B,C),u1_struct_0(A)))),
% 4.55/1.35 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 4.55/1.35 fof(f135,plain,(
% 4.55/1.35 ![X0,X1,X2]: (v3_struct_0(X0)|~v6_lattices(X0)|~l1_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|m1_subset_1(k4_lattices(X0,X1,X2),u1_struct_0(X0)))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f134])).
% 4.55/1.35 fof(f136,plain,(
% 4.55/1.35 ![A]: (~l1_lattices(A)|l1_struct_0(A))),
% 4.55/1.35 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 4.55/1.35 fof(f137,plain,(
% 4.55/1.35 ![X0]: (~l1_lattices(X0)|l1_struct_0(X0))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f136])).
% 4.55/1.35 fof(f140,plain,(
% 4.55/1.35 ![A]: (~l3_lattices(A)|(l1_lattices(A)&l2_lattices(A)))),
% 4.55/1.35 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 4.55/1.35 fof(f141,plain,(
% 4.55/1.35 ![X0]: (~l3_lattices(X0)|l1_lattices(X0))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f140])).
% 4.55/1.35 fof(f154,plain,(
% 4.55/1.35 l1_lattices(sK3_skl)),
% 4.55/1.35 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(A,sK3_skl)],[f39])).
% 4.55/1.35 fof(f155,plain,(
% 4.55/1.35 l1_lattices(sK3_skl)),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f154])).
% 4.55/1.35 fof(f160,plain,(
% 4.55/1.35 l3_lattices(sK6_skl)),
% 4.55/1.35 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(A,sK6_skl)],[f42])).
% 4.55/1.35 fof(f161,plain,(
% 4.55/1.35 l3_lattices(sK6_skl)),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f160])).
% 4.55/1.35 fof(f164,plain,(
% 4.55/1.35 ![A]: m1_subset_1(sK8_skl(A),A)),
% 4.55/1.35 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(B,sK8_skl(A))],[f44])).
% 4.55/1.35 fof(f165,plain,(
% 4.55/1.35 ![X0]: (m1_subset_1(sK8_skl(X0),X0))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f164])).
% 4.55/1.35 fof(f176,plain,(
% 4.55/1.35 ![X0]: (~v1_xboole_0(k1_zfmisc_1(X0)))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f49])).
% 4.55/1.35 fof(f177,plain,(
% 4.55/1.35 v1_xboole_0(k1_xboole_0)),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f50])).
% 4.55/1.35 fof(f198,plain,(
% 4.55/1.35 ![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)))))),
% 4.55/1.35 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 4.55/1.35 fof(f199,plain,(
% 4.55/1.35 ![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))))))),
% 4.55/1.35 inference(NNF_transformation,[status(thm)],[f198])).
% 4.55/1.35 fof(f200,plain,(
% 4.55/1.35 ![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)))))))),
% 4.55/1.35 inference(miniscoping,[status(thm)],[f199])).
% 4.55/1.35 fof(f201,plain,(
% 4.55/1.35 ![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(sK12_skl(A,C,B),u1_struct_0(B))&A=sK12_skl(A,C,B))&r3_lattices(B,sK12_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)))))))),
% 4.55/1.35 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(D,sK12_skl(A,C,B))],[f200])).
% 4.55/1.35 fof(f205,plain,(
% 4.55/1.35 ![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))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f201])).
% 4.55/1.35 fof(f222,plain,(
% 4.55/1.35 ((v1_relat_1(sK18_skl)&v1_xboole_0(sK18_skl))&v1_funct_1(sK18_skl))),
% 4.55/1.35 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(A,sK18_skl)],[f63])).
% 4.55/1.35 fof(f223,plain,(
% 4.55/1.35 v1_relat_1(sK18_skl)),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f222])).
% 4.55/1.35 fof(f224,plain,(
% 4.55/1.35 v1_xboole_0(sK18_skl)),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f222])).
% 4.55/1.35 fof(f229,plain,(
% 4.55/1.35 ![A]: (m1_subset_1(sK20_skl(A),k1_zfmisc_1(A))&v1_xboole_0(sK20_skl(A)))),
% 4.55/1.35 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl]),skolemize(B,sK20_skl(A))],[f65])).
% 4.55/1.35 fof(f230,plain,(
% 4.55/1.35 ![X0]: (m1_subset_1(sK20_skl(X0),k1_zfmisc_1(X0)))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f229])).
% 4.55/1.35 fof(f231,plain,(
% 4.55/1.35 ![X0]: (v1_xboole_0(sK20_skl(X0)))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f229])).
% 4.55/1.35 fof(f253,plain,(
% 4.55/1.35 ![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,C)<=>r1_lattices(A,B,C)))),
% 4.55/1.35 inference(pre_NNF_transformation,[status(thm)],[f73])).
% 4.55/1.35 fof(f254,plain,(
% 4.55/1.35 ![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,C)|r1_lattices(A,B,C))&(r3_lattices(A,B,C)|~r1_lattices(A,B,C))))),
% 4.55/1.35 inference(NNF_transformation,[status(thm)],[f253])).
% 4.55/1.35 fof(f256,plain,(
% 4.55/1.35 ![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,X2)|~r1_lattices(X0,X1,X2))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f254])).
% 4.55/1.35 fof(f257,plain,(
% 4.55/1.35 ![A]: r1_tarski(A,A)),
% 4.55/1.35 inference(miniscoping,[status(thm)],[f74])).
% 4.55/1.35 fof(f258,plain,(
% 4.55/1.35 ![X0]: (r1_tarski(X0,X0))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f257])).
% 4.55/1.35 fof(f259,plain,(
% 4.55/1.35 ![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))),
% 4.55/1.35 inference(pre_NNF_transformation,[status(thm)],[f75])).
% 4.55/1.35 fof(f260,plain,(
% 4.55/1.35 ![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))),
% 4.55/1.35 inference(miniscoping,[status(thm)],[f259])).
% 4.55/1.35 fof(f261,plain,(
% 4.55/1.35 ![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))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f260])).
% 4.55/1.35 fof(f264,plain,(
% 4.55/1.35 ![A]: ((((v3_struct_0(A)|~v6_lattices(A))|~v8_lattices(A))|~l3_lattices(A))|(![B]: (~m1_subset_1(B,u1_struct_0(A))|(![C]: (~m1_subset_1(C,u1_struct_0(A))|r1_lattices(A,k4_lattices(A,B,C),B))))))),
% 4.55/1.35 inference(pre_NNF_transformation,[status(thm)],[f77])).
% 4.55/1.35 fof(f265,plain,(
% 4.55/1.35 ![X0,X1,X2]: (v3_struct_0(X0)|~v6_lattices(X0)|~v8_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|r1_lattices(X0,k4_lattices(X0,X1,X2),X1))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f264])).
% 4.55/1.35 fof(f266,plain,(
% 4.55/1.35 ![A,B]: (~m1_subset_1(A,B)|(v1_xboole_0(B)|r2_hidden(A,B)))),
% 4.55/1.35 inference(pre_NNF_transformation,[status(thm)],[f78])).
% 4.55/1.35 fof(f267,plain,(
% 4.55/1.35 ![X0,X1]: (~m1_subset_1(X0,X1)|v1_xboole_0(X1)|r2_hidden(X0,X1))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f266])).
% 4.55/1.35 fof(f273,plain,(
% 4.55/1.35 ![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)))),
% 4.55/1.35 inference(NNF_transformation,[status(thm)],[f80])).
% 4.55/1.35 fof(f274,plain,(
% 4.55/1.35 (![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)))),
% 4.55/1.35 inference(miniscoping,[status(thm)],[f273])).
% 4.55/1.35 fof(f275,plain,(
% 4.55/1.35 ![X0,X1]: (~m1_subset_1(X0,k1_zfmisc_1(X1))|r1_tarski(X0,X1))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f274])).
% 4.55/1.35 fof(f276,plain,(
% 4.55/1.35 ![X0,X1]: (m1_subset_1(X0,k1_zfmisc_1(X1))|~r1_tarski(X0,X1))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f274])).
% 4.55/1.35 fof(f280,plain,(
% 4.55/1.35 ![A,B,C]: ((~r2_hidden(A,B)|~m1_subset_1(B,k1_zfmisc_1(C)))|~v1_xboole_0(C))),
% 4.55/1.35 inference(pre_NNF_transformation,[status(thm)],[f82])).
% 4.55/1.35 fof(f281,plain,(
% 4.55/1.35 ![C]: ((![B]: ((![A]: ~r2_hidden(A,B))|~m1_subset_1(B,k1_zfmisc_1(C))))|~v1_xboole_0(C))),
% 4.55/1.35 inference(miniscoping,[status(thm)],[f280])).
% 4.55/1.35 fof(f282,plain,(
% 4.55/1.35 ![X0,X1,X2]: (~r2_hidden(X0,X1)|~m1_subset_1(X1,k1_zfmisc_1(X2))|~v1_xboole_0(X2))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f281])).
% 4.55/1.35 fof(f283,plain,(
% 4.55/1.35 ![A]: (~v1_xboole_0(A)|A=k1_xboole_0)),
% 4.55/1.35 inference(pre_NNF_transformation,[status(thm)],[f83])).
% 4.55/1.35 fof(f284,plain,(
% 4.55/1.35 ![X0]: (~v1_xboole_0(X0)|X0=k1_xboole_0)),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f283])).
% 4.55/1.35 fof(f285,plain,(
% 4.55/1.35 ![A,B]: (~r2_hidden(A,B)|~v1_xboole_0(B))),
% 4.55/1.35 inference(pre_NNF_transformation,[status(thm)],[f84])).
% 4.55/1.35 fof(f286,plain,(
% 4.55/1.35 ![B]: ((![A]: ~r2_hidden(A,B))|~v1_xboole_0(B))),
% 4.55/1.35 inference(miniscoping,[status(thm)],[f285])).
% 4.55/1.35 fof(f287,plain,(
% 4.55/1.35 ![X0,X1]: (~r2_hidden(X0,X1)|~v1_xboole_0(X1))),
% 4.55/1.35 inference(cnf_transformation,[status(thm)],[f286])).
% 4.55/1.35 fof(f291,definition,(
% 4.55/1.35 sQ0_spl <=> (r2_hidden(sK1_skl,k18_filter_2(sK0_skl,sK1_skl)))),
% 4.55/1.35 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 4.55/1.35 fof(f294,definition,(
% 4.55/1.35 sQ1_spl <=> (r2_hidden(k4_lattices(sK0_skl,sK1_skl,sK2_skl),k18_filter_2(sK0_skl,sK1_skl)))),
% 4.55/1.35 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 4.55/1.35 fof(f296,plain,(
% 4.55/1.35 ~r2_hidden(k4_lattices(sK0_skl,sK1_skl,sK2_skl),k18_filter_2(sK0_skl,sK1_skl))|sQ1_spl),
% 4.55/1.35 inference(component_clause,[status(thm)],[f294])).
% 4.55/1.35 fof(f297,definition,(
% 4.55/1.35 sQ2_spl <=> (r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK1_skl),k18_filter_2(sK0_skl,sK1_skl)))),
% 4.55/1.35 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 4.55/1.35 fof(f299,plain,(
% 4.55/1.35 ~r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK1_skl),k18_filter_2(sK0_skl,sK1_skl))|sQ2_spl),
% 4.55/1.35 inference(component_clause,[status(thm)],[f297])).
% 4.55/1.35 fof(f300,plain,(
% 4.55/1.35 ~sQ0_spl|~sQ1_spl|~sQ2_spl),
% 4.55/1.35 inference(split_clause,[status(thm)],[f93,f291,f294,f297])).
% 4.55/1.35 fof(f301,plain,(
% 4.55/1.35 ![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))),
% 4.55/1.35 inference(destructive_equality_resolution,[status(thm)],[f205])).
% 4.55/1.35 fof(f317,plain,(
% 4.55/1.35 ![X0]: (v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|k18_filter_2(sK0_skl,X0)=a_2_0_filter_2(sK0_skl,X0))),
% 4.55/1.35 inference(resolution,[status(thm)],[f127,f90])).
% 4.55/1.35 fof(f318,definition,(
% 4.55/1.35 sQ6_spl <=> (v3_struct_0(sK0_skl))),
% 4.55/1.35 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 4.55/1.35 fof(f319,plain,(
% 4.55/1.35 v3_struct_0(sK0_skl)|~sQ6_spl),
% 4.55/1.35 inference(component_clause,[status(thm)],[f318])).
% 4.55/1.35 fof(f321,definition,(
% 4.55/1.35 sQ7_spl <=> (v10_lattices(sK0_skl))),
% 4.55/1.35 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 4.55/1.35 fof(f323,plain,(
% 4.55/1.35 ~v10_lattices(sK0_skl)|sQ7_spl),
% 4.55/1.35 inference(component_clause,[status(thm)],[f321])).
% 4.55/1.35 fof(f324,definition,(
% 4.55/1.35 ![X0]: (sQ8_spl <=> (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k18_filter_2(sK0_skl,X0)=a_2_0_filter_2(sK0_skl,X0)))),
% 4.55/1.35 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 4.55/1.35 fof(f325,plain,(
% 4.55/1.35 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k18_filter_2(sK0_skl,X0)=a_2_0_filter_2(sK0_skl,X0)|~sQ8_spl)),
% 4.55/1.35 inference(component_clause,[status(thm)],[f324])).
% 4.55/1.35 fof(f327,plain,(
% 4.55/1.35 sQ6_spl|~sQ7_spl|sQ8_spl),
% 4.55/1.35 inference(split_clause,[status(thm)],[f317,f318,f321,f324])).
% 4.55/1.35 fof(f328,plain,(
% 4.55/1.35 $false|sQ7_spl),
% 4.55/1.35 inference(forward_subsumption_resolution,[status(thm)],[f323,f89])).
% 4.55/1.35 fof(f329,plain,(
% 4.55/1.35 sQ7_spl),
% 4.55/1.35 inference(contradiction_clause,[status(thm)],[f328])).
% 4.55/1.35 fof(f330,plain,(
% 4.55/1.35 $false|~sQ6_spl),
% 4.55/1.35 inference(forward_subsumption_resolution,[status(thm)],[f319,f88])).
% 4.55/1.35 fof(f331,plain,(
% 4.55/1.35 ~sQ6_spl),
% 4.55/1.35 inference(contradiction_clause,[status(thm)],[f330])).
% 4.55/1.35 fof(f354,plain,(
% 4.55/1.35 ![X0]: (~r2_hidden(X0,k1_xboole_0))),
% 4.55/1.35 inference(resolution,[status(thm)],[f177,f287])).
% 4.55/1.35 fof(f358,definition,(
% 4.55/1.35 sQ15_spl <=> (l3_lattices(sK0_skl))),
% 4.55/1.35 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 4.55/1.35 fof(f360,plain,(
% 4.55/1.35 ~l3_lattices(sK0_skl)|sQ15_spl),
% 4.55/1.35 inference(component_clause,[status(thm)],[f358])).
% 4.55/1.35 fof(f365,plain,(
% 4.55/1.35 $false|sQ15_spl),
% 4.55/1.35 inference(forward_subsumption_resolution,[status(thm)],[f360,f90])).
% 4.55/1.35 fof(f366,plain,(
% 4.55/1.35 sQ15_spl),
% 4.55/1.35 inference(contradiction_clause,[status(thm)],[f365])).
% 4.55/1.35 fof(f378,plain,(
% 4.55/1.35 ~l3_lattices(sK0_skl)|~v10_lattices(sK0_skl)|v6_lattices(sK0_skl)),
% 4.55/1.35 inference(resolution,[status(thm)],[f102,f88])).
% 4.55/1.35 fof(f379,definition,(
% 4.55/1.35 sQ18_spl <=> (v6_lattices(sK0_skl))),
% 4.55/1.35 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 4.55/1.35 fof(f380,plain,(
% 4.55/1.35 v6_lattices(sK0_skl)|~sQ18_spl),
% 4.55/1.35 inference(component_clause,[status(thm)],[f379])).
% 4.55/1.35 fof(f382,plain,(
% 4.55/1.35 ~sQ15_spl|~sQ7_spl|sQ18_spl),
% 4.55/1.35 inference(split_clause,[status(thm)],[f378,f358,f321,f379])).
% 4.55/1.35 fof(f388,plain,(
% 4.55/1.35 ~l3_lattices(sK0_skl)|~v10_lattices(sK0_skl)|v8_lattices(sK0_skl)),
% 4.55/1.35 inference(resolution,[status(thm)],[f104,f88])).
% 4.55/1.35 fof(f389,definition,(
% 4.55/1.35 sQ20_spl <=> (v8_lattices(sK0_skl))),
% 4.55/1.35 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 4.55/1.35 fof(f392,plain,(
% 4.55/1.35 ~sQ15_spl|~sQ7_spl|sQ20_spl),
% 4.55/1.35 inference(split_clause,[status(thm)],[f388,f358,f321,f389])).
% 4.55/1.35 fof(f393,plain,(
% 4.55/1.35 ![X0,X1]: (v3_struct_0(sK0_skl)|~l1_lattices(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|~m1_subset_1(X1,u1_struct_0(sK0_skl))|m1_subset_1(k4_lattices(sK0_skl,X0,X1),u1_struct_0(sK0_skl))|~sQ18_spl)),
% 4.55/1.35 inference(resolution,[status(thm)],[f380,f135])).
% 4.55/1.35 fof(f394,definition,(
% 4.55/1.35 sQ21_spl <=> (l1_lattices(sK0_skl))),
% 4.55/1.35 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 4.55/1.35 fof(f396,plain,(
% 4.55/1.35 ~l1_lattices(sK0_skl)|sQ21_spl),
% 4.55/1.35 inference(component_clause,[status(thm)],[f394])).
% 4.55/1.35 fof(f397,definition,(
% 4.55/1.35 ![X0,X1]: (sQ22_spl <=> (~m1_subset_1(X0,u1_struct_0(sK0_skl))|~m1_subset_1(X1,u1_struct_0(sK0_skl))|m1_subset_1(k4_lattices(sK0_skl,X0,X1),u1_struct_0(sK0_skl))))),
% 4.55/1.35 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 4.55/1.35 fof(f398,plain,(
% 4.55/1.35 ![X0,X1]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|~m1_subset_1(X1,u1_struct_0(sK0_skl))|m1_subset_1(k4_lattices(sK0_skl,X0,X1),u1_struct_0(sK0_skl))|~sQ22_spl)),
% 4.55/1.35 inference(component_clause,[status(thm)],[f397])).
% 4.55/1.35 fof(f400,plain,(
% 4.55/1.35 sQ6_spl|~sQ21_spl|sQ22_spl|~sQ18_spl),
% 4.55/1.35 inference(split_clause,[status(thm)],[f393,f318,f394,f397,f379])).
% 4.55/1.35 fof(f405,plain,(
% 4.55/1.35 k18_filter_2(sK0_skl,sK1_skl)=a_2_0_filter_2(sK0_skl,sK1_skl)|~sQ8_spl),
% 4.55/1.35 inference(resolution,[status(thm)],[f325,f91])).
% 4.55/1.35 fof(f439,plain,(
% 4.55/1.35 ~l3_lattices(sK0_skl)|v3_struct_0(sK0_skl)|v9_lattices(sK0_skl)),
% 4.55/1.35 inference(resolution,[status(thm)],[f105,f89])).
% 4.55/1.35 fof(f440,definition,(
% 4.55/1.35 sQ30_spl <=> (v9_lattices(sK0_skl))),
% 4.55/1.35 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 4.55/1.35 fof(f443,plain,(
% 4.55/1.35 ~sQ15_spl|sQ6_spl|sQ30_spl),
% 4.55/1.35 inference(split_clause,[status(thm)],[f439,f358,f318,f440])).
% 4.55/1.35 fof(f563,definition,(
% 4.55/1.35 ![X0]: (sQ50_spl <=> (~m1_subset_1(X0,u1_struct_0(sK0_skl))))),
% 4.55/1.35 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 4.55/1.35 fof(f564,plain,(
% 4.55/1.35 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|~sQ50_spl)),
% 4.55/1.35 inference(component_clause,[status(thm)],[f563])).
% 4.55/1.35 fof(f570,plain,(
% 4.55/1.35 $false|~sQ50_spl),
% 4.55/1.35 inference(backward_subsumption_resolution,[status(thm)],[f92,f564])).
% 4.55/1.35 fof(f573,plain,(
% 4.55/1.35 ~sQ50_spl),
% 4.55/1.35 inference(contradiction_clause,[status(thm)],[f570])).
% 4.55/1.35 fof(f604,plain,(
% 4.55/1.35 l1_struct_0(sK3_skl)),
% 4.55/1.35 inference(resolution,[status(thm)],[f137,f155])).
% 4.55/1.35 fof(f605,plain,(
% 4.55/1.35 l1_lattices(sK6_skl)),
% 4.55/1.35 inference(resolution,[status(thm)],[f141,f161])).
% 4.55/1.35 fof(f606,plain,(
% 4.55/1.35 l1_lattices(sK0_skl)),
% 4.55/1.35 inference(resolution,[status(thm)],[f141,f90])).
% 4.55/1.35 fof(f607,plain,(
% 4.55/1.35 $false|sQ21_spl),
% 4.55/1.35 inference(forward_subsumption_resolution,[status(thm)],[f606,f396])).
% 4.55/1.35 fof(f608,plain,(
% 4.55/1.35 sQ21_spl),
% 4.55/1.35 inference(contradiction_clause,[status(thm)],[f607])).
% 4.55/1.35 fof(f609,plain,(
% 4.55/1.35 l1_struct_0(sK6_skl)),
% 4.55/1.35 inference(resolution,[status(thm)],[f605,f137])).
% 4.55/1.35 fof(f634,plain,(
% 4.55/1.35 l1_struct_0(sK0_skl)),
% 4.55/1.35 inference(resolution,[status(thm)],[f606,f137])).
% 4.55/1.35 fof(f636,plain,(
% 4.55/1.35 ![X0,X1]: (v3_struct_0(sK0_skl)|~v6_lattices(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|~m1_subset_1(X1,u1_struct_0(sK0_skl))|k4_lattices(sK0_skl,X0,X1)=k4_lattices(sK0_skl,X1,X0))),
% 4.55/1.35 inference(resolution,[status(thm)],[f606,f120])).
% 4.55/1.35 fof(f645,definition,(
% 4.55/1.35 ![X0,X1]: (sQ63_spl <=> (~m1_subset_1(X0,u1_struct_0(sK0_skl))|~m1_subset_1(X1,u1_struct_0(sK0_skl))|k4_lattices(sK0_skl,X0,X1)=k4_lattices(sK0_skl,X1,X0)))),
% 4.55/1.35 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 4.55/1.35 fof(f646,plain,(
% 4.55/1.35 ![X0,X1]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|~m1_subset_1(X1,u1_struct_0(sK0_skl))|k4_lattices(sK0_skl,X0,X1)=k4_lattices(sK0_skl,X1,X0)|~sQ63_spl)),
% 4.55/1.35 inference(component_clause,[status(thm)],[f645])).
% 4.55/1.35 fof(f648,plain,(
% 4.55/1.35 sQ6_spl|~sQ18_spl|sQ63_spl),
% 4.55/1.35 inference(split_clause,[status(thm)],[f636,f318,f379,f645])).
% 4.55/1.35 fof(f655,plain,(
% 4.55/1.35 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k4_lattices(sK0_skl,X0,sK1_skl)=k4_lattices(sK0_skl,sK1_skl,X0)|~sQ63_spl)),
% 4.55/1.35 inference(resolution,[status(thm)],[f646,f91])).
% 4.55/1.35 fof(f677,plain,(
% 4.55/1.35 ![X0]: (v1_xboole_0(X0)|r2_hidden(sK8_skl(X0),X0))),
% 4.55/1.35 inference(resolution,[status(thm)],[f165,f267])).
% 4.55/1.35 fof(f681,plain,(
% 4.55/1.35 ![X0]: (sK20_skl(X0)=k1_xboole_0)),
% 4.55/1.35 inference(resolution,[status(thm)],[f284,f231])).
% 4.55/1.35 fof(f682,plain,(
% 4.55/1.35 sK18_skl=k1_xboole_0),
% 4.55/1.35 inference(resolution,[status(thm)],[f284,f224])).
% 4.55/1.35 fof(f690,plain,(
% 4.55/1.35 v1_relat_1(k1_xboole_0)),
% 4.55/1.35 inference(backward_demodulation,[status(thm)],[f682,f223])).
% 4.55/1.35 fof(f816,plain,(
% 4.55/1.35 ![X0]: (m1_subset_1(k1_xboole_0,k1_zfmisc_1(X0)))),
% 4.55/1.35 inference(forward_demodulation,[status(thm)],[f681,f230])).
% 4.55/1.35 fof(f845,plain,(
% 4.55/1.35 k4_lattices(sK0_skl,sK2_skl,sK1_skl)=k4_lattices(sK0_skl,sK1_skl,sK2_skl)|~sQ63_spl),
% 4.55/1.35 inference(resolution,[status(thm)],[f655,f92])).
% 4.55/1.35 fof(f847,plain,(
% 4.55/1.35 ~m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))|~m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))|m1_subset_1(k4_lattices(sK0_skl,sK2_skl,sK1_skl),u1_struct_0(sK0_skl))|~sQ22_spl|~sQ63_spl),
% 4.55/1.35 inference(paramodulation,[status(thm)],[f845,f398])).
% 4.55/1.35 fof(f848,definition,(
% 4.55/1.35 sQ84_spl <=> (m1_subset_1(sK1_skl,u1_struct_0(sK0_skl)))),
% 4.55/1.35 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 4.55/1.35 fof(f850,plain,(
% 4.55/1.35 ~m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))|sQ84_spl),
% 4.55/1.35 inference(component_clause,[status(thm)],[f848])).
% 4.55/1.35 fof(f851,definition,(
% 4.55/1.35 sQ85_spl <=> (m1_subset_1(sK2_skl,u1_struct_0(sK0_skl)))),
% 4.55/1.35 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 4.55/1.35 fof(f853,plain,(
% 4.55/1.35 ~m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))|sQ85_spl),
% 4.55/1.35 inference(component_clause,[status(thm)],[f851])).
% 4.55/1.35 fof(f854,definition,(
% 4.55/1.35 sQ86_spl <=> (m1_subset_1(k4_lattices(sK0_skl,sK2_skl,sK1_skl),u1_struct_0(sK0_skl)))),
% 4.55/1.35 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 4.55/1.35 fof(f857,plain,(
% 4.55/1.35 ~sQ84_spl|~sQ85_spl|sQ86_spl|~sQ22_spl|~sQ63_spl),
% 4.55/1.35 inference(split_clause,[status(thm)],[f847,f848,f851,f854,f397,f645])).
% 4.55/1.35 fof(f858,plain,(
% 4.55/1.35 $false|sQ85_spl),
% 4.55/1.35 inference(forward_subsumption_resolution,[status(thm)],[f853,f92])).
% 4.55/1.35 fof(f859,plain,(
% 4.55/1.35 sQ85_spl),
% 4.55/1.35 inference(contradiction_clause,[status(thm)],[f858])).
% 4.55/1.35 fof(f860,plain,(
% 4.55/1.35 $false|sQ84_spl),
% 4.55/1.35 inference(forward_subsumption_resolution,[status(thm)],[f850,f91])).
% 4.55/1.35 fof(f861,plain,(
% 4.55/1.35 sQ84_spl),
% 4.55/1.35 inference(contradiction_clause,[status(thm)],[f860])).
% 4.55/1.35 fof(f877,plain,(
% 4.55/1.35 ![X0]: (r1_tarski(k1_xboole_0,X0))),
% 4.55/1.35 inference(resolution,[status(thm)],[f275,f816])).
% 4.55/1.35 fof(f883,plain,(
% 4.55/1.35 ![X0,X1]: (~r1_tarski(X0,X1)|v1_xboole_0(k1_zfmisc_1(X1))|r2_hidden(X0,k1_zfmisc_1(X1)))),
% 4.55/1.35 inference(resolution,[status(thm)],[f276,f267])).
% 4.55/1.35 fof(f884,plain,(
% 5.19/1.37 ![X0,X1]: (~r1_tarski(X0,X1)|r2_hidden(X0,k1_zfmisc_1(X1)))),
% 5.19/1.37 inference(forward_subsumption_resolution,[status(thm)],[f883,f176])).
% 5.19/1.37 fof(f897,plain,(
% 5.19/1.37 ![X0,X1]: (~r1_tarski(X0,X1)|~r2_hidden(k1_zfmisc_1(X1),X0))),
% 5.19/1.37 inference(resolution,[status(thm)],[f884,f95])).
% 5.19/1.37 fof(f903,plain,(
% 5.19/1.37 ![X0,X1]: (~r1_tarski(k1_zfmisc_1(X0),X1)|~r1_tarski(k1_zfmisc_1(X1),X0))),
% 5.19/1.37 inference(resolution,[status(thm)],[f897,f884])).
% 5.19/1.37 fof(f905,plain,(
% 5.19/1.37 ![X0]: (~r1_tarski(k1_zfmisc_1(k1_zfmisc_1(X0)),X0))),
% 5.19/1.37 inference(resolution,[status(thm)],[f903,f258])).
% 5.19/1.37 fof(f996,plain,(
% 5.19/1.37 ![X0,X1]: (~r2_hidden(X0,X1)|~m1_subset_1(X1,k1_zfmisc_1(k1_xboole_0)))),
% 5.19/1.37 inference(resolution,[status(thm)],[f282,f177])).
% 5.19/1.37 fof(f999,plain,(
% 5.19/1.37 ![X0]: (~r2_hidden(X0,sK8_skl(k1_zfmisc_1(k1_xboole_0))))),
% 5.19/1.37 inference(resolution,[status(thm)],[f996,f165])).
% 5.19/1.37 fof(f1005,definition,(
% 5.19/1.37 sQ92_spl <=> (v1_xboole_0(k1_xboole_0))),
% 5.19/1.37 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 5.19/1.37 fof(f1007,plain,(
% 5.19/1.37 ~v1_xboole_0(k1_xboole_0)|sQ92_spl),
% 5.19/1.37 inference(component_clause,[status(thm)],[f1005])).
% 5.19/1.37 fof(f1025,plain,(
% 5.19/1.37 v1_xboole_0(sK8_skl(k1_zfmisc_1(k1_xboole_0)))),
% 5.19/1.37 inference(resolution,[status(thm)],[f999,f677])).
% 5.19/1.37 fof(f1028,plain,(
% 5.19/1.37 sK8_skl(k1_zfmisc_1(k1_xboole_0))=k1_xboole_0),
% 5.19/1.37 inference(resolution,[status(thm)],[f1025,f284])).
% 5.19/1.37 fof(f1033,definition,(
% 5.19/1.37 sQ95_spl <=> (v1_relat_1(sK8_skl(k1_zfmisc_1(k1_xboole_0))))),
% 5.19/1.37 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 5.19/1.37 fof(f1035,plain,(
% 5.19/1.37 ~v1_relat_1(sK8_skl(k1_zfmisc_1(k1_xboole_0)))|sQ95_spl),
% 5.19/1.37 inference(component_clause,[status(thm)],[f1033])).
% 5.19/1.37 fof(f1050,definition,(
% 5.19/1.37 sQ97_spl <=> (v1_xboole_0(k1_zfmisc_1(k1_xboole_0)))),
% 5.19/1.37 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 5.19/1.37 fof(f1051,plain,(
% 5.19/1.37 v1_xboole_0(k1_zfmisc_1(k1_xboole_0))|~sQ97_spl),
% 5.19/1.37 inference(component_clause,[status(thm)],[f1050])).
% 5.19/1.37 fof(f1061,plain,(
% 5.19/1.37 $false|~sQ97_spl),
% 5.19/1.37 inference(forward_subsumption_resolution,[status(thm)],[f1051,f176])).
% 5.19/1.37 fof(f1062,plain,(
% 5.19/1.37 ~sQ97_spl),
% 5.19/1.37 inference(contradiction_clause,[status(thm)],[f1061])).
% 5.19/1.37 fof(f1065,plain,(
% 5.19/1.37 ~v1_relat_1(k1_xboole_0)|sQ95_spl),
% 5.19/1.37 inference(forward_demodulation,[status(thm)],[f1028,f1035])).
% 5.19/1.37 fof(f1066,plain,(
% 5.19/1.37 $false|sQ95_spl),
% 5.19/1.37 inference(forward_subsumption_resolution,[status(thm)],[f1065,f690])).
% 5.19/1.37 fof(f1067,plain,(
% 5.19/1.37 sQ95_spl),
% 5.19/1.37 inference(contradiction_clause,[status(thm)],[f1066])).
% 5.19/1.37 fof(f1098,definition,(
% 5.19/1.37 sQ102_spl <=> (l1_struct_0(sK0_skl))),
% 5.19/1.37 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 5.19/1.37 fof(f1100,plain,(
% 5.19/1.37 ~l1_struct_0(sK0_skl)|sQ102_spl),
% 5.19/1.37 inference(component_clause,[status(thm)],[f1098])).
% 5.19/1.37 fof(f1103,plain,(
% 5.19/1.37 $false|sQ102_spl),
% 5.19/1.37 inference(forward_subsumption_resolution,[status(thm)],[f1100,f634])).
% 5.19/1.37 fof(f1104,plain,(
% 5.19/1.37 sQ102_spl),
% 5.19/1.37 inference(contradiction_clause,[status(thm)],[f1103])).
% 5.19/1.37 fof(f1139,definition,(
% 5.19/1.37 sQ106_spl <=> (m1_subset_1(sK8_skl(u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)))),
% 5.19/1.37 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 5.19/1.37 fof(f1141,plain,(
% 5.19/1.37 ~m1_subset_1(sK8_skl(u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|sQ106_spl),
% 5.19/1.37 inference(component_clause,[status(thm)],[f1139])).
% 5.19/1.37 fof(f1146,plain,(
% 5.19/1.37 $false|sQ106_spl),
% 5.19/1.37 inference(forward_subsumption_resolution,[status(thm)],[f1141,f165])).
% 5.19/1.37 fof(f1147,plain,(
% 5.19/1.37 sQ106_spl),
% 5.19/1.37 inference(contradiction_clause,[status(thm)],[f1146])).
% 5.19/1.37 fof(f1313,plain,(
% 5.19/1.37 ![X0,X1]: (v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|r2_hidden(X1,a_2_0_filter_2(sK0_skl,X0))|~m1_subset_1(X1,u1_struct_0(sK0_skl))|~r3_lattices(sK0_skl,X1,X0))),
% 5.19/1.37 inference(resolution,[status(thm)],[f301,f89])).
% 5.19/1.37 fof(f1314,definition,(
% 5.19/1.37 ![X0,X1]: (sQ131_spl <=> (~m1_subset_1(X0,u1_struct_0(sK0_skl))|r2_hidden(X1,a_2_0_filter_2(sK0_skl,X0))|~m1_subset_1(X1,u1_struct_0(sK0_skl))|~r3_lattices(sK0_skl,X1,X0)))),
% 5.19/1.37 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 5.19/1.37 fof(f1315,plain,(
% 5.19/1.37 ![X0,X1]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|r2_hidden(X1,a_2_0_filter_2(sK0_skl,X0))|~m1_subset_1(X1,u1_struct_0(sK0_skl))|~r3_lattices(sK0_skl,X1,X0)|~sQ131_spl)),
% 5.19/1.37 inference(component_clause,[status(thm)],[f1314])).
% 5.19/1.37 fof(f1317,plain,(
% 5.19/1.37 sQ6_spl|~sQ15_spl|sQ131_spl),
% 5.19/1.37 inference(split_clause,[status(thm)],[f1313,f318,f358,f1314])).
% 5.19/1.37 fof(f1697,plain,(
% 5.19/1.37 ~r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK1_skl),k18_filter_2(sK0_skl,sK1_skl))|~sQ63_spl|sQ1_spl),
% 5.19/1.37 inference(forward_demodulation,[status(thm)],[f845,f296])).
% 5.19/1.37 fof(f1706,definition,(
% 5.19/1.37 sQ181_spl <=> (l1_struct_0(sK3_skl))),
% 5.19/1.37 introduced(definition,[new_symbols(definition,[sQ181_spl])],[split_symbol_definition])).
% 5.19/1.37 fof(f1708,plain,(
% 5.19/1.37 ~l1_struct_0(sK3_skl)|sQ181_spl),
% 5.19/1.37 inference(component_clause,[status(thm)],[f1706])).
% 5.19/1.37 fof(f1711,plain,(
% 5.19/1.37 $false|sQ181_spl),
% 5.19/1.37 inference(forward_subsumption_resolution,[status(thm)],[f1708,f604])).
% 5.19/1.37 fof(f1712,plain,(
% 5.19/1.37 sQ181_spl),
% 5.19/1.37 inference(contradiction_clause,[status(thm)],[f1711])).
% 5.19/1.37 fof(f1805,definition,(
% 5.19/1.37 sQ194_spl <=> (l1_lattices(sK3_skl))),
% 5.19/1.37 introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition])).
% 5.19/1.37 fof(f1807,plain,(
% 5.19/1.37 ~l1_lattices(sK3_skl)|sQ194_spl),
% 5.19/1.37 inference(component_clause,[status(thm)],[f1805])).
% 5.19/1.37 fof(f1856,plain,(
% 5.19/1.37 $false|sQ194_spl),
% 5.19/1.37 inference(forward_subsumption_resolution,[status(thm)],[f1807,f155])).
% 5.19/1.37 fof(f1857,plain,(
% 5.19/1.37 sQ194_spl),
% 5.19/1.37 inference(contradiction_clause,[status(thm)],[f1856])).
% 5.19/1.37 fof(f2038,plain,(
% 5.19/1.37 ![X0,X1]: (v3_struct_0(sK0_skl)|~v8_lattices(sK0_skl)|~v9_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|~m1_subset_1(X1,u1_struct_0(sK0_skl))|r3_lattices(sK0_skl,X0,X0)|~sQ18_spl)),
% 5.19/1.37 inference(resolution,[status(thm)],[f261,f380])).
% 5.19/1.37 fof(f2039,definition,(
% 5.19/1.37 ![X0]: (sQ236_spl <=> (~m1_subset_1(X0,u1_struct_0(sK0_skl))|r3_lattices(sK0_skl,X0,X0)))),
% 5.19/1.37 introduced(definition,[new_symbols(definition,[sQ236_spl])],[split_symbol_definition])).
% 5.19/1.37 fof(f2040,plain,(
% 5.19/1.37 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|r3_lattices(sK0_skl,X0,X0)|~sQ236_spl)),
% 5.19/1.37 inference(component_clause,[status(thm)],[f2039])).
% 5.19/1.37 fof(f2042,plain,(
% 5.19/1.37 sQ6_spl|~sQ20_spl|~sQ30_spl|~sQ15_spl|sQ236_spl|sQ50_spl|~sQ18_spl),
% 5.19/1.37 inference(split_clause,[status(thm)],[f2038,f318,f389,f440,f358,f2039,f563,f379])).
% 5.19/1.37 fof(f2043,plain,(
% 5.19/1.37 ![X0,X1]: (v3_struct_0(sK0_skl)|~v8_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|~m1_subset_1(X1,u1_struct_0(sK0_skl))|r1_lattices(sK0_skl,k4_lattices(sK0_skl,X0,X1),X0)|~sQ18_spl)),
% 5.19/1.37 inference(resolution,[status(thm)],[f265,f380])).
% 5.19/1.37 fof(f2044,definition,(
% 5.19/1.37 ![X0,X1]: (sQ237_spl <=> (~m1_subset_1(X0,u1_struct_0(sK0_skl))|~m1_subset_1(X1,u1_struct_0(sK0_skl))|r1_lattices(sK0_skl,k4_lattices(sK0_skl,X0,X1),X0)))),
% 5.19/1.37 introduced(definition,[new_symbols(definition,[sQ237_spl])],[split_symbol_definition])).
% 5.19/1.37 fof(f2045,plain,(
% 5.19/1.37 ![X0,X1]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|~m1_subset_1(X1,u1_struct_0(sK0_skl))|r1_lattices(sK0_skl,k4_lattices(sK0_skl,X0,X1),X0)|~sQ237_spl)),
% 5.19/1.37 inference(component_clause,[status(thm)],[f2044])).
% 5.19/1.37 fof(f2047,plain,(
% 5.19/1.37 sQ6_spl|~sQ20_spl|~sQ15_spl|sQ237_spl|~sQ18_spl),
% 5.19/1.37 inference(split_clause,[status(thm)],[f2043,f318,f389,f358,f2044,f379])).
% 5.19/1.37 fof(f2050,plain,(
% 5.19/1.37 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK0_skl))|r2_hidden(X0,a_2_0_filter_2(sK0_skl,X0))|~m1_subset_1(X0,u1_struct_0(sK0_skl))|~sQ236_spl|~sQ131_spl)),
% 5.19/1.37 inference(resolution,[status(thm)],[f2040,f1315])).
% 5.19/1.37 fof(f2051,plain,(
% 5.19/1.37 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|r2_hidden(X0,a_2_0_filter_2(sK0_skl,X0))|~sQ236_spl|~sQ131_spl)),
% 5.19/1.37 inference(duplicate_literals_removal,[status(thm)],[f2050])).
% 5.19/1.37 fof(f2305,plain,(
% 5.19/1.37 ~m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))|~m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))|r1_lattices(sK0_skl,k4_lattices(sK0_skl,sK2_skl,sK1_skl),sK1_skl)|~sQ237_spl|~sQ63_spl),
% 5.19/1.37 inference(paramodulation,[status(thm)],[f845,f2045])).
% 5.19/1.37 fof(f2314,definition,(
% 5.19/1.37 sQ267_spl <=> (r1_lattices(sK0_skl,k4_lattices(sK0_skl,sK2_skl,sK1_skl),sK1_skl))),
% 5.19/1.37 introduced(definition,[new_symbols(definition,[sQ267_spl])],[split_symbol_definition])).
% 5.19/1.37 fof(f2315,plain,(
% 5.19/1.37 r1_lattices(sK0_skl,k4_lattices(sK0_skl,sK2_skl,sK1_skl),sK1_skl)|~sQ267_spl),
% 5.19/1.37 inference(component_clause,[status(thm)],[f2314])).
% 5.19/1.37 fof(f2317,plain,(
% 5.19/1.37 ~sQ84_spl|~sQ85_spl|sQ267_spl|~sQ237_spl|~sQ63_spl),
% 5.19/1.37 inference(split_clause,[status(thm)],[f2305,f848,f851,f2314,f2044,f645])).
% 5.19/1.37 fof(f2390,definition,(
% 5.19/1.37 sQ280_spl <=> (k1_xboole_0=k1_zfmisc_1(k1_xboole_0))),
% 5.19/1.37 introduced(definition,[new_symbols(definition,[sQ280_spl])],[split_symbol_definition])).
% 5.19/1.37 fof(f2391,plain,(
% 5.19/1.37 k1_xboole_0=k1_zfmisc_1(k1_xboole_0)|~sQ280_spl),
% 5.19/1.37 inference(component_clause,[status(thm)],[f2390])).
% 5.19/1.37 fof(f2519,plain,(
% 5.19/1.37 ~r1_tarski(k1_zfmisc_1(k1_xboole_0),k1_xboole_0)|~sQ280_spl),
% 5.19/1.37 inference(paramodulation,[status(thm)],[f2391,f905])).
% 5.19/1.37 fof(f2540,definition,(
% 5.19/1.37 sQ284_spl <=> (r2_hidden(sK16_skl(k1_xboole_0),k1_xboole_0))),
% 5.19/1.37 introduced(definition,[new_symbols(definition,[sQ284_spl])],[split_symbol_definition])).
% 5.19/1.37 fof(f2541,plain,(
% 5.19/1.37 r2_hidden(sK16_skl(k1_xboole_0),k1_xboole_0)|~sQ284_spl),
% 5.19/1.37 inference(component_clause,[status(thm)],[f2540])).
% 5.19/1.37 fof(f2548,plain,(
% 5.19/1.37 ~r1_tarski(k1_xboole_0,k1_xboole_0)|~sQ280_spl),
% 5.19/1.37 inference(forward_demodulation,[status(thm)],[f2391,f2519])).
% 5.19/1.37 fof(f2549,plain,(
% 5.19/1.37 $false|~sQ280_spl),
% 5.19/1.37 inference(forward_subsumption_resolution,[status(thm)],[f2548,f877])).
% 5.19/1.37 fof(f2550,plain,(
% 5.19/1.37 ~sQ280_spl),
% 5.19/1.37 inference(contradiction_clause,[status(thm)],[f2549])).
% 5.19/1.37 fof(f2551,plain,(
% 5.19/1.37 $false|~sQ284_spl),
% 5.19/1.37 inference(forward_subsumption_resolution,[status(thm)],[f2541,f354])).
% 5.19/1.37 fof(f2552,plain,(
% 5.19/1.37 ~sQ284_spl),
% 5.19/1.37 inference(contradiction_clause,[status(thm)],[f2551])).
% 5.19/1.37 fof(f2647,definition,(
% 5.19/1.37 sQ290_spl <=> (r2_hidden(sK8_skl(sK8_skl(k1_xboole_0)),k1_xboole_0))),
% 5.19/1.37 introduced(definition,[new_symbols(definition,[sQ290_spl])],[split_symbol_definition])).
% 5.19/1.37 fof(f2648,plain,(
% 5.19/1.37 r2_hidden(sK8_skl(sK8_skl(k1_xboole_0)),k1_xboole_0)|~sQ290_spl),
% 5.19/1.37 inference(component_clause,[status(thm)],[f2647])).
% 5.19/1.37 fof(f2651,plain,(
% 5.19/1.37 $false|~sQ290_spl),
% 5.19/1.37 inference(forward_subsumption_resolution,[status(thm)],[f2648,f354])).
% 5.19/1.37 fof(f2652,plain,(
% 5.19/1.37 ~sQ290_spl),
% 5.19/1.37 inference(contradiction_clause,[status(thm)],[f2651])).
% 5.19/1.37 fof(f3007,definition,(
% 5.19/1.37 sQ315_spl <=> (v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(k1_xboole_0))))),
% 5.19/1.37 introduced(definition,[new_symbols(definition,[sQ315_spl])],[split_symbol_definition])).
% 5.19/1.37 fof(f3008,plain,(
% 5.19/1.37 v1_xboole_0(k1_zfmisc_1(k1_zfmisc_1(k1_xboole_0)))|~sQ315_spl),
% 5.19/1.37 inference(component_clause,[status(thm)],[f3007])).
% 5.19/1.37 fof(f3018,plain,(
% 5.19/1.37 $false|~sQ315_spl),
% 5.19/1.37 inference(forward_subsumption_resolution,[status(thm)],[f3008,f176])).
% 5.19/1.37 fof(f3019,plain,(
% 5.19/1.37 ~sQ315_spl),
% 5.19/1.37 inference(contradiction_clause,[status(thm)],[f3018])).
% 5.19/1.37 fof(f3187,plain,(
% 5.19/1.37 v3_struct_0(sK0_skl)|~v6_lattices(sK0_skl)|~v8_lattices(sK0_skl)|~v9_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~m1_subset_1(k4_lattices(sK0_skl,sK2_skl,sK1_skl),u1_struct_0(sK0_skl))|~m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))|r3_lattices(sK0_skl,k4_lattices(sK0_skl,sK2_skl,sK1_skl),sK1_skl)|~sQ267_spl),
% 5.19/1.37 inference(resolution,[status(thm)],[f2315,f256])).
% 5.19/1.37 fof(f3188,definition,(
% 5.19/1.37 sQ331_spl <=> (r3_lattices(sK0_skl,k4_lattices(sK0_skl,sK2_skl,sK1_skl),sK1_skl))),
% 5.19/1.37 introduced(definition,[new_symbols(definition,[sQ331_spl])],[split_symbol_definition])).
% 5.19/1.37 fof(f3189,plain,(
% 5.19/1.37 r3_lattices(sK0_skl,k4_lattices(sK0_skl,sK2_skl,sK1_skl),sK1_skl)|~sQ331_spl),
% 5.19/1.37 inference(component_clause,[status(thm)],[f3188])).
% 5.19/1.37 fof(f3191,plain,(
% 5.19/1.37 sQ6_spl|~sQ18_spl|~sQ20_spl|~sQ30_spl|~sQ15_spl|~sQ86_spl|~sQ84_spl|sQ331_spl|~sQ267_spl),
% 5.19/1.37 inference(split_clause,[status(thm)],[f3187,f318,f379,f389,f440,f358,f854,f848,f3188,f2314])).
% 5.19/1.37 fof(f3204,definition,(
% 5.19/1.37 sQ332_spl <=> (l1_struct_0(sK6_skl))),
% 5.19/1.37 introduced(definition,[new_symbols(definition,[sQ332_spl])],[split_symbol_definition])).
% 5.19/1.37 fof(f3206,plain,(
% 5.19/1.37 ~l1_struct_0(sK6_skl)|sQ332_spl),
% 5.19/1.37 inference(component_clause,[status(thm)],[f3204])).
% 5.19/1.37 fof(f3209,plain,(
% 5.19/1.37 $false|sQ332_spl),
% 5.19/1.37 inference(forward_subsumption_resolution,[status(thm)],[f3206,f609])).
% 5.19/1.37 fof(f3210,plain,(
% 5.19/1.37 sQ332_spl),
% 5.19/1.37 inference(contradiction_clause,[status(thm)],[f3209])).
% 5.19/1.37 fof(f3239,definition,(
% 5.19/1.37 sQ333_spl <=> (l1_lattices(sK6_skl))),
% 5.19/1.37 introduced(definition,[new_symbols(definition,[sQ333_spl])],[split_symbol_definition])).
% 5.19/1.37 fof(f3241,plain,(
% 5.19/1.37 ~l1_lattices(sK6_skl)|sQ333_spl),
% 5.19/1.37 inference(component_clause,[status(thm)],[f3239])).
% 5.19/1.37 fof(f3321,plain,(
% 5.19/1.37 $false|sQ333_spl),
% 5.19/1.37 inference(forward_subsumption_resolution,[status(thm)],[f3241,f605])).
% 5.19/1.37 fof(f3322,plain,(
% 5.19/1.37 sQ333_spl),
% 5.19/1.37 inference(contradiction_clause,[status(thm)],[f3321])).
% 5.19/1.37 fof(f3893,plain,(
% 5.19/1.37 $false|sQ92_spl),
% 5.19/1.37 inference(forward_subsumption_resolution,[status(thm)],[f1007,f177])).
% 5.19/1.37 fof(f3894,plain,(
% 5.19/1.37 sQ92_spl),
% 5.19/1.37 inference(contradiction_clause,[status(thm)],[f3893])).
% 5.19/1.37 fof(f4459,plain,(
% 5.19/1.37 ~m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))|r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK1_skl),a_2_0_filter_2(sK0_skl,sK1_skl))|~m1_subset_1(k4_lattices(sK0_skl,sK2_skl,sK1_skl),u1_struct_0(sK0_skl))|~sQ331_spl|~sQ131_spl),
% 5.19/1.37 inference(resolution,[status(thm)],[f3189,f1315])).
% 5.19/1.37 fof(f4461,definition,(
% 5.19/1.37 sQ430_spl <=> (r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK1_skl),a_2_0_filter_2(sK0_skl,sK1_skl)))),
% 5.19/1.37 introduced(definition,[new_symbols(definition,[sQ430_spl])],[split_symbol_definition])).
% 5.19/1.37 fof(f4462,plain,(
% 5.19/1.37 r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK1_skl),a_2_0_filter_2(sK0_skl,sK1_skl))|~sQ430_spl),
% 5.19/1.37 inference(component_clause,[status(thm)],[f4461])).
% 5.19/1.37 fof(f4464,plain,(
% 5.19/1.37 ~sQ84_spl|sQ430_spl|~sQ86_spl|~sQ331_spl|~sQ131_spl),
% 5.19/1.37 inference(split_clause,[status(thm)],[f4459,f848,f4461,f854,f3188,f1314])).
% 5.19/1.37 fof(f4465,plain,(
% 5.19/1.37 r2_hidden(k4_lattices(sK0_skl,sK2_skl,sK1_skl),k18_filter_2(sK0_skl,sK1_skl))|~sQ8_spl|~sQ430_spl),
% 5.19/1.37 inference(forward_demodulation,[status(thm)],[f405,f4462])).
% 5.19/1.37 fof(f4466,plain,(
% 5.19/1.37 $false|sQ2_spl|~sQ8_spl|~sQ430_spl),
% 5.19/1.37 inference(forward_subsumption_resolution,[status(thm)],[f4465,f299])).
% 5.19/1.37 fof(f4467,plain,(
% 5.19/1.37 sQ2_spl|~sQ8_spl|~sQ430_spl),
% 5.19/1.37 inference(contradiction_clause,[status(thm)],[f4466])).
% 5.19/1.37 fof(f5052,plain,(
% 5.19/1.37 ~m1_subset_1(sK1_skl,u1_struct_0(sK0_skl))|r2_hidden(sK1_skl,k18_filter_2(sK0_skl,sK1_skl))|~sQ236_spl|~sQ131_spl|~sQ8_spl),
% 5.19/1.37 inference(paramodulation,[status(thm)],[f405,f2051])).
% 5.19/1.37 fof(f5069,plain,(
% 5.19/1.37 ~sQ84_spl|sQ0_spl|~sQ236_spl|~sQ131_spl|~sQ8_spl),
% 5.19/1.37 inference(split_clause,[status(thm)],[f5052,f848,f291,f2039,f1314,f324])).
% 5.19/1.37 fof(f5070,plain,(
% 5.19/1.37 ~sQ2_spl|~sQ63_spl|sQ1_spl),
% 5.19/1.37 inference(split_clause,[status(thm)],[f1697,f297,f645,f294])).
% 5.19/1.37 fof(f5071,plain,(
% 5.19/1.37 $false),
% 5.19/1.37 inference(sat_refutation,[status(thm)],[f300,f327,f329,f331,f366,f382,f392,f400,f443,f573,f608,f648,f857,f859,f861,f1062,f1067,f1104,f1147,f1317,f1712,f1857,f2042,f2047,f2317,f2550,f2552,f2652,f3019,f3191,f3210,f3322,f3894,f4464,f4467,f5069,f5070])).
% 5.19/1.37 % SZS output end CNFRefutation for theBenchmark.p
% 5.19/1.40 % Elapsed time: 0.926131 seconds
% 5.19/1.40 % CPU time: 6.666681 seconds
% 5.19/1.40 % Total memory used: 184.260 MB
% 5.19/1.40 % Net memory used: 181.389 MB
%------------------------------------------------------------------------------