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