set(integer_ring).  % <+,-,*> is the ring of integers mod n
set(order_domain).  % "<" is the less-than relation on the domain

formulas(assumptions).  % Assume a domain of size 5: {0,1,2,3,4}

% The clues.

    England(x) <-> Red(x).
    Spain(x) <-> Dog(x).
    Norway(0).
    Kool(x) <-> Yellow(x).
    Chesterfield(x) & Fox(y) -> neighbor(x,y).
    Norway(x) & Blue(y) -> neighbor(x,y).
    Winston(x) <-> Snail(x).
    Lucky(x) <-> Juice(x).
    Ukraine(x) <-> Tea(x).
    Japan(x) <-> Parlaiment(x).
    Kool(x) & Horse(y) -> neighbor(x,y).
    Coffee(x) <-> Green(x).
    Green(x) & Ivory(y) -> successor(y,x).
    Milk(2).

% Definitions of successor and neighbor.

    successor(x,y) <-> x+1 = y & x < y.
    neighbor(x,y) <-> successor(x,y) | successor(y,x).

% Each house has at least one nationality, pet, drink, color, smoke.

    England(x) | Spain(x) | Ukraine(x) | Japan(x) | Norway(x).
    Dog(x) | Snail(x) | Horse(x) | Zebra(x) | Fox(x).
    Water(x) | Milk(x) | Juice(x) | Tea(x) | Coffee(x).
    Red(x) | Blue(x) | Yellow(x) | Ivory(x) | Green(x).
    Lucky(x) | Winston(x) | Kool(x) | Chesterfield(x) | Parlaiment(x).

% Each property applies to at most one house.

    England(x) & England(y) -> x = y.
    Spain(x) & Spain(y) -> x = y.
    Ukraine(x) & Ukraine(y) -> x = y.
    Japan(x) & Japan(y) -> x = y.
    Norway(x) & Norway(y) -> x = y.
    Dog(x) & Dog(y) -> x = y.
    Snail(x) & Snail(y) -> x = y.
    Horse(x) & Horse(y) -> x = y.
    Zebra(x) & Zebra(y) -> x = y.
    Fox(x) & Fox(y) -> x = y.
    Water(x) & Water(y) -> x = y.
    Milk(x) & Milk(y) -> x = y.
    Juice(x) & Juice(y) -> x = y.
    Tea(x) & Tea(y) -> x = y.
    Coffee(x) & Coffee(y) -> x = y.
    Red(x) & Red(y) -> x = y.
    Blue(x) & Blue(y) -> x = y.
    Yellow(x) & Yellow(y) -> x = y.
    Ivory(x) & Ivory(y) -> x = y.
    Green(x) & Green(y) -> x = y.
    Lucky(x) & Lucky(y) -> x = y.
    Winston(x) & Winston(y) -> x = y.
    Kool(x) & Kool(y) -> x = y.
    Chesterfield(x) & Chesterfield(y) -> x = y.
    Parlaiment(x) & Parlaiment(y) -> x = y.

end_of_list.

