YES
(THEORY
    (AC
        f
    )
    
)
(VAR
    x1 x
)
(RULES
    f(one(),x1) -> x1
    f(x,one()) -> x
)