(VAR x)
(RULES
f(a, a) -> c 
f(b, x) -> f(x, x)
f(x, b) -> f(x, x) 
a -> b
)
(COMMENT 
Example 8 in Nao Hirokawa and Aart Middeldorp, Decreasing Diagrams and
Relative Termination, JAR.  This example was provided by Vincent van
Oostrom.
)