Uses Modus ponens $(A, A → B |= B)$ or resolution to show that the following set is inconsistent:
- $Q(x) → P (x) \vee \sim R (a)$
- $R (a) \wedge \sim Q(a)$
- $Q(a)$
- $\sim P (y)$
where $x$ and $y$ are universally quantified variables, $a$ is a constant and $P, Q, R$ are monadic predicates.