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

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 73
   +(y,z) <-0|0[]- +(+(0(),y),z) -2|[]-> +(0(),+(y,z))
   +(-(0()),y) <-0|1[]- +(-(0()),+(0(),y)) -3|[]-> y
   0() <-0|[]- +(0(),0()) -4|[]-> 0()
   -(0()) <-0|[]- +(0(),-(0())) -7|[]-> 0()
   +(-(0()),y) <-0|[]- +(0(),+(-(0()),y)) -8|[]-> y
   -(y) <-0|0[]- -(+(0(),y)) -9|[]-> +(-(y),-(0()))
   y <-0|[]- +(0(),y) -10|[]-> +(y,0())
   +(0(),z) <-1|0[]- +(+(-(y),y),z) -2|[]-> +(-(y),+(y,z))
   +(-(-(y)),0()) <-1|1[]- +(-(-(y)),+(-(y),y)) -3|[]-> y
   0() <-1|[]- +(-(0()),0()) -4|[]-> -(0())
   +(y,0()) <-1|1[]- +(y,+(-(y),y)) -8|[]-> y
   -(0()) <-1|0[]- -(+(-(y),y)) -9|[]-> +(-(y),-(-(y)))
   0() <-1|[]- +(-(y),y) -10|[]-> +(y,-(y))
   +(+(x384,+(x385,y)),z) <-2|0[]- +(+(+(x384,x385),y),z) -2|[]-> +(+(x384,x385),+(y,z))
   +(-(+(x387,x388)),+(x387,+(x388,y))) <-2|1[]- +(-(+(x387,x388)),+(+(x387,x388),y)) -3|[]-> y
   +(x390,+(x391,0())) <-2|[]- +(+(x390,x391),0()) -4|[]-> +(x390,x391)
   +(x393,+(x394,-(+(x393,x394)))) <-2|[]- +(+(x393,x394),-(+(x393,x394))) -7|[]-> 0()
   +(x396,+(x397,+(-(+(x396,x397)),y))) <-2|[]- +(+(x396,x397),+(-(+(x396,x397)),y)) -8|[]-> y
   -(+(x399,+(x400,y))) <-2|0[]- -(+(+(x399,x400),y)) -9|[]-> +(-(y),-(+(x399,x400)))
   +(x402,+(x403,y)) <-2|[]- +(+(x402,x403),y) -10|[]-> +(y,+(x402,x403))
   +(x406,z) <-3|0[]- +(+(-(x405),+(x405,x406)),z) -2|[]-> +(-(x405),+(+(x405,x406),z))
   +(-(-(x407)),x408) <-3|1[]- +(-(-(x407)),+(-(x407),+(x407,x408))) -3|[]-> +(x407,x408)
   +(x,x410) <-3|1[]- +(x,+(-(x),+(x,x410))) -8|[]-> +(x,x410)
   -(x412) <-3|0[]- -(+(-(x411),+(x411,x412))) -9|[]-> +(-(+(x411,x412)),-(-(x411)))
   x414 <-3|[]- +(-(x413),+(x413,x414)) -10|[]-> +(+(x413,x414),-(x413))
   0() <-4|[]- +(0(),0()) -0|[]-> 0()
   -(0()) <-4|[]- +(-(0()),0()) -1|[]-> 0()
   +(x,y) <-4|[]- +(+(x,y),0()) -2|[]-> +(x,+(y,0()))
   +(x,z) <-4|0[]- +(+(x,0()),z) -2|[]-> +(x,+(0(),z))
   +(-(x),x) <-4|1[]- +(-(x),+(x,0())) -3|[]-> 0()
   +(x,-(x)) <-4|1[]- +(x,+(-(x),0())) -8|[]-> 0()
   -(x) <-4|0[]- -(+(x,0())) -9|[]-> +(-(0()),-(x))
   x <-4|[]- +(x,0()) -10|[]-> +(0(),x)
   +(0(),0()) <-5|0[]- +(-(0()),0()) -1|[]-> 0()
   +(0(),+(0(),y)) <-5|0[]- +(-(0()),+(0(),y)) -3|[]-> y
   -(0()) <-5|0[]- -(-(0())) -6|[]-> 0()
   +(0(),0()) <-5|1[]- +(0(),-(0())) -7|[]-> 0()
   +(0(),+(0(),y)) <-5|1,0[]- +(0(),+(-(0()),y)) -8|[]-> y
   +(x423,-(x423)) <-6|0[]- +(-(-(x423)),-(x423)) -1|[]-> 0()
   +(x424,+(-(x424),y)) <-6|0[]- +(-(-(x424)),+(-(x424),y)) -3|[]-> y
   -(x425) <-6|0[]- -(-(-(x425))) -6|[]-> -(x425)
   +(-(x426),x426) <-6|1[]- +(-(x426),-(-(x426))) -7|[]-> 0()
   +(-(x427),+(x427,y)) <-6|1,0[]- +(-(x427),+(-(-(x427)),y)) -8|[]-> y
   0() <-7|[]- +(0(),-(0())) -0|[]-> -(0())
   0() <-7|[]- +(+(x,y),-(+(x,y))) -2|[]-> +(x,+(y,-(+(x,y))))
   +(0(),z) <-7|0[]- +(+(x,-(x)),z) -2|[]-> +(x,+(-(x),z))
   +(-(x),0()) <-7|1[]- +(-(x),+(x,-(x))) -3|[]-> -(x)
   +(x,0()) <-7|1[]- +(x,+(-(x),-(-(x)))) -8|[]-> -(-(x))
   -(0()) <-7|0[]- -(+(x,-(x))) -9|[]-> +(-(-(x)),-(x))
   0() <-7|[]- +(x,-(x)) -10|[]-> +(-(x),x)
   x436 <-8|[]- +(0(),+(-(0()),x436)) -0|[]-> +(-(0()),x436)
   x438 <-8|[]- +(+(x,y),+(-(+(x,y)),x438)) -2|[]-> +(x,+(y,+(-(+(x,y)),x438)))
   +(x440,z) <-8|0[]- +(+(x,+(-(x),x440)),z) -2|[]-> +(x,+(+(-(x),x440),z))
   +(-(x),x442) <-8|1[]- +(-(x),+(x,+(-(x),x442))) -3|[]-> +(-(x),x442)
   +(x,x444) <-8|1[]- +(x,+(-(x),+(-(-(x)),x444))) -8|[]-> +(-(-(x)),x444)
   -(x446) <-8|0[]- -(+(x,+(-(x),x446))) -9|[]-> +(-(+(-(x),x446)),-(x))
   x448 <-8|[]- +(x,+(-(x),x448)) -10|[]-> +(+(-(x),x448),x)
   +(+(-(x450),-(x449)),+(x449,x450)) <-9|0[]- +(-(+(x449,x450)),+(x449,x450)) -1|[]-> 0()
   +(+(-(x452),-(x451)),+(+(x451,x452),y)) <-9|0[]- +(-(+(x451,x452)),+(+(x451,x452),y)) -3|[]-> y
   -(+(-(x454),-(x453))) <-9|0[]- -(-(+(x453,x454))) -6|[]-> +(x453,x454)
   +(+(x455,x456),+(-(x456),-(x455))) <-9|1[]- +(+(x455,x456),-(+(x455,x456))) -7|[]-> 0()
   +(+(x457,x458),+(+(-(x458),-(x457)),y)) <-9|1,0[]- +(+(x457,x458),+(-(+(x457,x458)),y)) -8|
                                                      []-> y
   +(x,0()) <-10|[]- +(0(),x) -0|[]-> x
   +(x,-(x)) <-10|[]- +(-(x),x) -1|[]-> 0()
   +(z,+(x,y)) <-10|[]- +(+(x,y),z) -2|[]-> +(x,+(y,z))
   +(+(y,x),z) <-10|0[]- +(+(x,y),z) -2|[]-> +(x,+(y,z))
   +(+(x,y),-(x)) <-10|[]- +(-(x),+(x,y)) -3|[]-> y
   +(-(x),+(y,x)) <-10|1[]- +(-(x),+(x,y)) -3|[]-> y
   +(0(),x) <-10|[]- +(x,0()) -4|[]-> x
   +(-(x),x) <-10|[]- +(x,-(x)) -7|[]-> 0()
   +(+(-(x),y),x) <-10|[]- +(x,+(-(x),y)) -8|[]-> y
   +(x,+(y,-(x))) <-10|1[]- +(x,+(-(x),y)) -8|[]-> y
   -(+(y,x)) <-10|0[]- -(+(x,y)) -9|[]-> +(-(y),-(x))
  Redundant Rules Transformation:
   +(+(x,y),z) -> +(x,+(y,z))
   +(x,0()) -> x
   -(0()) -> 0()
   -(-(x)) -> x
   +(x,-(x)) -> 0()
   +(x,+(-(x),y)) -> y
   -(+(x,y)) -> +(-(y),-(x))
   +(x,y) -> +(y,x)
   Church Rosser Transformation Processor (ac):
    f4_AC(x,0()) -> x
    -(0()) -> 0()
    -(-(x)) -> x
    f4_AC(x,-(x)) -> 0()
    f4_AC(x,f4_AC(-(x),y)) -> y
    -(f4_AC(x,y)) -> f4_AC(-(y),-(x))
    AC critical peaks: joinable
    AC-KBO Processor:
     precedence:
      - > 0 > f4_AC
      weight function:
       w0 = 4
       w(f4_AC) = 5
       w(0) = 4
       w(-) = 0
      problem:
       
      Qed