(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
)
(COMMENT Example 4.2 (Commutator) in \cite{SK90})