semantic tableaux - can't show sequent is valid

Question

I have the sequent

$\forall x\forall y(Rxy\to(Fx\lor Gy)), \forall x(Fx\to Gx) \vdash \forall x(Gx\lor \exists\lnot Ryy)$

I have tried several different ways, and I know all branches are supposed to close, but some remain open after using all the formulas in the sequent. Can anyone help?

Thanks!!

Answer 1

1) $∀x∀y(Rxy→(Fx∨Gy))$

2) $∀x(Fx→Gx)$

3) $\lnot ∀x(Gx∨∃¬Ryy)$

4) $\lnot (Ga∨∃¬Ryy)$ --- from 3) : $a$ new

5) $\lnot Ga$

6) $\lnot ∃¬Ryy$

7) $Raa$ --- from 6)

8) $Fa \to Ga$ --- from 2)

Branch :

$9_L) \ \lnot Fa$ --- from 8)

$9_R) \ Ga$ --- closes with 5) : $X$

$10) \ Raa \to (Fa \lor Ga)$ --- from 1)

Branch :

$10_L) \ \lnot Raa$ --- closes with 7) : $X$

$10_R) \ Fa \lor Ga$

Branch :

$11_L) \ Fa$ --- closes with $9_L)$ : $X$

$11_R) \ Ga$ --- closes with 5) : $X$.