Resolution refutation question confused I'm trying to solve this problem for my class. But now I'm so confused about the following question.  
*Consider the following statements:


*

*Every boy or girl is a child. 

*Every child gets a doll or a train or a lump of coal. 

*No boy gets a doll. 

*No child who is good gets a lump of coal. 


a. Use the predicates BOY, GIRL, CHILD, GET-DOLL, GET-TRAIN, GET-COAL and GOOD to represent these statements as predicate calculus formulas. 
b. Convert these statements to clauses. 
c. Use resolution refutation to prove that if no child gets a train, then no boy is good.* 
after first two-step, I can't prove the conclusion. One reason I think is that there is a girl function in the first clause, so I can't get an empty clause finally. The second reason is that I'm not sure whether I can use a clause many times to do the resolution refutation. Other similar questions are easy to prove by just using clause once and join them together, finally, I can get NIL or empty clause. But I can't prove this one. I don't know how to do.
The working step 01
The working step 02(Please ignore this, I think the goal is wrong in this image
==============
Goal and resolution refutation - 1(New version)
Goal and resolution refutation - 2(New version)
 A: Your goal is still not good. You treat the goal as being just one big universal statement, but the goal is a conditional between two universal statements:
$$\forall x_5 (CHILD(x_5) \to \neg GET-TRAIN(x_5)) \to \forall x_6 (BOY(x_6) \to \neg GOOD(x_6))$$
Negating that, you get:
$$\forall x_5 (CHILD(x_5) \to \neg GET-TRAIN(x_5)) \land \neg \forall x_6 (BOY(x_6) \to \neg GOOD(x_6))$$
And thus both:
$$\forall x_5 (CHILD(x_5) \to \neg GET-TRAIN(x_5))$$ 
and
$$\neg \forall x_6 (BOY(x_6) \to \neg GOOD(x_6))$$
the first one is easily clausified:
$$\neg CHILD(x_5) \lor \neg GET-TRAIN(x_5)$$ 
but for the second one you get:
$$\exists x_6 (BOY(x_6) \land GOOD(x_6))$$
Now, do you know what to do with an existential?
A: In formal logic I believe you can use a statement as many times as you like so long as it's derived or assumed (taken as an axiom) so if you have a statement at your disposal, you should be able to use it as many times as you like.  You need to think about what it means to negate a statement.
I believe you will need to create a formula for each of the 4 statements listed and join them with an AND connective. From what I just read on resolution refutation you should just need to cancel out conflicting terms as they appear.
I hope this helps.
