YES
(VAR x y)
(RULES
eq(p(x),x) -> false()
eq(x,p(x)) -> false()
eq(x,s(y)) -> eq(p(x),y)
eq(s(x),y) -> eq(x,p(y))
p(s(x)) -> x
eq(x,x) -> true()
eq(p(x),p(y)) -> eq(x,y)
)