MAYBE
Time: 0.020219
TRS:
 {  +(0(), y) -> y,
    +(s x, y) -> s +(x, y),
    *(x, 0()) -> 0(),
    *(x, s y) -> +(x, *(x, y)),
    twice 0() -> 0(),
    twice s x -> s s twice x,
    -(x, 0()) -> x,
  -(s x, s y) -> -(x, y),
        f s x -> f -(*(s s x, s s x), +(*(s x, s s x), s s 0()))}
 DP:
  DP:
   {  +#(s x, y) -> +#(x, y),
      *#(x, s y) -> +#(x, *(x, y)),
      *#(x, s y) -> *#(x, y),
      twice# s x -> twice# x,
    -#(s x, s y) -> -#(x, y),
          f# s x -> +#(*(s x, s s x), s s 0()),
          f# s x -> *#(s x, s s x),
          f# s x -> *#(s s x, s s x),
          f# s x -> -#(*(s s x, s s x), +(*(s x, s s x), s s 0())),
          f# s x -> f# -(*(s s x, s s x), +(*(s x, s s x), s s 0()))}
  TRS:
  {  +(0(), y) -> y,
     +(s x, y) -> s +(x, y),
     *(x, 0()) -> 0(),
     *(x, s y) -> +(x, *(x, y)),
     twice 0() -> 0(),
     twice s x -> s s twice x,
     -(x, 0()) -> x,
   -(s x, s y) -> -(x, y),
         f s x -> f -(*(s s x, s s x), +(*(s x, s s x), s s 0()))}
  UR:
   {  +(0(), y) -> y,
      +(s x, y) -> s +(x, y),
      *(x, 0()) -> 0(),
      *(x, s y) -> +(x, *(x, y)),
      -(x, 0()) -> x,
    -(s x, s y) -> -(x, y),
        a(z, w) -> z,
        a(z, w) -> w}
   EDG:
    {(*#(x, s y) -> +#(x, *(x, y)), +#(s x, y) -> +#(x, y))
     (f# s x -> +#(*(s x, s s x), s s 0()), +#(s x, y) -> +#(x, y))
     (f# s x -> *#(s s x, s s x), *#(x, s y) -> *#(x, y))
     (f# s x -> *#(s s x, s s x), *#(x, s y) -> +#(x, *(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 x, s s x), +(*(s x, s s x), s s 0())), f# s x -> f# -(*(s s x, s s x), +(*(s x, s s x), s s 0())))
     (f# s x -> f# -(*(s s x, s s x), +(*(s x, s s x), s s 0())), f# s x -> -#(*(s s x, s s x), +(*(s x, s s x), s s 0())))
     (f# s x -> f# -(*(s s x, s s x), +(*(s x, s s x), s s 0())), f# s x -> *#(s s x, s s x))
     (f# s x -> f# -(*(s s x, s s x), +(*(s x, s s x), s s 0())), f# s x -> *#(s x, s s x))
     (f# s x -> f# -(*(s s x, s s x), +(*(s x, s s x), s s 0())), f# s x -> +#(*(s x, s s x), s s 0()))
     (-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y))
     (+#(s x, y) -> +#(x, y), +#(s x, y) -> +#(x, y))
     (f# s x -> *#(s x, s s x), *#(x, s y) -> +#(x, *(x, y)))
     (f# s x -> *#(s x, s s x), *#(x, s y) -> *#(x, y))
     (f# s x -> -#(*(s s x, s s x), +(*(s x, s s x), s s 0())), -#(s x, s y) -> -#(x, y))
     (twice# s x -> twice# x, twice# s x -> twice# x)}
    EDG:
     {(*#(x, s y) -> +#(x, *(x, y)), +#(s x, y) -> +#(x, y))
      (f# s x -> +#(*(s x, s s x), s s 0()), +#(s x, y) -> +#(x, y))
      (f# s x -> *#(s s x, s s x), *#(x, s y) -> *#(x, y))
      (f# s x -> *#(s s x, s s x), *#(x, s y) -> +#(x, *(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 x, s s x), +(*(s x, s s x), s s 0())), f# s x -> f# -(*(s s x, s s x), +(*(s x, s s x), s s 0())))
      (f# s x -> f# -(*(s s x, s s x), +(*(s x, s s x), s s 0())), f# s x -> -#(*(s s x, s s x), +(*(s x, s s x), s s 0())))
      (f# s x -> f# -(*(s s x, s s x), +(*(s x, s s x), s s 0())), f# s x -> *#(s s x, s s x))
      (f# s x -> f# -(*(s s x, s s x), +(*(s x, s s x), s s 0())), f# s x -> *#(s x, s s x))
      (f# s x -> f# -(*(s s x, s s x), +(*(s x, s s x), s s 0())), f# s x -> +#(*(s x, s s x), s s 0()))
      (-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y))
      (+#(s x, y) -> +#(x, y), +#(s x, y) -> +#(x, y))
      (f# s x -> *#(s x, s s x), *#(x, s y) -> +#(x, *(x, y)))
      (f# s x -> *#(s x, s s x), *#(x, s y) -> *#(x, y))
      (f# s x -> -#(*(s s x, s s x), +(*(s x, s s x), s s 0())), -#(s x, s y) -> -#(x, y))
      (twice# s x -> twice# x, twice# s x -> twice# x)}
     EDG:
      {(*#(x, s y) -> +#(x, *(x, y)), +#(s x, y) -> +#(x, y))
       (f# s x -> +#(*(s x, s s x), s s 0()), +#(s x, y) -> +#(x, y))
       (f# s x -> *#(s s x, s s x), *#(x, s y) -> *#(x, y))
       (f# s x -> *#(s s x, s s x), *#(x, s y) -> +#(x, *(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 x, s s x), +(*(s x, s s x), s s 0())), f# s x -> f# -(*(s s x, s s x), +(*(s x, s s x), s s 0())))
       (f# s x -> f# -(*(s s x, s s x), +(*(s x, s s x), s s 0())), f# s x -> -#(*(s s x, s s x), +(*(s x, s s x), s s 0())))
       (f# s x -> f# -(*(s s x, s s x), +(*(s x, s s x), s s 0())), f# s x -> *#(s s x, s s x))
       (f# s x -> f# -(*(s s x, s s x), +(*(s x, s s x), s s 0())), f# s x -> *#(s x, s s x))
       (f# s x -> f# -(*(s s x, s s x), +(*(s x, s s x), s s 0())), f# s x -> +#(*(s x, s s x), s s 0()))
       (-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y))
       (+#(s x, y) -> +#(x, y), +#(s x, y) -> +#(x, y))
       (f# s x -> *#(s x, s s x), *#(x, s y) -> +#(x, *(x, y)))
       (f# s x -> *#(s x, s s x), *#(x, s y) -> *#(x, y))
       (f# s x -> -#(*(s s x, s s x), +(*(s x, s s x), s s 0())), -#(s x, s y) -> -#(x, y))
       (twice# s x -> twice# x, twice# s x -> twice# x)}
      EDG:
       {(*#(x, s y) -> +#(x, *(x, y)), +#(s x, y) -> +#(x, y))
        (f# s x -> +#(*(s x, s s x), s s 0()), +#(s x, y) -> +#(x, y))
        (f# s x -> *#(s s x, s s x), *#(x, s y) -> *#(x, y))
        (f# s x -> *#(s s x, s s x), *#(x, s y) -> +#(x, *(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 x, s s x), +(*(s x, s s x), s s 0())), f# s x -> f# -(*(s s x, s s x), +(*(s x, s s x), s s 0())))
        (f# s x -> f# -(*(s s x, s s x), +(*(s x, s s x), s s 0())), f# s x -> -#(*(s s x, s s x), +(*(s x, s s x), s s 0())))
        (f# s x -> f# -(*(s s x, s s x), +(*(s x, s s x), s s 0())), f# s x -> *#(s s x, s s x))
        (f# s x -> f# -(*(s s x, s s x), +(*(s x, s s x), s s 0())), f# s x -> *#(s x, s s x))
        (f# s x -> f# -(*(s s x, s s x), +(*(s x, s s x), s s 0())), f# s x -> +#(*(s x, s s x), s s 0()))
        (-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y))
        (+#(s x, y) -> +#(x, y), +#(s x, y) -> +#(x, y))
        (f# s x -> *#(s x, s s x), *#(x, s y) -> +#(x, *(x, y)))
        (f# s x -> *#(s x, s s x), *#(x, s y) -> *#(x, y))
        (f# s x -> -#(*(s s x, s s x), +(*(s x, s s x), s s 0())), -#(s x, s y) -> -#(x, y))
        (twice# s x -> twice# x, twice# s x -> twice# x)}
       STATUS:
        arrows: 0.830000
        SCCS (5):
         Scc:
          {f# s x -> f# -(*(s s x, s s x), +(*(s x, s s x), s s 0()))}
         Scc:
          {*#(x, s y) -> *#(x, y)}
         Scc:
          {-#(s x, s y) -> -#(x, y)}
         Scc:
          {+#(s x, y) -> +#(x, y)}
         Scc:
          {twice# s x -> twice# x}
         
         SCC (1):
          Strict:
           {f# s x -> f# -(*(s s x, s s x), +(*(s x, s s x), s s 0()))}
          Weak:
          {  +(0(), y) -> y,
             +(s x, y) -> s +(x, y),
             *(x, 0()) -> 0(),
             *(x, s y) -> +(x, *(x, y)),
             twice 0() -> 0(),
             twice s x -> s s twice x,
             -(x, 0()) -> x,
           -(s x, s y) -> -(x, y),
                 f s x -> f -(*(s s x, s s x), +(*(s x, s s x), s s 0()))}
          Open
         
         
         SCC (1):
          Strict:
           {*#(x, s y) -> *#(x, y)}
          Weak:
          {  +(0(), y) -> y,
             +(s x, y) -> s +(x, y),
             *(x, 0()) -> 0(),
             *(x, s y) -> +(x, *(x, y)),
             twice 0() -> 0(),
             twice s x -> s s twice x,
             -(x, 0()) -> x,
           -(s x, s y) -> -(x, y),
                 f s x -> f -(*(s s x, s s x), +(*(s x, s s x), s s 0()))}
          Open
         
         
         SCC (1):
          Strict:
           {-#(s x, s y) -> -#(x, y)}
          Weak:
          {  +(0(), y) -> y,
             +(s x, y) -> s +(x, y),
             *(x, 0()) -> 0(),
             *(x, s y) -> +(x, *(x, y)),
             twice 0() -> 0(),
             twice s x -> s s twice x,
             -(x, 0()) -> x,
           -(s x, s y) -> -(x, y),
                 f s x -> f -(*(s s x, s s x), +(*(s x, s s x), s s 0()))}
          Open
         
         SCC (1):
          Strict:
           {+#(s x, y) -> +#(x, y)}
          Weak:
          {  +(0(), y) -> y,
             +(s x, y) -> s +(x, y),
             *(x, 0()) -> 0(),
             *(x, s y) -> +(x, *(x, y)),
             twice 0() -> 0(),
             twice s x -> s s twice x,
             -(x, 0()) -> x,
           -(s x, s y) -> -(x, y),
                 f s x -> f -(*(s s x, s s x), +(*(s x, s s x), s s 0()))}
          Open
         SCC (1):
          Strict:
           {twice# s x -> twice# x}
          Weak:
          {  +(0(), y) -> y,
             +(s x, y) -> s +(x, y),
             *(x, 0()) -> 0(),
             *(x, s y) -> +(x, *(x, y)),
             twice 0() -> 0(),
             twice s x -> s s twice x,
             -(x, 0()) -> x,
           -(s x, s y) -> -(x, y),
                 f s x -> f -(*(s s x, s s x), +(*(s x, s s x), s s 0()))}
          Open