conjunctive normal form distribution over logical or?

Question

when converting to CNF do you have to distribute ors over ors ex. (A or B) or C, or can you leave it just like that I am wondering because I have to convert a bunch of first order logic to clausal form and then do resolution on it to find something out. It would be easier to leave it in the form (A or B) or C although I am a little uncertain about the resolution of C in that case or even the distributed case. thank you for your time

Answer 1

You don't distribute $\lor$'s over $\lor$'s. Rather, because of the associative property of $\lor$, which states that $(A \lor B) \lor C = A \lor (B \lor C)$, you can simply remove the parentheses completely:

$(A \lor B) \lor C = A \lor B \lor C$

and that is both in CNF and DNF