(VAR y x)
(RULES
   +(0,y) -> y
   +(s(x),y) -> s(+(x,y))
   +(p(x),y) -> p(+(y,x))
   p(s(x)) -> s(p(x))
   s(p(x)) -> x
)
(COMMENT from a collection of Aoto/Toyama/Kimura, FSCD 2017)