Consider the following premises. ~Q(e_2). forall x_3: Q(x_3) <-> W_2(x_3). Can we infer W_2(e_2) from them? If possible, name the inference rules being used at each step.
 From forall x_3: Q(x_3) <-> W_2(x_3) we can infer Q(e_2) <-> W_2(e_2) via universal instantiation. Finally, from Q(e_2) <-> W_2(e_2), ~Q(e_2) we can infer ~W_2(e_2) via biconditional elimination, which contradicts W_2(e_2). Therefore, the answer is no.