%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP628+1 : 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 : n015.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:36:57 PM UTC 2026
% Result : Theorem 0.21s 10.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP628+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/10.45 % Computer : n015.cluster.edu
% 0.18/10.45 % Model : x86_64 x86_64
% 0.18/10.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/10.45 % Memory : 8046.5625MB
% 0.18/10.45 % OS : Linux 6.8.0-71-generic
% 0.18/10.45 % CPULimit : 300
% 0.18/10.45 % WCLimit : 300
% 0.18/10.45 % DateTime : Sun Sep 20 20:24:16 UTC 2026
% 0.18/10.45 % CPUTime :
% 0.18/10.47 % Drodi V4.1.1
% 0.21/10.60 % Refutation found
% 0.21/10.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.21/10.60 % SZS output start CNFRefutation for theBenchmark
% 0.21/10.60 fof(f1,conjecture,(
% 0.21/10.60 (! [A] :( ( ~ v3_struct_0(A)& v1_group_1(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k4_autgroup(A))=> (! [C] :( m1_subset_1(C,u1_struct_0(k5_autgroup(A)))=> ( B = C=> k2_funct_1(B) = k3_group_1(k5_autgroup(A),C) ) ) )) )) )),
% 0.21/10.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/10.60 fof(f2,negated_conjecture,(
% 0.21/10.60 ~((! [A] :( ( ~ v3_struct_0(A)& v1_group_1(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k4_autgroup(A))=> (! [C] :( m1_subset_1(C,u1_struct_0(k5_autgroup(A)))=> ( B = C=> k2_funct_1(B) = k3_group_1(k5_autgroup(A),C) ) ) )) )) ))),
% 0.21/10.60 inference(negated_conjecture,[status(cth)],[f1])).
% 0.21/10.60 fof(f22,axiom,(
% 0.21/10.60 (! [A] :( ( ~ v3_struct_0(A)& v1_group_1(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> ( ~ v3_struct_0(k3_autgroup(A))& v1_group_1(k3_autgroup(A))& v3_group_1(k3_autgroup(A))& v4_group_1(k3_autgroup(A))& l1_group_1(k3_autgroup(A)) ) ) )),
% 0.21/10.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/10.60 fof(f25,axiom,(
% 0.21/10.60 (! [A] :( ( ~ v3_struct_0(A)& v1_group_1(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> ( v1_group_1(k5_autgroup(A))& v1_group_3(k5_autgroup(A),k3_autgroup(A))& m1_group_2(k5_autgroup(A),k3_autgroup(A)) ) ) )),
% 0.21/10.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/10.60 fof(f49,axiom,(
% 0.21/10.60 (? [A] :( v1_relat_1(A)& v1_funct_1(A) ) )),
% 0.21/10.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/10.60 fof(f51,axiom,(
% 0.21/10.60 (? [A] :( l1_group_1(A)& v1_group_1(A) ) )),
% 0.21/10.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/10.60 fof(f54,axiom,(
% 0.21/10.60 (? [A] :( v1_relat_1(A)& v1_funct_1(A)& v2_funct_1(A)& v1_xboole_0(A) ) )),
% 0.21/10.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/10.60 fof(f67,axiom,(
% 0.21/10.60 (! [A] :( ( ~ v3_struct_0(A)& v1_group_1(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k1_autgroup(A))=> (! [C] :( m1_subset_1(C,u1_struct_0(k3_autgroup(A)))=> ( B = C=> k2_funct_1(B) = k3_group_1(k3_autgroup(A),C) ) ) )) )) )),
% 0.21/10.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/10.60 fof(f68,axiom,(
% 0.21/10.60 (! [A] :( ( ~ v3_struct_0(A)& v1_group_1(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k4_autgroup(A))=> m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k1_autgroup(A)) ) )) )),
% 0.21/10.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/10.60 fof(f73,axiom,(
% 0.21/10.60 (! [A] :( ( ~ v3_struct_0(A)& v3_group_1(A)& l1_group_1(A) )=> (! [B] :( m1_group_2(B,A)=> (! [C] :( m1_subset_1(C,u1_struct_0(B))=> m1_subset_1(C,u1_struct_0(A)) ) )) )) )),
% 0.21/10.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/10.60 fof(f74,axiom,(
% 0.21/10.60 (! [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)=> (! [D] :( m1_subset_1(D,u1_struct_0(C))=> ( D = B=> k3_group_1(C,D) = k3_group_1(A,B) ) ) )) )) )) )),
% 0.21/10.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.21/10.60 fof(f79,plain,(
% 0.21/10.60 (?[A]: (((((~v3_struct_0(A)&v1_group_1(A))&v3_group_1(A))&v4_group_1(A))&l1_group_1(A))&(?[B]: (m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k4_autgroup(A))&(?[C]: (m1_subset_1(C,u1_struct_0(k5_autgroup(A)))&(B=C&~k2_funct_1(B)=k3_group_1(k5_autgroup(A),C))))))))),
% 0.21/10.60 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.21/10.60 fof(f80,plain,(
% 0.21/10.60 (((((~v3_struct_0(sK0_skl)&v1_group_1(sK0_skl))&v3_group_1(sK0_skl))&v4_group_1(sK0_skl))&l1_group_1(sK0_skl))&(m2_fraenkel(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k4_autgroup(sK0_skl))&(m1_subset_1(sK2_skl,u1_struct_0(k5_autgroup(sK0_skl)))&(sK1_skl=sK2_skl&~k2_funct_1(sK1_skl)=k3_group_1(k5_autgroup(sK0_skl),sK2_skl)))))),
% 0.21/10.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl),skolemize(C,sK2_skl)],[f79])).
% 0.21/10.60 fof(f81,plain,(
% 0.21/10.60 ~v3_struct_0(sK0_skl)),
% 0.21/10.60 inference(cnf_transformation,[status(thm)],[f80])).
% 0.21/10.60 fof(f82,plain,(
% 0.21/10.60 v1_group_1(sK0_skl)),
% 0.21/10.60 inference(cnf_transformation,[status(thm)],[f80])).
% 0.21/10.60 fof(f83,plain,(
% 0.21/10.60 v3_group_1(sK0_skl)),
% 0.21/10.60 inference(cnf_transformation,[status(thm)],[f80])).
% 0.21/10.60 fof(f84,plain,(
% 0.21/10.60 v4_group_1(sK0_skl)),
% 0.21/10.60 inference(cnf_transformation,[status(thm)],[f80])).
% 0.21/10.60 fof(f85,plain,(
% 0.21/10.60 l1_group_1(sK0_skl)),
% 0.21/10.60 inference(cnf_transformation,[status(thm)],[f80])).
% 0.21/10.60 fof(f86,plain,(
% 0.21/10.60 m2_fraenkel(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k4_autgroup(sK0_skl))),
% 0.21/10.60 inference(cnf_transformation,[status(thm)],[f80])).
% 0.21/10.60 fof(f87,plain,(
% 0.21/10.60 m1_subset_1(sK2_skl,u1_struct_0(k5_autgroup(sK0_skl)))),
% 0.21/10.60 inference(cnf_transformation,[status(thm)],[f80])).
% 0.21/10.60 fof(f88,plain,(
% 0.21/10.60 sK1_skl=sK2_skl),
% 0.21/10.60 inference(cnf_transformation,[status(thm)],[f80])).
% 0.21/10.60 fof(f89,plain,(
% 0.21/10.60 ~k2_funct_1(sK1_skl)=k3_group_1(k5_autgroup(sK0_skl),sK2_skl)),
% 0.21/10.60 inference(cnf_transformation,[status(thm)],[f80])).
% 0.21/10.60 fof(f138,plain,(
% 0.21/10.60 ![A]: (((((v3_struct_0(A)|~v1_group_1(A))|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|((((~v3_struct_0(k3_autgroup(A))&v1_group_1(k3_autgroup(A)))&v3_group_1(k3_autgroup(A)))&v4_group_1(k3_autgroup(A)))&l1_group_1(k3_autgroup(A))))),
% 0.21/10.60 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 0.21/10.60 fof(f139,plain,(
% 0.21/10.60 ![X0]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~v3_struct_0(k3_autgroup(X0)))),
% 0.21/10.60 inference(cnf_transformation,[status(thm)],[f138])).
% 0.21/10.60 fof(f141,plain,(
% 0.21/10.60 ![X0]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|v3_group_1(k3_autgroup(X0)))),
% 0.21/10.60 inference(cnf_transformation,[status(thm)],[f138])).
% 0.21/10.60 fof(f142,plain,(
% 0.21/10.60 ![X0]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|v4_group_1(k3_autgroup(X0)))),
% 0.21/10.60 inference(cnf_transformation,[status(thm)],[f138])).
% 0.21/10.60 fof(f143,plain,(
% 0.21/10.60 ![X0]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|l1_group_1(k3_autgroup(X0)))),
% 0.21/10.60 inference(cnf_transformation,[status(thm)],[f138])).
% 0.21/10.60 fof(f148,plain,(
% 0.21/10.60 ![A]: (((((v3_struct_0(A)|~v1_group_1(A))|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|((v1_group_1(k5_autgroup(A))&v1_group_3(k5_autgroup(A),k3_autgroup(A)))&m1_group_2(k5_autgroup(A),k3_autgroup(A))))),
% 0.21/10.60 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 0.21/10.60 fof(f151,plain,(
% 0.21/10.60 ![X0]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|m1_group_2(k5_autgroup(X0),k3_autgroup(X0)))),
% 0.21/10.60 inference(cnf_transformation,[status(thm)],[f148])).
% 0.21/10.60 fof(f202,plain,(
% 0.21/10.60 (v1_relat_1(sK12_skl)&v1_funct_1(sK12_skl))),
% 0.21/10.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(A,sK12_skl)],[f49])).
% 0.21/10.60 fof(f203,plain,(
% 0.21/10.60 v1_relat_1(sK12_skl)),
% 0.21/10.60 inference(cnf_transformation,[status(thm)],[f202])).
% 0.21/10.60 fof(f210,plain,(
% 0.21/10.60 (l1_group_1(sK14_skl)&v1_group_1(sK14_skl))),
% 0.21/10.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(A,sK14_skl)],[f51])).
% 0.21/10.60 fof(f212,plain,(
% 0.21/10.60 v1_group_1(sK14_skl)),
% 0.21/10.60 inference(cnf_transformation,[status(thm)],[f210])).
% 0.21/10.60 fof(f230,plain,(
% 0.21/10.60 (((v1_relat_1(sK17_skl)&v1_funct_1(sK17_skl))&v2_funct_1(sK17_skl))&v1_xboole_0(sK17_skl))),
% 0.21/10.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl]),skolemize(A,sK17_skl)],[f54])).
% 0.21/10.60 fof(f231,plain,(
% 0.21/10.60 v1_relat_1(sK17_skl)),
% 0.21/10.60 inference(cnf_transformation,[status(thm)],[f230])).
% 0.21/10.60 fof(f280,plain,(
% 0.21/10.60 ![A]: (((((v3_struct_0(A)|~v1_group_1(A))|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|(![B]: (~m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k1_autgroup(A))|(![C]: (~m1_subset_1(C,u1_struct_0(k3_autgroup(A)))|(~B=C|k2_funct_1(B)=k3_group_1(k3_autgroup(A),C)))))))),
% 0.21/10.60 inference(pre_NNF_transformation,[status(thm)],[f67])).
% 0.21/10.60 fof(f281,plain,(
% 0.21/10.60 ![X0,X1,X2]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))|~m1_subset_1(X2,u1_struct_0(k3_autgroup(X0)))|~X1=X2|k2_funct_1(X1)=k3_group_1(k3_autgroup(X0),X2))),
% 0.21/10.60 inference(cnf_transformation,[status(thm)],[f280])).
% 0.21/10.60 fof(f282,plain,(
% 0.21/10.60 ![A]: (((((v3_struct_0(A)|~v1_group_1(A))|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|(![B]: (~m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k4_autgroup(A))|m2_fraenkel(B,u1_struct_0(A),u1_struct_0(A),k1_autgroup(A)))))),
% 0.21/10.60 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 0.21/10.60 fof(f283,plain,(
% 0.21/10.60 ![X0,X1]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k4_autgroup(X0))|m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0)))),
% 0.21/10.60 inference(cnf_transformation,[status(thm)],[f282])).
% 0.21/10.60 fof(f295,plain,(
% 0.21/10.60 ![A]: (((v3_struct_0(A)|~v3_group_1(A))|~l1_group_1(A))|(![B]: (~m1_group_2(B,A)|(![C]: (~m1_subset_1(C,u1_struct_0(B))|m1_subset_1(C,u1_struct_0(A)))))))),
% 0.21/10.60 inference(pre_NNF_transformation,[status(thm)],[f73])).
% 0.21/10.60 fof(f296,plain,(
% 0.21/10.60 ![X0,X1,X2]: (v3_struct_0(X0)|~v3_group_1(X0)|~l1_group_1(X0)|~m1_group_2(X1,X0)|~m1_subset_1(X2,u1_struct_0(X1))|m1_subset_1(X2,u1_struct_0(X0)))),
% 0.21/10.60 inference(cnf_transformation,[status(thm)],[f295])).
% 0.21/10.60 fof(f297,plain,(
% 0.21/10.60 ![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)|(![D]: (~m1_subset_1(D,u1_struct_0(C))|(~D=B|k3_group_1(C,D)=k3_group_1(A,B)))))))))),
% 0.21/10.60 inference(pre_NNF_transformation,[status(thm)],[f74])).
% 0.21/10.60 fof(f298,plain,(
% 0.21/10.60 ![X0,X1,X2,X3]: (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)|~m1_subset_1(X3,u1_struct_0(X2))|~X3=X1|k3_group_1(X2,X3)=k3_group_1(X0,X1))),
% 0.21/10.60 inference(cnf_transformation,[status(thm)],[f297])).
% 0.21/10.60 fof(f310,plain,(
% 0.21/10.60 m1_subset_1(sK1_skl,u1_struct_0(k5_autgroup(sK0_skl)))),
% 0.21/10.60 inference(backward_demodulation,[status(thm)],[f88,f87])).
% 0.21/10.60 fof(f311,plain,(
% 0.21/10.60 ~k2_funct_1(sK1_skl)=k3_group_1(k5_autgroup(sK0_skl),sK1_skl)),
% 0.21/10.60 inference(forward_demodulation,[status(thm)],[f88,f89])).
% 0.21/10.60 fof(f314,plain,(
% 0.21/10.60 ![X0,X1]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m2_fraenkel(X1,u1_struct_0(X0),u1_struct_0(X0),k1_autgroup(X0))|~m1_subset_1(X1,u1_struct_0(k3_autgroup(X0)))|k2_funct_1(X1)=k3_group_1(k3_autgroup(X0),X1))),
% 0.21/10.61 inference(destructive_equality_resolution,[status(thm)],[f281])).
% 0.21/10.61 fof(f315,plain,(
% 0.21/10.61 ![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)|~m1_subset_1(X1,u1_struct_0(X2))|k3_group_1(X2,X1)=k3_group_1(X0,X1))),
% 0.21/10.61 inference(destructive_equality_resolution,[status(thm)],[f298])).
% 0.21/10.61 fof(f316,plain,(
% 0.21/10.61 ![X0,X1,X2]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m1_group_2(X1,X0)|~m1_subset_1(X2,u1_struct_0(X1))|k3_group_1(X1,X2)=k3_group_1(X0,X2))),
% 0.21/10.61 inference(forward_subsumption_resolution,[status(thm)],[f315,f296])).
% 0.21/10.61 fof(f326,definition,(
% 0.21/10.61 sQ2_spl <=> (v1_group_1(sK0_skl))),
% 0.21/10.61 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.21/10.61 fof(f328,plain,(
% 0.21/10.61 ~v1_group_1(sK0_skl)|sQ2_spl),
% 0.21/10.61 inference(component_clause,[status(thm)],[f326])).
% 0.21/10.61 fof(f333,plain,(
% 0.21/10.61 $false|sQ2_spl),
% 0.21/10.61 inference(forward_subsumption_resolution,[status(thm)],[f328,f82])).
% 0.21/10.61 fof(f334,plain,(
% 0.21/10.61 sQ2_spl),
% 0.21/10.61 inference(contradiction_clause,[status(thm)],[f333])).
% 0.21/10.61 fof(f371,definition,(
% 0.21/10.61 sQ13_spl <=> (v3_struct_0(sK0_skl))),
% 0.21/10.61 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.21/10.61 fof(f372,plain,(
% 0.21/10.61 v3_struct_0(sK0_skl)|~sQ13_spl),
% 0.21/10.61 inference(component_clause,[status(thm)],[f371])).
% 0.21/10.61 fof(f374,definition,(
% 0.21/10.61 sQ14_spl <=> (v3_group_1(sK0_skl))),
% 0.21/10.61 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.21/10.61 fof(f376,plain,(
% 0.21/10.61 ~v3_group_1(sK0_skl)|sQ14_spl),
% 0.21/10.61 inference(component_clause,[status(thm)],[f374])).
% 0.21/10.61 fof(f377,definition,(
% 0.21/10.61 sQ15_spl <=> (v4_group_1(sK0_skl))),
% 0.21/10.61 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.21/10.61 fof(f379,plain,(
% 0.21/10.61 ~v4_group_1(sK0_skl)|sQ15_spl),
% 0.21/10.61 inference(component_clause,[status(thm)],[f377])).
% 0.21/10.61 fof(f381,plain,(
% 0.21/10.61 $false|sQ15_spl),
% 0.21/10.61 inference(forward_subsumption_resolution,[status(thm)],[f379,f84])).
% 0.21/10.61 fof(f382,plain,(
% 0.21/10.61 sQ15_spl),
% 0.21/10.61 inference(contradiction_clause,[status(thm)],[f381])).
% 0.21/10.61 fof(f383,plain,(
% 0.21/10.61 $false|sQ14_spl),
% 0.21/10.61 inference(forward_subsumption_resolution,[status(thm)],[f376,f83])).
% 0.21/10.61 fof(f384,plain,(
% 0.21/10.61 sQ14_spl),
% 0.21/10.61 inference(contradiction_clause,[status(thm)],[f383])).
% 0.21/10.61 fof(f395,plain,(
% 0.21/10.61 $false|~sQ13_spl),
% 0.21/10.61 inference(forward_subsumption_resolution,[status(thm)],[f372,f81])).
% 0.21/10.61 fof(f396,plain,(
% 0.21/10.61 ~sQ13_spl),
% 0.21/10.61 inference(contradiction_clause,[status(thm)],[f395])).
% 0.21/10.61 fof(f398,plain,(
% 0.21/10.61 v3_struct_0(sK0_skl)|~v1_group_1(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|m1_group_2(k5_autgroup(sK0_skl),k3_autgroup(sK0_skl))),
% 0.21/10.61 inference(resolution,[status(thm)],[f151,f85])).
% 0.21/10.61 fof(f403,definition,(
% 0.21/10.61 sQ19_spl <=> (m1_group_2(k5_autgroup(sK0_skl),k3_autgroup(sK0_skl)))),
% 0.21/10.61 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.21/10.61 fof(f404,plain,(
% 0.21/10.61 m1_group_2(k5_autgroup(sK0_skl),k3_autgroup(sK0_skl))|~sQ19_spl),
% 0.21/10.61 inference(component_clause,[status(thm)],[f403])).
% 0.21/10.61 fof(f406,plain,(
% 0.21/10.61 sQ13_spl|~sQ2_spl|~sQ14_spl|~sQ15_spl|sQ19_spl),
% 0.21/10.61 inference(split_clause,[status(thm)],[f398,f371,f326,f374,f377,f403])).
% 0.21/10.61 fof(f407,plain,(
% 0.21/10.61 v3_struct_0(sK0_skl)|~v1_group_1(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|m2_fraenkel(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))),
% 0.21/10.61 inference(resolution,[status(thm)],[f283,f86])).
% 0.21/10.61 fof(f408,definition,(
% 0.21/10.61 sQ20_spl <=> (l1_group_1(sK0_skl))),
% 0.21/10.61 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.21/10.61 fof(f410,plain,(
% 0.21/10.61 ~l1_group_1(sK0_skl)|sQ20_spl),
% 0.21/10.61 inference(component_clause,[status(thm)],[f408])).
% 0.21/10.61 fof(f411,definition,(
% 0.21/10.61 sQ21_spl <=> (m2_fraenkel(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl)))),
% 0.21/10.61 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.21/10.61 fof(f412,plain,(
% 0.21/10.61 m2_fraenkel(sK1_skl,u1_struct_0(sK0_skl),u1_struct_0(sK0_skl),k1_autgroup(sK0_skl))|~sQ21_spl),
% 0.21/10.61 inference(component_clause,[status(thm)],[f411])).
% 0.21/10.61 fof(f414,plain,(
% 0.21/10.61 sQ13_spl|~sQ2_spl|~sQ14_spl|~sQ15_spl|~sQ20_spl|sQ21_spl),
% 0.21/10.61 inference(split_clause,[status(thm)],[f407,f371,f326,f374,f377,f408,f411])).
% 0.21/10.61 fof(f415,plain,(
% 0.21/10.61 $false|sQ20_spl),
% 0.21/10.61 inference(forward_subsumption_resolution,[status(thm)],[f410,f85])).
% 0.21/10.61 fof(f416,plain,(
% 0.21/10.61 sQ20_spl),
% 0.21/10.61 inference(contradiction_clause,[status(thm)],[f415])).
% 0.21/10.61 fof(f606,plain,(
% 0.21/10.61 v3_struct_0(sK0_skl)|~v1_group_1(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|v3_group_1(k3_autgroup(sK0_skl))),
% 0.21/10.61 inference(resolution,[status(thm)],[f141,f85])).
% 0.21/10.61 fof(f611,definition,(
% 0.21/10.61 sQ61_spl <=> (v3_group_1(k3_autgroup(sK0_skl)))),
% 0.21/10.61 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.21/10.61 fof(f614,plain,(
% 0.21/10.61 sQ13_spl|~sQ2_spl|~sQ14_spl|~sQ15_spl|sQ61_spl),
% 0.21/10.61 inference(split_clause,[status(thm)],[f606,f371,f326,f374,f377,f611])).
% 0.21/10.61 fof(f616,plain,(
% 0.21/10.61 v3_struct_0(sK0_skl)|~v1_group_1(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|v4_group_1(k3_autgroup(sK0_skl))),
% 0.21/10.61 inference(resolution,[status(thm)],[f142,f85])).
% 0.21/10.61 fof(f621,definition,(
% 0.21/10.61 sQ63_spl <=> (v4_group_1(k3_autgroup(sK0_skl)))),
% 0.21/10.61 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.21/10.61 fof(f624,plain,(
% 0.21/10.61 sQ13_spl|~sQ2_spl|~sQ14_spl|~sQ15_spl|sQ63_spl),
% 0.21/10.61 inference(split_clause,[status(thm)],[f616,f371,f326,f374,f377,f621])).
% 0.21/10.61 fof(f626,plain,(
% 0.21/10.61 v3_struct_0(sK0_skl)|~v1_group_1(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|l1_group_1(k3_autgroup(sK0_skl))),
% 0.21/10.61 inference(resolution,[status(thm)],[f143,f85])).
% 0.21/10.61 fof(f631,definition,(
% 0.21/10.61 sQ65_spl <=> (l1_group_1(k3_autgroup(sK0_skl)))),
% 0.21/10.61 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.21/10.61 fof(f634,plain,(
% 0.21/10.61 sQ13_spl|~sQ2_spl|~sQ14_spl|~sQ15_spl|sQ65_spl),
% 0.21/10.61 inference(split_clause,[status(thm)],[f626,f371,f326,f374,f377,f631])).
% 0.21/10.61 fof(f660,plain,(
% 0.21/10.61 ![X0]: (v3_struct_0(X0)|~v3_group_1(X0)|~l1_group_1(X0)|~m1_group_2(k5_autgroup(sK0_skl),X0)|m1_subset_1(sK1_skl,u1_struct_0(X0)))),
% 0.21/10.61 inference(resolution,[status(thm)],[f310,f296])).
% 0.21/10.61 fof(f661,plain,(
% 0.21/10.61 ![X0]: (v3_struct_0(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m1_group_2(k5_autgroup(sK0_skl),X0)|k3_group_1(k5_autgroup(sK0_skl),sK1_skl)=k3_group_1(X0,sK1_skl))),
% 0.21/10.61 inference(resolution,[status(thm)],[f310,f316])).
% 0.21/10.61 fof(f732,plain,(
% 0.21/10.61 v3_struct_0(k3_autgroup(sK0_skl))|~v3_group_1(k3_autgroup(sK0_skl))|~v4_group_1(k3_autgroup(sK0_skl))|~l1_group_1(k3_autgroup(sK0_skl))|k3_group_1(k5_autgroup(sK0_skl),sK1_skl)=k3_group_1(k3_autgroup(sK0_skl),sK1_skl)|~sQ19_spl),
% 0.21/10.61 inference(resolution,[status(thm)],[f404,f661])).
% 0.21/10.61 fof(f733,plain,(
% 0.21/10.61 v3_struct_0(k3_autgroup(sK0_skl))|~v3_group_1(k3_autgroup(sK0_skl))|~l1_group_1(k3_autgroup(sK0_skl))|m1_subset_1(sK1_skl,u1_struct_0(k3_autgroup(sK0_skl)))|~sQ19_spl),
% 0.21/10.61 inference(resolution,[status(thm)],[f404,f660])).
% 0.21/10.61 fof(f737,definition,(
% 0.21/10.61 sQ87_spl <=> (v3_struct_0(k3_autgroup(sK0_skl)))),
% 0.21/10.61 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 0.21/10.61 fof(f738,plain,(
% 0.21/10.61 v3_struct_0(k3_autgroup(sK0_skl))|~sQ87_spl),
% 0.21/10.61 inference(component_clause,[status(thm)],[f737])).
% 0.21/10.61 fof(f740,definition,(
% 0.21/10.61 sQ88_spl <=> (k3_group_1(k5_autgroup(sK0_skl),sK1_skl)=k3_group_1(k3_autgroup(sK0_skl),sK1_skl))),
% 0.21/10.61 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 0.21/10.61 fof(f741,plain,(
% 0.21/10.61 k3_group_1(k5_autgroup(sK0_skl),sK1_skl)=k3_group_1(k3_autgroup(sK0_skl),sK1_skl)|~sQ88_spl),
% 0.21/10.61 inference(component_clause,[status(thm)],[f740])).
% 0.21/10.61 fof(f743,plain,(
% 0.21/10.61 sQ87_spl|~sQ61_spl|~sQ63_spl|~sQ65_spl|sQ88_spl|~sQ19_spl),
% 0.21/10.61 inference(split_clause,[status(thm)],[f732,f737,f611,f621,f631,f740,f403])).
% 0.21/10.61 fof(f744,definition,(
% 0.21/10.61 sQ89_spl <=> (m1_subset_1(sK1_skl,u1_struct_0(k3_autgroup(sK0_skl))))),
% 0.21/10.61 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.21/10.61 fof(f747,plain,(
% 0.21/10.61 sQ87_spl|~sQ61_spl|~sQ65_spl|sQ89_spl|~sQ19_spl),
% 0.21/10.61 inference(split_clause,[status(thm)],[f733,f737,f611,f631,f744,f403])).
% 0.21/10.61 fof(f751,plain,(
% 0.21/10.61 v3_struct_0(sK0_skl)|~v1_group_1(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~m1_subset_1(sK1_skl,u1_struct_0(k3_autgroup(sK0_skl)))|k2_funct_1(sK1_skl)=k3_group_1(k3_autgroup(sK0_skl),sK1_skl)|~sQ21_spl),
% 0.21/10.61 inference(resolution,[status(thm)],[f412,f314])).
% 0.21/10.61 fof(f756,definition,(
% 0.21/10.61 sQ90_spl <=> (k2_funct_1(sK1_skl)=k3_group_1(k3_autgroup(sK0_skl),sK1_skl))),
% 0.21/10.61 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 0.21/10.61 fof(f757,plain,(
% 0.21/10.61 k2_funct_1(sK1_skl)=k3_group_1(k3_autgroup(sK0_skl),sK1_skl)|~sQ90_spl),
% 0.21/10.61 inference(component_clause,[status(thm)],[f756])).
% 0.21/10.61 fof(f759,plain,(
% 0.21/10.61 sQ13_spl|~sQ2_spl|~sQ14_spl|~sQ15_spl|~sQ20_spl|~sQ89_spl|sQ90_spl|~sQ21_spl),
% 0.21/10.61 inference(split_clause,[status(thm)],[f751,f371,f326,f374,f377,f408,f744,f756,f411])).
% 0.21/10.61 fof(f767,plain,(
% 0.21/10.61 k3_group_1(k5_autgroup(sK0_skl),sK1_skl)=k2_funct_1(sK1_skl)|~sQ90_spl|~sQ88_spl),
% 0.21/10.61 inference(backward_demodulation,[status(thm)],[f757,f741])).
% 0.21/10.61 fof(f768,plain,(
% 0.21/10.61 $false|~sQ90_spl|~sQ88_spl),
% 0.21/10.61 inference(forward_subsumption_resolution,[status(thm)],[f767,f311])).
% 0.21/10.61 fof(f769,plain,(
% 0.21/10.61 ~sQ90_spl|~sQ88_spl),
% 0.21/10.61 inference(contradiction_clause,[status(thm)],[f768])).
% 0.21/10.61 fof(f1208,definition,(
% 0.21/10.61 sQ179_spl <=> (v1_relat_1(sK12_skl))),
% 0.21/10.61 introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition])).
% 0.21/10.61 fof(f1210,plain,(
% 0.21/10.61 ~v1_relat_1(sK12_skl)|sQ179_spl),
% 0.21/10.61 inference(component_clause,[status(thm)],[f1208])).
% 0.21/10.61 fof(f1219,plain,(
% 0.21/10.61 $false|sQ179_spl),
% 0.21/10.61 inference(forward_subsumption_resolution,[status(thm)],[f1210,f203])).
% 0.21/10.61 fof(f1220,plain,(
% 0.21/10.61 sQ179_spl),
% 0.21/10.61 inference(contradiction_clause,[status(thm)],[f1219])).
% 0.21/10.61 fof(f1261,definition,(
% 0.21/10.61 sQ186_spl <=> (v1_group_1(sK14_skl))),
% 0.21/10.61 introduced(definition,[new_symbols(definition,[sQ186_spl])],[split_symbol_definition])).
% 0.21/10.61 fof(f1263,plain,(
% 0.21/10.61 ~v1_group_1(sK14_skl)|sQ186_spl),
% 0.21/10.61 inference(component_clause,[status(thm)],[f1261])).
% 0.21/10.61 fof(f1368,plain,(
% 0.21/10.61 $false|sQ186_spl),
% 0.21/10.61 inference(forward_subsumption_resolution,[status(thm)],[f1263,f212])).
% 0.21/10.61 fof(f1369,plain,(
% 0.21/10.61 sQ186_spl),
% 0.21/10.61 inference(contradiction_clause,[status(thm)],[f1368])).
% 0.21/10.61 fof(f1890,definition,(
% 0.21/10.61 sQ318_spl <=> (v1_relat_1(sK17_skl))),
% 0.21/10.61 introduced(definition,[new_symbols(definition,[sQ318_spl])],[split_symbol_definition])).
% 0.21/10.62 fof(f1892,plain,(
% 0.21/10.62 ~v1_relat_1(sK17_skl)|sQ318_spl),
% 0.21/10.62 inference(component_clause,[status(thm)],[f1890])).
% 0.21/10.62 fof(f1901,plain,(
% 0.21/10.62 $false|sQ318_spl),
% 0.21/10.62 inference(forward_subsumption_resolution,[status(thm)],[f1892,f231])).
% 0.21/10.62 fof(f1902,plain,(
% 0.21/10.62 sQ318_spl),
% 0.21/10.62 inference(contradiction_clause,[status(thm)],[f1901])).
% 0.21/10.62 fof(f1920,plain,(
% 0.21/10.62 v3_struct_0(sK0_skl)|~v1_group_1(sK0_skl)|~v3_group_1(sK0_skl)|~v4_group_1(sK0_skl)|~l1_group_1(sK0_skl)|~sQ87_spl),
% 0.21/10.62 inference(resolution,[status(thm)],[f139,f738])).
% 0.21/10.62 fof(f1925,plain,(
% 0.21/10.62 sQ13_spl|~sQ2_spl|~sQ14_spl|~sQ15_spl|~sQ20_spl|~sQ87_spl),
% 0.21/10.62 inference(split_clause,[status(thm)],[f1920,f371,f326,f374,f377,f408,f737])).
% 0.21/10.62 fof(f1926,plain,(
% 0.21/10.62 $false),
% 0.21/10.62 inference(sat_refutation,[status(thm)],[f334,f382,f384,f396,f406,f414,f416,f614,f624,f634,f743,f747,f759,f769,f1220,f1369,f1902,f1925])).
% 0.21/10.62 % SZS output end CNFRefutation for theBenchmark.p
% 0.21/10.63 % Elapsed time: 0.159392 seconds
% 0.21/10.63 % CPU time: 1.021188 seconds
% 0.21/10.63 % Total memory used: 123.262 MB
% 0.21/10.63 % Net memory used: 122.741 MB
%------------------------------------------------------------------------------