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)),
          p(s(x)) -> x,
    f(s(x), s(y)) -> f(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y)))}
 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), s(y)) -> min#(s(x), s(y)),
      f#(s(x), s(y)) -> max#(s(x), s(y)),
      f#(s(x), s(y)) -> -#(min(s(x), s(y)), max(s(x), s(y))),
      f#(s(x), s(y)) -> *#(s(x), s(y)),
      f#(s(x), s(y)) -> f#(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(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)),
           p(s(x)) -> x,
     f(s(x), s(y)) -> f(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y)))}
  EDG:
   {(max#(s(x), s(y)) -> max#(x, y), max#(s(x), s(y)) -> max#(x, y))
    (-#(s(x), s(y)) -> -#(x, y), -#(s(x), s(y)) -> -#(x, y))
    (f#(s(x), s(y)) -> min#(s(x), s(y)), min#(s(x), s(y)) -> min#(x, y))
    (f#(s(x), s(y)) -> *#(s(x), s(y)), *#(x, s(y)) -> *#(x, y))
    (f#(s(x), s(y)) -> *#(s(x), s(y)), *#(x, s(y)) -> +#(x, *(x, y)))
    (f#(s(x), s(y)) -> -#(min(s(x), s(y)), max(s(x), s(y))), -#(s(x), s(y)) -> -#(x, y))
    (f#(s(x), s(y)) -> f#(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y))), f#(s(x), s(y)) -> min#(s(x), s(y)))
    (f#(s(x), s(y)) -> f#(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y))), f#(s(x), s(y)) -> max#(s(x), s(y)))
    (f#(s(x), s(y)) -> f#(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y))), f#(s(x), s(y)) -> -#(min(s(x), s(y)), max(s(x), s(y))))
    (f#(s(x), s(y)) -> f#(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y))), f#(s(x), s(y)) -> *#(s(x), s(y)))
    (f#(s(x), s(y)) -> f#(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y))), f#(s(x), s(y)) -> f#(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y))))
    (*#(x, s(y)) -> +#(x, *(x, y)), +#(s(x), y) -> +#(x, y))
    (f#(s(x), s(y)) -> max#(s(x), s(y)), max#(s(x), s(y)) -> max#(x, y))
    (*#(x, s(y)) -> *#(x, y), *#(x, s(y)) -> +#(x, *(x, y)))
    (*#(x, s(y)) -> *#(x, y), *#(x, s(y)) -> *#(x, y))
    (+#(s(x), y) -> +#(x, y), +#(s(x), y) -> +#(x, y))
    (min#(s(x), s(y)) -> min#(x, y), min#(s(x), s(y)) -> min#(x, y))}
   SCCS:
    Scc:
     {f#(s(x), s(y)) -> f#(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y)))}
    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), s(y)) -> f#(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(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)),
              p(s(x)) -> x,
        f(s(x), s(y)) -> f(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y)))}
     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)),
              p(s(x)) -> x,
        f(s(x), s(y)) -> f(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y)))}
     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)),
              p(s(x)) -> x,
        f(s(x), s(y)) -> f(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y)))}
     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)),
              p(s(x)) -> x,
        f(s(x), s(y)) -> f(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y)))}
     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)),
              p(s(x)) -> x,
        f(s(x), s(y)) -> f(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y)))}
     SPSC:
      Simple Projection:
       pi(max#) = 1
      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)),
              p(s(x)) -> x,
        f(s(x), s(y)) -> f(-(min(s(x), s(y)), max(s(x), s(y))), *(s(x), s(y)))}
     SPSC:
      Simple Projection:
       pi(min#) = 0
      Strict:
       {}
      Qed