Zebra puzzle

You are encouraged to solve this task according to the task description, using any language you may know.
The Zebra puzzle, a.k.a. Einstein's Riddle,
is a logic puzzle which is to be solved programmatically.



It has several variants, one of them this:

   There are five houses.
   The English man lives in the red house.
   The Swede has a dog.
   The Dane drinks tea.
   The green house is immediately to the left of the white house.
   They drink coffee in the green house.
   The man who smokes Pall Mall has birds.
   In the yellow house they smoke Dunhill.
   In the middle house they drink milk.
   The Norwegian lives in the first house.
   The man who smokes Blend lives in the house next to the house with cats.
   In a house next to the house where they have a horse, they smoke Dunhill.
   The man who smokes Blue Master drinks beer.
   The German smokes Prince.
   The Norwegian lives next to the blue house.
   They drink water in a house next to the house where they smoke Blend. 

The question is, who owns the zebra?

Additionally, list the solution for all the houses.

Optionally, show the solution is unique.



Related tasks

   Dinesman's multiple-dwelling problem
   Twelve statements


 
// First, let's give some type-variables some values:
Nationality = Englishman | Swede   | Dane       | Norwegian | German 
Colour      = Red        | Green   | Yellow     | Blue      | White
Cigarette   = PallMall   | Dunhill | BlueMaster | Blend     | Prince
Domestic    = Dog        | Bird    | Cat        | Zebra     | Horse
Beverage    = Tea        | Coffee  | Milk       | Beer      | Water
HouseRow    = First      | Second  | Third      | Fourth    | Fifth 
 
{ 
We use injections to make the array-elements unique.
Example: 'Pet' is an array of unique elements of type 'Domestic', indexed by 'Nationality'. 
In the predicate 'Zebra', we use this injection 'Pet' to define the array-variable 'pet' 
as a parameter of the 'Zebra'-predicate.
The symbol used is the '->>'. 'Nationality->>Domestic' can be read as 'Domestic(Nationality)' 
in "plain array-speak";
the difference being that the elements are by definition unique (cf. 'injective function').
 
So, in FormulaOne we use a formula like: 'pet(Swede) = Dog', which simply means that the 'Swede' 
(type 'Nationality') has a 'pet' (type 'Pet', of type 'Domestic', indexed by 'Nationality'), 
which appears to be a 'Dog' (type 'Domestic'). 
Or, one could say that the 'Swede' has been mapped to the 'Dog' (Oh, well...).
}
 
Pet          = Nationality->>Domestic
Drink        = Nationality->>Beverage                             
HouseColour  = Nationality->>Colour
Smoke        = Nationality->>Cigarette
HouseOrder   = HouseRow->>Nationality 
 
pred Zebra(house_olour::HouseColour, pet::Pet, smoke::Smoke, drink::Drink, house_order::HouseOrder) iff
 
// For convenience sake, some temporary place_holder variables are used.
// An underscore distinguishes them:
 
     house_colour(green_house)     = Green      &
     house_colour(white_house)     = White      & 
     house_colour(yellow_house)    = Yellow     & 
     smoke(pallmall_smoker)        = PallMall   & 
     smoke(blend_smoker)           = Blend      & 
     smoke(dunhill_smoker)         = Dunhill    &  
     smoke(bluemaster_smoker)      = BlueMaster & 
     pet(cat_keeper)               = Cat        & 
     pet(neighbour_dunhill_smoker) = Horse      & 
 
{ 2. The English man lives in the red house: }
     house_colour(Englishman) = Red &
 
{ 3. The Swede has a dog: }
     pet(Swede) = Dog &     
 
{ 4. The Dane drinks tea: }
     drink(Dane) = Tea &  
 
    { 'smoke' and 'drink' are both nouns, like the other variables.
      One could read the formulas like: 'the colour of the Englishman's house is Red' ->
     'the Swede's pet is a dog' -> 'the Dane's drink is tea'.
    }
 
{ 5. The green house is immediately to the left of the white house.
     The local predicate 'LeftOf' (see below) determines the house order: }
     LeftOf(green_house, white_house, house_order) &  
 
{ 6. They drink coffee in the green house: }
     drink(green_house) = Coffee & 
 
{ 7. The man who smokes Pall Mall has birds: }
     pet(pallmall_smoker) = Bird &
 
{ 8. In the yellow house they smoke Dunhill: }
     smoke(yellow_house) = Dunhill & 
 
{ 9. In the middle house (third in the row) they drink milk: }
     drink(house_order(Third)) = Milk & 
 
{10. The Norwegian lives in the first house: }
     house_order(First) = Norwegian &  
 
