MAYBE
Time: 0.005460
TRS:
 {       plus(0(), Y) -> Y,
         plus(s X, Y) -> s plus(X, Y),
          min(X, 0()) -> X,
        min(s X, s Y) -> min(X, Y),
  min(min(X, Y), Z()) -> min(X, plus(Y, Z())),
       quot(0(), s Y) -> 0(),
       quot(s X, s Y) -> s quot(min(X, Y), s Y)}
 DP:
  DP:
   {       plus#(s X, Y) -> plus#(X, Y),
          min#(s X, s Y) -> min#(X, Y),
    min#(min(X, Y), Z()) -> plus#(Y, Z()),
    min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())),
         quot#(s X, s Y) -> min#(X, Y),
         quot#(s X, s Y) -> quot#(min(X, Y), s Y)}
  TRS:
  {       plus(0(), Y) -> Y,
          plus(s X, Y) -> s plus(X, Y),
           min(X, 0()) -> X,
         min(s X, s Y) -> min(X, Y),
   min(min(X, Y), Z()) -> min(X, plus(Y, Z())),
        quot(0(), s Y) -> 0(),
        quot(s X, s Y) -> s quot(min(X, Y), s Y)}
  EDG:
   {(min#(s X, s Y) -> min#(X, Y), min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())))
    (min#(s X, s Y) -> min#(X, Y), min#(min(X, Y), Z()) -> plus#(Y, Z()))
    (min#(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))
    (min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())), min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())))
    (min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())), min#(min(X, Y), Z()) -> plus#(Y, Z()))
    (min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())), min#(s X, s Y) -> min#(X, Y))
    (min#(min(X, Y), Z()) -> plus#(Y, Z()), plus#(s X, Y) -> plus#(X, Y))
    (quot#(s X, s Y) -> min#(X, Y), min#(s X, s Y) -> min#(X, Y))
    (quot#(s X, s Y) -> min#(X, Y), min#(min(X, Y), Z()) -> plus#(Y, Z()))
    (quot#(s X, s Y) -> min#(X, Y), min#(min(X, Y), Z()) -> min#(X, plus(Y, Z())))
    (plus#(s X, Y) -> plus#(X, Y), plus#(s X, Y) -> plus#(X, Y))}
   STATUS:
    arrows: 0.638889
    SCCS (3):
     Scc:
      {quot#(s X, s Y) -> quot#(min(X, Y), s Y)}
     Scc:
      {      min#(s X, s Y) -> min#(X, Y),
       min#(min(X, Y), Z()) -> min#(X, plus(Y, Z()))}
     Scc:
      {plus#(s X, Y) -> plus#(X, Y)}
     
     SCC (1):
      Strict:
       {quot#(s X, s Y) -> quot#(min(X, Y), s Y)}
      Weak:
      {       plus(0(), Y) -> Y,
              plus(s X, Y) -> s plus(X, Y),
               min(X, 0()) -> X,
             min(s X, s Y) -> min(X, Y),
       min(min(X, Y), Z()) -> min(X, plus(Y, Z())),
            quot(0(), s Y) -> 0(),
            quot(s X, s Y) -> s quot(min(X, Y), s Y)}
      Open
     
     SCC (2):
      Strict:
       {      min#(s X, s Y) -> min#(X, Y),
        min#(min(X, Y), Z()) -> min#(X, plus(Y, Z()))}
      Weak:
      {       plus(0(), Y) -> Y,
              plus(s X, Y) -> s plus(X, Y),
               min(X, 0()) -> X,
             min(s X, s Y) -> min(X, Y),
       min(min(X, Y), Z()) -> min(X, plus(Y, Z())),
            quot(0(), s Y) -> 0(),
            quot(s X, s Y) -> s quot(min(X, Y), s Y)}
      Open
     
     SCC (1):
      Strict:
       {plus#(s X, Y) -> plus#(X, Y)}
      Weak:
      {       plus(0(), Y) -> Y,
              plus(s X, Y) -> s plus(X, Y),
               min(X, 0()) -> X,
             min(s X, s Y) -> min(X, Y),
       min(min(X, Y), Z()) -> min(X, plus(Y, Z())),
            quot(0(), s Y) -> 0(),
            quot(s X, s Y) -> s quot(min(X, Y), s Y)}
      Open