Using TLA+ to solve a logic puzzle

To start learning how to use TLA+, I'm trying to use the toolbox to solve a logic puzzle.

I specified an invariant that should be false in order to get the model checker to return an error and provide a counter-example that solves the puzzle ("who owns the fish"?)

However, when I run the model checker on my module, it doesn't terminate after executing for at least 100 minutes, so I suspect I'm doing something wrong.

I'm running the model checker with the following parameters:

Behavior spec:
Init: Init
Next: Next

What to check?
Invariants: NobodyHasTheFish

(all other options are default)

Here's my module, fish.tla:

-------------------------------- MODULE fish --------------------------------

EXTENDS Integers

VARIABLES livesin, painted, keeps, drinks, smokes

People == { "Brit", "Swede", "Dane", "Norwegian", "German" }
Colors == { "white", "yellow", "blue", "red", "green" }
Pets == { "birds", "cats", "dogs", "horses", "fish" }
Beverages == { "tea", "coffee", "milk", "beer", "water" }
Cigarettes == { "Pall Mall", "Dunhill", "Marlboro", "Winfield", "Rothmans" }

Houses == 1..5

TypeOK ==  /\ livesin \in [ People -> Houses ]
/\ keeps \in [ People -> Pets ]
/\ drinks \in [ People -> Beverages ]
/\ smokes \in [ People -> Cigarettes ]
/\ painted \in  [ Houses -> Colors ]

FuncsAreOnto == /\ \A h \in Houses : \E p \in People : livesin[p] = h
/\ \A c \in Colors : \E h \in Houses : painted[h] = c
/\ \A t \in Pets   : \E p \in People : keeps[p] = t
/\ \A b \in Beverages : \E p \in People : drinks[p] = b
/\ \A c \in Cigarettes : \E p \in People : smokes[p] = c

Neighbor(p1, p2) == livesin[p2] \in { livesin[p1] - 1, livesin[p1] + 1 }

TheBritLivesInTheRedHouse == \A h \in Houses : painted[h] = "red" => livesin["Brit"] = h
TheSwedeKeepsDogsAsPets == keeps["Swede"] = "dogs"
TheDaneDrinksTea == drinks["Dane"] = "tea"
TheGreenHouseIsOnTheLeftOfTheWhiteHouse == \A h1, h2 \in Houses :
(painted[h1] = "green" /\ painted[h2] = "white") => h1 = h2 - 1
TheGreenHousesOwnerDrinksCoffee == \A p \in People, h \in Houses :
(painted[h] = "Green" /\ livesin[p] = h) => drinks[p] = "coffee"
ThePersonWhoSmokesPallMallRearsBirds == \A p \in People :
(smokes[p] = "Pall Mall") => keeps[p] = "birds"
TheYellowHouseOwnerSmokesDunhill == \A p \in People, h \in Houses:
(smokes[p] = "Dunhill" /\ painted[h] = "yellow") => livesin[p] = h
TheManLivingInTheCenterHouseDrinksMilk == \A p \in People :
(livesin[p] = 3) => (drinks[p] = "milk")
TheNorwegianLivesInTheFirstHouse == livesin["Norwegian"] = 1
ThePersonWhoSmokesMarlboroLiveNextToTheOneWhoKeepsCats == \A p1,p2 \in People :
(smokes[p1] = "Marlboro" /\ keeps[p2] = "cats") => Neighbor(p1, p2)
ThePersonWhoKeepsHorsesLivesNextToThePersonWhoSmokesDunhill == \A p1,p2 \in People :
(keeps[p1] = "horses" /\ smokes[p2] = "Dunhill") => Neighbor(p1, p2)
ThePersonWhoSmokesWinfieldDrinksBeer == \A p \in People:
(smokes[p] = "Winfield") => (drinks[p] = "Beer")
TheGermanSmokesRothmans == smokes["German"] = "Rothmans"
TheNorwegianLivesNextToTheBlueHouse == \A p \in People :
painted[livesin[p]] = "blue" => Neighbor("Norwegian", p)
ThePersonWhoSmokesMarlboroHasNeighborWhoDrinksWater == \A p1,p2 \in People :
(smokes[p1] = "Marlboro" /\ drinks[p2] = "water") => Neighbor(p1, p2)

Constraints == /\ TypeOK
/\ FuncsAreOnto
/\ TheBritLivesInTheRedHouse
/\ TheSwedeKeepsDogsAsPets
/\ TheDaneDrinksTea
/\ TheGreenHouseIsOnTheLeftOfTheWhiteHouse
/\ TheGreenHousesOwnerDrinksCoffee
/\ ThePersonWhoSmokesPallMallRearsBirds
/\ TheYellowHouseOwnerSmokesDunhill
/\ TheManLivingInTheCenterHouseDrinksMilk
/\ TheNorwegianLivesInTheFirstHouse
/\ ThePersonWhoSmokesMarlboroLiveNextToTheOneWhoKeepsCats
/\ ThePersonWhoKeepsHorsesLivesNextToThePersonWhoSmokesDunhill
/\ ThePersonWhoSmokesWinfieldDrinksBeer
/\ TheGermanSmokesRothmans
/\ TheNorwegianLivesNextToTheBlueHouse
/\ ThePersonWhoSmokesMarlboroHasNeighborWhoDrinksWater

NobodyHasTheFish == ~ \E p \in People: keeps[p] = "fish"

Init == Constraints
Next == UNCHANGED << livesin, painted, keeps, drinks >>

=============================================================================