Ticks for Basics
  max-open-constraints = 0
  pointers = 0
  pointers (reused) = 0
  max-open-metas = 1
  unequal terms = 2
  metas = 13
  equal terms = 23
Ticks for Pr
  max-open-constraints = 0
  pointers = 0
  pointers (reused) = 0
  max-open-metas = 3
  unequal terms = 17
  metas = 88
  equal terms = 172
Ticks for Nom
  pointers = 0
  pointers (reused) = 0
  max-open-constraints = 2
  max-open-metas = 4
  attempted-constraints = 8
  unequal terms = 75
  metas = 87
  equal terms = 216
Ticks for Kind
  max-open-constraints = 0
  pointers = 0
  pointers (reused) = 0
  max-open-metas = 1
  metas = 10
  equal terms = 20
Ticks for Cxt
  max-open-constraints = 0
  pointers = 0
  pointers (reused) = 0
  max-open-metas = 1
  unequal terms = 5
  metas = 59
  equal terms = 190
Ticks for Loc
  max-open-constraints = 0
  pointers = 0
  pointers (reused) = 0
  max-open-metas = 6
  metas = 145
  unequal terms = 145
  equal terms = 335
Ticks for Term
  pointers = 0
  pointers (reused) = 0
  max-open-constraints = 2
  attempted-constraints = 4
  max-open-metas = 10
  unequal terms = 158
  metas = 241
  equal terms = 615
Ticks for Shift
  pointers = 0
  pointers (reused) = 0
  max-open-constraints = 2
  max-open-metas = 14
  attempted-constraints = 16
  metas = 230
  unequal terms = 412
  equal terms = 639
Ticks for Eta
  pointers = 0
  pointers (reused) = 0
  max-open-constraints = 2
  attempted-constraints = 12
  max-open-metas = 18
  metas = 185
  unequal terms = 270
  equal terms = 486
Ticks for Inst
  pointers = 0
  pointers (reused) = 0
  max-open-constraints = 2
  attempted-constraints = 9
  max-open-metas = 16
  metas = 276
  unequal terms = 534
  equal terms = 948
Ticks for Subst
  pointers = 0
  pointers (reused) = 0
  max-open-constraints = 2
  attempted-constraints = 8
  max-open-metas = 13
  metas = 202
  unequal terms = 315
  equal terms = 576
Ticks for Syntacticosmos
  max-open-constraints = 0
  pointers = 0
  pointers (reused) = 0
  max-open-metas = 1
  metas = 1
  equal terms = 21
Ticks for UntypedLambda
  pointers = 0
  pointers (reused) = 0
  max-open-constraints = 2
  attempted-constraints = 20
  max-open-metas = 23
  metas = 101
  unequal terms = 124
  equal terms = 180
agda -v0 -v profile:100 Syntacticosmos/UntypedLambda.agda --ignore-interfaces -iSyntacticosmos +RTS -K32M -slogs/.tmp 
   3,116,720,416 bytes allocated in the heap
     750,780,368 bytes copied during GC
      29,579,048 bytes maximum residency (37 sample(s))
       1,027,112 bytes maximum slop
              68 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      5947 colls,     0 par    1.12s    1.12s     0.0002s    0.0011s
  Gen  1        37 colls,     0 par    0.79s    0.79s     0.0214s    0.0705s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time    3.32s  (  3.33s elapsed)
  GC      time    1.91s  (  1.91s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time    5.23s  (  5.24s elapsed)

  %GC     time      36.5%  (36.4% elapsed)

  Alloc rate    938,180,228 bytes per MUT second

  Productivity  63.5% of total user, 63.4% of total elapsed

──────────────────────────────────────────────────────────────────
No info
