Problem: a() -> a() a() -> b() f(a(),a()) -> f(b(),f(f(a(),b()),a())) Proof: Nonconfluence Processor: terms: f(a(),b()) *<- f(a(),a()) ->* f(b(),f(f(a(),b()),a())) Qed