Help with predicate logic

I'm trying to figure out how to do this problem and I was wondering if anyone on here knew how to solve it.


1. ((∀x-Fx v ∀xGx) v -(∀xKx → -∃y∀z∃w-Dyzw)) & ((∀xFx & ∀x-Gx) v (∃xKx → ∀y∃z∀wDyzw))

├ ∀x(((Fx → Gx) → (Kx → ∀y∃z∀wDyzw)) & ((∃y∀z∃w-Dyzw → -Kx) → (-Gx → -Fx)))



Thanks if anyone can.