For some, the object of automated reasoning is the design and implementation of a program that offers sufficient power to enable one to contribute new and significant results to mathematics and to logic, as well as elsewhere. One measure of success rests with the number and quality of the results obtained with the assistance of the program in focus. A less obvious measure (heavily in focus here) rests with the ability of a novice in the domain under investigation, to make significant contributions to one or more fields of science by relying heavily on a given reasoning program. For example, if one who is totally unfamiliar with the area of study but skilled in automated reasoning can discover with an automated reasoning program impressive proofs, previously unknown axiom dependencies, and far more, then the field of automated reasoning has indeed arrived. This article details how one such novice, with much experience with W. McCune's program OTTER, but no knowledge of the domains under investigation, obtained startling results in the study of areas of logic that include the BCSK logic and various extensions of that logic. Among those results was the discovery of a variety weaker than has been studied from what we know, a variety that appears to merit serious study, as, for example, does the study of semigroups when compared with that of the study of groups. A quite different result concerns the discovery of a most unexpected dependency in two extensions of the BCSK logic.