MAYBE
Time: 0.007972
TRS:
 {                         minus(x, 0()) -> x,
                         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(minus(x, s 0()), minus(y, s s z)) -> plus(minus(y, s s z), minus(x, s 0())),
                            plus(0(), y) -> y,
                            plus(s x, y) -> s plus(x, y),
    plus(plus(x, s 0()), plus(y, s s z)) -> plus(plus(y, s s z), plus(x, s 0()))}
 DP:
  DP:
   {                       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#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())),
                              plus#(s x, y) -> plus#(x, y),
      plus#(plus(x, s 0()), plus(y, s s z)) -> plus#(plus(y, s s z), plus(x, s 0()))}
  TRS:
  {                         minus(x, 0()) -> x,
                          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(minus(x, s 0()), minus(y, s s z)) -> plus(minus(y, s s z), minus(x, s 0())),
                             plus(0(), y) -> y,
                             plus(s x, y) -> s plus(x, y),
     plus(plus(x, s 0()), plus(y, s s z)) -> plus(plus(y, s s z), plus(x, s 0()))}
  UR:
   {                         minus(x, 0()) -> x,
                           minus(s x, s y) -> minus(x, y),
    plus(minus(x, s 0()), minus(y, s s z)) -> plus(minus(y, s s z), minus(x, s 0())),
                              plus(0(), y) -> y,
                              plus(s x, y) -> s plus(x, y),
      plus(plus(x, s 0()), plus(y, s s z)) -> plus(plus(y, s s z), plus(x, s 0())),
                                   a(w, v) -> w,
                                   a(w, v) -> v}
   EDG:
    {(quot#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, 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) -> quot#(minus(x, y), s y), quot#(s x, s y) -> minus#(x, y))
     (plus#(plus(x, s 0()), plus(y, s s z)) -> plus#(plus(y, s s z), plus(x, s 0())), plus#(plus(x, s 0()), plus(y, s s z)) -> plus#(plus(y, s s z), plus(x, s 0())))
     (plus#(plus(x, s 0()), plus(y, s s z)) -> plus#(plus(y, s s z), plus(x, s 0())), plus#(s x, y) -> plus#(x, y))
     (plus#(plus(x, s 0()), plus(y, s s z)) -> plus#(plus(y, s s z), plus(x, s 0())), plus#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())))
     (plus#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())), plus#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())))
     (plus#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())), plus#(s x, y) -> plus#(x, y))
     (plus#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())), plus#(plus(x, s 0()), plus(y, s s z)) -> plus#(plus(y, s s z), plus(x, s 0())))
     (plus#(s x, y) -> plus#(x, y), plus#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())))
     (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
     (plus#(s x, y) -> plus#(x, y), plus#(plus(x, s 0()), plus(y, s s z)) -> plus#(plus(y, s s z), plus(x, s 0())))
     (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))}
    EDG:
     {(quot#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, 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) -> quot#(minus(x, y), s y), quot#(s x, s y) -> minus#(x, y))
      (plus#(plus(x, s 0()), plus(y, s s z)) -> plus#(plus(y, s s z), plus(x, s 0())), plus#(plus(x, s 0()), plus(y, s s z)) -> plus#(plus(y, s s z), plus(x, s 0())))
      (plus#(plus(x, s 0()), plus(y, s s z)) -> plus#(plus(y, s s z), plus(x, s 0())), plus#(s x, y) -> plus#(x, y))
      (plus#(plus(x, s 0()), plus(y, s s z)) -> plus#(plus(y, s s z), plus(x, s 0())), plus#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())))
      (plus#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())), plus#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())))
      (plus#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())), plus#(s x, y) -> plus#(x, y))
      (plus#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())), plus#(plus(x, s 0()), plus(y, s s z)) -> plus#(plus(y, s s z), plus(x, s 0())))
      (plus#(s x, y) -> plus#(x, y), plus#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())))
      (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
      (plus#(s x, y) -> plus#(x, y), plus#(plus(x, s 0()), plus(y, s s z)) -> plus#(plus(y, s s z), plus(x, s 0())))
      (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))}
     EDG:
      {(quot#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, 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) -> quot#(minus(x, y), s y), quot#(s x, s y) -> minus#(x, y))
       (plus#(plus(x, s 0()), plus(y, s s z)) -> plus#(plus(y, s s z), plus(x, s 0())), plus#(s x, y) -> plus#(x, y))
       (plus#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())), plus#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())))
       (plus#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())), plus#(s x, y) -> plus#(x, y))
       (plus#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())), plus#(plus(x, s 0()), plus(y, s s z)) -> plus#(plus(y, s s z), plus(x, s 0())))
       (plus#(s x, y) -> plus#(x, y), plus#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())))
       (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
       (plus#(s x, y) -> plus#(x, y), plus#(plus(x, s 0()), plus(y, s s z)) -> plus#(plus(y, s s z), plus(x, s 0())))
       (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))}
      EDG:
       {(quot#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, 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) -> quot#(minus(x, y), s y), quot#(s x, s y) -> minus#(x, y))
        (plus#(plus(x, s 0()), plus(y, s s z)) -> plus#(plus(y, s s z), plus(x, s 0())), plus#(s x, y) -> plus#(x, y))
        (plus#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())), plus#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())))
        (plus#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())), plus#(s x, y) -> plus#(x, y))
        (plus#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())), plus#(plus(x, s 0()), plus(y, s s z)) -> plus#(plus(y, s s z), plus(x, s 0())))
        (plus#(s x, y) -> plus#(x, y), plus#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())))
        (plus#(s x, y) -> plus#(x, y), plus#(s x, y) -> plus#(x, y))
        (plus#(s x, y) -> plus#(x, y), plus#(plus(x, s 0()), plus(y, s s z)) -> plus#(plus(y, s s z), plus(x, s 0())))
        (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))}
       STATUS:
        arrows: 0.694444
        SCCS (3):
         Scc:
          {quot#(s x, s y) -> quot#(minus(x, y), s y)}
         Scc:
          {plus#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())),
                                     plus#(s x, y) -> plus#(x, y),
             plus#(plus(x, s 0()), plus(y, s s z)) -> plus#(plus(y, s s z), plus(x, s 0()))}
         Scc:
          {minus#(s x, s y) -> minus#(x, y)}
         
         SCC (1):
          Strict:
           {quot#(s x, s y) -> quot#(minus(x, y), s y)}
          Weak:
          {                         minus(x, 0()) -> x,
                                  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(minus(x, s 0()), minus(y, s s z)) -> plus(minus(y, s s z), minus(x, s 0())),
                                     plus(0(), y) -> y,
                                     plus(s x, y) -> s plus(x, y),
             plus(plus(x, s 0()), plus(y, s s z)) -> plus(plus(y, s s z), plus(x, s 0()))}
          Open
         SCC (3):
          Strict:
           {plus#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())),
                                      plus#(s x, y) -> plus#(x, y),
              plus#(plus(x, s 0()), plus(y, s s z)) -> plus#(plus(y, s s z), plus(x, s 0()))}
          Weak:
          {                         minus(x, 0()) -> x,
                                  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(minus(x, s 0()), minus(y, s s z)) -> plus(minus(y, s s z), minus(x, s 0())),
                                     plus(0(), y) -> y,
                                     plus(s x, y) -> s plus(x, y),
             plus(plus(x, s 0()), plus(y, s s z)) -> plus(plus(y, s s z), plus(x, s 0()))}
          Open
         
         SCC (1):
          Strict:
           {minus#(s x, s y) -> minus#(x, y)}
          Weak:
          {                         minus(x, 0()) -> x,
                                  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(minus(x, s 0()), minus(y, s s z)) -> plus(minus(y, s s z), minus(x, s 0())),
                                     plus(0(), y) -> y,
                                     plus(s x, y) -> s plus(x, y),
             plus(plus(x, s 0()), plus(y, s s z)) -> plus(plus(y, s s z), plus(x, s 0()))}
          Open