Ticks for Chain max-open-constraints = 0 max-open-metas = 7 metas = 85 Ticks for Setoid max-open-constraints = 5 max-open-metas = 24 attempted-constraints = 93 metas = 1560 Ticks for CwF max-open-constraints = 13 max-open-metas = 45 attempted-constraints = 294 metas = 1136 agda -v0 -v profile:100 cwf/CwF.agda --ignore-interfaces -icwf +RTS -slogs/.tmp 2,004,170,168 bytes allocated in the heap 786,727,168 bytes copied during GC 90,239,580 bytes maximum residency (19 sample(s)) 948,632 bytes maximum slop 256 MB total memory in use (0 MB lost due to fragmentation) Tot time (elapsed) Avg pause Max pause Gen 0 3812 colls, 0 par 1.19s 1.20s 0.0003s 0.0064s Gen 1 19 colls, 0 par 1.13s 1.24s 0.0653s 0.2998s INIT time 0.00s ( 0.00s elapsed) MUT time 3.08s ( 3.14s elapsed) GC time 2.33s ( 2.44s elapsed) EXIT time 0.00s ( 0.00s elapsed) Total time 5.42s ( 5.58s elapsed) %GC time 42.9% (43.7% elapsed) Alloc rate 648,440,531 bytes per MUT second Productivity 57.1% of total user, 55.3% of total elapsed ────────────────────────────────────────────────────────────────── Mach kernel version: Darwin Kernel Version 11.3.0: Thu Jan 12 18:47:41 PST 2012; root:xnu-1699.24.23~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: 8.00 gigabytes Default processor set: 134 tasks, 606 threads, 8 processors Load average: 2.81, Mach factor: 5.18