Consider the following premises. w_1 -> S_2(h). forall y_3: ~S_2(y_3). w and q_5. Can we infer w and ~w_1 from them? If possible, name the inference rules being used at each step.
 From forall y_3: ~S_2(y_3) we can infer ~S_2(h) via universal instantiation. From w_1 -> S_2(h), ~S_2(h) we can infer ~w_1 via modus tollens. From w and q_5 we can infer w via simplification. Finally, from w, ~w_1 we can infer w and ~w_1 via conjunction. Therefore, the answer is yes.