(VAR x y z)
(RULES
f(f(x, y), z) -> f(x, f(y, z))
f(a1, y) -> y
f(a2, y) -> y
f(x, i1(x)) -> a1
f(x, i2(x)) -> a2
)
(COMMENT Example A2 from \cite{Chr89})