diff --git a/lib/minikanren/clpfd.sx b/lib/minikanren/clpfd.sx
index ab2fb10b..fb2851a8 100644
--- a/lib/minikanren/clpfd.sx
+++ b/lib/minikanren/clpfd.sx
@@ -230,8 +230,10 @@
         (let
           ((s2 (fd-add-constraint s c)))
           (let
-            ((s3 (c s2)))
-            (cond ((= s3 nil) mzero) (:else (unit s3)))))))))
+            ((s2-or-nil (c s2)))
+            (let
+              ((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil)))))
+              (cond ((= s3 nil) mzero) (:else (unit s3))))))))))
 
 ;; --- fd-lt ---
 
@@ -294,8 +296,10 @@
         (let
           ((s2 (fd-add-constraint s c)))
           (let
-            ((s3 (c s2)))
-            (cond ((= s3 nil) mzero) (:else (unit s3)))))))))
+            ((s2-or-nil (c s2)))
+            (let
+              ((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil)))))
+              (cond ((= s3 nil) mzero) (:else (unit s3))))))))))
 
 ;; --- fd-lte ---
 
@@ -358,8 +362,10 @@
         (let
           ((s2 (fd-add-constraint s c)))
           (let
-            ((s3 (c s2)))
-            (cond ((= s3 nil) mzero) (:else (unit s3)))))))))
+            ((s2-or-nil (c s2)))
+            (let
+              ((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil)))))
+              (cond ((= s3 nil) mzero) (:else (unit s3))))))))))
 
 ;; --- fd-eq ---
 
@@ -428,8 +434,10 @@
         (let
           ((s2 (fd-add-constraint s c)))
           (let
-            ((s3 (c s2)))
-            (cond ((= s3 nil) mzero) (:else (unit s3)))))))))
+            ((s2-or-nil (c s2)))
+            (let
+              ((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil)))))
+              (cond ((= s3 nil) mzero) (:else (unit s3))))))))))
 
 ;; --- labelling ---
 
@@ -519,6 +527,118 @@
                 (cond ((= s2 nil) nil) (:else s2)))))))
       (:else nil))))
 
+(define
+  fd-narrow-or-skip
+  (fn
+    (s var-key d lo hi)
+    (cond
+      ((= d nil) s)
+      (:else
+        (fd-set-domain
+          s
+          var-key
+          (filter (fn (v) (and (>= v lo) (<= v hi))) d))))))
+
+(define
+  fd-plus-prop-vvn
+  (fn
+    (wx wy wz s)
+    (let
+      ((xd (fd-domain-of s (var-name wx)))
+        (yd (fd-domain-of s (var-name wy))))
+      (cond
+        ((or (= xd nil) (= yd nil)) s)
+        (:else
+          (let
+            ((s1 (fd-narrow-or-skip s (var-name wx) xd (- wz (fd-dom-max yd)) (- wz (fd-dom-min yd)))))
+            (cond
+              ((= s1 nil) nil)
+              (:else
+                (let
+                  ((xd2 (fd-domain-of s1 (var-name wx))))
+                  (fd-narrow-or-skip
+                    s1
+                    (var-name wy)
+                    yd
+                    (- wz (fd-dom-max xd2))
+                    (- wz (fd-dom-min xd2))))))))))))
+
+(define
+  fd-plus-prop-nvv
+  (fn
+    (wx wy wz s)
+    (let
+      ((yd (fd-domain-of s (var-name wy)))
+        (zd (fd-domain-of s (var-name wz))))
+      (cond
+        ((or (= yd nil) (= zd nil)) s)
+        (:else
+          (let
+            ((s1 (fd-narrow-or-skip s (var-name wy) yd (- (fd-dom-min zd) wx) (- (fd-dom-max zd) wx))))
+            (cond
+              ((= s1 nil) nil)
+              (:else
+                (let
+                  ((yd2 (fd-domain-of s1 (var-name wy))))
+                  (fd-narrow-or-skip
+                    s1
+                    (var-name wz)
+                    zd
+                    (+ wx (fd-dom-min yd2))
+                    (+ wx (fd-dom-max yd2))))))))))))
+
+(define
+  fd-plus-prop-vnv
+  (fn
+    (wx wy wz s)
+    (let
+      ((xd (fd-domain-of s (var-name wx)))
+        (zd (fd-domain-of s (var-name wz))))
+      (cond
+        ((or (= xd nil) (= zd nil)) s)
+        (:else
+          (let
+            ((s1 (fd-narrow-or-skip s (var-name wx) xd (- (fd-dom-min zd) wy) (- (fd-dom-max zd) wy))))
+            (cond
+              ((= s1 nil) nil)
+              (:else
+                (let
+                  ((xd2 (fd-domain-of s1 (var-name wx))))
+                  (fd-narrow-or-skip
+                    s1
+                    (var-name wz)
+                    zd
+                    (+ (fd-dom-min xd2) wy)
+                    (+ (fd-dom-max xd2) wy))))))))))) 
+
+(define
+  fd-plus-prop-vvv
+  (fn
+    (wx wy wz s)
+    (let
+      ((xd (fd-domain-of s (var-name wx)))
+        (yd (fd-domain-of s (var-name wy)))
+        (zd (fd-domain-of s (var-name wz))))
+      (cond
+        ((or (= xd nil) (or (= yd nil) (= zd nil))) s)
+        (:else
+          (let
+            ((s1 (fd-narrow-or-skip s (var-name wx) xd (- (fd-dom-min zd) (fd-dom-max yd)) (- (fd-dom-max zd) (fd-dom-min yd)))))
+            (cond
+              ((= s1 nil) nil)
+              (:else
+                (let
+                  ((s2 (fd-narrow-or-skip s1 (var-name wy) yd (- (fd-dom-min zd) (fd-dom-max xd)) (- (fd-dom-max zd) (fd-dom-min xd)))))
+                  (cond
+                    ((= s2 nil) nil)
+                    (:else
+                      (fd-narrow-or-skip
+                        s2
+                        (var-name wz)
+                        zd
+                        (+ (fd-dom-min xd) (fd-dom-min yd))
+                        (+ (fd-dom-max xd) (fd-dom-max yd))))))))))))))
+
 (define
   fd-plus-prop
   (fn
@@ -534,6 +654,14 @@
           (fd-bind-or-narrow wy (- wz wx) s))
         ((and (number? wy) (number? wz))
           (fd-bind-or-narrow wx (- wz wy) s))
+        ((and (is-var? wx) (is-var? wy) (number? wz))
+          (fd-plus-prop-vvn wx wy wz s))
+        ((and (number? wx) (is-var? wy) (is-var? wz))
+          (fd-plus-prop-nvv wx wy wz s))
+        ((and (is-var? wx) (number? wy) (is-var? wz))
+          (fd-plus-prop-vnv wx wy wz s))
+        ((and (is-var? wx) (is-var? wy) (is-var? wz))
+          (fd-plus-prop-vvv wx wy wz s))
         (:else s)))))
 
 (define
@@ -547,11 +675,141 @@
         (let
           ((s2 (fd-add-constraint s c)))
           (let
-            ((s3 (c s2)))
-            (cond ((= s3 nil) mzero) (:else (unit s3)))))))))
+            ((s2-or-nil (c s2)))
+            (let
+              ((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil)))))
+              (cond ((= s3 nil) mzero) (:else (unit s3))))))))))
 
 ;; --- fd-times (x * y = z, ground-cases propagator) ---
 
