Consider the following premises. S(j_3) -> r. forall y: P(y) -> S(y). r -> S(j_3). Can we infer ~(P(j_3) -> r) from them? If possible, name the inference rules being used at each step.
That contradicts the premises. Therefore the answer is no.