(still a couple of TODO's with respect to the new
notation).

R=r
DELTA=71  (10 added, 11 deleted, 50 changed)
OCL=15419
CL=15443