Trace of the subroutine "consequences" in Datalog forward chaining

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) }