How do I use rules of inferences to imply a conclusion from 4 premises?

Question

I am a little confused on how to use 4 premises to prove a conclusion. Can you please tell me if my logic is sound for the following proof:

1) ∀x[C(x) ∨ M(x)]
2) ∀x[¬M(x) ∨ N(x)]
3) ∀x[J(x) → ¬N(x)]
4) ∃x¬C(x)
∴ ∃x¬J(x)

5) C(a) ∨ M(a) Universal instantiation on 1
6) ¬M(a) ∨ N(a) Universal Instantiation on 2
7) C(a) ∨ N(a) Resolution on 5 and 6
8) J(a) → ¬N(a) Universal Instantiation on 3
9) ¬C(a) Existential Instantiation on 4
10) N(a) Disjunctive Syllogism on 7
11) ¬J(a) Modus tollens on 8
12) ∃x¬J(x) Existential Generalization

Answer 1

You'll need to invoke existential instantiation on line $(4)$ before invoking any universal instantiation for the proof to work.

But otherwise, you've got the main gist of how to work with the premises to derive the conclusion