Consider the following premises. S(f) -> ~u. forall x: W(x) -> S(x). p_8 -> u. p_8. forall x: S(x) -> W(x). Can we infer ~W(f) from them? If possible, name the inference rules being used at each step.
 From forall x: W(x) -> S(x), forall x: S(x) -> W(x) we can infer forall x: W(x) <-> S(x) via universal biconditional introduction. From p_8 -> u, p_8 we can infer u via modus ponens. From forall x: W(x) <-> S(x) we can infer W(f) <-> S(f) via universal instantiation. From S(f) -> ~u, u we can infer ~S(f) via modus tollens. Finally, from W(f) <-> S(f), ~S(f) we can infer ~W(f) via biconditional elimination. Therefore, the answer is yes.