Prove $P \lor Q, P \rightarrow R \lor S, R \rightarrow W \land Z, Z \land \lnot S \rightarrow \lnot W \vdash \lnot S \rightarrow Q$ using ND The problem is to prove
$$P \lor Q, P \rightarrow R \lor S, R \rightarrow W \land Z, Z \land \lnot S \rightarrow \lnot W \vdash \lnot S \rightarrow Q$$
using natural deduction.

I'm studying natural deduction for my upcoming exam in Logic and I have come across this problem. Unfortunately, I cannot seem to find a path to its solution. What I have done is the following and I don't know how to proceed any further:


  
  $P \lor Q$
  $P \rightarrow R \lor S$
  $R \rightarrow W \land Z$
  $Z \land \lnot S \rightarrow \lnot W$
  $P \qquad H$
  
  
    
    $R \lor S \qquad E \rightarrow 2,5$ 
    $R \qquad H$
    
    
      
      $W \land Z \qquad E\rightarrow 3,7$
      $W \qquad E\rightarrow 8$
      $Z \qquad E\rightarrow 8$
      
    
    
  
  


My professor only uses the Fitch notation, so I would appreciate you using it in your answer.

EDIT: Using the suggestions in the answers provided and studying the rules some more, I have come up with this solution. Can you tell me whether it is acceptable?

$1 \quad P \lor Q
\\ 2 \quad P \rightarrow R \lor S
\\ 3 \quad R \rightarrow W \land Z
\\ 4 \quad Z \land \lnot S \rightarrow \lnot W
\\ 5 \qquad \lnot S \qquad assumption
\\ 6 \qquad \qquad P \qquad assumption
\\ 7 \qquad \qquad R \lor S \qquad implication \ elim \ 2,6
\\ 8 \qquad \qquad R \qquad disjunctive \ syll \ 7,5
\\ 9 \qquad \qquad W \land Z \qquad implication \ elim \ 3,8
\\ 10 \qquad \qquad Z \qquad conjunction \ elim \ 9
\\ 11 \qquad \qquad Z \land \lnot S \qquad conjunction \ intro \ 10,5
\\ 12 \qquad \qquad \lnot W \qquad implication \ elim \ 4,11
\\ 13 \qquad \qquad W \qquad conjunction \ elim \ 9
\\ 14 \qquad \qquad false \qquad negation \ elim \ 13,12
\\ 15 \qquad \lnot P \qquad negation \ intro \ 14
\\ 16 \qquad Q \qquad disjunctive \ syll \ 1,15
\\ 17 \quad \lnot S \rightarrow Q \qquad implication \ intro \ 5,16$
We have to start from $P \lor Q$ and use $∨$elim [see here for the ND rules used].

The branch starting with $Q$ will be :

$1_Q)$ $Q$ --- assumed for $\lor$-elim


  
    A) $\lnot S \to Q$ --- from 1) by $\to$-intro.
  


For the "branch" starting with $P$ we have :

$1_P)$ $P$ --- assumed for $\lor$-elim

2) $R \lor S$ --- from 1) and 2nd premise by $\to$-elim

3) $S$ --- assumed [a] from 2) for $\lor$-elim

4) $\lnot S$ --- assumed [b]

5) $\bot$ --- contradiction : from 3) and 4) by $\lnot$-elim

6) $Q$ --- from 5) by $\bot$-elim


  7) $\lnot S \to Q$ --- from 4) and 6) by $\to$-intro, discharging [b].


Now for :

8) $R$ --- assumed [c] for $\lor$-elim

9) $W \land Z$ --- from 8) and 3rd premises by $\to$-elim

10) $W$ --- from 9) by $\land$-elim

11) $Z$ --- from 9) by $\land$-elim

12) $\lnot S$ --- assumed [d]

13) $Z \land \lnot S$ --- from 11) and 12) by $\land$-intro

14) $\lnot W$ --- from 13) and 4th premise by $\to$-elim

15) $\bot$ --- contradiction : from 10) and 14) by $\lnot$-elim

16) $Q$ --- from 15) by $\bot$-elim

17) $\lnot S \to Q$ --- from 12 and 16) by $\to$-intro, discharging [d]


  
    B) $\lnot S \to Q$ --- from 2), 3)-7) and 8)-9) by $\lor$-elim, discharging [a] and [c].
  


Now from A), B) and the 1st premise: $P \lor Q$, we conclude by $\lor$-elim with:


  $\lnot S \to Q$,


discharging assumptions $1_Q)$ and $1_P)$.
After an edit the OP asks the following:


  Using the suggestions in the answers provided and studying the rules some more, I have come up with this solution. Can you tell me whether it is acceptable?


One way to tell if a proof is likely acceptable is to put it in a proof checker. Since the OP is using a similar Fitch-style natural deduction system as presented by forallx, the proof checker associated with that text could be used to see if the proof is acceptable.  Here is the result:





Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

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/