(IN-PACKAGE "ACL2") 
"ACL2 Version 2.9.3" 
:BEGIN-PORTCULLIS-CMDS 
(DEFPKG "INSTANCE" (UNION-EQ (QUOTE NIL) (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*))) 
(DEFPKG "COMPUTED-HINTS" (UNION-EQ (QUOTE (MFC-ANCESTORS MFC-CLAUSE STRING-FOR-TILDE-@-CLAUSE-ID-PHRASE INSTANCE::INSTANCE-REWRITE)) (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*))) 
(DEFPKG "SETS" (SET-DIFFERENCE-EQUAL (UNION-EQ (QUOTE (LEXORDER COMPUTED-HINTS::REWRITING-GOAL-LIT COMPUTED-HINTS::REWRITING-CONC-LIT)) (UNION-EQ *ACL2-EXPORTS* *COMMON-LISP-SYMBOLS-FROM-MAIN-LISP-PACKAGE*)) (QUOTE (UNION DELETE FIND MAP)))) 
:END-PORTCULLIS-CMDS 
NIL 
(("/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/fast.lisp" "fast" "fast" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 161133424) ("/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/membership.lisp" "membership" "membership" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 72509769) ("/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/computed-hints.lisp" "computed-hints" "computed-hints" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 131649247) ("/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/instance.lisp" "instance" "instance" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 196777078) ("/v/filer3/v0q044/acl2space/jared/osets/osets-0.91/primitives.lisp" "primitives" "primitives" ((:SKIPPED-PROOFSP) (:AXIOMSP)) . 67192395)) 
122009293