(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))
        
)