Consider the following premises. R_14(b) <-> s. forall x_14: ~R_14(x_14). Can we infer s from them? If possible, name the inference rules being used at each step.
 From forall x_14: ~R_14(x_14) we can infer ~R_14(b) via universal instantiation. Finally, from R_14(b) <-> s, ~R_14(b) we can infer ~s via biconditional elimination, which contradicts s. Therefore, the answer is no.