Understanding Symbolic Logic, Virginia Klenk, Prentice Hall, 2008, Unit 20, Problem 1l

Working backwards from the conclusion here gets us only so far, which is why the conclusion is best reached by Indirect Proof after instantiating the first two premises. The tricky part was getting to step 44 from the information on line 35, 36 and 37. Instinctively, we could argue:

Either Samuel Clemens was Mark Twain or Clement Samuelson was Mark Twain.

Neither Samuel Clemens nor Clement Samuelson was Dick Tracy.

Therefore, Dick Tracy was not Mark Twain.

However, the reasoning appears more convincing to me if we argue by another Indirect Proof, on line 38. If we can prove that 'Dick Tracy was Mark Twain' is a contradiction, given our premises, we can be sure that the original conclusion 'Dick Tracy was not Mark Twain' is supported by the premises. Once this hurdle is cleared, it only remains to follow up with multiple instantiations of the main conclusion until we obtain another contradiction on line 88.

1. (∃x)(∃y)(∃z){Cx • Cy • Cz • Rx • Ry • Rz • ¬ (x = y) • ¬ (x = z) • ¬ (z = y) • (w){[(Cw • Rw) ⊃[(w = x) ∨(w = y) ∨(w = z)]}}
   
2. (∃x){Cx • Rx • Px • (y)[(Cy • Ry • Py) ⊃y = x]}


3. (x)[(Cx • Rx • ¬ Px) ⊃Ox]


4. ∴(∃x)(∃y)[Ox • Oy • Rx • Ry • ¬ (x = y)]


5. (∃y)(∃z){Ca • Cy • Cz • Ra • Ry • Rz • ¬ (a = y) • ¬ (a = z) • ¬ (z = y) • (w){[(Cw • Rw) ⊃[(w = a) ∨(w = y) ∨(w = z)]}} / 1EI


6. (∃z){Ca • Cm • Cz • Ra • Rm • Rz • ¬ (a = m) • ¬ (a = z) • ¬ (z = m) • (w){[(Cw • Rw) ⊃[(w = a) ∨(w = m) ∨(w = z)]}} / 5EI


7. Ca • Cm • Ch • Ra • Rm • Rh • ¬ (a = m) • ¬ (a = h) • ¬ (h = m) • (w){[(Cw • Rw) ⊃[(w = a) ∨(w = m) ∨(w = h)]}} / 6EI


8. Ci • Ri • Pi • (y)[(Cy • Ry • Py) ⊃y = i] / 2EI


9. * ¬ (∃x)(∃y)[Ox • Oy • Rx • Ry • ¬ (x = y)] / AIP


10. * (x)(y)[(Ox • Oy • Rx • Ry) ⊃x = y] / 9CQ


11. * (y)[(Oa • Oy • Ra • Ry) ⊃a = y] / 10UI


12. * (Oa • Om • Ra • Rm) ⊃a = m / 11UI


13. * ¬ (a = m) / 7Simp


14. * ¬ (Oa • Om • Ra • Rm) / 13,12MT


15. * ¬ Oa ∨ ¬ Om ∨ ¬ Ra ∨ ¬ Rm / 14DeM


16. * Ra • Rm / 7Simp


17. * ¬ Oa ∨ ¬ Om ∨/ 16,15DS


18. * (Ca • Ra • ¬ Pa) ⊃Oa / 3UI


19. * (Cm • Rm • ¬ Pm) ⊃Om / 3UI


20. * [(Ca • Ra • ¬ Pa) ⊃Oa] • [(Cm • Rm • ¬ Pm) ⊃Om] /18,19Conj


21. * ¬ (Ca • Ra • ¬ Pa) ∨¬ (Cm • Rm • ¬ Pm) / 17,20DD


22. * ¬ Ca ∨¬ Ra ∨ Pa ∨¬ Cm ∨¬ Rm ∨Pm / 21DeM


23. * Ca • Ra • Cm • Rm / 7Simp


24. * Pa ∨Pm / 22,23DS


25. * (y)[(Cy • Ry • Py) ⊃y = i] / 8Simp


26. * (Ca • Ra • Pa) ⊃a = i / 25UI


27. * (Ca • Ra) ⊃(Pa ⊃a = i) / 26Exp


28. * Ca • Ra / 23Simp


29. * Pa ⊃a = i / 28,27MP


30. * (Cm • Rm • Pm) ⊃m = i / 25UI


31. * Cm • Rm / 23Simp


32. * (Cm • Rm) ⊃(Pm ⊃m = i) / 30Exp


33. * Pm ⊃m = i / 31,32MP


34. * (Pa ⊃a = i) • (Pm ⊃m = i) / 29,33Conj


35. * a = i ∨ m = i / 24,34CD


36. * ¬ (a = h) / 7Simp


37. * ¬ (h = m) / 8Simp


38. * * i = h / AIP


39. * * ¬ (m = i) / 37,38Id


40. * * a = i / 39,35DS


41. * * i = a / 40Id


42. * * ¬ (i = h) / 41,36Id


43. * (i = h) • ¬ (i = h) / 38,42Contr


44. * ¬ (i = h) / 38-43IP


45. * (Ch • Rh • Ph) ⊃h = i / 25UI


46. * ¬ (Ch • Rh • Ph) / 44,45MT


47. * ¬ Ch ∨¬ Rh ∨ ¬ Ph / 46DeM


48. * Ch • Rh / 7Simp


49. * ¬ Ph / 48,47DS


50. * (Ch • Rh • ¬ Ph) ⊃Oh / 3UI


51. * Ch • Rh • ¬ Ph / 48,49Conj


52. * Oh / 51,50MP


53. * (y)[(Oa • Oy • Ra • Ry) ⊃a = y] / 10UI


54. * (Oa • Oh • Ra • Rh) ⊃a = h / 53UI


55. * ¬ (a = h) / 7Simp


56. * ¬ (Oa • Oh • Ra • Rh) / 55,54MT


57. * ¬ Oa ∨¬ Oh ∨¬ Ra ∨¬ Rh / 56DeM


58. * Ra • Rh / 7Simp


59. * ¬ Oa∨¬ Oh / 58,57DS


60. * ¬ Oa / 52,59DS


61. * (Ca • Ra • ¬ Pa) ⊃Oa / 3UI


62. * ¬ (Ca • Ra • ¬ Pa) / 60,61MT


63. * ¬ Ca ∨¬ Ra ∨Pa / 62DeM


64. * Pa / 23,63DS


65. * (Ca • Ra • Pa) ⊃a = i / 25UI


66. * Ca • Ra • Pa / 28,64Conj


67. * a = i / 66,65MP


68. * ¬ (m = a) / 13Id


69. * ¬ (m = i) / 67,68Id


70. * (y)[(Oh • Oy • Rh • Ry) ⊃h = y] / 10UI


71. * (Oh • Om • Rh • Rm) ⊃h = m / 70UI


72. * ¬ (h = m) /7Simp


73. * ¬ (Oh • Om • Rh • Rm) / 72,71MT


74. * ¬ Oh ∨¬ Om ∨¬ Rh ∨¬ Rm / 73DeM


75. * Rh • Rm / 7Simp


76. * ¬ Oh ∨¬ Om / 75,74DS


77. * (Ch • Rh • ¬ Ph) ⊃Oh / 3UI


78. * (Cm • Rm • ¬ Pm) ⊃Om / 3UI


79. * [(Ch • Rh • ¬ Ph) ⊃Oh] • [(Cm • Rm • ¬ Pm) ⊃Om] / 77,78Conj


80. * ¬ (Ch • Rh • ¬ Ph) ∨¬ (Cm • Rm • ¬ Pm) / 76,79DD


81. * ¬ Ch ∨¬ Rh ∨Ph ∨¬ Cm ∨¬ Rm ∨Pm / 80DeM


82. * Ch • Cm • Rh • Rm / 7Simp


83. * Ph ∨Pm / 82,81DS


84. * Pm / 49,83DS


85. * (Cm • Rm • Pm) ⊃m = i / 25UI


86. * Cm • Rm • Pm / 31,84Conj


87. * m = i / 86,85MP


88. * m = i • ¬ (m = i) / 87,69Contr


89. (∃x)(∃y)[Ox • Oy • Rx • Ry • ¬ (x = y)] / 9-88IP