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

Proof:
 Church Rosser Transformation Processor (ac):
  -(+(x,-(x))) -> 0()
  +(x,-(x)) -> 0()
  -(+(0(),0())) -> 0()
  +(0(),0()) -> 0()
  -(0()) -> 0()
  AC critical peaks: joinable
  AC-KBO Processor:
   precedence:
    0 > + > -
    weight function:
     w0 = 1
     w(-) = 7
     w(0) = 1
     w(+) = 0
    problem:
     
    Qed