GCL (GNU Common Lisp)  2.6.6 CLtL1    Jan 19 2005 20:24:14
Source License: LGPL(gcl,gmp), GPL(unexec,bfd)
Binary License:  GPL due to GPL'ed components: (BFD UNEXEC)
Modifications of this banner must retain notice of a compatible license
Dedicated to the memory of W. Schelter

Use (help) to get some basic information on how to use GCL.

 ACL2 Version 2.9.3 built August 2, 2005  18:40:53.
 Copyright (C) 2005  University of Texas at Austin
 ACL2 comes with ABSOLUTELY NO WARRANTY.  This is free software and you
 are welcome to redistribute it under certain conditions.  For details,
 see the GNU General Public License.

 Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*
                      NIL).
 See the documentation topic note-2-9-3 for recent changes.
 Note: We have modified the prompt in some underlying Lisps to further
 distinguish it from the ACL2 prompt.

 NOTE!!  Proof trees are disabled in ACL2.  To enable them in emacs,
 look under the ACL2 source directory in interface/emacs/README.doc; 
 and, to turn on proof trees, execute :START-PROOF-TREE in the ACL2 
 command loop.   Look in the ACL2 documentation under PROOF-TREE.

ACL2 Version 2.9.3.  Level 1.  Cbd 
"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !>
Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).
ACL2>
#<"ACL2" package>

ACL2>
ACL2 Version 2.9.3.  Level 1.  Cbd 
"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !> (PROVE PROOF-TREE WARNING OBSERVATION EVENT)
ACL2 !>
Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).

ACL2>
ACL2 Version 2.9.3.  Level 1.  Cbd 
"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !>
ACL2 Version 2.9.3.  Level 2.  Cbd 
"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !>>
Summary
Form:  ( DEFPKG "INSTANCE" ...)
Rules: NIL
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
 "INSTANCE"
ACL2 !>>
Summary
Form:  ( DEFPKG "COMPUTED-HINTS" ...)
Rules: NIL
Warnings:  None
Time:  0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
 "COMPUTED-HINTS"
ACL2 !>>[SGC for 444 CONS pages..(8302 writable)..(T=1).GC finished]

Summary
Form:  ( DEFPKG "SETS" ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 "SETS"
ACL2 !>>Bye.
 :EOF
ACL2 !>[SGC for 444 CONS pages..(8307 writable)..(T=1).GC finished]
[SGC for 12 STRING pages..(8393 writable)..(T=1).GC finished]
[SGC for 12 STRING pages..(8393 writable)..(T=1).GC finished]

Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/instance.o
start address -T 0x9e95000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/instance.o
[SGC for 20 CFUN pages..(8430 writable)..(T=1).GC finished]

Summary
Form:  ( INCLUDE-BOOK "instance" ...)
Rules: NIL
Warnings:  None
Time:  0.07 seconds (prove: 0.00, print: 0.00, other: 0.07)
"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/instance.lisp"
:INVISIBLE

Summary
Form:  ( DEFUN REWRITING-GOAL-LIT ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
REWRITING-GOAL-LIT

Summary
Form:  ( DEFUN REWRITING-CONC-LIT ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
REWRITING-CONC-LIT

Summary
Form:  ( DEFUN HARVEST-TRIGGER ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
HARVEST-TRIGGER

Summary
Form:  ( DEFUN OTHERS-TO-NEGATED-LIST ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
OTHERS-TO-NEGATED-LIST

Summary
Form:  ( DEFUN OTHERS-TO-HYPS ...)
Rules: NIL
Warnings:  None
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
OTHERS-TO-HYPS

Summary
Form:  ( DEFUN BUILD-HINT ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
BUILD-HINT

Summary
Form:  ( DEFUN BUILD-HINTS ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
BUILD-HINTS

Summary
Form:  ( DEFCONST *MESSAGE* ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
*MESSAGE*

Summary
Form:  ( DEFUN AUTOMATE-INSTANTIATION-FN ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
AUTOMATE-INSTANTIATION-FN

Summary
Form:  ( DEFMACRO AUTOMATE-INSTANTIATION ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
AUTOMATE-INSTANTIATION

Summary
Form:  ( TABLE ACL2::ACL2-DEFAULTS-TABLE ...)
Rules: NIL
Warnings:  None
Time:  0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
ACL2::ACL2-DEFAULTS-TABLE
[SGC for 20 CFUN pages..(8679 writable)..(T=1).GC finished]
Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/instance.o
start address -T 0x9ea5000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/instance.o

Summary
Form:  ( INCLUDE-BOOK "computed-hints" ...)
Rules: NIL
Warnings:  None
Time:  0.08 seconds (prove: 0.00, print: 0.00, other: 0.08)
Compiling /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/computed-hints.lisp.
End of Pass 1.  

;; Note: Tail-recursive call of HARVEST-TRIGGER was replaced by iteration.
End of Pass 2.  
OPTIMIZE levels: Safety=0 (No runtime error checking), Space=0, Speed=3
Finished compiling /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/computed-hints.o.

"/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/computed-hints.o" 

Loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/computed-hints.o
start address -T 0x89e1000 Finished loading /v/filer3/v0q044/acl2space/jared/osets/osets-0.91/computed-hints.o

Summary
Form:  (CERTIFY-BOOK "computed-hints" ...)
Rules: NIL
Warnings:  None
Time:  0.09 seconds (prove: 0.00, print: 0.00, other: 0.09)
 "/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/computed-hints.lisp"
ACL2 !>
Exiting the ACL2 read-eval-print loop.  To re-enter, execute (LP).

ACL2>