NO Problem: a() -> f(a(),b()) f(a(),b()) -> f(b(),a()) Proof: Ground Confluence Processor: non-confluent by decision procedure.