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