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