Predict Logic Exercise I have a question regarding Resolution and Substitution 
We are Given the following rules 
∀x∀y(p(x,y)=>∃z q(x,y,z))
∃x∀y∀z(r(y,z) <=> q(x,y,z))
∀x∃y (¬p(x,y) => ∀z q(x,y,z))

The question is, Can we prove this Rule
∃w ∃x ∃y ∃z ( r(x,y) ∧ q(x,w,z))

and we have these choices 
1.true
2.false
c.Sometimes
d.It depends on Skolem constants' values.

at the beginning I know I must start with 
¬(∃w ∃x ∃y ∃z ( r(x,y) ∧ q(x,w,z)))

so it will become 
∀w ∀x ∀y ∀z ¬(r(x,y) ∧ q(x,w,z))
∀w ∀x ∀y ∀z (¬r(x,y) V ¬q(x,w,z))
¬r(x,y) V ¬q(x,w,z)

and then I should convert the given rules into CNF so we will have the following rules 
1-  ¬p(x,y) V q(x,y,f(x,y))
2-  ¬r(y1,z1) V q(C1,y1,z1)
3-  ¬q(C1,y2,z2) V r(y2,z2)
4-  p(x3,f(x3)) V q (x3,f(x3),z3)
5-  ¬r(x4,y4) V ¬q(x4,w4,z4)

the answer is true, but I cannot prove that I feel like I am stuck 
so what is the right way to solve this question and get the correct answer?
 A: My Answer would be:
1-  ¬p(x,y) V q(x,y,f1(x,y))
2-  ¬r(y1,z1) V q(C1,y1,z1)
3-  ¬q(C1,y2,z2) V r(y2,z2)
4-  p(x3,f2(x3)) V q (x3,f2(x3),z3)
5-  ¬r(x4,y4) V ¬q(x4,w4,z4)

from (1,4) :
q (x3,f2(x3),z3) V q(x3,f2(x3),f1(x,f2(x3))) [x3|x ,f2(x3)|y]

then if we substitute [f1(x,f2(x3))|z3] we get:
6- q (x3,f2(x3),f1(x,f2(x3)))
7- ¬p(C1,y2) V r(y2,f1(C1,y2)) (1,3) [C1|x,y2|y,f1(C1,y2)|z2]
8- ¬r(x3,y4) (5+6) [x3|x4,f2(x3)|w4,f1(x,f2(x3))|z4]
9- q(C1,f2(C1),z3) V r(f2(C1),f1(C1,f2(C1))) (7,4) [C1|x3,f2(C1)|y2]

then if we try (9,3):
r(f2(C1),z3)V r(f2(C1),f1(C1,f2(C1))) [f2(C1)|y2,z3|z2]

then we substitute f1(C1,f2(C1))|z3 so we get:
10- r(f2(C1),f1(C1,f2(C1)))

finally:
11-⊥ (10,8)

A: First, a small correction: make sure to use a new skolem function if needed. So, you should get:
\begin{array}{ll}
1- & \neg p(x,y) \lor  q(x,y,f_2(x,y))\\
2- & \neg r(y_1,z_1) \lor q(c_1,y_1,z_1)\\
3- & \neg q(c_1,y_2,z_2) \lor r(y_2,z_2)\\
4- & p(x_3,f_1(x_3)) \lor q(x_3,f_1(x_3),z_3)\\
5- & \neg r(x_4,y_4) \lor \neg q(x_4,w_4,z_4)\\
\end{array}
Continue with:
\begin{array}{llll}
6. & q(x,f_1(x),f_2(x,f_1(x))) & (1,4) & [x/x_3,f_1(x)/y,f_2(x,f_1(x))/z_3]\\
7. & r(f_1(c_1),f_2(c_1,f_1(c_1))) & (3,6) & [c_1/x,f_1(c_1)/y_2, f_2(c_1,f_1(c_1))/z_2]\\
8. & \neg r(x,y_4) & (5,6) & [x/x_4,f_1(x)/w_4,f_2(x,f_1(x))/z_4]\\
9. & \bot & (7,8) & f_1(c_1)/x, f_2(c_1,f_1(c_1))/y_4]\\
\end{array} 
