(VAR x)
(RULES
  f(g(f(x))) -> x
  f(g(x)) -> g(f(x))
)
(COMMENT
doi:10.1017/CBO9781139172752
[4] Exercise 6.5(a)
submitted by: Takahito Aoto, Junichi Yoshida, and Yoshihito Toyama
)