```// **************************************************************************
//
//    eses                   eses
//   eses                     eses
//  eses    eseses  esesese    eses   Embedded Systems Group
//  ese    ese  ese ese         ese
//  ese    eseseses eseseses    ese   Department of Computer Science
//  eses   eses          ese   eses
//   eses   eseses  eseseses  eses    University of Kaiserslautern
//    eses                   eses
//
// **************************************************************************
//
// Someone who lives in Dreadsbury Mansion killed aunt Agatha. Agatha,
// the butler, and Charles live in Dreadsbury Mansion, and are the
// only people who live therein. A killer always hates his victim, and
// is never richer than his victim. Charles hates no one that aunt
// Agatha hates. Agatha hates everyone except the butler. The butler
// hates everyone not richer than aunt Agatha and the butler hates
// everyone that Agatha hates. No one hates everyone and Agatha is not
// the butler. Who killed aunt Agatha?
//
// **************************************************************************

module AuntAgatha(bool
k_A,k_B,k_C,    // killer is either Agatha, the Butler, or Charles
r_AA,r_AB,r_AC, // the "richer than" relation
r_BA,r_BB,r_BC,
r_CA,r_CB,r_CC,
h_AA,h_AB,h_AC, // the "hates" relation
h_BA,h_BB,h_BC,
h_CA,h_CB,h_CC,
!facts
) {
facts =
// ---- the killer is Agatha, the butler, or Charles:
(k_A | k_B | k_C) &
// ---- a killer always hates the victim:
(k_A -> h_AA) &
(k_B -> h_BA) &
(k_C -> h_CA) &
// ---- a killer is never richer than the victim
(k_A -> !r_AA) &
(k_B -> !r_BA) &
(k_C -> !r_CA) &
// ---- Charles hates no one that aunt Agatha hates.
(h_AA -> !h_CA) &
(h_AB -> !h_CB) &
(h_AC -> !h_CC) &
// ---- Agatha hates everyone except the butler.
(h_AA & !h_AB & h_AC) &
// ---- The butler hates everyone not richer than aunt Agatha
(!r_AA -> h_BA) &
(!r_BA -> h_BB) &
(!r_CA -> h_BC) &
// ---- and the butler hates everyone that Agatha hates.
(h_AA -> h_BA) &
(h_AB -> h_BB) &
(h_AC -> h_BC) &
// ---- No one hates everyone:
(!h_AA | !h_AB | !h_AC) &
(!h_BA | !h_BB | !h_BC) &
(!h_CA | !h_CB | !h_CC);
} satisfies {
hates : assert facts ->
h_AA & !h_AB &  h_AC & h_BA & !h_BB &  h_BC & !h_CA & !h_CC;
richer : assert facts ->
!r_AA & r_BA;
killer : assert facts ->
k_A & !k_B & !k_C;
}
```