Problem:
 b() -> c()
 a() -> a()

Proof:
 Uncurry Processor:
  b() -> c()
  a() -> a()
  Ground Confluence Processor:
   NFP by decision procedure.