%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT304+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 : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:03:36 PM UTC 2026
% Result : Theorem 0.14s 0.76s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT304+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n018.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:33:43 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.14/0.76 % Refutation found
% 0.14/0.76 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.76 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.76 fof(f1,conjecture,(
% 0.14/0.76 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> m2_filter_2(u1_struct_0(A),A) ) )),
% 0.14/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.76 fof(f2,negated_conjecture,(
% 0.14/0.76 ~((! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> m2_filter_2(u1_struct_0(A),A) ) ))),
% 0.14/0.76 inference(negated_conjecture,[status(cth)],[f1])).
% 0.14/0.76 fof(f3,axiom,(
% 0.14/0.76 (! [A] :( l3_lattices(A)=> ( v3_lattices(A)=> A = g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) ) ) )),
% 0.14/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.76 fof(f10,axiom,(
% 0.14/0.76 (! [A] :( l3_lattices(A)=> k1_lattice2(A) = g3_lattices(u1_struct_0(A),u1_lattices(A),u2_lattices(A)) ) )),
% 0.14/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.76 fof(f12,axiom,(
% 0.14/0.76 (! [A] :( l3_lattices(A)=> ( v3_lattices(k1_lattice2(A))& l3_lattices(k1_lattice2(A)) ) ) )),
% 0.14/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.76 fof(f19,axiom,(
% 0.14/0.76 (! [A] :( l3_lattices(A)=> ( l1_lattices(A)& l2_lattices(A) ) ) )),
% 0.14/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.76 fof(f27,axiom,(
% 0.14/0.76 (! [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)) ) ) )),
% 0.14/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.76 fof(f29,axiom,(
% 0.14/0.76 (! [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)) ) ) )),
% 0.14/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.76 fof(f41,axiom,(
% 0.14/0.76 (! [A] :( ( ~ v3_struct_0(A)& l3_lattices(A) )=> ( ~ v3_struct_0(k1_lattice2(A))& v3_lattices(k1_lattice2(A)) ) ) )),
% 0.14/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.76 fof(f51,axiom,(
% 0.14/0.76 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> ( ~ v3_struct_0(k1_lattice2(A))& v3_lattices(k1_lattice2(A))& v4_lattices(k1_lattice2(A))& v5_lattices(k1_lattice2(A))& v6_lattices(k1_lattice2(A))& v7_lattices(k1_lattice2(A))& v8_lattices(k1_lattice2(A))& v9_lattices(k1_lattice2(A))& v10_lattices(k1_lattice2(A)) ) ) )),
% 0.14/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.76 fof(f52,axiom,(
% 0.14/0.76 (! [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 ) ) )) )),
% 0.14/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.76 fof(f66,axiom,(
% 0.14/0.76 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m1_filter_2(B,A)<=> m1_filter_0(B,A) ) )) )),
% 0.14/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.76 fof(f67,axiom,(
% 0.14/0.76 (! [A,B,C] :( m2_relset_1(C,A,B)<=> m1_relset_1(C,A,B) ) )),
% 0.14/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.76 fof(f69,axiom,(
% 0.14/0.76 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> m1_filter_0(u1_struct_0(A),A) ) )),
% 0.14/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.76 fof(f71,axiom,(
% 0.14/0.76 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( m2_filter_2(B,A)<=> m1_filter_2(B,k1_lattice2(A)) ) )) )),
% 0.14/0.76 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.76 fof(f79,plain,(
% 0.14/0.76 (?[A]: (((~v3_struct_0(A)&v10_lattices(A))&l3_lattices(A))&~m2_filter_2(u1_struct_0(A),A)))),
% 0.14/0.76 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.14/0.76 fof(f80,plain,(
% 0.14/0.76 (((~v3_struct_0(sK0_skl)&v10_lattices(sK0_skl))&l3_lattices(sK0_skl))&~m2_filter_2(u1_struct_0(sK0_skl),sK0_skl))),
% 0.14/0.76 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(A,sK0_skl)],[f79])).
% 0.14/0.76 fof(f81,plain,(
% 0.14/0.76 ~v3_struct_0(sK0_skl)),
% 0.14/0.76 inference(cnf_transformation,[status(thm)],[f80])).
% 0.14/0.76 fof(f82,plain,(
% 0.14/0.76 v10_lattices(sK0_skl)),
% 0.14/0.76 inference(cnf_transformation,[status(thm)],[f80])).
% 0.14/0.76 fof(f83,plain,(
% 0.14/0.76 l3_lattices(sK0_skl)),
% 0.14/0.76 inference(cnf_transformation,[status(thm)],[f80])).
% 0.14/0.76 fof(f84,plain,(
% 0.14/0.76 ~m2_filter_2(u1_struct_0(sK0_skl),sK0_skl)),
% 0.14/0.76 inference(cnf_transformation,[status(thm)],[f80])).
% 0.14/0.76 fof(f85,plain,(
% 0.14/0.76 ![A]: (~l3_lattices(A)|(~v3_lattices(A)|A=g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A))))),
% 0.14/0.76 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.14/0.76 fof(f86,plain,(
% 0.14/0.76 ![X0]: (~l3_lattices(X0)|~v3_lattices(X0)|X0=g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)))),
% 0.14/0.76 inference(cnf_transformation,[status(thm)],[f85])).
% 0.14/0.76 fof(f109,plain,(
% 0.14/0.76 ![A]: (~l3_lattices(A)|k1_lattice2(A)=g3_lattices(u1_struct_0(A),u1_lattices(A),u2_lattices(A)))),
% 0.14/0.76 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.14/0.76 fof(f110,plain,(
% 0.14/0.76 ![X0]: (~l3_lattices(X0)|k1_lattice2(X0)=g3_lattices(u1_struct_0(X0),u1_lattices(X0),u2_lattices(X0)))),
% 0.14/0.76 inference(cnf_transformation,[status(thm)],[f109])).
% 0.14/0.76 fof(f114,plain,(
% 0.14/0.76 ![A]: (~l3_lattices(A)|(v3_lattices(k1_lattice2(A))&l3_lattices(k1_lattice2(A))))),
% 0.14/0.76 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.14/0.76 fof(f115,plain,(
% 0.14/0.76 ![X0]: (~l3_lattices(X0)|v3_lattices(k1_lattice2(X0)))),
% 0.14/0.76 inference(cnf_transformation,[status(thm)],[f114])).
% 0.14/0.76 fof(f116,plain,(
% 0.14/0.76 ![X0]: (~l3_lattices(X0)|l3_lattices(k1_lattice2(X0)))),
% 0.14/0.76 inference(cnf_transformation,[status(thm)],[f114])).
% 0.14/0.76 fof(f121,plain,(
% 0.14/0.76 ![A]: (~l3_lattices(A)|(l1_lattices(A)&l2_lattices(A)))),
% 0.14/0.76 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.14/0.76 fof(f122,plain,(
% 0.14/0.76 ![X0]: (~l3_lattices(X0)|l1_lattices(X0))),
% 0.14/0.76 inference(cnf_transformation,[status(thm)],[f121])).
% 0.14/0.76 fof(f123,plain,(
% 0.14/0.76 ![X0]: (~l3_lattices(X0)|l2_lattices(X0))),
% 0.14/0.76 inference(cnf_transformation,[status(thm)],[f121])).
% 0.14/0.76 fof(f137,plain,(
% 0.14/0.76 ![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))))),
% 0.14/0.76 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 0.14/0.76 fof(f138,plain,(
% 0.14/0.76 ![X0]: (~l1_lattices(X0)|v1_funct_1(u1_lattices(X0)))),
% 0.14/0.76 inference(cnf_transformation,[status(thm)],[f137])).
% 0.14/0.76 fof(f139,plain,(
% 0.14/0.76 ![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)))),
% 0.14/0.76 inference(cnf_transformation,[status(thm)],[f137])).
% 0.14/0.76 fof(f140,plain,(
% 0.14/0.76 ![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)))),
% 0.14/0.76 inference(cnf_transformation,[status(thm)],[f137])).
% 0.14/0.76 fof(f141,plain,(
% 0.14/0.76 ![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))))),
% 0.14/0.76 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 0.14/0.76 fof(f142,plain,(
% 0.14/0.76 ![X0]: (~l2_lattices(X0)|v1_funct_1(u2_lattices(X0)))),
% 0.14/0.76 inference(cnf_transformation,[status(thm)],[f141])).
% 0.14/0.76 fof(f143,plain,(
% 0.14/0.76 ![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)))),
% 0.14/0.76 inference(cnf_transformation,[status(thm)],[f141])).
% 0.14/0.76 fof(f144,plain,(
% 0.14/0.76 ![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)))),
% 0.14/0.76 inference(cnf_transformation,[status(thm)],[f141])).
% 0.14/0.76 fof(f171,plain,(
% 0.14/0.76 ![A]: ((v3_struct_0(A)|~l3_lattices(A))|(~v3_struct_0(k1_lattice2(A))&v3_lattices(k1_lattice2(A))))),
% 0.14/0.76 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 0.14/0.76 fof(f172,plain,(
% 0.14/0.76 ![X0]: (v3_struct_0(X0)|~l3_lattices(X0)|~v3_struct_0(k1_lattice2(X0)))),
% 0.14/0.76 inference(cnf_transformation,[status(thm)],[f171])).
% 0.14/0.76 fof(f207,plain,(
% 0.14/0.76 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|((((((((~v3_struct_0(k1_lattice2(A))&v3_lattices(k1_lattice2(A)))&v4_lattices(k1_lattice2(A)))&v5_lattices(k1_lattice2(A)))&v6_lattices(k1_lattice2(A)))&v7_lattices(k1_lattice2(A)))&v8_lattices(k1_lattice2(A)))&v9_lattices(k1_lattice2(A)))&v10_lattices(k1_lattice2(A))))),
% 0.14/0.76 inference(pre_NNF_transformation,[status(thm)],[f51])).
% 0.14/0.76 fof(f216,plain,(
% 0.14/0.76 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v10_lattices(k1_lattice2(X0)))),
% 0.14/0.76 inference(cnf_transformation,[status(thm)],[f207])).
% 0.14/0.76 fof(f217,plain,(
% 0.14/0.76 ![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))))),
% 0.14/0.76 inference(pre_NNF_transformation,[status(thm)],[f52])).
% 0.14/0.76 fof(f218,plain,(
% 0.14/0.76 ![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)),
% 0.14/0.76 inference(cnf_transformation,[status(thm)],[f217])).
% 0.14/0.76 fof(f272,plain,(
% 0.14/0.76 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (m1_filter_2(B,A)<=>m1_filter_0(B,A))))),
% 0.14/0.76 inference(pre_NNF_transformation,[status(thm)],[f66])).
% 0.14/0.76 fof(f273,plain,(
% 0.14/0.76 ![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)))))),
% 0.14/0.76 inference(NNF_transformation,[status(thm)],[f272])).
% 0.14/0.76 fof(f274,plain,(
% 0.14/0.76 ![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)))))),
% 0.14/0.76 inference(miniscoping,[status(thm)],[f273])).
% 0.14/0.76 fof(f276,plain,(
% 0.14/0.76 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|m1_filter_2(X1,X0)|~m1_filter_0(X1,X0))),
% 0.14/0.76 inference(cnf_transformation,[status(thm)],[f274])).
% 0.14/0.76 fof(f277,plain,(
% 0.14/0.76 ![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)))),
% 0.14/0.76 inference(NNF_transformation,[status(thm)],[f67])).
% 0.14/0.76 fof(f278,plain,(
% 0.14/0.76 (![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)))),
% 0.14/0.76 inference(miniscoping,[status(thm)],[f277])).
% 0.14/0.76 fof(f279,plain,(
% 0.14/0.76 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_relset_1(X0,X1,X2))),
% 0.14/0.76 inference(cnf_transformation,[status(thm)],[f278])).
% 0.14/0.76 fof(f283,plain,(
% 0.14/0.76 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|m1_filter_0(u1_struct_0(A),A))),
% 0.14/0.76 inference(pre_NNF_transformation,[status(thm)],[f69])).
% 0.14/0.76 fof(f284,plain,(
% 0.14/0.76 ![X0]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|m1_filter_0(u1_struct_0(X0),X0))),
% 0.14/0.76 inference(cnf_transformation,[status(thm)],[f283])).
% 0.14/0.76 fof(f287,plain,(
% 0.14/0.76 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (m2_filter_2(B,A)<=>m1_filter_2(B,k1_lattice2(A)))))),
% 0.14/0.76 inference(pre_NNF_transformation,[status(thm)],[f71])).
% 0.14/0.76 fof(f288,plain,(
% 0.14/0.76 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: ((~m2_filter_2(B,A)|m1_filter_2(B,k1_lattice2(A)))&(m2_filter_2(B,A)|~m1_filter_2(B,k1_lattice2(A))))))),
% 0.14/0.76 inference(NNF_transformation,[status(thm)],[f287])).
% 0.14/0.76 fof(f289,plain,(
% 0.14/0.76 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|((![B]: (~m2_filter_2(B,A)|m1_filter_2(B,k1_lattice2(A))))&(![B]: (m2_filter_2(B,A)|~m1_filter_2(B,k1_lattice2(A))))))),
% 0.14/0.76 inference(miniscoping,[status(thm)],[f288])).
% 0.14/0.76 fof(f291,plain,(
% 0.14/0.76 ![X0,X1]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|m2_filter_2(X1,X0)|~m1_filter_2(X1,k1_lattice2(X0)))),
% 0.14/0.76 inference(cnf_transformation,[status(thm)],[f289])).
% 0.14/0.76 fof(f346,plain,(
% 0.14/0.76 k1_lattice2(sK0_skl)=g3_lattices(u1_struct_0(sK0_skl),u1_lattices(sK0_skl),u2_lattices(sK0_skl))),
% 0.14/0.76 inference(resolution,[status(thm)],[f110,f83])).
% 0.14/0.76 fof(f348,plain,(
% 0.14/0.76 v3_lattices(k1_lattice2(sK0_skl))),
% 0.14/0.76 inference(resolution,[status(thm)],[f115,f83])).
% 0.14/0.76 fof(f350,plain,(
% 0.14/0.76 l3_lattices(k1_lattice2(sK0_skl))),
% 0.14/0.76 inference(resolution,[status(thm)],[f116,f83])).
% 0.14/0.76 fof(f351,plain,(
% 0.14/0.76 ~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)))),
% 0.14/0.76 inference(resolution,[status(thm)],[f348,f86])).
% 0.14/0.76 fof(f372,plain,(
% 0.14/0.76 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)))),
% 0.14/0.76 inference(forward_subsumption_resolution,[status(thm)],[f351,f350])).
% 0.14/0.76 fof(f382,plain,(
% 0.14/0.76 l1_lattices(sK0_skl)),
% 0.14/0.76 inference(resolution,[status(thm)],[f122,f83])).
% 0.14/0.76 fof(f386,plain,(
% 0.14/0.76 l2_lattices(sK0_skl)),
% 0.14/0.76 inference(resolution,[status(thm)],[f123,f83])).
% 0.14/0.76 fof(f396,plain,(
% 0.14/0.76 v1_funct_1(u1_lattices(sK0_skl))),
% 0.14/0.76 inference(resolution,[status(thm)],[f138,f382])).
% 0.14/0.76 fof(f416,plain,(
% 0.14/0.76 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))),
% 0.14/0.76 inference(resolution,[status(thm)],[f139,f382])).
% 0.14/0.76 fof(f419,plain,(
% 0.14/0.76 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))),
% 0.14/0.76 inference(resolution,[status(thm)],[f140,f382])).
% 0.14/0.76 fof(f422,plain,(
% 0.14/0.76 v1_funct_1(u2_lattices(sK0_skl))),
% 0.14/0.76 inference(resolution,[status(thm)],[f142,f386])).
% 0.14/0.76 fof(f425,plain,(
% 0.14/0.76 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))),
% 0.14/0.76 inference(resolution,[status(thm)],[f143,f386])).
% 0.14/0.76 fof(f428,plain,(
% 0.14/0.76 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))),
% 0.14/0.76 inference(resolution,[status(thm)],[f144,f386])).
% 0.14/0.76 fof(f824,plain,(
% 0.14/0.76 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|v10_lattices(k1_lattice2(sK0_skl))),
% 0.14/0.76 inference(resolution,[status(thm)],[f216,f83])).
% 0.14/0.76 fof(f827,plain,(
% 0.14/0.76 ~v10_lattices(sK0_skl)|v10_lattices(k1_lattice2(sK0_skl))),
% 0.14/0.76 inference(forward_subsumption_resolution,[status(thm)],[f824,f81])).
% 0.14/0.76 fof(f849,plain,(
% 0.14/0.76 v10_lattices(k1_lattice2(sK0_skl))),
% 0.14/0.76 inference(forward_subsumption_resolution,[status(thm)],[f827,f82])).
% 0.14/0.76 fof(f883,plain,(
% 0.14/0.76 ![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)),
% 0.14/0.76 inference(paramodulation,[status(thm)],[f346,f218])).
% 0.14/0.76 fof(f894,plain,(
% 0.14/0.76 ![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)),
% 0.14/0.76 inference(forward_subsumption_resolution,[status(thm)],[f883,f396])).
% 0.14/0.76 fof(f1070,plain,(
% 0.14/0.76 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))),
% 0.14/0.76 inference(resolution,[status(thm)],[f279,f428])).
% 0.14/0.76 fof(f1072,plain,(
% 0.14/0.76 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))),
% 0.14/0.76 inference(resolution,[status(thm)],[f279,f419])).
% 0.14/0.76 fof(f1080,plain,(
% 0.14/0.76 v3_struct_0(k1_lattice2(sK0_skl))|~v10_lattices(k1_lattice2(sK0_skl))|m1_filter_0(u1_struct_0(k1_lattice2(sK0_skl)),k1_lattice2(sK0_skl))),
% 0.14/0.76 inference(resolution,[status(thm)],[f284,f350])).
% 0.14/0.76 fof(f1085,plain,(
% 0.14/0.76 v3_struct_0(k1_lattice2(sK0_skl))|m1_filter_0(u1_struct_0(k1_lattice2(sK0_skl)),k1_lattice2(sK0_skl))),
% 0.14/0.76 inference(forward_subsumption_resolution,[status(thm)],[f1080,f849])).
% 0.14/0.76 fof(f1135,plain,(
% 0.14/0.76 ![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)),
% 0.14/0.78 inference(forward_subsumption_resolution,[status(thm)],[f894,f416])).
% 0.14/0.78 fof(f1246,plain,(
% 0.14/0.78 v3_struct_0(k1_lattice2(sK0_skl))|v3_struct_0(k1_lattice2(sK0_skl))|~v10_lattices(k1_lattice2(sK0_skl))|~l3_lattices(k1_lattice2(sK0_skl))|m1_filter_2(u1_struct_0(k1_lattice2(sK0_skl)),k1_lattice2(sK0_skl))),
% 0.14/0.78 inference(resolution,[status(thm)],[f1085,f276])).
% 0.14/0.78 fof(f1249,plain,(
% 0.14/0.78 v3_struct_0(k1_lattice2(sK0_skl))|~v10_lattices(k1_lattice2(sK0_skl))|~l3_lattices(k1_lattice2(sK0_skl))|m1_filter_2(u1_struct_0(k1_lattice2(sK0_skl)),k1_lattice2(sK0_skl))),
% 0.14/0.78 inference(duplicate_literals_removal,[status(thm)],[f1246])).
% 0.14/0.78 fof(f1250,plain,(
% 0.14/0.78 v3_struct_0(k1_lattice2(sK0_skl))|~l3_lattices(k1_lattice2(sK0_skl))|m1_filter_2(u1_struct_0(k1_lattice2(sK0_skl)),k1_lattice2(sK0_skl))),
% 0.14/0.78 inference(forward_subsumption_resolution,[status(thm)],[f1249,f849])).
% 0.14/0.78 fof(f1703,plain,(
% 0.14/0.78 ![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))|~k1_lattice2(sK0_skl)=g3_lattices(X0,X1,X2)|u1_struct_0(sK0_skl)=X0)),
% 0.14/0.78 inference(backward_subsumption_resolution,[status(thm)],[f1135,f1070])).
% 0.14/0.78 fof(f1746,plain,(
% 0.14/0.78 ![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_2(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)),
% 0.14/0.78 inference(forward_subsumption_resolution,[status(thm)],[f1703,f422])).
% 0.14/0.78 fof(f1829,plain,(
% 0.14/0.78 ![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))|~k1_lattice2(sK0_skl)=g3_lattices(X0,X1,X2)|u1_struct_0(sK0_skl)=X0)),
% 0.14/0.78 inference(forward_subsumption_resolution,[status(thm)],[f1746,f425])).
% 0.14/0.78 fof(f1830,plain,(
% 0.14/0.78 ![X0,X1,X2]: (~k1_lattice2(sK0_skl)=g3_lattices(X0,X1,X2)|u1_struct_0(sK0_skl)=X0)),
% 0.14/0.78 inference(backward_subsumption_resolution,[status(thm)],[f1829,f1072])).
% 0.14/0.78 fof(f1916,plain,(
% 0.14/0.78 u1_struct_0(sK0_skl)=u1_struct_0(k1_lattice2(sK0_skl))),
% 0.14/0.78 inference(resolution,[status(thm)],[f1830,f372])).
% 0.14/0.78 fof(f2332,plain,(
% 0.14/0.78 v3_struct_0(k1_lattice2(sK0_skl))|~l3_lattices(k1_lattice2(sK0_skl))|m1_filter_2(u1_struct_0(sK0_skl),k1_lattice2(sK0_skl))),
% 0.14/0.78 inference(forward_demodulation,[status(thm)],[f1916,f1250])).
% 0.14/0.78 fof(f2333,plain,(
% 0.14/0.78 v3_struct_0(k1_lattice2(sK0_skl))|m1_filter_2(u1_struct_0(sK0_skl),k1_lattice2(sK0_skl))),
% 0.14/0.78 inference(forward_subsumption_resolution,[status(thm)],[f2332,f350])).
% 0.14/0.78 fof(f2334,plain,(
% 0.14/0.78 v3_struct_0(k1_lattice2(sK0_skl))|v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m2_filter_2(u1_struct_0(sK0_skl),sK0_skl)),
% 0.14/0.78 inference(resolution,[status(thm)],[f2333,f291])).
% 0.14/0.78 fof(f2338,plain,(
% 0.14/0.78 v3_struct_0(sK0_skl)|~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m2_filter_2(u1_struct_0(sK0_skl),sK0_skl)),
% 0.14/0.78 inference(forward_subsumption_resolution,[status(thm)],[f2334,f172])).
% 0.14/0.78 fof(f5394,plain,(
% 0.14/0.78 ~v10_lattices(sK0_skl)|~l3_lattices(sK0_skl)|m2_filter_2(u1_struct_0(sK0_skl),sK0_skl)),
% 0.14/0.78 inference(forward_subsumption_resolution,[status(thm)],[f2338,f81])).
% 0.14/0.78 fof(f5395,plain,(
% 0.14/0.78 ~v10_lattices(sK0_skl)|m2_filter_2(u1_struct_0(sK0_skl),sK0_skl)),
% 0.14/0.78 inference(resolution,[status(thm)],[f5394,f83])).
% 0.14/0.78 fof(f5396,plain,(
% 0.14/0.78 m2_filter_2(u1_struct_0(sK0_skl),sK0_skl)),
% 0.14/0.78 inference(forward_subsumption_resolution,[status(thm)],[f5395,f82])).
% 0.14/0.78 fof(f5411,plain,(
% 0.14/0.78 $false),
% 0.14/0.78 inference(forward_subsumption_resolution,[status(thm)],[f5396,f84])).
% 0.14/0.78 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.82 % Elapsed time: 0.435397 seconds
% 0.14/0.82 % CPU time: 2.821904 seconds
% 0.14/0.82 % Total memory used: 125.832 MB
% 0.14/0.82 % Net memory used: 124.345 MB
%------------------------------------------------------------------------------