Name | mps-v2-20-10/plato.asu.edu/pub/fctp/normalized-mps-v2-20-10-gr4x6.opb |
MD5SUM | d90fce7408f7990dccb3ba4f8fa1c8f6 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 24752128 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 744 |
Biggest coefficient in the objective function | 151934468096 |
Number of bits for the biggest coefficient in the objective function | 38 |
Sum of the numbers in the objective function | 3470370333536 |
Number of bits of the sum of numbers in the objective function | 42 |
Biggest number in a constraint | 151934468096 |
Number of bits of the biggest number in a constraint | 38 |
Biggest sum of numbers in a constraint | 3470370333536 |
Number of bits of the biggest sum of numbers | 42 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.05 |
Number of variables | 744 |
Total number of constraints | 34 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 34 |
Minimum length of a constraint | 31 |
Maximum length of a constraint | 180 |
LAUNCH ON wulflinc30 THE 2005-09-19 18:23:10 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3021 boxname=wulflinc30 idbench=677 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: d90fce7408f7990dccb3ba4f8fa1c8f6 /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-gr4x6.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-gr4x6.opb IDLAUNCH: 3021 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 903156 kB Buffers: 32680 kB Cached: 70256 kB SwapCached: 764 kB Active: 33452 kB Inactive: 72092 kB HighTotal: 131008 kB HighFree: 60088 kB LowTotal: 903652 kB LowFree: 843068 kB SwapTotal: 2097892 kB SwapFree: 2096620 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5712 kB Slab: 20480 kB Committed_AS: 64304 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-19 18:43:20 (client local time) WITH STATUS 10 IN 1209.37 SECONDS stats: 3021 7 1209.37 10
c Parsing PB file... c Converting 44 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ########## c -- Clauses(.)/Splits(s): (none) c ---[ 42]---> Sorter-cost: 1236 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 40]---> Sorter-cost: 1236 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 38]---> Sorter-cost: 1164 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 36]---> Sorter-cost: 1152 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 34]---> Sorter-cost: 591 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 32]---> Sorter-cost: 575 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 30]---> Sorter-cost: 575 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 28]---> Sorter-cost: 519 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 26]---> Sorter-cost: 479 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 24]---> Sorter-cost: 479 Base: 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 23]---> BDD-cost: 22 c ---[ 22]---> BDD-cost: 19 c ---[ 21]---> BDD-cost: 16 c ---[ 20]---> BDD-cost: 16 c ---[ 19]---> BDD-cost: 18 c ---[ 18]---> BDD-cost: 18 c ---[ 17]---> BDD-cost: 18 c ---[ 16]---> BDD-cost: 18 c ---[ 15]---> BDD-cost: 16 c ---[ 14]---> BDD-cost: 16 c ---[ 13]---> BDD-cost: 18 c ---[ 12]---> BDD-cost: 18 c ---[ 11]---> BDD-cost: 20 c ---[ 10]---> BDD-cost: 18 c ---[ 9]---> BDD-cost: 18 c ---[ 8]---> BDD-cost: 16 c ---[ 7]---> BDD-cost: 16 c ---[ 6]---> BDD-cost: 18 c ---[ 5]---> BDD-cost: 16 c ---[ 4]---> BDD-cost: 16 c ---[ 3]---> BDD-cost: 22 c ---[ 2]---> BDD-cost: 19 c ---[ 1]---> BDD-cost: 20 c ---[ 0]---> BDD-cost: 18 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 20089 47581 | 6696 0 0 nan | 0.000 % | c | 100 | 20089 47581 | 7365 100 393 3.9 | 10.732 % | c | 250 | 20039 47467 | 8102 246 1058 4.3 | 10.902 % | c ============================================================================== c [1mFound solution: 48834098[0m c ---[ 0]---> Sorter-cost:80542 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 370 | 245919 574838 | 81973 366 1616 4.4 | 10.902 % | c | 472 | 245919 574838 | 90170 468 2875 6.1 | 0.987 % | c | 622 | 245919 574838 | 99187 618 5853 9.5 | 0.987 % | c | 849 | 245919 574838 | 109106 845 14016 16.6 | 0.987 % | c | 1186 | 245907 574812 | 120016 1180 28174 23.9 | 0.992 % | c | 1692 | 245756 574471 | 132018 1682 32367 19.2 | 1.040 % | c | 2452 | 245756 574471 | 145220 2442 41855 17.1 | 1.040 % | c | 3591 | 245756 574471 | 159742 3581 60900 17.0 | 1.040 % | c | 5299 | 245756 574471 | 175716 5289 78968 14.9 | 1.040 % | c ============================================================================== c [1mFound solution: 48658918[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6135 | 246491 576704 | 82163 6125 91885 15.0 | 1.040 % | c | 6235 | 246491 576704 | 90379 6225 92395 14.8 | 1.036 % | c | 6385 | 246491 576704 | 99417 6375 93090 14.6 | 1.036 % | c | 6612 | 246491 576704 | 109358 6602 95928 14.5 | 1.036 % | c | 6950 | 246433 576574 | 120294 6934 99591 14.4 | 1.054 % | c ============================================================================== c [1mFound solution: 48585107[0m c ---[ 0]---> Sorter-cost: 18 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6973 | 246457 576787 | 82152 6957 99867 14.4 | 1.054 % | c | 7073 | 246457 576787 | 90367 7057 103129 14.6 | 1.055 % | c ============================================================================== c [1mFound solution: 47745280[0m c ---[ 0]---> Sorter-cost: 18 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7205 | 246689 577396 | 82229 7184 104557 14.6 | 1.055 % | c | 7306 | 246689 577396 | 90451 7285 105083 14.4 | 1.089 % | c ============================================================================== c [1mFound solution: 47085915[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7349 | 246710 577456 | 82236 7328 105520 14.4 | 1.089 % | c | 7452 | 246710 577456 | 90459 7431 107688 14.5 | 1.090 % | c | 7603 | 246710 577456 | 99505 7582 110295 14.5 | 1.090 % | c ============================================================================== c [1mFound solution: 44602157[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7643 | 246761 577605 | 82253 7622 110961 14.6 | 1.090 % | c | 7744 | 246761 577605 | 90478 7723 111503 14.4 | 1.091 % | c | 7894 | 246761 577605 | 99526 7873 114029 14.5 | 1.091 % | c | 8120 | 246761 577605 | 109478 8099 116121 14.3 | 1.091 % | c | 8458 | 246761 577605 | 120426 8437 121174 14.4 | 1.091 % | c | 8964 | 246761 577605 | 132469 8943 140295 15.7 | 1.091 % | c | 9723 | 246713 577497 | 145716 9698 160602 16.6 | 1.105 % | c ============================================================================== c [1mFound solution: 43117436[0m c ---[ 0]---> Sorter-cost: 19 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10758 | 246413 576829 | 82137 10726 172946 16.1 | 1.105 % | c | 10859 | 246381 576755 | 90350 10825 177797 16.4 | 1.228 % | c ============================================================================== c [1mFound solution: 38341632[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10911 | 246445 576993 | 82148 10877 179492 16.5 | 1.228 % | c | 11011 | 246445 576993 | 90362 10977 189352 17.2 | 1.229 % | c | 11162 | 246445 576993 | 99399 11128 194545 17.5 | 1.229 % | c | 11387 | 246445 576993 | 109338 11353 205177 18.1 | 1.229 % | c ============================================================================== c [1mFound solution: 35700986[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11451 | 246500 577138 | 82166 11417 206570 18.1 | 1.229 % | c | 11552 | 246500 577138 | 90382 11518 211394 18.4 | 1.230 % | c | 11702 | 246473 577079 | 99420 11667 213352 18.3 | 1.239 % | c | 11928 | 246473 577079 | 109362 11893 217733 18.3 | 1.239 % | c | 12266 | 246228 576531 | 120299 12227 220451 18.0 | 1.313 % | c ============================================================================== c [1mFound solution: 29162936[0m c ---[ 0]---> Sorter-cost: 18 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12282 | 246318 576755 | 82106 12243 220850 18.0 | 1.313 % | c ============================================================================== c [1mFound solution: 28818010[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 12306 | 246341 576816 | 82113 12267 221457 18.1 | 1.313 % | c | 12406 | 246341 576816 | 90324 12367 227128 18.4 | 1.315 % | c | 12556 | 246341 576816 | 99356 12517 240047 19.2 | 1.315 % | c | 12781 | 246341 576816 | 109292 12742 249695 19.6 | 1.315 % | c | 13119 | 246341 576816 | 120221 13080 273178 20.9 | 1.315 % | c | 13625 | 246305 576737 | 132243 13584 291747 21.5 | 1.326 % | c | 14385 | 246305 576737 | 145468 14344 421666 29.4 | 1.326 % | c ============================================================================== c [1mFound solution: 27811840[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14935 | 246168 576442 | 82056 14861 451718 30.4 | 1.326 % | c | 15035 | 246168 576442 | 90261 14961 458151 30.6 | 1.387 % | c | 15185 | 246168 576442 | 99287 15111 473156 31.3 | 1.387 % | c | 15414 | 246168 576442 | 109216 15340 492350 32.1 | 1.387 % | c | 15751 | 246168 576442 | 120138 15677 502654 32.1 | 1.387 % | c | 16259 | 246138 576375 | 132152 16181 514597 31.8 | 1.397 % | c | 17018 | 246138 576375 | 145367 16940 530603 31.3 | 1.397 % | c ============================================================================== c [1mFound solution: 27486201[0m c ---[ 0]---> Sorter-cost: 18 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17219 | 246181 576484 | 82060 17141 574441 33.5 | 1.397 % | c ============================================================================== c [1mFound solution: 26736640[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17237 | 246199 576531 | 82066 17159 580599 33.8 | 1.397 % | c | 17337 | 246199 576531 | 90272 17259 582604 33.8 | 1.398 % | c | 17487 | 246199 576531 | 99299 17409 593424 34.1 | 1.398 % | c | 17712 | 246183 576496 | 109229 17631 634871 36.0 | 1.403 % | c | 18050 | 246183 576496 | 120152 17969 667698 37.2 | 1.403 % | c | 18556 | 246183 576496 | 132168 18475 712989 38.6 | 1.403 % | c | 19315 | 245813 575658 | 145384 19220 766158 39.9 | 1.529 % | c ============================================================================== c [1mFound solution: 25860848[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19568 | 245849 575750 | 81949 19473 776405 39.9 | 1.529 % | c | 19668 | 245849 575750 | 90143 19573 781991 40.0 | 1.530 % | c | 19818 | 245849 575750 | 99158 19723 793227 40.2 | 1.530 % | c | 20044 | 245849 575750 | 109074 19949 816105 40.9 | 1.530 % | c | 20382 | 245755 575540 | 119981 20274 827520 40.8 | 1.559 % | c | 20890 | 245755 575540 | 131979 20782 939777 45.2 | 1.559 % | c | 21651 | 245755 575540 | 145177 21543 986826 45.8 | 1.559 % | c ============================================================================== c [1mFound solution: 25036840[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21707 | 245768 575574 | 81922 21596 987544 45.7 | 1.559 % | c ============================================================================== c [1mFound solution: 24012840[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21712 | 245800 575656 | 81933 21601 988103 45.7 | 1.559 % | c ============================================================================== c [1mFound solution: 22640640[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21744 | 245821 575712 | 81940 21633 989391 45.7 | 1.559 % | c | 21844 | 245821 575712 | 90134 21733 992254 45.7 | 1.566 % | c | 21994 | 245817 575703 | 99147 21882 992899 45.4 | 1.568 % | c | 22219 | 245610 575234 | 109062 22102 1004170 45.4 | 1.636 % | c | 22556 | 245610 575234 | 119968 22439 1034715 46.1 | 1.636 % | c | 23062 | 245610 575234 | 131965 22945 1065473 46.4 | 1.636 % | c | 23821 | 245610 575234 | 145161 23704 1114638 47.0 | 1.636 % | c | 24960 | 245610 575234 | 159677 24843 1137537 45.8 | 1.636 % | c | 26669 | 245610 575234 | 175645 26552 1257092 47.3 | 1.636 % | c | 29232 | 245610 575234 | 193210 29115 1377406 47.3 | 1.636 % | c | 33077 | 245610 575234 | 212531 32960 1607439 48.8 | 1.636 % | c ============================================================================== c [1mFound solution: 21642240[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 3 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 36344 | 245635 575301 | 81878 36227 1831204 50.5 | 1.636 % | c | 36444 | 245635 575301 | 90065 36327 1835433 50.5 | 1.637 % | c | 36594 | 245635 575301 | 99072 36477 1849218 50.7 | 1.637 % | c | 36823 | 245635 575301 | 108979 36706 1861752 50.7 | 1.637 % | c | 37161 | 245635 575301 | 119877 37044 1892278 51.1 | 1.637 % | c | 37667 | 245635 575301 | 131865 37550 1918629 51.1 | 1.637 % | c | 38427 | 245635 575301 | 145051 38310 1970730 51.4 | 1.637 % | c | 39566 | 245635 575301 | 159557 39449 2053390 52.1 | 1.637 % | c | 41275 | 245635 575301 | 175512 41158 2249325 54.7 | 1.637 % | c | 43839 | 245498 574990 | 193064 43717 2344544 53.6 | 1.685 % | c | 47683 | 245451 574885 | 212370 47558 2554400 53.7 | 1.700 % | c | 53449 | 245425 574826 | 233607 53322 2987332 56.0 | 1.708 % | c | 62099 | 245425 574826 | 256968 61972 3566467 57.5 | 1.708 % | c | 75074 | 245318 574589 | 282665 74924 4460326 59.5 | 1.759 % | c c *** TERMINATED *** s SATISFIABLE v -X0_bit_10 -X0_bit_9 -X0_bit_8 -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 X0_bit0 X0_bit1 X0_bit2 X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X0_bit13 -X0_bit14 -X0_bit15 -X0_bit16 -X0_bit17 -X0_bit18 -X0_bit19 -X1_bit_10 -X1_bit_9 -X1_bit_8 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 X1_bit1 X1_bit2 X1_bit3 X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X1_bit13 -X1_bit14 -X1_bit15 -X1_bit16 -X1_bit17 -X1_bit18 -X1_bit19 -X2_bit_10 -X2_bit_9 -X2_bit_8 -X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 -X2_bit1 -X2_bit2 -X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X2_bit13 -X2_bit14 -X2_bit15 -X2_bit16 -X2_bit17 -X2_bit18 -X2_bit19 -X3_bit_10 -X3_bit_9 -X3_bit_8 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X3_bit13 -X3_bit14 -X3_bit15 -X3_bit16 -X3_bit17 -X3_bit18 -X3_bit19 -X4_bit_10 -X4_bit_9 -X4_bit_8 -X4_bit_7 -X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 -X4_bit_1 -X4_bit0 -X4_bit1 -X4_bit2 -X4_bit3 -X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X4_bit13 -X4_bit14 -X4_bit15 -X4_bit16 -X4_bit17 -X4_bit18 -X4_bit19 -X5_bit_10 -X5_bit_9 -X5_bit_8 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X5_bit13 -X5_bit14 -X5_bit15 -X5_bit16 -X5_bit17 -X5_bit18 -X5_bit19 -X6_bit_10 -X6_bit_9 -X6_bit_8 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 -X6_bit2 -X6_bit3 -X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X6_bit13 -X6_bit14 -X6_bit15 -X6_bit16 -X6_bit17 -X6_bit18 -X6_bit19 -X7_bit_10 -X7_bit_9 -X7_bit_8 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 -X7_bit2 -X7_bit3 -X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X7_bit13 -X7_bit14 -X7_bit15 -X7_bit16 -X7_bit17 -X7_bit18 -X7_bit19 -X8_bit_10 -X8_bit_9 -X8_bit_8 -X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 X8_bit0 -X8_bit1 -X8_bit2 X8_bit3 X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X8_bit13 -X8_bit14 -X8_bit15 -X8_bit16 -X8_bit17 -X8_bit18 -X8_bit19 -X9_bit_10 -X9_bit_9 -X9_bit_8 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 X9_bit1 -X9_bit2 X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X9_bit13 -X9_bit14 -X9_bit15 -X9_bit16 -X9_bit17 -X9_bit18 -X9_bit19 -X10_bit_10 -X10_bit_9 -X10_bit_8 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X10_bit13 -X10_bit14 -X10_bit15 -X10_bit16 -X10_bit17 -X10_bit18 -X10_bit19 -X11_bit_10 -X11_bit_9 -X11_bit_8 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 -X11_bit2 -X11_bit3 -X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -X11_bit13 -X11_bit14 -X11_bit15 -X11_bit16 -X11_bit17 -X11_bit18 -X11_bit19 -X12_bit_10 -X12_bit_9 -X12_bit_8 -X12_bit_7 -X12_bit_6 -X12_bit_5 -X12_bit_4 -X12_bit_3 -X12_bit_2 -X12_bit_1 -X12_bit0 -X12_bit1 X12_bit2 -X12_bit3 X12_bit4 -X12_bit5 -X12_bit6 -X12_bit7 -X12_bit8 -X12_bit9 -X12_bit10 -X12_bit11 -X12_bit12 -X12_bit13 -X12_bit14 -X12_bit15 -X12_bit16 -X12_bit17 -X12_bit18 -X12_bit19 -X13_bit_10 -X13_bit_9 -X13_bit_8 -X13_bit_7 -X13_bit_6 -X13_bit_5 -X13_bit_4 -X13_bit_3 -X13_bit_2 -X13_bit_1 -X13_bit0 -X13_bit1 -X13_bit2 -X13_bit3 -X13_bit4 -X13_bit5 -X13_bit6 -X13_bit7 -X13_bi
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/22633/stat): 22633 (minisat+_script) R 22632 22633 5245 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1852013372 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/22633/statm): 174 3 169 147 0 27 0 [pid=22633] 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=22634 New process pid=22635 New process pid=22636 execve syscall for /bin/sed executable One traced child (pid=22635) 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=22636) exited with status: 0 One traced child (pid=22634) exited with status: 0 New process pid=22637 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-gr4x6.opb [startup+10.0038 s] Raw data (loadavg): 0.93 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 7248 0 0 0 943 25 0 0 25 0 1 0 1852013377 32722944 6930 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22637/statm): 7989 6930 145 145 0 7844 0 [pid=22637] vsize: 31956 Current children cumulated CPU time (s) 9.68 Current children cumulated vsize (Kb) 34080 [startup+20.0056 s] Raw data (loadavg): 0.94 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 7344 0 0 0 1940 26 0 0 25 0 1 0 1852013377 33046528 7026 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22637/statm): 8068 7026 145 145 0 7923 0 [pid=22637] vsize: 32272 Current children cumulated CPU time (s) 19.66 Current children cumulated vsize (Kb) 34396 [startup+30.0074 s] Raw data (loadavg): 0.95 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 7577 0 0 0 2937 27 0 0 25 0 1 0 1852013377 34066432 7259 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 8317 7259 145 145 0 8172 0 [pid=22637] vsize: 33268 Current children cumulated CPU time (s) 29.64 Current children cumulated vsize (Kb) 35392 [startup+40.0071 s] Raw data (loadavg): 0.96 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 7652 0 0 0 3937 28 0 0 25 0 1 0 1852013377 34107392 7270 4294967295 134512640 135094434 3221224432 3221221860 134676608 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 8327 7270 145 145 0 8182 0 [pid=22637] vsize: 33308 Current children cumulated CPU time (s) 39.65 Current children cumulated vsize (Kb) 35432 [startup+50.0079 s] Raw data (loadavg): 0.96 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 7706 0 0 0 4937 28 0 0 25 0 1 0 1852013377 34320384 7324 4294967295 134512640 135094434 3221224432 3221221280 134677340 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 8379 7324 145 145 0 8234 0 [pid=22637] vsize: 33516 Current children cumulated CPU time (s) 49.65 Current children cumulated vsize (Kb) 35640 [startup+60.0087 s] Raw data (loadavg): 0.97 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 7718 0 0 0 5937 28 0 0 25 0 1 0 1852013377 34369536 7336 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 8391 7336 145 145 0 8246 0 [pid=22637] vsize: 33564 Current children cumulated CPU time (s) 59.65 Current children cumulated vsize (Kb) 35688 [startup+70.0105 s] Raw data (loadavg): 0.97 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 7917 0 0 0 6935 29 0 0 25 0 1 0 1852013377 34516992 7372 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22637/statm): 8427 7372 145 145 0 8282 0 [pid=22637] vsize: 33708 Current children cumulated CPU time (s) 69.64 Current children cumulated vsize (Kb) 35832 [startup+80.0113 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 8050 0 0 0 7933 30 0 0 25 0 1 0 1852013377 34648064 7406 4294967295 134512640 135094434 3221224432 3221222160 134677271 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22637/statm): 8459 7406 145 145 0 8314 0 [pid=22637] vsize: 33836 Current children cumulated CPU time (s) 79.63 Current children cumulated vsize (Kb) 35960 [startup+90.0121 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 8271 0 0 0 8931 32 0 0 25 0 1 0 1852013377 34959360 7490 4294967295 134512640 135094434 3221224432 3221221440 134600162 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22637/statm): 8535 7490 145 145 0 8390 0 [pid=22637] vsize: 34140 Current children cumulated CPU time (s) 89.63 Current children cumulated vsize (Kb) 36264 [startup+100.013 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 8288 0 0 0 9931 32 0 0 25 0 1 0 1852013377 35020800 7507 4294967295 134512640 135094434 3221224432 3221223060 134557564 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22637/statm): 8550 7507 145 145 0 8405 0 [pid=22637] vsize: 34200 Current children cumulated CPU time (s) 99.63 Current children cumulated vsize (Kb) 36324 [startup+110.015 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 8368 0 0 0 10929 33 0 0 25 0 1 0 1852013377 35356672 7587 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22637/statm): 8632 7587 145 145 0 8487 0 [pid=22637] vsize: 34528 Current children cumulated CPU time (s) 109.62 Current children cumulated vsize (Kb) 36652 [startup+120.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 8539 0 0 0 11928 34 0 0 25 0 1 0 1852013377 35782656 7694 4294967295 134512640 135094434 3221224432 3221221104 134599970 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 8736 7694 145 145 0 8591 0 [pid=22637] vsize: 34944 Current children cumulated CPU time (s) 119.62 Current children cumulated vsize (Kb) 37068 [startup+130.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 8619 0 0 0 12926 35 0 0 25 0 1 0 1852013377 35962880 7738 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 8780 7738 145 145 0 8635 0 [pid=22637] vsize: 35120 Current children cumulated CPU time (s) 129.61 Current children cumulated vsize (Kb) 37244 [startup+140.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 8654 0 0 0 13926 36 0 0 25 0 1 0 1852013377 36167680 7773 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 8830 7773 145 145 0 8685 0 [pid=22637] vsize: 35320 Current children cumulated CPU time (s) 139.62 Current children cumulated vsize (Kb) 37444 [startup+150.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 8808 0 0 0 14925 36 0 0 25 0 1 0 1852013377 36392960 7828 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 8885 7828 145 145 0 8740 0 [pid=22637] vsize: 35540 Current children cumulated CPU time (s) 149.61 Current children cumulated vsize (Kb) 37664 [startup+160.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 8984 0 0 0 15923 38 0 0 25 0 1 0 1852013377 36737024 7907 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 8969 7907 145 145 0 8824 0 [pid=22637] vsize: 35876 Current children cumulated CPU time (s) 159.61 Current children cumulated vsize (Kb) 38000 [startup+170.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 9066 0 0 0 16922 38 0 0 25 0 1 0 1852013377 37044224 7989 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 9044 7989 145 145 0 8899 0 [pid=22637] vsize: 36176 Current children cumulated CPU time (s) 169.6 Current children cumulated vsize (Kb) 38300 [startup+180.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 9214 0 0 0 17921 39 0 0 25 0 1 0 1852013377 37380096 8072 4294967295 134512640 135094434 3221224432 3221221632 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 9126 8072 145 145 0 8981 0 [pid=22637] vsize: 36504 Current children cumulated CPU time (s) 179.6 Current children cumulated vsize (Kb) 38628 [startup+190.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 9292 0 0 0 18919 39 0 0 25 0 1 0 1852013377 37548032 8114 4294967295 134512640 135094434 3221224432 3221223184 134559512 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 9167 8114 145 145 0 9022 0 [pid=22637] vsize: 36668 Current children cumulated CPU time (s) 189.58 Current children cumulated vsize (Kb) 38792 [startup+200.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 9407 0 0 0 19918 40 0 0 25 0 1 0 1852013377 38019072 8229 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 9282 8229 145 145 0 9137 0 [pid=22637] vsize: 37128 Current children cumulated CPU time (s) 199.58 Current children cumulated vsize (Kb) 39252 [startup+210.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 9543 0 0 0 20917 41 0 0 25 0 1 0 1852013377 38305792 8301 4294967295 134512640 135094434 3221224432 3221221808 134600904 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 9352 8301 145 145 0 9207 0 [pid=22637] vsize: 37408 Current children cumulated CPU time (s) 209.58 Current children cumulated vsize (Kb) 39532 [startup+220.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 9734 0 0 0 21916 42 0 0 25 0 1 0 1852013377 38535168 8357 4294967295 134512640 135094434 3221224432 3221221808 134676586 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 9408 8357 145 145 0 9263 0 [pid=22637] vsize: 37632 Current children cumulated CPU time (s) 219.58 Current children cumulated vsize (Kb) 39756 [startup+230.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 9736 0 0 0 22916 42 0 0 25 0 1 0 1852013377 38535168 8359 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 9408 8359 145 145 0 9263 0 [pid=22637] vsize: 37632 Current children cumulated CPU time (s) 229.58 Current children cumulated vsize (Kb) 39756 [startup+240.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 9781 0 0 0 23916 42 0 0 25 0 1 0 1852013377 38715392 8404 4294967295 134512640 135094434 3221224432 3221223056 134557585 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 9452 8404 145 145 0 9307 0 [pid=22637] vsize: 37808 Current children cumulated CPU time (s) 239.58 Current children cumulated vsize (Kb) 39932 [startup+250.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 9818 0 0 0 24916 43 0 0 25 0 1 0 1852013377 38866944 8441 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 9489 8441 145 145 0 9344 0 [pid=22637] vsize: 37956 Current children cumulated CPU time (s) 249.59 Current children cumulated vsize (Kb) 40080 [startup+260.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 9854 0 0 0 25915 43 0 0 25 0 1 0 1852013377 39010304 8477 4294967295 134512640 135094434 3221224432 3221223056 134557619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 9524 8477 145 145 0 9379 0 [pid=22637] vsize: 38096 Current children cumulated CPU time (s) 259.58 Current children cumulated vsize (Kb) 40220 [startup+270.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 9902 0 0 0 26914 43 0 0 25 0 1 0 1852013377 39202816 8525 4294967295 134512640 135094434 3221224432 3221223056 134557604 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 9571 8525 145 145 0 9426 0 [pid=22637] vsize: 38284 Current children cumulated CPU time (s) 269.57 Current children cumulated vsize (Kb) 40408 [startup+280.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 9958 0 0 0 27914 44 0 0 25 0 1 0 1852013377 39428096 8581 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 9626 8581 145 145 0 9481 0 [pid=22637] vsize: 38504 Current children cumulated CPU time (s) 279.58 Current children cumulated vsize (Kb) 40628 [startup+290.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10015 0 0 0 28913 44 0 0 25 0 1 0 1852013377 39661568 8638 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 9683 8638 145 145 0 9538 0 [pid=22637] vsize: 38732 Current children cumulated CPU time (s) 289.57 Current children cumulated vsize (Kb) 40856 [startup+300.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10065 0 0 0 29912 45 0 0 25 0 1 0 1852013377 39862272 8688 4294967295 134512640 135094434 3221224432 3221223056 134557621 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 9732 8688 145 145 0 9587 0 [pid=22637] vsize: 38928 Current children cumulated CPU time (s) 299.57 Current children cumulated vsize (Kb) 41052 [startup+310.032 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10123 0 0 0 30911 45 0 0 25 0 1 0 1852013377 40095744 8746 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 9789 8746 145 145 0 9644 0 [pid=22637] vsize: 39156 Current children cumulated CPU time (s) 309.56 Current children cumulated vsize (Kb) 41280 [startup+320.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10181 0 0 0 31910 46 0 0 25 0 1 0 1852013377 40329216 8804 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 9846 8804 145 145 0 9701 0 [pid=22637] vsize: 39384 Current children cumulated CPU time (s) 319.56 Current children cumulated vsize (Kb) 41508 [startup+330.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10232 0 0 0 32909 47 0 0 25 0 1 0 1852013377 40534016 8855 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 9896 8855 145 145 0 9751 0 [pid=22637] vsize: 39584 Current children cumulated CPU time (s) 329.56 Current children cumulated vsize (Kb) 41708 [startup+340.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10280 0 0 0 33908 47 0 0 25 0 1 0 1852013377 40730624 8903 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 9944 8903 145 145 0 9799 0 [pid=22637] vsize: 39776 Current children cumulated CPU time (s) 339.55 Current children cumulated vsize (Kb) 41900 [startup+350.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10331 0 0 0 34908 47 0 0 25 0 1 0 1852013377 40935424 8954 4294967295 134512640 135094434 3221224432 3221223088 134557792 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 9994 8954 145 145 0 9849 0 [pid=22637] vsize: 39976 Current children cumulated CPU time (s) 349.55 Current children cumulated vsize (Kb) 42100 [startup+360.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10371 0 0 0 35908 48 0 0 25 0 1 0 1852013377 41099264 8994 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 10034 8994 145 145 0 9889 0 [pid=22637] vsize: 40136 Current children cumulated CPU time (s) 359.56 Current children cumulated vsize (Kb) 42260 [startup+370.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10428 0 0 0 36907 48 0 0 25 0 1 0 1852013377 41459712 9051 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 10122 9051 145 145 0 9977 0 [pid=22637] vsize: 40488 Current children cumulated CPU time (s) 369.55 Current children cumulated vsize (Kb) 42612 [startup+380.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10481 0 0 0 37907 48 0 0 25 0 1 0 1852013377 41672704 9104 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 10174 9104 145 145 0 10029 0 [pid=22637] vsize: 40696 Current children cumulated CPU time (s) 379.55 Current children cumulated vsize (Kb) 42820 [startup+390.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10532 0 0 0 38905 49 0 0 25 0 1 0 1852013377 41877504 9155 4294967295 134512640 135094434 3221224432 3221223080 134558037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 10224 9155 145 145 0 10079 0 [pid=22637] vsize: 40896 Current children cumulated CPU time (s) 389.54 Current children cumulated vsize (Kb) 43020 [startup+400.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10587 0 0 0 39904 49 0 0 25 0 1 0 1852013377 42102784 9210 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 10279 9210 145 145 0 10134 0 [pid=22637] vsize: 41116 Current children cumulated CPU time (s) 399.53 Current children cumulated vsize (Kb) 43240 [startup+410.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10635 0 0 0 40904 49 0 0 25 0 1 0 1852013377 42295296 9258 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 10326 9258 145 145 0 10181 0 [pid=22637] vsize: 41304 Current children cumulated CPU time (s) 409.53 Current children cumulated vsize (Kb) 43428 [startup+420.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10777 0 0 0 41902 50 0 0 25 0 1 0 1852013377 42471424 9301 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 10369 9301 145 145 0 10224 0 [pid=22637] vsize: 41476 Current children cumulated CPU time (s) 419.52 Current children cumulated vsize (Kb) 43600 [startup+430.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10847 0 0 0 42902 51 0 0 25 0 1 0 1852013377 42754048 9371 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 10438 9371 145 145 0 10293 0 [pid=22637] vsize: 41752 Current children cumulated CPU time (s) 429.53 Current children cumulated vsize (Kb) 43876 [startup+440.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10905 0 0 0 43901 51 0 0 25 0 1 0 1852013377 42987520 9429 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 10495 9429 145 145 0 10350 0 [pid=22637] vsize: 41980 Current children cumulated CPU time (s) 439.52 Current children cumulated vsize (Kb) 44104 [startup+450.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 10969 0 0 0 44901 51 0 0 25 0 1 0 1852013377 43253760 9493 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 10560 9493 145 145 0 10415 0 [pid=22637] vsize: 42240 Current children cumulated CPU time (s) 449.52 Current children cumulated vsize (Kb) 44364 [startup+460.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11020 0 0 0 45900 52 0 0 25 0 1 0 1852013377 43454464 9544 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 10609 9544 145 145 0 10464 0 [pid=22637] vsize: 42436 Current children cumulated CPU time (s) 459.52 Current children cumulated vsize (Kb) 44560 [startup+470.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11094 0 0 0 46899 52 0 0 25 0 1 0 1852013377 43753472 9618 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 10682 9618 145 145 0 10537 0 [pid=22637] vsize: 42728 Current children cumulated CPU time (s) 469.51 Current children cumulated vsize (Kb) 44852 [startup+480.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11182 0 0 0 47898 53 0 0 25 0 1 0 1852013377 44118016 9706 4294967295 134512640 135094434 3221224432 3221223056 134562076 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 10771 9706 145 145 0 10626 0 [pid=22637] vsize: 43084 Current children cumulated CPU time (s) 479.51 Current children cumulated vsize (Kb) 45208 [startup+490.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11238 0 0 0 48898 53 0 0 25 0 1 0 1852013377 44343296 9762 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 10826 9762 145 145 0 10681 0 [pid=22637] vsize: 43304 Current children cumulated CPU time (s) 489.51 Current children cumulated vsize (Kb) 45428 [startup+500.048 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11295 0 0 0 49897 54 0 0 25 0 1 0 1852013377 44576768 9819 4294967295 134512640 135094434 3221224432 3221223088 134558276 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 10883 9819 145 145 0 10738 0 [pid=22637] vsize: 43532 Current children cumulated CPU time (s) 499.51 Current children cumulated vsize (Kb) 45656 [startup+510.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11345 0 0 0 50897 54 0 0 25 0 1 0 1852013377 44781568 9869 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 10933 9869 145 145 0 10788 0 [pid=22637] vsize: 43732 Current children cumulated CPU time (s) 509.51 Current children cumulated vsize (Kb) 45856 [startup+520.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11384 0 0 0 51896 55 0 0 25 0 1 0 1852013377 44941312 9908 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 10972 9908 145 145 0 10827 0 [pid=22637] vsize: 43888 Current children cumulated CPU time (s) 519.51 Current children cumulated vsize (Kb) 46012 [startup+530.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11435 0 0 0 52895 55 0 0 25 0 1 0 1852013377 45146112 9959 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 11022 9959 145 145 0 10877 0 [pid=22637] vsize: 44088 Current children cumulated CPU time (s) 529.5 Current children cumulated vsize (Kb) 46212 [startup+540.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11522 0 0 0 53893 56 0 0 25 0 1 0 1852013377 45502464 10046 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 11109 10046 145 145 0 10964 0 [pid=22637] vsize: 44436 Current children cumulated CPU time (s) 539.49 Current children cumulated vsize (Kb) 46560 [startup+550.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11584 0 0 0 54892 56 0 0 25 0 1 0 1852013377 45744128 10108 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 11168 10108 145 145 0 11023 0 [pid=22637] vsize: 44672 Current children cumulated CPU time (s) 549.48 Current children cumulated vsize (Kb) 46796 [startup+560.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11639 0 0 0 55892 57 0 0 25 0 1 0 1852013377 45969408 10163 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 11223 10163 145 145 0 11078 0 [pid=22637] vsize: 44892 Current children cumulated CPU time (s) 559.49 Current children cumulated vsize (Kb) 47016 [startup+570.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11676 0 0 0 56892 57 0 0 25 0 1 0 1852013377 46116864 10200 4294967295 134512640 135094434 3221224432 3221223024 134557375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 11259 10200 145 145 0 11114 0 [pid=22637] vsize: 45036 Current children cumulated CPU time (s) 569.49 Current children cumulated vsize (Kb) 47160 [startup+580.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11723 0 0 0 57892 57 0 0 25 0 1 0 1852013377 46309376 10247 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 11306 10247 145 145 0 11161 0 [pid=22637] vsize: 45224 Current children cumulated CPU time (s) 579.49 Current children cumulated vsize (Kb) 47348 [startup+590.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11763 0 0 0 58892 57 0 0 25 0 1 0 1852013377 46469120 10287 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 11345 10287 145 145 0 11200 0 [pid=22637] vsize: 45380 Current children cumulated CPU time (s) 589.49 Current children cumulated vsize (Kb) 47504 [startup+600.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11808 0 0 0 59891 57 0 0 25 0 1 0 1852013377 46653440 10332 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 11390 10332 145 145 0 11245 0 [pid=22637] vsize: 45560 Current children cumulated CPU time (s) 599.48 Current children cumulated vsize (Kb) 47684 [startup+610.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11861 0 0 0 60890 58 0 0 25 0 1 0 1852013377 46866432 10385 4294967295 134512640 135094434 3221224432 3221223056 134557630 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 11442 10385 145 145 0 11297 0 [pid=22637] vsize: 45768 Current children cumulated CPU time (s) 609.48 Current children cumulated vsize (Kb) 47892 [startup+620.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11903 0 0 0 61890 58 0 0 25 0 1 0 1852013377 47038464 10427 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 11484 10427 145 145 0 11339 0 [pid=22637] vsize: 45936 Current children cumulated CPU time (s) 619.48 Current children cumulated vsize (Kb) 48060 [startup+630.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 11951 0 0 0 62890 58 0 0 25 0 1 0 1852013377 47230976 10475 4294967295 134512640 135094434 3221224432 3221223024 134556776 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 11531 10475 145 145 0 11386 0 [pid=22637] vsize: 46124 Current children cumulated CPU time (s) 629.48 Current children cumulated vsize (Kb) 48248 [startup+640.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12000 0 0 0 63889 59 0 0 25 0 1 0 1852013377 47435776 10524 4294967295 134512640 135094434 3221224432 3221223024 134557375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 11581 10524 145 145 0 11436 0 [pid=22637] vsize: 46324 Current children cumulated CPU time (s) 639.48 Current children cumulated vsize (Kb) 48448 [startup+650.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12056 0 0 0 64889 59 0 0 25 0 1 0 1852013377 47656960 10580 4294967295 134512640 135094434 3221224432 3221223024 134557227 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 11635 10580 145 145 0 11490 0 [pid=22637] vsize: 46540 Current children cumulated CPU time (s) 649.48 Current children cumulated vsize (Kb) 48664 [startup+660.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12119 0 0 0 65887 60 0 0 25 0 1 0 1852013377 47910912 10643 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 11697 10643 145 145 0 11552 0 [pid=22637] vsize: 46788 Current children cumulated CPU time (s) 659.47 Current children cumulated vsize (Kb) 48912 [startup+670.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12162 0 0 0 66887 60 0 0 25 0 1 0 1852013377 48087040 10686 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 11740 10686 145 145 0 11595 0 [pid=22637] vsize: 46960 Current children cumulated CPU time (s) 669.47 Current children cumulated vsize (Kb) 49084 [startup+680.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12208 0 0 0 67887 60 0 0 25 0 1 0 1852013377 48271360 10732 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 11785 10732 145 145 0 11640 0 [pid=22637] vsize: 47140 Current children cumulated CPU time (s) 679.47 Current children cumulated vsize (Kb) 49264 [startup+690.066 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12249 0 0 0 68886 61 0 0 25 0 1 0 1852013377 48435200 10773 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 11825 10773 145 145 0 11680 0 [pid=22637] vsize: 47300 Current children cumulated CPU time (s) 689.47 Current children cumulated vsize (Kb) 49424 [startup+700.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12294 0 0 0 69886 61 0 0 25 0 1 0 1852013377 48619520 10818 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 11870 10818 145 145 0 11725 0 [pid=22637] vsize: 47480 Current children cumulated CPU time (s) 699.47 Current children cumulated vsize (Kb) 49604 [startup+710.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12352 0 0 0 70885 62 0 0 25 0 1 0 1852013377 48852992 10876 4294967295 134512640 135094434 3221224432 3221223056 134557627 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 11927 10876 145 145 0 11782 0 [pid=22637] vsize: 47708 Current children cumulated CPU time (s) 709.47 Current children cumulated vsize (Kb) 49832 [startup+720.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12397 0 0 0 71884 62 0 0 25 0 1 0 1852013377 49033216 10921 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 11971 10921 145 145 0 11826 0 [pid=22637] vsize: 47884 Current children cumulated CPU time (s) 719.46 Current children cumulated vsize (Kb) 50008 [startup+730.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12444 0 0 0 72884 62 0 0 25 0 1 0 1852013377 49225728 10968 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 12018 10968 145 145 0 11873 0 [pid=22637] vsize: 48072 Current children cumulated CPU time (s) 729.46 Current children cumulated vsize (Kb) 50196 [startup+740.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12494 0 0 0 73883 63 0 0 25 0 1 0 1852013377 49426432 11018 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 12067 11018 145 145 0 11922 0 [pid=22637] vsize: 48268 Current children cumulated CPU time (s) 739.46 Current children cumulated vsize (Kb) 50392 [startup+750.072 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12541 0 0 0 74883 63 0 0 25 0 1 0 1852013377 49614848 11065 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 12113 11065 145 145 0 11968 0 [pid=22637] vsize: 48452 Current children cumulated CPU time (s) 749.46 Current children cumulated vsize (Kb) 50576 [startup+760.073 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12604 0 0 0 75882 64 0 0 25 0 1 0 1852013377 49872896 11128 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 12176 11128 145 145 0 12031 0 [pid=22637] vsize: 48704 Current children cumulated CPU time (s) 759.46 Current children cumulated vsize (Kb) 50828 [startup+770.075 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12664 0 0 0 76881 64 0 0 25 0 1 0 1852013377 50114560 11188 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 12235 11188 145 145 0 12090 0 [pid=22637] vsize: 48940 Current children cumulated CPU time (s) 769.45 Current children cumulated vsize (Kb) 51064 [startup+780.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12723 0 0 0 77881 65 0 0 25 0 1 0 1852013377 50352128 11247 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 12293 11247 145 145 0 12148 0 [pid=22637] vsize: 49172 Current children cumulated CPU time (s) 779.46 Current children cumulated vsize (Kb) 51296 [startup+790.076 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12786 0 0 0 78880 65 0 0 25 0 1 0 1852013377 50610176 11310 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22637/statm): 12356 11310 145 145 0 12211 0 [pid=22637] vsize: 49424 Current children cumulated CPU time (s) 789.45 Current children cumulated vsize (Kb) 51548 [startup+800.078 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12841 0 0 0 79878 66 0 0 25 0 1 0 1852013377 50839552 11365 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 12412 11365 145 145 0 12267 0 [pid=22637] vsize: 49648 Current children cumulated CPU time (s) 799.44 Current children cumulated vsize (Kb) 51772 [startup+810.079 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12900 0 0 0 80878 67 0 0 25 0 1 0 1852013377 51081216 11424 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22637/statm): 12471 11424 145 145 0 12326 0 [pid=22637] vsize: 49884 Current children cumulated CPU time (s) 809.45 Current children cumulated vsize (Kb) 52008 [startup+820.081 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 12957 0 0 0 81876 68 0 0 25 0 1 0 1852013377 51318784 11481 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22637/statm): 12529 11481 145 145 0 12384 0 [pid=22637] vsize: 50116 Current children cumulated CPU time (s) 819.44 Current children cumulated vsize (Kb) 52240 [startup+830.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13004 0 0 0 82874 69 0 0 25 0 1 0 1852013377 51503104 11528 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22637/statm): 12574 11528 145 145 0 12429 0 [pid=22637] vsize: 50296 Current children cumulated CPU time (s) 829.43 Current children cumulated vsize (Kb) 52420 [startup+840.083 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13060 0 0 0 83873 70 0 0 25 0 1 0 1852013377 51990528 11584 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22637/statm): 12693 11584 145 145 0 12548 0 [pid=22637] vsize: 50772 Current children cumulated CPU time (s) 839.43 Current children cumulated vsize (Kb) 52896 [startup+850.085 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13118 0 0 0 84872 70 0 0 25 0 1 0 1852013377 52224000 11642 4294967295 134512640 135094434 3221224432 3221223024 134556826 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22637/statm): 12750 11642 145 145 0 12605 0 [pid=22637] vsize: 51000 Current children cumulated CPU time (s) 849.42 Current children cumulated vsize (Kb) 53124 [startup+860.086 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13175 0 0 0 85871 71 0 0 25 0 1 0 1852013377 52453376 11699 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22637/statm): 12806 11699 145 145 0 12661 0 [pid=22637] vsize: 51224 Current children cumulated CPU time (s) 859.42 Current children cumulated vsize (Kb) 53348 [startup+870.088 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13227 0 0 0 86869 72 0 0 25 0 1 0 1852013377 52662272 11751 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22637/statm): 12857 11751 145 145 0 12712 0 [pid=22637] vsize: 51428 Current children cumulated CPU time (s) 869.41 Current children cumulated vsize (Kb) 53552 [startup+880.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13287 0 0 0 87868 73 0 0 25 0 1 0 1852013377 52899840 11811 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22637/statm): 12915 11811 145 145 0 12770 0 [pid=22637] vsize: 51660 Current children cumulated CPU time (s) 879.41 Current children cumulated vsize (Kb) 53784 [startup+890.091 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13342 0 0 0 88867 74 0 0 25 0 1 0 1852013377 53121024 11866 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22637/statm): 12969 11866 145 145 0 12824 0 [pid=22637] vsize: 51876 Current children cumulated CPU time (s) 889.41 Current children cumulated vsize (Kb) 54000 [startup+900.092 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13399 0 0 0 89866 74 0 0 25 0 1 0 1852013377 53362688 11923 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22637/statm): 13028 11923 145 145 0 12883 0 [pid=22637] vsize: 52112 Current children cumulated CPU time (s) 899.4 Current children cumulated vsize (Kb) 54236 [startup+910.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13444 0 0 0 90865 75 0 0 25 0 1 0 1852013377 53551104 11968 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22637/statm): 13074 11968 145 145 0 12929 0 [pid=22637] vsize: 52296 Current children cumulated CPU time (s) 909.4 Current children cumulated vsize (Kb) 54420 [startup+920.095 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13492 0 0 0 91864 75 0 0 25 0 1 0 1852013377 53747712 12016 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 13122 12016 145 145 0 12977 0 [pid=22637] vsize: 52488 Current children cumulated CPU time (s) 919.39 Current children cumulated vsize (Kb) 54612 [startup+930.096 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13559 0 0 0 92863 76 0 0 25 0 1 0 1852013377 54050816 12083 4294967295 134512640 135094434 3221224432 3221223088 134557818 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 13196 12083 145 145 0 13051 0 [pid=22637] vsize: 52784 Current children cumulated CPU time (s) 929.39 Current children cumulated vsize (Kb) 54908 [startup+940.096 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13637 0 0 0 93862 77 0 0 25 0 1 0 1852013377 54374400 12161 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 13275 12161 145 145 0 13130 0 [pid=22637] vsize: 53100 Current children cumulated CPU time (s) 939.39 Current children cumulated vsize (Kb) 55224 [startup+950.097 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13713 0 0 0 94861 77 0 0 25 0 1 0 1852013377 54685696 12237 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 13351 12237 145 145 0 13206 0 [pid=22637] vsize: 53404 Current children cumulated CPU time (s) 949.38 Current children cumulated vsize (Kb) 55528 [startup+960.098 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13776 0 0 0 95860 78 0 0 25 0 1 0 1852013377 54939648 12300 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 13413 12300 145 145 0 13268 0 [pid=22637] vsize: 53652 Current children cumulated CPU time (s) 959.38 Current children cumulated vsize (Kb) 55776 [startup+970.099 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13847 0 0 0 96859 78 0 0 25 0 1 0 1852013377 55230464 12371 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22637/statm): 13484 12371 145 145 0 13339 0 [pid=22637] vsize: 53936 Current children cumulated CPU time (s) 969.37 Current children cumulated vsize (Kb) 56060 [startup+980.101 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13910 0 0 0 97858 79 0 0 25 0 1 0 1852013377 55480320 12434 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 13545 12434 145 145 0 13400 0 [pid=22637] vsize: 54180 Current children cumulated CPU time (s) 979.37 Current children cumulated vsize (Kb) 56304 [startup+990.102 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 13969 0 0 0 98857 79 0 0 25 0 1 0 1852013377 55713792 12493 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 13602 12493 145 145 0 13457 0 [pid=22637] vsize: 54408 Current children cumulated CPU time (s) 989.36 Current children cumulated vsize (Kb) 56532 [startup+1000.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14037 0 0 0 99856 80 0 0 25 0 1 0 1852013377 56000512 12561 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 13672 12561 145 145 0 13527 0 [pid=22637] vsize: 54688 Current children cumulated CPU time (s) 999.36 Current children cumulated vsize (Kb) 56812 [startup+1010.1 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14095 0 0 0 100855 80 0 0 25 0 1 0 1852013377 56250368 12619 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 13733 12619 145 145 0 13588 0 [pid=22637] vsize: 54932 Current children cumulated CPU time (s) 1009.35 Current children cumulated vsize (Kb) 57056 [startup+1020.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14142 0 0 0 101855 80 0 0 25 0 1 0 1852013377 56434688 12666 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 13778 12666 145 145 0 13633 0 [pid=22637] vsize: 55112 Current children cumulated CPU time (s) 1019.35 Current children cumulated vsize (Kb) 57236 [startup+1030.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14199 0 0 0 102855 80 0 0 25 0 1 0 1852013377 56668160 12723 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 13835 12723 145 145 0 13690 0 [pid=22637] vsize: 55340 Current children cumulated CPU time (s) 1029.35 Current children cumulated vsize (Kb) 57464 [startup+1040.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14249 0 0 0 103854 81 0 0 25 0 1 0 1852013377 56868864 12773 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/22637/statm): 13884 12773 145 145 0 13739 0 [pid=22637] vsize: 55536 Current children cumulated CPU time (s) 1039.35 Current children cumulated vsize (Kb) 57660 [startup+1050.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14287 0 0 0 104853 81 0 0 25 0 1 0 1852013377 57020416 12811 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 13921 12811 145 145 0 13776 0 [pid=22637] vsize: 55684 Current children cumulated CPU time (s) 1049.34 Current children cumulated vsize (Kb) 57808 [startup+1060.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14332 0 0 0 105853 82 0 0 25 0 1 0 1852013377 57200640 12856 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 13965 12856 145 145 0 13820 0 [pid=22637] vsize: 55860 Current children cumulated CPU time (s) 1059.35 Current children cumulated vsize (Kb) 57984 [startup+1070.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14388 0 0 0 106852 82 0 0 25 0 1 0 1852013377 57438208 12912 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 14023 12912 145 145 0 13878 0 [pid=22637] vsize: 56092 Current children cumulated CPU time (s) 1069.34 Current children cumulated vsize (Kb) 58216 [startup+1080.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14433 0 0 0 107851 83 0 0 25 0 1 0 1852013377 57610240 12957 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 14065 12957 145 145 0 13920 0 [pid=22637] vsize: 56260 Current children cumulated CPU time (s) 1079.34 Current children cumulated vsize (Kb) 58384 [startup+1090.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14493 0 0 0 108851 83 0 0 25 0 1 0 1852013377 57876480 13017 4294967295 134512640 135094434 3221224432 3221223088 134558276 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 14130 13017 145 145 0 13985 0 [pid=22637] vsize: 56520 Current children cumulated CPU time (s) 1089.34 Current children cumulated vsize (Kb) 58644 [startup+1100.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14563 0 0 0 109850 83 0 0 25 0 1 0 1852013377 58183680 13087 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 14205 13087 145 145 0 14060 0 [pid=22637] vsize: 56820 Current children cumulated CPU time (s) 1099.33 Current children cumulated vsize (Kb) 58944 [startup+1110.11 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14616 0 0 0 110849 84 0 0 25 0 1 0 1852013377 58396672 13140 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 14257 13140 145 145 0 14112 0 [pid=22637] vsize: 57028 Current children cumulated CPU time (s) 1109.33 Current children cumulated vsize (Kb) 59152 [startup+1120.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14669 0 0 0 111849 84 0 0 25 0 1 0 1852013377 58621952 13193 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 14312 13193 145 145 0 14167 0 [pid=22637] vsize: 57248 Current children cumulated CPU time (s) 1119.33 Current children cumulated vsize (Kb) 59372 [startup+1130.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14738 0 0 0 112849 85 0 0 25 0 1 0 1852013377 58896384 13262 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 14379 13262 145 145 0 14234 0 [pid=22637] vsize: 57516 Current children cumulated CPU time (s) 1129.34 Current children cumulated vsize (Kb) 59640 [startup+1140.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14792 0 0 0 113848 85 0 0 25 0 1 0 1852013377 59129856 13316 4294967295 134512640 135094434 3221224432 3221223088 134558411 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 14436 13316 145 145 0 14291 0 [pid=22637] vsize: 57744 Current children cumulated CPU time (s) 1139.33 Current children cumulated vsize (Kb) 59868 [startup+1150.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14850 0 0 0 114848 85 0 0 25 0 1 0 1852013377 59359232 13374 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 14492 13374 145 145 0 14347 0 [pid=22637] vsize: 57968 Current children cumulated CPU time (s) 1149.33 Current children cumulated vsize (Kb) 60092 [startup+1160.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14890 0 0 0 115848 85 0 0 25 0 1 0 1852013377 59527168 13414 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 14533 13414 145 145 0 14388 0 [pid=22637] vsize: 58132 Current children cumulated CPU time (s) 1159.33 Current children cumulated vsize (Kb) 60256 [startup+1170.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14941 0 0 0 116847 86 0 0 25 0 1 0 1852013377 59744256 13465 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 14586 13465 145 145 0 14441 0 [pid=22637] vsize: 58344 Current children cumulated CPU time (s) 1169.33 Current children cumulated vsize (Kb) 60468 [startup+1180.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 14989 0 0 0 117847 86 0 0 25 0 1 0 1852013377 59932672 13513 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 14632 13513 145 145 0 14487 0 [pid=22637] vsize: 58528 Current children cumulated CPU time (s) 1179.33 Current children cumulated vsize (Kb) 60652 [startup+1190.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 15039 0 0 0 118846 87 0 0 25 0 1 0 1852013377 60133376 13563 4294967295 134512640 135094434 3221224432 3221223056 134557606 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 14681 13563 145 145 0 14536 0 [pid=22637] vsize: 58724 Current children cumulated CPU time (s) 1189.33 Current children cumulated vsize (Kb) 60848 [startup+1200.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 15097 0 0 0 119845 88 0 0 25 0 1 0 1852013377 60387328 13621 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 14743 13621 145 145 0 14598 0 [pid=22637] vsize: 58972 Current children cumulated CPU time (s) 1199.33 Current children cumulated vsize (Kb) 61096 [startup+1210.12 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 15157 0 0 0 120845 88 0 0 25 0 1 0 1852013377 60637184 13681 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 14804 13681 145 145 0 14659 0 [pid=22637] vsize: 59216 Current children cumulated CPU time (s) 1209.33 Current children cumulated vsize (Kb) 61340 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.13 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 22637 Raw data (/proc/22633/stat): 22633 (minisat+_script) S 22632 22633 5245 0 -1 0 289 239 0 0 0 0 0 0 18 0 1 0 1852013372 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/22633/statm): 531 226 485 147 0 384 0 [pid=22633] vsize: 2124 Raw data (/proc/22637/stat): 22637 (minisat+_64-bit) R 22633 22633 5245 0 -1 0 15157 0 0 0 120845 88 0 0 25 0 1 0 1852013377 60637184 13681 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/22637/statm): 14804 13681 145 145 0 14659 0 [pid=22637] vsize: 59216 Current children cumulated CPU time (s) 1209.33 Current children cumulated vsize (Kb) 61340 Sending SIGTERM to -22633 Sleeping 2 seconds One traced child (pid=22633) ended because it received signal 15 (SIGTERM) One traced child (pid=22637) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.16 CPU time (s): 1209.37 CPU user time (s): 1208.46 CPU system time (s): 0.906862 CPU usage (%): 99.9344 Max. virtual memory (cumulated for all children) (Kb): 61340
ERROR: no interpretation found !