%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP641+2 : 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 : n016.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 8.96s 2.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP641+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.69 % Computer : n016.cluster.edu
% 0.18/0.69 % Model : x86_64 x86_64
% 0.18/0.69 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.69 % Memory : 8046.5625MB
% 0.18/0.69 % OS : Linux 6.8.0-71-generic
% 0.18/0.69 % CPULimit : 300
% 0.18/0.69 % WCLimit : 300
% 0.18/0.69 % DateTime : Sun Sep 20 20:29:24 UTC 2026
% 0.18/0.69 % CPUTime :
% 0.78/1.36 % Drodi V4.1.1
% 8.96/2.60 % Refutation found
% 8.96/2.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 8.96/2.60 % SZS output start CNFRefutation for theBenchmark
% 8.96/2.60 fof(f3812,axiom,(
% 8.96/2.60 (! [A] :( ( ~ v3_struct_0(A)& l1_group_1(A) )=> m1_subset_1(k2_group_1(A),u1_struct_0(A)) ) )),
% 8.96/2.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.96/2.60 fof(f4339,axiom,(
% 8.96/2.60 (! [A] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( m1_group_2(B,A)=> v4_group_1(B) ) )) )),
% 8.96/2.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.96/2.60 fof(f4397,axiom,(
% 8.96/2.60 (! [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) ) )) )),
% 8.96/2.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.96/2.60 fof(f4399,axiom,(
% 8.96/2.60 (! [A] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( m1_group_2(B,A)=> r1_rlvect_1(B,k2_group_1(A)) ) )) )),
% 8.96/2.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.96/2.60 fof(f4407,axiom,(
% 8.96/2.60 (! [A] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> m1_group_2(A,A) ) )),
% 8.96/2.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.96/2.60 fof(f4540,axiom,(
% 8.96/2.60 (! [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) ) ) )) )),
% 8.96/2.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.96/2.60 fof(f5636,axiom,(
% 8.96/2.60 (! [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))) ) ) )),
% 8.96/2.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.96/2.60 fof(f5653,axiom,(
% 8.96/2.60 (! [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) ) )) ) )) )),
% 8.96/2.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.96/2.60 fof(f5657,axiom,(
% 8.96/2.60 (! [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) )=> (! [C] :( m1_subset_1(C,u1_struct_0(A))=> ( r2_hidden(C,k1_funct_1(k1_latsubgr(A),B))<=> r1_rlvect_1(B,C) ) ) )) )) )),
% 8.96/2.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.96/2.60 fof(f5658,conjecture,(
% 8.96/2.60 (! [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)) ) )) )),
% 8.96/2.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 8.96/2.60 fof(f5659,negated_conjecture,(
% 8.96/2.60 ~((! [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)) ) )) ))),
% 8.96/2.60 inference(negated_conjecture,[status(cth)],[f5658])).
% 8.96/2.60 fof(f16371,plain,(
% 8.96/2.60 ![A]: ((v3_struct_0(A)|~l1_group_1(A))|m1_subset_1(k2_group_1(A),u1_struct_0(A)))),
% 8.96/2.60 inference(pre_NNF_transformation,[status(thm)],[f3812])).
% 8.96/2.60 fof(f16372,plain,(
% 8.96/2.60 ![X0]: (v3_struct_0(X0)|~l1_group_1(X0)|m1_subset_1(k2_group_1(X0),u1_struct_0(X0)))),
% 8.96/2.60 inference(cnf_transformation,[status(thm)],[f16371])).
% 8.96/2.60 fof(f17649,plain,(
% 8.96/2.60 ![A]: ((((v3_struct_0(A)|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|(![B]: (~m1_group_2(B,A)|v4_group_1(B))))),
% 8.96/2.60 inference(pre_NNF_transformation,[status(thm)],[f4339])).
% 8.96/2.60 fof(f17650,plain,(
% 8.96/2.60 ![X0,X1]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m1_group_2(X1,X0)|v4_group_1(X1))),
% 8.96/2.60 inference(cnf_transformation,[status(thm)],[f17649])).
% 8.96/2.60 fof(f17806,plain,(
% 8.96/2.60 ![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))))),
% 8.96/2.60 inference(pre_NNF_transformation,[status(thm)],[f4397])).
% 8.96/2.60 fof(f17807,plain,(
% 8.96/2.60 ![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))),
% 8.96/2.60 inference(cnf_transformation,[status(thm)],[f17806])).
% 8.96/2.60 fof(f17810,plain,(
% 8.96/2.60 ![A]: ((((v3_struct_0(A)|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|(![B]: (~m1_group_2(B,A)|r1_rlvect_1(B,k2_group_1(A)))))),
% 8.96/2.60 inference(pre_NNF_transformation,[status(thm)],[f4399])).
% 8.96/2.60 fof(f17811,plain,(
% 8.96/2.60 ![X0,X1]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m1_group_2(X1,X0)|r1_rlvect_1(X1,k2_group_1(X0)))),
% 8.96/2.60 inference(cnf_transformation,[status(thm)],[f17810])).
% 8.96/2.60 fof(f17832,plain,(
% 8.96/2.60 ![A]: ((((v3_struct_0(A)|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|m1_group_2(A,A))),
% 8.96/2.60 inference(pre_NNF_transformation,[status(thm)],[f4407])).
% 8.96/2.60 fof(f17833,plain,(
% 8.96/2.60 ![X0]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|m1_group_2(X0,X0))),
% 8.96/2.60 inference(cnf_transformation,[status(thm)],[f17832])).
% 8.96/2.60 fof(f18197,plain,(
% 8.96/2.60 ![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)))))),
% 8.96/2.60 inference(pre_NNF_transformation,[status(thm)],[f4540])).
% 8.96/2.60 fof(f18198,plain,(
% 8.96/2.60 ![X0,X1]: (v3_struct_0(X0)|~v3_group_1(X0)|~l1_group_1(X0)|~m1_group_2(X1,X0)|~v3_struct_0(X1))),
% 8.96/2.60 inference(cnf_transformation,[status(thm)],[f18197])).
% 8.96/2.60 fof(f18199,plain,(
% 8.96/2.60 ![X0,X1]: (v3_struct_0(X0)|~v3_group_1(X0)|~l1_group_1(X0)|~m1_group_2(X1,X0)|v3_group_1(X1))),
% 8.96/2.60 inference(cnf_transformation,[status(thm)],[f18197])).
% 8.96/2.60 fof(f18200,plain,(
% 8.96/2.60 ![X0,X1]: (v3_struct_0(X0)|~v3_group_1(X0)|~l1_group_1(X0)|~m1_group_2(X1,X0)|l1_group_1(X1))),
% 8.96/2.60 inference(cnf_transformation,[status(thm)],[f18197])).
% 8.96/2.60 fof(f22026,plain,(
% 8.96/2.60 ![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)))))),
% 8.96/2.60 inference(pre_NNF_transformation,[status(thm)],[f5636])).
% 8.96/2.60 fof(f22027,plain,(
% 8.96/2.60 ![X0]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|v1_funct_1(k1_latsubgr(X0)))),
% 8.96/2.60 inference(cnf_transformation,[status(thm)],[f22026])).
% 8.96/2.60 fof(f22028,plain,(
% 8.96/2.60 ![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))))),
% 8.96/2.60 inference(cnf_transformation,[status(thm)],[f22026])).
% 8.96/2.60 fof(f22029,plain,(
% 8.96/2.60 ![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))))),
% 8.96/2.60 inference(cnf_transformation,[status(thm)],[f22026])).
% 8.96/2.60 fof(f22074,plain,(
% 8.96/2.60 ![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)))))))),
% 8.96/2.60 inference(pre_NNF_transformation,[status(thm)],[f5653])).
% 8.96/2.60 fof(f22075,plain,(
% 8.96/2.60 ![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))))))))),
% 8.96/2.60 inference(NNF_transformation,[status(thm)],[f22074])).
% 8.96/2.60 fof(f22076,plain,(
% 8.96/2.60 ![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(sK1494_skl(B,A))&m1_group_2(sK1494_skl(B,A),A))&~k1_funct_1(B,sK1494_skl(B,A))=u1_struct_0(sK1494_skl(B,A))))))))),
% 8.96/2.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK1494_skl]),skolemize(C,sK1494_skl(B,A))],[f22075])).
% 8.96/2.60 fof(f22077,plain,(
% 8.96/2.60 ![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))),
% 8.96/2.60 inference(cnf_transformation,[status(thm)],[f22076])).
% 8.96/2.60 fof(f22081,plain,(
% 8.96/2.60 ![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))|(![C]: (~m1_subset_1(C,u1_struct_0(A))|(r2_hidden(C,k1_funct_1(k1_latsubgr(A),B))<=>r1_rlvect_1(B,C)))))))),
% 8.96/2.60 inference(pre_NNF_transformation,[status(thm)],[f5657])).
% 8.96/2.60 fof(f22082,plain,(
% 8.96/2.60 ![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))|(![C]: (~m1_subset_1(C,u1_struct_0(A))|((~r2_hidden(C,k1_funct_1(k1_latsubgr(A),B))|r1_rlvect_1(B,C))&(r2_hidden(C,k1_funct_1(k1_latsubgr(A),B))|~r1_rlvect_1(B,C))))))))),
% 8.96/2.60 inference(NNF_transformation,[status(thm)],[f22081])).
% 8.96/2.60 fof(f22084,plain,(
% 8.96/2.60 ![X0,X1,X2]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~v1_group_1(X1)|~m1_group_2(X1,X0)|~m1_subset_1(X2,u1_struct_0(X0))|r2_hidden(X2,k1_funct_1(k1_latsubgr(X0),X1))|~r1_rlvect_1(X1,X2))),
% 8.96/2.60 inference(cnf_transformation,[status(thm)],[f22082])).
% 8.96/2.60 fof(f22085,plain,(
% 8.96/2.60 (?[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))))))),
% 8.96/2.60 inference(pre_NNF_transformation,[status(thm)],[f5659])).
% 8.96/2.60 fof(f22086,plain,(
% 8.96/2.60 ((((~v3_struct_0(sK1495_skl)&v3_group_1(sK1495_skl))&v4_group_1(sK1495_skl))&l1_group_1(sK1495_skl))&((v1_group_1(sK1496_skl)&m1_group_2(sK1496_skl,sK1495_skl))&~r2_hidden(k2_group_1(sK1495_skl),k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl))))),
% 8.96/2.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK1495_skl,sK1496_skl]),skolemize(A,sK1495_skl),skolemize(B,sK1496_skl)],[f22085])).
% 8.96/2.60 fof(f22087,plain,(
% 8.96/2.60 ~v3_struct_0(sK1495_skl)),
% 8.96/2.60 inference(cnf_transformation,[status(thm)],[f22086])).
% 8.96/2.60 fof(f22088,plain,(
% 8.96/2.60 v3_group_1(sK1495_skl)),
% 8.96/2.60 inference(cnf_transformation,[status(thm)],[f22086])).
% 8.96/2.60 fof(f22089,plain,(
% 8.96/2.60 v4_group_1(sK1495_skl)),
% 8.96/2.60 inference(cnf_transformation,[status(thm)],[f22086])).
% 8.96/2.60 fof(f22090,plain,(
% 8.96/2.60 l1_group_1(sK1495_skl)),
% 8.96/2.60 inference(cnf_transformation,[status(thm)],[f22086])).
% 8.96/2.60 fof(f22091,plain,(
% 8.96/2.60 v1_group_1(sK1496_skl)),
% 8.96/2.60 inference(cnf_transformation,[status(thm)],[f22086])).
% 8.96/2.60 fof(f22092,plain,(
% 8.96/2.60 m1_group_2(sK1496_skl,sK1495_skl)),
% 8.96/2.60 inference(cnf_transformation,[status(thm)],[f22086])).
% 8.96/2.60 fof(f22093,plain,(
% 8.96/2.60 ~r2_hidden(k2_group_1(sK1495_skl),k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl))),
% 8.96/2.60 inference(cnf_transformation,[status(thm)],[f22086])).
% 8.96/2.60 fof(f26883,plain,(
% 8.96/2.60 ![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))),
% 8.96/2.60 inference(destructive_equality_resolution,[status(thm)],[f22077])).
% 8.96/2.60 fof(f27059,plain,(
% 8.96/2.60 v3_struct_0(sK1495_skl)|m1_subset_1(k2_group_1(sK1495_skl),u1_struct_0(sK1495_skl))),
% 8.96/2.60 inference(resolution,[status(thm)],[f16372,f22090])).
% 8.96/2.60 fof(f27060,definition,(
% 8.96/2.60 sQ609_spl <=> (v3_struct_0(sK1495_skl))),
% 8.96/2.60 introduced(definition,[new_symbols(definition,[sQ609_spl])],[split_symbol_definition])).
% 8.96/2.60 fof(f27061,plain,(
% 8.96/2.60 v3_struct_0(sK1495_skl)|~sQ609_spl),
% 8.96/2.60 inference(component_clause,[status(thm)],[f27060])).
% 8.96/2.60 fof(f27063,definition,(
% 8.96/2.60 sQ610_spl <=> (m1_subset_1(k2_group_1(sK1495_skl),u1_struct_0(sK1495_skl)))),
% 8.96/2.60 introduced(definition,[new_symbols(definition,[sQ610_spl])],[split_symbol_definition])).
% 8.96/2.60 fof(f27064,plain,(
% 8.96/2.60 m1_subset_1(k2_group_1(sK1495_skl),u1_struct_0(sK1495_skl))|~sQ610_spl),
% 8.96/2.60 inference(component_clause,[status(thm)],[f27063])).
% 8.96/2.60 fof(f27066,plain,(
% 8.96/2.60 sQ609_spl|sQ610_spl),
% 8.96/2.60 inference(split_clause,[status(thm)],[f27059,f27060,f27063])).
% 8.96/2.60 fof(f27067,plain,(
% 8.96/2.60 $false|~sQ609_spl),
% 8.96/2.60 inference(forward_subsumption_resolution,[status(thm)],[f27061,f22087])).
% 8.96/2.60 fof(f27068,plain,(
% 8.96/2.60 ~sQ609_spl),
% 8.96/2.60 inference(contradiction_clause,[status(thm)],[f27067])).
% 8.96/2.60 fof(f27070,definition,(
% 8.96/2.60 sQ611_spl <=> (v3_group_1(sK1495_skl))),
% 8.96/2.60 introduced(definition,[new_symbols(definition,[sQ611_spl])],[split_symbol_definition])).
% 8.96/2.60 fof(f27072,plain,(
% 8.96/2.60 ~v3_group_1(sK1495_skl)|sQ611_spl),
% 8.96/2.60 inference(component_clause,[status(thm)],[f27070])).
% 8.96/2.60 fof(f27073,definition,(
% 8.96/2.60 sQ612_spl <=> (v4_group_1(sK1495_skl))),
% 8.96/2.60 introduced(definition,[new_symbols(definition,[sQ612_spl])],[split_symbol_definition])).
% 8.96/2.60 fof(f27075,plain,(
% 8.96/2.60 ~v4_group_1(sK1495_skl)|sQ612_spl),
% 8.96/2.60 inference(component_clause,[status(thm)],[f27073])).
% 8.96/2.60 fof(f27080,plain,(
% 8.96/2.60 $false|sQ612_spl),
% 8.96/2.60 inference(forward_subsumption_resolution,[status(thm)],[f27075,f22089])).
% 8.96/2.60 fof(f27081,plain,(
% 8.96/2.60 sQ612_spl),
% 8.96/2.60 inference(contradiction_clause,[status(thm)],[f27080])).
% 8.96/2.60 fof(f27082,plain,(
% 8.96/2.60 $false|sQ611_spl),
% 8.96/2.60 inference(forward_subsumption_resolution,[status(thm)],[f27072,f22088])).
% 8.96/2.60 fof(f27083,plain,(
% 8.96/2.60 sQ611_spl),
% 8.96/2.60 inference(contradiction_clause,[status(thm)],[f27082])).
% 8.96/2.60 fof(f27085,plain,(
% 8.96/2.60 v3_struct_0(sK1495_skl)|~v3_group_1(sK1495_skl)|~l1_group_1(sK1495_skl)|~v3_struct_0(sK1496_skl)),
% 8.96/2.60 inference(resolution,[status(thm)],[f18198,f22092])).
% 8.96/2.60 fof(f27086,definition,(
% 8.96/2.60 sQ614_spl <=> (l1_group_1(sK1495_skl))),
% 8.96/2.60 introduced(definition,[new_symbols(definition,[sQ614_spl])],[split_symbol_definition])).
% 8.96/2.60 fof(f27088,plain,(
% 8.96/2.60 ~l1_group_1(sK1495_skl)|sQ614_spl),
% 8.96/2.60 inference(component_clause,[status(thm)],[f27086])).
% 8.96/2.60 fof(f27090,definition,(
% 8.96/2.60 sQ615_spl <=> (v3_struct_0(sK1496_skl))),
% 8.96/2.60 introduced(definition,[new_symbols(definition,[sQ615_spl])],[split_symbol_definition])).
% 8.96/2.60 fof(f27093,plain,(
% 8.96/2.60 sQ609_spl|~sQ611_spl|~sQ614_spl|~sQ615_spl),
% 8.96/2.60 inference(split_clause,[status(thm)],[f27085,f27060,f27070,f27086,f27090])).
% 8.96/2.60 fof(f27094,plain,(
% 8.96/2.60 $false|sQ614_spl),
% 8.96/2.60 inference(forward_subsumption_resolution,[status(thm)],[f27088,f22090])).
% 8.96/2.60 fof(f27095,plain,(
% 8.96/2.60 sQ614_spl),
% 8.96/2.60 inference(contradiction_clause,[status(thm)],[f27094])).
% 8.96/2.60 fof(f27169,plain,(
% 8.96/2.60 v3_struct_0(sK1495_skl)|~v3_group_1(sK1495_skl)|~l1_group_1(sK1495_skl)|v3_group_1(sK1496_skl)),
% 8.96/2.60 inference(resolution,[status(thm)],[f18199,f22092])).
% 8.96/2.60 fof(f27171,definition,(
% 8.96/2.60 sQ616_spl <=> (v3_group_1(sK1496_skl))),
% 8.96/2.60 introduced(definition,[new_symbols(definition,[sQ616_spl])],[split_symbol_definition])).
% 8.96/2.60 fof(f27174,plain,(
% 8.96/2.60 sQ609_spl|~sQ611_spl|~sQ614_spl|sQ616_spl),
% 8.96/2.60 inference(split_clause,[status(thm)],[f27169,f27060,f27070,f27086,f27171])).
% 8.96/2.60 fof(f27176,plain,(
% 8.96/2.60 v3_struct_0(sK1495_skl)|~v3_group_1(sK1495_skl)|~l1_group_1(sK1495_skl)|l1_group_1(sK1496_skl)),
% 8.96/2.60 inference(resolution,[status(thm)],[f18200,f22092])).
% 8.96/2.60 fof(f27178,definition,(
% 8.96/2.60 sQ617_spl <=> (l1_group_1(sK1496_skl))),
% 8.96/2.60 introduced(definition,[new_symbols(definition,[sQ617_spl])],[split_symbol_definition])).
% 8.96/2.60 fof(f27179,plain,(
% 8.96/2.60 l1_group_1(sK1496_skl)|~sQ617_spl),
% 8.96/2.60 inference(component_clause,[status(thm)],[f27178])).
% 8.96/2.60 fof(f27181,plain,(
% 8.96/2.60 sQ609_spl|~sQ611_spl|~sQ614_spl|sQ617_spl),
% 8.96/2.60 inference(split_clause,[status(thm)],[f27176,f27060,f27070,f27086,f27178])).
% 8.96/2.60 fof(f27182,plain,(
% 8.96/2.60 v3_struct_0(sK1496_skl)|~v3_group_1(sK1496_skl)|~v4_group_1(sK1496_skl)|m1_group_2(sK1496_skl,sK1496_skl)|~sQ617_spl),
% 8.96/2.60 inference(resolution,[status(thm)],[f27179,f17833])).
% 8.96/2.60 fof(f27184,definition,(
% 8.96/2.60 sQ618_spl <=> (v4_group_1(sK1496_skl))),
% 8.96/2.60 introduced(definition,[new_symbols(definition,[sQ618_spl])],[split_symbol_definition])).
% 8.96/2.60 fof(f27187,definition,(
% 8.96/2.60 sQ619_spl <=> (m1_group_2(sK1496_skl,sK1496_skl))),
% 8.96/2.60 introduced(definition,[new_symbols(definition,[sQ619_spl])],[split_symbol_definition])).
% 8.96/2.60 fof(f27188,plain,(
% 8.96/2.60 m1_group_2(sK1496_skl,sK1496_skl)|~sQ619_spl),
% 8.96/2.60 inference(component_clause,[status(thm)],[f27187])).
% 8.96/2.60 fof(f27190,plain,(
% 8.96/2.60 sQ615_spl|~sQ616_spl|~sQ618_spl|sQ619_spl|~sQ617_spl),
% 8.96/2.60 inference(split_clause,[status(thm)],[f27182,f27090,f27171,f27184,f27187,f27178])).
% 8.96/2.60 fof(f27344,plain,(
% 8.96/2.60 v3_struct_0(sK1495_skl)|~v3_group_1(sK1495_skl)|~v4_group_1(sK1495_skl)|~l1_group_1(sK1495_skl)|v4_group_1(sK1496_skl)),
% 8.96/2.60 inference(resolution,[status(thm)],[f17650,f22092])).
% 8.96/2.60 fof(f27347,plain,(
% 8.96/2.60 sQ609_spl|~sQ611_spl|~sQ612_spl|~sQ614_spl|sQ618_spl),
% 8.96/2.60 inference(split_clause,[status(thm)],[f27344,f27060,f27070,f27073,f27086,f27184])).
% 8.96/2.60 fof(f27449,plain,(
% 8.96/2.60 v3_struct_0(sK1495_skl)|~v3_group_1(sK1495_skl)|~v4_group_1(sK1495_skl)|~l1_group_1(sK1495_skl)|k2_group_1(sK1496_skl)=k2_group_1(sK1495_skl)),
% 8.96/2.60 inference(resolution,[status(thm)],[f17807,f22092])).
% 8.96/2.60 fof(f27458,definition,(
% 8.96/2.60 sQ626_spl <=> (k2_group_1(sK1496_skl)=k2_group_1(sK1495_skl))),
% 8.96/2.60 introduced(definition,[new_symbols(definition,[sQ626_spl])],[split_symbol_definition])).
% 8.96/2.60 fof(f27459,plain,(
% 8.96/2.60 k2_group_1(sK1496_skl)=k2_group_1(sK1495_skl)|~sQ626_spl),
% 8.96/2.60 inference(component_clause,[status(thm)],[f27458])).
% 8.96/2.60 fof(f27461,plain,(
% 8.96/2.60 sQ609_spl|~sQ611_spl|~sQ612_spl|~sQ614_spl|sQ626_spl),
% 8.96/2.60 inference(split_clause,[status(thm)],[f27449,f27060,f27070,f27073,f27086,f27458])).
% 8.96/2.60 fof(f27498,plain,(
% 8.96/2.60 ~r2_hidden(k2_group_1(sK1496_skl),k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl))|~sQ626_spl),
% 8.96/2.60 inference(backward_demodulation,[status(thm)],[f27459,f22093])).
% 8.96/2.60 fof(f27499,plain,(
% 8.96/2.60 m1_subset_1(k2_group_1(sK1496_skl),u1_struct_0(sK1495_skl))|~sQ626_spl|~sQ610_spl),
% 8.96/2.60 inference(backward_demodulation,[status(thm)],[f27459,f27064])).
% 8.96/2.60 fof(f27534,plain,(
% 8.96/2.60 v3_struct_0(sK1496_skl)|~v3_group_1(sK1496_skl)|~v4_group_1(sK1496_skl)|~l1_group_1(sK1496_skl)|r1_rlvect_1(sK1496_skl,k2_group_1(sK1496_skl))|~sQ619_spl),
% 8.96/2.60 inference(resolution,[status(thm)],[f17811,f27188])).
% 8.96/2.60 fof(f27540,definition,(
% 8.96/2.60 sQ632_spl <=> (r1_rlvect_1(sK1496_skl,k2_group_1(sK1496_skl)))),
% 8.96/2.60 introduced(definition,[new_symbols(definition,[sQ632_spl])],[split_symbol_definition])).
% 8.96/2.60 fof(f27543,plain,(
% 8.96/2.60 sQ615_spl|~sQ616_spl|~sQ618_spl|~sQ617_spl|sQ632_spl|~sQ619_spl),
% 8.96/2.60 inference(split_clause,[status(thm)],[f27534,f27090,f27171,f27184,f27178,f27540,f27187])).
% 8.96/2.60 fof(f28187,plain,(
% 8.96/2.60 v3_struct_0(sK1495_skl)|~v3_group_1(sK1495_skl)|~v4_group_1(sK1495_skl)|v1_funct_2(k1_latsubgr(sK1495_skl),k1_group_3(sK1495_skl),k1_zfmisc_1(u1_struct_0(sK1495_skl)))),
% 8.96/2.60 inference(resolution,[status(thm)],[f22028,f22090])).
% 8.96/2.60 fof(f28192,definition,(
% 8.96/2.60 sQ672_spl <=> (v1_funct_2(k1_latsubgr(sK1495_skl),k1_group_3(sK1495_skl),k1_zfmisc_1(u1_struct_0(sK1495_skl))))),
% 8.96/2.60 introduced(definition,[new_symbols(definition,[sQ672_spl])],[split_symbol_definition])).
% 8.96/2.60 fof(f28195,plain,(
% 8.96/2.60 sQ609_spl|~sQ611_spl|~sQ612_spl|sQ672_spl),
% 8.96/2.60 inference(split_clause,[status(thm)],[f28187,f27060,f27070,f27073,f28192])).
% 8.96/2.60 fof(f28197,plain,(
% 8.96/2.60 v3_struct_0(sK1495_skl)|~v3_group_1(sK1495_skl)|~v4_group_1(sK1495_skl)|m2_relset_1(k1_latsubgr(sK1495_skl),k1_group_3(sK1495_skl),k1_zfmisc_1(u1_struct_0(sK1495_skl)))),
% 8.96/2.60 inference(resolution,[status(thm)],[f22029,f22090])).
% 8.96/2.60 fof(f28202,definition,(
% 8.96/2.60 sQ674_spl <=> (m2_relset_1(k1_latsubgr(sK1495_skl),k1_group_3(sK1495_skl),k1_zfmisc_1(u1_struct_0(sK1495_skl))))),
% 8.96/2.60 introduced(definition,[new_symbols(definition,[sQ674_spl])],[split_symbol_definition])).
% 8.96/2.60 fof(f28203,plain,(
% 8.96/2.60 m2_relset_1(k1_latsubgr(sK1495_skl),k1_group_3(sK1495_skl),k1_zfmisc_1(u1_struct_0(sK1495_skl)))|~sQ674_spl),
% 8.96/2.60 inference(component_clause,[status(thm)],[f28202])).
% 8.96/2.60 fof(f28205,plain,(
% 8.96/2.60 sQ609_spl|~sQ611_spl|~sQ612_spl|sQ674_spl),
% 8.96/2.60 inference(split_clause,[status(thm)],[f28197,f27060,f27070,f27073,f28202])).
% 8.96/2.60 fof(f28247,plain,(
% 8.96/2.60 ![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))),
% 8.96/2.60 inference(forward_subsumption_resolution,[status(thm)],[f26883,f22027])).
% 8.96/2.60 fof(f28252,definition,(
% 8.96/2.60 ![X0]: (sQ683_spl <=> (~v1_group_1(X0)|~m1_group_2(X0,sK1495_skl)|k1_funct_1(k1_latsubgr(sK1495_skl),X0)=u1_struct_0(X0)))),
% 8.96/2.60 introduced(definition,[new_symbols(definition,[sQ683_spl])],[split_symbol_definition])).
% 8.96/2.60 fof(f28253,plain,(
% 8.96/2.60 ![X0]: (~v1_group_1(X0)|~m1_group_2(X0,sK1495_skl)|k1_funct_1(k1_latsubgr(sK1495_skl),X0)=u1_struct_0(X0)|~sQ683_spl)),
% 8.96/2.60 inference(component_clause,[status(thm)],[f28252])).
% 8.96/2.60 fof(f28275,plain,(
% 8.96/2.60 ![X0]: (v3_struct_0(sK1495_skl)|~v3_group_1(sK1495_skl)|~v4_group_1(sK1495_skl)|~l1_group_1(sK1495_skl)|~v1_funct_2(k1_latsubgr(sK1495_skl),k1_group_3(sK1495_skl),k1_zfmisc_1(u1_struct_0(sK1495_skl)))|~v1_group_1(X0)|~m1_group_2(X0,sK1495_skl)|k1_funct_1(k1_latsubgr(sK1495_skl),X0)=u1_struct_0(X0)|~sQ674_spl)),
% 8.96/2.60 inference(resolution,[status(thm)],[f28203,f28247])).
% 8.96/2.60 fof(f28277,plain,(
% 8.96/2.60 sQ609_spl|~sQ611_spl|~sQ612_spl|~sQ614_spl|~sQ672_spl|sQ683_spl|~sQ674_spl),
% 8.96/2.60 inference(split_clause,[status(thm)],[f28275,f27060,f27070,f27073,f27086,f28192,f28252,f28202])).
% 8.96/2.60 fof(f28287,plain,(
% 8.96/2.60 ![X0]: (v3_struct_0(sK1495_skl)|~v3_group_1(sK1495_skl)|~v4_group_1(sK1495_skl)|~l1_group_1(sK1495_skl)|~v1_group_1(sK1496_skl)|~m1_subset_1(X0,u1_struct_0(sK1495_skl))|r2_hidden(X0,k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl))|~r1_rlvect_1(sK1496_skl,X0))),
% 8.96/2.60 inference(resolution,[status(thm)],[f22084,f22092])).
% 8.96/2.60 fof(f28296,definition,(
% 8.96/2.60 sQ687_spl <=> (v1_group_1(sK1496_skl))),
% 8.96/2.60 introduced(definition,[new_symbols(definition,[sQ687_spl])],[split_symbol_definition])).
% 8.96/2.60 fof(f28298,plain,(
% 8.96/2.60 ~v1_group_1(sK1496_skl)|sQ687_spl),
% 8.96/2.60 inference(component_clause,[status(thm)],[f28296])).
% 8.96/2.60 fof(f28303,definition,(
% 8.96/2.60 ![X0]: (sQ689_spl <=> (~m1_subset_1(X0,u1_struct_0(sK1495_skl))|r2_hidden(X0,k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl))|~r1_rlvect_1(sK1496_skl,X0)))),
% 8.96/2.60 introduced(definition,[new_symbols(definition,[sQ689_spl])],[split_symbol_definition])).
% 8.96/2.60 fof(f28304,plain,(
% 8.96/2.60 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1495_skl))|r2_hidden(X0,k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl))|~r1_rlvect_1(sK1496_skl,X0)|~sQ689_spl)),
% 8.96/2.60 inference(component_clause,[status(thm)],[f28303])).
% 8.96/2.60 fof(f28306,plain,(
% 8.96/2.60 sQ609_spl|~sQ611_spl|~sQ612_spl|~sQ614_spl|~sQ687_spl|sQ689_spl),
% 8.96/2.60 inference(split_clause,[status(thm)],[f28287,f27060,f27070,f27073,f27086,f28296,f28303])).
% 8.96/2.60 fof(f28309,plain,(
% 8.96/2.60 $false|sQ687_spl),
% 8.96/2.60 inference(forward_subsumption_resolution,[status(thm)],[f28298,f22091])).
% 8.96/2.60 fof(f28310,plain,(
% 8.96/2.60 sQ687_spl),
% 8.96/2.60 inference(contradiction_clause,[status(thm)],[f28309])).
% 8.96/2.60 fof(f28403,plain,(
% 8.96/2.60 ~v1_group_1(sK1496_skl)|k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl)=u1_struct_0(sK1496_skl)|~sQ683_spl),
% 8.96/2.60 inference(resolution,[status(thm)],[f28253,f22092])).
% 8.96/2.60 fof(f28409,definition,(
% 8.96/2.60 sQ693_spl <=> (k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl)=u1_struct_0(sK1496_skl))),
% 8.96/2.60 introduced(definition,[new_symbols(definition,[sQ693_spl])],[split_symbol_definition])).
% 8.96/2.60 fof(f28410,plain,(
% 8.96/2.60 k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl)=u1_struct_0(sK1496_skl)|~sQ693_spl),
% 8.96/2.60 inference(component_clause,[status(thm)],[f28409])).
% 8.96/2.60 fof(f28412,plain,(
% 8.96/2.60 ~sQ687_spl|sQ693_spl|~sQ683_spl),
% 8.96/2.60 inference(split_clause,[status(thm)],[f28403,f28296,f28409,f28252])).
% 8.96/2.60 fof(f28419,plain,(
% 8.96/2.60 ~r2_hidden(k2_group_1(sK1496_skl),u1_struct_0(sK1496_skl))|~sQ693_spl|~sQ626_spl),
% 8.96/2.60 inference(backward_demodulation,[status(thm)],[f28410,f27498])).
% 8.96/2.60 fof(f28426,plain,(
% 8.96/2.60 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK1495_skl))|r2_hidden(X0,u1_struct_0(sK1496_skl))|~r1_rlvect_1(sK1496_skl,X0)|~sQ693_spl|~sQ689_spl)),
% 8.96/2.60 inference(forward_demodulation,[status(thm)],[f28410,f28304])).
% 8.96/2.60 fof(f28430,plain,(
% 8.96/2.60 r2_hidden(k2_group_1(sK1496_skl),u1_struct_0(sK1496_skl))|~r1_rlvect_1(sK1496_skl,k2_group_1(sK1496_skl))|~sQ693_spl|~sQ689_spl|~sQ626_spl|~sQ610_spl),
% 8.96/2.60 inference(resolution,[status(thm)],[f28426,f27499])).
% 8.96/2.60 fof(f28431,definition,(
% 8.96/2.60 sQ696_spl <=> (r2_hidden(k2_group_1(sK1496_skl),u1_struct_0(sK1496_skl)))),
% 8.96/2.60 introduced(definition,[new_symbols(definition,[sQ696_spl])],[split_symbol_definition])).
% 8.96/2.60 fof(f28432,plain,(
% 8.96/2.60 r2_hidden(k2_group_1(sK1496_skl),u1_struct_0(sK1496_skl))|~sQ696_spl),
% 8.96/2.60 inference(component_clause,[status(thm)],[f28431])).
% 8.96/2.60 fof(f28434,plain,(
% 8.96/2.60 sQ696_spl|~sQ632_spl|~sQ693_spl|~sQ689_spl|~sQ626_spl|~sQ610_spl),
% 8.96/2.60 inference(split_clause,[status(thm)],[f28430,f28431,f27540,f28409,f28303,f27458,f27063])).
% 8.96/2.60 fof(f28435,plain,(
% 8.96/2.60 $false|~sQ693_spl|~sQ626_spl|~sQ696_spl),
% 8.96/2.60 inference(forward_subsumption_resolution,[status(thm)],[f28432,f28419])).
% 8.96/2.60 fof(f28436,plain,(
% 8.96/2.60 ~sQ693_spl|~sQ626_spl|~sQ696_spl),
% 6.73/2.74 inference(contradiction_clause,[status(thm)],[f28435])).
% 6.73/2.74 fof(f28437,plain,(
% 6.73/2.74 $false),
% 6.73/2.74 inference(sat_refutation,[status(thm)],[f27066,f27068,f27081,f27083,f27093,f27095,f27174,f27181,f27190,f27347,f27461,f27543,f28195,f28205,f28277,f28306,f28310,f28412,f28434,f28436])).
% 6.73/2.74 % SZS output end CNFRefutation for theBenchmark.p
% 6.73/2.78 % Elapsed time: 2.059671 seconds
% 6.73/2.78 % CPU time: 9.724244 seconds
% 6.73/2.78 % Total memory used: 1.014 GB
% 6.73/2.78 % Net memory used: 1.001 GB
%------------------------------------------------------------------------------