def has_neighbor(prop1: str, prop2: str) -> str:
    """
    Builds the statements required for: The person who `prop1` has a neighbor who `prop2`.
    For example, "The Norwegian lives next to the Blue house."

    We can solve this by doing a disjunction of all satisfying possibilities. Because we've
    previously stated that, for example, there's only one Norwegian and only one blue house,
    we don't need to conjoin to prevent duplicates. Thus, we can say:

    ```ignore
    (assert (or
        (and (norwegian 1) (blue 2))
        (and (norwegian 2) (blue 1))
        (and (norwegian 2) (blue 3))
        (and (norwegian 3) (blue 2))
        (and (norwegian 3) (blue 4))
        ...
    ))
    ```
    """
    ands = []
    for i in range(1, 6):
        for j in range(1, 6):
            if abs(i-j) == 1:
                ands.append(f'    (and ({prop1} {i}) ({prop2} {j}))')

    return '(assert (or\n' \
        + '\n'.join(ands) \
        + '))\n'