> I am stuck with figuring out what to do with the existential quantifier in the third premise. Let us have a quick look. You are aiming to derive `Gse` from the premises, so first use universal elimination on the third, and then... | Pd ⟷ (Hj & Mj) | Gsd | ∀x∀y∃z(((Gxy & (Py ➝ Pz)) & Rxyz) ➝ Gxz) | Pe ⟷ ∀x(Hx ➝ Mx) | Rsde |- | ∀y∃z(((Gsy & (Py ➝ Pz)) & Rsyz) ➝ Gsz) | ∃z(((Gsd & (Pd ➝ Pz)) & Rsdz) ➝ Gsz) … Nope, you cannot do anything else. You cannot establish that term `e` is a witness for that existential, and further you cannot derive that `Pd ➝ Pe` . You have no route to deriving `Gse` ; it simply is not entailed by these premises.