YES

Problem:
 f(a(),b()) -> c()
 a() -> a'()
 b() -> b'()
 c() -> f(a'(),b())
 c() -> f(a(),b'())
 c() -> f(a(),b())

Proof:
 Ground Confluence Processor:
  confluent by decision procedure.