diff --git a/docs/paper/verify-reductions/adversary_naesat_setsplitting.py b/docs/paper/verify-reductions/adversary_naesat_setsplitting.py
new file mode 100644
index 00000000..802a9b74
--- /dev/null
+++ b/docs/paper/verify-reductions/adversary_naesat_setsplitting.py
@@ -0,0 +1,575 @@
+#!/usr/bin/env python3
+"""
+Adversary verification script for NAESatisfiability -> SetSplitting reduction.
+
+Independent implementation based solely on the Typst proof specification.
+Does NOT import or reference verify_naesat_setsplitting.py.
+"""
+
+import itertools
+import random
+import sys
+
+# ---------------------------------------------------------------------------
+# 1. Data structures
+# ---------------------------------------------------------------------------
+
+# NAE-SAT instance: n variables (1..n), clauses are lists of literals.
+# A literal is (var_index, is_positive) where var_index in 1..n.
+# E.g., v_1 -> (1, True), ~v_2 -> (2, False)
+
+# Set Splitting instance: universe_size (int), subsets (list of frozensets of ints)
+
+
+def reduce(n_vars, clauses):
+    """
+    Reduce NAE-SAT to Set Splitting per the Typst proof.
+
+    Universe S = {0, 1, ..., 2n-1} where element 2(i-1) = v_i, 2(i-1)+1 = ~v_i.
+    Subsets:
+      - Complementarity: P_i = {2(i-1), 2(i-1)+1} for i=1..n
+      - Clause: Q_j = {elem for each literal in clause_j}
+    """
+    universe_size = 2 * n_vars
+    subsets = []
+
+    # Complementarity subsets
+    for i in range(1, n_vars + 1):
+        pos_elem = 2 * (i - 1)
+        neg_elem = 2 * (i - 1) + 1
+        subsets.append(frozenset([pos_elem, neg_elem]))
+
+    # Clause subsets
+    for clause in clauses:
+        elems = set()
+        for var_idx, is_positive in clause:
+            if is_positive:
+                elems.add(2 * (var_idx - 1))
+            else:
+                elems.add(2 * (var_idx - 1) + 1)
+        subsets.append(frozenset(elems))
+
+    return universe_size, subsets
+
+
+def literal_to_elem(var_idx, is_positive):
+    """Convert a literal to its universe element index."""
+    if is_positive:
+        return 2 * (var_idx - 1)
+    else:
+        return 2 * (var_idx - 1) + 1
+
+
+def assignment_to_partition(n_vars, assignment):
+    """
+    Convert a boolean assignment (list of n bools, index 0 = var 1) to a partition.
+    Returns S1 as a frozenset. S2 = universe - S1.
+
+    S1 = {v_i : alpha(v_i)=True} union {~v_i : alpha(v_i)=False}
+    """
+    s1 = set()
+    for i in range(n_vars):
+        if assignment[i]:  # var (i+1) is True
+            s1.add(2 * i)      # v_{i+1} in S1
+        else:               # var (i+1) is False
+            s1.add(2 * i + 1)  # ~v_{i+1} in S1
+    return frozenset(s1)
+
+
+def partition_to_assignment(n_vars, s1):
+    """
+    Extract NAE-SAT assignment from a set splitting partition.
+    alpha(v_i) = True iff element 2(i-1) in S1.
+    """
+    assignment = []
+    for i in range(n_vars):
+        assignment.append(2 * i in s1)
+    return assignment
+
+
+def is_nae_satisfying(n_vars, clauses, assignment):
+    """Check if assignment NAE-satisfies all clauses."""
+    for clause in clauses:
+        values = set()
+        for var_idx, is_positive in clause:
+            val = assignment[var_idx - 1]
+            if not is_positive:
+                val = not val
+            values.add(val)
+        if len(values) < 2:  # all equal
+            return False
+    return True
+
+
+def is_valid_splitting(universe_size, subsets, s1):
+    """Check if partition (S1, S2) splits every subset."""
+    s2 = set(range(universe_size)) - set(s1)
+    for subset in subsets:
+        if not (subset & s1) or not (subset & s2):
+            return False
+    return True
+
+
+def is_consistent_partition(n_vars, s1):
+    """
+    Check that the partition is consistent with complementarity constraints:
+    for each variable i, exactly one of {2(i-1), 2(i-1)+1} is in S1.
+    """
+    for i in range(n_vars):
+        pos = 2 * i
+        neg = 2 * i + 1
+        in_s1_pos = pos in s1
+        in_s1_neg = neg in s1
+        if in_s1_pos == in_s1_neg:  # both in or both out
+            return False
+    return True
+
+
+# ---------------------------------------------------------------------------
+# 2. Test functions
+# ---------------------------------------------------------------------------
+
+passed = 0
+failed = 0
+bugs = []
+
+
+def check(condition, msg):
+    global passed, failed, bugs
+    if condition:
+        passed += 1
+    else:
+        failed += 1
+        if msg not in bugs:
+            bugs.append(msg)
+
+
+def test_yes_example():
+    """Reproduce the YES example from the Typst proof."""
+    global passed, failed
+    n = 4
+    # c1=(v1,v2,v3), c2=(~v1,v3,v4), c3=(v2,~v3,~v4), c4=(v1,~v2,v4)
+    clauses = [
+        [(1, True), (2, True), (3, True)],
+        [(1, False), (3, True), (4, True)],
+        [(2, True), (3, False), (4, False)],
+        [(1, True), (2, False), (4, True)],
+    ]
+    universe_size, subsets = reduce(n, clauses)
+
+    # Check overhead
+    check(universe_size == 8, "YES: universe_size should be 8")
+    check(len(subsets) == 8, "YES: num_subsets should be 8")
+
+    # Check specific subsets (0-indexed from proof)
+    expected_subsets = [
+        frozenset([0, 1]), frozenset([2, 3]), frozenset([4, 5]), frozenset([6, 7]),
+        frozenset([0, 2, 4]), frozenset([1, 4, 6]), frozenset([2, 5, 7]), frozenset([0, 3, 6]),
+    ]
+    for i, (got, exp) in enumerate(zip(subsets, expected_subsets)):
+        check(got == exp, f"YES: subset {i} mismatch: got {got}, expected {exp}")
+
+    # Assignment: v1=T, v2=F, v3=T, v4=F
+    assignment = [True, False, True, False]
+    check(is_nae_satisfying(n, clauses, assignment), "YES: assignment should NAE-satisfy")
+
+    s1 = assignment_to_partition(n, assignment)
+    expected_s1 = frozenset([0, 3, 4, 7])
+    check(s1 == expected_s1, f"YES: S1 should be {{0,3,4,7}}, got {s1}")
+
+    check(is_valid_splitting(universe_size, subsets, s1), "YES: partition should be valid splitting")
+
+    # Extract back
+    recovered = partition_to_assignment(n, s1)
+    check(recovered == assignment, "YES: extracted assignment should match original")
+
+
+def test_no_example():
+    """Reproduce the NO example from the Typst proof."""
+    n = 3
+    clauses = [
+        [(1, True), (2, True), (3, True)],
+        [(1, True), (2, True), (3, False)],
+        [(1, True), (2, False), (3, True)],
+        [(1, True), (2, False), (3, False)],
+    ]
+    universe_size, subsets = reduce(n, clauses)
+
+    check(universe_size == 6, "NO: universe_size should be 6")
+    check(len(subsets) == 7, "NO: num_subsets should be 7")
+
+    expected_subsets = [
+        frozenset([0, 1]), frozenset([2, 3]), frozenset([4, 5]),
+        frozenset([0, 2, 4]), frozenset([0, 2, 5]),
+        frozenset([0, 3, 4]), frozenset([0, 3, 5]),
+    ]
+    for i, (got, exp) in enumerate(zip(subsets, expected_subsets)):
+        check(got == exp, f"NO: subset {i} mismatch: got {got}, expected {exp}")
+
+    # Verify no assignment works
+    for bits in itertools.product([False, True], repeat=n):
+        assignment = list(bits)
+        check(not is_nae_satisfying(n, clauses, assignment),
+              f"NO: assignment {assignment} should NOT NAE-satisfy")
+
+    # Verify no consistent partition works
+    for bits in itertools.product([0, 1], repeat=2 * n):
+        s1 = frozenset(i for i, b in enumerate(bits) if b == 0)
+        if is_consistent_partition(n, s1):
+            check(not is_valid_splitting(universe_size, subsets, s1),
+                  f"NO: consistent partition {s1} should not be valid splitting")
+
+
+def test_exhaustive_small():
+    """Exhaustive testing for all NAE-SAT instances with n <= 5 variables."""
+    # For small n, generate many clause patterns and verify equivalence
+    for n in range(1, 6):
+        vars_list = list(range(1, n + 1))
+        # Generate all possible literals
+        all_literals = []
+        for v in vars_list:
+            all_literals.append((v, True))
+            all_literals.append((v, False))
+
+        # For n<=3, test all possible single-clause instances with 2-3 literals
+        if n <= 3:
+            clause_sizes = [2, 3] if n >= 2 else [2]
+            for size in clause_sizes:
+                for combo in itertools.combinations(all_literals, size):
+                    # Skip clauses with both v_i and ~v_i (tautological for NAE purposes)
+                    clause = list(combo)
+                    clauses = [clause]
+                    verify_reduction_equivalence(n, clauses)
+
+        # For all n, test random instances
+        rng = random.Random(42 + n)
+        num_random = 200 if n <= 3 else 100
+        for _ in range(num_random):
+            m = rng.randint(1, min(n * 2, 8))
+            clauses = []
+            for _ in range(m):
+                clause_size = rng.randint(2, min(len(all_literals), 4))
+                clause = rng.sample(all_literals, clause_size)
+                clauses.append(clause)
+            verify_reduction_equivalence(n, clauses)
+
+
+def verify_reduction_equivalence(n_vars, clauses):
+    """
+    Core verification: NAE-SAT instance is feasible iff the reduced
+    Set Splitting instance is feasible. Also checks solution extraction.
+    """
+    universe_size, subsets = reduce(n_vars, clauses)
+
+    # Check overhead formula
+    check(universe_size == 2 * n_vars,
+          f"Overhead: universe_size should be 2*{n_vars}={2*n_vars}, got {universe_size}")
+    check(len(subsets) == n_vars + len(clauses),
+          f"Overhead: num_subsets should be {n_vars}+{len(clauses)}, got {len(subsets)}")
+
+    # Enumerate all assignments for NAE-SAT
+    nae_feasible = False
+    nae_witnesses = []
+    for bits in itertools.product([False, True], repeat=n_vars):
+        assignment = list(bits)
+        if is_nae_satisfying(n_vars, clauses, assignment):
+            nae_feasible = True
+            nae_witnesses.append(assignment)
+
+    # Enumerate all valid splittings (consistent partitions only)
+    ss_feasible = False
+    ss_witnesses = []
+    for bits in itertools.product([0, 1], repeat=n_vars):
+        # Build consistent partition: for each var, bit=0 means v_i in S1
+        s1 = set()
+        for i in range(n_vars):
+            if bits[i] == 0:
+                s1.add(2 * i)       # v_{i+1} in S1
+            else:
+                s1.add(2 * i + 1)   # ~v_{i+1} in S1
+        # Complete s1: the complement elements go to S2
+        for i in range(n_vars):
+            if 2 * i not in s1:
+                s1.add(2 * i + 1)
+            if 2 * i + 1 not in s1:
+                pass  # already not in s1
+        # Actually, rebuild properly
+        s1 = set()
+        for i in range(n_vars):
+            if bits[i] == 0:
+                s1.add(2 * i)
+            else:
+                s1.add(2 * i + 1)
+        s1 = frozenset(s1)
+
+        if is_valid_splitting(universe_size, subsets, s1):
+            ss_feasible = True
+            ss_witnesses.append(s1)
+
+    # Equivalence
+    check(nae_feasible == ss_feasible,
+          f"Equivalence failed for n={n_vars}, clauses={clauses}: NAE={nae_feasible}, SS={ss_feasible}")
+
+    # Forward direction: every NAE witness maps to a valid splitting
+    for assignment in nae_witnesses:
+        s1 = assignment_to_partition(n_vars, assignment)
+        check(is_valid_splitting(universe_size, subsets, s1),
+              f"Forward: NAE assignment {assignment} -> partition not valid")
+
+    # Backward direction: every valid splitting maps to NAE assignment
+    for s1 in ss_witnesses:
+        assignment = partition_to_assignment(n_vars, s1)
+        check(is_nae_satisfying(n_vars, clauses, assignment),
+              f"Backward: partition {s1} -> assignment {assignment} not NAE-satisfying")
+
+    # Solution extraction roundtrip
+    for assignment in nae_witnesses:
+        s1 = assignment_to_partition(n_vars, assignment)
+        recovered = partition_to_assignment(n_vars, s1)
+        check(recovered == assignment,
+              f"Roundtrip: assignment {assignment} != recovered {recovered}")
+
+
+def test_overhead_formula():
+    """Verify overhead formula on many random instances."""
+    rng = random.Random(12345)
+    for _ in range(500):
+        n = rng.randint(1, 10)
+        m = rng.randint(1, 15)
+        all_literals = [(v, p) for v in range(1, n + 1) for p in [True, False]]
+        clauses = []
+        for _ in range(m):
+            size = rng.randint(2, min(len(all_literals), 5))
+            clause = rng.sample(all_literals, size)
+            clauses.append(clause)
+
+        universe_size, subsets = reduce(n, clauses)
+        check(universe_size == 2 * n,
+              f"Overhead: universe_size={universe_size} != 2*{n}")
+        check(len(subsets) == n + m,
+              f"Overhead: num_subsets={len(subsets)} != {n}+{m}")
+
+
+def test_complementarity_always_split():
+    """Every consistent partition always splits complementarity subsets."""
+    rng = random.Random(99999)
+    for _ in range(500):
+        n = rng.randint(1, 8)
+        # Any assignment -> partition must split all complementarity subsets
+        assignment = [rng.choice([True, False]) for _ in range(n)]
+        s1 = assignment_to_partition(n, assignment)
+        for i in range(n):
+            p_i = frozenset([2 * i, 2 * i + 1])
+            check(bool(p_i & s1) and bool(p_i - s1),
+                  f"Complementarity: P_{i+1} not split by assignment {assignment}")
+
+
+def test_nae_symmetry():
+    """
+    NAE-SAT has the property that if alpha is NAE-satisfying, so is ~alpha
+    (flipping all variables). Verify this is preserved through reduction.
+    """
+    rng = random.Random(77777)
+    for _ in range(500):
+        n = rng.randint(2, 6)
+        m = rng.randint(1, 8)
+        all_literals = [(v, p) for v in range(1, n + 1) for p in [True, False]]
+        clauses = []
+        for _ in range(m):
+            size = rng.randint(2, min(len(all_literals), 4))
+            clause = rng.sample(all_literals, size)
+            clauses.append(clause)
+
+        universe_size, subsets = reduce(n, clauses)
+
+        assignment = [rng.choice([True, False]) for _ in range(n)]
+        flipped = [not a for a in assignment]
+
+        nae_orig = is_nae_satisfying(n, clauses, assignment)
+        nae_flip = is_nae_satisfying(n, clauses, flipped)
+        check(nae_orig == nae_flip,
+              f"NAE symmetry: original={nae_orig}, flipped={nae_flip}")
+
+        # Also check that the corresponding partitions are complements
+        s1_orig = assignment_to_partition(n, assignment)
+        s1_flip = assignment_to_partition(n, flipped)
+        universe = frozenset(range(universe_size))
+        check(s1_orig | s1_flip == universe,
+              f"Partition symmetry: union != universe")
+        check(not (s1_orig & s1_flip),
+              f"Partition symmetry: non-empty intersection")
+
+        # Both partitions should give same splitting result
+        ss_orig = is_valid_splitting(universe_size, subsets, s1_orig)
+        ss_flip = is_valid_splitting(universe_size, subsets, s1_flip)
+        check(ss_orig == ss_flip,
+              f"Splitting symmetry: orig={ss_orig}, flip={ss_flip}")
+
+
+def test_single_clause_edge_cases():
+    """Test edge cases: single clause with all positive, all negative, mixed."""
+    for n in range(2, 6):
+        # All positive: (v1, v2, ..., vn) — NAE-sat iff not all same
+        clause_all_pos = [(i, True) for i in range(1, n + 1)]
+        verify_reduction_equivalence(n, [clause_all_pos])
+
+        # All negative: (~v1, ~v2, ..., ~vn)
+        clause_all_neg = [(i, False) for i in range(1, n + 1)]
+        verify_reduction_equivalence(n, [clause_all_neg])
+
+        # Mixed: (v1, ~v2, v3, ~v4, ...)
+        clause_mixed = [(i, i % 2 == 1) for i in range(1, n + 1)]
+        verify_reduction_equivalence(n, [clause_mixed])
+
+
+def test_two_literal_clauses():
+    """2-literal clauses are the minimum for NAE-SAT. Test systematically."""
+    for n in range(2, 5):
+        all_literals = [(v, p) for v in range(1, n + 1) for p in [True, False]]
+        for l1, l2 in itertools.combinations(all_literals, 2):
+            verify_reduction_equivalence(n, [[l1, l2]])
+
+
+# ---------------------------------------------------------------------------
+# 3. Hypothesis property-based tests
+# ---------------------------------------------------------------------------
+
+try:
+    from hypothesis import given, settings, assume
+    from hypothesis import strategies as st
+    HAS_HYPOTHESIS = True
+except ImportError:
+    HAS_HYPOTHESIS = False
+
+if HAS_HYPOTHESIS:
+    @given(st.lists(st.booleans(), min_size=2, max_size=8))
+    @settings(max_examples=500)
+    def test_roundtrip_hypothesis(assignment):
+        """Forward-backward roundtrip for random assignments."""
+        global passed, failed
+        n = len(assignment)
+        # Create a single clause that this assignment NAE-satisfies
+        # (v1, ~v2) if assignment has at least one T and one F
+        if all(assignment) or not any(assignment):
+            # All same -> can't NAE-satisfy any clause with all same polarity
+            # Just test overhead
+            clauses = [[(1, True), (2, True)]]
+            universe_size, subsets = reduce(n, clauses)
+            check(universe_size == 2 * n, "Hypothesis roundtrip: overhead")
+            return
+
+        # Build clause from first True and first False literal
+        true_idx = assignment.index(True) + 1
+        false_idx = assignment.index(False) + 1
+        clauses = [[(true_idx, True), (false_idx, True)]]
+
+        universe_size, subsets = reduce(n, clauses)
+        s1 = assignment_to_partition(n, assignment)
+        check(is_valid_splitting(universe_size, subsets, s1),
+              "Hypothesis roundtrip: partition should be valid")
+        recovered = partition_to_assignment(n, s1)
+        check(recovered == assignment,
+              "Hypothesis roundtrip: recovered != original")
+
+    @given(
+        st.integers(min_value=2, max_value=6),
+        st.lists(
+            st.lists(
+                st.tuples(st.integers(min_value=1, max_value=6), st.booleans()),
+                min_size=2, max_size=5
+            ),
+            min_size=1, max_size=6
+        )
+    )
+    @settings(max_examples=500)
+    def test_equivalence_hypothesis(n, raw_clauses):
+        """Equivalence check on random instances from hypothesis."""
+        # Filter literals to valid range
+        clauses = []
+        for raw_clause in raw_clauses:
+            clause = [(v, p) for v, p in raw_clause if 1 <= v <= n]
+            # Deduplicate
+            clause = list(set(clause))
+            if len(clause) >= 2:
+                clauses.append(clause)
+        assume(len(clauses) >= 1)
+
+        verify_reduction_equivalence(n, clauses)
+
+    @given(
+        st.integers(min_value=2, max_value=5),
+        st.integers(min_value=1, max_value=4),
+    )
+    @settings(max_examples=500)
+    def test_unsatisfiable_pattern_hypothesis(n, k):
+        """
+        Test patterns likely to be unsatisfiable:
+        For a single variable v1, add clauses with all combinations of other vars.
+        """
+        assume(n >= 2)
+        # Create clauses: (v1, ...) with all combinations of signs for vars 2..min(n,k+1)
+        other_vars = list(range(2, min(n, k + 1) + 1))
+        assume(len(other_vars) >= 1)
+        clauses = []
+        for signs in itertools.product([True, False], repeat=len(other_vars)):
+            clause = [(1, True)] + [(other_vars[i], signs[i]) for i in range(len(other_vars))]
+            clauses.append(clause)
+        verify_reduction_equivalence(n, clauses)
+
+
+# ---------------------------------------------------------------------------
+# 4. Run all tests
+# ---------------------------------------------------------------------------
+
+def main():
+    global passed, failed, bugs
+
+    print("Running YES example test...")
+    test_yes_example()
+
+    print("Running NO example test...")
+    test_no_example()
+
+    print("Running exhaustive small instances test...")
+    test_exhaustive_small()
+
+    print("Running overhead formula test...")
+    test_overhead_formula()
+
+    print("Running complementarity test...")
+    test_complementarity_always_split()
+
+    print("Running NAE symmetry test...")
+    test_nae_symmetry()
+
+    print("Running single clause edge cases test...")
+    test_single_clause_edge_cases()
+
+    print("Running two literal clauses test...")
+    test_two_literal_clauses()
+
+    if HAS_HYPOTHESIS:
+        print("Running hypothesis roundtrip test...")
+        test_roundtrip_hypothesis()
+
+        print("Running hypothesis equivalence test...")
+        test_equivalence_hypothesis()
+
+        print("Running hypothesis unsatisfiable pattern test...")
+        test_unsatisfiable_pattern_hypothesis()
+    else:
+        print("WARNING: hypothesis not installed, skipping property-based tests")
+
+    total = passed + failed
+    print(f"\nTotal checks: {total}")
+    print(f"ADVERSARY: NAESatisfiability -> SetSplitting: {passed} passed, {failed} failed")
+    if bugs:
+        print(f"BUGS FOUND: {bugs}")
+    else:
+        print("BUGS FOUND: none")
+
+    return 0 if failed == 0 else 1
+
+
+if __name__ == "__main__":
+    sys.exit(main())
diff --git a/docs/paper/verify-reductions/cross_compare_naesat_setsplitting.py b/docs/paper/verify-reductions/cross_compare_naesat_setsplitting.py
new file mode 100644
index 00000000..6b27b127
--- /dev/null
+++ b/docs/paper/verify-reductions/cross_compare_naesat_setsplitting.py
@@ -0,0 +1,116 @@
+#!/usr/bin/env python3
+"""Cross-compare constructor and adversary implementations for NAESatisfiability → SetSplitting."""
+import itertools
+import sys
+sys.path.insert(0, "docs/paper/verify-reductions")
+
+from verify_naesat_setsplitting import (
+    reduce as constructor_reduce,
+    is_feasible_source as c_is_feasible_source,
+    is_feasible_target as c_is_feasible_target,
+    is_nae_satisfying as c_is_nae_satisfying,
+    extract_assignment as c_extract_assignment,
+    is_set_splitting as c_is_set_splitting,
+)
+from adversary_naesat_setsplitting import (
+    reduce as adversary_reduce_raw,
+    is_nae_satisfying as a_is_nae_satisfying_raw,
+    is_valid_splitting as a_is_valid_splitting_raw,
+    partition_to_assignment as a_partition_to_assignment,
+)
+
+agree = disagree = 0
+feasibility_mismatch = 0
+
+
+def signed_to_tuple(clause):
+    """Convert signed literal list to (var_idx, is_positive) tuple list."""
+    return [(abs(lit), lit > 0) for lit in clause]
+
+
+def adversary_reduce(n, clauses):
+    """Adapter: convert signed-literal clauses to adversary format and reduce."""
+    a_clauses = [signed_to_tuple(c) for c in clauses]
+    u_size, subsets = adversary_reduce_raw(n, a_clauses)
+    # Convert frozensets to sorted lists for comparison
+    return u_size, [sorted(s) for s in subsets]
+
+
+def generate_all_valid_clauses(n):
+    """Generate all valid 2- and 3-literal NAE-SAT clauses for n variables."""
+    lits = list(range(1, n + 1)) + list(range(-n, 0))
+    clauses = []
+    for size in [2, 3]:
+        for combo in itertools.combinations(lits, size):
+            vars_used = [abs(l) for l in combo]
+            if len(set(vars_used)) == len(vars_used):
+                clauses.append(list(combo))
+    return clauses
+
+
+def normalize_subsets(universe_size, subsets):
+    """Normalize subsets to a canonical form for comparison."""
+    return (universe_size, tuple(tuple(sorted(s)) for s in sorted(subsets, key=lambda x: tuple(sorted(x)))))
+
+
+for n in range(2, 6):
+    all_clauses = generate_all_valid_clauses(n)
+    instances_tested = 0
+    max_instances = 200
+
+    for num_cl in [1, 2, 3, 4]:
+        for combo in itertools.combinations(range(len(all_clauses)), num_cl):
+            if instances_tested >= max_instances:
+                break
+            clauses = [all_clauses[i] for i in combo]
+
+            # Run both reductions
+            c_usize, c_subsets = constructor_reduce(n, clauses)
+            a_usize, a_subsets = adversary_reduce(n, clauses)
+
+            # Compare structural equivalence
+            c_norm = normalize_subsets(c_usize, c_subsets)
+            a_norm = normalize_subsets(a_usize, a_subsets)
+
+            if c_norm == a_norm:
+                agree += 1
+            else:
+                disagree += 1
+                print(f"  DISAGREE on n={n}, clauses={clauses}")
+                print(f"    Constructor: u={c_usize}, subsets={c_subsets}")
+                print(f"    Adversary:   u={a_usize}, subsets={a_subsets}")
+
+            # Compare source feasibility
+            c_feas = c_is_feasible_source(n, clauses)
+            a_clauses_tuples = [signed_to_tuple(c) for c in clauses]
+            a_feas = any(
+                a_is_nae_satisfying_raw(n, a_clauses_tuples, [(bits >> i) & 1 for i in range(n)])
+                for bits in range(2**n)
+            )
+
+            if c_feas != a_feas:
+                feasibility_mismatch += 1
+                print(f"  SOURCE FEASIBILITY MISMATCH on n={n}, clauses={clauses}: "
+                      f"constructor={c_feas}, adversary={a_feas}")
+
+            # Compare target feasibility via constructor's format
+            c_t_feas = c_is_feasible_target(c_usize, c_subsets)
+            # For adversary, check target via constructor's validator on constructor's output
+            # (since both should produce the same target, this checks structural agreement)
+            if c_norm == a_norm and c_feas != c_t_feas:
+                # This would mean the reduction is wrong
+                feasibility_mismatch += 1
+                print(f"  REDUCTION CONSISTENCY MISMATCH: source={c_feas}, target={c_t_feas}")
+
+            instances_tested += 1
+
+    print(f"n={n}: tested {instances_tested} instances")
+
+print(f"\nCross-comparison: {agree} agree, {disagree} disagree, "
+      f"{feasibility_mismatch} feasibility mismatches")
+if disagree > 0 or feasibility_mismatch > 0:
+    print("ACTION REQUIRED: investigate discrepancies before proceeding")
+    sys.exit(1)
+else:
+    print("All instances agree between constructor and adversary.")
+    sys.exit(0)
diff --git a/docs/paper/verify-reductions/naesat_setsplitting.pdf b/docs/paper/verify-reductions/naesat_setsplitting.pdf
new file mode 100644
index 00000000..0cf0188c
Binary files /dev/null and b/docs/paper/verify-reductions/naesat_setsplitting.pdf differ
diff --git a/docs/paper/verify-reductions/naesat_setsplitting.typ b/docs/paper/verify-reductions/naesat_setsplitting.typ
new file mode 100644
index 00000000..06bf7dee
--- /dev/null
+++ b/docs/paper/verify-reductions/naesat_setsplitting.typ
@@ -0,0 +1,173 @@
+// Verification proof: NAESatisfiability → SetSplitting (#841)
+#import "@preview/ctheorems:1.1.3": thmbox, thmplain, thmproof, thmrules
+
+#set page(paper: "a4", margin: (x: 2cm, y: 2.5cm))
+#set text(font: "New Computer Modern", size: 10pt)
+#set par(justify: true)
+#set heading(numbering: "1.1")
+
+#show: thmrules.with(qed-symbol: $square$)
+#let theorem = thmbox("theorem", "Theorem", fill: rgb("#e8e8f8"))
+#let proof = thmproof("proof", "Proof")
+
+== NAE Satisfiability $arrow.r$ Set Splitting <sec:naesat-setsplitting>
+
+#theorem[
+  NAE Satisfiability is polynomial-time reducible to Set Splitting.
+  Given a NAE-SAT instance with $n$ variables and $m$ clauses, the
+  constructed Set Splitting instance has universe size $2n$ and $m + n$
+  subsets.
+] <thm:naesat-setsplitting>
+
+#proof[
+  _Construction._
+  Let $phi$ be a NAE-SAT instance with variables $V = {v_1, dots, v_n}$ and
+  clauses $C = {c_1, dots, c_m}$, where each clause $c_j$ contains at least
+  two literals drawn from ${v_1, overline(v)_1, dots, v_n, overline(v)_n}$.
+
+  Construct a Set Splitting instance $(S, cal(C))$ as follows.
+
+  + Define the universe $S = {v_1, overline(v)_1, v_2, overline(v)_2, dots, v_n, overline(v)_n}$,
+    so $|S| = 2n$. Element $v_i$ represents the positive literal of
+    variable $i$, and element $overline(v)_i$ represents its negation.
+
+  + For each variable $v_i$ ($1 <= i <= n$), add a _complementarity subset_
+    $P_i = {v_i, overline(v)_i}$ to the collection $cal(C)$.
+
+  + For each clause $c_j = (ell_(j,1), dots, ell_(j,k_j))$ ($1 <= j <= m$),
+    add the _clause subset_ $Q_j = {ell_(j,1), dots, ell_(j,k_j)}$ to the
+    collection $cal(C)$, where each literal $ell_(j,t)$ is identified with
+    the corresponding element in $S$: a positive literal $v_i$ maps to
+    element $v_i$, and a negative literal $overline(v)_i$ maps to
+    element $overline(v)_i$.
+
+  The collection is $cal(C) = {P_1, dots, P_n, Q_1, dots, Q_m}$, giving
+  $|cal(C)| = n + m$ subsets in total.
+
+  _Correctness._
+
+  ($arrow.r.double$) Suppose $alpha: V -> {"true", "false"}$ is a NAE-satisfying
+  assignment for $phi$. Define a partition $(S_1, S_2)$ of $S$ by:
+  $ S_1 = {v_i : alpha(v_i) = "true"} union {overline(v)_i : alpha(v_i) = "false"}, $
+  $ S_2 = {v_i : alpha(v_i) = "false"} union {overline(v)_i : alpha(v_i) = "true"}. $
+  We verify that every subset in $cal(C)$ is split:
+  - _Complementarity subsets:_ For each $P_i = {v_i, overline(v)_i}$,
+    exactly one of $v_i, overline(v)_i$ is in $S_1$ and the other is in $S_2$
+    by construction. Hence $P_i$ is split.
+  - _Clause subsets:_ For each $Q_j$, since $alpha$ is NAE-satisfying,
+    clause $c_j$ contains at least one true literal $ell_t$ and at least one
+    false literal $ell_f$. The element corresponding to a true literal is in
+    $S_1$: for a positive literal $v_i$, truth means $alpha(v_i) = "true"$,
+    so $v_i in S_1$; for a negative literal $overline(v)_i$, truth means
+    $alpha(v_i) = "false"$, so $overline(v)_i in S_1$. By the same
+    reasoning, the element corresponding to a false literal is in $S_2$.
+    Hence $Q_j$ has at least one element in each part and is split.
+
+  ($arrow.l.double$) Suppose $(S_1, S_2)$ is a valid set splitting for
+  $(S, cal(C))$. Define the assignment $alpha$ by:
+  $ alpha(v_i) = cases("true" &"if" v_i in S_1, "false" &"if" v_i in S_2.) $
+  This is well-defined because the complementarity subset $P_i = {v_i, overline(v)_i}$
+  must be split, so exactly one of $v_i, overline(v)_i$ is in $S_1$ and the
+  other is in $S_2$. In particular, $overline(v)_i in S_1$ if and only if
+  $alpha(v_i) = "false"$.
+
+  We verify that $alpha$ is NAE-satisfying. Consider any clause
+  $c_j = (ell_(j,1), dots, ell_(j,k_j))$ with corresponding subset $Q_j$.
+  Since $Q_j$ is split, there exist elements $ell_a in Q_j sect S_1$ and
+  $ell_b in Q_j sect S_2$.
+  - If $ell_a = v_i$ for some $i$, then $v_i in S_1$, so
+    $alpha(v_i) = "true"$, and the literal $v_i$ evaluates to true.
+  - If $ell_a = overline(v)_i$ for some $i$, then $overline(v)_i in S_1$.
+    Since $P_i$ is split, $v_i in S_2$, so $alpha(v_i) = "false"$, and the
+    literal $overline(v)_i$ evaluates to true.
+  By the same reasoning applied to $ell_b in S_2$, literal $ell_b$ evaluates
+  to false. Hence clause $c_j$ has both a true and a false literal,
+  satisfying the NAE condition.
+
+  _Solution extraction._
+  Given a set splitting $(S_1, S_2)$, extract the NAE-satisfying assignment
+  by setting $alpha(v_i) = "true"$ if and only if $v_i in S_1$.
+  In the binary encoding used by the codebase, the universe has $2n$
+  elements indexed $0, 1, dots, 2n - 1$, where element $2(i - 1)$
+  represents $v_i$ and element $2(i - 1) + 1$ represents $overline(v)_i$.
+  A configuration assigns each element to part 0 ($S_1$) or part 1 ($S_2$).
+  Variable $i$ is set to true when element $2(i - 1)$ is in part 0.
+]
+
+*Overhead.*
+#table(
+  columns: (auto, auto),
+  align: (left, left),
+  table.header([Target metric], [Formula]),
+  [`universe_size`], [$2n$ where $n =$ `num_vars`],
+  [`num_subsets`], [$n + m$ where $m =$ `num_clauses`],
+)
+
+*Feasible example (YES instance).*
+Consider the NAE-SAT instance with $n = 4$ variables and $m = 4$ clauses:
+$ c_1 = (v_1, v_2, v_3), quad c_2 = (overline(v)_1, v_3, v_4), quad c_3 = (v_2, overline(v)_3, overline(v)_4), quad c_4 = (v_1, overline(v)_2, v_4). $
+
+The constructed Set Splitting instance has universe size $2 dot 4 = 8$ and
+$4 + 4 = 8$ subsets:
+- Complementarity: $P_1 = {v_1, overline(v)_1}$, $P_2 = {v_2, overline(v)_2}$,
+  $P_3 = {v_3, overline(v)_3}$, $P_4 = {v_4, overline(v)_4}$.
+- Clause: $Q_1 = {v_1, v_2, v_3}$, $Q_2 = {overline(v)_1, v_3, v_4}$,
+  $Q_3 = {v_2, overline(v)_3, overline(v)_4}$, $Q_4 = {v_1, overline(v)_2, v_4}$.
+
+Using 0-indexed elements: $v_i$ is element $2(i-1)$ and $overline(v)_i$ is
+element $2(i-1)+1$, so $v_1 = 0, overline(v)_1 = 1, v_2 = 2, overline(v)_2 = 3,
+v_3 = 4, overline(v)_3 = 5, v_4 = 6, overline(v)_4 = 7$.
+
+Subsets (0-indexed): ${0,1}, {2,3}, {4,5}, {6,7}, {0,2,4}, {1,4,6}, {2,5,7}, {0,3,6}$.
+
+The assignment $alpha = (v_1 = "true", v_2 = "false", v_3 = "true", v_4 = "false")$ is NAE-satisfying:
+- $c_1 = (v_1, v_2, v_3) = ("T", "F", "T")$: not all equal $checkmark$
+- $c_2 = (overline(v)_1, v_3, v_4) = ("F", "T", "F")$: not all equal $checkmark$
+- $c_3 = (v_2, overline(v)_3, overline(v)_4) = ("F", "F", "T")$: not all equal $checkmark$
+- $c_4 = (v_1, overline(v)_2, v_4) = ("T", "T", "F")$: not all equal $checkmark$
+
+The corresponding partition is:
+$S_1 = {v_1, overline(v)_2, v_3, overline(v)_4} = {0, 3, 4, 7}$,
+$S_2 = {overline(v)_1, v_2, overline(v)_3, v_4} = {1, 2, 5, 6}$.
+
+Verification that every subset is split:
+- $P_1 = {0, 1}$: $0 in S_1$, $1 in S_2$ $checkmark$
+- $P_2 = {2, 3}$: $3 in S_1$, $2 in S_2$ $checkmark$
+- $P_3 = {4, 5}$: $4 in S_1$, $5 in S_2$ $checkmark$
+- $P_4 = {6, 7}$: $7 in S_1$, $6 in S_2$ $checkmark$
+- $Q_1 = {0, 2, 4}$: $0 in S_1$, $2 in S_2$ $checkmark$
+- $Q_2 = {1, 4, 6}$: $4 in S_1$, $1 in S_2$ $checkmark$
+- $Q_3 = {2, 5, 7}$: $7 in S_1$, $2 in S_2$ $checkmark$
+- $Q_4 = {0, 3, 6}$: $0 in S_1$, $6 in S_2$ $checkmark$
+
+*Infeasible example (NO instance).*
+Consider the NAE-SAT instance with $n = 3$ variables and $m = 4$ clauses:
+$ c_1 = (v_1, v_2, v_3), quad c_2 = (v_1, v_2, overline(v)_3), quad c_3 = (v_1, overline(v)_2, v_3), quad c_4 = (v_1, overline(v)_2, overline(v)_3). $
+
+The constructed Set Splitting instance has universe size $2 dot 3 = 6$ and
+$3 + 4 = 7$ subsets:
+- Complementarity: $P_1 = {v_1, overline(v)_1}$, $P_2 = {v_2, overline(v)_2}$,
+  $P_3 = {v_3, overline(v)_3}$.
+- Clause: $Q_1 = {v_1, v_2, v_3}$, $Q_2 = {v_1, v_2, overline(v)_3}$,
+  $Q_3 = {v_1, overline(v)_2, v_3}$, $Q_4 = {v_1, overline(v)_2, overline(v)_3}$.
+
+Using 0-indexed elements: $v_1 = 0, overline(v)_1 = 1, v_2 = 2, overline(v)_2 = 3,
+v_3 = 4, overline(v)_3 = 5$.
+
+Subsets (0-indexed): ${0,1}, {2,3}, {4,5}, {0,2,4}, {0,2,5}, {0,3,4}, {0,3,5}$.
+
+This instance is unsatisfiable. The complementarity subsets force a consistent
+assignment. Each of the $2^3 = 8$ possible assignments violates at least one
+clause:
+- $alpha = ("T","T","T")$: $c_1 = ("T","T","T")$ — all equal, fails.
+- $alpha = ("T","T","F")$: $c_2 = ("T","T","T")$ — all equal, fails.
+- $alpha = ("T","F","T")$: $c_3 = ("T","T","T")$ — all equal, fails.
+- $alpha = ("T","F","F")$: $c_4 = ("T","T","T")$ — all equal, fails.
+- $alpha = ("F","T","T")$: $c_1 = ("F","T","T")$ NAE $checkmark$, $c_2 = ("F","T","F")$ NAE $checkmark$, $c_3 = ("F","F","T")$ NAE $checkmark$, $c_4 = ("F","F","F")$ — all equal, fails.
+- $alpha = ("F","T","F")$: $c_4 = ("F","F","T")$ NAE $checkmark$, $c_1 = ("F","T","F")$ NAE $checkmark$, $c_2 = ("F","T","T")$ NAE $checkmark$, $c_3 = ("F","F","F")$ — all equal, fails.
+- $alpha = ("F","F","T")$: $c_3 = ("F","T","T")$ NAE $checkmark$, $c_1 = ("F","F","T")$ NAE $checkmark$, $c_2 = ("F","F","F")$ — all equal, fails.
+- $alpha = ("F","F","F")$: $c_1 = ("F","F","F")$ — all equal, fails.
+
+Since no assignment is NAE-satisfying, the corresponding Set Splitting instance
+also has no valid partition: by the backward direction of the proof, any valid
+partition would yield a NAE-satisfying assignment, which does not exist.
diff --git a/docs/paper/verify-reductions/verify_naesat_setsplitting.py b/docs/paper/verify-reductions/verify_naesat_setsplitting.py
new file mode 100644
index 00000000..01f7bb1e
--- /dev/null
+++ b/docs/paper/verify-reductions/verify_naesat_setsplitting.py
@@ -0,0 +1,461 @@
+#!/usr/bin/env python3
+"""§1.1 NAESatisfiability → SetSplitting (#841): exhaustive + structural verification."""
+import itertools
+import sys
+from sympy import symbols, simplify, Eq
+
+passed = failed = 0
+
+
+def check(condition, msg=""):
+    global passed, failed
+    if condition:
+        passed += 1
+    else:
+        failed += 1
+        print(f"  FAIL: {msg}")
+
+
+# ── Reduction implementation ──────────────────────────────────────────────
+
+
+def literal_to_element(lit, n):
+    """Convert a 1-indexed signed literal to a 0-indexed universe element.
+    Positive literal i (1-indexed) → element 2*(i-1).
+    Negative literal -i → element 2*(i-1)+1.
+    """
+    var_idx = abs(lit) - 1  # 0-indexed variable
+    if lit > 0:
+        return 2 * var_idx
+    else:
+        return 2 * var_idx + 1
+
+
+def reduce(n, clauses):
+    """Reduce NAE-SAT instance to Set Splitting.
+
+    Args:
+        n: number of variables (1-indexed: v_1 .. v_n)
+        clauses: list of lists of signed 1-indexed literals
+
+    Returns:
+        (universe_size, subsets): Set Splitting instance
+    """
+    universe_size = 2 * n
+    subsets = []
+    # Complementarity subsets: {2i, 2i+1} for i = 0..n-1
+    for i in range(n):
+        subsets.append([2 * i, 2 * i + 1])
+    # Clause subsets
+    for clause in clauses:
+        subset = [literal_to_element(lit, n) for lit in clause]
+        subsets.append(subset)
+    return universe_size, subsets
+
+
+def is_nae_satisfying(n, clauses, assignment):
+    """Check if assignment (list of 0/1, length n) NAE-satisfies all clauses."""
+    for clause in clauses:
+        vals = set()
+        for lit in clause:
+            var_idx = abs(lit) - 1
+            val = assignment[var_idx]
+            if lit < 0:
+                val = 1 - val
+            vals.add(val)
+        if len(vals) == 1:  # all equal
+            return False
+    return True
+
+
+def is_feasible_source(n, clauses):
+    """Check if NAE-SAT instance is satisfiable (brute force)."""
+    for bits in range(2**n):
+        assignment = [(bits >> i) & 1 for i in range(n)]
+        if is_nae_satisfying(n, clauses, assignment):
+            return True
+    return False
+
+
+def is_set_splitting(universe_size, subsets, config):
+    """Check if config (list of 0/1, length universe_size) is a valid set splitting."""
+    for subset in subsets:
+        vals = set(config[e] for e in subset)
+        if len(vals) == 1:  # monochromatic
+            return False
+    return True
+
+
+def is_feasible_target(universe_size, subsets):
+    """Check if Set Splitting instance is feasible (brute force)."""
+    for bits in range(2**universe_size):
+        config = [(bits >> i) & 1 for i in range(universe_size)]
+        if is_set_splitting(universe_size, subsets, config):
+            return True
+    return False
+
+
+def extract_assignment(n, config):
+    """Extract NAE-SAT assignment from Set Splitting config.
+    Variable i (0-indexed) is true iff element 2i is in part 0.
+    """
+    return [1 - config[2 * i] for i in range(n)]
+    # config[2i] == 0 means element 2i is in S_1 (part 0), so variable is true (1)
+    # Actually: let's think about this more carefully.
+    # Part 0 = S_1. If v_i (element 2i) is in S_1 (config=0), then alpha(v_i)=true (1).
+    # So assignment[i] = 1 if config[2i] == 0, i.e., assignment[i] = 1 - config[2i].
+    # Wait, but the codebase uses config[e]=0 for "part 0" and config[e]=1 for "part 1".
+    # The convention is: S_1 gets config=0, S_2 gets config=1.
+    # True literals go to S_1 (config=0), so:
+    #   var i true => element 2i in S_1 => config[2i]=0 => assignment[i]=1-0=1 ✓
+    #   var i false => element 2i in S_2 => config[2i]=1 => assignment[i]=1-1=0 ✓
+
+
+def all_naesat_instances(n, max_clause_len=None):
+    """Generate all NAE-SAT instances with n variables.
+    Each clause has 2 or 3 literals (no variable appears twice in a clause).
+    """
+    lits = list(range(1, n + 1)) + list(range(-n, 0))
+    clause_sizes = [2, 3] if max_clause_len is None else list(range(2, max_clause_len + 1))
+
+    # Generate all valid clauses
+    all_clauses = []
+    for size in clause_sizes:
+        for combo in itertools.combinations(lits, size):
+            # No variable appears both positive and negative
+            vars_used = [abs(l) for l in combo]
+            if len(set(vars_used)) == len(vars_used):
+                all_clauses.append(list(combo))
+
+    return all_clauses
+
+
+def main():
+    # === Section 1: Symbolic checks (sympy) — MANDATORY ===
+    print("=== Section 1: Symbolic overhead verification ===")
+
+    n_sym, m_sym = symbols("n m", positive=True, integer=True)
+
+    # universe_size = 2n
+    universe_expr = 2 * n_sym
+    check(simplify(universe_expr - 2 * n_sym) == 0,
+          "universe_size should be 2n")
+
+    # num_subsets = n + m
+    subsets_expr = n_sym + m_sym
+    check(simplify(subsets_expr - (n_sym + m_sym)) == 0,
+          "num_subsets should be n + m")
+
+    # Verify for specific values
+    for n_val in range(2, 8):
+        for m_val in range(1, 8):
+            check(universe_expr.subs(n_sym, n_val) == 2 * n_val,
+                  f"universe_size({n_val}) = {2*n_val}")
+            check(subsets_expr.subs({n_sym: n_val, m_sym: m_val}) == n_val + m_val,
+                  f"num_subsets({n_val},{m_val}) = {n_val + m_val}")
+
+    # Complementarity subset size is always 2
+    for n_val in range(1, 10):
+        for i in range(n_val):
+            subset = [2 * i, 2 * i + 1]
+            check(len(subset) == 2,
+                  f"complementarity subset for var {i} has size 2")
+
+    print(f"  Section 1: {passed} passed, {failed} failed")
+
+    # === Section 2: Exhaustive forward + backward — MANDATORY ===
+    print("\n=== Section 2: Exhaustive forward + backward (n ≤ 5) ===")
+    sec2_start = passed
+
+    for n in range(2, 6):  # n = 2, 3, 4, 5
+        # Generate all valid clauses for this n
+        lits = list(range(1, n + 1)) + list(range(-n, 0))
+        all_valid_clauses = []
+        for size in [2, 3]:
+            for combo in itertools.combinations(lits, size):
+                vars_used = [abs(l) for l in combo]
+                if len(set(vars_used)) == len(vars_used):
+                    all_valid_clauses.append(list(combo))
+
+        # Test many clause combinations
+        # For small n, test all single-clause, double-clause, and triple-clause combos
+        num_tested = 0
+        max_per_n = 800 if n <= 3 else 400
+
+        # Single clause instances
+        for clause in all_valid_clauses:
+            if num_tested >= max_per_n:
+                break
+            clauses = [clause]
+            source_feasible = is_feasible_source(n, clauses)
+            u_size, subsets = reduce(n, clauses)
+            target_feasible = is_feasible_target(u_size, subsets)
+
+            check(source_feasible == target_feasible,
+                  f"n={n}, clauses={clauses}: source={source_feasible}, target={target_feasible}")
+            num_tested += 1
+
+        # Multi-clause instances (sample)
+        for num_clauses in [2, 3, 4]:
+            count = 0
+            for combo in itertools.combinations(range(len(all_valid_clauses)), num_clauses):
+                if count >= max_per_n // 3:
+                    break
+                clauses = [all_valid_clauses[i] for i in combo]
+                source_feasible = is_feasible_source(n, clauses)
+                u_size, subsets = reduce(n, clauses)
+                target_feasible = is_feasible_target(u_size, subsets)
+
+                check(source_feasible == target_feasible,
+                      f"n={n}, {num_clauses} clauses: source={source_feasible}, target={target_feasible}")
+                count += 1
+                num_tested += 1
+
+        print(f"  n={n}: tested {num_tested} instances")
+
+    print(f"  Section 2: {passed - sec2_start} new checks")
+
+    # === Section 3: Solution extraction — MANDATORY ===
+    print("\n=== Section 3: Solution extraction ===")
+    sec3_start = passed
+
+    for n in range(2, 6):
+        lits = list(range(1, n + 1)) + list(range(-n, 0))
+        all_valid_clauses = []
+        for size in [2, 3]:
+            for combo in itertools.combinations(lits, size):
+                vars_used = [abs(l) for l in combo]
+                if len(set(vars_used)) == len(vars_used):
+                    all_valid_clauses.append(list(combo))
+
+        num_extracted = 0
+        for num_cl in [1, 2, 3]:
+            for combo in itertools.combinations(range(len(all_valid_clauses)), num_cl):
+                if num_extracted >= 300:
+                    break
+                clauses = [all_valid_clauses[i] for i in combo]
+
+                if not is_feasible_source(n, clauses):
+                    continue
+
+                u_size, subsets = reduce(n, clauses)
+
+                # Find ALL valid set splitting configs and extract assignment from each
+                for bits in range(2**u_size):
+                    config = [(bits >> e) & 1 for e in range(u_size)]
+                    if not is_set_splitting(u_size, subsets, config):
+                        continue
+
+                    assignment = extract_assignment(n, config)
+                    check(is_nae_satisfying(n, clauses, assignment),
+                          f"extraction n={n}: config {config} -> assignment {assignment}")
+                    num_extracted += 1
+
+        print(f"  n={n}: extracted {num_extracted} solutions")
+
+    print(f"  Section 3: {passed - sec3_start} new checks")
+
+    # === Section 4: Overhead formula — MANDATORY ===
+    print("\n=== Section 4: Overhead formula verification ===")
+    sec4_start = passed
+
+    for n in range(2, 6):
+        lits = list(range(1, n + 1)) + list(range(-n, 0))
+        all_valid_clauses = []
+        for size in [2, 3]:
+            for combo in itertools.combinations(lits, size):
+                vars_used = [abs(l) for l in combo]
+                if len(set(vars_used)) == len(vars_used):
+                    all_valid_clauses.append(list(combo))
+
+        for num_cl in [1, 2, 3, 4, 5]:
+            count = 0
+            for combo in itertools.combinations(range(len(all_valid_clauses)), num_cl):
+                if count >= 50:
+                    break
+                clauses = [all_valid_clauses[i] for i in combo]
+                m = len(clauses)
+                u_size, subsets = reduce(n, clauses)
+
+                # Check overhead formula
+                check(u_size == 2 * n,
+                      f"overhead universe: got {u_size}, expected {2*n}")
+                check(len(subsets) == n + m,
+                      f"overhead subsets: got {len(subsets)}, expected {n + m}")
+                count += 1
+
+    print(f"  Section 4: {passed - sec4_start} new checks")
+
+    # === Section 5: Structural properties — MANDATORY ===
+    print("\n=== Section 5: Structural properties ===")
+    sec5_start = passed
+
+    for n in range(2, 6):
+        lits = list(range(1, n + 1)) + list(range(-n, 0))
+        all_valid_clauses = []
+        for size in [2, 3]:
+            for combo in itertools.combinations(lits, size):
+                vars_used = [abs(l) for l in combo]
+                if len(set(vars_used)) == len(vars_used):
+                    all_valid_clauses.append(list(combo))
+
+        for num_cl in [1, 2, 3]:
+            count = 0
+            for combo in itertools.combinations(range(len(all_valid_clauses)), num_cl):
+                if count >= 100:
+                    break
+                clauses = [all_valid_clauses[i] for i in combo]
+                u_size, subsets = reduce(n, clauses)
+
+                # 1. All elements in subsets are valid universe indices
+                for subset in subsets:
+                    for elem in subset:
+                        check(0 <= elem < u_size,
+                              f"element {elem} out of range [0, {u_size})")
+
+                # 2. Every subset has at least 2 elements
+                for subset in subsets:
+                    check(len(subset) >= 2,
+                          f"subset {subset} has fewer than 2 elements")
+
+                # 3. No duplicate elements within a subset
+                for subset in subsets:
+                    check(len(subset) == len(set(subset)),
+                          f"subset {subset} has duplicates")
+
+                # 4. Complementarity subsets come first and pair consecutive elements
+                for i in range(n):
+                    check(subsets[i] == [2 * i, 2 * i + 1],
+                          f"complementarity subset {i}: {subsets[i]}")
+
+                # 5. No empty subsets
+                for subset in subsets:
+                    check(len(subset) > 0, f"empty subset found")
+
+                count += 1
+
+    print(f"  Section 5: {passed - sec5_start} new checks")
+
+    # === Section 6: YES example from Typst — MANDATORY ===
+    print("\n=== Section 6: YES example verification ===")
+    sec6_start = passed
+
+    # From Typst: n=4, m=4
+    # c1 = (v1, v2, v3) = [1, 2, 3]
+    # c2 = (¬v1, v3, v4) = [-1, 3, 4]
+    # c3 = (v2, ¬v3, ¬v4) = [2, -3, -4]
+    # c4 = (v1, ¬v2, v4) = [1, -2, 4]
+    yes_n = 4
+    yes_clauses = [[1, 2, 3], [-1, 3, 4], [2, -3, -4], [1, -2, 4]]
+
+    u_size, subsets = reduce(yes_n, yes_clauses)
+
+    # Check overhead
+    check(u_size == 8, f"YES example: universe_size = {u_size}, expected 8")
+    check(len(subsets) == 8, f"YES example: num_subsets = {len(subsets)}, expected 8")
+
+    # Check exact subsets from Typst
+    expected_subsets = [
+        [0, 1], [2, 3], [4, 5], [6, 7],  # complementarity
+        [0, 2, 4], [1, 4, 6], [2, 5, 7], [0, 3, 6],  # clause
+    ]
+    for i, (got, exp) in enumerate(zip(subsets, expected_subsets)):
+        check(got == exp, f"YES subset {i}: got {got}, expected {exp}")
+
+    # Verify the assignment from Typst: v1=T, v2=F, v3=T, v4=F → [1, 0, 1, 0]
+    yes_assignment = [1, 0, 1, 0]
+    check(is_nae_satisfying(yes_n, yes_clauses, yes_assignment),
+          "YES example: assignment is NAE-satisfying")
+
+    # Verify the partition from Typst: S1 = {0, 3, 4, 7}
+    # config: element in S1 → config=0, element in S2 → config=1
+    # S1 = {0, 3, 4, 7} → config[0]=0, config[3]=0, config[4]=0, config[7]=0
+    # S2 = {1, 2, 5, 6} → config[1]=1, config[2]=1, config[5]=1, config[6]=1
+    yes_config = [0, 1, 1, 0, 0, 1, 1, 0]
+    check(is_set_splitting(u_size, subsets, yes_config),
+          "YES example: partition is a valid set splitting")
+
+    # Verify extraction
+    extracted = extract_assignment(yes_n, yes_config)
+    check(extracted == yes_assignment,
+          f"YES example: extracted {extracted}, expected {yes_assignment}")
+
+    # Verify each clause explicitly as in Typst
+    # c1 = (T, F, T)
+    check(yes_assignment[0] == 1 and yes_assignment[1] == 0 and yes_assignment[2] == 1,
+          "YES c1 values")
+    # c2 = (¬v1=F, v3=T, v4=F)
+    check((1 - yes_assignment[0]) == 0 and yes_assignment[2] == 1 and yes_assignment[3] == 0,
+          "YES c2 values")
+    # c3 = (v2=F, ¬v3=F, ¬v4=T)
+    check(yes_assignment[1] == 0 and (1 - yes_assignment[2]) == 0 and (1 - yes_assignment[3]) == 1,
+          "YES c3 values")
+    # c4 = (v1=T, ¬v2=T, v4=F)
+    check(yes_assignment[0] == 1 and (1 - yes_assignment[1]) == 1 and yes_assignment[3] == 0,
+          "YES c4 values")
+
+    check(is_feasible_source(yes_n, yes_clauses),
+          "YES example: source is feasible")
+    check(is_feasible_target(u_size, subsets),
+          "YES example: target is feasible")
+
+    print(f"  Section 6: {passed - sec6_start} new checks")
+
+    # === Section 7: NO example from Typst — MANDATORY ===
+    print("\n=== Section 7: NO example verification ===")
+    sec7_start = passed
+
+    # From Typst: n=3, m=4
+    # c1 = (v1, v2, v3) = [1, 2, 3]
+    # c2 = (v1, v2, ¬v3) = [1, 2, -3]
+    # c3 = (v1, ¬v2, v3) = [1, -2, 3]
+    # c4 = (v1, ¬v2, ¬v3) = [1, -2, -3]
+    no_n = 3
+    no_clauses = [[1, 2, 3], [1, 2, -3], [1, -2, 3], [1, -2, -3]]
+
+    u_size_no, subsets_no = reduce(no_n, no_clauses)
+
+    # Check overhead
+    check(u_size_no == 6, f"NO example: universe_size = {u_size_no}, expected 6")
+    check(len(subsets_no) == 7, f"NO example: num_subsets = {len(subsets_no)}, expected 7")
+
+    # Check exact subsets from Typst
+    expected_no_subsets = [
+        [0, 1], [2, 3], [4, 5],  # complementarity
+        [0, 2, 4], [0, 2, 5], [0, 3, 4], [0, 3, 5],  # clause
+    ]
+    for i, (got, exp) in enumerate(zip(subsets_no, expected_no_subsets)):
+        check(got == exp, f"NO subset {i}: got {got}, expected {exp}")
+
+    # Verify source is infeasible
+    check(not is_feasible_source(no_n, no_clauses),
+          "NO example: source is infeasible")
+
+    # Verify target is infeasible
+    check(not is_feasible_target(u_size_no, subsets_no),
+          "NO example: target is infeasible")
+
+    # Verify each of the 8 assignments fails as stated in Typst
+    for bits in range(8):
+        assignment = [(bits >> i) & 1 for i in range(3)]
+        check(not is_nae_satisfying(no_n, no_clauses, assignment),
+              f"NO example: assignment {assignment} should fail NAE")
+
+    # Verify no set splitting config works
+    no_splitting_count = 0
+    for bits in range(2**6):
+        config = [(bits >> e) & 1 for e in range(6)]
+        if not is_set_splitting(u_size_no, subsets_no, config):
+            no_splitting_count += 1
+    check(no_splitting_count == 64,
+          f"NO example: all 64 configs fail set splitting (got {64 - no_splitting_count} valid)")
+
+    print(f"  Section 7: {passed - sec7_start} new checks")
+
+    # ── Final report ──
+    print(f"\nNAESatisfiability → SetSplitting: {passed} passed, {failed} failed")
+    return 1 if failed else 0
+
+
+if __name__ == "__main__":
+    sys.exit(main())