%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP641+4 : 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:01 PM UTC 2026
% Result : Theorem 47.91s 13.76s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP641+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n011.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Sun Sep 20 20:25:35 UTC 2026
% 0.18/0.44 % CPUTime :
% 7.44/7.78 % Drodi V4.1.1
% 47.91/13.76 % Refutation found
% 47.91/13.76 % SZS status Theorem for theBenchmark: Theorem is valid
% 47.91/13.76 % SZS output start CNFRefutation for theBenchmark
% 47.91/13.76 fof(f18993,axiom,(
% 47.91/13.76 (! [A] :( ( ~ v3_struct_0(A)& l1_group_1(A) )=> m1_subset_1(k2_group_1(A),u1_struct_0(A)) ) )),
% 47.91/13.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 47.91/13.76 fof(f21866,axiom,(
% 47.91/13.76 (! [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)) ) )) )),
% 47.91/13.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 47.91/13.76 fof(f36508,axiom,(
% 47.91/13.76 (! [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) ) ) )) )) )),
% 47.91/13.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 47.91/13.76 fof(f36509,conjecture,(
% 47.91/13.76 (! [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)) ) )) )),
% 47.91/13.76 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 47.91/13.76 fof(f36510,negated_conjecture,(
% 47.91/13.76 ~((! [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)) ) )) ))),
% 47.91/13.76 inference(negated_conjecture,[status(cth)],[f36509])).
% 47.91/13.76 fof(f97877,plain,(
% 47.91/13.76 ![A]: ((v3_struct_0(A)|~l1_group_1(A))|m1_subset_1(k2_group_1(A),u1_struct_0(A)))),
% 47.91/13.76 inference(pre_NNF_transformation,[status(thm)],[f18993])).
% 47.91/13.76 fof(f97878,plain,(
% 47.91/13.76 ![X0]: (v3_struct_0(X0)|~l1_group_1(X0)|m1_subset_1(k2_group_1(X0),u1_struct_0(X0)))),
% 47.91/13.76 inference(cnf_transformation,[status(thm)],[f97877])).
% 47.91/13.76 fof(f108051,plain,(
% 47.91/13.76 ![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)))))),
% 47.91/13.76 inference(pre_NNF_transformation,[status(thm)],[f21866])).
% 47.91/13.76 fof(f108052,plain,(
% 47.91/13.76 ![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)))),
% 47.91/13.76 inference(cnf_transformation,[status(thm)],[f108051])).
% 47.91/13.76 fof(f162767,plain,(
% 47.91/13.76 ![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)))))))),
% 47.91/13.76 inference(pre_NNF_transformation,[status(thm)],[f36508])).
% 47.91/13.76 fof(f162768,plain,(
% 47.91/13.76 ![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))))))))),
% 47.91/13.76 inference(NNF_transformation,[status(thm)],[f162767])).
% 47.91/13.76 fof(f162770,plain,(
% 47.91/13.76 ![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))),
% 47.91/13.76 inference(cnf_transformation,[status(thm)],[f162768])).
% 47.91/13.76 fof(f162771,plain,(
% 47.91/13.76 (?[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))))))),
% 47.91/13.76 inference(pre_NNF_transformation,[status(thm)],[f36510])).
% 47.91/13.76 fof(f162772,plain,(
% 47.91/13.76 ((((~v3_struct_0(sK12737_skl)&v3_group_1(sK12737_skl))&v4_group_1(sK12737_skl))&l1_group_1(sK12737_skl))&((v1_group_1(sK12738_skl)&m1_group_2(sK12738_skl,sK12737_skl))&~r2_hidden(k2_group_1(sK12737_skl),k1_funct_1(k1_latsubgr(sK12737_skl),sK12738_skl))))),
% 47.91/13.76 inference(skolemize,[status(esa),new_symbols(skolem,[sK12737_skl,sK12738_skl]),skolemize(A,sK12737_skl),skolemize(B,sK12738_skl)],[f162771])).
% 47.91/13.76 fof(f162773,plain,(
% 47.91/13.76 ~v3_struct_0(sK12737_skl)),
% 47.91/13.76 inference(cnf_transformation,[status(thm)],[f162772])).
% 47.91/13.76 fof(f162774,plain,(
% 47.91/13.76 v3_group_1(sK12737_skl)),
% 47.91/13.76 inference(cnf_transformation,[status(thm)],[f162772])).
% 47.91/13.76 fof(f162775,plain,(
% 47.91/13.76 v4_group_1(sK12737_skl)),
% 47.91/13.76 inference(cnf_transformation,[status(thm)],[f162772])).
% 47.91/13.76 fof(f162776,plain,(
% 47.91/13.76 l1_group_1(sK12737_skl)),
% 47.91/13.76 inference(cnf_transformation,[status(thm)],[f162772])).
% 47.91/13.76 fof(f162777,plain,(
% 47.91/13.76 v1_group_1(sK12738_skl)),
% 47.91/13.76 inference(cnf_transformation,[status(thm)],[f162772])).
% 47.91/13.76 fof(f162778,plain,(
% 47.91/13.76 m1_group_2(sK12738_skl,sK12737_skl)),
% 47.91/13.76 inference(cnf_transformation,[status(thm)],[f162772])).
% 47.91/13.76 fof(f162779,plain,(
% 47.91/13.76 ~r2_hidden(k2_group_1(sK12737_skl),k1_funct_1(k1_latsubgr(sK12737_skl),sK12738_skl))),
% 47.91/13.76 inference(cnf_transformation,[status(thm)],[f162772])).
% 47.91/13.76 fof(f195537,plain,(
% 47.91/13.76 v3_struct_0(sK12737_skl)|m1_subset_1(k2_group_1(sK12737_skl),u1_struct_0(sK12737_skl))),
% 47.91/13.76 inference(resolution,[status(thm)],[f97878,f162776])).
% 47.91/13.76 fof(f195538,definition,(
% 47.91/13.76 sQ3065_spl <=> (v3_struct_0(sK12737_skl))),
% 47.91/13.76 introduced(definition,[new_symbols(definition,[sQ3065_spl])],[split_symbol_definition])).
% 47.91/13.76 fof(f195539,plain,(
% 47.91/13.76 v3_struct_0(sK12737_skl)|~sQ3065_spl),
% 47.91/13.76 inference(component_clause,[status(thm)],[f195538])).
% 47.91/13.76 fof(f195541,definition,(
% 47.91/13.76 sQ3066_spl <=> (m1_subset_1(k2_group_1(sK12737_skl),u1_struct_0(sK12737_skl)))),
% 47.91/13.77 introduced(definition,[new_symbols(definition,[sQ3066_spl])],[split_symbol_definition])).
% 47.91/13.77 fof(f195544,plain,(
% 47.91/13.77 sQ3065_spl|sQ3066_spl),
% 47.91/13.77 inference(split_clause,[status(thm)],[f195537,f195538,f195541])).
% 47.91/13.77 fof(f195545,plain,(
% 47.91/13.77 $false|~sQ3065_spl),
% 47.91/13.77 inference(forward_subsumption_resolution,[status(thm)],[f195539,f162773])).
% 47.91/13.77 fof(f195546,plain,(
% 47.91/13.77 ~sQ3065_spl),
% 47.91/13.77 inference(contradiction_clause,[status(thm)],[f195545])).
% 47.91/13.77 fof(f195548,definition,(
% 47.91/13.77 sQ3067_spl <=> (v3_group_1(sK12737_skl))),
% 47.91/13.77 introduced(definition,[new_symbols(definition,[sQ3067_spl])],[split_symbol_definition])).
% 47.91/13.77 fof(f195550,plain,(
% 47.91/13.77 ~v3_group_1(sK12737_skl)|sQ3067_spl),
% 47.91/13.77 inference(component_clause,[status(thm)],[f195548])).
% 47.91/13.77 fof(f195551,definition,(
% 47.91/13.77 sQ3068_spl <=> (l1_group_1(sK12737_skl))),
% 47.91/13.77 introduced(definition,[new_symbols(definition,[sQ3068_spl])],[split_symbol_definition])).
% 47.91/13.77 fof(f195553,plain,(
% 47.91/13.77 ~l1_group_1(sK12737_skl)|sQ3068_spl),
% 47.91/13.77 inference(component_clause,[status(thm)],[f195551])).
% 47.91/13.77 fof(f195558,plain,(
% 47.91/13.77 $false|sQ3068_spl),
% 47.91/13.77 inference(forward_subsumption_resolution,[status(thm)],[f195553,f162776])).
% 47.91/13.77 fof(f195559,plain,(
% 47.91/13.77 sQ3068_spl),
% 47.91/13.77 inference(contradiction_clause,[status(thm)],[f195558])).
% 47.91/13.77 fof(f195560,plain,(
% 47.91/13.77 $false|sQ3067_spl),
% 47.91/13.77 inference(forward_subsumption_resolution,[status(thm)],[f195550,f162774])).
% 47.91/13.77 fof(f195561,plain,(
% 47.91/13.77 sQ3067_spl),
% 47.91/13.77 inference(contradiction_clause,[status(thm)],[f195560])).
% 47.91/13.77 fof(f197047,plain,(
% 47.91/13.77 v3_struct_0(sK12737_skl)|~v3_group_1(sK12737_skl)|~v4_group_1(sK12737_skl)|~l1_group_1(sK12737_skl)|r1_rlvect_1(sK12738_skl,k2_group_1(sK12737_skl))),
% 47.91/13.77 inference(resolution,[status(thm)],[f162778,f108052])).
% 47.91/13.77 fof(f197053,definition,(
% 47.91/13.77 sQ3075_spl <=> (v4_group_1(sK12737_skl))),
% 47.91/13.77 introduced(definition,[new_symbols(definition,[sQ3075_spl])],[split_symbol_definition])).
% 47.91/13.77 fof(f197055,plain,(
% 47.91/13.77 ~v4_group_1(sK12737_skl)|sQ3075_spl),
% 47.91/13.77 inference(component_clause,[status(thm)],[f197053])).
% 47.91/13.77 fof(f197056,definition,(
% 47.91/13.77 sQ3076_spl <=> (v1_group_1(sK12738_skl))),
% 47.91/13.77 introduced(definition,[new_symbols(definition,[sQ3076_spl])],[split_symbol_definition])).
% 47.91/13.77 fof(f197058,plain,(
% 47.91/13.77 ~v1_group_1(sK12738_skl)|sQ3076_spl),
% 47.91/13.77 inference(component_clause,[status(thm)],[f197056])).
% 47.91/13.77 fof(f197144,definition,(
% 47.91/13.77 sQ3099_spl <=> (r1_rlvect_1(sK12738_skl,k2_group_1(sK12737_skl)))),
% 47.91/13.77 introduced(definition,[new_symbols(definition,[sQ3099_spl])],[split_symbol_definition])).
% 47.91/13.77 fof(f197147,plain,(
% 47.91/13.77 sQ3065_spl|~sQ3067_spl|~sQ3075_spl|~sQ3068_spl|sQ3099_spl),
% 47.91/13.77 inference(split_clause,[status(thm)],[f197047,f195538,f195548,f197053,f195551,f197144])).
% 47.91/13.77 fof(f197159,plain,(
% 47.91/13.77 $false|sQ3075_spl),
% 47.91/13.77 inference(forward_subsumption_resolution,[status(thm)],[f197055,f162775])).
% 47.91/13.77 fof(f197160,plain,(
% 47.91/13.77 sQ3075_spl),
% 47.91/13.77 inference(contradiction_clause,[status(thm)],[f197159])).
% 47.91/13.77 fof(f197161,plain,(
% 47.91/13.77 $false|sQ3076_spl),
% 47.91/13.77 inference(forward_subsumption_resolution,[status(thm)],[f197058,f162777])).
% 47.91/13.77 fof(f197162,plain,(
% 47.91/13.77 sQ3076_spl),
% 47.91/13.77 inference(contradiction_clause,[status(thm)],[f197161])).
% 47.91/13.77 fof(f197163,plain,(
% 51.41/14.53 v3_struct_0(sK12737_skl)|~v3_group_1(sK12737_skl)|~v4_group_1(sK12737_skl)|~l1_group_1(sK12737_skl)|~v1_group_1(sK12738_skl)|~m1_group_2(sK12738_skl,sK12737_skl)|~m1_subset_1(k2_group_1(sK12737_skl),u1_struct_0(sK12737_skl))|~r1_rlvect_1(sK12738_skl,k2_group_1(sK12737_skl))),
% 51.41/14.53 inference(resolution,[status(thm)],[f162779,f162770])).
% 51.41/14.53 fof(f197175,definition,(
% 51.41/14.53 sQ3102_spl <=> (m1_group_2(sK12738_skl,sK12737_skl))),
% 51.41/14.53 introduced(definition,[new_symbols(definition,[sQ3102_spl])],[split_symbol_definition])).
% 51.41/14.53 fof(f197177,plain,(
% 51.41/14.53 ~m1_group_2(sK12738_skl,sK12737_skl)|sQ3102_spl),
% 51.41/14.53 inference(component_clause,[status(thm)],[f197175])).
% 51.41/14.53 fof(f197178,plain,(
% 51.41/14.53 sQ3065_spl|~sQ3067_spl|~sQ3075_spl|~sQ3068_spl|~sQ3076_spl|~sQ3102_spl|~sQ3066_spl|~sQ3099_spl),
% 51.41/14.53 inference(split_clause,[status(thm)],[f197163,f195538,f195548,f197053,f195551,f197056,f197175,f195541,f197144])).
% 51.41/14.53 fof(f197179,plain,(
% 51.41/14.53 $false|sQ3102_spl),
% 51.41/14.53 inference(forward_subsumption_resolution,[status(thm)],[f197177,f162778])).
% 51.41/14.53 fof(f197180,plain,(
% 51.41/14.53 sQ3102_spl),
% 51.41/14.53 inference(contradiction_clause,[status(thm)],[f197179])).
% 51.41/14.53 fof(f197181,plain,(
% 51.41/14.53 $false),
% 51.41/14.53 inference(sat_refutation,[status(thm)],[f195544,f195546,f195559,f195561,f197147,f197160,f197162,f197178,f197180])).
% 51.41/14.53 % SZS output end CNFRefutation for theBenchmark.p
% 11.14/15.30 % Elapsed time: 14.580285 seconds
% 11.14/15.30 % CPU time: 49.591279 seconds
% 11.14/15.30 % Total memory used: 11.472 GB
% 11.14/15.30 % Net memory used: 11.405 GB
%------------------------------------------------------------------------------