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