MAYBE
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:
  Strict:
   {-#(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)))))}
  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)))))}
  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))}
   SCCS:
    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), y) -> +#(x, y)}
    Scc:
     {-#(s(x), s(y)) -> -#(x, y)}
    SCC:
     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)))))}
     Fail
    SCC:
     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)))))}
     SPSC:
      Simple Projection:
       pi(*#) = 1
      Strict:
       {}
      Qed
    SCC:
     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)))))}
     SPSC:
      Simple Projection:
       pi(+#) = 0
      Strict:
       {}
      Qed
    SCC:
     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)))))}
     SPSC:
      Simple Projection:
       pi(-#) = 0
      Strict:
       {}
      Qed