Deductive Logic, Warren Goldfarb, Hackett Publishing, 2003, Part IV, Exercise 5(b), p. 285

The task: to show that the premises imply the conclusion.

1. (x)Gxx
2. (x)(y)[¬ (x = y) ⊃ (∃z)(Gxz • Gzy)]
3. ∴(x)(y)(∃z)(Gxz • Gzy)
4. * ¬ (x)(y)(∃z)(Gxz • Gzy) ......... IP
5. * (∃x)¬(y)(∃z)(Gxz • Gzy) ......... 4 QC
6. * (∃x)(∃y)¬(∃z)(Gxz • Gzy) ......... 5 QC
7. * (∃x)(∃y)(z)¬(Gxz • Gzy) ......... 6 QC
8. * (∃x)(∃y)(z)(¬Gxz ∨¬ Gzy) ......... 7 DeM.
9. * (∃x)(∃y)(z)(Gxz ⊃¬ Gzy) ......... 8 MI
10. * (∃y)(z)(Gaz ⊃¬ Gzy) ......... 9 EI x/a
11. * (z)(Gaz ⊃¬ Gzm) ......... 10 EI y/m
12. * Gaa ⊃¬ Gam ......... 11 UI z/a
13. * Gaa ......... 1 UI x/a
14. * ¬ Gam ......... 12,13 MP
15. * ¬ (a = m) ......... 13,14 Id
16. * (y)[¬ (a = y) ⊃ (∃z)(Gaz • Gzy)] ......... 2 UI x/a
17. * ¬ (a = m) ⊃ (∃z)(Gaz • Gzm) ......... 16 UI y/m
18. * (∃z)(Gaz • Gzm) ......... 15,17 MP
19. * Gar • Grm ......... 18 EI z/r
20. * Gar ......... 19 Simp.
21. * Grm ......... 19 Simp.
22. * Gar ⊃¬ Grm ......... 11 UI z/r
23. * ¬ Grm ......... 20,22 MP
24. * Grm • ¬ Grm ......... 21,23 Conj.
25. ¬ ¬ (x)(y)(∃z)(Gxz • Gzy) ......... 4-24 IP
26. (x)(y)(∃z)(Gxz • Gzy) ......... 25 DN