It's very close. I put your proof into formal form to work it out.
The initial problem that I see is that PvQ cnanot be inferred from ~ (~Pv~Q). Negation elimination (also called double negation) states ~~P can replace or be replaced by P. It's like saying P is the same as not not P. The main problem is that even if you negate 1, you are still left with the same formula, only with redundant negations tied on. For 3 and 4, disjunction elimination requires 3 elements to derive a result. There needs to be;
2 R -->S
3 P v R__
Q v S
If you are looking at wiki for the definition of disjunction elimination Disjunction elimination - Wikipedia, the free encyclopedia
, it is both right and wrong. Yes, it does follow the same structure as constructive dilemma (the term I use for the same inference), but they infer that from the conclusion of 2 and 3, you can get one variable (i.e. C). This is not the case and it is very misleading. You must infer a disjunction of the conclusion of the second line and the third line to derive the full inference (i.e. Q v S).
In order to separate any variable the way you want to in line #2, it must be a conjunction rather than a disjunction. Otherwise it must have negated antecedent to set up the inference ( i.e. it must follow the form of a disjunctive syllogism).
As for solving the proof, it is difficult to do so because you have a completely negated statement. You basically say " It is not the case that either not Paul or not Quincy swimming in the pool." Actually, it is quite paradoxical if you think about it. This in a way seems like a variation the liars paradox. If it is not the case that neither Paul nor Quincy is in the pool, this means that they are actually swimming in the pool. If you had more premises in your argument, you could give it a whirl. By itself, the only way I could see it being solved is either by indirect or conditional proof. Essentially, you would have to begin the proof with an assumed premise and either assume ~P, derive a contradiction, and end the indentation by asserting P or
construct a conditional sentence , assume P, derive Q, and assert P-->Q. Its either those two inference rules or go into quantifier logic, which does not really apply well in this case. But indirect proof would probably be your best bet. You can assume ~P, add ~Pv~Q, but then that is where you will get hung up.