%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP629+2 : 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 : n013.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 3.31s 1.21s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP629+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n013.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 20 20:20:51 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.46/0.74 % Drodi V4.1.1
% 3.31/1.21 % Refutation found
% 3.31/1.21 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.31/1.21 % SZS output start CNFRefutation for theBenchmark
% 3.31/1.21 fof(f2668,axiom,(
% 3.31/1.21 (! [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) ) ) ) )) )) )),
% 3.31/1.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.31/1.21 fof(f2677,axiom,(
% 3.31/1.21 (! [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 ) )) )),
% 3.31/1.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.31/1.21 fof(f2771,axiom,(
% 3.31/1.21 (! [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)) ) )),
% 3.31/1.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.31/1.21 fof(f3838,axiom,(
% 3.31/1.21 (! [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)) ) )) )) )),
% 3.31/1.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.31/1.21 fof(f3839,axiom,(
% 3.31/1.21 (! [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)) ) )),
% 3.31/1.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.31/1.21 fof(f3841,conjecture,(
% 3.31/1.21 (! [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)) ) )) )),
% 3.31/1.21 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.31/1.21 fof(f3842,negated_conjecture,(
% 3.31/1.21 ~((! [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)) ) )) ))),
% 3.31/1.22 inference(negated_conjecture,[status(cth)],[f3841])).
% 3.31/1.22 fof(f11823,plain,(
% 3.31/1.22 ![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))))))))),
% 3.31/1.22 inference(pre_NNF_transformation,[status(thm)],[f2668])).
% 3.31/1.22 fof(f11824,plain,(
% 3.31/1.22 ![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)))))))))),
% 3.31/1.22 inference(NNF_transformation,[status(thm)],[f11823])).
% 3.31/1.22 fof(f11825,plain,(
% 3.31/1.22 ![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))),
% 3.31/1.22 inference(cnf_transformation,[status(thm)],[f11824])).
% 3.31/1.22 fof(f11842,plain,(
% 3.31/1.22 ![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)))),
% 3.31/1.22 inference(pre_NNF_transformation,[status(thm)],[f2677])).
% 3.31/1.22 fof(f11843,plain,(
% 3.31/1.22 ![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)),
% 3.31/1.22 inference(cnf_transformation,[status(thm)],[f11842])).
% 3.31/1.22 fof(f12059,plain,(
% 3.31/1.22 ![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)))),
% 3.31/1.22 inference(pre_NNF_transformation,[status(thm)],[f2771])).
% 3.31/1.22 fof(f12060,plain,(
% 3.31/1.22 ![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)))),
% 3.31/1.22 inference(cnf_transformation,[status(thm)],[f12059])).
% 3.31/1.22 fof(f15315,plain,(
% 3.31/1.22 ![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)))))))),
% 3.31/1.22 inference(pre_NNF_transformation,[status(thm)],[f3838])).
% 3.31/1.22 fof(f15316,plain,(
% 3.31/1.22 ![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)))),
% 3.31/1.22 inference(cnf_transformation,[status(thm)],[f15315])).
% 3.31/1.22 fof(f15317,plain,(
% 3.31/1.22 ![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)))),
% 3.31/1.22 inference(pre_NNF_transformation,[status(thm)],[f3839])).
% 3.31/1.22 fof(f15318,plain,(
% 3.31/1.22 ![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)))),
% 3.31/1.22 inference(cnf_transformation,[status(thm)],[f15317])).
% 3.31/1.22 fof(f15321,plain,(
% 3.31/1.22 (?[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))))))),
% 3.31/1.22 inference(pre_NNF_transformation,[status(thm)],[f3842])).
% 3.31/1.22 fof(f15322,plain,(
% 3.31/1.22 (((((~v3_struct_0(sK1057_skl)&v1_group_1(sK1057_skl))&v3_group_1(sK1057_skl))&v4_group_1(sK1057_skl))&l1_group_1(sK1057_skl))&(m1_subset_1(sK1058_skl,u1_struct_0(sK1057_skl))&~k7_funct_2(u1_struct_0(sK1057_skl),u1_struct_0(sK1057_skl),u1_struct_0(sK1057_skl),k6_autgroup(sK1057_skl,k3_group_1(sK1057_skl,sK1058_skl)),k6_autgroup(sK1057_skl,sK1058_skl))=k6_autgroup(sK1057_skl,k2_group_1(sK1057_skl))))),
% 3.31/1.22 inference(skolemize,[status(esa),new_symbols(skolem,[sK1057_skl,sK1058_skl]),skolemize(A,sK1057_skl),skolemize(B,sK1058_skl)],[f15321])).
% 3.31/1.22 fof(f15323,plain,(
% 3.31/1.22 ~v3_struct_0(sK1057_skl)),
% 3.31/1.22 inference(cnf_transformation,[status(thm)],[f15322])).
% 3.31/1.22 fof(f15324,plain,(
% 3.31/1.22 v1_group_1(sK1057_skl)),
% 3.31/1.22 inference(cnf_transformation,[status(thm)],[f15322])).
% 3.31/1.22 fof(f15325,plain,(
% 3.31/1.22 v3_group_1(sK1057_skl)),
% 3.31/1.22 inference(cnf_transformation,[status(thm)],[f15322])).
% 3.31/1.22 fof(f15326,plain,(
% 3.31/1.22 v4_group_1(sK1057_skl)),
% 3.31/1.22 inference(cnf_transformation,[status(thm)],[f15322])).
% 3.31/1.22 fof(f15327,plain,(
% 3.31/1.22 l1_group_1(sK1057_skl)),
% 3.31/1.22 inference(cnf_transformation,[status(thm)],[f15322])).
% 3.31/1.22 fof(f15328,plain,(
% 3.31/1.22 m1_subset_1(sK1058_skl,u1_struct_0(sK1057_skl))),
% 3.31/1.22 inference(cnf_transformation,[status(thm)],[f15322])).
% 3.31/1.22 fof(f15329,plain,(
% 3.31/1.22 ~k7_funct_2(u1_struct_0(sK1057_skl),u1_struct_0(sK1057_skl),u1_struct_0(sK1057_skl),k6_autgroup(sK1057_skl,k3_group_1(sK1057_skl,sK1058_skl)),k6_autgroup(sK1057_skl,sK1058_skl))=k6_autgroup(sK1057_skl,k2_group_1(sK1057_skl))),
% 3.31/1.22 inference(cnf_transformation,[status(thm)],[f15322])).
% 3.31/1.22 fof(f17007,plain,(
% 3.31/1.22 ![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))|k1_group_1(X0,X1,k3_group_1(X0,X1))=k2_group_1(X0))),
% 3.31/1.22 inference(destructive_equality_resolution,[status(thm)],[f11825])).
% 3.31/1.22 fof(f17385,plain,(
% 3.31/1.22 v3_struct_0(sK1057_skl)|~v3_group_1(sK1057_skl)|~v4_group_1(sK1057_skl)|~l1_group_1(sK1057_skl)|k3_group_1(sK1057_skl,k3_group_1(sK1057_skl,sK1058_skl))=sK1058_skl),
% 3.31/1.22 inference(resolution,[status(thm)],[f11843,f15328])).
% 3.31/1.22 fof(f17387,plain,(
% 3.31/1.22 ~v3_group_1(sK1057_skl)|~v4_group_1(sK1057_skl)|~l1_group_1(sK1057_skl)|k3_group_1(sK1057_skl,k3_group_1(sK1057_skl,sK1058_skl))=sK1058_skl),
% 3.31/1.22 inference(forward_subsumption_resolution,[status(thm)],[f17385,f15323])).
% 3.31/1.22 fof(f17388,plain,(
% 3.31/1.22 ~v4_group_1(sK1057_skl)|~l1_group_1(sK1057_skl)|k3_group_1(sK1057_skl,k3_group_1(sK1057_skl,sK1058_skl))=sK1058_skl),
% 3.31/1.22 inference(forward_subsumption_resolution,[status(thm)],[f17387,f15325])).
% 3.31/1.22 fof(f17389,plain,(
% 3.31/1.22 ~v4_group_1(sK1057_skl)|k3_group_1(sK1057_skl,k3_group_1(sK1057_skl,sK1058_skl))=sK1058_skl),
% 3.31/1.22 inference(resolution,[status(thm)],[f17388,f15327])).
% 3.31/1.22 fof(f17390,plain,(
% 3.31/1.22 k3_group_1(sK1057_skl,k3_group_1(sK1057_skl,sK1058_skl))=sK1058_skl),
% 3.31/1.22 inference(forward_subsumption_resolution,[status(thm)],[f17389,f15326])).
% 3.31/1.22 fof(f17392,plain,(
% 3.31/1.22 v3_struct_0(sK1057_skl)|~v1_group_1(sK1057_skl)|~v3_group_1(sK1057_skl)|~v4_group_1(sK1057_skl)|k6_autgroup(sK1057_skl,k2_group_1(sK1057_skl))=k6_partfun1(u1_struct_0(sK1057_skl))),
% 3.31/1.22 inference(resolution,[status(thm)],[f15318,f15327])).
% 3.31/1.22 fof(f17393,plain,(
% 3.31/1.22 ~v1_group_1(sK1057_skl)|~v3_group_1(sK1057_skl)|~v4_group_1(sK1057_skl)|k6_autgroup(sK1057_skl,k2_group_1(sK1057_skl))=k6_partfun1(u1_struct_0(sK1057_skl))),
% 3.31/1.22 inference(forward_subsumption_resolution,[status(thm)],[f17392,f15323])).
% 3.31/1.22 fof(f17394,plain,(
% 3.31/1.22 ~v3_group_1(sK1057_skl)|~v4_group_1(sK1057_skl)|k6_autgroup(sK1057_skl,k2_group_1(sK1057_skl))=k6_partfun1(u1_struct_0(sK1057_skl))),
% 3.31/1.22 inference(forward_subsumption_resolution,[status(thm)],[f17393,f15324])).
% 3.31/1.22 fof(f17395,plain,(
% 3.31/1.22 ~v4_group_1(sK1057_skl)|k6_autgroup(sK1057_skl,k2_group_1(sK1057_skl))=k6_partfun1(u1_struct_0(sK1057_skl))),
% 3.31/1.22 inference(resolution,[status(thm)],[f17394,f15325])).
% 3.31/1.22 fof(f17396,plain,(
% 3.31/1.22 k6_autgroup(sK1057_skl,k2_group_1(sK1057_skl))=k6_partfun1(u1_struct_0(sK1057_skl))),
% 3.31/1.22 inference(forward_subsumption_resolution,[status(thm)],[f17395,f15326])).
% 3.31/1.22 fof(f17398,plain,(
% 3.31/1.22 ~k7_funct_2(u1_struct_0(sK1057_skl),u1_struct_0(sK1057_skl),u1_struct_0(sK1057_skl),k6_autgroup(sK1057_skl,k3_group_1(sK1057_skl,sK1058_skl)),k6_autgroup(sK1057_skl,sK1058_skl))=k6_partfun1(u1_struct_0(sK1057_skl))),
% 3.31/1.22 inference(backward_demodulation,[status(thm)],[f17396,f15329])).
% 3.31/1.22 fof(f17400,plain,(
% 3.31/1.22 v3_struct_0(sK1057_skl)|~v3_group_1(sK1057_skl)|~v4_group_1(sK1057_skl)|~l1_group_1(sK1057_skl)|m1_subset_1(k3_group_1(sK1057_skl,sK1058_skl),u1_struct_0(sK1057_skl))),
% 3.31/1.22 inference(resolution,[status(thm)],[f12060,f15328])).
% 3.31/1.22 fof(f17402,plain,(
% 3.31/1.22 ~v3_group_1(sK1057_skl)|~v4_group_1(sK1057_skl)|~l1_group_1(sK1057_skl)|m1_subset_1(k3_group_1(sK1057_skl,sK1058_skl),u1_struct_0(sK1057_skl))),
% 3.31/1.22 inference(forward_subsumption_resolution,[status(thm)],[f17400,f15323])).
% 3.31/1.22 fof(f17403,plain,(
% 3.31/1.22 ~v4_group_1(sK1057_skl)|~l1_group_1(sK1057_skl)|m1_subset_1(k3_group_1(sK1057_skl,sK1058_skl),u1_struct_0(sK1057_skl))),
% 3.31/1.22 inference(forward_subsumption_resolution,[status(thm)],[f17402,f15325])).
% 3.31/1.22 fof(f17404,plain,(
% 3.31/1.22 ~v4_group_1(sK1057_skl)|m1_subset_1(k3_group_1(sK1057_skl,sK1058_skl),u1_struct_0(sK1057_skl))),
% 3.31/1.22 inference(resolution,[status(thm)],[f17403,f15327])).
% 3.31/1.22 fof(f17405,plain,(
% 3.31/1.22 m1_subset_1(k3_group_1(sK1057_skl,sK1058_skl),u1_struct_0(sK1057_skl))),
% 3.31/1.22 inference(forward_subsumption_resolution,[status(thm)],[f17404,f15326])).
% 3.31/1.22 fof(f17444,plain,(
% 3.31/1.22 ![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))|k1_group_1(X0,X1,k3_group_1(X0,X1))=k2_group_1(X0))),
% 3.31/1.22 inference(forward_subsumption_resolution,[status(thm)],[f17007,f12060])).
% 3.31/1.22 fof(f17445,plain,(
% 3.31/1.22 v3_struct_0(sK1057_skl)|~v3_group_1(sK1057_skl)|~v4_group_1(sK1057_skl)|~l1_group_1(sK1057_skl)|k1_group_1(sK1057_skl,k3_group_1(sK1057_skl,sK1058_skl),k3_group_1(sK1057_skl,k3_group_1(sK1057_skl,sK1058_skl)))=k2_group_1(sK1057_skl)),
% 3.31/1.22 inference(resolution,[status(thm)],[f17444,f17405])).
% 3.31/1.22 fof(f17448,plain,(
% 3.31/1.22 v3_struct_0(sK1057_skl)|~v3_group_1(sK1057_skl)|~v4_group_1(sK1057_skl)|~l1_group_1(sK1057_skl)|k1_group_1(sK1057_skl,k3_group_1(sK1057_skl,sK1058_skl),sK1058_skl)=k2_group_1(sK1057_skl)),
% 3.31/1.22 inference(forward_demodulation,[status(thm)],[f17390,f17445])).
% 3.31/1.22 fof(f17449,plain,(
% 3.31/1.22 ~v3_group_1(sK1057_skl)|~v4_group_1(sK1057_skl)|~l1_group_1(sK1057_skl)|k1_group_1(sK1057_skl,k3_group_1(sK1057_skl,sK1058_skl),sK1058_skl)=k2_group_1(sK1057_skl)),
% 3.31/1.22 inference(forward_subsumption_resolution,[status(thm)],[f17448,f15323])).
% 3.31/1.22 fof(f17463,plain,(
% 3.31/1.22 ~v4_group_1(sK1057_skl)|~l1_group_1(sK1057_skl)|k1_group_1(sK1057_skl,k3_group_1(sK1057_skl,sK1058_skl),sK1058_skl)=k2_group_1(sK1057_skl)),
% 3.31/1.22 inference(forward_subsumption_resolution,[status(thm)],[f17449,f15325])).
% 3.31/1.22 fof(f17464,plain,(
% 3.31/1.22 ~v4_group_1(sK1057_skl)|k1_group_1(sK1057_skl,k3_group_1(sK1057_skl,sK1058_skl),sK1058_skl)=k2_group_1(sK1057_skl)),
% 3.31/1.22 inference(resolution,[status(thm)],[f17463,f15327])).
% 3.31/1.22 fof(f17465,plain,(
% 3.31/1.22 k1_group_1(sK1057_skl,k3_group_1(sK1057_skl,sK1058_skl),sK1058_skl)=k2_group_1(sK1057_skl)),
% 3.31/1.22 inference(forward_subsumption_resolution,[status(thm)],[f17464,f15326])).
% 3.31/1.22 fof(f18160,plain,(
% 3.31/1.22 ![X0]: (v3_struct_0(sK1057_skl)|~v1_group_1(sK1057_skl)|~v3_group_1(sK1057_skl)|~v4_group_1(sK1057_skl)|~l1_group_1(sK1057_skl)|~m1_subset_1(X0,u1_struct_0(sK1057_skl))|k6_autgroup(sK1057_skl,k1_group_1(sK1057_skl,X0,sK1058_skl))=k7_funct_2(u1_struct_0(sK1057_skl),u1_struct_0(sK1057_skl),u1_struct_0(sK1057_skl),k6_autgroup(sK1057_skl,X0),k6_autgroup(sK1057_skl,sK1058_skl)))),
% 3.31/1.22 inference(resolution,[status(thm)],[f15316,f15328])).
% 3.31/1.22 fof(f18164,plain,(
% 3.31/1.22 ![X0]: (~v1_group_1(sK1057_skl)|~v3_group_1(sK1057_skl)|~v4_group_1(sK1057_skl)|~l1_group_1(sK1057_skl)|~m1_subset_1(X0,u1_struct_0(sK1057_skl))|k6_autgroup(sK1057_skl,k1_group_1(sK1057_skl,X0,sK1058_skl))=k7_funct_2(u1_struct_0(sK1057_skl),u1_struct_0(sK1057_skl),u1_struct_0(sK1057_skl),k6_autgroup(sK1057_skl,X0),k6_autgroup(sK1057_skl,sK1058_skl)))),
% 3.31/1.22 inference(forward_subsumption_resolution,[status(thm)],[f18160,f15323])).
% 3.31/1.22 fof(f18169,plain,(
% 3.31/1.22 ![X0]: (~v3_group_1(sK1057_skl)|~v4_group_1(sK1057_skl)|~l1_group_1(sK1057_skl)|~m1_subset_1(X0,u1_struct_0(sK1057_skl))|k6_autgroup(sK1057_skl,k1_group_1(sK1057_skl,X0,sK1058_skl))=k7_funct_2(u1_struct_0(sK1057_skl),u1_struct_0(sK1057_skl),u1_struct_0(sK1057_skl),k6_autgroup(sK1057_skl,X0),k6_autgroup(sK1057_skl,sK1058_skl)))),
% 3.31/1.22 inference(forward_subsumption_resolution,[status(thm)],[f18164,f15324])).
% 3.31/1.22 fof(f18170,plain,(
% 3.31/1.22 ~v3_group_1(sK1057_skl)|~v4_group_1(sK1057_skl)|~l1_group_1(sK1057_skl)|k6_autgroup(sK1057_skl,k1_group_1(sK1057_skl,k3_group_1(sK1057_skl,sK1058_skl),sK1058_skl))=k7_funct_2(u1_struct_0(sK1057_skl),u1_struct_0(sK1057_skl),u1_struct_0(sK1057_skl),k6_autgroup(sK1057_skl,k3_group_1(sK1057_skl,sK1058_skl)),k6_autgroup(sK1057_skl,sK1058_skl))),
% 3.31/1.22 inference(resolution,[status(thm)],[f18169,f17405])).
% 3.31/1.22 fof(f18173,plain,(
% 3.31/1.22 ~v3_group_1(sK1057_skl)|~v4_group_1(sK1057_skl)|~l1_group_1(sK1057_skl)|k6_autgroup(sK1057_skl,k2_group_1(sK1057_skl))=k7_funct_2(u1_struct_0(sK1057_skl),u1_struct_0(sK1057_skl),u1_struct_0(sK1057_skl),k6_autgroup(sK1057_skl,k3_group_1(sK1057_skl,sK1058_skl)),k6_autgroup(sK1057_skl,sK1058_skl))),
% 3.31/1.22 inference(forward_demodulation,[status(thm)],[f17465,f18170])).
% 3.31/1.22 fof(f18174,plain,(
% 3.31/1.22 ~v3_group_1(sK1057_skl)|~v4_group_1(sK1057_skl)|~l1_group_1(sK1057_skl)|k6_partfun1(u1_struct_0(sK1057_skl))=k7_funct_2(u1_struct_0(sK1057_skl),u1_struct_0(sK1057_skl),u1_struct_0(sK1057_skl),k6_autgroup(sK1057_skl,k3_group_1(sK1057_skl,sK1058_skl)),k6_autgroup(sK1057_skl,sK1058_skl))),
% 3.31/1.22 inference(forward_demodulation,[status(thm)],[f17396,f18173])).
% 3.31/1.22 fof(f18175,plain,(
% 3.31/1.22 ~v4_group_1(sK1057_skl)|~l1_group_1(sK1057_skl)|k6_partfun1(u1_struct_0(sK1057_skl))=k7_funct_2(u1_struct_0(sK1057_skl),u1_struct_0(sK1057_skl),u1_struct_0(sK1057_skl),k6_autgroup(sK1057_skl,k3_group_1(sK1057_skl,sK1058_skl)),k6_autgroup(sK1057_skl,sK1058_skl))),
% 3.31/1.22 inference(forward_subsumption_resolution,[status(thm)],[f18174,f15325])).
% 3.31/1.22 fof(f18184,plain,(
% 3.31/1.22 ~l1_group_1(sK1057_skl)|k6_partfun1(u1_struct_0(sK1057_skl))=k7_funct_2(u1_struct_0(sK1057_skl),u1_struct_0(sK1057_skl),u1_struct_0(sK1057_skl),k6_autgroup(sK1057_skl,k3_group_1(sK1057_skl,sK1058_skl)),k6_autgroup(sK1057_skl,sK1058_skl))),
% 3.31/1.22 inference(forward_subsumption_resolution,[status(thm)],[f18175,f15326])).
% 3.31/1.22 fof(f18185,plain,(
% 3.31/1.22 k6_partfun1(u1_struct_0(sK1057_skl))=k7_funct_2(u1_struct_0(sK1057_skl),u1_struct_0(sK1057_skl),u1_struct_0(sK1057_skl),k6_autgroup(sK1057_skl,k3_group_1(sK1057_skl,sK1058_skl)),k6_autgroup(sK1057_skl,sK1058_skl))),
% 3.31/1.22 inference(resolution,[status(thm)],[f18184,f15327])).
% 3.94/1.26 fof(f18186,plain,(
% 3.94/1.26 $false),
% 3.94/1.26 inference(forward_subsumption_resolution,[status(thm)],[f18185,f17398])).
% 3.94/1.26 % SZS output end CNFRefutation for theBenchmark.p
% 3.94/1.30 % Elapsed time: 0.934503 seconds
% 3.94/1.30 % CPU time: 4.177052 seconds
% 3.94/1.30 % Total memory used: 691.950 MB
% 3.94/1.30 % Net memory used: 685.203 MB
%------------------------------------------------------------------------------