%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP642+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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:01 PM UTC 2026
% Result : Theorem 0.08s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP642+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n001.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sun Sep 20 20:31:00 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.38 % Drodi V4.1.1
% 0.08/0.41 % Refutation found
% 0.08/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.08/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.08/0.41 fof(f1,conjecture,(
% 0.08/0.41 (! [A] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( ( v1_group_1(B)& m1_group_2(B,A) )=> k1_funct_1(k1_latsubgr(A),B) != k1_xboole_0 ) )) )),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f2,negated_conjecture,(
% 0.08/0.41 ~((! [A] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( ( v1_group_1(B)& m1_group_2(B,A) )=> k1_funct_1(k1_latsubgr(A),B) != k1_xboole_0 ) )) ))),
% 0.08/0.41 inference(negated_conjecture,[status(cth)],[f1])).
% 0.08/0.41 fof(f9,axiom,(
% 0.08/0.41 (! [A] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( ( v1_funct_1(B)& v1_funct_2(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))& m2_relset_1(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A))) )=> ( B = k1_latsubgr(A)<=> (! [C] :( ( v1_group_1(C)& m1_group_2(C,A) )=> k1_funct_1(B,C) = u1_struct_0(C) ) )) ) )) )),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f13,axiom,(
% 0.08/0.41 (! [A] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> ( v1_funct_1(k1_latsubgr(A))& v1_funct_2(k1_latsubgr(A),k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))& m2_relset_1(k1_latsubgr(A),k1_group_3(A),k1_zfmisc_1(u1_struct_0(A))) ) ) )),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f17,axiom,(
% 0.08/0.41 (! [A] :( l1_group_1(A)=> l1_struct_0(A) ) )),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f19,axiom,(
% 0.08/0.41 (! [A] :( ( ~ v3_struct_0(A)& v3_group_1(A)& l1_group_1(A) )=> (! [B] :( m1_group_2(B,A)=> ( ~ v3_struct_0(B)& v3_group_1(B)& l1_group_1(B) ) ) )) )),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f32,axiom,(
% 0.08/0.41 (! [A] :( ( ~ v3_struct_0(A)& l1_struct_0(A) )=> ~ v1_xboole_0(u1_struct_0(A)) ) )),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f39,axiom,(
% 0.08/0.41 (? [A] : v1_xboole_0(A) )),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f52,axiom,(
% 0.08/0.41 (! [A] :( v1_xboole_0(A)=> A = k1_xboole_0 ) )),
% 0.08/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.41 fof(f55,plain,(
% 0.08/0.41 (?[A]: ((((~v3_struct_0(A)&v3_group_1(A))&v4_group_1(A))&l1_group_1(A))&(?[B]: ((v1_group_1(B)&m1_group_2(B,A))&k1_funct_1(k1_latsubgr(A),B)=k1_xboole_0))))),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.08/0.41 fof(f56,plain,(
% 0.08/0.41 ((((~v3_struct_0(sK0_skl)&v3_group_1(sK0_skl))&v4_group_1(sK0_skl))&l1_group_1(sK0_skl))&((v1_group_1(sK1_skl)&m1_group_2(sK1_skl,sK0_skl))&k1_funct_1(k1_latsubgr(sK0_skl),sK1_skl)=k1_xboole_0))),
% 0.08/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl)],[f55])).
% 0.08/0.41 fof(f57,plain,(
% 0.08/0.41 ~v3_struct_0(sK0_skl)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f56])).
% 0.08/0.41 fof(f58,plain,(
% 0.08/0.41 v3_group_1(sK0_skl)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f56])).
% 0.08/0.41 fof(f59,plain,(
% 0.08/0.41 v4_group_1(sK0_skl)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f56])).
% 0.08/0.41 fof(f60,plain,(
% 0.08/0.41 l1_group_1(sK0_skl)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f56])).
% 0.08/0.41 fof(f61,plain,(
% 0.08/0.41 v1_group_1(sK1_skl)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f56])).
% 0.08/0.41 fof(f62,plain,(
% 0.08/0.41 m1_group_2(sK1_skl,sK0_skl)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f56])).
% 0.08/0.41 fof(f63,plain,(
% 0.08/0.41 k1_funct_1(k1_latsubgr(sK0_skl),sK1_skl)=k1_xboole_0),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f56])).
% 0.08/0.41 fof(f84,plain,(
% 0.08/0.41 ![A]: ((((v3_struct_0(A)|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|(![B]: (((~v1_funct_1(B)|~v1_funct_2(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A))))|~m2_relset_1(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A))))|(B=k1_latsubgr(A)<=>(![C]: ((~v1_group_1(C)|~m1_group_2(C,A))|k1_funct_1(B,C)=u1_struct_0(C)))))))),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.08/0.41 fof(f85,plain,(
% 0.08/0.41 ![A]: ((((v3_struct_0(A)|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|(![B]: (((~v1_funct_1(B)|~v1_funct_2(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A))))|~m2_relset_1(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A))))|((~B=k1_latsubgr(A)|(![C]: ((~v1_group_1(C)|~m1_group_2(C,A))|k1_funct_1(B,C)=u1_struct_0(C))))&(B=k1_latsubgr(A)|(?[C]: ((v1_group_1(C)&m1_group_2(C,A))&~k1_funct_1(B,C)=u1_struct_0(C))))))))),
% 0.08/0.41 inference(NNF_transformation,[status(thm)],[f84])).
% 0.08/0.41 fof(f86,plain,(
% 0.08/0.41 ![A]: ((((v3_struct_0(A)|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|(![B]: (((~v1_funct_1(B)|~v1_funct_2(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A))))|~m2_relset_1(B,k1_group_3(A),k1_zfmisc_1(u1_struct_0(A))))|((~B=k1_latsubgr(A)|(![C]: ((~v1_group_1(C)|~m1_group_2(C,A))|k1_funct_1(B,C)=u1_struct_0(C))))&(B=k1_latsubgr(A)|((v1_group_1(sK2_skl(B,A))&m1_group_2(sK2_skl(B,A),A))&~k1_funct_1(B,sK2_skl(B,A))=u1_struct_0(sK2_skl(B,A))))))))),
% 0.08/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(C,sK2_skl(B,A))],[f85])).
% 0.08/0.41 fof(f87,plain,(
% 0.08/0.41 ![X0,X1,X2]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~v1_funct_1(X1)|~v1_funct_2(X1,k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))|~m2_relset_1(X1,k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))|~X1=k1_latsubgr(X0)|~v1_group_1(X2)|~m1_group_2(X2,X0)|k1_funct_1(X1,X2)=u1_struct_0(X2))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f86])).
% 0.08/0.41 fof(f94,plain,(
% 0.08/0.41 ![A]: ((((v3_struct_0(A)|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|((v1_funct_1(k1_latsubgr(A))&v1_funct_2(k1_latsubgr(A),k1_group_3(A),k1_zfmisc_1(u1_struct_0(A))))&m2_relset_1(k1_latsubgr(A),k1_group_3(A),k1_zfmisc_1(u1_struct_0(A)))))),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.08/0.41 fof(f95,plain,(
% 0.08/0.41 ![X0]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|v1_funct_1(k1_latsubgr(X0)))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f94])).
% 0.08/0.41 fof(f96,plain,(
% 0.08/0.41 ![X0]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|v1_funct_2(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0))))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f94])).
% 0.08/0.41 fof(f97,plain,(
% 0.08/0.41 ![X0]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|m2_relset_1(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0))))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f94])).
% 0.08/0.41 fof(f98,plain,(
% 0.08/0.41 ![A]: (~l1_group_1(A)|l1_struct_0(A))),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 0.08/0.41 fof(f99,plain,(
% 0.08/0.41 ![X0]: (~l1_group_1(X0)|l1_struct_0(X0))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f98])).
% 0.08/0.41 fof(f100,plain,(
% 0.08/0.41 ![A]: (((v3_struct_0(A)|~v3_group_1(A))|~l1_group_1(A))|(![B]: (~m1_group_2(B,A)|((~v3_struct_0(B)&v3_group_1(B))&l1_group_1(B)))))),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.08/0.41 fof(f101,plain,(
% 0.08/0.41 ![X0,X1]: (v3_struct_0(X0)|~v3_group_1(X0)|~l1_group_1(X0)|~m1_group_2(X1,X0)|~v3_struct_0(X1))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f100])).
% 0.08/0.41 fof(f103,plain,(
% 0.08/0.41 ![X0,X1]: (v3_struct_0(X0)|~v3_group_1(X0)|~l1_group_1(X0)|~m1_group_2(X1,X0)|l1_group_1(X1))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f100])).
% 0.08/0.41 fof(f125,plain,(
% 0.08/0.41 ![A]: ((v3_struct_0(A)|~l1_struct_0(A))|~v1_xboole_0(u1_struct_0(A)))),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 0.08/0.41 fof(f126,plain,(
% 0.08/0.41 ![X0]: (v3_struct_0(X0)|~l1_struct_0(X0)|~v1_xboole_0(u1_struct_0(X0)))),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f125])).
% 0.08/0.41 fof(f143,plain,(
% 0.08/0.41 v1_xboole_0(sK11_skl)),
% 0.08/0.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(A,sK11_skl)],[f39])).
% 0.08/0.41 fof(f144,plain,(
% 0.08/0.41 v1_xboole_0(sK11_skl)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f143])).
% 0.08/0.41 fof(f181,plain,(
% 0.08/0.41 ![A]: (~v1_xboole_0(A)|A=k1_xboole_0)),
% 0.08/0.41 inference(pre_NNF_transformation,[status(thm)],[f52])).
% 0.08/0.41 fof(f182,plain,(
% 0.08/0.41 ![X0]: (~v1_xboole_0(X0)|X0=k1_xboole_0)),
% 0.08/0.41 inference(cnf_transformation,[status(thm)],[f181])).
% 0.08/0.41 fof(f189,plain,(
% 0.08/0.41 ![X0,X1]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~v1_funct_1(k1_latsubgr(X0))|~v1_funct_2(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))|~m2_relset_1(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))|~v1_group_1(X1)|~m1_group_2(X1,X0)|k1_funct_1(k1_latsubgr(X0),X1)=u1_struct_0(X1))),
% 0.08/0.41 inference(destructive_equality_resolution,[status(thm)],[f87])).
% 0.08/0.41 fof(f191,plain,(
% 0.08/0.41 v3_struct_0(sK0_skl)|~v3_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~v3_struct_0(sK1_skl)),
% 0.08/0.41 inference(resolution,[status(thm)],[f101,f62])).
% 0.08/0.41 fof(f192,definition,(
% 0.08/0.41 sQ0_spl <=> (v3_struct_0(sK0_skl))),
% 0.08/0.41 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.08/0.41 fof(f193,plain,(
% 0.08/0.41 v3_struct_0(sK0_skl)|~sQ0_spl),
% 0.08/0.41 inference(component_clause,[status(thm)],[f192])).
% 0.08/0.41 fof(f195,definition,(
% 0.08/0.41 sQ1_spl <=> (v3_group_1(sK0_skl))),
% 0.08/0.41 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.08/0.41 fof(f197,plain,(
% 0.08/0.41 ~v3_group_1(sK0_skl)|sQ1_spl),
% 0.08/0.41 inference(component_clause,[status(thm)],[f195])).
% 0.08/0.41 fof(f198,definition,(
% 0.08/0.41 sQ2_spl <=> (l1_group_1(sK0_skl))),
% 0.08/0.41 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.08/0.41 fof(f200,plain,(
% 0.08/0.41 ~l1_group_1(sK0_skl)|sQ2_spl),
% 0.08/0.41 inference(component_clause,[status(thm)],[f198])).
% 0.08/0.41 fof(f201,definition,(
% 0.08/0.41 sQ3_spl <=> (v3_struct_0(sK1_skl))),
% 0.08/0.41 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.08/0.41 fof(f204,plain,(
% 0.08/0.41 sQ0_spl|~sQ1_spl|~sQ2_spl|~sQ3_spl),
% 0.08/0.41 inference(split_clause,[status(thm)],[f191,f192,f195,f198,f201])).
% 0.08/0.41 fof(f210,plain,(
% 0.08/0.41 $false|sQ2_spl),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f200,f60])).
% 0.08/0.41 fof(f211,plain,(
% 0.08/0.41 sQ2_spl),
% 0.08/0.41 inference(contradiction_clause,[status(thm)],[f210])).
% 0.08/0.41 fof(f212,plain,(
% 0.08/0.41 $false|sQ1_spl),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f197,f58])).
% 0.08/0.41 fof(f213,plain,(
% 0.08/0.41 sQ1_spl),
% 0.08/0.41 inference(contradiction_clause,[status(thm)],[f212])).
% 0.08/0.41 fof(f214,plain,(
% 0.08/0.41 $false|~sQ0_spl),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f193,f57])).
% 0.08/0.41 fof(f215,plain,(
% 0.08/0.41 ~sQ0_spl),
% 0.08/0.41 inference(contradiction_clause,[status(thm)],[f214])).
% 0.08/0.41 fof(f216,plain,(
% 0.08/0.41 v3_struct_0(sK0_skl)|~v3_group_1(sK0_skl)|~l1_group_1(sK0_skl)|l1_group_1(sK1_skl)),
% 0.08/0.41 inference(resolution,[status(thm)],[f103,f62])).
% 0.08/0.41 fof(f217,definition,(
% 0.08/0.41 sQ5_spl <=> (l1_group_1(sK1_skl))),
% 0.08/0.41 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.08/0.41 fof(f218,plain,(
% 0.08/0.41 l1_group_1(sK1_skl)|~sQ5_spl),
% 0.08/0.41 inference(component_clause,[status(thm)],[f217])).
% 0.08/0.41 fof(f220,plain,(
% 0.08/0.41 sQ0_spl|~sQ1_spl|~sQ2_spl|sQ5_spl),
% 0.08/0.41 inference(split_clause,[status(thm)],[f216,f192,f195,f198,f217])).
% 0.08/0.41 fof(f221,plain,(
% 0.08/0.41 sK11_skl=k1_xboole_0),
% 0.08/0.41 inference(resolution,[status(thm)],[f144,f182])).
% 0.08/0.41 fof(f222,plain,(
% 0.08/0.41 k1_funct_1(k1_latsubgr(sK0_skl),sK1_skl)=sK11_skl),
% 0.08/0.41 inference(backward_demodulation,[status(thm)],[f221,f63])).
% 0.08/0.41 fof(f226,plain,(
% 0.08/0.41 l1_struct_0(sK1_skl)|~sQ5_spl),
% 0.08/0.41 inference(resolution,[status(thm)],[f99,f218])).
% 0.08/0.41 fof(f238,definition,(
% 0.08/0.41 sQ8_spl <=> (v1_group_1(sK1_skl))),
% 0.08/0.41 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.08/0.41 fof(f240,plain,(
% 0.08/0.41 ~v1_group_1(sK1_skl)|sQ8_spl),
% 0.08/0.41 inference(component_clause,[status(thm)],[f238])).
% 0.08/0.41 fof(f252,plain,(
% 0.08/0.41 $false|sQ8_spl),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f240,f61])).
% 0.08/0.41 fof(f253,plain,(
% 0.08/0.41 sQ8_spl),
% 0.08/0.41 inference(contradiction_clause,[status(thm)],[f252])).
% 0.08/0.41 fof(f257,plain,(
% 0.08/0.41 ![X0,X1]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~v1_funct_2(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))|~m2_relset_1(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))|~v1_group_1(X1)|~m1_group_2(X1,X0)|k1_funct_1(k1_latsubgr(X0),X1)=u1_struct_0(X1))),
% 0.08/0.41 inference(backward_subsumption_resolution,[status(thm)],[f189,f95])).
% 0.08/0.41 fof(f267,definition,(
% 0.08/0.41 sQ14_spl <=> (v4_group_1(sK0_skl))),
% 0.08/0.41 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.08/0.41 fof(f269,plain,(
% 0.08/0.41 ~v4_group_1(sK0_skl)|sQ14_spl),
% 0.08/0.41 inference(component_clause,[status(thm)],[f267])).
% 0.08/0.41 fof(f274,plain,(
% 0.08/0.41 $false|sQ14_spl),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f269,f59])).
% 0.08/0.41 fof(f275,plain,(
% 0.08/0.41 sQ14_spl),
% 0.08/0.41 inference(contradiction_clause,[status(thm)],[f274])).
% 0.08/0.41 fof(f287,plain,(
% 0.08/0.41 v3_struct_0(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|m2_relset_1(k1_latsubgr(sK0_skl),k1_group_3(sK0_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))),
% 0.08/0.41 inference(resolution,[status(thm)],[f97,f58])).
% 0.08/0.41 fof(f292,definition,(
% 0.08/0.41 sQ19_spl <=> (m2_relset_1(k1_latsubgr(sK0_skl),k1_group_3(sK0_skl),k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 0.08/0.41 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.08/0.41 fof(f293,plain,(
% 0.08/0.41 m2_relset_1(k1_latsubgr(sK0_skl),k1_group_3(sK0_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ19_spl),
% 0.08/0.41 inference(component_clause,[status(thm)],[f292])).
% 0.08/0.41 fof(f295,plain,(
% 0.08/0.41 sQ0_spl|~sQ14_spl|~sQ2_spl|sQ19_spl),
% 0.08/0.41 inference(split_clause,[status(thm)],[f287,f192,f267,f198,f292])).
% 0.08/0.41 fof(f296,plain,(
% 0.08/0.41 ![X0,X1]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m2_relset_1(k1_latsubgr(X0),k1_group_3(X0),k1_zfmisc_1(u1_struct_0(X0)))|~v1_group_1(X1)|~m1_group_2(X1,X0)|k1_funct_1(k1_latsubgr(X0),X1)=u1_struct_0(X1))),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f257,f96])).
% 0.08/0.41 fof(f297,plain,(
% 0.08/0.41 ![X0]: (v3_struct_0(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~v1_group_1(X0)|~m1_group_2(X0,sK0_skl)|k1_funct_1(k1_latsubgr(sK0_skl),X0)=u1_struct_0(X0)|~sQ19_spl)),
% 0.08/0.41 inference(resolution,[status(thm)],[f296,f293])).
% 0.08/0.41 fof(f298,definition,(
% 0.08/0.41 ![X0]: (sQ20_spl <=> (~v1_group_1(X0)|~m1_group_2(X0,sK0_skl)|k1_funct_1(k1_latsubgr(sK0_skl),X0)=u1_struct_0(X0)))),
% 0.08/0.41 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.08/0.41 fof(f299,plain,(
% 0.08/0.41 ![X0]: (~v1_group_1(X0)|~m1_group_2(X0,sK0_skl)|k1_funct_1(k1_latsubgr(sK0_skl),X0)=u1_struct_0(X0)|~sQ20_spl)),
% 0.08/0.41 inference(component_clause,[status(thm)],[f298])).
% 0.08/0.41 fof(f301,plain,(
% 0.08/0.41 sQ0_spl|~sQ1_spl|~sQ14_spl|~sQ2_spl|sQ20_spl|~sQ19_spl),
% 0.08/0.41 inference(split_clause,[status(thm)],[f297,f192,f195,f267,f198,f298,f292])).
% 0.08/0.41 fof(f302,plain,(
% 0.08/0.41 ~v1_group_1(sK1_skl)|k1_funct_1(k1_latsubgr(sK0_skl),sK1_skl)=u1_struct_0(sK1_skl)|~sQ20_spl),
% 0.08/0.41 inference(resolution,[status(thm)],[f299,f62])).
% 0.08/0.41 fof(f303,definition,(
% 0.08/0.41 sQ21_spl <=> (k1_funct_1(k1_latsubgr(sK0_skl),sK1_skl)=u1_struct_0(sK1_skl))),
% 0.08/0.41 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.08/0.41 fof(f304,plain,(
% 0.08/0.41 k1_funct_1(k1_latsubgr(sK0_skl),sK1_skl)=u1_struct_0(sK1_skl)|~sQ21_spl),
% 0.08/0.41 inference(component_clause,[status(thm)],[f303])).
% 0.08/0.41 fof(f306,plain,(
% 0.08/0.41 ~sQ8_spl|sQ21_spl|~sQ20_spl),
% 0.08/0.41 inference(split_clause,[status(thm)],[f302,f238,f303,f298])).
% 0.08/0.41 fof(f307,plain,(
% 0.08/0.41 sK11_skl=u1_struct_0(sK1_skl)|~sQ21_spl),
% 0.08/0.41 inference(forward_demodulation,[status(thm)],[f222,f304])).
% 0.08/0.41 fof(f405,plain,(
% 0.08/0.41 v3_struct_0(sK1_skl)|~l1_struct_0(sK1_skl)|~v1_xboole_0(sK11_skl)|~sQ21_spl),
% 0.08/0.41 inference(paramodulation,[status(thm)],[f307,f126])).
% 0.08/0.41 fof(f406,definition,(
% 0.08/0.41 sQ31_spl <=> (l1_struct_0(sK1_skl))),
% 0.08/0.41 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.08/0.41 fof(f408,plain,(
% 0.08/0.41 ~l1_struct_0(sK1_skl)|sQ31_spl),
% 0.08/0.41 inference(component_clause,[status(thm)],[f406])).
% 0.08/0.41 fof(f409,definition,(
% 0.08/0.41 sQ32_spl <=> (v1_xboole_0(sK11_skl))),
% 0.08/0.41 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.08/0.41 fof(f411,plain,(
% 0.08/0.41 ~v1_xboole_0(sK11_skl)|sQ32_spl),
% 0.08/0.41 inference(component_clause,[status(thm)],[f409])).
% 0.08/0.41 fof(f412,plain,(
% 0.08/0.41 sQ3_spl|~sQ31_spl|~sQ32_spl|~sQ21_spl),
% 0.08/0.41 inference(split_clause,[status(thm)],[f405,f201,f406,f409,f303])).
% 0.08/0.41 fof(f413,plain,(
% 0.08/0.41 $false|~sQ5_spl|sQ31_spl),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f408,f226])).
% 0.08/0.41 fof(f414,plain,(
% 0.08/0.41 ~sQ5_spl|sQ31_spl),
% 0.08/0.41 inference(contradiction_clause,[status(thm)],[f413])).
% 0.08/0.41 fof(f415,plain,(
% 0.08/0.41 $false|sQ32_spl),
% 0.08/0.41 inference(forward_subsumption_resolution,[status(thm)],[f411,f144])).
% 0.08/0.41 fof(f416,plain,(
% 0.08/0.41 sQ32_spl),
% 0.08/0.41 inference(contradiction_clause,[status(thm)],[f415])).
% 0.08/0.41 fof(f417,plain,(
% 0.08/0.41 $false),
% 0.08/0.41 inference(sat_refutation,[status(thm)],[f204,f211,f213,f215,f220,f253,f275,f295,f301,f306,f412,f414,f416])).
% 0.08/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.08/0.44 % Elapsed time: 0.057998 seconds
% 0.08/0.44 % CPU time: 0.171496 seconds
% 0.08/0.44 % Total memory used: 105.144 MB
% 0.08/0.44 % Net memory used: 105.085 MB
%------------------------------------------------------------------------------