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