MAYBE
Time: 0.000862
TRS:
 {  quot(x, 0(), s z) -> s quot(x, plus(z, s 0()), s z),
  quot(0(), s y, s z) -> 0(),
    quot(s x, s y, z) -> quot(x, y, z),
         plus(0(), y) -> y,
         plus(s x, y) -> s plus(x, y)}
 DP:
  DP:
   {quot#(x, 0(), s z) -> quot#(x, plus(z, s 0()), s z),
    quot#(x, 0(), s z) -> plus#(z, s 0()),
    quot#(s x, s y, z) -> quot#(x, y, z),
         plus#(s x, y) -> plus#(x, y)}
  TRS:
  {  quot(x, 0(), s z) -> s quot(x, plus(z, s 0()), s z),
   quot(0(), s y, s z) -> 0(),
     quot(s x, s y, z) -> quot(x, y, z),
          plus(0(), y) -> y,
          plus(s x, y) -> s plus(x, y)}
  UR:
   {plus(0(), y) -> y,
    plus(s x, y) -> s plus(x, y)}
   EDG:
    {(quot#(s x, s y, z) -> quot#(x, y, 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) -> plus#(z, s 0()))
     (quot#(s x, s y, z) -> quot#(x, y, z), quot#(x, 0(), s z) -> quot#(x, plus(z, s 0()), s z))
     (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
     (quot#(x, 0(), s z) -> quot#(x, plus(z, s 0()), s z), quot#(x, 0(), s z) -> quot#(x, plus(z, s 0()), s z))
     (quot#(x, 0(), s z) -> quot#(x, plus(z, s 0()), s z), quot#(x, 0(), s z) -> plus#(z, s 0()))
     (quot#(x, 0(), s z) -> quot#(x, plus(z, s 0()), s z), quot#(s x, s y, z) -> quot#(x, y, z))
     (quot#(x, 0(), s z) -> plus#(z, s 0()), plus#(s x, y) -> plus#(x, y))}
    STATUS:
     arrows: 0.500000
     SCCS (2):
      Scc:
       {quot#(x, 0(), s z) -> quot#(x, plus(z, s 0()), s z),
        quot#(s x, s y, z) -> quot#(x, y, z)}
      Scc:
       {plus#(s x, y) -> plus#(x, y)}
      
      SCC (2):
       Strict:
        {quot#(x, 0(), s z) -> quot#(x, plus(z, s 0()), s z),
         quot#(s x, s y, z) -> quot#(x, y, z)}
       Weak:
       {  quot(x, 0(), s z) -> s quot(x, plus(z, s 0()), s z),
        quot(0(), s y, s z) -> 0(),
          quot(s x, s y, z) -> quot(x, y, z),
               plus(0(), y) -> y,
               plus(s x, y) -> s plus(x, y)}
       Open
      
      SCC (1):
       Strict:
        {plus#(s x, y) -> plus#(x, y)}
       Weak:
       {  quot(x, 0(), s z) -> s quot(x, plus(z, s 0()), s z),
        quot(0(), s y, s z) -> 0(),
          quot(s x, s y, z) -> quot(x, y, z),
               plus(0(), y) -> y,
               plus(s x, y) -> s plus(x, y)}
       Open