MAYBE
Time: 13.495874
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:
  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 -> 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())))}
  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())))}
  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, *(x, y)), +#(s x, 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, 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))}
   STATUS:
    arrows: 0.875740
    SCCS (6):
     Scc:
      {min#(s x, s y) -> min#(x, y)}
     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:
      {max#(s x, s y) -> max#(x, y)}
     Scc:
      {+#(s x, y) -> +#(x, y)}
     
     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)),
               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())))}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [min](x0, x1) = x0 + x1 + 1,
        
        [max](x0, x1) = x0 + x1 + 1,
        
        [+](x0, x1) = 0,
        
        [-](x0, x1) = x0 + 1,
        
        [*](x0, x1) = x0 + 1,
        
        [s](x0) = x0 + 1,
        
        [f](x0) = 0,
        
        [0] = 1,
        
        [min#](x0, x1) = x0 + 1
       Strict:
        min#(s x, s y) -> min#(x, y)
        2 + 0y + 1x >= 1 + 0y + 1x
       Weak:
        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())))
        0 + 0x >= 0 + 0x
        *(x, s y) -> +(x, *(x, y))
        2 + 1y + 0x >= 0 + 0y + 0x
        *(x, 0()) -> 0()
        2 + 0x >= 1
        -(s x, s y) -> -(x, y)
        2 + 1y + 0x >= 1 + 1y + 0x
        -(x, 0()) -> x
        2 + 0x >= 1x
        +(s x, y) -> s +(x, y)
        0 + 0y + 0x >= 1 + 0y + 0x
        +(0(), y) -> y
        0 + 0y >= 1y
        max(s x, s y) -> s max(x, y)
        3 + 1y + 1x >= 2 + 1y + 1x
        max(0(), y) -> y
        2 + 1y >= 1y
        max(x, 0()) -> x
        2 + 1x >= 1x
        min(s x, s y) -> s min(x, y)
        3 + 1y + 1x >= 2 + 1y + 1x
        min(0(), y) -> 0()
        2 + 1y >= 1
        min(x, 0()) -> 0()
        2 + 1x >= 1
      Qed
    SCC (1):
     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 (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)),
              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())))}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [min](x0, x1) = x0 + x1 + 1,
       
       [max](x0, x1) = x0 + x1 + 1,
       
       [+](x0, x1) = x0 + 1,
       
       [-](x0, x1) = x0 + 1,
       
       [*](x0, x1) = x0 + 1,
       
       [s](x0) = x0 + 1,
       
       [f](x0) = 0,
       
       [0] = 1,
       
       [*#](x0, x1) = x0
      Strict:
       *#(x, s y) -> *#(x, y)
       1 + 1y + 0x >= 0 + 1y + 0x
      Weak:
       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())))
       0 + 0x >= 0 + 0x
       *(x, s y) -> +(x, *(x, y))
       2 + 1y + 0x >= 1 + 0y + 1x
       *(x, 0()) -> 0()
       2 + 0x >= 1
       -(s x, s y) -> -(x, y)
       2 + 1y + 0x >= 1 + 1y + 0x
       -(x, 0()) -> x
       2 + 0x >= 1x
       +(s x, y) -> s +(x, y)
       2 + 0y + 1x >= 2 + 0y + 1x
       +(0(), y) -> y
       2 + 0y >= 1y
       max(s x, s y) -> s max(x, y)
       3 + 1y + 1x >= 2 + 1y + 1x
       max(0(), y) -> y
       2 + 1y >= 1y
       max(x, 0()) -> x
       2 + 1x >= 1x
       min(s x, s y) -> s min(x, y)
       3 + 1y + 1x >= 2 + 1y + 1x
       min(0(), y) -> 0()
       2 + 1y >= 1
       min(x, 0()) -> 0()
       2 + 1x >= 1
     Qed
    
    
    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)),
              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())))}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [min](x0, x1) = x0 + x1 + 1,
       
       [max](x0, x1) = x0 + x1 + 1,
       
       [+](x0, x1) = 0,
       
       [-](x0, x1) = x0 + 1,
       
       [*](x0, x1) = x0 + 1,
       
       [s](x0) = x0 + 1,
       
       [f](x0) = 0,
       
       [0] = 1,
       
       [-#](x0, x1) = x0 + 1
      Strict:
       -#(s x, s y) -> -#(x, y)
       2 + 0y + 1x >= 1 + 0y + 1x
      Weak:
       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())))
       0 + 0x >= 0 + 0x
       *(x, s y) -> +(x, *(x, y))
       2 + 1y + 0x >= 0 + 0y + 0x
       *(x, 0()) -> 0()
       2 + 0x >= 1
       -(s x, s y) -> -(x, y)
       2 + 1y + 0x >= 1 + 1y + 0x
       -(x, 0()) -> x
       2 + 0x >= 1x
       +(s x, y) -> s +(x, y)
       0 + 0y + 0x >= 1 + 0y + 0x
       +(0(), y) -> y
       0 + 0y >= 1y
       max(s x, s y) -> s max(x, y)
       3 + 1y + 1x >= 2 + 1y + 1x
       max(0(), y) -> y
       2 + 1y >= 1y
       max(x, 0()) -> x
       2 + 1x >= 1x
       min(s x, s y) -> s min(x, y)
       3 + 1y + 1x >= 2 + 1y + 1x
       min(0(), y) -> 0()
       2 + 1y >= 1
       min(x, 0()) -> 0()
       2 + 1x >= 1
     Qed
   
   
   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)),
             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())))}
    POLY:
     Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
     Interpretation:
      [min](x0, x1) = x0 + x1 + 1,
      
      [max](x0, x1) = x0 + x1 + 1,
      
      [+](x0, x1) = 0,
      
      [-](x0, x1) = x0 + 1,
      
      [*](x0, x1) = x0 + 1,
      
      [s](x0) = x0 + 1,
      
      [f](x0) = 0,
      
      [0] = 1,
      
      [max#](x0, x1) = x0 + 1
     Strict:
      max#(s x, s y) -> max#(x, y)
      2 + 0y + 1x >= 1 + 0y + 1x
     Weak:
      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())))
      0 + 0x >= 0 + 0x
      *(x, s y) -> +(x, *(x, y))
      2 + 1y + 0x >= 0 + 0y + 0x
      *(x, 0()) -> 0()
      2 + 0x >= 1
      -(s x, s y) -> -(x, y)
      2 + 1y + 0x >= 1 + 1y + 0x
      -(x, 0()) -> x
      2 + 0x >= 1x
      +(s x, y) -> s +(x, y)
      0 + 0y + 0x >= 1 + 0y + 0x
      +(0(), y) -> y
      0 + 0y >= 1y
      max(s x, s y) -> s max(x, y)
      3 + 1y + 1x >= 2 + 1y + 1x
      max(0(), y) -> y
      2 + 1y >= 1y
      max(x, 0()) -> x
      2 + 1x >= 1x
      min(s x, s y) -> s min(x, y)
      3 + 1y + 1x >= 2 + 1y + 1x
      min(0(), y) -> 0()
      2 + 1y >= 1
      min(x, 0()) -> 0()
      2 + 1x >= 1
    Qed
   
   
   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)),
             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())))}
    POLY:
     Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
     Interpretation:
      [min](x0, x1) = x0 + x1 + 1,
      
      [max](x0, x1) = x0 + x1 + 1,
      
      [+](x0, x1) = x0 + 1,
      
      [-](x0, x1) = x0 + 1,
      
      [*](x0, x1) = x0 + 1,
      
      [s](x0) = x0 + 1,
      
      [f](x0) = 0,
      
      [0] = 1,
      
      [+#](x0, x1) = x0
     Strict:
      +#(s x, y) -> +#(x, y)
      1 + 0y + 1x >= 0 + 0y + 1x
     Weak:
      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())))
      0 + 0x >= 0 + 0x
      *(x, s y) -> +(x, *(x, y))
      2 + 1y + 0x >= 1 + 0y + 1x
      *(x, 0()) -> 0()
      2 + 0x >= 1
      -(s x, s y) -> -(x, y)
      2 + 1y + 0x >= 1 + 1y + 0x
      -(x, 0()) -> x
      2 + 0x >= 1x
      +(s x, y) -> s +(x, y)
      2 + 0y + 1x >= 2 + 0y + 1x
      +(0(), y) -> y
      2 + 0y >= 1y
      max(s x, s y) -> s max(x, y)
      3 + 1y + 1x >= 2 + 1y + 1x
      max(0(), y) -> y
      2 + 1y >= 1y
      max(x, 0()) -> x
      2 + 1x >= 1x
      min(s x, s y) -> s min(x, y)
      3 + 1y + 1x >= 2 + 1y + 1x
      min(0(), y) -> 0()
      2 + 1y >= 1
      min(x, 0()) -> 0()
      2 + 1x >= 1
    Qed