Problem:
 c() -> f(a(),b())
 c() -> f(a(),a())
 f(x,x) -> x
 f(x,y) -> f(y,x)
 f(a(),a()) -> f(b(),b())
 f(b(),b()) -> f(a(),a())

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