Total number of calls to head_norm = 1237608 Total number of calls to hnormOC = 20436 Number of choice points between Beta and BetaPrime : 1143535 Number of Beta reductions : 1449490 Number of Beta-prime reductions : 0 Number of calls to lazy_read from head_norm : 1676206 Number of iterations of lazy_read loop : 17582708 Number of nested suspensions in lazy_read loop : 7461847 Adjusted number of lazy_read iterations : 10120861 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): 479021 R5->R12 occurrences (t is a suspension, nl>l): 64461 R5->R13 occurrences (nl = l): 177617 Total number of these substitutions: 721099 Cases of R5-only and R5->R12 where the skeleton is compound: 54291 Cases of R5-only and R5->R12 where the skeleton is a bound variable: 4542 Cases of R5->R13 where skeleton is not a free variable or constant (and not closed if annotations apply): 5659 Cases of reindexing of compound term avoided because nl=0: 105709 Cases of reindexing of compound term avoided because term is closed (no intersection with above case): 333617 Number of times indices were adjusted: 2014831