The ACL2 system is freely available from the following website:
https://www.cs.utexas.edu/users/moore/acl2
ACL2 is Copyright (C) 2000 University of Texas at Austin and distributed under the terms of the GNU General Public License.
The ACL2 source code for our machine is available from:
https://www.cs.utexas.edu/users/moore/publications/m4/index.html
The authors can be contacted at the e-mail addresses specified on the first page.