Name | normalized-opb/mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-siena1.opb |
MD5SUM | 575f632072d90cb1b2032661c3842261 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | NO |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 70755 |
Biggest coefficient in the objective function | 536870912000000000000 |
Number of bits for the biggest coefficient in the objective function | 69 |
Sum of the numbers in the objective function | 28224865138562973040640 |
Number of bits of the sum of numbers in the objective function | 75 |
Biggest number in a constraint | 536870912000000000000 |
Number of bits of the biggest number in a constraint | 69 |
Biggest sum of numbers in a constraint | 28224967538562973040640 |
Number of bits of the biggest sum of numbers | 75 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.701893 |
Number of variables | 70755 |
Total number of constraints | 13995 |
Number of constraints which are clauses | 310 |
Number of constraints which are cardinality constraints (but not clauses) | 11776 |
Number of constraints which are nor clauses,nor cardinality constraints | 1909 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 70755 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc21 THE 2005-05-25 21:11:52 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=22355 boxname=wulflinc21 idbench=1171 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: 575f632072d90cb1b2032661c3842261 /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-siena1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-20-10-siena1.opb IDLAUNCH: 22355 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.161 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 840516 kB Buffers: 10052 kB Cached: 162448 kB SwapCached: 968 kB Active: 28204 kB Inactive: 146400 kB HighTotal: 131008 kB HighFree: 49560 kB LowTotal: 903652 kB LowFree: 790956 kB SwapTotal: 2097892 kB SwapFree: 2096008 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5112 kB Slab: 13804 kB Committed_AS: 63912 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-25 21:32:22 (client local time) WITH STATUS 152 IN 1230 SECONDS stats: 22355 7 1230 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c PARSE ERROR! [line 13745] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 4027 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: #########################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################=####################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################### c -- Clauses(.)/Splits(s): ......................................................................................................................................................................................................................................................................................sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss............................... c ---[4094]---> Adder-cost: 154 maxlim: 73728 bits: 18/17 c ---[4092]---> Adder-cost: 172 maxlim: 84992 bits: 18/17 c ---[4090]---> Adder-cost: 308 maxlim: 153600 bits: 19/18 c ---[4088]---> Adder-cost: 212 maxlim: 130048 bits: 18/17 c ---[4085]---> Adder-cost: 120 maxlim: 60416 bits: 17/16 c ---[4083]---> Adder-cost: 84 maxlim: 64512 bits: 17/16 c ---[4081]---> Adder-cost: 106 maxlim: 64512 bits: 17/16 c ---[4079]---> Adder-cost: 120 maxlim: 65536 bits: 18/17 c ---[4077]---> Adder-cost: 112 maxlim: 58368 bits: 17/16 c ---[4075]---> Sorter-cost: 1313 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[4073]---> Adder-cost: 102 maxlim: 86016 bits: 18/17 c ---[4071]---> Sorter-cost: 1191 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[4069]---> Sorter-cost: 1159 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[4067]---> Adder-cost: 188 maxlim: 97280 bits: 18/17 c ---[4065]---> Adder-cost: 190 maxlim: 98304 bits: 18/17 c ---[4063]---> Adder-cost: 176 maxlim: 101376 bits: 18/17 c ---[4061]---> Adder-cost: 122 maxlim: 89088 bits: 18/17 c ---[4059]---> Adder-cost: 154 maxlim: 89088 bits: 18/17 c ---[4057]---> Adder-cost: 66 maxlim: 86016 bits: 18/17 c ---[4055]---> Adder-cost: 148 maxlim: 96256 bits: 18/17 c ---[4053]---> Adder-cost: 150 maxlim: 92160 bits: 18/17 c ---[4051]---> Sorter-cost: 1219 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[4049]---> Sorter-cost: 1200 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[4047]---> Adder-cost: 178 maxlim: 88064 bits: 18/17 c ---[4045]---> Adder-cost: 186 maxlim: 93184 bits: 18/17 c ---[4043]---> Adder-cost: 134 maxlim: 93184 bits: 18/17 c ---[4041]---> Adder-cost: 108 maxlim: 76800 bits: 18/17 c ---[4038]---> Adder-cost: 166 maxlim: 107520 bits: 18/17 c ---[4036]---> Adder-cost: 200 maxlim: 106496 bits: 18/17 c ---[4034]---> Adder-cost: 256 maxlim: 147456 bits: 19/18 c ---[4032]---> Adder-cost: 248 maxlim: 149504 bits: 19/18 c ---[4030]---> Adder-cost: 216 maxlim: 158720 bits: 19/18 c ---[4028]---> Adder-cost: 236 maxlim: 160768 bits: 19/18 c ---[4026]---> Adder-cost: 210 maxlim: 164864 bits: 19/18 c ---[4024]---> Sorter-cost: 995 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[4022]---> Adder-cost: 100 maxlim: 164864 bits: 19/18 c ---[4020]---> Adder-cost: 316 maxlim: 199680 bits: 19/18 c ---[4018]---> Adder-cost: 288 maxlim: 175104 bits: 19/18 c ---[4016]---> Adder-cost: 200 maxlim: 164864 bits: 19/18 c ---[4014]---> Adder-cost: 224 maxlim: 131072 bits: 19/18 c ---[4012]---> Adder-cost: 194 maxlim: 110592 bits: 18/17 c ---[4010]---> Adder-cost: 158 maxlim: 87040 bits: 18/17 c ---[4008]---> Adder-cost: 144 maxlim: 81920 bits: 18/17 c ---[4006]---> Sorter-cost: 450 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[4004]---> Sorter-cost: 361 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[4002]---> Sorter-cost: 1313 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[4000]---> Sorter-cost: 1157 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3998]---> Sorter-cost: 1159 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3996]---> Sorter-cost: 1163 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3994]---> Sorter-cost: 1013 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3992]---> Sorter-cost: 1117 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3990]---> Adder-cost: 154 maxlim: 74752 bits: 18/17 c ---[3988]---> Adder-cost: 200 maxlim: 102400 bits: 18/17 c ---[3986]---> Adder-cost: 162 maxlim: 101376 bits: 18/17 c ---[3984]---> Adder-cost: 180 maxlim: 96256 bits: 18/17 c ---[3982]---> Adder-cost: 136 maxlim: 92160 bits: 18/17 c ---[3980]---> Adder-cost: 106 maxlim: 62464 bits: 17/16 c ---[3978]---> Adder-cost: 110 maxlim: 57344 bits: 17/16 c ---[3975]---> Adder-cost: 82 maxlim: 58368 bits: 17/16 c ---[3973]---> Adder-cost: 232 maxlim: 124928 bits: 18/17 c ---[3971]---> Adder-cost: 260 maxlim: 141312 bits: 19/18 c ---[3969]---> Adder-cost: 92 maxlim: 141312 bits: 19/18 c ---[3967]---> Adder-cost: 272 maxlim: 153600 bits: 19/18 c ---[3965]---> Adder-cost: 226 maxlim: 156672 bits: 19/18 c ---[3963]---> Adder-cost: 272 maxlim: 161792 bits: 19/18 c ---[3961]---> Adder-cost: 92 maxlim: 161792 bits: 19/18 c ---[3959]---> Adder-cost: 266 maxlim: 159744 bits: 19/18 c ---[3957]---> Adder-cost: 266 maxlim: 131072 bits: 19/18 c ---[3955]---> Adder-cost: 182 maxlim: 162816 bits: 19/18 c ---[3953]---> Adder-cost: 166 maxlim: 159744 bits: 19/18 c ---[3951]---> Adder-cost: 94 maxlim: 159744 bits: 19/18 c ---[3949]---> Adder-cost: 250 maxlim: 157696 bits: 19/18 c ---[3947]---> Adder-cost: 92 maxlim: 157696 bits: 19/18 c ---[3945]---> Adder-cost: 180 maxlim: 156672 bits: 19/18 c ---[3943]---> Adder-cost: 96 maxlim: 156672 bits: 19/18 c ---[3941]---> Adder-cost: 216 maxlim: 155648 bits: 19/18 c ---[3939]---> Adder-cost: 96 maxlim: 155648 bits: 19/18 c ---[3937]---> Adder-cost: 102 maxlim: 156672 bits: 19/18 c ---[3935]---> Adder-cost: 90 maxlim: 131072 bits: 19/18 c ---[3933]---> Adder-cost: 96 maxlim: 156672 bits: 19/18 c ---[3931]---> Adder-cost: 96 maxlim: 156672 bits: 19/18 c ---[3929]---> Adder-cost: 96 maxlim: 156672 bits: 19/18 c ---[3927]---> Adder-cost: 260 maxlim: 192512 bits: 19/18 c ---[3924]---> Adder-cost: 146 maxlim: 69632 bits: 18/17 c ---[3922]---> Adder-cost: 94 maxlim: 70656 bits: 18/17 c ---[3920]---> Sorter-cost: 1091 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3918]---> Sorter-cost: 1271 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3916]---> Adder-cost: 168 maxlim: 118784 bits: 18/17 c ---[3914]---> Adder-cost: 110 maxlim: 54272 bits: 17/16 c ---[3912]---> Adder-cost: 100 maxlim: 52224 bits: 17/16 c ---[3910]---> Adder-cost: 96 maxlim: 51200 bits: 17/16 c ---[3908]---> Adder-cost: 156 maxlim: 76800 bits: 18/17 c ---[3906]---> Adder-cost: 136 maxlim: 74752 bits: 18/17 c ---[3903]---> Adder-cost: 98 maxlim: 56320 bits: 17/16 c ---[3901]---> Adder-cost: 46 maxlim: 56320 bits: 17/16 c ---[3899]---> Sorter-cost: 971 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3897]---> Sorter-cost: 632 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3895]---> Sorter-cost: 1155 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3893]---> Sorter-cost: 737 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3891]---> Sorter-cost: 1073 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3888]---> Sorter-cost: 671 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3886]---> Adder-cost: 116 maxlim: 58368 bits: 17/16 c ---[3884]---> Adder-cost: 82 maxlim: 58368 bits: 17/16 c ---[3882]---> Sorter-cost: 1091 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3880]---> Sorter-cost: 671 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3878]---> Sorter-cost: 1154 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3876]---> Sorter-cost: 762 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3874]---> Sorter-cost: 1012 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3872]---> Sorter-cost: 793 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3870]---> Adder-cost: 142 maxlim: 68608 bits: 18/17 c ---[3868]---> Sorter-cost: 1271 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3866]---> Adder-cost: 58 maxlim: 68608 bits: 18/17 c ---[3864]---> Adder-cost: 132 maxlim: 73728 bits: 18/17 c ---[3862]---> Adder-cost: 102 maxlim: 71680 bits: 18/17 c ---[3860]---> Adder-cost: 120 maxlim: 68608 bits: 18/17 c ---[3858]---> Adder-cost: 84 maxlim: 71680 bits: 18/17 c ---[3856]---> Sorter-cost: 375 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3854]---> Sorter-cost: 526 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3852]---> Sorter-cost: 283 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3850]---> Sorter-cost: 414 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3848]---> Adder-cost: 204 maxlim: 101376 bits: 18/17 c ---[3846]---> Adder-cost: 118 maxlim: 102400 bits: 18/17 c ---[3844]---> Sorter-cost: 1061 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3842]---> Sorter-cost: 1036 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3840]---> Adder-cost: 204 maxlim: 101376 bits: 18/17 c ---[3838]---> Adder-cost: 72 maxlim: 101376 bits: 18/17 c ---[3836]---> Adder-cost: 186 maxlim: 94208 bits: 18/17 c ---[3834]---> Adder-cost: 104 maxlim: 95232 bits: 18/17 c ---[3832]---> Adder-cost: 74 maxlim: 94208 bits: 18/17 c ---[3830]---> Adder-cost: 70 maxlim: 94208 bits: 18/17 c ---[3828]---> Sorter-cost: 1287 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3826]---> Sorter-cost: 763 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3823]---> Sorter-cost: 317 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[3821]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[3819]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[3817]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[3815]---> Sorter-cost: 466 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3813]---> Sorter-cost: 1091 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3811]---> Sorter-cost: 1070 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3809]---> Sorter-cost: 1175 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3807]---> Sorter-cost: 1131 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3805]---> Sorter-cost: 1157 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3803]---> Sorter-cost: 446 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3801]---> Sorter-cost: 407 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3799]---> Sorter-cost: 1267 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3797]---> Adder-cost: 154 maxlim: 73728 bits: 18/17 c ---[3794]---> Sorter-cost: 779 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3791]---> Adder-cost: 170 maxlim: 82944 bits: 18/17 c ---[3789]---> Adder-cost: 140 maxlim: 66560 bits: 18/17 c ---[3787]---> Adder-cost: 60 maxlim: 66560 bits: 18/17 c ---[3785]---> Adder-cost: 152 maxlim: 78848 bits: 18/17 c ---[3783]---> Adder-cost: 122 maxlim: 79872 bits: 18/17 c ---[3781]---> Adder-cost: 120 maxlim: 62464 bits: 17/16 c ---[3779]---> Adder-cost: 190 maxlim: 96256 bits: 18/17 c ---[3777]---> Adder-cost: 122 maxlim: 63488 bits: 17/16 c ---[3775]---> Adder-cost: 134 maxlim: 66560 bits: 18/17 c ---[3773]---> Adder-cost: 130 maxlim: 65536 bits: 18/17 c ---[3771]---> Adder-cost: 186 maxlim: 92160 bits: 18/17 c ---[3769]---> Adder-cost: 96 maxlim: 93184 bits: 18/17 c ---[3767]---> Adder-cost: 122 maxlim: 87040 bits: 18/17 c ---[3765]---> Sorter-cost: 1091 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3763]---> Sorter-cost: 896 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3761]---> Sorter-cost: 1135 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3759]---> Adder-cost: 104 maxlim: 52224 bits: 17/16 c ---[3757]---> Adder-cost: 102 maxlim: 59392 bits: 17/16 c ---[3755]---> Sorter-cost: 1061 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3753]---> Sorter-cost: 779 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3751]---> Sorter-cost: 593 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3749]---> Sorter-cost: 680 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3747]---> Sorter-cost: 311 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[3745]---> Sorter-cost: 1084 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3743]---> Adder-cost: 270 maxlim: 131072 bits: 19/18 c ---[3740]---> Sorter-cost: 789 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3738]---> Adder-cost: 126 maxlim: 63488 bits: 17/16 c ---[3736]---> Adder-cost: 52 maxlim: 63488 bits: 17/16 c ---[3734]---> Adder-cost: 52 maxlim: 63488 bits: 17/16 c ---[3732]---> Adder-cost: 52 maxlim: 63488 bits: 17/16 c ---[3730]---> Sorter-cost: 694 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3728]---> Sorter-cost: 604 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3725]---> Adder-cost: 156 maxlim: 76800 bits: 18/17 c ---[3723]---> Adder-cost: 134 maxlim: 67584 bits: 18/17 c ---[3721]---> Adder-cost: 130 maxlim: 68608 bits: 18/17 c ---[3719]---> Sorter-cost: 1185 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3717]---> Sorter-cost: 1185 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3715]---> Adder-cost: 106 maxlim: 51200 bits: 17/16 c ---[3713]---> Adder-cost: 176 maxlim: 87040 bits: 18/17 c ---[3711]---> Adder-cost: 146 maxlim: 82944 bits: 18/17 c ---[3709]---> Adder-cost: 202 maxlim: 98304 bits: 18/17 c ---[3707]---> Adder-cost: 178 maxlim: 99328 bits: 18/17 c ---[3705]---> Adder-cost: 124 maxlim: 62464 bits: 17/16 c ---[3703]---> Adder-cost: 144 maxlim: 79872 bits: 18/17 c ---[3701]---> Sorter-cost: 684 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3699]---> Sorter-cost: 1224 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3697]---> Sorter-cost: 1149 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3695]---> Sorter-cost: 889 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3692]---> Adder-cost: 188 maxlim: 95232 bits: 18/17 c ---[3688]---> Adder-cost: 230 maxlim: 114688 bits: 18/17 c ---[3686]---> Adder-cost: 184 maxlim: 95232 bits: 18/17 c ---[3684]---> Adder-cost: 70 maxlim: 95232 bits: 18/17 c ---[3682]---> Adder-cost: 122 maxlim: 61440 bits: 17/16 c ---[3680]---> Sorter-cost: 1113 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3678]---> Adder-cost: 50 maxlim: 61440 bits: 17/16 c ---[3676]---> Adder-cost: 50 maxlim: 61440 bits: 17/16 c ---[3674]---> Adder-cost: 50 maxlim: 61440 bits: 17/16 c ---[3672]---> Adder-cost: 78 maxlim: 58368 bits: 17/16 c ---[3670]---> Adder-cost: 48 maxlim: 58368 bits: 17/16 c ---[3668]---> Sorter-cost: 317 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[3666]---> Sorter-cost: 373 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3664]---> Sorter-cost: 422 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3662]---> Adder-cost: 160 maxlim: 77824 bits: 18/17 c ---[3660]---> Adder-cost: 118 maxlim: 64512 bits: 17/16 c ---[3658]---> Adder-cost: 124 maxlim: 67584 bits: 18/17 c ---[3656]---> Adder-cost: 96 maxlim: 58368 bits: 17/16 c ---[3654]---> Adder-cost: 184 maxlim: 91136 bits: 18/17 c ---[3652]---> Sorter-cost: 935 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3650]---> Adder-cost: 72 maxlim: 91136 bits: 18/17 c ---[3648]---> Adder-cost: 132 maxlim: 75776 bits: 18/17 c ---[3646]---> Adder-cost: 64 maxlim: 75776 bits: 18/17 c ---[3644]---> Adder-cost: 180 maxlim: 95232 bits: 18/17 c ---[3642]---> Adder-cost: 70 maxlim: 95232 bits: 18/17 c ---[3640]---> Sorter-cost: 1178 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3638]---> Adder-cost: 200 maxlim: 98304 bits: 18/17 c ---[3636]---> Adder-cost: 152 maxlim: 78848 bits: 18/17 c ---[3634]---> Adder-cost: 246 maxlim: 123904 bits: 18/17 c ---[3632]---> Adder-cost: 78 maxlim: 123904 bits: 18/17 c ---[3630]---> Adder-cost: 268 maxlim: 135168 bits: 19/18 c ---[3628]---> Adder-cost: 88 maxlim: 135168 bits: 19/18 c ---[3626]---> Adder-cost: 150 maxlim: 130048 bits: 18/17 c ---[3624]---> Adder-cost: 74 maxlim: 130048 bits: 18/17 c ---[3622]---> Adder-cost: 176 maxlim: 87040 bits: 18/17 c ---[3620]---> Adder-cost: 66 maxlim: 87040 bits: 18/17 c ---[3618]---> Sorter-cost: 1185 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3616]---> Adder-cost: 124 maxlim: 61440 bits: 17/16 c ---[3612]---> Sorter-cost: 1311 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3610]---> Sorter-cost: 803 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3607]---> Adder-cost: 110 maxlim: 53248 bits: 17/16 c ---[3605]---> Sorter-cost: 1159 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3603]---> Sorter-cost: 605 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3601]---> Sorter-cost: 1181 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3599]---> Sorter-cost: 755 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3597]---> Sorter-cost: 755 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3595]---> Sorter-cost: 1017 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3593]---> Sorter-cost: 755 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3591]---> Adder-cost: 126 maxlim: 64512 bits: 17/16 c ---[3589]---> Adder-cost: 124 maxlim: 63488 bits: 17/16 c ---[3587]---> Sorter-cost: 1059 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3585]---> Adder-cost: 52 maxlim: 63488 bits: 17/16 c ---[3583]---> Sorter-cost: 1311 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3581]---> Adder-cost: 108 maxlim: 54272 bits: 17/16 c ---[3579]---> Sorter-cost: 999 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3577]---> Sorter-cost: 690 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3575]---> Sorter-cost: 520 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3573]---> Sorter-cost: 420 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3571]---> Sorter-cost: 1083 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3569]---> Sorter-cost: 406 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3567]---> Sorter-cost: 959 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3565]---> Adder-cost: 146 maxlim: 70656 bits: 18/17 c ---[3563]---> Adder-cost: 156 maxlim: 84992 bits: 18/17 c ---[3561]---> Adder-cost: 68 maxlim: 84992 bits: 18/17 c ---[3559]---> Adder-cost: 156 maxlim: 94208 bits: 18/17 c ---[3557]---> Adder-cost: 156 maxlim: 91136 bits: 18/17 c ---[3555]---> Adder-cost: 72 maxlim: 91136 bits: 18/17 c ---[3553]---> Sorter-cost: 1159 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3551]---> Sorter-cost: 1052 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3549]---> Sorter-cost: 793 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3547]---> Adder-cost: 112 maxlim: 56320 bits: 17/16 c ---[3545]---> Adder-cost: 112 maxlim: 55296 bits: 17/16 c ---[3543]---> Adder-cost: 214 maxlim: 113664 bits: 18/17 c ---[3541]---> Adder-cost: 136 maxlim: 117760 bits: 18/17 c ---[3537]---> Sorter-cost: 470 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3535]---> Sorter-cost: 607 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3533]---> Sorter-cost: 455 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3531]---> Sorter-cost: 628 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3529]---> Sorter-cost: 249 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[3527]---> Sorter-cost: 221 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[3525]---> Sorter-cost: 414 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3523]---> Sorter-cost: 409 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3521]---> Sorter-cost: 283 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3519]---> Adder-cost: 146 maxlim: 69632 bits: 18/17 c ---[3517]---> Adder-cost: 146 maxlim: 70656 bits: 18/17 c ---[3513]---> Sorter-cost: 642 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3511]---> Sorter-cost: 476 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3509]---> Adder-cost: 112 maxlim: 57344 bits: 17/16 c ---[3506]---> Sorter-cost: 1183 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3504]---> Sorter-cost: 800 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3502]---> Sorter-cost: 762 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3500]---> Adder-cost: 120 maxlim: 60416 bits: 17/16 c ---[3498]---> Adder-cost: 48 maxlim: 60416 bits: 17/16 c ---[3496]---> Sorter-cost: 1192 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3494]---> Sorter-cost: 762 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3492]---> Sorter-cost: 1210 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3490]---> Adder-cost: 110 maxlim: 55296 bits: 17/16 c ---[3488]---> Adder-cost: 84 maxlim: 59392 bits: 17/16 c ---[3486]---> Adder-cost: 50 maxlim: 59392 bits: 17/16 c ---[3484]---> Adder-cost: 126 maxlim: 69632 bits: 18/17 c ---[3482]---> Adder-cost: 62 maxlim: 69632 bits: 18/17 c ---[3480]---> Sorter-cost: 1313 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3478]---> Sorter-cost: 1001 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3476]---> Sorter-cost: 1077 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3474]---> Sorter-cost: 667 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3472]---> Sorter-cost: 317 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[3470]---> Adder-cost: 102 maxlim: 54272 bits: 17/16 c ---[3468]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[3466]---> Sorter-cost: 1051 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3464]---> Sorter-cost: 667 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3462]---> Sorter-cost: 852 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3460]---> Sorter-cost: 528 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3458]---> Adder-cost: 172 maxlim: 84992 bits: 18/17 c ---[3456]---> Adder-cost: 68 maxlim: 84992 bits: 18/17 c ---[3454]---> Adder-cost: 120 maxlim: 62464 bits: 17/16 c ---[3452]---> Adder-cost: 68 maxlim: 59392 bits: 17/16 c ---[3450]---> Adder-cost: 104 maxlim: 56320 bits: 17/16 c ---[3448]---> Adder-cost: 82 maxlim: 57344 bits: 17/16 c ---[3446]---> Adder-cost: 146 maxlim: 69632 bits: 18/17 c ---[3444]---> Adder-cost: 126 maxlim: 65536 bits: 18/17 c ---[3442]---> Adder-cost: 110 maxlim: 55296 bits: 17/16 c ---[3440]---> Adder-cost: 110 maxlim: 56320 bits: 17/16 c ---[3438]---> Adder-cost: 130 maxlim: 73728 bits: 18/17 c ---[3436]---> Adder-cost: 84 maxlim: 72704 bits: 18/17 c ---[3434]---> Adder-cost: 126 maxlim: 70656 bits: 18/17 c ---[3432]---> Adder-cost: 82 maxlim: 73728 bits: 18/17 c ---[3430]---> Adder-cost: 282 maxlim: 141312 bits: 19/18 c ---[3428]---> Adder-cost: 136 maxlim: 68608 bits: 18/17 c ---[3426]---> Adder-cost: 92 maxlim: 141312 bits: 19/18 c ---[3424]---> Adder-cost: 246 maxlim: 136192 bits: 19/18 c ---[3422]---> Adder-cost: 88 maxlim: 136192 bits: 19/18 c ---[3420]---> Adder-cost: 186 maxlim: 137216 bits: 19/18 c ---[3416]---> Sorter-cost: 1221 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3414]---> Sorter-cost: 800 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3412]---> Adder-cost: 58 maxlim: 68608 bits: 18/17 c ---[3410]---> Adder-cost: 184 maxlim: 90112 bits: 18/17 c ---[3408]---> Sorter-cost: 789 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3406]---> Sorter-cost: 723 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3404]---> Sorter-cost: 1156 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3402]---> Sorter-cost: 799 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3400]---> Sorter-cost: 466 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3398]---> Sorter-cost: 450 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3396]---> Sorter-cost: 440 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3394]---> Sorter-cost: 285 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[3392]---> Sorter-cost: 1024 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3390]---> Adder-cost: 138 maxlim: 65536 bits: 18/17 c ---[3388]---> Sorter-cost: 862 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3386]---> Sorter-cost: 1237 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3384]---> Sorter-cost: 688 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3382]---> Adder-cost: 154 maxlim: 74752 bits: 18/17 c ---[3380]---> Adder-cost: 134 maxlim: 68608 bits: 18/17 c ---[3378]---> Adder-cost: 58 maxlim: 68608 bits: 18/17 c ---[3376]---> Adder-cost: 154 maxlim: 79872 bits: 18/17 c ---[3374]---> Adder-cost: 96 maxlim: 58368 bits: 17/16 c ---[3372]---> Adder-cost: 104 maxlim: 59392 bits: 17/16 c ---[3370]---> Adder-cost: 176 maxlim: 99328 bits: 18/17 c ---[3368]---> Adder-cost: 62 maxlim: 65536 bits: 18/17 c ---[3366]---> Adder-cost: 134 maxlim: 70656 bits: 18/17 c ---[3364]---> Adder-cost: 94 maxlim: 71680 bits: 18/17 c ---[3362]---> Adder-cost: 118 maxlim: 63488 bits: 17/16 c ---[3360]---> Adder-cost: 116 maxlim: 64512 bits: 17/16 c ---[3358]---> Adder-cost: 94 maxlim: 56320 bits: 17/16 c ---[3356]---> Adder-cost: 126 maxlim: 66560 bits: 18/17 c ---[3354]---> Adder-cost: 144 maxlim: 74752 bits: 18/17 c ---[3352]---> Adder-cost: 182 maxlim: 100352 bits: 18/17 c ---[3350]---> Adder-cost: 164 maxlim: 100352 bits: 18/17 c ---[3348]---> Adder-cost: 148 maxlim: 97280 bits: 18/17 c ---[3346]---> Adder-cost: 124 maxlim: 67584 bits: 18/17 c ---[3344]---> Adder-cost: 116 maxlim: 63488 bits: 17/16 c ---[3342]---> Adder-cost: 106 maxlim: 59392 bits: 17/16 c ---[3340]---> Sorter-cost: 1192 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3338]---> Sorter-cost: 968 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3336]---> Sorter-cost: 981 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3334]---> Sorter-cost: 672 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3332]---> Sorter-cost: 510 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3330]---> Sorter-cost: 452 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3328]---> Sorter-cost: 401 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3326]---> Adder-cost: 60 maxlim: 67584 bits: 18/17 c ---[3324]---> Sorter-cost: 489 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3322]---> Adder-cost: 144 maxlim: 69632 bits: 18/17 c ---[3320]---> Adder-cost: 212 maxlim: 109568 bits: 18/17 c ---[3318]---> Adder-cost: 78 maxlim: 109568 bits: 18/17 c ---[3316]---> Adder-cost: 200 maxlim: 106496 bits: 18/17 c ---[3313]---> Sorter-cost: 317 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[3310]---> Adder-cost: 202 maxlim: 101376 bits: 18/17 c ---[3308]---> Adder-cost: 92 maxlim: 70656 bits: 18/17 c ---[3306]---> Adder-cost: 160 maxlim: 102400 bits: 18/17 c ---[3304]---> Adder-cost: 76 maxlim: 102400 bits: 18/17 c ---[3301]---> Sorter-cost: 720 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3299]---> Sorter-cost: 441 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3297]---> Sorter-cost: 259 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[3295]---> Adder-cost: 110 maxlim: 54272 bits: 17/16 c ---[3293]---> Adder-cost: 160 maxlim: 86016 bits: 18/17 c ---[3291]---> Adder-cost: 60 maxlim: 70656 bits: 18/17 c ---[3289]---> Adder-cost: 114 maxlim: 78848 bits: 18/17 c ---[3287]---> Adder-cost: 170 maxlim: 81920 bits: 18/17 c ---[3285]---> Sorter-cost: 1287 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3283]---> Sorter-cost: 849 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3281]---> Adder-cost: 110 maxlim: 55296 bits: 17/16 c ---[3279]---> Adder-cost: 150 maxlim: 76800 bits: 18/17 c ---[3277]---> Adder-cost: 92 maxlim: 77824 bits: 18/17 c ---[3275]---> Adder-cost: 154 maxlim: 79872 bits: 18/17 c ---[3273]---> Adder-cost: 138 maxlim: 68608 bits: 18/17 c ---[3271]---> Adder-cost: 192 maxlim: 97280 bits: 18/17 c ---[3269]---> Adder-cost: 160 maxlim: 103424 bits: 18/17 c ---[3267]---> Adder-cost: 150 maxlim: 97280 bits: 18/17 c ---[3265]---> Adder-cost: 64 maxlim: 97280 bits: 18/17 c ---[3263]---> Adder-cost: 108 maxlim: 95232 bits: 18/17 c ---[3259]---> Adder-cost: 218 maxlim: 109568 bits: 18/17 c ---[3256]---> Adder-cost: 58 maxlim: 68608 bits: 18/17 c ---[3254]---> Adder-cost: 186 maxlim: 114688 bits: 18/17 c ---[3250]---> Adder-cost: 152 maxlim: 74752 bits: 18/17 c ---[3248]---> Adder-cost: 60 maxlim: 74752 bits: 18/17 c ---[3244]---> Adder-cost: 282 maxlim: 140288 bits: 19/18 c ---[3242]---> Adder-cost: 272 maxlim: 136192 bits: 19/18 c ---[3240]---> Adder-cost: 214 maxlim: 133120 bits: 19/18 c ---[3238]---> Adder-cost: 250 maxlim: 129024 bits: 18/17 c ---[3234]---> Adder-cost: 154 maxlim: 77824 bits: 18/17 c ---[3232]---> Adder-cost: 112 maxlim: 60416 bits: 17/16 c ---[3230]---> Adder-cost: 112 maxlim: 61440 bits: 17/16 c ---[3228]---> Sorter-cost: 1271 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3226]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3224]---> Sorter-cost: 885 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3222]---> Sorter-cost: 468 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3220]---> Sorter-cost: 382 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3218]---> Adder-cost: 76 maxlim: 129024 bits: 18/17 c ---[3216]---> Sorter-cost: 583 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3214]---> Sorter-cost: 438 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3212]---> Sorter-cost: 401 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3210]---> Adder-cost: 112 maxlim: 55296 bits: 17/16 c ---[3208]---> Adder-cost: 92 maxlim: 56320 bits: 17/16 c ---[3206]---> Adder-cost: 62 maxlim: 55296 bits: 17/16 c ---[3204]---> Adder-cost: 88 maxlim: 57344 bits: 17/16 c ---[3202]---> Adder-cost: 292 maxlim: 145408 bits: 19/18 c ---[3200]---> Adder-cost: 274 maxlim: 161792 bits: 19/18 c ---[3198]---> Adder-cost: 310 maxlim: 165888 bits: 19/18 c ---[3196]---> Adder-cost: 198 maxlim: 108544 bits: 18/17 c ---[3194]---> Sorter-cost: 1192 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3192]---> Adder-cost: 156 maxlim: 75776 bits: 18/17 c ---[3190]---> Adder-cost: 136 maxlim: 79872 bits: 18/17 c ---[3188]---> Adder-cost: 128 maxlim: 75776 bits: 18/17 c ---[3186]---> Adder-cost: 92 maxlim: 59392 bits: 17/16 c ---[3184]---> Sorter-cost: 789 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3182]---> Sorter-cost: 1071 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3180]---> Sorter-cost: 1143 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3178]---> Sorter-cost: 1269 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3176]---> Adder-cost: 112 maxlim: 55296 bits: 17/16 c ---[3174]---> Sorter-cost: 655 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3172]---> Adder-cost: 78 maxlim: 108544 bits: 18/17 c ---[3170]---> Adder-cost: 118 maxlim: 58368 bits: 17/16 c ---[3168]---> Adder-cost: 68 maxlim: 58368 bits: 17/16 c ---[3166]---> Adder-cost: 116 maxlim: 62464 bits: 17/16 c ---[3164]---> Adder-cost: 162 maxlim: 86016 bits: 18/17 c ---[3162]---> Adder-cost: 160 maxlim: 101376 bits: 18/17 c ---[3160]---> Adder-cost: 170 maxlim: 114688 bits: 18/17 c ---[3158]---> Adder-cost: 174 maxlim: 119808 bits: 18/17 c ---[3155]---> Adder-cost: 156 maxlim: 75776 bits: 18/17 c ---[3153]---> Adder-cost: 178 maxlim: 100352 bits: 18/17 c ---[3150]---> Sorter-cost: 317 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[3148]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[3146]---> Sorter-cost: 605 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3144]---> Sorter-cost: 405 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3142]---> Adder-cost: 178 maxlim: 89088 bits: 18/17 c ---[3140]---> Adder-cost: 280 maxlim: 141312 bits: 19/18 c ---[3137]---> Adder-cost: 106 maxlim: 53248 bits: 17/16 c ---[3135]---> Adder-cost: 106 maxlim: 55296 bits: 17/16 c ---[3133]---> Adder-cost: 72 maxlim: 100352 bits: 18/17 c ---[3131]---> Adder-cost: 74 maxlim: 52224 bits: 17/16 c ---[3129]---> Adder-cost: 44 maxlim: 52224 bits: 17/16 c ---[3127]---> Sorter-cost: 1192 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3125]---> Sorter-cost: 677 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3123]---> Sorter-cost: 1017 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3121]---> Sorter-cost: 1299 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3119]---> Sorter-cost: 1267 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3117]---> Sorter-cost: 409 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3115]---> Adder-cost: 140 maxlim: 70656 bits: 18/17 c ---[3113]---> Sorter-cost: 458 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3111]---> Sorter-cost: 332 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3109]---> Sorter-cost: 442 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3107]---> Sorter-cost: 418 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3105]---> Sorter-cost: 955 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3103]---> Sorter-cost: 1004 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3101]---> Sorter-cost: 1040 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3099]---> Sorter-cost: 956 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3097]---> Adder-cost: 172 maxlim: 84992 bits: 18/17 c ---[3095]---> Adder-cost: 60 maxlim: 70656 bits: 18/17 c ---[3093]---> Adder-cost: 68 maxlim: 84992 bits: 18/17 c ---[3091]---> Adder-cost: 170 maxlim: 92160 bits: 18/17 c ---[3089]---> Adder-cost: 146 maxlim: 107520 bits: 18/17 c ---[3087]---> Adder-cost: 136 maxlim: 106496 bits: 18/17 c ---[3085]---> Adder-cost: 174 maxlim: 95232 bits: 18/17 c ---[3083]---> Adder-cost: 252 maxlim: 135168 bits: 19/18 c ---[3081]---> Adder-cost: 232 maxlim: 133120 bits: 19/18 c ---[3079]---> Adder-cost: 170 maxlim: 103424 bits: 18/17 c ---[3077]---> Adder-cost: 170 maxlim: 99328 bits: 18/17 c ---[3075]---> Adder-cost: 160 maxlim: 98304 bits: 18/17 c ---[3073]---> Adder-cost: 156 maxlim: 84992 bits: 18/17 c ---[3071]---> Adder-cost: 228 maxlim: 122880 bits: 18/17 c ---[3069]---> Adder-cost: 226 maxlim: 141312 bits: 19/18 c ---[3067]---> Adder-cost: 92 maxlim: 141312 bits: 19/18 c ---[3065]---> Adder-cost: 146 maxlim: 75776 bits: 18/17 c ---[3063]---> Adder-cost: 164 maxlim: 84992 bits: 18/17 c ---[3061]---> Adder-cost: 96 maxlim: 79872 bits: 18/17 c ---[3059]---> Adder-cost: 234 maxlim: 122880 bits: 18/17 c ---[3057]---> Adder-cost: 206 maxlim: 117760 bits: 18/17 c ---[3055]---> Adder-cost: 76 maxlim: 117760 bits: 18/17 c ---[3053]---> Adder-cost: 188 maxlim: 114688 bits: 18/17 c ---[3051]---> Adder-cost: 68 maxlim: 84992 bits: 18/17 c ---[3049]---> Adder-cost: 190 maxlim: 112640 bits: 18/17 c ---[3047]---> Adder-cost: 74 maxlim: 112640 bits: 18/17 c ---[3045]---> Adder-cost: 108 maxlim: 84992 bits: 18/17 c ---[3043]---> Sorter-cost: 1035 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3041]---> Sorter-cost: 713 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3039]---> Sorter-cost: 409 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3036]---> Sorter-cost: 1311 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3034]---> Sorter-cost: 803 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3032]---> Adder-cost: 260 maxlim: 134144 bits: 19/18 c ---[3030]---> Adder-cost: 184 maxlim: 93184 bits: 18/17 c ---[3028]---> Adder-cost: 104 maxlim: 54272 bits: 17/16 c ---[3026]---> Sorter-cost: 1261 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[3022]---> Adder-cost: 310 maxlim: 155648 bits: 19/18 c ---[3020]---> Adder-cost: 302 maxlim: 151552 bits: 19/18 c ---[3018]---> Adder-cost: 280 maxlim: 153600 bits: 19/18 c ---[3016]---> Adder-cost: 92 maxlim: 153600 bits: 19/18 c ---[3012]---> Adder-cost: 208 maxlim: 104448 bits: 18/17 c ---[3010]---> Adder-cost: 146 maxlim: 93184 bits: 18/17 c ---[3008]---> Adder-cost: 64 maxlim: 93184 bits: 18/17 c ---[3006]---> Adder-cost: 64 maxlim: 93184 bits: 18/17 c ---[3004]---> Adder-cost: 64 maxlim: 93184 bits: 18/17 c ---[3000]---> Adder-cost: 140 maxlim: 69632 bits: 18/17 c ---[2998]---> Adder-cost: 116 maxlim: 72704 bits: 18/17 c ---[2996]---> Adder-cost: 278 maxlim: 138240 bits: 19/18 c ---[2994]---> Adder-cost: 146 maxlim: 74752 bits: 18/17 c ---[2992]---> Adder-cost: 178 maxlim: 98304 bits: 18/17 c ---[2990]---> Sorter-cost: 468 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2988]---> Sorter-cost: 311 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2986]---> Adder-cost: 234 maxlim: 117760 bits: 18/17 c ---[2984]---> Adder-cost: 136 maxlim: 65536 bits: 18/17 c ---[2982]---> Sorter-cost: 1030 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2980]---> Sorter-cost: 915 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2978]---> Sorter-cost: 1010 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2976]---> Adder-cost: 224 maxlim: 112640 bits: 18/17 c ---[2974]---> Adder-cost: 88 maxlim: 138240 bits: 19/18 c ---[2972]---> Adder-cost: 250 maxlim: 129024 bits: 18/17 c ---[2970]---> Adder-cost: 206 maxlim: 103424 bits: 18/17 c ---[2968]---> Adder-cost: 148 maxlim: 98304 bits: 18/17 c ---[2966]---> Sorter-cost: 1061 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2964]---> Sorter-cost: 672 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2962]---> Sorter-cost: 1147 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2960]---> Adder-cost: 112 maxlim: 56320 bits: 17/16 c ---[2958]---> Adder-cost: 202 maxlim: 100352 bits: 18/17 c ---[2956]---> Adder-cost: 104 maxlim: 52224 bits: 17/16 c ---[2954]---> Adder-cost: 110 maxlim: 57344 bits: 17/16 c ---[2952]---> Adder-cost: 206 maxlim: 104448 bits: 18/17 c ---[2950]---> Sorter-cost: 1131 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2948]---> Sorter-cost: 1067 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2946]---> Sorter-cost: 921 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2944]---> Sorter-cost: 446 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2942]---> Sorter-cost: 365 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2940]---> Adder-cost: 228 maxlim: 114688 bits: 18/17 c ---[2937]---> Sorter-cost: 1076 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2935]---> Sorter-cost: 983 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2933]---> Sorter-cost: 1191 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2931]---> Adder-cost: 74 maxlim: 104448 bits: 18/17 c ---[2927]---> Adder-cost: 140 maxlim: 66560 bits: 18/17 c ---[2925]---> Adder-cost: 148 maxlim: 77824 bits: 18/17 c ---[2923]---> Adder-cost: 64 maxlim: 77824 bits: 18/17 c ---[2921]---> Adder-cost: 122 maxlim: 74752 bits: 18/17 c ---[2919]---> Adder-cost: 168 maxlim: 82944 bits: 18/17 c ---[2917]---> Adder-cost: 68 maxlim: 82944 bits: 18/17 c ---[2913]---> Adder-cost: 100 maxlim: 104448 bits: 18/17 c ---[2911]---> Adder-cost: 224 maxlim: 122880 bits: 18/17 c ---[2909]---> Adder-cost: 94 maxlim: 56320 bits: 17/16 c ---[2906]---> Sorter-cost: 317 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2904]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2902]---> Sorter-cost: 221 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2900]---> Sorter-cost: 221 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2898]---> Sorter-cost: 592 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2896]---> Sorter-cost: 476 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2894]---> Sorter-cost: 595 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2892]---> Adder-cost: 74 maxlim: 104448 bits: 18/17 c ---[2890]---> Sorter-cost: 607 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2888]---> Sorter-cost: 987 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2886]---> Sorter-cost: 607 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2884]---> Sorter-cost: 676 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2882]---> Sorter-cost: 402 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2880]---> Sorter-cost: 999 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2878]---> Sorter-cost: 607 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2876]---> Sorter-cost: 855 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2874]---> Sorter-cost: 607 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2872]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2870]---> Adder-cost: 122 maxlim: 102400 bits: 18/17 c ---[2868]---> Sorter-cost: 755 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2866]---> Adder-cost: 216 maxlim: 108544 bits: 18/17 c ---[2864]---> Adder-cost: 78 maxlim: 108544 bits: 18/17 c ---[2862]---> Adder-cost: 198 maxlim: 111616 bits: 18/17 c ---[2860]---> Adder-cost: 134 maxlim: 110592 bits: 18/17 c ---[2858]---> Adder-cost: 144 maxlim: 111616 bits: 18/17 c ---[2856]---> Adder-cost: 94 maxlim: 111616 bits: 18/17 c ---[2854]---> Adder-cost: 238 maxlim: 121856 bits: 18/17 c ---[2852]---> Adder-cost: 80 maxlim: 121856 bits: 18/17 c ---[2850]---> Adder-cost: 210 maxlim: 117760 bits: 18/17 c ---[2848]---> Adder-cost: 76 maxlim: 102400 bits: 18/17 c ---[2846]---> Adder-cost: 154 maxlim: 114688 bits: 18/17 c ---[2844]---> Adder-cost: 142 maxlim: 68608 bits: 18/17 c ---[2842]---> Adder-cost: 128 maxlim: 69632 bits: 18/17 c ---[2840]---> Adder-cost: 114 maxlim: 71680 bits: 18/17 c ---[2838]---> Adder-cost: 60 maxlim: 71680 bits: 18/17 c ---[2836]---> Adder-cost: 234 maxlim: 117760 bits: 18/17 c ---[2834]---> Adder-cost: 150 maxlim: 114688 bits: 18/17 c ---[2832]---> Adder-cost: 206 maxlim: 107520 bits: 18/17 c ---[2830]---> Adder-cost: 78 maxlim: 107520 bits: 18/17 c ---[2828]---> Adder-cost: 78 maxlim: 107520 bits: 18/17 c ---[2826]---> Adder-cost: 76 maxlim: 102400 bits: 18/17 c ---[2824]---> Adder-cost: 102 maxlim: 110592 bits: 18/17 c ---[2822]---> Adder-cost: 96 maxlim: 116736 bits: 18/17 c ---[2819]---> Adder-cost: 126 maxlim: 64512 bits: 17/16 c ---[2817]---> Adder-cost: 174 maxlim: 86016 bits: 18/17 c ---[2815]---> Adder-cost: 140 maxlim: 81920 bits: 18/17 c ---[2813]---> Adder-cost: 136 maxlim: 76800 bits: 18/17 c ---[2811]---> Adder-cost: 76 maxlim: 102400 bits: 18/17 c ---[2809]---> Adder-cost: 122 maxlim: 74752 bits: 18/17 c ---[2807]---> Adder-cost: 106 maxlim: 59392 bits: 17/16 c ---[2805]---> Sorter-cost: 1192 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2803]---> Adder-cost: 120 maxlim: 60416 bits: 17/16 c ---[2801]---> Sorter-cost: 1250 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2799]---> Adder-cost: 76 maxlim: 102400 bits: 18/17 c ---[2797]---> Adder-cost: 208 maxlim: 104448 bits: 18/17 c ---[2795]---> Adder-cost: 158 maxlim: 105472 bits: 18/17 c ---[2793]---> Adder-cost: 190 maxlim: 94208 bits: 18/17 c ---[2791]---> Adder-cost: 182 maxlim: 93184 bits: 18/17 c ---[2789]---> Adder-cost: 152 maxlim: 98304 bits: 18/17 c ---[2787]---> Sorter-cost: 434 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2784]---> Adder-cost: 196 maxlim: 106496 bits: 18/17 c ---[2782]---> Adder-cost: 220 maxlim: 119808 bits: 18/17 c ---[2780]---> Adder-cost: 188 maxlim: 111616 bits: 18/17 c ---[2778]---> Adder-cost: 106 maxlim: 52224 bits: 17/16 c ---[2776]---> Adder-cost: 108 maxlim: 57344 bits: 17/16 c ---[2773]---> Sorter-cost: 1287 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2771]---> Sorter-cost: 999 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2769]---> Sorter-cost: 887 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2767]---> Sorter-cost: 553 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2765]---> Sorter-cost: 1120 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2763]---> Sorter-cost: 317 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2760]---> Sorter-cost: 1030 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2758]---> Sorter-cost: 601 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2756]---> Sorter-cost: 455 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2753]---> Adder-cost: 274 maxlim: 136192 bits: 19/18 c ---[2751]---> Adder-cost: 238 maxlim: 122880 bits: 18/17 c ---[2749]---> Adder-cost: 106 maxlim: 51200 bits: 17/16 c ---[2746]---> Sorter-cost: 1084 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2744]---> Sorter-cost: 751 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2742]---> Adder-cost: 132 maxlim: 68608 bits: 18/17 c ---[2740]---> Sorter-cost: 1313 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2736]---> Sorter-cost: 803 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2734]---> Adder-cost: 60 maxlim: 57344 bits: 17/16 c ---[2732]---> Adder-cost: 154 maxlim: 73728 bits: 18/17 c ---[2730]---> Adder-cost: 146 maxlim: 74752 bits: 18/17 c ---[2728]---> Sorter-cost: 1192 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2726]---> Sorter-cost: 762 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2723]---> Adder-cost: 154 maxlim: 74752 bits: 18/17 c ---[2721]---> Adder-cost: 60 maxlim: 74752 bits: 18/17 c ---[2719]---> Adder-cost: 52 maxlim: 57344 bits: 17/16 c ---[2716]---> Adder-cost: 212 maxlim: 108544 bits: 18/17 c ---[2713]---> Adder-cost: 142 maxlim: 68608 bits: 18/17 c ---[2709]---> Adder-cost: 286 maxlim: 147456 bits: 19/18 c ---[2707]---> Adder-cost: 114 maxlim: 58368 bits: 17/16 c ---[2703]---> Adder-cost: 148 maxlim: 71680 bits: 18/17 c ---[2700]---> Sorter-cost: 1073 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2698]---> Sorter-cost: 971 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2695]---> Adder-cost: 48 maxlim: 58368 bits: 17/16 c ---[2692]---> Adder-cost: 272 maxlim: 133120 bits: 19/18 c ---[2688]---> Adder-cost: 248 maxlim: 125952 bits: 18/17 c ---[2684]---> Adder-cost: 238 maxlim: 118784 bits: 18/17 c ---[2682]---> Sorter-cost: 1223 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2680]---> Adder-cost: 98 maxlim: 53248 bits: 17/16 c ---[2676]---> Adder-cost: 274 maxlim: 135168 bits: 19/18 c ---[2674]---> Adder-cost: 176 maxlim: 89088 bits: 18/17 c ---[2670]---> Adder-cost: 276 maxlim: 143360 bits: 19/18 c ---[2666]---> Sorter-cost: 1117 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2664]---> Adder-cost: 48 maxlim: 53248 bits: 17/16 c ---[2661]---> Adder-cost: 110 maxlim: 54272 bits: 17/16 c ---[2659]---> Adder-cost: 88 maxlim: 55296 bits: 17/16 c ---[2657]---> Adder-cost: 168 maxlim: 82944 bits: 18/17 c ---[2653]---> Sorter-cost: 971 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2651]---> Adder-cost: 360 maxlim: 184320 bits: 19/18 c ---[2649]---> Adder-cost: 330 maxlim: 182272 bits: 19/18 c ---[2645]---> Adder-cost: 198 maxlim: 108544 bits: 18/17 c ---[2643]---> Adder-cost: 290 maxlim: 154624 bits: 19/18 c ---[2641]---> Adder-cost: 176 maxlim: 86016 bits: 18/17 c ---[2637]---> Adder-cost: 150 maxlim: 89088 bits: 18/17 c ---[2635]---> Sorter-cost: 831 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2631]---> Adder-cost: 238 maxlim: 118784 bits: 18/17 c ---[2628]---> Adder-cost: 124 maxlim: 62464 bits: 17/16 c ---[2626]---> Adder-cost: 48 maxlim: 62464 bits: 17/16 c ---[2622]---> Adder-cost: 118 maxlim: 61440 bits: 17/16 c ---[2620]---> Sorter-cost: 882 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2618]---> Adder-cost: 124 maxlim: 61440 bits: 17/16 c ---[2614]---> Adder-cost: 112 maxlim: 61440 bits: 17/16 c ---[2612]---> Sorter-cost: 999 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2610]---> Sorter-cost: 791 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2608]---> Sorter-cost: 1091 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2605]---> Sorter-cost: 845 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2603]---> Sorter-cost: 908 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2599]---> Adder-cost: 144 maxlim: 70656 bits: 18/17 c ---[2597]---> Adder-cost: 222 maxlim: 111616 bits: 18/17 c ---[2595]---> Adder-cost: 130 maxlim: 112640 bits: 18/17 c ---[2591]---> Adder-cost: 158 maxlim: 80896 bits: 18/17 c ---[2588]---> Sorter-cost: 787 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2585]---> Adder-cost: 106 maxlim: 52224 bits: 17/16 c ---[2583]---> Adder-cost: 274 maxlim: 137216 bits: 19/18 c ---[2581]---> Adder-cost: 140 maxlim: 138240 bits: 19/18 c ---[2577]---> Adder-cost: 184 maxlim: 90112 bits: 18/17 c ---[2573]---> Adder-cost: 264 maxlim: 138240 bits: 19/18 c ---[2571]---> Sorter-cost: 784 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2568]---> Adder-cost: 162 maxlim: 80896 bits: 18/17 c ---[2566]---> Adder-cost: 62 maxlim: 80896 bits: 18/17 c ---[2562]---> Adder-cost: 184 maxlim: 91136 bits: 18/17 c ---[2560]---> Sorter-cost: 450 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2558]---> Sorter-cost: 227 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2556]---> Sorter-cost: 703 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2554]---> Sorter-cost: 221 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2552]---> Sorter-cost: 221 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2550]---> Sorter-cost: 466 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2548]---> Sorter-cost: 593 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2546]---> Sorter-cost: 439 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2544]---> Sorter-cost: 412 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2541]---> Adder-cost: 122 maxlim: 61440 bits: 17/16 c ---[2539]---> Sorter-cost: 563 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2537]---> Adder-cost: 98 maxlim: 60416 bits: 17/16 c ---[2534]---> Sorter-cost: 619 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2532]---> Sorter-cost: 468 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2530]---> Sorter-cost: 332 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2528]---> Sorter-cost: 669 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2526]---> Adder-cost: 278 maxlim: 146432 bits: 19/18 c ---[2524]---> Adder-cost: 88 maxlim: 146432 bits: 19/18 c ---[2520]---> Adder-cost: 148 maxlim: 74752 bits: 18/17 c ---[2516]---> Adder-cost: 176 maxlim: 88064 bits: 18/17 c ---[2514]---> Adder-cost: 184 maxlim: 90112 bits: 18/17 c ---[2512]---> Adder-cost: 72 maxlim: 90112 bits: 18/17 c ---[2510]---> Sorter-cost: 563 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2506]---> Adder-cost: 152 maxlim: 77824 bits: 18/17 c ---[2503]---> Adder-cost: 182 maxlim: 91136 bits: 18/17 c ---[2501]---> Sorter-cost: 1157 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2498]---> Adder-cost: 170 maxlim: 82944 bits: 18/17 c ---[2496]---> Adder-cost: 298 maxlim: 149504 bits: 19/18 c ---[2494]---> Adder-cost: 210 maxlim: 105472 bits: 18/17 c ---[2492]---> Sorter-cost: 1244 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2490]---> Sorter-cost: 818 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2486]---> Adder-cost: 290 maxlim: 149504 bits: 19/18 c ---[2484]---> Sorter-cost: 470 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2481]---> Sorter-cost: 332 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2479]---> Sorter-cost: 785 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2477]---> Sorter-cost: 407 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2475]---> Adder-cost: 74 maxlim: 105472 bits: 18/17 c ---[2473]---> Adder-cost: 204 maxlim: 102400 bits: 18/17 c ---[2471]---> Adder-cost: 134 maxlim: 78848 bits: 18/17 c ---[2469]---> Sorter-cost: 999 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2467]---> Sorter-cost: 896 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2465]---> Sorter-cost: 623 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2463]---> Sorter-cost: 923 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2461]---> Adder-cost: 154 maxlim: 73728 bits: 18/17 c ---[2459]---> Adder-cost: 252 maxlim: 129024 bits: 18/17 c ---[2457]---> Adder-cost: 112 maxlim: 104448 bits: 18/17 c ---[2454]---> Adder-cost: 154 maxlim: 82944 bits: 18/17 c ---[2452]---> Adder-cost: 130 maxlim: 81920 bits: 18/17 c ---[2448]---> Sorter-cost: 1269 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2446]---> Sorter-cost: 931 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2444]---> Adder-cost: 180 maxlim: 105472 bits: 18/17 c ---[2441]---> Adder-cost: 152 maxlim: 76800 bits: 18/17 c ---[2439]---> Sorter-cost: 271 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2437]---> Sorter-cost: 599 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2435]---> Sorter-cost: 908 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2433]---> Sorter-cost: 905 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2429]---> Sorter-cost: 1215 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2427]---> Adder-cost: 146 maxlim: 74752 bits: 18/17 c ---[2425]---> Sorter-cost: 1182 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2423]---> Sorter-cost: 271 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2421]---> Sorter-cost: 418 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2419]---> Sorter-cost: 443 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2417]---> Sorter-cost: 584 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2415]---> Sorter-cost: 413 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2413]---> Adder-cost: 130 maxlim: 72704 bits: 18/17 c ---[2411]---> Sorter-cost: 436 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2409]---> Sorter-cost: 332 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2407]---> Sorter-cost: 395 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2404]---> Sorter-cost: 1313 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2402]---> Sorter-cost: 1279 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2400]---> Sorter-cost: 737 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2398]---> Adder-cost: 144 maxlim: 70656 bits: 18/17 c ---[2395]---> Adder-cost: 202 maxlim: 99328 bits: 18/17 c ---[2393]---> Adder-cost: 70 maxlim: 99328 bits: 18/17 c ---[2391]---> Sorter-cost: 271 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2388]---> Adder-cost: 118 maxlim: 60416 bits: 17/16 c ---[2384]---> Adder-cost: 166 maxlim: 87040 bits: 18/17 c ---[2382]---> Adder-cost: 136 maxlim: 69632 bits: 18/17 c ---[2380]---> Adder-cost: 132 maxlim: 76800 bits: 18/17 c ---[2378]---> Adder-cost: 62 maxlim: 69632 bits: 18/17 c ---[2375]---> Adder-cost: 66 maxlim: 87040 bits: 18/17 c ---[2371]---> Sorter-cost: 1034 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2369]---> Sorter-cost: 639 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2367]---> Sorter-cost: 1138 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2365]---> Adder-cost: 136 maxlim: 70656 bits: 18/17 c ---[2363]---> Sorter-cost: 1143 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2361]---> Adder-cost: 122 maxlim: 61440 bits: 17/16 c ---[2359]---> Adder-cost: 138 maxlim: 67584 bits: 18/17 c ---[2356]---> Adder-cost: 92 maxlim: 62464 bits: 17/16 c ---[2354]---> Adder-cost: 84 maxlim: 71680 bits: 18/17 c ---[2352]---> Sorter-cost: 269 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2350]---> Adder-cost: 298 maxlim: 151552 bits: 19/18 c ---[2348]---> Adder-cost: 302 maxlim: 153600 bits: 19/18 c ---[2346]---> Adder-cost: 222 maxlim: 110592 bits: 18/17 c ---[2343]---> Adder-cost: 186 maxlim: 95232 bits: 18/17 c ---[2341]---> Adder-cost: 228 maxlim: 125952 bits: 18/17 c ---[2339]---> Sorter-cost: 412 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2337]---> Sorter-cost: 314 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2335]---> Sorter-cost: 647 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2333]---> Adder-cost: 194 maxlim: 101376 bits: 18/17 c ---[2329]---> Sorter-cost: 1211 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2327]---> Adder-cost: 152 maxlim: 75776 bits: 18/17 c ---[2325]---> Adder-cost: 104 maxlim: 59392 bits: 17/16 c ---[2323]---> Sorter-cost: 450 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2321]---> Sorter-cost: 1153 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2319]---> Adder-cost: 164 maxlim: 99328 bits: 18/17 c ---[2316]---> Adder-cost: 218 maxlim: 108544 bits: 18/17 c ---[2314]---> Adder-cost: 214 maxlim: 118784 bits: 18/17 c ---[2312]---> Adder-cost: 80 maxlim: 118784 bits: 18/17 c ---[2310]---> Adder-cost: 174 maxlim: 86016 bits: 18/17 c ---[2308]---> Adder-cost: 66 maxlim: 86016 bits: 18/17 c ---[2306]---> Sorter-cost: 999 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2302]---> Adder-cost: 200 maxlim: 99328 bits: 18/17 c ---[2300]---> Sorter-cost: 1159 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2298]---> Sorter-cost: 1016 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2296]---> Sorter-cost: 677 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2294]---> Adder-cost: 184 maxlim: 90112 bits: 18/17 c ---[2292]---> Sorter-cost: 1311 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2290]---> Adder-cost: 126 maxlim: 63488 bits: 17/16 c ---[2288]---> Adder-cost: 252 maxlim: 136192 bits: 19/18 c ---[2285]---> Sorter-cost: 900 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2283]---> Adder-cost: 70 maxlim: 99328 bits: 18/17 c ---[2281]---> Sorter-cost: 528 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2279]---> Sorter-cost: 1259 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2276]---> Sorter-cost: 450 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2274]---> Adder-cost: 138 maxlim: 72704 bits: 18/17 c ---[2272]---> Sorter-cost: 314 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2270]---> Adder-cost: 188 maxlim: 98304 bits: 18/17 c ---[2267]---> Sorter-cost: 411 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2265]---> Sorter-cost: 271 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2263]---> Adder-cost: 106 maxlim: 54272 bits: 17/16 c ---[2261]---> Sorter-cost: 985 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2257]---> Adder-cost: 108 maxlim: 97280 bits: 18/17 c ---[2255]---> Adder-cost: 168 maxlim: 86016 bits: 18/17 c ---[2253]---> Sorter-cost: 688 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2249]---> Sorter-cost: 694 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2247]---> Sorter-cost: 520 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2245]---> Sorter-cost: 440 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2241]---> Adder-cost: 158 maxlim: 96256 bits: 18/17 c ---[2239]---> Sorter-cost: 1048 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2235]---> Sorter-cost: 779 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2233]---> Sorter-cost: 395 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2230]---> Sorter-cost: 460 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2226]---> Adder-cost: 108 maxlim: 95232 bits: 18/17 c ---[2224]---> Sorter-cost: 407 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2220]---> Adder-cost: 168 maxlim: 81920 bits: 18/17 c ---[2217]---> Adder-cost: 144 maxlim: 69632 bits: 18/17 c ---[2214]---> Adder-cost: 110 maxlim: 54272 bits: 17/16 c ---[2212]---> Adder-cost: 70 maxlim: 95232 bits: 18/17 c ---[2210]---> Adder-cost: 112 maxlim: 60416 bits: 17/16 c ---[2208]---> Adder-cost: 48 maxlim: 60416 bits: 17/16 c ---[2204]---> Adder-cost: 314 maxlim: 162816 bits: 19/18 c ---[2202]---> Adder-cost: 92 maxlim: 162816 bits: 19/18 c ---[2200]---> Adder-cost: 310 maxlim: 166912 bits: 19/18 c ---[2198]---> Adder-cost: 100 maxlim: 166912 bits: 19/18 c ---[2195]---> Adder-cost: 100 maxlim: 166912 bits: 19/18 c ---[2193]---> Adder-cost: 100 maxlim: 166912 bits: 19/18 c ---[2190]---> Sorter-cost: 619 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2188]---> Adder-cost: 112 maxlim: 56320 bits: 17/16 c ---[2186]---> Adder-cost: 92 maxlim: 54272 bits: 17/16 c ---[2184]---> Adder-cost: 78 maxlim: 51200 bits: 17/16 c ---[2182]---> Adder-cost: 278 maxlim: 141312 bits: 19/18 c ---[2178]---> Adder-cost: 128 maxlim: 68608 bits: 18/17 c ---[2176]---> Adder-cost: 96 maxlim: 66560 bits: 18/17 c ---[2174]---> Adder-cost: 136 maxlim: 65536 bits: 18/17 c ---[2170]---> Adder-cost: 86 maxlim: 53248 bits: 17/16 c ---[2168]---> Adder-cost: 364 maxlim: 184320 bits: 19/18 c ---[2166]---> Sorter-cost: 1219 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2162]---> Adder-cost: 178 maxlim: 89088 bits: 18/17 c ---[2160]---> Sorter-cost: 791 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2157]---> Adder-cost: 110 maxlim: 53248 bits: 17/16 c ---[2155]---> Adder-cost: 142 maxlim: 72704 bits: 18/17 c ---[2153]---> Adder-cost: 116 maxlim: 70656 bits: 18/17 c ---[2151]---> Adder-cost: 254 maxlim: 153600 bits: 19/18 c ---[2148]---> Adder-cost: 148 maxlim: 73728 bits: 18/17 c ---[2146]---> Adder-cost: 102 maxlim: 55296 bits: 17/16 c ---[2142]---> Adder-cost: 230 maxlim: 119808 bits: 18/17 c ---[2140]---> Adder-cost: 80 maxlim: 119808 bits: 18/17 c ---[2137]---> Sorter-cost: 460 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2134]---> Adder-cost: 168 maxlim: 152576 bits: 19/18 c ---[2131]---> Sorter-cost: 617 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2129]---> Sorter-cost: 548 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2127]---> Sorter-cost: 532 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2125]---> Sorter-cost: 706 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2123]---> Sorter-cost: 544 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2121]---> Sorter-cost: 1178 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2119]---> Adder-cost: 118 maxlim: 58368 bits: 17/16 c ---[2116]---> Sorter-cost: 1183 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2114]---> Adder-cost: 146 maxlim: 155648 bits: 19/18 c ---[2110]---> Sorter-cost: 411 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2106]---> Adder-cost: 124 maxlim: 61440 bits: 17/16 c ---[2104]---> Adder-cost: 50 maxlim: 61440 bits: 17/16 c ---[2102]---> Sorter-cost: 1053 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2100]---> Sorter-cost: 613 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2098]---> Adder-cost: 96 maxlim: 155648 bits: 19/18 c ---[2096]---> Sorter-cost: 455 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2092]---> Sorter-cost: 680 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2090]---> Adder-cost: 172 maxlim: 87040 bits: 18/17 c ---[2088]---> Adder-cost: 226 maxlim: 119808 bits: 18/17 c ---[2086]---> Adder-cost: 142 maxlim: 73728 bits: 18/17 c ---[2084]---> Adder-cost: 62 maxlim: 73728 bits: 18/17 c ---[2079]---> Sorter-cost: 554 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2075]---> Sorter-cost: 931 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2072]---> Sorter-cost: 271 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2070]---> Sorter-cost: 221 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2068]---> Adder-cost: 154 maxlim: 73728 bits: 18/17 c ---[2066]---> Sorter-cost: 221 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2063]---> Sorter-cost: 1147 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2061]---> Adder-cost: 110 maxlim: 53248 bits: 17/16 c ---[2057]---> Sorter-cost: 727 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2053]---> Sorter-cost: 363 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2051]---> Adder-cost: 88 maxlim: 73728 bits: 18/17 c ---[2048]---> Sorter-cost: 1084 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2045]---> Sorter-cost: 445 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2043]---> Sorter-cost: 261 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2041]---> Sorter-cost: 221 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2039]---> Sorter-cost: 534 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2036]---> Sorter-cost: 694 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2034]---> Adder-cost: 108 maxlim: 61440 bits: 17/16 c ---[2032]---> Adder-cost: 186 maxlim: 93184 bits: 18/17 c ---[2030]---> Adder-cost: 84 maxlim: 93184 bits: 18/17 c ---[2027]---> Sorter-cost: 1157 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2025]---> Sorter-cost: 771 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2023]---> Sorter-cost: 408 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2021]---> Sorter-cost: 698 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2017]---> Adder-cost: 172 maxlim: 90112 bits: 18/17 c ---[2015]---> Sorter-cost: 997 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2012]---> Sorter-cost: 1074 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2010]---> Sorter-cost: 987 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2008]---> Adder-cost: 172 maxlim: 86016 bits: 18/17 c ---[2006]---> Sorter-cost: 595 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2004]---> Sorter-cost: 466 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2002]---> Sorter-cost: 676 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2000]---> Sorter-cost: 443 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1998]---> Sorter-cost: 245 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1996]---> Sorter-cost: 375 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1993]---> Sorter-cost: 1133 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1991]---> Adder-cost: 108 maxlim: 79872 bits: 18/17 c ---[1989]---> Sorter-cost: 269 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1987]---> Sorter-cost: 231 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1985]---> Sorter-cost: 720 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1983]---> Sorter-cost: 704 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1980]---> Sorter-cost: 624 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1978]---> Sorter-cost: 315 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1976]---> Adder-cost: 150 maxlim: 77824 bits: 18/17 c ---[1973]---> Sorter-cost: 418 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1971]---> Adder-cost: 230 maxlim: 115712 bits: 18/17 c ---[1969]---> Adder-cost: 160 maxlim: 114688 bits: 18/17 c ---[1967]---> Adder-cost: 204 maxlim: 116736 bits: 18/17 c ---[1964]---> Sorter-cost: 468 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1962]---> Adder-cost: 64 maxlim: 77824 bits: 18/17 c ---[1959]---> Sorter-cost: 684 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1957]---> Sorter-cost: 510 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1955]---> Sorter-cost: 589 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1951]---> Adder-cost: 204 maxlim: 104448 bits: 18/17 c ---[1949]---> Sorter-cost: 1155 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1947]---> Adder-cost: 104 maxlim: 51200 bits: 17/16 c ---[1943]---> Sorter-cost: 1289 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1940]---> Sorter-cost: 271 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1938]---> Sorter-cost: 271 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1936]---> Sorter-cost: 221 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1933]---> Sorter-cost: 267 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1931]---> Adder-cost: 44 maxlim: 51200 bits: 17/16 c ---[1929]---> Sorter-cost: 221 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1926]---> Sorter-cost: 657 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1923]---> Sorter-cost: 733 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1920]---> Sorter-cost: 1159 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1917]---> Sorter-cost: 894 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1915]---> Sorter-cost: 1246 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1913]---> Sorter-cost: 951 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1911]---> Sorter-cost: 1129 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1908]---> Sorter-cost: 1061 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1906]---> Sorter-cost: 671 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1903]---> Adder-cost: 114 maxlim: 59392 bits: 17/16 c ---[1901]---> Adder-cost: 50 maxlim: 59392 bits: 17/16 c ---[1899]---> Adder-cost: 90 maxlim: 58368 bits: 17/16 c ---[1896]---> Adder-cost: 108 maxlim: 55296 bits: 17/16 c ---[1894]---> Sorter-cost: 607 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1892]---> Sorter-cost: 411 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1890]---> Sorter-cost: 1265 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1888]---> Adder-cost: 102 maxlim: 58368 bits: 17/16 c ---[1886]---> Sorter-cost: 1229 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1884]---> Adder-cost: 136 maxlim: 73728 bits: 18/17 c ---[1881]---> Sorter-cost: 657 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1879]---> Sorter-cost: 1209 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1877]---> Sorter-cost: 706 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1875]---> Sorter-cost: 448 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1873]---> Adder-cost: 304 maxlim: 163840 bits: 19/18 c ---[1871]---> Adder-cost: 124 maxlim: 61440 bits: 17/16 c ---[1868]---> Sorter-cost: 314 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1865]---> Sorter-cost: 1271 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1863]---> Adder-cost: 152 maxlim: 82944 bits: 18/17 c ---[1861]---> Sorter-cost: 680 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1857]---> Adder-cost: 146 maxlim: 79872 bits: 18/17 c ---[1855]---> Sorter-cost: 1128 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1852]---> Adder-cost: 212 maxlim: 111616 bits: 18/17 c ---[1849]---> Sorter-cost: 445 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1847]---> Sorter-cost: 697 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1845]---> Sorter-cost: 1287 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1843]---> Adder-cost: 132 maxlim: 75776 bits: 18/17 c ---[1839]---> Sorter-cost: 361 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1837]---> Sorter-cost: 653 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1834]---> Adder-cost: 106 maxlim: 52224 bits: 17/16 c ---[1831]---> Adder-cost: 44 maxlim: 52224 bits: 17/16 c ---[1828]---> Sorter-cost: 1178 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1825]---> Sorter-cost: 939 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1823]---> Sorter-cost: 1085 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1821]---> Sorter-cost: 1089 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1819]---> Sorter-cost: 577 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1817]---> Sorter-cost: 670 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1815]---> Sorter-cost: 883 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1813]---> Adder-cost: 218 maxlim: 110592 bits: 18/17 c ---[1811]---> Adder-cost: 192 maxlim: 101376 bits: 18/17 c ---[1809]---> Adder-cost: 114 maxlim: 57344 bits: 17/16 c ---[1806]---> Sorter-cost: 439 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1804]---> Sorter-cost: 450 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1802]---> Sorter-cost: 265 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1800]---> Sorter-cost: 261 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1798]---> Sorter-cost: 1301 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1796]---> Sorter-cost: 363 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1794]---> Sorter-cost: 1246 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1792]---> Sorter-cost: 249 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1790]---> Adder-cost: 174 maxlim: 89088 bits: 18/17 c ---[1788]---> Sorter-cost: 406 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1786]---> Sorter-cost: 296 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1784]---> Sorter-cost: 296 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1782]---> Sorter-cost: 581 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1780]---> Sorter-cost: 455 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1778]---> Sorter-cost: 455 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1774]---> Adder-cost: 124 maxlim: 62464 bits: 17/16 c ---[1772]---> Adder-cost: 174 maxlim: 108544 bits: 18/17 c ---[1770]---> Adder-cost: 164 maxlim: 82944 bits: 18/17 c ---[1767]---> Sorter-cost: 611 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1765]---> Sorter-cost: 305 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1763]---> Sorter-cost: 684 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1761]---> Sorter-cost: 991 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1759]---> Adder-cost: 242 maxlim: 123904 bits: 18/17 c ---[1757]---> Sorter-cost: 599 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1754]---> Sorter-cost: 657 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1752]---> Adder-cost: 110 maxlim: 55296 bits: 17/16 c ---[1748]---> Sorter-cost: 1248 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1746]---> Sorter-cost: 923 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1744]---> Adder-cost: 200 maxlim: 125952 bits: 18/17 c ---[1742]---> Adder-cost: 104 maxlim: 52224 bits: 17/16 c ---[1740]---> Adder-cost: 108 maxlim: 60416 bits: 17/16 c ---[1738]---> Adder-cost: 110 maxlim: 64512 bits: 17/16 c ---[1736]---> Adder-cost: 102 maxlim: 58368 bits: 17/16 c ---[1734]---> Sorter-cost: 999 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1732]---> Sorter-cost: 963 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1730]---> Sorter-cost: 1159 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1728]---> Adder-cost: 268 maxlim: 134144 bits: 19/18 c ---[1726]---> Adder-cost: 110 maxlim: 53248 bits: 17/16 c ---[1722]---> Sorter-cost: 975 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1720]---> Sorter-cost: 1073 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1717]---> Adder-cost: 154 maxlim: 73728 bits: 18/17 c ---[1714]---> Adder-cost: 242 maxlim: 138240 bits: 19/18 c ---[1712]---> Sorter-cost: 464 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1710]---> Sorter-cost: 259 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1707]---> Sorter-cost: 991 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1704]---> Sorter-cost: 937 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1702]---> Adder-cost: 264 maxlim: 141312 bits: 19/18 c ---[1700]---> Sorter-cost: 1132 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1698]---> Sorter-cost: 1016 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1694]---> Adder-cost: 110 maxlim: 64512 bits: 17/16 c ---[1692]---> Sorter-cost: 313 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1690]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1686]---> Sorter-cost: 636 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1683]---> Sorter-cost: 973 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1681]---> Sorter-cost: 668 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1678]---> Adder-cost: 160 maxlim: 78848 bits: 18/17 c ---[1676]---> Adder-cost: 60 maxlim: 78848 bits: 18/17 c ---[1674]---> Adder-cost: 110 maxlim: 56320 bits: 17/16 c ---[1672]---> Sorter-cost: 1275 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1669]---> Sorter-cost: 464 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1667]---> Adder-cost: 156 maxlim: 77824 bits: 18/17 c ---[1665]---> Adder-cost: 94 maxlim: 79872 bits: 18/17 c ---[1663]---> Adder-cost: 266 maxlim: 136192 bits: 19/18 c ---[1661]---> Adder-cost: 226 maxlim: 135168 bits: 19/18 c ---[1659]---> Adder-cost: 280 maxlim: 142336 bits: 19/18 c ---[1657]---> Adder-cost: 92 maxlim: 142336 bits: 19/18 c ---[1655]---> Sorter-cost: 559 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1652]---> Sorter-cost: 414 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1650]---> Sorter-cost: 904 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1648]---> Adder-cost: 140 maxlim: 65536 bits: 18/17 c ---[1646]---> Sorter-cost: 1091 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1644]---> Sorter-cost: 1082 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1641]---> Adder-cost: 244 maxlim: 128000 bits: 18/17 c ---[1639]---> Sorter-cost: 462 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1637]---> Adder-cost: 110 maxlim: 56320 bits: 17/16 c ---[1635]---> Sorter-cost: 1031 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1633]---> Adder-cost: 46 maxlim: 56320 bits: 17/16 c ---[1629]---> Sorter-cost: 581 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1627]---> Sorter-cost: 622 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1625]---> Sorter-cost: 476 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1623]---> Sorter-cost: 227 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1621]---> Sorter-cost: 221 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1618]---> Adder-cost: 180 maxlim: 91136 bits: 18/17 c ---[1616]---> Adder-cost: 104 maxlim: 52224 bits: 17/16 c ---[1614]---> Adder-cost: 158 maxlim: 84992 bits: 18/17 c ---[1611]---> Adder-cost: 142 maxlim: 67584 bits: 18/17 c ---[1609]---> Adder-cost: 200 maxlim: 99328 bits: 18/17 c ---[1607]---> Adder-cost: 70 maxlim: 99328 bits: 18/17 c ---[1603]---> Adder-cost: 124 maxlim: 62464 bits: 17/16 c ---[1599]---> Sorter-cost: 775 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1596]---> Sorter-cost: 1008 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1594]---> Sorter-cost: 967 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1592]---> Adder-cost: 152 maxlim: 90112 bits: 18/17 c ---[1589]---> Adder-cost: 282 maxlim: 159744 bits: 19/18 c ---[1587]---> Adder-cost: 106 maxlim: 58368 bits: 17/16 c ---[1585]---> Adder-cost: 84 maxlim: 59392 bits: 17/16 c ---[1583]---> Adder-cost: 108 maxlim: 61440 bits: 17/16 c ---[1580]---> Sorter-cost: 968 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1578]---> Sorter-cost: 613 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1576]---> Sorter-cost: 291 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1574]---> Sorter-cost: 1068 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1572]---> Adder-cost: 112 maxlim: 60416 bits: 17/16 c ---[1570]---> Sorter-cost: 873 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1568]---> Sorter-cost: 672 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1566]---> Sorter-cost: 495 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1564]---> Sorter-cost: 495 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1562]---> Adder-cost: 108 maxlim: 53248 bits: 17/16 c ---[1560]---> Adder-cost: 48 maxlim: 53248 bits: 17/16 c ---[1556]---> Adder-cost: 104 maxlim: 64512 bits: 17/16 c ---[1553]---> Sorter-cost: 894 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1550]---> Adder-cost: 220 maxlim: 111616 bits: 18/17 c ---[1548]---> Sorter-cost: 664 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1546]---> Sorter-cost: 510 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1544]---> Sorter-cost: 1313 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1542]---> Sorter-cost: 1175 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1539]---> Sorter-cost: 655 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1537]---> Sorter-cost: 309 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1535]---> Sorter-cost: 1221 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1533]---> Sorter-cost: 791 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1529]---> Sorter-cost: 259 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1527]---> Sorter-cost: 1057 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1525]---> Sorter-cost: 1103 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1523]---> Adder-cost: 236 maxlim: 122880 bits: 18/17 c ---[1521]---> Sorter-cost: 528 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1519]---> Adder-cost: 206 maxlim: 119808 bits: 18/17 c ---[1514]---> Sorter-cost: 1293 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1512]---> Adder-cost: 138 maxlim: 66560 bits: 18/17 c ---[1509]---> Sorter-cost: 448 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1507]---> Sorter-cost: 593 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1505]---> Sorter-cost: 811 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1502]---> Sorter-cost: 1069 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1500]---> Adder-cost: 122 maxlim: 67584 bits: 18/17 c ---[1498]---> Sorter-cost: 1183 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1496]---> Sorter-cost: 1281 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1494]---> Adder-cost: 124 maxlim: 61440 bits: 17/16 c ---[1492]---> Sorter-cost: 375 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1490]---> Sorter-cost: 553 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1488]---> Adder-cost: 202 maxlim: 102400 bits: 18/17 c ---[1486]---> Adder-cost: 138 maxlim: 101376 bits: 18/17 c ---[1484]---> Sorter-cost: 999 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1482]---> Adder-cost: 170 maxlim: 89088 bits: 18/17 c ---[1480]---> Adder-cost: 146 maxlim: 72704 bits: 18/17 c ---[1478]---> Adder-cost: 318 maxlim: 159744 bits: 19/18 c ---[1476]---> Adder-cost: 114 maxlim: 58368 bits: 17/16 c ---[1474]---> Adder-cost: 86 maxlim: 52224 bits: 17/16 c ---[1472]---> Sorter-cost: 1091 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1470]---> Sorter-cost: 882 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1468]---> Adder-cost: 146 maxlim: 69632 bits: 18/17 c ---[1466]---> Adder-cost: 158 maxlim: 78848 bits: 18/17 c ---[1464]---> Adder-cost: 206 maxlim: 104448 bits: 18/17 c ---[1462]---> Sorter-cost: 1246 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1460]---> Adder-cost: 224 maxlim: 119808 bits: 18/17 c ---[1458]---> Adder-cost: 186 maxlim: 96256 bits: 18/17 c ---[1456]---> Adder-cost: 236 maxlim: 126976 bits: 18/17 c ---[1454]---> Adder-cost: 192 maxlim: 106496 bits: 18/17 c ---[1452]---> Adder-cost: 156 maxlim: 75776 bits: 18/17 c ---[1450]---> Adder-cost: 172 maxlim: 87040 bits: 18/17 c ---[1448]---> Sorter-cost: 553 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1446]---> Adder-cost: 238 maxlim: 129024 bits: 18/17 c ---[1444]---> Sorter-cost: 1207 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1441]---> Sorter-cost: 553 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1439]---> Adder-cost: 102 maxlim: 51200 bits: 17/16 c ---[1437]---> Adder-cost: 92 maxlim: 57344 bits: 17/16 c ---[1435]---> Adder-cost: 76 maxlim: 54272 bits: 17/16 c ---[1433]---> Adder-cost: 214 maxlim: 110592 bits: 18/17 c ---[1431]---> Adder-cost: 256 maxlim: 135168 bits: 19/18 c ---[1429]---> Adder-cost: 262 maxlim: 141312 bits: 19/18 c ---[1427]---> Adder-cost: 354 maxlim: 199680 bits: 19/18 c ---[1425]---> Adder-cost: 230 maxlim: 152576 bits: 19/18 c ---[1423]---> Adder-cost: 338 maxlim: 196608 bits: 19/18 c ---[1421]---> Adder-cost: 264 maxlim: 194560 bits: 19/18 c ---[1419]---> Adder-cost: 310 maxlim: 191488 bits: 19/18 c ---[1417]---> Adder-cost: 276 maxlim: 178176 bits: 19/18 c ---[1415]---> Adder-cost: 266 maxlim: 151552 bits: 19/18 c ---[1413]---> Adder-cost: 274 maxlim: 171008 bits: 19/18 c ---[1411]---> Adder-cost: 366 maxlim: 203776 bits: 19/18 c ---[1409]---> Adder-cost: 364 maxlim: 218112 bits: 19/18 c ---[1407]---> Adder-cost: 346 maxlim: 216064 bits: 19/18 c ---[1405]---> Adder-cost: 306 maxlim: 195584 bits: 19/18 c ---[1403]---> Adder-cost: 216 maxlim: 142336 bits: 19/18 c ---[1401]---> Adder-cost: 198 maxlim: 118784 bits: 18/17 c ---[1399]---> Adder-cost: 184 maxlim: 110592 bits: 18/17 c ---[1397]---> Adder-cost: 196 maxlim: 120832 bits: 18/17 c ---[1395]---> Adder-cost: 184 maxlim: 115712 bits: 18/17 c ---[1393]---> Adder-cost: 168 maxlim: 94208 bits: 18/17 c ---[1391]---> Adder-cost: 272 maxlim: 142336 bits: 19/18 c ---[1389]---> Adder-cost: 186 maxlim: 143360 bits: 19/18 c ---[1387]---> Adder-cost: 252 maxlim: 141312 bits: 19/18 c ---[1385]---> Adder-cost: 168 maxlim: 146432 bits: 19/18 c ---[1383]---> Adder-cost: 190 maxlim: 144384 bits: 19/18 c ---[1381]---> Adder-cost: 196 maxlim: 148480 bits: 19/18 c ---[1379]---> Adder-cost: 250 maxlim: 156672 bits: 19/18 c ---[1377]---> Adder-cost: 180 maxlim: 154624 bits: 19/18 c ---[1375]---> Adder-cost: 108 maxlim: 53248 bits: 17/16 c ---[1373]---> Adder-cost: 208 maxlim: 140288 bits: 19/18 c ---[1371]---> Adder-cost: 210 maxlim: 141312 bits: 19/18 c ---[1369]---> Adder-cost: 170 maxlim: 136192 bits: 19/18 c ---[1367]---> Adder-cost: 228 maxlim: 135168 bits: 19/18 c ---[1365]---> Adder-cost: 216 maxlim: 139264 bits: 19/18 c ---[1363]---> Adder-cost: 156 maxlim: 136192 bits: 19/18 c ---[1361]---> Adder-cost: 178 maxlim: 111616 bits: 18/17 c ---[1359]---> Adder-cost: 156 maxlim: 80896 bits: 18/17 c ---[1357]---> Adder-cost: 180 maxlim: 109568 bits: 18/17 c ---[1356]---> Adder-cost: 2306 maxlim: 1125375 bits: 22/21 c ---[1355]---> Adder-cost: 11112 maxlim: 5775359 bits: 23/23 c ---[1353]---> Adder-cost: 257 maxlim: 135167 bits: 19/18 c ---[1352]---> Adder-cost: 275 maxlim: 146431 bits: 19/18 c ---[1351]---> Adder-cost: 309 maxlim: 149503 bits: 19/18 c ---[1349]---> Adder-cost: 323 maxlim: 157695 bits: 19/18 c ---[1348]---> Adder-cost: 345 maxlim: 173055 bits: 19/18 c ---[1346]---> Adder-cost: 520 maxlim: 244735 bits: 19/18 c ---[1345]---> Adder-cost: 303 maxlim: 150527 bits: 19/18 c ---[1343]---> Adder-cost: 496 maxlim: 243711 bits: 19/18 c ---[1337]---> Adder-cost: 351 maxlim: 162815 bits: 19/18 c ---[1335]---> Adder-cost: 496 maxlim: 254975 bits: 19/18 c ---[1334]---> Adder-cost: 603 maxlim: 301055 bits: 20/19 c ---[1330]---> Adder-cost: 406 maxlim: 195583 bits: 19/18 c ---[1329]---> Adder-cost: 2972 maxlim: 1595391 bits: 22/21 c ---[1325]---> Adder-cost: 725 maxlim: 359423 bits: 20/19 c ---[1324]---> Adder-cost: 3446 maxlim: 1300479 bits: 21/21 c ---[1323]---> Adder-cost: 77 maxlim: 41983 bits: 17/16 c ---[1322]---> Adder-cost: 182 maxlim: 23551 bits: 16/15 c ---[1319]---> Adder-cost: 232 maxlim: 95231 bits: 18/17 c ---[1317]---> Adder-cost: 157 maxlim: 46079 bits: 17/16 c ---[1316]---> Adder-cost: 75 maxlim: 50175 bits: 17/16 c ---[1314]---> Adder-cost: 420 maxlim: 184319 bits: 19/18 c ---[1313]---> Adder-cost: 196 maxlim: 20479 bits: 16/15 c ---[1310]---> Adder-cost: 105 maxlim: 27647 bits: 16/15 c ---[1309]---> Adder-cost: 1130 maxlim: 509951 bits: 20/19 c ---[1308]---> Adder-cost: 12571 maxlim: 4651007 bits: 24/23 c ---[1306]---> Adder-cost: 21792 maxlim: 11857919 bits: 24/24 c ---[1304]---> Adder-cost: 158 maxlim: 101376 bits: 18/17 c ---[1299]---> Adder-cost: 70965 maxlim: 378189823 bits: 30/29 c ---[1297]---> Adder-cost: 27402 maxlim: 70737919 bits: 28/27 c ---[1289]---> Adder-cost: 148 maxlim: 75776 bits: 18/17 c ---[1270]---> Adder-cost: 34136 maxlim: 161996799 bits: 29/28 c ---[1251]---> Adder-cost: 284 maxlim: 150528 bits: 19/18 c ---[1249]---> Adder-cost: 278 maxlim: 159744 bits: 19/18 c ---[1247]---> Adder-cost: 314 maxlim: 189440 bits: 19/18 c ---[1245]---> Adder-cost: 104 maxlim: 189440 bits: 19/18 c ---[1243]---> Adder-cost: 260 maxlim: 177152 bits: 19/18 c ---[1241]---> Adder-cost: 276 maxlim: 169984 bits: 19/18 c ---[1239]---> Adder-cost: 176 maxlim: 109568 bits: 18/17 c ---[1237]---> Adder-cost: 78 maxlim: 109568 bits: 18/17 c ---[1235]---> Adder-cost: 290 maxlim: 155648 bits: 19/18 c ---[1233]---> Adder-cost: 300 maxlim: 168960 bits: 19/18 c ---[1231]---> Adder-cost: 282 maxlim: 159744 bits: 19/18 c ---[1229]---> Adder-cost: 94 maxlim: 159744 bits: 19/18 c ---[1227]---> Adder-cost: 284 maxlim: 159744 bits: 19/18 c ---[1225]---> Adder-cost: 246 maxlim: 161792 bits: 19/18 c ---[1223]---> Adder-cost: 242 maxlim: 151552 bits: 19/18 c ---[1221]---> Adder-cost: 132 maxlim: 74752 bits: 18/17 c ---[1219]---> Adder-cost: 254 maxlim: 169984 bits: 19/18 c ---[1217]---> Adder-cost: 266 maxlim: 164864 bits: 19/18 c ---[1215]---> Adder-cost: 248 maxlim: 163840 bits: 19/18 c ---[1213]---> Adder-cost: 246 maxlim: 168960 bits: 19/18 c ---[1211]---> Adder-cost: 226 maxlim: 163840 bits: 19/18 c ---[1209]---> Adder-cost: 210 maxlim: 160768 bits: 19/18 c ---[1207]---> Adder-cost: 186 maxlim: 171008 bits: 19/18 c ---[1205]---> Adder-cost: 100 maxlim: 171008 bits: 19/18 c ---[1203]---> Adder-cost: 100 maxlim: 171008 bits: 19/18 c ---[1201]---> Adder-cost: 120 maxlim: 169984 bits: 19/18 c ---[1199]---> Adder-cost: 170 maxlim: 162816 bits: 19/18 c ---[1197]---> Adder-cost: 92 maxlim: 162816 bits: 19/18 c ---[1195]---> Adder-cost: 132 maxlim: 158720 bits: 19/18 c ---[1193]---> Adder-cost: 92 maxlim: 158720 bits: 19/18 c ---[1191]---> Adder-cost: 236 maxlim: 174080 bits: 19/18 c ---[1189]---> Adder-cost: 174 maxlim: 103424 bits: 18/17 c ---[1187]---> Adder-cost: 184 maxlim: 105472 bits: 18/17 c ---[1185]---> Sorter-cost: 1273 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1183]---> Sorter-cost: 789 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1181]---> Sorter-cost: 1197 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1179]---> Sorter-cost: 820 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1177]---> Sorter-cost: 959 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1175]---> Sorter-cost: 667 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1171]---> Adder-cost: 142 maxlim: 68608 bits: 18/17 c ---[1169]---> Adder-cost: 138 maxlim: 70656 bits: 18/17 c ---[1167]---> Adder-cost: 60 maxlim: 70656 bits: 18/17 c ---[1165]---> Adder-cost: 300 maxlim: 165888 bits: 19/18 c ---[1163]---> Adder-cost: 102 maxlim: 165888 bits: 19/18 c ---[1161]---> Adder-cost: 264 maxlim: 151552 bits: 19/18 c ---[1159]---> Adder-cost: 96 maxlim: 151552 bits: 19/18 c ---[1157]---> Adder-cost: 120 maxlim: 65536 bits: 18/17 c ---[1155]---> Adder-cost: 107 maxlim: 58368 bits: 17/16 c ---[1153]---> Adder-cost: 148 maxlim: 81920 bits: 18/17 c ---[1151]---> Adder-cost: 108 maxlim: 60416 bits: 17/16 c ---[1149]---> Adder-cost: 194 maxlim: 108544 bits: 18/17 c ---[1147]---> Adder-cost: 78 maxlim: 108544 bits: 18/17 c ---[1145]---> Adder-cost: 178 maxlim: 111616 bits: 18/17 c ---[1143]---> Adder-cost: 124 maxlim: 99328 bits: 18/17 c ---[1141]---> Adder-cost: 70 maxlim: 99328 bits: 18/17 c ---[1139]---> Adder-cost: 124 maxlim: 101376 bits: 18/17 c ---[1137]---> Adder-cost: 162 maxlim: 112640 bits: 18/17 c ---[1135]---> Adder-cost: 144 maxlim: 78848 bits: 18/17 c ---[1133]---> Adder-cost: 142 maxlim: 79872 bits: 18/17 c ---[1131]---> Adder-cost: 126 maxlim: 74752 bits: 18/17 c ---[1129]---> Adder-cost: 124 maxlim: 73728 bits: 18/17 c ---[1127]---> Adder-cost: 112 maxlim: 65536 bits: 18/17 c ---[1125]---> Adder-cost: 116 maxlim: 66560 bits: 18/17 c ---[1123]---> Adder-cost: 124 maxlim: 66560 bits: 18/17 c ---[1121]---> Adder-cost: 118 maxlim: 59392 bits: 17/16 c ---[1119]---> Sorter-cost: 789 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1117]---> Sorter-cost: 553 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1115]---> Adder-cost: 142 maxlim: 70656 bits: 18/17 c ---[1113]---> Sorter-cost: 433 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1111]---> Sorter-cost: 534 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1109]---> Sorter-cost: 999 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1107]---> Sorter-cost: 678 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1105]---> Sorter-cost: 592 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1103]---> Sorter-cost: 455 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1101]---> Sorter-cost: 442 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1099]---> Sorter-cost: 735 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1097]---> Sorter-cost: 455 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1095]---> Adder-cost: 154 maxlim: 74752 bits: 18/17 c ---[1093]---> Adder-cost: 138 maxlim: 75776 bits: 18/17 c ---[1091]---> Adder-cost: 106 maxlim: 76800 bits: 18/17 c ---[1089]---> Adder-cost: 108 maxlim: 54272 bits: 17/16 c ---[1087]---> Adder-cost: 86 maxlim: 63488 bits: 17/16 c ---[1085]---> Adder-cost: 52 maxlim: 63488 bits: 17/16 c ---[1083]---> Adder-cost: 120 maxlim: 64512 bits: 17/16 c ---[1081]---> Adder-cost: 120 maxlim: 65536 bits: 18/17 c ---[1079]---> Adder-cost: 62 maxlim: 65536 bits: 18/17 c ---[1077]---> Adder-cost: 102 maxlim: 66560 bits: 18/17 c ---[1075]---> Adder-cost: 128 maxlim: 75776 bits: 18/17 c ---[1073]---> Adder-cost: 86 maxlim: 62464 bits: 17/16 c ---[1070]---> Adder-cost: 164 maxlim: 90112 bits: 18/17 c ---[1068]---> Adder-cost: 156 maxlim: 91136 bits: 18/17 c ---[1066]---> Adder-cost: 132 maxlim: 90112 bits: 18/17 c ---[1064]---> Adder-cost: 272 maxlim: 135168 bits: 19/18 c ---[1062]---> Adder-cost: 230 maxlim: 131072 bits: 19/18 c ---[1060]---> Adder-cost: 182 maxlim: 101376 bits: 18/17 c ---[1058]---> Adder-cost: 184 maxlim: 98304 bits: 18/17 c ---[1056]---> Adder-cost: 224 maxlim: 117760 bits: 18/17 c ---[1054]---> Adder-cost: 278 maxlim: 145408 bits: 19/18 c ---[1052]---> Adder-cost: 90 maxlim: 77824 bits: 18/17 c ---[1050]---> Adder-cost: 220 maxlim: 124928 bits: 18/17 c ---[1048]---> Adder-cost: 228 maxlim: 123904 bits: 18/17 c ---[1046]---> Adder-cost: 186 maxlim: 116736 bits: 18/17 c ---[1044]---> Adder-cost: 78 maxlim: 116736 bits: 18/17 c ---[1042]---> Sorter-cost: 1078 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1040]---> Sorter-cost: 959 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1038]---> Sorter-cost: 599 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1036]---> Sorter-cost: 1016 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1034]---> Sorter-cost: 1107 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1032]---> Sorter-cost: 737 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1030]---> Adder-cost: 116 maxlim: 63488 bits: 17/16 c ---[1028]---> Sorter-cost: 1033 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1026]---> Sorter-cost: 1202 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1024]---> Sorter-cost: 1014 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1022]---> Sorter-cost: 1123 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1020]---> Adder-cost: 114 maxlim: 60416 bits: 17/16 c ---[1018]---> Adder-cost: 124 maxlim: 65536 bits: 18/17 c ---[1016]---> Adder-cost: 132 maxlim: 67584 bits: 18/17 c ---[1014]---> Adder-cost: 118 maxlim: 66560 bits: 18/17 c ---[1012]---> Adder-cost: 60 maxlim: 66560 bits: 18/17 c ---[1010]---> Adder-cost: 144 maxlim: 73728 bits: 18/17 c ---[1008]---> Adder-cost: 184 maxlim: 101376 bits: 18/17 c ---[1006]---> Adder-cost: 140 maxlim: 84992 bits: 18/17 c ---[1004]---> Sorter-cost: 1217 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1002]---> Adder-cost: 148 maxlim: 78848 bits: 18/17 c ---[1000]---> Adder-cost: 118 maxlim: 68608 bits: 18/17 c ---[ 998]---> Adder-cost: 174 maxlim: 91136 bits: 18/17 c ---[ 996]---> Adder-cost: 174 maxlim: 99328 bits: 18/17 c ---[ 994]---> Adder-cost: 178 maxlim: 100352 bits: 18/17 c ---[ 992]---> Sorter-cost: 1092 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 990]---> Adder-cost: 158 maxlim: 105472 bits: 18/17 c ---[ 988]---> Sorter-cost: 1269 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 986]---> Sorter-cost: 779 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 984]---> Adder-cost: 100 maxlim: 55296 bits: 17/16 c ---[ 982]---> Adder-cost: 48 maxlim: 55296 bits: 17/16 c ---[ 980]---> Adder-cost: 98 maxlim: 53248 bits: 17/16 c ---[ 978]---> Adder-cost: 48 maxlim: 53248 bits: 17/16 c ---[ 976]---> Adder-cost: 108 maxlim: 63488 bits: 17/16 c ---[ 974]---> Adder-cost: 52 maxlim: 63488 bits: 17/16 c ---[ 972]---> Sorter-cost: 572 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 970]---> Adder-cost: 106 maxlim: 61440 bits: 17/16 c ---[ 968]---> Adder-cost: 136 maxlim: 70656 bits: 18/17 c ---[ 966]---> Adder-cost: 122 maxlim: 74752 bits: 18/17 c ---[ 964]---> Adder-cost: 132 maxlim: 77824 bits: 18/17 c ---[ 962]---> Adder-cost: 198 maxlim: 110592 bits: 18/17 c ---[ 960]---> Adder-cost: 74 maxlim: 110592 bits: 18/17 c ---[ 958]---> Adder-cost: 48 maxlim: 53248 bits: 17/16 c ---[ 956]---> Adder-cost: 146 maxlim: 91136 bits: 18/17 c ---[ 954]---> Adder-cost: 164 maxlim: 97280 bits: 18/17 c ---[ 952]---> Adder-cost: 64 maxlim: 97280 bits: 18/17 c ---[ 950]---> Adder-cost: 168 maxlim: 111616 bits: 18/17 c ---[ 948]---> Adder-cost: 72 maxlim: 111616 bits: 18/17 c ---[ 946]---> Adder-cost: 270 maxlim: 143360 bits: 19/18 c ---[ 944]---> Adder-cost: 90 maxlim: 143360 bits: 19/18 c ---[ 942]---> Adder-cost: 208 maxlim: 128000 bits: 18/17 c ---[ 940]---> Adder-cost: 78 maxlim: 128000 bits: 18/17 c ---[ 938]---> Sorter-cost: 320 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 936]---> Adder-cost: 224 maxlim: 118784 bits: 18/17 c ---[ 934]---> Adder-cost: 80 maxlim: 118784 bits: 18/17 c ---[ 932]---> Adder-cost: 190 maxlim: 107520 bits: 18/17 c ---[ 930]---> Adder-cost: 78 maxlim: 107520 bits: 18/17 c ---[ 928]---> Adder-cost: 270 maxlim: 151552 bits: 19/18 c ---[ 926]---> Adder-cost: 96 maxlim: 151552 bits: 19/18 c ---[ 924]---> Adder-cost: 210 maxlim: 119808 bits: 18/17 c ---[ 922]---> Adder-cost: 80 maxlim: 119808 bits: 18/17 c ---[ 920]---> Adder-cost: 184 maxlim: 117760 bits: 18/17 c ---[ 918]---> Adder-cost: 76 maxlim: 117760 bits: 18/17 c ---[ 916]---> Sorter-cost: 401 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 914]---> Adder-cost: 208 maxlim: 118784 bits: 18/17 c ---[ 912]---> Adder-cost: 80 maxlim: 118784 bits: 18/17 c ---[ 910]---> Adder-cost: 190 maxlim: 112640 bits: 18/17 c ---[ 908]---> Adder-cost: 74 maxlim: 112640 bits: 18/17 c ---[ 906]---> Adder-cost: 172 maxlim: 114688 bits: 18/17 c ---[ 904]---> Adder-cost: 76 maxlim: 114688 bits: 18/17 c ---[ 902]---> Adder-cost: 174 maxlim: 96256 bits: 18/17 c ---[ 900]---> Adder-cost: 68 maxlim: 96256 bits: 18/17 c ---[ 898]---> Adder-cost: 154 maxlim: 84992 bits: 18/17 c ---[ 896]---> Adder-cost: 68 maxlim: 84992 bits: 18/17 c ---[ 894]---> Sorter-cost: 406 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 892]---> Adder-cost: 128 maxlim: 68608 bits: 18/17 c ---[ 890]---> Adder-cost: 138 maxlim: 72704 bits: 18/17 c ---[ 888]---> Adder-cost: 56 maxlim: 72704 bits: 18/17 c ---[ 886]---> Adder-cost: 116 maxlim: 61440 bits: 17/16 c ---[ 884]---> Adder-cost: 50 maxlim: 61440 bits: 17/16 c ---[ 882]---> Adder-cost: 142 maxlim: 80896 bits: 18/17 c ---[ 880]---> Adder-cost: 62 maxlim: 80896 bits: 18/17 c ---[ 878]---> Adder-cost: 120 maxlim: 62464 bits: 17/16 c ---[ 876]---> Adder-cost: 48 maxlim: 62464 bits: 17/16 c ---[ 874]---> Sorter-cost: 400 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 872]---> Adder-cost: 110 maxlim: 60416 bits: 17/16 c ---[ 870]---> Adder-cost: 48 maxlim: 60416 bits: 17/16 c ---[ 868]---> Adder-cost: 138 maxlim: 88064 bits: 18/17 c ---[ 866]---> Adder-cost: 68 maxlim: 88064 bits: 18/17 c ---[ 864]---> Adder-cost: 124 maxlim: 91136 bits: 18/17 c ---[ 862]---> Adder-cost: 72 maxlim: 91136 bits: 18/17 c ---[ 860]---> Adder-cost: 204 maxlim: 121856 bits: 18/17 c ---[ 858]---> Adder-cost: 80 maxlim: 121856 bits: 18/17 c ---[ 856]---> Adder-cost: 80 maxlim: 121856 bits: 18/17 c ---[ 854]---> Adder-cost: 80 maxlim: 121856 bits: 18/17 c ---[ 852]---> Adder-cost: 160 maxlim: 118784 bits: 18/17 c ---[ 848]---> Adder-cost: 140 maxlim: 71680 bits: 18/17 c ---[ 846]---> Adder-cost: 60 maxlim: 71680 bits: 18/17 c ---[ 844]---> Adder-cost: 128 maxlim: 66560 bits: 18/17 c ---[ 842]---> Adder-cost: 60 maxlim: 66560 bits: 18/17 c ---[ 840]---> Adder-cost: 110 maxlim: 66560 bits: 18/17 c ---[ 838]---> Adder-cost: 60 maxlim: 66560 bits: 18/17 c ---[ 836]---> Adder-cost: 156 maxlim: 76800 bits: 18/17 c ---[ 834]---> Sorter-cost: 653 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 832]---> Adder-cost: 94 maxlim: 74752 bits: 18/17 c ---[ 830]---> Sorter-cost: 884 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 828]---> Sorter-cost: 999 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 826]---> Sorter-cost: 854 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 824]---> Sorter-cost: 689 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 822]---> Adder-cost: 154 maxlim: 77824 bits: 18/17 c ---[ 820]---> Adder-cost: 64 maxlim: 77824 bits: 18/17 c ---[ 818]---> Adder-cost: 130 maxlim: 68608 bits: 18/17 c ---[ 816]---> Adder-cost: 58 maxlim: 68608 bits: 18/17 c ---[ 814]---> Sorter-cost: 1271 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 812]---> Sorter-cost: 763 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 810]---> Adder-cost: 112 maxlim: 56320 bits: 17/16 c ---[ 808]---> Adder-cost: 46 maxlim: 56320 bits: 17/16 c ---[ 806]---> Sorter-cost: 315 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 804]---> Sorter-cost: 249 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 802]---> Sorter-cost: 888 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 800]---> Sorter-cost: 642 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 798]---> Sorter-cost: 987 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 796]---> Adder-cost: 110 maxlim: 56320 bits: 17/16 c ---[ 794]---> Adder-cost: 168 maxlim: 89088 bits: 18/17 c ---[ 792]---> Adder-cost: 192 maxlim: 101376 bits: 18/17 c ---[ 790]---> Adder-cost: 116 maxlim: 62464 bits: 17/16 c ---[ 788]---> Adder-cost: 104 maxlim: 52224 bits: 17/16 c ---[ 786]---> Adder-cost: 138 maxlim: 67584 bits: 18/17 c ---[ 784]---> Adder-cost: 140 maxlim: 72704 bits: 18/17 c ---[ 782]---> Adder-cost: 112 maxlim: 75776 bits: 18/17 c ---[ 780]---> Adder-cost: 212 maxlim: 110592 bits: 18/17 c ---[ 778]---> Adder-cost: 74 maxlim: 110592 bits: 18/17 c ---[ 776]---> Adder-cost: 212 maxlim: 125952 bits: 18/17 c ---[ 774]---> Adder-cost: 78 maxlim: 125952 bits: 18/17 c ---[ 772]---> Sorter-cost: 615 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 770]---> Adder-cost: 132 maxlim: 70656 bits: 18/17 c ---[ 768]---> Adder-cost: 60 maxlim: 70656 bits: 18/17 c ---[ 766]---> Adder-cost: 174 maxlim: 88064 bits: 18/17 c ---[ 764]---> Adder-cost: 68 maxlim: 88064 bits: 18/17 c ---[ 762]---> Adder-cost: 186 maxlim: 100352 bits: 18/17 c ---[ 760]---> Adder-cost: 72 maxlim: 100352 bits: 18/17 c ---[ 758]---> Adder-cost: 150 maxlim: 92160 bits: 18/17 c ---[ 756]---> Adder-cost: 66 maxlim: 92160 bits: 18/17 c ---[ 754]---> Adder-cost: 110 maxlim: 96256 bits: 18/17 c ---[ 752]---> Adder-cost: 68 maxlim: 96256 bits: 18/17 c ---[ 750]---> Sorter-cost: 607 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 747]---> Adder-cost: 98 maxlim: 56320 bits: 17/16 c ---[ 745]---> Adder-cost: 102 maxlim: 62464 bits: 17/16 c ---[ 743]---> Adder-cost: 106 maxlim: 59392 bits: 17/16 c ---[ 741]---> Sorter-cost: 574 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 739]---> Sorter-cost: 880 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 736]---> Sorter-cost: 528 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 734]---> Sorter-cost: 1078 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 732]---> Sorter-cost: 1045 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 730]---> Sorter-cost: 667 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 728]---> Adder-cost: 170 maxlim: 86016 bits: 18/17 c ---[ 726]---> Adder-cost: 66 maxlim: 86016 bits: 18/17 c ---[ 724]---> Adder-cost: 166 maxlim: 88064 bits: 18/17 c ---[ 721]---> Adder-cost: 68 maxlim: 88064 bits: 18/17 c ---[ 719]---> Sorter-cost: 1248 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 717]---> Adder-cost: 100 maxlim: 52224 bits: 17/16 c ---[ 715]---> Adder-cost: 172 maxlim: 93184 bits: 18/17 c ---[ 712]---> Sorter-cost: 1283 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 710]---> Sorter-cost: 1249 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 708]---> Sorter-cost: 967 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 706]---> Adder-cost: 74 maxlim: 54272 bits: 17/16 c ---[ 704]---> Sorter-cost: 587 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 702]---> Sorter-cost: 1047 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 700]---> Sorter-cost: 739 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 698]---> Sorter-cost: 987 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 696]---> Sorter-cost: 599 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 694]---> Adder-cost: 202 maxlim: 102400 bits: 18/17 c ---[ 692]---> Adder-cost: 76 maxlim: 102400 bits: 18/17 c ---[ 690]---> Adder-cost: 184 maxlim: 102400 bits: 18/17 c ---[ 688]---> Adder-cost: 76 maxlim: 102400 bits: 18/17 c ---[ 686]---> Adder-cost: 142 maxlim: 89088 bits: 18/17 c ---[ 684]---> Sorter-cost: 422 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 682]---> Adder-cost: 122 maxlim: 83968 bits: 18/17 c ---[ 680]---> Adder-cost: 242 maxlim: 124928 bits: 18/17 c ---[ 678]---> Adder-cost: 138 maxlim: 122880 bits: 18/17 c ---[ 676]---> Sorter-cost: 927 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 674]---> Sorter-cost: 915 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 672]---> Adder-cost: 100 maxlim: 52224 bits: 17/16 c ---[ 670]---> Adder-cost: 44 maxlim: 52224 bits: 17/16 c ---[ 668]---> Sorter-cost: 1022 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 666]---> Sorter-cost: 636 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 664]---> Sorter-cost: 1281 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 662]---> Sorter-cost: 269 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 660]---> Adder-cost: 94 maxlim: 52224 bits: 17/16 c ---[ 658]---> Sorter-cost: 890 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 656]---> Sorter-cost: 528 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 654]---> Sorter-cost: 937 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 652]---> Sorter-cost: 743 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 649]---> Adder-cost: 144 maxlim: 80896 bits: 18/17 c ---[ 647]---> Sorter-cost: 1271 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 645]---> Sorter-cost: 545 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 643]---> Sorter-cost: 763 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 641]---> Sorter-cost: 1243 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 639]---> Sorter-cost: 779 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 637]---> Adder-cost: 104 maxlim: 57344 bits: 17/16 c ---[ 635]---> Adder-cost: 52 maxlim: 57344 bits: 17/16 c ---[ 633]---> Adder-cost: 172 maxlim: 83968 bits: 18/17 c ---[ 631]---> Adder-cost: 68 maxlim: 83968 bits: 18/17 c ---[ 629]---> Adder-cost: 150 maxlim: 76800 bits: 18/17 c ---[ 627]---> Adder-cost: 62 maxlim: 76800 bits: 18/17 c ---[ 625]---> Sorter-/oldhome/oroussel/solvers/minisat+_script: line 16: 18308 CPU time limit exceeded $XDIR/minisat+_bignum_static* "$@" #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.99 1.00 0.97 2/55 18303 Raw data (stat): 18303 (runsolver) R 18302 32363 32362 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 719286752 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0004 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+20.001 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+30.0007 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+40.0074 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+50.007 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+60.0067 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+70.0064 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+80.0061 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+90.0058 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+100.005 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+110.006 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+120.006 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+130.006 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+140.005 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+150.005 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+160.005 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+170.004 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+180.004 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+190.005 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+200.004 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+210.004 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+220.004 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+230.003 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+240.003 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+250.003 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+260.003 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+270.003 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+280.003 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+290.003 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+300.003 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+310.004 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+320.004 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+330.004 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+340.004 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+350.004 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+360.012 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+370.012 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+380.012 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+390.018 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+400.018 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+410.018 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+420.017 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+430.017 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+440.017 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+450.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+460.017 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+470.017 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+480.017 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+490.017 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+500.017 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+510.017 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+520.017 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+530.017 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+540.017 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+550.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+560.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+570.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+580.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+590.016 s] Raw data (loadavg): 0.99 1.00 0.97 3/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+600.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+610.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+620.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+630.015 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+640.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+650.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+660.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+670.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+680.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+690.017 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+700.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+710.017 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+720.017 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+730.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+740.017 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+750.017 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+760.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+770.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+780.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+790.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+800.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+810.017 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+820.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+830.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+840.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+850.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+860.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+870.016 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+880.015 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+890.015 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+900.015 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+910.015 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+920.015 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+930.015 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+940.014 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+950.014 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+960.015 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+970.015 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+980.015 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+990.017 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1000.02 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1010.02 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1020.02 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1030.02 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1040.02 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1050.02 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1060.02 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1070.02 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1080.02 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1090.02 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1100.02 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1110.02 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1120.02 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1130.02 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1140.02 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1150.02 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1160.02 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1170.02 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1180.01 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1190.01 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1200.01 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1210.02 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1220.01 s] Raw data (loadavg): 0.99 1.00 0.97 2/56 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1229.82 s] Raw data (loadavg): 0.99 1.00 0.97 1/54 18308 Raw data (stat): 18303 (minisat+_script) S 18302 32363 32362 0 -1 0 300 763 0 0 0 0 9 2 17 0 1 0 719286752 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 0 Child status: 152 Real time (s): 1229.82 CPU time (s): 1230 CPU user time (s): 1228.74 CPU system time (s): 1.26181 CPU usage (%): 100.015 Max. virtual memory (Kb): 2128 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####