(VAR x y z )
(RULES 
        *(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
        
)