Consider the following premises. ~t_4 -> w_2. t_4 -> Q_17(e). forall x_17: ~P_17(x_17). forall x_17: P_17(x_17) <-> Q_17(x_17). Can we infer ~w_2 from them? If possible, name the inference rules being used at each step.
 From forall x_17: P_17(x_17) <-> Q_17(x_17), forall x_17: ~P_17(x_17) we can infer forall x_17: ~Q_17(x_17) via universal biconditional elimination. From forall x_17: ~Q_17(x_17) we can infer ~Q_17(e) via universal instantiation. From t_4 -> Q_17(e), ~Q_17(e) we can infer ~t_4 via modus tollens. Finally, from ~t_4 -> w_2, ~t_4 we can infer w_2 via modus ponens, which contradicts ~w_2. Therefore, the answer is no.