MAYBE
TRS:
 {      -(x, 0()) -> x,
    -(s(x), s(y)) -> -(x, y),
      min(x, 0()) -> 0(),
      min(0(), y) -> 0(),
  min(s(x), s(y)) -> s(min(x, y)),
       twice(0()) -> 0(),
      twice(s(x)) -> s(s(twice(x))),
    f(s(x), s(y)) -> f(-(x, min(x, y)), s(twice(min(x, y)))),
    f(s(x), s(y)) -> f(-(y, min(x, y)), s(twice(min(x, y))))}
 DP:
  Strict:
   {  -#(s(x), s(y)) -> -#(x, y),
    min#(s(x), s(y)) -> min#(x, y),
        twice#(s(x)) -> twice#(x),
      f#(s(x), s(y)) -> -#(x, min(x, y)),
      f#(s(x), s(y)) -> -#(y, min(x, y)),
      f#(s(x), s(y)) -> min#(x, y),
      f#(s(x), s(y)) -> twice#(min(x, y)),
      f#(s(x), s(y)) -> f#(-(x, min(x, y)), s(twice(min(x, y)))),
      f#(s(x), s(y)) -> f#(-(y, min(x, y)), s(twice(min(x, y))))}
  Weak:
  {      -(x, 0()) -> x,
     -(s(x), s(y)) -> -(x, y),
       min(x, 0()) -> 0(),
       min(0(), y) -> 0(),
   min(s(x), s(y)) -> s(min(x, y)),
        twice(0()) -> 0(),
       twice(s(x)) -> s(s(twice(x))),
     f(s(x), s(y)) -> f(-(x, min(x, y)), s(twice(min(x, y)))),
     f(s(x), s(y)) -> f(-(y, min(x, y)), s(twice(min(x, y))))}
  EDG:
   {(min#(s(x), s(y)) -> min#(x, y), min#(s(x), s(y)) -> min#(x, y))
    (twice#(s(x)) -> twice#(x), twice#(s(x)) -> twice#(x))
    (f#(s(x), s(y)) -> f#(-(y, min(x, y)), s(twice(min(x, y)))), f#(s(x), s(y)) -> f#(-(y, min(x, y)), s(twice(min(x, y)))))
    (f#(s(x), s(y)) -> f#(-(y, min(x, y)), s(twice(min(x, y)))), f#(s(x), s(y)) -> f#(-(x, min(x, y)), s(twice(min(x, y)))))
    (f#(s(x), s(y)) -> f#(-(y, min(x, y)), s(twice(min(x, y)))), f#(s(x), s(y)) -> twice#(min(x, y)))
    (f#(s(x), s(y)) -> f#(-(y, min(x, y)), s(twice(min(x, y)))), f#(s(x), s(y)) -> min#(x, y))
    (f#(s(x), s(y)) -> f#(-(y, min(x, y)), s(twice(min(x, y)))), f#(s(x), s(y)) -> -#(y, min(x, y)))
    (f#(s(x), s(y)) -> f#(-(y, min(x, y)), s(twice(min(x, y)))), f#(s(x), s(y)) -> -#(x, min(x, y)))
    (f#(s(x), s(y)) -> -#(y, min(x, y)), -#(s(x), s(y)) -> -#(x, y))
    (f#(s(x), s(y)) -> twice#(min(x, y)), twice#(s(x)) -> twice#(x))
    (f#(s(x), s(y)) -> -#(x, min(x, y)), -#(s(x), s(y)) -> -#(x, y))
    (f#(s(x), s(y)) -> f#(-(x, min(x, y)), s(twice(min(x, y)))), f#(s(x), s(y)) -> -#(x, min(x, y)))
    (f#(s(x), s(y)) -> f#(-(x, min(x, y)), s(twice(min(x, y)))), f#(s(x), s(y)) -> -#(y, min(x, y)))
    (f#(s(x), s(y)) -> f#(-(x, min(x, y)), s(twice(min(x, y)))), f#(s(x), s(y)) -> min#(x, y))
    (f#(s(x), s(y)) -> f#(-(x, min(x, y)), s(twice(min(x, y)))), f#(s(x), s(y)) -> twice#(min(x, y)))
    (f#(s(x), s(y)) -> f#(-(x, min(x, y)), s(twice(min(x, y)))), f#(s(x), s(y)) -> f#(-(x, min(x, y)), s(twice(min(x, y)))))
    (f#(s(x), s(y)) -> f#(-(x, min(x, y)), s(twice(min(x, y)))), f#(s(x), s(y)) -> f#(-(y, min(x, y)), s(twice(min(x, y)))))
    (f#(s(x), s(y)) -> min#(x, y), min#(s(x), s(y)) -> min#(x, y))
    (-#(s(x), s(y)) -> -#(x, y), -#(s(x), s(y)) -> -#(x, y))}
   SCCS:
    Scc:
     {f#(s(x), s(y)) -> f#(-(x, min(x, y)), s(twice(min(x, y)))),
      f#(s(x), s(y)) -> f#(-(y, min(x, y)), s(twice(min(x, y))))}
    Scc:
     {twice#(s(x)) -> twice#(x)}
    Scc:
     {min#(s(x), s(y)) -> min#(x, y)}
    Scc:
     {-#(s(x), s(y)) -> -#(x, y)}
    SCC:
     Strict:
      {f#(s(x), s(y)) -> f#(-(x, min(x, y)), s(twice(min(x, y)))),
       f#(s(x), s(y)) -> f#(-(y, min(x, y)), s(twice(min(x, y))))}
     Weak:
     {      -(x, 0()) -> x,
        -(s(x), s(y)) -> -(x, y),
          min(x, 0()) -> 0(),
          min(0(), y) -> 0(),
      min(s(x), s(y)) -> s(min(x, y)),
           twice(0()) -> 0(),
          twice(s(x)) -> s(s(twice(x))),
        f(s(x), s(y)) -> f(-(x, min(x, y)), s(twice(min(x, y)))),
        f(s(x), s(y)) -> f(-(y, min(x, y)), s(twice(min(x, y))))}
     Fail
    SCC:
     Strict:
      {twice#(s(x)) -> twice#(x)}
     Weak:
     {      -(x, 0()) -> x,
        -(s(x), s(y)) -> -(x, y),
          min(x, 0()) -> 0(),
          min(0(), y) -> 0(),
      min(s(x), s(y)) -> s(min(x, y)),
           twice(0()) -> 0(),
          twice(s(x)) -> s(s(twice(x))),
        f(s(x), s(y)) -> f(-(x, min(x, y)), s(twice(min(x, y)))),
        f(s(x), s(y)) -> f(-(y, min(x, y)), s(twice(min(x, y))))}
     SPSC:
      Simple Projection:
       pi(twice#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {min#(s(x), s(y)) -> min#(x, y)}
     Weak:
     {      -(x, 0()) -> x,
        -(s(x), s(y)) -> -(x, y),
          min(x, 0()) -> 0(),
          min(0(), y) -> 0(),
      min(s(x), s(y)) -> s(min(x, y)),
           twice(0()) -> 0(),
          twice(s(x)) -> s(s(twice(x))),
        f(s(x), s(y)) -> f(-(x, min(x, y)), s(twice(min(x, y)))),
        f(s(x), s(y)) -> f(-(y, min(x, y)), s(twice(min(x, y))))}
     SPSC:
      Simple Projection:
       pi(min#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {-#(s(x), s(y)) -> -#(x, y)}
     Weak:
     {      -(x, 0()) -> x,
        -(s(x), s(y)) -> -(x, y),
          min(x, 0()) -> 0(),
          min(0(), y) -> 0(),
      min(s(x), s(y)) -> s(min(x, y)),
           twice(0()) -> 0(),
          twice(s(x)) -> s(s(twice(x))),
        f(s(x), s(y)) -> f(-(x, min(x, y)), s(twice(min(x, y)))),
        f(s(x), s(y)) -> f(-(y, min(x, y)), s(twice(min(x, y))))}
     SPSC:
      Simple Projection:
       pi(-#) = 0
      Strict:
       {}
      Qed