(VAR Z X Y)
(RULES
f(i(Z),f(X,f(Y,Z))) → f(X,Y)
f(i(Z),f(X,f(Z,Y))) → f(X,Y)
f(X,f(i(X),Y)) → Y
f(i(X),X) → unit
f(Z,f(X,f(Y,i(Z)))) → f(X,Y)
f(Z,f(X,f(i(Z),Y))) → f(X,Y)
f(unit,X) → X
f(f(X,Y),Z) → f(X,f(Y,Z))
i(unit) → unit
f(X,i(X)) → unit
i(i(X)) → X
f(Y,f(X,i(Y))) → X
f(X,unit) → X
i(f(X,Y)) → f(i(X),i(Y))
f(i(Y),f(X,Y)) → X
)(EQUATIONS →
f(X,Y) = f(Y,X) →
f(X,f(Y,Z)) = f(Y,f(X,Z)) →
)

(VAR )
(RULES
→
)(EQUATIONS →
f(X,Y) = f(Y,X) →
)

(VAR X Y Z)
(RULES
f(f(X,Y),Z) → f(X,f(Y,Z))
)(EQUATIONS →
f(X,Y) = f(Y,X) →
f(X,f(Y,Z)) = f(Y,f(X,Z)) →
)

(VAR X Y Z)
(RULES
f(unit,X) → X
f(f(X,Y),Z) → f(X,f(Y,Z))
f(X,unit) → X
)(EQUATIONS →
f(X,Y) = f(Y,X) →
f(X,f(Y,Z)) = f(Y,f(X,Z)) →
)

(VAR X Y Z)
(RULES
f(X,f(X,Y)) → Y
f(X,X) → unit
f(X,unit) → X
f(Y,f(X,Y)) → X
f(unit,X) → X
f(f(X,Y),Z) → f(X,f(Y,Z))
)(EQUATIONS →
f(X,Y) = f(Y,X) →
f(X,f(Y,Z)) = f(Y,f(X,Z)) →
)

(VAR X Y Z)
(RULES
plus(X,X) → zero
plus(Y,plus(Y,X)) → X
mult(X,plus(Y,Z)) → plus(mult(X,Y),mult(X,Z))
plus(X,zero) → X
mult(X,mult(X,Y)) → mult(X,Y)
plus(Z,plus(X,plus(Y,Z))) → plus(X,Y)
plus(Z,plus(X,plus(Z,Y))) → plus(X,Y)
plus(Y,plus(X,Y)) → X
mult(mult(X,Y),Z) → mult(X,mult(Y,Z))
plus(plus(X,Y),Z) → plus(X,plus(Y,Z))
mult(X,one) → X
mult(Y,mult(X,Y)) → mult(X,Y)
plus(zero,X) → X
mult(plus(X,Z),Y) → plus(mult(X,Y),mult(Z,Y))
mult(zero,X) → zero
mult(X,X) → X
mult(X,zero) → zero
mult(one,X) → X
)(EQUATIONS →
mult(X,mult(Y,Z)) = mult(Y,mult(X,Z)) →
plus(Y,plus(X,Z)) = plus(X,plus(Y,Z)) →
→
plus(X,Y) = plus(Y,X) →
mult(Y,X) = mult(X,Y) →
)

(VAR )
(RULES
→
)(EQUATIONS →
f(X,f(Y,Y)) = f(f(Y,Y),X) →
f(f(Y,Y),X) = f(X,f(Y,Y)) →
)