MAYBE

Problem:
 *(x,1()) -> x
 *(1(),y) -> y
 *(i(x),x) -> 1()
 *(x,i(x)) -> 1()
 *(x,*(y,z)) -> *(*(x,y),z)
 i(1()) -> 1()
 *(*(x,y),i(y)) -> x
 *(*(x,i(y)),y) -> x
 i(i(x)) -> x
 i(*(x,y)) -> *(i(y),i(x))
 k(x,1()) -> 1()
 k(x,x) -> 1()
 *(k(x,y),k(y,x)) -> 1()
 *(*(i(x),k(y,z)),x) -> k(*(*(i(x),y),x),*(*(i(x),z),x))
 k(*(x,i(y)),*(y,i(x))) -> 1()

Proof:
 DP Processor:
  DPs:
   *#(x,*(y,z)) -> *#(x,y)
   *#(x,*(y,z)) -> *#(*(x,y),z)
   i#(*(x,y)) -> i#(x)
   i#(*(x,y)) -> i#(y)
   i#(*(x,y)) -> *#(i(y),i(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),y),x)
   *#(*(i(x),k(y,z)),x) -> k#(*(*(i(x),y),x),*(*(i(x),z),x))
  TRS:
   *(x,1()) -> x
   *(1(),y) -> y
   *(i(x),x) -> 1()
   *(x,i(x)) -> 1()
   *(x,*(y,z)) -> *(*(x,y),z)
   i(1()) -> 1()
   *(*(x,y),i(y)) -> x
   *(*(x,i(y)),y) -> x
   i(i(x)) -> x
   i(*(x,y)) -> *(i(y),i(x))
   k(x,1()) -> 1()
   k(x,x) -> 1()
   *(k(x,y),k(y,x)) -> 1()
   *(*(i(x),k(y,z)),x) -> k(*(*(i(x),y),x),*(*(i(x),z),x))
   k(*(x,i(y)),*(y,i(x))) -> 1()
  Open