2026-07-072026-07-07http://salesiana.dossiersoluciones.com/handle/123456789/152928This paper describes some experiments involving the automated theorem-proving program OTTER in the system TRC of illative combinatory logic. We show how OTTER can be steered to find a contradiction in an inconsistent variant of TRC, and present some experimentally discovered identities in TRC.LogicOTTER Experiments in a System of Combinatory Logictext