--         File: murder_mystery.sql
--      Version: 1.0
-- Last Changed: 2017-12-11
--           by: Damir;  https://www.damirsystems.com
--      Project: Murder Mistery
--  Description: Fun challenge from Decision Management Community
--               https://dmcommunity.org/challenge/challenge-nov-2014/
--               Based on the problem No 55 from:
--               Seventy Five Problems for Testing Automatic Theorem Provers
--               by Francis Jeffry Pelletier
--
--           DB: PostgreSQL, MS SQL Server

WITH
-- (c1)   Agatha, Charles, and butler are the only ones to live there.
-- [p_01] Person (p) exists.
person  AS (
    SELECT p FROM (
        VALUES ('Agatha'), ('Charles'), ('butler')
    ) AS x(p)
),
-- (c2)   Agatha hates everybody except the butler.
-- [p_02] Agatha hates person (p).
agatha_hates AS (
    SELECT a.p
    FROM  person AS a
    WHERE a.p != 'butler'
),
-- (c3)   Charles hates no one that Agatha hates.
-- [p_03] Charles hates person (p).
charles_hates AS (
    SELECT a.p
    FROM  person AS a
    WHERE a.p NOT IN (SELECT p FROM agatha_hates)
),
-- (c4)   The butler hates everyone whom Agatha hates.
-- [p_04] The butler hates person (p).
butler_hates AS (
    SELECT p
    FROM agatha_hates
),
-- [p_05] Person (h) hates person (p).
hate  AS  (
    SELECT 'Agatha'  AS h, p FROM agatha_hates
    UNION
    SELECT 'Charles' AS h, p FROM charles_hates
    UNION
    SELECT 'butler'  AS h, p FROM butler_hates
),
-- [p_06] Person (h) hates (n) people.
hate_cnt AS (
    SELECT h, count(1) AS n
    FROM hate
    GROUP BY h
),
-- [p_07] Person (x) hates Agatha.
hates_agatha AS (
    SELECT a.h AS x
    FROM hate  AS a
    WHERE a.p = 'Agatha'
),
-- (c6)   The butler hates everyone not richer than Agatha.
-- [p_08] Person (x) is not richer than Agatha.
nrt_agatha AS (
    SELECT p AS x
    FROM butler_hates
)
-- (c7)   The murderer hates Agatha, and is not richer than Agatha.
-- (c5)   No one hates everyone
-- [p_09] Person (murderer) killed Agatha.
-- solution
SELECT a.x AS murderer
FROM hates_agatha AS a
JOIN nrt_agatha   AS b ON b.x = a.x
WHERE NOT exists (SELECT 1 FROM hate_cnt WHERE n = 3)
;