(VAR x)
(RULES
  c(b(x)) -> c(a(x))
  a(b(x)) -> b(a(x))
  b(b(x)) -> c(a(x))
  c(c(x)) -> c(b(x))
  a(a(x)) -> b(b(x))
  c(a(x)) -> a(a(x))
  b(a(x)) -> b(a(x))
  a(a(x)) -> b(c(x))
)
(COMMENT
submitted by: Johannes Waldmann
)