YES Problem: w(r(x)) -> r(w(x)) b(r(x)) -> r(b(x)) b(w(x)) -> w(b(x)) Proof: KBO Processor: weight function: w0 = 1 w(b) = w(w) = w(r) = 1 precedence: b > w > r problem: Qed