Consider the following premises. forall x_22: Q_22(x_22) -> R_22(x_22). forall x_22: P_22(x_22) -> R_22(x_22). forall x_22: P_22(x_22) or Q_22(x_22). R_22(a_18) -> t. Can we infer ~t from them? If possible, name the inference rules being used at each step.
 From forall x_22: P_22(x_22) -> R_22(x_22), forall x_22: Q_22(x_22) -> R_22(x_22), forall x_22: P_22(x_22) or Q_22(x_22) we can infer forall x_22: R_22(x_22) via universal disjunction elimination. From forall x_22: R_22(x_22) we can infer R_22(a_18) via universal instantiation. Finally, from R_22(a_18) -> t, R_22(a_18) we can infer t via modus ponens, which contradicts ~t. Therefore, the answer is no.