(CLUSTER-P)
(CLUSTER-P-OF-IMPLODE
 (24 3 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (22 6 (:REWRITE ACL2-NUMBERP-X))
 (10 2 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (8 3 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (8 3 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (8 2 (:REWRITE RATIONALP-X))
 (6 3 (:REWRITE DEFAULT-PLUS-2))
 (4 4 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (4 4 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (3 3 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (3 3 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (3 3 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (3 3 (:REWRITE NORMALIZE-ADDENDS))
 (3 3 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (3 3 (:REWRITE DEFAULT-PLUS-1))
 (3 3 (:REWRITE DEFAULT-CDR))
 (3 3 (:REWRITE |(equal c (/ x))|))
 (3 3 (:REWRITE |(equal c (- x))|))
 (3 3 (:REWRITE |(equal (/ x) c)|))
 (3 3 (:REWRITE |(equal (/ x) (/ y))|))
 (3 3 (:REWRITE |(equal (- x) c)|))
 (3 3 (:REWRITE |(equal (- x) (- y))|))
 (2 2 (:REWRITE REDUCE-RATIONALP-+))
 (2 2 (:REWRITE REDUCE-RATIONALP-*))
 (2 2 (:REWRITE REDUCE-INTEGERP-+))
 (2 2 (:REWRITE RATIONALP-MINUS-X))
 (2 2 (:REWRITE INTEGERP-MINUS-X))
 (2 2 (:META META-RATIONALP-CORRECT))
 (2 2 (:META META-INTEGERP-CORRECT))
 (1 1 (:LINEAR POSITION-WHEN-MEMBER))
 (1 1 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 )
(CLUSTER-P-CORRECTNESS-1)
(CLUSTER-LISTP)
(CLUSTER-LISTP-OF-UPDATE-NTH
 (1072 110 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (1059 421 (:REWRITE DEFAULT-CDR))
 (770 32 (:REWRITE ZP-OPEN))
 (670 50 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (441 269 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (385 269 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (385 269 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (326 326 (:REWRITE DEFAULT-PLUS-1))
 (289 289 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (289 289 (:REWRITE NORMALIZE-ADDENDS))
 (269 269 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (269 269 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (269 269 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (269 269 (:REWRITE |(equal c (/ x))|))
 (269 269 (:REWRITE |(equal c (- x))|))
 (269 269 (:REWRITE |(equal (/ x) c)|))
 (269 269 (:REWRITE |(equal (/ x) (/ y))|))
 (269 269 (:REWRITE |(equal (- x) c)|))
 (269 269 (:REWRITE |(equal (- x) (- y))|))
 (236 193 (:REWRITE DEFAULT-CAR))
 (212 37 (:REWRITE ACL2-NUMBERP-X))
 (212 34 (:REWRITE NONEMPTY-STRING-LISTP-OF-CDR-WHEN-NONEMPTY-STRING-LISTP))
 (199 199 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (186 5 (:DEFINITION NATP))
 (180 180 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (146 146 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (146 146 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (119 90 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (113 77 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (113 77 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (104 104 (:REWRITE THE-FLOOR-BELOW))
 (104 104 (:REWRITE THE-FLOOR-ABOVE))
 (91 77 (:REWRITE SIMPLIFY-SUMS-<))
 (89 89 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (89 89 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (83 23 (:REWRITE RATIONALP-X))
 (81 77 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (79 77 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (78 6 (:REWRITE NONEMPTY-STRING-LISTP-OF-UPDATE-NTH))
 (77 77 (:REWRITE INTEGERP-<-CONSTANT))
 (77 77 (:REWRITE CONSTANT-<-INTEGERP))
 (77 77 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (77 77 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (77 77 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (77 77 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (77 77 (:REWRITE |(< c (- x))|))
 (77 77 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (77 77 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (77 77 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (77 77 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (77 77 (:REWRITE |(< (/ x) (/ y))|))
 (77 77 (:REWRITE |(< (- x) c)|))
 (77 77 (:REWRITE |(< (- x) (- y))|))
 (75 2 (:REWRITE |(< (if a b c) x)|))
 (39 39 (:REWRITE |(< (* x y) 0)|))
 (38 38 (:LINEAR POSITION-WHEN-MEMBER))
 (38 38 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (35 35 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (35 35 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (35 35 (:REWRITE REDUCE-INTEGERP-+))
 (35 35 (:REWRITE INTEGERP-MINUS-X))
 (35 35 (:REWRITE |(< (/ x) 0)|))
 (35 35 (:META META-INTEGERP-CORRECT))
 (23 23 (:REWRITE REDUCE-RATIONALP-+))
 (23 23 (:REWRITE REDUCE-RATIONALP-*))
 (23 23 (:REWRITE RATIONALP-MINUS-X))
 (23 23 (:REWRITE |(< x (+ c/d y))|))
 (23 23 (:META META-RATIONALP-CORRECT))
 (20 20 (:REWRITE |(< 0 (* x y))|))
 (19 19 (:REWRITE |(< (+ c/d x) y)|))
 (18 18 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 (15 15 (:REWRITE |(< y (+ (- c) x))|))
 (15 15 (:REWRITE |(< (+ (- c) x) y)|))
 (12 12 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (12 12 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (12 12 (:REWRITE |(< 0 (/ x))|))
 (5 5 (:TYPE-PRESCRIPTION NATP))
 (4 4 (:REWRITE |(equal x (if a b c))|))
 )
(CLUSTER-P-OF-NTH
 (259 31 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (143 7 (:REWRITE ZP-OPEN))
 (132 16 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (126 31 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (108 57 (:REWRITE DEFAULT-CDR))
 (99 27 (:REWRITE ACL2-NUMBERP-X))
 (84 22 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (82 46 (:REWRITE DEFAULT-PLUS-2))
 (54 31 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (54 31 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (54 4 (:REWRITE STRINGP-OF-NTH))
 (52 52 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (48 8 (:REWRITE NONEMPTY-STRING-LISTP-OF-CDR-WHEN-NONEMPTY-STRING-LISTP))
 (46 46 (:REWRITE DEFAULT-PLUS-1))
 (46 2 (:DEFINITION STRING-LISTP))
 (42 42 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (42 42 (:REWRITE NORMALIZE-ADDENDS))
 (36 36 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (36 36 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (36 9 (:REWRITE RATIONALP-X))
 (34 24 (:REWRITE DEFAULT-LESS-THAN-2))
 (34 1 (:DEFINITION NATP))
 (31 31 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (31 31 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (31 31 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (31 31 (:REWRITE |(equal c (/ x))|))
 (31 31 (:REWRITE |(equal c (- x))|))
 (31 31 (:REWRITE |(equal (/ x) c)|))
 (31 31 (:REWRITE |(equal (/ x) (/ y))|))
 (31 31 (:REWRITE |(equal (- x) c)|))
 (31 31 (:REWRITE |(equal (- x) (- y))|))
 (28 20 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (28 20 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (27 20 (:REWRITE SIMPLIFY-SUMS-<))
 (26 26 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (24 24 (:REWRITE THE-FLOOR-BELOW))
 (24 24 (:REWRITE THE-FLOOR-ABOVE))
 (24 24 (:REWRITE DEFAULT-LESS-THAN-1))
 (24 2 (:REWRITE NONEMPTY-STRINGP-OF-NTH-WHEN-NONEMPTY-STRING-LISTP))
 (22 22 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (22 22 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (20 20 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (20 20 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (20 20 (:REWRITE INTEGERP-<-CONSTANT))
 (20 20 (:REWRITE DEFAULT-CAR))
 (20 20 (:REWRITE CONSTANT-<-INTEGERP))
 (20 20 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (20 20 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (20 20 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (20 20 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (20 20 (:REWRITE |(< c (- x))|))
 (20 20 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (20 20 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (20 20 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (20 20 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (20 20 (:REWRITE |(< (/ x) (/ y))|))
 (20 20 (:REWRITE |(< (- x) c)|))
 (20 20 (:REWRITE |(< (- x) (- y))|))
 (17 17 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (12 12 (:REWRITE REDUCE-INTEGERP-+))
 (12 12 (:REWRITE INTEGERP-MINUS-X))
 (12 12 (:META META-INTEGERP-CORRECT))
 (10 10 (:TYPE-PRESCRIPTION STRING-LISTP))
 (9 9 (:REWRITE REDUCE-RATIONALP-+))
 (9 9 (:REWRITE REDUCE-RATIONALP-*))
 (9 9 (:REWRITE RATIONALP-MINUS-X))
 (9 9 (:META META-RATIONALP-CORRECT))
 (8 8 (:REWRITE |(< x (+ c/d y))|))
 (8 8 (:LINEAR POSITION-WHEN-MEMBER))
 (8 8 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (8 2 (:REWRITE |(+ c (+ d x))|))
 (6 6 (:REWRITE |(< y (+ (- c) x))|))
 (5 5 (:REWRITE |(< 0 (* x y))|))
 (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 |(< (/ x) 0)|))
 (4 4 (:REWRITE |(< (* x y) 0)|))
 (3 3 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (3 3 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (3 3 (:REWRITE |(< 0 (/ x))|))
 (3 3 (:REWRITE |(< (+ c/d x) y)|))
 (3 3 (:REWRITE |(< (+ (- c) x) y)|))
 (2 2 (:REWRITE |(+ 0 x)|))
 (1 1 (:TYPE-PRESCRIPTION NATP))
 )
(CLUSTER-LISTP-OF-APPEND
 (4713 105 (:DEFINITION TRUE-LISTP))
 (4502 209 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (4202 51 (:REWRITE LIST-FIX-WHEN-TRUE-LISTP))
 (3978 161 (:DEFINITION STRING-LISTP))
 (3618 229 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (2654 50 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (2473 206 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (1322 209 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (1237 196 (:REWRITE NONEMPTY-STRING-LISTP-OF-CDR-WHEN-NONEMPTY-STRING-LISTP))
 (804 804 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (795 795 (:TYPE-PRESCRIPTION STRING-LISTP))
 (673 68 (:REWRITE CLUSTER-P-CORRECTNESS-1))
 (641 474 (:REWRITE DEFAULT-CDR))
 (607 607 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (458 458 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (458 458 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (402 402 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (318 318 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (318 159 (:REWRITE OMAP::SETP-WHEN-MAPP))
 (318 159 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (282 276 (:REWRITE DEFAULT-CAR))
 (209 209 (:REWRITE TRUE-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (196 98 (:TYPE-PRESCRIPTION TRUE-LISTP-APPEND))
 (159 159 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (159 159 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
 (159 159 (:REWRITE SET::IN-SET))
 (120 60 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (108 54 (:REWRITE DEFAULT-PLUS-2))
 (98 98 (:TYPE-PRESCRIPTION BINARY-APPEND))
 (72 60 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (69 23 (:REWRITE CAR-OF-APPEND))
 (65 40 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (60 60 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (60 60 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (60 60 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (60 60 (:REWRITE |(equal c (/ x))|))
 (60 60 (:REWRITE |(equal c (- x))|))
 (60 60 (:REWRITE |(equal (/ x) c)|))
 (60 60 (:REWRITE |(equal (/ x) (/ y))|))
 (60 60 (:REWRITE |(equal (- x) c)|))
 (60 60 (:REWRITE |(equal (- x) (- y))|))
 (54 54 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (54 54 (:REWRITE NORMALIZE-ADDENDS))
 (54 54 (:REWRITE DEFAULT-PLUS-1))
 (50 50 (:REWRITE LIST-FIX-WHEN-NOT-CONSP))
 (48 48 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-=-0))
 (48 48 (:LINEAR POSITION-WHEN-MEMBER))
 (48 48 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (46 46 (:REWRITE CONSP-OF-APPEND))
 (40 20 (:REWRITE PREFER-POSITIVE-EXPONENTS-SCATTER-EXPONENTS-EQUAL))
 (32 20 (:REWRITE SIMPLIFY-PRODUCTS-SCATTER-EXPONENTS-EQUAL))
 (23 23 (:REWRITE CDR-OF-APPEND-WHEN-CONSP))
 (2 2 (:REWRITE |(equal x (if a b c))|))
 (2 2 (:REWRITE |(equal (if a b c) x)|))
 )
(CLUSTER-LISTP-OF-RESIZE-LIST
 (4742 49 (:REWRITE RESIZE-LIST-OF-LEN-FREE))
 (2217 49 (:REWRITE NFIX-WHEN-ZP))
 (2114 42 (:REWRITE ZP-OPEN))
 (1485 167 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (631 40 (:REWRITE |(equal (+ (- c) x) y)|))
 (456 35 (:REWRITE CLUSTER-P-CORRECTNESS-1))
 (421 35 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (346 47 (:REWRITE NFIX-WHEN-NATP))
 (327 85 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (306 229 (:REWRITE DEFAULT-PLUS-2))
 (292 7 (:DEFINITION NATP))
 (267 6 (:REWRITE |(equal (if a b c) x)|))
 (254 62 (:REWRITE |(+ c (+ d x))|))
 (246 35 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (229 229 (:REWRITE DEFAULT-PLUS-1))
 (188 169 (:REWRITE DEFAULT-LESS-THAN-1))
 (169 169 (:REWRITE THE-FLOOR-BELOW))
 (169 169 (:REWRITE THE-FLOOR-ABOVE))
 (169 169 (:REWRITE DEFAULT-LESS-THAN-2))
 (167 167 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (167 167 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (145 125 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (142 125 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (139 125 (:REWRITE SIMPLIFY-SUMS-<))
 (125 125 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (125 125 (:REWRITE INTEGERP-<-CONSTANT))
 (125 125 (:REWRITE CONSTANT-<-INTEGERP))
 (125 125 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (125 125 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (125 125 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (125 125 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (125 125 (:REWRITE |(< c (- x))|))
 (125 125 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (125 125 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (125 125 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (125 125 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (125 125 (:REWRITE |(< (/ x) (/ y))|))
 (125 125 (:REWRITE |(< (- x) c)|))
 (125 125 (:REWRITE |(< (- x) (- y))|))
 (116 114 (:REWRITE DEFAULT-CDR))
 (111 111 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (111 111 (:REWRITE NORMALIZE-ADDENDS))
 (110 97 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (109 109 (:LINEAR POSITION-WHEN-MEMBER))
 (109 109 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (90 52 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (85 85 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (84 52 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (74 74 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (70 70 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (70 70 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (70 40 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (56 56 (:REWRITE |(+ 0 x)|))
 (55 53 (:REWRITE DEFAULT-CAR))
 (54 54 (:TYPE-PRESCRIPTION ZP))
 (52 52 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (52 52 (:REWRITE |(equal c (/ x))|))
 (52 52 (:REWRITE |(equal c (- x))|))
 (52 52 (:REWRITE |(equal (/ x) c)|))
 (52 52 (:REWRITE |(equal (/ x) (/ y))|))
 (52 52 (:REWRITE |(equal (- x) c)|))
 (52 52 (:REWRITE |(equal (- x) (- y))|))
 (51 51 (:REWRITE |(< 0 (* x y))|))
 (49 49 (:REWRITE ARITH-NORMALIZE-ADDENDS))
 (37 37 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (34 34 (:REWRITE |(< x (+ c/d y))|))
 (32 28 (:REWRITE SIMPLIFY-PRODUCTS-SCATTER-EXPONENTS-<))
 (32 28 (:REWRITE PREFER-POSITIVE-EXPONENTS-SCATTER-EXPONENTS-<-2))
 (32 28 (:REWRITE PREFER-POSITIVE-EXPONENTS-SCATTER-EXPONENTS-<))
 (30 30 (:REWRITE |(< (* x y) 0)|))
 (21 21 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (21 21 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (21 21 (:REWRITE |(< 0 (/ x))|))
 (20 12 (:REWRITE SIMPLIFY-PRODUCTS-SCATTER-EXPONENTS-EQUAL))
 (20 12 (:REWRITE PREFER-POSITIVE-EXPONENTS-SCATTER-EXPONENTS-EQUAL))
 (18 18 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (18 18 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (18 18 (:REWRITE |(< (/ x) 0)|))
 (17 17 (:REWRITE REDUCE-INTEGERP-+))
 (17 17 (:REWRITE INTEGERP-MINUS-X))
 (17 17 (:META META-INTEGERP-CORRECT))
 (14 14 (:REWRITE |(< (+ c/d x) y)|))
 (12 2 (:REWRITE NONEMPTY-STRING-LISTP-OF-CDR-WHEN-NONEMPTY-STRING-LISTP))
 (7 7 (:TYPE-PRESCRIPTION NATP))
 (6 6 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-=-0))
 (4 4 (:REWRITE |(< y (+ (- c) x))|))
 (2 2 (:REWRITE |(< (+ (- c) x) y)|))
 (1 1 (:LINEAR POSITION-WHEN-MEMBER-OF-TAKE))
 )
(MAKE-CLUSTERS
 (510 20 (:REWRITE NFIX-WHEN-ZP))
 (367 3 (:DEFINITION NTHCDR))
 (235 187 (:REWRITE DEFAULT-PLUS-2))
 (210 8 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (209 187 (:REWRITE DEFAULT-PLUS-1))
 (186 8 (:DEFINITION STRING-LISTP))
 (180 18 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (174 4 (:DEFINITION TRUE-LISTP))
 (173 64 (:REWRITE DEFAULT-CDR))
 (98 8 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (97 1 (:DEFINITION MAKE-LIST-AC))
 (96 2 (:REWRITE THEN-SUBSEQ-EMPTY-1))
 (89 58 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (71 63 (:REWRITE DEFAULT-LESS-THAN-2))
 (65 65 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (65 63 (:REWRITE DEFAULT-LESS-THAN-1))
 (64 8 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (63 63 (:REWRITE THE-FLOOR-BELOW))
 (63 63 (:REWRITE THE-FLOOR-ABOVE))
 (59 1 (:REWRITE |(< (if a b c) x)|))
 (58 58 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (58 58 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (55 55 (:REWRITE INTEGERP-<-CONSTANT))
 (55 55 (:REWRITE CONSTANT-<-INTEGERP))
 (55 55 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (55 55 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (55 55 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (55 55 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (55 55 (:REWRITE |(< c (- x))|))
 (55 55 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (55 55 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (55 55 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (55 55 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (55 55 (:REWRITE |(< (/ x) (/ y))|))
 (55 55 (:REWRITE |(< (- x) c)|))
 (55 55 (:REWRITE |(< (- x) (- y))|))
 (53 53 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (50 8 (:REWRITE NONEMPTY-STRING-LISTP-OF-CDR-WHEN-NONEMPTY-STRING-LISTP))
 (48 5 (:REWRITE |(< (+ (- c) x) y)|))
 (40 40 (:TYPE-PRESCRIPTION STRING-LISTP))
 (32 32 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (32 32 (:TYPE-PRESCRIPTION NONEMPTY-STRING-LISTP))
 (32 32 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (32 32 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (29 29 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (29 29 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (29 29 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (29 29 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (29 29 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (29 29 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (29 29 (:REWRITE |(equal c (/ x))|))
 (29 29 (:REWRITE |(equal c (- x))|))
 (29 29 (:REWRITE |(equal (/ x) c)|))
 (29 29 (:REWRITE |(equal (/ x) (/ y))|))
 (29 29 (:REWRITE |(equal (- x) c)|))
 (29 29 (:REWRITE |(equal (- x) (- y))|))
 (25 25 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (22 22 (:TYPE-PRESCRIPTION BUBBLE-DOWN))
 (21 21 (:REWRITE |(< 0 (* x y))|))
 (20 20 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (19 19 (:REWRITE |(< 0 (/ x))|))
 (17 17 (:REWRITE DEFAULT-MINUS))
 (16 16 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (16 16 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (16 16 (:LINEAR POSITION-WHEN-MEMBER))
 (16 16 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (16 8 (:REWRITE OMAP::SETP-WHEN-MAPP))
 (16 8 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (12 12 (:REWRITE |(< x (+ c/d y))|))
 (11 11 (:REWRITE |(< y (+ (- c) x))|))
 (11 8 (:REWRITE |(+ c (+ d x))|))
 (9 9 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (9 9 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (8 8 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (8 8 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
 (8 8 (:REWRITE TRUE-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (8 8 (:REWRITE SET::IN-SET))
 (8 8 (:REWRITE DEFAULT-CAR))
 (8 1 (:REWRITE STR::CHARACTER-LISTP-WHEN-HEX-DIGIT-CHAR-LISTP))
 (7 1 (:REWRITE |(+ x (if a b c))|))
 (5 5 (:REWRITE |(< (+ c/d x) y)|))
 (4 4 (:REWRITE DEFAULT-TIMES-2))
 (4 4 (:REWRITE DEFAULT-TIMES-1))
 (4 4 (:REWRITE |(< (/ x) 0)|))
 (4 4 (:REWRITE |(< (* x y) 0)|))
 (4 2 (:REWRITE SUBSEQ-OF-LENGTH-1))
 (3 1 (:REWRITE STR::HEX-DIGIT-CHAR-LISTP-WHEN-NOT-CONSP))
 (2 2 (:TYPE-PRESCRIPTION STR::HEX-DIGIT-CHAR-LISTP))
 (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 STR::HEX-DIGIT-CHAR-LISTP-WHEN-SUBSETP-EQUAL))
 (1 1 (:REWRITE FOLD-CONSTS-IN-+))
 (1 1 (:REWRITE |(<= (/ x) y) with (< x 0)|))
 (1 1 (:REWRITE |(<= (/ x) y) with (< 0 x)|))
 (1 1 (:REWRITE |(< x (/ y)) with (< y 0)|))
 )
(MAKE-CLUSTERS-CORRECTNESS-1
 (49083 74 (:REWRITE TAKE-OF-TOO-MANY))
 (25542 403 (:REWRITE |(< (if a b c) x)|))
 (21529 22 (:REWRITE APPEND-OF-NIL))
 (16681 273 (:REWRITE |(< x (if a b c))|))
 (15815 170 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (15467 111 (:DEFINITION STRING-LISTP))
 (15457 63 (:DEFINITION TRUE-LISTP))
 (11736 24 (:REWRITE LIST-FIX-WHEN-TRUE-LISTP))
 (11207 476 (:REWRITE NFIX-WHEN-ZP))
 (11037 26 (:DEFINITION TAKE))
 (8079 116 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (7275 99 (:REWRITE CONSP-OF-NTHCDR))
 (7189 55 (:REWRITE LEN-OF-NTHCDR))
 (7094 13 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (6782 169 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (5963 100 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (5370 1072 (:REWRITE DEFAULT-CDR))
 (5311 4411 (:REWRITE DEFAULT-PLUS-2))
 (5014 4411 (:REWRITE DEFAULT-PLUS-1))
 (4674 88 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (4367 1761 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (4119 268 (:REWRITE |(< (+ (- c) x) y)|))
 (3961 85 (:REWRITE NONEMPTY-STRING-LISTP-OF-CDR-WHEN-NONEMPTY-STRING-LISTP))
 (3420 52 (:REWRITE TAKE-OF-LEN-FREE))
 (3375 105 (:REWRITE |(equal (if a b c) x)|))
 (3152 192 (:REWRITE |(+ x (if a b c))|))
 (2847 2387 (:REWRITE DEFAULT-LESS-THAN-2))
 (2726 218 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (2612 22 (:REWRITE REPEAT-WHEN-ZP))
 (2586 35 (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-ATOM))
 (2494 2387 (:REWRITE DEFAULT-LESS-THAN-1))
 (2421 25 (:REWRITE CONSP-OF-MAKE-LIST-AC))
 (2387 2387 (:REWRITE THE-FLOOR-BELOW))
 (2387 2387 (:REWRITE THE-FLOOR-ABOVE))
 (2377 25 (:DEFINITION MAKE-LIST-AC))
 (2349 11 (:REWRITE CAR-OF-NTHCDR))
 (2234 22 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (2010 13 (:REWRITE LIST-FIX-WHEN-LEN-ZERO))
 (1840 139 (:REWRITE DEFAULT-CAR))
 (1820 1037 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (1806 11 (:DEFINITION NTH))
 (1780 162 (:REWRITE |(+ (if a b c) x)|))
 (1761 1761 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (1761 1761 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (1704 836 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (1620 108 (:REWRITE |(equal (+ (- c) x) y)|))
 (1597 1557 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (1561 1557 (:REWRITE |(< c (- x))|))
 (1557 1557 (:REWRITE INTEGERP-<-CONSTANT))
 (1557 1557 (:REWRITE CONSTANT-<-INTEGERP))
 (1557 1557 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (1557 1557 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (1557 1557 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (1557 1557 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (1557 1557 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (1557 1557 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (1557 1557 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (1557 1557 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (1557 1557 (:REWRITE |(< (/ x) (/ y))|))
 (1557 1557 (:REWRITE |(< (- x) c)|))
 (1557 1557 (:REWRITE |(< (- x) (- y))|))
 (1537 1537 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (1453 170 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (1315 1154 (:REWRITE SIMPLIFY-SUMS-<))
 (1272 1272 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (1200 10 (:REWRITE CHARACTER-LISTP-OF-TAKE))
 (1125 1125 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (1116 27 (:REWRITE THEN-SUBSEQ-EMPTY-1))
 (944 500 (:REWRITE SIMPLIFY-PRODUCTS-SCATTER-EXPONENTS-<))
 (892 467 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (855 13 (:REWRITE LIST-FIX-WHEN-NOT-CONSP))
 (833 833 (:LINEAR POSITION-WHEN-MEMBER))
 (833 833 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (810 156 (:REWRITE BUBBLE-DOWN-+-MATCH-3))
 (766 24 (:REWRITE |(+ (+ x y) z)|))
 (720 720 (:TYPE-PRESCRIPTION STRING-LISTP))
 (549 129 (:REWRITE |(- (if a b c))|))
 (544 500 (:REWRITE PREFER-POSITIVE-EXPONENTS-SCATTER-EXPONENTS-<-2))
 (544 500 (:REWRITE PREFER-POSITIVE-EXPONENTS-SCATTER-EXPONENTS-<))
 (515 515 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (515 515 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (513 263 (:REWRITE |(+ c (+ d x))|))
 (509 456 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (478 472 (:TYPE-PRESCRIPTION BUBBLE-DOWN))
 (467 467 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (467 467 (:REWRITE |(equal c (/ x))|))
 (467 467 (:REWRITE |(equal c (- x))|))
 (467 467 (:REWRITE |(equal (/ x) c)|))
 (467 467 (:REWRITE |(equal (/ x) (/ y))|))
 (467 467 (:REWRITE |(equal (- x) c)|))
 (467 467 (:REWRITE |(equal (- x) (- y))|))
 (463 52 (:REWRITE TAKE-WHEN-ATOM))
 (436 436 (:TYPE-PRESCRIPTION NONEMPTY-STRING-LISTP))
 (436 436 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (416 416 (:REWRITE |(< 0 (* x y))|))
 (402 376 (:REWRITE DEFAULT-MINUS))
 (366 327 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (360 45 (:REWRITE STR::CHARACTER-LISTP-WHEN-HEX-DIGIT-CHAR-LISTP))
 (342 342 (:REWRITE |(< x (+ c/d y))|))
 (320 80 (:REWRITE |(* y x)|))
 (310 310 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (310 155 (:REWRITE OMAP::SETP-WHEN-MAPP))
 (310 155 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (303 13 (:DEFINITION BINARY-APPEND))
 (294 294 (:REWRITE |(< 0 (/ x))|))
 (292 292 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (292 292 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (268 268 (:REWRITE |(< (+ c/d x) y)|))
 (260 260 (:REWRITE |(< y (+ (- c) x))|))
 (225 225 (:REWRITE ARITH-NORMALIZE-ADDENDS))
 (202 24 (:REWRITE |(- (+ x y))|))
 (186 186 (:REWRITE |(< (/ x) 0)|))
 (186 186 (:REWRITE |(< (* x y) 0)|))
 (170 170 (:REWRITE TRUE-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (160 160 (:REWRITE DEFAULT-TIMES-2))
 (160 160 (:REWRITE DEFAULT-TIMES-1))
 (156 140 (:REWRITE SIMPLIFY-PRODUCTS-SCATTER-EXPONENTS-EQUAL))
 (156 140 (:REWRITE PREFER-POSITIVE-EXPONENTS-SCATTER-EXPONENTS-EQUAL))
 (155 155 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (155 155 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
 (155 155 (:REWRITE SET::IN-SET))
 (132 22 (:REWRITE NONEMPTY-STRING-LISTP-OF-NTHCDR))
 (131 131 (:TYPE-PRESCRIPTION NFIX))
 (120 40 (:REWRITE STR::CONSP-OF-MAKE-CHARACTER-LIST))
 (115 45 (:REWRITE STR::HEX-DIGIT-CHAR-LISTP-WHEN-NOT-CONSP))
 (104 104 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (104 104 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (100 100 (:TYPE-PRESCRIPTION MAKE-CHARACTER-LIST))
 (100 100 (:TYPE-PRESCRIPTION STR::HEX-DIGIT-CHAR-LISTP))
 (90 90 (:REWRITE STR::HEX-DIGIT-CHAR-LISTP-WHEN-SUBSETP-EQUAL))
 (80 80 (:REWRITE |(* a (/ a))|))
 (80 48 (:REWRITE ACL2-NUMBERP-X))
 (66 11 (:REWRITE NONEMPTY-STRINGP-OF-NTH-WHEN-NONEMPTY-STRING-LISTP))
 (50 50 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (50 50 (:REWRITE CONSP-OF-TAKE))
 (44 11 (:REWRITE STRINGP-OF-NTH))
 (40 40 (:REWRITE |(<= (/ x) y) with (< x 0)|))
 (40 40 (:REWRITE |(<= (/ x) y) with (< 0 x)|))
 (40 40 (:REWRITE |(< x (/ y)) with (< y 0)|))
 (40 40 (:REWRITE |(< x (/ y)) with (< 0 y)|))
 (34 34 (:REWRITE REDUCE-INTEGERP-+))
 (34 34 (:REWRITE INTEGERP-MINUS-X))
 (34 34 (:META META-INTEGERP-CORRECT))
 (32 8 (:REWRITE RATIONALP-X))
 (25 25 (:REWRITE FOLD-CONSTS-IN-+))
 (24 24 (:REWRITE |(- (- x))|))
 (24 9 (:REWRITE |(equal x (if a b c))|))
 (20 10 (:REWRITE STR::HEX-DIGIT-CHAR-LISTP-OF-TAKE))
 (13 13 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (13 13 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (10 10 (:REWRITE CHARACTER-LISTP-OF-EXPLODE))
 (2 2 (:REWRITE THEN-SUBSEQ-SAME-1))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-=-0))
 )
(CLUSTER-LISTP-OF-MAKE-CLUSTERS
 (12441 32 (:REWRITE TAKE-OF-TOO-MANY))
 (10868 151 (:REWRITE |(< x (if a b c))|))
 (5683 22 (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-CHARACTER-LISTP))
 (5557 11 (:DEFINITION TAKE))
 (4902 126 (:REWRITE NFIX-WHEN-ZP))
 (4173 31 (:REWRITE NTHCDR-WHEN->=-N-LEN-L))
 (3936 44 (:REWRITE CONSP-OF-REPEAT))
 (3205 11 (:DEFINITION CHARACTER-LISTP))
 (2740 20 (:REWRITE LEN-OF-NTHCDR))
 (2403 253 (:REWRITE DEFAULT-CDR))
 (2172 1911 (:REWRITE DEFAULT-PLUS-2))
 (2148 1911 (:REWRITE DEFAULT-PLUS-1))
 (2116 115 (:REWRITE |(< (+ (- c) x) y)|))
 (2039 705 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (2001 21 (:REWRITE REPEAT-WHEN-ZP))
 (1710 22 (:REWRITE TAKE-OF-LEN-FREE))
 (1636 44 (:REWRITE |(equal (if a b c) x)|))
 (1413 46 (:REWRITE DEFAULT-CAR))
 (1318 11 (:REWRITE CHARACTER-LISTP-OF-TAKE))
 (1281 44 (:REWRITE STR::CHARACTER-LISTP-WHEN-HEX-DIGIT-CHAR-LISTP))
 (1083 960 (:REWRITE DEFAULT-LESS-THAN-2))
 (1072 22 (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-ATOM))
 (1000 10 (:REWRITE THEN-SUBSEQ-EMPTY-1))
 (984 11 (:REWRITE STR::HEX-DIGIT-CHAR-LISTP-OF-REPEAT))
 (980 960 (:REWRITE DEFAULT-LESS-THAN-1))
 (960 960 (:REWRITE THE-FLOOR-BELOW))
 (960 960 (:REWRITE THE-FLOOR-ABOVE))
 (765 44 (:REWRITE |(equal (+ (- c) x) y)|))
 (705 705 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (705 705 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (610 610 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (610 610 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (610 610 (:REWRITE INTEGERP-<-CONSTANT))
 (610 610 (:REWRITE CONSTANT-<-INTEGERP))
 (610 610 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (610 610 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (610 610 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (610 610 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (610 610 (:REWRITE |(< c (- x))|))
 (610 610 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (610 610 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (610 610 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (610 610 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (610 610 (:REWRITE |(< (/ x) (/ y))|))
 (610 610 (:REWRITE |(< (- x) c)|))
 (610 610 (:REWRITE |(< (- x) (- y))|))
 (610 610 (:LINEAR POSITION-WHEN-MEMBER))
 (610 610 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (592 382 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (578 21 (:REWRITE SUBSEQ-OF-LENGTH-1))
 (558 11 (:REWRITE THEN-SUBSEQ-SAME-2))
 (470 428 (:REWRITE SIMPLIFY-SUMS-<))
 (371 22 (:REWRITE TAKE-WHEN-ATOM))
 (354 354 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (348 228 (:REWRITE SIMPLIFY-PRODUCTS-SCATTER-EXPONENTS-<))
 (328 328 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (328 328 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (328 306 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (328 306 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (310 10 (:REWRITE |(+ (+ x y) z)|))
 (306 306 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (306 306 (:REWRITE |(equal c (/ x))|))
 (306 306 (:REWRITE |(equal c (- x))|))
 (306 306 (:REWRITE |(equal (/ x) c)|))
 (306 306 (:REWRITE |(equal (/ x) (/ y))|))
 (306 306 (:REWRITE |(equal (- x) c)|))
 (306 306 (:REWRITE |(equal (- x) (- y))|))
 (300 60 (:REWRITE BUBBLE-DOWN-+-MATCH-3))
 (248 228 (:REWRITE PREFER-POSITIVE-EXPONENTS-SCATTER-EXPONENTS-<-2))
 (248 228 (:REWRITE PREFER-POSITIVE-EXPONENTS-SCATTER-EXPONENTS-<))
 (231 11 (:DEFINITION BINARY-APPEND))
 (228 102 (:REWRITE |(+ c (+ d x))|))
 (222 222 (:TYPE-PRESCRIPTION BUBBLE-DOWN))
 (219 25 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (210 50 (:REWRITE |(- (if a b c))|))
 (208 194 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (199 199 (:REWRITE |(< 0 (* x y))|))
 (182 182 (:REWRITE |(< x (+ c/d y))|))
 (168 13 (:REWRITE CLUSTER-P-CORRECTNESS-1))
 (151 151 (:REWRITE DEFAULT-MINUS))
 (146 146 (:REWRITE |(< 0 (/ x))|))
 (140 140 (:REWRITE |(< y (+ (- c) x))|))
 (132 44 (:REWRITE STR::CONSP-OF-MAKE-CHARACTER-LIST))
 (130 130 (:REWRITE ARITH-NORMALIZE-ADDENDS))
 (120 112 (:REWRITE SIMPLIFY-PRODUCTS-SCATTER-EXPONENTS-EQUAL))
 (120 112 (:REWRITE PREFER-POSITIVE-EXPONENTS-SCATTER-EXPONENTS-EQUAL))
 (115 115 (:REWRITE |(< (+ c/d x) y)|))
 (112 112 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (110 110 (:TYPE-PRESCRIPTION MAKE-CHARACTER-LIST))
 (110 22 (:REWRITE APPEND-WHEN-NOT-CONSP))
 (94 12 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (88 22 (:REWRITE |(* y x)|))
 (80 10 (:REWRITE |(- (+ x y))|))
 (77 77 (:TYPE-PRESCRIPTION CHARACTER-LISTP))
 (73 73 (:REWRITE |(< (/ x) 0)|))
 (73 73 (:REWRITE |(< (* x y) 0)|))
 (66 66 (:REWRITE STR::HEX-DIGIT-CHAR-LISTP-WHEN-SUBSETP-EQUAL))
 (66 33 (:REWRITE STR::HEX-DIGIT-CHAR-LISTP-WHEN-NOT-CONSP))
 (63 63 (:TYPE-PRESCRIPTION NFIX))
 (55 55 (:REWRITE CONSP-OF-TAKE))
 (50 50 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (50 50 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (48 48 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (48 48 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (44 44 (:REWRITE DEFAULT-TIMES-2))
 (44 44 (:REWRITE DEFAULT-TIMES-1))
 (40 24 (:REWRITE ACL2-NUMBERP-X))
 (24 24 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (22 22 (:REWRITE |(* a (/ a))|))
 (22 11 (:REWRITE STR::HEX-DIGIT-CHAR-LISTP-OF-TAKE))
 (22 11 (:REWRITE STR::HEX-DIGIT-CHAR-LISTP-OF-CDR-WHEN-HEX-DIGIT-CHAR-LISTP))
 (20 20 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (20 10 (:TYPE-PRESCRIPTION TRUE-LISTP-NTHCDR-TYPE-PRESCRIPTION))
 (17 17 (:REWRITE REDUCE-INTEGERP-+))
 (17 17 (:REWRITE INTEGERP-MINUS-X))
 (17 17 (:META META-INTEGERP-CORRECT))
 (16 4 (:REWRITE RATIONALP-X))
 (12 12 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (11 11 (:REWRITE CHARACTER-LISTP-OF-EXPLODE))
 (11 11 (:REWRITE |(<= (/ x) y) with (< x 0)|))
 (11 11 (:REWRITE |(<= (/ x) y) with (< 0 x)|))
 (11 11 (:REWRITE |(< x (/ y)) with (< y 0)|))
 (11 11 (:REWRITE |(< x (/ y)) with (< 0 y)|))
 (10 10 (:REWRITE |(- (- x))|))
 (1 1 (:TYPE-PRESCRIPTION STRINGP-OF-IMPLODE))
 )
(MAKE-CLUSTERS-CORRECTNESS-2
 (39608 626 (:REWRITE |(< (if a b c) x)|))
 (35463 493 (:REWRITE |(< x (if a b c))|))
 (29882 1418 (:REWRITE NFIX-WHEN-ZP))
 (28687 346 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (27963 234 (:DEFINITION STRING-LISTP))
 (26369 134 (:DEFINITION TRUE-LISTP))
 (25718 40 (:DEFINITION TAKE))
 (13283 300 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (13099 2240 (:REWRITE DEFAULT-CDR))
 (12658 216 (:REWRITE CONSP-OF-NTHCDR))
 (11921 10047 (:REWRITE DEFAULT-PLUS-2))
 (11844 246 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (11787 216 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (11556 10047 (:REWRITE DEFAULT-PLUS-1))
 (10760 20 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (9196 3564 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (8515 504 (:REWRITE |(< (+ (- c) x) y)|))
 (7959 206 (:REWRITE NONEMPTY-STRING-LISTP-OF-CDR-WHEN-NONEMPTY-STRING-LISTP))
 (7628 80 (:REWRITE TAKE-OF-LEN-FREE))
 (6966 162 (:REWRITE |(equal (if a b c) x)|))
 (6469 309 (:REWRITE |(+ x (if a b c))|))
 (6228 30 (:REWRITE CAR-OF-NTHCDR))
 (5864 60 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (5628 488 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (5496 4614 (:REWRITE DEFAULT-LESS-THAN-2))
 (5146 66 (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-ATOM))
 (5076 60 (:REWRITE LEN-OF-LIST-FIX))
 (4878 4614 (:REWRITE DEFAULT-LESS-THAN-1))
 (4780 30 (:DEFINITION NTH))
 (4614 4614 (:REWRITE THE-FLOOR-BELOW))
 (4614 4614 (:REWRITE THE-FLOOR-ABOVE))
 (4370 36 (:REWRITE REPEAT-WHEN-ZP))
 (4002 12 (:REWRITE NTHCDR-OF-NTHCDR))
 (3880 2668 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (3702 3570 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (3684 264 (:REWRITE DEFAULT-CAR))
 (3564 3564 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (3560 38 (:DEFINITION MAKE-LIST-AC))
 (3500 38 (:REWRITE CONSP-OF-MAKE-LIST-AC))
 (3450 274 (:REWRITE |(+ (if a b c) x)|))
 (3444 16 (:REWRITE CHARACTER-LISTP-OF-TAKE))
 (3440 80 (:REWRITE CONSP-OF-TAKE))
 (3397 899 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (3200 3192 (:REWRITE |(< c (- x))|))
 (3192 3192 (:REWRITE INTEGERP-<-CONSTANT))
 (3192 3192 (:REWRITE CONSTANT-<-INTEGERP))
 (3192 3192 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (3192 3192 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (3192 3192 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (3192 3192 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (3192 3192 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (3192 3192 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (3192 3192 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (3192 3192 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (3192 3192 (:REWRITE |(< (/ x) (/ y))|))
 (3192 3192 (:REWRITE |(< (- x) c)|))
 (3192 3192 (:REWRITE |(< (- x) (- y))|))
 (3190 214 (:REWRITE |(equal (+ (- c) x) y)|))
 (3010 346 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (2880 64 (:REWRITE STR::CONSP-OF-MAKE-CHARACTER-LIST))
 (2733 20 (:REWRITE LIST-FIX-WHEN-LEN-ZERO))
 (2620 2620 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (2560 2560 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (2482 20 (:DEFINITION BINARY-APPEND))
 (1902 80 (:REWRITE TAKE-WHEN-ATOM))
 (1494 1494 (:TYPE-PRESCRIPTION STRING-LISTP))
 (1352 864 (:REWRITE |(+ c (+ d x))|))
 (1341 1341 (:LINEAR POSITION-WHEN-MEMBER))
 (1341 1341 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (1267 1255 (:TYPE-PRESCRIPTION BUBBLE-DOWN))
 (1204 20 (:REWRITE LIST-FIX-WHEN-NOT-CONSP))
 (1188 208 (:REWRITE |(- (if a b c))|))
 (1021 969 (:REWRITE DEFAULT-MINUS))
 (976 976 (:TYPE-PRESCRIPTION NONEMPTY-STRING-LISTP))
 (976 976 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (976 516 (:REWRITE SIMPLIFY-PRODUCTS-SCATTER-EXPONENTS-<))
 (975 975 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (975 975 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (925 839 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (899 899 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (899 899 (:REWRITE |(equal c (/ x))|))
 (899 899 (:REWRITE |(equal c (- x))|))
 (899 899 (:REWRITE |(equal (/ x) c)|))
 (899 899 (:REWRITE |(equal (/ x) (/ y))|))
 (899 899 (:REWRITE |(equal (- x) c)|))
 (899 899 (:REWRITE |(equal (- x) (- y))|))
 (857 857 (:REWRITE |(< x (+ c/d y))|))
 (848 848 (:REWRITE |(< 0 (* x y))|))
 (845 759 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (734 100 (:REWRITE STR::CHARACTER-LISTP-WHEN-HEX-DIGIT-CHAR-LISTP))
 (720 126 (:REWRITE |(+ x x)|))
 (697 697 (:REWRITE |(< y (+ (- c) x))|))
 (652 574 (:REWRITE DEFAULT-TIMES-2))
 (648 648 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (648 324 (:REWRITE OMAP::SETP-WHEN-MAPP))
 (648 324 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (642 642 (:REWRITE |(< 0 (/ x))|))
 (576 516 (:REWRITE PREFER-POSITIVE-EXPONENTS-SCATTER-EXPONENTS-<-2))
 (576 516 (:REWRITE PREFER-POSITIVE-EXPONENTS-SCATTER-EXPONENTS-<))
 (574 574 (:REWRITE DEFAULT-TIMES-1))
 (544 544 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (544 544 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (504 504 (:REWRITE |(< (+ c/d x) y)|))
 (346 346 (:REWRITE TRUE-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (336 84 (:REWRITE |(+ (* c x) (* d x))|))
 (324 324 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (324 324 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
 (324 324 (:REWRITE SET::IN-SET))
 (294 294 (:REWRITE |(< (/ x) 0)|))
 (294 294 (:REWRITE |(< (* x y) 0)|))
 (288 48 (:REWRITE NONEMPTY-STRING-LISTP-OF-NTHCDR))
 (264 6 (:REWRITE CDR-OF-LIST-FIX))
 (240 24 (:REWRITE |(* x (- y))|))
 (228 48 (:REWRITE |(- (* c x))|))
 (226 226 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (226 88 (:REWRITE STR::HEX-DIGIT-CHAR-LISTP-WHEN-NOT-CONSP))
 (225 225 (:REWRITE ARITH-NORMALIZE-ADDENDS))
 (208 208 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (208 208 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (204 204 (:TYPE-PRESCRIPTION STR::HEX-DIGIT-CHAR-LISTP))
 (176 176 (:REWRITE STR::HEX-DIGIT-CHAR-LISTP-WHEN-SUBSETP-EQUAL))
 (168 104 (:REWRITE ACL2-NUMBERP-X))
 (160 160 (:TYPE-PRESCRIPTION MAKE-CHARACTER-LIST))
 (156 140 (:REWRITE SIMPLIFY-PRODUCTS-SCATTER-EXPONENTS-EQUAL))
 (156 140 (:REWRITE PREFER-POSITIVE-EXPONENTS-SCATTER-EXPONENTS-EQUAL))
 (144 18 (:REWRITE CHARACTER-LISTP-OF-NTHCDR))
 (108 18 (:REWRITE NONEMPTY-STRINGP-OF-NTH-WHEN-NONEMPTY-STRING-LISTP))
 (92 92 (:REWRITE |(* a (/ a))|))
 (84 84 (:REWRITE REDUCE-INTEGERP-+))
 (84 84 (:REWRITE INTEGERP-MINUS-X))
 (84 84 (:META META-INTEGERP-CORRECT))
 (80 80 (:REWRITE FOLD-CONSTS-IN-+))
 (74 74 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (72 18 (:REWRITE STRINGP-OF-NTH))
 (66 6 (:REWRITE |(* y (* x z))|))
 (64 16 (:REWRITE RATIONALP-X))
 (48 18 (:REWRITE |(equal x (if a b c))|))
 (46 46 (:REWRITE |(<= (/ x) y) with (< x 0)|))
 (46 46 (:REWRITE |(<= (/ x) y) with (< 0 x)|))
 (46 46 (:REWRITE |(< x (/ y)) with (< y 0)|))
 (46 46 (:REWRITE |(< x (/ y)) with (< 0 y)|))
 (36 36 (:REWRITE |(* (- x) y)|))
 (32 16 (:REWRITE STR::HEX-DIGIT-CHAR-LISTP-OF-TAKE))
 (30 30 (:REWRITE ARITH-NORMALIZE-FACTORS-SCATTER-EXPONENTS))
 (28 28 (:REWRITE CHARACTER-LISTP-OF-EXPLODE))
 (26 26 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (26 26 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (24 12 (:REWRITE STR::HEX-DIGIT-CHAR-LISTP-OF-NTHCDR))
 (20 20 (:REWRITE |arith (* c (* d x))|))
 (8 8 (:REWRITE NORMALIZE-FACTORS-SCATTER-EXPONENTS))
 (6 6 (:TYPE-PRESCRIPTION NOT-INTEGERP-4A))
 (6 6 (:TYPE-PRESCRIPTION NOT-INTEGERP-3A))
 (6 6 (:TYPE-PRESCRIPTION NOT-INTEGERP-2A))
 (6 6 (:TYPE-PRESCRIPTION NOT-INTEGERP-1A))
 (6 6 (:TYPE-PRESCRIPTION ABS))
 (6 6 (:REWRITE |(< (/ x) y) with (< x 0)|))
 (6 6 (:REWRITE |(< (/ x) y) with (< 0 x)|))
 (6 6 (:REWRITE |(* a (/ a) b)|))
 (2 2 (:REWRITE THEN-SUBSEQ-SAME-1))
 (2 2 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-=-0))
 )
(LEN-OF-MAKE-CLUSTERS
 (34870 486 (:REWRITE |(< x (if a b c))|))
 (33211 428 (:REWRITE |(< (if a b c) x)|))
 (23196 23196 (:TYPE-PRESCRIPTION NOT-INTEGERP-3B))
 (23196 23196 (:TYPE-PRESCRIPTION NOT-INTEGERP-2B))
 (22547 758 (:REWRITE NFIX-WHEN-ZP))
 (22292 41 (:DEFINITION TAKE))
 (14918 8293 (:REWRITE DEFAULT-PLUS-2))
 (12967 1051 (:TYPE-PRESCRIPTION FLOOR-ZERO . 2))
 (9395 8293 (:REWRITE DEFAULT-PLUS-1))
 (9129 1053 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 1))
 (9111 1051 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 1))
 (9092 3303 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (8823 1019 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 1))
 (8640 488 (:REWRITE |(< (+ (- c) x) y)|))
 (8456 109 (:REWRITE FLOOR-ZERO . 3))
 (8242 1418 (:REWRITE DEFAULT-CDR))
 (6820 82 (:REWRITE TAKE-OF-LEN-FREE))
 (5265 1053 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 3))
 (5265 1053 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 3))
 (5265 1053 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 2))
 (5255 1051 (:TYPE-PRESCRIPTION FLOOR-ZERO . 1))
 (5255 1051 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 3))
 (5255 1051 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 2))
 (5249 35 (:REWRITE CHARACTER-LISTP-OF-TAKE))
 (5085 1017 (:TYPE-PRESCRIPTION FLOOR-NONNEGATIVE . 3))
 (5068 83 (:REWRITE STR::MAKE-CHARACTER-LIST-WHEN-ATOM))
 (4893 4182 (:REWRITE DEFAULT-LESS-THAN-2))
 (4460 4182 (:REWRITE DEFAULT-LESS-THAN-1))
 (4432 1405 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (4382 109 (:REWRITE FLOOR-X-Y-=-1 . 2))
 (4372 109 (:REWRITE FLOOR-ZERO . 4))
 (4182 4182 (:REWRITE THE-FLOOR-BELOW))
 (4182 4182 (:REWRITE THE-FLOOR-ABOVE))
 (4161 86 (:REWRITE TRUE-LISTP-WHEN-STRING-LIST))
 (4141 37 (:REWRITE REPEAT-WHEN-ZP))
 (3925 77 (:DEFINITION STRING-LISTP))
 (3876 40 (:DEFINITION MAKE-LIST-AC))
 (3800 40 (:REWRITE CONSP-OF-MAKE-LIST-AC))
 (3789 41 (:DEFINITION TRUE-LISTP))
 (3501 1388 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (3428 109 (:REWRITE FLOOR-ZERO . 5))
 (3395 3307 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (3303 3303 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (2924 2920 (:REWRITE |(< c (- x))|))
 (2924 203 (:REWRITE |(equal (+ (- c) x) y)|))
 (2920 2920 (:REWRITE INTEGERP-<-CONSTANT))
 (2920 2920 (:REWRITE CONSTANT-<-INTEGERP))
 (2920 2920 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (2920 2920 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (2920 2920 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (2920 2920 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (2920 2920 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (2920 2920 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (2920 2920 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (2920 2920 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (2920 2920 (:REWRITE |(< (/ x) (/ y))|))
 (2920 2920 (:REWRITE |(< (- x) c)|))
 (2920 2920 (:REWRITE |(< (- x) (- y))|))
 (2722 2177 (:REWRITE DEFAULT-TIMES-1))
 (2714 2177 (:REWRITE DEFAULT-TIMES-2))
 (2699 826 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (2668 8 (:REWRITE NTHCDR-OF-NTHCDR))
 (2643 146 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (2593 1802 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (2591 2200 (:REWRITE SIMPLIFY-SUMS-<))
 (2524 1107 (:REWRITE PREFER-POSITIVE-EXPONENTS-SCATTER-EXPONENTS-<-2))
 (2415 175 (:REWRITE CONSP-OF-TAKE))
 (2212 140 (:REWRITE STR::CONSP-OF-MAKE-CHARACTER-LIST))
 (2172 38 (:DEFINITION BINARY-APPEND))
 (2076 2076 (:LINEAR POSITION-WHEN-MEMBER))
 (2076 2076 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (2035 2035 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (1971 76 (:REWRITE NONEMPTY-STRINGP-OF-CAR-WHEN-NONEMPTY-STRING-LISTP))
 (1967 151 (:REWRITE DEFAULT-CAR))
 (1886 28 (:REWRITE CONSP-OF-CDR-OF-NTHCDR))
 (1877 25 (:REWRITE CONSP-OF-NTHCDR))
 (1822 115 (:REWRITE FLOOR-=-X/Y . 3))
 (1730 82 (:REWRITE TAKE-WHEN-ATOM))
 (1727 1091 (:REWRITE SIMPLIFY-PRODUCTS-SCATTER-EXPONENTS-<))
 (1488 1488 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (1408 1408 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (1408 1408 (:REWRITE |(equal c (/ x))|))
 (1408 1408 (:REWRITE |(equal c (- x))|))
 (1408 1408 (:REWRITE |(equal (/ x) c)|))
 (1408 1408 (:REWRITE |(equal (/ x) (/ y))|))
 (1408 1408 (:REWRITE |(equal (- x) c)|))
 (1408 1408 (:REWRITE |(equal (- x) (- y))|))
 (1309 71 (:REWRITE NONEMPTY-STRING-LISTP-OF-CDR-WHEN-NONEMPTY-STRING-LISTP))
 (1305 1305 (:TYPE-PRESCRIPTION NOT-INTEGERP-3A))
 (1305 1305 (:TYPE-PRESCRIPTION NOT-INTEGERP-2A))
 (1263 117 (:REWRITE DEFAULT-FLOOR-RATIO))
 (1252 1091 (:REWRITE PREFER-POSITIVE-EXPONENTS-SCATTER-EXPONENTS-<))
 (1227 5 (:REWRITE CAR-OF-NTHCDR))
 (1201 109 (:REWRITE FLOOR-=-X/Y . 2))
 (1166 3 (:REWRITE TRUE-LIST-FIX-WHEN-TRUE-LISTP))
 (1115 119 (:REWRITE |(* (- x) y)|))
 (1112 10 (:REWRITE NTH-WHEN->=-N-LEN-L))
 (1015 579 (:REWRITE SIMPLIFY-PRODUCTS-SCATTER-EXPONENTS-EQUAL))
 (996 130 (:REWRITE STR::CHARACTER-LISTP-WHEN-HEX-DIGIT-CHAR-LISTP))
 (970 964 (:TYPE-PRESCRIPTION BUBBLE-DOWN))
 (904 5 (:DEFINITION NTH))
 (884 854 (:REWRITE DEFAULT-MINUS))
 (868 868 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (868 868 (:REWRITE DEFAULT-DIVIDE))
 (834 834 (:REWRITE |(< 0 (* x y))|))
 (831 109 (:REWRITE FLOOR-X-Y-=--1 . 2))
 (808 808 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (802 47 (:LINEAR LINEAR-FLOOR-BOUNDS-2))
 (766 150 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-NOT-CONSP))
 (713 713 (:REWRITE |(< x (+ c/d y))|))
 (671 86 (:REWRITE SET::SETS-ARE-TRUE-LISTS-CHEAP))
 (629 629 (:REWRITE |(< 0 (/ x))|))
 (612 109 (:REWRITE FLOOR-ZERO . 2))
 (612 109 (:REWRITE FLOOR-X-Y-=-1 . 3))
 (612 109 (:REWRITE FLOOR-X-Y-=--1 . 3))
 (602 107 (:REWRITE FLOOR-CANCEL-*-REWRITING-GOAL-LITERAL))
 (602 107 (:REWRITE |(floor x (* y (/ z))) rewriting-goal-literal|))
 (602 107 (:REWRITE |(floor (* x (/ y)) z) rewriting-goal-literal|))
 (543 543 (:REWRITE |(< y (+ (- c) x))|))
 (538 107 (:REWRITE FLOOR-CANCEL-*-CONST))
 (491 491 (:REWRITE |(< (+ c/d x) y)|))
 (435 87 (:TYPE-PRESCRIPTION FLOOR-NONNEGATIVE . 1))
 (400 400 (:TYPE-PRESCRIPTION STRING-LISTP))
 (350 350 (:TYPE-PRESCRIPTION MAKE-CHARACTER-LIST))
 (311 3 (:REWRITE LIST-FIX-WHEN-LEN-ZERO))
 (302 302 (:REWRITE |(< (* x y) 0)|))
 (300 300 (:TYPE-PRESCRIPTION NONEMPTY-STRING-LISTP))
 (300 300 (:REWRITE NONEMPTY-STRING-LISTP-WHEN-SUBSETP-EQUAL))
 (300 300 (:REWRITE |(< (/ x) 0)|))
 (292 292 (:TYPE-PRESCRIPTION TRUE-LISTP))
 (292 122 (:REWRITE STR::HEX-DIGIT-CHAR-LISTP-WHEN-NOT-CONSP))
 (289 289 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (289 289 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (287 287 (:TYPE-PRESCRIPTION STR::HEX-DIGIT-CHAR-LISTP))
 (263 263 (:REWRITE ARITH-NORMALIZE-ADDENDS))
 (260 260 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (260 260 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (247 247 (:REWRITE |arith (* c (* d x))|))
 (244 244 (:REWRITE STR::HEX-DIGIT-CHAR-LISTP-WHEN-SUBSETP-EQUAL))
 (243 109 (:REWRITE |(< (* (/ x) y) 1) with (< 0 x)|))
 (228 48 (:REWRITE |(+ x x)|))
 (184 117 (:REWRITE DEFAULT-FLOOR-1))
 (183 123 (:REWRITE |(- (* c x))|))
 (176 109 (:REWRITE |(< (* (/ x) y) 1) with (< x 0)|))
 (162 162 (:TYPE-PRESCRIPTION SET::SETP-TYPE))
 (162 81 (:REWRITE OMAP::SETP-WHEN-MAPP))
 (162 81 (:REWRITE SET::NONEMPTY-MEANS-SET))
 (145 145 (:REWRITE NORMALIZE-FACTORS-SCATTER-EXPONENTS))
 (117 117 (:REWRITE DEFAULT-FLOOR-2))
 (114 8 (:REWRITE |(not (equal (* (/ x) y) 1))|))
 (114 8 (:REWRITE |(equal (* (/ x) y) 1)|))
 (112 28 (:REWRITE |(+ (* c x) (* d x))|))
 (107 107 (:REWRITE FLOOR-CANCEL-*-NOT-REWRITING-GOAL-LITERAL))
 (107 107 (:REWRITE |(floor x (- y))| . 2))
 (107 107 (:REWRITE |(floor x (- y))| . 1))
 (107 107 (:REWRITE |(floor x (* y (/ z))) not rewriting-goal-literal|))
 (107 107 (:REWRITE |(floor (- x) y)| . 2))
 (107 107 (:REWRITE |(floor (- x) y)| . 1))
 (107 107 (:REWRITE |(floor (* x (/ y)) z) not rewriting-goal-literal|))
 (100 100 (:REWRITE REDUCE-INTEGERP-+))
 (100 100 (:REWRITE INTEGERP-MINUS-X))
 (100 100 (:META META-INTEGERP-CORRECT))
 (99 3 (:REWRITE LIST-FIX-WHEN-NOT-CONSP))
 (96 12 (:REWRITE CHARACTER-LISTP-OF-NTHCDR))
 (86 86 (:REWRITE TRUE-LISTP-WHEN-UNSIGNED-BYTE-LISTP))
 (82 82 (:REWRITE ACL2-NUMBERP-X))
 (81 81 (:TYPE-PRESCRIPTION OMAP::MAPP))
 (81 81 (:TYPE-PRESCRIPTION SET::EMPTY-TYPE))
 (81 81 (:REWRITE SET::IN-SET))
 (73 73 (:REWRITE |arith (* (- x) y)|))
 (70 70 (:REWRITE-QUOTED-CONSTANT NFIX-UNDER-NAT-EQUIV))
 (70 35 (:REWRITE STR::HEX-DIGIT-CHAR-LISTP-OF-TAKE))
 (55 55 (:REWRITE |arith (- (* c x))|))
 (52 52 (:REWRITE FOLD-CONSTS-IN-+))
 (46 2 (:REWRITE INTEGERP-+-REDUCE-CONSTANT))
 (44 4 (:REWRITE |(* y (* x z))|))
 (43 43 (:REWRITE CHARACTER-LISTP-OF-EXPLODE))
 (39 9 (:REWRITE |(* (if a b c) x)|))
 (35 35 (:REWRITE |(<= (/ x) y) with (< x 0)|))
 (35 35 (:REWRITE |(<= (/ x) y) with (< 0 x)|))
 (35 35 (:REWRITE |(< x (/ y)) with (< y 0)|))
 (35 35 (:REWRITE |(< x (/ y)) with (< 0 y)|))
 (25 3 (:REWRITE FLOOR-=-X/Y . 4))
 (24 9 (:REWRITE |(equal x (if a b c))|))
 (16 8 (:REWRITE STR::HEX-DIGIT-CHAR-LISTP-OF-NTHCDR))
 (16 1 (:REWRITE |(integerp (- x))|))
 (15 15 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (15 15 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (12 2 (:REWRITE NONEMPTY-STRING-LISTP-OF-NTHCDR))
 (6 1 (:REWRITE NONEMPTY-STRINGP-OF-NTH-WHEN-NONEMPTY-STRING-LISTP))
 (5 1 (:REWRITE |(equal (floor (+ x y) z) x)|))
 (4 4 (:TYPE-PRESCRIPTION ABS))
 (4 4 (:REWRITE |(< (/ x) y) with (< x 0)|))
 (4 4 (:REWRITE |(< (/ x) y) with (< 0 x)|))
 (4 1 (:REWRITE STRINGP-OF-NTH))
 (2 2 (:REWRITE THEN-SUBSEQ-SAME-1))
 (2 2 (:REWRITE |(floor (+ x r) i)|))
 (2 2 (:REWRITE |(<= 1 (* (/ x) y)) with (< x 0)|))
 (2 2 (:REWRITE |(<= 1 (* (/ x) y)) with (< 0 x)|))
 (1 1 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-=-0))
 )
(MAKE-CLUSTERS-CORRECTNESS-3
 (10723 10723 (:TYPE-PRESCRIPTION NOT-INTEGERP-3B))
 (10723 10723 (:TYPE-PRESCRIPTION NOT-INTEGERP-2B))
 (10723 10723 (:TYPE-PRESCRIPTION NOT-INTEGERP-1B))
 (4828 436 (:TYPE-PRESCRIPTION FLOOR-ZERO . 2))
 (3922 3922 (:REWRITE |arith (* c (* d x))|))
 (3513 437 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 1))
 (3513 437 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 1))
 (3504 436 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 1))
 (2983 27 (:REWRITE FLOOR-ZERO . 3))
 (2185 437 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 3))
 (2185 437 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 2))
 (2185 437 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 3))
 (2185 437 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 2))
 (2180 436 (:TYPE-PRESCRIPTION FLOOR-ZERO . 1))
 (2180 436 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 3))
 (2180 436 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 2))
 (2180 436 (:TYPE-PRESCRIPTION FLOOR-NONNEGATIVE . 3))
 (1638 108 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (1624 163 (:REWRITE PREFER-POSITIVE-EXPONENTS-SCATTER-EXPONENTS-<-2))
 (1580 316 (:TYPE-PRESCRIPTION MOD-ZERO . 2))
 (1280 316 (:TYPE-PRESCRIPTION MOD-POSITIVE . 2))
 (1280 316 (:TYPE-PRESCRIPTION MOD-NEGATIVE . 2))
 (1249 27 (:REWRITE FLOOR-ZERO . 5))
 (1170 27 (:REWRITE FLOOR-X-Y-=-1 . 2))
 (1168 27 (:REWRITE FLOOR-ZERO . 4))
 (1146 61 (:DEFINITION LEN))
 (1115 190 (:REWRITE DEFAULT-PLUS-2))
 (1103 786 (:REWRITE DEFAULT-TIMES-1))
 (1057 786 (:REWRITE DEFAULT-TIMES-2))
 (1050 25 (:REWRITE CANCEL-MOD-+))
 (973 97 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (897 25 (:REWRITE MOD-X-Y-=-X . 4))
 (839 839 (:TYPE-PRESCRIPTION NOT-INTEGERP-3A))
 (839 839 (:TYPE-PRESCRIPTION NOT-INTEGERP-2A))
 (839 839 (:TYPE-PRESCRIPTION NOT-INTEGERP-1A))
 (797 25 (:REWRITE MOD-X-Y-=-X-Y . 2))
 (772 25 (:REWRITE MOD-X-Y-=-X . 3))
 (639 11 (:REWRITE MOD-X-Y-=-X-Y . 1))
 (637 55 (:REWRITE SIMPLIFY-PRODUCTS-SCATTER-EXPONENTS-EQUAL))
 (622 52 (:REWRITE |(* (- x) y)|))
 (600 25 (:REWRITE MOD-ZERO . 3))
 (594 27 (:REWRITE CANCEL-FLOOR-+))
 (561 72 (:REWRITE STR::CONSP-OF-EXPLODE))
 (525 105 (:TYPE-PRESCRIPTION FLOOR-NONNEGATIVE . 1))
 (461 25 (:REWRITE MOD-ZERO . 4))
 (432 27 (:REWRITE FLOOR-=-X/Y . 3))
 (400 25 (:REWRITE |(integerp (- x))|))
 (353 236 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (347 53 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (316 316 (:TYPE-PRESCRIPTION MOD-ZERO . 4))
 (316 316 (:TYPE-PRESCRIPTION MOD-ZERO . 3))
 (316 316 (:TYPE-PRESCRIPTION MOD-POSITIVE . 1))
 (316 316 (:TYPE-PRESCRIPTION MOD-NEGATIVE . 1))
 (315 315 (:TYPE-PRESCRIPTION MOD-NONPOSITIVE))
 (315 315 (:TYPE-PRESCRIPTION INTEGERP-MOD-2))
 (315 315 (:TYPE-PRESCRIPTION INTEGERP-MOD-1))
 (313 313 (:REWRITE DEFAULT-DIVIDE))
 (312 312 (:REWRITE NORMALIZE-TERMS-SUCH-AS-1/AX+BX))
 (308 12 (:LINEAR MOD-BOUNDS-3))
 (308 11 (:REWRITE MOD-ZERO . 1))
 (307 259 (:REWRITE DEFAULT-LESS-THAN-2))
 (297 27 (:REWRITE FLOOR-=-X/Y . 2))
 (297 27 (:REWRITE DEFAULT-FLOOR-RATIO))
 (259 259 (:REWRITE THE-FLOOR-BELOW))
 (259 259 (:REWRITE THE-FLOOR-ABOVE))
 (257 257 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (257 257 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (257 257 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (256 256 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (256 256 (:REWRITE INTEGERP-<-CONSTANT))
 (256 256 (:REWRITE CONSTANT-<-INTEGERP))
 (256 256 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (256 256 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (256 256 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (256 256 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (256 256 (:REWRITE |(< c (- x))|))
 (256 256 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (256 256 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (256 256 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (256 256 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (256 256 (:REWRITE |(< (/ x) (/ y))|))
 (256 256 (:REWRITE |(< (- x) c)|))
 (256 256 (:REWRITE |(< (- x) (- y))|))
 (236 35 (:REWRITE RATIONALP-X))
 (232 24 (:LINEAR MOD-BOUNDS-2))
 (224 145 (:REWRITE PREFER-POSITIVE-EXPONENTS-SCATTER-EXPONENTS-<))
 (213 213 (:REWRITE NORMALIZE-FACTORS-SCATTER-EXPONENTS))
 (205 190 (:REWRITE DEFAULT-PLUS-1))
 (192 12 (:LINEAR LINEAR-FLOOR-BOUNDS-2))
 (189 27 (:REWRITE FLOOR-X-Y-=--1 . 2))
 (170 170 (:REWRITE |arith (* (- x) y)|))
 (169 61 (:REWRITE DEFAULT-CDR))
 (163 63 (:REWRITE DEFAULT-MINUS))
 (162 27 (:REWRITE FLOOR-ZERO . 2))
 (162 27 (:REWRITE FLOOR-X-Y-=-1 . 3))
 (162 27 (:REWRITE FLOOR-X-Y-=--1 . 3))
 (162 27 (:REWRITE FLOOR-CANCEL-*-REWRITING-GOAL-LITERAL))
 (162 27 (:REWRITE FLOOR-CANCEL-*-CONST))
 (162 27 (:REWRITE |(floor x (* y (/ z))) rewriting-goal-literal|))
 (162 27 (:REWRITE |(floor (* x (/ y)) z) rewriting-goal-literal|))
 (155 155 (:REWRITE |arith (- (* c x))|))
 (131 131 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (130 92 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (126 14 (:REWRITE ACL2-NUMBERP-X))
 (125 110 (:REWRITE |(equal (/ x) c)|))
 (125 25 (:REWRITE MOD-X-Y-=-X-Y . 3))
 (125 25 (:REWRITE MOD-X-Y-=-X+Y . 3))
 (125 25 (:REWRITE MOD-X-Y-=-X+Y . 2))
 (125 25 (:REWRITE MOD-X-Y-=-X . 2))
 (125 25 (:REWRITE MOD-CANCEL-*-REWRITING-GOAL-LITERAL))
 (125 25 (:REWRITE MOD-CANCEL-*-CONST))
 (125 25 (:REWRITE |(mod x (* y (/ z))) rewriting-goal-literal|))
 (125 25 (:REWRITE |(mod (+ x (mod a b)) y)|))
 (125 25 (:REWRITE |(mod (+ x (- (mod a b))) y)|))
 (125 25 (:REWRITE |(mod (* x (/ y)) z) rewriting-goal-literal|))
 (119 119 (:REWRITE REDUCE-INTEGERP-+))
 (119 119 (:REWRITE INTEGERP-MINUS-X))
 (119 119 (:META META-INTEGERP-CORRECT))
 (110 110 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (110 110 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (110 110 (:REWRITE |(equal c (/ x))|))
 (110 110 (:REWRITE |(equal (/ x) (/ y))|))
 (110 110 (:REWRITE |(equal (- x) (- y))|))
 (109 109 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (109 109 (:REWRITE |(equal c (- x))|))
 (109 109 (:REWRITE |(equal (- x) c)|))
 (108 108 (:TYPE-PRESCRIPTION STR::TRUE-LISTP-OF-EXPLODE))
 (88 88 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (81 27 (:REWRITE |(< (* (/ x) y) 1) with (< 0 x)|))
 (75 75 (:REWRITE |(< 0 (* x y))|))
 (74 74 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (74 74 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (74 74 (:REWRITE |(< 0 (/ x))|))
 (65 13 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (62 62 (:LINEAR POSITION-WHEN-MEMBER))
 (62 62 (:LINEAR POSITION-EQUAL-AC-WHEN-MEMBER))
 (55 11 (:REWRITE MOD-ZERO . 2))
 (55 11 (:REWRITE MOD-X-Y-=-X+Y . 1))
 (55 11 (:REWRITE BUBBLE-DOWN-+-MATCH-3))
 (54 27 (:REWRITE DEFAULT-FLOOR-1))
 (54 27 (:REWRITE |(< (* (/ x) y) 1) with (< x 0)|))
 (52 52 (:REWRITE |(- (* c x))|))
 (50 50 (:TYPE-PRESCRIPTION MAKE-CLUSTERS))
 (37 37 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-=-0))
 (36 36 (:REWRITE STR::EXPLODE-WHEN-NOT-STRINGP))
 (35 35 (:REWRITE RATIONALP-MINUS-X))
 (31 31 (:REWRITE REDUCE-RATIONALP-+))
 (31 31 (:META META-RATIONALP-CORRECT))
 (28 28 (:REWRITE DEFAULT-MOD-2))
 (27 27 (:REWRITE FLOOR-CANCEL-*-NOT-REWRITING-GOAL-LITERAL))
 (27 27 (:REWRITE DEFAULT-FLOOR-2))
 (27 27 (:REWRITE |(floor x (- y))| . 2))
 (27 27 (:REWRITE |(floor x (- y))| . 1))
 (27 27 (:REWRITE |(floor x (* y (/ z))) not rewriting-goal-literal|))
 (27 27 (:REWRITE |(floor (- x) y)| . 2))
 (27 27 (:REWRITE |(floor (- x) y)| . 1))
 (27 27 (:REWRITE |(floor (* x (/ y)) z) not rewriting-goal-literal|))
 (26 26 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (26 26 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (25 25 (:REWRITE MOD-CANCEL-*-NOT-REWRITING-GOAL-LITERAL))
 (25 25 (:REWRITE |(mod x (- y))| . 3))
 (25 25 (:REWRITE |(mod x (- y))| . 2))
 (25 25 (:REWRITE |(mod x (- y))| . 1))
 (25 25 (:REWRITE |(mod x (* y (/ z))) not rewriting-goal-literal|))
 (25 25 (:REWRITE |(mod (- x) y)| . 3))
 (25 25 (:REWRITE |(mod (- x) y)| . 2))
 (25 25 (:REWRITE |(mod (- x) y)| . 1))
 (25 25 (:REWRITE |(mod (* x (/ y)) z) not rewriting-goal-literal|))
 (20 20 (:REWRITE |(equal (+ (- c) x) y)|))
 (18 18 (:REWRITE |(* 1 x)|))
 (15 15 (:TYPE-PRESCRIPTION BUBBLE-DOWN))
 (13 13 (:REWRITE ZP-OPEN))
 (11 11 (:REWRITE ARITH-NORMALIZE-ADDENDS))
 (11 11 (:REWRITE |(equal (mod (+ x y) z) x)|))
 (11 11 (:REWRITE |(+ c (+ d x))|))
 (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 |(< (/ x) 0)|))
 (4 4 (:REWRITE |(< (* x y) 0)|))
 (1 1 (:REWRITE |(not (equal x (/ y)))|))
 (1 1 (:REWRITE |(equal x (/ y))|))
 (1 1 (:REWRITE |(<= (/ x) y) with (< x 0)|))
 (1 1 (:REWRITE |(<= (/ x) y) with (< 0 x)|))
 (1 1 (:REWRITE |(< x (/ y)) with (< y 0)|))
 (1 1 (:REWRITE |(< (+ c/d x) y)|))
 (1 1 (:REWRITE |(< (+ (- c) x) y)|))
 (1 1 (:REWRITE |(/ (/ x))|))
 )
(MAKE-CLUSTERS-OF-NIL
 (5 1 (:REWRITE STRINGP-WHEN-NONEMPTY-STRINGP))
 (2 2 (:TYPE-PRESCRIPTION NONEMPTY-STRINGP))
 (2 2 (:REWRITE NONEMPTY-STRINGP-WHEN-MEMBER-EQUAL-OF-NONEMPTY-STRING-LISTP))
 (1 1 (:REWRITE LENGTH-WHEN-STRINGP))
 )