+(define
+  fd-int-ceil-div
+  (fn
+    (a b)
+    (cond
+      ((= (mod a b) 0) (/ a b))
+      (:else (+ (fd-int-floor-div a b) 1)))))
+
+(define fd-int-floor-div (fn (a b) (/ (- a (mod a b)) b)))
+
+(define
+  fd-dom-positive?
+  (fn
+    (d)
+    (cond ((empty? d) false) (:else (>= (fd-dom-min d) 1)))))
+
+(define
+  fd-times-prop-vvv
+  (fn
+    (wx wy wz s)
+    (let
+      ((xd (fd-domain-of s (var-name wx)))
+        (yd (fd-domain-of s (var-name wy)))
+        (zd (fd-domain-of s (var-name wz))))
+      (cond
+        ((or (= xd nil) (or (= yd nil) (= zd nil))) s)
+        ((not (and (fd-dom-positive? xd) (and (fd-dom-positive? yd) (fd-dom-positive? zd))))
+          s)
+        (:else
+          (let
+            ((s1 (fd-narrow-or-skip s (var-name wx) xd (fd-int-ceil-div (fd-dom-min zd) (fd-dom-max yd)) (fd-int-floor-div (fd-dom-max zd) (fd-dom-min yd)))))
+            (cond
+              ((= s1 nil) nil)
+              (:else
+                (let
+                  ((s2 (fd-narrow-or-skip s1 (var-name wy) yd (fd-int-ceil-div (fd-dom-min zd) (fd-dom-max xd)) (fd-int-floor-div (fd-dom-max zd) (fd-dom-min xd)))))
+                  (cond
+                    ((= s2 nil) nil)
+                    (:else
+                      (fd-narrow-or-skip
+                        s2
+                        (var-name wz)
+                        zd
+                        (* (fd-dom-min xd) (fd-dom-min yd))
+                        (* (fd-dom-max xd) (fd-dom-max yd))))))))))))))
+
+(define
+  fd-times-prop-vvn
+  (fn
+    (wx wy wz s)
+    (let
+      ((xd (fd-domain-of s (var-name wx)))
+        (yd (fd-domain-of s (var-name wy))))
+      (cond
+        ((or (= xd nil) (= yd nil)) s)
+        ((not (and (fd-dom-positive? xd) (fd-dom-positive? yd))) s)
+        ((<= wz 0) s)
+        (:else
+          (let
+            ((s1 (fd-narrow-or-skip s (var-name wx) xd (fd-int-ceil-div wz (fd-dom-max yd)) (fd-int-floor-div wz (fd-dom-min yd)))))
+            (cond
+              ((= s1 nil) nil)
+              (:else
+                (let
+                  ((xd2 (fd-domain-of s1 (var-name wx))))
+                  (fd-narrow-or-skip
+                    s1
+                    (var-name wy)
+                    yd
+                    (fd-int-ceil-div wz (fd-dom-max xd2))
+                    (fd-int-floor-div wz (fd-dom-min xd2))))))))))))
+
+(define
+  fd-times-prop-nvv
+  (fn
+    (wx wy wz s)
+    (cond
+      ((<= wx 0) s)
+      (:else
+        (let
+          ((yd (fd-domain-of s (var-name wy)))
+            (zd (fd-domain-of s (var-name wz))))
+          (cond
+            ((or (= yd nil) (= zd nil)) s)
+            ((not (and (fd-dom-positive? yd) (fd-dom-positive? zd))) s)
+            (:else
+              (let
+                ((s1 (fd-narrow-or-skip s (var-name wy) yd (fd-int-ceil-div (fd-dom-min zd) wx) (fd-int-floor-div (fd-dom-max zd) wx))))
+                (cond
+                  ((= s1 nil) nil)
+                  (:else
+                    (let
+                      ((yd2 (fd-domain-of s1 (var-name wy))))
+                      (fd-narrow-or-skip
+                        s1
+                        (var-name wz)
+                        zd
+                        (* wx (fd-dom-min yd2))
+                        (* wx (fd-dom-max yd2))))))))))))))
+
+(define
+  fd-times-prop-vnv
+  (fn
+    (wx wy wz s)
+    (cond
+      ((<= wy 0) s)
+      (:else
+        (let
+          ((xd (fd-domain-of s (var-name wx)))
+            (zd (fd-domain-of s (var-name wz))))
+          (cond
+            ((or (= xd nil) (= zd nil)) s)
+            ((not (and (fd-dom-positive? xd) (fd-dom-positive? zd))) s)
+            (:else
+              (let
+                ((s1 (fd-narrow-or-skip s (var-name wx) xd (fd-int-ceil-div (fd-dom-min zd) wy) (fd-int-floor-div (fd-dom-max zd) wy))))
+                (cond
+                  ((= s1 nil) nil)
+                  (:else
+                    (let
+                      ((xd2 (fd-domain-of s1 (var-name wx))))
+                      (fd-narrow-or-skip
+                        s1
+                        (var-name wz)
+                        zd
+                        (* (fd-dom-min xd2) wy)
+                        (* (fd-dom-max xd2) wy))))))))))))) 
+
 (define
   fd-times-prop
   (fn
@@ -573,6 +831,14 @@
             ((= wy 0) (cond ((= wz 0) s) (:else nil)))
             ((not (= (mod wz wy) 0)) nil)
             (:else (fd-bind-or-narrow wx (/ wz wy) s))))
