Consider the following premises. ~S_17(a_17). q_8 -> t. S_17(a_17) -> q_8. t -> R_17(a_17). forall x_17: R_17(x_17) -> S_17(x_17). Can we infer ~R_17(a_17) from them?
 From forall x_17: R_17(x_17) -> S_17(x_17) we can infer R_17(a_17) -> S_17(a_17). From S_17(a_17) -> q_8, q_8 -> t we can infer S_17(a_17) -> t. From S_17(a_17) -> t, t -> R_17(a_17) we can infer S_17(a_17) -> R_17(a_17). From R_17(a_17) -> S_17(a_17), S_17(a_17) -> R_17(a_17) we can infer R_17(a_17) <-> S_17(a_17). Finally, from R_17(a_17) <-> S_17(a_17), ~S_17(a_17) we can infer ~R_17(a_17). Therefore, the answer is yes.