Deduction problem in first order logic

Greetings to everybody.

I have tried to solve this problem about deduction in first order logic
unsuccessfully.

Let G be a the set which comprises the formulas:

AxAyAzAuAvAw(P(x,y,u) & P(y,z,v) & P(x,v,w) --> P(u,z,w))

AxAyEz(P(z,x,y))

AxAyEz(P(x,z,y))

And let F be the formula ExAy(P(y,x,y))

A and E stand for the universal and existencial quantifiers,
respectively. & stands for the AND conective, --> stands for the IF
conective and P is a 3-place predicate symbol of the first order
language L considered.

I want to know if G entails F. As said before, I have tried to prove or
disprove it unsuccessfully. But what I want is a formal proof of the
above by means of resolution method, in case G entails F, or by giving
a subset of the Herbrand's base of L in case G does not entail F.

As usual, thanks to all posts in advance.

.