Transforming a formula into clausal form

Question

I've been having some difficulty in transforming the following formula to a clausal form:

$\forall x(biker(x) \to \exists y((harley(y) \lor bmw(y)) \land rides(x,y)))$

I've taken the following steps:

1. $\forall x(\lnot biker(x) \lor \exists y((harley(y) \lor bmw(y)) \land rides(x,y)))$

2. $\forall x \exists y(\lnot biker(x) \lor ((harley(y) \lor bmw(y)) \land rides(x,y)))$

3. $\forall x \exists y(\lnot biker(x) \lor ((harley(y) \lor bmw(y)) \land rides(x,y)))$

4. $\forall x \exists y(\lnot biker(x) \lor (harley(y) \land rides(x,y)) \lor(bmw(y) \land rides(x,y))$

But 4 is not in CNF and I don't know how to proceed. How can I form clauses out of this? Did I make a wrong transformation or can I distribute 4 into something else?

Answer 1

You merely distributed the wrong way in the last line.

Instead, from line 3, distribute $\vee$ over $\wedge$. IE. the form: $p\vee(q\wedge r)=(p\vee q)\wedge(p\vee r)$

$$4'.~~\forall x\exists y~((\neg \operatorname{biker}(x)\vee \operatorname{harley}(y)\vee \operatorname{bmw}(y))\wedge (\neg\operatorname{biker}(x)\vee\operatorname{rides}(x,y)))$$