Using Add_implications in CP-SAT solver (google OR Tools)

I'm working on learning to use CP solver in ortools. I've built a test problem that attempts to locate feasible options for placing dogs that don't get along in cages so incompatible pairs are not next to each other. The problem I've put together only has two possible solutions, but the solver is not selecting either of these. Am I using add_implication incorrectly, since that is the part of the code where I am testing for bad combinations? I'm not currently using any other constraints other than that all dogs should be in a cage and only one dog per cage.

Here is my simple test code. It should produce one of the possible feasible solutions (Boone in either A or D, with Kensey next to him), but usually doesn't. I've tried other operations other than add_implication, but none of them seem to show the feasible values.

from ortools.sat.python import cp_model

# Data
animals = ["Lulu", "Abby", "Boone", "Kensey"]
cages = ["cage_A", "cage_B", "cage_C", "cage_D"]

# Incompatible pairs (cannot be next to each other)
incompatible_pairs = [("Boone", "Lulu"), ("Boone", "Abby")]

# Cage adjacencies (represented as pairs)
adjacent_cages = [("cage_A", "cage_B"), ("cage_B", "cage_C"), ("cage_C", "cage_D")]

# Model
model = cp_model.CpModel()

# Variables
x = {}
for animal in animals:
    for cage in cages:
        x[(animal, cage)] = model.new_bool_var(f"x_{animal}_{cage}")

# Constraints

# Each animal goes into exactly one cage
for animal in animals:
    model.add(sum(x[(animal, cage)] for cage in cages) == 1)

# Each cage holds at most one animal
for cage in cages:
    model.add(sum(x[(animal, cage)] for animal in animals) <= 1)

# Adjacency constraints
for animal1, animal2 in incompatible_pairs:
    for cage1, cage2 in adjacent_cages:
        # If animal1 is in cage1, then animal2 cannot be in cage2
        model.add_implication(x[(animal1, cage1)], x[(animal2, cage2)].Not())
        # And vice-versa: if animal2 is in cage2, animal1 cannot be in cage1
        model.add_implication(x[(animal2, cage2)], x[(animal1, cage1)].Not())

# Solve

solver = cp_model.CpSolver()
status = solver.Solve(model)

# Print solution
if status == cp_model.OPTIMAL or status == cp_model.FEASIBLE:
    print("Solution:")    
    for animal in animals:
        for cage in cages:
            if solver.value(x[(animal, cage)]):
                print(f"  {animal} assigned to {cage}")
else:
    print("No solution found.")

    ```

Thank you for any help you can offer.

I simplified the code, remove the implications

# Each animal goes into exactly one cage
for animal in animals:
    model.add_exactly_one(x[(animal, cage)] for cage in cages)

# Each cage holds at most one animal
for cage in cages:
    model.add_exactly_one(x[(animal, cage)] for animal in animals)

# Adjacency constraints
for animal1, animal2 in incompatible_pairs:
    for cage1, cage2 in adjacent_cages:
        model.add_at_least_one(~x[(animal1, cage1)], ~x[(animal2, cage2)])
        model.add_at_least_one(~x[(animal2, cage1)], ~x[(animal1, cage2)])

Now I can iterate all solutions, I get 4, which in retrospect should be correct

Solution 0, time = 0.02 s
  Abby assigned to cage_A
  Lulu assigned to cage_B
  Kensey assigned to cage_C
  Boone assigned to cage_D

Solution 1, time = 0.02 s
  Boone assigned to cage_A
  Kensey assigned to cage_B
  Lulu assigned to cage_C
  Abby assigned to cage_D

Solution 2, time = 0.02 s
  Boone assigned to cage_A
  Kensey assigned to cage_B
  Abby assigned to cage_C
  Lulu assigned to cage_D

Solution 3, time = 0.02 s
  Lulu assigned to cage_A
  Abby assigned to cage_B
  Kensey assigned to cage_C
  Boone assigned to cage_D