MAYBE
Time: 0.022520
TRS:
 {        0 #() -> #(),
      +(x, #()) -> x,
      +(#(), x) -> x,
    +(0 x, 0 y) -> 0 +(x, y),
    +(0 x, 1 y) -> 1 +(x, y),
    +(0 x, j y) -> j +(x, y),
  +(+(x, y), z) -> +(x, +(y, z)),
    +(1 x, 0 y) -> 1 +(x, y),
    +(1 x, 1 y) -> j +(+(x, y), 1 #()),
    +(1 x, j y) -> 0 +(x, y),
    +(j x, 0 y) -> j +(x, y),
    +(j x, 1 y) -> 0 +(x, y),
    +(j x, j y) -> 1 +(+(x, y), j #()),
        opp #() -> #(),
        opp 0 x -> 0 opp x,
        opp 1 x -> j opp x,
        opp j x -> 1 opp x,
        -(x, y) -> +(x, opp y),
      *(#(), x) -> #(),
      *(0 x, y) -> 0 *(x, y),
      *(1 x, y) -> +(0 *(x, y), y),
      *(j x, y) -> -(0 *(x, y), y),
  *(*(x, y), z) -> *(x, *(y, z))}
 DP:
  DP:
   {  +#(0 x, 0 y) -> 0# +(x, y),
      +#(0 x, 0 y) -> +#(x, y),
      +#(0 x, 1 y) -> +#(x, y),
      +#(0 x, j y) -> +#(x, y),
    +#(+(x, y), z) -> +#(x, +(y, z)),
    +#(+(x, y), z) -> +#(y, z),
      +#(1 x, 0 y) -> +#(x, y),
      +#(1 x, 1 y) -> +#(x, y),
      +#(1 x, 1 y) -> +#(+(x, y), 1 #()),
      +#(1 x, j y) -> 0# +(x, y),
      +#(1 x, j y) -> +#(x, y),
      +#(j x, 0 y) -> +#(x, y),
      +#(j x, 1 y) -> 0# +(x, y),
      +#(j x, 1 y) -> +#(x, y),
      +#(j x, j y) -> +#(x, y),
      +#(j x, j y) -> +#(+(x, y), j #()),
          opp# 0 x -> 0# opp x,
          opp# 0 x -> opp# x,
          opp# 1 x -> opp# x,
          opp# j x -> opp# x,
          -#(x, y) -> +#(x, opp y),
          -#(x, y) -> opp# y,
        *#(0 x, y) -> 0# *(x, y),
        *#(0 x, y) -> *#(x, y),
        *#(1 x, y) -> 0# *(x, y),
        *#(1 x, y) -> +#(0 *(x, y), y),
        *#(1 x, y) -> *#(x, y),
        *#(j x, y) -> 0# *(x, y),
        *#(j x, y) -> -#(0 *(x, y), y),
        *#(j x, y) -> *#(x, y),
    *#(*(x, y), z) -> *#(x, *(y, z)),
    *#(*(x, y), z) -> *#(y, z)}
  TRS:
  {        0 #() -> #(),
       +(x, #()) -> x,
       +(#(), x) -> x,
     +(0 x, 0 y) -> 0 +(x, y),
     +(0 x, 1 y) -> 1 +(x, y),
     +(0 x, j y) -> j +(x, y),
   +(+(x, y), z) -> +(x, +(y, z)),
     +(1 x, 0 y) -> 1 +(x, y),
     +(1 x, 1 y) -> j +(+(x, y), 1 #()),
     +(1 x, j y) -> 0 +(x, y),
     +(j x, 0 y) -> j +(x, y),
     +(j x, 1 y) -> 0 +(x, y),
     +(j x, j y) -> 1 +(+(x, y), j #()),
         opp #() -> #(),
         opp 0 x -> 0 opp x,
         opp 1 x -> j opp x,
         opp j x -> 1 opp x,
         -(x, y) -> +(x, opp y),
       *(#(), x) -> #(),
       *(0 x, y) -> 0 *(x, y),
       *(1 x, y) -> +(0 *(x, y), y),
       *(j x, y) -> -(0 *(x, y), y),
   *(*(x, y), z) -> *(x, *(y, z))}
  UR:
   {        0 #() -> #(),
        +(x, #()) -> x,
        +(#(), x) -> x,
      +(0 x, 0 y) -> 0 +(x, y),
      +(0 x, 1 y) -> 1 +(x, y),
      +(0 x, j y) -> j +(x, y),
    +(+(x, y), z) -> +(x, +(y, z)),
      +(1 x, 0 y) -> 1 +(x, y),
      +(1 x, 1 y) -> j +(+(x, y), 1 #()),
      +(1 x, j y) -> 0 +(x, y),
      +(j x, 0 y) -> j +(x, y),
      +(j x, 1 y) -> 0 +(x, y),
      +(j x, j y) -> 1 +(+(x, y), j #()),
          opp #() -> #(),
          opp 0 x -> 0 opp x,
          opp 1 x -> j opp x,
          opp j x -> 1 opp x,
          -(x, y) -> +(x, opp y),
        *(#(), x) -> #(),
        *(0 x, y) -> 0 *(x, y),
        *(1 x, y) -> +(0 *(x, y), y),
        *(j x, y) -> -(0 *(x, y), y),
    *(*(x, y), z) -> *(x, *(y, z)),
          a(w, v) -> w,
          a(w, v) -> v}
   EDG:
    {
     (+#(j x, j y) -> +#(+(x, y), j #()), +#(j x, j y) -> +#(+(x, y), j #()))
     (+#(j x, j y) -> +#(+(x, y), j #()), +#(j x, j y) -> +#(x, y))
     (+#(j x, j y) -> +#(+(x, y), j #()), +#(1 x, j y) -> +#(x, y))
     (+#(j x, j y) -> +#(+(x, y), j #()), +#(1 x, j y) -> 0# +(x, y))
     (+#(j x, j y) -> +#(+(x, y), j #()), +#(+(x, y), z) -> +#(y, z))
     (+#(j x, j y) -> +#(+(x, y), j #()), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(j x, j y) -> +#(+(x, y), j #()), +#(0 x, j y) -> +#(x, y))
     (-#(x, y) -> opp# y, opp# j x -> opp# x)
     (-#(x, y) -> opp# y, opp# 1 x -> opp# x)
     (-#(x, y) -> opp# y, opp# 0 x -> opp# x)
     (-#(x, y) -> opp# y, opp# 0 x -> 0# opp x)
     (*#(j x, y) -> -#(0 *(x, y), y), -#(x, y) -> opp# y)
     (*#(j x, y) -> -#(0 *(x, y), y), -#(x, y) -> +#(x, opp y))
     (*#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(y, z))
     (*#(*(x, y), z) -> *#(x, *(y, z)), *#(*(x, y), z) -> *#(x, *(y, z)))
     (*#(*(x, y), z) -> *#(x, *(y, z)), *#(j x, y) -> *#(x, y))
     (*#(*(x, y), z) -> *#(x, *(y, z)), *#(j x, y) -> -#(0 *(x, y), y))
     (*#(*(x, y), z) -> *#(x, *(y, z)), *#(j x, y) -> 0# *(x, y))
     (*#(*(x, y), z) -> *#(x, *(y, z)), *#(1 x, y) -> *#(x, y))
     (*#(*(x, y), z) -> *#(x, *(y, z)), *#(1 x, y) -> +#(0 *(x, y), y))
     (*#(*(x, y), z) -> *#(x, *(y, z)), *#(1 x, y) -> 0# *(x, y))
     (*#(*(x, y), z) -> *#(x, *(y, z)), *#(0 x, y) -> *#(x, y))
     (*#(*(x, y), z) -> *#(x, *(y, z)), *#(0 x, y) -> 0# *(x, y))
     (opp# 1 x -> opp# x, opp# j x -> opp# x)
     (opp# 1 x -> opp# x, opp# 1 x -> opp# x)
     (opp# 1 x -> opp# x, opp# 0 x -> opp# x)
     (opp# 1 x -> opp# x, opp# 0 x -> 0# opp x)
     (+#(0 x, 0 y) -> +#(x, y), +#(j x, j y) -> +#(+(x, y), j #()))
     (+#(0 x, 0 y) -> +#(x, y), +#(j x, j y) -> +#(x, y))
     (+#(0 x, 0 y) -> +#(x, y), +#(j x, 1 y) -> +#(x, y))
     (+#(0 x, 0 y) -> +#(x, y), +#(j x, 1 y) -> 0# +(x, y))
     (+#(0 x, 0 y) -> +#(x, y), +#(j x, 0 y) -> +#(x, y))
     (+#(0 x, 0 y) -> +#(x, y), +#(1 x, j y) -> +#(x, y))
     (+#(0 x, 0 y) -> +#(x, y), +#(1 x, j y) -> 0# +(x, y))
     (+#(0 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (+#(0 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y))
     (+#(0 x, 0 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y))
     (+#(0 x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
     (+#(0 x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(0 x, 0 y) -> +#(x, y), +#(0 x, j y) -> +#(x, y))
     (+#(0 x, 0 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y))
     (+#(0 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y))
     (+#(0 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y))
     (+#(0 x, j y) -> +#(x, y), +#(j x, j y) -> +#(+(x, y), j #()))
     (+#(0 x, j y) -> +#(x, y), +#(j x, j y) -> +#(x, y))
     (+#(0 x, j y) -> +#(x, y), +#(j x, 1 y) -> +#(x, y))
     (+#(0 x, j y) -> +#(x, y), +#(j x, 1 y) -> 0# +(x, y))
     (+#(0 x, j y) -> +#(x, y), +#(j x, 0 y) -> +#(x, y))
     (+#(0 x, j y) -> +#(x, y), +#(1 x, j y) -> +#(x, y))
     (+#(0 x, j y) -> +#(x, y), +#(1 x, j y) -> 0# +(x, y))
     (+#(0 x, j y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (+#(0 x, j y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y))
     (+#(0 x, j y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y))
     (+#(0 x, j y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
     (+#(0 x, j y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(0 x, j y) -> +#(x, y), +#(0 x, j y) -> +#(x, y))
     (+#(0 x, j y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y))
     (+#(0 x, j y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y))
     (+#(0 x, j y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y))
     (+#(1 x, 1 y) -> +#(x, y), +#(j x, j y) -> +#(+(x, y), j #()))
     (+#(1 x, 1 y) -> +#(x, y), +#(j x, j y) -> +#(x, y))
     (+#(1 x, 1 y) -> +#(x, y), +#(j x, 1 y) -> +#(x, y))
     (+#(1 x, 1 y) -> +#(x, y), +#(j x, 1 y) -> 0# +(x, y))
     (+#(1 x, 1 y) -> +#(x, y), +#(j x, 0 y) -> +#(x, y))
     (+#(1 x, 1 y) -> +#(x, y), +#(1 x, j y) -> +#(x, y))
     (+#(1 x, 1 y) -> +#(x, y), +#(1 x, j y) -> 0# +(x, y))
     (+#(1 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (+#(1 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y))
     (+#(1 x, 1 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y))
     (+#(1 x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
     (+#(1 x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(1 x, 1 y) -> +#(x, y), +#(0 x, j y) -> +#(x, y))
     (+#(1 x, 1 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y))
     (+#(1 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y))
     (+#(1 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y))
     (+#(j x, 0 y) -> +#(x, y), +#(j x, j y) -> +#(+(x, y), j #()))
     (+#(j x, 0 y) -> +#(x, y), +#(j x, j y) -> +#(x, y))
     (+#(j x, 0 y) -> +#(x, y), +#(j x, 1 y) -> +#(x, y))
     (+#(j x, 0 y) -> +#(x, y), +#(j x, 1 y) -> 0# +(x, y))
     (+#(j x, 0 y) -> +#(x, y), +#(j x, 0 y) -> +#(x, y))
     (+#(j x, 0 y) -> +#(x, y), +#(1 x, j y) -> +#(x, y))
     (+#(j x, 0 y) -> +#(x, y), +#(1 x, j y) -> 0# +(x, y))
     (+#(j x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (+#(j x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y))
     (+#(j x, 0 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y))
     (+#(j x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
     (+#(j x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(j x, 0 y) -> +#(x, y), +#(0 x, j y) -> +#(x, y))
     (+#(j x, 0 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y))
     (+#(j x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y))
     (+#(j x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y))
     (+#(j x, j y) -> +#(x, y), +#(j x, j y) -> +#(+(x, y), j #()))
     (+#(j x, j y) -> +#(x, y), +#(j x, j y) -> +#(x, y))
     (+#(j x, j y) -> +#(x, y), +#(j x, 1 y) -> +#(x, y))
     (+#(j x, j y) -> +#(x, y), +#(j x, 1 y) -> 0# +(x, y))
     (+#(j x, j y) -> +#(x, y), +#(j x, 0 y) -> +#(x, y))
     (+#(j x, j y) -> +#(x, y), +#(1 x, j y) -> +#(x, y))
     (+#(j x, j y) -> +#(x, y), +#(1 x, j y) -> 0# +(x, y))
     (+#(j x, j y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (+#(j x, j y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y))
     (+#(j x, j y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y))
     (+#(j x, j y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
     (+#(j x, j y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(j x, j y) -> +#(x, y), +#(0 x, j y) -> +#(x, y))
     (+#(j x, j y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y))
     (+#(j x, j y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y))
     (+#(j x, j y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y))
     (*#(1 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z))
     (*#(1 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z)))
     (*#(1 x, y) -> *#(x, y), *#(j x, y) -> *#(x, y))
     (*#(1 x, y) -> *#(x, y), *#(j x, y) -> -#(0 *(x, y), y))
     (*#(1 x, y) -> *#(x, y), *#(j x, y) -> 0# *(x, y))
     (*#(1 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y))
     (*#(1 x, y) -> *#(x, y), *#(1 x, y) -> +#(0 *(x, y), y))
     (*#(1 x, y) -> *#(x, y), *#(1 x, y) -> 0# *(x, y))
     (*#(1 x, y) -> *#(x, y), *#(0 x, y) -> *#(x, y))
     (*#(1 x, y) -> *#(x, y), *#(0 x, y) -> 0# *(x, y))
     (-#(x, y) -> +#(x, opp y), +#(j x, j y) -> +#(+(x, y), j #()))
     (-#(x, y) -> +#(x, opp y), +#(j x, j y) -> +#(x, y))
     (-#(x, y) -> +#(x, opp y), +#(j x, 1 y) -> +#(x, y))
     (-#(x, y) -> +#(x, opp y), +#(j x, 1 y) -> 0# +(x, y))
     (-#(x, y) -> +#(x, opp y), +#(j x, 0 y) -> +#(x, y))
     (-#(x, y) -> +#(x, opp y), +#(1 x, j y) -> +#(x, y))
     (-#(x, y) -> +#(x, opp y), +#(1 x, j y) -> 0# +(x, y))
     (-#(x, y) -> +#(x, opp y), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (-#(x, y) -> +#(x, opp y), +#(1 x, 1 y) -> +#(x, y))
     (-#(x, y) -> +#(x, opp y), +#(1 x, 0 y) -> +#(x, y))
     (-#(x, y) -> +#(x, opp y), +#(+(x, y), z) -> +#(y, z))
     (-#(x, y) -> +#(x, opp y), +#(+(x, y), z) -> +#(x, +(y, z)))
     (-#(x, y) -> +#(x, opp y), +#(0 x, j y) -> +#(x, y))
     (-#(x, y) -> +#(x, opp y), +#(0 x, 1 y) -> +#(x, y))
     (-#(x, y) -> +#(x, opp y), +#(0 x, 0 y) -> +#(x, y))
     (-#(x, y) -> +#(x, opp y), +#(0 x, 0 y) -> 0# +(x, y))
     (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(y, z))
     (*#(*(x, y), z) -> *#(y, z), *#(*(x, y), z) -> *#(x, *(y, z)))
     (*#(*(x, y), z) -> *#(y, z), *#(j x, y) -> *#(x, y))
     (*#(*(x, y), z) -> *#(y, z), *#(j x, y) -> -#(0 *(x, y), y))
     (*#(*(x, y), z) -> *#(y, z), *#(j x, y) -> 0# *(x, y))
     (*#(*(x, y), z) -> *#(y, z), *#(1 x, y) -> *#(x, y))
     (*#(*(x, y), z) -> *#(y, z), *#(1 x, y) -> +#(0 *(x, y), y))
     (*#(*(x, y), z) -> *#(y, z), *#(1 x, y) -> 0# *(x, y))
     (*#(*(x, y), z) -> *#(y, z), *#(0 x, y) -> *#(x, y))
     (*#(*(x, y), z) -> *#(y, z), *#(0 x, y) -> 0# *(x, y))
     (+#(+(x, y), z) -> +#(y, z), +#(0 x, 0 y) -> 0# +(x, y))
     (+#(+(x, y), z) -> +#(y, z), +#(0 x, 0 y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(y, z), +#(0 x, 1 y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(y, z), +#(0 x, j y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(+(x, y), z) -> +#(y, z), +#(+(x, y), z) -> +#(y, z))
     (+#(+(x, y), z) -> +#(y, z), +#(1 x, 0 y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(y, z), +#(1 x, 1 y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(y, z), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (+#(+(x, y), z) -> +#(y, z), +#(1 x, j y) -> 0# +(x, y))
     (+#(+(x, y), z) -> +#(y, z), +#(1 x, j y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(y, z), +#(j x, 0 y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(y, z), +#(j x, 1 y) -> 0# +(x, y))
     (+#(+(x, y), z) -> +#(y, z), +#(j x, 1 y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(y, z), +#(j x, j y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(y, z), +#(j x, j y) -> +#(+(x, y), j #()))
     (*#(j x, y) -> *#(x, y), *#(0 x, y) -> 0# *(x, y))
     (*#(j x, y) -> *#(x, y), *#(0 x, y) -> *#(x, y))
     (*#(j x, y) -> *#(x, y), *#(1 x, y) -> 0# *(x, y))
     (*#(j x, y) -> *#(x, y), *#(1 x, y) -> +#(0 *(x, y), y))
     (*#(j x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y))
     (*#(j x, y) -> *#(x, y), *#(j x, y) -> 0# *(x, y))
     (*#(j x, y) -> *#(x, y), *#(j x, y) -> -#(0 *(x, y), y))
     (*#(j x, y) -> *#(x, y), *#(j x, y) -> *#(x, y))
     (*#(j x, y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z)))
     (*#(j x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z))
     (*#(0 x, y) -> *#(x, y), *#(0 x, y) -> 0# *(x, y))
     (*#(0 x, y) -> *#(x, y), *#(0 x, y) -> *#(x, y))
     (*#(0 x, y) -> *#(x, y), *#(1 x, y) -> 0# *(x, y))
     (*#(0 x, y) -> *#(x, y), *#(1 x, y) -> +#(0 *(x, y), y))
     (*#(0 x, y) -> *#(x, y), *#(1 x, y) -> *#(x, y))
     (*#(0 x, y) -> *#(x, y), *#(j x, y) -> 0# *(x, y))
     (*#(0 x, y) -> *#(x, y), *#(j x, y) -> -#(0 *(x, y), y))
     (*#(0 x, y) -> *#(x, y), *#(j x, y) -> *#(x, y))
     (*#(0 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(x, *(y, z)))
     (*#(0 x, y) -> *#(x, y), *#(*(x, y), z) -> *#(y, z))
     (+#(j x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y))
     (+#(j x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y))
     (+#(j x, 1 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y))
     (+#(j x, 1 y) -> +#(x, y), +#(0 x, j y) -> +#(x, y))
     (+#(j x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(j x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
     (+#(j x, 1 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y))
     (+#(j x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y))
     (+#(j x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (+#(j x, 1 y) -> +#(x, y), +#(1 x, j y) -> 0# +(x, y))
     (+#(j x, 1 y) -> +#(x, y), +#(1 x, j y) -> +#(x, y))
     (+#(j x, 1 y) -> +#(x, y), +#(j x, 0 y) -> +#(x, y))
     (+#(j x, 1 y) -> +#(x, y), +#(j x, 1 y) -> 0# +(x, y))
     (+#(j x, 1 y) -> +#(x, y), +#(j x, 1 y) -> +#(x, y))
     (+#(j x, 1 y) -> +#(x, y), +#(j x, j y) -> +#(x, y))
     (+#(j x, 1 y) -> +#(x, y), +#(j x, j y) -> +#(+(x, y), j #()))
     (+#(1 x, j y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y))
     (+#(1 x, j y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y))
     (+#(1 x, j y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y))
     (+#(1 x, j y) -> +#(x, y), +#(0 x, j y) -> +#(x, y))
     (+#(1 x, j y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(1 x, j y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
     (+#(1 x, j y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y))
     (+#(1 x, j y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y))
     (+#(1 x, j y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (+#(1 x, j y) -> +#(x, y), +#(1 x, j y) -> 0# +(x, y))
     (+#(1 x, j y) -> +#(x, y), +#(1 x, j y) -> +#(x, y))
     (+#(1 x, j y) -> +#(x, y), +#(j x, 0 y) -> +#(x, y))
     (+#(1 x, j y) -> +#(x, y), +#(j x, 1 y) -> 0# +(x, y))
     (+#(1 x, j y) -> +#(x, y), +#(j x, 1 y) -> +#(x, y))
     (+#(1 x, j y) -> +#(x, y), +#(j x, j y) -> +#(x, y))
     (+#(1 x, j y) -> +#(x, y), +#(j x, j y) -> +#(+(x, y), j #()))
     (+#(1 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y))
     (+#(1 x, 0 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y))
     (+#(1 x, 0 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y))
     (+#(1 x, 0 y) -> +#(x, y), +#(0 x, j y) -> +#(x, y))
     (+#(1 x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(1 x, 0 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
     (+#(1 x, 0 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y))
     (+#(1 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y))
     (+#(1 x, 0 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (+#(1 x, 0 y) -> +#(x, y), +#(1 x, j y) -> 0# +(x, y))
     (+#(1 x, 0 y) -> +#(x, y), +#(1 x, j y) -> +#(x, y))
     (+#(1 x, 0 y) -> +#(x, y), +#(j x, 0 y) -> +#(x, y))
     (+#(1 x, 0 y) -> +#(x, y), +#(j x, 1 y) -> 0# +(x, y))
     (+#(1 x, 0 y) -> +#(x, y), +#(j x, 1 y) -> +#(x, y))
     (+#(1 x, 0 y) -> +#(x, y), +#(j x, j y) -> +#(x, y))
     (+#(1 x, 0 y) -> +#(x, y), +#(j x, j y) -> +#(+(x, y), j #()))
     (+#(0 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> 0# +(x, y))
     (+#(0 x, 1 y) -> +#(x, y), +#(0 x, 0 y) -> +#(x, y))
     (+#(0 x, 1 y) -> +#(x, y), +#(0 x, 1 y) -> +#(x, y))
     (+#(0 x, 1 y) -> +#(x, y), +#(0 x, j y) -> +#(x, y))
     (+#(0 x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(0 x, 1 y) -> +#(x, y), +#(+(x, y), z) -> +#(y, z))
     (+#(0 x, 1 y) -> +#(x, y), +#(1 x, 0 y) -> +#(x, y))
     (+#(0 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(x, y))
     (+#(0 x, 1 y) -> +#(x, y), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (+#(0 x, 1 y) -> +#(x, y), +#(1 x, j y) -> 0# +(x, y))
     (+#(0 x, 1 y) -> +#(x, y), +#(1 x, j y) -> +#(x, y))
     (+#(0 x, 1 y) -> +#(x, y), +#(j x, 0 y) -> +#(x, y))
     (+#(0 x, 1 y) -> +#(x, y), +#(j x, 1 y) -> 0# +(x, y))
     (+#(0 x, 1 y) -> +#(x, y), +#(j x, 1 y) -> +#(x, y))
     (+#(0 x, 1 y) -> +#(x, y), +#(j x, j y) -> +#(x, y))
     (+#(0 x, 1 y) -> +#(x, y), +#(j x, j y) -> +#(+(x, y), j #()))
     (opp# j x -> opp# x, opp# 0 x -> 0# opp x)
     (opp# j x -> opp# x, opp# 0 x -> opp# x)
     (opp# j x -> opp# x, opp# 1 x -> opp# x)
     (opp# j x -> opp# x, opp# j x -> opp# x)
     (opp# 0 x -> opp# x, opp# 0 x -> 0# opp x)
     (opp# 0 x -> opp# x, opp# 0 x -> opp# x)
     (opp# 0 x -> opp# x, opp# 1 x -> opp# x)
     (opp# 0 x -> opp# x, opp# j x -> opp# x)
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0 x, 0 y) -> 0# +(x, y))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0 x, 0 y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0 x, 1 y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(0 x, j y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(+(x, y), z) -> +#(y, z))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1 x, 0 y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1 x, 1 y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1 x, j y) -> 0# +(x, y))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(1 x, j y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(j x, 0 y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(j x, 1 y) -> 0# +(x, y))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(j x, 1 y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(j x, j y) -> +#(x, y))
     (+#(+(x, y), z) -> +#(x, +(y, z)), +#(j x, j y) -> +#(+(x, y), j #()))
     (*#(1 x, y) -> +#(0 *(x, y), y), +#(0 x, 0 y) -> 0# +(x, y))
     (*#(1 x, y) -> +#(0 *(x, y), y), +#(0 x, 0 y) -> +#(x, y))
     (*#(1 x, y) -> +#(0 *(x, y), y), +#(0 x, 1 y) -> +#(x, y))
     (*#(1 x, y) -> +#(0 *(x, y), y), +#(0 x, j y) -> +#(x, y))
     (*#(1 x, y) -> +#(0 *(x, y), y), +#(+(x, y), z) -> +#(x, +(y, z)))
     (*#(1 x, y) -> +#(0 *(x, y), y), +#(+(x, y), z) -> +#(y, z))
     (*#(1 x, y) -> +#(0 *(x, y), y), +#(1 x, 0 y) -> +#(x, y))
     (*#(1 x, y) -> +#(0 *(x, y), y), +#(1 x, 1 y) -> +#(x, y))
     (*#(1 x, y) -> +#(0 *(x, y), y), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (*#(1 x, y) -> +#(0 *(x, y), y), +#(1 x, j y) -> 0# +(x, y))
     (*#(1 x, y) -> +#(0 *(x, y), y), +#(1 x, j y) -> +#(x, y))
     (*#(1 x, y) -> +#(0 *(x, y), y), +#(j x, 0 y) -> +#(x, y))
     (*#(1 x, y) -> +#(0 *(x, y), y), +#(j x, 1 y) -> 0# +(x, y))
     (*#(1 x, y) -> +#(0 *(x, y), y), +#(j x, 1 y) -> +#(x, y))
     (*#(1 x, y) -> +#(0 *(x, y), y), +#(j x, j y) -> +#(x, y))
     (*#(1 x, y) -> +#(0 *(x, y), y), +#(j x, j y) -> +#(+(x, y), j #()))
     (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(0 x, 1 y) -> +#(x, y))
     (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(+(x, y), z) -> +#(x, +(y, z)))
     (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(+(x, y), z) -> +#(y, z))
     (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(1 x, 1 y) -> +#(x, y))
     (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(1 x, 1 y) -> +#(+(x, y), 1 #()))
     (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(j x, 1 y) -> 0# +(x, y))
     (+#(1 x, 1 y) -> +#(+(x, y), 1 #()), +#(j x, 1 y) -> +#(x, y))
    }
    STATUS:
     arrows: 0.716797
     SCCS (3):
      Scc:
       {    *#(0 x, y) -> *#(x, y),
            *#(1 x, y) -> *#(x, y),
            *#(j x, y) -> *#(x, y),
        *#(*(x, y), z) -> *#(x, *(y, z)),
        *#(*(x, y), z) -> *#(y, z)}
      Scc:
       {opp# 0 x -> opp# x,
        opp# 1 x -> opp# x,
        opp# j x -> opp# x}
      Scc:
       {  +#(0 x, 0 y) -> +#(x, y),
          +#(0 x, 1 y) -> +#(x, y),
          +#(0 x, j y) -> +#(x, y),
        +#(+(x, y), z) -> +#(x, +(y, z)),
        +#(+(x, y), z) -> +#(y, z),
          +#(1 x, 0 y) -> +#(x, y),
          +#(1 x, 1 y) -> +#(x, y),
          +#(1 x, 1 y) -> +#(+(x, y), 1 #()),
          +#(1 x, j y) -> +#(x, y),
          +#(j x, 0 y) -> +#(x, y),
          +#(j x, 1 y) -> +#(x, y),
          +#(j x, j y) -> +#(x, y),
          +#(j x, j y) -> +#(+(x, y), j #())}
      
      SCC (5):
       Strict:
        {    *#(0 x, y) -> *#(x, y),
             *#(1 x, y) -> *#(x, y),
             *#(j x, y) -> *#(x, y),
         *#(*(x, y), z) -> *#(x, *(y, z)),
         *#(*(x, y), z) -> *#(y, z)}
       Weak:
       {        0 #() -> #(),
            +(x, #()) -> x,
            +(#(), x) -> x,
          +(0 x, 0 y) -> 0 +(x, y),
          +(0 x, 1 y) -> 1 +(x, y),
          +(0 x, j y) -> j +(x, y),
        +(+(x, y), z) -> +(x, +(y, z)),
          +(1 x, 0 y) -> 1 +(x, y),
          +(1 x, 1 y) -> j +(+(x, y), 1 #()),
          +(1 x, j y) -> 0 +(x, y),
          +(j x, 0 y) -> j +(x, y),
          +(j x, 1 y) -> 0 +(x, y),
          +(j x, j y) -> 1 +(+(x, y), j #()),
              opp #() -> #(),
              opp 0 x -> 0 opp x,
              opp 1 x -> j opp x,
              opp j x -> 1 opp x,
              -(x, y) -> +(x, opp y),
            *(#(), x) -> #(),
            *(0 x, y) -> 0 *(x, y),
            *(1 x, y) -> +(0 *(x, y), y),
            *(j x, y) -> -(0 *(x, y), y),
        *(*(x, y), z) -> *(x, *(y, z))}
       Open
      
      
      
      
      
      
      
      SCC (3):
       Strict:
        {opp# 0 x -> opp# x,
         opp# 1 x -> opp# x,
         opp# j x -> opp# x}
       Weak:
       {        0 #() -> #(),
            +(x, #()) -> x,
            +(#(), x) -> x,
          +(0 x, 0 y) -> 0 +(x, y),
          +(0 x, 1 y) -> 1 +(x, y),
          +(0 x, j y) -> j +(x, y),
        +(+(x, y), z) -> +(x, +(y, z)),
          +(1 x, 0 y) -> 1 +(x, y),
          +(1 x, 1 y) -> j +(+(x, y), 1 #()),
          +(1 x, j y) -> 0 +(x, y),
          +(j x, 0 y) -> j +(x, y),
          +(j x, 1 y) -> 0 +(x, y),
          +(j x, j y) -> 1 +(+(x, y), j #()),
              opp #() -> #(),
              opp 0 x -> 0 opp x,
              opp 1 x -> j opp x,
              opp j x -> 1 opp x,
              -(x, y) -> +(x, opp y),
            *(#(), x) -> #(),
            *(0 x, y) -> 0 *(x, y),
            *(1 x, y) -> +(0 *(x, y), y),
            *(j x, y) -> -(0 *(x, y), y),
        *(*(x, y), z) -> *(x, *(y, z))}
       Open
      
      SCC (13):
       Strict:
        {  +#(0 x, 0 y) -> +#(x, y),
           +#(0 x, 1 y) -> +#(x, y),
           +#(0 x, j y) -> +#(x, y),
         +#(+(x, y), z) -> +#(x, +(y, z)),
         +#(+(x, y), z) -> +#(y, z),
           +#(1 x, 0 y) -> +#(x, y),
           +#(1 x, 1 y) -> +#(x, y),
           +#(1 x, 1 y) -> +#(+(x, y), 1 #()),
           +#(1 x, j y) -> +#(x, y),
           +#(j x, 0 y) -> +#(x, y),
           +#(j x, 1 y) -> +#(x, y),
           +#(j x, j y) -> +#(x, y),
           +#(j x, j y) -> +#(+(x, y), j #())}
       Weak:
       {        0 #() -> #(),
            +(x, #()) -> x,
            +(#(), x) -> x,
          +(0 x, 0 y) -> 0 +(x, y),
          +(0 x, 1 y) -> 1 +(x, y),
          +(0 x, j y) -> j +(x, y),
        +(+(x, y), z) -> +(x, +(y, z)),
          +(1 x, 0 y) -> 1 +(x, y),
          +(1 x, 1 y) -> j +(+(x, y), 1 #()),
          +(1 x, j y) -> 0 +(x, y),
          +(j x, 0 y) -> j +(x, y),
          +(j x, 1 y) -> 0 +(x, y),
          +(j x, j y) -> 1 +(+(x, y), j #()),
              opp #() -> #(),
              opp 0 x -> 0 opp x,
              opp 1 x -> j opp x,
              opp j x -> 1 opp x,
              -(x, y) -> +(x, opp y),
            *(#(), x) -> #(),
            *(0 x, y) -> 0 *(x, y),
            *(1 x, y) -> +(0 *(x, y), y),
            *(j x, y) -> -(0 *(x, y), y),
        *(*(x, y), z) -> *(x, *(y, z))}
       Open