(RGFI-!RGFI-SAME
 (312 37 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-ACCESS))
 (171 2 (:DEFINITION UPDATE-NTH))
 (111 3 (:REWRITE DEFAULT-CDR))
 (74 37 (:TYPE-PRESCRIPTION NATP-NTH-OF-STR))
 (74 37 (:TYPE-PRESCRIPTION NATP-NTH-OF-SSR))
 (74 37 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-LIMIT))
 (74 37 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-BASE))
 (74 37 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG))
 (74 37 (:TYPE-PRESCRIPTION NATP-NTH-OF-RGF))
 (74 37 (:TYPE-PRESCRIPTION NATP-NTH-OF-MEM))
 (74 37 (:TYPE-PRESCRIPTION NATP-NTH-OF-CTR))
 (55 1 (:REWRITE DEFAULT-CAR))
 (37 37 (:TYPE-PRESCRIPTION STRP))
 (37 37 (:TYPE-PRESCRIPTION SSRP))
 (37 37 (:TYPE-PRESCRIPTION SEGP))
 (37 37 (:TYPE-PRESCRIPTION SEG-LIMITP))
 (37 37 (:TYPE-PRESCRIPTION SEG-BASEP))
 (37 37 (:TYPE-PRESCRIPTION SEG-ACCESSP))
 (37 37 (:TYPE-PRESCRIPTION RGFP))
 (37 37 (:TYPE-PRESCRIPTION MEMP))
 (37 37 (:TYPE-PRESCRIPTION CTRP))
 (14 14 (:TYPE-PRESCRIPTION UPDATE-NTH-ARRAY))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE ZP-OPEN))
 (1 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(RGFI-!RGFI-DIFFERENT
 (1184 130 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-ACCESS))
 (260 130 (:TYPE-PRESCRIPTION NATP-NTH-OF-STR))
 (260 130 (:TYPE-PRESCRIPTION NATP-NTH-OF-SSR))
 (260 130 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-LIMIT))
 (260 130 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-BASE))
 (260 130 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG))
 (260 130 (:TYPE-PRESCRIPTION NATP-NTH-OF-RGF))
 (260 130 (:TYPE-PRESCRIPTION NATP-NTH-OF-MEM))
 (260 130 (:TYPE-PRESCRIPTION NATP-NTH-OF-CTR))
 (222 6 (:REWRITE DEFAULT-CDR))
 (130 130 (:TYPE-PRESCRIPTION STRP))
 (130 130 (:TYPE-PRESCRIPTION SSRP))
 (130 130 (:TYPE-PRESCRIPTION SEGP))
 (130 130 (:TYPE-PRESCRIPTION SEG-LIMITP))
 (130 130 (:TYPE-PRESCRIPTION SEG-BASEP))
 (130 130 (:TYPE-PRESCRIPTION SEG-ACCESSP))
 (130 130 (:TYPE-PRESCRIPTION RGFP))
 (130 130 (:TYPE-PRESCRIPTION MEMP))
 (130 130 (:TYPE-PRESCRIPTION CTRP))
 (110 2 (:REWRITE DEFAULT-CAR))
 (28 28 (:TYPE-PRESCRIPTION UPDATE-NTH-ARRAY))
 (6 6 (:REWRITE DEFAULT-<-2))
 (6 6 (:REWRITE DEFAULT-<-1))
 (2 2 (:REWRITE ZP-OPEN))
 (2 2 (:REWRITE DEFAULT-+-2))
 (2 2 (:REWRITE DEFAULT-+-1))
 )
(RGFI-!RGFI
 (4 4 (:REWRITE DEFAULT-<-2))
 (4 4 (:REWRITE DEFAULT-<-1))
 )
(MEMI-!MEMI-SAME
 (312 37 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-ACCESS))
 (172 2 (:DEFINITION UPDATE-NTH))
 (111 3 (:REWRITE DEFAULT-CDR))
 (74 37 (:TYPE-PRESCRIPTION NATP-NTH-OF-STR))
 (74 37 (:TYPE-PRESCRIPTION NATP-NTH-OF-SSR))
 (74 37 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-LIMIT))
 (74 37 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-BASE))
 (74 37 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG))
 (74 37 (:TYPE-PRESCRIPTION NATP-NTH-OF-RGF))
 (74 37 (:TYPE-PRESCRIPTION NATP-NTH-OF-MEM))
 (74 37 (:TYPE-PRESCRIPTION NATP-NTH-OF-CTR))
 (56 2 (:REWRITE DEFAULT-CAR))
 (37 37 (:TYPE-PRESCRIPTION STRP))
 (37 37 (:TYPE-PRESCRIPTION SSRP))
 (37 37 (:TYPE-PRESCRIPTION SEGP))
 (37 37 (:TYPE-PRESCRIPTION SEG-LIMITP))
 (37 37 (:TYPE-PRESCRIPTION SEG-BASEP))
 (37 37 (:TYPE-PRESCRIPTION SEG-ACCESSP))
 (37 37 (:TYPE-PRESCRIPTION RGFP))
 (37 37 (:TYPE-PRESCRIPTION MEMP))
 (37 37 (:TYPE-PRESCRIPTION CTRP))
 (14 14 (:TYPE-PRESCRIPTION UPDATE-NTH-ARRAY))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE ZP-OPEN))
 (1 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(MEMI-!MEMI-DIFFERENT
 (1166 121 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-ACCESS))
 (242 121 (:TYPE-PRESCRIPTION NATP-NTH-OF-STR))
 (242 121 (:TYPE-PRESCRIPTION NATP-NTH-OF-SSR))
 (242 121 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-LIMIT))
 (242 121 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-BASE))
 (242 121 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG))
 (242 121 (:TYPE-PRESCRIPTION NATP-NTH-OF-RGF))
 (242 121 (:TYPE-PRESCRIPTION NATP-NTH-OF-MEM))
 (242 121 (:TYPE-PRESCRIPTION NATP-NTH-OF-CTR))
 (172 2 (:DEFINITION UPDATE-NTH))
 (121 121 (:TYPE-PRESCRIPTION STRP))
 (121 121 (:TYPE-PRESCRIPTION SSRP))
 (121 121 (:TYPE-PRESCRIPTION SEGP))
 (121 121 (:TYPE-PRESCRIPTION SEG-LIMITP))
 (121 121 (:TYPE-PRESCRIPTION SEG-BASEP))
 (121 121 (:TYPE-PRESCRIPTION SEG-ACCESSP))
 (121 121 (:TYPE-PRESCRIPTION RGFP))
 (121 121 (:TYPE-PRESCRIPTION MEMP))
 (121 121 (:TYPE-PRESCRIPTION CTRP))
 (111 3 (:REWRITE DEFAULT-CDR))
 (56 2 (:REWRITE DEFAULT-CAR))
 (28 28 (:TYPE-PRESCRIPTION UPDATE-NTH-ARRAY))
 (6 6 (:REWRITE DEFAULT-<-2))
 (6 6 (:REWRITE DEFAULT-<-1))
 (1 1 (:REWRITE ZP-OPEN))
 (1 1 (:REWRITE DEFAULT-+-2))
 (1 1 (:REWRITE DEFAULT-+-1))
 )
(MEMI-!MEMI
 (37 37 (:REWRITE DEFAULT-<-2))
 (37 37 (:REWRITE DEFAULT-<-1))
 )
(RM08-WM08-SAME-LEMMA-1
 (3 3 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(ASH-ADDR--2-IS-LESS
 (1 1 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM08-WM08-SAME
 (90 2 (:LINEAR N01P-LOGAND-N01P-LESS-THAN-2))
 (77 42 (:REWRITE DEFAULT-<-1))
 (42 42 (:REWRITE DEFAULT-<-2))
 (22 22 (:LINEAR ASH-NEGATIVE-SHIFT-MAKES-INPUT-SMALLER))
 (11 11 (:LINEAR INDEX-OF-<-LEN))
 (8 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (3 2 (:REWRITE DEFAULT-+-2))
 (3 2 (:REWRITE DEFAULT-+-1))
 )
(RM08-WM08-DIFFERENT-SAME-DWORD-LEMMA
 (4 4 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(N32P-CONCAT-ASH-LOGAND
 (1 1 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM08-WM08-DIFFERENT-SAME-DWORD
 (171 9 (:LINEAR N01P-LOGAND-N01P-LESS-THAN-2))
 (147 96 (:REWRITE DEFAULT-<-1))
 (96 96 (:REWRITE DEFAULT-<-2))
 (51 39 (:LINEAR ASH-NEGATIVE-SHIFT-MAKES-INPUT-SMALLER))
 (31 31 (:LINEAR INDEX-OF-<-LEN))
 (18 8 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 (14 7 (:REWRITE DEFAULT-UNARY-MINUS))
 (8 1 (:REWRITE CONSP-OF-NTH-WHEN-ATOM-LISTP))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-ATOM-LISTP))
 (5 3 (:REWRITE DEFAULT-+-2))
 (4 3 (:REWRITE DEFAULT-+-1))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-STR))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-SSR))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-LIMIT))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-BASE))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-ACCESS))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-RGF))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-MEM))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-CTR))
 (3 1 (:REWRITE ATOM-LISTP-WHEN-NOT-CONSP))
 (2 2 (:TYPE-PRESCRIPTION ATOM-LISTP))
 (2 2 (:REWRITE ATOM-LISTP-WHEN-SUBSETP-EQUAL))
 )
