People could send e-mail containing a conjecture in combinatory logic, the problem would be given to the theorem prover ITP, and the results of the search would be returned by e-mail, all without human intervention.
See "A Note on Smullyan's Birds", by Overbeek and Glickfeld, Association of Automated Reasoning Newsletter #7, October 1986.