%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT297+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:34 PM UTC 2026
% Result : Theorem 11.20s 2.26s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT297+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n011.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 23:29:25 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 11.20/2.26 % Refutation found
% 11.20/2.26 % SZS status Theorem for theBenchmark: Theorem is valid
% 11.20/2.26 % SZS output start CNFRefutation for theBenchmark
% 11.20/2.26 fof(f1,conjecture,(
% 11.20/2.26 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))=> ( (! [C] :( m1_subset_1(C,u1_struct_0(A))=> (! [D] :( m1_subset_1(D,u1_struct_0(A))=> ( ( r2_hidden(C,B)& r2_hidden(D,B) )<=> r2_hidden(k4_lattices(A,C,D),B) ) ) )))=> m2_lattice4(B,A) ) ) )) )),
% 11.20/2.26 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.20/2.26 fof(f2,negated_conjecture,(
% 11.20/2.26 ~((! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))=> ( (! [C] :( m1_subset_1(C,u1_struct_0(A))=> (! [D] :( m1_subset_1(D,u1_struct_0(A))=> ( ( r2_hidden(C,B)& r2_hidden(D,B) )<=> r2_hidden(k4_lattices(A,C,D),B) ) ) )))=> m2_lattice4(B,A) ) ) )) ))),
% 11.20/2.26 inference(negated_conjecture,[status(cth)],[f1])).
% 11.20/2.26 fof(f5,axiom,(
% 11.20/2.26 (! [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) ) ) ) )),
% 11.20/2.26 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.20/2.26 fof(f11,axiom,(
% 11.20/2.26 (! [A,B,C] :( ( ~ v3_struct_0(A)& v4_lattices(A)& l2_lattices(A)& m1_subset_1(B,u1_struct_0(A))& m1_subset_1(C,u1_struct_0(A)) )=> k3_lattices(A,B,C) = k3_lattices(A,C,B) ) )),
% 11.20/2.26 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.20/2.26 fof(f12,axiom,(
% 11.20/2.26 (! [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) ) )),
% 11.20/2.26 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.20/2.26 fof(f13,axiom,(
% 11.20/2.26 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))=> ( m2_lattice4(B,A)<=> (! [C] :( m1_subset_1(C,u1_struct_0(A))=> (! [D] :( m1_subset_1(D,u1_struct_0(A))=> ( ( r2_hidden(C,B)& r2_hidden(D,B) )=> ( r2_hidden(k4_lattices(A,C,D),B)& r2_hidden(k3_lattices(A,C,D),B) ) ) ) )) )) ) )) )),
% 11.20/2.26 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.20/2.26 fof(f18,axiom,(
% 11.20/2.26 (! [A] :( ( ~ v3_struct_0(A)& l3_lattices(A) )=> ( v9_lattices(A)<=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> (! [C] :( m1_subset_1(C,u1_struct_0(A))=> k2_lattices(A,B,k1_lattices(A,B,C)) = B ) )) )) ) )),
% 11.20/2.26 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.20/2.26 fof(f29,axiom,(
% 11.20/2.26 (! [A,B,C] :( ( ~ v3_struct_0(A)& v4_lattices(A)& l2_lattices(A)& m1_subset_1(B,u1_struct_0(A))& m1_subset_1(C,u1_struct_0(A)) )=> m1_subset_1(k3_lattices(A,B,C),u1_struct_0(A)) ) )),
% 11.20/2.26 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.20/2.26 fof(f35,axiom,(
% 11.20/2.26 (! [A] :( l3_lattices(A)=> ( l1_lattices(A)& l2_lattices(A) ) ) )),
% 11.20/2.26 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.20/2.26 fof(f75,axiom,(
% 11.20/2.26 (! [A,B,C] :( ( ~ v3_struct_0(A)& v4_lattices(A)& l2_lattices(A)& m1_subset_1(B,u1_struct_0(A))& m1_subset_1(C,u1_struct_0(A)) )=> k3_lattices(A,B,C) = k1_lattices(A,B,C) ) )),
% 11.20/2.26 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.20/2.26 fof(f76,axiom,(
% 11.20/2.26 (! [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) = k2_lattices(A,B,C) ) )),
% 11.20/2.26 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 11.20/2.26 fof(f87,plain,(
% 11.20/2.26 (?[A]: (((~v3_struct_0(A)&v10_lattices(A))&l3_lattices(A))&(?[B]: (m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))&((![C]: (~m1_subset_1(C,u1_struct_0(A))|(![D]: (~m1_subset_1(D,u1_struct_0(A))|((r2_hidden(C,B)&r2_hidden(D,B))<=>r2_hidden(k4_lattices(A,C,D),B))))))&~m2_lattice4(B,A))))))),
% 11.20/2.26 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 11.20/2.26 fof(f88,plain,(
% 11.20/2.26 ?[A]: (((~v3_struct_0(A)&v10_lattices(A))&l3_lattices(A))&(?[B]: (m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))&((![C]: (~m1_subset_1(C,u1_struct_0(A))|(![D]: (~m1_subset_1(D,u1_struct_0(A))|(((~r2_hidden(C,B)|~r2_hidden(D,B))|r2_hidden(k4_lattices(A,C,D),B))&((r2_hidden(C,B)&r2_hidden(D,B))|~r2_hidden(k4_lattices(A,C,D),B)))))))&~m2_lattice4(B,A)))))),
% 11.20/2.26 inference(NNF_transformation,[status(thm)],[f87])).
% 11.20/2.26 fof(f89,plain,(
% 11.20/2.26 (((~v3_struct_0(sK0_skl)&v10_lattices(sK0_skl))&l3_lattices(sK0_skl))&(m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))&((![C]: (~m1_subset_1(C,u1_struct_0(sK0_skl))|(![D]: (~m1_subset_1(D,u1_struct_0(sK0_skl))|(((~r2_hidden(C,sK1_skl)|~r2_hidden(D,sK1_skl))|r2_hidden(k4_lattices(sK0_skl,C,D),sK1_skl))&((r2_hidden(C,sK1_skl)&r2_hidden(D,sK1_skl))|~r2_hidden(k4_lattices(sK0_skl,C,D),sK1_skl)))))))&~m2_lattice4(sK1_skl,sK0_skl))))),
% 11.20/2.26 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl)],[f88])).
% 11.20/2.26 fof(f90,plain,(
% 11.20/2.26 ~v3_struct_0(sK0_skl)),
% 11.20/2.26 inference(cnf_transformation,[status(thm)],[f89])).
% 11.20/2.26 fof(f91,plain,(
% 11.20/2.26 v10_lattices(sK0_skl)),
% 11.20/2.26 inference(cnf_transformation,[status(thm)],[f89])).
% 11.20/2.26 fof(f92,plain,(
% 11.20/2.26 l3_lattices(sK0_skl)),
% 11.20/2.26 inference(cnf_transformation,[status(thm)],[f89])).
% 11.20/2.26 fof(f93,plain,(
% 11.20/2.26 m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 11.20/2.26 inference(cnf_transformation,[status(thm)],[f89])).
% 11.20/2.26 fof(f94,plain,(
% 11.20/2.26 ![X0,X1]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|~m1_subset_1(X1,u1_struct_0(sK0_skl))|~r2_hidden(X0,sK1_skl)|~r2_hidden(X1,sK1_skl)|r2_hidden(k4_lattices(sK0_skl,X0,X1),sK1_skl))),
% 11.20/2.26 inference(cnf_transformation,[status(thm)],[f89])).
% 11.20/2.26 fof(f95,plain,(
% 11.20/2.26 ![X0,X1]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|~m1_subset_1(X1,u1_struct_0(sK0_skl))|r2_hidden(X0,sK1_skl)|~r2_hidden(k4_lattices(sK0_skl,X0,X1),sK1_skl))),
% 11.20/2.26 inference(cnf_transformation,[status(thm)],[f89])).
% 11.20/2.26 fof(f97,plain,(
% 11.20/2.26 ~m2_lattice4(sK1_skl,sK0_skl)),
% 11.20/2.26 inference(cnf_transformation,[status(thm)],[f89])).
% 11.20/2.26 fof(f102,plain,(
% 11.20/2.26 ![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))))),
% 11.20/2.26 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 11.20/2.26 fof(f104,plain,(
% 11.20/2.26 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v10_lattices(X0)|v4_lattices(X0))),
% 11.20/2.26 inference(cnf_transformation,[status(thm)],[f102])).
% 11.20/2.26 fof(f106,plain,(
% 11.20/2.26 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v10_lattices(X0)|v6_lattices(X0))),
% 11.20/2.26 inference(cnf_transformation,[status(thm)],[f102])).
% 11.20/2.26 fof(f109,plain,(
% 11.20/2.26 ![X0]: (~l3_lattices(X0)|v3_struct_0(X0)|~v10_lattices(X0)|v9_lattices(X0))),
% 11.20/2.26 inference(cnf_transformation,[status(thm)],[f102])).
% 11.20/2.26 fof(f123,plain,(
% 11.20/2.26 ![A,B,C]: (((((v3_struct_0(A)|~v4_lattices(A))|~l2_lattices(A))|~m1_subset_1(B,u1_struct_0(A)))|~m1_subset_1(C,u1_struct_0(A)))|k3_lattices(A,B,C)=k3_lattices(A,C,B))),
% 11.20/2.26 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 11.20/2.26 fof(f124,plain,(
% 11.20/2.26 ![X0,X1,X2]: (v3_struct_0(X0)|~v4_lattices(X0)|~l2_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|k3_lattices(X0,X1,X2)=k3_lattices(X0,X2,X1))),
% 11.20/2.26 inference(cnf_transformation,[status(thm)],[f123])).
% 11.20/2.26 fof(f125,plain,(
% 11.20/2.26 ![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))),
% 11.20/2.26 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 11.20/2.26 fof(f126,plain,(
% 11.20/2.26 ![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))),
% 11.20/2.26 inference(cnf_transformation,[status(thm)],[f125])).
% 11.20/2.26 fof(f127,plain,(
% 11.20/2.26 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))|(m2_lattice4(B,A)<=>(![C]: (~m1_subset_1(C,u1_struct_0(A))|(![D]: (~m1_subset_1(D,u1_struct_0(A))|((~r2_hidden(C,B)|~r2_hidden(D,B))|(r2_hidden(k4_lattices(A,C,D),B)&r2_hidden(k3_lattices(A,C,D),B)))))))))))),
% 11.20/2.26 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 11.20/2.26 fof(f128,plain,(
% 11.20/2.26 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))|((~m2_lattice4(B,A)|(![C]: (~m1_subset_1(C,u1_struct_0(A))|(![D]: (~m1_subset_1(D,u1_struct_0(A))|((~r2_hidden(C,B)|~r2_hidden(D,B))|(r2_hidden(k4_lattices(A,C,D),B)&r2_hidden(k3_lattices(A,C,D),B))))))))&(m2_lattice4(B,A)|(?[C]: (m1_subset_1(C,u1_struct_0(A))&(?[D]: (m1_subset_1(D,u1_struct_0(A))&((r2_hidden(C,B)&r2_hidden(D,B))&(~r2_hidden(k4_lattices(A,C,D),B)|~r2_hidden(k3_lattices(A,C,D),B))))))))))))),
% 11.20/2.26 inference(NNF_transformation,[status(thm)],[f127])).
% 11.20/2.26 fof(f129,plain,(
% 11.20/2.26 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))|((~m2_lattice4(B,A)|(![C]: (~m1_subset_1(C,u1_struct_0(A))|(![D]: (~m1_subset_1(D,u1_struct_0(A))|((~r2_hidden(C,B)|~r2_hidden(D,B))|(r2_hidden(k4_lattices(A,C,D),B)&r2_hidden(k3_lattices(A,C,D),B))))))))&(m2_lattice4(B,A)|(m1_subset_1(sK2_skl(B,A),u1_struct_0(A))&(m1_subset_1(sK3_skl(B,A),u1_struct_0(A))&((r2_hidden(sK2_skl(B,A),B)&r2_hidden(sK3_skl(B,A),B))&(~r2_hidden(k4_lattices(A,sK2_skl(B,A),sK3_skl(B,A)),B)|~r2_hidden(k3_lattices(A,sK2_skl(B,A),sK3_skl(B,A)),B))))))))))),
% 11.20/2.26 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(C,sK2_skl(B,A)),skolemize(D,sK3_skl(B,A))],[f128])).
% 11.20/2.26 fof(f132,plain,(
% 11.20/2.26 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|m2_lattice4(X1,X0)|m1_subset_1(sK2_skl(X1,X0),u1_struct_0(X0)))),
% 11.20/2.26 inference(cnf_transformation,[status(thm)],[f129])).
% 11.20/2.26 fof(f133,plain,(
% 11.20/2.26 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|m2_lattice4(X1,X0)|m1_subset_1(sK3_skl(X1,X0),u1_struct_0(X0)))),
% 11.20/2.26 inference(cnf_transformation,[status(thm)],[f129])).
% 11.20/2.26 fof(f134,plain,(
% 11.20/2.26 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|m2_lattice4(X1,X0)|r2_hidden(sK2_skl(X1,X0),X1))),
% 11.20/2.26 inference(cnf_transformation,[status(thm)],[f129])).
% 11.20/2.26 fof(f135,plain,(
% 11.20/2.26 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|m2_lattice4(X1,X0)|r2_hidden(sK3_skl(X1,X0),X1))),
% 11.20/2.26 inference(cnf_transformation,[status(thm)],[f129])).
% 11.20/2.26 fof(f136,plain,(
% 11.20/2.26 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|m2_lattice4(X1,X0)|~r2_hidden(k4_lattices(X0,sK2_skl(X1,X0),sK3_skl(X1,X0)),X1)|~r2_hidden(k3_lattices(X0,sK2_skl(X1,X0),sK3_skl(X1,X0)),X1))),
% 11.20/2.26 inference(cnf_transformation,[status(thm)],[f129])).
% 11.20/2.26 fof(f144,plain,(
% 11.20/2.26 ![A]: ((v3_struct_0(A)|~l3_lattices(A))|(v9_lattices(A)<=>(![B]: (~m1_subset_1(B,u1_struct_0(A))|(![C]: (~m1_subset_1(C,u1_struct_0(A))|k2_lattices(A,B,k1_lattices(A,B,C))=B))))))),
% 11.20/2.26 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 11.20/2.26 fof(f145,plain,(
% 11.20/2.26 ![A]: ((v3_struct_0(A)|~l3_lattices(A))|((~v9_lattices(A)|(![B]: (~m1_subset_1(B,u1_struct_0(A))|(![C]: (~m1_subset_1(C,u1_struct_0(A))|k2_lattices(A,B,k1_lattices(A,B,C))=B)))))&(v9_lattices(A)|(?[B]: (m1_subset_1(B,u1_struct_0(A))&(?[C]: (m1_subset_1(C,u1_struct_0(A))&~k2_lattices(A,B,k1_lattices(A,B,C))=B)))))))),
% 11.20/2.26 inference(NNF_transformation,[status(thm)],[f144])).
% 11.20/2.26 fof(f146,plain,(
% 11.20/2.26 ![A]: ((v3_struct_0(A)|~l3_lattices(A))|((~v9_lattices(A)|(![B]: (~m1_subset_1(B,u1_struct_0(A))|(![C]: (~m1_subset_1(C,u1_struct_0(A))|k2_lattices(A,B,k1_lattices(A,B,C))=B)))))&(v9_lattices(A)|(m1_subset_1(sK4_skl(A),u1_struct_0(A))&(m1_subset_1(sK5_skl(A),u1_struct_0(A))&~k2_lattices(A,sK4_skl(A),k1_lattices(A,sK4_skl(A),sK5_skl(A)))=sK4_skl(A))))))),
% 11.20/2.26 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl]),skolemize(B,sK4_skl(A)),skolemize(C,sK5_skl(A))],[f145])).
% 11.20/2.26 fof(f147,plain,(
% 11.20/2.26 ![X0,X1,X2]: (v3_struct_0(X0)|~l3_lattices(X0)|~v9_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|k2_lattices(X0,X1,k1_lattices(X0,X1,X2))=X1)),
% 11.20/2.26 inference(cnf_transformation,[status(thm)],[f146])).
% 11.20/2.26 fof(f157,plain,(
% 11.20/2.26 ![A,B,C]: (((((v3_struct_0(A)|~v4_lattices(A))|~l2_lattices(A))|~m1_subset_1(B,u1_struct_0(A)))|~m1_subset_1(C,u1_struct_0(A)))|m1_subset_1(k3_lattices(A,B,C),u1_struct_0(A)))),
% 11.20/2.26 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 11.20/2.26 fof(f158,plain,(
% 11.20/2.26 ![X0,X1,X2]: (v3_struct_0(X0)|~v4_lattices(X0)|~l2_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|m1_subset_1(k3_lattices(X0,X1,X2),u1_struct_0(X0)))),
% 11.20/2.26 inference(cnf_transformation,[status(thm)],[f157])).
% 11.20/2.26 fof(f165,plain,(
% 11.20/2.26 ![A]: (~l3_lattices(A)|(l1_lattices(A)&l2_lattices(A)))),
% 11.20/2.26 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 11.20/2.26 fof(f166,plain,(
% 11.20/2.26 ![X0]: (~l3_lattices(X0)|l1_lattices(X0))),
% 11.20/2.26 inference(cnf_transformation,[status(thm)],[f165])).
% 11.20/2.26 fof(f167,plain,(
% 11.20/2.26 ![X0]: (~l3_lattices(X0)|l2_lattices(X0))),
% 11.20/2.26 inference(cnf_transformation,[status(thm)],[f165])).
% 11.20/2.26 fof(f274,plain,(
% 11.20/2.26 ![A,B,C]: (((((v3_struct_0(A)|~v4_lattices(A))|~l2_lattices(A))|~m1_subset_1(B,u1_struct_0(A)))|~m1_subset_1(C,u1_struct_0(A)))|k3_lattices(A,B,C)=k1_lattices(A,B,C))),
% 11.20/2.26 inference(pre_NNF_transformation,[status(thm)],[f75])).
% 11.20/2.26 fof(f275,plain,(
% 11.20/2.26 ![X0,X1,X2]: (v3_struct_0(X0)|~v4_lattices(X0)|~l2_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|k3_lattices(X0,X1,X2)=k1_lattices(X0,X1,X2))),
% 11.20/2.26 inference(cnf_transformation,[status(thm)],[f274])).
% 11.20/2.26 fof(f276,plain,(
% 11.20/2.26 ![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)=k2_lattices(A,B,C))),
% 11.20/2.26 inference(pre_NNF_transformation,[status(thm)],[f76])).
% 11.20/2.26 fof(f277,plain,(
% 11.20/2.26 ![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)=k2_lattices(X0,X1,X2))),
% 11.20/2.26 inference(cnf_transformation,[status(thm)],[f276])).
% 11.20/2.26 fof(f320,plain,(
% 11.20/2.26 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|v4_lattices(sK0_skl)),
% 11.20/2.26 inference(resolution,[status(thm)],[f104,f92])).
% 11.20/2.26 fof(f321,definition,(
% 11.20/2.26 sQ2_spl <=> (v3_struct_0(sK0_skl))),
% 11.20/2.26 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 11.20/2.26 fof(f322,plain,(
% 11.20/2.26 v3_struct_0(sK0_skl)|~sQ2_spl),
% 11.20/2.26 inference(component_clause,[status(thm)],[f321])).
% 11.20/2.26 fof(f324,definition,(
% 11.20/2.26 sQ3_spl <=> (v10_lattices(sK0_skl))),
% 11.20/2.26 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 11.20/2.26 fof(f326,plain,(
% 11.20/2.26 ~v10_lattices(sK0_skl)|sQ3_spl),
% 11.20/2.26 inference(component_clause,[status(thm)],[f324])).
% 11.20/2.26 fof(f327,definition,(
% 11.20/2.26 sQ4_spl <=> (v4_lattices(sK0_skl))),
% 11.20/2.26 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 11.20/2.26 fof(f330,plain,(
% 11.20/2.26 sQ2_spl|~sQ3_spl|sQ4_spl),
% 11.20/2.26 inference(split_clause,[status(thm)],[f320,f321,f324,f327])).
% 11.20/2.26 fof(f336,plain,(
% 11.20/2.26 $false|sQ3_spl),
% 11.20/2.26 inference(forward_subsumption_resolution,[status(thm)],[f326,f91])).
% 11.20/2.26 fof(f337,plain,(
% 11.20/2.26 sQ3_spl),
% 11.20/2.26 inference(contradiction_clause,[status(thm)],[f336])).
% 11.20/2.26 fof(f338,plain,(
% 11.20/2.26 $false|~sQ2_spl),
% 11.20/2.26 inference(forward_subsumption_resolution,[status(thm)],[f322,f90])).
% 11.20/2.26 fof(f339,plain,(
% 11.20/2.26 ~sQ2_spl),
% 11.20/2.26 inference(contradiction_clause,[status(thm)],[f338])).
% 11.20/2.26 fof(f342,plain,(
% 11.20/2.26 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|v6_lattices(sK0_skl)),
% 11.20/2.26 inference(resolution,[status(thm)],[f106,f92])).
% 11.20/2.26 fof(f343,definition,(
% 11.20/2.26 sQ6_spl <=> (v6_lattices(sK0_skl))),
% 11.20/2.26 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 11.20/2.26 fof(f346,plain,(
% 11.20/2.26 sQ2_spl|~sQ3_spl|sQ6_spl),
% 11.20/2.26 inference(split_clause,[status(thm)],[f342,f321,f324,f343])).
% 11.20/2.26 fof(f357,plain,(
% 11.20/2.26 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|v9_lattices(sK0_skl)),
% 11.20/2.26 inference(resolution,[status(thm)],[f109,f92])).
% 11.20/2.26 fof(f358,definition,(
% 11.20/2.26 sQ9_spl <=> (v9_lattices(sK0_skl))),
% 11.20/2.26 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 11.20/2.26 fof(f361,plain,(
% 11.20/2.26 sQ2_spl|~sQ3_spl|sQ9_spl),
% 11.20/2.26 inference(split_clause,[status(thm)],[f357,f321,f324,f358])).
% 11.20/2.26 fof(f374,plain,(
% 11.20/2.26 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m2_lattice4(sK1_skl,sK0_skl)|m1_subset_1(sK2_skl(sK1_skl,sK0_skl),u1_struct_0(sK0_skl))),
% 11.20/2.26 inference(resolution,[status(thm)],[f132,f93])).
% 11.20/2.26 fof(f375,definition,(
% 11.20/2.26 sQ13_spl <=> (l3_lattices(sK0_skl))),
% 11.20/2.26 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 11.20/2.26 fof(f377,plain,(
% 11.20/2.26 ~l3_lattices(sK0_skl)|sQ13_spl),
% 11.20/2.26 inference(component_clause,[status(thm)],[f375])).
% 11.20/2.26 fof(f378,definition,(
% 11.20/2.26 sQ14_spl <=> (m2_lattice4(sK1_skl,sK0_skl))),
% 11.20/2.26 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 11.20/2.26 fof(f379,plain,(
% 11.20/2.26 m2_lattice4(sK1_skl,sK0_skl)|~sQ14_spl),
% 11.20/2.26 inference(component_clause,[status(thm)],[f378])).
% 11.20/2.26 fof(f381,definition,(
% 11.20/2.26 sQ15_spl <=> (m1_subset_1(sK2_skl(sK1_skl,sK0_skl),u1_struct_0(sK0_skl)))),
% 11.20/2.26 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 11.20/2.26 fof(f382,plain,(
% 11.20/2.26 m1_subset_1(sK2_skl(sK1_skl,sK0_skl),u1_struct_0(sK0_skl))|~sQ15_spl),
% 11.20/2.26 inference(component_clause,[status(thm)],[f381])).
% 11.20/2.26 fof(f384,plain,(
% 11.20/2.26 sQ2_spl|~sQ3_spl|~sQ13_spl|sQ14_spl|sQ15_spl),
% 11.20/2.26 inference(split_clause,[status(thm)],[f374,f321,f324,f375,f378,f381])).
% 11.20/2.26 fof(f385,plain,(
% 11.20/2.26 $false|~sQ14_spl),
% 11.20/2.26 inference(forward_subsumption_resolution,[status(thm)],[f379,f97])).
% 11.20/2.26 fof(f386,plain,(
% 11.20/2.26 ~sQ14_spl),
% 11.20/2.26 inference(contradiction_clause,[status(thm)],[f385])).
% 11.20/2.26 fof(f387,plain,(
% 11.20/2.26 $false|sQ13_spl),
% 11.20/2.26 inference(forward_subsumption_resolution,[status(thm)],[f377,f92])).
% 11.20/2.26 fof(f388,plain,(
% 11.20/2.26 sQ13_spl),
% 11.20/2.26 inference(contradiction_clause,[status(thm)],[f387])).
% 11.20/2.26 fof(f390,plain,(
% 11.20/2.26 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m2_lattice4(sK1_skl,sK0_skl)|m1_subset_1(sK3_skl(sK1_skl,sK0_skl),u1_struct_0(sK0_skl))),
% 11.20/2.26 inference(resolution,[status(thm)],[f133,f93])).
% 11.20/2.26 fof(f391,definition,(
% 11.20/2.26 sQ16_spl <=> (m1_subset_1(sK3_skl(sK1_skl,sK0_skl),u1_struct_0(sK0_skl)))),
% 11.20/2.26 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 11.20/2.26 fof(f392,plain,(
% 11.20/2.26 m1_subset_1(sK3_skl(sK1_skl,sK0_skl),u1_struct_0(sK0_skl))|~sQ16_spl),
% 11.20/2.26 inference(component_clause,[status(thm)],[f391])).
% 11.20/2.26 fof(f394,plain,(
% 11.20/2.26 sQ2_spl|~sQ3_spl|~sQ13_spl|sQ14_spl|sQ16_spl),
% 11.20/2.26 inference(split_clause,[status(thm)],[f390,f321,f324,f375,f378,f391])).
% 11.20/2.26 fof(f396,plain,(
% 11.20/2.26 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m2_lattice4(sK1_skl,sK0_skl)|r2_hidden(sK2_skl(sK1_skl,sK0_skl),sK1_skl)),
% 11.20/2.26 inference(resolution,[status(thm)],[f134,f93])).
% 11.20/2.26 fof(f397,definition,(
% 11.20/2.26 sQ17_spl <=> (r2_hidden(sK2_skl(sK1_skl,sK0_skl),sK1_skl))),
% 11.20/2.26 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 11.20/2.26 fof(f400,plain,(
% 11.20/2.26 sQ2_spl|~sQ3_spl|~sQ13_spl|sQ14_spl|sQ17_spl),
% 11.20/2.26 inference(split_clause,[status(thm)],[f396,f321,f324,f375,f378,f397])).
% 11.20/2.26 fof(f402,plain,(
% 11.20/2.26 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m2_lattice4(sK1_skl,sK0_skl)|r2_hidden(sK3_skl(sK1_skl,sK0_skl),sK1_skl)),
% 11.20/2.26 inference(resolution,[status(thm)],[f135,f93])).
% 11.20/2.26 fof(f403,definition,(
% 11.20/2.26 sQ18_spl <=> (r2_hidden(sK3_skl(sK1_skl,sK0_skl),sK1_skl))),
% 11.20/2.26 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 11.20/2.26 fof(f404,plain,(
% 11.20/2.26 r2_hidden(sK3_skl(sK1_skl,sK0_skl),sK1_skl)|~sQ18_spl),
% 11.20/2.26 inference(component_clause,[status(thm)],[f403])).
% 11.20/2.26 fof(f406,plain,(
% 11.20/2.26 sQ2_spl|~sQ3_spl|~sQ13_spl|sQ14_spl|sQ18_spl),
% 11.20/2.26 inference(split_clause,[status(thm)],[f402,f321,f324,f375,f378,f403])).
% 11.20/2.26 fof(f651,plain,(
% 11.20/2.26 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|~r2_hidden(sK2_skl(sK1_skl,sK0_skl),sK1_skl)|~r2_hidden(X0,sK1_skl)|r2_hidden(k4_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),X0),sK1_skl)|~sQ15_spl)),
% 11.20/2.26 inference(resolution,[status(thm)],[f382,f94])).
% 11.20/2.26 fof(f653,plain,(
% 11.20/2.26 ![X0]: (v3_struct_0(sK0_skl)|~v4_lattices(sK0_skl)|~l2_lattices(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|k3_lattices(sK0_skl,X0,sK2_skl(sK1_skl,sK0_skl))=k1_lattices(sK0_skl,X0,sK2_skl(sK1_skl,sK0_skl))|~sQ15_spl)),
% 11.20/2.26 inference(resolution,[status(thm)],[f382,f275])).
% 11.20/2.26 fof(f654,plain,(
% 11.20/2.26 ![X0]: (v3_struct_0(sK0_skl)|~v4_lattices(sK0_skl)|~l2_lattices(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|m1_subset_1(k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),X0),u1_struct_0(sK0_skl))|~sQ15_spl)),
% 11.20/2.26 inference(resolution,[status(thm)],[f382,f158])).
% 11.20/2.26 fof(f657,plain,(
% 11.20/2.26 ![X0]: (v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|~v9_lattices(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|k2_lattices(sK0_skl,X0,k1_lattices(sK0_skl,X0,sK2_skl(sK1_skl,sK0_skl)))=X0|~sQ15_spl)),
% 11.20/2.26 inference(resolution,[status(thm)],[f382,f147])).
% 11.20/2.26 fof(f660,plain,(
% 11.20/2.26 ![X0]: (v3_struct_0(sK0_skl)|~v4_lattices(sK0_skl)|~l2_lattices(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|k3_lattices(sK0_skl,X0,sK2_skl(sK1_skl,sK0_skl))=k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),X0)|~sQ15_spl)),
% 11.20/2.26 inference(resolution,[status(thm)],[f382,f124])).
% 11.20/2.26 fof(f664,definition,(
% 11.20/2.26 ![X0]: (sQ66_spl <=> (~m1_subset_1(X0,u1_struct_0(sK0_skl))|~r2_hidden(X0,sK1_skl)|r2_hidden(k4_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),X0),sK1_skl)))),
% 11.20/2.26 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 11.20/2.26 fof(f665,plain,(
% 11.20/2.26 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|~r2_hidden(X0,sK1_skl)|r2_hidden(k4_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),X0),sK1_skl)|~sQ66_spl)),
% 11.20/2.26 inference(component_clause,[status(thm)],[f664])).
% 11.20/2.26 fof(f667,plain,(
% 11.20/2.26 sQ66_spl|~sQ17_spl|~sQ15_spl),
% 11.20/2.26 inference(split_clause,[status(thm)],[f651,f664,f397,f381])).
% 11.20/2.26 fof(f668,definition,(
% 11.20/2.26 sQ67_spl <=> (l1_lattices(sK0_skl))),
% 11.20/2.26 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 11.20/2.26 fof(f670,plain,(
% 11.20/2.26 ~l1_lattices(sK0_skl)|sQ67_spl),
% 11.20/2.26 inference(component_clause,[status(thm)],[f668])).
% 11.20/2.26 fof(f675,definition,(
% 11.20/2.26 sQ69_spl <=> (l2_lattices(sK0_skl))),
% 11.20/2.26 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 11.20/2.26 fof(f677,plain,(
% 11.20/2.26 ~l2_lattices(sK0_skl)|sQ69_spl),
% 11.20/2.26 inference(component_clause,[status(thm)],[f675])).
% 11.20/2.26 fof(f678,definition,(
% 11.20/2.26 ![X0]: (sQ70_spl <=> (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k3_lattices(sK0_skl,X0,sK2_skl(sK1_skl,sK0_skl))=k1_lattices(sK0_skl,X0,sK2_skl(sK1_skl,sK0_skl))))),
% 11.20/2.26 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 11.20/2.26 fof(f679,plain,(
% 11.20/2.26 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k3_lattices(sK0_skl,X0,sK2_skl(sK1_skl,sK0_skl))=k1_lattices(sK0_skl,X0,sK2_skl(sK1_skl,sK0_skl))|~sQ70_spl)),
% 11.20/2.26 inference(component_clause,[status(thm)],[f678])).
% 11.20/2.26 fof(f681,plain,(
% 11.20/2.26 sQ2_spl|~sQ4_spl|~sQ69_spl|sQ70_spl|~sQ15_spl),
% 11.20/2.26 inference(split_clause,[status(thm)],[f653,f321,f327,f675,f678,f381])).
% 11.20/2.26 fof(f682,definition,(
% 11.20/2.26 ![X0]: (sQ71_spl <=> (~m1_subset_1(X0,u1_struct_0(sK0_skl))|m1_subset_1(k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),X0),u1_struct_0(sK0_skl))))),
% 11.20/2.26 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 11.20/2.26 fof(f683,plain,(
% 11.20/2.26 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|m1_subset_1(k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),X0),u1_struct_0(sK0_skl))|~sQ71_spl)),
% 11.20/2.26 inference(component_clause,[status(thm)],[f682])).
% 11.20/2.26 fof(f685,plain,(
% 11.20/2.26 sQ2_spl|~sQ4_spl|~sQ69_spl|sQ71_spl|~sQ15_spl),
% 11.20/2.26 inference(split_clause,[status(thm)],[f654,f321,f327,f675,f682,f381])).
% 11.20/2.26 fof(f694,definition,(
% 11.20/2.26 ![X0]: (sQ74_spl <=> (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k2_lattices(sK0_skl,X0,k1_lattices(sK0_skl,X0,sK2_skl(sK1_skl,sK0_skl)))=X0))),
% 11.20/2.26 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 11.20/2.26 fof(f695,plain,(
% 11.20/2.26 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k2_lattices(sK0_skl,X0,k1_lattices(sK0_skl,X0,sK2_skl(sK1_skl,sK0_skl)))=X0|~sQ74_spl)),
% 11.20/2.26 inference(component_clause,[status(thm)],[f694])).
% 11.20/2.26 fof(f697,plain,(
% 11.20/2.26 sQ2_spl|~sQ13_spl|~sQ9_spl|sQ74_spl|~sQ15_spl),
% 11.20/2.26 inference(split_clause,[status(thm)],[f657,f321,f375,f358,f694,f381])).
% 11.20/2.26 fof(f706,definition,(
% 11.20/2.26 ![X0]: (sQ77_spl <=> (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k3_lattices(sK0_skl,X0,sK2_skl(sK1_skl,sK0_skl))=k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),X0)))),
% 11.20/2.26 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 11.20/2.26 fof(f707,plain,(
% 11.20/2.26 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k3_lattices(sK0_skl,X0,sK2_skl(sK1_skl,sK0_skl))=k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),X0)|~sQ77_spl)),
% 11.20/2.26 inference(component_clause,[status(thm)],[f706])).
% 11.20/2.26 fof(f709,plain,(
% 11.20/2.26 sQ2_spl|~sQ4_spl|~sQ69_spl|sQ77_spl|~sQ15_spl),
% 11.20/2.26 inference(split_clause,[status(thm)],[f660,f321,f327,f675,f706,f381])).
% 11.20/2.26 fof(f733,plain,(
% 11.20/2.26 ![X0]: (v3_struct_0(sK0_skl)|~v6_lattices(sK0_skl)|~l1_lattices(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|k4_lattices(sK0_skl,X0,sK3_skl(sK1_skl,sK0_skl))=k4_lattices(sK0_skl,sK3_skl(sK1_skl,sK0_skl),X0)|~sQ16_spl)),
% 14.12/2.27 inference(resolution,[status(thm)],[f392,f126])).
% 14.12/2.27 fof(f779,definition,(
% 14.12/2.27 ![X0]: (sQ92_spl <=> (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k4_lattices(sK0_skl,X0,sK3_skl(sK1_skl,sK0_skl))=k4_lattices(sK0_skl,sK3_skl(sK1_skl,sK0_skl),X0)))),
% 14.12/2.27 introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition])).
% 14.12/2.27 fof(f780,plain,(
% 14.12/2.27 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k4_lattices(sK0_skl,X0,sK3_skl(sK1_skl,sK0_skl))=k4_lattices(sK0_skl,sK3_skl(sK1_skl,sK0_skl),X0)|~sQ92_spl)),
% 14.12/2.27 inference(component_clause,[status(thm)],[f779])).
% 14.12/2.27 fof(f782,plain,(
% 14.12/2.27 sQ2_spl|~sQ6_spl|~sQ67_spl|sQ92_spl|~sQ16_spl),
% 14.12/2.27 inference(split_clause,[status(thm)],[f733,f321,f343,f668,f779,f391])).
% 14.12/2.27 fof(f850,plain,(
% 14.12/2.27 k2_lattices(sK0_skl,sK3_skl(sK1_skl,sK0_skl),k1_lattices(sK0_skl,sK3_skl(sK1_skl,sK0_skl),sK2_skl(sK1_skl,sK0_skl)))=sK3_skl(sK1_skl,sK0_skl)|~sQ74_spl|~sQ16_spl),
% 14.12/2.27 inference(resolution,[status(thm)],[f695,f392])).
% 14.12/2.27 fof(f852,plain,(
% 14.12/2.27 ~r2_hidden(sK3_skl(sK1_skl,sK0_skl),sK1_skl)|r2_hidden(k4_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl)),sK1_skl)|~sQ66_spl|~sQ16_spl),
% 14.12/2.27 inference(resolution,[status(thm)],[f665,f392])).
% 14.12/2.27 fof(f854,definition,(
% 14.12/2.27 sQ105_spl <=> (r2_hidden(k4_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl)),sK1_skl))),
% 14.12/2.27 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 14.12/2.27 fof(f857,plain,(
% 14.12/2.27 ~sQ18_spl|sQ105_spl|~sQ66_spl|~sQ16_spl),
% 14.12/2.27 inference(split_clause,[status(thm)],[f852,f403,f854,f664,f391])).
% 14.12/2.27 fof(f1948,plain,(
% 14.12/2.27 l1_lattices(sK0_skl)),
% 14.12/2.27 inference(resolution,[status(thm)],[f166,f92])).
% 14.12/2.27 fof(f1949,plain,(
% 14.12/2.27 $false|sQ67_spl),
% 14.12/2.27 inference(forward_subsumption_resolution,[status(thm)],[f1948,f670])).
% 14.12/2.27 fof(f1950,plain,(
% 14.12/2.27 sQ67_spl),
% 14.12/2.27 inference(contradiction_clause,[status(thm)],[f1949])).
% 14.12/2.27 fof(f1952,plain,(
% 14.12/2.27 l2_lattices(sK0_skl)),
% 14.12/2.27 inference(resolution,[status(thm)],[f167,f92])).
% 14.12/2.27 fof(f1953,plain,(
% 14.12/2.27 $false|sQ69_spl),
% 14.12/2.27 inference(forward_subsumption_resolution,[status(thm)],[f1952,f677])).
% 14.12/2.27 fof(f1954,plain,(
% 14.12/2.27 sQ69_spl),
% 14.12/2.27 inference(contradiction_clause,[status(thm)],[f1953])).
% 14.12/2.27 fof(f2447,plain,(
% 14.12/2.27 k3_lattices(sK0_skl,sK3_skl(sK1_skl,sK0_skl),sK2_skl(sK1_skl,sK0_skl))=k1_lattices(sK0_skl,sK3_skl(sK1_skl,sK0_skl),sK2_skl(sK1_skl,sK0_skl))|~sQ70_spl|~sQ16_spl),
% 14.12/2.27 inference(resolution,[status(thm)],[f679,f392])).
% 14.12/2.27 fof(f2452,plain,(
% 14.12/2.27 k2_lattices(sK0_skl,sK3_skl(sK1_skl,sK0_skl),k3_lattices(sK0_skl,sK3_skl(sK1_skl,sK0_skl),sK2_skl(sK1_skl,sK0_skl)))=sK3_skl(sK1_skl,sK0_skl)|~sQ70_spl|~sQ74_spl|~sQ16_spl),
% 14.12/2.27 inference(backward_demodulation,[status(thm)],[f2447,f850])).
% 14.12/2.27 fof(f2457,plain,(
% 14.12/2.27 m1_subset_1(k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl)),u1_struct_0(sK0_skl))|~sQ71_spl|~sQ16_spl),
% 14.12/2.27 inference(resolution,[status(thm)],[f683,f392])).
% 14.12/2.27 fof(f2512,plain,(
% 14.12/2.27 k4_lattices(sK0_skl,k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl)),sK3_skl(sK1_skl,sK0_skl))=k4_lattices(sK0_skl,sK3_skl(sK1_skl,sK0_skl),k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl)))|~sQ71_spl|~sQ16_spl|~sQ92_spl),
% 14.12/2.27 inference(resolution,[status(thm)],[f2457,f780])).
% 14.12/2.27 fof(f2527,plain,(
% 14.12/2.27 ![X0]: (v3_struct_0(sK0_skl)|~v6_lattices(sK0_skl)|~l1_lattices(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|k4_lattices(sK0_skl,X0,k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl)))=k2_lattices(sK0_skl,X0,k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl)))|~sQ71_spl|~sQ16_spl)),
% 14.12/2.27 inference(resolution,[status(thm)],[f2457,f277])).
% 14.12/2.27 fof(f2544,definition,(
% 14.12/2.27 ![X0]: (sQ212_spl <=> (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k4_lattices(sK0_skl,X0,k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl)))=k2_lattices(sK0_skl,X0,k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl)))))),
% 14.12/2.27 introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition])).
% 14.12/2.27 fof(f2545,plain,(
% 14.12/2.27 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k4_lattices(sK0_skl,X0,k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl)))=k2_lattices(sK0_skl,X0,k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl)))|~sQ212_spl)),
% 14.12/2.27 inference(component_clause,[status(thm)],[f2544])).
% 14.12/2.27 fof(f2547,plain,(
% 14.12/2.27 sQ2_spl|~sQ6_spl|~sQ67_spl|sQ212_spl|~sQ71_spl|~sQ16_spl),
% 14.12/2.27 inference(split_clause,[status(thm)],[f2527,f321,f343,f668,f2544,f682,f391])).
% 14.12/2.27 fof(f2708,plain,(
% 14.12/2.27 k3_lattices(sK0_skl,sK3_skl(sK1_skl,sK0_skl),sK2_skl(sK1_skl,sK0_skl))=k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl))|~sQ77_spl|~sQ16_spl),
% 14.12/2.27 inference(resolution,[status(thm)],[f707,f392])).
% 14.12/2.27 fof(f2726,plain,(
% 14.12/2.27 k2_lattices(sK0_skl,sK3_skl(sK1_skl,sK0_skl),k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl)))=sK3_skl(sK1_skl,sK0_skl)|~sQ77_spl|~sQ70_spl|~sQ74_spl|~sQ16_spl),
% 14.12/2.27 inference(backward_demodulation,[status(thm)],[f2708,f2452])).
% 14.12/2.27 fof(f4377,plain,(
% 14.12/2.27 ~m1_subset_1(k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl)),u1_struct_0(sK0_skl))|~m1_subset_1(sK3_skl(sK1_skl,sK0_skl),u1_struct_0(sK0_skl))|r2_hidden(k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl)),sK1_skl)|~r2_hidden(k4_lattices(sK0_skl,sK3_skl(sK1_skl,sK0_skl),k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl))),sK1_skl)|~sQ71_spl|~sQ16_spl|~sQ92_spl),
% 14.12/2.27 inference(paramodulation,[status(thm)],[f2512,f95])).
% 14.12/2.27 fof(f4378,definition,(
% 14.12/2.27 sQ436_spl <=> (m1_subset_1(k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl)),u1_struct_0(sK0_skl)))),
% 14.12/2.27 introduced(definition,[new_symbols(definition,[sQ436_spl])],[split_symbol_definition])).
% 14.12/2.27 fof(f4380,plain,(
% 14.12/2.27 ~m1_subset_1(k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl)),u1_struct_0(sK0_skl))|sQ436_spl),
% 14.12/2.27 inference(component_clause,[status(thm)],[f4378])).
% 14.12/2.27 fof(f4381,definition,(
% 14.12/2.27 sQ437_spl <=> (r2_hidden(k4_lattices(sK0_skl,sK3_skl(sK1_skl,sK0_skl),k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl))),sK1_skl))),
% 14.12/2.27 introduced(definition,[new_symbols(definition,[sQ437_spl])],[split_symbol_definition])).
% 14.12/2.27 fof(f4383,plain,(
% 14.12/2.27 ~r2_hidden(k4_lattices(sK0_skl,sK3_skl(sK1_skl,sK0_skl),k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl))),sK1_skl)|sQ437_spl),
% 14.12/2.27 inference(component_clause,[status(thm)],[f4381])).
% 14.12/2.27 fof(f4385,definition,(
% 14.12/2.27 sQ438_spl <=> (r2_hidden(k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl)),sK1_skl))),
% 14.12/2.27 introduced(definition,[new_symbols(definition,[sQ438_spl])],[split_symbol_definition])).
% 14.12/2.27 fof(f4386,plain,(
% 14.12/2.27 r2_hidden(k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl)),sK1_skl)|~sQ438_spl),
% 14.12/2.27 inference(component_clause,[status(thm)],[f4385])).
% 14.12/2.27 fof(f4388,plain,(
% 14.12/2.27 ~sQ436_spl|~sQ16_spl|sQ438_spl|~sQ437_spl|~sQ71_spl|~sQ92_spl),
% 14.12/2.27 inference(split_clause,[status(thm)],[f4377,f4378,f391,f4385,f4381,f682,f779])).
% 14.12/2.27 fof(f4493,plain,(
% 14.12/2.27 $false|~sQ71_spl|~sQ16_spl|sQ436_spl),
% 14.12/2.27 inference(forward_subsumption_resolution,[status(thm)],[f4380,f2457])).
% 14.12/2.27 fof(f4494,plain,(
% 14.12/2.27 ~sQ71_spl|~sQ16_spl|sQ436_spl),
% 14.12/2.27 inference(contradiction_clause,[status(thm)],[f4493])).
% 14.12/2.27 fof(f4590,plain,(
% 14.12/2.27 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))|m2_lattice4(sK1_skl,sK0_skl)|~r2_hidden(k4_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl)),sK1_skl)|~sQ438_spl),
% 14.12/2.27 inference(resolution,[status(thm)],[f4386,f136])).
% 14.12/2.27 fof(f4601,definition,(
% 14.12/2.27 sQ464_spl <=> (m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 14.12/2.27 introduced(definition,[new_symbols(definition,[sQ464_spl])],[split_symbol_definition])).
% 14.12/2.27 fof(f4603,plain,(
% 14.12/2.27 ~m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))|sQ464_spl),
% 14.12/2.27 inference(component_clause,[status(thm)],[f4601])).
% 14.12/2.27 fof(f4604,plain,(
% 14.12/2.27 sQ2_spl|~sQ3_spl|~sQ13_spl|~sQ464_spl|sQ14_spl|~sQ105_spl|~sQ438_spl),
% 14.12/2.27 inference(split_clause,[status(thm)],[f4590,f321,f324,f375,f4601,f378,f854,f4385])).
% 14.12/2.27 fof(f4605,plain,(
% 14.12/2.27 $false|sQ464_spl),
% 14.12/2.27 inference(forward_subsumption_resolution,[status(thm)],[f4603,f93])).
% 14.12/2.27 fof(f4606,plain,(
% 14.12/2.27 sQ464_spl),
% 14.12/2.27 inference(contradiction_clause,[status(thm)],[f4605])).
% 14.12/2.31 fof(f4630,plain,(
% 14.12/2.31 k4_lattices(sK0_skl,sK3_skl(sK1_skl,sK0_skl),k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl)))=k2_lattices(sK0_skl,sK3_skl(sK1_skl,sK0_skl),k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl)))|~sQ212_spl|~sQ16_spl),
% 14.12/2.31 inference(resolution,[status(thm)],[f2545,f392])).
% 14.12/2.31 fof(f4637,plain,(
% 14.12/2.31 ~r2_hidden(sK3_skl(sK1_skl,sK0_skl),sK1_skl)|~sQ77_spl|~sQ70_spl|~sQ74_spl|~sQ212_spl|~sQ16_spl|sQ437_spl),
% 14.12/2.31 inference(backward_demodulation,[status(thm)],[f4675,f4383])).
% 14.12/2.31 fof(f4675,plain,(
% 14.12/2.31 k4_lattices(sK0_skl,sK3_skl(sK1_skl,sK0_skl),k3_lattices(sK0_skl,sK2_skl(sK1_skl,sK0_skl),sK3_skl(sK1_skl,sK0_skl)))=sK3_skl(sK1_skl,sK0_skl)|~sQ77_spl|~sQ70_spl|~sQ74_spl|~sQ212_spl|~sQ16_spl),
% 14.12/2.31 inference(forward_demodulation,[status(thm)],[f2726,f4630])).
% 14.12/2.31 fof(f4722,plain,(
% 14.12/2.31 $false|~sQ18_spl|~sQ77_spl|~sQ70_spl|~sQ74_spl|~sQ212_spl|~sQ16_spl|sQ437_spl),
% 14.12/2.31 inference(forward_subsumption_resolution,[status(thm)],[f4637,f404])).
% 14.12/2.31 fof(f4723,plain,(
% 14.12/2.31 ~sQ18_spl|~sQ77_spl|~sQ70_spl|~sQ74_spl|~sQ212_spl|~sQ16_spl|sQ437_spl),
% 14.12/2.31 inference(contradiction_clause,[status(thm)],[f4722])).
% 14.12/2.31 fof(f4724,plain,(
% 14.12/2.31 $false),
% 14.12/2.31 inference(sat_refutation,[status(thm)],[f330,f337,f339,f346,f361,f384,f386,f388,f394,f400,f406,f667,f681,f685,f697,f709,f782,f857,f1950,f1954,f2547,f4388,f4494,f4604,f4606,f4723])).
% 14.12/2.31 % SZS output end CNFRefutation for theBenchmark.p
% 14.12/2.33 % Elapsed time: 1.948446 seconds
% 14.12/2.33 % CPU time: 14.997843 seconds
% 14.12/2.33 % Total memory used: 263.915 MB
% 14.12/2.33 % Net memory used: 258.279 MB
%------------------------------------------------------------------------------