Consider the following premises. s <-> p_11. R_17(a_17) -> p_11. p_11 -> R_17(a_17). u_1 -> s. forall x_17: ~R_17(x_17). Can we infer ~u_1 from them? If possible, name the inference rules being used at each step.
 From forall x_17: ~R_17(x_17) we can infer ~R_17(a_17) via universal instantiation. From p_11 -> R_17(a_17), R_17(a_17) -> p_11 we can infer p_11 <-> R_17(a_17) via biconditional introduction. From p_11 <-> R_17(a_17), ~R_17(a_17) we can infer ~p_11 via biconditional elimination. From s <-> p_11, ~p_11 we can infer ~s via biconditional elimination. Finally, from u_1 -> s, ~s we can infer ~u_1 via modus tollens. Therefore, the answer is yes.