(CONDITIONTYPE ORIENTED)
(VAR x y z)
(RULES
  f(c(x),c(c(y))) -> a(a(x)) | c(f(x,y)) == c(a(b))
  f(c(c(c(x))),y) -> a(y) | c(f(c(x),c(c(y)))) == c(a(a(b)))
  h(b) -> b
  h(a(a(x))) -> a(b) | h(x) == b
)
(COMMENT from http://www.trs.cm.is.nagoya-u.ac.jp/co3/index.html#NKYG15v1.2)