(VAR x x' ) (RULES b(c(x)) -> b(a(x)) b(a(x)) -> c(b(x)) a(c(x)) -> a(b(x)) c(b(x)) -> a(a(x)) b(a(x)) -> b(c(x)) a(a(x)) -> b(a(x)) a(a(a(x'))) -> a(b(b(x'))) a(b(b(x'))) -> b(a(a(x'))) )