Consider the following premises. W_1(a_8) -> q_1. q_1 -> s_3. forall y_4: U_3(y_4) or W_1(y_4). U_3(a_8) -> s_3. Can we infer ~s_3 from them? If possible, name the inference rules being used at each step.
 From forall y_4: U_3(y_4) or W_1(y_4) we can infer U_3(a_8) or W_1(a_8) via universal instantiation. From W_1(a_8) -> q_1, q_1 -> s_3 we can infer W_1(a_8) -> s_3 via transitivity. Finally, from U_3(a_8) -> s_3, W_1(a_8) -> s_3, U_3(a_8) or W_1(a_8) we can infer s_3 via disjunction elimination, which contradicts ~s_3. Therefore, the answer is no.