truth tree

[SVEN11]

Hi!
I have been trying to solve the following semantic tree in first order predicate logic, and could use some help regarding the variables and constants. (sorry by quantifiers, but I could only type them with letter).

-(Ey)(Ex)Syx, (Vy)(Vx)(Rxy --> Sxy) ╞ (Vx)(Vy)-Ryx


-(Ey)(Ex)Syx

(Vy)(Vx)(Rxy --> Sxy)

-(Vx)(Vy) -Ryx


(Vy) -(Ex)Syx

-(Ex)Syx

(Vx)-Syx

 -Sba


(Ex)-(Vy)-Ryx

-(Vy)-Ryx

(Ey)- -Ryx

Rdc


(Vx)(Rxy --> Sxy)

(Rxy --> Sxy)

-Rcd Sab
X X

What confuses me are, that the variables in (Vx)-Syx need to be replaced with ba. But must I write dc to replace (Ey)- -Ryx, or can I write ba again?

Further, are the tree correct, and valid.

[Blaggard]

Can you put it in the form of a sentence in language? It's a nice homework question and you clearly have worked out much of it to some extent. But I doubt anyone regardless of their formal and predicate logic skills is going to answer that. That said ironically the fact that I just said that may lead someone to try, so glad to "help".