(VAR x y z )
(RULES 
        +(p1, p1) -> p2
        +(p1, +(p2, p2)) -> p5
        +(p5, p5) -> p10
        +(+(x, y), z) -> +(x, +(y, z))
        +(p1, +(p1, x)) -> +(p2, x)
        +(p1, +(p2, +(p2, x))) -> +(p5, x)
        +(p2, p1) -> +(p1, p2)
        +(p2, +(p1, x)) -> +(p1, +(p2, x))
        +(p2, +(p2, p2)) -> +(p1, p5)
        +(p2, +(p2, +(p2, x))) -> +(p1, +(p5, x))
        +(p5, p1) -> +(p1, p5)
        +(p5, +(p1, x)) -> +(p1, +(p5, x))
        +(p5, p2) -> +(p2, p5)
        +(p5, +(p2, x)) -> +(p2, +(p5, x))
        +(p5, +(p5, x)) -> +(p10, x)
        +(p10, p1) -> +(p1, p10)
        +(p10, +(p1, x)) -> +(p1, +(p10, x))
        +(p10, p2) -> +(p2, p10)
        +(p10, +(p2, x)) -> +(p2, +(p10, x))
        +(p10, p5) -> +(p5, p10)
        +(p10, +(p5, x)) -> +(p5, +(p10, x))
        
)