%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT322+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:40 PM UTC 2026
% Result : Theorem 20.49s 8.05s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT322+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.38 % Computer : n008.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Sun Sep 20 23:38:15 UTC 2026
% 0.10/5.39 % CPUTime :
% 0.14/5.40 % Drodi V4.1.1
% 20.49/8.05 % Refutation found
% 20.49/8.05 % SZS status Theorem for theBenchmark: Theorem is valid
% 20.49/8.05 % SZS output start CNFRefutation for theBenchmark
% 20.49/8.05 fof(f1,conjecture,(
% 20.49/8.05 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& l3_lattices(A) )=> (! [B] :( m2_filter_2(B,A)=> ( ( B != k17_filter_2(A)& v1_filter_2(B,A) )<=> r2_filter_2(A,B) ) ) )) )),
% 20.49/8.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.49/8.05 fof(f2,negated_conjecture,(
% 20.49/8.05 ~((! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& l3_lattices(A) )=> (! [B] :( m2_filter_2(B,A)=> ( ( B != k17_filter_2(A)& v1_filter_2(B,A) )<=> r2_filter_2(A,B) ) ) )) ))),
% 20.49/8.05 inference(negated_conjecture,[status(cth)],[f1])).
% 20.49/8.05 fof(f3,axiom,(
% 20.49/8.05 (! [A] :( l3_lattices(A)=> ( v3_lattices(A)=> A = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) ) ) )),
% 20.49/8.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.49/8.05 fof(f15,axiom,(
% 20.49/8.05 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> k1_filter_0(A) = u1_struct_0(A) ) )),
% 20.49/8.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.49/8.05 fof(f16,axiom,(
% 20.49/8.05 (! [A] :( l3_lattices(A)=> k1_lattice2(A) = g3_lattices(u1_struct_0(A),u1_lattices(A),u2_lattices(A)) ) )),
% 20.49/8.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.49/8.05 fof(f17,axiom,(
% 20.49/8.05 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))=> k7_filter_2(A,B) = B ) )) )),
% 20.49/8.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.49/8.05 fof(f18,axiom,(
% 20.49/8.05 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> k17_filter_2(A) = u1_struct_0(A) ) )),
% 20.49/8.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.49/8.05 fof(f20,axiom,(
% 20.49/8.05 (! [A,B] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A)& m2_filter_2(B,A) )=> m1_filter_2(k15_filter_2(A,B),k1_lattice2(A)) ) )),
% 20.49/8.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.49/8.05 fof(f21,axiom,(
% 20.49/8.05 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> m2_filter_2(k17_filter_2(A),A) ) )),
% 20.49/8.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.49/8.05 fof(f24,axiom,(
% 20.49/8.05 (! [A] :( l3_lattices(A)=> ( v3_lattices(k1_lattice2(A))& l3_lattices(k1_lattice2(A)) ) ) )),
% 20.49/8.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.49/8.05 fof(f32,axiom,(
% 20.49/8.05 (! [A] :( l3_lattices(A)=> ( l1_lattices(A)& l2_lattices(A) ) ) )),
% 20.49/8.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.49/8.05 fof(f37,axiom,(
% 20.49/8.05 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m2_filter_2(B,A)=> ( ~ v1_xboole_0(B)& m2_lattice4(B,A) ) ) )) )),
% 20.49/8.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.49/8.05 fof(f38,axiom,(
% 20.49/8.05 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m2_lattice4(B,A)=> m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) )) )),
% 20.49/8.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.49/8.05 fof(f40,axiom,(
% 20.49/8.05 (! [A] :( l1_lattices(A)=> ( v1_funct_1(u1_lattices(A))& v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))& m2_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) )),
% 20.49/8.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.49/8.05 fof(f42,axiom,(
% 20.49/8.05 (! [A] :( l2_lattices(A)=> ( v1_funct_1(u2_lattices(A))& v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))& m2_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) )),
% 20.49/8.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.49/8.05 fof(f55,axiom,(
% 20.49/8.05 (! [A] :( ( ~ v3_struct_0(A)& l3_lattices(A) )=> ( ~ v3_struct_0(k1_lattice2(A))& v3_lattices(k1_lattice2(A)) ) ) )),
% 20.49/8.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.49/8.05 fof(f61,axiom,(
% 20.49/8.05 (! [A,B,C] :( ( ~ v1_xboole_0(A)& v1_funct_1(B)& v1_funct_2(B,k2_zfmisc_1(A,A),A)& m1_relset_1(B,k2_zfmisc_1(A,A),A)& v1_funct_1(C)& v1_funct_2(C,k2_zfmisc_1(A,A),A)& m1_relset_1(C,k2_zfmisc_1(A,A),A) )=> ( ~ v3_struct_0(g3_lattices(A,B,C))& v3_lattices(g3_lattices(A,B,C)) ) ) )),
% 20.49/8.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.49/8.05 fof(f62,axiom,(
% 20.49/8.05 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& l3_lattices(A) )=> ( ~ v3_struct_0(k1_lattice2(A))& v3_lattices(k1_lattice2(A))& v4_lattices(k1_lattice2(A))& v5_lattices(k1_lattice2(A))& v6_lattices(k1_lattice2(A))& v7_lattices(k1_lattice2(A))& v8_lattices(k1_lattice2(A))& v9_lattices(k1_lattice2(A))& v10_lattices(k1_lattice2(A))& v11_lattices(k1_lattice2(A))& v12_lattices(k1_lattice2(A))& v13_lattices(k1_lattice2(A))& v14_lattices(k1_lattice2(A))& v15_lattices(k1_lattice2(A))& v16_lattices(k1_lattice2(A))& v17_lattices(k1_lattice2(A)) ) ) )),
% 20.49/8.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.49/8.05 fof(f67,axiom,(
% 20.49/8.05 (! [A,B,C] :( ( v1_funct_1(B)& v1_funct_2(B,k2_zfmisc_1(A,A),A)& m1_relset_1(B,k2_zfmisc_1(A,A),A)& v1_funct_1(C)& v1_funct_2(C,k2_zfmisc_1(A,A),A)& m1_relset_1(C,k2_zfmisc_1(A,A),A) )=> (! [D,E,F] :( g3_lattices(A,B,C) = g3_lattices(D,E,F)=> ( A = D& B = E& C = F ) ) )) )),
% 20.49/8.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.49/8.05 fof(f85,axiom,(
% 20.49/8.05 (! [A,B] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A)& m2_filter_2(B,A) )=> k15_filter_2(A,B) = k7_filter_2(A,B) ) )),
% 20.49/8.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.49/8.05 fof(f87,axiom,(
% 20.49/8.05 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_filter_2(B,A)<=> m1_filter_0(B,A) ) )) )),
% 20.49/8.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.49/8.05 fof(f88,axiom,(
% 20.49/8.05 (! [A,B,C] :( m2_relset_1(C,A,B)<=> m1_relset_1(C,A,B) ) )),
% 20.49/8.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.49/8.05 fof(f92,axiom,(
% 20.49/8.05 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m2_filter_2(B,A)=> ( r2_filter_2(A,B)<=> v1_filter_0(k15_filter_2(A,B),k1_lattice2(A)) ) ) )) )),
% 20.49/8.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.49/8.05 fof(f94,axiom,(
% 20.49/8.05 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m2_filter_2(B,A)=> ( v1_filter_2(B,A)<=> v2_filter_0(k15_filter_2(A,B),k1_lattice2(A)) ) ) )) )),
% 20.49/8.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.49/8.05 fof(f96,axiom,(
% 20.49/8.05 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_filter_0(B,A)=> ( ( B != k1_filter_0(A)& v2_filter_0(B,A) )<=> v1_filter_0(B,A) ) ) )) )),
% 20.49/8.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.49/8.05 fof(f101,plain,(
% 20.49/8.05 (?[A]: ((((~v3_struct_0(A)&v10_lattices(A))&v17_lattices(A))&l3_lattices(A))&(?[B]: (m2_filter_2(B,A)&((~B=k17_filter_2(A)&v1_filter_2(B,A))<~>r2_filter_2(A,B))))))),
% 20.49/8.05 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 20.49/8.05 fof(f102,plain,(
% 20.49/8.05 ?[A]: ((((~v3_struct_0(A)&v10_lattices(A))&v17_lattices(A))&l3_lattices(A))&(?[B]: (m2_filter_2(B,A)&(((~B=k17_filter_2(A)&v1_filter_2(B,A))|r2_filter_2(A,B))&((B=k17_filter_2(A)|~v1_filter_2(B,A))|~r2_filter_2(A,B))))))),
% 20.49/8.05 inference(NNF_transformation,[status(thm)],[f101])).
% 20.49/8.05 fof(f103,plain,(
% 20.49/8.05 ((((~v3_struct_0(sK0_skl)&v10_lattices(sK0_skl))&v17_lattices(sK0_skl))&l3_lattices(sK0_skl))&(m2_filter_2(sK1_skl,sK0_skl)&(((~sK1_skl=k17_filter_2(sK0_skl)&v1_filter_2(sK1_skl,sK0_skl))|r2_filter_2(sK0_skl,sK1_skl))&((sK1_skl=k17_filter_2(sK0_skl)|~v1_filter_2(sK1_skl,sK0_skl))|~r2_filter_2(sK0_skl,sK1_skl)))))),
% 20.49/8.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl)],[f102])).
% 20.49/8.05 fof(f104,plain,(
% 20.49/8.05 ~v3_struct_0(sK0_skl)),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f103])).
% 20.49/8.05 fof(f105,plain,(
% 20.49/8.05 v10_lattices(sK0_skl)),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f103])).
% 20.49/8.05 fof(f106,plain,(
% 20.49/8.05 v17_lattices(sK0_skl)),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f103])).
% 20.49/8.05 fof(f107,plain,(
% 20.49/8.05 l3_lattices(sK0_skl)),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f103])).
% 20.49/8.05 fof(f108,plain,(
% 20.49/8.05 m2_filter_2(sK1_skl,sK0_skl)),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f103])).
% 20.49/8.05 fof(f109,plain,(
% 20.49/8.05 ~sK1_skl=k17_filter_2(sK0_skl)|r2_filter_2(sK0_skl,sK1_skl)),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f103])).
% 20.49/8.05 fof(f110,plain,(
% 20.49/8.05 v1_filter_2(sK1_skl,sK0_skl)|r2_filter_2(sK0_skl,sK1_skl)),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f103])).
% 20.49/8.05 fof(f111,plain,(
% 20.49/8.05 sK1_skl=k17_filter_2(sK0_skl)|~v1_filter_2(sK1_skl,sK0_skl)|~r2_filter_2(sK0_skl,sK1_skl)),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f103])).
% 20.49/8.05 fof(f112,plain,(
% 20.49/8.05 ![A]: (~l3_lattices(A)|(~v3_lattices(A)|A=g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A))))),
% 20.49/8.05 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 20.49/8.05 fof(f113,plain,(
% 20.49/8.05 ![X0]: (~l3_lattices(X0)|~v3_lattices(X0)|X0=g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f112])).
% 20.49/8.05 fof(f163,plain,(
% 20.49/8.05 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|k1_filter_0(A)=u1_struct_0(A))),
% 20.49/8.05 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 20.49/8.05 fof(f164,plain,(
% 20.49/8.05 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|k1_filter_0(X0)=u1_struct_0(X0))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f163])).
% 20.49/8.05 fof(f165,plain,(
% 20.49/8.05 ![A]: (~l3_lattices(A)|k1_lattice2(A)=g3_lattices(u1_struct_0(A),u1_lattices(A),u2_lattices(A)))),
% 20.49/8.05 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 20.49/8.05 fof(f166,plain,(
% 20.49/8.05 ![X0]: (~l3_lattices(X0)|k1_lattice2(X0)=g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f165])).
% 20.49/8.05 fof(f167,plain,(
% 20.49/8.05 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))|k7_filter_2(A,B)=B)))),
% 20.49/8.05 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 20.49/8.05 fof(f168,plain,(
% 20.49/8.05 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|k7_filter_2(X0,X1)=X1)),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f167])).
% 20.49/8.05 fof(f169,plain,(
% 20.49/8.05 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|k17_filter_2(A)=u1_struct_0(A))),
% 20.49/8.05 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 20.49/8.05 fof(f170,plain,(
% 20.49/8.05 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|k17_filter_2(X0)=u1_struct_0(X0))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f169])).
% 20.49/8.05 fof(f174,plain,(
% 20.49/8.05 ![A,B]: ((((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|~m2_filter_2(B,A))|m1_filter_2(k15_filter_2(A,B),k1_lattice2(A)))),
% 20.49/8.05 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 20.49/8.05 fof(f175,plain,(
% 20.49/8.05 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_filter_2(X1,X0)|m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0)))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f174])).
% 20.49/8.05 fof(f176,plain,(
% 20.49/8.05 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|m2_filter_2(k17_filter_2(A),A))),
% 20.49/8.05 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 20.49/8.05 fof(f177,plain,(
% 20.49/8.05 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|m2_filter_2(k17_filter_2(X0),X0))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f176])).
% 20.49/8.05 fof(f182,plain,(
% 20.49/8.05 ![A]: (~l3_lattices(A)|(v3_lattices(k1_lattice2(A))&l3_lattices(k1_lattice2(A))))),
% 20.49/8.05 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 20.49/8.05 fof(f183,plain,(
% 20.49/8.05 ![X0]: (~l3_lattices(X0)|v3_lattices(k1_lattice2(X0)))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f182])).
% 20.49/8.05 fof(f184,plain,(
% 20.49/8.05 ![X0]: (~l3_lattices(X0)|l3_lattices(k1_lattice2(X0)))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f182])).
% 20.49/8.05 fof(f191,plain,(
% 20.49/8.05 ![A]: (~l3_lattices(A)|(l1_lattices(A)&l2_lattices(A)))),
% 20.49/8.05 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 20.49/8.05 fof(f192,plain,(
% 20.49/8.05 ![X0]: (~l3_lattices(X0)|l1_lattices(X0))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f191])).
% 20.49/8.05 fof(f193,plain,(
% 20.49/8.05 ![X0]: (~l3_lattices(X0)|l2_lattices(X0))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f191])).
% 20.49/8.05 fof(f200,plain,(
% 20.49/8.05 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m2_filter_2(B,A)|(~v1_xboole_0(B)&m2_lattice4(B,A)))))),
% 20.49/8.05 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 20.49/8.05 fof(f201,plain,(
% 20.49/8.05 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_filter_2(X1,X0)|~v1_xboole_0(X1))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f200])).
% 20.49/8.05 fof(f202,plain,(
% 20.49/8.05 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_filter_2(X1,X0)|m2_lattice4(X1,X0))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f200])).
% 20.49/8.05 fof(f203,plain,(
% 20.49/8.05 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m2_lattice4(B,A)|m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))))))),
% 20.49/8.05 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 20.49/8.05 fof(f204,plain,(
% 20.49/8.05 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_lattice4(X1,X0)|m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f203])).
% 20.49/8.05 fof(f207,plain,(
% 20.49/8.05 ![A]: (~l1_lattices(A)|((v1_funct_1(u1_lattices(A))&v1_funct_2(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)))&m2_relset_1(u1_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))))),
% 20.49/8.05 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 20.49/8.05 fof(f208,plain,(
% 20.49/8.05 ![X0]: (~l1_lattices(X0)|v1_funct_1(u1_lattices(X0)))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f207])).
% 20.49/8.05 fof(f209,plain,(
% 20.49/8.05 ![X0]: (~l1_lattices(X0)|v1_funct_2(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f207])).
% 20.49/8.05 fof(f210,plain,(
% 20.49/8.05 ![X0]: (~l1_lattices(X0)|m2_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f207])).
% 20.49/8.05 fof(f211,plain,(
% 20.49/8.05 ![A]: (~l2_lattices(A)|((v1_funct_1(u2_lattices(A))&v1_funct_2(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)))&m2_relset_1(u2_lattices(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))))),
% 20.49/8.05 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 20.49/8.05 fof(f212,plain,(
% 20.49/8.05 ![X0]: (~l2_lattices(X0)|v1_funct_1(u2_lattices(X0)))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f211])).
% 20.49/8.05 fof(f213,plain,(
% 20.49/8.05 ![X0]: (~l2_lattices(X0)|v1_funct_2(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f211])).
% 20.49/8.05 fof(f214,plain,(
% 20.49/8.05 ![X0]: (~l2_lattices(X0)|m2_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f211])).
% 20.49/8.05 fof(f243,plain,(
% 20.49/8.05 ![A]: ((v3_struct_0(A)|~l3_lattices(A))|(~v3_struct_0(k1_lattice2(A))&v3_lattices(k1_lattice2(A))))),
% 20.49/8.05 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 20.49/8.05 fof(f244,plain,(
% 20.49/8.05 ![X0]: (v3_struct_0(X0)|~l3_lattices(X0)|~v3_struct_0(k1_lattice2(X0)))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f243])).
% 20.49/8.05 fof(f262,plain,(
% 20.49/8.05 ![A,B,C]: (((((((v1_xboole_0(A)|~v1_funct_1(B))|~v1_funct_2(B,k2_zfmisc_1(A,A),A))|~m1_relset_1(B,k2_zfmisc_1(A,A),A))|~v1_funct_1(C))|~v1_funct_2(C,k2_zfmisc_1(A,A),A))|~m1_relset_1(C,k2_zfmisc_1(A,A),A))|(~v3_struct_0(g3_lattices(A,B,C))&v3_lattices(g3_lattices(A,B,C))))),
% 20.49/8.05 inference(pre_NNF_transformation,[status(thm)],[f61])).
% 20.49/8.05 fof(f263,plain,(
% 20.49/8.05 ![X0,X1,X2]: (v1_xboole_0(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,k2_zfmisc_1(X0,X0),X0)|~m1_relset_1(X1,k2_zfmisc_1(X0,X0),X0)|~v1_funct_1(X2)|~v1_funct_2(X2,k2_zfmisc_1(X0,X0),X0)|~m1_relset_1(X2,k2_zfmisc_1(X0,X0),X0)|~v3_struct_0(g3_lattices(X0,X1,X2)))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f262])).
% 20.49/8.05 fof(f265,plain,(
% 20.49/8.05 ![A]: ((((v3_struct_0(A)|~v10_lattices(A))|~v17_lattices(A))|~l3_lattices(A))|(((((((((((((((~v3_struct_0(k1_lattice2(A))&v3_lattices(k1_lattice2(A)))&v4_lattices(k1_lattice2(A)))&v5_lattices(k1_lattice2(A)))&v6_lattices(k1_lattice2(A)))&v7_lattices(k1_lattice2(A)))&v8_lattices(k1_lattice2(A)))&v9_lattices(k1_lattice2(A)))&v10_lattices(k1_lattice2(A)))&v11_lattices(k1_lattice2(A)))&v12_lattices(k1_lattice2(A)))&v13_lattices(k1_lattice2(A)))&v14_lattices(k1_lattice2(A)))&v15_lattices(k1_lattice2(A)))&v16_lattices(k1_lattice2(A)))&v17_lattices(k1_lattice2(A))))),
% 20.49/8.05 inference(pre_NNF_transformation,[status(thm)],[f62])).
% 20.49/8.05 fof(f274,plain,(
% 20.49/8.05 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~v17_lattices(X0)|~l3_lattices(X0)|v10_lattices(k1_lattice2(X0)))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f265])).
% 20.49/8.05 fof(f281,plain,(
% 20.49/8.05 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~v17_lattices(X0)|~l3_lattices(X0)|v17_lattices(k1_lattice2(X0)))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f265])).
% 20.49/8.05 fof(f306,plain,(
% 20.49/8.05 ![A,B,C]: ((((((~v1_funct_1(B)|~v1_funct_2(B,k2_zfmisc_1(A,A),A))|~m1_relset_1(B,k2_zfmisc_1(A,A),A))|~v1_funct_1(C))|~v1_funct_2(C,k2_zfmisc_1(A,A),A))|~m1_relset_1(C,k2_zfmisc_1(A,A),A))|(![D,E,F]: (~g3_lattices(A,B,C)=g3_lattices(D,E,F)|((A=D&B=E)&C=F))))),
% 20.49/8.05 inference(pre_NNF_transformation,[status(thm)],[f67])).
% 20.49/8.05 fof(f307,plain,(
% 20.49/8.05 ![X0,X1,X2,X3,X4,X5]: (~v1_funct_1(X0)|~v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)|~m1_relset_1(X0,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X2)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~g3_lattices(X1,X0,X2)=g3_lattices(X3,X4,X5)|X1=X3)),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f306])).
% 20.49/8.05 fof(f309,plain,(
% 20.49/8.05 ![X0,X1,X2,X3,X4,X5]: (~v1_funct_1(X0)|~v1_funct_2(X0,k2_zfmisc_1(X1,X1),X1)|~m1_relset_1(X0,k2_zfmisc_1(X1,X1),X1)|~v1_funct_1(X2)|~v1_funct_2(X2,k2_zfmisc_1(X1,X1),X1)|~m1_relset_1(X2,k2_zfmisc_1(X1,X1),X1)|~g3_lattices(X1,X0,X2)=g3_lattices(X3,X4,X5)|X2=X5)),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f306])).
% 20.49/8.05 fof(f422,plain,(
% 20.49/8.05 ![A,B]: ((((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|~m2_filter_2(B,A))|k15_filter_2(A,B)=k7_filter_2(A,B))),
% 20.49/8.05 inference(pre_NNF_transformation,[status(thm)],[f85])).
% 20.49/8.05 fof(f423,plain,(
% 20.49/8.05 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_filter_2(X1,X0)|k15_filter_2(X0,X1)=k7_filter_2(X0,X1))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f422])).
% 20.49/8.05 fof(f426,plain,(
% 20.49/8.05 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (m1_filter_2(B,A)<=>m1_filter_0(B,A))))),
% 20.49/8.05 inference(pre_NNF_transformation,[status(thm)],[f87])).
% 20.49/8.05 fof(f427,plain,(
% 20.49/8.05 ![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)))))),
% 20.49/8.05 inference(NNF_transformation,[status(thm)],[f426])).
% 20.49/8.05 fof(f428,plain,(
% 20.49/8.05 ![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)))))),
% 20.49/8.05 inference(miniscoping,[status(thm)],[f427])).
% 20.49/8.05 fof(f429,plain,(
% 20.49/8.05 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_2(X1,X0)|m1_filter_0(X1,X0))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f428])).
% 20.49/8.05 fof(f431,plain,(
% 20.49/8.05 ![A,B,C]: ((~m2_relset_1(C,A,B)|m1_relset_1(C,A,B))&(m2_relset_1(C,A,B)|~m1_relset_1(C,A,B)))),
% 20.49/8.05 inference(NNF_transformation,[status(thm)],[f88])).
% 20.49/8.05 fof(f432,plain,(
% 20.49/8.05 (![A,B,C]: (~m2_relset_1(C,A,B)|m1_relset_1(C,A,B)))&(![A,B,C]: (m2_relset_1(C,A,B)|~m1_relset_1(C,A,B)))),
% 20.49/8.05 inference(miniscoping,[status(thm)],[f431])).
% 20.49/8.05 fof(f433,plain,(
% 20.49/8.05 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_relset_1(X0,X1,X2))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f432])).
% 20.49/8.05 fof(f441,plain,(
% 20.49/8.05 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m2_filter_2(B,A)|(r2_filter_2(A,B)<=>v1_filter_0(k15_filter_2(A,B),k1_lattice2(A))))))),
% 20.49/8.05 inference(pre_NNF_transformation,[status(thm)],[f92])).
% 20.49/8.05 fof(f442,plain,(
% 20.49/8.05 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m2_filter_2(B,A)|((~r2_filter_2(A,B)|v1_filter_0(k15_filter_2(A,B),k1_lattice2(A)))&(r2_filter_2(A,B)|~v1_filter_0(k15_filter_2(A,B),k1_lattice2(A)))))))),
% 20.49/8.05 inference(NNF_transformation,[status(thm)],[f441])).
% 20.49/8.05 fof(f443,plain,(
% 20.49/8.05 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_filter_2(X1,X0)|~r2_filter_2(X0,X1)|v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f442])).
% 20.49/8.05 fof(f444,plain,(
% 20.49/8.05 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_filter_2(X1,X0)|r2_filter_2(X0,X1)|~v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f442])).
% 20.49/8.05 fof(f449,plain,(
% 20.49/8.05 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m2_filter_2(B,A)|(v1_filter_2(B,A)<=>v2_filter_0(k15_filter_2(A,B),k1_lattice2(A))))))),
% 20.49/8.05 inference(pre_NNF_transformation,[status(thm)],[f94])).
% 20.49/8.05 fof(f450,plain,(
% 20.49/8.05 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m2_filter_2(B,A)|((~v1_filter_2(B,A)|v2_filter_0(k15_filter_2(A,B),k1_lattice2(A)))&(v1_filter_2(B,A)|~v2_filter_0(k15_filter_2(A,B),k1_lattice2(A)))))))),
% 20.49/8.05 inference(NNF_transformation,[status(thm)],[f449])).
% 20.49/8.05 fof(f451,plain,(
% 20.49/8.05 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_filter_2(X1,X0)|~v1_filter_2(X1,X0)|v2_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f450])).
% 20.49/8.05 fof(f452,plain,(
% 20.49/8.05 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_filter_2(X1,X0)|v1_filter_2(X1,X0)|~v2_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f450])).
% 20.49/8.05 fof(f456,plain,(
% 20.49/8.05 ![A]: ((((v3_struct_0(A)|~v10_lattices(A))|~v17_lattices(A))|~l3_lattices(A))|(![B]: (~m1_filter_0(B,A)|((~B=k1_filter_0(A)&v2_filter_0(B,A))<=>v1_filter_0(B,A)))))),
% 20.49/8.05 inference(pre_NNF_transformation,[status(thm)],[f96])).
% 20.49/8.05 fof(f457,plain,(
% 20.49/8.05 ![A]: ((((v3_struct_0(A)|~v10_lattices(A))|~v17_lattices(A))|~l3_lattices(A))|(![B]: (~m1_filter_0(B,A)|(((B=k1_filter_0(A)|~v2_filter_0(B,A))|v1_filter_0(B,A))&((~B=k1_filter_0(A)&v2_filter_0(B,A))|~v1_filter_0(B,A))))))),
% 20.49/8.05 inference(NNF_transformation,[status(thm)],[f456])).
% 20.49/8.05 fof(f458,plain,(
% 20.49/8.05 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~v17_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|X1=k1_filter_0(X0)|~v2_filter_0(X1,X0)|v1_filter_0(X1,X0))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f457])).
% 20.49/8.05 fof(f459,plain,(
% 20.49/8.05 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~v17_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|~X1=k1_filter_0(X0)|~v1_filter_0(X1,X0))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f457])).
% 20.49/8.05 fof(f460,plain,(
% 20.49/8.05 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~v17_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|v2_filter_0(X1,X0)|~v1_filter_0(X1,X0))),
% 20.49/8.05 inference(cnf_transformation,[status(thm)],[f457])).
% 20.49/8.05 fof(f473,plain,(
% 20.49/8.05 v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|k17_filter_2(sK0_skl)=u1_struct_0(sK0_skl)),
% 20.49/8.05 inference(resolution,[status(thm)],[f170,f105])).
% 20.49/8.05 fof(f475,plain,(
% 20.49/8.05 ~l3_lattices(sK0_skl)|k17_filter_2(sK0_skl)=u1_struct_0(sK0_skl)),
% 20.49/8.05 inference(forward_subsumption_resolution,[status(thm)],[f473,f104])).
% 20.49/8.05 fof(f480,plain,(
% 20.49/8.05 sK1_skl=u1_struct_0(sK0_skl)|~v1_filter_2(sK1_skl,sK0_skl)|~r2_filter_2(sK0_skl,sK1_skl)),
% 20.49/8.05 inference(backward_demodulation,[status(thm)],[f482,f111])).
% 20.49/8.05 fof(f481,plain,(
% 20.49/8.05 ~sK1_skl=u1_struct_0(sK0_skl)|r2_filter_2(sK0_skl,sK1_skl)),
% 20.49/8.05 inference(backward_demodulation,[status(thm)],[f482,f109])).
% 20.49/8.05 fof(f482,plain,(
% 20.49/8.05 k17_filter_2(sK0_skl)=u1_struct_0(sK0_skl)),
% 20.49/8.05 inference(forward_subsumption_resolution,[status(thm)],[f475,f107])).
% 20.49/8.05 fof(f484,plain,(
% 20.49/8.05 v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|m2_filter_2(k17_filter_2(sK0_skl),sK0_skl)),
% 20.49/8.05 inference(resolution,[status(thm)],[f177,f105])).
% 20.49/8.05 fof(f489,plain,(
% 20.49/8.05 v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|m2_filter_2(u1_struct_0(sK0_skl),sK0_skl)),
% 20.49/8.05 inference(forward_demodulation,[status(thm)],[f482,f484])).
% 20.49/8.05 fof(f490,plain,(
% 20.49/8.05 ~l3_lattices(sK0_skl)|m2_filter_2(u1_struct_0(sK0_skl),sK0_skl)),
% 20.49/8.05 inference(forward_subsumption_resolution,[status(thm)],[f489,f104])).
% 20.49/8.05 fof(f494,plain,(
% 20.49/8.05 m2_filter_2(u1_struct_0(sK0_skl),sK0_skl)),
% 20.49/8.05 inference(forward_subsumption_resolution,[status(thm)],[f490,f107])).
% 20.49/8.05 fof(f495,plain,(
% 20.49/8.05 ![X0]: (v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|~m2_filter_2(X0,sK0_skl)|~v1_xboole_0(X0))),
% 20.49/8.05 inference(resolution,[status(thm)],[f201,f105])).
% 20.49/8.05 fof(f500,plain,(
% 20.49/8.05 ![X0]: (~l3_lattices(sK0_skl)|~m2_filter_2(X0,sK0_skl)|~v1_xboole_0(X0))),
% 20.49/8.05 inference(forward_subsumption_resolution,[status(thm)],[f495,f104])).
% 20.49/8.05 fof(f512,plain,(
% 20.49/8.05 ![X0]: (~m2_filter_2(X0,sK0_skl)|~v1_xboole_0(X0))),
% 20.49/8.05 inference(forward_subsumption_resolution,[status(thm)],[f500,f107])).
% 20.49/8.05 fof(f513,plain,(
% 20.49/8.05 ~v1_xboole_0(u1_struct_0(sK0_skl))),
% 20.49/8.05 inference(resolution,[status(thm)],[f512,f494])).
% 20.49/8.05 fof(f519,plain,(
% 20.49/8.05 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|v10_lattices(k1_lattice2(sK0_skl))),
% 20.49/8.05 inference(resolution,[status(thm)],[f274,f106])).
% 20.49/8.05 fof(f520,plain,(
% 20.49/8.05 ~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|v10_lattices(k1_lattice2(sK0_skl))),
% 20.49/8.05 inference(forward_subsumption_resolution,[status(thm)],[f519,f104])).
% 20.49/8.05 fof(f521,plain,(
% 20.49/8.05 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|v17_lattices(k1_lattice2(sK0_skl))),
% 20.49/8.05 inference(resolution,[status(thm)],[f281,f106])).
% 20.49/8.05 fof(f522,plain,(
% 20.49/8.05 ~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|v17_lattices(k1_lattice2(sK0_skl))),
% 20.49/8.05 inference(forward_subsumption_resolution,[status(thm)],[f521,f104])).
% 20.49/8.05 fof(f543,plain,(
% 20.49/8.05 ~l3_lattices(sK0_skl)|v10_lattices(k1_lattice2(sK0_skl))),
% 20.49/8.05 inference(forward_subsumption_resolution,[status(thm)],[f520,f105])).
% 20.49/8.05 fof(f544,plain,(
% 20.49/8.05 v10_lattices(k1_lattice2(sK0_skl))),
% 20.49/8.05 inference(resolution,[status(thm)],[f543,f107])).
% 20.49/8.05 fof(f600,plain,(
% 20.49/8.05 ~l3_lattices(sK0_skl)|v17_lattices(k1_lattice2(sK0_skl))),
% 20.49/8.05 inference(forward_subsumption_resolution,[status(thm)],[f522,f105])).
% 20.49/8.05 fof(f601,plain,(
% 20.49/8.05 v17_lattices(k1_lattice2(sK0_skl))),
% 20.49/8.05 inference(resolution,[status(thm)],[f600,f107])).
% 20.49/8.05 fof(f611,plain,(
% 20.49/8.05 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~m2_filter_2(sK1_skl,sK0_skl)|v2_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))|r2_filter_2(sK0_skl,sK1_skl)),
% 20.49/8.05 inference(resolution,[status(thm)],[f451,f110])).
% 20.49/8.05 fof(f612,plain,(
% 20.49/8.05 ~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~m2_filter_2(sK1_skl,sK0_skl)|v2_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))|r2_filter_2(sK0_skl,sK1_skl)),
% 20.49/8.05 inference(forward_subsumption_resolution,[status(thm)],[f611,f104])).
% 20.49/8.05 fof(f643,plain,(
% 20.49/8.05 ~l3_lattices(sK0_skl)|~m2_filter_2(sK1_skl,sK0_skl)|v2_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))|r2_filter_2(sK0_skl,sK1_skl)),
% 20.49/8.05 inference(forward_subsumption_resolution,[status(thm)],[f612,f105])).
% 20.49/8.05 fof(f646,plain,(
% 20.49/8.05 ~l3_lattices(sK0_skl)|~m2_filter_2(sK1_skl,sK0_skl)|v2_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))|v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~m2_filter_2(sK1_skl,sK0_skl)|v1_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))),
% 20.49/8.05 inference(resolution,[status(thm)],[f643,f443])).
% 20.49/8.05 fof(f649,plain,(
% 20.49/8.05 ~l3_lattices(sK0_skl)|~m2_filter_2(sK1_skl,sK0_skl)|v2_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))|v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|v1_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))),
% 20.49/8.05 inference(duplicate_literals_removal,[status(thm)],[f646])).
% 20.49/8.05 fof(f650,plain,(
% 20.49/8.05 ~m2_filter_2(sK1_skl,sK0_skl)|v2_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))|v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|v1_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))),
% 20.49/8.05 inference(forward_subsumption_resolution,[status(thm)],[f649,f107])).
% 20.49/8.05 fof(f828,plain,(
% 20.49/8.05 v2_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))|v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|v1_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))),
% 20.49/8.05 inference(forward_subsumption_resolution,[status(thm)],[f650,f108])).
% 20.49/8.05 fof(f913,plain,(
% 20.49/8.05 k1_lattice2(sK0_skl)=g3_lattices(u1_struct_0(sK0_skl),u1_lattices(sK0_skl),u2_lattices(sK0_skl))),
% 20.49/8.05 inference(resolution,[status(thm)],[f166,f107])).
% 20.49/8.05 fof(f1073,plain,(
% 20.49/8.05 ![X0]: (v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|k7_filter_2(sK0_skl,X0)=X0)),
% 20.49/8.05 inference(resolution,[status(thm)],[f168,f105])).
% 20.49/8.05 fof(f1085,plain,(
% 20.49/8.05 ![X0]: (~l3_lattices(sK0_skl)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|k7_filter_2(sK0_skl,X0)=X0)),
% 20.49/8.05 inference(forward_subsumption_resolution,[status(thm)],[f1073,f104])).
% 20.49/8.05 fof(f1159,plain,(
% 20.49/8.05 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m1_filter_2(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))),
% 20.49/8.05 inference(resolution,[status(thm)],[f175,f108])).
% 20.49/8.05 fof(f1170,plain,(
% 20.49/8.05 ~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m1_filter_2(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))),
% 20.49/8.05 inference(forward_subsumption_resolution,[status(thm)],[f1159,f104])).
% 20.49/8.05 fof(f1224,plain,(
% 20.49/8.05 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|k7_filter_2(sK0_skl,X0)=X0)),
% 20.49/8.05 inference(forward_subsumption_resolution,[status(thm)],[f1085,f107])).
% 20.49/8.05 fof(f1263,plain,(
% 20.49/8.05 v3_lattices(k1_lattice2(sK0_skl))),
% 20.49/8.05 inference(resolution,[status(thm)],[f183,f107])).
% 20.49/8.05 fof(f1271,plain,(
% 20.49/8.05 l3_lattices(k1_lattice2(sK0_skl))),
% 20.49/8.05 inference(resolution,[status(thm)],[f184,f107])).
% 20.49/8.06 fof(f1272,plain,(
% 20.49/8.06 ~l3_lattices(k1_lattice2(sK0_skl))|k1_lattice2(sK0_skl)=g3_lattices(u1_struct_0(k1_lattice2(sK0_skl)),u2_lattices(k1_lattice2(sK0_skl)),u1_lattices(k1_lattice2(sK0_skl)))),
% 20.49/8.06 inference(resolution,[status(thm)],[f1263,f113])).
% 20.49/8.06 fof(f1283,plain,(
% 20.49/8.06 v3_struct_0(k1_lattice2(sK0_skl))|~v10_lattices(k1_lattice2(sK0_skl))|k1_filter_0(k1_lattice2(sK0_skl))=u1_struct_0(k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(resolution,[status(thm)],[f1271,f164])).
% 20.49/8.06 fof(f1291,plain,(
% 20.49/8.06 v3_struct_0(k1_lattice2(sK0_skl))|k1_filter_0(k1_lattice2(sK0_skl))=u1_struct_0(k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f1283,f544])).
% 20.49/8.06 fof(f1380,plain,(
% 20.49/8.06 l1_lattices(sK0_skl)),
% 20.49/8.06 inference(resolution,[status(thm)],[f192,f107])).
% 20.49/8.06 fof(f1382,plain,(
% 20.49/8.06 ~l3_lattices(sK0_skl)|m1_filter_2(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f1170,f105])).
% 20.49/8.06 fof(f1383,plain,(
% 20.49/8.06 m1_filter_2(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(resolution,[status(thm)],[f1382,f107])).
% 20.49/8.06 fof(f1454,plain,(
% 20.49/8.06 l2_lattices(sK0_skl)),
% 20.49/8.06 inference(resolution,[status(thm)],[f193,f107])).
% 20.49/8.06 fof(f1621,plain,(
% 20.49/8.06 ![X0]: (v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|~m2_filter_2(X0,sK0_skl)|m2_lattice4(X0,sK0_skl))),
% 20.49/8.06 inference(resolution,[status(thm)],[f202,f105])).
% 20.49/8.06 fof(f1641,plain,(
% 20.49/8.06 ![X0]: (~l3_lattices(sK0_skl)|~m2_filter_2(X0,sK0_skl)|m2_lattice4(X0,sK0_skl))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f1621,f104])).
% 20.49/8.06 fof(f1741,plain,(
% 20.49/8.06 ![X0]: (v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|~m2_lattice4(X0,sK0_skl)|m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 20.49/8.06 inference(resolution,[status(thm)],[f204,f105])).
% 20.49/8.06 fof(f1761,plain,(
% 20.49/8.06 ![X0]: (~l3_lattices(sK0_skl)|~m2_lattice4(X0,sK0_skl)|m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f1741,f104])).
% 20.49/8.06 fof(f1781,plain,(
% 20.49/8.06 v1_funct_1(u1_lattices(sK0_skl))),
% 20.49/8.06 inference(resolution,[status(thm)],[f208,f1380])).
% 20.49/8.06 fof(f1889,plain,(
% 20.49/8.06 v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))),
% 20.49/8.06 inference(resolution,[status(thm)],[f209,f1380])).
% 20.49/8.06 fof(f1902,plain,(
% 20.49/8.06 m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))),
% 20.49/8.06 inference(resolution,[status(thm)],[f210,f1380])).
% 20.49/8.06 fof(f1912,plain,(
% 20.49/8.06 v1_funct_1(u2_lattices(sK0_skl))),
% 20.49/8.06 inference(resolution,[status(thm)],[f212,f1454])).
% 20.49/8.06 fof(f1940,plain,(
% 20.49/8.06 v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))),
% 20.49/8.06 inference(resolution,[status(thm)],[f213,f1454])).
% 20.49/8.06 fof(f1953,plain,(
% 20.49/8.06 m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))),
% 20.49/8.06 inference(resolution,[status(thm)],[f214,f1454])).
% 20.49/8.06 fof(f2410,plain,(
% 20.49/8.06 ![X0]: (~m2_filter_2(X0,sK0_skl)|m2_lattice4(X0,sK0_skl))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f1641,f107])).
% 20.49/8.06 fof(f2415,plain,(
% 20.49/8.06 m2_lattice4(sK1_skl,sK0_skl)),
% 20.49/8.06 inference(resolution,[status(thm)],[f2410,f108])).
% 20.49/8.06 fof(f2557,plain,(
% 20.49/8.06 ![X0]: (~m2_lattice4(X0,sK0_skl)|m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f1761,f107])).
% 20.49/8.06 fof(f2559,plain,(
% 20.49/8.06 m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 20.49/8.06 inference(resolution,[status(thm)],[f2557,f2415])).
% 20.49/8.06 fof(f2563,plain,(
% 20.49/8.06 k7_filter_2(sK0_skl,sK1_skl)=sK1_skl),
% 20.49/8.06 inference(resolution,[status(thm)],[f2559,f1224])).
% 20.49/8.06 fof(f2610,plain,(
% 20.49/8.06 v1_xboole_0(u1_struct_0(sK0_skl))|~v1_funct_1(u1_lattices(sK0_skl))|~v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~v1_funct_1(u2_lattices(sK0_skl))|~v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~v3_struct_0(k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(paramodulation,[status(thm)],[f913,f263])).
% 20.49/8.06 fof(f2611,plain,(
% 20.49/8.06 ~v1_funct_1(u1_lattices(sK0_skl))|~v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~v1_funct_1(u2_lattices(sK0_skl))|~v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~v3_struct_0(k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f2610,f513])).
% 20.49/8.06 fof(f3174,plain,(
% 20.49/8.06 k1_lattice2(sK0_skl)=g3_lattices(u1_struct_0(k1_lattice2(sK0_skl)),u2_lattices(k1_lattice2(sK0_skl)),u1_lattices(k1_lattice2(sK0_skl)))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f1272,f1271])).
% 20.49/8.06 fof(f3656,plain,(
% 20.49/8.06 ![X0,X1,X2]: (~v1_funct_1(u1_lattices(sK0_skl))|~v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~v1_funct_1(u2_lattices(sK0_skl))|~v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~k1_lattice2(sK0_skl)=g3_lattices(X0,X1,X2)|u1_struct_0(sK0_skl)=X0)),
% 20.49/8.06 inference(paramodulation,[status(thm)],[f913,f307])).
% 20.49/8.06 fof(f3661,plain,(
% 20.49/8.06 ![X0,X1,X2]: (~v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~v1_funct_1(u2_lattices(sK0_skl))|~v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~k1_lattice2(sK0_skl)=g3_lattices(X0,X1,X2)|u1_struct_0(sK0_skl)=X0)),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f3656,f1781])).
% 20.49/8.06 fof(f3684,plain,(
% 20.49/8.06 ![X0,X1,X2]: (~v1_funct_1(u1_lattices(sK0_skl))|~v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~v1_funct_1(u2_lattices(sK0_skl))|~v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~k1_lattice2(sK0_skl)=g3_lattices(X0,X1,X2)|u2_lattices(sK0_skl)=X2)),
% 20.49/8.06 inference(paramodulation,[status(thm)],[f913,f309])).
% 20.49/8.06 fof(f3691,plain,(
% 20.49/8.06 ![X0,X1,X2]: (~v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~v1_funct_1(u2_lattices(sK0_skl))|~v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~k1_lattice2(sK0_skl)=g3_lattices(X0,X1,X2)|u2_lattices(sK0_skl)=X2)),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f3684,f1781])).
% 20.49/8.06 fof(f3753,plain,(
% 20.49/8.06 k1_filter_0(k1_lattice2(sK0_skl))=u1_struct_0(k1_lattice2(sK0_skl))|v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)),
% 20.49/8.06 inference(resolution,[status(thm)],[f1291,f244])).
% 20.49/8.06 fof(f3754,plain,(
% 20.49/8.06 k1_filter_0(k1_lattice2(sK0_skl))=u1_struct_0(k1_lattice2(sK0_skl))|~l3_lattices(sK0_skl)),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f3753,f104])).
% 20.49/8.06 fof(f3921,plain,(
% 20.49/8.06 ![X0]: (v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|~m2_filter_2(X0,sK0_skl)|k15_filter_2(sK0_skl,X0)=k7_filter_2(sK0_skl,X0))),
% 20.49/8.06 inference(resolution,[status(thm)],[f423,f105])).
% 20.49/8.06 fof(f3960,plain,(
% 20.49/8.06 ![X0]: (~l3_lattices(sK0_skl)|~m2_filter_2(X0,sK0_skl)|k15_filter_2(sK0_skl,X0)=k7_filter_2(sK0_skl,X0))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f3921,f104])).
% 20.49/8.06 fof(f4060,plain,(
% 20.49/8.06 ![X0]: (v3_struct_0(k1_lattice2(sK0_skl))|~v10_lattices(k1_lattice2(sK0_skl))|~m1_filter_2(X0,k1_lattice2(sK0_skl))|m1_filter_0(X0,k1_lattice2(sK0_skl)))),
% 20.49/8.06 inference(resolution,[status(thm)],[f429,f1271])).
% 20.49/8.06 fof(f4080,plain,(
% 20.49/8.06 ![X0]: (v3_struct_0(k1_lattice2(sK0_skl))|~m1_filter_2(X0,k1_lattice2(sK0_skl))|m1_filter_0(X0,k1_lattice2(sK0_skl)))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f4060,f544])).
% 20.49/8.06 fof(f4098,plain,(
% 20.49/8.06 ![X0]: (~m2_filter_2(X0,sK0_skl)|k15_filter_2(sK0_skl,X0)=k7_filter_2(sK0_skl,X0))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f3960,f107])).
% 20.49/8.06 fof(f4104,plain,(
% 20.49/8.06 k15_filter_2(sK0_skl,sK1_skl)=k7_filter_2(sK0_skl,sK1_skl)),
% 20.49/8.06 inference(resolution,[status(thm)],[f4098,f108])).
% 20.49/8.06 fof(f4117,plain,(
% 20.49/8.06 k15_filter_2(sK0_skl,sK1_skl)=sK1_skl),
% 20.49/8.06 inference(forward_demodulation,[status(thm)],[f2563,f4104])).
% 20.49/8.06 fof(f4118,plain,(
% 20.49/8.06 m1_filter_2(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(backward_demodulation,[status(thm)],[f4117,f1383])).
% 20.49/8.06 fof(f4119,plain,(
% 20.49/8.06 v2_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))|v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(backward_demodulation,[status(thm)],[f4117,f828])).
% 20.49/8.06 fof(f4121,plain,(
% 20.49/8.06 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~m2_filter_2(sK1_skl,sK0_skl)|v1_filter_2(sK1_skl,sK0_skl)|~v2_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(paramodulation,[status(thm)],[f4117,f452])).
% 20.49/8.06 fof(f4122,plain,(
% 20.49/8.06 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~m2_filter_2(sK1_skl,sK0_skl)|r2_filter_2(sK0_skl,sK1_skl)|~v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(paramodulation,[status(thm)],[f4117,f444])).
% 20.49/8.06 fof(f4123,plain,(
% 20.49/8.06 v2_filter_0(sK1_skl,k1_lattice2(sK0_skl))|v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(forward_demodulation,[status(thm)],[f4117,f4119])).
% 20.49/8.06 fof(f4124,plain,(
% 20.49/8.06 v2_filter_0(sK1_skl,k1_lattice2(sK0_skl))|~v10_lattices(sK0_skl)|v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f4123,f104])).
% 20.49/8.06 fof(f4125,plain,(
% 20.49/8.06 ~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~m2_filter_2(sK1_skl,sK0_skl)|v1_filter_2(sK1_skl,sK0_skl)|~v2_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f4121,f104])).
% 20.49/8.06 fof(f4126,plain,(
% 20.49/8.06 ~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~m2_filter_2(sK1_skl,sK0_skl)|r2_filter_2(sK0_skl,sK1_skl)|~v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f4122,f104])).
% 20.49/8.06 fof(f4469,plain,(
% 20.49/8.06 ![X0]: (v3_struct_0(k1_lattice2(sK0_skl))|~v10_lattices(k1_lattice2(sK0_skl))|~v17_lattices(k1_lattice2(sK0_skl))|~m1_filter_0(X0,k1_lattice2(sK0_skl))|X0=k1_filter_0(k1_lattice2(sK0_skl))|~v2_filter_0(X0,k1_lattice2(sK0_skl))|v1_filter_0(X0,k1_lattice2(sK0_skl)))),
% 20.49/8.06 inference(resolution,[status(thm)],[f458,f1271])).
% 20.49/8.06 fof(f4496,plain,(
% 20.49/8.06 ![X0]: (v3_struct_0(k1_lattice2(sK0_skl))|~v17_lattices(k1_lattice2(sK0_skl))|~m1_filter_0(X0,k1_lattice2(sK0_skl))|X0=k1_filter_0(k1_lattice2(sK0_skl))|~v2_filter_0(X0,k1_lattice2(sK0_skl))|v1_filter_0(X0,k1_lattice2(sK0_skl)))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f4469,f544])).
% 20.49/8.06 fof(f4539,plain,(
% 20.49/8.06 ![X0]: (v3_struct_0(k1_lattice2(sK0_skl))|~v10_lattices(k1_lattice2(sK0_skl))|~v17_lattices(k1_lattice2(sK0_skl))|~m1_filter_0(X0,k1_lattice2(sK0_skl))|~X0=k1_filter_0(k1_lattice2(sK0_skl))|~v1_filter_0(X0,k1_lattice2(sK0_skl)))),
% 20.49/8.06 inference(resolution,[status(thm)],[f459,f1271])).
% 20.49/8.06 fof(f4566,plain,(
% 20.49/8.06 ![X0]: (v3_struct_0(k1_lattice2(sK0_skl))|~v17_lattices(k1_lattice2(sK0_skl))|~m1_filter_0(X0,k1_lattice2(sK0_skl))|~X0=k1_filter_0(k1_lattice2(sK0_skl))|~v1_filter_0(X0,k1_lattice2(sK0_skl)))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f4539,f544])).
% 20.49/8.06 fof(f4623,plain,(
% 20.49/8.06 ![X0]: (v3_struct_0(k1_lattice2(sK0_skl))|~v10_lattices(k1_lattice2(sK0_skl))|~v17_lattices(k1_lattice2(sK0_skl))|~m1_filter_0(X0,k1_lattice2(sK0_skl))|v2_filter_0(X0,k1_lattice2(sK0_skl))|~v1_filter_0(X0,k1_lattice2(sK0_skl)))),
% 20.49/8.06 inference(resolution,[status(thm)],[f460,f1271])).
% 20.49/8.06 fof(f4648,plain,(
% 20.49/8.06 ![X0]: (v3_struct_0(k1_lattice2(sK0_skl))|~v17_lattices(k1_lattice2(sK0_skl))|~m1_filter_0(X0,k1_lattice2(sK0_skl))|v2_filter_0(X0,k1_lattice2(sK0_skl))|~v1_filter_0(X0,k1_lattice2(sK0_skl)))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f4623,f544])).
% 20.49/8.06 fof(f5526,plain,(
% 20.49/8.06 m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))),
% 20.49/8.06 inference(resolution,[status(thm)],[f1902,f433])).
% 20.49/8.06 fof(f5536,plain,(
% 20.49/8.06 k1_filter_0(k1_lattice2(sK0_skl))=u1_struct_0(k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f3754,f107])).
% 20.49/8.06 fof(f5696,plain,(
% 20.49/8.06 m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))),
% 20.49/8.06 inference(resolution,[status(thm)],[f1953,f433])).
% 20.49/8.06 fof(f7149,plain,(
% 20.49/8.06 ~v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~v1_funct_1(u2_lattices(sK0_skl))|~v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~v3_struct_0(k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f2611,f1781])).
% 20.49/8.06 fof(f7779,plain,(
% 20.49/8.06 ![X0,X1,X2]: (~m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~v1_funct_1(u2_lattices(sK0_skl))|~v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~k1_lattice2(sK0_skl)=g3_lattices(X0,X1,X2)|u1_struct_0(sK0_skl)=X0)),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f3661,f1889])).
% 20.49/8.06 fof(f8104,plain,(
% 20.49/8.06 ![X0,X1,X2]: (~m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~v1_funct_1(u2_lattices(sK0_skl))|~v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~k1_lattice2(sK0_skl)=g3_lattices(X0,X1,X2)|u2_lattices(sK0_skl)=X2)),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f3691,f1889])).
% 20.49/8.06 fof(f8303,plain,(
% 20.49/8.06 v3_struct_0(k1_lattice2(sK0_skl))|m1_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(resolution,[status(thm)],[f4080,f4118])).
% 20.49/8.06 fof(f8729,plain,(
% 20.49/8.06 v2_filter_0(sK1_skl,k1_lattice2(sK0_skl))|v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f4124,f105])).
% 20.49/8.06 fof(f9013,plain,(
% 20.49/8.06 ![X0]: (v3_struct_0(k1_lattice2(sK0_skl))|~v17_lattices(k1_lattice2(sK0_skl))|~m1_filter_0(X0,k1_lattice2(sK0_skl))|X0=u1_struct_0(k1_lattice2(sK0_skl))|~v2_filter_0(X0,k1_lattice2(sK0_skl))|v1_filter_0(X0,k1_lattice2(sK0_skl)))),
% 20.49/8.06 inference(forward_demodulation,[status(thm)],[f5536,f4496])).
% 20.49/8.06 fof(f9014,plain,(
% 20.49/8.06 ![X0]: (v3_struct_0(k1_lattice2(sK0_skl))|~m1_filter_0(X0,k1_lattice2(sK0_skl))|X0=u1_struct_0(k1_lattice2(sK0_skl))|~v2_filter_0(X0,k1_lattice2(sK0_skl))|v1_filter_0(X0,k1_lattice2(sK0_skl)))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f9013,f601])).
% 20.49/8.06 fof(f9057,plain,(
% 20.49/8.06 ![X0]: (v3_struct_0(k1_lattice2(sK0_skl))|~v17_lattices(k1_lattice2(sK0_skl))|~m1_filter_0(X0,k1_lattice2(sK0_skl))|~X0=u1_struct_0(k1_lattice2(sK0_skl))|~v1_filter_0(X0,k1_lattice2(sK0_skl)))),
% 20.49/8.06 inference(forward_demodulation,[status(thm)],[f5536,f4566])).
% 20.49/8.06 fof(f9058,plain,(
% 20.49/8.06 ![X0]: (v3_struct_0(k1_lattice2(sK0_skl))|~m1_filter_0(X0,k1_lattice2(sK0_skl))|~X0=u1_struct_0(k1_lattice2(sK0_skl))|~v1_filter_0(X0,k1_lattice2(sK0_skl)))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f9057,f601])).
% 20.49/8.06 fof(f9356,plain,(
% 20.49/8.06 ![X0]: (v3_struct_0(k1_lattice2(sK0_skl))|~m1_filter_0(X0,k1_lattice2(sK0_skl))|v2_filter_0(X0,k1_lattice2(sK0_skl))|~v1_filter_0(X0,k1_lattice2(sK0_skl)))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f4648,f601])).
% 20.49/8.06 fof(f9715,plain,(
% 20.49/8.06 ![X0,X1,X2]: (~v1_funct_1(u2_lattices(sK0_skl))|~v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~k1_lattice2(sK0_skl)=g3_lattices(X0,X1,X2)|u2_lattices(sK0_skl)=X2)),
% 20.49/8.06 inference(backward_subsumption_resolution,[status(thm)],[f8104,f5526])).
% 20.49/8.06 fof(f9717,plain,(
% 20.49/8.06 ![X0,X1,X2]: (~v1_funct_1(u2_lattices(sK0_skl))|~v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~k1_lattice2(sK0_skl)=g3_lattices(X0,X1,X2)|u1_struct_0(sK0_skl)=X0)),
% 20.49/8.06 inference(backward_subsumption_resolution,[status(thm)],[f7779,f5526])).
% 20.49/8.06 fof(f9718,plain,(
% 20.49/8.06 ~v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~v1_funct_1(u2_lattices(sK0_skl))|~v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~v3_struct_0(k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(backward_subsumption_resolution,[status(thm)],[f7149,f5526])).
% 20.49/8.06 fof(f9722,plain,(
% 20.49/8.06 ![X0,X1,X2]: (~v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~k1_lattice2(sK0_skl)=g3_lattices(X0,X1,X2)|u2_lattices(sK0_skl)=X2)),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f9715,f1912])).
% 20.49/8.06 fof(f9724,plain,(
% 20.49/8.06 ![X0,X1,X2]: (~v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~k1_lattice2(sK0_skl)=g3_lattices(X0,X1,X2)|u1_struct_0(sK0_skl)=X0)),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f9717,f1912])).
% 20.49/8.06 fof(f9725,plain,(
% 20.49/8.06 ~v1_funct_1(u2_lattices(sK0_skl))|~v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~v3_struct_0(k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f9718,f1889])).
% 20.49/8.06 fof(f9733,plain,(
% 20.49/8.06 ![X0,X1,X2]: (~m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~k1_lattice2(sK0_skl)=g3_lattices(X0,X1,X2)|u2_lattices(sK0_skl)=X2)),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f9722,f1940])).
% 20.49/8.06 fof(f9734,plain,(
% 20.49/8.06 ![X0,X1,X2]: (~k1_lattice2(sK0_skl)=g3_lattices(X0,X1,X2)|u2_lattices(sK0_skl)=X2)),
% 20.49/8.06 inference(resolution,[status(thm)],[f9733,f5696])).
% 20.49/8.06 fof(f9735,plain,(
% 20.49/8.06 u2_lattices(sK0_skl)=u1_lattices(k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(resolution,[status(thm)],[f9734,f3174])).
% 20.49/8.06 fof(f9760,plain,(
% 20.49/8.06 k1_lattice2(sK0_skl)=g3_lattices(u1_struct_0(k1_lattice2(sK0_skl)),u2_lattices(k1_lattice2(sK0_skl)),u2_lattices(sK0_skl))),
% 20.49/8.06 inference(backward_demodulation,[status(thm)],[f9735,f3174])).
% 20.49/8.06 fof(f9990,plain,(
% 20.49/8.06 ![X0,X1,X2]: (~m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~k1_lattice2(sK0_skl)=g3_lattices(X0,X1,X2)|u1_struct_0(sK0_skl)=X0)),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f9724,f1940])).
% 20.49/8.06 fof(f9991,plain,(
% 20.49/8.06 ![X0,X1,X2]: (~k1_lattice2(sK0_skl)=g3_lattices(X0,X1,X2)|u1_struct_0(sK0_skl)=X0)),
% 20.49/8.06 inference(resolution,[status(thm)],[f9990,f5696])).
% 20.49/8.06 fof(f10050,plain,(
% 20.49/8.06 ~v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~v3_struct_0(k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f9725,f1912])).
% 20.49/8.06 fof(f10051,plain,(
% 20.49/8.06 ~v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~v3_struct_0(k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(resolution,[status(thm)],[f10050,f5696])).
% 20.49/8.06 fof(f10052,plain,(
% 20.49/8.06 ~v3_struct_0(k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f10051,f1940])).
% 20.49/8.06 fof(f10060,plain,(
% 20.49/8.06 ![X0]: (~m1_filter_0(X0,k1_lattice2(sK0_skl))|v2_filter_0(X0,k1_lattice2(sK0_skl))|~v1_filter_0(X0,k1_lattice2(sK0_skl)))),
% 20.49/8.06 inference(backward_subsumption_resolution,[status(thm)],[f9356,f10052])).
% 20.49/8.06 fof(f10061,plain,(
% 20.49/8.06 ![X0]: (~m1_filter_0(X0,k1_lattice2(sK0_skl))|~X0=u1_struct_0(k1_lattice2(sK0_skl))|~v1_filter_0(X0,k1_lattice2(sK0_skl)))),
% 20.49/8.06 inference(backward_subsumption_resolution,[status(thm)],[f9058,f10052])).
% 20.49/8.06 fof(f10063,plain,(
% 20.49/8.06 ![X0]: (~m1_filter_0(X0,k1_lattice2(sK0_skl))|X0=u1_struct_0(k1_lattice2(sK0_skl))|~v2_filter_0(X0,k1_lattice2(sK0_skl))|v1_filter_0(X0,k1_lattice2(sK0_skl)))),
% 20.49/8.06 inference(backward_subsumption_resolution,[status(thm)],[f9014,f10052])).
% 20.49/8.06 fof(f10073,plain,(
% 20.49/8.06 m1_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(backward_subsumption_resolution,[status(thm)],[f8303,f10052])).
% 20.49/8.06 fof(f10483,plain,(
% 20.49/8.06 u1_struct_0(sK0_skl)=u1_struct_0(k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(resolution,[status(thm)],[f9760,f9991])).
% 20.49/8.06 fof(f10771,plain,(
% 20.49/8.06 ![X0]: (~m1_filter_0(X0,k1_lattice2(sK0_skl))|~X0=u1_struct_0(sK0_skl)|~v1_filter_0(X0,k1_lattice2(sK0_skl)))),
% 20.49/8.06 inference(forward_demodulation,[status(thm)],[f10483,f10061])).
% 20.49/8.06 fof(f10810,plain,(
% 20.49/8.06 ![X0]: (~m1_filter_0(X0,k1_lattice2(sK0_skl))|X0=u1_struct_0(sK0_skl)|~v2_filter_0(X0,k1_lattice2(sK0_skl))|v1_filter_0(X0,k1_lattice2(sK0_skl)))),
% 20.49/8.06 inference(forward_demodulation,[status(thm)],[f10483,f10063])).
% 20.49/8.06 fof(f10811,plain,(
% 20.49/8.06 ~m1_filter_0(sK1_skl,k1_lattice2(sK0_skl))|sK1_skl=u1_struct_0(sK0_skl)|v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))|v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(resolution,[status(thm)],[f10810,f8729])).
% 20.49/8.06 fof(f10816,plain,(
% 20.49/8.06 ~m1_filter_0(sK1_skl,k1_lattice2(sK0_skl))|sK1_skl=u1_struct_0(sK0_skl)|v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(duplicate_literals_removal,[status(thm)],[f10811])).
% 20.49/8.06 fof(f10817,plain,(
% 20.49/8.06 sK1_skl=u1_struct_0(sK0_skl)|v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.06 inference(forward_subsumption_resolution,[status(thm)],[f10816,f10073])).
% 20.49/8.06 fof(f11384,plain,(
% 20.49/8.06 sK1_skl=u1_struct_0(sK0_skl)|~m1_filter_0(sK1_skl,k1_lattice2(sK0_skl))|v2_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.07 inference(resolution,[status(thm)],[f10817,f10060])).
% 20.49/8.07 fof(f11385,plain,(
% 20.49/8.07 sK1_skl=u1_struct_0(sK0_skl)|v2_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.07 inference(forward_subsumption_resolution,[status(thm)],[f11384,f10073])).
% 20.49/8.07 fof(f21800,plain,(
% 20.49/8.07 ~l3_lattices(sK0_skl)|~m2_filter_2(sK1_skl,sK0_skl)|v1_filter_2(sK1_skl,sK0_skl)|~v2_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.07 inference(forward_subsumption_resolution,[status(thm)],[f4125,f105])).
% 20.49/8.07 fof(f21801,plain,(
% 20.49/8.07 ~l3_lattices(sK0_skl)|v1_filter_2(sK1_skl,sK0_skl)|~v2_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.07 inference(resolution,[status(thm)],[f21800,f108])).
% 20.49/8.07 fof(f21807,plain,(
% 20.49/8.07 v1_filter_2(sK1_skl,sK0_skl)|~v2_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.07 inference(forward_subsumption_resolution,[status(thm)],[f21801,f107])).
% 20.49/8.07 fof(f21819,plain,(
% 20.49/8.07 v1_filter_2(sK1_skl,sK0_skl)|sK1_skl=u1_struct_0(sK0_skl)),
% 20.49/8.07 inference(resolution,[status(thm)],[f21807,f11385])).
% 20.49/8.07 fof(f21849,plain,(
% 20.49/8.07 sK1_skl=u1_struct_0(sK0_skl)|~r2_filter_2(sK0_skl,sK1_skl)),
% 20.49/8.10 inference(backward_subsumption_resolution,[status(thm)],[f480,f21819])).
% 20.49/8.10 fof(f21885,plain,(
% 20.49/8.10 ~l3_lattices(sK0_skl)|~m2_filter_2(sK1_skl,sK0_skl)|r2_filter_2(sK0_skl,sK1_skl)|~v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.10 inference(forward_subsumption_resolution,[status(thm)],[f4126,f105])).
% 20.49/8.10 fof(f21886,plain,(
% 20.49/8.10 ~l3_lattices(sK0_skl)|r2_filter_2(sK0_skl,sK1_skl)|~v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.10 inference(resolution,[status(thm)],[f21885,f108])).
% 20.49/8.10 fof(f21891,plain,(
% 20.49/8.10 r2_filter_2(sK0_skl,sK1_skl)|~v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.10 inference(forward_subsumption_resolution,[status(thm)],[f21886,f107])).
% 20.49/8.10 fof(f21963,plain,(
% 20.49/8.10 r2_filter_2(sK0_skl,sK1_skl)|sK1_skl=u1_struct_0(sK0_skl)),
% 20.49/8.10 inference(resolution,[status(thm)],[f21891,f10817])).
% 20.49/8.10 fof(f21965,plain,(
% 20.49/8.10 sK1_skl=u1_struct_0(sK0_skl)),
% 20.49/8.10 inference(forward_subsumption_resolution,[status(thm)],[f21963,f21849])).
% 20.49/8.10 fof(f22139,plain,(
% 20.49/8.10 ![X0]: (~m1_filter_0(X0,k1_lattice2(sK0_skl))|~X0=sK1_skl|~v1_filter_0(X0,k1_lattice2(sK0_skl)))),
% 20.49/8.10 inference(backward_demodulation,[status(thm)],[f21965,f10771])).
% 20.49/8.10 fof(f22233,plain,(
% 20.49/8.10 ~sK1_skl=sK1_skl|r2_filter_2(sK0_skl,sK1_skl)),
% 20.49/8.10 inference(backward_demodulation,[status(thm)],[f21965,f481])).
% 20.49/8.10 fof(f22309,plain,(
% 20.49/8.10 r2_filter_2(sK0_skl,sK1_skl)),
% 20.49/8.10 inference(trivial_equality_resolution,[status(thm)],[f22233])).
% 20.49/8.10 fof(f22318,plain,(
% 20.49/8.10 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~m2_filter_2(sK1_skl,sK0_skl)|v1_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))),
% 20.49/8.10 inference(resolution,[status(thm)],[f22309,f443])).
% 20.49/8.10 fof(f22319,plain,(
% 20.49/8.10 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~m2_filter_2(sK1_skl,sK0_skl)|v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.10 inference(forward_demodulation,[status(thm)],[f4117,f22318])).
% 20.49/8.10 fof(f22320,plain,(
% 20.49/8.10 ~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~m2_filter_2(sK1_skl,sK0_skl)|v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.10 inference(forward_subsumption_resolution,[status(thm)],[f22319,f104])).
% 20.49/8.10 fof(f22390,plain,(
% 20.49/8.10 ~l3_lattices(sK0_skl)|~m2_filter_2(sK1_skl,sK0_skl)|v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.10 inference(forward_subsumption_resolution,[status(thm)],[f22320,f105])).
% 20.49/8.10 fof(f22391,plain,(
% 20.49/8.10 ~l3_lattices(sK0_skl)|v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.10 inference(resolution,[status(thm)],[f22390,f108])).
% 20.49/8.10 fof(f22393,plain,(
% 20.49/8.10 v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.10 inference(forward_subsumption_resolution,[status(thm)],[f22391,f107])).
% 20.49/8.10 fof(f22549,plain,(
% 20.49/8.10 ~m1_filter_0(sK1_skl,k1_lattice2(sK0_skl))|~sK1_skl=sK1_skl),
% 20.49/8.10 inference(resolution,[status(thm)],[f22139,f22393])).
% 20.49/8.10 fof(f22551,plain,(
% 20.49/8.10 ~m1_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 20.49/8.10 inference(trivial_equality_resolution,[status(thm)],[f22549])).
% 20.49/8.10 fof(f22552,plain,(
% 20.49/8.10 $false),
% 20.49/8.10 inference(forward_subsumption_resolution,[status(thm)],[f22551,f10073])).
% 20.49/8.10 % SZS output end CNFRefutation for theBenchmark.p
% 2.85/8.12 % Elapsed time: 2.720796 seconds
% 2.85/8.12 % CPU time: 21.317635 seconds
% 2.85/8.12 % Total memory used: 368.369 MB
% 2.85/8.12 % Net memory used: 361.056 MB
%------------------------------------------------------------------------------