YES
TRS:
 { -(x, 0()) -> x,
  -(x, s(y)) -> if(greater(x, s(y)), s(-(x, p(s(y)))), 0()),
   -(0(), y) -> 0(),
      p(0()) -> 0(),
     p(s(x)) -> x}
 DP:
  Strict:
   {-#(x, s(y)) -> -#(x, p(s(y))),
    -#(x, s(y)) -> p#(s(y))}
  Weak:
  { -(x, 0()) -> x,
   -(x, s(y)) -> if(greater(x, s(y)), s(-(x, p(s(y)))), 0()),
    -(0(), y) -> 0(),
       p(0()) -> 0(),
      p(s(x)) -> x}
  EDG:
   {(-#(x, s(y)) -> -#(x, p(s(y))), -#(x, s(y)) -> -#(x, p(s(y))))
    (-#(x, s(y)) -> -#(x, p(s(y))), -#(x, s(y)) -> p#(s(y)))}
   SCCS:
    Scc:
     {-#(x, s(y)) -> -#(x, p(s(y)))}
    SCC:
     Strict:
      {-#(x, s(y)) -> -#(x, p(s(y)))}
     Weak:
     { -(x, 0()) -> x,
      -(x, s(y)) -> if(greater(x, s(y)), s(-(x, p(s(y)))), 0()),
       -(0(), y) -> 0(),
          p(0()) -> 0(),
         p(s(x)) -> x}
     UR:
      {p(s(x)) -> x}
      BOUND:
       Bound: match(-raise)-DP-bounded by 0
       Automaton:
        {     a_0() -> 2*
             p_0(3) -> 4*
             s_0(2) -> 3*
         -#_0(2, 4) -> 1*
                  2 -> 4*}
       Strict:
        {}
       Qed