(ignored inputs)COMMENT A Complete Set of Axioms for Group Theory , Example 1 of \cite{KB70}
Rewrite Rules:
   [ *(e,?x) -> ?x,
     *(-(?x),?x) -> e,
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     *(-(?x),*(?x,?y)) -> ?y,
     *(?x,e) -> ?x,
     -(e) -> e,
     -(-(?x)) -> ?x,
     *(?x,-(?x)) -> e,
     *(?x,*(-(?x),?y)) -> ?y,
     -(*(?x,?y)) -> *(-(?y),-(?x)) ]
Apply Direct Methods...
Inner CPs:
   [ *(e,e) = e,
     *(?x_5,-(?x_5)) = e,
     *(*(-(?y_8),-(?x_8)),*(?x_8,?y_8)) = e,
     *(?x,?z_2) = *(e,*(?x,?z_2)),
     *(e,?z_2) = *(-(?x_1),*(?x_1,?z_2)),
     *(?y_3,?z_2) = *(-(?x_3),*(*(?x_3,?y_3),?z_2)),
     *(?x_4,?z_2) = *(?x_4,*(e,?z_2)),
     *(e,?z_2) = *(?x_6,*(-(?x_6),?z_2)),
     *(?y_7,?z_2) = *(?x_7,*(*(-(?x_7),?y_7),?z_2)),
     *(-(e),?x) = ?x,
     *(-(-(?x_1)),e) = ?x_1,
     *(-(*(?x_2,?y_2)),*(?x_2,*(?y_2,?z_2))) = ?z_2,
     *(-(?x_4),?x_4) = e,
     *(e,*(e,?y_3)) = ?y_3,
     *(?x_5,*(-(?x_5),?y_3)) = ?y_3,
     *(-(?x_6),e) = -(?x_6),
     *(-(?x_7),?y_7) = *(-(?x_7),?y_7),
     *(*(-(?y_8),-(?x_8)),*(*(?x_8,?y_8),?y_3)) = ?y_3,
     -(e) = e,
     -(*(-(?y_8),-(?x_8))) = *(?x_8,?y_8),
     *(e,e) = e,
     *(-(?x_5),?x_5) = e,
     *(*(?x_8,?y_8),*(-(?y_8),-(?x_8))) = e,
     *(?x_1,e) = ?x_1,
     *(?x_3,?y_3) = *(?x_3,?y_3),
     *(?x_7,-(?x_7)) = e,
     *(e,*(e,?y_7)) = ?y_7,
     *(-(?x_5),*(?x_5,?y_7)) = ?y_7,
     *(?x_7,e) = -(-(?x_7)),
     *(*(?x_8,?y_8),*(*(-(?y_8),-(?x_8)),?y_7)) = ?y_7,
     -(?x) = *(-(?x),-(e)),
     -(e) = *(-(?x_1),-(-(?x_1))),
     -(*(?x_2,*(?y_2,?z_2))) = *(-(?z_2),-(*(?x_2,?y_2))),
     -(?y_3) = *(-(*(?x_3,?y_3)),-(-(?x_3))),
     -(?x_4) = *(-(e),-(?x_4)),
     -(e) = *(-(-(?x_6)),-(?x_6)),
     -(?y_7) = *(-(*(-(?x_7),?y_7)),-(?x_7)),
     *(*(?x,*(?y,?z)),?z_1) = *(*(?x,?y),*(?z,?z_1)),
     *(-(-(?x)),?y) = *(?x,?y),
     -(?x) = -(?x),
     *(?x_1,?y) = *(-(-(?x_1)),?y) ]
Outer CPs:
   [ e = e,
     -(e) = e,
     *(-(e),?y_7) = ?y_7,
     e = -(e),
     *(?x_2,*(?y_2,e)) = *(?x_2,?y_2),
     *(?x_2,*(?y_2,-(*(?x_2,?y_2)))) = e,
     *(?x_2,*(?y_2,*(-(*(?x_2,?y_2)),?y_7))) = ?y_7 ]
not Overlay, check Termination...
Terminating, WCR
Knuth&Bendix
Direct Methods: CR

Final result: CR
/local-scratch/hzankl/2012/cops2012/51.trs: Success(CR)
(12 msec.)