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