%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP644+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 : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:37:01 PM UTC 2026
% Result : Theorem 156.36s 21.05s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP644+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n018.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Sun Sep 20 20:27:59 UTC 2026
% 0.17/0.44 % CPUTime :
% 1.00/1.39 % Drodi V4.1.1
% 156.36/21.05 % Refutation found
% 156.36/21.05 % SZS status Theorem for theBenchmark: Theorem is valid
% 156.36/21.05 % SZS output start CNFRefutation for theBenchmark
% 156.36/21.05 fof(f3813,axiom,(
% 156.36/21.05 (! [A,B] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A)& m1_subset_1(B,u1_struct_0(A)) )=> m1_subset_1(k3_group_1(A,B),u1_struct_0(A)) ) )),
% 156.36/21.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 156.36/21.05 fof(f4404,axiom,(
% 156.36/21.05 (! [A] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> (! [C] :( m1_group_2(C,A)=> ( r1_rlvect_1(C,B)=> r1_rlvect_1(C,k3_group_1(A,B)) ) ) )) )) )),
% 156.36/21.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 156.36/21.05 fof(f5657,axiom,(
% 156.36/21.05 (! [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) ) ) )) )) )),
% 156.36/21.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 156.36/21.05 fof(f5661,conjecture,(
% 156.36/21.05 (! [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))=> r2_hidden(k3_group_1(A,C),k1_funct_1(k1_latsubgr(A),B)) ) ) )) )) )),
% 156.36/21.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 156.36/21.05 fof(f5662,negated_conjecture,(
% 156.36/21.05 ~((! [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))=> r2_hidden(k3_group_1(A,C),k1_funct_1(k1_latsubgr(A),B)) ) ) )) )) ))),
% 156.36/21.05 inference(negated_conjecture,[status(cth)],[f5661])).
% 156.36/21.05 fof(f16376,plain,(
% 156.36/21.05 ![A,B]: (((((v3_struct_0(A)|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|~m1_subset_1(B,u1_struct_0(A)))|m1_subset_1(k3_group_1(A,B),u1_struct_0(A)))),
% 156.36/21.05 inference(pre_NNF_transformation,[status(thm)],[f3813])).
% 156.36/21.05 fof(f16377,plain,(
% 156.36/21.05 ![X0,X1]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m1_subset_1(X1,u1_struct_0(X0))|m1_subset_1(k3_group_1(X0,X1),u1_struct_0(X0)))),
% 156.36/21.05 inference(cnf_transformation,[status(thm)],[f16376])).
% 156.36/21.05 fof(f17823,plain,(
% 156.36/21.05 ![A]: ((((v3_struct_0(A)|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|(![B]: (~m1_subset_1(B,u1_struct_0(A))|(![C]: (~m1_group_2(C,A)|(~r1_rlvect_1(C,B)|r1_rlvect_1(C,k3_group_1(A,B))))))))),
% 156.36/21.05 inference(pre_NNF_transformation,[status(thm)],[f4404])).
% 156.36/21.05 fof(f17824,plain,(
% 156.36/21.05 ![X0,X1,X2]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m1_subset_1(X1,u1_struct_0(X0))|~m1_group_2(X2,X0)|~r1_rlvect_1(X2,X1)|r1_rlvect_1(X2,k3_group_1(X0,X1)))),
% 156.36/21.05 inference(cnf_transformation,[status(thm)],[f17823])).
% 156.36/21.05 fof(f22084,plain,(
% 156.36/21.05 ![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)))))))),
% 156.36/21.05 inference(pre_NNF_transformation,[status(thm)],[f5657])).
% 156.36/21.05 fof(f22085,plain,(
% 156.36/21.05 ![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))))))))),
% 156.36/21.05 inference(NNF_transformation,[status(thm)],[f22084])).
% 156.36/21.05 fof(f22086,plain,(
% 156.36/21.05 ![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))),
% 156.36/21.05 inference(cnf_transformation,[status(thm)],[f22085])).
% 156.36/21.05 fof(f22087,plain,(
% 156.36/21.05 ![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))),
% 156.36/21.05 inference(cnf_transformation,[status(thm)],[f22085])).
% 156.36/21.05 fof(f22094,plain,(
% 156.36/21.05 (?[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))&~r2_hidden(k3_group_1(A,C),k1_funct_1(k1_latsubgr(A),B)))))))))),
% 156.36/21.05 inference(pre_NNF_transformation,[status(thm)],[f5662])).
% 156.36/21.05 fof(f22095,plain,(
% 156.36/21.05 ((((~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))&(m1_subset_1(sK1497_skl,u1_struct_0(sK1495_skl))&(r2_hidden(sK1497_skl,k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl))&~r2_hidden(k3_group_1(sK1495_skl,sK1497_skl),k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl))))))),
% 156.36/21.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK1495_skl,sK1496_skl,sK1497_skl]),skolemize(A,sK1495_skl),skolemize(B,sK1496_skl),skolemize(C,sK1497_skl)],[f22094])).
% 156.36/21.05 fof(f22096,plain,(
% 156.36/21.05 ~v3_struct_0(sK1495_skl)),
% 156.36/21.05 inference(cnf_transformation,[status(thm)],[f22095])).
% 156.36/21.05 fof(f22097,plain,(
% 156.36/21.05 v3_group_1(sK1495_skl)),
% 156.36/21.05 inference(cnf_transformation,[status(thm)],[f22095])).
% 156.36/21.05 fof(f22098,plain,(
% 156.36/21.05 v4_group_1(sK1495_skl)),
% 156.36/21.05 inference(cnf_transformation,[status(thm)],[f22095])).
% 156.36/21.05 fof(f22099,plain,(
% 156.36/21.05 l1_group_1(sK1495_skl)),
% 156.36/21.05 inference(cnf_transformation,[status(thm)],[f22095])).
% 156.36/21.05 fof(f22100,plain,(
% 156.36/21.05 v1_group_1(sK1496_skl)),
% 156.36/21.05 inference(cnf_transformation,[status(thm)],[f22095])).
% 156.36/21.05 fof(f22101,plain,(
% 156.36/21.05 m1_group_2(sK1496_skl,sK1495_skl)),
% 156.36/21.05 inference(cnf_transformation,[status(thm)],[f22095])).
% 156.36/21.05 fof(f22102,plain,(
% 156.36/21.05 m1_subset_1(sK1497_skl,u1_struct_0(sK1495_skl))),
% 156.36/21.05 inference(cnf_transformation,[status(thm)],[f22095])).
% 156.36/21.05 fof(f22103,plain,(
% 156.36/21.05 r2_hidden(sK1497_skl,k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl))),
% 156.36/21.05 inference(cnf_transformation,[status(thm)],[f22095])).
% 156.36/21.05 fof(f22104,plain,(
% 156.36/21.05 ~r2_hidden(k3_group_1(sK1495_skl,sK1497_skl),k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl))),
% 156.36/21.05 inference(cnf_transformation,[status(thm)],[f22095])).
% 156.36/21.05 fof(f27216,definition,(
% 156.36/21.05 sQ612_spl <=> (v3_struct_0(sK1495_skl))),
% 156.36/21.05 introduced(definition,[new_symbols(definition,[sQ612_spl])],[split_symbol_definition])).
% 156.36/21.05 fof(f27217,plain,(
% 156.36/21.05 v3_struct_0(sK1495_skl)|~sQ612_spl),
% 156.36/21.05 inference(component_clause,[status(thm)],[f27216])).
% 156.36/21.05 fof(f27219,definition,(
% 156.36/21.05 sQ613_spl <=> (v3_group_1(sK1495_skl))),
% 156.36/21.05 introduced(definition,[new_symbols(definition,[sQ613_spl])],[split_symbol_definition])).
% 156.36/21.05 fof(f27221,plain,(
% 156.36/21.05 ~v3_group_1(sK1495_skl)|sQ613_spl),
% 156.36/21.05 inference(component_clause,[status(thm)],[f27219])).
% 156.36/21.05 fof(f27222,definition,(
% 156.36/21.05 sQ614_spl <=> (v4_group_1(sK1495_skl))),
% 156.36/21.05 introduced(definition,[new_symbols(definition,[sQ614_spl])],[split_symbol_definition])).
% 156.36/21.05 fof(f27224,plain,(
% 156.36/21.05 ~v4_group_1(sK1495_skl)|sQ614_spl),
% 156.36/21.05 inference(component_clause,[status(thm)],[f27222])).
% 156.36/21.05 fof(f27225,definition,(
% 156.36/21.05 sQ615_spl <=> (l1_group_1(sK1495_skl))),
% 156.36/21.05 introduced(definition,[new_symbols(definition,[sQ615_spl])],[split_symbol_definition])).
% 156.36/21.05 fof(f27227,plain,(
% 156.36/21.05 ~l1_group_1(sK1495_skl)|sQ615_spl),
% 156.36/21.05 inference(component_clause,[status(thm)],[f27225])).
% 156.36/21.05 fof(f27232,plain,(
% 156.36/21.05 $false|sQ615_spl),
% 156.36/21.05 inference(forward_subsumption_resolution,[status(thm)],[f27227,f22099])).
% 156.36/21.05 fof(f27233,plain,(
% 156.36/21.05 sQ615_spl),
% 156.36/21.05 inference(contradiction_clause,[status(thm)],[f27232])).
% 156.36/21.05 fof(f27234,plain,(
% 156.36/21.05 $false|sQ614_spl),
% 156.36/21.05 inference(forward_subsumption_resolution,[status(thm)],[f27224,f22098])).
% 156.36/21.05 fof(f27235,plain,(
% 156.36/21.05 sQ614_spl),
% 156.36/21.05 inference(contradiction_clause,[status(thm)],[f27234])).
% 156.36/21.05 fof(f27236,plain,(
% 156.36/21.05 $false|sQ613_spl),
% 156.36/21.05 inference(forward_subsumption_resolution,[status(thm)],[f27221,f22097])).
% 156.36/21.05 fof(f27237,plain,(
% 156.36/21.05 sQ613_spl),
% 156.36/21.05 inference(contradiction_clause,[status(thm)],[f27236])).
% 156.36/21.05 fof(f27238,plain,(
% 156.36/21.05 $false|~sQ612_spl),
% 156.36/21.05 inference(forward_subsumption_resolution,[status(thm)],[f27217,f22096])).
% 156.36/21.05 fof(f27239,plain,(
% 156.36/21.05 ~sQ612_spl),
% 156.36/21.05 inference(contradiction_clause,[status(thm)],[f27238])).
% 156.36/21.05 fof(f27242,plain,(
% 156.36/21.05 v3_struct_0(sK1495_skl)|~v3_group_1(sK1495_skl)|~v4_group_1(sK1495_skl)|~l1_group_1(sK1495_skl)|m1_subset_1(k3_group_1(sK1495_skl,sK1497_skl),u1_struct_0(sK1495_skl))),
% 156.36/21.05 inference(resolution,[status(thm)],[f16377,f22102])).
% 156.36/21.05 fof(f27243,definition,(
% 156.36/21.05 sQ617_spl <=> (m1_subset_1(k3_group_1(sK1495_skl,sK1497_skl),u1_struct_0(sK1495_skl)))),
% 156.36/21.05 introduced(definition,[new_symbols(definition,[sQ617_spl])],[split_symbol_definition])).
% 156.36/21.05 fof(f27244,plain,(
% 156.36/21.05 m1_subset_1(k3_group_1(sK1495_skl,sK1497_skl),u1_struct_0(sK1495_skl))|~sQ617_spl),
% 156.36/21.05 inference(component_clause,[status(thm)],[f27243])).
% 156.36/21.05 fof(f27246,plain,(
% 156.36/21.05 sQ612_spl|~sQ613_spl|~sQ614_spl|~sQ615_spl|sQ617_spl),
% 156.36/21.05 inference(split_clause,[status(thm)],[f27242,f27216,f27219,f27222,f27225,f27243])).
% 156.36/21.05 fof(f27702,definition,(
% 156.36/21.05 sQ636_spl <=> (v1_group_1(sK1496_skl))),
% 156.36/21.05 introduced(definition,[new_symbols(definition,[sQ636_spl])],[split_symbol_definition])).
% 156.36/21.05 fof(f27704,plain,(
% 156.36/21.05 ~v1_group_1(sK1496_skl)|sQ636_spl),
% 156.36/21.05 inference(component_clause,[status(thm)],[f27702])).
% 156.36/21.05 fof(f27709,plain,(
% 156.36/21.05 $false|sQ636_spl),
% 156.36/21.05 inference(forward_subsumption_resolution,[status(thm)],[f27704,f22100])).
% 156.36/21.05 fof(f27710,plain,(
% 156.36/21.05 sQ636_spl),
% 156.36/21.05 inference(contradiction_clause,[status(thm)],[f27709])).
% 156.36/21.05 fof(f27718,definition,(
% 156.36/21.05 sQ638_spl <=> (m1_group_2(sK1496_skl,sK1495_skl))),
% 156.36/21.05 introduced(definition,[new_symbols(definition,[sQ638_spl])],[split_symbol_definition])).
% 156.36/21.05 fof(f27720,plain,(
% 156.36/21.05 ~m1_group_2(sK1496_skl,sK1495_skl)|sQ638_spl),
% 156.36/21.05 inference(component_clause,[status(thm)],[f27718])).
% 156.36/21.05 fof(f27728,definition,(
% 156.36/21.05 sQ641_spl <=> (m1_subset_1(sK1497_skl,u1_struct_0(sK1495_skl)))),
% 156.36/21.05 introduced(definition,[new_symbols(definition,[sQ641_spl])],[split_symbol_definition])).
% 156.36/21.05 fof(f27730,plain,(
% 156.36/21.05 ~m1_subset_1(sK1497_skl,u1_struct_0(sK1495_skl))|sQ641_spl),
% 156.36/21.05 inference(component_clause,[status(thm)],[f27728])).
% 156.36/21.05 fof(f27735,plain,(
% 156.36/21.05 $false|sQ638_spl),
% 156.36/21.05 inference(forward_subsumption_resolution,[status(thm)],[f27720,f22101])).
% 156.36/21.05 fof(f27736,plain,(
% 156.36/21.05 sQ638_spl),
% 156.36/21.05 inference(contradiction_clause,[status(thm)],[f27735])).
% 156.36/21.05 fof(f27737,plain,(
% 156.36/21.05 $false|sQ641_spl),
% 156.36/21.05 inference(forward_subsumption_resolution,[status(thm)],[f27730,f22102])).
% 156.36/21.05 fof(f27738,plain,(
% 156.36/21.05 sQ641_spl),
% 156.36/21.05 inference(contradiction_clause,[status(thm)],[f27737])).
% 156.36/21.05 fof(f30399,plain,(
% 156.36/21.05 ![X0]: (v3_struct_0(sK1495_skl)|~v3_group_1(sK1495_skl)|~v4_group_1(sK1495_skl)|~l1_group_1(sK1495_skl)|~m1_group_2(X0,sK1495_skl)|~r1_rlvect_1(X0,sK1497_skl)|r1_rlvect_1(X0,k3_group_1(sK1495_skl,sK1497_skl)))),
% 156.36/21.05 inference(resolution,[status(thm)],[f17824,f22102])).
% 156.36/21.05 fof(f30404,definition,(
% 156.36/21.05 ![X0]: (sQ722_spl <=> (~m1_group_2(X0,sK1495_skl)|~r1_rlvect_1(X0,sK1497_skl)|r1_rlvect_1(X0,k3_group_1(sK1495_skl,sK1497_skl))))),
% 156.36/21.05 introduced(definition,[new_symbols(definition,[sQ722_spl])],[split_symbol_definition])).
% 156.36/21.05 fof(f30405,plain,(
% 156.36/21.05 ![X0]: (~m1_group_2(X0,sK1495_skl)|~r1_rlvect_1(X0,sK1497_skl)|r1_rlvect_1(X0,k3_group_1(sK1495_skl,sK1497_skl))|~sQ722_spl)),
% 156.36/21.05 inference(component_clause,[status(thm)],[f30404])).
% 156.36/21.05 fof(f30407,plain,(
% 156.36/21.05 sQ612_spl|~sQ613_spl|~sQ614_spl|~sQ615_spl|sQ722_spl),
% 156.36/21.05 inference(split_clause,[status(thm)],[f30399,f27216,f27219,f27222,f27225,f30404])).
% 156.36/21.05 fof(f31168,plain,(
% 156.36/21.05 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)|~m1_subset_1(sK1497_skl,u1_struct_0(sK1495_skl))|r1_rlvect_1(sK1496_skl,sK1497_skl)),
% 156.36/21.05 inference(resolution,[status(thm)],[f22086,f22103])).
% 156.36/21.05 fof(f31177,definition,(
% 156.36/21.05 sQ761_spl <=> (r1_rlvect_1(sK1496_skl,sK1497_skl))),
% 156.36/21.05 introduced(definition,[new_symbols(definition,[sQ761_spl])],[split_symbol_definition])).
% 156.36/21.05 fof(f31180,plain,(
% 156.36/21.05 sQ612_spl|~sQ613_spl|~sQ614_spl|~sQ615_spl|~sQ636_spl|~sQ638_spl|~sQ641_spl|sQ761_spl),
% 156.36/21.05 inference(split_clause,[status(thm)],[f31168,f27216,f27219,f27222,f27225,f27702,f27718,f27728,f31177])).
% 156.36/21.05 fof(f31324,plain,(
% 156.36/21.05 ![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))),
% 156.36/21.05 inference(resolution,[status(thm)],[f22087,f22101])).
% 156.36/21.05 fof(f31333,definition,(
% 156.36/21.05 ![X0]: (sQ769_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)))),
% 157.16/21.22 introduced(definition,[new_symbols(definition,[sQ769_spl])],[split_symbol_definition])).
% 157.16/21.22 fof(f31334,plain,(
% 157.16/21.22 ![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)|~sQ769_spl)),
% 157.16/21.22 inference(component_clause,[status(thm)],[f31333])).
% 157.16/21.22 fof(f31336,plain,(
% 157.16/21.22 sQ612_spl|~sQ613_spl|~sQ614_spl|~sQ615_spl|~sQ636_spl|sQ769_spl),
% 157.16/21.22 inference(split_clause,[status(thm)],[f31324,f27216,f27219,f27222,f27225,f27702,f31333])).
% 157.16/21.22 fof(f45375,plain,(
% 157.16/21.22 ~r1_rlvect_1(sK1496_skl,sK1497_skl)|r1_rlvect_1(sK1496_skl,k3_group_1(sK1495_skl,sK1497_skl))|~sQ722_spl),
% 157.16/21.22 inference(resolution,[status(thm)],[f30405,f22101])).
% 157.16/21.22 fof(f45383,definition,(
% 157.16/21.22 sQ1649_spl <=> (r1_rlvect_1(sK1496_skl,k3_group_1(sK1495_skl,sK1497_skl)))),
% 157.16/21.22 introduced(definition,[new_symbols(definition,[sQ1649_spl])],[split_symbol_definition])).
% 157.16/21.22 fof(f45386,plain,(
% 157.16/21.22 ~sQ761_spl|sQ1649_spl|~sQ722_spl),
% 157.16/21.22 inference(split_clause,[status(thm)],[f45375,f31177,f45383,f30404])).
% 157.16/21.22 fof(f48447,plain,(
% 157.16/21.22 r2_hidden(k3_group_1(sK1495_skl,sK1497_skl),k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl))|~r1_rlvect_1(sK1496_skl,k3_group_1(sK1495_skl,sK1497_skl))|~sQ769_spl|~sQ617_spl),
% 157.16/21.22 inference(resolution,[status(thm)],[f31334,f27244])).
% 157.16/21.22 fof(f48456,definition,(
% 157.16/21.22 sQ1696_spl <=> (r2_hidden(k3_group_1(sK1495_skl,sK1497_skl),k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl)))),
% 157.16/21.22 introduced(definition,[new_symbols(definition,[sQ1696_spl])],[split_symbol_definition])).
% 157.16/21.22 fof(f48457,plain,(
% 157.16/21.22 r2_hidden(k3_group_1(sK1495_skl,sK1497_skl),k1_funct_1(k1_latsubgr(sK1495_skl),sK1496_skl))|~sQ1696_spl),
% 157.16/21.22 inference(component_clause,[status(thm)],[f48456])).
% 157.16/21.22 fof(f48459,plain,(
% 157.16/21.22 sQ1696_spl|~sQ1649_spl|~sQ769_spl|~sQ617_spl),
% 157.16/21.22 inference(split_clause,[status(thm)],[f48447,f48456,f45383,f31333,f27243])).
% 157.16/21.22 fof(f48461,plain,(
% 157.16/21.22 $false|~sQ1696_spl),
% 157.16/21.22 inference(forward_subsumption_resolution,[status(thm)],[f48457,f22104])).
% 157.16/21.22 fof(f48462,plain,(
% 157.16/21.22 ~sQ1696_spl),
% 157.16/21.22 inference(contradiction_clause,[status(thm)],[f48461])).
% 157.16/21.22 fof(f48463,plain,(
% 157.16/21.22 $false),
% 157.16/21.22 inference(sat_refutation,[status(thm)],[f27233,f27235,f27237,f27239,f27246,f27710,f27736,f27738,f30407,f31180,f31336,f45386,f48459,f48462])).
% 157.16/21.22 % SZS output end CNFRefutation for theBenchmark.p
% 86.51/21.32 % Elapsed time: 20.841902 seconds
% 86.51/21.32 % CPU time: 157.487788 seconds
% 86.51/21.32 % Total memory used: 1.516 GB
% 86.51/21.32 % Net memory used: 1.438 GB
%------------------------------------------------------------------------------