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 = 161
  metas = 241
  equal terms = 621
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 = 633
Ticks for Eta
  pointers = 0
  pointers (reused) = 0
  max-open-constraints = 2
  attempted-constraints = 12
  max-open-metas = 18
  metas = 185
  unequal terms = 271
  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 = 535
  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 = 316
  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 
   2,964,476,944 bytes allocated in the heap
     700,339,928 bytes copied during GC
      22,132,664 bytes maximum residency (40 sample(s))
         680,640 bytes maximum slop
              60 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0      5648 colls,     0 par    0.75s    0.75s     0.0001s    0.0008s
  Gen  1        40 colls,     0 par    0.53s    0.55s     0.0138s    0.0402s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time    2.16s  (  2.18s elapsed)
  GC      time    1.27s  (  1.30s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time    3.44s  (  3.49s elapsed)

  %GC     time      37.0%  (37.4% elapsed)

  Alloc rate    1,371,397,339 bytes per MUT second

  Productivity  63.0% of total user, 62.0% of total elapsed

──────────────────────────────────────────────────────────────────
Mach kernel version:
	 Darwin Kernel Version 12.4.0: Wed May  1 17:57:12 PDT 2013; root:xnu-2050.24.15~1/RELEASE_X86_64
Kernel configured for up to 8 processors.
4 processors are physically available.
8 processors are logically available.
Processor type: i486 (Intel 80486)
Processors active: 0 1 2 3 4 5 6 7
Primary memory available: 16.00 gigabytes
Default processor set: 124 tasks, 555 threads, 8 processors
Load average: 1.85, Mach factor: 6.14