Consider the following premises. p_6 <-> S_13(a_13). forall x_13: R_13(x_13) -> S_13(x_13). p_1 or p_6. ~p_1 or R_13(a_13). Can we infer ~S_13(a_13) from them?
 From forall x_13: R_13(x_13) -> S_13(x_13) we can infer R_13(a_13) -> S_13(a_13). From p_6 <-> S_13(a_13) we can infer p_6 -> S_13(a_13). From p_1 or p_6, ~p_1 or R_13(a_13) we can infer p_6 or R_13(a_13). Finally, from p_6 -> S_13(a_13), R_13(a_13) -> S_13(a_13), p_6 or R_13(a_13) we can infer S_13(a_13), which contradicts ~S_13(a_13). Therefore, the answer is no.