We have to prove:

with no assumptions.

Proof by sequent calculus with unit propagation:

Equivalence goal MouseOver is proven in both directions.

{1} Direction from left to right: Assume:

and prove:

Assumed conjunction MouseOver is split into:

Implicative goal MouseOver is split. Assume:

and prove:

Literal goal MouseOver is propagated !

Using literal goal MouseOver, assumption MouseOver is simplified to:

Literal assumption MouseOver is propagated !

Using literal assumption MouseOver, assumptions MouseOver and MouseOver are simplified to:

Contradictory assumptions MouseOver, MouseOver: success.

{2} Direction from right to left: Assume:

and prove:

Conjunctive goal MouseOver is decomposed on different proof branches.

{2, 1} Proof of MouseOver:

Implicative goal MouseOver is split. Assume:

and prove:

Literal assumption MouseOver is propagated !

Using literal assumption MouseOver, assumption MouseOver is simplified to:

Assumed MouseOver goal MouseOver: success.

{2, 2} Proof of MouseOver:

Implicative goal MouseOver is split. Assume:

and prove:

Literal assumption MouseOver is propagated !

Using literal assumption MouseOver, assumption MouseOver is simplified to:

Literal assumption MouseOver is propagated !

Literal goal MouseOver is propagated !

Formula is invalid. Counterexample: A->False, B->True, and C->True.