+        ((and (is-var? wx) (is-var? wy) (number? wz))
+          (fd-times-prop-vvn wx wy wz s))
+        ((and (number? wx) (is-var? wy) (is-var? wz))
+          (fd-times-prop-nvv wx wy wz s))
+        ((and (is-var? wx) (number? wy) (is-var? wz))
+          (fd-times-prop-vnv wx wy wz s))
+        ((and (is-var? wx) (is-var? wy) (is-var? wz))
+          (fd-times-prop-vvv wx wy wz s))
         (:else s)))))
 
 (define
@@ -586,5 +852,7 @@
         (let
           ((s2 (fd-add-constraint s c)))
           (let
-            ((s3 (c s2)))
-            (cond ((= s3 nil) mzero) (:else (unit s3)))))))))
+            ((s2-or-nil (c s2)))
+            (let
+              ((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil)))))
+              (cond ((= s3 nil) mzero) (:else (unit s3))))))))))
diff --git a/lib/minikanren/diseq.sx b/lib/minikanren/diseq.sx
new file mode 100644
index 00000000..1567287e
--- /dev/null
+++ b/lib/minikanren/diseq.sx
@@ -0,0 +1,71 @@
+;; lib/minikanren/diseq.sx — Phase 5 polish: =/= disequality with a
+;; constraint store, generalising nafc / fd-neq to logic terms.
+;;
+;; The constraint store lives under the same `_fd` reserved key as the
+;; CLP(FD) propagators (a disequality is just another constraint
+;; closure that the existing fd-fire-store machinery re-runs).
+;;
+;; =/= semantics:
+;;   - If u and v walk to ground non-unifiable terms, succeed (drop).
+;;   - If they walk to terms that COULD become equal under a future
+;;     binding, store the constraint; re-check after each binding.
+;;   - If they're already equal (unify with no new bindings), fail.
+;;
+;; Implementation: each =/= test attempts (mk-unify wu wv s).
+;;   nil      — distinct, keep s, drop the constraint (return s).
+;;   subst eq — equal, fail (return nil).
+;;   subst >  — partially unifiable; keep the constraint, return s.
+;;
+;; "Substitution equal to s" is detected via key-count: mk-unify only
+;; ever extends a substitution, never removes from it, so equal
+;; key-count means no new bindings were needed.
+
+(define
+  =/=-prop
+  (fn
+    (u v s)
+    (let
+      ((s-after (mk-unify u v s)))
+      (cond
+        ((= s-after nil) s)
+        ((= (len (keys s)) (len (keys s-after))) nil)
+        (:else s)))))
+
+(define
+  =/=
+  (fn
+    (u v)
+    (fn
+      (s)
+      (let
+        ((c (fn (sp) (=/=-prop u v sp))))
+        (let
+          ((s2 (fd-add-constraint s c)))
+          (let
+            ((s2-or-nil (c s2)))
+            (let
+              ((s3 (cond ((= s2-or-nil nil) nil) (:else (fd-fire-store s2-or-nil)))))
+              (cond ((= s3 nil) mzero) (:else (unit s3))))))))))
+
+;; --- constraint-aware == ---
+;;
+;; Plain `==` doesn't fire the constraint store, so a binding that
+;; should violate a pending =/= goes undetected. `==-cs` is the
+;; drop-in replacement that fires fd-fire-store after each binding.
+;; Use ==-cs in any program that mixes =/= (or fd-* goals that should
+;; re-check after non-FD bindings) with regular unification.
+
+(define
+  ==-cs
+  (fn
+    (u v)
+    (fn
+      (s)
+      (let
+        ((s2 (mk-unify u v s)))
+        (cond
+          ((= s2 nil) mzero)
+          (:else
+            (let
+              ((s3 (fd-fire-store s2)))
+              (cond ((= s3 nil) mzero) (:else (unit s3))))))))))
diff --git a/lib/minikanren/tabling-slg.sx b/lib/minikanren/tabling-slg.sx
new file mode 100644
index 00000000..c952e3ce
--- /dev/null
+++ b/lib/minikanren/tabling-slg.sx
@@ -0,0 +1,94 @@
+;; lib/minikanren/tabling-slg.sx — Phase 7 piece A: SLG-style tabling.
+;;
+;; Naive memoization (table-1/2/3 in tabling.sx) drains the body's
+;; answer stream eagerly, then caches. Recursive tabled calls with the
+;; SAME ground key see an empty cache (the in-progress entry doesn't
+;; exist), so they recurse and the host overflows on cyclic relations.
+;;
+;; This module ships the in-progress-sentinel piece of SLG resolution:
+;; before evaluating the body, mark the cache entry as :in-progress;
+;; any recursive call to the same key sees the sentinel and returns
+;; mzero (no answers yet). Outer recursion thus terminates on cycles.
+;; Limitation: a single pass — answers found by cycle-dependent
+;; recursive calls are NOT discovered. Full SLG with fixed-point
+;; iteration (re-running until no new answers) is left for follow-up.
+
+(define
+  table-2-slg-iter
+  (fn
+    (rel-fn input output s key prev-vals)
+    (begin
+      (mk-tab-store! key prev-vals)
+      (let
+        ((all-substs (stream-take -1 ((rel-fn input output) s))))
+        (let
+          ((vals (map (fn (s2) (mk-walk* output s2)) all-substs)))
+          (cond
+            ((= (len vals) (len prev-vals))
+              (begin
+                (mk-tab-store! key vals)
+                (mk-tab-replay-vals vals output s)))
+            (:else (table-2-slg-iter rel-fn input output s key vals))))))))
+
+(define
+  table-2-slg
+  (fn
+    (name rel-fn)
+    (fn
+      (input output)
+      (fn
+        (s)
+        (let
+          ((winput (mk-walk* input s)))
+          (cond
+            ((mk-tab-ground-term? winput)
+              (let
+                ((key (str name "/slg/" winput)))
+                (let
+                  ((cached (mk-tab-lookup key)))
+                  (cond
+                    ((not (= cached :miss))
+                      (mk-tab-replay-vals cached output s))
+                    (:else
+                      (table-2-slg-iter rel-fn input output s key (list)))))))
+            (:else ((rel-fn input output) s))))))))
+
+(define
+  table-3-slg-iter
+  (fn
+    (rel-fn i1 i2 output s key prev-vals)
+    (begin
+      (mk-tab-store! key prev-vals)
+      (let
+        ((all-substs (stream-take -1 ((rel-fn i1 i2 output) s))))
+        (let
+          ((vals (map (fn (s2) (mk-walk* output s2)) all-substs)))
+          (cond
+            ((= (len vals) (len prev-vals))
+              (begin
+                (mk-tab-store! key vals)
+                (mk-tab-replay-vals vals output s)))
+            (:else (table-3-slg-iter rel-fn i1 i2 output s key vals))))))))
+
+(define
+  table-3-slg
+  (fn
+    (name rel-fn)
+    (fn
+      (i1 i2 output)
+      (fn
+        (s)
+        (let
+          ((wi1 (mk-walk* i1 s)) (wi2 (mk-walk* i2 s)))
+          (cond
+            ((and (mk-tab-ground-term? wi1) (mk-tab-ground-term? wi2))
+              (let
+                ((key (str name "/slg3/" wi1 "/" wi2)))
+                (let
+                  ((cached (mk-tab-lookup key)))
+                  (cond
+                    ((not (= cached :miss))
+                      (mk-tab-replay-vals cached output s))
+                    (:else
+                      (table-3-slg-iter rel-fn i1 i2 output s key (list)))))))
+            (:else ((rel-fn i1 i2 output) s))))))))
diff --git a/lib/minikanren/tests/clpfd-bounds.sx b/lib/minikanren/tests/clpfd-bounds.sx
new file mode 100644
index 00000000..32a02f44
--- /dev/null
+++ b/lib/minikanren/tests/clpfd-bounds.sx
@@ -0,0 +1,316 @@
+;; lib/minikanren/tests/clpfd-bounds.sx — Phase 6 piece B: bounds-consistency
+;; for fd-plus and fd-times in the partial- and all-domain cases.
+;;
+;; We probe domains directly (peek at the FD store) before any labelling
+;; happens. This isolates the propagator's narrowing behaviour from the
+;; search engine.
+
+(define
+  probe-dom
+  (fn
+    (goal var-key)
+    (let
+      ((s (first (stream-take 1 (goal empty-s)))))
+      (cond ((= s nil) :no-subst) (:else (fd-domain-of s var-key))))))
+
+;; --- fd-plus partial-domain narrowing ---
+
+(mk-test
+  "fd-plus-vvn-narrows-x"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")))
+    (probe-dom
+      (mk-conj
+        (fd-in
+          x
+          (list
+            1
+            2
+            3
+            4
+            5
+            6
+            7
+            8
+            9
+            10))
+        (fd-in y (list 1 2 3))
+        (fd-plus x y 10))
+      "x"))
+  (list 7 8 9))
+
+(mk-test
+  "fd-plus-vvn-narrows-y"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")))
+    (probe-dom
+      (mk-conj
+        (fd-in
+          x
+          (list
+            1
+            2
+            3
+            4
+            5
+            6
+            7
+            8
+            9
+            10))
+        (fd-in y (list 1 2 3))
+        (fd-plus x y 10))
+      "y"))
+  (list 1 2 3))
+
+(mk-test
+  "fd-plus-nvv-narrows"
+  (let
+    ((y (mk-var "y")) (z (mk-var "z")))
+    (probe-dom
+      (mk-conj
+        (fd-in y (list 1 2 3))
+        (fd-in
+          z
+          (list
+            1
+            2
+            3
+            4
+            5
+            6
+            7
+            8
+            9
+            10
+            11
+            12
+            13
+            14
+            15
+            16
+            17
+            18
+            19
+            20))
+        (fd-plus 5 y z))
+      "z"))
+  (list 6 7 8))
+
+(mk-test
+  "fd-plus-vvv-narrows-z"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")) (z (mk-var "z")))
+    (probe-dom
+      (mk-conj
+        (fd-in x (list 1 2 3))
+        (fd-in y (list 1 2 3))
+        (fd-in
+          z
+          (list
+            1
+            2
+            3
+            4
+            5
+            6
+            7
+            8
+            9
+            10
+            11
+            12
+            13
+            14
+            15
+            16
+            17
+            18
+            19
+            20))
+        (fd-plus x y z))
+      "z"))
+  (list 2 3 4 5 6))
+
+(mk-test
+  "fd-plus-vvv-narrows-x"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")) (z (mk-var "z")))
+    (probe-dom
+      (mk-conj
+        (fd-in
+          x
+          (list
+            1
+            2
+            3
+            4
+            5
+            6
+            7
+            8
+            9
+            10))
+        (fd-in y (list 1 2 3))
+        (fd-in z (list 5 6 7))
+        (fd-plus x y z))
+      "x"))
+  (list 2 3 4 5 6))
+
+;; --- fd-times partial-domain narrowing (positive domains) ---
+
+(mk-test
+  "fd-times-vvn-narrows"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")))
+    (probe-dom
+      (mk-conj
+        (fd-in
+          x
+          (list
+            1
+            2
+            3
+            4
+            5
+            6))
+        (fd-in
+          y
+          (list
+            1
+            2
+            3
+            4
+            5
+            6))
+        (fd-times x y 12))
+      "x"))
+  (list 2 3 4 5 6))
+
+(mk-test
+  "fd-times-nvv-narrows"
+  (let
+    ((y (mk-var "y")) (z (mk-var "z")))
+    (probe-dom
+      (mk-conj
+        (fd-in y (list 1 2 3 4))
+        (fd-in
+          z
+          (list
+            1
+            2
+            3
+            4
+            5
+            6
+            7
+            8
+            9
+            10
+            11
+            12
+            13
+            14
+            15
+            16
+            17
+            18
+            19
+            20))
+        (fd-times 3 y z))
+      "z"))
+  (list
+    3
+    4
+    5
+    6
+    7
+    8
+    9
+    10
+    11
+    12))
+
+(mk-test
+  "fd-times-vvv-narrows"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")) (z (mk-var "z")))
+    (probe-dom
+      (mk-conj
+        (fd-in x (list 1 2 3))
+        (fd-in y (list 1 2 3))
+        (fd-in
+          z
+          (list
+            1
+            2
+            3
+            4
+            5
+            6
+            7
+            8
+            9
+            10
+            11
+            12
+            13
+            14
+            15
+            16
+            17
+            18
+            19
+            20))
+        (fd-times x y z))
+      "z"))
+  (list
+    1
+    2
+    3
+    4
+    5
+    6
+    7
+    8
+    9))
+
+;; --- bounds force impossible branches to fail early ---
+
+(mk-test
+  "fd-plus-impossible-via-bounds"
+  (let
+    ((x (mk-var "x")) (y (mk-var "y")))
+    (probe-dom
+      (mk-conj
+        (fd-in
+          x
+          (list
+            1
+            2
+            3
+            4
+            5
+            6
+            7
+            8
+            9
+            10))
+        (fd-in
+          y
+          (list
+            1
+            2
+            3
+            4
+            5
+            6
+            7
+            8
+            9
+            10))
+        (fd-plus x y 100))
+      "x"))
+  :no-subst)
+
+(mk-tests-run!)
diff --git a/lib/minikanren/tests/diseq.sx b/lib/minikanren/tests/diseq.sx
new file mode 100644
index 00000000..e88fc5bc
--- /dev/null
+++ b/lib/minikanren/tests/diseq.sx
@@ -0,0 +1,83 @@
+;; lib/minikanren/tests/diseq.sx — Phase 5 polish: =/= disequality.
+
+;; --- ground cases ---
+
+(mk-test
+  "=/=-ground-distinct"
+  (run* q (=/= 1 2))
+  (list (make-symbol "_.0")))
+(mk-test "=/=-ground-equal" (run* q (=/= 1 1)) (list))
+(mk-test
+  "=/=-ground-strings"
+  (run* q (=/= "a" "b"))
+  (list (make-symbol "_.0")))
+(mk-test "=/=-ground-strings-eq" (run* q (=/= "a" "a")) (list))
+
+;; --- structural ---
+
+(mk-test
+  "=/=-pair-distinct"
+  (run* q (=/= (list 1 2) (list 1 3)))
+  (list (make-symbol "_.0")))
+(mk-test
+  "=/=-pair-equal"
+  (run* q (=/= (list 1 2) (list 1 2)))
+  (list))
+(mk-test
+  "=/=-pair-vs-atom"
+  (run* q (=/= (list 1) 1))
+  (list (make-symbol "_.0")))
+
+;; --- partial / late binding ---
+;;
+;; ==-cs is required to wake up the constraint store after a binding;
+;; plain == doesn't fire constraints.
+
+(mk-test
+  "=/=-late-bind-violates"
+  (run* q (fresh (x) (=/= x 5) (==-cs x 5) (== q x)))
+  (list))
+
+(mk-test
+  "=/=-late-bind-ok"
+  (run* q (fresh (x) (=/= x 5) (==-cs x 7) (== q x)))
+  (list 7))
+
+(mk-test
+  "=/=-two-vars-equal-late-fails"
+  (run*
+    q
+    (fresh
+      (x y)
+      (=/= x y)
+      (==-cs x 1)
+      (==-cs y 1)
+      (== q (list x y))))
+  (list))
+
+(mk-test
+  "=/=-two-vars-distinct-late"
+  (run*
+    q
+    (fresh
+      (x y)
+      (=/= x y)
+      (==-cs x 1)
+      (==-cs y 2)
+      (== q (list x y))))
+  (list (list 1 2)))
+
+;; --- compose with conde / fresh ---
+
+(mk-test
+  "=/=-with-membero-filter"
+  (run*
+    q
+    (fresh
+      (x)
+      (membero x (list 1 2 3))
+      (=/= x 2)
+      (== q x)))
+  (list 1 3))
+
+(mk-tests-run!)
diff --git a/lib/minikanren/tests/send-more-money.sx b/lib/minikanren/tests/send-more-money.sx
new file mode 100644
index 00000000..9fd81cf9
--- /dev/null
+++ b/lib/minikanren/tests/send-more-money.sx
@@ -0,0 +1,97 @@
+;; lib/minikanren/tests/send-more-money.sx — classic cryptarithmetic
+;;
+;;     S E N D
+;;   + M O R E
+;;   ---------
+;;   M O N E Y
+;;
+;; Column-by-column encoding with carries c1, c2, c3, and the
+;; leftmost column produces a carry which equals M (the result is 5 digits).
+;; All 8 letters distinct; S ≠ 0, M ≠ 0.
+;; Unique solution: S=9, E=5, N=6, D=7, M=1, O=0, R=8, Y=2.
+;;
+;; Note: the full search labelling 11 variables from {0..9} is too slow
+;; for naive labelling order (10^11 combinations naively, even with
+;; bounds-consistency the branching factor dominates). Real CLP(FD)
+;; systems use first-fail heuristics. Here we only verify the encoding
+;; against the known answer.
+
+(define
+  digits-0-9
+  (list
+    0
+    1
+    2
+    3
+    4
+    5
+    6
+    7
+    8
+    9))
+(define
+  digits-1-9
+  (list
+    1
+    2
+    3
+    4
+    5
+    6
+    7
+    8
+    9))
+
+(define
+  smm-col-with-carry
+  (fn
+    (x y carry-in z carry-out)
+    (fresh
+      (xy xyc ten-cout z-plus-ten-cout)
+      (fd-plus x y xy)
+      (fd-plus xy carry-in xyc)
+      (fd-times 10 carry-out ten-cout)
+      (fd-plus z ten-cout z-plus-ten-cout)
+      (fd-eq xyc z-plus-ten-cout))))
+
+(define
+  send-more-money
+  (fn
+    (S E N D M O R Y)
+    (fresh
+      (c1 c2 c3)
+      (mk-conj
+        (fd-in S digits-1-9)
+        (fd-in M digits-1-9)
+        (fd-in E digits-0-9)
+        (fd-in N digits-0-9)
+        (fd-in D digits-0-9)
+        (fd-in O digits-0-9)
+        (fd-in R digits-0-9)
+        (fd-in Y digits-0-9)
+        (fd-in c1 (list 0 1))
+        (fd-in c2 (list 0 1))
+        (fd-in c3 (list 0 1))
+        (fd-distinct (list S E N D M O R Y))
+        (smm-col-with-carry D E 0 Y c1)
+        (smm-col-with-carry N R c1 E c2)
+        (smm-col-with-carry E O c2 N c3)
+        (smm-col-with-carry S M c3 O M)
+        (fd-label (list S E N D M O R Y c1 c2 c3))))))
+
+(mk-test
+  "send-more-money-verify-known-solution"
+  (run*
+    q
+    (send-more-money
+      9
+      5
+      6
+      7
+      1
+      0
+      8
+      2))
+  (list (make-symbol "_.0")))
+
+(mk-tests-run!)
diff --git a/lib/minikanren/tests/sudoku-4x4.sx b/lib/minikanren/tests/sudoku-4x4.sx
new file mode 100644
index 00000000..771e0fc7
--- /dev/null
+++ b/lib/minikanren/tests/sudoku-4x4.sx
@@ -0,0 +1,89 @@
+;; lib/minikanren/tests/sudoku-4x4.sx — Sudoku 4×4 via CLP(FD).
+;;
+;; Grid in row-major order:
+;;
+;;   c0 c1 | c2 c3
+;;   c4 c5 | c6 c7
+;;   ------+------
+;;   c8 c9 | cA cB
+;;   cC cD | cE cF
+;;
+;; Each cell ∈ {1, 2, 3, 4}. 4 rows + 4 cols + 4 2x2 boxes are each a
+;; distinct permutation.
+
+(define digits-1-4 (list 1 2 3 4))
+
+(define
+  sudoku-4x4
+  (fn
+    (cells)
+    (let
+      ((c0 (nth cells 0))
+        (c1 (nth cells 1))
+        (c2 (nth cells 2))
+        (c3 (nth cells 3))
+        (c4 (nth cells 4))
+        (c5 (nth cells 5))
+        (c6 (nth cells 6))
+        (c7 (nth cells 7))
+        (c8 (nth cells 8))
+        (c9 (nth cells 9))
+        (cA (nth cells 10))
+        (cB (nth cells 11))
+        (cC (nth cells 12))
+        (cD (nth cells 13))
+        (cE (nth cells 14))
+        (cF (nth cells 15)))
+      (mk-conj
+        (fd-in c0 digits-1-4)
+        (fd-in c1 digits-1-4)
+        (fd-in c2 digits-1-4)
+        (fd-in c3 digits-1-4)
+        (fd-in c4 digits-1-4)
+        (fd-in c5 digits-1-4)
+        (fd-in c6 digits-1-4)
+        (fd-in c7 digits-1-4)
+        (fd-in c8 digits-1-4)
+        (fd-in c9 digits-1-4)
+        (fd-in cA digits-1-4)
+        (fd-in cB digits-1-4)
+        (fd-in cC digits-1-4)
+        (fd-in cD digits-1-4)
+        (fd-in cE digits-1-4)
+        (fd-in cF digits-1-4)
+        (fd-distinct (list c0 c1 c2 c3))
+        (fd-distinct (list c4 c5 c6 c7))
+        (fd-distinct (list c8 c9 cA cB))
+        (fd-distinct (list cC cD cE cF))
+        (fd-distinct (list c0 c4 c8 cC))
+        (fd-distinct (list c1 c5 c9 cD))
+        (fd-distinct (list c2 c6 cA cE))
+        (fd-distinct (list c3 c7 cB cF))
+        (fd-distinct (list c0 c1 c4 c5))
+        (fd-distinct (list c2 c3 c6 c7))
+        (fd-distinct (list c8 c9 cC cD))
+        (fd-distinct (list cA cB cE cF))
+        (fd-label cells)))))
+
+;; --- Tests ---
+
+(mk-test
+  "sudoku-4x4-empty-grid-count"
+  (let
+    ((sols (run* q (fresh (c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 cA cB cC cD cE cF) (== q (list c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 cA cB cC cD cE cF)) (sudoku-4x4 (list c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 cA cB cC cD cE cF))))))
+    (len sols))
+  288)
+
+(mk-test
+  "sudoku-4x4-impossible-clue-empty"
+  (run*
+    q
+    (fresh
+      (c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 cA cB cC cD cE cF)
+      (== c0 1)
+      (== c1 1)
+      (== q (list c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 cA cB cC cD cE cF))
+      (sudoku-4x4 (list c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 cA cB cC cD cE cF))))
+  (list))
+
+(mk-tests-run!)
diff --git a/lib/minikanren/tests/tabling-slg.sx b/lib/minikanren/tests/tabling-slg.sx
new file mode 100644
index 00000000..e4409390
--- /dev/null
+++ b/lib/minikanren/tests/tabling-slg.sx
@@ -0,0 +1,56 @@
+;; lib/minikanren/tests/tabling-slg.sx — Phase 7 piece A: SLG-style tabling.
+
+;; --- table-2-slg with Fibonacci (sanity: same answer as naive table-2) ---
+
+(mk-tab-clear!)
+(define
+  slg-fib-o
+  (table-2-slg
+    "slg-fib"
+    (fn
+      (n result)
+      (conde
+        ((== n 0) (== result 0))
+        ((== n 1) (== result 1))
+        ((fresh (n-1 n-2 r-1 r-2) (lto-i 1 n) (minuso-i n 1 n-1) (minuso-i n 2 n-2) (slg-fib-o n-1 r-1) (slg-fib-o n-2 r-2) (pluso-i r-1 r-2 result)))))))
+
+(mk-tab-clear!)
+(mk-test "slg-fib-five" (run* q (slg-fib-o 5 q)) (list 5))
+(mk-tab-clear!)
+(mk-test "slg-fib-ten" (run* q (slg-fib-o 10 q)) (list 55))
+
+;; --- table-3-slg with cyclic-graph patho ---
+
+(define slg-cyc-edges (list (list :a :b) (list :b :a) (list :b :c)))
+(define slg-cyc-edgeo (fn (x y) (membero (list x y) slg-cyc-edges)))
+
+(mk-tab-clear!)
+(define
+  tab-patho
+  (table-3-slg
+    "patho"
+    (fn
+      (x y path)
+      (conde
+        ((slg-cyc-edgeo x y) (== path (list x y)))
+        ((fresh (z mid) (slg-cyc-edgeo x z) (tab-patho z y mid) (conso x mid path)))))))
+
+(mk-tab-clear!)
+(mk-test
+  "slg-cyclic-direct"
+  (run* q (tab-patho :a :b q))
+  (list (list :a :b)))
+
+(mk-tab-clear!)
+(mk-test
+  "slg-cyclic-multi-hop"
+  (run* q (tab-patho :a :c q))
+  (list (list :a :b :c)))
+
+(mk-tab-clear!)
+(mk-test
+  "slg-cyclic-self-loop-finite"
+  (run* q (tab-patho :a :a q))
+  (list (list :a :b :a)))
+
+(mk-tests-run!)
diff --git a/plans/minikanren-on-sx.md b/plans/minikanren-on-sx.md
index 16816005..8cc0f953 100644
--- a/plans/minikanren-on-sx.md
+++ b/plans/minikanren-on-sx.md
@@ -205,6 +205,23 @@ _(none yet)_
 
 _Newest first._
 
