Consider the following premises. forall x_15: R_15(x_15) -> S_15(x_15). q -> R_15(a_15). S_15(a_15) -> ~t_1. t_1. Can we infer q from them?
 From forall x_15: R_15(x_15) -> S_15(x_15) we can infer R_15(a_15) -> S_15(a_15). From S_15(a_15) -> ~t_1, t_1 we can infer ~S_15(a_15). From q -> R_15(a_15), R_15(a_15) -> S_15(a_15) we can infer q -> S_15(a_15). Finally, from q -> S_15(a_15), ~S_15(a_15) we can infer ~q, which contradicts q. Therefore, the answer is no.