Consider the following premises. p -> q. p. q -> w_1. w_1 -> t_4. Can we infer ~t_4 from them? If possible, name the inference rules being used at each step.
 From q -> w_1, w_1 -> t_4 we can infer q -> t_4 via transitivity. From p -> q, p we can infer q via modus ponens. Finally, from q -> t_4, q we can infer t_4 via modus ponens, which contradicts ~t_4. Therefore, the answer is no.