Name | mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-markshare1.opb |
MD5SUM | c8b965306fec2c21edee64824d12f378 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 36864 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 180 |
Biggest coefficient in the objective function | 536870912 |
Number of bits for the biggest coefficient in the objective function | 30 |
Sum of the numbers in the objective function | 6442450938 |
Number of bits of the sum of numbers in the objective function | 33 |
Biggest number in a constraint | 536870912 |
Number of bits of the biggest number in a constraint | 30 |
Biggest sum of numbers in a constraint | 6442450938 |
Number of bits of the biggest sum of numbers | 33 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.29 |
Number of variables | 230 |
Total number of constraints | 56 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 50 |
Number of constraints which are nor clauses,nor cardinality constraints | 6 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 80 |
LAUNCH ON wulflinc24 THE 2005-09-19 18:02:46 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2982 boxname=wulflinc24 idbench=638 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: c8b965306fec2c21edee64824d12f378 /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-markshare1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-markshare1.opb IDLAUNCH: 2982 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 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: 891220 kB Buffers: 34180 kB Cached: 81432 kB SwapCached: 736 kB Active: 69636 kB Inactive: 48588 kB HighTotal: 131008 kB HighFree: 45864 kB LowTotal: 903652 kB LowFree: 845356 kB SwapTotal: 2097892 kB SwapFree: 2096652 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5736 kB Slab: 19452 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-19 18:22:57 (client local time) WITH STATUS 10 IN 1209.89 SECONDS stats: 2982 7 1209.89 10
c Parsing PB file... c Converting 12 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ###### c -- Clauses(.)/Splits(s): (none) c ---[ 10]---> Adder-cost: 304 maxlim: 3240959 bits: 23/22 c ---[ 8]---> Adder-cost: 314 maxlim: 3453951 bits: 23/22 c ---[ 6]---> Adder-cost: 348 maxlim: 3482623 bits: 23/22 c ---[ 4]---> Adder-cost: 318 maxlim: 3294207 bits: 23/22 c ---[ 2]---> Adder-cost: 312 maxlim: 3286015 bits: 23/22 c ---[ 0]---> Adder-cost: 314 maxlim: 3289087 bits: 23/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 12820 45524 | 4273 0 0 nan | 0.000 % | c | 100 | 12820 45524 | 4700 100 594 5.9 | 14.261 % | c ============================================================================== c [1mFound solution: 4615168[0m c ---[ 0]---> Sorter-cost: 850 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 141 | 14814 50194 | 4938 141 1027 7.3 | 14.261 % | c | 241 | 14814 50194 | 5431 241 12192 50.6 | 10.969 % | c | 393 | 14814 50194 | 5974 393 26032 66.2 | 10.969 % | c | 618 | 14814 50194 | 6572 618 37060 60.0 | 10.969 % | c | 955 | 14814 50194 | 7229 955 69049 72.3 | 10.969 % | c ============================================================================== c [1mFound solution: 4444160[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1006 | 14929 50490 | 4976 1006 70987 70.6 | 10.969 % | c | 1107 | 14929 50490 | 5473 1107 85930 77.6 | 10.770 % | c ============================================================================== c [1mFound solution: 4152320[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1139 | 14941 50532 | 4980 1139 86375 75.8 | 10.770 % | c | 1240 | 14941 50532 | 5478 1240 94355 76.1 | 10.771 % | c | 1390 | 14941 50532 | 6025 1390 106104 76.3 | 10.771 % | c ============================================================================== c [1mFound solution: 3231744[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1590 | 14951 50556 | 4983 1590 117597 74.0 | 10.771 % | c | 1691 | 14951 50556 | 5481 1691 130635 77.3 | 10.786 % | c | 1841 | 14951 50556 | 6029 1841 142489 77.4 | 10.786 % | c | 2067 | 14943 50530 | 6632 2066 165570 80.1 | 10.819 % | c | 2404 | 14943 50530 | 7295 2403 186034 77.4 | 10.819 % | c | 2910 | 14943 50530 | 8025 2909 234223 80.5 | 10.819 % | c | 3669 | 14935 50504 | 8827 3667 297711 81.2 | 10.852 % | c | 4810 | 14919 50452 | 9710 4806 397534 82.7 | 10.917 % | c | 6518 | 14919 50452 | 10681 6514 543132 83.4 | 10.917 % | c | 9081 | 14919 50452 | 11749 9077 695094 76.6 | 10.917 % | c ============================================================================== c [1mFound solution: 3212288[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11955 | 14931 50479 | 4977 11951 922500 77.2 | 10.917 % | c | 12056 | 14931 50479 | 5474 3089 184035 59.6 | 10.932 % | c | 12207 | 14931 50479 | 6022 3240 193746 59.8 | 10.932 % | c | 12433 | 14931 50479 | 6624 3466 204232 58.9 | 10.932 % | c | 12770 | 14931 50479 | 7286 3803 246752 64.9 | 10.932 % | c | 13278 | 14923 50453 | 8015 4310 287955 66.8 | 10.965 % | c | 14042 | 14923 50453 | 8817 5074 357875 70.5 | 10.965 % | c | 15182 | 14923 50453 | 9698 6214 454785 73.2 | 10.965 % | c | 16891 | 14923 50453 | 10668 7923 596983 75.3 | 10.965 % | c | 19453 | 14915 50427 | 11735 10484 806542 76.9 | 10.998 % | c | 23299 | 14907 50401 | 12909 7910 531028 67.1 | 11.031 % | c | 29065 | 14891 50349 | 14199 13674 1005814 73.6 | 11.097 % | c | 37715 | 14884 50334 | 15619 14705 1118217 76.0 | 11.162 % | c ============================================================================== c [1mFound solution: 3169280[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 45485 | 14886 50339 | 4962 14152 1130949 79.9 | 11.162 % | c | 45586 | 14886 50339 | 5458 3639 207343 57.0 | 11.253 % | c | 45736 | 14886 50339 | 6004 3789 218603 57.7 | 11.253 % | c | 45961 | 14886 50339 | 6604 4014 238535 59.4 | 11.253 % | c | 46300 | 14886 50339 | 7264 4353 272968 62.7 | 11.253 % | c | 46807 | 14878 50313 | 7991 4859 321893 66.2 | 11.286 % | c | 47567 | 14878 50313 | 8790 5619 395734 70.4 | 11.286 % | c | 48706 | 14878 50313 | 9669 6758 514295 76.1 | 11.286 % | c | 50414 | 14878 50313 | 10636 8466 674245 79.6 | 11.286 % | c | 52979 | 14878 50313 | 11700 11031 894758 81.1 | 11.286 % | c | 56823 | 14878 50313 | 12870 8476 585487 69.1 | 11.286 % | c | 62589 | 14878 50313 | 14157 7246 470267 64.9 | 11.286 % | c | 71238 | 14878 50313 | 15572 8340 484689 58.1 | 11.286 % | c ============================================================================== c [1mFound solution: 3042304[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 81326 | 14886 50332 | 4962 10127 656025 64.8 | 11.286 % | c | 81428 | 14886 50332 | 5458 5166 279097 54.0 | 11.300 % | c | 81579 | 14886 50332 | 6004 5317 292474 55.0 | 11.300 % | c | 81804 | 14886 50332 | 6604 5542 307973 55.6 | 11.300 % | c | 82141 | 14886 50332 | 7264 5879 344300 58.6 | 11.300 % | c | 82647 | 14886 50332 | 7991 6385 389480 61.0 | 11.300 % | c | 83406 | 14886 50332 | 8790 7144 439505 61.5 | 11.300 % | c | 84547 | 14886 50332 | 9669 8285 529161 63.9 | 11.300 % | c | 86259 | 14886 50332 | 10636 9997 662102 66.2 | 11.300 % | c | 88822 | 14886 50332 | 11700 6767 420905 62.2 | 11.300 % | c | 92668 | 14886 50332 | 12870 10613 744951 70.2 | 11.300 % | c | 98434 | 14886 50332 | 14157 9409 652200 69.3 | 11.300 % | c | 107085 | 14886 50332 | 15572 10478 637247 60.8 | 11.300 % | c ============================================================================== c [1mFound solution: 3005440[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 111385 | 14888 50336 | 4962 14777 921886 62.4 | 11.300 % | c | 111486 | 14888 50336 | 5458 3796 173019 45.6 | 11.344 % | c | 111636 | 14888 50336 | 6004 3946 179318 45.4 | 11.344 % | c | 111861 | 14888 50336 | 6604 4171 192217 46.1 | 11.344 % | c | 112199 | 14880 50310 | 7264 4508 220479 48.9 | 11.376 % | c | 112705 | 14880 50310 | 7991 5014 263662 52.6 | 11.376 % | c | 113465 | 14880 50310 | 8790 5774 310667 53.8 | 11.376 % | c | 114604 | 14880 50310 | 9669 6913 409090 59.2 | 11.376 % | c | 116313 | 14872 50284 | 10636 8621 542723 63.0 | 11.409 % | c | 118875 | 14864 50258 | 11700 11182 716184 64.0 | 11.442 % | c | 122719 | 14864 50258 | 12870 8765 560433 63.9 | 11.442 % | c ============================================================================== c [1mFound solution: 2816000[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 124383 | 14877 50289 | 4959 10429 657968 63.1 | 11.442 % | c | 124484 | 14877 50289 | 5454 5316 265689 50.0 | 11.448 % | c | 124635 | 14877 50289 | 6000 5467 270323 49.4 | 11.448 % | c | 124860 | 14877 50289 | 6600 5692 292327 51.4 | 11.448 % | c | 125197 | 14877 50289 | 7260 6029 329895 54.7 | 11.448 % | c | 125703 | 14877 50289 | 7986 6535 361239 55.3 | 11.448 % | c | 126462 | 14877 50289 | 8785 7294 391859 53.7 | 11.448 % | c | 127603 | 14877 50289 | 9663 8435 478713 56.8 | 11.448 % | c | 129311 | 14877 50289 | 10630 10143 570334 56.2 | 11.448 % | c | 131874 | 14877 50289 | 11693 7035 309663 44.0 | 11.448 % | c ============================================================================== c [1mFound solution: 1213440[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 132830 | 14885 50302 | 4961 7990 344228 43.1 | 11.448 % | c | 132930 | 14885 50302 | 5457 4095 130652 31.9 | 11.487 % | c | 133082 | 14885 50302 | 6002 4247 140906 33.2 | 11.487 % | c | 133308 | 14885 50302 | 6603 4473 145839 32.6 | 11.487 % | c | 133645 | 14885 50302 | 7263 4810 163247 33.9 | 11.487 % | c | 134152 | 14885 50302 | 7989 5317 180646 34.0 | 11.487 % | c | 134911 | 14867 50262 | 8788 6074 210613 34.7 | 11.650 % | c | 136050 | 14867 50262 | 9667 7213 249425 34.6 | 11.650 % | c | 137760 | 14839 50199 | 10634 8921 304715 34.2 | 11.910 % | c | 140322 | 14839 50199 | 11697 11483 433802 37.8 | 11.910 % | c | 144166 | 14839 50199 | 12867 9063 353815 39.0 | 11.910 % | c | 149933 | 14839 50199 | 14154 7885 325078 41.2 | 11.910 % | c | 158582 | 14839 50199 | 15569 9129 370373 40.6 | 11.910 % | c | 171556 | 14839 50199 | 17126 13879 596591 43.0 | 11.910 % | c ============================================================================== c [1mFound solution: 1145856[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 183021 | 14849 50222 | 4949 16407 675729 41.2 | 11.910 % | c | 183123 | 14849 50222 | 5443 4204 124504 29.6 | 11.927 % | c | 183273 | 14849 50222 | 5988 4354 127342 29.2 | 11.927 % | c | 183498 | 14849 50222 | 6587 4579 133579 29.2 | 11.927 % | c | 183836 | 14849 50222 | 7245 4917 140722 28.6 | 11.927 % | c | 184343 | 14849 50222 | 7970 5424 153528 28.3 | 11.927 % | c | 185102 | 14849 50222 | 8767 6183 178163 28.8 | 11.927 % | c | 186244 | 14849 50222 | 9644 7325 224903 30.7 | 11.927 % | c | 187953 | 14849 50222 | 10608 9034 306970 34.0 | 11.927 % | c | 190516 | 14849 50222 | 11669 5935 207351 34.9 | 11.927 % | c | 194361 | 14849 50222 | 12836 9780 381421 39.0 | 11.927 % | c | 200127 | 14849 50222 | 14120 8789 336369 38.3 | 11.927 % | c | 208776 | 14849 50222 | 15532 10045 375187 37.4 | 11.927 % | c | 221750 | 14849 50222 | 17085 14863 663052 44.6 | 11.927 % | c ============================================================================== c [1mFound solution: 882688[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 226679 | 14815 50095 | 4938 10932 449646 41.1 | 11.927 % | c | 226780 | 14815 50095 | 5431 2834 95029 33.5 | 12.131 % | c | 226930 | 14815 50095 | 5974 2984 100132 33.6 | 12.131 % | c | 227155 | 14815 50095 | 6572 3209 103870 32.4 | 12.131 % | c | 227493 | 14815 50095 | 7229 3547 112944 31.8 | 12.131 % | c | 228002 | 14815 50095 | 7952 4056 131115 32.3 | 12.131 % | c | 228763 | 14815 50095 | 8747 4817 152790 31.7 | 12.131 % | c | 229903 | 14815 50095 | 9622 5957 192874 32.4 | 12.131 % | c | 231611 | 14815 50095 | 10585 7665 256994 33.5 | 12.131 % | c | 234173 | 14815 50095 | 11643 10227 369004 36.1 | 12.131 % | c | 238017 | 14815 50095 | 12807 7881 286356 36.3 | 12.131 % | c | 243784 | 14815 50095 | 14088 6898 265127 38.4 | 12.131 % | c | 252433 | 14725 49888 | 15497 8166 240170 29.4 | 13.104 % | c | 265408 | 14698 49827 | 17047 12985 490542 37.8 | 13.428 % | c ============================================================================== c [1mFound solution: 804864[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 267580 | 14710 49855 | 4903 15157 570717 37.7 | 13.428 % | c | 267682 | 14710 49855 | 5393 3892 103008 26.5 | 13.430 % | c | 267833 | 14710 49855 | 5932 4043 104747 25.9 | 13.430 % | c | 268058 | 14710 49855 | 6525 4268 108961 25.5 | 13.430 % | c | 268395 | 14710 49855 | 7178 4605 114605 24.9 | 13.430 % | c | 268901 | 14710 49855 | 7896 5111 127137 24.9 | 13.430 % | c | 269662 | 14710 49855 | 8685 5872 146984 25.0 | 13.430 % | c | 270803 | 14710 49855 | 9554 7013 203504 29.0 | 13.430 % | c | 272514 | 14710 49855 | 10510 8724 270568 31.0 | 13.430 % | c | 275076 | 14710 49855 | 11561 5653 166684 29.5 | 13.430 % | c | 278920 | 14710 49855 | 12717 9497 351916 37.1 | 13.430 % | c | 284686 | 14697 49825 | 13988 8584 333786 38.9 | 13.592 % | c | 293335 | 14697 49825 | 15387 9940 408374 41.1 | 13.592 % | c | 306309 | 14697 49825 | 16926 14883 678759 45.6 | 13.592 % | c | 325770 | 14697 49825 | 18619 16738 728728 43.5 | 13.592 % | c | 354962 | 14697 49825 | 20481 16697 780600 46.8 | 13.592 % | c | 398751 | 14673 49772 | 22529 18038 685094 38.0 | 13.819 % | c | 464435 | 14665 49750 | 24782 13779 573078 41.6 | 13.884 % | c | 562961 | 14665 49750 | 27260 22883 1101452 48.1 | 13.884 % | c | 710752 | 14658 49735 | 29986 15376 652286 42.4 | 13.948 % | c ============================================================================== c [1mFound solution: 623616[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 746664 | 14638 49690 | 4879 17992 706327 39.3 | 13.948 % | c | 746764 | 14638 49690 | 5366 4598 126096 27.4 | 14.193 % | c | 746914 | 14638 49690 | 5903 4748 127793 26.9 | 14.193 % | c | 747139 | 14638 49690 | 6493 4973 134208 27.0 | 14.193 % | c | 747476 | 14638 49690 | 7143 5310 144194 27.2 | 14.193 % | c | 747983 | 14638 49690 | 7857 5817 154204 26.5 | 14.193 % | c | 748742 | 14638 49690 | 8643 6576 178501 27.1 | 14.193 % | c | 749883 | 14638 49690 | 9507 7717 235750 30.5 | 14.193 % | c | 751592 | 14638 49690 | 10458 9426 293678 31.2 | 14.193 % | c | 754155 | 14638 49690 | 11504 6266 192414 30.7 | 14.193 % | c | 758000 | 14613 49633 | 12654 10109 337355 33.4 | 14.452 % | c | 763767 | 14613 49633 | 13920 9088 320912 35.3 | 14.452 % | c | 772417 | 14613 49633 | 15312 10244 395768 38.6 | 14.452 % |
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/1928/stat): 1928 (minisat+_script) R 1927 1928 20728 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1851904166 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/1928/statm): 174 3 169 147 0 27 0 [pid=1928] 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=1929 New process pid=1930 New process pid=1931 execve syscall for /bin/sed executable One traced child (pid=1930) 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=1931) exited with status: 0 One traced child (pid=1929) exited with status: 0 New process pid=1932 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-markshare1.opb [startup+10.0033 s] Raw data (loadavg): 0.93 0.97 0.88 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 995 0 0 0 983 4 0 0 25 0 1 0 1851904171 4362240 982 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 1065 982 145 145 0 920 0 [pid=1932] vsize: 4260 Current children cumulated CPU time (s) 9.88 Current children cumulated vsize (Kb) 6384 [startup+20.004 s] Raw data (loadavg): 0.94 0.97 0.88 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 1353 0 0 0 1975 8 0 0 25 0 1 0 1851904171 5844992 1340 4294967295 134512640 135094434 3221224432 3221223104 134555175 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1932/statm): 1427 1340 145 145 0 1282 0 [pid=1932] vsize: 5708 Current children cumulated CPU time (s) 19.84 Current children cumulated vsize (Kb) 7832 [startup+30.0057 s] Raw data (loadavg): 0.95 0.97 0.89 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 1555 0 0 0 2970 10 0 0 25 0 1 0 1851904171 6668288 1542 4294967295 134512640 135094434 3221224432 3221223104 134555323 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 1628 1542 145 145 0 1483 0 [pid=1932] vsize: 6512 Current children cumulated CPU time (s) 29.81 Current children cumulated vsize (Kb) 8636 [startup+40.0063 s] Raw data (loadavg): 0.96 0.97 0.89 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 1555 0 0 0 3969 10 0 0 25 0 1 0 1851904171 6668288 1542 4294967295 134512640 135094434 3221224432 3221223104 134556246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 1628 1542 145 145 0 1483 0 [pid=1932] vsize: 6512 Current children cumulated CPU time (s) 39.8 Current children cumulated vsize (Kb) 8636 [startup+50.008 s] Raw data (loadavg): 0.96 0.97 0.89 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 1688 0 0 0 4967 11 0 0 25 0 1 0 1851904171 7213056 1675 4294967295 134512640 135094434 3221224432 3221223024 134551434 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 1761 1675 145 145 0 1616 0 [pid=1932] vsize: 7044 Current children cumulated CPU time (s) 49.79 Current children cumulated vsize (Kb) 9168 [startup+60.0087 s] Raw data (loadavg): 0.97 0.97 0.89 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 1688 0 0 0 5968 11 0 0 25 0 1 0 1851904171 7213056 1675 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 1761 1675 145 145 0 1616 0 [pid=1932] vsize: 7044 Current children cumulated CPU time (s) 59.8 Current children cumulated vsize (Kb) 9168 [startup+70.0095 s] Raw data (loadavg): 0.97 0.97 0.89 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 1806 0 0 0 6965 12 0 0 25 0 1 0 1851904171 7696384 1793 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1932/statm): 1879 1793 145 145 0 1734 0 [pid=1932] vsize: 7516 Current children cumulated CPU time (s) 69.78 Current children cumulated vsize (Kb) 9640 [startup+80.0111 s] Raw data (loadavg): 0.98 0.97 0.89 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 1894 0 0 0 7963 13 0 0 25 0 1 0 1851904171 8060928 1881 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 1968 1881 145 145 0 1823 0 [pid=1932] vsize: 7872 Current children cumulated CPU time (s) 79.77 Current children cumulated vsize (Kb) 9996 [startup+90.0118 s] Raw data (loadavg): 0.98 0.97 0.89 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 1905 0 0 0 8963 13 0 0 25 0 1 0 1851904171 8110080 1892 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 1980 1892 145 145 0 1835 0 [pid=1932] vsize: 7920 Current children cumulated CPU time (s) 89.77 Current children cumulated vsize (Kb) 10044 [startup+100.013 s] Raw data (loadavg): 0.98 0.97 0.89 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2025 0 0 0 9962 13 0 0 25 0 1 0 1851904171 8609792 2012 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2102 2012 145 145 0 1957 0 [pid=1932] vsize: 8408 Current children cumulated CPU time (s) 99.76 Current children cumulated vsize (Kb) 10532 [startup+110.013 s] Raw data (loadavg): 0.98 0.97 0.89 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2098 0 0 0 10961 14 0 0 25 0 1 0 1851904171 8974336 2085 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2085 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 109.76 Current children cumulated vsize (Kb) 10888 [startup+120.014 s] Raw data (loadavg): 0.99 0.97 0.89 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2099 0 0 0 11961 14 0 0 25 0 1 0 1851904171 8974336 2086 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2086 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 119.76 Current children cumulated vsize (Kb) 10888 [startup+130.015 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2101 0 0 0 12961 14 0 0 25 0 1 0 1851904171 8974336 2088 4294967295 134512640 135094434 3221224432 3221223120 134554733 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2088 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 129.76 Current children cumulated vsize (Kb) 10888 [startup+140.015 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2101 0 0 0 13961 14 0 0 25 0 1 0 1851904171 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2088 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 139.76 Current children cumulated vsize (Kb) 10888 [startup+150.017 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2101 0 0 0 14961 14 0 0 25 0 1 0 1851904171 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2088 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 149.76 Current children cumulated vsize (Kb) 10888 [startup+160.018 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2101 0 0 0 15962 14 0 0 25 0 1 0 1851904171 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2088 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 159.77 Current children cumulated vsize (Kb) 10888 [startup+170.018 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2101 0 0 0 16962 14 0 0 25 0 1 0 1851904171 8974336 2088 4294967295 134512640 135094434 3221224432 3221223104 134555940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2088 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 169.77 Current children cumulated vsize (Kb) 10888 [startup+180.019 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2101 0 0 0 17962 14 0 0 25 0 1 0 1851904171 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2088 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 179.77 Current children cumulated vsize (Kb) 10888 [startup+190.02 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2101 0 0 0 18962 15 0 0 25 0 1 0 1851904171 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2088 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 189.78 Current children cumulated vsize (Kb) 10888 [startup+200.02 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2101 0 0 0 19962 15 0 0 25 0 1 0 1851904171 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2088 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 199.78 Current children cumulated vsize (Kb) 10888 [startup+210.021 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2101 0 0 0 20962 15 0 0 25 0 1 0 1851904171 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2088 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 209.78 Current children cumulated vsize (Kb) 10888 [startup+220.022 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2101 0 0 0 21963 15 0 0 25 0 1 0 1851904171 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2088 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 219.79 Current children cumulated vsize (Kb) 10888 [startup+230.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2101 0 0 0 22963 15 0 0 25 0 1 0 1851904171 8974336 2088 4294967295 134512640 135094434 3221224432 3221223064 134557638 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2088 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 229.79 Current children cumulated vsize (Kb) 10888 [startup+240.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2101 0 0 0 23963 15 0 0 25 0 1 0 1851904171 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134558169 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2088 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 239.79 Current children cumulated vsize (Kb) 10888 [startup+250.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2101 0 0 0 24963 15 0 0 25 0 1 0 1851904171 8974336 2088 4294967295 134512640 135094434 3221224432 3221223104 134555953 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2088 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 249.79 Current children cumulated vsize (Kb) 10888 [startup+260.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2101 0 0 0 25963 15 0 0 25 0 1 0 1851904171 8974336 2088 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2088 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 259.79 Current children cumulated vsize (Kb) 10888 [startup+270.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2101 0 0 0 26963 15 0 0 25 0 1 0 1851904171 8974336 2088 4294967295 134512640 135094434 3221224432 3221223056 134557705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2088 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 269.79 Current children cumulated vsize (Kb) 10888 [startup+280.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2101 0 0 0 27963 15 0 0 25 0 1 0 1851904171 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2088 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 279.79 Current children cumulated vsize (Kb) 10888 [startup+290.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2101 0 0 0 28964 15 0 0 25 0 1 0 1851904171 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2088 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 289.8 Current children cumulated vsize (Kb) 10888 [startup+300.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2101 0 0 0 29964 15 0 0 25 0 1 0 1851904171 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134558169 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2088 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 299.8 Current children cumulated vsize (Kb) 10888 [startup+310.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2101 0 0 0 30964 15 0 0 25 0 1 0 1851904171 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2088 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 309.8 Current children cumulated vsize (Kb) 10888 [startup+320.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2101 0 0 0 31964 15 0 0 25 0 1 0 1851904171 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2088 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 319.8 Current children cumulated vsize (Kb) 10888 [startup+330.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2101 0 0 0 32964 15 0 0 25 0 1 0 1851904171 8974336 2088 4294967295 134512640 135094434 3221224432 3221222412 134562710 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2088 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 329.8 Current children cumulated vsize (Kb) 10888 [startup+340.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2101 0 0 0 33964 16 0 0 25 0 1 0 1851904171 8974336 2088 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2088 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 339.81 Current children cumulated vsize (Kb) 10888 [startup+350.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2101 0 0 0 34964 16 0 0 25 0 1 0 1851904171 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2088 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 349.81 Current children cumulated vsize (Kb) 10888 [startup+360.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2101 0 0 0 35965 16 0 0 25 0 1 0 1851904171 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2088 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 359.82 Current children cumulated vsize (Kb) 10888 [startup+370.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2101 0 0 0 36965 16 0 0 25 0 1 0 1851904171 8974336 2088 4294967295 134512640 135094434 3221224432 3221223088 134558411 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2088 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 369.82 Current children cumulated vsize (Kb) 10888 [startup+380.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2102 0 0 0 37965 16 0 0 25 0 1 0 1851904171 8974336 2089 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2089 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 379.82 Current children cumulated vsize (Kb) 10888 [startup+390.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2102 0 0 0 38965 16 0 0 25 0 1 0 1851904171 8974336 2089 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2089 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 389.82 Current children cumulated vsize (Kb) 10888 [startup+400.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2102 0 0 0 39965 16 0 0 25 0 1 0 1851904171 8974336 2089 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2089 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 399.82 Current children cumulated vsize (Kb) 10888 [startup+410.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2102 0 0 0 40965 16 0 0 25 0 1 0 1851904171 8974336 2089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2089 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 409.82 Current children cumulated vsize (Kb) 10888 [startup+420.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2102 0 0 0 41966 16 0 0 25 0 1 0 1851904171 8974336 2089 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2089 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 419.83 Current children cumulated vsize (Kb) 10888 [startup+430.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2102 0 0 0 42965 16 0 0 25 0 1 0 1851904171 8974336 2089 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2089 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 429.82 Current children cumulated vsize (Kb) 10888 [startup+440.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2102 0 0 0 43966 16 0 0 25 0 1 0 1851904171 8974336 2089 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2089 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 439.83 Current children cumulated vsize (Kb) 10888 [startup+450.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2102 0 0 0 44965 17 0 0 25 0 1 0 1851904171 8974336 2089 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2089 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 449.83 Current children cumulated vsize (Kb) 10888 [startup+460.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2102 0 0 0 45964 18 0 0 25 0 1 0 1851904171 8974336 2089 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2089 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 459.83 Current children cumulated vsize (Kb) 10888 [startup+470.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2102 0 0 0 46964 19 0 0 25 0 1 0 1851904171 8974336 2089 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2089 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 469.84 Current children cumulated vsize (Kb) 10888 [startup+480.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2102 0 0 0 47964 19 0 0 25 0 1 0 1851904171 8974336 2089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2089 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 479.84 Current children cumulated vsize (Kb) 10888 [startup+490.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2102 0 0 0 48964 19 0 0 25 0 1 0 1851904171 8974336 2089 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2089 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 489.84 Current children cumulated vsize (Kb) 10888 [startup+500.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2102 0 0 0 49964 20 0 0 25 0 1 0 1851904171 8974336 2089 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2191 2089 145 145 0 2046 0 [pid=1932] vsize: 8764 Current children cumulated CPU time (s) 499.85 Current children cumulated vsize (Kb) 10888 [startup+510.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2143 0 0 0 50963 20 0 0 25 0 1 0 1851904171 9146368 2130 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2233 2130 145 145 0 2088 0 [pid=1932] vsize: 8932 Current children cumulated CPU time (s) 509.84 Current children cumulated vsize (Kb) 11056 [startup+520.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2144 0 0 0 51963 21 0 0 25 0 1 0 1851904171 9146368 2131 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2233 2131 145 145 0 2088 0 [pid=1932] vsize: 8932 Current children cumulated CPU time (s) 519.85 Current children cumulated vsize (Kb) 11056 [startup+530.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2206 0 0 0 52962 21 0 0 25 0 1 0 1851904171 9392128 2193 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2293 2193 145 145 0 2148 0 [pid=1932] vsize: 9172 Current children cumulated CPU time (s) 529.84 Current children cumulated vsize (Kb) 11296 [startup+540.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2291 0 0 0 53959 22 0 0 25 0 1 0 1851904171 9748480 2278 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2380 2278 145 145 0 2235 0 [pid=1932] vsize: 9520 Current children cumulated CPU time (s) 539.82 Current children cumulated vsize (Kb) 11644 [startup+550.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2422 0 0 0 54957 23 0 0 25 0 1 0 1851904171 10289152 2409 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2512 2409 145 145 0 2367 0 [pid=1932] vsize: 10048 Current children cumulated CPU time (s) 549.81 Current children cumulated vsize (Kb) 12172 [startup+560.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2430 0 0 0 55957 23 0 0 25 0 1 0 1851904171 10321920 2417 4294967295 134512640 135094434 3221224432 3221223088 134557849 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2520 2417 145 145 0 2375 0 [pid=1932] vsize: 10080 Current children cumulated CPU time (s) 559.81 Current children cumulated vsize (Kb) 12204 [startup+570.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2439 0 0 0 56957 23 0 0 25 0 1 0 1851904171 10371072 2426 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2532 2426 145 145 0 2387 0 [pid=1932] vsize: 10128 Current children cumulated CPU time (s) 569.81 Current children cumulated vsize (Kb) 12252 [startup+580.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2444 0 0 0 57957 23 0 0 25 0 1 0 1851904171 10395648 2431 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2538 2431 145 145 0 2393 0 [pid=1932] vsize: 10152 Current children cumulated CPU time (s) 579.81 Current children cumulated vsize (Kb) 12276 [startup+590.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2451 0 0 0 58958 23 0 0 25 0 1 0 1851904171 10428416 2438 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2546 2438 145 145 0 2401 0 [pid=1932] vsize: 10184 Current children cumulated CPU time (s) 589.82 Current children cumulated vsize (Kb) 12308 [startup+600.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2461 0 0 0 59957 23 0 0 25 0 1 0 1851904171 10477568 2448 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2558 2448 145 145 0 2413 0 [pid=1932] vsize: 10232 Current children cumulated CPU time (s) 599.81 Current children cumulated vsize (Kb) 12356 [startup+610.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2472 0 0 0 60958 23 0 0 25 0 1 0 1851904171 10543104 2459 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2574 2459 145 145 0 2429 0 [pid=1932] vsize: 10296 Current children cumulated CPU time (s) 609.82 Current children cumulated vsize (Kb) 12420 [startup+620.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2510 0 0 0 61957 24 0 0 25 0 1 0 1851904171 10702848 2497 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2613 2497 145 145 0 2468 0 [pid=1932] vsize: 10452 Current children cumulated CPU time (s) 619.82 Current children cumulated vsize (Kb) 12576 [startup+630.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2516 0 0 0 62958 24 0 0 25 0 1 0 1851904171 10727424 2503 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2619 2503 145 145 0 2474 0 [pid=1932] vsize: 10476 Current children cumulated CPU time (s) 629.83 Current children cumulated vsize (Kb) 12600 [startup+640.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2569 0 0 0 63956 25 0 0 25 0 1 0 1851904171 10944512 2556 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2672 2556 145 145 0 2527 0 [pid=1932] vsize: 10688 Current children cumulated CPU time (s) 639.82 Current children cumulated vsize (Kb) 12812 [startup+650.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2577 0 0 0 64957 25 0 0 25 0 1 0 1851904171 10977280 2564 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2680 2564 145 145 0 2535 0 [pid=1932] vsize: 10720 Current children cumulated CPU time (s) 649.83 Current children cumulated vsize (Kb) 12844 [startup+660.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2577 0 0 0 65957 25 0 0 25 0 1 0 1851904171 10977280 2564 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2680 2564 145 145 0 2535 0 [pid=1932] vsize: 10720 Current children cumulated CPU time (s) 659.83 Current children cumulated vsize (Kb) 12844 [startup+670.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2590 0 0 0 66957 25 0 0 25 0 1 0 1851904171 11030528 2577 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2693 2577 145 145 0 2548 0 [pid=1932] vsize: 10772 Current children cumulated CPU time (s) 669.83 Current children cumulated vsize (Kb) 12896 [startup+680.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2611 0 0 0 67957 25 0 0 25 0 1 0 1851904171 11145216 2598 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2721 2598 145 145 0 2576 0 [pid=1932] vsize: 10884 Current children cumulated CPU time (s) 679.83 Current children cumulated vsize (Kb) 13008 [startup+690.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2628 0 0 0 68957 25 0 0 25 0 1 0 1851904171 11218944 2615 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2739 2615 145 145 0 2594 0 [pid=1932] vsize: 10956 Current children cumulated CPU time (s) 689.83 Current children cumulated vsize (Kb) 13080 [startup+700.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2639 0 0 0 69957 25 0 0 25 0 1 0 1851904171 11268096 2626 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2751 2626 145 145 0 2606 0 [pid=1932] vsize: 11004 Current children cumulated CPU time (s) 699.83 Current children cumulated vsize (Kb) 13128 [startup+710.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2639 0 0 0 70957 25 0 0 25 0 1 0 1851904171 11268096 2626 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2751 2626 145 145 0 2606 0 [pid=1932] vsize: 11004 Current children cumulated CPU time (s) 709.83 Current children cumulated vsize (Kb) 13128 [startup+720.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2756 0 0 0 71955 26 0 0 25 0 1 0 1851904171 11735040 2743 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2865 2743 145 145 0 2720 0 [pid=1932] vsize: 11460 Current children cumulated CPU time (s) 719.82 Current children cumulated vsize (Kb) 13584 [startup+730.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2766 0 0 0 72955 27 0 0 25 0 1 0 1851904171 11784192 2753 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2877 2753 145 145 0 2732 0 [pid=1932] vsize: 11508 Current children cumulated CPU time (s) 729.83 Current children cumulated vsize (Kb) 13632 [startup+740.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2815 0 0 0 73954 27 0 0 25 0 1 0 1851904171 11988992 2802 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2927 2802 145 145 0 2782 0 [pid=1932] vsize: 11708 Current children cumulated CPU time (s) 739.82 Current children cumulated vsize (Kb) 13832 [startup+750.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2816 0 0 0 74954 27 0 0 25 0 1 0 1851904171 11988992 2803 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2927 2803 145 145 0 2782 0 [pid=1932] vsize: 11708 Current children cumulated CPU time (s) 749.82 Current children cumulated vsize (Kb) 13832 [startup+760.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2816 0 0 0 75955 27 0 0 25 0 1 0 1851904171 11988992 2803 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2927 2803 145 145 0 2782 0 [pid=1932] vsize: 11708 Current children cumulated CPU time (s) 759.83 Current children cumulated vsize (Kb) 13832 [startup+770.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2825 0 0 0 76955 27 0 0 25 0 1 0 1851904171 12034048 2812 4294967295 134512640 135094434 3221224432 3221223088 134557976 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2938 2812 145 145 0 2793 0 [pid=1932] vsize: 11752 Current children cumulated CPU time (s) 769.83 Current children cumulated vsize (Kb) 13876 [startup+780.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2875 0 0 0 77954 28 0 0 25 0 1 0 1851904171 12234752 2862 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2987 2862 145 145 0 2842 0 [pid=1932] vsize: 11948 Current children cumulated CPU time (s) 779.83 Current children cumulated vsize (Kb) 14072 [startup+790.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2875 0 0 0 78954 28 0 0 25 0 1 0 1851904171 12234752 2862 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 2987 2862 145 145 0 2842 0 [pid=1932] vsize: 11948 Current children cumulated CPU time (s) 789.83 Current children cumulated vsize (Kb) 14072 [startup+800.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2937 0 0 0 79954 29 0 0 25 0 1 0 1851904171 12500992 2924 4294967295 134512640 135094434 3221224432 3221223088 134557882 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1932/statm): 3052 2924 145 145 0 2907 0 [pid=1932] vsize: 12208 Current children cumulated CPU time (s) 799.84 Current children cumulated vsize (Kb) 14332 [startup+810.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2947 0 0 0 80953 29 0 0 25 0 1 0 1851904171 12550144 2934 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3064 2934 145 145 0 2919 0 [pid=1932] vsize: 12256 Current children cumulated CPU time (s) 809.83 Current children cumulated vsize (Kb) 14380 [startup+820.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2979 0 0 0 81953 29 0 0 25 0 1 0 1851904171 12693504 2966 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3099 2966 145 145 0 2954 0 [pid=1932] vsize: 12396 Current children cumulated CPU time (s) 819.83 Current children cumulated vsize (Kb) 14520 [startup+830.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2979 0 0 0 82953 29 0 0 25 0 1 0 1851904171 12693504 2966 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3099 2966 145 145 0 2954 0 [pid=1932] vsize: 12396 Current children cumulated CPU time (s) 829.83 Current children cumulated vsize (Kb) 14520 [startup+840.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2983 0 0 0 83953 29 0 0 25 0 1 0 1851904171 12709888 2970 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3103 2970 145 145 0 2958 0 [pid=1932] vsize: 12412 Current children cumulated CPU time (s) 839.83 Current children cumulated vsize (Kb) 14536 [startup+850.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 2994 0 0 0 84954 29 0 0 25 0 1 0 1851904171 12754944 2981 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3114 2981 145 145 0 2969 0 [pid=1932] vsize: 12456 Current children cumulated CPU time (s) 849.84 Current children cumulated vsize (Kb) 14580 [startup+860.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3005 0 0 0 85953 29 0 0 25 0 1 0 1851904171 12804096 2992 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/1932/statm): 3126 2992 145 145 0 2981 0 [pid=1932] vsize: 12504 Current children cumulated CPU time (s) 859.83 Current children cumulated vsize (Kb) 14628 [startup+870.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3099 0 0 0 86951 30 0 0 25 0 1 0 1851904171 13185024 3086 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3219 3086 145 145 0 3074 0 [pid=1932] vsize: 12876 Current children cumulated CPU time (s) 869.82 Current children cumulated vsize (Kb) 15000 [startup+880.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3105 0 0 0 87951 30 0 0 25 0 1 0 1851904171 13217792 3092 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3227 3092 145 145 0 3082 0 [pid=1932] vsize: 12908 Current children cumulated CPU time (s) 879.82 Current children cumulated vsize (Kb) 15032 [startup+890.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3110 0 0 0 88951 30 0 0 25 0 1 0 1851904171 13250560 3097 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3235 3097 145 145 0 3090 0 [pid=1932] vsize: 12940 Current children cumulated CPU time (s) 889.82 Current children cumulated vsize (Kb) 15064 [startup+900.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3110 0 0 0 89952 30 0 0 25 0 1 0 1851904171 13250560 3097 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3235 3097 145 145 0 3090 0 [pid=1932] vsize: 12940 Current children cumulated CPU time (s) 899.83 Current children cumulated vsize (Kb) 15064 [startup+910.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3112 0 0 0 90952 30 0 0 25 0 1 0 1851904171 13258752 3099 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3237 3099 145 145 0 3092 0 [pid=1932] vsize: 12948 Current children cumulated CPU time (s) 909.83 Current children cumulated vsize (Kb) 15072 [startup+920.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3115 0 0 0 91952 30 0 0 25 0 1 0 1851904171 13275136 3102 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3241 3102 145 145 0 3096 0 [pid=1932] vsize: 12964 Current children cumulated CPU time (s) 919.83 Current children cumulated vsize (Kb) 15088 [startup+930.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3115 0 0 0 92952 30 0 0 25 0 1 0 1851904171 13275136 3102 4294967295 134512640 135094434 3221224432 3221223120 134554733 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3241 3102 145 145 0 3096 0 [pid=1932] vsize: 12964 Current children cumulated CPU time (s) 929.83 Current children cumulated vsize (Kb) 15088 [startup+940.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3115 0 0 0 93952 31 0 0 25 0 1 0 1851904171 13275136 3102 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3241 3102 145 145 0 3096 0 [pid=1932] vsize: 12964 Current children cumulated CPU time (s) 939.84 Current children cumulated vsize (Kb) 15088 [startup+950.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3115 0 0 0 94953 31 0 0 25 0 1 0 1851904171 13275136 3102 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3241 3102 145 145 0 3096 0 [pid=1932] vsize: 12964 Current children cumulated CPU time (s) 949.85 Current children cumulated vsize (Kb) 15088 [startup+960.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3164 0 0 0 95952 31 0 0 25 0 1 0 1851904171 13488128 3151 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3293 3151 145 145 0 3148 0 [pid=1932] vsize: 13172 Current children cumulated CPU time (s) 959.84 Current children cumulated vsize (Kb) 15296 [startup+970.077 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3189 0 0 0 96952 31 0 0 25 0 1 0 1851904171 13598720 3176 4294967295 134512640 135094434 3221224432 3221223104 134556244 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3320 3176 145 145 0 3175 0 [pid=1932] vsize: 13280 Current children cumulated CPU time (s) 969.84 Current children cumulated vsize (Kb) 15404 [startup+980.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3194 0 0 0 97952 31 0 0 25 0 1 0 1851904171 13615104 3181 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3324 3181 145 145 0 3179 0 [pid=1932] vsize: 13296 Current children cumulated CPU time (s) 979.84 Current children cumulated vsize (Kb) 15420 [startup+990.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3273 0 0 0 98951 32 0 0 25 0 1 0 1851904171 13950976 3260 4294967295 134512640 135094434 3221224432 3221223104 134556156 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3406 3260 145 145 0 3261 0 [pid=1932] vsize: 13624 Current children cumulated CPU time (s) 989.84 Current children cumulated vsize (Kb) 15748 [startup+1000.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3279 0 0 0 99951 32 0 0 25 0 1 0 1851904171 14000128 3266 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3418 3266 145 145 0 3273 0 [pid=1932] vsize: 13672 Current children cumulated CPU time (s) 999.84 Current children cumulated vsize (Kb) 15796 [startup+1010.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3280 0 0 0 100951 32 0 0 25 0 1 0 1851904171 14000128 3267 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3418 3267 145 145 0 3273 0 [pid=1932] vsize: 13672 Current children cumulated CPU time (s) 1009.84 Current children cumulated vsize (Kb) 15796 [startup+1020.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3312 0 0 0 101951 33 0 0 25 0 1 0 1851904171 14118912 3299 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3447 3299 145 145 0 3302 0 [pid=1932] vsize: 13788 Current children cumulated CPU time (s) 1019.85 Current children cumulated vsize (Kb) 15912 [startup+1030.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3315 0 0 0 102951 33 0 0 25 0 1 0 1851904171 14135296 3302 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3451 3302 145 145 0 3306 0 [pid=1932] vsize: 13804 Current children cumulated CPU time (s) 1029.85 Current children cumulated vsize (Kb) 15928 [startup+1040.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3326 0 0 0 103951 33 0 0 25 0 1 0 1851904171 14184448 3313 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3463 3313 145 145 0 3318 0 [pid=1932] vsize: 13852 Current children cumulated CPU time (s) 1039.85 Current children cumulated vsize (Kb) 15976 [startup+1050.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3343 0 0 0 104950 34 0 0 25 0 1 0 1851904171 14254080 3330 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3480 3330 145 145 0 3335 0 [pid=1932] vsize: 13920 Current children cumulated CPU time (s) 1049.85 Current children cumulated vsize (Kb) 16044 [startup+1060.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3343 0 0 0 105949 35 0 0 25 0 1 0 1851904171 14254080 3330 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3480 3330 145 145 0 3335 0 [pid=1932] vsize: 13920 Current children cumulated CPU time (s) 1059.85 Current children cumulated vsize (Kb) 16044 [startup+1070.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3343 0 0 0 106949 35 0 0 25 0 1 0 1851904171 14254080 3330 4294967295 134512640 135094434 3221224432 3221222032 134562873 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3480 3330 145 145 0 3335 0 [pid=1932] vsize: 13920 Current children cumulated CPU time (s) 1069.85 Current children cumulated vsize (Kb) 16044 [startup+1080.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3343 0 0 0 107949 36 0 0 25 0 1 0 1851904171 14254080 3330 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3480 3330 145 145 0 3335 0 [pid=1932] vsize: 13920 Current children cumulated CPU time (s) 1079.86 Current children cumulated vsize (Kb) 16044 [startup+1090.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3349 0 0 0 108949 36 0 0 25 0 1 0 1851904171 14286848 3336 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3488 3336 145 145 0 3343 0 [pid=1932] vsize: 13952 Current children cumulated CPU time (s) 1089.86 Current children cumulated vsize (Kb) 16076 [startup+1100.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3360 0 0 0 109949 36 0 0 25 0 1 0 1851904171 14352384 3347 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3504 3347 145 145 0 3359 0 [pid=1932] vsize: 14016 Current children cumulated CPU time (s) 1099.86 Current children cumulated vsize (Kb) 16140 [startup+1110.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3360 0 0 0 110949 37 0 0 25 0 1 0 1851904171 14352384 3347 4294967295 134512640 135094434 3221224432 3221223088 134558172 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3504 3347 145 145 0 3359 0 [pid=1932] vsize: 14016 Current children cumulated CPU time (s) 1109.87 Current children cumulated vsize (Kb) 16140 [startup+1120.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3360 0 0 0 111949 37 0 0 25 0 1 0 1851904171 14352384 3347 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3504 3347 145 145 0 3359 0 [pid=1932] vsize: 14016 Current children cumulated CPU time (s) 1119.87 Current children cumulated vsize (Kb) 16140 [startup+1130.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3361 0 0 0 112949 37 0 0 25 0 1 0 1851904171 14352384 3348 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3504 3348 145 145 0 3359 0 [pid=1932] vsize: 14016 Current children cumulated CPU time (s) 1129.87 Current children cumulated vsize (Kb) 16140 [startup+1140.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3361 0 0 0 113948 37 0 0 25 0 1 0 1851904171 14352384 3348 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3504 3348 145 145 0 3359 0 [pid=1932] vsize: 14016 Current children cumulated CPU time (s) 1139.86 Current children cumulated vsize (Kb) 16140 [startup+1150.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3363 0 0 0 114949 37 0 0 25 0 1 0 1851904171 14352384 3350 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3504 3350 145 145 0 3359 0 [pid=1932] vsize: 14016 Current children cumulated CPU time (s) 1149.87 Current children cumulated vsize (Kb) 16140 [startup+1160.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3363 0 0 0 115948 38 0 0 25 0 1 0 1851904171 14352384 3350 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3504 3350 145 145 0 3359 0 [pid=1932] vsize: 14016 Current children cumulated CPU time (s) 1159.87 Current children cumulated vsize (Kb) 16140 [startup+1170.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3363 0 0 0 116949 38 0 0 25 0 1 0 1851904171 14352384 3350 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3504 3350 145 145 0 3359 0 [pid=1932] vsize: 14016 Current children cumulated CPU time (s) 1169.88 Current children cumulated vsize (Kb) 16140 [startup+1180.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3363 0 0 0 117949 38 0 0 25 0 1 0 1851904171 14352384 3350 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3504 3350 145 145 0 3359 0 [pid=1932] vsize: 14016 Current children cumulated CPU time (s) 1179.88 Current children cumulated vsize (Kb) 16140 [startup+1190.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3363 0 0 0 118949 38 0 0 25 0 1 0 1851904171 14352384 3350 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3504 3350 145 145 0 3359 0 [pid=1932] vsize: 14016 Current children cumulated CPU time (s) 1189.88 Current children cumulated vsize (Kb) 16140 [startup+1200.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3363 0 0 0 119949 38 0 0 25 0 1 0 1851904171 14352384 3350 4294967295 134512640 135094434 3221224432 3221223088 134558033 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3504 3350 145 145 0 3359 0 [pid=1932] vsize: 14016 Current children cumulated CPU time (s) 1199.88 Current children cumulated vsize (Kb) 16140 [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3363 0 0 0 120949 38 0 0 25 0 1 0 1851904171 14352384 3350 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3504 3350 145 145 0 3359 0 [pid=1932] vsize: 14016 Current children cumulated CPU time (s) 1209.88 Current children cumulated vsize (Kb) 16140 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 1932 Raw data (/proc/1928/stat): 1928 (minisat+_script) S 1927 1928 20728 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1851904166 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/1928/statm): 531 226 485 147 0 384 0 [pid=1928] vsize: 2124 Raw data (/proc/1932/stat): 1932 (minisat+_64-bit) R 1928 1928 20728 0 -1 0 3363 0 0 0 120949 38 0 0 25 0 1 0 1851904171 14352384 3350 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/1932/statm): 3504 3350 145 145 0 3359 0 [pid=1932] vsize: 14016 Current children cumulated CPU time (s) 1209.88 Current children cumulated vsize (Kb) 16140 Sending SIGTERM to -1928 Sleeping 2 seconds One traced child (pid=1928) ended because it received signal 15 (SIGTERM) One traced child (pid=1932) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.11 CPU time (s): 1209.89 CPU user time (s): 1209.5 CPU system time (s): 0.39394 CPU usage (%): 99.9823 Max. virtual memory (cumulated for all children) (Kb): 16140
ERROR: no interpretation found !