MAYBE
Time: 0.173661
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 -> f -(*(s s 0(), s x), s s x)}
 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 -> -#(*(s s 0(), s x), s s x),
          f# s x -> *#(s s 0(), s x),
          f# s x -> f# -(*(s s 0(), s x), s s x)}
  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 -> f -(*(s s 0(), s x), s s x)}
  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:
    {(*#(x, s y) -> +#(x, *(x, y)), +#(s x, y) -> +#(x, y))
     (-#(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 -> f# -(*(s s 0(), s x), s s x), f# s x -> -#(*(s s 0(), s x), s s x))
     (f# s x -> f# -(*(s s 0(), s x), s s x), f# s x -> *#(s s 0(), s x))
     (f# s x -> f# -(*(s s 0(), s x), s s x), f# s x -> f# -(*(s s 0(), s x), s s x))
     (+#(s x, y) -> +#(x, y), +#(s x, y) -> +#(x, y))
     (f# s x -> *#(s s 0(), s x), *#(x, s y) -> +#(x, *(x, y)))
     (f# s x -> *#(s s 0(), s x), *#(x, s y) -> *#(x, y))
     (f# s x -> -#(*(s s 0(), s x), s s x), -#(s x, s y) -> -#(x, y))}
    STATUS:
     arrows: 0.775510
     SCCS (4):
      Scc:
       {f# s x -> f# -(*(s s 0(), s x), s s x)}
      Scc:
       {*#(x, s y) -> *#(x, y)}
      Scc:
       {+#(s x, y) -> +#(x, y)}
      Scc:
       {-#(s x, s y) -> -#(x, y)}
      
      SCC (1):
       Strict:
        {f# s x -> f# -(*(s s 0(), s x), s s x)}
       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 -> f -(*(s s 0(), s x), s s x)}
       Open
      
      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 -> f -(*(s s 0(), s x), s s x)}
       Open
      
      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 -> f -(*(s s 0(), s x), s s x)}
       Open
      
      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 -> f -(*(s s 0(), s x), s s x)}
       Open