 Closer inspection of the left and right hand sides of (18) under the application of unification revealed the discovery of a 10-L bird, i.e. a 10-symbol bird expressed solely in terms of larks, which was a strong candidate for egocentricity. This discovery was exciting because the shortest egocentric L-bird known to Smullyan was of length 12. A subsequent run of the automated reasoning system produced a proof of this fact as well as another new significant bird: A possible egocentric 8-L bird! A few more runs of the system eventually produced a 22-line proof (with terms with as many as 50 symbols, excluding commas and parentheses) of the fact that ((LL)(L(LL)))(L(LL)) is indeed egocentric. The natural questions to ask next are, of course, whether there are other 8-L egocentric birds and whether there are shorter ones. The reader may want to attempt this with paper and pencil but, given that there are 429 such birds, it may be wiser to try it instead (or in conjunction) with an automated reasoning program; both approaches are explored in Glickfeld &amp; Overbeek 1986. For a more formal, but admittedly less colorful, introduction to combinatory logic and lambda-conversion the reader is referred to Hindley &amp; Seldin 1986. 