Consider the following premises. p_4 <-> s_4. R_17(b) -> s_4. S_17(b) -> s_4. forall x_17: R_17(x_17) or S_17(x_17). Can we infer p_4 from them? If possible, name the inference rules being used at each step.
 From forall x_17: R_17(x_17) or S_17(x_17) we can infer R_17(b) or S_17(b) via universal instantiation. From R_17(b) -> s_4, S_17(b) -> s_4, R_17(b) or S_17(b) we can infer s_4 via disjunction elimination. From p_4 <-> s_4 we can infer s_4 -> p_4 via biconditional elimination. Finally, from s_4 -> p_4, s_4 we can infer p_4 via modus ponens. Therefore, the answer is yes.