Consider the following premises. ~S_14(a_14). forall x_14: W_1(x_14) -> S_14(x_14). ~W_1(a_14) -> w_1. Can we infer w_1 from them? If possible, name the inference rules being used at each step.
 From forall x_14: W_1(x_14) -> S_14(x_14) we can infer W_1(a_14) -> S_14(a_14) via universal instantiation. From W_1(a_14) -> S_14(a_14), ~S_14(a_14) we can infer ~W_1(a_14) via modus tollens. Finally, from ~W_1(a_14) -> w_1, ~W_1(a_14) we can infer w_1 via modus ponens. Therefore, the answer is yes.