%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT331+2 : 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 : n001.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:43 PM UTC 2026
% Result : Theorem 132.62s 17.50s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT331+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.46 % Computer : n001.cluster.edu
% 0.17/0.46 % Model : x86_64 x86_64
% 0.17/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.46 % Memory : 8046.5625MB
% 0.17/0.46 % OS : Linux 6.8.0-71-generic
% 0.17/0.46 % CPULimit : 300
% 0.17/0.46 % WCLimit : 300
% 0.17/0.46 % DateTime : Sun Sep 20 23:45:29 UTC 2026
% 0.17/0.46 % CPUTime :
% 0.40/0.70 % Drodi V4.1.1
% 132.62/17.50 % Refutation found
% 132.62/17.50 % SZS status Theorem for theBenchmark: Theorem is valid
% 132.62/17.50 % SZS output start CNFRefutation for theBenchmark
% 132.62/17.50 fof(f2439,axiom,(
% 132.62/17.50 (! [A,B] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A)& m1_filter_0(B,A) )=> ( ~ v3_struct_0(k8_filter_0(A,B))& v3_lattices(k8_filter_0(A,B))& v4_lattices(k8_filter_0(A,B))& v5_lattices(k8_filter_0(A,B))& v6_lattices(k8_filter_0(A,B))& v7_lattices(k8_filter_0(A,B))& v8_lattices(k8_filter_0(A,B))& v9_lattices(k8_filter_0(A,B))& v10_lattices(k8_filter_0(A,B)) ) ) )),
% 132.62/17.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.62/17.50 fof(f2506,axiom,(
% 132.62/17.50 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_filter_0(B,A)=> (! [C] :( ( ~ v3_struct_0(C)& v10_lattices(C)& l3_lattices(C) )=> ( C = k8_filter_0(A,B)<=> (? [D] :( v1_funct_1(D)& v1_funct_2(D,k2_zfmisc_1(B,B),B)& m2_relset_1(D,k2_zfmisc_1(B,B),B)& (? [E] :( v1_funct_1(E)& v1_funct_2(E,k2_zfmisc_1(B,B),B)& m2_relset_1(E,k2_zfmisc_1(B,B),B)& D = k1_realset1(u2_lattices(A),B)& E = k1_realset1(u1_lattices(A),B)& C = g3_lattices(B,D,E) ) )) )) ) )) )) )),
% 132.62/17.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.62/17.50 fof(f2509,axiom,(
% 132.62/17.50 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_filter_0(B,A)=> ( u1_struct_0(k8_filter_0(A,B)) = B& u2_lattices(k8_filter_0(A,B)) = k1_realset1(u2_lattices(A),B)& u1_lattices(k8_filter_0(A,B)) = k1_realset1(u1_lattices(A),B) ) ) )) )),
% 132.62/17.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.62/17.50 fof(f2551,axiom,(
% 132.62/17.50 (! [A,B] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A)& m1_filter_0(B,A) )=> ( ~ v3_struct_0(k8_filter_0(A,B))& v10_lattices(k8_filter_0(A,B))& l3_lattices(k8_filter_0(A,B)) ) ) )),
% 132.62/17.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.62/17.50 fof(f2597,axiom,(
% 132.62/17.50 (! [A] :( ( ~ v3_struct_0(A)& l3_lattices(A) )=> ( u1_struct_0(A) = u1_struct_0(k1_lattice2(A))& u2_lattices(A) = u1_lattices(k1_lattice2(A))& u1_lattices(A) = u2_lattices(k1_lattice2(A)) ) ) )),
% 132.62/17.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.62/17.50 fof(f2872,axiom,(
% 132.62/17.50 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_filter_2(B,A)<=> m1_filter_0(B,A) ) )) )),
% 132.62/17.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.62/17.50 fof(f2922,axiom,(
% 132.62/17.50 (! [A] :( l3_lattices(A)=> (! [B] :( l3_lattices(B)=> ( g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) = g3_lattices(u1_struct_0(B),u2_lattices(B),u1_lattices(B))=> k1_lattice2(A) = k1_lattice2(B) ) ) )) )),
% 132.62/17.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.62/17.50 fof(f2923,axiom,(
% 132.62/17.50 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> k1_lattice2(k1_lattice2(A)) = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) ) )),
% 132.62/17.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.62/17.50 fof(f3004,conjecture,(
% 132.62/17.50 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v10_lattices(B)& l3_lattices(B) )=> (! [C] :( m1_filter_2(C,A)=> (! [D] :( m1_filter_2(D,B)=> ( ( g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) = g3_lattices(u1_struct_0(B),u2_lattices(B),u1_lattices(B))& C = D )=> k8_filter_0(A,C) = k8_filter_0(B,D) ) ) )) )) )) )),
% 132.62/17.50 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 132.62/17.50 fof(f3005,negated_conjecture,(
% 132.62/17.50 ~((! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v10_lattices(B)& l3_lattices(B) )=> (! [C] :( m1_filter_2(C,A)=> (! [D] :( m1_filter_2(D,B)=> ( ( g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) = g3_lattices(u1_struct_0(B),u2_lattices(B),u1_lattices(B))& C = D )=> k8_filter_0(A,C) = k8_filter_0(B,D) ) ) )) )) )) ))),
% 132.62/17.50 inference(negated_conjecture,[status(cth)],[f3004])).
% 132.62/17.50 fof(f10044,plain,(
% 132.62/17.50 ![A,B]: ((((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|~m1_filter_0(B,A))|((((((((~v3_struct_0(k8_filter_0(A,B))&v3_lattices(k8_filter_0(A,B)))&v4_lattices(k8_filter_0(A,B)))&v5_lattices(k8_filter_0(A,B)))&v6_lattices(k8_filter_0(A,B)))&v7_lattices(k8_filter_0(A,B)))&v8_lattices(k8_filter_0(A,B)))&v9_lattices(k8_filter_0(A,B)))&v10_lattices(k8_filter_0(A,B))))),
% 132.62/17.50 inference(pre_NNF_transformation,[status(thm)],[f2439])).
% 132.62/17.50 fof(f10045,plain,(
% 132.62/17.50 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|~v3_struct_0(k8_filter_0(X0,X1)))),
% 132.62/17.50 inference(cnf_transformation,[status(thm)],[f10044])).
% 132.62/17.50 fof(f10053,plain,(
% 132.62/17.50 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|v10_lattices(k8_filter_0(X0,X1)))),
% 132.62/17.50 inference(cnf_transformation,[status(thm)],[f10044])).
% 132.62/17.50 fof(f10278,plain,(
% 132.62/17.50 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m1_filter_0(B,A)|(![C]: (((v3_struct_0(C)|~v10_lattices(C))|~l3_lattices(C))|(C=k8_filter_0(A,B)<=>(?[D]: (((v1_funct_1(D)&v1_funct_2(D,k2_zfmisc_1(B,B),B))&m2_relset_1(D,k2_zfmisc_1(B,B),B))&(?[E]: (((((v1_funct_1(E)&v1_funct_2(E,k2_zfmisc_1(B,B),B))&m2_relset_1(E,k2_zfmisc_1(B,B),B))&D=k1_realset1(u2_lattices(A),B))&E=k1_realset1(u1_lattices(A),B))&C=g3_lattices(B,D,E)))))))))))),
% 132.62/17.50 inference(pre_NNF_transformation,[status(thm)],[f2506])).
% 132.62/17.50 fof(f10279,plain,(
% 132.62/17.50 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m1_filter_0(B,A)|(![C]: (((v3_struct_0(C)|~v10_lattices(C))|~l3_lattices(C))|((~C=k8_filter_0(A,B)|(?[D]: (((v1_funct_1(D)&v1_funct_2(D,k2_zfmisc_1(B,B),B))&m2_relset_1(D,k2_zfmisc_1(B,B),B))&(?[E]: (((((v1_funct_1(E)&v1_funct_2(E,k2_zfmisc_1(B,B),B))&m2_relset_1(E,k2_zfmisc_1(B,B),B))&D=k1_realset1(u2_lattices(A),B))&E=k1_realset1(u1_lattices(A),B))&C=g3_lattices(B,D,E))))))&(C=k8_filter_0(A,B)|(![D]: (((~v1_funct_1(D)|~v1_funct_2(D,k2_zfmisc_1(B,B),B))|~m2_relset_1(D,k2_zfmisc_1(B,B),B))|(![E]: (((((~v1_funct_1(E)|~v1_funct_2(E,k2_zfmisc_1(B,B),B))|~m2_relset_1(E,k2_zfmisc_1(B,B),B))|~D=k1_realset1(u2_lattices(A),B))|~E=k1_realset1(u1_lattices(A),B))|~C=g3_lattices(B,D,E))))))))))))),
% 132.62/17.50 inference(NNF_transformation,[status(thm)],[f10278])).
% 132.62/17.50 fof(f10280,plain,(
% 132.62/17.50 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m1_filter_0(B,A)|(![C]: (((v3_struct_0(C)|~v10_lattices(C))|~l3_lattices(C))|((~C=k8_filter_0(A,B)|(((v1_funct_1(sK806_skl(C,B,A))&v1_funct_2(sK806_skl(C,B,A),k2_zfmisc_1(B,B),B))&m2_relset_1(sK806_skl(C,B,A),k2_zfmisc_1(B,B),B))&(((((v1_funct_1(sK807_skl(C,B,A))&v1_funct_2(sK807_skl(C,B,A),k2_zfmisc_1(B,B),B))&m2_relset_1(sK807_skl(C,B,A),k2_zfmisc_1(B,B),B))&sK806_skl(C,B,A)=k1_realset1(u2_lattices(A),B))&sK807_skl(C,B,A)=k1_realset1(u1_lattices(A),B))&C=g3_lattices(B,sK806_skl(C,B,A),sK807_skl(C,B,A)))))&(C=k8_filter_0(A,B)|(![D]: (((~v1_funct_1(D)|~v1_funct_2(D,k2_zfmisc_1(B,B),B))|~m2_relset_1(D,k2_zfmisc_1(B,B),B))|(![E]: (((((~v1_funct_1(E)|~v1_funct_2(E,k2_zfmisc_1(B,B),B))|~m2_relset_1(E,k2_zfmisc_1(B,B),B))|~D=k1_realset1(u2_lattices(A),B))|~E=k1_realset1(u1_lattices(A),B))|~C=g3_lattices(B,D,E))))))))))))),
% 132.62/17.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK806_skl,sK807_skl]),skolemize(D,sK806_skl(C,B,A)),skolemize(E,sK807_skl(C,B,A))],[f10279])).
% 132.62/17.50 fof(f10287,plain,(
% 132.62/17.50 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|v3_struct_0(X2)|~v10_lattices(X2)|~l3_lattices(X2)|~X2=k8_filter_0(X0,X1)|sK806_skl(X2,X1,X0)=k1_realset1(u2_lattices(X0),X1))),
% 132.62/17.50 inference(cnf_transformation,[status(thm)],[f10280])).
% 132.62/17.50 fof(f10288,plain,(
% 132.62/17.50 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|v3_struct_0(X2)|~v10_lattices(X2)|~l3_lattices(X2)|~X2=k8_filter_0(X0,X1)|sK807_skl(X2,X1,X0)=k1_realset1(u1_lattices(X0),X1))),
% 132.62/17.50 inference(cnf_transformation,[status(thm)],[f10280])).
% 132.62/17.50 fof(f10289,plain,(
% 132.62/17.50 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|v3_struct_0(X2)|~v10_lattices(X2)|~l3_lattices(X2)|~X2=k8_filter_0(X0,X1)|X2=g3_lattices(X1,sK806_skl(X2,X1,X0),sK807_skl(X2,X1,X0)))),
% 132.62/17.50 inference(cnf_transformation,[status(thm)],[f10280])).
% 132.62/17.50 fof(f10293,plain,(
% 132.62/17.50 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m1_filter_0(B,A)|((u1_struct_0(k8_filter_0(A,B))=B&u2_lattices(k8_filter_0(A,B))=k1_realset1(u2_lattices(A),B))&u1_lattices(k8_filter_0(A,B))=k1_realset1(u1_lattices(A),B)))))),
% 132.62/17.50 inference(pre_NNF_transformation,[status(thm)],[f2509])).
% 132.62/17.50 fof(f10295,plain,(
% 132.62/17.50 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|u2_lattices(k8_filter_0(X0,X1))=k1_realset1(u2_lattices(X0),X1))),
% 132.62/17.50 inference(cnf_transformation,[status(thm)],[f10293])).
% 132.62/17.50 fof(f10296,plain,(
% 132.62/17.50 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|u1_lattices(k8_filter_0(X0,X1))=k1_realset1(u1_lattices(X0),X1))),
% 132.62/17.50 inference(cnf_transformation,[status(thm)],[f10293])).
% 132.62/17.50 fof(f10402,plain,(
% 132.62/17.50 ![A,B]: ((((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|~m1_filter_0(B,A))|((~v3_struct_0(k8_filter_0(A,B))&v10_lattices(k8_filter_0(A,B)))&l3_lattices(k8_filter_0(A,B))))),
% 132.62/17.50 inference(pre_NNF_transformation,[status(thm)],[f2551])).
% 132.62/17.50 fof(f10405,plain,(
% 132.62/17.50 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|l3_lattices(k8_filter_0(X0,X1)))),
% 132.62/17.50 inference(cnf_transformation,[status(thm)],[f10402])).
% 132.62/17.50 fof(f10643,plain,(
% 132.62/17.50 ![A]: ((v3_struct_0(A)|~l3_lattices(A))|((u1_struct_0(A)=u1_struct_0(k1_lattice2(A))&u2_lattices(A)=u1_lattices(k1_lattice2(A)))&u1_lattices(A)=u2_lattices(k1_lattice2(A))))),
% 132.62/17.50 inference(pre_NNF_transformation,[status(thm)],[f2597])).
% 132.62/17.50 fof(f10645,plain,(
% 132.62/17.50 ![X0]: (v3_struct_0(X0)|~l3_lattices(X0)|u2_lattices(X0)=u1_lattices(k1_lattice2(X0)))),
% 132.62/17.50 inference(cnf_transformation,[status(thm)],[f10643])).
% 132.62/17.50 fof(f10646,plain,(
% 132.62/17.50 ![X0]: (v3_struct_0(X0)|~l3_lattices(X0)|u1_lattices(X0)=u2_lattices(k1_lattice2(X0)))),
% 132.62/17.50 inference(cnf_transformation,[status(thm)],[f10643])).
% 132.62/17.50 fof(f11324,plain,(
% 132.62/17.50 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (m1_filter_2(B,A)<=>m1_filter_0(B,A))))),
% 132.62/17.50 inference(pre_NNF_transformation,[status(thm)],[f2872])).
% 132.62/17.50 fof(f11325,plain,(
% 132.62/17.50 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: ((~m1_filter_2(B,A)|m1_filter_0(B,A))&(m1_filter_2(B,A)|~m1_filter_0(B,A)))))),
% 132.62/17.50 inference(NNF_transformation,[status(thm)],[f11324])).
% 132.62/17.50 fof(f11326,plain,(
% 132.62/17.50 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|((![B]: (~m1_filter_2(B,A)|m1_filter_0(B,A)))&(![B]: (m1_filter_2(B,A)|~m1_filter_0(B,A)))))),
% 132.62/17.50 inference(miniscoping,[status(thm)],[f11325])).
% 132.62/17.50 fof(f11327,plain,(
% 132.62/17.50 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_2(X1,X0)|m1_filter_0(X1,X0))),
% 132.62/17.50 inference(cnf_transformation,[status(thm)],[f11326])).
% 132.62/17.50 fof(f11447,plain,(
% 132.62/17.50 ![A]: (~l3_lattices(A)|(![B]: (~l3_lattices(B)|(~g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A))=g3_lattices(u1_struct_0(B),u2_lattices(B),u1_lattices(B))|k1_lattice2(A)=k1_lattice2(B)))))),
% 132.62/17.50 inference(pre_NNF_transformation,[status(thm)],[f2922])).
% 132.62/17.50 fof(f11448,plain,(
% 132.62/17.50 ![X0,X1]: (~l3_lattices(X0)|~l3_lattices(X1)|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))|k1_lattice2(X0)=k1_lattice2(X1))),
% 132.62/17.50 inference(cnf_transformation,[status(thm)],[f11447])).
% 132.62/17.50 fof(f11449,plain,(
% 132.62/17.50 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|k1_lattice2(k1_lattice2(A))=g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)))),
% 132.62/17.50 inference(pre_NNF_transformation,[status(thm)],[f2923])).
% 132.62/17.50 fof(f11450,plain,(
% 132.62/17.50 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|k1_lattice2(k1_lattice2(X0))=g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)))),
% 132.62/17.50 inference(cnf_transformation,[status(thm)],[f11449])).
% 132.62/17.50 fof(f11788,plain,(
% 132.62/17.50 (?[A]: (((~v3_struct_0(A)&v10_lattices(A))&l3_lattices(A))&(?[B]: (((~v3_struct_0(B)&v10_lattices(B))&l3_lattices(B))&(?[C]: (m1_filter_2(C,A)&(?[D]: (m1_filter_2(D,B)&((g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A))=g3_lattices(u1_struct_0(B),u2_lattices(B),u1_lattices(B))&C=D)&~k8_filter_0(A,C)=k8_filter_0(B,D))))))))))),
% 132.62/17.50 inference(pre_NNF_transformation,[status(thm)],[f3005])).
% 132.62/17.50 fof(f11789,plain,(
% 132.62/17.50 (((~v3_struct_0(sK909_skl)&v10_lattices(sK909_skl))&l3_lattices(sK909_skl))&(((~v3_struct_0(sK910_skl)&v10_lattices(sK910_skl))&l3_lattices(sK910_skl))&(m1_filter_2(sK911_skl,sK909_skl)&(m1_filter_2(sK912_skl,sK910_skl)&((g3_lattices(u1_struct_0(sK909_skl),u2_lattices(sK909_skl),u1_lattices(sK909_skl))=g3_lattices(u1_struct_0(sK910_skl),u2_lattices(sK910_skl),u1_lattices(sK910_skl))&sK911_skl=sK912_skl)&~k8_filter_0(sK909_skl,sK911_skl)=k8_filter_0(sK910_skl,sK912_skl))))))),
% 132.62/17.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK909_skl,sK910_skl,sK911_skl,sK912_skl]),skolemize(A,sK909_skl),skolemize(B,sK910_skl),skolemize(C,sK911_skl),skolemize(D,sK912_skl)],[f11788])).
% 132.62/17.50 fof(f11790,plain,(
% 132.62/17.50 ~v3_struct_0(sK909_skl)),
% 132.62/17.50 inference(cnf_transformation,[status(thm)],[f11789])).
% 132.62/17.50 fof(f11791,plain,(
% 132.62/17.50 v10_lattices(sK909_skl)),
% 132.62/17.50 inference(cnf_transformation,[status(thm)],[f11789])).
% 132.62/17.50 fof(f11792,plain,(
% 132.62/17.50 l3_lattices(sK909_skl)),
% 132.62/17.50 inference(cnf_transformation,[status(thm)],[f11789])).
% 132.62/17.50 fof(f11793,plain,(
% 132.62/17.50 ~v3_struct_0(sK910_skl)),
% 132.62/17.50 inference(cnf_transformation,[status(thm)],[f11789])).
% 132.62/17.50 fof(f11794,plain,(
% 132.62/17.50 v10_lattices(sK910_skl)),
% 132.62/17.50 inference(cnf_transformation,[status(thm)],[f11789])).
% 132.62/17.50 fof(f11795,plain,(
% 132.62/17.50 l3_lattices(sK910_skl)),
% 132.62/17.50 inference(cnf_transformation,[status(thm)],[f11789])).
% 132.62/17.50 fof(f11796,plain,(
% 132.62/17.50 m1_filter_2(sK911_skl,sK909_skl)),
% 132.62/17.50 inference(cnf_transformation,[status(thm)],[f11789])).
% 132.62/17.50 fof(f11797,plain,(
% 132.62/17.50 m1_filter_2(sK912_skl,sK910_skl)),
% 132.62/17.50 inference(cnf_transformation,[status(thm)],[f11789])).
% 132.62/17.50 fof(f11798,plain,(
% 132.62/17.50 g3_lattices(u1_struct_0(sK909_skl),u2_lattices(sK909_skl),u1_lattices(sK909_skl))=g3_lattices(u1_struct_0(sK910_skl),u2_lattices(sK910_skl),u1_lattices(sK910_skl))),
% 132.62/17.50 inference(cnf_transformation,[status(thm)],[f11789])).
% 132.62/17.50 fof(f11799,plain,(
% 132.62/17.50 sK911_skl=sK912_skl),
% 132.62/17.50 inference(cnf_transformation,[status(thm)],[f11789])).
% 132.62/17.50 fof(f11800,plain,(
% 132.62/17.50 ~k8_filter_0(sK909_skl,sK911_skl)=k8_filter_0(sK910_skl,sK912_skl)),
% 132.62/17.50 inference(cnf_transformation,[status(thm)],[f11789])).
% 132.62/17.50 fof(f13591,plain,(
% 132.62/17.50 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|v3_struct_0(k8_filter_0(X0,X1))|~v10_lattices(k8_filter_0(X0,X1))|~l3_lattices(k8_filter_0(X0,X1))|sK806_skl(k8_filter_0(X0,X1),X1,X0)=k1_realset1(u2_lattices(X0),X1))),
% 132.62/17.50 inference(destructive_equality_resolution,[status(thm)],[f10287])).
% 132.62/17.50 fof(f13592,plain,(
% 132.62/17.50 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|~v10_lattices(k8_filter_0(X0,X1))|~l3_lattices(k8_filter_0(X0,X1))|sK806_skl(k8_filter_0(X0,X1),X1,X0)=k1_realset1(u2_lattices(X0),X1))),
% 132.62/17.50 inference(forward_subsumption_resolution,[status(thm)],[f13591,f10045])).
% 132.62/17.50 fof(f13593,plain,(
% 132.62/17.50 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|v3_struct_0(k8_filter_0(X0,X1))|~v10_lattices(k8_filter_0(X0,X1))|~l3_lattices(k8_filter_0(X0,X1))|sK807_skl(k8_filter_0(X0,X1),X1,X0)=k1_realset1(u1_lattices(X0),X1))),
% 132.62/17.50 inference(destructive_equality_resolution,[status(thm)],[f10288])).
% 132.62/17.50 fof(f13594,plain,(
% 132.62/17.50 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|~v10_lattices(k8_filter_0(X0,X1))|~l3_lattices(k8_filter_0(X0,X1))|sK807_skl(k8_filter_0(X0,X1),X1,X0)=k1_realset1(u1_lattices(X0),X1))),
% 132.62/17.50 inference(forward_subsumption_resolution,[status(thm)],[f13593,f10045])).
% 132.62/17.50 fof(f13595,plain,(
% 132.62/17.50 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|v3_struct_0(k8_filter_0(X0,X1))|~v10_lattices(k8_filter_0(X0,X1))|~l3_lattices(k8_filter_0(X0,X1))|k8_filter_0(X0,X1)=g3_lattices(X1,sK806_skl(k8_filter_0(X0,X1),X1,X0),sK807_skl(k8_filter_0(X0,X1),X1,X0)))),
% 132.62/17.50 inference(destructive_equality_resolution,[status(thm)],[f10289])).
% 132.62/17.50 fof(f13596,plain,(
% 132.62/17.50 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|~v10_lattices(k8_filter_0(X0,X1))|~l3_lattices(k8_filter_0(X0,X1))|k8_filter_0(X0,X1)=g3_lattices(X1,sK806_skl(k8_filter_0(X0,X1),X1,X0),sK807_skl(k8_filter_0(X0,X1),X1,X0)))),
% 132.62/17.50 inference(forward_subsumption_resolution,[status(thm)],[f13595,f10045])).
% 132.62/17.50 fof(f13633,plain,(
% 132.62/17.50 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|~v10_lattices(k8_filter_0(X0,X1))|k8_filter_0(X0,X1)=g3_lattices(X1,sK806_skl(k8_filter_0(X0,X1),X1,X0),sK807_skl(k8_filter_0(X0,X1),X1,X0)))),
% 132.62/17.50 inference(backward_subsumption_resolution,[status(thm)],[f13596,f10405])).
% 132.62/17.51 fof(f13634,plain,(
% 132.62/17.51 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|~v10_lattices(k8_filter_0(X0,X1))|sK807_skl(k8_filter_0(X0,X1),X1,X0)=k1_realset1(u1_lattices(X0),X1))),
% 132.62/17.51 inference(backward_subsumption_resolution,[status(thm)],[f13594,f10405])).
% 132.62/17.51 fof(f13635,plain,(
% 132.62/17.51 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|~v10_lattices(k8_filter_0(X0,X1))|sK806_skl(k8_filter_0(X0,X1),X1,X0)=k1_realset1(u2_lattices(X0),X1))),
% 132.62/17.51 inference(backward_subsumption_resolution,[status(thm)],[f13592,f10405])).
% 132.62/17.51 fof(f13924,plain,(
% 132.62/17.51 m1_filter_2(sK911_skl,sK910_skl)),
% 132.62/17.51 inference(backward_demodulation,[status(thm)],[f11799,f11797])).
% 132.62/17.51 fof(f13925,plain,(
% 132.62/17.51 ~k8_filter_0(sK909_skl,sK911_skl)=k8_filter_0(sK910_skl,sK911_skl)),
% 132.62/17.51 inference(forward_demodulation,[status(thm)],[f11799,f11800])).
% 132.62/17.51 fof(f14103,plain,(
% 132.62/17.51 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|k8_filter_0(X0,X1)=g3_lattices(X1,sK806_skl(k8_filter_0(X0,X1),X1,X0),sK807_skl(k8_filter_0(X0,X1),X1,X0)))),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f13633,f10053])).
% 132.62/17.51 fof(f14104,plain,(
% 132.62/17.51 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|sK807_skl(k8_filter_0(X0,X1),X1,X0)=k1_realset1(u1_lattices(X0),X1))),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f13634,f10053])).
% 132.62/17.51 fof(f14105,plain,(
% 132.62/17.51 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|sK806_skl(k8_filter_0(X0,X1),X1,X0)=k1_realset1(u2_lattices(X0),X1))),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f13635,f10053])).
% 132.62/17.51 fof(f14152,plain,(
% 132.62/17.51 ![X0]: (v3_struct_0(sK910_skl)|~l3_lattices(sK910_skl)|~m1_filter_2(X0,sK910_skl)|m1_filter_0(X0,sK910_skl))),
% 132.62/17.51 inference(resolution,[status(thm)],[f11327,f11794])).
% 132.62/17.51 fof(f14153,plain,(
% 132.62/17.51 ![X0]: (v3_struct_0(sK909_skl)|~l3_lattices(sK909_skl)|~m1_filter_2(X0,sK909_skl)|m1_filter_0(X0,sK909_skl))),
% 132.62/17.51 inference(resolution,[status(thm)],[f11327,f11791])).
% 132.62/17.51 fof(f14154,plain,(
% 132.62/17.51 ![X0]: (~l3_lattices(sK910_skl)|~m1_filter_2(X0,sK910_skl)|m1_filter_0(X0,sK910_skl))),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14152,f11793])).
% 132.62/17.51 fof(f14155,plain,(
% 132.62/17.51 ![X0]: (~l3_lattices(sK909_skl)|~m1_filter_2(X0,sK909_skl)|m1_filter_0(X0,sK909_skl))),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14153,f11790])).
% 132.62/17.51 fof(f14186,plain,(
% 132.62/17.51 v3_struct_0(sK910_skl)|u2_lattices(sK910_skl)=u1_lattices(k1_lattice2(sK910_skl))),
% 132.62/17.51 inference(resolution,[status(thm)],[f10645,f11795])).
% 132.62/17.51 fof(f14187,plain,(
% 132.62/17.51 v3_struct_0(sK909_skl)|u2_lattices(sK909_skl)=u1_lattices(k1_lattice2(sK909_skl))),
% 132.62/17.51 inference(resolution,[status(thm)],[f10645,f11792])).
% 132.62/17.51 fof(f14188,plain,(
% 132.62/17.51 u2_lattices(sK910_skl)=u1_lattices(k1_lattice2(sK910_skl))),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14186,f11793])).
% 132.62/17.51 fof(f14189,plain,(
% 132.62/17.51 u2_lattices(sK909_skl)=u1_lattices(k1_lattice2(sK909_skl))),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14187,f11790])).
% 132.62/17.51 fof(f14210,plain,(
% 132.62/17.51 v3_struct_0(sK910_skl)|u1_lattices(sK910_skl)=u2_lattices(k1_lattice2(sK910_skl))),
% 132.62/17.51 inference(resolution,[status(thm)],[f10646,f11795])).
% 132.62/17.51 fof(f14211,plain,(
% 132.62/17.51 v3_struct_0(sK909_skl)|u1_lattices(sK909_skl)=u2_lattices(k1_lattice2(sK909_skl))),
% 132.62/17.51 inference(resolution,[status(thm)],[f10646,f11792])).
% 132.62/17.51 fof(f14213,plain,(
% 132.62/17.51 u1_lattices(sK910_skl)=u2_lattices(k1_lattice2(sK910_skl))),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14210,f11793])).
% 132.62/17.51 fof(f14215,plain,(
% 132.62/17.51 u1_lattices(sK909_skl)=u2_lattices(k1_lattice2(sK909_skl))),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14211,f11790])).
% 132.62/17.51 fof(f14265,plain,(
% 132.62/17.51 ![X0]: (~m1_filter_2(X0,sK910_skl)|m1_filter_0(X0,sK910_skl))),
% 132.62/17.51 inference(resolution,[status(thm)],[f14154,f11795])).
% 132.62/17.51 fof(f14266,plain,(
% 132.62/17.51 ![X0]: (~m1_filter_2(X0,sK909_skl)|m1_filter_0(X0,sK909_skl))),
% 132.62/17.51 inference(resolution,[status(thm)],[f14155,f11792])).
% 132.62/17.51 fof(f14267,plain,(
% 132.62/17.51 m1_filter_0(sK911_skl,sK910_skl)),
% 132.62/17.51 inference(resolution,[status(thm)],[f14265,f13924])).
% 132.62/17.51 fof(f14269,plain,(
% 132.62/17.51 v3_struct_0(sK910_skl)|~v10_lattices(sK910_skl)|~l3_lattices(sK910_skl)|u1_lattices(k8_filter_0(sK910_skl,sK911_skl))=k1_realset1(u1_lattices(sK910_skl),sK911_skl)),
% 132.62/17.51 inference(resolution,[status(thm)],[f14267,f10296])).
% 132.62/17.51 fof(f14270,plain,(
% 132.62/17.51 v3_struct_0(sK910_skl)|~v10_lattices(sK910_skl)|~l3_lattices(sK910_skl)|u2_lattices(k8_filter_0(sK910_skl,sK911_skl))=k1_realset1(u2_lattices(sK910_skl),sK911_skl)),
% 132.62/17.51 inference(resolution,[status(thm)],[f14267,f10295])).
% 132.62/17.51 fof(f14273,plain,(
% 132.62/17.51 ~v10_lattices(sK910_skl)|~l3_lattices(sK910_skl)|u1_lattices(k8_filter_0(sK910_skl,sK911_skl))=k1_realset1(u1_lattices(sK910_skl),sK911_skl)),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14269,f11793])).
% 132.62/17.51 fof(f14274,plain,(
% 132.62/17.51 ~v10_lattices(sK910_skl)|~l3_lattices(sK910_skl)|u2_lattices(k8_filter_0(sK910_skl,sK911_skl))=k1_realset1(u2_lattices(sK910_skl),sK911_skl)),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14270,f11793])).
% 132.62/17.51 fof(f14277,plain,(
% 132.62/17.51 m1_filter_0(sK911_skl,sK909_skl)),
% 132.62/17.51 inference(resolution,[status(thm)],[f14266,f11796])).
% 132.62/17.51 fof(f14279,plain,(
% 132.62/17.51 v3_struct_0(sK909_skl)|~v10_lattices(sK909_skl)|~l3_lattices(sK909_skl)|u1_lattices(k8_filter_0(sK909_skl,sK911_skl))=k1_realset1(u1_lattices(sK909_skl),sK911_skl)),
% 132.62/17.51 inference(resolution,[status(thm)],[f14277,f10296])).
% 132.62/17.51 fof(f14280,plain,(
% 132.62/17.51 v3_struct_0(sK909_skl)|~v10_lattices(sK909_skl)|~l3_lattices(sK909_skl)|u2_lattices(k8_filter_0(sK909_skl,sK911_skl))=k1_realset1(u2_lattices(sK909_skl),sK911_skl)),
% 132.62/17.51 inference(resolution,[status(thm)],[f14277,f10295])).
% 132.62/17.51 fof(f14283,plain,(
% 132.62/17.51 ~v10_lattices(sK909_skl)|~l3_lattices(sK909_skl)|u1_lattices(k8_filter_0(sK909_skl,sK911_skl))=k1_realset1(u1_lattices(sK909_skl),sK911_skl)),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14279,f11790])).
% 132.62/17.51 fof(f14284,plain,(
% 132.62/17.51 ~v10_lattices(sK909_skl)|~l3_lattices(sK909_skl)|u2_lattices(k8_filter_0(sK909_skl,sK911_skl))=k1_realset1(u2_lattices(sK909_skl),sK911_skl)),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14280,f11790])).
% 132.62/17.51 fof(f14415,plain,(
% 132.62/17.51 ![X0]: (~l3_lattices(X0)|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(u1_struct_0(sK909_skl),u2_lattices(sK909_skl),u1_lattices(sK909_skl))|k1_lattice2(X0)=k1_lattice2(sK909_skl))),
% 132.62/17.51 inference(resolution,[status(thm)],[f11448,f11792])).
% 132.62/17.51 fof(f14421,plain,(
% 132.62/17.51 v3_struct_0(sK910_skl)|~l3_lattices(sK910_skl)|k1_lattice2(k1_lattice2(sK910_skl))=g3_lattices(u1_struct_0(sK910_skl),u2_lattices(sK910_skl),u1_lattices(sK910_skl))),
% 132.62/17.51 inference(resolution,[status(thm)],[f11450,f11794])).
% 132.62/17.51 fof(f14422,plain,(
% 132.62/17.51 v3_struct_0(sK909_skl)|~l3_lattices(sK909_skl)|k1_lattice2(k1_lattice2(sK909_skl))=g3_lattices(u1_struct_0(sK909_skl),u2_lattices(sK909_skl),u1_lattices(sK909_skl))),
% 132.62/17.51 inference(resolution,[status(thm)],[f11450,f11791])).
% 132.62/17.51 fof(f14427,plain,(
% 132.62/17.51 v3_struct_0(sK910_skl)|~l3_lattices(sK910_skl)|k1_lattice2(k1_lattice2(sK910_skl))=g3_lattices(u1_struct_0(sK909_skl),u2_lattices(sK909_skl),u1_lattices(sK909_skl))),
% 132.62/17.51 inference(forward_demodulation,[status(thm)],[f11798,f14421])).
% 132.62/17.51 fof(f14428,plain,(
% 132.62/17.51 ~l3_lattices(sK910_skl)|k1_lattice2(k1_lattice2(sK910_skl))=g3_lattices(u1_struct_0(sK909_skl),u2_lattices(sK909_skl),u1_lattices(sK909_skl))),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14427,f11793])).
% 132.62/17.51 fof(f14429,plain,(
% 132.62/17.51 ~l3_lattices(sK909_skl)|k1_lattice2(k1_lattice2(sK909_skl))=g3_lattices(u1_struct_0(sK909_skl),u2_lattices(sK909_skl),u1_lattices(sK909_skl))),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14422,f11790])).
% 132.62/17.51 fof(f14434,plain,(
% 132.62/17.51 k1_lattice2(k1_lattice2(sK910_skl))=g3_lattices(u1_struct_0(sK909_skl),u2_lattices(sK909_skl),u1_lattices(sK909_skl))),
% 132.62/17.51 inference(resolution,[status(thm)],[f14428,f11795])).
% 132.62/17.51 fof(f14438,plain,(
% 132.62/17.51 k1_lattice2(k1_lattice2(sK910_skl))=g3_lattices(u1_struct_0(sK910_skl),u2_lattices(sK910_skl),u1_lattices(sK910_skl))),
% 132.62/17.51 inference(backward_demodulation,[status(thm)],[f14434,f11798])).
% 132.62/17.51 fof(f14439,plain,(
% 132.62/17.51 ~l3_lattices(sK909_skl)|k1_lattice2(k1_lattice2(sK909_skl))=k1_lattice2(k1_lattice2(sK910_skl))),
% 132.62/17.51 inference(backward_demodulation,[status(thm)],[f14434,f14429])).
% 132.62/17.51 fof(f14440,plain,(
% 132.62/17.51 ![X0]: (~l3_lattices(X0)|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=k1_lattice2(k1_lattice2(sK910_skl))|k1_lattice2(X0)=k1_lattice2(sK909_skl))),
% 132.62/17.51 inference(backward_demodulation,[status(thm)],[f14434,f14415])).
% 132.62/17.51 fof(f14442,plain,(
% 132.62/17.51 k1_lattice2(k1_lattice2(sK909_skl))=g3_lattices(u1_struct_0(sK910_skl),u2_lattices(sK910_skl),u1_lattices(sK910_skl))),
% 132.62/17.51 inference(backward_demodulation,[status(thm)],[f14446,f14438])).
% 132.62/17.51 fof(f14446,plain,(
% 132.62/17.51 k1_lattice2(k1_lattice2(sK909_skl))=k1_lattice2(k1_lattice2(sK910_skl))),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14439,f11792])).
% 132.62/17.51 fof(f14447,plain,(
% 132.62/17.51 ![X0]: (~l3_lattices(X0)|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=k1_lattice2(k1_lattice2(sK909_skl))|k1_lattice2(X0)=k1_lattice2(sK909_skl))),
% 132.62/17.51 inference(forward_demodulation,[status(thm)],[f14446,f14440])).
% 132.62/17.51 fof(f14478,plain,(
% 132.62/17.51 ~l3_lattices(sK910_skl)|u1_lattices(k8_filter_0(sK910_skl,sK911_skl))=k1_realset1(u1_lattices(sK910_skl),sK911_skl)),
% 132.62/17.51 inference(resolution,[status(thm)],[f14273,f11794])).
% 132.62/17.51 fof(f14480,plain,(
% 132.62/17.51 u1_lattices(k8_filter_0(sK910_skl,sK911_skl))=k1_realset1(u1_lattices(sK910_skl),sK911_skl)),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14478,f11795])).
% 132.62/17.51 fof(f14484,plain,(
% 132.62/17.51 ~g3_lattices(u1_struct_0(sK910_skl),u2_lattices(sK910_skl),u1_lattices(sK910_skl))=k1_lattice2(k1_lattice2(sK909_skl))|k1_lattice2(sK910_skl)=k1_lattice2(sK909_skl)),
% 132.62/17.51 inference(resolution,[status(thm)],[f14447,f11795])).
% 132.62/17.51 fof(f14488,plain,(
% 132.62/17.51 ~k1_lattice2(k1_lattice2(sK909_skl))=k1_lattice2(k1_lattice2(sK909_skl))|k1_lattice2(sK910_skl)=k1_lattice2(sK909_skl)),
% 132.62/17.51 inference(forward_demodulation,[status(thm)],[f14442,f14484])).
% 132.62/17.51 fof(f14493,plain,(
% 132.62/17.51 u1_lattices(sK910_skl)=u2_lattices(k1_lattice2(sK909_skl))),
% 132.62/17.51 inference(backward_demodulation,[status(thm)],[f14500,f14213])).
% 132.62/17.51 fof(f14494,plain,(
% 132.62/17.51 u2_lattices(sK910_skl)=u1_lattices(k1_lattice2(sK909_skl))),
% 132.62/17.51 inference(backward_demodulation,[status(thm)],[f14500,f14188])).
% 132.62/17.51 fof(f14500,plain,(
% 132.62/17.51 k1_lattice2(sK910_skl)=k1_lattice2(sK909_skl)),
% 132.62/17.51 inference(trivial_equality_resolution,[status(thm)],[f14488])).
% 132.62/17.51 fof(f14509,plain,(
% 132.62/17.51 u1_lattices(k8_filter_0(sK910_skl,sK911_skl))=k1_realset1(u1_lattices(sK909_skl),sK911_skl)),
% 132.62/17.51 inference(backward_demodulation,[status(thm)],[f14512,f14480])).
% 132.62/17.51 fof(f14512,plain,(
% 132.62/17.51 u1_lattices(sK910_skl)=u1_lattices(sK909_skl)),
% 132.62/17.51 inference(forward_demodulation,[status(thm)],[f14215,f14493])).
% 132.62/17.51 fof(f14513,plain,(
% 132.62/17.51 ~v10_lattices(sK910_skl)|~l3_lattices(sK910_skl)|u2_lattices(k8_filter_0(sK910_skl,sK911_skl))=k1_realset1(u2_lattices(sK909_skl),sK911_skl)),
% 132.62/17.51 inference(backward_demodulation,[status(thm)],[f14514,f14274])).
% 132.62/17.51 fof(f14514,plain,(
% 132.62/17.51 u2_lattices(sK910_skl)=u2_lattices(sK909_skl)),
% 132.62/17.51 inference(forward_demodulation,[status(thm)],[f14189,f14494])).
% 132.62/17.51 fof(f14547,plain,(
% 132.62/17.51 ~v10_lattices(sK909_skl)|~l3_lattices(sK909_skl)|u1_lattices(k8_filter_0(sK909_skl,sK911_skl))=u1_lattices(k8_filter_0(sK910_skl,sK911_skl))),
% 132.62/17.51 inference(backward_demodulation,[status(thm)],[f14509,f14283])).
% 132.62/17.51 fof(f14558,plain,(
% 132.62/17.51 ~l3_lattices(sK910_skl)|u2_lattices(k8_filter_0(sK910_skl,sK911_skl))=k1_realset1(u2_lattices(sK909_skl),sK911_skl)),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14513,f11794])).
% 132.62/17.51 fof(f14559,plain,(
% 132.62/17.51 ~l3_lattices(sK909_skl)|u1_lattices(k8_filter_0(sK909_skl,sK911_skl))=u1_lattices(k8_filter_0(sK910_skl,sK911_skl))),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14547,f11791])).
% 132.62/17.51 fof(f14569,plain,(
% 132.62/17.51 v3_struct_0(sK909_skl)|~v10_lattices(sK909_skl)|~l3_lattices(sK909_skl)|k8_filter_0(sK909_skl,sK911_skl)=g3_lattices(sK911_skl,sK806_skl(k8_filter_0(sK909_skl,sK911_skl),sK911_skl,sK909_skl),sK807_skl(k8_filter_0(sK909_skl,sK911_skl),sK911_skl,sK909_skl))),
% 132.62/17.51 inference(resolution,[status(thm)],[f14103,f14277])).
% 132.62/17.51 fof(f14570,plain,(
% 132.62/17.51 v3_struct_0(sK910_skl)|~v10_lattices(sK910_skl)|~l3_lattices(sK910_skl)|k8_filter_0(sK910_skl,sK911_skl)=g3_lattices(sK911_skl,sK806_skl(k8_filter_0(sK910_skl,sK911_skl),sK911_skl,sK910_skl),sK807_skl(k8_filter_0(sK910_skl,sK911_skl),sK911_skl,sK910_skl))),
% 132.62/17.51 inference(resolution,[status(thm)],[f14103,f14267])).
% 132.62/17.51 fof(f14571,plain,(
% 132.62/17.51 ~v10_lattices(sK909_skl)|~l3_lattices(sK909_skl)|k8_filter_0(sK909_skl,sK911_skl)=g3_lattices(sK911_skl,sK806_skl(k8_filter_0(sK909_skl,sK911_skl),sK911_skl,sK909_skl),sK807_skl(k8_filter_0(sK909_skl,sK911_skl),sK911_skl,sK909_skl))),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14569,f11790])).
% 132.62/17.51 fof(f14572,plain,(
% 132.62/17.51 ~v10_lattices(sK910_skl)|~l3_lattices(sK910_skl)|k8_filter_0(sK910_skl,sK911_skl)=g3_lattices(sK911_skl,sK806_skl(k8_filter_0(sK910_skl,sK911_skl),sK911_skl,sK910_skl),sK807_skl(k8_filter_0(sK910_skl,sK911_skl),sK911_skl,sK910_skl))),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14570,f11793])).
% 132.62/17.51 fof(f14573,plain,(
% 132.62/17.51 v3_struct_0(sK909_skl)|~v10_lattices(sK909_skl)|~l3_lattices(sK909_skl)|sK807_skl(k8_filter_0(sK909_skl,sK911_skl),sK911_skl,sK909_skl)=k1_realset1(u1_lattices(sK909_skl),sK911_skl)),
% 132.62/17.51 inference(resolution,[status(thm)],[f14104,f14277])).
% 132.62/17.51 fof(f14574,plain,(
% 132.62/17.51 v3_struct_0(sK910_skl)|~v10_lattices(sK910_skl)|~l3_lattices(sK910_skl)|sK807_skl(k8_filter_0(sK910_skl,sK911_skl),sK911_skl,sK910_skl)=k1_realset1(u1_lattices(sK910_skl),sK911_skl)),
% 132.62/17.51 inference(resolution,[status(thm)],[f14104,f14267])).
% 132.62/17.51 fof(f14575,plain,(
% 132.62/17.51 v3_struct_0(sK909_skl)|~v10_lattices(sK909_skl)|~l3_lattices(sK909_skl)|sK807_skl(k8_filter_0(sK909_skl,sK911_skl),sK911_skl,sK909_skl)=u1_lattices(k8_filter_0(sK910_skl,sK911_skl))),
% 132.62/17.51 inference(forward_demodulation,[status(thm)],[f14509,f14573])).
% 132.62/17.51 fof(f14576,plain,(
% 132.62/17.51 ~v10_lattices(sK909_skl)|~l3_lattices(sK909_skl)|sK807_skl(k8_filter_0(sK909_skl,sK911_skl),sK911_skl,sK909_skl)=u1_lattices(k8_filter_0(sK910_skl,sK911_skl))),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14575,f11790])).
% 132.62/17.51 fof(f14577,plain,(
% 132.62/17.51 v3_struct_0(sK910_skl)|~v10_lattices(sK910_skl)|~l3_lattices(sK910_skl)|sK807_skl(k8_filter_0(sK910_skl,sK911_skl),sK911_skl,sK910_skl)=k1_realset1(u1_lattices(sK909_skl),sK911_skl)),
% 132.62/17.51 inference(forward_demodulation,[status(thm)],[f14512,f14574])).
% 132.62/17.51 fof(f14578,plain,(
% 132.62/17.51 v3_struct_0(sK910_skl)|~v10_lattices(sK910_skl)|~l3_lattices(sK910_skl)|sK807_skl(k8_filter_0(sK910_skl,sK911_skl),sK911_skl,sK910_skl)=u1_lattices(k8_filter_0(sK910_skl,sK911_skl))),
% 132.62/17.51 inference(forward_demodulation,[status(thm)],[f14509,f14577])).
% 132.62/17.51 fof(f14579,plain,(
% 132.62/17.51 ~v10_lattices(sK910_skl)|~l3_lattices(sK910_skl)|sK807_skl(k8_filter_0(sK910_skl,sK911_skl),sK911_skl,sK910_skl)=u1_lattices(k8_filter_0(sK910_skl,sK911_skl))),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14578,f11793])).
% 132.62/17.51 fof(f14627,plain,(
% 132.62/17.51 v3_struct_0(sK909_skl)|~v10_lattices(sK909_skl)|~l3_lattices(sK909_skl)|sK806_skl(k8_filter_0(sK909_skl,sK911_skl),sK911_skl,sK909_skl)=k1_realset1(u2_lattices(sK909_skl),sK911_skl)),
% 132.62/17.51 inference(resolution,[status(thm)],[f14105,f14277])).
% 132.62/17.51 fof(f14628,plain,(
% 132.62/17.51 v3_struct_0(sK910_skl)|~v10_lattices(sK910_skl)|~l3_lattices(sK910_skl)|sK806_skl(k8_filter_0(sK910_skl,sK911_skl),sK911_skl,sK910_skl)=k1_realset1(u2_lattices(sK910_skl),sK911_skl)),
% 132.62/17.51 inference(resolution,[status(thm)],[f14105,f14267])).
% 132.62/17.51 fof(f14629,plain,(
% 132.62/17.51 ~v10_lattices(sK909_skl)|~l3_lattices(sK909_skl)|sK806_skl(k8_filter_0(sK909_skl,sK911_skl),sK911_skl,sK909_skl)=k1_realset1(u2_lattices(sK909_skl),sK911_skl)),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14627,f11790])).
% 132.62/17.51 fof(f14630,plain,(
% 132.62/17.51 v3_struct_0(sK910_skl)|~v10_lattices(sK910_skl)|~l3_lattices(sK910_skl)|sK806_skl(k8_filter_0(sK910_skl,sK911_skl),sK911_skl,sK910_skl)=k1_realset1(u2_lattices(sK909_skl),sK911_skl)),
% 132.62/17.51 inference(forward_demodulation,[status(thm)],[f14514,f14628])).
% 132.62/17.51 fof(f14631,plain,(
% 132.62/17.51 ~v10_lattices(sK910_skl)|~l3_lattices(sK910_skl)|sK806_skl(k8_filter_0(sK910_skl,sK911_skl),sK911_skl,sK910_skl)=k1_realset1(u2_lattices(sK909_skl),sK911_skl)),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14630,f11793])).
% 132.62/17.51 fof(f14642,plain,(
% 132.62/17.51 u2_lattices(k8_filter_0(sK910_skl,sK911_skl))=k1_realset1(u2_lattices(sK909_skl),sK911_skl)),
% 132.62/17.51 inference(resolution,[status(thm)],[f14558,f11795])).
% 132.62/17.51 fof(f14644,plain,(
% 132.62/17.51 ~v10_lattices(sK910_skl)|~l3_lattices(sK910_skl)|sK806_skl(k8_filter_0(sK910_skl,sK911_skl),sK911_skl,sK910_skl)=u2_lattices(k8_filter_0(sK910_skl,sK911_skl))),
% 132.62/17.51 inference(backward_demodulation,[status(thm)],[f14642,f14631])).
% 132.62/17.51 fof(f14645,plain,(
% 132.62/17.51 ~v10_lattices(sK909_skl)|~l3_lattices(sK909_skl)|sK806_skl(k8_filter_0(sK909_skl,sK911_skl),sK911_skl,sK909_skl)=u2_lattices(k8_filter_0(sK910_skl,sK911_skl))),
% 132.62/17.51 inference(backward_demodulation,[status(thm)],[f14642,f14629])).
% 132.62/17.51 fof(f14647,plain,(
% 132.62/17.51 ~v10_lattices(sK909_skl)|~l3_lattices(sK909_skl)|u2_lattices(k8_filter_0(sK909_skl,sK911_skl))=u2_lattices(k8_filter_0(sK910_skl,sK911_skl))),
% 132.62/17.51 inference(backward_demodulation,[status(thm)],[f14642,f14284])).
% 132.62/17.51 fof(f14648,plain,(
% 132.62/17.51 ~l3_lattices(sK910_skl)|sK806_skl(k8_filter_0(sK910_skl,sK911_skl),sK911_skl,sK910_skl)=u2_lattices(k8_filter_0(sK910_skl,sK911_skl))),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14644,f11794])).
% 132.62/17.51 fof(f14649,plain,(
% 132.62/17.51 ~l3_lattices(sK909_skl)|sK806_skl(k8_filter_0(sK909_skl,sK911_skl),sK911_skl,sK909_skl)=u2_lattices(k8_filter_0(sK910_skl,sK911_skl))),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14645,f11791])).
% 132.62/17.51 fof(f14657,plain,(
% 132.62/17.51 ~l3_lattices(sK909_skl)|u2_lattices(k8_filter_0(sK909_skl,sK911_skl))=u2_lattices(k8_filter_0(sK910_skl,sK911_skl))),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14647,f11791])).
% 132.62/17.51 fof(f14725,plain,(
% 132.62/17.51 u1_lattices(k8_filter_0(sK909_skl,sK911_skl))=u1_lattices(k8_filter_0(sK910_skl,sK911_skl))),
% 132.62/17.51 inference(resolution,[status(thm)],[f14559,f11792])).
% 132.62/17.51 fof(f14729,plain,(
% 132.62/17.51 ~v10_lattices(sK910_skl)|~l3_lattices(sK910_skl)|sK807_skl(k8_filter_0(sK910_skl,sK911_skl),sK911_skl,sK910_skl)=u1_lattices(k8_filter_0(sK909_skl,sK911_skl))),
% 132.62/17.51 inference(backward_demodulation,[status(thm)],[f14725,f14579])).
% 132.62/17.51 fof(f14730,plain,(
% 132.62/17.51 ~v10_lattices(sK909_skl)|~l3_lattices(sK909_skl)|sK807_skl(k8_filter_0(sK909_skl,sK911_skl),sK911_skl,sK909_skl)=u1_lattices(k8_filter_0(sK909_skl,sK911_skl))),
% 132.62/17.51 inference(backward_demodulation,[status(thm)],[f14725,f14576])).
% 132.62/17.51 fof(f14744,plain,(
% 132.62/17.51 ~l3_lattices(sK910_skl)|sK807_skl(k8_filter_0(sK910_skl,sK911_skl),sK911_skl,sK910_skl)=u1_lattices(k8_filter_0(sK909_skl,sK911_skl))),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14729,f11794])).
% 132.62/17.51 fof(f14745,plain,(
% 132.62/17.51 ~l3_lattices(sK909_skl)|sK807_skl(k8_filter_0(sK909_skl,sK911_skl),sK911_skl,sK909_skl)=u1_lattices(k8_filter_0(sK909_skl,sK911_skl))),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14730,f11791])).
% 132.62/17.51 fof(f14802,plain,(
% 132.62/17.51 u2_lattices(k8_filter_0(sK909_skl,sK911_skl))=u2_lattices(k8_filter_0(sK910_skl,sK911_skl))),
% 132.62/17.51 inference(resolution,[status(thm)],[f14657,f11792])).
% 132.62/17.51 fof(f14812,plain,(
% 132.62/17.51 ~l3_lattices(sK909_skl)|sK806_skl(k8_filter_0(sK909_skl,sK911_skl),sK911_skl,sK909_skl)=u2_lattices(k8_filter_0(sK909_skl,sK911_skl))),
% 132.62/17.51 inference(backward_demodulation,[status(thm)],[f14802,f14649])).
% 132.62/17.51 fof(f14813,plain,(
% 132.62/17.51 ~l3_lattices(sK910_skl)|sK806_skl(k8_filter_0(sK910_skl,sK911_skl),sK911_skl,sK910_skl)=u2_lattices(k8_filter_0(sK909_skl,sK911_skl))),
% 132.62/17.51 inference(backward_demodulation,[status(thm)],[f14802,f14648])).
% 132.62/17.51 fof(f14836,plain,(
% 132.62/17.51 ~v10_lattices(sK909_skl)|~l3_lattices(sK909_skl)|k8_filter_0(sK909_skl,sK911_skl)=g3_lattices(sK911_skl,u2_lattices(k8_filter_0(sK909_skl,sK911_skl)),sK807_skl(k8_filter_0(sK909_skl,sK911_skl),sK911_skl,sK909_skl))),
% 132.62/17.51 inference(backward_demodulation,[status(thm)],[f14837,f14571])).
% 132.62/17.51 fof(f14837,plain,(
% 132.62/17.51 sK806_skl(k8_filter_0(sK909_skl,sK911_skl),sK911_skl,sK909_skl)=u2_lattices(k8_filter_0(sK909_skl,sK911_skl))),
% 132.62/17.51 inference(forward_subsumption_resolution,[status(thm)],[f14812,f11792])).
% 132.62/17.51 fof(f14839,plain,(
% 132.62/17.51 ~v10_lattices(sK910_skl)|~l3_lattices(sK910_skl)|k8_filter_0(sK910_skl,sK911_skl)=g3_lattices(sK911_skl,u2_lattices(k8_filter_0(sK909_skl,sK911_skl)),sK807_skl(k8_filter_0(sK910_skl,sK911_skl),sK911_skl,sK910_skl))),
% 132.62/17.51 inference(backward_demodulation,[status(thm)],[f14840,f14572])).
% 132.62/17.51 fof(f14840,plain,(
% 132.62/17.51 sK806_skl(k8_filter_0(sK910_skl,sK911_skl),sK911_skl,sK910_skl)=u2_lattices(k8_filter_0(sK909_skl,sK911_skl))),
% 49.23/17.63 inference(forward_subsumption_resolution,[status(thm)],[f14813,f11795])).
% 49.23/17.63 fof(f14843,plain,(
% 49.23/17.63 ~l3_lattices(sK909_skl)|k8_filter_0(sK909_skl,sK911_skl)=g3_lattices(sK911_skl,u2_lattices(k8_filter_0(sK909_skl,sK911_skl)),sK807_skl(k8_filter_0(sK909_skl,sK911_skl),sK911_skl,sK909_skl))),
% 49.23/17.63 inference(forward_subsumption_resolution,[status(thm)],[f14836,f11791])).
% 49.23/17.63 fof(f14845,plain,(
% 49.23/17.63 ~l3_lattices(sK910_skl)|k8_filter_0(sK910_skl,sK911_skl)=g3_lattices(sK911_skl,u2_lattices(k8_filter_0(sK909_skl,sK911_skl)),sK807_skl(k8_filter_0(sK910_skl,sK911_skl),sK911_skl,sK910_skl))),
% 49.23/17.63 inference(forward_subsumption_resolution,[status(thm)],[f14839,f11794])).
% 49.23/17.63 fof(f15178,plain,(
% 49.23/17.63 sK807_skl(k8_filter_0(sK910_skl,sK911_skl),sK911_skl,sK910_skl)=u1_lattices(k8_filter_0(sK909_skl,sK911_skl))),
% 49.23/17.63 inference(resolution,[status(thm)],[f14744,f11795])).
% 49.23/17.63 fof(f15181,plain,(
% 49.23/17.63 ~l3_lattices(sK910_skl)|k8_filter_0(sK910_skl,sK911_skl)=g3_lattices(sK911_skl,u2_lattices(k8_filter_0(sK909_skl,sK911_skl)),u1_lattices(k8_filter_0(sK909_skl,sK911_skl)))),
% 49.23/17.63 inference(backward_demodulation,[status(thm)],[f15178,f14845])).
% 49.23/17.63 fof(f15194,plain,(
% 49.23/17.63 k8_filter_0(sK910_skl,sK911_skl)=g3_lattices(sK911_skl,u2_lattices(k8_filter_0(sK909_skl,sK911_skl)),u1_lattices(k8_filter_0(sK909_skl,sK911_skl)))),
% 49.23/17.63 inference(forward_subsumption_resolution,[status(thm)],[f15181,f11795])).
% 49.23/17.63 fof(f15452,plain,(
% 49.23/17.63 sK807_skl(k8_filter_0(sK909_skl,sK911_skl),sK911_skl,sK909_skl)=u1_lattices(k8_filter_0(sK909_skl,sK911_skl))),
% 49.23/17.63 inference(resolution,[status(thm)],[f14745,f11792])).
% 49.23/17.63 fof(f15455,plain,(
% 49.23/17.63 ~l3_lattices(sK909_skl)|k8_filter_0(sK909_skl,sK911_skl)=g3_lattices(sK911_skl,u2_lattices(k8_filter_0(sK909_skl,sK911_skl)),u1_lattices(k8_filter_0(sK909_skl,sK911_skl)))),
% 49.23/17.63 inference(backward_demodulation,[status(thm)],[f15452,f14843])).
% 49.23/17.63 fof(f15459,plain,(
% 49.23/17.63 ~l3_lattices(sK909_skl)|k8_filter_0(sK909_skl,sK911_skl)=k8_filter_0(sK910_skl,sK911_skl)),
% 49.23/17.63 inference(forward_demodulation,[status(thm)],[f15194,f15455])).
% 49.23/17.63 fof(f15468,plain,(
% 49.23/17.63 ~k8_filter_0(sK909_skl,sK911_skl)=k8_filter_0(sK909_skl,sK911_skl)),
% 49.23/17.63 inference(backward_demodulation,[status(thm)],[f15491,f13925])).
% 49.23/17.63 fof(f15491,plain,(
% 49.23/17.63 k8_filter_0(sK909_skl,sK911_skl)=k8_filter_0(sK910_skl,sK911_skl)),
% 49.23/17.63 inference(forward_subsumption_resolution,[status(thm)],[f15459,f11792])).
% 49.23/17.63 fof(f15499,plain,(
% 49.23/17.63 $false),
% 49.23/17.63 inference(trivial_equality_resolution,[status(thm)],[f15468])).
% 49.23/17.63 % SZS output end CNFRefutation for theBenchmark.p
% 49.23/17.69 % Elapsed time: 17.202973 seconds
% 49.23/17.69 % CPU time: 134.072988 seconds
% 49.23/17.69 % Total memory used: 1.042 GB
% 49.23/17.69 % Net memory used: 988.919 MB
%------------------------------------------------------------------------------