YES
(THEORY
    (AC
        or and
    )
    
)
(VAR
    x1 x2 x
)
(RULES
    and(x1,x2) -> not(or(not(x1)
                        ,not(x2)))
    not(not(x)) -> x
)