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