EinsteinsMice29R

Einstein's Mice 29R

Our problem consists of three mice living next to each other in three holes in the wall. Each mouse (Mickey, Minnie, and Mighty) has a favorite cheese flavor (Brie, Gouda or Emmentaler) and a favorite TV show (Simpsons, Seinfeld, or ER). Here are the hints:

1. Mickey Mouse loves Gouda.
2. Mighty Mouse's favorite TV show is Emergency Room.
3. The mouse that lives in the left hole never misses an episode of Seinfeld.
4. Mickey Mouse and Mighty Mouse have one mouse hole between them.
5. The Simpsons fan does not live on the left of the Brie lover.

The problem is to figure out which mouse lives in which hole, likes which cheese, and has which favorite TV show.

Source: http://www.weitz.de/einstein.html

Answers: (MICKEY GOUDA SEINFELD Hole1)
(MINNY BRIE SIMPSONS Hole2)
(MIGHTY EMMENTALER ER Hole3))

To run the proof, click 'Prove' below.

Note: the prover here is running on a shared server, and the run time is slow due to that. On a dedicated machine, this proof takes only .357 seconds.

Use of the 'answer' predicate is explained in: Tau_JAR.pdf. For discussion of the problem, see P. 6.

Premises:

(forall ?X (or (favCheese ?X Brie) (favCheese ?X Gouda) (favCheese ?X Emmentaler)))
(forall ?X (or (livesInHole ?X Hole1) (livesInHole ?X Hole2) (livesInHole ?X Hole3)))
(forall ?X (or (favTVShow ?X Simpsons) (favTVShow ?X ER) (favTVShow ?X Seinfeld)))
(forall ?X (and (or (not (favCheese ?X Brie)) (not (favCheese ?X Gouda)))
(or (not (favCheese ?X Brie)) (not (favCheese ?X Emmentaler)))
(or (not (favCheese ?X Gouda)) (not (favCheese ?X Emmentaler)))))
(forall ?X (and (or (not (livesInHole ?X Hole1)) (not (livesInHole ?X Hole2)))
(or (not (livesInHole ?X Hole1)) (not (livesInHole ?X Hole3)))
(or (not (livesInHole ?X Hole2)) (not (livesInHole ?X Hole3)))))
(forall ?X (and (or (not (favTVShow ?X Simpsons)) (not (favTVShow ?X ER)))
(or (not (favTVShow ?X Simpsons)) (not (favTVShow ?X Seinfeld)))
(or (not (favTVShow ?X Seinfeld)) (not (favTVShow ?X ER)))))
(forall ?X (and (or (not (favCheese Mickey ?X)) (not (favCheese Mighty ?X)))
(or (not (favCheese Mickey ?X)) (not (favCheese Minnie ?X)))
(or (not (favCheese Mighty ?X)) (not (favCheese Minnie ?X)))))
(forall ?X (and (or (not (favTVShow Mickey ?X)) (not (favTVShow Mighty ?X)))
(or (not (favTVShow Mickey ?X)) (not (favTVShow Minnie ?X)))
(or (not (favTVShow Mighty ?X)) (not (favTVShow Minnie ?X)))))
(forall ?X (and (or (not (livesInHole Mickey ?X)) (not (livesInHole Mighty ?X)))
(or (not (livesInHole Mickey ?X)) (not (livesInHole Minnie ?X)))
(or (not (livesInHole Mighty ?X)) (not (livesInHole Minnie ?X)))))
(forall ?X (<=> (livesInHole ?X Hole1)  (favTVShow ?X Seinfeld)))
(favCheese Mickey Gouda)
(favTVShow Mighty ER)
(livesInHole Minnie Hole2)
(or (livesInHole Mickey Hole1) (livesInHole Mighty Hole1))
(or (livesInHole Mighty Hole3) (livesInHole Mickey Hole3))
(forall (?X ?Y) (=> (and (livesInHole ?X Hole1) (livesInHole ?Y Hole2)) (not (and (favTVShow ?X Simpsons) (favCheese ?Y Brie)))))
(forall (?X ?Y) (=> (and (livesInHole ?X Hole1) (livesInHole ?Y Hole3)) (not (and (favTVShow ?X Simpsons) (favCheese ?Y Brie)))))
(forall (?X ?Y) (=> (and (livesInHole ?X Hole2) (livesInHole ?Y Hole3)) (not (and (favTVShow ?X Simpsons) (favCheese ?Y Brie)))))
(forall ?X (=> (and (livesInHole Mighty ?X) (not (livesInHole Minnie ?X)) (not (livesInHole Mickey ?X))) (answer ?X)))
(forall ?X (=> (and (livesInHole Minnie ?X) (not (livesInHole Mighty ?X)) (not (livesInHole Mickey ?X))) (answer1 ?X)))
(forall ?X (=> (and (livesInHole Mickey ?X) (not (livesInHole Minnie ?X)) (not (livesInHole Mighty ?X))) (answer2 ?X)))
(forall ?X (=> (and (favCheese Minnie ?X) (not (favCheese Mickey ?X)) (not (favCheese Mighty ?X))) (answer3 ?X)))

Conclusion: