NO

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

Proof:
 Nonconfluence Processor:
  terms: +(s(f99()),f98()) *<- +(+(s(0()),f99()),f98()) ->* s(+(f99(),f98()))
  Qed
  
  first automaton:
   final states: {214}
   transitions:
    f99() -> 216*
    +(215,217) -> 214*
    +(217,215) -> 214*
    s(217) -> 217*
    s(216) -> 217*
    f98() -> 215*
  
  second automaton:
   final states: {224}
   transitions:
    f99() -> 226*
    +(226,225) -> 227*
    +(225,226) -> 227*
    s(227) -> 224*
    s(224) -> 224*
    f98() -> 225*