Consider the following premises. p_2 or T(g_1). forall y_4: S_2(y_4) -> T(y_4). ~p_2 or t_1. forall y_4: ~S_2(y_4). forall y_4: T(y_4) -> S_2(y_4). Can we infer ~w from them? If possible, name the inference rules being used at each step.
We cannot infer that from the premises. Therefore the answer is no.