¬((x0 v x1) ^ x1) v x0) ¬x10 v x01 ((x100 ^ x11) <-> ¬(¬(x100 ^ x11) v ¬(x100 ^ x11))) <-> true (((x0 -> x1 -> ¬x1) <-> ¬x1)) <-> ¬false