YES
Time: 0.009303
TRS:
 {  p(m, n, s r) -> p(m, r, n),
  p(m, s n, 0()) -> p(0(), n, m),
  p(m, 0(), 0()) -> m}
 DP:
  DP:
   {  p#(m, n, s r) -> p#(m, r, n),
    p#(m, s n, 0()) -> p#(0(), n, m)}
  TRS:
  {  p(m, n, s r) -> p(m, r, n),
   p(m, s n, 0()) -> p(0(), n, m),
   p(m, 0(), 0()) -> m}
  UR:
   {}
   EDG:
    {(p#(m, n, s r) -> p#(m, r, n), p#(m, s n, 0()) -> p#(0(), n, m))
     (p#(m, n, s r) -> p#(m, r, n), p#(m, n, s r) -> p#(m, r, n))
     (p#(m, s n, 0()) -> p#(0(), n, m), p#(m, n, s r) -> p#(m, r, n))
     (p#(m, s n, 0()) -> p#(0(), n, m), p#(m, s n, 0()) -> p#(0(), n, m))}
    STATUS:
     arrows: 0.000000
     SCCS (1):
      Scc:
       {  p#(m, n, s r) -> p#(m, r, n),
        p#(m, s n, 0()) -> p#(0(), n, m)}
      
      SCC (2):
       Strict:
        {  p#(m, n, s r) -> p#(m, r, n),
         p#(m, s n, 0()) -> p#(0(), n, m)}
       Weak:
       {  p(m, n, s r) -> p(m, r, n),
        p(m, s n, 0()) -> p(0(), n, m),
        p(m, 0(), 0()) -> m}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [p](x0, x1, x2) = 0,
         
         [s](x0) = x0 + 1,
         
         [0] = 1,
         
         [p#](x0, x1, x2) = x0 + x1 + x2
        Strict:
         p#(m, s n, 0()) -> p#(0(), n, m)
         2 + 1m + 1n >= 1 + 1m + 1n
         p#(m, n, s r) -> p#(m, r, n)
         1 + 1m + 1r + 1n >= 0 + 1m + 1r + 1n
        Weak:
         p(m, 0(), 0()) -> m
         0 + 0m >= 1m
         p(m, s n, 0()) -> p(0(), n, m)
         0 + 0m + 0n >= 0 + 0m + 0n
         p(m, n, s r) -> p(m, r, n)
         0 + 0m + 0r + 0n >= 0 + 0m + 0r + 0n
       Qed