(DEFAULT-ASH-1
 (8771 4 (:REWRITE FLOOR-=-X/Y . 4))
 (7038 6 (:LINEAR LINEAR-FLOOR-BOUNDS-1))
 (2806 61 (:REWRITE |(* (* x y) z)|))
 (1485 279 (:REWRITE DEFAULT-TIMES-1))
 (1431 279 (:REWRITE DEFAULT-TIMES-2))
 (1288 8 (:REWRITE FLOOR-ZERO . 3))
 (1091 1091 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NONPOSITIVE-BASE-ODD-EXPONENT))
 (1091 1091 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NONPOSITIVE-BASE-EVEN-EXPONENT))
 (1091 1091 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NEGATIVE-BASE-ODD-EXPONENT))
 (1091 1091 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NEGATIVE-BASE-EVEN-EXPONENT))
 (1091 1091 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-INTEGERP-BASE-B))
 (1091 1091 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-INTEGERP-BASE-A))
 (1091 1091 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-INTEGERP-BASE))
 (1040 8 (:REWRITE CANCEL-FLOOR-+))
 (832 8 (:REWRITE FLOOR-ZERO . 5))
 (832 8 (:REWRITE FLOOR-ZERO . 4))
 (824 14 (:REWRITE DEFAULT-FLOOR-RATIO))
 (824 8 (:REWRITE FLOOR-X-Y-=--1 . 2))
 (792 8 (:REWRITE FLOOR-X-Y-=-1 . 2))
 (704 8 (:REWRITE FLOOR-=-X/Y . 3))
 (704 8 (:REWRITE FLOOR-=-X/Y . 2))
 (552 8 (:REWRITE |(* (- x) y)|))
 (400 40 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (400 40 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (388 4 (:LINEAR LINEAR-FLOOR-BOUNDS-3))
 (352 4 (:LINEAR LINEAR-FLOOR-BOUNDS-2))
 (328 40 (:REWRITE DEFAULT-LESS-THAN-1))
 (248 8 (:REWRITE |(integerp (- x))|))
 (113 14 (:REWRITE DEFAULT-FLOOR-1))
 (112 40 (:REWRITE DEFAULT-LESS-THAN-2))
 (80 8 (:REWRITE FLOOR-ZERO . 2))
 (80 8 (:REWRITE FLOOR-X-Y-=-1 . 3))
 (80 8 (:REWRITE FLOOR-X-Y-=--1 . 3))
 (80 8 (:REWRITE FLOOR-CANCEL-*-CONST))
 (80 8 (:REWRITE DEFAULT-MINUS))
 (72 72 (:TYPE-PRESCRIPTION FLOOR-ZERO . 3))
 (72 72 (:TYPE-PRESCRIPTION FLOOR-ZERO . 2))
 (72 72 (:TYPE-PRESCRIPTION FLOOR-ZERO . 1))
 (72 72 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 3))
 (72 72 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 2))
 (72 72 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 1))
 (72 72 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 3))
 (72 72 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 2))
 (72 72 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 1))
 (72 72 (:TYPE-PRESCRIPTION FLOOR-NONNEGATIVE . 3))
 (72 72 (:TYPE-PRESCRIPTION FLOOR-NONNEGATIVE . 2))
 (72 72 (:TYPE-PRESCRIPTION FLOOR-NONNEGATIVE . 1))
 (72 72 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 3))
 (72 72 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 2))
 (72 72 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 1))
 (63 63 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (62 8 (:REWRITE FLOOR-CANCEL-*-NOT-REWRITING-GOAL-LITERAL))
 (62 8 (:REWRITE |(floor (* x (/ y)) z) not rewriting-goal-literal|))
 (48 48 (:REWRITE REDUCE-INTEGERP-+))
 (48 48 (:REWRITE INTEGERP-MINUS-X))
 (48 48 (:META META-INTEGERP-CORRECT))
 (40 40 (:REWRITE THE-FLOOR-BELOW))
 (40 40 (:REWRITE THE-FLOOR-ABOVE))
 (40 40 (:REWRITE SIMPLIFY-SUMS-<))
 (40 40 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (40 40 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (40 40 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (40 40 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (40 40 (:REWRITE INTEGERP-<-CONSTANT))
 (40 40 (:REWRITE CONSTANT-<-INTEGERP))
 (40 40 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (40 40 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (40 40 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (40 40 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (40 40 (:REWRITE |(< c (- x))|))
 (40 40 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (40 40 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (40 40 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (40 40 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (40 40 (:REWRITE |(< (/ x) (/ y))|))
 (40 40 (:REWRITE |(< (- x) c)|))
 (40 40 (:REWRITE |(< (- x) (- y))|))
 (32 32 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (28 2 (:REWRITE |(+ y x)|))
 (26 8 (:REWRITE FLOOR-CANCEL-*-REWRITING-GOAL-LITERAL))
 (26 8 (:REWRITE |(floor (* x (/ y)) z) rewriting-goal-literal|))
 (24 24 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (24 24 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (24 24 (:REWRITE |(< (/ x) 0)|))
 (24 24 (:REWRITE |(< (* x y) 0) rationalp (* x y)|))
 (24 24 (:REWRITE |(< (* x y) 0)|))
 (22 4 (:REWRITE DEFAULT-PLUS-2))
 (22 4 (:REWRITE DEFAULT-PLUS-1))
 (20 2 (:REWRITE |(equal (floor (+ x y) z) x)|))
 (14 14 (:REWRITE DEFAULT-FLOOR-2))
 (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 |(floor x (- y))| . 2))
 (8 8 (:REWRITE |(floor x (- y))| . 1))
 (8 8 (:REWRITE |(floor x (* y (/ z))) rewriting-goal-literal|))
 (8 8 (:REWRITE |(floor x (* y (/ z))) not rewriting-goal-literal|))
 (8 8 (:REWRITE |(floor (- x) y)| . 2))
 (8 8 (:REWRITE |(floor (- x) y)| . 1))
 (8 8 (:REWRITE |(< 0 (/ x))|))
 (8 8 (:REWRITE |(< 0 (* x y)) rationalp (* x y)|))
 (8 8 (:REWRITE |(< 0 (* x y))|))
 (8 8 (:REWRITE |(- (* c x))|))
 (4 4 (:REWRITE EXPT-WITH-VIOLATED-GUARDS))
 (2 2 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (2 2 (:REWRITE NORMALIZE-ADDENDS))
 (2 2 (:REWRITE DEFAULT-EXPT-1))
 (2 2 (:REWRITE |(expt 1/c n)|))
 (2 2 (:REWRITE |(expt (- x) n)|))
 )
(MAIN-1
 (30 6 (:TYPE-PRESCRIPTION MOD-ZERO . 2))
 (30 6 (:TYPE-PRESCRIPTION MOD-ZERO . 1))
 (30 6 (:TYPE-PRESCRIPTION MOD-POSITIVE . 2))
 (30 6 (:TYPE-PRESCRIPTION MOD-NEGATIVE . 2))
 (24 24 (:TYPE-PRESCRIPTION NOT-INTEGERP-4B))
 (24 24 (:TYPE-PRESCRIPTION NOT-INTEGERP-3B))
 (24 24 (:TYPE-PRESCRIPTION NOT-INTEGERP-2B))
 (24 24 (:TYPE-PRESCRIPTION NOT-INTEGERP-1B))
 (6 6 (:TYPE-PRESCRIPTION MOD-ZERO . 3))
 (6 6 (:TYPE-PRESCRIPTION MOD-POSITIVE . 1))
 (6 6 (:TYPE-PRESCRIPTION MOD-NONPOSITIVE))
 (6 6 (:TYPE-PRESCRIPTION MOD-NEGATIVE . 1))
 (6 6 (:TYPE-PRESCRIPTION INTEGERP-MOD-2))
 (2 2 (:TYPE-PRESCRIPTION |(< 0 (logior x y))| . 1))
 (2 2 (:TYPE-PRESCRIPTION |(< (logior x y) 0)| . 2))
 (2 2 (:TYPE-PRESCRIPTION |(< (logior x y) 0)| . 1))
 (2 2 (:REWRITE GL::SHAPE-SPEC-OBJ-IN-RANGE-BACKCHAIN-INTEGER-2))
 )
(MAIN-2
 (14640 12 (:LINEAR LOGIOR-BOUNDS-NEG . 1))
 (9182 1 (:REWRITE MOD-X-Y-=-X-Y . 1))
 (6522 6 (:REWRITE |(< x (if a b c))|))
 (5454 85 (:REWRITE CANCEL-MOD-+))
 (4798 4798 (:TYPE-PRESCRIPTION NOT-INTEGERP-3B))
 (4798 4798 (:TYPE-PRESCRIPTION NOT-INTEGERP-2B))
 (4798 4798 (:TYPE-PRESCRIPTION NOT-INTEGERP-1B))
 (4753 3 (:REWRITE |(equal (+ (- c) x) y)|))
 (4699 1 (:REWRITE MOD-X-Y-=-X+Y . 1))
 (4149 837 (:TYPE-PRESCRIPTION MOD-ZERO . 2))
 (4149 837 (:TYPE-PRESCRIPTION MOD-ZERO . 1))
 (4033 837 (:TYPE-PRESCRIPTION MOD-POSITIVE . 2))
 (4033 837 (:TYPE-PRESCRIPTION MOD-NEGATIVE . 2))
 (3392 85 (:REWRITE MOD-X-Y-=-X . 4))
 (3392 85 (:REWRITE MOD-X-Y-=-X . 3))
 (3244 85 (:REWRITE MOD-X-Y-=-X+Y . 2))
 (3083 85 (:REWRITE MOD-X-Y-=-X-Y . 2))
 (2741 421 (:REWRITE INTEGERP-MINUS-X))
 (2197 85 (:REWRITE MOD-ZERO . 4))
 (2141 85 (:REWRITE MOD-ZERO . 3))
 (2014 979 (:REWRITE DEFAULT-TIMES-1))
 (1756 189 (:REWRITE |(* (- x) y)|))
 (1746 1012 (:TYPE-PRESCRIPTION NOT-INTEGERP-4A))
 (1552 979 (:REWRITE DEFAULT-TIMES-2))
 (1056 12 (:LINEAR LOGIOR-BOUNDS-NEG . 2))
 (1012 1012 (:TYPE-PRESCRIPTION NOT-INTEGERP-3A))
 (1012 1012 (:TYPE-PRESCRIPTION NOT-INTEGERP-2A))
 (1012 1012 (:TYPE-PRESCRIPTION NOT-INTEGERP-1A))
 (1007 36 (:LINEAR MOD-BOUNDS-3))
 (996 170 (:REWRITE DEFAULT-MINUS))
 (966 340 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (966 340 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (937 346 (:REWRITE DEFAULT-LESS-THAN-2))
 (911 170 (:REWRITE |(- (* c x))|))
 (846 72 (:LINEAR MOD-BOUNDS-2))
 (837 837 (:TYPE-PRESCRIPTION MOD-ZERO . 3))
 (837 837 (:TYPE-PRESCRIPTION MOD-POSITIVE . 1))
 (837 837 (:TYPE-PRESCRIPTION MOD-NONPOSITIVE))
 (837 837 (:TYPE-PRESCRIPTION MOD-NEGATIVE . 1))
 (837 837 (:TYPE-PRESCRIPTION INTEGERP-MOD-2))
 (752 98 (:REWRITE RATIONALP-X))
 (571 85 (:REWRITE MOD-X-Y-=-X . 2))
 (571 85 (:REWRITE |(mod (+ x (mod a b)) y)|))
 (571 85 (:REWRITE |(mod (+ x (- (mod a b))) y)|))
 (555 346 (:REWRITE DEFAULT-LESS-THAN-1))
 (551 63 (:REWRITE ACL2-NUMBERP-X))
 (538 17 (:REWRITE DEFAULT-LOGIOR-2))
 (538 17 (:REWRITE DEFAULT-LOGIOR-1))
 (524 524 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (498 85 (:REWRITE MOD-X-Y-=-X-Y . 3))
 (498 85 (:REWRITE MOD-X-Y-=-X+Y . 3))
 (480 85 (:REWRITE MOD-CANCEL-*-CONST))
 (384 12 (:REWRITE MOD-POSITIVE . 3))
 (371 82 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (371 82 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (358 85 (:REWRITE MOD-CANCEL-*-REWRITING-GOAL-LITERAL))
 (358 85 (:REWRITE |(mod (* x (/ y)) z) rewriting-goal-literal|))
 (346 346 (:REWRITE THE-FLOOR-BELOW))
 (346 346 (:REWRITE THE-FLOOR-ABOVE))
 (340 340 (:REWRITE SIMPLIFY-SUMS-<))
 (340 340 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (340 340 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (340 340 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (340 340 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (340 340 (:REWRITE INTEGERP-<-CONSTANT))
 (340 340 (:REWRITE CONSTANT-<-INTEGERP))
 (340 340 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (340 340 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (340 340 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (340 340 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (340 340 (:REWRITE |(< c (- x))|))
 (340 340 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (340 340 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (340 340 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (340 340 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (340 340 (:REWRITE |(< (/ x) (/ y))|))
 (340 340 (:REWRITE |(< (- x) c)|))
 (340 340 (:REWRITE |(< (- x) (- y))|))
 (336 336 (:REWRITE REDUCE-INTEGERP-+))
 (336 336 (:META META-INTEGERP-CORRECT))
 (302 82 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (249 249 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (236 4 (:REWRITE MOD-NONNEGATIVE))
 (236 4 (:REWRITE MOD-NEGATIVE . 3))
 (225 85 (:REWRITE MOD-CANCEL-*-NOT-REWRITING-GOAL-LITERAL))
 (225 85 (:REWRITE |(mod (* x (/ y)) z) not rewriting-goal-literal|))
 (182 82 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 (165 165 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (165 165 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (165 165 (:REWRITE |(< (/ x) 0)|))
 (165 165 (:REWRITE |(< (* x y) 0)|))
 (135 135 (:TYPE-PRESCRIPTION |(< 0 (logior x y))| . 1))
 (135 135 (:TYPE-PRESCRIPTION |(< (logior x y) 0)| . 2))
 (135 135 (:TYPE-PRESCRIPTION |(< (logior x y) 0)| . 1))
 (111 3 (:REWRITE |(* (if a b c) x)|))
 (98 98 (:REWRITE RATIONALP-MINUS-X))
 (94 94 (:REWRITE DEFAULT-MOD-2))
 (92 92 (:REWRITE REDUCE-RATIONALP-+))
 (92 92 (:META META-RATIONALP-CORRECT))
 (91 91 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (91 91 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (91 91 (:REWRITE |(< 0 (/ x))|))
 (91 91 (:REWRITE |(< 0 (* x y))|))
 (85 85 (:REWRITE THIS-NEEDS-TO-BE-ADDED-TO-QUOTIENT-REMAINDER-LEMMAS))
 (85 85 (:REWRITE |(mod x (- y))| . 3))
 (85 85 (:REWRITE |(mod x (- y))| . 2))
 (85 85 (:REWRITE |(mod x (- y))| . 1))
 (85 85 (:REWRITE |(mod x (* y (/ z))) rewriting-goal-literal|))
 (85 85 (:REWRITE |(mod x (* y (/ z))) not rewriting-goal-literal|))
 (85 85 (:REWRITE |(mod (- x) y)| . 3))
 (85 85 (:REWRITE |(mod (- x) y)| . 2))
 (85 85 (:REWRITE |(mod (- x) y)| . 1))
 (83 83 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (83 83 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (82 82 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (82 82 (:REWRITE |(equal c (/ x))|))
 (82 82 (:REWRITE |(equal c (- x))|))
 (82 82 (:REWRITE |(equal (/ x) c)|))
 (82 82 (:REWRITE |(equal (/ x) (/ y))|))
 (82 82 (:REWRITE |(equal (- x) c)|))
 (82 82 (:REWRITE |(equal (- x) (- y))|))
 (79 79 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-=-0))
 (73 8 (:REWRITE DEFAULT-PLUS-2))
 (29 29 (:TYPE-PRESCRIPTION RATIONALP-MOD))
 (20 5 (:REWRITE INTEGERP-MOD-2))
 (20 5 (:REWRITE INTEGERP-MOD-1))
 (12 12 (:REWRITE MOD-POSITIVE . 2))
 (12 12 (:REWRITE MOD-POSITIVE . 1))
 (12 2 (:REWRITE |(+ y x)|))
 (10 8 (:REWRITE DEFAULT-PLUS-1))
 (6 6 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (6 6 (:REWRITE NORMALIZE-ADDENDS))
 (4 4 (:TYPE-PRESCRIPTION NATP))
 (4 4 (:REWRITE MOD-NEGATIVE . 2))
 (4 4 (:REWRITE MOD-NEGATIVE . 1))
 (2 1 (:REWRITE |(equal (mod (+ x y) z) x)|))
 )
(MAIN-3
 (130637 21 (:REWRITE FLOOR-=-X/Y . 4))
 (101165 13926 (:REWRITE DEFAULT-TIMES-1))
 (94530 12 (:REWRITE MOD-X-Y-=-X-Y . 1))
 (71727 13926 (:REWRITE DEFAULT-TIMES-2))
 (69420 12667 (:TYPE-PRESCRIPTION MOD-ZERO . 1))
 (68902 12693 (:TYPE-PRESCRIPTION MOD-POSITIVE . 2))
 (68902 12693 (:TYPE-PRESCRIPTION MOD-NEGATIVE . 2))
 (61663 239 (:REWRITE MOD-ZERO . 4))
 (55968 239 (:REWRITE MOD-X-Y-=-X . 3))
 (53120 384 (:REWRITE FLOOR-X-Y-=-1 . 2))
 (52674 239 (:REWRITE MOD-X-Y-=-X . 4))
 (49638 384 (:REWRITE FLOOR-ZERO . 3))
 (48744 239 (:REWRITE MOD-X-Y-=-X-Y . 2))
 (48389 35 (:REWRITE |(equal (+ (- c) x) y)|))
 (48343 48343 (:TYPE-PRESCRIPTION NOT-INTEGERP-3B))
 (48343 48343 (:TYPE-PRESCRIPTION NOT-INTEGERP-2B))
 (48343 48343 (:TYPE-PRESCRIPTION NOT-INTEGERP-1B))
 (47928 12 (:REWRITE MOD-X-Y-=-X+Y . 1))
 (47897 47897 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NONPOSITIVE-BASE-EVEN-EXPONENT))
 (47897 47897 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NEGATIVE-BASE-ODD-EXPONENT))
 (47897 47897 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NEGATIVE-BASE-EVEN-EXPONENT))
 (47897 47897 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-INTEGERP-BASE-B))
 (30581 387 (:REWRITE DEFAULT-FLOOR-RATIO))
 (30332 384 (:REWRITE FLOOR-ZERO . 4))
 (28837 239 (:REWRITE MOD-X-Y-=-X+Y . 2))
 (28836 239 (:REWRITE MOD-ZERO . 3))
 (26457 384 (:REWRITE FLOOR-ZERO . 5))
 (24672 12667 (:TYPE-PRESCRIPTION INTEGERP-MOD-2))
 (22850 425 (:REWRITE |(integerp (- x))|))
 (22806 1910 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (22799 1910 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (20088 386 (:REWRITE FLOOR-=-X/Y . 3))
 (16982 1913 (:REWRITE DEFAULT-LESS-THAN-1))
 (15685 384 (:REWRITE FLOOR-X-Y-=--1 . 2))
 (12693 12693 (:TYPE-PRESCRIPTION MOD-ZERO . 3))
 (12693 12693 (:TYPE-PRESCRIPTION MOD-POSITIVE . 1))
 (12693 12693 (:TYPE-PRESCRIPTION MOD-NEGATIVE . 1))
 (12667 12667 (:TYPE-PRESCRIPTION MOD-NONPOSITIVE))
 (12536 1817 (:REWRITE DEFAULT-PLUS-2))
 (11909 1937 (:REWRITE THE-FLOOR-ABOVE))
 (11491 72 (:LINEAR MOD-BOUNDS-3))
 (10882 243 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (10446 796 (:REWRITE DEFAULT-MINUS))
 (10077 1675 (:REWRITE INTEGERP-MINUS-X))
 (9720 1817 (:REWRITE DEFAULT-PLUS-1))
 (8231 378 (:REWRITE |(floor x 1)|))
 (8227 239 (:REWRITE MOD-X-Y-=-X . 2))
 (8227 239 (:REWRITE |(mod (+ x (mod a b)) y)|))
 (8227 239 (:REWRITE |(mod (+ x (- (mod a b))) y)|))
 (7858 142 (:LINEAR LINEAR-FLOOR-BOUNDS-2))
 (7733 1913 (:REWRITE DEFAULT-LESS-THAN-2))
 (6392 238 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (5457 238 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 (4377 239 (:REWRITE MOD-X-Y-=-X-Y . 3))
 (4377 239 (:REWRITE MOD-X-Y-=-X+Y . 3))
 (4313 238 (:REWRITE MOD-CANCEL-*-CONST))
 (3622 384 (:REWRITE FLOOR-ZERO . 2))
 (3622 384 (:REWRITE FLOOR-X-Y-=-1 . 3))
 (3622 384 (:REWRITE FLOOR-X-Y-=--1 . 3))
 (3602 387 (:REWRITE DEFAULT-FLOOR-1))
 (3566 382 (:REWRITE FLOOR-CANCEL-*-CONST))
 (3492 144 (:LINEAR MOD-BOUNDS-2))
 (3447 3303 (:TYPE-PRESCRIPTION FLOOR-ZERO . 2))
 (3447 3303 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 1))
 (3447 3303 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 1))
 (3447 3303 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 1))
 (3375 3303 (:TYPE-PRESCRIPTION FLOOR-ZERO . 3))
 (3375 3303 (:TYPE-PRESCRIPTION FLOOR-ZERO . 1))
 (3375 3303 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 3))
 (3375 3303 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 2))
 (3375 3303 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 3))
 (3375 3303 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 2))
 (3375 3303 (:TYPE-PRESCRIPTION FLOOR-NONNEGATIVE . 3))
 (3375 3303 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 3))
 (3375 3303 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 2))
 (3149 718 (:TYPE-PRESCRIPTION NOT-INTEGERP-4A))
 (2609 2465 (:TYPE-PRESCRIPTION FLOOR-NONNEGATIVE . 1))
 (2446 1937 (:REWRITE THE-FLOOR-BELOW))
 (2208 230 (:REWRITE MOD-CANCEL-*-NOT-REWRITING-GOAL-LITERAL))
 (2200 222 (:REWRITE |(mod (* x (/ y)) z) not rewriting-goal-literal|))
 (2058 374 (:REWRITE FLOOR-CANCEL-*-NOT-REWRITING-GOAL-LITERAL))
 (2058 374 (:REWRITE |(floor (* x (/ y)) z) not rewriting-goal-literal|))
 (1919 1913 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (1919 1913 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (1913 1913 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (1913 1913 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (1913 1913 (:REWRITE INTEGERP-<-CONSTANT))
 (1913 1913 (:REWRITE CONSTANT-<-INTEGERP))
 (1913 1913 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (1913 1913 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (1913 1913 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (1913 1913 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (1913 1913 (:REWRITE |(< c (- x))|))
 (1913 1913 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (1913 1913 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (1913 1913 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (1913 1913 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (1913 1913 (:REWRITE |(< (/ x) (/ y))|))
 (1913 1913 (:REWRITE |(< (- x) c)|))
 (1913 1913 (:REWRITE |(< (- x) (- y))|))
 (1893 222 (:REWRITE |(mod (* x (/ y)) z) rewriting-goal-literal|))
 (1890 38 (:REWRITE |(- (+ x y))|))
 (1637 374 (:REWRITE |(floor (* x (/ y)) z) rewriting-goal-literal|))
 (1576 1576 (:META META-INTEGERP-CORRECT))
 (1374 425 (:TYPE-PRESCRIPTION BUBBLE-DOWN))
 (1320 3 (:REWRITE |(equal (mod a n) (mod b n))|))
 (890 890 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (724 250 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (718 718 (:TYPE-PRESCRIPTION NOT-INTEGERP-3A))
 (718 718 (:TYPE-PRESCRIPTION NOT-INTEGERP-2A))
 (718 718 (:TYPE-PRESCRIPTION NOT-INTEGERP-1A))
 (696 696 (:REWRITE |(< (/ x) 0)|))
 (696 696 (:REWRITE |(< (* x y) 0)|))
 (693 693 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (693 693 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (580 580 (:REWRITE EXPT-WITH-VIOLATED-GUARDS))
 (541 541 (:REWRITE |(< (* x y) 0) rationalp (* x y)|))
 (404 404 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (404 404 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (404 404 (:REWRITE |(< 0 (/ x))|))
 (404 404 (:REWRITE |(< 0 (* x y))|))
 (387 387 (:REWRITE DEFAULT-FLOOR-2))
 (374 374 (:REWRITE |(floor x (- y))| . 2))
 (374 374 (:REWRITE |(floor x (- y))| . 1))
 (374 374 (:REWRITE |(floor x (* y (/ z))) rewriting-goal-literal|))
 (374 374 (:REWRITE |(floor x (* y (/ z))) not rewriting-goal-literal|))
 (374 374 (:REWRITE |(floor (- x) y)| . 2))
 (374 374 (:REWRITE |(floor (- x) y)| . 1))
 (346 346 (:REWRITE |(< 0 (* x y)) rationalp (* x y)|))
 (318 3 (:REWRITE MOD-ZERO . 1))
 (290 290 (:REWRITE DEFAULT-EXPT-2))
 (290 290 (:REWRITE DEFAULT-EXPT-1))
 (290 290 (:REWRITE |(expt 1/c n)|))
 (290 290 (:REWRITE |(expt (- x) n)|))
 (288 12 (:REWRITE |(equal (mod (+ x y) z) x)|))
 (259 244 (:REWRITE |(equal (/ x) c)|))
 (244 244 (:REWRITE DEFAULT-MOD-2))
 (244 244 (:REWRITE |(equal c (/ x))|))
 (244 244 (:REWRITE |(equal (/ x) (/ y))|))
 (244 244 (:REWRITE |(equal (- x) (- y))|))
 (243 243 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (243 243 (:REWRITE |(equal c (- x))|))
 (243 243 (:REWRITE |(equal (- x) c)|))
 (222 222 (:REWRITE THIS-NEEDS-TO-BE-ADDED-TO-QUOTIENT-REMAINDER-LEMMAS))
 (222 222 (:REWRITE |(mod x (- y))| . 3))
 (222 222 (:REWRITE |(mod x (- y))| . 2))
 (222 222 (:REWRITE |(mod x (- y))| . 1))
 (222 222 (:REWRITE |(mod x (* y (/ z))) rewriting-goal-literal|))
 (222 222 (:REWRITE |(mod x (* y (/ z))) not rewriting-goal-literal|))
 (222 222 (:REWRITE |(mod (- x) y)| . 3))
 (222 222 (:REWRITE |(mod (- x) y)| . 2))
 (222 222 (:REWRITE |(mod (- x) y)| . 1))
 (200 200 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-=-0))
 (168 168 (:TYPE-PRESCRIPTION COLLECT-*))
 (166 8 (:REWRITE FLOOR-POSITIVE . 3))
 (166 8 (:REWRITE FLOOR-POSITIVE . 2))
 (166 8 (:REWRITE FLOOR-NONPOSITIVE . 2))
 (166 8 (:REWRITE FLOOR-NONPOSITIVE . 1))
 (162 162 (:TYPE-PRESCRIPTION RATIONALP-MOD))
 (126 2 (:REWRITE |(floor (+ x r) i)|))
 (100 21 (:REWRITE |(equal (floor (+ x y) z) x)|))
 (87 8 (:REWRITE FLOOR-POSITIVE . 4))
 (87 8 (:REWRITE FLOOR-NONPOSITIVE . 3))
 (79 79 (:REWRITE INTEGERP-+-REDUCE-CONSTANT))
 (63 15 (:REWRITE RATIONALP-X))
 (57 3 (:REWRITE MOD-ZERO . 2))
 (44 44 (:REWRITE REDUCE-INTEGERP-+-CONSTANT))
 (44 22 (:REWRITE COLLECT-*-PROBLEM-FINDER))
 (38 38 (:REWRITE |(< (+ c/d x) y)|))
 (38 38 (:REWRITE |(< (+ (- c) x) y)|))
 (22 22 (:TYPE-PRESCRIPTION FMT-TO-COMMENT-WINDOW))
 (20 4 (:REWRITE ACL2-NUMBERP-X))
 (15 15 (:REWRITE RATIONALP-MINUS-X))
 (13 13 (:REWRITE REDUCE-RATIONALP-+))
 (13 13 (:META META-RATIONALP-CORRECT))
 (12 12 (:REWRITE FOLD-CONSTS-IN-+))
 (8 8 (:REWRITE INTEGERP-MOD-2))
 (8 8 (:REWRITE INTEGERP-MOD-1))
 (8 8 (:REWRITE FLOOR-ZERO . 1))
 (8 8 (:REWRITE FLOOR-POSITIVE . 1))
 (8 8 (:REWRITE |(mod (floor x y) z)| . 5))
 (8 8 (:REWRITE |(mod (floor x y) z)| . 4))
 (8 8 (:REWRITE |(mod (floor x y) z)| . 3))
 (8 8 (:REWRITE |(mod (floor x y) z)| . 2))
 (6 6 (:REWRITE |(< y (+ (- c) x))|))
 (6 6 (:REWRITE |(< x (+ c/d y))|))
 (1 1 (:REWRITE-QUOTED-CONSTANT IFIX-UNDER-INT-EQUIV))
 (1 1 (:REWRITE DEFAULT-DIVIDE))
 (1 1 (:REWRITE |(not (equal x (/ y)))|))
 (1 1 (:REWRITE |(equal x (/ y))|))
 (1 1 (:REWRITE |(/ (/ x))|))
 )
(MAIN-4
 (78090 84 (:LINEAR LINEAR-FLOOR-BOUNDS-1))
 (36805 26 (:REWRITE MOD-ZERO . 4))
 (26167 26 (:REWRITE MOD-X-Y-=-X . 3))
 (25699 26 (:REWRITE MOD-X-Y-=-X-Y . 2))
 (25529 26 (:REWRITE MOD-X-Y-=-X+Y . 2))
 (24851 26 (:REWRITE MOD-X-Y-=-X . 4))
 (21086 2881 (:REWRITE DEFAULT-TIMES-2))
 (19639 135 (:REWRITE CANCEL-FLOOR-+))
 (19210 2881 (:REWRITE DEFAULT-TIMES-1))
 (18672 128 (:REWRITE |(floor (* x (/ y)) z) not rewriting-goal-literal|))
 (17823 178 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (13777 199 (:REWRITE THE-FLOOR-ABOVE))
 (13116 13116 (:TYPE-PRESCRIPTION NOT-INTEGERP-3B))
 (13116 13116 (:TYPE-PRESCRIPTION NOT-INTEGERP-2B))
 (13116 13116 (:TYPE-PRESCRIPTION NOT-INTEGERP-1B))
 (10175 10175 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NONPOSITIVE-BASE-EVEN-EXPONENT))
 (10175 10175 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NEGATIVE-BASE-ODD-EXPONENT))
 (10175 10175 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NEGATIVE-BASE-EVEN-EXPONENT))
 (10175 10175 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-INTEGERP-BASE-B))
 (10068 135 (:REWRITE FLOOR-=-X/Y . 2))
 (9594 135 (:REWRITE DEFAULT-FLOOR-RATIO))
 (9340 371 (:REWRITE DEFAULT-PLUS-2))
 (8533 371 (:REWRITE DEFAULT-PLUS-1))
 (7122 135 (:REWRITE FLOOR-X-Y-=-1 . 2))
 (7008 135 (:REWRITE FLOOR-ZERO . 3))
 (6999 6999 (:TYPE-PRESCRIPTION INTEGERP-/-EXPT-1))
 (6672 1288 (:TYPE-PRESCRIPTION FLOOR-ZERO . 2))
 (6672 1288 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 1))
 (6672 1288 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 1))
 (6672 1288 (:TYPE-PRESCRIPTION FLOOR-NONNEGATIVE . 1))
 (6672 1288 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 1))
 (5753 26 (:REWRITE MOD-ZERO . 3))
 (5211 135 (:REWRITE |(integerp (- x))|))
 (4597 20 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (4584 135 (:REWRITE FLOOR-ZERO . 4))
 (4538 469 (:REWRITE DEFAULT-MINUS))
 (4351 135 (:REWRITE FLOOR-ZERO . 5))
 (4330 26 (:REWRITE DEFAULT-MOD-RATIO))
 (3980 1288 (:TYPE-PRESCRIPTION FLOOR-ZERO . 3))
 (3980 1288 (:TYPE-PRESCRIPTION FLOOR-ZERO . 1))
 (3980 1288 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 3))
 (3980 1288 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 2))
 (3980 1288 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 3))
 (3980 1288 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 2))
 (3980 1288 (:TYPE-PRESCRIPTION FLOOR-NONNEGATIVE . 3))
 (3980 1288 (:TYPE-PRESCRIPTION FLOOR-NONNEGATIVE . 2))
 (3980 1288 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 3))
 (3980 1288 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 2))
 (3883 178 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (3840 135 (:REWRITE FLOOR-=-X/Y . 3))
 (3784 135 (:REWRITE FLOOR-X-Y-=--1 . 2))
 (2522 178 (:REWRITE DEFAULT-LESS-THAN-1))
 (2175 135 (:REWRITE FLOOR-ZERO . 2))
 (2175 135 (:REWRITE FLOOR-X-Y-=-1 . 3))
 (2175 135 (:REWRITE FLOOR-X-Y-=--1 . 3))
 (2104 2 (:REWRITE |(* x (+ y z))|))
 (2014 151 (:TYPE-PRESCRIPTION BUBBLE-DOWN))
 (1760 176 (:REWRITE DEFAULT-DIVIDE))
 (1756 26 (:REWRITE |(mod (+ x (mod a b)) y)|))
 (1756 26 (:REWRITE |(mod (+ x (- (mod a b))) y)|))
 (1738 26 (:REWRITE MOD-X-Y-=-X . 2))
 (1721 135 (:REWRITE FLOOR-CANCEL-*-CONST))
 (1539 178 (:REWRITE DEFAULT-LESS-THAN-2))
 (1429 241 (:TYPE-PRESCRIPTION MOD-ZERO . 1))
 (1429 241 (:TYPE-PRESCRIPTION MOD-POSITIVE . 2))
 (1429 241 (:TYPE-PRESCRIPTION MOD-NEGATIVE . 2))
 (1421 133 (:REWRITE FLOOR-CANCEL-*-NOT-REWRITING-GOAL-LITERAL))
 (1379 174 (:REWRITE SIMPLIFY-SUMS-<))
 (1274 199 (:REWRITE THE-FLOOR-BELOW))
 (1169 241 (:TYPE-PRESCRIPTION MOD-ZERO . 2))
 (1168 82 (:REWRITE |(floor x 1)|))
 (1063 135 (:REWRITE DEFAULT-FLOOR-1))
 (950 26 (:REWRITE MOD-X-Y-=-X-Y . 3))
 (950 26 (:REWRITE MOD-X-Y-=-X+Y . 3))
 (942 42 (:LINEAR LINEAR-FLOOR-BOUNDS-3))
 (918 20 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (814 26 (:REWRITE DEFAULT-MOD-1))
 (696 132 (:REWRITE |(floor x (* y (/ z))) not rewriting-goal-literal|))
 (562 562 (:REWRITE EXPT-WITH-VIOLATED-GUARDS))
 (545 19 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 (540 135 (:REWRITE DEFAULT-FLOOR-2))
 (532 532 (:TYPE-PRESCRIPTION NOT-INTEGERP-3B-EXPT))
 (532 532 (:TYPE-PRESCRIPTION NOT-INTEGERP-2B-EXPT))
 (532 532 (:TYPE-PRESCRIPTION NOT-INTEGERP-1B-EXPT))
 (509 25 (:REWRITE MOD-CANCEL-*-CONST))
 (508 178 (:REWRITE |(< (- x) c)|))
 (508 178 (:REWRITE |(< (- x) (- y))|))
 (499 239 (:TYPE-PRESCRIPTION INTEGERP-MOD-2))
 (492 42 (:LINEAR LINEAR-FLOOR-BOUNDS-2))
 (486 6 (:LINEAR MOD-BOUNDS-3))
 (453 453 (:REWRITE DEFAULT-EXPT-2))
 (453 453 (:REWRITE DEFAULT-EXPT-1))
 (453 453 (:REWRITE |(expt (- x) n)|))
 (312 24 (:REWRITE |(* (expt x m) (expt x n))|))
 (288 178 (:REWRITE |(< c (- x))|))
 (281 19 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (254 132 (:REWRITE |(floor x (* y (/ z))) rewriting-goal-literal|))
 (241 241 (:TYPE-PRESCRIPTION MOD-ZERO . 3))
 (241 241 (:TYPE-PRESCRIPTION MOD-POSITIVE . 1))
 (241 241 (:TYPE-PRESCRIPTION MOD-NONPOSITIVE))
 (241 241 (:TYPE-PRESCRIPTION MOD-NEGATIVE . 1))
 (229 229 (:REWRITE REDUCE-INTEGERP-+))
 (229 229 (:META META-INTEGERP-CORRECT))
 (222 12 (:LINEAR MOD-BOUNDS-2))
 (218 13 (:LINEAR EXPT->=-1-ONE))
 (208 8 (:REWRITE FLOOR-=-X/Y . 4))
 (194 26 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (179 178 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (179 178 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (178 178 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (178 178 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (178 178 (:REWRITE INTEGERP-<-CONSTANT))
 (178 178 (:REWRITE CONSTANT-<-INTEGERP))
 (178 178 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (178 178 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (178 178 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (178 178 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (178 178 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (178 178 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (178 178 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (178 178 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (178 178 (:REWRITE |(< (/ x) (/ y))|))
 (176 16 (:REWRITE |(- (+ x y))|))
 (176 13 (:LINEAR EXPT-LINEAR-LOWER-<=))
 (162 162 (:TYPE-PRESCRIPTION NOT-INTEGERP-3A))
 (162 162 (:TYPE-PRESCRIPTION NOT-INTEGERP-2A))
 (162 162 (:TYPE-PRESCRIPTION NOT-INTEGERP-1A))
 (160 7 (:REWRITE FLOOR-POSITIVE . 3))
 (157 7 (:REWRITE FLOOR-POSITIVE . 2))
 (157 7 (:REWRITE FLOOR-NONPOSITIVE . 1))
 (151 7 (:REWRITE FLOOR-NONPOSITIVE . 2))
 (140 140 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (132 132 (:REWRITE |(floor x (- y))| . 2))
 (132 132 (:REWRITE |(floor x (- y))| . 1))
 (132 132 (:REWRITE |(floor (- x) y)| . 2))
 (132 132 (:REWRITE |(floor (- x) y)| . 1))
 (131 26 (:LINEAR EXPT-IS-WEAKLY-INCREASING-FOR-BASE->-1))
 (130 20 (:REWRITE |(equal (- x) c)|))
 (130 20 (:REWRITE |(equal (- x) (- y))|))
 (125 125 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (109 13 (:LINEAR EXPT-X->-X))
 (109 13 (:LINEAR EXPT->-1-ONE))
 (98 8 (:REWRITE |(equal (floor (+ x y) z) x)|))
 (91 7 (:REWRITE FLOOR-POSITIVE . 4))
 (91 7 (:REWRITE FLOOR-NONPOSITIVE . 3))
 (90 90 (:REWRITE |(< (/ x) 0)|))
 (90 90 (:REWRITE |(< (* x y) 0)|))
 (88 88 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (88 88 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (73 13 (:LINEAR EXPT-X->=-X))
 (71 71 (:REWRITE |(< (* x y) 0) rationalp (* x y)|))
 (69 15 (:REWRITE |(mod (* x (/ y)) z) rewriting-goal-literal|))
 (68 2 (:REWRITE |(mod x 1)|))
 (47 23 (:REWRITE MOD-CANCEL-*-NOT-REWRITING-GOAL-LITERAL))
 (45 15 (:REWRITE |(mod x (* y (/ z))) rewriting-goal-literal|))
 (44 26 (:REWRITE DEFAULT-MOD-2))
 (42 42 (:TYPE-PRESCRIPTION COLLECT-*))
 (39 15 (:REWRITE |(mod (* x (/ y)) z) not rewriting-goal-literal|))
 (35 35 (:REWRITE |(< 0 (/ x))|))
 (35 35 (:REWRITE |(< 0 (* x y))|))
 (34 34 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (34 34 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (33 15 (:REWRITE THIS-NEEDS-TO-BE-ADDED-TO-QUOTIENT-REMAINDER-LEMMAS))
 (26 26 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (26 26 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (20 20 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (20 20 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (20 20 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (20 20 (:REWRITE |(equal c (/ x))|))
 (20 20 (:REWRITE |(equal c (- x))|))
 (20 20 (:REWRITE |(equal (/ x) c)|))
 (20 20 (:REWRITE |(equal (/ x) (/ y))|))
 (18 18 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-=-0))
 (18 18 (:REWRITE |(< 0 (* x y)) rationalp (* x y)|))
 (15 15 (:REWRITE |(mod x (- y))| . 3))
 (15 15 (:REWRITE |(mod x (- y))| . 2))
 (15 15 (:REWRITE |(mod x (- y))| . 1))
 (15 15 (:REWRITE |(mod x (* y (/ z))) not rewriting-goal-literal|))
 (15 15 (:REWRITE |(mod (- x) y)| . 3))
 (15 15 (:REWRITE |(mod (- x) y)| . 2))
 (15 15 (:REWRITE |(mod (- x) y)| . 1))
 (13 13 (:LINEAR EXPT-LINEAR-UPPER-<=))
 (13 13 (:LINEAR EXPT-LINEAR-UPPER-<))
 (13 13 (:LINEAR EXPT-LINEAR-LOWER-<))
 (13 13 (:LINEAR EXPT->=-1-TWO))
 (13 13 (:LINEAR EXPT->-1-TWO))
 (13 13 (:LINEAR EXPT-<=-1-TWO))
 (13 13 (:LINEAR EXPT-<=-1-ONE))
 (13 13 (:LINEAR EXPT-<-1-TWO))
 (13 13 (:LINEAR EXPT-<-1-ONE))
 (12 6 (:REWRITE COLLECT-*-PROBLEM-FINDER))
 (9 1 (:REWRITE MOD-POSITIVE . 3))
 (8 8 (:REWRITE |(mod (floor x y) z)| . 5))
 (8 8 (:REWRITE |(mod (floor x y) z)| . 4))
 (8 8 (:REWRITE |(mod (floor x y) z)| . 3))
 (8 8 (:REWRITE |(mod (floor x y) z)| . 2))
 (8 8 (:REWRITE |(equal (* x y) 0)|))
 (8 6 (:REWRITE ODD-EXPT-THM))
 (7 7 (:REWRITE FLOOR-ZERO . 1))
 (7 7 (:REWRITE FLOOR-POSITIVE . 1))
 (7 7 (:REWRITE BUBBLE-DOWN-*-MATCH-3))
 (7 7 (:REWRITE |(* c (* d x))|))
 (6 6 (:TYPE-PRESCRIPTION FMT-TO-COMMENT-WINDOW))
 (5 1 (:REWRITE MOD-NONPOSITIVE))
 (3 3 (:REWRITE |(< (+ c/d x) y)|))
 (3 3 (:REWRITE |(< (+ (- c) x) y)|))
 (2 2 (:TYPE-PRESCRIPTION INTEGERP-MOD-3))
 (2 2 (:TYPE-PRESCRIPTION ABS))
 (2 2 (:REWRITE |(< y (+ (- c) x))|))
 (2 2 (:REWRITE |(< x (+ c/d y))|))
 (1 1 (:REWRITE REDUCE-INTEGERP-+-CONSTANT))
 (1 1 (:REWRITE MOD-POSITIVE . 2))
 (1 1 (:REWRITE MOD-POSITIVE . 1))
 (1 1 (:REWRITE INTEGERP-+-REDUCE-CONSTANT))
 (1 1 (:REWRITE |(equal (+ (- c) x) y)|))
 )
(MAIN-5
 (78090 84 (:LINEAR LINEAR-FLOOR-BOUNDS-1))
 (36805 26 (:REWRITE MOD-ZERO . 4))
 (26167 26 (:REWRITE MOD-X-Y-=-X . 3))
 (25699 26 (:REWRITE MOD-X-Y-=-X-Y . 2))
 (25529 26 (:REWRITE MOD-X-Y-=-X+Y . 2))
 (24851 26 (:REWRITE MOD-X-Y-=-X . 4))
 (21086 2881 (:REWRITE DEFAULT-TIMES-2))
 (19639 135 (:REWRITE CANCEL-FLOOR-+))
 (19210 2881 (:REWRITE DEFAULT-TIMES-1))
 (18672 128 (:REWRITE |(floor (* x (/ y)) z) not rewriting-goal-literal|))
 (17823 178 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (13777 199 (:REWRITE THE-FLOOR-ABOVE))
 (13116 13116 (:TYPE-PRESCRIPTION NOT-INTEGERP-3B))
 (13116 13116 (:TYPE-PRESCRIPTION NOT-INTEGERP-2B))
 (13116 13116 (:TYPE-PRESCRIPTION NOT-INTEGERP-1B))
 (10175 10175 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NONPOSITIVE-BASE-EVEN-EXPONENT))
 (10175 10175 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NEGATIVE-BASE-ODD-EXPONENT))
 (10175 10175 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-NEGATIVE-BASE-EVEN-EXPONENT))
 (10175 10175 (:TYPE-PRESCRIPTION EXPT-TYPE-PRESCRIPTION-INTEGERP-BASE-B))
 (10068 135 (:REWRITE FLOOR-=-X/Y . 2))
 (9594 135 (:REWRITE DEFAULT-FLOOR-RATIO))
 (9340 371 (:REWRITE DEFAULT-PLUS-2))
 (8533 371 (:REWRITE DEFAULT-PLUS-1))
 (7122 135 (:REWRITE FLOOR-X-Y-=-1 . 2))
 (7008 135 (:REWRITE FLOOR-ZERO . 3))
 (6999 6999 (:TYPE-PRESCRIPTION INTEGERP-/-EXPT-1))
 (6672 1288 (:TYPE-PRESCRIPTION FLOOR-ZERO . 2))
 (6672 1288 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 1))
 (6672 1288 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 1))
 (6672 1288 (:TYPE-PRESCRIPTION FLOOR-NONNEGATIVE . 1))
 (6672 1288 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 1))
 (5753 26 (:REWRITE MOD-ZERO . 3))
 (5211 135 (:REWRITE |(integerp (- x))|))
 (4597 20 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (4584 135 (:REWRITE FLOOR-ZERO . 4))
 (4538 469 (:REWRITE DEFAULT-MINUS))
 (4351 135 (:REWRITE FLOOR-ZERO . 5))
 (4330 26 (:REWRITE DEFAULT-MOD-RATIO))
 (3980 1288 (:TYPE-PRESCRIPTION FLOOR-ZERO . 3))
 (3980 1288 (:TYPE-PRESCRIPTION FLOOR-ZERO . 1))
 (3980 1288 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 3))
 (3980 1288 (:TYPE-PRESCRIPTION FLOOR-POSITIVE . 2))
 (3980 1288 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 3))
 (3980 1288 (:TYPE-PRESCRIPTION FLOOR-NONPOSITIVE . 2))
 (3980 1288 (:TYPE-PRESCRIPTION FLOOR-NONNEGATIVE . 3))
 (3980 1288 (:TYPE-PRESCRIPTION FLOOR-NONNEGATIVE . 2))
 (3980 1288 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 3))
 (3980 1288 (:TYPE-PRESCRIPTION FLOOR-NEGATIVE . 2))
 (3883 178 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (3840 135 (:REWRITE FLOOR-=-X/Y . 3))
 (3784 135 (:REWRITE FLOOR-X-Y-=--1 . 2))
 (2522 178 (:REWRITE DEFAULT-LESS-THAN-1))
 (2175 135 (:REWRITE FLOOR-ZERO . 2))
 (2175 135 (:REWRITE FLOOR-X-Y-=-1 . 3))
 (2175 135 (:REWRITE FLOOR-X-Y-=--1 . 3))
 (2104 2 (:REWRITE |(* x (+ y z))|))
 (2014 151 (:TYPE-PRESCRIPTION BUBBLE-DOWN))
 (1760 176 (:REWRITE DEFAULT-DIVIDE))
 (1756 26 (:REWRITE |(mod (+ x (mod a b)) y)|))
 (1756 26 (:REWRITE |(mod (+ x (- (mod a b))) y)|))
 (1738 26 (:REWRITE MOD-X-Y-=-X . 2))
 (1721 135 (:REWRITE FLOOR-CANCEL-*-CONST))
 (1539 178 (:REWRITE DEFAULT-LESS-THAN-2))
 (1429 241 (:TYPE-PRESCRIPTION MOD-ZERO . 1))
 (1429 241 (:TYPE-PRESCRIPTION MOD-POSITIVE . 2))
 (1429 241 (:TYPE-PRESCRIPTION MOD-NEGATIVE . 2))
 (1421 133 (:REWRITE FLOOR-CANCEL-*-NOT-REWRITING-GOAL-LITERAL))
 (1379 174 (:REWRITE SIMPLIFY-SUMS-<))
 (1274 199 (:REWRITE THE-FLOOR-BELOW))
 (1169 241 (:TYPE-PRESCRIPTION MOD-ZERO . 2))
 (1168 82 (:REWRITE |(floor x 1)|))
 (1063 135 (:REWRITE DEFAULT-FLOOR-1))
 (950 26 (:REWRITE MOD-X-Y-=-X-Y . 3))
 (950 26 (:REWRITE MOD-X-Y-=-X+Y . 3))
 (942 42 (:LINEAR LINEAR-FLOOR-BOUNDS-3))
 (918 20 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (814 26 (:REWRITE DEFAULT-MOD-1))
 (696 132 (:REWRITE |(floor x (* y (/ z))) not rewriting-goal-literal|))
 (562 562 (:REWRITE EXPT-WITH-VIOLATED-GUARDS))
 (545 19 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 (540 135 (:REWRITE DEFAULT-FLOOR-2))
 (532 532 (:TYPE-PRESCRIPTION NOT-INTEGERP-3B-EXPT))
 (532 532 (:TYPE-PRESCRIPTION NOT-INTEGERP-2B-EXPT))
 (532 532 (:TYPE-PRESCRIPTION NOT-INTEGERP-1B-EXPT))
 (509 25 (:REWRITE MOD-CANCEL-*-CONST))
 (508 178 (:REWRITE |(< (- x) c)|))
 (508 178 (:REWRITE |(< (- x) (- y))|))
 (499 239 (:TYPE-PRESCRIPTION INTEGERP-MOD-2))
 (492 42 (:LINEAR LINEAR-FLOOR-BOUNDS-2))
 (486 6 (:LINEAR MOD-BOUNDS-3))
 (453 453 (:REWRITE DEFAULT-EXPT-2))
 (453 453 (:REWRITE DEFAULT-EXPT-1))
 (453 453 (:REWRITE |(expt (- x) n)|))
 (312 24 (:REWRITE |(* (expt x m) (expt x n))|))
 (288 178 (:REWRITE |(< c (- x))|))
 (281 19 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (254 132 (:REWRITE |(floor x (* y (/ z))) rewriting-goal-literal|))
 (241 241 (:TYPE-PRESCRIPTION MOD-ZERO . 3))
 (241 241 (:TYPE-PRESCRIPTION MOD-POSITIVE . 1))
 (241 241 (:TYPE-PRESCRIPTION MOD-NONPOSITIVE))
 (241 241 (:TYPE-PRESCRIPTION MOD-NEGATIVE . 1))
 (229 229 (:REWRITE REDUCE-INTEGERP-+))
 (229 229 (:META META-INTEGERP-CORRECT))
 (222 12 (:LINEAR MOD-BOUNDS-2))
 (218 13 (:LINEAR EXPT->=-1-ONE))
 (208 8 (:REWRITE FLOOR-=-X/Y . 4))
 (194 26 (:LINEAR EXPT-IS-INCREASING-FOR-BASE->-1))
 (179 178 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (179 178 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (178 178 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (178 178 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (178 178 (:REWRITE INTEGERP-<-CONSTANT))
 (178 178 (:REWRITE CONSTANT-<-INTEGERP))
 (178 178 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (178 178 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (178 178 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (178 178 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (178 178 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (178 178 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (178 178 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (178 178 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (178 178 (:REWRITE |(< (/ x) (/ y))|))
 (176 16 (:REWRITE |(- (+ x y))|))
 (176 13 (:LINEAR EXPT-LINEAR-LOWER-<=))
 (162 162 (:TYPE-PRESCRIPTION NOT-INTEGERP-3A))
 (162 162 (:TYPE-PRESCRIPTION NOT-INTEGERP-2A))
 (162 162 (:TYPE-PRESCRIPTION NOT-INTEGERP-1A))
 (160 7 (:REWRITE FLOOR-POSITIVE . 3))
 (157 7 (:REWRITE FLOOR-POSITIVE . 2))
 (157 7 (:REWRITE FLOOR-NONPOSITIVE . 1))
 (151 7 (:REWRITE FLOOR-NONPOSITIVE . 2))
 (140 140 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (132 132 (:REWRITE |(floor x (- y))| . 2))
 (132 132 (:REWRITE |(floor x (- y))| . 1))
 (132 132 (:REWRITE |(floor (- x) y)| . 2))
 (132 132 (:REWRITE |(floor (- x) y)| . 1))
 (131 26 (:LINEAR EXPT-IS-WEAKLY-INCREASING-FOR-BASE->-1))
 (130 20 (:REWRITE |(equal (- x) c)|))
 (130 20 (:REWRITE |(equal (- x) (- y))|))
 (125 125 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (109 13 (:LINEAR EXPT-X->-X))
 (109 13 (:LINEAR EXPT->-1-ONE))
 (98 8 (:REWRITE |(equal (floor (+ x y) z) x)|))
 (91 7 (:REWRITE FLOOR-POSITIVE . 4))
 (91 7 (:REWRITE FLOOR-NONPOSITIVE . 3))
 (90 90 (:REWRITE |(< (/ x) 0)|))
 (90 90 (:REWRITE |(< (* x y) 0)|))
 (88 88 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (88 88 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (73 13 (:LINEAR EXPT-X->=-X))
 (71 71 (:REWRITE |(< (* x y) 0) rationalp (* x y)|))
 (69 15 (:REWRITE |(mod (* x (/ y)) z) rewriting-goal-literal|))
 (68 2 (:REWRITE |(mod x 1)|))
 (47 23 (:REWRITE MOD-CANCEL-*-NOT-REWRITING-GOAL-LITERAL))
 (45 15 (:REWRITE |(mod x (* y (/ z))) rewriting-goal-literal|))
 (44 26 (:REWRITE DEFAULT-MOD-2))
 (42 42 (:TYPE-PRESCRIPTION COLLECT-*))
 (39 15 (:REWRITE |(mod (* x (/ y)) z) not rewriting-goal-literal|))
 (35 35 (:REWRITE |(< 0 (/ x))|))
 (35 35 (:REWRITE |(< 0 (* x y))|))
 (34 34 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (34 34 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (33 15 (:REWRITE THIS-NEEDS-TO-BE-ADDED-TO-QUOTIENT-REMAINDER-LEMMAS))
 (26 26 (:LINEAR EXPT-IS-WEAKLY-DECREASING-FOR-POS-BASE-<-1))
 (26 26 (:LINEAR EXPT-IS-DECREASING-FOR-POS-BASE-<-1))
 (20 20 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (20 20 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (20 20 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (20 20 (:REWRITE |(equal c (/ x))|))
 (20 20 (:REWRITE |(equal c (- x))|))
 (20 20 (:REWRITE |(equal (/ x) c)|))
 (20 20 (:REWRITE |(equal (/ x) (/ y))|))
 (18 18 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-=-0))
 (18 18 (:REWRITE |(< 0 (* x y)) rationalp (* x y)|))
 (15 15 (:REWRITE |(mod x (- y))| . 3))
 (15 15 (:REWRITE |(mod x (- y))| . 2))
 (15 15 (:REWRITE |(mod x (- y))| . 1))
 (15 15 (:REWRITE |(mod x (* y (/ z))) not rewriting-goal-literal|))
 (15 15 (:REWRITE |(mod (- x) y)| . 3))
 (15 15 (:REWRITE |(mod (- x) y)| . 2))
 (15 15 (:REWRITE |(mod (- x) y)| . 1))
 (13 13 (:LINEAR EXPT-LINEAR-UPPER-<=))
 (13 13 (:LINEAR EXPT-LINEAR-UPPER-<))
 (13 13 (:LINEAR EXPT-LINEAR-LOWER-<))
 (13 13 (:LINEAR EXPT->=-1-TWO))
 (13 13 (:LINEAR EXPT->-1-TWO))
 (13 13 (:LINEAR EXPT-<=-1-TWO))
 (13 13 (:LINEAR EXPT-<=-1-ONE))
 (13 13 (:LINEAR EXPT-<-1-TWO))
 (13 13 (:LINEAR EXPT-<-1-ONE))
 (12 6 (:REWRITE COLLECT-*-PROBLEM-FINDER))
 (9 1 (:REWRITE MOD-POSITIVE . 3))
 (8 8 (:REWRITE |(mod (floor x y) z)| . 5))
 (8 8 (:REWRITE |(mod (floor x y) z)| . 4))
 (8 8 (:REWRITE |(mod (floor x y) z)| . 3))
 (8 8 (:REWRITE |(mod (floor x y) z)| . 2))
 (8 8 (:REWRITE |(equal (* x y) 0)|))
 (8 6 (:REWRITE ODD-EXPT-THM))
 (7 7 (:REWRITE FLOOR-ZERO . 1))
 (7 7 (:REWRITE FLOOR-POSITIVE . 1))
 (7 7 (:REWRITE BUBBLE-DOWN-*-MATCH-3))
 (7 7 (:REWRITE |(* c (* d x))|))
 (6 6 (:TYPE-PRESCRIPTION FMT-TO-COMMENT-WINDOW))
 (5 1 (:REWRITE MOD-NONPOSITIVE))
 (3 3 (:REWRITE |(< (+ c/d x) y)|))
 (3 3 (:REWRITE |(< (+ (- c) x) y)|))
 (2 2 (:TYPE-PRESCRIPTION INTEGERP-MOD-3))
 (2 2 (:TYPE-PRESCRIPTION ABS))
 (2 2 (:REWRITE |(< y (+ (- c) x))|))
 (2 2 (:REWRITE |(< x (+ c/d y))|))
 (1 1 (:REWRITE REDUCE-INTEGERP-+-CONSTANT))
 (1 1 (:REWRITE MOD-POSITIVE . 2))
 (1 1 (:REWRITE MOD-POSITIVE . 1))
 (1 1 (:REWRITE INTEGERP-+-REDUCE-CONSTANT))
 (1 1 (:REWRITE |(equal (+ (- c) x) y)|))
 )
(MAIN
 (12292 10 (:LINEAR LOGIOR-BOUNDS-NEG . 1))
 (9182 1 (:REWRITE MOD-X-Y-=-X-Y . 1))
 (6522 6 (:REWRITE |(< x (if a b c))|))
 (4753 3 (:REWRITE |(equal (+ (- c) x) y)|))
 (4699 1 (:REWRITE MOD-X-Y-=-X+Y . 1))
 (3523 815 (:TYPE-PRESCRIPTION MOD-ZERO . 2))
 (3523 815 (:TYPE-PRESCRIPTION MOD-ZERO . 1))
 (3466 3466 (:TYPE-PRESCRIPTION NOT-INTEGERP-3B))
 (3466 3466 (:TYPE-PRESCRIPTION NOT-INTEGERP-2B))
 (3466 3466 (:TYPE-PRESCRIPTION NOT-INTEGERP-1B))
 (3463 815 (:TYPE-PRESCRIPTION MOD-POSITIVE . 2))
 (3463 815 (:TYPE-PRESCRIPTION MOD-NEGATIVE . 2))
 (2614 40 (:REWRITE CANCEL-MOD-+))
 (1699 40 (:REWRITE MOD-X-Y-=-X . 4))
 (1699 40 (:REWRITE MOD-X-Y-=-X . 3))
 (1623 40 (:REWRITE MOD-X-Y-=-X+Y . 2))
 (1544 40 (:REWRITE MOD-X-Y-=-X-Y . 2))
 (1271 161 (:REWRITE INTEGERP-MINUS-X))
 (1112 40 (:REWRITE MOD-ZERO . 4))
 (1070 40 (:REWRITE MOD-ZERO . 3))
 (880 10 (:LINEAR LOGIOR-BOUNDS-NEG . 2))
 (847 95 (:REWRITE |(* (- x) y)|))
 (824 427 (:TYPE-PRESCRIPTION NOT-INTEGERP-4A))
 (815 815 (:TYPE-PRESCRIPTION MOD-ZERO . 3))
 (815 815 (:TYPE-PRESCRIPTION MOD-POSITIVE . 1))
 (815 815 (:TYPE-PRESCRIPTION MOD-NONPOSITIVE))
 (815 815 (:TYPE-PRESCRIPTION MOD-NEGATIVE . 1))
 (815 815 (:TYPE-PRESCRIPTION INTEGERP-MOD-2))
 (759 445 (:REWRITE DEFAULT-TIMES-2))
 (681 180 (:REWRITE DEFAULT-LESS-THAN-2))
 (660 22 (:REWRITE DEFAULT-LOGIOR-2))
 (660 22 (:REWRITE DEFAULT-LOGIOR-1))
 (629 445 (:REWRITE DEFAULT-TIMES-1))
 (613 174 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-<))
 (613 174 (:REWRITE PREFER-POSITIVE-ADDENDS-<))
 (476 80 (:REWRITE DEFAULT-MINUS))
 (436 80 (:REWRITE |(- (* c x))|))
 (432 16 (:LINEAR MOD-BOUNDS-3))
 (427 427 (:TYPE-PRESCRIPTION NOT-INTEGERP-3A))
 (427 427 (:TYPE-PRESCRIPTION NOT-INTEGERP-2A))
 (427 427 (:TYPE-PRESCRIPTION NOT-INTEGERP-1A))
 (320 10 (:REWRITE MOD-POSITIVE . 3))
 (299 42 (:REWRITE SIMPLIFY-PRODUCTS-GATHER-EXPONENTS-EQUAL))
 (299 42 (:REWRITE PREFER-POSITIVE-ADDENDS-EQUAL))
 (292 180 (:REWRITE DEFAULT-LESS-THAN-1))
 (276 40 (:REWRITE MOD-X-Y-=-X . 2))
 (276 40 (:REWRITE |(mod (+ x (mod a b)) y)|))
 (276 40 (:REWRITE |(mod (+ x (- (mod a b))) y)|))
 (262 42 (:REWRITE SIMPLIFY-SUMS-EQUAL))
 (248 248 (:REWRITE NORMALIZE-FACTORS-GATHER-EXPONENTS))
 (238 40 (:REWRITE MOD-X-Y-=-X-Y . 3))
 (238 40 (:REWRITE MOD-X-Y-=-X+Y . 3))
 (238 40 (:REWRITE MOD-CANCEL-*-CONST))
 (192 32 (:LINEAR MOD-BOUNDS-2))
 (180 180 (:REWRITE THE-FLOOR-BELOW))
 (180 180 (:REWRITE THE-FLOOR-ABOVE))
 (174 174 (:REWRITE SIMPLIFY-SUMS-<))
 (174 174 (:REWRITE REMOVE-STRICT-INEQUALITIES))
 (174 174 (:REWRITE REDUCE-RATIONAL-MULTIPLICATIVE-CONSTANT-<))
 (174 174 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-<))
 (174 174 (:REWRITE REDUCE-ADDITIVE-CONSTANT-<))
 (174 174 (:REWRITE INTEGERP-<-CONSTANT))
 (174 174 (:REWRITE CONSTANT-<-INTEGERP))
 (174 174 (:REWRITE |(< c (/ x)) positive c --- present in goal|))
 (174 174 (:REWRITE |(< c (/ x)) positive c --- obj t or nil|))
 (174 174 (:REWRITE |(< c (/ x)) negative c --- present in goal|))
 (174 174 (:REWRITE |(< c (/ x)) negative c --- obj t or nil|))
 (174 174 (:REWRITE |(< c (- x))|))
 (174 174 (:REWRITE |(< (/ x) c) positive c --- present in goal|))
 (174 174 (:REWRITE |(< (/ x) c) positive c --- obj t or nil|))
 (174 174 (:REWRITE |(< (/ x) c) negative c --- present in goal|))
 (174 174 (:REWRITE |(< (/ x) c) negative c --- obj t or nil|))
 (174 174 (:REWRITE |(< (/ x) (/ y))|))
 (174 174 (:REWRITE |(< (- x) c)|))
 (174 174 (:REWRITE |(< (- x) (- y))|))
 (173 173 (:TYPE-PRESCRIPTION |(< 0 (logior x y))| . 1))
 (173 173 (:TYPE-PRESCRIPTION |(< (logior x y) 0)| . 2))
 (173 173 (:TYPE-PRESCRIPTION |(< (logior x y) 0)| . 1))
 (140 40 (:REWRITE MOD-CANCEL-*-NOT-REWRITING-GOAL-LITERAL))
 (140 40 (:REWRITE |(mod (* x (/ y)) z) not rewriting-goal-literal|))
 (138 40 (:REWRITE MOD-CANCEL-*-REWRITING-GOAL-LITERAL))
 (138 40 (:REWRITE |(mod (* x (/ y)) z) rewriting-goal-literal|))
 (125 125 (:REWRITE REMOVE-WEAK-INEQUALITIES))
 (121 121 (:REWRITE REDUCE-INTEGERP-+))
 (121 121 (:META META-INTEGERP-CORRECT))
 (110 42 (:REWRITE EQUAL-OF-BOOLEANS-REWRITE))
 (81 81 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-REMAINDER))
 (81 81 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-<-0-RATIONAL-COMMON))
 (81 81 (:REWRITE |(< (/ x) 0)|))
 (81 81 (:REWRITE |(< (* x y) 0)|))
 (75 10 (:REWRITE DEFAULT-PLUS-2))
 (49 49 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-REMAINDER))
 (49 49 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-0-<-AX+BX-RATIONAL-COMMON))
 (49 49 (:REWRITE |(< 0 (/ x))|))
 (49 49 (:REWRITE |(< 0 (* x y))|))
 (48 6 (:REWRITE RATIONALP-X))
 (45 45 (:REWRITE DEFAULT-MOD-2))
 (43 43 (:REWRITE REDUCE-MULTIPLICATIVE-CONSTANT-EQUAL))
 (43 43 (:REWRITE REDUCE-ADDITIVE-CONSTANT-EQUAL))
 (42 42 (:REWRITE EQUAL-OF-PREDICATES-REWRITE))
 (42 42 (:REWRITE |(equal c (/ x))|))
 (42 42 (:REWRITE |(equal c (- x))|))
 (42 42 (:REWRITE |(equal (/ x) c)|))
 (42 42 (:REWRITE |(equal (/ x) (/ y))|))
 (42 42 (:REWRITE |(equal (- x) c)|))
 (42 42 (:REWRITE |(equal (- x) (- y))|))
 (40 40 (:REWRITE THIS-NEEDS-TO-BE-ADDED-TO-QUOTIENT-REMAINDER-LEMMAS))
 (40 40 (:REWRITE |(mod x (- y))| . 3))
 (40 40 (:REWRITE |(mod x (- y))| . 2))
 (40 40 (:REWRITE |(mod x (- y))| . 1))
 (40 40 (:REWRITE |(mod x (* y (/ z))) rewriting-goal-literal|))
 (40 40 (:REWRITE |(mod x (* y (/ z))) not rewriting-goal-literal|))
 (40 40 (:REWRITE |(mod (- x) y)| . 3))
 (40 40 (:REWRITE |(mod (- x) y)| . 2))
 (40 40 (:REWRITE |(mod (- x) y)| . 1))
 (39 39 (:REWRITE SIMPLIFY-TERMS-SUCH-AS-AX+BX-=-0))
 (27 3 (:REWRITE |(* (if a b c) x)|))
 (18 2 (:REWRITE ACL2-NUMBERP-X))
 (15 15 (:TYPE-PRESCRIPTION RATIONALP-MOD))
 (12 10 (:REWRITE DEFAULT-PLUS-1))
 (12 2 (:REWRITE |(+ y x)|))
 (10 10 (:REWRITE MOD-POSITIVE . 2))
 (10 10 (:REWRITE MOD-POSITIVE . 1))
 (8 8 (:REWRITE NORMALIZE-TERMS-SUCH-AS-A/A+B-+-B/A+B))
 (8 8 (:REWRITE NORMALIZE-ADDENDS))
 (6 6 (:REWRITE RATIONALP-MINUS-X))
 (4 4 (:REWRITE REDUCE-RATIONALP-+))
 (4 4 (:META META-RATIONALP-CORRECT))
 (2 1 (:REWRITE |(equal (mod (+ x y) z) x)|))
 )