theorem starbucks_enthymeme_is_contradictory
theorem starbucks_enthymeme_is_contradictory
(p1 : Sam loves Starbucks)
(p2 : Sam never-buys-from BigCoffeeChain)
(p3 : Starbucks is-a-big-coffee-chain)
(p4 : ∀ person coffeeChain,
      person loves coffeeChain → person buys-from coffeeChain)
: False