Proving the statement using Resolution?

Question

I'm trying to solve this problem for my logical programming class:

Every child loves Santa. Everyone who loves Santa loves any reindeer. Rudolph is a reindeer, and Rudolph has a red nose. Anything which has a red nose is weird or is a clown. No reindeer is a clown. John does not love anything which is weird. (Conclusion) John is not a child.

Here is my theory:

1. K(x) => L(x,s)                  % Every child loves Santa
2. L(x,s) => ( D(y) => L(x,y) )    % Everyone who loves Santa loves any reindeer
3. D(r) & R(r)                     % Rudolph is a reindeer, and Rudolph has a red nose.
4. R(x) => ( W(x) v C(x) )         % Anything which has a red nose is weird or is clown
5. ~( D(x) & C(x) )                % No reindeer is a clown.
6. W(x) => ~L(j,x)                 % John does not love anything which is weird.
7. ?=> ~K(j)                       % John is not a child?

Here are the clauses in CNF:

1. ~K(x) v L(x,s)
2. ~L(x,s) v ~D(y) v L(x,y)
3. D(r)
4. R(r)
5. ~R(x) v W(x) v C(x)
6. ~D(x) v ~C(x)
7. ~W(x) v ~L(j,x)
8. K(j)

I cannot seem to get an empty statement by Resolution. Is there a mistake in my theory or the conclusion indeed does not follow?

Edit: Resolution

[3,6]   9.  ~C(r)
[4,5]   10. W(r) v C(r)
[9,10]  11. W(r)
[8,1]   12. L(j,s)
[12,2]  13. ~D(y) v L(j,y)
[11,7]  14. ~L(j,r)
[13,14] 15. ~D(r)

Thank you for your help!

Answer 1

The conclusion is correct.

I will let you tidy this up and fill in the gaps, but you might want to consider the following

W(r) v C(r)
W(r)
~L(j,r)
~L(j,s)
~K(j)