Consider the following premises. S_1(a_11) -> t_4. forall y: S_1(y). forall y: W(y). Can we infer t_4 from them?
 From forall y: S_1(y), forall y: W(y) we can infer forall y: S_1(y) and W(y). From forall y: S_1(y) and W(y) we can infer S_1(a_11) and W(a_11). From S_1(a_11) and W(a_11) we can infer S_1(a_11). Finally, from S_1(a_11) -> t_4, S_1(a_11) we can infer t_4. Therefore, the answer is yes.