ntung-polysat-4-core

time ./Main +RTS -H256m -N -sstderr -RTS
./Main +RTS -H256m -N -sstderr
testing batcher sort sketch...
number of cnf clauses: 27871
converted poly with 27871 clauses
simplified to 9777 clauses
simplified to 4583 clauses

Finish Parse: 1.083167s
Finish Poly conversion: 0.227719s
Multiply small: 0.270662s
Multiply med-small: 18.033696s

  31,573,855,696 bytes allocated in the heap
     246,450,840 bytes copied during GC
      19,334,392 bytes maximum residency (6 sample(s))
         450,088 bytes maximum slop
             266 MB total memory in use (4 MB lost due to fragmentation)

  Generation 0:   163 collections,   162 parallel,  2.26s,  0.98s elapsed
  Generation 1:     6 collections,     6 parallel,  0.52s,  0.20s elapsed

  Parallel GC work balance: 2.02 (30796932 / 15210123, ideal 4)

                        MUT time (elapsed)       GC time  (elapsed)
  Task  0 (worker) :   15.08s    ( 18.44s)       0.49s    (  0.20s)
  Task  1 (worker) :   15.57s    ( 18.44s)       0.48s    (  0.18s)
  Task  2 (bound)  :    0.94s    ( 18.44s)       0.79s    (  0.42s)
  Task  3 (worker) :    0.00s    ( 18.44s)       0.00s    (  0.00s)
  Task  4 (worker) :   16.13s    ( 18.44s)       0.63s    (  0.23s)
  Task  5 (worker) :   15.95s    ( 18.44s)       0.38s    (  0.15s)

  SPARKS: 56502 (29763 converted, 212 pruned)

  INIT  time    0.00s  (  0.00s elapsed)
  MUT   time   61.96s  ( 18.44s elapsed)
  GC    time    2.78s  (  1.18s elapsed)
  EXIT  time    0.00s  (  0.00s elapsed)
  Total time   64.74s  ( 19.62s elapsed)

  %GC time       4.3%  (6.0% elapsed)

  Alloc rate    509,546,745 bytes per MUT second

  Productivity  95.7% of total user, 315.9% of total elapsed

gc_alloc_block_sync: 115554
whitehole_spin: 0
gen[0].steps[0].sync_large_objects: 359
gen[0].steps[1].sync_large_objects: 54
gen[1].steps[0].sync_large_objects: 342