Translate the following axioms to predicate calculus:
 
1. Every child loves Santa.
   Ax child(x) -> loves(x,Santa)
2. Everyone who loves Santa loves any raindeer.
   Ax,y loves(x,Santa) ^ reindeer(y) -> loves(x, y)
3. Rudolph is a raindeer, Rudolph has a red nose.
   reindeer(Rudolph) ^ rednose(Rudolph)
4. Anything which has a red nose is weird or is a clown.
   Ax rednose(x) -> weird(x) V clown(x)
5. No raindeer is a clown.
   Ax Reindeer(x) -> -clown(x)
6. Scrooge does not love anything that is weird.
   Ax weird(x) -> -loves(Scrooge, x)

Transform them to clause form

 1. -child(x) V loves(x,Santa)
 2. -loves(z,Santa) V -reindeer(y) V loves(z,y)
 3a. reindeer(Rudolph)
 3b. rednose(Rudolph)
 4. -rednose(w) V weird(w) V clown(w)
 5. -reindeer(u) V -clown(u)
 6. -weird(v) V -loves(Scrooge, v)

To prove using resolution that "Scrooge is not a child."  add the negation 
of what we want to prove to the knowledge base and find a contraddiction

 7.  child(Scrooge)

Resolution steps:

resolve 3a with 5 {u/Rudolph}
  and obtain 8. -clown(Rudolph)
resolve 8 with 4  {w/Rudolph}
  and obtain 9. -rednose(Rudolph) V weird(Rudolph)
resolve 3b with 9 
  and obtain 10. weird(Rudolph)
resolve 10 with 6 {v/Rudolph}
  and obtain 11. -loves(Scrooge, Rudolph)
resolve 11 with 2 {z/Scrooge, y/Rudolph}
  and obtain 12. -loves(Scrooge,Santa) V -reindeer(Rudolph) 
resolve 12 with 1 {x/Scrooge}
  and obtain 13. -child(Scrooge) V -reindeer(Rudolph)
resolve 13 with 3a 
  and obtain 14. -child(Scrooge)
resolve 14 with 7 
  and obtain NIL

This is not the only way to prove the result by resolution.  Here is
another proof:

resolve 7 with 1 {x/Scrooge}
  and obtain 8. loves(Scrooge,Santa)
resolve 8 with 2 {z/Scrooge}
  and obtain 9. -reindeer(y) V loves(Scrooge,y)
resolve 3a with 9 {y/Rudolph}
  and obtain 10. loves(Scrooge, Rudolph)
resolve 10 with 6 {v/Rudolph}
  and obtain 11. -weird(Rudolph)
resolve 11 with 4 {w/Rudolph}
  and obtain 12. -rednose(Rudolph) v clown(Rudolph)
resolve 12 with 3b 
  and obtain 13. clown(Rudolph)
resolve 13 with 5 {u/Rudolph}
  and obtain 14. -reindeer(Rudolph)
resolve 14 with 3a 
  and obtain NIL