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 = 487
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 (null) 
   1,729,921,352 bytes allocated in the heap
     330,880,688 bytes copied during GC
      13,587,564 bytes maximum residency (33 sample(s))
         238,368 bytes maximum slop
              34 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      3273 colls,     0 par    0.94s    1.00s     0.0003s    0.0200s
  Gen  1        33 colls,     0 par    0.64s    0.71s     0.0216s    0.0660s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time    3.87s  (  4.05s elapsed)
  GC      time    1.59s  (  1.72s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time    5.46s  (  5.77s elapsed)

  %GC     time      29.1%  (29.7% elapsed)

  Alloc rate    446,915,138 bytes per MUT second

  Productivity  70.9% of total user, 67.1% of total elapsed

──────────────────────────────────────────────────────────────────
Mach kernel version:
	 Darwin Kernel Version 10.8.0: Tue Jun  7 16:33:36 PDT 2011; root:xnu-1504.15.3~1/RELEASE_I386
Kernel configured for up to 2 processors.
2 processors are physically available.
2 processors are logically available.
Processor type: i486 (Intel 80486)
Processors active: 0 1
Primary memory available: 2.00 gigabytes
Default processor set: 112 tasks, 504 threads, 2 processors
Load average: 1.14, Mach factor: 0.88
