Name | mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-markshare2_1.opb |
MD5SUM | a84a96a9314212f3d8ecd5227c500cef |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 63179 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 210 |
Biggest coefficient in the objective function | 536870912 |
Number of bits for the biggest coefficient in the objective function | 30 |
Sum of the numbers in the objective function | 7516192761 |
Number of bits of the sum of numbers in the objective function | 33 |
Biggest number in a constraint | 536870912 |
Number of bits of the biggest number in a constraint | 30 |
Biggest sum of numbers in a constraint | 7516192761 |
Number of bits of the biggest sum of numbers | 33 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.03 |
Number of variables | 330 |
Total number of constraints | 67 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 54 |
Number of constraints which are nor clauses,nor cardinality constraints | 13 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 150 |
LAUNCH ON wulflinc5 THE 2005-09-20 01:28:09 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3059 boxname=wulflinc5 idbench=715 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: a84a96a9314212f3d8ecd5227c500cef /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-markshare2_1.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-markshare2_1.opb IDLAUNCH: 3059 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 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 : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 903096 kB Buffers: 20376 kB Cached: 86596 kB SwapCached: 740 kB Active: 30320 kB Inactive: 79364 kB HighTotal: 131008 kB HighFree: 42644 kB LowTotal: 903652 kB LowFree: 860452 kB SwapTotal: 2097136 kB SwapFree: 2095892 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5804 kB Slab: 16112 kB Committed_AS: 64300 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 01:48:19 (client local time) WITH STATUS 10 IN 1209.27 SECONDS stats: 3059 7 1209.27 10
c Parsing PB file... c Converting 20 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ####### c -- Clauses(.)/Splits(s): (none) c ---[ 19]---> BDD-cost: 10 c ---[ 18]---> BDD-cost: 10 c ---[ 17]---> BDD-cost: 10 c ---[ 16]---> BDD-cost: 10 c ---[ 15]---> BDD-cost: 10 c ---[ 14]---> BDD-cost: 10 c ---[ 12]---> Adder-cost: 708 maxlim: 3756758 bits: 23/22 c ---[ 10]---> Adder-cost: 758 maxlim: 4064912 bits: 23/22 c ---[ 8]---> Adder-cost: 714 maxlim: 3859164 bits: 23/22 c ---[ 6]---> Adder-cost: 676 maxlim: 4153021 bits: 23/22 c ---[ 4]---> Adder-cost: 812 maxlim: 3812158 bits: 23/22 c ---[ 2]---> Adder-cost: 766 maxlim: 4131466 bits: 23/22 c ---[ 0]---> Adder-cost: 692 maxlim: 3780388 bits: 23/22 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 34933 124179 | 11644 0 0 nan | 0.000 % | c | 100 | 34933 124179 | 12808 100 416 4.2 | 6.830 % | c | 250 | 34933 124179 | 14089 250 1526 6.1 | 6.830 % | c | 475 | 34933 124179 | 15498 475 3526 7.4 | 6.830 % | c ============================================================================== c [1mFound solution: 8658716[0m c ---[ 0]---> Sorter-cost: 2158 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 805 | 40455 137066 | 13485 804 7989 9.9 | 6.830 % | c ============================================================================== c [1mFound solution: 5260062[0m c ---[ 0]---> Sorter-cost: 19 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 835 | 40500 137210 | 13500 834 8278 9.9 | 6.830 % | c | 935 | 40492 137184 | 14850 933 9140 9.8 | 5.136 % | c | 1085 | 40460 137080 | 16335 1079 10291 9.5 | 5.189 % | c | 1310 | 40460 137080 | 17968 1304 11927 9.1 | 5.189 % | c | 1647 | 40460 137080 | 19765 1641 13700 8.3 | 5.189 % | c | 2154 | 40436 137002 | 21741 2145 20816 9.7 | 5.228 % | c | 2914 | 40428 136976 | 23916 2904 37504 12.9 | 5.242 % | c | 4054 | 40428 136976 | 26307 4044 60613 15.0 | 5.242 % | c ============================================================================== c [1mFound solution: 4950048[0m c ---[ 0]---> Sorter-cost: 20 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4373 | 40449 137020 | 13483 4356 90869 20.9 | 5.242 % | c | 4473 | 40449 137020 | 14831 4456 93625 21.0 | 5.271 % | c | 4623 | 40449 137020 | 16314 4606 94532 20.5 | 5.271 % | c | 4848 | 40449 137020 | 17945 4831 97424 20.2 | 5.271 % | c | 5186 | 40449 137020 | 19740 5169 101715 19.7 | 5.271 % | c | 5693 | 40449 137020 | 21714 5676 114014 20.1 | 5.271 % | c | 6452 | 40449 137020 | 23885 6435 142255 22.1 | 5.271 % | c ============================================================================== c [1mFound solution: 4620607[0m c ---[ 0]---> Sorter-cost: 21 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6683 | 40491 137120 | 13497 6666 159247 23.9 | 5.271 % | c | 6783 | 40483 137094 | 14846 6765 160692 23.8 | 5.282 % | c | 6933 | 40483 137094 | 16331 6915 164982 23.9 | 5.282 % | c | 7158 | 40483 137094 | 17964 7140 169116 23.7 | 5.282 % | c | 7495 | 40483 137094 | 19760 7477 174450 23.3 | 5.282 % | c | 8004 | 40467 137042 | 21737 7984 180282 22.6 | 5.308 % | c | 8763 | 40461 137024 | 23910 8742 191914 22.0 | 5.321 % | c | 9902 | 40453 136998 | 26301 9880 257083 26.0 | 5.335 % | c | 11611 | 40453 136998 | 28932 11589 499552 43.1 | 5.335 % | c ============================================================================== c [1mFound solution: 4249759[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11737 | 40475 137049 | 13491 11715 502214 42.9 | 5.335 % | c | 11837 | 40475 137049 | 14840 11815 507717 43.0 | 5.341 % | c | 11987 | 40475 137049 | 16324 11965 515534 43.1 | 5.341 % | c | 12212 | 40475 137049 | 17956 12190 524302 43.0 | 5.341 % | c | 12550 | 40475 137049 | 19752 12528 540452 43.1 | 5.341 % | c | 13056 | 40467 137023 | 21727 13033 550988 42.3 | 5.354 % | c | 13815 | 40467 137023 | 23900 13792 578807 42.0 | 5.354 % | c | 14955 | 40467 137023 | 26290 14932 644252 43.1 | 5.354 % | c ============================================================================== c [1mFound solution: 3339853[0m c ---[ 0]---> Sorter-cost: 21 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15826 | 40493 137087 | 13497 15803 672645 42.6 | 5.354 % | c | 15926 | 40493 137087 | 14846 8002 416550 52.1 | 5.356 % | c | 16076 | 40493 137087 | 16331 8152 422105 51.8 | 5.356 % | c | 16301 | 40493 137087 | 17964 8377 437923 52.3 | 5.356 % | c | 16638 | 40493 137087 | 19760 8714 445487 51.1 | 5.356 % | c | 17144 | 40493 137087 | 21737 9220 455219 49.4 | 5.356 % | c ============================================================================== c [1mFound solution: 3334229[0m c ---[ 0]---> Sorter-cost: 19 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17762 | 40515 137139 | 13505 9838 522989 53.2 | 5.356 % | c | 17863 | 40515 137139 | 14855 9939 525768 52.9 | 5.363 % | c | 18013 | 40515 137139 | 16341 10089 527063 52.2 | 5.363 % | c | 18241 | 40515 137139 | 17975 10317 529533 51.3 | 5.363 % | c | 18578 | 40515 137139 | 19772 10654 536878 50.4 | 5.363 % | c ============================================================================== c [1mFound solution: 3287413[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19079 | 40536 137188 | 13512 11155 547166 49.1 | 5.363 % | c | 19180 | 40536 137188 | 14863 11256 550369 48.9 | 5.368 % | c | 19330 | 40536 137188 | 16349 11406 553026 48.5 | 5.368 % | c | 19555 | 40536 137188 | 17984 11631 558823 48.0 | 5.368 % | c | 19893 | 40536 137188 | 19782 11969 572765 47.9 | 5.368 % | c | 20399 | 40528 137162 | 21761 12474 580989 46.6 | 5.381 % | c | 21158 | 40522 137149 | 23937 13228 596004 45.1 | 5.407 % | c ============================================================================== c [1mFound solution: 2290547[0m c ---[ 0]---> Sorter-cost: 20 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 21322 | 40544 137206 | 13514 13392 600636 44.9 | 5.407 % | c | 21422 | 40544 137206 | 14865 13492 604346 44.8 | 5.412 % | c | 21573 | 40544 137206 | 16351 13643 607938 44.6 | 5.412 % | c | 21798 | 40544 137206 | 17987 13868 614171 44.3 | 5.412 % | c | 22135 | 40544 137206 | 19785 14205 624729 44.0 | 5.412 % | c | 22644 | 40544 137206 | 21764 14714 638820 43.4 | 5.412 % | c | 23404 | 40544 137206 | 23940 15474 661163 42.7 | 5.412 % | c | 24543 | 40544 137206 | 26334 16613 721090 43.4 | 5.412 % | c | 26252 | 40544 137206 | 28968 18322 789853 43.1 | 5.412 % | c | 28815 | 40544 137206 | 31865 20885 905885 43.4 | 5.412 % | c | 32661 | 40535 137179 | 35051 24730 1011947 40.9 | 5.438 % | c | 38427 | 40535 137179 | 38557 30496 1345865 44.1 | 5.438 % | c ============================================================================== c [1mFound solution: 1436307[0m c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 45811 | 40559 137239 | 13519 37880 1653565 43.7 | 5.438 % | c | 45912 | 40559 137239 | 14870 7144 239022 33.5 | 5.440 % | c | 46063 | 40559 137239 | 16357 7295 247734 34.0 | 5.440 % | c | 46288 | 40559 137239 | 17993 7520 249720 33.2 | 5.440 % | c | 46627 | 40559 137239 | 19793 7859 253146 32.2 | 5.440 % | c | 47134 | 40559 137239 | 21772 8366 269347 32.2 | 5.440 % | c | 47893 | 40559 137239 | 23949 9125 361442 39.6 | 5.440 % | c | 49032 | 40559 137239 | 26344 10264 396132 38.6 | 5.440 % | c | 50741 | 40559 137239 | 28979 11973 437100 36.5 | 5.440 % | c | 53303 | 40559 137239 | 31877 14535 538464 37.0 | 5.440 % | c ============================================================================== c [1mFound solution: 1226125[0m c ---[ 0]---> Sorter-cost: 16 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 53727 | 40579 137287 | 13526 14959 548574 36.7 | 5.440 % | c | 53828 | 40579 137287 | 14878 7581 202510 26.7 | 5.445 % | c | 53978 | 40579 137287 | 16366 7731 204888 26.5 | 5.445 % | c | 54204 | 40579 137287 | 18003 7957 208315 26.2 | 5.445 % | c | 54542 | 40579 137287 | 19803 8295 216444 26.1 | 5.445 % | c | 55048 | 40579 137287 | 21783 8801 224770 25.5 | 5.445 % | c | 55809 | 40579 137287 | 23962 9562 252224 26.4 | 5.445 % | c | 56950 | 40579 137287 | 26358 10703 296178 27.7 | 5.445 % | c | 58660 | 40573 137269 | 28994 12412 374420 30.2 | 5.458 % | c | 61223 | 40573 137269 | 31893 14975 496937 33.2 | 5.458 % | c | 65067 | 40573 137269 | 35082 18819 695359 36.9 | 5.458 % | c | 70834 | 40573 137269 | 38591 24586 924178 37.6 | 5.458 % | c | 79483 | 40547 137211 | 42450 33229 1386072 41.7 | 5.549 % | c | 92457 | 40547 137211 | 46695 16206 718044 44.3 | 5.549 % | c | 111919 | 40547 137211 | 51364 35668 1877866 52.6 | 5.549 % | c | 141112 | 40547 137211 | 56501 26554 1476960 55.6 | 5.549 % | c | 184902 | 40547 137211 | 62151 25536 2450937 96.0 | 5.549 % | c | 250586 | 40535 137180 | 68366 43565 2228582 51.2 | 5.588 % | c | 349114 | 40535 137180 | 75203 35537 2570698 72.3 | 5.588 % | c | 496904 | 40535 137180 | 82723 63098 3631157 57.5 | 5.588 % | c ============================================================================== c [1mFound solution: 937675[0m c ---[ 0]---> Sorter-cost: 18 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 611637 | 40477 136981 | 13492 41360 3147226 76.1 | 5.588 % | c | 611737 | 40477 136981 | 14841 7432 636521 85.6 | 5.761 % | c | 611887 | 40477 136981 | 16325 7582 639768 84.4 | 5.761 % | c | 612112 | 40477 136981 | 17957 7807 641772 82.2 | 5.761 % | c | 612449 | 40477 136981 | 19753 8144 651973 80.1 | 5.761 % | c | 612956 | 40477 136981 | 21729 8651 667626 77.2 | 5.761 % | c | 613717 | 40477 136981 | 23901 9412 691168 73.4 | 5.761 % | c | 614857 | 40477 136981 | 26292 10552 723865 68.6 | 5.761 % | c | 616566 | 40477 136981 | 28921 12261 788603 64.3 | 5.761 % | c | 619128 | 40472 136970 | 31813 14822 938756 63.3 | 5.787 % | c | 622973 | 40472 136970 | 34994 18667 1092890 58.5 | 5.787 % | c | 628739 | 40472 136970 | 38494 24433 1322315 54.1 | 5.787 % | c | 637388 | 40448 136917 | 42343 33079 1753094 53.0 | 5.892 % | c | 650363 | 40404 136818 | 46578 17084 937926 54.9 | 6.061 % | c | 669828 | 40396 136796 | 51235 36548 1867018 51.1 | 6.087 % | c | 699020 | 40396 136796 | 56359 27623 1424195 51.6 | 6.087 % | c | 742811 | 40396 136796 | 61995 27073 1822699 67.3 | 6.087 % | c ============================================================================== c [1mFound solution: 681120[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 749104 | 40314 136607 | 13438 33351 2060389 61.8 | 6.087 % | c | 749204 | 40314 136607 | 14781 7777 221057 28.4 | 6.533 % | c | 749355 | 40314 136607 | 16259 7928 223104 28.1 | 6.533 % | c | 749580 | 40314 136607 | 17885 8153 227139 27.9 | 6.533 % | c | 749918 | 40314 136607 | 19674 8491 236519 27.9 | 6.533 % | c | 750424 | 40314 136607 | 21642 8997 248399 27.6 | 6.533 % | c | 751183 | 40314 136607 | 23806 9756 265928 27.3 | 6.533 % | c | 752322 | 40314 136607 | 26186 10895 306954 28.2 | 6.533 % | c | 754030 | 40314 136607 | 28805 12603 375521 29.8 | 6.533 % | c | 756592 | 40314 136607 | 31686 15165 477461 31.5 | 6.533 % | c | 760437 | 40314 136607 | 34854 19010 626240 32.9 | 6.533 % | c | 766203 | 40314 136607 | 38340 24776 878769 35.5 | 6.533 % | c | 774852 | 40314 136607 | 42174 33425 1385351 41.4 | 6.533 % |
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/24008/stat): 24008 (minisat+_script) R 24007 24008 824 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1796353810 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/24008/statm): 174 3 169 147 0 27 0 [pid=24008] 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=24009 New process pid=24010 New process pid=24011 execve syscall for /bin/sed executable open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 One traced child (pid=24010) exited with status: 0 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=24011) exited with status: 0 One traced child (pid=24009) exited with status: 0 New process pid=24012 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-markshare2_1.opb [startup+10.005 s] Raw data (loadavg): 0.93 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 1576 0 0 0 981 5 0 0 25 0 1 0 1796353815 6766592 1529 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 1652 1529 145 145 0 1507 0 [pid=24012] vsize: 6608 Current children cumulated CPU time (s) 9.88 Current children cumulated vsize (Kb) 8732 [startup+20.0058 s] Raw data (loadavg): 0.94 0.98 0.98 1/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) T 24008 24008 824 0 -1 0 1925 0 0 0 1976 7 0 0 25 0 1 0 1796353815 8179712 1878 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/24012/statm): 1997 1878 145 145 0 1852 0 [pid=24012] vsize: 7988 Current children cumulated CPU time (s) 19.85 Current children cumulated vsize (Kb) 10112 [startup+30.0065 s] Raw data (loadavg): 0.95 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 2722 0 0 0 2961 13 0 0 25 0 1 0 1796353815 11448320 2675 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24012/statm): 2795 2675 145 145 0 2650 0 [pid=24012] vsize: 11180 Current children cumulated CPU time (s) 29.76 Current children cumulated vsize (Kb) 13304 [startup+40.0072 s] Raw data (loadavg): 0.96 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 3098 0 0 0 3954 15 0 0 25 0 1 0 1796353815 13094912 3051 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 3197 3051 145 145 0 3052 0 [pid=24012] vsize: 12788 Current children cumulated CPU time (s) 39.71 Current children cumulated vsize (Kb) 14912 [startup+50.008 s] Raw data (loadavg): 0.96 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 3098 0 0 0 4954 15 0 0 25 0 1 0 1796353815 13094912 3051 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 3197 3051 145 145 0 3052 0 [pid=24012] vsize: 12788 Current children cumulated CPU time (s) 49.71 Current children cumulated vsize (Kb) 14912 [startup+60.0087 s] Raw data (loadavg): 0.97 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 3098 0 0 0 5955 15 0 0 25 0 1 0 1796353815 13094912 3051 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24012/statm): 3197 3051 145 145 0 3052 0 [pid=24012] vsize: 12788 Current children cumulated CPU time (s) 59.72 Current children cumulated vsize (Kb) 14912 [startup+70.0095 s] Raw data (loadavg): 0.97 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 3514 0 0 0 6945 18 0 0 25 0 1 0 1796353815 14774272 3467 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 3607 3467 145 145 0 3462 0 [pid=24012] vsize: 14428 Current children cumulated CPU time (s) 69.65 Current children cumulated vsize (Kb) 16552 [startup+80.0102 s] Raw data (loadavg): 0.98 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 3566 0 0 0 7944 19 0 0 25 0 1 0 1796353815 14987264 3519 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 3659 3519 145 145 0 3514 0 [pid=24012] vsize: 14636 Current children cumulated CPU time (s) 79.65 Current children cumulated vsize (Kb) 16760 [startup+90.0109 s] Raw data (loadavg): 0.98 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 3566 0 0 0 8945 19 0 0 25 0 1 0 1796353815 14987264 3519 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 3659 3519 145 145 0 3514 0 [pid=24012] vsize: 14636 Current children cumulated CPU time (s) 89.66 Current children cumulated vsize (Kb) 16760 [startup+100.012 s] Raw data (loadavg): 0.98 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 3821 0 0 0 9941 20 0 0 25 0 1 0 1796353815 16035840 3774 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 3915 3774 145 145 0 3770 0 [pid=24012] vsize: 15660 Current children cumulated CPU time (s) 99.63 Current children cumulated vsize (Kb) 17784 [startup+110.012 s] Raw data (loadavg): 0.98 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 4170 0 0 0 10935 23 0 0 25 0 1 0 1796353815 17461248 4123 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 4263 4123 145 145 0 4118 0 [pid=24012] vsize: 17052 Current children cumulated CPU time (s) 109.6 Current children cumulated vsize (Kb) 19176 [startup+120.013 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 4581 0 0 0 11928 25 0 0 25 0 1 0 1796353815 19132416 4534 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 4671 4534 145 145 0 4526 0 [pid=24012] vsize: 18684 Current children cumulated CPU time (s) 119.55 Current children cumulated vsize (Kb) 20808 [startup+130.013 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 4663 0 0 0 12927 26 0 0 25 0 1 0 1796353815 19460096 4616 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 4751 4616 145 145 0 4606 0 [pid=24012] vsize: 19004 Current children cumulated CPU time (s) 129.55 Current children cumulated vsize (Kb) 21128 [startup+140.014 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 4663 0 0 0 13927 26 0 0 25 0 1 0 1796353815 19460096 4616 4294967295 134512640 135094434 3221224432 3221223024 134557375 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 4751 4616 145 145 0 4606 0 [pid=24012] vsize: 19004 Current children cumulated CPU time (s) 139.55 Current children cumulated vsize (Kb) 21128 [startup+150.014 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 4663 0 0 0 14927 26 0 0 25 0 1 0 1796353815 19460096 4616 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 4751 4616 145 145 0 4606 0 [pid=24012] vsize: 19004 Current children cumulated CPU time (s) 149.55 Current children cumulated vsize (Kb) 21128 [startup+160.015 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 4663 0 0 0 15927 26 0 0 25 0 1 0 1796353815 19460096 4616 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 4751 4616 145 145 0 4606 0 [pid=24012] vsize: 19004 Current children cumulated CPU time (s) 159.55 Current children cumulated vsize (Kb) 21128 [startup+170.016 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 5076 0 0 0 16921 29 0 0 25 0 1 0 1796353815 21151744 5029 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 5164 5029 145 145 0 5019 0 [pid=24012] vsize: 20656 Current children cumulated CPU time (s) 169.52 Current children cumulated vsize (Kb) 22780 [startup+180.017 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 5534 0 0 0 17912 33 0 0 25 0 1 0 1796353815 23003136 5487 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 5616 5487 145 145 0 5471 0 [pid=24012] vsize: 22464 Current children cumulated CPU time (s) 179.47 Current children cumulated vsize (Kb) 24588 [startup+190.017 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 5676 0 0 0 18909 34 0 0 25 0 1 0 1796353815 23580672 5629 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 5757 5629 145 145 0 5612 0 [pid=24012] vsize: 23028 Current children cumulated CPU time (s) 189.45 Current children cumulated vsize (Kb) 25152 [startup+200.018 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 5676 0 0 0 19910 34 0 0 25 0 1 0 1796353815 23580672 5629 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 5757 5629 145 145 0 5612 0 [pid=24012] vsize: 23028 Current children cumulated CPU time (s) 199.46 Current children cumulated vsize (Kb) 25152 [startup+210.019 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 5676 0 0 0 20910 34 0 0 25 0 1 0 1796353815 23580672 5629 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 5757 5629 145 145 0 5612 0 [pid=24012] vsize: 23028 Current children cumulated CPU time (s) 209.46 Current children cumulated vsize (Kb) 25152 [startup+220.02 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 5676 0 0 0 21910 34 0 0 25 0 1 0 1796353815 23580672 5629 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 5757 5629 145 145 0 5612 0 [pid=24012] vsize: 23028 Current children cumulated CPU time (s) 219.46 Current children cumulated vsize (Kb) 25152 [startup+230.019 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 6013 0 0 0 22904 36 0 0 25 0 1 0 1796353815 24961024 5966 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 6094 5966 145 145 0 5949 0 [pid=24012] vsize: 24376 Current children cumulated CPU time (s) 229.42 Current children cumulated vsize (Kb) 26500 [startup+240.02 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 6501 0 0 0 23896 40 0 0 25 0 1 0 1796353815 26959872 6454 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 6582 6454 145 145 0 6437 0 [pid=24012] vsize: 26328 Current children cumulated CPU time (s) 239.38 Current children cumulated vsize (Kb) 28452 [startup+250.021 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7066 0 0 0 24886 44 0 0 25 0 1 0 1796353815 29270016 7019 4294967295 134512640 135094434 3221224432 3221223088 134558147 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 7146 7019 145 145 0 7001 0 [pid=24012] vsize: 28584 Current children cumulated CPU time (s) 249.32 Current children cumulated vsize (Kb) 30708 [startup+260.022 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7066 0 0 0 25886 44 0 0 25 0 1 0 1796353815 29270016 7019 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 7146 7019 145 145 0 7001 0 [pid=24012] vsize: 28584 Current children cumulated CPU time (s) 259.32 Current children cumulated vsize (Kb) 30708 [startup+270.022 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7066 0 0 0 26886 44 0 0 25 0 1 0 1796353815 29270016 7019 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 7146 7019 145 145 0 7001 0 [pid=24012] vsize: 28584 Current children cumulated CPU time (s) 269.32 Current children cumulated vsize (Kb) 30708 [startup+280.023 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7066 0 0 0 27887 44 0 0 25 0 1 0 1796353815 29270016 7019 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 7146 7019 145 145 0 7001 0 [pid=24012] vsize: 28584 Current children cumulated CPU time (s) 279.33 Current children cumulated vsize (Kb) 30708 [startup+290.025 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7066 0 0 0 28887 44 0 0 25 0 1 0 1796353815 29270016 7019 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 7146 7019 145 145 0 7001 0 [pid=24012] vsize: 28584 Current children cumulated CPU time (s) 289.33 Current children cumulated vsize (Kb) 30708 [startup+300.025 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7066 0 0 0 29887 44 0 0 25 0 1 0 1796353815 29270016 7019 4294967295 134512640 135094434 3221224432 3221223104 134555544 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 7146 7019 145 145 0 7001 0 [pid=24012] vsize: 28584 Current children cumulated CPU time (s) 299.33 Current children cumulated vsize (Kb) 30708 [startup+310.026 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7069 0 0 0 30888 44 0 0 25 0 1 0 1796353815 29532160 7022 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 7210 7022 145 145 0 7065 0 [pid=24012] vsize: 28840 Current children cumulated CPU time (s) 309.34 Current children cumulated vsize (Kb) 30964 [startup+320.027 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7073 0 0 0 31888 44 0 0 25 0 1 0 1796353815 29532160 7026 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 7210 7026 145 145 0 7065 0 [pid=24012] vsize: 28840 Current children cumulated CPU time (s) 319.34 Current children cumulated vsize (Kb) 30964 [startup+330.028 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7073 0 0 0 32888 44 0 0 25 0 1 0 1796353815 29532160 7026 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 7210 7026 145 145 0 7065 0 [pid=24012] vsize: 28840 Current children cumulated CPU time (s) 329.34 Current children cumulated vsize (Kb) 30964 [startup+340.028 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7073 0 0 0 33888 44 0 0 25 0 1 0 1796353815 29532160 7026 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 7210 7026 145 145 0 7065 0 [pid=24012] vsize: 28840 Current children cumulated CPU time (s) 339.34 Current children cumulated vsize (Kb) 30964 [startup+350.029 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7073 0 0 0 34888 44 0 0 25 0 1 0 1796353815 29532160 7026 4294967295 134512640 135094434 3221224432 3221223104 134556257 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 7210 7026 145 145 0 7065 0 [pid=24012] vsize: 28840 Current children cumulated CPU time (s) 349.34 Current children cumulated vsize (Kb) 30964 [startup+360.03 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7073 0 0 0 35888 44 0 0 25 0 1 0 1796353815 29532160 7026 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 7210 7026 145 145 0 7065 0 [pid=24012] vsize: 28840 Current children cumulated CPU time (s) 359.34 Current children cumulated vsize (Kb) 30964 [startup+370.031 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7073 0 0 0 36889 44 0 0 25 0 1 0 1796353815 29532160 7026 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 7210 7026 145 145 0 7065 0 [pid=24012] vsize: 28840 Current children cumulated CPU time (s) 369.35 Current children cumulated vsize (Kb) 30964 [startup+380.031 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7073 0 0 0 37889 44 0 0 25 0 1 0 1796353815 29532160 7026 4294967295 134512640 135094434 3221224432 3221223104 134555815 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 7210 7026 145 145 0 7065 0 [pid=24012] vsize: 28840 Current children cumulated CPU time (s) 379.35 Current children cumulated vsize (Kb) 30964 [startup+390.032 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7073 0 0 0 38889 44 0 0 25 0 1 0 1796353815 29532160 7026 4294967295 134512640 135094434 3221224432 3221223104 134556205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 7210 7026 145 145 0 7065 0 [pid=24012] vsize: 28840 Current children cumulated CPU time (s) 389.35 Current children cumulated vsize (Kb) 30964 [startup+400.033 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7073 0 0 0 39890 44 0 0 25 0 1 0 1796353815 29532160 7026 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 7210 7026 145 145 0 7065 0 [pid=24012] vsize: 28840 Current children cumulated CPU time (s) 399.36 Current children cumulated vsize (Kb) 30964 [startup+410.034 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7073 0 0 0 40890 45 0 0 25 0 1 0 1796353815 29532160 7026 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 7210 7026 145 145 0 7065 0 [pid=24012] vsize: 28840 Current children cumulated CPU time (s) 409.37 Current children cumulated vsize (Kb) 30964 [startup+420.034 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7142 0 0 0 41888 45 0 0 25 0 1 0 1796353815 29827072 7095 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 7282 7095 145 145 0 7137 0 [pid=24012] vsize: 29128 Current children cumulated CPU time (s) 419.35 Current children cumulated vsize (Kb) 31252 [startup+430.034 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7418 0 0 0 42884 47 0 0 25 0 1 0 1796353815 30982144 7371 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 7564 7371 145 145 0 7419 0 [pid=24012] vsize: 30256 Current children cumulated CPU time (s) 429.33 Current children cumulated vsize (Kb) 32380 [startup+440.035 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7670 0 0 0 43879 50 0 0 25 0 1 0 1796353815 32026624 7623 4294967295 134512640 135094434 3221224432 3221223024 134557514 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 7819 7623 145 145 0 7674 0 [pid=24012] vsize: 31276 Current children cumulated CPU time (s) 439.31 Current children cumulated vsize (Kb) 33400 [startup+450.036 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7909 0 0 0 44875 52 0 0 25 0 1 0 1796353815 33001472 7862 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8057 7862 145 145 0 7912 0 [pid=24012] vsize: 32228 Current children cumulated CPU time (s) 449.29 Current children cumulated vsize (Kb) 34352 [startup+460.037 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7998 0 0 0 45874 53 0 0 25 0 1 0 1796353815 33366016 7951 4294967295 134512640 135094434 3221224432 3221223024 134557277 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8146 7951 145 145 0 8001 0 [pid=24012] vsize: 32584 Current children cumulated CPU time (s) 459.29 Current children cumulated vsize (Kb) 34708 [startup+470.038 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7998 0 0 0 46873 53 0 0 25 0 1 0 1796353815 33366016 7951 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8146 7951 145 145 0 8001 0 [pid=24012] vsize: 32584 Current children cumulated CPU time (s) 469.28 Current children cumulated vsize (Kb) 34708 [startup+480.038 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 7998 0 0 0 47873 53 0 0 25 0 1 0 1796353815 33366016 7951 4294967295 134512640 135094434 3221224432 3221223056 134557705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8146 7951 145 145 0 8001 0 [pid=24012] vsize: 32584 Current children cumulated CPU time (s) 479.28 Current children cumulated vsize (Kb) 34708 [startup+490.039 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8003 0 0 0 48874 53 0 0 25 0 1 0 1796353815 33394688 7956 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8153 7956 145 145 0 8008 0 [pid=24012] vsize: 32612 Current children cumulated CPU time (s) 489.29 Current children cumulated vsize (Kb) 34736 [startup+500.039 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8011 0 0 0 49873 54 0 0 25 0 1 0 1796353815 33427456 7964 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8161 7964 145 145 0 8016 0 [pid=24012] vsize: 32644 Current children cumulated CPU time (s) 499.29 Current children cumulated vsize (Kb) 34768 [startup+510.04 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8015 0 0 0 50872 54 0 0 25 0 1 0 1796353815 33443840 7968 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24012/statm): 8165 7968 145 145 0 8020 0 [pid=24012] vsize: 32660 Current children cumulated CPU time (s) 509.28 Current children cumulated vsize (Kb) 34784 [startup+520.041 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8015 0 0 0 51872 54 0 0 25 0 1 0 1796353815 33443840 7968 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8165 7968 145 145 0 8020 0 [pid=24012] vsize: 32660 Current children cumulated CPU time (s) 519.28 Current children cumulated vsize (Kb) 34784 [startup+530.042 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8015 0 0 0 52872 54 0 0 25 0 1 0 1796353815 33443840 7968 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8165 7968 145 145 0 8020 0 [pid=24012] vsize: 32660 Current children cumulated CPU time (s) 529.28 Current children cumulated vsize (Kb) 34784 [startup+540.042 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8021 0 0 0 53872 54 0 0 25 0 1 0 1796353815 33476608 7974 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8173 7974 145 145 0 8028 0 [pid=24012] vsize: 32692 Current children cumulated CPU time (s) 539.28 Current children cumulated vsize (Kb) 34816 [startup+550.043 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8021 0 0 0 54872 55 0 0 25 0 1 0 1796353815 33476608 7974 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8173 7974 145 145 0 8028 0 [pid=24012] vsize: 32692 Current children cumulated CPU time (s) 549.29 Current children cumulated vsize (Kb) 34816 [startup+560.045 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8026 0 0 0 55873 55 0 0 25 0 1 0 1796353815 33492992 7979 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8177 7979 145 145 0 8032 0 [pid=24012] vsize: 32708 Current children cumulated CPU time (s) 559.3 Current children cumulated vsize (Kb) 34832 [startup+570.045 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8040 0 0 0 56873 55 0 0 25 0 1 0 1796353815 33542144 7993 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8189 7993 145 145 0 8044 0 [pid=24012] vsize: 32756 Current children cumulated CPU time (s) 569.3 Current children cumulated vsize (Kb) 34880 [startup+580.046 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8109 0 0 0 57872 56 0 0 25 0 1 0 1796353815 33816576 8062 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8256 8062 145 145 0 8111 0 [pid=24012] vsize: 33024 Current children cumulated CPU time (s) 579.3 Current children cumulated vsize (Kb) 35148 [startup+590.047 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8110 0 0 0 58872 56 0 0 25 0 1 0 1796353815 33816576 8063 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8256 8063 145 145 0 8111 0 [pid=24012] vsize: 33024 Current children cumulated CPU time (s) 589.3 Current children cumulated vsize (Kb) 35148 [startup+600.048 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8110 0 0 0 59872 56 0 0 25 0 1 0 1796353815 33816576 8063 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8256 8063 145 145 0 8111 0 [pid=24012] vsize: 33024 Current children cumulated CPU time (s) 599.3 Current children cumulated vsize (Kb) 35148 [startup+610.048 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8110 0 0 0 60872 56 0 0 25 0 1 0 1796353815 33816576 8063 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8256 8063 145 145 0 8111 0 [pid=24012] vsize: 33024 Current children cumulated CPU time (s) 609.3 Current children cumulated vsize (Kb) 35148 [startup+620.049 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8111 0 0 0 61872 56 0 0 25 0 1 0 1796353815 33816576 8064 4294967295 134512640 135094434 3221224432 3221223104 134555583 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8256 8064 145 145 0 8111 0 [pid=24012] vsize: 33024 Current children cumulated CPU time (s) 619.3 Current children cumulated vsize (Kb) 35148 [startup+630.05 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8111 0 0 0 62873 56 0 0 25 0 1 0 1796353815 33816576 8064 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8256 8064 145 145 0 8111 0 [pid=24012] vsize: 33024 Current children cumulated CPU time (s) 629.31 Current children cumulated vsize (Kb) 35148 [startup+640.051 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8119 0 0 0 63873 56 0 0 25 0 1 0 1796353815 33873920 8072 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8270 8072 145 145 0 8125 0 [pid=24012] vsize: 33080 Current children cumulated CPU time (s) 639.31 Current children cumulated vsize (Kb) 35204 [startup+650.051 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8119 0 0 0 64873 56 0 0 25 0 1 0 1796353815 33873920 8072 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8270 8072 145 145 0 8125 0 [pid=24012] vsize: 33080 Current children cumulated CPU time (s) 649.31 Current children cumulated vsize (Kb) 35204 [startup+660.053 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8119 0 0 0 65873 56 0 0 25 0 1 0 1796353815 33873920 8072 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8270 8072 145 145 0 8125 0 [pid=24012] vsize: 33080 Current children cumulated CPU time (s) 659.31 Current children cumulated vsize (Kb) 35204 [startup+670.054 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8119 0 0 0 66874 56 0 0 25 0 1 0 1796353815 33873920 8072 4294967295 134512640 135094434 3221224432 3221222944 134783376 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8270 8072 145 145 0 8125 0 [pid=24012] vsize: 33080 Current children cumulated CPU time (s) 669.32 Current children cumulated vsize (Kb) 35204 [startup+680.055 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8125 0 0 0 67874 56 0 0 25 0 1 0 1796353815 33906688 8078 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8278 8078 145 145 0 8133 0 [pid=24012] vsize: 33112 Current children cumulated CPU time (s) 679.32 Current children cumulated vsize (Kb) 35236 [startup+690.055 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8126 0 0 0 68874 56 0 0 25 0 1 0 1796353815 33906688 8079 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8278 8079 145 145 0 8133 0 [pid=24012] vsize: 33112 Current children cumulated CPU time (s) 689.32 Current children cumulated vsize (Kb) 35236 [startup+700.056 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8200 0 0 0 69873 57 0 0 25 0 1 0 1796353815 34234368 8153 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8358 8153 145 145 0 8213 0 [pid=24012] vsize: 33432 Current children cumulated CPU time (s) 699.32 Current children cumulated vsize (Kb) 35556 [startup+710.057 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8354 0 0 0 70870 58 0 0 25 0 1 0 1796353815 34881536 8307 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8516 8307 145 145 0 8371 0 [pid=24012] vsize: 34064 Current children cumulated CPU time (s) 709.3 Current children cumulated vsize (Kb) 36188 [startup+720.058 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8354 0 0 0 71870 58 0 0 25 0 1 0 1796353815 34881536 8307 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8516 8307 145 145 0 8371 0 [pid=24012] vsize: 34064 Current children cumulated CPU time (s) 719.3 Current children cumulated vsize (Kb) 36188 [startup+730.058 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8354 0 0 0 72870 58 0 0 25 0 1 0 1796353815 34881536 8307 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8516 8307 145 145 0 8371 0 [pid=24012] vsize: 34064 Current children cumulated CPU time (s) 729.3 Current children cumulated vsize (Kb) 36188 [startup+740.059 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8354 0 0 0 73871 58 0 0 25 0 1 0 1796353815 34881536 8307 4294967295 134512640 135094434 3221224432 3221223104 134556246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8516 8307 145 145 0 8371 0 [pid=24012] vsize: 34064 Current children cumulated CPU time (s) 739.31 Current children cumulated vsize (Kb) 36188 [startup+750.06 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8354 0 0 0 74871 58 0 0 25 0 1 0 1796353815 34881536 8307 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8516 8307 145 145 0 8371 0 [pid=24012] vsize: 34064 Current children cumulated CPU time (s) 749.31 Current children cumulated vsize (Kb) 36188 [startup+760.062 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8367 0 0 0 75871 58 0 0 25 0 1 0 1796353815 34947072 8320 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8532 8320 145 145 0 8387 0 [pid=24012] vsize: 34128 Current children cumulated CPU time (s) 759.31 Current children cumulated vsize (Kb) 36252 [startup+770.062 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8368 0 0 0 76871 58 0 0 25 0 1 0 1796353815 34947072 8321 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8532 8321 145 145 0 8387 0 [pid=24012] vsize: 34128 Current children cumulated CPU time (s) 769.31 Current children cumulated vsize (Kb) 36252 [startup+780.062 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8368 0 0 0 77871 58 0 0 25 0 1 0 1796353815 34947072 8321 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8532 8321 145 145 0 8387 0 [pid=24012] vsize: 34128 Current children cumulated CPU time (s) 779.31 Current children cumulated vsize (Kb) 36252 [startup+790.063 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8368 0 0 0 78872 58 0 0 25 0 1 0 1796353815 34947072 8321 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8532 8321 145 145 0 8387 0 [pid=24012] vsize: 34128 Current children cumulated CPU time (s) 789.32 Current children cumulated vsize (Kb) 36252 [startup+800.064 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8373 0 0 0 79870 59 0 0 25 0 1 0 1796353815 34979840 8326 4294967295 134512640 135094434 3221224432 3221223088 134557987 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24012/statm): 8540 8326 145 145 0 8395 0 [pid=24012] vsize: 34160 Current children cumulated CPU time (s) 799.31 Current children cumulated vsize (Kb) 36284 [startup+810.064 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8378 0 0 0 80870 59 0 0 25 0 1 0 1796353815 35012608 8331 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8548 8331 145 145 0 8403 0 [pid=24012] vsize: 34192 Current children cumulated CPU time (s) 809.31 Current children cumulated vsize (Kb) 36316 [startup+820.065 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8383 0 0 0 81870 59 0 0 25 0 1 0 1796353815 35012608 8336 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8548 8336 145 145 0 8403 0 [pid=24012] vsize: 34192 Current children cumulated CPU time (s) 819.31 Current children cumulated vsize (Kb) 36316 [startup+830.066 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8502 0 0 0 82868 60 0 0 25 0 1 0 1796353815 35483648 8455 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8663 8455 145 145 0 8518 0 [pid=24012] vsize: 34652 Current children cumulated CPU time (s) 829.3 Current children cumulated vsize (Kb) 36776 [startup+840.066 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8503 0 0 0 83868 60 0 0 25 0 1 0 1796353815 35487744 8456 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8664 8456 145 145 0 8519 0 [pid=24012] vsize: 34656 Current children cumulated CPU time (s) 839.3 Current children cumulated vsize (Kb) 36780 [startup+850.067 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8503 0 0 0 84868 60 0 0 25 0 1 0 1796353815 35487744 8456 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8664 8456 145 145 0 8519 0 [pid=24012] vsize: 34656 Current children cumulated CPU time (s) 849.3 Current children cumulated vsize (Kb) 36780 [startup+860.069 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8503 0 0 0 85869 60 0 0 25 0 1 0 1796353815 35487744 8456 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8664 8456 145 145 0 8519 0 [pid=24012] vsize: 34656 Current children cumulated CPU time (s) 859.31 Current children cumulated vsize (Kb) 36780 [startup+870.07 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8503 0 0 0 86869 60 0 0 25 0 1 0 1796353815 35487744 8456 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8664 8456 145 145 0 8519 0 [pid=24012] vsize: 34656 Current children cumulated CPU time (s) 869.31 Current children cumulated vsize (Kb) 36780 [startup+880.07 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8503 0 0 0 87869 60 0 0 25 0 1 0 1796353815 35487744 8456 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8664 8456 145 145 0 8519 0 [pid=24012] vsize: 34656 Current children cumulated CPU time (s) 879.31 Current children cumulated vsize (Kb) 36780 [startup+890.071 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8503 0 0 0 88869 60 0 0 25 0 1 0 1796353815 35487744 8456 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8664 8456 145 145 0 8519 0 [pid=24012] vsize: 34656 Current children cumulated CPU time (s) 889.31 Current children cumulated vsize (Kb) 36780 [startup+900.072 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8503 0 0 0 89870 60 0 0 25 0 1 0 1796353815 35487744 8456 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8664 8456 145 145 0 8519 0 [pid=24012] vsize: 34656 Current children cumulated CPU time (s) 899.32 Current children cumulated vsize (Kb) 36780 [startup+910.073 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8503 0 0 0 90870 60 0 0 25 0 1 0 1796353815 35487744 8456 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8664 8456 145 145 0 8519 0 [pid=24012] vsize: 34656 Current children cumulated CPU time (s) 909.32 Current children cumulated vsize (Kb) 36780 [startup+920.073 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8503 0 0 0 91870 60 0 0 25 0 1 0 1796353815 35487744 8456 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8664 8456 145 145 0 8519 0 [pid=24012] vsize: 34656 Current children cumulated CPU time (s) 919.32 Current children cumulated vsize (Kb) 36780 [startup+930.074 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 8763 0 0 0 92865 62 0 0 25 0 1 0 1796353815 36569088 8716 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 8928 8716 145 145 0 8783 0 [pid=24012] vsize: 35712 Current children cumulated CPU time (s) 929.29 Current children cumulated vsize (Kb) 37836 [startup+940.075 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9075 0 0 0 93859 65 0 0 25 0 1 0 1796353815 37871616 9028 4294967295 134512640 135094434 3221224432 3221223024 134557196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9246 9028 145 145 0 9101 0 [pid=24012] vsize: 36984 Current children cumulated CPU time (s) 939.26 Current children cumulated vsize (Kb) 39108 [startup+950.076 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9371 0 0 0 94855 67 0 0 25 0 1 0 1796353815 39108608 9324 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9548 9324 145 145 0 9403 0 [pid=24012] vsize: 38192 Current children cumulated CPU time (s) 949.24 Current children cumulated vsize (Kb) 40316 [startup+960.077 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9668 0 0 0 95851 68 0 0 25 0 1 0 1796353815 40378368 9621 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9858 9621 145 145 0 9713 0 [pid=24012] vsize: 39432 Current children cumulated CPU time (s) 959.21 Current children cumulated vsize (Kb) 41556 [startup+970.078 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9755 0 0 0 96850 69 0 0 25 0 1 0 1796353815 40730624 9708 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9944 9708 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 969.21 Current children cumulated vsize (Kb) 41900 [startup+980.079 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9755 0 0 0 97850 69 0 0 25 0 1 0 1796353815 40730624 9708 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9944 9708 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 979.21 Current children cumulated vsize (Kb) 41900 [startup+990.08 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9756 0 0 0 98850 69 0 0 25 0 1 0 1796353815 40730624 9709 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9944 9709 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 989.21 Current children cumulated vsize (Kb) 41900 [startup+1000.08 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9757 0 0 0 99850 69 0 0 25 0 1 0 1796353815 40730624 9710 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9944 9710 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 999.21 Current children cumulated vsize (Kb) 41900 [startup+1010.08 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9757 0 0 0 100850 69 0 0 25 0 1 0 1796353815 40730624 9710 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9944 9710 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 1009.21 Current children cumulated vsize (Kb) 41900 [startup+1020.08 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9757 0 0 0 101851 69 0 0 25 0 1 0 1796353815 40730624 9710 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9944 9710 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 1019.22 Current children cumulated vsize (Kb) 41900 [startup+1030.08 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 102850 70 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 1029.22 Current children cumulated vsize (Kb) 41900 [startup+1040.08 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 103849 71 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 1039.22 Current children cumulated vsize (Kb) 41900 [startup+1050.08 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 104849 71 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 1049.22 Current children cumulated vsize (Kb) 41900 [startup+1060.08 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 105849 71 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 1059.22 Current children cumulated vsize (Kb) 41900 [startup+1070.09 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 106849 71 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 1069.22 Current children cumulated vsize (Kb) 41900 [startup+1080.09 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 107849 72 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 1079.23 Current children cumulated vsize (Kb) 41900 [startup+1090.09 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 108849 72 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 1089.23 Current children cumulated vsize (Kb) 41900 [startup+1100.09 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 109849 72 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223024 134557213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 1099.23 Current children cumulated vsize (Kb) 41900 [startup+1110.09 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 110849 72 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 1109.23 Current children cumulated vsize (Kb) 41900 [startup+1120.09 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 111849 72 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 1119.23 Current children cumulated vsize (Kb) 41900 [startup+1130.09 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 112850 72 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 1129.24 Current children cumulated vsize (Kb) 41900 [startup+1140.09 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 113850 72 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223024 134557398 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 1139.24 Current children cumulated vsize (Kb) 41900 [startup+1150.09 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 114850 72 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223024 134557238 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 1149.24 Current children cumulated vsize (Kb) 41900 [startup+1160.09 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 115850 72 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 1159.24 Current children cumulated vsize (Kb) 41900 [startup+1170.09 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 116850 72 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 1169.24 Current children cumulated vsize (Kb) 41900 [startup+1180.1 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9758 0 0 0 117850 73 0 0 25 0 1 0 1796353815 40730624 9711 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9944 9711 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 1179.25 Current children cumulated vsize (Kb) 41900 [startup+1190.1 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9759 0 0 0 118850 73 0 0 25 0 1 0 1796353815 40730624 9712 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9944 9712 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 1189.25 Current children cumulated vsize (Kb) 41900 [startup+1200.1 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9759 0 0 0 119850 73 0 0 25 0 1 0 1796353815 40730624 9712 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9944 9712 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 1199.25 Current children cumulated vsize (Kb) 41900 [startup+1210.1 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9759 0 0 0 120851 73 0 0 25 0 1 0 1796353815 40730624 9712 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9944 9712 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 1209.26 Current children cumulated vsize (Kb) 41900 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.1 s] Raw data (loadavg): 0.99 0.98 0.98 2/57 24012 Raw data (/proc/24008/stat): 24008 (minisat+_script) S 24007 24008 824 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1796353810 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/24008/statm): 531 226 485 147 0 384 0 [pid=24008] vsize: 2124 Raw data (/proc/24012/stat): 24012 (minisat+_64-bit) R 24008 24008 824 0 -1 0 9759 0 0 0 120851 73 0 0 25 0 1 0 1796353815 40730624 9712 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24012/statm): 9944 9712 145 145 0 9799 0 [pid=24012] vsize: 39776 Current children cumulated CPU time (s) 1209.26 Current children cumulated vsize (Kb) 41900 Sending SIGTERM to -24008 Sleeping 2 seconds One traced child (pid=24008) ended because it received signal 15 (SIGTERM) One traced child (pid=24012) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.12 CPU time (s): 1209.27 CPU user time (s): 1208.51 CPU system time (s): 0.754885 CPU usage (%): 99.9292 Max. virtual memory (cumulated for all children) (Kb): 41900
ERROR: no interpretation found !