/*
The following test was found in a published collection.

Matteo, Nicola e Vittorio are engaged to Beatrice, Chiara e Gemma (not
necessarily in this order).  We know that:

1) If Nicola is engaged to Beatrice, then Matteo is engaged to
   to Chiara; 
2) If Matteo is engaged to Chiara, then Vittorio is engaged to
   Beatrice;
3) If Vittorio is not engaged to Gemma, then Nicola is engaged
   to Chiara;
4) If Matteo is engaged to Gemma, then Vittorio is engaged to
   Chiara.
 
We can than say that two of the existing couples (the third one
being identified as a consequence) are:

A) Matteo-Gemma and Vittorio-Chiara;
B) Matteo-Chiara and Vittorio-Beatrice;
C) Nicola-Beatrice and Matteo-Chiara;
D) Matteo-Gemma and Nicola-Beatrice;
E) Vittorio-Beatrice and Nicola-Chiara.

The correct option, according to the solutions given at the end,
is E.

We can check that the proposed answer is not correct, and generate
logical consequences of the stem, in order to identify the correct
option (if any).
*/

Types : woman man.
Predicates: engaged(man,woman).
Objects: Matteo Vittorio Nicola: man - 
	 Beatrice Gemma Chiara: woman .


Theory: 
;; every man is engaged to one and only one woman
forall x:man exists y:woman engaged(x,y),
forall x:man forall y z:woman 
      (engaged(x,y) & engaged(x,z) -> y=z),
;; every woman is engaged to a single man
forall x:woman forall y z:man
      (engaged(y,x) & engaged(z,x) -> y=z),

engaged(Nicola,Beatrice) -> engaged(Matteo,Chiara),
engaged(Matteo,Chiara) -> engaged(Vittorio,Beatrice),
- engaged(Vittorio,Gemma) -> engaged(Nicola,Chiara),
engaged(Matteo,Gemma) -> engaged(Vittorio,Chiara).


Deduce:
   engaged(Vittorio,Beatrice),      
   engaged(Nicola,Chiara),     
   engaged(Matteo,Gemma).

Generate: Derivable.