diff --git a/new.exs b/new.exs
index fbdcfde..b3f4630 100644
--- a/new.exs
+++ b/new.exs
@@ -716,7 +716,7 @@ defmodule Tdd.Consistency.Engine do
     end
   end
 
-  defp reduce_implication(_implication, _all, error, _), do: error
+  defp reduce_implication(_implication, _all_assumptions, error_acc), do: error_acc
 
   # --- Step 2: Flat Consistency Checks ---
 
@@ -766,48 +766,51 @@ defmodule Tdd.Consistency.Engine do
     if is_empty and (has_head_prop or has_tail_prop), do: :error, else: :ok
   end
 
-  defp check_integer_consistency(assumptions) do
-    # Reduce all integer-related assumptions to a single valid range [min, max].
-    # If the range becomes invalid (min > max), it's a contradiction.
+defp check_integer_consistency(assumptions) do
     initial_range = {:neg_inf, :pos_inf}
 
     result =
       Enum.reduce_while(assumptions, initial_range, fn assumption, {min, max} ->
         case assumption do
-          # x < N => max becomes min(max, N-1)
-          {{2, :alt, n, _}, true} -> narrow_range(min, :erlang.min(max, n - 1))
-          # not (x < N) <=> x >= N => min becomes max(min, N)
-          {{2, :alt, n, _}, false} -> narrow_range(:erlang.max(min, n), max)
-          # x == N => min becomes max(min, N), max becomes min(max, N)
-          {{2, :beq, n, _}, true} -> narrow_range(:erlang.max(min, n), :erlang.min(max, n))
-          # x != N : this is only a contradiction if the range is exactly {N, N}
+          {{2, :alt, n, _}, true} -> narrow_range(min, safe_min(max, n - 1))
+          {{2, :alt, n, _}, false} -> narrow_range(safe_max(min, n), max)
+          {{2, :beq, n, _}, true} -> narrow_range(safe_max(min, n), safe_min(max, n))
           {{2, :beq, n, _}, false} when min == n and max == n -> {:halt, :invalid}
-          # x > N => min becomes max(min, N+1)
-          {{2, :cgt, n, _}, true} -> narrow_range(:erlang.max(min, n + 1), max)
-          # not (x > N) <=> x <= N => max becomes min(max, N)
-          {{2, :cgt, n, _}, false} -> narrow_range(min, :erlang.min(max, n))
-          # Not an integer assumption, continue.
+          {{2, :cgt, n, _}, true} -> narrow_range(safe_max(min, n + 1), max)
+          {{2, :cgt, n, _}, false} -> narrow_range(min, safe_min(max, n))
           _ -> {:cont, {min, max}}
         end
       end)
 
-    case result,
-      do:
-        (
-          :invalid -> :error
-          _ -> :ok
-        )
+    case result, do: (:invalid -> :error; _ -> :ok)
   end
 
-  # Helper to check if a new range is valid and continue/halt the reduction.
+  # **IMPROVED**: A clearer implementation for checking range validity.
   defp narrow_range(min, max) do
-    cond do
-      min == :neg_inf or max == :pos_inf -> {:cont, {min, max}}
-      min > max -> {:halt, :invalid}
-      true -> {:cont, {min, max}}
-    end
+    is_invalid =
+      case {min, max} do
+        {:neg_inf, _} -> false
+        {_, :pos_inf} -> false
+        {m, n} when is_integer(m) and is_integer(n) -> m > n
+        _ -> false # Should not happen with safe helpers
+      end
+
+    if is_invalid, do: {:halt, :invalid}, else: {:cont, {min, max}}
   end
 
+  # **NEW**: Safe comparison helpers that understand :neg_inf and :pos_inf
+  defp safe_max(:neg_inf, x), do: x
+  defp safe_max(x, :neg_inf), do: x
+  defp safe_max(:pos_inf, _), do: :pos_inf
+  defp safe_max(_, :pos_inf), do: :pos_inf
+  defp safe_max(a, b), do: :erlang.max(a, b)
+
+  defp safe_min(:pos_inf, x), do: x
+  defp safe_min(x, :pos_inf), do: x
+  defp safe_min(:neg_inf, _), do: :neg_inf
+  defp safe_min(_, :neg_inf), do: :neg_inf
+  defp safe_min(a, b), do: :erlang.min(a, b)
+
   # --- Step 3: Recursive Consistency (Disabled but preserved) ---
   defp check_recursive_consistency(assumptions, full_context) do
     # 1. Gather all ambient constraints from the parent context.
@@ -1791,9 +1794,9 @@ defmodule ConsistencyEngineTests do
     test("A single valid assumption is consistent", :consistent, %{Variable.v_is_atom() => true})
 
     test(
-      "An explicit contradiction is caught",
+      "An implied contradiction is caught by expander",
       :contradiction,
-      %{Variable.v_is_atom() => true, Variable.v_is_atom() => false}
+      %{Variable.v_atom_eq(:foo) => true, Variable.v_is_atom() => false}
     )
 
     test(
@@ -2368,5 +2371,5 @@ TddStoreTests.run()
 TddVariableTests.run()
 # TddAlgoTests.run()
 ConsistencyEngineTests.run()
-# TypeReconstructorTests.run()
+TypeReconstructorTests.run()
 # CompilerAlgoTests.run()