References

[1] William Mccune, Otter 3.0 Reference Manual and Guide, Argonne National Laboratories (http://www-unix.mcs.anl.gov/AR/otter/)

[2] M. R. Holmes, Systems of Combinatory Logic Related to Quine's `New Foundations', Annals of Pure and Applied Logic 53, 103-133. See web page http://math.boisestate.edu/~holmes

[3] W. V. Quine, New Foundations for Mathematical Logic, American Mathematical Monthly, 44 (1937) 70-80.

[4] A. Quaife, ..............

[5] T. Jech, OTTER Experiments in a System of Combinatory Logic, Journal of Automated Reasoning 14, 413-426 (http://www.math.psu.edu/jech/preprints/exper.ps)

[6] T. Jech, Some Results on Combinators in the System TRC (http://www.math.psu.edu/jech/preprints/combin.ps)

[7] R. Smullyan, To Mock a Mockingbird, A. Knopf, New York, 1985

[8] Hart, J. & Kunen, K. Single Axioms for Odd Exponent Groups, Journal of Automated Reasoning 14 (1995) 383--412 (http://www.cs.wisc.edu/~kunen/odd.ps)