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

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 55
   -(x) <-0|0[]- -(+(x,0())) -3|[]-> +(-(x),-(0()))
   +(x,-(x)) <-0|[]- +(+(x,-(x)),0()) -5|[]-> 0()
   +(x,y) <-0|[]- +(+(x,y),0()) -6|[]-> +(x,+(y,0()))
   +(x,z) <-0|0[]- +(+(x,0()),z) -6|[]-> +(x,+(0(),z))
   +(x,y) <-0|1[]- +(x,+(y,0())) -7|[]-> +(+(x,y),0())
   x <-0|[]- +(x,0()) -8|[]-> +(0(),x)
   -(0()) <-1|0[]- -(-(0())) -2|[]-> 0()
   +(0(),0()) <-1|1[]- +(0(),-(0())) -4|[]-> 0()
   +(+(0(),0()),y) <-1|0,1[]- +(+(0(),-(0())),y) -5|[]-> y
   -(x279) <-2|0[]- -(-(-(x279))) -2|[]-> -(x279)
   +(-(x280),x280) <-2|1[]- +(-(x280),-(-(x280))) -4|[]-> 0()
   +(+(-(x281),x281),y) <-2|0,1[]- +(+(-(x281),-(-(x281))),y) -5|[]-> y
   -(+(-(x282),-(x283))) <-3|0[]- -(-(+(x282,x283))) -2|[]-> +(x282,x283)
   +(+(x284,x285),+(-(x284),-(x285))) <-3|1[]- +(+(x284,x285),-(+(x284,x285))) -4|[]-> 0()
   +(+(+(x286,x287),+(-(x286),-(x287))),y) <-3|0,1[]- +(+(+(x286,x287),-(+(x286,x287))),y) -5|
                                                      []-> y
   -(0()) <-4|0[]- -(+(x,-(x))) -3|[]-> +(-(x),-(-(x)))
   0() <-4|[]- +(+(x,-(x)),-(+(x,-(x)))) -5|[]-> -(+(x,-(x)))
   +(0(),y) <-4|0[]- +(+(x,-(x)),y) -5|[]-> y
   0() <-4|[]- +(+(x,y),-(+(x,y))) -6|[]-> +(x,+(y,-(+(x,y))))
   +(0(),z) <-4|0[]- +(+(x,-(x)),z) -6|[]-> +(x,+(-(x),z))
   +(x,0()) <-4|1[]- +(x,+(y,-(y))) -7|[]-> +(+(x,y),-(y))
   0() <-4|[]- +(x,-(x)) -8|[]-> +(-(x),x)
   0() <-5|[]- +(+(x295,-(x295)),0()) -0|[]-> +(x295,-(x295))
   -(y) <-5|0[]- -(+(+(x297,-(x297)),y)) -3|[]-> +(-(+(x297,-(x297))),-(y))
   -(+(x299,-(x299))) <-5|[]- +(+(x299,-(x299)),-(+(x299,-(x299)))) -4|[]-> 0()
   +(-(+(x301,-(x301))),y) <-5|0[]- +(+(+(x301,-(x301)),-(+(x301,-(x301)))),y) -5|[]-> y
   z <-5|[]- +(+(x,-(x)),z) -6|[]-> +(x,+(-(x),z))
   +(y,z) <-5|0[]- +(+(+(x305,-(x305)),y),z) -6|[]-> +(+(x305,-(x305)),+(y,z))
   +(y,z) <-5|[]- +(+(x307,-(x307)),+(y,z)) -7|[]-> +(+(+(x307,-(x307)),y),z)
   +(x,z) <-5|1[]- +(x,+(+(x309,-(x309)),z)) -7|[]-> +(+(x,+(x309,-(x309))),z)
   y <-5|[]- +(+(x311,-(x311)),y) -8|[]-> +(y,+(x311,-(x311)))
   +(x313,+(x314,0())) <-6|[]- +(+(x313,x314),0()) -0|[]-> +(x313,x314)
   -(+(x316,+(x317,y))) <-6|0[]- -(+(+(x316,x317),y)) -3|[]-> +(-(+(x316,x317)),-(y))
   +(x319,+(x320,-(+(x319,x320)))) <-6|[]- +(+(x319,x320),-(+(x319,x320))) -4|[]-> 0()
   +(x,+(-(x),y)) <-6|[]- +(+(x,-(x)),y) -5|[]-> y
   +(+(x325,+(x326,-(+(x325,x326)))),y) <-6|0[]- +(+(+(x325,x326),-(+(x325,x326))),y) -5|[]-> y
   +(+(x328,+(x329,y)),z) <-6|0[]- +(+(+(x328,x329),y),z) -6|[]-> +(+(x328,x329),+(y,z))
   +(x331,+(x332,+(y,z))) <-6|[]- +(+(x331,x332),+(y,z)) -7|[]-> +(+(+(x331,x332),y),z)
   +(x,+(x334,+(x335,z))) <-6|1[]- +(x,+(+(x334,x335),z)) -7|[]-> +(+(x,+(x334,x335)),z)
   +(x337,+(x338,y)) <-6|[]- +(+(x337,x338),y) -8|[]-> +(y,+(x337,x338))
   -(+(+(x,x341),x342)) <-7|0[]- -(+(x,+(x341,x342))) -3|[]-> +(-(x),-(+(x341,x342)))
   +(+(+(x,-(x)),x344),x345) <-7|[]- +(+(x,-(x)),+(x344,x345)) -5|[]-> +(x344,x345)
   +(+(+(x,y),x347),x348) <-7|[]- +(+(x,y),+(x347,x348)) -6|[]-> +(x,+(y,+(x347,x348)))
   +(+(+(x,x350),x351),z) <-7|0[]- +(+(x,+(x350,x351)),z) -6|[]-> +(x,+(+(x350,x351),z))
   +(x,+(+(y,x353),x354)) <-7|1[]- +(x,+(y,+(x353,x354))) -7|[]-> +(+(x,y),+(x353,x354))
   +(+(x,x356),x357) <-7|[]- +(x,+(x356,x357)) -8|[]-> +(+(x356,x357),x)
   +(0(),x) <-8|[]- +(x,0()) -0|[]-> x
   -(+(y,x)) <-8|0[]- -(+(x,y)) -3|[]-> +(-(x),-(y))
   +(-(x),x) <-8|[]- +(x,-(x)) -4|[]-> 0()
   +(y,+(x,-(x))) <-8|[]- +(+(x,-(x)),y) -5|[]-> y
   +(+(-(x),x),y) <-8|0[]- +(+(x,-(x)),y) -5|[]-> y
   +(z,+(x,y)) <-8|[]- +(+(x,y),z) -6|[]-> +(x,+(y,z))
   +(+(y,x),z) <-8|0[]- +(+(x,y),z) -6|[]-> +(x,+(y,z))
   +(+(y,z),x) <-8|[]- +(x,+(y,z)) -7|[]-> +(+(x,y),z)
   +(x,+(z,y)) <-8|1[]- +(x,+(y,z)) -7|[]-> +(+(x,y),z)
  Redundant Rules Transformation:
   +(x,0()) -> x
   -(0()) -> 0()
   -(-(x)) -> x
   -(+(x,y)) -> +(-(x),-(y))
   +(x,-(x)) -> 0()
   +(x,+(y,z)) -> +(+(x,y),z)
   +(x,y) -> +(y,x)
   Church Rosser Transformation Processor (ac):
    f4_AC(x,0()) -> x
    -(0()) -> 0()
    -(-(x)) -> x
    -(f4_AC(x,y)) -> f4_AC(-(x),-(y))
    f4_AC(x,-(x)) -> 0()
    AC critical peaks: joinable
    AC-KBO Processor:
     precedence:
      - > f4_AC > 0
      weight function:
       w0 = 2
       w(0) = 7
       w(f4_AC) = 3
       w(-) = 0
      problem:
       
      Qed