Name | normalized-opb/mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-biella1.opb |
MD5SUM | 4e03f8e015510f52ff53e17d84030db1 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 2147483647 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 42650 |
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 | 4779625155602030788608 |
Number of bits of the sum of numbers in the objective function | 73 |
Biggest number in a constraint | 536870912000000000000 |
Number of bits of the biggest number in a constraint | 69 |
Biggest sum of numbers in a constraint | 4779727555602030788608 |
Number of bits of the biggest sum of numbers | 73 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1206.47 |
Number of variables | 42650 |
Total number of constraints | 7313 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 6111 |
Number of constraints which are nor clauses,nor cardinality constraints | 1202 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 42650 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc6 THE 2005-05-25 20:58:24 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=22334 boxname=wulflinc6 idbench=1150 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: 4e03f8e015510f52ff53e17d84030db1 /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-biella1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-biella1.opb IDLAUNCH: 22334 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.042 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 : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.042 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: 886192 kB Buffers: 29612 kB Cached: 94076 kB SwapCached: 412 kB Active: 27764 kB Inactive: 98232 kB HighTotal: 131008 kB HighFree: 46424 kB LowTotal: 903652 kB LowFree: 839768 kB SwapTotal: 2097136 kB SwapFree: 2096036 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5696 kB Slab: 16664 kB Committed_AS: 63736 kB PageTables: 320 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-25 21:18:54 (client local time) WITH STATUS 152 IN 1229.96 SECONDS stats: 22334 7 1229.96 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c PARSE ERROR! [line 7332] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 2399 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ############################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################# c -- Clauses(.)/Splits(s): s c ---[2398]---> Sorter-cost: 971 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2396]---> Sorter-cost: 999 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2394]---> Adder-cost: 276 maxlim: 135168 bits: 19/18 c ---[2392]---> Adder-cost: 280 maxlim: 155648 bits: 19/18 c ---[2390]---> Adder-cost: 200 maxlim: 120832 bits: 18/17 c ---[2388]---> Sorter-cost: 470 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2386]---> Sorter-cost: 269 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2384]---> Sorter-cost: 311 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2382]---> Sorter-cost: 446 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2380]---> Adder-cost: 254 maxlim: 129024 bits: 18/17 c ---[2378]---> Sorter-cost: 640 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2376]---> Adder-cost: 76 maxlim: 129024 bits: 18/17 c ---[2374]---> Adder-cost: 220 maxlim: 120832 bits: 18/17 c ---[2372]---> Adder-cost: 80 maxlim: 120832 bits: 18/17 c ---[2370]---> Adder-cost: 186 maxlim: 106496 bits: 18/17 c ---[2368]---> Adder-cost: 116 maxlim: 107520 bits: 18/17 c ---[2366]---> Adder-cost: 184 maxlim: 100352 bits: 18/17 c ---[2364]---> Adder-cost: 72 maxlim: 100352 bits: 18/17 c ---[2362]---> Adder-cost: 72 maxlim: 100352 bits: 18/17 c ---[2360]---> Adder-cost: 72 maxlim: 100352 bits: 18/17 c ---[2358]---> Adder-cost: 190 maxlim: 106496 bits: 18/17 c ---[2356]---> Sorter-cost: 476 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2354]---> Adder-cost: 78 maxlim: 106496 bits: 18/17 c ---[2352]---> Adder-cost: 158 maxlim: 79872 bits: 18/17 c ---[2350]---> Adder-cost: 62 maxlim: 79872 bits: 18/17 c ---[2348]---> Adder-cost: 162 maxlim: 89088 bits: 18/17 c ---[2346]---> Adder-cost: 68 maxlim: 89088 bits: 18/17 c ---[2344]---> Adder-cost: 114 maxlim: 64512 bits: 17/16 c ---[2342]---> Adder-cost: 50 maxlim: 64512 bits: 17/16 c ---[2340]---> Sorter-cost: 1271 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2338]---> Sorter-cost: 763 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2336]---> Sorter-cost: 1303 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2334]---> Sorter-cost: 1159 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2332]---> Sorter-cost: 1067 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2330]---> Sorter-cost: 1099 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2328]---> Sorter-cost: 759 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2326]---> Sorter-cost: 407 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2324]---> Sorter-cost: 713 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2322]---> Sorter-cost: 563 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2320]---> Sorter-cost: 578 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2318]---> Sorter-cost: 1250 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2316]---> Sorter-cost: 365 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2314]---> Sorter-cost: 307 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2312]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2310]---> Sorter-cost: 428 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2308]---> Sorter-cost: 434 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2306]---> Sorter-cost: 445 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2304]---> Sorter-cost: 309 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2302]---> Sorter-cost: 537 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2300]---> Sorter-cost: 887 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2298]---> Sorter-cost: 369 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2296]---> Sorter-cost: 249 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2294]---> Sorter-cost: 249 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2292]---> Sorter-cost: 313 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2290]---> Sorter-cost: 771 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2288]---> Sorter-cost: 407 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2286]---> Sorter-cost: 601 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2284]---> Sorter-cost: 563 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2282]---> Sorter-cost: 668 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2280]---> Sorter-cost: 520 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2278]---> Sorter-cost: 613 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2276]---> Sorter-cost: 455 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2274]---> Sorter-cost: 880 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2272]---> Sorter-cost: 624 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2270]---> Sorter-cost: 668 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2268]---> Sorter-cost: 520 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2266]---> Sorter-cost: 632 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2264]---> Sorter-cost: 520 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2262]---> Sorter-cost: 520 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2260]---> Sorter-cost: 520 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2258]---> Sorter-cost: 1075 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2256]---> Sorter-cost: 713 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2254]---> Sorter-cost: 271 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2252]---> Sorter-cost: 361 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2250]---> Sorter-cost: 619 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2248]---> Sorter-cost: 455 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2246]---> Sorter-cost: 1020 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2244]---> Sorter-cost: 1061 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2242]---> Sorter-cost: 1091 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2240]---> Sorter-cost: 718 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2238]---> Sorter-cost: 544 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2236]---> Adder-cost: 140 maxlim: 66560 bits: 18/17 c ---[2234]---> Sorter-cost: 1087 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2232]---> Sorter-cost: 739 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2230]---> Sorter-cost: 716 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2228]---> Sorter-cost: 953 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2226]---> Sorter-cost: 269 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2224]---> Sorter-cost: 910 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2222]---> Sorter-cost: 733 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2220]---> Sorter-cost: 424 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2218]---> Sorter-cost: 355 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2216]---> Sorter-cost: 307 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2214]---> Sorter-cost: 1070 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2212]---> Adder-cost: 118 maxlim: 58368 bits: 17/16 c ---[2210]---> Sorter-cost: 422 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2208]---> Sorter-cost: 937 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2206]---> Sorter-cost: 686 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2204]---> Sorter-cost: 444 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2202]---> Sorter-cost: 332 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2200]---> Sorter-cost: 332 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2198]---> Adder-cost: 48 maxlim: 58368 bits: 17/16 c ---[2196]---> Sorter-cost: 332 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2194]---> Sorter-cost: 651 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2192]---> Sorter-cost: 564 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2190]---> Sorter-cost: 405 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2188]---> Sorter-cost: 400 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2186]---> Sorter-cost: 391 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2184]---> Sorter-cost: 293 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[2182]---> Sorter-cost: 429 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2180]---> Sorter-cost: 716 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2178]---> Adder-cost: 192 maxlim: 103424 bits: 18/17 c ---[2176]---> Adder-cost: 76 maxlim: 103424 bits: 18/17 c ---[2174]---> Adder-cost: 124 maxlim: 69632 bits: 18/17 c ---[2172]---> Adder-cost: 62 maxlim: 69632 bits: 18/17 c ---[2170]---> Adder-cost: 138 maxlim: 86016 bits: 18/17 c ---[2168]---> Adder-cost: 66 maxlim: 86016 bits: 18/17 c ---[2166]---> Adder-cost: 118 maxlim: 61440 bits: 17/16 c ---[2164]---> Adder-cost: 50 maxlim: 61440 bits: 17/16 c ---[2162]---> Adder-cost: 66 maxlim: 54272 bits: 17/16 c ---[2160]---> Adder-cost: 46 maxlim: 54272 bits: 17/16 c ---[2158]---> Sorter-cost: 1180 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2156]---> Sorter-cost: 762 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2154]---> Sorter-cost: 1244 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2152]---> Sorter-cost: 818 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2150]---> Sorter-cost: 710 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2148]---> Sorter-cost: 544 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2146]---> Adder-cost: 110 maxlim: 66560 bits: 18/17 c ---[2144]---> Sorter-cost: 1223 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2142]---> Adder-cost: 60 maxlim: 66560 bits: 18/17 c ---[2140]---> Adder-cost: 146 maxlim: 73728 bits: 18/17 c ---[2138]---> Adder-cost: 62 maxlim: 73728 bits: 18/17 c ---[2136]---> Adder-cost: 92 maxlim: 51200 bits: 17/16 c ---[2134]---> Adder-cost: 44 maxlim: 51200 bits: 17/16 c ---[2132]---> Adder-cost: 98 maxlim: 51200 bits: 17/16 c ---[2130]---> Sorter-cost: 1277 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2128]---> Sorter-cost: 694 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2126]---> Sorter-cost: 1210 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2124]---> Sorter-cost: 716 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2122]---> Sorter-cost: 544 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2120]---> Sorter-cost: 967 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2118]---> Sorter-cost: 564 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2116]---> Sorter-cost: 518 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2114]---> Sorter-cost: 440 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2112]---> Sorter-cost: 389 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2110]---> Sorter-cost: 283 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2108]---> Sorter-cost: 689 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2106]---> Sorter-cost: 563 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2104]---> Sorter-cost: 763 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2102]---> Sorter-cost: 407 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2100]---> Sorter-cost: 957 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2098]---> Sorter-cost: 587 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2096]---> Adder-cost: 120 maxlim: 59392 bits: 17/16 c ---[2094]---> Sorter-cost: 596 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2092]---> Sorter-cost: 476 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2090]---> Sorter-cost: 686 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2088]---> Sorter-cost: 520 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2086]---> Sorter-cost: 468 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2084]---> Sorter-cost: 436 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2082]---> Sorter-cost: 433 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2080]---> Sorter-cost: 309 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2078]---> Sorter-cost: 587 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2076]---> Sorter-cost: 567 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2074]---> Adder-cost: 70 maxlim: 56320 bits: 17/16 c ---[2072]---> Sorter-cost: 549 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2070]---> Sorter-cost: 583 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2068]---> Sorter-cost: 717 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2066]---> Sorter-cost: 989 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2064]---> Adder-cost: 184 maxlim: 91136 bits: 18/17 c ---[2062]---> Adder-cost: 168 maxlim: 88064 bits: 18/17 c ---[2060]---> Sorter-cost: 373 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2058]---> Adder-cost: 104 maxlim: 61440 bits: 17/16 c ---[2056]---> Adder-cost: 50 maxlim: 61440 bits: 17/16 c ---[2054]---> Adder-cost: 88 maxlim: 58368 bits: 17/16 c ---[2052]---> Adder-cost: 48 maxlim: 58368 bits: 17/16 c ---[2050]---> Adder-cost: 86 maxlim: 52224 bits: 17/16 c ---[2048]---> Adder-cost: 44 maxlim: 52224 bits: 17/16 c ---[2046]---> Sorter-cost: 964 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2044]---> Sorter-cost: 1183 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2042]---> Adder-cost: 110 maxlim: 53248 bits: 17/16 c ---[2040]---> Adder-cost: 48 maxlim: 53248 bits: 17/16 c ---[2038]---> Adder-cost: 80 maxlim: 56320 bits: 17/16 c ---[2036]---> Sorter-cost: 1221 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2034]---> Sorter-cost: 1151 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2032]---> Sorter-cost: 973 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2030]---> Sorter-cost: 735 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2028]---> Sorter-cost: 1070 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2026]---> Adder-cost: 154 maxlim: 74752 bits: 18/17 c ---[2024]---> Sorter-cost: 721 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2022]---> Adder-cost: 100 maxlim: 62464 bits: 17/16 c ---[2020]---> Sorter-cost: 636 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2018]---> Sorter-cost: 684 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2016]---> Sorter-cost: 977 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2014]---> Sorter-cost: 979 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2012]---> Adder-cost: 146 maxlim: 69632 bits: 18/17 c ---[2010]---> Sorter-cost: 1072 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2008]---> Sorter-cost: 694 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2006]---> Sorter-cost: 967 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2004]---> Sorter-cost: 787 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2002]---> Sorter-cost: 563 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[2000]---> Adder-cost: 120 maxlim: 60416 bits: 17/16 c ---[1998]---> Sorter-cost: 365 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1996]---> Sorter-cost: 737 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1994]---> Sorter-cost: 698 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1992]---> Sorter-cost: 544 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1990]---> Sorter-cost: 313 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1988]---> Adder-cost: 230 maxlim: 114688 bits: 18/17 c ---[1986]---> Adder-cost: 140 maxlim: 113664 bits: 18/17 c ---[1984]---> Adder-cost: 104 maxlim: 52224 bits: 17/16 c ---[1982]---> Adder-cost: 184 maxlim: 102400 bits: 18/17 c ---[1980]---> Adder-cost: 248 maxlim: 124928 bits: 18/17 c ---[1978]---> Adder-cost: 78 maxlim: 124928 bits: 18/17 c ---[1976]---> Adder-cost: 166 maxlim: 84992 bits: 18/17 c ---[1974]---> Sorter-cost: 999 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1972]---> Sorter-cost: 574 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1970]---> Sorter-cost: 440 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1968]---> Sorter-cost: 684 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1966]---> Sorter-cost: 991 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1964]---> Sorter-cost: 883 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1962]---> Sorter-cost: 441 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1960]---> Adder-cost: 112 maxlim: 56320 bits: 17/16 c ---[1958]---> Sorter-cost: 375 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1956]---> Sorter-cost: 787 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1954]---> Sorter-cost: 424 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1952]---> Sorter-cost: 572 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1950]---> Sorter-cost: 648 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1948]---> Sorter-cost: 605 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1946]---> Sorter-cost: 634 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1944]---> Sorter-cost: 1271 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1942]---> Sorter-cost: 729 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1940]---> Sorter-cost: 666 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1938]---> Sorter-cost: 510 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1936]---> Adder-cost: 184 maxlim: 91136 bits: 18/17 c ---[1934]---> Adder-cost: 268 maxlim: 135168 bits: 19/18 c ---[1932]---> Sorter-cost: 1074 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1930]---> Sorter-cost: 763 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1928]---> Adder-cost: 136 maxlim: 67584 bits: 18/17 c ---[1926]---> Adder-cost: 208 maxlim: 102400 bits: 18/17 c ---[1924]---> Sorter-cost: 1135 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1922]---> Sorter-cost: 636 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1920]---> Sorter-cost: 720 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1918]---> Sorter-cost: 1087 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1916]---> Adder-cost: 234 maxlim: 118784 bits: 18/17 c ---[1914]---> Adder-cost: 80 maxlim: 118784 bits: 18/17 c ---[1912]---> Adder-cost: 214 maxlim: 114688 bits: 18/17 c ---[1910]---> Adder-cost: 132 maxlim: 65536 bits: 18/17 c ---[1908]---> Adder-cost: 202 maxlim: 103424 bits: 18/17 c ---[1906]---> Adder-cost: 104 maxlim: 52224 bits: 17/16 c ---[1904]---> Sorter-cost: 1080 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1902]---> Sorter-cost: 763 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1900]---> Sorter-cost: 271 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1898]---> Sorter-cost: 443 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1896]---> Sorter-cost: 420 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1894]---> Sorter-cost: 269 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1892]---> Adder-cost: 202 maxlim: 120832 bits: 18/17 c ---[1890]---> Adder-cost: 230 maxlim: 124928 bits: 18/17 c ---[1888]---> Adder-cost: 182 maxlim: 93184 bits: 18/17 c ---[1886]---> Sorter-cost: 1191 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1884]---> Adder-cost: 182 maxlim: 92160 bits: 18/17 c ---[1882]---> Adder-cost: 138 maxlim: 77824 bits: 18/17 c ---[1880]---> Adder-cost: 126 maxlim: 72704 bits: 18/17 c ---[1878]---> Adder-cost: 104 maxlim: 71680 bits: 18/17 c ---[1876]---> Adder-cost: 224 maxlim: 113664 bits: 18/17 c ---[1874]---> Adder-cost: 270 maxlim: 138240 bits: 19/18 c ---[1872]---> Adder-cost: 190 maxlim: 139264 bits: 19/18 c ---[1870]---> Sorter-cost: 791 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1868]---> Sorter-cost: 1285 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1866]---> Sorter-cost: 412 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1864]---> Adder-cost: 112 maxlim: 55296 bits: 17/16 c ---[1862]---> Adder-cost: 112 maxlim: 60416 bits: 17/16 c ---[1860]---> Adder-cost: 364 maxlim: 186368 bits: 19/18 c ---[1858]---> Adder-cost: 174 maxlim: 89088 bits: 18/17 c ---[1856]---> Adder-cost: 112 maxlim: 74752 bits: 18/17 c ---[1854]---> Adder-cost: 96 maxlim: 65536 bits: 18/17 c ---[1852]---> Adder-cost: 154 maxlim: 73728 bits: 18/17 c ---[1850]---> Adder-cost: 104 maxlim: 52224 bits: 17/16 c ---[1848]---> Sorter-cost: 1157 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1846]---> Sorter-cost: 422 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1844]---> Sorter-cost: 1057 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1842]---> Adder-cost: 264 maxlim: 134144 bits: 19/18 c ---[1840]---> Sorter-cost: 1309 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1838]---> Sorter-cost: 999 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1836]---> Sorter-cost: 576 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1834]---> Adder-cost: 162 maxlim: 80896 bits: 18/17 c ---[1832]---> Adder-cost: 142 maxlim: 72704 bits: 18/17 c ---[1830]---> Adder-cost: 156 maxlim: 76800 bits: 18/17 c ---[1828]---> Adder-cost: 62 maxlim: 76800 bits: 18/17 c ---[1826]---> Sorter-cost: 1283 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1824]---> Adder-cost: 184 maxlim: 94208 bits: 18/17 c ---[1822]---> Adder-cost: 114 maxlim: 59392 bits: 17/16 c ---[1820]---> Adder-cost: 168 maxlim: 83968 bits: 18/17 c ---[1818]---> Adder-cost: 92 maxlim: 78848 bits: 18/17 c ---[1816]---> Adder-cost: 162 maxlim: 80896 bits: 18/17 c ---[1814]---> Adder-cost: 74 maxlim: 80896 bits: 18/17 c ---[1812]---> Adder-cost: 110 maxlim: 56320 bits: 17/16 c ---[1810]---> Adder-cost: 176 maxlim: 102400 bits: 18/17 c ---[1808]---> Adder-cost: 212 maxlim: 122880 bits: 18/17 c ---[1806]---> Adder-cost: 172 maxlim: 140288 bits: 19/18 c ---[1804]---> Adder-cost: 174 maxlim: 137216 bits: 19/18 c ---[1802]---> Adder-cost: 108 maxlim: 54272 bits: 17/16 c ---[1800]---> Adder-cost: 136 maxlim: 65536 bits: 18/17 c ---[1798]---> Sorter-cost: 581 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1796]---> Sorter-cost: 470 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1794]---> Sorter-cost: 643 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1792]---> Adder-cost: 140 maxlim: 67584 bits: 18/17 c ---[1790]---> Sorter-cost: 597 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1788]---> Adder-cost: 204 maxlim: 102400 bits: 18/17 c ---[1786]---> Adder-cost: 336 maxlim: 180224 bits: 19/18 c ---[1784]---> Sorter-cost: 1059 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1782]---> Sorter-cost: 277 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1780]---> Sorter-cost: 1287 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1778]---> Adder-cost: 60 maxlim: 67584 bits: 18/17 c ---[1776]---> Sorter-cost: 841 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1774]---> Sorter-cost: 714 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1772]---> Sorter-cost: 694 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1770]---> Adder-cost: 136 maxlim: 70656 bits: 18/17 c ---[1768]---> Adder-cost: 144 maxlim: 71680 bits: 18/17 c ---[1766]---> Sorter-cost: 593 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1764]---> Sorter-cost: 433 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1762]---> Sorter-cost: 929 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1760]---> Adder-cost: 144 maxlim: 69632 bits: 18/17 c ---[1758]---> Sorter-cost: 267 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1756]---> Adder-cost: 156 maxlim: 113664 bits: 18/17 c ---[1754]---> Sorter-cost: 267 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1752]---> Adder-cost: 136 maxlim: 68608 bits: 18/17 c ---[1750]---> Adder-cost: 216 maxlim: 111616 bits: 18/17 c ---[1748]---> Adder-cost: 172 maxlim: 86016 bits: 18/17 c ---[1746]---> Sorter-cost: 1221 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1744]---> Adder-cost: 118 maxlim: 59392 bits: 17/16 c ---[1742]---> Sorter-cost: 1171 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1740]---> Adder-cost: 110 maxlim: 56320 bits: 17/16 c ---[1738]---> Adder-cost: 222 maxlim: 125952 bits: 18/17 c ---[1736]---> Adder-cost: 146 maxlim: 75776 bits: 18/17 c ---[1734]---> Adder-cost: 132 maxlim: 67584 bits: 18/17 c ---[1732]---> Sorter-cost: 937 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1730]---> Adder-cost: 178 maxlim: 88064 bits: 18/17 c ---[1728]---> Sorter-cost: 1185 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1726]---> Adder-cost: 68 maxlim: 88064 bits: 18/17 c ---[1724]---> Adder-cost: 216 maxlim: 109568 bits: 18/17 c ---[1722]---> Adder-cost: 184 maxlim: 95232 bits: 18/17 c ---[1720]---> Adder-cost: 152 maxlim: 96256 bits: 18/17 c ---[1718]---> Adder-cost: 120 maxlim: 59392 bits: 17/16 c ---[1716]---> Sorter-cost: 399 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1714]---> Sorter-cost: 251 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1712]---> Sorter-cost: 821 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1710]---> Sorter-cost: 468 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1708]---> Sorter-cost: 361 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1706]---> Adder-cost: 332 maxlim: 163840 bits: 19/18 c ---[1704]---> Adder-cost: 314 maxlim: 162816 bits: 19/18 c ---[1702]---> Adder-cost: 234 maxlim: 134144 bits: 19/18 c ---[1700]---> Adder-cost: 168 maxlim: 88064 bits: 18/17 c ---[1698]---> Adder-cost: 112 maxlim: 57344 bits: 17/16 c ---[1696]---> Adder-cost: 160 maxlim: 79872 bits: 18/17 c ---[1694]---> Sorter-cost: 1079 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1692]---> Adder-cost: 212 maxlim: 120832 bits: 18/17 c ---[1690]---> Adder-cost: 172 maxlim: 119808 bits: 18/17 c ---[1688]---> Sorter-cost: 1028 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1686]---> Adder-cost: 142 maxlim: 68608 bits: 18/17 c ---[1684]---> Sorter-cost: 739 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1682]---> Sorter-cost: 964 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1680]---> Adder-cost: 162 maxlim: 80896 bits: 18/17 c ---[1678]---> Adder-cost: 120 maxlim: 59392 bits: 17/16 c ---[1676]---> Adder-cost: 124 maxlim: 62464 bits: 17/16 c ---[1674]---> Sorter-cost: 424 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1672]---> Sorter-cost: 619 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1670]---> Sorter-cost: 448 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1668]---> Sorter-cost: 574 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1666]---> Sorter-cost: 1004 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1664]---> Sorter-cost: 466 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1662]---> Sorter-cost: 589 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1660]---> Sorter-cost: 466 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1658]---> Sorter-cost: 593 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1656]---> Adder-cost: 120 maxlim: 60416 bits: 17/16 c ---[1654]---> Sorter-cost: 929 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1652]---> Sorter-cost: 893 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1650]---> Sorter-cost: 317 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1648]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1646]---> Adder-cost: 394 maxlim: 200704 bits: 19/18 c ---[1644]---> Adder-cost: 356 maxlim: 184320 bits: 19/18 c ---[1642]---> Adder-cost: 208 maxlim: 186368 bits: 19/18 c ---[1640]---> Sorter-cost: 910 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1638]---> Sorter-cost: 1133 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1636]---> Sorter-cost: 881 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1634]---> Adder-cost: 228 maxlim: 121856 bits: 18/17 c ---[1632]---> Sorter-cost: 315 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1630]---> Adder-cost: 142 maxlim: 73728 bits: 18/17 c ---[1628]---> Adder-cost: 124 maxlim: 62464 bits: 17/16 c ---[1626]---> Adder-cost: 104 maxlim: 61440 bits: 17/16 c ---[1624]---> Sorter-cost: 578 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1622]---> Sorter-cost: 734 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1620]---> Sorter-cost: 1219 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1618]---> Sorter-cost: 1177 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1616]---> Sorter-cost: 1045 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1614]---> Sorter-cost: 956 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1612]---> Sorter-cost: 638 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1610]---> Sorter-cost: 317 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1608]---> Adder-cost: 110 maxlim: 54272 bits: 17/16 c ---[1606]---> Adder-cost: 150 maxlim: 77824 bits: 18/17 c ---[1604]---> Adder-cost: 112 maxlim: 57344 bits: 17/16 c ---[1602]---> Sorter-cost: 1309 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1600]---> Sorter-cost: 448 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1598]---> Sorter-cost: 319 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1596]---> Sorter-cost: 446 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1594]---> Sorter-cost: 314 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1592]---> Sorter-cost: 399 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1590]---> Sorter-cost: 271 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1588]---> Adder-cost: 160 maxlim: 80896 bits: 18/17 c ---[1586]---> Adder-cost: 154 maxlim: 80896 bits: 18/17 c ---[1584]---> Sorter-cost: 789 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1582]---> Sorter-cost: 1084 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1580]---> Sorter-cost: 271 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1578]---> Sorter-cost: 1159 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1576]---> Adder-cost: 108 maxlim: 60416 bits: 17/16 c ---[1574]---> Adder-cost: 166 maxlim: 81920 bits: 18/17 c ---[1572]---> Sorter-cost: 999 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1570]---> Sorter-cost: 271 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1568]---> Sorter-cost: 183 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1566]---> Adder-cost: 336 maxlim: 167936 bits: 19/18 c ---[1564]---> Adder-cost: 324 maxlim: 168960 bits: 19/18 c ---[1562]---> Adder-cost: 246 maxlim: 122880 bits: 18/17 c ---[1560]---> Adder-cost: 200 maxlim: 106496 bits: 18/17 c ---[1558]---> Sorter-cost: 877 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1556]---> Adder-cost: 296 maxlim: 151552 bits: 19/18 c ---[1554]---> Adder-cost: 244 maxlim: 192512 bits: 19/18 c ---[1552]---> Adder-cost: 240 maxlim: 131072 bits: 19/18 c ---[1550]---> Adder-cost: 188 maxlim: 95232 bits: 18/17 c ---[1548]---> Adder-cost: 124 maxlim: 78848 bits: 18/17 c ---[1546]---> Sorter-cost: 913 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1544]---> Sorter-cost: 1246 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1542]---> Sorter-cost: 892 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1540]---> Sorter-cost: 761 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1538]---> Sorter-cost: 673 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1536]---> BDD-cost: 59 c ---[1534]---> Sorter-cost: 249 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1532]---> Sorter-cost: 679 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1530]---> Sorter-cost: 1250 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1528]---> Sorter-cost: 737 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1526]---> Adder-cost: 108 maxlim: 54272 bits: 17/16 c ---[1524]---> Sorter-cost: 1311 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1522]---> Sorter-cost: 803 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1520]---> Adder-cost: 106 maxlim: 51200 bits: 17/16 c ---[1518]---> Adder-cost: 44 maxlim: 51200 bits: 17/16 c ---[1516]---> Adder-cost: 124 maxlim: 65536 bits: 18/17 c ---[1514]---> Sorter-cost: 271 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1512]---> Adder-cost: 98 maxlim: 68608 bits: 18/17 c ---[1510]---> Adder-cost: 204 maxlim: 102400 bits: 18/17 c ---[1508]---> Adder-cost: 240 maxlim: 122880 bits: 18/17 c ---[1506]---> Adder-cost: 150 maxlim: 78848 bits: 18/17 c ---[1504]---> Adder-cost: 140 maxlim: 74752 bits: 18/17 c ---[1502]---> Adder-cost: 128 maxlim: 72704 bits: 18/17 c ---[1500]---> Sorter-cost: 999 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1498]---> Sorter-cost: 607 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1496]---> Sorter-cost: 1167 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1494]---> Sorter-cost: 965 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1492]---> Sorter-cost: 1159 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1490]---> Sorter-cost: 657 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1488]---> Adder-cost: 196 maxlim: 108544 bits: 18/17 c ---[1486]---> Adder-cost: 200 maxlim: 107520 bits: 18/17 c ---[1484]---> Adder-cost: 202 maxlim: 130048 bits: 18/17 c ---[1482]---> Sorter-cost: 929 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1480]---> Adder-cost: 74 maxlim: 130048 bits: 18/17 c ---[1478]---> Adder-cost: 136 maxlim: 70656 bits: 18/17 c ---[1476]---> Adder-cost: 78 maxlim: 60416 bits: 17/16 c ---[1474]---> Adder-cost: 146 maxlim: 80896 bits: 18/17 c ---[1472]---> Sorter-cost: 1183 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1470]---> Sorter-cost: 1046 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1468]---> Adder-cost: 118 maxlim: 59392 bits: 17/16 c ---[1466]---> Sorter-cost: 271 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1464]---> Adder-cost: 118 maxlim: 62464 bits: 17/16 c ---[1462]---> Adder-cost: 194 maxlim: 100352 bits: 18/17 c ---[1460]---> Adder-cost: 200 maxlim: 112640 bits: 18/17 c ---[1458]---> Adder-cost: 178 maxlim: 117760 bits: 18/17 c ---[1456]---> Sorter-cost: 269 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1454]---> Sorter-cost: 438 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1452]---> Sorter-cost: 977 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1450]---> Sorter-cost: 1073 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1448]---> Sorter-cost: 448 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1446]---> Sorter-cost: 1061 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1444]---> Sorter-cost: 667 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1442]---> Sorter-cost: 1163 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1440]---> Sorter-cost: 557 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1438]---> Sorter-cost: 587 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1436]---> Sorter-cost: 785 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1434]---> Sorter-cost: 1211 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1432]---> Sorter-cost: 1221 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1430]---> Sorter-cost: 791 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1428]---> Adder-cost: 106 maxlim: 51200 bits: 17/16 c ---[1426]---> Sorter-cost: 450 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1424]---> Sorter-cost: 1192 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1422]---> Sorter-cost: 259 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1420]---> Adder-cost: 276 maxlim: 160768 bits: 19/18 c ---[1418]---> Adder-cost: 224 maxlim: 125952 bits: 18/17 c ---[1416]---> Sorter-cost: 965 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1414]---> Sorter-cost: 423 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1412]---> Sorter-cost: 931 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1410]---> Sorter-cost: 285 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1408]---> Sorter-cost: 519 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1406]---> Sorter-cost: 433 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1404]---> Adder-cost: 110 maxlim: 58368 bits: 17/16 c ---[1402]---> Adder-cost: 106 maxlim: 53248 bits: 17/16 c ---[1400]---> Sorter-cost: 430 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1398]---> Sorter-cost: 735 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1396]---> Sorter-cost: 1251 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1394]---> Adder-cost: 140 maxlim: 65536 bits: 18/17 c ---[1392]---> Adder-cost: 76 maxlim: 71680 bits: 18/17 c ---[1390]---> Adder-cost: 142 maxlim: 70656 bits: 18/17 c ---[1388]---> Sorter-cost: 716 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1386]---> Sorter-cost: 388 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1384]---> Adder-cost: 140 maxlim: 76800 bits: 18/17 c ---[1382]---> Sorter-cost: 714 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1380]---> Sorter-cost: 544 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1378]---> Sorter-cost: 1269 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1376]---> Adder-cost: 104 maxlim: 53248 bits: 17/16 c ---[1374]---> Sorter-cost: 1190 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1372]---> Sorter-cost: 640 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1370]---> Sorter-cost: 653 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1368]---> Sorter-cost: 640 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1366]---> Sorter-cost: 494 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1364]---> Sorter-cost: 762 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1362]---> Sorter-cost: 674 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1360]---> Adder-cost: 146 maxlim: 70656 bits: 18/17 c ---[1358]---> Adder-cost: 112 maxlim: 60416 bits: 17/16 c ---[1356]---> Sorter-cost: 445 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1354]---> Sorter-cost: 322 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1352]---> Sorter-cost: 640 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1350]---> Sorter-cost: 655 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1348]---> Sorter-cost: 495 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1346]---> Sorter-cost: 1006 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1344]---> Sorter-cost: 1055 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1342]---> Sorter-cost: 607 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1340]---> Sorter-cost: 889 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1338]---> Sorter-cost: 415 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1336]---> Sorter-cost: 686 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1334]---> Sorter-cost: 520 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1332]---> Sorter-cost: 955 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1330]---> Sorter-cost: 703 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1329]---> Adder-cost: 1058 maxlim: 575487 bits: 21/20 c ---[1328]---> Adder-cost: 2502 maxlim: 1370111 bits: 22/21 c ---[1327]---> Adder-cost: 2332 maxlim: 1282047 bits: 22/21 c ---[1324]---> Sorter-cost: 987 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1322]---> Sorter-cost: 856 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1320]---> Sorter-cost: 1111 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1318]---> Sorter-cost: 1263 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1316]---> Sorter-cost: 440 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1314]---> Sorter-cost: 576 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1312]---> Sorter-cost: 443 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1310]---> Sorter-cost: 593 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1308]---> Sorter-cost: 372 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1306]---> Sorter-cost: 296 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1304]---> Sorter-cost: 383 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1302]---> Sorter-cost: 296 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1300]---> Sorter-cost: 327 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1298]---> Sorter-cost: 597 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1296]---> Sorter-cost: 628 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1294]---> Sorter-cost: 443 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1292]---> Sorter-cost: 373 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1290]---> Sorter-cost: 267 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1288]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1286]---> Sorter-cost: 399 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1284]---> Sorter-cost: 313 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1282]---> Adder-cost: 170 maxlim: 86016 bits: 18/17 c ---[1280]---> Adder-cost: 162 maxlim: 96256 bits: 18/17 c ---[1278]---> Sorter-cost: 1283 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1276]---> Adder-cost: 146 maxlim: 70656 bits: 18/17 c ---[1274]---> Adder-cost: 148 maxlim: 80896 bits: 18/17 c ---[1272]---> Sorter-cost: 1255 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1270]---> Sorter-cost: 1205 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1268]---> Sorter-cost: 626 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1266]---> Sorter-cost: 476 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1264]---> Sorter-cost: 443 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1262]---> Sorter-cost: 309 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1260]---> Sorter-cost: 655 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1258]---> Sorter-cost: 569 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1256]---> Sorter-cost: 789 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1254]---> Sorter-cost: 407 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1252]---> Sorter-cost: 450 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1250]---> Sorter-cost: 587 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1248]---> Sorter-cost: 433 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1246]---> Sorter-cost: 259 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1244]---> Sorter-cost: 221 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1242]---> Sorter-cost: 619 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1240]---> Sorter-cost: 455 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1238]---> Sorter-cost: 466 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1236]---> Sorter-cost: 332 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1234]---> Sorter-cost: 585 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1232]---> Sorter-cost: 433 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1230]---> Sorter-cost: 420 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1228]---> Sorter-cost: 1135 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1226]---> Sorter-cost: 931 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1224]---> Sorter-cost: 797 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1222]---> Sorter-cost: 315 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1220]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1218]---> Sorter-cost: 566 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1216]---> Sorter-cost: 296 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1214]---> Sorter-cost: 440 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1212]---> Sorter-cost: 1261 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1210]---> Sorter-cost: 411 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1208]---> Sorter-cost: 283 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1206]---> Sorter-cost: 684 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1204]---> Sorter-cost: 889 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1202]---> Sorter-cost: 313 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1200]---> Sorter-cost: 572 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1198]---> Sorter-cost: 560 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1196]---> Sorter-cost: 620 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1194]---> Sorter-cost: 619 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1192]---> Sorter-cost: 576 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1190]---> Sorter-cost: 423 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1188]---> Sorter-cost: 450 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1186]---> Sorter-cost: 395 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1184]---> Sorter-cost: 642 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1182]---> Sorter-cost: 652 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1180]---> Sorter-cost: 313 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1178]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1176]---> Sorter-cost: 265 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1174]---> Sorter-cost: 221 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1172]---> Sorter-cost: 445 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1170]---> Sorter-cost: 574 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1168]---> Sorter-cost: 446 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1166]---> Sorter-cost: 314 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1164]---> Sorter-cost: 305 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1162]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1160]---> Sorter-cost: 317 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1158]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1156]---> Sorter-cost: 387 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1154]---> Sorter-cost: 283 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1152]---> Sorter-cost: 1064 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1150]---> Sorter-cost: 441 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1148]---> Sorter-cost: 410 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1146]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1144]---> Sorter-cost: 1183 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1142]---> Sorter-cost: 1023 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1140]---> Adder-cost: 154 maxlim: 76800 bits: 18/17 c ---[1138]---> Sorter-cost: 664 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1136]---> Adder-cost: 142 maxlim: 72704 bits: 18/17 c ---[1134]---> Sorter-cost: 267 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1132]---> Sorter-cost: 221 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1130]---> Sorter-cost: 1066 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1128]---> Sorter-cost: 1133 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1126]---> Sorter-cost: 947 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1124]---> Sorter-cost: 892 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1122]---> Sorter-cost: 835 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1120]---> Sorter-cost: 997 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1118]---> Sorter-cost: 737 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1116]---> Sorter-cost: 407 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1114]---> Sorter-cost: 407 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1112]---> Sorter-cost: 939 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1110]---> Sorter-cost: 607 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1108]---> Sorter-cost: 931 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1106]---> Sorter-cost: 570 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1104]---> Sorter-cost: 369 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1102]---> Sorter-cost: 993 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1100]---> Sorter-cost: 943 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1098]---> Adder-cost: 138 maxlim: 71680 bits: 18/17 c ---[1096]---> Adder-cost: 104 maxlim: 58368 bits: 17/16 c ---[1094]---> Sorter-cost: 1083 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1092]---> Sorter-cost: 721 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1090]---> Sorter-cost: 311 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[1088]---> Sorter-cost: 718 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1086]---> Sorter-cost: 947 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1084]---> Sorter-cost: 1159 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1082]---> Sorter-cost: 1036 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1080]---> Sorter-cost: 1007 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1078]---> Sorter-cost: 943 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1076]---> Sorter-cost: 1010 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1074]---> Sorter-cost: 565 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1072]---> Sorter-cost: 762 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1070]---> Sorter-cost: 1069 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1068]---> Sorter-cost: 1129 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1066]---> Sorter-cost: 1035 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1064]---> Sorter-cost: 667 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1062]---> Sorter-cost: 1062 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1060]---> Sorter-cost: 875 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1058]---> Sorter-cost: 700 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1056]---> Sorter-cost: 591 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1054]---> Sorter-cost: 435 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1052]---> Sorter-cost: 597 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1050]---> Sorter-cost: 1267 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1048]---> Sorter-cost: 898 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1046]---> Adder-cost: 120 maxlim: 60416 bits: 17/16 c ---[1044]---> Adder-cost: 152 maxlim: 77824 bits: 18/17 c ---[1042]---> Sorter-cost: 892 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1040]---> Sorter-cost: 309 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1038]---> Sorter-cost: 1237 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1036]---> Sorter-cost: 763 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1034]---> Sorter-cost: 1043 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1032]---> Sorter-cost: 1012 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1030]---> Sorter-cost: 980 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1028]---> Sorter-cost: 923 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1026]---> Adder-cost: 120 maxlim: 59392 bits: 17/16 c ---[1024]---> Sorter-cost: 640 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1022]---> Adder-cost: 138 maxlim: 66560 bits: 18/17 c ---[1020]---> Adder-cost: 108 maxlim: 60416 bits: 17/16 c ---[1018]---> Sorter-cost: 787 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1016]---> Sorter-cost: 1155 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1014]---> Sorter-cost: 1162 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1012]---> Sorter-cost: 1074 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1010]---> Sorter-cost: 660 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1008]---> Sorter-cost: 923 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1006]---> Sorter-cost: 777 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1004]---> Sorter-cost: 407 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[1002]---> Adder-cost: 146 maxlim: 74752 bits: 18/17 c ---[1000]---> Adder-cost: 60 maxlim: 74752 bits: 18/17 c ---[ 998]---> Sorter-cost: 1085 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 996]---> Sorter-cost: 671 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 994]---> Sorter-cost: 686 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 992]---> Sorter-cost: 630 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 990]---> Sorter-cost: 476 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 988]---> Sorter-cost: 987 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 986]---> Sorter-cost: 976 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 984]---> Sorter-cost: 1151 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 982]---> Sorter-cost: 755 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 980]---> Sorter-cost: 1174 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 978]---> Sorter-cost: 747 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 976]---> Sorter-cost: 452 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 974]---> Sorter-cost: 444 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 972]---> Sorter-cost: 412 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 970]---> Sorter-cost: 359 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 968]---> Sorter-cost: 410 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 966]---> Adder-cost: 124 maxlim: 61440 bits: 17/16 c ---[ 964]---> Adder-cost: 94 maxlim: 65536 bits: 18/17 c ---[ 962]---> Sorter-cost: 994 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 960]---> Sorter-cost: 1133 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 958]---> Sorter-cost: 1153 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 956]---> Sorter-cost: 1054 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 954]---> Sorter-cost: 949 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 952]---> Sorter-cost: 1084 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 950]---> Sorter-cost: 1062 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 948]---> Sorter-cost: 1031 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 946]---> Sorter-cost: 983 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 944]---> Sorter-cost: 1063 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 942]---> Sorter-cost: 911 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 940]---> Sorter-cost: 557 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 938]---> Sorter-cost: 690 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 936]---> Sorter-cost: 573 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 934]---> Sorter-cost: 1127 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 932]---> Sorter-cost: 987 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 930]---> Sorter-cost: 863 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 928]---> Sorter-cost: 1059 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 926]---> Sorter-cost: 1219 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 924]---> Adder-cost: 110 maxlim: 53248 bits: 17/16 c ---[ 922]---> Adder-cost: 48 maxlim: 53248 bits: 17/16 c ---[ 920]---> Sorter-cost: 1083 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 918]---> Adder-cost: 104 maxlim: 53248 bits: 17/16 c ---[ 916]---> Sorter-cost: 1309 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 914]---> Adder-cost: 182 maxlim: 90112 bits: 18/17 c ---[ 912]---> Adder-cost: 194 maxlim: 103424 bits: 18/17 c ---[ 910]---> Sorter-cost: 640 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 908]---> Sorter-cost: 476 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 906]---> Sorter-cost: 638 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 904]---> Sorter-cost: 1242 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 902]---> Adder-cost: 106 maxlim: 52224 bits: 17/16 c ---[ 900]---> Sorter-cost: 1269 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 898]---> Sorter-cost: 1041 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 896]---> Sorter-cost: 313 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 894]---> Sorter-cost: 249 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 892]---> Sorter-cost: 317 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 890]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 888]---> Sorter-cost: 632 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 886]---> Sorter-cost: 424 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 884]---> Sorter-cost: 296 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 882]---> Adder-cost: 112 maxlim: 55296 bits: 17/16 c ---[ 880]---> Sorter-cost: 1221 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 878]---> Sorter-cost: 1232 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 876]---> Sorter-cost: 818 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 874]---> Sorter-cost: 464 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 872]---> Sorter-cost: 698 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 870]---> Sorter-cost: 423 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 868]---> Adder-cost: 132 maxlim: 68608 bits: 18/17 c ---[ 866]---> Adder-cost: 96 maxlim: 56320 bits: 17/16 c ---[ 864]---> Adder-cost: 138 maxlim: 66560 bits: 18/17 c ---[ 862]---> Sorter-cost: 1287 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 860]---> Sorter-cost: 721 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 858]---> Sorter-cost: 779 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 856]---> Adder-cost: 206 maxlim: 105472 bits: 18/17 c ---[ 854]---> Adder-cost: 188 maxlim: 97280 bits: 18/17 c ---[ 852]---> Adder-cost: 152 maxlim: 86016 bits: 18/17 c ---[ 850]---> Adder-cost: 130 maxlim: 84992 bits: 18/17 c ---[ 848]---> Adder-cost: 108 maxlim: 54272 bits: 17/16 c ---[ 846]---> Adder-cost: 90 maxlim: 51200 bits: 17/16 c ---[ 844]---> Sorter-cost: 1155 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 842]---> Sorter-cost: 407 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 840]---> Sorter-cost: 361 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 838]---> Sorter-cost: 692 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 836]---> Sorter-cost: 418 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 834]---> Adder-cost: 116 maxlim: 64512 bits: 17/16 c ---[ 832]---> Sorter-cost: 925 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 830]---> Sorter-cost: 979 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 828]---> Sorter-cost: 678 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 826]---> Sorter-cost: 683 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 824]---> Sorter-cost: 678 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 822]---> Sorter-cost: 520 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 820]---> Sorter-cost: 638 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 818]---> Sorter-cost: 510 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 816]---> Sorter-cost: 1050 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 814]---> Sorter-cost: 664 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 812]---> Sorter-cost: 1018 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 810]---> Sorter-cost: 636 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 808]---> Sorter-cost: 605 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 806]---> Sorter-cost: 1045 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 804]---> Sorter-cost: 667 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 802]---> Sorter-cost: 576 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 800]---> Sorter-cost: 704 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 798]---> Sorter-cost: 397 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 796]---> Sorter-cost: 409 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 794]---> Sorter-cost: 361 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 792]---> Sorter-cost: 612 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 790]---> Sorter-cost: 297 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 788]---> Sorter-cost: 577 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 786]---> Sorter-cost: 676 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 784]---> Sorter-cost: 1125 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 782]---> Sorter-cost: 1159 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 780]---> Adder-cost: 104 maxlim: 52224 bits: 17/16 c ---[ 778]---> Sorter-cost: 426 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 776]---> Sorter-cost: 631 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 774]---> Sorter-cost: 929 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 772]---> Sorter-cost: 637 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 770]---> Sorter-cost: 952 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 768]---> Sorter-cost: 436 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 766]---> Sorter-cost: 406 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 764]---> Sorter-cost: 355 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 762]---> Sorter-cost: 314 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 760]---> Sorter-cost: 443 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 758]---> Sorter-cost: 436 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 756]---> Sorter-cost: 253 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 754]---> Sorter-cost: 931 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 752]---> Sorter-cost: 896 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 750]---> Sorter-cost: 635 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 748]---> Sorter-cost: 580 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 746]---> Sorter-cost: 579 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 744]---> Sorter-cost: 291 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 742]---> Sorter-cost: 624 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 740]---> Sorter-cost: 969 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 738]---> Sorter-cost: 1035 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 736]---> Sorter-cost: 1139 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 734]---> Sorter-cost: 781 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 732]---> Sorter-cost: 965 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 730]---> Sorter-cost: 570 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 728]---> Sorter-cost: 589 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 726]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 724]---> Sorter-cost: 636 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 722]---> Sorter-cost: 595 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 720]---> Sorter-cost: 452 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 718]---> Sorter-cost: 595 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 716]---> Sorter-cost: 293 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 714]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 712]---> Sorter-cost: 361 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 710]---> Sorter-cost: 403 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 708]---> Sorter-cost: 1139 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 706]---> Sorter-cost: 951 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 704]---> Sorter-cost: 989 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 702]---> Sorter-cost: 985 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 700]---> Sorter-cost: 982 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 698]---> Sorter-cost: 1030 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 696]---> Sorter-cost: 929 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 694]---> Sorter-cost: 830 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 692]---> Sorter-cost: 652 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 690]---> Sorter-cost: 921 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 688]---> Sorter-cost: 629 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 686]---> Sorter-cost: 532 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 684]---> Sorter-cost: 624 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 682]---> Sorter-cost: 642 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 680]---> Sorter-cost: 510 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 678]---> Sorter-cost: 510 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 676]---> Sorter-cost: 1042 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 674]---> Sorter-cost: 622 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 672]---> Adder-cost: 104 maxlim: 57344 bits: 17/16 c ---[ 670]---> Sorter-cost: 373 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 668]---> Adder-cost: 74 maxlim: 56320 bits: 17/16 c ---[ 666]---> Sorter-cost: 1255 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 664]---> Adder-cost: 106 maxlim: 53248 bits: 17/16 c ---[ 662]---> Sorter-cost: 1026 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 660]---> Sorter-cost: 636 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 658]---> Adder-cost: 118 maxlim: 57344 bits: 17/16 c ---[ 656]---> Sorter-cost: 1066 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 654]---> Sorter-cost: 249 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 652]---> Adder-cost: 126 maxlim: 67584 bits: 18/17 c ---[ 650]---> Adder-cost: 178 maxlim: 91136 bits: 18/17 c ---[ 648]---> Adder-cost: 96 maxlim: 56320 bits: 17/16 c ---[ 646]---> Adder-cost: 184 maxlim: 95232 bits: 18/17 c ---[ 644]---> Adder-cost: 92 maxlim: 95232 bits: 18/17 c ---[ 642]---> Sorter-cost: 576 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 640]---> Sorter-cost: 440 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 638]---> Sorter-cost: 446 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 636]---> Sorter-cost: 314 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 634]---> Sorter-cost: 249 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 632]---> Sorter-cost: 716 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 630]---> Sorter-cost: 399 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 628]---> Sorter-cost: 1121 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 626]---> Adder-cost: 106 maxlim: 55296 bits: 17/16 c ---[ 624]---> Sorter-cost: 898 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 622]---> Sorter-cost: 407 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 620]---> Adder-cost: 224 maxlim: 120832 bits: 18/17 c ---[ 618]---> Adder-cost: 232 maxlim: 136192 bits: 19/18 c ---[ 616]---> Adder-cost: 214 maxlim: 134144 bits: 19/18 c ---[ 614]---> Sorter-cost: 1287 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 612]---> Sorter-cost: 1047 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 610]---> Adder-cost: 110 maxlim: 55296 bits: 17/16 c ---[ 608]---> Adder-cost: 72 maxlim: 55296 bits: 17/16 c ---[ 606]---> Sorter-cost: 570 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 604]---> Sorter-cost: 408 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 602]---> Sorter-cost: 296 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 600]---> Adder-cost: 118 maxlim: 57344 bits: 17/16 c ---[ 598]---> Adder-cost: 136 maxlim: 65536 bits: 18/17 c ---[ 596]---> Adder-cost: 142 maxlim: 80896 bits: 18/17 c ---[ 594]---> Adder-cost: 156 maxlim: 83968 bits: 18/17 c ---[ 592]---> Sorter-cost: 1185 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 590]---> Sorter-cost: 395 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 588]---> Sorter-cost: 1075 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 586]---> Sorter-cost: 999 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 584]---> Sorter-cost: 607 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 582]---> Sorter-cost: 1251 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 580]---> Adder-cost: 100 maxlim: 55296 bits: 17/16 c ---[ 578]---> Sorter-cost: 311 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 576]---> Adder-cost: 146 maxlim: 77824 bits: 18/17 c ---[ 574]---> Adder-cost: 64 maxlim: 77824 bits: 18/17 c ---[ 572]---> Adder-cost: 214 maxlim: 119808 bits: 18/17 c ---[ 570]---> Adder-cost: 186 maxlim: 120832 bits: 18/17 c ---[ 568]---> Adder-cost: 184 maxlim: 116736 bits: 18/17 c ---[ 566]---> Adder-cost: 78 maxlim: 116736 bits: 18/17 c ---[ 564]---> Sorter-cost: 1149 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 562]---> Sorter-cost: 365 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 560]---> Sorter-cost: 1161 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 558]---> Sorter-cost: 865 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 556]---> Adder-cost: 106 maxlim: 51200 bits: 17/16 c ---[ 554]---> Adder-cost: 44 maxlim: 51200 bits: 17/16 c ---[ 552]---> Sorter-cost: 1197 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 550]---> Sorter-cost: 587 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 548]---> Sorter-cost: 959 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 546]---> Sorter-cost: 823 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 544]---> Sorter-cost: 681 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 542]---> Adder-cost: 104 maxlim: 51200 bits: 17/16 c ---[ 540]---> Adder-cost: 44 maxlim: 51200 bits: 17/16 c ---[ 538]---> Adder-cost: 104 maxlim: 55296 bits: 17/16 c ---[ 536]---> Adder-cost: 70 maxlim: 52224 bits: 17/16 c ---[ 534]---> Sorter-cost: 566 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 532]---> Sorter-cost: 426 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 530]---> Sorter-cost: 597 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 528]---> Sorter-cost: 618 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 526]---> Sorter-cost: 558 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 524]---> Sorter-cost: 608 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 522]---> Sorter-cost: 426 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 520]---> Sorter-cost: 518 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 518]---> Sorter-cost: 533 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 516]---> Sorter-cost: 430 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 514]---> Sorter-cost: 322 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 512]---> Sorter-cost: 314 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 510]---> Sorter-cost: 579 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 508]---> Sorter-cost: 967 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 506]---> Sorter-cost: 433 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 504]---> Sorter-cost: 421 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 502]---> Sorter-cost: 402 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 500]---> Sorter-cost: 462 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 498]---> Sorter-cost: 558 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 496]---> Sorter-cost: 678 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 494]---> Sorter-cost: 694 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 492]---> Sorter-cost: 1083 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 490]---> Sorter-cost: 1023 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 488]---> Sorter-cost: 662 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 486]---> Sorter-cost: 587 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 484]---> Adder-cost: 98 maxlim: 58368 bits: 17/16 c ---[ 482]---> Adder-cost: 76 maxlim: 61440 bits: 17/16 c ---[ 480]---> Adder-cost: 100 maxlim: 62464 bits: 17/16 c ---[ 478]---> Adder-cost: 116 maxlim: 72704 bits: 18/17 c ---[ 476]---> Sorter-cost: 1301 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 474]---> Sorter-cost: 1049 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 472]---> Sorter-cost: 985 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 470]---> Sorter-cost: 548 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 468]---> Sorter-cost: 440 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 466]---> Adder-cost: 110 maxlim: 54272 bits: 17/16 c ---[ 464]---> Sorter-cost: 1153 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 462]---> Sorter-cost: 763 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 460]---> Sorter-cost: 1166 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 458]---> Sorter-cost: 599 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 456]---> Sorter-cost: 664 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 454]---> Sorter-cost: 647 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 452]---> Sorter-cost: 1263 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 450]---> Sorter-cost: 1063 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 448]---> Sorter-cost: 872 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 446]---> Sorter-cost: 1052 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 444]---> Sorter-cost: 927 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 442]---> Sorter-cost: 1155 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 440]---> Sorter-cost: 1093 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 438]---> Sorter-cost: 755 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 436]---> Sorter-cost: 1197 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 434]---> Sorter-cost: 468 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 432]---> Sorter-cost: 574 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 430]---> Sorter-cost: 459 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 428]---> Sorter-cost: 1309 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 426]---> Sorter-cost: 1111 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 424]---> Adder-cost: 136 maxlim: 68608 bits: 18/17 c ---[ 422]---> Adder-cost: 84 maxlim: 61440 bits: 17/16 c ---[ 420]---> Sorter-cost: 441 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 418]---> Sorter-cost: 716 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 416]---> Sorter-cost: 574 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 414]---> Sorter-cost: 403 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 412]---> Sorter-cost: 1231 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 410]---> Sorter-cost: 1053 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 408]---> Sorter-cost: 1043 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 406]---> Adder-cost: 116 maxlim: 64512 bits: 17/16 c ---[ 404]---> Adder-cost: 50 maxlim: 64512 bits: 17/16 c ---[ 402]---> Sorter-cost: 1039 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 400]---> Adder-cost: 100 maxlim: 60416 bits: 17/16 c ---[ 398]---> Adder-cost: 48 maxlim: 60416 bits: 17/16 c ---[ 396]---> Sorter-cost: 619 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 394]---> Sorter-cost: 455 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 392]---> Sorter-cost: 444 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 390]---> Sorter-cost: 251 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 388]---> Sorter-cost: 221 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 386]---> Sorter-cost: 221 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 384]---> Sorter-cost: 303 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 382]---> Sorter-cost: 395 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 380]---> Sorter-cost: 623 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 378]---> Sorter-cost: 606 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 376]---> Sorter-cost: 633 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 374]---> Sorter-cost: 699 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 372]---> Sorter-cost: 753 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 370]---> Sorter-cost: 1118 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 368]---> Sorter-cost: 757 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 366]---> Sorter-cost: 684 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 364]---> Sorter-cost: 666 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 362]---> Sorter-cost: 625 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 360]---> Adder-cost: 130 maxlim: 65536 bits: 18/17 c ---[ 358]---> Sorter-cost: 269 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 356]---> Sorter-cost: 221 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 354]---> Sorter-cost: 313 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 352]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 350]---> Adder-cost: 154 maxlim: 80896 bits: 18/17 c ---[ 348]---> Sorter-cost: 617 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 346]---> Sorter-cost: 628 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 344]---> Adder-cost: 104 maxlim: 54272 bits: 17/16 c ---[ 342]---> Adder-cost: 188 maxlim: 101376 bits: 18/17 c ---[ 340]---> Adder-cost: 72 maxlim: 101376 bits: 18/17 c ---[ 338]---> Sorter-cost: 267 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 336]---> Sorter-cost: 265 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 334]---> Sorter-cost: 688 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 332]---> Adder-cost: 160 maxlim: 84992 bits: 18/17 c ---[ 330]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 328]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 326]---> Adder-cost: 130 maxlim: 78848 bits: 18/17 c ---[ 324]---> Adder-cost: 150 maxlim: 88064 bits: 18/17 c ---[ 322]---> Sorter-cost: 1180 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 320]---> Sorter-cost: 973 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 318]---> Sorter-cost: 1279 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 316]---> Sorter-cost: 429 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 314]---> Sorter-cost: 557 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 312]---> Sorter-cost: 374 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 310]---> Sorter-cost: 296 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 308]---> Sorter-cost: 296 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 306]---> Adder-cost: 132 maxlim: 76800 bits: 18/17 c ---[ 304]---> Sorter-cost: 317 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 302]---> Sorter-cost: 524 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 300]---> Sorter-cost: 619 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 298]---> Sorter-cost: 361 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 296]---> Sorter-cost: 439 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 294]---> Sorter-cost: 309 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 292]---> Adder-cost: 62 maxlim: 76800 bits: 18/17 c ---[ 290]---> Sorter-cost: 632 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 288]---> Sorter-cost: 476 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 286]---> Sorter-cost: 309 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 284]---> Sorter-cost: 179 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 282]---> Sorter-cost: 409 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 280]---> Sorter-cost: 283 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 278]---> Sorter-cost: 283 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 276]---> Sorter-cost: 283 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 274]---> Sorter-cost: 424 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 272]---> Sorter-cost: 296 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 270]---> Sorter-cost: 333 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 268]---> Sorter-cost: 249 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 266]---> Adder-cost: 148 maxlim: 73728 bits: 18/17 c ---[ 264]---> Adder-cost: 138 maxlim: 83968 bits: 18/17 c ---[ 262]---> Sorter-cost: 1228 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 260]---> Sorter-cost: 799 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 258]---> Sorter-cost: 737 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 256]---> Sorter-cost: 271 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 254]---> Sorter-cost: 221 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 252]---> Sorter-cost: 365 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 250]---> Sorter-cost: 428 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 248]---> Sorter-cost: 416 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 246]---> Sorter-cost: 435 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 244]---> Sorter-cost: 529 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 242]---> Sorter-cost: 311 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 240]---> Adder-cost: 110 maxlim: 56320 bits: 17/16 c ---[ 238]---> Sorter-cost: 395 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 236]---> Sorter-cost: 891 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 234]---> Sorter-cost: 553 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 232]---> Sorter-cost: 401 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 230]---> Sorter-cost: 325 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 228]---> Sorter-cost: 401 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 226]---> Sorter-cost: 420 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 224]---> Sorter-cost: 283 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 222]---> Sorter-cost: 632 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 220]---> Sorter-cost: 476 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 218]---> Adder-cost: 102 maxlim: 52224 bits: 17/16 c ---[ 216]---> Sorter-cost: 933 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 214]---> Sorter-cost: 985 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 212]---> Sorter-cost: 296 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 210]---> Sorter-cost: 257 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 208]---> Sorter-cost: 981 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 206]---> Adder-cost: 106 maxlim: 56320 bits: 17/16 c ---[ 204]---> Sorter-cost: 688 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 202]---> Sorter-cost: 520 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 200]---> Sorter-cost: 1240 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 198]---> Adder-cost: 182 maxlim: 103424 bits: 18/17 c ---[ 196]---> Sorter-cost: 299 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 194]---> Sorter-cost: 1125 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 192]---> Adder-cost: 200 maxlim: 142336 bits: 19/18 c ---[ 190]---> Adder-cost: 92 maxlim: 142336 bits: 19/18 c ---[ 188]---> Adder-cost: 92 maxlim: 142336 bits: 19/18 c ---[ 186]---> Adder-cost: 92 maxlim: 142336 bits: 19/18 c ---[ 184]---> Adder-cost: 156 maxlim: 144384 bits: 19/18 c ---[ 182]---> Adder-cost: 166 maxlim: 124928 bits: 18/17 c ---[ 180]---> Adder-cost: 78 maxlim: 124928 bits: 18/17 c ---[ 178]---> Sorter-cost: 544 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 176]---> Sorter-cost: 433 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 174]---> Adder-cost: 194 maxlim: 145408 bits: 19/18 c ---[ 172]---> Adder-cost: 88 maxlim: 145408 bits: 19/18 c ---[ 170]---> Adder-cost: 154 maxlim: 101376 bits: 18/17 c ---[ 168]---> Adder-cost: 72 maxlim: 101376 bits: 18/17 c ---[ 166]---> Adder-cost: 152 maxlim: 104448 bits: 18/17 c ---[ 164]---> Adder-cost: 74 maxlim: 104448 bits: 18/17 c ---[ 162]---> Adder-cost: 130 maxlim: 103424 bits: 18/17 c ---[ 160]---> Adder-cost: 76 maxlim: 103424 bits: 18/17 c ---[ 158]---> Sorter-cost: 444 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 156]---> Sorter-cost: 1120 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 154]---> Sorter-cost: 1010 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 152]---> Sorter-cost: 762 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 150]---> Sorter-cost: 756 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 148]---> Sorter-cost: 528 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 146]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 144]---> Sorter-cost: 1014 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 142]---> Sorter-cost: 959 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 140]---> Sorter-cost: 907 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 138]---> Sorter-cost: 992 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 136]---> Sorter-cost: 667 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 134]---> Sorter-cost: 965 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 132]---> Sorter-cost: 947 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 130]---> Sorter-cost: 607 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 128]---> Sorter-cost: 1183 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 126]---> Sorter-cost: 401 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 124]---> Sorter-cost: 443 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 122]---> Sorter-cost: 444 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 120]---> Sorter-cost: 981 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 118]---> Sorter-cost: 1168 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 116]---> Sorter-cost: 1117 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 114]---> Adder-cost: 128 maxlim: 67584 bits: 18/17 c ---[ 112]---> Adder-cost: 112 maxlim: 62464 bits: 17/16 c ---[ 110]---> Sorter-cost: 632 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 108]---> Adder-cost: 152 maxlim: 76800 bits: 18/17 c ---[ 106]---> Sorter-cost: 1257 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 104]---> Sorter-cost: 445 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 102]---> Sorter-cost: 1236 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 100]---> Sorter-cost: 408 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 98]---> Sorter-cost: 401 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 96]---> Sorter-cost: 927 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 94]---> Sorter-cost: 315 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 92]---> Sorter-cost: 426 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 90]---> Sorter-cost: 656 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 88]---> Sorter-cost: 596 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 86]---> Sorter-cost: 476 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 84]---> Sorter-cost: 773 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 82]---> Sorter-cost: 407 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 80]---> Sorter-cost: 660 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 78]---> Sorter-cost: 588 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 76]---> Sorter-cost: 984 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 74]---> Sorter-cost: 657 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 72]---> Sorter-cost: 666 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 70]---> Sorter-cost: 969 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 68]---> Sorter-cost: 1305 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 66]---> Sorter-cost: 1049 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 64]---> Adder-cost: 100 maxlim: 55296 bits: 17/16 c ---[ 62]---> Adder-cost: 158 maxlim: 90112 bits: 18/17 c ---[ 60]---> Adder-cost: 150 maxlim: 81920 bits: 18/17 c ---[ 58]---> Sorter-cost: 599 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 56]---> Sorter-cost: 392 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 54]---> Sorter-cost: 370 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 52]---> Sorter-cost: 301 Base: 2 2 2 2 2 2 2 2 2 2 2 c ---[ 50]---> Sorter-cost: 399 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 48]---> Sorter-cost: 1076 Base: 2 2 2 2 2 2 2 2 2 2 7 c ---[ 46]---> Sorter-cost: 1115 Base: 2/oldhome/oroussel/solvers/minisat+_script: line 16: 11091 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.92 0.97 0.94 2/54 11086 Raw data (stat): 11086 (runsolver) R 11085 25568 25567 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 783718566 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.0006 s] Raw data (loadavg): 0.93 0.97 0.94 2/55 11091 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.0022 s] Raw data (loadavg): 0.94 0.97 0.94 2/55 11091 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.0029 s] Raw data (loadavg): 0.95 0.97 0.94 2/55 11091 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.003 s] Raw data (loadavg): 0.96 0.97 0.94 2/55 11091 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.0047 s] Raw data (loadavg): 0.96 0.97 0.94 2/55 11091 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.0053 s] Raw data (loadavg): 0.97 0.97 0.94 2/55 11091 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.0065 s] Raw data (loadavg): 0.97 0.97 0.94 2/55 11091 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.0081 s] Raw data (loadavg): 0.98 0.97 0.94 2/55 11091 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.0088 s] Raw data (loadavg): 0.98 0.97 0.94 2/55 11091 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.009 s] Raw data (loadavg): 0.98 0.97 0.94 2/58 11094 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.01 s] Raw data (loadavg): 1.06 0.99 0.94 2/55 11144 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.011 s] Raw data (loadavg): 1.05 0.99 0.94 2/55 11144 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.011 s] Raw data (loadavg): 1.04 0.99 0.94 2/55 11144 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.012 s] Raw data (loadavg): 1.03 0.99 0.94 2/55 11144 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.013 s] Raw data (loadavg): 1.03 0.99 0.94 2/55 11144 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.013 s] Raw data (loadavg): 1.02 0.99 0.94 2/55 11144 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.013 s] Raw data (loadavg): 1.02 0.99 0.94 2/55 11146 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.013 s] Raw data (loadavg): 1.02 0.99 0.94 2/55 11146 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.014 s] Raw data (loadavg): 1.01 0.99 0.94 2/55 11146 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.014 s] Raw data (loadavg): 1.01 0.99 0.94 2/55 11146 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.015 s] Raw data (loadavg): 1.01 0.99 0.94 2/55 11146 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.016 s] Raw data (loadavg): 1.01 0.99 0.94 2/55 11146 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.016 s] Raw data (loadavg): 1.01 0.99 0.94 2/55 11146 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.016 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11146 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.016 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11146 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.017 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11146 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.017 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11146 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.018 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11146 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.019 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11146 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.019 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11146 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.019 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11146 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.019 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11146 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.02 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11146 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.021 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11146 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.021 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11146 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.022 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11146 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.022 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11146 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.022 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11146 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.022 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11146 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.023 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11146 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.024 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11146 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.024 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.025 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.025 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.025 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.025 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.027 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.027 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.028 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.029 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.029 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.029 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.029 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.031 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.032 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.032 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.033 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.033 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.033 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.034 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.034 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.035 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.035 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.036 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.036 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.139 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.14 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.141 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.148 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.148 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.149 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.149 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.157 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.157 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.159 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.159 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.159 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.16 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.161 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.161 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.161 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.163 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.163 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.163 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.164 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.164 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.164 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.164 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.167 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.168 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.169 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.17 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.17 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.17 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.17 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.172 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.173 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.173 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.174 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.17 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.17 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.17 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.18 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.18 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.18 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.18 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.18 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.18 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.18 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.18 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.18 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.18 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.18 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.18 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.19 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.18 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.18 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.18 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.18 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.19 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.19 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.19 s] Raw data (loadavg): 1.00 0.99 0.94 2/55 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.63 s] Raw data (loadavg): 1.00 0.99 0.94 1/53 11148 Raw data (stat): 11086 (minisat+_script) S 11085 25568 25567 0 -1 0 300 553 0 0 0 0 4 1 18 0 1 0 783718566 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.63 CPU time (s): 1229.96 CPU user time (s): 1228.6 CPU system time (s): 1.36879 CPU usage (%): 100.027 Max. virtual memory (Kb): 2128 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####