Consider the following premises. ~t. t or s. p -> u. p. Can we infer s from them? If possible, name the inference rules being used at each step.
 From p -> u, p we can infer u via modus ponens. Finally, from t or s, ~t we can infer s via disjunctive syllogism. Therefore, the answer is yes.