MAYBE
Time: 0.001364
TRS:
 {   min(X, 0()) -> X,
   min(s X, s Y) -> min(X, Y),
  quot(0(), s Y) -> 0(),
  quot(s X, s Y) -> s quot(min(X, Y), s Y),
       log s 0() -> 0(),
       log s s X -> s log s quot(X, s s 0())}
 DP:
  DP:
   { min#(s X, s Y) -> min#(X, Y),
    quot#(s X, s Y) -> min#(X, Y),
    quot#(s X, s Y) -> quot#(min(X, Y), s Y),
         log# s s X -> quot#(X, s s 0()),
         log# s s X -> log# s quot(X, s s 0())}
  TRS:
  {   min(X, 0()) -> X,
    min(s X, s Y) -> min(X, Y),
   quot(0(), s Y) -> 0(),
   quot(s X, s Y) -> s quot(min(X, Y), s Y),
        log s 0() -> 0(),
        log s s X -> s log s quot(X, s s 0())}
  UR:
   {   min(X, 0()) -> X,
     min(s X, s Y) -> min(X, Y),
    quot(0(), s Y) -> 0(),
    quot(s X, s Y) -> s quot(min(X, Y), s Y),
           a(x, y) -> x,
           a(x, y) -> y}
   EDG:
    {(quot#(s X, s Y) -> min#(X, Y), min#(s X, s Y) -> min#(X, Y))
     (quot#(s X, s Y) -> quot#(min(X, Y), s Y), quot#(s X, s Y) -> quot#(min(X, Y), s Y))
     (quot#(s X, s Y) -> quot#(min(X, Y), s Y), quot#(s X, s Y) -> min#(X, Y))
     (log# s s X -> log# s quot(X, s s 0()), log# s s X -> quot#(X, s s 0()))
     (log# s s X -> log# s quot(X, s s 0()), log# s s X -> log# s quot(X, s s 0()))
     (log# s s X -> quot#(X, s s 0()), quot#(s X, s Y) -> min#(X, Y))
     (log# s s X -> quot#(X, s s 0()), quot#(s X, s Y) -> quot#(min(X, Y), s Y))
     (min#(s X, s Y) -> min#(X, Y), min#(s X, s Y) -> min#(X, Y))}
    STATUS:
     arrows: 0.680000
     SCCS (3):
      Scc:
       {log# s s X -> log# s quot(X, s s 0())}
      Scc:
       {quot#(s X, s Y) -> quot#(min(X, Y), s Y)}
      Scc:
       {min#(s X, s Y) -> min#(X, Y)}
      
      SCC (1):
       Strict:
        {log# s s X -> log# s quot(X, s s 0())}
       Weak:
       {   min(X, 0()) -> X,
         min(s X, s Y) -> min(X, Y),
        quot(0(), s Y) -> 0(),
        quot(s X, s Y) -> s quot(min(X, Y), s Y),
             log s 0() -> 0(),
             log s s X -> s log s quot(X, s s 0())}
       Open
      
      SCC (1):
       Strict:
        {quot#(s X, s Y) -> quot#(min(X, Y), s Y)}
       Weak:
       {   min(X, 0()) -> X,
         min(s X, s Y) -> min(X, Y),
        quot(0(), s Y) -> 0(),
        quot(s X, s Y) -> s quot(min(X, Y), s Y),
             log s 0() -> 0(),
             log s s X -> s log s quot(X, s s 0())}
       Open
      
      SCC (1):
       Strict:
        {min#(s X, s Y) -> min#(X, Y)}
       Weak:
       {   min(X, 0()) -> X,
         min(s X, s Y) -> min(X, Y),
        quot(0(), s Y) -> 0(),
        quot(s X, s Y) -> s quot(min(X, Y), s Y),
             log s 0() -> 0(),
             log s s X -> s log s quot(X, s s 0())}
       Open