{11. The man who smokes Blend lives in the house next to the house with cats.
     Another local predicate 'Neighbour' makes them neighbours: }
     Neighbour(blend_smoker, cat_keeper, house_order) & 
 
{12. In a house next to the house where they have a horse, they smoke Dunhill: }
     Neighbour(dunhill_smoker, neighbour_dunhill_smoker, house_order) &
 
{13. The man who smokes Blue Master drinks beer: }
     drink(bluemaster_smoker) = Beer &
 
{14. The German smokes Prince: }
     smoke(German) = Prince &
 
{15. The Norwegian lives next to the blue house 
     Cf. 10. "The Norwegian lives in the first house", so the blue house is the second house: }
     house_colour(house_order(Second)) = Blue & 
 
{16. They drink water in a house next to the house where they smoke Blend: }
     drink(neighbour_blend_smoker) = Water & 
     Neighbour(blend_smoker, neighbour_blend_smoker, house_order)  
 
{  A simplified solution would number the houses 1, 2, 3, 4, 5
   which makes it easier to order the houses.
   'right in the center' would become 3; 'in the first house', 1
   But we stick to the original puzzle and use some local predicates.
}
 
local pred Neighbour(neighbour1::Nationality, neighbour2::Nationality, house_order::HouseOrder)iff
   neighbour1 <> neighbour2 &
   house_order(house1) = neighbour1 & 
   house_order(house2) = neighbour2 & 
   ( house1 = house2 + 1 | 
     house1 = house2 - 1 ) 
 
local pred LeftOf(neighbour1::Nationality, neighbour2::Nationality, house_order::HouseOrder) iff 
   neighbour1 <> neighbour2 &
   house_order(house1) = neighbour1 & 
   house_order(house2) = neighbour2 & 
   house1 = house2 - 1 
 
{ 
The 'all'-query in FormulaOne:
     all Zebra(house_colour, pet, smokes, drinks, house_order) 
gives, of course, only one solution, so it can be replaced by:
     one Zebra(house_colour, pet, smokes, drinks, house_order)
}
 
// The compacted version:
 
Nationality = Englishman | Swede   | Dane       | Norwegian | German 
Colour      = Red        | Green   | Yellow     | Blue      | White
Cigarette   = PallMall   | Dunhill | BlueMaster | Blend     | Prince
Domestic    = Dog        | Bird    | Cat        | Zebra     | Horse
Beverage    = Tea        | Coffee  | Milk       | Beer      | Water
HouseRow    = First      | Second  | Third      | Fourth    | Fifth 
 
Pet          = Nationality->>Domestic
Drink        = Nationality->>Beverage                             
HouseColour  = Nationality->>Colour
Smoke        = Nationality->>Cigarette
HouseOrder   = HouseRow->>Nationality 
 
pred Zebra(house_colour::HouseColour, pet::Pet, smoke::Smoke, drink::Drink, house_order::HouseOrder) iff
 
  house-colour(green_house) = Green &
  house-colour(white_house) = White & 
  house-colour(yellow_house) = Yellow & 
  smoke(pallmall_smoker) = PallMall & 
  smoke(blend_smoker) = Blend & 
  smoke(dunhill_smoker) = Dunhill &  
  smoke(bluemaster_smoker) = BlueMaster & 
  pet(cat_keeper) = Cat & 
  pet(neighbour_dunhill_smoker) = Horse & 
  house_colour(Englishman) = Red &
  pet(Swede) = Dog &     
  drink(Dane) = Tea &  
  LeftOf(green_house, white_house, house_order) &  
  drink(green_house) = Coffee & 
  pet(pallmall_smoker) = Bird &
  smoke(yellow_house) = Dunhill & 
  drink(house_order(Third)) = Milk & 
  house_order(First) = Norwegian &  
  Neighbour(blend_smoker, cat_keeper, house_order) & 
  Neighbour(dunhill_smoker, neighbour_dunhill_smoker, house_order) &
  drink(bluemaster_smoker) = Beer &
  smoke(German) = Prince & 
  house_colour(house_order(Second)) = Blue &
  drink(neighbour_blend_smoker) = Water & 
  Neighbour(blend_smoker, neighbour_blend_smoker, house_order)  
 
local pred Neighbour(neighbour1::Nationality, neighbour2::Nationality, house_order::HouseOrder)iff
   neighbour1 <> neighbour2 & 
   house_order(house1) = neighbour1 & house_order(house2) = neighbour2 & 
   ( house1 = house2 + 1 | house1 = house2 - 1 ) 
 
local pred LeftOf(neighbour1::Nationality, neighbour2::Nationality, house_::HouseOrder) iff 
   neighbour1 <> neighbour2 &
   house_order(house1) = neighbour1 & house_order(house2) = neighbour2 & 
   house1 = house2 - 1
 