Well. I wouldn't call this a mistake. But one thing that I would have done differently is the transformation of the inner ↔. For the outer one, you picked the CNF version. It generated two copies of the inner ↔. One with a negation, one without a negation. By replaying the inner ↔, one copy stays a CNF, the other one becomes a DNF. If you chose the DNF for the negated inner ↔, the negation would transform it to a CNF and your life would be easier.