Total number of calls to head_norm = 621878
Total number of calls to hnormOC = 10475
Number of choice points between Beta and BetaPrime : 176271
Number of Beta reductions : 203265
Number of Beta-prime reductions : 0
Number of calls to lazy_read from head_norm : 226399
Number of iterations of lazy_read loop : 3391088
Number of nested suspensions in lazy_read loop : 1528712
Adjusted number of lazy_read iterations : 1862376
Number of calls to lread_withoc from hnormOC : 0
Number of calls to head_norm from lazy_read : 0

The following figures counts the number of substitutions,
i.e.: [[#1,ol,nl,(t,l)::e]] --> [[t,0,nl-l,nil]]:
R5-only occurrences (t is not a suspension, nl>l): 15919
R5->R12 occurrences (t is a suspension, nl>l): 71335
R5->R13 occurrences (nl = l): 12674
Total number of these substitutions: 99928
Cases of R5-only and R5->R12 where the skeleton is compound: 67372
Cases of R5-only and R5->R12 where the skeleton is a bound variable: 2444
Cases of R5->R13 where skeleton is not a free variable or constant (and not closed if annotations apply): 9234
Cases of reindexing of compound term avoided because nl=0: 10621
Cases of reindexing of compound term avoided because term is closed (no intersection with above case): 9390
Number of times indices were adjusted: 428002