Consider the following premises. forall y: U(y) -> W_3(y). W_3(d_4) -> p. forall x_3: U(x_3). Can we infer ~p from them? If possible, name the inference rules being used at each step.
 From forall x_3: U(x_3) we can infer U(d_4) via universal instantiation. From forall y: U(y) -> W_3(y) we can infer U(d_4) -> W_3(d_4) via universal instantiation. From U(d_4) -> W_3(d_4), U(d_4) we can infer W_3(d_4) via modus ponens. Finally, from W_3(d_4) -> p, W_3(d_4) we can infer p via modus ponens, which contradicts ~p. Therefore, the answer is no.