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