Consider the following premises. ~S_6(c_4). ~R_6(c_4) or w_4. forall x_6: R_6(x_6) or S_6(x_6). Can we infer w_4 from them? If possible, name the inference rules being used at each step.
 From forall x_6: R_6(x_6) or S_6(x_6) we can infer R_6(c_4) or S_6(c_4) via universal instantiation. From R_6(c_4) or S_6(c_4), ~R_6(c_4) or w_4 we can infer S_6(c_4) or w_4 via resolution. Finally, from S_6(c_4) or w_4, ~S_6(c_4) we can infer w_4 via disjunctive syllogism. Therefore, the answer is yes.