%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT323+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 : n020.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:41 PM UTC 2026
% Result : Theorem 88.29s 11.73s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT323+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.18/0.43 % Computer : n020.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Sun Sep 20 23:37:48 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.47 % Drodi V4.1.1
% 88.29/11.73 % Refutation found
% 88.29/11.73 % SZS status Theorem for theBenchmark: Theorem is valid
% 88.29/11.73 % SZS output start CNFRefutation for theBenchmark
% 88.29/11.73 fof(f1,conjecture,(
% 88.29/11.73 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& l3_lattices(A) )=> (! [B] :( m2_filter_2(B,A)=> ( r2_filter_2(A,B)=> (! [C] :( m1_subset_1(C,u1_struct_0(A))=> ( r2_hidden(C,B)<=> ~ r2_hidden(k7_lattices(A,C),B) ) ) )) ) )) )),
% 88.29/11.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 88.29/11.73 fof(f2,negated_conjecture,(
% 88.29/11.73 ~((! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& l3_lattices(A) )=> (! [B] :( m2_filter_2(B,A)=> ( r2_filter_2(A,B)=> (! [C] :( m1_subset_1(C,u1_struct_0(A))=> ( r2_hidden(C,B)<=> ~ r2_hidden(k7_lattices(A,C),B) ) ) )) ) )) ))),
% 88.29/11.73 inference(negated_conjecture,[status(cth)],[f1])).
% 88.29/11.73 fof(f3,axiom,(
% 88.29/11.73 (! [A] :( l3_lattices(A)=> ( v3_lattices(A)=> A = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) ) ) )),
% 88.29/11.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 88.29/11.73 fof(f15,axiom,(
% 88.29/11.73 (! [A] :( l3_lattices(A)=> k1_lattice2(A) = g3_lattices(u1_struct_0(A),u1_lattices(A),u2_lattices(A)) ) )),
% 88.29/11.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 88.29/11.73 fof(f16,axiom,(
% 88.29/11.73 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> k5_filter_2(A,B) = B ) )) )),
% 88.29/11.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 88.29/11.73 fof(f17,axiom,(
% 88.29/11.73 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))=> k7_filter_2(A,B) = B ) )) )),
% 88.29/11.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 88.29/11.73 fof(f19,axiom,(
% 88.29/11.73 (! [A,B] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A)& m2_filter_2(B,A) )=> m1_filter_2(k15_filter_2(A,B),k1_lattice2(A)) ) )),
% 88.29/11.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 88.29/11.73 fof(f20,axiom,(
% 88.29/11.73 (! [A] :( l3_lattices(A)=> ( v3_lattices(k1_lattice2(A))& l3_lattices(k1_lattice2(A)) ) ) )),
% 88.29/11.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 88.29/11.73 fof(f24,axiom,(
% 88.29/11.73 (! [A,B] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A)& m1_subset_1(B,u1_struct_0(A)) )=> m1_subset_1(k5_filter_2(A,B),u1_struct_0(k1_lattice2(A))) ) )),
% 88.29/11.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 88.29/11.73 fof(f30,axiom,(
% 88.29/11.73 (! [A] :( l3_lattices(A)=> ( l1_lattices(A)& l2_lattices(A) ) ) )),
% 88.29/11.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 88.29/11.73 fof(f35,axiom,(
% 88.29/11.73 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m2_filter_2(B,A)=> ( ~ v1_xboole_0(B)& m2_lattice4(B,A) ) ) )) )),
% 88.29/11.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 88.29/11.73 fof(f36,axiom,(
% 88.29/11.73 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m2_lattice4(B,A)=> m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) ) )) )),
% 88.29/11.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 88.29/11.73 fof(f38,axiom,(
% 88.29/11.73 (! [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)) ) ) )),
% 88.29/11.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 88.29/11.73 fof(f40,axiom,(
% 88.29/11.73 (! [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)) ) ) )),
% 88.29/11.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 88.29/11.73 fof(f53,axiom,(
% 88.29/11.73 (! [A] :( ( ~ v3_struct_0(A)& l3_lattices(A) )=> ( ~ v3_struct_0(k1_lattice2(A))& v3_lattices(k1_lattice2(A)) ) ) )),
% 88.29/11.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 88.29/11.73 fof(f60,axiom,(
% 88.29/11.73 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& l3_lattices(A) )=> ( ~ v3_struct_0(k1_lattice2(A))& v3_lattices(k1_lattice2(A))& v4_lattices(k1_lattice2(A))& v5_lattices(k1_lattice2(A))& v6_lattices(k1_lattice2(A))& v7_lattices(k1_lattice2(A))& v8_lattices(k1_lattice2(A))& v9_lattices(k1_lattice2(A))& v10_lattices(k1_lattice2(A))& v11_lattices(k1_lattice2(A))& v12_lattices(k1_lattice2(A))& v13_lattices(k1_lattice2(A))& v14_lattices(k1_lattice2(A))& v15_lattices(k1_lattice2(A))& v16_lattices(k1_lattice2(A))& v17_lattices(k1_lattice2(A)) ) ) )),
% 88.29/11.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 88.29/11.73 fof(f65,axiom,(
% 88.29/11.73 (! [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 ) ) )) )),
% 88.29/11.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 88.29/11.73 fof(f66,axiom,(
% 88.29/11.73 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> k7_lattices(k1_lattice2(A),k5_filter_2(A,B)) = k7_lattices(A,B) ) )) )),
% 88.29/11.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 88.29/11.73 fof(f84,axiom,(
% 88.29/11.73 (! [A,B] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A)& m2_filter_2(B,A) )=> k15_filter_2(A,B) = k7_filter_2(A,B) ) )),
% 88.29/11.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 88.29/11.73 fof(f85,axiom,(
% 88.29/11.73 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_filter_2(B,A)<=> m1_filter_0(B,A) ) )) )),
% 88.29/11.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 88.29/11.73 fof(f86,axiom,(
% 88.29/11.73 (! [A,B,C] :( m2_relset_1(C,A,B)<=> m1_relset_1(C,A,B) ) )),
% 88.29/11.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 88.29/11.73 fof(f90,axiom,(
% 88.29/11.73 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m2_filter_2(B,A)=> ( r2_filter_2(A,B)<=> v1_filter_0(k15_filter_2(A,B),k1_lattice2(A)) ) ) )) )),
% 88.29/11.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 88.29/11.73 fof(f93,axiom,(
% 88.29/11.73 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& v17_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_filter_0(B,A)=> ( v1_filter_0(B,A)=> (! [C] :( m1_subset_1(C,u1_struct_0(A))=> ( r2_hidden(C,B)<=> ~ r2_hidden(k7_lattices(A,C),B) ) ) )) ) )) )),
% 88.29/11.73 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 88.29/11.73 fof(f98,plain,(
% 88.29/11.73 (?[A]: ((((~v3_struct_0(A)&v10_lattices(A))&v17_lattices(A))&l3_lattices(A))&(?[B]: (m2_filter_2(B,A)&(r2_filter_2(A,B)&(?[C]: (m1_subset_1(C,u1_struct_0(A))&(r2_hidden(C,B)<~>~r2_hidden(k7_lattices(A,C),B)))))))))),
% 88.29/11.73 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 88.29/11.73 fof(f99,plain,(
% 88.29/11.73 ?[A]: ((((~v3_struct_0(A)&v10_lattices(A))&v17_lattices(A))&l3_lattices(A))&(?[B]: (m2_filter_2(B,A)&(r2_filter_2(A,B)&(?[C]: (m1_subset_1(C,u1_struct_0(A))&((r2_hidden(C,B)|~r2_hidden(k7_lattices(A,C),B))&(~r2_hidden(C,B)|r2_hidden(k7_lattices(A,C),B)))))))))),
% 88.29/11.73 inference(NNF_transformation,[status(thm)],[f98])).
% 88.29/11.73 fof(f100,plain,(
% 88.29/11.73 ((((~v3_struct_0(sK0_skl)&v10_lattices(sK0_skl))&v17_lattices(sK0_skl))&l3_lattices(sK0_skl))&(m2_filter_2(sK1_skl,sK0_skl)&(r2_filter_2(sK0_skl,sK1_skl)&(m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))&((r2_hidden(sK2_skl,sK1_skl)|~r2_hidden(k7_lattices(sK0_skl,sK2_skl),sK1_skl))&(~r2_hidden(sK2_skl,sK1_skl)|r2_hidden(k7_lattices(sK0_skl,sK2_skl),sK1_skl)))))))),
% 88.29/11.73 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl)],[f99])).
% 88.29/11.73 fof(f101,plain,(
% 88.29/11.73 ~v3_struct_0(sK0_skl)),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f100])).
% 88.29/11.73 fof(f102,plain,(
% 88.29/11.73 v10_lattices(sK0_skl)),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f100])).
% 88.29/11.73 fof(f103,plain,(
% 88.29/11.73 v17_lattices(sK0_skl)),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f100])).
% 88.29/11.73 fof(f104,plain,(
% 88.29/11.73 l3_lattices(sK0_skl)),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f100])).
% 88.29/11.73 fof(f105,plain,(
% 88.29/11.73 m2_filter_2(sK1_skl,sK0_skl)),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f100])).
% 88.29/11.73 fof(f106,plain,(
% 88.29/11.73 r2_filter_2(sK0_skl,sK1_skl)),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f100])).
% 88.29/11.73 fof(f107,plain,(
% 88.29/11.73 m1_subset_1(sK2_skl,u1_struct_0(sK0_skl))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f100])).
% 88.29/11.73 fof(f108,plain,(
% 88.29/11.73 r2_hidden(sK2_skl,sK1_skl)|~r2_hidden(k7_lattices(sK0_skl,sK2_skl),sK1_skl)),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f100])).
% 88.29/11.73 fof(f109,plain,(
% 88.29/11.73 ~r2_hidden(sK2_skl,sK1_skl)|r2_hidden(k7_lattices(sK0_skl,sK2_skl),sK1_skl)),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f100])).
% 88.29/11.73 fof(f110,plain,(
% 88.29/11.73 ![A]: (~l3_lattices(A)|(~v3_lattices(A)|A=g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A))))),
% 88.29/11.73 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 88.29/11.73 fof(f111,plain,(
% 88.29/11.73 ![X0]: (~l3_lattices(X0)|~v3_lattices(X0)|X0=g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f110])).
% 88.29/11.73 fof(f161,plain,(
% 88.29/11.73 ![A]: (~l3_lattices(A)|k1_lattice2(A)=g3_lattices(u1_struct_0(A),u1_lattices(A),u2_lattices(A)))),
% 88.29/11.73 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 88.29/11.73 fof(f162,plain,(
% 88.29/11.73 ![X0]: (~l3_lattices(X0)|k1_lattice2(X0)=g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f161])).
% 88.29/11.73 fof(f163,plain,(
% 88.29/11.73 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m1_subset_1(B,u1_struct_0(A))|k5_filter_2(A,B)=B)))),
% 88.29/11.73 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 88.29/11.73 fof(f164,plain,(
% 88.29/11.73 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|k5_filter_2(X0,X1)=X1)),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f163])).
% 88.29/11.73 fof(f165,plain,(
% 88.29/11.73 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))|k7_filter_2(A,B)=B)))),
% 88.29/11.73 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 88.29/11.73 fof(f166,plain,(
% 88.29/11.73 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))|k7_filter_2(X0,X1)=X1)),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f165])).
% 88.29/11.73 fof(f170,plain,(
% 88.29/11.73 ![A,B]: ((((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|~m2_filter_2(B,A))|m1_filter_2(k15_filter_2(A,B),k1_lattice2(A)))),
% 88.29/11.73 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 88.29/11.73 fof(f171,plain,(
% 88.29/11.73 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_filter_2(X1,X0)|m1_filter_2(k15_filter_2(X0,X1),k1_lattice2(X0)))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f170])).
% 88.29/11.73 fof(f172,plain,(
% 88.29/11.73 ![A]: (~l3_lattices(A)|(v3_lattices(k1_lattice2(A))&l3_lattices(k1_lattice2(A))))),
% 88.29/11.73 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 88.29/11.73 fof(f173,plain,(
% 88.29/11.73 ![X0]: (~l3_lattices(X0)|v3_lattices(k1_lattice2(X0)))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f172])).
% 88.29/11.73 fof(f174,plain,(
% 88.29/11.73 ![X0]: (~l3_lattices(X0)|l3_lattices(k1_lattice2(X0)))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f172])).
% 88.29/11.73 fof(f175,plain,(
% 88.29/11.73 ![A,B]: ((((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|~m1_subset_1(B,u1_struct_0(A)))|m1_subset_1(k5_filter_2(A,B),u1_struct_0(k1_lattice2(A))))),
% 88.29/11.73 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 88.29/11.73 fof(f176,plain,(
% 88.29/11.73 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|m1_subset_1(k5_filter_2(X0,X1),u1_struct_0(k1_lattice2(X0))))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f175])).
% 88.29/11.73 fof(f185,plain,(
% 88.29/11.73 ![A]: (~l3_lattices(A)|(l1_lattices(A)&l2_lattices(A)))),
% 88.29/11.73 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 88.29/11.73 fof(f186,plain,(
% 88.29/11.73 ![X0]: (~l3_lattices(X0)|l1_lattices(X0))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f185])).
% 88.29/11.73 fof(f187,plain,(
% 88.29/11.73 ![X0]: (~l3_lattices(X0)|l2_lattices(X0))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f185])).
% 88.29/11.73 fof(f194,plain,(
% 88.29/11.73 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m2_filter_2(B,A)|(~v1_xboole_0(B)&m2_lattice4(B,A)))))),
% 88.29/11.73 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 88.29/11.73 fof(f196,plain,(
% 88.29/11.73 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_filter_2(X1,X0)|m2_lattice4(X1,X0))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f194])).
% 88.29/11.73 fof(f197,plain,(
% 88.29/11.73 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m2_lattice4(B,A)|m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))))))),
% 88.29/11.73 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 88.29/11.73 fof(f198,plain,(
% 88.29/11.73 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_lattice4(X1,X0)|m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f197])).
% 88.29/11.73 fof(f201,plain,(
% 88.29/11.73 ![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))))),
% 88.29/11.73 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 88.29/11.73 fof(f202,plain,(
% 88.29/11.73 ![X0]: (~l1_lattices(X0)|v1_funct_1(u1_lattices(X0)))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f201])).
% 88.29/11.73 fof(f203,plain,(
% 88.29/11.73 ![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)))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f201])).
% 88.29/11.73 fof(f204,plain,(
% 88.29/11.73 ![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)))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f201])).
% 88.29/11.73 fof(f205,plain,(
% 88.29/11.73 ![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))))),
% 88.29/11.73 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 88.29/11.73 fof(f206,plain,(
% 88.29/11.73 ![X0]: (~l2_lattices(X0)|v1_funct_1(u2_lattices(X0)))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f205])).
% 88.29/11.73 fof(f207,plain,(
% 88.29/11.73 ![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)))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f205])).
% 88.29/11.73 fof(f208,plain,(
% 88.29/11.73 ![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)))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f205])).
% 88.29/11.73 fof(f237,plain,(
% 88.29/11.73 ![A]: ((v3_struct_0(A)|~l3_lattices(A))|(~v3_struct_0(k1_lattice2(A))&v3_lattices(k1_lattice2(A))))),
% 88.29/11.73 inference(pre_NNF_transformation,[status(thm)],[f53])).
% 88.29/11.73 fof(f238,plain,(
% 88.29/11.73 ![X0]: (v3_struct_0(X0)|~l3_lattices(X0)|~v3_struct_0(k1_lattice2(X0)))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f237])).
% 88.29/11.73 fof(f259,plain,(
% 88.29/11.73 ![A]: ((((v3_struct_0(A)|~v10_lattices(A))|~v17_lattices(A))|~l3_lattices(A))|(((((((((((((((~v3_struct_0(k1_lattice2(A))&v3_lattices(k1_lattice2(A)))&v4_lattices(k1_lattice2(A)))&v5_lattices(k1_lattice2(A)))&v6_lattices(k1_lattice2(A)))&v7_lattices(k1_lattice2(A)))&v8_lattices(k1_lattice2(A)))&v9_lattices(k1_lattice2(A)))&v10_lattices(k1_lattice2(A)))&v11_lattices(k1_lattice2(A)))&v12_lattices(k1_lattice2(A)))&v13_lattices(k1_lattice2(A)))&v14_lattices(k1_lattice2(A)))&v15_lattices(k1_lattice2(A)))&v16_lattices(k1_lattice2(A)))&v17_lattices(k1_lattice2(A))))),
% 88.29/11.73 inference(pre_NNF_transformation,[status(thm)],[f60])).
% 88.29/11.73 fof(f268,plain,(
% 88.29/11.73 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~v17_lattices(X0)|~l3_lattices(X0)|v10_lattices(k1_lattice2(X0)))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f259])).
% 88.29/11.73 fof(f275,plain,(
% 88.29/11.73 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~v17_lattices(X0)|~l3_lattices(X0)|v17_lattices(k1_lattice2(X0)))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f259])).
% 88.29/11.73 fof(f300,plain,(
% 88.29/11.73 ![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))))),
% 88.29/11.73 inference(pre_NNF_transformation,[status(thm)],[f65])).
% 88.29/11.73 fof(f301,plain,(
% 88.29/11.73 ![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)),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f300])).
% 88.29/11.73 fof(f304,plain,(
% 88.29/11.73 ![A]: ((((v3_struct_0(A)|~v10_lattices(A))|~v17_lattices(A))|~l3_lattices(A))|(![B]: (~m1_subset_1(B,u1_struct_0(A))|k7_lattices(k1_lattice2(A),k5_filter_2(A,B))=k7_lattices(A,B))))),
% 88.29/11.73 inference(pre_NNF_transformation,[status(thm)],[f66])).
% 88.29/11.73 fof(f305,plain,(
% 88.29/11.73 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~v17_lattices(X0)|~l3_lattices(X0)|~m1_subset_1(X1,u1_struct_0(X0))|k7_lattices(k1_lattice2(X0),k5_filter_2(X0,X1))=k7_lattices(X0,X1))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f304])).
% 88.29/11.73 fof(f418,plain,(
% 88.29/11.73 ![A,B]: ((((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|~m2_filter_2(B,A))|k15_filter_2(A,B)=k7_filter_2(A,B))),
% 88.29/11.73 inference(pre_NNF_transformation,[status(thm)],[f84])).
% 88.29/11.73 fof(f419,plain,(
% 88.29/11.73 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_filter_2(X1,X0)|k15_filter_2(X0,X1)=k7_filter_2(X0,X1))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f418])).
% 88.29/11.73 fof(f420,plain,(
% 88.29/11.73 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (m1_filter_2(B,A)<=>m1_filter_0(B,A))))),
% 88.29/11.73 inference(pre_NNF_transformation,[status(thm)],[f85])).
% 88.29/11.73 fof(f421,plain,(
% 88.29/11.73 ![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)))))),
% 88.29/11.73 inference(NNF_transformation,[status(thm)],[f420])).
% 88.29/11.73 fof(f422,plain,(
% 88.29/11.73 ![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)))))),
% 88.29/11.73 inference(miniscoping,[status(thm)],[f421])).
% 88.29/11.73 fof(f423,plain,(
% 88.29/11.73 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m1_filter_2(X1,X0)|m1_filter_0(X1,X0))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f422])).
% 88.29/11.73 fof(f425,plain,(
% 88.29/11.73 ![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)))),
% 88.29/11.73 inference(NNF_transformation,[status(thm)],[f86])).
% 88.29/11.73 fof(f426,plain,(
% 88.29/11.73 (![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)))),
% 88.29/11.73 inference(miniscoping,[status(thm)],[f425])).
% 88.29/11.73 fof(f427,plain,(
% 88.29/11.73 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_relset_1(X0,X1,X2))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f426])).
% 88.29/11.73 fof(f435,plain,(
% 88.29/11.73 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m2_filter_2(B,A)|(r2_filter_2(A,B)<=>v1_filter_0(k15_filter_2(A,B),k1_lattice2(A))))))),
% 88.29/11.73 inference(pre_NNF_transformation,[status(thm)],[f90])).
% 88.29/11.73 fof(f436,plain,(
% 88.29/11.73 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (~m2_filter_2(B,A)|((~r2_filter_2(A,B)|v1_filter_0(k15_filter_2(A,B),k1_lattice2(A)))&(r2_filter_2(A,B)|~v1_filter_0(k15_filter_2(A,B),k1_lattice2(A)))))))),
% 88.29/11.73 inference(NNF_transformation,[status(thm)],[f435])).
% 88.29/11.73 fof(f437,plain,(
% 88.29/11.73 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|~m2_filter_2(X1,X0)|~r2_filter_2(X0,X1)|v1_filter_0(k15_filter_2(X0,X1),k1_lattice2(X0)))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f436])).
% 88.29/11.73 fof(f446,plain,(
% 88.29/11.73 ![A]: ((((v3_struct_0(A)|~v10_lattices(A))|~v17_lattices(A))|~l3_lattices(A))|(![B]: (~m1_filter_0(B,A)|(~v1_filter_0(B,A)|(![C]: (~m1_subset_1(C,u1_struct_0(A))|(r2_hidden(C,B)<=>~r2_hidden(k7_lattices(A,C),B))))))))),
% 88.29/11.73 inference(pre_NNF_transformation,[status(thm)],[f93])).
% 88.29/11.73 fof(f447,plain,(
% 88.29/11.73 ![A]: ((((v3_struct_0(A)|~v10_lattices(A))|~v17_lattices(A))|~l3_lattices(A))|(![B]: (~m1_filter_0(B,A)|(~v1_filter_0(B,A)|(![C]: (~m1_subset_1(C,u1_struct_0(A))|((~r2_hidden(C,B)|~r2_hidden(k7_lattices(A,C),B))&(r2_hidden(C,B)|r2_hidden(k7_lattices(A,C),B)))))))))),
% 88.29/11.73 inference(NNF_transformation,[status(thm)],[f446])).
% 88.29/11.73 fof(f448,plain,(
% 88.29/11.73 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~v17_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|~v1_filter_0(X1,X0)|~m1_subset_1(X2,u1_struct_0(X0))|~r2_hidden(X2,X1)|~r2_hidden(k7_lattices(X0,X2),X1))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f447])).
% 88.29/11.73 fof(f449,plain,(
% 88.29/11.73 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~v17_lattices(X0)|~l3_lattices(X0)|~m1_filter_0(X1,X0)|~v1_filter_0(X1,X0)|~m1_subset_1(X2,u1_struct_0(X0))|r2_hidden(X2,X1)|r2_hidden(k7_lattices(X0,X2),X1))),
% 88.29/11.73 inference(cnf_transformation,[status(thm)],[f447])).
% 88.29/11.73 fof(f490,plain,(
% 88.29/11.73 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|v10_lattices(k1_lattice2(sK0_skl))),
% 88.29/11.73 inference(resolution,[status(thm)],[f268,f103])).
% 88.29/11.73 fof(f491,plain,(
% 88.29/11.73 ~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|v10_lattices(k1_lattice2(sK0_skl))),
% 88.29/11.73 inference(forward_subsumption_resolution,[status(thm)],[f490,f101])).
% 88.29/11.73 fof(f492,plain,(
% 88.29/11.73 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|v17_lattices(k1_lattice2(sK0_skl))),
% 88.29/11.73 inference(resolution,[status(thm)],[f275,f103])).
% 88.29/11.73 fof(f493,plain,(
% 88.29/11.73 ~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|v17_lattices(k1_lattice2(sK0_skl))),
% 88.29/11.73 inference(forward_subsumption_resolution,[status(thm)],[f492,f101])).
% 88.29/11.73 fof(f509,plain,(
% 88.29/11.73 ~l3_lattices(sK0_skl)|v10_lattices(k1_lattice2(sK0_skl))),
% 88.29/11.73 inference(forward_subsumption_resolution,[status(thm)],[f491,f102])).
% 88.29/11.73 fof(f510,plain,(
% 88.29/11.73 v10_lattices(k1_lattice2(sK0_skl))),
% 88.29/11.73 inference(resolution,[status(thm)],[f509,f104])).
% 88.29/11.73 fof(f529,plain,(
% 88.29/11.73 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~m2_filter_2(sK1_skl,sK0_skl)|v1_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))),
% 88.29/11.73 inference(resolution,[status(thm)],[f437,f106])).
% 88.29/11.73 fof(f530,plain,(
% 88.29/11.73 ~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~m2_filter_2(sK1_skl,sK0_skl)|v1_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))),
% 88.29/11.73 inference(forward_subsumption_resolution,[status(thm)],[f529,f101])).
% 88.29/11.73 fof(f542,plain,(
% 88.29/11.73 ~l3_lattices(sK0_skl)|v17_lattices(k1_lattice2(sK0_skl))),
% 88.29/11.73 inference(forward_subsumption_resolution,[status(thm)],[f493,f102])).
% 88.29/11.73 fof(f543,plain,(
% 88.29/11.73 v17_lattices(k1_lattice2(sK0_skl))),
% 88.29/11.73 inference(resolution,[status(thm)],[f542,f104])).
% 88.29/11.73 fof(f606,plain,(
% 88.29/11.73 ~l3_lattices(sK0_skl)|~m2_filter_2(sK1_skl,sK0_skl)|v1_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))),
% 88.29/11.73 inference(forward_subsumption_resolution,[status(thm)],[f530,f102])).
% 88.29/11.73 fof(f607,plain,(
% 88.29/11.73 ~l3_lattices(sK0_skl)|v1_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))),
% 88.29/11.73 inference(resolution,[status(thm)],[f606,f105])).
% 88.29/11.73 fof(f609,plain,(
% 88.29/11.73 v1_filter_0(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))),
% 88.29/11.73 inference(forward_subsumption_resolution,[status(thm)],[f607,f104])).
% 88.29/11.73 fof(f927,plain,(
% 88.29/11.73 k1_lattice2(sK0_skl)=g3_lattices(u1_struct_0(sK0_skl),u1_lattices(sK0_skl),u2_lattices(sK0_skl))),
% 88.29/11.73 inference(resolution,[status(thm)],[f162,f104])).
% 88.29/11.73 fof(f959,plain,(
% 88.29/11.73 ![X0]: (v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|k5_filter_2(sK0_skl,X0)=X0)),
% 88.29/11.73 inference(resolution,[status(thm)],[f164,f102])).
% 88.29/11.73 fof(f971,plain,(
% 88.29/11.73 ![X0]: (~l3_lattices(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|k5_filter_2(sK0_skl,X0)=X0)),
% 88.29/11.73 inference(forward_subsumption_resolution,[status(thm)],[f959,f101])).
% 88.29/11.73 fof(f983,plain,(
% 88.29/11.73 ![X0]: (v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|k7_filter_2(sK0_skl,X0)=X0)),
% 88.29/11.73 inference(resolution,[status(thm)],[f166,f102])).
% 88.29/11.73 fof(f995,plain,(
% 88.29/11.73 ![X0]: (~l3_lattices(sK0_skl)|~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|k7_filter_2(sK0_skl,X0)=X0)),
% 88.29/11.73 inference(forward_subsumption_resolution,[status(thm)],[f983,f101])).
% 88.29/11.73 fof(f1002,plain,(
% 88.29/11.73 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k5_filter_2(sK0_skl,X0)=X0)),
% 88.29/11.73 inference(forward_subsumption_resolution,[status(thm)],[f971,f104])).
% 88.29/11.73 fof(f1005,plain,(
% 88.29/11.73 k5_filter_2(sK0_skl,sK2_skl)=sK2_skl),
% 88.29/11.73 inference(resolution,[status(thm)],[f1002,f107])).
% 88.29/11.73 fof(f1040,plain,(
% 88.29/11.73 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m1_filter_2(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))),
% 88.29/11.73 inference(resolution,[status(thm)],[f171,f105])).
% 88.29/11.73 fof(f1041,plain,(
% 88.29/11.73 ~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m1_filter_2(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))),
% 88.29/11.73 inference(forward_subsumption_resolution,[status(thm)],[f1040,f101])).
% 88.29/11.73 fof(f1047,plain,(
% 88.29/11.73 v3_lattices(k1_lattice2(sK0_skl))),
% 88.29/11.73 inference(resolution,[status(thm)],[f173,f104])).
% 88.29/11.73 fof(f1048,plain,(
% 88.29/11.73 ~l3_lattices(k1_lattice2(sK0_skl))|k1_lattice2(sK0_skl)=g3_lattices(u1_struct_0(k1_lattice2(sK0_skl)),u2_lattices(k1_lattice2(sK0_skl)),u1_lattices(k1_lattice2(sK0_skl)))),
% 88.29/11.73 inference(resolution,[status(thm)],[f1047,f111])).
% 88.29/11.73 fof(f1070,plain,(
% 88.29/11.73 ![X0]: (~m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl)))|k7_filter_2(sK0_skl,X0)=X0)),
% 88.29/11.73 inference(forward_subsumption_resolution,[status(thm)],[f995,f104])).
% 88.29/11.73 fof(f1094,plain,(
% 88.29/11.73 l3_lattices(k1_lattice2(sK0_skl))),
% 88.29/11.73 inference(resolution,[status(thm)],[f174,f104])).
% 88.29/11.73 fof(f1097,plain,(
% 88.29/11.73 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m1_subset_1(k5_filter_2(sK0_skl,sK2_skl),u1_struct_0(k1_lattice2(sK0_skl)))),
% 88.29/11.73 inference(resolution,[status(thm)],[f176,f107])).
% 88.29/11.73 fof(f1100,plain,(
% 88.29/11.73 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m1_subset_1(sK2_skl,u1_struct_0(k1_lattice2(sK0_skl)))),
% 88.29/11.73 inference(forward_demodulation,[status(thm)],[f1005,f1097])).
% 88.29/11.73 fof(f1101,plain,(
% 88.29/11.73 ~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m1_subset_1(sK2_skl,u1_struct_0(k1_lattice2(sK0_skl)))),
% 88.29/11.73 inference(forward_subsumption_resolution,[status(thm)],[f1100,f101])).
% 88.29/11.73 fof(f1132,plain,(
% 88.29/11.73 ~l3_lattices(sK0_skl)|m1_filter_2(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))),
% 88.29/11.73 inference(forward_subsumption_resolution,[status(thm)],[f1041,f102])).
% 88.29/11.73 fof(f1133,plain,(
% 88.29/11.73 m1_filter_2(k15_filter_2(sK0_skl,sK1_skl),k1_lattice2(sK0_skl))),
% 88.29/11.73 inference(resolution,[status(thm)],[f1132,f104])).
% 88.29/11.73 fof(f1208,plain,(
% 88.29/11.73 l1_lattices(sK0_skl)),
% 88.29/11.73 inference(resolution,[status(thm)],[f186,f104])).
% 88.29/11.73 fof(f1210,plain,(
% 88.29/11.73 ~l3_lattices(sK0_skl)|m1_subset_1(sK2_skl,u1_struct_0(k1_lattice2(sK0_skl)))),
% 88.29/11.73 inference(forward_subsumption_resolution,[status(thm)],[f1101,f102])).
% 88.29/11.73 fof(f1211,plain,(
% 88.29/11.73 m1_subset_1(sK2_skl,u1_struct_0(k1_lattice2(sK0_skl)))),
% 88.29/11.73 inference(resolution,[status(thm)],[f1210,f104])).
% 88.29/11.73 fof(f1272,plain,(
% 88.29/11.73 l2_lattices(sK0_skl)),
% 88.29/11.73 inference(resolution,[status(thm)],[f187,f104])).
% 88.29/11.73 fof(f1439,plain,(
% 88.29/11.73 ![X0]: (v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|~m2_filter_2(X0,sK0_skl)|m2_lattice4(X0,sK0_skl))),
% 88.29/11.73 inference(resolution,[status(thm)],[f196,f102])).
% 88.29/11.73 fof(f1458,plain,(
% 88.29/11.73 ![X0]: (~l3_lattices(sK0_skl)|~m2_filter_2(X0,sK0_skl)|m2_lattice4(X0,sK0_skl))),
% 88.29/11.73 inference(forward_subsumption_resolution,[status(thm)],[f1439,f101])).
% 88.29/11.73 fof(f1501,plain,(
% 88.29/11.73 ![X0]: (v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|~m2_lattice4(X0,sK0_skl)|m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 88.29/11.73 inference(resolution,[status(thm)],[f198,f102])).
% 88.29/11.73 fof(f1521,plain,(
% 88.29/11.73 ![X0]: (~l3_lattices(sK0_skl)|~m2_lattice4(X0,sK0_skl)|m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 88.29/11.74 inference(forward_subsumption_resolution,[status(thm)],[f1501,f101])).
% 88.29/11.74 fof(f1540,plain,(
% 88.29/11.74 v1_funct_1(u1_lattices(sK0_skl))),
% 88.29/11.74 inference(resolution,[status(thm)],[f202,f1208])).
% 88.29/11.74 fof(f1565,plain,(
% 88.29/11.74 v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))),
% 88.29/11.74 inference(resolution,[status(thm)],[f203,f1208])).
% 88.29/11.74 fof(f1577,plain,(
% 88.29/11.74 m2_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))),
% 88.29/11.74 inference(resolution,[status(thm)],[f204,f1208])).
% 88.29/11.74 fof(f1586,plain,(
% 88.29/11.74 v1_funct_1(u2_lattices(sK0_skl))),
% 88.29/11.74 inference(resolution,[status(thm)],[f206,f1272])).
% 88.29/11.74 fof(f1588,plain,(
% 88.29/11.74 ![X0]: (~m2_filter_2(X0,sK0_skl)|m2_lattice4(X0,sK0_skl))),
% 88.29/11.74 inference(forward_subsumption_resolution,[status(thm)],[f1458,f104])).
% 88.29/11.74 fof(f1589,plain,(
% 88.29/11.74 m2_lattice4(sK1_skl,sK0_skl)),
% 88.29/11.74 inference(resolution,[status(thm)],[f1588,f105])).
% 88.29/11.74 fof(f1606,plain,(
% 88.29/11.74 v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))),
% 88.29/11.74 inference(resolution,[status(thm)],[f207,f1272])).
% 88.29/11.74 fof(f1618,plain,(
% 88.29/11.74 m2_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))),
% 88.29/11.74 inference(resolution,[status(thm)],[f208,f1272])).
% 88.29/11.74 fof(f1661,plain,(
% 88.29/11.74 ![X0]: (~m2_lattice4(X0,sK0_skl)|m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 88.29/11.74 inference(forward_subsumption_resolution,[status(thm)],[f1521,f104])).
% 88.29/11.74 fof(f1662,plain,(
% 88.29/11.74 m1_subset_1(sK1_skl,k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 88.29/11.74 inference(resolution,[status(thm)],[f1661,f1589])).
% 88.29/11.74 fof(f2096,plain,(
% 88.29/11.74 k7_filter_2(sK0_skl,sK1_skl)=sK1_skl),
% 88.29/11.74 inference(resolution,[status(thm)],[f1662,f1070])).
% 88.29/11.74 fof(f2103,plain,(
% 88.29/11.74 k1_lattice2(sK0_skl)=g3_lattices(u1_struct_0(k1_lattice2(sK0_skl)),u2_lattices(k1_lattice2(sK0_skl)),u1_lattices(k1_lattice2(sK0_skl)))),
% 88.29/11.74 inference(forward_subsumption_resolution,[status(thm)],[f1048,f1094])).
% 88.29/11.74 fof(f3284,plain,(
% 88.29/11.74 ![X0,X1,X2]: (~v1_funct_1(u1_lattices(sK0_skl))|~v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~v1_funct_1(u2_lattices(sK0_skl))|~v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~k1_lattice2(sK0_skl)=g3_lattices(X0,X1,X2)|u1_struct_0(sK0_skl)=X0)),
% 88.29/11.74 inference(paramodulation,[status(thm)],[f927,f301])).
% 88.29/11.74 fof(f3291,plain,(
% 88.29/11.74 ![X0,X1,X2]: (~v1_funct_2(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~v1_funct_1(u2_lattices(sK0_skl))|~v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~k1_lattice2(sK0_skl)=g3_lattices(X0,X1,X2)|u1_struct_0(sK0_skl)=X0)),
% 88.29/11.74 inference(forward_subsumption_resolution,[status(thm)],[f3284,f1540])).
% 88.29/11.74 fof(f3332,plain,(
% 88.29/11.74 ![X0]: (v3_struct_0(sK0_skl)|~v17_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|k7_lattices(k1_lattice2(sK0_skl),k5_filter_2(sK0_skl,X0))=k7_lattices(sK0_skl,X0))),
% 88.29/11.74 inference(resolution,[status(thm)],[f305,f102])).
% 88.29/11.74 fof(f3375,plain,(
% 88.29/11.74 ![X0]: (~v17_lattices(sK0_skl)|~l3_lattices(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|k7_lattices(k1_lattice2(sK0_skl),k5_filter_2(sK0_skl,X0))=k7_lattices(sK0_skl,X0))),
% 88.29/11.74 inference(forward_subsumption_resolution,[status(thm)],[f3332,f101])).
% 88.29/11.74 fof(f3451,plain,(
% 88.29/11.74 ![X0]: (~l3_lattices(sK0_skl)|~m1_subset_1(X0,u1_struct_0(sK0_skl))|k7_lattices(k1_lattice2(sK0_skl),k5_filter_2(sK0_skl,X0))=k7_lattices(sK0_skl,X0))),
% 88.29/11.74 inference(forward_subsumption_resolution,[status(thm)],[f3375,f103])).
% 88.29/11.74 fof(f3452,plain,(
% 88.29/11.74 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK0_skl))|k7_lattices(k1_lattice2(sK0_skl),k5_filter_2(sK0_skl,X0))=k7_lattices(sK0_skl,X0))),
% 88.29/11.74 inference(resolution,[status(thm)],[f3451,f104])).
% 88.29/11.74 fof(f3590,plain,(
% 88.29/11.74 ![X0]: (v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)|~m2_filter_2(X0,sK0_skl)|k15_filter_2(sK0_skl,X0)=k7_filter_2(sK0_skl,X0))),
% 88.29/11.74 inference(resolution,[status(thm)],[f419,f102])).
% 88.29/11.74 fof(f3628,plain,(
% 88.29/11.74 ![X0]: (~l3_lattices(sK0_skl)|~m2_filter_2(X0,sK0_skl)|k15_filter_2(sK0_skl,X0)=k7_filter_2(sK0_skl,X0))),
% 88.29/11.74 inference(forward_subsumption_resolution,[status(thm)],[f3590,f101])).
% 88.29/11.74 fof(f3668,plain,(
% 88.29/11.74 ![X0]: (v3_struct_0(k1_lattice2(sK0_skl))|~v10_lattices(k1_lattice2(sK0_skl))|~m1_filter_2(X0,k1_lattice2(sK0_skl))|m1_filter_0(X0,k1_lattice2(sK0_skl)))),
% 88.29/11.74 inference(resolution,[status(thm)],[f423,f1094])).
% 88.29/11.74 fof(f3688,plain,(
% 88.29/11.74 ![X0]: (v3_struct_0(k1_lattice2(sK0_skl))|~m1_filter_2(X0,k1_lattice2(sK0_skl))|m1_filter_0(X0,k1_lattice2(sK0_skl)))),
% 88.29/11.74 inference(forward_subsumption_resolution,[status(thm)],[f3668,f510])).
% 88.29/11.75 fof(f3721,plain,(
% 88.29/11.75 ![X0]: (~m2_filter_2(X0,sK0_skl)|k15_filter_2(sK0_skl,X0)=k7_filter_2(sK0_skl,X0))),
% 88.29/11.75 inference(forward_subsumption_resolution,[status(thm)],[f3628,f104])).
% 88.29/11.75 fof(f3724,plain,(
% 88.29/11.75 k15_filter_2(sK0_skl,sK1_skl)=k7_filter_2(sK0_skl,sK1_skl)),
% 88.29/11.75 inference(resolution,[status(thm)],[f3721,f105])).
% 88.29/11.75 fof(f3728,plain,(
% 88.29/11.75 k15_filter_2(sK0_skl,sK1_skl)=sK1_skl),
% 88.29/11.75 inference(forward_demodulation,[status(thm)],[f2096,f3724])).
% 88.29/11.75 fof(f3729,plain,(
% 88.29/11.75 m1_filter_2(sK1_skl,k1_lattice2(sK0_skl))),
% 88.29/11.75 inference(backward_demodulation,[status(thm)],[f3728,f1133])).
% 88.29/11.75 fof(f3730,plain,(
% 88.29/11.75 v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 88.29/11.75 inference(backward_demodulation,[status(thm)],[f3728,f609])).
% 88.29/11.75 fof(f3990,plain,(
% 88.29/11.75 ![X0,X1]: (v3_struct_0(k1_lattice2(sK0_skl))|~v10_lattices(k1_lattice2(sK0_skl))|~v17_lattices(k1_lattice2(sK0_skl))|~m1_filter_0(X0,k1_lattice2(sK0_skl))|~v1_filter_0(X0,k1_lattice2(sK0_skl))|~m1_subset_1(X1,u1_struct_0(k1_lattice2(sK0_skl)))|~r2_hidden(X1,X0)|~r2_hidden(k7_lattices(k1_lattice2(sK0_skl),X1),X0))),
% 88.29/11.75 inference(resolution,[status(thm)],[f448,f1094])).
% 88.29/11.75 fof(f4015,plain,(
% 88.29/11.75 ![X0,X1]: (v3_struct_0(k1_lattice2(sK0_skl))|~v17_lattices(k1_lattice2(sK0_skl))|~m1_filter_0(X0,k1_lattice2(sK0_skl))|~v1_filter_0(X0,k1_lattice2(sK0_skl))|~m1_subset_1(X1,u1_struct_0(k1_lattice2(sK0_skl)))|~r2_hidden(X1,X0)|~r2_hidden(k7_lattices(k1_lattice2(sK0_skl),X1),X0))),
% 88.29/11.75 inference(forward_subsumption_resolution,[status(thm)],[f3990,f510])).
% 88.29/11.75 fof(f4084,plain,(
% 88.29/11.75 ![X0,X1]: (v3_struct_0(k1_lattice2(sK0_skl))|~v10_lattices(k1_lattice2(sK0_skl))|~v17_lattices(k1_lattice2(sK0_skl))|~m1_filter_0(X0,k1_lattice2(sK0_skl))|~v1_filter_0(X0,k1_lattice2(sK0_skl))|~m1_subset_1(X1,u1_struct_0(k1_lattice2(sK0_skl)))|r2_hidden(X1,X0)|r2_hidden(k7_lattices(k1_lattice2(sK0_skl),X1),X0))),
% 88.29/11.75 inference(resolution,[status(thm)],[f449,f1094])).
% 88.29/11.75 fof(f4109,plain,(
% 88.29/11.75 ![X0,X1]: (v3_struct_0(k1_lattice2(sK0_skl))|~v17_lattices(k1_lattice2(sK0_skl))|~m1_filter_0(X0,k1_lattice2(sK0_skl))|~v1_filter_0(X0,k1_lattice2(sK0_skl))|~m1_subset_1(X1,u1_struct_0(k1_lattice2(sK0_skl)))|r2_hidden(X1,X0)|r2_hidden(k7_lattices(k1_lattice2(sK0_skl),X1),X0))),
% 88.29/11.75 inference(forward_subsumption_resolution,[status(thm)],[f4084,f510])).
% 88.29/11.75 fof(f4224,plain,(
% 88.29/11.75 m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))),
% 88.29/11.75 inference(resolution,[status(thm)],[f1577,f427])).
% 88.29/11.75 fof(f4258,plain,(
% 88.29/11.75 m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))),
% 88.29/11.75 inference(resolution,[status(thm)],[f1618,f427])).
% 88.29/11.75 fof(f5461,plain,(
% 88.29/11.75 ![X0,X1,X2]: (~m1_relset_1(u1_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~v1_funct_1(u2_lattices(sK0_skl))|~v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~k1_lattice2(sK0_skl)=g3_lattices(X0,X1,X2)|u1_struct_0(sK0_skl)=X0)),
% 88.29/11.75 inference(forward_subsumption_resolution,[status(thm)],[f3291,f1565])).
% 88.29/11.75 fof(f6878,plain,(
% 88.29/11.75 k7_lattices(k1_lattice2(sK0_skl),k5_filter_2(sK0_skl,sK2_skl))=k7_lattices(sK0_skl,sK2_skl)),
% 88.29/11.75 inference(resolution,[status(thm)],[f3452,f107])).
% 88.29/11.75 fof(f6886,plain,(
% 88.29/11.75 k7_lattices(k1_lattice2(sK0_skl),sK2_skl)=k7_lattices(sK0_skl,sK2_skl)),
% 88.29/11.75 inference(forward_demodulation,[status(thm)],[f1005,f6878])).
% 88.29/11.75 fof(f7111,plain,(
% 88.29/11.75 v3_struct_0(k1_lattice2(sK0_skl))|m1_filter_0(sK1_skl,k1_lattice2(sK0_skl))),
% 88.29/11.75 inference(resolution,[status(thm)],[f3688,f3729])).
% 88.29/11.75 fof(f7489,plain,(
% 88.29/11.75 ![X0,X1]: (v3_struct_0(k1_lattice2(sK0_skl))|~m1_filter_0(X0,k1_lattice2(sK0_skl))|~v1_filter_0(X0,k1_lattice2(sK0_skl))|~m1_subset_1(X1,u1_struct_0(k1_lattice2(sK0_skl)))|~r2_hidden(X1,X0)|~r2_hidden(k7_lattices(k1_lattice2(sK0_skl),X1),X0))),
% 88.29/11.75 inference(forward_subsumption_resolution,[status(thm)],[f4015,f543])).
% 88.29/11.75 fof(f7491,plain,(
% 88.29/11.75 ![X0]: (v3_struct_0(k1_lattice2(sK0_skl))|~m1_filter_0(X0,k1_lattice2(sK0_skl))|~v1_filter_0(X0,k1_lattice2(sK0_skl))|~m1_subset_1(sK2_skl,u1_struct_0(k1_lattice2(sK0_skl)))|~r2_hidden(sK2_skl,X0)|~r2_hidden(k7_lattices(sK0_skl,sK2_skl),X0))),
% 88.29/11.75 inference(paramodulation,[status(thm)],[f6886,f7489])).
% 88.29/11.75 fof(f7492,plain,(
% 88.29/11.75 ![X0]: (v3_struct_0(k1_lattice2(sK0_skl))|~m1_filter_0(X0,k1_lattice2(sK0_skl))|~v1_filter_0(X0,k1_lattice2(sK0_skl))|~r2_hidden(sK2_skl,X0)|~r2_hidden(k7_lattices(sK0_skl,sK2_skl),X0))),
% 88.29/11.75 inference(forward_subsumption_resolution,[status(thm)],[f7491,f1211])).
% 88.29/11.75 fof(f7782,plain,(
% 88.29/11.75 ![X0,X1]: (v3_struct_0(k1_lattice2(sK0_skl))|~m1_filter_0(X0,k1_lattice2(sK0_skl))|~v1_filter_0(X0,k1_lattice2(sK0_skl))|~m1_subset_1(X1,u1_struct_0(k1_lattice2(sK0_skl)))|r2_hidden(X1,X0)|r2_hidden(k7_lattices(k1_lattice2(sK0_skl),X1),X0))),
% 88.29/11.75 inference(forward_subsumption_resolution,[status(thm)],[f4109,f543])).
% 88.29/11.75 fof(f7783,plain,(
% 88.29/11.75 ![X0]: (v3_struct_0(k1_lattice2(sK0_skl))|~m1_filter_0(sK1_skl,k1_lattice2(sK0_skl))|~m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0_skl)))|r2_hidden(X0,sK1_skl)|r2_hidden(k7_lattices(k1_lattice2(sK0_skl),X0),sK1_skl))),
% 88.29/11.75 inference(resolution,[status(thm)],[f7782,f3730])).
% 88.29/11.75 fof(f7784,plain,(
% 88.29/11.75 ![X0]: (v3_struct_0(k1_lattice2(sK0_skl))|~m1_subset_1(X0,u1_struct_0(k1_lattice2(sK0_skl)))|r2_hidden(X0,sK1_skl)|r2_hidden(k7_lattices(k1_lattice2(sK0_skl),X0),sK1_skl))),
% 88.29/11.75 inference(forward_subsumption_resolution,[status(thm)],[f7783,f7111])).
% 88.29/11.75 fof(f10837,plain,(
% 88.29/11.75 ![X0,X1,X2]: (~v1_funct_1(u2_lattices(sK0_skl))|~v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~k1_lattice2(sK0_skl)=g3_lattices(X0,X1,X2)|u1_struct_0(sK0_skl)=X0)),
% 88.29/11.75 inference(backward_subsumption_resolution,[status(thm)],[f5461,f4224])).
% 88.29/11.75 fof(f10844,plain,(
% 88.29/11.75 ![X0,X1,X2]: (~v1_funct_2(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~k1_lattice2(sK0_skl)=g3_lattices(X0,X1,X2)|u1_struct_0(sK0_skl)=X0)),
% 88.29/11.75 inference(forward_subsumption_resolution,[status(thm)],[f10837,f1586])).
% 88.29/11.75 fof(f10854,plain,(
% 88.29/11.75 ![X0,X1,X2]: (~m1_relset_1(u2_lattices(sK0_skl),k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))|~k1_lattice2(sK0_skl)=g3_lattices(X0,X1,X2)|u1_struct_0(sK0_skl)=X0)),
% 88.29/11.75 inference(forward_subsumption_resolution,[status(thm)],[f10844,f1606])).
% 88.29/11.75 fof(f10873,plain,(
% 88.29/11.75 ![X0,X1,X2]: (~k1_lattice2(sK0_skl)=g3_lattices(X0,X1,X2)|u1_struct_0(sK0_skl)=X0)),
% 88.29/11.75 inference(backward_subsumption_resolution,[status(thm)],[f10854,f4258])).
% 88.29/11.75 fof(f10881,plain,(
% 88.29/11.75 u1_struct_0(sK0_skl)=u1_struct_0(k1_lattice2(sK0_skl))),
% 88.29/11.75 inference(resolution,[status(thm)],[f10873,f2103])).
% 88.29/11.75 fof(f25876,plain,(
% 88.29/11.75 ![X0]: (v3_struct_0(k1_lattice2(sK0_skl))|~m1_subset_1(X0,u1_struct_0(sK0_skl))|r2_hidden(X0,sK1_skl)|r2_hidden(k7_lattices(k1_lattice2(sK0_skl),X0),sK1_skl))),
% 88.29/11.75 inference(forward_demodulation,[status(thm)],[f10881,f7784])).
% 88.29/11.75 fof(f25944,plain,(
% 88.29/11.75 v3_struct_0(k1_lattice2(sK0_skl))|r2_hidden(sK2_skl,sK1_skl)|r2_hidden(k7_lattices(k1_lattice2(sK0_skl),sK2_skl),sK1_skl)),
% 88.29/11.75 inference(resolution,[status(thm)],[f25876,f107])).
% 88.29/11.75 fof(f25966,plain,(
% 88.29/11.75 v3_struct_0(k1_lattice2(sK0_skl))|r2_hidden(sK2_skl,sK1_skl)|r2_hidden(k7_lattices(sK0_skl,sK2_skl),sK1_skl)),
% 88.29/11.75 inference(forward_demodulation,[status(thm)],[f6886,f25944])).
% 88.29/11.75 fof(f25967,plain,(
% 88.29/11.75 v3_struct_0(k1_lattice2(sK0_skl))|r2_hidden(k7_lattices(sK0_skl,sK2_skl),sK1_skl)),
% 88.29/11.75 inference(forward_subsumption_resolution,[status(thm)],[f25966,f109])).
% 88.29/11.75 fof(f25968,plain,(
% 88.29/11.75 v3_struct_0(k1_lattice2(sK0_skl))|r2_hidden(sK2_skl,sK1_skl)),
% 88.29/11.75 inference(resolution,[status(thm)],[f25967,f108])).
% 88.29/11.75 fof(f43618,plain,(
% 88.29/11.75 v3_struct_0(k1_lattice2(sK0_skl))|~m1_filter_0(sK1_skl,k1_lattice2(sK0_skl))|~v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))|~r2_hidden(sK2_skl,sK1_skl)|v3_struct_0(k1_lattice2(sK0_skl))),
% 88.29/11.75 inference(resolution,[status(thm)],[f7492,f25967])).
% 88.29/11.75 fof(f43621,plain,(
% 88.29/11.75 v3_struct_0(k1_lattice2(sK0_skl))|~m1_filter_0(sK1_skl,k1_lattice2(sK0_skl))|~v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))|~r2_hidden(sK2_skl,sK1_skl)),
% 88.29/11.75 inference(duplicate_literals_removal,[status(thm)],[f43618])).
% 88.29/11.75 fof(f43622,plain,(
% 88.29/11.75 v3_struct_0(k1_lattice2(sK0_skl))|~v1_filter_0(sK1_skl,k1_lattice2(sK0_skl))|~r2_hidden(sK2_skl,sK1_skl)),
% 88.29/11.75 inference(forward_subsumption_resolution,[status(thm)],[f43621,f7111])).
% 88.29/11.75 fof(f43640,plain,(
% 88.29/11.75 v3_struct_0(k1_lattice2(sK0_skl))),
% 88.29/11.75 inference(backward_subsumption_resolution,[status(thm)],[f25968,f43641])).
% 88.29/11.75 fof(f43641,plain,(
% 88.29/11.75 v3_struct_0(k1_lattice2(sK0_skl))|~r2_hidden(sK2_skl,sK1_skl)),
% 88.29/11.75 inference(forward_subsumption_resolution,[status(thm)],[f43622,f3730])).
% 88.29/11.75 fof(f43643,plain,(
% 88.29/11.75 v3_struct_0(sK0_skl)|~l3_lattices(sK0_skl)),
% 88.29/11.75 inference(resolution,[status(thm)],[f43640,f238])).
% 88.29/11.75 fof(f43644,plain,(
% 88.29/11.75 ~l3_lattices(sK0_skl)),
% 88.29/11.75 inference(forward_subsumption_resolution,[status(thm)],[f43643,f101])).
% 88.29/11.75 fof(f43645,plain,(
% 88.29/11.75 $false),
% 88.29/11.75 inference(forward_subsumption_resolution,[status(thm)],[f43644,f104])).
% 57.62/11.87 % SZS output end CNFRefutation for theBenchmark.p
% 4.07/11.97 % Elapsed time: 11.512656 seconds
% 4.07/11.97 % CPU time: 90.264924 seconds
% 4.07/11.97 % Total memory used: 623.204 MB
% 4.07/11.97 % Net memory used: 608.924 MB
%------------------------------------------------------------------------------