(VAR x)
(RULES
  a -> b
  f(a,b) -> f(a,a)
  f(b,a) -> f(a,a)
  f(a,a) -> c
  g(x) -> f(x,x)
)
(COMMENT
doi:10.23638/LMCS-13(2:4)2017
[131] Example 5.11
submitted by: Julian Nagele
)