| Name | mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-rgn.opb |
| MD5SUM | 1400a638b0a1a6fa8602672cb986ba1d |
| Bench Category | optimization, big integers (OPTBIGINT) |
| Has Objective Function | YES |
| Satisfiable | YES |
| (Un)Satisfiability was proved | YES |
| Best value of the objective function | 67200 |
| Optimality of the best value was proved | NO |
| Number of terms in the objective function | 920 |
| Biggest coefficient in the objective function | 24576 |
| Number of bits for the biggest coefficient in the objective function | 15 |
| Sum of the numbers in the objective function | 1986400 |
| Number of bits of the sum of numbers in the objective function | 21 |
| Biggest number in a constraint | 3200000000 |
| Number of bits of the biggest number in a constraint | 32 |
| Biggest sum of numbers in a constraint | 29101875011 |
| Number of bits of the biggest sum of numbers | 35 |
| Best result obtained on this benchmark | SAT |
| Best CPU time to get the best result obtained on this benchmark | 1257.5 |
| Number of variables | 1020 |
| Total number of constraints | 204 |
| Number of constraints which are clauses | 0 |
| Number of constraints which are cardinality constraints (but not clauses) | 104 |
| Number of constraints which are nor clauses,nor cardinality constraints | 100 |
| Minimum length of a constraint | 1 |
| Maximum length of a constraint | 103 |
LAUNCH ON wulflinc5 THE 2005-09-20 03:23:44 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3266 boxname=wulflinc5 idbench=922 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 1400a638b0a1a6fa8602672cb986ba1d /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-rgn.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-rgn.opb IDLAUNCH: 3266 /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: 916620 kB Buffers: 4808 kB Cached: 88800 kB SwapCached: 708 kB Active: 23228 kB Inactive: 73064 kB HighTotal: 131008 kB HighFree: 37968 kB LowTotal: 903652 kB LowFree: 878652 kB SwapTotal: 2097136 kB SwapFree: 2095884 kB Dirty: 52 kB Writeback: 0 kB Mapped: 5756 kB Slab: 16100 kB Committed_AS: 64264 kB PageTables: 332 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 03:43:54 (client local time) WITH STATUS 10 IN 1208.66 SECONDS stats: 3266 7 1208.66 10
c Parsing PB file... c Converting 124 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: #################### c -- Clauses(.)/Splits(s): (none) c ---[ 123]---> BDD-cost: 13 c ---[ 122]---> BDD-cost: 13 c ---[ 121]---> BDD-cost: 13 c ---[ 120]---> BDD-cost: 13 c ---[ 119]---> BDD-cost: 13 c ---[ 118]---> BDD-cost: 13 c ---[ 117]---> BDD-cost: 13 c ---[ 116]---> BDD-cost: 13 c ---[ 115]---> BDD-cost: 13 c ---[ 114]---> BDD-cost: 13 c ---[ 113]---> BDD-cost: 13 c ---[ 112]---> BDD-cost: 13 c ---[ 111]---> BDD-cost: 13 c ---[ 110]---> BDD-cost: 13 c ---[ 109]---> BDD-cost: 13 c ---[ 108]---> BDD-cost: 13 c ---[ 107]---> BDD-cost: 13 c ---[ 106]---> BDD-cost: 13 c ---[ 105]---> BDD-cost: 13 c ---[ 104]---> BDD-cost: 13 c ---[ 103]---> BDD-cost: 8 c ---[ 102]---> BDD-cost: 8 c ---[ 101]---> BDD-cost: 8 c ---[ 100]---> BDD-cost: 8 c ---[ 99]---> BDD-cost: 8 c ---[ 98]---> BDD-cost: 8 c ---[ 97]---> BDD-cost: 8 c ---[ 96]---> BDD-cost: 8 c ---[ 95]---> BDD-cost: 8 c ---[ 94]---> BDD-cost: 8 c ---[ 93]---> BDD-cost: 8 c ---[ 92]---> BDD-cost: 8 c ---[ 91]---> BDD-cost: 8 c ---[ 90]---> BDD-cost: 8 c ---[ 89]---> BDD-cost: 8 c ---[ 88]---> BDD-cost: 8 c ---[ 87]---> BDD-cost: 8 c ---[ 86]---> BDD-cost: 8 c ---[ 85]---> BDD-cost: 8 c ---[ 84]---> BDD-cost: 8 c ---[ 83]---> BDD-cost: 8 c ---[ 82]---> BDD-cost: 8 c ---[ 81]---> BDD-cost: 8 c ---[ 80]---> BDD-cost: 8 c ---[ 79]---> BDD-cost: 8 c ---[ 78]---> BDD-cost: 8 c ---[ 77]---> BDD-cost: 8 c ---[ 76]---> BDD-cost: 8 c ---[ 75]---> BDD-cost: 8 c ---[ 74]---> BDD-cost: 8 c ---[ 73]---> BDD-cost: 8 c ---[ 72]---> BDD-cost: 8 c ---[ 71]---> BDD-cost: 8 c ---[ 70]---> BDD-cost: 8 c ---[ 69]---> BDD-cost: 8 c ---[ 68]---> BDD-cost: 8 c ---[ 67]---> BDD-cost: 8 c ---[ 66]---> BDD-cost: 8 c ---[ 65]---> BDD-cost: 8 c ---[ 64]---> BDD-cost: 8 c ---[ 63]---> BDD-cost: 13 c ---[ 62]---> BDD-cost: 13 c ---[ 61]---> BDD-cost: 13 c ---[ 60]---> BDD-cost: 13 c ---[ 59]---> BDD-cost: 13 c ---[ 58]---> BDD-cost: 13 c ---[ 57]---> BDD-cost: 13 c ---[ 56]---> BDD-cost: 13 c ---[ 55]---> BDD-cost: 13 c ---[ 54]---> BDD-cost: 13 c ---[ 53]---> BDD-cost: 13 c ---[ 52]---> BDD-cost: 13 c ---[ 51]---> BDD-cost: 13 c ---[ 50]---> BDD-cost: 13 c ---[ 49]---> BDD-cost: 13 c ---[ 48]---> BDD-cost: 13 c ---[ 47]---> BDD-cost: 13 c ---[ 46]---> BDD-cost: 13 c ---[ 45]---> BDD-cost: 13 c ---[ 44]---> BDD-cost: 13 c ---[ 42]---> BDD-cost: 228 c ---[ 40]---> BDD-cost: 906 c ---[ 38]---> BDD-cost: 906 c ---[ 36]---> BDD-cost: 906 c ---[ 34]---> BDD-cost: 906 c ---[ 32]---> BDD-cost: 906 c ---[ 30]---> BDD-cost: 906 c ---[ 28]---> BDD-cost: 906 c ---[ 26]---> BDD-cost: 906 c ---[ 24]---> BDD-cost: 906 c ---[ 23]---> BDD-cost: 47 c ---[ 21]---> BDD-cost: 906 c ---[ 19]---> BDD-cost: 906 c ---[ 17]---> BDD-cost: 906 c ---[ 15]---> BDD-cost: 906 c ---[ 13]---> BDD-cost: 906 c ---[ 11]---> BDD-cost: 906 c ---[ 10]---> BDD-cost: 47 c ---[ 9]---> BDD-cost: 47 c ---[ 8]---> BDD-cost: 47 c ---[ 6]---> BDD-cost: 228 c ---[ 4]---> BDD-cost: 228 c ---[ 2]---> BDD-cost: 228 c ---[ 0]---> BDD-cost: 228 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 40259 113278 | 13419 0 0 nan | 0.000 % | c | 100 | 40118 112996 | 14760 92 564 6.1 | 0.951 % | c | 250 | 40103 112966 | 16236 240 1981 8.3 | 0.998 % | c | 477 | 40092 112944 | 17860 466 5702 12.2 | 1.031 % | c | 814 | 40092 112944 | 19646 803 17649 22.0 | 1.031 % | c | 1322 | 40092 112944 | 21611 1311 27839 21.2 | 1.031 % | c | 2083 | 40092 112944 | 23772 2072 38233 18.5 | 1.031 % | c | 3223 | 39997 112751 | 26149 3200 52692 16.5 | 1.247 % | c | 4932 | 39983 112722 | 28764 4908 86494 17.6 | 1.254 % | c | 7498 | 39909 112571 | 31641 7459 133322 17.9 | 1.483 % | c | 11343 | 39891 112535 | 34805 11301 187175 16.6 | 1.537 % | c | 17110 | 39766 112261 | 38285 17004 338276 19.9 | 1.874 % | c | 25759 | 39746 112220 | 42114 25652 792984 30.9 | 1.881 % | c | 38734 | 39746 112220 | 46326 38627 1026727 26.6 | 1.881 % | c | 58198 | 39619 111941 | 50958 22540 676426 30.0 | 2.002 % | c | 87390 | 39602 111907 | 56054 51730 1239064 24.0 | 2.056 % | c | 131179 | 39292 111258 | 61659 50028 1324784 26.5 | 2.596 % | c | 196863 | 39125 110902 | 67825 63381 1605437 25.3 | 3.034 % | c | 295389 | 38687 109943 | 74608 50436 1436146 28.5 | 3.978 % | c | 443178 | 38500 109542 | 82069 64703 1786871 27.6 | 4.402 % | c ============================================================================== c [1mFound solution: 814378[0m c ---[ 0]---> Sorter-cost:66120 Base: 2 2 2 2 2 2 3 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 658244 | 220981 535504 | 73660 52875 3351582 63.4 | 4.402 % | c | 658344 | 220973 535488 | 81026 52973 3352621 63.3 | 1.005 % | c | 658495 | 220952 535443 | 89128 53122 3353583 63.1 | 1.005 % | c | 658720 | 220952 535443 | 98041 53347 3357206 62.9 | 1.005 % | c | 659058 | 220952 535443 | 107845 53685 3362862 62.6 | 1.005 % | c | 659564 | 220952 535443 | 118630 54191 3371925 62.2 | 1.005 % | c | 660323 | 220952 535443 | 130493 54950 3394228 61.8 | 1.005 % | c | 661462 | 220952 535443 | 143542 56089 3432961 61.2 | 1.005 % | c | 663171 | 220952 535443 | 157896 57798 3459088 59.8 | 1.005 % | c | 665733 | 220952 535443 | 173686 60360 3528174 58.5 | 1.005 % | c | 669577 | 220952 535443 | 191055 64204 3606827 56.2 | 1.005 % | c | 675343 | 220952 535443 | 210160 69970 3682771 52.6 | 1.005 % | c | 683992 | 220952 535443 | 231176 78619 3957858 50.3 | 1.005 % | c | 696967 | 220952 535443 | 254294 91594 4746587 51.8 | 1.005 % | c | 716429 | 220935 535406 | 279723 111045 5477152 49.3 | 1.016 % | c | 745621 | 220935 535406 | 307696 140237 6912181 49.3 | 1.016 % | c | 789411 | 220903 535339 | 338465 184022 9087383 49.4 | 1.035 % | c ============================================================================== c [1mFound solution: 448098[0m c ---[ 0]---> Sorter-cost: 12 Base: 2 2 2 2 2 2 3 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 805474 | 221600 537386 | 73866 200085 9691724 48.4 | 1.035 % | c | 805576 | 221600 537386 | 81252 22706 518069 22.8 | 1.031 % | c | 805727 | 221600 537386 | 89377 22857 519321 22.7 | 1.031 % | c | 805952 | 221600 537386 | 98315 23082 522059 22.6 | 1.031 % | c | 806290 | 221600 537386 | 108147 23420 525041 22.4 | 1.031 % | c | 806797 | 221600 537386 | 118961 23927 529488 22.1 | 1.031 % | c | 807556 | 221518 537202 | 130858 24683 541108 21.9 | 1.058 % | c | 808695 | 221477 537108 | 143943 25821 552112 21.4 | 1.071 % | c | 810404 | 221477 537108 | 158338 27530 582434 21.2 | 1.071 % | c | 812969 | 221477 537108 | 174172 30095 668074 22.2 | 1.071 % | c | 816814 | 221477 537108 | 191589 33940 772663 22.8 | 1.071 % | c | 822580 | 221477 537108 | 210748 39706 1057784 26.6 | 1.071 % | c | 831229 | 221477 537108 | 231823 48355 1421889 29.4 | 1.071 % | c | 844203 | 221477 537108 | 255005 61329 1917977 31.3 | 1.071 % | c | 863664 | 221477 537108 | 280506 80790 2407543 29.8 | 1.071 % | c | 892856 | 221381 536907 | 308556 109946 3371240 30.7 | 1.129 % | c ============================================================================== c [1mFound solution: 233250[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 3 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 897055 | 221462 537101 | 73820 114145 3524606 30.9 | 1.129 % | c | 897155 | 221462 537101 | 81202 27724 519075 18.7 | 1.129 % | c | 897305 | 221462 537101 | 89322 27874 520470 18.7 | 1.129 % | c | 897530 | 221462 537101 | 98254 28099 522245 18.6 | 1.129 % | c | 897868 | 221171 536443 | 108079 28404 524583 18.5 | 1.232 % | c | 898374 | 221171 536443 | 118887 28910 538384 18.6 | 1.232 % | c | 899133 | 221171 536443 | 130776 29669 549995 18.5 | 1.232 % | c | 900273 | 221171 536443 | 143854 30809 561146 18.2 | 1.232 % | c | 901981 | 221171 536443 | 158239 32517 592744 18.2 | 1.232 % | c | 904543 | 221171 536443 | 174063 35079 710858 20.3 | 1.232 % | c | 908389 | 221171 536443 | 191470 38925 853279 21.9 | 1.232 % | c | 914155 | 221171 536443 | 210617 44691 1111469 24.9 | 1.232 % | c | 922804 | 221171 536443 | 231678 53340 1322266 24.8 | 1.232 % | c | 935778 | 221134 536360 | 254846 66304 1882902 28.4 | 1.254 % | c | 955240 | 221134 536360 | 280331 85766 2967169 34.6 | 1.254 % | c | 984432 | 221107 536306 | 308364 114945 4194533 36.5 | 1.270 % | c ============================================================================== c [1mFound solution: 233162[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 3 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 988122 | 221125 536453 | 73708 118635 4301809 36.3 | 1.270 % | c | 988222 | 221123 536449 | 81078 30375 683144 22.5 | 1.273 % | c | 988372 | 221123 536449 | 89186 30525 684026 22.4 | 1.273 % | c | 988597 | 221123 536449 | 98105 30750 686137 22.3 | 1.273 % | c | 988934 | 220944 536046 | 107915 31076 688900 22.2 | 1.334 % | c | 989440 | 220944 536046 | 118707 31582 693327 22.0 | 1.334 % | c | 990201 | 220944 536046 | 130578 32343 703900 21.8 | 1.334 % | c | 991340 | 220944 536046 | 143636 33482 716103 21.4 | 1.334 % | c | 993048 | 220944 536046 | 157999 35190 774995 22.0 | 1.334 % | c | 995610 | 220932 536019 | 173799 37751 921702 24.4 | 1.338 % | c | 999454 | 220932 536019 | 191179 41595 1028393 24.7 | 1.338 % | c | 1005222 | 220932 536019 | 210297 47363 2188043 46.2 | 1.338 % | c | 1013873 | 220932 536019 | 231327 56014 2367858 42.3 | 1.338 % | c | 1026847 | 220932 536019 | 254460 68988 3142624 45.6 | 1.338 % | c | 1046310 | 220932 536019 | 279906 88451 4144431 46.9 | 1.338 % | c ============================================================================== c [1mFound solution: 216484[0m c ---[ 0]---> Sorter-cost: 14 Base: 2 2 2 2 2 2 3 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1047505 | 220617 535311 | 73539 89627 4182324 46.7 | 1.338 % | c | 1047606 | 220617 535311 | 80892 32998 660591 20.0 | 1.471 % | c | 1047757 | 220617 535311 | 88982 33149 662245 20.0 | 1.471 % | c | 1047982 | 220617 535311 | 97880 33374 664248 19.9 | 1.471 % | c | 1048319 | 220617 535311 | 107668 33711 668588 19.8 | 1.471 % | c | 1048825 | 220617 535311 | 118435 34217 674919 19.7 | 1.471 % | c | 1049584 | 220280 534537 | 130278 34959 688719 19.7 | 1.609 % | c | 1050724 | 220280 534537 | 143306 36099 723586 20.0 | 1.609 % | c | 1052432 | 220280 534537 | 157637 37807 783850 20.7 | 1.609 % | c | 1054994 | 220280 534537 | 173401 40369 858493 21.3 | 1.609 % | c | 1058838 | 220280 534537 | 190741 44213 1043337 23.6 | 1.609 % | c | 1064606 | 220280 534537 | 209815 49981 1280146 25.6 | 1.609 % | c c *** TERMINATED *** s SATISFIABLE v TA1_bit_7 TA1_bit_6 TA1_bit_5 TA1_bit_4 TA1_bit_3 TA1_bit_2 -TA1_bit_1 -TA1_bit0 -TA1_bit1 TA1_bit2 -TA1_bit3 -TA1_bit4 -TA1_bit5 -TA1_bit6 TA2_bit_7 TA2_bit_6 TA2_bit_5 TA2_bit_4 TA2_bit_3 TA2_bit_2 -TA2_bit_1 -TA2_bit0 -TA2_bit1 TA2_bit2 -TA2_bit3 -TA2_bit4 -TA2_bit5 -TA2_bit6 TA3_bit_7 TA3_bit_6 TA3_bit_5 TA3_bit_4 TA3_bit_3 TA3_bit_2 -TA3_bit_1 -TA3_bit0 TA3_bit1 -TA3_bit2 -TA3_bit3 -TA3_bit4 -TA3_bit5 -TA3_bit6 TA4_bit_7 TA4_bit_6 TA4_bit_5 TA4_bit_4 TA4_bit_3 TA4_bit_2 -TA4_bit_1 TA4_bit0 -TA4_bit1 -TA4_bit2 -TA4_bit3 -TA4_bit4 -TA4_bit5 -TA4_bit6 TB1_bit_7 TB1_bit_6 TB1_bit_5 TB1_bit_4 TB1_bit_3 TB1_bit_2 -TB1_bit_1 -TB1_bit0 -TB1_bit1 TB1_bit2 TB1_bit3 -TB1_bit4 -TB1_bit5 -TB1_bit6 TB2_bit_7 TB2_bit_6 TB2_bit_5 TB2_bit_4 TB2_bit_3 TB2_bit_2 TB2_bit_1 -TB2_bit0 -TB2_bit1 -TB2_bit2 -TB2_bit3 -TB2_bit4 -TB2_bit5 -TB2_bit6 TB3_bit_7 TB3_bit_6 TB3_bit_5 TB3_bit_4 TB3_bit_3 TB3_bit_2 -TB3_bit_1 -TB3_bit0 TB3_bit1 -TB3_bit2 -TB3_bit3 -TB3_bit4 -TB3_bit5 -TB3_bit6 TB4_bit_7 TB4_bit_6 TB4_bit_5 TB4_bit_4 TB4_bit_3 TB4_bit_2 -TB4_bit_1 -TB4_bit0 TB4_bit1 TB4_bit2 -TB4_bit3 -TB4_bit4 -TB4_bit5 -TB4_bit6 -TC1_bit_7 TC1_bit_6 -TC1_bit_5 TC1_bit_4 TC1_bit_3 TC1_bit_2 -TC1_bit_1 -TC1_bit0 -TC1_bit1 TC1_bit2 TC1_bit3 -TC1_bit4 -TC1_bit5 -TC1_bit6 -TC2_bit_7 TC2_bit_6 TC2_bit_5 TC2_bit_4 TC2_bit_3 TC2_bit_2 -TC2_bit_1 TC2_bit0 -TC2_bit1 TC2_bit2 TC2_bit3 -TC2_bit4 -TC2_bit5 -TC2_bit6 TC3_bit_7 TC3_bit_6 TC3_bit_5 TC3_bit_4 TC3_bit_3 TC3_bit_2 -TC3_bit_1 TC3_bit0 -TC3_bit1 TC3_bit2 TC3_bit3 -TC3_bit4 -TC3_bit5 -TC3_bit6 TC4_bit_7 TC4_bit_6 TC4_bit_5 TC4_bit_4 TC4_bit_3 TC4_bit_2 -TC4_bit_1 TC4_bit0 TC4_bit1 TC4_bit2 TC4_bit3 -TC4_bit4 -TC4_bit5 -TC4_bit6 TD1_bit_7 TD1_bit_6 TD1_bit_5 TD1_bit_4 TD1_bit_3 TD1_bit_2 -TD1_bit_1 -TD1_bit0 TD1_bit1 TD1_bit2 TD1_bit3 -TD1_bit4 -TD1_bit5 -TD1_bit6 TD2_bit_7 TD2_bit_6 TD2_bit_5 TD2_bit_4 TD2_bit_3 TD2_bit_2 -TD2_bit_1 TD2_bit0 -TD2_bit1 TD2_bit2 TD2_bit3 TD2_bit4 -TD2_bit5 -TD2_bit6 TD3_bit_7 TD3_bit_6 TD3_bit_5 TD3_bit_4 TD3_bit_3 TD3_bit_2 -TD3_bit_1 -TD3_bit0 TD3_bit1 TD3_bit2 -TD3_bit3 -TD3_bit4 -TD3_bit5 -TD3_bit6 TD4_bit_7 TD4_bit_6 TD4_bit_5 TD4_bit_4 TD4_bit_3 TD4_bit_2 -TD4_bit_1 TD4_bit0 TD4_bit1 TD4_bit2 TD4_bit3 -TD4_bit4 -TD4_bit5 -TD4_bit6 TE1_bit_7 TE1_bit_6 TE1_bit_5 TE1_bit_4 TE1_bit_3 TE1_bit_2 -TE1_bit_1 -TE1_bit0 TE1_bit1 TE1_bit2 -TE1_bit3 -TE1_bit4 -TE1_bit5 -TE1_bit6 TE2_bit_7 TE2_bit_6 TE2_bit_5 TE2_bit_4 TE2_bit_3 TE2_bit_2 -TE2_bit_1 -TE2_bit0 TE2_bit1 TE2_bit2 TE2_bit3 -TE2_bit4 -TE2_bit5 -TE2_bit6 TE3_bit_7 TE3_bit_6 TE3_bit_5 TE3_bit_4 TE3_bit_3 TE3_bit_2 -TE3_bit_1 -TE3_bit0 TE3_bit1 TE3_bit2 -TE3_bit3 -TE3_bit4 -TE3_bit5 -TE3_bit6 TE4_bit_7 TE4_bit_6 TE4_bit_5 TE4_bit_4 TE4_bit_3 TE4_bit_2 -TE4_bit_1 -TE4_bit0 -TE4_bit1 TE4_bit2 -TE4_bit3 -TE4_bit4 -TE4_bit5 -TE4_bit6 UA1_bit_7 UA1_bit_6 UA1_bit_5 UA1_bit_4 UA1_bit_3 UA1_bit_2 -UA1_bit_1 UA1_bit0 -UA1_bit1 UA2_bit_7 UA2_bit_6 UA2_bit_5 UA2_bit_4 UA2_bit_3 UA2_bit_2 -UA2_bit_1 -UA2_bit0 -UA2_bit1 UA3_bit_7 UA3_bit_6 UA3_bit_5 UA3_bit_4 UA3_bit_3 UA3_bit_2 UA3_bit_1 -UA3_bit0 -UA3_bit1 UA4_bit_7 UA4_bit_6 UA4_bit_5 UA4_bit_4 UA4_bit_3 UA4_bit_2 -UA4_bit_1 -UA4_bit0 -UA4_bit1 UB1_bit_7 UB1_bit_6 UB1_bit_5 UB1_bit_4 UB1_bit_3 UB1_bit_2 -UB1_bit_1 UB1_bit0 -UB1_bit1 UB2_bit_7 UB2_bit_6 UB2_bit_5 UB2_bit_4 UB2_bit_3 UB2_bit_2 UB2_bit_1 UB2_bit0 -UB2_bit1 UB3_bit_7 UB3_bit_6 UB3_bit_5 UB3_bit_4 UB3_bit_3 UB3_bit_2 UB3_bit_1 -UB3_bit0 -UB3_bit1 UB4_bit_7 UB4_bit_6 UB4_bit_5 UB4_bit_4 UB4_bit_3 UB4_bit_2 -UB4_bit_1 -UB4_bit0 -UB4_bit1 -UC1_bit_7 -UC1_bit_6 UC1_bit_5 UC1_bit_4 UC1_bit_3 UC1_bit_2 -UC1_bit_1 UC1_bit0 -UC1_bit1 -UC2_bit_7 -UC2_bit_6 UC2_bit_5 UC2_bit_4 UC2_bit_3 UC2_bit_2 -UC2_bit_1 UC2_bit0 -UC2_bit1 UC3_bit_7 -UC3_bit_6 UC3_bit_5 UC3_bit_4 UC3_bit_3 UC3_bit_2 -UC3_bit_1 -UC3_bit0 -UC3_bit1 UC4_bit_7 -UC4_bit_6 UC4_bit_5 UC4_bit_4 UC4_bit_3 UC4_bit_2 -UC4_bit_1 -UC4_bit0 -UC4_bit1 UD1_bit_7 UD1_bit_6 UD1_bit_5 UD1_bit_4 UD1_bit_3 UD1_bit_2 -UD1_bit_1 -UD1_bit0 -UD1_bit1 UD2_bit_7 UD2_bit_6 UD2_bit_5 UD2_bit_4 UD2_bit_3 UD2_bit_2 -UD2_bit_1 UD2_bit0 -UD2_bit1 UD3_bit_7 UD3_bit_6 UD3_bit_5 UD3_bit_4 UD3_bit_3 UD3_bit_2 UD3_bit_1 UD3_bit0 -UD3_bit1 UD4_bit_7 UD4_bit_6 UD4_bit_5 UD4_bit_4 UD4_bit_3 UD4_bit_2 UD4_bit_1 UD4_bit0 -UD4_bit1 UE1_bit_7 UE1_bit_6 UE1_bit_5 UE1_bit_4 UE1_bit_3 UE1_bit_2 -UE1_bit_1 -UE1_bit0 -UE1_bit1 UE2_bit_7 UE2_bit_6 UE2_bit_5 UE2_bit_4 UE2_bit_3 UE2_bit_2 UE2_bit_1 -UE2_bit0 -UE2_bit1 UE3_bit_7 UE3_bit_6 UE3_bit_5 UE3_bit_4 UE3_bit_3 UE3_bit_2 -UE3_bit_1 -UE3_bit0 -UE3_bit1 UE4_bit_7 UE4_bit_6 UE4_bit_5 UE4_bit_4 UE4_bit_3 UE4_bit_2 UE4_bit_1 -UE4_bit0 -UE4_bit1 VA1_bit_7 VA1_bit_6 VA1_bit_5 VA1_bit_4 VA1_bit_3 VA1_bit_2 -VA1_bit_1 -VA1_bit0 -VA1_bit1 VA2_bit_7 VA2_bit_6 VA2_bit_5 VA2_bit_4 VA2_bit_3 VA2_bit_2 -VA2_bit_1 -VA2_bit0 -VA2_bit1 VA3_bit_7 VA3_bit_6 VA3_bit_5 VA3_bit_4 VA3_bit_3 VA3_bit_2 -VA3_bit_1 -VA3_bit0 -VA3_bit1 VA4_bit_7 VA4_bit_6 VA4_bit_5 VA4_bit_4 VA4_bit_3 VA4_bit_2 -VA4_bit_1 VA4_bit0 -VA4_bit1 VB1_bit_7 VB1_bit_6 VB1_bit_5 VB1_bit_4 VB1_bit_3 VB1_bit_2 VB1_bit_1 -VB1_bit0 -VB1_bit1 VB2_bit_7 VB2_bit_6 VB2_bit_5 VB2_bit_4 VB2_bit_3 VB2_bit_2 -VB2_bit_1 VB2_bit0 -VB2_bit1 VB3_bit_7 VB3_bit_6 VB3_bit_5 VB3_bit_4 VB3_bit_3 VB3_bit_2 -VB3_bit_1 VB3_bit0 -VB3_bit1 VB4_bit_7 VB4_bit_6 VB4_bit_5 VB4_bit_4 VB4_bit_3 VB4_bit_2 -VB4_bit_1 -VB4_bit0 -VB4_bit1 VC1_bit_7 -VC1_bit_6 VC1_bit_5 VC1_bit_4 VC1_bit_3 VC1_bit_2 VC1_bit_1 VC1_bit0 -VC1_bit1 VC2_bit_7 -VC2_bit_6 VC2_bit_5 VC2_bit_4 VC2_bit_3 VC2_bit_2 -VC2_bit_1 -VC2_bit0 -VC2_bit1 VC3_bit_7 -VC3_bit_6 VC3_bit_5 VC3_bit_4 VC3_bit_3 VC3_bit_2 VC3_bit_1 -VC3_bit0 -VC3_bit1 VC4_bit_7 -VC4_bit_6 VC4_bit_5 VC4_bit_4 VC4_bit_3 VC4_bit_2 -VC4_bit_1 VC4_bit0 -VC4_bit1 VD1_bit_7 VD1_bit_6 VD1_bit_5 VD1_bit_4 VD1_bit_3 VD1_bit_2 VD1_bit_1 -VD1_bit0 -VD1_bit1 VD2_bit_7 VD2_bit_6 VD2_bit_5 VD2_bit_4 VD2_bit_3 VD2_bit_2 -VD2_bit_1 VD2_bit0 -VD2_bit1 VD3_bit_7 VD3_bit_6 VD3_bit_5 VD3_bit_4 VD3_bit_3 VD3_bit_2 -VD3_bit_1 VD3_bit0 -VD3_bit1 VD4_bit_7 VD4_bit_6 VD4_bit_5 VD4_bit_4 VD4_bit_3 VD4_bit_2 VD4_bit_1 VD4_bit0 -VD4_bit1 VE1_bit_7 VE1_bit_6 VE1_bit_5 VE1_bit_4 VE1_bit_3 VE1_bit_2 VE1_bit_1 VE1_bit0 -VE1_bit1 VE2_bit_7 VE2_bit_6 VE2_bit_5 VE2_bit_4 VE2_bit_3 VE2_bit_2 VE2_bit_1 VE2_bit0 -VE2_bit1 VE3_bit_7 VE3_bit_6 VE3_bit_5 VE3_bit_4 VE3_bit_3 VE3_bit_2 -VE3_bit_1 -VE3_bit0 -VE3_bit1 VE4_bit_7 VE4_bit_6 VE4_bit_5 VE4_bit_4 VE4_bit_3 VE4_bit_2 -VE4_bit_1 VE4_bit0 -VE4_bit1 WA1_bit_7 WA1_bit_6 WA1_bit_5 WA1_bit_4 WA1_bit_3 WA1_bit_2 WA1_bit_1 -WA1_bit0 -WA1_bit1 -WA1_bit2 WA1_bit3 -WA1_bit4 -WA1_bit5 -WA1_bit6 WA2_bit_7 WA2_bit_6 WA2_bit_5 WA2_bit_4 WA2_bit_3 WA2_bit_2 -WA2_bit_1 WA2_bit0 WA2_bit1 -WA2_bit2 WA2_bit3 -WA2_bit4 -WA2_bit5 -WA2_bit6 WA3_bit_7 WA3_bit_6 WA3_bit_5 WA3_bit_4 WA3_bit_3 WA3_bit_2 -WA3_bit_1 WA3_bit0 -WA3_bit1 WA3_bit2 WA3_bit3 -WA3_bit4 -WA3_bit5 -WA3_bit6 WA4_bit_7 WA4_bit_6 WA4_bit_5 WA4_bit_4 WA4_bit_3 WA4_bit_2 -WA4_bit_1 -WA4_bit0 WA4_bit1 WA4_bit2 WA4_bit3 -WA4_bit4 -WA4_bit5 -WA4_bit6 WB1_bit_7 WB1_bit_6 WB1_bit_5 WB1_bit_4 WB1_bit_3 WB1_bit_2 -WB1_bit_1 -WB1_bit0 -WB1_bit1 -WB1_bit2 -WB1_bit3 WB1_bit4 -WB1_bit5 -WB1_bit6 WB2_bit_7 WB2_bit_6 WB2_bit_5 WB2_bit_4 WB2_bit_3 WB2_bit_2 -WB2_bit_1 -WB2_bit0 -WB2_bit1 -WB2_bit2 WB2_bit3 -WB2_bit4 -WB2_bit5 -WB2_bit6 WB3_bit_7 WB3_bit_6 WB3_bit_5 WB3_bit_4 WB3_bit_3 WB3_bit_2 -WB3_bit_1 -WB3_bit0 -WB3_bit1 WB3_bit2 WB3_bit3 -WB3_bit4 -WB3_bit5 -WB3_bit6 WB4_bit_7 WB4_bit_6 WB4_bit_5 WB4_bit_4 WB4_bit_3 WB4_bit_2 -WB4_bit_1 -WB4_bit0 -WB4_bit1 WB4_bit2 -WB4_bit3 WB4_bit4 -WB4_bit5 -WB4_bit6 WC1_bit_7 -WC1_bit_6 -WC1_bit_5 WC1_bit_4 WC1_bit_3 WC1_bit_2 -WC1_bit_1 WC1_bit0 WC1_bit1 WC1_bit2 WC1_bit3 -WC1_bit4 -WC1_bit5 -WC1_bit6 WC2_bit_7 -WC2_bit_6 WC2_bit_5 WC2_bit_4 WC2_bit_3 WC2_bit_2 -WC2_bit_1 WC2_bit0 -WC2_bit1 WC2_bit2 -WC2_bit3 WC2_bit4 -WC2_bit5 -WC2_bit6 WC3_bit_7 WC3_bit_6 WC3_bit_5 WC3_bit_4 WC3_bit_3 WC3_bit_2 -WC3_bit_1 WC3_bit0 WC3_bit1 WC3_bit2 -WC3_bit3 WC3_bit4 -WC3_bit5 -WC3_bit6 WC4_bit_7 WC4_bit_6 WC4_bit_5 WC4_bit_4 WC4_bit_3 WC4_bit_2 -WC4_bit_1 -WC4_bit0 -WC4_bit1 WC4_bit2 WC4_bit3 WC4_bit4 -WC4_bit5 -WC4_bit6 WD1_bit_7 WD1_bit_6 WD1_bit_5 WD1_bit_4 WD1_bit_3 WD1_bit_2 -WD1_bit_1 WD1_bit0 -WD1_bit1 -
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/24908/stat): 24908 (minisat+_script) R 24907 24908 824 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797047412 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/24908/statm): 174 3 169 147 0 27 0 [pid=24908] 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=24909 New process pid=24910 New process pid=24911 execve syscall for /bin/sed executable One traced child (pid=24910) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=24911) exited with status: 0 One traced child (pid=24909) exited with status: 0 New process pid=24912 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-13-7-rgn.opb [startup+10.0035 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 2287 0 0 0 973 9 0 0 25 0 1 0 1797047417 9596928 2216 4294967295 134512640 135094434 3221224448 3221223088 134556681 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 2343 2216 145 145 0 2198 0 [pid=24912] vsize: 9372 Current children cumulated CPU time (s) 9.83 Current children cumulated vsize (Kb) 11496 [startup+20.0043 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 2950 0 0 0 1962 13 0 0 25 0 1 0 1797047417 12406784 2879 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24912/statm): 3029 2879 145 145 0 2884 0 [pid=24912] vsize: 12116 Current children cumulated CPU time (s) 19.76 Current children cumulated vsize (Kb) 14240 [startup+30.005 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 3274 0 0 0 2956 16 0 0 25 0 1 0 1797047417 13709312 3203 4294967295 134512640 135094434 3221224448 3221223096 134558037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 3347 3203 145 145 0 3202 0 [pid=24912] vsize: 13388 Current children cumulated CPU time (s) 29.73 Current children cumulated vsize (Kb) 15512 [startup+40.0057 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 3302 0 0 0 3956 16 0 0 25 0 1 0 1797047417 13840384 3231 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 3379 3231 145 145 0 3234 0 [pid=24912] vsize: 13516 Current children cumulated CPU time (s) 39.73 Current children cumulated vsize (Kb) 15640 [startup+50.0065 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 3355 0 0 0 4956 16 0 0 25 0 1 0 1797047417 14053376 3284 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 3431 3284 145 145 0 3286 0 [pid=24912] vsize: 13724 Current children cumulated CPU time (s) 49.73 Current children cumulated vsize (Kb) 15848 [startup+60.0062 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 3647 0 0 0 5952 18 0 0 25 0 1 0 1797047417 15290368 3576 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 3733 3576 145 145 0 3588 0 [pid=24912] vsize: 14932 Current children cumulated CPU time (s) 59.71 Current children cumulated vsize (Kb) 17056 [startup+70.007 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 3676 0 0 0 6952 19 0 0 25 0 1 0 1797047417 15421440 3605 4294967295 134512640 135094434 3221224448 3221223136 134554779 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 3765 3605 145 145 0 3620 0 [pid=24912] vsize: 15060 Current children cumulated CPU time (s) 69.72 Current children cumulated vsize (Kb) 17184 [startup+80.0077 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 4250 0 0 0 7944 22 0 0 25 0 1 0 1797047417 17756160 4179 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 4335 4179 145 145 0 4190 0 [pid=24912] vsize: 17340 Current children cumulated CPU time (s) 79.67 Current children cumulated vsize (Kb) 19464 [startup+90.0084 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 4401 0 0 0 8943 23 0 0 25 0 1 0 1797047417 18620416 4330 4294967295 134512640 135094434 3221224448 3221223104 134558002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 4546 4330 145 145 0 4401 0 [pid=24912] vsize: 18184 Current children cumulated CPU time (s) 89.67 Current children cumulated vsize (Kb) 20308 [startup+100.009 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 4425 0 0 0 9943 23 0 0 25 0 1 0 1797047417 18735104 4354 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 4574 4354 145 145 0 4429 0 [pid=24912] vsize: 18296 Current children cumulated CPU time (s) 99.67 Current children cumulated vsize (Kb) 20420 [startup+110.012 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 4469 0 0 0 10943 23 0 0 25 0 1 0 1797047417 18948096 4398 4294967295 134512640 135094434 3221224448 3221223108 134553480 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 4626 4398 145 145 0 4481 0 [pid=24912] vsize: 18504 Current children cumulated CPU time (s) 109.67 Current children cumulated vsize (Kb) 20628 [startup+120.013 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 4621 0 0 0 11941 24 0 0 25 0 1 0 1797047417 19570688 4550 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 4778 4550 145 145 0 4633 0 [pid=24912] vsize: 19112 Current children cumulated CPU time (s) 119.66 Current children cumulated vsize (Kb) 21236 [startup+130.012 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 4622 0 0 0 12941 24 0 0 25 0 1 0 1797047417 19570688 4551 4294967295 134512640 135094434 3221224448 3221223120 134556327 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 4778 4551 145 145 0 4633 0 [pid=24912] vsize: 19112 Current children cumulated CPU time (s) 129.66 Current children cumulated vsize (Kb) 21236 [startup+140.013 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 4673 0 0 0 13941 25 0 0 25 0 1 0 1797047417 19832832 4602 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 4842 4602 145 145 0 4697 0 [pid=24912] vsize: 19368 Current children cumulated CPU time (s) 139.67 Current children cumulated vsize (Kb) 21492 [startup+150.014 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 5358 0 0 0 14931 29 0 0 25 0 1 0 1797047417 22675456 5287 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 5536 5287 145 145 0 5391 0 [pid=24912] vsize: 22144 Current children cumulated CPU time (s) 149.61 Current children cumulated vsize (Kb) 24268 [startup+160.015 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 5382 0 0 0 15930 29 0 0 25 0 1 0 1797047417 22769664 5311 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 5559 5311 145 145 0 5414 0 [pid=24912] vsize: 22236 Current children cumulated CPU time (s) 159.6 Current children cumulated vsize (Kb) 24360 [startup+170.015 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 5408 0 0 0 16931 29 0 0 25 0 1 0 1797047417 22900736 5337 4294967295 134512640 135094434 3221224448 3221223120 134556246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 5591 5337 145 145 0 5446 0 [pid=24912] vsize: 22364 Current children cumulated CPU time (s) 169.61 Current children cumulated vsize (Kb) 24488 [startup+180.016 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 5479 0 0 0 17930 29 0 0 25 0 1 0 1797047417 23244800 5408 4294967295 134512640 135094434 3221224448 3221223104 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 5675 5408 145 145 0 5530 0 [pid=24912] vsize: 22700 Current children cumulated CPU time (s) 179.6 Current children cumulated vsize (Kb) 24824 [startup+190.017 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 5898 0 0 0 18924 31 0 0 25 0 1 0 1797047417 24907776 5827 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 6081 5827 145 145 0 5936 0 [pid=24912] vsize: 24324 Current children cumulated CPU time (s) 189.56 Current children cumulated vsize (Kb) 26448 [startup+200.018 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 5899 0 0 0 19924 31 0 0 25 0 1 0 1797047417 24907776 5828 4294967295 134512640 135094434 3221224448 3221223060 134563134 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 6081 5828 145 145 0 5936 0 [pid=24912] vsize: 24324 Current children cumulated CPU time (s) 199.56 Current children cumulated vsize (Kb) 26448 [startup+210.017 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 5899 0 0 0 20924 31 0 0 25 0 1 0 1797047417 24907776 5828 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 6081 5828 145 145 0 5936 0 [pid=24912] vsize: 24324 Current children cumulated CPU time (s) 209.56 Current children cumulated vsize (Kb) 26448 [startup+220.018 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 5910 0 0 0 21925 31 0 0 25 0 1 0 1797047417 24973312 5839 4294967295 134512640 135094434 3221224448 3221223072 134562108 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 6097 5839 145 145 0 5952 0 [pid=24912] vsize: 24388 Current children cumulated CPU time (s) 219.57 Current children cumulated vsize (Kb) 26512 [startup+230.019 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 5911 0 0 0 22925 31 0 0 25 0 1 0 1797047417 24973312 5840 4294967295 134512640 135094434 3221224448 3221223136 134554796 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 6097 5840 145 145 0 5952 0 [pid=24912] vsize: 24388 Current children cumulated CPU time (s) 229.57 Current children cumulated vsize (Kb) 26512 [startup+240.02 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 5911 0 0 0 23925 31 0 0 25 0 1 0 1797047417 24973312 5840 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 6097 5840 145 145 0 5952 0 [pid=24912] vsize: 24388 Current children cumulated CPU time (s) 239.57 Current children cumulated vsize (Kb) 26512 [startup+250.02 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 5911 0 0 0 24925 31 0 0 25 0 1 0 1797047417 24973312 5840 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 6097 5840 145 145 0 5952 0 [pid=24912] vsize: 24388 Current children cumulated CPU time (s) 249.57 Current children cumulated vsize (Kb) 26512 [startup+260.02 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 5911 0 0 0 25926 31 0 0 25 0 1 0 1797047417 24973312 5840 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 6097 5840 145 145 0 5952 0 [pid=24912] vsize: 24388 Current children cumulated CPU time (s) 259.58 Current children cumulated vsize (Kb) 26512 [startup+270.021 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 6300 0 0 0 26919 34 0 0 25 0 1 0 1797047417 26578944 6229 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 6489 6229 145 145 0 6344 0 [pid=24912] vsize: 25956 Current children cumulated CPU time (s) 269.54 Current children cumulated vsize (Kb) 28080 [startup+280.022 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 6373 0 0 0 27919 34 0 0 25 0 1 0 1797047417 26890240 6302 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 6565 6302 145 145 0 6420 0 [pid=24912] vsize: 26260 Current children cumulated CPU time (s) 279.54 Current children cumulated vsize (Kb) 28384 [startup+290.023 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 6424 0 0 0 28919 34 0 0 25 0 1 0 1797047417 27152384 6353 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 6629 6353 145 145 0 6484 0 [pid=24912] vsize: 26516 Current children cumulated CPU time (s) 289.54 Current children cumulated vsize (Kb) 28640 [startup+300.024 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 6475 0 0 0 29919 34 0 0 25 0 1 0 1797047417 27414528 6404 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 6693 6404 145 145 0 6548 0 [pid=24912] vsize: 26772 Current children cumulated CPU time (s) 299.54 Current children cumulated vsize (Kb) 28896 [startup+310.024 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 6524 0 0 0 30918 34 0 0 25 0 1 0 1797047417 27742208 6453 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 6773 6453 145 145 0 6628 0 [pid=24912] vsize: 27092 Current children cumulated CPU time (s) 309.53 Current children cumulated vsize (Kb) 29216 [startup+320.025 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 6536 0 0 0 31919 34 0 0 25 0 1 0 1797047417 27807744 6465 4294967295 134512640 135094434 3221224448 3221223040 134557236 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 6789 6465 145 145 0 6644 0 [pid=24912] vsize: 27156 Current children cumulated CPU time (s) 319.54 Current children cumulated vsize (Kb) 29280 [startup+330.026 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 6778 0 0 0 32915 36 0 0 25 0 1 0 1797047417 28794880 6707 4294967295 134512640 135094434 3221224448 3221222912 134781514 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 7030 6707 145 145 0 6885 0 [pid=24912] vsize: 28120 Current children cumulated CPU time (s) 329.52 Current children cumulated vsize (Kb) 30244 [startup+340.027 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 6786 0 0 0 33915 36 0 0 25 0 1 0 1797047417 28827648 6715 4294967295 134512640 135094434 3221224448 3221223040 134551956 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 7038 6715 145 145 0 6893 0 [pid=24912] vsize: 28152 Current children cumulated CPU time (s) 339.52 Current children cumulated vsize (Kb) 30276 [startup+350.028 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 6788 0 0 0 34916 36 0 0 25 0 1 0 1797047417 28827648 6717 4294967295 134512640 135094434 3221224448 3221223120 134555579 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 7038 6717 145 145 0 6893 0 [pid=24912] vsize: 28152 Current children cumulated CPU time (s) 349.53 Current children cumulated vsize (Kb) 30276 [startup+360.028 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 6800 0 0 0 35916 36 0 0 25 0 1 0 1797047417 28893184 6729 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 7054 6729 145 145 0 6909 0 [pid=24912] vsize: 28216 Current children cumulated CPU time (s) 359.53 Current children cumulated vsize (Kb) 30340 [startup+370.029 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 7492 0 0 0 36906 40 0 0 25 0 1 0 1797047417 31703040 7421 4294967295 134512640 135094434 3221224448 3221223040 134551457 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 7740 7421 145 145 0 7595 0 [pid=24912] vsize: 30960 Current children cumulated CPU time (s) 369.47 Current children cumulated vsize (Kb) 33084 [startup+380.03 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 7492 0 0 0 37907 40 0 0 25 0 1 0 1797047417 31703040 7421 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 7740 7421 145 145 0 7595 0 [pid=24912] vsize: 30960 Current children cumulated CPU time (s) 379.48 Current children cumulated vsize (Kb) 33084 [startup+390.032 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 7492 0 0 0 38907 41 0 0 25 0 1 0 1797047417 31703040 7421 4294967295 134512640 135094434 3221224448 3221223040 134557275 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/24912/statm): 7740 7421 145 145 0 7595 0 [pid=24912] vsize: 30960 Current children cumulated CPU time (s) 389.49 Current children cumulated vsize (Kb) 33084 [startup+400.032 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 7502 0 0 0 39906 41 0 0 25 0 1 0 1797047417 31768576 7431 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 7756 7431 145 145 0 7611 0 [pid=24912] vsize: 31024 Current children cumulated CPU time (s) 399.48 Current children cumulated vsize (Kb) 33148 [startup+410.033 s] Raw data (loadavg): 0.99 0.97 0.96 1/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) T 24908 24908 824 0 -1 0 8004 0 0 0 40897 46 0 0 25 0 1 0 1797047417 33832960 7933 4294967295 134512640 135094434 3221224448 3221222828 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0 Raw data (/proc/24912/statm): 8260 7933 145 145 0 8115 0 [pid=24912] vsize: 33040 Current children cumulated CPU time (s) 409.44 Current children cumulated vsize (Kb) 35164 [startup+420.034 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 13257 0 0 0 41854 67 0 0 25 0 1 0 1797047417 59379712 13060 4294967295 134512640 135094434 3221224448 3221223096 134670532 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 14497 13060 145 145 0 14352 0 [pid=24912] vsize: 57988 Current children cumulated CPU time (s) 419.22 Current children cumulated vsize (Kb) 60112 [startup+430.035 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 13500 0 0 0 42850 69 0 0 25 0 1 0 1797047417 60268544 13303 4294967295 134512640 135094434 3221224448 3221223072 134557650 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 14714 13303 145 145 0 14569 0 [pid=24912] vsize: 58856 Current children cumulated CPU time (s) 429.2 Current children cumulated vsize (Kb) 60980 [startup+440.035 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 13646 0 0 0 43847 70 0 0 25 0 1 0 1797047417 60866560 13449 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 14860 13449 145 145 0 14715 0 [pid=24912] vsize: 59440 Current children cumulated CPU time (s) 439.18 Current children cumulated vsize (Kb) 61564 [startup+450.036 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 13726 0 0 0 44846 70 0 0 25 0 1 0 1797047417 61194240 13529 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 14940 13529 145 145 0 14795 0 [pid=24912] vsize: 59760 Current children cumulated CPU time (s) 449.17 Current children cumulated vsize (Kb) 61884 [startup+460.037 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 13878 0 0 0 45843 71 0 0 25 0 1 0 1797047417 61784064 13681 4294967295 134512640 135094434 3221224448 3221223104 134558276 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 15084 13681 145 145 0 14939 0 [pid=24912] vsize: 60336 Current children cumulated CPU time (s) 459.15 Current children cumulated vsize (Kb) 62460 [startup+470.038 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 14119 0 0 0 46837 74 0 0 25 0 1 0 1797047417 62771200 13922 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 15325 13922 145 145 0 15180 0 [pid=24912] vsize: 61300 Current children cumulated CPU time (s) 469.12 Current children cumulated vsize (Kb) 63424 [startup+480.037 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 14422 0 0 0 47832 76 0 0 25 0 1 0 1797047417 64004096 14225 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 15626 14225 145 145 0 15481 0 [pid=24912] vsize: 62504 Current children cumulated CPU time (s) 479.09 Current children cumulated vsize (Kb) 64628 [startup+490.038 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 14834 0 0 0 48825 79 0 0 25 0 1 0 1797047417 65691648 14637 4294967295 134512640 135094434 3221224448 3221223072 134557585 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 16038 14637 145 145 0 15893 0 [pid=24912] vsize: 64152 Current children cumulated CPU time (s) 489.05 Current children cumulated vsize (Kb) 66276 [startup+500.039 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 15065 0 0 0 49822 80 0 0 25 0 1 0 1797047417 66633728 14868 4294967295 134512640 135094434 3221224448 3221223060 134563043 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 16268 14868 145 145 0 16123 0 [pid=24912] vsize: 65072 Current children cumulated CPU time (s) 499.03 Current children cumulated vsize (Kb) 67196 [startup+510.038 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 15307 0 0 0 50817 82 0 0 25 0 1 0 1797047417 67596288 15110 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 16503 15110 145 145 0 16358 0 [pid=24912] vsize: 66012 Current children cumulated CPU time (s) 509 Current children cumulated vsize (Kb) 68136 [startup+520.039 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 15636 0 0 0 51812 85 0 0 25 0 1 0 1797047417 68947968 15439 4294967295 134512640 135094434 3221224448 3221223040 134557421 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 16833 15439 145 145 0 16688 0 [pid=24912] vsize: 67332 Current children cumulated CPU time (s) 518.98 Current children cumulated vsize (Kb) 69456 [startup+530.04 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 16047 0 0 0 52805 88 0 0 25 0 1 0 1797047417 70594560 15850 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 17235 15850 145 145 0 17090 0 [pid=24912] vsize: 68940 Current children cumulated CPU time (s) 528.94 Current children cumulated vsize (Kb) 71064 [startup+540.041 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 16949 0 0 0 53788 96 0 0 25 0 1 0 1797047417 74772480 16752 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 18255 16752 145 145 0 18110 0 [pid=24912] vsize: 73020 Current children cumulated CPU time (s) 538.85 Current children cumulated vsize (Kb) 75144 [startup+550.042 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 17365 0 0 0 54780 100 0 0 25 0 1 0 1797047417 76468224 17168 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 18669 17168 145 145 0 18524 0 [pid=24912] vsize: 74676 Current children cumulated CPU time (s) 548.81 Current children cumulated vsize (Kb) 76800 [startup+560.042 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 17498 0 0 0 55777 101 0 0 25 0 1 0 1797047417 77004800 17301 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 18800 17301 145 145 0 18655 0 [pid=24912] vsize: 75200 Current children cumulated CPU time (s) 558.79 Current children cumulated vsize (Kb) 77324 [startup+570.043 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 17720 0 0 0 56775 102 0 0 25 0 1 0 1797047417 77934592 17523 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 19027 17523 145 145 0 18882 0 [pid=24912] vsize: 76108 Current children cumulated CPU time (s) 568.78 Current children cumulated vsize (Kb) 78232 [startup+580.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 18014 0 0 0 57770 104 0 0 25 0 1 0 1797047417 79138816 17817 4294967295 134512640 135094434 3221224448 3221223092 134558261 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 19321 17817 145 145 0 19176 0 [pid=24912] vsize: 77284 Current children cumulated CPU time (s) 578.75 Current children cumulated vsize (Kb) 79408 [startup+590.044 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 18380 0 0 0 58764 107 0 0 25 0 1 0 1797047417 80609280 18183 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 19680 18183 145 145 0 19535 0 [pid=24912] vsize: 78720 Current children cumulated CPU time (s) 588.72 Current children cumulated vsize (Kb) 80844 [startup+600.045 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 18567 0 0 0 59761 109 0 0 25 0 1 0 1797047417 81362944 18370 4294967295 134512640 135094434 3221224448 3221223076 134557637 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 19864 18370 145 145 0 19719 0 [pid=24912] vsize: 79456 Current children cumulated CPU time (s) 598.71 Current children cumulated vsize (Kb) 81580 [startup+610.045 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 18780 0 0 0 60757 110 0 0 25 0 1 0 1797047417 82214912 18583 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 20072 18583 145 145 0 19927 0 [pid=24912] vsize: 80288 Current children cumulated CPU time (s) 608.68 Current children cumulated vsize (Kb) 82412 [startup+620.046 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 18911 0 0 0 61754 112 0 0 25 0 1 0 1797047417 82735104 18714 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 20199 18714 145 145 0 20054 0 [pid=24912] vsize: 80796 Current children cumulated CPU time (s) 618.67 Current children cumulated vsize (Kb) 82920 [startup+630.046 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 19214 0 0 0 62748 114 0 0 25 0 1 0 1797047417 83947520 19017 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 20495 19017 145 145 0 20350 0 [pid=24912] vsize: 81980 Current children cumulated CPU time (s) 628.63 Current children cumulated vsize (Kb) 84104 [startup+640.047 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 19659 0 0 0 63739 117 0 0 25 0 1 0 1797047417 85753856 19462 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 20936 19462 145 145 0 20791 0 [pid=24912] vsize: 83744 Current children cumulated CPU time (s) 638.57 Current children cumulated vsize (Kb) 85868 [startup+650.048 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 19958 0 0 0 64733 120 0 0 25 0 1 0 1797047417 86953984 19761 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 21229 19761 145 145 0 21084 0 [pid=24912] vsize: 84916 Current children cumulated CPU time (s) 648.54 Current children cumulated vsize (Kb) 87040 [startup+660.048 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 20260 0 0 0 65728 122 0 0 25 0 1 0 1797047417 88166400 20063 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 21525 20063 145 145 0 21380 0 [pid=24912] vsize: 86100 Current children cumulated CPU time (s) 658.51 Current children cumulated vsize (Kb) 88224 [startup+670.048 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 20497 0 0 0 66725 124 0 0 25 0 1 0 1797047417 89112576 20300 4294967295 134512640 135094434 3221224448 3221223040 134557002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 21756 20300 145 145 0 21611 0 [pid=24912] vsize: 87024 Current children cumulated CPU time (s) 668.5 Current children cumulated vsize (Kb) 89148 [startup+680.049 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21037 0 0 0 67722 126 0 0 25 0 1 0 1797047417 90710016 20675 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20675 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 678.49 Current children cumulated vsize (Kb) 90708 [startup+690.05 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21037 0 0 0 68722 126 0 0 25 0 1 0 1797047417 90710016 20675 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20675 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 688.49 Current children cumulated vsize (Kb) 90708 [startup+700.051 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21037 0 0 0 69722 126 0 0 25 0 1 0 1797047417 90710016 20675 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20675 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 698.49 Current children cumulated vsize (Kb) 90708 [startup+710.051 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21037 0 0 0 70722 126 0 0 25 0 1 0 1797047417 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20675 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 708.49 Current children cumulated vsize (Kb) 90708 [startup+720.052 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21037 0 0 0 71723 126 0 0 25 0 1 0 1797047417 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20675 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 718.5 Current children cumulated vsize (Kb) 90708 [startup+730.053 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21037 0 0 0 72723 126 0 0 25 0 1 0 1797047417 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20675 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 728.5 Current children cumulated vsize (Kb) 90708 [startup+740.055 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21037 0 0 0 73723 126 0 0 25 0 1 0 1797047417 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20675 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 738.5 Current children cumulated vsize (Kb) 90708 [startup+750.055 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21037 0 0 0 74723 126 0 0 25 0 1 0 1797047417 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134557818 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20675 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 748.5 Current children cumulated vsize (Kb) 90708 [startup+760.056 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21037 0 0 0 75724 126 0 0 25 0 1 0 1797047417 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20675 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 758.51 Current children cumulated vsize (Kb) 90708 [startup+770.057 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21037 0 0 0 76724 126 0 0 25 0 1 0 1797047417 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20675 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 768.51 Current children cumulated vsize (Kb) 90708 [startup+780.057 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21037 0 0 0 77724 126 0 0 25 0 1 0 1797047417 90710016 20675 4294967295 134512640 135094434 3221224448 3221223072 134562085 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20675 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 778.51 Current children cumulated vsize (Kb) 90708 [startup+790.057 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21037 0 0 0 78724 126 0 0 25 0 1 0 1797047417 90710016 20675 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20675 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 788.51 Current children cumulated vsize (Kb) 90708 [startup+800.058 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21037 0 0 0 79724 126 0 0 25 0 1 0 1797047417 90710016 20675 4294967295 134512640 135094434 3221224448 3221223072 134557598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20675 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 798.51 Current children cumulated vsize (Kb) 90708 [startup+810.059 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21037 0 0 0 80725 126 0 0 25 0 1 0 1797047417 90710016 20675 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20675 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 808.52 Current children cumulated vsize (Kb) 90708 [startup+820.059 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21038 0 0 0 81725 126 0 0 25 0 1 0 1797047417 90710016 20676 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20676 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 818.52 Current children cumulated vsize (Kb) 90708 [startup+830.06 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21038 0 0 0 82725 126 0 0 25 0 1 0 1797047417 90710016 20676 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20676 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 828.52 Current children cumulated vsize (Kb) 90708 [startup+840.061 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21041 0 0 0 83725 126 0 0 25 0 1 0 1797047417 90710016 20679 4294967295 134512640 135094434 3221224448 3221223104 134558153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20679 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 838.52 Current children cumulated vsize (Kb) 90708 [startup+850.062 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21041 0 0 0 84726 126 0 0 25 0 1 0 1797047417 90710016 20679 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20679 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 848.53 Current children cumulated vsize (Kb) 90708 [startup+860.062 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21041 0 0 0 85726 126 0 0 25 0 1 0 1797047417 90710016 20679 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20679 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 858.53 Current children cumulated vsize (Kb) 90708 [startup+870.063 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21041 0 0 0 86726 126 0 0 25 0 1 0 1797047417 90710016 20679 4294967295 134512640 135094434 3221224448 3221223040 134556791 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20679 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 868.53 Current children cumulated vsize (Kb) 90708 [startup+880.064 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21041 0 0 0 87726 126 0 0 25 0 1 0 1797047417 90710016 20679 4294967295 134512640 135094434 3221224448 3221223104 134558002 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20679 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 878.53 Current children cumulated vsize (Kb) 90708 [startup+890.066 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21041 0 0 0 88727 126 0 0 25 0 1 0 1797047417 90710016 20679 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20679 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 888.54 Current children cumulated vsize (Kb) 90708 [startup+900.066 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21041 0 0 0 89727 126 0 0 25 0 1 0 1797047417 90710016 20679 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20679 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 898.54 Current children cumulated vsize (Kb) 90708 [startup+910.067 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21041 0 0 0 90727 126 0 0 25 0 1 0 1797047417 90710016 20679 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20679 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 908.54 Current children cumulated vsize (Kb) 90708 [startup+920.069 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21041 0 0 0 91727 126 0 0 25 0 1 0 1797047417 90710016 20679 4294967295 134512640 135094434 3221224448 3221223040 134556987 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20679 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 918.54 Current children cumulated vsize (Kb) 90708 [startup+930.069 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21042 0 0 0 92727 126 0 0 25 0 1 0 1797047417 90710016 20680 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20680 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 928.54 Current children cumulated vsize (Kb) 90708 [startup+940.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21042 0 0 0 93728 126 0 0 25 0 1 0 1797047417 90710016 20680 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20680 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 938.55 Current children cumulated vsize (Kb) 90708 [startup+950.071 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21042 0 0 0 94728 126 0 0 25 0 1 0 1797047417 90710016 20680 4294967295 134512640 135094434 3221224448 3221223104 134558402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20680 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 948.55 Current children cumulated vsize (Kb) 90708 [startup+960.071 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21042 0 0 0 95728 126 0 0 25 0 1 0 1797047417 90710016 20680 4294967295 134512640 135094434 3221224448 3221223040 134557111 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20680 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 958.55 Current children cumulated vsize (Kb) 90708 [startup+970.072 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21042 0 0 0 96728 126 0 0 25 0 1 0 1797047417 90710016 20680 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20680 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 968.55 Current children cumulated vsize (Kb) 90708 [startup+980.072 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21042 0 0 0 97728 127 0 0 25 0 1 0 1797047417 90710016 20680 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20680 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 978.56 Current children cumulated vsize (Kb) 90708 [startup+990.073 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21042 0 0 0 98729 127 0 0 25 0 1 0 1797047417 90710016 20680 4294967295 134512640 135094434 3221224448 3221223092 134558040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20680 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 988.57 Current children cumulated vsize (Kb) 90708 [startup+1000.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21042 0 0 0 99729 127 0 0 25 0 1 0 1797047417 90710016 20680 4294967295 134512640 135094434 3221224448 3221222928 134781309 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20680 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 998.57 Current children cumulated vsize (Kb) 90708 [startup+1010.07 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21043 0 0 0 100729 127 0 0 25 0 1 0 1797047417 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20681 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 1008.57 Current children cumulated vsize (Kb) 90708 [startup+1020.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21043 0 0 0 101729 127 0 0 25 0 1 0 1797047417 90710016 20681 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20681 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 1018.57 Current children cumulated vsize (Kb) 90708 [startup+1030.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21043 0 0 0 102729 127 0 0 25 0 1 0 1797047417 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20681 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 1028.57 Current children cumulated vsize (Kb) 90708 [startup+1040.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21043 0 0 0 103730 127 0 0 25 0 1 0 1797047417 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20681 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 1038.58 Current children cumulated vsize (Kb) 90708 [startup+1050.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21043 0 0 0 104730 127 0 0 25 0 1 0 1797047417 90710016 20681 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20681 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 1048.58 Current children cumulated vsize (Kb) 90708 [startup+1060.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21043 0 0 0 105730 127 0 0 25 0 1 0 1797047417 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20681 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 1058.58 Current children cumulated vsize (Kb) 90708 [startup+1070.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21043 0 0 0 106730 127 0 0 25 0 1 0 1797047417 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20681 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 1068.58 Current children cumulated vsize (Kb) 90708 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21043 0 0 0 107730 127 0 0 25 0 1 0 1797047417 90710016 20681 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20681 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 1078.58 Current children cumulated vsize (Kb) 90708 [startup+1090.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21043 0 0 0 108731 127 0 0 25 0 1 0 1797047417 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20681 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 1088.59 Current children cumulated vsize (Kb) 90708 [startup+1100.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21043 0 0 0 109731 127 0 0 25 0 1 0 1797047417 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20681 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 1098.59 Current children cumulated vsize (Kb) 90708 [startup+1110.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21043 0 0 0 110731 127 0 0 25 0 1 0 1797047417 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20681 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 1108.59 Current children cumulated vsize (Kb) 90708 [startup+1120.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21043 0 0 0 111732 127 0 0 25 0 1 0 1797047417 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20681 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 1118.6 Current children cumulated vsize (Kb) 90708 [startup+1130.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21043 0 0 0 112732 127 0 0 25 0 1 0 1797047417 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20681 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 1128.6 Current children cumulated vsize (Kb) 90708 [startup+1140.08 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21043 0 0 0 113732 127 0 0 25 0 1 0 1797047417 90710016 20681 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20681 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 1138.6 Current children cumulated vsize (Kb) 90708 [startup+1150.09 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21043 0 0 0 114732 127 0 0 25 0 1 0 1797047417 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134558392 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20681 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 1148.6 Current children cumulated vsize (Kb) 90708 [startup+1160.09 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21043 0 0 0 115733 127 0 0 25 0 1 0 1797047417 90710016 20681 4294967295 134512640 135094434 3221224448 3221223072 134557612 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20681 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 1158.61 Current children cumulated vsize (Kb) 90708 [startup+1170.09 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21043 0 0 0 116733 127 0 0 25 0 1 0 1797047417 90710016 20681 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20681 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 1168.61 Current children cumulated vsize (Kb) 90708 [startup+1180.09 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21045 0 0 0 117733 127 0 0 25 0 1 0 1797047417 90710016 20683 4294967295 134512640 135094434 3221224448 3221223104 134558284 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20683 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 1178.61 Current children cumulated vsize (Kb) 90708 [startup+1190.09 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21045 0 0 0 118733 127 0 0 25 0 1 0 1797047417 90710016 20683 4294967295 134512640 135094434 3221224448 3221223040 134556773 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20683 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 1188.61 Current children cumulated vsize (Kb) 90708 [startup+1200.09 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21045 0 0 0 119734 127 0 0 25 0 1 0 1797047417 90710016 20683 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20683 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 1198.62 Current children cumulated vsize (Kb) 90708 [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21045 0 0 0 120734 127 0 0 25 0 1 0 1797047417 90710016 20683 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20683 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 1208.62 Current children cumulated vsize (Kb) 90708 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 0.99 0.97 0.96 2/57 24912 Raw data (/proc/24908/stat): 24908 (minisat+_script) S 24907 24908 824 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1797047412 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/24908/statm): 531 226 485 147 0 384 0 [pid=24908] vsize: 2124 Raw data (/proc/24912/stat): 24912 (minisat+_64-bit) R 24908 24908 824 0 -1 0 21045 0 0 0 120734 127 0 0 25 0 1 0 1797047417 90710016 20683 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/24912/statm): 22146 20683 145 145 0 22001 0 [pid=24912] vsize: 88584 Current children cumulated CPU time (s) 1208.62 Current children cumulated vsize (Kb) 90708 Sending SIGTERM to -24908 Sleeping 2 seconds One traced child (pid=24908) ended because it received signal 15 (SIGTERM) One traced child (pid=24912) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.14 CPU time (s): 1208.66 CPU user time (s): 1207.35 CPU system time (s): 1.3138 CPU usage (%): 99.8775 Max. virtual memory (cumulated for all children) (Kb): 90708
ERROR: no interpretation found !