Consider the following premises. forall z_3: T(z_3) -> W_4(z_3). p -> p_1. W_4(f_2) -> u. p_1 -> T(f_2). Can we infer ~(p -> u) from them? If possible, name the inference rules being used at each step.
That contradicts the premises. Therefore the answer is no.