(VAR x)
(SIG (s 1) (p 1) (0 0))
(RULES
   s(p(x)) -> x
   p(s(x)) -> x
)
(COMMENT from a collection of Aoto/Toyama, FSCD 2016)