YES

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

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 28
   +(y,0()) <-0|[]- +(0(),y) -1|[]-> y
   +(0(),x) <-0|[]- +(x,0()) -2|[]-> x
   +(y,s(x)) <-0|[]- +(s(x),y) -3|[]-> s(+(x,y))
   +(s(y),x) <-0|[]- +(x,s(y)) -4|[]-> +(s(x),y)
   +(+(y,z),x) <-0|[]- +(x,+(y,z)) -5|[]-> +(+(x,y),z)
   +(x,+(z,y)) <-0|1[]- +(x,+(y,z)) -5|[]-> +(+(x,y),z)
   y <-1|[]- +(0(),y) -0|[]-> +(y,0())
   0() <-1|[]- +(0(),0()) -2|[]-> 0()
   s(y) <-1|[]- +(0(),s(y)) -4|[]-> +(s(0()),y)
   +(y,z) <-1|[]- +(0(),+(y,z)) -5|[]-> +(+(0(),y),z)
   +(x,z) <-1|1[]- +(x,+(0(),z)) -5|[]-> +(+(x,0()),z)
   x <-2|[]- +(x,0()) -0|[]-> +(0(),x)
   0() <-2|[]- +(0(),0()) -1|[]-> 0()
   s(x) <-2|[]- +(s(x),0()) -3|[]-> s(+(x,0()))
   +(x,y) <-2|1[]- +(x,+(y,0())) -5|[]-> +(+(x,y),0())
   s(+(x145,y)) <-3|[]- +(s(x145),y) -0|[]-> +(y,s(x145))
   s(+(x147,0())) <-3|[]- +(s(x147),0()) -2|[]-> s(x147)
   s(+(x149,s(y))) <-3|[]- +(s(x149),s(y)) -4|[]-> +(s(s(x149)),y)
   s(+(x151,+(y,z))) <-3|[]- +(s(x151),+(y,z)) -5|[]-> +(+(s(x151),y),z)
   +(x,s(+(x153,z))) <-3|1[]- +(x,+(s(x153),z)) -5|[]-> +(+(x,s(x153)),z)
   +(s(x),x156) <-4|[]- +(x,s(x156)) -0|[]-> +(s(x156),x)
   +(s(0()),x158) <-4|[]- +(0(),s(x158)) -1|[]-> s(x158)
   +(s(s(x)),x160) <-4|[]- +(s(x),s(x160)) -3|[]-> s(+(x,s(x160)))
   +(x,+(s(y),x162)) <-4|1[]- +(x,+(y,s(x162))) -5|[]-> +(+(x,y),s(x162))
   +(+(x,x164),x165) <-5|[]- +(x,+(x164,x165)) -0|[]-> +(+(x164,x165),x)
   +(+(0(),x167),x168) <-5|[]- +(0(),+(x167,x168)) -1|[]-> +(x167,x168)
   +(+(s(x),x170),x171) <-5|[]- +(s(x),+(x170,x171)) -3|[]-> s(+(x,+(x170,x171)))
   +(x,+(+(y,x173),x174)) <-5|1[]- +(x,+(y,+(x173,x174))) -5|[]-> +(+(x,y),+(x173,x174))
  Redundant Rules Transformation:
   +(x,y) -> +(y,x)
   +(x,0()) -> x
   +(s(x),y) -> s(+(x,y))
   +(x,+(y,z)) -> +(+(x,y),z)
   Church Rosser Transformation Processor (ac):
    f3_AC(x,0()) -> x
    f3_AC(s(x),y) -> s(f3_AC(x,y))
    AC critical peaks: joinable
    AC-KBO Processor:
     precedence:
      f3_AC > s > 0
      weight function:
       w0 = 4
       w(0) = 4
       w(s) = 2
       w(f3_AC) = 0
      problem:
       
      Qed