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