MAYBE
Time: 0.001211
TRS:
 {        minus(x, 0()) -> x,
  minus(minus(x, y), z) -> minus(x, plus(y, z)),
        minus(s x, s y) -> minus(x, y),
         quot(0(), s y) -> 0(),
         quot(s x, s y) -> s quot(minus(x, y), s y),
           plus(0(), y) -> y,
           plus(s x, y) -> s plus(x, y)}
 DP:
  DP:
   {minus#(minus(x, y), z) -> minus#(x, plus(y, z)),
    minus#(minus(x, y), z) -> plus#(y, z),
          minus#(s x, s y) -> minus#(x, y),
           quot#(s x, s y) -> minus#(x, y),
           quot#(s x, s y) -> quot#(minus(x, y), s y),
             plus#(s x, y) -> plus#(x, y)}
  TRS:
  {        minus(x, 0()) -> x,
   minus(minus(x, y), z) -> minus(x, plus(y, z)),
         minus(s x, s y) -> minus(x, y),
          quot(0(), s y) -> 0(),
          quot(s x, s y) -> s quot(minus(x, y), s y),
            plus(0(), y) -> y,
            plus(s x, y) -> s plus(x, y)}
  UR:
   {        minus(x, 0()) -> x,
    minus(minus(x, y), z) -> minus(x, plus(y, z)),
          minus(s x, s y) -> minus(x, y),
             plus(0(), y) -> y,
             plus(s x, y) -> s plus(x, y),
                  a(w, v) -> w,
                  a(w, v) -> v}
   EDG:
    {(minus#(minus(x, y), z) -> plus#(y, z), plus#(s x, y) -> plus#(x, y))
     (quot#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (quot#(s x, s y) -> minus#(x, y), minus#(minus(x, y), z) -> plus#(y, z))
     (quot#(s x, s y) -> minus#(x, y), minus#(minus(x, y), z) -> minus#(x, plus(y, z)))
     (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> quot#(minus(x, y), s y))
     (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> minus#(x, y))
     (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
     (minus#(s x, s y) -> minus#(x, y), minus#(minus(x, y), z) -> minus#(x, plus(y, z)))
     (minus#(s x, s y) -> minus#(x, y), minus#(minus(x, y), z) -> plus#(y, z))
     (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (minus#(minus(x, y), z) -> minus#(x, plus(y, z)), minus#(minus(x, y), z) -> minus#(x, plus(y, z)))
     (minus#(minus(x, y), z) -> minus#(x, plus(y, z)), minus#(minus(x, y), z) -> plus#(y, z))
     (minus#(minus(x, y), z) -> minus#(x, plus(y, z)), minus#(s x, s y) -> minus#(x, y))}
    STATUS:
     arrows: 0.638889
     SCCS (3):
      Scc:
       {quot#(s x, s y) -> quot#(minus(x, y), s y)}
      Scc:
       {minus#(minus(x, y), z) -> minus#(x, plus(y, z)),
              minus#(s x, s y) -> minus#(x, y)}
      Scc:
       {plus#(s x, y) -> plus#(x, y)}
      
      SCC (1):
       Strict:
        {quot#(s x, s y) -> quot#(minus(x, y), s y)}
       Weak:
       {        minus(x, 0()) -> x,
        minus(minus(x, y), z) -> minus(x, plus(y, z)),
              minus(s x, s y) -> minus(x, y),
               quot(0(), s y) -> 0(),
               quot(s x, s y) -> s quot(minus(x, y), s y),
                 plus(0(), y) -> y,
                 plus(s x, y) -> s plus(x, y)}
       Open
      
      SCC (2):
       Strict:
        {minus#(minus(x, y), z) -> minus#(x, plus(y, z)),
               minus#(s x, s y) -> minus#(x, y)}
       Weak:
       {        minus(x, 0()) -> x,
        minus(minus(x, y), z) -> minus(x, plus(y, z)),
              minus(s x, s y) -> minus(x, y),
               quot(0(), s y) -> 0(),
               quot(s x, s y) -> s quot(minus(x, y), s y),
                 plus(0(), y) -> y,
                 plus(s x, y) -> s plus(x, y)}
       Open
      
      SCC (1):
       Strict:
        {plus#(s x, y) -> plus#(x, y)}
       Weak:
       {        minus(x, 0()) -> x,
        minus(minus(x, y), z) -> minus(x, plus(y, z)),
              minus(s x, s y) -> minus(x, y),
               quot(0(), s y) -> 0(),
               quot(s x, s y) -> s quot(minus(x, y), s y),
                 plus(0(), y) -> y,
                 plus(s x, y) -> s plus(x, y)}
       Open