%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT287+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 : n015.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:31 PM UTC 2026
% Result : Theorem 7.46s 1.37s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT287+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n015.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 23:29:38 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 7.46/1.37 % Refutation found
% 7.46/1.37 % SZS status Theorem for theBenchmark: Theorem is valid
% 7.46/1.37 % SZS output start CNFRefutation for theBenchmark
% 7.46/1.37 fof(f1,conjecture,(
% 7.46/1.37 (! [A] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A) )=> m1_subset_1(k1_pre_topc(A),u1_struct_0(k6_lopclset(A))) ) )),
% 7.46/1.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.46/1.37 fof(f2,negated_conjecture,(
% 7.46/1.37 ~((! [A] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A) )=> m1_subset_1(k1_pre_topc(A),u1_struct_0(k6_lopclset(A))) ) ))),
% 7.46/1.37 inference(negated_conjecture,[status(cth)],[f1])).
% 7.46/1.37 fof(f9,axiom,(
% 7.46/1.37 (! [A] :( l3_lattices(A)=> ( v3_lattices(A)=> A = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) ) ) )),
% 7.46/1.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.46/1.37 fof(f14,axiom,(
% 7.46/1.37 (! [A,B,C] :( m2_relset_1(C,A,B)<=> m1_relset_1(C,A,B) ) )),
% 7.46/1.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.46/1.37 fof(f52,axiom,(
% 7.46/1.37 (! [A,B] :( r2_hidden(A,B)=> m1_subset_1(A,B) ) )),
% 7.46/1.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.46/1.37 fof(f55,axiom,(
% 7.46/1.37 (! [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 ) ) )) )),
% 7.46/1.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.46/1.37 fof(f59,axiom,(
% 7.46/1.37 (! [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) )=> ( v3_lattices(g3_lattices(A,B,C))& l3_lattices(g3_lattices(A,B,C)) ) ) )),
% 7.46/1.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.46/1.37 fof(f60,axiom,(
% 7.46/1.37 (! [A] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A) )=> ( v1_funct_1(k4_lopclset(A))& v1_funct_2(k4_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A))& m2_relset_1(k4_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A)) ) ) )),
% 7.46/1.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.46/1.37 fof(f61,axiom,(
% 7.46/1.37 (! [A] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A) )=> ( v1_funct_1(k5_lopclset(A))& v1_funct_2(k5_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A))& m2_relset_1(k5_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A)) ) ) )),
% 7.46/1.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.46/1.37 fof(f69,axiom,(
% 7.46/1.37 (! [A] :( l1_struct_0(A)=> ( v1_xboole_0(k1_pre_topc(A))& v1_membered(k1_pre_topc(A))& v2_membered(k1_pre_topc(A))& v3_membered(k1_pre_topc(A))& v4_membered(k1_pre_topc(A))& v5_membered(k1_pre_topc(A)) ) ) )),
% 7.46/1.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.46/1.37 fof(f73,axiom,(
% 7.46/1.37 (! [A,B] :( m1_subset_1(A,B)=> ( v1_xboole_0(B)| r2_hidden(A,B) ) ) )),
% 7.46/1.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.46/1.37 fof(f74,axiom,(
% 7.46/1.37 (! [A] :( v1_xboole_0(A)=> A = k1_xboole_0 ) )),
% 7.46/1.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.46/1.37 fof(f78,axiom,(
% 7.46/1.37 (! [A,B] :( ( ~ v3_struct_0(B)& l1_pre_topc(B) )=> ( r2_hidden(A,a_1_0_lopclset(B))<=> (? [C] :( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))& A = C& v3_pre_topc(C,B)& v4_pre_topc(C,B) ) )) ) )),
% 7.46/1.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.46/1.37 fof(f82,axiom,(
% 7.46/1.37 (! [A,B] :( ( ~ v1_xboole_0(A)& ~ v1_xboole_0(B)& m1_subset_1(B,k1_zfmisc_1(A)) )=> (! [C] :( m2_subset_1(C,A,B)<=> m1_subset_1(C,B) ) )) )),
% 7.46/1.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.46/1.37 fof(f83,axiom,(
% 7.46/1.37 (! [A] :( ( ~ v3_struct_0(A)& l1_pre_topc(A) )=> m1_subset_1(k1_lopclset(A),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A)))) ) )),
% 7.46/1.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.46/1.37 fof(f84,axiom,(
% 7.46/1.37 (! [A] :( l1_struct_0(A)=> m1_subset_1(k1_pre_topc(A),k1_zfmisc_1(u1_struct_0(A))) ) )),
% 7.46/1.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.46/1.37 fof(f86,axiom,(
% 7.46/1.37 (! [A] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A) )=> ( ~ v3_struct_0(k6_lopclset(A))& v10_lattices(k6_lopclset(A))& l3_lattices(k6_lopclset(A)) ) ) )),
% 7.46/1.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.46/1.39 fof(f87,axiom,(
% 7.46/1.39 (! [A] :( l1_pre_topc(A)=> l1_struct_0(A) ) )),
% 7.46/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.46/1.39 fof(f91,axiom,(
% 7.46/1.39 (! [A] :( ~ v1_xboole_0(k1_zfmisc_1(A))& v1_finsub_1(k1_zfmisc_1(A))& v3_finsub_1(k1_zfmisc_1(A))& v4_finsub_1(k1_zfmisc_1(A)) ) )),
% 7.46/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.46/1.39 fof(f92,axiom,(
% 7.46/1.39 (! [A] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A) )=> ~ v1_xboole_0(k1_lopclset(A)) ) )),
% 7.46/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.46/1.39 fof(f94,axiom,(
% 7.46/1.39 (! [A] :( ( ~ v3_struct_0(A)& l1_pre_topc(A) )=> k1_lopclset(A) = a_1_0_lopclset(A) ) )),
% 7.46/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.46/1.39 fof(f95,axiom,(
% 7.46/1.39 (! [A] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A) )=> k6_lopclset(A) = g3_lattices(k1_lopclset(A),k4_lopclset(A),k5_lopclset(A)) ) )),
% 7.46/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.46/1.39 fof(f96,axiom,(
% 7.46/1.39 (! [A] :( ( ~ v3_struct_0(A)& v2_pre_topc(A)& l1_pre_topc(A) )=> m2_subset_1(k1_pre_topc(A),k1_zfmisc_1(u1_struct_0(A)),k1_lopclset(A)) ) )),
% 7.46/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.46/1.39 fof(f97,plain,(
% 7.46/1.39 (?[A]: (((~v3_struct_0(A)&v2_pre_topc(A))&l1_pre_topc(A))&~m1_subset_1(k1_pre_topc(A),u1_struct_0(k6_lopclset(A)))))),
% 7.46/1.39 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 7.46/1.39 fof(f98,plain,(
% 7.46/1.39 (((~v3_struct_0(sK0_skl)&v2_pre_topc(sK0_skl))&l1_pre_topc(sK0_skl))&~m1_subset_1(k1_pre_topc(sK0_skl),u1_struct_0(k6_lopclset(sK0_skl))))),
% 7.46/1.39 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(A,sK0_skl)],[f97])).
% 7.46/1.39 fof(f99,plain,(
% 7.46/1.39 ~v3_struct_0(sK0_skl)),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f98])).
% 7.46/1.39 fof(f100,plain,(
% 7.46/1.39 v2_pre_topc(sK0_skl)),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f98])).
% 7.46/1.39 fof(f101,plain,(
% 7.46/1.39 l1_pre_topc(sK0_skl)),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f98])).
% 7.46/1.39 fof(f102,plain,(
% 7.46/1.39 ~m1_subset_1(k1_pre_topc(sK0_skl),u1_struct_0(k6_lopclset(sK0_skl)))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f98])).
% 7.46/1.39 fof(f125,plain,(
% 7.46/1.39 ![A]: (~l3_lattices(A)|(~v3_lattices(A)|A=g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A))))),
% 7.46/1.39 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 7.46/1.39 fof(f126,plain,(
% 7.46/1.39 ![X0]: (~l3_lattices(X0)|~v3_lattices(X0)|X0=g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f125])).
% 7.46/1.39 fof(f135,plain,(
% 7.46/1.39 ![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)))),
% 7.46/1.39 inference(NNF_transformation,[status(thm)],[f14])).
% 7.46/1.39 fof(f136,plain,(
% 7.46/1.39 (![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)))),
% 7.46/1.39 inference(miniscoping,[status(thm)],[f135])).
% 7.46/1.39 fof(f137,plain,(
% 7.46/1.39 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_relset_1(X0,X1,X2))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f136])).
% 7.46/1.39 fof(f269,plain,(
% 7.46/1.39 ![A,B]: (~r2_hidden(A,B)|m1_subset_1(A,B))),
% 7.46/1.39 inference(pre_NNF_transformation,[status(thm)],[f52])).
% 7.46/1.39 fof(f270,plain,(
% 7.46/1.39 ![X0,X1]: (~r2_hidden(X0,X1)|m1_subset_1(X0,X1))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f269])).
% 7.46/1.39 fof(f277,plain,(
% 7.46/1.39 ![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))))),
% 7.46/1.39 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 7.46/1.39 fof(f278,plain,(
% 7.46/1.39 ![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)),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f277])).
% 7.46/1.39 fof(f279,plain,(
% 7.46/1.39 ![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)),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f277])).
% 7.46/1.39 fof(f280,plain,(
% 7.46/1.39 ![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)),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f277])).
% 7.46/1.39 fof(f287,plain,(
% 7.46/1.39 ![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))|(v3_lattices(g3_lattices(A,B,C))&l3_lattices(g3_lattices(A,B,C))))),
% 7.46/1.39 inference(pre_NNF_transformation,[status(thm)],[f59])).
% 7.46/1.39 fof(f288,plain,(
% 7.46/1.39 ![X0,X1,X2]: (~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)|v3_lattices(g3_lattices(X1,X0,X2)))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f287])).
% 7.46/1.39 fof(f290,plain,(
% 7.46/1.39 ![A]: (((v3_struct_0(A)|~v2_pre_topc(A))|~l1_pre_topc(A))|((v1_funct_1(k4_lopclset(A))&v1_funct_2(k4_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A)))&m2_relset_1(k4_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A))))),
% 7.46/1.39 inference(pre_NNF_transformation,[status(thm)],[f60])).
% 7.46/1.39 fof(f291,plain,(
% 7.46/1.39 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|v1_funct_1(k4_lopclset(X0)))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f290])).
% 7.46/1.39 fof(f292,plain,(
% 7.46/1.39 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|v1_funct_2(k4_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0)))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f290])).
% 7.46/1.39 fof(f293,plain,(
% 7.46/1.39 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|m2_relset_1(k4_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0)))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f290])).
% 7.46/1.39 fof(f294,plain,(
% 7.46/1.39 ![A]: (((v3_struct_0(A)|~v2_pre_topc(A))|~l1_pre_topc(A))|((v1_funct_1(k5_lopclset(A))&v1_funct_2(k5_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A)))&m2_relset_1(k5_lopclset(A),k2_zfmisc_1(k1_lopclset(A),k1_lopclset(A)),k1_lopclset(A))))),
% 7.46/1.39 inference(pre_NNF_transformation,[status(thm)],[f61])).
% 7.46/1.39 fof(f295,plain,(
% 7.46/1.39 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|v1_funct_1(k5_lopclset(X0)))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f294])).
% 7.46/1.39 fof(f296,plain,(
% 7.46/1.39 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|v1_funct_2(k5_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0)))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f294])).
% 7.46/1.39 fof(f297,plain,(
% 7.46/1.39 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|m2_relset_1(k5_lopclset(X0),k2_zfmisc_1(k1_lopclset(X0),k1_lopclset(X0)),k1_lopclset(X0)))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f294])).
% 7.46/1.39 fof(f322,plain,(
% 7.46/1.39 ![A]: (~l1_struct_0(A)|(((((v1_xboole_0(k1_pre_topc(A))&v1_membered(k1_pre_topc(A)))&v2_membered(k1_pre_topc(A)))&v3_membered(k1_pre_topc(A)))&v4_membered(k1_pre_topc(A)))&v5_membered(k1_pre_topc(A))))),
% 7.46/1.39 inference(pre_NNF_transformation,[status(thm)],[f69])).
% 7.46/1.39 fof(f323,plain,(
% 7.46/1.39 ![X0]: (~l1_struct_0(X0)|v1_xboole_0(k1_pre_topc(X0)))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f322])).
% 7.46/1.39 fof(f338,plain,(
% 7.46/1.39 ![A,B]: (~m1_subset_1(A,B)|(v1_xboole_0(B)|r2_hidden(A,B)))),
% 7.46/1.39 inference(pre_NNF_transformation,[status(thm)],[f73])).
% 7.46/1.39 fof(f339,plain,(
% 7.46/1.39 ![X0,X1]: (~m1_subset_1(X0,X1)|v1_xboole_0(X1)|r2_hidden(X0,X1))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f338])).
% 7.46/1.39 fof(f340,plain,(
% 7.46/1.39 ![A]: (~v1_xboole_0(A)|A=k1_xboole_0)),
% 7.46/1.39 inference(pre_NNF_transformation,[status(thm)],[f74])).
% 7.46/1.39 fof(f341,plain,(
% 7.46/1.39 ![X0]: (~v1_xboole_0(X0)|X0=k1_xboole_0)),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f340])).
% 7.46/1.39 fof(f353,plain,(
% 7.46/1.39 ![A,B]: ((v3_struct_0(B)|~l1_pre_topc(B))|(r2_hidden(A,a_1_0_lopclset(B))<=>(?[C]: (((m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))&A=C)&v3_pre_topc(C,B))&v4_pre_topc(C,B)))))),
% 7.46/1.39 inference(pre_NNF_transformation,[status(thm)],[f78])).
% 7.46/1.39 fof(f354,plain,(
% 7.46/1.39 ![A,B]: ((v3_struct_0(B)|~l1_pre_topc(B))|((~r2_hidden(A,a_1_0_lopclset(B))|(?[C]: (((m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))&A=C)&v3_pre_topc(C,B))&v4_pre_topc(C,B))))&(r2_hidden(A,a_1_0_lopclset(B))|(![C]: (((~m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))|~A=C)|~v3_pre_topc(C,B))|~v4_pre_topc(C,B))))))),
% 7.46/1.39 inference(NNF_transformation,[status(thm)],[f353])).
% 7.46/1.39 fof(f355,plain,(
% 7.46/1.39 ![B]: ((v3_struct_0(B)|~l1_pre_topc(B))|((![A]: (~r2_hidden(A,a_1_0_lopclset(B))|(?[C]: (((m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))&A=C)&v3_pre_topc(C,B))&v4_pre_topc(C,B)))))&(![A]: (r2_hidden(A,a_1_0_lopclset(B))|(![C]: (((~m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))|~A=C)|~v3_pre_topc(C,B))|~v4_pre_topc(C,B)))))))),
% 7.46/1.39 inference(miniscoping,[status(thm)],[f354])).
% 7.46/1.39 fof(f356,plain,(
% 7.46/1.39 ![B]: ((v3_struct_0(B)|~l1_pre_topc(B))|((![A]: (~r2_hidden(A,a_1_0_lopclset(B))|(((m1_subset_1(sK21_skl(A,B),k1_zfmisc_1(u1_struct_0(B)))&A=sK21_skl(A,B))&v3_pre_topc(sK21_skl(A,B),B))&v4_pre_topc(sK21_skl(A,B),B))))&(![A]: (r2_hidden(A,a_1_0_lopclset(B))|(![C]: (((~m1_subset_1(C,k1_zfmisc_1(u1_struct_0(B)))|~A=C)|~v3_pre_topc(C,B))|~v4_pre_topc(C,B)))))))),
% 7.46/1.39 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(C,sK21_skl(A,B))],[f355])).
% 7.46/1.39 fof(f358,plain,(
% 7.46/1.39 ![X0,X1]: (v3_struct_0(X0)|~l1_pre_topc(X0)|~r2_hidden(X1,a_1_0_lopclset(X0))|X1=sK21_skl(X1,X0))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f356])).
% 7.46/1.39 fof(f359,plain,(
% 7.46/1.39 ![X0,X1]: (v3_struct_0(X0)|~l1_pre_topc(X0)|~r2_hidden(X1,a_1_0_lopclset(X0))|v3_pre_topc(sK21_skl(X1,X0),X0))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f356])).
% 7.46/1.39 fof(f360,plain,(
% 7.46/1.39 ![X0,X1]: (v3_struct_0(X0)|~l1_pre_topc(X0)|~r2_hidden(X1,a_1_0_lopclset(X0))|v4_pre_topc(sK21_skl(X1,X0),X0))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f356])).
% 7.46/1.39 fof(f361,plain,(
% 7.46/1.39 ![X0,X1,X2]: (v3_struct_0(X0)|~l1_pre_topc(X0)|r2_hidden(X1,a_1_0_lopclset(X0))|~m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))|~X1=X2|~v3_pre_topc(X2,X0)|~v4_pre_topc(X2,X0))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f356])).
% 7.46/1.39 fof(f369,plain,(
% 7.46/1.39 ![A,B]: (((v1_xboole_0(A)|v1_xboole_0(B))|~m1_subset_1(B,k1_zfmisc_1(A)))|(![C]: (m2_subset_1(C,A,B)<=>m1_subset_1(C,B))))),
% 7.46/1.39 inference(pre_NNF_transformation,[status(thm)],[f82])).
% 7.46/1.39 fof(f370,plain,(
% 7.46/1.39 ![A,B]: (((v1_xboole_0(A)|v1_xboole_0(B))|~m1_subset_1(B,k1_zfmisc_1(A)))|(![C]: ((~m2_subset_1(C,A,B)|m1_subset_1(C,B))&(m2_subset_1(C,A,B)|~m1_subset_1(C,B)))))),
% 7.46/1.39 inference(NNF_transformation,[status(thm)],[f369])).
% 7.46/1.39 fof(f371,plain,(
% 7.46/1.39 ![A,B]: (((v1_xboole_0(A)|v1_xboole_0(B))|~m1_subset_1(B,k1_zfmisc_1(A)))|((![C]: (~m2_subset_1(C,A,B)|m1_subset_1(C,B)))&(![C]: (m2_subset_1(C,A,B)|~m1_subset_1(C,B)))))),
% 7.46/1.39 inference(miniscoping,[status(thm)],[f370])).
% 7.46/1.39 fof(f372,plain,(
% 7.46/1.39 ![X0,X1,X2]: (v1_xboole_0(X0)|v1_xboole_0(X1)|~m1_subset_1(X1,k1_zfmisc_1(X0))|~m2_subset_1(X2,X0,X1)|m1_subset_1(X2,X1))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f371])).
% 7.46/1.39 fof(f374,plain,(
% 7.46/1.39 ![A]: ((v3_struct_0(A)|~l1_pre_topc(A))|m1_subset_1(k1_lopclset(A),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(A)))))),
% 7.46/1.39 inference(pre_NNF_transformation,[status(thm)],[f83])).
% 7.46/1.39 fof(f375,plain,(
% 7.46/1.39 ![X0]: (v3_struct_0(X0)|~l1_pre_topc(X0)|m1_subset_1(k1_lopclset(X0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0)))))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f374])).
% 7.46/1.39 fof(f376,plain,(
% 7.46/1.39 ![A]: (~l1_struct_0(A)|m1_subset_1(k1_pre_topc(A),k1_zfmisc_1(u1_struct_0(A))))),
% 7.46/1.39 inference(pre_NNF_transformation,[status(thm)],[f84])).
% 7.46/1.39 fof(f377,plain,(
% 7.46/1.39 ![X0]: (~l1_struct_0(X0)|m1_subset_1(k1_pre_topc(X0),k1_zfmisc_1(u1_struct_0(X0))))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f376])).
% 7.46/1.39 fof(f378,plain,(
% 7.46/1.39 ![A]: (((v3_struct_0(A)|~v2_pre_topc(A))|~l1_pre_topc(A))|((~v3_struct_0(k6_lopclset(A))&v10_lattices(k6_lopclset(A)))&l3_lattices(k6_lopclset(A))))),
% 7.46/1.39 inference(pre_NNF_transformation,[status(thm)],[f86])).
% 7.46/1.39 fof(f381,plain,(
% 7.46/1.39 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|l3_lattices(k6_lopclset(X0)))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f378])).
% 7.46/1.39 fof(f382,plain,(
% 7.46/1.39 ![A]: (~l1_pre_topc(A)|l1_struct_0(A))),
% 7.46/1.39 inference(pre_NNF_transformation,[status(thm)],[f87])).
% 7.46/1.39 fof(f383,plain,(
% 7.46/1.39 ![X0]: (~l1_pre_topc(X0)|l1_struct_0(X0))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f382])).
% 7.46/1.39 fof(f386,plain,(
% 7.46/1.39 (((![A]: ~v1_xboole_0(k1_zfmisc_1(A)))&(![A]: v1_finsub_1(k1_zfmisc_1(A))))&(![A]: v3_finsub_1(k1_zfmisc_1(A))))&(![A]: v4_finsub_1(k1_zfmisc_1(A)))),
% 7.46/1.39 inference(miniscoping,[status(thm)],[f91])).
% 7.46/1.39 fof(f387,plain,(
% 7.46/1.39 ![X0]: (~v1_xboole_0(k1_zfmisc_1(X0)))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f386])).
% 7.46/1.39 fof(f391,plain,(
% 7.46/1.39 ![A]: (((v3_struct_0(A)|~v2_pre_topc(A))|~l1_pre_topc(A))|~v1_xboole_0(k1_lopclset(A)))),
% 7.46/1.39 inference(pre_NNF_transformation,[status(thm)],[f92])).
% 7.46/1.39 fof(f392,plain,(
% 7.46/1.39 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|~v1_xboole_0(k1_lopclset(X0)))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f391])).
% 7.46/1.39 fof(f397,plain,(
% 7.46/1.39 ![A]: ((v3_struct_0(A)|~l1_pre_topc(A))|k1_lopclset(A)=a_1_0_lopclset(A))),
% 7.46/1.39 inference(pre_NNF_transformation,[status(thm)],[f94])).
% 7.46/1.39 fof(f398,plain,(
% 7.46/1.39 ![X0]: (v3_struct_0(X0)|~l1_pre_topc(X0)|k1_lopclset(X0)=a_1_0_lopclset(X0))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f397])).
% 7.46/1.39 fof(f399,plain,(
% 7.46/1.39 ![A]: (((v3_struct_0(A)|~v2_pre_topc(A))|~l1_pre_topc(A))|k6_lopclset(A)=g3_lattices(k1_lopclset(A),k4_lopclset(A),k5_lopclset(A)))),
% 7.46/1.39 inference(pre_NNF_transformation,[status(thm)],[f95])).
% 7.46/1.39 fof(f400,plain,(
% 7.46/1.39 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|k6_lopclset(X0)=g3_lattices(k1_lopclset(X0),k4_lopclset(X0),k5_lopclset(X0)))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f399])).
% 7.46/1.39 fof(f401,plain,(
% 7.46/1.39 ![A]: (((v3_struct_0(A)|~v2_pre_topc(A))|~l1_pre_topc(A))|m2_subset_1(k1_pre_topc(A),k1_zfmisc_1(u1_struct_0(A)),k1_lopclset(A)))),
% 7.46/1.39 inference(pre_NNF_transformation,[status(thm)],[f96])).
% 7.46/1.39 fof(f402,plain,(
% 7.46/1.39 ![X0]: (v3_struct_0(X0)|~v2_pre_topc(X0)|~l1_pre_topc(X0)|m2_subset_1(k1_pre_topc(X0),k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0)))),
% 7.46/1.39 inference(cnf_transformation,[status(thm)],[f401])).
% 7.46/1.39 fof(f403,plain,(
% 7.46/1.39 ![X0,X1]: (v3_struct_0(X0)|~l1_pre_topc(X0)|r2_hidden(X1,a_1_0_lopclset(X0))|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|~v3_pre_topc(X1,X0)|~v4_pre_topc(X1,X0))),
% 7.46/1.39 inference(destructive_equality_resolution,[status(thm)],[f361])).
% 7.46/1.39 fof(f407,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|l3_lattices(k6_lopclset(sK0_skl))),
% 7.46/1.39 inference(resolution,[status(thm)],[f381,f101])).
% 7.46/1.39 fof(f408,plain,(
% 7.46/1.39 ~v2_pre_topc(sK0_skl)|l3_lattices(k6_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f407,f99])).
% 7.46/1.39 fof(f409,plain,(
% 7.46/1.39 l3_lattices(k6_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f408,f100])).
% 7.46/1.39 fof(f558,plain,(
% 7.46/1.39 ~v3_lattices(k6_lopclset(sK0_skl))|k6_lopclset(sK0_skl)=g3_lattices(u1_struct_0(k6_lopclset(sK0_skl)),u2_lattices(k6_lopclset(sK0_skl)),u1_lattices(k6_lopclset(sK0_skl)))),
% 7.46/1.39 inference(resolution,[status(thm)],[f126,f409])).
% 7.46/1.39 fof(f618,plain,(
% 7.46/1.39 l1_struct_0(sK0_skl)),
% 7.46/1.39 inference(resolution,[status(thm)],[f383,f101])).
% 7.46/1.39 fof(f626,plain,(
% 7.46/1.39 m1_subset_1(k1_pre_topc(sK0_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 7.46/1.39 inference(resolution,[status(thm)],[f618,f377])).
% 7.46/1.39 fof(f632,plain,(
% 7.46/1.39 v1_xboole_0(k1_pre_topc(sK0_skl))),
% 7.46/1.39 inference(resolution,[status(thm)],[f618,f323])).
% 7.46/1.39 fof(f647,plain,(
% 7.46/1.39 k1_pre_topc(sK0_skl)=k1_xboole_0),
% 7.46/1.39 inference(resolution,[status(thm)],[f632,f341])).
% 7.46/1.39 fof(f719,plain,(
% 7.46/1.39 m1_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 7.46/1.39 inference(backward_demodulation,[status(thm)],[f647,f626])).
% 7.46/1.39 fof(f726,plain,(
% 7.46/1.39 ~m1_subset_1(k1_xboole_0,u1_struct_0(k6_lopclset(sK0_skl)))),
% 7.46/1.39 inference(backward_demodulation,[status(thm)],[f647,f102])).
% 7.46/1.39 fof(f1645,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|k1_lopclset(sK0_skl)=a_1_0_lopclset(sK0_skl)),
% 7.46/1.39 inference(resolution,[status(thm)],[f398,f101])).
% 7.46/1.39 fof(f1646,plain,(
% 7.46/1.39 k1_lopclset(sK0_skl)=a_1_0_lopclset(sK0_skl)),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f1645,f99])).
% 7.46/1.39 fof(f1875,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|v1_funct_1(k4_lopclset(sK0_skl))),
% 7.46/1.39 inference(resolution,[status(thm)],[f291,f101])).
% 7.46/1.39 fof(f1876,plain,(
% 7.46/1.39 ~v2_pre_topc(sK0_skl)|v1_funct_1(k4_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f1875,f99])).
% 7.46/1.39 fof(f1877,plain,(
% 7.46/1.39 v1_funct_1(k4_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f1876,f100])).
% 7.46/1.39 fof(f1998,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))),
% 7.46/1.39 inference(resolution,[status(thm)],[f292,f101])).
% 7.46/1.39 fof(f1999,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_demodulation,[status(thm)],[f1646,f1998])).
% 7.46/1.39 fof(f2000,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),k1_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_demodulation,[status(thm)],[f1646,f1999])).
% 7.46/1.39 fof(f2001,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_demodulation,[status(thm)],[f1646,f2000])).
% 7.46/1.39 fof(f2002,plain,(
% 7.46/1.39 ~v2_pre_topc(sK0_skl)|v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f2001,f99])).
% 7.46/1.39 fof(f2004,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|m2_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))),
% 7.46/1.39 inference(resolution,[status(thm)],[f293,f101])).
% 7.46/1.39 fof(f2005,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|m2_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_demodulation,[status(thm)],[f1646,f2004])).
% 7.46/1.39 fof(f2006,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|m2_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),k1_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_demodulation,[status(thm)],[f1646,f2005])).
% 7.46/1.39 fof(f2007,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|m2_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_demodulation,[status(thm)],[f1646,f2006])).
% 7.46/1.39 fof(f2008,plain,(
% 7.46/1.39 ~v2_pre_topc(sK0_skl)|m2_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f2007,f99])).
% 7.46/1.39 fof(f2010,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|v1_funct_1(k5_lopclset(sK0_skl))),
% 7.46/1.39 inference(resolution,[status(thm)],[f295,f101])).
% 7.46/1.39 fof(f2011,plain,(
% 7.46/1.39 ~v2_pre_topc(sK0_skl)|v1_funct_1(k5_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f2010,f99])).
% 7.46/1.39 fof(f2012,plain,(
% 7.46/1.39 v1_funct_1(k5_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f2011,f100])).
% 7.46/1.39 fof(f2040,plain,(
% 7.46/1.39 v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f2002,f100])).
% 7.46/1.39 fof(f2079,plain,(
% 7.46/1.39 m2_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f2008,f100])).
% 7.46/1.39 fof(f2081,plain,(
% 7.46/1.39 m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))),
% 7.46/1.39 inference(resolution,[status(thm)],[f2079,f137])).
% 7.46/1.39 fof(f2156,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))),
% 7.46/1.39 inference(resolution,[status(thm)],[f296,f101])).
% 7.46/1.39 fof(f2157,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_demodulation,[status(thm)],[f1646,f2156])).
% 7.46/1.39 fof(f2158,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),k1_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_demodulation,[status(thm)],[f1646,f2157])).
% 7.46/1.39 fof(f2159,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_demodulation,[status(thm)],[f1646,f2158])).
% 7.46/1.39 fof(f2160,plain,(
% 7.46/1.39 ~v2_pre_topc(sK0_skl)|v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f2159,f99])).
% 7.46/1.39 fof(f2162,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|m2_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(k1_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))),
% 7.46/1.39 inference(resolution,[status(thm)],[f297,f101])).
% 7.46/1.39 fof(f2163,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|m2_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),k1_lopclset(sK0_skl)),k1_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_demodulation,[status(thm)],[f1646,f2162])).
% 7.46/1.39 fof(f2164,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|m2_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),k1_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_demodulation,[status(thm)],[f1646,f2163])).
% 7.46/1.39 fof(f2165,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|m2_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_demodulation,[status(thm)],[f1646,f2164])).
% 7.46/1.39 fof(f2166,plain,(
% 7.46/1.39 ~v2_pre_topc(sK0_skl)|m2_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f2165,f99])).
% 7.46/1.39 fof(f2195,plain,(
% 7.46/1.39 v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f2160,f100])).
% 7.46/1.39 fof(f2199,plain,(
% 7.46/1.39 ![X0]: (~v1_funct_1(X0)|~v1_funct_2(X0,k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~m1_relset_1(X0,k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~v1_funct_1(k5_lopclset(sK0_skl))|~m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|v3_lattices(g3_lattices(a_1_0_lopclset(sK0_skl),X0,k5_lopclset(sK0_skl))))),
% 7.46/1.39 inference(resolution,[status(thm)],[f2195,f288])).
% 7.46/1.39 fof(f2205,plain,(
% 7.46/1.39 ![X0]: (~v1_funct_1(X0)|~v1_funct_2(X0,k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~m1_relset_1(X0,k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|v3_lattices(g3_lattices(a_1_0_lopclset(sK0_skl),X0,k5_lopclset(sK0_skl))))),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f2199,f2012])).
% 7.46/1.39 fof(f2223,plain,(
% 7.46/1.39 m2_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f2166,f100])).
% 7.46/1.39 fof(f2225,plain,(
% 7.46/1.39 m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))),
% 7.46/1.39 inference(resolution,[status(thm)],[f2223,f137])).
% 7.46/1.39 fof(f2375,plain,(
% 7.46/1.39 ![X0]: (~v1_funct_1(X0)|~v1_funct_2(X0,k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~m1_relset_1(X0,k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|v3_lattices(g3_lattices(a_1_0_lopclset(sK0_skl),X0,k5_lopclset(sK0_skl))))),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f2205,f2225])).
% 7.46/1.39 fof(f2377,plain,(
% 7.46/1.39 ~v1_funct_1(k4_lopclset(sK0_skl))|~m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|v3_lattices(g3_lattices(a_1_0_lopclset(sK0_skl),k4_lopclset(sK0_skl),k5_lopclset(sK0_skl)))),
% 7.46/1.39 inference(resolution,[status(thm)],[f2375,f2040])).
% 7.46/1.39 fof(f2380,plain,(
% 7.46/1.39 ~m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|v3_lattices(g3_lattices(a_1_0_lopclset(sK0_skl),k4_lopclset(sK0_skl),k5_lopclset(sK0_skl)))),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f2377,f1877])).
% 7.46/1.39 fof(f2653,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~l1_pre_topc(sK0_skl)|r2_hidden(k1_xboole_0,a_1_0_lopclset(sK0_skl))|~v3_pre_topc(k1_xboole_0,sK0_skl)|~v4_pre_topc(k1_xboole_0,sK0_skl)),
% 7.46/1.39 inference(resolution,[status(thm)],[f403,f719])).
% 7.46/1.39 fof(f2665,plain,(
% 7.46/1.39 ~l1_pre_topc(sK0_skl)|r2_hidden(k1_xboole_0,a_1_0_lopclset(sK0_skl))|~v3_pre_topc(k1_xboole_0,sK0_skl)|~v4_pre_topc(k1_xboole_0,sK0_skl)),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f2653,f99])).
% 7.46/1.39 fof(f2908,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|m1_subset_1(k1_lopclset(sK0_skl),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 7.46/1.39 inference(resolution,[status(thm)],[f375,f101])).
% 7.46/1.39 fof(f2909,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|m1_subset_1(a_1_0_lopclset(sK0_skl),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 7.46/1.39 inference(forward_demodulation,[status(thm)],[f1646,f2908])).
% 7.46/1.39 fof(f2910,plain,(
% 7.46/1.39 m1_subset_1(a_1_0_lopclset(sK0_skl),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f2909,f99])).
% 7.46/1.39 fof(f2947,plain,(
% 7.46/1.39 ![X0]: (v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK0_skl)))|v1_xboole_0(a_1_0_lopclset(sK0_skl))|~m2_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)),a_1_0_lopclset(sK0_skl))|m1_subset_1(X0,a_1_0_lopclset(sK0_skl)))),
% 7.46/1.39 inference(resolution,[status(thm)],[f2910,f372])).
% 7.46/1.39 fof(f2960,plain,(
% 7.46/1.39 ![X0]: (v1_xboole_0(a_1_0_lopclset(sK0_skl))|~m2_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)),a_1_0_lopclset(sK0_skl))|m1_subset_1(X0,a_1_0_lopclset(sK0_skl)))),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f2947,f387])).
% 7.46/1.39 fof(f3044,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|~l1_pre_topc(sK0_skl)|~v1_xboole_0(a_1_0_lopclset(sK0_skl))),
% 7.46/1.39 inference(paramodulation,[status(thm)],[f1646,f392])).
% 7.46/1.39 fof(f3045,plain,(
% 7.46/1.39 ~v2_pre_topc(sK0_skl)|~l1_pre_topc(sK0_skl)|~v1_xboole_0(a_1_0_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f3044,f99])).
% 7.46/1.39 fof(f3047,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|k6_lopclset(sK0_skl)=g3_lattices(k1_lopclset(sK0_skl),k4_lopclset(sK0_skl),k5_lopclset(sK0_skl))),
% 7.46/1.39 inference(resolution,[status(thm)],[f400,f101])).
% 7.46/1.39 fof(f3048,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|k6_lopclset(sK0_skl)=g3_lattices(a_1_0_lopclset(sK0_skl),k4_lopclset(sK0_skl),k5_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_demodulation,[status(thm)],[f1646,f3047])).
% 7.46/1.39 fof(f3049,plain,(
% 7.46/1.39 ~v2_pre_topc(sK0_skl)|k6_lopclset(sK0_skl)=g3_lattices(a_1_0_lopclset(sK0_skl),k4_lopclset(sK0_skl),k5_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f3048,f99])).
% 7.46/1.39 fof(f3051,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|m2_subset_1(k1_pre_topc(sK0_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)),k1_lopclset(sK0_skl))),
% 7.46/1.39 inference(resolution,[status(thm)],[f402,f101])).
% 7.46/1.39 fof(f3053,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|m2_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK0_skl)),k1_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_demodulation,[status(thm)],[f647,f3051])).
% 7.46/1.39 fof(f3054,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~v2_pre_topc(sK0_skl)|m2_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK0_skl)),a_1_0_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_demodulation,[status(thm)],[f1646,f3053])).
% 7.46/1.39 fof(f3055,plain,(
% 7.46/1.39 ~v2_pre_topc(sK0_skl)|m2_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK0_skl)),a_1_0_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f3054,f99])).
% 7.46/1.39 fof(f3056,plain,(
% 7.46/1.39 ~l1_pre_topc(sK0_skl)|~v1_xboole_0(a_1_0_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f3045,f100])).
% 7.46/1.39 fof(f3057,plain,(
% 7.46/1.39 m2_subset_1(k1_xboole_0,k1_zfmisc_1(u1_struct_0(sK0_skl)),a_1_0_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f3055,f100])).
% 7.46/1.39 fof(f3058,plain,(
% 7.46/1.39 k6_lopclset(sK0_skl)=g3_lattices(a_1_0_lopclset(sK0_skl),k4_lopclset(sK0_skl),k5_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f3049,f100])).
% 7.46/1.39 fof(f3060,plain,(
% 7.46/1.39 ![X0,X1,X2]: (~v1_funct_1(k4_lopclset(sK0_skl))|~v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~v1_funct_1(k5_lopclset(sK0_skl))|~v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~k6_lopclset(sK0_skl)=g3_lattices(X0,X1,X2)|k5_lopclset(sK0_skl)=X2)),
% 7.46/1.39 inference(paramodulation,[status(thm)],[f3058,f280])).
% 7.46/1.39 fof(f3062,plain,(
% 7.46/1.39 ![X0,X1,X2]: (~v1_funct_1(k4_lopclset(sK0_skl))|~v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~v1_funct_1(k5_lopclset(sK0_skl))|~v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~k6_lopclset(sK0_skl)=g3_lattices(X0,X1,X2)|k4_lopclset(sK0_skl)=X1)),
% 7.46/1.39 inference(paramodulation,[status(thm)],[f3058,f279])).
% 7.46/1.39 fof(f3064,plain,(
% 7.46/1.39 ![X0,X1,X2]: (~v1_funct_1(k4_lopclset(sK0_skl))|~v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~v1_funct_1(k5_lopclset(sK0_skl))|~v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~k6_lopclset(sK0_skl)=g3_lattices(X0,X1,X2)|a_1_0_lopclset(sK0_skl)=X0)),
% 7.46/1.39 inference(paramodulation,[status(thm)],[f3058,f278])).
% 7.46/1.39 fof(f3066,plain,(
% 7.46/1.39 ![X0,X1,X2]: (~v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~v1_funct_1(k5_lopclset(sK0_skl))|~v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~k6_lopclset(sK0_skl)=g3_lattices(X0,X1,X2)|k5_lopclset(sK0_skl)=X2)),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f3060,f1877])).
% 7.46/1.39 fof(f3067,plain,(
% 7.46/1.39 ![X0,X1,X2]: (~v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~v1_funct_1(k5_lopclset(sK0_skl))|~v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~k6_lopclset(sK0_skl)=g3_lattices(X0,X1,X2)|k4_lopclset(sK0_skl)=X1)),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f3062,f1877])).
% 7.46/1.39 fof(f3068,plain,(
% 7.46/1.39 ![X0,X1,X2]: (~v1_funct_2(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~v1_funct_1(k5_lopclset(sK0_skl))|~v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~k6_lopclset(sK0_skl)=g3_lattices(X0,X1,X2)|a_1_0_lopclset(sK0_skl)=X0)),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f3064,f1877])).
% 7.46/1.39 fof(f3528,plain,(
% 7.46/1.39 r2_hidden(k1_xboole_0,a_1_0_lopclset(sK0_skl))|~v3_pre_topc(k1_xboole_0,sK0_skl)|~v4_pre_topc(k1_xboole_0,sK0_skl)),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f2665,f101])).
% 7.46/1.39 fof(f3531,plain,(
% 7.46/1.39 v1_xboole_0(a_1_0_lopclset(sK0_skl))|m1_subset_1(k1_xboole_0,a_1_0_lopclset(sK0_skl))),
% 7.46/1.39 inference(resolution,[status(thm)],[f2960,f3057])).
% 7.46/1.39 fof(f3613,plain,(
% 7.46/1.39 v1_xboole_0(a_1_0_lopclset(sK0_skl))|v1_xboole_0(a_1_0_lopclset(sK0_skl))|r2_hidden(k1_xboole_0,a_1_0_lopclset(sK0_skl))),
% 7.46/1.39 inference(resolution,[status(thm)],[f3531,f339])).
% 7.46/1.39 fof(f3615,plain,(
% 7.46/1.39 v1_xboole_0(a_1_0_lopclset(sK0_skl))|r2_hidden(k1_xboole_0,a_1_0_lopclset(sK0_skl))),
% 7.46/1.39 inference(duplicate_literals_removal,[status(thm)],[f3613])).
% 7.46/1.39 fof(f3617,plain,(
% 7.46/1.39 v1_xboole_0(a_1_0_lopclset(sK0_skl))|v3_struct_0(sK0_skl)|~l1_pre_topc(sK0_skl)|v4_pre_topc(sK21_skl(k1_xboole_0,sK0_skl),sK0_skl)),
% 7.46/1.39 inference(resolution,[status(thm)],[f3615,f360])).
% 7.46/1.39 fof(f3618,plain,(
% 7.46/1.39 v1_xboole_0(a_1_0_lopclset(sK0_skl))|v3_struct_0(sK0_skl)|~l1_pre_topc(sK0_skl)|v3_pre_topc(sK21_skl(k1_xboole_0,sK0_skl),sK0_skl)),
% 7.46/1.39 inference(resolution,[status(thm)],[f3615,f359])).
% 7.46/1.39 fof(f3619,plain,(
% 7.46/1.39 v1_xboole_0(a_1_0_lopclset(sK0_skl))|v3_struct_0(sK0_skl)|~l1_pre_topc(sK0_skl)|k1_xboole_0=sK21_skl(k1_xboole_0,sK0_skl)),
% 7.46/1.39 inference(resolution,[status(thm)],[f3615,f358])).
% 7.46/1.39 fof(f3623,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~l1_pre_topc(sK0_skl)|v4_pre_topc(sK21_skl(k1_xboole_0,sK0_skl),sK0_skl)),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f3617,f3056])).
% 7.46/1.39 fof(f3624,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~l1_pre_topc(sK0_skl)|v3_pre_topc(sK21_skl(k1_xboole_0,sK0_skl),sK0_skl)),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f3618,f3056])).
% 7.46/1.39 fof(f3625,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~l1_pre_topc(sK0_skl)|k1_xboole_0=sK21_skl(k1_xboole_0,sK0_skl)),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f3619,f3056])).
% 7.46/1.39 fof(f3627,plain,(
% 7.46/1.39 ~l1_pre_topc(sK0_skl)|k1_xboole_0=sK21_skl(k1_xboole_0,sK0_skl)),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f3625,f99])).
% 7.46/1.39 fof(f3628,plain,(
% 7.46/1.39 k1_xboole_0=sK21_skl(k1_xboole_0,sK0_skl)),
% 7.46/1.39 inference(resolution,[status(thm)],[f3627,f101])).
% 7.46/1.39 fof(f3630,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~l1_pre_topc(sK0_skl)|v4_pre_topc(k1_xboole_0,sK0_skl)),
% 7.46/1.39 inference(forward_demodulation,[status(thm)],[f3628,f3623])).
% 7.46/1.39 fof(f3631,plain,(
% 7.46/1.39 ~l1_pre_topc(sK0_skl)|v4_pre_topc(k1_xboole_0,sK0_skl)),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f3630,f99])).
% 7.46/1.39 fof(f3632,plain,(
% 7.46/1.39 v4_pre_topc(k1_xboole_0,sK0_skl)),
% 7.46/1.39 inference(resolution,[status(thm)],[f3631,f101])).
% 7.46/1.39 fof(f3633,plain,(
% 7.46/1.39 r2_hidden(k1_xboole_0,a_1_0_lopclset(sK0_skl))|~v3_pre_topc(k1_xboole_0,sK0_skl)),
% 7.46/1.39 inference(backward_subsumption_resolution,[status(thm)],[f3528,f3632])).
% 7.46/1.39 fof(f3642,plain,(
% 7.46/1.39 v3_struct_0(sK0_skl)|~l1_pre_topc(sK0_skl)|v3_pre_topc(k1_xboole_0,sK0_skl)),
% 7.46/1.39 inference(forward_demodulation,[status(thm)],[f3628,f3624])).
% 7.46/1.39 fof(f3643,plain,(
% 7.46/1.39 ~l1_pre_topc(sK0_skl)|v3_pre_topc(k1_xboole_0,sK0_skl)),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f3642,f99])).
% 7.46/1.39 fof(f3644,plain,(
% 7.46/1.39 v3_pre_topc(k1_xboole_0,sK0_skl)),
% 7.46/1.39 inference(resolution,[status(thm)],[f3643,f101])).
% 7.46/1.39 fof(f3645,plain,(
% 7.46/1.39 r2_hidden(k1_xboole_0,a_1_0_lopclset(sK0_skl))),
% 7.46/1.39 inference(backward_subsumption_resolution,[status(thm)],[f3633,f3644])).
% 7.46/1.39 fof(f3651,plain,(
% 7.46/1.39 m1_subset_1(k1_xboole_0,a_1_0_lopclset(sK0_skl))),
% 7.46/1.39 inference(resolution,[status(thm)],[f3645,f270])).
% 7.46/1.39 fof(f3665,plain,(
% 7.46/1.39 ![X0,X1,X2]: (~m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~v1_funct_1(k5_lopclset(sK0_skl))|~v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~k6_lopclset(sK0_skl)=g3_lattices(X0,X1,X2)|k5_lopclset(sK0_skl)=X2)),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f3066,f2040])).
% 7.46/1.39 fof(f3666,plain,(
% 7.46/1.39 ![X0,X1,X2]: (~m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~v1_funct_1(k5_lopclset(sK0_skl))|~m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~k6_lopclset(sK0_skl)=g3_lattices(X0,X1,X2)|k5_lopclset(sK0_skl)=X2)),
% 7.46/1.39 inference(resolution,[status(thm)],[f3665,f2195])).
% 7.46/1.39 fof(f3668,plain,(
% 7.46/1.39 ![X0,X1,X2]: (~v1_funct_1(k5_lopclset(sK0_skl))|~m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~k6_lopclset(sK0_skl)=g3_lattices(X0,X1,X2)|k5_lopclset(sK0_skl)=X2)),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f3666,f2081])).
% 7.46/1.39 fof(f3814,plain,(
% 7.46/1.39 ![X0,X1,X2]: (~m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~v1_funct_1(k5_lopclset(sK0_skl))|~v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~k6_lopclset(sK0_skl)=g3_lattices(X0,X1,X2)|k4_lopclset(sK0_skl)=X1)),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f3067,f2040])).
% 7.46/1.39 fof(f3815,plain,(
% 7.46/1.39 ![X0,X1,X2]: (~m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~v1_funct_1(k5_lopclset(sK0_skl))|~m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~k6_lopclset(sK0_skl)=g3_lattices(X0,X1,X2)|k4_lopclset(sK0_skl)=X1)),
% 7.46/1.39 inference(resolution,[status(thm)],[f3814,f2195])).
% 7.46/1.39 fof(f3817,plain,(
% 7.46/1.39 ![X0,X1,X2]: (~v1_funct_1(k5_lopclset(sK0_skl))|~m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~k6_lopclset(sK0_skl)=g3_lattices(X0,X1,X2)|k4_lopclset(sK0_skl)=X1)),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f3815,f2081])).
% 7.46/1.39 fof(f3848,plain,(
% 7.46/1.39 ![X0,X1,X2]: (~m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~v1_funct_1(k5_lopclset(sK0_skl))|~v1_funct_2(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~k6_lopclset(sK0_skl)=g3_lattices(X0,X1,X2)|a_1_0_lopclset(sK0_skl)=X0)),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f3068,f2040])).
% 7.46/1.39 fof(f3849,plain,(
% 7.46/1.39 ![X0,X1,X2]: (~m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~v1_funct_1(k5_lopclset(sK0_skl))|~m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~k6_lopclset(sK0_skl)=g3_lattices(X0,X1,X2)|a_1_0_lopclset(sK0_skl)=X0)),
% 7.46/1.39 inference(resolution,[status(thm)],[f3848,f2195])).
% 7.46/1.39 fof(f3851,plain,(
% 7.46/1.39 ![X0,X1,X2]: (~v1_funct_1(k5_lopclset(sK0_skl))|~m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~k6_lopclset(sK0_skl)=g3_lattices(X0,X1,X2)|a_1_0_lopclset(sK0_skl)=X0)),
% 7.46/1.39 inference(forward_subsumption_resolution,[status(thm)],[f3849,f2081])).
% 7.46/1.39 fof(f5653,plain,(
% 7.46/1.39 ~m1_relset_1(k4_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|v3_lattices(k6_lopclset(sK0_skl))),
% 7.46/1.39 inference(forward_demodulation,[status(thm)],[f3058,f2380])).
% 7.46/1.41 fof(f5654,plain,(
% 7.46/1.41 k6_lopclset(sK0_skl)=g3_lattices(u1_struct_0(k6_lopclset(sK0_skl)),u2_lattices(k6_lopclset(sK0_skl)),u1_lattices(k6_lopclset(sK0_skl)))),
% 7.46/1.41 inference(backward_subsumption_resolution,[status(thm)],[f558,f5655])).
% 7.46/1.41 fof(f5655,plain,(
% 7.46/1.41 v3_lattices(k6_lopclset(sK0_skl))),
% 7.46/1.41 inference(forward_subsumption_resolution,[status(thm)],[f5653,f2081])).
% 7.46/1.41 fof(f8718,plain,(
% 7.46/1.41 ![X0,X1,X2]: (~m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~k6_lopclset(sK0_skl)=g3_lattices(X0,X1,X2)|k5_lopclset(sK0_skl)=X2)),
% 7.46/1.41 inference(forward_subsumption_resolution,[status(thm)],[f3668,f2012])).
% 7.46/1.41 fof(f8719,plain,(
% 7.46/1.41 ![X0,X1,X2]: (~k6_lopclset(sK0_skl)=g3_lattices(X0,X1,X2)|k5_lopclset(sK0_skl)=X2)),
% 7.46/1.41 inference(resolution,[status(thm)],[f8718,f2225])).
% 7.46/1.41 fof(f8720,plain,(
% 7.46/1.41 k5_lopclset(sK0_skl)=u1_lattices(k6_lopclset(sK0_skl))),
% 7.46/1.41 inference(resolution,[status(thm)],[f8719,f5654])).
% 7.46/1.41 fof(f8728,plain,(
% 7.46/1.41 k6_lopclset(sK0_skl)=g3_lattices(u1_struct_0(k6_lopclset(sK0_skl)),u2_lattices(k6_lopclset(sK0_skl)),k5_lopclset(sK0_skl))),
% 7.46/1.41 inference(backward_demodulation,[status(thm)],[f8720,f5654])).
% 7.46/1.41 fof(f9522,plain,(
% 7.46/1.41 ![X0,X1,X2]: (~m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~k6_lopclset(sK0_skl)=g3_lattices(X0,X1,X2)|k4_lopclset(sK0_skl)=X1)),
% 7.46/1.41 inference(forward_subsumption_resolution,[status(thm)],[f3817,f2012])).
% 7.46/1.41 fof(f9523,plain,(
% 7.46/1.41 ![X0,X1,X2]: (~k6_lopclset(sK0_skl)=g3_lattices(X0,X1,X2)|k4_lopclset(sK0_skl)=X1)),
% 7.46/1.41 inference(resolution,[status(thm)],[f9522,f2225])).
% 7.46/1.41 fof(f9524,plain,(
% 7.46/1.41 k4_lopclset(sK0_skl)=u2_lattices(k6_lopclset(sK0_skl))),
% 7.46/1.41 inference(resolution,[status(thm)],[f9523,f8728])).
% 7.46/1.41 fof(f9535,plain,(
% 7.46/1.41 k6_lopclset(sK0_skl)=g3_lattices(u1_struct_0(k6_lopclset(sK0_skl)),k4_lopclset(sK0_skl),k5_lopclset(sK0_skl))),
% 7.46/1.41 inference(backward_demodulation,[status(thm)],[f9524,f8728])).
% 7.46/1.41 fof(f10429,plain,(
% 7.46/1.41 ![X0,X1,X2]: (~m1_relset_1(k5_lopclset(sK0_skl),k2_zfmisc_1(a_1_0_lopclset(sK0_skl),a_1_0_lopclset(sK0_skl)),a_1_0_lopclset(sK0_skl))|~k6_lopclset(sK0_skl)=g3_lattices(X0,X1,X2)|a_1_0_lopclset(sK0_skl)=X0)),
% 7.46/1.41 inference(forward_subsumption_resolution,[status(thm)],[f3851,f2012])).
% 7.46/1.41 fof(f10430,plain,(
% 7.46/1.41 ![X0,X1,X2]: (~k6_lopclset(sK0_skl)=g3_lattices(X0,X1,X2)|a_1_0_lopclset(sK0_skl)=X0)),
% 7.46/1.41 inference(resolution,[status(thm)],[f10429,f2225])).
% 7.46/1.41 fof(f10431,plain,(
% 7.46/1.41 a_1_0_lopclset(sK0_skl)=u1_struct_0(k6_lopclset(sK0_skl))),
% 7.46/1.41 inference(resolution,[status(thm)],[f10430,f9535])).
% 7.46/1.41 fof(f10475,plain,(
% 7.46/1.41 ~m1_subset_1(k1_xboole_0,a_1_0_lopclset(sK0_skl))),
% 7.46/1.41 inference(backward_demodulation,[status(thm)],[f10431,f726])).
% 7.46/1.41 fof(f10488,plain,(
% 7.46/1.41 $false),
% 7.46/1.41 inference(forward_subsumption_resolution,[status(thm)],[f10475,f3651])).
% 7.46/1.41 % SZS output end CNFRefutation for theBenchmark.p
% 7.46/1.42 % Elapsed time: 1.045613 seconds
% 7.46/1.42 % CPU time: 7.930417 seconds
% 7.46/1.42 % Total memory used: 205.773 MB
% 7.46/1.42 % Net memory used: 201.393 MB
%------------------------------------------------------------------------------