MAYBE
Time: 0.002667
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:
  DP:
   {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))}
  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))}
  UR:
   {  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)),
          a(z, w) -> z,
          a(z, w) -> w}
   EDG:
    {(f#(s x, s y) -> max#(s x, s y), max#(s x, s y) -> max#(x, y))
     (*#(x, s y) -> +#(x, *(x, y)), +#(s x, 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) -> 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)), 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) -> -#(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) -> 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) -> max#(x, y), max#(s x, s y) -> max#(x, y))
     (-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(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))
     (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) -> *#(s x, s y), *#(x, s y) -> +#(x, *(x, y)))
     (f#(s x, s y) -> *#(s x, s y), *#(x, s y) -> *#(x, y))
     (f#(s x, s y) -> min#(s x, s y), min#(s x, s y) -> min#(x, y))}
    STATUS:
     arrows: 0.859504
     SCCS (6):
      Scc:
       {f#(s x, s y) -> f#(-(min(s x, s y), max(s x, s y)), *(s x, s y))}
      Scc:
       {-#(s x, s y) -> -#(x, y)}
      Scc:
       {*#(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 (1):
       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))}
       Open
      
      SCC (1):
       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))}
       Open
      
      SCC (1):
       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))}
       Open
      
      SCC (1):
       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))}
       Open
      
      SCC (1):
       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))}
       Open
      
      SCC (1):
       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))}
       Open