YES

Problem:
 -(+(x(),-(x()))) -> 0()
 +(x(),-(x())) -> 0()
 0() -> -(0())

Proof:
 Uncurry Processor:
  f4(-(),f4(f4(+(),x()),f4(-(),x()))) -> 0()
  f4(f4(+(),x()),f4(-(),x())) -> 0()
  0() -> f4(-(),0())
  Ground Confluence Processor:
   confluent by decision procedure.