Consider the following premises. t_1 -> R_3(a_5). forall y: W(y) -> R_3(y). forall y: R_3(y) -> W(y). forall y: ~W(y). Can we infer t_1 from them?
 From forall y: R_3(y) -> W(y), forall y: W(y) -> R_3(y) we can infer forall y: R_3(y) <-> W(y). From forall y: R_3(y) <-> W(y), forall y: ~W(y) we can infer forall y: ~R_3(y). From forall y: ~R_3(y) we can infer ~R_3(a_5). Finally, from t_1 -> R_3(a_5), ~R_3(a_5) we can infer ~t_1, which contradicts t_1. Therefore, the answer is no.