Name | submitted/een/normalized-p0282.opb |
MD5SUM | dd62132555621025f45a5a6099c90742 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 258411 |
Optimality of the best value was proved | YES |
Number of terms in the objective function | 282 |
Biggest coefficient in the objective function | 160646 |
Number of bits for the biggest coefficient in the objective function | 18 |
Sum of the numbers in the objective function | 1302615 |
Number of bits of the sum of numbers in the objective function | 21 |
Biggest number in a constraint | 160646 |
Number of bits of the biggest number in a constraint | 18 |
Biggest sum of numbers in a constraint | 1302615 |
Number of bits of the biggest sum of numbers | 21 |
Best result obtained on this benchmark | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 24.5993 |
Number of variables | 282 |
Total number of constraints | 221 |
Number of constraints which are clauses | 177 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 44 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 57 |
LAUNCH ON wulflinc20 THE 2005-09-18 18:24:56 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2618 boxname=wulflinc20 idbench=274 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: dd62132555621025f45a5a6099c90742 /oldhome/oroussel/tmp/wulflinc20/normalized-p0282.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc20/normalized-p0282.opb IDLAUNCH: 2618 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 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.215 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 912344 kB Buffers: 35380 kB Cached: 58308 kB SwapCached: 832 kB Active: 66684 kB Inactive: 29624 kB HighTotal: 131008 kB HighFree: 69412 kB LowTotal: 903652 kB LowFree: 842932 kB SwapTotal: 2097892 kB SwapFree: 2096604 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5732 kB Slab: 20456 kB Committed_AS: 64140 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-18 18:45:06 (client local time) WITH STATUS 10 IN 1209.3 SECONDS stats: 2618 7 1209.3 10
c Parsing PB file... c Converting 221 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .................................................................................................................................................................................sss c ---[ 46]---> BDD-cost: 4 c ---[ 45]---> BDD-cost: 8 c ---[ 44]---> BDD-cost: 10 c ---[ 43]---> BDD-cost: 16 c ---[ 42]---> Sorter-cost: 1109 Base: 2 5 3 3 c ---[ 41]---> Sorter-cost: 898 Base: 2 5 3 2 c ---[ 40]---> Sorter-cost: 1116 Base: 2 5 5 c ---[ 38]---> Sorter-cost: 1010 Base: 2 5 5 c ---[ 37]---> Sorter-cost: 909 Base: 2 5 5 c ---[ 36]---> Sorter-cost: 998 Base: 2 5 3 2 c ---[ 35]---> Sorter-cost: 852 Base: 2 5 3 3 c ---[ 34]---> Sorter-cost: 842 Base: 5 2 3 3 c ---[ 33]---> Sorter-cost: 712 Base: 5 2 3 3 c ---[ 32]---> Sorter-cost: 946 Base: 2 5 3 3 c ---[ 31]---> Sorter-cost: 841 Base: 2 5 3 3 c ---[ 30]---> Sorter-cost: 909 Base: 2 5 5 c ---[ 29]---> Sorter-cost: 935 Base: 2 5 3 2 c ---[ 28]---> Sorter-cost: 998 Base: 2 5 3 c ---[ 27]---> Sorter-cost: 762 Base: 5 2 3 3 c ---[ 26]---> Sorter-cost: 908 Base: 2 5 5 c ---[ 25]---> Sorter-cost: 907 Base: 2 5 5 c ---[ 24]---> Sorter-cost: 713 Base: 5 2 3 3 c ---[ 23]---> Sorter-cost: 908 Base: 2 5 5 c ---[ 22]---> Sorter-cost: 909 Base: 2 5 5 c ---[ 21]---> Sorter-cost: 1008 Base: 2 5 3 c ---[ 20]---> Sorter-cost: 898 Base: 2 5 3 3 c ---[ 19]---> Sorter-cost: 841 Base: 2 5 3 3 c ---[ 18]---> Sorter-cost: 760 Base: 2 5 3 3 c ---[ 17]---> Sorter-cost: 713 Base: 5 2 3 3 c ---[ 16]---> Sorter-cost: 1071 Base: 2 5 3 3 c ---[ 15]---> Sorter-cost: 949 Base: 2 5 3 3 c ---[ 14]---> BDD-cost: 26 c ---[ 13]---> Sorter-cost: 1108 Base: 2 5 3 3 c ---[ 11]---> Sorter-cost: 1081 Base: 2 5 3 3 c ---[ 10]---> Sorter-cost: 999 Base: 2 5 3 2 c ---[ 9]---> Sorter-cost: 995 Base: 2 5 3 3 c ---[ 8]---> Sorter-cost: 982 Base: 2 5 3 2 c ---[ 7]---> Sorter-cost: 996 Base: 2 5 3 3 c ---[ 5]---> BDD-cost: 56 c ---[ 4]---> BDD-cost: 56 c ---[ 3]---> BDD-cost: 56 c ---[ 2]---> BDD-cost: 12 c ---[ 1]---> Sorter-cost: 717 Base: 2 5 3 c ---[ 0]---> Sorter-cost: 655 Base: 2 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 70255 164891 | 23418 0 0 nan | 0.000 % | c | 100 | 69917 164139 | 25759 93 577 6.2 | 0.539 % | c ============================================================================== c [1mFound solution: 628263[0m c ---[ 0]---> Sorter-cost:77312 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 154 | 289324 676780 | 96441 145 1012 7.0 | 0.539 % | c | 254 | 289196 676496 | 106085 241 7343 30.5 | 0.195 % | c | 404 | 289140 676372 | 116693 389 8935 23.0 | 0.210 % | c | 629 | 289026 676117 | 128362 613 10286 16.8 | 0.239 % | c | 967 | 288994 676045 | 141199 949 19599 20.7 | 0.248 % | c | 1473 | 288994 676045 | 155319 1455 26362 18.1 | 0.248 % | c | 2232 | 288994 676045 | 170851 2214 33093 14.9 | 0.248 % | c | 3371 | 288854 675733 | 187936 3345 114434 34.2 | 0.285 % | c | 5080 | 288563 675077 | 206729 5053 138020 27.3 | 0.356 % | c ============================================================================== c [1mFound solution: 566001[0m c ---[ 0]---> Sorter-cost: 10 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5423 | 288839 675889 | 96279 5395 169300 31.4 | 0.356 % | c | 5523 | 288839 675889 | 105906 5495 170399 31.0 | 0.359 % | c | 5674 | 288839 675889 | 116497 5646 171301 30.3 | 0.359 % | c | 5899 | 288743 675673 | 128147 5869 175852 30.0 | 0.384 % | c | 6236 | 288743 675673 | 140962 6206 177830 28.7 | 0.384 % | c | 6742 | 288688 675549 | 155058 6711 181373 27.0 | 0.399 % | c | 7501 | 288688 675549 | 170564 7470 186837 25.0 | 0.399 % | c | 8640 | 288688 675549 | 187620 8609 216152 25.1 | 0.399 % | c ============================================================================== c [1mFound solution: 484674[0m c ---[ 0]---> Sorter-cost: 13 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10092 | 288996 676700 | 96332 10053 237028 23.6 | 0.399 % | c | 10193 | 288996 676700 | 105965 10154 237467 23.4 | 0.473 % | c | 10343 | 288996 676700 | 116561 10304 238188 23.1 | 0.473 % | c | 10568 | 288996 676700 | 128217 10529 239895 22.8 | 0.473 % | c | 10905 | 288996 676700 | 141039 10866 248577 22.9 | 0.473 % | c | 11412 | 288996 676700 | 155143 11373 259298 22.8 | 0.473 % | c | 12171 | 288851 676374 | 170658 12127 270935 22.3 | 0.512 % | c | 13310 | 288847 676365 | 187723 13265 320224 24.1 | 0.513 % | c ============================================================================== c [1mFound solution: 445249[0m c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14034 | 289183 677345 | 96394 13931 345351 24.8 | 0.513 % | c | 14134 | 289183 677345 | 106033 14031 345862 24.6 | 0.575 % | c | 14285 | 289162 677300 | 116636 14181 351345 24.8 | 0.582 % | c | 14510 | 289162 677300 | 128300 14406 356420 24.7 | 0.582 % | c | 14847 | 289100 677161 | 141130 14740 360896 24.5 | 0.601 % | c | 15353 | 288611 676053 | 155243 15228 370340 24.3 | 0.741 % | c | 16112 | 288611 676053 | 170767 15987 409928 25.6 | 0.741 % | c | 17255 | 288391 675554 | 187844 17122 447923 26.2 | 0.803 % | c | 18963 | 288078 674859 | 206629 18820 529203 28.1 | 0.890 % | c | 21525 | 288034 674761 | 227292 21380 570591 26.7 | 0.902 % | c | 25371 | 288034 674761 | 250021 25226 640379 25.4 | 0.902 % | c ============================================================================== c [1mFound solution: 444335[0m c ---[ 0]---> Sorter-cost: 13 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 26271 | 288407 675860 | 96135 26126 763005 29.2 | 0.902 % | c | 26371 | 288407 675860 | 105748 26226 763504 29.1 | 0.901 % | c | 26521 | 288407 675860 | 116323 26375 770197 29.2 | 0.907 % | c | 26746 | 288386 675814 | 127955 26600 778032 29.2 | 0.907 % | c | 27085 | 288363 675762 | 140751 26938 780776 29.0 | 0.915 % | c | 27591 | 288316 675654 | 154826 27443 802878 29.3 | 0.930 % | c | 28350 | 288316 675654 | 170309 28202 825991 29.3 | 0.930 % | c | 29489 | 288316 675654 | 187339 29341 845911 28.8 | 0.930 % | c ============================================================================== c [1mFound solution: 436563[0m c ---[ 0]---> Sorter-cost: 7 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 30056 | 288324 675691 | 96108 29908 872577 29.2 | 0.930 % | c | 30156 | 288275 675585 | 105718 30004 876794 29.2 | 0.945 % | c | 30306 | 288275 675585 | 116290 30154 888553 29.5 | 0.945 % | c | 30532 | 288203 675424 | 127919 30379 901516 29.7 | 0.964 % | c | 30870 | 288163 675336 | 140711 30716 915078 29.8 | 0.975 % | c | 31376 | 288163 675336 | 154782 31222 924876 29.6 | 0.975 % | c | 32137 | 287950 674856 | 170261 31949 937478 29.3 | 1.036 % | c | 33276 | 287871 674673 | 187287 33082 954844 28.9 | 1.063 % | c | 34984 | 287756 674415 | 206016 34788 981681 28.2 | 1.093 % | c | 37548 | 287736 674370 | 226617 37351 1248671 33.4 | 1.098 % | c | 41392 | 287637 674148 | 249279 41193 1343488 32.6 | 1.123 % | c ============================================================================== c [1mFound solution: 436402[0m c ---[ 0]---> Sorter-cost: 7 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 43764 | 287605 674082 | 95868 43564 1447376 33.2 | 1.123 % | c | 43867 | 287605 674082 | 105454 43667 1448737 33.2 | 1.133 % | c | 44018 | 287605 674082 | 116000 43818 1449657 33.1 | 1.133 % | c | 44244 | 287605 674082 | 127600 44044 1460157 33.2 | 1.133 % | c | 44581 | 287560 673982 | 140360 44380 1479136 33.3 | 1.145 % | c | 45088 | 287560 673982 | 154396 44887 1496111 33.3 | 1.145 % | c | 45848 | 287223 673220 | 169836 45621 1520809 33.3 | 1.238 % | c | 46988 | 287163 673084 | 186819 46758 1538696 32.9 | 1.256 % | c | 48697 | 287039 672805 | 205501 48465 1592787 32.9 | 1.289 % | c | 51261 | 286990 672696 | 226051 51028 1898314 37.2 | 1.303 % | c | 55105 | 286990 672696 | 248656 54872 2298636 41.9 | 1.303 % | c | 60871 | 286990 672696 | 273522 60638 2869733 47.3 | 1.303 % | c ============================================================================== c [1mFound solution: 435910[0m c ---[ 0]---> Sorter-cost: 12 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 63492 | 286856 672401 | 95618 63256 3040113 48.1 | 1.303 % | c | 63592 | 286856 672401 | 105179 63356 3040956 48.0 | 1.340 % | c | 63743 | 286856 672401 | 115697 63507 3046265 48.0 | 1.340 % | c | 63968 | 286856 672401 | 127267 63732 3058484 48.0 | 1.340 % | c | 64306 | 286815 672308 | 139994 64069 3075581 48.0 | 1.350 % | c ============================================================================== c [1mFound solution: 435909[0m c ---[ 0]---> Sorter-cost: 13 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 64468 | 286827 672341 | 95609 64231 3084273 48.0 | 1.350 % | c | 64568 | 286827 672341 | 105169 64331 3085548 48.0 | 1.351 % | c | 64718 | 286452 671488 | 115686 64436 3086303 47.9 | 1.456 % | c | 64943 | 286452 671488 | 127255 64661 3088405 47.8 | 1.456 % | c | 65280 | 286452 671488 | 139981 64998 3091356 47.6 | 1.456 % | c | 65786 | 286440 671461 | 153979 65501 3105468 47.4 | 1.459 % | c ============================================================================== c [1mFound solution: 433675[0m c ---[ 0]---> Sorter-cost: 9 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 66530 | 286450 671528 | 95483 66245 3144016 47.5 | 1.459 % | c | 66630 | 286450 671528 | 105031 66345 3144764 47.4 | 1.460 % | c | 66780 | 286450 671528 | 115534 66495 3147292 47.3 | 1.460 % | c | 67005 | 286450 671528 | 127087 66720 3168130 47.5 | 1.460 % | c | 67342 | 286396 671405 | 139796 67054 3206859 47.8 | 1.474 % | c | 67848 | 286396 671405 | 153776 67560 3222948 47.7 | 1.474 % | c | 68607 | 286396 671405 | 169153 68319 3233174 47.3 | 1.474 % | c | 69746 | 286396 671405 | 186069 69458 3332574 48.0 | 1.474 % | c | 71454 | 286372 671351 | 204676 71165 3432460 48.2 | 1.482 % | c ============================================================================== c [1mFound solution: 429382[0m c ---[ 0]---> Sorter-cost: 10 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 72160 | 286384 671380 | 95461 71871 3458870 48.1 | 1.482 % | c | 72260 | 286384 671380 | 105007 71971 3461748 48.1 | 1.483 % | c | 72411 | 286340 671278 | 115507 72120 3463828 48.0 | 1.497 % | c | 72636 | 286340 671278 | 127058 72345 3469925 48.0 | 1.497 % | c | 72973 | 286340 671278 | 139764 72682 3483184 47.9 | 1.497 % | c | 73479 | 286340 671278 | 153740 73188 3502426 47.9 | 1.497 % | c | 74238 | 286340 671278 | 169114 73947 3510471 47.5 | 1.497 % | c | 75377 | 286340 671278 | 186026 75086 3755391 50.0 | 1.497 % | c | 77086 | 286143 670826 | 204629 76775 3812101 49.7 | 1.558 % | c | 79648 | 286064 670648 | 225092 79322 3887526 49.0 | 1.579 % | c ============================================================================== c [1mFound solution: 389989[0m c ---[ 0]---> Sorter-cost: 9 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 82574 | 286093 670721 | 95364 82248 4017147 48.8 | 1.579 % | c | 82675 | 286093 670721 | 104900 82349 4018604 48.8 | 1.580 % | c | 82827 | 285926 670342 | 115390 82480 4019751 48.7 | 1.627 % | c | 83052 | 285926 670342 | 126929 82705 4020916 48.6 | 1.627 % | c | 83389 | 285926 670342 | 139622 83042 4067516 49.0 | 1.627 % | c | 83895 | 285926 670342 | 153584 83548 4081876 48.9 | 1.627 % | c | 84654 | 285906 670297 | 168943 84306 4136077 49.1 | 1.633 % | c | 85794 | 285906 670297 | 185837 85446 4266042 49.9 | 1.633 % | c | 87505 | 285861 670194 | 204421 87135 4307281 49.4 | 1.647 % | c ============================================================================== c [1mFound solution: 380037[0m c ---[ 0]---> Sorter-cost: 12 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 88132 | 285880 670357 | 95293 87762 4424781 50.4 | 1.647 % | c | 88233 | 285880 670357 | 104822 87863 4425663 50.4 | 1.647 % | c | 88383 | 285880 670357 | 115304 88013 4426722 50.3 | 1.647 % | c | 88608 | 285880 670357 | 126834 88238 4434089 50.3 | 1.647 % | c | 88947 | 285880 670357 | 139518 88577 4448639 50.2 | 1.647 % | c | 89453 | 285880 670357 | 153470 89083 4552809 51.1 | 1.647 % | c | 90212 | 285880 670357 | 168817 89842 4625864 51.5 | 1.647 % | c | 91351 | 285880 670357 | 185699 90981 4649981 51.1 | 1.647 % | c | 93061 | 285809 670195 | 204269 92673 4689988 50.6 | 1.668 % | c | 95623 | 285809 670195 | 224695 95235 4809300 50.5 | 1.668 % | c | 99467 | 285809 670195 | 247165 99079 5424523 54.7 | 1.668 % | c ============================================================================== c [1mFound solution: 376742[0m c ---[ 0]---> Sorter-cost: 15 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 102944 | 285767 670104 | 95255 102555 5563757 54.3 | 1.668 % | c | 103044 | 285767 670104 | 104780 31949 1034771 32.4 | 1.684 % | c ============================================================================== c [1mFound solution: 370710[0m c ---[ 0]---> Sorter-cost: 9 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 103120 | 285749 670068 | 95249 32023 1036273 32.4 | 1.684 % | c | 103221 | 285749 670068 | 104773 32124 1038051 32.3 | 1.693 % | c | 103371 | 285749 670068 | 115251 32274 1038728 32.2 | 1.693 % | c | 103596 | 285749 670068 | 126776 32499 1055537 32.5 | 1.693 % | c | 103933 | 285749 670068 | 139454 32836 1067491 32.5 | 1.693 % | c | 104439 | 285749 670068 | 153399 33342 1100316 33.0 | 1.693 % | c | 105198 | 285749 670068 | 168739 34101 1126293 33.0 | 1.693 % | c | 106337 | 285698 669949 | 185613 35239 1187793 33.7 | 1.708 % | c ============================================================================== c [1mFound solution: 369981[0m c ---[ 0]---> Sorter-cost: 6 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 107949 | 285682 669915 | 95227 36850 1504973 40.8 | 1.708 % | c | 108052 | 285682 669915 | 104749 36953 1506173 40.8 | 1.717 % | c | 108202 | 285682 669915 | 115224 37103 1507610 40.6 | 1.717 % | c | 108428 | 285682 669915 | 126747 37329 1515140 40.6 | 1.717 % | c | 108765 | 285682 669915 | 139421 37666 1529271 40.6 | 1.717 % | c | 109271 | 285682 669915 | 153364 38172 1556483 40.8 | 1.717 % | c | 110032 | 285682 669915 | 168700 38933 1603181 41.2 | 1.717 % | c ============================================================================== c [1mFound solution: 369979[0m c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 110278 | 285690 669939 | 95230 39179 1612569 41.2 | 1.717 % | c | 110379 | 285633 669810 | 104753 39279 1615846 41.1 | 1.732 % | c | 110529 | 285633 669810 | 115228 39429 1617918 41.0 | 1.732 % | c | 110755 | 285506 669522 | 126751 39644 1619251 40.8 | 1.767 % | c | 111094 | 285506 669522 | 139426 39983 1642570 41.1 | 1.767 % | c | 111600 | 285506 669522 | 153368 40489 1711038 42.3 | 1.767 % | c | 112359 | 285506 669522 | 168705 41248 1757059 42.6 | 1.767 % | c ============================================================================== c [1mFound solution: 366578[0m c ---[ 0]---> Sorter-cost: 12 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 113082 | 285514 669547 | 95171 41971 1829234 43.6 | 1.767 % | c | 113183 | 285468 669444 | 104688 42069 1831438 43.5 | 1.780 % | c | 113335 | 285468 669444 | 115156 42221 1834165 43.4 | 1.780 % | c | 113561 | 285468 669444 | 126672 42447 1845787 43.5 | 1.780 % | c | 113899 | 285449 669402 | 139339 42784 1869641 43.7 | 1.785 % | c | 114406 | 285430 669360 | 153273 43290 1904924 44.0 | 1.790 % | c | 115165 | 285430 669360 | 168601 44049 1959172 44.5 | 1.790 % | c | 116304 | 285430 669360 | 185461 45188 2046279 45.3 | 1.790 % | c | 118014 | 285430 669360 | 204007 46898 2170140 46.3 | 1.790 % | c | 120577 | 285430 669360 | 224408 49461 2316819 46.8 | 1.790 % | c | 124422 | 285317 669105 | 246849 53304 2510434 47.1 | 1.818 % | c | 130188 | 285317 669105 | 271533 59070 2821596 47.8 | 1.818 % | c ============================================================================== c [1mFound solution: 366570[0m c ---[ 0]---> Sorter-cost: 12 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 131845 | 285328 669136 | 95109 60727 2949783 48.6 | 1.818 % | c | 131946 | 285328 669136 | 104619 60828 2953165 48.5 | 1.819 % | c | 132096 | 285328 669136 | 115081 60978 2961053 48.6 | 1.819 % | c | 132321 | 285328 669136 | 126590 61203 2971592 48.6 | 1.819 % | c | 132658 | 285328 669136 | 139249 61540 2979009 48.4 | 1.819 % | c | 133164 | 285328 669136 | 153173 62046 3021918 48.7 | 1.819 % | c | 133924 | 285298 669070 | 168491 62805 3109161 49.5 | 1.827 % | c | 135063 | 285298 669070 | 185340 63944 3194490 50.0 | 1.827 % | c | 136771 | 285204 668861 | 203874 65650 3399419 51.8 | 1.853 % | c ============================================================================== c [1mFound solution: 365125[0m c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 137522 | 285218 668892 | 95072 66401 3415093 51.4 | 1.853 % | c | 137623 | 285218 668892 | 104579 66502 3415717 51.4 | 1.854 % | c | 137773 | 285218 668892 | 115037 66652 3416706 51.3 | 1.854 % | c | 137999 | 285218 668892 | 126540 66878 3418322 51.1 | 1.854 % | c | 138336 | 285218 668892 | 139194 67215 3440255 51.2 | 1.854 % | c | 138842 | 285218 668892 | 153114 67721 3480470 51.4 | 1.854 % | c | 139602 | 285218 668892 | 168425 68481 3545219 51.8 | 1.854 % | c ============================================================================== c [1mFound solution: 360746[0m c ---[ 0]---> Sorter-cost: 6 Base: 3 3 3 3 2 3 3 3 3 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 139957 | 285208 668877 | 95069 68835 3617548 52.6 | 1.854 % | c | 140057 | 285208 668877 | 104575 68935 3621012 52.5 | 1.861 % | c | 140207 | 285208 668877 | 115033 69085 3622746 52.4 | 1.861 % | c | 140432 | 285208 668877 | 126536 69310 3635414 52.5 | 1.861 % | c | 140769 | 285208 668877 | 139190 69647 3648677 52.4 | 1.861 % | c | 141275 | 285208 668877 | 153109 70153 3672456 52.3 | 1.861 % | c | 142035 | 285208 668877 | 168420 70913 3706877 52.3 | 1.861 % | c | 143174 | 285208 668877 | 185262 72052 3785458 52.5 | 1.861 % |
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/13194/stat): 13194 (minisat+_script) R 13193 13194 2660 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843395303 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/13194/statm): 174 3 169 147 0 27 0 [pid=13194] 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=13195 New process pid=13196 New process pid=13197 execve syscall for /bin/sed executable One traced child (pid=13196) 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=13197) exited with status: 0 One traced child (pid=13195) exited with status: 0 New process pid=13198 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-p0282.opb [startup+10.004 s] Raw data (loadavg): 0.94 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 8526 0 0 0 928 35 0 0 25 0 1 0 1843395308 37228544 8171 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 9089 8171 145 145 0 8944 0 [pid=13198] vsize: 36356 Current children cumulated CPU time (s) 9.63 Current children cumulated vsize (Kb) 38480 [startup+20.0048 s] Raw data (loadavg): 0.95 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 8710 0 0 0 1925 37 0 0 25 0 1 0 1843395308 37838848 8355 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 9238 8355 145 145 0 9093 0 [pid=13198] vsize: 36952 Current children cumulated CPU time (s) 19.62 Current children cumulated vsize (Kb) 39076 [startup+30.0055 s] Raw data (loadavg): 0.95 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 8897 0 0 0 2923 37 0 0 25 0 1 0 1843395308 38522880 8542 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13198/statm): 9405 8542 145 145 0 9260 0 [pid=13198] vsize: 37620 Current children cumulated CPU time (s) 29.6 Current children cumulated vsize (Kb) 39744 [startup+40.0062 s] Raw data (loadavg): 0.96 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 8977 0 0 0 3923 38 0 0 25 0 1 0 1843395308 38858752 8622 4294967295 134512640 135094434 3221224448 3221223072 134557702 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 9487 8622 145 145 0 9342 0 [pid=13198] vsize: 37948 Current children cumulated CPU time (s) 39.61 Current children cumulated vsize (Kb) 40072 [startup+50.0079 s] Raw data (loadavg): 0.97 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 9050 0 0 0 4922 38 0 0 25 0 1 0 1843395308 39145472 8695 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 9557 8695 145 145 0 9412 0 [pid=13198] vsize: 38228 Current children cumulated CPU time (s) 49.6 Current children cumulated vsize (Kb) 40352 [startup+60.0086 s] Raw data (loadavg): 0.97 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 9131 0 0 0 5922 38 0 0 25 0 1 0 1843395308 39485440 8776 4294967295 134512640 135094434 3221224448 3221221648 134600232 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 9640 8776 145 145 0 9495 0 [pid=13198] vsize: 38560 Current children cumulated CPU time (s) 59.6 Current children cumulated vsize (Kb) 40684 [startup+70.0094 s] Raw data (loadavg): 0.98 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 9146 0 0 0 6921 38 0 0 25 0 1 0 1843395308 39522304 8791 4294967295 134512640 135094434 3221224448 3221223140 134558984 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13198/statm): 9649 8791 145 145 0 9504 0 [pid=13198] vsize: 38596 Current children cumulated CPU time (s) 69.59 Current children cumulated vsize (Kb) 40720 [startup+80.0111 s] Raw data (loadavg): 0.98 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 9219 0 0 0 7920 39 0 0 25 0 1 0 1843395308 39870464 8864 4294967295 134512640 135094434 3221224448 3221223120 134556415 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 9734 8864 145 145 0 9589 0 [pid=13198] vsize: 38936 Current children cumulated CPU time (s) 79.59 Current children cumulated vsize (Kb) 41060 [startup+90.0118 s] Raw data (loadavg): 0.98 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 9283 0 0 0 8919 39 0 0 25 0 1 0 1843395308 40128512 8928 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 9797 8928 145 145 0 9652 0 [pid=13198] vsize: 39188 Current children cumulated CPU time (s) 89.58 Current children cumulated vsize (Kb) 41312 [startup+100.013 s] Raw data (loadavg): 0.98 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 9398 0 0 0 9917 40 0 0 25 0 1 0 1843395308 40583168 9043 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 9908 9043 145 145 0 9763 0 [pid=13198] vsize: 39632 Current children cumulated CPU time (s) 99.57 Current children cumulated vsize (Kb) 41756 [startup+110.013 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 9646 0 0 0 10914 42 0 0 25 0 1 0 1843395308 41582592 9291 4294967295 134512640 135094434 3221224448 3221221040 134676280 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 10152 9291 145 145 0 10007 0 [pid=13198] vsize: 40608 Current children cumulated CPU time (s) 109.56 Current children cumulated vsize (Kb) 42732 [startup+120.014 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 9684 0 0 0 11913 42 0 0 25 0 1 0 1843395308 41709568 9329 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 10183 9329 145 145 0 10038 0 [pid=13198] vsize: 40732 Current children cumulated CPU time (s) 119.55 Current children cumulated vsize (Kb) 42856 [startup+130.015 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 9747 0 0 0 12912 43 0 0 25 0 1 0 1843395308 41959424 9392 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 10244 9392 145 145 0 10099 0 [pid=13198] vsize: 40976 Current children cumulated CPU time (s) 129.55 Current children cumulated vsize (Kb) 43100 [startup+140.015 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 9802 0 0 0 13911 43 0 0 25 0 1 0 1843395308 42172416 9447 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 10296 9447 145 145 0 10151 0 [pid=13198] vsize: 41184 Current children cumulated CPU time (s) 139.54 Current children cumulated vsize (Kb) 43308 [startup+150.017 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 9845 0 0 0 14911 43 0 0 25 0 1 0 1843395308 42344448 9490 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 10338 9490 145 145 0 10193 0 [pid=13198] vsize: 41352 Current children cumulated CPU time (s) 149.54 Current children cumulated vsize (Kb) 43476 [startup+160.018 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 9942 0 0 0 15909 44 0 0 25 0 1 0 1843395308 42860544 9587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 10464 9587 145 145 0 10319 0 [pid=13198] vsize: 41856 Current children cumulated CPU time (s) 159.53 Current children cumulated vsize (Kb) 43980 [startup+170.019 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 10087 0 0 0 16907 45 0 0 25 0 1 0 1843395308 43450368 9732 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 10608 9732 145 145 0 10463 0 [pid=13198] vsize: 42432 Current children cumulated CPU time (s) 169.52 Current children cumulated vsize (Kb) 44556 [startup+180.019 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 10199 0 0 0 17905 46 0 0 25 0 1 0 1843395308 43905024 9844 4294967295 134512640 135094434 3221224448 3221223104 134558298 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 10719 9844 145 145 0 10574 0 [pid=13198] vsize: 42876 Current children cumulated CPU time (s) 179.51 Current children cumulated vsize (Kb) 45000 [startup+190.02 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 10305 0 0 0 18903 46 0 0 25 0 1 0 1843395308 44322816 9950 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 10821 9950 145 145 0 10676 0 [pid=13198] vsize: 43284 Current children cumulated CPU time (s) 189.49 Current children cumulated vsize (Kb) 45408 [startup+200.021 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 10356 0 0 0 19903 47 0 0 25 0 1 0 1843395308 44531712 10001 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 10872 10001 145 145 0 10727 0 [pid=13198] vsize: 43488 Current children cumulated CPU time (s) 199.5 Current children cumulated vsize (Kb) 45612 [startup+210.021 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 10459 0 0 0 20901 47 0 0 25 0 1 0 1843395308 44945408 10104 4294967295 134512640 135094434 3221224448 3221221004 134677228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 10973 10104 145 145 0 10828 0 [pid=13198] vsize: 43892 Current children cumulated CPU time (s) 209.48 Current children cumulated vsize (Kb) 46016 [startup+220.022 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 10479 0 0 0 21901 47 0 0 25 0 1 0 1843395308 45015040 10124 4294967295 134512640 135094434 3221224448 3221223040 134551702 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 10990 10124 145 145 0 10845 0 [pid=13198] vsize: 43960 Current children cumulated CPU time (s) 219.48 Current children cumulated vsize (Kb) 46084 [startup+230.023 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 10544 0 0 0 22901 48 0 0 25 0 1 0 1843395308 45273088 10189 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 11053 10189 145 145 0 10908 0 [pid=13198] vsize: 44212 Current children cumulated CPU time (s) 229.49 Current children cumulated vsize (Kb) 46336 [startup+240.024 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 10616 0 0 0 23900 48 0 0 25 0 1 0 1843395308 45613056 10261 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 11136 10261 145 145 0 10991 0 [pid=13198] vsize: 44544 Current children cumulated CPU time (s) 239.48 Current children cumulated vsize (Kb) 46668 [startup+250.025 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 10721 0 0 0 24899 49 0 0 25 0 1 0 1843395308 46018560 10366 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 11235 10366 145 145 0 11090 0 [pid=13198] vsize: 44940 Current children cumulated CPU time (s) 249.48 Current children cumulated vsize (Kb) 47064 [startup+260.026 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 10868 0 0 0 25897 50 0 0 25 0 1 0 1843395308 46620672 10513 4294967295 134512640 135094434 3221224448 3221223120 134555579 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 11382 10513 145 145 0 11237 0 [pid=13198] vsize: 45528 Current children cumulated CPU time (s) 259.47 Current children cumulated vsize (Kb) 47652 [startup+270.027 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 10990 0 0 0 26895 50 0 0 25 0 1 0 1843395308 47112192 10635 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 11502 10635 145 145 0 11357 0 [pid=13198] vsize: 46008 Current children cumulated CPU time (s) 269.45 Current children cumulated vsize (Kb) 48132 [startup+280.028 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11128 0 0 0 27893 52 0 0 25 0 1 0 1843395308 47673344 10773 4294967295 134512640 135094434 3221224448 3221223072 134557568 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 11639 10773 145 145 0 11494 0 [pid=13198] vsize: 46556 Current children cumulated CPU time (s) 279.45 Current children cumulated vsize (Kb) 48680 [startup+290.028 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11227 0 0 0 28892 52 0 0 25 0 1 0 1843395308 48074752 10872 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 11737 10872 145 145 0 11592 0 [pid=13198] vsize: 46948 Current children cumulated CPU time (s) 289.44 Current children cumulated vsize (Kb) 49072 [startup+300.029 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11309 0 0 0 29890 53 0 0 25 0 1 0 1843395308 48406528 10954 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 11818 10954 145 145 0 11673 0 [pid=13198] vsize: 47272 Current children cumulated CPU time (s) 299.43 Current children cumulated vsize (Kb) 49396 [startup+310.03 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11375 0 0 0 30890 54 0 0 25 0 1 0 1843395308 48672768 11020 4294967295 134512640 135094434 3221224448 3221223040 134556812 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 11883 11020 145 145 0 11738 0 [pid=13198] vsize: 47532 Current children cumulated CPU time (s) 309.44 Current children cumulated vsize (Kb) 49656 [startup+320.03 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11438 0 0 0 31889 54 0 0 25 0 1 0 1843395308 48930816 11083 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 11946 11083 145 145 0 11801 0 [pid=13198] vsize: 47784 Current children cumulated CPU time (s) 319.43 Current children cumulated vsize (Kb) 49908 [startup+330.032 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11498 0 0 0 32888 55 0 0 25 0 1 0 1843395308 49172480 11143 4294967295 134512640 135094434 3221224448 3221223040 134557269 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 12005 11143 145 145 0 11860 0 [pid=13198] vsize: 48020 Current children cumulated CPU time (s) 329.43 Current children cumulated vsize (Kb) 50144 [startup+340.033 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11552 0 0 0 33887 55 0 0 25 0 1 0 1843395308 49393664 11197 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 12059 11197 145 145 0 11914 0 [pid=13198] vsize: 48236 Current children cumulated CPU time (s) 339.42 Current children cumulated vsize (Kb) 50360 [startup+350.034 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11617 0 0 0 34885 56 0 0 25 0 1 0 1843395308 49655808 11262 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 12123 11262 145 145 0 11978 0 [pid=13198] vsize: 48492 Current children cumulated CPU time (s) 349.41 Current children cumulated vsize (Kb) 50616 [startup+360.034 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11688 0 0 0 35884 57 0 0 25 0 1 0 1843395308 49946624 11333 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 12194 11333 145 145 0 12049 0 [pid=13198] vsize: 48776 Current children cumulated CPU time (s) 359.41 Current children cumulated vsize (Kb) 50900 [startup+370.034 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11771 0 0 0 36882 58 0 0 25 0 1 0 1843395308 50282496 11416 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 12276 11416 145 145 0 12131 0 [pid=13198] vsize: 49104 Current children cumulated CPU time (s) 369.4 Current children cumulated vsize (Kb) 51228 [startup+380.035 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11837 0 0 0 37881 58 0 0 25 0 1 0 1843395308 50548736 11482 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 12341 11482 145 145 0 12196 0 [pid=13198] vsize: 49364 Current children cumulated CPU time (s) 379.39 Current children cumulated vsize (Kb) 51488 [startup+390.035 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11908 0 0 0 38880 59 0 0 25 0 1 0 1843395308 50839552 11553 4294967295 134512640 135094434 3221224448 3221223040 134556870 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 12412 11553 145 145 0 12267 0 [pid=13198] vsize: 49648 Current children cumulated CPU time (s) 389.39 Current children cumulated vsize (Kb) 51772 [startup+400.037 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 11980 0 0 0 39879 59 0 0 25 0 1 0 1843395308 51130368 11625 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13198/statm): 12483 11625 145 145 0 12338 0 [pid=13198] vsize: 49932 Current children cumulated CPU time (s) 399.38 Current children cumulated vsize (Kb) 52056 [startup+410.038 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12022 0 0 0 40877 60 0 0 25 0 1 0 1843395308 51302400 11667 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 12525 11667 145 145 0 12380 0 [pid=13198] vsize: 50100 Current children cumulated CPU time (s) 409.37 Current children cumulated vsize (Kb) 52224 [startup+420.038 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12086 0 0 0 41876 60 0 0 25 0 1 0 1843395308 51560448 11731 4294967295 134512640 135094434 3221224448 3221223108 134553508 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 12588 11731 145 145 0 12443 0 [pid=13198] vsize: 50352 Current children cumulated CPU time (s) 419.36 Current children cumulated vsize (Kb) 52476 [startup+430.038 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12198 0 0 0 42874 61 0 0 25 0 1 0 1843395308 52015104 11843 4294967295 134512640 135094434 3221224448 3221221648 134677346 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 12699 11843 145 145 0 12554 0 [pid=13198] vsize: 50796 Current children cumulated CPU time (s) 429.35 Current children cumulated vsize (Kb) 52920 [startup+440.039 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12218 0 0 0 43874 62 0 0 25 0 1 0 1843395308 52092928 11863 4294967295 134512640 135094434 3221224448 3221223072 134557612 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 12718 11863 145 145 0 12573 0 [pid=13198] vsize: 50872 Current children cumulated CPU time (s) 439.36 Current children cumulated vsize (Kb) 52996 [startup+450.04 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12259 0 0 0 44874 62 0 0 25 0 1 0 1843395308 52256768 11904 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 12758 11904 145 145 0 12613 0 [pid=13198] vsize: 51032 Current children cumulated CPU time (s) 449.36 Current children cumulated vsize (Kb) 53156 [startup+460.041 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12331 0 0 0 45873 62 0 0 25 0 1 0 1843395308 52805632 11976 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 12892 11976 145 145 0 12747 0 [pid=13198] vsize: 51568 Current children cumulated CPU time (s) 459.35 Current children cumulated vsize (Kb) 53692 [startup+470.041 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12412 0 0 0 46872 62 0 0 25 0 1 0 1843395308 53129216 12057 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 12971 12057 145 145 0 12826 0 [pid=13198] vsize: 51884 Current children cumulated CPU time (s) 469.34 Current children cumulated vsize (Kb) 54008 [startup+480.042 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12523 0 0 0 47870 63 0 0 25 0 1 0 1843395308 53579776 12168 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 13081 12168 145 145 0 12936 0 [pid=13198] vsize: 52324 Current children cumulated CPU time (s) 479.33 Current children cumulated vsize (Kb) 54448 [startup+490.043 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12580 0 0 0 48870 64 0 0 25 0 1 0 1843395308 53809152 12225 4294967295 134512640 135094434 3221224448 3221223104 134558169 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 13137 12225 145 145 0 12992 0 [pid=13198] vsize: 52548 Current children cumulated CPU time (s) 489.34 Current children cumulated vsize (Kb) 54672 [startup+500.044 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12646 0 0 0 49869 64 0 0 25 0 1 0 1843395308 54075392 12291 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 13202 12291 145 145 0 13057 0 [pid=13198] vsize: 52808 Current children cumulated CPU time (s) 499.33 Current children cumulated vsize (Kb) 54932 [startup+510.045 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12689 0 0 0 50869 64 0 0 25 0 1 0 1843395308 54247424 12334 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 13244 12334 145 145 0 13099 0 [pid=13198] vsize: 52976 Current children cumulated CPU time (s) 509.33 Current children cumulated vsize (Kb) 55100 [startup+520.046 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12791 0 0 0 51868 65 0 0 25 0 1 0 1843395308 54661120 12436 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 13345 12436 145 145 0 13200 0 [pid=13198] vsize: 53380 Current children cumulated CPU time (s) 519.33 Current children cumulated vsize (Kb) 55504 [startup+530.047 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 12979 0 0 0 52865 66 0 0 25 0 1 0 1843395308 55427072 12624 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 13532 12624 145 145 0 13387 0 [pid=13198] vsize: 54128 Current children cumulated CPU time (s) 529.31 Current children cumulated vsize (Kb) 56252 [startup+540.047 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 13022 0 0 0 53864 66 0 0 25 0 1 0 1843395308 55599104 12667 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 13574 12667 145 145 0 13429 0 [pid=13198] vsize: 54296 Current children cumulated CPU time (s) 539.3 Current children cumulated vsize (Kb) 56420 [startup+550.049 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 13086 0 0 0 54863 67 0 0 25 0 1 0 1843395308 55853056 12731 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 13636 12731 145 145 0 13491 0 [pid=13198] vsize: 54544 Current children cumulated CPU time (s) 549.3 Current children cumulated vsize (Kb) 56668 [startup+560.05 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 13198 0 0 0 55861 68 0 0 25 0 1 0 1843395308 56303616 12843 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 13746 12843 145 145 0 13601 0 [pid=13198] vsize: 54984 Current children cumulated CPU time (s) 559.29 Current children cumulated vsize (Kb) 57108 [startup+570.05 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 13343 0 0 0 56859 69 0 0 25 0 1 0 1843395308 56885248 12988 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 13888 12988 145 145 0 13743 0 [pid=13198] vsize: 55552 Current children cumulated CPU time (s) 569.28 Current children cumulated vsize (Kb) 57676 [startup+580.051 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 13372 0 0 0 57859 69 0 0 25 0 1 0 1843395308 57004032 13017 4294967295 134512640 135094434 3221224448 3221223072 134557728 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 13917 13017 145 145 0 13772 0 [pid=13198] vsize: 55668 Current children cumulated CPU time (s) 579.28 Current children cumulated vsize (Kb) 57792 [startup+590.052 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 13449 0 0 0 58857 70 0 0 25 0 1 0 1843395308 57315328 13094 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 13993 13094 145 145 0 13848 0 [pid=13198] vsize: 55972 Current children cumulated CPU time (s) 589.27 Current children cumulated vsize (Kb) 58096 [startup+600.053 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 13544 0 0 0 59857 70 0 0 25 0 1 0 1843395308 57700352 13189 4294967295 134512640 135094434 3221224448 3221223040 134557273 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 14087 13189 145 145 0 13942 0 [pid=13198] vsize: 56348 Current children cumulated CPU time (s) 599.27 Current children cumulated vsize (Kb) 58472 [startup+610.053 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 13617 0 0 0 60855 71 0 0 25 0 1 0 1843395308 57991168 13262 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 14158 13262 145 145 0 14013 0 [pid=13198] vsize: 56632 Current children cumulated CPU time (s) 609.26 Current children cumulated vsize (Kb) 58756 [startup+620.054 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 13768 0 0 0 61854 72 0 0 25 0 1 0 1843395308 58609664 13413 4294967295 134512640 135094434 3221224448 3221223236 134553536 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 14309 13413 145 145 0 14164 0 [pid=13198] vsize: 57236 Current children cumulated CPU time (s) 619.26 Current children cumulated vsize (Kb) 59360 [startup+630.055 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 13815 0 0 0 62853 72 0 0 25 0 1 0 1843395308 58798080 13460 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 14355 13460 145 145 0 14210 0 [pid=13198] vsize: 57420 Current children cumulated CPU time (s) 629.25 Current children cumulated vsize (Kb) 59544 [startup+640.056 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 13931 0 0 0 63852 73 0 0 25 0 1 0 1843395308 59269120 13576 4294967295 134512640 135094434 3221224448 3221223084 134557639 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 14470 13576 145 145 0 14325 0 [pid=13198] vsize: 57880 Current children cumulated CPU time (s) 639.25 Current children cumulated vsize (Kb) 60004 [startup+650.057 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 13990 0 0 0 64851 73 0 0 25 0 1 0 1843395308 59506688 13635 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 14528 13635 145 145 0 14383 0 [pid=13198] vsize: 58112 Current children cumulated CPU time (s) 649.24 Current children cumulated vsize (Kb) 60236 [startup+660.058 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 14038 0 0 0 65850 73 0 0 25 0 1 0 1843395308 59695104 13683 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 14574 13683 145 145 0 14429 0 [pid=13198] vsize: 58296 Current children cumulated CPU time (s) 659.23 Current children cumulated vsize (Kb) 60420 [startup+670.059 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 14144 0 0 0 66848 74 0 0 25 0 1 0 1843395308 60133376 13789 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 14681 13789 145 145 0 14536 0 [pid=13198] vsize: 58724 Current children cumulated CPU time (s) 669.22 Current children cumulated vsize (Kb) 60848 [startup+680.06 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 14233 0 0 0 67847 75 0 0 25 0 1 0 1843395308 60493824 13878 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 14769 13878 145 145 0 14624 0 [pid=13198] vsize: 59076 Current children cumulated CPU time (s) 679.22 Current children cumulated vsize (Kb) 61200 [startup+690.061 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 14327 0 0 0 68846 75 0 0 25 0 1 0 1843395308 60874752 13972 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 14862 13972 145 145 0 14717 0 [pid=13198] vsize: 59448 Current children cumulated CPU time (s) 689.21 Current children cumulated vsize (Kb) 61572 [startup+700.063 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 14486 0 0 0 69843 76 0 0 25 0 1 0 1843395308 61526016 14131 4294967295 134512640 135094434 3221224448 3221223040 134556975 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15021 14131 145 145 0 14876 0 [pid=13198] vsize: 60084 Current children cumulated CPU time (s) 699.19 Current children cumulated vsize (Kb) 62208 [startup+710.064 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 14622 0 0 0 70842 77 0 0 25 0 1 0 1843395308 62078976 14267 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15156 14267 145 145 0 15011 0 [pid=13198] vsize: 60624 Current children cumulated CPU time (s) 709.19 Current children cumulated vsize (Kb) 62748 [startup+720.063 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 14806 0 0 0 71840 78 0 0 25 0 1 0 1843395308 62828544 14451 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15339 14451 145 145 0 15194 0 [pid=13198] vsize: 61356 Current children cumulated CPU time (s) 719.18 Current children cumulated vsize (Kb) 63480 [startup+730.064 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 14889 0 0 0 72839 78 0 0 25 0 1 0 1843395308 63168512 14534 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15422 14534 145 145 0 15277 0 [pid=13198] vsize: 61688 Current children cumulated CPU time (s) 729.17 Current children cumulated vsize (Kb) 63812 [startup+740.065 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 14981 0 0 0 73838 79 0 0 25 0 1 0 1843395308 63524864 14626 4294967295 134512640 135094434 3221224448 3221223060 134563083 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15509 14626 145 145 0 15364 0 [pid=13198] vsize: 62036 Current children cumulated CPU time (s) 739.17 Current children cumulated vsize (Kb) 64160 [startup+750.066 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15013 0 0 0 74838 79 0 0 25 0 1 0 1843395308 63651840 14658 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14658 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 749.17 Current children cumulated vsize (Kb) 64284 [startup+760.066 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15013 0 0 0 75838 79 0 0 25 0 1 0 1843395308 63651840 14658 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14658 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 759.17 Current children cumulated vsize (Kb) 64284 [startup+770.067 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15013 0 0 0 76838 79 0 0 25 0 1 0 1843395308 63651840 14658 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13198/statm): 15540 14658 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 769.17 Current children cumulated vsize (Kb) 64284 [startup+780.069 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15013 0 0 0 77837 80 0 0 25 0 1 0 1843395308 63651840 14658 4294967295 134512640 135094434 3221224448 3221223104 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13198/statm): 15540 14658 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 779.17 Current children cumulated vsize (Kb) 64284 [startup+790.069 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15013 0 0 0 78837 80 0 0 25 0 1 0 1843395308 63651840 14658 4294967295 134512640 135094434 3221224448 3221223104 134557872 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13198/statm): 15540 14658 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 789.17 Current children cumulated vsize (Kb) 64284 [startup+800.071 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15013 0 0 0 79836 80 0 0 25 0 1 0 1843395308 63651840 14658 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14658 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 799.16 Current children cumulated vsize (Kb) 64284 [startup+810.073 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15013 0 0 0 80837 80 0 0 25 0 1 0 1843395308 63651840 14658 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14658 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 809.17 Current children cumulated vsize (Kb) 64284 [startup+820.073 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15013 0 0 0 81837 80 0 0 25 0 1 0 1843395308 63651840 14658 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14658 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 819.17 Current children cumulated vsize (Kb) 64284 [startup+830.074 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15013 0 0 0 82837 80 0 0 25 0 1 0 1843395308 63651840 14658 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14658 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 829.17 Current children cumulated vsize (Kb) 64284 [startup+840.075 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15014 0 0 0 83838 80 0 0 25 0 1 0 1843395308 63651840 14659 4294967295 134512640 135094434 3221224448 3221221472 134676489 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14659 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 839.18 Current children cumulated vsize (Kb) 64284 [startup+850.077 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15016 0 0 0 84838 80 0 0 25 0 1 0 1843395308 63651840 14661 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14661 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 849.18 Current children cumulated vsize (Kb) 64284 [startup+860.077 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 85838 80 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 859.18 Current children cumulated vsize (Kb) 64284 [startup+870.078 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 86838 80 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 869.18 Current children cumulated vsize (Kb) 64284 [startup+880.08 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 87838 80 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 879.18 Current children cumulated vsize (Kb) 64284 [startup+890.081 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 88839 80 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134557832 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 889.19 Current children cumulated vsize (Kb) 64284 [startup+900.081 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 89839 80 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 899.19 Current children cumulated vsize (Kb) 64284 [startup+910.082 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 90839 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 909.2 Current children cumulated vsize (Kb) 64284 [startup+920.083 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 91839 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 919.2 Current children cumulated vsize (Kb) 64284 [startup+930.083 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 92839 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 929.2 Current children cumulated vsize (Kb) 64284 [startup+940.084 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 93840 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 939.21 Current children cumulated vsize (Kb) 64284 [startup+950.086 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 94840 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 949.21 Current children cumulated vsize (Kb) 64284 [startup+960.087 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 95839 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 959.2 Current children cumulated vsize (Kb) 64284 [startup+970.087 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 96839 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134557988 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 969.2 Current children cumulated vsize (Kb) 64284 [startup+980.088 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 97839 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 979.2 Current children cumulated vsize (Kb) 64284 [startup+990.089 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 98839 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223120 134556317 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 989.2 Current children cumulated vsize (Kb) 64284 [startup+1000.09 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 99839 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 999.2 Current children cumulated vsize (Kb) 64284 [startup+1010.09 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 100840 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 1009.21 Current children cumulated vsize (Kb) 64284 [startup+1020.09 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 101840 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223040 134557537 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 1019.21 Current children cumulated vsize (Kb) 64284 [startup+1030.09 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 102840 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 1029.21 Current children cumulated vsize (Kb) 64284 [startup+1040.09 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 103840 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134558289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 1039.21 Current children cumulated vsize (Kb) 64284 [startup+1050.1 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 104841 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 1049.22 Current children cumulated vsize (Kb) 64284 [startup+1060.1 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15017 0 0 0 105841 81 0 0 25 0 1 0 1843395308 63651840 14662 4294967295 134512640 135094434 3221224448 3221223104 134557978 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14662 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 1059.22 Current children cumulated vsize (Kb) 64284 [startup+1070.1 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15018 0 0 0 106841 81 0 0 25 0 1 0 1843395308 63651840 14663 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14663 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 1069.22 Current children cumulated vsize (Kb) 64284 [startup+1080.1 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15018 0 0 0 107841 81 0 0 25 0 1 0 1843395308 63651840 14663 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14663 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 1079.22 Current children cumulated vsize (Kb) 64284 [startup+1090.1 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15018 0 0 0 108842 81 0 0 25 0 1 0 1843395308 63651840 14663 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14663 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 1089.23 Current children cumulated vsize (Kb) 64284 [startup+1100.1 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15018 0 0 0 109842 81 0 0 25 0 1 0 1843395308 63651840 14663 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14663 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 1099.23 Current children cumulated vsize (Kb) 64284 [startup+1110.1 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15018 0 0 0 110842 81 0 0 25 0 1 0 1843395308 63651840 14663 4294967295 134512640 135094434 3221224448 3221223040 134557034 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14663 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 1109.23 Current children cumulated vsize (Kb) 64284 [startup+1120.1 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15018 0 0 0 111842 81 0 0 25 0 1 0 1843395308 63651840 14663 4294967295 134512640 135094434 3221224448 3221221216 134677138 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14663 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 1119.23 Current children cumulated vsize (Kb) 64284 [startup+1130.1 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15018 0 0 0 112843 82 0 0 25 0 1 0 1843395308 63651840 14663 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14663 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 1129.25 Current children cumulated vsize (Kb) 64284 [startup+1140.1 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15018 0 0 0 113843 82 0 0 25 0 1 0 1843395308 63651840 14663 4294967295 134512640 135094434 3221224448 3221223108 134553536 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14663 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 1139.25 Current children cumulated vsize (Kb) 64284 [startup+1150.11 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15018 0 0 0 114843 82 0 0 25 0 1 0 1843395308 63651840 14663 4294967295 134512640 135094434 3221224448 3221221648 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14663 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 1149.25 Current children cumulated vsize (Kb) 64284 [startup+1160.11 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15019 0 0 0 115843 82 0 0 25 0 1 0 1843395308 63651840 14664 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14664 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 1159.25 Current children cumulated vsize (Kb) 64284 [startup+1170.11 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15019 0 0 0 116844 82 0 0 25 0 1 0 1843395308 63651840 14664 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14664 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 1169.26 Current children cumulated vsize (Kb) 64284 [startup+1180.11 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15019 0 0 0 117844 82 0 0 25 0 1 0 1843395308 63651840 14664 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14664 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 1179.26 Current children cumulated vsize (Kb) 64284 [startup+1190.11 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15019 0 0 0 118844 82 0 0 25 0 1 0 1843395308 63651840 14664 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14664 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 1189.26 Current children cumulated vsize (Kb) 64284 [startup+1200.11 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15019 0 0 0 119844 82 0 0 25 0 1 0 1843395308 63651840 14664 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14664 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 1199.26 Current children cumulated vsize (Kb) 64284 [startup+1210.11 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15019 0 0 0 120844 82 0 0 25 0 1 0 1843395308 63651840 14664 4294967295 134512640 135094434 3221224448 3221223072 134562088 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14664 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 1209.26 Current children cumulated vsize (Kb) 64284 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.11 s] Raw data (loadavg): 0.99 0.98 0.97 2/57 13198 Raw data (/proc/13194/stat): 13194 (minisat+_script) S 13193 13194 2660 0 -1 0 288 239 0 0 0 0 0 0 22 0 1 0 1843395303 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/13194/statm): 531 226 485 147 0 384 0 [pid=13194] vsize: 2124 Raw data (/proc/13198/stat): 13198 (minisat+_64-bit) R 13194 13194 2660 0 -1 0 15019 0 0 0 120845 82 0 0 25 0 1 0 1843395308 63651840 14664 4294967295 134512640 135094434 3221224448 3221223120 134555413 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/13198/statm): 15540 14664 145 145 0 15395 0 [pid=13198] vsize: 62160 Current children cumulated CPU time (s) 1209.27 Current children cumulated vsize (Kb) 64284 Sending SIGTERM to -13194 Sleeping 2 seconds One traced child (pid=13194) ended because it received signal 15 (SIGTERM) One traced child (pid=13198) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.14 CPU time (s): 1209.3 CPU user time (s): 1208.45 CPU system time (s): 0.85087 CPU usage (%): 99.9304 Max. virtual memory (cumulated for all children) (Kb): 64284
ERROR: no interpretation found !