Consider the following premises. forall y: ~W(y). q. s <-> W(i). Can we infer ~s and q from them? If possible, name the inference rules being used at each step.
 From forall y: ~W(y) we can infer ~W(i) via universal instantiation. From s <-> W(i), ~W(i) we can infer ~s via biconditional elimination. Finally, from ~s, q we can infer ~s and q via conjunction. Therefore, the answer is yes.