MAYBE
Time: 0.023305
TRS:
 {          *(x, *(y, z)) -> *(*(x, y), z),
                *(x, 1()) -> x,
                *(x, i x) -> 1(),
          *(*(x, y), i y) -> x,
          *(*(x, i y), y) -> x,
    *(*(i x, k(y, z)), x) -> k(*(*(i x, y), x), *(*(i x, z), x)),
                *(1(), y) -> y,
                *(i x, x) -> 1(),
      *(k(x, y), k(y, x)) -> 1(),
                i *(x, y) -> *(i y, i x),
                    i 1() -> 1(),
                    i i x -> x,
                  k(x, x) -> 1(),
                k(x, 1()) -> 1(),
  k(*(x, i y), *(y, i x)) -> 1()}
 DP:
  DP:
   {        *#(x, *(y, z)) -> *#(x, y),
            *#(x, *(y, z)) -> *#(*(x, y), z),
    *#(*(i x, k(y, z)), x) -> *#(*(i x, y), x),
    *#(*(i x, k(y, z)), x) -> *#(*(i x, z), x),
    *#(*(i x, k(y, z)), x) -> *#(i x, y),
    *#(*(i x, k(y, z)), x) -> *#(i x, z),
    *#(*(i x, k(y, z)), x) -> k#(*(*(i x, y), x), *(*(i x, z), x)),
                i# *(x, y) -> *#(i y, i x),
                i# *(x, y) -> i# x,
                i# *(x, y) -> i# y}
  TRS:
  {          *(x, *(y, z)) -> *(*(x, y), z),
                 *(x, 1()) -> x,
                 *(x, i x) -> 1(),
           *(*(x, y), i y) -> x,
           *(*(x, i y), y) -> x,
     *(*(i x, k(y, z)), x) -> k(*(*(i x, y), x), *(*(i x, z), x)),
                 *(1(), y) -> y,
                 *(i x, x) -> 1(),
       *(k(x, y), k(y, x)) -> 1(),
                 i *(x, y) -> *(i y, i x),
                     i 1() -> 1(),
                     i i x -> x,
                   k(x, x) -> 1(),
                 k(x, 1()) -> 1(),
   k(*(x, i y), *(y, i x)) -> 1()}
  UR:
   {          *(x, *(y, z)) -> *(*(x, y), z),
                  *(x, 1()) -> x,
                  *(x, i x) -> 1(),
            *(*(x, y), i y) -> x,
            *(*(x, i y), y) -> x,
      *(*(i x, k(y, z)), x) -> k(*(*(i x, y), x), *(*(i x, z), x)),
                  *(1(), y) -> y,
                  *(i x, x) -> 1(),
        *(k(x, y), k(y, x)) -> 1(),
                  i *(x, y) -> *(i y, i x),
                      i 1() -> 1(),
                      i i x -> x,
                    k(x, x) -> 1(),
                  k(x, 1()) -> 1(),
    k(*(x, i y), *(y, i x)) -> 1(),
                    a(w, v) -> w,
                    a(w, v) -> v}
   EDG:
    {(*#(x, *(y, z)) -> *#(x, y), *#(*(i x, k(y, z)), x) -> k#(*(*(i x, y), x), *(*(i x, z), x)))
     (*#(x, *(y, z)) -> *#(x, y), *#(*(i x, k(y, z)), x) -> *#(i x, z))
     (*#(x, *(y, z)) -> *#(x, y), *#(*(i x, k(y, z)), x) -> *#(i x, y))
     (*#(x, *(y, z)) -> *#(x, y), *#(*(i x, k(y, z)), x) -> *#(*(i x, z), x))
     (*#(x, *(y, z)) -> *#(x, y), *#(*(i x, k(y, z)), x) -> *#(*(i x, y), x))
     (*#(x, *(y, z)) -> *#(x, y), *#(x, *(y, z)) -> *#(*(x, y), z))
     (*#(x, *(y, z)) -> *#(x, y), *#(x, *(y, z)) -> *#(x, y))
     (*#(*(i x, k(y, z)), x) -> *#(i x, z), *#(*(i x, k(y, z)), x) -> k#(*(*(i x, y), x), *(*(i x, z), x)))
     (*#(*(i x, k(y, z)), x) -> *#(i x, z), *#(*(i x, k(y, z)), x) -> *#(i x, z))
     (*#(*(i x, k(y, z)), x) -> *#(i x, z), *#(*(i x, k(y, z)), x) -> *#(i x, y))
     (*#(*(i x, k(y, z)), x) -> *#(i x, z), *#(*(i x, k(y, z)), x) -> *#(*(i x, z), x))
     (*#(*(i x, k(y, z)), x) -> *#(i x, z), *#(*(i x, k(y, z)), x) -> *#(*(i x, y), x))
     (*#(*(i x, k(y, z)), x) -> *#(i x, z), *#(x, *(y, z)) -> *#(*(x, y), z))
     (*#(*(i x, k(y, z)), x) -> *#(i x, z), *#(x, *(y, z)) -> *#(x, y))
     (*#(*(i x, k(y, z)), x) -> *#(*(i x, y), x), *#(*(i x, k(y, z)), x) -> k#(*(*(i x, y), x), *(*(i x, z), x)))
     (*#(*(i x, k(y, z)), x) -> *#(*(i x, y), x), *#(*(i x, k(y, z)), x) -> *#(i x, z))
     (*#(*(i x, k(y, z)), x) -> *#(*(i x, y), x), *#(*(i x, k(y, z)), x) -> *#(i x, y))
     (*#(*(i x, k(y, z)), x) -> *#(*(i x, y), x), *#(*(i x, k(y, z)), x) -> *#(*(i x, z), x))
     (*#(*(i x, k(y, z)), x) -> *#(*(i x, y), x), *#(*(i x, k(y, z)), x) -> *#(*(i x, y), x))
     (*#(*(i x, k(y, z)), x) -> *#(*(i x, y), x), *#(x, *(y, z)) -> *#(*(x, y), z))
     (*#(*(i x, k(y, z)), x) -> *#(*(i x, y), x), *#(x, *(y, z)) -> *#(x, y))
     (i# *(x, y) -> i# x, i# *(x, y) -> i# y)
     (i# *(x, y) -> i# x, i# *(x, y) -> i# x)
     (i# *(x, y) -> i# x, i# *(x, y) -> *#(i y, i x))
     (*#(*(i x, k(y, z)), x) -> *#(*(i x, z), x), *#(x, *(y, z)) -> *#(x, y))
     (*#(*(i x, k(y, z)), x) -> *#(*(i x, z), x), *#(x, *(y, z)) -> *#(*(x, y), z))
     (*#(*(i x, k(y, z)), x) -> *#(*(i x, z), x), *#(*(i x, k(y, z)), x) -> *#(*(i x, y), x))
     (*#(*(i x, k(y, z)), x) -> *#(*(i x, z), x), *#(*(i x, k(y, z)), x) -> *#(*(i x, z), x))
     (*#(*(i x, k(y, z)), x) -> *#(*(i x, z), x), *#(*(i x, k(y, z)), x) -> *#(i x, y))
     (*#(*(i x, k(y, z)), x) -> *#(*(i x, z), x), *#(*(i x, k(y, z)), x) -> *#(i x, z))
     (*#(*(i x, k(y, z)), x) -> *#(*(i x, z), x), *#(*(i x, k(y, z)), x) -> k#(*(*(i x, y), x), *(*(i x, z), x)))
     (*#(*(i x, k(y, z)), x) -> *#(i x, y), *#(x, *(y, z)) -> *#(x, y))
     (*#(*(i x, k(y, z)), x) -> *#(i x, y), *#(x, *(y, z)) -> *#(*(x, y), z))
     (*#(*(i x, k(y, z)), x) -> *#(i x, y), *#(*(i x, k(y, z)), x) -> *#(*(i x, y), x))
     (*#(*(i x, k(y, z)), x) -> *#(i x, y), *#(*(i x, k(y, z)), x) -> *#(*(i x, z), x))
     (*#(*(i x, k(y, z)), x) -> *#(i x, y), *#(*(i x, k(y, z)), x) -> *#(i x, y))
     (*#(*(i x, k(y, z)), x) -> *#(i x, y), *#(*(i x, k(y, z)), x) -> *#(i x, z))
     (*#(*(i x, k(y, z)), x) -> *#(i x, y), *#(*(i x, k(y, z)), x) -> k#(*(*(i x, y), x), *(*(i x, z), x)))
     (*#(x, *(y, z)) -> *#(*(x, y), z), *#(x, *(y, z)) -> *#(x, y))
     (*#(x, *(y, z)) -> *#(*(x, y), z), *#(x, *(y, z)) -> *#(*(x, y), z))
     (*#(x, *(y, z)) -> *#(*(x, y), z), *#(*(i x, k(y, z)), x) -> *#(*(i x, y), x))
     (*#(x, *(y, z)) -> *#(*(x, y), z), *#(*(i x, k(y, z)), x) -> *#(*(i x, z), x))
     (*#(x, *(y, z)) -> *#(*(x, y), z), *#(*(i x, k(y, z)), x) -> *#(i x, y))
     (*#(x, *(y, z)) -> *#(*(x, y), z), *#(*(i x, k(y, z)), x) -> *#(i x, z))
     (*#(x, *(y, z)) -> *#(*(x, y), z), *#(*(i x, k(y, z)), x) -> k#(*(*(i x, y), x), *(*(i x, z), x)))
     (i# *(x, y) -> *#(i y, i x), *#(x, *(y, z)) -> *#(x, y))
     (i# *(x, y) -> *#(i y, i x), *#(x, *(y, z)) -> *#(*(x, y), z))
     (i# *(x, y) -> *#(i y, i x), *#(*(i x, k(y, z)), x) -> *#(*(i x, y), x))
     (i# *(x, y) -> *#(i y, i x), *#(*(i x, k(y, z)), x) -> *#(*(i x, z), x))
     (i# *(x, y) -> *#(i y, i x), *#(*(i x, k(y, z)), x) -> *#(i x, y))
     (i# *(x, y) -> *#(i y, i x), *#(*(i x, k(y, z)), x) -> *#(i x, z))
     (i# *(x, y) -> *#(i y, i x), *#(*(i x, k(y, z)), x) -> k#(*(*(i x, y), x), *(*(i x, z), x)))
     (i# *(x, y) -> i# y, i# *(x, y) -> *#(i y, i x))
     (i# *(x, y) -> i# y, i# *(x, y) -> i# x)
     (i# *(x, y) -> i# y, i# *(x, y) -> i# y)}
    STATUS:
     arrows: 0.450000
     SCCS (2):
      Scc:
       {i# *(x, y) -> i# x,
        i# *(x, y) -> i# y}
      Scc:
       {        *#(x, *(y, z)) -> *#(x, y),
                *#(x, *(y, z)) -> *#(*(x, y), z),
        *#(*(i x, k(y, z)), x) -> *#(*(i x, y), x),
        *#(*(i x, k(y, z)), x) -> *#(*(i x, z), x),
        *#(*(i x, k(y, z)), x) -> *#(i x, y),
        *#(*(i x, k(y, z)), x) -> *#(i x, z)}
      
      SCC (2):
       Strict:
        {i# *(x, y) -> i# x,
         i# *(x, y) -> i# y}
       Weak:
       {          *(x, *(y, z)) -> *(*(x, y), z),
                      *(x, 1()) -> x,
                      *(x, i x) -> 1(),
                *(*(x, y), i y) -> x,
                *(*(x, i y), y) -> x,
          *(*(i x, k(y, z)), x) -> k(*(*(i x, y), x), *(*(i x, z), x)),
                      *(1(), y) -> y,
                      *(i x, x) -> 1(),
            *(k(x, y), k(y, x)) -> 1(),
                      i *(x, y) -> *(i y, i x),
                          i 1() -> 1(),
                          i i x -> x,
                        k(x, x) -> 1(),
                      k(x, 1()) -> 1(),
        k(*(x, i y), *(y, i x)) -> 1()}
       Open
      
      SCC (6):
       Strict:
        {        *#(x, *(y, z)) -> *#(x, y),
                 *#(x, *(y, z)) -> *#(*(x, y), z),
         *#(*(i x, k(y, z)), x) -> *#(*(i x, y), x),
         *#(*(i x, k(y, z)), x) -> *#(*(i x, z), x),
         *#(*(i x, k(y, z)), x) -> *#(i x, y),
         *#(*(i x, k(y, z)), x) -> *#(i x, z)}
       Weak:
       {          *(x, *(y, z)) -> *(*(x, y), z),
                      *(x, 1()) -> x,
                      *(x, i x) -> 1(),
                *(*(x, y), i y) -> x,
                *(*(x, i y), y) -> x,
          *(*(i x, k(y, z)), x) -> k(*(*(i x, y), x), *(*(i x, z), x)),
                      *(1(), y) -> y,
                      *(i x, x) -> 1(),
            *(k(x, y), k(y, x)) -> 1(),
                      i *(x, y) -> *(i y, i x),
                          i 1() -> 1(),
                          i i x -> x,
                        k(x, x) -> 1(),
                      k(x, 1()) -> 1(),
        k(*(x, i y), *(y, i x)) -> 1()}
       Open