#automated-reasoning

Let $\vee$ be a commutative and associative binary operation and $\neg$ a unary operation on a set, satisfying Robbins's equation $\neg (\neg (a\vee b)\vee \neg (a\vee \neg b))=a$ for all $a,b$. Prove that the structure is a Boolean algebra, or find a counterexample.