  We present a new encoding of the Battle of Hercules and Hydra as a rewrite
system with AC symbols. Unlike earlier term rewriting encodings, it faithfully
models any strategy of Hercules to beat Hydra. To prove the termination of our
encoding, we employ type introduction in connection with many-sorted semantic
labeling for AC rewriting and AC-MPO, a new AC compatible reduction order that
can be seen as a much weakened version of AC-RPO.
