The question is: "How would one go about working with negations of quantifiers in scenarios as the one above?"
I will provide two proofs which may help answer the question. The first will be an indirect proof similar to the attempt in the OP. The second will be more direct.
Here is the first proof:
The premises are on the first two lines. On the third line I assume the negation of what I want to show to get a contradiction. I reach the desired contradiction on line 9 which leads to the completion of the proof on line 10.
On line 4 I use the second premise. On line 5 I use the first premise. These quickly generate a contradiction.
The second proof is more direct.
The first two lines are the premise. In line 3 I start the process to complete existential elimination. To do that I have to make an assumption which will be discharged on line 15 allowing existential elimination.
Using the first premise I consider the two cases "Ra" and "Sa". I want both cases to give me (1) the same result and (2) a result I can use. The result I want is "¬¬Sa". Having those double negatives allows me to introduce an existential quantifier and then with a conversion of quantifiers move one of those negations to the outside of a universal quantifier.
For more information on how these rules work, associated with the proof checker I used, see forall x: Calgary Remix.
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/