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

Proof:
 Nonconfluence Processor:
  terms: s(s(s(+(x217,+(x217,x217))))) *<- +(+(s(x217),s(x217)),s(x217)) ->* 
  s(s(+(x217,s(+(x217,x217)))))
  Qed