NO Problem: a(a(x)) -> b(b(b(x))) b(b(b(b(x)))) -> a(a(a(x))) Proof: Nonconfluence Processor: terms: a(b(b(b(x17)))) *<- a(a(a(x17))) ->* b(b(b(a(x17)))) Qed