Name | mps-v2-20-10/www.csit.fsu.edu/~burkardt/datasets/mps/normalized-mps-v2-20-10-afiro.opb |
MD5SUM | 27c455853db0a1f70b6ba60ff91cb013 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -4120833 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 150 |
Biggest coefficient in the objective function | 134217728000 |
Number of bits for the biggest coefficient in the objective function | 37 |
Sum of the numbers in the objective function | 316753837785 |
Number of bits of the sum of numbers in the objective function | 39 |
Biggest number in a constraint | 1304059445248 |
Number of bits of the biggest number in a constraint | 41 |
Biggest sum of numbers in a constraint | 20964809094075 |
Number of bits of the biggest sum of numbers | 45 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.14 |
Number of variables | 960 |
Total number of constraints | 27 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 27 |
Minimum length of a constraint | 30 |
Maximum length of a constraint | 270 |
LAUNCH ON wulflinc18 THE 2005-09-20 02:27:52 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3130 boxname=wulflinc18 idbench=786 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 27c455853db0a1f70b6ba60ff91cb013 /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-afiro.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-20-10-afiro.opb IDLAUNCH: 3130 /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: 861464 kB Buffers: 22164 kB Cached: 118148 kB SwapCached: 856 kB Active: 31488 kB Inactive: 111468 kB HighTotal: 131008 kB HighFree: 27300 kB LowTotal: 903652 kB LowFree: 834164 kB SwapTotal: 2097892 kB SwapFree: 2096528 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5732 kB Slab: 24604 kB Committed_AS: 64148 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 02:48:02 (client local time) WITH STATUS 10 IN 1209.48 SECONDS stats: 3130 7 1209.48 10
c Parsing PB file... c Converting 35 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ######## c -- Clauses(.)/Splits(s): ss c ---[ 35]---> BDD-cost: 145 c ---[ 33]---> Sorter-cost: 1542 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 c ---[ 31]---> Sorter-cost: 1565 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 29]---> Adder-cost: 589 maxlim: 26214350 bits: 26/25 c ---[ 27]---> Sorter-cost: 720 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 25]---> Sorter-cost: 1695 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 c ---[ 23]---> Adder-cost: 620 maxlim: 52428700 bits: 27/26 c ---[ 21]---> Sorter-cost: 1982 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 20]---> BDD-cost: 16 c ---[ 19]---> BDD-cost: 60 c ---[ 18]---> BDD-cost: 52 c ---[ 17]---> BDD-cost: 52 c ---[ 16]---> BDD-cost: 52 c ---[ 15]---> Sorter-cost: 1057 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 c ---[ 13]---> BDD-cost: 66 c ---[ 12]---> BDD-cost: 52 c ---[ 11]---> BDD-cost: 52 c ---[ 10]---> BDD-cost: 52 c ---[ 9]---> Sorter-cost: 1187 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 c ---[ 8]---> Adder-cost: 1890 maxlim: 4856199074 bits: 33/33 c ---[ 7]---> Sorter-cost: 3181 Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 6]---> Adder-cost: 788 maxlim: 198966863 bits: 29/28 c ---[ 4]---> Adder-cost: 797 maxlim: 407370522 bits: 30/29 c ---[ 3]---> BDD-cost: 83 c ---[ 2]---> BDD-cost: 88 c ---[ 1]---> BDD-cost: 13 c ---[ 0]---> Sorter-cost: 2580 Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 72289 210130 | 24096 0 0 nan | 0.000 % | c | 100 | 72282 210115 | 26505 99 624 6.3 | 4.777 % | c | 250 | 72240 210019 | 29156 248 2949 11.9 | 4.837 % | c | 475 | 72240 210019 | 32071 473 7762 16.4 | 4.837 % | c | 812 | 72222 209977 | 35278 809 11867 14.7 | 4.857 % | c | 1318 | 72105 209670 | 38806 1299 17237 13.3 | 4.993 % | c | 2077 | 72036 209515 | 42687 2052 30721 15.0 | 5.094 % | c | 3218 | 71770 208916 | 46956 3169 50288 15.9 | 5.497 % | c | 4928 | 71607 208533 | 51651 4867 93101 19.1 | 5.714 % | c | 7491 | 71398 207969 | 56817 7407 146223 19.7 | 5.931 % | c | 11336 | 71298 207745 | 62498 11236 240159 21.4 | 6.062 % | c | 17103 | 71223 207577 | 68748 16990 398518 23.5 | 6.162 % | c | 25754 | 71144 207391 | 75623 25634 619317 24.2 | 6.268 % | c | 38729 | 71093 207268 | 83185 38604 1009610 26.2 | 6.329 % | c | 58190 | 70964 206939 | 91504 58049 1634735 28.2 | 6.475 % | c | 87382 | 70932 206850 | 100654 87233 2838746 32.5 | 6.510 % | c | 131171 | 70821 206570 | 110720 44210 1648689 37.3 | 6.651 % | c ============================================================================== c [1mFound solution: -939884[0m c ---[ 0]---> Sorter-cost: 5556 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 165774 | 85451 240745 | 28483 78794 2862315 36.3 | 6.651 % | c | 165874 | 85451 240745 | 31331 18019 466393 25.9 | 5.499 % | c | 166024 | 85451 240745 | 34464 18169 468086 25.8 | 5.499 % | c | 166250 | 85451 240745 | 37910 18395 470271 25.6 | 5.499 % | c | 166588 | 85451 240745 | 41701 18733 484272 25.9 | 5.499 % | c | 167094 | 85426 240690 | 45872 19238 492725 25.6 | 5.527 % | c | 167855 | 85395 240621 | 50459 19997 506436 25.3 | 5.559 % | c | 168995 | 85395 240621 | 55505 21137 535394 25.3 | 5.559 % | c | 170703 | 85395 240621 | 61055 22845 583733 25.6 | 5.559 % | c | 173265 | 85375 240565 | 67161 25404 672150 26.5 | 5.575 % | c | 177109 | 85375 240565 | 73877 29248 778653 26.6 | 5.575 % | c ============================================================================== c [1mFound solution: -983297[0m c ---[ 0]---> Sorter-cost: 18 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 181867 | 85475 240886 | 28491 34005 927025 27.3 | 5.575 % | c | 181967 | 85475 240886 | 31340 16620 372237 22.4 | 5.573 % | c | 182118 | 85475 240886 | 34474 16771 374143 22.3 | 5.573 % | c | 182343 | 85447 240824 | 37921 16995 377444 22.2 | 5.605 % | c | 182681 | 85447 240824 | 41713 17333 387124 22.3 | 5.605 % | c | 183187 | 85447 240824 | 45885 17839 401752 22.5 | 5.605 % | c | 183946 | 85447 240824 | 50473 18598 423950 22.8 | 5.605 % | c | 185088 | 85447 240824 | 55520 19740 468638 23.7 | 5.605 % | c | 186796 | 85447 240824 | 61072 21448 518506 24.2 | 5.605 % | c | 189358 | 85447 240824 | 67180 24010 585663 24.4 | 5.605 % | c | 193203 | 85447 240824 | 73898 27855 694448 24.9 | 5.605 % | c | 198969 | 85447 240824 | 81288 33621 918948 27.3 | 5.605 % | c | 207618 | 85256 240390 | 89416 42262 1223144 28.9 | 5.797 % | c ============================================================================== c [1mFound solution: -985507[0m c ---[ 0]---> Sorter-cost: 1475 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 210921 | 88674 248407 | 29558 45565 1348924 29.6 | 5.797 % | c | 211022 | 88674 248407 | 32513 18678 465794 24.9 | 5.537 % | c | 211173 | 88636 248321 | 35765 18826 467473 24.8 | 5.579 % | c | 211400 | 88636 248321 | 39341 19053 472963 24.8 | 5.579 % | c | 211737 | 88636 248321 | 43275 19390 481019 24.8 | 5.579 % | c | 212245 | 88636 248321 | 47603 19898 493299 24.8 | 5.579 % | c | 213006 | 88636 248321 | 52363 20659 507992 24.6 | 5.579 % | c | 214146 | 88636 248321 | 57600 21799 530936 24.4 | 5.579 % | c | 215854 | 88636 248321 | 63360 23507 592764 25.2 | 5.579 % | c | 218416 | 88636 248321 | 69696 26069 686338 26.3 | 5.579 % | c | 222262 | 88636 248321 | 76665 29915 777069 26.0 | 5.579 % | c | 228029 | 88619 248278 | 84332 35679 1095746 30.7 | 5.594 % | c | 236679 | 88554 248132 | 92765 44324 1519219 34.3 | 5.663 % | c ============================================================================== c [1mFound solution: -1250179[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 238998 | 88640 248382 | 29546 46642 1589626 34.1 | 5.663 % | c | 239098 | 88640 248382 | 32500 18685 577923 30.9 | 5.660 % | c | 239248 | 88640 248382 | 35750 18835 581872 30.9 | 5.660 % | c | 239474 | 88640 248382 | 39325 19061 585881 30.7 | 5.660 % | c | 239811 | 88640 248382 | 43258 19398 590640 30.4 | 5.660 % | c | 240318 | 88640 248382 | 47584 19905 602929 30.3 | 5.660 % | c | 241078 | 88640 248382 | 52342 20665 618345 29.9 | 5.660 % | c | 242217 | 88640 248382 | 57576 21804 647814 29.7 | 5.660 % | c | 243926 | 88629 248358 | 63334 23512 688023 29.3 | 5.671 % | c | 246488 | 88629 248358 | 69667 26074 778690 29.9 | 5.671 % | c | 250332 | 88629 248358 | 76634 29918 879850 29.4 | 5.671 % | c | 256099 | 88629 248358 | 84298 35685 1120223 31.4 | 5.671 % | c ============================================================================== c [1mFound solution: -1250566[0m c ---[ 0]---> Sorter-cost: 21 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 260603 | 88627 248370 | 29542 40188 1273799 31.7 | 5.671 % | c | 260703 | 88627 248370 | 32496 17929 466945 26.0 | 5.695 % | c | 260853 | 88627 248370 | 35745 18079 469576 26.0 | 5.695 % | c | 261079 | 88627 248370 | 39320 18305 471205 25.7 | 5.695 % | c | 261416 | 88627 248370 | 43252 18642 475550 25.5 | 5.695 % | c | 261922 | 88627 248370 | 47577 19148 484301 25.3 | 5.695 % | c | 262681 | 88627 248370 | 52335 19907 499178 25.1 | 5.695 % | c | 263820 | 88627 248370 | 57569 21046 529981 25.2 | 5.695 % | c | 265529 | 88627 248370 | 63325 22755 588875 25.9 | 5.695 % | c | 268094 | 88587 248283 | 69658 25319 682037 26.9 | 5.745 % | c | 271939 | 88587 248283 | 76624 29164 823285 28.2 | 5.745 % | c | 277705 | 88587 248283 | 84286 34930 1015111 29.1 | 5.745 % | c ============================================================================== c [1mFound solution: -8102161[0m c ---[ 0]---> Sorter-cost: 1730 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 279952 | 92764 258060 | 30921 37166 1138664 30.6 | 5.745 % | c | 280052 | 92764 258060 | 34013 17396 473610 27.2 | 5.671 % | c | 280203 | 92764 258060 | 37414 17547 475646 27.1 | 5.671 % | c | 280428 | 92114 256038 | 41155 17356 470073 27.1 | 6.060 % | c | 280767 | 91422 254488 | 45271 17348 459091 26.5 | 6.724 % | c | 281274 | 91422 254488 | 49798 17855 469409 26.3 | 6.724 % | c | 282033 | 91422 254488 | 54778 18614 481414 25.9 | 6.724 % | c | 283173 | 91422 254488 | 60256 19754 537640 27.2 | 6.724 % | c | 284881 | 91422 254488 | 66281 21462 581025 27.1 | 6.724 % | c | 287446 | 91422 254488 | 72910 24027 679689 28.3 | 6.724 % | c | 291290 | 91422 254488 | 80201 27871 916008 32.9 | 6.724 % | c ============================================================================== c [1mFound solution: -8226529[0m c ---[ 0]---> Sorter-cost: 1476 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 296289 | 94872 262566 | 31624 32870 1093833 33.3 | 6.724 % | c | 296390 | 94872 262566 | 34786 32971 1095499 33.2 | 6.442 % | c | 296540 | 94656 261853 | 38265 33102 1098714 33.2 | 6.521 % | c | 296765 | 94621 261777 | 42091 33323 1101916 33.1 | 6.556 % | c | 297102 | 94621 261777 | 46300 33660 1109662 33.0 | 6.556 % | c | 297611 | 94289 260680 | 50930 34124 1124033 32.9 | 6.715 % | c | 298370 | 94289 260680 | 56023 34883 1150591 33.0 | 6.715 % | c | 299509 | 94282 260665 | 61626 36021 1184935 32.9 | 6.721 % | c | 301218 | 94282 260665 | 67788 37730 1250596 33.1 | 6.721 % | c | 303781 | 94260 260617 | 74567 40291 1396153 34.7 | 6.742 % | c | 307625 | 94245 260584 | 82024 44133 1522088 34.5 | 6.756 % | c | 313391 | 94245 260584 | 90226 49899 1679357 33.7 | 6.756 % | c ============================================================================== c [1mFound solution: -8579837[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 316137 | 94305 260762 | 31435 52645 1759724 33.4 | 6.756 % | c | 316237 | 94305 260762 | 34578 19181 391864 20.4 | 6.754 % | c | 316388 | 94305 260762 | 38036 19332 394613 20.4 | 6.754 % | c | 316613 | 94305 260762 | 41839 19557 398258 20.4 | 6.754 % | c | 316951 | 94305 260762 | 46023 19895 405540 20.4 | 6.754 % | c | 317457 | 94305 260762 | 50626 20401 416403 20.4 | 6.754 % | c | 318216 | 94305 260762 | 55689 21160 436357 20.6 | 6.754 % | c | 319356 | 94305 260762 | 61257 22300 459627 20.6 | 6.754 % | c | 321064 | 94305 260762 | 67383 24008 504516 21.0 | 6.754 % | c | 323626 | 94305 260762 | 74122 26570 567129 21.3 | 6.754 % | c | 327471 | 94305 260762 | 81534 30415 688826 22.6 | 6.754 % | c | 333238 | 94305 260762 | 89687 36182 1067582 29.5 | 6.754 % | c | 341887 | 94301 260753 | 98656 44830 1531878 34.2 | 6.757 % | c ============================================================================== c [1mFound solution: -8621307[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 346370 | 94314 260801 | 31438 49313 1675513 34.0 | 6.757 % | c | 346472 | 94314 260801 | 34581 18775 608700 32.4 | 6.759 % | c | 346622 | 94314 260801 | 38039 18925 611848 32.3 | 6.759 % | c | 346847 | 94314 260801 | 41843 19150 615641 32.1 | 6.759 % | c | 347185 | 94314 260801 | 46028 19488 628568 32.3 | 6.759 % | c | 347694 | 94314 260801 | 50631 19997 638032 31.9 | 6.759 % | c | 348453 | 94314 260801 | 55694 20756 655512 31.6 | 6.759 % | c | 349592 | 94273 260710 | 61263 21894 679836 31.1 | 6.800 % | c | 351302 | 94273 260710 | 67390 23604 722415 30.6 | 6.800 % | c | 353866 | 94237 260630 | 74129 26166 803378 30.7 | 6.834 % | c | 357711 | 94233 260621 | 81542 30010 913378 30.4 | 6.838 % | c | 363477 | 94231 260615 | 89696 35768 1080197 30.2 | 6.841 % | c ============================================================================== c [1mFound solution: -8666624[0m c ---[ 0]---> Sorter-cost: 18 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 368574 | 94286 260753 | 31428 40863 1214975 29.7 | 6.841 % | c | 368674 | 94286 260753 | 34570 18249 348384 19.1 | 6.855 % | c | 368825 | 94286 260753 | 38027 18400 350111 19.0 | 6.855 % | c | 369050 | 94286 260753 | 41830 18625 353652 19.0 | 6.855 % | c | 369391 | 94286 260753 | 46013 18966 358755 18.9 | 6.855 % | c | 369898 | 94286 260753 | 50615 19473 366573 18.8 | 6.855 % | c | 370657 | 94271 260719 | 55676 20230 407843 20.2 | 6.869 % | c | 371796 | 94271 260719 | 61244 21369 439731 20.6 | 6.869 % | c | 373504 | 94271 260719 | 67368 23077 478415 20.7 | 6.869 % | c | 376067 | 94271 260719 | 74105 25640 548309 21.4 | 6.869 % | c | 379912 | 94271 260719 | 81516 29485 684383 23.2 | 6.869 % | c | 385678 | 94177 260508 | 89667 35249 881979 25.0 | 6.955 % | c | 394328 | 94133 260409 | 98634 43896 1155863 26.3 | 7.000 % | c ============================================================================== c [1mFound solution: -8700288[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 397896 | 94145 260445 | 31381 47464 1340605 28.2 | 7.000 % | c | 397996 | 94145 260445 | 34519 19017 485826 25.5 | 7.001 % | c | 398147 | 94145 260445 | 37971 19168 487970 25.5 | 7.001 % | c | 398372 | 94145 260445 | 41768 19393 491026 25.3 | 7.001 % | c | 398709 | 94145 260445 | 45944 19730 495225 25.1 | 7.001 % | c | 399217 | 94145 260445 | 50539 20238 507093 25.1 | 7.001 % | c | 399978 | 94145 260445 | 55593 20999 526948 25.1 | 7.001 % | c | 401118 | 94042 260216 | 61152 22135 559086 25.3 | 7.098 % | c | 402827 | 94027 260165 | 67267 23836 606749 25.5 | 7.105 % | c | 405391 | 94027 260165 | 73994 26400 701319 26.6 | 7.105 % | c ============================================================================== c [1mFound solution: -8715502[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 408018 | 94049 260213 | 31349 29027 797749 27.5 | 7.105 % | c | 408122 | 94049 260213 | 34483 29131 800660 27.5 | 7.106 % | c | 408272 | 94049 260213 | 37932 29281 802369 27.4 | 7.106 % | c | 408499 | 94049 260213 | 41725 29508 805642 27.3 | 7.106 % | c | 408836 | 94049 260213 | 45898 29845 812759 27.2 | 7.106 % | c | 409342 | 94049 260213 | 50487 30351 828341 27.3 | 7.106 % | c | 410102 | 94049 260213 | 55536 31111 859300 27.6 | 7.106 % | c | 411241 | 94049 260213 | 61090 32250 886086 27.5 | 7.106 % | c | 412949 | 94049 260213 | 67199 33958 929880 27.4 | 7.106 % | c | 415512 | 94049 260213 | 73919 36521 999541 27.4 | 7.106 % | c ============================================================================== c [1mFound solution: -8721144[0m c ---[ 0]---> Sorter-cost: 18 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 419239 | 94090 260314 | 31363 40248 1112393 27.6 | 7.106 % | c | 419340 | 94090 260314 | 34499 19679 377827 19.2 | 7.104 % | c | 419491 | 94090 260314 | 37949 19830 380335 19.2 | 7.104 % | c | 419716 | 94090 260314 | 41744 20055 382864 19.1 | 7.104 % | c | 420053 | 94090 260314 | 45918 20392 388991 19.1 | 7.104 % | c | 420560 | 94090 260314 | 50510 20899 400656 19.2 | 7.104 % | c | 421320 | 94090 260314 | 55561 21659 416263 19.2 | 7.104 % | c | 422459 | 94090 260314 | 61117 22798 440616 19.3 | 7.104 % | c | 424167 | 94090 260314 | 67229 24506 483311 19.7 | 7.104 % | c | 426729 | 94083 260298 | 73952 27067 561312 20.7 | 7.111 % | c | 430575 | 94083 260298 | 81347 30913 676503 21.9 | 7.111 % | c | 436341 | 94083 260298 | 89482 36679 849719 23.2 | 7.111 % | c ============================================================================== c [1mFound solution: -8888309[0m c ---[ 0]---> Sorter-cost: 19 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 439505 | 94108 260358 | 31369 39843 959472 24.1 | 7.111 % | c | 439607 | 94108 260358 | 34505 20024 409922 20.5 | 7.112 % | c | 439759 | 94108 260358 | 37956 20176 412969 20.5 | 7.112 % | c | 439984 | 94108 260358 | 41752 20401 416435 20.4 | 7.112 % | c | 440321 | 94108 260358 | 45927 20738 422538 20.4 | 7.112 % | c | 440827 | 94093 260307 | 50520 21243 433245 20.4 | 7.119 % | c | 441587 | 94093 260307 | 55572 22003 450068 20.5 | 7.119 % | c | 442726 | 94093 260307 | 61129 23142 476740 20.6 | 7.119 % | c | 444434 | 94082 260282 | 67242 24848 526243 21.2 | 7.129 % | c | 446996 | 94082 260282 | 73966 27410 610930 22.3 | 7.129 % | c | 450841 | 94082 260282 | 81363 31255 744432 23.8 | 7.129 % | c | 456607 | 94041 260191 | 89499 37018 925105 25.0 | 7.167 % | c ============================================================================== c [1mFound solution: -8888600[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 462336 | 93972 259930 | 31324 41926 1165540 27.8 | 7.167 % | c | 462437 | 93972 259930 | 34456 20103 487376 24.2 | 7.185 % | c | 462588 | 93935 259802 | 37902 20249 490451 24.2 | 7.196 % | c | 462813 | 93935 259802 | 41692 20474 496191 24.2 | 7.196 % | c | 463151 | 93935 259802 | 45861 20812 502342 24.1 | 7.196 % | c | 463657 | 93935 259802 | 50447 21318 521851 24.5 | 7.196 % | c | 464417 | 93723 259120 | 55492 22068 535358 24.3 | 7.295 % | c | 465556 | 93723 259120 | 61041 23207 563353 24.3 | 7.295 % | c | 467265 | 93723 259120 | 67145 24916 633466 25.4 | 7.295 % | c | 469827 | 93673 259002 | 73860 27473 704301 25.6 | 7.340 % | c ============================================================================== c [1mFound solution: -8890619[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 470924 | 93689 259039 | 31229 28570 728321 25.5 | 7.340 % | c | 471024 | 93689 259039 | 34351 28670 730301 25.5 | 7.341 % | c | 471174 | 93689 259039 | 37787 28820 732903 25.4 | 7.341 % | c | 471399 | 93689 259039 | 41565 29045 736661 25.4 | 7.341 % | c | 471736 | 93689 259039 | 45722 29382 741221 25.2 | 7.341 % | c | 472242 | 93689 259039 | 50294 29888 756252 25.3 | 7.341 % | c | 473002 | 93689 259039 | 55324 30648 769765 25.1 | 7.341 % | c | 474144 | 93678 259014 | 60856 31788 802743 25.3 | 7.351 % | c | 475852 | 93678 259014 | 66942 33496 860503 25.7 | 7.351 % | c | 478414 | 93678 259014 | 73636 36058 941131 26.1 | 7.351 % | c | 482260 | 93678 259014 | 80999 39904 1112521 27.9 | 7.351 % | c | 488028 | 93678 259014 | 89099 45672 1371593 30.0 | 7.351 % | c | 496677 | 93553 258574 | 98009 54285 1904144 35.1 | 7.386 % | c ============================================================================== c [1mFound solution: -8896763[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 509030 | 93552 258575 | 31184 66637 2470886 37.1 | 7.386 % | c | 509130 | 93552 258575 | 34302 19357 590982 30.5 | 7.398 % | c | 509280 | 92716 256609 | 37732 19482 594057 30.5 | 8.177 % | c | 509505 | 92716 256609 | 41505 19707 598648 30.4 | 8.177 % | c | 509844 | 92716 256609 | 45656 20046 612256 30.5 | 8.177 % | c | 510350 | 92701 256574 | 50222 20551 622163 30.3 | 8.195 % | c | 511109 | 92701 256574 | 55244 21310 635254 29.8 | 8.195 % | c | 512248 | 92701 256574 | 60768 22449 653138 29.1 | 8.195 % | c | 513959 | 92692 256543 | 66845 24159 690596 28.6 | 8.198 % | c | 516521 | 92677 256510 | 73530 26720 763545 28.6 | 8.219 % | c | 520366 | 92677 256510 | 80883 30565 862565 28.2 | 8.219 % | c | 526132 | 92677 256510 | 88971 36331 1142403 31.4 | 8.219 % | c ============================================================================== c [1mFound solution: -9200016[0m c ---[ 0]---> Sorter-cost: 1534 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 526781 | 96289 264961 | 32096 36980 1159724 31.4 | 8.219 % | c | 526883 | 96289 264961 | 35305 17263 451541 26.2 | 7.923 % | c | 527033 | 96289 264961 | 38836 17413 454651 26.1 | 7.923 % | c | 527259 | 96289 264961 | 42719 17639 457788 26.0 | 7.923 % | c | 527596 | 96289 264961 | 46991 17976 465944 25.9 | 7.923 % | c | 528102 | 96289 264961 | 51690 18482 476186 25.8 | 7.923 % | c | 528861 | 96289 264961 | 56860 19241 495983 25.8 | 7.923 % | c | 530000 | 96289 264961 | 62546 20380 516998 25.4 | 7.923 % | c | 531710 | 96281 264943 | 68800 22089 560746 25.4 | 7.930 % | c | 534272 | 96281 264943 | 75680 24651 636399 25.8 | 7.930 % | c | 538116 | 96281 264943 | 83248 28495 759238 26.6 | 7.930 % | c | 543882 | 95856 263560 | 91573 34196 953022 27.9 | 8.153 % | c ============================================================================== c [1mFound solution: -9314760[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 549997 | 96012 263940 | 32004 40311 1157113 28.7 | 8.153 % | c | 550098 | 96012 263940 | 35204 18299 427370 23.4 | 8.133 % | c | 550249 | 96012 263940 | 38724 18450 429122 23.3 | 8.133 % | c | 550476 | 96012 263940 | 42597 18677 433784 23.2 | 8.133 % | c | 550814 | 96012 263940 | 46857 19015 438516 23.1 | 8.133 % | c | 551320 | 96012 263940 | 51542 19521 449327 23.0 | 8.133 % | c | 552079 | 96003 263909 | 56697 20278 469871 23.2 | 8.136 % | c | 553218 | 96003 263909 | 62366 21417 497639 23.2 | 8.136 % | c | 554926 | 96003 263909 | 68603 23125 625749 27.1 | 8.136 % | c | 557488 | 96003 263909 | 75463 25687 698540 27.2 | 8.136 % | c | 561332 | 96003 263909 | 83010 29531 843454 28.6 | 8.136 % | c ============================================================================== c [1mFound solution: -9470115[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 566001 | 96013 263941 | 32004 34198 1021808 29.9 | 8.136 % | c | 566101 | 96013 263941 | 35204 34298 1023488 29.8 | 8.141 % | c | 566251 | 95996 263904 | 38724 34445 1025423 29.8 | 8.158 % | c | 566479 | 95996 263904 | 42597 34673 1033404 29.8 | 8.158 % | c | 566816 | 95973 263853 | 46857 35005 1044773 29.8 | 8.177 % | c | 567323 | 95973 263853 | 51542 35512 1059645 29.8 | 8.177 % | c | 568082 | 95973 263853 | 56697 36271 1077196 29.7 | 8.177 % | c | 569223 | 95823 263343 | 62366 37389 1115322 29.8 | 8.249 % | c | 570931 | 95823 263343 | 68603 39097 1159965 29.7 | 8.250 % | c | 573495 | 95823 263343 | 75463 41661 1219947 29.3 | 8.249 % | c ============================================================================== c [1mFound solution: -9470836[0m c ---[ 0]---> Sorter-cost: 18 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 576918 | 95842 263390 | 31947 45084 1348356 29.9 | 8.249 % | c | 577018 | 95827 263356 | 35141 20251 408082 20.2 | 8.263 % | c | 577171 | 95827 263356 | 38655 20404 411066 20.1 | 8.263 % | c | 577396 | 95827 263356 | 42521 20629 415499 20.1 | 8.263 % | c | 577734 | 95827 263356 | 46773 20967 420850 20.1 | 8.263 % | c | 578241 | 95827 263356 | 51450 21474 436686 20.3 | 8.263 % | c | 579001 | 95799 263294 | 56596 22231 457648 20.6 | 8.290 % | c | 580140 | 95799 263294 | 62255 23370 493047 21.1 | 8.290 % | c | 581849 | 95799 263294 | 68481 25079 535190 21.3 | 8.290 % | c | 584411 | 95799 263294 | 75329 27641 625970 22.6 | 8.290 % | c | 588255 | 95799 263294 | 82862 31485 766418 24.3 | 8.290 % | c ============================================================================== c [1mFound solution: -9470975[0m c ---[ 0]---> Sorter-cost: 19 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 592741 | 95794 263290 | 31931 35969 932720 25.9 | 8.290 % | c | 592841 | 95794 263290 | 35124 18085 420838 23.3 | 8.314 % | c | 592992 | 95794 263290 | 38636 18236 426139 23.4 | 8.314 % | c | 593218 | 95794 263290 | 42500 18462 428483 23.2 | 8.314 % | c | 593555 | 95794 263290 | 46750 18799 433933 23.1 | 8.314 % | c | 594063 | 95794 263290 | 51425 19307 442242 22.9 | 8.314 % | c | 594822 | 95794 263290 | 56567 20066 456127 22.7 | 8.314 % | c | 595961 | 95794 263290 | 62224 21205 493014 23.2 | 8.314 % | c | 597669 | 95794 263290 | 68446 22913 529113 23.1 | 8.314 % | c | 600232 | 95794 263290 | 75291 25476 625995 24.6 | 8.314 % | c | 604076 | 95794 263290 | 82820 29320 737591 25.2 | 8.314 % | c | 609842 | 95794 263290 | 91102 35086 914441 26.1 | 8.314 % | c | 618492 | 95739 263167 | 100213 43735 1244184 28.4 | 8.360 % | c ============================================================================== c [1mFound solution: -9476276[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 622869 | 95740 263140 | 31913 48101 1408379 29.3 | 8.360 % | c | 622969 | 95740 263140 | 35104 21290 503749 23.7 | 8.373 % | c | 623122 | 95740 263140 | 38614 21443 506578 23.6 | 8.373 % | c | 623348 | 95740 263140 | 42476 21669 511706 23.6 | 8.373 % | c | 623686 | 95740 263140 | 46723 22007 518971 23.6 | 8.373 % | c | 624192 | 95740 263140 | 51396 22513 529490 23.5 | 8.373 % | c | 624953 | 95662 262877 | 56535 23248 551082 23.7 | 8.432 % | c | 626092 | 95662 262877 | 62189 24387 570853 23.4 | 8.432 % | c | 627802 | 95662 262877 | 68408 26097 627074 24.0 | 8.432 % | c | 630366 | 95662 262877 | 75249 28661 693960 24.2 | 8.432 % | c | 634210 | 95302 262056 | 82774 32459 809163 24.9 | 8.766 % | c | 639978 | 95266 261974 | 91051 38224 973176 25.5 | 8.802 % | c | 648627 | 95266 261974 | 100156 46873 1451359 31.0 | 8.802 % | c ============================================================================== c [1mFound solution: -9493755[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 661033 | 95230 261876 | 31743 59275 1835451 31.0 | 8.802 % | c | 661133 | 95230 261876 | 34917 22481 439504 19.6 | 8.847 % | c | 661283 | 95230 261876 | 38409 22631 442076 19.5 | 8.847 % | c | 661508 | 95230 261876 | 42249 22856 445755 19.5 | 8.847 % | c | 661847 | 95230 261876 | 46474 23195 452181 19.5 | 8.847 % | c | 662355 | 95215 261842 | 51122 23702 462012 19.5 | 8.860 % | c | 663115 | 95215 261842 | 56234 24462 483501 19.8 | 8.860 % | c | 664255 | 95215 261842 | 61858 25602 507986 19.8 | 8.860 % | c | 665963 | 95215 261842 | 68043 27310 569362 20.8 | 8.860 % | c | 668525 | 95215 261842 | 74848 29872 658470 22.0 | 8.860 % | c | 672369 | 95215 261842 | 82333 33716 797185 23.6 | 8.860 % | c | 678135 | 95193 261790 | 90566 39480 969658 24.6 | 8.880 % | c ============================================================================== c [1mFound solution: -9494778[0m c ---[ 0]---> Sorter-cost: 18 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 685880 | 95202 261820 | 31734 47225 1252332 26.5 | 8.880 % | c | 685980 | 95202 261820 | 34907 20639 439584 21.3 | 8.882 % | c | 686130 | 95202 261820 | 38398 20789 441988 21.3 | 8.882 % | c | 686355 | 95168 261743 | 42237 21010 446059 21.2 | 8.918 % | c | 686692 | 95168 261743 | 46461 21347 453396 21.2 | 8.918 % | c | 687198 | 95168 261743 | 51107 21853 467217 21.4 | 8.918 % | c | 687957 | 95168 261743 | 56218 22612 483850 21.4 | 8.918 % | c | 689096 | 95168 261743 | 61840 23751 524878 22.1 | 8.918 % | c | 690804 | 95168 261743 | 68024 25459 559745 22.0 | 8.918 % | c | 693369 | 95168 261743 | 74827 28024 672176 24.0 | 8.918 % | c | 697214 | 95168 261743 | 82309 31869 776133 24.4 | 8.918 % | c | 702981 | 95168 261743 | 90540 37636 1003679 26.7 | 8.918 % | c | 711632 | 95168 261743 | 99594 46287 1344578 29.0 | 8.918 % | c | 724608 | 95142 261667 | 109554 59260 1842718 31.1 | 8.934 % | c ============================================================================== c [1mFound solution: -9501954[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 730974 | 95157 261705 | 31719 65626 2060488 31.4 | 8.934 % | c | 731075 | 95157 261705 | 34890 21355 453278 21.2 | 8.936 % | c | 731226 | 95157 261705 | 38379 21506 456685 21.2 | 8.936 % | c | 731451 | 95157 261705 | 42217 21731 461020 21.2 | 8.936 % | c | 731789 | 95157 261705 | 46439 22069 466252 21.1 | 8.936 % | c | 732295 | 95157 261705 | 51083 22575 474792 21.0 | 8.936 % | c | 733055 | 95157 261705 | 56192 23335 494451 21.2 | 8.936 % | c | 734194 | 95157 261705 | 61811 24474 523296 21.4 | 8.936 % | c | 735902 | 95157 261705 | 67992 26182 571285 21.8 | 8.936 % | c | 738469 | 95157 261705 | 74791 28749 670427 23.3 | 8.936 % | c | 742313 | 94838 260975 | 82270 32579 760477 23.3 | 9.198 % | c ============================================================================== c [1mFound solution: -9501981[0m c ---[ 0]---> Sorter-cost: 1677 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 743769 | 98985 270675 | 32995 34035 800957 23.5 | 9.198 % | c | 743869 | 98985 270675 | 36294 34135 802938 23.5 | 8.815 % | c | 744021 | 98985 270675 | 39923 34287 805830 23.5 | 8.815 % | c | 744246 | 98985 270675 | 43916 34512 811167 23.5 | 8.815 % | c | 744585 | 98985 270675 | 48307 34851 819102 23.5 | 8.815 % | c | 745092 | 98985 270675 | 53138 35358 830217 23.5 | 8.815 % | c | 745852 | 98985 270675 | 58452 36118 849843 23.5 | 8.815 % | c | 746991 | 98985 270675 | 64297 37257 870206 23.4 | 8.815 % | c | 748699 | 98985 270675 | 70727 38965 961961 24.7 | 8.815 % | c ============================================================================== c [1mFound solution: -9502326[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 749602 | 99017 270776 | 33005 39868 994491 24.9 | 8.815 % | c | 749702 | 99017 270776 | 36305 20034 370604 18.5 | 8.814 % | c | 749853 | 99017 270776 | 39936 20185 375652 18.6 | 8.814 % | c | 750079 | 99017 270776 | 43929 20411 379317 18.6 | 8.814 % | c | 750416 | 99017 270776 | 48322 20748 386919 18.6 | 8.814 % | c | 750925 | 99017 270776 | 53154 21257 409609 19.3 | 8.814 % | c | 751684 | 99017 270776 | 58470 22016 435978 19.8 | 8.814 % | c | 752823 | 99017 270776 | 64317 23155 476762 20.6 | 8.814 % | c | 754531 | 99017 270776 | 70749 24863 543855 21.9 | 8.814 % | c | 757093 | 99017 270776 | 77824 27425 633931 23.1 | 8.814 % | c | 760937 | 99017 270776 | 85606 31269 749382 24.0 | 8.814 % | c | 766704 | 99017 270776 | 94167 37036 938955 25.4 | 8.814 % | c ============================================================================== c [1mFound solution: -9502475[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 775324 | 99037 270825 | 33012 45656 1347798 29.5 | 8.814 % | c | 775424 | 99037 270825 | 36313 20610 565744 27.4 | 8.814 % | c | 775575 | 99037 270825 | 39944 20761 568050 27.4 | 8.814 % | c | 775800 | 99037 270825 | 43938 20986 572986 27.3 | 8.814 % | c | 776137 | 99037 270825 | 48332 21323 578512 27.1 | 8.814 % | c | 776644 | 99037 270825 | 53166 21830 588540 27.0 | 8.814 % | c | 777403 | 99037 270825 | 58482 22589 606313 26.8 | 8.814 % | c | 778542 | 99037 270825 | 64331 23728 635509 26.8 | 8.814 % | c ============================================================================== c [1mFound solution: -9918740[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 779920 | 99094 270967 | 33031 25106 679017 27.0 | 8.814 % | c | 780020 | 99094 270967 | 36334 25206 680342 27.0 | 8.811 % | c | 780173 | 99094 270967 | 39967 25359 683377 26.9 | 8.811 % | c | 780399 | 99094 270967 | 43964 25585 686958 26.9 | 8.811 % | c | 780736 | 99094 270967 | 48360 25922 696648 26.9 | 8.811 % | c | 781242 | 99094 270967 | 53196 26428 708915 26.8 | 8.811 % | c | 782001 | 99094 270967 | 58516 27187 724058 26.6 | 8.811 % | c | 783141 | 99094 270967 | 64368 28327 752067 26.5 | 8.811 % | c | 784850 | 99094 270967 | 70804 30036 804332 26.8 | 8.811 % | c | 787413 | 99081 270939 | 77885 32598 868130 26.6 | 8.823 % | c | 791258 | 99081 270939 | 85673 36443 967300 26.5 | 8.823 % | c | 797024 | 99081 270939 | 94241 42209 1140218 27.0 | 8.823 % | c | 805673 | 99081 270939 | 103665 50858 1485290 29.2 | 8.823 % | c | 818647 | 99081 270939 | 114031 63832 1944233 30.5 | 8.823 % | c ============================================================================== c [1mFound solution: -9919741[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 822574 | 99094 270971 | 33031 67759 2061079 30.4 | 8.823 % | c | 822674 | 99094 270971 | 36334 22167 507287 22.9 | 8.825 % | c | 822825 | 99094 270971 | 39967 22318 510839 22.9 | 8.825 % | c | 823051 | 99094 270971 | 43964 22544 516663 22.9 | 8.825 % | c | 823388 | 99049 270872 | 48360 22877 522572 22.8 | 8.865 % | c | 823895 | 99049 270872 | 53196 23384 537790 23.0 | 8.865 % | c | 824655 | 99049 270872 | 58516 24144 559231 23.2 | 8.865 % | c | 825794 | 99049 270872 | 64368 25283 599732 23.7 | 8.865 % | c | 827502 | 99049 270872 | 70804 26991 675678 25.0 | 8.865 % | c | 830064 | 99049 270872 | 77885 29553 784705 26.6 | 8.865 % | c | 833909 | 99049 270872 | 85673 33398 901353 27.0 | 8.865 % | c | 839675 | 99049 270872 | 94241 39164 1083049 27.7 | 8.865 % | c | 848324 | 99049 270872 | 103665 47813 1332699 27.9 | 8.865 % | c ============================================================================== c [1mFound solution: -9961736[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 851725 | 99056 270899 | 33018 51214 1443695 28.2 | 8.865 % | c | 851825 | 99056 270899 | 36319 21257 408696 19.2 | 8.867 % | c | 851975 | 99056 270899 | 39951 21407 410379 19.2 | 8.867 % | c | 852200 | 99056 270899 | 43946 21632 413747 19.1 | 8.867 % | c | 852538 | 99056 270899 | 48341 21970 421279 19.2 | 8.867 % | c | 853044 | 99056 270899 | 53175 22476 430909 19.2 | 8.867 % | c | 853803 | 99056 270899 | 58493 23235 463081 19.9 | 8.867 % | c | 854943 | 99056 270899 | 64342 24375 501805 20.6 | 8.867 % | c | 856652 | 99056 270899 | 70777 26084 569058 21.8 | 8.867 % | c ============================================================================== c [1mFound solution: -10002683[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 858736 | 99125 271068 | 33041 28168 635190 22.6 | 8.867 % | c | 858836 | 99125 271068 | 36345 28268 638801 22.6 | 8.862 % | c | 858986 | 99125 271068 | 39979 28418 641441 22.6 | 8.862 % | c | 859211 | 99125 271068 | 43977 28643 645700 22.5 | 8.862 % | c | 859548 | 99125 271068 | 48375 28980 653529 22.6 | 8.862 % | c | 860054 | 99125 271068 | 53212 29486 668603 22.7 | 8.862 % | c | 860813 | 99125 271068 | 58534 30245 682079 22.6 | 8.862 % | c | 861953 | 99125 271068 | 64387 31385 721674 23.0 | 8.862 % | c | 863662 | 99125 271068 | 70826 33094 771522 23.3 | 8.862 % | c | 866224 | 99125 271068 | 77908 35656 852052 23.9 | 8.862 % | c | 870069 | 99125 271068 | 85699 39501 971737 24.6 | 8.862 % | c ============================================================================== c [1mFound solution: -10035469[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 873125 | 99137 271105 | 33045 42557 1059604 24.9 | 8.862 % | c | 873226 | 99137 271105 | 36349 20719 396117 19.1 | 8.863 % | c | 873377 | 99137 271105 | 39984 20870 398156 19.1 | 8.863 % | c | 873603 | 99137 271105 | 43982 21096 403534 19.1 | 8.863 % | c | 873940 | 99137 271105 | 48381 21433 410111 19.1 | 8.863 % | c | 874447 | 99137 271105 | 53219 21940 422166 19.2 | 8.863 % | c | 875210 | 99137 271105 | 58541 22703 436337 19.2 | 8.863 % | c | 876350 | 99137 271105 | 64395 23843 482989 20.3 | 8.863 % | c | 878058 | 99137 271105 | 70834 25551 523819 20.5 | 8.863 % | c | 880620 | 99137 271105 | 77918 28113 594466 21.1 | 8.863 % | c | 884466 | 99137 271105 | 85710 31959 693369 21.7 | 8.863 % | c | 890232 | 99137 271105 | 94281 37725 857953 22.7 | 8.863 % | c ============================================================================== c [1mFound solution: -10090748[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 893828 | 99140 271119 | 33046 41319 961598 23.3 | 8.863 % | c | 893930 | 99140 271119 | 36350 20576 363440 17.7 | 8.873 % | c | 894081 | 99140 271119 | 39985 20727 365566 17.6 | 8.873 % | c | 894307 | 99140 271119 | 43984 20953 370617 17.7 | 8.873 % | c | 894644 | 99140 271119 | 48382 21290 375940 17.7 | 8.873 % | c | 895151 | 99140 271119 | 53220 21797 388209 17.8 | 8.873 % | c | 895910 | 99140 271119 | 58543 22556 406229 18.0 | 8.873 % | c | 897050 | 99140 271119 | 64397 23696 434516 18.3 | 8.873 % | c | 898758 | 99140 271119 | 70837 25404 487591 19.2 | 8.873 % | c | 901321 | 99131 271088 | 77920 27964 555404 19.9 | 8.876 % | c | 905165 | 99131 271088 | 85712 31808 659322 20.7 | 8.876 % | c | 910931 | 99131 271088 | 94284 37574 867744 23.1 | 8.876 % | c | 919583 | 99131 271088 | 103712 46226 1215174 26.3 | 8.876 % | c ============================================================================== c [1mFound solution: -10356985[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 929616 | 99105 271033 | 33035 56252 1553529 27.6 | 8.876 % | c | 929716 | 99105 271033 | 36338 20717 461159 22.3 | 8.912 % | c | 929869 | 99105 271033 | 39972 20870 464338 22.2 | 8.912 % | c | 930095 | 99105 271033 | 43969 21096 467807 22.2 | 8.912 % | c | 930432 | 99105 271033 | 48366 21433 474300 22.1 | 8.912 % | c | 930938 | 99105 271033 | 53203 21939 491435 22.4 | 8.912 % | c | 931697 | 99105 271033 | 58523 22698 509153 22.4 | 8.912 % | c | 932836 | 97683 266368 | 64375 21380 476818 22.3 | 9.616 % | c | 934545 | 97683 266368 | 70813 23089 525273 22.7 | 9.616 % | c | 937109 | 97596 266172 | 77894 25647 592957 23.1 | 9.693 % | c | 940953 | 97594 266166 | 85684 29470 694254 23.6 | 9.696 % | c | 946719 | 97578 266129 | 94252 35234 863120 24.5 | 9.715 % | c | 955369 | 97578 266129 | 103677 43884 1109394 25.3 | 9.715 % | c ============================================================================== c [1mFound solution: -10383617[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 968226 | 97577 266134 | 32525 56740 1526832 26.9 | 9.715 % | c | 968327 | 97577 266134 | 35777 21844 442384 20.3 | 9.728 % | c | 968478 | 97577 266134 | 39355 21995 445335 20.2 | 9.728 % | c | 968703 | 97577 266134 | 43290 22220 450421 20.3 | 9.728 % | c | 969040 | 97577 266134 | 47619 22557 455852 20.2 | 9.728 % | c | 969547 | 97577 266134 | 52381 23064 473916 20.5 | 9.728 % | c | 970306 | 97577 266134 | 57620 23823 491179 20.6 | 9.728 % | c | 971445 | 97577 266134 | 63382 24962 538852 21.6 | 9.728 % | c | 973153 | 97577 266134 | 69720 26670 589020 22.1 | 9.728 % | c | 975718 | 97577 266134 | 76692 29235 667456 22.8 | 9.728 % | c | 979563 | 97577 266134 | 84361 33080 807010 24.4 | 9.728 % | c | 985329 | 97577 266134 | 92797 38846 967628 24.9 | 9.728 % | c | 993978 | 97577 266134 | 102077 47495 1379611 29.0 | 9.728 % | c | 1006953 | 97577 266134 | 112285 60470 1951982 32.3 | 9.728 % | c | 1026415 | 97534 266039 | 123513 79926 2870638 35.9 | 9.765 % | c ============================================================================== c [1mFound solution: -10384638[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1047105 | 97551 266084 | 32517 100616 4010576 39.9 | 9.765 % | c | 1047205 | 97551 266084 | 35768 18945 775083 40.9 | 9.765 % | c | 1047356 | 97551 266084 | 39345 19096 777230 40.7 | 9.765 % | c | 1047582 | 97551 266084 | 43280 19322 781834 40.5 | 9.765 % | c | 1047919 | 97551 266084 | 47608 19659 788113 40.1 | 9.765 % | c | 1048426 | 97551 266084 | 52368 20166 796723 39.5 | 9.765 % | c | 1049185 | 97551 266084 | 57605 20925 809824 38.7 | 9.765 % | c | 1050324 | 97466 265878 | 63366 22048 836609 37.9 | 9.858 % | c | 1052033 | 97451 265844 | 69703 23756 873956 36.8 | 9.871 % | c | 1054596 | 97449 265840 | 76673 26318 925335 35.2 | 9.874 % | c | 1058440 | 97449 265840 | 84340 30162 1004658 33.3 | 9.874 % | c | 1064206 | 97449 265840 | 92774 35928 1126342 31.3 | 9.874 % | c | 1072855 | 97449 265840 | 102052 44577 1391482 31.2 | 9.874 % | c | 1085830 | 97449 265840 | 112257 57552 1896368 33.0 | 9.874 % | c ============================================================================== c [1mFound solution: -10395901[0m c ---[ 0]---> Sorter-cost: 97 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1094994 | 97535 266043 | 32511 66711 2214945 33.2 | 9.874 % | c | 1095094 | 97535 266043 | 35762 20013 520387 26.0 | 9.868 % | c | 1095246 | 97535 266043 | 39338 20165 522779 25.9 | 9.868 % | c | 1095471 | 97535 266043 | 43272 20390 526721 25.8 | 9.868 % | c | 1095810 | 97535 266043 | 47599 20729 533253 25.7 | 9.868 % | c | 1096316 | 97535 266043 | 52359 21235 541290 25.5 | 9.868 % | c | 1097076 | 97535 266043 | 57595 21995 558786 25.4 | 9.868 % | c | 1098215 | 97535 266043 | 63354 23134 586486 25.4 | 9.868 % | c | 1099923 | 97535 266043 | 69690 24842 623907 25.1 | 9.868 % | c | 1102485 | 97535 266043 | 76659 27404 733224 26.8 | 9.868 % | c | 1106329 | 97535 266043 | 84325 31248 859196 27.5 | 9.868 % | c | 1112097 | 97535 266043 | 92757 37016 1112222 30.0 | 9.868 % | c | 1120749 | 97500 265940 | 102033 45665 1345384 29.5 | 9.896 % | c ============================================================================== c [1mFound solution: -10435834[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1124102 | 97515 265980 | 32505 49018 1496273 30.5 | 9.896 % | c | 1124203 | 97515 265980 | 35755 21834 425313 19.5 | 9.897 % | c | 1124354 | 97515 265980 | 39331 21985 427883 19.5 | 9.897 % | c | 1124581 | 97515 265980 | 43264 22212 430749 19.4 | 9.897 % | c | 1124918 | 97460 265854 | 47590 22545 435949 19.3 | 9.953 % | c | 1125426 | 97460 265854 | 52349 23053 446208 19.4 | 9.953 % | c | 1126185 | 97460 265854 | 57584 23812 460776 19.4 | 9.953 % | c | 1127324 | 97460 265854 | 63343 24951 490716 19.7 | 9.953 % | c | 1129032 | 97460 265854 | 69677 26659 551183 20.7 | 9.953 % | c ============================================================================== c [1mFound solution: -11794676[0m c ---[ 0]---> Sorter-cost: 15 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1130356 | 97518 265991 | 32506 27983 588621 21.0 | 9.953 % | c | 1130456 | 97518 265991 | 35756 28083 590601 21.0 | 9.946 % | c | 1130607 | 97518 265991 | 39332 28234 593425 21.0 | 9.946 % | c | 1130833 | 97518 265991 | 43265 28460 597500 21.0 | 9.946 % | c | 1131172 | 97518 265991 | 47592 28799 603072 20.9 | 9.946 % | c | 1131678 | 97518 265991 | 52351 29305 611709 20.9 | 9.946 % | c | 1132438 | 96570 263842 | 57586 30015 633380 21.1 | 10.789 % | c | 1133577 | 96555 263808 | 63344 31153 656357 21.1 | 10.805 % | c | 1135286 | 91321 251443 | 69679 28960 592559 20.5 | 15.568 % | c ============================================================================== c [1mFound solution: -11805006[0m c ---[ 0]---> Sorter-cost: 1224 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1137351 | 93249 255997 | 31083 30861 670121 21.7 | 15.568 % | c | 1137452 | 93056 255351 | 34191 30817 669536 21.7 | 16.076 % | c | 1137602 | 93056 255351 | 37610 30967 672302 21.7 | 16.076 % | c | 1137830 | 92833 254599 | 41371 31039 672044 21.7 | 16.172 % | c | 1138167 | 92833 254599 | 45508 31376 680023 21.7 | 16.172 % | c | 1138673 | 92520 253569 | 50059 31300 681067 21.8 | 16.344 % | c | 1139432 | 92159 252501 | 55065 31772 685640 21.6 | 16.548 % | c | 1140571 | 91644 250827 | 60571 31524 671164 21.3 | 16.810 % | c | 1142280 | 91644 250827 | 66629 33233 738837 22.2 | 16.810 % | c ============================================================================== c [1mFound solution: -11810562[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1144659 | 91658 250875 | 30552 35612 800860 22.5 | 16.810 % | c | 1144760 | 88234 242916 | 33607 35508 796118 22.4 | 20.253 % | c | 1144911 | 88234 242916 | 36967 35659 800651 22.5 | 20.253 % | c | 1145136 | 88234 242916 | 40664 35884 805278 22.4 | 20.253 % | c | 1145476 | 88049 242381 | 44731 36190 809698 22.4 | 20.370 % | c | 1145982 | 88049 242381 | 49204 36696 826083 22.5 | 20.370 % | c | 1146742 | 87212 240433 | 54124 37373 849466 22.7 | 21.113 % | c | 1147881 | 87212 240433 | 59537 38512 901321 23.4 | 21.113 % | c | 1149589 | 85603 236636 | 65490 39958 938100 23.5 | 22.620 % | c | 1152151 | 85582 236561 | 72040 42505 1039150 24.4 | 22.632 % | c ============================================================================== c [1mFound solution: -11810566[0m c ---[ 0]---> Sorter-cost: 1837 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1155889 | 89766 246167 | 29922 46146 1211542 26.3 | 22.632 % | c | 1155989 | 89766 246167 | 32914 21056 486668 23.1 | 21.695 % | c | 1156139 | 89547 245492 | 36205 20984 487173 23.2 | 21.824 % | c | 1156366 | 89547 245492 | 39826 21211 493405 23.3 | 21.824 % | c | 1156703 | 89212 244368 | 43808 21476 498880 23.2 | 21.953 % | c | 1157210 | 89159 244181 | 48189 21940 514619 23.5 | 21.979 % | c | 1157970 | 88759 243011 | 53008 22668 535837 23.6 | 22.252 % | c | 1159109 | 88759 243011 | 58309 23807 582364 24.5 | 22.252 % | c | 1160817 | 88260 241728 | 64140 25466 648053 25.4 | 22.703 % | c | 1163380 | 88058 241077 | 70554 28009 753079 26.9 | 22.795 % | c | 1167227 | 87589 239655 | 77609 31808 851143 26.8 | 23.062 % | c ============================================================================== c [1mFound solution: -11811067[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1169670 | 87593 239687 | 29197 34245 931895 27.2 | 23.062 % | c | 1169770 | 87416 239101 | 32116 34282 931805 27.2 | 23.191 % | c | 1169921 | 87416 239101 | 35328 34433 935235 27.2 | 23.191 % | c | 1170146 | 87395 239030 | 38861 34655 940566 27.1 | 23.200 % | c | 1170484 | 87271 238605 | 42747 34917 950661 27.2 | 23.283 % | c | 1170990 | 87254 238546 | 47022 35420 961650 27.1 | 23.292 % | c | 1171750 | 87254 238546 | 51724 36180 989033 27.3 | 23.292 % | c | 1172893 | 87121 238153 | 56896 37269 1021896 27.4 | 23.361 % | c | 1174601 | 87121 238153 | 62586 38977 1067981 27.4 | 23.361 % | c ============================================================================== c [1mFound solution: -11829510[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1175835 | 87162 238263 | 29054 40200 1099898 27.4 | 23.361 % | c | 1175935 | 87162 238263 | 31959 20200 363469 18.0 | 23.355 % | c | 1176085 | 87162 238263 | 35155 20350 365140 17.9 | 23.355 % | c | 1176311 | 87162 238263 | 38670 20576 371623 18.1 | 23.355 % | c | 1176649 | 87162 238263 | 42537 20914 378074 18.1 | 23.355 % | c | 1177155 | 87162 238263 | 46791 21420 390340 18.2 | 23.355 % | c | 1177915 | 87082 237981 | 51470 22164 414093 18.7 | 23.384 % | c | 1179054 | 86810 237140 | 56618 23263 440872 19.0 | 23.553 % | c | 1180762 | 86810 237140 | 62279 24971 500301 20.0 | 23.553 % | c | 1183324 | 86791 237098 | 68507 27532 593995 21.6 | 23.568 % | c ============================================================================== c [1mFound solution: -11829548[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1185602 | 86802 237128 | 28934 29810 670718 22.5 | 23.568 % | c | 1185703 | 86802 237128 | 31827 29911 672475 22.5 | 23.566 % | c | 1185854 | 86802 237128 | 35010 30062 674852 22.4 | 23.566 % | c | 1186081 | 86802 237128 | 38511 30289 680560 22.5 | 23.566 % | c | 1186418 | 86802 237128 | 42362 30626 690629 22.6 | 23.566 % | c | 1186926 | 86802 237128 | 46598 31134 706594 22.7 | 23.566 % | c ============================================================================== c [1mFound solution: -11830019[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1187505 | 86813 237156 | 28937 31713 729344 23.0 | 23.566 % | c | 1187605 | 86813 237156 | 31830 31813 730795 23.0 | 23.564 % | c | 1187755 | 86813 237156 | 35013 31963 733645 23.0 | 23.564 % | c | 1187980 | 86813 237156 | 38515 32188 737947 22.9 | 23.564 % | c | 1188317 | 86813 237156 | 42366 32525 744189 22.9 | 23.564 % | c | 1188826 | 86813 237156 | 46603 33034 752944 22.8 | 23.564 % | c | 1189585 | 86813 237156 | 51263 33793 778897 23.0 | 23.564 % | c | 1190724 | 86813 237156 | 56390 34932 820877 23.5 | 23.564 % | c | 1192432 | 86813 237156 | 62029 36640 906092 24.7 | 23.564 % | c ============================================================================== c [1mFound solution: -11830110[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1193143 | 86828 237193 | 28942 37351 947660 25.4 | 23.564 % | c | 1193243 | 86828 237193 | 31836 18776 403216 21.5 | 23.561 % | c | 1193394 | 86828 237193 | 35019 18927 405350 21.4 | 23.561 % | c | 1193619 | 86828 237193 | 38521 19152 408518 21.3 | 23.561 % | c | 1193958 | 86828 237193 | 42373 19491 416451 21.4 | 23.561 % | c | 1194464 | 86828 237193 | 46611 19997 430086 21.5 | 23.561 % | c | 1195223 | 86754 236925 | 51272 20744 449415 21.7 | 23.596 % | c | 1196363 | 86625 236616 | 56399 21880 480085 21.9 | 23.710 % | c | 1198072 | 86625 236616 | 62039 23589 526181 22.3 | 23.710 % | c | 1200635 | 86614 236592 | 68243 26151 603001 23.1 | 23.719 % | c | 1204480 | 86614 236592 | 75068 29996 686594 22.9 | 23.719 % | c ============================================================================== c [1mFound solution: -11831691[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1209726 | 86179 235590 | 28726 35216 885313 25.1 | 23.719 % | c | 1209827 | 86179 235590 | 31598 35317 887076 25.1 | 24.114 % | c | 1209978 | 86167 235563 | 34758 35463 889381 25.1 | 24.128 % | c | 1210206 | 86167 235563 | 38234 35691 893975 25.0 | 24.128 % | c | 1210543 | 86167 235563 | 42057 36028 901331 25.0 | 24.128 % | c | 1211051 | 86167 235563 | 46263 36536 912818 25.0 | 24.128 % | c | 1211810 | 85224 233359 | 50889 37197 931812 25.1 | 24.956 % | c | 1212949 | 85224 233359 | 55978 38336 975249 25.4 | 24.956 % | c | 1214661 | 85051 232965 | 61576 40041 1031905 25.8 | 25.096 % | c | 1217223 | 84981 232805 | 67734 42599 1132156 26.6 | 25.162 % | c ============================================================================== c [1mFound solution: -11831872[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1220708 | 84847 232448 | 28282 46067 1249091 27.1 | 25.162 % | c | 1220809 | 84847 232448 | 31110 21674 450563 20.8 | 25.291 % | c | 1220960 | 84847 232448 | 34221 21825 452360 20.7 | 25.291 % | c | 1221185 | 84847 232448 | 37643 22050 455273 20.6 | 25.291 % | c | 1221523 | 84847 232448 | 41407 22388 461849 20.6 | 25.291 % | c | 1222030 | 84847 232448 | 45548 22895 471635 20.6 | 25.291 % | c | 1222789 | 84836 232409 | 50103 23571 481909 20.4 | 25.297 % | c | 1223929 | 84836 232409 | 55113 24711 522516 21.1 | 25.297 % | c | 1225637 | 84836 232409 | 60624 26419 586412 22.2 | 25.297 % | c ============================================================================== c [1mFound solution: -11831937[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1227363 | 84851 232446 | 28283 28145 661850 23.5 | 25.297 % | c | 1227463 | 84851 232446 | 31111 28245 664796 23.5 | 25.293 % | c | 1227613 | 84851 232446 | 34222 28395 667303 23.5 | 25.293 % | c | 1227840 | 84851 232446 | 37644 28622 673326 23.5 | 25.293 % | c | 1228178 | 84851 232446 | 41409 28960 678835 23.4 | 25.293 % | c | 1228684 | 84811 232357 | 45550 29465 686762 23.3 | 25.325 % | c | 1229443 | 84811 232357 | 50105 30224 709516 23.5 | 25.325 % | c | 1230584 | 84568 231800 | 55115 31362 748095 23.9 | 25.537 % | c | 1232292 | 84463 231500 | 60627 33068 806805 24.4 | 25.625 % | c | 1234854 | 84409 231320 | 66689 35605 903022 25.4 | 25.643 % | c | 1238701 | 84409 231320 | 73358 39452 989709 25.1 | 25.643 % | c ============================================================================== c [1mFound solution: -11831957[0m c ---[ 0]---> Sorter-cost: 13 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1241419 | 84427 231363 | 28142 42170 1073037 25.4 | 25.643 % | c | 1241520 | 84427 231363 | 30956 21186 391329 18.5 | 25.638 % | c | 1241671 | 84427 231363 | 34051 21337 394020 18.5 | 25.638 % | c | 1241900 | 84427 231363 | 37457 21566 398463 18.5 | 25.638 % | c | 1242238 | 84427 231363 | 41202 21904 404793 18.5 | 25.638 % | c | 1242744 | 84427 231363 | 45322 22410 414265 18.5 | 25.638 % | c | 1243505 | 84427 231363 | 49855 23171 455124 19.6 | 25.638 % | c | 1244645 | 84427 231363 | 54840 24311 484024 19.9 | 25.638 % | c | 1246354 | 84427 231363 | 60324 26020 545550 21.0 | 25.638 % | c ============================================================================== c [1mFound solution: -11850813[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1247799 | 84487 231511 | 28162 27465 594782 21.7 | 25.638 % | c | 1247901 | 84487 231511 | 30978 27567 596980 21.7 | 25.617 % | c | 1248051 | 84487 231511 | 34076 27717 598994 21.6 | 25.617 % | c | 1248278 | 84487 231511 | 37483 27944 604141 21.6 | 25.617 % | c | 1248615 | 84473 231479 | 41231 28280 609968 21.6 | 25.634 % | c | 1249121 | 84473 231479 | 45355 28786 618534 21.5 | 25.634 % | c | 1249883 | 83884 229504 | 49890 26565 531032 20.0 | 25.885 % | c | 1251022 | 83884 229504 | 54879 27704 562416 20.3 | 25.885 % | c | 1252730 | 81899 224751 | 60367 29227 604937 20.7 | 27.683 % | c | 1255292 | 81899 224751 | 66404 31789 665426 20.9 | 27.683 % | c ============================================================================== c [1mFound solution: -11850885[0m c ---[ 0]---> Sorter-cost: 1372 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1256288 | 85004 232025 | 28334 32785 700932 21.4 | 27.683 % | c | 1256388 | 85004 232025 | 31167 32885 702393 21.4 | 26.836 % | c | 1256539 | 84993 231986 | 34284 32995 703715 21.3 | 26.842 % | c | 1256765 | 84993 231986 | 37712 33221 708319 21.3 | 26.842 % | c | 1257103 | 84993 231986 | 41483 33559 713888 21.3 | 26.842 % | c | 1257609 | 84978 231951 | 45632 34064 723473 21.2 | 26.859 % | c | 1258369 | 84875 231714 | 50195 34823 746970 21.5 | 26.961 % | c | 1259510 | 84875 231714 | 55214 35964 791811 22.0 | 26.961 % | c | 1261220 | 84875 231714 | 60736 37674 842895 22.4 | 26.961 % | c | 1263782 | 84875 231714 | 66810 40236 922574 22.9 | 26.961 % | c ============================================================================== c [1mFound solution: -11850975[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 3 5 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1267155 | 84892 231768 | 28297 43609 1114158 25.5 | 26.961 % | c | 1267255 | 84892 231768 | 31126 21439 490625 22.9 | 26.957 % | c | 1267405 | 84892 231768 | 34239 21589 493912 22.9 | 26.957 % | c | 1267630 | 84892 231768 | 37663 21814 498559 22.9 | 26.957 % | c | 1267967 | 84892 231768 | 41429 22151 512045 23.1 | 26.957 % | c | 1268474 | 84892 231768 | 45572 22658 530252 23.4 | 26.957 % | c c *** TERMINATED *** s SATISFIABLE v -X02_bit_10 X02_bit_9 X02_bit_8 X02_bit_7 X02_bit_6 X02_bit_5 X02_bit_4 X02_bit_3 X02_bit_2 X02_bit_1 X02_bit0 X02_bit1 X02_bit2 -X02_bit3 X02_bit4 -X02_bit5 -X02_bit6 -X02_bit7 -X02_bit8 -X02_bit9 -X02_bit10 -X02_bit11 -X02_bit12 -X02_bit13 -X02_bit14 -X02_bit15 -X02_bit16 -X02_bit17 -X02_bit18 -X02_bit19 X14_bit_10 X14_bit_9 X14_bit_8 -X14_bit_7 X14_bit_6 X14_bit_5 X14_bit_4 -X14_bit_3 -X14_bit_2 -X14_bit_1 X14_bit0 -X14_bit1 -X14_bit2 -X14_bit3 X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 -X14_bit13 -X14_bit14 -X14_bit15 -X14_bit16 -X14_bit17 -X14_bit18 -X14_bit19 X23_bit_10 -X23_bit_9 -X23_bit_8 X23_bit_7 -X23_bit_6 -X23_bit_5 -X23_bit_4 -X23_bit_3 -X23_bit_2 -X23_bit_1 X23_bit0 X23_bit1 -X23_bit2 X23_bit3 X23_bit4 -X23_bit5 X23_bit6 X23_bit7 X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 -X23_bit13 -X23_bit14 -X23_bit15 -X23_bit16 -X23_bit17 -X23_bit18 -X23_bit19 X36_bit_10 X36_bit_9 X36_bit_8 X36_bit_7 -X36_bit_6 -X36_bit_5 -X36_bit_4 -X36_bit_3 X36_bit_2 -X36_bit_1 X36_bit0 X36_bit1 -X36_bit2 -X36_bit3 X36_bit4 -X36_bit5 X36_bit6 -X36_bit7 X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 -X36_bit13 -X36_bit14 -X36_bit15 -X36_bit16 -X36_bit17 -X36_bit18 -X36_bit19 -X39_bit_10 -X39_bit_9 -X39_bit_8 -X39_bit_7 -X39_bit_6 -X39_bit_5 -X39_bit_4 -X39_bit_3 -X39_bit_2 -X39_bit_1 -X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 -X39_bit13 -X39_bit14 -X39_bit15 -X39_bit16 -X39_bit17 -X39_bit18 -X39_bit19 -X01_bit_10 X01_bit_9 -X01_bit_8 -X01_bit_7 -X01_bit_6 -X01_bit_5 X01_bit_4 -X01_bit_3 -X01_bit_2 X01_bit_1 -X01_bit0 X01_bit1 X01_bit2 X01_bit3 -X01_bit4 -X01_bit5 X01_bit6 -X01_bit7 -X01_bit8 -X01_bit9 -X01_bit10 -X01_bit11 -X01_bit12 -X01_bit13 -X01_bit14 -X01_bit15 -X01_bit16 -X01_bit17 -X01_bit18 -X01_bit19 -X03_bit_10 -X03_bit_9 X03_bit_8 -X03_bit_7 -X03_bit_6 -X03_bit_5 X03_bit_4 -X03_bit_3 -X03_bit_2 X03_bit_1 -X03_bit0 X03_bit1 X03_bit2 -X03_bit3 X03_bit4 X03_bit5 -X03_bit6 -X03_bit7 -X03_bit8 -X03_bit9 -X03_bit10 -X03_bit11 -X03_bit12 -X03_bit13 -X03_bit14 -X03_bit15 -X03_bit16 -X03_bit17 -X03_bit18 -X03_bit19 X04_bit_10 -X04_bit_9 X04_bit_8 X04_bit_7 X04_bit_6 -X04_bit_5 -X04_bit_4 -X04_bit_3 X04_bit_2 -X04_bit_1 X04_bit0 X04_bit1 -X04_bit2 -X04_bit3 X04_bit4 -X04_bit5 X04_bit6 -X04_bit7 -X04_bit8 -X04_bit9 -X04_bit10 -X04_bit11 -X04_bit12 -X04_bit13 -X04_bit14 -X04_bit15 -X04_bit16 -X04_bit17 -X04_bit18 -X04_bit19 X06_bit_10 X06_bit_9 X06_bit_8 X06_bit_7 X06_bit_6 -X06_bit_5 X06_bit_4 X06_bit_3 X06_bit_2 X06_bit_1 X06_bit0 X06_bit1 X06_bit2 -X06_bit3 -X06_bit4 -X06_bit5 X06_bit6 -X06_bit7 -X06_bit8 -X06_bit9 -X06_bit10 -X06_bit11 -X06_bit12 -X06_bit13 -X06_bit14 -X06_bit15 -X06_bit16 -X06_bit17 -X06_bit18 -X06_bit19 X07_bit_10 X07_bit_9 X07_bit_8 -X07_bit_7 -X07_bit_6 X07_bit_5 -X07_bit_4 -X07_bit_3 -X07_bit_2 -X07_bit_1 -X07_bit0 -X07_bit1 -X07_bit2 -X07_bit3 -X07_bit4 -X07_bit5 -X07_bit6 -X07_bit7 -X07_bit8 -X07_bit9 -X07_bit10 -X07_bit11 -X07_bit12 -X07_bit13 -X07_bit14 -X07_bit15 -X07_bit16 -X07_bit17 -X07_bit18 -X07_bit19 -X08_bit_10 X08_bit_9 -X08_bit_8 -X08_bit_7 -X08_bit_6 -X08_bit_5 -X08_bit_4 -X08_bit_3 -X08_bit_2 -X08_bit_1 -X08_bit0 -X08_bit1 -X08_bit2 -X08_bit3 -X08_bit4 -X08_bit5 -X08_bit6 -X08_bit7 -X08_bit8 -X08_bit9 -X08_bit10 -X08_bit11 -X08_bit12 -X08_bit13 -X08_bit14 -X08_bit15 -X08_bit16 -X08_bit17 -X08_bit18 -X08_bit19 -X09_bit_10 X09_bit_9 X09_bit_8 X09_bit_7 -X09_bit_6 -X09_bit_5 -X09_bit_4 -X09_bit_3 -X09_bit_2 -X09_bit_1 -X09_bit0 -X09_bit1 -X09_bit2 -X09_bit3 -X09_bit4 -X09_bit5 -X09_bit6 -X09_bit7 -X09_bit8 -X09_bit9 -X09_bit10 -X09_bit11 -X09_bit12 -X09_bit13 -X09_bit14 -X09_bit15 -X09_bit16 -X09_bit17 -X09_bit18 -X09_bit19 X15_bit_10 X15_bit_9 X15_bit_8 X15_bit_7 X15_bit_6 -X15_bit_5 -X15_bit_4 X15_bit_3 X15_bit_2 X15_bit_1 -X15_bit0 X15_bit1 X15_bit2 -X15_bit3 X15_bit4 X15_bit5 -X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X15_bit13 -X15_bit14 -X15_bit15 -X15_bit16 -X15_bit17 -X15_bit18 -X15_bit19 -X16_bit_10 -X16_bit_9 X16_bit_8 X16_bit_7 X16_bit_6 -X16_bit_5 X16_bit_4 -X16_bit_3 X16_bit_2 -X16_bit_1 -X16_bit0 -X16_bit1 X16_bit2 X16_bit3 -X16_bit4 -X16_bit5 X16_bit6 -X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X16_bit13 -X16_bit14 -X16_bit15 -X16_bit16 -X16_bit17 -X16_bit18 -X16_bit19 -X22_bit_10 -X22_bit_9 -X22_bit_8 -X22_bit_7 -X22_bit_6 -X22_bit_5 -X22_bit_4 -X22_bit_3 -X22_bit_2 -X22_bit_1 -X22_bit0 -X22_bit1 X22_bit2 -X22_bit3 X22_bit4 X22_bit5 X22_bit6 X22_bit7 X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 -X22_bit13 -X22_bit14 -X22_bit15 -X22_bit16 -X22_bit17 -X22_bit18 -X22_bit19 -X24_bit_10 -X24_bit_9 X24_bit_8 X24_bit_7 X24_bit_6 -X24_bit_5 -X24_bit_4 X24_bit_3 -X24_bit_2 X24_bit_1 X24_bit0 X24_bit1 X24_bit2 -X24_bit3 X24_bit4 -X24_bit5 -X24_bit6 -X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 -X24_bit13 -X24_bit14 -X24_bit15 -X24_bit16 -X24_bit17 -X24_bit18 -X24_bit19 X25_bit_10 X25_bit_9 -X25_bit_8 X25_bit_7 X25_bit_6 -X25_bit_5 X25_bit_4 -X25_bit_3 X25_bit_2 -X25_bit_1 X25_bit0 -X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X25_bit13 -X25_bit14 -X25_bit15 -X25_bit16 -X25_bit17 -X25_bit18 -X25_bit19 -X26_bit_10 -X26_bit_9 -X26_bit_8 -X26_bit_7 -X26_bit_6 -X26_bit_5 -X26_bit_4 -X26_bit_3 -X26_bit_2 -X26_bit_1 X26_bit0 X26_bit1 X26_bit2 -X26_bit3 X26_bit4 -X26_bit5 X26_bit6 X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 -X26_bit13 -X26_bit14 -X26_bit15 -X26_bit16 -X26_bit17 -X26_bit18 -X26_bit19 -X28_bit_10 -X28_bit_9 -X28_bit_8 -X28_bit_7 -X28_bit_6 -X28_bit_5 -X28_bit_4 -X28_bit_3 -X28_bit_2 -X28_bit_1 -X28_bit0 -X28_bit1 -X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 -X28_bit13 -X28_bit14 -X28_bit15 -X28_bit16 -X28_bit17 -X28_bit18 -X28_bit19 -X29_bit_10 -X29_bit_9 -X29_bit_8 -X29_bit_7 -X29_bit_6 -X29_bit_5 -X29_bit_4 -X29_bit_3 -X29_bit_2 -X29_bit_1 -X29_bit0 -X29_bit1 -X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 -X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 -X29_bit13 -X29_bit14 -X29_bit15 -X29_bit16 -X29_bit17 -X29_bit18 -X29_bit19 -X30_bit_10 -X30_bit_9 -X30_bit_8 -X30_bit_7 -X30_bit_6 -X30_bit_5 -X30_bit_4 -X30_bit_3 -X30_bit_2 -X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 -X30_bit13 -X30_bit14 -X30_bit15 -X30_bit16 -X30_bit17 -X30_bit18 -X30_bit19 -X31_bit_10 -X31_bit_9 -X31_bit_8 -X31_bit_7 -X31_bit_6 -X31_bit_5 -X31_bit_4 -X31_bit_3 -X31_bit_2 -X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X31_bit13 -X31_bit14 -X31_bit15 -X31_bit16 -X31_bit17 -X31_bit18 -X31_bit19 -X38_bit_10 -X38_bit_9 -X38_bit_8 -X38_bit_7 -X38_bit_6 -X38_bit_5 -X38_bit_4 -X38_bit_3 -X38_bit_2 -X38_bit_1 -X38_bit0 -X38_bit1 -X38_bit2 -X38_bit3 -X38_bit4 -X38_bit5 -X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 -X38_bit13 -X38_bit14 -X38_bit15 -X38_bit16 -X38_bit17 -X38_bit18 -X38_bit19 X37_bit_10 X37_bit_9 X37_bit_8 X37_bit_7 -X37_bit_6 -X37_bit_5 -X37_bit_4 -X37_bit_3 X37_bit_2 -X37_bit_1 X37_bit0 X37_bit1 X37_bit2 X37_bit3 X37_bit4 X37_bit5 X37_bit6 -X37_bit7 X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_bit12 -X37_bit13 -X37_bit14 -X37_bit15 -X37_bit16 -X37_bit17 -X37_bit18 -X37_bit19 X10_bit_10 -X10_bit_9 -X10_bit_8 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X10_bit13 -X10_bit14 -X10_bit15 -X10_bit16 -X10_bit17 -X10_bit18 -X10_bit19 -X11_bit_10 -X11_bit_9 -X11_bit_8 X11_bit_7 -X11_bit_6 X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X11_bit13 -X11_bit14 -X11_bit1
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/27495/stat): 27495 (minisat+_script) R 27494 27495 31027 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1854900623 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/27495/statm): 174 3 169 147 0 27 0 [pid=27495] 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=27496 New process pid=27497 New process pid=27498 execve syscall for /bin/sed executable One traced child (pid=27497) 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=27498) exited with status: 0 One traced child (pid=27496) exited with status: 0 New process pid=27499 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-20-10-afiro.opb [startup+10.0038 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 895 0 0 0 990 3 0 0 25 0 1 0 1854900628 2584576 548 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27499/statm): 631 548 145 145 0 486 0 [pid=27499] vsize: 2524 Current children cumulated CPU time (s) 9.94 Current children cumulated vsize (Kb) 4648 [startup+20.0047 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 895 0 0 0 1989 3 0 0 25 0 1 0 1854900628 2584576 548 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27499/statm): 631 548 145 145 0 486 0 [pid=27499] vsize: 2524 Current children cumulated CPU time (s) 19.93 Current children cumulated vsize (Kb) 4648 [startup+30.0057 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 961 0 0 0 2989 4 0 0 25 0 1 0 1854900628 2674688 572 4294967295 134512640 135094434 3221224432 3221219520 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27499/statm): 653 572 145 145 0 508 0 [pid=27499] vsize: 2612 Current children cumulated CPU time (s) 29.94 Current children cumulated vsize (Kb) 4736 [startup+40.0066 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 2506 0 0 0 3976 11 0 0 25 0 1 0 1854900628 9912320 2107 4294967295 134512640 135094434 3221224432 3221223024 134557494 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27499/statm): 2420 2107 145 145 0 2275 0 [pid=27499] vsize: 9680 Current children cumulated CPU time (s) 39.88 Current children cumulated vsize (Kb) 11804 [startup+50.0076 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 3117 0 0 0 4967 16 0 0 25 0 1 0 1854900628 12443648 2718 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27499/statm): 3038 2718 145 145 0 2893 0 [pid=27499] vsize: 12152 Current children cumulated CPU time (s) 49.84 Current children cumulated vsize (Kb) 14276 [startup+60.0085 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 3768 0 0 0 5956 21 0 0 25 0 1 0 1854900628 15175680 3369 4294967295 134512640 135094434 3221224432 3221223088 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27499/statm): 3705 3369 145 145 0 3560 0 [pid=27499] vsize: 14820 Current children cumulated CPU time (s) 59.78 Current children cumulated vsize (Kb) 16944 [startup+70.0094 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 4238 0 0 0 6947 25 0 0 25 0 1 0 1854900628 17055744 3839 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 4164 3839 145 145 0 4019 0 [pid=27499] vsize: 16656 Current children cumulated CPU time (s) 69.73 Current children cumulated vsize (Kb) 18780 [startup+80.0113 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 4842 0 0 0 7938 29 0 0 25 0 1 0 1854900628 19472384 4443 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 4754 4443 145 145 0 4609 0 [pid=27499] vsize: 19016 Current children cumulated CPU time (s) 79.68 Current children cumulated vsize (Kb) 21140 [startup+90.0122 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 5518 0 0 0 8926 34 0 0 25 0 1 0 1854900628 22454272 5119 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 5482 5119 145 145 0 5337 0 [pid=27499] vsize: 21928 Current children cumulated CPU time (s) 89.61 Current children cumulated vsize (Kb) 24052 [startup+100.012 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 5864 0 0 0 9920 37 0 0 25 0 1 0 1854900628 23846912 5465 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 5822 5465 145 145 0 5677 0 [pid=27499] vsize: 23288 Current children cumulated CPU time (s) 99.58 Current children cumulated vsize (Kb) 25412 [startup+110.013 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 6305 0 0 0 10913 40 0 0 25 0 1 0 1854900628 25608192 5906 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 6252 5906 145 145 0 6107 0 [pid=27499] vsize: 25008 Current children cumulated CPU time (s) 109.54 Current children cumulated vsize (Kb) 27132 [startup+120.014 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 6889 0 0 0 11904 43 0 0 25 0 1 0 1854900628 27955200 6490 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 6825 6490 145 145 0 6680 0 [pid=27499] vsize: 27300 Current children cumulated CPU time (s) 119.48 Current children cumulated vsize (Kb) 29424 [startup+130.015 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7073 0 0 0 12901 45 0 0 25 0 1 0 1854900628 28696576 6674 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7006 6674 145 145 0 6861 0 [pid=27499] vsize: 28024 Current children cumulated CPU time (s) 129.47 Current children cumulated vsize (Kb) 30148 [startup+140.016 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7073 0 0 0 13901 45 0 0 25 0 1 0 1854900628 28696576 6674 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7006 6674 145 145 0 6861 0 [pid=27499] vsize: 28024 Current children cumulated CPU time (s) 139.47 Current children cumulated vsize (Kb) 30148 [startup+150.016 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7073 0 0 0 14901 45 0 0 25 0 1 0 1854900628 28696576 6674 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7006 6674 145 145 0 6861 0 [pid=27499] vsize: 28024 Current children cumulated CPU time (s) 149.47 Current children cumulated vsize (Kb) 30148 [startup+160.017 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7073 0 0 0 15901 45 0 0 25 0 1 0 1854900628 28696576 6674 4294967295 134512640 135094434 3221224432 3221223024 134557514 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7006 6674 145 145 0 6861 0 [pid=27499] vsize: 28024 Current children cumulated CPU time (s) 159.47 Current children cumulated vsize (Kb) 30148 [startup+170.018 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7073 0 0 0 16901 45 0 0 25 0 1 0 1854900628 28696576 6674 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7006 6674 145 145 0 6861 0 [pid=27499] vsize: 28024 Current children cumulated CPU time (s) 169.47 Current children cumulated vsize (Kb) 30148 [startup+180.019 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7174 0 0 0 17901 45 0 0 25 0 1 0 1854900628 28778496 6775 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7026 6775 145 145 0 6881 0 [pid=27499] vsize: 28104 Current children cumulated CPU time (s) 179.47 Current children cumulated vsize (Kb) 30228 [startup+190.019 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7205 0 0 0 18901 46 0 0 25 0 1 0 1854900628 28938240 6806 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7065 6806 145 145 0 6920 0 [pid=27499] vsize: 28260 Current children cumulated CPU time (s) 189.48 Current children cumulated vsize (Kb) 30384 [startup+200.02 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7205 0 0 0 19901 46 0 0 25 0 1 0 1854900628 28938240 6806 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7065 6806 145 145 0 6920 0 [pid=27499] vsize: 28260 Current children cumulated CPU time (s) 199.48 Current children cumulated vsize (Kb) 30384 [startup+210.021 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7226 0 0 0 20901 46 0 0 25 0 1 0 1854900628 28938240 6827 4294967295 134512640 135094434 3221224432 3221223056 134557585 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7065 6827 145 145 0 6920 0 [pid=27499] vsize: 28260 Current children cumulated CPU time (s) 209.48 Current children cumulated vsize (Kb) 30384 [startup+220.021 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7226 0 0 0 21901 46 0 0 25 0 1 0 1854900628 28938240 6827 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7065 6827 145 145 0 6920 0 [pid=27499] vsize: 28260 Current children cumulated CPU time (s) 219.48 Current children cumulated vsize (Kb) 30384 [startup+230.023 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7226 0 0 0 22902 46 0 0 25 0 1 0 1854900628 28938240 6827 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7065 6827 145 145 0 6920 0 [pid=27499] vsize: 28260 Current children cumulated CPU time (s) 229.49 Current children cumulated vsize (Kb) 30384 [startup+240.024 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7228 0 0 0 23902 46 0 0 25 0 1 0 1854900628 28938240 6829 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7065 6829 145 145 0 6920 0 [pid=27499] vsize: 28260 Current children cumulated CPU time (s) 239.49 Current children cumulated vsize (Kb) 30384 [startup+250.024 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7228 0 0 0 24902 46 0 0 25 0 1 0 1854900628 28938240 6829 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7065 6829 145 145 0 6920 0 [pid=27499] vsize: 28260 Current children cumulated CPU time (s) 249.49 Current children cumulated vsize (Kb) 30384 [startup+260.025 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7228 0 0 0 25902 46 0 0 25 0 1 0 1854900628 28938240 6829 4294967295 134512640 135094434 3221224432 3221223056 134557583 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7065 6829 145 145 0 6920 0 [pid=27499] vsize: 28260 Current children cumulated CPU time (s) 259.49 Current children cumulated vsize (Kb) 30384 [startup+270.026 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7255 0 0 0 26902 46 0 0 25 0 1 0 1854900628 28938240 6856 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7065 6856 145 145 0 6920 0 [pid=27499] vsize: 28260 Current children cumulated CPU time (s) 269.49 Current children cumulated vsize (Kb) 30384 [startup+280.027 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7281 0 0 0 27902 46 0 0 25 0 1 0 1854900628 29593600 6882 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6882 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 279.49 Current children cumulated vsize (Kb) 31024 [startup+290.028 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7281 0 0 0 28902 46 0 0 25 0 1 0 1854900628 29593600 6882 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6882 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 289.49 Current children cumulated vsize (Kb) 31024 [startup+300.029 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7285 0 0 0 29902 46 0 0 25 0 1 0 1854900628 29593600 6886 4294967295 134512640 135094434 3221224432 3221223084 134670544 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6886 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 299.49 Current children cumulated vsize (Kb) 31024 [startup+310.03 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7285 0 0 0 30903 46 0 0 25 0 1 0 1854900628 29593600 6886 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6886 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 309.5 Current children cumulated vsize (Kb) 31024 [startup+320.031 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7286 0 0 0 31903 46 0 0 25 0 1 0 1854900628 29593600 6887 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6887 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 319.5 Current children cumulated vsize (Kb) 31024 [startup+330.031 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7286 0 0 0 32903 46 0 0 25 0 1 0 1854900628 29593600 6887 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6887 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 329.5 Current children cumulated vsize (Kb) 31024 [startup+340.032 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7286 0 0 0 33903 46 0 0 25 0 1 0 1854900628 29593600 6887 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6887 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 339.5 Current children cumulated vsize (Kb) 31024 [startup+350.033 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7286 0 0 0 34903 46 0 0 25 0 1 0 1854900628 29593600 6887 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6887 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 349.5 Current children cumulated vsize (Kb) 31024 [startup+360.034 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7286 0 0 0 35903 46 0 0 25 0 1 0 1854900628 29593600 6887 4294967295 134512640 135094434 3221224432 3221223056 134557593 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6887 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 359.5 Current children cumulated vsize (Kb) 31024 [startup+370.034 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7286 0 0 0 36904 46 0 0 25 0 1 0 1854900628 29593600 6887 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6887 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 369.51 Current children cumulated vsize (Kb) 31024 [startup+380.036 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7286 0 0 0 37904 46 0 0 25 0 1 0 1854900628 29593600 6887 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6887 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 379.51 Current children cumulated vsize (Kb) 31024 [startup+390.037 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7287 0 0 0 38904 46 0 0 25 0 1 0 1854900628 29593600 6888 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6888 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 389.51 Current children cumulated vsize (Kb) 31024 [startup+400.037 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7287 0 0 0 39904 47 0 0 25 0 1 0 1854900628 29593600 6888 4294967295 134512640 135094434 3221224432 3221223120 134554676 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6888 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 399.52 Current children cumulated vsize (Kb) 31024 [startup+410.038 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7287 0 0 0 40904 47 0 0 25 0 1 0 1854900628 29593600 6888 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6888 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 409.52 Current children cumulated vsize (Kb) 31024 [startup+420.039 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7287 0 0 0 41904 47 0 0 25 0 1 0 1854900628 29593600 6888 4294967295 134512640 135094434 3221224432 3221222976 134779266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6888 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 419.52 Current children cumulated vsize (Kb) 31024 [startup+430.04 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7287 0 0 0 42904 47 0 0 25 0 1 0 1854900628 29593600 6888 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6888 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 429.52 Current children cumulated vsize (Kb) 31024 [startup+440.041 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7287 0 0 0 43904 47 0 0 25 0 1 0 1854900628 29593600 6888 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6888 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 439.52 Current children cumulated vsize (Kb) 31024 [startup+450.043 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7287 0 0 0 44904 47 0 0 25 0 1 0 1854900628 29593600 6888 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6888 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 449.52 Current children cumulated vsize (Kb) 31024 [startup+460.044 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7287 0 0 0 45905 47 0 0 25 0 1 0 1854900628 29593600 6888 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6888 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 459.53 Current children cumulated vsize (Kb) 31024 [startup+470.044 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7287 0 0 0 46905 47 0 0 25 0 1 0 1854900628 29593600 6888 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6888 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 469.53 Current children cumulated vsize (Kb) 31024 [startup+480.045 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7287 0 0 0 47905 47 0 0 25 0 1 0 1854900628 29593600 6888 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6888 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 479.53 Current children cumulated vsize (Kb) 31024 [startup+490.046 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7310 0 0 0 48905 47 0 0 25 0 1 0 1854900628 29593600 6911 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6911 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 489.53 Current children cumulated vsize (Kb) 31024 [startup+500.047 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7310 0 0 0 49905 47 0 0 25 0 1 0 1854900628 29593600 6911 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6911 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 499.53 Current children cumulated vsize (Kb) 31024 [startup+510.048 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7314 0 0 0 50906 47 0 0 25 0 1 0 1854900628 29593600 6915 4294967295 134512640 135094434 3221224432 3221223088 134557849 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6915 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 509.54 Current children cumulated vsize (Kb) 31024 [startup+520.049 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7314 0 0 0 51906 47 0 0 25 0 1 0 1854900628 29593600 6915 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6915 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 519.54 Current children cumulated vsize (Kb) 31024 [startup+530.05 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7314 0 0 0 52906 47 0 0 25 0 1 0 1854900628 29593600 6915 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6915 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 529.54 Current children cumulated vsize (Kb) 31024 [startup+540.051 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7314 0 0 0 53906 47 0 0 25 0 1 0 1854900628 29593600 6915 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6915 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 539.54 Current children cumulated vsize (Kb) 31024 [startup+550.051 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7314 0 0 0 54906 47 0 0 25 0 1 0 1854900628 29593600 6915 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6915 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 549.54 Current children cumulated vsize (Kb) 31024 [startup+560.053 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7314 0 0 0 55906 47 0 0 25 0 1 0 1854900628 29593600 6915 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6915 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 559.54 Current children cumulated vsize (Kb) 31024 [startup+570.054 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7314 0 0 0 56907 47 0 0 25 0 1 0 1854900628 29593600 6915 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6915 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 569.55 Current children cumulated vsize (Kb) 31024 [startup+580.055 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7314 0 0 0 57907 48 0 0 25 0 1 0 1854900628 29593600 6915 4294967295 134512640 135094434 3221224432 3221223104 134556254 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6915 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 579.56 Current children cumulated vsize (Kb) 31024 [startup+590.056 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7314 0 0 0 58907 48 0 0 25 0 1 0 1854900628 29593600 6915 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6915 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 589.56 Current children cumulated vsize (Kb) 31024 [startup+600.057 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7314 0 0 0 59907 48 0 0 25 0 1 0 1854900628 29593600 6915 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6915 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 599.56 Current children cumulated vsize (Kb) 31024 [startup+610.057 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7314 0 0 0 60907 48 0 0 25 0 1 0 1854900628 29593600 6915 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6915 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 609.56 Current children cumulated vsize (Kb) 31024 [startup+620.058 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7314 0 0 0 61907 48 0 0 25 0 1 0 1854900628 29593600 6915 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6915 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 619.56 Current children cumulated vsize (Kb) 31024 [startup+630.059 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7314 0 0 0 62908 48 0 0 25 0 1 0 1854900628 29593600 6915 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6915 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 629.57 Current children cumulated vsize (Kb) 31024 [startup+640.06 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7314 0 0 0 63908 48 0 0 25 0 1 0 1854900628 29593600 6915 4294967295 134512640 135094434 3221224432 3221223088 134557804 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6915 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 639.57 Current children cumulated vsize (Kb) 31024 [startup+650.061 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7314 0 0 0 64908 48 0 0 25 0 1 0 1854900628 29593600 6915 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6915 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 649.57 Current children cumulated vsize (Kb) 31024 [startup+660.063 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7314 0 0 0 65908 48 0 0 25 0 1 0 1854900628 29593600 6915 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6915 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 659.57 Current children cumulated vsize (Kb) 31024 [startup+670.063 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7314 0 0 0 66908 48 0 0 25 0 1 0 1854900628 29593600 6915 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6915 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 669.57 Current children cumulated vsize (Kb) 31024 [startup+680.064 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7316 0 0 0 67908 48 0 0 25 0 1 0 1854900628 29593600 6917 4294967295 134512640 135094434 3221224432 3221223104 134556205 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6917 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 679.57 Current children cumulated vsize (Kb) 31024 [startup+690.065 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7340 0 0 0 68908 48 0 0 25 0 1 0 1854900628 29593600 6941 4294967295 134512640 135094434 3221224432 3221223088 134558295 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6941 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 689.57 Current children cumulated vsize (Kb) 31024 [startup+700.066 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7346 0 0 0 69908 48 0 0 25 0 1 0 1854900628 29593600 6947 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6947 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 699.57 Current children cumulated vsize (Kb) 31024 [startup+710.067 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7346 0 0 0 70909 48 0 0 25 0 1 0 1854900628 29593600 6947 4294967295 134512640 135094434 3221224432 3221223088 134557792 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6947 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 709.58 Current children cumulated vsize (Kb) 31024 [startup+720.068 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7346 0 0 0 71909 48 0 0 25 0 1 0 1854900628 29593600 6947 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6947 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 719.58 Current children cumulated vsize (Kb) 31024 [startup+730.069 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7347 0 0 0 72909 49 0 0 25 0 1 0 1854900628 29593600 6948 4294967295 134512640 135094434 3221224432 3221223024 134557210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6948 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 729.59 Current children cumulated vsize (Kb) 31024 [startup+740.069 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7347 0 0 0 73909 49 0 0 25 0 1 0 1854900628 29593600 6948 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6948 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 739.59 Current children cumulated vsize (Kb) 31024 [startup+750.07 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7347 0 0 0 74909 49 0 0 25 0 1 0 1854900628 29593600 6948 4294967295 134512640 135094434 3221224432 3221223084 134562168 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6948 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 749.59 Current children cumulated vsize (Kb) 31024 [startup+760.072 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7349 0 0 0 75909 49 0 0 25 0 1 0 1854900628 29593600 6950 4294967295 134512640 135094434 3221224432 3221223088 134558276 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6950 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 759.59 Current children cumulated vsize (Kb) 31024 [startup+770.073 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7349 0 0 0 76909 49 0 0 25 0 1 0 1854900628 29593600 6950 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6950 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 769.59 Current children cumulated vsize (Kb) 31024 [startup+780.074 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7349 0 0 0 77910 49 0 0 25 0 1 0 1854900628 29593600 6950 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6950 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 779.6 Current children cumulated vsize (Kb) 31024 [startup+790.075 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7349 0 0 0 78910 49 0 0 25 0 1 0 1854900628 29593600 6950 4294967295 134512640 135094434 3221224432 3221223088 134557818 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6950 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 789.6 Current children cumulated vsize (Kb) 31024 [startup+800.076 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7350 0 0 0 79910 49 0 0 25 0 1 0 1854900628 29593600 6951 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6951 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 799.6 Current children cumulated vsize (Kb) 31024 [startup+810.077 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7350 0 0 0 80910 50 0 0 25 0 1 0 1854900628 29593600 6951 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6951 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 809.61 Current children cumulated vsize (Kb) 31024 [startup+820.078 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7350 0 0 0 81910 50 0 0 25 0 1 0 1854900628 29593600 6951 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6951 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 819.61 Current children cumulated vsize (Kb) 31024 [startup+830.079 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7350 0 0 0 82910 50 0 0 25 0 1 0 1854900628 29593600 6951 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6951 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 829.61 Current children cumulated vsize (Kb) 31024 [startup+840.08 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7350 0 0 0 83910 50 0 0 25 0 1 0 1854900628 29593600 6951 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6951 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 839.61 Current children cumulated vsize (Kb) 31024 [startup+850.08 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7350 0 0 0 84910 50 0 0 25 0 1 0 1854900628 29593600 6951 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6951 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 849.61 Current children cumulated vsize (Kb) 31024 [startup+860.082 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7350 0 0 0 85910 50 0 0 25 0 1 0 1854900628 29593600 6951 4294967295 134512640 135094434 3221224432 3221223056 134557648 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6951 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 859.61 Current children cumulated vsize (Kb) 31024 [startup+870.082 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7350 0 0 0 86910 50 0 0 25 0 1 0 1854900628 29593600 6951 4294967295 134512640 135094434 3221224432 3221223056 134562108 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6951 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 869.61 Current children cumulated vsize (Kb) 31024 [startup+880.083 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7350 0 0 0 87911 50 0 0 25 0 1 0 1854900628 29593600 6951 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6951 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 879.62 Current children cumulated vsize (Kb) 31024 [startup+890.084 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7350 0 0 0 88911 50 0 0 25 0 1 0 1854900628 29593600 6951 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6951 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 889.62 Current children cumulated vsize (Kb) 31024 [startup+900.085 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7350 0 0 0 89911 50 0 0 25 0 1 0 1854900628 29593600 6951 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6951 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 899.62 Current children cumulated vsize (Kb) 31024 [startup+910.086 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7350 0 0 0 90911 50 0 0 25 0 1 0 1854900628 29593600 6951 4294967295 134512640 135094434 3221224432 3221223104 134555274 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6951 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 909.62 Current children cumulated vsize (Kb) 31024 [startup+920.087 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7350 0 0 0 91911 50 0 0 25 0 1 0 1854900628 29593600 6951 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6951 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 919.62 Current children cumulated vsize (Kb) 31024 [startup+930.089 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7350 0 0 0 92912 50 0 0 25 0 1 0 1854900628 29593600 6951 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7225 6951 145 145 0 7080 0 [pid=27499] vsize: 28900 Current children cumulated CPU time (s) 929.63 Current children cumulated vsize (Kb) 31024 [startup+940.09 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 7540 0 0 0 93909 51 0 0 25 0 1 0 1854900628 30371840 7141 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 7415 7141 145 145 0 7270 0 [pid=27499] vsize: 29660 Current children cumulated CPU time (s) 939.61 Current children cumulated vsize (Kb) 31784 [startup+950.091 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 8128 0 0 0 94898 57 0 0 25 0 1 0 1854900628 32780288 7729 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 8003 7729 145 145 0 7858 0 [pid=27499] vsize: 32012 Current children cumulated CPU time (s) 949.56 Current children cumulated vsize (Kb) 34136 [startup+960.093 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 8641 0 0 0 95889 60 0 0 25 0 1 0 1854900628 34881536 8242 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 8516 8242 145 145 0 8371 0 [pid=27499] vsize: 34064 Current children cumulated CPU time (s) 959.5 Current children cumulated vsize (Kb) 36188 [startup+970.093 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9092 0 0 0 96882 63 0 0 25 0 1 0 1854900628 36745216 8693 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 8971 8693 145 145 0 8826 0 [pid=27499] vsize: 35884 Current children cumulated CPU time (s) 969.46 Current children cumulated vsize (Kb) 38008 [startup+980.094 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9446 0 0 0 97875 66 0 0 25 0 1 0 1854900628 38187008 9047 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 9323 9047 145 145 0 9178 0 [pid=27499] vsize: 37292 Current children cumulated CPU time (s) 979.42 Current children cumulated vsize (Kb) 39416 [startup+990.095 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9549 0 0 0 98874 67 0 0 25 0 1 0 1854900628 38633472 9150 4294967295 134512640 135094434 3221224432 3221223056 134557675 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 9432 9150 145 145 0 9287 0 [pid=27499] vsize: 37728 Current children cumulated CPU time (s) 989.42 Current children cumulated vsize (Kb) 39852 [startup+1000.1 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9549 0 0 0 99874 67 0 0 25 0 1 0 1854900628 38633472 9150 4294967295 134512640 135094434 3221224432 3221223044 134563041 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 9432 9150 145 145 0 9287 0 [pid=27499] vsize: 37728 Current children cumulated CPU time (s) 999.42 Current children cumulated vsize (Kb) 39852 [startup+1010.1 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9549 0 0 0 100874 67 0 0 25 0 1 0 1854900628 38633472 9150 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 9432 9150 145 145 0 9287 0 [pid=27499] vsize: 37728 Current children cumulated CPU time (s) 1009.42 Current children cumulated vsize (Kb) 39852 [startup+1020.1 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9549 0 0 0 101874 67 0 0 25 0 1 0 1854900628 38633472 9150 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 9432 9150 145 145 0 9287 0 [pid=27499] vsize: 37728 Current children cumulated CPU time (s) 1019.42 Current children cumulated vsize (Kb) 39852 [startup+1030.1 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9549 0 0 0 102874 67 0 0 25 0 1 0 1854900628 38633472 9150 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 9432 9150 145 145 0 9287 0 [pid=27499] vsize: 37728 Current children cumulated CPU time (s) 1029.42 Current children cumulated vsize (Kb) 39852 [startup+1040.1 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9550 0 0 0 103874 67 0 0 25 0 1 0 1854900628 38633472 9151 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 9432 9151 145 145 0 9287 0 [pid=27499] vsize: 37728 Current children cumulated CPU time (s) 1039.42 Current children cumulated vsize (Kb) 39852 [startup+1050.1 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9550 0 0 0 104875 67 0 0 25 0 1 0 1854900628 38633472 9151 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 9432 9151 145 145 0 9287 0 [pid=27499] vsize: 37728 Current children cumulated CPU time (s) 1049.43 Current children cumulated vsize (Kb) 39852 [startup+1060.1 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9550 0 0 0 105874 67 0 0 25 0 1 0 1854900628 38633472 9151 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 9432 9151 145 145 0 9287 0 [pid=27499] vsize: 37728 Current children cumulated CPU time (s) 1059.42 Current children cumulated vsize (Kb) 39852 [startup+1070.1 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9662 0 0 0 106874 68 0 0 25 0 1 0 1854900628 40468480 9263 4294967295 134512640 135094434 3221224432 3221223056 134562131 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 9880 9263 145 145 0 9735 0 [pid=27499] vsize: 39520 Current children cumulated CPU time (s) 1069.43 Current children cumulated vsize (Kb) 41644 [startup+1080.1 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9665 0 0 0 107874 68 0 0 25 0 1 0 1854900628 40468480 9266 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 9880 9266 145 145 0 9735 0 [pid=27499] vsize: 39520 Current children cumulated CPU time (s) 1079.43 Current children cumulated vsize (Kb) 41644 [startup+1090.1 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9665 0 0 0 108874 68 0 0 25 0 1 0 1854900628 40468480 9266 4294967295 134512640 135094434 3221224432 3221223056 134557636 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 9880 9266 145 145 0 9735 0 [pid=27499] vsize: 39520 Current children cumulated CPU time (s) 1089.43 Current children cumulated vsize (Kb) 41644 [startup+1100.1 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9689 0 0 0 109874 68 0 0 25 0 1 0 1854900628 40468480 9290 4294967295 134512640 135094434 3221224432 3221223120 134554748 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 9880 9290 145 145 0 9735 0 [pid=27499] vsize: 39520 Current children cumulated CPU time (s) 1099.43 Current children cumulated vsize (Kb) 41644 [startup+1110.11 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9697 0 0 0 110874 68 0 0 25 0 1 0 1854900628 40468480 9298 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 9880 9298 145 145 0 9735 0 [pid=27499] vsize: 39520 Current children cumulated CPU time (s) 1109.43 Current children cumulated vsize (Kb) 41644 [startup+1120.11 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9698 0 0 0 111874 68 0 0 25 0 1 0 1854900628 40468480 9299 4294967295 134512640 135094434 3221224432 3221223056 134562088 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 9880 9299 145 145 0 9735 0 [pid=27499] vsize: 39520 Current children cumulated CPU time (s) 1119.43 Current children cumulated vsize (Kb) 41644 [startup+1130.11 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9698 0 0 0 112875 68 0 0 25 0 1 0 1854900628 40468480 9299 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 9880 9299 145 145 0 9735 0 [pid=27499] vsize: 39520 Current children cumulated CPU time (s) 1129.44 Current children cumulated vsize (Kb) 41644 [startup+1140.11 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9698 0 0 0 113874 69 0 0 25 0 1 0 1854900628 40468480 9299 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 9880 9299 145 145 0 9735 0 [pid=27499] vsize: 39520 Current children cumulated CPU time (s) 1139.44 Current children cumulated vsize (Kb) 41644 [startup+1150.11 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9698 0 0 0 114874 69 0 0 25 0 1 0 1854900628 40468480 9299 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 9880 9299 145 145 0 9735 0 [pid=27499] vsize: 39520 Current children cumulated CPU time (s) 1149.44 Current children cumulated vsize (Kb) 41644 [startup+1160.11 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9698 0 0 0 115874 69 0 0 25 0 1 0 1854900628 40468480 9299 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 9880 9299 145 145 0 9735 0 [pid=27499] vsize: 39520 Current children cumulated CPU time (s) 1159.44 Current children cumulated vsize (Kb) 41644 [startup+1170.11 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9698 0 0 0 116874 69 0 0 25 0 1 0 1854900628 40468480 9299 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 9880 9299 145 145 0 9735 0 [pid=27499] vsize: 39520 Current children cumulated CPU time (s) 1169.44 Current children cumulated vsize (Kb) 41644 [startup+1180.11 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9698 0 0 0 117875 69 0 0 25 0 1 0 1854900628 40468480 9299 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 9880 9299 145 145 0 9735 0 [pid=27499] vsize: 39520 Current children cumulated CPU time (s) 1179.45 Current children cumulated vsize (Kb) 41644 [startup+1190.11 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9698 0 0 0 118875 69 0 0 25 0 1 0 1854900628 40468480 9299 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 9880 9299 145 145 0 9735 0 [pid=27499] vsize: 39520 Current children cumulated CPU time (s) 1189.45 Current children cumulated vsize (Kb) 41644 [startup+1200.11 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9716 0 0 0 119875 69 0 0 25 0 1 0 1854900628 40632320 9317 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 9920 9317 145 145 0 9775 0 [pid=27499] vsize: 39680 Current children cumulated CPU time (s) 1199.45 Current children cumulated vsize (Kb) 41804 [startup+1210.11 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9884 0 0 0 120875 70 0 0 25 0 1 0 1854900628 41308160 9485 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 10085 9485 145 145 0 9940 0 [pid=27499] vsize: 40340 Current children cumulated CPU time (s) 1209.46 Current children cumulated vsize (Kb) 42464 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.12 s] Raw data (loadavg): 0.99 1.00 0.92 2/57 27499 Raw data (/proc/27495/stat): 27495 (minisat+_script) S 27494 27495 31027 0 -1 0 289 239 0 0 0 1 0 0 18 0 1 0 1854900623 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27495/statm): 531 226 485 147 0 384 0 [pid=27495] vsize: 2124 Raw data (/proc/27499/stat): 27499 (minisat+_64-bit) R 27495 27495 31027 0 -1 0 9884 0 0 0 120875 70 0 0 25 0 1 0 1854900628 41308160 9485 4294967295 134512640 135094434 3221224432 3221223088 134561734 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27499/statm): 10085 9485 145 145 0 9940 0 [pid=27499] vsize: 40340 Current children cumulated CPU time (s) 1209.46 Current children cumulated vsize (Kb) 42464 Sending SIGTERM to -27495 Sleeping 2 seconds One traced child (pid=27495) ended because it received signal 15 (SIGTERM) One traced child (pid=27499) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.14 CPU time (s): 1209.48 CPU user time (s): 1208.76 CPU system time (s): 0.71989 CPU usage (%): 99.9449 Max. virtual memory (cumulated for all children) (Kb): 42464
ERROR: no interpretation found !