(VAR x1 ) (RULES b(b(x1)) -> c(d(x1)) c(c(x1)) -> d(d(d(x1))) c(x1) -> g(x1) d(d(x1)) -> c(f(x1)) d(d(d(x1))) -> g(c(x1)) f(x1) -> a(g(x1)) g(x1) -> d(a(b(x1))) g(g(x1)) -> b(c(x1)) )