Consider the following premises. u. forall x_11: P_11(x_11) or W(x_11). forall x_11: ~P_11(x_11). Can we infer u and W(a) from them? If possible, name the inference rules being used at each step.
 From forall x_11: P_11(x_11) or W(x_11), forall x_11: ~P_11(x_11) we can infer forall x_11: W(x_11) via universal disjunctive syllogism. From forall x_11: W(x_11) we can infer W(a) via universal instantiation. Finally, from u, W(a) we can infer u and W(a) via conjunction. Therefore, the answer is yes.