%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT331+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:03:43 PM UTC 2026
% Result : Theorem 8.25s 1.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT331+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.44 % Computer : n026.cluster.edu
% 0.20/0.44 % Model : x86_64 x86_64
% 0.20/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.44 % Memory : 8046.5625MB
% 0.20/0.44 % OS : Linux 6.8.0-71-generic
% 0.20/0.44 % CPULimit : 300
% 0.20/0.44 % WCLimit : 300
% 0.20/0.44 % DateTime : Sun Sep 20 23:42:36 UTC 2026
% 0.20/0.45 % CPUTime :
% 0.20/0.48 % Drodi V4.1.1
% 8.25/1.59 % Refutation found
% 8.25/1.59 % SZS status Theorem for theBenchmark: Theorem is valid
% 8.25/1.59 % SZS output start CNFRefutation for theBenchmark
% 8.25/1.59 fof(f1,conjecture,(
% 8.25/1.59 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v10_lattices(B)& l3_lattices(B) )=> (! [C] :( m1_filter_2(C,A)=> (! [D] :( m1_filter_2(D,B)=> ( ( g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) = g3_lattices(u1_struct_0(B),u2_lattices(B),u1_lattices(B))& C = D )=> k8_filter_0(A,C) = k8_filter_0(B,D) ) ) )) )) )) )),
% 8.25/1.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.25/1.59 fof(f2,negated_conjecture,(
% 8.25/1.59 ~((! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v10_lattices(B)& l3_lattices(B) )=> (! [C] :( m1_filter_2(C,A)=> (! [D] :( m1_filter_2(D,B)=> ( ( g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) = g3_lattices(u1_struct_0(B),u2_lattices(B),u1_lattices(B))& C = D )=> k8_filter_0(A,C) = k8_filter_0(B,D) ) ) )) )) )) ))),
% 8.25/1.59 inference(negated_conjecture,[status(cth)],[f1])).
% 8.25/1.59 fof(f10,axiom,(
% 8.25/1.59 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_filter_0(B,A)=> (! [C] :( ( ~ v3_struct_0(C)& v10_lattices(C)& l3_lattices(C) )=> ( C = k8_filter_0(A,B)<=> (? [D] :( v1_funct_1(D)& v1_funct_2(D,k2_zfmisc_1(B,B),B)& m2_relset_1(D,k2_zfmisc_1(B,B),B)& (? [E] :( v1_funct_1(E)& v1_funct_2(E,k2_zfmisc_1(B,B),B)& m2_relset_1(E,k2_zfmisc_1(B,B),B)& D = k1_realset1(u2_lattices(A),B)& E = k1_realset1(u1_lattices(A),B)& C = g3_lattices(B,D,E) ) )) )) ) )) )) )),
% 8.25/1.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.25/1.59 fof(f18,axiom,(
% 8.25/1.59 (! [A,B] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A)& m1_filter_0(B,A) )=> ( ~ v3_struct_0(k8_filter_0(A,B))& v10_lattices(k8_filter_0(A,B))& l3_lattices(k8_filter_0(A,B)) ) ) )),
% 8.25/1.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.25/1.59 fof(f22,axiom,(
% 8.25/1.59 (! [A] :( l3_lattices(A)=> ( l1_lattices(A)& l2_lattices(A) ) ) )),
% 8.25/1.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.25/1.59 fof(f29,axiom,(
% 8.25/1.59 (! [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)) ) ) )),
% 8.25/1.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.25/1.59 fof(f31,axiom,(
% 8.25/1.59 (! [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)) ) ) )),
% 8.25/1.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.25/1.59 fof(f55,axiom,(
% 8.25/1.59 (! [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 ) ) )) )),
% 8.25/1.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.25/1.59 fof(f69,axiom,(
% 8.25/1.59 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_filter_2(B,A)<=> m1_filter_0(B,A) ) )) )),
% 8.25/1.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.25/1.59 fof(f70,axiom,(
% 8.25/1.59 (! [A,B,C] :( m2_relset_1(C,A,B)<=> m1_relset_1(C,A,B) ) )),
% 8.25/1.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.25/1.59 fof(f80,plain,(
% 8.25/1.59 (?[A]: (((~v3_struct_0(A)&v10_lattices(A))&l3_lattices(A))&(?[B]: (((~v3_struct_0(B)&v10_lattices(B))&l3_lattices(B))&(?[C]: (m1_filter_2(C,A)&(?[D]: (m1_filter_2(D,B)&((g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A))=g3_lattices(u1_struct_0(B),u2_lattices(B),u1_lattices(B))&C=D)&~k8_filter_0(A,C)=k8_filter_0(B,D))))))))))),
% 8.25/1.59 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 8.25/1.59 fof(f81,plain,(
% 8.25/1.59 (((~v3_struct_0(sK0_skl)&v10_lattices(sK0_skl))&l3_lattices(sK0_skl))&(((~v3_struct_0(sK1_skl)&v10_lattices(sK1_skl))&l3_lattices(sK1_skl))&(m1_filter_2(sK2_skl,sK0_skl)&(m1_filter_2(sK3_skl,sK1_skl)&((g3_lattices(u1_struct_0(sK0_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl))=g3_lattices(u1_struct_0(sK1_skl),u2_lattices(sK1_skl),u1_lattices(sK1_skl))&sK2_skl=sK3_skl)&~k8_filter_0(sK0_skl,sK2_skl)=k8_filter_0(sK1_skl,sK3_skl))))))),
% 8.25/1.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl),skolemize(D,sK3_skl)],[f80])).
% 8.25/1.59 fof(f82,plain,(
% 8.25/1.59 ~v3_struct_0(sK0_skl)),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f81])).
% 8.25/1.59 fof(f83,plain,(
% 8.25/1.59 v10_lattices(sK0_skl)),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f81])).
% 8.25/1.59 fof(f84,plain,(
% 8.25/1.59 l3_lattices(sK0_skl)),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f81])).
% 8.25/1.59 fof(f85,plain,(
% 8.25/1.59 ~v3_struct_0(sK1_skl)),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f81])).
% 8.25/1.59 fof(f86,plain,(
% 8.25/1.59 v10_lattices(sK1_skl)),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f81])).
% 8.25/1.59 fof(f87,plain,(
% 8.25/1.59 l3_lattices(sK1_skl)),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f81])).
% 8.25/1.59 fof(f88,plain,(
% 8.25/1.59 m1_filter_2(sK2_skl,sK0_skl)),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f81])).
% 8.25/1.59 fof(f89,plain,(
% 8.25/1.59 m1_filter_2(sK3_skl,sK1_skl)),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f81])).
% 8.25/1.59 fof(f90,plain,(
% 8.25/1.59 g3_lattices(u1_struct_0(sK0_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl))=g3_lattices(u1_struct_0(sK1_skl),u2_lattices(sK1_skl),u1_lattices(sK1_skl))),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f81])).
% 8.25/1.59 fof(f91,plain,(
% 8.25/1.59 sK2_skl=sK3_skl),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f81])).
% 8.25/1.59 fof(f92,plain,(
% 8.25/1.59 ~k8_filter_0(sK0_skl,sK2_skl)=k8_filter_0(sK1_skl,sK3_skl)),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f81])).
% 8.25/1.59 fof(f117,plain,(
% 8.25/1.59 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m1_filter_0(B,A)|(![C]: (((v3_struct_0(C)|~v10_lattices(C))|~l3_lattices(C))|(C=k8_filter_0(A,B)<=>(?[D]: (((v1_funct_1(D)&v1_funct_2(D,k2_zfmisc_1(B,B),B))&m2_relset_1(D,k2_zfmisc_1(B,B),B))&(?[E]: (((((v1_funct_1(E)&v1_funct_2(E,k2_zfmisc_1(B,B),B))&m2_relset_1(E,k2_zfmisc_1(B,B),B))&D=k1_realset1(u2_lattices(A),B))&E=k1_realset1(u1_lattices(A),B))&C=g3_lattices(B,D,E)))))))))))),
% 8.25/1.59 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 8.25/1.59 fof(f118,plain,(
% 8.25/1.59 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m1_filter_0(B,A)|(![C]: (((v3_struct_0(C)|~v10_lattices(C))|~l3_lattices(C))|((~C=k8_filter_0(A,B)|(?[D]: (((v1_funct_1(D)&v1_funct_2(D,k2_zfmisc_1(B,B),B))&m2_relset_1(D,k2_zfmisc_1(B,B),B))&(?[E]: (((((v1_funct_1(E)&v1_funct_2(E,k2_zfmisc_1(B,B),B))&m2_relset_1(E,k2_zfmisc_1(B,B),B))&D=k1_realset1(u2_lattices(A),B))&E=k1_realset1(u1_lattices(A),B))&C=g3_lattices(B,D,E))))))&(C=k8_filter_0(A,B)|(![D]: (((~v1_funct_1(D)|~v1_funct_2(D,k2_zfmisc_1(B,B),B))|~m2_relset_1(D,k2_zfmisc_1(B,B),B))|(![E]: (((((~v1_funct_1(E)|~v1_funct_2(E,k2_zfmisc_1(B,B),B))|~m2_relset_1(E,k2_zfmisc_1(B,B),B))|~D=k1_realset1(u2_lattices(A),B))|~E=k1_realset1(u1_lattices(A),B))|~C=g3_lattices(B,D,E))))))))))))),
% 8.25/1.59 inference(NNF_transformation,[status(thm)],[f117])).
% 8.25/1.59 fof(f119,plain,(
% 8.25/1.59 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m1_filter_0(B,A)|(![C]: (((v3_struct_0(C)|~v10_lattices(C))|~l3_lattices(C))|((~C=k8_filter_0(A,B)|(((v1_funct_1(sK4_skl(C,B,A))&v1_funct_2(sK4_skl(C,B,A),k2_zfmisc_1(B,B),B))&m2_relset_1(sK4_skl(C,B,A),k2_zfmisc_1(B,B),B))&(((((v1_funct_1(sK5_skl(C,B,A))&v1_funct_2(sK5_skl(C,B,A),k2_zfmisc_1(B,B),B))&m2_relset_1(sK5_skl(C,B,A),k2_zfmisc_1(B,B),B))&sK4_skl(C,B,A)=k1_realset1(u2_lattices(A),B))&sK5_skl(C,B,A)=k1_realset1(u1_lattices(A),B))&C=g3_lattices(B,sK4_skl(C,B,A),sK5_skl(C,B,A)))))&(C=k8_filter_0(A,B)|(![D]: (((~v1_funct_1(D)|~v1_funct_2(D,k2_zfmisc_1(B,B),B))|~m2_relset_1(D,k2_zfmisc_1(B,B),B))|(![E]: (((((~v1_funct_1(E)|~v1_funct_2(E,k2_zfmisc_1(B,B),B))|~m2_relset_1(E,k2_zfmisc_1(B,B),B))|~D=k1_realset1(u2_lattices(A),B))|~E=k1_realset1(u1_lattices(A),B))|~C=g3_lattices(B,D,E))))))))))))),
% 8.25/1.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl]),skolemize(D,sK4_skl(C,B,A)),skolemize(E,sK5_skl(C,B,A))],[f118])).
% 8.25/1.59 fof(f126,plain,(
% 8.25/1.59 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|v3_struct_0(X2)|~v10_lattices(X2)|~l3_lattices(X2)|~X2=k8_filter_0(X0,X1)|sK4_skl(X2,X1,X0)=k1_realset1(u2_lattices(X0),X1))),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f119])).
% 8.25/1.59 fof(f127,plain,(
% 8.25/1.59 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|v3_struct_0(X2)|~v10_lattices(X2)|~l3_lattices(X2)|~X2=k8_filter_0(X0,X1)|sK5_skl(X2,X1,X0)=k1_realset1(u1_lattices(X0),X1))),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f119])).
% 8.25/1.59 fof(f128,plain,(
% 8.25/1.59 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|v3_struct_0(X2)|~v10_lattices(X2)|~l3_lattices(X2)|~X2=k8_filter_0(X0,X1)|X2=g3_lattices(X1,sK4_skl(X2,X1,X0),sK5_skl(X2,X1,X0)))),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f119])).
% 8.25/1.59 fof(f138,plain,(
% 8.25/1.59 ![A,B]: ((((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|~m1_filter_0(B,A))|((~v3_struct_0(k8_filter_0(A,B))&v10_lattices(k8_filter_0(A,B)))&l3_lattices(k8_filter_0(A,B))))),
% 8.25/1.59 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 8.25/1.59 fof(f139,plain,(
% 8.25/1.59 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|~v3_struct_0(k8_filter_0(X0,X1)))),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f138])).
% 8.25/1.59 fof(f140,plain,(
% 8.25/1.59 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|v10_lattices(k8_filter_0(X0,X1)))),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f138])).
% 8.25/1.59 fof(f141,plain,(
% 8.25/1.59 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|l3_lattices(k8_filter_0(X0,X1)))),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f138])).
% 8.25/1.59 fof(f146,plain,(
% 8.25/1.59 ![A]: (~l3_lattices(A)|(l1_lattices(A)&l2_lattices(A)))),
% 8.25/1.59 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 8.25/1.59 fof(f147,plain,(
% 8.25/1.59 ![X0]: (~l3_lattices(X0)|l1_lattices(X0))),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f146])).
% 8.25/1.59 fof(f148,plain,(
% 8.25/1.59 ![X0]: (~l3_lattices(X0)|l2_lattices(X0))),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f146])).
% 8.25/1.59 fof(f159,plain,(
% 8.25/1.59 ![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))))),
% 8.25/1.59 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 8.25/1.59 fof(f160,plain,(
% 8.25/1.59 ![X0]: (~l1_lattices(X0)|v1_funct_1(u1_lattices(X0)))),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f159])).
% 8.25/1.59 fof(f161,plain,(
% 8.25/1.59 ![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)))),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f159])).
% 8.25/1.59 fof(f162,plain,(
% 8.25/1.59 ![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)))),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f159])).
% 8.25/1.59 fof(f163,plain,(
% 8.25/1.59 ![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))))),
% 8.25/1.59 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 8.25/1.59 fof(f164,plain,(
% 8.25/1.59 ![X0]: (~l2_lattices(X0)|v1_funct_1(u2_lattices(X0)))),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f163])).
% 8.25/1.59 fof(f165,plain,(
% 8.25/1.59 ![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)))),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f163])).
% 8.25/1.59 fof(f166,plain,(
% 8.25/1.59 ![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)))),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f163])).
% 8.25/1.59 fof(f244,plain,(
% 8.25/1.59 ![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))))),
% 8.25/1.59 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 8.25/1.59 fof(f245,plain,(
% 8.25/1.59 ![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)),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f244])).
% 8.25/1.59 fof(f246,plain,(
% 8.25/1.59 ![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)|X0=X4)),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f244])).
% 8.25/1.59 fof(f247,plain,(
% 8.25/1.59 ![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)),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f244])).
% 8.25/1.59 fof(f299,plain,(
% 8.25/1.59 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (m1_filter_2(B,A)<=>m1_filter_0(B,A))))),
% 8.25/1.59 inference(pre_NNF_transformation,[status(thm)],[f69])).
% 8.25/1.59 fof(f300,plain,(
% 8.25/1.59 ![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)))))),
% 8.25/1.59 inference(NNF_transformation,[status(thm)],[f299])).
% 8.25/1.59 fof(f301,plain,(
% 8.25/1.59 ![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)))))),
% 8.25/1.59 inference(miniscoping,[status(thm)],[f300])).
% 8.25/1.59 fof(f302,plain,(
% 8.25/1.59 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_2(X1,X0)|m1_filter_0(X1,X0))),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f301])).
% 8.25/1.59 fof(f304,plain,(
% 8.25/1.59 ![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)))),
% 8.25/1.59 inference(NNF_transformation,[status(thm)],[f70])).
% 8.25/1.59 fof(f305,plain,(
% 8.25/1.59 (![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)))),
% 8.25/1.59 inference(miniscoping,[status(thm)],[f304])).
% 8.25/1.59 fof(f306,plain,(
% 8.25/1.59 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_relset_1(X0,X1,X2))),
% 8.25/1.59 inference(cnf_transformation,[status(thm)],[f305])).
% 8.25/1.59 fof(f332,plain,(
% 8.25/1.59 m1_filter_2(sK3_skl,sK0_skl)),
% 8.25/1.59 inference(backward_demodulation,[status(thm)],[f91,f88])).
% 8.25/1.59 fof(f333,plain,(
% 8.25/1.59 ~k8_filter_0(sK0_skl,sK3_skl)=k8_filter_0(sK1_skl,sK3_skl)),
% 8.25/1.59 inference(forward_demodulation,[status(thm)],[f91,f92])).
% 8.25/1.59 fof(f341,plain,(
% 8.25/1.59 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|v3_struct_0(k8_filter_0(X0,X1))|~v10_lattices(k8_filter_0(X0,X1))|~l3_lattices(k8_filter_0(X0,X1))|sK4_skl(k8_filter_0(X0,X1),X1,X0)=k1_realset1(u2_lattices(X0),X1))),
% 8.25/1.59 inference(destructive_equality_resolution,[status(thm)],[f126])).
% 8.25/1.59 fof(f342,plain,(
% 8.25/1.59 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|v3_struct_0(k8_filter_0(X0,X1))|~v10_lattices(k8_filter_0(X0,X1))|~l3_lattices(k8_filter_0(X0,X1))|sK5_skl(k8_filter_0(X0,X1),X1,X0)=k1_realset1(u1_lattices(X0),X1))),
% 8.25/1.59 inference(destructive_equality_resolution,[status(thm)],[f127])).
% 8.25/1.59 fof(f343,plain,(
% 8.25/1.59 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|v3_struct_0(k8_filter_0(X0,X1))|~v10_lattices(k8_filter_0(X0,X1))|~l3_lattices(k8_filter_0(X0,X1))|k8_filter_0(X0,X1)=g3_lattices(X1,sK4_skl(k8_filter_0(X0,X1),X1,X0),sK5_skl(k8_filter_0(X0,X1),X1,X0)))),
% 8.25/1.59 inference(destructive_equality_resolution,[status(thm)],[f128])).
% 8.25/1.59 fof(f345,plain,(
% 8.25/1.59 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|~v10_lattices(k8_filter_0(X0,X1))|~l3_lattices(k8_filter_0(X0,X1))|k8_filter_0(X0,X1)=g3_lattices(X1,sK4_skl(k8_filter_0(X0,X1),X1,X0),sK5_skl(k8_filter_0(X0,X1),X1,X0)))),
% 8.25/1.59 inference(backward_subsumption_resolution,[status(thm)],[f343,f139])).
% 8.25/1.59 fof(f346,plain,(
% 8.25/1.59 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|~v10_lattices(k8_filter_0(X0,X1))|~l3_lattices(k8_filter_0(X0,X1))|sK5_skl(k8_filter_0(X0,X1),X1,X0)=k1_realset1(u1_lattices(X0),X1))),
% 8.25/1.59 inference(backward_subsumption_resolution,[status(thm)],[f342,f139])).
% 8.25/1.59 fof(f347,plain,(
% 8.25/1.59 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|~v10_lattices(k8_filter_0(X0,X1))|~l3_lattices(k8_filter_0(X0,X1))|sK4_skl(k8_filter_0(X0,X1),X1,X0)=k1_realset1(u2_lattices(X0),X1))),
% 8.25/1.59 inference(backward_subsumption_resolution,[status(thm)],[f341,f139])).
% 8.25/1.59 fof(f354,plain,(
% 8.25/1.59 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|~l3_lattices(k8_filter_0(X0,X1))|k8_filter_0(X0,X1)=g3_lattices(X1,sK4_skl(k8_filter_0(X0,X1),X1,X0),sK5_skl(k8_filter_0(X0,X1),X1,X0)))),
% 8.25/1.59 inference(forward_subsumption_resolution,[status(thm)],[f345,f140])).
% 8.25/1.59 fof(f355,plain,(
% 8.25/1.59 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|~l3_lattices(k8_filter_0(X0,X1))|sK5_skl(k8_filter_0(X0,X1),X1,X0)=k1_realset1(u1_lattices(X0),X1))),
% 8.25/1.59 inference(forward_subsumption_resolution,[status(thm)],[f346,f140])).
% 8.25/1.59 fof(f356,plain,(
% 8.25/1.59 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|~l3_lattices(k8_filter_0(X0,X1))|sK4_skl(k8_filter_0(X0,X1),X1,X0)=k1_realset1(u2_lattices(X0),X1))),
% 8.25/1.59 inference(forward_subsumption_resolution,[status(thm)],[f347,f140])).
% 8.25/1.59 fof(f363,plain,(
% 8.25/1.59 ![X0]: (v3_struct_0(sK1_skl)|~l3_lattices(sK1_skl)|~m1_filter_2(X0,sK1_skl)|m1_filter_0(X0,sK1_skl))),
% 8.25/1.59 inference(resolution,[status(thm)],[f302,f86])).
% 8.25/1.59 fof(f364,plain,(
% 8.25/1.59 ![X0]: (v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|~m1_filter_2(X0,sK0_skl)|m1_filter_0(X0,sK0_skl))),
% 8.25/1.59 inference(resolution,[status(thm)],[f302,f83])).
% 8.25/1.59 fof(f365,plain,(
% 8.25/1.59 ![X0]: (~l3_lattices(sK1_skl)|~m1_filter_2(X0,sK1_skl)|m1_filter_0(X0,sK1_skl))),
% 8.25/1.59 inference(forward_subsumption_resolution,[status(thm)],[f363,f85])).
% 8.25/1.59 fof(f366,plain,(
% 8.25/1.59 ![X0]: (~l3_lattices(sK0_skl)|~m1_filter_2(X0,sK0_skl)|m1_filter_0(X0,sK0_skl))),
% 8.25/1.59 inference(forward_subsumption_resolution,[status(thm)],[f364,f82])).
% 8.25/1.59 fof(f367,plain,(
% 8.25/1.59 ![X0]: (~m1_filter_2(X0,sK1_skl)|m1_filter_0(X0,sK1_skl))),
% 8.25/1.59 inference(resolution,[status(thm)],[f365,f87])).
% 8.25/1.59 fof(f376,plain,(
% 8.25/1.59 m1_filter_0(sK3_skl,sK1_skl)),
% 8.25/1.59 inference(resolution,[status(thm)],[f367,f89])).
% 8.25/1.59 fof(f377,plain,(
% 8.25/1.59 ![X0]: (~m1_filter_2(X0,sK0_skl)|m1_filter_0(X0,sK0_skl))),
% 8.25/1.59 inference(resolution,[status(thm)],[f366,f84])).
% 8.25/1.59 fof(f378,plain,(
% 8.25/1.59 m1_filter_0(sK3_skl,sK0_skl)),
% 8.25/1.59 inference(resolution,[status(thm)],[f377,f332])).
% 8.25/1.59 fof(f462,plain,(
% 8.25/1.59 l1_lattices(sK0_skl)),
% 8.25/1.59 inference(resolution,[status(thm)],[f147,f84])).
% 8.25/1.59 fof(f476,plain,(
% 8.25/1.59 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|k8_filter_0(X0,X1)=g3_lattices(X1,sK4_skl(k8_filter_0(X0,X1),X1,X0),sK5_skl(k8_filter_0(X0,X1),X1,X0))|v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0))),
% 8.25/1.59 inference(resolution,[status(thm)],[f354,f141])).
% 8.25/1.59 fof(f477,plain,(
% 8.25/1.59 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|k8_filter_0(X0,X1)=g3_lattices(X1,sK4_skl(k8_filter_0(X0,X1),X1,X0),sK5_skl(k8_filter_0(X0,X1),X1,X0)))),
% 8.25/1.59 inference(duplicate_literals_removal,[status(thm)],[f476])).
% 8.25/1.59 fof(f485,plain,(
% 8.25/1.59 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|sK5_skl(k8_filter_0(X0,X1),X1,X0)=k1_realset1(u1_lattices(X0),X1)|v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0))),
% 8.25/1.59 inference(resolution,[status(thm)],[f355,f141])).
% 8.25/1.59 fof(f486,plain,(
% 8.25/1.59 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|sK5_skl(k8_filter_0(X0,X1),X1,X0)=k1_realset1(u1_lattices(X0),X1))),
% 8.25/1.59 inference(duplicate_literals_removal,[status(thm)],[f485])).
% 8.25/1.59 fof(f487,plain,(
% 8.25/1.59 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|sK5_skl(k8_filter_0(sK0_skl,sK3_skl),sK3_skl,sK0_skl)=k1_realset1(u1_lattices(sK0_skl),sK3_skl)),
% 8.25/1.59 inference(resolution,[status(thm)],[f486,f378])).
% 8.25/1.59 fof(f488,plain,(
% 8.25/1.59 v3_struct_0(sK1_skl)|~v10_lattices(sK1_skl)|~l3_lattices(sK1_skl)|sK5_skl(k8_filter_0(sK1_skl,sK3_skl),sK3_skl,sK1_skl)=k1_realset1(u1_lattices(sK1_skl),sK3_skl)),
% 8.25/1.59 inference(resolution,[status(thm)],[f486,f376])).
% 8.25/1.59 fof(f489,plain,(
% 8.25/1.59 ~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|sK5_skl(k8_filter_0(sK0_skl,sK3_skl),sK3_skl,sK0_skl)=k1_realset1(u1_lattices(sK0_skl),sK3_skl)),
% 8.25/1.59 inference(forward_subsumption_resolution,[status(thm)],[f487,f82])).
% 8.25/1.59 fof(f490,plain,(
% 8.25/1.59 ~v10_lattices(sK1_skl)|~l3_lattices(sK1_skl)|sK5_skl(k8_filter_0(sK1_skl,sK3_skl),sK3_skl,sK1_skl)=k1_realset1(u1_lattices(sK1_skl),sK3_skl)),
% 8.25/1.59 inference(forward_subsumption_resolution,[status(thm)],[f488,f85])).
% 8.25/1.59 fof(f491,plain,(
% 8.25/1.59 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|sK4_skl(k8_filter_0(X0,X1),X1,X0)=k1_realset1(u2_lattices(X0),X1)|v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0))),
% 8.25/1.59 inference(resolution,[status(thm)],[f356,f141])).
% 8.25/1.59 fof(f492,plain,(
% 8.25/1.59 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|sK4_skl(k8_filter_0(X0,X1),X1,X0)=k1_realset1(u2_lattices(X0),X1))),
% 8.25/1.59 inference(duplicate_literals_removal,[status(thm)],[f491])).
% 8.25/1.59 fof(f499,plain,(
% 8.25/1.59 l2_lattices(sK0_skl)),
% 8.25/1.59 inference(resolution,[status(thm)],[f148,f84])).
% 8.25/1.59 fof(f503,plain,(
% 8.25/1.59 ~l3_lattices(sK0_skl)|sK5_skl(k8_filter_0(sK0_skl,sK3_skl),sK3_skl,sK0_skl)=k1_realset1(u1_lattices(sK0_skl),sK3_skl)),
% 8.25/1.59 inference(resolution,[status(thm)],[f489,f83])).
% 8.25/1.59 fof(f505,plain,(
% 8.25/1.59 sK5_skl(k8_filter_0(sK0_skl,sK3_skl),sK3_skl,sK0_skl)=k1_realset1(u1_lattices(sK0_skl),sK3_skl)),
% 8.25/1.59 inference(forward_subsumption_resolution,[status(thm)],[f503,f84])).
% 8.25/1.59 fof(f514,plain,(
% 8.25/1.59 ~l3_lattices(sK1_skl)|sK5_skl(k8_filter_0(sK1_skl,sK3_skl),sK3_skl,sK1_skl)=k1_realset1(u1_lattices(sK1_skl),sK3_skl)),
% 8.25/1.59 inference(resolution,[status(thm)],[f490,f86])).
% 8.25/1.59 fof(f516,plain,(
% 8.25/1.59 sK5_skl(k8_filter_0(sK1_skl,sK3_skl),sK3_skl,sK1_skl)=k1_realset1(u1_lattices(sK1_skl),sK3_skl)),
% 8.25/1.59 inference(forward_subsumption_resolution,[status(thm)],[f514,f87])).
% 8.25/1.59 fof(f525,plain,(
% 8.25/1.59 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|sK4_skl(k8_filter_0(sK0_skl,sK3_skl),sK3_skl,sK0_skl)=k1_realset1(u2_lattices(sK0_skl),sK3_skl)),
% 8.25/1.59 inference(resolution,[status(thm)],[f492,f378])).
% 8.25/1.59 fof(f526,plain,(
% 8.25/1.59 v3_struct_0(sK1_skl)|~v10_lattices(sK1_skl)|~l3_lattices(sK1_skl)|sK4_skl(k8_filter_0(sK1_skl,sK3_skl),sK3_skl,sK1_skl)=k1_realset1(u2_lattices(sK1_skl),sK3_skl)),
% 8.25/1.59 inference(resolution,[status(thm)],[f492,f376])).
% 8.25/1.59 fof(f527,plain,(
% 8.25/1.59 ~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|sK4_skl(k8_filter_0(sK0_skl,sK3_skl),sK3_skl,sK0_skl)=k1_realset1(u2_lattices(sK0_skl),sK3_skl)),
% 8.25/1.59 inference(forward_subsumption_resolution,[status(thm)],[f525,f82])).
% 8.25/1.59 fof(f528,plain,(
% 8.25/1.59 ~v10_lattices(sK1_skl)|~l3_lattices(sK1_skl)|sK4_skl(k8_filter_0(sK1_skl,sK3_skl),sK3_skl,sK1_skl)=k1_realset1(u2_lattices(sK1_skl),sK3_skl)),
% 8.25/1.59 inference(forward_subsumption_resolution,[status(thm)],[f526,f85])).
% 8.25/1.59 fof(f529,plain,(
% 8.25/1.59 ~l3_lattices(sK0_skl)|sK4_skl(k8_filter_0(sK0_skl,sK3_skl),sK3_skl,sK0_skl)=k1_realset1(u2_lattices(sK0_skl),sK3_skl)),
% 8.25/1.59 inference(resolution,[status(thm)],[f527,f83])).
% 8.25/1.59 fof(f531,plain,(
% 8.25/1.59 sK4_skl(k8_filter_0(sK0_skl,sK3_skl),sK3_skl,sK0_skl)=k1_realset1(u2_lattices(sK0_skl),sK3_skl)),
% 8.25/1.59 inference(forward_subsumption_resolution,[status(thm)],[f529,f84])).
% 8.25/1.59 fof(f583,plain,(
% 8.25/1.59 ~l3_lattices(sK1_skl)|sK4_skl(k8_filter_0(sK1_skl,sK3_skl),sK3_skl,sK1_skl)=k1_realset1(u2_lattices(sK1_skl),sK3_skl)),
% 8.25/1.59 inference(resolution,[status(thm)],[f528,f86])).
% 8.25/1.59 fof(f585,plain,(
% 8.25/1.59 sK4_skl(k8_filter_0(sK1_skl,sK3_skl),sK3_skl,sK1_skl)=k1_realset1(u2_lattices(sK1_skl),sK3_skl)),
% 8.25/1.59 inference(forward_subsumption_resolution,[status(thm)],[f583,f87])).
% 8.25/1.59 fof(f697,plain,(
% 8.25/1.59 ![X0,X1,X2,X3,X4]: (~l1_lattices(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~m1_relset_1(X1,k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~v1_funct_1(u1_lattices(X0))|~m1_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~g3_lattices(u1_struct_0(X0),X1,u1_lattices(X0))=g3_lattices(X2,X3,X4)|u1_lattices(X0)=X4)),
% 8.25/1.59 inference(resolution,[status(thm)],[f161,f247])).
% 8.25/1.59 fof(f698,plain,(
% 8.25/1.59 ![X0,X1,X2,X3,X4]: (~l1_lattices(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~m1_relset_1(X1,k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~v1_funct_1(u1_lattices(X0))|~m1_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~g3_lattices(u1_struct_0(X0),X1,u1_lattices(X0))=g3_lattices(X2,X3,X4)|X1=X3)),
% 8.25/1.59 inference(resolution,[status(thm)],[f161,f246])).
% 8.25/1.59 fof(f699,plain,(
% 8.25/1.59 ![X0,X1,X2,X3,X4]: (~l1_lattices(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~m1_relset_1(X1,k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~v1_funct_1(u1_lattices(X0))|~m1_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~g3_lattices(u1_struct_0(X0),X1,u1_lattices(X0))=g3_lattices(X2,X3,X4)|u1_struct_0(X0)=X2)),
% 8.25/1.59 inference(resolution,[status(thm)],[f161,f245])).
% 8.25/1.59 fof(f702,plain,(
% 8.25/1.59 ![X0,X1,X2,X3,X4]: (~l1_lattices(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~m1_relset_1(X1,k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~m1_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~g3_lattices(u1_struct_0(X0),X1,u1_lattices(X0))=g3_lattices(X2,X3,X4)|u1_lattices(X0)=X4)),
% 8.25/1.59 inference(forward_subsumption_resolution,[status(thm)],[f697,f160])).
% 8.25/1.59 fof(f703,plain,(
% 8.25/1.59 ![X0,X1,X2,X3,X4]: (~l1_lattices(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~m1_relset_1(X1,k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~m1_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~g3_lattices(u1_struct_0(X0),X1,u1_lattices(X0))=g3_lattices(X2,X3,X4)|X1=X3)),
% 8.25/1.59 inference(forward_subsumption_resolution,[status(thm)],[f698,f160])).
% 8.25/1.59 fof(f704,plain,(
% 8.25/1.59 ![X0,X1,X2,X3,X4]: (~l1_lattices(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~m1_relset_1(X1,k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~m1_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~g3_lattices(u1_struct_0(X0),X1,u1_lattices(X0))=g3_lattices(X2,X3,X4)|u1_struct_0(X0)=X2)),
% 8.25/1.59 inference(forward_subsumption_resolution,[status(thm)],[f699,f160])).
% 8.25/1.59 fof(f707,plain,(
% 8.25/1.59 ![X0]: (~l1_lattices(X0)|m1_relset_1(u1_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)))),
% 8.25/1.59 inference(resolution,[status(thm)],[f162,f306])).
% 8.25/1.59 fof(f709,plain,(
% 8.25/1.59 ![X0,X1,X2,X3,X4]: (~l1_lattices(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~m1_relset_1(X1,k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~g3_lattices(u1_struct_0(X0),X1,u1_lattices(X0))=g3_lattices(X2,X3,X4)|u1_struct_0(X0)=X2)),
% 8.25/1.59 inference(backward_subsumption_resolution,[status(thm)],[f704,f707])).
% 8.25/1.59 fof(f710,plain,(
% 8.25/1.59 ![X0,X1,X2,X3,X4]: (~l1_lattices(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~m1_relset_1(X1,k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~g3_lattices(u1_struct_0(X0),X1,u1_lattices(X0))=g3_lattices(X2,X3,X4)|X1=X3)),
% 8.25/1.59 inference(backward_subsumption_resolution,[status(thm)],[f703,f707])).
% 8.25/1.59 fof(f711,plain,(
% 8.25/1.59 ![X0,X1,X2,X3,X4]: (~l1_lattices(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~m1_relset_1(X1,k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~g3_lattices(u1_struct_0(X0),X1,u1_lattices(X0))=g3_lattices(X2,X3,X4)|u1_lattices(X0)=X4)),
% 8.25/1.59 inference(backward_subsumption_resolution,[status(thm)],[f702,f707])).
% 8.25/1.59 fof(f766,plain,(
% 8.25/1.59 ![X0]: (~l2_lattices(X0)|m1_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)))),
% 8.25/1.59 inference(resolution,[status(thm)],[f166,f306])).
% 8.25/1.59 fof(f860,plain,(
% 8.25/1.59 ![X0]: (v3_struct_0(sK1_skl)|~l3_lattices(sK1_skl)|~m1_filter_0(X0,sK1_skl)|k8_filter_0(sK1_skl,X0)=g3_lattices(X0,sK4_skl(k8_filter_0(sK1_skl,X0),X0,sK1_skl),sK5_skl(k8_filter_0(sK1_skl,X0),X0,sK1_skl)))),
% 8.25/1.59 inference(resolution,[status(thm)],[f477,f86])).
% 8.25/1.59 fof(f861,plain,(
% 8.25/1.59 ![X0]: (v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|~m1_filter_0(X0,sK0_skl)|k8_filter_0(sK0_skl,X0)=g3_lattices(X0,sK4_skl(k8_filter_0(sK0_skl,X0),X0,sK0_skl),sK5_skl(k8_filter_0(sK0_skl,X0),X0,sK0_skl)))),
% 8.25/1.59 inference(resolution,[status(thm)],[f477,f83])).
% 8.25/1.59 fof(f864,plain,(
% 8.25/1.59 ![X0]: (~l3_lattices(sK1_skl)|~m1_filter_0(X0,sK1_skl)|k8_filter_0(sK1_skl,X0)=g3_lattices(X0,sK4_skl(k8_filter_0(sK1_skl,X0),X0,sK1_skl),sK5_skl(k8_filter_0(sK1_skl,X0),X0,sK1_skl)))),
% 8.25/1.59 inference(forward_subsumption_resolution,[status(thm)],[f860,f85])).
% 8.25/1.59 fof(f865,plain,(
% 8.25/1.59 ![X0]: (~l3_lattices(sK0_skl)|~m1_filter_0(X0,sK0_skl)|k8_filter_0(sK0_skl,X0)=g3_lattices(X0,sK4_skl(k8_filter_0(sK0_skl,X0),X0,sK0_skl),sK5_skl(k8_filter_0(sK0_skl,X0),X0,sK0_skl)))),
% 8.25/1.59 inference(forward_subsumption_resolution,[status(thm)],[f861,f82])).
% 8.25/1.59 fof(f923,plain,(
% 8.25/1.59 ![X0]: (~m1_filter_0(X0,sK1_skl)|k8_filter_0(sK1_skl,X0)=g3_lattices(X0,sK4_skl(k8_filter_0(sK1_skl,X0),X0,sK1_skl),sK5_skl(k8_filter_0(sK1_skl,X0),X0,sK1_skl)))),
% 8.25/1.59 inference(resolution,[status(thm)],[f864,f87])).
% 8.25/1.59 fof(f975,plain,(
% 8.25/1.59 ![X0]: (~m1_filter_0(X0,sK0_skl)|k8_filter_0(sK0_skl,X0)=g3_lattices(X0,sK4_skl(k8_filter_0(sK0_skl,X0),X0,sK0_skl),sK5_skl(k8_filter_0(sK0_skl,X0),X0,sK0_skl)))),
% 8.25/1.59 inference(resolution,[status(thm)],[f865,f84])).
% 8.25/1.59 fof(f988,plain,(
% 8.25/1.59 ![X0,X1,X2,X3]: (~l1_lattices(X0)|~v1_funct_1(u2_lattices(X0))|~m1_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(X1,X2,X3)|u1_struct_0(X0)=X1|~l2_lattices(X0))),
% 8.25/1.59 inference(resolution,[status(thm)],[f709,f165])).
% 8.25/1.59 fof(f990,plain,(
% 8.25/1.59 ![X0,X1,X2,X3]: (~l1_lattices(X0)|~m1_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(X1,X2,X3)|u1_struct_0(X0)=X1|~l2_lattices(X0))),
% 8.25/1.59 inference(forward_subsumption_resolution,[status(thm)],[f988,f164])).
% 8.25/1.59 fof(f1043,plain,(
% 8.25/1.59 ![X0,X1,X2,X3]: (~l1_lattices(X0)|~v1_funct_1(u2_lattices(X0))|~m1_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(X1,X2,X3)|u2_lattices(X0)=X2|~l2_lattices(X0))),
% 8.25/1.59 inference(resolution,[status(thm)],[f710,f165])).
% 8.25/1.59 fof(f1045,plain,(
% 8.25/1.59 ![X0,X1,X2,X3]: (~l1_lattices(X0)|~m1_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(X1,X2,X3)|u2_lattices(X0)=X2|~l2_lattices(X0))),
% 8.25/1.59 inference(forward_subsumption_resolution,[status(thm)],[f1043,f164])).
% 8.25/1.59 fof(f1048,plain,(
% 8.25/1.59 ![X0,X1,X2,X3]: (~l1_lattices(X0)|~v1_funct_1(u2_lattices(X0))|~m1_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(X1,X2,X3)|u1_lattices(X0)=X3|~l2_lattices(X0))),
% 8.25/1.59 inference(resolution,[status(thm)],[f711,f165])).
% 8.25/1.59 fof(f1050,plain,(
% 8.25/1.59 ![X0,X1,X2,X3]: (~l1_lattices(X0)|~m1_relset_1(u2_lattices(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0))|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(X1,X2,X3)|u1_lattices(X0)=X3|~l2_lattices(X0))),
% 8.25/1.59 inference(forward_subsumption_resolution,[status(thm)],[f1048,f164])).
% 8.25/1.59 fof(f1773,plain,(
% 8.25/1.59 ![X0,X1,X2,X3]: (~l1_lattices(X0)|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(X1,X2,X3)|u1_struct_0(X0)=X1|~l2_lattices(X0)|~l2_lattices(X0))),
% 8.25/1.59 inference(resolution,[status(thm)],[f990,f766])).
% 8.25/1.59 fof(f1774,plain,(
% 8.25/1.59 ![X0,X1,X2,X3]: (~l1_lattices(X0)|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(X1,X2,X3)|u1_struct_0(X0)=X1|~l2_lattices(X0))),
% 8.25/1.59 inference(duplicate_literals_removal,[status(thm)],[f1773])).
% 8.25/1.59 fof(f1890,plain,(
% 8.25/1.59 ![X0,X1,X2,X3]: (~l1_lattices(X0)|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(X1,X2,X3)|u2_lattices(X0)=X2|~l2_lattices(X0)|~l2_lattices(X0))),
% 8.25/1.59 inference(resolution,[status(thm)],[f1045,f766])).
% 8.25/1.59 fof(f1891,plain,(
% 8.25/1.59 ![X0,X1,X2,X3]: (~l1_lattices(X0)|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(X1,X2,X3)|u2_lattices(X0)=X2|~l2_lattices(X0))),
% 8.25/1.59 inference(duplicate_literals_removal,[status(thm)],[f1890])).
% 8.25/1.59 fof(f1894,plain,(
% 8.25/1.59 ![X0,X1,X2,X3]: (~l1_lattices(X0)|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(X1,X2,X3)|u1_lattices(X0)=X3|~l2_lattices(X0)|~l2_lattices(X0))),
% 8.25/1.59 inference(resolution,[status(thm)],[f1050,f766])).
% 8.25/1.59 fof(f1895,plain,(
% 8.25/1.59 ![X0,X1,X2,X3]: (~l1_lattices(X0)|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(X1,X2,X3)|u1_lattices(X0)=X3|~l2_lattices(X0))),
% 8.25/1.59 inference(duplicate_literals_removal,[status(thm)],[f1894])).
% 8.25/1.59 fof(f2609,plain,(
% 8.25/1.59 k8_filter_0(sK1_skl,sK3_skl)=g3_lattices(sK3_skl,sK4_skl(k8_filter_0(sK1_skl,sK3_skl),sK3_skl,sK1_skl),sK5_skl(k8_filter_0(sK1_skl,sK3_skl),sK3_skl,sK1_skl))),
% 8.25/1.59 inference(resolution,[status(thm)],[f923,f376])).
% 8.25/1.59 fof(f2612,plain,(
% 8.25/1.59 k8_filter_0(sK1_skl,sK3_skl)=g3_lattices(sK3_skl,k1_realset1(u2_lattices(sK1_skl),sK3_skl),sK5_skl(k8_filter_0(sK1_skl,sK3_skl),sK3_skl,sK1_skl))),
% 8.25/1.59 inference(forward_demodulation,[status(thm)],[f585,f2609])).
% 8.25/1.59 fof(f2613,plain,(
% 8.25/1.59 k8_filter_0(sK1_skl,sK3_skl)=g3_lattices(sK3_skl,k1_realset1(u2_lattices(sK1_skl),sK3_skl),k1_realset1(u1_lattices(sK1_skl),sK3_skl))),
% 8.25/1.59 inference(forward_demodulation,[status(thm)],[f516,f2612])).
% 8.25/1.59 fof(f2710,plain,(
% 8.25/1.59 k8_filter_0(sK0_skl,sK3_skl)=g3_lattices(sK3_skl,sK4_skl(k8_filter_0(sK0_skl,sK3_skl),sK3_skl,sK0_skl),sK5_skl(k8_filter_0(sK0_skl,sK3_skl),sK3_skl,sK0_skl))),
% 8.25/1.59 inference(resolution,[status(thm)],[f975,f378])).
% 8.25/1.59 fof(f2713,plain,(
% 8.25/1.59 k8_filter_0(sK0_skl,sK3_skl)=g3_lattices(sK3_skl,k1_realset1(u2_lattices(sK0_skl),sK3_skl),sK5_skl(k8_filter_0(sK0_skl,sK3_skl),sK3_skl,sK0_skl))),
% 8.25/1.59 inference(forward_demodulation,[status(thm)],[f531,f2710])).
% 8.25/1.59 fof(f2714,plain,(
% 8.25/1.59 k8_filter_0(sK0_skl,sK3_skl)=g3_lattices(sK3_skl,k1_realset1(u2_lattices(sK0_skl),sK3_skl),k1_realset1(u1_lattices(sK0_skl),sK3_skl))),
% 8.25/1.59 inference(forward_demodulation,[status(thm)],[f505,f2713])).
% 8.25/1.59 fof(f2869,plain,(
% 8.25/1.59 ![X0,X1,X2]: (~g3_lattices(u1_struct_0(sK0_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl))=g3_lattices(X0,X1,X2)|u1_struct_0(sK0_skl)=X0|~l2_lattices(sK0_skl))),
% 8.25/1.59 inference(resolution,[status(thm)],[f1774,f462])).
% 8.25/1.59 fof(f2877,plain,(
% 8.25/1.59 ![X0,X1,X2]: (~g3_lattices(u1_struct_0(sK1_skl),u2_lattices(sK1_skl),u1_lattices(sK1_skl))=g3_lattices(X0,X1,X2)|u1_struct_0(sK0_skl)=X0|~l2_lattices(sK0_skl))),
% 8.25/1.59 inference(forward_demodulation,[status(thm)],[f90,f2869])).
% 8.25/1.59 fof(f2878,plain,(
% 8.25/1.59 ![X0,X1,X2]: (~g3_lattices(u1_struct_0(sK1_skl),u2_lattices(sK1_skl),u1_lattices(sK1_skl))=g3_lattices(X0,X1,X2)|u1_struct_0(sK0_skl)=X0)),
% 8.25/1.59 inference(forward_subsumption_resolution,[status(thm)],[f2877,f499])).
% 8.25/1.59 fof(f2941,plain,(
% 8.25/1.59 u1_struct_0(sK0_skl)=u1_struct_0(sK1_skl)),
% 8.25/1.59 inference(equality_resolution,[status(thm)],[f2878])).
% 8.25/1.59 fof(f2967,plain,(
% 8.25/1.59 g3_lattices(u1_struct_0(sK1_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl))=g3_lattices(u1_struct_0(sK1_skl),u2_lattices(sK1_skl),u1_lattices(sK1_skl))),
% 8.25/1.59 inference(backward_demodulation,[status(thm)],[f2941,f90])).
% 8.25/1.59 fof(f3809,plain,(
% 8.25/1.59 ![X0,X1,X2]: (~g3_lattices(u1_struct_0(sK0_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl))=g3_lattices(X0,X1,X2)|u2_lattices(sK0_skl)=X1|~l2_lattices(sK0_skl))),
% 8.25/1.59 inference(resolution,[status(thm)],[f1891,f462])).
% 8.25/1.59 fof(f3817,plain,(
% 8.25/1.59 ![X0,X1,X2]: (~g3_lattices(u1_struct_0(sK1_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl))=g3_lattices(X0,X1,X2)|u2_lattices(sK0_skl)=X1|~l2_lattices(sK0_skl))),
% 8.25/1.59 inference(forward_demodulation,[status(thm)],[f2941,f3809])).
% 8.25/1.59 fof(f3818,plain,(
% 8.25/1.59 ![X0,X1,X2]: (~g3_lattices(u1_struct_0(sK1_skl),u2_lattices(sK1_skl),u1_lattices(sK1_skl))=g3_lattices(X0,X1,X2)|u2_lattices(sK0_skl)=X1|~l2_lattices(sK0_skl))),
% 8.25/1.59 inference(forward_demodulation,[status(thm)],[f2967,f3817])).
% 8.25/1.59 fof(f3819,plain,(
% 8.25/1.59 ![X0,X1,X2]: (~g3_lattices(u1_struct_0(sK1_skl),u2_lattices(sK1_skl),u1_lattices(sK1_skl))=g3_lattices(X0,X1,X2)|u2_lattices(sK0_skl)=X1)),
% 8.25/1.59 inference(forward_subsumption_resolution,[status(thm)],[f3818,f499])).
% 8.25/1.59 fof(f3914,plain,(
% 8.25/1.59 ![X0,X1,X2]: (~g3_lattices(u1_struct_0(sK0_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl))=g3_lattices(X0,X1,X2)|u1_lattices(sK0_skl)=X2|~l2_lattices(sK0_skl))),
% 8.25/1.62 inference(resolution,[status(thm)],[f1895,f462])).
% 8.25/1.62 fof(f3922,plain,(
% 8.25/1.62 ![X0,X1,X2]: (~g3_lattices(u1_struct_0(sK1_skl),u2_lattices(sK0_skl),u1_lattices(sK0_skl))=g3_lattices(X0,X1,X2)|u1_lattices(sK0_skl)=X2|~l2_lattices(sK0_skl))),
% 8.25/1.62 inference(forward_demodulation,[status(thm)],[f2941,f3914])).
% 8.25/1.62 fof(f3923,plain,(
% 8.25/1.62 ![X0,X1,X2]: (~g3_lattices(u1_struct_0(sK1_skl),u2_lattices(sK1_skl),u1_lattices(sK1_skl))=g3_lattices(X0,X1,X2)|u1_lattices(sK0_skl)=X2|~l2_lattices(sK0_skl))),
% 8.25/1.62 inference(forward_demodulation,[status(thm)],[f2967,f3922])).
% 8.25/1.62 fof(f3924,plain,(
% 8.25/1.62 ![X0,X1,X2]: (~g3_lattices(u1_struct_0(sK1_skl),u2_lattices(sK1_skl),u1_lattices(sK1_skl))=g3_lattices(X0,X1,X2)|u1_lattices(sK0_skl)=X2)),
% 8.25/1.62 inference(forward_subsumption_resolution,[status(thm)],[f3923,f499])).
% 8.25/1.62 fof(f4024,plain,(
% 8.25/1.62 u2_lattices(sK0_skl)=u2_lattices(sK1_skl)),
% 8.25/1.62 inference(equality_resolution,[status(thm)],[f3819])).
% 8.25/1.62 fof(f4104,plain,(
% 8.25/1.62 k8_filter_0(sK0_skl,sK3_skl)=g3_lattices(sK3_skl,k1_realset1(u2_lattices(sK1_skl),sK3_skl),k1_realset1(u1_lattices(sK0_skl),sK3_skl))),
% 8.25/1.62 inference(backward_demodulation,[status(thm)],[f4024,f2714])).
% 8.25/1.62 fof(f4651,plain,(
% 8.25/1.62 u1_lattices(sK0_skl)=u1_lattices(sK1_skl)),
% 8.25/1.62 inference(equality_resolution,[status(thm)],[f3924])).
% 8.25/1.62 fof(f4691,plain,(
% 8.25/1.62 k8_filter_0(sK0_skl,sK3_skl)=g3_lattices(sK3_skl,k1_realset1(u2_lattices(sK1_skl),sK3_skl),k1_realset1(u1_lattices(sK1_skl),sK3_skl))),
% 8.25/1.62 inference(backward_demodulation,[status(thm)],[f4651,f4104])).
% 8.25/1.62 fof(f4815,plain,(
% 8.25/1.62 k8_filter_0(sK0_skl,sK3_skl)=k8_filter_0(sK1_skl,sK3_skl)),
% 8.25/1.62 inference(forward_demodulation,[status(thm)],[f2613,f4691])).
% 8.25/1.62 fof(f4816,plain,(
% 8.25/1.62 $false),
% 8.25/1.62 inference(forward_subsumption_resolution,[status(thm)],[f4815,f333])).
% 8.25/1.62 % SZS output end CNFRefutation for theBenchmark.p
% 0.40/1.64 % Elapsed time: 1.179143 seconds
% 0.40/1.64 % CPU time: 8.742588 seconds
% 0.40/1.64 % Total memory used: 210.080 MB
% 0.40/1.64 % Net memory used: 207.401 MB
%------------------------------------------------------------------------------