Trace of the subroutine "consequences" in Datalog forward chaining

Assume that variables range over the natural numbers 0, 1, ...

Let R be the rule
M1. geq(U,V) ^ plus(U,X,Y) ^ plus(V,X,Z) => geq(Y,Z).
(That is, if U >= V then U+X >= V+X. Note that, since this is Datalog, we have to use plus as a predicate rather than as a function.)

Let FF be the facts:
M2. geq(A,0). (That is, for all A, A >= 0).
M3. plus(0,B,B). (That is, for all B, 0+B = B.)
M4. plus(2,3,5). The call consequence(R,FF) proceeds as follows:

```Call C1: consequence(R,FF)
T1 := geq(U,V).
NEWFACTS := empty set.
for loop:
F := M2
U := unify(T1,M2) = {{U,A} {V,0}}
R1 := apply(U, drop(T1 from R)) = plus(A,X,Y) ^ plus(0,X,Z) => geq(Y,Z).

Call C1.1 consequences(R1,FF)
T1 := plus(A,X,Y).
NEWFACTS := empty set.
for loop:
F := M2
U := unify(T1,M2) = FAIL
F := M3
U := unify(T1,M3) = {{A,0} {X,Y,B}}
R1 := apply(U, drop(T1 from R)) =  plus(0,B,Z) => geq(B,Z).

Call C1.1.1 consequences(R1,FF)
T1 := plus(0,B,Z).
NEWFACTS := empty set.
for loop:
F := M2
U := unify(T1,M2) = FAIL
F := M3
rename M3 as plus(0,B1,B1)
U := unify(T1,M3) = {B,Z,B1}
R1 := apply(U, drop(T1 from R)) =  geq(B,B).

Call C1.1.1.1 consequences(R1,FF)
C1.1.1.1 returns { geq(B,B) }
/* We have inferred the new fact forall(B) B >= B. */
NEWFACTS := { geq(B,B) }
F := M4
U := unify(T1,M4) = FAIL.
C1.1.1 returns { geq(B,B) }

/* Continue in C1.1 */

NEWFACTS := { geq(B,B) }
F := M4.
U := unify(T1,M4) = {{A,2}, {X,3}, {Y,5}}
R1 := apply(U, drop(T1 from R)) =  plus(0,3,Z) => geq(5,Z).

Call C1.1.2 consequences(R1,FF)
T1 := plus(0,3,Z).
NEWFACTS := empty set.
for loop:
F := M2
U := unify(T1,M2) = FAIL.
F := M3
U := unify(T1,M3) = {{B,Z,3}}
R1 := apply(U, drop(T1 from R)) =  geq(5,3).

Call C1.1.2.1 consequence(R1,FF)
C1.1.2.1 returns { geq(5,3) }
/* We have inferred that 5 >= 3. */
NEWFACTS := { geq(5,3) }
F := M4
U := unify(T1,M2) = FAIL.
C1.1.2 returns { geq(5,3) }

/* Continue in C1.1 */
NEWFACTS := { geq(B,B), geq(5.3) }
C1.1 returns   { geq(B,B), geq(5.3) }

/* Continue in C1 */
NEWFACTS := { geq(B,B), geq(5.3) }
F := M3;
U := unify(T1,M3) = FAIL
F := M4;
U := unify(T1,M4) = FAIL
C1 returns { geq(B,B), geq(5,3) }
```