Consider the following premises. ~R_21(a_21) <-> q_1. ~q_18. forall x_21: R_21(x_21) <-> S_21(x_21). S_21(a_21) <-> q_18. Can we infer q_1 from them?
 From forall x_21: R_21(x_21) <-> S_21(x_21) we can infer R_21(a_21) <-> S_21(a_21). From S_21(a_21) <-> q_18, ~q_18 we can infer ~S_21(a_21). From R_21(a_21) <-> S_21(a_21), ~S_21(a_21) we can infer ~R_21(a_21). From ~R_21(a_21) <-> q_1 we can infer ~R_21(a_21) -> q_1. Finally, from ~R_21(a_21) -> q_1, ~R_21(a_21) we can infer q_1. Therefore, the answer is yes.