%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP629+4 : 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 : n006.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 21.14s 12.11s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP629+4 : 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.18/0.45 % Computer : n006.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Sun Sep 20 20:21:16 UTC 2026
% 0.18/0.45 % CPUTime :
% 10.11/10.48 % Drodi V4.1.1
% 21.14/12.11 % Refutation found
% 21.14/12.11 % SZS status Theorem for theBenchmark: Theorem is valid
% 21.14/12.11 % SZS output start CNFRefutation for theBenchmark
% 21.14/12.11 fof(f18891,axiom,(
% 21.14/12.11 (! [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) ) ) ) )) )) )),
% 21.14/12.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.14/12.11 fof(f18994,axiom,(
% 21.14/12.11 (! [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)) ) )),
% 21.14/12.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.14/12.11 fof(f33422,axiom,(
% 21.14/12.11 (! [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)) ) )) )) )),
% 21.14/12.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.14/12.11 fof(f33423,axiom,(
% 21.14/12.11 (! [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)) ) )),
% 21.14/12.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.14/12.11 fof(f33425,conjecture,(
% 21.14/12.11 (! [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)) ) )) )),
% 21.14/12.11 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 21.14/12.11 fof(f33426,negated_conjecture,(
% 21.14/12.11 ~((! [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)) ) )) ))),
% 21.14/12.11 inference(negated_conjecture,[status(cth)],[f33425])).
% 21.14/12.11 fof(f94559,plain,(
% 21.14/12.11 ![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))))))))),
% 21.14/12.11 inference(pre_NNF_transformation,[status(thm)],[f18891])).
% 21.14/12.11 fof(f94560,plain,(
% 21.14/12.11 ![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)))))))))),
% 21.14/12.11 inference(NNF_transformation,[status(thm)],[f94559])).
% 21.14/12.11 fof(f94562,plain,(
% 21.14/12.11 ![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,X2,X1)=k2_group_1(X0))),
% 21.14/12.11 inference(cnf_transformation,[status(thm)],[f94560])).
% 21.14/12.11 fof(f94795,plain,(
% 21.14/12.11 ![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)))),
% 21.14/12.11 inference(pre_NNF_transformation,[status(thm)],[f18994])).
% 21.14/12.11 fof(f94796,plain,(
% 21.14/12.11 ![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)))),
% 21.14/12.11 inference(cnf_transformation,[status(thm)],[f94795])).
% 21.14/12.11 fof(f147699,plain,(
% 21.14/12.11 ![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)))))))),
% 21.14/12.11 inference(pre_NNF_transformation,[status(thm)],[f33422])).
% 21.14/12.11 fof(f147700,plain,(
% 21.14/12.11 ![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)))),
% 21.14/12.12 inference(cnf_transformation,[status(thm)],[f147699])).
% 21.14/12.12 fof(f147701,plain,(
% 21.14/12.12 ![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)))),
% 21.14/12.12 inference(pre_NNF_transformation,[status(thm)],[f33423])).
% 21.14/12.12 fof(f147702,plain,(
% 21.14/12.12 ![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)))),
% 21.14/12.12 inference(cnf_transformation,[status(thm)],[f147701])).
% 21.14/12.12 fof(f147705,plain,(
% 21.14/12.12 (?[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))))))),
% 21.14/12.12 inference(pre_NNF_transformation,[status(thm)],[f33426])).
% 21.14/12.12 fof(f147706,plain,(
% 21.14/12.12 (((((~v3_struct_0(sK11609_skl)&v1_group_1(sK11609_skl))&v3_group_1(sK11609_skl))&v4_group_1(sK11609_skl))&l1_group_1(sK11609_skl))&(m1_subset_1(sK11610_skl,u1_struct_0(sK11609_skl))&~k7_funct_2(u1_struct_0(sK11609_skl),u1_struct_0(sK11609_skl),u1_struct_0(sK11609_skl),k6_autgroup(sK11609_skl,k3_group_1(sK11609_skl,sK11610_skl)),k6_autgroup(sK11609_skl,sK11610_skl))=k6_autgroup(sK11609_skl,k2_group_1(sK11609_skl))))),
% 21.14/12.12 inference(skolemize,[status(esa),new_symbols(skolem,[sK11609_skl,sK11610_skl]),skolemize(A,sK11609_skl),skolemize(B,sK11610_skl)],[f147705])).
% 21.14/12.12 fof(f147707,plain,(
% 21.14/12.12 ~v3_struct_0(sK11609_skl)),
% 21.14/12.12 inference(cnf_transformation,[status(thm)],[f147706])).
% 21.14/12.12 fof(f147708,plain,(
% 21.14/12.12 v1_group_1(sK11609_skl)),
% 21.14/12.12 inference(cnf_transformation,[status(thm)],[f147706])).
% 21.14/12.12 fof(f147709,plain,(
% 21.14/12.12 v3_group_1(sK11609_skl)),
% 21.14/12.12 inference(cnf_transformation,[status(thm)],[f147706])).
% 21.14/12.12 fof(f147710,plain,(
% 21.14/12.12 v4_group_1(sK11609_skl)),
% 21.14/12.12 inference(cnf_transformation,[status(thm)],[f147706])).
% 21.14/12.12 fof(f147711,plain,(
% 21.14/12.12 l1_group_1(sK11609_skl)),
% 21.14/12.12 inference(cnf_transformation,[status(thm)],[f147706])).
% 21.14/12.12 fof(f147712,plain,(
% 21.14/12.12 m1_subset_1(sK11610_skl,u1_struct_0(sK11609_skl))),
% 21.14/12.12 inference(cnf_transformation,[status(thm)],[f147706])).
% 21.14/12.12 fof(f147713,plain,(
% 21.14/12.12 ~k7_funct_2(u1_struct_0(sK11609_skl),u1_struct_0(sK11609_skl),u1_struct_0(sK11609_skl),k6_autgroup(sK11609_skl,k3_group_1(sK11609_skl,sK11610_skl)),k6_autgroup(sK11609_skl,sK11610_skl))=k6_autgroup(sK11609_skl,k2_group_1(sK11609_skl))),
% 21.14/12.12 inference(cnf_transformation,[status(thm)],[f147706])).
% 21.14/12.12 fof(f169281,plain,(
% 21.14/12.12 ![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,k3_group_1(X0,X1),X1)=k2_group_1(X0))),
% 21.14/12.12 inference(destructive_equality_resolution,[status(thm)],[f94562])).
% 21.14/12.12 fof(f174147,plain,(
% 21.14/12.12 v3_struct_0(sK11609_skl)|~v1_group_1(sK11609_skl)|~v4_group_1(sK11609_skl)|~l1_group_1(sK11609_skl)|k6_autgroup(sK11609_skl,k2_group_1(sK11609_skl))=k6_partfun1(u1_struct_0(sK11609_skl))),
% 21.14/12.12 inference(resolution,[status(thm)],[f147702,f147709])).
% 21.14/12.12 fof(f174149,plain,(
% 21.14/12.12 ~v1_group_1(sK11609_skl)|~v4_group_1(sK11609_skl)|~l1_group_1(sK11609_skl)|k6_autgroup(sK11609_skl,k2_group_1(sK11609_skl))=k6_partfun1(u1_struct_0(sK11609_skl))),
% 21.14/12.12 inference(forward_subsumption_resolution,[status(thm)],[f174147,f147707])).
% 21.14/12.12 fof(f174151,plain,(
% 21.14/12.12 ![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,k3_group_1(X0,X1),X1)=k2_group_1(X0))),
% 21.14/12.12 inference(backward_subsumption_resolution,[status(thm)],[f169281,f94796])).
% 21.14/12.12 fof(f174153,plain,(
% 21.14/12.12 ![X0]: (v3_struct_0(sK11609_skl)|~v3_group_1(sK11609_skl)|~l1_group_1(sK11609_skl)|~m1_subset_1(X0,u1_struct_0(sK11609_skl))|m1_subset_1(k3_group_1(sK11609_skl,X0),u1_struct_0(sK11609_skl)))),
% 21.14/12.12 inference(resolution,[status(thm)],[f94796,f147710])).
% 21.14/12.12 fof(f174154,plain,(
% 21.14/12.12 ![X0]: (~v3_group_1(sK11609_skl)|~l1_group_1(sK11609_skl)|~m1_subset_1(X0,u1_struct_0(sK11609_skl))|m1_subset_1(k3_group_1(sK11609_skl,X0),u1_struct_0(sK11609_skl)))),
% 21.14/12.12 inference(forward_subsumption_resolution,[status(thm)],[f174153,f147707])).
% 21.14/12.12 fof(f174493,plain,(
% 21.14/12.12 ~v4_group_1(sK11609_skl)|~l1_group_1(sK11609_skl)|k6_autgroup(sK11609_skl,k2_group_1(sK11609_skl))=k6_partfun1(u1_struct_0(sK11609_skl))),
% 21.14/12.12 inference(forward_subsumption_resolution,[status(thm)],[f174149,f147708])).
% 21.14/12.12 fof(f174494,plain,(
% 21.14/12.12 ~l1_group_1(sK11609_skl)|k6_autgroup(sK11609_skl,k2_group_1(sK11609_skl))=k6_partfun1(u1_struct_0(sK11609_skl))),
% 21.14/12.12 inference(resolution,[status(thm)],[f174493,f147710])).
% 21.14/12.12 fof(f174495,plain,(
% 21.14/12.12 k6_autgroup(sK11609_skl,k2_group_1(sK11609_skl))=k6_partfun1(u1_struct_0(sK11609_skl))),
% 21.14/12.12 inference(forward_subsumption_resolution,[status(thm)],[f174494,f147711])).
% 21.14/12.12 fof(f174501,plain,(
% 21.14/12.12 ~k7_funct_2(u1_struct_0(sK11609_skl),u1_struct_0(sK11609_skl),u1_struct_0(sK11609_skl),k6_autgroup(sK11609_skl,k3_group_1(sK11609_skl,sK11610_skl)),k6_autgroup(sK11609_skl,sK11610_skl))=k6_partfun1(u1_struct_0(sK11609_skl))),
% 21.14/12.12 inference(backward_demodulation,[status(thm)],[f174495,f147713])).
% 21.14/12.12 fof(f174582,plain,(
% 21.14/12.12 ![X0]: (~l1_group_1(sK11609_skl)|~m1_subset_1(X0,u1_struct_0(sK11609_skl))|m1_subset_1(k3_group_1(sK11609_skl,X0),u1_struct_0(sK11609_skl)))),
% 21.14/12.12 inference(forward_subsumption_resolution,[status(thm)],[f174154,f147709])).
% 21.14/12.12 fof(f174583,plain,(
% 21.14/12.12 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK11609_skl))|m1_subset_1(k3_group_1(sK11609_skl,X0),u1_struct_0(sK11609_skl)))),
% 21.14/12.12 inference(resolution,[status(thm)],[f174582,f147711])).
% 21.14/12.12 fof(f174586,plain,(
% 21.14/12.12 m1_subset_1(k3_group_1(sK11609_skl,sK11610_skl),u1_struct_0(sK11609_skl))),
% 21.14/12.12 inference(resolution,[status(thm)],[f174583,f147712])).
% 21.14/12.12 fof(f174736,plain,(
% 21.14/12.12 ![X0,X1]: (v3_struct_0(sK11609_skl)|~v1_group_1(sK11609_skl)|~v4_group_1(sK11609_skl)|~l1_group_1(sK11609_skl)|~m1_subset_1(X0,u1_struct_0(sK11609_skl))|~m1_subset_1(X1,u1_struct_0(sK11609_skl))|k6_autgroup(sK11609_skl,k1_group_1(sK11609_skl,X0,X1))=k7_funct_2(u1_struct_0(sK11609_skl),u1_struct_0(sK11609_skl),u1_struct_0(sK11609_skl),k6_autgroup(sK11609_skl,X0),k6_autgroup(sK11609_skl,X1)))),
% 21.14/12.12 inference(resolution,[status(thm)],[f147700,f147709])).
% 21.14/12.12 fof(f174738,plain,(
% 21.14/12.12 ![X0,X1]: (~v1_group_1(sK11609_skl)|~v4_group_1(sK11609_skl)|~l1_group_1(sK11609_skl)|~m1_subset_1(X0,u1_struct_0(sK11609_skl))|~m1_subset_1(X1,u1_struct_0(sK11609_skl))|k6_autgroup(sK11609_skl,k1_group_1(sK11609_skl,X0,X1))=k7_funct_2(u1_struct_0(sK11609_skl),u1_struct_0(sK11609_skl),u1_struct_0(sK11609_skl),k6_autgroup(sK11609_skl,X0),k6_autgroup(sK11609_skl,X1)))),
% 21.14/12.12 inference(forward_subsumption_resolution,[status(thm)],[f174736,f147707])).
% 21.14/12.12 fof(f174873,plain,(
% 21.14/12.12 ![X0]: (v3_struct_0(sK11609_skl)|~v3_group_1(sK11609_skl)|~l1_group_1(sK11609_skl)|~m1_subset_1(X0,u1_struct_0(sK11609_skl))|k1_group_1(sK11609_skl,k3_group_1(sK11609_skl,X0),X0)=k2_group_1(sK11609_skl))),
% 21.14/12.12 inference(resolution,[status(thm)],[f174151,f147710])).
% 21.14/12.12 fof(f174874,plain,(
% 21.14/12.12 ![X0]: (~v3_group_1(sK11609_skl)|~l1_group_1(sK11609_skl)|~m1_subset_1(X0,u1_struct_0(sK11609_skl))|k1_group_1(sK11609_skl,k3_group_1(sK11609_skl,X0),X0)=k2_group_1(sK11609_skl))),
% 21.14/12.12 inference(forward_subsumption_resolution,[status(thm)],[f174873,f147707])).
% 21.14/12.12 fof(f174983,plain,(
% 21.14/12.12 ![X0,X1]: (~v4_group_1(sK11609_skl)|~l1_group_1(sK11609_skl)|~m1_subset_1(X0,u1_struct_0(sK11609_skl))|~m1_subset_1(X1,u1_struct_0(sK11609_skl))|k6_autgroup(sK11609_skl,k1_group_1(sK11609_skl,X0,X1))=k7_funct_2(u1_struct_0(sK11609_skl),u1_struct_0(sK11609_skl),u1_struct_0(sK11609_skl),k6_autgroup(sK11609_skl,X0),k6_autgroup(sK11609_skl,X1)))),
% 21.14/12.12 inference(forward_subsumption_resolution,[status(thm)],[f174738,f147708])).
% 21.14/12.12 fof(f174984,plain,(
% 21.14/12.12 ![X0,X1]: (~l1_group_1(sK11609_skl)|~m1_subset_1(X0,u1_struct_0(sK11609_skl))|~m1_subset_1(X1,u1_struct_0(sK11609_skl))|k6_autgroup(sK11609_skl,k1_group_1(sK11609_skl,X0,X1))=k7_funct_2(u1_struct_0(sK11609_skl),u1_struct_0(sK11609_skl),u1_struct_0(sK11609_skl),k6_autgroup(sK11609_skl,X0),k6_autgroup(sK11609_skl,X1)))),
% 21.14/12.12 inference(resolution,[status(thm)],[f174983,f147710])).
% 21.14/12.12 fof(f174985,plain,(
% 21.73/12.37 ![X0,X1]: (~m1_subset_1(X0,u1_struct_0(sK11609_skl))|~m1_subset_1(X1,u1_struct_0(sK11609_skl))|k6_autgroup(sK11609_skl,k1_group_1(sK11609_skl,X0,X1))=k7_funct_2(u1_struct_0(sK11609_skl),u1_struct_0(sK11609_skl),u1_struct_0(sK11609_skl),k6_autgroup(sK11609_skl,X0),k6_autgroup(sK11609_skl,X1)))),
% 21.73/12.37 inference(forward_subsumption_resolution,[status(thm)],[f174984,f147711])).
% 21.73/12.37 fof(f174989,plain,(
% 21.73/12.37 ![X0]: (~l1_group_1(sK11609_skl)|~m1_subset_1(X0,u1_struct_0(sK11609_skl))|k1_group_1(sK11609_skl,k3_group_1(sK11609_skl,X0),X0)=k2_group_1(sK11609_skl))),
% 21.73/12.37 inference(forward_subsumption_resolution,[status(thm)],[f174874,f147709])).
% 21.73/12.37 fof(f174990,plain,(
% 21.73/12.37 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK11609_skl))|k1_group_1(sK11609_skl,k3_group_1(sK11609_skl,X0),X0)=k2_group_1(sK11609_skl))),
% 21.73/12.37 inference(resolution,[status(thm)],[f174989,f147711])).
% 21.73/12.37 fof(f175014,plain,(
% 21.73/12.37 k1_group_1(sK11609_skl,k3_group_1(sK11609_skl,sK11610_skl),sK11610_skl)=k2_group_1(sK11609_skl)),
% 21.73/12.37 inference(resolution,[status(thm)],[f174990,f147712])).
% 21.73/12.37 fof(f175285,plain,(
% 21.73/12.37 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK11609_skl))|k6_autgroup(sK11609_skl,k1_group_1(sK11609_skl,X0,sK11610_skl))=k7_funct_2(u1_struct_0(sK11609_skl),u1_struct_0(sK11609_skl),u1_struct_0(sK11609_skl),k6_autgroup(sK11609_skl,X0),k6_autgroup(sK11609_skl,sK11610_skl)))),
% 21.73/12.37 inference(resolution,[status(thm)],[f174985,f147712])).
% 21.73/12.37 fof(f176125,plain,(
% 21.73/12.37 k6_autgroup(sK11609_skl,k1_group_1(sK11609_skl,k3_group_1(sK11609_skl,sK11610_skl),sK11610_skl))=k7_funct_2(u1_struct_0(sK11609_skl),u1_struct_0(sK11609_skl),u1_struct_0(sK11609_skl),k6_autgroup(sK11609_skl,k3_group_1(sK11609_skl,sK11610_skl)),k6_autgroup(sK11609_skl,sK11610_skl))),
% 21.73/12.37 inference(resolution,[status(thm)],[f175285,f174586])).
% 21.73/12.37 fof(f176128,plain,(
% 21.73/12.37 k6_autgroup(sK11609_skl,k2_group_1(sK11609_skl))=k7_funct_2(u1_struct_0(sK11609_skl),u1_struct_0(sK11609_skl),u1_struct_0(sK11609_skl),k6_autgroup(sK11609_skl,k3_group_1(sK11609_skl,sK11610_skl)),k6_autgroup(sK11609_skl,sK11610_skl))),
% 21.73/12.37 inference(forward_demodulation,[status(thm)],[f175014,f176125])).
% 21.73/12.37 fof(f176129,plain,(
% 21.73/12.37 k6_partfun1(u1_struct_0(sK11609_skl))=k7_funct_2(u1_struct_0(sK11609_skl),u1_struct_0(sK11609_skl),u1_struct_0(sK11609_skl),k6_autgroup(sK11609_skl,k3_group_1(sK11609_skl,sK11610_skl)),k6_autgroup(sK11609_skl,sK11610_skl))),
% 21.73/12.37 inference(forward_demodulation,[status(thm)],[f174495,f176128])).
% 21.73/12.37 fof(f176130,plain,(
% 21.73/12.37 $false),
% 21.73/12.37 inference(forward_subsumption_resolution,[status(thm)],[f176129,f174501])).
% 21.73/12.37 % SZS output end CNFRefutation for theBenchmark.p
% 18.51/13.96 % Elapsed time: 13.192038 seconds
% 18.51/13.96 % CPU time: 27.453561 seconds
% 18.51/13.96 % Total memory used: 10.679 GB
% 18.51/13.96 % Net memory used: 10.631 GB
%------------------------------------------------------------------------------