Resolution and Substitution Exercise We are Given the Following Rules:
∀x∀y∀z(R(x,y)∧R(x,z))=>R(y,z)
∀x∀y(R(x,y)=>∃u(R(u,x)∧R(u,y))

Now the question is, Can we prove the following Rule?
∀x∀y(R(x,y)=>R(y,x))

It's a Multiple Choice question so the choices are:
a.True
b.False
c.Sometimes
d.It depends on Skolem constants' values.

The Book that contains this question says that the answer is True, But I can't figure it out.
What I've done so far is Turning the Rules into CNF so the first rule would Become:
1) $\neg R(x,y)\lor \neg R(x,z)\lor R(y,z)$
The Second one would become:
2) $\neg R(x_1,y_1)\lor R(f(x_1,y_1),x_1)$
3) $\neg R(x_2,y_2)\lor R(f(x_2,y_2),y_2)$
After that I'm Stuck, I can't Prove the rule mentioned in the question from the following three CNF rules using Substitution or Unification, Am I doing Something Wrong??
 A: You need to negate the conclusion and add it to your clauses. So, you get:
$\neg \forall x \forall y (R(x,y) \to R(y,x))$
which becomes:
$\exists x \exists y (R(x,y) \land \neg  R(y,x))$
and that gives you:
$R(c1,c2)$
and 
$\neg  R(c2,c1)$
So adding those to your clause set, you get:
$1. \neg R(x,y) \lor \neg R(x,z) \lor R(y,z)$
$2. \neg R(x1,y1) \lor R(f(x1,y1),x1)$
$3. \neg R(x2,y2) \lor R(f(x2,y2),y2)$
$4. R(c1,c2)$
$5. \neg R(c2,c1)$
and now you can resolve as follows:
$6. R(f(c1,c2),c1)  \ (2,4)$
$7. R(f(c1,c2),c2) \ (3,4)$
$8. \neg R(f(c1,c2),z) \lor R(c2,z) \ (1,7)$
$9. R(c2,c1) \ (6,8)$
$10. \bot \ (5,9)$
A: 

$\forall x~\forall y~\forall z~(R(x,y)\land R(x,z)\to R(y,z))$
$\forall x~\forall y~(R(x,y)\to ∃u~(R(u,x)∧R(u,y))$

Now the question is, Can we prove the following Rule?

$\forall x~\forall y~(R(x,y)\to R(y,x))$


Yes.  Moreover, we do not need to actually do so to know it may be done.
The first rule is that if any things have anything that is $R$-related to them, then they will be $R$-related to each other.   Note that conjunction is commutative.
The second rule is that any things $R$-related to each other will have some thing that is $R$-related to each of them.
So clearly the relation $R$ is symmetric.
That is all the reasoning that you need to answer such a multi-choice question.