(RM08-WM08-DIFFERENT-DIFFERENT-DWORD
 (132 3 (:LINEAR N05P-LOGAND-N05P-LESS-THAN-32))
 (132 3 (:LINEAR N04P-LOGAND-N04P-LESS-THAN-16))
 (132 3 (:LINEAR N03P-LOGAND-N03P-LESS-THAN-8))
 (132 3 (:LINEAR N02P-LOGAND-N02P-LESS-THAN-4))
 (129 3 (:LINEAR N01P-LOGAND-N01P-LESS-THAN-2))
 (104 57 (:REWRITE DEFAULT-<-1))
 (57 57 (:REWRITE DEFAULT-<-2))
 (45 37 (:LINEAR ASH-NEGATIVE-SHIFT-MAKES-INPUT-SMALLER))
 (12 6 (:REWRITE DEFAULT-UNARY-MINUS))
 (10 10 (:LINEAR INDEX-OF-<-LEN))
 (3 2 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 (3 2 (:REWRITE DEFAULT-+-2))
 (3 2 (:REWRITE DEFAULT-+-1))
 )
(RM08-WM08-DIFFERENT)
(RM08-WM08
 (30 30 (:LINEAR INDEX-OF-<-LEN))
 (16 16 (:REWRITE DEFAULT-<-2))
 (16 16 (:REWRITE DEFAULT-<-1))
 (9 5 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 )
(RM16-WM16-SAME-LEMMA-1
 (1 1 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM16-WM16-SAME-LEMMA-2
 (1 1 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM16-WM16-SAME-LEMMA-3
 (1 1 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM16-WM16-SAME-LEMMA-4
 (3 3 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM16-WM16-SAME
 (44 30 (:REWRITE DEFAULT-<-1))
 (30 30 (:REWRITE DEFAULT-<-2))
 (30 30 (:LINEAR INDEX-OF-<-LEN))
 (29 6 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 (14 12 (:REWRITE DEFAULT-+-2))
 (14 2 (:LINEAR N01P-LOGAND-N01P-LESS-THAN-2))
 (13 12 (:REWRITE DEFAULT-+-1))
 (10 5 (:REWRITE DEFAULT-UNARY-MINUS))
 )
(HACK1
 (4 4 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(HACK2
 (1 1 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM32-WM32-SAME
 (67 6 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 (62 36 (:REWRITE DEFAULT-<-1))
 (39 25 (:REWRITE DEFAULT-+-2))
 (36 36 (:REWRITE DEFAULT-<-2))
 (30 30 (:LINEAR INDEX-OF-<-LEN))
 (29 25 (:REWRITE DEFAULT-+-1))
 (17 12 (:REWRITE DEFAULT-UNARY-MINUS))
 (14 2 (:LINEAR N01P-LOGAND-N01P-LESS-THAN-2))
 (2 2 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(HACK3
 (2 2 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(HACK4
 (2 2 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(HACK5
 (2 2 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(HACK6
 (2 2 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(HACK7
 (2 2 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(HACK8
 (4 4 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM32-WM32-DIFFERENT-I<J
 (6496 136 (:DEFINITION NATP))
 (3136 224 (:REWRITE NATP-MEMI-WHEN-N30P-ADDR))
 (1139 617 (:REWRITE DEFAULT-<-1))
 (617 617 (:REWRITE DEFAULT-<-2))
 (600 8 (:LINEAR N64P-LOGIOR-N64P-LESS-THAN-18446744073709551616))
 (600 8 (:LINEAR N48P-LOGIOR-N48P-LESS-THAN-281474976710656))
 (600 8 (:LINEAR N32P-LOGIOR-N32P-LESS-THAN-4294967296))
 (600 8 (:LINEAR N30P-LOGIOR-N30P-LESS-THAN-1073741824))
 (600 8 (:LINEAR N24P-LOGIOR-N24P-LESS-THAN-16777216))
 (600 8 (:LINEAR N20P-LOGIOR-N20P-LESS-THAN-1048576))
 (600 8 (:LINEAR N16P-LOGIOR-N16P-LESS-THAN-65536))
 (600 8 (:LINEAR N12P-LOGIOR-N12P-LESS-THAN-4096))
 (600 8 (:LINEAR N08P-LOGIOR-N08P-LESS-THAN-256))
 (600 8 (:LINEAR N05P-LOGIOR-N05P-LESS-THAN-32))
 (600 8 (:LINEAR N04P-LOGIOR-N04P-LESS-THAN-16))
 (600 8 (:LINEAR N03P-LOGIOR-N03P-LESS-THAN-8))
 (600 8 (:LINEAR N02P-LOGIOR-N02P-LESS-THAN-4))
 (600 8 (:LINEAR N01P-LOGIOR-N01P-LESS-THAN-2))
 (436 8 (:LINEAR LOGIOR-LESS-THAN-OR-EQUAL))
 (436 8 (:LINEAR LOGIOR-GREATER-OR-EQUAL-TO-ZERO))
 (116 80 (:REWRITE DEFAULT-+-2))
 (108 11 (:LINEAR N01P-LOGAND-N01P-LESS-THAN-2))
 (99 19 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 (87 80 (:REWRITE DEFAULT-+-1))
 (61 61 (:LINEAR INDEX-OF-<-LEN))
 (45 32 (:REWRITE DEFAULT-UNARY-MINUS))
 (2 2 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(HACK9
 (2 2 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(HACK10
 (4 4 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(HACK11
 (2 2 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM32-WM32-DIFFERENT-J<I
 (24576 184 (:DEFINITION NATP))
 (3323 1457 (:REWRITE DEFAULT-<-1))
 (3136 224 (:REWRITE NATP-MEMI-WHEN-N30P-ADDR))
 (2832 64 (:LINEAR N64P-LOGIOR-N64P-LESS-THAN-18446744073709551616))
 (2832 64 (:LINEAR N48P-LOGIOR-N48P-LESS-THAN-281474976710656))
 (2832 64 (:LINEAR N32P-LOGIOR-N32P-LESS-THAN-4294967296))
 (2832 64 (:LINEAR N30P-LOGIOR-N30P-LESS-THAN-1073741824))
 (2832 64 (:LINEAR N24P-LOGIOR-N24P-LESS-THAN-16777216))
 (2832 64 (:LINEAR N20P-LOGIOR-N20P-LESS-THAN-1048576))
 (2832 64 (:LINEAR N16P-LOGIOR-N16P-LESS-THAN-65536))
 (2832 64 (:LINEAR N12P-LOGIOR-N12P-LESS-THAN-4096))
 (2832 64 (:LINEAR N08P-LOGIOR-N08P-LESS-THAN-256))
 (2832 64 (:LINEAR N05P-LOGIOR-N05P-LESS-THAN-32))
 (2832 64 (:LINEAR N04P-LOGIOR-N04P-LESS-THAN-16))
 (2832 64 (:LINEAR N03P-LOGIOR-N03P-LESS-THAN-8))
 (2832 64 (:LINEAR N02P-LOGIOR-N02P-LESS-THAN-4))
 (2832 64 (:LINEAR N01P-LOGIOR-N01P-LESS-THAN-2))
 (1457 1457 (:REWRITE DEFAULT-<-2))
 (784 64 (:LINEAR LOGIOR-LESS-THAN-OR-EQUAL))
 (784 64 (:LINEAR LOGIOR-GREATER-OR-EQUAL-TO-ZERO))
 (116 80 (:REWRITE DEFAULT-+-2))
 (108 11 (:LINEAR N01P-LOGAND-N01P-LESS-THAN-2))
 (97 19 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 (87 80 (:REWRITE DEFAULT-+-1))
 (61 61 (:LINEAR INDEX-OF-<-LEN))
 (49 34 (:REWRITE DEFAULT-UNARY-MINUS))
 (2 2 (:TYPE-PRESCRIPTION BOOLEANP))
 )
(RM32-WM32-DIFFERENT)
(RM32-WM32-NO-OVERLAP
 (10 10 (:REWRITE DEFAULT-<-2))
 (10 10 (:REWRITE DEFAULT-<-1))
 (10 10 (:LINEAR INDEX-OF-<-LEN))
 (4 4 (:REWRITE DEFAULT-+-2))
 (4 4 (:REWRITE DEFAULT-+-1))
 )
(HACK12
 (2 2 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(HACK13
 (2 2 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(HACK14
 (1 1 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(HACK15
 (1 1 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(HACK16
 (2 2 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(HACK17
 (4 4 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 (1 1 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-LIST-OF-G-BOOLEANS))
 (1 1 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-ATOM))
 )
(HACK18
 (4 4 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 (1 1 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-LIST-OF-G-BOOLEANS))
 (1 1 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-ATOM))
 )
(HACK19
 (4 4 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 (1 1 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-LIST-OF-G-BOOLEANS))
 (1 1 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-ATOM))
 )
(HACK20
 (3 3 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 (2 2 (:TYPE-PRESCRIPTION N32P-ASH--2-IS-N30P))
 (2 2 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-LIST-OF-G-BOOLEANS))
 (2 2 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-ATOM))
 )
(HACK21
 (3 3 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 (2 2 (:TYPE-PRESCRIPTION N32P-ASH--2-IS-N30P))
 (2 2 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-LIST-OF-G-BOOLEANS))
 (2 2 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-ATOM))
 )
(HACK22
 (3 3 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 (2 2 (:TYPE-PRESCRIPTION N32P-ASH--2-IS-N30P))
 (2 2 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-LIST-OF-G-BOOLEANS))
 (2 2 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-ATOM))
 )
(RM32-RM08
 (15976 80 (:DEFINITION NATP))
 (8724 60 (:LINEAR LOGIOR-LESS-THAN-OR-EQUAL))
 (8724 60 (:LINEAR LOGIOR-GREATER-OR-EQUAL-TO-ZERO))
 (2326 1000 (:REWRITE DEFAULT-<-1))
 (1248 60 (:LINEAR N64P-LOGIOR-N64P-LESS-THAN-18446744073709551616))
 (1248 60 (:LINEAR N48P-LOGIOR-N48P-LESS-THAN-281474976710656))
 (1248 60 (:LINEAR N32P-LOGIOR-N32P-LESS-THAN-4294967296))
 (1248 60 (:LINEAR N30P-LOGIOR-N30P-LESS-THAN-1073741824))
 (1248 60 (:LINEAR N24P-LOGIOR-N24P-LESS-THAN-16777216))
 (1248 60 (:LINEAR N20P-LOGIOR-N20P-LESS-THAN-1048576))
 (1248 60 (:LINEAR N16P-LOGIOR-N16P-LESS-THAN-65536))
 (1248 60 (:LINEAR N12P-LOGIOR-N12P-LESS-THAN-4096))
 (1248 60 (:LINEAR N08P-LOGIOR-N08P-LESS-THAN-256))
 (1248 60 (:LINEAR N05P-LOGIOR-N05P-LESS-THAN-32))
 (1248 60 (:LINEAR N04P-LOGIOR-N04P-LESS-THAN-16))
 (1248 60 (:LINEAR N03P-LOGIOR-N03P-LESS-THAN-8))
 (1248 60 (:LINEAR N02P-LOGIOR-N02P-LESS-THAN-4))
 (1248 60 (:LINEAR N01P-LOGIOR-N01P-LESS-THAN-2))
 (1000 1000 (:REWRITE DEFAULT-<-2))
 (167 41 (:LINEAR N01P-LOGAND-N01P-LESS-THAN-2))
 (134 134 (:LINEAR INDEX-OF-<-LEN))
 (90 64 (:REWRITE DEFAULT-+-2))
 (76 38 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 (65 64 (:REWRITE DEFAULT-+-1))
 (46 24 (:REWRITE DEFAULT-UNARY-MINUS))
 (3 3 (:REWRITE SUBSETP-MEMBER . 4))
 (3 3 (:REWRITE SUBSETP-MEMBER . 3))
 (3 3 (:REWRITE SUBSETP-MEMBER . 2))
 (3 3 (:REWRITE SUBSETP-MEMBER . 1))
 (3 3 (:REWRITE INTERSECTP-MEMBER . 3))
 (3 3 (:REWRITE INTERSECTP-MEMBER . 2))
 )
(ASH--2-MONOTONE
 (2 2 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(+-ASSOC-CONSTANTS)
(LOGIOR-COMMUTATIVE
 (136 4 (:DEFINITION NATP))
 (72 2 (:LINEAR LOGIOR-LESS-THAN-OR-EQUAL))
 (72 2 (:LINEAR LOGIOR-GREATER-OR-EQUAL-TO-ZERO))
 (68 34 (:TYPE-PRESCRIPTION LOGIOR-GREATER-OR-EQUAL-TO-ZERO))
 (52 52 (:REWRITE REDUCE-INTEGERP-+))
 (52 52 (:REWRITE INTEGERP-MINUS-X))
 (52 52 (:META META-INTEGERP-CORRECT))
 (38 38 (:TYPE-PRESCRIPTION NATP))
 (34 34 (:TYPE-PRESCRIPTION |(< 0 (logior x y))| . 2))
 (34 34 (:TYPE-PRESCRIPTION |(< 0 (logior x y))| . 1))
 (34 34 (:TYPE-PRESCRIPTION |(< (logior x y) 0)| . 2))
 (34 34 (:TYPE-PRESCRIPTION |(< (logior x y) 0)| . 1))
 (8 2 (:LINEAR N64P-LOGIOR-N64P-LESS-THAN-18446744073709551616))
 (8 2 (:LINEAR N48P-LOGIOR-N48P-LESS-THAN-281474976710656))
 (8 2 (:LINEAR N32P-LOGIOR-N32P-LESS-THAN-4294967296))
 (8 2 (:LINEAR N30P-LOGIOR-N30P-LESS-THAN-1073741824))
 (8 2 (:LINEAR N24P-LOGIOR-N24P-LESS-THAN-16777216))
 (8 2 (:LINEAR N20P-LOGIOR-N20P-LESS-THAN-1048576))
 (8 2 (:LINEAR N16P-LOGIOR-N16P-LESS-THAN-65536))
 (8 2 (:LINEAR N12P-LOGIOR-N12P-LESS-THAN-4096))
 (8 2 (:LINEAR N08P-LOGIOR-N08P-LESS-THAN-256))
 (8 2 (:LINEAR N05P-LOGIOR-N05P-LESS-THAN-32))
 (8 2 (:LINEAR N04P-LOGIOR-N04P-LESS-THAN-16))
 (8 2 (:LINEAR N03P-LOGIOR-N03P-LESS-THAN-8))
 (8 2 (:LINEAR N02P-LOGIOR-N02P-LESS-THAN-4))
 (8 2 (:LINEAR N01P-LOGIOR-N01P-LESS-THAN-2))
 (8 2 (:LINEAR LOGIOR-BOUNDS-POS . 2))
 (8 2 (:LINEAR LOGIOR-BOUNDS-POS . 1))
 (8 2 (:LINEAR LOGIOR-BOUNDS-NEG . 2))
 (8 2 (:LINEAR LOGIOR-BOUNDS-NEG . 1))
 (4 4 (:REWRITE THE-FLOOR-BELOW))
 (4 4 (:REWRITE THE-FLOOR-ABOVE))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (4 4 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (4 4 (:REWRITE SIMPLIFY-SUMS-<))
 (4 4 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (4 4 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (4 4 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (4 4 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (4 4 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (4 4 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (4 4 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (4 4 (:REWRITE INTEGERP-<-CONSTANT))
 (4 4 (:REWRITE DEFAULT-LESS-THAN-2))
 (4 4 (:REWRITE DEFAULT-LESS-THAN-1))
 (4 4 (:REWRITE CONSTANT-<-INTEGERP))
 (4 4 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (4 4 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (4 4 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (4 4 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (4 4 (:REWRITE |(< c (- x))|))
 (4 4 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (4 4 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (4 4 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (4 4 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (4 4 (:REWRITE |(< (/ x) 0)|))
 (4 4 (:REWRITE |(< (/ x) (/ y))|))
 (4 4 (:REWRITE |(< (- x) c)|))
 (4 4 (:REWRITE |(< (- x) (- y))|))
 (4 4 (:REWRITE |(< (* x y) 0)|))
 )
(LOGIOR-ASSOCIATIVE
 (24 12 (:TYPE-PRESCRIPTION LOGIOR-GREATER-OR-EQUAL-TO-ZERO))
 (12 12 (:TYPE-PRESCRIPTION NATP))
 (12 12 (:TYPE-PRESCRIPTION |(< 0 (logior x y))| . 1))
 (12 12 (:TYPE-PRESCRIPTION |(< (logior x y) 0)| . 2))
 (12 12 (:TYPE-PRESCRIPTION |(< (logior x y) 0)| . 1))
 )
(LOGIOR-COMMUTATIVE-2
 (632 20 (:DEFINITION NATP))
 (544 272 (:TYPE-PRESCRIPTION LOGIOR-GREATER-OR-EQUAL-TO-ZERO))
 (336 10 (:LINEAR LOGIOR-LESS-THAN-OR-EQUAL))
 (336 10 (:LINEAR LOGIOR-GREATER-OR-EQUAL-TO-ZERO))
 (292 292 (:TYPE-PRESCRIPTION NATP))
 (272 272 (:TYPE-PRESCRIPTION |(< 0 (logior x y))| . 1))
 (272 272 (:TYPE-PRESCRIPTION |(< (logior x y) 0)| . 2))
 (272 272 (:TYPE-PRESCRIPTION |(< (logior x y) 0)| . 1))
 (270 10 (:LINEAR LOGIOR-BOUNDS-POS . 2))
 (270 10 (:LINEAR LOGIOR-BOUNDS-POS . 1))
 (262 10 (:LINEAR LOGIOR-BOUNDS-NEG . 2))
 (262 10 (:LINEAR LOGIOR-BOUNDS-NEG . 1))
 (256 10 (:LINEAR N64P-LOGIOR-N64P-LESS-THAN-18446744073709551616))
 (256 10 (:LINEAR N48P-LOGIOR-N48P-LESS-THAN-281474976710656))
 (256 10 (:LINEAR N32P-LOGIOR-N32P-LESS-THAN-4294967296))
 (256 10 (:LINEAR N30P-LOGIOR-N30P-LESS-THAN-1073741824))
 (256 10 (:LINEAR N24P-LOGIOR-N24P-LESS-THAN-16777216))
 (256 10 (:LINEAR N20P-LOGIOR-N20P-LESS-THAN-1048576))
 (256 10 (:LINEAR N16P-LOGIOR-N16P-LESS-THAN-65536))
 (256 10 (:LINEAR N12P-LOGIOR-N12P-LESS-THAN-4096))
 (256 10 (:LINEAR N08P-LOGIOR-N08P-LESS-THAN-256))
 (256 10 (:LINEAR N05P-LOGIOR-N05P-LESS-THAN-32))
 (256 10 (:LINEAR N04P-LOGIOR-N04P-LESS-THAN-16))
 (256 10 (:LINEAR N03P-LOGIOR-N03P-LESS-THAN-8))
 (256 10 (:LINEAR N02P-LOGIOR-N02P-LESS-THAN-4))
 (256 10 (:LINEAR N01P-LOGIOR-N01P-LESS-THAN-2))
 (164 164 (:REWRITE THE-FLOOR-BELOW))
 (164 164 (:REWRITE THE-FLOOR-ABOVE))
 (164 164 (:REWRITE SIMPLIFY-SUMS-<))
 (164 164 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (164 164 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (164 164 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (164 164 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (164 164 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (164 164 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (164 164 (:REWRITE INTEGERP-<-CONSTANT))
 (164 164 (:REWRITE DEFAULT-LESS-THAN-2))
 (164 164 (:REWRITE DEFAULT-LESS-THAN-1))
 (164 164 (:REWRITE CONSTANT-<-INTEGERP))
 (164 164 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (164 164 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (164 164 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (164 164 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (164 164 (:REWRITE |(< c (- x))|))
 (164 164 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (164 164 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (164 164 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (164 164 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (164 164 (:REWRITE |(< (/ x) (/ y))|))
 (164 164 (:REWRITE |(< (- x) c)|))
 (164 164 (:REWRITE |(< (- x) (- y))|))
 (156 156 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (156 156 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (156 156 (:REWRITE |(< (/ x) 0)|))
 (156 156 (:REWRITE |(< (* x y) 0)|))
 (148 148 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (75 5 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (75 5 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (75 5 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (68 68 (:REWRITE REDUCE-INTEGERP-+))
 (68 68 (:REWRITE INTEGERP-MINUS-X))
 (68 68 (:META META-INTEGERP-CORRECT))
 (40 5 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 (8 8 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (8 8 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (8 8 (:REWRITE |(< 0 (/ x))|))
 (8 8 (:REWRITE |(< 0 (* x y))|))
 (5 5 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (5 5 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (5 5 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (5 5 (:REWRITE |(equal c (/ x))|))
 (5 5 (:REWRITE |(equal c (- x))|))
 (5 5 (:REWRITE |(equal (/ x) c)|))
 (5 5 (:REWRITE |(equal (/ x) (/ y))|))
 (5 5 (:REWRITE |(equal (- x) c)|))
 (5 5 (:REWRITE |(equal (- x) (- y))|))
 (3 3 (:REWRITE |(logior c d x)|))
 )
(RM08-WM32-HACK-1
 (4 4 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM08-WM32-HACK-2
 (4 4 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM08-WM32-HACK-3
 (4 4 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM08-WM32-HACK-4
 (4 4 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM08-WM32-HACK-5
 (4 4 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM08-WM32-HACK-6
 (4 4 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM08-WM32-HACK-7
 (4 4 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM08-WM32-HACK-8
 (3 3 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM08-WM32-HACK-8-A
 (1 1 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(ASH-0
 (66 2 (:LINEAR ASH-N02P-IS-ZERO-OR-POSITIVE))
 (62 2 (:DEFINITION NATP))
 (7 1 (:REWRITE DEFAULT-FLOOR-RATIO))
 (4 1 (:REWRITE |(* y x)|))
 (2 2 (:TYPE-PRESCRIPTION NATP))
 (2 2 (:REWRITE THE-FLOOR-BELOW))
 (2 2 (:REWRITE THE-FLOOR-ABOVE))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (2 2 (:REWRITE SIMPLIFY-SUMS-<))
 (2 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2 2 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (2 2 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (2 2 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (2 2 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (2 2 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (2 2 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (2 2 (:REWRITE INTEGERP-<-CONSTANT))
 (2 2 (:REWRITE DEFAULT-TIMES-2))
 (2 2 (:REWRITE DEFAULT-TIMES-1))
 (2 2 (:REWRITE DEFAULT-LESS-THAN-2))
 (2 2 (:REWRITE DEFAULT-LESS-THAN-1))
 (2 2 (:REWRITE CONSTANT-<-INTEGERP))
 (2 2 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (2 2 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (2 2 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (2 2 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (2 2 (:REWRITE |(< c (- x))|))
 (2 2 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (2 2 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (2 2 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (2 2 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (2 2 (:REWRITE |(< (/ x) 0)|))
 (2 2 (:REWRITE |(< (/ x) (/ y))|))
 (2 2 (:REWRITE |(< (- x) c)|))
 (2 2 (:REWRITE |(< (- x) (- y))|))
 (2 2 (:REWRITE |(< (* x y) 0)|))
 (2 2 (:LINEAR ASH-NEGATIVE-SHIFT-MAKES-INPUT-SMALLER))
 (1 1 (:REWRITE REDUCE-INTEGERP-+))
 (1 1 (:REWRITE INTEGERP-MINUS-X))
 (1 1 (:REWRITE DEFAULT-FLOOR-2))
 (1 1 (:REWRITE DEFAULT-FLOOR-1))
 (1 1 (:REWRITE |(* 1 x)|))
 (1 1 (:META META-INTEGERP-CORRECT))
 )
(RM08-WM32-HACK-9
 (1 1 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM08-WM32-HACK-10
 (2 2 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM08-WM32-HACK-11
 (4 4 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM08-WM32-HACK-12
 (4 4 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM08-WM32
 (8964 6270 (:REWRITE DEFAULT-<-1))
 (7833 197 (:LINEAR N01P-LOGAND-N01P-LESS-THAN-2))
 (7060 840 (:TYPE-PRESCRIPTION LOGIOR-GREATER-OR-EQUAL-TO-ZERO))
 (6272 6270 (:REWRITE DEFAULT-<-2))
 (5240 140 (:REWRITE RM08-WM32-HACK-1))
 (1732 1732 (:TYPE-PRESCRIPTION NATP))
 (1300 20 (:REWRITE X86-32P-!MEMI-N30P))
 (1196 7 (:REWRITE HACK20))
 (1004 611 (:REWRITE DEFAULT-+-2))
 (840 840 (:TYPE-PRESCRIPTION BINARY-LOGIOR))
 (612 611 (:REWRITE DEFAULT-+-1))
 (590 590 (:TYPE-PRESCRIPTION !MEMI))
 (504 3 (:REWRITE HACK22))
 (266 266 (:LINEAR INDEX-OF-<-LEN))
 (237 139 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 (128 1 (:REWRITE HACK21))
 (100 100 (:TYPE-PRESCRIPTION BINARY-LOGAND))
 (98 61 (:REWRITE DEFAULT-UNARY-MINUS))
 (25 5 (:REWRITE HACK9))
 (25 5 (:REWRITE HACK3))
 (16 2 (:REWRITE CONSP-OF-NTH-WHEN-ATOM-LISTP))
 (12 12 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-ATOM-LISTP))
 (11 5 (:REWRITE HACK4))
 (10 2 (:REWRITE HACK10))
 (8 4 (:TYPE-PRESCRIPTION NATP-NTH-OF-STR))
 (8 4 (:TYPE-PRESCRIPTION NATP-NTH-OF-SSR))
 (8 4 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-LIMIT))
 (8 4 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-BASE))
 (8 4 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-ACCESS))
 (8 4 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG))
 (8 4 (:TYPE-PRESCRIPTION NATP-NTH-OF-RGF))
 (8 4 (:TYPE-PRESCRIPTION NATP-NTH-OF-MEM))
 (8 4 (:TYPE-PRESCRIPTION NATP-NTH-OF-CTR))
 (6 2 (:REWRITE ATOM-LISTP-WHEN-NOT-CONSP))
 (4 4 (:TYPE-PRESCRIPTION ATOM-LISTP))
 (4 4 (:REWRITE ATOM-LISTP-WHEN-SUBSETP-EQUAL))
 (3 3 (:REWRITE SUBSETP-MEMBER . 4))
 (3 3 (:REWRITE SUBSETP-MEMBER . 3))
 (3 3 (:REWRITE SUBSETP-MEMBER . 2))
 (3 3 (:REWRITE SUBSETP-MEMBER . 1))
 (3 3 (:REWRITE INTERSECTP-MEMBER . 3))
 (3 3 (:REWRITE INTERSECTP-MEMBER . 2))
 )
(RM32-WM32-HACK1
 (3 3 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM32-WM32-HACK2
 (2 2 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM32-WM32-HACK3
 (1 1 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM32-WM32-HACK4
 (2 2 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM32-WM32-HACK5
 (3 3 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM32-WM32
 (11016 3128 (:LINEAR ASH-N02P-IS-ZERO-OR-POSITIVE))
 (6496 124 (:LINEAR N08P-LOGIOR-N08P-LESS-THAN-256))
 (6458 124 (:LINEAR N12P-LOGIOR-N12P-LESS-THAN-4096))
 (6420 124 (:LINEAR N16P-LOGIOR-N16P-LESS-THAN-65536))
 (6382 124 (:LINEAR N20P-LOGIOR-N20P-LESS-THAN-1048576))
 (6344 124 (:LINEAR N24P-LOGIOR-N24P-LESS-THAN-16777216))
 (6306 124 (:LINEAR N30P-LOGIOR-N30P-LESS-THAN-1073741824))
 (6268 124 (:LINEAR N32P-LOGIOR-N32P-LESS-THAN-4294967296))
 (6230 124 (:LINEAR N48P-LOGIOR-N48P-LESS-THAN-281474976710656))
 (6192 124 (:LINEAR N64P-LOGIOR-N64P-LESS-THAN-18446744073709551616))
 (5640 2502 (:REWRITE DEFAULT-<-1))
 (3516 124 (:LINEAR N05P-LOGIOR-N05P-LESS-THAN-32))
 (3516 124 (:LINEAR N04P-LOGIOR-N04P-LESS-THAN-16))
 (3516 124 (:LINEAR N03P-LOGIOR-N03P-LESS-THAN-8))
 (3516 124 (:LINEAR N02P-LOGIOR-N02P-LESS-THAN-4))
 (3516 124 (:LINEAR N01P-LOGIOR-N01P-LESS-THAN-2))
 (2502 2502 (:REWRITE DEFAULT-<-2))
 (2168 1768 (:LINEAR ASH-NEGATIVE-SHIFT-MAKES-INPUT-SMALLER))
 (1096 124 (:LINEAR LOGIOR-LESS-THAN-OR-EQUAL))
 (1096 124 (:LINEAR LOGIOR-GREATER-OR-EQUAL-TO-ZERO))
 (830 30 (:LINEAR N05P-LOGAND-N05P-LESS-THAN-32))
 (830 30 (:LINEAR N04P-LOGAND-N04P-LESS-THAN-16))
 (830 30 (:LINEAR N03P-LOGAND-N03P-LESS-THAN-8))
 (830 30 (:LINEAR N02P-LOGAND-N02P-LESS-THAN-4))
 (810 30 (:LINEAR N01P-LOGAND-N01P-LESS-THAN-2))
 (522 84 (:LINEAR N64P-LOGAND-N64P-LESS-THAN-18446744073709551616))
 (484 78 (:LINEAR N48P-LOGAND-N48P-LESS-THAN-281474976710656))
 (446 72 (:LINEAR N32P-LOGAND-N32P-LESS-THAN-4294967296))
 (408 66 (:LINEAR N30P-LOGAND-N30P-LESS-THAN-1073741824))
 (370 60 (:LINEAR N24P-LOGAND-N24P-LESS-THAN-16777216))
 (332 54 (:LINEAR N20P-LOGAND-N20P-LESS-THAN-1048576))
 (311 311 (:REWRITE DEFAULT-+-2))
 (311 311 (:REWRITE DEFAULT-+-1))
 (294 48 (:LINEAR N16P-LOGAND-N16P-LESS-THAN-65536))
 (256 42 (:LINEAR N12P-LOGAND-N12P-LESS-THAN-4096))
 (240 60 (:LINEAR LOGAND-LESS-THAN-OR-EQUAL))
 (218 36 (:LINEAR N08P-LOGAND-N08P-LESS-THAN-256))
 (161 97 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 (90 90 (:LINEAR INDEX-OF-<-LEN))
 )
(LOGAND-+1-3
 (4028 76 (:REWRITE CANCEL-MOD-+))
 (3230 314 (:REWRITE DEFAULT-PLUS-2))
 (2704 76 (:REWRITE MOD-X-Y-=-X-Y . 2))
 (2660 2660 (:TYPE-PRESCRIPTION NOT-INTEGERP-4B))
 (2660 2660 (:TYPE-PRESCRIPTION NOT-INTEGERP-3B))
 (2660 2660 (:TYPE-PRESCRIPTION NOT-INTEGERP-2B))
 (2660 2660 (:TYPE-PRESCRIPTION NOT-INTEGERP-1B))
 (2629 76 (:REWRITE MOD-X-Y-=-X . 3))
 (2086 76 (:REWRITE MOD-X-Y-=-X . 4))
 (1977 229 (:REWRITE INTEGERP-MINUS-X))
 (1930 386 (:TYPE-PRESCRIPTION MOD-ZERO . 2))
 (1930 386 (:TYPE-PRESCRIPTION MOD-ZERO . 1))
 (1930 386 (:TYPE-PRESCRIPTION MOD-POSITIVE . 2))
 (1930 386 (:TYPE-PRESCRIPTION MOD-NEGATIVE . 2))
 (1903 76 (:REWRITE MOD-ZERO . 3))
 (1692 267 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (1344 228 (:REWRITE |(* y x)|))
 (1292 152 (:REWRITE |(* (- x) y)|))
 (1174 76 (:REWRITE MOD-ZERO . 4))
 (1052 76 (:REWRITE DEFAULT-MOD-RATIO))
 (1044 314 (:REWRITE DEFAULT-PLUS-1))
 (771 267 (:REWRITE DEFAULT-LESS-THAN-1))
 (760 152 (:REWRITE DEFAULT-MINUS))
 (733 229 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (733 229 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (720 720 (:TYPE-PRESCRIPTION NOT-INTEGERP-4A))
 (720 720 (:TYPE-PRESCRIPTION NOT-INTEGERP-3A))
 (720 720 (:TYPE-PRESCRIPTION NOT-INTEGERP-2A))
 (720 720 (:TYPE-PRESCRIPTION NOT-INTEGERP-1A))
 (720 720 (:REWRITE DEFAULT-TIMES-2))
 (720 720 (:REWRITE DEFAULT-TIMES-1))
 (684 152 (:REWRITE |(- (* c x))|))
 (432 36 (:REWRITE |(* x (+ y z))|))
 (416 416 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (386 386 (:TYPE-PRESCRIPTION MOD-ZERO . 4))
 (386 386 (:TYPE-PRESCRIPTION MOD-ZERO . 3))
 (386 386 (:TYPE-PRESCRIPTION MOD-POSITIVE . 1))
 (386 386 (:TYPE-PRESCRIPTION MOD-NONPOSITIVE))
 (386 386 (:TYPE-PRESCRIPTION MOD-NEGATIVE . 1))
 (386 386 (:TYPE-PRESCRIPTION INTEGERP-MOD-2))
 (380 76 (:REWRITE MOD-X-Y-=-X-Y . 3))
 (380 76 (:REWRITE MOD-X-Y-=-X+Y . 3))
 (380 76 (:REWRITE MOD-X-Y-=-X+Y . 2))
 (380 76 (:REWRITE MOD-X-Y-=-X . 2))
 (380 76 (:REWRITE MOD-CANCEL-*-REWRITING-GOAL-LITERAL))
 (380 76 (:REWRITE |(mod (+ x (mod a b)) y)|))
 (380 76 (:REWRITE |(mod (+ x (- (mod a b))) y)|))
 (380 76 (:REWRITE |(mod (* x (/ y)) z) rewriting-goal-literal|))
 (267 267 (:REWRITE THE-FLOOR-BELOW))
 (267 267 (:REWRITE THE-FLOOR-ABOVE))
 (267 267 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (267 267 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (267 267 (:REWRITE DEFAULT-LESS-THAN-2))
 (229 229 (:REWRITE SIMPLIFY-SUMS-<))
 (229 229 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (229 229 (:REWRITE INTEGERP-<-CONSTANT))
 (229 229 (:REWRITE CONSTANT-<-INTEGERP))
 (229 229 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (229 229 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (229 229 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (229 229 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (229 229 (:REWRITE |(< c (- x))|))
 (229 229 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (229 229 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (229 229 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (229 229 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (229 229 (:REWRITE |(< (/ x) (/ y))|))
 (229 229 (:REWRITE |(< (- x) c)|))
 (229 229 (:REWRITE |(< (- x) (- y))|))
 (228 76 (:REWRITE MOD-CANCEL-*-CONST))
 (153 153 (:REWRITE REDUCE-INTEGERP-+))
 (153 153 (:META META-INTEGERP-CORRECT))
 (152 152 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (151 151 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (145 61 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (145 61 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (120 1 (:LINEAR N01P-LOGAND-N01P-LESS-THAN-2))
 (88 63 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (88 60 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 (78 78 (:TYPE-PRESCRIPTION |(< (logand x y) 0)| . 1))
 (76 76 (:REWRITE MOD-CANCEL-*-NOT-REWRITING-GOAL-LITERAL))
 (76 76 (:REWRITE DEFAULT-MOD-2))
 (76 76 (:REWRITE DEFAULT-MOD-1))
 (76 76 (:REWRITE |(mod x (- y))| . 3))
 (76 76 (:REWRITE |(mod x (- y))| . 2))
 (76 76 (:REWRITE |(mod x (- y))| . 1))
 (76 76 (:REWRITE |(mod x (* y (/ z))) rewriting-goal-literal|))
 (76 76 (:REWRITE |(mod x (* y (/ z))) not rewriting-goal-literal|))
 (76 76 (:REWRITE |(mod (- x) y)| . 3))
 (76 76 (:REWRITE |(mod (- x) y)| . 2))
 (76 76 (:REWRITE |(mod (- x) y)| . 1))
 (76 76 (:REWRITE |(mod (* x (/ y)) z) not rewriting-goal-literal|))
 (63 63 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (61 61 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (61 61 (:REWRITE |(equal c (/ x))|))
 (61 61 (:REWRITE |(equal c (- x))|))
 (61 61 (:REWRITE |(equal (/ x) c)|))
 (61 61 (:REWRITE |(equal (/ x) (/ y))|))
 (61 61 (:REWRITE |(equal (- x) c)|))
 (61 61 (:REWRITE |(equal (- x) (- y))|))
 (58 58 (:REWRITE THIS-NEEDS-TO-BE-ADDED-TO-QUOTIENT-REMAINDER-LEMMAS))
 (58 58 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-=-0))
 (58 2 (:TYPE-PRESCRIPTION BUBBLE-DOWN))
 (57 57 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (57 57 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (57 57 (:REWRITE |(< 0 (/ x))|))
 (57 57 (:REWRITE |(< 0 (* x y))|))
 (56 56 (:REWRITE |(< (+ c/d x) y)|))
 (40 40 (:REWRITE DEFAULT-LOGAND-2))
 (40 40 (:REWRITE DEFAULT-LOGAND-1))
 (39 39 (:REWRITE |(+ 0 x)|))
 (33 1 (:REWRITE MOD-X-Y-=-X-Y . 1))
 (22 1 (:LINEAR MOD-BOUNDS-3))
 (21 1 (:REWRITE MOD-X-Y-=-X+Y . 1))
 (20 20 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NONPOSITIVE-BASE-ODD-EXPONENT))
 (20 20 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NONPOSITIVE-BASE-EVEN-EXPONENT))
 (20 20 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NEGATIVE-BASE-ODD-EXPONENT))
 (20 20 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NEGATIVE-BASE-EVEN-EXPONENT))
 (20 20 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-INTEGERP-BASE-B))
 (20 20 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-INTEGERP-BASE-A))
 (18 18 (:REWRITE REDUCE-INTEGERP-+-CONSTANT))
 (18 18 (:REWRITE INTEGERP-+-REDUCE-CONSTANT))
 (18 18 (:REWRITE |(< (+ (- c) x) y)|))
 (10 2 (:LINEAR MOD-BOUNDS-2))
 (2 2 (:REWRITE |(equal (+ (- c) x) y)|))
 (2 2 (:REWRITE |(< (* x y) 0)|))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (1 1 (:REWRITE |(equal (mod (+ x y) z) x)|))
 (1 1 (:REWRITE |(< (/ x) 0)|))
 (1 1 (:LINEAR LOGAND-BOUNDS-NEG . 2))
 (1 1 (:LINEAR LOGAND-BOUNDS-NEG . 1))
 )
(LOGAND-<-EXPT-32-IDENTITY
 (1 1 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(ASH-+1--2
 (11532 4 (:REWRITE FLOOR-=-X/Y . 4))
 (6884 15 (:LINEAR LINEAR-FLOOR-BOUNDS-1))
 (3080 3080 (:TYPE-PRESCRIPTION NOT-INTEGERP-4B))
 (3080 3080 (:TYPE-PRESCRIPTION NOT-INTEGERP-3B))
 (3080 3080 (:TYPE-PRESCRIPTION NOT-INTEGERP-2B))
 (3080 3080 (:TYPE-PRESCRIPTION NOT-INTEGERP-1B))
 (1658 62 (:REWRITE DEFAULT-PLUS-2))
 (1586 122 (:TYPE-PRESCRIPTION FLOOR-ZERO . 2))
 (1424 62 (:REWRITE DEFAULT-PLUS-1))
 (1393 20 (:REWRITE FLOOR-ZERO . 3))
 (1098 122 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 1))
 (1098 122 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 1))
 (1098 122 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 1))
 (1060 20 (:REWRITE CANCEL-FLOOR-+))
 (717 12 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (717 12 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (670 20 (:REWRITE FLOOR-ZERO . 5))
 (662 110 (:REWRITE INTEGERP-MINUS-X))
 (636 147 (:REWRITE |(* y x)|))
 (635 20 (:REWRITE FLOOR-X-Y-=-1 . 2))
 (621 20 (:REWRITE FLOOR-ZERO . 4))
 (610 122 (:TYPE-PRESCRIPTION FLOOR-ZERO . 4))
 (610 122 (:TYPE-PRESCRIPTION FLOOR-ZERO . 3))
 (610 122 (:TYPE-PRESCRIPTION FLOOR-ZERO . 1))
 (610 122 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 3))
 (610 122 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 2))
 (610 122 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 3))
 (610 122 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 2))
 (610 122 (:TYPE-PRESCRIPTION FLOOR-NONNEGATIVE . 3))
 (610 122 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 3))
 (610 122 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 2))
 (464 464 (:TYPE-PRESCRIPTION NOT-INTEGERP-4A))
 (464 464 (:TYPE-PRESCRIPTION NOT-INTEGERP-3A))
 (464 464 (:TYPE-PRESCRIPTION NOT-INTEGERP-2A))
 (464 464 (:TYPE-PRESCRIPTION NOT-INTEGERP-1A))
 (454 20 (:REWRITE FLOOR-=-X/Y . 3))
 (454 20 (:REWRITE FLOOR-=-X/Y . 2))
 (408 48 (:REWRITE |(* (- x) y)|))
 (384 4 (:TYPE-PRESCRIPTION BUBBLE-DOWN))
 (380 372 (:REWRITE DEFAULT-TIMES-2))
 (372 372 (:REWRITE DEFAULT-TIMES-1))
 (275 55 (:TYPE-PRESCRIPTION MOD-ZERO . 2))
 (275 55 (:TYPE-PRESCRIPTION MOD-ZERO . 1))
 (275 55 (:TYPE-PRESCRIPTION MOD-POSITIVE . 2))
 (275 55 (:TYPE-PRESCRIPTION MOD-NEGATIVE . 2))
 (240 48 (:REWRITE DEFAULT-MINUS))
 (232 20 (:REWRITE DEFAULT-FLOOR-RATIO))
 (216 48 (:REWRITE |(- (* c x))|))
 (212 4 (:REWRITE CANCEL-MOD-+))
 (208 8 (:LINEAR LINEAR-FLOOR-BOUNDS-3))
 (206 94 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (203 95 (:REWRITE DEFAULT-LESS-THAN-1))
 (200 200 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (195 91 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (179 91 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (176 8 (:LINEAR LINEAR-FLOOR-BOUNDS-2))
 (169 10 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 (113 94 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (113 94 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (106 4 (:REWRITE MOD-X-Y-=-X . 4))
 (100 20 (:REWRITE FLOOR-ZERO . 2))
 (100 20 (:REWRITE FLOOR-X-Y-=-1 . 3))
 (100 20 (:REWRITE FLOOR-X-Y-=--1 . 3))
 (100 20 (:REWRITE FLOOR-X-Y-=--1 . 2))
 (100 20 (:REWRITE FLOOR-CANCEL-*-CONST))
 (95 95 (:REWRITE THE-FLOOR-BELOW))
 (95 95 (:REWRITE THE-FLOOR-ABOVE))
 (95 95 (:REWRITE DEFAULT-LESS-THAN-2))
 (94 4 (:REWRITE MOD-X-Y-=-X-Y . 2))
 (91 91 (:REWRITE SIMPLIFY-SUMS-<))
 (91 91 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (91 91 (:REWRITE INTEGERP-<-CONSTANT))
 (91 91 (:REWRITE CONSTANT-<-INTEGERP))
 (91 91 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (91 91 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (91 91 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (91 91 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (91 91 (:REWRITE |(< c (- x))|))
 (91 91 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (91 91 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (91 91 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (91 91 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (91 91 (:REWRITE |(< (/ x) (/ y))|))
 (91 91 (:REWRITE |(< (- x) c)|))
 (91 91 (:REWRITE |(< (- x) (- y))|))
 (91 4 (:REWRITE MOD-X-Y-=-X . 3))
 (86 86 (:REWRITE REDUCE-INTEGERP-+))
 (86 86 (:META META-INTEGERP-CORRECT))
 (80 20 (:REWRITE FLOOR-CANCEL-*-NOT-REWRITING-GOAL-LITERAL))
 (80 20 (:REWRITE |(floor (* x (/ y)) z) not rewriting-goal-literal|))
 (77 5 (:REWRITE |(< (+ c/d x) y)|))
 (67 4 (:REWRITE MOD-ZERO . 3))
 (66 2 (:REWRITE MOD-X-Y-=-X-Y . 1))
 (60 5 (:REWRITE |(* x (+ y z))|))
 (58 15 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (58 4 (:REWRITE MOD-ZERO . 4))
 (55 55 (:TYPE-PRESCRIPTION MOD-ZERO . 4))
 (55 55 (:TYPE-PRESCRIPTION MOD-ZERO . 3))
 (55 55 (:TYPE-PRESCRIPTION MOD-POSITIVE . 1))
 (55 55 (:TYPE-PRESCRIPTION MOD-NONPOSITIVE))
 (55 55 (:TYPE-PRESCRIPTION MOD-NEGATIVE . 1))
 (55 55 (:TYPE-PRESCRIPTION INTEGERP-MOD-2))
 (44 4 (:REWRITE DEFAULT-MOD-RATIO))
 (41 41 (:TYPE-PRESCRIPTION ABS))
 (41 41 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (40 20 (:REWRITE FLOOR-CANCEL-*-REWRITING-GOAL-LITERAL))
 (40 20 (:REWRITE |(floor (* x (/ y)) z) rewriting-goal-literal|))
 (27 27 (:TYPE-PRESCRIPTION |(< (logand x y) 0)| . 1))
 (26 1 (:REWRITE |(floor (+ x r) i)|))
 (25 6 (:REWRITE |(+ c (+ d x))|))
 (24 24 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (22 22 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (22 22 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (22 22 (:REWRITE |(< 0 (/ x))|))
 (22 22 (:REWRITE |(< 0 (* x y))|))
 (22 2 (:REWRITE MOD-X-Y-=-X+Y . 1))
 (22 1 (:LINEAR MOD-BOUNDS-3))
 (20 20 (:REWRITE DEFAULT-FLOOR-2))
 (20 20 (:REWRITE DEFAULT-FLOOR-1))
 (20 20 (:REWRITE |(floor x (- y))| . 2))
 (20 20 (:REWRITE |(floor x (- y))| . 1))
 (20 20 (:REWRITE |(floor x (* y (/ z))) rewriting-goal-literal|))
 (20 20 (:REWRITE |(floor x (* y (/ z))) not rewriting-goal-literal|))
 (20 20 (:REWRITE |(floor (- x) y)| . 2))
 (20 20 (:REWRITE |(floor (- x) y)| . 1))
 (20 4 (:REWRITE MOD-X-Y-=-X-Y . 3))
 (20 4 (:REWRITE MOD-X-Y-=-X+Y . 3))
 (20 4 (:REWRITE MOD-X-Y-=-X+Y . 2))
 (20 4 (:REWRITE MOD-X-Y-=-X . 2))
 (20 4 (:REWRITE MOD-CANCEL-*-REWRITING-GOAL-LITERAL))
 (20 4 (:REWRITE |(mod (+ x (mod a b)) y)|))
 (20 4 (:REWRITE |(mod (+ x (- (mod a b))) y)|))
 (20 4 (:REWRITE |(mod (* x (/ y)) z) rewriting-goal-literal|))
 (19 19 (:REWRITE |(< (* (/ x) y) 1) with (< x 0)|))
 (19 19 (:REWRITE |(< (* (/ x) y) 1) with (< 0 x)|))
 (18 15 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (16 4 (:REWRITE MOD-CANCEL-*-CONST))
 (15 3 (:REWRITE |(equal (floor (+ x y) z) x)|))
 (12 12 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (12 12 (:REWRITE |(equal c (/ x))|))
 (12 12 (:REWRITE |(equal c (- x))|))
 (12 12 (:REWRITE |(equal (/ x) c)|))
 (12 12 (:REWRITE |(equal (/ x) (/ y))|))
 (12 12 (:REWRITE |(equal (- x) c)|))
 (12 12 (:REWRITE |(equal (- x) (- y))|))
 (10 2 (:LINEAR MOD-BOUNDS-2))
 (5 5 (:REWRITE |(equal (+ (- c) x) y)|))
 (5 5 (:REWRITE |(+ 0 x)|))
 (4 4 (:REWRITE THIS-NEEDS-TO-BE-ADDED-TO-QUOTIENT-REMAINDER-LEMMAS))
 (4 4 (:REWRITE MOD-CANCEL-*-NOT-REWRITING-GOAL-LITERAL))
 (4 4 (:REWRITE DEFAULT-MOD-2))
 (4 4 (:REWRITE DEFAULT-MOD-1))
 (4 4 (:REWRITE |(mod x (- y))| . 3))
 (4 4 (:REWRITE |(mod x (- y))| . 2))
 (4 4 (:REWRITE |(mod x (- y))| . 1))
 (4 4 (:REWRITE |(mod x (* y (/ z))) rewriting-goal-literal|))
 (4 4 (:REWRITE |(mod x (* y (/ z))) not rewriting-goal-literal|))
 (4 4 (:REWRITE |(mod (- x) y)| . 3))
 (4 4 (:REWRITE |(mod (- x) y)| . 2))
 (4 4 (:REWRITE |(mod (- x) y)| . 1))
 (4 4 (:REWRITE |(mod (* x (/ y)) z) not rewriting-goal-literal|))
 (3 3 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-=-0))
 (2 2 (:REWRITE REDUCE-INTEGERP-+-CONSTANT))
 (2 2 (:REWRITE INTEGERP-+-REDUCE-CONSTANT))
 (2 2 (:REWRITE DEFAULT-LOGAND-2))
 (2 2 (:REWRITE DEFAULT-LOGAND-1))
 (2 2 (:REWRITE |(equal (mod (+ x y) z) x)|))
 (1 1 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NONPOSITIVE-BASE-ODD-EXPONENT))
 (1 1 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NONPOSITIVE-BASE-EVEN-EXPONENT))
 (1 1 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NEGATIVE-BASE-ODD-EXPONENT))
 (1 1 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NEGATIVE-BASE-EVEN-EXPONENT))
 (1 1 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-INTEGERP-BASE-B))
 (1 1 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-INTEGERP-BASE-A))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (1 1 (:REWRITE |(< (/ x) 0)|))
 (1 1 (:REWRITE |(< (+ (- c) x) y)|))
 (1 1 (:REWRITE |(< (* x y) 0)|))
 (1 1 (:REWRITE |(* a (/ a) b)|))
 )
(RM16-RM08-LEMMA-LEMMA
 (3 3 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 (1 1 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-LIST-OF-G-BOOLEANS))
 (1 1 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-ATOM))
 )
(RM16-RM08-LEMMA
 (348 14 (:LINEAR ASH--2-MONOTONE))
 (284 224 (:REWRITE DEFAULT-<-1))
 (282 2 (:REWRITE HACK20))
 (224 224 (:REWRITE DEFAULT-<-2))
 (84 4 (:LINEAR N64P-LOGIOR-N64P-LESS-THAN-18446744073709551616))
 (84 4 (:LINEAR N48P-LOGIOR-N48P-LESS-THAN-281474976710656))
 (84 4 (:LINEAR N32P-LOGIOR-N32P-LESS-THAN-4294967296))
 (84 4 (:LINEAR N30P-LOGIOR-N30P-LESS-THAN-1073741824))
 (84 4 (:LINEAR N24P-LOGIOR-N24P-LESS-THAN-16777216))
 (84 4 (:LINEAR N20P-LOGIOR-N20P-LESS-THAN-1048576))
 (84 4 (:LINEAR N16P-LOGIOR-N16P-LESS-THAN-65536))
 (84 4 (:LINEAR N12P-LOGIOR-N12P-LESS-THAN-4096))
 (84 4 (:LINEAR N08P-LOGIOR-N08P-LESS-THAN-256))
 (84 4 (:LINEAR N05P-LOGIOR-N05P-LESS-THAN-32))
 (84 4 (:LINEAR N04P-LOGIOR-N04P-LESS-THAN-16))
 (84 4 (:LINEAR N03P-LOGIOR-N03P-LESS-THAN-8))
 (84 4 (:LINEAR N02P-LOGIOR-N02P-LESS-THAN-4))
 (84 4 (:LINEAR N01P-LOGIOR-N01P-LESS-THAN-2))
 (62 58 (:LINEAR ASH-NEGATIVE-SHIFT-MAKES-INPUT-SMALLER))
 (35 7 (:LINEAR RM08-WM32-HACK-8-A))
 (24 4 (:LINEAR LOGIOR-LESS-THAN-OR-EQUAL))
 (24 4 (:LINEAR LOGIOR-GREATER-OR-EQUAL-TO-ZERO))
 (21 21 (:LINEAR INDEX-OF-<-LEN))
 (17 15 (:REWRITE DEFAULT-+-2))
 (15 15 (:REWRITE DEFAULT-+-1))
 (14 2 (:LINEAR N01P-LOGAND-N01P-LESS-THAN-2))
 (10 4 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 (8 4 (:REWRITE DEFAULT-UNARY-MINUS))
 (8 1 (:REWRITE CONSP-OF-NTH-WHEN-ATOM-LISTP))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-ATOM-LISTP))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-STR))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-SSR))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-LIMIT))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-BASE))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-ACCESS))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-RGF))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-MEM))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-CTR))
 (3 1 (:REWRITE ATOM-LISTP-WHEN-NOT-CONSP))
 (2 2 (:TYPE-PRESCRIPTION ATOM-LISTP))
 (2 2 (:REWRITE ATOM-LISTP-WHEN-SUBSETP-EQUAL))
 )
(RM16-RM08
 (629 173 (:LINEAR ASH-N02P-IS-ZERO-OR-POSITIVE))
 (250 4 (:REWRITE HACK20))
 (232 148 (:REWRITE DEFAULT-<-1))
 (148 148 (:REWRITE DEFAULT-<-2))
 (136 12 (:LINEAR ASH--2-MONOTONE))
 (122 6 (:LINEAR N64P-LOGIOR-N64P-LESS-THAN-18446744073709551616))
 (122 6 (:LINEAR N48P-LOGIOR-N48P-LESS-THAN-281474976710656))
 (122 6 (:LINEAR N32P-LOGIOR-N32P-LESS-THAN-4294967296))
 (122 6 (:LINEAR N30P-LOGIOR-N30P-LESS-THAN-1073741824))
 (122 6 (:LINEAR N24P-LOGIOR-N24P-LESS-THAN-16777216))
 (122 6 (:LINEAR N20P-LOGIOR-N20P-LESS-THAN-1048576))
 (122 6 (:LINEAR N16P-LOGIOR-N16P-LESS-THAN-65536))
 (122 6 (:LINEAR N12P-LOGIOR-N12P-LESS-THAN-4096))
 (122 6 (:LINEAR N08P-LOGIOR-N08P-LESS-THAN-256))
 (122 6 (:LINEAR N05P-LOGIOR-N05P-LESS-THAN-32))
 (122 6 (:LINEAR N04P-LOGIOR-N04P-LESS-THAN-16))
 (122 6 (:LINEAR N03P-LOGIOR-N03P-LESS-THAN-8))
 (122 6 (:LINEAR N02P-LOGIOR-N02P-LESS-THAN-4))
 (122 6 (:LINEAR N01P-LOGIOR-N01P-LESS-THAN-2))
 (95 89 (:LINEAR ASH-NEGATIVE-SHIFT-MAKES-INPUT-SMALLER))
 (66 60 (:TYPE-PRESCRIPTION INTEGERP-RM16))
 (47 10 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 (36 6 (:LINEAR LOGIOR-LESS-THAN-OR-EQUAL))
 (36 6 (:LINEAR LOGIOR-GREATER-OR-EQUAL-TO-ZERO))
 (34 34 (:TYPE-PRESCRIPTION N32P-ASH--2-IS-N30P))
 (27 27 (:REWRITE DEFAULT-+-2))
 (27 27 (:REWRITE DEFAULT-+-1))
 (24 12 (:REWRITE DEFAULT-UNARY-MINUS))
 (20 20 (:LINEAR INDEX-OF-<-LEN))
 (18 6 (:REWRITE LOGAND-+1-3))
 (18 6 (:REWRITE HACK16))
 (18 6 (:REWRITE HACK13))
 (18 6 (:REWRITE HACK12))
 (18 6 (:REWRITE ASH-+1--2))
 (18 6 (:LINEAR RM08-WM32-HACK-8-A))
 (14 6 (:LINEAR ASH-ADDR--2-IS-LESS))
 (11 5 (:LINEAR N32P-ASH--2-IS-N30P))
 (10 4 (:REWRITE RM16-RM08-LEMMA))
 (1 1 (:LINEAR N01P-LOGAND-N01P-LESS-THAN-2))
 )
(LOGAND-ASH--8
 (1 1 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(UPDATE-NTH-UPDATE-NTH-SAME
 (30 3 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 (8 8 (:REWRITE ZP-OPEN))
 (7 7 (:REWRITE DEFAULT-+-2))
 (7 7 (:REWRITE DEFAULT-+-1))
 )
(!MEMI-!MEMI-SAME
 (15 6 (:DEFINITION UPDATE-NTH))
 (10 10 (:LINEAR INDEX-OF-<-LEN))
 (3 3 (:REWRITE ZP-OPEN))
 (3 3 (:REWRITE DEFAULT-+-2))
 (3 3 (:REWRITE DEFAULT-+-1))
 (2 2 (:REWRITE DEFAULT-<-2))
 (2 2 (:REWRITE DEFAULT-<-1))
 )
(WM16-WM08-LEMMA
 (3 3 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(WM16-WM08
 (943 7 (:REWRITE HACK20))
 (773 754 (:REWRITE DEFAULT-<-1))
 (754 754 (:REWRITE DEFAULT-<-2))
 (145 29 (:LINEAR RM08-WM32-HACK-8-A))
 (91 67 (:REWRITE DEFAULT-+-2))
 (70 67 (:REWRITE DEFAULT-+-1))
 (42 16 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 (41 41 (:LINEAR INDEX-OF-<-LEN))
 (28 4 (:LINEAR N01P-LOGAND-N01P-LESS-THAN-2))
 (18 6 (:LINEAR ASH-NEGATIVE-SHIFT-MAKES-INPUT-SMALLER))
 (14 7 (:REWRITE DEFAULT-UNARY-MINUS))
 (8 1 (:REWRITE CONSP-OF-NTH-WHEN-ATOM-LISTP))
 (6 6 (:TYPE-PRESCRIPTION INTEGERP-RM16))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-ATOM-LISTP))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-STR))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-SSR))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-LIMIT))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-BASE))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-ACCESS))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-RGF))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-MEM))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-CTR))
 (3 1 (:REWRITE ATOM-LISTP-WHEN-NOT-CONSP))
 (2 2 (:TYPE-PRESCRIPTION ATOM-LISTP))
 (2 2 (:REWRITE ATOM-LISTP-WHEN-SUBSETP-EQUAL))
 )
(ASH--8-LINEAR
 (851 24 (:REWRITE THE-FLOOR-BELOW))
 (637 637 (:TYPE-PRESCRIPTION NOT-INTEGERP-4B))
 (637 637 (:TYPE-PRESCRIPTION NOT-INTEGERP-3B))
 (637 637 (:TYPE-PRESCRIPTION NOT-INTEGERP-2B))
 (637 637 (:TYPE-PRESCRIPTION NOT-INTEGERP-1B))
 (340 5 (:REWRITE FLOOR-ZERO . 3))
 (338 26 (:TYPE-PRESCRIPTION FLOOR-ZERO . 2))
 (265 5 (:REWRITE CANCEL-FLOOR-+))
 (234 26 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 1))
 (234 26 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 1))
 (234 26 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 1))
 (175 5 (:REWRITE FLOOR-ZERO . 5))
 (155 5 (:REWRITE FLOOR-X-Y-=-1 . 2))
 (150 5 (:REWRITE FLOOR-ZERO . 4))
 (140 25 (:REWRITE INTEGERP-MINUS-X))
 (139 24 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (139 24 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (130 26 (:TYPE-PRESCRIPTION FLOOR-ZERO . 4))
 (130 26 (:TYPE-PRESCRIPTION FLOOR-ZERO . 3))
 (130 26 (:TYPE-PRESCRIPTION FLOOR-ZERO . 1))
 (130 26 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 3))
 (130 26 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 2))
 (130 26 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 3))
 (130 26 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 2))
 (130 26 (:TYPE-PRESCRIPTION FLOOR-NONNEGATIVE . 3))
 (130 26 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 3))
 (130 26 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 2))
 (119 24 (:REWRITE DEFAULT-LESS-THAN-2))
 (110 5 (:REWRITE FLOOR-=-X/Y . 3))
 (110 5 (:REWRITE FLOOR-=-X/Y . 2))
 (102 102 (:TYPE-PRESCRIPTION NOT-INTEGERP-4A))
 (102 102 (:TYPE-PRESCRIPTION NOT-INTEGERP-3A))
 (102 102 (:TYPE-PRESCRIPTION NOT-INTEGERP-2A))
 (102 102 (:TYPE-PRESCRIPTION NOT-INTEGERP-1A))
 (97 2 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (97 2 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (86 82 (:REWRITE DEFAULT-TIMES-2))
 (85 10 (:REWRITE |(* (- x) y)|))
 (82 82 (:REWRITE DEFAULT-TIMES-1))
 (55 5 (:REWRITE DEFAULT-FLOOR-RATIO))
 (52 2 (:LINEAR LINEAR-FLOOR-BOUNDS-3))
 (50 10 (:REWRITE DEFAULT-MINUS))
 (45 10 (:REWRITE |(- (* c x))|))
 (45 1 (:REWRITE FLOOR-=-X/Y . 4))
 (44 24 (:REWRITE DEFAULT-LESS-THAN-1))
 (44 2 (:LINEAR LINEAR-FLOOR-BOUNDS-2))
 (43 43 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (30 1 (:LINEAR ASH-NEGATIVE-SHIFT-MAKES-INPUT-SMALLER))
 (29 24 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (29 24 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (27 3 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (25 5 (:REWRITE FLOOR-ZERO . 2))
 (25 5 (:REWRITE FLOOR-X-Y-=-1 . 3))
 (25 5 (:REWRITE FLOOR-X-Y-=--1 . 3))
 (25 5 (:REWRITE FLOOR-X-Y-=--1 . 2))
 (25 5 (:REWRITE FLOOR-CANCEL-*-REWRITING-GOAL-LITERAL))
 (25 5 (:REWRITE FLOOR-CANCEL-*-CONST))
 (25 5 (:REWRITE |(floor (* x (/ y)) z) rewriting-goal-literal|))
 (24 24 (:REWRITE THE-FLOOR-ABOVE))
 (24 24 (:REWRITE SIMPLIFY-SUMS-<))
 (24 24 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (24 24 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (24 24 (:REWRITE INTEGERP-<-CONSTANT))
 (24 24 (:REWRITE CONSTANT-<-INTEGERP))
 (24 24 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (24 24 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (24 24 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (24 24 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (24 24 (:REWRITE |(< c (- x))|))
 (24 24 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (24 24 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (24 24 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (24 24 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (24 24 (:REWRITE |(< (/ x) (/ y))|))
 (24 24 (:REWRITE |(< (- x) c)|))
 (24 24 (:REWRITE |(< (- x) (- y))|))
 (20 20 (:REWRITE REDUCE-INTEGERP-+))
 (20 20 (:META META-INTEGERP-CORRECT))
 (13 13 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (11 11 (:TYPE-PRESCRIPTION ABS))
 (6 6 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (6 6 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (6 6 (:REWRITE |(< 0 (/ x))|))
 (6 6 (:REWRITE |(< 0 (* x y))|))
 (6 2 (:REWRITE DEFAULT-PLUS-2))
 (6 2 (:REWRITE DEFAULT-PLUS-1))
 (5 5 (:REWRITE FLOOR-CANCEL-*-NOT-REWRITING-GOAL-LITERAL))
 (5 5 (:REWRITE DEFAULT-FLOOR-2))
 (5 5 (:REWRITE DEFAULT-FLOOR-1))
 (5 5 (:REWRITE |(floor x (- y))| . 2))
 (5 5 (:REWRITE |(floor x (- y))| . 1))
 (5 5 (:REWRITE |(floor x (* y (/ z))) rewriting-goal-literal|))
 (5 5 (:REWRITE |(floor x (* y (/ z))) not rewriting-goal-literal|))
 (5 5 (:REWRITE |(floor (- x) y)| . 2))
 (5 5 (:REWRITE |(floor (- x) y)| . 1))
 (5 5 (:REWRITE |(floor (* x (/ y)) z) not rewriting-goal-literal|))
 (5 5 (:REWRITE |(< (* (/ x) y) 1) with (< x 0)|))
 (5 5 (:REWRITE |(< (* (/ x) y) 1) with (< 0 x)|))
 (5 1 (:REWRITE |(equal (floor (+ x y) z) x)|))
 (2 2 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (2 2 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (2 2 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (2 2 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 (2 2 (:REWRITE |(equal c (/ x))|))
 (2 2 (:REWRITE |(equal c (- x))|))
 (2 2 (:REWRITE |(equal (/ x) c)|))
 (2 2 (:REWRITE |(equal (/ x) (/ y))|))
 (2 2 (:REWRITE |(equal (- x) c)|))
 (2 2 (:REWRITE |(equal (- x) (- y))|))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (1 1 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (1 1 (:REWRITE NORMALIZE-ADDENDS))
 (1 1 (:REWRITE |(< (/ x) 0)|))
 (1 1 (:REWRITE |(< (* x y) 0)|))
 (1 1 (:REWRITE |(* a (/ a) b)|))
 )
(RM16-WM16-DIFFERENT
 (462 84 (:LINEAR RM08-LESS-THAN-EXPT-2-32))
 (295 163 (:REWRITE DEFAULT-<-1))
 (228 6 (:LINEAR N64P-LOGIOR-N64P-LESS-THAN-18446744073709551616))
 (228 6 (:LINEAR N48P-LOGIOR-N48P-LESS-THAN-281474976710656))
 (228 6 (:LINEAR N32P-LOGIOR-N32P-LESS-THAN-4294967296))
 (228 6 (:LINEAR N30P-LOGIOR-N30P-LESS-THAN-1073741824))
 (228 6 (:LINEAR N24P-LOGIOR-N24P-LESS-THAN-16777216))
 (228 6 (:LINEAR N20P-LOGIOR-N20P-LESS-THAN-1048576))
 (228 6 (:LINEAR N16P-LOGIOR-N16P-LESS-THAN-65536))
 (228 6 (:LINEAR N12P-LOGIOR-N12P-LESS-THAN-4096))
 (228 6 (:LINEAR N08P-LOGIOR-N08P-LESS-THAN-256))
 (163 163 (:REWRITE DEFAULT-<-2))
 (162 6 (:LINEAR N05P-LOGIOR-N05P-LESS-THAN-32))
 (162 6 (:LINEAR N04P-LOGIOR-N04P-LESS-THAN-16))
 (162 6 (:LINEAR N03P-LOGIOR-N03P-LESS-THAN-8))
 (162 6 (:LINEAR N02P-LOGIOR-N02P-LESS-THAN-4))
 (162 6 (:LINEAR N01P-LOGIOR-N01P-LESS-THAN-2))
 (90 90 (:REWRITE DEFAULT-+-2))
 (90 90 (:REWRITE DEFAULT-+-1))
 (54 54 (:LINEAR ASH-NEGATIVE-SHIFT-MAKES-INPUT-SMALLER))
 (50 6 (:LINEAR LOGIOR-LESS-THAN-OR-EQUAL))
 (50 6 (:LINEAR LOGIOR-GREATER-OR-EQUAL-TO-ZERO))
 (45 13 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 (43 9 (:REWRITE RM16-RM08-LEMMA))
 (30 30 (:LINEAR INDEX-OF-<-LEN))
 (20 20 (:TYPE-PRESCRIPTION RM08))
 )
(RM16-WM16-WRITE-HIGH-BYTE
 (198 28 (:LINEAR RM08-LESS-THAN-EXPT-2-32))
 (140 74 (:REWRITE DEFAULT-<-1))
 (107 3 (:LINEAR N64P-LOGIOR-N64P-LESS-THAN-18446744073709551616))
 (107 3 (:LINEAR N48P-LOGIOR-N48P-LESS-THAN-281474976710656))
 (107 3 (:LINEAR N32P-LOGIOR-N32P-LESS-THAN-4294967296))
 (107 3 (:LINEAR N30P-LOGIOR-N30P-LESS-THAN-1073741824))
 (107 3 (:LINEAR N24P-LOGIOR-N24P-LESS-THAN-16777216))
 (107 3 (:LINEAR N20P-LOGIOR-N20P-LESS-THAN-1048576))
 (107 3 (:LINEAR N16P-LOGIOR-N16P-LESS-THAN-65536))
 (107 3 (:LINEAR N12P-LOGIOR-N12P-LESS-THAN-4096))
 (107 3 (:LINEAR N08P-LOGIOR-N08P-LESS-THAN-256))
 (87 3 (:LINEAR N05P-LOGIOR-N05P-LESS-THAN-32))
 (87 3 (:LINEAR N04P-LOGIOR-N04P-LESS-THAN-16))
 (87 3 (:LINEAR N03P-LOGIOR-N03P-LESS-THAN-8))
 (87 3 (:LINEAR N02P-LOGIOR-N02P-LESS-THAN-4))
 (87 3 (:LINEAR N01P-LOGIOR-N01P-LESS-THAN-2))
 (74 74 (:REWRITE DEFAULT-<-2))
 (38 37 (:REWRITE DEFAULT-+-2))
 (37 37 (:REWRITE DEFAULT-+-1))
 (36 2 (:REWRITE RM16-WM16-DIFFERENT))
 (32 32 (:LINEAR ASH-NEGATIVE-SHIFT-MAKES-INPUT-SMALLER))
 (24 3 (:LINEAR LOGIOR-LESS-THAN-OR-EQUAL))
 (24 3 (:LINEAR LOGIOR-GREATER-OR-EQUAL-TO-ZERO))
 (20 20 (:LINEAR INDEX-OF-<-LEN))
 (12 4 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 (8 1 (:REWRITE CONSP-OF-NTH-WHEN-ATOM-LISTP))
 (6 6 (:REWRITE CONSP-WHEN-MEMBER-EQUAL-OF-ATOM-LISTP))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-STR))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-SSR))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-LIMIT))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-BASE))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG-ACCESS))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-SEG))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-RGF))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-MEM))
 (4 2 (:TYPE-PRESCRIPTION NATP-NTH-OF-CTR))
 (3 1 (:REWRITE ATOM-LISTP-WHEN-NOT-CONSP))
 (2 2 (:TYPE-PRESCRIPTION ATOM-LISTP))
 (2 2 (:REWRITE ATOM-LISTP-WHEN-SUBSETP-EQUAL))
 )
(RM16-WM16-WRITE-LOW-BYTE
 (198 28 (:LINEAR RM08-LESS-THAN-EXPT-2-32))
 (129 64 (:REWRITE DEFAULT-<-1))
 (107 3 (:LINEAR N64P-LOGIOR-N64P-LESS-THAN-18446744073709551616))
 (107 3 (:LINEAR N48P-LOGIOR-N48P-LESS-THAN-281474976710656))
 (107 3 (:LINEAR N32P-LOGIOR-N32P-LESS-THAN-4294967296))
 (107 3 (:LINEAR N30P-LOGIOR-N30P-LESS-THAN-1073741824))
 (107 3 (:LINEAR N24P-LOGIOR-N24P-LESS-THAN-16777216))
 (107 3 (:LINEAR N20P-LOGIOR-N20P-LESS-THAN-1048576))
 (107 3 (:LINEAR N16P-LOGIOR-N16P-LESS-THAN-65536))
 (107 3 (:LINEAR N12P-LOGIOR-N12P-LESS-THAN-4096))
 (107 3 (:LINEAR N08P-LOGIOR-N08P-LESS-THAN-256))
 (87 3 (:LINEAR N05P-LOGIOR-N05P-LESS-THAN-32))
 (87 3 (:LINEAR N04P-LOGIOR-N04P-LESS-THAN-16))
 (87 3 (:LINEAR N03P-LOGIOR-N03P-LESS-THAN-8))
 (87 3 (:LINEAR N02P-LOGIOR-N02P-LESS-THAN-4))
 (87 3 (:LINEAR N01P-LOGIOR-N01P-LESS-THAN-2))
 (64 64 (:REWRITE DEFAULT-<-2))
 (60 60 (:REWRITE DEFAULT-+-2))
 (60 60 (:REWRITE DEFAULT-+-1))
 (36 2 (:REWRITE RM16-WM16-DIFFERENT))
 (32 32 (:LINEAR ASH-NEGATIVE-SHIFT-MAKES-INPUT-SMALLER))
 (28 2 (:REWRITE RM16-WM16-WRITE-HIGH-BYTE))
 (24 3 (:LINEAR LOGIOR-LESS-THAN-OR-EQUAL))
 (24 3 (:LINEAR LOGIOR-GREATER-OR-EQUAL-TO-ZERO))
 (11 5 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 (10 10 (:TYPE-PRESCRIPTION RM08))
 (10 10 (:LINEAR INDEX-OF-<-LEN))
 )
(HACK-LAST
 (1 1 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(RM16-WM16
 (298 238 (:REWRITE DEFAULT-<-1))
 (238 238 (:REWRITE DEFAULT-<-2))
 (182 4 (:LINEAR N05P-LOGIOR-N05P-LESS-THAN-32))
 (182 4 (:LINEAR N04P-LOGIOR-N04P-LESS-THAN-16))
 (182 4 (:LINEAR N03P-LOGIOR-N03P-LESS-THAN-8))
 (182 4 (:LINEAR N02P-LOGIOR-N02P-LESS-THAN-4))
 (182 4 (:LINEAR N01P-LOGIOR-N01P-LESS-THAN-2))
 (146 4 (:LINEAR N08P-LOGIOR-N08P-LESS-THAN-256))
 (140 4 (:LINEAR N12P-LOGIOR-N12P-LESS-THAN-4096))
 (134 4 (:LINEAR N16P-LOGIOR-N16P-LESS-THAN-65536))
 (128 4 (:LINEAR N20P-LOGIOR-N20P-LESS-THAN-1048576))
 (122 4 (:LINEAR N24P-LOGIOR-N24P-LESS-THAN-16777216))
 (116 4 (:LINEAR N30P-LOGIOR-N30P-LESS-THAN-1073741824))
 (110 4 (:LINEAR N32P-LOGIOR-N32P-LESS-THAN-4294967296))
 (104 4 (:LINEAR N48P-LOGIOR-N48P-LESS-THAN-281474976710656))
 (98 4 (:LINEAR N64P-LOGIOR-N64P-LESS-THAN-18446744073709551616))
 (70 10 (:LINEAR N05P-LOGAND-N05P-LESS-THAN-32))
 (70 10 (:LINEAR N04P-LOGAND-N04P-LESS-THAN-16))
 (70 10 (:LINEAR N03P-LOGAND-N03P-LESS-THAN-8))
 (70 10 (:LINEAR N02P-LOGAND-N02P-LESS-THAN-4))
 (70 10 (:LINEAR N01P-LOGAND-N01P-LESS-THAN-2))
 (66 28 (:LINEAR RM08-LESS-THAN-EXPT-2-32))
 (60 20 (:LINEAR LOGAND-LESS-THAN-OR-EQUAL))
 (36 36 (:LINEAR ASH-NEGATIVE-SHIFT-MAKES-INPUT-SMALLER))
 (34 34 (:REWRITE DEFAULT-+-2))
 (34 34 (:REWRITE DEFAULT-+-1))
 (30 30 (:LINEAR INDEX-OF-<-LEN))
 (28 4 (:LINEAR LOGIOR-LESS-THAN-OR-EQUAL))
 (28 4 (:LINEAR LOGIOR-GREATER-OR-EQUAL-TO-ZERO))
 (19 12 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 )