Consider the following premises. forall z_2: ~W_4(z_2). p_2. q <-> W_4(a_14). Can we infer p_2 and ~q from them? If possible, name the inference rules being used at each step.
 From forall z_2: ~W_4(z_2) we can infer ~W_4(a_14) via universal instantiation. From q <-> W_4(a_14), ~W_4(a_14) we can infer ~q via biconditional elimination. Finally, from p_2, ~q we can infer p_2 and ~q via conjunction. Therefore, the answer is yes.