(VAR x1 ) (RULES b(a(a(x1))) -> a(b(c(x1))) c(a(x1)) -> a(c(x1)) c(b(x1)) -> b(a(x1)) L(a(a(x1))) -> L(a(b(c(x1)))) c(R(x1)) -> b(a(R(x1))) )