/home/nowonder/forschung/aprove/TPDB05/TRS/SK90/4.04.trs

The program

(VAR x y z)
(RULES
+(*(x,y),*(a,y)) -> *(+(x,a),y)
*(*(x,y),z) -> *(x,*(y,z))
)
(COMMENT Example 4.4 in \cite{SK90})