(VAR x y z)

(RULES
 .(1,x) -> x
 .(x,1) -> x
 .(i(x),x) -> 1
 .(x,i(x)) -> 1
 i(1) -> 1
 i(i(x)) -> x
 .(i(y),.(y,z)) -> z
 .(y,.(i(y),z)) -> z
)

(COMMENT Example 2 in \cite{D33})