ACL2 PUBLIC SOFTWARE LICENSE
                           Computational Logic, Inc.
                          1717 West Sixth, Suite 290
                           Austin, Texas 78703-4776

Please  read  this  License Agreement carefully before using the ACL2 Software.
By using and/or copying the ACL2 Software, you are agreeing to be bound by  the
terms  of  this  License  Agreement.   If you do not agree to the terms of this
License Agreement, promptly discontinue use of and  remove  the  ACL2  Software
from  your  system, and if it was distributed using a physical medium such as a
diskette, return it to the place where you obtained it.

The ACL2 Software was developed by Computational Logic, Inc. ("CLI").  The ACL2
Software  is  the  sole property of CLI.  Subject to the terms of this License,
CLI retains all rights in the ACL2 Software.  You own the disk or other  medium
on  which  the  ACL2  Software  is  recorded, but CLI retains title to the ACL2
Software.  The purposes of this License Agreement  are  to  identify  the  ACL2
Software and to make the ACL2 Software, including its source code, available on
a royalty-free basis.    This  License  Agreement  allows  you  to  use,  copy,
distribute  and modify the ACL2 Software, on the condition that you comply with
all the Limitations set forth below.

LIMITATIONS

   1. Subject  to  the  export  restrictions  below,  you  may  copy   and
      distribute  verbatim  copies of the ACL2 Software as you receive it,
      in any medium, including embedding it verbatim in derivative  works,
      provided  that  you  (a)  conspicuously and appropriately publish on
      each copy a copyright notice as follows:  "Copyright  (C)  1989-1995
      by  Computational  Logic,  Inc. All Rights Reserved.", (b) display a
      complete copy of this ACL2 Public Software License Agreement on  all
      copies of the ACL2 Software, including derivative works thereof, and
      (c) give all recipients of the ACL2 Software a  copy  of  this  ACL2
      Public Software License Agreement along with the program.

   2. You  may  modify  your  copy  or  copies of the ACL2 Software or any
      portion of it, for internal use only.

   3. You may incorporate parts of the ACL2 Software into  other  programs
      for  internal  use  only, provided that you acknowledge ownership of
      the ACL2  Software  by  Computational  Logic  Inc.  in  the  program
      documentation.

   4. EXPORT/RE-EXPORT LIMITATIONS

      ACL2  may  be  exported  under  a  "General  License GTDA" ("General
      Technical Data Available to  All  Destinations")  to  any  countries
      except those subject to embargoes under various laws administered by
      the   Office   of   Foreign   Assets   Control   ("OFAC")   of   the
      U. S. Department of the Treasury.

      It  is  the understanding of Computational Logic, that, as of August
      22, 1995, ACL2 may be exported to any country except as follows:

         - Both electronic transfer and export of magnetic  tape  to  Iraq
           and Yugoslavia require specific licensing by OFAC.

         - Electronic transfer to North Korea and Libya is prohibited.

      However,  OFAC  should  be consulted for the current status of these
      and any other embargoes.

CLI also requests, but does not require, that any improvements or extensions to
the  ACL2  Software be returned to one of the addresses below, so that they may
be shared with other ACL2 users.  The ACL2 Software, including its source code,
can be obtained by contacting one of these addresses.

     Software-Request                   or       Software-Request@CLI.COM
     Computational Logic Inc.
     1717 West Sixth, Suite 290
     Austin, Texas 78703-4776

NO WARRANTY

BECAUSE  THE  ACL2  SOFTWARE  IS  LICENSED  ON A ROYALTY-FREE BASIS, WE PROVIDE
ABSOLUTELY NO WARRANTY.  THE ACL2 SOFTWARE IS PROVIDED "AS IS" WITHOUT WARRANTY
OF  ANY  KIND,  EITHER  EXPRESS  OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, ANY
IMPLIED WARRANTIES OF MERCHANTABILITY OR FITNESS FOR A  PARTICULAR  PURPOSE  OR
OTHER  WARRANTIES,  STATUTORY  OR  OTHERWISE,  WHICH  WARRANTIES  ARE EXPRESSLY
DISCLAIMED HEREBY.  THE ENTIRE RISK AS TO THE QUALITY AND  PERFORMANCE  OF  THE
ACL2  SOFTWARE RESIDES WITH YOU.  SHOULD THE ACL2 SOFTWARE PROVE DEFECTIVE, YOU
ASSUME THE WHOLE COST AND RESPONSIBILITY FOR ALL NECESSARY SERVICING, REPAIR OR
CORRECTION.

UNDER NO CIRCUMSTANCES, INCLUDING NEGLIGENCE, SHALL COMPUTATIONAL LOGIC INC. BE
LIABLE TO YOU  FOR  ANY  DAMAGES,  ANY  LOST  PROFITS,  LOST  MONIES,  SPECIAL,
INDIRECT,  INCIDENTAL, CONSEQUENTIAL OR OTHER DAMAGES ARISING OUT OF THE USE OR
INABILITY TO USE THE ACL2 SOFTWARE (INCLUDING BUT NOT LIMITED TO LOSS  OF  DATA
OR  DATA  BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY THIRD PARTIES), EVEN
IF YOU HAVE ADVISED US OF THE POSSIBILITY OF SUCH DAMAGES, OR FOR ANY CLAIM  BY
ANY OTHER PARTY.