MAYBE
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:
  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),
    *#(*(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)}
  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()}
  EDG:
   {(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)), *#(*(i(x), k(y, z)), x) -> *#(i(x), z))
    (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), x))
    (i#(*(x, y)) -> *#(i(y), i(x)), *#(*(i(x), k(y, z)), x) -> *#(*(i(x), y), x))
    (i#(*(x, y)) -> *#(i(y), i(x)), *#(x, *(y, z)) -> *#(*(x, y), z))
    (i#(*(x, y)) -> *#(i(y), i(x)), *#(x, *(y, z)) -> *#(x, y))
    (*#(x, *(y, z)) -> *#(*(x, y), z), *#(*(i(x), k(y, z)), x) -> k#(*(*(i(x), y), x), *(*(i(x), z), x)))
    (*#(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) -> *#(i(x), y))
    (*#(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))
    (*#(x, *(y, z)) -> *#(*(x, y), z), *#(x, *(y, z)) -> *#(*(x, y), z))
    (*#(x, *(y, z)) -> *#(*(x, y), z), *#(x, *(y, z)) -> *#(x, y))
    (*#(*(i(x), k(y, z)), x) -> *#(i(x), y), *#(*(i(x), k(y, z)), x) -> k#(*(*(i(x), y), 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) -> *#(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), 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), y), *#(x, *(y, z)) -> *#(*(x, y), z))
    (*#(*(i(x), k(y, z)), x) -> *#(i(x), y), *#(x, *(y, z)) -> *#(x, y))
    (*#(*(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), 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) -> *#(i(x), y))
    (*#(*(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), x))
    (*#(*(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), *#(x, *(y, z)) -> *#(x, y))
    (*#(*(i(x), k(y, z)), x) -> *#(*(i(x), y), x), *#(x, *(y, z)) -> *#(x, y))
    (*#(*(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), *#(*(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), z), x))
    (*#(*(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))
    (*#(*(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), z), *#(x, *(y, z)) -> *#(x, y))
    (*#(*(i(x), k(y, z)), x) -> *#(i(x), z), *#(x, *(y, z)) -> *#(*(x, y), z))
    (*#(*(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), *#(*(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))
    (*#(*(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) -> k#(*(*(i(x), y), x), *(*(i(x), z), x)))
    (*#(x, *(y, z)) -> *#(x, y), *#(x, *(y, z)) -> *#(x, y))
    (*#(x, *(y, z)) -> *#(x, y), *#(x, *(y, z)) -> *#(*(x, y), z))
    (*#(x, *(y, z)) -> *#(x, y), *#(*(i(x), k(y, z)), x) -> *#(*(i(x), y), x))
    (*#(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, *(y, z)) -> *#(x, y), *#(*(i(x), k(y, z)), x) -> *#(i(x), z))
    (*#(x, *(y, z)) -> *#(x, y), *#(*(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))
    (i#(*(x, y)) -> i#(x), i#(*(x, y)) -> *#(i(y), i(x)))
    (i#(*(x, y)) -> i#(x), i#(*(x, y)) -> i#(x))
    (i#(*(x, y)) -> i#(x), i#(*(x, y)) -> i#(y))}
   SCCS:
    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:
     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()}
     SPSC:
      Simple Projection:
       pi(i#) = 0
      Strict:
       {i#(*(x, y)) -> i#(y)}
      EDG:
       {(i#(*(x, y)) -> i#(y), i#(*(x, y)) -> i#(y))}
       SCCS:
        Scc:
         {i#(*(x, y)) -> i#(y)}
        SCC:
         Strict:
          {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()}
         SPSC:
          Simple Projection:
           pi(i#) = 0
          Strict:
           {}
          Qed
    SCC:
     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()}
     Fail