/* 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).