MAYBE
Time: 0.003391
TRS:
 {+(0(), y) -> y,
  +(s x, y) -> s +(x, y),
  +(p x, y) -> p +(x, y),
  minus 0() -> 0(),
  minus s x -> p minus x,
  minus p x -> s minus x,
  *(0(), y) -> 0(),
  *(s x, y) -> +(*(x, y), y),
  *(p x, y) -> +(*(x, y), minus y)}
 DP:
  DP:
   {+#(s x, y) -> +#(x, y),
    +#(p x, y) -> +#(x, y),
    minus# s x -> minus# x,
    minus# p x -> minus# x,
    *#(s x, y) -> +#(*(x, y), y),
    *#(s x, y) -> *#(x, y),
    *#(p x, y) -> +#(*(x, y), minus y),
    *#(p x, y) -> minus# y,
    *#(p x, y) -> *#(x, y)}
  TRS:
  {+(0(), y) -> y,
   +(s x, y) -> s +(x, y),
   +(p x, y) -> p +(x, y),
   minus 0() -> 0(),
   minus s x -> p minus x,
   minus p x -> s minus x,
   *(0(), y) -> 0(),
   *(s x, y) -> +(*(x, y), y),
   *(p x, y) -> +(*(x, y), minus y)}
  UR:
   {+(0(), y) -> y,
    +(s x, y) -> s +(x, y),
    +(p x, y) -> p +(x, y),
    minus 0() -> 0(),
    minus s x -> p minus x,
    minus p x -> s minus x,
    *(0(), y) -> 0(),
    *(s x, y) -> +(*(x, y), y),
    *(p x, y) -> +(*(x, y), minus y),
      a(z, w) -> z,
      a(z, w) -> w}
   EDG:
    {(*#(s x, y) -> +#(*(x, y), y), +#(p x, y) -> +#(x, y))
     (*#(s x, y) -> +#(*(x, y), y), +#(s x, y) -> +#(x, y))
     (+#(p x, y) -> +#(x, y), +#(p x, y) -> +#(x, y))
     (+#(p x, y) -> +#(x, y), +#(s x, y) -> +#(x, y))
     (*#(p x, y) -> *#(x, y), *#(p x, y) -> *#(x, y))
     (*#(p x, y) -> *#(x, y), *#(p x, y) -> minus# y)
     (*#(p x, y) -> *#(x, y), *#(p x, y) -> +#(*(x, y), minus y))
     (*#(p x, y) -> *#(x, y), *#(s x, y) -> *#(x, y))
     (*#(p x, y) -> *#(x, y), *#(s x, y) -> +#(*(x, y), y))
     (minus# p x -> minus# x, minus# p x -> minus# x)
     (minus# p x -> minus# x, minus# s x -> minus# x)
     (*#(p x, y) -> +#(*(x, y), minus y), +#(s x, y) -> +#(x, y))
     (*#(p x, y) -> +#(*(x, y), minus y), +#(p x, y) -> +#(x, y))
     (minus# s x -> minus# x, minus# s x -> minus# x)
     (minus# s x -> minus# x, minus# p x -> minus# x)
     (*#(s x, y) -> *#(x, y), *#(s x, y) -> +#(*(x, y), y))
     (*#(s x, y) -> *#(x, y), *#(s x, y) -> *#(x, y))
     (*#(s x, y) -> *#(x, y), *#(p x, y) -> +#(*(x, y), minus y))
     (*#(s x, y) -> *#(x, y), *#(p x, y) -> minus# y)
     (*#(s x, y) -> *#(x, y), *#(p x, y) -> *#(x, y))
     (+#(s x, y) -> +#(x, y), +#(s x, y) -> +#(x, y))
     (+#(s x, y) -> +#(x, y), +#(p x, y) -> +#(x, y))
     (*#(p x, y) -> minus# y, minus# s x -> minus# x)
     (*#(p x, y) -> minus# y, minus# p x -> minus# x)}
    STATUS:
     arrows: 0.703704
     SCCS (3):
      Scc:
       {*#(s x, y) -> *#(x, y),
        *#(p x, y) -> *#(x, y)}
      Scc:
       {+#(s x, y) -> +#(x, y),
        +#(p x, y) -> +#(x, y)}
      Scc:
       {minus# s x -> minus# x,
        minus# p x -> minus# x}
      
      SCC (2):
       Strict:
        {*#(s x, y) -> *#(x, y),
         *#(p x, y) -> *#(x, y)}
       Weak:
       {+(0(), y) -> y,
        +(s x, y) -> s +(x, y),
        +(p x, y) -> p +(x, y),
        minus 0() -> 0(),
        minus s x -> p minus x,
        minus p x -> s minus x,
        *(0(), y) -> 0(),
        *(s x, y) -> +(*(x, y), y),
        *(p x, y) -> +(*(x, y), minus y)}
       Open
      
      
      SCC (2):
       Strict:
        {+#(s x, y) -> +#(x, y),
         +#(p x, y) -> +#(x, y)}
       Weak:
       {+(0(), y) -> y,
        +(s x, y) -> s +(x, y),
        +(p x, y) -> p +(x, y),
        minus 0() -> 0(),
        minus s x -> p minus x,
        minus p x -> s minus x,
        *(0(), y) -> 0(),
        *(s x, y) -> +(*(x, y), y),
        *(p x, y) -> +(*(x, y), minus y)}
       Open
      
      SCC (2):
       Strict:
        {minus# s x -> minus# x,
         minus# p x -> minus# x}
       Weak:
       {+(0(), y) -> y,
        +(s x, y) -> s +(x, y),
        +(p x, y) -> p +(x, y),
        minus 0() -> 0(),
        minus s x -> p minus x,
        minus p x -> s minus x,
        *(0(), y) -> 0(),
        *(s x, y) -> +(*(x, y), y),
        *(p x, y) -> +(*(x, y), minus y)}
       Open