Consider the following premises. Karen is an electrician or Charles is a nurse. For all x_13, if x_13 were a nurse, then x_13 is sleeping. Karen is not an electrician or it is overcast. It is overcast if and only if Charles is sleeping. Can we infer the following from them? If we can, name the inference rule being used: Charles is not sleeping.
 From the fact that for all x_13, if x_13 were a nurse, then x_13 is sleeping we can infer that if Charles were a nurse, then Charles is sleeping via universal instantiation. From the fact that Karen is an electrician or Charles is a nurse, and that Karen is not an electrician or it is overcast we can infer that Charles is a nurse or it is overcast via resolution. From the fact that it is overcast if and only if Charles is sleeping we can infer that if it is overcast, then Charles is sleeping via biconditional elimination. Finally, from the fact that if Charles were a nurse, then Charles is sleeping, that if it is overcast, then Charles is sleeping, and that Charles is a nurse or it is overcast we can infer that Charles is sleeping via disjunction elimination, which contradicts that Charles is not sleeping. Therefore, the answer is no.