Automatic Inference of Term Equivalence in Term Rewriting Systems