Consider the following premises. p -> r_1. r_1 -> w_4. p or w_4. w_4 -> r_1. Can we infer ~r_1 from them? If possible, name the inference rules being used at each step.
 From r_1 -> w_4, w_4 -> r_1 we can infer r_1 <-> w_4 via biconditional introduction. From r_1 <-> w_4 we can infer w_4 -> r_1 via biconditional elimination. Finally, from p -> r_1, w_4 -> r_1, p or w_4 we can infer r_1 via disjunction elimination, which contradicts ~r_1. Therefore, the answer is no.