%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP629+3 : 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 : n001.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 16.35s 4.67s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP629+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n001.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:13 UTC 2026
% 0.17/0.44 % CPUTime :
% 2.56/2.83 % Drodi V4.1.1
% 16.35/4.67 % Refutation found
% 16.35/4.67 % SZS status Theorem for theBenchmark: Theorem is valid
% 16.35/4.67 % SZS output start CNFRefutation for theBenchmark
% 16.35/4.67 fof(f7368,axiom,(
% 16.35/4.67 (! [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_subset_1(C,u1_struct_0(A))=> ( C = k3_group_1(A,B)<=> ( k1_group_1(A,B,C) = k2_group_1(A)& k1_group_1(A,C,B) = k2_group_1(A) ) ) ) )) )) )),
% 16.35/4.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 16.35/4.67 fof(f7377,axiom,(
% 16.35/4.67 (! [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))=> k3_group_1(A,k3_group_1(A,B)) = B ) )) )),
% 16.35/4.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 16.35/4.67 fof(f7471,axiom,(
% 16.35/4.67 (! [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)) ) )),
% 16.35/4.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 16.35/4.67 fof(f12904,axiom,(
% 16.35/4.67 (! [A] :( ( ~ v3_struct_0(A)& v1_group_1(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> (! [C] :( m1_subset_1(C,u1_struct_0(A))=> k6_autgroup(A,k1_group_1(A,B,C)) = k7_funct_2(u1_struct_0(A),u1_struct_0(A),u1_struct_0(A),k6_autgroup(A,B),k6_autgroup(A,C)) ) )) )) )),
% 16.35/4.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 16.35/4.67 fof(f12905,axiom,(
% 16.35/4.67 (! [A] :( ( ~ v3_struct_0(A)& v1_group_1(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> k6_autgroup(A,k2_group_1(A)) = k6_partfun1(u1_struct_0(A)) ) )),
% 16.35/4.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 16.35/4.67 fof(f12907,conjecture,(
% 16.35/4.67 (! [A] :( ( ~ v3_struct_0(A)& v1_group_1(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> k7_funct_2(u1_struct_0(A),u1_struct_0(A),u1_struct_0(A),k6_autgroup(A,k3_group_1(A,B)),k6_autgroup(A,B)) = k6_autgroup(A,k2_group_1(A)) ) )) )),
% 16.35/4.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 16.35/4.67 fof(f12908,negated_conjecture,(
% 16.35/4.67 ~((! [A] :( ( ~ v3_struct_0(A)& v1_group_1(A)& v3_group_1(A)& v4_group_1(A)& l1_group_1(A) )=> (! [B] :( m1_subset_1(B,u1_struct_0(A))=> k7_funct_2(u1_struct_0(A),u1_struct_0(A),u1_struct_0(A),k6_autgroup(A,k3_group_1(A,B)),k6_autgroup(A,B)) = k6_autgroup(A,k2_group_1(A)) ) )) ))),
% 16.35/4.67 inference(negated_conjecture,[status(cth)],[f12907])).
% 16.35/4.67 fof(f35306,plain,(
% 16.35/4.67 ![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_subset_1(C,u1_struct_0(A))|(C=k3_group_1(A,B)<=>(k1_group_1(A,B,C)=k2_group_1(A)&k1_group_1(A,C,B)=k2_group_1(A))))))))),
% 16.35/4.67 inference(pre_NNF_transformation,[status(thm)],[f7368])).
% 16.35/4.67 fof(f35307,plain,(
% 16.35/4.67 ![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_subset_1(C,u1_struct_0(A))|((~C=k3_group_1(A,B)|(k1_group_1(A,B,C)=k2_group_1(A)&k1_group_1(A,C,B)=k2_group_1(A)))&(C=k3_group_1(A,B)|(~k1_group_1(A,B,C)=k2_group_1(A)|~k1_group_1(A,C,B)=k2_group_1(A)))))))))),
% 16.35/4.67 inference(NNF_transformation,[status(thm)],[f35306])).
% 16.35/4.67 fof(f35308,plain,(
% 16.35/4.67 ![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_subset_1(X2,u1_struct_0(X0))|~X2=k3_group_1(X0,X1)|k1_group_1(X0,X1,X2)=k2_group_1(X0))),
% 16.35/4.67 inference(cnf_transformation,[status(thm)],[f35307])).
% 16.35/4.67 fof(f35325,plain,(
% 16.35/4.67 ![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))|k3_group_1(A,k3_group_1(A,B))=B)))),
% 16.35/4.67 inference(pre_NNF_transformation,[status(thm)],[f7377])).
% 16.35/4.67 fof(f35326,plain,(
% 16.35/4.67 ![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))|k3_group_1(X0,k3_group_1(X0,X1))=X1)),
% 16.35/4.67 inference(cnf_transformation,[status(thm)],[f35325])).
% 16.35/4.67 fof(f35542,plain,(
% 16.35/4.67 ![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)))),
% 16.35/4.67 inference(pre_NNF_transformation,[status(thm)],[f7471])).
% 16.35/4.67 fof(f35543,plain,(
% 16.35/4.67 ![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)))),
% 16.35/4.67 inference(cnf_transformation,[status(thm)],[f35542])).
% 16.35/4.67 fof(f54016,plain,(
% 16.35/4.67 ![A]: (((((v3_struct_0(A)|~v1_group_1(A))|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|(![B]: (~m1_subset_1(B,u1_struct_0(A))|(![C]: (~m1_subset_1(C,u1_struct_0(A))|k6_autgroup(A,k1_group_1(A,B,C))=k7_funct_2(u1_struct_0(A),u1_struct_0(A),u1_struct_0(A),k6_autgroup(A,B),k6_autgroup(A,C)))))))),
% 16.35/4.67 inference(pre_NNF_transformation,[status(thm)],[f12904])).
% 16.35/4.67 fof(f54017,plain,(
% 16.35/4.67 ![X0,X1,X2]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|k6_autgroup(X0,k1_group_1(X0,X1,X2))=k7_funct_2(u1_struct_0(X0),u1_struct_0(X0),u1_struct_0(X0),k6_autgroup(X0,X1),k6_autgroup(X0,X2)))),
% 16.35/4.67 inference(cnf_transformation,[status(thm)],[f54016])).
% 16.35/4.67 fof(f54018,plain,(
% 16.35/4.67 ![A]: (((((v3_struct_0(A)|~v1_group_1(A))|~v3_group_1(A))|~v4_group_1(A))|~l1_group_1(A))|k6_autgroup(A,k2_group_1(A))=k6_partfun1(u1_struct_0(A)))),
% 16.35/4.67 inference(pre_NNF_transformation,[status(thm)],[f12905])).
% 16.35/4.67 fof(f54019,plain,(
% 16.35/4.67 ![X0]: (v3_struct_0(X0)|~v1_group_1(X0)|~v3_group_1(X0)|~v4_group_1(X0)|~l1_group_1(X0)|k6_autgroup(X0,k2_group_1(X0))=k6_partfun1(u1_struct_0(X0)))),
% 16.35/4.67 inference(cnf_transformation,[status(thm)],[f54018])).
% 16.35/4.67 fof(f54022,plain,(
% 16.35/4.67 (?[A]: (((((~v3_struct_0(A)&v1_group_1(A))&v3_group_1(A))&v4_group_1(A))&l1_group_1(A))&(?[B]: (m1_subset_1(B,u1_struct_0(A))&~k7_funct_2(u1_struct_0(A),u1_struct_0(A),u1_struct_0(A),k6_autgroup(A,k3_group_1(A,B)),k6_autgroup(A,B))=k6_autgroup(A,k2_group_1(A))))))),
% 16.35/4.67 inference(pre_NNF_transformation,[status(thm)],[f12908])).
% 16.35/4.67 fof(f54023,plain,(
% 16.35/4.67 (((((~v3_struct_0(sK3710_skl)&v1_group_1(sK3710_skl))&v3_group_1(sK3710_skl))&v4_group_1(sK3710_skl))&l1_group_1(sK3710_skl))&(m1_subset_1(sK3711_skl,u1_struct_0(sK3710_skl))&~k7_funct_2(u1_struct_0(sK3710_skl),u1_struct_0(sK3710_skl),u1_struct_0(sK3710_skl),k6_autgroup(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl)),k6_autgroup(sK3710_skl,sK3711_skl))=k6_autgroup(sK3710_skl,k2_group_1(sK3710_skl))))),
% 16.35/4.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK3710_skl,sK3711_skl]),skolemize(A,sK3710_skl),skolemize(B,sK3711_skl)],[f54022])).
% 16.35/4.67 fof(f54024,plain,(
% 16.35/4.67 ~v3_struct_0(sK3710_skl)),
% 16.35/4.67 inference(cnf_transformation,[status(thm)],[f54023])).
% 16.35/4.67 fof(f54025,plain,(
% 16.35/4.67 v1_group_1(sK3710_skl)),
% 16.35/4.67 inference(cnf_transformation,[status(thm)],[f54023])).
% 16.35/4.67 fof(f54026,plain,(
% 16.35/4.67 v3_group_1(sK3710_skl)),
% 16.35/4.67 inference(cnf_transformation,[status(thm)],[f54023])).
% 16.35/4.67 fof(f54027,plain,(
% 16.35/4.67 v4_group_1(sK3710_skl)),
% 16.35/4.67 inference(cnf_transformation,[status(thm)],[f54023])).
% 16.35/4.67 fof(f54028,plain,(
% 16.35/4.67 l1_group_1(sK3710_skl)),
% 16.35/4.67 inference(cnf_transformation,[status(thm)],[f54023])).
% 16.35/4.67 fof(f54029,plain,(
% 16.35/4.67 m1_subset_1(sK3711_skl,u1_struct_0(sK3710_skl))),
% 16.35/4.67 inference(cnf_transformation,[status(thm)],[f54023])).
% 16.35/4.67 fof(f54030,plain,(
% 16.35/4.67 ~k7_funct_2(u1_struct_0(sK3710_skl),u1_struct_0(sK3710_skl),u1_struct_0(sK3710_skl),k6_autgroup(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl)),k6_autgroup(sK3710_skl,sK3711_skl))=k6_autgroup(sK3710_skl,k2_group_1(sK3710_skl))),
% 16.35/4.67 inference(cnf_transformation,[status(thm)],[f54023])).
% 16.35/4.67 fof(f57488,plain,(
% 16.35/4.67 v3_struct_0(sK3710_skl)|~v3_group_1(sK3710_skl)|~v4_group_1(sK3710_skl)|~l1_group_1(sK3710_skl)|k3_group_1(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl))=sK3711_skl),
% 16.35/4.67 inference(resolution,[status(thm)],[f35326,f54029])).
% 16.35/4.67 fof(f57490,plain,(
% 16.35/4.67 ~v3_group_1(sK3710_skl)|~v4_group_1(sK3710_skl)|~l1_group_1(sK3710_skl)|k3_group_1(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl))=sK3711_skl),
% 16.35/4.67 inference(forward_subsumption_resolution,[status(thm)],[f57488,f54024])).
% 16.35/4.67 fof(f57491,plain,(
% 16.35/4.67 ~v4_group_1(sK3710_skl)|~l1_group_1(sK3710_skl)|k3_group_1(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl))=sK3711_skl),
% 16.35/4.67 inference(forward_subsumption_resolution,[status(thm)],[f57490,f54026])).
% 16.35/4.67 fof(f57492,plain,(
% 16.35/4.67 ~l1_group_1(sK3710_skl)|k3_group_1(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl))=sK3711_skl),
% 16.35/4.67 inference(resolution,[status(thm)],[f57491,f54027])).
% 16.35/4.67 fof(f57493,plain,(
% 16.35/4.67 k3_group_1(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl))=sK3711_skl),
% 16.35/4.67 inference(forward_subsumption_resolution,[status(thm)],[f57492,f54028])).
% 16.35/4.67 fof(f57502,plain,(
% 16.35/4.67 v3_struct_0(sK3710_skl)|~v1_group_1(sK3710_skl)|~v3_group_1(sK3710_skl)|~l1_group_1(sK3710_skl)|k6_autgroup(sK3710_skl,k2_group_1(sK3710_skl))=k6_partfun1(u1_struct_0(sK3710_skl))),
% 16.35/4.67 inference(resolution,[status(thm)],[f54019,f54027])).
% 16.35/4.67 fof(f57503,plain,(
% 16.35/4.67 ~v1_group_1(sK3710_skl)|~v3_group_1(sK3710_skl)|~l1_group_1(sK3710_skl)|k6_autgroup(sK3710_skl,k2_group_1(sK3710_skl))=k6_partfun1(u1_struct_0(sK3710_skl))),
% 16.35/4.67 inference(forward_subsumption_resolution,[status(thm)],[f57502,f54024])).
% 16.35/4.67 fof(f57504,plain,(
% 16.35/4.67 ~v3_group_1(sK3710_skl)|~l1_group_1(sK3710_skl)|k6_autgroup(sK3710_skl,k2_group_1(sK3710_skl))=k6_partfun1(u1_struct_0(sK3710_skl))),
% 16.35/4.67 inference(forward_subsumption_resolution,[status(thm)],[f57503,f54025])).
% 16.35/4.67 fof(f57505,plain,(
% 16.35/4.67 ~l1_group_1(sK3710_skl)|k6_autgroup(sK3710_skl,k2_group_1(sK3710_skl))=k6_partfun1(u1_struct_0(sK3710_skl))),
% 16.35/4.67 inference(resolution,[status(thm)],[f57504,f54026])).
% 16.35/4.67 fof(f57506,plain,(
% 16.35/4.67 k6_autgroup(sK3710_skl,k2_group_1(sK3710_skl))=k6_partfun1(u1_struct_0(sK3710_skl))),
% 16.35/4.67 inference(forward_subsumption_resolution,[status(thm)],[f57505,f54028])).
% 16.35/4.67 fof(f57508,plain,(
% 16.35/4.67 ~k7_funct_2(u1_struct_0(sK3710_skl),u1_struct_0(sK3710_skl),u1_struct_0(sK3710_skl),k6_autgroup(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl)),k6_autgroup(sK3710_skl,sK3711_skl))=k6_partfun1(u1_struct_0(sK3710_skl))),
% 16.35/4.67 inference(backward_demodulation,[status(thm)],[f57506,f54030])).
% 16.35/4.67 fof(f57510,plain,(
% 16.35/4.67 v3_struct_0(sK3710_skl)|~v3_group_1(sK3710_skl)|~v4_group_1(sK3710_skl)|~l1_group_1(sK3710_skl)|m1_subset_1(k3_group_1(sK3710_skl,sK3711_skl),u1_struct_0(sK3710_skl))),
% 16.35/4.67 inference(resolution,[status(thm)],[f35543,f54029])).
% 16.35/4.67 fof(f57512,plain,(
% 16.35/4.67 ~v3_group_1(sK3710_skl)|~v4_group_1(sK3710_skl)|~l1_group_1(sK3710_skl)|m1_subset_1(k3_group_1(sK3710_skl,sK3711_skl),u1_struct_0(sK3710_skl))),
% 16.35/4.67 inference(forward_subsumption_resolution,[status(thm)],[f57510,f54024])).
% 16.35/4.67 fof(f57513,plain,(
% 16.35/4.67 ~v4_group_1(sK3710_skl)|~l1_group_1(sK3710_skl)|m1_subset_1(k3_group_1(sK3710_skl,sK3711_skl),u1_struct_0(sK3710_skl))),
% 16.35/4.67 inference(forward_subsumption_resolution,[status(thm)],[f57512,f54026])).
% 16.35/4.67 fof(f57514,plain,(
% 16.35/4.67 ~l1_group_1(sK3710_skl)|m1_subset_1(k3_group_1(sK3710_skl,sK3711_skl),u1_struct_0(sK3710_skl))),
% 16.35/4.67 inference(resolution,[status(thm)],[f57513,f54027])).
% 16.35/4.67 fof(f57515,plain,(
% 16.35/4.67 m1_subset_1(k3_group_1(sK3710_skl,sK3711_skl),u1_struct_0(sK3710_skl))),
% 16.35/4.67 inference(forward_subsumption_resolution,[status(thm)],[f57514,f54028])).
% 16.35/4.67 fof(f57659,plain,(
% 16.35/4.67 ![X0]: (v3_struct_0(sK3710_skl)|~v3_group_1(sK3710_skl)|~v4_group_1(sK3710_skl)|~l1_group_1(sK3710_skl)|~m1_subset_1(X0,u1_struct_0(sK3710_skl))|~X0=k3_group_1(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl))|k1_group_1(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl),X0)=k2_group_1(sK3710_skl))),
% 16.35/4.67 inference(resolution,[status(thm)],[f35308,f57515])).
% 16.35/4.67 fof(f57662,plain,(
% 16.35/4.67 ![X0]: (v3_struct_0(sK3710_skl)|~v3_group_1(sK3710_skl)|~v4_group_1(sK3710_skl)|~l1_group_1(sK3710_skl)|~m1_subset_1(X0,u1_struct_0(sK3710_skl))|~X0=sK3711_skl|k1_group_1(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl),X0)=k2_group_1(sK3710_skl))),
% 16.35/4.67 inference(forward_demodulation,[status(thm)],[f57493,f57659])).
% 16.35/4.67 fof(f57663,plain,(
% 16.35/4.67 ![X0]: (~v3_group_1(sK3710_skl)|~v4_group_1(sK3710_skl)|~l1_group_1(sK3710_skl)|~m1_subset_1(X0,u1_struct_0(sK3710_skl))|~X0=sK3711_skl|k1_group_1(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl),X0)=k2_group_1(sK3710_skl))),
% 16.35/4.67 inference(forward_subsumption_resolution,[status(thm)],[f57662,f54024])).
% 16.35/4.67 fof(f57733,plain,(
% 16.35/4.67 ![X0]: (~v4_group_1(sK3710_skl)|~l1_group_1(sK3710_skl)|~m1_subset_1(X0,u1_struct_0(sK3710_skl))|~X0=sK3711_skl|k1_group_1(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl),X0)=k2_group_1(sK3710_skl))),
% 16.35/4.67 inference(forward_subsumption_resolution,[status(thm)],[f57663,f54026])).
% 16.35/4.67 fof(f57736,plain,(
% 16.35/4.67 ~v4_group_1(sK3710_skl)|~l1_group_1(sK3710_skl)|~sK3711_skl=sK3711_skl|k1_group_1(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl),sK3711_skl)=k2_group_1(sK3710_skl)),
% 16.35/4.67 inference(resolution,[status(thm)],[f57733,f54029])).
% 16.35/4.67 fof(f57739,plain,(
% 16.35/4.67 ~v4_group_1(sK3710_skl)|~l1_group_1(sK3710_skl)|k1_group_1(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl),sK3711_skl)=k2_group_1(sK3710_skl)),
% 16.35/4.67 inference(trivial_equality_resolution,[status(thm)],[f57736])).
% 16.35/4.67 fof(f57740,plain,(
% 16.35/4.67 ~l1_group_1(sK3710_skl)|k1_group_1(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl),sK3711_skl)=k2_group_1(sK3710_skl)),
% 16.35/4.67 inference(forward_subsumption_resolution,[status(thm)],[f57739,f54027])).
% 16.35/4.67 fof(f57743,plain,(
% 16.35/4.67 k1_group_1(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl),sK3711_skl)=k2_group_1(sK3710_skl)),
% 16.35/4.67 inference(forward_subsumption_resolution,[status(thm)],[f57740,f54028])).
% 16.35/4.67 fof(f58413,plain,(
% 16.35/4.67 ![X0]: (v3_struct_0(sK3710_skl)|~v1_group_1(sK3710_skl)|~v3_group_1(sK3710_skl)|~v4_group_1(sK3710_skl)|~l1_group_1(sK3710_skl)|~m1_subset_1(X0,u1_struct_0(sK3710_skl))|k6_autgroup(sK3710_skl,k1_group_1(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl),X0))=k7_funct_2(u1_struct_0(sK3710_skl),u1_struct_0(sK3710_skl),u1_struct_0(sK3710_skl),k6_autgroup(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl)),k6_autgroup(sK3710_skl,X0)))),
% 16.35/4.67 inference(resolution,[status(thm)],[f54017,f57515])).
% 16.35/4.67 fof(f58416,plain,(
% 16.35/4.67 ![X0]: (~v1_group_1(sK3710_skl)|~v3_group_1(sK3710_skl)|~v4_group_1(sK3710_skl)|~l1_group_1(sK3710_skl)|~m1_subset_1(X0,u1_struct_0(sK3710_skl))|k6_autgroup(sK3710_skl,k1_group_1(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl),X0))=k7_funct_2(u1_struct_0(sK3710_skl),u1_struct_0(sK3710_skl),u1_struct_0(sK3710_skl),k6_autgroup(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl)),k6_autgroup(sK3710_skl,X0)))),
% 16.35/4.67 inference(forward_subsumption_resolution,[status(thm)],[f58413,f54024])).
% 16.35/4.67 fof(f58832,plain,(
% 16.35/4.67 ![X0]: (~v3_group_1(sK3710_skl)|~v4_group_1(sK3710_skl)|~l1_group_1(sK3710_skl)|~m1_subset_1(X0,u1_struct_0(sK3710_skl))|k6_autgroup(sK3710_skl,k1_group_1(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl),X0))=k7_funct_2(u1_struct_0(sK3710_skl),u1_struct_0(sK3710_skl),u1_struct_0(sK3710_skl),k6_autgroup(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl)),k6_autgroup(sK3710_skl,X0)))),
% 16.35/4.67 inference(forward_subsumption_resolution,[status(thm)],[f58416,f54025])).
% 16.35/4.67 fof(f58835,plain,(
% 16.35/4.67 ~v3_group_1(sK3710_skl)|~v4_group_1(sK3710_skl)|~l1_group_1(sK3710_skl)|k6_autgroup(sK3710_skl,k1_group_1(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl),sK3711_skl))=k7_funct_2(u1_struct_0(sK3710_skl),u1_struct_0(sK3710_skl),u1_struct_0(sK3710_skl),k6_autgroup(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl)),k6_autgroup(sK3710_skl,sK3711_skl))),
% 16.35/4.67 inference(resolution,[status(thm)],[f58832,f54029])).
% 16.35/4.67 fof(f58841,plain,(
% 16.35/4.67 ~v3_group_1(sK3710_skl)|~v4_group_1(sK3710_skl)|~l1_group_1(sK3710_skl)|k6_autgroup(sK3710_skl,k2_group_1(sK3710_skl))=k7_funct_2(u1_struct_0(sK3710_skl),u1_struct_0(sK3710_skl),u1_struct_0(sK3710_skl),k6_autgroup(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl)),k6_autgroup(sK3710_skl,sK3711_skl))),
% 16.35/4.67 inference(forward_demodulation,[status(thm)],[f57743,f58835])).
% 16.35/4.67 fof(f58842,plain,(
% 16.35/4.67 ~v3_group_1(sK3710_skl)|~v4_group_1(sK3710_skl)|~l1_group_1(sK3710_skl)|k6_partfun1(u1_struct_0(sK3710_skl))=k7_funct_2(u1_struct_0(sK3710_skl),u1_struct_0(sK3710_skl),u1_struct_0(sK3710_skl),k6_autgroup(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl)),k6_autgroup(sK3710_skl,sK3711_skl))),
% 16.35/4.67 inference(forward_demodulation,[status(thm)],[f57506,f58841])).
% 16.35/4.67 fof(f58843,plain,(
% 16.35/4.67 ~v4_group_1(sK3710_skl)|~l1_group_1(sK3710_skl)|k6_partfun1(u1_struct_0(sK3710_skl))=k7_funct_2(u1_struct_0(sK3710_skl),u1_struct_0(sK3710_skl),u1_struct_0(sK3710_skl),k6_autgroup(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl)),k6_autgroup(sK3710_skl,sK3711_skl))),
% 16.35/4.67 inference(forward_subsumption_resolution,[status(thm)],[f58842,f54026])).
% 16.35/4.67 fof(f58844,plain,(
% 16.35/4.67 ~l1_group_1(sK3710_skl)|k6_partfun1(u1_struct_0(sK3710_skl))=k7_funct_2(u1_struct_0(sK3710_skl),u1_struct_0(sK3710_skl),u1_struct_0(sK3710_skl),k6_autgroup(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl)),k6_autgroup(sK3710_skl,sK3711_skl))),
% 16.35/4.67 inference(forward_subsumption_resolution,[status(thm)],[f58843,f54027])).
% 13.47/4.94 fof(f58845,plain,(
% 13.47/4.94 k6_partfun1(u1_struct_0(sK3710_skl))=k7_funct_2(u1_struct_0(sK3710_skl),u1_struct_0(sK3710_skl),u1_struct_0(sK3710_skl),k6_autgroup(sK3710_skl,k3_group_1(sK3710_skl,sK3711_skl)),k6_autgroup(sK3710_skl,sK3711_skl))),
% 13.47/4.94 inference(resolution,[status(thm)],[f58844,f54028])).
% 13.47/4.94 fof(f58846,plain,(
% 13.47/4.94 $false),
% 13.47/4.94 inference(forward_subsumption_resolution,[status(thm)],[f58845,f57508])).
% 13.47/4.94 % SZS output end CNFRefutation for theBenchmark.p
% 3.03/5.05 % Elapsed time: 4.546050 seconds
% 3.03/5.05 % CPU time: 17.089108 seconds
% 3.03/5.05 % Total memory used: 3.683 GB
% 3.03/5.05 % Net memory used: 3.658 GB
%------------------------------------------------------------------------------