diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/1.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/1.diff
index 28b9f96ba1..2f34a2fac4 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/1.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/1.diff
@@ -10,10 +10,9 @@
 <    (balance (c t_1 n_2 (ins n_1 t_2)))
 ---
 >    (c t_1 n_2 (ins n_1 t_2))
-301a302,307
+301a302,306
 > (define small-counter-example
 >   (term (B (R E (num->n 0) E)
 >            (num->n 2)
 >            E)))
 > (test-equal (check small-counter-example) #f)
-> 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/2.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/2.diff
index f70058c005..e719f0d691 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/2.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/2.diff
@@ -5,10 +5,9 @@
 100,101d99
 <   [(balance (B (R (R t_1 n_1 t_2) n_2 t_3) n_3 t_4))
 <    (R (B t_1 n_1 t_2) n_2 (B t_3 n_3 t_4))]
-301a300,305
+301a300,304
 > (define small-counter-example
 >   (term (B (R E (num->n 1) E)
 >            (num->n 2)
 >            E)))
 > (test-equal (check small-counter-example) #f)
-> 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/3.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/3.diff
index beb2092ac7..2f134e84cf 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/3.diff
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/3.diff
@@ -6,7 +6,7 @@
 <   [(rbt (B (c_1 t_11 n_1 t_12) n (c_2 t_21 n_2 t_22)) n_1min n_2max (s n_bd))
 ---
 >   [(rbt (B (c_1 t_11 n_1 t_12) n (c_2 t_21 n_2 t_22)) n_1min n_2max n_bd)
-301a302,311
+301a302,310
 > (define small-counter-example
 >   (term (B 
 >          (B 
@@ -16,4 +16,3 @@
 >          (num->n 4)
 >          (R E (num->n 5) E))))
 > (test-equal (check small-counter-example) #f)
-> 
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-1.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-1.rkt
index 650a892bad..f345efc3a3 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-1.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-1.rkt
@@ -304,22 +304,3 @@
            (num->n 2)
            E)))
 (test-equal (check small-counter-example) #f)
-
-(define fixed
-  (term
-   (;; 1 and 2
-    (B (R E (num->n 1) E)
-       (num->n 3)
-       E)
-    ;; 3
-    (B
-     ;;; size should be 1, but in 3 it's 0
-     (B 
-      ;; size is 0
-      (R E (num->n 1) E)
-      (num->n 2)
-      ;; size is 0
-      (R E (num->n 3) E))
-     (num->n 5)
-     ;; size is 0
-     (R E (num->n 10) E)))))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-2.rkt
index 5f7b19856a..3673bb8bf7 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-2.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-2.rkt
@@ -302,22 +302,3 @@
            (num->n 2)
            E)))
 (test-equal (check small-counter-example) #f)
-
-(define fixed
-  (term
-   (;; 1 and 2
-    (B (R E (num->n 1) E)
-       (num->n 3)
-       E)
-    ;; 3
-    (B
-     ;;; size should be 1, but in 3 it's 0
-     (B 
-      ;; size is 0
-      (R E (num->n 1) E)
-      (num->n 2)
-      ;; size is 0
-      (R E (num->n 3) E))
-     (num->n 5)
-     ;; size is 0
-     (R E (num->n 10) E)))))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-3.rkt
index b557baf65a..5d6134943c 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-3.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-3.rkt
@@ -308,22 +308,3 @@
          (num->n 4)
          (R E (num->n 5) E))))
 (test-equal (check small-counter-example) #f)
-
-(define fixed
-  (term
-   (;; 1 and 2
-    (B (R E (num->n 1) E)
-       (num->n 3)
-       E)
-    ;; 3
-    (B
-     ;;; size should be 1, but in 3 it's 0
-     (B 
-      ;; size is 0
-      (R E (num->n 1) E)
-      (num->n 2)
-      ;; size is 0
-      (R E (num->n 3) E))
-     (num->n 5)
-     ;; size is 0
-     (R E (num->n 10) E)))))
diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-base.rkt
index d48f55eecc..5a3a9622a8 100644
--- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-base.rkt
+++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rbtrees/rbtrees-base.rkt
@@ -299,21 +299,3 @@
         (generate-term rbtrees t #:i-th index)
         (set! index (add1 index))))))
 
-(define fixed
-  (term
-   (;; 1 and 2
-    (B (R E (num->n 1) E)
-       (num->n 3)
-       E)
-    ;; 3
-    (B
-     ;;; size should be 1, but in 3 it's 0
-     (B 
-      ;; size is 0
-      (R E (num->n 1) E)
-      (num->n 2)
-      ;; size is 0
-      (R E (num->n 3) E))
-     (num->n 5)
-     ;; size is 0
-     (R E (num->n 10) E)))))