How to convert this formula to CNF

Question

I have the following formula and want to turn it into CNF without creating a truth table:

~((X -> ~(Y or Z)) and ((X and Y) or ~Z))

I was doing the following steps:

1. Remove Implication
2. Move negation inwards
3. Apply distributive laws

Then I get:

(((X and Y) or (X and Z)) or ((Z and ~X) or (Z and ~Y)))

But that is not CNF. What are the next steps to do so I will get a CNF?

Answer 1

\begin{gather} \neg((X \implies \neg(Y \lor Z)) \land ((X \land Y) \lor \neg Z)) \\ \neg ((\neg X \lor \neg (Y \lor Z)) \land ((X \land Y) \lor \neg Z)) \\ \neg (\neg X \lor \neg (Y \lor Z)) \lor \neg ((X \land Y) \lor \neg Z)\\ (X \land (Y \lor Z)) \lor ((\neg X \lor \neg Y) \land Z)\\ (X \lor (\neg X \lor \neg Y)) \land (X \lor Z) \land ((Y \lor Z) \lor (\neg X \lor \neg Y)) \land ((Y \lor Z) \lor Z) \\ (X \lor \neg X \lor \neg Y) \land (X \lor Z) \land (Y \lor Z \lor \neg X \lor \neg Y) \land (Y \lor Z \lor Z)&\text{already CNF}\\ 1 \land (X \lor Z) \land 1 \land (Y \lor Z)\\ (X \lor Z) \land (Y \lor Z) \end{gather} You could stop at line 6, but the CNF can be simplified further, as shown.