Consider the following premises. Q_2(h) <-> S_20(a_20). forall x_20: R_20(x_20) -> S_20(x_20). ~P_4(h). forall z: Q_2(z) -> P_4(z). Can we infer ~R_20(a_20) from them? If possible, name the inference rules being used at each step.
 From forall x_20: R_20(x_20) -> S_20(x_20) we can infer R_20(a_20) -> S_20(a_20) via universal instantiation. From forall z: Q_2(z) -> P_4(z) we can infer Q_2(h) -> P_4(h) via universal instantiation. From Q_2(h) -> P_4(h), ~P_4(h) we can infer ~Q_2(h) via modus tollens. From Q_2(h) <-> S_20(a_20), ~Q_2(h) we can infer ~S_20(a_20) via biconditional elimination. Finally, from R_20(a_20) -> S_20(a_20), ~S_20(a_20) we can infer ~R_20(a_20) via modus tollens. Therefore, the answer is yes.