YES
Time: 0.005148
TRS:
 {  f(x, y, s z) -> s f(0(), 1(), z),
  f(0(), 1(), x) -> f(s x, x, x)}
 DP:
  DP:
   {  f#(x, y, s z) -> f#(0(), 1(), z),
    f#(0(), 1(), x) -> f#(s x, x, x)}
  TRS:
  {  f(x, y, s z) -> s f(0(), 1(), z),
   f(0(), 1(), x) -> f(s x, x, x)}
  UR:
   {a(w, v) -> w,
    a(w, v) -> v}
   EDG:
    {(f#(0(), 1(), x) -> f#(s x, x, x), f#(0(), 1(), x) -> f#(s x, x, x))
     (f#(0(), 1(), x) -> f#(s x, x, x), f#(x, y, s z) -> f#(0(), 1(), z))
     (f#(x, y, s z) -> f#(0(), 1(), z), f#(x, y, s z) -> f#(0(), 1(), z))
     (f#(x, y, s z) -> f#(0(), 1(), z), f#(0(), 1(), x) -> f#(s x, x, x))}
    EDG:
     {(f#(0(), 1(), x) -> f#(s x, x, x), f#(x, y, s z) -> f#(0(), 1(), z))
      (f#(x, y, s z) -> f#(0(), 1(), z), f#(x, y, s z) -> f#(0(), 1(), z))
      (f#(x, y, s z) -> f#(0(), 1(), z), f#(0(), 1(), x) -> f#(s x, x, x))}
     EDG:
      {(f#(0(), 1(), x) -> f#(s x, x, x), f#(x, y, s z) -> f#(0(), 1(), z))
       (f#(x, y, s z) -> f#(0(), 1(), z), f#(x, y, s z) -> f#(0(), 1(), z))
       (f#(x, y, s z) -> f#(0(), 1(), z), f#(0(), 1(), x) -> f#(s x, x, x))}
      EDG:
       {(f#(0(), 1(), x) -> f#(s x, x, x), f#(x, y, s z) -> f#(0(), 1(), z))
        (f#(x, y, s z) -> f#(0(), 1(), z), f#(x, y, s z) -> f#(0(), 1(), z))
        (f#(x, y, s z) -> f#(0(), 1(), z), f#(0(), 1(), x) -> f#(s x, x, x))}
       STATUS:
        arrows: 0.250000
        SCCS (1):
         Scc:
          {  f#(x, y, s z) -> f#(0(), 1(), z),
           f#(0(), 1(), x) -> f#(s x, x, x)}
         
         SCC (2):
          Strict:
           {  f#(x, y, s z) -> f#(0(), 1(), z),
            f#(0(), 1(), x) -> f#(s x, x, x)}
          Weak:
          {  f(x, y, s z) -> s f(0(), 1(), z),
           f(0(), 1(), x) -> f(s x, x, x)}
          POLY:
           Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
           Interpretation:
            [f](x0, x1, x2) = 0,
            
            [s](x0) = x0 + 1,
            
            [0] = 0,
            
            [1] = 0,
            
            [f#](x0, x1, x2) = x0
           Strict:
            f#(0(), 1(), x) -> f#(s x, x, x)
            0 + 1x >= 0 + 1x
            f#(x, y, s z) -> f#(0(), 1(), z)
            1 + 0x + 1z + 0y >= 0 + 1z
           Weak:
            f(0(), 1(), x) -> f(s x, x, x)
            0 + 0x >= 0 + 0x
            f(x, y, s z) -> s f(0(), 1(), z)
            0 + 0x + 0z + 0y >= 1 + 0z
          SCCS (0):