Name | mps-v2-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-p0201.opb |
MD5SUM | 8c361d02d5162bb0b133ab6ed38f9294 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 1523 |
Optimality of the best value was proved | YES |
Number of terms in the objective function | 201 |
Biggest coefficient in the objective function | 1920 |
Number of bits for the biggest coefficient in the objective function | 11 |
Sum of the numbers in the objective function | 19980 |
Number of bits of the sum of numbers in the objective function | 15 |
Biggest number in a constraint | 1920 |
Number of bits of the biggest number in a constraint | 11 |
Biggest sum of numbers in a constraint | 19980 |
Number of bits of the biggest sum of numbers | 15 |
Best result obtained on this benchmark | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 212.013 |
Number of variables | 201 |
Total number of constraints | 334 |
Number of constraints which are clauses | 20 |
Number of constraints which are cardinality constraints (but not clauses) | 227 |
Number of constraints which are nor clauses,nor cardinality constraints | 87 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 67 |
LAUNCH ON wulflinc28 THE 2005-09-19 18:05:52 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2996 boxname=wulflinc28 idbench=652 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 8c361d02d5162bb0b133ab6ed38f9294 /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-20-10-p0201.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-20-10-p0201.opb IDLAUNCH: 2996 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.077 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.077 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: 840328 kB Buffers: 35704 kB Cached: 130064 kB SwapCached: 696 kB Active: 75316 kB Inactive: 93032 kB HighTotal: 131008 kB HighFree: 34972 kB LowTotal: 903652 kB LowFree: 805356 kB SwapTotal: 2097640 kB SwapFree: 2096372 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5816 kB Slab: 20252 kB Committed_AS: 64164 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-19 18:26:03 (client local time) WITH STATUS 10 IN 1209.75 SECONDS stats: 2996 7 1209.75 10
c Parsing PB file... c Converting 133 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: #################### c -- Clauses(.)/Splits(s): sssss c ---[ 137]---> BDD-cost: 3 c ---[ 136]---> BDD-cost: 3 c ---[ 135]---> BDD-cost: 3 c ---[ 133]---> BDD-cost: 15 c ---[ 131]---> BDD-cost: 15 c ---[ 129]---> BDD-cost: 15 c ---[ 127]---> BDD-cost: 15 c ---[ 125]---> BDD-cost: 15 c ---[ 123]---> BDD-cost: 15 c ---[ 121]---> BDD-cost: 15 c ---[ 119]---> BDD-cost: 15 c ---[ 117]---> BDD-cost: 15 c ---[ 115]---> BDD-cost: 15 c ---[ 113]---> BDD-cost: 15 c ---[ 111]---> BDD-cost: 15 c ---[ 109]---> BDD-cost: 15 c ---[ 107]---> BDD-cost: 15 c ---[ 105]---> BDD-cost: 15 c ---[ 103]---> BDD-cost: 15 c ---[ 101]---> BDD-cost: 15 c ---[ 99]---> BDD-cost: 15 c ---[ 97]---> BDD-cost: 15 c ---[ 95]---> BDD-cost: 15 c ---[ 89]---> BDD-cost: 39 c ---[ 88]---> BDD-cost: 42 c ---[ 87]---> BDD-cost: 42 c ---[ 86]---> BDD-cost: 54 c ---[ 85]---> BDD-cost: 73 c ---[ 84]---> BDD-cost: 73 c ---[ 83]---> BDD-cost: 98 c ---[ 82]---> BDD-cost: 85 c ---[ 81]---> BDD-cost: 85 c ---[ 80]---> BDD-cost: 160 c ---[ 79]---> BDD-cost: 107 c ---[ 78]---> BDD-cost: 107 c ---[ 77]---> BDD-cost: 201 c ---[ 76]---> BDD-cost: 128 c ---[ 75]---> BDD-cost: 128 c ---[ 74]---> BDD-cost: 241 c ---[ 73]---> BDD-cost: 150 c ---[ 72]---> BDD-cost: 150 c ---[ 71]---> BDD-cost: 281 c ---[ 70]---> BDD-cost: 172 c ---[ 69]---> BDD-cost: 172 c ---[ 68]---> BDD-cost: 321 c ---[ 67]---> BDD-cost: 194 c ---[ 66]---> BDD-cost: 194 c ---[ 65]---> BDD-cost: 361 c ---[ 64]---> BDD-cost: 3 c ---[ 63]---> BDD-cost: 3 c ---[ 62]---> BDD-cost: 3 c ---[ 61]---> BDD-cost: 3 c ---[ 60]---> BDD-cost: 3 c ---[ 59]---> BDD-cost: 3 c ---[ 58]---> BDD-cost: 9 c ---[ 57]---> BDD-cost: 11 c ---[ 56]---> BDD-cost: 11 c ---[ 55]---> BDD-cost: 9 c ---[ 54]---> BDD-cost: 11 c ---[ 53]---> BDD-cost: 11 c ---[ 52]---> BDD-cost: 9 c ---[ 51]---> BDD-cost: 11 c ---[ 50]---> BDD-cost: 11 c ---[ 49]---> BDD-cost: 9 c ---[ 48]---> BDD-cost: 11 c ---[ 47]---> BDD-cost: 11 c ---[ 46]---> BDD-cost: 9 c ---[ 45]---> BDD-cost: 11 c ---[ 44]---> BDD-cost: 11 c ---[ 43]---> BDD-cost: 9 c ---[ 42]---> BDD-cost: 11 c ---[ 41]---> BDD-cost: 11 c ---[ 40]---> BDD-cost: 9 c ---[ 39]---> BDD-cost: 11 c ---[ 38]---> BDD-cost: 11 c ---[ 37]---> BDD-cost: 9 c ---[ 36]---> BDD-cost: 11 c ---[ 35]---> BDD-cost: 11 c ---[ 34]---> BDD-cost: 9 c ---[ 33]---> BDD-cost: 11 c ---[ 32]---> BDD-cost: 11 c ---[ 31]---> BDD-cost: 9 c ---[ 30]---> BDD-cost: 11 c ---[ 29]---> BDD-cost: 11 c ---[ 28]---> BDD-cost: 9 c ---[ 27]---> BDD-cost: 11 c ---[ 26]---> BDD-cost: 11 c ---[ 25]---> BDD-cost: 9 c ---[ 24]---> BDD-cost: 11 c ---[ 23]---> BDD-cost: 11 c ---[ 22]---> BDD-cost: 9 c ---[ 21]---> BDD-cost: 11 c ---[ 20]---> BDD-cost: 11 c ---[ 19]---> BDD-cost: 9 c ---[ 18]---> BDD-cost: 11 c ---[ 17]---> BDD-cost: 11 c ---[ 16]---> BDD-cost: 9 c ---[ 15]---> BDD-cost: 11 c ---[ 14]---> BDD-cost: 11 c ---[ 13]---> BDD-cost: 9 c ---[ 12]---> BDD-cost: 11 c ---[ 11]---> BDD-cost: 11 c ---[ 10]---> BDD-cost: 9 c ---[ 9]---> BDD-cost: 11 c ---[ 8]---> BDD-cost: 11 c ---[ 7]---> BDD-cost: 9 c ---[ 6]---> BDD-cost: 11 c ---[ 5]---> BDD-cost: 11 c ---[ 4]---> BDD-cost: 1 c ---[ 3]---> BDD-cost: 1 c ---[ 2]---> BDD-cost: 1 c ---[ 1]---> BDD-cost: 1 c ---[ 0]---> BDD-cost: 1 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 11741 34621 | 3913 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 2213[0m c ---[ 0]---> Sorter-cost:21097 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 58 | 58177 143044 | 19392 56 148 2.6 | 0.000 % | c ============================================================================== c [1mFound solution: 2087[0m c ---[ 0]---> Sorter-cost: 6 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 88 | 58581 144183 | 19527 81 549 6.8 | 0.000 % | c | 188 | 58581 144183 | 21479 181 2385 13.2 | 0.542 % | c ============================================================================== c [1mFound solution: 2077[0m c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 307 | 58494 144055 | 19498 298 8553 28.7 | 0.542 % | c | 409 | 57412 141593 | 21447 382 9171 24.0 | 1.991 % | c | 559 | 54361 134594 | 23592 487 9880 20.3 | 5.933 % | c ============================================================================== c [1mFound solution: 2076[0m c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 612 | 54176 134172 | 18058 537 12758 23.8 | 5.933 % | c | 712 | 53761 133220 | 19863 632 13949 22.1 | 6.753 % | c | 862 | 53131 131774 | 21850 768 17863 23.3 | 7.596 % | c ============================================================================== c [1mFound solution: 2015[0m c ---[ 0]---> Sorter-cost: 5 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1004 | 53241 132050 | 17747 910 28831 31.7 | 7.596 % | c | 1106 | 53176 131902 | 19521 1010 30785 30.5 | 7.667 % | c | 1256 | 53016 131530 | 21473 1157 35572 30.7 | 7.907 % | c | 1482 | 50129 124875 | 23621 1328 39088 29.4 | 11.871 % | c ============================================================================== c [1mFound solution: 2014[0m c ---[ 0]---> Sorter-cost: 5 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1689 | 50199 125050 | 16733 1535 47004 30.6 | 11.871 % | c | 1790 | 50164 124959 | 18406 1635 47984 29.3 | 11.926 % | c | 1941 | 50143 124911 | 20246 1784 49437 27.7 | 12.060 % | c | 2166 | 48818 121858 | 22271 1852 53041 28.6 | 13.758 % | c | 2503 | 48818 121858 | 24498 2189 83892 38.3 | 13.758 % | c | 3010 | 48250 120520 | 26948 2656 108054 40.7 | 14.588 % | c ============================================================================== c [1mFound solution: 2008[0m c ---[ 0]---> Sorter-cost: 5 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3349 | 47655 119142 | 15885 2985 116858 39.1 | 14.588 % | c | 3450 | 47645 119116 | 17473 3083 122439 39.7 | 15.446 % | c | 3600 | 47645 119116 | 19220 3233 125119 38.7 | 15.446 % | c ============================================================================== c [1mFound solution: 1944[0m c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3684 | 47645 119119 | 15881 3313 128636 38.8 | 15.446 % | c | 3784 | 47642 119110 | 17469 3408 133871 39.3 | 15.463 % | c | 3937 | 47525 118845 | 19216 3555 134588 37.9 | 15.628 % | c | 4162 | 46824 117216 | 21137 3767 144530 38.4 | 16.636 % | c ============================================================================== c [1mFound solution: 1924[0m c ---[ 0]---> Sorter-cost: 3 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4272 | 46828 117225 | 15609 3877 149017 38.4 | 16.636 % | c | 4376 | 46828 117225 | 17169 3981 153904 38.7 | 16.638 % | c | 4526 | 46129 115608 | 18886 4104 160348 39.1 | 17.606 % | c | 4754 | 46129 115608 | 20775 4332 167592 38.7 | 17.606 % | c | 5092 | 46129 115608 | 22853 4670 179196 38.4 | 17.606 % | c | 5598 | 46129 115608 | 25138 5176 190777 36.9 | 17.606 % | c | 6359 | 45838 114933 | 27652 5928 228619 38.6 | 17.997 % | c ============================================================================== c [1mFound solution: 1919[0m c ---[ 0]---> Sorter-cost: 5 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6462 | 45848 114959 | 15282 6027 234251 38.9 | 17.997 % | c | 6563 | 45848 114959 | 16810 6128 237549 38.8 | 18.005 % | c | 6715 | 45543 114264 | 18491 6275 247244 39.4 | 18.404 % | c ============================================================================== c [1mFound solution: 1918[0m c ---[ 0]---> Sorter-cost: 3 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6777 | 45548 114281 | 15182 6337 248676 39.2 | 18.404 % | c | 6880 | 45548 114281 | 16700 6440 251831 39.1 | 18.405 % | c | 7031 | 45548 114281 | 18370 6591 255386 38.7 | 18.405 % | c | 7257 | 45484 114134 | 20207 6815 263672 38.7 | 18.488 % | c ============================================================================== c [1mFound solution: 1916[0m c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7344 | 45488 114145 | 15162 6902 267676 38.8 | 18.488 % | c | 7444 | 45488 114145 | 16678 7002 274101 39.1 | 18.490 % | c | 7594 | 45488 114145 | 18346 7152 280094 39.2 | 18.490 % | c | 7820 | 45488 114145 | 20180 7378 284897 38.6 | 18.490 % | c | 8157 | 45484 114137 | 22198 7713 291786 37.8 | 18.498 % | c ============================================================================== c [1mFound solution: 1846[0m c ---[ 0]---> Sorter-cost: 5 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8275 | 45493 114162 | 15164 7831 301898 38.6 | 18.498 % | c | 8376 | 45493 114162 | 16680 7932 304635 38.4 | 18.498 % | c | 8526 | 45493 114162 | 18348 8082 310387 38.4 | 18.498 % | c | 8751 | 45493 114162 | 20183 8307 326338 39.3 | 18.498 % | c | 9088 | 45493 114162 | 22201 8644 350743 40.6 | 18.498 % | c | 9595 | 45487 114149 | 24421 9149 378954 41.4 | 18.507 % | c ============================================================================== c [1mFound solution: 1843[0m c ---[ 0]---> Sorter-cost: 5 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9817 | 45493 114164 | 15164 9371 396771 42.3 | 18.507 % | c | 9917 | 45493 114164 | 16680 9471 405490 42.8 | 18.508 % | c | 10067 | 45043 113120 | 18348 9590 409422 42.7 | 19.128 % | c | 10292 | 44860 112696 | 20183 9807 421869 43.0 | 19.384 % | c | 10629 | 44704 112330 | 22201 10139 441298 43.5 | 19.592 % | c | 11139 | 44704 112330 | 24421 10649 466222 43.8 | 19.592 % | c | 11898 | 44680 112268 | 26863 11369 490362 43.1 | 19.626 % | c | 13040 | 44680 112268 | 29550 12511 608632 48.6 | 19.626 % | c | 14752 | 44669 112242 | 32505 14218 720930 50.7 | 19.644 % | c ============================================================================== c [1mFound solution: 1769[0m c ---[ 0]---> Sorter-cost: 3 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15639 | 44689 112297 | 14896 15105 787606 52.1 | 19.644 % | c | 15739 | 44614 112122 | 16385 15204 791922 52.1 | 19.753 % | c | 15889 | 44609 112109 | 18024 15353 803812 52.4 | 19.762 % | c | 16116 | 44609 112109 | 19826 15580 814384 52.3 | 19.762 % | c | 16454 | 44605 112100 | 21809 15917 838394 52.7 | 19.766 % | c | 16960 | 44590 112061 | 23990 16418 854500 52.0 | 19.792 % | c | 17719 | 44590 112061 | 26389 17177 917295 53.4 | 19.792 % | c | 18859 | 44590 112061 | 29028 18317 999570 54.6 | 19.792 % | c | 20567 | 44590 112061 | 31930 20025 1075528 53.7 | 19.792 % | c | 23130 | 44178 111114 | 35123 22532 1237111 54.9 | 20.394 % | c | 26974 | 44157 111063 | 38636 26371 1393049 52.8 | 20.433 % | c | 32744 | 44139 111013 | 42500 32137 1636168 50.9 | 20.455 % | c | 41393 | 42971 108270 | 46750 40731 2120834 52.1 | 22.110 % | c ============================================================================== c [1mFound solution: 1761[0m c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 48818 | 42886 108076 | 14295 48152 2633672 54.7 | 22.110 % | c | 48918 | 42886 108076 | 15724 17188 786843 45.8 | 22.254 % | c | 49070 | 42886 108076 | 17296 17340 794497 45.8 | 22.254 % | c | 49296 | 42886 108076 | 19026 17566 802504 45.7 | 22.254 % | c | 49635 | 42886 108076 | 20929 17905 826393 46.2 | 22.254 % | c | 50142 | 42886 108076 | 23022 18412 865716 47.0 | 22.254 % | c | 50902 | 42878 108060 | 25324 19169 913273 47.6 | 22.271 % | c ============================================================================== c [1mFound solution: 1759[0m c ---[ 0]---> Sorter-cost: 5 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 51206 | 42886 108079 | 14295 19473 926514 47.6 | 22.271 % | c | 51310 | 42803 107886 | 15724 9838 411836 41.9 | 22.392 % | c | 51460 | 42701 107650 | 17296 9986 422304 42.3 | 22.539 % | c | 51685 | 42697 107641 | 19026 10209 428287 42.0 | 22.543 % | c | 52023 | 42432 107026 | 20929 10519 434920 41.3 | 22.898 % | c | 52529 | 42432 107026 | 23022 11025 448791 40.7 | 22.898 % | c | 53292 | 42432 107026 | 25324 11788 467859 39.7 | 22.898 % | c ============================================================================== c [1mFound solution: 1756[0m c ---[ 0]---> Sorter-cost: 3 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 54231 | 42437 107038 | 14145 12727 559381 44.0 | 22.898 % | c | 54331 | 42437 107038 | 15559 12827 560789 43.7 | 22.900 % | c | 54481 | 42437 107038 | 17115 12977 573557 44.2 | 22.900 % | c | 54706 | 42434 107029 | 18826 13198 579935 43.9 | 22.904 % | c | 55043 | 42434 107029 | 20709 13535 601435 44.4 | 22.904 % | c | 55550 | 42434 107029 | 22780 14042 661065 47.1 | 22.904 % | c | 56309 | 42401 106930 | 25058 14797 680051 46.0 | 22.952 % | c | 57449 | 42322 106745 | 27564 15935 760344 47.7 | 23.069 % | c ============================================================================== c [1mFound solution: 1749[0m c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 58385 | 42200 106464 | 14066 16861 826619 49.0 | 23.069 % | c | 58485 | 42200 106464 | 15472 16961 829910 48.9 | 23.248 % | c | 58635 | 42200 106464 | 17019 17111 836797 48.9 | 23.248 % | c | 58860 | 42200 106464 | 18721 17336 867691 50.1 | 23.248 % | c | 59197 | 42200 106464 | 20594 17673 885830 50.1 | 23.248 % | c | 59703 | 42200 106464 | 22653 18179 915589 50.4 | 23.249 % | c | 60462 | 42196 106456 | 24918 18937 964396 50.9 | 23.257 % | c | 61604 | 42196 106456 | 27410 20079 1033370 51.5 | 23.257 % | c | 63312 | 42196 106456 | 30151 21787 1114193 51.1 | 23.257 % | c | 65874 | 42196 106456 | 33166 24349 1253412 51.5 | 23.257 % | c | 69718 | 42187 106435 | 36483 28190 1394186 49.5 | 23.274 % | c ============================================================================== c [1mFound solution: 1743[0m c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 72990 | 42189 106437 | 14063 31459 1576631 50.1 | 23.274 % | c | 73091 | 42189 106437 | 15469 15831 562887 35.6 | 23.281 % | c | 73241 | 42189 106437 | 17016 15981 566465 35.4 | 23.281 % | c | 73466 | 42189 106437 | 18717 16206 570598 35.2 | 23.281 % | c | 73805 | 41908 105779 | 20589 16536 579979 35.1 | 23.705 % | c | 74311 | 41662 105210 | 22648 17030 627126 36.8 | 24.048 % | c | 75070 | 41523 104885 | 24913 17781 648143 36.5 | 24.251 % | c | 76211 | 41523 104885 | 27404 18922 717960 37.9 | 24.251 % | c | 77919 | 41512 104854 | 30145 20628 782194 37.9 | 24.268 % | c | 80484 | 41512 104854 | 33159 23193 910444 39.3 | 24.268 % | c | 84329 | 40399 102256 | 36475 26987 1186359 44.0 | 25.849 % | c | 90099 | 39769 100788 | 40123 32705 1642873 50.2 | 26.758 % | c | 98749 | 39730 100682 | 44135 41347 2170899 52.5 | 26.819 % | c | 111725 | 39713 100639 | 48549 54317 3086904 56.8 | 26.849 % | c ============================================================================== c [1mFound solution: 1741[0m c ---[ 0]---> Sorter-cost: 1 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 118195 | 39699 100609 | 13233 23258 1388829 59.7 | 26.849 % | c | 118296 | 39689 100586 | 14556 11727 665419 56.7 | 26.884 % | c | 118446 | 39679 100560 | 16011 11873 670901 56.5 | 26.902 % | c | 118671 | 39679 100560 | 17613 12098 687485 56.8 | 26.902 % | c | 119008 | 39679 100560 | 19374 12435 703065 56.5 | 26.902 % | c | 119514 | 39679 100560 | 21311 12941 720728 55.7 | 26.902 % | c ============================================================================== c [1mFound solution: 1729[0m c ---[ 0]---> Sorter-cost: 3 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 119798 | 39683 100570 | 13227 13225 738497 55.8 | 26.902 % | c | 119900 | 39683 100570 | 14549 13327 742833 55.7 | 26.902 % | c | 120052 | 39683 100570 | 16004 13479 752015 55.8 | 26.902 % | c | 120277 | 39683 100570 | 17605 13704 756186 55.2 | 26.902 % | c | 120614 | 39683 100570 | 19365 14041 782319 55.7 | 26.902 % | c | 121120 | 39683 100570 | 21302 14547 817325 56.2 | 26.902 % | c | 121880 | 39683 100570 | 23432 15307 877308 57.3 | 26.902 % | c | 123019 | 39659 100511 | 25775 16443 938598 57.1 | 26.937 % | c | 124729 | 39659 100511 | 28353 18153 1000399 55.1 | 26.937 % | c ============================================================================== c [1mFound solution: 1701[0m c ---[ 0]---> Sorter-cost: 2 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 125372 | 39664 100522 | 13221 18796 1039475 55.3 | 26.937 % | c | 125473 | 39664 100522 | 14543 18897 1043357 55.2 | 26.938 % | c | 125623 | 39664 100522 | 15997 19047 1048216 55.0 | 26.938 % | c | 125848 | 39664 100522 | 17597 19272 1057344 54.9 | 26.938 % | c | 126186 | 39664 100522 | 19356 19610 1080876 55.1 | 26.938 % | c | 126693 | 39650 100490 | 21292 20114 1106316 55.0 | 26.955 % | c | 127452 | 39650 100490 | 23421 20873 1170355 56.1 | 26.955 % | c | 128592 | 39650 100490 | 25763 22013 1242185 56.4 | 26.955 % | c | 130300 | 39650 100490 | 28340 23721 1375243 58.0 | 26.955 % | c | 132866 | 39647 100481 | 31174 26285 1590875 60.5 | 26.960 % | c | 136710 | 39637 100455 | 34291 30126 1822172 60.5 | 26.977 % | c | 142477 | 39637 100455 | 37721 35893 2196023 61.2 | 26.977 % | c ============================================================================== c [1mFound solution: 1696[0m c ---[ 0]---> Sorter-cost: 2 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 143937 | 39642 100466 | 13214 37353 2277346 61.0 | 26.977 % | c | 144038 | 39642 100466 | 14535 16962 764796 45.1 | 26.978 % | c | 144188 | 39642 100466 | 15988 17112 775442 45.3 | 26.978 % | c | 144413 | 39642 100466 | 17587 17337 780597 45.0 | 26.978 % | c | 144751 | 39642 100466 | 19346 17675 798050 45.2 | 26.978 % | c | 145257 | 39642 100466 | 21281 18181 821444 45.2 | 26.978 % | c | 146016 | 39642 100466 | 23409 18940 863635 45.6 | 26.978 % | c | 147155 | 39642 100466 | 25750 20079 904913 45.1 | 26.978 % | c ============================================================================== c [1mFound solution: 1693[0m c ---[ 0]---> Sorter-cost: 3 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 148336 | 39644 100469 | 13214 21259 971574 45.7 | 26.978 % | c | 148436 | 39644 100469 | 14535 10730 315161 29.4 | 26.983 % | c | 148586 | 39644 100469 | 15988 10880 321998 29.6 | 26.983 % | c | 148812 | 39644 100469 | 17587 11106 328461 29.6 | 26.983 % | c | 149149 | 39644 100469 | 19346 11443 344450 30.1 | 26.983 % | c | 149655 | 39644 100469 | 21281 11949 382445 32.0 | 26.983 % | c | 150416 | 39644 100469 | 23409 12710 427011 33.6 | 26.983 % | c | 151555 | 39644 100469 | 25750 13849 492378 35.6 | 26.983 % | c | 153265 | 39644 100469 | 28325 15559 622810 40.0 | 26.983 % | c | 155829 | 39632 100439 | 31157 18121 766535 42.3 | 27.004 % | c | 159673 | 39632 100439 | 34273 21965 1039505 47.3 | 27.005 % | c | 165445 | 39622 100413 | 37701 27733 1317732 47.5 | 27.022 % | c ============================================================================== c [1mFound solution: 1679[0m c ---[ 0]---> Sorter-cost: 2 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 171269 | 39638 100455 | 13212 33557 1651605 49.2 | 27.022 % | c | 171371 | 39638 100455 | 14533 16881 647248 38.3 | 27.014 % | c | 171521 | 39638 100455 | 15986 17031 651040 38.2 | 27.014 % | c | 171746 | 39638 100455 | 17585 17256 662783 38.4 | 27.014 % | c | 172085 | 39638 100455 | 19343 17595 685001 38.9 | 27.014 % | c | 172592 | 39638 100455 | 21278 18102 701598 38.8 | 27.014 % | c ============================================================================== c [1mFound solution: 1677[0m c ---[ 0]---> Sorter-cost: 4 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 172877 | 39643 100472 | 13214 18387 719968 39.2 | 27.014 % | c | 172977 | 39643 100472 | 14535 18487 724554 39.2 | 27.014 % | c | 173127 | 39643 100472 | 15988 18637 729431 39.1 | 27.014 % | c | 173352 | 39643 100472 | 17587 18862 740892 39.3 | 27.014 % | c | 173689 | 39643 100472 | 19346 19199 754655 39.3 | 27.014 % | c | 174196 | 39643 100472 | 21281 19706 785502 39.9 | 27.014 % | c | 174955 | 39411 99937 | 23409 20453 819913 40.1 | 27.360 % | c | 176094 | 39397 99904 | 25750 21590 847207 39.2 | 27.360 % | c | 177807 | 39249 99557 | 28325 23293 943484 40.5 | 27.572 % | c | 180369 | 39249 99557 | 31157 25855 1038523 40.2 | 27.572 % | c | 184213 | 39249 99557 | 34273 29699 1239558 41.7 | 27.572 % | c ============================================================================== c [1mFound solution: 1672[0m c ---[ 0]---> Sorter-cost: 5 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 187009 | 39256 99582 | 13085 32495 1391426 42.8 | 27.572 % | c | 187111 | 39256 99582 | 14393 16350 570794 34.9 | 27.570 % | c | 187263 | 39256 99582 | 15832 16502 578503 35.1 | 27.570 % | c | 187490 | 39247 99555 | 17416 16726 588517 35.2 | 27.583 % | c | 187827 | 39235 99519 | 19157 17060 611560 35.8 | 27.601 % | c | 188334 | 39235 99519 | 21073 17567 634162 36.1 | 27.601 % | c | 189094 | 39229 99501 | 23180 18325 668812 36.5 | 27.609 % | c | 190234 | 39229 99501 | 25498 19465 738337 37.9 | 27.609 % | c | 191943 | 39223 99483 | 28048 21173 832692 39.3 | 27.618 % | c | 194505 | 39223 99483 | 30853 23735 931114 39.2 | 27.618 % | c | 198349 | 39223 99483 | 33939 27579 1169224 42.4 | 27.618 % | c | 204115 | 39223 99483 | 37333 33345 1491711 44.7 | 27.618 % | c | 212764 | 39217 99465 | 41066 41992 2071589 49.3 | 27.626 % | c ============================================================================== c [1mFound solution: 1665[0m c ---[ 0]---> Sorter-cost: 5 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 214192 | 39225 99484 | 13075 43420 2150246 49.5 | 27.626 % | c | 214293 | 39225 99484 | 14382 17445 812180 46.6 | 27.625 % | c | 214443 | 39225 99484 | 15820 17595 819216 46.6 | 27.625 % | c | 214668 | 39225 99484 | 17402 17820 834210 46.8 | 27.625 % | c | 215008 | 39203 99433 | 19143 18153 847906 46.7 | 27.655 % | c | 215515 | 39203 99433 | 21057 18660 879984 47.2 | 27.655 % | c | 216274 | 39203 99433 | 23163 19419 913894 47.1 | 27.655 % | c | 217413 | 39203 99433 | 25479 20558 970424 47.2 | 27.655 % | c | 219121 | 38981 98922 | 28027 22264 1088223 48.9 | 27.945 % | c | 221684 | 38981 98922 | 30830 24827 1212727 48.8 | 27.945 % | c | 225528 | 38981 98922 | 33913 28671 1371799 47.8 | 27.945 % | c | 231294 | 38981 98922 | 37304 34437 1650776 47.9 | 27.945 % | c ============================================================================== c [1mFound solution: 1649[0m c ---[ 0]---> Sorter-cost: 2 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 237485 | 38974 98903 | 12991 40623 1971527 48.5 | 27.945 % | c | 237586 | 38974 98903 | 14290 17766 648734 36.5 | 27.967 % | c | 237737 | 38974 98903 | 15719 17917 654797 36.5 | 27.967 % | c | 237962 | 38974 98903 | 17291 18142 666798 36.8 | 27.967 % | c | 238301 | 38974 98903 | 19020 18481 684022 37.0 | 27.967 % | c | 238807 | 38974 98903 | 20922 18987 707043 37.2 | 27.967 % | c | 239566 | 38942 98829 | 23014 19745 747250 37.8 | 28.010 % | c | 240705 | 38942 98829 | 25315 20884 807899 38.7 | 28.010 % | c | 242413 | 38942 98829 | 27847 22592 913056 40.4 | 28.010 % | c | 244977 | 38942 98829 | 30632 25156 1061313 42.2 | 28.010 % | c | 248822 | 38942 98829 | 33695 29001 1230713 42.4 | 28.010 % | c | 254589 | 38942 98829 | 37064 34768 1572707 45.2 | 28.010 % | c | 263239 | 38942 98829 | 40771 43418 2149352 49.5 | 28.010 % | c ============================================================================== c [1mFound solution: 1644[0m c ---[ 0]---> Sorter-cost: 2 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 264270 | 38947 98840 | 12982 44449 2208838 49.7 | 28.010 % | c | 264370 | 38947 98840 | 14280 18634 814489 43.7 | 28.011 % | c | 264521 | 38947 98840 | 15708 18785 819644 43.6 | 28.011 % | c | 264747 | 38947 98840 | 17279 19011 829567 43.6 | 28.011 % | c | 265085 | 38947 98840 | 19006 19349 847697 43.8 | 28.011 % | c | 265593 | 38947 98840 | 20907 19857 867080 43.7 | 28.011 % | c | 266352 | 38947 98840 | 22998 20616 900910 43.7 | 28.011 % | c | 267491 | 38947 98840 | 25298 21755 959365 44.1 | 28.011 % | c | 269199 | 38947 98840 | 27828 23463 1057461 45.1 | 28.011 % | c | 271762 | 38947 98840 | 30610 26026 1177586 45.2 | 28.011 % | c | 275607 | 38947 98840 | 33671 29871 1378191 46.1 | 28.011 % | c | 281374 | 38947 98840 | 37039 35638 1645153 46.2 | 28.011 % | c ============================================================================== c [1mFound solution: 1643[0m c ---[ 0]---> Sorter-cost: 3 Base: 5 2 3 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 289757 | 38952 98852 | 12984 44021 2047298 46.5 | 28.011 % | c | 289862 | 38748 98381 | 14282 17891 627874 35.1 | 28.297 % |
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/11672/stat): 11672 (minisat+_script) R 11671 11672 20115 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1851932777 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/11672/statm): 174 3 169 147 0 27 0 [pid=11672] 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=11673 New process pid=11674 New process pid=11675 execve syscall for /bin/sed executable 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 One traced child (pid=11674) exited with status: 0 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=11675) exited with status: 0 One traced child (pid=11673) exited with status: 0 New process pid=11676 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-20-10-p0201.opb [startup+10.004 s] Raw data (loadavg): 0.87 0.94 0.87 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 2189 0 0 0 977 9 0 0 25 0 1 0 1851932782 9678848 2124 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11676/statm): 2363 2124 145 145 0 2218 0 [pid=11676] vsize: 9452 Current children cumulated CPU time (s) 9.86 Current children cumulated vsize (Kb) 11576 [startup+20.0046 s] Raw data (loadavg): 0.89 0.94 0.87 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 2323 0 0 0 1974 11 0 0 25 0 1 0 1851932782 10227712 2258 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 2497 2258 145 145 0 2352 0 [pid=11676] vsize: 9988 Current children cumulated CPU time (s) 19.85 Current children cumulated vsize (Kb) 12112 [startup+30.0053 s] Raw data (loadavg): 0.91 0.94 0.87 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 2485 0 0 0 2972 11 0 0 25 0 1 0 1851932782 10895360 2420 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 2660 2420 145 145 0 2515 0 [pid=11676] vsize: 10640 Current children cumulated CPU time (s) 29.83 Current children cumulated vsize (Kb) 12764 [startup+40.006 s] Raw data (loadavg): 0.92 0.94 0.87 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 2689 0 0 0 3969 13 0 0 25 0 1 0 1851932782 11730944 2624 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 2864 2624 145 145 0 2719 0 [pid=11676] vsize: 11456 Current children cumulated CPU time (s) 39.82 Current children cumulated vsize (Kb) 13580 [startup+50.0077 s] Raw data (loadavg): 0.93 0.94 0.88 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 2900 0 0 0 4965 14 0 0 25 0 1 0 1851932782 12587008 2835 4294967295 134512640 135094434 3221224432 3221223024 134557040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 3073 2835 145 145 0 2928 0 [pid=11676] vsize: 12292 Current children cumulated CPU time (s) 49.79 Current children cumulated vsize (Kb) 14416 [startup+60.0084 s] Raw data (loadavg): 0.94 0.95 0.88 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 3059 0 0 0 5961 15 0 0 25 0 1 0 1851932782 13295616 2994 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 3246 2994 145 145 0 3101 0 [pid=11676] vsize: 12984 Current children cumulated CPU time (s) 59.76 Current children cumulated vsize (Kb) 15108 [startup+70.009 s] Raw data (loadavg): 0.95 0.95 0.88 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 3255 0 0 0 6958 17 0 0 25 0 1 0 1851932782 14086144 3190 4294967295 134512640 135094434 3221224432 3221223056 134557711 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 3439 3190 145 145 0 3294 0 [pid=11676] vsize: 13756 Current children cumulated CPU time (s) 69.75 Current children cumulated vsize (Kb) 15880 [startup+80.0107 s] Raw data (loadavg): 0.96 0.95 0.88 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 3423 0 0 0 7955 18 0 0 25 0 1 0 1851932782 14766080 3358 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 3605 3358 145 145 0 3460 0 [pid=11676] vsize: 14420 Current children cumulated CPU time (s) 79.73 Current children cumulated vsize (Kb) 16544 [startup+90.0114 s] Raw data (loadavg): 0.96 0.95 0.88 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 3583 0 0 0 8953 19 0 0 25 0 1 0 1851932782 15409152 3518 4294967295 134512640 135094434 3221224432 3221223024 134557152 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 3762 3518 145 145 0 3617 0 [pid=11676] vsize: 15048 Current children cumulated CPU time (s) 89.72 Current children cumulated vsize (Kb) 17172 [startup+100.012 s] Raw data (loadavg): 0.97 0.95 0.88 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 3689 0 0 0 9950 21 0 0 25 0 1 0 1851932782 15835136 3624 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 3866 3624 145 145 0 3721 0 [pid=11676] vsize: 15464 Current children cumulated CPU time (s) 99.71 Current children cumulated vsize (Kb) 17588 [startup+110.013 s] Raw data (loadavg): 0.97 0.95 0.88 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 3783 0 0 0 10949 21 0 0 25 0 1 0 1851932782 16211968 3718 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 3958 3718 145 145 0 3813 0 [pid=11676] vsize: 15832 Current children cumulated CPU time (s) 109.7 Current children cumulated vsize (Kb) 17956 [startup+120.013 s] Raw data (loadavg): 0.98 0.95 0.88 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 3901 0 0 0 11947 22 0 0 25 0 1 0 1851932782 16687104 3836 4294967295 134512640 135094434 3221224432 3221223056 134557621 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 4074 3836 145 145 0 3929 0 [pid=11676] vsize: 16296 Current children cumulated CPU time (s) 119.69 Current children cumulated vsize (Kb) 18420 [startup+130.014 s] Raw data (loadavg): 0.98 0.95 0.88 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 4033 0 0 0 12945 23 0 0 25 0 1 0 1851932782 17231872 3968 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 4207 3968 145 145 0 4062 0 [pid=11676] vsize: 16828 Current children cumulated CPU time (s) 129.68 Current children cumulated vsize (Kb) 18952 [startup+140.015 s] Raw data (loadavg): 0.98 0.95 0.88 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 4164 0 0 0 13943 24 0 0 25 0 1 0 1851932782 17895424 4099 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 4369 4099 145 145 0 4224 0 [pid=11676] vsize: 17476 Current children cumulated CPU time (s) 139.67 Current children cumulated vsize (Kb) 19600 [startup+150.015 s] Raw data (loadavg): 0.98 0.95 0.89 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 4354 0 0 0 14940 26 0 0 25 0 1 0 1851932782 18657280 4289 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 4555 4289 145 145 0 4410 0 [pid=11676] vsize: 18220 Current children cumulated CPU time (s) 149.66 Current children cumulated vsize (Kb) 20344 [startup+160.016 s] Raw data (loadavg): 0.99 0.96 0.89 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 4477 0 0 0 15938 27 0 0 25 0 1 0 1851932782 19177472 4412 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 4682 4412 145 145 0 4537 0 [pid=11676] vsize: 18728 Current children cumulated CPU time (s) 159.65 Current children cumulated vsize (Kb) 20852 [startup+170.017 s] Raw data (loadavg): 0.99 0.96 0.89 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 4594 0 0 0 16936 27 0 0 25 0 1 0 1851932782 19648512 4529 4294967295 134512640 135094434 3221224432 3221223056 134562110 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 4797 4529 145 145 0 4652 0 [pid=11676] vsize: 19188 Current children cumulated CPU time (s) 169.63 Current children cumulated vsize (Kb) 21312 [startup+180.017 s] Raw data (loadavg): 0.99 0.96 0.89 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 4751 0 0 0 17934 28 0 0 25 0 1 0 1851932782 20275200 4686 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 4950 4686 145 145 0 4805 0 [pid=11676] vsize: 19800 Current children cumulated CPU time (s) 179.62 Current children cumulated vsize (Kb) 21924 [startup+190.018 s] Raw data (loadavg): 0.99 0.96 0.89 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 4912 0 0 0 18930 29 0 0 25 0 1 0 1851932782 20926464 4847 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5109 4847 145 145 0 4964 0 [pid=11676] vsize: 20436 Current children cumulated CPU time (s) 189.59 Current children cumulated vsize (Kb) 22560 [startup+200.02 s] Raw data (loadavg): 0.99 0.96 0.89 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5083 0 0 0 19927 31 0 0 25 0 1 0 1851932782 21630976 5018 4294967295 134512640 135094434 3221224432 3221223024 134557377 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5281 5018 145 145 0 5136 0 [pid=11676] vsize: 21124 Current children cumulated CPU time (s) 199.58 Current children cumulated vsize (Kb) 23248 [startup+210.02 s] Raw data (loadavg): 0.99 0.96 0.89 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 20926 31 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0 [pid=11676] vsize: 21508 Current children cumulated CPU time (s) 209.57 Current children cumulated vsize (Kb) 23632 [startup+220.021 s] Raw data (loadavg): 0.99 0.96 0.89 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 21926 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0 [pid=11676] vsize: 21508 Current children cumulated CPU time (s) 219.58 Current children cumulated vsize (Kb) 23632 [startup+230.022 s] Raw data (loadavg): 0.99 0.96 0.89 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 22926 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0 [pid=11676] vsize: 21508 Current children cumulated CPU time (s) 229.58 Current children cumulated vsize (Kb) 23632 [startup+240.023 s] Raw data (loadavg): 0.99 0.96 0.89 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 23926 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223056 134557614 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0 [pid=11676] vsize: 21508 Current children cumulated CPU time (s) 239.58 Current children cumulated vsize (Kb) 23632 [startup+250.023 s] Raw data (loadavg): 0.99 0.96 0.89 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 24927 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0 [pid=11676] vsize: 21508 Current children cumulated CPU time (s) 249.59 Current children cumulated vsize (Kb) 23632 [startup+260.024 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 25927 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0 [pid=11676] vsize: 21508 Current children cumulated CPU time (s) 259.59 Current children cumulated vsize (Kb) 23632 [startup+270.024 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 26927 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0 [pid=11676] vsize: 21508 Current children cumulated CPU time (s) 269.59 Current children cumulated vsize (Kb) 23632 [startup+280.024 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 27927 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0 [pid=11676] vsize: 21508 Current children cumulated CPU time (s) 279.59 Current children cumulated vsize (Kb) 23632 [startup+290.025 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 28927 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0 [pid=11676] vsize: 21508 Current children cumulated CPU time (s) 289.59 Current children cumulated vsize (Kb) 23632 [startup+300.026 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 29928 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0 [pid=11676] vsize: 21508 Current children cumulated CPU time (s) 299.6 Current children cumulated vsize (Kb) 23632 [startup+310.026 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 30928 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0 [pid=11676] vsize: 21508 Current children cumulated CPU time (s) 309.6 Current children cumulated vsize (Kb) 23632 [startup+320.027 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 31928 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0 [pid=11676] vsize: 21508 Current children cumulated CPU time (s) 319.6 Current children cumulated vsize (Kb) 23632 [startup+330.028 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 32928 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0 [pid=11676] vsize: 21508 Current children cumulated CPU time (s) 329.6 Current children cumulated vsize (Kb) 23632 [startup+340.028 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 33928 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0 [pid=11676] vsize: 21508 Current children cumulated CPU time (s) 339.6 Current children cumulated vsize (Kb) 23632 [startup+350.029 s] Raw data (loadavg): 0.99 0.97 0.90 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 34929 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0 [pid=11676] vsize: 21508 Current children cumulated CPU time (s) 349.61 Current children cumulated vsize (Kb) 23632 [startup+360.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 35929 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0 [pid=11676] vsize: 21508 Current children cumulated CPU time (s) 359.61 Current children cumulated vsize (Kb) 23632 [startup+370.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 36929 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0 [pid=11676] vsize: 21508 Current children cumulated CPU time (s) 369.61 Current children cumulated vsize (Kb) 23632 [startup+380.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 37929 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0 [pid=11676] vsize: 21508 Current children cumulated CPU time (s) 379.61 Current children cumulated vsize (Kb) 23632 [startup+390.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 38930 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0 [pid=11676] vsize: 21508 Current children cumulated CPU time (s) 389.62 Current children cumulated vsize (Kb) 23632 [startup+400.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 39930 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0 [pid=11676] vsize: 21508 Current children cumulated CPU time (s) 399.62 Current children cumulated vsize (Kb) 23632 [startup+410.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 40930 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0 [pid=11676] vsize: 21508 Current children cumulated CPU time (s) 409.62 Current children cumulated vsize (Kb) 23632 [startup+420.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5180 0 0 0 41930 32 0 0 25 0 1 0 1851932782 22024192 5115 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5377 5115 145 145 0 5232 0 [pid=11676] vsize: 21508 Current children cumulated CPU time (s) 419.62 Current children cumulated vsize (Kb) 23632 [startup+430.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5217 0 0 0 42930 33 0 0 25 0 1 0 1851932782 22175744 5152 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5414 5152 145 145 0 5269 0 [pid=11676] vsize: 21656 Current children cumulated CPU time (s) 429.63 Current children cumulated vsize (Kb) 23780 [startup+440.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5366 0 0 0 43928 34 0 0 25 0 1 0 1851932782 22806528 5301 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5568 5301 145 145 0 5423 0 [pid=11676] vsize: 22272 Current children cumulated CPU time (s) 439.62 Current children cumulated vsize (Kb) 24396 [startup+450.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5512 0 0 0 44925 35 0 0 25 0 1 0 1851932782 23412736 5447 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 5716 5447 145 145 0 5571 0 [pid=11676] vsize: 22864 Current children cumulated CPU time (s) 449.6 Current children cumulated vsize (Kb) 24988 [startup+460.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5694 0 0 0 45921 37 0 0 25 0 1 0 1851932782 24150016 5629 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11676/statm): 5896 5629 145 145 0 5751 0 [pid=11676] vsize: 23584 Current children cumulated CPU time (s) 459.58 Current children cumulated vsize (Kb) 25708 [startup+470.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5880 0 0 0 46917 39 0 0 25 0 1 0 1851932782 24903680 5815 4294967295 134512640 135094434 3221224432 3221222912 134780543 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6080 5815 145 145 0 5935 0 [pid=11676] vsize: 24320 Current children cumulated CPU time (s) 469.56 Current children cumulated vsize (Kb) 26444 [startup+480.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5934 0 0 0 47916 39 0 0 25 0 1 0 1851932782 25120768 5869 4294967295 134512640 135094434 3221224432 3221223024 134557022 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6133 5869 145 145 0 5988 0 [pid=11676] vsize: 24532 Current children cumulated CPU time (s) 479.55 Current children cumulated vsize (Kb) 26656 [startup+490.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5934 0 0 0 48916 39 0 0 25 0 1 0 1851932782 25120768 5869 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6133 5869 145 145 0 5988 0 [pid=11676] vsize: 24532 Current children cumulated CPU time (s) 489.55 Current children cumulated vsize (Kb) 26656 [startup+500.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 49916 39 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 499.55 Current children cumulated vsize (Kb) 26716 [startup+510.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 50915 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 509.55 Current children cumulated vsize (Kb) 26716 [startup+520.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 51915 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 519.55 Current children cumulated vsize (Kb) 26716 [startup+530.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 52915 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 529.55 Current children cumulated vsize (Kb) 26716 [startup+540.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 53916 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 539.56 Current children cumulated vsize (Kb) 26716 [startup+550.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 54916 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 549.56 Current children cumulated vsize (Kb) 26716 [startup+560.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 55916 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 559.56 Current children cumulated vsize (Kb) 26716 [startup+570.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 56916 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 569.56 Current children cumulated vsize (Kb) 26716 [startup+580.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 57917 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 579.57 Current children cumulated vsize (Kb) 26716 [startup+590.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 58917 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 589.57 Current children cumulated vsize (Kb) 26716 [startup+600.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 59917 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223024 134551434 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 599.57 Current children cumulated vsize (Kb) 26716 [startup+610.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 60917 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 609.57 Current children cumulated vsize (Kb) 26716 [startup+620.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 61917 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 619.57 Current children cumulated vsize (Kb) 26716 [startup+630.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 62917 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 629.57 Current children cumulated vsize (Kb) 26716 [startup+640.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 63918 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 639.58 Current children cumulated vsize (Kb) 26716 [startup+650.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 64918 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 649.58 Current children cumulated vsize (Kb) 26716 [startup+660.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 65918 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 659.58 Current children cumulated vsize (Kb) 26716 [startup+670.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 66918 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 669.58 Current children cumulated vsize (Kb) 26716 [startup+680.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 67918 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 679.58 Current children cumulated vsize (Kb) 26716 [startup+690.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 68919 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 689.59 Current children cumulated vsize (Kb) 26716 [startup+700.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 69919 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 699.59 Current children cumulated vsize (Kb) 26716 [startup+710.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 70919 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 709.59 Current children cumulated vsize (Kb) 26716 [startup+720.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 71919 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223056 134557691 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 719.59 Current children cumulated vsize (Kb) 26716 [startup+730.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 72920 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223024 134557168 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 729.6 Current children cumulated vsize (Kb) 26716 [startup+740.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 73920 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 739.6 Current children cumulated vsize (Kb) 26716 [startup+750.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 74920 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 749.6 Current children cumulated vsize (Kb) 26716 [startup+760.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 75920 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 759.6 Current children cumulated vsize (Kb) 26716 [startup+770.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 76921 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 769.61 Current children cumulated vsize (Kb) 26716 [startup+780.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 77921 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 779.61 Current children cumulated vsize (Kb) 26716 [startup+790.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 78921 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 789.61 Current children cumulated vsize (Kb) 26716 [startup+800.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 79921 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 799.61 Current children cumulated vsize (Kb) 26716 [startup+810.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 80922 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 809.62 Current children cumulated vsize (Kb) 26716 [startup+820.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 81922 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223040 134539502 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 819.62 Current children cumulated vsize (Kb) 26716 [startup+830.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 82922 40 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 829.62 Current children cumulated vsize (Kb) 26716 [startup+840.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 83922 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 839.63 Current children cumulated vsize (Kb) 26716 [startup+850.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 84923 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 849.64 Current children cumulated vsize (Kb) 26716 [startup+860.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 85923 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223120 134554796 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 859.64 Current children cumulated vsize (Kb) 26716 [startup+870.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 86923 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 869.64 Current children cumulated vsize (Kb) 26716 [startup+880.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 87923 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 879.64 Current children cumulated vsize (Kb) 26716 [startup+890.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 88923 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 889.64 Current children cumulated vsize (Kb) 26716 [startup+900.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 89924 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 899.65 Current children cumulated vsize (Kb) 26716 [startup+910.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 90924 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 909.65 Current children cumulated vsize (Kb) 26716 [startup+920.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 91924 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 919.65 Current children cumulated vsize (Kb) 26716 [startup+930.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 92924 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 929.65 Current children cumulated vsize (Kb) 26716 [startup+940.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 93925 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 939.66 Current children cumulated vsize (Kb) 26716 [startup+950.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 94925 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 949.66 Current children cumulated vsize (Kb) 26716 [startup+960.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 95925 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558281 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 959.66 Current children cumulated vsize (Kb) 26716 [startup+970.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 96925 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 969.66 Current children cumulated vsize (Kb) 26716 [startup+980.074 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 97926 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 979.67 Current children cumulated vsize (Kb) 26716 [startup+990.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 98926 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 989.67 Current children cumulated vsize (Kb) 26716 [startup+1000.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 99926 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 999.67 Current children cumulated vsize (Kb) 26716 [startup+1010.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 100926 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 1009.67 Current children cumulated vsize (Kb) 26716 [startup+1020.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 101927 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223056 134557577 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 1019.68 Current children cumulated vsize (Kb) 26716 [startup+1030.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 102927 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 1029.68 Current children cumulated vsize (Kb) 26716 [startup+1040.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 103927 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 1039.68 Current children cumulated vsize (Kb) 26716 [startup+1050.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 104927 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 1049.68 Current children cumulated vsize (Kb) 26716 [startup+1060.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 105928 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 1059.69 Current children cumulated vsize (Kb) 26716 [startup+1070.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 106928 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 1069.69 Current children cumulated vsize (Kb) 26716 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 107928 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 1079.69 Current children cumulated vsize (Kb) 26716 [startup+1090.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5949 0 0 0 108928 41 0 0 25 0 1 0 1851932782 25182208 5884 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5884 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 1089.69 Current children cumulated vsize (Kb) 26716 [startup+1100.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 109928 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 1099.69 Current children cumulated vsize (Kb) 26716 [startup+1110.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 110929 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 1109.7 Current children cumulated vsize (Kb) 26716 [startup+1120.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 111929 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 1119.7 Current children cumulated vsize (Kb) 26716 [startup+1130.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 112929 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 1129.7 Current children cumulated vsize (Kb) 26716 [startup+1140.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 113930 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 1139.71 Current children cumulated vsize (Kb) 26716 [startup+1150.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 114930 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 1149.71 Current children cumulated vsize (Kb) 26716 [startup+1160.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 115930 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223060 134557564 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 1159.71 Current children cumulated vsize (Kb) 26716 [startup+1170.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 116930 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 1169.71 Current children cumulated vsize (Kb) 26716 [startup+1180.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 117931 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 1179.72 Current children cumulated vsize (Kb) 26716 [startup+1190.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 118931 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 1189.72 Current children cumulated vsize (Kb) 26716 [startup+1200.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 119931 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 1199.72 Current children cumulated vsize (Kb) 26716 [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 120932 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 1209.73 Current children cumulated vsize (Kb) 26716 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 11676 Raw data (/proc/11672/stat): 11672 (minisat+_script) S 11671 11672 20115 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1851932777 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/11672/statm): 531 226 485 147 0 384 0 [pid=11672] vsize: 2124 Raw data (/proc/11676/stat): 11676 (minisat+_64-bit) R 11672 11672 20115 0 -1 0 5950 0 0 0 120932 41 0 0 25 0 1 0 1851932782 25182208 5885 4294967295 134512640 135094434 3221224432 3221223120 134554682 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11676/statm): 6148 5885 145 145 0 6003 0 [pid=11676] vsize: 24592 Current children cumulated CPU time (s) 1209.73 Current children cumulated vsize (Kb) 26716 Sending SIGTERM to -11672 Sleeping 2 seconds One traced child (pid=11672) ended because it received signal 15 (SIGTERM) One traced child (pid=11676) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.11 CPU time (s): 1209.75 CPU user time (s): 1209.32 CPU system time (s): 0.424935 CPU usage (%): 99.9697 Max. virtual memory (cumulated for all children) (Kb): 26716
ERROR: no interpretation found !