YES

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

(COMMENT
Termination is shown by KBO with weight

  w0 = 1
  w(p) = 1
  w(s) = 2
  w(eq) = 0
  w(true) = 1
  w(false) = 1

and precedence:

  p > s > eq > true > false
)