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