(VAR x y)
(RULES
f(a) -> c
f(b) -> d
a -> b
b -> a
)
(COMMENT
Example 5 (R2) in Nao Hirokawa and Aart Middeldorp, Decreasing Diagrams and
Relative Termination, JAR.  This TRS is not confluent.
)