(VAR x y z )
(RULES 
        +(*(x, y), *(x, z)) -> *(x, +(y, z))
        +(+(x, y), z) -> +(x, +(y, z))
        +(*(x, y), +(*(x, z), u)) -> +(*(x, +(y, z)), u)
        
)