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