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