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

Proof:
 Nonconfluence Processor:
  terms: if(y,x,s(+(x,-(y,s(0()))))) *<- +(x,y) ->* if(x,y,s(+(-(x,s(0())),y)))
  Qed