MAYBE
Time: 0.008670
TRS:
 {      O 0() -> 0(),
    +(x, 0()) -> x,
    +(0(), x) -> x,
  +(O x, O y) -> O +(x, y),
  +(O x, I y) -> I +(x, y),
  +(I x, O y) -> I +(x, y),
  +(I x, I y) -> O +(+(x, y), I 0()),
    *(x, 0()) -> 0(),
    *(0(), x) -> 0(),
    *(O x, y) -> O *(x, y),
    *(I x, y) -> +(O *(x, y), y),
    -(x, 0()) -> x,
    -(0(), x) -> 0(),
  -(O x, O y) -> O -(x, y),
  -(O x, I y) -> I -(-(x, y), I 1()),
  -(I x, O y) -> I -(x, y),
  -(I x, I y) -> O -(x, y)}
 DP:
  DP:
   {+#(O x, O y) -> O# +(x, y),
    +#(O x, O y) -> +#(x, y),
    +#(O x, I y) -> +#(x, y),
    +#(I x, O y) -> +#(x, y),
    +#(I x, I y) -> O# +(+(x, y), I 0()),
    +#(I x, I y) -> +#(x, y),
    +#(I x, I y) -> +#(+(x, y), I 0()),
      *#(O x, y) -> O# *(x, y),
      *#(O x, y) -> *#(x, y),
      *#(I x, y) -> O# *(x, y),
      *#(I x, y) -> +#(O *(x, y), y),
      *#(I x, y) -> *#(x, y),
    -#(O x, O y) -> O# -(x, y),
    -#(O x, O y) -> -#(x, y),
    -#(O x, I y) -> -#(x, y),
    -#(O x, I y) -> -#(-(x, y), I 1()),
    -#(I x, O y) -> -#(x, y),
    -#(I x, I y) -> O# -(x, y),
    -#(I x, I y) -> -#(x, y)}
  TRS:
  {      O 0() -> 0(),
     +(x, 0()) -> x,
     +(0(), x) -> x,
   +(O x, O y) -> O +(x, y),
   +(O x, I y) -> I +(x, y),
   +(I x, O y) -> I +(x, y),
   +(I x, I y) -> O +(+(x, y), I 0()),
     *(x, 0()) -> 0(),
     *(0(), x) -> 0(),
     *(O x, y) -> O *(x, y),
     *(I x, y) -> +(O *(x, y), y),
     -(x, 0()) -> x,
     -(0(), x) -> 0(),
   -(O x, O y) -> O -(x, y),
   -(O x, I y) -> I -(-(x, y), I 1()),
   -(I x, O y) -> I -(x, y),
   -(I x, I y) -> O -(x, y)}
  UR:
   {      O 0() -> 0(),
      +(x, 0()) -> x,
      +(0(), x) -> x,
    +(O x, O y) -> O +(x, y),
    +(O x, I y) -> I +(x, y),
    +(I x, O y) -> I +(x, y),
    +(I x, I y) -> O +(+(x, y), I 0()),
      *(x, 0()) -> 0(),
      *(0(), x) -> 0(),
      *(O x, y) -> O *(x, y),
      *(I x, y) -> +(O *(x, y), y),
      -(x, 0()) -> x,
      -(0(), x) -> 0(),
    -(O x, O y) -> O -(x, y),
    -(O x, I y) -> I -(-(x, y), I 1()),
    -(I x, O y) -> I -(x, y),
    -(I x, I y) -> O -(x, y),
        a(z, w) -> z,
        a(z, w) -> w}
   EDG:
    {(+#(O x, I y) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0()))
     (+#(O x, I y) -> +#(x, y), +#(I x, I y) -> +#(x, y))
     (+#(O x, I y) -> +#(x, y), +#(I x, I y) -> O# +(+(x, y), I 0()))
     (+#(O x, I y) -> +#(x, y), +#(I x, O y) -> +#(x, y))
     (+#(O x, I y) -> +#(x, y), +#(O x, I y) -> +#(x, y))
     (+#(O x, I y) -> +#(x, y), +#(O x, O y) -> +#(x, y))
     (+#(O x, I y) -> +#(x, y), +#(O x, O y) -> O# +(x, y))
     (+#(I x, I y) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0()))
     (+#(I x, I y) -> +#(x, y), +#(I x, I y) -> +#(x, y))
     (+#(I x, I y) -> +#(x, y), +#(I x, I y) -> O# +(+(x, y), I 0()))
     (+#(I x, I y) -> +#(x, y), +#(I x, O y) -> +#(x, y))
     (+#(I x, I y) -> +#(x, y), +#(O x, I y) -> +#(x, y))
     (+#(I x, I y) -> +#(x, y), +#(O x, O y) -> +#(x, y))
     (+#(I x, I y) -> +#(x, y), +#(O x, O y) -> O# +(x, y))
     (*#(I x, y) -> *#(x, y), *#(I x, y) -> *#(x, y))
     (*#(I x, y) -> *#(x, y), *#(I x, y) -> +#(O *(x, y), y))
     (*#(I x, y) -> *#(x, y), *#(I x, y) -> O# *(x, y))
     (*#(I x, y) -> *#(x, y), *#(O x, y) -> *#(x, y))
     (*#(I x, y) -> *#(x, y), *#(O x, y) -> O# *(x, y))
     (-#(O x, I y) -> -#(x, y), -#(I x, I y) -> -#(x, y))
     (-#(O x, I y) -> -#(x, y), -#(I x, I y) -> O# -(x, y))
     (-#(O x, I y) -> -#(x, y), -#(I x, O y) -> -#(x, y))
     (-#(O x, I y) -> -#(x, y), -#(O x, I y) -> -#(-(x, y), I 1()))
     (-#(O x, I y) -> -#(x, y), -#(O x, I y) -> -#(x, y))
     (-#(O x, I y) -> -#(x, y), -#(O x, O y) -> -#(x, y))
     (-#(O x, I y) -> -#(x, y), -#(O x, O y) -> O# -(x, y))
     (-#(I x, I y) -> -#(x, y), -#(I x, I y) -> -#(x, y))
     (-#(I x, I y) -> -#(x, y), -#(I x, I y) -> O# -(x, y))
     (-#(I x, I y) -> -#(x, y), -#(I x, O y) -> -#(x, y))
     (-#(I x, I y) -> -#(x, y), -#(O x, I y) -> -#(-(x, y), I 1()))
     (-#(I x, I y) -> -#(x, y), -#(O x, I y) -> -#(x, y))
     (-#(I x, I y) -> -#(x, y), -#(O x, O y) -> -#(x, y))
     (-#(I x, I y) -> -#(x, y), -#(O x, O y) -> O# -(x, y))
     (+#(I x, I y) -> +#(+(x, y), I 0()), +#(I x, I y) -> +#(+(x, y), I 0()))
     (+#(I x, I y) -> +#(+(x, y), I 0()), +#(I x, I y) -> +#(x, y))
     (+#(I x, I y) -> +#(+(x, y), I 0()), +#(I x, I y) -> O# +(+(x, y), I 0()))
     (+#(I x, I y) -> +#(+(x, y), I 0()), +#(I x, O y) -> +#(x, y))
     (+#(I x, I y) -> +#(+(x, y), I 0()), +#(O x, I y) -> +#(x, y))
     (+#(I x, I y) -> +#(+(x, y), I 0()), +#(O x, O y) -> +#(x, y))
     (+#(I x, I y) -> +#(+(x, y), I 0()), +#(O x, O y) -> O# +(x, y))
     (-#(O x, I y) -> -#(-(x, y), I 1()), -#(O x, O y) -> O# -(x, y))
     (-#(O x, I y) -> -#(-(x, y), I 1()), -#(O x, O y) -> -#(x, y))
     (-#(O x, I y) -> -#(-(x, y), I 1()), -#(O x, I y) -> -#(x, y))
     (-#(O x, I y) -> -#(-(x, y), I 1()), -#(O x, I y) -> -#(-(x, y), I 1()))
     (-#(O x, I y) -> -#(-(x, y), I 1()), -#(I x, O y) -> -#(x, y))
     (-#(O x, I y) -> -#(-(x, y), I 1()), -#(I x, I y) -> O# -(x, y))
     (-#(O x, I y) -> -#(-(x, y), I 1()), -#(I x, I y) -> -#(x, y))
     (-#(I x, O y) -> -#(x, y), -#(O x, O y) -> O# -(x, y))
     (-#(I x, O y) -> -#(x, y), -#(O x, O y) -> -#(x, y))
     (-#(I x, O y) -> -#(x, y), -#(O x, I y) -> -#(x, y))
     (-#(I x, O y) -> -#(x, y), -#(O x, I y) -> -#(-(x, y), I 1()))
     (-#(I x, O y) -> -#(x, y), -#(I x, O y) -> -#(x, y))
     (-#(I x, O y) -> -#(x, y), -#(I x, I y) -> O# -(x, y))
     (-#(I x, O y) -> -#(x, y), -#(I x, I y) -> -#(x, y))
     (-#(O x, O y) -> -#(x, y), -#(O x, O y) -> O# -(x, y))
     (-#(O x, O y) -> -#(x, y), -#(O x, O y) -> -#(x, y))
     (-#(O x, O y) -> -#(x, y), -#(O x, I y) -> -#(x, y))
     (-#(O x, O y) -> -#(x, y), -#(O x, I y) -> -#(-(x, y), I 1()))
     (-#(O x, O y) -> -#(x, y), -#(I x, O y) -> -#(x, y))
     (-#(O x, O y) -> -#(x, y), -#(I x, I y) -> O# -(x, y))
     (-#(O x, O y) -> -#(x, y), -#(I x, I y) -> -#(x, y))
     (*#(O x, y) -> *#(x, y), *#(O x, y) -> O# *(x, y))
     (*#(O x, y) -> *#(x, y), *#(O x, y) -> *#(x, y))
     (*#(O x, y) -> *#(x, y), *#(I x, y) -> O# *(x, y))
     (*#(O x, y) -> *#(x, y), *#(I x, y) -> +#(O *(x, y), y))
     (*#(O x, y) -> *#(x, y), *#(I x, y) -> *#(x, y))
     (+#(I x, O y) -> +#(x, y), +#(O x, O y) -> O# +(x, y))
     (+#(I x, O y) -> +#(x, y), +#(O x, O y) -> +#(x, y))
     (+#(I x, O y) -> +#(x, y), +#(O x, I y) -> +#(x, y))
     (+#(I x, O y) -> +#(x, y), +#(I x, O y) -> +#(x, y))
     (+#(I x, O y) -> +#(x, y), +#(I x, I y) -> O# +(+(x, y), I 0()))
     (+#(I x, O y) -> +#(x, y), +#(I x, I y) -> +#(x, y))
     (+#(I x, O y) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0()))
     (+#(O x, O y) -> +#(x, y), +#(O x, O y) -> O# +(x, y))
     (+#(O x, O y) -> +#(x, y), +#(O x, O y) -> +#(x, y))
     (+#(O x, O y) -> +#(x, y), +#(O x, I y) -> +#(x, y))
     (+#(O x, O y) -> +#(x, y), +#(I x, O y) -> +#(x, y))
     (+#(O x, O y) -> +#(x, y), +#(I x, I y) -> O# +(+(x, y), I 0()))
     (+#(O x, O y) -> +#(x, y), +#(I x, I y) -> +#(x, y))
     (+#(O x, O y) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0()))
     (*#(I x, y) -> +#(O *(x, y), y), +#(O x, O y) -> O# +(x, y))
     (*#(I x, y) -> +#(O *(x, y), y), +#(O x, O y) -> +#(x, y))
     (*#(I x, y) -> +#(O *(x, y), y), +#(O x, I y) -> +#(x, y))
     (*#(I x, y) -> +#(O *(x, y), y), +#(I x, O y) -> +#(x, y))
     (*#(I x, y) -> +#(O *(x, y), y), +#(I x, I y) -> O# +(+(x, y), I 0()))
     (*#(I x, y) -> +#(O *(x, y), y), +#(I x, I y) -> +#(x, y))
     (*#(I x, y) -> +#(O *(x, y), y), +#(I x, I y) -> +#(+(x, y), I 0()))}
    STATUS:
     arrows: 0.759003
     SCCS (3):
      Scc:
       {-#(O x, O y) -> -#(x, y),
        -#(O x, I y) -> -#(x, y),
        -#(O x, I y) -> -#(-(x, y), I 1()),
        -#(I x, O y) -> -#(x, y),
        -#(I x, I y) -> -#(x, y)}
      Scc:
       {*#(O x, y) -> *#(x, y),
        *#(I x, y) -> *#(x, y)}
      Scc:
       {+#(O x, O y) -> +#(x, y),
        +#(O x, I y) -> +#(x, y),
        +#(I x, O y) -> +#(x, y),
        +#(I x, I y) -> +#(x, y),
        +#(I x, I y) -> +#(+(x, y), I 0())}
      
      SCC (5):
       Strict:
        {-#(O x, O y) -> -#(x, y),
         -#(O x, I y) -> -#(x, y),
         -#(O x, I y) -> -#(-(x, y), I 1()),
         -#(I x, O y) -> -#(x, y),
         -#(I x, I y) -> -#(x, y)}
       Weak:
       {      O 0() -> 0(),
          +(x, 0()) -> x,
          +(0(), x) -> x,
        +(O x, O y) -> O +(x, y),
        +(O x, I y) -> I +(x, y),
        +(I x, O y) -> I +(x, y),
        +(I x, I y) -> O +(+(x, y), I 0()),
          *(x, 0()) -> 0(),
          *(0(), x) -> 0(),
          *(O x, y) -> O *(x, y),
          *(I x, y) -> +(O *(x, y), y),
          -(x, 0()) -> x,
          -(0(), x) -> 0(),
        -(O x, O y) -> O -(x, y),
        -(O x, I y) -> I -(-(x, y), I 1()),
        -(I x, O y) -> I -(x, y),
        -(I x, I y) -> O -(x, y)}
       Open
      SCC (2):
       Strict:
        {*#(O x, y) -> *#(x, y),
         *#(I x, y) -> *#(x, y)}
       Weak:
       {      O 0() -> 0(),
          +(x, 0()) -> x,
          +(0(), x) -> x,
        +(O x, O y) -> O +(x, y),
        +(O x, I y) -> I +(x, y),
        +(I x, O y) -> I +(x, y),
        +(I x, I y) -> O +(+(x, y), I 0()),
          *(x, 0()) -> 0(),
          *(0(), x) -> 0(),
          *(O x, y) -> O *(x, y),
          *(I x, y) -> +(O *(x, y), y),
          -(x, 0()) -> x,
          -(0(), x) -> 0(),
        -(O x, O y) -> O -(x, y),
        -(O x, I y) -> I -(-(x, y), I 1()),
        -(I x, O y) -> I -(x, y),
        -(I x, I y) -> O -(x, y)}
       Open
      
      
      
      
      
      SCC (5):
       Strict:
        {+#(O x, O y) -> +#(x, y),
         +#(O x, I y) -> +#(x, y),
         +#(I x, O y) -> +#(x, y),
         +#(I x, I y) -> +#(x, y),
         +#(I x, I y) -> +#(+(x, y), I 0())}
       Weak:
       {      O 0() -> 0(),
          +(x, 0()) -> x,
          +(0(), x) -> x,
        +(O x, O y) -> O +(x, y),
        +(O x, I y) -> I +(x, y),
        +(I x, O y) -> I +(x, y),
        +(I x, I y) -> O +(+(x, y), I 0()),
          *(x, 0()) -> 0(),
          *(0(), x) -> 0(),
          *(O x, y) -> O *(x, y),
          *(I x, y) -> +(O *(x, y), y),
          -(x, 0()) -> x,
          -(0(), x) -> 0(),
        -(O x, O y) -> O -(x, y),
        -(O x, I y) -> I -(-(x, y), I 1()),
        -(I x, O y) -> I -(x, y),
        -(I x, I y) -> O -(x, y)}
       Open