+- **2026-05-09** — **deferred-plan execution**: shipped all four pieces from
+  `plans/minikanren-deferred.md` (on architecture):
+  - **Piece B** — bounds-consistency for `fd-plus` / `fd-times` (vvn / nvv /
+    vnv / vvv branches; integer-division helpers for ceil/floor);
+  - **Piece D** — send-more-money (column-with-carry encoding, verified
+    against the known answer) and Sudoku 4×4 (288 fillings of empty grid;
+    immediate failure on contradictory clues);
+  - **Piece C** — `=/=` disequality with constraint store, plus `==-cs`
+    constraint-aware unify so the store re-fires on bindings;
+  - **Piece A** — SLG-style tabling: in-progress sentinel + fixed-point
+    iteration. Cyclic patho terminates: `(tab-patho :a :c q)` on a graph
+    with cycle `a↔b` plus `b→c` returns `((:a :b :c))`. Naive tabling
+    diverged on the same query. Mutually-recursive coordination across
+    independent tabled relations is left for follow-up (proper SLG
+    worklist).
+  170/170 across the new+FD-related test files.
+
 - **2026-05-08** — **Session snapshot**: 17 lib files, 61 test files, 1229
   library LOC + 4360 test LOC, **551/551 tests cumulative**. Library covers
   Phases 1–5 fully, Phase 6 partial (FD helpers + intarith escape), Phase 7