Variable Personne : Set.
Variable dans_la_maison : Personne -> Prop.
Variable a_tue : Personne -> Personne -> Prop.
Variable deteste : Personne -> Personne -> Prop.
Variable plus_riche_que : Personne -> Personne -> Prop.
Variable Agatha, Majordome, Charles : Personne.

Axiom meurtre : (EX x:Personne | (dans_la_maison x) /\ (a_tue x Agatha)).
Axiom Agatha_la : (dans_la_maison Agatha).
Axiom Majordome_la : (dans_la_maison Majordome).
Axiom Charles_la : (dans_la_maison Charles).
Axiom presents : (x:Personne) (dans_la_maison x) ->
                              x=Agatha \/ x=Majordome \/ x=Charles.
Axiom haine : (y,x:Personne) (a_tue x y) -> (deteste x y).
Axiom fortune : (y,x:Personne) (a_tue x y) -> ~(plus_riche_que x y).
Axiom Agatha_et_Charles : (x:Personne) (deteste Agatha x) -> ~(deteste Charles x).
Axiom Agatha_deteste_presque_tout_le_monde : (x:Personne) ~x=Majordome -> (deteste Agatha x).
Axiom Majordome_condescendant : (x:Personne) ~(plus_riche_que x Agatha) -> (deteste Majordome x).
Axiom Majordome_fidele : (x:Personne) (deteste Agatha x) -> (deteste Majordome x).
Axiom il_y_a_de_l_espoir : (x:Personne) (EX y:Personne | (dans_la_maison y) /\ ~(deteste x y)).
Axiom faut_pas_confondre : ~(Agatha=Majordome).

Lemma mais_c_est_bien_sur : (a_tue Agatha Agatha).