MAYBE
Time: 0.001910
TRS:
 {    minus(x, x) -> 0(),
    minus(x, 0()) -> x,
    minus(0(), x) -> 0(),
  minus(s x, s y) -> minus(x, y),
    div(0(), s y) -> 0(),
    div(s x, s y) -> s div(minus(x, y), s y),
     f(x, 0(), b) -> x,
     f(x, s y, b) -> div(f(x, minus(s y, s 0()), b), b)}
 DP:
  DP:
   {minus#(s x, s y) -> minus#(x, y),
      div#(s x, s y) -> minus#(x, y),
      div#(s x, s y) -> div#(minus(x, y), s y),
       f#(x, s y, b) -> minus#(s y, s 0()),
       f#(x, s y, b) -> div#(f(x, minus(s y, s 0()), b), b),
       f#(x, s y, b) -> f#(x, minus(s y, s 0()), b)}
  TRS:
  {    minus(x, x) -> 0(),
     minus(x, 0()) -> x,
     minus(0(), x) -> 0(),
   minus(s x, s y) -> minus(x, y),
     div(0(), s y) -> 0(),
     div(s x, s y) -> s div(minus(x, y), s y),
      f(x, 0(), b) -> x,
      f(x, s y, b) -> div(f(x, minus(s y, s 0()), b), b)}
  UR:
   {    minus(x, x) -> 0(),
      minus(x, 0()) -> x,
      minus(0(), x) -> 0(),
    minus(s x, s y) -> minus(x, y),
      div(0(), s y) -> 0(),
      div(s x, s y) -> s div(minus(x, y), s y),
       f(x, 0(), b) -> x,
       f(x, s y, b) -> div(f(x, minus(s y, s 0()), b), b),
            a(z, w) -> z,
            a(z, w) -> w}
   EDG:
    {(div#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (div#(s x, s y) -> div#(minus(x, y), s y), div#(s x, s y) -> div#(minus(x, y), s y))
     (div#(s x, s y) -> div#(minus(x, y), s y), div#(s x, s y) -> minus#(x, y))
     (f#(x, s y, b) -> f#(x, minus(s y, s 0()), b), f#(x, s y, b) -> f#(x, minus(s y, s 0()), b))
     (f#(x, s y, b) -> f#(x, minus(s y, s 0()), b), f#(x, s y, b) -> div#(f(x, minus(s y, s 0()), b), b))
     (f#(x, s y, b) -> f#(x, minus(s y, s 0()), b), f#(x, s y, b) -> minus#(s y, s 0()))
     (f#(x, s y, b) -> div#(f(x, minus(s y, s 0()), b), b), div#(s x, s y) -> minus#(x, y))
     (f#(x, s y, b) -> div#(f(x, minus(s y, s 0()), b), b), div#(s x, s y) -> div#(minus(x, y), s y))
     (f#(x, s y, b) -> minus#(s y, s 0()), minus#(s x, s y) -> minus#(x, y))
     (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))}
    STATUS:
     arrows: 0.722222
     SCCS (3):
      Scc:
       {f#(x, s y, b) -> f#(x, minus(s y, s 0()), b)}
      Scc:
       {div#(s x, s y) -> div#(minus(x, y), s y)}
      Scc:
       {minus#(s x, s y) -> minus#(x, y)}
      
      SCC (1):
       Strict:
        {f#(x, s y, b) -> f#(x, minus(s y, s 0()), b)}
       Weak:
       {    minus(x, x) -> 0(),
          minus(x, 0()) -> x,
          minus(0(), x) -> 0(),
        minus(s x, s y) -> minus(x, y),
          div(0(), s y) -> 0(),
          div(s x, s y) -> s div(minus(x, y), s y),
           f(x, 0(), b) -> x,
           f(x, s y, b) -> div(f(x, minus(s y, s 0()), b), b)}
       Open
      
      SCC (1):
       Strict:
        {div#(s x, s y) -> div#(minus(x, y), s y)}
       Weak:
       {    minus(x, x) -> 0(),
          minus(x, 0()) -> x,
          minus(0(), x) -> 0(),
        minus(s x, s y) -> minus(x, y),
          div(0(), s y) -> 0(),
          div(s x, s y) -> s div(minus(x, y), s y),
           f(x, 0(), b) -> x,
           f(x, s y, b) -> div(f(x, minus(s y, s 0()), b), b)}
       Open
      
      
      SCC (1):
       Strict:
        {minus#(s x, s y) -> minus#(x, y)}
       Weak:
       {    minus(x, x) -> 0(),
          minus(x, 0()) -> x,
          minus(0(), x) -> 0(),
        minus(s x, s y) -> minus(x, y),
          div(0(), s y) -> 0(),
          div(s x, s y) -> s div(minus(x, y), s y),
           f(x, 0(), b) -> x,
           f(x, s y, b) -> div(f(x, minus(s y, s 0()), b), b)}
       Open