I find very confusing to understand how combined qualifiers might expand on a tableaux. While for $\exists x\ p(x)$, I would just create a new term, a, and for $\forall x\ p(x)$ I would use an existing one, I find it very confusing what should happen when mixing both.
So I drew this table. Am I correct in saying the the third one will stop and the fourth won't? Am I missing some other edge cases?
Yes, you run out of steps to use in case 3, but the branch in case 4 can go on for ever.
But to be pernickety (just in case your mode of presentation does indeed represent your thinking) ...
No, no, no, you never instantiate two quantifiers at once in a tableau (which is what you seem to be doing). You are only allowed, at a given step, to instantiate the outermost quantifier. Look at the rules (in my logic text or any other tableau-based textbook).
So if a wff is of the form $\forall x\varphi(x)$ then you instantiate with a new name $a$ to derive $\varphi(a)$ -- and that still applies if $\varphi$ itself starts with a quantifier. Once you have $\varphi(a)$ you then apply whatever rule is now appropriate.
Thus the tableau might go
$$\forall x\exists y Rxy$$ $$\exists yRay$$ $$ Rab$$ And now you could (if you want) continue $$\exists yRby$$ $$ Rbc$$ But the intervening steps (not indicated in any way in your trees) are essential.