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