(IN-PACKAGE "ACL2") "ACL2 Version 3.6" :BEGIN-PORTCULLIS-CMDS :END-PORTCULLIS-CMDS NIL (("/Users/cce/git/planet/dracula/teachpacks/io-utilities.lisp" "io-utilities" "io-utilities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1643554831) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/floor-mod/floor-mod.lisp" "arithmetic-3/floor-mod/floor-mod" "floor-mod" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 207910552)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/bind-free/top.lisp" "../bind-free/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 711889438)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/bind-free/banner.lisp" "banner" "banner" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1116442791)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/bind-free/arithmetic-theory.lisp" "arithmetic-theory" "arithmetic-theory" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 759536443)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/bind-free/remove-weak-inequalities.lisp" "remove-weak-inequalities" "remove-weak-inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 133738376)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/bind-free/collect.lisp" "collect" "collect" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 761980248)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/bind-free/integerp-meta.lisp" "integerp-meta" "integerp-meta" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 361899380)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/bind-free/integerp.lisp" "integerp" "integerp" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1275913392)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/bind-free/numerator-and-denominator.lisp" "numerator-and-denominator" "numerator-and-denominator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 31207312)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/bind-free/simplify.lisp" "simplify" "simplify" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 293487690)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/bind-free/simplify-helper.lisp" "simplify-helper" "simplify-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 485881655)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/bind-free/normalize.lisp" "normalize" "normalize" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 934811827)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/bind-free/basic.lisp" "basic" "basic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1533971491)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/bind-free/basic-helper.lisp" "basic-helper" "basic-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1923723189)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/bind-free/common.lisp" "common" "common" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1887779347)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/bind-free/mini-theories.lisp" "mini-theories" "mini-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 61363025)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/bind-free/mini-theories-helper.lisp" "mini-theories-helper" "mini-theories-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 844819714)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/pass1/top.lisp" "../pass1/top" "top" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 297845109)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/pass1/numerator-and-denominator.lisp" "numerator-and-denominator" "numerator-and-denominator" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1372278983)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/pass1/num-and-denom-helper.lisp" "num-and-denom-helper" "num-and-denom-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 780598969)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/pass1/non-linear.lisp" "non-linear" "non-linear" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 586136495)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/pass1/mini-theories.lisp" "mini-theories" "mini-theories" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 996253343)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/pass1/expt.lisp" "expt" "expt" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1529554243)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/pass1/expt-helper.lisp" "expt-helper" "expt-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1633624426)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/pass1/prefer-times.lisp" "prefer-times" "prefer-times" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1274646109)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/pass1/inequalities.lisp" "inequalities" "inequalities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 2102146537)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/pass1/basic-arithmetic.lisp" "basic-arithmetic" "basic-arithmetic" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1012600563)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/pass1/basic-arithmetic-helper.lisp" "basic-arithmetic-helper" "basic-arithmetic-helper" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 434009698)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/bind-free/building-blocks.lisp" "building-blocks" "building-blocks" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1821880993)) (LOCAL ("/Users/cce/local/acl2-3.6/books/arithmetic-3/bind-free/default-hint.lisp" "default-hint" "default-hint" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1118879409)) ("/Users/cce/git/planet/dracula/teachpacks/list-utilities.lisp" "list-utilities" "list-utilities" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 376000559)) 949322491