An inference in predicate logic that has to be established using resolution method

Question

I have been struggling with breaking down this logic problem with the use of resolution method. Below is what i have done. I feel it is incorrect and humbly need your assistance. Thanks

Problem: ∃x(p(x) → q(x)) → ¬∀xp(x) |= ∃x ¬p(x)

What i have done.

¬∀xp(x)

∃x¬p(x)

¬p(a)

∃x(¬p(x) ∨ q(x)) → ∀xp(x)

¬∃x(¬p(x) ∨ q(x)) ∨ ∀xp(x)

∀x¬(¬p(x) ∨ q(x)) ∨ ∀xp(x)

∀x (p(x) ∧ ¬q(x)) ∨ ∀xp(x)

∀x∀y(p(x) ∧ ¬q(x)) ∨ p(y))

(p(x) ∧ ¬q(x)) ∨ p(y)

(p(x) ∨ p(y)) ∧ (¬q(x) ∨ p(y))

p(x), p(y) ←, p(y)←q(x), ← p(a)

p(x), p(y) ←, ← p(a)

p(y) ←, ← p(a)

←

Answer 1

Let $p(x)\equiv x=x$ and $q(x)\equiv x\ne x$. Then clearly $p(x)\to q(x)$ is false for all $x$, i.e., there is no $x$ with $p(x)\to q(x)$, i.e., $\exists x(p(x)\to q(x))$ is false, hence $\exists x(p(x)\to q(x))\to\text{whatever}$ is true. You will however hardly be able to prove $\exists x\neg p(x)$.