| Name | mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-trento1.opb |
| MD5SUM | a75eaaeeef32947fd9ba7cf4d126c00a |
| Bench Category | optimization, big integers (OPTBIGINT) |
| Has Objective Function | YES |
| Satisfiable | |
| (Un)Satisfiability was proved | |
| Best value of the objective function | |
| Optimality of the best value was proved | |
| Number of terms in the objective function | 31855 |
| Biggest coefficient in the objective function | 524288000000000000 |
| Number of bits for the biggest coefficient in the objective function | 59 |
| Sum of the numbers in the objective function | 3494440607063922925 |
| Number of bits of the sum of numbers in the objective function | 62 |
| Biggest number in a constraint | 524288000000000000 |
| Number of bits of the biggest number in a constraint | 59 |
| Biggest sum of numbers in a constraint | 3507240607063922925 |
| Number of bits of the biggest sum of numbers | 62 |
| Best result obtained on this benchmark | |
| Best CPU time to get the best result obtained on this benchmark | |
| Number of variables | 31855 |
| Total number of constraints | 7680 |
| Number of constraints which are clauses | 0 |
| Number of constraints which are cardinality constraints (but not clauses) | 6416 |
| Number of constraints which are nor clauses,nor cardinality constraints | 1264 |
| Minimum length of a constraint | 1 |
| Maximum length of a constraint | 31855 |
LAUNCH ON wulflinc18 THE 2005-09-20 05:46:13 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3504 boxname=wulflinc18 idbench=1160 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: a75eaaeeef32947fd9ba7cf4d126c00a /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-trento1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-trento1.opb IDLAUNCH: 3504 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.177 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 : 3 cpu MHz : 451.177 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: 901464 kB Buffers: 8244 kB Cached: 95920 kB SwapCached: 760 kB Active: 26864 kB Inactive: 79880 kB HighTotal: 131008 kB HighFree: 31584 kB LowTotal: 903652 kB LowFree: 869880 kB SwapTotal: 2097892 kB SwapFree: 2096528 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5772 kB Slab: 20648 kB Committed_AS: 64184 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 06:06:24 (client local time) WITH STATUS 0 IN 1208.18 SECONDS stats: 3504 7 1208.18 0
c Parsing PB file... c PARSE ERROR! [line 7691] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 2512 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################ c -- Clauses(.)/Splits(s): sssssss c ---[2517]---> Adder-cost: 96 maxlim: 6016 bits: 14/13 c ---[2515]---> Adder-cost: 104 maxlim: 6144 bits: 14/13 c ---[2513]---> Adder-cost: 140 maxlim: 8320 bits: 15/14 c ---[2511]---> Adder-cost: 96 maxlim: 6016 bits: 14/13 c ---[2509]---> Sorter-cost: 786 Base: 2 2 2 2 2 2 2 7 c ---[2507]---> Sorter-cost: 621 Base: 2 2 2 2 2 2 2 7 c ---[2505]---> Sorter-cost: 679 Base: 2 2 2 2 2 2 2 7 c ---[2503]---> Adder-cost: 106 maxlim: 6528 bits: 14/13 c ---[2501]---> Adder-cost: 84 maxlim: 7168 bits: 14/13 c ---[2499]---> Adder-cost: 72 maxlim: 6144 bits: 14/13 c ---[2497]---> Adder-cost: 62 maxlim: 6016 bits: 14/13 c ---[2495]---> Sorter-cost: 575 Base: 2 2 2 2 2 2 2 7 c ---[2493]---> Sorter-cost: 575 Base: 2 2 2 2 2 2 2 7 c ---[2491]---> Adder-cost: 140 maxlim: 11648 bits: 15/14 c ---[2489]---> Sorter-cost: 671 Base: 2 2 2 2 2 2 2 7 c ---[2487]---> Sorter-cost: 258 Base: 2 2 2 2 2 2 2 2 c ---[2485]---> Sorter-cost: 717 Base: 2 2 2 2 2 2 2 7 c ---[2483]---> Sorter-cost: 779 Base: 2 2 2 2 2 2 2 7 c ---[2481]---> Sorter-cost: 964 Base: 2 2 2 2 2 2 2 7 c ---[2479]---> Adder-cost: 82 maxlim: 4992 bits: 14/13 c ---[2477]---> Adder-cost: 152 maxlim: 9472 bits: 15/14 c ---[2475]---> Adder-cost: 96 maxlim: 7168 bits: 14/13 c ---[2473]---> Adder-cost: 150 maxlim: 11776 bits: 15/14 c ---[2471]---> Adder-cost: 80 maxlim: 5376 bits: 14/13 c ---[2469]---> Sorter-cost: 934 Base: 2 2 2 2 2 2 2 7 c ---[2467]---> Sorter-cost: 715 Base: 2 2 2 2 2 2 2 7 c ---[2465]---> Sorter-cost: 656 Base: 2 2 2 2 2 2 2 7 c ---[2463]---> Sorter-cost: 1246 Base: 2 2 2 2 2 2 2 7 c ---[2461]---> Sorter-cost: 370 Base: 2 2 2 2 2 2 2 7 c ---[2459]---> Sorter-cost: 264 Base: 2 2 2 2 2 2 2 2 c ---[2457]---> Sorter-cost: 356 Base: 2 2 2 2 2 2 2 7 c ---[2455]---> Sorter-cost: 594 Base: 2 2 2 2 2 2 2 7 c ---[2453]---> Adder-cost: 160 maxlim: 10880 bits: 15/14 c ---[2451]---> Sorter-cost: 430 Base: 2 2 2 2 2 2 2 7 c ---[2449]---> Sorter-cost: 419 Base: 2 2 2 2 2 2 2 7 c ---[2447]---> Sorter-cost: 264 Base: 2 2 2 2 2 2 2 2 c ---[2445]---> Sorter-cost: 226 Base: 2 2 2 2 2 2 2 2 c ---[2443]---> Sorter-cost: 639 Base: 2 2 2 2 2 2 2 7 c ---[2441]---> Sorter-cost: 608 Base: 2 2 2 2 2 2 2 7 c ---[2439]---> Sorter-cost: 604 Base: 2 2 2 2 2 2 2 7 c ---[2437]---> Adder-cost: 292 maxlim: 18304 bits: 16/15 c ---[2435]---> Adder-cost: 278 maxlim: 18944 bits: 16/15 c ---[2433]---> Adder-cost: 204 maxlim: 15104 bits: 15/14 c ---[2431]---> Adder-cost: 126 maxlim: 9600 bits: 15/14 c ---[2429]---> Adder-cost: 124 maxlim: 7808 bits: 14/13 c ---[2427]---> Adder-cost: 48 maxlim: 7808 bits: 14/13 c ---[2425]---> Adder-cost: 84 maxlim: 6912 bits: 14/13 c ---[2423]---> Adder-cost: 104 maxlim: 6144 bits: 14/13 c ---[2421]---> Adder-cost: 118 maxlim: 7168 bits: 14/13 c ---[2419]---> Adder-cost: 90 maxlim: 5760 bits: 14/13 c ---[2417]---> Sorter-cost: 442 Base: 2 2 2 2 2 2 2 7 c ---[2415]---> Sorter-cost: 467 Base: 2 2 2 2 2 2 2 7 c ---[2413]---> Sorter-cost: 703 Base: 2 2 2 2 2 2 2 7 c ---[2411]---> Adder-cost: 108 maxlim: 7936 bits: 14/13 c ---[2409]---> Adder-cost: 106 maxlim: 6528 bits: 14/13 c ---[2407]---> Adder-cost: 82 maxlim: 4992 bits: 14/13 c ---[2405]---> Sorter-cost: 658 Base: 2 2 2 2 2 2 2 7 c ---[2403]---> Sorter-cost: 370 Base: 2 2 2 2 2 2 2 7 c ---[2401]---> Sorter-cost: 689 Base: 2 2 2 2 2 2 2 7 c ---[2399]---> Sorter-cost: 639 Base: 2 2 2 2 2 2 2 7 c ---[2397]---> Sorter-cost: 228 Base: 2 2 2 2 2 2 2 2 c ---[2395]---> Sorter-cost: 218 Base: 2 2 2 2 2 2 2 2 c ---[2393]---> Sorter-cost: 264 Base: 2 2 2 2 2 2 2 2 c ---[2391]---> Sorter-cost: 637 Base: 2 2 2 2 2 2 2 7 c ---[2389]---> Adder-cost: 118 maxlim: 7808 bits: 14/13 c ---[2387]---> Sorter-cost: 657 Base: 2 2 2 2 2 2 2 7 c ---[2385]---> Sorter-cost: 511 Base: 2 2 2 2 2 2 2 7 c ---[2383]---> Sorter-cost: 736 Base: 2 2 2 2 2 2 2 7 c ---[2381]---> Sorter-cost: 885 Base: 2 2 2 2 2 2 2 7 c ---[2379]---> Sorter-cost: 974 Base: 2 2 2 2 2 2 2 7 c ---[2377]---> Sorter-cost: 852 Base: 2 2 2 2 2 2 2 7 c ---[2375]---> Sorter-cost: 406 Base: 2 2 2 2 2 2 2 7 c ---[2373]---> Sorter-cost: 370 Base: 2 2 2 2 2 2 2 7 c ---[2371]---> Sorter-cost: 246 Base: 2 2 2 2 2 2 2 7 c ---[2369]---> Sorter-cost: 264 Base: 2 2 2 2 2 2 2 2 c ---[2367]---> Adder-cost: 84 maxlim: 7296 bits: 14/13 c ---[2365]---> Sorter-cost: 934 Base: 2 2 2 2 2 2 2 7 c ---[2363]---> Sorter-cost: 1023 Base: 2 2 2 2 2 2 2 7 c ---[2361]---> Adder-cost: 90 maxlim: 5376 bits: 14/13 c ---[2359]---> Adder-cost: 92 maxlim: 5632 bits: 14/13 c ---[2357]---> Adder-cost: 86 maxlim: 5376 bits: 14/13 c ---[2355]---> Sorter-cost: 736 Base: 2 2 2 2 2 2 2 7 c ---[2353]---> Adder-cost: 82 maxlim: 4992 bits: 14/13 c ---[2351]---> Adder-cost: 58 maxlim: 5120 bits: 14/13 c ---[2349]---> Adder-cost: 62 maxlim: 5376 bits: 14/13 c ---[2347]---> Adder-cost: 58 maxlim: 5248 bits: 14/13 c ---[2345]---> Adder-cost: 76 maxlim: 6400 bits: 14/13 c ---[2343]---> Sorter-cost: 575 Base: 2 2 2 2 2 2 2 7 c ---[2341]---> Sorter-cost: 573 Base: 2 2 2 2 2 2 2 7 c ---[2339]---> Sorter-cost: 407 Base: 2 2 2 2 2 2 2 7 c ---[2337]---> Sorter-cost: 228 Base: 2 2 2 2 2 2 2 2 c ---[2335]---> Sorter-cost: 691 Base: 2 2 2 2 2 2 2 7 c ---[2333]---> Sorter-cost: 786 Base: 2 2 2 2 2 2 2 7 c ---[2331]---> Sorter-cost: 399 Base: 2 2 2 2 2 2 2 7 c ---[2329]---> Sorter-cost: 268 Base: 2 2 2 2 2 2 2 2 c ---[2327]---> Sorter-cost: 302 Base: 2 2 2 2 2 2 2 2 c ---[2325]---> Adder-cost: 66 maxlim: 6784 bits: 14/13 c ---[2323]---> Sorter-cost: 590 Base: 2 2 2 2 2 2 2 7 c ---[2321]---> Adder-cost: 88 maxlim: 5248 bits: 14/13 c ---[2319]---> Adder-cost: 68 maxlim: 5120 bits: 14/13 c ---[2317]---> Sorter-cost: 996 Base: 2 2 2 2 2 2 2 7 c ---[2315]---> Sorter-cost: 736 Base: 2 2 2 2 2 2 2 7 c ---[2313]---> Sorter-cost: 1130 Base: 2 2 2 2 2 2 2 7 c ---[2311]---> Sorter-cost: 966 Base: 2 2 2 2 2 2 2 7 c ---[2309]---> Sorter-cost: 262 Base: 2 2 2 2 2 2 2 2 c ---[2307]---> Sorter-cost: 276 Base: 2 2 2 2 2 2 2 2 c ---[2305]---> Sorter-cost: 465 Base: 2 2 2 2 2 2 2 7 c ---[2303]---> Adder-cost: 72 maxlim: 5888 bits: 14/13 c ---[2301]---> Sorter-cost: 314 Base: 2 2 2 2 2 2 2 2 c ---[2299]---> Sorter-cost: 234 Base: 2 2 2 2 2 2 2 2 c ---[2297]---> Adder-cost: 142 maxlim: 8448 bits: 15/14 c ---[2295]---> Adder-cost: 104 maxlim: 9344 bits: 15/14 c ---[2293]---> Adder-cost: 136 maxlim: 8192 bits: 15/14 c ---[2291]---> Adder-cost: 82 maxlim: 4864 bits: 14/13 c ---[2289]---> Adder-cost: 78 maxlim: 4992 bits: 14/13 c ---[2287]---> Adder-cost: 70 maxlim: 4864 bits: 14/13 c ---[2285]---> Sorter-cost: 430 Base: 2 2 2 2 2 2 2 7 c ---[2283]---> Sorter-cost: 594 Base: 2 2 2 2 2 2 2 7 c ---[2281]---> Sorter-cost: 730 Base: 2 2 2 2 2 2 2 7 c ---[2279]---> Sorter-cost: 629 Base: 2 2 2 2 2 2 2 7 c ---[2277]---> Sorter-cost: 306 Base: 2 2 2 2 2 2 2 2 c ---[2275]---> Sorter-cost: 370 Base: 2 2 2 2 2 2 2 7 c ---[2273]---> Sorter-cost: 770 Base: 2 2 2 2 2 2 2 7 c ---[2271]---> Adder-cost: 82 maxlim: 4864 bits: 14/13 c ---[2269]---> Adder-cost: 40 maxlim: 4864 bits: 14/13 c ---[2267]---> Adder-cost: 40 maxlim: 4864 bits: 14/13 c ---[2265]---> Adder-cost: 252 maxlim: 15872 bits: 15/14 c ---[2263]---> Sorter-cost: 639 Base: 2 2 2 2 2 2 2 7 c ---[2261]---> Sorter-cost: 934 Base: 2 2 2 2 2 2 2 7 c ---[2259]---> Sorter-cost: 550 Base: 2 2 2 2 2 2 2 7 c ---[2257]---> Sorter-cost: 467 Base: 2 2 2 2 2 2 2 7 c ---[2255]---> Sorter-cost: 264 Base: 2 2 2 2 2 2 2 2 c ---[2253]---> Sorter-cost: 404 Base: 2 2 2 2 2 2 2 7 c ---[2251]---> Sorter-cost: 314 Base: 2 2 2 2 2 2 2 2 c ---[2249]---> Sorter-cost: 276 Base: 2 2 2 2 2 2 2 2 c ---[2247]---> Sorter-cost: 268 Base: 2 2 2 2 2 2 2 2 c ---[2245]---> Adder-cost: 94 maxlim: 5632 bits: 14/13 c ---[2243]---> Adder-cost: 86 maxlim: 5120 bits: 14/13 c ---[2241]---> Sorter-cost: 872 Base: 2 2 2 2 2 2 2 7 c ---[2239]---> Adder-cost: 80 maxlim: 4736 bits: 14/13 c ---[2237]---> Adder-cost: 68 maxlim: 5248 bits: 14/13 c ---[2235]---> Sorter-cost: 372 Base: 2 2 2 2 2 2 2 7 c ---[2233]---> Sorter-cost: 573 Base: 2 2 2 2 2 2 2 7 c ---[2231]---> Sorter-cost: 394 Base: 2 2 2 2 2 2 2 7 c ---[2229]---> Sorter-cost: 415 Base: 2 2 2 2 2 2 2 7 c ---[2227]---> Sorter-cost: 417 Base: 2 2 2 2 2 2 2 7 c ---[2225]---> Sorter-cost: 266 Base: 2 2 2 2 2 2 2 2 c ---[2223]---> Sorter-cost: 594 Base: 2 2 2 2 2 2 2 7 c ---[2221]---> Sorter-cost: 618 Base: 2 2 2 2 2 2 2 7 c ---[2219]---> Sorter-cost: 956 Base: 2 2 2 2 2 2 2 7 c ---[2217]---> Adder-cost: 176 maxlim: 10752 bits: 15/14 c ---[2215]---> Adder-cost: 142 maxlim: 8704 bits: 15/14 c ---[2213]---> Adder-cost: 98 maxlim: 6272 bits: 14/13 c ---[2211]---> Sorter-cost: 934 Base: 2 2 2 2 2 2 2 7 c ---[2209]---> Sorter-cost: 372 Base: 2 2 2 2 2 2 2 7 c ---[2207]---> Sorter-cost: 457 Base: 2 2 2 2 2 2 2 7 c ---[2205]---> Sorter-cost: 571 Base: 2 2 2 2 2 2 2 7 c ---[2203]---> Sorter-cost: 437 Base: 2 2 2 2 2 2 2 7 c ---[2201]---> Sorter-cost: 252 Base: 2 2 2 2 2 2 2 2 c ---[2199]---> Sorter-cost: 967 Base: 2 2 2 2 2 2 2 7 c ---[2197]---> Sorter-cost: 575 Base: 2 2 2 2 2 2 2 7 c ---[2195]---> Sorter-cost: 570 Base: 2 2 2 2 2 2 2 7 c ---[2193]---> Sorter-cost: 366 Base: 2 2 2 2 2 2 2 7 c ---[2191]---> Sorter-cost: 218 Base: 2 2 2 2 2 2 2 2 c ---[2189]---> Sorter-cost: 407 Base: 2 2 2 2 2 2 2 7 c ---[2187]---> Sorter-cost: 592 Base: 2 2 2 2 2 2 2 7 c ---[2185]---> Sorter-cost: 580 Base: 2 2 2 2 2 2 2 7 c ---[2183]---> Sorter-cost: 616 Base: 2 2 2 2 2 2 2 7 c ---[2181]---> Sorter-cost: 564 Base: 2 2 2 2 2 2 2 7 c ---[2179]---> Adder-cost: 88 maxlim: 5248 bits: 14/13 c ---[2177]---> Sorter-cost: 950 Base: 2 2 2 2 2 2 2 7 c ---[2175]---> Adder-cost: 78 maxlim: 5376 bits: 14/13 c ---[2173]---> Adder-cost: 112 maxlim: 7040 bits: 14/13 c ---[2171]---> Adder-cost: 80 maxlim: 5632 bits: 14/13 c ---[2169]---> Adder-cost: 64 maxlim: 4992 bits: 14/13 c ---[2167]---> Sorter-cost: 996 Base: 2 2 2 2 2 2 2 7 c ---[2165]---> Sorter-cost: 266 Base: 2 2 2 2 2 2 2 2 c ---[2163]---> BDD-cost: 31 c ---[2161]---> Sorter-cost: 633 Base: 2 2 2 2 2 2 2 7 c ---[2159]---> Sorter-cost: 736 Base: 2 2 2 2 2 2 2 7 c ---[2157]---> Sorter-cost: 593 Base: 2 2 2 2 2 2 2 7 c ---[2155]---> Sorter-cost: 473 Base: 2 2 2 2 2 2 2 7 c ---[2153]---> Sorter-cost: 774 Base: 2 2 2 2 2 2 2 7 c ---[2151]---> Adder-cost: 76 maxlim: 4480 bits: 14/13 c ---[2149]---> Adder-cost: 78 maxlim: 5504 bits: 14/13 c ---[2147]---> Adder-cost: 76 maxlim: 4864 bits: 14/13 c ---[2145]---> Adder-cost: 64 maxlim: 4992 bits: 14/13 c ---[2143]---> Sorter-cost: 736 Base: 2 2 2 2 2 2 2 7 c ---[2141]---> Sorter-cost: 934 Base: 2 2 2 2 2 2 2 7 c ---[2139]---> Sorter-cost: 461 Base: 2 2 2 2 2 2 2 7 c ---[2137]---> Sorter-cost: 641 Base: 2 2 2 2 2 2 2 7 c ---[2135]---> Adder-cost: 88 maxlim: 5120 bits: 14/13 c ---[2133]---> Adder-cost: 58 maxlim: 4992 bits: 14/13 c ---[2131]---> Adder-cost: 104 maxlim: 6528 bits: 14/13 c ---[2129]---> Adder-cost: 90 maxlim: 6912 bits: 14/13 c ---[2127]---> Sorter-cost: 934 Base: 2 2 2 2 2 2 2 7 c ---[2125]---> Sorter-cost: 907 Base: 2 2 2 2 2 2 2 7 c ---[2123]---> Sorter-cost: 676 Base: 2 2 2 2 2 2 2 7 c ---[2121]---> Adder-cost: 106 maxlim: 6528 bits: 14/13 c ---[2119]---> Sorter-cost: 381 Base: 2 2 2 2 2 2 2 7 c ---[2117]---> Adder-cost: 146 maxlim: 8832 bits: 15/14 c ---[2115]---> Sorter-cost: 681 Base: 2 2 2 2 2 2 2 7 c ---[2113]---> Sorter-cost: 447 Base: 2 2 2 2 2 2 2 7 c ---[2111]---> Sorter-cost: 681 Base: 2 2 2 2 2 2 2 7 c ---[2109]---> Adder-cost: 104 maxlim: 6144 bits: 14/13 c ---[2107]---> Adder-cost: 84 maxlim: 6016 bits: 14/13 c ---[2105]---> Adder-cost: 40 maxlim: 6016 bits: 14/13 c ---[2103]---> Sorter-cost: 445 Base: 2 2 2 2 2 2 2 7 c ---[2101]---> Adder-cost: 118 maxlim: 7296 bits: 14/13 c ---[2099]---> Adder-cost: 68 maxlim: 4352 bits: 14/13 c ---[2097]---> Sorter-cost: 736 Base: 2 2 2 2 2 2 2 7 c ---[2095]---> Sorter-cost: 415 Base: 2 2 2 2 2 2 2 7 c ---[2093]---> Adder-cost: 82 maxlim: 4992 bits: 14/13 c ---[2091]---> Adder-cost: 106 maxlim: 6912 bits: 14/13 c ---[2089]---> Adder-cost: 88 maxlim: 5248 bits: 14/13 c ---[2087]---> Adder-cost: 110 maxlim: 6784 bits: 14/13 c ---[2085]---> Adder-cost: 66 maxlim: 4992 bits: 14/13 c ---[2083]---> Adder-cost: 70 maxlim: 5376 bits: 14/13 c ---[2081]---> Sorter-cost: 996 Base: 2 2 2 2 2 2 2 7 c ---[2079]---> Sorter-cost: 924 Base: 2 2 2 2 2 2 2 7 c ---[2077]---> Sorter-cost: 528 Base: 2 2 2 2 2 2 2 7 c ---[2075]---> Sorter-cost: 934 Base: 2 2 2 2 2 2 2 7 c ---[2073]---> Sorter-cost: 392 Base: 2 2 2 2 2 2 2 7 c ---[2071]---> Sorter-cost: 645 Base: 2 2 2 2 2 2 2 7 c ---[2069]---> Adder-cost: 124 maxlim: 7808 bits: 14/13 c ---[2067]---> Adder-cost: 94 maxlim: 7296 bits: 14/13 c ---[2065]---> Adder-cost: 72 maxlim: 4352 bits: 14/13 c ---[2063]---> Adder-cost: 106 maxlim: 6400 bits: 14/13 c ---[2061]---> Adder-cost: 84 maxlim: 6912 bits: 14/13 c ---[2059]---> Sorter-cost: 406 Base: 2 2 2 2 2 2 2 7 c ---[2057]---> Sorter-cost: 574 Base: 2 2 2 2 2 2 2 7 c ---[2055]---> Sorter-cost: 711 Base: 2 2 2 2 2 2 2 7 c ---[2053]---> Sorter-cost: 582 Base: 2 2 2 2 2 2 2 7 c ---[2051]---> Sorter-cost: 390 Base: 2 2 2 2 2 2 2 7 c ---[2049]---> Sorter-cost: 565 Base: 2 2 2 2 2 2 2 7 c ---[2047]---> Sorter-cost: 324 Base: 2 2 2 2 2 2 2 7 c ---[2045]---> Sorter-cost: 228 Base: 2 2 2 2 2 2 2 2 c ---[2043]---> Adder-cost: 126 maxlim: 7936 bits: 14/13 c ---[2041]---> Adder-cost: 52 maxlim: 7936 bits: 14/13 c ---[2039]---> Sorter-cost: 996 Base: 2 2 2 2 2 2 2 7 c ---[2037]---> Adder-cost: 94 maxlim: 5632 bits: 14/13 c ---[2035]---> Adder-cost: 60 maxlim: 5248 bits: 14/13 c ---[2033]---> Adder-cost: 110 maxlim: 6656 bits: 14/13 c ---[2031]---> Sorter-cost: 314 Base: 2 2 2 2 2 2 2 2 c ---[2029]---> Adder-cost: 110 maxlim: 7168 bits: 14/13 c ---[2027]---> Sorter-cost: 907 Base: 2 2 2 2 2 2 2 7 c ---[2025]---> Sorter-cost: 1082 Base: 2 2 2 2 2 2 2 7 c ---[2023]---> Sorter-cost: 687 Base: 2 2 2 2 2 2 2 7 c ---[2021]---> Sorter-cost: 691 Base: 2 2 2 2 2 2 2 7 c ---[2019]---> Sorter-cost: 442 Base: 2 2 2 2 2 2 2 7 c ---[2017]---> Sorter-cost: 290 Base: 2 2 2 2 2 2 2 2 c ---[2015]---> Sorter-cost: 383 Base: 2 2 2 2 2 2 2 7 c ---[2013]---> Adder-cost: 276 maxlim: 16896 bits: 16/15 c ---[2011]---> Sorter-cost: 388 Base: 2 2 2 2 2 2 2 7 c ---[2009]---> Sorter-cost: 372 Base: 2 2 2 2 2 2 2 7 c ---[2007]---> Sorter-cost: 246 Base: 2 2 2 2 2 2 2 7 c ---[2005]---> Sorter-cost: 398 Base: 2 2 2 2 2 2 2 7 c ---[2003]---> Sorter-cost: 264 Base: 2 2 2 2 2 2 2 2 c ---[2001]---> Sorter-cost: 639 Base: 2 2 2 2 2 2 2 7 c ---[1999]---> Sorter-cost: 256 Base: 2 2 2 2 2 2 2 2 c ---[1997]---> Sorter-cost: 534 Base: 2 2 2 2 2 2 2 7 c ---[1995]---> Sorter-cost: 408 Base: 2 2 2 2 2 2 2 7 c ---[1993]---> Sorter-cost: 397 Base: 2 2 2 2 2 2 2 7 c ---[1991]---> Sorter-cost: 574 Base: 2 2 2 2 2 2 2 7 c ---[1989]---> Sorter-cost: 569 Base: 2 2 2 2 2 2 2 7 c ---[1987]---> Sorter-cost: 218 Base: 2 2 2 2 2 2 2 2 c ---[1985]---> Sorter-cost: 594 Base: 2 2 2 2 2 2 2 7 c ---[1983]---> Sorter-cost: 407 Base: 2 2 2 2 2 2 2 7 c ---[1981]---> Sorter-cost: 228 Base: 2 2 2 2 2 2 2 2 c ---[1979]---> Sorter-cost: 639 Base: 2 2 2 2 2 2 2 7 c ---[1977]---> Sorter-cost: 473 Base: 2 2 2 2 2 2 2 7 c ---[1975]---> Sorter-cost: 581 Base: 2 2 2 2 2 2 2 7 c ---[1973]---> Sorter-cost: 654 Base: 2 2 2 2 2 2 2 7 c ---[1971]---> Adder-cost: 94 maxlim: 5760 bits: 14/13 c ---[1969]---> Sorter-cost: 218 Base: 2 2 2 2 2 2 2 2 c ---[1967]---> Adder-cost: 110 maxlim: 6912 bits: 14/13 c ---[1965]---> Adder-cost: 84 maxlim: 5120 bits: 14/13 c ---[1963]---> Adder-cost: 86 maxlim: 5888 bits: 14/13 c ---[1961]---> Adder-cost: 86 maxlim: 5504 bits: 14/13 c ---[1959]---> Sorter-cost: 934 Base: 2 2 2 2 2 2 2 7 c ---[1957]---> Adder-cost: 94 maxlim: 5632 bits: 14/13 c ---[1955]---> Adder-cost: 72 maxlim: 4736 bits: 14/13 c ---[1953]---> Adder-cost: 58 maxlim: 4480 bits: 14/13 c ---[1951]---> Sorter-cost: 786 Base: 2 2 2 2 2 2 2 7 c ---[1949]---> Sorter-cost: 421 Base: 2 2 2 2 2 2 2 7 c ---[1947]---> Adder-cost: 118 maxlim: 7296 bits: 14/13 c ---[1945]---> Sorter-cost: 293 Base: 2 2 2 2 2 2 2 7 c ---[1943]---> Sorter-cost: 463 Base: 2 2 2 2 2 2 2 7 c ---[1941]---> Sorter-cost: 404 Base: 2 2 2 2 2 2 2 7 c ---[1939]---> Adder-cost: 90 maxlim: 5504 bits: 14/13 c ---[1937]---> Adder-cost: 70 maxlim: 5504 bits: 14/13 c ---[1935]---> Adder-cost: 70 maxlim: 7168 bits: 14/13 c ---[1933]---> Sorter-cost: 575 Base: 2 2 2 2 2 2 2 7 c ---[1931]---> Sorter-cost: 656 Base: 2 2 2 2 2 2 2 7 c ---[1929]---> Sorter-cost: 580 Base: 2 2 2 2 2 2 2 7 c ---[1927]---> Sorter-cost: 571 Base: 2 2 2 2 2 2 2 7 c ---[1925]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 c ---[1923]---> Sorter-cost: 616 Base: 2 2 2 2 2 2 2 7 c ---[1921]---> Adder-cost: 126 maxlim: 8064 bits: 14/13 c ---[1919]---> Sorter-cost: 266 Base: 2 2 2 2 2 2 2 2 c ---[1917]---> Adder-cost: 94 maxlim: 5632 bits: 14/13 c ---[1915]---> Adder-cost: 42 maxlim: 5632 bits: 14/13 c ---[1913]---> Adder-cost: 82 maxlim: 6144 bits: 14/13 c ---[1911]---> Adder-cost: 68 maxlim: 5120 bits: 14/13 c ---[1909]---> Adder-cost: 80 maxlim: 4736 bits: 14/13 c ---[1907]---> Adder-cost: 68 maxlim: 4992 bits: 14/13 c ---[1905]---> Adder-cost: 62 maxlim: 4736 bits: 14/13 c ---[1903]---> Adder-cost: 172 maxlim: 10496 bits: 15/14 c ---[1901]---> Adder-cost: 62 maxlim: 4864 bits: 14/13 c ---[1899]---> Sorter-cost: 372 Base: 2 2 2 2 2 2 2 7 c ---[1897]---> Sorter-cost: 525 Base: 2 2 2 2 2 2 2 7 c ---[1895]---> Sorter-cost: 523 Base: 2 2 2 2 2 2 2 7 c ---[1893]---> Sorter-cost: 358 Base: 2 2 2 2 2 2 2 7 c ---[1891]---> Sorter-cost: 679 Base: 2 2 2 2 2 2 2 7 c ---[1889]---> Sorter-cost: 616 Base: 2 2 2 2 2 2 2 7 c ---[1887]---> Adder-cost: 102 maxlim: 6272 bits: 14/13 c ---[1885]---> Sorter-cost: 268 Base: 2 2 2 2 2 2 2 2 c ---[1883]---> Sorter-cost: 681 Base: 2 2 2 2 2 2 2 7 c ---[1881]---> Adder-cost: 138 maxlim: 10624 bits: 15/14 c ---[1879]---> Sorter-cost: 507 Base: 2 2 2 2 2 2 2 7 c ---[1877]---> Adder-cost: 162 maxlim: 9984 bits: 15/14 c ---[1875]---> Sorter-cost: 447 Base: 2 2 2 2 2 2 2 7 c ---[1873]---> Sorter-cost: 395 Base: 2 2 2 2 2 2 2 7 c ---[1871]---> Sorter-cost: 736 Base: 2 2 2 2 2 2 2 7 c ---[1869]---> Sorter-cost: 620 Base: 2 2 2 2 2 2 2 7 c ---[1867]---> Sorter-cost: 665 Base: 2 2 2 2 2 2 2 7 c ---[1865]---> Sorter-cost: 685 Base: 2 2 2 2 2 2 2 7 c ---[1863]---> Sorter-cost: 990 Base: 2 2 2 2 2 2 2 7 c ---[1861]---> Adder-cost: 112 maxlim: 8448 bits: 15/14 c ---[1859]---> Adder-cost: 92 maxlim: 5760 bits: 14/13 c ---[1857]---> Sorter-cost: 312 Base: 2 2 2 2 2 2 2 2 c ---[1855]---> Adder-cost: 74 maxlim: 4480 bits: 14/13 c ---[1853]---> Adder-cost: 124 maxlim: 8064 bits: 14/13 c ---[1851]---> Adder-cost: 120 maxlim: 7936 bits: 14/13 c ---[1849]---> Adder-cost: 98 maxlim: 7936 bits: 14/13 c ---[1847]---> Adder-cost: 84 maxlim: 7296 bits: 14/13 c ---[1845]---> Adder-cost: 86 maxlim: 7168 bits: 14/13 c ---[1843]---> Sorter-cost: 616 Base: 2 2 2 2 2 2 2 7 c ---[1841]---> Sorter-cost: 893 Base: 2 2 2 2 2 2 2 7 c ---[1839]---> Adder-cost: 86 maxlim: 7680 bits: 14/13 c ---[1837]---> Sorter-cost: 885 Base: 2 2 2 2 2 2 2 7 c ---[1835]---> Sorter-cost: 1013 Base: 2 2 2 2 2 2 2 7 c ---[1833]---> Sorter-cost: 903 Base: 2 2 2 2 2 2 2 7 c ---[1831]---> Sorter-cost: 598 Base: 2 2 2 2 2 2 2 7 c ---[1829]---> Sorter-cost: 590 Base: 2 2 2 2 2 2 2 7 c ---[1827]---> Sorter-cost: 362 Base: 2 2 2 2 2 2 2 7 c ---[1825]---> Adder-cost: 82 maxlim: 4992 bits: 14/13 c ---[1823]---> Adder-cost: 72 maxlim: 4736 bits: 14/13 c ---[1821]---> Sorter-cost: 440 Base: 2 2 2 2 2 2 2 7 c ---[1819]---> Sorter-cost: 996 Base: 2 2 2 2 2 2 2 7 c ---[1817]---> Sorter-cost: 932 Base: 2 2 2 2 2 2 2 7 c ---[1815]---> Sorter-cost: 674 Base: 2 2 2 2 2 2 2 7 c ---[1813]---> Sorter-cost: 893 Base: 2 2 2 2 2 2 2 7 c ---[1811]---> Adder-cost: 158 maxlim: 9856 bits: 15/14 c ---[1809]---> Adder-cost: 114 maxlim: 7680 bits: 14/13 c ---[1807]---> Adder-cost: 98 maxlim: 7680 bits: 14/13 c ---[1805]---> Sorter-cost: 616 Base: 2 2 2 2 2 2 2 7 c ---[1803]---> Sorter-cost: 604 Base: 2 2 2 2 2 2 2 7 c ---[1801]---> Sorter-cost: 634 Base: 2 2 2 2 2 2 2 7 c ---[1799]---> Sorter-cost: 717 Base: 2 2 2 2 2 2 2 7 c ---[1797]---> Sorter-cost: 268 Base: 2 2 2 2 2 2 2 2 c ---[1795]---> Sorter-cost: 465 Base: 2 2 2 2 2 2 2 7 c ---[1793]---> Sorter-cost: 405 Base: 2 2 2 2 2 2 2 7 c ---[1791]---> Sorter-cost: 364 Base: 2 2 2 2 2 2 2 7 c ---[1789]---> Sorter-cost: 354 Base: 2 2 2 2 2 2 2 7 c ---[1787]---> Adder-cost: 112 maxlim: 7040 bits: 14/13 c ---[1785]---> Adder-cost: 72 maxlim: 6272 bits: 14/13 c ---[1783]---> Adder-cost: 62 maxlim: 6272 bits: 14/13 c ---[1781]---> Sorter-cost: 447 Base: 2 2 2 2 2 2 2 7 c ---[1779]---> Sorter-cost: 644 Base: 2 2 2 2 2 2 2 7 c ---[1777]---> Sorter-cost: 779 Base: 2 2 2 2 2 2 2 7 c ---[1775]---> Sorter-cost: 639 Base: 2 2 2 2 2 2 2 7 c ---[1773]---> Sorter-cost: 442 Base: 2 2 2 2 2 2 2 7 c ---[1771]---> Sorter-cost: 371 Base: 2 2 2 2 2 2 2 7 c ---[1769]---> Sorter-cost: 316 Base: 2 2 2 2 2 2 2 7 c ---[1767]---> Sorter-cost: 555 Base: 2 2 2 2 2 2 2 7 c ---[1765]---> Sorter-cost: 946 Base: 2 2 2 2 2 2 2 7 c ---[1763]---> Sorter-cost: 715 Base: 2 2 2 2 2 2 2 7 c ---[1761]---> Sorter-cost: 724 Base: 2 2 2 2 2 2 2 7 c ---[1759]---> Sorter-cost: 675 Base: 2 2 2 2 2 2 2 7 c ---[1757]---> Sorter-cost: 758 Base: 2 2 2 2 2 2 2 7 c ---[1755]---> Adder-cost: 88 maxlim: 5248 bits: 14/13 c ---[1753]---> Adder-cost: 80 maxlim: 5248 bits: 14/13 c ---[1751]---> Adder-cost: 74 maxlim: 4736 bits: 14/13 c ---[1749]---> Sorter-cost: 934 Base: 2 2 2 2 2 2 2 7 c ---[1747]---> Adder-cost: 78 maxlim: 5120 bits: 14/13 c ---[1745]---> Sorter-cost: 658 Base: 2 2 2 2 2 2 2 7 c ---[1743]---> Sorter-cost: 631 Base: 2 2 2 2 2 2 2 7 c ---[1741]---> Sorter-cost: 718 Base: 2 2 2 2 2 2 2 7 c ---[1739]---> Sorter-cost: 620 Base: 2 2 2 2 2 2 2 7 c ---[1737]---> Sorter-cost: 960 Base: 2 2 2 2 2 2 2 7 c ---[1735]---> Sorter-cost: 891 Base: 2 2 2 2 2 2 2 7 c ---[1733]---> Sorter-cost: 413 Base: 2 2 2 2 2 2 2 7 c ---[1731]---> Sorter-cost: 586 Base: 2 2 2 2 2 2 2 7 c ---[1729]---> Sorter-cost: 443 Base: 2 2 2 2 2 2 2 7 c ---[1727]---> Sorter-cost: 264 Base: 2 2 2 2 2 2 2 2 c ---[1725]---> Sorter-cost: 230 Base: 2 2 2 2 2 2 2 2 c ---[1723]---> Sorter-cost: 554 Base: 2 2 2 2 2 2 2 7 c ---[1721]---> Sorter-cost: 266 Base: 2 2 2 2 2 2 2 2 c ---[1719]---> Sorter-cost: 262 Base: 2 2 2 2 2 2 2 2 c ---[1717]---> Sorter-cost: 417 Base: 2 2 2 2 2 2 2 7 c ---[1715]---> Sorter-cost: 973 Base: 2 2 2 2 2 2 2 7 c ---[1713]---> Sorter-cost: 659 Base: 2 2 2 2 2 2 2 7 c ---[1711]---> Sorter-cost: 404 Base: 2 2 2 2 2 2 2 7 c ---[1709]---> Sorter-cost: 310 Base: 2 2 2 2 2 2 2 2 c ---[1707]---> Sorter-cost: 404 Base: 2 2 2 2 2 2 2 7 c ---[1705]---> Sorter-cost: 366 Base: 2 2 2 2 2 2 2 7 c ---[1703]---> Sorter-cost: 419 Base: 2 2 2 2 2 2 2 7 c ---[1701]---> Sorter-cost: 310 Base: 2 2 2 2 2 2 2 2 c ---[1699]---> Sorter-cost: 402 Base: 2 2 2 2 2 2 2 7 c ---[1697]---> Sorter-cost: 407 Base: 2 2 2 2 2 2 2 7 c ---[1695]---> Sorter-cost: 956 Base: 2 2 2 2 2 2 2 7 c ---[1693]---> Sorter-cost: 545 Base: 2 2 2 2 2 2 2 7 c ---[1691]---> Sorter-cost: 577 Base: 2 2 2 2 2 2 2 7 c ---[1689]---> Sorter-cost: 541 Base: 2 2 2 2 2 2 2 7 c ---[1687]---> Sorter-cost: 568 Base: 2 2 2 2 2 2 2 7 c ---[1685]---> Sorter-cost: 543 Base: 2 2 2 2 2 2 2 7 c ---[1683]---> Sorter-cost: 794 Base: 2 2 2 2 2 2 2 7 c ---[1681]---> Sorter-cost: 575 Base: 2 2 2 2 2 2 2 7 c ---[1679]---> Sorter-cost: 455 Base: 2 2 2 2 2 2 2 7 c ---[1677]---> Sorter-cost: 1026 Base: 2 2 2 2 2 2 2 7 c ---[1675]---> Sorter-cost: 280 Base: 2 2 2 2 2 2 2 7 c ---[1673]---> Sorter-cost: 280 Base: 2 2 2 2 2 2 2 7 c ---[1671]---> Sorter-cost: 280 Base: 2 2 2 2 2 2 2 7 c ---[1669]---> Sorter-cost: 590 Base: 2 2 2 2 2 2 2 7 c ---[1667]---> Adder-cost: 126 maxlim: 7936 bits: 14/13 c ---[1665]---> Adder-cost: 140 maxlim: 8832 bits: 15/14 c ---[1663]---> Adder-cost: 112 maxlim: 8064 bits: 14/13 c ---[1661]---> Adder-cost: 58 maxlim: 5376 bits: 14/13 c ---[1659]---> Sorter-cost: 994 Base: 2 2 2 2 2 2 2 7 c ---[1657]---> Sorter-cost: 749 Base: 2 2 2 2 2 2 2 7 c ---[1655]---> Sorter-cost: 912 Base: 2 2 2 2 2 2 2 7 c ---[1653]---> Sorter-cost: 612 Base: 2 2 2 2 2 2 2 7 c ---[1651]---> Sorter-cost: 689 Base: 2 2 2 2 2 2 2 7 c ---[1649]---> Sorter-cost: 656 Base: 2 2 2 2 2 2 2 7 c ---[1647]---> Sorter-cost: 828 Base: 2 2 2 2 2 2 2 7 c ---[1645]---> Sorter-cost: 828 Base: 2 2 2 2 2 2 2 7 c ---[1643]---> Adder-cost: 148 maxlim: 9088 bits: 15/14 c ---[1641]---> Adder-cost: 170 maxlim: 10240 bits: 15/14 c ---[1639]---> Adder-cost: 114 maxlim: 8576 bits: 15/14 c ---[1637]---> Adder-cost: 92 maxlim: 6528 bits: 14/13 c ---[1635]---> Adder-cost: 72 maxlim: 6400 bits: 14/13 c ---[1633]---> Sorter-cost: 916 Base: 2 2 2 2 2 2 2 7 c ---[1631]---> Adder-cost: 68 maxlim: 5888 bits: 14/13 c ---[1629]---> Adder-cost: 60 maxlim: 5632 bits: 14/13 c ---[1627]---> Adder-cost: 58 maxlim: 5760 bits: 14/13 c ---[1625]---> Adder-cost: 106 maxlim: 6400 bits: 14/13 c ---[1623]---> Adder-cost: 104 maxlim: 6400 bits: 14/13 c ---[1621]---> Adder-cost: 44 maxlim: 6400 bits: 14/13 c ---[1619]---> Adder-cost: 44 maxlim: 6400 bits: 14/13 c ---[1617]---> Adder-cost: 68 maxlim: 6656 bits: 14/13 c ---[1615]---> Adder-cost: 92 maxlim: 5888 bits: 14/13 c ---[1613]---> Adder-cost: 56 maxlim: 4864 bits: 14/13 c ---[1611]---> Sorter-cost: 602 Base: 2 2 2 2 2 2 2 7 c ---[1609]---> Adder-cost: 66 maxlim: 4352 bits: 14/13 c ---[1607]---> Sorter-cost: 905 Base: 2 2 2 2 2 2 2 7 c ---[1605]---> Sorter-cost: 581 Base: 2 2 2 2 2 2 2 7 c ---[1603]---> Sorter-cost: 598 Base: 2 2 2 2 2 2 2 7 c ---[1601]---> Sorter-cost: 551 Base: 2 2 2 2 2 2 2 7 c ---[1599]---> Sorter-cost: 559 Base: 2 2 2 2 2 2 2 7 c ---[1597]---> Sorter-cost: 585 Base: 2 2 2 2 2 2 2 7 c ---[1595]---> Sorter-cost: 606 Base: 2 2 2 2 2 2 2 7 c ---[1593]---> Sorter-cost: 891 Base: 2 2 2 2 2 2 2 7 c ---[1591]---> Sorter-cost: 826 Base: 2 2 2 2 2 2 2 7 c ---[1589]---> Sorter-cost: 656 Base: 2 2 2 2 2 2 2 7 c ---[1587]---> Sorter-cost: 772 Base: 2 2 2 2 2 2 2 7 c ---[1585]---> Sorter-cost: 663 Base: 2 2 2 2 2 2 2 7 c ---[1583]---> Sorter-cost: 628 Base: 2 2 2 2 2 2 2 7 c ---[1581]---> Sorter-cost: 570 Base: 2 2 2 2 2 2 2 7 c ---[1579]---> Sorter-cost: 650 Base: 2 2 2 2 2 2 2 7 c ---[1577]---> Sorter-cost: 781 Base: 2 2 2 2 2 2 2 7 c ---[1575]---> Sorter-cost: 1030 Base: 2 2 2 2 2 2 2 7 c ---[1573]---> Sorter-cost: 984 Base: 2 2 2 2 2 2 2 7 c ---[1571]---> Adder-cost: 140 maxlim: 8192 bits: 15/14 c ---[1569]---> Adder-cost: 140 maxlim: 8320 bits: 15/14 c ---[1567]---> Adder-cost: 40 maxlim: 6016 bits: 14/13 c ---[1565]---> Sorter-cost: 464 Base: 2 2 2 2 2 2 2 7 c ---[1563]---> Adder-cost: 104 maxlim: 8448 bits: 15/14 c ---[1561]---> Adder-cost: 86 maxlim: 8704 bits: 15/14 c ---[1559]---> Adder-cost: 112 maxlim: 8832 bits: 15/14 c ---[1557]---> Adder-cost: 88 maxlim: 5504 bits: 14/13 c ---[1555]---> Adder-cost: 84 maxlim: 6016 bits: 14/13 c ---[1553]---> Adder-cost: 80 maxlim: 5760 bits: 14/13 c ---[1551]---> Adder-cost: 60 maxlim: 5760 bits: 14/13 c ---[1549]---> Adder-cost: 62 maxlim: 5632 bits: 14/13 c ---[1547]---> Adder-cost: 80 maxlim: 6400 bits: 14/13 c ---[1545]---> Adder-cost: 122 maxlim: 8064 bits: 14/13 c ---[1543]---> Sorter-cost: 528 Base: 2 2 2 2 2 2 2 7 c ---[1541]---> Adder-cost: 86 maxlim: 7808 bits: 14/13 c ---[1539]---> Adder-cost: 80 maxlim: 7936 bits: 14/13 c ---[1537]---> Adder-cost: 80 maxlim: 7552 bits: 14/13 c ---[1535]---> Adder-cost: 80 maxlim: 7424 bits: 14/13 c ---[1533]---> Adder-cost: 100 maxlim: 7168 bits: 14/13 c ---[1531]---> Adder-cost: 70 maxlim: 6656 bits: 14/13 c ---[1529]---> Adder-cost: 88 maxlim: 5120 bits: 14/13 c ---[1527]---> Adder-cost: 70 maxlim: 5120 bits: 14/13 c ---[1525]---> Adder-cost: 62 maxlim: 5120 bits: 14/13 c ---[1523]---> Adder-cost: 58 maxlim: 4992 bits: 14/13 c ---[1521]---> Sorter-cost: 577 Base: 2 2 2 2 2 2 2 7 c ---[1519]---> Adder-cost: 50 maxlim: 4736 bits: 14/13 c ---[1518]---> Adder-cost: 8864 maxlim: 460671 bits: 20/19 c ---[1516]---> Adder-cost: 2600 maxlim: 170112 bits: 18/18 c ---[1514]---> Adder-cost: 269 maxlim: 15744 bits: 15/14 c ---[1512]---> Adder-cost: 842 maxlim: 53120 bits: 17/16 c ---[1511]---> Adder-cost: 7577 maxlim: 503679 bits: 20/19 c ---[1510]---> Adder-cost: 2143 maxlim: 148991 bits: 19/18 c ---[1509]---> Adder-cost: 10766 maxlim: 799871 bits: 20/20 c ---[1508]---> Adder-cost: 4653 maxlim: 211839 bits: 19/18 c ---[1503]---> Adder-cost: 31320 maxlim: 3785983 bits: 23/22 c ---[1501]---> Adder-cost: 17437 maxlim: 3013503 bits: 23/22 c ---[1500]---> Adder-cost: 6183 maxlim: 1485695 bits: 22/21 c ---[1496]---> Adder-cost: 38 maxlim: 4736 bits: 14/13 c ---[1494]---> Adder-cost: 70 maxlim: 4352 bits: 14/13 c ---[1492]---> Sorter-cost: 691 Base: 2 2 2 2 2 2 2 7 c ---[1490]---> Sorter-cost: 517 Base: 2 2 2 2 2 2 2 7 c ---[1488]---> Sorter-cost: 878 Base: 2 2 2 2 2 2 2 7 c ---[1486]---> Sorter-cost: 722 Base: 2 2 2 2 2 2 2 7 c ---[1484]---> Sorter-cost: 924 Base: 2 2 2 2 2 2 2 7 c ---[1482]---> Sorter-cost: 966 Base: 2 2 2 2 2 2 2 7 c ---[1480]---> Sorter-cost: 731 Base: 2 2 2 2 2 2 2 7 c ---[1478]---> Sorter-cost: 337 Base: 2 2 2 2 2 2 2 7 c ---[1476]---> Sorter-cost: 654 Base: 2 2 2 2 2 2 2 7 c ---[1474]---> Sorter-cost: 777 Base: 2 2 2 2 2 2 2 7 c ---[1472]---> Sorter-cost: 778 Base: 2 2 2 2 2 2 2 7 c ---[1470]---> Sorter-cost: 954 Base: 2 2 2 2 2 2 2 7 c ---[1468]---> Sorter-cost: 776 Base: 2 2 2 2 2 2 2 7 c ---[1466]---> Adder-cost: 72 maxlim: 4992 bits: 14/13 c ---[1464]---> Sorter-cost: 784 Base: 2 2 2 2 2 2 2 7 c ---[1462]---> Sorter-cost: 889 Base: 2 2 2 2 2 2 2 7 c ---[1460]---> Sorter-cost: 679 Base: 2 2 2 2 2 2 2 7 c ---[1458]---> Sorter-cost: 640 Base: 2 2 2 2 2 2 2 7 c ---[1456]---> Sorter-cost: 786 Base: 2 2 2 2 2 2 2 7 c ---[1454]---> Sorter-cost: 615 Base: 2 2 2 2 2 2 2 7 c ---[1452]---> Adder-cost: 80 maxlim: 5504 bits: 14/13 c ---[1450]---> Adder-cost: 108 maxlim: 7808 bits: 14/13 c ---[1448]---> Adder-cost: 94 maxlim: 6400 bits: 14/13 c ---[1446]---> Sorter-cost: 1216 Base: 2 2 2 2 2 2 2 7 c ---[1444]---> Sorter-cost: 788 Base: 2 2 2 2 2 2 2 7 c ---[1442]---> Sorter-cost: 734 Base: 2 2 2 2 2 2 2 7 c ---[1440]---> Adder-cost: 82 maxlim: 5248 bits: 14/13 c ---[1438]---> Adder-cost: 40 maxlim: 5248 bits: 14/13 c ---[1436]---> Adder-cost: 66 maxlim: 4352 bits: 14/13 c ---[1434]---> Sorter-cost: 587 Base: 2 2 2 2 2 2 2 7 c ---[1432]---> Adder-cost: 40 maxlim: 4352 bits: 14/13 c ---[1430]---> Adder-cost: 94 maxlim: 6912 bits: 14/13 c ---[1428]---> Adder-cost: 80 maxlim: 4864 bits: 14/13 c ---[1426]---> Adder-cost: 184 maxlim: 12160 bits: 15/14 c ---[1424]---> Adder-cost: 110 maxlim: 6784 bits: 14/13 c ---[1422]---> Adder-cost: 96 maxlim: 6400 bits: 14/13 c ---[1420]---> Adder-cost: 82 maxlim: 4992 bits: 14/13 c ---[1418]---> Adder-cost: 70 maxlim: 5120 bits: 14/13 c ---[1416]---> Sorter-cost: 651 Base: 2 2 2 2 2 2 2 7 c ---[1414]---> Sorter-cost: 488 Base: 2 2 2 2 2 2 2 7 c ---[1412]---> Sorter-cost: 527 Base: 2 2 2 2 2 2 2 7 c ---[1410]---> Sorter-cost: 604 Base: 2 2 2 2 2 2 2 7 c ---[1408]---> Sorter-cost: 442 Base: 2 2 2 2 2 2 2 7 c ---[1406]---> Sorter-cost: 901 Base: 2 2 2 2 2 2 2 7 c ---[1404]---> Sorter-cost: 256 Base: 2 2 2 2 2 2 2 2 c ---[1402]---> Sorter-cost: 639 Base: 2 2 2 2 2 2 2 7 c ---[1400]---> Sorter-cost: 538 Base: 2 2 2 2 2 2 2 7 c ---[1398]---> Sorter-cost: 561 Base: 2 2 2 2 2 2 2 7 c ---[1396]---> Sorter-cost: 437 Base: 2 2 2 2 2 2 2 7 c ---[1394]---> Sorter-cost: 437 Base: 2 2 2 2 2 2 2 7 c ---[1392]---> Adder-cost: 120 maxlim: 7680 bits: 14/13 c ---[1390]---> Adder-cost: 86 maxlim: 5248 bits: 14/13 c ---[1388]---> Adder-cost: 78 maxlim: 4736 bits: 14/13 c ---[1386]---> Adder-cost: 98 maxlim: 6912 bits: 14/13 c ---[1384]---> Sorter-cost: 996 Base: 2 2 2 2 2 2 2 7 c ---[1382]---> Sorter-cost: 669 Base: 2 2 2 2 2 2 2 7 c ---[1380]---> Adder-cost: 110 maxlim: 7168 bits: 14/13 c ---[1378]---> Adder-cost: 96 maxlim: 6912 bits: 14/13 c ---[1376]---> Sorter-cost: 715 Base: 2 2 2 2 2 2 2 7 c ---[1374]---> Sorter-cost: 992 Base: 2 2 2 2 2 2 2 7 c ---[1372]---> Sorter-cost: 437 Base: 2 2 2 2 2 2 2 7 c ---[1370]---> Sorter-cost: 976 Base: 2 2 2 2 2 2 2 7 c ---[1368]---> Sorter-cost: 461 Base: 2 2 2 2 2 2 2 7 c ---[1366]---> Sorter-cost: 248 Base: 2 2 2 2 2 2 2 2 c ---[1364]---> Sorter-cost: 639 Base: 2 2 2 2 2 2 2 7 c ---[1362]---> Sorter-cost: 473 Base: 2 2 2 2 2 2 2 7 c ---[1360]---> Sorter-cost: 536 Base: 2 2 2 2 2 2 2 7 c ---[1358]---> Sorter-cost: 542 Base: 2 2 2 2 2 2 2 7 c ---[1356]---> Sorter-cost: 546 Base: 2 2 2 2 2 2 2 7 c ---[1354]---> Adder-cost: 88 maxlim: 6144 bits: 14/13 c ---[1352]---> Adder-cost: 90 maxlim: 6912 bits: 14/13 c ---[1350]---> Adder-cost: 106 maxlim: 6400 bits: 14/13 c ---[1348]---> Adder-cost: 96 maxlim: 7424 bits: 14/13 c ---[1346]---> Adder-cost: 104 maxlim: 7680 bits: 14/13 c ---[1344]---> Adder-cost: 164 maxlim: 12416 bits: 15/14 c ---[1342]---> Adder-cost: 140 maxlim: 10496 bits: 15/14 c ---[1340]---> Adder-cost: 118 maxlim: 8960 bits: 15/14 c ---[1338]---> Adder-cost: 114 maxlim: 7936 bits: 14/13 c ---[1336]---> Adder-cost: 129 maxlim: 8192 bits: 15/14 c ---[1334]---> Adder-cost: 40 maxlim: 6016 bits: 14/13 c ---[1332]---> Sorter-cost: 551 Base: 2 2 2 2 2 2 2 7 c ---[1330]---> Sorter-cost: 370 Base: 2 2 2 2 2 2 2 7 c ---[1328]---> Sorter-cost: 893 Base: 2 2 2 2 2 2 2 7 c ---[1326]---> Sorter-cost: 447 Base: 2 2 2 2 2 2 2 7 c ---[1324]---> Sorter-cost: 364 Base: 2 2 2 2 2 2 2 7 c ---[1322]---> Sorter-cost: 264 Base: 2 2 2 2 2 2 2 2 c ---[1320]---> Adder-cost: 84 maxlim: 5504 bits: 14/13 c ---[1318]---> Sorter-cost: 432 Base: 2 2 2 2 2 2 2 7 c ---[1316]---> Sorter-cost: 658 Base: 2 2 2 2 2 2 2 7 c ---[1314]---> Adder-cost: 118 maxlim: 7424 bits: 14/13 c ---[1312]---> Adder-cost: 90 maxlim: 5632 bits: 14/13 c ---[1310]---> Sorter-cost: 572 Base: 2 2 2 2 2 2 2 7 c ---[1308]---> Adder-cost: 88 maxlim: 5120 bits: 14/13 c ---[1306]---> Adder-cost: 72 maxlim: 6016 bits: 14/13 c ---[1304]---> Sorter-cost: 786 Base: 2 2 2 2 2 2 2 7 c ---[1302]---> Sorter-cost: 404 Base: 2 2 2 2 2 2 2 7 c ---[1300]---> Sorter-cost: 436 Base: 2 2 2 2 2 2 2 7 c ---[1298]---> Adder-cost: 90 maxlim: 5376 bits: 14/13 c ---[1296]---> Adder-cost: 87 maxlim: 5248 bits: 14/13 c ---[1294]---> Sorter-cost: 681 Base: 2 2 2 2 2 2 2 7 c ---[1292]---> Sorter-cost: 507 Base: 2 2 2 2 2 2 2 7 c ---[1290]---> Sorter-cost: 507 Base: 2 2 2 2 2 2 2 7 c ---[1288]---> Sorter-cost: 582 Base: 2 2 2 2 2 2 2 7 c ---[1286]---> Adder-cost: 124 maxlim: 8064 bits: 14/13 c ---[1284]---> Sorter-cost: 658 Base: 2 2 2 2 2 2 2 7 c ---[1282]---> Sorter-cost: 312 Base: 2 2 2 2 2 2 2 2 c ---[1280]---> Adder-cost: 76 maxlim: 4480 bits: 14/13 c ---[1278]---> Adder-cost: 166 maxlim: 11136 bits: 15/14 c ---[1276]---> Adder-cost: 100 maxlim: 6912 bits: 14/13 c ---[1274]---> Adder-cost: 108 maxlim: 6656 bits: 14/13 c ---[1272]---> Adder-cost: 80 maxlim: 6272 bits: 14/13 c ---[1270]---> Adder-cost: 132 maxlim: 8832 bits: 15/14 c ---[1268]---> Adder-cost: 112 maxlim: 8960 bits: 15/14 c ---[1266]---> Sorter-cost: 558 Base: 2 2 2 2 2 2 2 7 c ---[1264]---> Adder-cost: 80 maxlim: 5248 bits: 14/13 c ---[1262]---> Sorter-cost: 717 Base: 2 2 2 2 2 2 2 7 c ---[1260]---> Sorter-cost: 736 Base: 2 2 2 2 2 2 2 7 c ---[1258]---> Sorter-cost: 596 Base: 2 2 2 2 2 2 2 7 c ---[1256]---> Sorter-cost: 786 Base: 2 2 2 2 2 2 2 7 c ---[1254]---> Sorter-cost: 784 Base: 2 2 2 2 2 2 2 7 c ---[1252]---> Sorter-cost: 1028 Base: 2 2 2 2 2 2 2 7 c ---[1250]---> Adder-cost: 82 maxlim: 4864 bits: 14/13 c ---[1248]---> Sorter-cost: 691 Base: 2 2 2 2 2 2 2 7 c ---[1246]---> Adder-cost: 70 maxlim: 4480 bits: 14/13 c ---[1244]---> Sorter-cost: 568 Base: 2 2 2 2 2 2 2 7 c ---[1242]---> Sorter-cost: 996 Base: 2 2 2 2 2 2 2 7 c ---[1240]---> Adder-cost: 112 maxlim: 7168 bits: 14/13 c ---[1238]---> Adder-cost: 102 maxlim: 7424 bits: 14/13 c ---[1236]---> Adder-cost: 116 maxlim: 8064 bits: 14/13 c ---[1234]---> Adder-cost: 166 maxlim: 11648 bits: 15/14 c ---[1232]---> Sorter-cost: 312 Base: 2 2 2 2 2 2 2 2 c ---[1230]---> Sorter-cost: 160 Base: 2 2 2 2 2 2 2 2 c ---[1228]---> Sorter-cost: 418 Base: 2 2 2 2 2 2 2 7 c ---[1226]---> Adder-cost: 100 maxlim: 6784 bits: 14/13 c ---[1224]---> Adder-cost: 46 maxlim: 6784 bits: 14/13 c ---[1222]---> Adder-cost: 78 maxlim: 7040 bits: 14/13 c ---[1220]---> Sorter-cost: 467 Base: 2 2 2 2 2 2 2 7 c ---[1218]---> Sorter-cost: 623 Base: 2 2 2 2 2 2 2 7 c ---[1216]---> Adder-cost: 90 maxlim: 5504 bits: 14/13 c ---[1214]---> Adder-cost: 64 maxlim: 4736 bits: 14/13 c ---[1212]---> Adder-cost: 66 maxlim: 4480 bits: 14/13 c ---[1210]---> Sorter-cost: 594 Base: 2 2 2 2 2 2 2 7 c ---[1208]---> Sorter-cost: 576 Base: 2 2 2 2 2 2 2 7 c ---[1206]---> Sorter-cost: 440 Base: 2 2 2 2 2 2 2 7 c ---[1204]---> Sorter-cost: 623 Base: 2 2 2 2 2 2 2 7 c ---[1202]---> Adder-cost: 130 maxlim: 8576 bits: 15/14 c ---[1200]---> Adder-cost: 98 maxlim: 6400 bits: 14/13 c ---[1198]---> Sorter-cost: 639 Base: 2 2 2 2 2 2 2 7 c ---[1196]---> Sorter-cost: 462 Base: 2 2 2 2 2 2 2 7 c ---[1194]---> Sorter-cost: 717 Base: 2 2 2 2 2 2 2 7 c ---[1192]---> Sorter-cost: 220 Base: 2 2 2 2 2 2 2 2 c ---[1190]---> Sorter-cost: 218 Base: 2 2 2 2 2 2 2 2 c ---[1188]---> Sorter-cost: 554 Base: 2 2 2 2 2 2 2 7 c ---[1186]---> Sorter-cost: 438 Base: 2 2 2 2 2 2 2 7 c ---[1184]---> Sorter-cost: 382 Base: 2 2 2 2 2 2 2 7 c ---[1182]---> Adder-cost: 104 maxlim: 6272 bits: 14/13 c ---[1180]---> Adder-cost: 94 maxlim: 6528 bits: 14/13 c ---[1178]---> Adder-cost: 116 maxlim: 7296 bits: 14/13 c ---[1176]---> Adder-cost: 100 maxlim: 7296 bits: 14/13 c ---[1174]---> Adder-cost: 82 maxlim: 5376 bits: 14/13 c ---[1172]---> Adder-cost: 74 maxlim: 5504 bits: 14/13 c ---[1170]---> Sorter-cost: 612 Base: 2 2 2 2 2 2 2 7 c ---[1168]---> Sorter-cost: 300 Base: 2 2 2 2 2 2 2 2 c ---[1166]---> Adder-cost: 102 maxlim: 6400 bits: 14/13 c ---[1164]---> Sorter-cost: 691 Base: 2 2 2 2 2 2 2 7 c ---[1162]---> Sorter-cost: 381 Base: 2 2 2 2 2 2 2 7 c ---[1160]---> Sorter-cost: 406 Base: 2 2 2 2 2 2 2 7 c ---[1158]---> Sorter-cost: 681 Base: 2 2 2 2 2 2 2 7 c ---[1156]---> Sorter-cost: 507 Base: 2 2 2 2 2 2 2 7 c ---[1154]---> Sorter-cost: 499 Base: 2 2 2 2 2 2 2 7 c ---[1152]---> Adder-cost: 84 maxlim: 5760 bits: 14/13 c ---[1150]---> Adder-cost: 42 maxlim: 5760 bits: 14/13 c ---[1148]---> Sorter-cost: 572 Base: 2 2 2 2 2 2 2 7 c ---[1146]---> Adder-cost: 42 maxlim: 5760 bits: 14/13 c ---[1144]---> Sorter-cost: 308 Base: 2 2 2 2 2 2 2 2 c ---[1142]---> Adder-cost: 84 maxlim: 5248 bits: 14/13 c ---[1140]---> Adder-cost: 72 maxlim: 5120 bits: 14/13 c ---[1138]---> Adder-cost: 108 maxlim: 6656 bits: 14/13 c ---[1136]---> Adder-cost: 48 maxlim: 6656 bits: 14/13 c ---[1134]---> Adder-cost: 68 maxlim: 6784 bits: 14/13 c ---[1132]---> Adder-cost: 66 maxlim: 4352 bits: 14/13 c ---[1130]---> Adder-cost: 72 maxlim: 5632 bits: 14/13 c ---[1128]---> Sorter-cost: 445 Base: 2 2 2 2 2 2 2 7 c ---[1126]---> Adder-cost: 40 maxlim: 4352 bits: 14/13 c ---[1124]---> Adder-cost: 40 maxlim: 4352 bits: 14/13 c ---[1122]---> Adder-cost: 78 maxlim: 4992 bits: 14/13 c ---[1120]---> Adder-cost: 40 maxlim: 4992 bits: 14/13 c ---[1118]---> Adder-cost: 92 maxlim: 6400 bits: 14/13 c ---[1116]---> Adder-cost: 110 maxlim: 7424 bits: 14/13 c ---[1114]---> Adder-cost: 50 maxlim: 7424 bits: 14/13 c ---[1112]---> Adder-cost: 80 maxlim: 7680 bits: 14/13 c ---[1110]---> Adder-cost: 110 maxlim: 7424 bits: 14/13 c ---[1108]---> Adder-cost: 50 maxlim: 7424 bits: 14/13 c ---[1106]---> Sorter-cost: 431 Base: 2 2 2 2 2 2 2 7 c ---[1104]---> Sorter-cost: 616 Base: 2 2 2 2 2 2 2 7 c ---[1102]---> Sorter-cost: 430 Base: 2 2 2 2 2 2 2 7 c ---[1100]---> Sorter-cost: 611 Base: 2 2 2 2 2 2 2 7 c ---[1098]---> Sorter-cost: 653 Base: 2 2 2 2 2 2 2 7 c ---[1096]---> Adder-cost: 118 maxlim: 7936 bits: 14/13 c ---[1094]---> Adder-cost: 120 maxlim: 8960 bits: 15/14 c ---[1092]---> Adder-cost: 112 maxlim: 8576 bits: 15/14 c ---[1090]---> Adder-cost: 118 maxlim: 8448 bits: 15/14 c ---[1088]---> Sorter-cost: 713 Base: 2 2 2 2 2 2 2 7 c ---[1086]---> Sorter-cost: 618 Base: 2 2 2 2 2 2 2 7 c ---[1084]---> Sorter-cost: 617 Base: 2 2 2 2 2 2 2 7 c ---[1082]---> Sorter-cost: 970 Base: 2 2 2 2 2 2 2 7 c ---[1080]---> Sorter-cost: 419 Base: 2 2 2 2 2 2 2 7 c ---[1078]---> Sorter-cost: 392 Base: 2 2 2 2 2 2 2 7 c ---[1076]---> Sorter-cost: 468 Base: 2 2 2 2 2 2 2 7 c ---[1074]---> Sorter-cost: 372 Base: 2 2 2 2 2 2 2 7 c ---[1072]---> Sorter-cost: 254 Base: 2 2 2 2 2 2 2 2 c ---[1070]---> Adder-cost: 196 maxlim: 14592 bits: 15/14 c ---[1068]---> Adder-cost: 86 maxlim: 5376 bits: 14/13 c ---[1066]---> Adder-cost: 72 maxlim: 4864 bits: 14/13 c ---[1064]---> Adder-cost: 94 maxlim: 5760 bits: 14/13 c ---[1062]---> Adder-cost: 82 maxlim: 5248 bits: 14/13 c ---[1060]---> Sorter-cost: 408 Base: 2 2 2 2 2 2 2 7 c ---[1058]---> Sorter-cost: 246 Base: 2 2 2 2 2 2 2 7 c ---[1056]---> Sorter-cost: 262 Base: 2 2 2 2 2 2 2 2 c ---[1054]---> Sorter-cost: 639 Base: 2 2 2 2 2 2 2 7 c ---[1052]---> Adder-cost: 80 maxlim: 5632 bits: 14/13 c ---[1050]---> Sorter-cost: 568 Base: 2 2 2 2 2 2 2 7 c ---[1048]---> Sorter-cost: 621 Base: 2 2 2 2 2 2 2 7 c ---[1046]---> Sorter-cost: 585 Base: 2 2 2 2 2 2 2 7 c ---[1044]---> Sorter-cost: 415 Base: 2 2 2 2 2 2 2 7 c ---[1042]---> Sorter-cost: 687 Base: 2 2 2 2 2 2 2 7 c ---[1040]---> Adder-cost: 82 maxlim: 6016 bits: 14/13 c ---[1038]---> Sorter-cost: 616 Base: 2 2 2 2 2 2 2 7 c ---[1036]---> Sorter-cost: 585 Base: 2 2 2 2 2 2 2 7 c ---[1034]---> Sorter-cost: 447 Base: 2 2 2 2 2 2 2 7 c ---[1032]---> Sorter-cost: 360 Base: 2 2 2 2 2 2 2 7 c ---[1030]---> Sorter-cost: 246 Base: 2 2 2 2 2 2 2 7 c ---[1028]---> Sorter-cost: 928 Base: 2 2 2 2 2 2 2 7 c ---[1026]---> Sorter-cost: 391 Base: 2 2 2 2 2 2 2 7 c ---[1024]---> Sorter-cost: 584 Base: 2 2 2 2 2 2 2 7 c ---[1022]---> Sorter-cost: 268 Base: 2 2 2 2 2 2 2 2 c ---[1020]---> Sorter-cost: 264 Base: 2 2 2 2 2 2 2 2 c ---[1018]---> Sorter-cost: 575 Base: 2 2 2 2 2 2 2 7 c ---[1016]---> Sorter-cost: 679 Base: 2 2 2 2 2 2 2 7 c ---[1014]---> Sorter-cost: 437 Base: 2 2 2 2 2 2 2 7 c ---[1012]---> Sorter-cost: 555 Base: 2 2 2 2 2 2 2 7 c ---[1010]---> Adder-cost: 94 maxlim: 5632 bits: 14/13 c ---[1008]---> Adder-cost: 84 maxlim: 5760 bits: 14/13 c ---[1006]---> Adder-cost: 94 maxlim: 6784 bits: 14/13 c ---[1004]---> Sorter-cost: 722 Base: 2 2 2 2 2 2 2 7 c ---[1002]---> Adder-cost: 104 maxlim: 7168 bits: 14/13 c ---[1000]---> Adder-cost: 90 maxlim: 7040 bits: 14/13 c ---[ 998]---> Adder-cost: 100 maxlim: 6272 bits: 14/13 c ---[ 996]---> Adder-cost: 76 maxlim: 6656 bits: 14/13 c ---[ 994]---> Sorter-cost: 408 Base: 2 2 2 2 2 2 2 7 c ---[ 992]---> Adder-cost: 144 maxlim: 9088 bits: 15/14 c ---[ 990]---> Sorter-cost: 276 Base: 2 2 2 2 2 2 2 2 c ---[ 988]---> Sorter-cost: 218 Base: 2 2 2 2 2 2 2 2 c ---[ 986]---> Sorter-cost: 643 Base: 2 2 2 2 2 2 2 7 c ---[ 984]---> Sorter-cost: 661 Base: 2 2 2 2 2 2 2 7 c ---[ 982]---> Adder-cost: 88 maxlim: 5120 bits: 14/13 c ---[ 980]---> Adder-cost: 80 maxlim: 5760 bits: 14/13 c ---[ 978]---> Adder-cost: 56 maxlim: 9088 bits: 15/14 c ---[ 976]---> Sorter-cost: 994 Base: 2 2 2 2 2 2 2 7 c ---[ 974]---> Sorter-cost: 830 Base: 2 2 2 2 2 2 2 7 c ---[ 972]---> Adder-cost: 88 maxlim: 7040 bits: 14/13 c ---[ 970]---> Adder-cost: 92 maxlim: 6912 bits: 14/13 c ---[ 968]---> Adder-cost: 56 maxlim: 9088 bits: 15/14 c ---[ 966]---> Adder-cost: 74 maxlim: 7168 bits: 14/13 c ---[ 964]---> Adder-cost: 74 maxlim: 5504 bits: 14/13 c ---[ 962]---> Adder-cost: 92 maxlim: 6144 bits: 14/13 c ---[ 960]---> Adder-cost: 74 maxlim: 4736 bits: 14/13 c ---[ 958]---> Sorter-cost: 786 Base: 2 2 2 2 2 2 2 7 c ---[ 956]---> Adder-cost: 114 maxlim: 9216 bits: 15/14 c ---[ 954]---> Sorter-cost: 656 Base: 2 2 2 2 2 2 2 7 c ---[ 952]---> Sorter-cost: 528 Base: 2 2 2 2 2 2 2 7 c ---[ 950]---> Adder-cost: 84 maxlim: 5376 bits: 14/13 c ---[ 948]---> Adder-cost: 72 maxlim: 5632 bits: 14/13 c ---[ 946]---> Adder-cost: 72 maxlim: 4864 bits: 14/13 c ---[ 944]---> Adder-cost: 80 maxlim: 5504 bits: 14/13 c ---[ 942]---> Adder-cost: 62 maxlim: 5248 bits: 14/13 c ---[ 940]---> Adder-cost: 66 maxlim: 5504 bits: 14/13 c ---[ 938]---> Sorter-cost: 467 Base: 2 2 2 2 2 2 2 7 c ---[ 936]---> Sorter-cost: 604 Base: 2 2 2 2 2 2 2 7 c ---[ 934]---> Sorter-cost: 425 Base: 2 2 2 2 2 2 2 7 c ---[ 932]---> Sorter-cost: 907 Base: 2 2 2 2 2 2 2 7 c ---[ 930]---> Sorter-cost: 264 Base: 2 2 2 2 2 2 2 2 c ---[ 928]---> Sorter-cost: 274 Base: 2 2 2 2 2 2 2 2 c ---[ 926]---> Adder-cost: 108 maxlim: 6656 bits: 14/13 c ---[ 924]---> Adder-cost: 48 maxlim: 6656 bits: 14/13 c ---[ 922]---> Adder-cost: 82 maxlim: 6272 bits: 14/13 c ---[ 920]---> Sorter-cost: 770 Base: 2 2 2 2 2 2 2 7 c ---[ 918]---> Sorter-cost: 575 Base: 2 2 2 2 2 2 2 7 c ---[ 916]---> Sorter-cost: 713 Base: 2 2 2 2 2 2 2 7 c ---[ 914]---> Sorter-cost: 666 Base: 2 2 2 2 2 2 2 7 c ---[ 912]---> Sorter-cost: 891 Base: 2 2 2 2 2 2 2 7 c ---[ 910]---> Adder-cost: 82 maxlim: 5376 bits: 14/13 c ---[ 908]---> Sorter-cost: 936 Base: 2 2 2 2 2 2 2 7 c ---[ 906]---> Adder-cost: 60 maxlim: 5248 bits: 14/13 c ---[ 904]---> Adder-cost: 56 maxlim: 5504 bits: 14/13 c ---[ 902]---> Adder-cost: 62 maxlim: 5120 bits: 14/13 c ---[ 900]---> Adder-cost: 44 maxlim: 4736 bits: 14/13 c ---[ 898]---> Sorter-cost: 440 Base: 2 2 2 2 2 2 2 7 c ---[ 896]---> Adder-cost: 104 maxlim: 6528 bits: 14/13 c ---[ 894]---> Sorter-cost: 438 Base: 2 2 2 2 2 2 2 7 c ---[ 892]---> Sorter-cost: 447 Base: 2 2 2 2 2 2 2 7 c ---[ 890]---> Sorter-cost: 428 Base: 2 2 2 2 2 2 2 7 c ---[ 888]---> Sorter-cost: 589 Base: 2 2 2 2 2 2 2 7 c ---[ 886]---> Adder-cost: 72 maxlim: 5888 bits: 14/13 c ---[ 884]---> Adder-cost: 132 maxlim: 8832 bits: 15/14 c ---[ 882]---> Adder-cost: 60 maxlim: 8832 bits: 15/14 c ---[ 880]---> Adder-cost: 122 maxlim: 7808 bits: 14/13 c ---[ 878]---> Adder-cost: 102 maxlim: 6272 bits: 14/13 c ---[ 876]---> Adder-cost: 90 maxlim: 6784 bits: 14/13 c ---[ 874]---> Adder-cost: 46 maxlim: 6784 bits: 14/13 c ---[ 872]---> Adder-cost: 46 maxlim: 6784 bits: 14/13 c ---[ 870]---> Adder-cost: 158 maxlim: 10496 bits: 15/14 c ---[ 868]---> Adder-cost: 118 maxlim: 9856 bits: 15/14 c ---[ 866]---> Adder-cost: 60 maxlim: 5888 bits: 14/13 c ---[ 864]---> Sorter-cost: 658 Base: 2 2 2 2 2 2 2 7 c ---[ 862]---> Sorter-cost: 461 Base: 2 2 2 2 2 2 2 7 c ---[ 860]---> Sorter-cost: 218 Base: 2 2 2 2 2 2 2 2 c ---[ 858]---> Sorter-cost: 589 Base: 2 2 2 2 2 2 2 7 c ---[ 856]---> Adder-cost: 80 maxlim: 4992 bits: 14/13 c ---[ 854]---> Adder-cost: 78 maxlim: 5504 bits: 14/13 c ---[ 852]---> Adder-cost: 98 maxlim: 7040 bits: 14/13 c ---[ 850]---> Adder-cost: 90 maxlim: 6144 bits: 14/13 c ---[ 848]---> Adder-cost: 82 maxlim: 5632 bits: 14/13 c ---[ 846]---> Adder-cost: 62 maxlim: 5760 bits: 14/13 c ---[ 844]---> Adder-cost: 80 maxlim: 5248 bits: 14/13 c ---[ 842]---> Sorter-cost: 637 Base: 2 2 2 2 2 2 2 7 c ---[ 840]---> Adder-cost: 44 maxlim: 5760 bits: 14/13 c ---[ 838]---> Adder-cost: 68 maxlim: 6016 bits: 14/13 c ---[ 836]---> Sorter-cost: 990 Base: 2 2 2 2 2 2 2 7 c ---[ 834]---> Adder-cost: 90 maxlim: 5888 bits: 14/13 c ---[ 832]---> Sorter-cost: 565 Base: 2 2 2 2 2 2 2 7 c ---[ 830]---> Sorter-cost: 691 Base: 2 2 2 2 2 2 2 7 c ---[ 828]---> Sorter-cost: 1044 Base: 2 2 2 2 2 2 2 7 c ---[ 826]---> Adder-cost: 94 maxlim: 6272 bits: 14/13 c ---[ 824]---> Sorter-cost: 578 Base: 2 2 2 2 2 2 2 7 c ---[ 822]---> Sorter-cost: 366 Base: 2 2 2 2 2 2 2 7 c ---[ 820]---> Sorter-cost: 372 Base: 2 2 2 2 2 2 2 7 c ---[ 818]---> Sorter-cost: 226 Base: 2 2 2 2 2 2 2 2 c ---[ 816]---> Sorter-cost: 426 Base: 2 2 2 2 2 2 2 7 c ---[ 814]---> Sorter-cost: 646 Base: 2 2 2 2 2 2 2 7 c ---[ 812]---> Adder-cost: 118 maxlim: 7808 bits: 14/13 c ---[ 810]---> Adder-cost: 98 maxlim: 7808 bits: 14/13 c ---[ 808]---> Adder-cost: 134 maxlim: 9856 bits: 15/14 c ---[ 806]---> Sorter-cost: 616 Base: 2 2 2 2 2 2 2 7 c ---[ 804]---> Sorter-cost: 903 Base: 2 2 2 2 2 2 2 7 c ---[ 802]---> Sorter-cost: 419 Base: 2 2 2 2 2 2 2 7 c ---[ 800]---> Sorter-cost: 440 Base: 2 2 2 2 2 2 2 7 c ---[ 798]---> Adder-cost: 76 maxlim: 4480 bits: 14/13 c ---[ 796]---> Adder-cost: 40 maxlim: 4480 bits: 14/13 c ---[ 794]---> Adder-cost: 72 maxlim: 4864 bits: 14/13 c ---[ 792]---> Adder-cost: 104 maxlim: 6144 bits: 14/13 c ---[ 790]---> Adder-cost: 86 maxlim: 6144 bits: 14/13 c ---[ 788]---> Adder-cost: 70 maxlim: 5504 bits: 14/13 c ---[ 786]---> Adder-cost: 74 maxlim: 5760 bits: 14/13 c ---[ 784]---> Sorter-cost: 979 Base: 2 2 2 2 2 2 2 7 c ---[ 782]---> Sorter-cost: 447 Base: 2 2 2 2 2 2 2 7 c ---[ 780]---> Sorter-cost: 556 Base: 2 2 2 2 2 2 2 7 c ---[ 778]---> Sorter-cost: 396 Base: 2 2 2 2 2 2 2 7 c ---[ 776]---> Sorter-cost: 264 Base: 2 2 2 2 2 2 2 2 c ---[ 774]---> Sorter-cost: 268 Base: 2 2 2 2 2 2 2 2 c ---[ 772]---> Sorter-cost: 382 Base: 2 2 2 2 2 2 2 7 c ---[ 770]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 7 c ---[ 768]---> Adder-cost: 144 maxlim: 11008 bits: 15/14 c ---[ 766]---> Adder-cost: 68 maxlim: 11008 bits: 15/14 c ---[ 764]---> Sorter-cost: 1022 Base: 2 2 2 2 2 2 2 7 c ---[ 762]---> Adder-cost: 84 maxlim: 5376 bits: 14/13 c ---[ 760]---> Adder-cost: 84 maxlim: 5376 bits: 14/13 c ---[ 758]---> Adder-cost: 102 maxlim: 6272 bits: 14/13 c ---[ 756]---> Adder-cost: 98 maxlim: 6400 bits: 14/13 c ---[ 754]---> Adder-cost: 176 maxlim: 12288 bits: 15/14 c ---[ 752]---> Adder-cost: 186 maxlim: 13952 bits: 15/14 c ---[ 750]---> Adder-cost: 80 maxlim: 5120 bits: 14/13 c ---[ 748]---> Adder-cost: 70 maxlim: 5120 bits: 14/13 c ---[ 746]---> Adder-cost: 66 maxlim: 4480 bits: 14/13 c ---[ 744]---> Sorter-cost: 616 Base: 2 2 2 2 2 2 2 7 c ---[ 742]---> Sorter-cost: 856 Base: 2 2 2 2 2 2 2 7 c ---[ 740]---> Sorter-cost: 266 Base: 2 2 2 2 2 2 2 2 c ---[ 738]---> Sorter-cost: 274 Base: 2 2 2 2 2 2 2 2 c ---[ 736]---> Sorter-cost: 675 Base: 2 2 2 2 2 2 2 7 c ---[ 734]---> Adder-cost: 92 maxlim: 5632 bits: 14/13 c ---[ 732]---> Adder-cost: 74 maxlim: 4992 bits: 14/13 c ---[ 730]---> Sorter-cost: 996 Base: 2 2 2 2 2 2 2 7 c ---[ 728]---> Sorter-cost: 1080 Base: 2 2 2 2 2 2 2 7 c ---[ 726]---> Adder-cost: 122 maxlim: 7808 bits: 14/13 c ---[ 724]---> Adder-cost: 94 maxlim: 8192 bits: 15/14 c ---[ 722]---> Adder-cost: 74 maxlim: 7168 bits: 14/13 c ---[ 720]---> Sorter-cost: 717 Base: 2 2 2 2 2 2 2 7 c ---[ 718]---> Adder-cost: 52 maxlim: 7168 bits: 14/13 c ---[ 716]---> Sorter-cost: 268 Base: 2 2 2 2 2 2 2 2 c ---[ 714]---> Sorter-cost: 442 Base: 2 2 2 2 2 2 2 7 c ---[ 712]---> Sorter-cost: 685 Base: 2 2 2 2 2 2 2 7 c ---[ 710]---> Adder-cost: 146 maxlim: 9344 bits: 15/14 c ---[ 708]---> Adder-cost: 60 maxlim: 9344 bits: 15/14 c ---[ 706]---> Sorter-cost: 658 Base: 2 2 2 2 2 2 2 7 c ---[ 704]---> Sorter-cost: 608 Base: 2 2 2 2 2 2 2 7 c ---[ 702]---> Sorter-cost: 615 Base: 2 2 2 2 2 2 2 7 c ---[ 700]---> Sorter-cost: 651 Base: 2 2 2 2 2 2 2 7 c ---[ 698]---> Sorter-cost: 439 Base: 2 2 2 2 2 2 2 7 c ---[ 696]---> Adder-cost: 80 maxlim: 5248 bits: 14/13 c ---[ 694]---> Adder-cost: 84 maxlim: 5888 bits: 14/13 c ---[ 692]---> Adder-cost: 84 maxlim: 6144 bits: 14/13 c ---[ 690]---> Adder-cost: 72 maxlim: 6528 bits: 14/13 c ---[ 688]---> Sorter-cost: 594 Base: 2 2 2 2 2 2 2 7 c ---[ 686]---> Sorter-cost: 575 Base: 2 2 2 2 2 2 2 7 c ---[ 684]---> Sorter-cost: 371 Base: 2 2 2 2 2 2 2 7 c ---[ 682]---> Sorter-cost: 314 Base: 2 2 2 2 2 2 2 2 c ---[ 680]---> Sorter-cost: 684 Base: 2 2 2 2 2 2 2 7 c ---[ 678]---> Sorter-cost: 447 Base: 2 2 2 2 2 2 2 7 c ---[ 676]---> Sorter-cost: 608 Base: 2 2 2 2 2 2 2 7 c ---[ 674]---> Sorter-cost: 614 Base: 2 2 2 2 2 2 2 7 c ---[ 672]---> Adder-cost: 82 maxlim: 4992 bits: 14/13 c ---[ 670]---> Adder-cost: 88 maxlim: 5888 bits: 14/13 c ---[ 668]---> Adder-cost: 98 maxlim: 7040 bits: 14/13 c ---[ 666]---> Adder-cost: 88 maxlim: 5376 bits: 14/13 c ---[ 664]---> Sorter-cost: 566 Base: 2 2 2 2 2 2 2 7 c ---[ 662]---> Adder-cost: 88 maxlim: 5632 bits: 14/13 c ---[ 660]---> Adder-cost: 74 maxlim: 5760 bits: 14/13 c ---[ 658]---> Adder-cost: 62 maxlim: 6016 bits: 14/13 c ---[ 656]---> Sorter-cost: 594 Base: 2 2 2 2 2 2 2 7 c ---[ 654]---> Sorter-cost: 413 Base: 2 2 2 2 2 2 2 7 c ---[ 652]---> Sorter-cost: 302 Base: 2 2 2 2 2 2 2 2 c ---[ 650]---> Sorter-cost: 616 Base: 2 2 2 2 2 2 2 7 c ---[ 648]---> Sorter-cost: 426 Base: 2 2 2 2 2 2 2 7 c ---[ 646]---> Sorter-cost: 306 Base: 2 2 2 2 2 2 2 7 c ---[ 644]---> Adder-cost: 70 maxlim: 4864 bits: 14/13 c ---[ 642]---> Sorter-cost: 389 Base: 2 2 2 2 2 2 2 7 c ---[ 640]---> Sorter-cost: 293 Base: 2 2 2 2 2 2 2 7 c ---[ 638]---> Sorter-cost: 705 Base: 2 2 2 2 2 2 2 7 c ---[ 636]---> Sorter-cost: 849 Base: 2 2 2 2 2 2 2 7 c ---[ 634]---> Adder-cost: 74 maxlim: 4352 bits: 14/13 c ---[ 632]---> Adder-cost: 86 maxlim: 6016 bits: 14/13 c ---[ 630]---> Adder-cost: 82 maxlim: 4992 bits: 14/13 c ---[ 628]---> Adder-cost: 288 maxlim: 18816 bits: 16/15 c ---[ 626]---> Adder-cost: 104 maxlim: 6400 bits: 14/13 c ---[ 624]---> Adder-cost: 106 maxlim: 6656 bits: 14/13 c ---[ 622]---> Adder-cost: 98 maxlim: 6400 bits: 14/13 c ---[ 620]---> Sorter-cost: 612 Base: 2 2 2 2 2 2 2 7 c ---[ 618]---> Adder-cost: 78 maxlim: 6016 bits: 14/13 c ---[ 616]---> Adder-cost: 124 maxlim: 8960 bits: 15/14 c ---[ 614]---> Adder-cost: 142 maxlim: 10112 bits: 15/14 c ---[ 612]---> Adder-cost: 128 maxlim: 8448 bits: 15/14 c ---[ 610]---> Sorter-cost: 932 Base: 2 2 2 2 2 2 2 7 c ---[ 608]---> Adder-cost: 100 maxlim: 6272 bits: 14/13 c ---[ 606]---> Adder-cost: 112 maxlim: 7296 bits: 14/13 c ---[ 604]---> Sorter-cost: 637 Base: 2 2 2 2 2 2 2 7 c ---[ 602]---> Sorter-cost: 400 Base: 2 2 2 2 2 2 2 7 c ---[ 600]---> Sorter-cost: 614 Base: 2 2 2 2 2 2 2 7 c ---[ 598]---> Sorter-cost: 457 Base: 2 2 2 2 2 2 2 7 c ---[ 596]---> Sorter-cost: 595 Base: 2 2 2 2 2 2 2 7 c ---[ 594]---> Sorter-cost: 638 Base: 2 2 2 2 2 2 2 7 c ---[ 592]---> Sorter-cost: 358 Base: 2 2 2 2 2 2 2 7 c ---[ 590]---> Sorter-cost: 306 Base: 2 2 2 2 2 2 2 2 c ---[ 588]---> Sorter-cost: 402 Base: 2 2 2 2 2 2 2 7 c ---[ 586]---> Sorter-cost: 312 Base: 2 2 2 2 2 2 2 2 c ---[ 584]---> Sorter-cost: 226 Base: 2 2 2 2 2 2 2 2 c ---[ 582]---> Sorter-cost: 950 Base: 2 2 2 2 2 2 2 7 c ---[ 580]---> Sorter-cost: 928 Base: 2 2 2 2 2 2 2 7 c ---[ 578]---> Sorter-cost: 442 Base: 2 2 2 2 2 2 2 7 c ---[ 576]---> Adder-cost: 90 maxlim: 5888 bits: 14/13 c ---[ 574]---> Sorter-cost: 306 Base: 2 2 2 2 2 2 2 7 c ---[ 572]---> Sorter-cost: 407 Base: 2 2 2 2 2 2 2 7 c ---[ 570]---> Sorter-cost: 304 Base: 2 2 2 2 2 2 2 2 c ---[ 568]---> Adder-cost: 138 maxlim: 8704 bits: 15/14 c ---[ 566]---> Adder-cost: 100 maxlim: 7808 bits: 14/13 c ---[ 564]---> Adder-cost: 90 maxlim: 7552 bits: 14/13 c ---[ 562]---> Adder-cost: 100 maxlim: 7808 bits: 14/13 c ---[ 560]---> Adder-cost: 102 maxlim: 6400 bits: 14/13 c ---[ 558]---> Adder-cost: 90 maxlim: 6400 bits: 14/13 c ---[ 556]---> Adder-cost: 82 maxlim: 5632 bits: 14/13 c ---[ 554]---> Adder-cost: 60 maxlim: 4864 bits: 14/13 c ---[ 552]---> Adder-cost: 72 maxlim: 8064 bits: 14/13 c ---[ 550]---> Adder-cost: 88 maxlim: 8448 bits: 15/14 c ---[ 548]---> Adder-cost: 88 maxlim: 7168 bits: 14/13 c ---[ 546]---> Adder-cost: 64 maxlim: 7168 bits: 14/13 c ---[ 544]---> Sorter-cost: 266 Base: 2 2 2 2 2 2 2 2 c ---[ 542]---> Sorter-cost: 404 Base: 2 2 2 2 2 2 2 7 c ---[ 540]---> Sorter-cost: 434 Base: 2 2 2 2 2 2 2 7 c ---[ 538]---> Sorter-cost: 404 Base: 2 2 2 2 2 2 2 7 c ---[ 536]---> Sorter-cost: 366 Base: 2 2 2 2 2 2 2 7 c ---[ 534]---> Sorter-cost: 264 Base: 2 2 2 2 2 2 2 2 c ---[ 532]---> Adder-cost: 52 maxlim: 4736 bits: 14/13 c ---[ 530]---> Adder-cost: 146 maxlim: 11008 bits: 15/14 c ---[ 528]---> Adder-cost: 68 maxlim: 11008 bits: 15/14 c ---[ 526]---> Adder-cost: 130 maxlim: 11520 bits: 15/14 c ---[ 524]---> Adder-cost: 90 maxlim: 6912 bits: 14/13 c ---[ 522]---> Adder-cost: 100 maxlim: 6656 bits: 14/13 c ---[ 520]---> Adder-cost: 90 maxlim: 6400 bits: 14/13 c ---[ 518]---> Adder-cost: 74 maxlim: 5888 bits: 14/13 c ---[ 516]---> Adder-cost: 50 maxlim: 4864 bits: 14/13 c ---[ 514]---> Adder-cost: 82 maxlim: 5376 bits: 14/13 c ---[ 512]---> Sorter-cost: 372 Base: 2 2 2 2 2 2 2 7 c ---[ 510]---> Sorter-cost: 322 Base: 2 2 2 2 2 2 2 7 c ---[ 508]---> Sorter-cost: 266 Base: 2 2 2 2 2 2 2 2 c ---[ 506]---> Sorter-cost: 360 Base: 2 2 2 2 2 2 2 7 c ---[ 504]---> Sorter-cost: 992 Base: 2 2 2 2 2 2 2 7 c ---[ 502]---> Sorter-cost: 1064 Base: 2 2 2 2 2 2 2 7 c ---[ 500]---> Sorter-cost: 845 Base: 2 2 2 2 2 2 2 7 c ---[ 498]---> Adder-cost: 72 maxlim: 5504 bits: 14/13 c ---[ 496]---> Adder-cost: 80 maxlim: 6016 bits: 14/13 c ---[ 494]---> Adder-cost: 54 maxlim: 4480 bits: 14/13 c ---[ 492]---> Adder-cost: 50 maxlim: 5376 bits: 14/13 c ---[ 490]---> Adder-cost: 72 maxlim: 5376 bits: 14/13 c ---[ 488]---> Adder-cost: 68 maxlim: 5632 bits: 14/13 c ---[ 486]---> Adder-cost: 92 maxlim: 5760 bits: 14/13 c ---[ 484]---> Adder-cost: 64 maxlim: 6144 bits: 14/13 c ---[ 482]---> Adder-cost: 109 maxlim: 8192 bits: 15/14 c ---[ 480]---> Adder-cost: 116 maxlim: 8448 bits: 15/14 c ---[ 478]---> Adder-cost: 82 maxlim: 6016 bits: 14/13 c ---[ 476]---> Sorter-cost: 784 Base: 2 2 2 2 2 2 2 7 c ---[ 474]---> Sorter-cost: 730 Base: 2 2 2 2 2 2 2 7 c ---[ 472]---> Sorter-cost: 934 Base: 2 2 2 2 2 2 2 7 c ---[ 470]---> Sorter-cost: 650 Base: 2 2 2 2 2 2 2 7 c ---[ 468]---> Sorter-cost: 614 Base: 2 2 2 2 2 2 2 7 c ---[ 466]---> Adder-cost: 84 maxlim: 5120 bits: 14/13 c ---[ 464]---> Adder-cost: 76 maxlim: 4864 bits: 14/13 c ---[ 462]---> Adder-cost: 52 maxlim: 4864 bits: 14/13 c ---[ 460]---> Adder-cost: 100 maxlim: 7040 bits: 14/13 c ---[ 458]---> Sorter-cost: 675 Base: 2 2 2 2 2 2 2 7 c ---[ 456]---> Sorter-cost: 563 Base: 2 2 2 2 2 2 2 7 c ---[ 454]---> Sorter-cost: 392 Base: 2 2 2 2 2 2 2 7 c ---[ 452]---> Sorter-cost: 447 Base: 2 2 2 2 2 2 2 7 c ---[ 450]---> Adder-cost: 98 maxlim: 6528 bits: 14/13 c ---[ 448]---> Sorter-cost: 415 Base: 2 2 2 2 2 2 2 7 c ---[ 446]---> Sorter-cost: 582 Base: 2 2 2 2 2 2 2 7 c ---[ 444]---> Sorter-cost: 456 Base: 2 2 2 2 2 2 2 7 c ---[ 442]---> Adder-cost: 140 maxlim: 8704 bits: 15/14 c ---[ 440]---> Adder-cost: 62 maxlim: 8704 bits: 15/14 c ---[ 438]---> Adder-cost: 136 maxlim: 8448 bits: 15/14 c ---[ 436]---> Adder-cost: 112 maxlim: 7552 bits: 14/13 c ---[ 434]---> Sorter-cost: 314 Base: 2 2 2 2 2 2 2 2 c ---[ 432]---> Sorter-cost: 455 Base: 2 2 2 2 2 2 2 7 c ---[ 430]---> Adder-cost: 102 maxlim: 6272 bits: 14/13 c ---[ 428]---> Adder-cost: 68 maxlim: 5632 bits: 14/13 c ---[ 426]---> Adder-cost: 84 maxlim: 6528 bits: 14/13 c ---[ 424]---> Adder-cost: 88 maxlim: 6144 bits: 14/13 c ---[ 422]---> Sorter-cost: 713 Base: 2 2 2 2 2 2 2 7 c ---[ 420]---> Sorter-cost: 639 Base: 2 2 2 2 2 2 2 7 c ---[ 418]---> Sorter-cost: 415 Base: 2 2 2 2 2 2 2 7 c ---[ 416]---> Sorter-cost: 573 Base: 2 2 2 2 2 2 2 7 c ---[ 414]---> Adder-cost: 86 maxlim: 5248 bits: 14/13 c ---[ 412]---> Sorter-cost: 673 Base: 2 2 2 2 2 2 2 7 c ---[ 410]---> Sorter-cost: 308 Base: 2 2 2 2 2 2 2 2 c ---[ 408]---> Sorter-cost: 400 Base: 2 2 2 2 2 2 2 7 c ---[ 406]---> Sorter-cost: 248 Base: 2 2 2 2 2 2 2 2 c ---[ 404]---> Adder-cost: 88 maxlim: 6912 bits: 14/13 c ---[ 402]---> Sorter-cost: 272 Base: 2 2 2 2 2 2 2 2 c ---[ 400]---> Sorter-cost: 368 Base: 2 2 2 2 2 2 2 7 c ---[ 398]---> Sorter-cost: 440 Base: 2 2 2 2 2 2 2 7 c ---[ 396]---> Sorter-cost: 396 Base: 2 2 2 2 2 2 2 7 c ---[ 394]---> Sorter-cost: 280 Base: 2 2 2 2 2 2 2 7 c ---[ 392]---> Adder-cost: 90 maxlim: 5888 bits: 14/13 c ---[ 390]---> Adder-cost: 40 maxlim: 5888 bits: 14/13 c ---[ 388]---> Adder-cost: 82 maxlim: 6400 bits: 14/13 c ---[ 386]---> Adder-cost: 108 maxlim: 7296 bits: 14/13 c ---[ 384]---> Adder-cost: 72 maxlim: 6528 bits: 14/13 c ---[ 382]---> Adder-cost: 82 maxlim: 6656 bits: 14/13 c ---[ 380]---> Adder-cost: 148 maxlim: 13184 bits: 15/14 c ---[ 378]---> Adder-cost: 74 maxlim: 13184 bits: 15/14 c ---[ 376]---> Sorter-cost: 658 Base: 2 2 2 2 2 2 2 7 c ---[ 374]---> Sorter-cost: 492 Base: 2 2 2 2 2 2 2 7 c ---[ 372]---> Sorter-cost: 575 Base: 2 2 2 2 2 2 2 7 c ---[ 370]---> Sorter-cost: 982 Base: 2 2 2 2 2 2 2 7 c ---[ 368]---> Adder-cost: 90 maxlim: 6016 bits: 14/13 c ---[ 366]---> Sorter-cost: 370 Base: 2 2 2 2 2 2 2 7 c ---[ 364]---> Sorter-cost: 679 Base: 2 2 2 2 2 2 2 7 c ---[ 362]---> Sorter-cost: 680 Base: 2 2 2 2 2 2 2 7 c ---[ 360]---> Adder-cost: 90 maxlim: 6528 bits: 14/13 c ---[ 358]---> Adder-cost: 194 maxlim: 12416 bits: 15/14 c ---[ 356]---> Sorter-cost: 986 Base: 2 2 2 2 2 2 2 7 c ---[ 354]---> Sorter-cost: 687 Base: 2 2 2 2 2 2 2 7 c ---[ 352]---> Sorter-cost: 409 Base: 2 2 2 2 2 2 2 7 c ---[ 350]---> Adder-cost: 176 maxlim: 13184 bits: 15/14 c ---[ 348]---> Adder-cost: 190 maxlim: 16000 bits: 15/14 c ---[ 346]---> Adder-cost: 148 maxlim: 11392 bits: 15/14 c ---[ 344]---> Adder-cost: 310 maxlim: 21888 bits: 16/15 c ---[ 342]---> Adder-cost: 80 maxlim: 6784 bits: 14/13 c ---[ 340]---> Adder-cost: 210 maxlim: 21888 bits: 16/15 c ---[ 338]---> Adder-cost: 230 maxlim: 16256 bits: 15/14 c ---[ 336]---> Adder-cost: 98 maxlim: 7040 bits: 14/13 c ---[ 334]---> Adder-cost: 108 maxlim: 7296 bits: 14/13 c ---[ 332]---> Adder-cost: 120 maxlim: 7680 bits: 14/13 c ---[ 330]---> Adder-cost: 122 maxlim: 8064 bits: 14/13 c ---[ 328]---> Adder-cost: 126 maxlim: 10752 bits: 15/14 c ---[ 326]---> Adder-cost: 204 maxlim: 16256 bits: 15/14 c ---[ 324]---> Adder-cost: 150 maxlim: 11264 bits: 15/14 c ---[ 322]---> Adder-cost: 120 maxlim: 8960 bits: 15/14 c ---[ 320]---> Sorter-cost: 978 Base: 2 2 2 2 2 2 2 7 c ---[ 318]---> Sorter-cost: 594 Base: 2 2 2 2 2 2 2 7 c ---[ 316]---> Sorter-cost: 563 Base: 2 2 2 2 2 2 2 7 c ---[ 314]---> Sorter-cost: 409 Base: 2 2 2 2 2 2 2 7 c ---[ 312]---> Sorter-cost: 429 Base: 2 2 2 2 2 2 2 7 c ---[ 310]---> Sorter-cost: 584 Base: 2 2 2 2 2 2 2 7 c ---[ 308]---> Sorter-cost: 406 Base: 2 2 2 2 2 2 2 7 c ---[ 306]---> Sorter-cost: 426 Base: 2 2 2 2 2 2 2 7 c ---[ 304]---> Sorter-cost: 392 Base: 2 2 2 2 2 2 2 7 c ---[ 302]---> Sorter-cost: 637 Base: 2 2 2 2 2 2 2 7 c ---[ 300]---> Sorter-cost: 820 Base: 2 2 2 2 2 2 2 7 c ---[ 298]---> Sorter-cost: 897 Base: 2 2 2 2 2 2 2 7 c ---[ 296]---> Adder-cost: 142 maxlim: 9728 bits: 15/14 c ---[ 294]---> Adder-cost: 112 maxlim: 9216 bits: 15/14 c ---[ 292]---> Adder-cost: 102 maxlim: 10880 bits: 15/14 c ---[ 290]---> Adder-cost: 92 maxlim: 6400 bits: 14/13 c ---[ 288]---> Sorter-cost: 616 Base: 2 2 2 2 2 2 2 7 c ---[ 286]---> Sorter-cost: 616 Base: 2 2 2 2 2 2 2 7 c ---[ 284]---> Adder-cost: 84 maxlim: 5248 bits: 14/13 c ---[ 282]---> Sorter-cost: 916 Base: 2 2 2 2 2 2 2 7 c ---[ 280]---> Sorter-cost: 579 Base: 2 2 2 2 2 2 2 7 c ---[ 278]---> Adder-cost: 116 maxlim: 7552 bits: 14/13 c ---[ 276]---> Sorter-cost: 850 Base: 2 2 2 2 2 2 2 7 c ---[ 274]---> Adder-cost: 116 maxlim: 8192 bits: 15/14 c ---[ 272]---> Adder-cost: 94 maxlim: 8704 bits: 15/14 c ---[ 270]---> Adder-cost: 76 maxlim: 4864 bits: 14/13 c ---[ 268]---> Adder-cost: 76 maxlim: 5120 bits: 14/13 c ---[ 266]---> Sorter-cost: 907 Base: 2 2 2 2 2 2 2 7 c ---[ 264]---> Sorter-cost: 677 Base: 2 2 2 2 2 2 2 7 c ---[ 262]---> Sorter-cost: 1157 Base: 2 2 2 2 2 2 2 7 c ---[ 260]---> Sorter-cost: 1044 Base: 2 2 2 2 2 2 2 7 c ---[ 258]---> Adder-cost: 118 maxlim: 7424 bits: 14/13 c ---[ 256]---> Adder-cost: 104 maxlim: 8064 bits: 14/13 c ---[ 254]---> Sorter-cost: 877 Base: 2 2 2 2 2 2 2 7 c ---[ 252]---> Adder-cost: 94 maxlim: 7680 bits: 14/13 c ---[ 250]---> Adder-cost: 70 maxlim: 7552 bits: 14/13 c ---[ 248]---> Adder-cost: 60 maxlim: 4992 bits: 14/13 c ---[ 246]---> Adder-cost: 88 maxlim: 5504 bits: 14/13 c ---[ 244]---> Sorter-cost: 730 Base: 2 2 2 2 2 2 2 7 c ---[ 242]---> Sorter-cost: 930 Base: 2 2 2 2 2 2 2 7 c ---[ 240]---> Sorter-cost: 1054 Base: 2 2 2 2 2 2 2 7 c ---[ 238]---> Sorter-cost: 1145 Base: 2 2 2 2 2 2 2 7 c ---[ 236]---> Sorter-cost: 888 Base: 2 2 2 2 2 2 2 7 c ---[ 234]---> Sorter-cost: 447 Base: 2 2 2 2 2 2 2 7 c ---[ 232]---> Sorter-cost: 564 Base: 2 2 2 2 2 2 2 7 c ---[ 230]---> Sorter-cost: 311 Base: 2 2 2 2 2 2 2 7 c ---[ 228]---> Sorter-cost: 419 Base: 2 2 2 2 2 2 2 7 c ---[ 226]---> Sorter-cost: 563 Base: 2 2 2 2 2 2 2 7 c ---[ 224]---> Adder-cost: 138 maxlim: 9600 bits: 15/14 c ---[ 222]---> Adder-cost: 112 maxlim: 9856 bits: 15/14 c ---[ 220]---> Adder-cost: 82 maxlim: 6016 bits: 14/13 c ---[ 218]---> Adder-cost: 96 maxlim: 6528 bits: 14/13 c ---[ 216]---> Sorter-cost: 901 Base: 2 2 2 2 2 2 2 7 c ---[ 214]---> Sorter-cost: 339 Base: 2 2 2 2 2 2 2 7 c ---[ 212]---> Sorter-cost: 266 Base: 2 2 2 2 2 2 2 2 c ---[ 210]---> Adder-cost: 58 maxlim: 6144 bits: 14/13 c ---[ 208]---> Sorter-cost: 454 Base: 2 2 2 2 2 2 2 7 c ---[ 206]---> Adder-cost: 86 maxlim: 5248 bits: 14/13 c ---[ 204]---> Adder-cost: 74 maxlim: 5376 bits: 14/13 c ---[ 202]---> Adder-cost: 40 maxlim: 5376 bits: 14/13 c ---[ 200]---> Adder-cost: 82 maxlim: 5376 bits: 14/13 c ---[ 198]---> Adder-cost: 258 maxlim: 16768 bits: 16/15 c ---[ 196]---> Adder-cost: 176 maxlim: 11264 bits: 15/14 c ---[ 194]---> Adder-cost: 160 maxlim: 10368 bits: 15/14 c ---[ 192]---> Sorter-cost: 542 Base: 2 2 2 2 2 2 2 7 c ---[ 190]---> Adder-cost: 134 maxlim: 9600 bits: 15/14 c ---[ 188]---> Adder-cost: 182 maxlim: 15872 bits: 15/14 c ---[ 186]---> Adder-cost: 242 maxlim: 18048 bits: 16/15 c ---[ 184]---> Adder-cost: 232 maxlim: 18432 bits: 16/15 c ---[ 182]---> Adder-cost: 142 maxlim: 10112 bits: 15/14 c ---[ 180]---> Adder-cost: 90 maxlim: 6016 bits: 14/13 c ---[ 178]---> Sorter-cost: 656 Base: 2 2 2 2 2 2 2 7 c ---[ 176]---> Sorter-cost: 692 Base: 2 2 2 2 2 2 2 7 c ---[ 174]---> Sorter-cost: 962 Base: 2 2 2 2 2 2 2 7 c ---[ 172]---> Sorter-cost: 406 Base: 2 2 2 2 2 2 2 7 c ---[ 170]---> Sorter-cost: 652 Base: 2 2 2 2 2 2 2 7 c ---[ 168]---> Sorter-cost: 306 Base: 2 2 2 2 2 2 2 2 c ---[ 166]---> Sorter-cost: 356 Base: 2 2 2 2 2 2 2 7 c ---[ 164]---> Sorter-cost: 230 Base: 2 2 2 2 2 2 2 2 c ---[ 162]---> Sorter-cost: 250 Base: 2 2 2 2 2 2 2 2 c ---[ 160]---> Sorter-cost: 404 Base: 2 2 2 2 2 2 2 7 c ---[ 158]---> Sorter-cost: 270 Base: 2 2 2 2 2 2 2 2 c ---[ 156]---> Sorter-cost: 256 Base: 2 2 2 2 2 2 2 2 c ---[ 154]---> Sorter-cost: 691 Base: 2 2 2 2 2 2 2 7 c ---[ 152]---> Sorter-cost: 551 Base: 2 2 2 2 2 2 2 7 c ---[ 150]---> Sorter-cost: 507 Base: 2 2 2 2 2 2 2 7 c ---[ 148]---> Sorter-cost: 671 Base: 2 2 2 2 2 2 2 7 c ---[ 146]---> Sorter-cost: 1016 Base: 2 2 2 2 2 2 2 7 c ---[ 144]---> Sorter-cost: 656 Base: 2 2 2 2 2 2 2 7 c ---[ 142]---> Sorter-cost: 665 Base: 2 2 2 2 2 2 2 7 c ---[ 140]---> Sorter-cost: 523 Base: 2 2 2 2 2 2 2 7 c ---[ 138]---> Sorter-cost: 302 Base: 2 2 2 2 2 2 2 2 c ---[ 136]---> Adder-cost: 152 maxlim: 9344 bits: 15/14 c ---[ 134]---> Adder-cost: 128 maxlim: 8576 bits: 15/14 c ---[ 132]---> Adder-cost: 102 maxlim: 8320 bits: 15/14 c ---[ 130]---> Adder-cost: 94 maxlim: 6400 bits: 14/13 c ---[ 128]---> Sorter-cost: 901 Base: 2 2 2 2 2 2 2 7 c ---[ 126]---> Sorter-cost: 553 Base: 2 2 2 2 2 2 2 7 c ---[ 124]---> Sorter-cost: 1004 Base: 2 2 2 2 2 2 2 7 c ---[ 122]---> Sorter-cost: 1074 Base: 2 2 2 2 2 2 2 7 c ---[ 120]---> Sorter-cost: 956 Base: 2 2 2 2 2 2 2 7 c ---[ 118]---> Sorter-cost: 627 Base:
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/28686/stat): 28686 (minisat+_script) R 28685 28686 31027 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1856090863 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/28686/statm): 174 3 169 147 0 27 0 [pid=28686] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libtermcap.so.2 open syscall for file tls/i686/libtermcap.so.2 open syscall for file tls/mmx/libtermcap.so.2 open syscall for file tls/libtermcap.so.2 open syscall for file i686/mmx/libtermcap.so.2 open syscall for file i686/libtermcap.so.2 open syscall for file mmx/libtermcap.so.2 open syscall for file libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/libtermcap.so.2 open syscall for file /etc/ld.so.cache open syscall for file /lib/libtermcap.so.2 open syscall for file tls/i686/mmx/libdl.so.2 open syscall for file tls/i686/libdl.so.2 open syscall for file tls/mmx/libdl.so.2 open syscall for file tls/libdl.so.2 open syscall for file i686/mmx/libdl.so.2 open syscall for file i686/libdl.so.2 open syscall for file mmx/libdl.so.2 open syscall for file libdl.so.2 open syscall for file /oldhome/oroussel/lib/libdl.so.2 open syscall for file /lib/libdl.so.2 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file /dev/tty open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script New process pid=28687 New process pid=28688 New process pid=28689 execve syscall for /bin/sed executable One traced child (pid=28688) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=28689) exited with status: 0 One traced child (pid=28687) exited with status: 0 New process pid=28690 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-trento1.opb One traced child (pid=28690) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=28691 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-trento1.opb [startup+10.0041 s] Raw data (loadavg): 0.93 0.96 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 4508 0 0 0 918 25 0 0 25 0 1 0 1856090897 14790656 3422 4294967295 134512640 135167914 3221224448 3221223200 134844706 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28691/statm): 3611 3422 162 162 0 3449 0 [pid=28691] vsize: 14444 Current children cumulated CPU time (s) 9.68 Current children cumulated vsize (Kb) 16572 [startup+20.005 s] Raw data (loadavg): 0.94 0.96 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 7122 0 0 0 1894 38 0 0 25 0 1 0 1856090897 22577152 5179 4294967295 134512640 135167914 3221224448 3221222544 134844725 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28691/statm): 5512 5179 162 162 0 5350 0 [pid=28691] vsize: 22048 Current children cumulated CPU time (s) 19.57 Current children cumulated vsize (Kb) 24176 [startup+30.0069 s] Raw data (loadavg): 0.95 0.96 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 9135 0 0 0 2883 45 0 0 25 0 1 0 1856090897 28676096 6697 4294967295 134512640 135167914 3221224448 3221223196 134843002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 7001 6697 162 162 0 6839 0 [pid=28691] vsize: 28004 Current children cumulated CPU time (s) 29.53 Current children cumulated vsize (Kb) 30132 [startup+40.0079 s] Raw data (loadavg): 0.96 0.96 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 14067 0 0 0 3854 63 0 0 25 0 1 0 1856090897 51036160 10928 4294967295 134512640 135167914 3221224448 3221223024 134849196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 12460 10928 162 162 0 12298 0 [pid=28691] vsize: 49840 Current children cumulated CPU time (s) 39.42 Current children cumulated vsize (Kb) 51968 [startup+50.0088 s] Raw data (loadavg): 0.96 0.96 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 18469 0 0 0 4835 75 0 0 25 0 1 0 1856090897 61067264 13909 4294967295 134512640 135167914 3221224448 3221221840 134844723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 14909 13909 162 162 0 14747 0 [pid=28691] vsize: 59636 Current children cumulated CPU time (s) 49.35 Current children cumulated vsize (Kb) 61764 [startup+60.0097 s] Raw data (loadavg): 0.97 0.96 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 19364 0 0 0 5828 78 0 0 25 0 1 0 1856090897 61288448 13966 4294967295 134512640 135167914 3221224448 3221221472 134629340 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 14963 13966 162 162 0 14801 0 [pid=28691] vsize: 59852 Current children cumulated CPU time (s) 59.31 Current children cumulated vsize (Kb) 61980 [startup+70.0106 s] Raw data (loadavg): 0.97 0.96 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 19726 0 0 0 6825 80 0 0 25 0 1 0 1856090897 61083648 13918 4294967295 134512640 135167914 3221224448 3221221612 134722227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 14913 13918 162 162 0 14751 0 [pid=28691] vsize: 59652 Current children cumulated CPU time (s) 69.3 Current children cumulated vsize (Kb) 61780 [startup+80.0116 s] Raw data (loadavg): 0.98 0.96 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 19732 0 0 0 7825 80 0 0 25 0 1 0 1856090897 61108224 13924 4294967295 134512640 135167914 3221224448 3221221664 134844668 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 14919 13924 162 162 0 14757 0 [pid=28691] vsize: 59676 Current children cumulated CPU time (s) 79.3 Current children cumulated vsize (Kb) 61804 [startup+90.0125 s] Raw data (loadavg): 0.98 0.96 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 19732 0 0 0 8825 80 0 0 25 0 1 0 1856090897 61108224 13924 4294967295 134512640 135167914 3221224448 3221222960 134845913 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 14919 13924 162 162 0 14757 0 [pid=28691] vsize: 59676 Current children cumulated CPU time (s) 89.3 Current children cumulated vsize (Kb) 61804 [startup+100.014 s] Raw data (loadavg): 0.98 0.96 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 19921 0 0 0 9824 81 0 0 25 0 1 0 1856090897 61067264 13914 4294967295 134512640 135167914 3221224448 3221221088 134849068 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 14909 13914 162 162 0 14747 0 [pid=28691] vsize: 59636 Current children cumulated CPU time (s) 99.3 Current children cumulated vsize (Kb) 61764 [startup+110.015 s] Raw data (loadavg): 0.98 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 19921 0 0 0 10824 81 0 0 25 0 1 0 1856090897 61067264 13914 4294967295 134512640 135167914 3221224448 3221221664 134844653 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 14909 13914 162 162 0 14747 0 [pid=28691] vsize: 59636 Current children cumulated CPU time (s) 109.3 Current children cumulated vsize (Kb) 61764 [startup+120.016 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 19921 0 0 0 11824 81 0 0 25 0 1 0 1856090897 61067264 13914 4294967295 134512640 135167914 3221224448 3221222256 134844682 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 14909 13914 162 162 0 14747 0 [pid=28691] vsize: 59636 Current children cumulated CPU time (s) 119.3 Current children cumulated vsize (Kb) 61764 [startup+130.017 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 20795 0 0 0 12817 84 0 0 25 0 1 0 1856090897 63291392 14788 4294967295 134512640 135167914 3221224448 3221222080 134843402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 15452 14788 162 162 0 15290 0 [pid=28691] vsize: 61808 Current children cumulated CPU time (s) 129.26 Current children cumulated vsize (Kb) 63936 [startup+140.018 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 20795 0 0 0 13817 85 0 0 25 0 1 0 1856090897 63291392 14788 4294967295 134512640 135167914 3221224448 3221223248 134849092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28691/statm): 15452 14788 162 162 0 15290 0 [pid=28691] vsize: 61808 Current children cumulated CPU time (s) 139.27 Current children cumulated vsize (Kb) 63936 [startup+150.02 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 20795 0 0 0 14816 85 0 0 25 0 1 0 1856090897 63291392 14788 4294967295 134512640 135167914 3221224448 3221218452 134843117 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 15452 14788 162 162 0 15290 0 [pid=28691] vsize: 61808 Current children cumulated CPU time (s) 149.26 Current children cumulated vsize (Kb) 63936 [startup+160.021 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 20795 0 0 0 15815 85 0 0 25 0 1 0 1856090897 63291392 14788 4294967295 134512640 135167914 3221224448 3221223232 134843426 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 15452 14788 162 162 0 15290 0 [pid=28691] vsize: 61808 Current children cumulated CPU time (s) 159.25 Current children cumulated vsize (Kb) 63936 [startup+170.021 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 25649 0 0 0 16782 102 0 0 25 0 1 0 1856090897 80633856 19022 4294967295 134512640 135167914 3221224448 3216187440 134624334 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 19686 19022 162 162 0 19524 0 [pid=28691] vsize: 78744 Current children cumulated CPU time (s) 169.09 Current children cumulated vsize (Kb) 80872 [startup+180.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 30483 0 0 0 17740 122 0 0 25 0 1 0 1856090897 97300480 23197 4294967295 134512640 135167914 3221224448 3216822004 134625024 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 23755 23197 162 162 0 23593 0 [pid=28691] vsize: 95020 Current children cumulated CPU time (s) 178.87 Current children cumulated vsize (Kb) 97148 [startup+190.022 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 35829 0 0 0 18705 141 0 0 25 0 1 0 1856090897 113737728 27225 4294967295 134512640 135167914 3221224448 3216919456 134844694 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 27768 27225 162 162 0 27606 0 [pid=28691] vsize: 111072 Current children cumulated CPU time (s) 188.71 Current children cumulated vsize (Kb) 113200 [startup+200.023 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 38832 0 0 0 19671 157 0 0 25 0 1 0 1856090897 125800448 30228 4294967295 134512640 135167914 3221224448 3216611104 134847156 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 30713 30228 162 162 0 30551 0 [pid=28691] vsize: 122852 Current children cumulated CPU time (s) 198.53 Current children cumulated vsize (Kb) 124980 [startup+210.024 s] Raw data (loadavg): 0.99 0.97 0.93 1/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) T 28686 28686 31027 0 -1 0 42607 0 0 0 20631 173 0 0 25 0 1 0 1856090897 140156928 34003 4294967295 134512640 135167914 3221224448 3216297084 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/28691/statm): 34218 34003 162 162 0 34056 0 [pid=28691] vsize: 136872 Current children cumulated CPU time (s) 208.29 Current children cumulated vsize (Kb) 139000 [startup+220.025 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 21599 187 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221221552 134843010 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 218.11 Current children cumulated vsize (Kb) 151220 [startup+230.026 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 22599 187 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215152 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 228.11 Current children cumulated vsize (Kb) 151220 [startup+240.026 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 23600 187 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215280 134849143 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 238.12 Current children cumulated vsize (Kb) 151220 [startup+250.027 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 24600 187 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215520 134845927 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 248.12 Current children cumulated vsize (Kb) 151220 [startup+260.028 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 25600 187 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215612 134845876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 258.12 Current children cumulated vsize (Kb) 151220 [startup+270.029 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 26600 187 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215264 134843123 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 268.12 Current children cumulated vsize (Kb) 151220 [startup+280.031 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 27600 187 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215484 134693792 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 278.12 Current children cumulated vsize (Kb) 151220 [startup+290.031 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 28601 187 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215776 134845881 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 288.13 Current children cumulated vsize (Kb) 151220 [startup+300.032 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 29601 187 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215680 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 298.13 Current children cumulated vsize (Kb) 151220 [startup+310.033 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 30601 188 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215920 134844706 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 308.14 Current children cumulated vsize (Kb) 151220 [startup+320.033 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 31601 188 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215296 134694351 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 318.14 Current children cumulated vsize (Kb) 151220 [startup+330.034 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 32601 188 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215568 134843036 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 328.14 Current children cumulated vsize (Kb) 151220 [startup+340.035 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 33601 188 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215496 134629277 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 338.14 Current children cumulated vsize (Kb) 151220 [startup+350.036 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 34601 188 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215456 134694517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 348.14 Current children cumulated vsize (Kb) 151220 [startup+360.037 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 35602 188 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215744 134844668 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 358.15 Current children cumulated vsize (Kb) 151220 [startup+370.037 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 36602 188 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215120 134522227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 368.15 Current children cumulated vsize (Kb) 151220 [startup+380.038 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 37602 188 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216508 134722542 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 378.15 Current children cumulated vsize (Kb) 151220 [startup+390.038 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 38602 188 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215292 134722656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 388.15 Current children cumulated vsize (Kb) 151220 [startup+400.04 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 39603 188 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215304 134693744 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 398.16 Current children cumulated vsize (Kb) 151220 [startup+410.041 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 40603 188 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216008 134849057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 408.16 Current children cumulated vsize (Kb) 151220 [startup+420.042 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 41603 188 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216208 134844706 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 418.16 Current children cumulated vsize (Kb) 151220 [startup+430.043 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 42603 189 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216000 134849099 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 428.17 Current children cumulated vsize (Kb) 151220 [startup+440.043 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 43603 189 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216000 134693570 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 438.17 Current children cumulated vsize (Kb) 151220 [startup+450.045 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 44603 189 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216352 134693561 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 448.17 Current children cumulated vsize (Kb) 151220 [startup+460.046 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 45603 189 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216096 134844653 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 458.17 Current children cumulated vsize (Kb) 151220 [startup+470.046 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 46604 189 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216020 134629281 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 468.18 Current children cumulated vsize (Kb) 151220 [startup+480.047 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 47604 189 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215392 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 478.18 Current children cumulated vsize (Kb) 151220 [startup+490.048 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 48604 189 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215732 134843117 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 488.18 Current children cumulated vsize (Kb) 151220 [startup+500.049 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 49604 189 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215920 134843074 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 498.18 Current children cumulated vsize (Kb) 151220 [startup+510.05 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 50604 189 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215920 134843036 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 508.18 Current children cumulated vsize (Kb) 151220 [startup+520.051 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 51604 189 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216336 134849108 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 518.18 Current children cumulated vsize (Kb) 151220 [startup+530.052 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 52605 189 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216476 134842996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 528.19 Current children cumulated vsize (Kb) 151220 [startup+540.052 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 53605 189 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216336 134843113 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 538.19 Current children cumulated vsize (Kb) 151220 [startup+550.053 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 54605 189 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215408 134843107 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 548.19 Current children cumulated vsize (Kb) 151220 [startup+560.054 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 55605 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215632 134694517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 558.2 Current children cumulated vsize (Kb) 151220 [startup+570.057 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 56605 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215916 134718504 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 568.2 Current children cumulated vsize (Kb) 151220 [startup+580.058 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 57606 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216112 134843036 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 578.21 Current children cumulated vsize (Kb) 151220 [startup+590.058 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 58606 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215808 134694532 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 588.21 Current children cumulated vsize (Kb) 151220 [startup+600.059 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 59606 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215824 134693563 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 598.21 Current children cumulated vsize (Kb) 151220 [startup+610.06 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 60606 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216300 134843033 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 608.21 Current children cumulated vsize (Kb) 151220 [startup+620.06 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 61606 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215952 134695257 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 618.21 Current children cumulated vsize (Kb) 151220 [startup+630.061 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 62607 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215680 134844736 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 628.22 Current children cumulated vsize (Kb) 151220 [startup+640.062 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 63607 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215664 134630853 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 638.22 Current children cumulated vsize (Kb) 151220 [startup+650.063 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 64607 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215392 134845903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 648.22 Current children cumulated vsize (Kb) 151220 [startup+660.064 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 65607 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215856 134844647 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 658.22 Current children cumulated vsize (Kb) 151220 [startup+670.065 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 66607 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215152 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 668.22 Current children cumulated vsize (Kb) 151220 [startup+680.066 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 67608 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215584 134849153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 678.23 Current children cumulated vsize (Kb) 151220 [startup+690.066 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 68608 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216448 134845927 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 688.23 Current children cumulated vsize (Kb) 151220 [startup+700.068 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 69608 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215952 134722521 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 698.23 Current children cumulated vsize (Kb) 151220 [startup+710.069 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 70608 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217424 134629224 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 708.23 Current children cumulated vsize (Kb) 151220 [startup+720.07 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 71609 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217532 134723206 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 718.24 Current children cumulated vsize (Kb) 151220 [startup+730.071 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 72609 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215828 134843000 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 728.24 Current children cumulated vsize (Kb) 151220 [startup+740.071 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 73609 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215824 134693576 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 738.24 Current children cumulated vsize (Kb) 151220 [startup+750.073 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 74609 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215744 134845927 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 748.24 Current children cumulated vsize (Kb) 151220 [startup+760.074 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 75609 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215728 134843118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 758.24 Current children cumulated vsize (Kb) 151220 [startup+770.074 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 76609 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215652 134696564 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 768.24 Current children cumulated vsize (Kb) 151220 [startup+780.075 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 77610 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216080 134845903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 778.25 Current children cumulated vsize (Kb) 151220 [startup+790.076 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 78610 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216124 134693600 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 788.25 Current children cumulated vsize (Kb) 151220 [startup+800.077 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 79610 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217068 134849056 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 798.25 Current children cumulated vsize (Kb) 151220 [startup+810.078 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 80610 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217424 134630893 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 808.25 Current children cumulated vsize (Kb) 151220 [startup+820.078 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 81610 190 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217744 134849082 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 818.25 Current children cumulated vsize (Kb) 151220 [startup+830.079 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 82611 191 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215552 134845913 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 828.27 Current children cumulated vsize (Kb) 151220 [startup+840.08 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 83611 191 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216160 134843081 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 838.27 Current children cumulated vsize (Kb) 151220 [startup+850.082 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 84611 191 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216160 134849143 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 848.27 Current children cumulated vsize (Kb) 151220 [startup+860.083 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 85611 191 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215964 134845940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 858.27 Current children cumulated vsize (Kb) 151220 [startup+870.084 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 86611 191 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216496 134849148 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 868.27 Current children cumulated vsize (Kb) 151220 [startup+880.086 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 87612 191 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217648 134844672 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 878.28 Current children cumulated vsize (Kb) 151220 [startup+890.087 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 88612 191 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217696 134849163 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 888.28 Current children cumulated vsize (Kb) 151220 [startup+900.088 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 89612 191 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217384 134845877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 898.28 Current children cumulated vsize (Kb) 151220 [startup+910.089 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 90612 191 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221218252 134845876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 908.28 Current children cumulated vsize (Kb) 151220 [startup+920.09 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 91612 191 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217696 134723229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 918.28 Current children cumulated vsize (Kb) 151220 [startup+930.091 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 92613 191 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221218128 134630790 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 928.29 Current children cumulated vsize (Kb) 151220 [startup+940.092 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 93613 191 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216016 134629172 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 938.29 Current children cumulated vsize (Kb) 151220 [startup+950.093 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 94613 191 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216192 134630751 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 948.29 Current children cumulated vsize (Kb) 151220 [startup+960.094 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 95613 191 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216272 134843402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 958.29 Current children cumulated vsize (Kb) 151220 [startup+970.095 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 96613 191 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217408 134693563 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 968.29 Current children cumulated vsize (Kb) 151220 [startup+980.095 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 97614 191 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217328 134844644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 978.3 Current children cumulated vsize (Kb) 151220 [startup+990.096 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 98614 191 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217856 134845933 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 988.3 Current children cumulated vsize (Kb) 151220 [startup+1000.1 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 99614 191 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217488 134845911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 998.3 Current children cumulated vsize (Kb) 151220 [startup+1010.1 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 100615 191 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217944 134522234 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 1008.31 Current children cumulated vsize (Kb) 151220 [startup+1020.1 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 101615 191 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217856 134844689 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 1018.31 Current children cumulated vsize (Kb) 151220 [startup+1030.1 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 102615 191 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221215376 134845906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 1028.31 Current children cumulated vsize (Kb) 151220 [startup+1040.1 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 103615 192 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216176 134849108 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 1038.32 Current children cumulated vsize (Kb) 151220 [startup+1050.1 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 104615 192 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217632 134844697 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 1048.32 Current children cumulated vsize (Kb) 151220 [startup+1060.1 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 105615 192 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217152 134844694 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 1058.32 Current children cumulated vsize (Kb) 151220 [startup+1070.1 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 106616 192 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216352 134694338 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 1068.33 Current children cumulated vsize (Kb) 151220 [startup+1080.1 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 107616 192 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216560 134629451 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 1078.33 Current children cumulated vsize (Kb) 151220 [startup+1090.11 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 108616 192 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216624 134843118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 1088.33 Current children cumulated vsize (Kb) 151220 [startup+1100.11 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 109616 192 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216640 134723225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 1098.33 Current children cumulated vsize (Kb) 151220 [startup+1110.11 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 110616 192 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217212 134722512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 1108.33 Current children cumulated vsize (Kb) 151220 [startup+1120.11 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 111616 192 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217728 134845881 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 1118.33 Current children cumulated vsize (Kb) 151220 [startup+1130.11 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 112617 192 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217840 134845911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 1128.34 Current children cumulated vsize (Kb) 151220 [startup+1140.11 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 113617 192 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217968 134630786 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 1138.34 Current children cumulated vsize (Kb) 151220 [startup+1150.11 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 114617 192 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217216 134849068 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 1148.34 Current children cumulated vsize (Kb) 151220 [startup+1160.11 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 115617 192 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217416 134693783 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 1158.34 Current children cumulated vsize (Kb) 151220 [startup+1170.11 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 116618 192 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217696 134843400 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 1168.35 Current children cumulated vsize (Kb) 151220 [startup+1180.11 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 117618 192 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217920 134843406 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 1178.35 Current children cumulated vsize (Kb) 151220 [startup+1190.12 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 118618 192 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217856 134845888 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 1188.35 Current children cumulated vsize (Kb) 151220 [startup+1200.12 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 119618 192 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221217028 134849147 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 1198.35 Current children cumulated vsize (Kb) 151220 [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 120618 192 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216592 134844637 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 1208.35 Current children cumulated vsize (Kb) 151220 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.93 2/57 28691 Raw data (/proc/28686/stat): 28686 (minisat+_script) S 28685 28686 31027 0 -1 0 314 1325 0 0 0 1 18 6 17 0 1 0 1856090863 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28686/statm): 532 234 485 147 0 385 0 [pid=28686] vsize: 2128 Raw data (/proc/28691/stat): 28691 (minisat+_bignum) R 28686 28686 31027 0 -1 0 45685 0 0 0 120618 192 0 0 25 0 1 0 1856090897 152670208 34444 4294967295 134512640 135167914 3221224448 3221216704 134693582 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28691/statm): 37273 34444 162 162 0 37111 0 [pid=28691] vsize: 149092 Current children cumulated CPU time (s) 1208.35 Current children cumulated vsize (Kb) 151220 Sending SIGTERM to -28686 Sleeping 2 seconds One traced child (pid=28686) ended because it received signal 15 (SIGTERM) One traced child (pid=28691) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.19 CPU time (s): 1208.18 CPU user time (s): 1206.19 CPU system time (s): 1.9917 CPU usage (%): 99.8344 Max. virtual memory (cumulated for all children) (Kb): 151220
ERROR: no interpretation found !