Consider the following premises. t_2. forall x_20: R(x_20) and S_20(x_20). t_2 -> s_3. Can we infer s_3 and R(a_20) from them? If possible, name the inference rules being used at each step.
 From forall x_20: R(x_20) and S_20(x_20) we can infer R(a_20) and S_20(a_20) via universal instantiation. From t_2 -> s_3, t_2 we can infer s_3 via modus ponens. From R(a_20) and S_20(a_20) we can infer R(a_20) via simplification. Finally, from s_3, R(a_20) we can infer s_3 and R(a_20) via conjunction. Therefore, the answer is yes.