%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP641+3 : 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 : n020.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 16.99s 4.97s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP641+3 : 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.15/0.41 % Computer : n020.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Sun Sep 20 20:25:35 UTC 2026
% 0.15/0.41 % CPUTime :
% 2.80/3.09 % Drodi V4.1.1
% 16.99/4.97 % Refutation found
% 16.99/4.97 % SZS status Theorem for theBenchmark: Theorem is valid
% 16.99/4.97 % SZS output start CNFRefutation for theBenchmark
% 16.99/4.97 fof(f7470,axiom,(
% 16.99/4.97 (! [A] :( ( ~ v3_struct_0(A)& l1_group_1(A) )=> m1_subset_1(k2_group_1(A),u1_struct_0(A)) ) )),
% 16.99/4.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.99/4.97 fof(f8757,axiom,(
% 16.99/4.97 (! [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)) ) )) )),
% 16.99/4.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.99/4.97 fof(f13982,axiom,(
% 16.99/4.97 (! [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) ) ) )) )) )),
% 16.99/4.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.99/4.97 fof(f13983,conjecture,(
% 16.99/4.97 (! [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)) ) )) )),
% 16.99/4.97 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 16.99/4.97 fof(f13984,negated_conjecture,(
% 16.99/4.97 ~((! [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)) ) )) ))),
% 16.99/4.97 inference(negated_conjecture,[status(cth)],[f13983])).
% 16.99/4.97 fof(f36616,plain,(
% 16.99/4.97 ![A]: ((v3_struct_0(A)|~l1_group_1(A))|m1_subset_1(k2_group_1(A),u1_struct_0(A)))),
% 16.99/4.97 inference(pre_NNF_transformation,[status(thm)],[f7470])).
% 16.99/4.97 fof(f36617,plain,(
% 16.99/4.97 ![X0]: (v3_struct_0(X0)|~l1_group_1(X0)|m1_subset_1(k2_group_1(X0),u1_struct_0(X0)))),
% 16.99/4.97 inference(cnf_transformation,[status(thm)],[f36616])).
% 16.99/4.97 fof(f40343,plain,(
% 16.99/4.97 ![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)))))),
% 16.99/4.97 inference(pre_NNF_transformation,[status(thm)],[f8757])).
% 16.99/4.97 fof(f40344,plain,(
% 16.99/4.97 ![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)))),
% 16.99/4.97 inference(cnf_transformation,[status(thm)],[f40343])).
% 16.99/4.97 fof(f59572,plain,(
% 16.99/4.97 ![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)))))))),
% 16.99/4.97 inference(pre_NNF_transformation,[status(thm)],[f13982])).
% 16.99/4.97 fof(f59573,plain,(
% 16.99/4.97 ![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))))))))),
% 16.99/4.97 inference(NNF_transformation,[status(thm)],[f59572])).
% 16.99/4.97 fof(f59575,plain,(
% 16.99/4.97 ![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))),
% 16.99/4.97 inference(cnf_transformation,[status(thm)],[f59573])).
% 16.99/4.97 fof(f59576,plain,(
% 16.99/4.97 (?[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))))))),
% 16.99/4.97 inference(pre_NNF_transformation,[status(thm)],[f13984])).
% 16.99/4.97 fof(f59577,plain,(
% 16.99/4.97 ((((~v3_struct_0(sK4179_skl)&v3_group_1(sK4179_skl))&v4_group_1(sK4179_skl))&l1_group_1(sK4179_skl))&((v1_group_1(sK4180_skl)&m1_group_2(sK4180_skl,sK4179_skl))&~r2_hidden(k2_group_1(sK4179_skl),k1_funct_1(k1_latsubgr(sK4179_skl),sK4180_skl))))),
% 16.99/4.97 inference(skolemize,[status(esa),new_symbols(skolem,[sK4179_skl,sK4180_skl]),skolemize(A,sK4179_skl),skolemize(B,sK4180_skl)],[f59576])).
% 16.99/4.97 fof(f59578,plain,(
% 16.99/4.97 ~v3_struct_0(sK4179_skl)),
% 16.99/4.97 inference(cnf_transformation,[status(thm)],[f59577])).
% 16.99/4.97 fof(f59579,plain,(
% 16.99/4.97 v3_group_1(sK4179_skl)),
% 16.99/4.97 inference(cnf_transformation,[status(thm)],[f59577])).
% 16.99/4.97 fof(f59580,plain,(
% 16.99/4.97 v4_group_1(sK4179_skl)),
% 16.99/4.97 inference(cnf_transformation,[status(thm)],[f59577])).
% 16.99/4.97 fof(f59581,plain,(
% 16.99/4.97 l1_group_1(sK4179_skl)),
% 16.99/4.97 inference(cnf_transformation,[status(thm)],[f59577])).
% 16.99/4.97 fof(f59582,plain,(
% 16.99/4.97 v1_group_1(sK4180_skl)),
% 16.99/4.97 inference(cnf_transformation,[status(thm)],[f59577])).
% 16.99/4.97 fof(f59583,plain,(
% 16.99/4.97 m1_group_2(sK4180_skl,sK4179_skl)),
% 16.99/4.97 inference(cnf_transformation,[status(thm)],[f59577])).
% 16.99/4.97 fof(f59584,plain,(
% 16.99/4.97 ~r2_hidden(k2_group_1(sK4179_skl),k1_funct_1(k1_latsubgr(sK4179_skl),sK4180_skl))),
% 16.99/4.97 inference(cnf_transformation,[status(thm)],[f59577])).
% 16.99/4.97 fof(f68412,plain,(
% 16.99/4.97 v3_struct_0(sK4179_skl)|m1_subset_1(k2_group_1(sK4179_skl),u1_struct_0(sK4179_skl))),
% 16.99/4.97 inference(resolution,[status(thm)],[f36617,f59581])).
% 16.99/4.97 fof(f68413,definition,(
% 16.99/4.97 sQ1246_spl <=> (v3_struct_0(sK4179_skl))),
% 16.99/4.97 introduced(definition,[new_symbols(definition,[sQ1246_spl])],[split_symbol_definition])).
% 16.99/4.97 fof(f68414,plain,(
% 16.99/4.97 v3_struct_0(sK4179_skl)|~sQ1246_spl),
% 16.99/4.97 inference(component_clause,[status(thm)],[f68413])).
% 16.99/4.97 fof(f68416,definition,(
% 16.99/4.97 sQ1247_spl <=> (m1_subset_1(k2_group_1(sK4179_skl),u1_struct_0(sK4179_skl)))),
% 16.99/4.97 introduced(definition,[new_symbols(definition,[sQ1247_spl])],[split_symbol_definition])).
% 16.99/4.97 fof(f68419,plain,(
% 16.99/4.97 sQ1246_spl|sQ1247_spl),
% 16.99/4.97 inference(split_clause,[status(thm)],[f68412,f68413,f68416])).
% 16.99/4.97 fof(f68420,plain,(
% 16.99/4.97 $false|~sQ1246_spl),
% 16.99/4.97 inference(forward_subsumption_resolution,[status(thm)],[f68414,f59578])).
% 16.99/4.97 fof(f68421,plain,(
% 16.99/4.97 ~sQ1246_spl),
% 16.99/4.97 inference(contradiction_clause,[status(thm)],[f68420])).
% 16.99/4.97 fof(f68423,definition,(
% 16.99/4.97 sQ1248_spl <=> (v3_group_1(sK4179_skl))),
% 16.99/4.97 introduced(definition,[new_symbols(definition,[sQ1248_spl])],[split_symbol_definition])).
% 16.99/4.97 fof(f68425,plain,(
% 16.99/4.97 ~v3_group_1(sK4179_skl)|sQ1248_spl),
% 16.99/4.97 inference(component_clause,[status(thm)],[f68423])).
% 16.99/4.97 fof(f68426,definition,(
% 16.99/4.97 sQ1249_spl <=> (l1_group_1(sK4179_skl))),
% 16.99/4.97 introduced(definition,[new_symbols(definition,[sQ1249_spl])],[split_symbol_definition])).
% 16.99/4.97 fof(f68428,plain,(
% 16.99/4.97 ~l1_group_1(sK4179_skl)|sQ1249_spl),
% 16.99/4.97 inference(component_clause,[status(thm)],[f68426])).
% 16.99/4.97 fof(f68433,plain,(
% 16.99/4.97 $false|sQ1249_spl),
% 16.99/4.97 inference(forward_subsumption_resolution,[status(thm)],[f68428,f59581])).
% 16.99/4.97 fof(f68434,plain,(
% 16.99/4.97 sQ1249_spl),
% 16.99/4.97 inference(contradiction_clause,[status(thm)],[f68433])).
% 16.99/4.97 fof(f68435,plain,(
% 16.99/4.97 $false|sQ1248_spl),
% 16.99/4.97 inference(forward_subsumption_resolution,[status(thm)],[f68425,f59579])).
% 16.99/4.97 fof(f68436,plain,(
% 16.99/4.97 sQ1248_spl),
% 16.99/4.97 inference(contradiction_clause,[status(thm)],[f68435])).
% 16.99/4.97 fof(f70062,plain,(
% 16.99/4.97 v3_struct_0(sK4179_skl)|~v3_group_1(sK4179_skl)|~v4_group_1(sK4179_skl)|~l1_group_1(sK4179_skl)|r1_rlvect_1(sK4180_skl,k2_group_1(sK4179_skl))),
% 16.99/4.97 inference(resolution,[status(thm)],[f59583,f40344])).
% 16.99/4.97 fof(f70073,definition,(
% 16.99/4.97 sQ1256_spl <=> (v4_group_1(sK4179_skl))),
% 16.99/4.97 introduced(definition,[new_symbols(definition,[sQ1256_spl])],[split_symbol_definition])).
% 16.99/4.97 fof(f70075,plain,(
% 16.99/4.97 ~v4_group_1(sK4179_skl)|sQ1256_spl),
% 16.99/4.97 inference(component_clause,[status(thm)],[f70073])).
% 16.99/4.97 fof(f70076,definition,(
% 16.99/4.97 sQ1257_spl <=> (v1_group_1(sK4180_skl))),
% 16.99/4.97 introduced(definition,[new_symbols(definition,[sQ1257_spl])],[split_symbol_definition])).
% 16.99/4.97 fof(f70078,plain,(
% 16.99/4.97 ~v1_group_1(sK4180_skl)|sQ1257_spl),
% 16.99/4.97 inference(component_clause,[status(thm)],[f70076])).
% 16.99/4.97 fof(f70154,definition,(
% 16.99/4.97 sQ1278_spl <=> (r1_rlvect_1(sK4180_skl,k2_group_1(sK4179_skl)))),
% 16.99/4.97 introduced(definition,[new_symbols(definition,[sQ1278_spl])],[split_symbol_definition])).
% 16.99/4.97 fof(f70157,plain,(
% 16.99/4.97 sQ1246_spl|~sQ1248_spl|~sQ1256_spl|~sQ1249_spl|sQ1278_spl),
% 16.99/4.97 inference(split_clause,[status(thm)],[f70062,f68413,f68423,f70073,f68426,f70154])).
% 16.99/4.97 fof(f70183,plain,(
% 16.99/4.97 $false|sQ1256_spl),
% 16.99/4.97 inference(forward_subsumption_resolution,[status(thm)],[f70075,f59580])).
% 16.99/4.97 fof(f70184,plain,(
% 16.99/4.97 sQ1256_spl),
% 16.99/4.97 inference(contradiction_clause,[status(thm)],[f70183])).
% 16.99/4.97 fof(f70185,plain,(
% 16.99/4.97 $false|sQ1257_spl),
% 16.99/4.97 inference(forward_subsumption_resolution,[status(thm)],[f70078,f59582])).
% 16.99/4.97 fof(f70186,plain,(
% 16.99/4.97 sQ1257_spl),
% 16.99/4.97 inference(contradiction_clause,[status(thm)],[f70185])).
% 16.99/4.97 fof(f70187,plain,(
% 16.99/4.97 v3_struct_0(sK4179_skl)|~v3_group_1(sK4179_skl)|~v4_group_1(sK4179_skl)|~l1_group_1(sK4179_skl)|~v1_group_1(sK4180_skl)|~m1_group_2(sK4180_skl,sK4179_skl)|~m1_subset_1(k2_group_1(sK4179_skl),u1_struct_0(sK4179_skl))|~r1_rlvect_1(sK4180_skl,k2_group_1(sK4179_skl))),
% 18.54/5.20 inference(resolution,[status(thm)],[f59584,f59575])).
% 18.54/5.20 fof(f70199,definition,(
% 18.54/5.20 sQ1284_spl <=> (m1_group_2(sK4180_skl,sK4179_skl))),
% 18.54/5.20 introduced(definition,[new_symbols(definition,[sQ1284_spl])],[split_symbol_definition])).
% 18.54/5.20 fof(f70201,plain,(
% 18.54/5.20 ~m1_group_2(sK4180_skl,sK4179_skl)|sQ1284_spl),
% 18.54/5.20 inference(component_clause,[status(thm)],[f70199])).
% 18.54/5.20 fof(f70202,plain,(
% 18.54/5.20 sQ1246_spl|~sQ1248_spl|~sQ1256_spl|~sQ1249_spl|~sQ1257_spl|~sQ1284_spl|~sQ1247_spl|~sQ1278_spl),
% 18.54/5.20 inference(split_clause,[status(thm)],[f70187,f68413,f68423,f70073,f68426,f70076,f70199,f68416,f70154])).
% 18.54/5.20 fof(f70203,plain,(
% 18.54/5.20 $false|sQ1284_spl),
% 18.54/5.20 inference(forward_subsumption_resolution,[status(thm)],[f70201,f59583])).
% 18.54/5.20 fof(f70204,plain,(
% 18.54/5.20 sQ1284_spl),
% 18.54/5.20 inference(contradiction_clause,[status(thm)],[f70203])).
% 18.54/5.20 fof(f70205,plain,(
% 18.54/5.20 $false),
% 18.54/5.20 inference(sat_refutation,[status(thm)],[f68419,f68421,f68434,f68436,f70157,f70184,f70186,f70202,f70204])).
% 18.54/5.20 % SZS output end CNFRefutation for theBenchmark.p
% 5.96/5.37 % Elapsed time: 4.895862 seconds
% 5.96/5.37 % CPU time: 17.945561 seconds
% 5.96/5.37 % Total memory used: 3.926 GB
% 5.96/5.37 % Net memory used: 3.897 GB
%------------------------------------------------------------------------------