%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP641+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 : n011.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:00 PM UTC 2026
% Result : Theorem 0.09s 0.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP641+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.09/0.51 % Computer : n011.cluster.edu
% 0.09/0.51 % Model : x86_64 x86_64
% 0.09/0.51 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.51 % Memory : 8046.5625MB
% 0.09/0.51 % OS : Linux 6.8.0-71-generic
% 0.09/0.51 % CPULimit : 300
% 0.09/0.51 % WCLimit : 300
% 0.09/0.51 % DateTime : Sun Sep 20 20:24:55 UTC 2026
% 0.09/0.51 % CPUTime :
% 0.09/0.52 % Drodi V4.1.1
% 0.09/0.56 % Refutation found
% 0.09/0.56 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.56 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.56 fof(f1,conjecture,(
% 0.09/0.56 (! [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) )=> r2_hidden(k2_group_1(A),k1_funct_1(k1_latsubgr(A),B)) ) )) )),
% 0.09/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.56 fof(f2,negated_conjecture,(
% 0.09/0.56 ~((! [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) )=> r2_hidden(k2_group_1(A),k1_funct_1(k1_latsubgr(A),B)) ) )) ))),
% 0.09/0.56 inference(negated_conjecture,[status(cth)],[f1])).
% 0.09/0.56 fof(f9,axiom,(
% 0.09/0.56 (! [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.09/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.56 fof(f13,axiom,(
% 0.09/0.56 (! [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.09/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.56 fof(f16,axiom,(
% 0.09/0.56 (! [A] :( ( ~ v3_struct_0(A)& l1_group_1(A) )=> m1_subset_1(k2_group_1(A),u1_struct_0(A)) ) )),
% 0.09/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.56 fof(f18,axiom,(
% 0.09/0.56 (! [A] :( l1_group_1(A)=> l1_struct_0(A) ) )),
% 0.09/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.56 fof(f20,axiom,(
% 0.09/0.56 (! [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.09/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.56 fof(f24,axiom,(
% 0.09/0.56 (! [A] :( l1_group_1(A)=> ( v1_funct_1(u1_group_1(A))& v1_funct_2(u1_group_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))& m2_relset_1(u1_group_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) ) ) )),
% 0.09/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.56 fof(f26,axiom,(
% 0.09/0.56 (? [A] : l1_group_1(A) )),
% 0.09/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.56 fof(f33,axiom,(
% 0.09/0.56 (! [A] :( ( ~ v3_struct_0(A)& l1_struct_0(A) )=> ~ v1_xboole_0(u1_struct_0(A)) ) )),
% 0.09/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.56 fof(f34,axiom,(
% 0.09/0.56 (! [A] : ~ v1_xboole_0(k1_zfmisc_1(A)) )),
% 0.09/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.56 fof(f46,axiom,(
% 0.09/0.56 (! [A,B,C] :( m2_relset_1(C,A,B)<=> m1_relset_1(C,A,B) ) )),
% 0.09/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.56 fof(f49,axiom,(
% 0.09/0.56 (! [A,B] :( m1_subset_1(A,B)=> ( v1_xboole_0(B)| r2_hidden(A,B) ) ) )),
% 0.09/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.56 fof(f52,axiom,(
% 0.09/0.56 (! [A] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( m1_group_2(B,A)=> k2_group_1(B) = k2_group_1(A) ) )) )),
% 0.09/0.56 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.56 fof(f57,plain,(
% 0.09/0.56 (?[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))&~r2_hidden(k2_group_1(A),k1_funct_1(k1_latsubgr(A),B))))))),
% 0.09/0.56 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.09/0.56 fof(f58,plain,(
% 0.09/0.56 ((((~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))&~r2_hidden(k2_group_1(sK0_skl),k1_funct_1(k1_latsubgr(sK0_skl),sK1_skl))))),
% 0.09/0.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl)],[f57])).
% 0.09/0.56 fof(f59,plain,(
% 0.09/0.56 ~v3_struct_0(sK0_skl)),
% 0.09/0.56 inference(cnf_transformation,[status(thm)],[f58])).
% 0.09/0.56 fof(f60,plain,(
% 0.09/0.56 v3_group_1(sK0_skl)),
% 0.09/0.56 inference(cnf_transformation,[status(thm)],[f58])).
% 0.09/0.56 fof(f61,plain,(
% 0.09/0.56 v4_group_1(sK0_skl)),
% 0.09/0.56 inference(cnf_transformation,[status(thm)],[f58])).
% 0.09/0.56 fof(f62,plain,(
% 0.09/0.56 l1_group_1(sK0_skl)),
% 0.09/0.56 inference(cnf_transformation,[status(thm)],[f58])).
% 0.09/0.56 fof(f63,plain,(
% 0.09/0.56 v1_group_1(sK1_skl)),
% 0.09/0.56 inference(cnf_transformation,[status(thm)],[f58])).
% 0.09/0.56 fof(f64,plain,(
% 0.09/0.56 m1_group_2(sK1_skl,sK0_skl)),
% 0.09/0.56 inference(cnf_transformation,[status(thm)],[f58])).
% 0.09/0.56 fof(f65,plain,(
% 0.09/0.56 ~r2_hidden(k2_group_1(sK0_skl),k1_funct_1(k1_latsubgr(sK0_skl),sK1_skl))),
% 0.09/0.56 inference(cnf_transformation,[status(thm)],[f58])).
% 0.09/0.56 fof(f86,plain,(
% 0.09/0.56 ![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.09/0.56 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.09/0.56 fof(f87,plain,(
% 0.09/0.56 ![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.09/0.56 inference(NNF_transformation,[status(thm)],[f86])).
% 0.09/0.56 fof(f88,plain,(
% 0.09/0.56 ![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.09/0.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(C,sK2_skl(B,A))],[f87])).
% 0.09/0.56 fof(f89,plain,(
% 0.09/0.56 ![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.09/0.56 inference(cnf_transformation,[status(thm)],[f88])).
% 0.09/0.56 fof(f96,plain,(
% 0.09/0.56 ![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.09/0.56 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.09/0.56 fof(f97,plain,(
% 0.09/0.56 ![X0]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|v1_funct_1(k1_latsubgr(X0)))),
% 0.09/0.56 inference(cnf_transformation,[status(thm)],[f96])).
% 0.09/0.56 fof(f98,plain,(
% 0.09/0.56 ![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.09/0.56 inference(cnf_transformation,[status(thm)],[f96])).
% 0.09/0.56 fof(f99,plain,(
% 0.09/0.56 ![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.09/0.56 inference(cnf_transformation,[status(thm)],[f96])).
% 0.09/0.56 fof(f100,plain,(
% 0.09/0.56 ![A]: ((v3_struct_0(A)|~l1_group_1(A))|m1_subset_1(k2_group_1(A),u1_struct_0(A)))),
% 0.09/0.56 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.09/0.56 fof(f101,plain,(
% 0.09/0.56 ![X0]: (v3_struct_0(X0)|~l1_group_1(X0)|m1_subset_1(k2_group_1(X0),u1_struct_0(X0)))),
% 0.09/0.56 inference(cnf_transformation,[status(thm)],[f100])).
% 0.09/0.56 fof(f102,plain,(
% 0.09/0.56 ![A]: (~l1_group_1(A)|l1_struct_0(A))),
% 0.09/0.56 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.09/0.56 fof(f103,plain,(
% 0.09/0.56 ![X0]: (~l1_group_1(X0)|l1_struct_0(X0))),
% 0.09/0.56 inference(cnf_transformation,[status(thm)],[f102])).
% 0.09/0.56 fof(f104,plain,(
% 0.09/0.56 ![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.09/0.56 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.09/0.56 fof(f105,plain,(
% 0.09/0.56 ![X0,X1]: (v3_struct_0(X0)|~v3_group_1(X0)|~l1_group_1(X0)|~m1_group_2(X1,X0)|~v3_struct_0(X1))),
% 0.09/0.56 inference(cnf_transformation,[status(thm)],[f104])).
% 0.09/0.56 fof(f107,plain,(
% 0.09/0.56 ![X0,X1]: (v3_struct_0(X0)|~v3_group_1(X0)|~l1_group_1(X0)|~m1_group_2(X1,X0)|l1_group_1(X1))),
% 0.09/0.56 inference(cnf_transformation,[status(thm)],[f104])).
% 0.09/0.56 fof(f110,plain,(
% 0.09/0.56 ![A]: (~l1_group_1(A)|((v1_funct_1(u1_group_1(A))&v1_funct_2(u1_group_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)))&m2_relset_1(u1_group_1(A),k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))))),
% 0.09/0.56 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 0.09/0.56 fof(f111,plain,(
% 0.09/0.56 ![X0]: (~l1_group_1(X0)|v1_funct_1(u1_group_1(X0)))),
% 0.09/0.56 inference(cnf_transformation,[status(thm)],[f110])).
% 0.09/0.56 fof(f113,plain,(
% 0.09/0.56 ![X0]: (~l1_group_1(X0)|m2_relset_1(u1_group_1(X0),k2_zfmisc_1(u1_struct_0(X0),u1_struct_0(X0)),u1_struct_0(X0)))),
% 0.09/0.56 inference(cnf_transformation,[status(thm)],[f110])).
% 0.09/0.56 fof(f114,plain,(
% 0.09/0.56 l1_group_1(sK3_skl)),
% 0.09/0.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(A,sK3_skl)],[f26])).
% 0.09/0.56 fof(f115,plain,(
% 0.09/0.56 l1_group_1(sK3_skl)),
% 0.09/0.56 inference(cnf_transformation,[status(thm)],[f114])).
% 0.09/0.56 fof(f129,plain,(
% 0.09/0.56 ![A]: ((v3_struct_0(A)|~l1_struct_0(A))|~v1_xboole_0(u1_struct_0(A)))),
% 0.09/0.56 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 0.09/0.56 fof(f130,plain,(
% 0.09/0.56 ![X0]: (v3_struct_0(X0)|~l1_struct_0(X0)|~v1_xboole_0(u1_struct_0(X0)))),
% 0.09/0.56 inference(cnf_transformation,[status(thm)],[f129])).
% 0.09/0.56 fof(f131,plain,(
% 0.09/0.56 ![X0]: (~v1_xboole_0(k1_zfmisc_1(X0)))),
% 0.09/0.56 inference(cnf_transformation,[status(thm)],[f34])).
% 0.09/0.56 fof(f165,plain,(
% 0.09/0.56 ![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.09/0.56 inference(NNF_transformation,[status(thm)],[f46])).
% 0.09/0.56 fof(f166,plain,(
% 0.09/0.56 (![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.09/0.56 inference(miniscoping,[status(thm)],[f165])).
% 0.09/0.56 fof(f167,plain,(
% 0.09/0.56 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_relset_1(X0,X1,X2))),
% 0.09/0.56 inference(cnf_transformation,[status(thm)],[f166])).
% 0.09/0.56 fof(f173,plain,(
% 0.09/0.56 ![A,B]: (~m1_subset_1(A,B)|(v1_xboole_0(B)|r2_hidden(A,B)))),
% 0.09/0.56 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 0.09/0.56 fof(f174,plain,(
% 0.09/0.56 ![X0,X1]: (~m1_subset_1(X0,X1)|v1_xboole_0(X1)|r2_hidden(X0,X1))),
% 0.09/0.56 inference(cnf_transformation,[status(thm)],[f173])).
% 0.09/0.56 fof(f182,plain,(
% 0.09/0.56 ![A]: ((((v3_struct_0(A)|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|(![B]: (~m1_group_2(B,A)|k2_group_1(B)=k2_group_1(A))))),
% 0.09/0.56 inference(pre_NNF_transformation,[status(thm)],[f52])).
% 0.09/0.56 fof(f183,plain,(
% 0.09/0.56 ![X0,X1]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m1_group_2(X1,X0)|k2_group_1(X1)=k2_group_1(X0))),
% 0.09/0.56 inference(cnf_transformation,[status(thm)],[f182])).
% 0.09/0.56 fof(f195,plain,(
% 0.09/0.56 ![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.09/0.56 inference(destructive_equality_resolution,[status(thm)],[f89])).
% 0.09/0.56 fof(f196,plain,(
% 0.09/0.56 ![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.09/0.56 inference(backward_subsumption_resolution,[status(thm)],[f195,f97])).
% 0.09/0.56 fof(f197,plain,(
% 0.09/0.56 ![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.09/0.56 inference(forward_subsumption_resolution,[status(thm)],[f196,f98])).
% 0.09/0.56 fof(f199,definition,(
% 0.09/0.56 sQ0_spl <=> (l1_group_1(sK1_skl))),
% 0.09/0.56 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.09/0.56 fof(f200,plain,(
% 0.09/0.56 l1_group_1(sK1_skl)|~sQ0_spl),
% 0.09/0.56 inference(component_clause,[status(thm)],[f199])).
% 0.09/0.56 fof(f227,definition,(
% 0.09/0.56 sQ6_spl <=> (v3_struct_0(sK0_skl))),
% 0.09/0.56 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.09/0.56 fof(f228,plain,(
% 0.09/0.56 v3_struct_0(sK0_skl)|~sQ6_spl),
% 0.09/0.56 inference(component_clause,[status(thm)],[f227])).
% 0.09/0.56 fof(f230,definition,(
% 0.09/0.56 sQ7_spl <=> (v3_group_1(sK0_skl))),
% 0.09/0.56 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.09/0.56 fof(f232,plain,(
% 0.09/0.56 ~v3_group_1(sK0_skl)|sQ7_spl),
% 0.09/0.56 inference(component_clause,[status(thm)],[f230])).
% 0.09/0.56 fof(f233,definition,(
% 0.09/0.56 sQ8_spl <=> (v4_group_1(sK0_skl))),
% 0.09/0.56 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.09/0.56 fof(f235,plain,(
% 0.09/0.56 ~v4_group_1(sK0_skl)|sQ8_spl),
% 0.09/0.56 inference(component_clause,[status(thm)],[f233])).
% 0.09/0.56 fof(f240,plain,(
% 0.09/0.56 $false|sQ8_spl),
% 0.09/0.56 inference(forward_subsumption_resolution,[status(thm)],[f235,f61])).
% 0.09/0.56 fof(f241,plain,(
% 0.09/0.56 sQ8_spl),
% 0.09/0.56 inference(contradiction_clause,[status(thm)],[f240])).
% 0.09/0.56 fof(f242,plain,(
% 0.09/0.56 $false|sQ7_spl),
% 0.09/0.56 inference(forward_subsumption_resolution,[status(thm)],[f232,f60])).
% 0.09/0.56 fof(f243,plain,(
% 0.09/0.56 sQ7_spl),
% 0.09/0.56 inference(contradiction_clause,[status(thm)],[f242])).
% 0.09/0.56 fof(f244,plain,(
% 0.09/0.56 $false|~sQ6_spl),
% 0.09/0.56 inference(forward_subsumption_resolution,[status(thm)],[f228,f59])).
% 0.09/0.56 fof(f245,plain,(
% 0.09/0.56 ~sQ6_spl),
% 0.09/0.56 inference(contradiction_clause,[status(thm)],[f244])).
% 0.09/0.56 fof(f257,plain,(
% 0.09/0.56 v3_struct_0(sK0_skl)|~v3_group_1(sK0_skl)|~v4_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.09/0.56 inference(resolution,[status(thm)],[f99,f62])).
% 0.09/0.56 fof(f262,definition,(
% 0.09/0.56 sQ13_spl <=> (m2_relset_1(k1_latsubgr(sK0_skl),k1_group_3(sK0_skl),k1_zfmisc_1(u1_struct_0(sK0_skl))))),
% 0.09/0.56 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.09/0.56 fof(f263,plain,(
% 0.09/0.56 m2_relset_1(k1_latsubgr(sK0_skl),k1_group_3(sK0_skl),k1_zfmisc_1(u1_struct_0(sK0_skl)))|~sQ13_spl),
% 0.09/0.56 inference(component_clause,[status(thm)],[f262])).
% 0.09/0.56 fof(f265,plain,(
% 0.09/0.56 sQ6_spl|~sQ7_spl|~sQ8_spl|sQ13_spl),
% 0.09/0.56 inference(split_clause,[status(thm)],[f257,f227,f230,f233,f262])).
% 0.09/0.56 fof(f276,plain,(
% 0.09/0.56 v3_struct_0(sK0_skl)|~v3_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~v3_struct_0(sK1_skl)),
% 0.09/0.56 inference(resolution,[status(thm)],[f105,f64])).
% 0.09/0.56 fof(f277,definition,(
% 0.09/0.56 sQ16_spl <=> (l1_group_1(sK0_skl))),
% 0.09/0.56 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.09/0.56 fof(f279,plain,(
% 0.09/0.56 ~l1_group_1(sK0_skl)|sQ16_spl),
% 0.09/0.56 inference(component_clause,[status(thm)],[f277])).
% 0.09/0.56 fof(f280,definition,(
% 0.09/0.56 sQ17_spl <=> (v3_struct_0(sK1_skl))),
% 0.09/0.56 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.09/0.56 fof(f283,plain,(
% 0.09/0.56 sQ6_spl|~sQ7_spl|~sQ16_spl|~sQ17_spl),
% 0.09/0.56 inference(split_clause,[status(thm)],[f276,f227,f230,f277,f280])).
% 0.09/0.56 fof(f284,plain,(
% 0.09/0.56 $false|sQ16_spl),
% 0.09/0.56 inference(forward_subsumption_resolution,[status(thm)],[f279,f62])).
% 0.09/0.56 fof(f285,plain,(
% 0.09/0.56 sQ16_spl),
% 0.09/0.56 inference(contradiction_clause,[status(thm)],[f284])).
% 0.09/0.56 fof(f295,plain,(
% 0.09/0.56 v3_struct_0(sK0_skl)|~v3_group_1(sK0_skl)|~l1_group_1(sK0_skl)|l1_group_1(sK1_skl)),
% 0.09/0.56 inference(resolution,[status(thm)],[f107,f64])).
% 0.09/0.56 fof(f296,plain,(
% 0.09/0.56 sQ6_spl|~sQ7_spl|~sQ16_spl|sQ0_spl),
% 0.15/0.56 inference(split_clause,[status(thm)],[f295,f227,f230,f277,f199])).
% 0.15/0.56 fof(f330,plain,(
% 0.15/0.56 v1_funct_1(u1_group_1(sK3_skl))),
% 0.15/0.56 inference(resolution,[status(thm)],[f111,f115])).
% 0.15/0.56 fof(f334,plain,(
% 0.15/0.56 m2_relset_1(u1_group_1(sK3_skl),k2_zfmisc_1(u1_struct_0(sK3_skl),u1_struct_0(sK3_skl)),u1_struct_0(sK3_skl))),
% 0.15/0.56 inference(resolution,[status(thm)],[f113,f115])).
% 0.15/0.56 fof(f361,plain,(
% 0.15/0.56 l1_struct_0(sK1_skl)|~sQ0_spl),
% 0.15/0.56 inference(resolution,[status(thm)],[f200,f103])).
% 0.15/0.56 fof(f362,plain,(
% 0.15/0.56 v3_struct_0(sK1_skl)|m1_subset_1(k2_group_1(sK1_skl),u1_struct_0(sK1_skl))|~sQ0_spl),
% 0.15/0.56 inference(resolution,[status(thm)],[f200,f101])).
% 0.15/0.56 fof(f370,definition,(
% 0.15/0.56 sQ32_spl <=> (m1_subset_1(k2_group_1(sK1_skl),u1_struct_0(sK1_skl)))),
% 0.15/0.56 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.15/0.56 fof(f371,plain,(
% 0.15/0.56 m1_subset_1(k2_group_1(sK1_skl),u1_struct_0(sK1_skl))|~sQ32_spl),
% 0.15/0.56 inference(component_clause,[status(thm)],[f370])).
% 0.15/0.56 fof(f373,plain,(
% 0.15/0.56 sQ17_spl|sQ32_spl|~sQ0_spl),
% 0.15/0.56 inference(split_clause,[status(thm)],[f362,f280,f370,f199])).
% 0.15/0.56 fof(f389,plain,(
% 0.15/0.56 v3_struct_0(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|k2_group_1(sK1_skl)=k2_group_1(sK0_skl)),
% 0.15/0.56 inference(resolution,[status(thm)],[f183,f64])).
% 0.15/0.56 fof(f390,definition,(
% 0.15/0.56 sQ37_spl <=> (k2_group_1(sK1_skl)=k2_group_1(sK0_skl))),
% 0.15/0.56 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.15/0.56 fof(f391,plain,(
% 0.15/0.56 k2_group_1(sK1_skl)=k2_group_1(sK0_skl)|~sQ37_spl),
% 0.15/0.56 inference(component_clause,[status(thm)],[f390])).
% 0.15/0.56 fof(f393,plain,(
% 0.15/0.56 sQ6_spl|~sQ7_spl|~sQ8_spl|~sQ16_spl|sQ37_spl),
% 0.15/0.56 inference(split_clause,[status(thm)],[f389,f227,f230,f233,f277,f390])).
% 0.15/0.56 fof(f394,plain,(
% 0.15/0.56 m1_subset_1(k2_group_1(sK0_skl),u1_struct_0(sK1_skl))|~sQ37_spl|~sQ32_spl),
% 0.15/0.56 inference(backward_demodulation,[status(thm)],[f391,f371])).
% 0.15/0.56 fof(f396,plain,(
% 0.15/0.56 ![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)|~sQ13_spl)),
% 0.15/0.56 inference(resolution,[status(thm)],[f197,f263])).
% 0.15/0.56 fof(f397,definition,(
% 0.15/0.56 ![X0]: (sQ38_spl <=> (~v1_group_1(X0)|~m1_group_2(X0,sK0_skl)|k1_funct_1(k1_latsubgr(sK0_skl),X0)=u1_struct_0(X0)))),
% 0.15/0.56 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.15/0.56 fof(f398,plain,(
% 0.15/0.56 ![X0]: (~v1_group_1(X0)|~m1_group_2(X0,sK0_skl)|k1_funct_1(k1_latsubgr(sK0_skl),X0)=u1_struct_0(X0)|~sQ38_spl)),
% 0.15/0.56 inference(component_clause,[status(thm)],[f397])).
% 0.15/0.56 fof(f400,plain,(
% 0.15/0.56 sQ6_spl|~sQ7_spl|~sQ8_spl|~sQ16_spl|sQ38_spl|~sQ13_spl),
% 0.15/0.56 inference(split_clause,[status(thm)],[f396,f227,f230,f233,f277,f397,f262])).
% 0.15/0.56 fof(f657,definition,(
% 0.15/0.56 sQ78_spl <=> (v1_xboole_0(u1_struct_0(sK1_skl)))),
% 0.15/0.56 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.15/0.56 fof(f658,plain,(
% 0.15/0.56 v1_xboole_0(u1_struct_0(sK1_skl))|~sQ78_spl),
% 0.15/0.56 inference(component_clause,[status(thm)],[f657])).
% 0.15/0.56 fof(f696,plain,(
% 0.15/0.56 v1_xboole_0(u1_struct_0(sK1_skl))|r2_hidden(k2_group_1(sK0_skl),u1_struct_0(sK1_skl))|~sQ37_spl|~sQ32_spl),
% 0.15/0.56 inference(resolution,[status(thm)],[f394,f174])).
% 0.15/0.56 fof(f697,definition,(
% 0.15/0.56 sQ85_spl <=> (r2_hidden(k2_group_1(sK0_skl),u1_struct_0(sK1_skl)))),
% 0.15/0.56 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 0.15/0.56 fof(f698,plain,(
% 0.15/0.56 r2_hidden(k2_group_1(sK0_skl),u1_struct_0(sK1_skl))|~sQ85_spl),
% 0.15/0.56 inference(component_clause,[status(thm)],[f697])).
% 0.15/0.56 fof(f700,plain,(
% 0.15/0.56 sQ78_spl|sQ85_spl|~sQ37_spl|~sQ32_spl),
% 0.15/0.56 inference(split_clause,[status(thm)],[f696,f657,f697,f390,f370])).
% 0.15/0.56 fof(f702,plain,(
% 0.15/0.56 ~v1_group_1(sK1_skl)|k1_funct_1(k1_latsubgr(sK0_skl),sK1_skl)=u1_struct_0(sK1_skl)|~sQ38_spl),
% 0.15/0.56 inference(resolution,[status(thm)],[f398,f64])).
% 0.15/0.56 fof(f710,definition,(
% 0.15/0.56 sQ88_spl <=> (v1_group_1(sK1_skl))),
% 0.15/0.56 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 0.15/0.56 fof(f712,plain,(
% 0.15/0.56 ~v1_group_1(sK1_skl)|sQ88_spl),
% 0.15/0.56 inference(component_clause,[status(thm)],[f710])).
% 0.15/0.56 fof(f713,definition,(
% 0.15/0.56 sQ89_spl <=> (k1_funct_1(k1_latsubgr(sK0_skl),sK1_skl)=u1_struct_0(sK1_skl))),
% 0.15/0.56 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.15/0.56 fof(f714,plain,(
% 0.15/0.56 k1_funct_1(k1_latsubgr(sK0_skl),sK1_skl)=u1_struct_0(sK1_skl)|~sQ89_spl),
% 0.15/0.56 inference(component_clause,[status(thm)],[f713])).
% 0.15/0.56 fof(f716,plain,(
% 0.15/0.56 ~sQ88_spl|sQ89_spl|~sQ38_spl),
% 0.15/0.56 inference(split_clause,[status(thm)],[f702,f710,f713,f397])).
% 0.15/0.56 fof(f717,plain,(
% 0.15/0.56 $false|sQ88_spl),
% 0.15/0.56 inference(forward_subsumption_resolution,[status(thm)],[f712,f63])).
% 0.15/0.56 fof(f718,plain,(
% 0.15/0.56 sQ88_spl),
% 0.15/0.56 inference(contradiction_clause,[status(thm)],[f717])).
% 0.15/0.56 fof(f719,plain,(
% 0.15/0.56 ~r2_hidden(k2_group_1(sK0_skl),u1_struct_0(sK1_skl))|~sQ89_spl),
% 0.15/0.56 inference(backward_demodulation,[status(thm)],[f714,f65])).
% 0.15/0.56 fof(f780,definition,(
% 0.15/0.56 sQ94_spl <=> (v1_xboole_0(k1_zfmisc_1(k2_zfmisc_1(k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl)))))),
% 0.15/0.56 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 0.15/0.56 fof(f781,plain,(
% 0.15/0.56 v1_xboole_0(k1_zfmisc_1(k2_zfmisc_1(k2_zfmisc_1(u1_struct_0(sK0_skl),u1_struct_0(sK0_skl)),u1_struct_0(sK0_skl))))|~sQ94_spl),
% 0.15/0.56 inference(component_clause,[status(thm)],[f780])).
% 0.15/0.56 fof(f787,plain,(
% 0.15/0.56 $false|~sQ94_spl),
% 0.15/0.56 inference(forward_subsumption_resolution,[status(thm)],[f781,f131])).
% 0.15/0.56 fof(f788,plain,(
% 0.15/0.56 ~sQ94_spl),
% 0.15/0.56 inference(contradiction_clause,[status(thm)],[f787])).
% 0.15/0.56 fof(f805,definition,(
% 0.15/0.56 sQ96_spl <=> (v1_funct_1(u1_group_1(sK3_skl)))),
% 0.15/0.56 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 0.15/0.56 fof(f807,plain,(
% 0.15/0.56 ~v1_funct_1(u1_group_1(sK3_skl))|sQ96_spl),
% 0.15/0.56 inference(component_clause,[status(thm)],[f805])).
% 0.15/0.56 fof(f808,definition,(
% 0.15/0.56 sQ97_spl <=> (m1_relset_1(u1_group_1(sK3_skl),k2_zfmisc_1(u1_struct_0(sK3_skl),u1_struct_0(sK3_skl)),u1_struct_0(sK3_skl)))),
% 0.15/0.56 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 0.15/0.56 fof(f810,plain,(
% 0.15/0.56 ~m1_relset_1(u1_group_1(sK3_skl),k2_zfmisc_1(u1_struct_0(sK3_skl),u1_struct_0(sK3_skl)),u1_struct_0(sK3_skl))|sQ97_spl),
% 0.15/0.56 inference(component_clause,[status(thm)],[f808])).
% 0.15/0.56 fof(f841,plain,(
% 0.15/0.56 $false|sQ96_spl),
% 0.15/0.56 inference(forward_subsumption_resolution,[status(thm)],[f807,f330])).
% 0.15/0.56 fof(f842,plain,(
% 0.15/0.56 sQ96_spl),
% 0.15/0.56 inference(contradiction_clause,[status(thm)],[f841])).
% 0.15/0.56 fof(f843,plain,(
% 0.15/0.56 m1_relset_1(u1_group_1(sK3_skl),k2_zfmisc_1(u1_struct_0(sK3_skl),u1_struct_0(sK3_skl)),u1_struct_0(sK3_skl))),
% 0.15/0.56 inference(resolution,[status(thm)],[f334,f167])).
% 0.15/0.56 fof(f845,plain,(
% 0.15/0.56 $false|sQ97_spl),
% 0.15/0.56 inference(forward_subsumption_resolution,[status(thm)],[f843,f810])).
% 0.15/0.56 fof(f846,plain,(
% 0.15/0.56 sQ97_spl),
% 0.15/0.56 inference(contradiction_clause,[status(thm)],[f845])).
% 0.15/0.56 fof(f859,plain,(
% 0.15/0.56 v3_struct_0(sK1_skl)|~l1_struct_0(sK1_skl)|~sQ78_spl),
% 0.15/0.56 inference(resolution,[status(thm)],[f658,f130])).
% 0.15/0.56 fof(f862,definition,(
% 0.15/0.56 sQ106_spl <=> (l1_struct_0(sK1_skl))),
% 0.15/0.56 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 0.15/0.56 fof(f864,plain,(
% 0.15/0.56 ~l1_struct_0(sK1_skl)|sQ106_spl),
% 0.15/0.56 inference(component_clause,[status(thm)],[f862])).
% 0.15/0.56 fof(f865,plain,(
% 0.15/0.56 sQ17_spl|~sQ106_spl|~sQ78_spl),
% 0.15/0.56 inference(split_clause,[status(thm)],[f859,f280,f862,f657])).
% 0.15/0.56 fof(f886,plain,(
% 0.15/0.56 $false|~sQ0_spl|sQ106_spl),
% 0.15/0.56 inference(forward_subsumption_resolution,[status(thm)],[f864,f361])).
% 0.15/0.56 fof(f887,plain,(
% 0.15/0.56 ~sQ0_spl|sQ106_spl),
% 0.15/0.56 inference(contradiction_clause,[status(thm)],[f886])).
% 0.15/0.56 fof(f888,plain,(
% 0.15/0.56 $false|~sQ85_spl|~sQ89_spl),
% 0.15/0.56 inference(forward_subsumption_resolution,[status(thm)],[f719,f698])).
% 0.15/0.56 fof(f889,plain,(
% 0.15/0.56 ~sQ85_spl|~sQ89_spl),
% 0.15/0.56 inference(contradiction_clause,[status(thm)],[f888])).
% 0.15/0.56 fof(f890,plain,(
% 0.15/0.56 $false),
% 0.15/0.56 inference(sat_refutation,[status(thm)],[f241,f243,f245,f265,f283,f285,f296,f373,f393,f400,f700,f716,f718,f788,f842,f846,f865,f887,f889])).
% 0.15/0.56 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/0.58 % Elapsed time: 0.068347 seconds
% 0.15/0.58 % CPU time: 0.209927 seconds
% 0.15/0.58 % Total memory used: 85.412 MB
% 0.15/0.58 % Net memory used: 85.300 MB
%------------------------------------------------------------------------------