Name | web/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:20:4.5:0.95:98.opb |
MD5SUM | a89f4ed95903fddf213992506514bcf0 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 15 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 906 |
Biggest coefficient in the objective function | 553 |
Number of bits for the biggest coefficient in the objective function | 10 |
Sum of the numbers in the objective function | 2526 |
Number of bits of the sum of numbers in the objective function | 12 |
Biggest number in a constraint | 553 |
Number of bits of the biggest number in a constraint | 10 |
Biggest sum of numbers in a constraint | 2526 |
Number of bits of the biggest sum of numbers | 12 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1223.74 |
Number of variables | 906 |
Total number of constraints | 1944 |
Number of constraints which are clauses | 852 |
Number of constraints which are cardinality constraints (but not clauses) | 1092 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 18 |
LAUNCH ON wulflinc17 THE 2005-09-18 19:11:40 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2740 boxname=wulflinc17 idbench=396 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: a89f4ed95903fddf213992506514bcf0 /oldhome/oroussel/tmp/wulflinc17/normalized-10:20:4.5:0.95:98.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc17/normalized-10:20:4.5:0.95:98.opb IDLAUNCH: 2740 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 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.072 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: 931940 kB Buffers: 28424 kB Cached: 47356 kB SwapCached: 516 kB Active: 28784 kB Inactive: 49420 kB HighTotal: 131008 kB HighFree: 79660 kB LowTotal: 903652 kB LowFree: 852280 kB SwapTotal: 2097892 kB SwapFree: 2096672 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5680 kB Slab: 18760 kB Committed_AS: 64184 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 19:31:50 (client local time) WITH STATUS 10 IN 1209.07 SECONDS stats: 2740 7 1209.07 10
c Parsing PB file... c Converting 1038 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ---[ 187]---> BDD-cost: 5 c ---[ 186]---> BDD-cost: 8 c ---[ 185]---> BDD-cost: 14 c ---[ 184]---> BDD-cost: 14 c ---[ 183]---> BDD-cost: 17 c ---[ 182]---> BDD-cost: 14 c ---[ 181]---> BDD-cost: 23 c ---[ 180]---> BDD-cost: 20 c ---[ 179]---> BDD-cost: 29 c ---[ 178]---> BDD-cost: 29 c ---[ 177]---> BDD-cost: 38 c ---[ 176]---> BDD-cost: 32 c ---[ 175]---> BDD-cost: 32 c ---[ 174]---> BDD-cost: 23 c ---[ 173]---> BDD-cost: 26 c ---[ 172]---> BDD-cost: 20 c ---[ 171]---> BDD-cost: 20 c ---[ 170]---> BDD-cost: 14 c ---[ 169]---> BDD-cost: 14 c ---[ 168]---> BDD-cost: 8 c ---[ 167]---> BDD-cost: 8 c ---[ 166]---> BDD-cost: 11 c ---[ 165]---> BDD-cost: 14 c ---[ 164]---> BDD-cost: 17 c ---[ 163]---> BDD-cost: 18 c ---[ 162]---> BDD-cost: 18 c ---[ 161]---> BDD-cost: 35 c ---[ 160]---> BDD-cost: 35 c ---[ 159]---> BDD-cost: 41 c ---[ 158]---> BDD-cost: 35 c ---[ 157]---> BDD-cost: 38 c ---[ 156]---> BDD-cost: 38 c ---[ 155]---> BDD-cost: 41 c ---[ 154]---> BDD-cost: 35 c ---[ 153]---> BDD-cost: 38 c ---[ 152]---> BDD-cost: 23 c ---[ 151]---> BDD-cost: 20 c ---[ 150]---> BDD-cost: 17 c ---[ 149]---> BDD-cost: 20 c ---[ 148]---> BDD-cost: 11 c ---[ 147]---> BDD-cost: 8 c ---[ 146]---> BDD-cost: 11 c ---[ 145]---> BDD-cost: 14 c ---[ 144]---> BDD-cost: 17 c ---[ 143]---> BDD-cost: 23 c ---[ 142]---> BDD-cost: 29 c ---[ 141]---> BDD-cost: 41 c ---[ 140]---> BDD-cost: 44 c ---[ 139]---> BDD-cost: 44 c ---[ 138]---> BDD-cost: 38 c ---[ 137]---> BDD-cost: 39 c ---[ 136]---> BDD-cost: 41 c ---[ 135]---> BDD-cost: 44 c ---[ 134]---> BDD-cost: 44 c ---[ 133]---> BDD-cost: 41 c ---[ 132]---> BDD-cost: 29 c ---[ 131]---> BDD-cost: 29 c ---[ 130]---> BDD-cost: 23 c ---[ 129]---> BDD-cost: 26 c ---[ 128]---> BDD-cost: 14 c ---[ 127]---> BDD-cost: 8 c ---[ 126]---> BDD-cost: 11 c ---[ 125]---> BDD-cost: 14 c ---[ 124]---> BDD-cost: 17 c ---[ 123]---> BDD-cost: 21 c ---[ 122]---> BDD-cost: 29 c ---[ 121]---> BDD-cost: 35 c ---[ 120]---> BDD-cost: 44 c ---[ 119]---> BDD-cost: 47 c ---[ 118]---> BDD-cost: 44 c ---[ 117]---> BDD-cost: 44 c ---[ 116]---> BDD-cost: 44 c ---[ 115]---> BDD-cost: 41 c ---[ 114]---> BDD-cost: 38 c ---[ 113]---> BDD-cost: 35 c ---[ 112]---> BDD-cost: 32 c ---[ 111]---> BDD-cost: 29 c ---[ 110]---> BDD-cost: 26 c ---[ 109]---> BDD-cost: 20 c ---[ 108]---> BDD-cost: 6 c ---[ 107]---> BDD-cost: 5 c ---[ 106]---> BDD-cost: 14 c ---[ 105]---> BDD-cost: 20 c ---[ 104]---> BDD-cost: 23 c ---[ 103]---> BDD-cost: 26 c ---[ 102]---> BDD-cost: 35 c ---[ 101]---> BDD-cost: 38 c ---[ 100]---> BDD-cost: 35 c ---[ 99]---> BDD-cost: 41 c ---[ 98]---> BDD-cost: 44 c ---[ 97]---> BDD-cost: 41 c ---[ 96]---> BDD-cost: 38 c ---[ 95]---> BDD-cost: 41 c ---[ 94]---> BDD-cost: 38 c ---[ 93]---> BDD-cost: 29 c ---[ 92]---> BDD-cost: 20 c ---[ 91]---> BDD-cost: 26 c ---[ 90]---> BDD-cost: 20 c ---[ 89]---> BDD-cost: 14 c ---[ 88]---> BDD-cost: 5 c ---[ 87]---> BDD-cost: 5 c ---[ 86]---> BDD-cost: 11 c ---[ 85]---> BDD-cost: 20 c ---[ 84]---> BDD-cost: 20 c ---[ 83]---> BDD-cost: 32 c ---[ 82]---> BDD-cost: 41 c ---[ 81]---> BDD-cost: 38 c ---[ 80]---> BDD-cost: 35 c ---[ 79]---> BDD-cost: 32 c ---[ 78]---> BDD-cost: 35 c ---[ 77]---> BDD-cost: 44 c ---[ 76]---> BDD-cost: 35 c ---[ 75]---> BDD-cost: 38 c ---[ 74]---> BDD-cost: 35 c ---[ 73]---> BDD-cost: 29 c ---[ 72]---> BDD-cost: 23 c ---[ 71]---> BDD-cost: 17 c ---[ 70]---> BDD-cost: 17 c ---[ 69]---> BDD-cost: 11 c ---[ 68]---> BDD-cost: 3 c ---[ 67]---> BDD-cost: 7 c ---[ 66]---> BDD-cost: 11 c ---[ 65]---> BDD-cost: 17 c ---[ 64]---> BDD-cost: 23 c ---[ 63]---> BDD-cost: 32 c ---[ 62]---> BDD-cost: 26 c ---[ 61]---> BDD-cost: 38 c ---[ 60]---> BDD-cost: 32 c ---[ 59]---> BDD-cost: 32 c ---[ 58]---> BDD-cost: 35 c ---[ 57]---> BDD-cost: 38 c ---[ 56]---> BDD-cost: 32 c ---[ 55]---> BDD-cost: 35 c ---[ 54]---> BDD-cost: 29 c ---[ 53]---> BDD-cost: 32 c ---[ 52]---> BDD-cost: 29 c ---[ 51]---> BDD-cost: 23 c ---[ 50]---> BDD-cost: 17 c ---[ 49]---> BDD-cost: 11 c ---[ 47]---> BDD-cost: 8 c ---[ 46]---> BDD-cost: 20 c ---[ 45]---> BDD-cost: 14 c ---[ 44]---> BDD-cost: 17 c ---[ 43]---> BDD-cost: 20 c ---[ 42]---> BDD-cost: 20 c ---[ 41]---> BDD-cost: 35 c ---[ 40]---> BDD-cost: 35 c ---[ 39]---> BDD-cost: 35 c ---[ 38]---> BDD-cost: 23 c ---[ 37]---> BDD-cost: 26 c ---[ 36]---> BDD-cost: 23 c ---[ 35]---> BDD-cost: 23 c ---[ 34]---> BDD-cost: 23 c ---[ 33]---> BDD-cost: 26 c ---[ 32]---> BDD-cost: 17 c ---[ 31]---> BDD-cost: 5 c ---[ 30]---> BDD-cost: 8 c ---[ 29]---> BDD-cost: 14 c ---[ 28]---> BDD-cost: 14 c ---[ 27]---> BDD-cost: 14 c ---[ 26]---> BDD-cost: 26 c ---[ 25]---> BDD-cost: 20 c ---[ 24]---> BDD-cost: 26 c ---[ 23]---> BDD-cost: 17 c ---[ 22]---> BDD-cost: 15 c ---[ 21]---> BDD-cost: 20 c ---[ 20]---> BDD-cost: 20 c ---[ 19]---> BDD-cost: 17 c ---[ 18]---> BDD-cost: 20 c ---[ 17]---> BDD-cost: 11 c ---[ 16]---> BDD-cost: 8 c ---[ 14]---> BDD-cost: 7 c ---[ 13]---> BDD-cost: 9 c ---[ 12]---> BDD-cost: 14 c ---[ 11]---> BDD-cost: 11 c ---[ 10]---> BDD-cost: 17 c ---[ 9]---> BDD-cost: 14 c ---[ 8]---> BDD-cost: 14 c ---[ 7]---> BDD-cost: 14 c ---[ 6]---> BDD-cost: 14 c ---[ 5]---> BDD-cost: 14 c ---[ 4]---> BDD-cost: 17 c ---[ 3]---> BDD-cost: 14 c ---[ 2]---> BDD-cost: 14 c ---[ 1]---> BDD-cost: 8 c ---[ 0]---> BDD-cost: 8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 11181 31975 | 3727 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 959[0m c ---[ 0]---> Adder-cost: 2188 maxlim: 461 bits: 10/9 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 26442 86478 | 8814 0 0 nan | 0.000 % | c | 100 | 26442 86478 | 9695 100 380 3.8 | 2.547 % | c | 250 | 26433 86447 | 10664 248 1059 4.3 | 2.560 % | c | 476 | 26433 86447 | 11731 474 2412 5.1 | 2.560 % | c ============================================================================== c [1mFound solution: 206[0m c ---[ 0]---> Adder-cost: 2 maxlim: 1214 bits: 11/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 806 | 26471 86617 | 8823 804 4288 5.3 | 2.560 % | c ============================================================================== c [1mFound solution: 143[0m c ---[ 0]---> Adder-cost: 0 maxlim: 1277 bits: 11/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 814 | 26480 86667 | 8826 812 4330 5.3 | 2.560 % | c | 914 | 26480 86667 | 9708 912 8172 9.0 | 2.738 % | c | 1064 | 26480 86667 | 10679 1062 8878 8.4 | 2.738 % | c | 1289 | 26480 86667 | 11747 1287 13915 10.8 | 2.738 % | c | 1626 | 26480 86667 | 12922 1624 15594 9.6 | 2.738 % | c | 2132 | 26480 86667 | 14214 2130 18615 8.7 | 2.738 % | c | 2892 | 26480 86667 | 15635 2890 40463 14.0 | 2.738 % | c | 4031 | 26480 86667 | 17199 4029 61525 15.3 | 2.738 % | c | 5740 | 26480 86667 | 18919 5738 145592 25.4 | 2.738 % | c | 8302 | 26480 86667 | 20811 8300 400387 48.2 | 2.738 % | c | 12147 | 26480 86667 | 22892 12145 750271 61.8 | 2.738 % | c ============================================================================== c [1mFound solution: 130[0m c ---[ 0]---> Adder-cost: 0 maxlim: 1290 bits: 11/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14029 | 26485 86701 | 8828 14027 824966 58.8 | 2.738 % | c | 14129 | 26485 86701 | 9710 7114 431246 60.6 | 2.789 % | c | 14279 | 26485 86701 | 10681 7264 431919 59.5 | 2.789 % | c | 14505 | 26485 86701 | 11750 7490 433807 57.9 | 2.789 % | c | 14842 | 26485 86701 | 12925 7827 440942 56.3 | 2.789 % | c | 15349 | 26485 86701 | 14217 8334 463419 55.6 | 2.789 % | c | 16108 | 26485 86701 | 15639 9093 482022 53.0 | 2.789 % | c | 17247 | 26485 86701 | 17203 10232 538561 52.6 | 2.789 % | c | 18955 | 26485 86701 | 18923 11940 602513 50.5 | 2.789 % | c | 21519 | 26485 86701 | 20815 14504 833364 57.5 | 2.789 % | c ============================================================================== c [1mFound solution: 127[0m c ---[ 0]---> Adder-cost: 0 maxlim: 1293 bits: 11/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 23171 | 26489 86723 | 8829 16156 882076 54.6 | 2.789 % | c | 23272 | 26489 86723 | 9711 8179 357304 43.7 | 2.814 % | c | 23422 | 26489 86723 | 10683 8329 358840 43.1 | 2.814 % | c | 23647 | 26489 86723 | 11751 8554 363731 42.5 | 2.814 % | c | 23984 | 26489 86723 | 12926 8891 369197 41.5 | 2.814 % | c | 24490 | 26489 86723 | 14219 9397 396462 42.2 | 2.814 % | c | 25250 | 26489 86723 | 15641 10157 425636 41.9 | 2.814 % | c | 26389 | 26489 86723 | 17205 11296 470056 41.6 | 2.814 % | c | 28097 | 26489 86723 | 18925 13004 538210 41.4 | 2.814 % | c | 30662 | 26489 86723 | 20818 15569 771366 49.5 | 2.814 % | c | 34507 | 26489 86723 | 22900 19414 1108591 57.1 | 2.814 % | c | 40273 | 26489 86723 | 25190 25180 1530602 60.8 | 2.814 % | c ============================================================================== c [1mFound solution: 117[0m c ---[ 0]---> Adder-cost: 0 maxlim: 1303 bits: 11/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 47450 | 26491 86738 | 8830 18237 1218106 66.8 | 2.814 % | c | 47550 | 26491 86738 | 9713 4660 289106 62.0 | 2.839 % | c | 47700 | 26491 86738 | 10684 4810 290323 60.4 | 2.839 % | c | 47925 | 26491 86738 | 11752 5035 300392 59.7 | 2.839 % | c | 48262 | 26491 86738 | 12928 5372 302069 56.2 | 2.839 % | c | 48768 | 26491 86738 | 14220 5878 320891 54.6 | 2.839 % | c | 49527 | 26491 86738 | 15642 6637 330420 49.8 | 2.839 % | c | 50666 | 26491 86738 | 17207 7776 374858 48.2 | 2.839 % | c | 52374 | 26491 86738 | 18927 9484 530806 56.0 | 2.839 % | c | 54937 | 26491 86738 | 20820 12047 686209 57.0 | 2.839 % | c | 58782 | 26491 86738 | 22902 15892 975705 61.4 | 2.839 % | c ============================================================================== c [1mFound solution: 109[0m c ---[ 0]---> Adder-cost: 0 maxlim: 1311 bits: 11/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 60887 | 26492 86744 | 8830 17997 1087821 60.4 | 2.839 % | c | 60987 | 26492 86744 | 9713 9099 440274 48.4 | 2.852 % | c | 61137 | 26492 86744 | 10684 9249 442243 47.8 | 2.852 % | c | 61363 | 26492 86744 | 11752 9475 447923 47.3 | 2.852 % | c | 61701 | 26492 86744 | 12928 9813 460334 46.9 | 2.852 % | c | 62209 | 26492 86744 | 14220 10321 482479 46.7 | 2.852 % | c | 62968 | 26492 86744 | 15642 11080 518644 46.8 | 2.852 % | c | 64109 | 26492 86744 | 17207 12221 575864 47.1 | 2.852 % | c | 65817 | 26492 86744 | 18927 13929 671448 48.2 | 2.852 % | c | 68380 | 26492 86744 | 20820 16492 791321 48.0 | 2.852 % | c | 72224 | 26492 86744 | 22902 20336 1038178 51.1 | 2.852 % | c | 77993 | 26492 86744 | 25193 26105 1602134 61.4 | 2.852 % | c | 86642 | 26492 86744 | 27712 21702 1613426 74.3 | 2.852 % | c ============================================================================== c [1mFound solution: 107[0m c ---[ 0]---> Adder-cost: 0 maxlim: 1313 bits: 11/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 90492 | 26493 86754 | 8831 25552 1851614 72.5 | 2.852 % | c | 90592 | 26493 86754 | 9714 6488 296083 45.6 | 2.865 % | c | 90742 | 26493 86754 | 10685 6638 298105 44.9 | 2.865 % | c | 90967 | 26493 86754 | 11754 6863 301577 43.9 | 2.865 % | c | 91304 | 26493 86754 | 12929 7200 303911 42.2 | 2.865 % | c | 91810 | 26493 86754 | 14222 7706 318504 41.3 | 2.865 % | c | 92569 | 26493 86754 | 15644 8465 366545 43.3 | 2.865 % | c | 93708 | 26493 86754 | 17209 9604 427191 44.5 | 2.865 % | c | 95418 | 26493 86754 | 18930 11314 506391 44.8 | 2.865 % | c | 97982 | 26493 86754 | 20823 13878 666721 48.0 | 2.865 % | c | 101827 | 26493 86754 | 22905 17723 1003862 56.6 | 2.865 % | c | 107595 | 26493 86754 | 25195 23491 1603772 68.3 | 2.865 % | c | 116244 | 26493 86754 | 27715 18209 2007969 110.3 | 2.865 % | c | 129219 | 26493 86754 | 30487 14477 1299051 89.7 | 2.865 % | c | 148680 | 26493 86754 | 33535 33938 3505926 103.3 | 2.865 % | c | 177873 | 26493 86754 | 36889 19569 1981304 101.2 | 2.865 % | c ============================================================================== c [1mFound solution: 106[0m c ---[ 0]---> Adder-cost: 0 maxlim: 1314 bits: 11/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 203130 | 26495 86767 | 8831 17932 2342869 130.7 | 2.865 % | c | 203230 | 26495 86767 | 9714 9066 1059460 116.9 | 2.877 % | c | 203380 | 26495 86767 | 10685 9216 1060308 115.1 | 2.877 % | c | 203605 | 26495 86767 | 11754 9441 1061663 112.5 | 2.877 % | c | 203942 | 26495 86767 | 12929 9778 1064191 108.8 | 2.877 % | c | 204450 | 26495 86767 | 14222 10286 1076718 104.7 | 2.877 % | c | 205211 | 26495 86767 | 15644 11047 1099524 99.5 | 2.877 % | c | 206350 | 26495 86767 | 17209 12186 1151779 94.5 | 2.877 % | c | 208058 | 26495 86767 | 18930 13894 1290178 92.9 | 2.877 % | c | 210620 | 26495 86767 | 20823 16456 1424602 86.6 | 2.877 % | c | 214466 | 26495 86767 | 22905 20302 1945374 95.8 | 2.877 % | c | 220234 | 26495 86767 | 25195 13589 1290861 95.0 | 2.877 % | c | 228886 | 26495 86767 | 27715 22241 2221897 99.9 | 2.877 % | c | 241860 | 26495 86767 | 30487 16824 1624022 96.5 | 2.877 % | c | 261324 | 26495 86767 | 33535 18036 1297748 72.0 | 2.877 % | c | 290519 | 26495 86767 | 36889 27027 2715164 100.5 | 2.877 % | c | 334311 | 26495 86767 | 40578 18135 1843579 101.7 | 2.877 % | c | 399995 | 26495 86767 | 44636 25387 6045749 238.1 | 2.877 % | c ============================================================================== c [1mFound solution: 98[0m c ---[ 0]---> Adder-cost: 0 maxlim: 1322 bits: 11/11 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 445674 | 26500 86799 | 8833 37759 6320294 167.4 | 2.877 % | c | 445774 | 26500 86799 | 9716 6732 774985 115.1 | 2.915 % | c | 445924 | 26500 86799 | 10687 6882 775935 112.7 | 2.915 % | c | 446151 | 26500 86799 | 11756 7109 777542 109.4 | 2.915 % | c | 446488 | 26500 86799 | 12932 7446 782594 105.1 | 2.915 % | c | 446994 | 26500 86799 | 14225 7952 795902 100.1 | 2.915 % | c | 447753 | 26500 86799 | 15648 8711 803084 92.2 | 2.915 % | c | 448892 | 26500 86799 | 17213 9850 821221 83.4 | 2.915 % | c | 450600 | 26500 86799 | 18934 11558 878453 76.0 | 2.915 % | c | 453165 | 26500 86799 | 20827 14123 1062292 75.2 | 2.915 % | c | 457009 | 26500 86799 | 22910 17967 1272621 70.8 | 2.915 % | c | 462775 | 26500 86799 | 25201 11982 661214 55.2 | 2.915 % | c | 471427 | 26500 86799 | 27721 20634 1378808 66.8 | 2.915 % | c | 484402 | 26500 86799 | 30493 14154 2586201 182.7 | 2.915 % | c | 503864 | 26500 86799 | 33543 33616 5188761 154.4 | 2.915 % | c | 533056 | 26500 86799 | 36897 18884 2969903 157.3 | 2.915 % | c | 576845 | 26500 86799 | 40587 35392 5877484 166.1 | 2.915 % | c | 642534 | 26500 86799 | 44646 42901 8342933 194.5 | 2.915 % | c c *** TERMINATED *** s SATISFIABLE v -v785 v740 v420 v82 -v860 v744 v418 -v859 -v784 v501 -v307 -v85 v788 v419 -v86 -v63 -v861 v504 -v424 v354 -v306 -v62 v863 -v789 -v573 v505 -v64 -v572 -v478 -v441 v353 -v312 -v65 -v27 v864 -v574 -v477 -v310 -v102 v66 v866 -v810 v575 -v479 -v440 -v359 -v262 -v185 -v101 v73 v26 v867 -v814 v576 -v482 -v357 -v311 -v190 v107 -v67 -v30 -v697 v583 v481 -v446 -v399 -v315 -v265 -v216 -v189 -v143 v106 -v68 -v701 v577 v486 -v444 -v358 -v266 -v142 v108 -v69 -v31 -v2 -v578 v485 -v398 v362 v192 -v166 -v144 v112 -v1 -v660 -v579 v483 -v445 v193 v147 v111 -v7 -v659 -v594 -v558 v484 -v449 -v404 -v196 v165 v146 v109 -v6 -v661 -v598 -v557 -v402 -v194 v151 v110 -v8 -v662 v559 -v332 -v195 v171 v150 -v12 v663 -v562 -v403 v169 v148 -v11 v668 v561 v407 -v335 v149 -v9 v664 v563 -v336 v170 -v10 v739 v421 v81 -v855 v743 -v854 -v786 v500 v425 -v302 -v87 v790 -v423 -v862 v506 -v349 -v308 v865 v869 -v835 -v792 -v436 v355 -v313 -v90 -v76 v868 -v839 -v793 -v77 -v809 -v586 -v509 -v442 v360 -v316 -v261 -v212 -v72 v28 -v813 -v587 v480 -v314 -v184 v103 -v32 -v696 v582 -v494 -v447 -v394 v363 -v267 -v215 -v186 v104 -v70 -v700 v490 v361 -v191 v105 v580 v489 -v450 -v400 v188 -v161 v116 -v34 -v448 -v197 -v145 -v35 -v3 -v593 -v542 -v405 -v270 v167 -v159 -v4 -v597 -v155 v5 v671 v408 -v331 v172 -v154 -v16 v672 v560 v406 v667 -v571 -v466 -v337 -v173 v567 v470 -v174 v781 v741 -v496 v422 v83 v745 v426 -v787 v502 -v88 -v856 v791 -v301 -v857 -v795 v747 v507 -v303 v91 -v75 v858 -v794 v748 -v348 -v309 -v89 -v74 -v22 v873 -v834 v761 -v585 -v510 v350 v305 -v257 -v21 -v838 -v765 -v584 -v508 -v435 v356 -v317 -v811 -v491 -v437 v352 -v263 -v211 v29 -v815 -v493 -v443 v364 -v33 -v698 -v439 -v268 -v217 v119 -v71 -v37 -v702 -v451 -v393 -v187 v120 -v36 -v817 v581 -v538 v487 -v395 -v271 -v205 -v156 v115 -v818 -v401 -v269 v201 -v160 -v158 -v704 v670 -v595 -v541 v488 v397 -v327 -v220 v200 -v162 v113 v19 -v705 v669 -v599 v409 v168 v20 -v722 -v568 -v333 v164 -v152 -v15 -v726 -v570 v175 v665 v601 -v465 -v338 -v153 -v131 -v13 v602 -v566 v469 v742 v434 -v79 v780 v746 -v495 v430 v84 v782 v750 -v497 v429 v80 v783 v749 v503 v92 -v876 v799 v499 v877 -v805 -v511 -v304 v872 -v836 v804 v760 v325 -v207 -v840 -v764 -v692 -v492 v351 v321 -v256 -v23 -v884 -v870 -v812 -v691 -v372 v320 v258 -v213 v118 -v24 -v888 -v816 -v438 -v368 -v264 v117 v25 -v842 -v820 -v699 -v459 -v367 v260 -v218 -v202 -v41 -v843 -v819 -v703 -v589 -v455 -v272 -v204 -v157 -v707 -v588 -v537 -v454 -v221 -v18 -v706 -v396 -v219 -v17 -v596 -v543 -v417 v198 -v114 -v600 -v569 -v413 -v326 -v163 -v721 v604 -v412 -v328 -v199 -v183 v127 -v725 v603 -v334 -v179 v666 v546 -v467 v330 -v178 v130 -v14 -v564 v471 v339 v903 v433 -v78 -v875 v802 -v754 v427 v100 -v874 -v830 v803 -v498 v96 -v829 v798 -v519 v428 -v322 v95 -v515 v324 -v837 -v796 v762 -v514 -v369 -v841 v806 v766 -v371 -v206 -v883 -v871 -v845 v807 -v456 -v318 -v291 -v208 v44 -v887 -v844 v808 -v693 -v458 v259 -v214 -v203 v45 -v824 -v768 -v694 v533 -v383 -v365 -v319 v280 -v210 -v40 -v769 -v695 v276 -v222 -v711 v619 v539 -v452 -v414 -v366 v275 -v38 v623 -v590 -v416 v591 -v544 -v453 -v180 v592 v461 -v182 -v723 -v608 v547 v460 -v410 v126 -v727 v545 -v329 -v468 -v411 -v347 -v176 v132 -v565 v472 v343 v801 -v431 v97 v800 v99 -v753 -v654 -v516 -v756 -v518 -v323 v755 -v751 v521 v93 -v831 v525 -v370 -v832 -v797 v763 -v512 v287 -v249 v94 v43 -v833 v767 -v457 v42 -v885 -v849 v827 v771 -v513 -v379 -v290 -v277 -v889 v828 -v770 v279 -v209 -v823 -v714 -v382 -v230 -v715 v532 -v415 -v226 v891 -v821 -v710 -v641 v618 v534 -v273 -v225 -v39 v892 -v717 -v645 v622 v540 -v181 -v716 -v708 -v679 v611 v536 -v274 -v122 -v55 -v683 v612 v548 -v724 -v607 -v344 v128 -v728 v462 -v346 v729 -v605 v463 -v240 -v177 v133 v730 v464 -v342 v904 -v432 v98 -v517 -v653 -v752 v520 -v245 -v879 v757 v524 -v878 -v852 -v826 v758 v286 v248 -v853 -v825 v759 -v278 -v886 -v848 v775 -v713 -v378 -v292 -v227 v890 -v712 -v229 v894 -v846 -v384 v893 -v822 -v640 v620 -v610 -v295 -v223 -v51 -v644 v624 -v609 v535 -v709 v678 v556 -v387 -v224 -v54 -v718 v682 -v552 -v345 v121 -v719 -v626 -v551 -v236 v123 v720 -v627 v12
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/26260/stat): 26260 (minisat+_script) R 26259 26260 19316 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843700651 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/26260/statm): 174 3 169 147 0 27 0 [pid=26260] 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=26261 New process pid=26262 New process pid=26263 execve syscall for /bin/sed executable One traced child (pid=26262) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=26263) exited with status: 0 One traced child (pid=26261) exited with status: 0 New process pid=26264 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-10:20:4.5:0.95:98.opb [startup+10.0031 s] Raw data (loadavg): 0.93 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) T 26260 26260 19316 0 -1 0 2621 0 0 0 969 12 0 0 25 0 1 0 1843700656 11137024 2482 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/26264/statm): 2719 2482 145 145 0 2574 0 [pid=26264] vsize: 10876 Current children cumulated CPU time (s) 9.81 Current children cumulated vsize (Kb) 13000 [startup+20.0047 s] Raw data (loadavg): 0.94 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 2822 0 0 0 1966 14 0 0 25 0 1 0 1843700656 11788288 2642 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 2878 2642 145 145 0 2733 0 [pid=26264] vsize: 11512 Current children cumulated CPU time (s) 19.8 Current children cumulated vsize (Kb) 13636 [startup+30.0053 s] Raw data (loadavg): 0.95 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 3486 0 0 0 2956 18 0 0 25 0 1 0 1843700656 14532608 3306 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26264/statm): 3548 3306 145 145 0 3403 0 [pid=26264] vsize: 14192 Current children cumulated CPU time (s) 29.74 Current children cumulated vsize (Kb) 16316 [startup+40.0059 s] Raw data (loadavg): 0.96 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 3735 0 0 0 3951 20 0 0 25 0 1 0 1843700656 15556608 3555 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 3798 3555 145 145 0 3653 0 [pid=26264] vsize: 15192 Current children cumulated CPU time (s) 39.71 Current children cumulated vsize (Kb) 17316 [startup+50.0065 s] Raw data (loadavg): 0.96 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 3740 0 0 0 4951 20 0 0 25 0 1 0 1843700656 15556608 3560 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 3798 3560 145 145 0 3653 0 [pid=26264] vsize: 15192 Current children cumulated CPU time (s) 49.71 Current children cumulated vsize (Kb) 17316 [startup+60.0061 s] Raw data (loadavg): 0.97 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 3740 0 0 0 5952 20 0 0 25 0 1 0 1843700656 15556608 3560 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 3798 3560 145 145 0 3653 0 [pid=26264] vsize: 15192 Current children cumulated CPU time (s) 59.72 Current children cumulated vsize (Kb) 17316 [startup+70.0067 s] Raw data (loadavg): 0.97 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 3828 0 0 0 6951 21 0 0 25 0 1 0 1843700656 15917056 3648 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26264/statm): 3886 3648 145 145 0 3741 0 [pid=26264] vsize: 15544 Current children cumulated CPU time (s) 69.72 Current children cumulated vsize (Kb) 17668 [startup+80.0073 s] Raw data (loadavg): 0.98 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 4052 0 0 0 7947 22 0 0 25 0 1 0 1843700656 16670720 3832 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 4070 3832 145 145 0 3925 0 [pid=26264] vsize: 16280 Current children cumulated CPU time (s) 79.69 Current children cumulated vsize (Kb) 18404 [startup+90.0079 s] Raw data (loadavg): 0.98 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 4335 0 0 0 8943 24 0 0 25 0 1 0 1843700656 17829888 4115 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 4353 4115 145 145 0 4208 0 [pid=26264] vsize: 17412 Current children cumulated CPU time (s) 89.67 Current children cumulated vsize (Kb) 19536 [startup+100.009 s] Raw data (loadavg): 0.98 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 4616 0 0 0 9939 25 0 0 25 0 1 0 1843700656 18980864 4396 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 4634 4396 145 145 0 4489 0 [pid=26264] vsize: 18536 Current children cumulated CPU time (s) 99.64 Current children cumulated vsize (Kb) 20660 [startup+110.009 s] Raw data (loadavg): 0.98 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 5548 0 0 0 10925 32 0 0 25 0 1 0 1843700656 22794240 5328 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 5565 5328 145 145 0 5420 0 [pid=26264] vsize: 22260 Current children cumulated CPU time (s) 109.57 Current children cumulated vsize (Kb) 24384 [startup+120.011 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 5563 0 0 0 11925 32 0 0 25 0 1 0 1843700656 22851584 5343 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 5579 5343 145 145 0 5434 0 [pid=26264] vsize: 22316 Current children cumulated CPU time (s) 119.57 Current children cumulated vsize (Kb) 24440 [startup+130.01 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 5563 0 0 0 12925 32 0 0 25 0 1 0 1843700656 22851584 5343 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 5579 5343 145 145 0 5434 0 [pid=26264] vsize: 22316 Current children cumulated CPU time (s) 129.57 Current children cumulated vsize (Kb) 24440 [startup+140.011 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 5882 0 0 0 13919 35 0 0 25 0 1 0 1843700656 24289280 5662 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26264/statm): 5930 5662 145 145 0 5785 0 [pid=26264] vsize: 23720 Current children cumulated CPU time (s) 139.54 Current children cumulated vsize (Kb) 25844 [startup+150.013 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 5882 0 0 0 14919 35 0 0 25 0 1 0 1843700656 24289280 5662 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 5930 5662 145 145 0 5785 0 [pid=26264] vsize: 23720 Current children cumulated CPU time (s) 149.54 Current children cumulated vsize (Kb) 25844 [startup+160.012 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 5882 0 0 0 15920 35 0 0 25 0 1 0 1843700656 24289280 5662 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 5930 5662 145 145 0 5785 0 [pid=26264] vsize: 23720 Current children cumulated CPU time (s) 159.55 Current children cumulated vsize (Kb) 25844 [startup+170.013 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 6425 0 0 0 16910 39 0 0 25 0 1 0 1843700656 26505216 6205 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26264/statm): 6471 6205 145 145 0 6326 0 [pid=26264] vsize: 25884 Current children cumulated CPU time (s) 169.49 Current children cumulated vsize (Kb) 28008 [startup+180.013 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 6425 0 0 0 17909 39 0 0 25 0 1 0 1843700656 26505216 6205 4294967295 134512640 135094434 3221224432 3221223072 134538540 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26264/statm): 6471 6205 145 145 0 6326 0 [pid=26264] vsize: 25884 Current children cumulated CPU time (s) 179.48 Current children cumulated vsize (Kb) 28008 [startup+190.015 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 6425 0 0 0 18909 40 0 0 25 0 1 0 1843700656 26505216 6205 4294967295 134512640 135094434 3221224432 3221223024 134552008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26264/statm): 6471 6205 145 145 0 6326 0 [pid=26264] vsize: 25884 Current children cumulated CPU time (s) 189.49 Current children cumulated vsize (Kb) 28008 [startup+200.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 6569 0 0 0 19906 41 0 0 25 0 1 0 1843700656 27095040 6349 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26264/statm): 6615 6349 145 145 0 6470 0 [pid=26264] vsize: 26460 Current children cumulated CPU time (s) 199.47 Current children cumulated vsize (Kb) 28584 [startup+210.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7453 0 0 0 20892 48 0 0 25 0 1 0 1843700656 30711808 7233 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26264/statm): 7498 7233 145 145 0 7353 0 [pid=26264] vsize: 29992 Current children cumulated CPU time (s) 209.4 Current children cumulated vsize (Kb) 32116 [startup+220.017 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 21884 51 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0 [pid=26264] vsize: 31796 Current children cumulated CPU time (s) 219.35 Current children cumulated vsize (Kb) 33920 [startup+230.017 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 22884 51 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223056 134557728 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0 [pid=26264] vsize: 31796 Current children cumulated CPU time (s) 229.35 Current children cumulated vsize (Kb) 33920 [startup+240.019 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 23883 52 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223120 134554748 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0 [pid=26264] vsize: 31796 Current children cumulated CPU time (s) 239.35 Current children cumulated vsize (Kb) 33920 [startup+250.02 s] Raw data (loadavg): 0.99 0.97 0.98 3/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 24883 52 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0 [pid=26264] vsize: 31796 Current children cumulated CPU time (s) 249.35 Current children cumulated vsize (Kb) 33920 [startup+260.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 25883 53 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0 [pid=26264] vsize: 31796 Current children cumulated CPU time (s) 259.36 Current children cumulated vsize (Kb) 33920 [startup+270.022 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 26882 53 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0 [pid=26264] vsize: 31796 Current children cumulated CPU time (s) 269.35 Current children cumulated vsize (Kb) 33920 [startup+280.022 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 27883 53 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0 [pid=26264] vsize: 31796 Current children cumulated CPU time (s) 279.36 Current children cumulated vsize (Kb) 33920 [startup+290.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 28882 54 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223024 134557310 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0 [pid=26264] vsize: 31796 Current children cumulated CPU time (s) 289.36 Current children cumulated vsize (Kb) 33920 [startup+300.025 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 29881 54 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223024 134557310 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0 [pid=26264] vsize: 31796 Current children cumulated CPU time (s) 299.35 Current children cumulated vsize (Kb) 33920 [startup+310.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 30881 54 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0 [pid=26264] vsize: 31796 Current children cumulated CPU time (s) 309.35 Current children cumulated vsize (Kb) 33920 [startup+320.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 31880 55 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0 [pid=26264] vsize: 31796 Current children cumulated CPU time (s) 319.35 Current children cumulated vsize (Kb) 33920 [startup+330.027 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 32880 55 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0 [pid=26264] vsize: 31796 Current children cumulated CPU time (s) 329.35 Current children cumulated vsize (Kb) 33920 [startup+340.028 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 33879 56 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0 [pid=26264] vsize: 31796 Current children cumulated CPU time (s) 339.35 Current children cumulated vsize (Kb) 33920 [startup+350.029 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 34880 56 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0 [pid=26264] vsize: 31796 Current children cumulated CPU time (s) 349.36 Current children cumulated vsize (Kb) 33920 [startup+360.029 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 35880 56 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0 [pid=26264] vsize: 31796 Current children cumulated CPU time (s) 359.36 Current children cumulated vsize (Kb) 33920 [startup+370.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 36880 57 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223024 134557321 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0 [pid=26264] vsize: 31796 Current children cumulated CPU time (s) 369.37 Current children cumulated vsize (Kb) 33920 [startup+380.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 37880 57 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0 [pid=26264] vsize: 31796 Current children cumulated CPU time (s) 379.37 Current children cumulated vsize (Kb) 33920 [startup+390.032 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 38880 57 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0 [pid=26264] vsize: 31796 Current children cumulated CPU time (s) 389.37 Current children cumulated vsize (Kb) 33920 [startup+400.033 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 7907 0 0 0 39880 57 0 0 25 0 1 0 1843700656 32559104 7687 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 7949 7687 145 145 0 7804 0 [pid=26264] vsize: 31796 Current children cumulated CPU time (s) 399.37 Current children cumulated vsize (Kb) 33920 [startup+410.033 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 8271 0 0 0 40875 59 0 0 25 0 1 0 1843700656 34054144 8051 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 8314 8051 145 145 0 8169 0 [pid=26264] vsize: 33256 Current children cumulated CPU time (s) 409.34 Current children cumulated vsize (Kb) 35380 [startup+420.034 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 9065 0 0 0 41860 65 0 0 25 0 1 0 1843700656 37289984 8845 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 9104 8845 145 145 0 8959 0 [pid=26264] vsize: 36416 Current children cumulated CPU time (s) 419.25 Current children cumulated vsize (Kb) 38540 [startup+430.034 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 9065 0 0 0 42860 65 0 0 25 0 1 0 1843700656 37289984 8845 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 9104 8845 145 145 0 8959 0 [pid=26264] vsize: 36416 Current children cumulated CPU time (s) 429.25 Current children cumulated vsize (Kb) 38540 [startup+440.035 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 9070 0 0 0 43860 65 0 0 25 0 1 0 1843700656 37322752 8850 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 9112 8850 145 145 0 8967 0 [pid=26264] vsize: 36448 Current children cumulated CPU time (s) 439.25 Current children cumulated vsize (Kb) 38572 [startup+450.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 9070 0 0 0 44860 65 0 0 25 0 1 0 1843700656 37322752 8850 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 9112 8850 145 145 0 8967 0 [pid=26264] vsize: 36448 Current children cumulated CPU time (s) 449.25 Current children cumulated vsize (Kb) 38572 [startup+460.035 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 9298 0 0 0 45856 66 0 0 25 0 1 0 1843700656 38256640 9078 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 9340 9078 145 145 0 9195 0 [pid=26264] vsize: 37360 Current children cumulated CPU time (s) 459.22 Current children cumulated vsize (Kb) 39484 [startup+470.037 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 10147 0 0 0 46842 73 0 0 25 0 1 0 1843700656 41754624 9927 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 10194 9927 145 145 0 10049 0 [pid=26264] vsize: 40776 Current children cumulated CPU time (s) 469.15 Current children cumulated vsize (Kb) 42900 [startup+480.037 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 10860 0 0 0 47831 78 0 0 25 0 1 0 1843700656 44675072 10640 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 10907 10640 145 145 0 10762 0 [pid=26264] vsize: 43628 Current children cumulated CPU time (s) 479.09 Current children cumulated vsize (Kb) 45752 [startup+490.038 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 11618 0 0 0 48819 84 0 0 25 0 1 0 1843700656 47800320 11398 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 11670 11398 145 145 0 11525 0 [pid=26264] vsize: 46680 Current children cumulated CPU time (s) 489.03 Current children cumulated vsize (Kb) 48804 [startup+500.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 12351 0 0 0 49806 89 0 0 25 0 1 0 1843700656 50802688 12131 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 12403 12131 145 145 0 12258 0 [pid=26264] vsize: 49612 Current children cumulated CPU time (s) 498.95 Current children cumulated vsize (Kb) 51736 [startup+510.038 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13066 0 0 0 50794 95 0 0 25 0 1 0 1843700656 53755904 12846 4294967295 134512640 135094434 3221224432 3221223024 134557277 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13124 12846 145 145 0 12979 0 [pid=26264] vsize: 52496 Current children cumulated CPU time (s) 508.89 Current children cumulated vsize (Kb) 54620 [startup+520.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13274 0 0 0 51791 96 0 0 25 0 1 0 1843700656 54607872 13054 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13332 13054 145 145 0 13187 0 [pid=26264] vsize: 53328 Current children cumulated CPU time (s) 518.87 Current children cumulated vsize (Kb) 55452 [startup+530.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13274 0 0 0 52791 96 0 0 25 0 1 0 1843700656 54607872 13054 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13332 13054 145 145 0 13187 0 [pid=26264] vsize: 53328 Current children cumulated CPU time (s) 528.87 Current children cumulated vsize (Kb) 55452 [startup+540.041 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13275 0 0 0 53792 96 0 0 25 0 1 0 1843700656 54607872 13055 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26264/statm): 13332 13055 145 145 0 13187 0 [pid=26264] vsize: 53328 Current children cumulated CPU time (s) 538.88 Current children cumulated vsize (Kb) 55452 [startup+550.042 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13275 0 0 0 54791 96 0 0 25 0 1 0 1843700656 54607872 13055 4294967295 134512640 135094434 3221224432 3221223024 134551702 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13332 13055 145 145 0 13187 0 [pid=26264] vsize: 53328 Current children cumulated CPU time (s) 548.87 Current children cumulated vsize (Kb) 55452 [startup+560.042 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13275 0 0 0 55791 97 0 0 25 0 1 0 1843700656 54607872 13055 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13332 13055 145 145 0 13187 0 [pid=26264] vsize: 53328 Current children cumulated CPU time (s) 558.88 Current children cumulated vsize (Kb) 55452 [startup+570.044 s] Raw data (loadavg): 0.99 0.97 0.98 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13275 0 0 0 56792 97 0 0 25 0 1 0 1843700656 54607872 13055 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13332 13055 145 145 0 13187 0 [pid=26264] vsize: 53328 Current children cumulated CPU time (s) 568.89 Current children cumulated vsize (Kb) 55452 [startup+580.043 s] Raw data (loadavg): 1.07 0.99 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13276 0 0 0 57792 97 0 0 25 0 1 0 1843700656 54607872 13056 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13332 13056 145 145 0 13187 0 [pid=26264] vsize: 53328 Current children cumulated CPU time (s) 578.89 Current children cumulated vsize (Kb) 55452 [startup+590.044 s] Raw data (loadavg): 1.14 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 58792 97 0 0 25 0 1 0 1843700656 54411264 13010 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13284 13010 145 145 0 13139 0 [pid=26264] vsize: 53136 Current children cumulated CPU time (s) 588.89 Current children cumulated vsize (Kb) 55260 [startup+600.044 s] Raw data (loadavg): 1.11 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 59792 97 0 0 25 0 1 0 1843700656 54411264 13010 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13284 13010 145 145 0 13139 0 [pid=26264] vsize: 53136 Current children cumulated CPU time (s) 598.89 Current children cumulated vsize (Kb) 55260 [startup+610.045 s] Raw data (loadavg): 1.10 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 60793 97 0 0 25 0 1 0 1843700656 54411264 13010 4294967295 134512640 135094434 3221224432 3221223024 134557435 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13284 13010 145 145 0 13139 0 [pid=26264] vsize: 53136 Current children cumulated CPU time (s) 608.9 Current children cumulated vsize (Kb) 55260 [startup+620.046 s] Raw data (loadavg): 1.08 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 61793 97 0 0 25 0 1 0 1843700656 54411264 13010 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13284 13010 145 145 0 13139 0 [pid=26264] vsize: 53136 Current children cumulated CPU time (s) 618.9 Current children cumulated vsize (Kb) 55260 [startup+630.046 s] Raw data (loadavg): 1.07 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 62793 97 0 0 25 0 1 0 1843700656 54411264 13010 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13284 13010 145 145 0 13139 0 [pid=26264] vsize: 53136 Current children cumulated CPU time (s) 628.9 Current children cumulated vsize (Kb) 55260 [startup+640.048 s] Raw data (loadavg): 1.06 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 63793 97 0 0 25 0 1 0 1843700656 54411264 13010 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13284 13010 145 145 0 13139 0 [pid=26264] vsize: 53136 Current children cumulated CPU time (s) 638.9 Current children cumulated vsize (Kb) 55260 [startup+650.048 s] Raw data (loadavg): 1.05 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 64793 97 0 0 25 0 1 0 1843700656 54112256 12937 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13211 12937 145 145 0 13066 0 [pid=26264] vsize: 52844 Current children cumulated CPU time (s) 648.9 Current children cumulated vsize (Kb) 54968 [startup+660.049 s] Raw data (loadavg): 1.04 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 65793 97 0 0 25 0 1 0 1843700656 54112256 12937 4294967295 134512640 135094434 3221224432 3221223024 134557485 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13211 12937 145 145 0 13066 0 [pid=26264] vsize: 52844 Current children cumulated CPU time (s) 658.9 Current children cumulated vsize (Kb) 54968 [startup+670.05 s] Raw data (loadavg): 1.03 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 66794 97 0 0 25 0 1 0 1843700656 54112256 12937 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13211 12937 145 145 0 13066 0 [pid=26264] vsize: 52844 Current children cumulated CPU time (s) 668.91 Current children cumulated vsize (Kb) 54968 [startup+680.05 s] Raw data (loadavg): 1.03 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 67794 97 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223024 134557157 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 678.91 Current children cumulated vsize (Kb) 54640 [startup+690.052 s] Raw data (loadavg): 1.02 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 68794 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 688.92 Current children cumulated vsize (Kb) 54640 [startup+700.053 s] Raw data (loadavg): 1.02 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 69794 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223024 134557372 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 698.92 Current children cumulated vsize (Kb) 54640 [startup+710.053 s] Raw data (loadavg): 1.02 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 70794 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 708.92 Current children cumulated vsize (Kb) 54640 [startup+720.054 s] Raw data (loadavg): 1.01 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 71794 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 718.92 Current children cumulated vsize (Kb) 54640 [startup+730.054 s] Raw data (loadavg): 1.01 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 72795 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 728.93 Current children cumulated vsize (Kb) 54640 [startup+740.055 s] Raw data (loadavg): 1.01 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 73795 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 738.93 Current children cumulated vsize (Kb) 54640 [startup+750.056 s] Raw data (loadavg): 1.01 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 74795 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 748.93 Current children cumulated vsize (Kb) 54640 [startup+760.056 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 75795 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 758.93 Current children cumulated vsize (Kb) 54640 [startup+770.057 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 76795 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 768.93 Current children cumulated vsize (Kb) 54640 [startup+780.057 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 77795 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 778.93 Current children cumulated vsize (Kb) 54640 [startup+790.058 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 78796 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 788.94 Current children cumulated vsize (Kb) 54640 [startup+800.058 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 79796 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 798.94 Current children cumulated vsize (Kb) 54640 [startup+810.059 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 80796 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 808.94 Current children cumulated vsize (Kb) 54640 [startup+820.061 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 81797 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 818.95 Current children cumulated vsize (Kb) 54640 [startup+830.061 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 82797 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 828.95 Current children cumulated vsize (Kb) 54640 [startup+840.062 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 83797 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223024 134551457 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 838.95 Current children cumulated vsize (Kb) 54640 [startup+850.062 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 84797 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 848.95 Current children cumulated vsize (Kb) 54640 [startup+860.063 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 85797 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 858.95 Current children cumulated vsize (Kb) 54640 [startup+870.064 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 86798 98 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 868.96 Current children cumulated vsize (Kb) 54640 [startup+880.064 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 87797 99 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 878.96 Current children cumulated vsize (Kb) 54640 [startup+890.068 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 88797 100 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 888.97 Current children cumulated vsize (Kb) 54640 [startup+900.068 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 89797 100 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 898.97 Current children cumulated vsize (Kb) 54640 [startup+910.069 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 90797 101 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 908.98 Current children cumulated vsize (Kb) 54640 [startup+920.071 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 91797 101 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 918.98 Current children cumulated vsize (Kb) 54640 [startup+930.071 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 92797 101 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 928.98 Current children cumulated vsize (Kb) 54640 [startup+940.072 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 93797 101 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 938.98 Current children cumulated vsize (Kb) 54640 [startup+950.072 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 94797 101 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 948.98 Current children cumulated vsize (Kb) 54640 [startup+960.073 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 95797 101 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 958.98 Current children cumulated vsize (Kb) 54640 [startup+970.074 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 96797 101 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 968.98 Current children cumulated vsize (Kb) 54640 [startup+980.074 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 97798 101 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 978.99 Current children cumulated vsize (Kb) 54640 [startup+990.076 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 98797 102 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 988.99 Current children cumulated vsize (Kb) 54640 [startup+1000.08 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 99798 102 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 999 Current children cumulated vsize (Kb) 54640 [startup+1010.08 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 100798 102 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 1009 Current children cumulated vsize (Kb) 54640 [startup+1020.08 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 101797 102 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 1018.99 Current children cumulated vsize (Kb) 54640 [startup+1030.08 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 102797 102 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 1028.99 Current children cumulated vsize (Kb) 54640 [startup+1040.08 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 103797 102 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 1038.99 Current children cumulated vsize (Kb) 54640 [startup+1050.08 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13278 0 0 0 104798 102 0 0 25 0 1 0 1843700656 53776384 12855 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12855 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 1049 Current children cumulated vsize (Kb) 54640 [startup+1060.08 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 105798 102 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223104 134556336 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 1059 Current children cumulated vsize (Kb) 54640 [startup+1070.08 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 106798 102 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 1069 Current children cumulated vsize (Kb) 54640 [startup+1080.08 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 107798 102 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 1079 Current children cumulated vsize (Kb) 54640 [startup+1090.08 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 108798 102 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 1089 Current children cumulated vsize (Kb) 54640 [startup+1100.08 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 109799 102 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 1099.01 Current children cumulated vsize (Kb) 54640 [startup+1110.08 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 110798 103 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223024 134557494 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 1109.01 Current children cumulated vsize (Kb) 54640 [startup+1120.08 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 111799 103 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 1119.02 Current children cumulated vsize (Kb) 54640 [startup+1130.08 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 112799 103 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 1129.02 Current children cumulated vsize (Kb) 54640 [startup+1140.08 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 113799 103 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 1139.02 Current children cumulated vsize (Kb) 54640 [startup+1150.09 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 114799 103 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223024 134557037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 1149.02 Current children cumulated vsize (Kb) 54640 [startup+1160.09 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 115799 103 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223104 134555673 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 1159.02 Current children cumulated vsize (Kb) 54640 [startup+1170.09 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 116800 103 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 1169.03 Current children cumulated vsize (Kb) 54640 [startup+1180.09 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 117800 103 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 1179.03 Current children cumulated vsize (Kb) 54640 [startup+1190.09 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 118800 103 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 1189.03 Current children cumulated vsize (Kb) 54640 [startup+1200.09 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 119800 103 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 1199.03 Current children cumulated vsize (Kb) 54640 [startup+1210.09 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 120801 103 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 1209.04 Current children cumulated vsize (Kb) 54640 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 1.00 1.00 0.99 2/57 26264 Raw data (/proc/26260/stat): 26260 (minisat+_script) S 26259 26260 19316 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1843700651 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26260/statm): 531 226 485 147 0 384 0 [pid=26260] vsize: 2124 Raw data (/proc/26264/stat): 26264 (minisat+_64-bit) R 26260 26260 19316 0 -1 0 13280 0 0 0 120801 103 0 0 25 0 1 0 1843700656 53776384 12857 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26264/statm): 13129 12857 145 145 0 12984 0 [pid=26264] vsize: 52516 Current children cumulated CPU time (s) 1209.04 Current children cumulated vsize (Kb) 54640 Sending SIGTERM to -26260 Sleeping 2 seconds One traced child (pid=26260) ended because it received signal 15 (SIGTERM) One traced child (pid=26264) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.12 CPU time (s): 1209.07 CPU user time (s): 1208.02 CPU system time (s): 1.05884 CPU usage (%): 99.9134 Max. virtual memory (cumulated for all children) (Kb): 55452
ERROR: no interpretation found !