diff --git a/new.exs b/new.exs
index 99b16b8..8e19283 100644
--- a/new.exs
+++ b/new.exs
@@ -1,3 +1,46 @@
+defmodule Tdd.Debug do
+  @moduledoc "Helpers for debugging TDD structures."
+  alias Tdd.Store
+
+  @doc "Prints a formatted representation of a TDD graph starting from an ID."
+  def print(id) do
+    IO.puts("--- TDD Graph (ID: #{id}) ---")
+    do_print(id, 0, MapSet.new())
+    IO.puts("------------------------")
+  end
+
+  defp do_print(id, indent_level, visited) do
+    prefix = String.duplicate("  ", indent_level)
+
+    if MapSet.member?(visited, id) do
+      IO.puts("#{prefix}ID #{id} -> [Seen, recursive link]")
+      :ok
+    else
+      new_visited = MapSet.put(visited, id)
+
+      case Store.get_node(id) do
+        {:ok, :true_terminal} ->
+          IO.puts("#{prefix}ID #{id} -> TRUE")
+
+        {:ok, :false_terminal} ->
+          IO.puts("#{prefix}ID #{id} -> FALSE")
+
+        {:ok, {var, y, n, d}} ->
+          IO.puts("#{prefix}ID #{id}: IF #{inspect(var)}")
+          IO.puts("#{prefix}  ├─ Yes:")
+          do_print(y, indent_level + 2, new_visited)
+          IO.puts("#{prefix}  ├─ No:")
+          do_print(n, indent_level + 2, new_visited)
+          IO.puts("#{prefix}  └─ DC:")
+          do_print(d, indent_level + 2, new_visited)
+
+        {:error, reason} ->
+          IO.puts("#{prefix}ID #{id}: ERROR - #{reason}")
+      end
+    end
+  end
+end
+
 defmodule Tdd.TypeSpec do
   @moduledoc """
   Defines the `TypeSpec` structure and functions for its manipulation.
@@ -529,15 +572,19 @@ defmodule Tdd.Variable do
 
   # --- Category 5: List Properties ---
   # All are now 4-element tuples. The sorting will be correct.
-  @spec v_list_all_elements_are(TypeSpec.t()) :: term()
-  def v_list_all_elements_are(element_spec), do: {5, :a_all_elements, element_spec, nil}
+  # @spec v_list_all_elements_are(TypeSpec.t()) :: term()
+  # def v_list_all_elements_are(element_spec), do: {5, :a_all_elements, element_spec, nil}
 
+
+  @doc "Predicate: The list is the empty list `[]`."
   @spec v_list_is_empty() :: term()
   def v_list_is_empty, do: {5, :b_is_empty, nil, nil}
 
+  @doc "Predicate: Applies a nested predicate to the head of a non-empty list."
   @spec v_list_head_pred(term()) :: term()
   def v_list_head_pred(nested_pred_var), do: {5, :c_head, nested_pred_var, nil}
 
+  @doc "Predicate: Applies a nested predicate to the tail of a non-empty list."
   @spec v_list_tail_pred(term()) :: term()
   def v_list_tail_pred(nested_pred_var), do: {5, :d_tail, nested_pred_var, nil}
 end
@@ -629,14 +676,14 @@ defmodule Tdd.Predicate.Info do
     }
   end
 
-  def get_traits({5, :a_all_elements, element_spec, _}) do
-    %{
-      type: :list_recursive_ambient,
-      category: :list,
-      ambient_constraint_spec: element_spec,
-      implies: [{Variable.v_is_list(), true}]
-    }
-  end
+  # def get_traits({5, :a_all_elements, element_spec, _}) do
+  #   %{
+  #     type: :list_recursive_ambient,
+  #     category: :list,
+  #     ambient_constraint_spec: element_spec,
+  #     implies: [{Variable.v_is_list(), true}]
+  #   }
+  # end
 
   def get_traits({5, :b_is_empty, _, _}) do
     %{type: :list_prop, category: :list, implies: [{Variable.v_is_list(), true}]}
@@ -694,6 +741,17 @@ defmodule Tdd.Consistency.Engine do
     do_check(assumptions)
   end
 
+  @doc """
+  Expands a map of assumptions with all their logical implications.
+
+  Returns `{:ok, expanded_map}` or `{:error, :contradiction}`.
+  """
+  @spec expand(map()) :: {:ok, map()} | {:error, :contradiction}
+  def expand(assumptions) do
+    # Just expose the internal helper.
+    expand_with_implications(assumptions)
+  end
+
   # --- The Core Recursive Checker ---
 
   defp do_check(assumptions) do
@@ -729,7 +787,7 @@ defmodule Tdd.Consistency.Engine do
       end
     else
       # `expand_with_implications` or `check_flat_consistency` failed.
-      :error -> :contradiction
+      {:error, _reason} -> :contradiction
     end
   end
 
@@ -770,8 +828,8 @@ defmodule Tdd.Consistency.Engine do
     case Enum.reduce(implications, {:ok, %{}}, fn {implied_var, implied_val}, acc ->
            reduce_implication({implied_var, implied_val}, all_assumptions, acc)
          end) do
-      {:error, :contradiction} ->
-        :error
+      {:error, :contradiction} = err ->
+        err
 
       {:ok, newly_added} when map_size(newly_added) == 0 ->
         {:ok, all_assumptions}
@@ -801,7 +859,7 @@ defmodule Tdd.Consistency.Engine do
          :ok <- check_tuple_consistency(assumptions) do
       :ok
     else
-      :error -> :error
+      :error -> {:error, :consistency_error}
     end
   end
 
@@ -1018,7 +1076,6 @@ defmodule Tdd.Algo do
   @spec simplify(non_neg_integer(), map()) :: non_neg_integer
   def simplify(tdd_id, assumptions \\ %{}) do
     # The main cache uses a sorted list of assumptions for a canonical key.
-    # The internal context set uses this same canonical form.
     sorted_assumptions = Enum.sort(assumptions)
     cache_key = {:simplify, tdd_id, sorted_assumptions}
 
@@ -1288,8 +1345,8 @@ defmodule Tdd.TypeReconstructor do
             {5, :b_is_empty, _, _} -> {:literal, []}
             # --- THIS IS THE FIX ---
             # Correctly reconstruct a list_of spec from the ambient predicate.
-            {5, :a_all_elements, element_spec, _} ->
-              {:list_of, element_spec}
+            # {5, :a_all_elements, element_spec, _} ->
+            #   {:list_of, element_spec}
             # Ignore recursive and ambient vars at this flat level
             _ -> :any
           end
@@ -1384,13 +1441,13 @@ defmodule Tdd.Compiler do
 
         # --- RECURSIVE TYPES ---
         #
-        {:list_of, element_spec} ->
-          id_list = spec_to_id(:list)
-          # The element_spec MUST be normalized to be a canonical part of the variable.
+        # {:list_of, element_spec} ->
+        #   id_list = spec_to_id(:list)
+        #   # The element_spec MUST be normalized to be a canonical part of the variable.
           norm_elem_spec = TypeSpec.normalize(element_spec)
           var = Variable.v_list_all_elements_are(norm_elem_spec)
-          id_check = create_base_type_tdd(var)
-          Algo.apply(:intersect, &op_intersect_terminals/2, id_list, id_check)
+        #   id_check = create_base_type_tdd(var)
+        #   Algo.apply(:intersect, &op_intersect_terminals/2, id_list, id_check)
         {:cons, head_spec, tail_spec} ->
           id_head = spec_to_id(head_spec)
           id_tail = spec_to_id(tail_spec)
@@ -1917,11 +1974,11 @@ defmodule TddVariableTests do
       Variable.v_list_head_pred(Variable.v_is_atom())
     )
 
-    test(
-      "v_list_all_elements_are nests a TypeSpec correctly",
-      {5, :a_all_elements, {:union, [:atom, :integer]}, nil},
-      Variable.v_list_all_elements_are(TypeSpec.normalize({:union, [:integer, :atom]}))
-    )
+    # test(
+    #   "v_list_all_elements_are nests a TypeSpec correctly",
+    #   {5, :a_all_elements, {:union, [:atom, :integer]}, nil},
+    #   Variable.v_list_all_elements_are(TypeSpec.normalize({:union, [:integer, :atom]}))
+    # )
 
     # --- Test Section: Global Ordering ---
     IO.puts("\n--- Section: Global Ordering (Based on Elixir Term Comparison) ---")
@@ -1968,17 +2025,17 @@ defmodule TddVariableTests do
         Variable.v_tuple_elem_pred(0, Variable.v_is_integer())
     )
 
-    IO.inspect(Variable.v_list_all_elements_are(:atom),
-      label: "Variable.v_list_all_elements_are(:atom)"
-    )
+    # IO.inspect(Variable.v_list_all_elements_are(:atom),
+    #   label: "Variable.v_list_all_elements_are(:atom)"
+    # )
 
     IO.inspect(Variable.v_list_is_empty(), label: "Variable.v_list_is_empty()")
 
-    test(
-      "List :a_all_elements var < List :b_is_empty var",
-      true,
-      Variable.v_list_all_elements_are(:atom) < Variable.v_list_is_empty()
-    )
+    # test(
+    #   "List :a_all_elements var < List :b_is_empty var",
+    #   true,
+    #   Variable.v_list_all_elements_are(:atom) < Variable.v_list_is_empty()
+    # )
 
     test(
       "List :b_is_empty var < List :c_head var",