EinsteinsMice26R
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 (or (favTVShow Mickey ?X) (favTVShow Minnie ?X) (favTVShow Mighty ?X))) (forall ?X (or (favCheese Mickey ?X) (favCheese Minnie ?X) (favCheese Mighty ?X))) (forall ?X (or (livesInHole Mickey ?X) (livesInHole Minnie ?X) (livesInHole Mighty ?X))) (forall ?X (or (not (favCheese ?X Brie)) (not (favCheese ?X Gouda)) (not (favCheese ?X Emmentaler)))) (forall ?X (or (not (favTVShow ?X Simpsons)) (not (favTVShow ?X Seinfeld)) (not (favTVShow ?X ER)))) (forall ?X (or (not (livesInHole ?X Hole1)) (not (livesInHole ?X Hole2)) (not (livesInHole ?X Hole3)))) (forall ?X (or (not (favCheese Mickey ?X)) (not (favCheese Minnie ?X)) (not (favCheese Mighty ?X )))) (forall ?X (or (not (favTVShow Mickey ?X)) (not (favTVShow Minnie ?X)) (not (favTVShow Mighty ?X)))) (forall ?X (or (not (livesInHole Mickey ?X)) (not (livesInHole Minnie ?X)) (not (livesInHole Mighty ?X )))) (forall (?X ?Y) (=> (same ?X ?Y) (same ?Y ?X))) (forall (?X ?Y ?Z) (=> (and (livesInHole ?X ?Y) (same ?Y ?Z)) (livesInHole ?X ?Z))) (forall (?X ?Y ?Z) (=> (and (livesInHole ?X ?Z) (livesInHole ?Y ?Z)) (same ?X ?Y))) (forall (?X ?Y ?Z) (=> (and (livesInHole ?Z ?X) (livesInHole ?Z ?Y)) (same ?X ?Y))) (forall (?X ?Y ?Z) (=> (and (favCheese ?X ?Y) (same ?Y ?Z)) (favCheese ?X ?Z))) (forall (?X ?Y ?Z) (=> (and (favCheese ?X ?Z) (favCheese ?Y ?Z)) (same ?X ?Y))) (forall (?X ?Y ?Z) (=> (and (favCheese ?Z ?X) (favCheese ?Z ?Y)) (same ?X ?Y))) (forall (?X ?Y ?Z) (=> (and (favTVShow ?X ?Y) (same ?Y ?Z)) (favTVShow ?X ?Z))) (forall (?X ?Y ?Z) (=> (and (favTVShow ?X ?Z) (favTVShow ?Y ?Z)) (same ?X ?Y))) (forall (?X ?Y ?Z) (=> (and (favTVShow ?Z ?X) (favTVShow ?Z ?Y)) (same ?X ?Y))) (forall (?X ?Y) (=> (favCheese ?X ?Y) (forall ?Z (=> (not (same ?Y ?Z)) (not (favCheese ?X ?Z)))))) (forall (?X ?Y) (=> (favTVShow ?X ?Y) (forall ?Z (=> (not (same ?Y ?Z)) (not (favTVShow ?X ?Z)))))) (forall (?X ?Y) (=> (livesInHole ?X ?Y) (forall ?Z (=> (not (same ?Y ?Z)) (not (livesInHole ?X ?Z)))))) (not (same Mickey Minnie)) (not (same Mickey Mighty)) (not (same Minnie Mighty)) (not (same Brie Gouda)) (not (same Brie Emmentaler)) (not (same Gouda Emmentaler)) (not (same ER Simpsons)) (not (same ER Seinfeld)) (not (same Simpsons Seinfeld)) (not (same Hole1 Hole2)) (not (same Hole1 Hole3)) (not (same Hole2 Hole3)) (not (same Hole2 Hole1)) (not (same Hole2 Hole3)) (not (same Hole3 Hole2)) (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)) (not (livesInHole Minnie Hole1)) (not (livesInHole Mickey Hole2)) (not (livesInHole Mickey Hole2)) (leftOf Hole1 Hole2) (leftOf Hole2 Hole3) (leftOf Hole1 Hole3) (not (leftOf Hole2 Hole1)) (not (leftOf Hole3 Hole1)) (not (leftOf Hole3 Hole2)) (not (leftOf Hole1 Hole1)) (not (leftOf Hole2 Hole2)) (not (leftOf Hole3 Hole3)) (forall ?X (<=> (favCheese ?X Brie) (favTVShow ?X Simpsons))) (forall (?X ?Y ?Z ?W) (=> (and (livesInHole ?X ?W) (livesInHole ?Y ?Z) (leftOf ?W ?Z) (favTVShow ?X Simpsons)) (not (favCheese ?Y Brie) )))
Conclusion:
(and (livesInHole Minnie Hole2) (livesInHole Mighty Hole3) (favCheese Mickey Gouda) (not (livesInHole Mickey Hole2)) (not (livesInHole Minnie Hole3)) (favCheese Minnie Brie) (livesInHole Minnie Hole2) (favCheese Mighty Emmentaler) (favTVShow Mighty ER) (favTVShow Minnie Simpsons) (favTVShow Mickey Seinfeld) )