The Logic Book, M. Bergmann, J. Moor, J. Nelson, McGraw Hill, 4th edition, 2004, Ex. 10.5, 5(f)

We are asked to show that a set of sentences is inconsistent. The solution comes down to showing that we can derive a sentence and its negation within the scope of only the primary assumptions. In instantiating line 3 by Existential Instantiation we have to choose a constant other than 'a', as that already occurs in our premises. Working through the set, we derive 'Kam' on line 12 and '¬ Kam' on line 15, which shows that our sentences are indeed inconsistent.

1. (x)[(Sx • Bxx) ⊃Kax] / Premise
2. (x)(Hx ⊃Bxx) / Premise
3. (∃x)(Sx • Hx) / Premise
4. (x) ¬ (Kax • Hx) / Premise
5. Sm • Hm / 3EI x/m
6. Hm ⊃Bmm / 2UI x/m
7. Hm / 5Simp.
8. Bmm / 7,6MP
9. (Sm • Bmm) ⊃Kam / 1UI x/m
10. Sm / 5Simp.
11. Sm • Bmm / 8,10Conj.
12. Kam / 11,9MP
13. ¬ (Kam • Hm) / 4UI x/m
14. ¬ Kam ∨¬ Hm / 13DeM
15. ¬ Kam / 7,14DS