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 1,989,901,056 bytes allocated in the heap 787,379,236 bytes copied during GC 90,268,356 bytes maximum residency (19 sample(s)) 931,724 bytes maximum slop 256 MB total memory in use (0 MB lost due to fragmentation) Tot time (elapsed) Avg pause Max pause Gen 0 3784 colls, 0 par 1.06s 1.06s 0.0003s 0.0052s Gen 1 19 colls, 0 par 1.03s 1.12s 0.0591s 0.2684s INIT time 0.00s ( 0.00s elapsed) MUT time 2.78s ( 2.82s elapsed) GC time 2.09s ( 2.19s elapsed) EXIT time 0.00s ( 0.00s elapsed) Total time 4.87s ( 5.01s elapsed) %GC time 42.8% (43.6% elapsed) Alloc rate 713,536,151 bytes per MUT second Productivity 57.2% of total user, 55.7% 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: 109 tasks, 508 threads, 8 processors Load average: 1.33, Mach factor: 6.66