MAYBE
Time: 0.044591
TRS:
 {  -(x, 0()) -> x,
  -(s x, s y) -> -(x, y),
    +(0(), y) -> y,
    +(s x, y) -> s +(x, y),
    *(x, 0()) -> 0(),
    *(x, s y) -> +(x, *(x, y)),
    f(s x, y) -> f(-(*(s x, s y), s *(s x, y)), *(y, y))}
 DP:
  DP:
   {-#(s x, s y) -> -#(x, y),
      +#(s x, y) -> +#(x, y),
      *#(x, s y) -> +#(x, *(x, y)),
      *#(x, s y) -> *#(x, y),
      f#(s x, y) -> -#(*(s x, s y), s *(s x, y)),
      f#(s x, y) -> *#(y, y),
      f#(s x, y) -> *#(s x, y),
      f#(s x, y) -> *#(s x, s y),
      f#(s x, y) -> f#(-(*(s x, s y), s *(s x, y)), *(y, y))}
  TRS:
  {  -(x, 0()) -> x,
   -(s x, s y) -> -(x, y),
     +(0(), y) -> y,
     +(s x, y) -> s +(x, y),
     *(x, 0()) -> 0(),
     *(x, s y) -> +(x, *(x, y)),
     f(s x, y) -> f(-(*(s x, s y), s *(s x, y)), *(y, y))}
  UR:
   {  -(x, 0()) -> x,
    -(s x, s y) -> -(x, y),
      +(0(), y) -> y,
      +(s x, y) -> s +(x, y),
      *(x, 0()) -> 0(),
      *(x, s y) -> +(x, *(x, y)),
        a(z, w) -> z,
        a(z, w) -> w}
   EDG:
    {(-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y))
     (*#(x, s y) -> *#(x, y), *#(x, s y) -> *#(x, y))
     (*#(x, s y) -> *#(x, y), *#(x, s y) -> +#(x, *(x, y)))
     (f#(s x, y) -> -#(*(s x, s y), s *(s x, y)), -#(s x, s y) -> -#(x, y))
     (f#(s x, y) -> f#(-(*(s x, s y), s *(s x, y)), *(y, y)), f#(s x, y) -> f#(-(*(s x, s y), s *(s x, y)), *(y, y)))
     (f#(s x, y) -> f#(-(*(s x, s y), s *(s x, y)), *(y, y)), f#(s x, y) -> *#(s x, s y))
     (f#(s x, y) -> f#(-(*(s x, s y), s *(s x, y)), *(y, y)), f#(s x, y) -> *#(s x, y))
     (f#(s x, y) -> f#(-(*(s x, s y), s *(s x, y)), *(y, y)), f#(s x, y) -> *#(y, y))
     (f#(s x, y) -> f#(-(*(s x, s y), s *(s x, y)), *(y, y)), f#(s x, y) -> -#(*(s x, s y), s *(s x, y)))
     (f#(s x, y) -> *#(s x, s y), *#(x, s y) -> +#(x, *(x, y)))
     (f#(s x, y) -> *#(s x, s y), *#(x, s y) -> *#(x, y))
     (*#(x, s y) -> +#(x, *(x, y)), +#(s x, y) -> +#(x, y))
     (f#(s x, y) -> *#(y, y), *#(x, s y) -> +#(x, *(x, y)))
     (f#(s x, y) -> *#(y, y), *#(x, s y) -> *#(x, y))
     (+#(s x, y) -> +#(x, y), +#(s x, y) -> +#(x, y))
     (f#(s x, y) -> *#(s x, y), *#(x, s y) -> +#(x, *(x, y)))
     (f#(s x, y) -> *#(s x, y), *#(x, s y) -> *#(x, y))}
    STATUS:
     arrows: 0.790123
     SCCS (4):
      Scc:
       {f#(s x, y) -> f#(-(*(s x, s y), s *(s x, y)), *(y, y))}
      Scc:
       {-#(s x, s y) -> -#(x, y)}
      Scc:
       {*#(x, s y) -> *#(x, y)}
      Scc:
       {+#(s x, y) -> +#(x, y)}
      
      SCC (1):
       Strict:
        {f#(s x, y) -> f#(-(*(s x, s y), s *(s x, y)), *(y, y))}
       Weak:
       {  -(x, 0()) -> x,
        -(s x, s y) -> -(x, y),
          +(0(), y) -> y,
          +(s x, y) -> s +(x, y),
          *(x, 0()) -> 0(),
          *(x, s y) -> +(x, *(x, y)),
          f(s x, y) -> f(-(*(s x, s y), s *(s x, y)), *(y, y))}
       Fail
      
      
      
      SCC (1):
       Strict:
        {-#(s x, s y) -> -#(x, y)}
       Weak:
       {  -(x, 0()) -> x,
        -(s x, s y) -> -(x, y),
          +(0(), y) -> y,
          +(s x, y) -> s +(x, y),
          *(x, 0()) -> 0(),
          *(x, s y) -> +(x, *(x, y)),
          f(s x, y) -> f(-(*(s x, s y), s *(s x, y)), *(y, y))}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [-](x0, x1) = x0 + 1,
         
         [+](x0, x1) = x0 + 1,
         
         [*](x0, x1) = x0 + 1,
         
         [f](x0, x1) = x0,
         
         [s](x0) = x0 + 1,
         
         [0] = 1,
         
         [-#](x0, x1) = x0
        Strict:
         -#(s x, s y) -> -#(x, y)
         1 + 0x + 1y >= 0 + 0x + 1y
        Weak:
         f(s x, y) -> f(-(*(s x, s y), s *(s x, y)), *(y, y))
         1 + 1x + 0y >= 3 + 0x + 1y
         *(x, s y) -> +(x, *(x, y))
         2 + 0x + 1y >= 1 + 1x + 0y
         *(x, 0()) -> 0()
         2 + 0x >= 1
         +(s x, y) -> s +(x, y)
         2 + 1x + 0y >= 2 + 1x + 0y
         +(0(), y) -> y
         2 + 0y >= 1y
         -(s x, s y) -> -(x, y)
         2 + 0x + 1y >= 1 + 0x + 1y
         -(x, 0()) -> x
         2 + 0x >= 1x
       Qed
     
     SCC (1):
      Strict:
       {*#(x, s y) -> *#(x, y)}
      Weak:
      {  -(x, 0()) -> x,
       -(s x, s y) -> -(x, y),
         +(0(), y) -> y,
         +(s x, y) -> s +(x, y),
         *(x, 0()) -> 0(),
         *(x, s y) -> +(x, *(x, y)),
         f(s x, y) -> f(-(*(s x, s y), s *(s x, y)), *(y, y))}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [-](x0, x1) = x0 + 1,
        
        [+](x0, x1) = x0 + 1,
        
        [*](x0, x1) = x0 + 1,
        
        [f](x0, x1) = x0,
        
        [s](x0) = x0 + 1,
        
        [0] = 1,
        
        [*#](x0, x1) = x0
       Strict:
        *#(x, s y) -> *#(x, y)
        1 + 0x + 1y >= 0 + 0x + 1y
       Weak:
        f(s x, y) -> f(-(*(s x, s y), s *(s x, y)), *(y, y))
        1 + 1x + 0y >= 3 + 0x + 1y
        *(x, s y) -> +(x, *(x, y))
        2 + 0x + 1y >= 1 + 1x + 0y
        *(x, 0()) -> 0()
        2 + 0x >= 1
        +(s x, y) -> s +(x, y)
        2 + 1x + 0y >= 2 + 1x + 0y
        +(0(), y) -> y
        2 + 0y >= 1y
        -(s x, s y) -> -(x, y)
        2 + 0x + 1y >= 1 + 0x + 1y
        -(x, 0()) -> x
        2 + 0x >= 1x
      Qed
     
     SCC (1):
      Strict:
       {+#(s x, y) -> +#(x, y)}
      Weak:
      {  -(x, 0()) -> x,
       -(s x, s y) -> -(x, y),
         +(0(), y) -> y,
         +(s x, y) -> s +(x, y),
         *(x, 0()) -> 0(),
         *(x, s y) -> +(x, *(x, y)),
         f(s x, y) -> f(-(*(s x, s y), s *(s x, y)), *(y, y))}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [-](x0, x1) = x0 + 1,
        
        [+](x0, x1) = x0 + 1,
        
        [*](x0, x1) = x0 + 1,
        
        [f](x0, x1) = x0,
        
        [s](x0) = x0 + 1,
        
        [0] = 1,
        
        [+#](x0, x1) = x0
       Strict:
        +#(s x, y) -> +#(x, y)
        1 + 1x + 0y >= 0 + 1x + 0y
       Weak:
        f(s x, y) -> f(-(*(s x, s y), s *(s x, y)), *(y, y))
        1 + 1x + 0y >= 3 + 0x + 1y
        *(x, s y) -> +(x, *(x, y))
        2 + 0x + 1y >= 1 + 1x + 0y
        *(x, 0()) -> 0()
        2 + 0x >= 1
        +(s x, y) -> s +(x, y)
        2 + 1x + 0y >= 2 + 1x + 0y
        +(0(), y) -> y
        2 + 0y >= 1y
        -(s x, s y) -> -(x, y)
        2 + 0x + 1y >= 1 + 0x + 1y
        -(x, 0()) -> x
        2 + 0x >= 1x
      Qed