YES Problem: a(b(x)) -> b(a(x)) a(c(x)) -> x Proof: String Reversal Processor: b(a(x)) -> a(b(x)) c(a(x)) -> x KBO Processor: weight function: w0 = 1 w(c) = w(a) = 1 w(b) = 0 precedence: b > a > c problem: Qed