YES
(THEORY
    (AC
        . +
    )
    
)
(VAR
    x1 x2
)
(RULES
    .(x1,x2) -> +(x2,x1)
    +(x1,1()) -> x1
    0() -> 1()
    +(1(),x1) -> x1
)