MAYBE
Time: 0.008419
TRS:
 {    +(x, 0()) -> x,
  +(minus x, x) -> 0(),
  minus +(x, y) -> +(minus y, minus x),
      minus 0() -> 0(),
  minus minus x -> x,
  *(x, +(y, z)) -> +(*(x, y), *(x, z)),
      *(x, 0()) -> 0(),
  *(x, minus y) -> minus *(x, y),
      *(x, 1()) -> x}
 DP:
  DP:
   {minus# +(x, y) -> +#(minus y, minus x),
    minus# +(x, y) -> minus# x,
    minus# +(x, y) -> minus# y,
    *#(x, +(y, z)) -> +#(*(x, y), *(x, z)),
    *#(x, +(y, z)) -> *#(x, y),
    *#(x, +(y, z)) -> *#(x, z),
    *#(x, minus y) -> minus# *(x, y),
    *#(x, minus y) -> *#(x, y)}
  TRS:
  {    +(x, 0()) -> x,
   +(minus x, x) -> 0(),
   minus +(x, y) -> +(minus y, minus x),
       minus 0() -> 0(),
   minus minus x -> x,
   *(x, +(y, z)) -> +(*(x, y), *(x, z)),
       *(x, 0()) -> 0(),
   *(x, minus y) -> minus *(x, y),
       *(x, 1()) -> x}
  EDG:
   {(*#(x, minus y) -> *#(x, y), *#(x, minus y) -> *#(x, y))
    (*#(x, minus y) -> *#(x, y), *#(x, minus y) -> minus# *(x, y))
    (*#(x, minus y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z))
    (*#(x, minus y) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y))
    (*#(x, minus y) -> *#(x, y), *#(x, +(y, z)) -> +#(*(x, y), *(x, z)))
    (minus# +(x, y) -> minus# y, minus# +(x, y) -> minus# y)
    (minus# +(x, y) -> minus# y, minus# +(x, y) -> minus# x)
    (minus# +(x, y) -> minus# y, minus# +(x, y) -> +#(minus y, minus x))
    (*#(x, +(y, z)) -> *#(x, z), *#(x, minus y) -> *#(x, y))
    (*#(x, +(y, z)) -> *#(x, z), *#(x, minus y) -> minus# *(x, y))
    (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, z))
    (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> *#(x, y))
    (*#(x, +(y, z)) -> *#(x, z), *#(x, +(y, z)) -> +#(*(x, y), *(x, z)))
    (*#(x, minus y) -> minus# *(x, y), minus# +(x, y) -> +#(minus y, minus x))
    (*#(x, minus y) -> minus# *(x, y), minus# +(x, y) -> minus# x)
    (*#(x, minus y) -> minus# *(x, y), minus# +(x, y) -> minus# y)
    (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> +#(*(x, y), *(x, z)))
    (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, y))
    (*#(x, +(y, z)) -> *#(x, y), *#(x, +(y, z)) -> *#(x, z))
    (*#(x, +(y, z)) -> *#(x, y), *#(x, minus y) -> minus# *(x, y))
    (*#(x, +(y, z)) -> *#(x, y), *#(x, minus y) -> *#(x, y))
    (minus# +(x, y) -> minus# x, minus# +(x, y) -> +#(minus y, minus x))
    (minus# +(x, y) -> minus# x, minus# +(x, y) -> minus# x)
    (minus# +(x, y) -> minus# x, minus# +(x, y) -> minus# y)}
   STATUS:
    arrows: 0.625000
    SCCS (2):
     Scc:
      {*#(x, +(y, z)) -> *#(x, y),
       *#(x, +(y, z)) -> *#(x, z),
       *#(x, minus y) -> *#(x, y)}
     Scc:
      {minus# +(x, y) -> minus# x,
       minus# +(x, y) -> minus# y}
     
     SCC (3):
      Strict:
       {*#(x, +(y, z)) -> *#(x, y),
        *#(x, +(y, z)) -> *#(x, z),
        *#(x, minus y) -> *#(x, y)}
      Weak:
      {    +(x, 0()) -> x,
       +(minus x, x) -> 0(),
       minus +(x, y) -> +(minus y, minus x),
           minus 0() -> 0(),
       minus minus x -> x,
       *(x, +(y, z)) -> +(*(x, y), *(x, z)),
           *(x, 0()) -> 0(),
       *(x, minus y) -> minus *(x, y),
           *(x, 1()) -> x}
      Open
     
     
     SCC (2):
      Strict:
       {minus# +(x, y) -> minus# x,
        minus# +(x, y) -> minus# y}
      Weak:
      {    +(x, 0()) -> x,
       +(minus x, x) -> 0(),
       minus +(x, y) -> +(minus y, minus x),
           minus 0() -> 0(),
       minus minus x -> x,
       *(x, +(y, z)) -> +(*(x, y), *(x, z)),
           *(x, 0()) -> 0(),
       *(x, minus y) -> minus *(x, y),
           *(x, 1()) -> x}
      Open