Consider the following premises. p or ~t. p <-> r. p_12 or r. ~p_12 or t. Can we infer p from them?
 From p_12 or r, ~p_12 or t we can infer r or t. From p or ~t we can infer t -> p. From p <-> r we can infer r -> p. Finally, from r -> p, t -> p, r or t we can infer p. Therefore, the answer is yes.