%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT306+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 : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:03:36 PM UTC 2026
% Result : Theorem 22.40s 3.31s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT306+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.07/0.34 % Computer : n006.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Sun Sep 20 23:31:42 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 22.40/3.31 % Refutation found
% 22.40/3.31 % SZS status Theorem for theBenchmark: Theorem is valid
% 22.40/3.31 % SZS output start CNFRefutation for theBenchmark
% 22.40/3.31 fof(f1,conjecture,(
% 22.40/3.31 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> ( v14_lattices(A)=> r1_filter_2(u1_struct_0(A),k17_filter_2(A),k18_filter_2(A,k6_lattices(A))) ) ) )),
% 22.40/3.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.40/3.31 fof(f2,negated_conjecture,(
% 22.40/3.31 ~((! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> ( v14_lattices(A)=> r1_filter_2(u1_struct_0(A),k17_filter_2(A),k18_filter_2(A,k6_lattices(A))) ) ) ))),
% 22.40/3.31 inference(negated_conjecture,[status(cth)],[f1])).
% 22.40/3.31 fof(f3,axiom,(
% 22.40/3.31 (! [A] :( l3_lattices(A)=> ( v3_lattices(A)=> A = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) ) ) )),
% 22.40/3.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.40/3.31 fof(f12,axiom,(
% 22.40/3.31 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> k1_filter_0(A) = u1_struct_0(A) ) )),
% 22.40/3.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.40/3.31 fof(f13,axiom,(
% 22.40/3.31 (! [A] :( l3_lattices(A)=> k1_lattice2(A) = g3_lattices(u1_struct_0(A),u1_lattices(A),u2_lattices(A)) ) )),
% 22.40/3.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.40/3.31 fof(f15,axiom,(
% 22.40/3.31 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> k5_filter_2(A,B) = B ) )) )),
% 22.40/3.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.40/3.31 fof(f16,axiom,(
% 22.40/3.31 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> k17_filter_2(A) = u1_struct_0(A) ) )),
% 22.40/3.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.40/3.31 fof(f21,axiom,(
% 22.40/3.31 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> m1_filter_0(k1_filter_0(A),A) ) )),
% 22.40/3.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.40/3.31 fof(f23,axiom,(
% 22.40/3.31 (! [A] :( l3_lattices(A)=> ( v3_lattices(k1_lattice2(A))& l3_lattices(k1_lattice2(A)) ) ) )),
% 22.40/3.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.40/3.31 fof(f31,axiom,(
% 22.40/3.31 (! [A] :( ( ~ v3_struct_0(A)& l2_lattices(A) )=> m1_subset_1(k6_lattices(A),u1_struct_0(A)) ) )),
% 22.40/3.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.40/3.31 fof(f35,axiom,(
% 22.40/3.31 (! [A] :( l3_lattices(A)=> ( l1_lattices(A)& l2_lattices(A) ) ) )),
% 22.40/3.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.40/3.31 fof(f36,axiom,(
% 22.40/3.31 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_filter_0(B,A)=> ( ~ v1_xboole_0(B)& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) ) )) )),
% 22.40/3.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.40/3.31 fof(f43,axiom,(
% 22.40/3.31 (! [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)) ) ) )),
% 22.40/3.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.40/3.31 fof(f45,axiom,(
% 22.40/3.31 (! [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)) ) ) )),
% 22.40/3.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.40/3.32 fof(f57,axiom,(
% 22.40/3.32 (! [A] :( ( ~ v3_struct_0(A)& l3_lattices(A) )=> ( ~ v3_struct_0(k1_lattice2(A))& v3_lattices(k1_lattice2(A)) ) ) )),
% 22.40/3.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.40/3.32 fof(f63,axiom,(
% 22.40/3.32 (! [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)) ) ) )),
% 22.40/3.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.40/3.32 fof(f67,axiom,(
% 22.40/3.32 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> ( ~ v3_struct_0(k1_lattice2(A))& v3_lattices(k1_lattice2(A))& v4_lattices(k1_lattice2(A))& v5_lattices(k1_lattice2(A))& v6_lattices(k1_lattice2(A))& v7_lattices(k1_lattice2(A))& v8_lattices(k1_lattice2(A))& v9_lattices(k1_lattice2(A))& v10_lattices(k1_lattice2(A)) ) ) )),
% 22.40/3.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.40/3.32 fof(f70,axiom,(
% 22.40/3.32 (! [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 ) ) )) )),
% 22.40/3.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.40/3.32 fof(f86,axiom,(
% 22.40/3.32 (! [A,B] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A)& m1_subset_1(B,u1_struct_0(A)) )=> k2_filter_2(A,B) = k2_filter_0(A,B) ) )),
% 22.40/3.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.40/3.32 fof(f88,axiom,(
% 22.40/3.32 (! [A,B,C] :( m2_relset_1(C,A,B)<=> m1_relset_1(C,A,B) ) )),
% 22.40/3.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.40/3.32 fof(f89,axiom,(
% 22.40/3.32 (! [A,B,C] :( ( ~ v1_xboole_0(A)& m1_subset_1(B,k1_zfmisc_1(A))& m1_subset_1(C,k1_zfmisc_1(A)) )=> ( r1_filter_2(A,B,C)<=> B = C ) ) )),
% 22.40/3.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.40/3.32 fof(f96,axiom,(
% 22.40/3.32 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> ( ( ~ v3_struct_0(A)& v10_lattices(A)& v13_lattices(A)& l3_lattices(A) )=> k1_filter_0(A) = k2_filter_0(A,k5_lattices(A)) ) ) )),
% 22.40/3.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.40/3.32 fof(f99,axiom,(
% 22.40/3.32 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> ( k18_filter_2(A,B) = k2_filter_2(k1_lattice2(A),k5_filter_2(A,B))& k18_filter_2(k1_lattice2(A),k5_filter_2(A,B)) = k2_filter_2(A,B) ) ) )) )),
% 22.40/3.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.40/3.32 fof(f103,axiom,(
% 22.40/3.32 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> ( v14_lattices(A)<=> v13_lattices(k1_lattice2(A)) ) ) )),
% 22.40/3.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.40/3.32 fof(f105,axiom,(
% 22.40/3.32 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v14_lattices(A)& l3_lattices(A) )=> k6_lattices(A) = k5_lattices(k1_lattice2(A)) ) )),
% 22.40/3.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.40/3.32 fof(f108,plain,(
% 22.40/3.32 (?[A]: (((~v3_struct_0(A)&v10_lattices(A))&l3_lattices(A))&(v14_lattices(A)&~r1_filter_2(u1_struct_0(A),k17_filter_2(A),k18_filter_2(A,k6_lattices(A))))))),
% 22.40/3.32 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 22.40/3.32 fof(f109,plain,(
% 22.40/3.32 (((~v3_struct_0(sK0_skl)&v10_lattices(sK0_skl))&l3_lattices(sK0_skl))&(v14_lattices(sK0_skl)&~r1_filter_2(u1_struct_0(sK0_skl),k17_filter_2(sK0_skl),k18_filter_2(sK0_skl,k6_lattices(sK0_skl)))))),
% 22.40/3.32 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(A,sK0_skl)],[f108])).
% 22.40/3.32 fof(f110,plain,(
% 22.40/3.32 ~v3_struct_0(sK0_skl)),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f109])).
% 22.40/3.32 fof(f111,plain,(
% 22.40/3.32 v10_lattices(sK0_skl)),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f109])).
% 22.40/3.32 fof(f112,plain,(
% 22.40/3.32 l3_lattices(sK0_skl)),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f109])).
% 22.40/3.32 fof(f113,plain,(
% 22.40/3.32 v14_lattices(sK0_skl)),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f109])).
% 22.40/3.32 fof(f114,plain,(
% 22.40/3.32 ~r1_filter_2(u1_struct_0(sK0_skl),k17_filter_2(sK0_skl),k18_filter_2(sK0_skl,k6_lattices(sK0_skl)))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f109])).
% 22.40/3.32 fof(f115,plain,(
% 22.40/3.32 ![A]: (~l3_lattices(A)|(~v3_lattices(A)|A=g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A))))),
% 22.40/3.32 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 22.40/3.32 fof(f116,plain,(
% 22.40/3.32 ![X0]: (~l3_lattices(X0)|~v3_lattices(X0)|X0=g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f115])).
% 22.40/3.32 fof(f146,plain,(
% 22.40/3.32 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|k1_filter_0(A)=u1_struct_0(A))),
% 22.40/3.32 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 22.40/3.32 fof(f147,plain,(
% 22.40/3.32 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|k1_filter_0(X0)=u1_struct_0(X0))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f146])).
% 22.40/3.32 fof(f148,plain,(
% 22.40/3.32 ![A]: (~l3_lattices(A)|k1_lattice2(A)=g3_lattices(u1_struct_0(A),u1_lattices(A),u2_lattices(A)))),
% 22.40/3.32 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 22.40/3.32 fof(f149,plain,(
% 22.40/3.32 ![X0]: (~l3_lattices(X0)|k1_lattice2(X0)=g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f148])).
% 22.40/3.32 fof(f152,plain,(
% 22.40/3.32 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m1_subset_1(B,u1_struct_0(A))|k5_filter_2(A,B)=B)))),
% 22.40/3.32 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 22.40/3.32 fof(f153,plain,(
% 22.40/3.32 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|k5_filter_2(X0,X1)=X1)),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f152])).
% 22.40/3.32 fof(f154,plain,(
% 22.40/3.32 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|k17_filter_2(A)=u1_struct_0(A))),
% 22.40/3.32 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 22.40/3.32 fof(f155,plain,(
% 22.40/3.32 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|k17_filter_2(X0)=u1_struct_0(X0))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f154])).
% 22.40/3.32 fof(f165,plain,(
% 22.40/3.32 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|m1_filter_0(k1_filter_0(A),A))),
% 22.40/3.32 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 22.40/3.32 fof(f166,plain,(
% 22.40/3.32 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|m1_filter_0(k1_filter_0(X0),X0))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f165])).
% 22.40/3.32 fof(f169,plain,(
% 22.40/3.32 ![A]: (~l3_lattices(A)|(v3_lattices(k1_lattice2(A))&l3_lattices(k1_lattice2(A))))),
% 22.40/3.32 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 22.40/3.32 fof(f170,plain,(
% 22.40/3.32 ![X0]: (~l3_lattices(X0)|v3_lattices(k1_lattice2(X0)))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f169])).
% 22.40/3.32 fof(f171,plain,(
% 22.40/3.32 ![X0]: (~l3_lattices(X0)|l3_lattices(k1_lattice2(X0)))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f169])).
% 22.40/3.32 fof(f180,plain,(
% 22.40/3.32 ![A]: ((v3_struct_0(A)|~l2_lattices(A))|m1_subset_1(k6_lattices(A),u1_struct_0(A)))),
% 22.40/3.32 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 22.40/3.32 fof(f181,plain,(
% 22.40/3.32 ![X0]: (v3_struct_0(X0)|~l2_lattices(X0)|m1_subset_1(k6_lattices(X0),u1_struct_0(X0)))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f180])).
% 22.40/3.32 fof(f186,plain,(
% 22.40/3.32 ![A]: (~l3_lattices(A)|(l1_lattices(A)&l2_lattices(A)))),
% 22.40/3.32 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 22.40/3.32 fof(f187,plain,(
% 22.40/3.32 ![X0]: (~l3_lattices(X0)|l1_lattices(X0))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f186])).
% 22.40/3.32 fof(f188,plain,(
% 22.40/3.32 ![X0]: (~l3_lattices(X0)|l2_lattices(X0))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f186])).
% 22.40/3.32 fof(f189,plain,(
% 22.40/3.32 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m1_filter_0(B,A)|(~v1_xboole_0(B)&m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))))))),
% 22.40/3.32 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 22.40/3.32 fof(f190,plain,(
% 22.40/3.32 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|~v1_xboole_0(X1))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f189])).
% 22.40/3.32 fof(f191,plain,(
% 22.40/3.32 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f189])).
% 22.40/3.32 fof(f202,plain,(
% 22.40/3.32 ![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))))),
% 22.40/3.32 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 22.40/3.32 fof(f203,plain,(
% 22.40/3.32 ![X0]: (~l1_lattices(X0)|v1_funct_1(u1_lattices(X0)))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f202])).
% 22.40/3.32 fof(f204,plain,(
% 22.40/3.32 ![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)))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f202])).
% 22.40/3.32 fof(f205,plain,(
% 22.40/3.32 ![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)))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f202])).
% 22.40/3.32 fof(f206,plain,(
% 22.40/3.32 ![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))))),
% 22.40/3.32 inference(pre_NNF_transformation,[status(thm)],[f45])).
% 22.40/3.32 fof(f207,plain,(
% 22.40/3.32 ![X0]: (~l2_lattices(X0)|v1_funct_1(u2_lattices(X0)))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f206])).
% 22.40/3.32 fof(f208,plain,(
% 22.40/3.32 ![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)))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f206])).
% 22.40/3.32 fof(f209,plain,(
% 22.40/3.32 ![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)))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f206])).
% 22.40/3.32 fof(f236,plain,(
% 22.40/3.32 ![A]: ((v3_struct_0(A)|~l3_lattices(A))|(~v3_struct_0(k1_lattice2(A))&v3_lattices(k1_lattice2(A))))),
% 22.40/3.32 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 22.40/3.32 fof(f237,plain,(
% 22.40/3.32 ![X0]: (v3_struct_0(X0)|~l3_lattices(X0)|~v3_struct_0(k1_lattice2(X0)))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f236])).
% 22.40/3.32 fof(f255,plain,(
% 22.40/3.32 ![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))))),
% 22.40/3.32 inference(pre_NNF_transformation,[status(thm)],[f63])).
% 22.40/3.32 fof(f256,plain,(
% 22.40/3.32 ![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)))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f255])).
% 22.40/3.32 fof(f272,plain,(
% 22.40/3.32 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|((((((((~v3_struct_0(k1_lattice2(A))&v3_lattices(k1_lattice2(A)))&v4_lattices(k1_lattice2(A)))&v5_lattices(k1_lattice2(A)))&v6_lattices(k1_lattice2(A)))&v7_lattices(k1_lattice2(A)))&v8_lattices(k1_lattice2(A)))&v9_lattices(k1_lattice2(A)))&v10_lattices(k1_lattice2(A))))),
% 22.40/3.32 inference(pre_NNF_transformation,[status(thm)],[f67])).
% 22.40/3.32 fof(f281,plain,(
% 22.40/3.32 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v10_lattices(k1_lattice2(X0)))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f272])).
% 22.40/3.32 fof(f298,plain,(
% 22.40/3.32 ![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))))),
% 22.40/3.32 inference(pre_NNF_transformation,[status(thm)],[f70])).
% 22.40/3.32 fof(f299,plain,(
% 22.40/3.32 ![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)),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f298])).
% 22.40/3.32 fof(f369,plain,(
% 22.40/3.32 ![A,B]: ((((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|~m1_subset_1(B,u1_struct_0(A)))|k2_filter_2(A,B)=k2_filter_0(A,B))),
% 22.40/3.32 inference(pre_NNF_transformation,[status(thm)],[f86])).
% 22.40/3.32 fof(f370,plain,(
% 22.40/3.32 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|k2_filter_2(X0,X1)=k2_filter_0(X0,X1))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f369])).
% 22.40/3.32 fof(f376,plain,(
% 22.40/3.32 ![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)))),
% 22.40/3.32 inference(NNF_transformation,[status(thm)],[f88])).
% 22.40/3.32 fof(f377,plain,(
% 22.40/3.32 (![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)))),
% 22.40/3.32 inference(miniscoping,[status(thm)],[f376])).
% 22.40/3.32 fof(f378,plain,(
% 22.40/3.32 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_relset_1(X0,X1,X2))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f377])).
% 22.40/3.32 fof(f380,plain,(
% 22.40/3.32 ![A,B,C]: (((v1_xboole_0(A)|~m1_subset_1(B,k1_zfmisc_1(A)))|~m1_subset_1(C,k1_zfmisc_1(A)))|(r1_filter_2(A,B,C)<=>B=C))),
% 22.40/3.32 inference(pre_NNF_transformation,[status(thm)],[f89])).
% 22.40/3.32 fof(f381,plain,(
% 22.40/3.32 ![A,B,C]: (((v1_xboole_0(A)|~m1_subset_1(B,k1_zfmisc_1(A)))|~m1_subset_1(C,k1_zfmisc_1(A)))|((~r1_filter_2(A,B,C)|B=C)&(r1_filter_2(A,B,C)|~B=C)))),
% 22.40/3.32 inference(NNF_transformation,[status(thm)],[f380])).
% 22.40/3.32 fof(f383,plain,(
% 22.40/3.32 ![X0,X1,X2]: (v1_xboole_0(X0)|~m1_subset_1(X1,k1_zfmisc_1(X0))|~m1_subset_1(X2,k1_zfmisc_1(X0))|r1_filter_2(X0,X1,X2)|~X1=X2)),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f381])).
% 22.40/3.32 fof(f400,plain,(
% 22.40/3.32 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|((((v3_struct_0(A)|~v10_lattices(A))|~v13_lattices(A))|~l3_lattices(A))|k1_filter_0(A)=k2_filter_0(A,k5_lattices(A))))),
% 22.40/3.32 inference(pre_NNF_transformation,[status(thm)],[f96])).
% 22.40/3.32 fof(f401,plain,(
% 22.40/3.32 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v3_struct_0(X0)|~v10_lattices(X0)|~v13_lattices(X0)|~l3_lattices(X0)|k1_filter_0(X0)=k2_filter_0(X0,k5_lattices(X0)))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f400])).
% 22.40/3.32 fof(f409,plain,(
% 22.40/3.32 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m1_subset_1(B,u1_struct_0(A))|(k18_filter_2(A,B)=k2_filter_2(k1_lattice2(A),k5_filter_2(A,B))&k18_filter_2(k1_lattice2(A),k5_filter_2(A,B))=k2_filter_2(A,B)))))),
% 22.40/3.32 inference(pre_NNF_transformation,[status(thm)],[f99])).
% 22.40/3.32 fof(f410,plain,(
% 22.40/3.32 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|k18_filter_2(X0,X1)=k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1)))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f409])).
% 22.40/3.32 fof(f422,plain,(
% 22.40/3.32 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(v14_lattices(A)<=>v13_lattices(k1_lattice2(A))))),
% 22.40/3.32 inference(pre_NNF_transformation,[status(thm)],[f103])).
% 22.40/3.32 fof(f423,plain,(
% 22.40/3.32 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|((~v14_lattices(A)|v13_lattices(k1_lattice2(A)))&(v14_lattices(A)|~v13_lattices(k1_lattice2(A)))))),
% 22.40/3.32 inference(NNF_transformation,[status(thm)],[f422])).
% 22.40/3.32 fof(f424,plain,(
% 22.40/3.32 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~v14_lattices(X0)|v13_lattices(k1_lattice2(X0)))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f423])).
% 22.40/3.32 fof(f428,plain,(
% 22.40/3.32 ![A]: ((((v3_struct_0(A)|~v10_lattices(A))|~v14_lattices(A))|~l3_lattices(A))|k6_lattices(A)=k5_lattices(k1_lattice2(A)))),
% 22.40/3.32 inference(pre_NNF_transformation,[status(thm)],[f105])).
% 22.40/3.32 fof(f429,plain,(
% 22.40/3.32 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~v14_lattices(X0)|~l3_lattices(X0)|k6_lattices(X0)=k5_lattices(k1_lattice2(X0)))),
% 22.40/3.32 inference(cnf_transformation,[status(thm)],[f428])).
% 22.40/3.32 fof(f438,plain,(
% 22.40/3.32 ![X0,X2]: (v1_xboole_0(X0)|~m1_subset_1(X2,k1_zfmisc_1(X0))|~m1_subset_1(X2,k1_zfmisc_1(X0))|r1_filter_2(X0,X2,X2))),
% 22.40/3.32 inference(destructive_equality_resolution,[status(thm)],[f383])).
% 22.40/3.32 fof(f439,plain,(
% 22.40/3.32 ![X0,X1]: (v1_xboole_0(X0)|~m1_subset_1(X1,k1_zfmisc_1(X0))|r1_filter_2(X0,X1,X1))),
% 22.40/3.32 inference(duplicate_literals_removal,[status(thm)],[f438])).
% 22.40/3.32 fof(f440,plain,(
% 22.40/3.32 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~v13_lattices(X0)|k1_filter_0(X0)=k2_filter_0(X0,k5_lattices(X0)))),
% 22.40/3.32 inference(duplicate_literals_removal,[status(thm)],[f401])).
% 22.40/3.32 fof(f441,plain,(
% 22.40/3.32 v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|k17_filter_2(sK0_skl)=u1_struct_0(sK0_skl)),
% 22.40/3.32 inference(resolution,[status(thm)],[f155,f111])).
% 22.40/3.32 fof(f443,plain,(
% 22.40/3.32 ~l3_lattices(sK0_skl)|k17_filter_2(sK0_skl)=u1_struct_0(sK0_skl)),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f441,f110])).
% 22.40/3.32 fof(f460,plain,(
% 22.40/3.32 ~r1_filter_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k18_filter_2(sK0_skl,k6_lattices(sK0_skl)))),
% 22.40/3.32 inference(backward_demodulation,[status(thm)],[f461,f114])).
% 22.40/3.32 fof(f461,plain,(
% 22.40/3.32 k17_filter_2(sK0_skl)=u1_struct_0(sK0_skl)),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f443,f112])).
% 22.40/3.32 fof(f517,plain,(
% 22.40/3.32 v3_struct_0(sK0_skl)|~v14_lattices(sK0_skl)|~l3_lattices(sK0_skl)|k6_lattices(sK0_skl)=k5_lattices(k1_lattice2(sK0_skl))),
% 22.40/3.32 inference(resolution,[status(thm)],[f429,f111])).
% 22.40/3.32 fof(f524,plain,(
% 22.40/3.32 ~v14_lattices(sK0_skl)|~l3_lattices(sK0_skl)|k6_lattices(sK0_skl)=k5_lattices(k1_lattice2(sK0_skl))),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f517,f110])).
% 22.40/3.32 fof(f544,plain,(
% 22.40/3.32 v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|k1_filter_0(sK0_skl)=u1_struct_0(sK0_skl)),
% 22.40/3.32 inference(resolution,[status(thm)],[f147,f111])).
% 22.40/3.32 fof(f549,plain,(
% 22.40/3.32 ~l3_lattices(sK0_skl)|k1_filter_0(sK0_skl)=u1_struct_0(sK0_skl)),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f544,f110])).
% 22.40/3.32 fof(f555,plain,(
% 22.40/3.32 k1_lattice2(sK0_skl)=g3_lattices(u1_struct_0(sK0_skl),u1_lattices(sK0_skl),u2_lattices(sK0_skl))),
% 22.40/3.32 inference(resolution,[status(thm)],[f149,f112])).
% 22.40/3.32 fof(f585,plain,(
% 22.40/3.32 ![X0]: (v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|k5_filter_2(sK0_skl,X0)=X0)),
% 22.40/3.32 inference(resolution,[status(thm)],[f153,f111])).
% 22.40/3.32 fof(f590,plain,(
% 22.40/3.32 ![X0]: (~l3_lattices(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|k5_filter_2(sK0_skl,X0)=X0)),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f585,f110])).
% 22.40/3.32 fof(f594,plain,(
% 22.40/3.32 v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|m1_filter_0(k1_filter_0(sK0_skl),sK0_skl)),
% 22.40/3.32 inference(resolution,[status(thm)],[f166,f111])).
% 22.40/3.32 fof(f599,plain,(
% 22.40/3.32 ~l3_lattices(sK0_skl)|m1_filter_0(k1_filter_0(sK0_skl),sK0_skl)),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f594,f110])).
% 22.40/3.32 fof(f614,plain,(
% 22.40/3.32 v3_lattices(k1_lattice2(sK0_skl))),
% 22.40/3.32 inference(resolution,[status(thm)],[f170,f112])).
% 22.40/3.32 fof(f615,plain,(
% 22.40/3.32 ~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)))),
% 22.40/3.32 inference(resolution,[status(thm)],[f614,f116])).
% 22.40/3.32 fof(f616,plain,(
% 22.40/3.32 ~l3_lattices(sK0_skl)|k6_lattices(sK0_skl)=k5_lattices(k1_lattice2(sK0_skl))),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f524,f113])).
% 22.40/3.32 fof(f617,plain,(
% 22.40/3.32 k6_lattices(sK0_skl)=k5_lattices(k1_lattice2(sK0_skl))),
% 22.40/3.32 inference(resolution,[status(thm)],[f616,f112])).
% 22.40/3.32 fof(f619,plain,(
% 22.40/3.32 k1_filter_0(sK0_skl)=u1_struct_0(sK0_skl)),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f549,f112])).
% 22.40/3.32 fof(f668,plain,(
% 22.40/3.32 l3_lattices(k1_lattice2(sK0_skl))),
% 22.40/3.32 inference(resolution,[status(thm)],[f171,f112])).
% 22.40/3.32 fof(f704,plain,(
% 22.40/3.32 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))),
% 22.40/3.32 inference(resolution,[status(thm)],[f668,f147])).
% 22.40/3.32 fof(f805,plain,(
% 22.40/3.32 l1_lattices(sK0_skl)),
% 22.40/3.32 inference(resolution,[status(thm)],[f187,f112])).
% 22.40/3.32 fof(f810,plain,(
% 22.40/3.32 l2_lattices(sK0_skl)),
% 22.40/3.32 inference(resolution,[status(thm)],[f188,f112])).
% 22.40/3.32 fof(f812,plain,(
% 22.40/3.32 ![X0]: (v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|~m1_filter_0(X0,sK0_skl)|~v1_xboole_0(X0))),
% 22.40/3.32 inference(resolution,[status(thm)],[f190,f111])).
% 22.40/3.32 fof(f821,plain,(
% 22.40/3.32 ![X0]: (~l3_lattices(sK0_skl)|~m1_filter_0(X0,sK0_skl)|~v1_xboole_0(X0))),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f812,f110])).
% 22.40/3.32 fof(f826,plain,(
% 22.40/3.32 ![X0]: (v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|~m1_filter_0(X0,sK0_skl)|m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 22.40/3.32 inference(resolution,[status(thm)],[f191,f111])).
% 22.40/3.32 fof(f834,plain,(
% 22.40/3.32 ![X0]: (~l3_lattices(sK0_skl)|~m1_filter_0(X0,sK0_skl)|m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f826,f110])).
% 22.40/3.32 fof(f857,plain,(
% 22.40/3.32 v3_struct_0(sK0_skl)|m1_subset_1(k6_lattices(sK0_skl),u1_struct_0(sK0_skl))),
% 22.40/3.32 inference(resolution,[status(thm)],[f810,f181])).
% 22.40/3.32 fof(f858,plain,(
% 22.40/3.32 m1_subset_1(k6_lattices(sK0_skl),u1_struct_0(sK0_skl))),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f857,f110])).
% 22.40/3.32 fof(f1022,plain,(
% 22.40/3.32 v1_funct_1(u1_lattices(sK0_skl))),
% 22.40/3.32 inference(resolution,[status(thm)],[f203,f805])).
% 22.40/3.32 fof(f1024,plain,(
% 22.40/3.32 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k5_filter_2(sK0_skl,X0)=X0)),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f590,f112])).
% 22.40/3.32 fof(f1047,plain,(
% 22.40/3.32 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))),
% 22.40/3.32 inference(resolution,[status(thm)],[f204,f805])).
% 22.40/3.32 fof(f1050,plain,(
% 22.40/3.32 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))),
% 22.40/3.32 inference(resolution,[status(thm)],[f205,f805])).
% 22.40/3.32 fof(f1052,plain,(
% 22.40/3.32 v1_funct_1(u2_lattices(sK0_skl))),
% 22.40/3.32 inference(resolution,[status(thm)],[f207,f810])).
% 22.40/3.32 fof(f1054,plain,(
% 22.40/3.32 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))),
% 22.40/3.32 inference(resolution,[status(thm)],[f208,f810])).
% 22.40/3.32 fof(f1056,plain,(
% 22.40/3.32 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))),
% 22.40/3.32 inference(resolution,[status(thm)],[f209,f810])).
% 22.40/3.32 fof(f1076,plain,(
% 22.40/3.32 ~l3_lattices(sK0_skl)|m1_filter_0(u1_struct_0(sK0_skl),sK0_skl)),
% 22.40/3.32 inference(forward_demodulation,[status(thm)],[f619,f599])).
% 22.40/3.32 fof(f1077,plain,(
% 22.40/3.32 m1_filter_0(u1_struct_0(sK0_skl),sK0_skl)),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f1076,f112])).
% 22.40/3.32 fof(f1196,plain,(
% 22.40/3.32 ![X0]: (~m1_filter_0(X0,sK0_skl)|~v1_xboole_0(X0))),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f821,f112])).
% 22.40/3.32 fof(f1197,plain,(
% 22.40/3.32 ~v1_xboole_0(u1_struct_0(sK0_skl))),
% 22.40/3.32 inference(resolution,[status(thm)],[f1196,f1077])).
% 22.40/3.32 fof(f1203,plain,(
% 22.40/3.32 ![X0]: (~m1_filter_0(X0,sK0_skl)|m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f834,f112])).
% 22.40/3.32 fof(f1204,plain,(
% 22.40/3.32 m1_subset_1(u1_struct_0(sK0_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 22.40/3.32 inference(resolution,[status(thm)],[f1203,f1077])).
% 22.40/3.32 fof(f1325,plain,(
% 22.40/3.32 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))),
% 22.40/3.32 inference(paramodulation,[status(thm)],[f555,f256])).
% 22.40/3.32 fof(f1326,plain,(
% 22.40/3.32 ~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))),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f1325,f1197])).
% 22.40/3.32 fof(f1629,plain,(
% 22.40/3.32 v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|v10_lattices(k1_lattice2(sK0_skl))),
% 22.40/3.32 inference(resolution,[status(thm)],[f281,f111])).
% 22.40/3.32 fof(f1633,plain,(
% 22.40/3.32 ~l3_lattices(sK0_skl)|v10_lattices(k1_lattice2(sK0_skl))),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f1629,f110])).
% 22.40/3.32 fof(f1840,plain,(
% 22.40/3.32 k5_filter_2(sK0_skl,k6_lattices(sK0_skl))=k6_lattices(sK0_skl)),
% 22.40/3.32 inference(resolution,[status(thm)],[f858,f1024])).
% 22.40/3.32 fof(f1914,plain,(
% 22.40/3.32 ![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)),
% 22.40/3.32 inference(paramodulation,[status(thm)],[f555,f299])).
% 22.40/3.32 fof(f1917,plain,(
% 22.40/3.32 ![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)),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f1914,f1022])).
% 22.40/3.32 fof(f1964,plain,(
% 22.40/3.32 v10_lattices(k1_lattice2(sK0_skl))),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f1633,f112])).
% 22.40/3.32 fof(f2142,plain,(
% 22.40/3.32 ![X0]: (v3_struct_0(k1_lattice2(sK0_skl))|~l3_lattices(k1_lattice2(sK0_skl))|~m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0_skl)))|k2_filter_2(k1_lattice2(sK0_skl),X0)=k2_filter_0(k1_lattice2(sK0_skl),X0))),
% 22.40/3.32 inference(resolution,[status(thm)],[f370,f1964])).
% 22.40/3.32 fof(f2156,plain,(
% 22.40/3.32 ![X0]: (v3_struct_0(k1_lattice2(sK0_skl))|~m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0_skl)))|k2_filter_2(k1_lattice2(sK0_skl),X0)=k2_filter_0(k1_lattice2(sK0_skl),X0))),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f2142,f668])).
% 22.40/3.32 fof(f2387,plain,(
% 22.40/3.32 v3_struct_0(k1_lattice2(sK0_skl))|~l3_lattices(k1_lattice2(sK0_skl))|~v13_lattices(k1_lattice2(sK0_skl))|k1_filter_0(k1_lattice2(sK0_skl))=k2_filter_0(k1_lattice2(sK0_skl),k5_lattices(k1_lattice2(sK0_skl)))),
% 22.40/3.32 inference(resolution,[status(thm)],[f440,f1964])).
% 22.40/3.32 fof(f2403,plain,(
% 22.40/3.32 v3_struct_0(k1_lattice2(sK0_skl))|~l3_lattices(k1_lattice2(sK0_skl))|~v13_lattices(k1_lattice2(sK0_skl))|k1_filter_0(k1_lattice2(sK0_skl))=k2_filter_0(k1_lattice2(sK0_skl),k6_lattices(sK0_skl))),
% 22.40/3.32 inference(forward_demodulation,[status(thm)],[f617,f2387])).
% 22.40/3.32 fof(f2404,plain,(
% 22.40/3.32 v3_struct_0(k1_lattice2(sK0_skl))|~v13_lattices(k1_lattice2(sK0_skl))|k1_filter_0(k1_lattice2(sK0_skl))=k2_filter_0(k1_lattice2(sK0_skl),k6_lattices(sK0_skl))),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f2403,f668])).
% 22.40/3.32 fof(f2468,plain,(
% 22.40/3.32 ![X0]: (v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|k18_filter_2(sK0_skl,X0)=k2_filter_2(k1_lattice2(sK0_skl),k5_filter_2(sK0_skl,X0)))),
% 22.40/3.32 inference(resolution,[status(thm)],[f410,f111])).
% 22.40/3.32 fof(f2482,plain,(
% 22.40/3.32 ![X0]: (~l3_lattices(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|k18_filter_2(sK0_skl,X0)=k2_filter_2(k1_lattice2(sK0_skl),k5_filter_2(sK0_skl,X0)))),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f2468,f110])).
% 22.40/3.32 fof(f2554,plain,(
% 22.40/3.32 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|v13_lattices(k1_lattice2(sK0_skl))),
% 22.40/3.32 inference(resolution,[status(thm)],[f424,f113])).
% 22.40/3.32 fof(f2557,plain,(
% 22.40/3.32 ~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|v13_lattices(k1_lattice2(sK0_skl))),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f2554,f110])).
% 22.40/3.32 fof(f2702,plain,(
% 22.40/3.32 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k18_filter_2(sK0_skl,X0)=k2_filter_2(k1_lattice2(sK0_skl),k5_filter_2(sK0_skl,X0)))),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f2482,f112])).
% 22.40/3.32 fof(f2705,plain,(
% 22.40/3.32 k18_filter_2(sK0_skl,k6_lattices(sK0_skl))=k2_filter_2(k1_lattice2(sK0_skl),k5_filter_2(sK0_skl,k6_lattices(sK0_skl)))),
% 22.40/3.32 inference(resolution,[status(thm)],[f2702,f858])).
% 22.40/3.32 fof(f2805,plain,(
% 22.40/3.32 ~l3_lattices(sK0_skl)|v13_lattices(k1_lattice2(sK0_skl))),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f2557,f111])).
% 22.40/3.32 fof(f2806,plain,(
% 22.40/3.32 v13_lattices(k1_lattice2(sK0_skl))),
% 22.40/3.32 inference(resolution,[status(thm)],[f2805,f112])).
% 22.40/3.32 fof(f2911,plain,(
% 22.40/3.32 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)))),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f615,f668])).
% 22.40/3.32 fof(f3147,plain,(
% 22.40/3.32 v1_xboole_0(u1_struct_0(sK0_skl))|r1_filter_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))),
% 22.40/3.32 inference(resolution,[status(thm)],[f1204,f439])).
% 22.40/3.32 fof(f3149,plain,(
% 22.40/3.32 r1_filter_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f3147,f1197])).
% 22.40/3.32 fof(f3195,plain,(
% 22.40/3.32 v3_struct_0(k1_lattice2(sK0_skl))|k1_filter_0(k1_lattice2(sK0_skl))=u1_struct_0(k1_lattice2(sK0_skl))),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f704,f1964])).
% 22.40/3.32 fof(f3196,plain,(
% 22.40/3.32 k1_filter_0(k1_lattice2(sK0_skl))=u1_struct_0(k1_lattice2(sK0_skl))|v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)),
% 22.40/3.32 inference(resolution,[status(thm)],[f3195,f237])).
% 22.40/3.32 fof(f3197,plain,(
% 22.40/3.32 k1_filter_0(k1_lattice2(sK0_skl))=u1_struct_0(k1_lattice2(sK0_skl))|~l3_lattices(sK0_skl)),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f3196,f110])).
% 22.40/3.32 fof(f4115,plain,(
% 22.40/3.32 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))),
% 22.40/3.32 inference(resolution,[status(thm)],[f1050,f378])).
% 22.40/3.32 fof(f4222,plain,(
% 22.40/3.32 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))),
% 22.40/3.32 inference(resolution,[status(thm)],[f1056,f378])).
% 22.40/3.32 fof(f4923,plain,(
% 22.40/3.32 ~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))),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f1326,f1022])).
% 22.40/3.32 fof(f5986,plain,(
% 22.40/3.32 ![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)),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f1917,f1047])).
% 22.40/3.32 fof(f8102,plain,(
% 22.40/3.32 v3_struct_0(k1_lattice2(sK0_skl))|k1_filter_0(k1_lattice2(sK0_skl))=k2_filter_0(k1_lattice2(sK0_skl),k6_lattices(sK0_skl))),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f2404,f2806])).
% 22.40/3.32 fof(f13046,plain,(
% 22.40/3.32 v3_struct_0(k1_lattice2(sK0_skl))|u1_struct_0(k1_lattice2(sK0_skl))=k2_filter_0(k1_lattice2(sK0_skl),k6_lattices(sK0_skl))),
% 22.40/3.32 inference(backward_demodulation,[status(thm)],[f13051,f8102])).
% 22.40/3.32 fof(f13051,plain,(
% 22.40/3.32 k1_filter_0(k1_lattice2(sK0_skl))=u1_struct_0(k1_lattice2(sK0_skl))),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f3197,f112])).
% 22.40/3.32 fof(f14432,plain,(
% 22.40/3.32 k18_filter_2(sK0_skl,k6_lattices(sK0_skl))=k2_filter_2(k1_lattice2(sK0_skl),k6_lattices(sK0_skl))),
% 22.40/3.32 inference(forward_demodulation,[status(thm)],[f1840,f2705])).
% 22.40/3.32 fof(f16111,plain,(
% 22.40/3.32 ![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)),
% 22.40/3.32 inference(backward_subsumption_resolution,[status(thm)],[f5986,f4115])).
% 22.40/3.32 fof(f16112,plain,(
% 22.40/3.32 ~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))),
% 22.40/3.32 inference(backward_subsumption_resolution,[status(thm)],[f4923,f4115])).
% 22.40/3.32 fof(f16118,plain,(
% 22.40/3.32 ![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)),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f16111,f1052])).
% 22.40/3.32 fof(f16119,plain,(
% 22.40/3.32 ~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))),
% 22.40/3.32 inference(forward_subsumption_resolution,[status(thm)],[f16112,f1047])).
% 19.26/3.38 fof(f16124,plain,(
% 19.26/3.38 ![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)),
% 19.26/3.38 inference(forward_subsumption_resolution,[status(thm)],[f16118,f1054])).
% 19.26/3.38 fof(f16143,plain,(
% 19.26/3.38 ~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))),
% 19.26/3.38 inference(forward_subsumption_resolution,[status(thm)],[f16119,f1052])).
% 19.26/3.38 fof(f16186,plain,(
% 19.26/3.38 ~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))),
% 19.26/3.38 inference(backward_subsumption_resolution,[status(thm)],[f16143,f4222])).
% 19.26/3.38 fof(f16187,plain,(
% 19.26/3.38 ![X0,X1,X2]: (~k1_lattice2(sK0_skl)=g3_lattices(X0,X1,X2)|u1_struct_0(sK0_skl)=X0)),
% 19.26/3.38 inference(backward_subsumption_resolution,[status(thm)],[f16124,f4222])).
% 19.26/3.38 fof(f16193,plain,(
% 19.26/3.38 ~v3_struct_0(k1_lattice2(sK0_skl))),
% 19.26/3.38 inference(forward_subsumption_resolution,[status(thm)],[f16186,f1054])).
% 19.26/3.38 fof(f16225,plain,(
% 19.26/3.38 ![X0]: (~m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0_skl)))|k2_filter_2(k1_lattice2(sK0_skl),X0)=k2_filter_0(k1_lattice2(sK0_skl),X0))),
% 19.26/3.38 inference(backward_subsumption_resolution,[status(thm)],[f2156,f16193])).
% 19.26/3.38 fof(f16270,plain,(
% 19.26/3.38 u1_struct_0(k1_lattice2(sK0_skl))=k2_filter_0(k1_lattice2(sK0_skl),k6_lattices(sK0_skl))),
% 19.26/3.38 inference(backward_subsumption_resolution,[status(thm)],[f13046,f16193])).
% 19.26/3.38 fof(f16317,plain,(
% 19.26/3.38 u1_struct_0(sK0_skl)=u1_struct_0(k1_lattice2(sK0_skl))),
% 19.26/3.38 inference(resolution,[status(thm)],[f16187,f2911])).
% 19.26/3.38 fof(f17258,plain,(
% 19.26/3.38 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k2_filter_2(k1_lattice2(sK0_skl),X0)=k2_filter_0(k1_lattice2(sK0_skl),X0))),
% 19.26/3.38 inference(backward_demodulation,[status(thm)],[f16317,f16225])).
% 19.26/3.38 fof(f17867,plain,(
% 19.26/3.38 u1_struct_0(sK0_skl)=k2_filter_0(k1_lattice2(sK0_skl),k6_lattices(sK0_skl))),
% 19.26/3.38 inference(forward_demodulation,[status(thm)],[f16317,f16270])).
% 19.26/3.38 fof(f17898,plain,(
% 19.26/3.38 k2_filter_2(k1_lattice2(sK0_skl),k6_lattices(sK0_skl))=k2_filter_0(k1_lattice2(sK0_skl),k6_lattices(sK0_skl))),
% 19.26/3.38 inference(resolution,[status(thm)],[f17258,f858])).
% 19.26/3.38 fof(f17902,plain,(
% 19.26/3.38 k18_filter_2(sK0_skl,k6_lattices(sK0_skl))=k2_filter_0(k1_lattice2(sK0_skl),k6_lattices(sK0_skl))),
% 19.26/3.38 inference(forward_demodulation,[status(thm)],[f14432,f17898])).
% 19.26/3.38 fof(f17903,plain,(
% 19.26/3.38 k18_filter_2(sK0_skl,k6_lattices(sK0_skl))=u1_struct_0(sK0_skl)),
% 19.26/3.38 inference(forward_demodulation,[status(thm)],[f17867,f17902])).
% 19.26/3.38 fof(f17970,plain,(
% 19.26/3.38 ~r1_filter_2(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),u1_struct_0(sK0_skl))),
% 19.26/3.38 inference(backward_demodulation,[status(thm)],[f17903,f460])).
% 19.26/3.38 fof(f17971,plain,(
% 19.26/3.38 $false),
% 19.26/3.38 inference(forward_subsumption_resolution,[status(thm)],[f17970,f3149])).
% 19.26/3.38 % SZS output end CNFRefutation for theBenchmark.p
% 11.95/3.41 % Elapsed time: 3.043270 seconds
% 11.95/3.41 % CPU time: 23.633971 seconds
% 11.95/3.41 % Total memory used: 388.311 MB
% 11.95/3.41 % Net memory used: 379.722 MB
%------------------------------------------------------------------------------