%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP653+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 : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:37:04 PM UTC 2026
% Result : Theorem 0.15s 0.48s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP653+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.15/0.42 % Computer : n006.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Sun Sep 20 20:27:43 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.44 % Drodi V4.1.1
% 0.15/0.48 % Refutation found
% 0.15/0.48 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.48 % SZS output start CNFRefutation for theBenchmark
% 0.15/0.48 fof(f1,conjecture,(
% 0.15/0.48 (! [A] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v3_group_1(B)& v4_group_1(B)& l1_group_1(B) )=> (! [C] :( ( v1_funct_1(C)& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))& v1_group_6(C,A,B)& m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )=> ( v2_funct_1(C)=> m1_lattice4(k3_latsubgr(A,B,C),k11_group_4(A),k11_group_4(B)) ) ) )) )) )),
% 0.15/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.48 fof(f2,negated_conjecture,(
% 0.15/0.48 ~((! [A] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v3_group_1(B)& v4_group_1(B)& l1_group_1(B) )=> (! [C] :( ( v1_funct_1(C)& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))& v1_group_6(C,A,B)& m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )=> ( v2_funct_1(C)=> m1_lattice4(k3_latsubgr(A,B,C),k11_group_4(A),k11_group_4(B)) ) ) )) )) ))),
% 0.15/0.48 inference(negated_conjecture,[status(cth)],[f1])).
% 0.15/0.48 fof(f10,axiom,(
% 0.15/0.48 (! [A] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> ( ~ v3_struct_0(k11_group_4(A))& v3_lattices(k11_group_4(A))& v10_lattices(k11_group_4(A))& l3_lattices(k11_group_4(A)) ) ) )),
% 0.15/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.48 fof(f14,axiom,(
% 0.15/0.48 (! [A,B,C] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A)& ~ v3_struct_0(B)& v3_group_1(B)& v4_group_1(B)& l1_group_1(B)& v1_funct_1(C)& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))& m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )=> ( v1_funct_1(k3_latsubgr(A,B,C))& v1_funct_2(k3_latsubgr(A,B,C),u1_struct_0(k11_group_4(A)),u1_struct_0(k11_group_4(B)))& m2_relset_1(k3_latsubgr(A,B,C),u1_struct_0(k11_group_4(A)),u1_struct_0(k11_group_4(B))) ) ) )),
% 0.15/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.48 fof(f25,axiom,(
% 0.15/0.48 (! [A,B] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A)& ~ v3_struct_0(B)& v10_lattices(B)& l3_lattices(B) )=> (! [C] :( m4_vectsp_8(C,A,B)=> ( v1_funct_1(C)& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))& m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) ) ) )) )),
% 0.15/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.48 fof(f55,axiom,(
% 0.15/0.48 (! [A,B,C] :( m2_relset_1(C,A,B)<=> m1_relset_1(C,A,B) ) )),
% 0.15/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.48 fof(f57,axiom,(
% 0.15/0.48 (! [A] :( ( ~ v3_struct_0(A)& v10_lattices(A)& l3_lattices(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v10_lattices(B)& l3_lattices(B) )=> (! [C] :( ( v1_funct_1(C)& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))& m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )=> ( m1_lattice4(C,A,B)<=> ( m4_vectsp_8(C,A,B)& m3_vectsp_8(C,A,B) ) ) ) )) )) )),
% 0.15/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.48 fof(f60,axiom,(
% 0.15/0.48 (! [A] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v3_group_1(B)& v4_group_1(B)& l1_group_1(B) )=> (! [C] :( ( v1_funct_1(C)& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))& v1_group_6(C,A,B)& m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )=> ( v2_funct_1(C)=> m3_vectsp_8(k3_latsubgr(A,B,C),k11_group_4(A),k11_group_4(B)) ) ) )) )) )),
% 0.15/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.48 fof(f61,axiom,(
% 0.15/0.48 (! [A] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v3_group_1(B)& v4_group_1(B)& l1_group_1(B) )=> (! [C] :( ( v1_funct_1(C)& v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))& v1_group_6(C,A,B)& m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )=> m4_vectsp_8(k3_latsubgr(A,B,C),k11_group_4(A),k11_group_4(B)) ) )) )) )),
% 0.15/0.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.48 fof(f68,plain,(
% 0.15/0.48 (?[A]: ((((~v3_struct_0(A)&v3_group_1(A))&v4_group_1(A))&l1_group_1(A))&(?[B]: ((((~v3_struct_0(B)&v3_group_1(B))&v4_group_1(B))&l1_group_1(B))&(?[C]: ((((v1_funct_1(C)&v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)))&v1_group_6(C,A,B))&m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)))&(v2_funct_1(C)&~m1_lattice4(k3_latsubgr(A,B,C),k11_group_4(A),k11_group_4(B)))))))))),
% 0.15/0.49 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.15/0.49 fof(f69,plain,(
% 0.15/0.49 ((((~v3_struct_0(sK0_skl)&v3_group_1(sK0_skl))&v4_group_1(sK0_skl))&l1_group_1(sK0_skl))&((((~v3_struct_0(sK1_skl)&v3_group_1(sK1_skl))&v4_group_1(sK1_skl))&l1_group_1(sK1_skl))&((((v1_funct_1(sK2_skl)&v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))&v1_group_6(sK2_skl,sK0_skl,sK1_skl))&m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))&(v2_funct_1(sK2_skl)&~m1_lattice4(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),k11_group_4(sK0_skl),k11_group_4(sK1_skl))))))),
% 0.15/0.49 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)],[f68])).
% 0.15/0.49 fof(f70,plain,(
% 0.15/0.49 ~v3_struct_0(sK0_skl)),
% 0.15/0.49 inference(cnf_transformation,[status(thm)],[f69])).
% 0.15/0.49 fof(f71,plain,(
% 0.15/0.49 v3_group_1(sK0_skl)),
% 0.15/0.49 inference(cnf_transformation,[status(thm)],[f69])).
% 0.15/0.49 fof(f72,plain,(
% 0.15/0.49 v4_group_1(sK0_skl)),
% 0.15/0.49 inference(cnf_transformation,[status(thm)],[f69])).
% 0.15/0.49 fof(f73,plain,(
% 0.15/0.49 l1_group_1(sK0_skl)),
% 0.15/0.49 inference(cnf_transformation,[status(thm)],[f69])).
% 0.15/0.49 fof(f74,plain,(
% 0.15/0.49 ~v3_struct_0(sK1_skl)),
% 0.15/0.49 inference(cnf_transformation,[status(thm)],[f69])).
% 0.15/0.49 fof(f75,plain,(
% 0.15/0.49 v3_group_1(sK1_skl)),
% 0.15/0.49 inference(cnf_transformation,[status(thm)],[f69])).
% 0.15/0.49 fof(f76,plain,(
% 0.15/0.49 v4_group_1(sK1_skl)),
% 0.15/0.49 inference(cnf_transformation,[status(thm)],[f69])).
% 0.15/0.49 fof(f77,plain,(
% 0.15/0.49 l1_group_1(sK1_skl)),
% 0.15/0.49 inference(cnf_transformation,[status(thm)],[f69])).
% 0.15/0.49 fof(f78,plain,(
% 0.15/0.49 v1_funct_1(sK2_skl)),
% 0.15/0.49 inference(cnf_transformation,[status(thm)],[f69])).
% 0.15/0.49 fof(f79,plain,(
% 0.15/0.49 v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
% 0.15/0.49 inference(cnf_transformation,[status(thm)],[f69])).
% 0.15/0.49 fof(f80,plain,(
% 0.15/0.49 v1_group_6(sK2_skl,sK0_skl,sK1_skl)),
% 0.15/0.49 inference(cnf_transformation,[status(thm)],[f69])).
% 0.15/0.49 fof(f81,plain,(
% 0.15/0.49 m2_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
% 0.15/0.49 inference(cnf_transformation,[status(thm)],[f69])).
% 0.15/0.49 fof(f82,plain,(
% 0.15/0.49 v2_funct_1(sK2_skl)),
% 0.15/0.49 inference(cnf_transformation,[status(thm)],[f69])).
% 0.15/0.49 fof(f83,plain,(
% 0.15/0.49 ~m1_lattice4(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),k11_group_4(sK0_skl),k11_group_4(sK1_skl))),
% 0.15/0.49 inference(cnf_transformation,[status(thm)],[f69])).
% 0.15/0.49 fof(f107,plain,(
% 0.15/0.49 ![A]: ((((v3_struct_0(A)|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|(((~v3_struct_0(k11_group_4(A))&v3_lattices(k11_group_4(A)))&v10_lattices(k11_group_4(A)))&l3_lattices(k11_group_4(A))))),
% 0.15/0.49 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.15/0.49 fof(f108,plain,(
% 0.15/0.49 ![X0]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~v3_struct_0(k11_group_4(X0)))),
% 0.15/0.49 inference(cnf_transformation,[status(thm)],[f107])).
% 0.15/0.49 fof(f110,plain,(
% 0.15/0.49 ![X0]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|v10_lattices(k11_group_4(X0)))),
% 0.15/0.49 inference(cnf_transformation,[status(thm)],[f107])).
% 0.15/0.49 fof(f111,plain,(
% 0.15/0.49 ![X0]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|l3_lattices(k11_group_4(X0)))),
% 0.15/0.49 inference(cnf_transformation,[status(thm)],[f107])).
% 0.15/0.49 fof(f112,plain,(
% 0.15/0.49 ![A,B,C]: (((((((((((v3_struct_0(A)|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|v3_struct_0(B))|~v3_group_1(B))|~v4_group_1(B))|~l1_group_1(B))|~v1_funct_1(C))|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)))|~m1_relset_1(C,u1_struct_0(A),u1_struct_0(B)))|((v1_funct_1(k3_latsubgr(A,B,C))&v1_funct_2(k3_latsubgr(A,B,C),u1_struct_0(k11_group_4(A)),u1_struct_0(k11_group_4(B))))&m2_relset_1(k3_latsubgr(A,B,C),u1_struct_0(k11_group_4(A)),u1_struct_0(k11_group_4(B)))))),
% 0.15/0.49 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.15/0.49 fof(f114,plain,(
% 0.15/0.49 ![X0,X1,X2]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|v3_struct_0(X1)|~v3_group_1(X1)|~v4_group_1(X1)|~l1_group_1(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|v1_funct_2(k3_latsubgr(X0,X1,X2),u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1))))),
% 0.15/0.49 inference(cnf_transformation,[status(thm)],[f112])).
% 0.15/0.49 fof(f115,plain,(
% 0.15/0.49 ![X0,X1,X2]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|v3_struct_0(X1)|~v3_group_1(X1)|~v4_group_1(X1)|~l1_group_1(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m1_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|m2_relset_1(k3_latsubgr(X0,X1,X2),u1_struct_0(k11_group_4(X0)),u1_struct_0(k11_group_4(X1))))),
% 0.15/0.49 inference(cnf_transformation,[status(thm)],[f112])).
% 0.15/0.49 fof(f135,plain,(
% 0.15/0.49 ![A,B]: ((((((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|v3_struct_0(B))|~v10_lattices(B))|~l3_lattices(B))|(![C]: (~m4_vectsp_8(C,A,B)|((v1_funct_1(C)&v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)))&m2_relset_1(C,u1_struct_0(A),u1_struct_0(B))))))),
% 0.15/0.49 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 0.15/0.49 fof(f136,plain,(
% 0.15/0.49 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v3_struct_0(X1)|~v10_lattices(X1)|~l3_lattices(X1)|~m4_vectsp_8(X2,X0,X1)|v1_funct_1(X2))),
% 0.15/0.49 inference(cnf_transformation,[status(thm)],[f135])).
% 0.15/0.49 fof(f227,plain,(
% 0.15/0.49 ![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.15/0.50 inference(NNF_transformation,[status(thm)],[f55])).
% 0.15/0.50 fof(f228,plain,(
% 0.15/0.50 (![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.15/0.50 inference(miniscoping,[status(thm)],[f227])).
% 0.15/0.50 fof(f229,plain,(
% 0.15/0.50 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_relset_1(X0,X1,X2))),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f228])).
% 0.15/0.50 fof(f233,plain,(
% 0.15/0.50 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (((v3_struct_0(B)|~v10_lattices(B))|~l3_lattices(B))|(![C]: (((~v1_funct_1(C)|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)))|~m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)))|(m1_lattice4(C,A,B)<=>(m4_vectsp_8(C,A,B)&m3_vectsp_8(C,A,B))))))))),
% 0.15/0.50 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 0.15/0.50 fof(f234,plain,(
% 0.15/0.50 ![A]: (((v3_struct_0(A)|~v10_lattices(A))|~l3_lattices(A))|(![B]: (((v3_struct_0(B)|~v10_lattices(B))|~l3_lattices(B))|(![C]: (((~v1_funct_1(C)|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)))|~m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)))|((~m1_lattice4(C,A,B)|(m4_vectsp_8(C,A,B)&m3_vectsp_8(C,A,B)))&(m1_lattice4(C,A,B)|(~m4_vectsp_8(C,A,B)|~m3_vectsp_8(C,A,B)))))))))),
% 0.15/0.50 inference(NNF_transformation,[status(thm)],[f233])).
% 0.15/0.50 fof(f237,plain,(
% 0.15/0.50 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v3_struct_0(X1)|~v10_lattices(X1)|~l3_lattices(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|m1_lattice4(X2,X0,X1)|~m4_vectsp_8(X2,X0,X1)|~m3_vectsp_8(X2,X0,X1))),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f234])).
% 0.15/0.50 fof(f242,plain,(
% 0.15/0.50 ![A]: ((((v3_struct_0(A)|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|(![B]: ((((v3_struct_0(B)|~v3_group_1(B))|~v4_group_1(B))|~l1_group_1(B))|(![C]: ((((~v1_funct_1(C)|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)))|~v1_group_6(C,A,B))|~m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)))|(~v2_funct_1(C)|m3_vectsp_8(k3_latsubgr(A,B,C),k11_group_4(A),k11_group_4(B))))))))),
% 0.15/0.50 inference(pre_NNF_transformation,[status(thm)],[f60])).
% 0.15/0.50 fof(f243,plain,(
% 0.15/0.50 ![X0,X1,X2]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|v3_struct_0(X1)|~v3_group_1(X1)|~v4_group_1(X1)|~l1_group_1(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~v1_group_6(X2,X0,X1)|~m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|~v2_funct_1(X2)|m3_vectsp_8(k3_latsubgr(X0,X1,X2),k11_group_4(X0),k11_group_4(X1)))),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f242])).
% 0.15/0.50 fof(f244,plain,(
% 0.15/0.50 ![A]: ((((v3_struct_0(A)|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|(![B]: ((((v3_struct_0(B)|~v3_group_1(B))|~v4_group_1(B))|~l1_group_1(B))|(![C]: ((((~v1_funct_1(C)|~v1_funct_2(C,u1_struct_0(A),u1_struct_0(B)))|~v1_group_6(C,A,B))|~m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)))|m4_vectsp_8(k3_latsubgr(A,B,C),k11_group_4(A),k11_group_4(B)))))))),
% 0.15/0.50 inference(pre_NNF_transformation,[status(thm)],[f61])).
% 0.15/0.50 fof(f245,plain,(
% 0.15/0.50 ![X0,X1,X2]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|v3_struct_0(X1)|~v3_group_1(X1)|~v4_group_1(X1)|~l1_group_1(X1)|~v1_funct_1(X2)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~v1_group_6(X2,X0,X1)|~m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|m4_vectsp_8(k3_latsubgr(X0,X1,X2),k11_group_4(X0),k11_group_4(X1)))),
% 0.15/0.50 inference(cnf_transformation,[status(thm)],[f244])).
% 0.15/0.50 fof(f266,plain,(
% 0.15/0.50 ![X0,X1,X2]: (v3_struct_0(X0)|~v10_lattices(X0)|~l3_lattices(X0)|v3_struct_0(X1)|~v10_lattices(X1)|~l3_lattices(X1)|~v1_funct_2(X2,u1_struct_0(X0),u1_struct_0(X1))|~m2_relset_1(X2,u1_struct_0(X0),u1_struct_0(X1))|m1_lattice4(X2,X0,X1)|~m4_vectsp_8(X2,X0,X1)|~m3_vectsp_8(X2,X0,X1))),
% 0.15/0.50 inference(forward_subsumption_resolution,[status(thm)],[f237,f136])).
% 0.15/0.50 fof(f267,plain,(
% 0.15/0.50 v3_struct_0(sK1_skl)|~v3_group_1(sK1_skl)|~l1_group_1(sK1_skl)|v10_lattices(k11_group_4(sK1_skl))),
% 0.15/0.50 inference(resolution,[status(thm)],[f110,f76])).
% 0.15/0.50 fof(f268,plain,(
% 0.15/0.50 v3_struct_0(sK0_skl)|~v3_group_1(sK0_skl)|~l1_group_1(sK0_skl)|v10_lattices(k11_group_4(sK0_skl))),
% 0.15/0.50 inference(resolution,[status(thm)],[f110,f72])).
% 0.15/0.50 fof(f269,definition,(
% 0.15/0.50 sQ0_spl <=> (v3_struct_0(sK1_skl))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f270,plain,(
% 0.15/0.50 v3_struct_0(sK1_skl)|~sQ0_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f269])).
% 0.15/0.50 fof(f272,definition,(
% 0.15/0.50 sQ1_spl <=> (v3_group_1(sK1_skl))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f274,plain,(
% 0.15/0.50 ~v3_group_1(sK1_skl)|sQ1_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f272])).
% 0.15/0.50 fof(f275,definition,(
% 0.15/0.50 sQ2_spl <=> (l1_group_1(sK1_skl))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f277,plain,(
% 0.15/0.50 ~l1_group_1(sK1_skl)|sQ2_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f275])).
% 0.15/0.50 fof(f278,definition,(
% 0.15/0.50 sQ3_spl <=> (v10_lattices(k11_group_4(sK1_skl)))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f281,plain,(
% 0.15/0.50 sQ0_spl|~sQ1_spl|~sQ2_spl|sQ3_spl),
% 0.15/0.50 inference(split_clause,[status(thm)],[f267,f269,f272,f275,f278])).
% 0.15/0.50 fof(f282,definition,(
% 0.15/0.50 sQ4_spl <=> (v3_struct_0(sK0_skl))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f283,plain,(
% 0.15/0.50 v3_struct_0(sK0_skl)|~sQ4_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f282])).
% 0.15/0.50 fof(f285,definition,(
% 0.15/0.50 sQ5_spl <=> (v3_group_1(sK0_skl))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f287,plain,(
% 0.15/0.50 ~v3_group_1(sK0_skl)|sQ5_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f285])).
% 0.15/0.50 fof(f288,definition,(
% 0.15/0.50 sQ6_spl <=> (l1_group_1(sK0_skl))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f290,plain,(
% 0.15/0.50 ~l1_group_1(sK0_skl)|sQ6_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f288])).
% 0.15/0.50 fof(f291,definition,(
% 0.15/0.50 sQ7_spl <=> (v10_lattices(k11_group_4(sK0_skl)))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f294,plain,(
% 0.15/0.50 sQ4_spl|~sQ5_spl|~sQ6_spl|sQ7_spl),
% 0.15/0.50 inference(split_clause,[status(thm)],[f268,f282,f285,f288,f291])).
% 0.15/0.50 fof(f295,plain,(
% 0.15/0.50 $false|sQ6_spl),
% 0.15/0.50 inference(forward_subsumption_resolution,[status(thm)],[f290,f73])).
% 0.15/0.50 fof(f296,plain,(
% 0.15/0.50 sQ6_spl),
% 0.15/0.50 inference(contradiction_clause,[status(thm)],[f295])).
% 0.15/0.50 fof(f297,plain,(
% 0.15/0.50 $false|sQ5_spl),
% 0.15/0.50 inference(forward_subsumption_resolution,[status(thm)],[f287,f71])).
% 0.15/0.50 fof(f298,plain,(
% 0.15/0.50 sQ5_spl),
% 0.15/0.50 inference(contradiction_clause,[status(thm)],[f297])).
% 0.15/0.50 fof(f299,plain,(
% 0.15/0.50 $false|~sQ4_spl),
% 0.15/0.50 inference(forward_subsumption_resolution,[status(thm)],[f283,f70])).
% 0.15/0.50 fof(f300,plain,(
% 0.15/0.50 ~sQ4_spl),
% 0.15/0.50 inference(contradiction_clause,[status(thm)],[f299])).
% 0.15/0.50 fof(f301,plain,(
% 0.15/0.50 v3_struct_0(sK1_skl)|~v3_group_1(sK1_skl)|~l1_group_1(sK1_skl)|l3_lattices(k11_group_4(sK1_skl))),
% 0.15/0.50 inference(resolution,[status(thm)],[f111,f76])).
% 0.15/0.50 fof(f302,plain,(
% 0.15/0.50 v3_struct_0(sK0_skl)|~v3_group_1(sK0_skl)|~l1_group_1(sK0_skl)|l3_lattices(k11_group_4(sK0_skl))),
% 0.15/0.50 inference(resolution,[status(thm)],[f111,f72])).
% 0.15/0.50 fof(f303,definition,(
% 0.15/0.50 sQ8_spl <=> (l3_lattices(k11_group_4(sK1_skl)))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f306,plain,(
% 0.15/0.50 sQ0_spl|~sQ1_spl|~sQ2_spl|sQ8_spl),
% 0.15/0.50 inference(split_clause,[status(thm)],[f301,f269,f272,f275,f303])).
% 0.15/0.50 fof(f307,definition,(
% 0.15/0.50 sQ9_spl <=> (l3_lattices(k11_group_4(sK0_skl)))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f310,plain,(
% 0.15/0.50 sQ4_spl|~sQ5_spl|~sQ6_spl|sQ9_spl),
% 0.15/0.50 inference(split_clause,[status(thm)],[f302,f282,f285,f288,f307])).
% 0.15/0.50 fof(f311,plain,(
% 0.15/0.50 $false|sQ2_spl),
% 0.15/0.50 inference(forward_subsumption_resolution,[status(thm)],[f277,f77])).
% 0.15/0.50 fof(f312,plain,(
% 0.15/0.50 sQ2_spl),
% 0.15/0.50 inference(contradiction_clause,[status(thm)],[f311])).
% 0.15/0.50 fof(f313,plain,(
% 0.15/0.50 $false|sQ1_spl),
% 0.15/0.50 inference(forward_subsumption_resolution,[status(thm)],[f274,f75])).
% 0.15/0.50 fof(f314,plain,(
% 0.15/0.50 sQ1_spl),
% 0.15/0.50 inference(contradiction_clause,[status(thm)],[f313])).
% 0.15/0.50 fof(f315,plain,(
% 0.15/0.50 $false|~sQ0_spl),
% 0.15/0.50 inference(forward_subsumption_resolution,[status(thm)],[f270,f74])).
% 0.15/0.50 fof(f316,plain,(
% 0.15/0.50 ~sQ0_spl),
% 0.15/0.50 inference(contradiction_clause,[status(thm)],[f315])).
% 0.15/0.50 fof(f330,definition,(
% 0.15/0.50 sQ14_spl <=> (v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f332,plain,(
% 0.15/0.50 ~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|sQ14_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f330])).
% 0.15/0.50 fof(f345,plain,(
% 0.15/0.50 v3_struct_0(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|v3_struct_0(sK1_skl)|~v3_group_1(sK1_skl)|~v4_group_1(sK1_skl)|~l1_group_1(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v1_group_6(sK2_skl,sK0_skl,sK1_skl)|m4_vectsp_8(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),k11_group_4(sK0_skl),k11_group_4(sK1_skl))),
% 0.15/0.50 inference(resolution,[status(thm)],[f245,f81])).
% 0.15/0.50 fof(f346,definition,(
% 0.15/0.50 sQ18_spl <=> (v4_group_1(sK0_skl))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f348,plain,(
% 0.15/0.50 ~v4_group_1(sK0_skl)|sQ18_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f346])).
% 0.15/0.50 fof(f349,definition,(
% 0.15/0.50 sQ19_spl <=> (v4_group_1(sK1_skl))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f351,plain,(
% 0.15/0.50 ~v4_group_1(sK1_skl)|sQ19_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f349])).
% 0.15/0.50 fof(f352,definition,(
% 0.15/0.50 sQ20_spl <=> (v1_funct_1(sK2_skl))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f354,plain,(
% 0.15/0.50 ~v1_funct_1(sK2_skl)|sQ20_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f352])).
% 0.15/0.50 fof(f355,definition,(
% 0.15/0.50 sQ21_spl <=> (v1_group_6(sK2_skl,sK0_skl,sK1_skl))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f357,plain,(
% 0.15/0.50 ~v1_group_6(sK2_skl,sK0_skl,sK1_skl)|sQ21_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f355])).
% 0.15/0.50 fof(f358,definition,(
% 0.15/0.50 sQ22_spl <=> (m4_vectsp_8(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),k11_group_4(sK0_skl),k11_group_4(sK1_skl)))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f361,plain,(
% 0.15/0.50 sQ4_spl|~sQ5_spl|~sQ18_spl|~sQ6_spl|sQ0_spl|~sQ1_spl|~sQ19_spl|~sQ2_spl|~sQ20_spl|~sQ14_spl|~sQ21_spl|sQ22_spl),
% 0.15/0.50 inference(split_clause,[status(thm)],[f345,f282,f285,f346,f288,f269,f272,f349,f275,f352,f330,f355,f358])).
% 0.15/0.50 fof(f362,plain,(
% 0.15/0.50 $false|sQ14_spl),
% 0.15/0.50 inference(forward_subsumption_resolution,[status(thm)],[f332,f79])).
% 0.15/0.50 fof(f363,plain,(
% 0.15/0.50 sQ14_spl),
% 0.15/0.50 inference(contradiction_clause,[status(thm)],[f362])).
% 0.15/0.50 fof(f364,plain,(
% 0.15/0.50 v3_struct_0(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|v3_struct_0(sK1_skl)|~v3_group_1(sK1_skl)|~v4_group_1(sK1_skl)|~l1_group_1(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|~v1_group_6(sK2_skl,sK0_skl,sK1_skl)|~v2_funct_1(sK2_skl)|m3_vectsp_8(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),k11_group_4(sK0_skl),k11_group_4(sK1_skl))),
% 0.15/0.50 inference(resolution,[status(thm)],[f243,f81])).
% 0.15/0.50 fof(f365,definition,(
% 0.15/0.50 sQ23_spl <=> (v2_funct_1(sK2_skl))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f367,plain,(
% 0.15/0.50 ~v2_funct_1(sK2_skl)|sQ23_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f365])).
% 0.15/0.50 fof(f368,definition,(
% 0.15/0.50 sQ24_spl <=> (m3_vectsp_8(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),k11_group_4(sK0_skl),k11_group_4(sK1_skl)))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f371,plain,(
% 0.15/0.50 sQ4_spl|~sQ5_spl|~sQ18_spl|~sQ6_spl|sQ0_spl|~sQ1_spl|~sQ19_spl|~sQ2_spl|~sQ20_spl|~sQ14_spl|~sQ21_spl|~sQ23_spl|sQ24_spl),
% 0.15/0.50 inference(split_clause,[status(thm)],[f364,f282,f285,f346,f288,f269,f272,f349,f275,f352,f330,f355,f365,f368])).
% 0.15/0.50 fof(f372,plain,(
% 0.15/0.50 $false|sQ21_spl),
% 0.15/0.50 inference(forward_subsumption_resolution,[status(thm)],[f357,f80])).
% 0.15/0.50 fof(f373,plain,(
% 0.15/0.50 sQ21_spl),
% 0.15/0.50 inference(contradiction_clause,[status(thm)],[f372])).
% 0.15/0.50 fof(f374,plain,(
% 0.15/0.50 $false|sQ20_spl),
% 0.15/0.50 inference(forward_subsumption_resolution,[status(thm)],[f354,f78])).
% 0.15/0.50 fof(f375,plain,(
% 0.15/0.50 sQ20_spl),
% 0.15/0.50 inference(contradiction_clause,[status(thm)],[f374])).
% 0.15/0.50 fof(f376,plain,(
% 0.15/0.50 $false|sQ19_spl),
% 0.15/0.50 inference(forward_subsumption_resolution,[status(thm)],[f351,f76])).
% 0.15/0.50 fof(f377,plain,(
% 0.15/0.50 sQ19_spl),
% 0.15/0.50 inference(contradiction_clause,[status(thm)],[f376])).
% 0.15/0.50 fof(f378,plain,(
% 0.15/0.50 $false|sQ18_spl),
% 0.15/0.50 inference(forward_subsumption_resolution,[status(thm)],[f348,f72])).
% 0.15/0.50 fof(f379,plain,(
% 0.15/0.50 sQ18_spl),
% 0.15/0.50 inference(contradiction_clause,[status(thm)],[f378])).
% 0.15/0.50 fof(f380,plain,(
% 0.15/0.50 $false|sQ23_spl),
% 0.15/0.50 inference(forward_subsumption_resolution,[status(thm)],[f367,f82])).
% 0.15/0.50 fof(f381,plain,(
% 0.15/0.50 sQ23_spl),
% 0.15/0.50 inference(contradiction_clause,[status(thm)],[f380])).
% 0.15/0.50 fof(f489,definition,(
% 0.15/0.50 sQ45_spl <=> (v3_struct_0(k11_group_4(sK0_skl)))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f490,plain,(
% 0.15/0.50 v3_struct_0(k11_group_4(sK0_skl))|~sQ45_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f489])).
% 0.15/0.50 fof(f507,definition,(
% 0.15/0.50 sQ49_spl <=> (v3_struct_0(k11_group_4(sK1_skl)))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f508,plain,(
% 0.15/0.50 v3_struct_0(k11_group_4(sK1_skl))|~sQ49_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f507])).
% 0.15/0.50 fof(f525,definition,(
% 0.15/0.50 sQ53_spl <=> (m2_relset_1(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(k11_group_4(sK0_skl)),u1_struct_0(k11_group_4(sK1_skl))))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f526,plain,(
% 0.15/0.50 m2_relset_1(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(k11_group_4(sK0_skl)),u1_struct_0(k11_group_4(sK1_skl)))|~sQ53_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f525])).
% 0.15/0.50 fof(f529,definition,(
% 0.15/0.50 sQ54_spl <=> (v1_funct_2(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(k11_group_4(sK0_skl)),u1_struct_0(k11_group_4(sK1_skl))))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f543,plain,(
% 0.15/0.50 m1_relset_1(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))),
% 0.15/0.50 inference(resolution,[status(thm)],[f229,f81])).
% 0.15/0.50 fof(f563,plain,(
% 0.15/0.50 v3_struct_0(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|v3_struct_0(sK1_skl)|~v3_group_1(sK1_skl)|~v4_group_1(sK1_skl)|~l1_group_1(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|m2_relset_1(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(k11_group_4(sK0_skl)),u1_struct_0(k11_group_4(sK1_skl)))),
% 0.15/0.50 inference(resolution,[status(thm)],[f543,f115])).
% 0.15/0.50 fof(f564,plain,(
% 0.15/0.50 v3_struct_0(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|v3_struct_0(sK1_skl)|~v3_group_1(sK1_skl)|~v4_group_1(sK1_skl)|~l1_group_1(sK1_skl)|~v1_funct_1(sK2_skl)|~v1_funct_2(sK2_skl,u1_struct_0(sK0_skl),u1_struct_0(sK1_skl))|v1_funct_2(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(k11_group_4(sK0_skl)),u1_struct_0(k11_group_4(sK1_skl)))),
% 0.15/0.50 inference(resolution,[status(thm)],[f543,f114])).
% 0.15/0.50 fof(f568,plain,(
% 0.15/0.50 sQ4_spl|~sQ5_spl|~sQ18_spl|~sQ6_spl|sQ0_spl|~sQ1_spl|~sQ19_spl|~sQ2_spl|~sQ20_spl|~sQ14_spl|sQ53_spl),
% 0.15/0.50 inference(split_clause,[status(thm)],[f563,f282,f285,f346,f288,f269,f272,f349,f275,f352,f330,f525])).
% 0.15/0.50 fof(f569,plain,(
% 0.15/0.50 sQ4_spl|~sQ5_spl|~sQ18_spl|~sQ6_spl|sQ0_spl|~sQ1_spl|~sQ19_spl|~sQ2_spl|~sQ20_spl|~sQ14_spl|sQ54_spl),
% 0.15/0.50 inference(split_clause,[status(thm)],[f564,f282,f285,f346,f288,f269,f272,f349,f275,f352,f330,f529])).
% 0.15/0.50 fof(f585,plain,(
% 0.15/0.50 v3_struct_0(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~sQ45_spl),
% 0.15/0.50 inference(resolution,[status(thm)],[f490,f108])).
% 0.15/0.50 fof(f586,plain,(
% 0.15/0.50 sQ4_spl|~sQ5_spl|~sQ18_spl|~sQ6_spl|~sQ45_spl),
% 0.15/0.50 inference(split_clause,[status(thm)],[f585,f282,f285,f346,f288,f489])).
% 0.15/0.50 fof(f617,plain,(
% 0.15/0.50 v3_struct_0(sK1_skl)|~v3_group_1(sK1_skl)|~v4_group_1(sK1_skl)|~l1_group_1(sK1_skl)|~sQ49_spl),
% 0.15/0.50 inference(resolution,[status(thm)],[f508,f108])).
% 0.15/0.50 fof(f618,plain,(
% 0.15/0.50 sQ0_spl|~sQ1_spl|~sQ19_spl|~sQ2_spl|~sQ49_spl),
% 0.15/0.50 inference(split_clause,[status(thm)],[f617,f269,f272,f349,f275,f507])).
% 0.15/0.50 fof(f694,plain,(
% 0.15/0.50 v3_struct_0(k11_group_4(sK0_skl))|~v10_lattices(k11_group_4(sK0_skl))|~l3_lattices(k11_group_4(sK0_skl))|v3_struct_0(k11_group_4(sK1_skl))|~v10_lattices(k11_group_4(sK1_skl))|~l3_lattices(k11_group_4(sK1_skl))|~v1_funct_2(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),u1_struct_0(k11_group_4(sK0_skl)),u1_struct_0(k11_group_4(sK1_skl)))|m1_lattice4(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),k11_group_4(sK0_skl),k11_group_4(sK1_skl))|~m4_vectsp_8(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),k11_group_4(sK0_skl),k11_group_4(sK1_skl))|~m3_vectsp_8(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),k11_group_4(sK0_skl),k11_group_4(sK1_skl))|~sQ53_spl),
% 0.15/0.50 inference(resolution,[status(thm)],[f526,f266])).
% 0.15/0.50 fof(f700,definition,(
% 0.15/0.50 sQ85_spl <=> (m1_lattice4(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),k11_group_4(sK0_skl),k11_group_4(sK1_skl)))),
% 0.15/0.50 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.15/0.50 fof(f701,plain,(
% 0.15/0.50 m1_lattice4(k3_latsubgr(sK0_skl,sK1_skl,sK2_skl),k11_group_4(sK0_skl),k11_group_4(sK1_skl))|~sQ85_spl),
% 0.15/0.50 inference(component_clause,[status(thm)],[f700])).
% 0.15/0.50 fof(f703,plain,(
% 0.15/0.50 sQ45_spl|~sQ7_spl|~sQ9_spl|sQ49_spl|~sQ3_spl|~sQ8_spl|~sQ54_spl|sQ85_spl|~sQ22_spl|~sQ24_spl|~sQ53_spl),
% 0.15/0.50 inference(split_clause,[status(thm)],[f694,f489,f291,f307,f507,f278,f303,f529,f700,f358,f368,f525])).
% 0.15/0.50 fof(f738,plain,(
% 0.15/0.50 $false|~sQ85_spl),
% 0.15/0.50 inference(forward_subsumption_resolution,[status(thm)],[f701,f83])).
% 0.15/0.50 fof(f739,plain,(
% 0.15/0.50 ~sQ85_spl),
% 0.15/0.50 inference(contradiction_clause,[status(thm)],[f738])).
% 0.15/0.50 fof(f740,plain,(
% 0.15/0.50 $false),
% 0.15/0.50 inference(sat_refutation,[status(thm)],[f281,f294,f296,f298,f300,f306,f310,f312,f314,f316,f361,f363,f371,f373,f375,f377,f379,f381,f568,f569,f586,f618,f703,f739])).
% 0.15/0.50 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/0.52 % Elapsed time: 0.084943 seconds
% 0.15/0.52 % CPU time: 0.330587 seconds
% 0.15/0.52 % Total memory used: 75.781 MB
% 0.15/0.52 % Net memory used: 75.660 MB
%------------------------------------------------------------------------------