Translation of english sentences to first order logic in conjunctive normal form walkthrough? I am having a hard time on a homework problem which involves converting a given English sentence into first order logic and then converting that into Conjunctive Normal Form. 
The sentences are (EDIT: Along with the entire problem statement)

Translate the following into First Order Logic and then convert to
  Conjunctive Normal Form (CNF):
According to the Pidgeon: If little girls eat eggs, then they are a kind of
  serpent. Alice (who is a little girl) eats eggs. Therefore, she is a kind of
  serpent.

I think I have done well so far below but I seem to be stuck trying to reduce the sentences any further, I am not sure what rule to apply from here. 

Hypothesis where L(x) = LittleGirl(x), E(x) = EatEggs(x), S(x) = Serpent(x)
{[∀x ((L(x) ∧ E(x)) ⇒ S(x))] ∧ [L(Alice) ∧ E(Alice)]} ⇒ S(Alice)

Implication: [A ⇒ B ≡ ¬A ∨ B] Applied to: L and E
{[∀x (¬(L(x) ∧ E(x)) ∨ S(x))] ∧ [L(Alice) ∧ E(Alice)]} ⇒ S(Alice)

Implication: [A ⇒ B ≡ ¬A ∨ B] Applied to: Pidgeon's final implication
¬{[∀x (¬(L(x) ∧ E(x)) ∨ S(x))] ∧ [L(Alice) ∧ E(Alice)]} ∨ S(Alice)

Universal Instantiation: [∀x P(x) ⇒ P(a/x)] Applied to: The only occurance
¬{[(¬(L(a/x) ∧ E(a/x)) ∨ S(a/x))] ∧ [L(Alice) ∧ E(Alice)]} ∨ S(Alice)

DeMorgan's Law: [¬(A ∧ B) ≡ ¬A ∨ ¬B, ¬(A ∨ B) ≡ ¬A ∧ ¬B] Applied to: Statement in brackets
¬[(¬(L(a/x) ∧ E(a/x)) ∨ S(a/x))] ∨ ¬[L(Alice) ∧ E(Alice)] ∨ S(Alice)

DeMorgan's Law: [¬(A ∧ B) ≡ ¬A ∨ ¬B, ¬(A ∨ B) ≡ ¬A ∧ ¬B] Applied to: a/x statement
(¬¬(L(a/x) ∧ E(a/x)) ∧ ¬S(a/x)) ∨ ¬[L(Alice) ∧ E(Alice)] ∨ S(Alice)

DeMorgan's Law: [¬(A ∧ B) ≡ ¬A ∨ ¬B, ¬(A ∨ B) ≡ ¬A ∧ ¬B] Applied to: Middle statement
(¬¬(L(a/x) ∧ E(a/x)) ∧ ¬S(a/x)) ∨ ¬L(Alice) ∨ ¬E(Alice) ∨ S(Alice)

Double negation elimination: [¬¬A ≡ A] Applied to: Left statement
((L(a/x) ∧ E(a/x)) ∧ ¬S(a/x)) ∨ ¬L(Alice) ∨ ¬E(Alice) ∨ S(Alice)


Though after doing some reading I think that I might have done this wrong. After reviewing this webpage describing Universal Instantiation I feel like I could apply its example problem directly to mine. I could have initially applied Universal Instantiation and then Modus ponens to have simply ended with Serpent(Alice) which is in CNF. But this feels like I am "cheating" the problem, or is this most likely the solution the professor seeks for the question?
Am I on the right track above or should I try applying the example from the website to my problem? If I am on the right track what rule might I apply next (specifically to the top statement) to continue?
 A: One immediate problem I see is that hou have three sentences (making up 1 argument), but you treat this as 1 sentence.  Instead, you should put each of the three sentences in CNF by themselves.
Second, you say to put the sentences in CNF, but the first sentence involves a quantifier. Does this mean that you just have to put the body in CNF and leave the quantifier? Or are you doing the preprocessing to use resolution? I get the feeling you are ...
Anyway, let's take that first sentence, and do some algebraic manipulation:
$\forall x ((L(x) \land E(x)) \rightarrow S(x)) \Leftrightarrow$ (Implication)
$\forall x (\neg (L(x) \land E(x)) \lor S(x)) \Leftrightarrow$ (DeMorgan)
$\forall x (\neg L(x) \lor \neg E(x) \lor S(x))$
And now the body is in CNF.  If you have to get rid of the unatifier in preparation of resolution, you just drop it and get:
$\neg L(x) \lor \neg E(x) \lor S(x)$
The second statement is already in CNF:
$L(a) \land E(a)$
And again , assuming you are setting this up for resolution (which is a consistency checking method), you should negate the conclusion ... Which is also in CNF:
$\neg S(a)$
This gives you 4 clauses:


*

*$\{ \neg L(x) , \neg E(x) , S(x) \}$

*$\{ L(a) \}$

*$\{ E(a) \}$

*$\{ \neg S(a)\}$
And now we ca resolve:


*$\{ \neg E(a), S(a) \}$ 1,2

*$\{ S(a) \}$ 3,5

*$\{ \}$ 4,6
Contradition, so the original argument is valid!
