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 ELPO with interpretations on natural numbers

  p_A(x1) = x1 + 1
  s_A(x1) = x1 + 2
  eq_A(x1,x2) = x1 + x2
  true_A = 0
  false_A = 1
  eq#_A(x1,x2) = x1 + x2
  true#_A = 0
  false#_A = 0

and precedence:

eq > p > s > true > false
)