%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP644+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 : n009.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:02 PM UTC 2026
% Result : Theorem 60.38s 9.78s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP644+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.14/0.42 % Computer : n009.cluster.edu
% 0.14/0.42 % Model : x86_64 x86_64
% 0.14/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.42 % Memory : 8046.5625MB
% 0.14/0.42 % OS : Linux 6.8.0-71-generic
% 0.14/0.42 % CPULimit : 300
% 0.14/0.42 % WCLimit : 300
% 0.14/0.42 % DateTime : Sun Sep 20 20:26:02 UTC 2026
% 0.14/0.42 % CPUTime :
% 2.05/2.37 % Drodi V4.1.1
% 60.38/9.78 % Refutation found
% 60.38/9.78 % SZS status Theorem for theBenchmark: Theorem is valid
% 60.38/9.78 % SZS output start CNFRefutation for theBenchmark
% 60.38/9.78 fof(f7471,axiom,(
% 60.38/9.78 (! [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)) ) )),
% 60.38/9.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 60.38/9.78 fof(f8697,axiom,(
% 60.38/9.78 (! [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) ) )) )),
% 60.38/9.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 60.38/9.78 fof(f8762,axiom,(
% 60.38/9.78 (! [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)) ) ) )) )) )),
% 60.38/9.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 60.38/9.78 fof(f8765,axiom,(
% 60.38/9.78 (! [A] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> m1_group_2(A,A) ) )),
% 60.38/9.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 60.38/9.78 fof(f8767,axiom,(
% 60.38/9.78 (! [A] :( ( ~ v3_struct_0(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v3_group_1(B)& v4_group_1(B)& l1_group_1(B) )=> (! [C] :( ( ~ v3_struct_0(C)& v3_group_1(C)& v4_group_1(C)& l1_group_1(C) )=> ( ( m1_group_2(A,B)& m1_group_2(B,C) )=> m1_group_2(A,C) ) ) )) )) )),
% 60.38/9.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 60.38/9.78 fof(f8898,axiom,(
% 60.38/9.78 (! [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) ) ) )) )),
% 60.38/9.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 60.38/9.78 fof(f13982,axiom,(
% 60.38/9.78 (! [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) ) ) )) )) )),
% 60.38/9.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 60.38/9.78 fof(f13986,conjecture,(
% 60.38/9.78 (! [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)) ) ) )) )) )),
% 60.38/9.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 60.38/9.78 fof(f13987,negated_conjecture,(
% 60.38/9.78 ~((! [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)) ) ) )) )) ))),
% 60.38/9.78 inference(negated_conjecture,[status(cth)],[f13986])).
% 60.38/9.78 fof(f36621,plain,(
% 60.38/9.78 ![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)))),
% 60.38/9.78 inference(pre_NNF_transformation,[status(thm)],[f7471])).
% 60.38/9.78 fof(f36622,plain,(
% 60.38/9.78 ![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)))),
% 60.38/9.78 inference(cnf_transformation,[status(thm)],[f36621])).
% 60.38/9.78 fof(f40185,plain,(
% 60.38/9.78 ![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))))),
% 60.38/9.78 inference(pre_NNF_transformation,[status(thm)],[f8697])).
% 60.38/9.78 fof(f40186,plain,(
% 60.38/9.78 ![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))),
% 60.38/9.78 inference(cnf_transformation,[status(thm)],[f40185])).
% 60.38/9.78 fof(f40356,plain,(
% 60.38/9.78 ![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))))))))),
% 60.38/9.78 inference(pre_NNF_transformation,[status(thm)],[f8762])).
% 60.38/9.78 fof(f40357,plain,(
% 60.38/9.78 ![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)))),
% 60.38/9.78 inference(cnf_transformation,[status(thm)],[f40356])).
% 60.38/9.78 fof(f40368,plain,(
% 60.38/9.78 ![A]: ((((v3_struct_0(A)|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|m1_group_2(A,A))),
% 60.38/9.78 inference(pre_NNF_transformation,[status(thm)],[f8765])).
% 60.38/9.78 fof(f40369,plain,(
% 60.38/9.78 ![X0]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|m1_group_2(X0,X0))),
% 60.38/9.78 inference(cnf_transformation,[status(thm)],[f40368])).
% 60.38/9.78 fof(f40372,plain,(
% 60.38/9.78 ![A]: ((((v3_struct_0(A)|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|(![B]: ((((v3_struct_0(B)|~v3_group_1(B))|~v4_group_1(B))|~l1_group_1(B))|(![C]: ((((v3_struct_0(C)|~v3_group_1(C))|~v4_group_1(C))|~l1_group_1(C))|((~m1_group_2(A,B)|~m1_group_2(B,C))|m1_group_2(A,C)))))))),
% 60.38/9.78 inference(pre_NNF_transformation,[status(thm)],[f8767])).
% 60.38/9.78 fof(f40373,plain,(
% 60.38/9.78 ![X0,X1,X2]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|v3_struct_0(X1)|~v3_group_1(X1)|~v4_group_1(X1)|~l1_group_1(X1)|v3_struct_0(X2)|~v3_group_1(X2)|~v4_group_1(X2)|~l1_group_1(X2)|~m1_group_2(X0,X1)|~m1_group_2(X1,X2)|m1_group_2(X0,X2))),
% 60.38/9.78 inference(cnf_transformation,[status(thm)],[f40372])).
% 60.38/9.78 fof(f40733,plain,(
% 60.38/9.78 ![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)))))),
% 60.38/9.78 inference(pre_NNF_transformation,[status(thm)],[f8898])).
% 60.38/9.78 fof(f40734,plain,(
% 60.38/9.78 ![X0,X1]: (v3_struct_0(X0)|~v3_group_1(X0)|~l1_group_1(X0)|~m1_group_2(X1,X0)|~v3_struct_0(X1))),
% 60.38/9.78 inference(cnf_transformation,[status(thm)],[f40733])).
% 60.38/9.78 fof(f40735,plain,(
% 60.38/9.78 ![X0,X1]: (v3_struct_0(X0)|~v3_group_1(X0)|~l1_group_1(X0)|~m1_group_2(X1,X0)|v3_group_1(X1))),
% 60.38/9.78 inference(cnf_transformation,[status(thm)],[f40733])).
% 60.38/9.78 fof(f40736,plain,(
% 60.38/9.78 ![X0,X1]: (v3_struct_0(X0)|~v3_group_1(X0)|~l1_group_1(X0)|~m1_group_2(X1,X0)|l1_group_1(X1))),
% 60.38/9.78 inference(cnf_transformation,[status(thm)],[f40733])).
% 60.38/9.78 fof(f59575,plain,(
% 60.38/9.78 ![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)))))))),
% 60.38/9.78 inference(pre_NNF_transformation,[status(thm)],[f13982])).
% 60.38/9.78 fof(f59576,plain,(
% 60.38/9.78 ![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))))))))),
% 60.38/9.78 inference(NNF_transformation,[status(thm)],[f59575])).
% 60.38/9.78 fof(f59577,plain,(
% 60.38/9.78 ![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))),
% 60.38/9.78 inference(cnf_transformation,[status(thm)],[f59576])).
% 60.38/9.78 fof(f59578,plain,(
% 60.38/9.78 ![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))),
% 60.38/9.78 inference(cnf_transformation,[status(thm)],[f59576])).
% 60.38/9.78 fof(f59585,plain,(
% 60.38/9.78 (?[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)))))))))),
% 60.38/9.78 inference(pre_NNF_transformation,[status(thm)],[f13987])).
% 60.38/9.78 fof(f59586,plain,(
% 60.38/9.78 ((((~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(sK4181_skl,u1_struct_0(sK4179_skl))&(r2_hidden(sK4181_skl,k1_funct_1(k1_latsubgr(sK4179_skl),sK4180_skl))&~r2_hidden(k3_group_1(sK4179_skl,sK4181_skl),k1_funct_1(k1_latsubgr(sK4179_skl),sK4180_skl))))))),
% 60.38/9.78 inference(skolemize,[status(esa),new_symbols(skolem,[sK4179_skl,sK4180_skl,sK4181_skl]),skolemize(A,sK4179_skl),skolemize(B,sK4180_skl),skolemize(C,sK4181_skl)],[f59585])).
% 60.38/9.78 fof(f59587,plain,(
% 60.38/9.78 ~v3_struct_0(sK4179_skl)),
% 60.38/9.78 inference(cnf_transformation,[status(thm)],[f59586])).
% 60.38/9.78 fof(f59588,plain,(
% 60.38/9.78 v3_group_1(sK4179_skl)),
% 60.38/9.78 inference(cnf_transformation,[status(thm)],[f59586])).
% 60.38/9.78 fof(f59589,plain,(
% 60.38/9.78 v4_group_1(sK4179_skl)),
% 60.38/9.78 inference(cnf_transformation,[status(thm)],[f59586])).
% 60.38/9.78 fof(f59590,plain,(
% 60.38/9.78 l1_group_1(sK4179_skl)),
% 60.38/9.78 inference(cnf_transformation,[status(thm)],[f59586])).
% 60.38/9.78 fof(f59591,plain,(
% 60.38/9.78 v1_group_1(sK4180_skl)),
% 60.38/9.78 inference(cnf_transformation,[status(thm)],[f59586])).
% 60.38/9.78 fof(f59592,plain,(
% 60.38/9.78 m1_group_2(sK4180_skl,sK4179_skl)),
% 60.38/9.78 inference(cnf_transformation,[status(thm)],[f59586])).
% 60.38/9.78 fof(f59593,plain,(
% 60.38/9.78 m1_subset_1(sK4181_skl,u1_struct_0(sK4179_skl))),
% 60.38/9.78 inference(cnf_transformation,[status(thm)],[f59586])).
% 60.38/9.78 fof(f59594,plain,(
% 60.38/9.78 r2_hidden(sK4181_skl,k1_funct_1(k1_latsubgr(sK4179_skl),sK4180_skl))),
% 60.38/9.78 inference(cnf_transformation,[status(thm)],[f59586])).
% 60.38/9.78 fof(f59595,plain,(
% 60.38/9.78 ~r2_hidden(k3_group_1(sK4179_skl,sK4181_skl),k1_funct_1(k1_latsubgr(sK4179_skl),sK4180_skl))),
% 60.38/9.78 inference(cnf_transformation,[status(thm)],[f59586])).
% 60.38/9.78 fof(f68358,definition,(
% 60.38/9.79 sQ1247_spl <=> (v3_struct_0(sK4179_skl))),
% 60.38/9.79 introduced(definition,[new_symbols(definition,[sQ1247_spl])],[split_symbol_definition])).
% 60.38/9.79 fof(f68359,plain,(
% 60.38/9.79 v3_struct_0(sK4179_skl)|~sQ1247_spl),
% 60.38/9.79 inference(component_clause,[status(thm)],[f68358])).
% 60.38/9.79 fof(f68361,definition,(
% 60.38/9.79 sQ1248_spl <=> (v4_group_1(sK4179_skl))),
% 60.38/9.79 introduced(definition,[new_symbols(definition,[sQ1248_spl])],[split_symbol_definition])).
% 60.38/9.79 fof(f68363,plain,(
% 60.38/9.79 ~v4_group_1(sK4179_skl)|sQ1248_spl),
% 60.38/9.79 inference(component_clause,[status(thm)],[f68361])).
% 60.38/9.79 fof(f68364,definition,(
% 60.38/9.79 sQ1249_spl <=> (l1_group_1(sK4179_skl))),
% 60.38/9.79 introduced(definition,[new_symbols(definition,[sQ1249_spl])],[split_symbol_definition])).
% 60.38/9.79 fof(f68366,plain,(
% 60.38/9.79 ~l1_group_1(sK4179_skl)|sQ1249_spl),
% 60.38/9.79 inference(component_clause,[status(thm)],[f68364])).
% 60.38/9.79 fof(f68371,plain,(
% 60.38/9.79 $false|sQ1249_spl),
% 60.38/9.79 inference(forward_subsumption_resolution,[status(thm)],[f68366,f59590])).
% 60.38/9.79 fof(f68372,plain,(
% 60.38/9.79 sQ1249_spl),
% 60.38/9.79 inference(contradiction_clause,[status(thm)],[f68371])).
% 60.38/9.79 fof(f68373,plain,(
% 60.38/9.79 $false|sQ1248_spl),
% 60.38/9.79 inference(forward_subsumption_resolution,[status(thm)],[f68363,f59589])).
% 60.38/9.79 fof(f68374,plain,(
% 60.38/9.79 sQ1248_spl),
% 60.38/9.79 inference(contradiction_clause,[status(thm)],[f68373])).
% 60.38/9.79 fof(f68375,plain,(
% 60.38/9.79 $false|~sQ1247_spl),
% 60.38/9.79 inference(forward_subsumption_resolution,[status(thm)],[f68359,f59587])).
% 60.38/9.79 fof(f68376,plain,(
% 60.38/9.79 ~sQ1247_spl),
% 60.38/9.79 inference(contradiction_clause,[status(thm)],[f68375])).
% 60.38/9.79 fof(f68378,plain,(
% 60.38/9.79 v3_struct_0(sK4179_skl)|~v3_group_1(sK4179_skl)|~l1_group_1(sK4179_skl)|~v3_struct_0(sK4180_skl)),
% 60.38/9.79 inference(resolution,[status(thm)],[f40734,f59592])).
% 60.38/9.79 fof(f68379,definition,(
% 60.38/9.79 sQ1251_spl <=> (v3_group_1(sK4179_skl))),
% 60.38/9.79 introduced(definition,[new_symbols(definition,[sQ1251_spl])],[split_symbol_definition])).
% 60.38/9.79 fof(f68381,plain,(
% 60.38/9.79 ~v3_group_1(sK4179_skl)|sQ1251_spl),
% 60.38/9.79 inference(component_clause,[status(thm)],[f68379])).
% 60.38/9.79 fof(f68383,definition,(
% 60.38/9.79 sQ1252_spl <=> (v3_struct_0(sK4180_skl))),
% 60.38/9.79 introduced(definition,[new_symbols(definition,[sQ1252_spl])],[split_symbol_definition])).
% 60.38/9.79 fof(f68386,plain,(
% 60.38/9.79 sQ1247_spl|~sQ1251_spl|~sQ1249_spl|~sQ1252_spl),
% 60.38/9.79 inference(split_clause,[status(thm)],[f68378,f68358,f68379,f68364,f68383])).
% 60.38/9.79 fof(f68387,plain,(
% 60.38/9.79 $false|sQ1251_spl),
% 60.38/9.79 inference(forward_subsumption_resolution,[status(thm)],[f68381,f59588])).
% 60.38/9.79 fof(f68388,plain,(
% 60.38/9.79 sQ1251_spl),
% 60.38/9.79 inference(contradiction_clause,[status(thm)],[f68387])).
% 60.38/9.79 fof(f68390,plain,(
% 60.38/9.79 v3_struct_0(sK4179_skl)|~v3_group_1(sK4179_skl)|~l1_group_1(sK4179_skl)|v3_group_1(sK4180_skl)),
% 60.38/9.79 inference(resolution,[status(thm)],[f40735,f59592])).
% 60.38/9.79 fof(f68392,definition,(
% 60.38/9.79 sQ1253_spl <=> (v3_group_1(sK4180_skl))),
% 60.38/9.79 introduced(definition,[new_symbols(definition,[sQ1253_spl])],[split_symbol_definition])).
% 60.38/9.79 fof(f68393,plain,(
% 60.38/9.79 v3_group_1(sK4180_skl)|~sQ1253_spl),
% 60.38/9.79 inference(component_clause,[status(thm)],[f68392])).
% 60.38/9.79 fof(f68395,plain,(
% 60.38/9.79 sQ1247_spl|~sQ1251_spl|~sQ1249_spl|sQ1253_spl),
% 60.38/9.79 inference(split_clause,[status(thm)],[f68390,f68358,f68379,f68364,f68392])).
% 60.38/9.79 fof(f68494,plain,(
% 60.38/9.79 v3_struct_0(sK4180_skl)|~v4_group_1(sK4180_skl)|~l1_group_1(sK4180_skl)|m1_group_2(sK4180_skl,sK4180_skl)|~sQ1253_spl),
% 60.38/9.79 inference(resolution,[status(thm)],[f68393,f40369])).
% 60.38/9.79 fof(f68495,definition,(
% 60.38/9.79 sQ1256_spl <=> (v4_group_1(sK4180_skl))),
% 60.38/9.79 introduced(definition,[new_symbols(definition,[sQ1256_spl])],[split_symbol_definition])).
% 60.38/9.79 fof(f68498,definition,(
% 60.38/9.79 sQ1257_spl <=> (l1_group_1(sK4180_skl))),
% 60.38/9.79 introduced(definition,[new_symbols(definition,[sQ1257_spl])],[split_symbol_definition])).
% 60.38/9.79 fof(f68501,definition,(
% 60.38/9.79 sQ1258_spl <=> (m1_group_2(sK4180_skl,sK4180_skl))),
% 60.38/9.79 introduced(definition,[new_symbols(definition,[sQ1258_spl])],[split_symbol_definition])).
% 60.38/9.79 fof(f68502,plain,(
% 60.38/9.79 m1_group_2(sK4180_skl,sK4180_skl)|~sQ1258_spl),
% 60.38/9.79 inference(component_clause,[status(thm)],[f68501])).
% 60.38/9.79 fof(f68504,plain,(
% 60.38/9.79 sQ1252_spl|~sQ1256_spl|~sQ1257_spl|sQ1258_spl|~sQ1253_spl),
% 60.38/9.79 inference(split_clause,[status(thm)],[f68494,f68383,f68495,f68498,f68501,f68392])).
% 60.38/9.79 fof(f68511,plain,(
% 60.38/9.79 v3_struct_0(sK4179_skl)|~v3_group_1(sK4179_skl)|~l1_group_1(sK4179_skl)|l1_group_1(sK4180_skl)),
% 60.38/9.79 inference(resolution,[status(thm)],[f40736,f59592])).
% 60.38/9.79 fof(f68514,plain,(
% 60.38/9.79 sQ1247_spl|~sQ1251_spl|~sQ1249_spl|sQ1257_spl),
% 60.38/9.79 inference(split_clause,[status(thm)],[f68511,f68358,f68379,f68364,f68498])).
% 60.38/9.79 fof(f68696,definition,(
% 60.38/9.79 sQ1268_spl <=> (m1_subset_1(sK4181_skl,u1_struct_0(sK4179_skl)))),
% 60.38/9.79 introduced(definition,[new_symbols(definition,[sQ1268_spl])],[split_symbol_definition])).
% 60.38/9.79 fof(f68698,plain,(
% 60.38/9.79 ~m1_subset_1(sK4181_skl,u1_struct_0(sK4179_skl))|sQ1268_spl),
% 60.38/9.79 inference(component_clause,[status(thm)],[f68696])).
% 60.38/9.79 fof(f68715,plain,(
% 60.38/9.79 $false|sQ1268_spl),
% 60.38/9.79 inference(forward_subsumption_resolution,[status(thm)],[f68698,f59593])).
% 60.38/9.79 fof(f68716,plain,(
% 60.38/9.79 sQ1268_spl),
% 60.38/9.79 inference(contradiction_clause,[status(thm)],[f68715])).
% 60.38/9.79 fof(f68772,definition,(
% 60.38/9.79 sQ1274_spl <=> (m1_subset_1(k3_group_1(sK4179_skl,sK4181_skl),u1_struct_0(sK4179_skl)))),
% 60.38/9.79 introduced(definition,[new_symbols(definition,[sQ1274_spl])],[split_symbol_definition])).
% 60.38/9.79 fof(f68773,plain,(
% 60.38/9.79 m1_subset_1(k3_group_1(sK4179_skl,sK4181_skl),u1_struct_0(sK4179_skl))|~sQ1274_spl),
% 60.38/9.79 inference(component_clause,[status(thm)],[f68772])).
% 60.38/9.79 fof(f68833,plain,(
% 60.38/9.79 v3_struct_0(sK4179_skl)|~v3_group_1(sK4179_skl)|~v4_group_1(sK4179_skl)|~l1_group_1(sK4179_skl)|v4_group_1(sK4180_skl)),
% 60.38/9.79 inference(resolution,[status(thm)],[f40186,f59592])).
% 60.38/9.79 fof(f68836,plain,(
% 60.38/9.79 sQ1247_spl|~sQ1251_spl|~sQ1248_spl|~sQ1249_spl|sQ1256_spl),
% 60.38/9.79 inference(split_clause,[status(thm)],[f68833,f68358,f68379,f68361,f68364,f68495])).
% 60.38/9.79 fof(f70878,plain,(
% 60.38/9.79 v3_struct_0(sK4179_skl)|~v3_group_1(sK4179_skl)|~v4_group_1(sK4179_skl)|~l1_group_1(sK4179_skl)|m1_subset_1(k3_group_1(sK4179_skl,sK4181_skl),u1_struct_0(sK4179_skl))),
% 60.38/9.79 inference(resolution,[status(thm)],[f36622,f59593])).
% 60.38/9.79 fof(f70879,plain,(
% 60.38/9.79 sQ1247_spl|~sQ1251_spl|~sQ1248_spl|~sQ1249_spl|sQ1274_spl),
% 60.38/9.79 inference(split_clause,[status(thm)],[f70878,f68358,f68379,f68361,f68364,f68772])).
% 60.38/9.79 fof(f71500,plain,(
% 60.38/9.79 ![X0]: (v3_struct_0(sK4179_skl)|~v3_group_1(sK4179_skl)|~v4_group_1(sK4179_skl)|~l1_group_1(sK4179_skl)|~m1_group_2(X0,sK4179_skl)|~r1_rlvect_1(X0,sK4181_skl)|r1_rlvect_1(X0,k3_group_1(sK4179_skl,sK4181_skl)))),
% 60.38/9.79 inference(resolution,[status(thm)],[f40357,f59593])).
% 60.38/9.79 fof(f71505,definition,(
% 60.38/9.79 ![X0]: (sQ1464_spl <=> (~m1_group_2(X0,sK4179_skl)|~r1_rlvect_1(X0,sK4181_skl)|r1_rlvect_1(X0,k3_group_1(sK4179_skl,sK4181_skl))))),
% 60.38/9.79 introduced(definition,[new_symbols(definition,[sQ1464_spl])],[split_symbol_definition])).
% 60.38/9.79 fof(f71506,plain,(
% 60.38/9.79 ![X0]: (~m1_group_2(X0,sK4179_skl)|~r1_rlvect_1(X0,sK4181_skl)|r1_rlvect_1(X0,k3_group_1(sK4179_skl,sK4181_skl))|~sQ1464_spl)),
% 60.38/9.79 inference(component_clause,[status(thm)],[f71505])).
% 60.38/9.79 fof(f71508,plain,(
% 60.38/9.79 sQ1247_spl|~sQ1251_spl|~sQ1248_spl|~sQ1249_spl|sQ1464_spl),
% 60.38/9.79 inference(split_clause,[status(thm)],[f71500,f68358,f68379,f68361,f68364,f71505])).
% 60.38/9.79 fof(f71714,plain,(
% 60.38/9.79 ![X0,X1,X2]: (~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|v3_struct_0(X1)|~v3_group_1(X1)|~v4_group_1(X1)|~l1_group_1(X1)|v3_struct_0(X2)|~v3_group_1(X2)|~v4_group_1(X2)|~l1_group_1(X2)|~m1_group_2(X0,X1)|~m1_group_2(X1,X2)|m1_group_2(X0,X2))),
% 60.38/9.79 inference(forward_subsumption_resolution,[status(thm)],[f40373,f40734])).
% 60.38/9.79 fof(f71717,plain,(
% 60.38/9.79 ![X0]: (~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|v3_struct_0(sK4180_skl)|~v3_group_1(sK4180_skl)|~v4_group_1(sK4180_skl)|~l1_group_1(sK4180_skl)|v3_struct_0(sK4179_skl)|~v3_group_1(sK4179_skl)|~v4_group_1(sK4179_skl)|~l1_group_1(sK4179_skl)|~m1_group_2(X0,sK4180_skl)|m1_group_2(X0,sK4179_skl))),
% 60.38/9.79 inference(resolution,[status(thm)],[f71714,f59592])).
% 60.38/9.79 fof(f71733,definition,(
% 60.38/9.79 ![X0]: (sQ1496_spl <=> (~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m1_group_2(X0,sK4180_skl)|m1_group_2(X0,sK4179_skl)))),
% 60.38/9.79 introduced(definition,[new_symbols(definition,[sQ1496_spl])],[split_symbol_definition])).
% 60.38/9.79 fof(f71734,plain,(
% 60.38/9.79 ![X0]: (~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m1_group_2(X0,sK4180_skl)|m1_group_2(X0,sK4179_skl)|~sQ1496_spl)),
% 60.38/9.79 inference(component_clause,[status(thm)],[f71733])).
% 60.38/9.79 fof(f71736,plain,(
% 60.38/9.79 sQ1496_spl|sQ1252_spl|~sQ1253_spl|~sQ1256_spl|~sQ1257_spl|sQ1247_spl|~sQ1251_spl|~sQ1248_spl|~sQ1249_spl),
% 60.38/9.79 inference(split_clause,[status(thm)],[f71717,f71733,f68383,f68392,f68495,f68498,f68358,f68379,f68361,f68364])).
% 60.38/9.79 fof(f71953,definition,(
% 60.38/9.79 sQ1498_spl <=> (m1_group_2(sK4180_skl,sK4179_skl))),
% 60.38/9.79 introduced(definition,[new_symbols(definition,[sQ1498_spl])],[split_symbol_definition])).
% 60.38/9.79 fof(f73749,definition,(
% 60.38/9.79 sQ1573_spl <=> (v1_group_1(sK4180_skl))),
% 60.38/9.79 introduced(definition,[new_symbols(definition,[sQ1573_spl])],[split_symbol_definition])).
% 60.38/9.79 fof(f73751,plain,(
% 60.38/9.79 ~v1_group_1(sK4180_skl)|sQ1573_spl),
% 60.38/9.79 inference(component_clause,[status(thm)],[f73749])).
% 60.38/9.79 fof(f73759,plain,(
% 60.38/9.79 $false|sQ1573_spl),
% 60.38/9.79 inference(forward_subsumption_resolution,[status(thm)],[f73751,f59591])).
% 60.38/9.79 fof(f73760,plain,(
% 60.38/9.79 sQ1573_spl),
% 60.38/9.79 inference(contradiction_clause,[status(thm)],[f73759])).
% 60.38/9.79 fof(f73763,plain,(
% 60.38/9.79 ![X0]: (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_subset_1(X0,u1_struct_0(sK4179_skl))|r2_hidden(X0,k1_funct_1(k1_latsubgr(sK4179_skl),sK4180_skl))|~r1_rlvect_1(sK4180_skl,X0))),
% 60.38/9.79 inference(resolution,[status(thm)],[f59578,f59592])).
% 60.38/9.79 fof(f73773,definition,(
% 60.38/9.79 ![X0]: (sQ1578_spl <=> (~m1_subset_1(X0,u1_struct_0(sK4179_skl))|r2_hidden(X0,k1_funct_1(k1_latsubgr(sK4179_skl),sK4180_skl))|~r1_rlvect_1(sK4180_skl,X0)))),
% 60.38/9.79 introduced(definition,[new_symbols(definition,[sQ1578_spl])],[split_symbol_definition])).
% 60.38/9.79 fof(f73774,plain,(
% 60.38/9.79 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK4179_skl))|r2_hidden(X0,k1_funct_1(k1_latsubgr(sK4179_skl),sK4180_skl))|~r1_rlvect_1(sK4180_skl,X0)|~sQ1578_spl)),
% 60.38/9.79 inference(component_clause,[status(thm)],[f73773])).
% 60.38/9.79 fof(f73776,plain,(
% 60.38/9.79 sQ1247_spl|~sQ1251_spl|~sQ1248_spl|~sQ1249_spl|~sQ1573_spl|sQ1578_spl),
% 60.38/9.79 inference(split_clause,[status(thm)],[f73763,f68358,f68379,f68361,f68364,f73749,f73773])).
% 60.38/9.79 fof(f74235,plain,(
% 60.38/9.79 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(sK4181_skl,u1_struct_0(sK4179_skl))|r1_rlvect_1(sK4180_skl,sK4181_skl)),
% 60.38/9.79 inference(resolution,[status(thm)],[f59594,f59577])).
% 60.38/9.79 fof(f74274,definition,(
% 60.38/9.79 sQ1611_spl <=> (r1_rlvect_1(sK4180_skl,sK4181_skl))),
% 60.38/9.79 introduced(definition,[new_symbols(definition,[sQ1611_spl])],[split_symbol_definition])).
% 60.38/9.79 fof(f74275,plain,(
% 60.38/9.79 r1_rlvect_1(sK4180_skl,sK4181_skl)|~sQ1611_spl),
% 60.38/9.79 inference(component_clause,[status(thm)],[f74274])).
% 60.38/9.79 fof(f74277,plain,(
% 60.38/9.79 sQ1247_spl|~sQ1251_spl|~sQ1248_spl|~sQ1249_spl|~sQ1573_spl|~sQ1498_spl|~sQ1268_spl|sQ1611_spl),
% 60.38/9.79 inference(split_clause,[status(thm)],[f74235,f68358,f68379,f68361,f68364,f73749,f71953,f68696,f74274])).
% 60.38/9.79 fof(f77468,plain,(
% 60.38/9.79 ~m1_group_2(sK4180_skl,sK4179_skl)|r1_rlvect_1(sK4180_skl,k3_group_1(sK4179_skl,sK4181_skl))|~sQ1464_spl|~sQ1611_spl),
% 60.38/9.79 inference(resolution,[status(thm)],[f71506,f74275])).
% 60.38/9.79 fof(f77469,definition,(
% 60.38/9.79 sQ1779_spl <=> (r1_rlvect_1(sK4180_skl,k3_group_1(sK4179_skl,sK4181_skl)))),
% 60.38/9.79 introduced(definition,[new_symbols(definition,[sQ1779_spl])],[split_symbol_definition])).
% 60.38/9.79 fof(f77472,plain,(
% 60.38/9.79 ~sQ1498_spl|sQ1779_spl|~sQ1464_spl|~sQ1611_spl),
% 61.55/10.01 inference(split_clause,[status(thm)],[f77468,f71953,f77469,f71505,f74274])).
% 61.55/10.01 fof(f78910,plain,(
% 61.55/10.01 ~v3_group_1(sK4180_skl)|~v4_group_1(sK4180_skl)|~l1_group_1(sK4180_skl)|m1_group_2(sK4180_skl,sK4179_skl)|~sQ1496_spl|~sQ1258_spl),
% 61.55/10.01 inference(resolution,[status(thm)],[f71734,f68502])).
% 61.55/10.01 fof(f78912,plain,(
% 61.55/10.01 ~sQ1253_spl|~sQ1256_spl|~sQ1257_spl|sQ1498_spl|~sQ1496_spl|~sQ1258_spl),
% 61.55/10.01 inference(split_clause,[status(thm)],[f78910,f68392,f68495,f68498,f71953,f71733,f68501])).
% 61.55/10.01 fof(f79833,plain,(
% 61.55/10.01 r2_hidden(k3_group_1(sK4179_skl,sK4181_skl),k1_funct_1(k1_latsubgr(sK4179_skl),sK4180_skl))|~r1_rlvect_1(sK4180_skl,k3_group_1(sK4179_skl,sK4181_skl))|~sQ1578_spl|~sQ1274_spl),
% 61.55/10.01 inference(resolution,[status(thm)],[f73774,f68773])).
% 61.55/10.01 fof(f79862,definition,(
% 61.55/10.01 sQ1923_spl <=> (r2_hidden(k3_group_1(sK4179_skl,sK4181_skl),k1_funct_1(k1_latsubgr(sK4179_skl),sK4180_skl)))),
% 61.55/10.01 introduced(definition,[new_symbols(definition,[sQ1923_spl])],[split_symbol_definition])).
% 61.55/10.01 fof(f79863,plain,(
% 61.55/10.01 r2_hidden(k3_group_1(sK4179_skl,sK4181_skl),k1_funct_1(k1_latsubgr(sK4179_skl),sK4180_skl))|~sQ1923_spl),
% 61.55/10.01 inference(component_clause,[status(thm)],[f79862])).
% 61.55/10.01 fof(f79865,plain,(
% 61.55/10.01 sQ1923_spl|~sQ1779_spl|~sQ1578_spl|~sQ1274_spl),
% 61.55/10.01 inference(split_clause,[status(thm)],[f79833,f79862,f77469,f73773,f68772])).
% 61.55/10.01 fof(f79946,plain,(
% 61.55/10.01 $false|~sQ1923_spl),
% 61.55/10.01 inference(forward_subsumption_resolution,[status(thm)],[f79863,f59595])).
% 61.55/10.01 fof(f79947,plain,(
% 61.55/10.01 ~sQ1923_spl),
% 61.55/10.01 inference(contradiction_clause,[status(thm)],[f79946])).
% 61.55/10.01 fof(f79948,plain,(
% 61.55/10.01 $false),
% 61.55/10.01 inference(sat_refutation,[status(thm)],[f68372,f68374,f68376,f68386,f68388,f68395,f68504,f68514,f68716,f68836,f70879,f71508,f71736,f73760,f73776,f74277,f77472,f78912,f79865,f79947])).
% 61.55/10.01 % SZS output end CNFRefutation for theBenchmark.p
% 39.72/10.10 % Elapsed time: 9.624449 seconds
% 39.72/10.10 % CPU time: 61.211530 seconds
% 39.72/10.10 % Total memory used: 4.087 GB
% 39.72/10.10 % Net memory used: 4.031 GB
%------------------------------------------------------------------------------