/* succ(X, Y): X and Y are integers and Y is the successor of X. */
succ(1, 2).   succ(2, 3).   succ(3, 4).   succ(4, 5).
succ(5, 6).   succ(6, 7).   succ(7, 8).   succ(8, 9).
succ(9, 10).  succ(10, 11). succ(11, 12).

/* num(X): X is a numeral. */
num(1).
num(X) :- succ(_, X).

/* plus(X, Y, Z): X + Y = Z */
plus(X, 1, Y) :- succ(X, Y).
plus(X, Y, Z) :- succ(X, A), succ(B, Y), plus(A, B, Z).

/* minus(X, Y, Z): X - Y = Z */
minus(X, 1, Z) :- succ(Z, X).
minus(X, Y, Z) :- succ(A, X), succ(B, Y), minus(A, B, Z).


/* exp(X, Z): X is an expression that evaluates to Z.  An expression
 * is a numeral or list [+, A, B] or [-, A, B], where A and B are
 * expressions. */
exp(X, X) :- num(X).
exp([+, X, Y], Z) :- exp(X, Vx), exp(Y, Vy), plus(Vx, Vy, Z).
exp([-, X, Y], Z) :- exp(X, Vx), exp(Y, Vy), minus(Vx, Vy, Z).


/* Limit depth of search. */
dlim(6).
cd(Goal) :- dlim(Depth), call_with_depth_limit(Goal, Depth, _).