Consider the following premises. p -> u_3. ~t_4. t_4 <-> r_4. u_3 <-> r_4. Can we infer ~p from them? If possible, name the inference rules being used at each step.
 From t_4 <-> r_4, ~t_4 we can infer ~r_4 via biconditional elimination. From u_3 <-> r_4, ~r_4 we can infer ~u_3 via biconditional elimination. Finally, from p -> u_3, ~u_3 we can infer ~p via modus tollens. Therefore, the answer is yes.