A Concise Introduction to Logic, Patrick J. Hurley, Wadsworth, 2006, 9th ed,. 8.7, III, 12 p. 449

The only dogs that barked were Fido and Pluto. Fido is not Pluto. Every dog except Fido ran on the beach. Therefore, exactly one barking dog ran on the beach. (Dx: x is a dog; Bx: x barked; Rx: x ran on the beach; f: Fido; p: Pluto)

1.     Df • Bf • Dp • Bp • (x)[(Dx • Bx) ⊃ (x = f v x = p)] 2.     f ≠ p 3.     Df • ~ Rf • (x)[(Dx • x ≠ f) ⊃ Rx] ∴ (∃x){Dx • Bx • Rx • (y)[(Dy • By • Ry) ⊃ x = y)]} 4.     ~ (∃x){Dx • Bx • Rx • (y)[(Dy • By • Ry) ⊃ x = y)]} 5.     (x) ~ {Dx • Bx • Rx • (y)[(Dy • By • Ry) ⊃ x = y)]} 6.     (x){~ (Dx • Bx • Rx) v ~ (y) [(Dy • By • Ry) ⊃ x = y)]} 7.     (x){~ (Dx • Bx • Rx) v (∃y) ~ [(Dy • By • Ry) ⊃ x = y)]} 8.     (x){~ (Dx • Bx • Rx) v (∃y) ~ [~ (Dy • By • Ry) v x = y)]} 9.     (x){~ (Dx • Bx • Rx) v (∃y) [(Dy • By • Ry) • x ≠ y)]} 10.  Dp • Bp • Df • Bf • (x)[(Dx • Bx) ⊃ (x = f v x = p)] 11.  Dp 12.  p ≠ f 13.  Dp • p ≠ f 14.  (x)[(Dx • x ≠ f) ⊃ Rx] • Df • ~ Rf 15.  (x)[(Dx • x ≠ f) ⊃ Rx] 16.  (Dp • p ≠ f) ⊃ Rp 17.  Rp 18.  ~ (Dp • Bp • Rp) v (∃y) [(Dy • By • Ry) • p ≠ y)] 19.  Dp • Bp 20.  Dp • Bp • Rp 21.  (∃y)[(Dy • By • Ry) • p ≠ y)] 22.  Dm • Bm • Rm • p ≠ m 23.  (x)[(Dx • Bx) ⊃ (x = f v x = p)] • Df • Bf • Dp • Bp 24.  (x)[(Dx • Bx) ⊃ (x = f v x = p)] 25.  (Dm • Bm) ⊃ (m = f v m = p) 26.  Dm • Bm 27.  m = f v m = p 28.  p ≠ m • Dm • Bm • Rm 29.  p ≠ m 30.  m ≠ p 31.  m = f 32.  Rm • Dm • Bm • p ≠ m 33.  Rm 34.  Rf 35.  ~ Rf • Df • (x)[(Dx • x ≠ f) ⊃ Rx] 36.  ~ Rf 37.  Rf • ~ Rf 38.  ~ ~ (∃x){Dx • Bx • Rx • (y)[(Dy • By • Ry) ⊃ x = y)]} 39.  (∃x){Dx • Bx • Rx • (y)[(Dy • By • Ry) ⊃ x = y)]}

AIP 4 QC 5 DM 6 QC 7 Impl 8 DM 1 Com 10 Simp 2 Id 11,12 Conj 3 Com 13 Simp 15 UI 13,16 MP 9 UI 10 Simp 17,19 Conj 18,20 DS 21 EI 1 Com 23 Simp 24 UI 22 EI 25,26 MP 22 Com 28 Simp 29 Id 27,30 DS 22 Com 32 Simp 31,33 Id 3 Com 25 Simp 34,36 Conj 4-37 IP 38 DN