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

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

weights

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

and precedence:

p > s > eq > true > false
)