Consider the following premises. r -> W_1(b_4). p_2 or Q(b_4). ~p_2 or r. forall x: Q(x) -> W_1(x). Can we infer W_1(b_4) from them? If possible, name the inference rules being used at each step.
 From forall x: Q(x) -> W_1(x) we can infer Q(b_4) -> W_1(b_4) via universal instantiation. From p_2 or Q(b_4), ~p_2 or r we can infer Q(b_4) or r via resolution. Finally, from Q(b_4) -> W_1(b_4), r -> W_1(b_4), Q(b_4) or r we can infer W_1(b_4) via disjunction elimination. Therefore, the answer is yes.