MAYBE Problem: b(a(a(x1))) -> a(b(c(x1))) c(a(x1)) -> a(c(x1)) b(c(a(x1))) -> a(b(c(x1))) c(b(x1)) -> d(x1) a(d(x1)) -> d(a(x1)) d(x1) -> b(a(x1)) L(a(a(x1))) -> L(a(b(c(x1)))) c(R(x1)) -> c(b(R(x1))) Proof: Open