  This paper reports on an exploration of Boolos' Curious Inference, using
higher-order automated theorem provers (ATPs). Surprisingly, only suitable
shorthand notations had to be provided by hand for ATPs to find a short proof.
The higher-order lemmas required for constructing a short proof are
automatically discovered by the ATPs. Given the observations and suggestions in
this paper, full proof automation of Boolos' and related examples now seems to
be within reach of higher-order ATPs.
