I need help with the following question:

I need help with the following question on Resolution in predicate logic:

The custom officials searched everyone who entered this country who was not a VIP. Some of the drug pushers entered this country and they were only searched by drug pushers. No drug pushers was a VIP. Let E(x) mean ”x entered this country”, V (x) mean ”x was a VIP, S(x, y) mean ”y searched x”, C(x) mean ”x was a custom official”, and P(x) mean ”x was a drug pusher”. Use these predicates to express the above statements in first order logic. Conclude by resolution that some of the officials were drug pushers.

I first tried to translate the sentences to the language of FOL as follows:

1.The custom officials searched everyone who entered this country who was not a VIP

∀x (E(x) /\ ¬V(x)) ----> ∃y (C(y) /\ S(x,y)

2. Some of the drug pushers entered this country and they were only searched by drug pushers.

∃x (P(x) /\ E(x)) /\ ∃y (S(x,y) /\ P(y)

3. No drug pushers was a VIP

∀x V(x) ---> ¬P(x)

4. some of the officials were drug pushers(conclusion)

∃x C(x) /\ P(x)

Since I want to go through resolution, the next step, as long as I know, is to convert the above sentences one by one to Conjunction Normal form (CNF), and then remover the quantifiers, before doing resolution. I tried for each sentence, though it was quite unsuccessful:

a) First i need to remove the implication:

Sentence1. ∀x (E(x) /\ ¬V(x)) ----> ∃y (C(y) /\ S(x,y)

a) First i need to remove the implication:

∀x ¬(E(x) /\ ¬V(x)) \/ ∃y (C(y) /\ S(x,y) //by Implication elimination

∀x (¬E(x) /\ V(x)) \/ ∃y (C(y) /\ S(x,y) //by Implication elimination

b) Now I need to remove the quantifiers by introducing constants:

(¬E(P) /\ V(P)) \/ ∃y (C(Q) /\ S(P,Q) //Not sure at all ...

c) now i need to convert to CNF, but instead i have DNF, disjunction of two sentence.

Sentence 2. ∃x (P(x) /\ E(x)) /\ ∃y (S(x,y) /\ P(y)

a) what i need is to remove existential, but i am really not sure.

Sentence 3. ∀x V(x) ---> ¬P(x)

a) ∀x ¬ V(x) \/ P(x) // Implication elimination

b) again existential elimination which i don't know how...

sentence 4. ∃x C(x) /\ P(x)

a) existential elimination is required...

I really appreciate if you please help me to convert them to CNF and removing quantifiers.