I have to prove using the resolution method that :
$\varphi_1,\varphi_2,\varphi_3 \models \varphi_4 $ where:
$\varphi_1 = \exists z\, \forall x\, ( \forall y\, (q(g(x),y) \vee p(z,g(x))) $
$\varphi_2 = \exists z\, \forall y\, ( p(y,g(g(y)) \rightarrow \forall x\, q(x, g(z))) $
$\varphi_3 = \forall x\, \forall y\, ( r(x, g(y)) \rightarrow (r(g(y),x) \vee \neg \exists x\, \exists y\, r(x,y))) $
$\varphi_4 = \exists z\, ( \exists x\, q(g(x), z) \wedge \exists x\, q(z,x)) $
I know that I have to use the method on $\varphi_1 \wedge \varphi_2 \wedge \varphi_3 \wedge \neg \varphi_4 $, but from there on I have no idea what to do. Any help is welcomed :)