/* The symbols a, b, c, d, e represent integers.  
The expression `x points to y' means that if x is even, then y is odd,
and if x is odd than y is even.  We know that d points to e,
b points to d and c does not point to b.

What can we add to derive the option "a points to both b and c"?
*/

Types : integer.
Predicates: points(integer,integer) even(integer) odd(integer).
Objects: a b c d e: integer.

; solutions containing "even" or "odd" must be excluded
Abducibles: points.

Theory: 
# definition of "points to"
forall x y : integer 
       (points(x,y) <-> (even(x) <-> odd(y))),
# some knowledge about even and odd numbers
forall x:integer (even(x) <-> - odd(x)),
forall x:integer (even(x) | odd(x)),

# facts 
points(d,e), points(b,d), -points(c,b).

Abduce: points(a,b) & points(a,c).