Consider the following premises. w or T(j_2). P(j_2) or ~w. forall y: T(y) -> P(y). Can we infer ~P(j_2) from them? If possible, name the inference rules being used at each step.
 From forall y: T(y) -> P(y) we can infer T(j_2) -> P(j_2) via universal instantiation. From P(j_2) or ~w we can infer w -> P(j_2) via rewriting. Finally, from w -> P(j_2), T(j_2) -> P(j_2), w or T(j_2) we can infer P(j_2) via disjunction elimination, which contradicts ~P(j_2). Therefore, the answer is no.